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
K : Type u_4
inst : Monoid K
inst_1 : (i : ι) → Group (G i)
inst_2 : Group H
φ : (i : ι) → MonoidHom.{u_3, u_2} H (G i)
d : Transversal (G := G) φ
inst_3 : DecidableEq ι
inst_4 : (i : ι) → DecidableEq (G i)
motive : NormalWord (G := G) d → Sort u_5
empty : motive (NormalWord.empty (G := G))
cons :
  (i : ι) →
    (g : G i) →
      (w : NormalWord (G := G) d) →
        (hmw : w.toWord (G := G).fstIdx (M := G) ≠ some i) →
          (_hgn : g ∈ d.set (G := G) i) →
            (hgr : g ∉ (φ i).range) →
              (_hw1 : w.head (G := G) = 1) → motive w → motive (NormalWord.cons (G := G) g w hmw hgr)
base :
  (h : H) →
    (w : NormalWord (G := G) d) →
      w.head (G := G) = 1 →
        motive w →
          motive
            (HSMul.hSMul (α := PushoutI (G := G) φ)
              ((PushoutI.base (G := G) φ : (a : H) → PushoutI φ) h : PushoutI (G := G) φ) w)
w : Word G
head : H
h3 : ∀ (i : ι) (g : G i), Sigma.mk (β := fun (i : ι) ↦ G i) i g ∈ w.toList (M := G) → g ∈ d.set (G := G) i
⊢ motive (mk (G := G) w head h3)
have h : head =
  (HSMul.hSMul (α := PushoutI (G := G) φ) ((PushoutI.base (G := G) φ : (a : H) → PushoutI φ) head : PushoutI (G := G) φ)
        (mk (G := G) w 1 h3)).head
    (G := G)
Tactic: convert! base head ⟨w, 1, h3⟩ rfl ?_
-- Lean 4 proof step from Mathlib.GroupTheory.PushoutI (goal)
Goal:
ι : Type u_1
G : ι → Type u_2
H : Type u_3
K : Type u_4
inst : Monoid K
inst_1 : (i : ι) → Group (G i)
inst_2 : Group H
φ : (i : ι) → MonoidHom.{u_3, u_2} H (G i)
d : Transversal (G := G) φ
inst_3 : DecidableEq ι
inst_4 : (i : ι) → DecidableEq (G i)
motive : NormalWord (G := G) d → Sort u_5
empty : motive (NormalWord.empty (G := G))
cons :
  (i : ι) →
    (g : G i) →
      (w : NormalWord (G := G) d) →
        (hmw : w.toWord (G := G).fstIdx (M := G) ≠ some i) →
          (_hgn : g ∈ d.set (G := G) i) →
            (hgr : g ∉ (φ i).range) →
              (_hw1 : w.head (G := G) = 1) → motive w → motive (NormalWord.cons (G := G) g w hmw hgr)
base :
  (h : H) →
    (w : NormalWord (G := G) d) →
      w.head (G := G) = 1 →
        motive w →
          motive
            (HSMul.hSMul (α := PushoutI (G := G) φ)
              ((PushoutI.base (G := G) φ : (a : H) → PushoutI φ) h : PushoutI (G := G) φ) w)
w : Word G
head : H
h3 : ∀ (i : ι) (g : G i), Sigma.mk (β := fun (i : ι) ↦ G i) i g ∈ w.toList (M := G) → g ∈ d.set (G := G) i
h :
  head =
    (HSMul.hSMul (α := PushoutI (G := G) φ)
          ((PushoutI.base (G := G) φ : (a : H) → PushoutI φ) head : PushoutI (G := G) φ) (mk (G := G) w 1 h3)).head
      (G := G)
⊢ motive (mk (G := G) w head h3)
have convert! : motive (mk (G := G) w 1 h3)
Tactic: convert! base head ⟨w, 1, h3⟩ rfl ?_
-- Lean 4 proof step from Mathlib.GroupTheory.PushoutI (goal)
Goal:
ι : Type u_1
G : ι → Type u_2
H : Type u_3
K : Type u_4
inst : Monoid K
inst_1 : (i : ι) → Group (G i)
inst_2 : Group H
φ : (i : ι) → MonoidHom.{u_3, u_2} H (G i)
d : Transversal (G := G) φ
inst_3 : DecidableEq ι
inst_4 : (i : ι) → DecidableEq (G i)
motive : NormalWord (G := G) d → Sort u_5
empty : motive (NormalWord.empty (G := G))
cons :
  (i : ι) →
    (g : G i) →
      (w : NormalWord (G := G) d) →
        (hmw : w.toWord (G := G).fstIdx (M := G) ≠ some i) →
          (_hgn : g ∈ d.set (G := G) i) →
            (hgr : g ∉ (φ i).range) →
              (_hw1 : w.head (G := G) = 1) → motive w → motive (NormalWord.cons (G := G) g w hmw hgr)
