awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.GroupTheory.CoprodI (goal)
Goal:
ι : Type u_1
M : ι → Type u_2
inst : (i : ι) → Monoid (M i)
inst_1 : DecidableEq ι
inst_2 : (i : ι) → DecidableEq (M i)
m : CoprodI M
one : ∀ (w : Word M), (HSMul.hSMul (α := CoprodI M) 1 w).prod (M := M) = 1 * w.prod (M := M)
⊢ ∀ (w : Word M), (m • w).prod (M := M) = m * w.prod (M := M)
have of : ∀ (i : ι) (m : M i) (w : Word M),
  (HSMul.hSMul (α := CoprodI M) ((of (M := M) : (a : M i) → CoprodI M) m : CoprodI M) w).prod (M := M) =
    HMul.hMul (α := CoprodI M) ((of (M := M) : (a : M i) → CoprodI M) m : CoprodI M) (w.prod (M := M))
Tactic: induction m using CoprodI.induction_on with
  | one =>
    intro
    rw [one_smul, one_mul]
  | of _ =>
    intros
    rw [of_smul_def, prod_rcons, of.map_mul, mul_assoc, ← prod_rcons, ← equivPair_symm,
      Equiv.symm_apply_apply]
  | mul x y hx hy =>
    intro w
    rw [mul_smul, hx, hy, mul_assoc]
Cleared hypotheses: m
-- Lean 4 proof step from Mathlib.GroupTheory.CoprodI (goal)
Goal:
ι : Type u_1
M : ι → Type u_2
inst : (i : ι) → Monoid (M i)
inst_1 : DecidableEq ι
inst_2 : (i : ι) → DecidableEq (M i)
m : CoprodI M
one : ∀ (w : Word M), (HSMul.hSMul (α := CoprodI M) 1 w).prod (M := M) = 1 * w.prod (M := M)
of :
  ∀ (i : ι) (m : M i) (w : Word M),
    (HSMul.hSMul (α := CoprodI M) ((CoprodI.of (M := M) : (a : M i) → CoprodI M) m : CoprodI M) w).prod (M := M) =
      HMul.hMul (α := CoprodI M) ((CoprodI.of (M := M) : (a : M i) → CoprodI M) m : CoprodI M) (w.prod (M := M))
⊢ ∀ (w : Word M), (m • w).prod (M := M) = m * w.prod (M := M)
have mul : ∀ (x y : CoprodI M) (hx : ∀ (w : Word M), (x • w).prod (M := M) = x * w.prod (M := M))
  (hy : ∀ (w : Word M), (y • w).prod (M := M) = y * w.prod (M := M)) (w : Word M),
  ((x * y) • w).prod (M := M) = x * y * w.prod (M := M)
Tactic: induction m using CoprodI.induction_on with
  | one =>
    intro
    rw [one_smul, one_mul]
  | of _ =>
    intros
    rw [of_smul_def, prod_rcons, of.map_mul, mul_assoc, ← prod_rcons, ← equivPair_symm,
      Equiv.symm_apply_apply]
  | mul x y hx hy =>
    intro w
    rw [mul_smul, hx, hy, mul_assoc]
Cleared hypotheses: m
-- Lean 4 proof step from Mathlib.GroupTheory.CoprodI (goal)
Goal:
ι : Type u_1
M : ι → Type u_2
inst : (i : ι) → Monoid (M i)
N : Type u_3
inst_1 : Monoid N
inst_2 : DecidableEq ι
inst_3 : (i : ι) → DecidableEq (M i)
m : CoprodI M
⊢ (HSMul.hSMul (β := Word M) m (empty (M := M))).prod (M := M) = m
have rw : m * prod (M := M) (empty (M := M)) = m
Tactic: rw [prod_smul, prod_empty, mul_one]
-- Lean 4 proof step from Mathlib.GroupTheory.CoprodI (goal)
Goal:
ι : Type u_1
M : ι → Type u_2
inst : (i : ι) → Monoid (M i)
N : Type u_3
inst_1 : Monoid N
inst_2 : DecidableEq ι
inst_3 : (i : ι) → DecidableEq (M i)
m : CoprodI M
rw : m * prod (M := M) (empty (M := M)) = m
⊢ (HSMul.hSMul (β := Word M) m (empty (M := M))).prod (M := M) = m
have rw₁ : m * 1 = m
Tactic: rw [prod_smul, prod_empty, mul_one]
-- Lean 4 proof step from Mathlib.GroupTheory.CoprodI (goal)
Goal:
ι : Type u_1
M : ι → Type u_2
inst : (i : ι) → Monoid (M i)
N : Type u_3
inst_1 : Monoid N
inst_2 : DecidableEq ι
inst_3 : (i : ι) → DecidableEq (M i)
m : CoprodI M
rw : m * prod (M := M) (empty (M := M)) = m
rw₁ : m * 1 = m
⊢ (HSMul.hSMul (β := Word M) m (empty (M := M))).prod (M := M) = m
have rw₂ : m = m
Tactic: rw [prod_smul, prod_empty, mul_one]
-- Lean 4 proof step from Mathlib.GroupTheory.CoprodI (goal)
Goal:
ι : Type u_1
M : ι → Type u_2
inst : (i : ι) → Monoid (M i)
N : Type u_3
inst_1 : Monoid N
inst_2 : DecidableEq ι
inst_3 : (i : ι) → DecidableEq (M i)
⊢ Function.RightInverse (fun (w : Word M) ↦ w.prod (M := M)) fun (m : CoprodI M) ↦
    HSMul.hSMul (β := Word M) m (empty (M := M))
have empty : Eq (α := Word M)
  ((fun (m : CoprodI M) ↦ HSMul.hSMul (β := Word M) m (empty (M := M)))
    ((fun (w : Word M) ↦ w.prod (M := M)) (empty (M := M))))
  (empty (M := M))
Tactic: apply smul_induction
-- Lean 4 proof step from Mathlib.GroupTheory.CoprodI (goal)
Goal:
ι : Type u_1
M : ι → Type u_2
inst : (i : ι) → Monoid (M i)
N : Type u_3
inst_1 : Monoid N
inst_2 : DecidableEq ι
inst_3 : (i : ι) → DecidableEq (M i)
empty :
  Eq (α := Word M)
    ((fun (m : CoprodI M) ↦ HSMul.hSMul (β := Word M) m (Word.empty (M := M)))
      ((fun (w : Word M) ↦ w.prod (M := M)) (Word.empty (M := M))))
    (Word.empty (M := M))
⊢ Function.RightInverse (fun (w : Word M) ↦ w.prod (M := M)) fun (m : CoprodI M) ↦
    HSMul.hSMul (β := Word M) m (Word.empty (M := M))
have smul : ∀ (i : ι) (m : M i) (w : Word M),
  (fun (m : CoprodI M) ↦ HSMul.hSMul (β := Word M) m (Word.empty (M := M))) ((fun (w : Word M) ↦ w.prod (M := M)) w) =
      w →
    (fun (m : CoprodI M) ↦ HSMul.hSMul (β := Word M) m (Word.empty (M := M)))
        ((fun (w : Word M) ↦ w.prod (M := M))
          (HSMul.hSMul (α := CoprodI M) ((of (M := M) : (a : M i) → CoprodI M) m : CoprodI M) w)) =
      HSMul.hSMul (α := CoprodI M) ((of (M := M) : (a : M i) → CoprodI M) m : CoprodI M) w
Tactic: apply smul_induction
-- Lean 4 proof step from Mathlib.GroupTheory.CoprodI (goal)
Goal:
ι : Type u_1
M : ι → Type u_2
inst : (i : ι) → Monoid (M i)
N : Type u_3
inst_1 : Monoid N
inst_2 : DecidableEq ι
inst_3 : (i : ι) → DecidableEq (M i)
⊢ HSMul.hSMul (α := CoprodI M) (β := Word M) (prod (M := M) (empty (M := M))) (empty (M := M)) = empty (M := M)
have empty : HSMul.hSMul (α := CoprodI M) (β := Word M) 1 (empty (M := M)) = empty (M := M)
Tactic: rw [prod_empty, one_smul]
-- Lean 4 proof step from Mathlib.GroupTheory.CoprodI (goal)
Goal:
ι : Type u_1
M : ι → Type u_2
inst : (i : ι) → Monoid (M i)
N : Type u_3
inst_1 : Monoid N
inst_2 : DecidableEq ι
inst_3 : (i : ι) → DecidableEq (M i)
empty : HSMul.hSMul (α := CoprodI M) (β := Word M) 1 (Word.empty (M := M)) = Word.empty (M := M)
⊢ HSMul.hSMul (α := CoprodI M) (β := Word M) (prod (M := M) (Word.empty (M := M))) (Word.empty (M := M)) =
    Word.empty (M := M)
have empty₁ : Eq (α := Word M) (Word.empty (M := M)) (Word.empty (M := M))
Tactic: rw [prod_empty, one_smul]
-- Lean 4 proof step from Mathlib.GroupTheory.CoprodI (goal)
Goal:
ι : Type u_1
M : ι → Type u_2
inst : (i : ι) → Monoid (M i)
N : Type u_3
inst_1 : Monoid N
inst_2 : DecidableEq ι
inst_3 : (i : ι) → DecidableEq (M i)
i : ι
m : M i
w : Word M
ih : HSMul.hSMul (β := Word M) (w.prod (M := M)) (empty (M := M)) = w
⊢ HSMul.hSMul (β := Word M)
      ((HSMul.hSMul (α := CoprodI M) ((of (M := M) : (a : M i) → CoprodI M) m : CoprodI M) w).prod (M := M))
      (empty (M := M)) =
    HSMul.hSMul (α := CoprodI M) ((of (M := M) : (a : M i) → CoprodI M) m : CoprodI M) w
have smul : HSMul.hSMul (β := Word M)
    (HMul.hMul (α := CoprodI M) ((of (M := M) : (a : M i) → CoprodI M) m : CoprodI M) (w.prod (M := M)))
    (empty (M := M)) =
  HSMul.hSMul (α := CoprodI M) ((of (M := M) : (a : M i) → CoprodI M) m : CoprodI M) w
Tactic: rw [prod_smul, mul_smul, ih]
-- Lean 4 proof step from Mathlib.GroupTheory.CoprodI (goal)
Goal:
ι : Type u_1
M : ι → Type u_2
inst : (i : ι) → Monoid (M i)
N : Type u_3
inst_1 : Monoid N
inst_2 : DecidableEq ι
inst_3 : (i : ι) → DecidableEq (M i)
i : ι
m : M i
w : Word M
ih : HSMul.hSMul (β := Word M) (w.prod (M := M)) (empty (M := M)) = w
smul :
  HSMul.hSMul (β := Word M)
      (HMul.hMul (α := CoprodI M) ((of (M := M) : (a : M i) → CoprodI M) m : CoprodI M) (w.prod (M := M)))
      (empty (M := M)) =
    HSMul.hSMul (α := CoprodI M) ((of (M := M) : (a : M i) → CoprodI M) m : CoprodI M) w
⊢ HSMul.hSMul (β := Word M)
      ((HSMul.hSMul (α := CoprodI M) ((of (M := M) : (a : M i) → CoprodI M) m : CoprodI M) w).prod (M := M))
      (empty (M := M)) =
    HSMul.hSMul (α := CoprodI M) ((of (M := M) : (a : M i) → CoprodI M) m : CoprodI M) w
have smul₁ : HSMul.hSMul (α := CoprodI M) ((of (M := M) : (a : M i) → CoprodI M) m : CoprodI M)
    (HSMul.hSMul (β := Word M) (w.prod (M := M)) (empty (M := M))) =
  HSMul.hSMul (α := CoprodI M) ((of (M := M) : (a : M i) → CoprodI M) m : CoprodI M) w
Tactic: rw [prod_smul, mul_smul, ih]
-- Lean 4 proof step from Mathlib.GroupTheory.CoprodI (goal)
Goal:
ι : Type u_1
M : ι → Type u_2
inst : (i : ι) → Monoid (M i)
N : Type u_3
inst_1 : Monoid N
inst_2 : DecidableEq ι
inst_3 : (i : ι) → DecidableEq (M i)
i : ι
m : M i
w : Word M
ih : HSMul.hSMul (β := Word M) (w.prod (M := M)) (empty (M := M)) = w
smul :
  HSMul.hSMul (β := Word M)
      (HMul.hMul (α := CoprodI M) ((of (M := M) : (a : M i) → CoprodI M) m : CoprodI M) (w.prod (M := M)))
      (empty (M := M)) =
    HSMul.hSMul (α := CoprodI M) ((of (M := M) : (a : M i) → CoprodI M) m : CoprodI M) w
