awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Ring.Ext
Goal:
R : Type u
inst₁ inst₂ : AddGroupWithOne R
h_add : Eq (α := R → R → R) HAdd.hAdd HAdd.hAdd
h_one : Eq.{u + 1} (α := R) One.one One.one
this_1 : Eq.{u + 1} (α := AddMonoidWithOne R) toAddMonoidWithOne toAddMonoidWithOne
this : Eq.{u + 1} (α := NatCast R) AddMonoidWithOne.toNatCast AddMonoidWithOne.toNatCast
toAddMonoid_eq : Eq.{u + 1} (α := AddMonoid R) AddMonoidWithOne.toAddMonoid AddMonoidWithOne.toAddMonoid
toNeg_eq : Eq.{u + 1} (α := Neg R) toNeg toNeg
toSub_eq : Eq.{u + 1} (α := Sub R) toSub toSub
zsmul_eq : Eq.{u + 1} (α := ℤ → R → R) AddGroupWithOne.zsmul AddGroupWithOne.zsmul
n : ℕ
⊢ Eq.{u + 1} (α := R) (-(↑(n + 1) : R)) (-(↑(n + 1) : R))

Tactic:
congr
-- Module: Mathlib.Algebra.Ring.Ext
Goal:
R : Type u
inst₁ inst₂ : AddGroupWithOne R
h_add : Eq (α := R → R → R) HAdd.hAdd HAdd.hAdd
h_one : Eq.{u + 1} (α := R) One.one One.one
this_1 : Eq.{u + 1} (α := AddMonoidWithOne R) toAddMonoidWithOne toAddMonoidWithOne
this : Eq.{u + 1} (α := NatCast R) AddMonoidWithOne.toNatCast AddMonoidWithOne.toNatCast
toAddMonoid_eq : Eq.{u + 1} (α := AddMonoid R) AddMonoidWithOne.toAddMonoid AddMonoidWithOne.toAddMonoid
toNeg_eq : Eq.{u + 1} (α := Neg R) toNeg toNeg
toSub_eq : Eq.{u + 1} (α := Sub R) toSub toSub
zsmul_eq : Eq.{u + 1} (α := ℤ → R → R) AddGroupWithOne.zsmul AddGroupWithOne.zsmul
n : ℤ
h : ∀ (n : ℕ), Eq.{u + 1} (α := R) (IntCast.intCast (Int.ofNat n)) (IntCast.intCast (Int.ofNat n))
h₁ : ∀ (n : ℕ), Eq.{u + 1} (α := R) (IntCast.intCast (Int.negSucc n)) (IntCast.intCast (Int.negSucc n))
⊢ Eq.{u + 1} (α := R) (IntCast.intCast n) (IntCast.intCast n)

Tactic:
cases n with
    | ofNat n => rewrite [Int.ofNat_eq_natCast, inst₁.intCast_ofNat, inst₂.intCast_ofNat]; congr
    | negSucc n => rewrite [inst₁.intCast_negSucc, inst₂.intCast_negSucc]; congr

Premises used: Int.ofNat_eq_natCast, AddGroupWithOne.intCast_negSucc, AddGroupWithOne.intCast_ofNat
-- Module: Mathlib.Algebra.Ring.Ext
Goal:
R : Type u
inst₁ inst₂ : AddGroupWithOne R
h_add : Eq (α := R → R → R) HAdd.hAdd HAdd.hAdd
h_one : Eq.{u + 1} (α := R) One.one One.one
this_1 : Eq.{u + 1} (α := AddMonoidWithOne R) toAddMonoidWithOne toAddMonoidWithOne
this : Eq.{u + 1} (α := NatCast R) AddMonoidWithOne.toNatCast AddMonoidWithOne.toNatCast
toAddMonoid_eq : Eq.{u + 1} (α := AddMonoid R) AddMonoidWithOne.toAddMonoid AddMonoidWithOne.toAddMonoid
toNeg_eq : Eq.{u + 1} (α := Neg R) toNeg toNeg
toSub_eq : Eq.{u + 1} (α := Sub R) toSub toSub
zsmul_eq : Eq.{u + 1} (α := ℤ → R → R) AddGroupWithOne.zsmul AddGroupWithOne.zsmul
⊢ Eq.{u + 1} (α := ℤ → R) IntCast.intCast IntCast.intCast

