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)
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 :
  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 ⋯) h1 ⋯)))
⊢ 1 = NormalWord.head (G := G) (d := d) (NormalWord.cons (G := G) g (mk (G := G) w 1 ⋯) h1 ⋯)

Tactic:
apply d.injective i

Premises used: Monoid.PushoutI.NormalWord.Transversal.injective
-- 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
⊢ 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 ⋯) h1 ⋯)))

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

Premises used: Iff.mpr, Subgroup.IsComplement.equiv_snd_eq_self_iff_mem, Monoid.PushoutI.NormalWord.Transversal.compl, map_one, mul_inv_cancel, List.mem_cons_self, OneMemClass.one_mem, mul_one, Subgroup.IsComplement.equiv_fst_eq_mul_inv, MonoidHom.apply_ofInjective_symm, Monoid.PushoutI.NormalWord.cons
-- 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
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
cons₃ cons₄ cons₅ cons₆ : ¬g = 1
⊢ g ∉ (φ i).range

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

Premises used: Iff.mpr, Subgroup.IsComplement.coe_equiv_snd_eq_one_iff_mem, Subgroup.IsComplement.equiv_snd_eq_self_iff_mem, Monoid.PushoutI.NormalWord.Transversal.compl, Monoid.PushoutI.NormalWord.Transversal.one_mem, SetLike.mem_coe, List.mem_cons_self, OneMemClass.one_mem
-- 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
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)
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)
⊢ motive (mk (G := G) w 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)]

Premises used: map_one, SetLike.mem_coe, mul_inv_cancel, Monoid.CoprodI.Word.cons, mul_one, Subgroup.IsComplement.equiv_fst_eq_mul_inv, MonoidHom.apply_ofInjective_symm, Monoid.PushoutI.NormalWord.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) φ
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
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))
⊢ 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

Tactic:
apply 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
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
⊢ 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:
simp only [cons, Word.cons_eq_smul, MonoidHom.apply_ofInjective_symm,
    equiv_fst_eq_mul_inv, mul_assoc, map_mul, map_inv, mul_smul, inv_smul_smul, summand_smul_def,
    equivPair, rcons, Word.equivPair_symm, Word.rcons_eq_smul, Equiv.coe_fn_mk,
    Word.equivPair_tail_eq_inv_smul, Equiv.coe_fn_symm_mk, smul_inv_smul]

Premises used: Equiv.coe_fn_symm_mk, map_inv, mul_assoc, Monoid.CoprodI.Word.cons_eq_smul, inv_smul_smul, smul_inv_smul, Monoid.CoprodI.Word.equivPair_symm, map_mul, 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, Monoid.PushoutI.NormalWord.summand_smul_def, Monoid.PushoutI.NormalWord.cons, 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)
i : ι
g : G i
w : NormalWord (G := G) d
⊢ (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:
simp only [prod, 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, ← of_apply_eq_base φ i,
    MonoidHom.apply_ofInjective_symm, equiv_fst_eq_mul_inv, mul_assoc, map_mul, map_inv,
    Word.prod_smul, ofCoprodI_of, inv_mul_cancel_left, mul_inv_cancel_left]

Premises used: Equiv.coe_fn_symm_mk, map_inv, inv_mul_cancel_left, Monoid.PushoutI.NormalWord.prod, Monoid.CoprodI.Word.prod_smul, mul_assoc, Monoid.PushoutI.of_apply_eq_base, Monoid.PushoutI.ofCoprodI_of, 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, mul_inv_cancel_left, MonoidHom.apply_ofInjective_symm, 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)
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))
of₁ 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))
⊢ (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))

Tactic:
rw [of_smul_eq_smul, prod_summand_smul]

Premises used: Monoid.PushoutI.NormalWord.prod_summand_smul, Monoid.PushoutI.NormalWord.of_smul_eq_smul
-- 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
base :
  (h • w).prod (G := G) =
    HMul.hMul (α := PushoutI (G := G) φ) ((PushoutI.base (G := G) φ : (a : H) → PushoutI φ) h : PushoutI (G := G) φ)
      (w.prod (G := G))
base₁ base₂ :
  HMul.hMul (α := PushoutI (G := G) φ) ((PushoutI.base (G := G) φ : (a : H) → PushoutI φ) h : PushoutI (G := G) φ)
      (w.prod (G := G)) =
    HMul.hMul (α := PushoutI (G := G) φ) ((PushoutI.base (G := G) φ : (a : H) → PushoutI φ) h : PushoutI (G := G) φ)
      (w.prod (G := G))
⊢ (HSMul.hSMul (α := PushoutI (G := G) φ) ((PushoutI.base (G := G) φ : (a : H) → PushoutI φ) h : PushoutI (G := G) φ)
          w).prod
      (G := G) =
    HMul.hMul (α := PushoutI (G := G) φ) ((PushoutI.base (G := G) φ : (a : H) → PushoutI φ) h : PushoutI (G := G) φ)
      (w.prod (G := G))

Tactic:
rw [base_smul_eq_smul, prod_base_smul]

Premises used: Monoid.PushoutI.NormalWord.base_smul_eq_smul, Monoid.PushoutI.NormalWord.prod_base_smul
-- 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)
x y : PushoutI (G := G) φ
ihx : ∀ (w : NormalWord (G := G) d), (x • w).prod (G := G) = x * w.prod (G := G)
ihy : ∀ (w : NormalWord (G := G) d), (y • w).prod (G := G) = y * w.prod (G := G)
w : NormalWord (G := G) d
mul : (x • y • w).prod (G := G) = x * y * w.prod (G := G)
mul₁ : x * (y • w).prod (G := G) = x * y * w.prod (G := G)
mul₂ : x * (y * w.prod (G := G)) = x * y * w.prod (G := G)
mul₃ mul₄ : x * (y * w.prod (G := G)) = x * (y * w.prod (G := G))
⊢ ((x * y) • w).prod (G := G) = x * y * w.prod (G := G)

Tactic:
rw [mul_smul, ihx, ihy, mul_assoc]

Premises used: mul_assoc, SemigroupAction.mul_smul
-- 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)
g : PushoutI (G := G) φ
w : NormalWord (G := G) d
of :
  ∀ (i : ι) (g : G i) (w : NormalWord (G := G) d),
    (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))
base :
  ∀ (h : H) (w : NormalWord (G := G) d),
    (HSMul.hSMul (α := PushoutI (G := G) φ) ((PushoutI.base (G := G) φ : (a : H) → PushoutI φ) h : PushoutI (G := G) φ)
            w).prod
        (G := G) =
      HMul.hMul (α := PushoutI (G := G) φ) ((PushoutI.base (G := G) φ : (a : H) → PushoutI φ) h : PushoutI (G := G) φ)
        (w.prod (G := G))
mul :
  ∀ (x y : PushoutI (G := G) φ) (ihx : ∀ (w : NormalWord (G := G) d), (x • w).prod (G := G) = x * w.prod (G := G))
    (ihy : ∀ (w : NormalWord (G := G) d), (y • w).prod (G := G) = y * w.prod (G := G)) (w : NormalWord (G := G) d),
    ((x * y) • w).prod (G := G) = x * y * w.prod (G := G)
⊢ (g • w).prod (G := G) = g * w.prod (G := G)

Tactic:
induction g using PushoutI.induction_on generalizing w with
  | of i g => rw [of_smul_eq_smul, prod_summand_smul]
  | base h => rw [base_smul_eq_smul, prod_base_smul]
  | mul x y ihx ihy => rw [mul_smul, ihx, ihy, mul_assoc]

Premises used: Monoid.PushoutI.induction_on, Monoid.PushoutI.NormalWord.base_smul_eq_smul, mul_assoc, Subgroup.mul, Monoid.PushoutI.base, Monoid.PushoutI.NormalWord.prod_summand_smul, Monoid.PushoutI.NormalWord.prod_base_smul, Monoid.PushoutI.NormalWord.of_smul_eq_smul, Monoid.PushoutI.of, SemigroupAction.mul_smul
-- 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)
⊢ HSMul.hSMul (α := PushoutI (G := G) φ) (β := NormalWord (G := G) d) (prod (G := G) (d := d) (empty (G := G)))
      (empty (G := G)) =
    empty (G := G)

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)
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
_hgn : g ∈ d.set (G := G) i
hgr : g ∉ (φ i).range
_hw1 : w.head (G := G) = 1
ih : HSMul.hSMul (β := NormalWord (G := G) d) (w.prod (G := G)) (empty (G := G)) = w
cons :
  HSMul.hSMul (β := NormalWord (G := G) d)
      (HMul.hMul (α := PushoutI (G := G) φ) ((of (G := G) i : (a : G i) → PushoutI φ) g : PushoutI (G := G) φ)
        (w.prod (G := G)))
      (empty (G := G)) =
    NormalWord.cons (G := G) g w hmw hgr
