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)
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))
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)
⊢ ∀ (w : Word M), (m • w).prod (M := M) = 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]

Premises used: Monoid.CoprodI.of, Equiv.symm_apply_apply, mul_assoc, Monoid.CoprodI.Word.of_smul_def, Monoid.CoprodI.Word.equivPair_symm, one_smul, Monoid.CoprodI.Word.prod_rcons, MonoidHom.map_mul, SemigroupAction.mul_smul, one_mul
-- 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)
m : CoprodI M
rw : m * prod (M := M) (empty (M := M)) = m
rw₁ : m * 1 = m
rw₂ rw₃ : m = m
⊢ (HSMul.hSMul (β := Word M) m (empty (M := M))).prod (M := M) = m

Tactic:
rw [prod_smul, prod_empty, mul_one]

Premises used: Monoid.CoprodI.Word.prod_smul, Monoid.CoprodI.Word.prod_empty, mul_one
-- 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)
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))
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
⊢ Function.RightInverse (fun (w : Word M) ↦ w.prod (M := M)) fun (m : CoprodI M) ↦
    HSMul.hSMul (β := Word M) m (Word.empty (M := M))

Tactic:
apply smul_induction
-- 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)
empty : HSMul.hSMul (α := CoprodI M) (β := Word M) 1 (Word.empty (M := M)) = Word.empty (M := M)
empty₁ empty₂ : Eq (α := Word M) (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)

Tactic:
rw [prod_empty, one_smul]

Premises used: one_smul, Monoid.CoprodI.Word.prod_empty
-- 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 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
smul₂ 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
⊢ 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

Tactic:
rw [prod_smul, mul_smul, ih]

Premises used: Monoid.CoprodI.Word.prod_smul, SemigroupAction.mul_smul
-- Module: Mathlib.GroupTheory.CoprodI
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) ≠ []
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) ≠ []
⊢ w.toList (M := M) ≠ []

Tactic:
induction w
-- Module: Mathlib.GroupTheory.CoprodI
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₁.toList (M := M) ≠ []
_w₂_ih : _w₂.toList (M := M) ≠ []
append : _w₁.toList (M := M) ≠ []
⊢ (_w₁.append (M := M) _hne _w₂).toList (M := M) ≠ []

Tactic:
apply List.append_ne_nil_of_left_ne_nil

Premises used: List.append_ne_nil_of_left_ne_nil
-- Module: Mathlib.GroupTheory.CoprodI
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₁.toList (M := M) ≠ []
_w₂_ih : _w₂.toList (M := M) ≠ []
⊢ _w₁.toList (M := M) ≠ []

Tactic:
assumption
-- Module: Mathlib.GroupTheory.CoprodI
Goal:
ι : Type u_1
M : ι → Type u_2
inst : (i : ι) → Monoid (M i)
i j i_1 : ι
x : M i_1
h : x ≠ 1
⊢ [Sigma.mk (β := fun (i : ι) ↦ M i) i_1 x].head? =
    some (Sigma.mk (β := fun (i : ι) ↦ M i) i_1 ((singleton (M := M) x h).head (M := M)))

Tactic:
grind [head]

Premises used: Monoid.CoprodI.NeWord.head
-- Module: Mathlib.GroupTheory.CoprodI
Goal:
ι : Type u_1
M : ι → Type u_2
inst : (i : ι) → Monoid (M i)
i j x x_1 j_1 k : ι
w₁ : NeWord M x j_1
_hne : j_1 ≠ k
w₂ : NeWord M k x_1
ih2 : w₁.toList (M := M).head? = some (Sigma.mk (β := fun (i : ι) ↦ M i) x (w₁.head (M := M)))
ih1 : 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:
grind [head]

Premises used: Monoid.CoprodI.NeWord.head
-- Module: Mathlib.GroupTheory.CoprodI
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)))
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)))
⊢ w.toList (M := M).head? = some (Sigma.mk (β := fun (i : ι) ↦ M i) i (w.head (M := M)))

Tactic:
fun_induction toList with grind [head]

Premises used: Monoid.CoprodI.NeWord.toList, Monoid.CoprodI.NeWord.head
-- Module: Mathlib.GroupTheory.CoprodI
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?
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?
⊢ Sigma.mk (β := fun (i : ι) ↦ M i) j (w.last (M := M)) ∈ w.toList (M := M).getLast?

Tactic:
induction w
-- Module: Mathlib.GroupTheory.CoprodI
Goal:
ι : Type u_1
M : ι → Type u_2
inst : (i : ι) → Monoid (M i)
i j i_1 : ι
x : M i_1
h : x ≠ 1
⊢ (singleton (M := M) x h).toList (M := M).getLast? =
    some (Sigma.mk (β := fun (i : ι) ↦ M i) i_1 ((singleton (M := M) x h).last (M := M)))

Tactic:
rfl
-- Module: Mathlib.GroupTheory.CoprodI
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 : Sigma.mk (β := fun (i : ι) ↦ M i) j_1 (_w₁.last (M := M)) ∈ _w₁.toList (M := M).getLast?
_w₂_ih : 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₂.toList (M := M).getLast?

Tactic:
assumption
-- Module: Mathlib.GroupTheory.CoprodI
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 : Sigma.mk (β := fun (i : ι) ↦ M i) j_1 (_w₁.last (M := M)) ∈ _w₁.toList (M := M).getLast?
_w₂_ih : 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:
exact List.mem_getLast?_append_of_mem_getLast? (by assumption)

Premises used: List.mem_getLast?_append_of_mem_getLast?
-- 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
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
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
⊢ ∀ l ∈ w.toList (M := M), l.snd (β := fun (i : ι) ↦ M i) ≠ 1

Tactic:
induction w
-- 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
i j i_1 : ι
x : M i_1
h : x ≠ 1
⊢ ∀ l ∈ (singleton (M := M) x h).toList (M := M), l.snd (β := fun (i : ι) ↦ M i) ≠ 1

Tactic:
simpa only [toList, List.mem_singleton, ne_eq, forall_eq]

Premises used: forall_eq, List.mem_singleton, ne_eq, Monoid.CoprodI.NeWord.toList
-- 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
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 ∈ _w₁.toList (M := M) ∨ l ∈ _w₂.toList (M := M)

Tactic:
simp only [toList, List.mem_append] at h

Premises used: List.mem_append, Monoid.CoprodI.NeWord.toList
-- 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
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
append₁ : l ∈ _w₂.toList (M := M) → l.snd (β := fun (i : ι) ↦ M i) ≠ 1
⊢ l.snd (β := fun (i : ι) ↦ M i) ≠ 1

Tactic:
cases h
-- 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
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.snd (β := fun (i : ι) ↦ M i) ≠ 1

Tactic:
aesop
-- 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
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.snd (β := fun (i : ι) ↦ M i) ≠ 1

Tactic:
aesop
-- 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
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))
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))
⊢ List.IsChain (fun (l l' : (i : ι) × M i) ↦ l.fst (β := fun (i : ι) ↦ M i) ≠ l'.fst (β := fun (i : ι) ↦ M i))
    (w.toList (M := M))

Tactic:
induction w
-- 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
i j i_1 : ι
x : M i_1
h : 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 h).toList (M := M))

Tactic:
List.isChain_singleton _

Premises used: List.isChain_singleton, Monoid.CoprodI.NeWord.toList
-- 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
i j i_1 : ι
x : M i_1
h : 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 h).toList (M := M))

Tactic:
exact List.isChain_singleton _

Premises used: List.isChain_singleton
-- 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
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₁.toList (M := M))

Tactic:
assumption
-- 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
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₂.toList (M := M))

Tactic:
assumption
-- 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
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))
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)
⊢ 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:
refine List.IsChain.append (by assumption) (by assumption) ?_

Premises used: List.IsChain.append
-- 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
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?
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)
⊢ x.fst (β := fun (i : ι) ↦ M i) ≠ y.fst (β := fun (i : ι) ↦ M i)

Tactic:
rw [toList_getLast?, Option.mem_some_iff] at hx

Premises used: Option.mem_some_iff, Monoid.CoprodI.NeWord.toList_getLast?
-- 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
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?
⊢ Sigma.mk (β := fun (i : ι) ↦ M i) k (_w₂.head (M := M)) = y

Tactic:
rw [toList_head?, Option.mem_some_iff] at hy

Premises used: Monoid.CoprodI.NeWord.toList_head?, Option.mem_some_iff
-- 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
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
append :
  (Sigma.mk (β := fun (i : ι) ↦ M i) j_1 (_w₁.last (M := M))).fst (β := fun (i : ι) ↦ M i) ≠
    y.fst (β := fun (i : ι) ↦ M i)
⊢ x.fst (β := fun (i : ι) ↦ M i) ≠ y.fst (β := fun (i : ι) ↦ M i)

Tactic:
subst hx
-- 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
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
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)
⊢ (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 hy
-- 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
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))
⊢ (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:
assumption
-- 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)
this : ∃ (i : ι) (j : ι) (w' : NeWord M i j), w'.toWord (M := M).toList (M := M) = w.toList (M := M)
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
⊢ ∃ (i : ι) (j : ι) (w' : NeWord M i j), w'.toWord (M := M) = w

Tactic:
rcases this with ⟨i, j, w, h⟩
-- 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 : ι) (j : ι) (w' : NeWord M i j), w'.toWord (M := M) = w_1

Tactic:
⟨i, j, w, ?_⟩

Premises used: Exists.intro
-- 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)
refine : w.toWord (M := M) = w_1
⊢ ∃ (i : ι) (j : ι) (w' : NeWord M i j), w'.toWord (M := M) = w_1

Tactic:
refine ⟨i, j, w, ?_⟩
-- 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)
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
⊢ w.toWord (M := M) = w_1

Tactic:
ext