awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.CoprodI
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
m : M i
⊢ HSMul.hSMul (α := CoprodI M) ((of (M := M) : (a : M i) → CoprodI M) m : CoprodI M) w =
    rcons (M := M) (i := 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 (Pair.head (M := M) ((equivPair (M := M) i : (a : Word M) → Pair M i) w) : M i))
        (__src.tail (M := M)) ⋯)

Tactic:
rfl

Premises used: FreeMonoid.prodAux, Quotient.liftOn', List.foldl, dite, SMul.comp.smul, Con.liftOn, Monoid.CoprodI.Word.rcons, rfl
-- Module: Mathlib.GroupTheory.CoprodI
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
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)) ⋯)) :
      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)
⊢ 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)

Tactic:
rw [of_smul_def, ← equivPair_symm]

Premises used: Monoid.CoprodI.Word.of_smul_def, Monoid.CoprodI.Word.equivPair_symm
-- Module: Mathlib.GroupTheory.CoprodI
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)
        ((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)) ⋯)) :
      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)

Tactic:
simp
-- Module: Mathlib.GroupTheory.CoprodI
Goal:
ι : Type u_1
M : ι → Type u_2
inst : (i : ι) → Monoid (M i)
inst_1 : DecidableEq ι
inst_2 : (i : ι) → DecidableEq (M i)
i : ι
p : Pair M i
⊢ (equivPair (M := M) i : (a : Word M) → Pair M i) (p.tail (M := M)) = Pair.mk (M := M) 1 (p.tail (M := M)) ⋯

Tactic:
equivPair_eq_of_fstIdx_ne _

Premises used: Monoid.CoprodI.Word.equivPair_eq_of_fstIdx_ne
-- Module: Mathlib.GroupTheory.CoprodI
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
⊢ m • w = HSMul.hSMul (α := CoprodI M) ((of (M := M) : (a : M i) → CoprodI M) m : CoprodI M) w

Tactic:
rfl

Premises used: FreeMonoid.prodAux, Quotient.liftOn', List.foldl, dite, SMul.comp.smul, Con.liftOn, Monoid.CoprodI.Word.rcons, rfl
-- Module: Mathlib.GroupTheory.CoprodI
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
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 ⋯).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) ↔
    ¬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₂ ⋯
⊢ 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₂ ⋯

Tactic:
rw [of_smul_def, mem_rcons_iff, mem_equivPair_tail_iff, equivPair_head, or_assoc]

Premises used: Monoid.CoprodI.Word.of_smul_def, Monoid.CoprodI.Word.mem_equivPair_tail_iff, Monoid.CoprodI.Word.mem_rcons_iff, Monoid.CoprodI.Word.equivPair_head, or_assoc
-- Module: Mathlib.GroupTheory.CoprodI
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 :
  (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 ∨
      (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₂ ⋯

Tactic:
simp only [not_true, ne_eq, false_and, exists_prop, true_and, false_or]

Premises used: false_and, false_or, exists_prop, ne_eq, not_true, true_and
-- Module: Mathlib.GroupTheory.CoprodI
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₂)
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 ⋯).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₂)

Tactic:
by_cases hw : ⟨j, m₁⟩ ∈ w.toList.tail

Premises used: Monoid.CoprodI.Word.toList, List.tail
-- Module: Mathlib.GroupTheory.CoprodI
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₂)

Tactic:
simp [hw, show m₁ ≠ 1 from w.ne_one _ (List.mem_of_mem_tail hw)]

Premises used: List.mem_of_mem_tail, Monoid.CoprodI.Word.ne_one, Sigma.mk
-- Module: Mathlib.GroupTheory.CoprodI
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
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 ⋯).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₂)
⊢ (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₂)

Tactic:
simp only [hw, false_or, Option.mem_def, and_congr_right_iff]

Premises used: and_congr_right_iff, false_or, Option.mem_def
-- Module: Mathlib.GroupTheory.CoprodI
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₂
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₂
⊢ (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₂

Tactic:
split_ifs with h
-- Module: Mathlib.GroupTheory.CoprodI
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
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 ⋯).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₂
⊢ 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₂

Tactic:
rcases h with ⟨hnil, rfl⟩

Premises used: rfl
-- Module: Mathlib.GroupTheory.CoprodI
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₁ =
      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₂

Tactic:
simp only [List.head?_eq_some_head hnil, Option.some.injEq]

Premises used: List.head?_eq_some_head, Option.some.injEq
-- Module: Mathlib.GroupTheory.CoprodI
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₂
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 ⋯).snd (β := fun (i : ι) ↦ M i)
⊢ 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₂

Tactic:
constructor
-- Module: Mathlib.GroupTheory.CoprodI
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 ((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).head ⋯).snd (β := fun (i : ι) ↦ M i)) ∉
    w.toList (M := M).tail
hm1 : ¬m₂ * (w.toList (M := M).head ⋯).snd (β := fun (i : ι) ↦ M i) = 1
⊢ (∃ (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₂ * (w.toList (M := M).head ⋯).snd (β := fun (i : ι) ↦ M i) = m₂ * m') ∨
    ¬w.fstIdx (M := M) = some ((w.toList (M := M).head hnil).fst (β := fun (i : ι) ↦ M i)) ∧
      m₂ * (w.toList (M := M).head ⋯).snd (β := fun (i : ι) ↦ M i) = m₂

Tactic:
Or.inl ⟨_, rfl, rfl⟩

Premises used: And.intro, Exists.intro, Or.inl, rfl
-- Module: Mathlib.GroupTheory.CoprodI
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 ((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).head ⋯).snd (β := fun (i : ι) ↦ M i)) ∉
    w.toList (M := M).tail
hm1 : ¬m₂ * (w.toList (M := M).head ⋯).snd (β := fun (i : ι) ↦ M i) = 1
⊢ (∃ (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₂ * (w.toList (M := M).head ⋯).snd (β := fun (i : ι) ↦ M i) = m₂ * m') ∨
    ¬w.fstIdx (M := M) = some ((w.toList (M := M).head hnil).fst (β := fun (i : ι) ↦ M i)) ∧
      m₂ * (w.toList (M := M).head ⋯).snd (β := fun (i : ι) ↦ M i) = m₂

Tactic:
exact Or.inl ⟨_, rfl, rfl⟩

Premises used: Or.inl
-- Module: Mathlib.GroupTheory.CoprodI
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
⊢ (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

Premises used: heq_eq_eq, Sigma.ext_iff, true_and