base :
  (h : H) →
    (w : NormalWord (G := G) d) →
      w.head (G := G) = 1 →
        motive w →
          motive
            (HSMul.hSMul (α := PushoutI (G := G) φ)
              ((PushoutI.base (G := G) φ : (a : H) → PushoutI φ) h : PushoutI (G := G) φ) w)
head : H
i : ι
g : G i
w : Word G
h1 : w.fstIdx (M := G) ≠ some i
hg1 : g ≠ 1
ih :
  (h3 : ∀ (i : ι) (g : G i), Sigma.mk (β := fun (i : ι) ↦ G i) i g ∈ w.toList (M := G) → g ∈ d.set (G := G) i) →
    motive (mk (G := G) w 1 h3)
h3 :
  ∀ (i_1 : ι) (g_1 : G i_1),
    Sigma.mk (β := fun (i : ι) ↦ G i) i_1 g_1 ∈ (Word.cons (M := G) g w h1 hg1).toList (M := G) →
      g_1 ∈ d.set (G := G) i_1
⊢ motive (mk (G := G) (Word.cons (M := G) g w h1 hg1) 1 h3)
have h : Word.cons (M := G) g w h1 hg1 = toWord (G := G) (d := d) (NormalWord.cons (G := G) g (mk (G := G) w 1 sorry) h1 sorry)
Tactic: convert!
        cons i g ⟨w, 1, fun _ _ h => h3 _ _ (List.mem_cons_of_mem _ h)⟩ h1
          (h3 _ _ List.mem_cons_self) ?_ rfl (ih ?_)
-- Lean 4 proof step from Mathlib.GroupTheory.PushoutI (goal)
Goal:
ι : Type u_1
G : ι → Type u_2
H : Type u_3
K : Type u_4
inst : Monoid K
inst_1 : (i : ι) → Group (G i)
inst_2 : Group H
φ : (i : ι) → MonoidHom.{u_3, u_2} H (G i)
d : Transversal (G := G) φ
inst_3 : DecidableEq ι
inst_4 : (i : ι) → DecidableEq (G i)
motive : NormalWord (G := G) d → Sort u_5
empty : motive (NormalWord.empty (G := G))
cons :
  (i : ι) →
    (g : G i) →
      (w : NormalWord (G := G) d) →
        (hmw : w.toWord (G := G).fstIdx (M := G) ≠ some i) →
          (_hgn : g ∈ d.set (G := G) i) →
            (hgr : g ∉ (φ i).range) →
              (_hw1 : w.head (G := G) = 1) → motive w → motive (NormalWord.cons (G := G) g w hmw hgr)
base :
  (h : H) →
    (w : NormalWord (G := G) d) →
      w.head (G := G) = 1 →
        motive w →
          motive
            (HSMul.hSMul (α := PushoutI (G := G) φ)
              ((PushoutI.base (G := G) φ : (a : H) → PushoutI φ) h : PushoutI (G := G) φ) w)
head : H
i : ι
g : G i
w : Word G
h1 : w.fstIdx (M := G) ≠ some i
hg1 : g ≠ 1
ih :
  (h3 : ∀ (i : ι) (g : G i), Sigma.mk (β := fun (i : ι) ↦ G i) i g ∈ w.toList (M := G) → g ∈ d.set (G := G) i) →
    motive (mk (G := G) w 1 h3)
h3 :
  ∀ (i_1 : ι) (g_1 : G i_1),
    Sigma.mk (β := fun (i : ι) ↦ G i) i_1 g_1 ∈ (Word.cons (M := G) g w h1 hg1).toList (M := G) →
      g_1 ∈ d.set (G := G) i_1
