-- Mathlib/Algebra/Ring/Ext.lean
theorem ext ⦃inst₁ inst₂ : Semiring R⦄
    (h_add : local_hAdd[R, inst₁] = local_hAdd[R, inst₂])
    (h_mul : local_hMul[R, inst₁] = local_hMul[R, inst₂]) :
    inst₁ = inst₂

Proof state:
R : Type u
inst₁ inst₂ : Semiring R
h_add : HAdd.hAdd = HAdd.hAdd
h_mul : HMul.hMul = HMul.hMul
h₁ : toNonUnitalSemiring = toNonUnitalSemiring
h₂ : toNonAssocSemiring = toNonAssocSemiring
⊢ MonoidWithZero.toMonoid = MonoidWithZero.toMonoid

Tactic:
ext : 1

Result:
case h_mul
R : Type u
inst₁ inst₂ : Semiring R
h_add : HAdd.hAdd = HAdd.hAdd
h_mul : HMul.hMul = HMul.hMul
h₁ : toNonUnitalSemiring = toNonUnitalSemiring
h₂ : toNonAssocSemiring = toNonAssocSemiring
⊢ HMul.hMul = HMul.hMul

Proof state:
case mk.mk.e_npow
R : Type u
toNonUnitalSemiring✝¹ : NonUnitalSemiring R
toOne✝¹ : One R
one_mul✝¹ : ∀ (a : R), 1 * a = a
mul_one✝¹ : ∀ (a : R), a * 1 = a
toNatCast✝¹ : NatCast R
natCast_zero✝¹ : NatCast.natCast 0 = 0
natCast_succ✝¹ : ∀ (n : ℕ), NatCast.natCast (n + 1) = NatCast.natCast n + 1
npow✝¹ : ℕ → R → R
npow_zero✝¹ : ∀ (x : R), npow✝¹ 0 x = 1
npow_succ✝¹ : ∀ (n : ℕ) (x : R), npow✝¹ (n + 1) x = npow✝¹ n x * x
toNonUnitalSemiring✝ : NonUnitalSemiring R
toOne✝ : One R
one_mul✝ : ∀ (a : R), 1 * a = a
mul_one✝ : ∀ (a : R), a * 1 = a
toNatCast✝ : NatCast R
natCast_zero✝ : NatCast.natCast 0 = 0
natCast_succ✝ : ∀ (n : ℕ), NatCast.natCast (n + 1) = NatCast.natCast n + 1
npow✝ : ℕ → R → R
npow_zero✝ : ∀ (x : R), npow✝ 0 x = 1
npow_succ✝ : ∀ (n : ℕ) (x : R), npow✝ (n + 1) x = npow✝ n x * x
h_add : HAdd.hAdd = HAdd.hAdd
h_mul : HMul.hMul = HMul.hMul
h₁ : toNonUnitalSemiring = toNonUnitalSemiring
h₂ : toNonAssocSemiring = toNonAssocSemiring
h₃ : MonoidWithZero.toMonoid = MonoidWithZero.toMonoid
⊢ npow✝¹ = npow✝

Tactic:
injection h₂

Result:
case mk.mk.e_npow
R : Type u
toNonUnitalSemiring✝¹ : NonUnitalSemiring R
toOne✝¹ : One R
one_mul✝¹ : ∀ (a : R), 1 * a = a
mul_one✝¹ : ∀ (a : R), a * 1 = a
toNatCast✝¹ : NatCast R
natCast_zero✝¹ : NatCast.natCast 0 = 0
natCast_succ✝¹ : ∀ (n : ℕ), NatCast.natCast (n + 1) = NatCast.natCast n + 1
npow✝¹ : ℕ → R → R
npow_zero✝¹ : ∀ (x : R), npow✝¹ 0 x = 1
npow_succ✝¹ : ∀ (n : ℕ) (x : R), npow✝¹ (n + 1) x = npow✝¹ n x * x
toNonUnitalSemiring✝ : NonUnitalSemiring R
toOne✝ : One R
one_mul✝ : ∀ (a : R), 1 * a = a
mul_one✝ : ∀ (a : R), a * 1 = a
toNatCast✝ : NatCast R
natCast_zero✝ : NatCast.natCast 0 = 0
natCast_succ✝ : ∀ (n : ℕ), NatCast.natCast (n + 1) = NatCast.natCast n + 1
npow✝ : ℕ → R → R
npow_zero✝ : ∀ (x : R), npow✝ 0 x = 1
npow_succ✝ : ∀ (n : ℕ) (x : R), npow✝ (n + 1) x = npow✝ n x * x
h_add : HAdd.hAdd = HAdd.hAdd
h_mul : HMul.hMul = HMul.hMul
h₁ : toNonUnitalSemiring = toNonUnitalSemiring
h₃ : MonoidWithZero.toMonoid = MonoidWithZero.toMonoid
toNonUnitalNonAssocSemiring_eq✝ :
  NonUnitalSemiring.toNonUnitalNonAssocSemiring = NonUnitalSemiring.toNonUnitalNonAssocSemiring
