-- Mathlib/Algebra/Group/Ext.lean
theorem Monoid.ext {M : Type u} ⦃m₁ m₂ : Monoid M⦄
    (h_mul : (letI := m₁; HMul.hMul : M → M → M) = (letI := m₂; HMul.hMul : M → M → M)) :
    m₁ = m₂

Proof state:
case mk.mk.mk.mk.mk.mk.mk.mk
M : Type u
npow✝¹ : ℕ → M → M
mul✝¹ : M → M → M
mul_assoc✝¹ : ∀ (a b c : M), a * b * c = a * (b * c)
npow_succ✝¹ : ∀ (n : ℕ) (x : M), npow✝¹ (n + 1) x = npow✝¹ n x * x
one✝¹ : M
npow_zero✝¹ : ∀ (x : M), npow✝¹ 0 x = 1
one_mul✝¹ : ∀ (a : M), 1 * a = a
mul_one✝¹ : ∀ (a : M), a * 1 = a
npow✝ : ℕ → M → M
mul✝ : M → M → M
mul_assoc✝ : ∀ (a b c : M), a * b * c = a * (b * c)
npow_succ✝ : ∀ (n : ℕ) (x : M), npow✝ (n + 1) x = npow✝ n x * x
one✝ : M
npow_zero✝ : ∀ (x : M), npow✝ 0 x = 1
one_mul✝ : ∀ (a : M), 1 * a = a
mul_one✝ : ∀ (a : M), a * 1 = a
h_mul : HMul.hMul = HMul.hMul
this✝ : toMulOneClass = toMulOneClass
h₁ : One.one = One.one
f : M →* M := { toFun := id, map_one' := h₁, map_mul' := ⋯ }
this : Monoid.npow = Monoid.npow
⊢ mk one_mul✝¹ mul_one✝¹ npow✝¹ npow_zero✝¹ npow_succ✝¹ = mk one_mul✝ mul_one✝ npow✝ npow_zero✝ npow_succ✝

Tactic:
congr

Result:
no goals

Proof state:
case h.h
M : Type u
m₁ m₂ : Monoid M
h_mul : HMul.hMul = HMul.hMul
this : toMulOneClass = toMulOneClass
h₁ : One.one = One.one
f : M →* M := { toFun := id, map_one' := h₁, map_mul' := ⋯ }
n : ℕ
x : M
⊢ Monoid.npow n x = Monoid.npow n x

Tactic:
exact @MonoidHom.map_pow M M m₁ m₂ f x n

Result:
no goals

Proof state:
M : Type u
m₁ m₂ : Monoid M
h_mul : HMul.hMul = HMul.hMul
this : toMulOneClass = toMulOneClass
h₁ : One.one = One.one
⊢ m₁ = m₂

Tactic:
let f : @MonoidHom M M m₁.toMulOneClass m₂.toMulOneClass :=
  @MonoidHom.mk _ _ (_) _ (@OneHom.mk _ _ (_) _ id h₁)
    (fun x y => congr_fun (congr_fun h_mul x) y)

Result:
M : Type u
m₁ m₂ : Monoid M
h_mul : HMul.hMul = HMul.hMul
this : toMulOneClass = toMulOneClass
h₁ : One.one = One.one
f : M →* M := { toFun := id, map_one' := h₁, map_mul' := ⋯ }
⊢ m₁ = m₂

Proof state:
M : Type u
m₁ m₂ : Monoid M
h_mul : HMul.hMul = HMul.hMul
this : toMulOneClass = toMulOneClass
h₁ : One.one = One.one
f : M →* M := { toFun := id, map_one' := h₁, map_mul' := ⋯ }
⊢ m₁ = m₂

Tactic:
have : m₁.npow = m₂.npow := by
  ext n x
  exact @MonoidHom.map_pow M M m₁ m₂ f x n

Result:
M : Type u
m₁ m₂ : Monoid M
h_mul : HMul.hMul = HMul.hMul
this✝ : toMulOneClass = toMulOneClass
h₁ : One.one = One.one
f : M →* M := { toFun := id, map_one' := h₁, map_mul' := ⋯ }
this : Monoid.npow = Monoid.npow
⊢ m₁ = m₂

Proof state:
case mk.mk.mk.mk
M : Type u
m₂ : Monoid M
npow✝ : ℕ → M → M
mul✝ : M → M → M
mul_assoc✝ : ∀ (a b c : M), a * b * c = a * (b * c)
npow_succ✝ : ∀ (n : ℕ) (x : M), npow✝ (n + 1) x = npow✝ n x * x
one✝ : M
npow_zero✝ : ∀ (x : M), npow✝ 0 x = 1
one_mul✝ : ∀ (a : M), 1 * a = a
mul_one✝ : ∀ (a : M), a * 1 = a
h_mul : HMul.hMul = HMul.hMul
this✝ : toMulOneClass = toMulOneClass
h₁ : One.one = One.one
f : M →* M := { toFun := id, map_one' := h₁, map_mul' := ⋯ }
this : Monoid.npow = Monoid.npow
⊢ mk one_mul✝ mul_one✝ npow✝ npow_zero✝ npow_succ✝ = m₂

Tactic:
rcases m₂ with @⟨@⟨⟨_⟩⟩, ⟨_⟩⟩

Result:
case mk.mk.mk.mk.mk.mk.mk.mk
M : Type u
npow✝¹ : ℕ → M → M
mul✝¹ : M → M → M
mul_assoc✝¹ : ∀ (a b c : M), a * b * c = a * (b * c)
npow_succ✝¹ : ∀ (n : ℕ) (x : M), npow✝¹ (n + 1) x = npow✝¹ n x * x
one✝¹ : M
npow_zero✝¹ : ∀ (x : M), npow✝¹ 0 x = 1
one_mul✝¹ : ∀ (a : M), 1 * a = a
mul_one✝¹ : ∀ (a : M), a * 1 = a
npow✝ : ℕ → M → M
mul✝ : M → M → M
mul_assoc✝ : ∀ (a b c : M), a * b * c = a * (b * c)
npow_succ✝ : ∀ (n : ℕ) (x : M), npow✝ (n + 1) x = npow✝ n x * x
one✝ : M
npow_zero✝ : ∀ (x : M), npow✝ 0 x = 1
one_mul✝ : ∀ (a : M), 1 * a = a
mul_one✝ : ∀ (a : M), a * 1 = a
h_mul : HMul.hMul = HMul.hMul
this✝ : toMulOneClass = toMulOneClass
h₁ : One.one = One.one
f : M →* M := { toFun := id, map_one' := h₁, map_mul' := ⋯ }
this : Monoid.npow = Monoid.npow
⊢ mk one_mul✝¹ mul_one✝¹ npow✝¹ npow_zero✝¹ npow_succ✝¹ = mk one_mul✝ mul_one✝ npow✝ npow_zero✝ npow_succ✝

Proof state:
M : Type u
m₁ m₂ : Monoid M
h_mul : HMul.hMul = HMul.hMul
this : toMulOneClass = toMulOneClass
h₁ : One.one = One.one
f : M →* M := { toFun := id, map_one' := h₁, map_mul' := ⋯ }
⊢ Monoid.npow = Monoid.npow

Tactic:
ext n x

Result:
case h.h
M : Type u
m₁ m₂ : Monoid M
h_mul : HMul.hMul = HMul.hMul
this : toMulOneClass = toMulOneClass
h₁ : One.one = One.one
f : M →* M := { toFun := id, map_one' := h₁, map_mul' := ⋯ }
n : ℕ
x : M
⊢ Monoid.npow n x = Monoid.npow n x

Proof state:
M : Type u
m₁ m₂ : Monoid M
h_mul : HMul.hMul = HMul.hMul
this✝ : toMulOneClass = toMulOneClass
h₁ : One.one = One.one
f : M →* M := { toFun := id, map_one' := h₁, map_mul' := ⋯ }
this : Monoid.npow = Monoid.npow
⊢ m₁ = m₂

Tactic:
rcases m₁ with @⟨@⟨⟨_⟩⟩, ⟨_⟩⟩

Result:
case mk.mk.mk.mk
M : Type u
m₂ : Monoid M
npow✝ : ℕ → M → M
mul✝ : M → M → M
mul_assoc✝ : ∀ (a b c : M), a * b * c = a * (b * c)
npow_succ✝ : ∀ (n : ℕ) (x : M), npow✝ (n + 1) x = npow✝ n x * x
one✝ : M
npow_zero✝ : ∀ (x : M), npow✝ 0 x = 1
one_mul✝ : ∀ (a : M), 1 * a = a
mul_one✝ : ∀ (a : M), a * 1 = a
h_mul : HMul.hMul = HMul.hMul
this✝ : toMulOneClass = toMulOneClass
h₁ : One.one = One.one
f : M →* M := { toFun := id, map_one' := h₁, map_mul' := ⋯ }
this : Monoid.npow = Monoid.npow
⊢ mk one_mul✝ mul_one✝ npow✝ npow_zero✝ npow_succ✝ = m₂

Proof state:
M : Type u
m₁ m₂ : Monoid M
h_mul : HMul.hMul = HMul.hMul
⊢ m₁ = m₂

Tactic:
have : m₁.toMulOneClass = m₂.toMulOneClass := MulOneClass.ext h_mul

Result:
M : Type u
m₁ m₂ : Monoid M
h_mul : HMul.hMul = HMul.hMul
this : toMulOneClass = toMulOneClass
⊢ m₁ = m₂