h : Word.cons (M := G) g w h1 hg1 = toWord (G := G) (d := d) (NormalWord.cons (G := G) g (mk (G := G) w 1 ⋯) h1 ⋯)
⊢ motive (mk (G := G) (Word.cons (M := G) g w h1 hg1) 1 h3)
have h₁ : 1 = NormalWord.head (G := G) (d := d) (NormalWord.cons (G := G) g (mk (G := G) w 1 sorry) h1 sorry)
Tactic: convert!
        cons i g ⟨w, 1, fun _ _ h => h3 _ _ (List.mem_cons_of_mem _ h)⟩ h1
          (h3 _ _ List.mem_cons_self) ?_ rfl (ih ?_)
-- Lean 4 proof step from Mathlib.GroupTheory.PushoutI (goal)
Goal:
ι : Type u_1
G : ι → Type u_2
H : Type u_3
K : Type u_4
inst : Monoid K
inst_1 : (i : ι) → Group (G i)
inst_2 : Group H
φ : (i : ι) → MonoidHom.{u_3, u_2} H (G i)
d : Transversal (G := G) φ
inst_3 : DecidableEq ι
inst_4 : (i : ι) → DecidableEq (G i)
motive : NormalWord (G := G) d → Sort u_5
empty : motive (NormalWord.empty (G := G))
cons :
  (i : ι) →
    (g : G i) →
      (w : NormalWord (G := G) d) →
        (hmw : w.toWord (G := G).fstIdx (M := G) ≠ some i) →
          (_hgn : g ∈ d.set (G := G) i) →
            (hgr : g ∉ (φ i).range) →
              (_hw1 : w.head (G := G) = 1) → motive w → motive (NormalWord.cons (G := G) g w hmw hgr)
base :
  (h : H) →
    (w : NormalWord (G := G) d) →
      w.head (G := G) = 1 →
        motive w →
          motive
            (HSMul.hSMul (α := PushoutI (G := G) φ)
              ((PushoutI.base (G := G) φ : (a : H) → PushoutI φ) h : PushoutI (G := G) φ) w)
head : H
i : ι
g : G i
w : Word G
h1 : w.fstIdx (M := G) ≠ some i
hg1 : g ≠ 1
ih :
  (h3 : ∀ (i : ι) (g : G i), Sigma.mk (β := fun (i : ι) ↦ G i) i g ∈ w.toList (M := G) → g ∈ d.set (G := G) i) →
    motive (mk (G := G) w 1 h3)
h3 :
  ∀ (i_1 : ι) (g_1 : G i_1),
    Sigma.mk (β := fun (i : ι) ↦ G i) i_1 g_1 ∈ (Word.cons (M := G) g w h1 hg1).toList (M := G) →
      g_1 ∈ d.set (G := G) i_1
h : Word.cons (M := G) g w h1 hg1 = toWord (G := G) (d := d) (NormalWord.cons (G := G) g (mk (G := G) w 1 ⋯) h1 ⋯)
h₁ : 1 = NormalWord.head (G := G) (d := d) (NormalWord.cons (G := G) g (mk (G := G) w 1 ⋯) h1 ⋯)
⊢ motive (mk (G := G) (Word.cons (M := G) g w h1 hg1) 1 h3)
have cons₁ : g ∉ (φ i).range
Tactic: convert!
        cons i g ⟨w, 1, fun _ _ h => h3 _ _ (List.mem_cons_of_mem _ h)⟩ h1
          (h3 _ _ List.mem_cons_self) ?_ rfl (ih ?_)
-- Lean 4 proof step from Mathlib.GroupTheory.PushoutI (goal)
Goal:
ι : Type u_1
G : ι → Type u_2
H : Type u_3
K : Type u_4
inst : Monoid K
inst_1 : (i : ι) → Group (G i)
inst_2 : Group H
φ : (i : ι) → MonoidHom.{u_3, u_2} H (G i)
d : Transversal (G := G) φ
inst_3 : DecidableEq ι
inst_4 : (i : ι) → DecidableEq (G i)
motive : NormalWord (G := G) d → Sort u_5
empty : motive (NormalWord.empty (G := G))
cons :
  (i : ι) →
    (g : G i) →
      (w : NormalWord (G := G) d) →
        (hmw : w.toWord (G := G).fstIdx (M := G) ≠ some i) →
          (_hgn : g ∈ d.set (G := G) i) →
            (hgr : g ∉ (φ i).range) →
              (_hw1 : w.head (G := G) = 1) → motive w → motive (NormalWord.cons (G := G) g w hmw hgr)
