awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Order.Ring.Basic
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 ^ n + (c ^ n + d ^ n) < b ^ n + (c ^ n + d ^ n)
⊢ (fun (a : R) ↦ a ^ n) a + (c ^ n + d ^ n) < (fun (a : R) ↦ a ^ n) b + (c ^ n + d ^ n)

Tactic:
dsimp
-- Module: Mathlib.Algebra.Order.Ring.Basic
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 ^ n < c ^ n

Tactic:
pow_lt_pow_left₀ ?_ hd hn₀

Premises used: pow_lt_pow_left₀
-- Module: Mathlib.Algebra.Order.Ring.Basic
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
rw₂ rw₃ : c ^ n = c ^ n
⊢ c ^ n = b ^ n + (c ^ n + d ^ n)

Tactic:
rw [add_left_comm, hn.pow_add_pow_eq_zero hbd.symm, add_zero]

Premises used: add_left_comm, add_zero, Eq.symm, Odd.pow_add_pow_eq_zero
-- Module: Mathlib.Algebra.Order.Ring.Basic
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 : d < c
⊢ a ^ n + (c ^ n + d ^ n) < b ^ n + (c ^ n + d ^ n)

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]

Premises used: HPow.hPow, HAdd.hAdd, pow_lt_pow_left₀
-- Module: Mathlib.Algebra.Order.Ring.Basic
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

Tactic:
lt_of_add_lt_add_right (a := a + b) ?_

Premises used: lt_of_add_lt_add_right
-- Module: Mathlib.Algebra.Order.Ring.Basic
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 : d + (a + b) < c + (a + b)
⊢ d < c

Tactic:
refine lt_of_add_lt_add_right (a := a + b) ?_

Premises used: lt_of_add_lt_add_right
-- Module: Mathlib.Algebra.Order.Ring.Basic
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
inr₅ : a < 0 + b
inr₆ inr₇ inr₈ inr₉ : a < b
⊢ d + (a + b) < c + (a + b)

Tactic:
rwa [add_rotate', ← hbd, add_zero, add_left_comm, ← add_assoc, ← hac, zero_add]

Premises used: add_left_comm, add_assoc, zero_add, add_rotate', add_zero
-- Module: Mathlib.Algebra.Order.Ring.Basic
Goal:
R : Type u_3
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : ExistsAddOfLE R
n : ℕ
hn : Odd n
⊢ Injective (β := R) fun (x : R) ↦ x ^ n

Tactic:
hn.strictMono_pow.injective

Premises used: Odd.strictMono_pow, StrictMono.injective
-- Module: Mathlib.Algebra.Order.Ring.Basic
Goal:
R : Type u_3
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : ExistsAddOfLE R
n : ℕ
hn : Odd n
a b : R
⊢ a ^ n < b ^ n ↔ a < b

Tactic:
hn.strictMono_pow.lt_iff_lt

Premises used: StrictMono.lt_iff_lt, Odd.strictMono_pow
-- Module: Mathlib.Algebra.Order.Ring.Basic
Goal:
R : Type u_3
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : ExistsAddOfLE R
n : ℕ
hn : Odd n
a b : R
⊢ a ^ n ≤ b ^ n ↔ a ≤ b

Tactic:
hn.strictMono_pow.le_iff_le

Premises used: Odd.strictMono_pow, StrictMono.le_iff_le
-- Module: Mathlib.Algebra.Order.Ring.Basic
Goal:
R : Type u_3
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : ExistsAddOfLE R
n : ℕ
hn : Odd n
a b : R
⊢ a ^ n = b ^ n ↔ a = b

Tactic:
hn.pow_injective.eq_iff

Premises used: Function.Injective.eq_iff, Odd.pow_injective
-- Module: Mathlib.Algebra.Order.Ring.Basic
Goal:
R : Type u_3
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : ExistsAddOfLE R
a : R
⊢ 0 < HPow.hPow (β := ℕ) a 2 ↔ a ≠ 0

Tactic:
even_two.pow_pos_iff two_ne_zero

Premises used: even_two, two_ne_zero, Even.pow_pos_iff
-- Module: Mathlib.Algebra.Order.Ring.Cast
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
⊢ 0 ≤ n - m

Tactic:
rw [← sub_nonneg] at h

Premises used: sub_nonneg
-- Module: Mathlib.Algebra.Order.Ring.Cast
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
⊢ 0 ≤ n - m

Tactic:
h
-- Module: Mathlib.Algebra.Order.Ring.Cast
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
lift : ∀ (k : ℕ) (hk : (↑k : ℤ) = n - m), LE.le.{u_1} (α := R) (↑m : R) (↑n : R)
⊢ LE.le.{u_1} (α := R) (↑m : R) (↑n : R)

Tactic:
lift n - m to ℕ using h with k hk
-- Module: Mathlib.Algebra.Order.Ring.Cast
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
rw : LE.le.{u_1} (α := R) 0 (↑k : R)
⊢ LE.le.{u_1} (α := R) (↑m : R) (↑n : R)

Tactic:
rw [← sub_nonneg, ← cast_sub, ← hk, cast_natCast]

Premises used: Int.cast_natCast, Int.cast_sub, sub_nonneg
-- Module: Mathlib.Algebra.Order.Ring.Cast
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) 0 (↑k : R)

