Module: Mathlib.Algebra.Ring.Ext

Goal state before:
pp: case mk
R : Type u
inst₂ : AddCommGroupWithOne R
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 =
    inst₂.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 =
    inst₂.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 =
    inst₂.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 =
    inst₂.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 =
    inst₂.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 =
    inst₂.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 =
    inst₂.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 =
    inst₂.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✝ } =
    inst₂

Tactic:
;

Goal state after:
case mk
R : Type u
inst₂ : AddCommGroupWithOne R
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 =
    inst₂.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 =
    inst₂.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 =
    inst₂.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 =
    inst₂.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 =
    inst₂.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 =
    inst₂.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 =
    inst₂.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 =
    inst₂.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✝ } =
    inst₂