base :
  (h : H) →
    (w : NormalWord (G := G) d) →
      w.head (G := G) = 1 →
        motive w →
          motive
            (HSMul.hSMul (α := PushoutI (G := G) φ)
              ((PushoutI.base (G := G) φ : (a : H) → PushoutI φ) h : PushoutI (G := G) φ) w)
head : H
i : ι
g : G i
w : Word G
h1 : w.fstIdx (M := G) ≠ some i
hg1 : g ≠ 1
ih :
  (h3 : ∀ (i : ι) (g : G i), Sigma.mk (β := fun (i : ι) ↦ G i) i g ∈ w.toList (M := G) → g ∈ d.set (G := G) i) →
    motive (mk (G := G) w 1 h3)
h3 :
  ∀ (i_1 : ι) (g_1 : G i_1),
    Sigma.mk (β := fun (i : ι) ↦ G i) i_1 g_1 ∈ (Word.cons (M := G) g w h1 hg1).toList (M := G) →
      g_1 ∈ d.set (G := G) i_1
⊢ 1 = NormalWord.head (G := G) (d := d) (NormalWord.cons (G := G) g (mk (G := G) w 1 ⋯) h1 ⋯)
have h : Eq.{u_2 + 1} (α := G i) ((φ i : (a : H) → G i) 1)
  ((φ i : (a : H) → G i) (NormalWord.head (G := G) (d := d) (NormalWord.cons (G := G) g (mk (G := G) w 1 sorry) h1 sorry)))
Tactic: apply d.injective i
-- Lean 4 proof step from Mathlib.GroupTheory.PushoutI (goal)
Goal:
ι : Type u_1
G : ι → Type u_2
H : Type u_3
K : Type u_4
inst : Monoid K
inst_1 : (i : ι) → Group (G i)
inst_2 : Group H
φ : (i : ι) → MonoidHom.{u_3, u_2} H (G i)
d : Transversal (G := G) φ
inst_3 : DecidableEq ι
inst_4 : (i : ι) → DecidableEq (G i)
motive : NormalWord (G := G) d → Sort u_5
empty : motive (NormalWord.empty (G := G))
cons :
  (i : ι) →
    (g : G i) →
      (w : NormalWord (G := G) d) →
        (hmw : w.toWord (G := G).fstIdx (M := G) ≠ some i) →
          (_hgn : g ∈ d.set (G := G) i) →
            (hgr : g ∉ (φ i).range) →
              (_hw1 : w.head (G := G) = 1) → motive w → motive (NormalWord.cons (G := G) g w hmw hgr)
base :
  (h : H) →
    (w : NormalWord (G := G) d) →
      w.head (G := G) = 1 →
        motive w →
          motive
            (HSMul.hSMul (α := PushoutI (G := G) φ)
              ((PushoutI.base (G := G) φ : (a : H) → PushoutI φ) h : PushoutI (G := G) φ) w)
head : H
i : ι
g : G i
w : Word G
h1 : w.fstIdx (M := G) ≠ some i
hg1 : g ≠ 1
ih :
  (h3 : ∀ (i : ι) (g : G i), Sigma.mk (β := fun (i : ι) ↦ G i) i g ∈ w.toList (M := G) → g ∈ d.set (G := G) i) →
    motive (mk (G := G) w 1 h3)
h3 :
  ∀ (i_1 : ι) (g_1 : G i_1),
    Sigma.mk (β := fun (i : ι) ↦ G i) i_1 g_1 ∈ (Word.cons (M := G) g w h1 hg1).toList (M := G) →
      g_1 ∈ d.set (G := G) i_1
⊢ g ∉ (φ i).range
have cons₁ : g ∉ (↑(φ i).range : Set (G i))
Tactic: rwa [← SetLike.mem_coe,
          ← coe_equiv_snd_eq_one_iff_mem (d.compl i) (d.one_mem _),
          (equiv_snd_eq_self_iff_mem (d.compl i) (one_mem _)).2
          (h3 _ _ List.mem_cons_self)]