Tactic:
k.cast_nonneg'

Premises used: Nat.cast_nonneg'
-- Module: Mathlib.Algebra.Order.Ring.Cast
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) 0 (↑k : R)

Tactic:
exact k.cast_nonneg'

Premises used: Nat.cast_nonneg'
-- Module: Mathlib.Algebra.Order.Ring.Cast
Goal:
R : Type u_1
inst : AddCommGroupWithOne R
inst_1 : PartialOrder R
inst_2 : AddLeftMono R
inst_3 : ZeroLEOneClass R
n : ℕ
h : LE.le (α := ℤ) 0 (↑n : ℤ)
⊢ LE.le.{u_1} (α := R) 0 (↑(↑n : ℤ) : R)

Tactic:
simp
-- Module: Mathlib.Algebra.Order.Ring.Cast
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 : ℤ) : R) ↔ LE.le (α := ℤ) 0 (↑n : ℤ)

Tactic:
simp
-- Module: Mathlib.Algebra.Order.Ring.Cast
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

Tactic:
simp
-- Module: Mathlib.Algebra.Order.Ring.Cast
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)) 1

Tactic:
have : -(n : R) < 1 := lt_of_le_of_lt (by simp) zero_lt_one
-- Module: Mathlib.Algebra.Order.Ring.Cast
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 : ℕ
this : LT.lt.{u_1} (α := R) (-(↑n : R)) 1
⊢ LE.le.{u_1} (α := R) 0 (↑-[n+1] : R) ↔ 0 ≤ -[n+1]

Tactic:
simpa [(negSucc_lt_zero n).not_ge, ← sub_eq_add_neg, le_neg] using this.not_ge

Premises used: sub_eq_add_neg, le_neg, Int.negSucc_lt_zero, LT.lt.not_ge
-- Module: Mathlib.Algebra.Order.Ring.Cast
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
rw₃ rw₄ : m ≤ n ↔ m ≤ n
⊢ LE.le.{u_1} (α := R) (↑m : R) (↑n : R) ↔ m ≤ n

Tactic:
rw [← sub_nonneg, ← cast_sub, cast_nonneg_iff, sub_nonneg]

Premises used: Int.cast_sub, Int.cast_nonneg_iff, sub_nonneg
-- Module: Mathlib.Algebra.Order.Ring.Cast
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
⊢ StrictMono.{0, u_1} (β := R) fun (x : ℤ) ↦ (↑x : R)

Tactic:
strictMono_of_le_iff_le fun _ _ => cast_le.symm

Premises used: Int.cast_le, strictMono_of_le_iff_le, Iff.symm
-- Module: Mathlib.Algebra.Order.Ring.Cast
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 : ℤ
⊢ LT.lt.{u_1} (α := R) (↑m : R) (↑n : R) ↔ m < n

Tactic:
cast_strictMono.lt_iff_lt

Premises used: StrictMono.lt_iff_lt, Int.cast_strictMono
-- Module: Mathlib.Algebra.Order.Ring.Cast
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
rw₁ rw₂ : n ≤ 0 ↔ n ≤ 0
⊢ LE.le.{u_1} (α := R) (↑n : R) 0 ↔ n ≤ 0

