awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.NNRat.Defs
Goal:
q : ℚ
p : ℚ≥0
⊢ q.toNNRat ≤ p ↔ q ≤ (↑p : ℚ)

Tactic:
NNRat.gi.gc q p

Premises used: NNRat.gi, GaloisInsertion.gc
-- Module: Mathlib.Data.NNRat.Defs
Goal:
p : ℚ
q : ℚ≥0
hp : 0 ≤ p
rw : LE.le (α := ℚ) (↑q : ℚ) (↑p.toNNRat : ℚ) ↔ (↑q : ℚ) ≤ p
rw₁ rw₂ : (↑q : ℚ) ≤ p ↔ (↑q : ℚ) ≤ p
⊢ q ≤ p.toNNRat ↔ (↑q : ℚ) ≤ p

Tactic:
rw [← coe_le_coe, Rat.coe_toNNRat p hp]

Premises used: NNRat.coe_le_coe, Rat.coe_toNNRat
-- Module: Mathlib.Data.NNRat.Defs
Goal:
p : ℚ
q : ℚ≥0
hq : 0 < q
hp : p < 0
⊢ q ≤ p.toNNRat ↔ (↑q : ℚ) ≤ p

Tactic:
simp only [(hp.trans_le q.coe_nonneg).not_ge, toNNRat_eq_zero.2 hp.le, hq.not_ge]

Premises used: Iff.mpr, LT.lt.le, LT.lt.trans_le, NNRat.coe_nonneg, LT.lt.not_ge, Rat.toNNRat_eq_zero
-- Module: Mathlib.Data.NNRat.Defs
Goal:
q : ℚ
p : ℚ≥0
hq : 0 ≤ q
rw : LT.lt (α := ℚ) (↑q.toNNRat : ℚ) (↑p : ℚ) ↔ q < (↑p : ℚ)
rw₁ rw₂ : q < (↑p : ℚ) ↔ q < (↑p : ℚ)
⊢ q.toNNRat < p ↔ q < (↑p : ℚ)

Tactic:
rw [← coe_lt_coe, Rat.coe_toNNRat q hq]

Premises used: NNRat.coe_lt_coe, Rat.coe_toNNRat
-- Module: Mathlib.Data.NNRat.Defs
Goal:
p : ℚ
q : ℚ≥0
⊢ q < p.toNNRat ↔ (↑q : ℚ) < p

Tactic:
NNRat.gi.gc.lt_iff_lt

Premises used: NNRat.gi, GaloisInsertion.gc, GaloisConnection.lt_iff_lt
-- Module: Mathlib.Data.NNRat.Defs
Goal:
p q : ℚ
hp : 0 ≤ p
inl : ∀ (hq : 0 ≤ q), (p * q).toNNRat = p.toNNRat * q.toNNRat
inr : ∀ (hq : q ≤ 0), (p * q).toNNRat = p.toNNRat * q.toNNRat
⊢ (p * q).toNNRat = p.toNNRat * q.toNNRat

Tactic:
rcases le_total 0 q with hq | hq

Premises used: le_total, OfNat.ofNat
-- Module: Mathlib.Data.NNRat.Defs
Goal:
p q : ℚ
hp : 0 ≤ p
hq : 0 ≤ q
inl : Eq (α := ℚ) (↑(p * q).toNNRat : ℚ) (↑(p.toNNRat * q.toNNRat) : ℚ)
⊢ (p * q).toNNRat = p.toNNRat * q.toNNRat

Tactic:
ext
-- Module: Mathlib.Data.NNRat.Defs
Goal:
p q : ℚ
hp : 0 ≤ p
hq : 0 ≤ q
⊢ Eq (α := ℚ) (↑(p * q).toNNRat : ℚ) (↑(p.toNNRat * q.toNNRat) : ℚ)

Tactic:
simp [toNNRat, hp, hq, mul_nonneg]

Premises used: mul_nonneg, Rat.toNNRat
-- Module: Mathlib.Data.NNRat.Defs
Goal:
p q : ℚ
hp : 0 ≤ p
hq : q ≤ 0
⊢ p * q ≤ 0

Tactic:
have hpq := mul_nonpos_of_nonneg_of_nonpos hp hq
-- Module: Mathlib.Data.NNRat.Defs
Goal:
p q : ℚ
hp : 0 ≤ p
hq : q ≤ 0
hpq : p * q ≤ 0
inr : (p * q).toNNRat = p.toNNRat * 0
inr₁ : 0 = p.toNNRat * 0
inr₂ inr₃ : Eq (α := ℚ≥0) 0 0
⊢ (p * q).toNNRat = p.toNNRat * q.toNNRat

Tactic:
rw [toNNRat_eq_zero.2 hq, toNNRat_eq_zero.2 hpq, mul_zero]

Premises used: Iff.mpr, MulZeroClass.mul_zero, Rat.toNNRat_eq_zero
-- Module: Mathlib.Data.NNRat.Defs
Goal:
x : ℚ
⊢ (↑(nnabs x) : ℚ) = |x|

Tactic:
rfl

Premises used: abs, rfl
-- Module: Mathlib.Data.NNRat.Defs
Goal:
q : ℚ≥0
⊢ Rat.num (↑q : ℚ) = (↑q.num : ℤ)

Tactic:
simp only [num, Int.natCast_natAbs, Rat.num_nonneg, coe_nonneg, abs_of_nonneg]

Premises used: NNRat.num, NNRat.coe_nonneg, abs_of_nonneg, Rat.num_nonneg, Int.natCast_natAbs
-- Module: Mathlib.Data.NNRat.Defs
Goal:
q : ℚ≥0
⊢ (Rat.num (↑q : ℚ)).natAbs = q.num

Tactic:
rfl

