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:
rcases inst₂ with @⟨⟨⟩⟩

Goal state after:
R : Type u
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)
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 =
    { 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
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 =
    { 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
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 =
    { 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
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 =
    { 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
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 =
    { 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
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 =
    { 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
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✝¹ } =
    { 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✝ }