English
A dependent version of Subgroup.iSup_induction: given a family S_i of subgroups and a predicate depending on the index i and membership in ⨆ i, S_i, the conclusion follows by an induction on the iSup-structure.
Русский
Зависимая версия Subgroup.iSup_induction: дано семейство подпгрупп S_i и предикат, зависящий от i и от принадлежности элемента ⨆ i, S_i; заключение следует по индукции на структуре iSup.
LaTeX
$$$\\text{Dependent induction on } iSup: \\; {S_i},\\; C:\\forall x,(x\\in \\bigvee_i S_i)\\to\\Prop,\\; \\dots \\Rightarrow C x hx.$$$
Lean4
@[to_additive]
instance sup_normal (H K : Subgroup G) [hH : H.Normal] [hK : K.Normal] : (H ⊔ K).Normal where
conj_mem n hmem
g := by
rw [← SetLike.mem_coe, normal_mul] at hmem ⊢
rcases hmem with ⟨h, hh, k, hk, rfl⟩
refine ⟨g * h * g⁻¹, hH.conj_mem h hh g, g * k * g⁻¹, hK.conj_mem k hk g, ?_⟩
simp only [mul_assoc, inv_mul_cancel_left]
