Module: Mathlib.Algebra.Ring.Ext

Goal state before:
pp: R : Type u
inst₂ : AddGroupWithOne R
toAddMonoidWithOne✝ : AddMonoidWithOne 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
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_one : One.one = One.one
this✝¹ :
  { intCast := intCast✝, toAddMonoidWithOne := toAddMonoidWithOne✝, 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✝,
        intCast_ofNat := intCast_ofNat✝, intCast_negSucc := intCast_negSucc✝ }.toAddMonoidWithOne =
    inst₂.toAddMonoidWithOne
this✝ :
  { intCast := intCast✝, toAddMonoidWithOne := toAddMonoidWithOne✝, 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✝,
        intCast_ofNat := intCast_ofNat✝, intCast_negSucc := intCast_negSucc✝ }.toNatCast =
    inst₂.toNatCast
toAddMonoid_eq✝ :
  { intCast := intCast✝, toAddMonoidWithOne := toAddMonoidWithOne✝, 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✝,
        intCast_ofNat := intCast_ofNat✝, intCast_negSucc := intCast_negSucc✝ }.toAddMonoid =
    inst₂.toAddMonoid
toNeg_eq✝ :
  { intCast := intCast✝, toAddMonoidWithOne := toAddMonoidWithOne✝, 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✝,
        intCast_ofNat := intCast_ofNat✝, intCast_negSucc := intCast_negSucc✝ }.toNeg =
    inst₂.toNeg
toSub_eq✝ :
  { intCast := intCast✝, toAddMonoidWithOne := toAddMonoidWithOne✝, 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✝,
        intCast_ofNat := intCast_ofNat✝, intCast_negSucc := intCast_negSucc✝ }.toSub =
    inst₂.toSub
toZSMul_eq✝ :
  { intCast := intCast✝, toAddMonoidWithOne := toAddMonoidWithOne✝, 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✝,
        intCast_ofNat := intCast_ofNat✝, intCast_negSucc := intCast_negSucc✝ }.toZSMul =
    inst₂.toZSMul
this : IntCast.intCast = IntCast.intCast
⊢ { intCast := intCast✝, toAddMonoidWithOne := toAddMonoidWithOne✝, 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✝, intCast_ofNat := intCast_ofNat✝,
      intCast_negSucc := intCast_negSucc✝ } =
    inst₂

Tactic:
;

Goal state after:
R : Type u
inst₂ : AddGroupWithOne R
toAddMonoidWithOne✝ : AddMonoidWithOne 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
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_one : One.one = One.one
this✝¹ :
  { intCast := intCast✝, toAddMonoidWithOne := toAddMonoidWithOne✝, 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✝,
        intCast_ofNat := intCast_ofNat✝, intCast_negSucc := intCast_negSucc✝ }.toAddMonoidWithOne =
    inst₂.toAddMonoidWithOne
this✝ :
  { intCast := intCast✝, toAddMonoidWithOne := toAddMonoidWithOne✝, 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✝,
        intCast_ofNat := intCast_ofNat✝, intCast_negSucc := intCast_negSucc✝ }.toNatCast =
    inst₂.toNatCast
toAddMonoid_eq✝ :
  { intCast := intCast✝, toAddMonoidWithOne := toAddMonoidWithOne✝, 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✝,
        intCast_ofNat := intCast_ofNat✝, intCast_negSucc := intCast_negSucc✝ }.toAddMonoid =
    inst₂.toAddMonoid
toNeg_eq✝ :
  { intCast := intCast✝, toAddMonoidWithOne := toAddMonoidWithOne✝, 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✝,
        intCast_ofNat := intCast_ofNat✝, intCast_negSucc := intCast_negSucc✝ }.toNeg =
    inst₂.toNeg
toSub_eq✝ :
  { intCast := intCast✝, toAddMonoidWithOne := toAddMonoidWithOne✝, 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✝,
        intCast_ofNat := intCast_ofNat✝, intCast_negSucc := intCast_negSucc✝ }.toSub =
    inst₂.toSub
toZSMul_eq✝ :
  { intCast := intCast✝, toAddMonoidWithOne := toAddMonoidWithOne✝, 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✝,
        intCast_ofNat := intCast_ofNat✝, intCast_negSucc := intCast_negSucc✝ }.toZSMul =
    inst₂.toZSMul
this : IntCast.intCast = IntCast.intCast
⊢ { intCast := intCast✝, toAddMonoidWithOne := toAddMonoidWithOne✝, 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✝, intCast_ofNat := intCast_ofNat✝,
      intCast_negSucc := intCast_negSucc✝ } =
    inst₂