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) φ
inst_2 : DecidableEq ι
inst_3 : (i : ι) → DecidableEq (G i)
i : ι
h₁ : H
w₂ : Word G
h₂ : H
hw₂ : ∀ (i : ι) (g : G i), Sigma.mk (β := fun (i : ι) ↦ G i) i g ∈ w₂.toList (M := G) → g ∈ d.set (G := G) i
hw₁_1 :
  ∀ (i_1 : ι) (g : G i_1),
    Sigma.mk (β := fun (i : ι) ↦ G i) i_1 g ∈
        (HMul.hMul (α := CoprodI G) (β := CoprodI G)
                (((CoprodI.of (M := G) : (a : G i) → CoprodI G) ((φ i : (a : H) → G i) h₁))⁻¹ : CoprodI G)
                ((CoprodI.of (M := G) : (a : G i) → CoprodI G) ((φ i : (a : H) → G i) h₂) : CoprodI G) •
              w₂).toList
          (M := G) →
      g ∈ d.set (G := G) i_1
hw₁ :
  ∀ (i_1 : ι) (g : G i_1),
    Sigma.mk (β := fun (i : ι) ↦ G i) i_1 g ∈
        (HSMul.hSMul (α := CoprodI G)
              ((CoprodI.of (M := G) : (a : G i) → CoprodI G) ((φ i : (a : H) → G i) (h₁⁻¹ * h₂)) : CoprodI G) w₂).toList
          (M := G) →
      g ∈ d.set (G := G) i_1
this : h₁ = h₂
⊢ mk (G := G)
      (HMul.hMul (α := CoprodI G) (β := CoprodI G)
          (((CoprodI.of (M := G) : (a : G i) → CoprodI G) ((φ i : (a : H) → G i) h₁))⁻¹ : CoprodI G)
          ((CoprodI.of (M := G) : (a : G i) → CoprodI G) ((φ i : (a : H) → G i) h₂) : CoprodI G) •
        w₂)
      h₁ hw₁_1 =
    mk (G := G) w₂ h₂ hw₂
have subst : ∀
  (hw₁ :
    ∀ (i_1 : ι) (g : G i_1),
      Sigma.mk (β := fun (i : ι) ↦ G i) i_1 g ∈
          (HMul.hMul (α := CoprodI G) (β := CoprodI G)
                  (((CoprodI.of (M := G) : (a : G i) → CoprodI G) ((φ i : (a : H) → G i) h₁))⁻¹ : CoprodI G)
                  ((CoprodI.of (M := G) : (a : G i) → CoprodI G) ((φ i : (a : H) → G i) h₁) : CoprodI G) •
                w₂).toList
            (M := G) →
        g ∈ d.set (G := G) i_1)
  (hw₁_2 :
    ∀ (i_1 : ι) (g : G i_1),
      Sigma.mk (β := fun (i : ι) ↦ G i) i_1 g ∈
          (HSMul.hSMul (α := CoprodI G)
                ((CoprodI.of (M := G) : (a : G i) → CoprodI G) ((φ i : (a : H) → G i) (h₁⁻¹ * h₁)) : CoprodI G)
                w₂).toList
            (M := G) →
        g ∈ d.set (G := G) i_1),
  mk (G := G)
      (HMul.hMul (α := CoprodI G) (β := CoprodI G)
          (((CoprodI.of (M := G) : (a : G i) → CoprodI G) ((φ i : (a : H) → G i) h₁))⁻¹ : CoprodI G)
          ((CoprodI.of (M := G) : (a : G i) → CoprodI G) ((φ i : (a : H) → G i) h₁) : CoprodI G) •
        w₂)
      h₁ hw₁ =
    mk (G := G) w₂ h₁ hw₂
Tactic: subst this
Cleared hypotheses: h₂, hw₁_1, hw₁, this
-- Lean 4 proof step from Mathlib.GroupTheory.PushoutI (hypothesis)
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)
i_1 : ι
p : Pair (G := G) d i_1
n : (↑(↑(φ i_1).range : Set (G i_1)) : Type u_2) × (↑(d.set (G := G) i_1) : Type u_2) :=
  (⋯.equiv (S := (↑(φ i_1).range : Set (G i_1))) (T := d.set (G := G) i_1) :
      (a : G i_1) → (↑(↑(φ i_1).range : Set (G i_1)) : Type u_2) × (↑(d.set i_1) : Type u_2))
    (p.toPair (G := G).head (M := G))
