awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Basic (goal)
Goal:
R : Type u_3
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
a : R
inst_3 : ExistsAddOfLE R
k : ℕ
h₀ : k + k ≠ 0
rw : 0 < a ^ k * a ^ k ↔ a ≠ 0
rw₁ : a ^ k ≠ 0 ↔ a ≠ 0
⊢ 0 < a ^ (k + k) ↔ a ≠ 0
have rw₂ : a ≠ 0 ↔ a ≠ 0
Tactic: rw [pow_add, mul_self_pos, pow_ne_zero_iff (by simpa using h₀)]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Basic (goal)
Goal:
R : Type u_3
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
a : R
n : ℕ
inst_3 : ExistsAddOfLE R
hn : Odd n
⊢ a ^ n < 0 ↔ a < 0
have refine : ∀ (ha : a < 0), a ^ n < 0
Tactic: refine ⟨lt_imp_lt_of_le_imp_le (pow_nonneg · _), fun ha ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Basic (goal)
Goal:
R : Type u_3
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
a : R
n : ℕ
inst_3 : ExistsAddOfLE R
hn : Odd n
ha : a < 0
⊢ a ^ n < 0
have obtain : ∀ (k : ℕ), a ^ (2 * k + 1) < 0
Tactic: obtain ⟨k, rfl⟩ := hn
Cleared hypotheses: n, hn
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Basic (goal)
Goal:
R : Type u_3
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
a : R
inst_3 : ExistsAddOfLE R
ha : a < 0
k : ℕ
⊢ a ^ (2 * k + 1) < 0
have rw : a ^ (2 * k) * a < 0
Tactic: rw [pow_succ]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Basic (goal)
Goal:
R : Type u_3
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
a : R
n : ℕ
inst_3 : ExistsAddOfLE R
hn : Odd n
⊢ a ^ n ≤ 0 ↔ a ≤ 0
have rw : n ≠ 0
Tactic: rw [le_iff_lt_or_eq, le_iff_lt_or_eq, hn.pow_neg_iff, pow_eq_zero_iff]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Basic (hypothesis)
Goal:
R : Type u_3
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
n : ℕ
inst_3 : ExistsAddOfLE R
hn : Odd n
⊢ StrictMono (β := R) fun (a : R) ↦ a ^ n
have hn₀ : n ≠ 0
Tactic: have hn₀ : n ≠ 0 := by rintro rfl; simp [Odd] at hn
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Basic (goal)
Goal:
R : Type u_3
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
n : ℕ
inst_3 : ExistsAddOfLE R
hn : Odd n
hn₀ : n ≠ 0
a b : R
hab : a < b
⊢ LT.lt.{u_3} (α := R) ((fun (a : R) ↦ a ^ n) a) ((fun (a : R) ↦ a ^ n) b)
have inl : ∀ (ha : 0 ≤ a), LT.lt.{u_3} (α := R) ((fun (a : R) ↦ a ^ n) a) ((fun (a : R) ↦ a ^ n) b)
Tactic: obtain ha | ha := le_total 0 a
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Basic (goal)
Goal:
R : Type u_3
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
n : ℕ
inst_3 : ExistsAddOfLE R
hn : Odd n
hn₀ : n ≠ 0
a b : R
hab : a < b
inl : ∀ (ha : 0 ≤ a), LT.lt.{u_3} (α := R) ((fun (a : R) ↦ a ^ n) a) ((fun (a : R) ↦ a ^ n) b)
⊢ LT.lt.{u_3} (α := R) ((fun (a : R) ↦ a ^ n) a) ((fun (a : R) ↦ a ^ n) b)
have inr : ∀ (ha : a ≤ 0), LT.lt.{u_3} (α := R) ((fun (a : R) ↦ a ^ n) a) ((fun (a : R) ↦ a ^ n) b)
Tactic: obtain ha | ha := le_total 0 a
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Basic (goal)
Goal:
R : Type u_3
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
n : ℕ
inst_3 : ExistsAddOfLE R
hn : Odd n
hn₀ : n ≠ 0
a b : R
hab : a < b
ha : a ≤ 0
⊢ LT.lt.{u_3} (α := R) ((fun (a : R) ↦ a ^ n) a) ((fun (a : R) ↦ a ^ n) b)
have inr : ∀ (hb : 0 < b), LT.lt.{u_3} (α := R) ((fun (a : R) ↦ a ^ n) a) ((fun (a : R) ↦ a ^ n) b)
Tactic: obtain hb | hb := lt_or_ge 0 b
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Basic (goal)
Goal:
R : Type u_3
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
n : ℕ
inst_3 : ExistsAddOfLE R
hn : Odd n
hn₀ : n ≠ 0
a b : R
hab : a < b
ha : a ≤ 0
inr : ∀ (hb : 0 < b), LT.lt.{u_3} (α := R) ((fun (a : R) ↦ a ^ n) a) ((fun (a : R) ↦ a ^ n) b)
⊢ LT.lt.{u_3} (α := R) ((fun (a : R) ↦ a ^ n) a) ((fun (a : R) ↦ a ^ n) b)
have inr₁ : ∀ (hb : b ≤ 0), LT.lt.{u_3} (α := R) ((fun (a : R) ↦ a ^ n) a) ((fun (a : R) ↦ a ^ n) b)
Tactic: obtain hb | hb := lt_or_ge 0 b
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Basic (goal)
Goal:
R : Type u_3
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
n : ℕ
inst_3 : ExistsAddOfLE R
hn : Odd n
hn₀ : n ≠ 0
a b : R
hab : a < b
ha : a ≤ 0
hb : b ≤ 0
⊢ LT.lt.{u_3} (α := R) ((fun (a : R) ↦ a ^ n) a) ((fun (a : R) ↦ a ^ n) b)
have inr : ∀ (c : R) (hac : 0 = a + c), LT.lt.{u_3} (α := R) ((fun (a : R) ↦ a ^ n) a) ((fun (a : R) ↦ a ^ n) b)
Tactic: obtain ⟨c, hac⟩ := exists_add_of_le ha
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Basic (goal)
Goal:
R : Type u_3
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
n : ℕ
inst_3 : ExistsAddOfLE R
hn : Odd n
hn₀ : n ≠ 0
a b : R
hab : a < b
ha : a ≤ 0
hb : b ≤ 0
c : R
hac : 0 = a + c
⊢ LT.lt.{u_3} (α := R) ((fun (a : R) ↦ a ^ n) a) ((fun (a : R) ↦ a ^ n) b)
have inr : ∀ (d : R) (hbd : 0 = b + d), LT.lt.{u_3} (α := R) ((fun (a : R) ↦ a ^ n) a) ((fun (a : R) ↦ a ^ n) b)
Tactic: obtain ⟨d, hbd⟩ := exists_add_of_le hb
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Basic (hypothesis)
Goal:
R : Type u_3
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
n : ℕ
inst_3 : ExistsAddOfLE R
hn : Odd n
hn₀ : n ≠ 0
a b : R
hab : a < b
ha : a ≤ 0
hb : b ≤ 0
c : R
hac : 0 = a + c
d : R
hbd : 0 = b + d
⊢ LT.lt.{u_3} (α := R) ((fun (a : R) ↦ a ^ n) a) ((fun (a : R) ↦ a ^ n) b)
have hd : 0 ≤ d
Tactic: have hd := nonneg_of_le_add_right (hb.trans_eq hbd)
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Basic (goal)
Goal:
R : Type u_3
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
n : ℕ
inst_3 : ExistsAddOfLE R
hn : Odd n
hn₀ : n ≠ 0
a b : R
hab : a < b
ha : a ≤ 0
hb : b ≤ 0
c : R
hac : 0 = a + c
d : R
hbd : 0 = b + d
hd : 0 ≤ d
⊢ LT.lt.{u_3} (α := R) ((fun (a : R) ↦ a ^ n) a) ((fun (a : R) ↦ a ^ n) b)
have inr : (fun (a : R) ↦ a ^ n) a + (c ^ n + d ^ n) < (fun (a : R) ↦ a ^ n) b + (c ^ n + d ^ n)
Tactic: refine lt_of_add_lt_add_right (a := c ^ n + d ^ n) ?_
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Basic (goal)
Goal:
R : Type u_3
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
n : ℕ
inst_3 : ExistsAddOfLE R
hn : Odd n
hn₀ : n ≠ 0
a b : R
hab : a < b
ha : a ≤ 0
hb : b ≤ 0
c : R
hac : 0 = a + c
d : R
hbd : 0 = b + d
hd : 0 ≤ d
⊢ c ^ n = b ^ n + (c ^ n + d ^ n)
have rw : c ^ n = c ^ n + (b ^ n + d ^ n)
Tactic: rw [add_left_comm, hn.pow_add_pow_eq_zero hbd.symm, add_zero]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Basic (goal)
Goal:
R : Type u_3
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
n : ℕ
inst_3 : ExistsAddOfLE R
hn : Odd n
hn₀ : n ≠ 0
a b : R
hab : a < b
ha : a ≤ 0
hb : b ≤ 0
c : R
hac : 0 = a + c
d : R
hbd : 0 = b + d
hd : 0 ≤ d
rw : c ^ n = c ^ n + (b ^ n + d ^ n)
⊢ c ^ n = b ^ n + (c ^ n + d ^ n)
have rw₁ : c ^ n = c ^ n + 0
Tactic: rw [add_left_comm, hn.pow_add_pow_eq_zero hbd.symm, add_zero]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Basic (goal)
Goal:
R : Type u_3
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
n : ℕ
inst_3 : ExistsAddOfLE R
hn : Odd n
hn₀ : n ≠ 0
a b : R
hab : a < b
ha : a ≤ 0
hb : b ≤ 0
c : R
hac : 0 = a + c
d : R
hbd : 0 = b + d
hd : 0 ≤ d
rw : c ^ n = c ^ n + (b ^ n + d ^ n)
rw₁ : c ^ n = c ^ n + 0
⊢ c ^ n = b ^ n + (c ^ n + d ^ n)
have rw₂ : c ^ n = c ^ n
Tactic: rw [add_left_comm, hn.pow_add_pow_eq_zero hbd.symm, add_zero]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Basic (goal)
Goal:
R : Type u_3
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
n : ℕ
inst_3 : ExistsAddOfLE R
hn : Odd n
hn₀ : n ≠ 0
a b : R
hab : a < b
ha : a ≤ 0
hb : b ≤ 0
c : R
hac : 0 = a + c
d : R
hbd : 0 = b + d
hd : 0 ≤ d
⊢ a ^ n + (c ^ n + d ^ n) < b ^ n + (c ^ n + d ^ n)
have inr : d < c
Tactic: calc
    a ^ n + (c ^ n + d ^ n) = d ^ n := by
      rw [← add_assoc, hn.pow_add_pow_eq_zero hac.symm, zero_add]
    _ < c ^ n := pow_lt_pow_left₀ ?_ hd hn₀
    _ = b ^ n + (c ^ n + d ^ n) := by rw [add_left_comm, hn.pow_add_pow_eq_zero hbd.symm, add_zero]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Basic (goal)
Goal:
R : Type u_3
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
n : ℕ
inst_3 : ExistsAddOfLE R
hn : Odd n
hn₀ : n ≠ 0
a b : R
hab : a < b
ha : a ≤ 0
hb : b ≤ 0
c : R
hac : 0 = a + c
d : R
hbd : 0 = b + d
hd : 0 ≤ d
⊢ d < c
have inr : d + (a + b) < c + (a + b)
Tactic: refine lt_of_add_lt_add_right (a := a + b) ?_
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Basic (goal)
Goal:
R : Type u_3
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
n : ℕ
inst_3 : ExistsAddOfLE R
hn : Odd n
hn₀ : n ≠ 0
a b : R
hab : a < b
ha : a ≤ 0
hb : b ≤ 0
c : R
hac : 0 = a + c
d : R
hbd : 0 = b + d
hd : 0 ≤ d
⊢ d + (a + b) < c + (a + b)
have inr : a + (b + d) < c + (a + b)
Tactic: rwa [add_rotate', ← hbd, add_zero, add_left_comm, ← add_assoc, ← hac, zero_add]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Basic (goal)
Goal:
R : Type u_3
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
n : ℕ
inst_3 : ExistsAddOfLE R
hn : Odd n
hn₀ : n ≠ 0
a b : R
hab : a < b
ha : a ≤ 0
hb : b ≤ 0
c : R
hac : 0 = a + c
d : R
hbd : 0 = b + d
hd : 0 ≤ d
inr : a + (b + d) < c + (a + b)
⊢ d + (a + b) < c + (a + b)
have inr₁ : a + 0 < c + (a + b)
Tactic: rwa [add_rotate', ← hbd, add_zero, add_left_comm, ← add_assoc, ← hac, zero_add]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Basic (goal)
Goal:
R : Type u_3
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
n : ℕ
inst_3 : ExistsAddOfLE R
hn : Odd n
hn₀ : n ≠ 0
a b : R
hab : a < b
ha : a ≤ 0
hb : b ≤ 0
c : R
hac : 0 = a + c
d : R
hbd : 0 = b + d
hd : 0 ≤ d
inr : a + (b + d) < c + (a + b)
inr₁ : a + 0 < c + (a + b)
⊢ d + (a + b) < c + (a + b)
have inr₂ : a < c + (a + b)
Tactic: rwa [add_rotate', ← hbd, add_zero, add_left_comm, ← add_assoc, ← hac, zero_add]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Basic (goal)
Goal:
R : Type u_3
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
n : ℕ
inst_3 : ExistsAddOfLE R
hn : Odd n
hn₀ : n ≠ 0
a b : R
hab : a < b
ha : a ≤ 0
hb : b ≤ 0
c : R
hac : 0 = a + c
d : R
hbd : 0 = b + d
hd : 0 ≤ d
inr : a + (b + d) < c + (a + b)
inr₁ : a + 0 < c + (a + b)
inr₂ : a < c + (a + b)
⊢ d + (a + b) < c + (a + b)
have inr₃ : a < a + (c + b)
Tactic: rwa [add_rotate', ← hbd, add_zero, add_left_comm, ← add_assoc, ← hac, zero_add]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Basic (goal)
Goal:
R : Type u_3
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
n : ℕ
inst_3 : ExistsAddOfLE R
hn : Odd n
hn₀ : n ≠ 0
a b : R
hab : a < b
ha : a ≤ 0
hb : b ≤ 0
c : R
hac : 0 = a + c
d : R
hbd : 0 = b + d
hd : 0 ≤ d
inr : a + (b + d) < c + (a + b)
inr₁ : a + 0 < c + (a + b)
inr₂ : a < c + (a + b)
inr₃ : a < a + (c + b)
⊢ d + (a + b) < c + (a + b)
have inr₄ : a < a + c + b
Tactic: rwa [add_rotate', ← hbd, add_zero, add_left_comm, ← add_assoc, ← hac, zero_add]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Basic (goal)
Goal:
R : Type u_3
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
n : ℕ
inst_3 : ExistsAddOfLE R
hn : Odd n
hn₀ : n ≠ 0
a b : R
hab : a < b
ha : a ≤ 0
hb : b ≤ 0
c : R
hac : 0 = a + c
d : R
hbd : 0 = b + d
hd : 0 ≤ d
inr : a + (b + d) < c + (a + b)
inr₁ : a + 0 < c + (a + b)
inr₂ : a < c + (a + b)
inr₃ : a < a + (c + b)
inr₄ : a < a + c + b
⊢ d + (a + b) < c + (a + b)
have inr₅ : a < 0 + b
Tactic: rwa [add_rotate', ← hbd, add_zero, add_left_comm, ← add_assoc, ← hac, zero_add]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Cast (hypothesis)
Goal:
R : Type u_1
inst : AddCommGroupWithOne R
inst_1 : PartialOrder R
inst_2 : AddLeftMono R
inst_3 : ZeroLEOneClass R
m n : ℤ
h : m ≤ n
⊢ LE.le.{u_1} (α := R) (↑m : R) (↑n : R)
have h₁ : 0 ≤ n - m
Tactic: rw [← sub_nonneg] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Cast (goal)
Goal:
R : Type u_1
inst : AddCommGroupWithOne R
inst_1 : PartialOrder R
inst_2 : AddLeftMono R
inst_3 : ZeroLEOneClass R
m n : ℤ
h : 0 ≤ n - m
⊢ LE.le.{u_1} (α := R) (↑m : R) (↑n : R)
have lift : ∀ (k : ℕ) (hk : (↑k : ℤ) = n - m), LE.le.{u_1} (α := R) (↑m : R) (↑n : R)
Tactic: lift n - m to ℕ using h with k hk
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Cast (goal)
Goal:
R : Type u_1
inst : AddCommGroupWithOne R
inst_1 : PartialOrder R
inst_2 : AddLeftMono R
inst_3 : ZeroLEOneClass R
m n : ℤ
k : ℕ
hk : (↑k : ℤ) = n - m
⊢ LE.le.{u_1} (α := R) (↑m : R) (↑n : R)
have rw : LE.le.{u_1} (α := R) 0 (↑k : R)
Tactic: rw [← sub_nonneg, ← cast_sub, ← hk, cast_natCast]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Cast (hypothesis)
Goal:
R : Type u_1
inst : AddCommGroupWithOne R
inst_1 : PartialOrder R
inst_2 : AddLeftMono R
inst_3 : ZeroLEOneClass R
inst_4 : NeZero.{u_1} (R := R) 1
n : ℕ
⊢ LE.le.{u_1} (α := R) 0 (↑-[n+1] : R) ↔ 0 ≤ -[n+1]
have this : LT.lt.{u_1} (α := R) (-(↑n : R)) 1
Tactic: have : -(n : R) < 1 := lt_of_le_of_lt (by simp) zero_lt_one
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Cast (goal)
Goal:
R : Type u_1
inst : AddCommGroupWithOne R
inst_1 : PartialOrder R
inst_2 : AddLeftMono R
inst_3 : ZeroLEOneClass R
inst_4 : NeZero.{u_1} (R := R) 1
m n : ℤ
⊢ LE.le.{u_1} (α := R) (↑m : R) (↑n : R) ↔ m ≤ n
have rw : 0 ≤ HSub.hSub (α := R) (↑n : R) (↑m : R) ↔ m ≤ n
Tactic: rw [← sub_nonneg, ← cast_sub, cast_nonneg_iff, sub_nonneg]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Cast (goal)
Goal:
R : Type u_1
inst : AddCommGroupWithOne R
inst_1 : PartialOrder R
inst_2 : AddLeftMono R
inst_3 : ZeroLEOneClass R
inst_4 : NeZero.{u_1} (R := R) 1
m n : ℤ
rw : 0 ≤ HSub.hSub (α := R) (↑n : R) (↑m : R) ↔ m ≤ n
⊢ LE.le.{u_1} (α := R) (↑m : R) (↑n : R) ↔ m ≤ n
have rw₁ : LE.le.{u_1} (α := R) 0 (↑(n - m) : R) ↔ m ≤ n
Tactic: rw [← sub_nonneg, ← cast_sub, cast_nonneg_iff, sub_nonneg]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Cast (goal)
Goal:
R : Type u_1
inst : AddCommGroupWithOne R
inst_1 : PartialOrder R
inst_2 : AddLeftMono R
inst_3 : ZeroLEOneClass R
inst_4 : NeZero.{u_1} (R := R) 1
m n : ℤ
rw : 0 ≤ HSub.hSub (α := R) (↑n : R) (↑m : R) ↔ m ≤ n
rw₁ : LE.le.{u_1} (α := R) 0 (↑(n - m) : R) ↔ m ≤ n
⊢ LE.le.{u_1} (α := R) (↑m : R) (↑n : R) ↔ m ≤ n
have rw₂ : 0 ≤ n - m ↔ m ≤ n
Tactic: rw [← sub_nonneg, ← cast_sub, cast_nonneg_iff, sub_nonneg]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Cast (goal)
Goal:
R : Type u_1
inst : AddCommGroupWithOne R
inst_1 : PartialOrder R
inst_2 : AddLeftMono R
inst_3 : ZeroLEOneClass R
inst_4 : NeZero.{u_1} (R := R) 1
m n : ℤ
rw : 0 ≤ HSub.hSub (α := R) (↑n : R) (↑m : R) ↔ m ≤ n
rw₁ : LE.le.{u_1} (α := R) 0 (↑(n - m) : R) ↔ m ≤ n
rw₂ : 0 ≤ n - m ↔ m ≤ n
⊢ LE.le.{u_1} (α := R) (↑m : R) (↑n : R) ↔ m ≤ n
have rw₃ : m ≤ n ↔ m ≤ n
Tactic: rw [← sub_nonneg, ← cast_sub, cast_nonneg_iff, sub_nonneg]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Cast (goal)
Goal:
R : Type u_1
inst : AddCommGroupWithOne R
inst_1 : PartialOrder R
inst_2 : AddLeftMono R
inst_3 : ZeroLEOneClass R
inst_4 : NeZero.{u_1} (R := R) 1
n : ℤ
⊢ LE.le.{u_1} (α := R) (↑n : R) 0 ↔ n ≤ 0
have rw : LE.le.{u_1} (α := R) (↑n : R) (↑0 : R) ↔ n ≤ 0
Tactic: rw [← cast_zero, cast_le]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Cast (goal)
Goal:
R : Type u_1
inst : AddCommGroupWithOne R
inst_1 : PartialOrder R
inst_2 : AddLeftMono R
inst_3 : ZeroLEOneClass R
inst_4 : NeZero.{u_1} (R := R) 1
n : ℤ
rw : LE.le.{u_1} (α := R) (↑n : R) (↑0 : R) ↔ n ≤ 0
⊢ LE.le.{u_1} (α := R) (↑n : R) 0 ↔ n ≤ 0
have rw₁ : n ≤ 0 ↔ n ≤ 0
Tactic: rw [← cast_zero, cast_le]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Cast (goal)
Goal:
R : Type u_1
inst : AddCommGroupWithOne R
inst_1 : PartialOrder R
inst_2 : AddLeftMono R
inst_3 : ZeroLEOneClass R
inst_4 : NeZero.{u_1} (R := R) 1
n : ℤ
⊢ LT.lt.{u_1} (α := R) 0 (↑n : R) ↔ 0 < n
have rw : LT.lt.{u_1} (α := R) (↑0 : R) (↑n : R) ↔ 0 < n
Tactic: rw [← cast_zero, cast_lt]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Cast (goal)
Goal:
R : Type u_1
inst : AddCommGroupWithOne R
inst_1 : PartialOrder R
inst_2 : AddLeftMono R
inst_3 : ZeroLEOneClass R
inst_4 : NeZero.{u_1} (R := R) 1
n : ℤ
rw : LT.lt.{u_1} (α := R) (↑0 : R) (↑n : R) ↔ 0 < n
⊢ LT.lt.{u_1} (α := R) 0 (↑n : R) ↔ 0 < n
have rw₁ : 0 < n ↔ 0 < n
Tactic: rw [← cast_zero, cast_lt]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Cast (goal)
Goal:
R : Type u_1
inst : AddCommGroupWithOne R
inst_1 : PartialOrder R
inst_2 : AddLeftMono R
inst_3 : ZeroLEOneClass R
inst_4 : NeZero.{u_1} (R := R) 1
n : ℤ
⊢ LT.lt.{u_1} (α := R) (↑n : R) 0 ↔ n < 0
have rw : LT.lt.{u_1} (α := R) (↑n : R) (↑0 : R) ↔ n < 0
Tactic: rw [← cast_zero, cast_lt]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Cast (goal)
Goal:
R : Type u_1
inst : AddCommGroupWithOne R
inst_1 : PartialOrder R
inst_2 : AddLeftMono R
inst_3 : ZeroLEOneClass R
inst_4 : NeZero.{u_1} (R := R) 1
n : ℤ
rw : LT.lt.{u_1} (α := R) (↑n : R) (↑0 : R) ↔ n < 0
⊢ LT.lt.{u_1} (α := R) (↑n : R) 0 ↔ n < 0
have rw₁ : n < 0 ↔ n < 0
Tactic: rw [← cast_zero, cast_lt]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Cast (goal)
Goal:
R : Type u_1
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
a : ℤ
h : a < 0
⊢ LE.le.{u_1} (α := R) (↑a : R) (-1)
have rw : a ≤ -1
Tactic: rw [← Int.cast_one, ← Int.cast_neg, cast_le]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Cast (hypothesis)
Goal:
R : Type u_1
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
x : R
n : ℤ
hx : |x| ≤ 1
hn : 0 < n
⊢ 0 ≤ x + (↑n : R)
have this : HAdd.hAdd (α := R) (-1) 1 ≤ x + (↑n : R)
Tactic: have := _root_.add_le_add (neg_le_of_abs_le hx) (cast_one_le_of_pos hn)
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Cast (goal)
Goal:
R : Type u_1
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
x : R
n : ℤ
hx : |x| ≤ 1
hn : 0 < n
this : HAdd.hAdd (α := R) (-1) 1 ≤ x + (↑n : R)
⊢ 0 ≤ x + (↑n : R)
have rwa : ∀ (this : 0 ≤ x + (↑n : R)), 0 ≤ x + (↑n : R)
Tactic: rwa [neg_add_cancel] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Cast (hypothesis)
Goal:
R : Type u_1
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
x : R
n : ℤ
hx : |x| ≤ 1
⊢ 0 ≤ (↑n : R) * x + HMul.hMul (α := R) (↑n : R) (↑n : R)
have hnx : 0 < n → 0 ≤ x + (↑n : R)
Tactic: have hnx : 0 < n → 0 ≤ x + n := fun hn => by
    have := _root_.add_le_add (neg_le_of_abs_le hx) (cast_one_le_of_pos hn)
    rwa [neg_add_cancel] at this
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Cast (hypothesis)
Goal:
R : Type u_1
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
x : R
n : ℤ
hx : |x| ≤ 1
hnx : 0 < n → 0 ≤ x + (↑n : R)
hn : n < 0
⊢ x + (↑n : R) ≤ 0
have this : x + (↑n : R) ≤ HAdd.hAdd (α := R) 1 (-1)
Tactic: have := _root_.add_le_add (le_of_abs_le hx) (cast_le_neg_one_of_neg hn)
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Cast (goal)
Goal:
R : Type u_1
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
x : R
n : ℤ
hx : |x| ≤ 1
hnx : 0 < n → 0 ≤ x + (↑n : R)
hn : n < 0
this : x + (↑n : R) ≤ HAdd.hAdd (α := R) 1 (-1)
⊢ x + (↑n : R) ≤ 0
have rwa : ∀ (this : x + (↑n : R) ≤ 0), x + (↑n : R) ≤ 0
Tactic: rwa [add_neg_cancel] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Cast (hypothesis)
Goal:
R : Type u_1
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
x : R
n : ℤ
hx : |x| ≤ 1
hnx : 0 < n → 0 ≤ x + (↑n : R)
⊢ 0 ≤ (↑n : R) * x + HMul.hMul (α := R) (↑n : R) (↑n : R)
have hnx' : n < 0 → x + (↑n : R) ≤ 0
Tactic: have hnx' : n < 0 → x + n ≤ 0 := fun hn => by
    have := _root_.add_le_add (le_of_abs_le hx) (cast_le_neg_one_of_neg hn)
    rwa [add_neg_cancel] at this
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Cast (goal)
Goal:
R : Type u_1
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
x : R
n : ℤ
hx : |x| ≤ 1
hnx : 0 < n → 0 ≤ x + (↑n : R)
hnx' : n < 0 → x + (↑n : R) ≤ 0
⊢ 0 ≤ (↑n : R) * x + HMul.hMul (α := R) (↑n : R) (↑n : R)
have rw : LE.le.{u_1} (α := R) 0 (↑n : R) ∧ 0 ≤ x + (↑n : R) ∨ LE.le.{u_1} (α := R) (↑n : R) 0 ∧ x + (↑n : R) ≤ 0
Tactic: rw [← mul_add, mul_nonneg_iff]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Cast (goal)
Goal:
R : Type u_1
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
x : R
n : ℤ
hx : |x| ≤ 1
hnx : 0 < n → 0 ≤ x + (↑n : R)
hnx' : n < 0 → x + (↑n : R) ≤ 0
⊢ LE.le.{u_1} (α := R) 0 (↑n : R) ∧ 0 ≤ x + (↑n : R) ∨ LE.le.{u_1} (α := R) (↑n : R) 0 ∧ x + (↑n : R) ≤ 0
have inl : ∀ (h : n < 0), LE.le.{u_1} (α := R) 0 (↑n : R) ∧ 0 ≤ x + (↑n : R) ∨ LE.le.{u_1} (α := R) (↑n : R) 0 ∧ x + (↑n : R) ≤ 0
Tactic: rcases lt_trichotomy n 0 with (h | rfl | h)
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Cast (goal)
Goal:
R : Type u_1
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
x : R
n : ℤ
hx : |x| ≤ 1
hnx : 0 < n → 0 ≤ x + (↑n : R)
hnx' : n < 0 → x + (↑n : R) ≤ 0
inl :
  ∀ (h : n < 0), LE.le.{u_1} (α := R) 0 (↑n : R) ∧ 0 ≤ x + (↑n : R) ∨ LE.le.{u_1} (α := R) (↑n : R) 0 ∧ x + (↑n : R) ≤ 0
⊢ LE.le.{u_1} (α := R) 0 (↑n : R) ∧ 0 ≤ x + (↑n : R) ∨ LE.le.{u_1} (α := R) (↑n : R) 0 ∧ x + (↑n : R) ≤ 0
have inr : ∀ (hnx : LT.lt (α := ℤ) 0 0 → 0 ≤ x + (↑0 : R)) (hnx' : LT.lt (α := ℤ) 0 0 → x + (↑0 : R) ≤ 0),
  LE.le.{u_1} (α := R) 0 (↑0 : R) ∧ 0 ≤ x + (↑0 : R) ∨ LE.le.{u_1} (α := R) (↑0 : R) 0 ∧ x + (↑0 : R) ≤ 0
Tactic: rcases lt_trichotomy n 0 with (h | rfl | h)
Cleared hypotheses: n, hnx, hnx'
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Cast (goal)
Goal:
R : Type u_1
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
x : R
n : ℤ
hx : |x| ≤ 1
hnx : 0 < n → 0 ≤ x + (↑n : R)
hnx' : n < 0 → x + (↑n : R) ≤ 0
inl :
  ∀ (h : n < 0), LE.le.{u_1} (α := R) 0 (↑n : R) ∧ 0 ≤ x + (↑n : R) ∨ LE.le.{u_1} (α := R) (↑n : R) 0 ∧ x + (↑n : R) ≤ 0
inr :
  ∀ (hnx : LT.lt (α := ℤ) 0 0 → 0 ≤ x + (↑0 : R)) (hnx' : LT.lt (α := ℤ) 0 0 → x + (↑0 : R) ≤ 0),
    LE.le.{u_1} (α := R) 0 (↑0 : R) ∧ 0 ≤ x + (↑0 : R) ∨ LE.le.{u_1} (α := R) (↑0 : R) 0 ∧ x + (↑0 : R) ≤ 0
⊢ LE.le.{u_1} (α := R) 0 (↑n : R) ∧ 0 ≤ x + (↑n : R) ∨ LE.le.{u_1} (α := R) (↑n : R) 0 ∧ x + (↑n : R) ≤ 0
have inr₁ : ∀ (h : 0 < n), LE.le.{u_1} (α := R) 0 (↑n : R) ∧ 0 ≤ x + (↑n : R) ∨ LE.le.{u_1} (α := R) (↑n : R) 0 ∧ x + (↑n : R) ≤ 0
Tactic: rcases lt_trichotomy n 0 with (h | rfl | h)
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Cone (goal)
Goal:
R : Type u_1
inst : Ring R
p q : RingCone R
h : Eq.{u_1 + 1} (α := Set R) ((fun (C : RingCone R) ↦ C.carrier) p) ((fun (C : RingCone R) ↦ C.carrier) q)
⊢ p = q
have mk : ∀ (toSubsemiring : Subsemiring R)
  (eq_zero_of_mem_of_neg_mem' : ∀ {a : R}, a ∈ toSubsemiring.carrier → -a ∈ toSubsemiring.carrier → a = 0)
  (h :
    Eq.{u_1 + 1} (α := Set R)
      ((fun (C : RingCone R) ↦ C.carrier)
        { toSubsemiring := toSubsemiring, eq_zero_of_mem_of_neg_mem' := @eq_zero_of_mem_of_neg_mem' })
      ((fun (C : RingCone R) ↦ C.carrier) q)),
  { toSubsemiring := toSubsemiring, eq_zero_of_mem_of_neg_mem' := @eq_zero_of_mem_of_neg_mem' : RingCone R } = q
Tactic: cases p
Cleared hypotheses: p, h