Module: Mathlib.Algebra.Ring.Ext

Goal state before:
pp: case mk
R : Type u
inst₂ : Semiring R
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 =
    inst₂.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 =
    inst₂.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 =
    inst₂.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 =
    inst₂.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✝ } =
    inst₂

Tactic:
;

Goal state after:
case mk
R : Type u
inst₂ : Semiring R
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 =
    inst₂.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 =
    inst₂.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 =
    inst₂.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 =
    inst₂.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✝ } =
    inst₂