-- Lean 4 proof step from Mathlib.GroupTheory.PushoutI (goal)
Goal:
ι : Type u_1
G : ι → Type u_2
H : Type u_3
K : Type u_4
inst : Monoid K
inst_1 : (i : ι) → Group (G i)
inst_2 : Group H
φ : (i : ι) → MonoidHom.{u_3, u_2} H (G i)
d : Transversal (G := G) φ
inst_3 : DecidableEq ι
inst_4 : (i : ι) → DecidableEq (G i)
motive : NormalWord (G := G) d → Sort u_5
empty : motive (NormalWord.empty (G := G))
cons :
  (i : ι) →
    (g : G i) →
      (w : NormalWord (G := G) d) →
        (hmw : w.toWord (G := G).fstIdx (M := G) ≠ some i) →
          (_hgn : g ∈ d.set (G := G) i) →
            (hgr : g ∉ (φ i).range) →
              (_hw1 : w.head (G := G) = 1) → motive w → motive (NormalWord.cons (G := G) g w hmw hgr)
base :
  (h : H) →
    (w : NormalWord (G := G) d) →
      w.head (G := G) = 1 →
        motive w →
          motive
            (HSMul.hSMul (α := PushoutI (G := G) φ)
              ((PushoutI.base (G := G) φ : (a : H) → PushoutI φ) h : PushoutI (G := G) φ) w)
head : H
i : ι
g : G i
w : Word G
h1 : w.fstIdx (M := G) ≠ some i
hg1 : g ≠ 1
ih :
  (h3 : ∀ (i : ι) (g : G i), Sigma.mk (β := fun (i : ι) ↦ G i) i g ∈ w.toList (M := G) → g ∈ d.set (G := G) i) →
    motive (mk (G := G) w 1 h3)
h3 :
  ∀ (i_1 : ι) (g_1 : G i_1),
    Sigma.mk (β := fun (i : ι) ↦ G i) i_1 g_1 ∈ (Word.cons (M := G) g w h1 hg1).toList (M := G) →
      g_1 ∈ d.set (G := G) i_1
cons₁ : g ∉ (↑(φ i).range : Set (G i))
⊢ g ∉ (φ i).range
have cons₂ : ¬Eq.{u_2 + 1} (α := G i)
    (↑((sorry.equiv (S := (↑(φ i).range : Set (G i))) (T := d.set (G := G) i) :
              (a : G i) → (↑(↑(φ i).range : Set (G i)) : Type u_2) × (↑(d.set i) : Type u_2))
            g).2 :
      G i)
    1
Tactic: rwa [← SetLike.mem_coe,
          ← coe_equiv_snd_eq_one_iff_mem (d.compl i) (d.one_mem _),
          (equiv_snd_eq_self_iff_mem (d.compl i) (one_mem _)).2
          (h3 _ _ List.mem_cons_self)]
-- Lean 4 proof step from Mathlib.GroupTheory.PushoutI (goal)
Goal:
ι : Type u_1
G : ι → Type u_2
H : Type u_3
K : Type u_4
inst : Monoid K
inst_1 : (i : ι) → Group (G i)
inst_2 : Group H
φ : (i : ι) → MonoidHom.{u_3, u_2} H (G i)
d : Transversal (G := G) φ
inst_3 : DecidableEq ι
inst_4 : (i : ι) → DecidableEq (G i)
motive : NormalWord (G := G) d → Sort u_5
empty : motive (NormalWord.empty (G := G))
cons :
  (i : ι) →
    (g : G i) →
      (w : NormalWord (G := G) d) →
        (hmw : w.toWord (G := G).fstIdx (M := G) ≠ some i) →
          (_hgn : g ∈ d.set (G := G) i) →
            (hgr : g ∉ (φ i).range) →
              (_hw1 : w.head (G := G) = 1) → motive w → motive (NormalWord.cons (G := G) g w hmw hgr)
base :
  (h : H) →
    (w : NormalWord (G := G) d) →
      w.head (G := G) = 1 →
        motive w →
          motive
            (HSMul.hSMul (α := PushoutI (G := G) φ)
              ((PushoutI.base (G := G) φ : (a : H) → PushoutI φ) h : PushoutI (G := G) φ) w)