w : Word G :=
  (Equiv.symm (Word.equivPair (M := G) i_1) : (a : Word.Pair G i_1) → Word G)
    (let __src := p.toPair (G := G);
    Word.Pair.mk (M := G) (↑n.2 : G i_1) (__src.tail (M := G)) ⋯)
i : ι
g : G i
hg :
  Membership.mem (γ := List ((i : ι) × G i))
    (Word.toList (M := G)
      ((Equiv.symm (Word.equivPair (M := G) i_1) : (a : Word.Pair G i_1) → Word G)
        (Word.Pair.mk (M := G) (↑n.2 : G i_1) (p.toPair (G := G).tail (M := G)) ⋯)))
    (Sigma.mk (β := fun (i : ι) ↦ G i) i g)
⊢ g ∈ d.set (G := G) i
have hg₁ : Sigma.mk (β := fun (i : ι) ↦ G i) i g ∈
    (Word.Pair.mk (M := G) (↑n.2 : G i_1) (p.toPair (G := G).tail (M := G)) sorry).tail (M := G).toList (M := G) ∨
  g ≠ 1 ∧
    ∃ (h : i_1 = i),
      g =
        Eq.rec (motive := fun (x : ι) (h : i_1 = x) ↦ G x)
          ((Word.Pair.mk (M := G) (↑n.2 : G i_1) (p.toPair (G := G).tail (M := G)) sorry).head (M := G)) h
Tactic: rw [Word.equivPair_symm, Word.mem_rcons_iff] at hg
Cleared hypotheses: hg
-- 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)
i_1 : ι
p : Pair (G := G) d i_1
n : (↑(↑(φ i_1).range : Set (G i_1)) : Type u_2) × (↑(d.set (G := G) i_1) : Type u_2) :=
  (⋯.equiv (S := (↑(φ i_1).range : Set (G i_1))) (T := d.set (G := G) i_1) :
      (a : G i_1) → (↑(↑(φ i_1).range : Set (G i_1)) : Type u_2) × (↑(d.set i_1) : Type u_2))
    (p.toPair (G := G).head (M := G))
w : Word G :=
  (Equiv.symm (Word.equivPair (M := G) i_1) : (a : Word.Pair G i_1) → Word G)
    (let __src := p.toPair (G := G);
    Word.Pair.mk (M := G) (↑n.2 : G i_1) (__src.tail (M := G)) ⋯)
i : ι
g : G i
hg :
  Sigma.mk (β := fun (i : ι) ↦ G i) i g ∈
      (Word.Pair.mk (M := G) (↑n.2 : G i_1) (p.toPair (G := G).tail (M := G)) ⋯).tail (M := G).toList (M := G) ∨
    g ≠ 1 ∧
      ∃ (h : i_1 = i),
        g =
          Eq.rec (motive := fun (x : ι) (h : i_1 = x) ↦ G x)
            ((Word.Pair.mk (M := G) (↑n.2 : G i_1) (p.toPair (G := G).tail (M := G)) ⋯).head (M := G)) h
⊢ g ∈ d.set (G := G) i
have inl : ∀
  (hg :
    Sigma.mk (β := fun (i : ι) ↦ G i) i g ∈
      (Word.Pair.mk (M := G) (↑n.2 : G i_1) (p.toPair (G := G).tail (M := G)) sorry).tail (M := G).toList (M := G)),
  g ∈ d.set (G := G) i
Tactic: rcases hg with hg | ⟨_, rfl, rfl⟩
Cleared hypotheses: hg
-- 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)
i_1 : ι
p : Pair (G := G) d i_1
n : (↑(↑(φ i_1).range : Set (G i_1)) : Type u_2) × (↑(d.set (G := G) i_1) : Type u_2) :=
  (⋯.equiv (S := (↑(φ i_1).range : Set (G i_1))) (T := d.set (G := G) i_1) :
      (a : G i_1) → (↑(↑(φ i_1).range : Set (G i_1)) : Type u_2) × (↑(d.set i_1) : Type u_2))
    (p.toPair (G := G).head (M := G))
w : Word G :=
  (Equiv.symm (Word.equivPair (M := G) i_1) : (a : Word.Pair G i_1) → Word G)
    (let __src := p.toPair (G := G);
    Word.Pair.mk (M := G) (↑n.2 : G i_1) (__src.tail (M := G)) ⋯)
i : ι
g : G i
hg :
  Sigma.mk (β := fun (i : ι) ↦ G i) i g ∈
      (Word.Pair.mk (M := G) (↑n.2 : G i_1) (p.toPair (G := G).tail (M := G)) ⋯).tail (M := G).toList (M := G) ∨
    g ≠ 1 ∧
      ∃ (h : i_1 = i),
        g =
          Eq.rec (motive := fun (x : ι) (h : i_1 = x) ↦ G x)
            ((Word.Pair.mk (M := G) (↑n.2 : G i_1) (p.toPair (G := G).tail (M := G)) ⋯).head (M := G)) h
inl :
  ∀
    (hg :
      Sigma.mk (β := fun (i : ι) ↦ G i) i g ∈
        (Word.Pair.mk (M := G) (↑n.2 : G i_1) (p.toPair (G := G).tail (M := G)) ⋯).tail (M := G).toList (M := G)),
    g ∈ d.set (G := G) i
⊢ g ∈ d.set (G := G) i
have inr : Ne.{u_2 + 1} (α := G i_1)
    (Eq.rec (motive := fun (x : ι) (h : i_1 = x) ↦ G x)
        ((Word.Pair.mk (M := G) (↑n.2 : G i_1) (p.toPair (G := G).tail (M := G)) sorry).head (M := G)) sorry :
      G i_1)
    (1 : G i_1) →
  Membership.mem (α := G i_1) (d.set (G := G) i_1)
    (Eq.rec (motive := fun (x : ι) (h : i_1 = x) ↦ G x)
        ((Word.Pair.mk (M := G) (↑n.2 : G i_1) (p.toPair (G := G).tail (M := G)) sorry).head (M := G)) sorry :
      G i_1)
Tactic: rcases hg with hg | ⟨_, rfl, rfl⟩
Cleared hypotheses: i, g, hg
-- 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 : ι
head₁ : G i
tail₁ : Word G
fstIdx_ne : tail₁.fstIdx (M := G) ≠ some i
normalized :
  ∀ (i_1 : ι) (g : G i_1),
    Sigma.mk (β := fun (i : ι) ↦ G i) i_1 g ∈
        (Word.Pair.mk (M := G) head₁ tail₁ fstIdx_ne).tail (M := G).toList (M := G) →
      g ∈ d.set (G := G) i_1
head₂ : G i
tail₂ : Word G
fstIdx_ne_1 : tail₂.fstIdx (M := G) ≠ some i
normalized_1 :
  ∀ (i_1 : ι) (g : G i_1),
    Sigma.mk (β := fun (i : ι) ↦ G i) i_1 g ∈
        (Word.Pair.mk (M := G) head₂ tail₂ fstIdx_ne_1).tail (M := G).toList (M := G) →
      g ∈ d.set (G := G) i_1
⊢ rcons (G := G) i (Pair.mk (G := G) (Word.Pair.mk (M := G) head₁ tail₁ fstIdx_ne) normalized) =
      rcons (G := G) i (Pair.mk (G := G) (Word.Pair.mk (M := G) head₂ tail₂ fstIdx_ne_1) normalized_1) →
    Pair.mk (G := G) (Word.Pair.mk (M := G) head₁ tail₁ fstIdx_ne) normalized =
      Pair.mk (G := G) (Word.Pair.mk (M := G) head₂ tail₂ fstIdx_ne_1) normalized_1
