Module: Mathlib.Algebra.Ring.Ext

Goal state before:
pp: case mk.mk.e_toIntCast
R : Type u
toNonUnitalNonAssocRing✝¹ : NonUnitalNonAssocRing R
toOne✝¹ : One R
one_mul✝¹ : ∀ (a : R), 1 * a = a
mul_one✝¹ : ∀ (a : R), a * 1 = a
toNatCast✝¹ : NatCast R
natCast_zero✝¹ : ↑0 = 0
natCast_succ✝¹ : ∀ (n : ℕ), ↑(n + 1) = ↑n + 1
toIntCast✝¹ : IntCast R
intCast_ofNat✝¹ : ∀ (n : ℕ), IntCast.intCast ↑n = ↑n
intCast_negSucc✝¹ : ∀ (n : ℕ), IntCast.intCast (Int.negSucc n) = -↑(n + 1)
toNonUnitalNonAssocRing✝ : NonUnitalNonAssocRing R
toOne✝ : One R
one_mul✝ : ∀ (a : R), 1 * a = a
mul_one✝ : ∀ (a : R), a * 1 = a
toNatCast✝ : NatCast R
natCast_zero✝ : ↑0 = 0
natCast_succ✝ : ∀ (n : ℕ), ↑(n + 1) = ↑n + 1
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₁ :
  { toNonUnitalNonAssocRing := toNonUnitalNonAssocRing✝¹, toOne := toOne✝¹, one_mul := one_mul✝¹, mul_one := mul_one✝¹,
        toNatCast := toNatCast✝¹, natCast_zero := natCast_zero✝¹, natCast_succ := natCast_succ✝¹,
        toIntCast := toIntCast✝¹, intCast_ofNat := intCast_ofNat✝¹,
        intCast_negSucc := intCast_negSucc✝¹ }.toNonUnitalNonAssocRing =
    { toNonUnitalNonAssocRing := toNonUnitalNonAssocRing✝, toOne := toOne✝, one_mul := one_mul✝, mul_one := mul_one✝,
        toNatCast := toNatCast✝, natCast_zero := natCast_zero✝, natCast_succ := natCast_succ✝, toIntCast := toIntCast✝,
        intCast_ofNat := intCast_ofNat✝, intCast_negSucc := intCast_negSucc✝ }.toNonUnitalNonAssocRing
h₂ :
  { toNonUnitalNonAssocRing := toNonUnitalNonAssocRing✝¹, toOne := toOne✝¹, one_mul := one_mul✝¹, mul_one := mul_one✝¹,
        toNatCast := toNatCast✝¹, natCast_zero := natCast_zero✝¹, natCast_succ := natCast_succ✝¹,
        toIntCast := toIntCast✝¹, intCast_ofNat := intCast_ofNat✝¹,
        intCast_negSucc := intCast_negSucc✝¹ }.toNonAssocSemiring =
    { toNonUnitalNonAssocRing := toNonUnitalNonAssocRing✝, toOne := toOne✝, one_mul := one_mul✝, mul_one := mul_one✝,
        toNatCast := toNatCast✝, natCast_zero := natCast_zero✝, natCast_succ := natCast_succ✝, toIntCast := toIntCast✝,
        intCast_ofNat := intCast_ofNat✝, intCast_negSucc := intCast_negSucc✝ }.toNonAssocSemiring
h₃ :
  { toNonUnitalNonAssocRing := toNonUnitalNonAssocRing✝¹, toOne := toOne✝¹, one_mul := one_mul✝¹, mul_one := mul_one✝¹,
        toNatCast := toNatCast✝¹, natCast_zero := natCast_zero✝¹, natCast_succ := natCast_succ✝¹,
        toIntCast := toIntCast✝¹, intCast_ofNat := intCast_ofNat✝¹,
        intCast_negSucc := intCast_negSucc✝¹ }.toAddCommGroupWithOne =
    { toNonUnitalNonAssocRing := toNonUnitalNonAssocRing✝, toOne := toOne✝, one_mul := one_mul✝, mul_one := mul_one✝,
        toNatCast := toNatCast✝, natCast_zero := natCast_zero✝, natCast_succ := natCast_succ✝, toIntCast := toIntCast✝,
        intCast_ofNat := intCast_ofNat✝, intCast_negSucc := intCast_negSucc✝ }.toAddCommGroupWithOne
⊢ toIntCast✝¹ = toIntCast✝

Tactic:
injection h₂

Goal state after:
case mk.mk.e_toIntCast
R : Type u
toNonUnitalNonAssocRing✝¹ : NonUnitalNonAssocRing R
toOne✝¹ : One R
one_mul✝¹ : ∀ (a : R), 1 * a = a
mul_one✝¹ : ∀ (a : R), a * 1 = a
toNatCast✝¹ : NatCast R
natCast_zero✝¹ : ↑0 = 0
natCast_succ✝¹ : ∀ (n : ℕ), ↑(n + 1) = ↑n + 1
toIntCast✝¹ : IntCast R
intCast_ofNat✝¹ : ∀ (n : ℕ), IntCast.intCast ↑n = ↑n
intCast_negSucc✝¹ : ∀ (n : ℕ), IntCast.intCast (Int.negSucc n) = -↑(n + 1)
toNonUnitalNonAssocRing✝ : NonUnitalNonAssocRing R
toOne✝ : One R
one_mul✝ : ∀ (a : R), 1 * a = a
mul_one✝ : ∀ (a : R), a * 1 = a
toNatCast✝ : NatCast R
natCast_zero✝ : ↑0 = 0
natCast_succ✝ : ∀ (n : ℕ), ↑(n + 1) = ↑n + 1
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₁ :
  { toNonUnitalNonAssocRing := toNonUnitalNonAssocRing✝¹, toOne := toOne✝¹, one_mul := one_mul✝¹, mul_one := mul_one✝¹,
        toNatCast := toNatCast✝¹, natCast_zero := natCast_zero✝¹, natCast_succ := natCast_succ✝¹,
        toIntCast := toIntCast✝¹, intCast_ofNat := intCast_ofNat✝¹,
        intCast_negSucc := intCast_negSucc✝¹ }.toNonUnitalNonAssocRing =
    { toNonUnitalNonAssocRing := toNonUnitalNonAssocRing✝, toOne := toOne✝, one_mul := one_mul✝, mul_one := mul_one✝,
        toNatCast := toNatCast✝, natCast_zero := natCast_zero✝, natCast_succ := natCast_succ✝, toIntCast := toIntCast✝,
        intCast_ofNat := intCast_ofNat✝, intCast_negSucc := intCast_negSucc✝ }.toNonUnitalNonAssocRing
h₃ :
  { toNonUnitalNonAssocRing := toNonUnitalNonAssocRing✝¹, toOne := toOne✝¹, one_mul := one_mul✝¹, mul_one := mul_one✝¹,
        toNatCast := toNatCast✝¹, natCast_zero := natCast_zero✝¹, natCast_succ := natCast_succ✝¹,
        toIntCast := toIntCast✝¹, intCast_ofNat := intCast_ofNat✝¹,
        intCast_negSucc := intCast_negSucc✝¹ }.toAddCommGroupWithOne =
    { toNonUnitalNonAssocRing := toNonUnitalNonAssocRing✝, toOne := toOne✝, one_mul := one_mul✝, mul_one := mul_one✝,
        toNatCast := toNatCast✝, natCast_zero := natCast_zero✝, natCast_succ := natCast_succ✝, toIntCast := toIntCast✝,
        intCast_ofNat := intCast_ofNat✝, intCast_negSucc := intCast_negSucc✝ }.toAddCommGroupWithOne
toNonUnitalNonAssocSemiring_eq✝ :
  {
      toAddMonoid :=
        { toNonUnitalNonAssocRing := toNonUnitalNonAssocRing✝¹, toOne := toOne✝¹, one_mul := one_mul✝¹,
            mul_one := mul_one✝¹, toNatCast := toNatCast✝¹, natCast_zero := natCast_zero✝¹,
            natCast_succ := natCast_succ✝¹, toIntCast := toIntCast✝¹, intCast_ofNat := intCast_ofNat✝¹,
            intCast_negSucc := intCast_negSucc✝¹ }.toAddMonoid,
      add_comm := ⋯,
      toMul :=
        { toNonUnitalNonAssocRing := toNonUnitalNonAssocRing✝¹, toOne := toOne✝¹, one_mul := one_mul✝¹,
            mul_one := mul_one✝¹, toNatCast := toNatCast✝¹, natCast_zero := natCast_zero✝¹,
            natCast_succ := natCast_succ✝¹, toIntCast := toIntCast✝¹, intCast_ofNat := intCast_ofNat✝¹,
            intCast_negSucc := intCast_negSucc✝¹ }.toMul,
      left_distrib := ⋯, right_distrib := ⋯, zero_mul := ⋯, mul_zero := ⋯ } =
    {
      toAddMonoid :=
        { toNonUnitalNonAssocRing := toNonUnitalNonAssocRing✝, toOne := toOne✝, one_mul := one_mul✝,
            mul_one := mul_one✝, toNatCast := toNatCast✝, natCast_zero := natCast_zero✝, natCast_succ := natCast_succ✝,
            toIntCast := toIntCast✝, intCast_ofNat := intCast_ofNat✝, intCast_negSucc := intCast_negSucc✝ }.toAddMonoid,
      add_comm := ⋯,
      toMul :=
        { toNonUnitalNonAssocRing := toNonUnitalNonAssocRing✝, toOne := toOne✝, one_mul := one_mul✝,
            mul_one := mul_one✝, toNatCast := toNatCast✝, natCast_zero := natCast_zero✝, natCast_succ := natCast_succ✝,
            toIntCast := toIntCast✝, intCast_ofNat := intCast_ofNat✝, intCast_negSucc := intCast_negSucc✝ }.toMul,
      left_distrib := ⋯, right_distrib := ⋯, zero_mul := ⋯, mul_zero := ⋯ }
toOne_eq✝ :
  { toNonUnitalNonAssocRing := toNonUnitalNonAssocRing✝¹, toOne := toOne✝¹, one_mul := one_mul✝¹, mul_one := mul_one✝¹,
        toNatCast := toNatCast✝¹, natCast_zero := natCast_zero✝¹, natCast_succ := natCast_succ✝¹,
        toIntCast := toIntCast✝¹, intCast_ofNat := intCast_ofNat✝¹, intCast_negSucc := intCast_negSucc✝¹ }.toOne =
    { toNonUnitalNonAssocRing := toNonUnitalNonAssocRing✝, toOne := toOne✝, one_mul := one_mul✝, mul_one := mul_one✝,
        toNatCast := toNatCast✝, natCast_zero := natCast_zero✝, natCast_succ := natCast_succ✝, toIntCast := toIntCast✝,
        intCast_ofNat := intCast_ofNat✝, intCast_negSucc := intCast_negSucc✝ }.toOne
toNatCast_eq✝ :
  { toNonUnitalNonAssocRing := toNonUnitalNonAssocRing✝¹, toOne := toOne✝¹, one_mul := one_mul✝¹, mul_one := mul_one✝¹,
        toNatCast := toNatCast✝¹, natCast_zero := natCast_zero✝¹, natCast_succ := natCast_succ✝¹,
        toIntCast := toIntCast✝¹, intCast_ofNat := intCast_ofNat✝¹, intCast_negSucc := intCast_negSucc✝¹ }.toNatCast =
    { toNonUnitalNonAssocRing := toNonUnitalNonAssocRing✝, toOne := toOne✝, one_mul := one_mul✝, mul_one := mul_one✝,
        toNatCast := toNatCast✝, natCast_zero := natCast_zero✝, natCast_succ := natCast_succ✝, toIntCast := toIntCast✝,
        intCast_ofNat := intCast_ofNat✝, intCast_negSucc := intCast_negSucc✝ }.toNatCast
⊢ toIntCast✝¹ = toIntCast✝