head : H
i : ι
g : G i
w : Word G
h1 : w.fstIdx (M := G) ≠ some i
hg1 : g ≠ 1
ih :
  (h3 : ∀ (i : ι) (g : G i), Sigma.mk (β := fun (i : ι) ↦ G i) i g ∈ w.toList (M := G) → g ∈ d.set (G := G) i) →
    motive (mk (G := G) w 1 h3)
h3 :
  ∀ (i_1 : ι) (g_1 : G i_1),
    Sigma.mk (β := fun (i : ι) ↦ G i) i_1 g_1 ∈ (Word.cons (M := G) g w h1 hg1).toList (M := G) →
      g_1 ∈ d.set (G := G) i_1
cons₁ : g ∉ (↑(φ i).range : Set (G i))
cons₂ :
  ¬Eq.{u_2 + 1} (α := G i)
      (↑((⋯.equiv (S := (↑(φ i).range : Set (G i))) (T := d.set (G := G) i) :
                (a : G i) → (↑(↑(φ i).range : Set (G i)) : Type u_2) × (↑(d.set i) : Type u_2))
              g).2 :
        G i)
      1
⊢ g ∉ (φ i).range
have cons₃ : ¬g = 1
Tactic: rwa [← SetLike.mem_coe,
          ← coe_equiv_snd_eq_one_iff_mem (d.compl i) (d.one_mem _),
          (equiv_snd_eq_self_iff_mem (d.compl i) (one_mem _)).2
          (h3 _ _ List.mem_cons_self)]
-- Lean 4 proof step from Mathlib.GroupTheory.PushoutI (goal)
Goal:
ι : Type u_1
G : ι → Type u_2
H : Type u_3
K : Type u_4
inst : Monoid K
inst_1 : (i : ι) → Group (G i)
inst_2 : Group H
φ : (i : ι) → MonoidHom.{u_3, u_2} H (G i)
d : Transversal (G := G) φ
inst_3 : DecidableEq ι
inst_4 : (i : ι) → DecidableEq (G i)
motive : NormalWord (G := G) d → Sort u_5
empty : motive (NormalWord.empty (G := G))
cons :
  (i : ι) →
    (g : G i) →
      (w : NormalWord (G := G) d) →
        (hmw : w.toWord (G := G).fstIdx (M := G) ≠ some i) →
          (_hgn : g ∈ d.set (G := G) i) →
            (hgr : g ∉ (φ i).range) →
              (_hw1 : w.head (G := G) = 1) → motive w → motive (NormalWord.cons (G := G) g w hmw hgr)
base :
  (h : H) →
    (w : NormalWord (G := G) d) →
      w.head (G := G) = 1 →
        motive w →
          motive
            (HSMul.hSMul (α := PushoutI (G := G) φ)
              ((PushoutI.base (G := G) φ : (a : H) → PushoutI φ) h : PushoutI (G := G) φ) w)
w : Word G
head : H
h3 : ∀ (i : ι) (g : G i), Sigma.mk (β := fun (i : ι) ↦ G i) i g ∈ w.toList (M := G) → g ∈ d.set (G := G) i
⊢ motive (mk (G := G) w 1 h3)
have empty₁ : (h3 :
    ∀ (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) →
  motive (mk (G := G) (Word.empty (M := G)) 1 h3)
Tactic: induction w using Word.consRecOn with
    | empty => exact empty
    | cons i g w h1 hg1 ih =>
      convert!
        cons i g ⟨w, 1, fun _ _ h => h3 _ _ (List.mem_cons_of_mem _ h)⟩ h1
          (h3 _ _ List.mem_cons_self) ?_ rfl (ih ?_)
      · simp only [Word.cons, NormalWord.cons, map_one, mul_one,
          (equiv_snd_eq_self_iff_mem (d.compl i) (one_mem _)).2
          (h3 _ _ List.mem_cons_self)]
      · apply d.injective i
        simp only [NormalWord.cons, equiv_fst_eq_mul_inv, MonoidHom.apply_ofInjective_symm,
          map_one, mul_one, mul_inv_cancel, (equiv_snd_eq_self_iff_mem (d.compl i) (one_mem _)).2
          (h3 _ _ List.mem_cons_self)]
      · rwa [← SetLike.mem_coe,
          ← coe_equiv_snd_eq_one_iff_mem (d.compl i) (d.one_mem _),
          (equiv_snd_eq_self_iff_mem (d.compl i) (one_mem _)).2
          (h3 _ _ List.mem_cons_self)]
Cleared hypotheses: w, h3
-- Lean 4 proof step from Mathlib.GroupTheory.PushoutI (goal)
Goal:
ι : Type u_1
G : ι → Type u_2
H : Type u_3
K : Type u_4
inst : Monoid K
inst_1 : (i : ι) → Group (G i)
inst_2 : Group H
φ : (i : ι) → MonoidHom.{u_3, u_2} H (G i)
d : Transversal (G := G) φ
inst_3 : DecidableEq ι
inst_4 : (i : ι) → DecidableEq (G i)
motive : NormalWord (G := G) d → Sort u_5
empty : motive (NormalWord.empty (G := G))
cons :
  (i : ι) →
    (g : G i) →
      (w : NormalWord (G := G) d) →
        (hmw : w.toWord (G := G).fstIdx (M := G) ≠ some i) →
          (_hgn : g ∈ d.set (G := G) i) →
            (hgr : g ∉ (φ i).range) →
              (_hw1 : w.head (G := G) = 1) → motive w → motive (NormalWord.cons (G := G) g w hmw hgr)
base :
  (h : H) →
    (w : NormalWord (G := G) d) →
      w.head (G := G) = 1 →
        motive w →
          motive
            (HSMul.hSMul (α := PushoutI (G := G) φ)
              ((PushoutI.base (G := G) φ : (a : H) → PushoutI φ) h : PushoutI (G := G) φ) w)
w : Word G
head : H
h3 : ∀ (i : ι) (g : G i), Sigma.mk (β := fun (i : ι) ↦ G i) i g ∈ w.toList (M := G) → g ∈ d.set (G := G) i
empty₁ :
  (h3 :
      ∀ (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) →
    motive (mk (G := G) (Word.empty (M := G)) 1 h3)
⊢ motive (mk (G := G) w 1 h3)
have cons₁ : (i : ι) →
  (g : G i) →
    (w : Word G) →
      (h1 : w.fstIdx (M := G) ≠ some i) →
        (hg1 : g ≠ 1) →
          (ih :
              (h3 :
                  ∀ (i : ι) (g : G i),
                    Sigma.mk (β := fun (i : ι) ↦ G i) i g ∈ w.toList (M := G) → g ∈ d.set (G := G) i) →
                motive (mk (G := G) w 1 h3)) →
            (h3 :
                ∀ (i_1 : ι) (g_1 : G i_1),
                  Sigma.mk (β := fun (i : ι) ↦ G i) i_1 g_1 ∈ (Word.cons (M := G) g w h1 hg1).toList (M := G) →
                    g_1 ∈ d.set (G := G) i_1) →
              motive (mk (G := G) (Word.cons (M := G) g w h1 hg1) 1 h3)
Tactic: induction w using Word.consRecOn with
    | empty => exact empty
    | cons i g w h1 hg1 ih =>
      convert!
        cons i g ⟨w, 1, fun _ _ h => h3 _ _ (List.mem_cons_of_mem _ h)⟩ h1
          (h3 _ _ List.mem_cons_self) ?_ rfl (ih ?_)
      · simp only [Word.cons, NormalWord.cons, map_one, mul_one,
          (equiv_snd_eq_self_iff_mem (d.compl i) (one_mem _)).2
          (h3 _ _ List.mem_cons_self)]
      · apply d.injective i
        simp only [NormalWord.cons, equiv_fst_eq_mul_inv, MonoidHom.apply_ofInjective_symm,
          map_one, mul_one, mul_inv_cancel, (equiv_snd_eq_self_iff_mem (d.compl i) (one_mem _)).2
          (h3 _ _ List.mem_cons_self)]
      · rwa [← SetLike.mem_coe,
          ← coe_equiv_snd_eq_one_iff_mem (d.compl i) (d.one_mem _),
          (equiv_snd_eq_self_iff_mem (d.compl i) (one_mem _)).2
          (h3 _ _ List.mem_cons_self)]
Cleared hypotheses: w, h3
-- 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) φ
inst_2 : DecidableEq ι
inst_3 : (i : ι) → DecidableEq (G i)
i : ι
g : G i
w : NormalWord (G := G) d
hmw : w.toWord (G := G).fstIdx (M := G) ≠ some i
hgr : g ∉ (φ i).range
⊢ cons (G := G) g w hmw hgr =
    HSMul.hSMul (α := PushoutI (G := G) φ) ((of (G := G) i : (a : G i) → PushoutI φ) g : PushoutI (G := G) φ) w
have apply : HSMul.hSMul (α := CoprodI G)
    ((CoprodI.of (M := G) : (a : G i) → CoprodI G) ((φ i : (a : H) → G i) ((cons (G := G) g w hmw hgr).head (G := G))) :
      CoprodI G)
    ((cons (G := G) g w hmw hgr).toWord (G := G)) =
  HSMul.hSMul (α := CoprodI G)
    ((CoprodI.of (M := G) : (a : G i) → CoprodI G)
        ((φ i : (a : H) → G i)
          ((HSMul.hSMul (α := PushoutI (G := G) φ) ((of (G := G) i : (a : G i) → PushoutI φ) g : PushoutI (G := G) φ)
                w).head
            (G := G))) :
      CoprodI G)
    ((HSMul.hSMul (α := PushoutI (G := G) φ) ((of (G := G) i : (a : G i) → PushoutI φ) g : PushoutI (G := G) φ)
          w).toWord
      (G := G))
Tactic: apply ext_smul i
-- 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) φ
inst_2 : DecidableEq ι
inst_3 : (i : ι) → DecidableEq (G i)
i : ι
g : G i
w : NormalWord (G := G) d
⊢ (HSMul.hSMul (α := PushoutI (G := G) φ) ((of (G := G) i : (a : G i) → PushoutI φ) g : PushoutI (G := G) φ) w).prod
      (G := G) =
    HMul.hMul (α := PushoutI (G := G) φ) ((of (G := G) i : (a : G i) → PushoutI φ) g : PushoutI (G := G) φ)
      (w.prod (G := G))
