-- Mathlib/GroupTheory/CoprodI.lean
theorem mulHead_prod {i j : ι} (w : NeWord M i j) (x : M i) (hnotone : x * w.head ≠ 1) :
    (mulHead w x hnotone).prod = of x * w.prod

Proof state:
case append
ι : Type u_1
M : ι → Type u_2
inst✝ : (i : ι) → Monoid (M i)
i j 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 ≠ 1), (replaceHead (x * _w₁✝.head) hnotone _w₁✝).prod = of x * _w₁✝.prod
w_ih_w₂ : ∀ (x : M k✝) (hnotone : x * _w₂✝.head ≠ 1), (replaceHead (x * _w₂✝.head) hnotone _w₂✝).prod = of x * _w₂✝.prod
x : M i✝
hnotone : x * (_w₁✝.append _hne✝ _w₂✝).head ≠ 1
⊢ (replaceHead (x * (_w₁✝.append _hne✝ _w₂✝).head) hnotone (_w₁✝.append _hne✝ _w₂✝)).prod =
    of x * (_w₁✝.append _hne✝ _w₂✝).prod

Tactic:
specialize w_ih_w₁ _ hnotone

Result:
case append
ι : Type u_1
M : ι → Type u_2
inst✝ : (i : ι) → Monoid (M i)
i j i✝ j✝ k✝ l✝ : ι
_w₁✝ : NeWord M i✝ j✝
_hne✝ : j✝ ≠ k✝
_w₂✝ : NeWord M k✝ l✝
w_ih_w₂ : ∀ (x : M k✝) (hnotone : x * _w₂✝.head ≠ 1), (replaceHead (x * _w₂✝.head) hnotone _w₂✝).prod = of x * _w₂✝.prod
x : M i✝
hnotone : x * (_w₁✝.append _hne✝ _w₂✝).head ≠ 1
w_ih_w₁ : (replaceHead (x * _w₁✝.head) hnotone _w₁✝).prod = of x * _w₁✝.prod
⊢ (replaceHead (x * (_w₁✝.append _hne✝ _w₂✝).head) hnotone (_w₁✝.append _hne✝ _w₂✝)).prod =
    of x * (_w₁✝.append _hne✝ _w₂✝).prod

Proof state:
case append
ι : Type u_1
M : ι → Type u_2
inst✝ : (i : ι) → Monoid (M i)
i j i✝ j✝ k✝ l✝ : ι
_w₁✝ : NeWord M i✝ j✝
_hne✝ : j✝ ≠ k✝
_w₂✝ : NeWord M k✝ l✝
x : M i✝
hnotone : x * (_w₁✝.append _hne✝ _w₂✝).head ≠ 1
w_ih_w₁ : (replaceHead (x * _w₁✝.head) hnotone _w₁✝).prod = of x * _w₁✝.prod
⊢ (replaceHead (x * (_w₁✝.append _hne✝ _w₂✝).head) hnotone (_w₁✝.append _hne✝ _w₂✝)).prod =
    of x * (_w₁✝.append _hne✝ _w₂✝).prod

Tactic:
simp? [replaceHead, ← mul_assoc] at * says
  simp only [replaceHead, head, append_prod, ← mul_assoc] at *

Result:
case append
ι : Type u_1
M : ι → Type u_2
inst✝ : (i : ι) → Monoid (M i)
i j i✝ j✝ k✝ l✝ : ι
_w₁✝ : NeWord M i✝ j✝
_hne✝ : j✝ ≠ k✝
_w₂✝ : NeWord M k✝ l✝
x : M i✝
hnotone : x * (_w₁✝.append _hne✝ _w₂✝).head ≠ 1
w_ih_w₁ : (replaceHead (x * _w₁✝.head) hnotone _w₁✝).prod = of x * _w₁✝.prod
⊢ (replaceHead (x * _w₁✝.head) ⋯ _w₁✝).prod * _w₂✝.prod = of x * _w₁✝.prod * _w₂✝.prod

Proof state:
ι : 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 ≠ 1
⊢ (w.mulHead x hnotone).prod = of x * w.prod

Tactic:
unfold mulHead

Result:
ι : 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 ≠ 1
⊢ (replaceHead (x * w.head) hnotone w).prod = of x * w.prod

Proof state:
case append
ι : Type u_1
M : ι → Type u_2
inst✝ : (i : ι) → Monoid (M i)
i j i✝ j✝ k✝ l✝ : ι
_w₁✝ : NeWord M i✝ j✝
_hne✝ : j✝ ≠ k✝
_w₂✝ : NeWord M k✝ l✝
w_ih_w₂ : ∀ (x : M k✝) (hnotone : x * _w₂✝.head ≠ 1), (replaceHead (x * _w₂✝.head) hnotone _w₂✝).prod = of x * _w₂✝.prod
x : M i✝
hnotone : x * (_w₁✝.append _hne✝ _w₂✝).head ≠ 1
w_ih_w₁ : (replaceHead (x * _w₁✝.head) hnotone _w₁✝).prod = of x * _w₁✝.prod
⊢ (replaceHead (x * (_w₁✝.append _hne✝ _w₂✝).head) hnotone (_w₁✝.append _hne✝ _w₂✝)).prod =
    of x * (_w₁✝.append _hne✝ _w₂✝).prod