cons₁ :
  HSMul.hSMul (α := PushoutI (G := G) φ) ((of (G := G) i : (a : G i) → PushoutI φ) g : PushoutI (G := G) φ)
      (HSMul.hSMul (β := NormalWord (G := G) d) (w.prod (G := G)) (empty (G := G))) =
    NormalWord.cons (G := G) g w hmw hgr
cons₂ :
  HSMul.hSMul (α := PushoutI (G := G) φ) ((of (G := G) i : (a : G i) → PushoutI φ) g : PushoutI (G := G) φ) w =
    NormalWord.cons (G := G) g w hmw hgr
cons₃ cons₄ :
  HSMul.hSMul (α := PushoutI (G := G) φ) ((of (G := G) i : (a : G i) → PushoutI φ) g : PushoutI (G := G) φ) w =
    HSMul.hSMul (α := PushoutI (G := G) φ) ((of (G := G) i : (a : G i) → PushoutI φ) g : PushoutI (G := G) φ) w
⊢ HSMul.hSMul (β := NormalWord (G := G) d) ((NormalWord.cons (G := G) g w hmw hgr).prod (G := G)) (empty (G := G)) =
    NormalWord.cons (G := G) g w hmw hgr

Tactic:
rw [prod_cons, mul_smul, ih, cons_eq_smul]

Premises used: Monoid.PushoutI.NormalWord.prod_cons, Monoid.PushoutI.NormalWord.cons_eq_smul, SemigroupAction.mul_smul
-- 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
h_1 : w.head (G := G) = 1
ih : HSMul.hSMul (β := NormalWord (G := G) d) (w.prod (G := G)) (empty (G := G)) = w
base :
  HSMul.hSMul (β := NormalWord (G := G) d)
      (HMul.hMul (α := PushoutI (G := G) φ) ((PushoutI.base (G := G) φ : (a : H) → PushoutI φ) h : PushoutI (G := G) φ)
        (w.prod (G := G)))
      (empty (G := G)) =
    HSMul.hSMul (α := PushoutI (G := G) φ) ((PushoutI.base (G := G) φ : (a : H) → PushoutI φ) h : PushoutI (G := G) φ) w
base₁ :
  HSMul.hSMul (α := PushoutI (G := G) φ) ((PushoutI.base (G := G) φ : (a : H) → PushoutI φ) h : PushoutI (G := G) φ)
      (HSMul.hSMul (β := NormalWord (G := G) d) (w.prod (G := G)) (empty (G := G))) =
    HSMul.hSMul (α := PushoutI (G := G) φ) ((PushoutI.base (G := G) φ : (a : H) → PushoutI φ) h : PushoutI (G := G) φ) w
base₂ base₃ :
  HSMul.hSMul (α := PushoutI (G := G) φ) ((PushoutI.base (G := G) φ : (a : H) → PushoutI φ) h : PushoutI (G := G) φ) w =
    HSMul.hSMul (α := PushoutI (G := G) φ) ((PushoutI.base (G := G) φ : (a : H) → PushoutI φ) h : PushoutI (G := G) φ) w
⊢ HSMul.hSMul (β := NormalWord (G := G) d)
      ((HSMul.hSMul (α := PushoutI (G := G) φ)
            ((PushoutI.base (G := G) φ : (a : H) → PushoutI φ) h : PushoutI (G := G) φ) w).prod
        (G := G))
      (empty (G := G)) =
    HSMul.hSMul (α := PushoutI (G := G) φ) ((PushoutI.base (G := G) φ : (a : H) → PushoutI φ) h : PushoutI (G := G) φ) w

Tactic:
rw [prod_smul, mul_smul, ih]

Premises used: Monoid.PushoutI.NormalWord.prod_smul, SemigroupAction.mul_smul