awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.PushoutI
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))
⊢ g ∉ (φ i).range

Tactic:
hw _ List.mem_cons_self

Premises used: Set.Mem, List.mem_cons_self
-- Module: Mathlib.GroupTheory.PushoutI
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))
⊢ g ∉ (φ i).range

Tactic:
exact hw _ List.mem_cons_self

Premises used: List.mem_cons_self
-- Module: Mathlib.GroupTheory.PushoutI
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))
⊢ (NormalWord.cons (G := G) g 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))
        ((NormalWord.cons (G := G) g 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:
simp [hw'prod, hw'map]
-- Module: Mathlib.GroupTheory.PushoutI
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)))
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))
⊢ ∃ (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))

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]

Premises used: List.head?_map, Monoid.CoprodI.Word.fstIdx, Monoid.PushoutI.NormalWord.empty, List.cons
-- Module: Mathlib.GroupTheory.PushoutI
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)))
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))
⊢ ∃ (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))

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]

Premises used: List.head?_map, Monoid.CoprodI.Word.fstIdx, Monoid.PushoutI.NormalWord.empty, List.cons
-- Module: Mathlib.GroupTheory.PushoutI
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) φ)
rcases : ∀ (d : Transversal (G := G) φ), w = Word.empty (M := G)
⊢ w = Word.empty (M := G)

Tactic:
rcases transversal_nonempty φ hφ with ⟨d⟩

Premises used: Monoid.PushoutI.NormalWord.transversal_nonempty
-- Module: Mathlib.GroupTheory.PushoutI
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) φ
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)
⊢ w = Word.empty (M := G)

Tactic:
rcases hw.exists_normalWord_prod_eq d with ⟨w', hw'prod, hw'map⟩

Premises used: Monoid.PushoutI.Reduced.exists_normalWord_prod_eq
-- Module: Mathlib.GroupTheory.PushoutI
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))
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)
⊢ w = Word.empty (M := G)

Tactic:
rcases h with ⟨h, heq⟩
-- Module: Mathlib.GroupTheory.PushoutI
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) φ)
⊢ ∀ (i : ι) (g : G i),
    Membership.mem (γ := List ((i : ι) × G i)) (Word.toList (M := G) (Word.empty (M := G)))
        (Sigma.mk (β := fun (i : ι) ↦ G i) i g) →
      g ∈ d.set (G := G) i

Tactic:
simp
-- Module: Mathlib.GroupTheory.PushoutI
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) φ)
⊢ Eq (α := PushoutI (G := G) φ) (NormalWord.prod (G := G) (d := d) (NormalWord.mk (G := G) (Word.empty (M := G)) h ⋯))
    ((base (G := G) φ : (a : H) → PushoutI φ) h)

Tactic:
simp [NormalWord.prod]

Premises used: Monoid.PushoutI.NormalWord.prod
-- Module: Mathlib.GroupTheory.PushoutI
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) φ)
⊢ Eq (α := PushoutI (G := G) φ) (NormalWord.prod (G := G) (d := d) (NormalWord.mk (G := G) (Word.empty (M := G)) h ⋯))
    ((base (G := G) φ : (a : H) → PushoutI φ) h)

Tactic:
have : (NormalWord.prod (d := d) ⟨.empty, h, by simp⟩) = base φ h := by
    simp [NormalWord.prod]
-- Module: Mathlib.GroupTheory.PushoutI
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) φ)
this :
  Eq (α := PushoutI (G := G) φ) (NormalWord.prod (G := G) (d := d) (NormalWord.mk (G := G) (Word.empty (M := G)) h ⋯))
    ((base (G := G) φ : (a : H) → PushoutI φ) h)
⊢ NormalWord.prod (G := G) (d := d) (NormalWord.mk (G := G) (Word.empty (M := G)) h ⋯) = w'.prod (G := G)

Tactic:
rw [← hw'prod, ← this] at heq
-- Module: Mathlib.GroupTheory.PushoutI
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) φ)
this :
  Eq (α := PushoutI (G := G) φ) (NormalWord.prod (G := G) (d := d) (NormalWord.mk (G := G) (Word.empty (M := G)) h ⋯))
    ((base (G := G) φ : (a : H) → PushoutI φ) h)
heq₁ : NormalWord.prod (G := G) (d := d) (NormalWord.mk (G := G) (Word.empty (M := G)) h ⋯) = w'.prod (G := G)
⊢ Eq (α := PushoutI (G := G) φ) (NormalWord.prod (G := G) (d := d) (NormalWord.mk (G := G) (Word.empty (M := G)) h ⋯))
    ((base (G := G) φ : (a : H) → PushoutI φ) h)

Tactic:
rw [← hw'prod, ← this] at heq
-- Module: Mathlib.GroupTheory.PushoutI
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 : NormalWord.prod (G := G) (d := d) (NormalWord.mk (G := G) (Word.empty (M := G)) h ⋯) = w'.prod (G := G)
this_1 :
  Eq (α := PushoutI (G := G) φ) (NormalWord.prod (G := G) (d := d) (NormalWord.mk (G := G) (Word.empty (M := G)) h ⋯))
    ((base (G := G) φ : (a : H) → PushoutI φ) h)
this : w'.toWord (G := G) = Word.empty (M := G)
⊢ w.toList (M := G) = []

Tactic:
simp [this, @eq_comm _ []] at hw'map

Premises used: eq_comm
-- Module: Mathlib.GroupTheory.PushoutI
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))
h : H
heq : NormalWord.prod (G := G) (d := d) (NormalWord.mk (G := G) (Word.empty (M := G)) h ⋯) = w'.prod (G := G)
this_1 :
  Eq (α := PushoutI (G := G) φ) (NormalWord.prod (G := G) (d := d) (NormalWord.mk (G := G) (Word.empty (M := G)) h ⋯))
    ((base (G := G) φ : (a : H) → PushoutI φ) h)
