Module: Mathlib.Algebra.Ring.Ext

Goal state before:
pp: case mk.mk
R : Type u
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
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 =
    { toNonUnitalNonAssocSemiring := toNonUnitalNonAssocSemiring✝, toOne := toOne✝, one_mul := one_mul✝,
        mul_one := mul_one✝, toNatCast := toNatCast✝, natCast_zero := natCast_zero✝,
        natCast_succ := natCast_succ✝ }.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 =
    { toNonUnitalNonAssocSemiring := toNonUnitalNonAssocSemiring✝, toOne := toOne✝, one_mul := one_mul✝,
          mul_one := mul_one✝, toNatCast := toNatCast✝, natCast_zero := natCast_zero✝,
          natCast_succ := natCast_succ✝ }.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 =
    { toNonUnitalNonAssocSemiring := toNonUnitalNonAssocSemiring✝, toOne := toOne✝, one_mul := one_mul✝,
        mul_one := mul_one✝, toNatCast := toNatCast✝, natCast_zero := natCast_zero✝,
        natCast_succ := natCast_succ✝ }.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 =
    { toNonUnitalNonAssocSemiring := toNonUnitalNonAssocSemiring✝, toOne := toOne✝, one_mul := one_mul✝,
        mul_one := mul_one✝, toNatCast := toNatCast✝, natCast_zero := natCast_zero✝,
        natCast_succ := natCast_succ✝ }.toNatCast
⊢ { toNonUnitalNonAssocSemiring := toNonUnitalNonAssocSemiring✝¹, toOne := toOne✝¹, one_mul := one_mul✝¹,
      mul_one := mul_one✝¹, toNatCast := toNatCast✝¹, natCast_zero := natCast_zero✝¹, natCast_succ := natCast_succ✝¹ } =
    { toNonUnitalNonAssocSemiring := toNonUnitalNonAssocSemiring✝, toOne := toOne✝, one_mul := one_mul✝,
      mul_one := mul_one✝, toNatCast := toNatCast✝, natCast_zero := natCast_zero✝, natCast_succ := natCast_succ✝ }

Tactic:
congr

Goal state after: