Module: Mathlib.Algebra.Ring.Ext

Goal state before:
pp: case mk
R : Type u
inst₂ : NonAssocSemiring R
toNonUnitalNonAssocSemiring✝ : NonUnitalNonAssocSemiring R
toOne✝ : One R
one_mul✝ : ∀ (a : R), 1 * a = a
mul_one✝ : ∀ (a : R), a * 1 = a
toNatCast✝ : NatCast R
natCast_zero✝ : ↑0 = 0
natCast_succ✝ : ∀ (n : ℕ), ↑(n + 1) = ↑n + 1
h_add : HAdd.hAdd = HAdd.hAdd
h_mul : HMul.hMul = HMul.hMul
h :
  { toNonUnitalNonAssocSemiring := toNonUnitalNonAssocSemiring✝, toOne := toOne✝, one_mul := one_mul✝,
        mul_one := mul_one✝, toNatCast := toNatCast✝, natCast_zero := natCast_zero✝,
        natCast_succ := natCast_succ✝ }.toNonUnitalNonAssocSemiring =
    inst₂.toNonUnitalNonAssocSemiring
h_zero : Zero.zero = Zero.zero
h_one' :
  { toNonUnitalNonAssocSemiring := toNonUnitalNonAssocSemiring✝, toOne := toOne✝, one_mul := one_mul✝,
          mul_one := mul_one✝, toNatCast := toNatCast✝, natCast_zero := natCast_zero✝,
          natCast_succ := natCast_succ✝ }.toMulZeroOneClass.toOne =
    inst₂.toMulZeroOneClass.toOne
h_one : One.one = One.one
this✝ :
  { toNonUnitalNonAssocSemiring := toNonUnitalNonAssocSemiring✝, toOne := toOne✝, one_mul := one_mul✝,
        mul_one := mul_one✝, toNatCast := toNatCast✝, natCast_zero := natCast_zero✝,
        natCast_succ := natCast_succ✝ }.toAddCommMonoidWithOne =
    inst₂.toAddCommMonoidWithOne
this :
  { toNonUnitalNonAssocSemiring := toNonUnitalNonAssocSemiring✝, toOne := toOne✝, one_mul := one_mul✝,
        mul_one := mul_one✝, toNatCast := toNatCast✝, natCast_zero := natCast_zero✝,
        natCast_succ := natCast_succ✝ }.toNatCast =
    inst₂.toNatCast
⊢ { toNonUnitalNonAssocSemiring := toNonUnitalNonAssocSemiring✝, toOne := toOne✝, one_mul := one_mul✝,
      mul_one := mul_one✝, toNatCast := toNatCast✝, natCast_zero := natCast_zero✝, natCast_succ := natCast_succ✝ } =
    inst₂

Tactic:
;

Goal state after:
case mk
R : Type u
inst₂ : NonAssocSemiring R
toNonUnitalNonAssocSemiring✝ : NonUnitalNonAssocSemiring R
toOne✝ : One R
one_mul✝ : ∀ (a : R), 1 * a = a
mul_one✝ : ∀ (a : R), a * 1 = a
toNatCast✝ : NatCast R
natCast_zero✝ : ↑0 = 0
natCast_succ✝ : ∀ (n : ℕ), ↑(n + 1) = ↑n + 1
h_add : HAdd.hAdd = HAdd.hAdd
h_mul : HMul.hMul = HMul.hMul
h :
  { toNonUnitalNonAssocSemiring := toNonUnitalNonAssocSemiring✝, toOne := toOne✝, one_mul := one_mul✝,
        mul_one := mul_one✝, toNatCast := toNatCast✝, natCast_zero := natCast_zero✝,
        natCast_succ := natCast_succ✝ }.toNonUnitalNonAssocSemiring =
    inst₂.toNonUnitalNonAssocSemiring
h_zero : Zero.zero = Zero.zero
h_one' :
  { toNonUnitalNonAssocSemiring := toNonUnitalNonAssocSemiring✝, toOne := toOne✝, one_mul := one_mul✝,
          mul_one := mul_one✝, toNatCast := toNatCast✝, natCast_zero := natCast_zero✝,
          natCast_succ := natCast_succ✝ }.toMulZeroOneClass.toOne =
    inst₂.toMulZeroOneClass.toOne
h_one : One.one = One.one
this✝ :
  { toNonUnitalNonAssocSemiring := toNonUnitalNonAssocSemiring✝, toOne := toOne✝, one_mul := one_mul✝,
        mul_one := mul_one✝, toNatCast := toNatCast✝, natCast_zero := natCast_zero✝,
        natCast_succ := natCast_succ✝ }.toAddCommMonoidWithOne =
    inst₂.toAddCommMonoidWithOne
this :
  { toNonUnitalNonAssocSemiring := toNonUnitalNonAssocSemiring✝, toOne := toOne✝, one_mul := one_mul✝,
        mul_one := mul_one✝, toNatCast := toNatCast✝, natCast_zero := natCast_zero✝,
        natCast_succ := natCast_succ✝ }.toNatCast =
    inst₂.toNatCast
⊢ { toNonUnitalNonAssocSemiring := toNonUnitalNonAssocSemiring✝, toOne := toOne✝, one_mul := one_mul✝,
      mul_one := mul_one✝, toNatCast := toNatCast✝, natCast_zero := natCast_zero✝, natCast_succ := natCast_succ✝ } =
    inst₂