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)
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
⊢ 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
have 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
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.GroupTheory.CoprodI (goal)
Goal:
ι : Type u_1
M : ι → Type u_2
inst : (i : ι) → Monoid (M i)
w : Word M
h : w ≠ empty (M := M)
⊢ ∃ (i : ι) (j : ι) (w' : NeWord M i j), w'.toWord (M := M) = w
have suffices : ∃ (i : ι) (j : ι) (w' : NeWord M i j), w'.toWord (M := M).toList (M := M) = w.toList (M := M)
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]
-- Lean 4 proof step from Mathlib.GroupTheory.CoprodI (goal)
Goal:
ι : Type u_1
M : ι → Type u_2
inst : (i : ι) → Monoid (M i)
w : Word M
h : w ≠ empty (M := M)
⊢ ∃ (i : ι) (j : ι) (w' : NeWord M i j), w'.toWord (M := M).toList (M := M) = w.toList (M := M)
have 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)
Tactic: obtain ⟨l, hnot1, hchain⟩ := w
Cleared hypotheses: w, h
-- Lean 4 proof step from Mathlib.GroupTheory.CoprodI (hypothesis)
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)
⊢ ∃ (i : ι) (j : ι) (w' : NeWord M i j),
    w'.toWord (M := M).toList (M := M) = (Word.mk (M := M) (x :: l) hnot1 hchain).toList (M := M)
have hnot1₁ : x.snd (β := fun (i : ι) ↦ M i) ≠ 1 ∧ ∀ x ∈ l, x.snd (β := fun (i : ι) ↦ M i) ≠ 1
Tactic: rw [List.forall_mem_cons] at hnot1
Cleared hypotheses: hchain, h
-- Lean 4 proof step from Mathlib.GroupTheory.CoprodI (goal)
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_1 : ∀ l_1 ∈ x :: l, l_1.snd (β := fun (i : ι) ↦ M i) ≠ 1
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)
h : Word.mk (M := M) (x :: l) 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 :: l) hnot1_1 hchain).toList (M := M)
have cons : ∀
  (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 : ∀ l ∈ [x], l.snd (β := fun (i : ι) ↦ M i) ≠ 1)
  (hnot1_2 :
    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 hchain ≠ empty (M := M)),
  ∃ (i : ι) (j : ι) (w' : NeWord M i j),
    w'.toWord (M := M).toList (M := M) = (Word.mk (M := M) [x] hnot1 hchain).toList (M := M)
Tactic: rcases l with - | ⟨y, l⟩
Cleared hypotheses: l, hi, hnot1_1, hnot1, hchain, h
-- Lean 4 proof step from Mathlib.GroupTheory.CoprodI (goal)
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)
have cons : (singleton (M := M) (x.snd (β := fun (i : ι) ↦ M i)) sorry).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, ?_⟩
-- Lean 4 proof step from Mathlib.GroupTheory.CoprodI (hypothesis)
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)
⊢ ∃ (i : ι) (j : ι) (w' : NeWord M i j),
    w'.toWord (M := M).toList (M := M) = (Word.mk (M := M) (x :: y :: l) hnot1_1 hchain).toList (M := M)
have 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)
Tactic: rw [List.isChain_cons_cons] at hchain
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.GroupTheory.CoprodI (hypothesis)
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) (x :: y :: l) hnot1_1 hchain_1).toList (M := M)
have hi₁ : ∃ (i : ι) (j : ι) (w' : NeWord M i j),
  w'.toWord (M := M).toList (M := M) = (Word.mk (M := M) (y :: l) sorry sorry).toList (M := M)
Tactic: specialize hi hnot1.2 hchain.2 (by rintro ⟨rfl⟩)
Cleared hypotheses: hi
-- Lean 4 proof step from Mathlib.GroupTheory.CoprodI (goal)
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)
⊢ ∃ (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)
have 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)
Tactic: obtain ⟨i, j, w', hw' : w'.toList = y::l⟩ := hi
Cleared hypotheses: hi
-- Lean 4 proof step from Mathlib.GroupTheory.CoprodI (goal)
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
⊢ ∃ (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)
have 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)
Tactic: obtain rfl : y = ⟨i, w'.head⟩ := by simpa [hw'] using w'.toList_head?
Cleared hypotheses: y, hnot1_1, hnot1, hchain_1, hchain, h, hw'
-- Lean 4 proof step from Mathlib.GroupTheory.CoprodI (goal)
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)
have cons : ((singleton (M := M) (x.snd (β := fun (i : ι) ↦ M i)) sorry).append (M := M) sorry 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: refine ⟨x.1, j, append (singleton x.2 hnot1.1) hchain.1 w', ?_⟩
-- Lean 4 proof step from Mathlib.GroupTheory.CoprodI (goal)
Goal:
ι : Type u_1
M : ι → Type u_2
inst : (i : ι) → Monoid (M i)
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)
have nil : ∀ (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: induction l with
  | nil => contradiction
  | cons x l hi =>
    rw [List.forall_mem_cons] at hnot1
    rcases l with - | ⟨y, l⟩
    · refine ⟨x.1, x.1, singleton x.2 hnot1.1, ?_⟩
      simp [toWord]
    · rw [List.isChain_cons_cons] at hchain
      specialize hi hnot1.2 hchain.2 (by rintro ⟨rfl⟩)
      obtain ⟨i, j, w', hw' : w'.toList = y::l⟩ := hi
      obtain rfl : y = ⟨i, w'.head⟩ := by simpa [hw'] using w'.toList_head?
      refine ⟨x.1, j, append (singleton x.2 hnot1.1) hchain.1 w', ?_⟩
      simpa [toWord] using hw'
Cleared hypotheses: l, hnot1, hchain, h
-- Lean 4 proof step from Mathlib.GroupTheory.CoprodI (goal)
Goal:
ι : Type u_1
M : ι → Type u_2
inst : (i : ι) → Monoid (M i)
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)
nil :
  ∀
    (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)
⊢ ∃ (i : ι) (j : ι) (w' : NeWord M i j),
    w'.toWord (M := M).toList (M := M) = (Word.mk (M := M) l hnot1 hchain).toList (M := M)
have cons : ∀ (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)),
  ∃ (i : ι) (j : ι) (w' : NeWord M i j),
    w'.toWord (M := M).toList (M := M) = (Word.mk (M := M) (x :: l) hnot1 hchain).toList (M := M)
Tactic: induction l with
  | nil => contradiction
  | cons x l hi =>
    rw [List.forall_mem_cons] at hnot1
    rcases l with - | ⟨y, l⟩
    · refine ⟨x.1, x.1, singleton x.2 hnot1.1, ?_⟩
      simp [toWord]
    · rw [List.isChain_cons_cons] at hchain
      specialize hi hnot1.2 hchain.2 (by rintro ⟨rfl⟩)
      obtain ⟨i, j, w', hw' : w'.toList = y::l⟩ := hi
      obtain rfl : y = ⟨i, w'.head⟩ := by simpa [hw'] using w'.toList_head?
      refine ⟨x.1, j, append (singleton x.2 hnot1.1) hchain.1 w', ?_⟩
      simpa [toWord] using hw'
Cleared hypotheses: l, hnot1, hchain, h
-- Lean 4 proof step from Mathlib.GroupTheory.CoprodI (goal)
Goal:
ι : Type u_1
M : ι → Type u_2
inst : (i : ι) → Monoid (M i)
i j : ι
x : M i
hnotone : x ≠ 1
w : NeWord M i j
⊢ (replaceHead (M := M) x hnotone w).head (M := M) = x
have singleton : ∀ {i : ι} (x : M i) (a : x ≠ 1) (x_1 : M i) (hnotone : x_1 ≠ 1),
  (replaceHead (M := M) x_1 hnotone (singleton (M := M) x a)).head (M := M) = x_1
Tactic: induction w
Cleared hypotheses: x, hnotone, w
-- Lean 4 proof step from Mathlib.GroupTheory.CoprodI (goal)
Goal:
ι : Type u_1
M : ι → Type u_2
inst : (i : ι) → Monoid (M i)
i j : ι
x : M i
hnotone : x ≠ 1
w : NeWord M i j
singleton :
  ∀ {i : ι} (x : M i) (a : x ≠ 1) (x_1 : M i) (hnotone : x_1 ≠ 1),
    (replaceHead (M := M) x_1 hnotone (NeWord.singleton (M := M) x a)).head (M := M) = x_1
⊢ (replaceHead (M := M) x hnotone w).head (M := M) = x
have append : ∀ {i j k l : ι} (_w₁ : NeWord M i j) (_hne : j ≠ k) (_w₂ : NeWord M k l),
  (∀ (x : M i) (hnotone : x ≠ 1), (replaceHead (M := M) x hnotone _w₁).head (M := M) = x) →
    (∀ (x : M k) (hnotone : x ≠ 1), (replaceHead (M := M) x hnotone _w₂).head (M := M) = x) →
      ∀ (x : M i) (hnotone : x ≠ 1), (replaceHead (M := M) x hnotone (_w₁.append (M := M) _hne _w₂)).head (M := M) = x
Tactic: induction w
Cleared hypotheses: x, hnotone, w
-- Lean 4 proof step from Mathlib.GroupTheory.CoprodI (goal)
Goal:
ι : Type u_1
M : ι → Type u_2
inst : (i : ι) → Monoid (M i)
i j : ι
w : NeWord M i j
x : M i
hnotone : x * w.head (M := M) ≠ 1
⊢ (w.mulHead (M := M) x hnotone).head (M := M) = x * w.head (M := M)
have singleton : ∀ {i : ι} (x : M i) (a : x ≠ 1) (x_1 : M i) (hnotone : x_1 * (singleton (M := M) x a).head (M := M) ≠ 1),
  ((singleton (M := M) x a).mulHead (M := M) x_1 hnotone).head (M := M) = x_1 * (singleton (M := M) x a).head (M := M)
Tactic: induction w
Cleared hypotheses: w, x, hnotone
-- Lean 4 proof step from Mathlib.GroupTheory.CoprodI (goal)
Goal:
ι : Type u_1
M : ι → Type u_2
inst : (i : ι) → Monoid (M i)
i j : ι
w : NeWord M i j
x : M i
hnotone : x * w.head (M := M) ≠ 1
singleton :
  ∀ {i : ι} (x : M i) (a : x ≠ 1) (x_1 : M i) (hnotone : x_1 * (NeWord.singleton (M := M) x a).head (M := M) ≠ 1),
    ((NeWord.singleton (M := M) x a).mulHead (M := M) x_1 hnotone).head (M := M) =
      x_1 * (NeWord.singleton (M := M) x a).head (M := M)
⊢ (w.mulHead (M := M) x hnotone).head (M := M) = x * w.head (M := M)
have append : ∀ {i j k l : ι} (_w₁ : NeWord M i j) (_hne : j ≠ k) (_w₂ : NeWord M k l),
  (∀ (x : M i) (hnotone : x * _w₁.head (M := M) ≠ 1),
      (_w₁.mulHead (M := M) x hnotone).head (M := M) = x * _w₁.head (M := M)) →
    (∀ (x : M k) (hnotone : x * _w₂.head (M := M) ≠ 1),
        (_w₂.mulHead (M := M) x hnotone).head (M := M) = x * _w₂.head (M := M)) →
      ∀ (x : M i) (hnotone : x * (_w₁.append (M := M) _hne _w₂).head (M := M) ≠ 1),
        ((_w₁.append (M := M) _hne _w₂).mulHead (M := M) x hnotone).head (M := M) =
          x * (_w₁.append (M := M) _hne _w₂).head (M := M)
Tactic: induction w
Cleared hypotheses: w, x, hnotone
-- Lean 4 proof step from Mathlib.GroupTheory.CoprodI (hypothesis)
Goal:
ι : Type u_1
M : ι → Type u_2
inst : (i : ι) → Monoid (M i)
i j i_1 j_1 k l : ι
_w₁ : NeWord M i_1 j_1
_hne : j_1 ≠ k
_w₂ : NeWord M k l
w_ih_w₁ :
  ∀ (x : M i_1) (hnotone : x * _w₁.head (M := M) ≠ 1),
    (replaceHead (M := M) (x * _w₁.head (M := M)) hnotone _w₁).prod (M := M) =
      HMul.hMul (α := CoprodI M) ((of (M := M) : (a : M i_1) → CoprodI M) x : CoprodI M) (_w₁.prod (M := M))
w_ih_w₂ :
  ∀ (x : M k) (hnotone : x * _w₂.head (M := M) ≠ 1),
    (replaceHead (M := M) (x * _w₂.head (M := M)) hnotone _w₂).prod (M := M) =
      HMul.hMul (α := CoprodI M) ((of (M := M) : (a : M k) → CoprodI M) x : CoprodI M) (_w₂.prod (M := M))
x : M i_1
hnotone : x * (_w₁.append (M := M) _hne _w₂).head (M := M) ≠ 1
⊢ (replaceHead (M := M) (x * (_w₁.append (M := M) _hne _w₂).head (M := M)) hnotone (_w₁.append (M := M) _hne _w₂)).prod
      (M := M) =
    HMul.hMul (α := CoprodI M) ((of (M := M) : (a : M i_1) → CoprodI M) x : CoprodI M)
      ((_w₁.append (M := M) _hne _w₂).prod (M := M))
have w_ih_w₃ : (replaceHead (M := M) (x * _w₁.head (M := M)) hnotone _w₁).prod (M := M) =
  HMul.hMul (α := CoprodI M) ((of (M := M) : (a : M i_1) → CoprodI M) x : CoprodI M) (_w₁.prod (M := M))
Tactic: specialize w_ih_w₁ _ hnotone
Cleared hypotheses: w_ih_w₁