awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.GroupTheory.PushoutI (goal)
Goal:
ι : Type u_1
G : ι → Type u_2
H : Type u_3
inst : (i : ι) → Group (G i)
inst_1 : Group H
φ : (i : ι) → MonoidHom.{u_3, u_2} H (G i)
d : Transversal (G := G) φ
i : ι
g : G i
w : Word G
hIdx : w.fstIdx (M := G) ≠ some i
hg1 : g ≠ 1
ih :
  ∀ (hw : Reduced (G := G) φ w),
    ∃ (w' : NormalWord (G := G) d),
      w'.prod (G := G) = (ofCoprodI (G := G) : (a : CoprodI G) → PushoutI φ) (w.prod (M := G)) ∧
        List.map (Sigma.fst (β := fun (i : ι) ↦ G i)) (w'.toWord (G := G).toList (M := G)) =
          List.map (Sigma.fst (β := fun (i : ι) ↦ G i)) (w.toList (M := G))
hw : Reduced (G := G) φ (Word.cons (M := G) g w hIdx hg1)
⊢ ∃ (w' : NormalWord (G := G) d),
    w'.prod (G := G) =
        (ofCoprodI (G := G) : (a : CoprodI G) → PushoutI φ) ((Word.cons (M := G) g w hIdx hg1).prod (M := G)) ∧
      List.map (Sigma.fst (β := fun (i : ι) ↦ G i)) (w'.toWord (G := G).toList (M := G)) =
        List.map (Sigma.fst (β := fun (i : ι) ↦ G i)) ((Word.cons (M := G) g w hIdx hg1).toList (M := G))
have cons : ∀ (w' : NormalWord (G := G) d)
  (hw'prod : w'.prod (G := G) = (ofCoprodI (G := G) : (a : CoprodI G) → PushoutI φ) (w.prod (M := G)))
  (hw'map :
    List.map (Sigma.fst (β := fun (i : ι) ↦ G i)) (w'.toWord (G := G).toList (M := G)) =
      List.map (Sigma.fst (β := fun (i : ι) ↦ G i)) (w.toList (M := G))),
  ∃ (w' : NormalWord (G := G) d),
    w'.prod (G := G) =
        (ofCoprodI (G := G) : (a : CoprodI G) → PushoutI φ) ((Word.cons (M := G) g w hIdx hg1).prod (M := G)) ∧
      List.map (Sigma.fst (β := fun (i : ι) ↦ G i)) (w'.toWord (G := G).toList (M := G)) =
        List.map (Sigma.fst (β := fun (i : ι) ↦ G i)) ((Word.cons (M := G) g w hIdx hg1).toList (M := G))
Tactic: rcases ih (fun _ hg => hw _ (List.mem_cons_of_mem _ hg)) with
      ⟨w', hw'prod, hw'map⟩
-- Lean 4 proof step from Mathlib.GroupTheory.PushoutI (goal)
Goal:
ι : Type u_1
G : ι → Type u_2
H : Type u_3
inst : (i : ι) → Group (G i)
inst_1 : Group H
φ : (i : ι) → MonoidHom.{u_3, u_2} H (G i)
d : Transversal (G := G) φ
i : ι
g : G i
w : Word G
hIdx : w.fstIdx (M := G) ≠ some i
hg1 : g ≠ 1
ih :
  ∀ (hw : Reduced (G := G) φ w),
    ∃ (w' : NormalWord (G := G) d),
      w'.prod (G := G) = (ofCoprodI (G := G) : (a : CoprodI G) → PushoutI φ) (w.prod (M := G)) ∧
        List.map (Sigma.fst (β := fun (i : ι) ↦ G i)) (w'.toWord (G := G).toList (M := G)) =
          List.map (Sigma.fst (β := fun (i : ι) ↦ G i)) (w.toList (M := G))
hw : Reduced (G := G) φ (Word.cons (M := G) g w hIdx hg1)
w' : NormalWord (G := G) d
hw'prod : w'.prod (G := G) = (ofCoprodI (G := G) : (a : CoprodI G) → PushoutI φ) (w.prod (M := G))
hw'map :
  List.map (Sigma.fst (β := fun (i : ι) ↦ G i)) (w'.toWord (G := G).toList (M := G)) =
    List.map (Sigma.fst (β := fun (i : ι) ↦ G i)) (w.toList (M := G))
⊢ ∃ (w' : NormalWord (G := G) d),
    w'.prod (G := G) =
        (ofCoprodI (G := G) : (a : CoprodI G) → PushoutI φ) ((Word.cons (M := G) g w hIdx hg1).prod (M := G)) ∧
      List.map (Sigma.fst (β := fun (i : ι) ↦ G i)) (w'.toWord (G := G).toList (M := G)) =
        List.map (Sigma.fst (β := fun (i : ι) ↦ G i)) ((Word.cons (M := G) g w hIdx hg1).toList (M := G))
have cons : w'.toWord (G := G).fstIdx (M := G) ≠ some i
Tactic: refine ⟨cons g w' ?_ ?_, ?_⟩
-- Lean 4 proof step from Mathlib.GroupTheory.PushoutI (goal)
Goal:
ι : Type u_1
G : ι → Type u_2
H : Type u_3
inst : (i : ι) → Group (G i)
inst_1 : Group H
φ : (i : ι) → MonoidHom.{u_3, u_2} H (G i)
d : Transversal (G := G) φ
i : ι
g : G i
w : Word G
hIdx : w.fstIdx (M := G) ≠ some i
hg1 : g ≠ 1
ih :
  ∀ (hw : Reduced (G := G) φ w),
    ∃ (w' : NormalWord (G := G) d),
      w'.prod (G := G) = (ofCoprodI (G := G) : (a : CoprodI G) → PushoutI φ) (w.prod (M := G)) ∧
        List.map (Sigma.fst (β := fun (i : ι) ↦ G i)) (w'.toWord (G := G).toList (M := G)) =
          List.map (Sigma.fst (β := fun (i : ι) ↦ G i)) (w.toList (M := G))
hw : Reduced (G := G) φ (Word.cons (M := G) g w hIdx hg1)
w' : NormalWord (G := G) d
hw'prod : w'.prod (G := G) = (ofCoprodI (G := G) : (a : CoprodI G) → PushoutI φ) (w.prod (M := G))
hw'map :
  List.map (Sigma.fst (β := fun (i : ι) ↦ G i)) (w'.toWord (G := G).toList (M := G)) =
    List.map (Sigma.fst (β := fun (i : ι) ↦ G i)) (w.toList (M := G))
cons : w'.toWord (G := G).fstIdx (M := G) ≠ some i
⊢ ∃ (w' : NormalWord (G := G) d),
    w'.prod (G := G) =
        (ofCoprodI (G := G) : (a : CoprodI G) → PushoutI φ) ((Word.cons (M := G) g w hIdx hg1).prod (M := G)) ∧
      List.map (Sigma.fst (β := fun (i : ι) ↦ G i)) (w'.toWord (G := G).toList (M := G)) =
        List.map (Sigma.fst (β := fun (i : ι) ↦ G i)) ((Word.cons (M := G) g w hIdx hg1).toList (M := G))
have cons₁ : g ∉ (φ i).range
Tactic: refine ⟨cons g w' ?_ ?_, ?_⟩
-- Lean 4 proof step from Mathlib.GroupTheory.PushoutI (goal)
Goal:
ι : Type u_1
G : ι → Type u_2
H : Type u_3
inst : (i : ι) → Group (G i)
inst_1 : Group H
φ : (i : ι) → MonoidHom.{u_3, u_2} H (G i)
d : Transversal (G := G) φ
i : ι
g : G i
w : Word G
hIdx : w.fstIdx (M := G) ≠ some i
hg1 : g ≠ 1
ih :
  ∀ (hw : Reduced (G := G) φ w),
    ∃ (w' : NormalWord (G := G) d),
      w'.prod (G := G) = (ofCoprodI (G := G) : (a : CoprodI G) → PushoutI φ) (w.prod (M := G)) ∧
        List.map (Sigma.fst (β := fun (i : ι) ↦ G i)) (w'.toWord (G := G).toList (M := G)) =
          List.map (Sigma.fst (β := fun (i : ι) ↦ G i)) (w.toList (M := G))
hw : Reduced (G := G) φ (Word.cons (M := G) g w hIdx hg1)
w' : NormalWord (G := G) d
hw'prod : w'.prod (G := G) = (ofCoprodI (G := G) : (a : CoprodI G) → PushoutI φ) (w.prod (M := G))
hw'map :
  List.map (Sigma.fst (β := fun (i : ι) ↦ G i)) (w'.toWord (G := G).toList (M := G)) =
    List.map (Sigma.fst (β := fun (i : ι) ↦ G i)) (w.toList (M := G))
cons : w'.toWord (G := G).fstIdx (M := G) ≠ some i
cons₁ : g ∉ (φ i).range
⊢ ∃ (w' : NormalWord (G := G) d),
    w'.prod (G := G) =
        (ofCoprodI (G := G) : (a : CoprodI G) → PushoutI φ) ((Word.cons (M := G) g w hIdx hg1).prod (M := G)) ∧
      List.map (Sigma.fst (β := fun (i : ι) ↦ G i)) (w'.toWord (G := G).toList (M := G)) =
        List.map (Sigma.fst (β := fun (i : ι) ↦ G i)) ((Word.cons (M := G) g w hIdx hg1).toList (M := G))
have cons₂ : (NormalWord.cons (G := G) g w' sorry sorry).prod (G := G) =
    (ofCoprodI (G := G) : (a : CoprodI G) → PushoutI φ) ((Word.cons (M := G) g w hIdx hg1).prod (M := G)) ∧
  List.map (Sigma.fst (β := fun (i : ι) ↦ G i)) ((NormalWord.cons (G := G) g w' sorry sorry).toWord (G := G).toList (M := G)) =
    List.map (Sigma.fst (β := fun (i : ι) ↦ G i)) ((Word.cons (M := G) g w hIdx hg1).toList (M := G))
Tactic: refine ⟨cons g w' ?_ ?_, ?_⟩
-- Lean 4 proof step from Mathlib.GroupTheory.PushoutI (goal)
Goal:
ι : Type u_1
G : ι → Type u_2
H : Type u_3
inst : (i : ι) → Group (G i)
inst_1 : Group H
φ : (i : ι) → MonoidHom.{u_3, u_2} H (G i)
d : Transversal (G := G) φ
i : ι
g : G i
w : Word G
hIdx : w.fstIdx (M := G) ≠ some i
hg1 : g ≠ 1
ih :
  ∀ (hw : Reduced (G := G) φ w),
    ∃ (w' : NormalWord (G := G) d),
      w'.prod (G := G) = (ofCoprodI (G := G) : (a : CoprodI G) → PushoutI φ) (w.prod (M := G)) ∧
        List.map (Sigma.fst (β := fun (i : ι) ↦ G i)) (w'.toWord (G := G).toList (M := G)) =
          List.map (Sigma.fst (β := fun (i : ι) ↦ G i)) (w.toList (M := G))
hw : Reduced (G := G) φ (Word.cons (M := G) g w hIdx hg1)
w' : NormalWord (G := G) d
hw'prod : w'.prod (G := G) = (ofCoprodI (G := G) : (a : CoprodI G) → PushoutI φ) (w.prod (M := G))
hw'map :
  List.map (Sigma.fst (β := fun (i : ι) ↦ G i)) (w'.toWord (G := G).toList (M := G)) =
    List.map (Sigma.fst (β := fun (i : ι) ↦ G i)) (w.toList (M := G))
⊢ w'.toWord (G := G).fstIdx (M := G) ≠ some i
have cons : Option.map (Sigma.fst (β := fun (i : ι) ↦ G i)) w'.toWord (G := G).toList (M := G).head? ≠ some i
Tactic: rwa [Word.fstIdx, ← List.head?_map, hw'map, List.head?_map]
-- Lean 4 proof step from Mathlib.GroupTheory.PushoutI (goal)
Goal:
ι : Type u_1
G : ι → Type u_2
H : Type u_3
inst : (i : ι) → Group (G i)
inst_1 : Group H
φ : (i : ι) → MonoidHom.{u_3, u_2} H (G i)
d : Transversal (G := G) φ
i : ι
g : G i
w : Word G
hIdx : w.fstIdx (M := G) ≠ some i
hg1 : g ≠ 1
ih :
  ∀ (hw : Reduced (G := G) φ w),
    ∃ (w' : NormalWord (G := G) d),
      w'.prod (G := G) = (ofCoprodI (G := G) : (a : CoprodI G) → PushoutI φ) (w.prod (M := G)) ∧
        List.map (Sigma.fst (β := fun (i : ι) ↦ G i)) (w'.toWord (G := G).toList (M := G)) =
          List.map (Sigma.fst (β := fun (i : ι) ↦ G i)) (w.toList (M := G))
hw : Reduced (G := G) φ (Word.cons (M := G) g w hIdx hg1)
w' : NormalWord (G := G) d
hw'prod : w'.prod (G := G) = (ofCoprodI (G := G) : (a : CoprodI G) → PushoutI φ) (w.prod (M := G))
hw'map :
  List.map (Sigma.fst (β := fun (i : ι) ↦ G i)) (w'.toWord (G := G).toList (M := G)) =
    List.map (Sigma.fst (β := fun (i : ι) ↦ G i)) (w.toList (M := G))
cons : Option.map (Sigma.fst (β := fun (i : ι) ↦ G i)) w'.toWord (G := G).toList (M := G).head? ≠ some i
⊢ w'.toWord (G := G).fstIdx (M := G) ≠ some i
have cons₁ : (List.map (Sigma.fst (β := fun (i : ι) ↦ G i)) (w'.toWord (G := G).toList (M := G))).head? ≠ some i
Tactic: rwa [Word.fstIdx, ← List.head?_map, hw'map, List.head?_map]
-- Lean 4 proof step from Mathlib.GroupTheory.PushoutI (goal)
Goal:
ι : Type u_1
G : ι → Type u_2
H : Type u_3
inst : (i : ι) → Group (G i)
inst_1 : Group H
φ : (i : ι) → MonoidHom.{u_3, u_2} H (G i)
d : Transversal (G := G) φ
i : ι
g : G i
w : Word G
hIdx : w.fstIdx (M := G) ≠ some i
hg1 : g ≠ 1
ih :
  ∀ (hw : Reduced (G := G) φ w),
    ∃ (w' : NormalWord (G := G) d),
      w'.prod (G := G) = (ofCoprodI (G := G) : (a : CoprodI G) → PushoutI φ) (w.prod (M := G)) ∧
        List.map (Sigma.fst (β := fun (i : ι) ↦ G i)) (w'.toWord (G := G).toList (M := G)) =
          List.map (Sigma.fst (β := fun (i : ι) ↦ G i)) (w.toList (M := G))
hw : Reduced (G := G) φ (Word.cons (M := G) g w hIdx hg1)
w' : NormalWord (G := G) d
hw'prod : w'.prod (G := G) = (ofCoprodI (G := G) : (a : CoprodI G) → PushoutI φ) (w.prod (M := G))
hw'map :
  List.map (Sigma.fst (β := fun (i : ι) ↦ G i)) (w'.toWord (G := G).toList (M := G)) =
    List.map (Sigma.fst (β := fun (i : ι) ↦ G i)) (w.toList (M := G))
cons : Option.map (Sigma.fst (β := fun (i : ι) ↦ G i)) w'.toWord (G := G).toList (M := G).head? ≠ some i
cons₁ : (List.map (Sigma.fst (β := fun (i : ι) ↦ G i)) (w'.toWord (G := G).toList (M := G))).head? ≠ some i
⊢ w'.toWord (G := G).fstIdx (M := G) ≠ some i
have cons₂ : (List.map (Sigma.fst (β := fun (i : ι) ↦ G i)) (w.toList (M := G))).head? ≠ some i
Tactic: rwa [Word.fstIdx, ← List.head?_map, hw'map, List.head?_map]
-- Lean 4 proof step from Mathlib.GroupTheory.PushoutI (goal)
Goal:
ι : Type u_1
G : ι → Type u_2
H : Type u_3
inst : (i : ι) → Group (G i)
inst_1 : Group H
φ : (i : ι) → MonoidHom.{u_3, u_2} H (G i)
d : Transversal (G := G) φ
i : ι
g : G i
w : Word G
hIdx : w.fstIdx (M := G) ≠ some i
hg1 : g ≠ 1
ih :
  ∀ (hw : Reduced (G := G) φ w),
    ∃ (w' : NormalWord (G := G) d),
      w'.prod (G := G) = (ofCoprodI (G := G) : (a : CoprodI G) → PushoutI φ) (w.prod (M := G)) ∧
        List.map (Sigma.fst (β := fun (i : ι) ↦ G i)) (w'.toWord (G := G).toList (M := G)) =
          List.map (Sigma.fst (β := fun (i : ι) ↦ G i)) (w.toList (M := G))
hw : Reduced (G := G) φ (Word.cons (M := G) g w hIdx hg1)
w' : NormalWord (G := G) d
hw'prod : w'.prod (G := G) = (ofCoprodI (G := G) : (a : CoprodI G) → PushoutI φ) (w.prod (M := G))
hw'map :
  List.map (Sigma.fst (β := fun (i : ι) ↦ G i)) (w'.toWord (G := G).toList (M := G)) =
    List.map (Sigma.fst (β := fun (i : ι) ↦ G i)) (w.toList (M := G))
cons : Option.map (Sigma.fst (β := fun (i : ι) ↦ G i)) w'.toWord (G := G).toList (M := G).head? ≠ some i
cons₁ : (List.map (Sigma.fst (β := fun (i : ι) ↦ G i)) (w'.toWord (G := G).toList (M := G))).head? ≠ some i
cons₂ : (List.map (Sigma.fst (β := fun (i : ι) ↦ G i)) (w.toList (M := G))).head? ≠ some i
⊢ w'.toWord (G := G).fstIdx (M := G) ≠ some i
have cons₃ : Option.map (Sigma.fst (β := fun (i : ι) ↦ G i)) w.toList (M := G).head? ≠ some i
Tactic: rwa [Word.fstIdx, ← List.head?_map, hw'map, List.head?_map]
-- Lean 4 proof step from Mathlib.GroupTheory.PushoutI (goal)
Goal:
ι : Type u_1
G : ι → Type u_2
H : Type u_3
inst : (i : ι) → Group (G i)
inst_1 : Group H
φ : (i : ι) → MonoidHom.{u_3, u_2} H (G i)
d : Transversal (G := G) φ
w : Word G
hw : Reduced (G := G) φ w
⊢ ∃ (w' : NormalWord (G := G) d),
    w'.prod (G := G) = (ofCoprodI (G := G) : (a : CoprodI G) → PushoutI φ) (w.prod (M := G)) ∧
      List.map (Sigma.fst (β := fun (i : ι) ↦ G i)) (w'.toWord (G := G).toList (M := G)) =
        List.map (Sigma.fst (β := fun (i : ι) ↦ G i)) (w.toList (M := G))
have empty : ∀ (hw : Reduced (G := G) φ (Word.empty (M := G))),
  ∃ (w' : NormalWord (G := G) d),
    w'.prod (G := G) = (ofCoprodI (G := G) : (a : CoprodI G) → PushoutI φ) (Word.prod (M := G) (Word.empty (M := G))) ∧
      List.map (Sigma.fst (β := fun (i : ι) ↦ G i)) (w'.toWord (G := G).toList (M := G)) =
        List.map (α := (i : ι) × G i) (Sigma.fst (β := fun (i : ι) ↦ G i)) (Word.toList (M := G) (Word.empty (M := G)))
Tactic: induction w using Word.consRecOn with
  | empty => exact ⟨empty, by simp, rfl⟩
  | cons i g w hIdx hg1 ih =>
    rcases ih (fun _ hg => hw _ (List.mem_cons_of_mem _ hg)) with
      ⟨w', hw'prod, hw'map⟩
    refine ⟨cons g w' ?_ ?_, ?_⟩
    · rwa [Word.fstIdx, ← List.head?_map, hw'map, List.head?_map]
    · exact hw _ List.mem_cons_self
    · simp [hw'prod, hw'map]
Cleared hypotheses: w, hw
-- Lean 4 proof step from Mathlib.GroupTheory.PushoutI (goal)
Goal:
ι : Type u_1
G : ι → Type u_2
H : Type u_3
inst : (i : ι) → Group (G i)
inst_1 : Group H
φ : (i : ι) → MonoidHom.{u_3, u_2} H (G i)
d : Transversal (G := G) φ
w : Word G
hw : Reduced (G := G) φ w
empty :
  ∀ (hw : Reduced (G := G) φ (Word.empty (M := G))),
    ∃ (w' : NormalWord (G := G) d),
      w'.prod (G := G) =
          (ofCoprodI (G := G) : (a : CoprodI G) → PushoutI φ) (Word.prod (M := G) (Word.empty (M := G))) ∧
        List.map (Sigma.fst (β := fun (i : ι) ↦ G i)) (w'.toWord (G := G).toList (M := G)) =
          List.map (α := (i : ι) × G i) (Sigma.fst (β := fun (i : ι) ↦ G i))
            (Word.toList (M := G) (Word.empty (M := G)))
⊢ ∃ (w' : NormalWord (G := G) d),
    w'.prod (G := G) = (ofCoprodI (G := G) : (a : CoprodI G) → PushoutI φ) (w.prod (M := G)) ∧
      List.map (Sigma.fst (β := fun (i : ι) ↦ G i)) (w'.toWord (G := G).toList (M := G)) =
        List.map (Sigma.fst (β := fun (i : ι) ↦ G i)) (w.toList (M := G))
have cons : ∀ (i : ι) (g : G i) (w : Word G) (hIdx : w.fstIdx (M := G) ≠ some i) (hg1 : g ≠ 1)
  (ih :
    ∀ (hw : Reduced (G := G) φ w),
      ∃ (w' : NormalWord (G := G) d),
        w'.prod (G := G) = (ofCoprodI (G := G) : (a : CoprodI G) → PushoutI φ) (w.prod (M := G)) ∧
          List.map (Sigma.fst (β := fun (i : ι) ↦ G i)) (w'.toWord (G := G).toList (M := G)) =
            List.map (Sigma.fst (β := fun (i : ι) ↦ G i)) (w.toList (M := G)))
  (hw : Reduced (G := G) φ (Word.cons (M := G) g w hIdx hg1)),
  ∃ (w' : NormalWord (G := G) d),
    w'.prod (G := G) =
        (ofCoprodI (G := G) : (a : CoprodI G) → PushoutI φ) ((Word.cons (M := G) g w hIdx hg1).prod (M := G)) ∧
      List.map (Sigma.fst (β := fun (i : ι) ↦ G i)) (w'.toWord (G := G).toList (M := G)) =
        List.map (Sigma.fst (β := fun (i : ι) ↦ G i)) ((Word.cons (M := G) g w hIdx hg1).toList (M := G))
Tactic: induction w using Word.consRecOn with
  | empty => exact ⟨empty, by simp, rfl⟩
  | cons i g w hIdx hg1 ih =>
    rcases ih (fun _ hg => hw _ (List.mem_cons_of_mem _ hg)) with
      ⟨w', hw'prod, hw'map⟩
    refine ⟨cons g w' ?_ ?_, ?_⟩
    · rwa [Word.fstIdx, ← List.head?_map, hw'map, List.head?_map]
    · exact hw _ List.mem_cons_self
    · simp [hw'prod, hw'map]
Cleared hypotheses: w, hw
-- Lean 4 proof step from Mathlib.GroupTheory.PushoutI (goal)
Goal:
ι : Type u_1
G : ι → Type u_2
H : Type u_3
inst : (i : ι) → Group (G i)
inst_1 : Group H
φ : (i : ι) → MonoidHom.{u_3, u_2} H (G i)
d : Transversal (G := G) φ
w : Word G
hw : Reduced (G := G) φ w
⊢ ∃ (w' : NormalWord (G := G) d),
    w'.prod (G := G) = (ofCoprodI (G := G) : (a : CoprodI G) → PushoutI φ) (w.prod (M := G)) ∧
      List.map (Sigma.fst (β := fun (i : ι) ↦ G i)) (w'.toWord (G := G).toList (M := G)) =
        List.map (Sigma.fst (β := fun (i : ι) ↦ G i)) (w.toList (M := G))
have empty : ∀ (hw : Reduced (G := G) φ (Word.empty (M := G))),
  ∃ (w' : NormalWord (G := G) d),
    w'.prod (G := G) = (ofCoprodI (G := G) : (a : CoprodI G) → PushoutI φ) (Word.prod (M := G) (Word.empty (M := G))) ∧
      List.map (Sigma.fst (β := fun (i : ι) ↦ G i)) (w'.toWord (G := G).toList (M := G)) =
        List.map (α := (i : ι) × G i) (Sigma.fst (β := fun (i : ι) ↦ G i)) (Word.toList (M := G) (Word.empty (M := G)))
Tactic: classical
  induction w using Word.consRecOn with
  | empty => exact ⟨empty, by simp, rfl⟩
  | cons i g w hIdx hg1 ih =>
    rcases ih (fun _ hg => hw _ (List.mem_cons_of_mem _ hg)) with
      ⟨w', hw'prod, hw'map⟩
    refine ⟨cons g w' ?_ ?_, ?_⟩
    · rwa [Word.fstIdx, ← List.head?_map, hw'map, List.head?_map]
    · exact hw _ List.mem_cons_self
    · simp [hw'prod, hw'map]
Cleared hypotheses: w, hw
-- Lean 4 proof step from Mathlib.GroupTheory.PushoutI (goal)
Goal:
ι : Type u_1
G : ι → Type u_2
H : Type u_3
inst : (i : ι) → Group (G i)
inst_1 : Group H
φ : (i : ι) → MonoidHom.{u_3, u_2} H (G i)
d : Transversal (G := G) φ
w : Word G
hw : Reduced (G := G) φ w
empty :
  ∀ (hw : Reduced (G := G) φ (Word.empty (M := G))),
    ∃ (w' : NormalWord (G := G) d),
      w'.prod (G := G) =
          (ofCoprodI (G := G) : (a : CoprodI G) → PushoutI φ) (Word.prod (M := G) (Word.empty (M := G))) ∧
        List.map (Sigma.fst (β := fun (i : ι) ↦ G i)) (w'.toWord (G := G).toList (M := G)) =
          List.map (α := (i : ι) × G i) (Sigma.fst (β := fun (i : ι) ↦ G i))
            (Word.toList (M := G) (Word.empty (M := G)))
⊢ ∃ (w' : NormalWord (G := G) d),
    w'.prod (G := G) = (ofCoprodI (G := G) : (a : CoprodI G) → PushoutI φ) (w.prod (M := G)) ∧
      List.map (Sigma.fst (β := fun (i : ι) ↦ G i)) (w'.toWord (G := G).toList (M := G)) =
        List.map (Sigma.fst (β := fun (i : ι) ↦ G i)) (w.toList (M := G))
have cons : ∀ (i : ι) (g : G i) (w : Word G) (hIdx : w.fstIdx (M := G) ≠ some i) (hg1 : g ≠ 1)
  (ih :
    ∀ (hw : Reduced (G := G) φ w),
      ∃ (w' : NormalWord (G := G) d),
        w'.prod (G := G) = (ofCoprodI (G := G) : (a : CoprodI G) → PushoutI φ) (w.prod (M := G)) ∧
          List.map (Sigma.fst (β := fun (i : ι) ↦ G i)) (w'.toWord (G := G).toList (M := G)) =
            List.map (Sigma.fst (β := fun (i : ι) ↦ G i)) (w.toList (M := G)))
  (hw : Reduced (G := G) φ (Word.cons (M := G) g w hIdx hg1)),
  ∃ (w' : NormalWord (G := G) d),
    w'.prod (G := G) =
        (ofCoprodI (G := G) : (a : CoprodI G) → PushoutI φ) ((Word.cons (M := G) g w hIdx hg1).prod (M := G)) ∧
      List.map (Sigma.fst (β := fun (i : ι) ↦ G i)) (w'.toWord (G := G).toList (M := G)) =
        List.map (Sigma.fst (β := fun (i : ι) ↦ G i)) ((Word.cons (M := G) g w hIdx hg1).toList (M := G))
Tactic: classical
  induction w using Word.consRecOn with
  | empty => exact ⟨empty, by simp, rfl⟩
  | cons i g w hIdx hg1 ih =>
    rcases ih (fun _ hg => hw _ (List.mem_cons_of_mem _ hg)) with
      ⟨w', hw'prod, hw'map⟩
    refine ⟨cons g w' ?_ ?_, ?_⟩
    · rwa [Word.fstIdx, ← List.head?_map, hw'map, List.head?_map]
    · exact hw _ List.mem_cons_self
    · simp [hw'prod, hw'map]
Cleared hypotheses: w, hw
-- Lean 4 proof step from Mathlib.GroupTheory.PushoutI (goal)
Goal:
ι : Type u_1
G : ι → Type u_2
H : Type u_3
inst : (i : ι) → Group (G i)
inst_1 : Group H
φ : (i : ι) → MonoidHom.{u_3, u_2} H (G i)
hφ : ∀ (i : ι), Injective.{u_3 + 1, u_2 + 1} (α := H) (β := G i) (⇑(φ i) : (a : H) → G i)
w : Word G
hw : Reduced (G := G) φ w
h :
  Membership.mem (α := PushoutI (G := G) φ) (base (G := G) φ).range
    ((ofCoprodI (G := G) : (a : CoprodI G) → PushoutI φ) (w.prod (M := G)) : PushoutI (G := G) φ)
⊢ w = Word.empty (M := G)
have rcases : ∀ (d : Transversal (G := G) φ), w = Word.empty (M := G)
Tactic: rcases transversal_nonempty φ hφ with ⟨d⟩
-- Lean 4 proof step from Mathlib.GroupTheory.PushoutI (goal)
Goal:
ι : Type u_1
G : ι → Type u_2
H : Type u_3
inst : (i : ι) → Group (G i)
inst_1 : Group H
φ : (i : ι) → MonoidHom.{u_3, u_2} H (G i)
hφ : ∀ (i : ι), Injective.{u_3 + 1, u_2 + 1} (α := H) (β := G i) (⇑(φ i) : (a : H) → G i)
w : Word G
hw : Reduced (G := G) φ w
h :
  Membership.mem (α := PushoutI (G := G) φ) (base (G := G) φ).range
    ((ofCoprodI (G := G) : (a : CoprodI G) → PushoutI φ) (w.prod (M := G)) : PushoutI (G := G) φ)
d : Transversal (G := G) φ
⊢ w = Word.empty (M := G)
have rcases : ∀ (w' : NormalWord (G := G) d)
  (hw'prod : w'.prod (G := G) = (ofCoprodI (G := G) : (a : CoprodI G) → PushoutI φ) (w.prod (M := G)))
  (hw'map :
    List.map (Sigma.fst (β := fun (i : ι) ↦ G i)) (w'.toWord (G := G).toList (M := G)) =
      List.map (Sigma.fst (β := fun (i : ι) ↦ G i)) (w.toList (M := G))),
  w = Word.empty (M := G)
Tactic: rcases hw.exists_normalWord_prod_eq d with ⟨w', hw'prod, hw'map⟩
-- Lean 4 proof step from Mathlib.GroupTheory.PushoutI (goal)
Goal:
ι : Type u_1
G : ι → Type u_2
H : Type u_3
inst : (i : ι) → Group (G i)
inst_1 : Group H
φ : (i : ι) → MonoidHom.{u_3, u_2} H (G i)
hφ : ∀ (i : ι), Injective.{u_3 + 1, u_2 + 1} (α := H) (β := G i) (⇑(φ i) : (a : H) → G i)
w : Word G
hw : Reduced (G := G) φ w
h :
  Membership.mem (α := PushoutI (G := G) φ) (base (G := G) φ).range
    ((ofCoprodI (G := G) : (a : CoprodI G) → PushoutI φ) (w.prod (M := G)) : PushoutI (G := G) φ)
d : Transversal (G := G) φ
w' : NormalWord (G := G) d
hw'prod : w'.prod (G := G) = (ofCoprodI (G := G) : (a : CoprodI G) → PushoutI φ) (w.prod (M := G))
hw'map :
  List.map (Sigma.fst (β := fun (i : ι) ↦ G i)) (w'.toWord (G := G).toList (M := G)) =
    List.map (Sigma.fst (β := fun (i : ι) ↦ G i)) (w.toList (M := G))
⊢ w = Word.empty (M := G)
have rcases : ∀ (h : H)
  (heq :
    Eq (α := PushoutI (G := G) φ) ((base (G := G) φ : (a : H) → PushoutI φ) h : PushoutI (G := G) φ)
      ((ofCoprodI (G := G) : (a : CoprodI G) → PushoutI φ) (w.prod (M := G)) : PushoutI (G := G) φ)),
  w = Word.empty (M := G)
Tactic: rcases h with ⟨h, heq⟩
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.GroupTheory.PushoutI (hypothesis)
Goal:
ι : Type u_1
G : ι → Type u_2
H : Type u_3
inst : (i : ι) → Group (G i)
inst_1 : Group H
φ : (i : ι) → MonoidHom.{u_3, u_2} H (G i)
hφ : ∀ (i : ι), Injective.{u_3 + 1, u_2 + 1} (α := H) (β := G i) (⇑(φ i) : (a : H) → G i)
w : Word G
hw : Reduced (G := G) φ w
d : Transversal (G := G) φ
w' : NormalWord (G := G) d
hw'prod : w'.prod (G := G) = (ofCoprodI (G := G) : (a : CoprodI G) → PushoutI φ) (w.prod (M := G))
hw'map :
  List.map (Sigma.fst (β := fun (i : ι) ↦ G i)) (w'.toWord (G := G).toList (M := G)) =
    List.map (Sigma.fst (β := fun (i : ι) ↦ G i)) (w.toList (M := G))
h : H
heq :
  Eq (α := PushoutI (G := G) φ) ((base (G := G) φ : (a : H) → PushoutI φ) h : PushoutI (G := G) φ)
    ((ofCoprodI (G := G) : (a : CoprodI G) → PushoutI φ) (w.prod (M := G)) : PushoutI (G := G) φ)
⊢ w = Word.empty (M := G)
have this : Eq (α := PushoutI (G := G) φ) (NormalWord.prod (G := G) (d := d) (NormalWord.mk (G := G) (Word.empty (M := G)) h sorry))
  ((base (G := G) φ : (a : H) → PushoutI φ) h)
Tactic: have : (NormalWord.prod (d := d) ⟨.empty, h, by simp⟩) = base φ h := by
    simp [NormalWord.prod]