have of : (g • w).prod (G := G) =
  HMul.hMul (α := PushoutI (G := G) φ) ((of (G := G) i : (a : G i) → PushoutI φ) g : PushoutI (G := G) φ)
    (w.prod (G := G))
Tactic: rw [of_smul_eq_smul, prod_summand_smul]
-- 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) φ
inst_2 : DecidableEq ι
inst_3 : (i : ι) → DecidableEq (G i)
i : ι
g : G i
w : NormalWord (G := G) d
of :
  (g • w).prod (G := G) =
    HMul.hMul (α := PushoutI (G := G) φ) ((PushoutI.of (G := G) i : (a : G i) → PushoutI φ) g : PushoutI (G := G) φ)
      (w.prod (G := G))
⊢ (HSMul.hSMul (α := PushoutI (G := G) φ) ((PushoutI.of (G := G) i : (a : G i) → PushoutI φ) g : PushoutI (G := G) φ)
          w).prod
      (G := G) =
    HMul.hMul (α := PushoutI (G := G) φ) ((PushoutI.of (G := G) i : (a : G i) → PushoutI φ) g : PushoutI (G := G) φ)
      (w.prod (G := G))
have of₁ : HMul.hMul (α := PushoutI (G := G) φ) ((PushoutI.of (G := G) i : (a : G i) → PushoutI φ) g : PushoutI (G := G) φ)
    (w.prod (G := G)) =
  HMul.hMul (α := PushoutI (G := G) φ) ((PushoutI.of (G := G) i : (a : G i) → PushoutI φ) g : PushoutI (G := G) φ)
    (w.prod (G := G))
Tactic: rw [of_smul_eq_smul, prod_summand_smul]
-- 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) φ
inst_2 : DecidableEq ι
inst_3 : (i : ι) → DecidableEq (G i)
h : H
w : NormalWord (G := G) d
⊢ (HSMul.hSMul (α := PushoutI (G := G) φ) ((base (G := G) φ : (a : H) → PushoutI φ) h : PushoutI (G := G) φ) w).prod
      (G := G) =
    HMul.hMul (α := PushoutI (G := G) φ) ((base (G := G) φ : (a : H) → PushoutI φ) h : PushoutI (G := G) φ)
      (w.prod (G := G))
have base : (h • w).prod (G := G) =
  HMul.hMul (α := PushoutI (G := G) φ) ((base (G := G) φ : (a : H) → PushoutI φ) h : PushoutI (G := G) φ)
    (w.prod (G := G))
Tactic: rw [base_smul_eq_smul, prod_base_smul]