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)
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))
⊢ (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))
have 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))
Tactic: rw [base_smul_eq_smul, prod_base_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)
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)
have mul : (x • y • w).prod (G := G) = x * y * w.prod (G := G)
Tactic: rw [mul_smul, ihx, ihy, mul_assoc]
-- 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)
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)
⊢ ((x * y) • w).prod (G := G) = x * y * w.prod (G := G)
have mul₁ : x * (y • w).prod (G := G) = x * y * w.prod (G := G)
Tactic: rw [mul_smul, ihx, ihy, mul_assoc]
-- 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)
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)
⊢ ((x * y) • w).prod (G := G) = x * y * w.prod (G := G)
have mul₂ : x * (y * w.prod (G := G)) = x * y * w.prod (G := G)
Tactic: rw [mul_smul, ihx, ihy, mul_assoc]
-- 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)
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)
⊢ ((x * y) • w).prod (G := G) = x * y * w.prod (G := G)
have mul₃ : x * (y * w.prod (G := G)) = x * (y * w.prod (G := G))
Tactic: rw [mul_smul, ihx, ihy, mul_assoc]
-- 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)
g : PushoutI (G := G) φ
w : NormalWord (G := G) d
⊢ (g • w).prod (G := G) = g * w.prod (G := G)
have of : ∀ (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))
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]
Cleared hypotheses: g, w
-- 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)
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))
⊢ (g • w).prod (G := G) = g * w.prod (G := G)
have base : ∀ (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))
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]
Cleared hypotheses: g, w
-- 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)
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))
⊢ (g • w).prod (G := G) = g * w.prod (G := G)
have 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)
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]
Cleared hypotheses: g, w
-- 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
_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
⊢ HSMul.hSMul (β := NormalWord (G := G) d) ((cons (G := G) g w hmw hgr).prod (G := G)) (empty (G := G)) =
    cons (G := G) g w hmw hgr
have 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)) =
  cons (G := G) g w hmw hgr
Tactic: rw [prod_cons, mul_smul, ih, cons_eq_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
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
⊢ 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
have 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
Tactic: rw [prod_cons, mul_smul, ih, cons_eq_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
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
⊢ 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
have 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
Tactic: rw [prod_cons, mul_smul, ih, cons_eq_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
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
⊢ 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
have 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
Tactic: rw [prod_cons, mul_smul, ih, cons_eq_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
h_1 : w.head (G := G) = 1
ih : HSMul.hSMul (β := NormalWord (G := G) d) (w.prod (G := G)) (empty (G := G)) = w
⊢ HSMul.hSMul (β := NormalWord (G := G) d)
      ((HSMul.hSMul (α := PushoutI (G := G) φ) ((base (G := G) φ : (a : H) → PushoutI φ) h : PushoutI (G := G) φ)
            w).prod
        (G := G))
      (empty (G := G)) =
    HSMul.hSMul (α := PushoutI (G := G) φ) ((base (G := G) φ : (a : H) → PushoutI φ) h : PushoutI (G := G) φ) w
have base : HSMul.hSMul (β := NormalWord (G := G) d)
    (HMul.hMul (α := PushoutI (G := G) φ) ((base (G := G) φ : (a : H) → PushoutI φ) h : PushoutI (G := G) φ)
      (w.prod (G := G)))
    (empty (G := G)) =
  HSMul.hSMul (α := PushoutI (G := G) φ) ((base (G := G) φ : (a : H) → PushoutI φ) h : PushoutI (G := G) φ) w
Tactic: rw [prod_smul, mul_smul, ih]
-- 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
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
⊢ 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
have 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
Tactic: rw [prod_smul, mul_smul, ih]
-- 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
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
⊢ 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
have 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
Tactic: rw [prod_smul, mul_smul, ih]
-- 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)
w : NormalWord (G := G) d
⊢ HSMul.hSMul (β := NormalWord (G := G) d) (w.prod (G := G)) (empty (G := G)) = w
have empty : HSMul.hSMul (α := PushoutI (G := G) φ) (β := NormalWord (G := G) d) (prod (G := G) (d := d) (empty (G := G)))
    (empty (G := G)) =
  empty (G := G)
Tactic: induction w using consRecOn with
  | empty => simp
  | cons i g w _ _ _ _ ih =>
    rw [prod_cons, mul_smul, ih, cons_eq_smul]
  | base h w _ ih =>
    rw [prod_smul, mul_smul, ih]
Cleared hypotheses: w
-- 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)
w : NormalWord (G := G) d
empty :
  HSMul.hSMul (α := PushoutI (G := G) φ) (β := NormalWord (G := G) d)
      (prod (G := G) (d := d) (NormalWord.empty (G := G))) (NormalWord.empty (G := G)) =
    NormalWord.empty (G := G)
⊢ HSMul.hSMul (β := NormalWord (G := G) d) (w.prod (G := G)) (NormalWord.empty (G := G)) = w
have cons : ∀ (i : ι) (g : G i) (w : NormalWord (G := G) d) (hmw : w.toWord (G := G).fstIdx (M := G) ≠ some i),
  g ∈ d.set (G := G) i →
    ∀ (hgr : g ∉ (φ i).range),
      w.head (G := G) = 1 →
        ∀ (ih : HSMul.hSMul (β := NormalWord (G := G) d) (w.prod (G := G)) (NormalWord.empty (G := G)) = w),
          HSMul.hSMul (β := NormalWord (G := G) d) ((cons (G := G) g w hmw hgr).prod (G := G))
              (NormalWord.empty (G := G)) =
            cons (G := G) g w hmw hgr
Tactic: induction w using consRecOn with
  | empty => simp
  | cons i g w _ _ _ _ ih =>
    rw [prod_cons, mul_smul, ih, cons_eq_smul]
  | base h w _ ih =>
    rw [prod_smul, mul_smul, ih]
Cleared hypotheses: w
-- 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)
w : NormalWord (G := G) d
empty :
  HSMul.hSMul (α := PushoutI (G := G) φ) (β := NormalWord (G := G) d)
      (prod (G := G) (d := d) (NormalWord.empty (G := G))) (NormalWord.empty (G := G)) =
    NormalWord.empty (G := G)
cons :
  ∀ (i : ι) (g : G i) (w : NormalWord (G := G) d) (hmw : w.toWord (G := G).fstIdx (M := G) ≠ some i),
    g ∈ d.set (G := G) i →
      ∀ (hgr : g ∉ (φ i).range),
        w.head (G := G) = 1 →
          ∀ (ih : HSMul.hSMul (β := NormalWord (G := G) d) (w.prod (G := G)) (NormalWord.empty (G := G)) = w),
            HSMul.hSMul (β := NormalWord (G := G) d) ((NormalWord.cons (G := G) g w hmw hgr).prod (G := G))
                (NormalWord.empty (G := G)) =
              NormalWord.cons (G := G) g w hmw hgr
⊢ HSMul.hSMul (β := NormalWord (G := G) d) (w.prod (G := G)) (NormalWord.empty (G := G)) = w
have base : ∀ (h : H) (w : NormalWord (G := G) d),
  w.head (G := G) = 1 →
    ∀ (ih : HSMul.hSMul (β := NormalWord (G := G) d) (w.prod (G := G)) (NormalWord.empty (G := G)) = w),
      HSMul.hSMul (β := NormalWord (G := G) d)
          ((HSMul.hSMul (α := PushoutI (G := G) φ) ((base (G := G) φ : (a : H) → PushoutI φ) h : PushoutI (G := G) φ)
                w).prod
            (G := G))
          (NormalWord.empty (G := G)) =
        HSMul.hSMul (α := PushoutI (G := G) φ) ((base (G := G) φ : (a : H) → PushoutI φ) h : PushoutI (G := G) φ) w
Tactic: induction w using consRecOn with
  | empty => simp
  | cons i g w _ _ _ _ ih =>
    rw [prod_cons, mul_smul, ih, cons_eq_smul]
  | base h w _ ih =>
    rw [prod_smul, mul_smul, ih]
Cleared hypotheses: w
-- 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)
hφ : ∀ (i : ι), Injective.{u_3 + 1, u_2 + 1} (α := H) (β := G i) (⇑(φ i) : (a : H) → G i)
i : ι
⊢ Injective (α := G i) (β := PushoutI (G := G) φ) (⇑(of (G := G) i) : (a : G i) → PushoutI φ)
have rcases : ∀ (d : Transversal (G := G) φ),
  Injective (α := G i) (β := PushoutI (G := G) φ) (⇑(of (G := G) i) : (a : G i) → PushoutI φ)
Tactic: rcases transversal_nonempty φ hφ with ⟨d⟩
-- 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)
hφ : ∀ (i : ι), Injective.{u_3 + 1, u_2 + 1} (α := H) (β := G i) (⇑(φ i) : (a : H) → G i)
i : ι
d : Transversal (G := G) φ
x : DecidableEq ι := Classical.decEq ι
x_1 : (i : ι) → DecidableEq (G i) := fun (i : ι) ↦ Classical.decEq (G i)
⊢ Injective (α := G i) (β := PushoutI (G := G) φ) (⇑(of (G := G) i) : (a : G i) → PushoutI φ)
have refine : Injective (α := G i) (β := NormalWord (G := G) d → NormalWord (G := G) d)
  ((fun (x1 : PushoutI (G := G) φ) (x2 : NormalWord (G := G) d) ↦ x1 • x2) ∘
    (⇑(of (G := G) i) : (a : G i) → PushoutI φ))
Tactic: refine Function.Injective.of_comp
    (f := ((· • ·) : PushoutI φ → NormalWord d → NormalWord d)) ?_
-- 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)
hφ : ∀ (i : ι), Injective.{u_3 + 1, u_2 + 1} (α := H) (β := G i) (⇑(φ i) : (a : H) → G i)
⊢ Injective (α := H) (β := PushoutI (G := G) φ) (⇑(base (G := G) φ) : (a : H) → PushoutI φ)
have rcases : ∀ (d : Transversal (G := G) φ),
  Injective (α := H) (β := PushoutI (G := G) φ) (⇑(base (G := G) φ) : (a : H) → PushoutI φ)
Tactic: rcases transversal_nonempty φ hφ with ⟨d⟩
-- 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)
hφ : ∀ (i : ι), Injective.{u_3 + 1, u_2 + 1} (α := H) (β := G i) (⇑(φ i) : (a : H) → G i)
d : Transversal (G := G) φ
x : DecidableEq ι := Classical.decEq ι
x_1 : (i : ι) → DecidableEq (G i) := fun (i : ι) ↦ Classical.decEq (G i)
⊢ Injective (α := H) (β := PushoutI (G := G) φ) (⇑(base (G := G) φ) : (a : H) → PushoutI φ)
have refine : Injective (α := H) (β := NormalWord (G := G) d → NormalWord (G := G) d)
  ((fun (x1 : PushoutI (G := G) φ) (x2 : NormalWord (G := G) d) ↦ x1 • x2) ∘
    (⇑(base (G := G) φ) : (a : H) → PushoutI φ))
Tactic: refine Function.Injective.of_comp
    (f := ((· • ·) : PushoutI φ → NormalWord d → NormalWord d)) ?_