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 : (i : ι) → DecidableEq (M i)
i : ι
p : Pair M i
hm : ¬p.head (M := M) = 1
rw :
  prod (M := M)
      (if h : p.head (M := M) = 1 then p.tail (M := M) else cons (M := M) (p.head (M := M)) (p.tail (M := M)) ⋯ h) =
    HMul.hMul (α := CoprodI M) ((of (M := M) : (a : M i) → CoprodI M) (p.head (M := M)) : CoprodI M)
      (p.tail (M := M).prod (M := M))
⊢ (rcons (M := M) p).prod (M := M) =
    HMul.hMul (α := CoprodI M) ((of (M := M) : (a : M i) → CoprodI M) (p.head (M := M)) : CoprodI M)
      (p.tail (M := M).prod (M := M))
have rw₁ : (cons (M := M) (p.head (M := M)) (p.tail (M := M)) sorry hm).prod (M := M) =
  HMul.hMul (α := CoprodI M) ((of (M := M) : (a : M i) → CoprodI M) (p.head (M := M)) : CoprodI M)
    (p.tail (M := M).prod (M := M))
Tactic: rw [rcons, dif_neg hm, cons, prod, List.map_cons, List.prod_cons, prod]
-- Lean 4 proof step from Mathlib.GroupTheory.CoprodI (goal)
Goal:
ι : Type u_1
M : ι → Type u_2
inst : (i : ι) → Monoid (M i)
inst_1 : (i : ι) → DecidableEq (M i)
i : ι
p : Pair M i
hm : ¬p.head (M := M) = 1
rw :
  prod (M := M)
      (if h : p.head (M := M) = 1 then p.tail (M := M) else cons (M := M) (p.head (M := M)) (p.tail (M := M)) ⋯ h) =
    HMul.hMul (α := CoprodI M) ((of (M := M) : (a : M i) → CoprodI M) (p.head (M := M)) : CoprodI M)
      (p.tail (M := M).prod (M := M))
rw₁ :
  (cons (M := M) (p.head (M := M)) (p.tail (M := M)) ⋯ hm).prod (M := M) =
    HMul.hMul (α := CoprodI M) ((of (M := M) : (a : M i) → CoprodI M) (p.head (M := M)) : CoprodI M)
      (p.tail (M := M).prod (M := M))
⊢ (rcons (M := M) p).prod (M := M) =
    HMul.hMul (α := CoprodI M) ((of (M := M) : (a : M i) → CoprodI M) (p.head (M := M)) : CoprodI M)
      (p.tail (M := M).prod (M := M))
have rw₂ : (mk (M := M) (Sigma.mk (β := fun (i : ι) ↦ M i) i (p.head (M := M)) :: p.tail (M := M).toList (M := M)) sorry sorry).prod (M :=
    M) =
  HMul.hMul (α := CoprodI M) ((of (M := M) : (a : M i) → CoprodI M) (p.head (M := M)) : CoprodI M)
    (p.tail (M := M).prod (M := M))
Tactic: rw [rcons, dif_neg hm, cons, prod, List.map_cons, List.prod_cons, prod]
-- Lean 4 proof step from Mathlib.GroupTheory.CoprodI (goal)
Goal:
ι : Type u_1
M : ι → Type u_2
inst : (i : ι) → Monoid (M i)
inst_1 : (i : ι) → DecidableEq (M i)
i : ι
p : Pair M i
hm : ¬p.head (M := M) = 1
rw :
  prod (M := M)
      (if h : p.head (M := M) = 1 then p.tail (M := M) else cons (M := M) (p.head (M := M)) (p.tail (M := M)) ⋯ h) =
    HMul.hMul (α := CoprodI M) ((of (M := M) : (a : M i) → CoprodI M) (p.head (M := M)) : CoprodI M)
      (p.tail (M := M).prod (M := M))
rw₁ :
  (cons (M := M) (p.head (M := M)) (p.tail (M := M)) ⋯ hm).prod (M := M) =
    HMul.hMul (α := CoprodI M) ((of (M := M) : (a : M i) → CoprodI M) (p.head (M := M)) : CoprodI M)
      (p.tail (M := M).prod (M := M))
rw₂ :
  (mk (M := M) (Sigma.mk (β := fun (i : ι) ↦ M i) i (p.head (M := M)) :: p.tail (M := M).toList (M := M)) ⋯ ⋯).prod
      (M := M) =
    HMul.hMul (α := CoprodI M) ((of (M := M) : (a : M i) → CoprodI M) (p.head (M := M)) : CoprodI M)
      (p.tail (M := M).prod (M := M))
⊢ (rcons (M := M) p).prod (M := M) =
    HMul.hMul (α := CoprodI M) ((of (M := M) : (a : M i) → CoprodI M) (p.head (M := M)) : CoprodI M)
      (p.tail (M := M).prod (M := M))
have rw₃ : List.prod
    (List.map (fun (l : (i : ι) × M i) ↦ (of (M := M) : (a : M l.fst) → CoprodI M) (l.snd (β := fun (i : ι) ↦ M i)))
      ((mk (M := M) (Sigma.mk (β := fun (i : ι) ↦ M i) i (p.head (M := M)) :: p.tail (M := M).toList (M := M)) sorry
            sorry).toList
        (M := M))) =
  HMul.hMul (α := CoprodI M) ((of (M := M) : (a : M i) → CoprodI M) (p.head (M := M)) : CoprodI M)
    (p.tail (M := M).prod (M := M))
Tactic: rw [rcons, dif_neg hm, cons, prod, List.map_cons, List.prod_cons, prod]
-- Lean 4 proof step from Mathlib.GroupTheory.CoprodI (goal)
Goal:
ι : Type u_1
M : ι → Type u_2
inst : (i : ι) → Monoid (M i)
inst_1 : (i : ι) → DecidableEq (M i)
i : ι
p : Pair M i
hm : ¬p.head (M := M) = 1
rw :
  prod (M := M)
      (if h : p.head (M := M) = 1 then p.tail (M := M) else cons (M := M) (p.head (M := M)) (p.tail (M := M)) ⋯ h) =
    HMul.hMul (α := CoprodI M) ((of (M := M) : (a : M i) → CoprodI M) (p.head (M := M)) : CoprodI M)
      (p.tail (M := M).prod (M := M))
rw₁ :
  (cons (M := M) (p.head (M := M)) (p.tail (M := M)) ⋯ hm).prod (M := M) =
    HMul.hMul (α := CoprodI M) ((of (M := M) : (a : M i) → CoprodI M) (p.head (M := M)) : CoprodI M)
      (p.tail (M := M).prod (M := M))
rw₂ :
  (mk (M := M) (Sigma.mk (β := fun (i : ι) ↦ M i) i (p.head (M := M)) :: p.tail (M := M).toList (M := M)) ⋯ ⋯).prod
      (M := M) =
    HMul.hMul (α := CoprodI M) ((of (M := M) : (a : M i) → CoprodI M) (p.head (M := M)) : CoprodI M)
      (p.tail (M := M).prod (M := M))
rw₃ :
  List.prod
      (List.map (fun (l : (i : ι) × M i) ↦ (of (M := M) : (a : M l.fst) → CoprodI M) (l.snd (β := fun (i : ι) ↦ M i)))
        ((mk (M := M) (Sigma.mk (β := fun (i : ι) ↦ M i) i (p.head (M := M)) :: p.tail (M := M).toList (M := M)) ⋯
              ⋯).toList
          (M := M))) =
    HMul.hMul (α := CoprodI M) ((of (M := M) : (a : M i) → CoprodI M) (p.head (M := M)) : CoprodI M)
      (p.tail (M := M).prod (M := M))
⊢ (rcons (M := M) p).prod (M := M) =
    HMul.hMul (α := CoprodI M) ((of (M := M) : (a : M i) → CoprodI M) (p.head (M := M)) : CoprodI M)
      (p.tail (M := M).prod (M := M))
have rw₄ : List.prod
    ((of (M := M) : (a : M ⟨i, p.head⟩.fst) → CoprodI M)
        ((Sigma.mk (β := fun (i : ι) ↦ M i) i (p.head (M := M))).snd (β := fun (i : ι) ↦ M i)) ::
      List.map (fun (l : (i : ι) × M i) ↦ (of (M := M) : (a : M l.fst) → CoprodI M) (l.snd (β := fun (i : ι) ↦ M i)))
        (p.tail (M := M).toList (M := M))) =
  HMul.hMul (α := CoprodI M) ((of (M := M) : (a : M i) → CoprodI M) (p.head (M := M)) : CoprodI M)
    (p.tail (M := M).prod (M := M))
Tactic: rw [rcons, dif_neg hm, cons, prod, List.map_cons, List.prod_cons, prod]
-- Lean 4 proof step from Mathlib.GroupTheory.CoprodI (goal)
Goal:
ι : Type u_1
M : ι → Type u_2
inst : (i : ι) → Monoid (M i)
inst_1 : (i : ι) → DecidableEq (M i)
i : ι
p : Pair M i
hm : ¬p.head (M := M) = 1
rw :
  prod (M := M)
      (if h : p.head (M := M) = 1 then p.tail (M := M) else cons (M := M) (p.head (M := M)) (p.tail (M := M)) ⋯ h) =
    HMul.hMul (α := CoprodI M) ((of (M := M) : (a : M i) → CoprodI M) (p.head (M := M)) : CoprodI M)
      (p.tail (M := M).prod (M := M))
rw₁ :
  (cons (M := M) (p.head (M := M)) (p.tail (M := M)) ⋯ hm).prod (M := M) =
    HMul.hMul (α := CoprodI M) ((of (M := M) : (a : M i) → CoprodI M) (p.head (M := M)) : CoprodI M)
      (p.tail (M := M).prod (M := M))
rw₂ :
  (mk (M := M) (Sigma.mk (β := fun (i : ι) ↦ M i) i (p.head (M := M)) :: p.tail (M := M).toList (M := M)) ⋯ ⋯).prod
      (M := M) =
    HMul.hMul (α := CoprodI M) ((of (M := M) : (a : M i) → CoprodI M) (p.head (M := M)) : CoprodI M)
      (p.tail (M := M).prod (M := M))
rw₃ :
  List.prod
      (List.map (fun (l : (i : ι) × M i) ↦ (of (M := M) : (a : M l.fst) → CoprodI M) (l.snd (β := fun (i : ι) ↦ M i)))
        ((mk (M := M) (Sigma.mk (β := fun (i : ι) ↦ M i) i (p.head (M := M)) :: p.tail (M := M).toList (M := M)) ⋯
              ⋯).toList
          (M := M))) =
    HMul.hMul (α := CoprodI M) ((of (M := M) : (a : M i) → CoprodI M) (p.head (M := M)) : CoprodI M)
      (p.tail (M := M).prod (M := M))
rw₄ :
  List.prod
      ((of (M := M) : (a : M ⟨i, p.head⟩.fst) → CoprodI M)
          ((Sigma.mk (β := fun (i : ι) ↦ M i) i (p.head (M := M))).snd (β := fun (i : ι) ↦ M i)) ::
        List.map (fun (l : (i : ι) × M i) ↦ (of (M := M) : (a : M l.fst) → CoprodI M) (l.snd (β := fun (i : ι) ↦ M i)))
          (p.tail (M := M).toList (M := M))) =
    HMul.hMul (α := CoprodI M) ((of (M := M) : (a : M i) → CoprodI M) (p.head (M := M)) : CoprodI M)
      (p.tail (M := M).prod (M := M))
⊢ (rcons (M := M) p).prod (M := M) =
    HMul.hMul (α := CoprodI M) ((of (M := M) : (a : M i) → CoprodI M) (p.head (M := M)) : CoprodI M)
      (p.tail (M := M).prod (M := M))
have rw₅ : HMul.hMul (α := CoprodI M) (β := CoprodI M)
    ((of (M := M) : (a : M ⟨i, p.head⟩.fst) → CoprodI M)
        ((Sigma.mk (β := fun (i : ι) ↦ M i) i (p.head (M := M))).snd (β := fun (i : ι) ↦ M i)) :
      CoprodI M)
    (List.prod
        (List.map (fun (l : (i : ι) × M i) ↦ (of (M := M) : (a : M l.fst) → CoprodI M) (l.snd (β := fun (i : ι) ↦ M i)))
          (p.tail (M := M).toList (M := M))) :
      CoprodI M) =
  HMul.hMul (α := CoprodI M) ((of (M := M) : (a : M i) → CoprodI M) (p.head (M := M)) : CoprodI M)
    (p.tail (M := M).prod (M := M))
Tactic: rw [rcons, dif_neg hm, cons, prod, List.map_cons, List.prod_cons, prod]
-- Lean 4 proof step from Mathlib.GroupTheory.CoprodI (goal)
Goal:
ι : Type u_1
M : ι → Type u_2
inst : (i : ι) → Monoid (M i)
inst_1 : (i : ι) → DecidableEq (M i)
i : ι
m : M i
w : Word M
h : w.fstIdx (M := M) ≠ some i
m' : M i
w' : Word M
h' : w'.fstIdx (M := M) ≠ some i
he : rcons (M := M) (Pair.mk (M := M) m w h) = rcons (M := M) (Pair.mk (M := M) m' w' h')
⊢ Pair.mk (M := M) m w h = Pair.mk (M := M) m' w' h'
have pos : ∀ (hm : m = 1), Pair.mk (M := M) m w h = Pair.mk (M := M) m' w' h'
Tactic: by_cases hm : m = 1
-- Lean 4 proof step from Mathlib.GroupTheory.CoprodI (goal)
Goal:
ι : Type u_1
M : ι → Type u_2
inst : (i : ι) → Monoid (M i)
inst_1 : (i : ι) → DecidableEq (M i)
i : ι
m : M i
w : Word M
h : w.fstIdx (M := M) ≠ some i
m' : M i
w' : Word M
h' : w'.fstIdx (M := M) ≠ some i
he : rcons (M := M) (Pair.mk (M := M) m w h) = rcons (M := M) (Pair.mk (M := M) m' w' h')
pos : ∀ (hm : m = 1), Pair.mk (M := M) m w h = Pair.mk (M := M) m' w' h'
⊢ Pair.mk (M := M) m w h = Pair.mk (M := M) m' w' h'
have neg : ∀ (hm : ¬m = 1), Pair.mk (M := M) m w h = Pair.mk (M := M) m' w' h'
Tactic: by_cases hm : m = 1
-- Lean 4 proof step from Mathlib.GroupTheory.CoprodI (goal)
Goal:
ι : Type u_1
M : ι → Type u_2
inst : (i : ι) → Monoid (M i)
inst_1 : (i : ι) → DecidableEq (M i)
i : ι
m : M i
w : Word M
h : w.fstIdx (M := M) ≠ some i
m' : M i
w' : Word M
h' : w'.fstIdx (M := M) ≠ some i
he : rcons (M := M) (Pair.mk (M := M) m w h) = rcons (M := M) (Pair.mk (M := M) m' w' h')
hm : m = 1
⊢ Pair.mk (M := M) m w h = Pair.mk (M := M) m' w' h'
have pos : ∀ (hm' : m' = 1), Pair.mk (M := M) m w h = Pair.mk (M := M) m' w' h'
Tactic: by_cases hm' : m' = 1
-- Lean 4 proof step from Mathlib.GroupTheory.CoprodI (goal)
Goal:
ι : Type u_1
M : ι → Type u_2
inst : (i : ι) → Monoid (M i)
inst_1 : (i : ι) → DecidableEq (M i)
i : ι
m : M i
w : Word M
h : w.fstIdx (M := M) ≠ some i
m' : M i
w' : Word M
h' : w'.fstIdx (M := M) ≠ some i
he : rcons (M := M) (Pair.mk (M := M) m w h) = rcons (M := M) (Pair.mk (M := M) m' w' h')
hm : m = 1
pos : ∀ (hm' : m' = 1), Pair.mk (M := M) m w h = Pair.mk (M := M) m' w' h'
⊢ Pair.mk (M := M) m w h = Pair.mk (M := M) m' w' h'
have neg : ∀ (hm' : ¬m' = 1), Pair.mk (M := M) m w h = Pair.mk (M := M) m' w' h'
Tactic: by_cases hm' : m' = 1
-- Lean 4 proof step from Mathlib.GroupTheory.CoprodI (goal)
Goal:
ι : Type u_1
M : ι → Type u_2
inst : (i : ι) → Monoid (M i)
inst_1 : (i : ι) → DecidableEq (M i)
i : ι
m : M i
w : Word M
h : w.fstIdx (M := M) ≠ some i
m' : M i
w' : Word M
h' : w'.fstIdx (M := M) ≠ some i
he : rcons (M := M) (Pair.mk (M := M) m w h) = rcons (M := M) (Pair.mk (M := M) m' w' h')
hm : ¬m = 1
⊢ Pair.mk (M := M) m w h = Pair.mk (M := M) m' w' h'
have pos : ∀ (hm' : m' = 1), Pair.mk (M := M) m w h = Pair.mk (M := M) m' w' h'
Tactic: by_cases hm' : m' = 1
-- Lean 4 proof step from Mathlib.GroupTheory.CoprodI (goal)
Goal:
ι : Type u_1
M : ι → Type u_2
inst : (i : ι) → Monoid (M i)
inst_1 : (i : ι) → DecidableEq (M i)
i : ι
m : M i
w : Word M
h : w.fstIdx (M := M) ≠ some i
m' : M i
w' : Word M
h' : w'.fstIdx (M := M) ≠ some i
he : rcons (M := M) (Pair.mk (M := M) m w h) = rcons (M := M) (Pair.mk (M := M) m' w' h')
hm : ¬m = 1
pos : ∀ (hm' : m' = 1), Pair.mk (M := M) m w h = Pair.mk (M := M) m' w' h'
⊢ Pair.mk (M := M) m w h = Pair.mk (M := M) m' w' h'
have neg : ∀ (hm' : ¬m' = 1), Pair.mk (M := M) m w h = Pair.mk (M := M) m' w' h'
Tactic: by_cases hm' : m' = 1
-- Lean 4 proof step from Mathlib.GroupTheory.CoprodI (hypothesis)
Goal:
ι : Type u_1
M : ι → Type u_2
inst : (i : ι) → Monoid (M i)
inst_1 : (i : ι) → DecidableEq (M i)
i : ι
m : M i
w : Word M
h : w.fstIdx (M := M) ≠ some i
m' : M i
w' : Word M
h' : w'.fstIdx (M := M) ≠ some i
he : rcons (M := M) (Pair.mk (M := M) m w h) = rcons (M := M) (Pair.mk (M := M) m' w' h')
hm : m = 1
hm' : m' = 1
⊢ Pair.mk (M := M) m w h = Pair.mk (M := M) m' w' h'
have he₁ : w = w'
Tactic: simp only [rcons, dif_pos hm, dif_pos hm'] at he
Cleared hypotheses: he
-- Lean 4 proof step from Mathlib.GroupTheory.CoprodI (goal)
Goal:
ι : Type u_1
M : ι → Type u_2
inst : (i : ι) → Monoid (M i)
inst_1 : (i : ι) → DecidableEq (M i)
i : ι
m : M i
w : Word M
h : w.fstIdx (M := M) ≠ some i
m' : M i
w' : Word M
h' : w'.fstIdx (M := M) ≠ some i
he : rcons (M := M) (Pair.mk (M := M) m w h) = rcons (M := M) (Pair.mk (M := M) m' w' h')
hm : m = 1
hm' : ¬m' = 1
⊢ Pair.mk (M := M) m w h = Pair.mk (M := M) m' w' h'
have neg : False
Tactic: exfalso
-- Lean 4 proof step from Mathlib.GroupTheory.CoprodI (hypothesis)
Goal:
ι : Type u_1
M : ι → Type u_2
inst : (i : ι) → Monoid (M i)
inst_1 : (i : ι) → DecidableEq (M i)
i : ι
m : M i
w : Word M
h : w.fstIdx (M := M) ≠ some i
m' : M i
w' : Word M
h' : w'.fstIdx (M := M) ≠ some i
he : rcons (M := M) (Pair.mk (M := M) m w h) = rcons (M := M) (Pair.mk (M := M) m' w' h')
hm : m = 1
hm' : ¬m' = 1
⊢ False
have he₁ : w = cons (M := M) m' w' sorry sorry
Tactic: simp only [rcons, dif_pos hm, dif_neg hm'] at he
Cleared hypotheses: he
-- Lean 4 proof step from Mathlib.GroupTheory.CoprodI (hypothesis)
Goal:
ι : Type u_1
M : ι → Type u_2
inst : (i : ι) → Monoid (M i)
inst_1 : (i : ι) → DecidableEq (M i)
i : ι
m : M i
w : Word M
h : w.fstIdx (M := M) ≠ some i
m' : M i
w' : Word M
h' : w'.fstIdx (M := M) ≠ some i
hm : m = 1
hm' : ¬m' = 1
he : w = cons (M := M) m' w' ⋯ ⋯
⊢ False
have h₁ : (cons (M := M) m' w' sorry sorry).fstIdx (M := M) ≠ some i
Tactic: rw [he] at h
Cleared hypotheses: h, he
-- Lean 4 proof step from Mathlib.GroupTheory.CoprodI (goal)
Goal:
ι : Type u_1
M : ι → Type u_2
inst : (i : ι) → Monoid (M i)
inst_1 : (i : ι) → DecidableEq (M i)
i : ι
m : M i
w : Word M
h : w.fstIdx (M := M) ≠ some i
m' : M i
w' : Word M
h' : w'.fstIdx (M := M) ≠ some i
he : rcons (M := M) (Pair.mk (M := M) m w h) = rcons (M := M) (Pair.mk (M := M) m' w' h')
hm : ¬m = 1
hm' : m' = 1
⊢ Pair.mk (M := M) m w h = Pair.mk (M := M) m' w' h'
have pos : False
Tactic: exfalso
-- Lean 4 proof step from Mathlib.GroupTheory.CoprodI (hypothesis)
Goal:
ι : Type u_1
M : ι → Type u_2
inst : (i : ι) → Monoid (M i)
inst_1 : (i : ι) → DecidableEq (M i)
i : ι
m : M i
w : Word M
h : w.fstIdx (M := M) ≠ some i
m' : M i
w' : Word M
h' : w'.fstIdx (M := M) ≠ some i
he : rcons (M := M) (Pair.mk (M := M) m w h) = rcons (M := M) (Pair.mk (M := M) m' w' h')
hm : ¬m = 1
hm' : m' = 1
⊢ False
have he₁ : cons (M := M) m w sorry sorry = w'
Tactic: simp only [rcons, dif_pos hm', dif_neg hm] at he
Cleared hypotheses: he
-- Lean 4 proof step from Mathlib.GroupTheory.CoprodI (hypothesis)
Goal:
ι : Type u_1
M : ι → Type u_2
inst : (i : ι) → Monoid (M i)
inst_1 : (i : ι) → DecidableEq (M i)
i : ι
m : M i
w : Word M
h : w.fstIdx (M := M) ≠ some i
m' : M i
w' : Word M
h' : w'.fstIdx (M := M) ≠ some i
hm : ¬m = 1
hm' : m' = 1
he : cons (M := M) m w ⋯ ⋯ = w'
⊢ False
have h'₁ : (cons (M := M) m w sorry sorry).fstIdx (M := M) ≠ some i
Tactic: rw [← he] at h'
Cleared hypotheses: h', hm', he
-- Lean 4 proof step from Mathlib.GroupTheory.CoprodI (hypothesis)
Goal:
ι : Type u_1
M : ι → Type u_2
inst : (i : ι) → Monoid (M i)
inst_1 : (i : ι) → DecidableEq (M i)
i : ι
m : M i
w : Word M
h : w.fstIdx (M := M) ≠ some i
m' : M i
w' : Word M
h' : w'.fstIdx (M := M) ≠ some i
he : rcons (M := M) (Pair.mk (M := M) m w h) = rcons (M := M) (Pair.mk (M := M) m' w' h')
hm : ¬m = 1
hm' : ¬m' = 1
⊢ Pair.mk (M := M) m w h = Pair.mk (M := M) m' w' h'
have this : m = m' ∧ w.toList (M := M) = w'.toList (M := M)
Tactic: have : m = m' ∧ w.toList = w'.toList := by
      simpa [cons, rcons, dif_neg hm, dif_neg hm', eq_self_iff_true, Subtype.mk_eq_mk,
        heq_iff_eq, ← Subtype.ext_iff] using he
-- Lean 4 proof step from Mathlib.GroupTheory.CoprodI (goal)
Goal:
ι : Type u_1
M : ι → Type u_2
inst : (i : ι) → Monoid (M i)
inst_1 : (i : ι) → DecidableEq (M i)
i : ι
m : M i
w : Word M
h : w.fstIdx (M := M) ≠ some i
m' : M i
w' : Word M
h' : w'.fstIdx (M := M) ≠ some i
he : rcons (M := M) (Pair.mk (M := M) m w h) = rcons (M := M) (Pair.mk (M := M) m' w' h')
hm : ¬m = 1
hm' : ¬m' = 1
this : m = m' ∧ w.toList (M := M) = w'.toList (M := M)
⊢ Pair.mk (M := M) m w h = Pair.mk (M := M) m' w' h'
have neg : ∀ (h_1 : w.toList (M := M) = w'.toList (M := M))
  (he : rcons (M := M) (Pair.mk (M := M) m w h) = rcons (M := M) (Pair.mk (M := M) m w' h')) (hm' : ¬m = 1),
  Pair.mk (M := M) m w h = Pair.mk (M := M) m w' h'
Tactic: rcases this with ⟨rfl, h⟩
Cleared hypotheses: m', he, hm', this
-- Lean 4 proof step from Mathlib.GroupTheory.CoprodI (goal)
Goal:
ι : Type u_1
M : ι → Type u_2
inst : (i : ι) → Monoid (M i)
inst_1 : (i : ι) → DecidableEq (M i)
i : ι
m : M i
w : Word M
h_1 : w.fstIdx (M := M) ≠ some i
w' : Word M
h' : w'.fstIdx (M := M) ≠ some i
hm : ¬m = 1
h : w.toList (M := M) = w'.toList (M := M)
he : rcons (M := M) (Pair.mk (M := M) m w h_1) = rcons (M := M) (Pair.mk (M := M) m w' h')
hm' : ¬m = 1
⊢ Pair.mk (M := M) m w h_1 = Pair.mk (M := M) m w' h'
have neg : w = w'
Tactic: congr
-- 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
motive : Word M → Sort u_4
w : Word M
empty : motive (Word.empty (M := M))
cons :
  (i : ι) →
    (m : M i) →
      (w : Word M) → (h1 : w.fstIdx (M := M) ≠ some i) → (h2 : m ≠ 1) → motive w → motive (Word.cons (M := M) m w h1 h2)
⊢ motive w
have rcases : (w : List ((i : ι) × M i)) →
  (h1 : ∀ l ∈ w, l.snd (β := fun (i : ι) ↦ M i) ≠ 1) →
    (h2 :
        List.IsChain (fun (l l' : (i : ι) × M i) ↦ l.fst (β := fun (i : ι) ↦ M i) ≠ l'.fst (β := fun (i : ι) ↦ M i))
          w) →
      motive (mk (M := M) w h1 h2)
Tactic: rcases w with ⟨w, h1, h2⟩
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
motive : Word M → Sort u_4
empty : motive (Word.empty (M := M))
cons :
  (i : ι) →
    (m : M i) →
      (w : Word M) → (h1 : w.fstIdx (M := M) ≠ some i) → (h2 : m ≠ 1) → motive w → motive (Word.cons (M := M) m w h1 h2)
m : (i : ι) × M i
w : List ((i : ι) × M i)
ih :
  (h1 : ∀ l ∈ w, l.snd (β := fun (i : ι) ↦ M i) ≠ 1) →
    (h2 :
        List.IsChain (fun (l l' : (i : ι) × M i) ↦ l.fst (β := fun (i : ι) ↦ M i) ≠ l'.fst (β := fun (i : ι) ↦ M i))
          w) →
      motive (mk (M := M) w h1 h2)
h1 : ∀ l ∈ m :: w, l.snd (β := fun (i : ι) ↦ M i) ≠ 1
h2 :
  List.IsChain (fun (l l' : (i : ι) × M i) ↦ l.fst (β := fun (i : ι) ↦ M i) ≠ l'.fst (β := fun (i : ι) ↦ M i)) (m :: w)
⊢ motive (mk (M := M) (m :: w) h1 h2)
have cons₁ : fstIdx (M := M) (mk (M := M) w sorry sorry) ≠ some (m.fst (β := fun (i : ι) ↦ M i))
Tactic: refine cons m.1 m.2 ⟨w, fun _ hl => h1 _ (List.mem_cons_of_mem _ hl), h2.tail⟩ ?_ ?_ (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
motive : Word M → Sort u_4
empty : motive (Word.empty (M := M))
cons :
  (i : ι) →
    (m : M i) →
      (w : Word M) → (h1 : w.fstIdx (M := M) ≠ some i) → (h2 : m ≠ 1) → motive w → motive (Word.cons (M := M) m w h1 h2)
m : (i : ι) × M i
w : List ((i : ι) × M i)
ih :
  (h1 : ∀ l ∈ w, l.snd (β := fun (i : ι) ↦ M i) ≠ 1) →
    (h2 :
        List.IsChain (fun (l l' : (i : ι) × M i) ↦ l.fst (β := fun (i : ι) ↦ M i) ≠ l'.fst (β := fun (i : ι) ↦ M i))
          w) →
      motive (mk (M := M) w h1 h2)
h1 : ∀ l ∈ m :: w, l.snd (β := fun (i : ι) ↦ M i) ≠ 1
h2 :
  List.IsChain (fun (l l' : (i : ι) × M i) ↦ l.fst (β := fun (i : ι) ↦ M i) ≠ l'.fst (β := fun (i : ι) ↦ M i)) (m :: w)
cons₁ : fstIdx (M := M) (mk (M := M) w ⋯ ⋯) ≠ some (m.fst (β := fun (i : ι) ↦ M i))
⊢ motive (mk (M := M) (m :: w) h1 h2)
have cons₂ : m.snd (β := fun (i : ι) ↦ M i) ≠ 1
Tactic: refine cons m.1 m.2 ⟨w, fun _ hl => h1 _ (List.mem_cons_of_mem _ hl), h2.tail⟩ ?_ ?_ (ih _ _)
-- 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
motive : Word M → Sort u_4
empty : motive (Word.empty (M := M))
cons :
  (i : ι) →
    (m : M i) →
      (w : Word M) → (h1 : w.fstIdx (M := M) ≠ some i) → (h2 : m ≠ 1) → motive w → motive (Word.cons (M := M) m w h1 h2)
m : (i : ι) × M i
w : List ((i : ι) × M i)
ih :
  (h1 : ∀ l ∈ w, l.snd (β := fun (i : ι) ↦ M i) ≠ 1) →
    (h2 :
        List.IsChain (fun (l l' : (i : ι) × M i) ↦ l.fst (β := fun (i : ι) ↦ M i) ≠ l'.fst (β := fun (i : ι) ↦ M i))
          w) →
      motive (mk (M := M) w h1 h2)
h1 : ∀ l ∈ m :: w, l.snd (β := fun (i : ι) ↦ M i) ≠ 1
h2 :
  List.IsChain (fun (l l' : (i : ι) × M i) ↦ l.fst (β := fun (i : ι) ↦ M i) ≠ l'.fst (β := fun (i : ι) ↦ M i)) (m :: w)
⊢ fstIdx (M := M) (mk (M := M) w ⋯ ⋯) ≠ some (m.fst (β := fun (i : ι) ↦ M i))
have h2₁ : (∀ y ∈ w.head?, m.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
Tactic: rw [List.isChain_cons] at h2
-- 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
motive : Word M → Sort u_4
empty : motive (Word.empty (M := M))
cons :
  (i : ι) →
    (m : M i) →
      (w : Word M) → (h1 : w.fstIdx (M := M) ≠ some i) → (h2 : m ≠ 1) → motive w → motive (Word.cons (M := M) m w h1 h2)
m : (i : ι) × M i
w : List ((i : ι) × M i)
ih :
  (h1 : ∀ l ∈ w, l.snd (β := fun (i : ι) ↦ M i) ≠ 1) →
    (h2 :
        List.IsChain (fun (l l' : (i : ι) × M i) ↦ l.fst (β := fun (i : ι) ↦ M i) ≠ l'.fst (β := fun (i : ι) ↦ M i))
          w) →
      motive (mk (M := M) w h1 h2)
h1 : ∀ l ∈ m :: w, l.snd (β := fun (i : ι) ↦ M i) ≠ 1
h2_1 :
  List.IsChain (fun (l l' : (i : ι) × M i) ↦ l.fst (β := fun (i : ι) ↦ M i) ≠ l'.fst (β := fun (i : ι) ↦ M i)) (m :: w)
h2 :
  (∀ y ∈ w.head?, m.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
⊢ fstIdx (M := M) (mk (M := M) w ⋯ ⋯) ≠ some (m.fst (β := fun (i : ι) ↦ M i))
have cons₁ : ∀ (x : M (m.fst (β := fun (i : ι) ↦ M i))),
  ¬w.head? = some (Sigma.mk (β := fun (a : ι) ↦ M a) (m.fst (β := fun (i : ι) ↦ M i)) x)
Tactic: simp only [fstIdx, ne_eq, Option.map_eq_some_iff,
        Sigma.exists, exists_and_right, exists_eq_right, not_exists]