-- Mathlib/Algebra/Group/Ext.lean
theorem CancelCommMonoid.toCommMonoid_injective {M : Type u} :
    Function.Injective (@CancelCommMonoid.toCommMonoid M)

Proof state:
case mk.mk.mk.mk.mk.mk.e_toCommMonoid.e_toMonoid.e_npow
M : Type u
toSemigroup✝¹ : Semigroup M
toOne✝¹ : One M
one_mul✝¹ : ∀ (a : M), 1 * a = a
mul_one✝¹ : ∀ (a : M), a * 1 = a
npow✝¹ : ℕ → M → M
npow_zero✝¹ : ∀ (x : M), npow✝¹ 0 x = 1
npow_succ✝¹ : ∀ (n : ℕ) (x : M), npow✝¹ (n + 1) x = npow✝¹ n x * x
mul_comm✝¹ : ∀ (a b : M), a * b = b * a
mul_left_cancel✝¹ : ∀ (a b c : M), a * b = a * c → b = c
toSemigroup✝ : Semigroup M
toOne✝ : One M
one_mul✝ : ∀ (a : M), 1 * a = a
mul_one✝ : ∀ (a : M), a * 1 = a
npow✝ : ℕ → M → M
npow_zero✝ : ∀ (x : M), npow✝ 0 x = 1
npow_succ✝ : ∀ (n : ℕ) (x : M), npow✝ (n + 1) x = npow✝ n x * x
mul_comm✝ : ∀ (a b : M), a * b = b * a
mul_left_cancel✝ : ∀ (a b c : M), a * b = a * c → b = c
h : toCommMonoid = toCommMonoid
⊢ npow✝¹ = npow✝

Tactic:
injection h with h'

Result:
case mk.mk.mk.mk.mk.mk.e_toCommMonoid.e_toMonoid.e_npow
M : Type u
toSemigroup✝¹ : Semigroup M
toOne✝¹ : One M
one_mul✝¹ : ∀ (a : M), 1 * a = a
mul_one✝¹ : ∀ (a : M), a * 1 = a
npow✝¹ : ℕ → M → M
npow_zero✝¹ : ∀ (x : M), npow✝¹ 0 x = 1
npow_succ✝¹ : ∀ (n : ℕ) (x : M), npow✝¹ (n + 1) x = npow✝¹ n x * x
mul_comm✝¹ : ∀ (a b : M), a * b = b * a
mul_left_cancel✝¹ : ∀ (a b c : M), a * b = a * c → b = c
toSemigroup✝ : Semigroup M
toOne✝ : One M
one_mul✝ : ∀ (a : M), 1 * a = a
mul_one✝ : ∀ (a : M), a * 1 = a
npow✝ : ℕ → M → M
npow_zero✝ : ∀ (x : M), npow✝ 0 x = 1
npow_succ✝ : ∀ (n : ℕ) (x : M), npow✝ (n + 1) x = npow✝ n x * x
mul_comm✝ : ∀ (a b : M), a * b = b * a
mul_left_cancel✝ : ∀ (a b c : M), a * b = a * c → b = c
h' :
  Monoid.mk one_mul✝¹ mul_one✝¹ npow✝¹ npow_zero✝¹ npow_succ✝¹ = Monoid.mk one_mul✝ mul_one✝ npow✝ npow_zero✝ npow_succ✝
⊢ npow✝¹ = npow✝

Proof state:
M : Type u
⊢ Injective (@toCommMonoid M)

Tactic:
rintro @⟨@⟨@⟨⟩⟩⟩ @⟨@⟨@⟨⟩⟩⟩ h

