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 j : ι
m : M i
k : ι
g : M k
tail : Word M
h1 : tail.fstIdx (M := M) ≠ some k
h2 : g ≠ 1
ih :
  Membership.mem (γ := List ((i : ι) × M i))
      (toList (M := M)
        (Pair.tail (M := M) (i := j)
          (↑(consRecOn (M := M) (motive := fun (x : Word M) ↦ { p : Pair M j // rcons (M := M) p = x }) tail
                (Subtype.mk (p := fun (p : Pair M j) ↦ rcons (M := M) p = empty (M := M))
                  (Pair.mk (M := M) 1 (empty (M := M)) ⋯) ⋯)
                fun (j_1 : ι) (m : M j_1) (w : Word M) (h1 : ¬w.fstIdx (M := M) = some j_1) (h2 : ¬m = 1)
                  (x : { p : Pair M j // rcons (M := M) p = w }) ↦
                if ij : j = j_1 then
                  Subtype.mk (p := fun (p : Pair M j) ↦ rcons (M := M) p = cons (M := M) m w h1 h2)
                    (Pair.mk (M := M) (Eq.rec (motive := fun (x : ι) (h : j_1 = x) ↦ M x) m ⋯) w ⋯) ⋯
                else
                  Subtype.mk (p := fun (p : Pair M j) ↦ rcons (M := M) p = cons (M := M) m w h1 h2)
                    (Pair.mk (M := M) 1 (cons (M := M) m w h1 h2) ⋯) ⋯) :
            Pair M j)))
      (Sigma.mk (β := fun (i : ι) ↦ M i) i m) ↔
    Sigma.mk (β := fun (i : ι) ↦ M i) i m ∈ tail.toList (M := M).tail ∨
      ¬i = j ∧ ∃ (h : ¬tail.toList (M := M) = []), tail.toList (M := M).head h = Sigma.mk (β := fun (i : ι) ↦ M i) i m
h : j = k
pos :
  ∀ (g : M j) (h1 : tail.fstIdx (M := M) ≠ some j) (h2 : g ≠ 1),
    Sigma.mk (β := fun (i : ι) ↦ M i) i m ∈
        (↑(Subtype.mk (p := fun (p : Pair M j) ↦ rcons (M := M) p = cons (M := M) g tail h1 h2)
                      (Pair.mk (M := M) (Eq.rec (motive := fun (x : ι) (h : j = x) ↦ M x) g ⋯) tail ⋯) ⋯) :
                  Pair M j).tail
              (M := M).toList
          (M := M) ↔
      Sigma.mk (β := fun (i : ι) ↦ M i) i m ∈ (cons (M := M) g tail h1 h2).toList (M := M).tail ∨
        ¬i = j ∧
          ∃ (h : ¬(cons (M := M) g tail h1 h2).toList (M := M) = []),
            (cons (M := M) g tail h1 h2).toList (M := M).head h = Sigma.mk (β := fun (i : ι) ↦ M i) i m
⊢ Sigma.mk (β := fun (i : ι) ↦ M i) i m ∈
      (↑(Subtype.mk (p := fun (p : Pair M j) ↦ rcons (M := M) p = cons (M := M) g tail h1 h2)
                    (Pair.mk (M := M) (Eq.rec (motive := fun (x : ι) (h : k = x) ↦ M x) g ⋯) tail ⋯) ⋯) :
                Pair M j).tail
            (M := M).toList
        (M := M) ↔
    Sigma.mk (β := fun (i : ι) ↦ M i) i m ∈ (cons (M := M) g tail h1 h2).toList (M := M).tail ∨
      ¬i = j ∧
        ∃ (h : ¬(cons (M := M) g tail h1 h2).toList (M := M) = []),
          (cons (M := M) g tail h1 h2).toList (M := M).head h = Sigma.mk (β := fun (i : ι) ↦ M i) i m

Tactic:
subst k
-- 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
tail : Word M
ih :
  Membership.mem (γ := List ((i : ι) × M i))
      (toList (M := M)
        (Pair.tail (M := M) (i := j)
          (↑(consRecOn (M := M) (motive := fun (x : Word M) ↦ { p : Pair M j // rcons (M := M) p = x }) tail
                (Subtype.mk (p := fun (p : Pair M j) ↦ rcons (M := M) p = empty (M := M))
                  (Pair.mk (M := M) 1 (empty (M := M)) ⋯) ⋯)
                fun (j_1 : ι) (m : M j_1) (w : Word M) (h1 : ¬w.fstIdx (M := M) = some j_1) (h2 : ¬m = 1)
                  (x : { p : Pair M j // rcons (M := M) p = w }) ↦
                if ij : j = j_1 then
                  Subtype.mk (p := fun (p : Pair M j) ↦ rcons (M := M) p = cons (M := M) m w h1 h2)
                    (Pair.mk (M := M) (Eq.rec (motive := fun (x : ι) (h : j_1 = x) ↦ M x) m ⋯) w ⋯) ⋯
                else
                  Subtype.mk (p := fun (p : Pair M j) ↦ rcons (M := M) p = cons (M := M) m w h1 h2)
                    (Pair.mk (M := M) 1 (cons (M := M) m w h1 h2) ⋯) ⋯) :
            Pair M j)))
      (Sigma.mk (β := fun (i : ι) ↦ M i) i m) ↔
    Sigma.mk (β := fun (i : ι) ↦ M i) i m ∈ tail.toList (M := M).tail ∨
      ¬i = j ∧ ∃ (h : ¬tail.toList (M := M) = []), tail.toList (M := M).head h = Sigma.mk (β := fun (i : ι) ↦ M i) i m
g : M j
h1 : tail.fstIdx (M := M) ≠ some j
h2 : g ≠ 1
hij : j = i
⊢ Sigma.mk (β := fun (i : ι) ↦ M i) i m ∈
      (↑(Subtype.mk (p := fun (p : Pair M j) ↦ rcons (M := M) p = cons (M := M) g tail h1 h2)
                    (Pair.mk (M := M) (Eq.rec (motive := fun (x : ι) (h : j = x) ↦ M x) g ⋯) tail ⋯) ⋯) :
                Pair M j).tail
            (M := M).toList
        (M := M) ↔
    Sigma.mk (β := fun (i : ι) ↦ M i) i m ∈ (cons (M := M) g tail h1 h2).toList (M := M).tail ∨
      ¬i = j ∧
        ∃ (h : ¬(cons (M := M) g tail h1 h2).toList (M := M) = []),
          (cons (M := M) g tail h1 h2).toList (M := M).head h = Sigma.mk (β := fun (i : ι) ↦ M i) i m

Tactic:
simp_all
-- 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
tail : Word M
ih :
  Membership.mem (γ := List ((i : ι) × M i))
      (toList (M := M)
        (Pair.tail (M := M) (i := j)
          (↑(consRecOn (M := M) (motive := fun (x : Word M) ↦ { p : Pair M j // rcons (M := M) p = x }) tail
                (Subtype.mk (p := fun (p : Pair M j) ↦ rcons (M := M) p = empty (M := M))
                  (Pair.mk (M := M) 1 (empty (M := M)) ⋯) ⋯)
                fun (j_1 : ι) (m : M j_1) (w : Word M) (h1 : ¬w.fstIdx (M := M) = some j_1) (h2 : ¬m = 1)
                  (x : { p : Pair M j // rcons (M := M) p = w }) ↦
                if ij : j = j_1 then
                  Subtype.mk (p := fun (p : Pair M j) ↦ rcons (M := M) p = cons (M := M) m w h1 h2)
                    (Pair.mk (M := M) (Eq.rec (motive := fun (x : ι) (h : j_1 = x) ↦ M x) m ⋯) w ⋯) ⋯
                else
                  Subtype.mk (p := fun (p : Pair M j) ↦ rcons (M := M) p = cons (M := M) m w h1 h2)
                    (Pair.mk (M := M) 1 (cons (M := M) m w h1 h2) ⋯) ⋯) :
            Pair M j)))
      (Sigma.mk (β := fun (i : ι) ↦ M i) i m) ↔
    Sigma.mk (β := fun (i : ι) ↦ M i) i m ∈ tail.toList (M := M).tail ∨
      ¬i = j ∧ ∃ (h : ¬tail.toList (M := M) = []), tail.toList (M := M).head h = Sigma.mk (β := fun (i : ι) ↦ M i) i m
g : M j
h1 : tail.fstIdx (M := M) ≠ some j
h2 : g ≠ 1
hij : ¬j = i
⊢ Sigma.mk (β := fun (i : ι) ↦ M i) i m ∈
      (↑(Subtype.mk (p := fun (p : Pair M j) ↦ rcons (M := M) p = cons (M := M) g tail h1 h2)
                    (Pair.mk (M := M) (Eq.rec (motive := fun (x : ι) (h : j = x) ↦ M x) g ⋯) tail ⋯) ⋯) :
                Pair M j).tail
            (M := M).toList
        (M := M) ↔
    Sigma.mk (β := fun (i : ι) ↦ M i) i m ∈ (cons (M := M) g tail h1 h2).toList (M := M).tail ∨
      ¬i = j ∧
        ∃ (h : ¬(cons (M := M) g tail h1 h2).toList (M := M) = []),
          (cons (M := M) g tail h1 h2).toList (M := M).head h = Sigma.mk (β := fun (i : ι) ↦ M i) i m

Tactic:
simp_all
-- 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 k : ι
g : M k
tail : Word M
h1 : tail.fstIdx (M := M) ≠ some k
h2 : g ≠ 1
h : ¬j = k
m : M k
ih :
  Membership.mem (γ := List ((i : ι) × M i))
      (toList (M := M)
        (Pair.tail (M := M) (i := j)
          (↑(consRecOn (M := M) (motive := fun (x : Word M) ↦ { p : Pair M j // rcons (M := M) p = x }) tail
                (Subtype.mk (p := fun (p : Pair M j) ↦ rcons (M := M) p = empty (M := M))
                  (Pair.mk (M := M) 1 (empty (M := M)) ⋯) ⋯)
                fun (j_1 : ι) (m : M j_1) (w : Word M) (h1 : ¬w.fstIdx (M := M) = some j_1) (h2 : ¬m = 1)
                  (x : { p : Pair M j // rcons (M := M) p = w }) ↦
                if ij : j = j_1 then
                  Subtype.mk (p := fun (p : Pair M j) ↦ rcons (M := M) p = cons (M := M) m w h1 h2)
                    (Pair.mk (M := M) (Eq.rec (motive := fun (x : ι) (h : j_1 = x) ↦ M x) m ⋯) w ⋯) ⋯
                else
                  Subtype.mk (p := fun (p : Pair M j) ↦ rcons (M := M) p = cons (M := M) m w h1 h2)
                    (Pair.mk (M := M) 1 (cons (M := M) m w h1 h2) ⋯) ⋯) :
            Pair M j)))
      (Sigma.mk (β := fun (i : ι) ↦ M i) k m) ↔
    Sigma.mk (β := fun (i : ι) ↦ M i) k m ∈ tail.toList (M := M).tail ∨
      ¬k = j ∧ ∃ (h : ¬tail.toList (M := M) = []), tail.toList (M := M).head h = Sigma.mk (β := fun (i : ι) ↦ M i) k m
⊢ Sigma.mk (β := fun (i : ι) ↦ M i) k m ∈
      (↑(Subtype.mk (p := fun (p : Pair M j) ↦ rcons (M := M) p = cons (M := M) g tail h1 h2)
                    (Pair.mk (M := M) 1 (cons (M := M) g tail h1 h2) ⋯) ⋯) :
                Pair M j).tail
            (M := M).toList
        (M := M) ↔
    Sigma.mk (β := fun (i : ι) ↦ M i) k m ∈ (cons (M := M) g tail h1 h2).toList (M := M).tail ∨
      ¬k = j ∧
        ∃ (h : ¬(cons (M := M) g tail h1 h2).toList (M := M) = []),
          (cons (M := M) g tail h1 h2).toList (M := M).head h = Sigma.mk (β := fun (i : ι) ↦ M i) k m

Tactic:
simp_all [@eq_comm _ m g, @eq_comm _ k j, or_comm]

Premises used: eq_comm, or_comm
-- 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
k : ι
g : M k
tail : Word M
h1 : tail.fstIdx (M := M) ≠ some k
h2 : g ≠ 1
ih :
  Membership.mem (γ := List ((i : ι) × M i))
      (toList (M := M)
        (Pair.tail (M := M) (i := j)
          (↑(consRecOn (M := M) (motive := fun (x : Word M) ↦ { p : Pair M j // rcons (M := M) p = x }) tail
                (Subtype.mk (p := fun (p : Pair M j) ↦ rcons (M := M) p = empty (M := M))
                  (Pair.mk (M := M) 1 (empty (M := M)) ⋯) ⋯)
                fun (j_1 : ι) (m : M j_1) (w : Word M) (h1 : ¬w.fstIdx (M := M) = some j_1) (h2 : ¬m = 1)
                  (x : { p : Pair M j // rcons (M := M) p = w }) ↦
                if ij : j = j_1 then
                  Subtype.mk (p := fun (p : Pair M j) ↦ rcons (M := M) p = cons (M := M) m w h1 h2)
                    (Pair.mk (M := M) (Eq.rec (motive := fun (x : ι) (h : j_1 = x) ↦ M x) m ⋯) w ⋯) ⋯
                else
                  Subtype.mk (p := fun (p : Pair M j) ↦ rcons (M := M) p = cons (M := M) m w h1 h2)
                    (Pair.mk (M := M) 1 (cons (M := M) m w h1 h2) ⋯) ⋯) :
            Pair M j)))
      (Sigma.mk (β := fun (i : ι) ↦ M i) i m) ↔
    Sigma.mk (β := fun (i : ι) ↦ M i) i m ∈ tail.toList (M := M).tail ∨
      ¬i = j ∧ ∃ (h : ¬tail.toList (M := M) = []), tail.toList (M := M).head h = Sigma.mk (β := fun (i : ι) ↦ M i) i m
h : ¬j = k
hik : ¬i = k
⊢ Sigma.mk (β := fun (i : ι) ↦ M i) i m ∈
      (↑(Subtype.mk (p := fun (p : Pair M j) ↦ rcons (M := M) p = cons (M := M) g tail h1 h2)
                    (Pair.mk (M := M) 1 (cons (M := M) g tail h1 h2) ⋯) ⋯) :
                Pair M j).tail
            (M := M).toList
        (M := M) ↔
    Sigma.mk (β := fun (i : ι) ↦ M i) i m ∈ (cons (M := M) g tail h1 h2).toList (M := M).tail ∨
      ¬i = j ∧
        ∃ (h : ¬(cons (M := M) g tail h1 h2).toList (M := M) = []),
          (cons (M := M) g tail h1 h2).toList (M := M).head h = Sigma.mk (β := fun (i : ι) ↦ M i) i m

Tactic:
simp [hik, Ne.symm hik]

Premises used: Ne.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 j : ι
w : Word M
m : M i
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) →
    Sigma.mk (β := fun (i : ι) ↦ M i) i m ∈ w.toList (M := M)
⊢ Membership.mem (γ := List ((i : ι) × M i))
      (toList (M := M) (Pair.tail (M := M) (i := j) ((equivPair (M := M) j : (a : Word M) → Pair M j) w)) :
        List ((i : ι) × M i))
      (Sigma.mk (β := fun (i : ι) ↦ M i) i m) →
    Sigma.mk (β := fun (i : ι) ↦ M i) i m ∈ w.toList (M := M)

Tactic:
rw [mem_equivPair_tail_iff]

Premises used: Monoid.CoprodI.Word.mem_equivPair_tail_iff
-- 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 : ι
w : Word M
m : M i
h : Sigma.mk (β := fun (i : ι) ↦ M i) i m ∈ w.toList (M := M).tail
⊢ Sigma.mk (β := fun (i : ι) ↦ M i) i m ∈ w.toList (M := M)

Tactic:
List.mem_of_mem_tail h

Premises used: List.mem_of_mem_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)
i j : ι
w : Word M
m : M i
h : Sigma.mk (β := fun (i : ι) ↦ M i) i m ∈ w.toList (M := M).tail
⊢ Sigma.mk (β := fun (i : ι) ↦ M i) i m ∈ w.toList (M := M)

Tactic:
exact List.mem_of_mem_tail h

Premises used: List.mem_of_mem_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)
i j : ι
w : Word M
m : M i
h : i ≠ j ∧ ∃ (h : w.toList (M := M) ≠ []), w.toList (M := M).head h = Sigma.mk (β := fun (i : ι) ↦ M i) i m
inr :
  ∀ (h : i ≠ j ∧ ∃ (h : w.toList (M := M) ≠ []), w.toList (M := M).head h = Sigma.mk (β := fun (i : ι) ↦ M i) i m),
    Sigma.mk (β := fun (i : ι) ↦ M i) i m ∈ w.toList (M := M)
⊢ Sigma.mk (β := fun (i : ι) ↦ M i) i m ∈ w.toList (M := M)

Tactic:
revert 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)
i j : ι
w : Word M
m : M i
inr :
  ∀ (h : i ≠ j ∧ ∃ (h : Ne (α := List ((i : ι) × M i)) [] []), List.head [] h = Sigma.mk (β := fun (i : ι) ↦ M i) i m),
    Membership.mem (γ := List ((i : ι) × M i)) [] (Sigma.mk (β := fun (i : ι) ↦ M i) i m)
inr₁ :
  ∀ (head : (i : ι) × M i) (tail : List ((i : ι) × M i))
    (h : i ≠ j ∧ ∃ (h : head :: tail ≠ []), (head :: tail).head h = Sigma.mk (β := fun (i : ι) ↦ M i) i m),
    Sigma.mk (β := fun (i : ι) ↦ M i) i m ∈ head :: tail
⊢ ∀ (h : i ≠ j ∧ ∃ (h : w.toList (M := M) ≠ []), w.toList (M := M).head h = Sigma.mk (β := fun (i : ι) ↦ M i) i m),
    Sigma.mk (β := fun (i : ι) ↦ M i) i m ∈ w.toList (M := M)

Tactic:
cases w.toList

Premises used: Monoid.CoprodI.Word.toList
-- 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 : ι
w : Word M
m : M i
⊢ ∀ (h : i ≠ j ∧ ∃ (h : Ne (α := List ((i : ι) × M i)) [] []), List.head [] h = Sigma.mk (β := fun (i : ι) ↦ M i) i m),
    Membership.mem (γ := List ((i : ι) × M i)) [] (Sigma.mk (β := fun (i : ι) ↦ M i) i m)

Tactic:
simp +contextual
-- 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 : ι
w : Word M
m : M i
head : (i : ι) × M i
tail : List ((i : ι) × M i)
⊢ ∀ (h : i ≠ j ∧ ∃ (h : head :: tail ≠ []), (head :: tail).head h = Sigma.mk (β := fun (i : ι) ↦ M i) i m),
    Sigma.mk (β := fun (i : ι) ↦ M i) i m ∈ head :: tail

Tactic:
simp +contextual
-- 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
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)) ⋯) ⋯)
                      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 ⋯) w ⋯) ⋯
                      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) ⋯) ⋯) :
                  Pair M i),
              invFun := rcons (M := M), left_inv := ⋯, right_inv := ⋯ } :
            (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)
⊢ 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)

Tactic:
simp only [equivPair, equivPairAux]

Premises used: Monoid.CoprodI.Word.equivPair, _private.0.Monoid.CoprodI.Word.equivPairAux
-- 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 : ι
⊢ 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)) ⋯) ⋯)
                      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 ⋯) w ⋯) ⋯
                      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) ⋯) ⋯) :
                  Pair M i),
              invFun := rcons (M := M), left_inv := ⋯, right_inv := ⋯ } :
            (a : Word M) → Pair M i)
          (empty (M := M))) :
      M i)
    (if h :
          ∃ (h : Ne (α := List ((i : ι) × M i)) (toList (M := M) (empty (M := M))) []),
            (List.head (toList (M := M) (empty (M := M))) h).fst (β := fun (i : ι) ↦ M i) = i then
        Eq.rec (motive :=
          fun (x : ι) (h : (List.head (toList (M := M) (empty (M := M))) ⋯).fst (β := fun (i : ι) ↦ M i) = x) ↦ M x)
          (Sigma.snd (β := fun (i : ι) ↦ M i) (List.head (toList (M := M) (empty (M := M))) ⋯)) ⋯
      else 1 :
      M i)

