Module: Mathlib.Algebra.Ring.Ext

Goal state before:
pp: case mk.mk
R : Type u
toAddCommGroup✝¹ : AddCommGroup R
toIntCast✝¹ : IntCast R
toNatCast✝¹ : NatCast R
toOne✝¹ : One R
natCast_zero✝¹ : ↑0 = 0
natCast_succ✝¹ : ∀ (n : ℕ), ↑(n + 1) = ↑n + 1
intCast_ofNat✝¹ : ∀ (n : ℕ), IntCast.intCast ↑n = ↑n
intCast_negSucc✝¹ : ∀ (n : ℕ), IntCast.intCast (Int.negSucc n) = -↑(n + 1)
toAddCommGroup✝ : AddCommGroup R
toIntCast✝ : IntCast R
toNatCast✝ : NatCast R
toOne✝ : One R
natCast_zero✝ : ↑0 = 0
natCast_succ✝ : ∀ (n : ℕ), ↑(n + 1) = ↑n + 1
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 :
  { toAddCommGroup := toAddCommGroup✝¹, toIntCast := toIntCast✝¹, toNatCast := toNatCast✝¹, toOne := toOne✝¹,
        natCast_zero := natCast_zero✝¹, natCast_succ := natCast_succ✝¹, intCast_ofNat := intCast_ofNat✝¹,
        intCast_negSucc := intCast_negSucc✝¹ }.toAddCommGroup =
    { toAddCommGroup := toAddCommGroup✝, toIntCast := toIntCast✝, toNatCast := toNatCast✝, toOne := toOne✝,
        natCast_zero := natCast_zero✝, natCast_succ := natCast_succ✝, intCast_ofNat := intCast_ofNat✝,
        intCast_negSucc := intCast_negSucc✝ }.toAddCommGroup
toIntCast_eq✝ :
  { toAddCommGroup := toAddCommGroup✝¹, toIntCast := toIntCast✝¹, toNatCast := toNatCast✝¹, toOne := toOne✝¹,
        natCast_zero := natCast_zero✝¹, natCast_succ := natCast_succ✝¹, intCast_ofNat := intCast_ofNat✝¹,
        intCast_negSucc := intCast_negSucc✝¹ }.toIntCast =
    { toAddCommGroup := toAddCommGroup✝, toIntCast := toIntCast✝, toNatCast := toNatCast✝, toOne := toOne✝,
        natCast_zero := natCast_zero✝, natCast_succ := natCast_succ✝, intCast_ofNat := intCast_ofNat✝,
        intCast_negSucc := intCast_negSucc✝ }.toIntCast
toNeg_eq✝ :
  { toAddCommGroup := toAddCommGroup✝¹, toIntCast := toIntCast✝¹, toNatCast := toNatCast✝¹, toOne := toOne✝¹,
        natCast_zero := natCast_zero✝¹, natCast_succ := natCast_succ✝¹, intCast_ofNat := intCast_ofNat✝¹,
        intCast_negSucc := intCast_negSucc✝¹ }.toNeg =
    { toAddCommGroup := toAddCommGroup✝, toIntCast := toIntCast✝, toNatCast := toNatCast✝, toOne := toOne✝,
        natCast_zero := natCast_zero✝, natCast_succ := natCast_succ✝, intCast_ofNat := intCast_ofNat✝,
        intCast_negSucc := intCast_negSucc✝ }.toNeg
toSub_eq✝ :
  { toAddCommGroup := toAddCommGroup✝¹, toIntCast := toIntCast✝¹, toNatCast := toNatCast✝¹, toOne := toOne✝¹,
        natCast_zero := natCast_zero✝¹, natCast_succ := natCast_succ✝¹, intCast_ofNat := intCast_ofNat✝¹,
        intCast_negSucc := intCast_negSucc✝¹ }.toSub =
    { toAddCommGroup := toAddCommGroup✝, toIntCast := toIntCast✝, toNatCast := toNatCast✝, toOne := toOne✝,
        natCast_zero := natCast_zero✝, natCast_succ := natCast_succ✝, intCast_ofNat := intCast_ofNat✝,
        intCast_negSucc := intCast_negSucc✝ }.toSub
