Module: Mathlib.Algebra.Ring.Ext

Goal state before:
pp: case mk.mk
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
⊢ { 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✝, 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✝ }

Tactic:
congr

Goal state after:
case e_toNeg
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
⊢ toNeg✝¹ = toNeg✝

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✝

case mk.mk.e_toZSMul
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
⊢ toZSMul✝¹ = toZSMul✝

case e_toIntCast
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
⊢ toIntCast✝¹ = toIntCast✝