Tactic:
have : inst₁.toIntCast.intCast = inst₂.toIntCast.intCast := by
    funext n; cases n with
    | ofNat n => rewrite [Int.ofNat_eq_natCast, inst₁.intCast_ofNat, inst₂.intCast_ofNat]; congr
    | negSucc n => rewrite [inst₁.intCast_negSucc, inst₂.intCast_negSucc]; congr
-- Module: Mathlib.Algebra.Ring.Ext
Goal:
R : Type u
inst₁ inst₂ : AddGroupWithOne R
h_add : Eq (α := R → R → R) HAdd.hAdd HAdd.hAdd
h_one : Eq.{u + 1} (α := R) One.one One.one
this_1 : Eq.{u + 1} (α := AddMonoidWithOne R) toAddMonoidWithOne toAddMonoidWithOne
this_2 : Eq.{u + 1} (α := NatCast R) AddMonoidWithOne.toNatCast AddMonoidWithOne.toNatCast
toAddMonoid_eq : Eq.{u + 1} (α := AddMonoid R) AddMonoidWithOne.toAddMonoid AddMonoidWithOne.toAddMonoid
toNeg_eq : Eq.{u + 1} (α := Neg R) toNeg toNeg
toSub_eq : Eq.{u + 1} (α := Sub R) toSub toSub
zsmul_eq : Eq.{u + 1} (α := ℤ → R → R) AddGroupWithOne.zsmul AddGroupWithOne.zsmul
this : Eq.{u + 1} (α := ℤ → R) IntCast.intCast IntCast.intCast
rcases :
  ∀ [toAddMonoidWithOne : AddMonoidWithOne R] [toNeg : Neg R] [toSub : Sub R]
    (sub_eq_add_neg : ∀ (a b : R), a - b = a + -b) (zsmul : ℤ → R → R) (zsmul_zero' : ∀ (a : R), zsmul 0 a = 0)
    (zsmul_succ' : ∀ (n : ℕ) (a : R), zsmul (↑n.succ : ℤ) a = zsmul (↑n : ℤ) a + a)
    (zsmul_neg' : ∀ (n : ℕ) (a : R), zsmul (Int.negSucc n) a = -zsmul (↑n.succ : ℤ) a)
    (neg_add_cancel : ∀ (a : R), -a + a = 0) (intCast : ℤ → R)
    (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} (α := AddMonoidWithOne R) AddGroupWithOne.toAddMonoidWithOne AddGroupWithOne.toAddMonoidWithOne)
    (this : Eq.{u + 1} (α := NatCast R) AddMonoidWithOne.toNatCast AddMonoidWithOne.toNatCast),
    Eq.{u + 1} (α := AddMonoid R) AddMonoidWithOne.toAddMonoid AddMonoidWithOne.toAddMonoid →
      Eq.{u + 1} (α := Neg R) AddGroupWithOne.toNeg AddGroupWithOne.toNeg →
        Eq.{u + 1} (α := Sub R) AddGroupWithOne.toSub AddGroupWithOne.toSub →
          Eq.{u + 1} (α := ℤ → R → R) AddGroupWithOne.zsmul AddGroupWithOne.zsmul →
            ∀ (this : Eq.{u + 1} (α := ℤ → R) IntCast.intCast IntCast.intCast),
              { intCast := intCast, toAddMonoidWithOne := toAddMonoidWithOne, toNeg := toNeg, toSub := toSub,
                  sub_eq_add_neg := sub_eq_add_neg, zsmul := zsmul, zsmul_zero' := zsmul_zero',
                  zsmul_succ' := zsmul_succ', zsmul_neg' := zsmul_neg', neg_add_cancel := neg_add_cancel,
                  intCast_ofNat := intCast_ofNat, intCast_negSucc := intCast_negSucc : AddGroupWithOne R } =
                inst₂
⊢ inst₁ = inst₂

Tactic:
rcases inst₁ with @⟨⟨⟩⟩
-- Module: Mathlib.Algebra.Ring.Ext
Goal:
R : Type u
toAddMonoidWithOne : AddMonoidWithOne R
toNeg : Neg R
toSub : Sub R
sub_eq_add_neg : ∀ (a b : R), a - b = a + -b
zsmul : ℤ → R → R
zsmul_zero' : ∀ (a : R), zsmul 0 a = 0
zsmul_succ' : ∀ (n : ℕ) (a : R), zsmul (↑n.succ : ℤ) a = zsmul (↑n : ℤ) a + a
zsmul_neg' : ∀ (n : ℕ) (a : R), zsmul (Int.negSucc n) a = -zsmul (↑n.succ : ℤ) a
neg_add_cancel : ∀ (a : R), -a + a = 0
intCast : ℤ → R
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))
toAddMonoidWithOne_1 : AddMonoidWithOne R
toNeg_1 : Neg R
toSub_1 : Sub R
sub_eq_add_neg_1 : ∀ (a b : R), a - b = a + -b
zsmul_1 : ℤ → R → R
zsmul_zero'_1 : ∀ (a : R), zsmul_1 0 a = 0
zsmul_succ'_1 : ∀ (n : ℕ) (a : R), zsmul_1 (↑n.succ : ℤ) a = zsmul_1 (↑n : ℤ) a + a
zsmul_neg'_1 : ∀ (n : ℕ) (a : R), zsmul_1 (Int.negSucc n) a = -zsmul_1 (↑n.succ : ℤ) a
neg_add_cancel_1 : ∀ (a : R), -a + a = 0
intCast_1 : ℤ → R
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_1 : Eq.{u + 1} (α := AddMonoidWithOne R) AddGroupWithOne.toAddMonoidWithOne AddGroupWithOne.toAddMonoidWithOne
this_2 : Eq.{u + 1} (α := NatCast R) AddMonoidWithOne.toNatCast AddMonoidWithOne.toNatCast
toAddMonoid_eq : Eq.{u + 1} (α := AddMonoid R) AddMonoidWithOne.toAddMonoid AddMonoidWithOne.toAddMonoid
toNeg_eq : Eq.{u + 1} (α := Neg R) AddGroupWithOne.toNeg AddGroupWithOne.toNeg
toSub_eq : Eq.{u + 1} (α := Sub R) AddGroupWithOne.toSub AddGroupWithOne.toSub
zsmul_eq : Eq.{u + 1} (α := ℤ → R → R) AddGroupWithOne.zsmul AddGroupWithOne.zsmul
this : Eq.{u + 1} (α := ℤ → R) IntCast.intCast IntCast.intCast
⊢ { intCast := intCast, toAddMonoidWithOne := toAddMonoidWithOne, toNeg := toNeg, toSub := toSub,
      sub_eq_add_neg := sub_eq_add_neg, zsmul := zsmul, zsmul_zero' := zsmul_zero', zsmul_succ' := zsmul_succ',
      zsmul_neg' := zsmul_neg', neg_add_cancel := neg_add_cancel, intCast_ofNat := intCast_ofNat,
      intCast_negSucc := intCast_negSucc : AddGroupWithOne R } =
    { intCast := intCast_1, toAddMonoidWithOne := toAddMonoidWithOne_1, toNeg := toNeg_1, toSub := toSub_1,
      sub_eq_add_neg := sub_eq_add_neg_1, zsmul := zsmul_1, zsmul_zero' := zsmul_zero'_1, zsmul_succ' := zsmul_succ'_1,
      zsmul_neg' := zsmul_neg'_1, neg_add_cancel := neg_add_cancel_1, intCast_ofNat := intCast_ofNat_1,
      intCast_negSucc := intCast_negSucc_1 }

Tactic:
congr
-- Module: Mathlib.Algebra.Ring.Ext
Goal:
R : Type u
inst₁ inst₂ : AddCommGroupWithOne R
h_add : Eq (α := R → R → R) HAdd.hAdd HAdd.hAdd
h_one : Eq.{u + 1} (α := R) One.one One.one
⊢ Eq.{u + 1} (α := AddCommGroup R) toAddCommGroup toAddCommGroup

Tactic:
have : inst₁.toAddCommGroup = inst₂.toAddCommGroup :=
    AddCommGroup.ext h_add
-- Module: Mathlib.Algebra.Ring.Ext
Goal:
R : Type u
inst₁ inst₂ : AddCommGroupWithOne 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) toAddCommGroup toAddCommGroup
⊢ Eq.{u + 1} (α := AddGroupWithOne R) toAddGroupWithOne toAddGroupWithOne

Tactic:
have : inst₁.toAddGroupWithOne = inst₂.toAddGroupWithOne :=
    AddGroupWithOne.ext h_add h_one
-- Module: Mathlib.Algebra.Ring.Ext
Goal:
R : Type u
inst₁ inst₂ : AddCommGroupWithOne R
h_add : Eq (α := R → R → R) HAdd.hAdd HAdd.hAdd
h_one : Eq.{u + 1} (α := R) One.one One.one
this_1 : Eq.{u + 1} (α := AddCommGroup R) toAddCommGroup toAddCommGroup
this : Eq.{u + 1} (α := AddGroupWithOne R) toAddGroupWithOne toAddGroupWithOne
⊢ Eq.{u + 1} (α := IntCast R) toIntCast toIntCast

Tactic:
injection this with _ h_addMonoidWithOne
-- Module: Mathlib.Algebra.Ring.Ext
Goal:
R : Type u
inst₁ inst₂ : AddCommGroupWithOne R
h_add : Eq (α := R → R → R) HAdd.hAdd HAdd.hAdd
h_one : Eq.{u + 1} (α := R) One.one One.one
this_1 : Eq.{u + 1} (α := AddCommGroup R) toAddCommGroup toAddCommGroup
this : Eq.{u + 1} (α := AddGroupWithOne R) toAddGroupWithOne toAddGroupWithOne
toIntCast_eq : Eq.{u + 1} (α := IntCast R) toIntCast toIntCast
⊢ Eq.{u + 1} (α := AddMonoidWithOne R)
    { toNatCast := inst₁.toNatCast, toAddMonoid := inst₁.toAddMonoid, toOne := inst₁.toOne, natCast_zero := ⋯,
      natCast_succ := ⋯ }
    { toNatCast := inst₂.toNatCast, toAddMonoid := inst₂.toAddMonoid, toOne := inst₂.toOne, natCast_zero := ⋯,
      natCast_succ := ⋯ }

Tactic:
injection this with _ h_addMonoidWithOne
-- Module: Mathlib.Algebra.Ring.Ext
Goal:
R : Type u
inst₁ inst₂ : AddCommGroupWithOne R
h_add : Eq (α := R → R → R) HAdd.hAdd HAdd.hAdd
h_one : Eq.{u + 1} (α := R) One.one One.one
this_1 : Eq.{u + 1} (α := AddCommGroup R) toAddCommGroup toAddCommGroup
this : Eq.{u + 1} (α := AddGroupWithOne R) toAddGroupWithOne toAddGroupWithOne
toIntCast_eq : Eq.{u + 1} (α := IntCast R) toIntCast toIntCast
h_addMonoidWithOne :
  Eq.{u + 1} (α := AddMonoidWithOne R)
    { toNatCast := inst₁.toNatCast, toAddMonoid := inst₁.toAddMonoid, toOne := inst₁.toOne, natCast_zero := ⋯,
      natCast_succ := ⋯ }
    { toNatCast := inst₂.toNatCast, toAddMonoid := inst₂.toAddMonoid, toOne := inst₂.toOne, natCast_zero := ⋯,
      natCast_succ := ⋯ }
⊢ Eq.{u + 1} (α := Neg R) SubNegMonoid.toNeg SubNegMonoid.toNeg

Tactic:
injection this with _ h_addMonoidWithOne
-- Module: Mathlib.Algebra.Ring.Ext
Goal:
R : Type u
inst₁ inst₂ : AddCommGroupWithOne R
h_add : Eq (α := R → R → R) HAdd.hAdd HAdd.hAdd
h_one : Eq.{u + 1} (α := R) One.one One.one
this_1 : Eq.{u + 1} (α := AddCommGroup R) toAddCommGroup toAddCommGroup
this : Eq.{u + 1} (α := AddGroupWithOne R) toAddGroupWithOne toAddGroupWithOne
toIntCast_eq : Eq.{u + 1} (α := IntCast R) toIntCast toIntCast
h_addMonoidWithOne :
  Eq.{u + 1} (α := AddMonoidWithOne R)
    { toNatCast := inst₁.toNatCast, toAddMonoid := inst₁.toAddMonoid, toOne := inst₁.toOne, natCast_zero := ⋯,
      natCast_succ := ⋯ }
    { toNatCast := inst₂.toNatCast, toAddMonoid := inst₂.toAddMonoid, toOne := inst₂.toOne, natCast_zero := ⋯,
      natCast_succ := ⋯ }
toNeg_eq : Eq.{u + 1} (α := Neg R) SubNegMonoid.toNeg SubNegMonoid.toNeg
⊢ Eq.{u + 1} (α := Sub R) SubNegMonoid.toSub SubNegMonoid.toSub

Tactic:
injection this with _ h_addMonoidWithOne
-- Module: Mathlib.Algebra.Ring.Ext
Goal:
R : Type u
inst₁ inst₂ : AddCommGroupWithOne R
h_add : Eq (α := R → R → R) HAdd.hAdd HAdd.hAdd
h_one : Eq.{u + 1} (α := R) One.one One.one
this_1 : Eq.{u + 1} (α := AddCommGroup R) toAddCommGroup toAddCommGroup
this : Eq.{u + 1} (α := AddGroupWithOne R) toAddGroupWithOne toAddGroupWithOne
toIntCast_eq : Eq.{u + 1} (α := IntCast R) toIntCast toIntCast
h_addMonoidWithOne :
  Eq.{u + 1} (α := AddMonoidWithOne R)
    { toNatCast := inst₁.toNatCast, toAddMonoid := inst₁.toAddMonoid, toOne := inst₁.toOne, natCast_zero := ⋯,
      natCast_succ := ⋯ }
    { toNatCast := inst₂.toNatCast, toAddMonoid := inst₂.toAddMonoid, toOne := inst₂.toOne, natCast_zero := ⋯,
      natCast_succ := ⋯ }
toNeg_eq : Eq.{u + 1} (α := Neg R) SubNegMonoid.toNeg SubNegMonoid.toNeg
toSub_eq : Eq.{u + 1} (α := Sub R) SubNegMonoid.toSub SubNegMonoid.toSub
⊢ Eq.{u + 1} (α := ℤ → R → R) SubNegMonoid.zsmul SubNegMonoid.zsmul

Tactic:
injection this with _ h_addMonoidWithOne
-- Module: Mathlib.Algebra.Ring.Ext
Goal:
R : Type u
inst₁ inst₂ : AddCommGroupWithOne 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) toAddCommGroup toAddCommGroup
toIntCast_eq : Eq.{u + 1} (α := IntCast R) toIntCast toIntCast
h_addMonoidWithOne :
  Eq.{u + 1} (α := AddMonoidWithOne R)
    { toNatCast := inst₁.toNatCast, toAddMonoid := inst₁.toAddMonoid, toOne := inst₁.toOne, natCast_zero := ⋯,
      natCast_succ := ⋯ }
    { toNatCast := inst₂.toNatCast, toAddMonoid := inst₂.toAddMonoid, toOne := inst₂.toOne, natCast_zero := ⋯,
      natCast_succ := ⋯ }
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
⊢ Eq.{u + 1} (α := NatCast R) toNatCast toNatCast

Tactic:
injection h_addMonoidWithOne
-- Module: Mathlib.Algebra.Ring.Ext
Goal:
R : Type u
inst₁ inst₂ : AddCommGroupWithOne 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) toAddCommGroup toAddCommGroup
toIntCast_eq : Eq.{u + 1} (α := IntCast R) toIntCast toIntCast
h_addMonoidWithOne :
  Eq.{u + 1} (α := AddMonoidWithOne R)
    { toNatCast := inst₁.toNatCast, toAddMonoid := inst₁.toAddMonoid, toOne := inst₁.toOne, natCast_zero := ⋯,
      natCast_succ := ⋯ }
    { toNatCast := inst₂.toNatCast, toAddMonoid := inst₂.toAddMonoid, toOne := inst₂.toOne, natCast_zero := ⋯,
      natCast_succ := ⋯ }
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) toNatCast toNatCast
⊢ Eq.{u + 1} (α := AddMonoid R) SubNegMonoid.toAddMonoid SubNegMonoid.toAddMonoid

Tactic:
injection h_addMonoidWithOne
-- Module: Mathlib.Algebra.Ring.Ext
Goal:
R : Type u
inst₁ inst₂ : AddCommGroupWithOne 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) toAddCommGroup toAddCommGroup
toIntCast_eq : Eq.{u + 1} (α := IntCast R) toIntCast toIntCast
h_addMonoidWithOne :
  Eq.{u + 1} (α := AddMonoidWithOne R)
    { toNatCast := inst₁.toNatCast, toAddMonoid := inst₁.toAddMonoid, toOne := inst₁.toOne, natCast_zero := ⋯,
      natCast_succ := ⋯ }
    { toNatCast := inst₂.toNatCast, toAddMonoid := inst₂.toAddMonoid, toOne := inst₂.toOne, natCast_zero := ⋯,
      natCast_succ := ⋯ }
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) toNatCast toNatCast
toAddMonoid_eq : Eq.{u + 1} (α := AddMonoid R) SubNegMonoid.toAddMonoid SubNegMonoid.toAddMonoid
⊢ Eq.{u + 1} (α := One R) toOne toOne

Tactic:
injection h_addMonoidWithOne
-- Module: Mathlib.Algebra.Ring.Ext
Goal:
R : Type u
inst₁ inst₂ : AddCommGroupWithOne 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) toAddCommGroup toAddCommGroup
toIntCast_eq : Eq.{u + 1} (α := IntCast R) toIntCast 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) toNatCast toNatCast
toAddMonoid_eq : Eq.{u + 1} (α := AddMonoid R) SubNegMonoid.toAddMonoid SubNegMonoid.toAddMonoid
toOne_eq : Eq.{u + 1} (α := One R) toOne toOne
mk :
  ∀ [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),
    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 } =
                    inst₂
⊢ inst₁ = inst₂

Tactic:
cases inst₁
-- Module: Mathlib.Algebra.Ring.Ext
Goal:
R : Type u
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))
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
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 } =
    { 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:
congr
-- Module: Mathlib.Algebra.Ring.Ext
Goal:
R : Type u
inst₁ inst₂ : NonAssocRing R
h_add : Eq (α := R → R → R) HAdd.hAdd HAdd.hAdd
h_mul : Eq (α := R → R → R) HMul.hMul HMul.hMul
h_add₁ : Eq (α := R → R → R) HAdd.hAdd HAdd.hAdd
h_mul₁ : Eq (α := R → R → R) HMul.hMul HMul.hMul
⊢ Eq.{u + 1} (α := NonUnitalNonAssocRing R) toNonUnitalNonAssocRing toNonUnitalNonAssocRing

Tactic:
ext : 1
-- Module: Mathlib.Algebra.Ring.Ext
Goal:
R : Type u
inst₁ inst₂ : NonAssocRing R
h_add : Eq (α := R → R → R) HAdd.hAdd HAdd.hAdd
h_mul : Eq (α := R → R → R) HMul.hMul HMul.hMul
⊢ Eq (α := R → R → R) HAdd.hAdd HAdd.hAdd

Tactic:
assumption
-- Module: Mathlib.Algebra.Ring.Ext
Goal:
R : Type u
inst₁ inst₂ : NonAssocRing R
h_add : Eq (α := R → R → R) HAdd.hAdd HAdd.hAdd
h_mul : Eq (α := R → R → R) HMul.hMul HMul.hMul
⊢ Eq (α := R → R → R) HMul.hMul HMul.hMul

Tactic:
assumption
-- Module: Mathlib.Algebra.Ring.Ext
Goal:
R : Type u
inst₁ inst₂ : NonAssocRing R
h_add : Eq (α := R → R → R) HAdd.hAdd HAdd.hAdd
h_mul : Eq (α := R → R → R) HMul.hMul HMul.hMul
⊢ Eq.{u + 1} (α := NonUnitalNonAssocRing R) toNonUnitalNonAssocRing toNonUnitalNonAssocRing

Tactic:
have h₁ : inst₁.toNonUnitalNonAssocRing = inst₂.toNonUnitalNonAssocRing := by
    ext : 1 <;> assumption
-- Module: Mathlib.Algebra.Ring.Ext
Goal:
R : Type u
inst₁ inst₂ : NonAssocRing R
h_add : Eq (α := R → R → R) HAdd.hAdd HAdd.hAdd
h_mul : Eq (α := R → R → R) HMul.hMul HMul.hMul
h₁ : Eq.{u + 1} (α := NonUnitalNonAssocRing R) toNonUnitalNonAssocRing toNonUnitalNonAssocRing
h_add₁ : Eq (α := R → R → R) HAdd.hAdd HAdd.hAdd
h_mul₁ : Eq (α := R → R → R) HMul.hMul HMul.hMul
⊢ Eq.{u + 1} (α := NonAssocSemiring R) toNonAssocSemiring toNonAssocSemiring

Tactic:
ext : 1
-- Module: Mathlib.Algebra.Ring.Ext
Goal:
R : Type u
inst₁ inst₂ : NonAssocRing R
h_add : Eq (α := R → R → R) HAdd.hAdd HAdd.hAdd
h_mul : Eq (α := R → R → R) HMul.hMul HMul.hMul
h₁ : Eq.{u + 1} (α := NonUnitalNonAssocRing R) toNonUnitalNonAssocRing toNonUnitalNonAssocRing
⊢ Eq (α := R → R → R) HAdd.hAdd HAdd.hAdd

Tactic:
assumption
-- Module: Mathlib.Algebra.Ring.Ext
Goal:
R : Type u
inst₁ inst₂ : NonAssocRing R
h_add : Eq (α := R → R → R) HAdd.hAdd HAdd.hAdd
h_mul : Eq (α := R → R → R) HMul.hMul HMul.hMul
h₁ : Eq.{u + 1} (α := NonUnitalNonAssocRing R) toNonUnitalNonAssocRing toNonUnitalNonAssocRing
⊢ Eq (α := R → R → R) HMul.hMul HMul.hMul

Tactic:
assumption
-- Module: Mathlib.Algebra.Ring.Ext
Goal:
R : Type u
inst₁ inst₂ : NonAssocRing R
h_add : Eq (α := R → R → R) HAdd.hAdd HAdd.hAdd
h_mul : Eq (α := R → R → R) HMul.hMul HMul.hMul
h₁ : Eq.{u + 1} (α := NonUnitalNonAssocRing R) toNonUnitalNonAssocRing toNonUnitalNonAssocRing
⊢ Eq.{u + 1} (α := NonAssocSemiring R) toNonAssocSemiring toNonAssocSemiring

Tactic:
have h₂ : inst₁.toNonAssocSemiring = inst₂.toNonAssocSemiring := by
    ext : 1 <;> assumption
-- Module: Mathlib.Algebra.Ring.Ext
Goal:
R : Type u
inst₁ inst₂ : NonAssocRing R
h_add : Eq (α := R → R → R) HAdd.hAdd HAdd.hAdd
h_mul : Eq (α := R → R → R) HMul.hMul HMul.hMul
h₁ : Eq.{u + 1} (α := NonUnitalNonAssocRing R) toNonUnitalNonAssocRing toNonUnitalNonAssocRing
h₂ : Eq.{u + 1} (α := NonAssocSemiring R) toNonAssocSemiring toNonAssocSemiring
⊢ Eq.{u + 1} (α := AddCommGroupWithOne R) toAddCommGroupWithOne toAddCommGroupWithOne

Tactic:
have h₃ : inst₁.toAddCommGroupWithOne = inst₂.toAddCommGroupWithOne :=
    AddCommGroupWithOne.ext h_add (congrArg (·.toOne.one) h₂)