Width.lean

def IsProductOfCommutatorsAlongInSubgroup
    {G : Type u} [Group G] (A : Subgroup G) {n : ℕ}
    (x : Fin n → G) (g : G) : Prop

def IsProductOfCommutatorsAlongPairInSubgroup
    {G : Type u} [Group G] (A : Subgroup G) {m n : ℕ}
    (x : Fin m → G) (y : Fin n → G) (g : G) : Prop

theorem IsProductOfCommutatorsAlongInSubgroup.mono
    {G : Type u} [Group G] {A B : Subgroup G} {n : ℕ}
    {x : Fin n → G} {g : G}
    (hAB : A ≤ B)
    (h : IsProductOfCommutatorsAlongInSubgroup A x g) :
    IsProductOfCommutatorsAlongInSubgroup B x g

theorem IsProductOfCommutatorsAlongInSubgroup.map
    {G H : Type u} [Group G] [Group H] {A : Subgroup G} {n : ℕ}
    {x : Fin n → G} {g : G}
    (f : G →* H)
    (h : IsProductOfCommutatorsAlongInSubgroup A x g) :
    IsProductOfCommutatorsAlongInSubgroup (A.map f) (fun i => f (x i)) (f g) := by
    rcases h with ⟨a, ha, hprod⟩
    refine ⟨fun i => f (a i), ?_, ?_⟩
    · intro i
      exact ⟨a i, ha i, rfl⟩
    · let l : List (G × G) := List.ofFn fun i : Fin n => (a i, x i)
      have hmapList :
          ∀ l : List (G × G),
            f ((l.map fun p : G × G => ⁅p.1, p.2⁆).prod) =
              (l.map fun p : G × G => ⁅f p.1, f p.2⁆).prod := by
        intro l
        induction l with
        | nil =>
            simp only [List.map_nil, List.prod_nil, map_one]
        | cons p t ih =>
            simp only [List.map_cons, List.prod_cons, map_mul, map_commutatorElement, ih]
      calc
        (List.ofFn fun i : Fin n => ⁅f (a i), f (x i)⁆).prod =
            (l.map fun p : G × G => ⁅f p.1, f p.2⁆).prod := by
              dsimp [l]
              rw [List.map_ofFn]
              rfl
        _ = f ((l.map fun p : G × G => ⁅p.1, p.2⁆).prod) := (hmapList l).symm
        _ = f g := by
              have hcommList :
                  (l.map fun p : G × G => ⁅p.1, p.2⁆) =
                    List.ofFn (fun i : Fin n => ⁅a i, x i⁆) := by
                dsimp [l]
                rw [List.map_ofFn]
                rfl
              rw [hcommList, hprod]

theorem IsProductOfCommutatorsAlongInSubgroup.mul
    {G : Type u} [Group G] {A : Subgroup G} {m n : ℕ}
    {x : Fin m → G} {y : Fin n → G} {g h : G}
    (hg : IsProductOfCommutatorsAlongInSubgroup A x g)
    (hh : IsProductOfCommutatorsAlongInSubgroup A y h) :
    IsProductOfCommutatorsAlongInSubgroup A (Fin.append x y) (g * h)

theorem exists_generating_family_of_rank_le
    {K : Type u} [Group K] [Group.FG K] {d : ℕ}
    (hd : Group.rank K ≤ d) :
    ∃ x : Fin d → K, Subgroup.closure (Set.range x) = (⊤ : Subgroup K)

theorem exists_normalGenerators_of_split_group_of_rank_le
    {K : Type u} [Group K] [Group.FG K] {H L : Subgroup K} [_hH : H.Normal]
    (hsplit : IsCompl H L) {d : ℕ} (hd : Group.rank K ≤ d) :
    ∃ y : Fin d → K, Subgroup.normalClosure (Set.range y) = H