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)
w : Word M
hnil : ¬w.toList (M := M) = []
m₂ w_1 : M ((w.toList (M := M).head hnil).fst (β := fun (i : ι) ↦ M i))
hw :
  Sigma.mk (β := fun (i : ι) ↦ M i) ((w.toList (M := M).head hnil).fst (β := fun (i : ι) ↦ M i)) (m₂ * w_1) ∉
    w.toList (M := M).tail
hm1 : ¬m₂ * w_1 = 1
h : (w.toList (M := M).head hnil).snd (β := fun (i : ι) ↦ M i) = w_1
pos :
  ∀
    (hw :
      Sigma.mk (β := fun (i : ι) ↦ M i) ((w.toList (M := M).head hnil).fst (β := fun (i : ι) ↦ M i))
          (m₂ * (w.toList (M := M).head hnil).snd (β := fun (i : ι) ↦ M i)) ∉
        w.toList (M := M).tail)
    (hm1 : ¬m₂ * (w.toList (M := M).head hnil).snd (β := fun (i : ι) ↦ M i) = 1),
    m₂ * (w.toList (M := M).head hnil).snd (β := fun (i : ι) ↦ M i) =
      m₂ * (w.toList (M := M).head ⋯).snd (β := fun (i : ι) ↦ M i)
⊢ m₂ * w_1 = m₂ * (w.toList (M := M).head ⋯).snd (β := fun (i : ι) ↦ M i)

Tactic:
subst h
-- 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)
w : Word M
hnil : ¬w.toList (M := M) = []
m₂ : M ((w.toList (M := M).head hnil).fst (β := fun (i : ι) ↦ M i))
hw :
  Sigma.mk (β := fun (i : ι) ↦ M i) ((w.toList (M := M).head hnil).fst (β := fun (i : ι) ↦ M i))
      (m₂ * (w.toList (M := M).head hnil).snd (β := fun (i : ι) ↦ M i)) ∉
    w.toList (M := M).tail
hm1 : ¬m₂ * (w.toList (M := M).head hnil).snd (β := fun (i : ι) ↦ M i) = 1
⊢ m₂ * (w.toList (M := M).head hnil).snd (β := fun (i : ι) ↦ M i) =
    m₂ * (w.toList (M := M).head ⋯).snd (β := fun (i : ι) ↦ M i)

Tactic:
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)
w : Word M
hnil : ¬w.toList (M := M) = []
m₂ m₁ : M ((w.toList (M := M).head hnil).fst (β := fun (i : ι) ↦ M i))
hw :
  Sigma.mk (β := fun (i : ι) ↦ M i) ((w.toList (M := M).head hnil).fst (β := fun (i : ι) ↦ M i)) m₁ ∉
    w.toList (M := M).tail
hm1 : ¬m₁ = 1
hm' : ¬w.fstIdx (M := M) = some ((w.toList (M := M).head hnil).fst (β := fun (i : ι) ↦ M i)) ∧ m₁ = m₂
⊢ (∀ (x : M ((w.toList (M := M).head hnil).fst (β := fun (i : ι) ↦ M i))),
      ¬w.toList (M := M).head? =
          some (Sigma.mk (β := fun (a : ι) ↦ M a) ((w.toList (M := M).head hnil).fst (β := fun (i : ι) ↦ M i)) x)) ∧
    m₁ = m₂

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

Premises used: Monoid.CoprodI.Word.fstIdx, Sigma.exists, not_exists, exists_eq_right, exists_and_right, Option.map_eq_some_iff
-- 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)
w : Word M
hnil : ¬w.toList (M := M) = []
m₂ m₁ : M ((w.toList (M := M).head hnil).fst (β := fun (i : ι) ↦ M i))
hw :
  Sigma.mk (β := fun (i : ι) ↦ M i) ((w.toList (M := M).head hnil).fst (β := fun (i : ι) ↦ M i)) m₁ ∉
    w.toList (M := M).tail
hm1 : ¬m₁ = 1
hm' :
  (∀ (x : M ((w.toList (M := M).head hnil).fst (β := fun (i : ι) ↦ M i))),
      ¬w.toList (M := M).head? =
          some (Sigma.mk (β := fun (a : ι) ↦ M a) ((w.toList (M := M).head hnil).fst (β := fun (i : ι) ↦ M i)) x)) ∧
    m₁ = m₂
rw :
  some (w.toList (M := M).head hnil) =
    some
      (Sigma.mk (β := fun (a : ι) ↦ M a) ((w.toList (M := M).head hnil).fst (β := fun (i : ι) ↦ M i))
        ((w.toList (M := M).head hnil).snd (β := fun (i : ι) ↦ M i)))
rw₁ : w.toList (M := M) ≠ []
rw₂ :
  some (w.toList (M := M).head hnil) =
    some
      (Sigma.mk (β := fun (a : ι) ↦ M a) ((w.toList (M := M).head hnil).fst (β := fun (i : ι) ↦ M i))
        ((w.toList (M := M).head hnil).snd (β := fun (i : ι) ↦ M i)))
rw₃ : w.toList (M := M) ≠ []
⊢ w.toList (M := M).head? =
    some
      (Sigma.mk (β := fun (a : ι) ↦ M a) ((w.toList (M := M).head hnil).fst (β := fun (i : ι) ↦ M i))
        ((w.toList (M := M).head hnil).snd (β := fun (i : ι) ↦ M i)))

Tactic:
rw [List.head?_eq_some_head]

Premises used: List.head?_eq_some_head
-- 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)
w : Word M
hnil : ¬w.toList (M := M) = []
m₂ m₁ : M ((w.toList (M := M).head hnil).fst (β := fun (i : ι) ↦ M i))
hw :
  Sigma.mk (β := fun (i : ι) ↦ M i) ((w.toList (M := M).head hnil).fst (β := fun (i : ι) ↦ M i)) m₁ ∉
    w.toList (M := M).tail
hm1 : ¬m₁ = 1
hm' :
  (∀ (x : M ((w.toList (M := M).head hnil).fst (β := fun (i : ι) ↦ M i))),
      ¬w.toList (M := M).head? =
          some (Sigma.mk (β := fun (a : ι) ↦ M a) ((w.toList (M := M).head hnil).fst (β := fun (i : ι) ↦ M i)) x)) ∧
    m₁ = m₂
⊢ m₁ = m₂ * (w.toList (M := M).head ⋯).snd (β := fun (i : ι) ↦ M i)