smul₁ :
  HSMul.hSMul (α := CoprodI M) ((of (M := M) : (a : M i) → CoprodI M) m : CoprodI M)
      (HSMul.hSMul (β := Word M) (w.prod (M := M)) (empty (M := M))) =
    HSMul.hSMul (α := CoprodI M) ((of (M := M) : (a : M i) → CoprodI M) m : CoprodI M) w
⊢ HSMul.hSMul (β := Word M)
      ((HSMul.hSMul (α := CoprodI M) ((of (M := M) : (a : M i) → CoprodI M) m : CoprodI M) w).prod (M := M))
      (empty (M := M)) =
    HSMul.hSMul (α := CoprodI M) ((of (M := M) : (a : M i) → CoprodI M) m : CoprodI M) w
have smul₂ : HSMul.hSMul (α := CoprodI M) ((of (M := M) : (a : M i) → CoprodI M) m : CoprodI M) w =
  HSMul.hSMul (α := CoprodI M) ((of (M := M) : (a : M i) → CoprodI M) m : CoprodI M) w
Tactic: rw [prod_smul, mul_smul, ih]
-- 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
⊢ w.toList (M := M) ≠ []
have singleton : ∀ {i : ι} (x : M i) (a : x ≠ 1), (singleton (M := M) x a).toList (M := M) ≠ []
Tactic: induction w
Cleared hypotheses: 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
singleton : ∀ {i : ι} (x : M i) (a : x ≠ 1), (NeWord.singleton (M := M) x a).toList (M := M) ≠ []
⊢ w.toList (M := M) ≠ []
have append : ∀ {i j k l : ι} (_w₁ : NeWord M i j) (_hne : j ≠ k) (_w₂ : NeWord M k l),
  _w₁.toList (M := M) ≠ [] → _w₂.toList (M := M) ≠ [] → (_w₁.append (M := M) _hne _w₂).toList (M := M) ≠ []
Tactic: induction w
Cleared hypotheses: 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
⊢ w.toList (M := M).head? = some (Sigma.mk (β := fun (i : ι) ↦ M i) i (w.head (M := M)))
have case1 : ∀ (i : ι) (x : M i) (a : x ≠ 1),
  [Sigma.mk (β := fun (i : ι) ↦ M i) i x].head? =
    some (Sigma.mk (β := fun (i : ι) ↦ M i) i ((singleton (M := M) x a).head (M := M)))
Tactic: fun_induction toList with grind [head]
Cleared hypotheses: 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
case1 :
  ∀ (i : ι) (x : M i) (a : x ≠ 1),
    [Sigma.mk (β := fun (i : ι) ↦ M i) i x].head? =
      some (Sigma.mk (β := fun (i : ι) ↦ M i) i ((singleton (M := M) x a).head (M := M)))
⊢ w.toList (M := M).head? = some (Sigma.mk (β := fun (i : ι) ↦ M i) i (w.head (M := M)))
have case2 : ∀ (x x_1 j k : ι) (w₁ : NeWord M x j) (_hne : j ≠ k) (w₂ : NeWord M k x_1),
  w₁.toList (M := M).head? = some (Sigma.mk (β := fun (i : ι) ↦ M i) x (w₁.head (M := M))) →
    w₂.toList (M := M).head? = some (Sigma.mk (β := fun (i : ι) ↦ M i) k (w₂.head (M := M))) →
      (w₁.toList (M := M) ++ w₂.toList (M := M)).head? =
        some (Sigma.mk (β := fun (i : ι) ↦ M i) x ((w₁.append (M := M) _hne w₂).head (M := M)))
Tactic: fun_induction toList with grind [head]
Cleared hypotheses: 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
⊢ Sigma.mk (β := fun (i : ι) ↦ M i) j (w.last (M := M)) ∈ w.toList (M := M).getLast?
have singleton : ∀ {i : ι} (x : M i) (a : x ≠ 1),
  Sigma.mk (β := fun (i : ι) ↦ M i) i ((singleton (M := M) x a).last (M := M)) ∈
    (singleton (M := M) x a).toList (M := M).getLast?
