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)
i : ι
w : Word M
⊢ Eq.{u_2 + 1} (α := M i) (Pair.head (M := M) ((equivPair (M := M) i : (a : Word M) → Pair M i) w) : M i)
    (if h : ∃ (h : w.toList (M := M) ≠ []), (w.toList (M := M).head h).fst (β := fun (i : ι) ↦ M i) = i then
        Eq.rec (motive := fun (x : ι) (h : (w.toList (M := M).head ⋯).fst (β := fun (i : ι) ↦ M i) = x) ↦ M x)
          ((w.toList (M := M).head ⋯).snd (β := fun (i : ι) ↦ M i)) ⋯
      else 1 :
      M i)
have simp : Eq.{u_2 + 1} (α := M i)
  (Pair.head (M := M)
      (({
            toFun := fun (w : Word M) ↦
              (↑(consRecOn (M := M) (motive := fun (x : Word M) ↦ { p : Pair M i // rcons (M := M) p = x }) w
                    (Subtype.mk (p := fun (p : Pair M i) ↦ rcons (M := M) p = empty (M := M))
                      (Pair.mk (M := M) 1 (empty (M := M)) sorry) sorry)
                    fun (j : ι) (m : M j) (w : Word M) (h1 : w.fstIdx (M := M) ≠ some j) (h2 : m ≠ 1)
                      (x : { p : Pair M i // rcons (M := M) p = w }) ↦
                    if ij : i = j then
                      Subtype.mk (p := fun (p : Pair M i) ↦ rcons (M := M) p = cons (M := M) m w h1 h2)
                        (Pair.mk (M := M) (Eq.rec (motive := fun (x : ι) (h : j = x) ↦ M x) m sorry) w sorry) sorry
                    else
                      Subtype.mk (p := fun (p : Pair M i) ↦ rcons (M := M) p = cons (M := M) m w h1 h2)
                        (Pair.mk (M := M) 1 (cons (M := M) m w h1 h2) sorry) sorry) :
                Pair M i),
            invFun := rcons (M := M), left_inv := sorry, right_inv := sorry } :
          (a : Word M) → Pair M i)
        w) :
    M i)
  (if h : ∃ (h : w.toList (M := M) ≠ []), (w.toList (M := M).head h).fst (β := fun (i : ι) ↦ M i) = i then
      Eq.rec (motive := fun (x : ι) (h : (w.toList (M := M).head sorry).fst (β := fun (i : ι) ↦ M i) = x) ↦ M x)
        ((w.toList (M := M).head sorry).snd (β := fun (i : ι) ↦ M i)) sorry
    else 1 :
    M i)
Tactic: simp only [equivPair, equivPairAux]
-- Lean 4 proof step from Mathlib.GroupTheory.CoprodI (goal)
Goal:
ι : Type u_1
M : ι → Type u_2
inst : (i : ι) → Monoid (M i)
N : Type u_3
inst_1 : Monoid N
inst_2 : DecidableEq ι
inst_3 : (i : ι) → DecidableEq (M i)
i : ι
m m' : M i
w : Word M
⊢ (m * m') • w = m • m' • w
have dsimp : Eq (α := Word M)
  (rcons (M := M)
    (Pair.mk (M := M)
      (HMul.hMul (β := M i) (m * m') (Pair.head (M := M) ((equivPair (M := M) i : (a : Word M) → Pair M i) w) : M i))
      (Pair.tail (M := M) (i := i) ((equivPair (M := M) i : (a : Word M) → Pair M i) w)) sorry))
  (rcons (M := M)
    (Pair.mk (M := M)
      (HMul.hMul (β := M i) m
        (Pair.head (M := M)
            ((equivPair (M := M) i : (a : Word M) → Pair M i)
              (rcons (M := M)
                (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))
                  (Pair.tail (M := M) (i := i) ((equivPair (M := M) i : (a : Word M) → Pair M i) w)) sorry))) :
          M i))
      (Pair.tail (M := M) (i := i)
        ((equivPair (M := M) i : (a : Word M) → Pair M i)
          (rcons (M := M)
            (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))
              (Pair.tail (M := M) (i := i) ((equivPair (M := M) i : (a : Word M) → Pair M i) w)) sorry))))
      sorry))
Tactic: dsimp +instances [instHSMul]
-- Lean 4 proof step from Mathlib.GroupTheory.CoprodI (goal)
Goal:
ι : Type u_1
M : ι → Type u_2
inst : (i : ι) → Monoid (M i)
N : Type u_3
inst_1 : Monoid N
inst_2 : DecidableEq ι
inst_3 : (i : ι) → DecidableEq (M i)
i : ι
w : Word M
⊢ HSMul.hSMul (α := M i) 1 w = w
have apply : Eq (α := Pair M i)
  (let __src : Pair M i := (equivPair (M := M) i : (a : Word M) → Pair M i) w;
  Pair.mk (M := M)
    (HMul.hMul (α := M i) (β := M i) (1 : M i)
      (Pair.head (M := M) ((equivPair (M := M) i : (a : Word M) → Pair M i) w) : M i))
    (__src.tail (M := M)) sorry)
  ((equivPair (M := M) i : (a : Word M) → Pair M i) w : Pair M i)
Tactic: apply (equivPair i).symm_apply_eq.mpr
-- 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
⊢ Eq (α := Pair M i)
    ((equivPair (M := M) i : (a : Word M) → Pair M i)
        (HSMul.hSMul (α := CoprodI M) ((of (M := M) : (a : M i) → CoprodI M) m : CoprodI M) w) :
      Pair M i)
    (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))
        (Pair.tail (M := M) (i := i) ((equivPair (M := M) i : (a : Word M) → Pair M i) w)) ⋯ :
      Pair M i)
have rw : Eq (α := Pair M i)
  ((equivPair (M := M) i : (a : Word M) → Pair M i)
      ((Equiv.symm (equivPair (M := M) i) : (a : Pair M i) → Word 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)) :
    Pair M i)
  (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))
      (Pair.tail (M := M) (i := i) ((equivPair (M := M) i : (a : Word M) → Pair M i) w)) sorry :
    Pair M i)