toZSMul_eq✝ :
  { toAddCommGroup := toAddCommGroup✝¹, toIntCast := toIntCast✝¹, toNatCast := toNatCast✝¹, toOne := toOne✝¹,
        natCast_zero := natCast_zero✝¹, natCast_succ := natCast_succ✝¹, intCast_ofNat := intCast_ofNat✝¹,
        intCast_negSucc := intCast_negSucc✝¹ }.toZSMul =
    { toAddCommGroup := toAddCommGroup✝, toIntCast := toIntCast✝, toNatCast := toNatCast✝, toOne := toOne✝,
        natCast_zero := natCast_zero✝, natCast_succ := natCast_succ✝, intCast_ofNat := intCast_ofNat✝,
        intCast_negSucc := intCast_negSucc✝ }.toZSMul
toNatCast_eq✝ :
  { toAddCommGroup := toAddCommGroup✝¹, toIntCast := toIntCast✝¹, toNatCast := toNatCast✝¹, toOne := toOne✝¹,
        natCast_zero := natCast_zero✝¹, natCast_succ := natCast_succ✝¹, intCast_ofNat := intCast_ofNat✝¹,
        intCast_negSucc := intCast_negSucc✝¹ }.toNatCast =
    { toAddCommGroup := toAddCommGroup✝, toIntCast := toIntCast✝, toNatCast := toNatCast✝, toOne := toOne✝,
        natCast_zero := natCast_zero✝, natCast_succ := natCast_succ✝, intCast_ofNat := intCast_ofNat✝,
        intCast_negSucc := intCast_negSucc✝ }.toNatCast
toAddMonoid_eq✝ :
  { toAddCommGroup := toAddCommGroup✝¹, toIntCast := toIntCast✝¹, toNatCast := toNatCast✝¹, toOne := toOne✝¹,
        natCast_zero := natCast_zero✝¹, natCast_succ := natCast_succ✝¹, intCast_ofNat := intCast_ofNat✝¹,
        intCast_negSucc := intCast_negSucc✝¹ }.toAddMonoid =
    { toAddCommGroup := toAddCommGroup✝, toIntCast := toIntCast✝, toNatCast := toNatCast✝, toOne := toOne✝,
        natCast_zero := natCast_zero✝, natCast_succ := natCast_succ✝, intCast_ofNat := intCast_ofNat✝,
        intCast_negSucc := intCast_negSucc✝ }.toAddMonoid
toOne_eq✝ :
  { toAddCommGroup := toAddCommGroup✝¹, toIntCast := toIntCast✝¹, toNatCast := toNatCast✝¹, toOne := toOne✝¹,
        natCast_zero := natCast_zero✝¹, natCast_succ := natCast_succ✝¹, intCast_ofNat := intCast_ofNat✝¹,
        intCast_negSucc := intCast_negSucc✝¹ }.toOne =
    { toAddCommGroup := toAddCommGroup✝, toIntCast := toIntCast✝, toNatCast := toNatCast✝, toOne := toOne✝,
        natCast_zero := natCast_zero✝, natCast_succ := natCast_succ✝, intCast_ofNat := intCast_ofNat✝,
        intCast_negSucc := intCast_negSucc✝ }.toOne
⊢ { toAddCommGroup := toAddCommGroup✝¹, toIntCast := toIntCast✝¹, toNatCast := toNatCast✝¹, toOne := toOne✝¹,
      natCast_zero := natCast_zero✝¹, natCast_succ := natCast_succ✝¹, intCast_ofNat := intCast_ofNat✝¹,
      intCast_negSucc := intCast_negSucc✝¹ } =
    { toAddCommGroup := toAddCommGroup✝, toIntCast := toIntCast✝, toNatCast := toNatCast✝, toOne := toOne✝,
      natCast_zero := natCast_zero✝, natCast_succ := natCast_succ✝, intCast_ofNat := intCast_ofNat✝,
      intCast_negSucc := intCast_negSucc✝ }

Tactic:
congr

Goal state after: