awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.PushoutI
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 : ι
toFun : NormalWord (G := G) d → Pair (G := G) d i :=
  fun (w : NormalWord (G := G) d) ↦
    Pair.mk (G := G)
      ((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))))
      ⋯
w : NormalWord (G := G) d
⊢ HSMul.hSMul (α := CoprodI G)
      ((CoprodI.of (M := G) : (a : G i) → CoprodI G)
          ((φ i : (a : H) → G i) ((rcons (G := G) i (toFun w)).head (G := G))) :
        CoprodI G)
      ((rcons (G := G) i (toFun w)).toWord (G := G)) =
    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))

Tactic:
simp only [toFun, rcons, Word.equivPair_symm,
        Word.equivPair_smul_same, Word.equivPair_tail_eq_inv_smul, Word.rcons_eq_smul,
        MonoidHom.apply_ofInjective_symm, equiv_fst_eq_mul_inv, mul_assoc, map_mul, map_inv,
        mul_smul, inv_smul_smul, smul_inv_smul]

Premises used: map_inv, mul_assoc, inv_smul_smul, smul_inv_smul, Monoid.CoprodI.Word.equivPair_symm, map_mul, Monoid.CoprodI.Word.equivPair_smul_same, Monoid.CoprodI.Word.rcons_eq_smul, Subgroup.IsComplement.equiv_fst_eq_mul_inv, MonoidHom.apply_ofInjective_symm, SemigroupAction.mul_smul, Monoid.CoprodI.Word.equivPair_tail_eq_inv_smul, Monoid.PushoutI.NormalWord.rcons
-- Module: Mathlib.GroupTheory.PushoutI
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
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)))
          ⋯)
        ⋯) =
    x
⊢ (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

Tactic:
rw [one_mul]

Premises used: one_mul
-- Module: Mathlib.GroupTheory.PushoutI
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)
          (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)))
          ⋯)
        ⋯) =
    x

Tactic:
(equivPair i).symm_apply_apply _

Premises used: Equiv.symm_apply_apply, Monoid.PushoutI.NormalWord.equivPair
-- Module: Mathlib.GroupTheory.PushoutI
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)
          (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)))
          ⋯)
        ⋯) =
    x

Tactic:
exact (equivPair i).symm_apply_apply _

Premises used: Equiv.symm_apply_apply, Monoid.PushoutI.NormalWord.equivPair
-- 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) φ
inst_2 : DecidableEq ι
inst_3 : (i : ι) → DecidableEq (G i)
i : ι
g : G i
w : NormalWord (G := G) d
⊢ g • w =
    (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)) ⋯)
        ⋯)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.GroupTheory.PushoutI
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 : ι
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
⊢ 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

Tactic:
simp only [MulAction.toEndHom, DFunLike.ext_iff, MonoidHom.coe_comp, MonoidHom.coe_mk,
      OneHom.coe_mk, comp_apply]

Premises used: MonoidHom.coe_comp, OneHom.coe_mk, DFunLike.ext_iff, MulAction.toEndHom, MonoidHom.coe_mk, Function.comp_apply
-- Module: Mathlib.GroupTheory.PushoutI
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
h₁ : ∀ (w : NormalWord (G := G) d), HSMul.hSMul (α := G i) ((φ i : (a : H) → G i) h : G i) w = h • w
⊢ 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

Tactic:
funext w
-- Module: Mathlib.GroupTheory.PushoutI
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
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))
⊢ HSMul.hSMul (α := G i) ((φ i : (a : H) → G i) h : G i) w = h • w

Tactic:
apply NormalWord.ext_smul i