Tactic:
rw [← cast_zero, cast_le]

Premises used: Int.cast_le, Int.cast_zero
-- Module: Mathlib.Algebra.Order.Ring.Cast
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
rw₁ rw₂ : 0 < n ↔ 0 < n
⊢ LT.lt.{u_1} (α := R) 0 (↑n : R) ↔ 0 < n

Tactic:
rw [← cast_zero, cast_lt]

Premises used: Int.cast_zero, Int.cast_lt
-- Module: Mathlib.Algebra.Order.Ring.Cast
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
rw₁ rw₂ : n < 0 ↔ n < 0
⊢ LT.lt.{u_1} (α := R) (↑n : R) 0 ↔ n < 0

Tactic:
rw [← cast_zero, cast_lt]

Premises used: Int.cast_zero, Int.cast_lt
-- Module: Mathlib.Algebra.Order.Ring.Cast
Goal:
R : Type u_1
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
a b : ℤ
⊢ Eq.{u_1 + 1} (α := R) (↑(min a b) : R) (min (↑a : R) (↑b : R))

Tactic:
Monotone.map_min cast_mono

Premises used: Monotone.map_min, Int.cast_mono
-- Module: Mathlib.Algebra.Order.Ring.Cast
Goal:
R : Type u_1
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
a b : ℤ
⊢ Eq.{u_1 + 1} (α := R) (↑(max a b) : R) (max (↑a : R) (↑b : R))

Tactic:
Monotone.map_max cast_mono

Premises used: Monotone.map_max, Int.cast_mono
-- Module: Mathlib.Algebra.Order.Ring.Cast
Goal:
R : Type u_1
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
a : ℤ
⊢ Eq.{u_1 + 1} (α := R) (↑|a| : R) |(↑a : R)|

Tactic:
simp [abs_eq_max_neg]

Premises used: abs_eq_max_neg
-- Module: Mathlib.Algebra.Order.Ring.Cast
Goal:
R : Type u_1
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
a : ℤ
h : 0 < a
⊢ LE.le.{u_1} (α := R) 1 (↑a : R)

Tactic:
mod_cast Int.add_one_le_of_lt h

Premises used: Int.cast, congrArg, Nat.cast_add._simp_1, Int.add_one_le_of_lt, cast, LE.le, Int.cast_le._simp_1, HAdd.hAdd, congr, congrFun', Nat.cast_zero, OfNat.ofNat, Eq.symm, Nat.cast_one, Int.cast_one, Eq.trans
-- Module: Mathlib.Algebra.Order.Ring.Cast
Goal:
R : Type u_1
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
a : ℤ
h : a < 0
rw : a ≤ -1
⊢ LE.le.{u_1} (α := R) (↑a : R) (-1)

Tactic:
rw [← Int.cast_one, ← Int.cast_neg, cast_le]

Premises used: Int.cast_neg, Int.cast_le, Int.cast_one
-- Module: Mathlib.Algebra.Order.Ring.Cast
Goal:
R : Type u_1
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
a : ℤ
h : a < 0
⊢ a ≤ -1

Tactic:
Int.le_sub_one_of_lt h

Premises used: Int.le_sub_one_of_lt, Int.sub, Int.subNatNat, Int.add, Int.neg, Int.negOfNat
-- Module: Mathlib.Algebra.Order.Ring.Cast
Goal:
R : Type u_1
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
a : ℤ
h : a < 0
⊢ a ≤ -1

Tactic:
exact Int.le_sub_one_of_lt h

Premises used: Int.le_sub_one_of_lt
-- Module: Mathlib.Algebra.Order.Ring.Cast
Goal:
R : Type u_1
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
n : ℤ
hn : n ≠ 0
⊢ LE.le.{u_1} (α := R) (↑n : R) (-1) ∨ LE.le.{u_1} (α := R) 1 (↑n : R)

Tactic:
hn.lt_or_gt.imp cast_le_neg_one_of_neg cast_one_le_of_pos

