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)
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)
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)
have nil : (h1 : ∀ (l : (i : ι) × M i), Membership.mem (γ := List ((i : ι) × M i)) [] l → 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)) []) →
    motive (mk (M := M) [] h1 h2)
Tactic: induction w with
  | nil => exact empty
  | cons m w ih =>
    refine cons m.1 m.2 ⟨w, fun _ hl => h1 _ (List.mem_cons_of_mem _ hl), h2.tail⟩ ?_ ?_ (ih _ _)
    · rw [List.isChain_cons] at h2
      simp only [fstIdx, ne_eq, Option.map_eq_some_iff,
        Sigma.exists, exists_and_right, exists_eq_right, not_exists]
      intro m' hm'
      exact h2.1 _ hm' rfl
    · exact h1 _ List.mem_cons_self
Cleared hypotheses: w, h1, 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)
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
nil :
  (h1 : ∀ (l : (i : ι) × M i), Membership.mem (γ := List ((i : ι) × M i)) [] l → 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))
          []) →
      motive (mk (M := M) [] h1 h2)
⊢ motive (mk (M := M) w h1 h2)
have cons₁ : (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)
Tactic: induction w with
  | nil => exact empty
  | cons m w ih =>
    refine cons m.1 m.2 ⟨w, fun _ hl => h1 _ (List.mem_cons_of_mem _ hl), h2.tail⟩ ?_ ?_ (ih _ _)
    · rw [List.isChain_cons] at h2
      simp only [fstIdx, ne_eq, Option.map_eq_some_iff,
        Sigma.exists, exists_and_right, exists_eq_right, not_exists]
      intro m' hm'
      exact h2.1 _ hm' rfl
    · exact h1 _ List.mem_cons_self
Cleared hypotheses: w, h1, 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
inst_2 : DecidableEq ι
inst_3 : (i : ι) → DecidableEq (M i)
i : ι
w_1 : Word M
j : ι
m : M j
w : Word M
h1 : w.fstIdx (M := M) ≠ some j
h2 : m ≠ 1
x : { p : Pair M i // rcons (M := M) p = w }
ij : i = j
⊢ rcons (M := M) (i := i) (Pair.mk (M := M) (Eq.rec (motive := fun (x : ι) (h : j = x) ↦ M x) m ⋯) w ⋯) =
    cons (M := M) m w h1 h2
have subst : ∀ (m : M i) (h1 : w.fstIdx (M := M) ≠ some i) (h2 : m ≠ 1),
  rcons (M := M) (i := i) (Pair.mk (M := M) (Eq.rec (motive := fun (x : ι) (h : i = x) ↦ M x) m sorry) w sorry) =
    cons (M := M) m w h1 h2
Tactic: subst ij
Cleared hypotheses: j, m, h1, h2, ij
-- 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)
i j : ι
w : Word M
m : M i
⊢ Membership.mem (γ := List ((i : ι) × M i))
      (toList (M := M) (Pair.tail (M := M) (i := j) ((equivPair (M := M) j : (a : Word M) → Pair M j) w)) :
        List ((i : ι) × M i))
      (Sigma.mk (β := fun (i : ι) ↦ M i) i m) ↔
    Sigma.mk (β := fun (i : ι) ↦ M i) i m ∈ w.toList (M := M).tail ∨
      i ≠ j ∧ ∃ (h : w.toList (M := M) ≠ []), w.toList (M := M).head h = Sigma.mk (β := fun (i : ι) ↦ M i) i m
have simp : Membership.mem (γ := List ((i : ι) × M i))
    (toList (M := M)
      (Pair.tail (M := M) (i := j)
        (↑(consRecOn (M := M) (motive := fun (x : Word M) ↦ { p : Pair M j // rcons (M := M) p = x }) w
              (Subtype.mk (p := fun (p : Pair M j) ↦ rcons (M := M) p = empty (M := M))
                (Pair.mk (M := M) 1 (empty (M := M)) sorry) sorry)
              fun (j_1 : ι) (m : M j_1) (w : Word M) (h1 : ¬w.fstIdx (M := M) = some j_1) (h2 : ¬m = 1)
                (x : { p : Pair M j // rcons (M := M) p = w }) ↦
              if ij : j = j_1 then
                Subtype.mk (p := fun (p : Pair M j) ↦ rcons (M := M) p = cons (M := M) m w h1 h2)
                  (Pair.mk (M := M) (Eq.rec (motive := fun (x : ι) (h : j_1 = x) ↦ M x) m sorry) w sorry) sorry
              else
                Subtype.mk (p := fun (p : Pair M j) ↦ rcons (M := M) p = cons (M := M) m w h1 h2)
                  (Pair.mk (M := M) 1 (cons (M := M) m w h1 h2) sorry) sorry) :
          Pair M j)))
    (Sigma.mk (β := fun (i : ι) ↦ M i) i m) ↔
  Sigma.mk (β := fun (i : ι) ↦ M i) i m ∈ w.toList (M := M).tail ∨
    ¬i = j ∧ ∃ (h : ¬w.toList (M := M) = []), w.toList (M := M).head h = Sigma.mk (β := fun (i : ι) ↦ M i) i m
Tactic: simp only [equivPair, equivPairAux, ne_eq, Equiv.coe_fn_mk]
-- 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)
i j : ι
m : M i
k : ι
g : M k
tail : Word M
h1 : tail.fstIdx (M := M) ≠ some k
h2 : g ≠ 1
ih :
  Membership.mem (γ := List ((i : ι) × M i))
      (toList (M := M)
        (Pair.tail (M := M) (i := j)
          (↑(consRecOn (M := M) (motive := fun (x : Word M) ↦ { p : Pair M j // rcons (M := M) p = x }) tail
                (Subtype.mk (p := fun (p : Pair M j) ↦ rcons (M := M) p = empty (M := M))
                  (Pair.mk (M := M) 1 (empty (M := M)) ⋯) ⋯)
                fun (j_1 : ι) (m : M j_1) (w : Word M) (h1 : ¬w.fstIdx (M := M) = some j_1) (h2 : ¬m = 1)
                  (x : { p : Pair M j // rcons (M := M) p = w }) ↦
                if ij : j = j_1 then
                  Subtype.mk (p := fun (p : Pair M j) ↦ rcons (M := M) p = cons (M := M) m w h1 h2)
                    (Pair.mk (M := M) (Eq.rec (motive := fun (x : ι) (h : j_1 = x) ↦ M x) m ⋯) w ⋯) ⋯
                else
                  Subtype.mk (p := fun (p : Pair M j) ↦ rcons (M := M) p = cons (M := M) m w h1 h2)
                    (Pair.mk (M := M) 1 (cons (M := M) m w h1 h2) ⋯) ⋯) :
            Pair M j)))
      (Sigma.mk (β := fun (i : ι) ↦ M i) i m) ↔
    Sigma.mk (β := fun (i : ι) ↦ M i) i m ∈ tail.toList (M := M).tail ∨
      ¬i = j ∧ ∃ (h : ¬tail.toList (M := M) = []), tail.toList (M := M).head h = Sigma.mk (β := fun (i : ι) ↦ M i) i m
⊢ Membership.mem (γ := List ((i : ι) × M i))
      (toList (M := M)
        (Pair.tail (M := M) (i := j)
          (↑(if ij : j = k then
                Subtype.mk (p := fun (p : Pair M j) ↦ rcons (M := M) p = cons (M := M) g tail h1 h2)
                  (Pair.mk (M := M) (Eq.rec (motive := fun (x : ι) (h : k = x) ↦ M x) g ⋯) tail ⋯) ⋯
              else
                Subtype.mk (p := fun (p : Pair M j) ↦ rcons (M := M) p = cons (M := M) g tail h1 h2)
                  (Pair.mk (M := M) 1 (cons (M := M) g tail h1 h2) ⋯) ⋯) :
            Pair M j)))
      (Sigma.mk (β := fun (i : ι) ↦ M i) i m) ↔
    Sigma.mk (β := fun (i : ι) ↦ M i) i m ∈ (cons (M := M) g tail h1 h2).toList (M := M).tail ∨
      ¬i = j ∧
        ∃ (h : ¬(cons (M := M) g tail h1 h2).toList (M := M) = []),
          (cons (M := M) g tail h1 h2).toList (M := M).head h = Sigma.mk (β := fun (i : ι) ↦ M i) i m
have pos : ∀ (h : j = k),
  Sigma.mk (β := fun (i : ι) ↦ M i) i m ∈
      (↑(Subtype.mk (p := fun (p : Pair M j) ↦ rcons (M := M) p = cons (M := M) g tail h1 h2)
                    (Pair.mk (M := M) (Eq.rec (motive := fun (x : ι) (h : k = x) ↦ M x) g sorry) tail sorry) sorry) :
                Pair M j).tail
            (M := M).toList
        (M := M) ↔
    Sigma.mk (β := fun (i : ι) ↦ M i) i m ∈ (cons (M := M) g tail h1 h2).toList (M := M).tail ∨
      ¬i = j ∧
        ∃ (h : ¬(cons (M := M) g tail h1 h2).toList (M := M) = []),
          (cons (M := M) g tail h1 h2).toList (M := M).head h = Sigma.mk (β := fun (i : ι) ↦ M i) i m
Tactic: split_ifs with h
-- 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)
i j : ι
m : M i
k : ι
g : M k
tail : Word M
h1 : tail.fstIdx (M := M) ≠ some k
h2 : g ≠ 1
ih :
  Membership.mem (γ := List ((i : ι) × M i))
      (toList (M := M)
        (Pair.tail (M := M) (i := j)
          (↑(consRecOn (M := M) (motive := fun (x : Word M) ↦ { p : Pair M j // rcons (M := M) p = x }) tail
                (Subtype.mk (p := fun (p : Pair M j) ↦ rcons (M := M) p = empty (M := M))
                  (Pair.mk (M := M) 1 (empty (M := M)) ⋯) ⋯)
                fun (j_1 : ι) (m : M j_1) (w : Word M) (h1 : ¬w.fstIdx (M := M) = some j_1) (h2 : ¬m = 1)
                  (x : { p : Pair M j // rcons (M := M) p = w }) ↦
                if ij : j = j_1 then
                  Subtype.mk (p := fun (p : Pair M j) ↦ rcons (M := M) p = cons (M := M) m w h1 h2)
                    (Pair.mk (M := M) (Eq.rec (motive := fun (x : ι) (h : j_1 = x) ↦ M x) m ⋯) w ⋯) ⋯
                else
                  Subtype.mk (p := fun (p : Pair M j) ↦ rcons (M := M) p = cons (M := M) m w h1 h2)
                    (Pair.mk (M := M) 1 (cons (M := M) m w h1 h2) ⋯) ⋯) :
            Pair M j)))
      (Sigma.mk (β := fun (i : ι) ↦ M i) i m) ↔
    Sigma.mk (β := fun (i : ι) ↦ M i) i m ∈ tail.toList (M := M).tail ∨
      ¬i = j ∧ ∃ (h : ¬tail.toList (M := M) = []), tail.toList (M := M).head h = Sigma.mk (β := fun (i : ι) ↦ M i) i m
h : j = k
⊢ Sigma.mk (β := fun (i : ι) ↦ M i) i m ∈
      (↑(Subtype.mk (p := fun (p : Pair M j) ↦ rcons (M := M) p = cons (M := M) g tail h1 h2)
                    (Pair.mk (M := M) (Eq.rec (motive := fun (x : ι) (h : k = x) ↦ M x) g ⋯) tail ⋯) ⋯) :
                Pair M j).tail
            (M := M).toList
        (M := M) ↔
    Sigma.mk (β := fun (i : ι) ↦ M i) i m ∈ (cons (M := M) g tail h1 h2).toList (M := M).tail ∨
      ¬i = j ∧
        ∃ (h : ¬(cons (M := M) g tail h1 h2).toList (M := M) = []),
          (cons (M := M) g tail h1 h2).toList (M := M).head h = Sigma.mk (β := fun (i : ι) ↦ M i) i m
have pos : ∀ (g : M j) (h1 : tail.fstIdx (M := M) ≠ some j) (h2 : g ≠ 1),
  Sigma.mk (β := fun (i : ι) ↦ M i) i m ∈
      (↑(Subtype.mk (p := fun (p : Pair M j) ↦ rcons (M := M) p = cons (M := M) g tail h1 h2)
                    (Pair.mk (M := M) (Eq.rec (motive := fun (x : ι) (h : j = x) ↦ M x) g sorry) tail sorry) sorry) :
                Pair M j).tail
            (M := M).toList
        (M := M) ↔
    Sigma.mk (β := fun (i : ι) ↦ M i) i m ∈ (cons (M := M) g tail h1 h2).toList (M := M).tail ∨
      ¬i = j ∧
        ∃ (h : ¬(cons (M := M) g tail h1 h2).toList (M := M) = []),
          (cons (M := M) g tail h1 h2).toList (M := M).head h = Sigma.mk (β := fun (i : ι) ↦ M i) i m
Tactic: subst k
Cleared hypotheses: k, g, h1, h2, h
-- 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)
i j : ι
m : M i
tail : Word M
ih :
  Membership.mem (γ := List ((i : ι) × M i))
      (toList (M := M)
        (Pair.tail (M := M) (i := j)
          (↑(consRecOn (M := M) (motive := fun (x : Word M) ↦ { p : Pair M j // rcons (M := M) p = x }) tail
                (Subtype.mk (p := fun (p : Pair M j) ↦ rcons (M := M) p = empty (M := M))
                  (Pair.mk (M := M) 1 (empty (M := M)) ⋯) ⋯)
                fun (j_1 : ι) (m : M j_1) (w : Word M) (h1 : ¬w.fstIdx (M := M) = some j_1) (h2 : ¬m = 1)
                  (x : { p : Pair M j // rcons (M := M) p = w }) ↦
                if ij : j = j_1 then
                  Subtype.mk (p := fun (p : Pair M j) ↦ rcons (M := M) p = cons (M := M) m w h1 h2)
                    (Pair.mk (M := M) (Eq.rec (motive := fun (x : ι) (h : j_1 = x) ↦ M x) m ⋯) w ⋯) ⋯
                else
                  Subtype.mk (p := fun (p : Pair M j) ↦ rcons (M := M) p = cons (M := M) m w h1 h2)
                    (Pair.mk (M := M) 1 (cons (M := M) m w h1 h2) ⋯) ⋯) :
            Pair M j)))
      (Sigma.mk (β := fun (i : ι) ↦ M i) i m) ↔
    Sigma.mk (β := fun (i : ι) ↦ M i) i m ∈ tail.toList (M := M).tail ∨
      ¬i = j ∧ ∃ (h : ¬tail.toList (M := M) = []), tail.toList (M := M).head h = Sigma.mk (β := fun (i : ι) ↦ M i) i m
g : M j
h1 : tail.fstIdx (M := M) ≠ some j
h2 : g ≠ 1
⊢ Sigma.mk (β := fun (i : ι) ↦ M i) i m ∈
      (↑(Subtype.mk (p := fun (p : Pair M j) ↦ rcons (M := M) p = cons (M := M) g tail h1 h2)
                    (Pair.mk (M := M) (Eq.rec (motive := fun (x : ι) (h : j = x) ↦ M x) g ⋯) tail ⋯) ⋯) :
                Pair M j).tail
            (M := M).toList
        (M := M) ↔
    Sigma.mk (β := fun (i : ι) ↦ M i) i m ∈ (cons (M := M) g tail h1 h2).toList (M := M).tail ∨
      ¬i = j ∧
        ∃ (h : ¬(cons (M := M) g tail h1 h2).toList (M := M) = []),
          (cons (M := M) g tail h1 h2).toList (M := M).head h = Sigma.mk (β := fun (i : ι) ↦ M i) i m
have pos : ∀ (hij : j = i),
  Sigma.mk (β := fun (i : ι) ↦ M i) i m ∈
      (↑(Subtype.mk (p := fun (p : Pair M j) ↦ rcons (M := M) p = cons (M := M) g tail h1 h2)
                    (Pair.mk (M := M) (Eq.rec (motive := fun (x : ι) (h : j = x) ↦ M x) g sorry) tail sorry) sorry) :
                Pair M j).tail
            (M := M).toList
        (M := M) ↔
    Sigma.mk (β := fun (i : ι) ↦ M i) i m ∈ (cons (M := M) g tail h1 h2).toList (M := M).tail ∨
      ¬i = j ∧
        ∃ (h : ¬(cons (M := M) g tail h1 h2).toList (M := M) = []),
          (cons (M := M) g tail h1 h2).toList (M := M).head h = Sigma.mk (β := fun (i : ι) ↦ M i) i m
Tactic: by_cases hij : j = i
-- 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)
i j : ι
m : M i
k : ι
g : M k
tail : Word M
h1 : tail.fstIdx (M := M) ≠ some k
h2 : g ≠ 1
ih :
  Membership.mem (γ := List ((i : ι) × M i))
      (toList (M := M)
        (Pair.tail (M := M) (i := j)
          (↑(consRecOn (M := M) (motive := fun (x : Word M) ↦ { p : Pair M j // rcons (M := M) p = x }) tail
                (Subtype.mk (p := fun (p : Pair M j) ↦ rcons (M := M) p = empty (M := M))
                  (Pair.mk (M := M) 1 (empty (M := M)) ⋯) ⋯)
                fun (j_1 : ι) (m : M j_1) (w : Word M) (h1 : ¬w.fstIdx (M := M) = some j_1) (h2 : ¬m = 1)
                  (x : { p : Pair M j // rcons (M := M) p = w }) ↦
                if ij : j = j_1 then
                  Subtype.mk (p := fun (p : Pair M j) ↦ rcons (M := M) p = cons (M := M) m w h1 h2)
                    (Pair.mk (M := M) (Eq.rec (motive := fun (x : ι) (h : j_1 = x) ↦ M x) m ⋯) w ⋯) ⋯
                else
                  Subtype.mk (p := fun (p : Pair M j) ↦ rcons (M := M) p = cons (M := M) m w h1 h2)
                    (Pair.mk (M := M) 1 (cons (M := M) m w h1 h2) ⋯) ⋯) :
            Pair M j)))
      (Sigma.mk (β := fun (i : ι) ↦ M i) i m) ↔
    Sigma.mk (β := fun (i : ι) ↦ M i) i m ∈ tail.toList (M := M).tail ∨
      ¬i = j ∧ ∃ (h : ¬tail.toList (M := M) = []), tail.toList (M := M).head h = Sigma.mk (β := fun (i : ι) ↦ M i) i m
h : ¬j = k
⊢ Sigma.mk (β := fun (i : ι) ↦ M i) i m ∈
      (↑(Subtype.mk (p := fun (p : Pair M j) ↦ rcons (M := M) p = cons (M := M) g tail h1 h2)
                    (Pair.mk (M := M) 1 (cons (M := M) g tail h1 h2) ⋯) ⋯) :
                Pair M j).tail
            (M := M).toList
        (M := M) ↔
    Sigma.mk (β := fun (i : ι) ↦ M i) i m ∈ (cons (M := M) g tail h1 h2).toList (M := M).tail ∨
      ¬i = j ∧
        ∃ (h : ¬(cons (M := M) g tail h1 h2).toList (M := M) = []),
          (cons (M := M) g tail h1 h2).toList (M := M).head h = Sigma.mk (β := fun (i : ι) ↦ M i) i m
have pos : ∀ (hik : i = k),
  Sigma.mk (β := fun (i : ι) ↦ M i) i m ∈
      (↑(Subtype.mk (p := fun (p : Pair M j) ↦ rcons (M := M) p = cons (M := M) g tail h1 h2)
                    (Pair.mk (M := M) 1 (cons (M := M) g tail h1 h2) sorry) sorry) :
                Pair M j).tail
            (M := M).toList
        (M := M) ↔
    Sigma.mk (β := fun (i : ι) ↦ M i) i m ∈ (cons (M := M) g tail h1 h2).toList (M := M).tail ∨
      ¬i = j ∧
        ∃ (h : ¬(cons (M := M) g tail h1 h2).toList (M := M) = []),
          (cons (M := M) g tail h1 h2).toList (M := M).head h = Sigma.mk (β := fun (i : ι) ↦ M i) i m
Tactic: by_cases hik : i = k
-- 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)
i j : ι
w : Word M
m : M i
⊢ Membership.mem (γ := List ((i : ι) × M i))
      (toList (M := M)
        (Pair.tail (M := M) (i := j)
          (↑(consRecOn (M := M) (motive := fun (x : Word M) ↦ { p : Pair M j // rcons (M := M) p = x }) w
                (Subtype.mk (p := fun (p : Pair M j) ↦ rcons (M := M) p = empty (M := M))
                  (Pair.mk (M := M) 1 (empty (M := M)) ⋯) ⋯)
                fun (j_1 : ι) (m : M j_1) (w : Word M) (h1 : ¬w.fstIdx (M := M) = some j_1) (h2 : ¬m = 1)
                  (x : { p : Pair M j // rcons (M := M) p = w }) ↦
                if ij : j = j_1 then
                  Subtype.mk (p := fun (p : Pair M j) ↦ rcons (M := M) p = cons (M := M) m w h1 h2)
                    (Pair.mk (M := M) (Eq.rec (motive := fun (x : ι) (h : j_1 = x) ↦ M x) m ⋯) w ⋯) ⋯
                else
                  Subtype.mk (p := fun (p : Pair M j) ↦ rcons (M := M) p = cons (M := M) m w h1 h2)
                    (Pair.mk (M := M) 1 (cons (M := M) m w h1 h2) ⋯) ⋯) :
            Pair M j)))
      (Sigma.mk (β := fun (i : ι) ↦ M i) i m) ↔
    Sigma.mk (β := fun (i : ι) ↦ M i) i m ∈ w.toList (M := M).tail ∨
      ¬i = j ∧ ∃ (h : ¬w.toList (M := M) = []), w.toList (M := M).head h = Sigma.mk (β := fun (i : ι) ↦ M i) i m
have empty : Membership.mem (γ := List ((i : ι) × M i))
    (toList (M := M)
      (Pair.tail (M := M) (i := j)
        (↑(consRecOn (M := M) (motive := fun (x : Word M) ↦ { p : Pair M j // rcons (M := M) p = x }) (empty (M := M))
              (Subtype.mk (p := fun (p : Pair M j) ↦ rcons (M := M) p = empty (M := M))
                (Pair.mk (M := M) 1 (empty (M := M)) sorry) sorry)
              fun (j_1 : ι) (m : M j_1) (w : Word M) (h1 : ¬w.fstIdx (M := M) = some j_1) (h2 : ¬m = 1)
                (x : { p : Pair M j // rcons (M := M) p = w }) ↦
              if ij : j = j_1 then
                Subtype.mk (p := fun (p : Pair M j) ↦ rcons (M := M) p = cons (M := M) m w h1 h2)
                  (Pair.mk (M := M) (Eq.rec (motive := fun (x : ι) (h : j_1 = x) ↦ M x) m sorry) w sorry) sorry
              else
                Subtype.mk (p := fun (p : Pair M j) ↦ rcons (M := M) p = cons (M := M) m w h1 h2)
                  (Pair.mk (M := M) 1 (cons (M := M) m w h1 h2) sorry) sorry) :
          Pair M j)))
    (Sigma.mk (β := fun (i : ι) ↦ M i) i m) ↔
  Membership.mem (γ := List ((i : ι) × M i)) (List.tail (toList (M := M) (empty (M := M))))
      (Sigma.mk (β := fun (i : ι) ↦ M i) i m) ∨
    ¬i = j ∧
      ∃ (h : ¬Eq (α := List ((i : ι) × M i)) (toList (M := M) (empty (M := M))) []),
        List.head (toList (M := M) (empty (M := M))) h = Sigma.mk (β := fun (i : ι) ↦ M i) i m
Tactic: induction w using consRecOn with
  | empty => simp
  | cons k g tail h1 h2 ih =>
    simp only [consRecOn_cons]
    split_ifs with h
    · subst k
      by_cases hij : j = i <;> simp_all
    · by_cases hik : i = k
      · subst i; simp_all [@eq_comm _ m g, @eq_comm _ k j, or_comm]
      · simp [hik, Ne.symm hik]
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)
inst_1 : DecidableEq ι
inst_2 : (i : ι) → DecidableEq (M i)
i j : ι
w : Word M
m : M i
⊢ Membership.mem (γ := List ((i : ι) × M i))
      (toList (M := M) (Pair.tail (M := M) (i := j) ((equivPair (M := M) j : (a : Word M) → Pair M j) w)) :
        List ((i : ι) × M i))
      (Sigma.mk (β := fun (i : ι) ↦ M i) i m) →
    Sigma.mk (β := fun (i : ι) ↦ M i) i m ∈ w.toList (M := M)
have rw : (Sigma.mk (β := fun (i : ι) ↦ M i) i m ∈ w.toList (M := M).tail ∨
    i ≠ j ∧ ∃ (h : w.toList (M := M) ≠ []), w.toList (M := M).head h = Sigma.mk (β := fun (i : ι) ↦ M i) i m) →
  Sigma.mk (β := fun (i : ι) ↦ M i) i m ∈ w.toList (M := M)
Tactic: rw [mem_equivPair_tail_iff]
-- 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)
i j : ι
w : Word M
m : M i
h : i ≠ j ∧ ∃ (h : w.toList (M := M) ≠ []), w.toList (M := M).head h = Sigma.mk (β := fun (i : ι) ↦ M i) i m
⊢ Sigma.mk (β := fun (i : ι) ↦ M i) i m ∈ w.toList (M := M)
have inr : ∀ (h : i ≠ j ∧ ∃ (h : w.toList (M := M) ≠ []), w.toList (M := M).head h = Sigma.mk (β := fun (i : ι) ↦ M i) i m),
  Sigma.mk (β := fun (i : ι) ↦ M i) i m ∈ w.toList (M := M)
Tactic: revert 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)
inst_1 : DecidableEq ι
inst_2 : (i : ι) → DecidableEq (M i)
i j : ι
w : Word M
m : M i
⊢ ∀ (h : i ≠ j ∧ ∃ (h : w.toList (M := M) ≠ []), w.toList (M := M).head h = Sigma.mk (β := fun (i : ι) ↦ M i) i m),
    Sigma.mk (β := fun (i : ι) ↦ M i) i m ∈ w.toList (M := M)
have inr : ∀ (h : i ≠ j ∧ ∃ (h : Ne (α := List ((i : ι) × M i)) [] []), List.head [] h = Sigma.mk (β := fun (i : ι) ↦ M i) i m),
  Membership.mem (γ := List ((i : ι) × M i)) [] (Sigma.mk (β := fun (i : ι) ↦ M i) i m)
Tactic: cases w.toList
-- 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)
i j : ι
w : Word M
m : M i
inr :
  ∀ (h : i ≠ j ∧ ∃ (h : Ne (α := List ((i : ι) × M i)) [] []), List.head [] h = Sigma.mk (β := fun (i : ι) ↦ M i) i m),
    Membership.mem (γ := List ((i : ι) × M i)) [] (Sigma.mk (β := fun (i : ι) ↦ M i) i m)
⊢ ∀ (h : i ≠ j ∧ ∃ (h : w.toList (M := M) ≠ []), w.toList (M := M).head h = Sigma.mk (β := fun (i : ι) ↦ M i) i m),
    Sigma.mk (β := fun (i : ι) ↦ M i) i m ∈ w.toList (M := M)
have inr₁ : ∀ (head : (i : ι) × M i) (tail : List ((i : ι) × M i))
  (h : i ≠ j ∧ ∃ (h : head :: tail ≠ []), (head :: tail).head h = Sigma.mk (β := fun (i : ι) ↦ M i) i m),
  Sigma.mk (β := fun (i : ι) ↦ M i) i m ∈ head :: tail
Tactic: cases w.toList