have simp : 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))
            head₁).2 :
      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))
            head₂).2 :
      G i) →
  tail₁ = tail₂ →
    Eq.{u_2 + 1} (α := ↥(φ i).range)
        ((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))
            head₁).1
        ((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))
            head₂).1 →
      head₁ = head₂ ∧ tail₁ = tail₂
Tactic: simp only [rcons, NormalWord.mk.injEq, EmbeddingLike.apply_eq_iff_eq,
    Word.Pair.mk.injEq, Pair.mk.injEq, and_imp]
-- 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 : ι
head₁ : G i
tail₁ : Word G
fstIdx_ne : tail₁.fstIdx (M := G) ≠ some i
normalized :
  ∀ (i_1 : ι) (g : G i_1),
    Sigma.mk (β := fun (i : ι) ↦ G i) i_1 g ∈
        (Word.Pair.mk (M := G) head₁ tail₁ fstIdx_ne).tail (M := G).toList (M := G) →
      g ∈ d.set (G := G) i_1
head₂ : G i
h₁ :
  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))
            head₁).2 :
      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))
            head₂).2 :
      G i)
fstIdx_ne_1 : tail₁.fstIdx (M := G) ≠ some i
normalized_1 :
  ∀ (i_1 : ι) (g : G i_1),
    Sigma.mk (β := fun (i : ι) ↦ G i) i_1 g ∈
        (Word.Pair.mk (M := G) head₂ tail₁ fstIdx_ne_1).tail (M := G).toList (M := G) →
      g ∈ d.set (G := G) i_1
h₃ :
  Eq.{u_2 + 1} (α := ↥(φ i).range)
    ((⋯.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))
        head₁).1
    ((⋯.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))
        head₂).1
⊢ head₁ = head₂ ∧ tail₁ = tail₁
have rw : HMul.hMul (α := 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))
              head₂).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))
              head₂).2 :
        G i) =
    HMul.hMul (α := 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))
              head₂).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))
              head₂).2 :
        G i) ∧
  tail₁ = tail₁
Tactic: rw [← equiv_fst_mul_equiv_snd (d.compl i) head₁,
      ← equiv_fst_mul_equiv_snd (d.compl i) head₂,
    h₁, h₃]
-- Lean 4 proof step from Mathlib.GroupTheory.PushoutI (hypothesis)
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)
i : ι
w : NormalWord (G := G) d
p : Word.Pair G i :=
  (Word.equivPair (M := G) i : (a : Word G) → Word.Pair G i)
    (HSMul.hSMul (α := CoprodI G)
      ((CoprodI.of (M := G) : (a : G i) → CoprodI G) ((φ i : (a : H) → G i) (w.head (G := G))) : CoprodI G)
      (w.toWord (G := G)))
j : ι
g : G j
hg :
  Membership.mem (γ := List ((i : ι) × G i))
    (Word.toList (M := G)
        (Word.Pair.tail (M := G) (i := i)
          ((Word.equivPair (M := G) i : (a : Word G) → Word.Pair G i)
            (HSMul.hSMul (α := CoprodI G)
              ((CoprodI.of (M := G) : (a : G i) → CoprodI G) ((φ i : (a : H) → G i) (w.head (G := G))) : CoprodI G)
              (w.toWord (G := G))))) :
      List ((i : ι) × G i))
    (Sigma.mk (β := fun (i : ι) ↦ G i) j g)
⊢ g ∈ d.set (G := G) j
have hg₁ : Membership.mem (γ := List ((i : ι) × G i))
  (Word.toList (M := G)
    (Word.Pair.tail (M := G) (i := i)
      (have __src : Word.Pair G i := (Word.equivPair (M := G) i : (a : Word G) → Word.Pair G i) (w.toWord (G := G));
      Word.Pair.mk (M := G)
        (HMul.hMul (α := G i) (β := G i) ((φ i : (a : H) → G i) (w.head (G := G)) : G i)
          (Word.Pair.head (M := G) ((Word.equivPair (M := G) i : (a : Word G) → Word.Pair G i) (w.toWord (G := G))) :
            G i))
        (__src.tail (M := G)) sorry)))
  (Sigma.mk (β := fun (i : ι) ↦ G i) j g)