Premises used: Int.cast_one_le_of_pos, Int.cast_le_neg_one_of_neg, Or.imp, Ne.lt_or_gt
-- Module: Mathlib.Algebra.Order.Ring.Cast
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
⊢ 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)
-- Module: Mathlib.Algebra.Order.Ring.Cast
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)
rwa rwa₁ rwa₂ rwa₃ : ∀ (this : 0 ≤ x + (↑n : R)), 0 ≤ x + (↑n : R)
⊢ 0 ≤ x + (↑n : R)

Tactic:
rwa [neg_add_cancel] at this

Premises used: neg_add_cancel
-- Module: Mathlib.Algebra.Order.Ring.Cast
Goal:
R : Type u_1
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
x : R
n : ℤ
hx : |x| ≤ 1
⊢ 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
-- Module: Mathlib.Algebra.Order.Ring.Cast
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) ≤ HAdd.hAdd (α := R) 1 (-1)

Tactic:
have := _root_.add_le_add (le_of_abs_le hx) (cast_le_neg_one_of_neg hn)
-- Module: Mathlib.Algebra.Order.Ring.Cast
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)
rwa rwa₁ rwa₂ rwa₃ : ∀ (this : x + (↑n : R) ≤ 0), x + (↑n : R) ≤ 0
⊢ x + (↑n : R) ≤ 0

Tactic:
rwa [add_neg_cancel] at this

Premises used: add_neg_cancel
-- Module: Mathlib.Algebra.Order.Ring.Cast
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)
⊢ 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
-- Module: Mathlib.Algebra.Order.Ring.Cast
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
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
⊢ 0 ≤ (↑n : R) * x + HMul.hMul (α := R) (↑n : R) (↑n : R)

Tactic:
rw [← mul_add, mul_nonneg_iff]

Premises used: mul_nonneg_iff, mul_add
-- Module: Mathlib.Algebra.Order.Ring.Cast
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
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
⊢ 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)

Premises used: OfNat.ofNat, rfl, lt_trichotomy
-- Module: Mathlib.Algebra.Order.Ring.Cast
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
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:
Or.inr ⟨mod_cast h.le, hnx' h⟩

Premises used: Int.cast, congrArg, Int.cast_zero, cast, LT.lt.le, LE.le, Int.cast_le._simp_1, And.intro, Nat.cast_zero, Eq.symm, Or.inr, Eq.trans
-- Module: Mathlib.Algebra.Order.Ring.Cast
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
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:
exact Or.inr ⟨mod_cast h.le, hnx' h⟩

Premises used: Or.inr
-- Module: Mathlib.Algebra.Order.Ring.Cast
Goal:
R : Type u_1
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
x : R
hx : |x| ≤ 1
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:
simp [le_total 0 x]

Premises used: le_total, OfNat.ofNat
-- Module: Mathlib.Algebra.Order.Ring.Cast
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
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:
Or.inl ⟨mod_cast h.le, hnx h⟩

Premises used: Int.cast, congrArg, Int.cast_zero, cast, LT.lt.le, LE.le, Int.cast_le._simp_1, And.intro, congrFun', Or.inl, Nat.cast_zero, Eq.symm, Eq.trans
-- Module: Mathlib.Algebra.Order.Ring.Cast
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
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:
exact Or.inl ⟨mod_cast h.le, hnx h⟩

Premises used: Or.inl
-- Module: Mathlib.Algebra.Order.Ring.Cast
Goal:
R : Type u_1
inst : IntCast R
n : ℤ
⊢ Eq.{u_1 + 1} (α := Lex R) ((toLex : (a : R) → Lex R) (↑n : R) : Lex R) ((↑n : Lex R) : Lex R)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Order.Ring.Cast
Goal:
R : Type u_1
inst : IntCast R
n : ℤ
⊢ Eq.{u_1 + 1} (α := R) ((ofLex : (a : Lex R) → R) (↑n : Lex R) : R) ((↑n : R) : R)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Order.Ring.Cone
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)
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
⊢ p = q