toOne_eq✝ : toOne = toOne
toNatCast_eq✝ : toNatCast = toNatCast
⊢ npow✝¹ = npow✝

Proof state:
R : Type u
inst₁ inst₂ : Semiring R
h_add : HAdd.hAdd = HAdd.hAdd
h_mul : HMul.hMul = HMul.hMul
h₁ : toNonUnitalSemiring = toNonUnitalSemiring
h₂ : toNonAssocSemiring = toNonAssocSemiring
⊢ inst₁ = inst₂

Tactic:
have h₃ : (inst₁.toMonoidWithZero).toMonoid = (inst₂.toMonoidWithZero).toMonoid := by
  ext : 1; exact h_mul

Result:
R : Type u
inst₁ inst₂ : Semiring R
h_add : HAdd.hAdd = HAdd.hAdd
h_mul : HMul.hMul = HMul.hMul
h₁ : toNonUnitalSemiring = toNonUnitalSemiring
h₂ : toNonAssocSemiring = toNonAssocSemiring
h₃ : MonoidWithZero.toMonoid = MonoidWithZero.toMonoid
⊢ inst₁ = inst₂

Proof state:
R : Type u
inst₁ inst₂ : Semiring R
h_add : HAdd.hAdd = HAdd.hAdd
h_mul : HMul.hMul = HMul.hMul
h₁ : toNonUnitalSemiring = toNonUnitalSemiring
h₂ : toNonAssocSemiring = toNonAssocSemiring
h₃ : MonoidWithZero.toMonoid = MonoidWithZero.toMonoid
⊢ inst₁ = inst₂

Tactic:
cases inst₁

Result:
case mk
R : Type u
inst₂ : Semiring R
toNonUnitalSemiring✝ : NonUnitalSemiring R
toOne✝ : One R
one_mul✝ : ∀ (a : R), 1 * a = a
mul_one✝ : ∀ (a : R), a * 1 = a
toNatCast✝ : NatCast R
natCast_zero✝ : NatCast.natCast 0 = 0
natCast_succ✝ : ∀ (n : ℕ), NatCast.natCast (n + 1) = NatCast.natCast n + 1
npow✝ : ℕ → R → R
npow_zero✝ : ∀ (x : R), npow✝ 0 x = 1
npow_succ✝ : ∀ (n : ℕ) (x : R), npow✝ (n + 1) x = npow✝ n x * x
h_add : HAdd.hAdd = HAdd.hAdd
h_mul : HMul.hMul = HMul.hMul
h₁ : toNonUnitalSemiring = toNonUnitalSemiring
h₂ : toNonAssocSemiring = toNonAssocSemiring
h₃ : MonoidWithZero.toMonoid = MonoidWithZero.toMonoid
⊢ mk one_mul✝ mul_one✝ natCast_zero✝ natCast_succ✝ npow✝ npow_zero✝ npow_succ✝ = inst₂

Proof state:
case mk.mk.e_npow
R : Type u
toNonUnitalSemiring✝¹ : NonUnitalSemiring R
toOne✝¹ : One R
one_mul✝¹ : ∀ (a : R), 1 * a = a
mul_one✝¹ : ∀ (a : R), a * 1 = a
toNatCast✝¹ : NatCast R
natCast_zero✝¹ : NatCast.natCast 0 = 0
natCast_succ✝¹ : ∀ (n : ℕ), NatCast.natCast (n + 1) = NatCast.natCast n + 1
npow✝¹ : ℕ → R → R
npow_zero✝¹ : ∀ (x : R), npow✝¹ 0 x = 1
npow_succ✝¹ : ∀ (n : ℕ) (x : R), npow✝¹ (n + 1) x = npow✝¹ n x * x
toNonUnitalSemiring✝ : NonUnitalSemiring R
toOne✝ : One R
one_mul✝ : ∀ (a : R), 1 * a = a
mul_one✝ : ∀ (a : R), a * 1 = a
toNatCast✝ : NatCast R
natCast_zero✝ : NatCast.natCast 0 = 0
natCast_succ✝ : ∀ (n : ℕ), NatCast.natCast (n + 1) = NatCast.natCast n + 1
npow✝ : ℕ → R → R
npow_zero✝ : ∀ (x : R), npow✝ 0 x = 1
npow_succ✝ : ∀ (n : ℕ) (x : R), npow✝ (n + 1) x = npow✝ n x * x
h_add : HAdd.hAdd = HAdd.hAdd
h_mul : HMul.hMul = HMul.hMul
h₁ : toNonUnitalSemiring = toNonUnitalSemiring
h₂ : toNonAssocSemiring = toNonAssocSemiring
h₃ : MonoidWithZero.toMonoid = MonoidWithZero.toMonoid
⊢ npow✝¹ = npow✝