Result:
case mk.mk.mk.mk.mk.mk
M : Type u
toSemigroup✝¹ : Semigroup M
toOne✝¹ : One M
one_mul✝¹ : ∀ (a : M), 1 * a = a
mul_one✝¹ : ∀ (a : M), a * 1 = a
npow✝¹ : ℕ → M → M
npow_zero✝¹ : ∀ (x : M), npow✝¹ 0 x = 1
npow_succ✝¹ : ∀ (n : ℕ) (x : M), npow✝¹ (n + 1) x = npow✝¹ n x * x
mul_comm✝¹ : ∀ (a b : M), a * b = b * a
mul_left_cancel✝¹ : ∀ (a b c : M), a * b = a * c → b = c
toSemigroup✝ : Semigroup M
toOne✝ : One M
one_mul✝ : ∀ (a : M), 1 * a = a
mul_one✝ : ∀ (a : M), a * 1 = a
npow✝ : ℕ → M → M
npow_zero✝ : ∀ (x : M), npow✝ 0 x = 1
npow_succ✝ : ∀ (n : ℕ) (x : M), npow✝ (n + 1) x = npow✝ n x * x
mul_comm✝ : ∀ (a b : M), a * b = b * a
mul_left_cancel✝ : ∀ (a b c : M), a * b = a * c → b = c
h : toCommMonoid = toCommMonoid
⊢ mk mul_left_cancel✝¹ = mk mul_left_cancel✝

Proof state:
case mk.mk.mk.mk.mk.mk.e_toCommMonoid.e_toMonoid.e_npow
M : Type u
toSemigroup✝¹ : Semigroup M
toOne✝¹ : One M
one_mul✝¹ : ∀ (a : M), 1 * a = a
mul_one✝¹ : ∀ (a : M), a * 1 = a
npow✝¹ : ℕ → M → M
npow_zero✝¹ : ∀ (x : M), npow✝¹ 0 x = 1
npow_succ✝¹ : ∀ (n : ℕ) (x : M), npow✝¹ (n + 1) x = npow✝¹ n x * x
mul_comm✝¹ : ∀ (a b : M), a * b = b * a
mul_left_cancel✝¹ : ∀ (a b c : M), a * b = a * c → b = c
toSemigroup✝ : Semigroup M
toOne✝ : One M
one_mul✝ : ∀ (a : M), 1 * a = a
mul_one✝ : ∀ (a : M), a * 1 = a
npow✝ : ℕ → M → M
npow_zero✝ : ∀ (x : M), npow✝ 0 x = 1
npow_succ✝ : ∀ (n : ℕ) (x : M), npow✝ (n + 1) x = npow✝ n x * x
mul_comm✝ : ∀ (a b : M), a * b = b * a
mul_left_cancel✝ : ∀ (a b c : M), a * b = a * c → b = c
h' :
  Monoid.mk one_mul✝¹ mul_one✝¹ npow✝¹ npow_zero✝¹ npow_succ✝¹ = Monoid.mk one_mul✝ mul_one✝ npow✝ npow_zero✝ npow_succ✝
⊢ npow✝¹ = npow✝

Tactic:
injection h'

Result:
no goals

Proof state:
case mk.mk.mk.mk.mk.mk
M : Type u
toSemigroup✝¹ : Semigroup M
toOne✝¹ : One M
one_mul✝¹ : ∀ (a : M), 1 * a = a
mul_one✝¹ : ∀ (a : M), a * 1 = a
npow✝¹ : ℕ → M → M
npow_zero✝¹ : ∀ (x : M), npow✝¹ 0 x = 1
npow_succ✝¹ : ∀ (n : ℕ) (x : M), npow✝¹ (n + 1) x = npow✝¹ n x * x
mul_comm✝¹ : ∀ (a b : M), a * b = b * a
mul_left_cancel✝¹ : ∀ (a b c : M), a * b = a * c → b = c
toSemigroup✝ : Semigroup M
toOne✝ : One M
one_mul✝ : ∀ (a : M), 1 * a = a
mul_one✝ : ∀ (a : M), a * 1 = a
npow✝ : ℕ → M → M
npow_zero✝ : ∀ (x : M), npow✝ 0 x = 1
npow_succ✝ : ∀ (n : ℕ) (x : M), npow✝ (n + 1) x = npow✝ n x * x
mul_comm✝ : ∀ (a b : M), a * b = b * a
mul_left_cancel✝ : ∀ (a b c : M), a * b = a * c → b = c
h : toCommMonoid = toCommMonoid
⊢ mk mul_left_cancel✝¹ = mk mul_left_cancel✝

Tactic:
congr <;> {
  injection h with h'
  injection h' }

Result:
no goals