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 : (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)
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'
⊢ Pair.mk (M := M) m w h = Pair.mk (M := M) m' w' h'

Tactic:
rcases this with ⟨rfl, h⟩

Premises used: rfl
-- Module: Mathlib.GroupTheory.CoprodI
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
neg : w = w'
⊢ Pair.mk (M := M) m w h_1 = Pair.mk (M := M) m w' h'

Tactic:
congr
-- Module: Mathlib.GroupTheory.CoprodI
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
⊢ w = w'

Tactic:
Word.ext h

Premises used: Monoid.CoprodI.Word.ext
-- Module: Mathlib.GroupTheory.CoprodI
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
⊢ w = w'

Tactic:
exact Word.ext h

Premises used: Monoid.CoprodI.Word.ext
-- Module: Mathlib.GroupTheory.CoprodI
Goal:
ι : Type u_1
M : ι → Type u_2
inst : (i : ι) → Monoid (M i)
inst_1 : (i : ι) → DecidableEq (M i)
i j : ι
p : Pair M i
m : M j
⊢ Membership.mem (γ := List ((i : ι) × M i))
      (toList (M := M)
        (if h : p.head (M := M) = 1 then p.tail (M := M)
        else
          mk (M := M) (Sigma.mk (β := fun (i : ι) ↦ M i) i (p.head (M := M)) :: p.tail (M := M).toList (M := M)) ⋯ ⋯))
      (Sigma.mk (β := fun (i : ι) ↦ M i) j m) ↔
    Sigma.mk (β := fun (i : ι) ↦ M i) j m ∈ p.tail (M := M).toList (M := M) ∨
      ¬m = 1 ∧ ∃ (h : i = j), m = Eq.rec (motive := fun (x : ι) (h : i = x) ↦ M x) (p.head (M := M)) h

Tactic:
grind
-- 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
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)
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)
⊢ motive w

Tactic:
rcases w with ⟨w, h1, h2⟩
-- 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
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)
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:
exact 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
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))
cons₂ : m.snd (β := fun (i : ι) ↦ M i) ≠ 1
⊢ motive (mk (M := M) (m :: w) h1 h2)

Tactic:
refine cons m.1 m.2 ⟨w, fun _ hl => h1 _ (List.mem_cons_of_mem _ hl), h2.tail⟩ ?_ ?_ (ih _ _)

Premises used: List.mem_cons_of_mem, Sigma.fst, List.IsChain.tail, Monoid.CoprodI.Word.mk, Sigma.snd
-- 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
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)
⊢ (∀ 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

Premises used: List.isChain_cons
-- 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
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
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)
⊢ fstIdx (M := M) (mk (M := M) w ⋯ ⋯) ≠ some (m.fst (β := fun (i : ι) ↦ M i))

Tactic:
simp only [fstIdx, ne_eq, Option.map_eq_some_iff,
        Sigma.exists, exists_and_right, exists_eq_right, not_exists]

Premises used: Monoid.CoprodI.Word.fstIdx, Sigma.exists, not_exists, exists_eq_right, exists_and_right, ne_eq, Option.map_eq_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
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
m' : M (m.fst (β := fun (i : ι) ↦ M i))
hm' : w.head? = some (Sigma.mk (β := fun (a : ι) ↦ M a) (m.fst (β := fun (i : ι) ↦ M i)) m')
⊢ False

Tactic:
h2.1 _ hm' rfl

Premises used: And.left, rfl
-- 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
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
m' : M (m.fst (β := fun (i : ι) ↦ M i))
hm' : w.head? = some (Sigma.mk (β := fun (a : ι) ↦ M a) (m.fst (β := fun (i : ι) ↦ M i)) m')
⊢ False

Tactic:
exact h2.1 _ hm' rfl

Premises used: And.left, rfl
-- 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
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)
⊢ m.snd (β := fun (i : ι) ↦ M i) ≠ 1

Tactic:
h1 _ List.mem_cons_self

Premises used: List.mem_cons_self
-- 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
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)
⊢ m.snd (β := fun (i : ι) ↦ M i) ≠ 1

Tactic:
exact h1 _ List.mem_cons_self

Premises used: List.mem_cons_self
-- 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
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)
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)
⊢ motive (mk (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

Premises used: Monoid.CoprodI.Word.fstIdx, Sigma.exists, not_exists, exists_eq_right, exists_and_right, ne_eq, List.isChain_cons, Option.map_eq_some_iff
-- Module: Mathlib.GroupTheory.CoprodI
Goal:
ι : Type u_1
M : ι → Type u_2
inst : (i : ι) → Monoid (M i)
motive : Word M → Sort u_4
h_empty : motive (empty (M := M))
h_cons :
  (i : ι) →
    (m : M i) →
      (w : Word M) → (h1 : w.fstIdx (M := M) ≠ some i) → (h2 : m ≠ 1) → motive w → motive (cons (M := M) m w h1 h2)
⊢ consRecOn (M := M) (motive := fun (x : Word M) ↦ motive x) (empty (M := M)) h_empty h_cons = h_empty

Tactic:
rfl

Premises used: rfl, Monoid.CoprodI.Word.consRecOn
-- Module: Mathlib.GroupTheory.CoprodI
Goal:
ι : Type u_1
M : ι → Type u_2
inst : (i : ι) → Monoid (M i)
motive : Word M → Sort u_4
i : ι
m : M i
w : Word M
h1 : w.fstIdx (M := M) ≠ some i
h2 : m ≠ 1
h_empty : motive (empty (M := M))
h_cons :
  (i : ι) →
    (m : M i) →
      (w : Word M) → (h1 : w.fstIdx (M := M) ≠ some i) → (h2 : m ≠ 1) → motive w → motive (cons (M := M) m w h1 h2)
⊢ consRecOn (M := M) (motive := fun (x : Word M) ↦ motive x) (cons (M := M) m w h1 h2) h_empty h_cons =
    h_cons i m w h1 h2 (consRecOn (M := M) (motive := fun (x : Word M) ↦ motive x) w h_empty h_cons)

Tactic:
rfl

Premises used: List.tail, rfl, Monoid.CoprodI.Word.consRecOn
-- 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 : ι
w : Word M
⊢ fstIdx (M := M) (empty (M := M)) ≠ some i

Tactic:
simp [fstIdx, empty]

Premises used: Monoid.CoprodI.Word.fstIdx, Monoid.CoprodI.Word.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 : ι
w : Word M
⊢ Eq (α := Word M) (rcons (M := M) (i := i) (Pair.mk (M := M) 1 (empty (M := M)) ⋯)) (empty (M := M))

Tactic:
simp [rcons]

Premises used: Monoid.CoprodI.Word.rcons
-- 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 : ι
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
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 ⋯) w ⋯) =
      cons (M := M) m w h1 h2
⊢ 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

Tactic:
subst ij
-- 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 : ι
w_1 w : Word M
x : { p : Pair M i // rcons (M := M) p = w }
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 ⋯) w ⋯) =
    cons (M := M) m w h1 h2

Tactic:
simp [rcons, h2]

Premises used: Monoid.CoprodI.Word.rcons
-- 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 : ι
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
⊢ (cons (M := M) m w h1 h2).fstIdx (M := M) ≠ some i

Tactic:
simp [cons, fstIdx, Ne.symm ij]

Premises used: Monoid.CoprodI.Word.fstIdx, Ne.symm, Monoid.CoprodI.Word.cons
-- 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 : ι
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) (Pair.mk (M := M) 1 (cons (M := M) m w h1 h2) ⋯) = cons (M := M) m w h1 h2

Tactic:
simp [rcons]

Premises used: Monoid.CoprodI.Word.rcons
-- 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)
i : ι
p : Pair M i
⊢ (Equiv.symm (equivPair (M := M) i) : (a : Pair M i) → Word M) p = rcons (M := M) p

Tactic:
rfl

Premises used: dite, Monoid.CoprodI.Word.rcons, rfl
-- 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)
i : ι
w : Word M
h : w.fstIdx (M := M) ≠ some i
⊢ (equivPair (M := M) i : (a : Word M) → Pair M i) w = Pair.mk (M := M) 1 w h

Tactic:
(equivPair i).apply_eq_iff_eq_symm_apply.mpr <| Eq.symm (dif_pos rfl)

Premises used: Iff.mpr, dif_pos, Monoid.CoprodI.Word.equivPair, Eq.symm, rfl, Equiv.apply_eq_iff_eq_symm_apply
-- 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)
i j : ι
w : Word M
m : M i
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)) ⋯) ⋯)
                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
⊢ 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

Tactic:
simp only [equivPair, equivPairAux, ne_eq, Equiv.coe_fn_mk]

Premises used: Monoid.CoprodI.Word.equivPair, ne_eq, Equiv.coe_fn_mk, _private.0.Monoid.CoprodI.Word.equivPairAux
-- 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)
i j : ι
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 }) (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)) ⋯) ⋯)
                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) ↔
    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:
simp