Module: Mathlib.Algebra.Ring.Ext

Goal state before:
pp: case e_toSub
R : Type u
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)
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 =
    { 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
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 =
    { 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
⊢ toSub✝¹ = toSub✝

Tactic:
injection h₂

Goal state after:
case e_toSub
R : Type u
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)
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 =
    { 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
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 =
    { 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
toNonUnitalNonAssocRing_eq✝ :
  {
      toAddMonoid :=
        { 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✝¹ }.toAddMonoid,
      toNeg :=
        { 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✝¹ }.toNeg,
      toSub :=
        { 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✝¹ }.toSub,
      toZSMul :=
        { 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✝¹ }.toZSMul,
      sub_eq_add_neg := ⋯, zsmul_zero' := ⋯, zsmul_succ' := ⋯, zsmul_neg' := ⋯, neg_add_cancel := ⋯, add_comm := ⋯,
      toMul :=
        { 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✝¹ }.toMul,
      left_distrib := ⋯, right_distrib := ⋯, zero_mul := ⋯, mul_zero := ⋯ } =
    {
      toAddMonoid :=
        { 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✝ }.toAddMonoid,
      toNeg :=
        { 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✝ }.toNeg,
      toSub :=
        { 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✝ }.toSub,
      toZSMul :=
        { 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✝ }.toZSMul,
      sub_eq_add_neg := ⋯, zsmul_zero' := ⋯, zsmul_succ' := ⋯, zsmul_neg' := ⋯, neg_add_cancel := ⋯, add_comm := ⋯,
      toMul :=
        { 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✝ }.toMul,
      left_distrib := ⋯, right_distrib := ⋯, zero_mul := ⋯, mul_zero := ⋯ }
toOne_eq✝ :
  { 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✝¹ }.toOne =
    { 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✝ }.toOne
toNatCast_eq✝ :
  { 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✝¹ }.toNatCast =
    { 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✝ }.toNatCast
toIntCast_eq✝ :
  { 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✝¹ }.toIntCast =
    { 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✝ }.toIntCast
⊢ toSub✝¹ = toSub✝