Tactic: induction w
Cleared hypotheses: 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
singleton :
  ∀ {i : ι} (x : M i) (a : x ≠ 1),
    Sigma.mk (β := fun (i : ι) ↦ M i) i ((NeWord.singleton (M := M) x a).last (M := M)) ∈
      (NeWord.singleton (M := M) x a).toList (M := M).getLast?
⊢ Sigma.mk (β := fun (i : ι) ↦ M i) j (w.last (M := M)) ∈ w.toList (M := M).getLast?
have append : ∀ {i j k l : ι} (_w₁ : NeWord M i j) (_hne : j ≠ k) (_w₂ : NeWord M k l),
  Sigma.mk (β := fun (i : ι) ↦ M i) j (_w₁.last (M := M)) ∈ _w₁.toList (M := M).getLast? →
    Sigma.mk (β := fun (i : ι) ↦ M i) l (_w₂.last (M := M)) ∈ _w₂.toList (M := M).getLast? →
      Sigma.mk (β := fun (i : ι) ↦ M i) l ((_w₁.append (M := M) _hne _w₂).last (M := M)) ∈
        (_w₁.append (M := M) _hne _w₂).toList (M := M).getLast?
Tactic: induction w
Cleared hypotheses: w
-- Lean 4 proof step from Mathlib.GroupTheory.CoprodI (goal)
Goal:
ι : Type u_1
M : ι → Type u_2
inst : (i : ι) → Monoid (M i)
N : Type u_3
inst_1 : Monoid N
i j : ι
w : NeWord M i j
⊢ ∀ l ∈ w.toList (M := M), l.snd (β := fun (i : ι) ↦ M i) ≠ 1
have singleton : ∀ {i : ι} (x : M i) (a : x ≠ 1), ∀ l ∈ (singleton (M := M) x a).toList (M := M), l.snd (β := fun (i : ι) ↦ M i) ≠ 1
Tactic: induction w
Cleared hypotheses: w
-- Lean 4 proof step from Mathlib.GroupTheory.CoprodI (goal)
Goal:
ι : Type u_1
M : ι → Type u_2
inst : (i : ι) → Monoid (M i)
N : Type u_3
inst_1 : Monoid N
i j : ι
w : NeWord M i j
singleton :
  ∀ {i : ι} (x : M i) (a : x ≠ 1),
    ∀ l ∈ (NeWord.singleton (M := M) x a).toList (M := M), l.snd (β := fun (i : ι) ↦ M i) ≠ 1
⊢ ∀ l ∈ w.toList (M := M), l.snd (β := fun (i : ι) ↦ M i) ≠ 1
have append : ∀ {i j k l : ι} (_w₁ : NeWord M i j) (_hne : j ≠ k) (_w₂ : NeWord M k l),
  (∀ l ∈ _w₁.toList (M := M), l.snd (β := fun (i : ι) ↦ M i) ≠ 1) →
    (∀ l_1 ∈ _w₂.toList (M := M), l_1.snd (β := fun (i : ι) ↦ M i) ≠ 1) →
      ∀ l_1 ∈ (_w₁.append (M := M) _hne _w₂).toList (M := M), l_1.snd (β := fun (i : ι) ↦ M i) ≠ 1
