awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.NNRat.Floor (goal)
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
⊢ Nat.ceil.{u_1} (α := K) (↑x : K) = ⌈x⌉₊
have inr : ∀ (hx : x ≠ 0), Nat.ceil.{u_1} (α := K) (↑x : K) = ⌈x⌉₊
Tactic: obtain rfl | hx := eq_or_ne x 0
-- Lean 4 proof step from Mathlib.Data.NNRat.Floor (goal)
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⌉₊
have inr : ⌈x⌉₊ ≠ 0
Tactic: refine (Nat.ceil_eq_iff ?_).2 (mod_cast (Nat.ceil_eq_iff ?_).1 (Eq.refl ⌈x⌉₊))
-- Lean 4 proof step from Mathlib.Data.NNRat.Floor (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : FloorRing K
x : ℚ≥0
⊢ Int.floor.{u_1} (α := K) (↑x : K) = Int.floor (α := ℚ) (↑x : ℚ)
have rw : LE.le.{u_1} (α := K) (↑(↑⌊x⌋₊ : ℤ) : K) (↑x : K) ∧ (↑x : K) < HAdd.hAdd (α := K) (↑(↑⌊x⌋₊ : ℤ) : K) 1
Tactic: rw [Int.floor_eq_iff, ← coe_floor]
-- Lean 4 proof step from Mathlib.Data.NNRat.Floor (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : FloorRing K
x : ℚ≥0
⊢ LE.le.{u_1} (α := K) (↑(↑⌊x⌋₊ : ℤ) : K) (↑x : K) ∧ (↑x : K) < HAdd.hAdd (α := K) (↑(↑⌊x⌋₊ : ℤ) : K) 1
have norm_cast : LE.le.{u_1} (α := K) (↑⌊x⌋₊ : K) (↑x : K) ∧ LT.lt.{u_1} (α := K) (↑x : K) (↑(⌊x⌋₊ + 1) : K)
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Data.NNRat.Floor (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : FloorRing K
x : ℚ≥0
⊢ LE.le.{u_1} (α := K) (↑⌊x⌋₊ : K) (↑x : K) ∧ LT.lt.{u_1} (α := K) (↑x : K) (↑(⌊x⌋₊ + 1) : K)
have norm_cast : (↑⌊x⌋₊ : ℚ≥0) ≤ x ∧ x < (↑(⌊x⌋₊ + 1) : ℚ≥0)
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Data.NNRat.Floor (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : FloorRing K
x : ℚ≥0
⊢ (↑⌊x⌋₊ : ℚ≥0) ≤ x ∧ x < (↑(⌊x⌋₊ + 1) : ℚ≥0)
have rw : (↑⌊x⌋₊ : ℚ≥0) ≤ x ∧ x < HAdd.hAdd (α := ℚ≥0) (↑⌊x⌋₊ : ℚ≥0) 1
Tactic: rw [Nat.cast_add_one, ← Nat.floor_eq_iff zero_le]
-- Lean 4 proof step from Mathlib.Data.NNRat.Floor (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : FloorRing K
x : ℚ≥0
rw : (↑⌊x⌋₊ : ℚ≥0) ≤ x ∧ x < HAdd.hAdd (α := ℚ≥0) (↑⌊x⌋₊ : ℚ≥0) 1
⊢ (↑⌊x⌋₊ : ℚ≥0) ≤ x ∧ x < (↑(⌊x⌋₊ + 1) : ℚ≥0)
have rw₁ : ⌊x⌋₊ = ⌊x⌋₊
Tactic: rw [Nat.cast_add_one, ← Nat.floor_eq_iff zero_le]
-- Lean 4 proof step from Mathlib.Data.NNRat.Floor (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : FloorRing K
x : ℚ≥0
⊢ Int.ceil.{u_1} (α := K) (↑x : K) = Int.ceil (α := ℚ) (↑x : ℚ)
have rw : (↑(↑⌈x⌉₊ : ℤ) : K) < HAdd.hAdd (α := K) (↑x : K) 1 ∧ LE.le.{u_1} (α := K) (↑x : K) (↑(↑⌈x⌉₊ : ℤ) : K)
Tactic: rw [Int.ceil_eq_iff, ← coe_ceil, sub_lt_iff_lt_add]
-- Lean 4 proof step from Mathlib.Data.NNRat.Floor (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : FloorRing K
x : ℚ≥0
⊢ (↑(↑⌈x⌉₊ : ℤ) : K) < HAdd.hAdd (α := K) (↑x : K) 1 ∧ LE.le.{u_1} (α := K) (↑x : K) (↑(↑⌈x⌉₊ : ℤ) : K)
have left : (↑(↑⌈x⌉₊ : ℤ) : K) < HAdd.hAdd (α := K) (↑x : K) 1
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.NNRat.Floor (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : FloorRing K
x : ℚ≥0
left : (↑(↑⌈x⌉₊ : ℤ) : K) < HAdd.hAdd (α := K) (↑x : K) 1
⊢ (↑(↑⌈x⌉₊ : ℤ) : K) < HAdd.hAdd (α := K) (↑x : K) 1 ∧ LE.le.{u_1} (α := K) (↑x : K) (↑(↑⌈x⌉₊ : ℤ) : K)
have right : LE.le.{u_1} (α := K) (↑x : K) (↑(↑⌈x⌉₊ : ℤ) : K)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.NNRat.Floor (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : FloorRing K
x : ℚ≥0
⊢ LE.le.{u_1} (α := K) (↑x : K) (↑(↑⌈x⌉₊ : ℤ) : K)
have right : x ≤ (↑⌈x⌉₊ : ℚ≥0)
Tactic: rw [Int.cast_natCast, NNRat.cast_le_natCast]
-- Lean 4 proof step from Mathlib.Data.NNRat.Floor (goal)
Goal:
R : Type u_1
inst : Semifield R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : FloorSemiring R
r : R
n d : ℕ
h : IsNNRat r n d
res : ℕ
hres : ⌈HDiv.hDiv (α := ℚ≥0) (↑n : ℚ≥0) (↑d : ℚ≥0)⌉₊ = res
⊢ IsNat ⌈r⌉₊ res
have out : ⌈r⌉₊ = (↑res : ℕ)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.NNRat.Floor (goal)
Goal:
R : Type u_1
inst : Semifield R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : FloorSemiring R
r : R
n d : ℕ
h : IsNNRat r n d
res : ℕ
hres : ⌈HDiv.hDiv (α := ℚ≥0) (↑n : ℚ≥0) (↑d : ℚ≥0)⌉₊ = res
⊢ ⌈r⌉₊ = (↑res : ℕ)
have out : ⌈HDiv.hDiv (α := R) (↑n : R) (↑d : R)⌉₊ =
  (↑(Nat.ceil.{u_1} (α := R) (↑(HDiv.hDiv (α := ℚ≥0) (↑n : ℚ≥0) (↑d : ℚ≥0)) : R)) : ℕ)
Tactic: rw [← hres, h.to_eq rfl rfl, ← @NNRat.ceil_cast R]
-- Lean 4 proof step from Mathlib.Data.NNRat.Floor (goal)
Goal:
R : Type u_1
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : FloorSemiring R
r : R
n d : ℕ
h : IsRat r (Int.negOfNat n) d
⊢ IsNat ⌈r⌉₊ 0
have out : ⌈r⌉₊ = (↑0 : ℕ)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.NNRat.Lemmas (goal)
Goal:
q : ℚ
⊢ q⁻¹.toNNRat = q.toNNRat⁻¹
have inl : ∀ (hq : q ≤ 0), q⁻¹.toNNRat = q.toNNRat⁻¹
Tactic: obtain hq | hq := le_total q 0
-- Lean 4 proof step from Mathlib.Data.NNRat.Lemmas (goal)
Goal:
q : ℚ
inl : ∀ (hq : q ≤ 0), q⁻¹.toNNRat = q.toNNRat⁻¹
⊢ q⁻¹.toNNRat = q.toNNRat⁻¹
have inr : ∀ (hq : 0 ≤ q), q⁻¹.toNNRat = q.toNNRat⁻¹
Tactic: obtain hq | hq := le_total q 0
-- Lean 4 proof step from Mathlib.Data.NNRat.Lemmas (goal)
Goal:
q : ℚ
hq : q ≤ 0
⊢ q⁻¹.toNNRat = q.toNNRat⁻¹
have inl : q⁻¹.toNNRat = 0⁻¹
Tactic: rw [toNNRat_eq_zero.mpr hq, inv_zero, toNNRat_eq_zero.mpr (inv_nonpos.mpr hq)]
-- Lean 4 proof step from Mathlib.Data.NNRat.Lemmas (goal)
Goal:
q : ℚ
hq : q ≤ 0
inl : q⁻¹.toNNRat = 0⁻¹
⊢ q⁻¹.toNNRat = q.toNNRat⁻¹
have inl₁ : q⁻¹.toNNRat = 0
Tactic: rw [toNNRat_eq_zero.mpr hq, inv_zero, toNNRat_eq_zero.mpr (inv_nonpos.mpr hq)]
-- Lean 4 proof step from Mathlib.Data.NNRat.Lemmas (goal)
Goal:
q : ℚ
hq : q ≤ 0
inl : q⁻¹.toNNRat = 0⁻¹
inl₁ : q⁻¹.toNNRat = 0
⊢ q⁻¹.toNNRat = q.toNNRat⁻¹
have inl₂ : Eq (α := ℚ≥0) 0 0
Tactic: rw [toNNRat_eq_zero.mpr hq, inv_zero, toNNRat_eq_zero.mpr (inv_nonpos.mpr hq)]
-- Lean 4 proof step from Mathlib.Data.NNRat.Lemmas (goal)
Goal:
q : ℚ
hq : 0 ≤ q
⊢ q⁻¹.toNNRat = q.toNNRat⁻¹
have inr : toNNRat (↑q.toNNRat : ℚ)⁻¹ = q.toNNRat⁻¹
Tactic: nth_rw 1 [← Rat.coe_toNNRat q hq]
-- Lean 4 proof step from Mathlib.Data.NNRat.Lemmas (goal)
Goal:
q : ℚ
hq : 0 ≤ q
⊢ toNNRat (↑q.toNNRat : ℚ)⁻¹ = q.toNNRat⁻¹
have inr : toNNRat (↑q.toNNRat⁻¹ : ℚ) = q.toNNRat⁻¹
Tactic: rw [← coe_inv, toNNRat_coe]
-- Lean 4 proof step from Mathlib.Data.NNRat.Lemmas (goal)
Goal:
q : ℚ
hq : 0 ≤ q
inr : toNNRat (↑q.toNNRat⁻¹ : ℚ) = q.toNNRat⁻¹
⊢ toNNRat (↑q.toNNRat : ℚ)⁻¹ = q.toNNRat⁻¹
have inr₁ : q.toNNRat⁻¹ = q.toNNRat⁻¹
Tactic: rw [← coe_inv, toNNRat_coe]
-- Lean 4 proof step from Mathlib.Data.NNRat.Lemmas (goal)
Goal:
p q : ℚ
hp : 0 ≤ p
⊢ (p / q).toNNRat = p.toNNRat / q.toNNRat
have rw : (p * q⁻¹).toNNRat = p.toNNRat / q.toNNRat
Tactic: rw [div_eq_mul_inv, div_eq_mul_inv, ← toNNRat_inv, ← toNNRat_mul hp]
-- Lean 4 proof step from Mathlib.Data.NNRat.Lemmas (goal)
Goal:
p q : ℚ
hp : 0 ≤ p
rw : (p * q⁻¹).toNNRat = p.toNNRat / q.toNNRat
⊢ (p / q).toNNRat = p.toNNRat / q.toNNRat
have rw₁ : (p * q⁻¹).toNNRat = p.toNNRat * q.toNNRat⁻¹
Tactic: rw [div_eq_mul_inv, div_eq_mul_inv, ← toNNRat_inv, ← toNNRat_mul hp]
-- Lean 4 proof step from Mathlib.Data.NNRat.Lemmas (goal)
Goal:
p q : ℚ
hp : 0 ≤ p
rw : (p * q⁻¹).toNNRat = p.toNNRat / q.toNNRat
rw₁ : (p * q⁻¹).toNNRat = p.toNNRat * q.toNNRat⁻¹
⊢ (p / q).toNNRat = p.toNNRat / q.toNNRat
have rw₂ : (p * q⁻¹).toNNRat = p.toNNRat * q⁻¹.toNNRat
Tactic: rw [div_eq_mul_inv, div_eq_mul_inv, ← toNNRat_inv, ← toNNRat_mul hp]
-- Lean 4 proof step from Mathlib.Data.NNRat.Lemmas (goal)
Goal:
p q : ℚ
hp : 0 ≤ p
rw : (p * q⁻¹).toNNRat = p.toNNRat / q.toNNRat
rw₁ : (p * q⁻¹).toNNRat = p.toNNRat * q.toNNRat⁻¹
rw₂ : (p * q⁻¹).toNNRat = p.toNNRat * q⁻¹.toNNRat
⊢ (p / q).toNNRat = p.toNNRat / q.toNNRat
have rw₃ : (p * q⁻¹).toNNRat = (p * q⁻¹).toNNRat
Tactic: rw [div_eq_mul_inv, div_eq_mul_inv, ← toNNRat_inv, ← toNNRat_mul hp]
-- Lean 4 proof step from Mathlib.Data.NNRat.Lemmas (goal)
Goal:
p q : ℚ
hq : 0 ≤ q
⊢ (p / q).toNNRat = p.toNNRat / q.toNNRat
have rw : (q⁻¹ * p).toNNRat = p.toNNRat / q.toNNRat
Tactic: rw [div_eq_inv_mul, div_eq_inv_mul, toNNRat_mul (inv_nonneg.2 hq), toNNRat_inv]
-- Lean 4 proof step from Mathlib.Data.NNRat.Lemmas (goal)
Goal:
p q : ℚ
hq : 0 ≤ q
rw : (q⁻¹ * p).toNNRat = p.toNNRat / q.toNNRat
⊢ (p / q).toNNRat = p.toNNRat / q.toNNRat
have rw₁ : (q⁻¹ * p).toNNRat = q.toNNRat⁻¹ * p.toNNRat
Tactic: rw [div_eq_inv_mul, div_eq_inv_mul, toNNRat_mul (inv_nonneg.2 hq), toNNRat_inv]
-- Lean 4 proof step from Mathlib.Data.NNRat.Lemmas (goal)
Goal:
p q : ℚ
hq : 0 ≤ q
rw : (q⁻¹ * p).toNNRat = p.toNNRat / q.toNNRat
rw₁ : (q⁻¹ * p).toNNRat = q.toNNRat⁻¹ * p.toNNRat
⊢ (p / q).toNNRat = p.toNNRat / q.toNNRat
have rw₂ : q⁻¹.toNNRat * p.toNNRat = q.toNNRat⁻¹ * p.toNNRat
Tactic: rw [div_eq_inv_mul, div_eq_inv_mul, toNNRat_mul (inv_nonneg.2 hq), toNNRat_inv]
-- Lean 4 proof step from Mathlib.Data.NNRat.Lemmas (goal)
Goal:
p q : ℚ
hq : 0 ≤ q
rw : (q⁻¹ * p).toNNRat = p.toNNRat / q.toNNRat
rw₁ : (q⁻¹ * p).toNNRat = q.toNNRat⁻¹ * p.toNNRat
rw₂ : q⁻¹.toNNRat * p.toNNRat = q.toNNRat⁻¹ * p.toNNRat
⊢ (p / q).toNNRat = p.toNNRat / q.toNNRat
have rw₃ : q.toNNRat⁻¹ * p.toNNRat = q.toNNRat⁻¹ * p.toNNRat
Tactic: rw [div_eq_inv_mul, div_eq_inv_mul, toNNRat_mul (inv_nonneg.2 hq), toNNRat_inv]
-- Lean 4 proof step from Mathlib.Data.NNRat.Lemmas (goal)
Goal:
q_1 : ℚ≥0
α : ℚ≥0 → Sort u_1
h : (m n : ℕ) → α (HDiv.hDiv (α := ℚ≥0) (↑m : ℚ≥0) (↑n : ℚ≥0))
q : ℚ≥0
⊢ α q
have rw : α (HDiv.hDiv (α := ℚ≥0) (↑q.num : ℚ≥0) (↑q.den : ℚ≥0))
Tactic: rw [← num_div_den q]
-- Lean 4 proof step from Mathlib.Data.NNRat.Lemmas (goal)
Goal:
q₁ q₂ : ℚ≥0
⊢ (q₁ * q₂).num = q₁.num * q₂.num / (q₁.num * q₂.num).gcd (q₁.den * q₂.den)
have zify : (↑(q₁ * q₂).num : ℤ) = HMul.hMul (α := ℤ) (↑q₁.num : ℤ) (↑q₂.num : ℤ) / (↑((q₁.num * q₂.num).gcd (q₁.den * q₂.den)) : ℤ)
Tactic: zify
-- Lean 4 proof step from Mathlib.Data.NNRat.Lemmas (goal)
Goal:
q₁ q₂ : ℚ≥0
⊢ (↑(q₁ * q₂).num : ℤ) =
    HMul.hMul (α := ℤ) (↑q₁.num : ℤ) (↑q₂.num : ℤ) / (↑((q₁.num * q₂.num).gcd (q₁.den * q₂.den)) : ℤ)
have h : (↑(q₁ * q₂).num : ℤ) = (HMul.hMul (α := ℚ) (↑q₁ : ℚ) (↑q₂ : ℚ)).num
Tactic: convert! Rat.mul_num q₁ q₂
-- Lean 4 proof step from Mathlib.Data.NNRat.Lemmas (goal)
Goal:
q₁ q₂ : ℚ≥0
h : (↑(q₁ * q₂).num : ℤ) = (HMul.hMul (α := ℚ) (↑q₁ : ℚ) (↑q₂ : ℚ)).num
⊢ (↑(q₁ * q₂).num : ℤ) =
    HMul.hMul (α := ℤ) (↑q₁.num : ℤ) (↑q₂.num : ℤ) / (↑((q₁.num * q₂.num).gcd (q₁.den * q₂.den)) : ℤ)
have h₁ : (↑q₁.num : ℤ) = Rat.num (↑q₁ : ℚ)
Tactic: convert! Rat.mul_num q₁ q₂
-- Lean 4 proof step from Mathlib.Data.NNRat.Lemmas (goal)
Goal:
q₁ q₂ : ℚ≥0
h : (↑(q₁ * q₂).num : ℤ) = (HMul.hMul (α := ℚ) (↑q₁ : ℚ) (↑q₂ : ℚ)).num
h₁ : (↑q₁.num : ℤ) = Rat.num (↑q₁ : ℚ)
⊢ (↑(q₁ * q₂).num : ℤ) =
    HMul.hMul (α := ℤ) (↑q₁.num : ℤ) (↑q₂.num : ℤ) / (↑((q₁.num * q₂.num).gcd (q₁.den * q₂.den)) : ℤ)
have h₂ : (↑q₂.num : ℤ) = Rat.num (↑q₂ : ℚ)
Tactic: convert! Rat.mul_num q₁ q₂
-- Lean 4 proof step from Mathlib.Data.NNRat.Lemmas (goal)
Goal:
q₁ q₂ : ℚ≥0
h : (↑(q₁ * q₂).num : ℤ) = (HMul.hMul (α := ℚ) (↑q₁ : ℚ) (↑q₂ : ℚ)).num
h₁ : (↑q₁.num : ℤ) = Rat.num (↑q₁ : ℚ)
h₂ : (↑q₂.num : ℤ) = Rat.num (↑q₂ : ℚ)
⊢ (↑(q₁ * q₂).num : ℤ) =
    HMul.hMul (α := ℤ) (↑q₁.num : ℤ) (↑q₂.num : ℤ) / (↑((q₁.num * q₂.num).gcd (q₁.den * q₂.den)) : ℤ)
have h₃ : q₁.num * q₂.num = (Rat.num (↑q₁ : ℚ) * Rat.num (↑q₂ : ℚ)).natAbs
Tactic: convert! Rat.mul_num q₁ q₂
-- Lean 4 proof step from Mathlib.Data.NNRat.Lemmas (goal)
Goal:
q₁ q₂ : ℚ≥0
⊢ (↑(q₁ * q₂).num : ℤ) = (HMul.hMul (α := ℚ) (↑q₁ : ℚ) (↑q₂ : ℚ)).num
have h : (q₁ * q₂).num = (q₁ * q₂).num
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Data.NNRat.Lemmas (goal)
Goal:
q₁ q₂ : ℚ≥0
⊢ (↑q₁.num : ℤ) = Rat.num (↑q₁ : ℚ)
have h : q₁.num = q₁.num
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Data.NNRat.Lemmas (goal)
Goal:
q₁ q₂ : ℚ≥0
⊢ (↑q₂.num : ℤ) = Rat.num (↑q₂ : ℚ)
have h : q₂.num = q₂.num
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Data.NNRat.Lemmas (goal)
Goal:
q₁ q₂ : ℚ≥0
⊢ q₁.num * q₂.num = (Rat.num (↑q₁ : ℚ) * Rat.num (↑q₂ : ℚ)).natAbs
have h : q₁.num * q₂.num = q₁.num * q₂.num
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Data.NNRat.Lemmas (goal)
Goal:
q₁ q₂ : ℚ≥0
⊢ (q₁ * q₂).den = q₁.den * q₂.den / (q₁.num * q₂.num).gcd (q₁.den * q₂.den)
have h : q₁.num * q₂.num = (Rat.num (↑q₁ : ℚ) * Rat.num (↑q₂ : ℚ)).natAbs
Tactic: convert! Rat.mul_den q₁ q₂
-- Lean 4 proof step from Mathlib.Data.NNRat.Lemmas (goal)
Goal:
q₁ q₂ : ℚ≥0
⊢ q₁.den * q₂.den = (q₁ * q₂).den * (q₁.num * q₂.num).gcd (q₁.den * q₂.den)
have h : q₁.num * q₂.num = (Rat.num (↑q₁ : ℚ) * Rat.num (↑q₂ : ℚ)).natAbs
Tactic: convert! Rat.den_mul_den_eq_den_mul_gcd q₁ q₂
-- Lean 4 proof step from Mathlib.Data.NNRat.Lemmas (goal)
Goal:
q₁ q₂ : ℚ≥0
⊢ q₁.num * q₂.num = (q₁ * q₂).num * (q₁.num * q₂.num).gcd (q₁.den * q₂.den)
have zify : HMul.hMul (α := ℤ) (↑q₁.num : ℤ) (↑q₂.num : ℤ) =
  HMul.hMul (α := ℤ) (↑(q₁ * q₂).num : ℤ) (↑((q₁.num * q₂.num).gcd (q₁.den * q₂.den)) : ℤ)
Tactic: zify
-- Lean 4 proof step from Mathlib.Data.NNRat.Lemmas (goal)
Goal:
q₁ q₂ : ℚ≥0
⊢ HMul.hMul (α := ℤ) (↑q₁.num : ℤ) (↑q₂.num : ℤ) =
    HMul.hMul (α := ℤ) (↑(q₁ * q₂).num : ℤ) (↑((q₁.num * q₂.num).gcd (q₁.den * q₂.den)) : ℤ)
have h : (↑q₁.num : ℤ) = Rat.num (↑q₁ : ℚ)
Tactic: convert! Rat.num_mul_num_eq_num_mul_gcd q₁ q₂
-- Lean 4 proof step from Mathlib.Data.NNRat.Lemmas (goal)
Goal:
q₁ q₂ : ℚ≥0
h : (↑q₁.num : ℤ) = Rat.num (↑q₁ : ℚ)
⊢ HMul.hMul (α := ℤ) (↑q₁.num : ℤ) (↑q₂.num : ℤ) =
    HMul.hMul (α := ℤ) (↑(q₁ * q₂).num : ℤ) (↑((q₁.num * q₂.num).gcd (q₁.den * q₂.den)) : ℤ)
have h₁ : (↑q₂.num : ℤ) = Rat.num (↑q₂ : ℚ)
Tactic: convert! Rat.num_mul_num_eq_num_mul_gcd q₁ q₂
-- Lean 4 proof step from Mathlib.Data.NNRat.Lemmas (goal)
Goal:
q₁ q₂ : ℚ≥0
h : (↑q₁.num : ℤ) = Rat.num (↑q₁ : ℚ)
h₁ : (↑q₂.num : ℤ) = Rat.num (↑q₂ : ℚ)
⊢ HMul.hMul (α := ℤ) (↑q₁.num : ℤ) (↑q₂.num : ℤ) =
    HMul.hMul (α := ℤ) (↑(q₁ * q₂).num : ℤ) (↑((q₁.num * q₂.num).gcd (q₁.den * q₂.den)) : ℤ)
have h₂ : (↑(q₁ * q₂).num : ℤ) = (HMul.hMul (α := ℚ) (↑q₁ : ℚ) (↑q₂ : ℚ)).num
Tactic: convert! Rat.num_mul_num_eq_num_mul_gcd q₁ q₂
-- Lean 4 proof step from Mathlib.Data.NNRat.Lemmas (goal)
Goal:
q₁ q₂ : ℚ≥0
h : (↑q₁.num : ℤ) = Rat.num (↑q₁ : ℚ)
h₁ : (↑q₂.num : ℤ) = Rat.num (↑q₂ : ℚ)
h₂ : (↑(q₁ * q₂).num : ℤ) = (HMul.hMul (α := ℚ) (↑q₁ : ℚ) (↑q₂ : ℚ)).num
⊢ HMul.hMul (α := ℤ) (↑q₁.num : ℤ) (↑q₂.num : ℤ) =
    HMul.hMul (α := ℤ) (↑(q₁ * q₂).num : ℤ) (↑((q₁.num * q₂.num).gcd (q₁.den * q₂.den)) : ℤ)
have h₃ : q₁.num * q₂.num = (Rat.num (↑q₁ : ℚ) * Rat.num (↑q₂ : ℚ)).natAbs
Tactic: convert! Rat.num_mul_num_eq_num_mul_gcd q₁ q₂
-- Lean 4 proof step from Mathlib.Data.NNReal.Basic (goal)
Goal:
ι : Type u_1
s : Finset ι
f : ι → ℝ
hf : ∀ i ∈ s, 0 ≤ f i
⊢ Real.toNNReal (∑ a ∈ s, f a) = ∑ a ∈ s, (f a).toNNReal
have rw : Eq (α := ℝ) (∑ i ∈ s, f i) (∑ i ∈ s, (↑(f i).toNNReal : ℝ))
Tactic: rw [← coe_inj, NNReal.coe_sum, Real.coe_toNNReal _ (Finset.sum_nonneg hf)]
-- Lean 4 proof step from Mathlib.Data.NNReal.Basic (goal)
Goal:
ι : Type u_1
s : Finset ι
f : ι → ℝ
hf : ∀ i ∈ s, 0 ≤ f i
x : ι
hxs : x ∈ s
⊢ f x = (↑(f x).toNNReal : ℝ)
have rw : f x = f x
Tactic: rw [Real.coe_toNNReal _ (hf x hxs)]
-- Lean 4 proof step from Mathlib.Data.NNReal.Basic (goal)
Goal:
ι : Type u_1
s : Finset ι
f : ι → ℝ
hf : ∀ a ∈ s, 0 ≤ f a
⊢ Real.toNNReal (∏ a ∈ s, f a) = ∏ a ∈ s, (f a).toNNReal
have rw : Eq (α := ℝ) (∏ i ∈ s, f i) (∏ a ∈ s, (↑(f a).toNNReal : ℝ))
Tactic: rw [← coe_inj, NNReal.coe_prod, Real.coe_toNNReal _ (Finset.prod_nonneg hf)]
-- Lean 4 proof step from Mathlib.Data.NNReal.Basic (goal)
Goal:
ι : Type u_1
s : Finset ι
f : ι → ℝ
hf : ∀ a ∈ s, 0 ≤ f a
x : ι
hxs : x ∈ s
⊢ f x = (↑(f x).toNNReal : ℝ)
have rw : f x = f x
Tactic: rw [Real.coe_toNNReal _ (hf x hxs)]
-- Lean 4 proof step from Mathlib.Data.NNReal.Basic (goal)
Goal:
ι : Sort u_2
ι' : Sort u_3
inst : Nonempty ι
inst_1 : Nonempty ι'
f : ι → ℝ≥0
g : ι' → ℝ≥0
a : ℝ≥0
h : ∀ (i : ι) (j : ι'), a ≤ f i + g j
⊢ a ≤ HAdd.hAdd (α := ℝ≥0) (⨅ (i : ι), f i) (⨅ (j : ι'), g j)
have rw : (↑a : ℝ) ≤ HAdd.hAdd (α := ℝ) (⨅ (i : ι), (↑(f i) : ℝ)) (⨅ (i : ι'), (↑(g i) : ℝ))
Tactic: rw [← NNReal.coe_le_coe, NNReal.coe_add, coe_iInf, coe_iInf]
-- Lean 4 proof step from Mathlib.Data.NNReal.Basic (goal)
Goal:
ι : Sort u_2
f : ι → ℕ
⊢ BddAbove (α := ℝ≥0) (range fun (x : ι) ↦ (↑(f x) : ℝ≥0)) ↔ BddAbove (range f)
have rw : BddAbove (α := ℝ≥0) (range fun (x : ι) ↦ (↑(f x) : ℝ≥0)) ↔ BddAbove (α := ℝ≥0) (range (Nat.cast ∘ f))
Tactic: rw [← bddAbove_natCast_image_iff, ← Set.range_comp]
-- Lean 4 proof step from Mathlib.Data.NNReal.Basic (goal)
Goal:
ι : Sort u_2
f : ι → ℝ≥0
a : ℝ≥0
⊢ iInf f * a = ⨅ (i : ι), f i * a
have rw : (⨅ (i : ι), (↑(f i) : ℝ)) * (↑a : ℝ) = ⨅ (i : ι), (↑(f i * a) : ℝ)
Tactic: rw [← coe_inj, NNReal.coe_mul, coe_iInf, coe_iInf]
-- Lean 4 proof step from Mathlib.Data.NNReal.Basic (goal)
Goal:
ι : Sort u_2
f : ι → ℝ≥0
a : ℝ≥0
⊢ a * ⨆ (i : ι), f i = ⨆ (i : ι), a * f i
have rw : (↑a : ℝ) * ⨆ (i : ι), (↑(f i) : ℝ) = ⨆ (i : ι), (↑(a * f i) : ℝ)
Tactic: rw [← coe_inj, NNReal.coe_mul, NNReal.coe_iSup, NNReal.coe_iSup]
-- Lean 4 proof step from Mathlib.Data.NNReal.Basic (goal)
Goal:
ι : Sort u_2
f : ι → ℝ≥0
a : ℝ≥0
⊢ (⨆ (i : ι), f i) * a = ⨆ (i : ι), f i * a
have rw : Eq (α := ℝ≥0) (⨆ (i : ι), a * f i) (⨆ (i : ι), f i * a)
Tactic: rw [mul_comm, mul_iSup]
-- Lean 4 proof step from Mathlib.Data.NNReal.Basic (goal)
Goal:
ι : Sort u_2
a g : ℝ≥0
h : ι → ℝ≥0
H : ∀ (j : ι), g * h j ≤ a
⊢ g * iSup h ≤ a
have rw : ⨆ (i : ι), g * h i ≤ a
Tactic: rw [mul_iSup]
-- Lean 4 proof step from Mathlib.Data.NNReal.Basic (goal)
Goal:
ι : Sort u_2
a : ℝ≥0
g : ι → ℝ≥0
h : ℝ≥0
H : ∀ (i : ι), g i * h ≤ a
⊢ iSup g * h ≤ a
have rw : ⨆ (i : ι), g i * h ≤ a
Tactic: rw [iSup_mul]
-- Lean 4 proof step from Mathlib.Data.NNReal.Basic (goal)
Goal:
ι : Sort u_2
inst : Nonempty ι
a g : ℝ≥0
h : ι → ℝ≥0
H : ∀ (j : ι), a ≤ g * h j
⊢ a ≤ g * iInf h
have rw : a ≤ ⨅ (i : ι), g * h i
Tactic: rw [mul_iInf]
-- Lean 4 proof step from Mathlib.Data.NNReal.Basic (goal)
Goal:
ι : Sort u_2
inst : Nonempty ι
a : ℝ≥0
g : ι → ℝ≥0
h : ℝ≥0
H : ∀ (i : ι), a ≤ g i * h
⊢ a ≤ iInf g * h
have rw : a ≤ ⨅ (i : ι), g i * h
Tactic: rw [iInf_mul]
-- Lean 4 proof step from Mathlib.Data.NNReal.Basic (goal)
Goal:
ι : Sort u_3
f : ι → ℕ
⊢ Eq (α := ℝ≥0) (↑(⨆ (i : ι), f i) : ℝ≥0) (⨆ (i : ι), (↑(f i) : ℝ≥0))
have pos : ∀ (h : BddAbove (range f)), Eq (α := ℝ≥0) (↑(⨆ (i : ι), f i) : ℝ≥0) (⨆ (i : ι), (↑(f i) : ℝ≥0))
Tactic: by_cases h : BddAbove (Set.range f)
-- Lean 4 proof step from Mathlib.Data.NNReal.Basic (goal)
Goal:
ι : Sort u_3
f : ι → ℕ
pos : ∀ (h : BddAbove (range f)), Eq (α := ℝ≥0) (↑(⨆ (i : ι), f i) : ℝ≥0) (⨆ (i : ι), (↑(f i) : ℝ≥0))
⊢ Eq (α := ℝ≥0) (↑(⨆ (i : ι), f i) : ℝ≥0) (⨆ (i : ι), (↑(f i) : ℝ≥0))
have neg : ∀ (h : ¬BddAbove (range f)), Eq (α := ℝ≥0) (↑(⨆ (i : ι), f i) : ℝ≥0) (⨆ (i : ι), (↑(f i) : ℝ≥0))
Tactic: by_cases h : BddAbove (Set.range f)
-- Lean 4 proof step from Mathlib.Data.NNReal.Basic (goal)
Goal:
ι : Sort u_3
f : ι → ℕ
h : BddAbove (range f)
⊢ Eq (α := ℝ≥0) (↑(⨆ (i : ι), f i) : ℝ≥0) (⨆ (i : ι), (↑(f i) : ℝ≥0))
have pos : ∀ (c : ℝ≥0), (↑(⨆ (i : ι), f i) : ℝ≥0) ≤ c ↔ ⨆ (i : ι), (↑(f i) : ℝ≥0) ≤ c
Tactic: apply eq_of_forall_ge_iff
-- Lean 4 proof step from Mathlib.Data.NNReal.Basic (goal)
Goal:
ι : Sort u_3
f : ι → ℕ
⊢ Eq (α := ℝ≥0) (↑(⨅ (i : ι), f i) : ℝ≥0) (⨅ (i : ι), (↑(f i) : ℝ≥0))
have inl : ∀ (hι : IsEmpty ι), Eq (α := ℝ≥0) (↑(⨅ (i : ι), f i) : ℝ≥0) (⨅ (i : ι), (↑(f i) : ℝ≥0))
Tactic: obtain hι | hι := isEmpty_or_nonempty ι
-- Lean 4 proof step from Mathlib.Data.NNReal.Basic (goal)
Goal:
ι : Sort u_3
f : ι → ℕ
inl : ∀ (hι : IsEmpty ι), Eq (α := ℝ≥0) (↑(⨅ (i : ι), f i) : ℝ≥0) (⨅ (i : ι), (↑(f i) : ℝ≥0))
⊢ Eq (α := ℝ≥0) (↑(⨅ (i : ι), f i) : ℝ≥0) (⨅ (i : ι), (↑(f i) : ℝ≥0))
have inr : ∀ (hι : Nonempty ι), Eq (α := ℝ≥0) (↑(⨅ (i : ι), f i) : ℝ≥0) (⨅ (i : ι), (↑(f i) : ℝ≥0))
Tactic: obtain hι | hι := isEmpty_or_nonempty ι
-- Lean 4 proof step from Mathlib.Data.NNReal.Basic (goal)
Goal:
ι : Sort u_3
f : ι → ℕ
hι : Nonempty ι
⊢ Eq (α := ℝ≥0) (↑(⨅ (i : ι), f i) : ℝ≥0) (⨅ (i : ι), (↑(f i) : ℝ≥0))
have inr : ∀ (c : ℝ≥0), c ≤ (↑(⨅ (i : ι), f i) : ℝ≥0) ↔ c ≤ ⨅ (i : ι), (↑(f i) : ℝ≥0)
Tactic: apply eq_of_forall_le_iff
-- Lean 4 proof step from Mathlib.Data.NNReal.Defs (goal)
Goal:
r : ℝ≥0
⊢ (↑r : ℝ) = 0 ↔ r = 0
have rw : (↑r : ℝ) = (↑0 : ℝ) ↔ r = 0
Tactic: rw [← coe_zero, coe_inj]
-- Lean 4 proof step from Mathlib.Data.NNReal.Defs (goal)
Goal:
r : ℝ≥0
rw : (↑r : ℝ) = (↑0 : ℝ) ↔ r = 0
⊢ (↑r : ℝ) = 0 ↔ r = 0
have rw₁ : r = 0 ↔ r = 0
Tactic: rw [← coe_zero, coe_inj]
-- Lean 4 proof step from Mathlib.Data.NNReal.Defs (goal)
Goal:
r : ℝ≥0
⊢ (↑r : ℝ) = 1 ↔ r = 1
have rw : (↑r : ℝ) = (↑1 : ℝ) ↔ r = 1
Tactic: rw [← coe_one, coe_inj]
-- Lean 4 proof step from Mathlib.Data.NNReal.Defs (goal)
Goal:
r : ℝ≥0
rw : (↑r : ℝ) = (↑1 : ℝ) ↔ r = 1
⊢ (↑r : ℝ) = 1 ↔ r = 1
have rw₁ : r = 1 ↔ r = 1
Tactic: rw [← coe_one, coe_inj]
-- Lean 4 proof step from Mathlib.Data.NNReal.Defs (goal)
Goal:
r : ℝ≥0
⊢ 1 ≤ (↑r : ℝ) ↔ 1 ≤ r
have rw : 1 ≤ (↑r : ℝ) ↔ (↑1 : ℝ) ≤ (↑r : ℝ)
Tactic: rw [← coe_le_coe, coe_one]
-- Lean 4 proof step from Mathlib.Data.NNReal.Defs (goal)
Goal:
r : ℝ≥0
rw : 1 ≤ (↑r : ℝ) ↔ (↑1 : ℝ) ≤ (↑r : ℝ)
⊢ 1 ≤ (↑r : ℝ) ↔ 1 ≤ r
have rw₁ : 1 ≤ (↑r : ℝ) ↔ 1 ≤ (↑r : ℝ)
Tactic: rw [← coe_le_coe, coe_one]
-- Lean 4 proof step from Mathlib.Data.NNReal.Defs (goal)
Goal:
r : ℝ≥0
⊢ 1 < (↑r : ℝ) ↔ 1 < r
have rw : 1 < (↑r : ℝ) ↔ (↑1 : ℝ) < (↑r : ℝ)
Tactic: rw [← coe_lt_coe, coe_one]
-- Lean 4 proof step from Mathlib.Data.NNReal.Defs (goal)
Goal:
r : ℝ≥0
rw : 1 < (↑r : ℝ) ↔ (↑1 : ℝ) < (↑r : ℝ)
⊢ 1 < (↑r : ℝ) ↔ 1 < r
have rw₁ : 1 < (↑r : ℝ) ↔ 1 < (↑r : ℝ)
Tactic: rw [← coe_lt_coe, coe_one]
-- Lean 4 proof step from Mathlib.Data.NNReal.Defs (goal)
Goal:
r : ℝ≥0
⊢ (↑r : ℝ) ≤ 1 ↔ r ≤ 1
have rw : (↑r : ℝ) ≤ 1 ↔ (↑r : ℝ) ≤ (↑1 : ℝ)
Tactic: rw [← coe_le_coe, coe_one]
-- Lean 4 proof step from Mathlib.Data.NNReal.Defs (goal)
Goal:
r : ℝ≥0
rw : (↑r : ℝ) ≤ 1 ↔ (↑r : ℝ) ≤ (↑1 : ℝ)
⊢ (↑r : ℝ) ≤ 1 ↔ r ≤ 1
have rw₁ : (↑r : ℝ) ≤ 1 ↔ (↑r : ℝ) ≤ 1
Tactic: rw [← coe_le_coe, coe_one]
-- Lean 4 proof step from Mathlib.Data.NNReal.Defs (goal)
Goal:
r : ℝ≥0
⊢ (↑r : ℝ) < 1 ↔ r < 1
have rw : (↑r : ℝ) < 1 ↔ (↑r : ℝ) < (↑1 : ℝ)
Tactic: rw [← coe_lt_coe, coe_one]
-- Lean 4 proof step from Mathlib.Data.NNReal.Defs (goal)
Goal:
r : ℝ≥0
rw : (↑r : ℝ) < 1 ↔ (↑r : ℝ) < (↑1 : ℝ)
⊢ (↑r : ℝ) < 1 ↔ r < 1
have rw₁ : (↑r : ℝ) < 1 ↔ (↑r : ℝ) < 1
Tactic: rw [← coe_lt_coe, coe_one]
-- Lean 4 proof step from Mathlib.Data.NNReal.Defs (goal)
Goal:
s : Set ℝ≥0
⊢ (↑(sSup s) : ℝ) = sSup (toReal '' s)
have inl : (↑(sSup ∅) : ℝ) = sSup (toReal '' ∅)
Tactic: rcases Set.eq_empty_or_nonempty s with rfl | hs
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Data.NNReal.Defs (goal)
Goal:
s : Set ℝ≥0
inl : (↑(sSup ∅) : ℝ) = sSup (toReal '' ∅)
⊢ (↑(sSup s) : ℝ) = sSup (toReal '' s)
have inr : ∀ (hs : s.Nonempty), (↑(sSup s) : ℝ) = sSup (toReal '' s)
Tactic: rcases Set.eq_empty_or_nonempty s with rfl | hs
-- Lean 4 proof step from Mathlib.Data.NNReal.Defs (goal)
Goal:
s : Set ℝ≥0
hs : s.Nonempty
⊢ (↑(sSup s) : ℝ) = sSup (toReal '' s)
have pos : ∀ (H : BddAbove s), (↑(sSup s) : ℝ) = sSup (toReal '' s)
Tactic: by_cases H : BddAbove s
-- Lean 4 proof step from Mathlib.Data.NNReal.Defs (goal)
Goal:
s : Set ℝ≥0
hs : s.Nonempty
pos : ∀ (H : BddAbove s), (↑(sSup s) : ℝ) = sSup (toReal '' s)
⊢ (↑(sSup s) : ℝ) = sSup (toReal '' s)
have neg : ∀ (H : ¬BddAbove s), (↑(sSup s) : ℝ) = sSup (toReal '' s)
Tactic: by_cases H : BddAbove s
-- Lean 4 proof step from Mathlib.Data.NNReal.Defs (goal)
Goal:
s : Set ℝ≥0
hs : s.Nonempty
H : BddAbove s
⊢ Membership.mem (γ := Set ℝ) (Set.Ici 0) (sSup (Subtype.val (p := fun (r : ℝ) ↦ 0 ≤ r) '' s))
have hs₁ : ∀ x ∈ Subtype.val (p := fun (r : ℝ) ↦ 0 ≤ r) '' s, 0 ≤ x
Tactic: apply Real.sSup_nonneg