awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.CoprodI
Goal:
ι : Type u_1
M : ι → Type u_2
inst : (i : ι) → Monoid (M i)
l : List ((i : ι) × M i)
hnot1 : ∀ l_1 ∈ l, l_1.snd (β := fun (i : ι) ↦ M i) ≠ 1
hchain : List.IsChain (fun (l l' : (i : ι) × M i) ↦ l.fst (β := fun (i : ι) ↦ M i) ≠ l'.fst (β := fun (i : ι) ↦ M i)) l
h : Word.mk (M := M) l hnot1 hchain ≠ empty (M := M)
nil :
  ∀
    (hnot1 :
      ∀ (l : (i : ι) × M i), Membership.mem (γ := List ((i : ι) × M i)) [] l → l.snd (β := fun (i : ι) ↦ M i) ≠ 1)
    (hchain :
      List.IsChain (fun (l l' : (i : ι) × M i) ↦ l.fst (β := fun (i : ι) ↦ M i) ≠ l'.fst (β := fun (i : ι) ↦ M i)) [])
    (h : Word.mk (M := M) [] hnot1 hchain ≠ empty (M := M)),
    ∃ (i : ι) (j : ι) (w' : NeWord M i j),
      w'.toWord (M := M).toList (M := M) = (Word.mk (M := M) [] hnot1 hchain).toList (M := M)
cons :
  ∀ (x : (i : ι) × M i) (l : List ((i : ι) × M i))
    (hi :
      ∀ (hnot1 : ∀ l_1 ∈ l, l_1.snd (β := fun (i : ι) ↦ M i) ≠ 1)
        (hchain :
          List.IsChain (fun (l l' : (i : ι) × M i) ↦ l.fst (β := fun (i : ι) ↦ M i) ≠ l'.fst (β := fun (i : ι) ↦ M i))
            l)
        (h : Word.mk (M := M) l hnot1 hchain ≠ empty (M := M)),
        ∃ (i : ι) (j : ι) (w' : NeWord M i j),
          w'.toWord (M := M).toList (M := M) = (Word.mk (M := M) l hnot1 hchain).toList (M := M))
    (hnot1 : ∀ l_1 ∈ x :: l, l_1.snd (β := fun (i : ι) ↦ M i) ≠ 1)
    (hchain :
      List.IsChain (fun (l l' : (i : ι) × M i) ↦ l.fst (β := fun (i : ι) ↦ M i) ≠ l'.fst (β := fun (i : ι) ↦ M i))
        (x :: l))
    (h : Word.mk (M := M) (x :: l) hnot1 hchain ≠ empty (M := M)),
    ∃ (i : ι) (j : ι) (w' : NeWord M i j),
      w'.toWord (M := M).toList (M := M) = (Word.mk (M := M) (x :: l) hnot1 hchain).toList (M := M)
⊢ ∃ (i : ι) (j : ι) (w' : NeWord M i j),
    w'.toWord (M := M).toList (M := M) = (Word.mk (M := M) l hnot1 hchain).toList (M := M)

Tactic:
induction l with
  | nil => contradiction
  | cons x l hi =>
    rw [List.forall_mem_cons] at hnot1
    rcases l with - | ⟨y, l⟩
    · refine ⟨x.1, x.1, singleton x.2 hnot1.1, ?_⟩
      simp [toWord]
    · rw [List.isChain_cons_cons] at hchain
      specialize hi hnot1.2 hchain.2 (by rintro ⟨rfl⟩)
      obtain ⟨i, j, w', hw' : w'.toList = y::l⟩ := hi
      obtain rfl : y = ⟨i, w'.head⟩ := by simpa [hw'] using w'.toList_head?
      refine ⟨x.1, j, append (singleton x.2 hnot1.1) hchain.1 w', ?_⟩
      simpa [toWord] using hw'

Premises used: Monoid.CoprodI.NeWord.toWord, List.isChain_cons_cons, List.forall_mem_cons, Monoid.CoprodI.Word.cons, rfl
-- Module: Mathlib.GroupTheory.CoprodI
Goal:
ι : Type u_1
M : ι → Type u_2
inst : (i : ι) → Monoid (M i)
i : ι
x : M i
hne_one : x ≠ 1
⊢ (singleton (M := M) x hne_one).head (M := M) = x

Tactic:
rfl

Premises used: Monoid.CoprodI.NeWord.head, rfl
-- Module: Mathlib.GroupTheory.CoprodI
Goal:
ι : Type u_1
M : ι → Type u_2
inst : (i : ι) → Monoid (M i)
i : ι
x : M i
hne_one : x ≠ 1
⊢ (singleton (M := M) x hne_one).last (M := M) = x

Tactic:
rfl

Premises used: Monoid.CoprodI.NeWord.last, rfl
-- Module: Mathlib.GroupTheory.CoprodI
Goal:
ι : Type u_1
M : ι → Type u_2
inst : (i : ι) → Monoid (M i)
i : ι
x : M i
hne_one : x ≠ 1
⊢ (singleton (M := M) x hne_one).prod (M := M) = (of (M := M) : (a : M i) → CoprodI M) x

Tactic:
simp [toWord, prod, Word.prod]

Premises used: Monoid.CoprodI.NeWord.toWord, Monoid.CoprodI.Word.prod, Monoid.CoprodI.NeWord.prod
-- Module: Mathlib.GroupTheory.CoprodI
Goal:
ι : Type u_1
M : ι → Type u_2
inst : (i : ι) → Monoid (M i)
i j k l : ι
w₁ : NeWord M i j
hne : j ≠ k
w₂ : NeWord M k l
⊢ (w₁.append (M := M) hne w₂).head (M := M) = w₁.head (M := M)

Tactic:
rfl

Premises used: Monoid.CoprodI.NeWord.head, rfl
-- Module: Mathlib.GroupTheory.CoprodI
Goal:
ι : Type u_1
M : ι → Type u_2
inst : (i : ι) → Monoid (M i)
i j k l : ι
w₁ : NeWord M i j
hne : j ≠ k
w₂ : NeWord M k l
⊢ (w₁.append (M := M) hne w₂).last (M := M) = w₂.last (M := M)

Tactic:
rfl

Premises used: Monoid.CoprodI.NeWord.last, rfl
-- Module: Mathlib.GroupTheory.CoprodI
Goal:
ι : Type u_1
M : ι → Type u_2
inst : (i : ι) → Monoid (M i)
i j k l : ι
w₁ : NeWord M i j
hne : j ≠ k
w₂ : NeWord M k l
⊢ (w₁.append (M := M) hne w₂).prod (M := M) = w₁.prod (M := M) * w₂.prod (M := M)

Tactic:
simp [toWord, prod, Word.prod]

Premises used: Monoid.CoprodI.NeWord.toWord, Monoid.CoprodI.Word.prod, Monoid.CoprodI.NeWord.prod
-- Module: Mathlib.GroupTheory.CoprodI
Goal:
ι : Type u_1
M : ι → Type u_2
inst : (i : ι) → Monoid (M i)
i j : ι
x : M i
hnotone : x ≠ 1
w : NeWord M i j
singleton :
  ∀ {i : ι} (x : M i) (a : x ≠ 1) (x_1 : M i) (hnotone : x_1 ≠ 1),
    (replaceHead (M := M) x_1 hnotone (NeWord.singleton (M := M) x a)).head (M := M) = x_1
append :
  ∀ {i j k l : ι} (_w₁ : NeWord M i j) (_hne : j ≠ k) (_w₂ : NeWord M k l),
    (∀ (x : M i) (hnotone : x ≠ 1), (replaceHead (M := M) x hnotone _w₁).head (M := M) = x) →
      (∀ (x : M k) (hnotone : x ≠ 1), (replaceHead (M := M) x hnotone _w₂).head (M := M) = x) →
        ∀ (x : M i) (hnotone : x ≠ 1), (replaceHead (M := M) x hnotone (_w₁.append (M := M) _hne _w₂)).head (M := M) = x
⊢ (replaceHead (M := M) x hnotone w).head (M := M) = x

Tactic:
induction w
-- Module: Mathlib.GroupTheory.CoprodI
Goal:
ι : Type u_1
M : ι → Type u_2
inst : (i : ι) → Monoid (M i)
i j i_1 : ι
x_1 : M i_1
h : x_1 ≠ 1
x : M i_1
hnotone : x ≠ 1
⊢ (replaceHead (M := M) x hnotone (singleton (M := M) x_1 h)).head (M := M) = x

Tactic:
rfl
-- Module: Mathlib.GroupTheory.CoprodI
Goal:
ι : Type u_1
M : ι → Type u_2
inst : (i : ι) → Monoid (M i)
i j i_1 j_1 k l : ι
_w₁ : NeWord M i_1 j_1
_hne : j_1 ≠ k
_w₂ : NeWord M k l
_w₁_ih : ∀ (x : M i_1) (hnotone : x ≠ 1), (replaceHead (M := M) x hnotone _w₁).head (M := M) = x
_w₂_ih : ∀ (x : M k) (hnotone : x ≠ 1), (replaceHead (M := M) x hnotone _w₂).head (M := M) = x
x : M i_1
hnotone : x ≠ 1
⊢ (replaceHead (M := M) x hnotone (_w₁.append (M := M) _hne _w₂)).head (M := M) = x

Tactic:
simp [*, replaceHead]

Premises used: Monoid.CoprodI.NeWord.replaceHead
-- Module: Mathlib.GroupTheory.CoprodI
Goal:
ι : Type u_1
M : ι → Type u_2
inst : (i : ι) → Monoid (M i)
i j : ι
w : NeWord M i j
x : M i
hnotone : x * w.head (M := M) ≠ 1
singleton :
  ∀ {i : ι} (x : M i) (a : x ≠ 1) (x_1 : M i) (hnotone : x_1 * (NeWord.singleton (M := M) x a).head (M := M) ≠ 1),
    ((NeWord.singleton (M := M) x a).mulHead (M := M) x_1 hnotone).head (M := M) =
      x_1 * (NeWord.singleton (M := M) x a).head (M := M)
append :
  ∀ {i j k l : ι} (_w₁ : NeWord M i j) (_hne : j ≠ k) (_w₂ : NeWord M k l),
    (∀ (x : M i) (hnotone : x * _w₁.head (M := M) ≠ 1),
        (_w₁.mulHead (M := M) x hnotone).head (M := M) = x * _w₁.head (M := M)) →
      (∀ (x : M k) (hnotone : x * _w₂.head (M := M) ≠ 1),
          (_w₂.mulHead (M := M) x hnotone).head (M := M) = x * _w₂.head (M := M)) →
        ∀ (x : M i) (hnotone : x * (_w₁.append (M := M) _hne _w₂).head (M := M) ≠ 1),
          ((_w₁.append (M := M) _hne _w₂).mulHead (M := M) x hnotone).head (M := M) =
            x * (_w₁.append (M := M) _hne _w₂).head (M := M)
⊢ (w.mulHead (M := M) x hnotone).head (M := M) = x * w.head (M := M)

Tactic:
induction w
-- Module: Mathlib.GroupTheory.CoprodI
Goal:
ι : Type u_1
M : ι → Type u_2
inst : (i : ι) → Monoid (M i)
i j i_1 : ι
x_1 : M i_1
h : x_1 ≠ 1
x : M i_1
hnotone : x * (singleton (M := M) x_1 h).head (M := M) ≠ 1
⊢ ((singleton (M := M) x_1 h).mulHead (M := M) x hnotone).head (M := M) = x * (singleton (M := M) x_1 h).head (M := M)

Tactic:
rfl
-- Module: Mathlib.GroupTheory.CoprodI
Goal:
ι : Type u_1
M : ι → Type u_2
inst : (i : ι) → Monoid (M i)
i j i_1 j_1 k l : ι
_w₁ : NeWord M i_1 j_1
_hne : j_1 ≠ k
_w₂ : NeWord M k l
_w₁_ih :
  ∀ (x : M i_1) (hnotone : x * _w₁.head (M := M) ≠ 1),
    (_w₁.mulHead (M := M) x hnotone).head (M := M) = x * _w₁.head (M := M)
_w₂_ih :
  ∀ (x : M k) (hnotone : x * _w₂.head (M := M) ≠ 1),
    (_w₂.mulHead (M := M) x hnotone).head (M := M) = x * _w₂.head (M := M)
x : M i_1
hnotone : x * (_w₁.append (M := M) _hne _w₂).head (M := M) ≠ 1
⊢ ((_w₁.append (M := M) _hne _w₂).mulHead (M := M) x hnotone).head (M := M) =
    x * (_w₁.append (M := M) _hne _w₂).head (M := M)

Tactic:
simp [*, mulHead]

Premises used: Monoid.CoprodI.NeWord.mulHead
-- Module: Mathlib.GroupTheory.CoprodI
Goal:
ι : Type u_1
M : ι → Type u_2
inst : (i : ι) → Monoid (M i)
i j i_1 : ι
x_1 : M i_1
h : x_1 ≠ 1
x : M i_1
hnotone : x * (singleton (M := M) x_1 h).head (M := M) ≠ 1
⊢ (replaceHead (M := M) (x * (singleton (M := M) x_1 h).head (M := M)) hnotone (singleton (M := M) x_1 h)).prod (M :=
      M) =
    HMul.hMul (α := CoprodI M) ((of (M := M) : (a : M i_1) → CoprodI M) x : CoprodI M)
      ((singleton (M := M) x_1 h).prod (M := M))

Tactic:
simp [replaceHead]

Premises used: Monoid.CoprodI.NeWord.replaceHead
-- Module: Mathlib.GroupTheory.CoprodI
Goal:
ι : Type u_1
M : ι → Type u_2
inst : (i : ι) → Monoid (M i)
i j i_1 j_1 k l : ι
_w₁ : NeWord M i_1 j_1
_hne : j_1 ≠ k
_w₂ : NeWord M k l
w_ih_w₁ :
  ∀ (x : M i_1) (hnotone : x * _w₁.head (M := M) ≠ 1),
    (replaceHead (M := M) (x * _w₁.head (M := M)) hnotone _w₁).prod (M := M) =
      HMul.hMul (α := CoprodI M) ((of (M := M) : (a : M i_1) → CoprodI M) x : CoprodI M) (_w₁.prod (M := M))
w_ih_w₂ :
  ∀ (x : M k) (hnotone : x * _w₂.head (M := M) ≠ 1),
    (replaceHead (M := M) (x * _w₂.head (M := M)) hnotone _w₂).prod (M := M) =
      HMul.hMul (α := CoprodI M) ((of (M := M) : (a : M k) → CoprodI M) x : CoprodI M) (_w₂.prod (M := M))
x : M i_1
hnotone : x * (_w₁.append (M := M) _hne _w₂).head (M := M) ≠ 1
⊢ (replaceHead (M := M) (x * _w₁.head (M := M)) hnotone _w₁).prod (M := M) =
    HMul.hMul (α := CoprodI M) ((of (M := M) : (a : M i_1) → CoprodI M) x : CoprodI M) (_w₁.prod (M := M))

Tactic:
specialize w_ih_w₁ _ hnotone
-- Module: Mathlib.GroupTheory.CoprodI
Goal:
ι : Type u_1
M : ι → Type u_2
inst : (i : ι) → Monoid (M i)
i j i_1 j_1 k l : ι
_w₁ : NeWord M i_1 j_1
_hne : j_1 ≠ k
_w₂ : NeWord M k l
w_ih_w₂ :
  ∀ (x : M k) (hnotone : x * _w₂.head (M := M) ≠ 1),
    (replaceHead (M := M) (x * _w₂.head (M := M)) hnotone _w₂).prod (M := M) =
      HMul.hMul (α := CoprodI M) ((of (M := M) : (a : M k) → CoprodI M) x : CoprodI M) (_w₂.prod (M := M))
x : M i_1
hnotone : x * (_w₁.append (M := M) _hne _w₂).head (M := M) ≠ 1
w_ih_w₁ :
  (replaceHead (M := M) (x * _w₁.head (M := M)) hnotone _w₁).prod (M := M) =
    HMul.hMul (α := CoprodI M) ((of (M := M) : (a : M i_1) → CoprodI M) x : CoprodI M) (_w₁.prod (M := M))
append :
  (replaceHead (M := M) (x * (_w₁.append (M := M) _hne _w₂).head (M := M)) hnotone _w₁).prod (M := M) *
      _w₂.prod (M := M) =
    HMul.hMul (α := CoprodI M) ((of (M := M) : (a : M i_1) → CoprodI M) x : CoprodI M) (_w₁.prod (M := M)) *
      _w₂.prod (M := M)
⊢ (replaceHead (M := M) (x * (_w₁.append (M := M) _hne _w₂).head (M := M)) hnotone (_w₁.append (M := M) _hne _w₂)).prod
      (M := M) =
    HMul.hMul (α := CoprodI M) ((of (M := M) : (a : M i_1) → CoprodI M) x : CoprodI M)
      ((_w₁.append (M := M) _hne _w₂).prod (M := M))

Tactic:
simp only [replaceHead, append_prod, ← mul_assoc]

Premises used: Monoid.CoprodI.NeWord.append_prod, mul_assoc, Monoid.CoprodI.NeWord.replaceHead
-- Module: Mathlib.GroupTheory.CoprodI
Goal:
ι : Type u_1
M : ι → Type u_2
inst : (i : ι) → Monoid (M i)
i j i_1 j_1 k l : ι
_w₁ : NeWord M i_1 j_1
_hne : j_1 ≠ k
_w₂ : NeWord M k l
w_ih_w₂ :
  ∀ (x : M k) (hnotone : x * _w₂.head (M := M) ≠ 1),
    (replaceHead (M := M) (x * _w₂.head (M := M)) hnotone _w₂).prod (M := M) =
      HMul.hMul (α := CoprodI M) ((of (M := M) : (a : M k) → CoprodI M) x : CoprodI M) (_w₂.prod (M := M))
x : M i_1
hnotone : x * (_w₁.append (M := M) _hne _w₂).head (M := M) ≠ 1
w_ih_w₁ :
  (replaceHead (M := M) (x * _w₁.head (M := M)) hnotone _w₁).prod (M := M) =
    HMul.hMul (α := CoprodI M) ((of (M := M) : (a : M i_1) → CoprodI M) x : CoprodI M) (_w₁.prod (M := M))
⊢ (replaceHead (M := M) (x * (_w₁.append (M := M) _hne _w₂).head (M := M)) hnotone _w₁).prod (M := M) *
      _w₂.prod (M := M) =
    HMul.hMul (α := CoprodI M) ((of (M := M) : (a : M i_1) → CoprodI M) x : CoprodI M) (_w₁.prod (M := M)) *
      _w₂.prod (M := M)

Tactic:
congr 1
-- Module: Mathlib.GroupTheory.CoprodI
Goal:
ι : Type u_1
M : ι → Type u_2
inst : (i : ι) → Monoid (M i)
i j : ι
w : NeWord M i j
x : M i
hnotone : x * w.head (M := M) ≠ 1
singleton :
  ∀ {i : ι} (x : M i) (a : x ≠ 1) (x_1 : M i) (hnotone : x_1 * (NeWord.singleton (M := M) x a).head (M := M) ≠ 1),
    (replaceHead (M := M) (x_1 * (NeWord.singleton (M := M) x a).head (M := M)) hnotone
            (NeWord.singleton (M := M) x a)).prod
        (M := M) =
      HMul.hMul (α := CoprodI M) ((of (M := M) : (a : M i) → CoprodI M) x_1 : CoprodI M)
        ((NeWord.singleton (M := M) x a).prod (M := M))
append :
  ∀ {i j k l : ι} (_w₁ : NeWord M i j) (_hne : j ≠ k) (_w₂ : NeWord M k l)
    (w_ih_w₁ :
      ∀ (x : M i) (hnotone : x * _w₁.head (M := M) ≠ 1),
        (replaceHead (M := M) (x * _w₁.head (M := M)) hnotone _w₁).prod (M := M) =
          HMul.hMul (α := CoprodI M) ((of (M := M) : (a : M i) → CoprodI M) x : CoprodI M) (_w₁.prod (M := M)))
    (w_ih_w₂ :
      ∀ (x : M k) (hnotone : x * _w₂.head (M := M) ≠ 1),
        (replaceHead (M := M) (x * _w₂.head (M := M)) hnotone _w₂).prod (M := M) =
          HMul.hMul (α := CoprodI M) ((of (M := M) : (a : M k) → CoprodI M) x : CoprodI M) (_w₂.prod (M := M)))
    (x : M i) (hnotone : x * (_w₁.append (M := M) _hne _w₂).head (M := M) ≠ 1),
    (replaceHead (M := M) (x * (_w₁.append (M := M) _hne _w₂).head (M := M)) hnotone
            (_w₁.append (M := M) _hne _w₂)).prod
        (M := M) =
      HMul.hMul (α := CoprodI M) ((of (M := M) : (a : M i) → CoprodI M) x : CoprodI M)
        ((_w₁.append (M := M) _hne _w₂).prod (M := M))
⊢ (replaceHead (M := M) (x * w.head (M := M)) hnotone w).prod (M := M) =
    HMul.hMul (α := CoprodI M) ((of (M := M) : (a : M i) → CoprodI M) x : CoprodI M) (w.prod (M := M))

Tactic:
induction w with
  | singleton => simp [replaceHead]
  | append _ _ _ w_ih_w₁ w_ih_w₂ =>
    specialize w_ih_w₁ _ hnotone
    simp only [replaceHead, append_prod, ← mul_assoc]
    congr 1

Premises used: Monoid.CoprodI.NeWord.append_prod, mul_assoc, Monoid.CoprodI.NeWord.singleton, Monoid.CoprodI.NeWord.append, Monoid.CoprodI.NeWord.replaceHead
-- Module: Mathlib.GroupTheory.CoprodI
Goal:
ι : Type u_1
G : ι → Type u_4
inst : (i : ι) → Group (G i)
i j : ι
w : NeWord G i j
singleton :
  ∀ {i : ι} (x : G i) (a : x ≠ 1),
    Eq (α := CoprodI G) (prod (M := G) (inv (G := G) (NeWord.singleton (M := G) x a)))
      (prod (M := G) (NeWord.singleton (M := G) x a))⁻¹
append :
  ∀ {i j k l : ι} (_w₁ : NeWord G i j) (_hne : j ≠ k) (_w₂ : NeWord G k l),
    _w₁.inv (G := G).prod (M := G) = (_w₁.prod (M := G))⁻¹ →
      _w₂.inv (G := G).prod (M := G) = (_w₂.prod (M := G))⁻¹ →
        (_w₁.append (M := G) _hne _w₂).inv (G := G).prod (M := G) = ((_w₁.append (M := G) _hne _w₂).prod (M := G))⁻¹
⊢ w.inv (G := G).prod (M := G) = (w.prod (M := G))⁻¹

Tactic:
induction w
-- Module: Mathlib.GroupTheory.CoprodI
Goal:
ι : Type u_1
G : ι → Type u_4
inst : (i : ι) → Group (G i)
i j i_1 : ι
x : G i_1
h : x ≠ 1
⊢ Eq (α := CoprodI G) (prod (M := G) (inv (G := G) (singleton (M := G) x h))) (prod (M := G) (singleton (M := G) x h))⁻¹

Tactic:
simp [inv, *]

Premises used: Monoid.CoprodI.NeWord.inv
-- Module: Mathlib.GroupTheory.CoprodI
Goal:
ι : Type u_1
G : ι → Type u_4
inst : (i : ι) → Group (G i)
i j i_1 j_1 k l : ι
_w₁ : NeWord G i_1 j_1
_hne : j_1 ≠ k
_w₂ : NeWord G k l
_w₁_ih : _w₁.inv (G := G).prod (M := G) = (_w₁.prod (M := G))⁻¹
_w₂_ih : _w₂.inv (G := G).prod (M := G) = (_w₂.prod (M := G))⁻¹
⊢ (_w₁.append (M := G) _hne _w₂).inv (G := G).prod (M := G) = ((_w₁.append (M := G) _hne _w₂).prod (M := G))⁻¹

Tactic:
simp [inv, *]

Premises used: Monoid.CoprodI.NeWord.inv
-- Module: Mathlib.GroupTheory.CoprodI
Goal:
ι : Type u_1
G : ι → Type u_4
inst : (i : ι) → Group (G i)
i j : ι
w : NeWord G i j
singleton :
  ∀ {i : ι} (x : G i) (a : x ≠ 1),
    head (M := G) (inv (G := G) (NeWord.singleton (M := G) x a)) = (last (M := G) (NeWord.singleton (M := G) x a))⁻¹
append :
  ∀ {i j k l : ι} (_w₁ : NeWord G i j) (_hne : j ≠ k) (_w₂ : NeWord G k l),
    _w₁.inv (G := G).head (M := G) = (_w₁.last (M := G))⁻¹ →
      _w₂.inv (G := G).head (M := G) = (_w₂.last (M := G))⁻¹ →
        (_w₁.append (M := G) _hne _w₂).inv (G := G).head (M := G) = ((_w₁.append (M := G) _hne _w₂).last (M := G))⁻¹
⊢ w.inv (G := G).head (M := G) = (w.last (M := G))⁻¹

Tactic:
induction w
-- Module: Mathlib.GroupTheory.CoprodI
Goal:
ι : Type u_1
G : ι → Type u_4
inst : (i : ι) → Group (G i)
i j i_1 : ι
x : G i_1
h : x ≠ 1
⊢ head (M := G) (inv (G := G) (singleton (M := G) x h)) = (last (M := G) (singleton (M := G) x h))⁻¹

Tactic:
simp [inv, *]

Premises used: Monoid.CoprodI.NeWord.inv
-- Module: Mathlib.GroupTheory.CoprodI
Goal:
ι : Type u_1
G : ι → Type u_4
inst : (i : ι) → Group (G i)
i j i_1 j_1 k l : ι
_w₁ : NeWord G i_1 j_1
_hne : j_1 ≠ k
_w₂ : NeWord G k l
_w₁_ih : _w₁.inv (G := G).head (M := G) = (_w₁.last (M := G))⁻¹
_w₂_ih : _w₂.inv (G := G).head (M := G) = (_w₂.last (M := G))⁻¹
⊢ (_w₁.append (M := G) _hne _w₂).inv (G := G).head (M := G) = ((_w₁.append (M := G) _hne _w₂).last (M := G))⁻¹

Tactic:
simp [inv, *]

Premises used: Monoid.CoprodI.NeWord.inv
-- Module: Mathlib.GroupTheory.CoprodI
Goal:
ι : Type u_1
G : ι → Type u_4
inst : (i : ι) → Group (G i)
i j : ι
w : NeWord G i j
singleton :
  ∀ {i : ι} (x : G i) (a : x ≠ 1),
    last (M := G) (inv (G := G) (NeWord.singleton (M := G) x a)) = (head (M := G) (NeWord.singleton (M := G) x a))⁻¹
append :
  ∀ {i j k l : ι} (_w₁ : NeWord G i j) (_hne : j ≠ k) (_w₂ : NeWord G k l),
    _w₁.inv (G := G).last (M := G) = (_w₁.head (M := G))⁻¹ →
      _w₂.inv (G := G).last (M := G) = (_w₂.head (M := G))⁻¹ →
        (_w₁.append (M := G) _hne _w₂).inv (G := G).last (M := G) = ((_w₁.append (M := G) _hne _w₂).head (M := G))⁻¹
⊢ w.inv (G := G).last (M := G) = (w.head (M := G))⁻¹

Tactic:
induction w
-- Module: Mathlib.GroupTheory.CoprodI
Goal:
ι : Type u_1
G : ι → Type u_4
inst : (i : ι) → Group (G i)
i j i_1 : ι
x : G i_1
h : x ≠ 1
⊢ last (M := G) (inv (G := G) (singleton (M := G) x h)) = (head (M := G) (singleton (M := G) x h))⁻¹

Tactic:
simp [inv, *]

Premises used: Monoid.CoprodI.NeWord.inv
-- Module: Mathlib.GroupTheory.CoprodI
Goal:
ι : Type u_1
G : ι → Type u_4
inst : (i : ι) → Group (G i)
i j i_1 j_1 k l : ι
_w₁ : NeWord G i_1 j_1
_hne : j_1 ≠ k
_w₂ : NeWord G k l
_w₁_ih : _w₁.inv (G := G).last (M := G) = (_w₁.head (M := G))⁻¹
_w₂_ih : _w₂.inv (G := G).last (M := G) = (_w₂.head (M := G))⁻¹
⊢ (_w₁.append (M := G) _hne _w₂).inv (G := G).last (M := G) = ((_w₁.append (M := G) _hne _w₂).head (M := G))⁻¹

Tactic:
simp [inv, *]

Premises used: Monoid.CoprodI.NeWord.inv
-- Module: Mathlib.GroupTheory.CoprodI
Goal:
ι : Type u_1
G : Type u_4
inst : Group G
H : ι → Type u_5
inst_1 : (i : ι) → Group (H i)
f : (i : ι) → MonoidHom.{u_5, u_4} (H i) G
α : Type u_6
inst_2 : MulAction G α
X : ι → Set α
hpp :
  Pairwise fun (i j : ι) ↦
    ∀ (h : H i), h ≠ 1 → HSMul.hSMul.{u_4, u_6, u_6} (α := G) ((f i : (a : H i) → G) h : G) (X j) ⊆ X i
i j i_1 : ι
x : H i_1
hne_one : x ≠ 1
k : ι
hk : i_1 ≠ k
⊢ HSMul.hSMul.{u_4, u_6, u_6} (α := G)
      ((((lift (M := H) : (a : (i : ι) → H i →* G) → CoprodI H →* G) f : CoprodI H →* G) : (a : CoprodI H) → G)
          (NeWord.prod (M := H) (NeWord.singleton (M := H) x hne_one)) :
        G)
      (X k) ⊆
    X i_1

Tactic:
simpa using hpp hk _ hne_one
-- Module: Mathlib.GroupTheory.CoprodI
Goal:
ι : Type u_1
G : Type u_4
inst : Group G
H : ι → Type u_5
inst_1 : (i : ι) → Group (H i)
f : (i : ι) → MonoidHom.{u_5, u_4} (H i) G
α : Type u_6
inst_2 : MulAction G α
X : ι → Set α
hpp :
  Pairwise fun (i j : ι) ↦
    ∀ (h : H i), h ≠ 1 → HSMul.hSMul.{u_4, u_6, u_6} (α := G) ((f i : (a : H i) → G) h : G) (X j) ⊆ X i
i_1 j_1 i j k_1 l : ι
w₁ : NeWord H i j
hne : j ≠ k_1
w₂ : NeWord H k_1 l
hIw₁ :
  ∀ {k : ι} (hk : j ≠ k),
    HSMul.hSMul.{u_4, u_6, u_6} (α := G)
        ((((lift (M := H) : (a : (i : ι) → H i →* G) → CoprodI H →* G) f : CoprodI H →* G) : (a : CoprodI H) → G)
            (w₁.prod (M := H)) :
          G)
        (X k) ⊆
      X i
hIw₂ :
  ∀ {k : ι} (hk : l ≠ k),
    HSMul.hSMul.{u_4, u_6, u_6} (α := G)
        ((((lift (M := H) : (a : (i : ι) → H i →* G) → CoprodI H →* G) f : CoprodI H →* G) : (a : CoprodI H) → G)
            (w₂.prod (M := H)) :
          G)
        (X k) ⊆
      X k_1
k : ι
hk : l ≠ k
⊢ HSMul.hSMul.{u_4, u_6, u_6} (α := G)
      ((((lift (M := H) : (a : (i : ι) → H i →* G) → CoprodI H →* G) f : CoprodI H →* G) : (a : CoprodI H) → G)
          ((w₁.append (M := H) hne w₂).prod (M := H)) :
        G)
      (X k) =
    HSMul.hSMul.{u_4, u_6, u_6} (α := G)
      ((((lift (M := H) : (a : (i : ι) → H i →* G) → CoprodI H →* G) f : CoprodI H →* G) : (a : CoprodI H) → G)
          (w₁.prod (M := H)) :
        G)
      (HSMul.hSMul.{u_4, u_6, u_6} (α := G)
        ((((lift (M := H) : (a : (i : ι) → H i →* G) → CoprodI H →* G) f : CoprodI H →* G) : (a : CoprodI H) → G)
            (w₂.prod (M := H)) :
          G)
        (X k))

Tactic:
simp [mul_smul]

Premises used: SemigroupAction.mul_smul
-- Module: Mathlib.GroupTheory.CoprodI
Goal:
ι : Type u_1
G : Type u_4
inst : Group G
H : ι → Type u_5
inst_1 : (i : ι) → Group (H i)
f : (i : ι) → MonoidHom.{u_5, u_4} (H i) G
α : Type u_6
inst_2 : MulAction G α
X : ι → Set α
hpp :
  Pairwise fun (i j : ι) ↦
    ∀ (h : H i), h ≠ 1 → HSMul.hSMul.{u_4, u_6, u_6} (α := G) ((f i : (a : H i) → G) h : G) (X j) ⊆ X i
i_1 j_1 i j k_1 l : ι
w₁ : NeWord H i j
hne : j ≠ k_1
w₂ : NeWord H k_1 l
hIw₁ :
  ∀ {k : ι} (hk : j ≠ k),
    HSMul.hSMul.{u_4, u_6, u_6} (α := G)
        ((((lift (M := H) : (a : (i : ι) → H i →* G) → CoprodI H →* G) f : CoprodI H →* G) : (a : CoprodI H) → G)
            (w₁.prod (M := H)) :
          G)
        (X k) ⊆
      X i
hIw₂ :
  ∀ {k : ι} (hk : l ≠ k),
    HSMul.hSMul.{u_4, u_6, u_6} (α := G)
        ((((lift (M := H) : (a : (i : ι) → H i →* G) → CoprodI H →* G) f : CoprodI H →* G) : (a : CoprodI H) → G)
            (w₂.prod (M := H)) :
          G)
        (X k) ⊆
      X k_1
k : ι
hk : l ≠ k
⊢ HSMul.hSMul.{u_4, u_6, u_6} (α := G)
      ((((lift (M := H) : (a : (i : ι) → H i →* G) → CoprodI H →* G) f : CoprodI H →* G) : (a : CoprodI H) → G)
          (w₁.prod (M := H)) :
        G)
      (HSMul.hSMul.{u_4, u_6, u_6} (α := G)
        ((((lift (M := H) : (a : (i : ι) → H i →* G) → CoprodI H →* G) f : CoprodI H →* G) : (a : CoprodI H) → G)
            (w₂.prod (M := H)) :
          G)
        (X k)) ⊆
    HSMul.hSMul.{u_4, u_6, u_6} (α := G)
      ((((lift (M := H) : (a : (i : ι) → H i →* G) → CoprodI H →* G) f : CoprodI H →* G) : (a : CoprodI H) → G)
          (w₁.prod (M := H)) :
        G)
      (X k_1)

Tactic:
smul_set_subset_smul_set_iff.mpr (hIw₂ hk)

Premises used: Iff.mpr, Set.smul_set_subset_smul_set_iff
-- Module: Mathlib.GroupTheory.CoprodI
Goal:
ι : Type u_1
G : Type u_4
inst : Group G
H : ι → Type u_5
inst_1 : (i : ι) → Group (H i)
f : (i : ι) → MonoidHom.{u_5, u_4} (H i) G
α : Type u_6
inst_2 : MulAction G α
X : ι → Set α
hpp :
  Pairwise fun (i j : ι) ↦
    ∀ (h : H i), h ≠ 1 → HSMul.hSMul.{u_4, u_6, u_6} (α := G) ((f i : (a : H i) → G) h : G) (X j) ⊆ X i
i_1 j_1 i j k_1 l : ι
w₁ : NeWord H i j
hne : j ≠ k_1
w₂ : NeWord H k_1 l
hIw₁ :
  ∀ {k : ι} (hk : j ≠ k),
    HSMul.hSMul.{u_4, u_6, u_6} (α := G)
        ((((lift (M := H) : (a : (i : ι) → H i →* G) → CoprodI H →* G) f : CoprodI H →* G) : (a : CoprodI H) → G)
            (w₁.prod (M := H)) :
          G)
        (X k) ⊆
      X i
hIw₂ :
  ∀ {k : ι} (hk : l ≠ k),
    HSMul.hSMul.{u_4, u_6, u_6} (α := G)
        ((((lift (M := H) : (a : (i : ι) → H i →* G) → CoprodI H →* G) f : CoprodI H →* G) : (a : CoprodI H) → G)
            (w₂.prod (M := H)) :
          G)
        (X k) ⊆
      X k_1
k : ι
hk : l ≠ k
⊢ HSMul.hSMul.{u_4, u_6, u_6} (α := G)
      ((((lift (M := H) : (a : (i : ι) → H i →* G) → CoprodI H →* G) f : CoprodI H →* G) : (a : CoprodI H) → G)
          (w₁.prod (M := H)) :
        G)
      (X k_1) ⊆
    X i

Tactic:
hIw₁ hne