Tactic:
simp
-- Module: Mathlib.GroupTheory.CoprodI
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
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)) ⋯))
    (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)) ⋯))) :
            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)) ⋯))))
        ⋯))
⊢ (m * m') • w = m • m' • w

Tactic:
dsimp +instances [instHSMul]

Premises used: instHSMul
-- Module: Mathlib.GroupTheory.CoprodI
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
⊢ 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)) ⋯))
    (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)) ⋯))) :
            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)) ⋯))))
        ⋯))

Tactic:
simp [mul_assoc, ← equivPair_symm, Equiv.apply_symm_apply]

Premises used: Equiv.apply_symm_apply, mul_assoc, Monoid.CoprodI.Word.equivPair_symm
-- Module: Mathlib.GroupTheory.CoprodI
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
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)) ⋯)
    ((equivPair (M := M) i : (a : Word M) → Pair M i) w : Pair M i)
⊢ HSMul.hSMul (α := M i) 1 w = w

Tactic:
apply (equivPair i).symm_apply_eq.mpr

Premises used: Iff.mpr, Equiv.symm_apply_eq, Monoid.CoprodI.Word.equivPair
-- Module: Mathlib.GroupTheory.CoprodI
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
⊢ 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)) ⋯)
    ((equivPair (M := M) i : (a : Word M) → Pair M i) w : Pair M i)

Tactic:
simp [equivPair]

Premises used: Monoid.CoprodI.Word.equivPair
-- 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 =
    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: rfl