Tactic:
clear w_ih_w₂

Result:
case append
ι : Type u_1
M : ι → Type u_2
inst✝ : (i : ι) → Monoid (M i)
i j i✝ j✝ k✝ l✝ : ι
_w₁✝ : NeWord M i✝ j✝
_hne✝ : j✝ ≠ k✝
_w₂✝ : NeWord M k✝ l✝
x : M i✝
hnotone : x * (_w₁✝.append _hne✝ _w₂✝).head ≠ 1
w_ih_w₁ : (replaceHead (x * _w₁✝.head) hnotone _w₁✝).prod = of x * _w₁✝.prod
⊢ (replaceHead (x * (_w₁✝.append _hne✝ _w₂✝).head) hnotone (_w₁✝.append _hne✝ _w₂✝)).prod =
    of x * (_w₁✝.append _hne✝ _w₂✝).prod

Proof state:
case append
ι : Type u_1
M : ι → Type u_2
inst✝ : (i : ι) → Monoid (M i)
i j i✝ j✝ k✝ l✝ : ι
_w₁✝ : NeWord M i✝ j✝
_hne✝ : j✝ ≠ k✝
_w₂✝ : NeWord M k✝ l✝
x : M i✝
hnotone : x * (_w₁✝.append _hne✝ _w₂✝).head ≠ 1
w_ih_w₁ : (replaceHead (x * _w₁✝.head) hnotone _w₁✝).prod = of x * _w₁✝.prod
⊢ (replaceHead (x * _w₁✝.head) ⋯ _w₁✝).prod * _w₂✝.prod = of x * _w₁✝.prod * _w₂✝.prod

Tactic:
congr 1

Result:
no goals

Proof state:
case singleton
ι : Type u_1
M : ι → Type u_2
inst✝ : (i : ι) → Monoid (M i)
i j i✝ : ι
x✝ : M i✝
a✝ : x✝ ≠ 1
x : M i✝
hnotone : x * (singleton x✝ a✝).head ≠ 1
⊢ (replaceHead (x * (singleton x✝ a✝).head) hnotone (singleton x✝ a✝)).prod = of x * (singleton x✝ a✝).prod

Tactic:
simp [mulHead, replaceHead]

Result:
no goals

Proof state:
case append
ι : Type u_1
M : ι → Type u_2
inst✝ : (i : ι) → Monoid (M i)
i j i✝ j✝ k✝ l✝ : ι
_w₁✝ : NeWord M i✝ j✝
_hne✝ : j✝ ≠ k✝
_w₂✝ : NeWord M k✝ l✝
x : M i✝
hnotone : x * (_w₁✝.append _hne✝ _w₂✝).head ≠ 1
w_ih_w₁ : (replaceHead (x * _w₁✝.head) hnotone _w₁✝).prod = of x * _w₁✝.prod
⊢ (replaceHead (x * (_w₁✝.append _hne✝ _w₂✝).head) hnotone (_w₁✝.append _hne✝ _w₂✝)).prod =
    of x * (_w₁✝.append _hne✝ _w₂✝).prod

Tactic:
simp only [replaceHead, head, append_prod, ← mul_assoc] at *

Result:
case append
ι : Type u_1
M : ι → Type u_2
inst✝ : (i : ι) → Monoid (M i)
i j i✝ j✝ k✝ l✝ : ι
_w₁✝ : NeWord M i✝ j✝
_hne✝ : j✝ ≠ k✝
_w₂✝ : NeWord M k✝ l✝
x : M i✝
hnotone : x * (_w₁✝.append _hne✝ _w₂✝).head ≠ 1
w_ih_w₁ : (replaceHead (x * _w₁✝.head) hnotone _w₁✝).prod = of x * _w₁✝.prod
⊢ (replaceHead (x * _w₁✝.head) ⋯ _w₁✝).prod * _w₂✝.prod = of x * _w₁✝.prod * _w₂✝.prod

Proof state:
ι : 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 ≠ 1
⊢ (replaceHead (x * w.head) hnotone w).prod = of x * w.prod

Tactic:
induction w with
| singleton => simp [mulHead, replaceHead]
| append _ _ _ w_ih_w₁ w_ih_w₂ =>
  specialize w_ih_w₁ _ hnotone
  clear w_ih_w₂
  simp? [replaceHead, ← mul_assoc] at * says
    simp only [replaceHead, head, append_prod, ← mul_assoc] at *
  congr 1

Result:
no goals