Tactic: induction w
Cleared hypotheses: w
-- Lean 4 proof step from Mathlib.GroupTheory.CoprodI (hypothesis)
Goal:
ι : Type u_1
M : ι → Type u_2
inst : (i : ι) → Monoid (M i)
N : Type u_3
inst_1 : Monoid N
i j i_1 j_1 k l_1 : ι
_w₁ : NeWord M i_1 j_1
_hne : j_1 ≠ k
_w₂ : NeWord M k l_1
_w₁_ih : ∀ l ∈ _w₁.toList (M := M), l.snd (β := fun (i : ι) ↦ M i) ≠ 1
_w₂_ih : ∀ l ∈ _w₂.toList (M := M), l.snd (β := fun (i : ι) ↦ M i) ≠ 1
l : (i : ι) × M i
h : l ∈ (_w₁.append (M := M) _hne _w₂).toList (M := M)
⊢ l.snd (β := fun (i : ι) ↦ M i) ≠ 1
have h₁ : l ∈ _w₁.toList (M := M) ∨ l ∈ _w₂.toList (M := M)
Tactic: simp only [toList, List.mem_append] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.GroupTheory.CoprodI (goal)
Goal:
ι : Type u_1
M : ι → Type u_2
inst : (i : ι) → Monoid (M i)
N : Type u_3
inst_1 : Monoid N
i j i_1 j_1 k l_1 : ι
_w₁ : NeWord M i_1 j_1
_hne : j_1 ≠ k
_w₂ : NeWord M k l_1
_w₁_ih : ∀ l ∈ _w₁.toList (M := M), l.snd (β := fun (i : ι) ↦ M i) ≠ 1
_w₂_ih : ∀ l ∈ _w₂.toList (M := M), l.snd (β := fun (i : ι) ↦ M i) ≠ 1
l : (i : ι) × M i
h : l ∈ _w₁.toList (M := M) ∨ l ∈ _w₂.toList (M := M)
⊢ l.snd (β := fun (i : ι) ↦ M i) ≠ 1
have append : l ∈ _w₁.toList (M := M) → l.snd (β := fun (i : ι) ↦ M i) ≠ 1
Tactic: cases h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.GroupTheory.CoprodI (goal)
Goal:
ι : Type u_1
M : ι → Type u_2
inst : (i : ι) → Monoid (M i)
N : Type u_3
inst_1 : Monoid N
i j i_1 j_1 k l_1 : ι
_w₁ : NeWord M i_1 j_1
_hne : j_1 ≠ k
_w₂ : NeWord M k l_1
_w₁_ih : ∀ l ∈ _w₁.toList (M := M), l.snd (β := fun (i : ι) ↦ M i) ≠ 1
_w₂_ih : ∀ l ∈ _w₂.toList (M := M), l.snd (β := fun (i : ι) ↦ M i) ≠ 1
l : (i : ι) × M i
h : l ∈ _w₁.toList (M := M) ∨ l ∈ _w₂.toList (M := M)
append : l ∈ _w₁.toList (M := M) → l.snd (β := fun (i : ι) ↦ M i) ≠ 1
⊢ l.snd (β := fun (i : ι) ↦ M i) ≠ 1
have append₁ : l ∈ _w₂.toList (M := M) → l.snd (β := fun (i : ι) ↦ M i) ≠ 1
Tactic: cases h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.GroupTheory.CoprodI (goal)
Goal:
ι : Type u_1
M : ι → Type u_2
inst : (i : ι) → Monoid (M i)
N : Type u_3
inst_1 : Monoid N
i j : ι
w : NeWord M i j
⊢ List.IsChain (fun (l l' : (i : ι) × M i) ↦ l.fst (β := fun (i : ι) ↦ M i) ≠ l'.fst (β := fun (i : ι) ↦ M i))
    (w.toList (M := M))
have singleton : ∀ {i : ι} (x : M i) (a : x ≠ 1),
  List.IsChain (fun (l l' : (i : ι) × M i) ↦ l.fst (β := fun (i : ι) ↦ M i) ≠ l'.fst (β := fun (i : ι) ↦ M i))
    ((singleton (M := M) x a).toList (M := M))
Tactic: induction w
Cleared hypotheses: w
-- Lean 4 proof step from Mathlib.GroupTheory.CoprodI (goal)
Goal:
ι : Type u_1
M : ι → Type u_2
inst : (i : ι) → Monoid (M i)
N : Type u_3
inst_1 : Monoid N
i j : ι
w : NeWord M i j
singleton :
  ∀ {i : ι} (x : M i) (a : x ≠ 1),
    List.IsChain (fun (l l' : (i : ι) × M i) ↦ l.fst (β := fun (i : ι) ↦ M i) ≠ l'.fst (β := fun (i : ι) ↦ M i))
      ((NeWord.singleton (M := M) x a).toList (M := M))
⊢ List.IsChain (fun (l l' : (i : ι) × M i) ↦ l.fst (β := fun (i : ι) ↦ M i) ≠ l'.fst (β := fun (i : ι) ↦ M i))
    (w.toList (M := M))
have append : ∀ {i j k l : ι} (_w₁ : NeWord M i j) (_hne : j ≠ k) (_w₂ : NeWord M k l),
  List.IsChain (fun (l l' : (i : ι) × M i) ↦ l.fst (β := fun (i : ι) ↦ M i) ≠ l'.fst (β := fun (i : ι) ↦ M i))
      (_w₁.toList (M := M)) →
    List.IsChain (fun (l l' : (i : ι) × M i) ↦ l.fst (β := fun (i : ι) ↦ M i) ≠ l'.fst (β := fun (i : ι) ↦ M i))
        (_w₂.toList (M := M)) →
      List.IsChain (fun (l l' : (i : ι) × M i) ↦ l.fst (β := fun (i : ι) ↦ M i) ≠ l'.fst (β := fun (i : ι) ↦ M i))
        ((_w₁.append (M := M) _hne _w₂).toList (M := M))
Tactic: induction w
Cleared hypotheses: w
-- Lean 4 proof step from Mathlib.GroupTheory.CoprodI (goal)
Goal:
ι : Type u_1
M : ι → Type u_2
inst : (i : ι) → Monoid (M i)
N : Type u_3
inst_1 : Monoid N
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 :
  List.IsChain (fun (l l' : (i : ι) × M i) ↦ l.fst (β := fun (i : ι) ↦ M i) ≠ l'.fst (β := fun (i : ι) ↦ M i))
    (_w₁.toList (M := M))
_w₂_ih :
  List.IsChain (fun (l l' : (i : ι) × M i) ↦ l.fst (β := fun (i : ι) ↦ M i) ≠ l'.fst (β := fun (i : ι) ↦ M i))
    (_w₂.toList (M := M))
⊢ List.IsChain (fun (l l' : (i : ι) × M i) ↦ l.fst (β := fun (i : ι) ↦ M i) ≠ l'.fst (β := fun (i : ι) ↦ M i))
    ((_w₁.append (M := M) _hne _w₂).toList (M := M))
have append : ∀ x ∈ _w₁.toList (M := M).getLast?,
  ∀ y ∈ _w₂.toList (M := M).head?, x.fst (β := fun (i : ι) ↦ M i) ≠ y.fst (β := fun (i : ι) ↦ M i)
Tactic: refine List.IsChain.append (by assumption) (by assumption) ?_
-- Lean 4 proof step from Mathlib.GroupTheory.CoprodI (goal)
Goal:
ι : Type u_1
M : ι → Type u_2
inst : (i : ι) → Monoid (M i)
N : Type u_3
inst_1 : Monoid N
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 :
  List.IsChain (fun (l l' : (i : ι) × M i) ↦ l.fst (β := fun (i : ι) ↦ M i) ≠ l'.fst (β := fun (i : ι) ↦ M i))
    (_w₁.toList (M := M))
_w₂_ih :
  List.IsChain (fun (l l' : (i : ι) × M i) ↦ l.fst (β := fun (i : ι) ↦ M i) ≠ l'.fst (β := fun (i : ι) ↦ M i))
    (_w₂.toList (M := M))
x : (i : ι) × M i
hx : x ∈ _w₁.toList (M := M).getLast?
y : (i : ι) × M i
hy : y ∈ _w₂.toList (M := M).head?
⊢ x.fst (β := fun (i : ι) ↦ M i) ≠ y.fst (β := fun (i : ι) ↦ M i)
have append : ∀ (hx : Sigma.mk (β := fun (i : ι) ↦ M i) j_1 (_w₁.last (M := M)) = x) (y : (i : ι) × M i)
  (hy : y ∈ _w₂.toList (M := M).head?), x.fst (β := fun (i : ι) ↦ M i) ≠ y.fst (β := fun (i : ι) ↦ M i)
Tactic: rw [toList_getLast?, Option.mem_some_iff] at hx
Cleared hypotheses: hx, y, hy
-- Lean 4 proof step from Mathlib.GroupTheory.CoprodI (hypothesis)
Goal:
ι : Type u_1
M : ι → Type u_2
inst : (i : ι) → Monoid (M i)
N : Type u_3
inst_1 : Monoid N
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 :
  List.IsChain (fun (l l' : (i : ι) × M i) ↦ l.fst (β := fun (i : ι) ↦ M i) ≠ l'.fst (β := fun (i : ι) ↦ M i))
    (_w₁.toList (M := M))
_w₂_ih :
  List.IsChain (fun (l l' : (i : ι) × M i) ↦ l.fst (β := fun (i : ι) ↦ M i) ≠ l'.fst (β := fun (i : ι) ↦ M i))
    (_w₂.toList (M := M))
x : (i : ι) × M i
hx : Sigma.mk (β := fun (i : ι) ↦ M i) j_1 (_w₁.last (M := M)) = x
y : (i : ι) × M i
hy : y ∈ _w₂.toList (M := M).head?
⊢ x.fst (β := fun (i : ι) ↦ M i) ≠ y.fst (β := fun (i : ι) ↦ M i)
have hy₁ : Sigma.mk (β := fun (i : ι) ↦ M i) k (_w₂.head (M := M)) = y
Tactic: rw [toList_head?, Option.mem_some_iff] at hy
Cleared hypotheses: hy
-- Lean 4 proof step from Mathlib.GroupTheory.CoprodI (goal)
Goal:
ι : Type u_1
M : ι → Type u_2
inst : (i : ι) → Monoid (M i)
N : Type u_3
inst_1 : Monoid N
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 :
  List.IsChain (fun (l l' : (i : ι) × M i) ↦ l.fst (β := fun (i : ι) ↦ M i) ≠ l'.fst (β := fun (i : ι) ↦ M i))
    (_w₁.toList (M := M))
_w₂_ih :
  List.IsChain (fun (l l' : (i : ι) × M i) ↦ l.fst (β := fun (i : ι) ↦ M i) ≠ l'.fst (β := fun (i : ι) ↦ M i))
    (_w₂.toList (M := M))
x : (i : ι) × M i
hx : Sigma.mk (β := fun (i : ι) ↦ M i) j_1 (_w₁.last (M := M)) = x
y : (i : ι) × M i
hy : Sigma.mk (β := fun (i : ι) ↦ M i) k (_w₂.head (M := M)) = y
⊢ x.fst (β := fun (i : ι) ↦ M i) ≠ y.fst (β := fun (i : ι) ↦ M i)
have append : (Sigma.mk (β := fun (i : ι) ↦ M i) j_1 (_w₁.last (M := M))).fst (β := fun (i : ι) ↦ M i) ≠
  y.fst (β := fun (i : ι) ↦ M i)
Tactic: subst hx
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.GroupTheory.CoprodI (goal)
Goal:
ι : Type u_1
M : ι → Type u_2
inst : (i : ι) → Monoid (M i)
N : Type u_3
inst_1 : Monoid N
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 :
  List.IsChain (fun (l l' : (i : ι) × M i) ↦ l.fst (β := fun (i : ι) ↦ M i) ≠ l'.fst (β := fun (i : ι) ↦ M i))
    (_w₁.toList (M := M))
_w₂_ih :
  List.IsChain (fun (l l' : (i : ι) × M i) ↦ l.fst (β := fun (i : ι) ↦ M i) ≠ l'.fst (β := fun (i : ι) ↦ M i))
    (_w₂.toList (M := M))
y : (i : ι) × M i
hy : Sigma.mk (β := fun (i : ι) ↦ M i) k (_w₂.head (M := M)) = y
⊢ (Sigma.mk (β := fun (i : ι) ↦ M i) j_1 (_w₁.last (M := M))).fst (β := fun (i : ι) ↦ M i) ≠
    y.fst (β := fun (i : ι) ↦ M i)
have append : (Sigma.mk (β := fun (i : ι) ↦ M i) j_1 (_w₁.last (M := M))).fst (β := fun (i : ι) ↦ M i) ≠
  (Sigma.mk (β := fun (i : ι) ↦ M i) k (_w₂.head (M := M))).fst (β := fun (i : ι) ↦ M i)
Tactic: subst hy
Cleared hypotheses: y, hy
-- 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)
this : ∃ (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
have rcases : ∀ (i j : ι) (w_1 : NeWord M i j) (h : w_1.toWord (M := M).toList (M := M) = w.toList (M := M)),
  ∃ (i : ι) (j : ι) (w' : NeWord M i j), w'.toWord (M := M) = w
Tactic: rcases this with ⟨i, j, w, h⟩
Cleared hypotheses: this
-- 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 : ι) (j : ι) (w' : NeWord M i j), w'.toWord (M := M) = w_1
have refine : w.toWord (M := M) = w_1
Tactic: refine ⟨i, j, w, ?_⟩
-- 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)
⊢ w.toWord (M := M) = w_1
have toList : ∀ (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
Tactic: ext