awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.CoprodI
Goal:
ι : Type u_1
M : ι → Type u_2
inst : (i : ι) → Monoid (M i)
w_1 : Word M
h_1 : w_1 ≠ empty (M := M)
i j : ι
w : NeWord M i j
h : w.toWord (M := M).toList (M := M) = w_1.toList (M := M)
i_1 : ℕ
a : (i : ι) × M i
toList toList₁ :
  getElem? (valid := fun (as : List ((i : ι) × M i)) (i : ℕ) ↦ i < as.length) (w_1.toList (M := M)) i_1 = some a ↔
    getElem? (valid := fun (as : List ((i : ι) × M i)) (i : ℕ) ↦ i < as.length) (w_1.toList (M := M)) i_1 = some a
⊢ getElem? (valid := fun (as : List ((i : ι) × M i)) (i : ℕ) ↦ i < as.length) (w.toWord (M := M).toList (M := M)) i_1 =
      some a ↔
    getElem? (valid := fun (as : List ((i : ι) × M i)) (i : ℕ) ↦ i < as.length) (w_1.toList (M := M)) i_1 = some a

Tactic:
rw [h]
-- Module: Mathlib.GroupTheory.CoprodI
Goal:
ι : Type u_1
M : ι → Type u_2
inst : (i : ι) → Monoid (M i)
w : Word M
h : w ≠ empty (M := M)
suffices : ∃ (i : ι) (j : ι) (w' : NeWord M i j), w'.toWord (M := M).toList (M := M) = w.toList (M := M)
⊢ ∃ (i : ι) (j : ι) (w' : NeWord M i j), w'.toWord (M := M) = w

Tactic:
suffices ∃ (i j : _) (w' : NeWord M i j), w'.toWord.toList = w.toList by
    rcases this with ⟨i, j, w, h⟩
    refine ⟨i, j, w, ?_⟩
    ext
    rw [h]
-- Module: Mathlib.GroupTheory.CoprodI
Goal:
ι : Type u_1
M : ι → Type u_2
inst : (i : ι) → Monoid (M i)
w : Word M
h : w ≠ empty (M := M)
obtain :
  ∀ (l : List ((i : ι) × M i)) (hnot1 : ∀ l_1 ∈ l, l_1.snd (β := fun (i : ι) ↦ M i) ≠ 1)
    (hchain :
      List.IsChain (fun (l l' : (i : ι) × M i) ↦ l.fst (β := fun (i : ι) ↦ M i) ≠ l'.fst (β := fun (i : ι) ↦ M i)) l)
    (h : Word.mk (M := M) l hnot1 hchain ≠ empty (M := M)),
    ∃ (i : ι) (j : ι) (w' : NeWord M i j),
      w'.toWord (M := M).toList (M := M) = (Word.mk (M := M) l hnot1 hchain).toList (M := M)
⊢ ∃ (i : ι) (j : ι) (w' : NeWord M i j), w'.toWord (M := M).toList (M := M) = w.toList (M := M)

Tactic:
obtain ⟨l, hnot1, hchain⟩ := w
-- Module: Mathlib.GroupTheory.CoprodI
Goal:
ι : Type u_1
M : ι → Type u_2
inst : (i : ι) → Monoid (M i)
hnot1 : ∀ (l : (i : ι) × M i), Membership.mem (γ := List ((i : ι) × M i)) [] l → l.snd (β := fun (i : ι) ↦ M i) ≠ 1
hchain : List.IsChain (fun (l l' : (i : ι) × M i) ↦ l.fst (β := fun (i : ι) ↦ M i) ≠ l'.fst (β := fun (i : ι) ↦ M i)) []
h : Word.mk (M := M) [] hnot1 hchain ≠ empty (M := M)
⊢ ∃ (i : ι) (j : ι) (w' : NeWord M i j),
    w'.toWord (M := M).toList (M := M) = (Word.mk (M := M) [] hnot1 hchain).toList (M := M)

Tactic:
contradiction
-- Module: Mathlib.GroupTheory.CoprodI
Goal:
ι : Type u_1
M : ι → Type u_2
inst : (i : ι) → Monoid (M i)
x : (i : ι) × M i
l : List ((i : ι) × M i)
hi :
  ∀ (hnot1 : ∀ l_1 ∈ l, l_1.snd (β := fun (i : ι) ↦ M i) ≠ 1)
    (hchain :
      List.IsChain (fun (l l' : (i : ι) × M i) ↦ l.fst (β := fun (i : ι) ↦ M i) ≠ l'.fst (β := fun (i : ι) ↦ M i)) l)
    (h : Word.mk (M := M) l hnot1 hchain ≠ empty (M := M)),
    ∃ (i : ι) (j : ι) (w' : NeWord M i j),
      w'.toWord (M := M).toList (M := M) = (Word.mk (M := M) l hnot1 hchain).toList (M := M)
hnot1 : ∀ l_1 ∈ x :: l, l_1.snd (β := fun (i : ι) ↦ M i) ≠ 1
hchain :
  List.IsChain (fun (l l' : (i : ι) × M i) ↦ l.fst (β := fun (i : ι) ↦ M i) ≠ l'.fst (β := fun (i : ι) ↦ M i)) (x :: l)
h : Word.mk (M := M) (x :: l) hnot1 hchain ≠ empty (M := M)
⊢ x.snd (β := fun (i : ι) ↦ M i) ≠ 1 ∧ ∀ x ∈ l, x.snd (β := fun (i : ι) ↦ M i) ≠ 1

Tactic:
rw [List.forall_mem_cons] at hnot1

Premises used: List.forall_mem_cons
-- Module: Mathlib.GroupTheory.CoprodI
Goal:
ι : Type u_1
M : ι → Type u_2
inst : (i : ι) → Monoid (M i)
x : (i : ι) × M i
l : List ((i : ι) × M i)
hi :
  ∀ (hnot1 : ∀ l_1 ∈ l, l_1.snd (β := fun (i : ι) ↦ M i) ≠ 1)
    (hchain :
      List.IsChain (fun (l l' : (i : ι) × M i) ↦ l.fst (β := fun (i : ι) ↦ M i) ≠ l'.fst (β := fun (i : ι) ↦ M i)) l)
    (h : Word.mk (M := M) l hnot1 hchain ≠ empty (M := M)),
    ∃ (i : ι) (j : ι) (w' : NeWord M i j),
      w'.toWord (M := M).toList (M := M) = (Word.mk (M := M) l hnot1 hchain).toList (M := M)
hnot1 : ∀ l_1 ∈ x :: l, l_1.snd (β := fun (i : ι) ↦ M i) ≠ 1
hchain :
  List.IsChain (fun (l l' : (i : ι) × M i) ↦ l.fst (β := fun (i : ι) ↦ M i) ≠ l'.fst (β := fun (i : ι) ↦ M i)) (x :: l)
h : Word.mk (M := M) (x :: l) hnot1 hchain ≠ empty (M := M)
hnot1₁ : x.snd (β := fun (i : ι) ↦ M i) ≠ 1 ∧ ∀ x ∈ l, x.snd (β := fun (i : ι) ↦ M i) ≠ 1
⊢ List.IsChain (fun (l l' : (i : ι) × M i) ↦ l.fst (β := fun (i : ι) ↦ M i) ≠ l'.fst (β := fun (i : ι) ↦ M i)) (x :: l)

Tactic:
rw [List.forall_mem_cons] at hnot1

Premises used: List.forall_mem_cons
-- Module: Mathlib.GroupTheory.CoprodI
Goal:
ι : Type u_1
M : ι → Type u_2
inst : (i : ι) → Monoid (M i)
x : (i : ι) × M i
l : List ((i : ι) × M i)
hi :
  ∀ (hnot1 : ∀ l_1 ∈ l, l_1.snd (β := fun (i : ι) ↦ M i) ≠ 1)
    (hchain :
      List.IsChain (fun (l l' : (i : ι) × M i) ↦ l.fst (β := fun (i : ι) ↦ M i) ≠ l'.fst (β := fun (i : ι) ↦ M i)) l)
    (h : Word.mk (M := M) l hnot1 hchain ≠ empty (M := M)),
    ∃ (i : ι) (j : ι) (w' : NeWord M i j),
      w'.toWord (M := M).toList (M := M) = (Word.mk (M := M) l hnot1 hchain).toList (M := M)
hnot1 : ∀ l_1 ∈ x :: l, l_1.snd (β := fun (i : ι) ↦ M i) ≠ 1
hchain :
  List.IsChain (fun (l l' : (i : ι) × M i) ↦ l.fst (β := fun (i : ι) ↦ M i) ≠ l'.fst (β := fun (i : ι) ↦ M i)) (x :: l)
h : Word.mk (M := M) (x :: l) hnot1 hchain ≠ empty (M := M)
hnot1₁ : x.snd (β := fun (i : ι) ↦ M i) ≠ 1 ∧ ∀ x ∈ l, x.snd (β := fun (i : ι) ↦ M i) ≠ 1
hchain₁ :
  List.IsChain (fun (l l' : (i : ι) × M i) ↦ l.fst (β := fun (i : ι) ↦ M i) ≠ l'.fst (β := fun (i : ι) ↦ M i)) (x :: l)
⊢ Word.mk (M := M) (x :: l) hnot1 hchain₁ ≠ empty (M := M)

Tactic:
rw [List.forall_mem_cons] at hnot1

Premises used: List.forall_mem_cons
-- Module: Mathlib.GroupTheory.CoprodI
Goal:
ι : Type u_1
M : ι → Type u_2
inst : (i : ι) → Monoid (M i)
x : (i : ι) × M i
hi :
  ∀
    (hnot1 :
      ∀ (l : (i : ι) × M i), Membership.mem (γ := List ((i : ι) × M i)) [] l → l.snd (β := fun (i : ι) ↦ M i) ≠ 1)
    (hchain :
      List.IsChain (fun (l l' : (i : ι) × M i) ↦ l.fst (β := fun (i : ι) ↦ M i) ≠ l'.fst (β := fun (i : ι) ↦ M i)) [])
    (h : Word.mk (M := M) [] hnot1 hchain ≠ empty (M := M)),
    ∃ (i : ι) (j : ι) (w' : NeWord M i j),
      w'.toWord (M := M).toList (M := M) = (Word.mk (M := M) [] hnot1 hchain).toList (M := M)
hnot1_1 : ∀ l ∈ [x], l.snd (β := fun (i : ι) ↦ M i) ≠ 1
hnot1 :
  x.snd (β := fun (i : ι) ↦ M i) ≠ 1 ∧
    ∀ (x : (i : ι) × M i), Membership.mem (γ := List ((i : ι) × M i)) [] x → x.snd (β := fun (i : ι) ↦ M i) ≠ 1
hchain :
  List.IsChain (fun (l l' : (i : ι) × M i) ↦ l.fst (β := fun (i : ι) ↦ M i) ≠ l'.fst (β := fun (i : ι) ↦ M i)) [x]
h : Word.mk (M := M) [x] hnot1_1 hchain ≠ empty (M := M)
⊢ ∃ (i : ι) (j : ι) (w' : NeWord M i j),
    w'.toWord (M := M).toList (M := M) = (Word.mk (M := M) [x] hnot1_1 hchain).toList (M := M)

Tactic:
⟨x.1, x.1, singleton x.2 hnot1.1, ?_⟩

Premises used: Monoid.CoprodI.NeWord.singleton, Sigma.fst, And.left, Exists.intro, Sigma.snd
-- Module: Mathlib.GroupTheory.CoprodI
Goal:
ι : Type u_1
M : ι → Type u_2
inst : (i : ι) → Monoid (M i)
x : (i : ι) × M i
hi :
  ∀
    (hnot1 :
      ∀ (l : (i : ι) × M i), Membership.mem (γ := List ((i : ι) × M i)) [] l → l.snd (β := fun (i : ι) ↦ M i) ≠ 1)
    (hchain :
      List.IsChain (fun (l l' : (i : ι) × M i) ↦ l.fst (β := fun (i : ι) ↦ M i) ≠ l'.fst (β := fun (i : ι) ↦ M i)) [])
    (h : Word.mk (M := M) [] hnot1 hchain ≠ empty (M := M)),
    ∃ (i : ι) (j : ι) (w' : NeWord M i j),
      w'.toWord (M := M).toList (M := M) = (Word.mk (M := M) [] hnot1 hchain).toList (M := M)
hnot1_1 : ∀ l ∈ [x], l.snd (β := fun (i : ι) ↦ M i) ≠ 1
hnot1 :
  x.snd (β := fun (i : ι) ↦ M i) ≠ 1 ∧
    ∀ (x : (i : ι) × M i), Membership.mem (γ := List ((i : ι) × M i)) [] x → x.snd (β := fun (i : ι) ↦ M i) ≠ 1
hchain :
  List.IsChain (fun (l l' : (i : ι) × M i) ↦ l.fst (β := fun (i : ι) ↦ M i) ≠ l'.fst (β := fun (i : ι) ↦ M i)) [x]
h : Word.mk (M := M) [x] hnot1_1 hchain ≠ empty (M := M)
cons :
  (singleton (M := M) (x.snd (β := fun (i : ι) ↦ M i)) ⋯).toWord (M := M).toList (M := M) =
    (Word.mk (M := M) [x] hnot1_1 hchain).toList (M := M)
⊢ ∃ (i : ι) (j : ι) (w' : NeWord M i j),
    w'.toWord (M := M).toList (M := M) = (Word.mk (M := M) [x] hnot1_1 hchain).toList (M := M)

Tactic:
refine ⟨x.1, x.1, singleton x.2 hnot1.1, ?_⟩
-- Module: Mathlib.GroupTheory.CoprodI
Goal:
ι : Type u_1
M : ι → Type u_2
inst : (i : ι) → Monoid (M i)
x : (i : ι) × M i
hi :
  ∀
    (hnot1 :
      ∀ (l : (i : ι) × M i), Membership.mem (γ := List ((i : ι) × M i)) [] l → l.snd (β := fun (i : ι) ↦ M i) ≠ 1)
    (hchain :
      List.IsChain (fun (l l' : (i : ι) × M i) ↦ l.fst (β := fun (i : ι) ↦ M i) ≠ l'.fst (β := fun (i : ι) ↦ M i)) [])
    (h : Word.mk (M := M) [] hnot1 hchain ≠ empty (M := M)),
    ∃ (i : ι) (j : ι) (w' : NeWord M i j),
      w'.toWord (M := M).toList (M := M) = (Word.mk (M := M) [] hnot1 hchain).toList (M := M)
hnot1_1 : ∀ l ∈ [x], l.snd (β := fun (i : ι) ↦ M i) ≠ 1
hnot1 :
  x.snd (β := fun (i : ι) ↦ M i) ≠ 1 ∧
    ∀ (x : (i : ι) × M i), Membership.mem (γ := List ((i : ι) × M i)) [] x → x.snd (β := fun (i : ι) ↦ M i) ≠ 1
hchain :
  List.IsChain (fun (l l' : (i : ι) × M i) ↦ l.fst (β := fun (i : ι) ↦ M i) ≠ l'.fst (β := fun (i : ι) ↦ M i)) [x]
h : Word.mk (M := M) [x] hnot1_1 hchain ≠ empty (M := M)
⊢ (singleton (M := M) (x.snd (β := fun (i : ι) ↦ M i)) ⋯).toWord (M := M).toList (M := M) =
    (Word.mk (M := M) [x] hnot1_1 hchain).toList (M := M)

Tactic:
simp [toWord]

Premises used: Monoid.CoprodI.NeWord.toWord
-- Module: Mathlib.GroupTheory.CoprodI
Goal:
ι : Type u_1
M : ι → Type u_2
inst : (i : ι) → Monoid (M i)
x y : (i : ι) × M i
l : List ((i : ι) × M i)
hi :
  ∀ (hnot1 : ∀ l_1 ∈ y :: l, l_1.snd (β := fun (i : ι) ↦ M i) ≠ 1)
    (hchain :
      List.IsChain (fun (l l' : (i : ι) × M i) ↦ l.fst (β := fun (i : ι) ↦ M i) ≠ l'.fst (β := fun (i : ι) ↦ M i))
        (y :: l))
    (h : Word.mk (M := M) (y :: l) hnot1 hchain ≠ empty (M := M)),
    ∃ (i : ι) (j : ι) (w' : NeWord M i j),
      w'.toWord (M := M).toList (M := M) = (Word.mk (M := M) (y :: l) hnot1 hchain).toList (M := M)
hnot1_1 : ∀ l_1 ∈ x :: y :: l, l_1.snd (β := fun (i : ι) ↦ M i) ≠ 1
hnot1 : x.snd (β := fun (i : ι) ↦ M i) ≠ 1 ∧ ∀ x ∈ y :: l, x.snd (β := fun (i : ι) ↦ M i) ≠ 1
hchain :
  List.IsChain (fun (l l' : (i : ι) × M i) ↦ l.fst (β := fun (i : ι) ↦ M i) ≠ l'.fst (β := fun (i : ι) ↦ M i))
    (x :: y :: l)
h : Word.mk (M := M) (x :: y :: l) hnot1_1 hchain ≠ empty (M := M)
⊢ x.fst (β := fun (i : ι) ↦ M i) ≠ y.fst (β := fun (i : ι) ↦ M i) ∧
    List.IsChain (fun (l l' : (i : ι) × M i) ↦ l.fst (β := fun (i : ι) ↦ M i) ≠ l'.fst (β := fun (i : ι) ↦ M i))
      (y :: l)

Tactic:
rw [List.isChain_cons_cons] at hchain

Premises used: List.isChain_cons_cons
-- Module: Mathlib.GroupTheory.CoprodI
Goal:
ι : Type u_1
M : ι → Type u_2
inst : (i : ι) → Monoid (M i)
x y : (i : ι) × M i
l : List ((i : ι) × M i)
hi :
  ∀ (hnot1 : ∀ l_1 ∈ y :: l, l_1.snd (β := fun (i : ι) ↦ M i) ≠ 1)
    (hchain :
      List.IsChain (fun (l l' : (i : ι) × M i) ↦ l.fst (β := fun (i : ι) ↦ M i) ≠ l'.fst (β := fun (i : ι) ↦ M i))
        (y :: l))
    (h : Word.mk (M := M) (y :: l) hnot1 hchain ≠ empty (M := M)),
    ∃ (i : ι) (j : ι) (w' : NeWord M i j),
      w'.toWord (M := M).toList (M := M) = (Word.mk (M := M) (y :: l) hnot1 hchain).toList (M := M)
hnot1_1 : ∀ l_1 ∈ x :: y :: l, l_1.snd (β := fun (i : ι) ↦ M i) ≠ 1
hnot1 : x.snd (β := fun (i : ι) ↦ M i) ≠ 1 ∧ ∀ x ∈ y :: l, x.snd (β := fun (i : ι) ↦ M i) ≠ 1
hchain :
  List.IsChain (fun (l l' : (i : ι) × M i) ↦ l.fst (β := fun (i : ι) ↦ M i) ≠ l'.fst (β := fun (i : ι) ↦ M i))
    (x :: y :: l)
h : Word.mk (M := M) (x :: y :: l) hnot1_1 hchain ≠ empty (M := M)
hchain₁ :
  x.fst (β := fun (i : ι) ↦ M i) ≠ y.fst (β := fun (i : ι) ↦ M i) ∧
    List.IsChain (fun (l l' : (i : ι) × M i) ↦ l.fst (β := fun (i : ι) ↦ M i) ≠ l'.fst (β := fun (i : ι) ↦ M i))
      (y :: l)
⊢ Word.mk (M := M) (x :: y :: l) hnot1_1 hchain ≠ empty (M := M)

Tactic:
rw [List.isChain_cons_cons] at hchain

Premises used: List.isChain_cons_cons
-- Module: Mathlib.GroupTheory.CoprodI
Goal:
ι : Type u_1
M : ι → Type u_2
inst : (i : ι) → Monoid (M i)
x y : (i : ι) × M i
l : List ((i : ι) × M i)
hi :
  ∀ (hnot1 : ∀ l_1 ∈ y :: l, l_1.snd (β := fun (i : ι) ↦ M i) ≠ 1)
    (hchain :
      List.IsChain (fun (l l' : (i : ι) × M i) ↦ l.fst (β := fun (i : ι) ↦ M i) ≠ l'.fst (β := fun (i : ι) ↦ M i))
        (y :: l))
    (h : Word.mk (M := M) (y :: l) hnot1 hchain ≠ empty (M := M)),
    ∃ (i : ι) (j : ι) (w' : NeWord M i j),
      w'.toWord (M := M).toList (M := M) = (Word.mk (M := M) (y :: l) hnot1 hchain).toList (M := M)
hnot1_1 : ∀ l_1 ∈ x :: y :: l, l_1.snd (β := fun (i : ι) ↦ M i) ≠ 1
hnot1 : x.snd (β := fun (i : ι) ↦ M i) ≠ 1 ∧ ∀ x ∈ y :: l, x.snd (β := fun (i : ι) ↦ M i) ≠ 1
hchain_1 :
  List.IsChain (fun (l l' : (i : ι) × M i) ↦ l.fst (β := fun (i : ι) ↦ M i) ≠ l'.fst (β := fun (i : ι) ↦ M i))
    (x :: y :: l)
hchain :
  x.fst (β := fun (i : ι) ↦ M i) ≠ y.fst (β := fun (i : ι) ↦ M i) ∧
    List.IsChain (fun (l l' : (i : ι) × M i) ↦ l.fst (β := fun (i : ι) ↦ M i) ≠ l'.fst (β := fun (i : ι) ↦ M i))
      (y :: l)
h : Word.mk (M := M) (x :: y :: l) hnot1_1 hchain_1 ≠ empty (M := M)
⊢ ∃ (i : ι) (j : ι) (w' : NeWord M i j),
    w'.toWord (M := M).toList (M := M) = (Word.mk (M := M) (y :: l) ⋯ ⋯).toList (M := M)

Tactic:
specialize hi hnot1.2 hchain.2 (by rintro ⟨rfl⟩)

Premises used: And.right
-- Module: Mathlib.GroupTheory.CoprodI
Goal:
ι : Type u_1
M : ι → Type u_2
inst : (i : ι) → Monoid (M i)
x y : (i : ι) × M i
l : List ((i : ι) × M i)
hnot1_1 : ∀ l_1 ∈ x :: y :: l, l_1.snd (β := fun (i : ι) ↦ M i) ≠ 1
hnot1 : x.snd (β := fun (i : ι) ↦ M i) ≠ 1 ∧ ∀ x ∈ y :: l, x.snd (β := fun (i : ι) ↦ M i) ≠ 1
hchain_1 :
  List.IsChain (fun (l l' : (i : ι) × M i) ↦ l.fst (β := fun (i : ι) ↦ M i) ≠ l'.fst (β := fun (i : ι) ↦ M i))
    (x :: y :: l)
hchain :
  x.fst (β := fun (i : ι) ↦ M i) ≠ y.fst (β := fun (i : ι) ↦ M i) ∧
    List.IsChain (fun (l l' : (i : ι) × M i) ↦ l.fst (β := fun (i : ι) ↦ M i) ≠ l'.fst (β := fun (i : ι) ↦ M i))
      (y :: l)
h : Word.mk (M := M) (x :: y :: l) hnot1_1 hchain_1 ≠ empty (M := M)
hi :
  ∃ (i : ι) (j : ι) (w' : NeWord M i j),
    w'.toWord (M := M).toList (M := M) = (Word.mk (M := M) (y :: l) ⋯ ⋯).toList (M := M)
cons :
  ∀ (i j : ι) (w' : NeWord M i j) (hw' : w'.toList (M := M) = y :: l),
    ∃ (i : ι) (j : ι) (w' : NeWord M i j),
      w'.toWord (M := M).toList (M := M) = (Word.mk (M := M) (x :: y :: l) hnot1_1 hchain_1).toList (M := M)
⊢ ∃ (i : ι) (j : ι) (w' : NeWord M i j),
    w'.toWord (M := M).toList (M := M) = (Word.mk (M := M) (x :: y :: l) hnot1_1 hchain_1).toList (M := M)

Tactic:
obtain ⟨i, j, w', hw' : w'.toList = y::l⟩ := hi
-- Module: Mathlib.GroupTheory.CoprodI
Goal:
ι : Type u_1
M : ι → Type u_2
inst : (i : ι) → Monoid (M i)
x y : (i : ι) × M i
l : List ((i : ι) × M i)
hnot1_1 : ∀ l_1 ∈ x :: y :: l, l_1.snd (β := fun (i : ι) ↦ M i) ≠ 1
hnot1 : x.snd (β := fun (i : ι) ↦ M i) ≠ 1 ∧ ∀ x ∈ y :: l, x.snd (β := fun (i : ι) ↦ M i) ≠ 1
hchain_1 :
  List.IsChain (fun (l l' : (i : ι) × M i) ↦ l.fst (β := fun (i : ι) ↦ M i) ≠ l'.fst (β := fun (i : ι) ↦ M i))
    (x :: y :: l)
hchain :
  x.fst (β := fun (i : ι) ↦ M i) ≠ y.fst (β := fun (i : ι) ↦ M i) ∧
    List.IsChain (fun (l l' : (i : ι) × M i) ↦ l.fst (β := fun (i : ι) ↦ M i) ≠ l'.fst (β := fun (i : ι) ↦ M i))
      (y :: l)
h : Word.mk (M := M) (x :: y :: l) hnot1_1 hchain_1 ≠ empty (M := M)
i j : ι
w' : NeWord M i j
hw' : w'.toList (M := M) = y :: l
⊢ y = Sigma.mk (β := fun (i : ι) ↦ M i) i (w'.head (M := M))

Tactic:
simpa [hw'] using w'.toList_head?

Premises used: Monoid.CoprodI.NeWord.toList_head?
-- Module: Mathlib.GroupTheory.CoprodI
Goal:
ι : Type u_1
M : ι → Type u_2
inst : (i : ι) → Monoid (M i)
x y : (i : ι) × M i
l : List ((i : ι) × M i)
hnot1_1 : ∀ l_1 ∈ x :: y :: l, l_1.snd (β := fun (i : ι) ↦ M i) ≠ 1
hnot1 : x.snd (β := fun (i : ι) ↦ M i) ≠ 1 ∧ ∀ x ∈ y :: l, x.snd (β := fun (i : ι) ↦ M i) ≠ 1
hchain_1 :
  List.IsChain (fun (l l' : (i : ι) × M i) ↦ l.fst (β := fun (i : ι) ↦ M i) ≠ l'.fst (β := fun (i : ι) ↦ M i))
    (x :: y :: l)
hchain :
  x.fst (β := fun (i : ι) ↦ M i) ≠ y.fst (β := fun (i : ι) ↦ M i) ∧
    List.IsChain (fun (l l' : (i : ι) × M i) ↦ l.fst (β := fun (i : ι) ↦ M i) ≠ l'.fst (β := fun (i : ι) ↦ M i))
      (y :: l)
h : Word.mk (M := M) (x :: y :: l) hnot1_1 hchain_1 ≠ empty (M := M)
i j : ι
w' : NeWord M i j
hw' : w'.toList (M := M) = y :: l
cons :
  ∀
    (hnot1 :
      ∀ l_1 ∈ x :: Sigma.mk (β := fun (i : ι) ↦ M i) i (w'.head (M := M)) :: l, l_1.snd (β := fun (i : ι) ↦ M i) ≠ 1)
    (hnot1_2 :
      x.snd (β := fun (i : ι) ↦ M i) ≠ 1 ∧
        ∀ x ∈ Sigma.mk (β := fun (i : ι) ↦ M i) i (w'.head (M := M)) :: l, x.snd (β := fun (i : ι) ↦ M i) ≠ 1)
    (hchain :
      List.IsChain (fun (l l' : (i : ι) × M i) ↦ l.fst (β := fun (i : ι) ↦ M i) ≠ l'.fst (β := fun (i : ι) ↦ M i))
        (x :: Sigma.mk (β := fun (i : ι) ↦ M i) i (w'.head (M := M)) :: l))
    (hchain_2 :
      x.fst (β := fun (i : ι) ↦ M i) ≠
          (Sigma.mk (β := fun (i : ι) ↦ M i) i (w'.head (M := M))).fst (β := fun (i : ι) ↦ M i) ∧
        List.IsChain (fun (l l' : (i : ι) × M i) ↦ l.fst (β := fun (i : ι) ↦ M i) ≠ l'.fst (β := fun (i : ι) ↦ M i))
          (Sigma.mk (β := fun (i : ι) ↦ M i) i (w'.head (M := M)) :: l))
    (h :
      Word.mk (M := M) (x :: Sigma.mk (β := fun (i : ι) ↦ M i) i (w'.head (M := M)) :: l) hnot1 hchain ≠ empty (M := M))
    (hw' : w'.toList (M := M) = Sigma.mk (β := fun (i : ι) ↦ M i) i (w'.head (M := M)) :: l),
    ∃ (i_1 : ι) (j_1 : ι) (w'_1 : NeWord M i_1 j_1),
      w'_1.toWord (M := M).toList (M := M) =
        (Word.mk (M := M) (x :: Sigma.mk (β := fun (i : ι) ↦ M i) i (w'.head (M := M)) :: l) hnot1 hchain).toList (M :=
          M)
⊢ ∃ (i : ι) (j : ι) (w' : NeWord M i j),
    w'.toWord (M := M).toList (M := M) = (Word.mk (M := M) (x :: y :: l) hnot1_1 hchain_1).toList (M := M)

Tactic:
obtain rfl : y = ⟨i, w'.head⟩ := by simpa [hw'] using w'.toList_head?

Premises used: rfl
-- Module: Mathlib.GroupTheory.CoprodI
Goal:
ι : Type u_1
M : ι → Type u_2
inst : (i : ι) → Monoid (M i)
x : (i : ι) × M i
l : List ((i : ι) × M i)
i j : ι
w' : NeWord M i j
hnot1_1 : ∀ l_1 ∈ x :: Sigma.mk (β := fun (i : ι) ↦ M i) i (w'.head (M := M)) :: l, l_1.snd (β := fun (i : ι) ↦ M i) ≠ 1
hnot1 :
  x.snd (β := fun (i : ι) ↦ M i) ≠ 1 ∧
    ∀ x ∈ Sigma.mk (β := fun (i : ι) ↦ M i) i (w'.head (M := M)) :: l, x.snd (β := fun (i : ι) ↦ M i) ≠ 1
hchain_1 :
  List.IsChain (fun (l l' : (i : ι) × M i) ↦ l.fst (β := fun (i : ι) ↦ M i) ≠ l'.fst (β := fun (i : ι) ↦ M i))
    (x :: Sigma.mk (β := fun (i : ι) ↦ M i) i (w'.head (M := M)) :: l)
hchain :
  x.fst (β := fun (i : ι) ↦ M i) ≠
      (Sigma.mk (β := fun (i : ι) ↦ M i) i (w'.head (M := M))).fst (β := fun (i : ι) ↦ M i) ∧
    List.IsChain (fun (l l' : (i : ι) × M i) ↦ l.fst (β := fun (i : ι) ↦ M i) ≠ l'.fst (β := fun (i : ι) ↦ M i))
      (Sigma.mk (β := fun (i : ι) ↦ M i) i (w'.head (M := M)) :: l)
h :
  Word.mk (M := M) (x :: Sigma.mk (β := fun (i : ι) ↦ M i) i (w'.head (M := M)) :: l) hnot1_1 hchain_1 ≠ empty (M := M)
hw' : w'.toList (M := M) = Sigma.mk (β := fun (i : ι) ↦ M i) i (w'.head (M := M)) :: l
⊢ ∃ (i_1 : ι) (j_1 : ι) (w'_1 : NeWord M i_1 j_1),
    w'_1.toWord (M := M).toList (M := M) =
      (Word.mk (M := M) (x :: Sigma.mk (β := fun (i : ι) ↦ M i) i (w'.head (M := M)) :: l) hnot1_1 hchain_1).toList
        (M := M)

Tactic:
⟨x.1, j, append (singleton x.2 hnot1.1) hchain.1 w', ?_⟩

Premises used: Monoid.CoprodI.NeWord.singleton, Sigma.fst, Monoid.CoprodI.NeWord.append, And.left, Exists.intro, Sigma.snd
-- Module: Mathlib.GroupTheory.CoprodI
Goal:
ι : Type u_1
M : ι → Type u_2
inst : (i : ι) → Monoid (M i)
x : (i : ι) × M i
l : List ((i : ι) × M i)
i j : ι
w' : NeWord M i j
hnot1_1 : ∀ l_1 ∈ x :: Sigma.mk (β := fun (i : ι) ↦ M i) i (w'.head (M := M)) :: l, l_1.snd (β := fun (i : ι) ↦ M i) ≠ 1
hnot1 :
  x.snd (β := fun (i : ι) ↦ M i) ≠ 1 ∧
    ∀ x ∈ Sigma.mk (β := fun (i : ι) ↦ M i) i (w'.head (M := M)) :: l, x.snd (β := fun (i : ι) ↦ M i) ≠ 1
hchain_1 :
  List.IsChain (fun (l l' : (i : ι) × M i) ↦ l.fst (β := fun (i : ι) ↦ M i) ≠ l'.fst (β := fun (i : ι) ↦ M i))
    (x :: Sigma.mk (β := fun (i : ι) ↦ M i) i (w'.head (M := M)) :: l)
hchain :
  x.fst (β := fun (i : ι) ↦ M i) ≠
      (Sigma.mk (β := fun (i : ι) ↦ M i) i (w'.head (M := M))).fst (β := fun (i : ι) ↦ M i) ∧
    List.IsChain (fun (l l' : (i : ι) × M i) ↦ l.fst (β := fun (i : ι) ↦ M i) ≠ l'.fst (β := fun (i : ι) ↦ M i))
      (Sigma.mk (β := fun (i : ι) ↦ M i) i (w'.head (M := M)) :: l)
h :
  Word.mk (M := M) (x :: Sigma.mk (β := fun (i : ι) ↦ M i) i (w'.head (M := M)) :: l) hnot1_1 hchain_1 ≠ empty (M := M)
hw' : w'.toList (M := M) = Sigma.mk (β := fun (i : ι) ↦ M i) i (w'.head (M := M)) :: l
cons :
  ((singleton (M := M) (x.snd (β := fun (i : ι) ↦ M i)) ⋯).append (M := M) ⋯ w').toWord (M := M).toList (M := M) =
    (Word.mk (M := M) (x :: Sigma.mk (β := fun (i : ι) ↦ M i) i (w'.head (M := M)) :: l) hnot1_1 hchain_1).toList (M :=
      M)
⊢ ∃ (i_1 : ι) (j_1 : ι) (w'_1 : NeWord M i_1 j_1),
    w'_1.toWord (M := M).toList (M := M) =
      (Word.mk (M := M) (x :: Sigma.mk (β := fun (i : ι) ↦ M i) i (w'.head (M := M)) :: l) hnot1_1 hchain_1).toList
        (M := M)

Tactic:
refine ⟨x.1, j, append (singleton x.2 hnot1.1) hchain.1 w', ?_⟩
-- Module: Mathlib.GroupTheory.CoprodI
Goal:
ι : Type u_1
M : ι → Type u_2
inst : (i : ι) → Monoid (M i)
x : (i : ι) × M i
l : List ((i : ι) × M i)
i j : ι
w' : NeWord M i j
hnot1_1 : ∀ l_1 ∈ x :: Sigma.mk (β := fun (i : ι) ↦ M i) i (w'.head (M := M)) :: l, l_1.snd (β := fun (i : ι) ↦ M i) ≠ 1
hnot1 :
  x.snd (β := fun (i : ι) ↦ M i) ≠ 1 ∧
    ∀ x ∈ Sigma.mk (β := fun (i : ι) ↦ M i) i (w'.head (M := M)) :: l, x.snd (β := fun (i : ι) ↦ M i) ≠ 1
hchain_1 :
  List.IsChain (fun (l l' : (i : ι) × M i) ↦ l.fst (β := fun (i : ι) ↦ M i) ≠ l'.fst (β := fun (i : ι) ↦ M i))
    (x :: Sigma.mk (β := fun (i : ι) ↦ M i) i (w'.head (M := M)) :: l)
hchain :
  x.fst (β := fun (i : ι) ↦ M i) ≠
      (Sigma.mk (β := fun (i : ι) ↦ M i) i (w'.head (M := M))).fst (β := fun (i : ι) ↦ M i) ∧
    List.IsChain (fun (l l' : (i : ι) × M i) ↦ l.fst (β := fun (i : ι) ↦ M i) ≠ l'.fst (β := fun (i : ι) ↦ M i))
      (Sigma.mk (β := fun (i : ι) ↦ M i) i (w'.head (M := M)) :: l)
h :
  Word.mk (M := M) (x :: Sigma.mk (β := fun (i : ι) ↦ M i) i (w'.head (M := M)) :: l) hnot1_1 hchain_1 ≠ empty (M := M)
hw' : w'.toList (M := M) = Sigma.mk (β := fun (i : ι) ↦ M i) i (w'.head (M := M)) :: l
⊢ ((singleton (M := M) (x.snd (β := fun (i : ι) ↦ M i)) ⋯).append (M := M) ⋯ w').toWord (M := M).toList (M := M) =
    (Word.mk (M := M) (x :: Sigma.mk (β := fun (i : ι) ↦ M i) i (w'.head (M := M)) :: l) hnot1_1 hchain_1).toList (M :=
      M)

Tactic:
simpa [toWord] using hw'

Premises used: Monoid.CoprodI.NeWord.toWord