Module: Mathlib.Algebra.Ring.Ext

Goal state before:
pp: case mk
R : Type u
inst₂ : NonAssocRing R
toNonUnitalNonAssocRing✝ : NonUnitalNonAssocRing 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
toIntCast✝ : IntCast R
intCast_ofNat✝ : ∀ (n : ℕ), IntCast.intCast ↑n = ↑n
intCast_negSucc✝ : ∀ (n : ℕ), IntCast.intCast (Int.negSucc n) = -↑(n + 1)
h_add : HAdd.hAdd = HAdd.hAdd
h_mul : HMul.hMul = HMul.hMul
h₁ :
  { toNonUnitalNonAssocRing := toNonUnitalNonAssocRing✝, toOne := toOne✝, one_mul := one_mul✝, mul_one := mul_one✝,
        toNatCast := toNatCast✝, natCast_zero := natCast_zero✝, natCast_succ := natCast_succ✝, toIntCast := toIntCast✝,
        intCast_ofNat := intCast_ofNat✝, intCast_negSucc := intCast_negSucc✝ }.toNonUnitalNonAssocRing =
    inst₂.toNonUnitalNonAssocRing
h₂ :
  { toNonUnitalNonAssocRing := toNonUnitalNonAssocRing✝, toOne := toOne✝, one_mul := one_mul✝, mul_one := mul_one✝,
        toNatCast := toNatCast✝, natCast_zero := natCast_zero✝, natCast_succ := natCast_succ✝, toIntCast := toIntCast✝,
        intCast_ofNat := intCast_ofNat✝, intCast_negSucc := intCast_negSucc✝ }.toNonAssocSemiring =
    inst₂.toNonAssocSemiring
h₃ :
  { toNonUnitalNonAssocRing := toNonUnitalNonAssocRing✝, toOne := toOne✝, one_mul := one_mul✝, mul_one := mul_one✝,
        toNatCast := toNatCast✝, natCast_zero := natCast_zero✝, natCast_succ := natCast_succ✝, toIntCast := toIntCast✝,
        intCast_ofNat := intCast_ofNat✝, intCast_negSucc := intCast_negSucc✝ }.toAddCommGroupWithOne =
    inst₂.toAddCommGroupWithOne
⊢ { toNonUnitalNonAssocRing := toNonUnitalNonAssocRing✝, toOne := toOne✝, one_mul := one_mul✝, mul_one := mul_one✝,
      toNatCast := toNatCast✝, natCast_zero := natCast_zero✝, natCast_succ := natCast_succ✝, toIntCast := toIntCast✝,
      intCast_ofNat := intCast_ofNat✝, intCast_negSucc := intCast_negSucc✝ } =
    inst₂

Tactic:
;

Goal state after:
case mk
R : Type u
inst₂ : NonAssocRing R
toNonUnitalNonAssocRing✝ : NonUnitalNonAssocRing 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
toIntCast✝ : IntCast R
intCast_ofNat✝ : ∀ (n : ℕ), IntCast.intCast ↑n = ↑n
intCast_negSucc✝ : ∀ (n : ℕ), IntCast.intCast (Int.negSucc n) = -↑(n + 1)
h_add : HAdd.hAdd = HAdd.hAdd
h_mul : HMul.hMul = HMul.hMul
h₁ :
  { toNonUnitalNonAssocRing := toNonUnitalNonAssocRing✝, toOne := toOne✝, one_mul := one_mul✝, mul_one := mul_one✝,
        toNatCast := toNatCast✝, natCast_zero := natCast_zero✝, natCast_succ := natCast_succ✝, toIntCast := toIntCast✝,
        intCast_ofNat := intCast_ofNat✝, intCast_negSucc := intCast_negSucc✝ }.toNonUnitalNonAssocRing =
    inst₂.toNonUnitalNonAssocRing
h₂ :
  { toNonUnitalNonAssocRing := toNonUnitalNonAssocRing✝, toOne := toOne✝, one_mul := one_mul✝, mul_one := mul_one✝,
        toNatCast := toNatCast✝, natCast_zero := natCast_zero✝, natCast_succ := natCast_succ✝, toIntCast := toIntCast✝,
        intCast_ofNat := intCast_ofNat✝, intCast_negSucc := intCast_negSucc✝ }.toNonAssocSemiring =
    inst₂.toNonAssocSemiring
h₃ :
  { toNonUnitalNonAssocRing := toNonUnitalNonAssocRing✝, toOne := toOne✝, one_mul := one_mul✝, mul_one := mul_one✝,
        toNatCast := toNatCast✝, natCast_zero := natCast_zero✝, natCast_succ := natCast_succ✝, toIntCast := toIntCast✝,
        intCast_ofNat := intCast_ofNat✝, intCast_negSucc := intCast_negSucc✝ }.toAddCommGroupWithOne =
    inst₂.toAddCommGroupWithOne
⊢ { toNonUnitalNonAssocRing := toNonUnitalNonAssocRing✝, toOne := toOne✝, one_mul := one_mul✝, mul_one := mul_one✝,
      toNatCast := toNatCast✝, natCast_zero := natCast_zero✝, natCast_succ := natCast_succ✝, toIntCast := toIntCast✝,
      intCast_ofNat := intCast_ofNat✝, intCast_negSucc := intCast_negSucc✝ } =
    inst₂