Tactic: rw [Word.of_smul_def, ← Word.equivPair_symm, Equiv.apply_symm_apply] at hg
Cleared hypotheses: hg
-- 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)
i : ι
x : NormalWord (G := G) d
⊢ (Equiv.symm (equivPair (G := G) i) : (a : Pair d i) → NormalWord d)
      (Pair.mk (G := G)
        (Word.Pair.mk (M := G)
          (HMul.hMul (α := G i) (β := G i) (1 : G i)
            (Word.Pair.head (M := G)
                (Pair.toPair.{u_1, u_2, u_3} (G := G) (H := H) (φ := φ) (d := d)
                  ((equivPair (G := G) i : (a : NormalWord d) → Pair d i) x)) :
              G i))
          (Word.Pair.tail (M := G) (i := i)
            (Pair.toPair.{u_1, u_2, u_3} (G := G) (H := H) (φ := φ) (d := d)
              ((equivPair (G := G) i : (a : NormalWord d) → Pair d i) x)))
          ⋯)
        ⋯) =
    x
have rw : (Equiv.symm (equivPair (G := G) i) : (a : Pair d i) → NormalWord d)
    (Pair.mk (G := G)
      (Word.Pair.mk (M := G)
        (Word.Pair.head (M := G)
          (Pair.toPair.{u_1, u_2, u_3} (G := G) (H := H) (φ := φ) (d := d)
            ((equivPair (G := G) i : (a : NormalWord d) → Pair d i) x)))
        (Word.Pair.tail (M := G) (i := i)
          (Pair.toPair.{u_1, u_2, u_3} (G := G) (H := H) (φ := φ) (d := d)
            ((equivPair (G := G) i : (a : NormalWord d) → Pair d i) x)))
        sorry)
      sorry) =
  x
Tactic: rw [one_mul]
-- 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)
i : ι
⊢ Eq (α := H →* Function.End (NormalWord (G := G) d))
    (MonoidHom.comp ((fun (x : ι) ↦ (MulAction.toEndHom : G x →* Function.End (NormalWord (G := G) d))) i) (φ i))
    MulAction.toEndHom
have simp : ∀ (x : H),
  Eq (α := Function.End (NormalWord (G := G) d))
    (fun (x2 : NormalWord (G := G) d) ↦ HSMul.hSMul (α := G i) ((φ i : (a : H) → G i) x : G i) x2)
    fun (x2 : NormalWord (G := G) d) ↦ x • x2
Tactic: simp only [MulAction.toEndHom, DFunLike.ext_iff, MonoidHom.coe_comp, MonoidHom.coe_mk,
      OneHom.coe_mk, comp_apply]
-- 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)
i : ι
h : H
⊢ Eq (α := Function.End (NormalWord (G := G) d))
    (fun (x2 : NormalWord (G := G) d) ↦ HSMul.hSMul (α := G i) ((φ i : (a : H) → G i) h : G i) x2)
    fun (x2 : NormalWord (G := G) d) ↦ h • x2
have h₁ : ∀ (w : NormalWord (G := G) d), HSMul.hSMul (α := G i) ((φ i : (a : H) → G i) h : G i) w = h • w
Tactic: funext w
-- 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)
i : ι
h : H
w : NormalWord (G := G) d
⊢ HSMul.hSMul (α := G i) ((φ i : (a : H) → G i) h : G i) w = h • w
have h₁ : HSMul.hSMul (α := CoprodI G)
    ((CoprodI.of (M := G) : (a : G i) → CoprodI G)
        ((φ i : (a : H) → G i) ((HSMul.hSMul (α := G i) ((φ i : (a : H) → G i) h : G i) w).head (G := G))) :
      CoprodI G)
    ((HSMul.hSMul (α := G i) ((φ i : (a : H) → G i) h : G i) w).toWord (G := G)) =
  HSMul.hSMul (α := CoprodI G)
    ((CoprodI.of (M := G) : (a : G i) → CoprodI G) ((φ i : (a : H) → G i) ((h • w).head (G := G))) : CoprodI G)
    ((h • w).toWord (G := G))