Premises used: NNRat.num, rfl
-- Module: Mathlib.Data.NNRat.Defs
Goal:
q : ℚ≥0
⊢ Rat.den (↑q : ℚ) = q.den

Tactic:
rfl

Premises used: NNRat.den, rfl
-- Module: Mathlib.Data.NNRat.Defs
Goal:
q : ℚ≥0
⊢ q.num ≠ 0 ↔ q ≠ 0

Tactic:
simp [num]

Premises used: NNRat.num
-- Module: Mathlib.Data.NNRat.Defs
Goal:
q : ℚ≥0
⊢ 0 < q.num ↔ 0 < q

Tactic:
simpa [num, -nonpos_iff_eq_zero] using nonpos_iff_eq_zero _ |>.not.symm

Premises used: NNRat.nonpos_iff_eq_zero, Iff.not, NNRat.num, Iff.symm
-- Module: Mathlib.Data.NNRat.Defs
Goal:
q : ℚ≥0
⊢ 0 < q.den

Tactic:
Rat.den_pos _

Premises used: NNRat.den, Rat.den_pos
-- Module: Mathlib.Data.NNRat.Defs
Goal:
q : ℚ≥0
⊢ q.den ≠ 0

Tactic:
Rat.den_ne_zero _

Premises used: Rat.den_ne_zero, NNRat.den
-- Module: Mathlib.Data.NNRat.Defs
Goal:
q : ℚ≥0
⊢ q.num.Coprime q.den

Tactic:
simpa [num, den] using Rat.reduced _

Premises used: Rat.reduced, NNRat.num, NNRat.den
-- Module: Mathlib.Data.NNRat.Defs
Goal:
n : ℕ
⊢ num (↑n : ℚ≥0) = n

Tactic:
rfl

Premises used: NNRat.num, Int.natAbs, rfl
-- Module: Mathlib.Data.NNRat.Defs
Goal:
n : ℕ
⊢ den (↑n : ℚ≥0) = 1

Tactic:
rfl

Premises used: NNRat.den, rfl
-- Module: Mathlib.Data.NNRat.Defs
Goal:
n : ℕ
inst : n.AtLeastTwo
⊢ num (OfNat.ofNat n) = OfNat.ofNat n

Tactic:
rfl

Premises used: NNRat.num, Int.natAbs, rfl
-- Module: Mathlib.Data.NNRat.Defs
Goal:
n : ℕ
inst : n.AtLeastTwo
⊢ den (OfNat.ofNat n) = 1

Tactic:
rfl

Premises used: NNRat.den, rfl
-- Module: Mathlib.Data.NNRat.Defs
Goal:
p q : ℚ≥0
hn : p.num = q.num
hd : p.den = q.den
⊢ p = q

Tactic:
ext <| Rat.ext ?_ hd

Premises used: Rat.ext, NNRat.ext
-- Module: Mathlib.Data.NNRat.Defs
Goal:
p q : ℚ≥0
hn : p.num = q.num
hd : p.den = q.den
refine : Rat.num (↑p : ℚ) = Rat.num (↑q : ℚ)
⊢ p = q

Tactic:
refine ext <| Rat.ext ?_ hd

Premises used: Rat.ext, NNRat.ext
-- Module: Mathlib.Data.NNRat.Defs
Goal:
p q : ℚ≥0
hn : p.num = q.num
hd : p.den = q.den
⊢ Rat.num (↑p : ℚ) = Rat.num (↑q : ℚ)

Tactic:
simpa [num_coe]

Premises used: NNRat.num_coe
-- Module: Mathlib.Data.NNRat.Defs
Goal:
p : ℚ≥0
⊢ p.num = p.num ∧ p.den = p.den

Tactic:
⟨rfl, rfl⟩

Premises used: And.intro, rfl
-- Module: Mathlib.Data.NNRat.Defs
Goal:
p : ℚ≥0
⊢ p.num = p.num ∧ p.den = p.den

Tactic:
exact ⟨rfl, rfl⟩
-- Module: Mathlib.Data.NNRat.Defs
Goal:
n d : ℕ
⊢ (↑(divNat n d) : ℚ) = Rat.divInt (↑n : ℤ) (↑d : ℤ)

Tactic:
rfl

Premises used: Rat.divInt, inline, dite, mkRat, rfl
-- Module: Mathlib.Data.NNRat.Defs
Goal:
n d : ℕ
⊢ Subtype.mk (p := fun (q : ℚ) ↦ 0 ≤ q) (Rat.divInt (↑n : ℤ) (↑d : ℤ)) ⋯ = divNat n d

Tactic:
rfl

Premises used: NNRat.divNat, rfl
-- Module: Mathlib.Data.NNRat.Defs
Goal:
n₁ n₂ d₁ d₂ : ℕ
h₁ : d₁ ≠ 0
h₂ : d₂ ≠ 0
rw : Eq (α := ℚ) (↑(divNat n₁ d₁) : ℚ) (↑(divNat n₂ d₂) : ℚ) ↔ n₁ * d₂ = n₂ * d₁
⊢ divNat n₁ d₁ = divNat n₂ d₂ ↔ n₁ * d₂ = n₂ * d₁

Tactic:
rw [← coe_inj]

Premises used: NNRat.coe_inj
-- Module: Mathlib.Data.NNRat.Defs
Goal:
n₁ n₂ d₁ d₂ : ℕ
h₁ : d₁ ≠ 0
h₂ : d₂ ≠ 0
simp : HMul.hMul (α := ℤ) (↑n₁ : ℤ) (↑d₂ : ℤ) = HMul.hMul (α := ℤ) (↑n₂ : ℤ) (↑d₁ : ℤ) ↔ n₁ * d₂ = n₂ * d₁
⊢ Eq (α := ℚ) (↑(divNat n₁ d₁) : ℚ) (↑(divNat n₂ d₂) : ℚ) ↔ n₁ * d₂ = n₂ * d₁