Tactic: rw [of_smul_def, ← equivPair_symm]
-- 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 j : ι
m₁ : M i
m₂ : M j
w : Word M
⊢ Sigma.mk (β := fun (i : ι) ↦ M i) i m₁ ∈
      (HSMul.hSMul (α := CoprodI M) ((of (M := M) : (a : M j) → CoprodI M) m₂ : CoprodI M) w).toList (M := M) ↔
    ¬i = j ∧ Sigma.mk (β := fun (i : ι) ↦ M i) i m₁ ∈ w.toList (M := M) ∨
      m₁ ≠ 1 ∧
        ∃ (hij : i = j),
          Sigma.mk (β := fun (i : ι) ↦ M i) i m₁ ∈ w.toList (M := M).tail ∨
            (∃ (m' : M j),
                Sigma.mk (β := fun (i : ι) ↦ M i) j m' ∈ w.toList (M := M).head? ∧
                  m₁ = Eq.rec (motive := fun (x : ι) (h : j = x) ↦ M x) (m₂ * m') ⋯) ∨
              w.fstIdx (M := M) ≠ some j ∧ m₁ = Eq.rec (motive := fun (x : ι) (h : j = x) ↦ M x) m₂ ⋯
have rw : (Sigma.mk (β := fun (i : ι) ↦ M i) i m₁ ∈ w.toList (M := M).tail ∨
    (i ≠ j ∧ ∃ (h : w.toList (M := M) ≠ []), w.toList (M := M).head h = Sigma.mk (β := fun (i : ι) ↦ M i) i m₁) ∨
      m₁ ≠ 1 ∧
        ∃ (h : j = i),
          m₁ =
            Eq.rec (motive := fun (x : ι) (h : j = x) ↦ M x)
              (Pair.head (M := M)
                (have __src : Pair M j := (equivPair (M := M) j : (a : Word M) → Pair M j) w;
                Pair.mk (M := M)
                  (m₂ *
                    if h :
                        ∃ (h : w.toList (M := M) ≠ []), (w.toList (M := M).head h).fst (β := fun (i : ι) ↦ M i) = j then
                      Eq.rec (motive := fun (x : ι) (h : (w.toList (M := M).head sorry).fst (β := fun (i : ι) ↦ M i) = x) ↦
                        M x) ((w.toList (M := M).head sorry).snd (β := fun (i : ι) ↦ M i)) sorry
                    else 1)
                  (__src.tail (M := M)) sorry))
              h) ↔
  ¬i = j ∧ Sigma.mk (β := fun (i : ι) ↦ M i) i m₁ ∈ w.toList (M := M) ∨
    m₁ ≠ 1 ∧
      ∃ (hij : i = j),
        Sigma.mk (β := fun (i : ι) ↦ M i) i m₁ ∈ w.toList (M := M).tail ∨
          (∃ (m' : M j),
              Sigma.mk (β := fun (i : ι) ↦ M i) j m' ∈ w.toList (M := M).head? ∧
                m₁ = Eq.rec (motive := fun (x : ι) (h : j = x) ↦ M x) (m₂ * m') sorry) ∨
            w.fstIdx (M := M) ≠ some j ∧ m₁ = Eq.rec (motive := fun (x : ι) (h : j = x) ↦ M x) m₂ sorry
Tactic: rw [of_smul_def, mem_rcons_iff, mem_equivPair_tail_iff, equivPair_head, or_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)
j : ι
m₂ : M j
w : Word M
m₁ : M j
⊢ (Sigma.mk (β := fun (i : ι) ↦ M i) j m₁ ∈ w.toList (M := M).tail ∨
      (j ≠ j ∧ ∃ (h : w.toList (M := M) ≠ []), w.toList (M := M).head h = Sigma.mk (β := fun (i : ι) ↦ M i) j m₁) ∨
        m₁ ≠ 1 ∧
          ∃ (h : j = j),
            m₁ =
              Eq.rec (motive := fun (x : ι) (h : j = x) ↦ M x)
                (Pair.head (M := M)
                  (have __src : Pair M j := (equivPair (M := M) j : (a : Word M) → Pair M j) w;
                  Pair.mk (M := M)
                    (m₂ *
                      if h :
                          ∃ (h : w.toList (M := M) ≠ []),
                            (w.toList (M := M).head h).fst (β := fun (i : ι) ↦ M i) = j then
                        Eq.rec (motive :=
                          fun (x : ι) (h : (w.toList (M := M).head ⋯).fst (β := fun (i : ι) ↦ M i) = x) ↦ M x)
                          ((w.toList (M := M).head ⋯).snd (β := fun (i : ι) ↦ M i)) ⋯
                      else 1)
                    (__src.tail (M := M)) ⋯))
                h) ↔
    ¬j = j ∧ Sigma.mk (β := fun (i : ι) ↦ M i) j m₁ ∈ w.toList (M := M) ∨
      m₁ ≠ 1 ∧
        ∃ (hij : j = j),
          Sigma.mk (β := fun (i : ι) ↦ M i) j m₁ ∈ w.toList (M := M).tail ∨
            (∃ (m' : M j),
                Sigma.mk (β := fun (i : ι) ↦ M i) j m' ∈ w.toList (M := M).head? ∧
                  m₁ = Eq.rec (motive := fun (x : ι) (h : j = x) ↦ M x) (m₂ * m') ⋯) ∨
              w.fstIdx (M := M) ≠ some j ∧ m₁ = Eq.rec (motive := fun (x : ι) (h : j = x) ↦ M x) m₂ ⋯
have pos : (Sigma.mk (β := fun (i : ι) ↦ M i) j m₁ ∈ w.toList (M := M).tail ∨
    ¬m₁ = 1 ∧
      m₁ =
        m₂ *
          if h : ∃ (h : ¬w.toList (M := M) = []), (w.toList (M := M).head h).fst (β := fun (i : ι) ↦ M i) = j then
            Eq.rec (motive := fun (x : ι) (h : (w.toList (M := M).head sorry).fst (β := fun (i : ι) ↦ M i) = x) ↦ M x)
              ((w.toList (M := M).head sorry).snd (β := fun (i : ι) ↦ M i)) sorry
          else 1) ↔
  ¬m₁ = 1 ∧
    (Sigma.mk (β := fun (i : ι) ↦ M i) j m₁ ∈ w.toList (M := M).tail ∨
      (∃ (m' : M j), Sigma.mk (β := fun (i : ι) ↦ M i) j m' ∈ w.toList (M := M).head? ∧ m₁ = m₂ * m') ∨
        ¬w.fstIdx (M := M) = some j ∧ m₁ = m₂)
Tactic: simp only [not_true, ne_eq, false_and, exists_prop, true_and, false_or]
-- 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
⊢ (Sigma.mk (β := fun (i : ι) ↦ M i) j m₁ ∈ w.toList (M := M).tail ∨
      ¬m₁ = 1 ∧
        m₁ =
          m₂ *
            if h : ∃ (h : ¬w.toList (M := M) = []), (w.toList (M := M).head h).fst (β := fun (i : ι) ↦ M i) = j then
              Eq.rec (motive := fun (x : ι) (h : (w.toList (M := M).head ⋯).fst (β := fun (i : ι) ↦ M i) = x) ↦ M x)
                ((w.toList (M := M).head ⋯).snd (β := fun (i : ι) ↦ M i)) ⋯
            else 1) ↔
    ¬m₁ = 1 ∧
      (Sigma.mk (β := fun (i : ι) ↦ M i) j m₁ ∈ w.toList (M := M).tail ∨
        (∃ (m' : M j), Sigma.mk (β := fun (i : ι) ↦ M i) j m' ∈ w.toList (M := M).head? ∧ m₁ = m₂ * m') ∨
          ¬w.fstIdx (M := M) = some j ∧ m₁ = m₂)
have pos : ∀ (hw : Sigma.mk (β := fun (i : ι) ↦ M i) j m₁ ∈ w.toList (M := M).tail),
  (Sigma.mk (β := fun (i : ι) ↦ M i) j m₁ ∈ w.toList (M := M).tail ∨
      ¬m₁ = 1 ∧
        m₁ =
          m₂ *
            if h : ∃ (h : ¬w.toList (M := M) = []), (w.toList (M := M).head h).fst (β := fun (i : ι) ↦ M i) = j then
              Eq.rec (motive := fun (x : ι) (h : (w.toList (M := M).head sorry).fst (β := fun (i : ι) ↦ M i) = x) ↦ M x)
                ((w.toList (M := M).head sorry).snd (β := fun (i : ι) ↦ M i)) sorry
            else 1) ↔
    ¬m₁ = 1 ∧
      (Sigma.mk (β := fun (i : ι) ↦ M i) j m₁ ∈ w.toList (M := M).tail ∨
        (∃ (m' : M j), Sigma.mk (β := fun (i : ι) ↦ M i) j m' ∈ w.toList (M := M).head? ∧ m₁ = m₂ * m') ∨
          ¬w.fstIdx (M := M) = some j ∧ m₁ = m₂)
Tactic: by_cases hw : ⟨j, m₁⟩ ∈ w.toList.tail
-- 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
pos :
  ∀ (hw : Sigma.mk (β := fun (i : ι) ↦ M i) j m₁ ∈ w.toList (M := M).tail),
    (Sigma.mk (β := fun (i : ι) ↦ M i) j m₁ ∈ w.toList (M := M).tail ∨
        ¬m₁ = 1 ∧
          m₁ =
            m₂ *
              if h : ∃ (h : ¬w.toList (M := M) = []), (w.toList (M := M).head h).fst (β := fun (i : ι) ↦ M i) = j then
                Eq.rec (motive := fun (x : ι) (h : (w.toList (M := M).head ⋯).fst (β := fun (i : ι) ↦ M i) = x) ↦ M x)
                  ((w.toList (M := M).head ⋯).snd (β := fun (i : ι) ↦ M i)) ⋯
              else 1) ↔
      ¬m₁ = 1 ∧
        (Sigma.mk (β := fun (i : ι) ↦ M i) j m₁ ∈ w.toList (M := M).tail ∨
          (∃ (m' : M j), Sigma.mk (β := fun (i : ι) ↦ M i) j m' ∈ w.toList (M := M).head? ∧ m₁ = m₂ * m') ∨
            ¬w.fstIdx (M := M) = some j ∧ m₁ = m₂)
⊢ (Sigma.mk (β := fun (i : ι) ↦ M i) j m₁ ∈ w.toList (M := M).tail ∨
      ¬m₁ = 1 ∧
        m₁ =
          m₂ *
            if h : ∃ (h : ¬w.toList (M := M) = []), (w.toList (M := M).head h).fst (β := fun (i : ι) ↦ M i) = j then
              Eq.rec (motive := fun (x : ι) (h : (w.toList (M := M).head ⋯).fst (β := fun (i : ι) ↦ M i) = x) ↦ M x)
                ((w.toList (M := M).head ⋯).snd (β := fun (i : ι) ↦ M i)) ⋯
            else 1) ↔
    ¬m₁ = 1 ∧
      (Sigma.mk (β := fun (i : ι) ↦ M i) j m₁ ∈ w.toList (M := M).tail ∨
        (∃ (m' : M j), Sigma.mk (β := fun (i : ι) ↦ M i) j m' ∈ w.toList (M := M).head? ∧ m₁ = m₂ * m') ∨
          ¬w.fstIdx (M := M) = some j ∧ m₁ = m₂)
have neg : ∀ (hw : Sigma.mk (β := fun (i : ι) ↦ M i) j m₁ ∉ w.toList (M := M).tail),
  (Sigma.mk (β := fun (i : ι) ↦ M i) j m₁ ∈ w.toList (M := M).tail ∨
      ¬m₁ = 1 ∧
        m₁ =
          m₂ *
            if h : ∃ (h : ¬w.toList (M := M) = []), (w.toList (M := M).head h).fst (β := fun (i : ι) ↦ M i) = j then
              Eq.rec (motive := fun (x : ι) (h : (w.toList (M := M).head sorry).fst (β := fun (i : ι) ↦ M i) = x) ↦ M x)
                ((w.toList (M := M).head sorry).snd (β := fun (i : ι) ↦ M i)) sorry
            else 1) ↔
    ¬m₁ = 1 ∧
      (Sigma.mk (β := fun (i : ι) ↦ M i) j m₁ ∈ w.toList (M := M).tail ∨
        (∃ (m' : M j), Sigma.mk (β := fun (i : ι) ↦ M i) j m' ∈ w.toList (M := M).head? ∧ m₁ = m₂ * m') ∨
          ¬w.fstIdx (M := M) = some j ∧ m₁ = m₂)
Tactic: by_cases hw : ⟨j, m₁⟩ ∈ w.toList.tail
-- 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
⊢ (Sigma.mk (β := fun (i : ι) ↦ M i) j m₁ ∈ w.toList (M := M).tail ∨
      ¬m₁ = 1 ∧
        m₁ =
          m₂ *
            if h : ∃ (h : ¬w.toList (M := M) = []), (w.toList (M := M).head h).fst (β := fun (i : ι) ↦ M i) = j then
              Eq.rec (motive := fun (x : ι) (h : (w.toList (M := M).head ⋯).fst (β := fun (i : ι) ↦ M i) = x) ↦ M x)
                ((w.toList (M := M).head ⋯).snd (β := fun (i : ι) ↦ M i)) ⋯
            else 1) ↔
    ¬m₁ = 1 ∧
      (Sigma.mk (β := fun (i : ι) ↦ M i) j m₁ ∈ w.toList (M := M).tail ∨
        (∃ (m' : M j), Sigma.mk (β := fun (i : ι) ↦ M i) j m' ∈ w.toList (M := M).head? ∧ m₁ = m₂ * m') ∨
          ¬w.fstIdx (M := M) = some j ∧ m₁ = m₂)
have neg : ¬m₁ = 1 →
  ((m₁ =
      m₂ *
        if h : ∃ (h : ¬w.toList (M := M) = []), (w.toList (M := M).head h).fst (β := fun (i : ι) ↦ M i) = j then
          Eq.rec (motive := fun (x : ι) (h : (w.toList (M := M).head sorry).fst (β := fun (i : ι) ↦ M i) = x) ↦ M x)
            ((w.toList (M := M).head sorry).snd (β := fun (i : ι) ↦ M i)) sorry
        else 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: simp only [hw, false_or, Option.mem_def, and_congr_right_iff]
-- 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
⊢ (m₁ =
      m₂ *
        if h : ∃ (h : ¬w.toList (M := M) = []), (w.toList (M := M).head h).fst (β := fun (i : ι) ↦ M i) = j then
          Eq.rec (motive := fun (x : ι) (h : (w.toList (M := M).head ⋯).fst (β := fun (i : ι) ↦ M i) = x) ↦ M x)
            ((w.toList (M := M).head ⋯).snd (β := fun (i : ι) ↦ M i)) ⋯
        else 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 pos : ∀ (h : ∃ (h : ¬w.toList (M := M) = []), (w.toList (M := M).head h).fst (β := fun (i : ι) ↦ M i) = j),
  m₁ =
      HMul.hMul (β := M j) m₂
        (Eq.rec (motive := fun (x : ι) (h : (w.toList (M := M).head sorry).fst (β := fun (i : ι) ↦ M i) = x) ↦ M x)
            ((w.toList (M := M).head sorry).snd (β := fun (i : ι) ↦ M i)) sorry :
          M j) ↔
    (∃ (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: split_ifs with 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
pos :
  ∀ (h : ∃ (h : ¬w.toList (M := M) = []), (w.toList (M := M).head h).fst (β := fun (i : ι) ↦ M i) = j),
    m₁ =
        HMul.hMul (β := M j) m₂
          (Eq.rec (motive := fun (x : ι) (h : (w.toList (M := M).head ⋯).fst (β := fun (i : ι) ↦ M i) = x) ↦ M x)
              ((w.toList (M := M).head ⋯).snd (β := fun (i : ι) ↦ M i)) ⋯ :
            M j) ↔
      (∃ (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₂
⊢ (m₁ =
      m₂ *
        if h : ∃ (h : ¬w.toList (M := M) = []), (w.toList (M := M).head h).fst (β := fun (i : ι) ↦ M i) = j then
          Eq.rec (motive := fun (x : ι) (h : (w.toList (M := M).head ⋯).fst (β := fun (i : ι) ↦ M i) = x) ↦ M x)
            ((w.toList (M := M).head ⋯).snd (β := fun (i : ι) ↦ M i)) ⋯
        else 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: split_ifs with 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₁ =
      HMul.hMul (β := M j) m₂
        (Eq.rec (motive := fun (x : ι) (h : (w.toList (M := M).head ⋯).fst (β := fun (i : ι) ↦ M i) = x) ↦ M x)
            ((w.toList (M := M).head ⋯).snd (β := fun (i : ι) ↦ M i)) ⋯ :
          M j) ↔
    (∃ (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 pos : ∀ (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),
  m₁ =
      HMul.hMul (β := M ((w.toList (M := M).head hnil).fst (β := fun (i : ι) ↦ M i))) m₂
        (@Eq.rec _ _ (fun (x : ι) (h : (w.toList (M := M).head sorry).fst (β := fun (i : ι) ↦ M i) = x) ↦ M x)
            ((w.toList (M := M).head sorry).snd (β := fun (i : ι) ↦ M i))
            ((w.toList (M := M).head hnil).fst (β := fun (i : ι) ↦ M i)) sorry :
          M ((w.toList (M := M).head hnil).fst (β := fun (i : ι) ↦ M i))) ↔
    (∃ (m' : M ((w.toList (M := M).head hnil).fst (β := fun (i : ι) ↦ M i))),
        w.toList (M := M).head? =
            some (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₂
Tactic: rcases h with ⟨hnil, rfl⟩
Cleared hypotheses: j, m₂, m₁, hw, hm1, 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₂ 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
⊢ m₁ =
      HMul.hMul (β := M ((w.toList (M := M).head hnil).fst (β := fun (i : ι) ↦ M i))) m₂
        (@Eq.rec _ _ (fun (x : ι) (h : (w.toList (M := M).head ⋯).fst (β := fun (i : ι) ↦ M i) = x) ↦ M x)
            ((w.toList (M := M).head ⋯).snd (β := fun (i : ι) ↦ M i))
            ((w.toList (M := M).head hnil).fst (β := fun (i : ι) ↦ M i)) ⋯ :
          M ((w.toList (M := M).head hnil).fst (β := fun (i : ι) ↦ M i))) ↔
    (∃ (m' : M ((w.toList (M := M).head hnil).fst (β := fun (i : ι) ↦ M i))),
        w.toList (M := M).head? =
            some (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 sorry).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₂
Tactic: simp only [List.head?_eq_some_head hnil, Option.some.injEq]
-- 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
⊢ 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 sorry).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₂
Tactic: constructor