Tactic: apply NormalWord.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 = g • w
have rw : (Equiv.symm (equivPair (G := G) i) : (a : Pair d i) → NormalWord d)
    (let __src : Pair (G := G) d i := (equivPair (G := G) i : (a : NormalWord d) → Pair d i) w;
    Pair.mk (G := G)
      (Word.Pair.mk (M := G)
        (HMul.hMul (β := G i) g
          (Word.Pair.head (M := G)
              (Pair.toPair.{u_1, u_2, u_3} (G := G) (H := H) (φ := φ) (d := d)
                ((equivPair (G := G) i : (a : NormalWord d) → Pair d i) w)) :
            G i))
        (__src.toPair (G := G).tail (M := G)) sorry)
      sorry) =
  g • w
Tactic: rw [summand_smul_def, summand_smul_def']
-- 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
rw :
  (Equiv.symm (equivPair (G := G) i) : (a : Pair d i) → NormalWord d)
      (let __src : Pair (G := G) d i := (equivPair (G := G) i : (a : NormalWord d) → Pair d i) w;
      Pair.mk (G := G)
        (Word.Pair.mk (M := G)
          (HMul.hMul (β := G i) g
            (Word.Pair.head (M := G)
                (Pair.toPair.{u_1, u_2, u_3} (G := G) (H := H) (φ := φ) (d := d)
                  ((equivPair (G := G) i : (a : NormalWord d) → Pair d i) w)) :
              G i))
          (__src.toPair (G := G).tail (M := G)) ⋯)
        ⋯) =
    g • w
⊢ HSMul.hSMul (α := PushoutI (G := G) φ) ((of (G := G) i : (a : G i) → PushoutI φ) g : PushoutI (G := G) φ) w = g • w
have rw₁ : Eq (α := NormalWord (G := G) d)
  ((Equiv.symm (equivPair (G := G) i) : (a : Pair d i) → NormalWord d)
    (let __src : Pair (G := G) d i := (equivPair (G := G) i : (a : NormalWord d) → Pair d i) w;
    Pair.mk (G := G)
      (Word.Pair.mk (M := G)
        (HMul.hMul (β := G i) g
          (Word.Pair.head (M := G)
              (Pair.toPair.{u_1, u_2, u_3} (G := G) (H := H) (φ := φ) (d := d)
                ((equivPair (G := G) i : (a : NormalWord d) → Pair d i) w)) :
            G i))
        (__src.toPair (G := G).tail (M := G)) sorry)
      sorry))
  ((Equiv.symm (equivPair (G := G) i) : (a : Pair d i) → NormalWord d)
    (let __src : Pair (G := G) d i := (equivPair (G := G) i : (a : NormalWord d) → Pair d i) w;
    Pair.mk (G := G)
      (Word.Pair.mk (M := G)
        (HMul.hMul (β := G i) g
          (Word.Pair.head (M := G)
              (Pair.toPair.{u_1, u_2, u_3} (G := G) (H := H) (φ := φ) (d := d)
                ((equivPair (G := G) i : (a : NormalWord d) → Pair d i) w)) :
            G i))
        (__src.toPair (G := G).tail (M := G)) sorry)
      sorry))
Tactic: rw [summand_smul_def, summand_smul_def']
-- 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 = h • w
have rw : mk (G := G) (w.toWord (G := G)) (h * w.head (G := G)) sorry = h • w
Tactic: rw [base_smul_def, base_smul_def']
-- 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
rw : mk (G := G) (w.toWord (G := G)) (h * w.head (G := G)) ⋯ = h • w
⊢ HSMul.hSMul (α := PushoutI (G := G) φ) ((base (G := G) φ : (a : H) → PushoutI φ) h : PushoutI (G := G) φ) w = h • w
have rw₁ : mk (G := G) (w.toWord (G := G)) (h * w.head (G := G)) sorry = mk (G := G) (w.toWord (G := G)) (h * w.head (G := G)) sorry
Tactic: rw [base_smul_def, base_smul_def']
-- 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
w : NormalWord (G := G) d
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)
⊢ motive w
have rcases : (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)
Tactic: rcases w with ⟨w, head, h3⟩
Cleared hypotheses: w