awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Int.Cast.Basic (goal)
Goal:
R : Type u
inst : AddGroupWithOne R
m n : ℕ
rw : (↑(subNatNat n m.succ) : R) = HAdd.hAdd (α := R) (↑-[m+1] : R) (↑(↑n : ℤ) : R)
rw₁ : HSub.hSub (α := R) (↑n : R) (↑m.succ : R) = HAdd.hAdd (α := R) (↑-[m+1] : R) (↑(↑n : ℤ) : R)
rw₂ : HSub.hSub (α := R) (↑n : R) (↑m.succ : R) = HAdd.hAdd (α := R) (↑-[m+1] : R) (↑n : R)
⊢ (↑(-[m+1] + (↑n : ℤ)) : R) = HAdd.hAdd (α := R) (↑-[m+1] : R) (↑(↑n : ℤ) : R)
have rw₃ : HSub.hSub (α := R) (↑n : R) (↑m.succ : R) = HAdd.hAdd (α := R) (-(↑(m + 1) : R)) (↑n : R)
Tactic: rw [Int.negSucc_add_ofNat, cast_subNatNat, cast_natCast, cast_negSucc, sub_eq_iff_eq_add,
      add_assoc, eq_neg_add_iff_add_eq, ← Nat.cast_add, ← Nat.cast_add, Nat.add_comm]
-- Lean 4 proof step from Mathlib.Data.Int.Cast.Basic (goal)
Goal:
R : Type u
inst : AddGroupWithOne R
m n : ℕ
rw : (↑(subNatNat n m.succ) : R) = HAdd.hAdd (α := R) (↑-[m+1] : R) (↑(↑n : ℤ) : R)
rw₁ : HSub.hSub (α := R) (↑n : R) (↑m.succ : R) = HAdd.hAdd (α := R) (↑-[m+1] : R) (↑(↑n : ℤ) : R)
rw₂ : HSub.hSub (α := R) (↑n : R) (↑m.succ : R) = HAdd.hAdd (α := R) (↑-[m+1] : R) (↑n : R)
rw₃ : HSub.hSub (α := R) (↑n : R) (↑m.succ : R) = HAdd.hAdd (α := R) (-(↑(m + 1) : R)) (↑n : R)
⊢ (↑(-[m+1] + (↑n : ℤ)) : R) = HAdd.hAdd (α := R) (↑-[m+1] : R) (↑(↑n : ℤ) : R)
have rw₄ : (↑n : R) = HAdd.hAdd (α := R) (-(↑(m + 1) : R)) (↑n : R) + (↑m.succ : R)
Tactic: rw [Int.negSucc_add_ofNat, cast_subNatNat, cast_natCast, cast_negSucc, sub_eq_iff_eq_add,
      add_assoc, eq_neg_add_iff_add_eq, ← Nat.cast_add, ← Nat.cast_add, Nat.add_comm]
-- Lean 4 proof step from Mathlib.Data.Int.Cast.Basic (goal)
Goal:
R : Type u
inst : AddGroupWithOne R
m n : ℕ
rw : (↑(subNatNat n m.succ) : R) = HAdd.hAdd (α := R) (↑-[m+1] : R) (↑(↑n : ℤ) : R)
rw₁ : HSub.hSub (α := R) (↑n : R) (↑m.succ : R) = HAdd.hAdd (α := R) (↑-[m+1] : R) (↑(↑n : ℤ) : R)
rw₂ : HSub.hSub (α := R) (↑n : R) (↑m.succ : R) = HAdd.hAdd (α := R) (↑-[m+1] : R) (↑n : R)
rw₃ : HSub.hSub (α := R) (↑n : R) (↑m.succ : R) = HAdd.hAdd (α := R) (-(↑(m + 1) : R)) (↑n : R)
rw₄ : (↑n : R) = HAdd.hAdd (α := R) (-(↑(m + 1) : R)) (↑n : R) + (↑m.succ : R)
⊢ (↑(-[m+1] + (↑n : ℤ)) : R) = HAdd.hAdd (α := R) (↑-[m+1] : R) (↑(↑n : ℤ) : R)
have rw₅ : (↑n : R) = -(↑(m + 1) : R) + HAdd.hAdd (α := R) (↑n : R) (↑m.succ : R)
Tactic: rw [Int.negSucc_add_ofNat, cast_subNatNat, cast_natCast, cast_negSucc, sub_eq_iff_eq_add,
      add_assoc, eq_neg_add_iff_add_eq, ← Nat.cast_add, ← Nat.cast_add, Nat.add_comm]
