-- Lean 4 proof step from Mathlib.Algebra.Ring.Ext (goal)
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
⊢ { 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₂
have 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 }
Tactic: cases inst₂
Cleared hypotheses: inst₂, h_add, h_one, this, toIntCast_eq, toNeg_eq, toSub_eq, zsmul_eq, toNatCast_eq, toAddMonoid_eq, toOne_eq