-- Module: Mathlib.Algebra.Ring.Ext
Goal:
R : Type u
inst₂ : AddCommGroupWithOne R
toAddCommGroup : AddCommGroup R
toIntCast : IntCast R
toNatCast : NatCast R
toOne : One R
natCast_zero : Eq.{u + 1} (α := R) (↑0) 0
natCast_succ : ∀ (n : ℕ), ↑(n + 1) = HAdd.hAdd (α := R) (↑n) 1
intCast_ofNat : ∀ (n : ℕ), Eq.{u + 1} (α := R) (IntCast.intCast (↑n : ℤ)) (↑n : R)
intCast_negSucc : ∀ (n : ℕ), Eq.{u + 1} (α := R) (IntCast.intCast (Int.negSucc n)) (-(↑(n + 1) : R))
h_add : Eq (α := R → R → R) HAdd.hAdd HAdd.hAdd
h_one : Eq.{u + 1} (α := R) One.one One.one
this : Eq.{u + 1} (α := AddCommGroup R) AddCommGroupWithOne.toAddCommGroup AddCommGroupWithOne.toAddCommGroup
toIntCast_eq : Eq.{u + 1} (α := IntCast R) AddCommGroupWithOne.toIntCast AddCommGroupWithOne.toIntCast
toNeg_eq : Eq.{u + 1} (α := Neg R) SubNegMonoid.toNeg SubNegMonoid.toNeg
toSub_eq : Eq.{u + 1} (α := Sub R) SubNegMonoid.toSub SubNegMonoid.toSub
zsmul_eq : Eq.{u + 1} (α := ℤ → R → R) SubNegMonoid.zsmul SubNegMonoid.zsmul
toNatCast_eq : Eq.{u + 1} (α := NatCast R) AddCommGroupWithOne.toNatCast AddCommGroupWithOne.toNatCast
toAddMonoid_eq : Eq.{u + 1} (α := AddMonoid R) SubNegMonoid.toAddMonoid SubNegMonoid.toAddMonoid
toOne_eq : Eq.{u + 1} (α := One R) AddCommGroupWithOne.toOne AddCommGroupWithOne.toOne
mk :
  ∀ [toAddCommGroup_1 : AddCommGroup R] [toIntCast_1 : IntCast R] [toNatCast_1 : NatCast R] [toOne_1 : One R]
    (natCast_zero_1 : Eq.{u + 1} (α := R) (↑0) 0) (natCast_succ_1 : ∀ (n : ℕ), ↑(n + 1) = HAdd.hAdd (α := R) (↑n) 1)
    (intCast_ofNat_1 : ∀ (n : ℕ), Eq.{u + 1} (α := R) (IntCast.intCast (↑n : ℤ)) (↑n : R))
    (intCast_negSucc_1 : ∀ (n : ℕ), Eq.{u + 1} (α := R) (IntCast.intCast (Int.negSucc n)) (-(↑(n + 1) : R)))
    (h_add : Eq (α := R → R → R) HAdd.hAdd HAdd.hAdd) (h_one : Eq.{u + 1} (α := R) One.one One.one)
    (this : Eq.{u + 1} (α := AddCommGroup R) AddCommGroupWithOne.toAddCommGroup AddCommGroupWithOne.toAddCommGroup),
    Eq.{u + 1} (α := IntCast R) AddCommGroupWithOne.toIntCast AddCommGroupWithOne.toIntCast →
      Eq.{u + 1} (α := Neg R) SubNegMonoid.toNeg SubNegMonoid.toNeg →
        Eq.{u + 1} (α := Sub R) SubNegMonoid.toSub SubNegMonoid.toSub →
          Eq.{u + 1} (α := ℤ → R → R) SubNegMonoid.zsmul SubNegMonoid.zsmul →
            Eq.{u + 1} (α := NatCast R) AddCommGroupWithOne.toNatCast AddCommGroupWithOne.toNatCast →
              Eq.{u + 1} (α := AddMonoid R) SubNegMonoid.toAddMonoid SubNegMonoid.toAddMonoid →
                Eq.{u + 1} (α := One R) AddCommGroupWithOne.toOne AddCommGroupWithOne.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 : AddCommGroupWithOne R } =
                    { toAddCommGroup := toAddCommGroup_1, toIntCast := toIntCast_1, toNatCast := toNatCast_1,
                      toOne := toOne_1, natCast_zero := natCast_zero_1, natCast_succ := natCast_succ_1,
                      intCast_ofNat := intCast_ofNat_1, intCast_negSucc := intCast_negSucc_1 }
⊢ { toAddCommGroup := toAddCommGroup, toIntCast := toIntCast, toNatCast := toNatCast, toOne := toOne,
      natCast_zero := natCast_zero, natCast_succ := natCast_succ, intCast_ofNat := intCast_ofNat,
      intCast_negSucc := intCast_negSucc : AddCommGroupWithOne R } =
    inst₂

Tactic:
cases inst₂