Tactic:
simp [Rat.mkRat_eq_iff, h₁, h₂]

Premises used: Rat.mkRat_eq_iff
-- Module: Mathlib.Data.NNRat.Defs
Goal:
n₁ n₂ d₁ d₂ : ℕ
h₁ : d₁ ≠ 0
h₂ : d₂ ≠ 0
norm_cast norm_cast₁ norm_cast₂ norm_cast₃ : n₁ * d₂ = n₂ * d₁ ↔ n₁ * d₂ = n₂ * d₁
⊢ HMul.hMul (α := ℤ) (↑n₁ : ℤ) (↑d₂ : ℤ) = HMul.hMul (α := ℤ) (↑n₂ : ℤ) (↑d₁ : ℤ) ↔ n₁ * d₂ = n₂ * d₁

Tactic:
norm_cast
-- Module: Mathlib.Data.NNRat.Defs
Goal:
n : ℕ
⊢ divNat n 0 = 0

Tactic:
simp [divNat]

Premises used: NNRat.divNat
-- Module: Mathlib.Data.NNRat.Defs
Goal:
q : ℚ≥0
rw : (↑(divNat q.num q.den) : ℚ) = mkRat (Rat.num (↑q : ℚ)) (Rat.den (↑q : ℚ))
⊢ Eq (α := ℚ) (↑(divNat q.num q.den) : ℚ) (↑q : ℚ)

Tactic:
rw [← (q : ℚ).mkRat_num_den']

Premises used: Rat.mkRat_num_den', NNRat.cast
-- Module: Mathlib.Data.NNRat.Defs
Goal:
q : ℚ≥0
⊢ (↑(divNat q.num q.den) : ℚ) = mkRat (Rat.num (↑q : ℚ)) (Rat.den (↑q : ℚ))

Tactic:
simp [num_coe, den_coe]

Premises used: NNRat.den_coe, NNRat.num_coe
-- Module: Mathlib.Data.NNRat.Defs
Goal:
n : ℕ
⊢ (↑n : ℚ≥0) = divNat n 1

Tactic:
(num_divNat_den _).symm

Premises used: NNRat.num, NNRat.den, Int.natAbs, NNRat.num_divNat_den, Eq.symm
-- Module: Mathlib.Data.NNRat.Defs
Goal:
n₁ n₂ d₁ d₂ : ℕ
a : Eq (α := ℚ) (↑(divNat n₁ d₁ * divNat n₂ d₂) : ℚ) (↑(divNat (n₁ * n₂) (d₁ * d₂)) : ℚ)
⊢ divNat n₁ d₁ * divNat n₂ d₂ = divNat (n₁ * n₂) (d₁ * d₂)

Tactic:
ext
-- Module: Mathlib.Data.NNRat.Defs
Goal:
n₁ n₂ d₁ d₂ : ℕ
a :
  Rat.divInt (↑n₁ : ℤ) (↑d₁ : ℤ) * Rat.divInt (↑n₂ : ℤ) (↑d₂ : ℤ) =
    Rat.divInt (HMul.hMul (α := ℤ) (↑n₁ : ℤ) (↑n₂ : ℤ)) (HMul.hMul (α := ℤ) (↑d₁ : ℤ) (↑d₂ : ℤ))
⊢ Eq (α := ℚ) (↑(divNat n₁ d₁ * divNat n₂ d₂) : ℚ) (↑(divNat (n₁ * n₂) (d₁ * d₂)) : ℚ)

Tactic:
push_cast
-- Module: Mathlib.Data.NNRat.Defs
Goal:
n₁ n₂ d₁ d₂ : ℕ
⊢ Rat.divInt (↑n₁ : ℤ) (↑d₁ : ℤ) * Rat.divInt (↑n₂ : ℤ) (↑d₂ : ℤ) =
    Rat.divInt (HMul.hMul (α := ℤ) (↑n₁ : ℤ) (↑n₂ : ℤ)) (HMul.hMul (α := ℤ) (↑d₁ : ℤ) (↑d₂ : ℤ))

Tactic:
Rat.divInt_mul_divInt _ _

Premises used: Rat.divInt_mul_divInt
-- Module: Mathlib.Data.NNRat.Defs
Goal:
n₁ n₂ d₁ d₂ : ℕ
⊢ Rat.divInt (↑n₁ : ℤ) (↑d₁ : ℤ) * Rat.divInt (↑n₂ : ℤ) (↑d₂ : ℤ) =
    Rat.divInt (HMul.hMul (α := ℤ) (↑n₁ : ℤ) (↑n₂ : ℤ)) (HMul.hMul (α := ℤ) (↑d₁ : ℤ) (↑d₂ : ℤ))

Tactic:
exact Rat.divInt_mul_divInt _ _

Premises used: Rat.divInt_mul_divInt
-- Module: Mathlib.Data.NNRat.Defs
Goal:
a : ℕ
ha : a ≠ 0
n d : ℕ
a₁ : Eq (α := ℚ) (↑(divNat (a * n) (a * d)) : ℚ) (↑(divNat n d) : ℚ)
⊢ divNat (a * n) (a * d) = divNat n d

Tactic:
ext
-- Module: Mathlib.Data.NNRat.Defs
Goal:
a : ℕ
ha : a ≠ 0
n d : ℕ
a₁ :
  Rat.divInt (HMul.hMul (α := ℤ) (↑a : ℤ) (↑n : ℤ)) (HMul.hMul (α := ℤ) (↑a : ℤ) (↑d : ℤ)) =
    Rat.divInt (↑n : ℤ) (↑d : ℤ)
⊢ Eq (α := ℚ) (↑(divNat (a * n) (a * d)) : ℚ) (↑(divNat n d) : ℚ)

Tactic:
push_cast
-- Module: Mathlib.Data.NNRat.Defs
Goal:
a : ℕ
ha : a ≠ 0
n d : ℕ
⊢ Rat.divInt (HMul.hMul (α := ℤ) (↑a : ℤ) (↑n : ℤ)) (HMul.hMul (α := ℤ) (↑a : ℤ) (↑d : ℤ)) =
    Rat.divInt (↑n : ℤ) (↑d : ℤ)

Tactic:
Rat.divInt_mul_left (mod_cast ha)

Premises used: congrArg, cast, Ne, Nat.cast, Rat.divInt_mul_left, Nat.cast_inj._simp_1, Nat.cast_zero, Eq.symm, Not, Eq.trans
-- Module: Mathlib.Data.NNRat.Defs
Goal:
a : ℕ
ha : a ≠ 0
n d : ℕ
⊢ Rat.divInt (HMul.hMul (α := ℤ) (↑a : ℤ) (↑n : ℤ)) (HMul.hMul (α := ℤ) (↑a : ℤ) (↑d : ℤ)) =
    Rat.divInt (↑n : ℤ) (↑d : ℤ)

Tactic:
exact Rat.divInt_mul_left (mod_cast ha)

Premises used: Rat.divInt_mul_left
-- Module: Mathlib.Data.NNRat.Defs
Goal:
a : ℕ
ha : a ≠ 0
n d : ℕ
a₁ : Eq (α := ℚ) (↑(divNat (n * a) (d * a)) : ℚ) (↑(divNat n d) : ℚ)
⊢ divNat (n * a) (d * a) = divNat n d

Tactic:
ext
-- Module: Mathlib.Data.NNRat.Defs
Goal:
a : ℕ
ha : a ≠ 0
n d : ℕ
a₁ :
  Rat.divInt (HMul.hMul (α := ℤ) (↑n : ℤ) (↑a : ℤ)) (HMul.hMul (α := ℤ) (↑d : ℤ) (↑a : ℤ)) =
    Rat.divInt (↑n : ℤ) (↑d : ℤ)
⊢ Eq (α := ℚ) (↑(divNat (n * a) (d * a)) : ℚ) (↑(divNat n d) : ℚ)

Tactic:
push_cast
-- Module: Mathlib.Data.NNRat.Defs
Goal:
a : ℕ
ha : a ≠ 0
n d : ℕ
⊢ Rat.divInt (HMul.hMul (α := ℤ) (↑n : ℤ) (↑a : ℤ)) (HMul.hMul (α := ℤ) (↑d : ℤ) (↑a : ℤ)) =
    Rat.divInt (↑n : ℤ) (↑d : ℤ)

Tactic:
Rat.divInt_mul_right (mod_cast ha)

Premises used: congrArg, cast, Ne, Nat.cast, Nat.cast_inj._simp_1, Nat.cast_zero, Rat.divInt_mul_right, Eq.symm, Not, Eq.trans
-- Module: Mathlib.Data.NNRat.Defs
Goal:
a : ℕ
ha : a ≠ 0
n d : ℕ
⊢ Rat.divInt (HMul.hMul (α := ℤ) (↑n : ℤ) (↑a : ℤ)) (HMul.hMul (α := ℤ) (↑d : ℤ) (↑a : ℤ)) =
    Rat.divInt (↑n : ℤ) (↑d : ℤ)

Tactic:
exact Rat.divInt_mul_right (mod_cast ha)

Premises used: Rat.divInt_mul_right
-- Module: Mathlib.Data.NNRat.Defs
Goal:
q : ℚ≥0
a : Eq (α := ℚ) (↑(q * (↑q.den : ℚ≥0)) : ℚ) (↑(↑q.num : ℚ≥0) : ℚ)
⊢ q * (↑q.den : ℚ≥0) = (↑q.num : ℚ≥0)

Tactic:
ext
-- Module: Mathlib.Data.NNRat.Defs
Goal:
q : ℚ≥0
a : HMul.hMul (α := ℚ) (↑q : ℚ) (↑(↑(Rat.den (↑q : ℚ)) : ℤ) : ℚ) = (↑(Rat.num (↑q : ℚ)) : ℚ)
⊢ HMul.hMul (α := ℚ) (↑q : ℚ) (↑q.den : ℚ) = (↑q.num : ℚ)

Tactic:
rw [← Int.cast_natCast, ← den_coe, ← Int.cast_natCast q.num, ← num_coe]

Premises used: Int.cast_natCast, NNRat.den_coe, NNRat.num, NNRat.num_coe
-- Module: Mathlib.Data.NNRat.Defs
Goal:
q : ℚ≥0
⊢ HMul.hMul (α := ℚ) (↑q : ℚ) (↑(↑(Rat.den (↑q : ℚ)) : ℤ) : ℚ) = (↑(Rat.num (↑q : ℚ)) : ℚ)

Tactic:
Rat.mul_den_eq_num _

Premises used: Rat.mul_den_eq_num
-- Module: Mathlib.Data.NNRat.Defs
Goal:
q : ℚ≥0
⊢ HMul.hMul (α := ℚ) (↑q : ℚ) (↑(↑(Rat.den (↑q : ℚ)) : ℤ) : ℚ) = (↑(Rat.num (↑q : ℚ)) : ℚ)

Tactic:
exact Rat.mul_den_eq_num _

Premises used: Rat.mul_den_eq_num
-- Module: Mathlib.Data.NNRat.Defs
Goal:
q : ℚ≥0
rw : q * (↑q.den : ℚ≥0) = (↑q.num : ℚ≥0)
rw₁ rw₂ : Eq (α := ℚ≥0) (↑q.num : ℚ≥0) (↑q.num : ℚ≥0)
⊢ (↑q.den : ℚ≥0) * q = (↑q.num : ℚ≥0)

Tactic:
rw [mul_comm, mul_den_eq_num]

Premises used: NNRat.mul_den_eq_num, mul_comm
-- Module: Mathlib.Data.NNRat.Defs
Goal:
p q_1 : ℚ≥0
n₁ n₂ d₁ d₂ : ℕ
C : ℚ≥0 → Sort u
q : ℚ≥0
H : (n d : ℕ) → d ≠ 0 → n.Coprime d → C (divNat n d)
rw : C (divNat q.num q.den)
⊢ C q

Tactic:
rw [← q.num_divNat_den]

Premises used: NNRat.num_divNat_den
-- Module: Mathlib.Data.NNRat.Defs
Goal:
p q_1 : ℚ≥0
n₁ n₂ d₁ d₂ : ℕ
C : ℚ≥0 → Sort u
q : ℚ≥0
H : (n d : ℕ) → d ≠ 0 → n.Coprime d → C (divNat n d)
⊢ C (divNat q.num q.den)

Tactic:
exact H _ _ q.den_ne_zero q.coprime_num_den

Premises used: NNRat.den_ne_zero, NNRat.coprime_num_den
-- Module: Mathlib.Data.NNRat.Defs
Goal:
q r : ℚ≥0
a : Eq (α := ℚ) (↑(q + r) : ℚ) (↑(divNat (q.num * r.den + r.num * q.den) (q.den * r.den)) : ℚ)
⊢ q + r = divNat (q.num * r.den + r.num * q.den) (q.den * r.den)

Tactic:
ext
-- Module: Mathlib.Data.NNRat.Defs
Goal:
q r : ℚ≥0
⊢ Eq (α := ℚ) (↑(q + r) : ℚ) (↑(divNat (q.num * r.den + r.num * q.den) (q.den * r.den)) : ℚ)

Tactic:
simp [Rat.add_def', Rat.mkRat_eq_divInt, num_coe, den_coe]

Premises used: Rat.add_def', NNRat.den_coe, Rat.mkRat_eq_divInt, NNRat.num_coe
-- Module: Mathlib.Data.NNRat.Defs
Goal:
q r : ℚ≥0
a : Eq (α := ℚ) (↑(q * r) : ℚ) (↑(divNat (q.num * r.num) (q.den * r.den)) : ℚ)
⊢ q * r = divNat (q.num * r.num) (q.den * r.den)

Tactic:
ext
-- Module: Mathlib.Data.NNRat.Defs
Goal:
q r : ℚ≥0
⊢ Eq (α := ℚ) (↑(q * r) : ℚ) (↑(divNat (q.num * r.num) (q.den * r.den)) : ℚ)

Tactic:
simp [Rat.mul_eq_mkRat, Rat.mkRat_eq_divInt, num_coe, den_coe]

Premises used: NNRat.den_coe, Rat.mul_eq_mkRat, Rat.mkRat_eq_divInt, NNRat.num_coe
-- Module: Mathlib.Data.NNRat.Defs
Goal:
p q : ℚ≥0
rw :
  Rat.num (↑p : ℚ) * (↑(Rat.den (↑q : ℚ)) : ℤ) < Rat.num (↑q : ℚ) * (↑(Rat.den (↑p : ℚ)) : ℤ) ↔
    p.num * q.den < q.num * p.den
⊢ p < q ↔ p.num * q.den < q.num * p.den

Tactic:
rw [← NNRat.coe_lt_coe, Rat.lt_iff]

Premises used: NNRat.coe_lt_coe, Rat.lt_iff
-- Module: Mathlib.Data.NNRat.Defs
Goal:
p q : ℚ≥0
norm_cast norm_cast₁ norm_cast₂ norm_cast₃ : p.num * q.den < q.num * p.den ↔ p.num * q.den < q.num * p.den
⊢ Rat.num (↑p : ℚ) * (↑(Rat.den (↑q : ℚ)) : ℤ) < Rat.num (↑q : ℚ) * (↑(Rat.den (↑p : ℚ)) : ℤ) ↔
    p.num * q.den < q.num * p.den

Tactic:
norm_cast
-- Module: Mathlib.Data.NNRat.Defs
Goal:
p q : ℚ≥0
rw :
  Rat.num (↑p : ℚ) * (↑(Rat.den (↑q : ℚ)) : ℤ) ≤ Rat.num (↑q : ℚ) * (↑(Rat.den (↑p : ℚ)) : ℤ) ↔
    p.num * q.den ≤ q.num * p.den
⊢ p ≤ q ↔ p.num * q.den ≤ q.num * p.den

Tactic:
rw [← NNRat.coe_le_coe, Rat.le_iff]

Premises used: NNRat.coe_le_coe, Rat.le_iff
-- Module: Mathlib.Data.NNRat.Defs
Goal:
p q : ℚ≥0
norm_cast norm_cast₁ norm_cast₂ norm_cast₃ : p.num * q.den ≤ q.num * p.den ↔ p.num * q.den ≤ q.num * p.den
⊢ Rat.num (↑p : ℚ) * (↑(Rat.den (↑q : ℚ)) : ℤ) ≤ Rat.num (↑q : ℚ) * (↑(Rat.den (↑p : ℚ)) : ℤ) ↔
    p.num * q.den ≤ q.num * p.den

Tactic:
norm_cast
-- Module: Mathlib.Data.NNRat.Defs
Goal:
a b : ℚ≥0
⊢ a = b ↔ Eq (α := ℚ) (↑a : ℚ) (↑b : ℚ)

Tactic:
NNRat.coe_inj.symm

Premises used: NNRat.coe_inj, Iff.symm
-- Module: Mathlib.Data.NNRat.Defs
Goal:
a b : ℚ≥0
⊢ a ≤ b ↔ LE.le (α := ℚ) (↑a : ℚ) (↑b : ℚ)

Tactic:
NNRat.coe_le_coe.symm

Premises used: NNRat.coe_le_coe, Iff.symm
-- Module: Mathlib.Data.NNRat.Defs
Goal:
a b : ℚ≥0
⊢ a < b ↔ LT.lt (α := ℚ) (↑a : ℚ) (↑b : ℚ)

Tactic:
NNRat.coe_lt_coe.symm

Premises used: NNRat.coe_lt_coe, Iff.symm
-- Module: Mathlib.Data.NNRat.Defs
Goal:
a b : ℚ≥0
⊢ a ≠ b ↔ Ne (α := ℚ) (↑a : ℚ) (↑b : ℚ)

Tactic:
NNRat.ne_iff.symm

Premises used: NNRat.ne_iff, Iff.symm
-- Module: Mathlib.Data.NNRat.Encodable
Goal:
x : ℚ≥0
num : ℤ
den : ℕ
den_nz : den ≠ 0
reduced : num.natAbs.Coprime den
hq : 0 ≤ { num := num, den := den, den_nz := den_nz, reduced := reduced : ℚ }
⊢ 0 ≤ num

Tactic:
Rat.num_nonneg.mpr hq

Premises used: Iff.mpr, Rat.num_nonneg
-- Module: Mathlib.Data.NNRat.Encodable
Goal:
x : ℚ≥0
num : ℤ
den : ℕ
den_nz : den ≠ 0
reduced : num.natAbs.Coprime den
hq : 0 ≤ { num := num, den := den, den_nz := den_nz, reduced := reduced : ℚ }
lift :
  ∀ (num : ℕ) (reduced : (Int.natAbs (↑num : ℤ)).Coprime den)
    (hq : 0 ≤ { num := (↑num : ℤ), den := den, den_nz := den_nz, reduced := reduced : ℚ }),
    (fun (x : (n : ℕ) × { d : ℕ // 0 < d ∧ n.Coprime d }) ↦
          (match (motive := (n : ℕ) × { d : ℕ // 0 < d ∧ n.Coprime d } → ℚ≥0) x with
            | ⟨num, ⟨den, prop⟩⟩ =>
              Subtype.mk (p := fun (q : ℚ) ↦ 0 ≤ q) { num := (↑num : ℤ), den := den, den_nz := ⋯, reduced := ⋯ } ⋯ :
            ℚ≥0))
        ((fun (q : ℚ≥0) ↦
            (Sigma.mk (β := fun (n : ℕ) ↦ { d : ℕ // 0 < d ∧ n.Coprime d }) q.num
                (Subtype.mk (p := fun (d : ℕ) ↦ 0 < d ∧ q.num.Coprime d) q.den ⋯) :
              (n : ℕ) × { d : ℕ // 0 < d ∧ n.Coprime d }))
          (Subtype.mk (p := fun (q : ℚ) ↦ 0 ≤ q) { num := (↑num : ℤ), den := den, den_nz := den_nz, reduced := reduced }
            hq)) =
      Subtype.mk (p := fun (q : ℚ) ↦ 0 ≤ q) { num := (↑num : ℤ), den := den, den_nz := den_nz, reduced := reduced : ℚ }
        hq
⊢ (fun (x : (n : ℕ) × { d : ℕ // 0 < d ∧ n.Coprime d }) ↦
        (match (motive := (n : ℕ) × { d : ℕ // 0 < d ∧ n.Coprime d } → ℚ≥0) x with
          | ⟨num, ⟨den, prop⟩⟩ =>
            Subtype.mk (p := fun (q : ℚ) ↦ 0 ≤ q) { num := (↑num : ℤ), den := den, den_nz := ⋯, reduced := ⋯ } ⋯ :
          ℚ≥0))
      ((fun (q : ℚ≥0) ↦
          (Sigma.mk (β := fun (n : ℕ) ↦ { d : ℕ // 0 < d ∧ n.Coprime d }) q.num
              (Subtype.mk (p := fun (d : ℕ) ↦ 0 < d ∧ q.num.Coprime d) q.den ⋯) :
            (n : ℕ) × { d : ℕ // 0 < d ∧ n.Coprime d }))
        (Subtype.mk (p := fun (q : ℚ) ↦ 0 ≤ q) { num := num, den := den, den_nz := den_nz, reduced := reduced } hq)) =
    Subtype.mk (p := fun (q : ℚ) ↦ 0 ≤ q) { num := num, den := den, den_nz := den_nz, reduced := reduced : ℚ } hq

Tactic:
lift num to ℕ using Rat.num_nonneg.mpr hq

Premises used: Iff.mpr, Rat.num_nonneg
-- Module: Mathlib.Data.NNRat.Encodable
Goal:
x : ℚ≥0
den : ℕ
den_nz : den ≠ 0
num : ℕ
reduced : (Int.natAbs (↑num : ℤ)).Coprime den
hq : 0 ≤ { num := (↑num : ℤ), den := den, den_nz := den_nz, reduced := reduced : ℚ }
⊢ (fun (x : (n : ℕ) × { d : ℕ // 0 < d ∧ n.Coprime d }) ↦
        (match (motive := (n : ℕ) × { d : ℕ // 0 < d ∧ n.Coprime d } → ℚ≥0) x with
          | ⟨num, ⟨den, prop⟩⟩ =>
            Subtype.mk (p := fun (q : ℚ) ↦ 0 ≤ q) { num := (↑num : ℤ), den := den, den_nz := ⋯, reduced := ⋯ } ⋯ :
          ℚ≥0))
      ((fun (q : ℚ≥0) ↦
          (Sigma.mk (β := fun (n : ℕ) ↦ { d : ℕ // 0 < d ∧ n.Coprime d }) q.num
              (Subtype.mk (p := fun (d : ℕ) ↦ 0 < d ∧ q.num.Coprime d) q.den ⋯) :
            (n : ℕ) × { d : ℕ // 0 < d ∧ n.Coprime d }))
        (Subtype.mk (p := fun (q : ℚ) ↦ 0 ≤ q) { num := (↑num : ℤ), den := den, den_nz := den_nz, reduced := reduced }
          hq)) =
    Subtype.mk (p := fun (q : ℚ) ↦ 0 ≤ q) { num := (↑num : ℤ), den := den, den_nz := den_nz, reduced := reduced : ℚ } hq

Tactic:
rfl
-- Module: Mathlib.Data.NNRat.Floor
Goal:
a : ℚ≥0
h : a < 0
⊢ ⌊(↑a : ℚ)⌋₊ = 0

Tactic:
simpa using h.trans zero_lt_one

Premises used: zero_lt_one, LT.lt.trans
-- Module: Mathlib.Data.NNRat.Floor
Goal:
a : ℚ≥0
n : ℕ
h : 0 ≤ a
rw : (↑n : ℚ) ≤ (↑a : ℚ) ↔ LE.le (α := ℚ) (↑(↑n : ℚ≥0) : ℚ) (↑a : ℚ)
rw₁ : 0 ≤ (↑a : ℚ)
⊢ n ≤ ⌊(↑a : ℚ)⌋₊ ↔ (↑n : ℚ≥0) ≤ a

Tactic:
rw [← NNRat.coe_le_coe, Nat.le_floor_iff]

Premises used: Nat.le_floor_iff, NNRat.coe_le_coe
-- Module: Mathlib.Data.NNRat.Floor
Goal:
a : ℚ≥0
n : ℕ
h : 0 ≤ a
norm_cast norm_cast₁ norm_cast₂ norm_cast₃ : (↑n : ℚ) ≤ (↑a : ℚ) ↔ (↑n : ℚ≥0) ≤ a
⊢ (↑n : ℚ) ≤ (↑a : ℚ) ↔ LE.le (α := ℚ) (↑(↑n : ℚ≥0) : ℚ) (↑a : ℚ)

Tactic:
norm_cast
-- Module: Mathlib.Data.NNRat.Floor
Goal:
a : ℚ≥0
n : ℕ
h : 0 ≤ a
norm_cast norm_cast₁ norm_cast₂ norm_cast₃ : 0 ≤ (↑a : ℚ)
⊢ 0 ≤ (↑a : ℚ)

Tactic:
norm_cast
-- Module: Mathlib.Data.NNRat.Floor
Goal:
a : ℚ≥0
b : ℕ
rw : (↑a : ℚ) ≤ (↑b : ℚ) ↔ LE.le (α := ℚ) (↑a : ℚ) (↑(↑b : ℚ≥0) : ℚ)
⊢ (fun (q : ℚ≥0) ↦ ⌈(↑q : ℚ)⌉₊) a ≤ b ↔ a ≤ (↑b : ℚ≥0)

Tactic:
rw [← NNRat.coe_le_coe, Nat.ceil_le]

Premises used: NNRat.coe_le_coe, Nat.ceil_le
-- Module: Mathlib.Data.NNRat.Floor
Goal:
a : ℚ≥0
b : ℕ
norm_cast norm_cast₁ norm_cast₂ norm_cast₃ : (↑a : ℚ) ≤ (↑b : ℚ) ↔ a ≤ (↑b : ℚ≥0)
⊢ (↑a : ℚ) ≤ (↑b : ℚ) ↔ LE.le (α := ℚ) (↑a : ℚ) (↑(↑b : ℚ≥0) : ℚ)

Tactic:
norm_cast
-- Module: Mathlib.Data.NNRat.Floor
Goal:
q : ℚ≥0
⊢ Nat.floor (α := ℚ) (↑q : ℚ) = ⌊q⌋₊

Tactic:
rfl

Premises used: Nat.floor, Int.toNat, rfl
-- Module: Mathlib.Data.NNRat.Floor
Goal:
q : ℚ≥0
⊢ Nat.ceil (α := ℚ) (↑q : ℚ) = ⌈q⌉₊

Tactic:
rfl

Premises used: Nat.ceil, Int.toNat, rfl
-- Module: Mathlib.Data.NNRat.Floor
Goal:
q : ℚ≥0
⊢ (↑⌊q⌋₊ : ℤ) = Int.floor (α := ℚ) (↑q : ℚ)

Tactic:
Int.natCast_floor_eq_floor q.coe_nonneg

Premises used: Int.natCast_floor_eq_floor, NNRat.coe_nonneg, Nat.floor, Int.toNat
-- Module: Mathlib.Data.NNRat.Floor
Goal:
q : ℚ≥0
⊢ (↑⌈q⌉₊ : ℤ) = Int.ceil (α := ℚ) (↑q : ℚ)

Tactic:
Int.natCast_ceil_eq_ceil q.coe_nonneg

Premises used: Nat.ceil, NNRat.coe_nonneg, Int.natCast_ceil_eq_ceil, Int.toNat
-- Module: Mathlib.Data.NNRat.Floor
Goal:
q : ℚ≥0
rw : Eq (α := ℤ) (↑⌊q⌋₊ : ℤ) (↑(q.num / q.den) : ℤ)
rw₁ : Int.floor (α := ℚ) (↑q : ℚ) = (↑(q.num / q.den) : ℤ)
rw₂ : Rat.num (↑q : ℚ) / (↑(Rat.den (↑q : ℚ)) : ℤ) = (↑(q.num / q.den) : ℤ)
rw₃ : Rat.num (↑q : ℚ) / (↑(Rat.den (↑q : ℚ)) : ℤ) = HDiv.hDiv (α := ℤ) (↑q.num : ℤ) (↑q.den : ℤ)
rw₄ : Rat.num (↑q : ℚ) / (↑q.den : ℤ) = HDiv.hDiv (α := ℤ) (↑q.num : ℤ) (↑q.den : ℤ)
rw₅ rw₆ : HDiv.hDiv (α := ℤ) (↑q.num : ℤ) (↑q.den : ℤ) = HDiv.hDiv (α := ℤ) (↑q.num : ℤ) (↑q.den : ℤ)
⊢ ⌊q⌋₊ = q.num / q.den

Tactic:
rw [← Int.natCast_inj, NNRat.coe_floor, Rat.floor_def', Int.natCast_ediv, den_coe, num_coe]

Premises used: NNRat.coe_floor, NNRat.den_coe, Int.natCast_ediv, Rat.floor_def', NNRat.num_coe, Int.natCast_inj
-- Module: Mathlib.Data.NNRat.Floor
Goal:
K : Type u_1
inst : Semifield K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : FloorSemiring K
x : ℚ≥0
⊢ Nat.floor.{u_1} (α := K) (↑x : K) = ⌊x⌋₊

Tactic:
(Nat.floor_eq_iff x.cast_nonneg).2 (mod_cast (Nat.floor_eq_iff x.cast_nonneg).1 (Eq.refl ⌊x⌋₊))

Premises used: Iff.mpr, Nat.floor_eq_iff, congrArg, Nat.cast_add._simp_1, cast, NNRat.cast_nonneg, NNRat.natCast_le_cast._simp_1, LE.le, Nat.cast, And, HAdd.hAdd, congr, LT.lt, Iff.mp, Nat.floor, Eq.refl, NNRat.cast_lt_natCast._simp_1, OfNat.ofNat, Eq.symm, NNRat.cast, Nat.cast_one, Eq.trans
-- Module: Mathlib.Data.NNRat.Floor
Goal:
K : Type u_1
inst : Semifield K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : FloorSemiring K
x : ℚ≥0
inl : Nat.ceil.{u_1} (α := K) (↑0 : K) = Nat.ceil (α := ℚ≥0) 0
inr : ∀ (hx : x ≠ 0), Nat.ceil.{u_1} (α := K) (↑x : K) = ⌈x⌉₊
⊢ Nat.ceil.{u_1} (α := K) (↑x : K) = ⌈x⌉₊

Tactic:
obtain rfl | hx := eq_or_ne x 0

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Data.NNRat.Floor
Goal:
K : Type u_1
inst : Semifield K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : FloorSemiring K
⊢ Nat.ceil.{u_1} (α := K) (↑0 : K) = Nat.ceil (α := ℚ≥0) 0

Tactic:
simp
-- Module: Mathlib.Data.NNRat.Floor
Goal:
K : Type u_1
inst : Semifield K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : FloorSemiring K
x : ℚ≥0
hx : x ≠ 0
⊢ Nat.ceil.{u_1} (α := K) (↑x : K) = ⌈x⌉₊

Tactic:
(Nat.ceil_eq_iff ?_).2 (mod_cast (Nat.ceil_eq_iff ?_).1 (Eq.refl ⌈x⌉₊))

Premises used: Iff.mpr, congrArg, cast, And, Nat.ceil, congr, Iff.mp, NNRat.natCast_lt_cast._simp_1, Eq.refl, Eq.symm, Nat.ceil_eq_iff, NNRat.cast_le_natCast._simp_1
-- Module: Mathlib.Data.NNRat.Floor
Goal:
K : Type u_1
inst : Semifield K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : FloorSemiring K
x : ℚ≥0
hx : x ≠ 0
inr inr₁ : ⌈x⌉₊ ≠ 0
⊢ Nat.ceil.{u_1} (α := K) (↑x : K) = ⌈x⌉₊

Tactic:
refine (Nat.ceil_eq_iff ?_).2 (mod_cast (Nat.ceil_eq_iff ?_).1 (Eq.refl ⌈x⌉₊))

Premises used: Iff.mpr, Nat.ceil_eq_iff
-- Module: Mathlib.Data.NNRat.Floor
Goal:
K : Type u_1
inst : Semifield K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : FloorSemiring K
x : ℚ≥0
hx : x ≠ 0
⊢ ⌈x⌉₊ ≠ 0

Tactic:
simpa
-- Module: Mathlib.Data.NNRat.Floor
Goal:
K : Type u_1
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : FloorRing K
x : ℚ≥0
rw : LE.le.{u_1} (α := K) (↑(↑⌊x⌋₊ : ℤ) : K) (↑x : K) ∧ (↑x : K) < HAdd.hAdd (α := K) (↑(↑⌊x⌋₊ : ℤ) : K) 1
⊢ Int.floor.{u_1} (α := K) (↑x : K) = Int.floor (α := ℚ) (↑x : ℚ)

Tactic:
rw [Int.floor_eq_iff, ← coe_floor]

Premises used: NNRat.coe_floor, Int.floor_eq_iff
-- Module: Mathlib.Data.NNRat.Floor
Goal:
K : Type u_1
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : FloorRing K
x : ℚ≥0
norm_cast : LE.le.{u_1} (α := K) (↑⌊x⌋₊ : K) (↑x : K) ∧ LT.lt.{u_1} (α := K) (↑x : K) (↑(⌊x⌋₊ + 1) : K)
⊢ LE.le.{u_1} (α := K) (↑(↑⌊x⌋₊ : ℤ) : K) (↑x : K) ∧ (↑x : K) < HAdd.hAdd (α := K) (↑(↑⌊x⌋₊ : ℤ) : K) 1

Tactic:
norm_cast