awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Nat.Cast.Field
Goal:
K : Type u_1
inst : DivisionSemiring K
n : ℕ
hn : Ne.{u_1 + 1} (α := K) (↑n : K) 0
k : ℕ
⊢ n ≠ 0

Tactic:
have : n ≠ 0 := by rintro rfl; simp at hn
-- Module: Mathlib.Data.Nat.Cast.Field
Goal:
K : Type u_1
inst : DivisionSemiring K
n : ℕ
hn : Ne.{u_1 + 1} (α := K) (↑n : K) 0
k : ℕ
this : n ≠ 0
rw : (↑k : K) = HDiv.hDiv (α := K) (↑(n * k) : K) (↑n : K)
rw₁ : (↑k : K) = HDiv.hDiv (α := K) (↑(k * n) : K) (↑n : K)
rw₂ : (↑k : K) = HMul.hMul (α := K) (↑k : K) (↑n : K) / (↑n : K)
rw₃ rw₄ : Eq.{u_1 + 1} (α := K) (↑k : K) (↑k : K)
⊢ (↑(n * k / n) : K) = HDiv.hDiv (α := K) (↑(n * k) : K) (↑n : K)

Tactic:
rw [Nat.mul_div_cancel_left _ <| zero_lt_of_ne_zero this, mul_comm n,
    cast_mul, mul_div_cancel_right₀ _ hn]

Premises used: Nat.mul_div_cancel_left, Nat.zero_lt_of_ne_zero, mul_div_cancel_right₀, Nat.cast_mul, mul_comm
-- Module: Mathlib.Data.Nat.Cast.Field
Goal:
K : Type u_1
inst : DivisionSemiring K
m n : ℕ
inst_1 : CharZero K
hnm : n ∣ m
inl : ∀ (hnm : 0 ∣ m), (↑(m / 0) : K) = HDiv.hDiv (α := K) (↑m : K) (↑0 : K)
inr : ∀ (hn : n ≠ 0), (↑(m / n) : K) = HDiv.hDiv (α := K) (↑m : K) (↑n : K)
⊢ (↑(m / n) : K) = HDiv.hDiv (α := K) (↑m : K) (↑n : K)

Tactic:
obtain rfl | hn := eq_or_ne n 0

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Data.Nat.Cast.Field
Goal:
K : Type u_1
inst : DivisionSemiring K
m : ℕ
inst_1 : CharZero K
hnm : 0 ∣ m
⊢ (↑(m / 0) : K) = HDiv.hDiv (α := K) (↑m : K) (↑0 : K)

Tactic:
simp [*]
-- Module: Mathlib.Data.Nat.Cast.Field
Goal:
K : Type u_1
inst : DivisionSemiring K
m n : ℕ
inst_1 : CharZero K
hnm : n ∣ m
hn : n ≠ 0
⊢ (↑(m / n) : K) = HDiv.hDiv (α := K) (↑m : K) (↑n : K)

Tactic:
simp [*]
-- Module: Mathlib.Data.Nat.Cast.Field
Goal:
K : Type u_1
inst : DivisionSemiring K
d m n : ℕ
inst_1 : CharZero K
hn : d ∣ n
hm : d ∣ m
inl :
  ∀ (hn : 0 ∣ n) (hm : 0 ∣ m), HDiv.hDiv (α := K) (↑(m / 0) : K) (↑(n / 0) : K) = HDiv.hDiv (α := K) (↑m : K) (↑n : K)
inr : ∀ (hd : d ≠ 0), HDiv.hDiv (α := K) (↑(m / d) : K) (↑(n / d) : K) = HDiv.hDiv (α := K) (↑m : K) (↑n : K)
⊢ HDiv.hDiv (α := K) (↑(m / d) : K) (↑(n / d) : K) = HDiv.hDiv (α := K) (↑m : K) (↑n : K)

Tactic:
rcases eq_or_ne d 0 with (rfl | hd)

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Data.Nat.Cast.Field
Goal:
K : Type u_1
inst : DivisionSemiring K
m n : ℕ
inst_1 : CharZero K
hn : 0 ∣ n
hm : 0 ∣ m
⊢ HDiv.hDiv (α := K) (↑(m / 0) : K) (↑(n / 0) : K) = HDiv.hDiv (α := K) (↑m : K) (↑n : K)

Tactic:
simp [Nat.zero_dvd.1 hm]

Premises used: Nat.zero_dvd, Iff.mp
-- Module: Mathlib.Data.Nat.Cast.Field
Goal:
K : Type u_1
inst : DivisionSemiring K
d m n : ℕ
inst_1 : CharZero K
hn : d ∣ n
hm : d ∣ m
hd : d ≠ 0
norm_cast norm_cast₁ norm_cast₂ norm_cast₃ : ¬d = 0
⊢ Ne.{u_1 + 1} (α := K) (↑d : K) 0

Tactic:
norm_cast
-- Module: Mathlib.Data.Nat.Cast.Field
Goal:
K : Type u_1
inst : DivisionSemiring K
d m n : ℕ
inst_1 : CharZero K
hn : d ∣ n
hm : d ∣ m
hd : d ≠ 0
⊢ Ne.{u_1 + 1} (α := K) (↑d : K) 0

Tactic:
replace hd : (d : K) ≠ 0 := by norm_cast
-- Module: Mathlib.Data.Nat.Cast.Field
Goal:
K : Type u_1
inst : DivisionSemiring K
d m n : ℕ
inst_1 : CharZero K
hn : d ∣ n
hm : d ∣ m
hd inr inr₁ : Ne.{u_1 + 1} (α := K) (↑d : K) 0
⊢ HDiv.hDiv (α := K) (↑(m / d) : K) (↑(n / d) : K) = HDiv.hDiv (α := K) (↑m : K) (↑n : K)

Tactic:
rw [cast_div hm, cast_div hn, div_div_div_cancel_right₀ hd]

Premises used: div_div_div_cancel_right₀, Nat.cast_div
-- Module: Mathlib.Data.Nat.Cast.Field
Goal:
K : Type u_1
inst : DivisionSemiring K
d m n : ℕ
inst_1 : CharZero K
hn : d ∣ n
hm : d ∣ m
hd : Ne.{u_1 + 1} (α := K) (↑d : K) 0
⊢ Ne.{u_1 + 1} (α := K) (↑d : K) 0

Tactic:
hd
-- Module: Mathlib.Data.Nat.Cast.Field
Goal:
K : Type u_1
inst : DivisionSemiring K
d m n : ℕ
inst_1 : CharZero K
hn : d ∣ n
hm : d ∣ m
hd : Ne.{u_1 + 1} (α := K) (↑d : K) 0
⊢ Ne.{u_1 + 1} (α := K) (↑d : K) 0

Tactic:
exact hd
-- Module: Mathlib.Data.Nat.Cast.NeZero
Goal:
n : ℕ
inst : NeZero n
⊢ n ≠ 0

Tactic:
have := NeZero.ne n
-- Module: Mathlib.Data.Nat.Cast.NeZero
Goal:
n : ℕ
inst : NeZero n
this : n ≠ 0
⊢ 1 ≤ n

Tactic:
lia
-- Module: Mathlib.Data.Nat.Cast.NeZero
Goal:
n : ℕ
R : Type u_1
inst : AddMonoidWithOne R
h : NeZero.{u_1} (R := R) (↑n : R)
⊢ Ne.{u_1 + 1} (α := R) (↑n : R) 0

Tactic:
h.out

Premises used: NeZero.out
-- Module: Mathlib.Data.Nat.Cast.NeZero
Goal:
R : Type u_1
inst : AddMonoidWithOne R
h : NeZero.{u_1} (R := R) (↑0 : R)
⊢ False

Tactic:
h.out Nat.cast_zero

Premises used: NeZero.out, Nat.cast_zero
-- Module: Mathlib.Data.Nat.Cast.NeZero
Goal:
R : Type u_1
inst : AddMonoidWithOne R
h : NeZero.{u_1} (R := R) (↑0 : R)
⊢ False

Tactic:
exact h.out Nat.cast_zero

Premises used: NeZero.out, Nat.cast_zero
-- Module: Mathlib.Data.Nat.Cast.NeZero
Goal:
R : Type u_1
inst : AddMonoidWithOne R
n : ℕ
inst_1 : NeZero.{u_1} (R := R) (↑n : R)
⊢ 0 < n

Tactic:
Nat.pos_of_ne_zero (of_neZero_natCast R).out

Premises used: Nat.pos_of_ne_zero, NeZero.out
-- Module: Mathlib.Data.Nat.Cast.Order.Basic
Goal:
α : Type u_1
inst : AddMonoidWithOne α
inst_1 : PartialOrder α
inst_2 : AddLeftMono α
inst_3 : ZeroLEOneClass α
n : ℕ
rw : (↑n : α) ≤ HAdd.hAdd (α := α) (↑n : α) 1
⊢ LE.le.{u_1} (α := α) (↑n : α) (↑(n + 1) : α)

Tactic:
rw [Nat.cast_succ]

Premises used: Nat.cast_succ
-- Module: Mathlib.Data.Nat.Cast.Order.Basic
Goal:
α : Type u_1
inst : AddMonoidWithOne α
inst_1 : PartialOrder α
inst_2 : AddLeftMono α
inst_3 : ZeroLEOneClass α
n : ℕ
⊢ (↑n : α) ≤ HAdd.hAdd (α := α) (↑n : α) 1

Tactic:
le_add_of_nonneg_right zero_le_one

Premises used: zero_le_one, le_add_of_nonneg_right
-- Module: Mathlib.Data.Nat.Cast.Order.Basic
Goal:
α : Type u_1
inst : AddMonoidWithOne α
inst_1 : PartialOrder α
inst_2 : AddLeftMono α
inst_3 : ZeroLEOneClass α
n : ℕ
⊢ (↑n : α) ≤ HAdd.hAdd (α := α) (↑n : α) 1

Tactic:
exact le_add_of_nonneg_right zero_le_one

Premises used: zero_le_one, le_add_of_nonneg_right
-- Module: Mathlib.Data.Nat.Cast.Order.Basic
Goal:
α : Type u_1
inst : AddMonoidWithOne α
inst_1 : PartialOrder α
inst_2 : AddLeftMono α
inst_3 : ZeroLEOneClass α
n : ℕ
⊢ LE.le.{u_1} (α := α) 0 (↑n : α)

Tactic:
@Nat.cast_zero α _ ▸ mono_cast (Nat.zero_le n)

Premises used: Nat.zero_le, Nat.mono_cast, Eq.rec, Nat.cast_zero
-- Module: Mathlib.Data.Nat.Cast.Order.Basic
Goal:
α : Type u_1
inst : AddMonoidWithOne α
inst_1 : PartialOrder α
inst_2 : AddLeftMono α
inst_3 : ZeroLEOneClass α
n : ℕ
inst_4 : n.AtLeastTwo
⊢ LE.le.{u_1} (α := α) 0 (OfNat.ofNat n)

Tactic:
cast_nonneg' n

Premises used: Nat.cast_nonneg'
-- Module: Mathlib.Data.Nat.Cast.Order.Basic
Goal:
α : Type u_1
inst : AddMonoidWithOne α
inst_1 : PartialOrder α
inst_2 : AddLeftMono α
inst_3 : ZeroLEOneClass α
inst_4 : NeZero.{u_1} (R := α) 1
n : ℕ
apply : 1 ≤ HAdd.hAdd (α := α) (↑n : α) 1
⊢ 0 < HAdd.hAdd (α := α) (↑n : α) 1

Tactic:
apply zero_lt_one.trans_le

Premises used: zero_lt_one, LT.lt.trans_le
-- Module: Mathlib.Data.Nat.Cast.Order.Basic
Goal:
α : Type u_1
inst : AddMonoidWithOne α
inst_1 : PartialOrder α
inst_2 : AddLeftMono α
inst_3 : ZeroLEOneClass α
inst_4 : NeZero.{u_1} (R := α) 1
n : ℕ
⊢ LE.le.{u_1} (α := α) (↑1 : α) (↑(n + 1) : α)

Tactic:
(@mono_cast α _).imp (?_ : 1 ≤ n + 1)

Premises used: Nat.mono_cast, Monotone.imp
-- Module: Mathlib.Data.Nat.Cast.Order.Basic
Goal:
α : Type u_1
inst : AddMonoidWithOne α
inst_1 : PartialOrder α
inst_2 : AddLeftMono α
inst_3 : ZeroLEOneClass α
inst_4 : NeZero.{u_1} (R := α) 1
n : ℕ
h : Eq.{u_1 + 1} (α := α) 1 (↑1 : α)
h₁ : HAdd.hAdd (α := α) (↑n : α) 1 = (↑(n + 1) : α)
convert! : 1 ≤ n + 1
⊢ 1 ≤ HAdd.hAdd (α := α) (↑n : α) 1

Tactic:
convert! (@mono_cast α _).imp (?_ : 1 ≤ n + 1)

Premises used: Nat.mono_cast, Monotone.imp
-- Module: Mathlib.Data.Nat.Cast.Order.Basic
Goal:
α : Type u_1
inst : AddMonoidWithOne α
inst_1 : PartialOrder α
inst_2 : AddLeftMono α
inst_3 : ZeroLEOneClass α
inst_4 : NeZero.{u_1} (R := α) 1
n : ℕ
⊢ Eq.{u_1 + 1} (α := α) 1 (↑1 : α)

Tactic:
simp
-- Module: Mathlib.Data.Nat.Cast.Order.Basic
Goal:
α : Type u_1
inst : AddMonoidWithOne α
inst_1 : PartialOrder α
inst_2 : AddLeftMono α
inst_3 : ZeroLEOneClass α
inst_4 : NeZero.{u_1} (R := α) 1
n : ℕ
⊢ HAdd.hAdd (α := α) (↑n : α) 1 = (↑(n + 1) : α)

Tactic:
simp
-- Module: Mathlib.Data.Nat.Cast.Order.Basic
Goal:
α : Type u_1
inst : AddMonoidWithOne α
inst_1 : PartialOrder α
inst_2 : AddLeftMono α
inst_3 : ZeroLEOneClass α
inst_4 : NeZero.{u_1} (R := α) 1
n : ℕ
⊢ 1 ≤ n + 1

Tactic:
simp
-- Module: Mathlib.Data.Nat.Cast.Order.Basic
Goal:
α : Type u_1
inst : AddMonoidWithOne α
inst_1 : PartialOrder α
inst_2 : AddLeftMono α
inst_3 : ZeroLEOneClass α
inst_4 : NeZero.{u_1} (R := α) 1
n : ℕ
zero : LT.lt.{u_1} (α := α) 0 (↑0 : α) ↔ LT.lt (α := ℕ) 0 0
succ : ∀ (n : ℕ), LT.lt.{u_1} (α := α) 0 (↑(n + 1) : α) ↔ 0 < n + 1
⊢ LT.lt.{u_1} (α := α) 0 (↑n : α) ↔ 0 < n

Tactic:
cases n
-- Module: Mathlib.Data.Nat.Cast.Order.Basic
Goal:
α : Type u_1
inst : AddMonoidWithOne α
inst_1 : PartialOrder α
inst_2 : AddLeftMono α
inst_3 : ZeroLEOneClass α
inst_4 : NeZero.{u_1} (R := α) 1
⊢ LT.lt.{u_1} (α := α) 0 (↑0 : α) ↔ LT.lt (α := ℕ) 0 0

Tactic:
simp [cast_add_one_pos]

Premises used: Nat.cast_add_one_pos
-- Module: Mathlib.Data.Nat.Cast.Order.Basic
Goal:
α : Type u_1
inst : AddMonoidWithOne α
inst_1 : PartialOrder α
inst_2 : AddLeftMono α
inst_3 : ZeroLEOneClass α
inst_4 : NeZero.{u_1} (R := α) 1
n : ℕ
⊢ LT.lt.{u_1} (α := α) 0 (↑(n + 1) : α) ↔ 0 < n + 1

Tactic:
simp [cast_add_one_pos]

Premises used: Nat.cast_add_one_pos
-- Module: Mathlib.Data.Nat.Cast.Order.Basic
Goal:
α : Type u_1
inst : AddMonoidWithOne α
inst_1 : PartialOrder α
inst_2 : AddLeftMono α
inst_3 : ZeroLEOneClass α
inst_4 : CharZero α
⊢ StrictMono.{0, u_1} (β := α) Nat.cast

Tactic:
mono_cast.strictMono_of_injective cast_injective

Premises used: Nat.mono_cast, Monotone.strictMono_of_injective, Nat.cast_injective
-- Module: Mathlib.Data.Nat.Cast.Order.Basic
Goal:
α : Type u_1
inst : AddMonoidWithOne α
inst_1 : PartialOrder α
inst_2 : AddLeftMono α
inst_3 : ZeroLEOneClass α
inst_4 : CharZero α
m n : ℕ
⊢ LE.le.{u_1} (α := α) (↑m : α) (↑n : α) ↔ m ≤ n

Tactic:
strictMono_cast.le_iff_le

Premises used: Nat.strictMono_cast, StrictMono.le_iff_le
-- Module: Mathlib.Data.Nat.Cast.Order.Basic
Goal:
α : Type u_1
inst : AddMonoidWithOne α
inst_1 : PartialOrder α
inst_2 : AddLeftMono α
inst_3 : ZeroLEOneClass α
inst_4 : CharZero α
m n : ℕ
⊢ LT.lt.{u_1} (α := α) (↑m : α) (↑n : α) ↔ m < n

Tactic:
strictMono_cast.lt_iff_lt

Premises used: StrictMono.lt_iff_lt, Nat.strictMono_cast
-- Module: Mathlib.Data.Nat.Cast.Order.Basic
Goal:
α : Type u_1
inst : AddMonoidWithOne α
inst_1 : PartialOrder α
inst_2 : AddLeftMono α
inst_3 : ZeroLEOneClass α
inst_4 : CharZero α
n : ℕ
rw : LT.lt.{u_1} (α := α) (↑1 : α) (↑n : α) ↔ 1 < n
rw₁ rw₂ : 1 < n ↔ 1 < n
⊢ LT.lt.{u_1} (α := α) 1 (↑n : α) ↔ 1 < n

Tactic:
rw [← cast_one, cast_lt]

Premises used: Nat.cast_lt, Nat.cast_one
-- Module: Mathlib.Data.Nat.Cast.Order.Basic
Goal:
α : Type u_1
inst : AddMonoidWithOne α
inst_1 : PartialOrder α
inst_2 : AddLeftMono α
inst_3 : ZeroLEOneClass α
inst_4 : CharZero α
n : ℕ
rw : LE.le.{u_1} (α := α) (↑1 : α) (↑n : α) ↔ 1 ≤ n
rw₁ rw₂ : 1 ≤ n ↔ 1 ≤ n
⊢ LE.le.{u_1} (α := α) 1 (↑n : α) ↔ 1 ≤ n

Tactic:
rw [← cast_one, cast_le]

Premises used: Nat.cast_le, Nat.cast_one
-- Module: Mathlib.Data.Nat.Cast.Order.Basic
Goal:
α : Type u_1
inst : AddMonoidWithOne α
inst_1 : PartialOrder α
inst_2 : AddLeftMono α
inst_3 : ZeroLEOneClass α
inst_4 : CharZero α
n : ℕ
⊢ LE.le.{u_1} (α := α) 1 (↑n : α) ↔ n ≠ 0

Tactic:
one_le_cast.trans one_le_iff_ne_zero

Premises used: Nat.one_le_cast, Iff.trans, Nat.one_le_iff_ne_zero
-- Module: Mathlib.Data.Nat.Cast.Order.Basic
Goal:
α : Type u_1
inst : AddMonoidWithOne α
inst_1 : PartialOrder α
inst_2 : AddLeftMono α
inst_3 : ZeroLEOneClass α
inst_4 : CharZero α
n : ℕ
rw : LT.lt.{u_1} (α := α) (↑n : α) (↑1 : α) ↔ n = 0
rw₁ : n < 1 ↔ n = 0
rw₂ : n ≤ 0 ↔ n = 0
rw₃ rw₄ : n = 0 ↔ n = 0
⊢ LT.lt.{u_1} (α := α) (↑n : α) 1 ↔ n = 0

Tactic:
rw [← cast_one, cast_lt, Nat.lt_succ_iff, le_zero]

Premises used: Nat.le_zero, Nat.lt_succ_iff, Nat.cast_lt, Nat.cast_one
-- Module: Mathlib.Data.Nat.Cast.Order.Basic
Goal:
α : Type u_1
inst : AddMonoidWithOne α
inst_1 : PartialOrder α
inst_2 : AddLeftMono α
inst_3 : ZeroLEOneClass α
inst_4 : CharZero α
n : ℕ
rw : LE.le.{u_1} (α := α) (↑n : α) (↑1 : α) ↔ n ≤ 1
rw₁ rw₂ : n ≤ 1 ↔ n ≤ 1
⊢ LE.le.{u_1} (α := α) (↑n : α) 1 ↔ n ≤ 1

Tactic:
rw [← cast_one, cast_le]

Premises used: Nat.cast_le, Nat.cast_one
-- Module: Mathlib.Data.Nat.Cast.Order.Basic
Goal:
α : Type u_1
inst : AddMonoidWithOne α
inst_1 : PartialOrder α
inst_2 : AddLeftMono α
inst_3 : ZeroLEOneClass α
inst_4 : CharZero α
n : ℕ
norm_cast : n ≤ 0 ↔ n = 0
⊢ LE.le.{u_1} (α := α) (↑n : α) 0 ↔ n = 0

Tactic:
norm_cast
-- Module: Mathlib.Data.Nat.Cast.Order.Basic
Goal:
α : Type u_1
inst : AddMonoidWithOne α
inst_1 : PartialOrder α
inst_2 : AddLeftMono α
inst_3 : ZeroLEOneClass α
inst_4 : CharZero α
n : ℕ
⊢ n ≤ 0 ↔ n = 0

Tactic:
lia
-- Module: Mathlib.Data.Nat.Cast.Order.Basic
Goal:
α : Type u_1
inst : AddMonoidWithOne α
inst_1 : PartialOrder α
inst_2 : AddLeftMono α
inst_3 : ZeroLEOneClass α
inst_4 : CharZero α
m n : ℕ
inst_5 : m.AtLeastTwo
⊢ LE.le.{u_1} (α := α) (OfNat.ofNat m) (↑n : α) ↔ OfNat.ofNat m ≤ n

Tactic:
cast_le

Premises used: Nat.cast_le
-- Module: Mathlib.Data.Nat.Cast.Order.Basic
Goal:
α : Type u_1
inst : AddMonoidWithOne α
inst_1 : PartialOrder α
inst_2 : AddLeftMono α
inst_3 : ZeroLEOneClass α
inst_4 : CharZero α
m n : ℕ
inst_5 : m.AtLeastTwo
⊢ LT.lt.{u_1} (α := α) (OfNat.ofNat m) (↑n : α) ↔ OfNat.ofNat m < n

Tactic:
cast_lt

Premises used: Nat.cast_lt
-- Module: Mathlib.Data.Nat.Cast.Order.Basic
Goal:
α : Type u_1
inst : AddMonoidWithOne α
inst_1 : PartialOrder α
inst_2 : AddLeftMono α
inst_3 : ZeroLEOneClass α
inst_4 : CharZero α
m n : ℕ
inst_5 : n.AtLeastTwo
⊢ LE.le.{u_1} (α := α) (↑m : α) (OfNat.ofNat n) ↔ m ≤ OfNat.ofNat n

Tactic:
cast_le

Premises used: Nat.cast_le
-- Module: Mathlib.Data.Nat.Cast.Order.Basic
Goal:
α : Type u_1
inst : AddMonoidWithOne α
inst_1 : PartialOrder α
inst_2 : AddLeftMono α
inst_3 : ZeroLEOneClass α
inst_4 : CharZero α
m n : ℕ
inst_5 : n.AtLeastTwo
⊢ LT.lt.{u_1} (α := α) (↑m : α) (OfNat.ofNat n) ↔ m < OfNat.ofNat n

Tactic:
cast_lt

Premises used: Nat.cast_lt
-- Module: Mathlib.Data.Nat.Cast.Order.Basic
Goal:
α : Type u_1
inst : AddMonoidWithOne α
inst_1 : PartialOrder α
inst_2 : AddLeftMono α
inst_3 : ZeroLEOneClass α
inst_4 : CharZero α
n : ℕ
inst_5 : n.AtLeastTwo
⊢ LT.lt.{u_1} (α := α) 1 (OfNat.ofNat n)

Tactic:
one_lt_cast.mpr AtLeastTwo.one_lt

Premises used: Iff.mpr, Nat.AtLeastTwo.one_lt, Nat.one_lt_cast
-- Module: Mathlib.Data.Nat.Cast.Order.Basic
Goal:
α : Type u_1
inst : AddMonoidWithOne α
inst_1 : PartialOrder α
inst_2 : AddLeftMono α
inst_3 : ZeroLEOneClass α
inst_4 : CharZero α
n : ℕ
inst_5 : n.AtLeastTwo
⊢ LE.le.{u_1} (α := α) 1 (OfNat.ofNat n)

Tactic:
one_le_cast.mpr NeZero.one_le

Premises used: Iff.mpr, Nat.one_le_cast, NeZero.one_le
-- Module: Mathlib.Data.Nat.Cast.Order.Basic
Goal:
α : Type u_1
inst : AddMonoidWithOne α
inst_1 : PartialOrder α
inst_2 : AddLeftMono α
inst_3 : ZeroLEOneClass α
inst_4 : CharZero α
n : ℕ
inst_5 : n.AtLeastTwo
⊢ ¬LE.le.{u_1} (α := α) (OfNat.ofNat n) 1

Tactic:
(cast_le_one.not.trans not_le).mpr AtLeastTwo.one_lt

Premises used: not_le, Iff.mpr, Nat.AtLeastTwo.one_lt, Iff.not, Iff.trans, Nat.cast_le_one
-- Module: Mathlib.Data.Nat.Cast.Order.Basic
Goal:
α : Type u_1
inst : AddMonoidWithOne α
inst_1 : PartialOrder α
inst_2 : AddLeftMono α
inst_3 : ZeroLEOneClass α
inst_4 : CharZero α
n : ℕ
inst_5 : n.AtLeastTwo
⊢ ¬LT.lt.{u_1} (α := α) (OfNat.ofNat n) 1

Tactic:
mt le_of_lt not_ofNat_le_one

Premises used: le_of_lt, mt, Nat.not_ofNat_le_one
-- Module: Mathlib.Data.Nat.Cast.Order.Basic
Goal:
α : Type u_1
inst : AddMonoidWithOne α
inst_1 : PartialOrder α
inst_2 : AddLeftMono α
inst_3 : ZeroLEOneClass α
inst_4 : CharZero α
m n : ℕ
inst_5 : n.AtLeastTwo
inst_6 : m.AtLeastTwo
⊢ LE.le.{u_1} (α := α) (OfNat.ofNat m) (OfNat.ofNat n) ↔ LE.le (α := ℕ) (OfNat.ofNat m) (OfNat.ofNat n)

Tactic:
cast_le

Premises used: Nat.cast_le
-- Module: Mathlib.Data.Nat.Cast.Order.Basic
Goal:
α : Type u_1
inst : AddMonoidWithOne α
inst_1 : PartialOrder α
inst_2 : AddLeftMono α
inst_3 : ZeroLEOneClass α
inst_4 : CharZero α
m n : ℕ
inst_5 : n.AtLeastTwo
inst_6 : m.AtLeastTwo
⊢ LT.lt.{u_1} (α := α) (OfNat.ofNat m) (OfNat.ofNat n) ↔ LT.lt (α := ℕ) (OfNat.ofNat m) (OfNat.ofNat n)

Tactic:
cast_lt

Premises used: Nat.cast_lt
-- Module: Mathlib.Data.Nat.Cast.Order.Basic
Goal:
α : Type u_1
inst : AddMonoidWithOne α
inst_1 : CharZero α
⊢ Ne (α := ℕ) 1 0

Tactic:
decide
-- Module: Mathlib.Data.Nat.Cast.Order.Basic
Goal:
R : Type u_2
S : Type u_3
F : Type u_4
inst : NonAssocSemiring R
inst_1 : NonAssocSemiring S
inst_2 : FunLike F R S
n : ℕ
inst_3 : NeZero.{u_2} (R := R) (↑n : R)
inst_4 : RingHomClass F R S
f : F
hf : Function.Injective.{u_2 + 1, u_3 + 1} (α := R) (β := S) (⇑f : (a : R) → S)
h : Eq.{u_3 + 1} (α := S) (↑n : S) 0
⊢ Eq.{u_3 + 1} (α := S) ((f : (a : R) → S) (↑n : R) : S) ((f : (a : R) → S) 0 : S)

Tactic:
simpa only [map_natCast, map_zero f]

Premises used: map_zero, map_natCast
-- Module: Mathlib.Data.Nat.Cast.Order.Field
Goal:
α : Type u_1
inst : Semifield α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
⊢ LE.le.{u_1} (α := α) (↑0 : α)⁻¹ 1

Tactic:
simp
-- Module: Mathlib.Data.Nat.Cast.Order.Field
Goal:
α : Type u_1
inst : Semifield α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
n : ℕ
⊢ LE.le.{u_1} (α := α) 1 (↑(n + 1) : α)

Tactic:
simp [Nat.cast_nonneg]

Premises used: Nat.cast_nonneg
-- Module: Mathlib.Data.Nat.Cast.Order.Field
Goal:
α : Type u_1
inst : Semifield α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
m n : ℕ
zero : (↑(m / 0) : α) ≤ HDiv.hDiv (α := α) (↑m : α) (↑0 : α)
succ : ∀ (n : ℕ), (↑(m / (n + 1)) : α) ≤ HDiv.hDiv (α := α) (↑m : α) (↑(n + 1) : α)
⊢ (↑(m / n) : α) ≤ HDiv.hDiv (α := α) (↑m : α) (↑n : α)

Tactic:
cases n
-- Module: Mathlib.Data.Nat.Cast.Order.Field
Goal:
α : Type u_1
inst : Semifield α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
m : ℕ
zero : (↑(m / 0) : α) ≤ HDiv.hDiv (α := α) (↑m : α) 0
zero₁ : LE.le.{u_1} (α := α) (↑(m / 0) : α) 0
zero₂ : LE.le.{u_1} (α := α) (↑0 : α) 0
zero₃ zero₄ : LE.le.{u_1} (α := α) 0 0
⊢ (↑(m / 0) : α) ≤ HDiv.hDiv (α := α) (↑m : α) (↑0 : α)

Tactic:
rw [cast_zero, div_zero, Nat.div_zero, cast_zero]

Premises used: Nat.div_zero, Nat.cast_zero, div_zero
-- Module: Mathlib.Data.Nat.Cast.Order.Field
Goal:
α : Type u_1
inst : Semifield α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
m n : ℕ
succ : m / (n + 1) * (n + 1) ≤ m
succ₁ : LT.lt.{u_1} (α := α) 0 (↑(n + 1) : α)
⊢ (↑(m / (n + 1)) : α) ≤ HDiv.hDiv (α := α) (↑m : α) (↑(n + 1) : α)

Tactic:
rw [le_div_iff₀, ← Nat.cast_mul, @Nat.cast_le]

Premises used: Nat.cast_mul, Nat.cast_le, le_div_iff₀
-- Module: Mathlib.Data.Nat.Cast.Order.Field
Goal:
α : Type u_1
inst : Semifield α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
m n : ℕ
⊢ m / (n + 1) * (n + 1) ≤ m

Tactic:
Nat.div_mul_le_self m _

Premises used: Nat.div_mul_le_self
-- Module: Mathlib.Data.Nat.Cast.Order.Field
Goal:
α : Type u_1
inst : Semifield α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
m n : ℕ
⊢ m / (n + 1) * (n + 1) ≤ m

Tactic:
exact Nat.div_mul_le_self m _

Premises used: Nat.div_mul_le_self
-- Module: Mathlib.Data.Nat.Cast.Order.Field
Goal:
α : Type u_1
inst : Semifield α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
m n : ℕ
⊢ LT.lt.{u_1} (α := α) 0 (↑(n + 1) : α)

Tactic:
Nat.cast_pos.2 (Nat.succ_pos _)

Premises used: Iff.mpr, Nat.cast_pos, Nat.succ_pos
-- Module: Mathlib.Data.Nat.Cast.Order.Field
Goal:
α : Type u_1
inst : Semifield α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
m n : ℕ
⊢ LT.lt.{u_1} (α := α) 0 (↑(n + 1) : α)

Tactic:
exact Nat.cast_pos.2 (Nat.succ_pos _)

Premises used: Iff.mpr, Nat.cast_pos, Nat.succ_pos
-- Module: Mathlib.Data.Nat.Cast.Order.Field
Goal:
α : Type u_1
inst : Semifield α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
n : ℕ
⊢ 0 < (HAdd.hAdd (α := α) (↑n : α) 1)⁻¹

Tactic:
inv_pos.2 <| add_pos_of_nonneg_of_pos n.cast_nonneg zero_lt_one

Premises used: Iff.mpr, Nat.cast_nonneg, inv_pos, zero_lt_one, add_pos_of_nonneg_of_pos
-- Module: Mathlib.Data.Nat.Cast.Order.Field
Goal:
α : Type u_1
inst : Semifield α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
n : ℕ
rw : 0 < (HAdd.hAdd (α := α) (↑n : α) 1)⁻¹
⊢ 0 < 1 / HAdd.hAdd (α := α) (↑n : α) 1

Tactic:
rw [one_div]

Premises used: one_div
-- Module: Mathlib.Data.Nat.Cast.Order.Field
Goal:
α : Type u_1
inst : Semifield α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
n : ℕ
⊢ 0 < (HAdd.hAdd (α := α) (↑n : α) 1)⁻¹

Tactic:
inv_pos_of_nat

Premises used: Nat.inv_pos_of_nat
-- Module: Mathlib.Data.Nat.Cast.Order.Field
Goal:
α : Type u_1
inst : Semifield α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
n : ℕ
⊢ 0 < (HAdd.hAdd (α := α) (↑n : α) 1)⁻¹

Tactic:
exact inv_pos_of_nat

Premises used: Nat.inv_pos_of_nat
-- Module: Mathlib.Data.Nat.Cast.Order.Field
Goal:
α : Type u_1
inst : Semifield α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
n m : ℕ
h : n ≤ m
⊢ 1 / HAdd.hAdd (α := α) (↑m : α) 1 ≤ 1 / HAdd.hAdd (α := α) (↑n : α) 1

Tactic:
one_div_le_one_div_of_le ?_ ?_

Premises used: one_div_le_one_div_of_le
-- Module: Mathlib.Data.Nat.Cast.Order.Field
Goal:
α : Type u_1
inst : Semifield α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
n m : ℕ
h : n ≤ m
refine_1 : 0 < HAdd.hAdd (α := α) (↑n : α) 1
refine_2 : HAdd.hAdd (α := α) (↑n : α) 1 ≤ HAdd.hAdd (α := α) (↑m : α) 1
⊢ 1 / HAdd.hAdd (α := α) (↑m : α) 1 ≤ 1 / HAdd.hAdd (α := α) (↑n : α) 1

Tactic:
refine one_div_le_one_div_of_le ?_ ?_

Premises used: one_div_le_one_div_of_le
-- Module: Mathlib.Data.Nat.Cast.Order.Field
Goal:
α : Type u_1
inst : Semifield α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
n m : ℕ
h : n ≤ m
⊢ 0 < HAdd.hAdd (α := α) (↑n : α) 1

Tactic:
Nat.cast_add_one_pos _

Premises used: Nat.cast_add_one_pos
-- Module: Mathlib.Data.Nat.Cast.Order.Field
Goal:
α : Type u_1
inst : Semifield α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
n m : ℕ
h : n ≤ m
⊢ 0 < HAdd.hAdd (α := α) (↑n : α) 1

Tactic:
exact Nat.cast_add_one_pos _

Premises used: Nat.cast_add_one_pos
-- Module: Mathlib.Data.Nat.Cast.Order.Field
Goal:
α : Type u_1
inst : Semifield α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
n m : ℕ
h : n ≤ m
⊢ HAdd.hAdd (α := α) (↑n : α) 1 ≤ HAdd.hAdd (α := α) (↑m : α) 1

Tactic:
simpa
-- Module: Mathlib.Data.Nat.Cast.Order.Field
Goal:
α : Type u_1
inst : Semifield α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
n m : ℕ
h : n < m
⊢ 1 / HAdd.hAdd (α := α) (↑m : α) 1 < 1 / HAdd.hAdd (α := α) (↑n : α) 1

Tactic:
one_div_lt_one_div_of_lt ?_ ?_

Premises used: one_div_lt_one_div_of_lt
-- Module: Mathlib.Data.Nat.Cast.Order.Field
Goal:
α : Type u_1
inst : Semifield α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
n m : ℕ
h : n < m
refine_1 : 0 < HAdd.hAdd (α := α) (↑n : α) 1
refine_2 : HAdd.hAdd (α := α) (↑n : α) 1 < HAdd.hAdd (α := α) (↑m : α) 1
⊢ 1 / HAdd.hAdd (α := α) (↑m : α) 1 < 1 / HAdd.hAdd (α := α) (↑n : α) 1

Tactic:
refine one_div_lt_one_div_of_lt ?_ ?_

Premises used: one_div_lt_one_div_of_lt
-- Module: Mathlib.Data.Nat.Cast.Order.Field
Goal:
α : Type u_1
inst : Semifield α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
n m : ℕ
h : n < m
⊢ 0 < HAdd.hAdd (α := α) (↑n : α) 1

Tactic:
Nat.cast_add_one_pos _

Premises used: Nat.cast_add_one_pos
-- Module: Mathlib.Data.Nat.Cast.Order.Field
Goal:
α : Type u_1
inst : Semifield α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
n m : ℕ
h : n < m
⊢ 0 < HAdd.hAdd (α := α) (↑n : α) 1

Tactic:
exact Nat.cast_add_one_pos _

Premises used: Nat.cast_add_one_pos
-- Module: Mathlib.Data.Nat.Cast.Order.Field
Goal:
α : Type u_1
inst : Semifield α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
n m : ℕ
h : n < m
⊢ HAdd.hAdd (α := α) (↑n : α) 1 < HAdd.hAdd (α := α) (↑m : α) 1

Tactic:
simpa
-- Module: Mathlib.Data.Nat.Cast.Order.Field
Goal:
α : Type u_1
inst : Semifield α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
n : ℕ
hn : n ≠ 0
⊢ 0 < HDiv.hDiv (α := α) 1 (↑n : α)

Tactic:
one_div_pos.mpr (cast_pos.mpr (Nat.pos_of_ne_zero hn))

Premises used: Iff.mpr, Nat.cast_pos, Nat.pos_of_ne_zero, one_div_pos