awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.GroupTheory.CoprodI (goal)
Goal:
ι : Type u_1
M : ι → Type u_2
inst : (i : ι) → Monoid (M i)
inst_1 : DecidableEq ι
inst_2 : (i : ι) → DecidableEq (M i)
w : Word M
hnil : ¬w.toList (M := M) = []
m₂ m₁ : M ((w.toList (M := M).head hnil).fst (β := fun (i : ι) ↦ M i))
hw :
  Sigma.mk (β := fun (i : ι) ↦ M i) ((w.toList (M := M).head hnil).fst (β := fun (i : ι) ↦ M i)) m₁ ∉
    w.toList (M := M).tail
hm1 : ¬m₁ = 1
pos :
  m₁ = m₂ * (w.toList (M := M).head ⋯).snd (β := fun (i : ι) ↦ M i) →
    (∃ (m' : M ((w.toList (M := M).head hnil).fst (β := fun (i : ι) ↦ M i))),
        w.toList (M := M).head hnil =
            Sigma.mk (β := fun (i : ι) ↦ M i) ((w.toList (M := M).head hnil).fst (β := fun (i : ι) ↦ M i)) m' ∧
          m₁ = m₂ * m') ∨
      ¬w.fstIdx (M := M) = some ((w.toList (M := M).head hnil).fst (β := fun (i : ι) ↦ M i)) ∧ m₁ = m₂
⊢ m₁ = m₂ * (w.toList (M := M).head ⋯).snd (β := fun (i : ι) ↦ M i) ↔
    (∃ (m' : M ((w.toList (M := M).head hnil).fst (β := fun (i : ι) ↦ M i))),
        w.toList (M := M).head hnil =
            Sigma.mk (β := fun (i : ι) ↦ M i) ((w.toList (M := M).head hnil).fst (β := fun (i : ι) ↦ M i)) m' ∧
          m₁ = m₂ * m') ∨
      ¬w.fstIdx (M := M) = some ((w.toList (M := M).head hnil).fst (β := fun (i : ι) ↦ M i)) ∧ m₁ = m₂
have pos₁ : (∃ (m' : M ((w.toList (M := M).head hnil).fst (β := fun (i : ι) ↦ M i))),
      w.toList (M := M).head hnil =
          Sigma.mk (β := fun (i : ι) ↦ M i) ((w.toList (M := M).head hnil).fst (β := fun (i : ι) ↦ M i)) m' ∧
        m₁ = m₂ * m') ∨
    ¬w.fstIdx (M := M) = some ((w.toList (M := M).head hnil).fst (β := fun (i : ι) ↦ M i)) ∧ m₁ = m₂ →
  m₁ = m₂ * (w.toList (M := M).head sorry).snd (β := fun (i : ι) ↦ M i)
Tactic: constructor
-- Lean 4 proof step from Mathlib.GroupTheory.CoprodI (hypothesis)
Goal:
ι : Type u_1
M : ι → Type u_2
inst : (i : ι) → Monoid (M i)
inst_1 : DecidableEq ι
inst_2 : (i : ι) → DecidableEq (M i)
w : Word M
hnil : ¬w.toList (M := M) = []
m₂ w_1 : M ((w.toList (M := M).head hnil).fst (β := fun (i : ι) ↦ M i))
h :
  w.toList (M := M).head hnil =
    Sigma.mk (β := fun (i : ι) ↦ M i) ((w.toList (M := M).head hnil).fst (β := fun (i : ι) ↦ M i)) w_1
hw :
  Sigma.mk (β := fun (i : ι) ↦ M i) ((w.toList (M := M).head hnil).fst (β := fun (i : ι) ↦ M i)) (m₂ * w_1) ∉
    w.toList (M := M).tail
hm1 : ¬m₂ * w_1 = 1
⊢ m₂ * w_1 = m₂ * (w.toList (M := M).head ⋯).snd (β := fun (i : ι) ↦ M i)
have h₁ : (w.toList (M := M).head hnil).snd (β := fun (i : ι) ↦ M i) = w_1
Tactic: simp only [Sigma.ext_iff, heq_eq_eq, true_and] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.GroupTheory.CoprodI (goal)
Goal:
ι : Type u_1
M : ι → Type u_2
inst : (i : ι) → Monoid (M i)
inst_1 : DecidableEq ι
inst_2 : (i : ι) → DecidableEq (M i)
w : Word M
hnil : ¬w.toList (M := M) = []
m₂ w_1 : M ((w.toList (M := M).head hnil).fst (β := fun (i : ι) ↦ M i))
hw :
  Sigma.mk (β := fun (i : ι) ↦ M i) ((w.toList (M := M).head hnil).fst (β := fun (i : ι) ↦ M i)) (m₂ * w_1) ∉
    w.toList (M := M).tail
hm1 : ¬m₂ * w_1 = 1
h : (w.toList (M := M).head hnil).snd (β := fun (i : ι) ↦ M i) = w_1
⊢ m₂ * w_1 = m₂ * (w.toList (M := M).head ⋯).snd (β := fun (i : ι) ↦ M i)
have pos : ∀
  (hw :
    Sigma.mk (β := fun (i : ι) ↦ M i) ((w.toList (M := M).head hnil).fst (β := fun (i : ι) ↦ M i))
        (m₂ * (w.toList (M := M).head hnil).snd (β := fun (i : ι) ↦ M i)) ∉
      w.toList (M := M).tail)
  (hm1 : ¬m₂ * (w.toList (M := M).head hnil).snd (β := fun (i : ι) ↦ M i) = 1),
  m₂ * (w.toList (M := M).head hnil).snd (β := fun (i : ι) ↦ M i) =
    m₂ * (w.toList (M := M).head sorry).snd (β := fun (i : ι) ↦ M i)
Tactic: subst h
Cleared hypotheses: w_1, hw, hm1, h
-- Lean 4 proof step from Mathlib.GroupTheory.CoprodI (hypothesis)
Goal:
ι : Type u_1
M : ι → Type u_2
inst : (i : ι) → Monoid (M i)
inst_1 : DecidableEq ι
inst_2 : (i : ι) → DecidableEq (M i)
w : Word M
hnil : ¬w.toList (M := M) = []
m₂ m₁ : M ((w.toList (M := M).head hnil).fst (β := fun (i : ι) ↦ M i))
hw :
  Sigma.mk (β := fun (i : ι) ↦ M i) ((w.toList (M := M).head hnil).fst (β := fun (i : ι) ↦ M i)) m₁ ∉
    w.toList (M := M).tail
hm1 : ¬m₁ = 1
hm' : ¬w.fstIdx (M := M) = some ((w.toList (M := M).head hnil).fst (β := fun (i : ι) ↦ M i)) ∧ m₁ = m₂
⊢ m₁ = m₂ * (w.toList (M := M).head ⋯).snd (β := fun (i : ι) ↦ M i)
have hm'₁ : (∀ (x : M ((w.toList (M := M).head hnil).fst (β := fun (i : ι) ↦ M i))),
    ¬w.toList (M := M).head? =
        some (Sigma.mk (β := fun (a : ι) ↦ M a) ((w.toList (M := M).head hnil).fst (β := fun (i : ι) ↦ M i)) x)) ∧
  m₁ = m₂
Tactic: simp only [fstIdx, Option.map_eq_some_iff, Sigma.exists,
              exists_and_right, exists_eq_right, not_exists] at hm'
Cleared hypotheses: hm'
-- Lean 4 proof step from Mathlib.GroupTheory.CoprodI (goal)
Goal:
ι : Type u_1
M : ι → Type u_2
inst : (i : ι) → Monoid (M i)
inst_1 : DecidableEq ι
inst_2 : (i : ι) → DecidableEq (M i)
w : Word M
hnil : ¬w.toList (M := M) = []
m₂ m₁ : M ((w.toList (M := M).head hnil).fst (β := fun (i : ι) ↦ M i))
hw :
  Sigma.mk (β := fun (i : ι) ↦ M i) ((w.toList (M := M).head hnil).fst (β := fun (i : ι) ↦ M i)) m₁ ∉
    w.toList (M := M).tail
hm1 : ¬m₁ = 1
hm' :
  (∀ (x : M ((w.toList (M := M).head hnil).fst (β := fun (i : ι) ↦ M i))),
      ¬w.toList (M := M).head? =
          some (Sigma.mk (β := fun (a : ι) ↦ M a) ((w.toList (M := M).head hnil).fst (β := fun (i : ι) ↦ M i)) x)) ∧
    m₁ = m₂
⊢ w.toList (M := M).head? =
    some
      (Sigma.mk (β := fun (a : ι) ↦ M a) ((w.toList (M := M).head hnil).fst (β := fun (i : ι) ↦ M i))
        ((w.toList (M := M).head hnil).snd (β := fun (i : ι) ↦ M i)))
have rw : some (w.toList (M := M).head hnil) =
  some
    (Sigma.mk (β := fun (a : ι) ↦ M a) ((w.toList (M := M).head hnil).fst (β := fun (i : ι) ↦ M i))
      ((w.toList (M := M).head hnil).snd (β := fun (i : ι) ↦ M i)))
Tactic: rw [List.head?_eq_some_head]
-- Lean 4 proof step from Mathlib.GroupTheory.CoprodI (goal)
Goal:
ι : Type u_1
M : ι → Type u_2
inst : (i : ι) → Monoid (M i)
inst_1 : DecidableEq ι
inst_2 : (i : ι) → DecidableEq (M i)
w : Word M
hnil : ¬w.toList (M := M) = []
m₂ m₁ : M ((w.toList (M := M).head hnil).fst (β := fun (i : ι) ↦ M i))
hw :
  Sigma.mk (β := fun (i : ι) ↦ M i) ((w.toList (M := M).head hnil).fst (β := fun (i : ι) ↦ M i)) m₁ ∉
    w.toList (M := M).tail
hm1 : ¬m₁ = 1
hm' :
  (∀ (x : M ((w.toList (M := M).head hnil).fst (β := fun (i : ι) ↦ M i))),
      ¬w.toList (M := M).head? =
          some (Sigma.mk (β := fun (a : ι) ↦ M a) ((w.toList (M := M).head hnil).fst (β := fun (i : ι) ↦ M i)) x)) ∧
    m₁ = m₂
rw :
  some (w.toList (M := M).head hnil) =
    some
      (Sigma.mk (β := fun (a : ι) ↦ M a) ((w.toList (M := M).head hnil).fst (β := fun (i : ι) ↦ M i))
        ((w.toList (M := M).head hnil).snd (β := fun (i : ι) ↦ M i)))
⊢ w.toList (M := M).head? =
    some
      (Sigma.mk (β := fun (a : ι) ↦ M a) ((w.toList (M := M).head hnil).fst (β := fun (i : ι) ↦ M i))
        ((w.toList (M := M).head hnil).snd (β := fun (i : ι) ↦ M i)))
have rw₁ : w.toList (M := M) ≠ []
Tactic: rw [List.head?_eq_some_head]
-- Lean 4 proof step from Mathlib.GroupTheory.CoprodI (goal)
Goal:
ι : Type u_1
M : ι → Type u_2
inst : (i : ι) → Monoid (M i)
inst_1 : DecidableEq ι
inst_2 : (i : ι) → DecidableEq (M i)
j : ι
m₂ : M j
w : Word M
m₁ : M j
hw : Sigma.mk (β := fun (i : ι) ↦ M i) j m₁ ∉ w.toList (M := M).tail
hm1 : ¬m₁ = 1
h : ¬∃ (h : ¬w.toList (M := M) = []), (w.toList (M := M).head h).fst (β := fun (i : ι) ↦ M i) = j
⊢ m₁ = m₂ * 1 ↔
    (∃ (m' : M j), w.toList (M := M).head? = some (Sigma.mk (β := fun (i : ι) ↦ M i) j m') ∧ m₁ = m₂ * m') ∨
      ¬w.fstIdx (M := M) = some j ∧ m₁ = m₂
have neg : ∀ (h : ¬∃ (h : ¬w.toList (M := M) = []), (w.toList (M := M).head h).fst (β := fun (i : ι) ↦ M i) = j),
  m₁ = m₂ * 1 ↔
    (∃ (m' : M j), w.toList (M := M).head? = some (Sigma.mk (β := fun (i : ι) ↦ M i) j m') ∧ m₁ = m₂ * m') ∨
      ¬w.fstIdx (M := M) = some j ∧ m₁ = m₂
Tactic: revert h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.GroupTheory.CoprodI (goal)
Goal:
ι : Type u_1
M : ι → Type u_2
inst : (i : ι) → Monoid (M i)
inst_1 : DecidableEq ι
inst_2 : (i : ι) → DecidableEq (M i)
j : ι
m₂ : M j
w : Word M
m₁ : M j
hw : Sigma.mk (β := fun (i : ι) ↦ M i) j m₁ ∉ w.toList (M := M).tail
hm1 : ¬m₁ = 1
⊢ ∀ (h : ¬∃ (h : ¬w.toList (M := M) = []), (w.toList (M := M).head h).fst (β := fun (i : ι) ↦ M i) = j),
    m₁ = m₂ * 1 ↔
      (∃ (m' : M j), w.toList (M := M).head? = some (Sigma.mk (β := fun (i : ι) ↦ M i) j m') ∧ m₁ = m₂ * m') ∨
        ¬Option.map (Sigma.fst (β := fun (i : ι) ↦ M i)) w.toList (M := M).head? = some j ∧ m₁ = m₂
have neg : ∀ (h : ¬∃ (h : ¬Eq (α := List ((i : ι) × M i)) [] []), (List.head [] h).fst (β := fun (i : ι) ↦ M i) = j),
  m₁ = m₂ * 1 ↔
    (∃ (m' : M j), List.head? [] = some (Sigma.mk (β := fun (i : ι) ↦ M i) j m') ∧ m₁ = m₂ * m') ∨
      ¬Option.map (α := (i : ι) × M i) (Sigma.fst (β := fun (i : ι) ↦ M i)) (List.head? []) = some j ∧ m₁ = m₂
Tactic: cases w.toList
-- Lean 4 proof step from Mathlib.GroupTheory.CoprodI (goal)
Goal:
ι : Type u_1
M : ι → Type u_2
inst : (i : ι) → Monoid (M i)
inst_1 : DecidableEq ι
inst_2 : (i : ι) → DecidableEq (M i)
j : ι
m₂ : M j
w : Word M
m₁ : M j
hw : Sigma.mk (β := fun (i : ι) ↦ M i) j m₁ ∉ w.toList (M := M).tail
hm1 : ¬m₁ = 1
neg :
  ∀ (h : ¬∃ (h : ¬Eq (α := List ((i : ι) × M i)) [] []), (List.head [] h).fst (β := fun (i : ι) ↦ M i) = j),
    m₁ = m₂ * 1 ↔
      (∃ (m' : M j), List.head? [] = some (Sigma.mk (β := fun (i : ι) ↦ M i) j m') ∧ m₁ = m₂ * m') ∨
        ¬Option.map (α := (i : ι) × M i) (Sigma.fst (β := fun (i : ι) ↦ M i)) (List.head? []) = some j ∧ m₁ = m₂
⊢ ∀ (h : ¬∃ (h : ¬w.toList (M := M) = []), (w.toList (M := M).head h).fst (β := fun (i : ι) ↦ M i) = j),
    m₁ = m₂ * 1 ↔
      (∃ (m' : M j), w.toList (M := M).head? = some (Sigma.mk (β := fun (i : ι) ↦ M i) j m') ∧ m₁ = m₂ * m') ∨
        ¬Option.map (Sigma.fst (β := fun (i : ι) ↦ M i)) w.toList (M := M).head? = some j ∧ m₁ = m₂
have neg₁ : ∀ (head : (i : ι) × M i) (tail : List ((i : ι) × M i))
  (h : ¬∃ (h : ¬head :: tail = []), ((head :: tail).head h).fst (β := fun (i : ι) ↦ M i) = j),
  m₁ = m₂ * 1 ↔
    (∃ (m' : M j), (head :: tail).head? = some (Sigma.mk (β := fun (i : ι) ↦ M i) j m') ∧ m₁ = m₂ * m') ∨
      ¬Option.map (Sigma.fst (β := fun (i : ι) ↦ M i)) (head :: tail).head? = some j ∧ m₁ = m₂
Tactic: cases w.toList
-- Lean 4 proof step from Mathlib.GroupTheory.CoprodI (goal)
Goal:
ι : Type u_1
M : ι → Type u_2
inst : (i : ι) → Monoid (M i)
inst_1 : DecidableEq ι
inst_2 : (i : ι) → DecidableEq (M i)
i : ι
m : M i
ls : Word M
h1 : ls.fstIdx (M := M) ≠ some i
h2 : m ≠ 1
⊢ cons (M := M) m ls h1 h2 = HSMul.hSMul (α := CoprodI M) ((of (M := M) : (a : M i) → CoprodI M) m : CoprodI M) ls
have rw : cons (M := M) m ls h1 h2 =
  rcons (M := M) (i := i)
    (have __src := Pair.mk (M := M) 1 ls h1;
    Pair.mk (M := M) (m * (Pair.mk (M := M) 1 ls h1).head (M := M)) (__src.tail (M := M)) sorry)
Tactic: rw [of_smul_def, equivPair_eq_of_fstIdx_ne _]
-- Lean 4 proof step from Mathlib.GroupTheory.CoprodI (goal)
Goal:
ι : Type u_1
M : ι → Type u_2
inst : (i : ι) → Monoid (M i)
inst_1 : DecidableEq ι
inst_2 : (i : ι) → DecidableEq (M i)
i : ι
w : Word M
⊢ HSMul.hSMul (α := CoprodI M) (β := Word M)
      ((of (M := M) : (a : M i) → CoprodI M) (Pair.head (M := M) ((equivPair (M := M) i : (a : Word M) → Pair M i) w)) :
        CoprodI M)
      (Pair.tail (M := M) (i := i) ((equivPair (M := M) i : (a : Word M) → Pair M i) w) : Word M) =
    w
have rw : rcons (M := M) (i := i) ((equivPair (M := M) i : (a : Word M) → Pair M i) w) = w
Tactic: rw [← rcons_eq_smul, ← equivPair_symm, Equiv.symm_apply_apply]
-- Lean 4 proof step from Mathlib.GroupTheory.CoprodI (goal)
Goal:
ι : Type u_1
M : ι → Type u_2
inst : (i : ι) → Monoid (M i)
inst_1 : DecidableEq ι
inst_2 : (i : ι) → DecidableEq (M i)
i : ι
w : Word M
rw : rcons (M := M) (i := i) ((equivPair (M := M) i : (a : Word M) → Pair M i) w) = w
⊢ HSMul.hSMul (α := CoprodI M) (β := Word M)
      ((of (M := M) : (a : M i) → CoprodI M) (Pair.head (M := M) ((equivPair (M := M) i : (a : Word M) → Pair M i) w)) :
        CoprodI M)
      (Pair.tail (M := M) (i := i) ((equivPair (M := M) i : (a : Word M) → Pair M i) w) : Word M) =
    w
have rw₁ : (Equiv.symm (equivPair (M := M) i) : (a : Pair M i) → Word M) ((equivPair (M := M) i : (a : Word M) → Pair M i) w) = w
Tactic: rw [← rcons_eq_smul, ← equivPair_symm, Equiv.symm_apply_apply]
-- Lean 4 proof step from Mathlib.GroupTheory.CoprodI (goal)
Goal:
ι : Type u_1
M : ι → Type u_2
inst : (i : ι) → Monoid (M i)
inst_1 : DecidableEq ι
inst_2 : (i : ι) → DecidableEq (M i)
i : ι
w : Word M
rw : rcons (M := M) (i := i) ((equivPair (M := M) i : (a : Word M) → Pair M i) w) = w
rw₁ :
  (Equiv.symm (equivPair (M := M) i) : (a : Pair M i) → Word M) ((equivPair (M := M) i : (a : Word M) → Pair M i) w) = w
⊢ HSMul.hSMul (α := CoprodI M) (β := Word M)
      ((of (M := M) : (a : M i) → CoprodI M) (Pair.head (M := M) ((equivPair (M := M) i : (a : Word M) → Pair M i) w)) :
        CoprodI M)
      (Pair.tail (M := M) (i := i) ((equivPair (M := M) i : (a : Word M) → Pair M i) w) : Word M) =
    w
have rw₂ : w = w
Tactic: rw [← rcons_eq_smul, ← equivPair_symm, Equiv.symm_apply_apply]
-- Lean 4 proof step from Mathlib.GroupTheory.CoprodI (goal)
Goal:
ι : Type u_1
M : ι → Type u_2
inst : (i : ι) → Monoid (M i)
inst_1 : DecidableEq ι
inst_2 : (i : ι) → DecidableEq (M i)
motive : Word M → Prop
empty : motive (Word.empty (M := M))
smul :
  ∀ (i : ι) (m : M i) (w : Word M),
    motive w → motive (HSMul.hSMul (α := CoprodI M) ((of (M := M) : (a : M i) → CoprodI M) m : CoprodI M) w)
i : ι
m : M i
w : Word M
h1 : w.fstIdx (M := M) ≠ some i
h2 : m ≠ 1
ih : motive w
⊢ motive (cons (M := M) m w h1 h2)
have cons : motive (HSMul.hSMul (α := CoprodI M) ((of (M := M) : (a : M i) → CoprodI M) m : CoprodI M) w)
Tactic: rw [cons_eq_smul]
-- Lean 4 proof step from Mathlib.GroupTheory.CoprodI (goal)
Goal:
ι : Type u_1
M : ι → Type u_2
inst : (i : ι) → Monoid (M i)
inst_1 : DecidableEq ι
inst_2 : (i : ι) → DecidableEq (M i)
motive : Word M → Prop
empty : motive (Word.empty (M := M))
smul :
  ∀ (i : ι) (m : M i) (w : Word M),
    motive w → motive (HSMul.hSMul (α := CoprodI M) ((of (M := M) : (a : M i) → CoprodI M) m : CoprodI M) w)
w : Word M
empty₁ : motive (Word.empty (M := M))
⊢ motive w
have cons : ∀ (i : ι) (m : M i) (w : Word M) (h1 : w.fstIdx (M := M) ≠ some i) (h2 : m ≠ 1) (ih : motive w),
  motive (cons (M := M) m w h1 h2)
Tactic: induction w using consRecOn with
  | empty => exact empty
  | cons _ _ _ _ _ ih =>
    rw [cons_eq_smul]
    exact smul _ _ _ ih
Cleared hypotheses: w
-- Lean 4 proof step from Mathlib.GroupTheory.CoprodI (goal)
Goal:
ι : Type u_1
M : ι → Type u_2
inst : (i : ι) → Monoid (M i)
inst_1 : DecidableEq ι
inst_2 : (i : ι) → DecidableEq (M i)
w : Word M
⊢ (HSMul.hSMul (α := CoprodI M) 1 w).prod (M := M) = 1 * w.prod (M := M)
have one : w.prod (M := M) = 1 * w.prod (M := M)
Tactic: rw [one_smul, one_mul]
-- Lean 4 proof step from Mathlib.GroupTheory.CoprodI (goal)
Goal:
ι : Type u_1
M : ι → Type u_2
inst : (i : ι) → Monoid (M i)
inst_1 : DecidableEq ι
inst_2 : (i : ι) → DecidableEq (M i)
w : Word M
one : w.prod (M := M) = 1 * w.prod (M := M)
⊢ (HSMul.hSMul (α := CoprodI M) 1 w).prod (M := M) = 1 * w.prod (M := M)
have one₁ : w.prod (M := M) = w.prod (M := M)
Tactic: rw [one_smul, one_mul]
-- Lean 4 proof step from Mathlib.GroupTheory.CoprodI (goal)
Goal:
ι : Type u_1
M : ι → Type u_2
inst : (i : ι) → Monoid (M i)
inst_1 : DecidableEq ι
inst_2 : (i : ι) → DecidableEq (M i)
i : ι
m : M i
w : Word M
⊢ (HSMul.hSMul (α := CoprodI M) ((of (M := M) : (a : M i) → CoprodI M) m : CoprodI M) w).prod (M := M) =
    HMul.hMul (α := CoprodI M) ((of (M := M) : (a : M i) → CoprodI M) m : CoprodI M) (w.prod (M := M))
have of : prod (M := M)
    (rcons (M := M) (i := i)
      (have __src : Pair M i := (equivPair (M := M) i : (a : Word M) → Pair M i) w;
      Pair.mk (M := M)
        (HMul.hMul (β := M i) m (Pair.head (M := M) ((equivPair (M := M) i : (a : Word M) → Pair M i) w) : M i))
        (__src.tail (M := M)) sorry)) =
  HMul.hMul (α := CoprodI M) ((of (M := M) : (a : M i) → CoprodI M) m : CoprodI M) (w.prod (M := M))
Tactic: rw [of_smul_def, prod_rcons, of.map_mul, mul_assoc, ← prod_rcons, ← equivPair_symm,
      Equiv.symm_apply_apply]
-- Lean 4 proof step from Mathlib.GroupTheory.CoprodI (goal)
Goal:
ι : Type u_1
M : ι → Type u_2
inst : (i : ι) → Monoid (M i)
inst_1 : DecidableEq ι
inst_2 : (i : ι) → DecidableEq (M i)
i : ι
m : M i
w : Word M
of :
  prod (M := M)
      (rcons (M := M) (i := i)
        (have __src : Pair M i := (equivPair (M := M) i : (a : Word M) → Pair M i) w;
        Pair.mk (M := M)
          (HMul.hMul (β := M i) m (Pair.head (M := M) ((equivPair (M := M) i : (a : Word M) → Pair M i) w) : M i))
          (__src.tail (M := M)) ⋯)) =
    HMul.hMul (α := CoprodI M) ((CoprodI.of (M := M) : (a : M i) → CoprodI M) m : CoprodI M) (w.prod (M := M))
⊢ (HSMul.hSMul (α := CoprodI M) ((CoprodI.of (M := M) : (a : M i) → CoprodI M) m : CoprodI M) w).prod (M := M) =
    HMul.hMul (α := CoprodI M) ((CoprodI.of (M := M) : (a : M i) → CoprodI M) m : CoprodI M) (w.prod (M := M))
have of₁ : HMul.hMul (α := CoprodI M)
    ((CoprodI.of (M := M) : (a : M i) → CoprodI M)
      (Pair.head (M := M)
        (have __src : Pair M i := (equivPair (M := M) i : (a : Word M) → Pair M i) w;
        Pair.mk (M := M)
          (HMul.hMul (β := M i) m (Pair.head (M := M) ((equivPair (M := M) i : (a : Word M) → Pair M i) w) : M i))
          (__src.tail (M := M)) sorry)))
    (prod (M := M)
      (Pair.tail (M := M) (i := i)
        (have __src : Pair M i := (equivPair (M := M) i : (a : Word M) → Pair M i) w;
        Pair.mk (M := M)
          (HMul.hMul (β := M i) m (Pair.head (M := M) ((equivPair (M := M) i : (a : Word M) → Pair M i) w) : M i))
          (__src.tail (M := M)) sorry))) =
  HMul.hMul (α := CoprodI M) ((CoprodI.of (M := M) : (a : M i) → CoprodI M) m : CoprodI M) (w.prod (M := M))
Tactic: rw [of_smul_def, prod_rcons, of.map_mul, mul_assoc, ← prod_rcons, ← equivPair_symm,
      Equiv.symm_apply_apply]
-- Lean 4 proof step from Mathlib.GroupTheory.CoprodI (goal)
Goal:
ι : Type u_1
M : ι → Type u_2
inst : (i : ι) → Monoid (M i)
inst_1 : DecidableEq ι
inst_2 : (i : ι) → DecidableEq (M i)
i : ι
m : M i
w : Word M
of :
  prod (M := M)
      (rcons (M := M) (i := i)
        (have __src : Pair M i := (equivPair (M := M) i : (a : Word M) → Pair M i) w;
        Pair.mk (M := M)
          (HMul.hMul (β := M i) m (Pair.head (M := M) ((equivPair (M := M) i : (a : Word M) → Pair M i) w) : M i))
          (__src.tail (M := M)) ⋯)) =
    HMul.hMul (α := CoprodI M) ((CoprodI.of (M := M) : (a : M i) → CoprodI M) m : CoprodI M) (w.prod (M := M))
of₁ :
  HMul.hMul (α := CoprodI M)
      ((CoprodI.of (M := M) : (a : M i) → CoprodI M)
        (Pair.head (M := M)
          (have __src : Pair M i := (equivPair (M := M) i : (a : Word M) → Pair M i) w;
          Pair.mk (M := M)
            (HMul.hMul (β := M i) m (Pair.head (M := M) ((equivPair (M := M) i : (a : Word M) → Pair M i) w) : M i))
            (__src.tail (M := M)) ⋯)))
      (prod (M := M)
        (Pair.tail (M := M) (i := i)
          (have __src : Pair M i := (equivPair (M := M) i : (a : Word M) → Pair M i) w;
          Pair.mk (M := M)
            (HMul.hMul (β := M i) m (Pair.head (M := M) ((equivPair (M := M) i : (a : Word M) → Pair M i) w) : M i))
            (__src.tail (M := M)) ⋯))) =
    HMul.hMul (α := CoprodI M) ((CoprodI.of (M := M) : (a : M i) → CoprodI M) m : CoprodI M) (w.prod (M := M))
⊢ (HSMul.hSMul (α := CoprodI M) ((CoprodI.of (M := M) : (a : M i) → CoprodI M) m : CoprodI M) w).prod (M := M) =
    HMul.hMul (α := CoprodI M) ((CoprodI.of (M := M) : (a : M i) → CoprodI M) m : CoprodI M) (w.prod (M := M))
have of₂ : HMul.hMul (α := CoprodI M) (β := CoprodI M) ((CoprodI.of (M := M) : (a : M i) → CoprodI M) m : CoprodI M)
      ((CoprodI.of (M := M) : (a : M i) → CoprodI M)
          (Pair.head (M := M) ((equivPair (M := M) i : (a : Word M) → Pair M i) w)) :
        CoprodI M) *
    prod (M := M)
      (Pair.tail (M := M) (i := i)
        (have __src : Pair M i := (equivPair (M := M) i : (a : Word M) → Pair M i) w;
        Pair.mk (M := M)
          (HMul.hMul (β := M i) m (Pair.head (M := M) ((equivPair (M := M) i : (a : Word M) → Pair M i) w) : M i))
          (__src.tail (M := M)) sorry)) =
  HMul.hMul (α := CoprodI M) ((CoprodI.of (M := M) : (a : M i) → CoprodI M) m : CoprodI M) (w.prod (M := M))
Tactic: rw [of_smul_def, prod_rcons, of.map_mul, mul_assoc, ← prod_rcons, ← equivPair_symm,
      Equiv.symm_apply_apply]
-- Lean 4 proof step from Mathlib.GroupTheory.CoprodI (goal)
Goal:
ι : Type u_1
M : ι → Type u_2
inst : (i : ι) → Monoid (M i)
inst_1 : DecidableEq ι
inst_2 : (i : ι) → DecidableEq (M i)
x y : CoprodI M
hx : ∀ (w : Word M), (x • w).prod (M := M) = x * w.prod (M := M)
hy : ∀ (w : Word M), (y • w).prod (M := M) = y * w.prod (M := M)
w : Word M
⊢ ((x * y) • w).prod (M := M) = x * y * w.prod (M := M)
have mul : (x • y • w).prod (M := M) = x * y * w.prod (M := M)
Tactic: rw [mul_smul, hx, hy, mul_assoc]
-- Lean 4 proof step from Mathlib.GroupTheory.CoprodI (goal)
Goal:
ι : Type u_1
M : ι → Type u_2
inst : (i : ι) → Monoid (M i)
inst_1 : DecidableEq ι
inst_2 : (i : ι) → DecidableEq (M i)
x y : CoprodI M
hx : ∀ (w : Word M), (x • w).prod (M := M) = x * w.prod (M := M)
hy : ∀ (w : Word M), (y • w).prod (M := M) = y * w.prod (M := M)
w : Word M
mul : (x • y • w).prod (M := M) = x * y * w.prod (M := M)
⊢ ((x * y) • w).prod (M := M) = x * y * w.prod (M := M)
have mul₁ : x * (y • w).prod (M := M) = x * y * w.prod (M := M)
Tactic: rw [mul_smul, hx, hy, mul_assoc]
-- Lean 4 proof step from Mathlib.GroupTheory.CoprodI (goal)
Goal:
ι : Type u_1
M : ι → Type u_2
inst : (i : ι) → Monoid (M i)
inst_1 : DecidableEq ι
inst_2 : (i : ι) → DecidableEq (M i)
x y : CoprodI M
hx : ∀ (w : Word M), (x • w).prod (M := M) = x * w.prod (M := M)
hy : ∀ (w : Word M), (y • w).prod (M := M) = y * w.prod (M := M)
w : Word M
mul : (x • y • w).prod (M := M) = x * y * w.prod (M := M)
mul₁ : x * (y • w).prod (M := M) = x * y * w.prod (M := M)
⊢ ((x * y) • w).prod (M := M) = x * y * w.prod (M := M)
have mul₂ : x * (y * w.prod (M := M)) = x * y * w.prod (M := M)
Tactic: rw [mul_smul, hx, hy, mul_assoc]
-- Lean 4 proof step from Mathlib.GroupTheory.CoprodI (goal)
Goal:
ι : Type u_1
M : ι → Type u_2
inst : (i : ι) → Monoid (M i)
inst_1 : DecidableEq ι
inst_2 : (i : ι) → DecidableEq (M i)
x y : CoprodI M
hx : ∀ (w : Word M), (x • w).prod (M := M) = x * w.prod (M := M)
hy : ∀ (w : Word M), (y • w).prod (M := M) = y * w.prod (M := M)
w : Word M
mul : (x • y • w).prod (M := M) = x * y * w.prod (M := M)
mul₁ : x * (y • w).prod (M := M) = x * y * w.prod (M := M)
mul₂ : x * (y * w.prod (M := M)) = x * y * w.prod (M := M)
⊢ ((x * y) • w).prod (M := M) = x * y * w.prod (M := M)
have mul₃ : x * (y * w.prod (M := M)) = x * (y * w.prod (M := M))
Tactic: rw [mul_smul, hx, hy, mul_assoc]
-- Lean 4 proof step from Mathlib.GroupTheory.CoprodI (goal)
Goal:
ι : Type u_1
M : ι → Type u_2
inst : (i : ι) → Monoid (M i)
inst_1 : DecidableEq ι
inst_2 : (i : ι) → DecidableEq (M i)
m : CoprodI M
⊢ ∀ (w : Word M), (m • w).prod (M := M) = m * w.prod (M := M)
have one : ∀ (w : Word M), (HSMul.hSMul (α := CoprodI M) 1 w).prod (M := M) = 1 * w.prod (M := M)
Tactic: induction m using CoprodI.induction_on with
  | one =>
    intro
    rw [one_smul, one_mul]
  | of _ =>
    intros
    rw [of_smul_def, prod_rcons, of.map_mul, mul_assoc, ← prod_rcons, ← equivPair_symm,
      Equiv.symm_apply_apply]
  | mul x y hx hy =>
    intro w
    rw [mul_smul, hx, hy, mul_assoc]
Cleared hypotheses: m