Module: Mathlib.Algebra.Ring.Ext

Goal state before:
pp: case mk
R : Type u
inst₂ : Ring R
toSemiring✝ : Semiring R
toNeg✝ : Neg R
toSub✝ : Sub R
toZSMul✝ : ZSMul R
sub_eq_add_neg✝ : ∀ (a b : R), a - b = a + -b
zsmul_zero'✝ : ∀ (a : R), 0 • a = 0
zsmul_succ'✝ : ∀ (n : ℕ) (a : R), ↑n.succ • a = ↑n • a + a
zsmul_neg'✝ : ∀ (n : ℕ) (a : R), Int.negSucc n • a = -(↑n.succ • a)
neg_add_cancel✝ : ∀ (a : R), -a + a = 0
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₁ :
  { toSemiring := toSemiring✝, toNeg := toNeg✝, toSub := toSub✝, toZSMul := toZSMul✝, sub_eq_add_neg := sub_eq_add_neg✝,
        zsmul_zero' := zsmul_zero'✝, zsmul_succ' := zsmul_succ'✝, zsmul_neg' := zsmul_neg'✝,
        neg_add_cancel := neg_add_cancel✝, toIntCast := toIntCast✝, intCast_ofNat := intCast_ofNat✝,
        intCast_negSucc := intCast_negSucc✝ }.toSemiring =
    inst₂.toSemiring
h₂ : toNonAssocRing = toNonAssocRing
h₃ :
  { toSemiring := toSemiring✝, toNeg := toNeg✝, toSub := toSub✝, toZSMul := toZSMul✝, sub_eq_add_neg := sub_eq_add_neg✝,
          zsmul_zero' := zsmul_zero'✝, zsmul_succ' := zsmul_succ'✝, zsmul_neg' := zsmul_neg'✝,
          neg_add_cancel := neg_add_cancel✝, toIntCast := toIntCast✝, intCast_ofNat := intCast_ofNat✝,
          intCast_negSucc := intCast_negSucc✝ }.toAddCommGroup.toSubNegMonoid =
    inst₂.toAddCommGroup.toSubNegMonoid
⊢ { toSemiring := toSemiring✝, toNeg := toNeg✝, toSub := toSub✝, toZSMul := toZSMul✝, sub_eq_add_neg := sub_eq_add_neg✝,
      zsmul_zero' := zsmul_zero'✝, zsmul_succ' := zsmul_succ'✝, zsmul_neg' := zsmul_neg'✝,
      neg_add_cancel := neg_add_cancel✝, toIntCast := toIntCast✝, intCast_ofNat := intCast_ofNat✝,
      intCast_negSucc := intCast_negSucc✝ } =
    inst₂

Tactic:
;

Goal state after:
case mk
R : Type u
inst₂ : Ring R
toSemiring✝ : Semiring R
toNeg✝ : Neg R
toSub✝ : Sub R
toZSMul✝ : ZSMul R
sub_eq_add_neg✝ : ∀ (a b : R), a - b = a + -b
zsmul_zero'✝ : ∀ (a : R), 0 • a = 0
zsmul_succ'✝ : ∀ (n : ℕ) (a : R), ↑n.succ • a = ↑n • a + a
zsmul_neg'✝ : ∀ (n : ℕ) (a : R), Int.negSucc n • a = -(↑n.succ • a)
neg_add_cancel✝ : ∀ (a : R), -a + a = 0
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₁ :
  { toSemiring := toSemiring✝, toNeg := toNeg✝, toSub := toSub✝, toZSMul := toZSMul✝, sub_eq_add_neg := sub_eq_add_neg✝,
        zsmul_zero' := zsmul_zero'✝, zsmul_succ' := zsmul_succ'✝, zsmul_neg' := zsmul_neg'✝,
        neg_add_cancel := neg_add_cancel✝, toIntCast := toIntCast✝, intCast_ofNat := intCast_ofNat✝,
        intCast_negSucc := intCast_negSucc✝ }.toSemiring =
    inst₂.toSemiring
h₂ : toNonAssocRing = toNonAssocRing
h₃ :
  { toSemiring := toSemiring✝, toNeg := toNeg✝, toSub := toSub✝, toZSMul := toZSMul✝, sub_eq_add_neg := sub_eq_add_neg✝,
          zsmul_zero' := zsmul_zero'✝, zsmul_succ' := zsmul_succ'✝, zsmul_neg' := zsmul_neg'✝,
          neg_add_cancel := neg_add_cancel✝, toIntCast := toIntCast✝, intCast_ofNat := intCast_ofNat✝,
          intCast_negSucc := intCast_negSucc✝ }.toAddCommGroup.toSubNegMonoid =
    inst₂.toAddCommGroup.toSubNegMonoid
⊢ { toSemiring := toSemiring✝, toNeg := toNeg✝, toSub := toSub✝, toZSMul := toZSMul✝, sub_eq_add_neg := sub_eq_add_neg✝,
      zsmul_zero' := zsmul_zero'✝, zsmul_succ' := zsmul_succ'✝, zsmul_neg' := zsmul_neg'✝,
      neg_add_cancel := neg_add_cancel✝, toIntCast := toIntCast✝, intCast_ofNat := intCast_ofNat✝,
      intCast_negSucc := intCast_negSucc✝ } =
    inst₂