Tactic:
exact (hm'.1 (w.toList.head hnil).2 (by rw [List.head?_eq_some_head])).elim

Premises used: List.head, False.elim, Monoid.CoprodI.Word.toList, And.left, Sigma.snd
-- 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)
j : ι
m₂ : M j
w : Word M
m₁ : M j
hw : Sigma.mk (β := fun (i : ι) ↦ M i) j m₁ ∉ w.toList (M := M).tail
hm1 : ¬m₁ = 1
h : ¬∃ (h : ¬w.toList (M := M) = []), (w.toList (M := M).head h).fst (β := fun (i : ι) ↦ M i) = j
neg :
  ∀ (h : ¬∃ (h : ¬w.toList (M := M) = []), (w.toList (M := M).head h).fst (β := fun (i : ι) ↦ M i) = j),
    m₁ = m₂ * 1 ↔
      (∃ (m' : M j), w.toList (M := M).head? = some (Sigma.mk (β := fun (i : ι) ↦ M i) j m') ∧ m₁ = m₂ * m') ∨
        ¬w.fstIdx (M := M) = some j ∧ m₁ = m₂
⊢ m₁ = m₂ * 1 ↔
    (∃ (m' : M j), w.toList (M := M).head? = some (Sigma.mk (β := fun (i : ι) ↦ M i) j m') ∧ m₁ = m₂ * m') ∨
      ¬w.fstIdx (M := M) = some j ∧ m₁ = m₂

Tactic:
revert h
-- 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)
j : ι
m₂ : M j
w : Word M
m₁ : M j
hw : Sigma.mk (β := fun (i : ι) ↦ M i) j m₁ ∉ w.toList (M := M).tail
hm1 : ¬m₁ = 1
neg :
  ∀ (h : ¬∃ (h : ¬Eq (α := List ((i : ι) × M i)) [] []), (List.head [] h).fst (β := fun (i : ι) ↦ M i) = j),
    m₁ = m₂ * 1 ↔
      (∃ (m' : M j), List.head? [] = some (Sigma.mk (β := fun (i : ι) ↦ M i) j m') ∧ m₁ = m₂ * m') ∨
        ¬Option.map (α := (i : ι) × M i) (Sigma.fst (β := fun (i : ι) ↦ M i)) (List.head? []) = some j ∧ m₁ = m₂
neg₁ :
  ∀ (head : (i : ι) × M i) (tail : List ((i : ι) × M i))
    (h : ¬∃ (h : ¬head :: tail = []), ((head :: tail).head h).fst (β := fun (i : ι) ↦ M i) = j),
    m₁ = m₂ * 1 ↔
      (∃ (m' : M j), (head :: tail).head? = some (Sigma.mk (β := fun (i : ι) ↦ M i) j m') ∧ m₁ = m₂ * m') ∨
        ¬Option.map (Sigma.fst (β := fun (i : ι) ↦ M i)) (head :: tail).head? = some j ∧ m₁ = m₂
⊢ ∀ (h : ¬∃ (h : ¬w.toList (M := M) = []), (w.toList (M := M).head h).fst (β := fun (i : ι) ↦ M i) = j),
    m₁ = m₂ * 1 ↔
      (∃ (m' : M j), w.toList (M := M).head? = some (Sigma.mk (β := fun (i : ι) ↦ M i) j m') ∧ m₁ = m₂ * m') ∨
        ¬Option.map (Sigma.fst (β := fun (i : ι) ↦ M i)) w.toList (M := M).head? = some j ∧ m₁ = m₂

Tactic:
cases w.toList

Premises used: Monoid.CoprodI.Word.toList
-- 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)
j : ι
m₂ : M j
w : Word M
m₁ : M j
hw : Sigma.mk (β := fun (i : ι) ↦ M i) j m₁ ∉ w.toList (M := M).tail
hm1 : ¬m₁ = 1
⊢ ∀ (h : ¬∃ (h : ¬Eq (α := List ((i : ι) × M i)) [] []), (List.head [] h).fst (β := fun (i : ι) ↦ M i) = j),
    m₁ = m₂ * 1 ↔
      (∃ (m' : M j), List.head? [] = some (Sigma.mk (β := fun (i : ι) ↦ M i) j m') ∧ m₁ = m₂ * m') ∨
        ¬Option.map (α := (i : ι) × M i) (Sigma.fst (β := fun (i : ι) ↦ M i)) (List.head? []) = some j ∧ m₁ = m₂

Tactic:
simp
-- 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)
j : ι
m₂ : M j
w : Word M
m₁ : M j
hw : Sigma.mk (β := fun (i : ι) ↦ M i) j m₁ ∉ w.toList (M := M).tail
hm1 : ¬m₁ = 1
head : (i : ι) × M i
tail : List ((i : ι) × M i)
⊢ ∀ (h : ¬∃ (h : ¬head :: tail = []), ((head :: tail).head h).fst (β := fun (i : ι) ↦ M i) = j),
    m₁ = m₂ * 1 ↔
      (∃ (m' : M j), (head :: tail).head? = some (Sigma.mk (β := fun (i : ι) ↦ M i) j m') ∧ m₁ = m₂ * m') ∨
        ¬Option.map (Sigma.fst (β := fun (i : ι) ↦ M i)) (head :: tail).head? = some j ∧ m₁ = m₂

Tactic:
simp +contextual [Sigma.ext_iff]

Premises used: Sigma.ext_iff
-- 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
m₂ : M j
hij : ¬i = j
ne_one : ∀ (l : (i : ι) × M i), Membership.mem (γ := List ((i : ι) × M i)) [] l → l.snd (β := fun (i : ι) ↦ M i) ≠ 1
chain_ne :
  List.IsChain (fun (l l' : (i : ι) × M i) ↦ l.fst (β := fun (i : ι) ↦ M i) ≠ l'.fst (β := fun (i : ι) ↦ M i)) []
⊢ (Sigma.mk (β := fun (i : ι) ↦ M i) i m₁ ∈ (mk (M := M) [] ne_one chain_ne).toList (M := M).tail ∨
      (i ≠ j ∧
          ∃ (h : (mk (M := M) [] ne_one chain_ne).toList (M := M) ≠ []),
            (mk (M := M) [] ne_one chain_ne).toList (M := M).head h = Sigma.mk (β := fun (i : ι) ↦ M i) i m₁) ∨
        m₁ ≠ 1 ∧
          ∃ (h : j = i),
            m₁ =
              Eq.rec (motive := fun (x : ι) (h : j = x) ↦ M x)
                (Pair.head (M := M)
                  (have __src : Pair M j :=
                    (equivPair (M := M) j : (a : Word M) → Pair M j) (mk (M := M) [] ne_one chain_ne);
                  Pair.mk (M := M)
                    (m₂ *
                      if h :
                          ∃ (h : (mk (M := M) [] ne_one chain_ne).toList (M := M) ≠ []),
                            ((mk (M := M) [] ne_one chain_ne).toList (M := M).head h).fst (β := fun (i : ι) ↦ M i) =
                              j then
                        Eq.rec (motive :=
                          fun (x : ι)
                            (h :
                              ((mk (M := M) [] ne_one chain_ne).toList (M := M).head ⋯).fst (β := fun (i : ι) ↦ M i) =
                                x) ↦
                          M x) (((mk (M := M) [] ne_one chain_ne).toList (M := M).head ⋯).snd (β := fun (i : ι) ↦ M i))
                          ⋯
                      else 1)
                    (__src.tail (M := M)) ⋯))
                h) ↔
    ¬i = j ∧ Sigma.mk (β := fun (i : ι) ↦ M i) i m₁ ∈ (mk (M := M) [] ne_one chain_ne).toList (M := M) ∨
      m₁ ≠ 1 ∧
        ∃ (hij : i = j),
          Sigma.mk (β := fun (i : ι) ↦ M i) i m₁ ∈ (mk (M := M) [] ne_one chain_ne).toList (M := M).tail ∨
            (∃ (m' : M j),
                Sigma.mk (β := fun (i : ι) ↦ M i) j m' ∈ (mk (M := M) [] ne_one chain_ne).toList (M := M).head? ∧
                  m₁ = Eq.rec (motive := fun (x : ι) (h : j = x) ↦ M x) (m₂ * m') ⋯) ∨
              (mk (M := M) [] ne_one chain_ne).fstIdx (M := M) ≠ some j ∧
                m₁ = Eq.rec (motive := fun (x : ι) (h : j = x) ↦ M x) m₂ ⋯

Tactic:
simp [or_comm, hij, Ne.symm hij, eq_comm]

Premises used: Ne.symm, eq_comm, or_comm
-- 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
m₂ : M j
hij : ¬i = j
head : (i : ι) × M i
tail : List ((i : ι) × M i)
ne_one : ∀ l ∈ head :: tail, l.snd (β := fun (i : ι) ↦ M i) ≠ 1
chain_ne :
  List.IsChain (fun (l l' : (i : ι) × M i) ↦ l.fst (β := fun (i : ι) ↦ M i) ≠ l'.fst (β := fun (i : ι) ↦ M i))
    (head :: tail)
⊢ (Sigma.mk (β := fun (i : ι) ↦ M i) i m₁ ∈ (mk (M := M) (head :: tail) ne_one chain_ne).toList (M := M).tail ∨
      (i ≠ j ∧
          ∃ (h : (mk (M := M) (head :: tail) ne_one chain_ne).toList (M := M) ≠ []),
            (mk (M := M) (head :: tail) ne_one chain_ne).toList (M := M).head h =
              Sigma.mk (β := fun (i : ι) ↦ M i) i m₁) ∨
        m₁ ≠ 1 ∧
          ∃ (h : j = i),
            m₁ =
              Eq.rec (motive := fun (x : ι) (h : j = x) ↦ M x)
                (Pair.head (M := M)
                  (have __src : Pair M j :=
                    (equivPair (M := M) j : (a : Word M) → Pair M j) (mk (M := M) (head :: tail) ne_one chain_ne);
                  Pair.mk (M := M)
                    (m₂ *
                      if h :
                          ∃ (h : (mk (M := M) (head :: tail) ne_one chain_ne).toList (M := M) ≠ []),
                            ((mk (M := M) (head :: tail) ne_one chain_ne).toList (M := M).head h).fst (β :=
                                fun (i : ι) ↦ M i) =
                              j then
                        Eq.rec (motive :=
                          fun (x : ι)
                            (h :
                              ((mk (M := M) (head :: tail) ne_one chain_ne).toList (M := M).head ⋯).fst (β :=
                                  fun (i : ι) ↦ M i) =
                                x) ↦
                          M x)
                          (((mk (M := M) (head :: tail) ne_one chain_ne).toList (M := M).head ⋯).snd (β := fun (i : ι) ↦
                            M i))
                          ⋯
                      else 1)
                    (__src.tail (M := M)) ⋯))
                h) ↔
    ¬i = j ∧ Sigma.mk (β := fun (i : ι) ↦ M i) i m₁ ∈ (mk (M := M) (head :: tail) ne_one chain_ne).toList (M := M) ∨
      m₁ ≠ 1 ∧
        ∃ (hij : i = j),
          Sigma.mk (β := fun (i : ι) ↦ M i) i m₁ ∈ (mk (M := M) (head :: tail) ne_one chain_ne).toList (M := M).tail ∨
            (∃ (m' : M j),
                Sigma.mk (β := fun (i : ι) ↦ M i) j m' ∈
                    (mk (M := M) (head :: tail) ne_one chain_ne).toList (M := M).head? ∧
                  m₁ = Eq.rec (motive := fun (x : ι) (h : j = x) ↦ M x) (m₂ * m') ⋯) ∨
              (mk (M := M) (head :: tail) ne_one chain_ne).fstIdx (M := M) ≠ some j ∧
                m₁ = Eq.rec (motive := fun (x : ι) (h : j = x) ↦ M x) m₂ ⋯

Tactic:
simp [or_comm, hij, Ne.symm hij, eq_comm]

Premises used: Ne.symm, eq_comm, or_comm
-- 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 : ι
hij : i ≠ j
m₁ : M i
m₂ : M j
w : Word M
⊢ Sigma.mk (β := fun (i : ι) ↦ M i) i m₁ ∈
      (HSMul.hSMul (α := CoprodI M) ((of (M := M) : (a : M j) → CoprodI M) m₂ : CoprodI M) w).toList (M := M) ↔
    Sigma.mk (β := fun (i : ι) ↦ M i) i m₁ ∈ w.toList (M := M)

Tactic:
simp [mem_smul_iff, *]

Premises used: Monoid.CoprodI.Word.mem_smul_iff
-- 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 : ι
m : M i
ls : Word M
h1 : ls.fstIdx (M := M) ≠ some i
h2 : m ≠ 1
rw :
  cons (M := M) m ls h1 h2 =
    rcons (M := M) (i := i)
      (have __src := Pair.mk (M := M) 1 ls h1;
      Pair.mk (M := M) (m * (Pair.mk (M := M) 1 ls h1).head (M := M)) (__src.tail (M := M)) ⋯)
rw₁ : ls.fstIdx (M := M) ≠ some i
⊢ cons (M := M) m ls h1 h2 = HSMul.hSMul (α := CoprodI M) ((of (M := M) : (a : M i) → CoprodI M) m : CoprodI M) ls

Tactic:
rw [of_smul_def, equivPair_eq_of_fstIdx_ne _]

Premises used: Monoid.CoprodI.Word.of_smul_def, Monoid.CoprodI.Word.equivPair_eq_of_fstIdx_ne
-- 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 : ι
m : M i
ls : Word M
h1 : ls.fstIdx (M := M) ≠ some i
h2 : m ≠ 1
⊢ cons (M := M) m ls h1 h2 =
    rcons (M := M) (i := i)
      (have __src := Pair.mk (M := M) 1 ls h1;
      Pair.mk (M := M) (m * (Pair.mk (M := M) 1 ls h1).head (M := M)) (__src.tail (M := M)) ⋯)

Tactic:
simp [cons, rcons, h2]

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

Tactic:
h1
-- 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 : ι
m : M i
ls : Word M
h1 : ls.fstIdx (M := M) ≠ some i
h2 : m ≠ 1
⊢ ls.fstIdx (M := M) ≠ some i

Tactic:
exact h1
-- 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
⊢ rcons (M := M) p =
    HSMul.hSMul (α := CoprodI M) ((of (M := M) : (a : M i) → CoprodI M) (p.head (M := M)) : CoprodI M) (p.tail (M := M))

Tactic:
simp [of_smul_def]

Premises used: Monoid.CoprodI.Word.of_smul_def
-- 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
rw : rcons (M := M) (i := i) ((equivPair (M := M) i : (a : Word M) → Pair M i) w) = w
rw₁ :
  (Equiv.symm (equivPair (M := M) i) : (a : Pair M i) → Word M) ((equivPair (M := M) i : (a : Word M) → Pair M i) w) = w
rw₂ rw₃ : w = w
⊢ HSMul.hSMul (α := CoprodI M) (β := Word M)
      ((of (M := M) : (a : M i) → CoprodI M) (Pair.head (M := M) ((equivPair (M := M) i : (a : Word M) → Pair M i) w)) :
        CoprodI M)
      (Pair.tail (M := M) (i := i) ((equivPair (M := M) i : (a : Word M) → Pair M i) w) : Word M) =
    w

Tactic:
rw [← rcons_eq_smul, ← equivPair_symm, Equiv.symm_apply_apply]

Premises used: Equiv.symm_apply_apply, Monoid.CoprodI.Word.equivPair_symm, Monoid.CoprodI.Word.rcons_eq_smul
-- Module: Mathlib.GroupTheory.CoprodI
Goal:
ι : Type u_1
inst : DecidableEq ι
G : ι → Type u_4
inst_1 : (i : ι) → Group (G i)
inst_2 : (i : ι) → DecidableEq (G i)
i : ι
w : Word G
⊢ Pair.tail (M := G) (i := i) ((equivPair (M := G) i : (a : Word G) → Pair G i) w) =
    HSMul.hSMul (α := CoprodI G)
      (((of (M := G) : (a : G i) → CoprodI G)
            (Pair.head (M := G) ((equivPair (M := G) i : (a : Word G) → Pair G i) w)))⁻¹ :
        CoprodI G)
      w

Tactic:
Eq.symm <| inv_smul_eq_iff.2 (equivPair_head_smul_equivPair_tail w).symm

Premises used: Iff.mpr, inv_smul_eq_iff, Monoid.CoprodI.Word.equivPair_head_smul_equivPair_tail, Eq.symm
-- 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)
motive : Word M → Prop
empty : motive (Word.empty (M := M))
smul :
  ∀ (i : ι) (m : M i) (w : Word M),
    motive w → motive (HSMul.hSMul (α := CoprodI M) ((of (M := M) : (a : M i) → CoprodI M) m : CoprodI M) w)
⊢ motive (Word.empty (M := M))

Tactic:
empty
-- 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)
motive : Word M → Prop
empty : motive (Word.empty (M := M))
smul :
  ∀ (i : ι) (m : M i) (w : Word M),
    motive w → motive (HSMul.hSMul (α := CoprodI M) ((of (M := M) : (a : M i) → CoprodI M) m : CoprodI M) w)
⊢ motive (Word.empty (M := M))

Tactic:
exact empty
-- 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)
motive : Word M → Prop
empty : motive (Word.empty (M := M))
smul :
  ∀ (i : ι) (m : M i) (w : Word M),
    motive w → motive (HSMul.hSMul (α := CoprodI M) ((of (M := M) : (a : M i) → CoprodI M) m : CoprodI M) w)
i : ι
m : M i
w : Word M
h1 : w.fstIdx (M := M) ≠ some i
h2 : m ≠ 1
ih : motive w
cons : motive (HSMul.hSMul (α := CoprodI M) ((of (M := M) : (a : M i) → CoprodI M) m : CoprodI M) w)
⊢ motive (Word.cons (M := M) m w h1 h2)

Tactic:
rw [cons_eq_smul]

Premises used: Monoid.CoprodI.Word.cons_eq_smul
-- 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)
motive : Word M → Prop
empty : motive (Word.empty (M := M))
smul :
  ∀ (i : ι) (m : M i) (w : Word M),
    motive w → motive (HSMul.hSMul (α := CoprodI M) ((of (M := M) : (a : M i) → CoprodI M) m : CoprodI M) w)
i : ι
m : M i
w : Word M
h1 : w.fstIdx (M := M) ≠ some i
h2 : m ≠ 1
ih : motive w
⊢ motive (HSMul.hSMul (α := CoprodI M) ((of (M := M) : (a : M i) → CoprodI M) m : CoprodI M) w)

Tactic:
smul _ _ _ ih
-- 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)
motive : Word M → Prop
empty : motive (Word.empty (M := M))
smul :
  ∀ (i : ι) (m : M i) (w : Word M),
    motive w → motive (HSMul.hSMul (α := CoprodI M) ((of (M := M) : (a : M i) → CoprodI M) m : CoprodI M) w)
i : ι
m : M i
w : Word M
h1 : w.fstIdx (M := M) ≠ some i
h2 : m ≠ 1
ih : motive w
⊢ motive (HSMul.hSMul (α := CoprodI M) ((of (M := M) : (a : M i) → CoprodI M) m : CoprodI M) w)

Tactic:
exact smul _ _ _ ih
-- 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)
motive : Word M → Prop
empty : motive (Word.empty (M := M))
smul :
  ∀ (i : ι) (m : M i) (w : Word M),
    motive w → motive (HSMul.hSMul (α := CoprodI M) ((of (M := M) : (a : M i) → CoprodI M) m : CoprodI M) w)
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) (ih : motive w),
    motive (Word.cons (M := M) m w h1 h2)
⊢ motive w

Tactic:
induction w using consRecOn with
  | empty => exact empty
  | cons _ _ _ _ _ ih =>
    rw [cons_eq_smul]
    exact smul _ _ _ ih

Premises used: Monoid.CoprodI.Word.cons_eq_smul, Monoid.CoprodI.Word.cons
-- 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)
w : Word M
one : w.prod (M := M) = 1 * w.prod (M := M)
one₁ one₂ : w.prod (M := M) = w.prod (M := M)
⊢ (HSMul.hSMul (α := CoprodI M) 1 w).prod (M := M) = 1 * w.prod (M := M)

Tactic:
rw [one_smul, one_mul]

Premises used: one_smul, one_mul
-- 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)
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
mul : (x • y • w).prod (M := M) = x * y * w.prod (M := M)
mul₁ : x * (y • w).prod (M := M) = x * y * w.prod (M := M)
mul₂ : x * (y * w.prod (M := M)) = x * y * w.prod (M := M)
mul₃ mul₄ : x * (y * w.prod (M := M)) = x * (y * w.prod (M := M))
⊢ ((x * y) • w).prod (M := M) = x * y * w.prod (M := M)

Tactic:
rw [mul_smul, hx, hy, mul_assoc]

Premises used: mul_assoc, SemigroupAction.mul_smul