-- Lean 4 proof step from Mathlib.Data.Int.Cast.Basic (goal)
Goal:
R : Type u
inst : AddGroupWithOne R
m n : ℕ
rw : (↑(subNatNat n m.succ) : R) = HAdd.hAdd (α := R) (↑-[m+1] : R) (↑(↑n : ℤ) : R)
rw₁ : HSub.hSub (α := R) (↑n : R) (↑m.succ : R) = HAdd.hAdd (α := R) (↑-[m+1] : R) (↑(↑n : ℤ) : R)
rw₂ : HSub.hSub (α := R) (↑n : R) (↑m.succ : R) = HAdd.hAdd (α := R) (↑-[m+1] : R) (↑n : R)
rw₃ : HSub.hSub (α := R) (↑n : R) (↑m.succ : R) = HAdd.hAdd (α := R) (-(↑(m + 1) : R)) (↑n : R)
rw₄ : (↑n : R) = HAdd.hAdd (α := R) (-(↑(m + 1) : R)) (↑n : R) + (↑m.succ : R)
rw₅ : (↑n : R) = -(↑(m + 1) : R) + HAdd.hAdd (α := R) (↑n : R) (↑m.succ : R)
⊢ (↑(-[m+1] + (↑n : ℤ)) : R) = HAdd.hAdd (α := R) (↑-[m+1] : R) (↑(↑n : ℤ) : R)
have rw₆ : HAdd.hAdd (α := R) (↑(m + 1) : R) (↑n : R) = HAdd.hAdd (α := R) (↑n : R) (↑m.succ : R)
Tactic: rw [Int.negSucc_add_ofNat, cast_subNatNat, cast_natCast, cast_negSucc, sub_eq_iff_eq_add,
      add_assoc, eq_neg_add_iff_add_eq, ← Nat.cast_add, ← Nat.cast_add, Nat.add_comm]
-- Lean 4 proof step from Mathlib.Data.Int.Cast.Basic (goal)
Goal:
R : Type u
inst : AddGroupWithOne R
m n : ℕ
rw : (↑(subNatNat n m.succ) : R) = HAdd.hAdd (α := R) (↑-[m+1] : R) (↑(↑n : ℤ) : R)
rw₁ : HSub.hSub (α := R) (↑n : R) (↑m.succ : R) = HAdd.hAdd (α := R) (↑-[m+1] : R) (↑(↑n : ℤ) : R)
rw₂ : HSub.hSub (α := R) (↑n : R) (↑m.succ : R) = HAdd.hAdd (α := R) (↑-[m+1] : R) (↑n : R)
rw₃ : HSub.hSub (α := R) (↑n : R) (↑m.succ : R) = HAdd.hAdd (α := R) (-(↑(m + 1) : R)) (↑n : R)
rw₄ : (↑n : R) = HAdd.hAdd (α := R) (-(↑(m + 1) : R)) (↑n : R) + (↑m.succ : R)
rw₅ : (↑n : R) = -(↑(m + 1) : R) + HAdd.hAdd (α := R) (↑n : R) (↑m.succ : R)
rw₆ : HAdd.hAdd (α := R) (↑(m + 1) : R) (↑n : R) = HAdd.hAdd (α := R) (↑n : R) (↑m.succ : R)
⊢ (↑(-[m+1] + (↑n : ℤ)) : R) = HAdd.hAdd (α := R) (↑-[m+1] : R) (↑(↑n : ℤ) : R)
have rw₇ : (↑(m + 1 + n) : R) = HAdd.hAdd (α := R) (↑n : R) (↑m.succ : R)
Tactic: rw [Int.negSucc_add_ofNat, cast_subNatNat, cast_natCast, cast_negSucc, sub_eq_iff_eq_add,
      add_assoc, eq_neg_add_iff_add_eq, ← Nat.cast_add, ← Nat.cast_add, Nat.add_comm]
-- Lean 4 proof step from Mathlib.Data.Int.Cast.Basic (goal)
Goal:
R : Type u
inst : AddGroupWithOne R
m n : ℕ
rw : (↑(subNatNat n m.succ) : R) = HAdd.hAdd (α := R) (↑-[m+1] : R) (↑(↑n : ℤ) : R)
rw₁ : HSub.hSub (α := R) (↑n : R) (↑m.succ : R) = HAdd.hAdd (α := R) (↑-[m+1] : R) (↑(↑n : ℤ) : R)
rw₂ : HSub.hSub (α := R) (↑n : R) (↑m.succ : R) = HAdd.hAdd (α := R) (↑-[m+1] : R) (↑n : R)
rw₃ : HSub.hSub (α := R) (↑n : R) (↑m.succ : R) = HAdd.hAdd (α := R) (-(↑(m + 1) : R)) (↑n : R)
rw₄ : (↑n : R) = HAdd.hAdd (α := R) (-(↑(m + 1) : R)) (↑n : R) + (↑m.succ : R)
rw₅ : (↑n : R) = -(↑(m + 1) : R) + HAdd.hAdd (α := R) (↑n : R) (↑m.succ : R)
rw₆ : HAdd.hAdd (α := R) (↑(m + 1) : R) (↑n : R) = HAdd.hAdd (α := R) (↑n : R) (↑m.succ : R)
rw₇ : (↑(m + 1 + n) : R) = HAdd.hAdd (α := R) (↑n : R) (↑m.succ : R)
⊢ (↑(-[m+1] + (↑n : ℤ)) : R) = HAdd.hAdd (α := R) (↑-[m+1] : R) (↑(↑n : ℤ) : R)
have rw₈ : Eq.{u + 1} (α := R) (↑(m + 1 + n) : R) (↑(n + m.succ) : R)
Tactic: rw [Int.negSucc_add_ofNat, cast_subNatNat, cast_natCast, cast_negSucc, sub_eq_iff_eq_add,
      add_assoc, eq_neg_add_iff_add_eq, ← Nat.cast_add, ← Nat.cast_add, Nat.add_comm]
-- Lean 4 proof step from Mathlib.Data.Int.Cast.Basic (goal)
Goal:
R : Type u
inst : AddGroupWithOne R
m n : ℕ
rw : (↑(subNatNat n m.succ) : R) = HAdd.hAdd (α := R) (↑-[m+1] : R) (↑(↑n : ℤ) : R)
rw₁ : HSub.hSub (α := R) (↑n : R) (↑m.succ : R) = HAdd.hAdd (α := R) (↑-[m+1] : R) (↑(↑n : ℤ) : R)
rw₂ : HSub.hSub (α := R) (↑n : R) (↑m.succ : R) = HAdd.hAdd (α := R) (↑-[m+1] : R) (↑n : R)
rw₃ : HSub.hSub (α := R) (↑n : R) (↑m.succ : R) = HAdd.hAdd (α := R) (-(↑(m + 1) : R)) (↑n : R)
rw₄ : (↑n : R) = HAdd.hAdd (α := R) (-(↑(m + 1) : R)) (↑n : R) + (↑m.succ : R)
rw₅ : (↑n : R) = -(↑(m + 1) : R) + HAdd.hAdd (α := R) (↑n : R) (↑m.succ : R)
rw₆ : HAdd.hAdd (α := R) (↑(m + 1) : R) (↑n : R) = HAdd.hAdd (α := R) (↑n : R) (↑m.succ : R)
rw₇ : (↑(m + 1 + n) : R) = HAdd.hAdd (α := R) (↑n : R) (↑m.succ : R)
rw₈ : Eq.{u + 1} (α := R) (↑(m + 1 + n) : R) (↑(n + m.succ) : R)
⊢ (↑(-[m+1] + (↑n : ℤ)) : R) = HAdd.hAdd (α := R) (↑-[m+1] : R) (↑(↑n : ℤ) : R)
have rw₉ : Eq.{u + 1} (α := R) (↑(n + (m + 1)) : R) (↑(n + m.succ) : R)
Tactic: rw [Int.negSucc_add_ofNat, cast_subNatNat, cast_natCast, cast_negSucc, sub_eq_iff_eq_add,
      add_assoc, eq_neg_add_iff_add_eq, ← Nat.cast_add, ← Nat.cast_add, Nat.add_comm]
-- Lean 4 proof step from Mathlib.Data.Int.Cast.Basic (goal)
Goal:
R : Type u
inst : AddGroupWithOne R
m n : ℕ
⊢ (↑(-[m+1] + -[n+1]) : R) = HAdd.hAdd (α := R) (↑-[m+1] : R) (↑-[n+1] : R)
have rw : (↑-[(m + n).succ+1] : R) = HAdd.hAdd (α := R) (↑-[m+1] : R) (↑-[n+1] : R)
Tactic: rw [Int.negSucc_add_negSucc, succ_eq_add_one, cast_negSucc, cast_negSucc, cast_negSucc,
      ← neg_add_rev, ← Nat.cast_add, Nat.add_right_comm m n 1, Nat.add_assoc, Nat.add_comm]
-- Lean 4 proof step from Mathlib.Data.Int.Cast.Basic (goal)
Goal:
R : Type u
inst : AddGroupWithOne R
m n : ℕ
rw : (↑-[(m + n).succ+1] : R) = HAdd.hAdd (α := R) (↑-[m+1] : R) (↑-[n+1] : R)
rw₁ : (↑-[m + n + 1+1] : R) = HAdd.hAdd (α := R) (↑-[m+1] : R) (↑-[n+1] : R)
⊢ (↑(-[m+1] + -[n+1]) : R) = HAdd.hAdd (α := R) (↑-[m+1] : R) (↑-[n+1] : R)
have rw₂ : -(↑(m + n + 1 + 1) : R) = HAdd.hAdd (α := R) (↑-[m+1] : R) (↑-[n+1] : R)
Tactic: rw [Int.negSucc_add_negSucc, succ_eq_add_one, cast_negSucc, cast_negSucc, cast_negSucc,
      ← neg_add_rev, ← Nat.cast_add, Nat.add_right_comm m n 1, Nat.add_assoc, Nat.add_comm]
-- Lean 4 proof step from Mathlib.Data.Int.Cast.Basic (goal)
Goal:
R : Type u
inst : AddGroupWithOne R
m n : ℕ
rw : (↑-[(m + n).succ+1] : R) = HAdd.hAdd (α := R) (↑-[m+1] : R) (↑-[n+1] : R)
rw₁ : (↑-[m + n + 1+1] : R) = HAdd.hAdd (α := R) (↑-[m+1] : R) (↑-[n+1] : R)
rw₂ : -(↑(m + n + 1 + 1) : R) = HAdd.hAdd (α := R) (↑-[m+1] : R) (↑-[n+1] : R)
⊢ (↑(-[m+1] + -[n+1]) : R) = HAdd.hAdd (α := R) (↑-[m+1] : R) (↑-[n+1] : R)
have rw₃ : -(↑(m + n + 1 + 1) : R) = HAdd.hAdd (α := R) (-(↑(m + 1) : R)) (↑-[n+1] : R)
Tactic: rw [Int.negSucc_add_negSucc, succ_eq_add_one, cast_negSucc, cast_negSucc, cast_negSucc,
      ← neg_add_rev, ← Nat.cast_add, Nat.add_right_comm m n 1, Nat.add_assoc, Nat.add_comm]