this : w'.toWord (G := G) = Word.empty (M := G)
hw'map : w.toList (M := G) = []
toList :
  ∀ (i : ℕ) (a : (i : ι) × G i),
    getElem? (valid := fun (as : List ((i : ι) × G i)) (i : ℕ) ↦ i < as.length) (w.toList (M := G)) i = some a ↔
      getElem? (valid := fun (as : List ((i : ι) × G i)) (i : ℕ) ↦ i < as.length)
          (Word.toList (M := G) (Word.empty (M := G))) i =
        some a
⊢ w = Word.empty (M := G)

Tactic:
ext
-- Module: Mathlib.GroupTheory.PushoutI
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))
h : H
heq : NormalWord.prod (G := G) (d := d) (NormalWord.mk (G := G) (Word.empty (M := G)) h ⋯) = w'.prod (G := G)
this_1 :
  Eq (α := PushoutI (G := G) φ) (NormalWord.prod (G := G) (d := d) (NormalWord.mk (G := G) (Word.empty (M := G)) h ⋯))
    ((base (G := G) φ : (a : H) → PushoutI φ) h)
this : w'.toWord (G := G) = Word.empty (M := G)
hw'map : w.toList (M := G) = []
i : ℕ
a : (i : ι) × G i
⊢ getElem? (valid := fun (as : List ((i : ι) × G i)) (i : ℕ) ↦ i < as.length) (w.toList (M := G)) i = some a ↔
    getElem? (valid := fun (as : List ((i : ι) × G i)) (i : ℕ) ↦ i < as.length)
        (Word.toList (M := G) (Word.empty (M := G))) i =
      some a

Tactic:
simp [hw'map]
-- Module: Mathlib.GroupTheory.PushoutI
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 : NormalWord.prod (G := G) (d := d) (NormalWord.mk (G := G) (Word.empty (M := G)) h ⋯) = w'.prod (G := G)
this :
  Eq (α := PushoutI (G := G) φ) (NormalWord.prod (G := G) (d := d) (NormalWord.mk (G := G) (Word.empty (M := G)) h ⋯))
    ((base (G := G) φ : (a : H) → PushoutI φ) h)
suffices : w'.toWord (G := G) = Word.empty (M := G)
⊢ w = Word.empty (M := G)

Tactic:
suffices w'.toWord = .empty by
    simp [this, @eq_comm _ []] at hw'map
    ext
    simp [hw'map]
-- Module: Mathlib.GroupTheory.PushoutI
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 : NormalWord.prod (G := G) (d := d) (NormalWord.mk (G := G) (Word.empty (M := G)) h ⋯) = w'.prod (G := G)
this :
  Eq (α := PushoutI (G := G) φ) (NormalWord.prod (G := G) (d := d) (NormalWord.mk (G := G) (Word.empty (M := G)) h ⋯))
    ((base (G := G) φ : (a : H) → PushoutI φ) h)
rw rw₁ :
  Eq (α := Word G) (toWord (G := G) (φ := φ) (d := d) (NormalWord.mk (G := G) (Word.empty (M := G)) h ⋯))
    (Word.empty (M := G))
⊢ w'.toWord (G := G) = Word.empty (M := G)

Tactic:
rw [← prod_injective heq]

Premises used: Monoid.PushoutI.NormalWord.prod_injective
-- Module: Mathlib.GroupTheory.PushoutI
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)
i j : ι
hij : i ≠ j
x : PushoutI (G := G) φ
this :
  ∀ (g₁ : G i) (hg₁ : (of (G := G) i : (a : G i) → PushoutI φ) g₁ = x) (g₂ : G j)
    (hg₂ : (of (G := G) j : (a : G j) → PushoutI φ) g₂ = x), x ∈ (base (G := G) φ).range
⊢ Membership.mem (γ := Subgroup (PushoutI (G := G) φ))
      (MonoidHom.range (of (G := G) i) ⊓ MonoidHom.range (of (G := G) j)) x →
    x ∈ (base (G := G) φ).range

Tactic:
⟨⟨g₁, hg₁⟩, ⟨g₂, hg₂⟩⟩
-- Module: Mathlib.GroupTheory.PushoutI
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)
i j : ι
hij : i ≠ j
x : PushoutI (G := G) φ
g₁ : G i
hg₁ : (of (G := G) i : (a : G i) → PushoutI φ) g₁ = x
g₂ : G j
hg₂ : (of (G := G) j : (a : G j) → PushoutI φ) g₂ = x
by_contra : ∀ (hx : ¬x ∈ (base (G := G) φ).range), False
⊢ x ∈ (base (G := G) φ).range

Tactic:
by_contra hx
-- Module: Mathlib.GroupTheory.PushoutI
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)
i j : ι
hij : i ≠ j
g₁ : G i
g₂ : G j
hg₁ :
  Eq (α := PushoutI (G := G) φ) ((of (G := G) i : (a : G i) → PushoutI φ) g₁ : PushoutI (G := G) φ)
    (1 : PushoutI (G := G) φ)
hg₂ :
  Eq (α := PushoutI (G := G) φ) ((of (G := G) j : (a : G j) → PushoutI φ) g₂ : PushoutI (G := G) φ)
    (1 : PushoutI (G := G) φ)
hx : ¬1 ∈ (base (G := G) φ).range
⊢ False

Tactic:
simp_all only [ne_eq, one_mem, not_true_eq_false]

Premises used: not_true_eq_false, ne_eq, OneMemClass.one_mem