Tactic:
injection h₃

Result:
no goals

Proof state:
case mk
R : Type u
inst₂ : Semiring R
toNonUnitalSemiring✝ : NonUnitalSemiring R
toOne✝ : One R
one_mul✝ : ∀ (a : R), 1 * a = a
mul_one✝ : ∀ (a : R), a * 1 = a
toNatCast✝ : NatCast R
natCast_zero✝ : NatCast.natCast 0 = 0
natCast_succ✝ : ∀ (n : ℕ), NatCast.natCast (n + 1) = NatCast.natCast n + 1
npow✝ : ℕ → R → R
npow_zero✝ : ∀ (x : R), npow✝ 0 x = 1
npow_succ✝ : ∀ (n : ℕ) (x : R), npow✝ (n + 1) x = npow✝ n x * x
h_add : HAdd.hAdd = HAdd.hAdd
h_mul : HMul.hMul = HMul.hMul
h₁ : toNonUnitalSemiring = toNonUnitalSemiring
h₂ : toNonAssocSemiring = toNonAssocSemiring
h₃ : MonoidWithZero.toMonoid = MonoidWithZero.toMonoid
⊢ mk one_mul✝ mul_one✝ natCast_zero✝ natCast_succ✝ npow✝ npow_zero✝ npow_succ✝ = inst₂

Tactic:
cases inst₂

Result:
case mk.mk
R : Type u
toNonUnitalSemiring✝¹ : NonUnitalSemiring R
toOne✝¹ : One R
one_mul✝¹ : ∀ (a : R), 1 * a = a
mul_one✝¹ : ∀ (a : R), a * 1 = a
toNatCast✝¹ : NatCast R
natCast_zero✝¹ : NatCast.natCast 0 = 0
natCast_succ✝¹ : ∀ (n : ℕ), NatCast.natCast (n + 1) = NatCast.natCast n + 1
npow✝¹ : ℕ → R → R
npow_zero✝¹ : ∀ (x : R), npow✝¹ 0 x = 1
npow_succ✝¹ : ∀ (n : ℕ) (x : R), npow✝¹ (n + 1) x = npow✝¹ n x * x
toNonUnitalSemiring✝ : NonUnitalSemiring R
toOne✝ : One R
one_mul✝ : ∀ (a : R), 1 * a = a
mul_one✝ : ∀ (a : R), a * 1 = a
toNatCast✝ : NatCast R
natCast_zero✝ : NatCast.natCast 0 = 0
natCast_succ✝ : ∀ (n : ℕ), NatCast.natCast (n + 1) = NatCast.natCast n + 1
npow✝ : ℕ → R → R
npow_zero✝ : ∀ (x : R), npow✝ 0 x = 1
npow_succ✝ : ∀ (n : ℕ) (x : R), npow✝ (n + 1) x = npow✝ n x * x
h_add : HAdd.hAdd = HAdd.hAdd
h_mul : HMul.hMul = HMul.hMul
h₁ : toNonUnitalSemiring = toNonUnitalSemiring
h₂ : toNonAssocSemiring = toNonAssocSemiring
h₃ : MonoidWithZero.toMonoid = MonoidWithZero.toMonoid
⊢ mk one_mul✝¹ mul_one✝¹ natCast_zero✝¹ natCast_succ✝¹ npow✝¹ npow_zero✝¹ npow_succ✝¹ =
    mk one_mul✝ mul_one✝ natCast_zero✝ natCast_succ✝ npow✝ npow_zero✝ npow_succ✝

Proof state:
R : Type u
inst₁ inst₂ : Semiring R
h_add : HAdd.hAdd = HAdd.hAdd
h_mul : HMul.hMul = HMul.hMul
⊢ toNonUnitalSemiring = toNonUnitalSemiring

Tactic:
ext : 1 <;> assumption

Result:
no goals