Premises used: Monoid.PushoutI.NormalWord.ext_smul
-- Module: Mathlib.GroupTheory.PushoutI
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 (α := 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:
simp only [summand_smul_def', equivPair, rcons, Word.equivPair_symm, Equiv.coe_fn_mk,
      Equiv.coe_fn_symm_mk, Word.equivPair_smul_same, Word.equivPair_tail_eq_inv_smul,
      Word.rcons_eq_smul, equiv_fst_eq_mul_inv, map_mul, map_inv, mul_smul, inv_smul_smul,
      smul_inv_smul, base_smul_def', MonoidHom.apply_ofInjective_symm]

Premises used: Equiv.coe_fn_symm_mk, map_inv, Monoid.PushoutI.NormalWord.base_smul_def', inv_smul_smul, smul_inv_smul, Monoid.CoprodI.Word.equivPair_symm, map_mul, Monoid.PushoutI.NormalWord.summand_smul_def', Monoid.CoprodI.Word.equivPair_smul_same, Equiv.coe_fn_mk, Monoid.PushoutI.NormalWord.equivPair, Monoid.CoprodI.Word.rcons_eq_smul, Subgroup.IsComplement.equiv_fst_eq_mul_inv, MonoidHom.apply_ofInjective_symm, SemigroupAction.mul_smul, Monoid.CoprodI.Word.equivPair_tail_eq_inv_smul, Monoid.PushoutI.NormalWord.rcons
-- 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) φ
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 =
    mk (G := G) (w.toWord (G := G)) (h * w.head (G := G)) ⋯

Tactic:
rfl

Premises used: FreeMonoid.prodAux, Quotient.liftOn', List.foldl, SMul.comp.smul, Con.liftOn, rfl, Sum.elim
-- 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) φ
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 =
    (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)) ⋯)
        ⋯)

Tactic:
rfl

Premises used: FreeMonoid.prodAux, Quotient.liftOn', Set.Mem, List.foldl, SMul.comp.smul, Con.liftOn, rfl, Monoid.PushoutI.NormalWord.rcons, Sum.elim
-- 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) φ
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
rw₁ 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)) ⋯)
        ⋯))
    ((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)) ⋯)
        ⋯))
⊢ HSMul.hSMul (α := PushoutI (G := G) φ) ((of (G := G) i : (a : G i) → PushoutI φ) g : PushoutI (G := G) φ) w = g • w

Tactic:
rw [summand_smul_def, summand_smul_def']

Premises used: Monoid.PushoutI.NormalWord.summand_smul_def', Monoid.PushoutI.NormalWord.summand_smul_def
-- 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) φ
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
rw₁ rw₂ :
  mk (G := G) (w.toWord (G := G)) (h * w.head (G := G)) ⋯ = mk (G := G) (w.toWord (G := G)) (h * w.head (G := G)) ⋯
⊢ HSMul.hSMul (α := PushoutI (G := G) φ) ((base (G := G) φ : (a : H) → PushoutI φ) h : PushoutI (G := G) φ) w = h • w

Tactic:
rw [base_smul_def, base_smul_def']

Premises used: Monoid.PushoutI.NormalWord.base_smul_def, Monoid.PushoutI.NormalWord.base_smul_def'
-- Module: Mathlib.GroupTheory.PushoutI
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)
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)
⊢ motive w

Tactic:
rcases w with ⟨w, head, h3⟩

Premises used: Monoid.PushoutI.NormalWord.head
-- Module: Mathlib.GroupTheory.PushoutI
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)
convert! : motive (mk (G := G) w 1 h3)
⊢ motive (mk (G := G) w head h3)

Tactic:
convert! base head ⟨w, 1, h3⟩ rfl ?_

Premises used: Monoid.PushoutI.NormalWord.mk, OfNat.ofNat, rfl
-- Module: Mathlib.GroupTheory.PushoutI
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
⊢ 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:
simp [base_smul_def]

Premises used: Monoid.PushoutI.NormalWord.base_smul_def
-- Module: Mathlib.GroupTheory.PushoutI
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
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:
exact empty
-- Module: Mathlib.GroupTheory.PushoutI
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 ⋯)
cons₁ : g ∉ (φ i).range
⊢ motive (mk (G := G) (Word.cons (M := G) g w h1 hg1) 1 h3)

Tactic:
convert!
        cons i g ⟨w, 1, fun _ _ h => h3 _ _ (List.mem_cons_of_mem _ h)⟩ h1
          (h3 _ _ List.mem_cons_self) ?_ rfl (ih ?_)

Premises used: List.mem_cons_of_mem, Monoid.PushoutI.NormalWord.mk, Sigma.mk, List.mem_cons_self, OfNat.ofNat, rfl
-- Module: Mathlib.GroupTheory.PushoutI
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
⊢ Word.cons (M := G) g w h1 hg1 = toWord (G := G) (d := d) (NormalWord.cons (G := G) g (mk (G := G) w 1 ⋯) h1 ⋯)

Tactic:
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)]

Premises used: Iff.mpr, Subgroup.IsComplement.equiv_snd_eq_self_iff_mem, Monoid.PushoutI.NormalWord.Transversal.compl, map_one, Monoid.CoprodI.Word.cons, List.mem_cons_self, OneMemClass.one_mem, mul_one, Monoid.PushoutI.NormalWord.cons