Tactic:
cases p
-- Module: Mathlib.Algebra.Order.Ring.Cone
Goal:
R : Type u_1
inst : Ring R
q : RingCone R
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)
mk :
  ∀ (toSubsemiring_1 : Subsemiring R)
    (eq_zero_of_mem_of_neg_mem'_1 : ∀ {a : R}, a ∈ toSubsemiring_1.carrier → -a ∈ toSubsemiring_1.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)
          { toSubsemiring := toSubsemiring_1, eq_zero_of_mem_of_neg_mem' := @eq_zero_of_mem_of_neg_mem'_1 })),
    { toSubsemiring := toSubsemiring, eq_zero_of_mem_of_neg_mem' := @eq_zero_of_mem_of_neg_mem' : RingCone R } =
      { toSubsemiring := toSubsemiring_1, eq_zero_of_mem_of_neg_mem' := @eq_zero_of_mem_of_neg_mem'_1 }
⊢ { toSubsemiring := toSubsemiring, eq_zero_of_mem_of_neg_mem' := @eq_zero_of_mem_of_neg_mem' : RingCone R } = q

Tactic:
cases q
-- Module: Mathlib.Algebra.Order.Ring.Cone
Goal:
R : Type u_1
inst : Ring R
toSubsemiring : Subsemiring R
eq_zero_of_mem_of_neg_mem' : ∀ {a : R}, a ∈ toSubsemiring.carrier → -a ∈ toSubsemiring.carrier → a = 0
toSubsemiring_1 : Subsemiring R
eq_zero_of_mem_of_neg_mem'_1 : ∀ {a : R}, a ∈ toSubsemiring_1.carrier → -a ∈ toSubsemiring_1.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)
      { toSubsemiring := toSubsemiring_1, eq_zero_of_mem_of_neg_mem' := @eq_zero_of_mem_of_neg_mem'_1 })
mk : toSubsemiring = toSubsemiring_1
⊢ { toSubsemiring := toSubsemiring, eq_zero_of_mem_of_neg_mem' := @eq_zero_of_mem_of_neg_mem' : RingCone R } =
    { toSubsemiring := toSubsemiring_1, eq_zero_of_mem_of_neg_mem' := @eq_zero_of_mem_of_neg_mem'_1 }

Tactic:
congr
-- Module: Mathlib.Algebra.Order.Ring.Cone
Goal:
R : Type u_1
inst : Ring R
toSubsemiring : Subsemiring R
eq_zero_of_mem_of_neg_mem' : ∀ {a : R}, a ∈ toSubsemiring.carrier → -a ∈ toSubsemiring.carrier → a = 0
toSubsemiring_1 : Subsemiring R
eq_zero_of_mem_of_neg_mem'_1 : ∀ {a : R}, a ∈ toSubsemiring_1.carrier → -a ∈ toSubsemiring_1.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)
      { toSubsemiring := toSubsemiring_1, eq_zero_of_mem_of_neg_mem' := @eq_zero_of_mem_of_neg_mem'_1 })
⊢ toSubsemiring = toSubsemiring_1

Tactic:
SetLike.ext' h

Premises used: SetLike.ext'
-- Module: Mathlib.Algebra.Order.Ring.Cone
Goal:
R : Type u_1
inst : Ring R
toSubsemiring : Subsemiring R
eq_zero_of_mem_of_neg_mem' : ∀ {a : R}, a ∈ toSubsemiring.carrier → -a ∈ toSubsemiring.carrier → a = 0
toSubsemiring_1 : Subsemiring R
eq_zero_of_mem_of_neg_mem'_1 : ∀ {a : R}, a ∈ toSubsemiring_1.carrier → -a ∈ toSubsemiring_1.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)
      { toSubsemiring := toSubsemiring_1, eq_zero_of_mem_of_neg_mem' := @eq_zero_of_mem_of_neg_mem'_1 })
⊢ toSubsemiring = toSubsemiring_1

Tactic:
exact SetLike.ext' h

Premises used: SetLike.ext'
-- Module: Mathlib.Algebra.Order.Ring.Cone
Goal:
R : Type u_1
inst : Ring R
toSubsemiring : Subsemiring R
eq_zero_of_mem_of_neg_mem : ∀ {a : R}, a ∈ toSubsemiring.carrier → -a ∈ toSubsemiring.carrier → a = 0
x : R
⊢ x ∈ { toSubsemiring := toSubsemiring, eq_zero_of_mem_of_neg_mem' := @eq_zero_of_mem_of_neg_mem : RingCone R } ↔
    x ∈ toSubsemiring

Tactic:
.rfl

Premises used: Set.Mem, Iff.rfl