-- Lean 4 proof step from Mathlib.Data.Int.Cast.Basic (goal)
Goal:
R : Type u
inst : AddGroupWithOne R
m n : ℕ
rw : (↑-[(m + n).succ+1] : R) = HAdd.hAdd (α := R) (↑-[m+1] : R) (↑-[n+1] : R)
rw₁ : (↑-[m + n + 1+1] : R) = HAdd.hAdd (α := R) (↑-[m+1] : R) (↑-[n+1] : R)
rw₂ : -(↑(m + n + 1 + 1) : R) = HAdd.hAdd (α := R) (↑-[m+1] : R) (↑-[n+1] : R)
rw₃ : -(↑(m + n + 1 + 1) : R) = HAdd.hAdd (α := R) (-(↑(m + 1) : R)) (↑-[n+1] : R)
⊢ (↑(-[m+1] + -[n+1]) : R) = HAdd.hAdd (α := R) (↑-[m+1] : R) (↑-[n+1] : R)
have rw₄ : -(↑(m + n + 1 + 1) : R) = HAdd.hAdd (α := R) (-(↑(m + 1) : R)) (-(↑(n + 1) : R))
Tactic: rw [Int.negSucc_add_negSucc, succ_eq_add_one, cast_negSucc, cast_negSucc, cast_negSucc,
      ← neg_add_rev, ← Nat.cast_add, Nat.add_right_comm m n 1, Nat.add_assoc, Nat.add_comm]
-- Lean 4 proof step from Mathlib.Data.Int.Cast.Basic (goal)
Goal:
R : Type u
inst : AddGroupWithOne R
m n : ℕ
rw : (↑-[(m + n).succ+1] : R) = HAdd.hAdd (α := R) (↑-[m+1] : R) (↑-[n+1] : R)
rw₁ : (↑-[m + n + 1+1] : R) = HAdd.hAdd (α := R) (↑-[m+1] : R) (↑-[n+1] : R)
rw₂ : -(↑(m + n + 1 + 1) : R) = HAdd.hAdd (α := R) (↑-[m+1] : R) (↑-[n+1] : R)
rw₃ : -(↑(m + n + 1 + 1) : R) = HAdd.hAdd (α := R) (-(↑(m + 1) : R)) (↑-[n+1] : R)
rw₄ : -(↑(m + n + 1 + 1) : R) = HAdd.hAdd (α := R) (-(↑(m + 1) : R)) (-(↑(n + 1) : R))
⊢ (↑(-[m+1] + -[n+1]) : R) = HAdd.hAdd (α := R) (↑-[m+1] : R) (↑-[n+1] : R)
have rw₅ : -(↑(m + n + 1 + 1) : R) = -HAdd.hAdd (α := R) (↑(n + 1) : R) (↑(m + 1) : R)
Tactic: rw [Int.negSucc_add_negSucc, succ_eq_add_one, cast_negSucc, cast_negSucc, cast_negSucc,
      ← neg_add_rev, ← Nat.cast_add, Nat.add_right_comm m n 1, Nat.add_assoc, Nat.add_comm]
-- Lean 4 proof step from Mathlib.Data.Int.Cast.Basic (goal)
Goal:
R : Type u
inst : AddGroupWithOne R
m n : ℕ
rw : (↑-[(m + n).succ+1] : R) = HAdd.hAdd (α := R) (↑-[m+1] : R) (↑-[n+1] : R)
rw₁ : (↑-[m + n + 1+1] : R) = HAdd.hAdd (α := R) (↑-[m+1] : R) (↑-[n+1] : R)
rw₂ : -(↑(m + n + 1 + 1) : R) = HAdd.hAdd (α := R) (↑-[m+1] : R) (↑-[n+1] : R)
rw₃ : -(↑(m + n + 1 + 1) : R) = HAdd.hAdd (α := R) (-(↑(m + 1) : R)) (↑-[n+1] : R)
rw₄ : -(↑(m + n + 1 + 1) : R) = HAdd.hAdd (α := R) (-(↑(m + 1) : R)) (-(↑(n + 1) : R))
rw₅ : -(↑(m + n + 1 + 1) : R) = -HAdd.hAdd (α := R) (↑(n + 1) : R) (↑(m + 1) : R)
⊢ (↑(-[m+1] + -[n+1]) : R) = HAdd.hAdd (α := R) (↑-[m+1] : R) (↑-[n+1] : R)
have rw₆ : Eq.{u + 1} (α := R) (-(↑(m + n + 1 + 1) : R)) (-(↑(n + 1 + (m + 1)) : R))
Tactic: rw [Int.negSucc_add_negSucc, succ_eq_add_one, cast_negSucc, cast_negSucc, cast_negSucc,
      ← neg_add_rev, ← Nat.cast_add, Nat.add_right_comm m n 1, Nat.add_assoc, Nat.add_comm]
-- Lean 4 proof step from Mathlib.Data.Int.Cast.Basic (goal)
Goal:
R : Type u
inst : AddGroupWithOne R
m n : ℕ
rw : (↑-[(m + n).succ+1] : R) = HAdd.hAdd (α := R) (↑-[m+1] : R) (↑-[n+1] : R)
rw₁ : (↑-[m + n + 1+1] : R) = HAdd.hAdd (α := R) (↑-[m+1] : R) (↑-[n+1] : R)
rw₂ : -(↑(m + n + 1 + 1) : R) = HAdd.hAdd (α := R) (↑-[m+1] : R) (↑-[n+1] : R)
rw₃ : -(↑(m + n + 1 + 1) : R) = HAdd.hAdd (α := R) (-(↑(m + 1) : R)) (↑-[n+1] : R)
rw₄ : -(↑(m + n + 1 + 1) : R) = HAdd.hAdd (α := R) (-(↑(m + 1) : R)) (-(↑(n + 1) : R))
rw₅ : -(↑(m + n + 1 + 1) : R) = -HAdd.hAdd (α := R) (↑(n + 1) : R) (↑(m + 1) : R)
rw₆ : Eq.{u + 1} (α := R) (-(↑(m + n + 1 + 1) : R)) (-(↑(n + 1 + (m + 1)) : R))
⊢ (↑(-[m+1] + -[n+1]) : R) = HAdd.hAdd (α := R) (↑-[m+1] : R) (↑-[n+1] : R)
have rw₇ : Eq.{u + 1} (α := R) (-(↑(m + 1 + n + 1) : R)) (-(↑(n + 1 + (m + 1)) : R))
Tactic: rw [Int.negSucc_add_negSucc, succ_eq_add_one, cast_negSucc, cast_negSucc, cast_negSucc,
      ← neg_add_rev, ← Nat.cast_add, Nat.add_right_comm m n 1, Nat.add_assoc, Nat.add_comm]
-- Lean 4 proof step from Mathlib.Data.Int.Cast.Basic (goal)
Goal:
R : Type u
inst : AddGroupWithOne R
m n : ℕ
rw : (↑-[(m + n).succ+1] : R) = HAdd.hAdd (α := R) (↑-[m+1] : R) (↑-[n+1] : R)
rw₁ : (↑-[m + n + 1+1] : R) = HAdd.hAdd (α := R) (↑-[m+1] : R) (↑-[n+1] : R)
rw₂ : -(↑(m + n + 1 + 1) : R) = HAdd.hAdd (α := R) (↑-[m+1] : R) (↑-[n+1] : R)
rw₃ : -(↑(m + n + 1 + 1) : R) = HAdd.hAdd (α := R) (-(↑(m + 1) : R)) (↑-[n+1] : R)
rw₄ : -(↑(m + n + 1 + 1) : R) = HAdd.hAdd (α := R) (-(↑(m + 1) : R)) (-(↑(n + 1) : R))
rw₅ : -(↑(m + n + 1 + 1) : R) = -HAdd.hAdd (α := R) (↑(n + 1) : R) (↑(m + 1) : R)
rw₆ : Eq.{u + 1} (α := R) (-(↑(m + n + 1 + 1) : R)) (-(↑(n + 1 + (m + 1)) : R))
rw₇ : Eq.{u + 1} (α := R) (-(↑(m + 1 + n + 1) : R)) (-(↑(n + 1 + (m + 1)) : R))
⊢ (↑(-[m+1] + -[n+1]) : R) = HAdd.hAdd (α := R) (↑-[m+1] : R) (↑-[n+1] : R)
have rw₈ : Eq.{u + 1} (α := R) (-(↑(m + 1 + (n + 1)) : R)) (-(↑(n + 1 + (m + 1)) : R))
Tactic: rw [Int.negSucc_add_negSucc, succ_eq_add_one, cast_negSucc, cast_negSucc, cast_negSucc,
      ← neg_add_rev, ← Nat.cast_add, Nat.add_right_comm m n 1, Nat.add_assoc, Nat.add_comm]
-- Lean 4 proof step from Mathlib.Data.Int.Cast.Basic (goal)
Goal:
R : Type u
inst : AddGroupWithOne R
m n : ℕ
rw : (↑-[(m + n).succ+1] : R) = HAdd.hAdd (α := R) (↑-[m+1] : R) (↑-[n+1] : R)
rw₁ : (↑-[m + n + 1+1] : R) = HAdd.hAdd (α := R) (↑-[m+1] : R) (↑-[n+1] : R)
rw₂ : -(↑(m + n + 1 + 1) : R) = HAdd.hAdd (α := R) (↑-[m+1] : R) (↑-[n+1] : R)
rw₃ : -(↑(m + n + 1 + 1) : R) = HAdd.hAdd (α := R) (-(↑(m + 1) : R)) (↑-[n+1] : R)
rw₄ : -(↑(m + n + 1 + 1) : R) = HAdd.hAdd (α := R) (-(↑(m + 1) : R)) (-(↑(n + 1) : R))
rw₅ : -(↑(m + n + 1 + 1) : R) = -HAdd.hAdd (α := R) (↑(n + 1) : R) (↑(m + 1) : R)
rw₆ : Eq.{u + 1} (α := R) (-(↑(m + n + 1 + 1) : R)) (-(↑(n + 1 + (m + 1)) : R))
rw₇ : Eq.{u + 1} (α := R) (-(↑(m + 1 + n + 1) : R)) (-(↑(n + 1 + (m + 1)) : R))
rw₈ : Eq.{u + 1} (α := R) (-(↑(m + 1 + (n + 1)) : R)) (-(↑(n + 1 + (m + 1)) : R))
⊢ (↑(-[m+1] + -[n+1]) : R) = HAdd.hAdd (α := R) (↑-[m+1] : R) (↑-[n+1] : R)
have rw₉ : Eq.{u + 1} (α := R) (-(↑(n + 1 + (m + 1)) : R)) (-(↑(n + 1 + (m + 1)) : R))
Tactic: rw [Int.negSucc_add_negSucc, succ_eq_add_one, cast_negSucc, cast_negSucc, cast_negSucc,
      ← neg_add_rev, ← Nat.cast_add, Nat.add_right_comm m n 1, Nat.add_assoc, Nat.add_comm]
-- Lean 4 proof step from Mathlib.Data.Int.Cast.Basic (goal)
Goal:
R : Type u_1
inst : AddGroupWithOne R
n : ℤ
⊢ HSMul.hSMul (β := R) n 1 = (↑n : R)
have ofNat : ∀ (a : ℕ), HSMul.hSMul (β := R) (Int.ofNat a) 1 = (↑(Int.ofNat a) : R)
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Int.Cast.Basic (goal)
Goal:
R : Type u_1
inst : AddGroupWithOne R
n : ℤ
ofNat : ∀ (a : ℕ), HSMul.hSMul (β := R) (Int.ofNat a) 1 = (↑(Int.ofNat a) : R)
⊢ HSMul.hSMul (β := R) n 1 = (↑n : R)
have negSucc : ∀ (a : ℕ), HSMul.hSMul (β := R) (Int.negSucc a) 1 = (↑(Int.negSucc a) : R)
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Int.Cast.Field (goal)
Goal:
α : Type u_1
inst : DivisionRing α
m n : ℤ
n_dvd : n ∣ m
hn : Ne.{u_1 + 1} (α := α) (↑n : α) 0
⊢ (↑(m / n) : α) = HDiv.hDiv (α := α) (↑m : α) (↑n : α)
have rcases : ∀ (k : ℤ), (↑(n * k / n) : α) = HDiv.hDiv (α := α) (↑(n * k) : α) (↑n : α)
Tactic: rcases n_dvd with ⟨k, rfl⟩
Cleared hypotheses: m, n_dvd
-- Lean 4 proof step from Mathlib.Data.Int.Cast.Field (hypothesis)
Goal:
α : Type u_1
inst : DivisionRing α
n : ℤ
hn : Ne.{u_1 + 1} (α := α) (↑n : α) 0
k : ℤ
⊢ (↑(n * k / n) : α) = HDiv.hDiv (α := α) (↑(n * k) : α) (↑n : α)
have this : n ≠ 0
Tactic: have : n ≠ 0 := by rintro rfl; simp at hn
-- Lean 4 proof step from Mathlib.Data.Int.Cast.Field (goal)
Goal:
α : Type u_1
inst : DivisionRing α
n : ℤ
hn : Ne.{u_1 + 1} (α := α) (↑n : α) 0
k : ℤ
this : n ≠ 0
⊢ (↑(n * k / n) : α) = HDiv.hDiv (α := α) (↑(n * k) : α) (↑n : α)
have rw : (↑k : α) = HDiv.hDiv (α := α) (↑(n * k) : α) (↑n : α)
Tactic: rw [Int.mul_ediv_cancel_left _ this, mul_comm n, Int.cast_mul, mul_div_cancel_right₀ _ hn]
-- Lean 4 proof step from Mathlib.Data.Int.Cast.Field (goal)
Goal:
α : Type u_1
inst : DivisionRing α
n : ℤ
hn : Ne.{u_1 + 1} (α := α) (↑n : α) 0
k : ℤ
this : n ≠ 0
rw : (↑k : α) = HDiv.hDiv (α := α) (↑(n * k) : α) (↑n : α)
⊢ (↑(n * k / n) : α) = HDiv.hDiv (α := α) (↑(n * k) : α) (↑n : α)
have rw₁ : (↑k : α) = HDiv.hDiv (α := α) (↑(k * n) : α) (↑n : α)
Tactic: rw [Int.mul_ediv_cancel_left _ this, mul_comm n, Int.cast_mul, mul_div_cancel_right₀ _ hn]
-- Lean 4 proof step from Mathlib.Data.Int.Cast.Field (goal)
Goal:
α : Type u_1
inst : DivisionRing α
n : ℤ
hn : Ne.{u_1 + 1} (α := α) (↑n : α) 0
k : ℤ
this : n ≠ 0
rw : (↑k : α) = HDiv.hDiv (α := α) (↑(n * k) : α) (↑n : α)
rw₁ : (↑k : α) = HDiv.hDiv (α := α) (↑(k * n) : α) (↑n : α)
⊢ (↑(n * k / n) : α) = HDiv.hDiv (α := α) (↑(n * k) : α) (↑n : α)
have rw₂ : (↑k : α) = HMul.hMul (α := α) (↑k : α) (↑n : α) / (↑n : α)
Tactic: rw [Int.mul_ediv_cancel_left _ this, mul_comm n, Int.cast_mul, mul_div_cancel_right₀ _ hn]
-- Lean 4 proof step from Mathlib.Data.Int.Cast.Field (goal)
Goal:
α : Type u_1
inst : DivisionRing α
n : ℤ
hn : Ne.{u_1 + 1} (α := α) (↑n : α) 0
k : ℤ
this : n ≠ 0
rw : (↑k : α) = HDiv.hDiv (α := α) (↑(n * k) : α) (↑n : α)
rw₁ : (↑k : α) = HDiv.hDiv (α := α) (↑(k * n) : α) (↑n : α)
rw₂ : (↑k : α) = HMul.hMul (α := α) (↑k : α) (↑n : α) / (↑n : α)
⊢ (↑(n * k / n) : α) = HDiv.hDiv (α := α) (↑(n * k) : α) (↑n : α)
have rw₃ : Eq.{u_1 + 1} (α := α) (↑k : α) (↑k : α)
Tactic: rw [Int.mul_ediv_cancel_left _ this, mul_comm n, Int.cast_mul, mul_div_cancel_right₀ _ hn]
-- Lean 4 proof step from Mathlib.Data.Int.Cast.Lemmas (goal)
Goal:
α : Type u_3
inst : AddGroupWithOne α
inst_1 : CharZero α
n : ℤ
h : Eq.{u_3 + 1} (α := α) (↑n : α) 0
⊢ n = 0
have ofNat : ∀ (a : ℕ) (h : Eq.{u_3 + 1} (α := α) (↑(ofNat a) : α) 0), ofNat a = 0
Tactic: cases n
Cleared hypotheses: n, h
-- Lean 4 proof step from Mathlib.Data.Int.Cast.Lemmas (goal)
Goal:
α : Type u_3
inst : AddGroupWithOne α
inst_1 : CharZero α
n : ℤ
h : Eq.{u_3 + 1} (α := α) (↑n : α) 0
ofNat : ∀ (a : ℕ) (h : Eq.{u_3 + 1} (α := α) (↑(Int.ofNat a) : α) 0), Int.ofNat a = 0
⊢ n = 0
have negSucc : ∀ (a : ℕ) (h : Eq.{u_3 + 1} (α := α) (↑-[a+1] : α) 0), -[a+1] = 0
Tactic: cases n
Cleared hypotheses: n, h
-- Lean 4 proof step from Mathlib.Data.Int.Cast.Lemmas (hypothesis)
Goal:
α : Type u_3
inst : AddGroupWithOne α
inst_1 : CharZero α
a : ℕ
h : Eq.{u_3 + 1} (α := α) (↑(ofNat a) : α) 0
⊢ ofNat a = 0
have h₁ : Eq.{u_3 + 1} (α := α) (↑a : α) 0
Tactic: rw [ofNat_eq_natCast, Int.cast_natCast] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.Int.Cast.Lemmas (hypothesis)
Goal:
α : Type u_3
inst : AddGroupWithOne α
inst_1 : CharZero α
a : ℕ
h : Eq.{u_3 + 1} (α := α) (↑-[a+1] : α) 0
⊢ -[a+1] = 0
have h₁ : a + 1 = 0
Tactic: rw [cast_negSucc, neg_eq_zero, Nat.cast_eq_zero] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.Int.Cast.Lemmas (goal)
Goal:
α : Type u_3
inst : AddGroupWithOne α
inst_1 : CharZero α
n : ℤ
h : n = 0
⊢ Eq.{u_3 + 1} (α := α) (↑n : α) 0
have rw : Eq.{u_3 + 1} (α := α) (↑0 : α) 0
Tactic: rw [h, cast_zero]
-- Lean 4 proof step from Mathlib.Data.Int.Cast.Lemmas (goal)
Goal:
α : Type u_3
inst : AddGroupWithOne α
inst_1 : CharZero α
n : ℤ
h : n = 0
rw : Eq.{u_3 + 1} (α := α) (↑0 : α) 0
⊢ Eq.{u_3 + 1} (α := α) (↑n : α) 0
have rw₁ : Eq.{u_3 + 1} (α := α) 0 0
Tactic: rw [h, cast_zero]
-- Lean 4 proof step from Mathlib.Data.Int.Cast.Lemmas (goal)
Goal:
α : Type u_3
inst : AddGroupWithOne α
inst_1 : CharZero α
m n : ℤ
⊢ Eq.{u_3 + 1} (α := α) (↑m : α) (↑n : α) ↔ m = n
have rw : HSub.hSub (α := α) (↑m : α) (↑n : α) = 0 ↔ m = n
Tactic: rw [← sub_eq_zero, ← cast_sub, cast_eq_zero, sub_eq_zero]
-- Lean 4 proof step from Mathlib.Data.Int.Cast.Lemmas (goal)
Goal:
α : Type u_3
inst : AddGroupWithOne α
inst_1 : CharZero α
m n : ℤ
rw : HSub.hSub (α := α) (↑m : α) (↑n : α) = 0 ↔ m = n
⊢ Eq.{u_3 + 1} (α := α) (↑m : α) (↑n : α) ↔ m = n
have rw₁ : Eq.{u_3 + 1} (α := α) (↑(m - n) : α) 0 ↔ m = n
Tactic: rw [← sub_eq_zero, ← cast_sub, cast_eq_zero, sub_eq_zero]
-- Lean 4 proof step from Mathlib.Data.Int.Cast.Lemmas (goal)
Goal:
α : Type u_3
inst : AddGroupWithOne α
inst_1 : CharZero α
m n : ℤ
rw : HSub.hSub (α := α) (↑m : α) (↑n : α) = 0 ↔ m = n
rw₁ : Eq.{u_3 + 1} (α := α) (↑(m - n) : α) 0 ↔ m = n
⊢ Eq.{u_3 + 1} (α := α) (↑m : α) (↑n : α) ↔ m = n
have rw₂ : m - n = 0 ↔ m = n
Tactic: rw [← sub_eq_zero, ← cast_sub, cast_eq_zero, sub_eq_zero]
-- Lean 4 proof step from Mathlib.Data.Int.Cast.Lemmas (goal)
Goal:
α : Type u_3
inst : AddGroupWithOne α
inst_1 : CharZero α
m n : ℤ
rw : HSub.hSub (α := α) (↑m : α) (↑n : α) = 0 ↔ m = n
rw₁ : Eq.{u_3 + 1} (α := α) (↑(m - n) : α) 0 ↔ m = n
rw₂ : m - n = 0 ↔ m = n
⊢ Eq.{u_3 + 1} (α := α) (↑m : α) (↑n : α) ↔ m = n
have rw₃ : m = n ↔ m = n
Tactic: rw [← sub_eq_zero, ← cast_sub, cast_eq_zero, sub_eq_zero]
-- Lean 4 proof step from Mathlib.Data.Int.Cast.Lemmas (goal)
Goal:
α : Type u_3
inst : AddGroupWithOne α
inst_1 : CharZero α
n : ℤ
⊢ Eq.{u_3 + 1} (α := α) (↑n : α) 1 ↔ n = 1
have rw : Eq.{u_3 + 1} (α := α) (↑n : α) (↑1 : α) ↔ n = 1
Tactic: rw [← cast_one, cast_inj]
-- Lean 4 proof step from Mathlib.Data.Int.Cast.Lemmas (goal)
Goal:
α : Type u_3
inst : AddGroupWithOne α
inst_1 : CharZero α
n : ℤ
rw : Eq.{u_3 + 1} (α := α) (↑n : α) (↑1 : α) ↔ n = 1
⊢ Eq.{u_3 + 1} (α := α) (↑n : α) 1 ↔ n = 1
have rw₁ : n = 1 ↔ n = 1
Tactic: rw [← cast_one, cast_inj]
-- Lean 4 proof step from Mathlib.Data.Int.Cast.Lemmas (goal)
Goal:
α : Type u_3
inst : NonAssocRing α
a : α
n : ℕ
⊢ HSMul.hSMul (α := ℤ) (↑n : ℤ) a = (↑(↑n : ℤ) : α) * a
have rw : n • a = (↑(↑n : ℤ) : α) * a
Tactic: rw [natCast_zsmul, nsmul_eq_mul, Int.cast_natCast]
-- Lean 4 proof step from Mathlib.Data.Int.Cast.Lemmas (goal)
Goal:
α : Type u_3
inst : NonAssocRing α
a : α
n : ℕ
rw : n • a = (↑(↑n : ℤ) : α) * a
⊢ HSMul.hSMul (α := ℤ) (↑n : ℤ) a = (↑(↑n : ℤ) : α) * a
have rw₁ : (↑n : α) * a = (↑(↑n : ℤ) : α) * a
Tactic: rw [natCast_zsmul, nsmul_eq_mul, Int.cast_natCast]
-- Lean 4 proof step from Mathlib.Data.Int.Cast.Lemmas (goal)
Goal:
α : Type u_3
inst : NonAssocRing α
a : α
n : ℕ
rw : n • a = (↑(↑n : ℤ) : α) * a
rw₁ : (↑n : α) * a = (↑(↑n : ℤ) : α) * a
⊢ HSMul.hSMul (α := ℤ) (↑n : ℤ) a = (↑(↑n : ℤ) : α) * a
have rw₂ : (↑n : α) * a = (↑n : α) * a
Tactic: rw [natCast_zsmul, nsmul_eq_mul, Int.cast_natCast]
-- Lean 4 proof step from Mathlib.Data.Int.Cast.Lemmas (goal)
Goal:
α : Type u_3
inst : NonAssocRing α
a : α
n : ℤ
⊢ n • a = a * (↑n : α)
have rw : (↑n : α) * a = a * (↑n : α)
Tactic: rw [zsmul_eq_mul, (n.cast_commute a).eq]
-- Lean 4 proof step from Mathlib.Data.Int.Cast.Lemmas (goal)
Goal:
α : Type u_3
inst : NonAssocRing α
a : α
n : ℤ
rw : (↑n : α) * a = a * (↑n : α)
⊢ n • a = a * (↑n : α)
have rw₁ : a * (↑n : α) = a * (↑n : α)
Tactic: rw [zsmul_eq_mul, (n.cast_commute a).eq]
-- Lean 4 proof step from Mathlib.Data.Int.Cast.Lemmas (goal)
Goal:
M : Type u_5
inst : Monoid M
f g : ℤ →* M
h_neg_one : Eq (α := M) ((f : (a : ℤ) → M) (-1) : M) ((g : (a : ℤ) → M) (-1) : M)
h_nat : f.comp (↑ofNatHom : ℕ →* ℤ) = g.comp (↑ofNatHom : ℕ →* ℤ)
⊢ f = g
have h : ∀ (x : ℕ), Eq (α := M) ((f : (a : ℤ) → M) (ofNat x) : M) ((g : (a : ℤ) → M) (ofNat x) : M)
Tactic: ext (x | x)
-- Lean 4 proof step from Mathlib.Data.Int.Cast.Lemmas (goal)
Goal:
M : Type u_5
inst : Monoid M
f g : ℤ →* M
h_neg_one : Eq (α := M) ((f : (a : ℤ) → M) (-1) : M) ((g : (a : ℤ) → M) (-1) : M)
h_nat : f.comp (↑ofNatHom : ℕ →* ℤ) = g.comp (↑ofNatHom : ℕ →* ℤ)
h : ∀ (x : ℕ), Eq (α := M) ((f : (a : ℤ) → M) (ofNat x) : M) ((g : (a : ℤ) → M) (ofNat x) : M)
⊢ f = g
have h₁ : ∀ (x : ℕ), Eq (α := M) ((f : (a : ℤ) → M) -[x+1] : M) ((g : (a : ℤ) → M) -[x+1] : M)
Tactic: ext (x | x)