Module: Mathlib.Algebra.Ring.Ext

Goal state before:
pp: case mk.mk
R : Type u
toAddCommMonoid✝¹ : AddCommMonoid R
toMonoid✝¹ : Monoid R
zero_mul✝¹ : ∀ (a : R), 0 * a = 0
mul_zero✝¹ : ∀ (a : R), a * 0 = 0
left_distrib✝¹ : ∀ (a b c : R), a * (b + c) = a * b + a * c
right_distrib✝¹ : ∀ (a b c : R), (a + b) * c = a * c + b * c
toNatCast✝¹ : NatCast R
natCast_zero✝¹ : ↑0 = 0
natCast_succ✝¹ : ∀ (n : ℕ), ↑(n + 1) = ↑n + 1
toAddCommMonoid✝ : AddCommMonoid R
toMonoid✝ : Monoid R
zero_mul✝ : ∀ (a : R), 0 * a = 0
mul_zero✝ : ∀ (a : R), a * 0 = 0
left_distrib✝ : ∀ (a b c : R), a * (b + c) = a * b + a * c
right_distrib✝ : ∀ (a b c : R), (a + b) * c = a * c + b * c
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₀ :
  { toAddCommMonoid := toAddCommMonoid✝¹, toMonoid := toMonoid✝¹, zero_mul := zero_mul✝¹, mul_zero := mul_zero✝¹,
        left_distrib := left_distrib✝¹, right_distrib := right_distrib✝¹, toNatCast := toNatCast✝¹,
        natCast_zero := natCast_zero✝¹, natCast_succ := natCast_succ✝¹ }.toAddCommMonoid =
    { toAddCommMonoid := toAddCommMonoid✝, toMonoid := toMonoid✝, zero_mul := zero_mul✝, mul_zero := mul_zero✝,
        left_distrib := left_distrib✝, right_distrib := right_distrib✝, toNatCast := toNatCast✝,
        natCast_zero := natCast_zero✝, natCast_succ := natCast_succ✝ }.toAddCommMonoid
h₁ :
  { toAddCommMonoid := toAddCommMonoid✝¹, toMonoid := toMonoid✝¹, zero_mul := zero_mul✝¹, mul_zero := mul_zero✝¹,
        left_distrib := left_distrib✝¹, right_distrib := right_distrib✝¹, toNatCast := toNatCast✝¹,
        natCast_zero := natCast_zero✝¹, natCast_succ := natCast_succ✝¹ }.toNonUnitalSemiring =
    { toAddCommMonoid := toAddCommMonoid✝, toMonoid := toMonoid✝, zero_mul := zero_mul✝, mul_zero := mul_zero✝,
        left_distrib := left_distrib✝, right_distrib := right_distrib✝, toNatCast := toNatCast✝,
        natCast_zero := natCast_zero✝, natCast_succ := natCast_succ✝ }.toNonUnitalSemiring
h₂ :
  { toAddCommMonoid := toAddCommMonoid✝¹, toMonoid := toMonoid✝¹, zero_mul := zero_mul✝¹, mul_zero := mul_zero✝¹,
        left_distrib := left_distrib✝¹, right_distrib := right_distrib✝¹, toNatCast := toNatCast✝¹,
        natCast_zero := natCast_zero✝¹, natCast_succ := natCast_succ✝¹ }.toNonAssocSemiring =
    { toAddCommMonoid := toAddCommMonoid✝, toMonoid := toMonoid✝, zero_mul := zero_mul✝, mul_zero := mul_zero✝,
        left_distrib := left_distrib✝, right_distrib := right_distrib✝, toNatCast := toNatCast✝,
        natCast_zero := natCast_zero✝, natCast_succ := natCast_succ✝ }.toNonAssocSemiring
h₃ :
  { toAddCommMonoid := toAddCommMonoid✝¹, toMonoid := toMonoid✝¹, zero_mul := zero_mul✝¹, mul_zero := mul_zero✝¹,
          left_distrib := left_distrib✝¹, right_distrib := right_distrib✝¹, toNatCast := toNatCast✝¹,
          natCast_zero := natCast_zero✝¹, natCast_succ := natCast_succ✝¹ }.toMonoidWithZero.toMonoid =
    { toAddCommMonoid := toAddCommMonoid✝, toMonoid := toMonoid✝, zero_mul := zero_mul✝, mul_zero := mul_zero✝,
          left_distrib := left_distrib✝, right_distrib := right_distrib✝, toNatCast := toNatCast✝,
          natCast_zero := natCast_zero✝, natCast_succ := natCast_succ✝ }.toMonoidWithZero.toMonoid
⊢ { toAddCommMonoid := toAddCommMonoid✝¹, toMonoid := toMonoid✝¹, zero_mul := zero_mul✝¹, mul_zero := mul_zero✝¹,
      left_distrib := left_distrib✝¹, right_distrib := right_distrib✝¹, toNatCast := toNatCast✝¹,
      natCast_zero := natCast_zero✝¹, natCast_succ := natCast_succ✝¹ } =
    { toAddCommMonoid := toAddCommMonoid✝, toMonoid := toMonoid✝, zero_mul := zero_mul✝, mul_zero := mul_zero✝,
      left_distrib := left_distrib✝, right_distrib := right_distrib✝, toNatCast := toNatCast✝,
      natCast_zero := natCast_zero✝, natCast_succ := natCast_succ✝ }

Tactic:
congr <;> solve | injection h₁ | injection h₂

Goal state after: