awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : (↑⌊x⌋₊ : ℚ≥0) ≤ x ∧ x < (↑(⌊x⌋₊ + 1) : ℚ≥0)
⊢ LE.le.{u_1} (α := K) (↑⌊x⌋₊ : K) (↑x : K) ∧ LT.lt.{u_1} (α := K) (↑x : K) (↑(⌊x⌋₊ + 1) : K)

Tactic:
norm_cast
-- 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 : (↑⌊x⌋₊ : ℚ≥0) ≤ x ∧ x < HAdd.hAdd (α := ℚ≥0) (↑⌊x⌋₊ : ℚ≥0) 1
rw₁ rw₂ : ⌊x⌋₊ = ⌊x⌋₊
⊢ (↑⌊x⌋₊ : ℚ≥0) ≤ x ∧ x < (↑(⌊x⌋₊ + 1) : ℚ≥0)

Tactic:
rw [Nat.cast_add_one, ← Nat.floor_eq_iff zero_le]

Premises used: zero_le, Nat.floor_eq_iff, Nat.cast_add_one
-- 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 : (↑(↑⌈x⌉₊ : ℤ) : K) < HAdd.hAdd (α := K) (↑x : K) 1 ∧ LE.le.{u_1} (α := K) (↑x : K) (↑(↑⌈x⌉₊ : ℤ) : K)
⊢ Int.ceil.{u_1} (α := K) (↑x : K) = Int.ceil (α := ℚ) (↑x : ℚ)

Tactic:
rw [Int.ceil_eq_iff, ← coe_ceil, sub_lt_iff_lt_add]

Premises used: Int.ceil_eq_iff, NNRat.coe_ceil, sub_lt_iff_lt_add
-- 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
left : (↑(↑⌈x⌉₊ : ℤ) : K) < HAdd.hAdd (α := K) (↑x : K) 1
right : LE.le.{u_1} (α := K) (↑x : K) (↑(↑⌈x⌉₊ : ℤ) : K)
⊢ (↑(↑⌈x⌉₊ : ℤ) : K) < HAdd.hAdd (α := K) (↑x : K) 1 ∧ LE.le.{u_1} (α := K) (↑x : K) (↑(↑⌈x⌉₊ : ℤ) : K)

Tactic:
constructor
-- 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
⊢ (↑(↑⌈x⌉₊ : ℤ) : K) < HAdd.hAdd (α := K) (↑x : K) 1

Tactic:
exact_mod_cast NNRat.cast_strictMono <| Nat.ceil_lt_add_one zero_le

Premises used: zero_le, NNRat.cast_strictMono, Nat.ceil_lt_add_one
-- 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
right : x ≤ (↑⌈x⌉₊ : ℚ≥0)
⊢ LE.le.{u_1} (α := K) (↑x : K) (↑(↑⌈x⌉₊ : ℤ) : K)

Tactic:
rw [Int.cast_natCast, NNRat.cast_le_natCast]

Premises used: Int.cast_natCast, NNRat.cast_le_natCast
-- 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
⊢ x ≤ (↑⌈x⌉₊ : ℚ≥0)

Tactic:
Nat.le_ceil _

Premises used: Nat.le_ceil
-- 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
⊢ x ≤ (↑⌈x⌉₊ : ℚ≥0)

Tactic:
exact Nat.le_ceil _

Premises used: Nat.le_ceil
-- Module: Mathlib.Data.NNRat.Floor
Goal:
n d : ℕ
⊢ ⌊HDiv.hDiv (α := ℚ≥0) (↑n : ℚ≥0) (↑d : ℚ≥0)⌋₊ = n / d

Tactic:
Rat.natFloor_natCast_div_natCast n d

Premises used: Rat.natFloor_natCast_div_natCast, Nat.floor, Int.toNat, Rat.div, Rat.ofInt
-- Module: Mathlib.Data.NNRat.Floor
Goal:
R : Type u_1
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : FloorSemiring R
m : ℕ
⊢ Nat.ceil.{u_1} (α := R) (↑m : R) = (↑m : ℕ)

Tactic:
simp
-- Module: Mathlib.Data.NNRat.Floor
Goal:
R : Type u_1
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : FloorSemiring R
m : ℕ
⊢ IsNat (Nat.ceil.{u_1} (α := R) (↑m : R)) m

Tactic:
exact ⟨by simp⟩
-- Module: Mathlib.Data.NNRat.Floor
Goal:
R : Type u_1
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : FloorSemiring R
m : ℕ
⊢ Nat.ceil.{u_1} (α := R) (↑(Int.negOfNat m) : R) = (↑0 : ℕ)

Tactic:
simp
-- Module: Mathlib.Data.NNRat.Floor
Goal:
R : Type u_1
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : FloorSemiring R
m : ℕ
⊢ IsNat (Nat.ceil.{u_1} (α := R) (↑(Int.negOfNat m) : R)) 0

Tactic:
exact ⟨by simp⟩
-- Module: Mathlib.Data.NNRat.Floor
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
out : ⌈r⌉₊ = (↑res : ℕ)
⊢ IsNat ⌈r⌉₊ res

Tactic:
constructor
-- Module: Mathlib.Data.NNRat.Floor
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
out :
  ⌈HDiv.hDiv (α := R) (↑n : R) (↑d : R)⌉₊ =
    (↑(Nat.ceil.{u_1} (α := R) (↑(HDiv.hDiv (α := ℚ≥0) (↑n : ℚ≥0) (↑d : ℚ≥0)) : R)) : ℕ)
⊢ ⌈r⌉₊ = (↑res : ℕ)

Tactic:
rw [← hres, h.to_eq rfl rfl, ← @NNRat.ceil_cast R]

Premises used: Mathlib.Meta.NormNum.IsNNRat.to_eq, NNRat.ceil_cast, rfl
-- Module: Mathlib.Data.NNRat.Floor
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
⊢ ⌈HDiv.hDiv (α := R) (↑n : R) (↑d : R)⌉₊ =
    (↑(Nat.ceil.{u_1} (α := R) (↑(HDiv.hDiv (α := ℚ≥0) (↑n : ℚ≥0) (↑d : ℚ≥0)) : R)) : ℕ)

Tactic:
simp
-- Module: Mathlib.Data.NNRat.Floor
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
out : ⌈r⌉₊ = (↑0 : ℕ)
⊢ IsNat ⌈r⌉₊ 0

Tactic:
constructor
-- Module: Mathlib.Data.NNRat.Floor
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
⊢ ⌈r⌉₊ = (↑0 : ℕ)

Tactic:
simp [h.neg_to_eq, div_nonneg]

Premises used: div_nonneg, Mathlib.Meta.NormNum.IsRat.neg_to_eq
-- Module: Mathlib.Data.NNRat.Lemmas
Goal:
α : Type u_1
s : Set α
f : α → ℚ≥0
a : α
⊢ Eq (α := ℚ) (↑(s.indicator f a) : ℚ) (s.indicator (fun (x : α) ↦ (↑(f x) : ℚ)) a)

Tactic:
map_indicator coeHom _ _ _

Premises used: NNRat.coeHom, map_indicator
-- Module: Mathlib.Data.NNRat.Lemmas
Goal:
q : ℚ
inl : ∀ (hq : q ≤ 0), q⁻¹.toNNRat = q.toNNRat⁻¹
inr : ∀ (hq : 0 ≤ q), q⁻¹.toNNRat = q.toNNRat⁻¹
⊢ q⁻¹.toNNRat = q.toNNRat⁻¹

Tactic:
obtain hq | hq := le_total q 0

Premises used: le_total, OfNat.ofNat
-- Module: Mathlib.Data.NNRat.Lemmas
Goal:
q : ℚ
hq : q ≤ 0
inl : q⁻¹.toNNRat = 0⁻¹
inl₁ : q⁻¹.toNNRat = 0
inl₂ inl₃ : Eq (α := ℚ≥0) 0 0
⊢ q⁻¹.toNNRat = q.toNNRat⁻¹

Tactic:
rw [toNNRat_eq_zero.mpr hq, inv_zero, toNNRat_eq_zero.mpr (inv_nonpos.mpr hq)]

Premises used: Iff.mpr, inv_zero, inv_nonpos, Rat.toNNRat_eq_zero
-- Module: Mathlib.Data.NNRat.Lemmas
Goal:
q : ℚ
hq : 0 ≤ q
inr : toNNRat (↑q.toNNRat : ℚ)⁻¹ = q.toNNRat⁻¹
⊢ q⁻¹.toNNRat = q.toNNRat⁻¹

Tactic:
nth_rw 1 [← Rat.coe_toNNRat q hq]

Premises used: Rat.coe_toNNRat
-- Module: Mathlib.Data.NNRat.Lemmas
Goal:
q : ℚ
hq : 0 ≤ q
inr : toNNRat (↑q.toNNRat⁻¹ : ℚ) = q.toNNRat⁻¹
inr₁ inr₂ : q.toNNRat⁻¹ = q.toNNRat⁻¹
⊢ toNNRat (↑q.toNNRat : ℚ)⁻¹ = q.toNNRat⁻¹

Tactic:
rw [← coe_inv, toNNRat_coe]

Premises used: NNRat.coe_inv, NNRat.toNNRat_coe
-- Module: Mathlib.Data.NNRat.Lemmas
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
rw₃ rw₄ : (p * q⁻¹).toNNRat = (p * q⁻¹).toNNRat
⊢ (p / q).toNNRat = p.toNNRat / q.toNNRat

Tactic:
rw [div_eq_mul_inv, div_eq_mul_inv, ← toNNRat_inv, ← toNNRat_mul hp]

Premises used: Rat.toNNRat_mul, div_eq_mul_inv, Rat.toNNRat_inv
-- Module: Mathlib.Data.NNRat.Lemmas
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
rw₃ rw₄ : q.toNNRat⁻¹ * p.toNNRat = q.toNNRat⁻¹ * p.toNNRat
⊢ (p / q).toNNRat = p.toNNRat / q.toNNRat

Tactic:
rw [div_eq_inv_mul, div_eq_inv_mul, toNNRat_mul (inv_nonneg.2 hq), toNNRat_inv]

Premises used: Iff.mpr, Rat.toNNRat_mul, inv_nonneg, Rat.toNNRat_inv, div_eq_inv_mul
-- Module: Mathlib.Data.NNRat.Lemmas
Goal:
q_1 : ℚ≥0
α : ℚ≥0 → Sort u_1
h : (m n : ℕ) → α (HDiv.hDiv (α := ℚ≥0) (↑m : ℚ≥0) (↑n : ℚ≥0))
q : ℚ≥0
rw : α (HDiv.hDiv (α := ℚ≥0) (↑q.num : ℚ≥0) (↑q.den : ℚ≥0))
⊢ α q

Tactic:
rw [← num_div_den q]

Premises used: NNRat.num_div_den
-- Module: Mathlib.Data.NNRat.Lemmas
Goal:
q_1 : ℚ≥0
α : ℚ≥0 → Sort u_1
h : (m n : ℕ) → α (HDiv.hDiv (α := ℚ≥0) (↑m : ℚ≥0) (↑n : ℚ≥0))
q : ℚ≥0
⊢ α (HDiv.hDiv (α := ℚ≥0) (↑q.num : ℚ≥0) (↑q.den : ℚ≥0))

Tactic:
apply h
-- Module: Mathlib.Data.NNRat.Lemmas
Goal:
q₁ q₂ : ℚ≥0
zify :
  (↑(q₁ * q₂).num : ℤ) =
    HMul.hMul (α := ℤ) (↑q₁.num : ℤ) (↑q₂.num : ℤ) / (↑((q₁.num * q₂.num).gcd (q₁.den * q₂.den)) : ℤ)
⊢ (q₁ * q₂).num = q₁.num * q₂.num / (q₁.num * q₂.num).gcd (q₁.den * q₂.den)

Tactic:
zify
-- Module: Mathlib.Data.NNRat.Lemmas
Goal:
q₁ q₂ : ℚ≥0
⊢ (HMul.hMul (α := ℚ) (↑q₁ : ℚ) (↑q₂ : ℚ)).num =
    Rat.num (↑q₁ : ℚ) * Rat.num (↑q₂ : ℚ) /
      (↑((Rat.num (↑q₁ : ℚ) * Rat.num (↑q₂ : ℚ)).natAbs.gcd (Rat.den (↑q₁ : ℚ) * Rat.den (↑q₂ : ℚ))) : ℤ)

Tactic:
Rat.mul_num q₁ q₂

Premises used: NNRat.cast, Rat.mul_num
-- Module: Mathlib.Data.NNRat.Lemmas
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₂ : ℚ)
h₃ : q₁.num * q₂.num = (Rat.num (↑q₁ : ℚ) * Rat.num (↑q₂ : ℚ)).natAbs
⊢ (↑(q₁ * q₂).num : ℤ) =
    HMul.hMul (α := ℤ) (↑q₁.num : ℤ) (↑q₂.num : ℤ) / (↑((q₁.num * q₂.num).gcd (q₁.den * q₂.den)) : ℤ)

Tactic:
convert! Rat.mul_num q₁ q₂

Premises used: NNRat.cast, Rat.mul_num
-- Module: Mathlib.Data.NNRat.Lemmas
Goal:
q₁ q₂ : ℚ≥0
h h₁ h₂ h₃ : (q₁ * q₂).num = (q₁ * q₂).num
⊢ (↑(q₁ * q₂).num : ℤ) = (HMul.hMul (α := ℚ) (↑q₁ : ℚ) (↑q₂ : ℚ)).num

Tactic:
norm_cast
-- Module: Mathlib.Data.NNRat.Lemmas
Goal:
q₁ q₂ : ℚ≥0
h h₁ h₂ h₃ : q₁.num = q₁.num
⊢ (↑q₁.num : ℤ) = Rat.num (↑q₁ : ℚ)

Tactic:
norm_cast
-- Module: Mathlib.Data.NNRat.Lemmas
Goal:
q₁ q₂ : ℚ≥0
h h₁ h₂ h₃ : q₂.num = q₂.num
⊢ (↑q₂.num : ℤ) = Rat.num (↑q₂ : ℚ)

Tactic:
norm_cast
-- Module: Mathlib.Data.NNRat.Lemmas
Goal:
q₁ q₂ : ℚ≥0
h h₁ h₂ h₃ : q₁.num * q₂.num = q₁.num * q₂.num
⊢ q₁.num * q₂.num = (Rat.num (↑q₁ : ℚ) * Rat.num (↑q₂ : ℚ)).natAbs

Tactic:
norm_cast
-- Module: Mathlib.Data.NNRat.Lemmas
Goal:
q₁ q₂ : ℚ≥0
⊢ (HMul.hMul (α := ℚ) (↑q₁ : ℚ) (↑q₂ : ℚ)).den =
    Rat.den (↑q₁ : ℚ) * Rat.den (↑q₂ : ℚ) /
      (Rat.num (↑q₁ : ℚ) * Rat.num (↑q₂ : ℚ)).natAbs.gcd (Rat.den (↑q₁ : ℚ) * Rat.den (↑q₂ : ℚ))

Tactic:
Rat.mul_den q₁ q₂

Premises used: NNRat.cast, Rat.mul_den
-- Module: Mathlib.Data.NNRat.Lemmas
Goal:
q₁ q₂ : ℚ≥0
h : q₁.num * q₂.num = (Rat.num (↑q₁ : ℚ) * Rat.num (↑q₂ : ℚ)).natAbs
⊢ (q₁ * q₂).den = q₁.den * q₂.den / (q₁.num * q₂.num).gcd (q₁.den * q₂.den)

Tactic:
convert! Rat.mul_den q₁ q₂

Premises used: NNRat.cast, Rat.mul_den
-- Module: Mathlib.Data.NNRat.Lemmas
Goal:
q₁ q₂ : ℚ≥0
⊢ Rat.den (↑q₁ : ℚ) * Rat.den (↑q₂ : ℚ) =
    (HMul.hMul (α := ℚ) (↑q₁ : ℚ) (↑q₂ : ℚ)).den *
      (Rat.num (↑q₁ : ℚ) * Rat.num (↑q₂ : ℚ)).natAbs.gcd (Rat.den (↑q₁ : ℚ) * Rat.den (↑q₂ : ℚ))

Tactic:
Rat.den_mul_den_eq_den_mul_gcd q₁ q₂

Premises used: Rat.den_mul_den_eq_den_mul_gcd, NNRat.cast
-- Module: Mathlib.Data.NNRat.Lemmas
Goal:
q₁ q₂ : ℚ≥0
h : q₁.num * q₂.num = (Rat.num (↑q₁ : ℚ) * Rat.num (↑q₂ : ℚ)).natAbs
⊢ q₁.den * q₂.den = (q₁ * q₂).den * (q₁.num * q₂.num).gcd (q₁.den * q₂.den)

Tactic:
convert! Rat.den_mul_den_eq_den_mul_gcd q₁ q₂

Premises used: Rat.den_mul_den_eq_den_mul_gcd, NNRat.cast
-- Module: Mathlib.Data.NNRat.Lemmas
Goal:
q₁ q₂ : ℚ≥0
zify :
  HMul.hMul (α := ℤ) (↑q₁.num : ℤ) (↑q₂.num : ℤ) =
    HMul.hMul (α := ℤ) (↑(q₁ * q₂).num : ℤ) (↑((q₁.num * q₂.num).gcd (q₁.den * q₂.den)) : ℤ)
⊢ q₁.num * q₂.num = (q₁ * q₂).num * (q₁.num * q₂.num).gcd (q₁.den * q₂.den)

Tactic:
zify
-- Module: Mathlib.Data.NNRat.Lemmas
Goal:
q₁ q₂ : ℚ≥0
⊢ Rat.num (↑q₁ : ℚ) * Rat.num (↑q₂ : ℚ) =
    (HMul.hMul (α := ℚ) (↑q₁ : ℚ) (↑q₂ : ℚ)).num *
      (↑((Rat.num (↑q₁ : ℚ) * Rat.num (↑q₂ : ℚ)).natAbs.gcd (Rat.den (↑q₁ : ℚ) * Rat.den (↑q₂ : ℚ))) : ℤ)

Tactic:
Rat.num_mul_num_eq_num_mul_gcd q₁ q₂

Premises used: Rat.num_mul_num_eq_num_mul_gcd, NNRat.cast
-- Module: Mathlib.Data.NNRat.Lemmas
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
h₃ : q₁.num * q₂.num = (Rat.num (↑q₁ : ℚ) * Rat.num (↑q₂ : ℚ)).natAbs
⊢ HMul.hMul (α := ℤ) (↑q₁.num : ℤ) (↑q₂.num : ℤ) =
    HMul.hMul (α := ℤ) (↑(q₁ * q₂).num : ℤ) (↑((q₁.num * q₂.num).gcd (q₁.den * q₂.den)) : ℤ)

Tactic:
convert! Rat.num_mul_num_eq_num_mul_gcd q₁ q₂

Premises used: Rat.num_mul_num_eq_num_mul_gcd, NNRat.cast
-- Module: Mathlib.Data.NNRat.Order
Goal:
⊢ IsStrictOrderedRing ℚ≥0

Tactic:
Nonneg.isStrictOrderedRing

Premises used: Nonneg.isStrictOrderedRing, NNRat
-- Module: Mathlib.Data.NNRat.Order
Goal:
⊢ OrderedSub ℚ≥0

Tactic:
Nonneg.orderedSub

Premises used: NNRat, Nonneg.orderedSub
-- Module: Mathlib.Data.NNRat.Order
Goal:
⊢ CanonicallyOrderedAdd ℚ≥0

Tactic:
Nonneg.canonicallyOrderedAdd

Premises used: Nonneg.canonicallyOrderedAdd, NNRat
-- Module: Mathlib.Data.NNReal.Basic
Goal:
α : Type u_1
s : Set α
f : α → ℝ≥0
a : α
⊢ (↑(s.mulIndicator f a) : ℝ) = s.mulIndicator (fun (x : α) ↦ (↑(f x) : ℝ)) a

Tactic:
map_mulIndicator toRealHom _ _ _

Premises used: NNReal.toRealHom, map_mulIndicator, NNReal.toReal
-- Module: Mathlib.Data.NNReal.Basic
Goal:
α : Type u_1
s : Set α
f : α → ℝ≥0
a : α
⊢ (↑(s.indicator f a) : ℝ) = s.indicator (fun (x : α) ↦ (↑(f x) : ℝ)) a

Tactic:
map_indicator toRealHom _ _ _

Premises used: NNReal.toRealHom, map_indicator, NNReal.toReal
-- Module: Mathlib.Data.NNReal.Basic
Goal:
α : Type u_1
inst : DecidableEq α
a : α
b : ℝ≥0
c : α
⊢ (↑(Pi.mulSingle (M := fun (a : α) ↦ ℝ≥0) a b c) : ℝ) = Pi.mulSingle (M := fun (a : α) ↦ ℝ) a (↑b : ℝ) c

Tactic:
simpa using coe_mulIndicator {a} (fun _ ↦ b) c

Premises used: NNReal.coe_mulIndicator, Singleton.singleton
-- Module: Mathlib.Data.NNReal.Basic
Goal:
α : Type u_1
inst : DecidableEq α
a : α
b : ℝ≥0
c : α
⊢ (↑(Pi.single (M := fun (a : α) ↦ ℝ≥0) a b c) : ℝ) = Pi.single (M := fun (a : α) ↦ ℝ) a (↑b : ℝ) c

Tactic:
simpa using coe_indicator {a} (fun _ ↦ b) c

Premises used: NNReal.coe_indicator, Singleton.singleton
-- Module: Mathlib.Data.NNReal.Basic
Goal:
l : List ℝ≥0
⊢ (↑l.sum : ℝ) = (List.map toReal l).sum

Tactic:
map_list_sum toRealHom l

Premises used: NNReal.toRealHom, NNReal, map_list_sum, NNReal.toReal
-- Module: Mathlib.Data.NNReal.Basic
Goal:
l : List ℝ≥0
⊢ (↑l.prod : ℝ) = (List.map toReal l).prod

Tactic:
map_list_prod toRealHom l

Premises used: NNReal.toRealHom, map_list_prod, NNReal, NNReal.toReal
-- Module: Mathlib.Data.NNReal.Basic
Goal:
s : Multiset ℝ≥0
⊢ (↑s.sum : ℝ) = (Multiset.map toReal s).sum

Tactic:
map_multiset_sum toRealHom s

Premises used: NNReal.toRealHom, map_multiset_sum, NNReal, NNReal.toReal
-- Module: Mathlib.Data.NNReal.Basic
Goal:
s : Multiset ℝ≥0
⊢ (↑s.prod : ℝ) = (Multiset.map toReal s).prod

Tactic:
map_multiset_prod toRealHom s

Premises used: NNReal.toRealHom, NNReal, map_multiset_prod, NNReal.toReal
-- Module: Mathlib.Data.NNReal.Basic
Goal:
ι : Type u_1
s : Finset ι
f : ι → ℝ≥0
⊢ (↑(∑ i ∈ s, f i) : ℝ) = ∑ i ∈ s, (↑(f i) : ℝ)

Tactic:
map_sum toRealHom _ _

Premises used: NNReal.toRealHom, map_sum, NNReal.toReal
-- Module: Mathlib.Data.NNReal.Basic
Goal:
ι : Type u_1
s : Finset ι
f : ι → ℝ≥0
⊢ (↑(𝔼 i ∈ s, f i) : ℝ) = 𝔼 i ∈ s, (↑(f i) : ℝ)

Tactic:
map_expect toRealHom ..

Premises used: NNReal.toRealHom, map_expect, NNReal.toReal
-- Module: Mathlib.Data.NNReal.Basic
Goal:
ι : Type u_1
s : Finset ι
f : ι → ℝ
hf : ∀ i ∈ s, 0 ≤ f i
rw : Eq (α := ℝ) (∑ i ∈ s, f i) (∑ i ∈ s, (↑(f i).toNNReal : ℝ))
⊢ Real.toNNReal (∑ a ∈ s, f a) = ∑ a ∈ s, (f a).toNNReal

Tactic:
rw [← coe_inj, NNReal.coe_sum, Real.coe_toNNReal _ (Finset.sum_nonneg hf)]

Premises used: Finset.sum_nonneg, NNReal.coe_sum, Real.coe_toNNReal, NNReal.coe_inj
-- Module: Mathlib.Data.NNReal.Basic
Goal:
ι : Type u_1
s : Finset ι
f : ι → ℝ
hf : ∀ i ∈ s, 0 ≤ f i
x : ι
hxs : x ∈ s
rw rw₁ : f x = f x
⊢ f x = (↑(f x).toNNReal : ℝ)

Tactic:
rw [Real.coe_toNNReal _ (hf x hxs)]

Premises used: Real.coe_toNNReal
-- Module: Mathlib.Data.NNReal.Basic
Goal:
ι : Type u_1
s : Finset ι
f : ι → ℝ
hf : ∀ i ∈ s, 0 ≤ f i
⊢ Eq (α := ℝ) (∑ i ∈ s, f i) (∑ i ∈ s, (↑(f i).toNNReal : ℝ))

Tactic:
exact Finset.sum_congr rfl fun x hxs => by rw [Real.coe_toNNReal _ (hf x hxs)]

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.Data.NNReal.Basic
Goal:
ι : Type u_1
s : Finset ι
f : ι → ℝ≥0
⊢ (↑(∏ a ∈ s, f a) : ℝ) = ∏ a ∈ s, (↑(f a) : ℝ)

Tactic:
map_prod toRealHom _ _

Premises used: NNReal.toRealHom, map_prod, NNReal.toReal
-- Module: Mathlib.Data.NNReal.Basic
Goal:
ι : Type u_1
s : Finset ι
f : ι → ℝ
hf : ∀ a ∈ s, 0 ≤ f a
rw : Eq (α := ℝ) (∏ i ∈ s, f i) (∏ a ∈ s, (↑(f a).toNNReal : ℝ))
⊢ Real.toNNReal (∏ a ∈ s, f a) = ∏ a ∈ s, (f a).toNNReal

Tactic:
rw [← coe_inj, NNReal.coe_prod, Real.coe_toNNReal _ (Finset.prod_nonneg hf)]

Premises used: NNReal.coe_prod, Real.coe_toNNReal, NNReal.coe_inj, Finset.prod_nonneg
-- Module: Mathlib.Data.NNReal.Basic
Goal:
ι : Type u_1
s : Finset ι
f : ι → ℝ
hf : ∀ a ∈ s, 0 ≤ f a
x : ι
hxs : x ∈ s
rw rw₁ : f x = f x
⊢ f x = (↑(f x).toNNReal : ℝ)

Tactic:
rw [Real.coe_toNNReal _ (hf x hxs)]

Premises used: Real.coe_toNNReal
-- Module: Mathlib.Data.NNReal.Basic
Goal:
ι : Type u_1
s : Finset ι
f : ι → ℝ
hf : ∀ a ∈ s, 0 ≤ f a
⊢ Eq (α := ℝ) (∏ i ∈ s, f i) (∏ a ∈ s, (↑(f a).toNNReal : ℝ))

Tactic:
exact Finset.prod_congr rfl fun x hxs => by rw [Real.coe_toNNReal _ (hf x hxs)]

Premises used: Finset.prod_congr, rfl
-- Module: Mathlib.Data.NNReal.Basic
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
rw : (↑a : ℝ) ≤ HAdd.hAdd (α := ℝ) (⨅ (i : ι), (↑(f i) : ℝ)) (⨅ (i : ι'), (↑(g i) : ℝ))
⊢ a ≤ HAdd.hAdd (α := ℝ≥0) (⨅ (i : ι), f i) (⨅ (j : ι'), g j)

Tactic:
rw [← NNReal.coe_le_coe, NNReal.coe_add, coe_iInf, coe_iInf]

Premises used: NNReal.coe_add, NNReal.coe_iInf, NNReal.coe_le_coe
-- Module: Mathlib.Data.NNReal.Basic
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 (α := ℝ) (⨅ (i : ι), (↑(f i) : ℝ)) (⨅ (i : ι'), (↑(g i) : ℝ))

Tactic:
le_ciInf_add_ciInf h

Premises used: le_ciInf_add_ciInf
-- Module: Mathlib.Data.NNReal.Basic
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 (α := ℝ) (⨅ (i : ι), (↑(f i) : ℝ)) (⨅ (i : ι'), (↑(g i) : ℝ))

Tactic:
exact le_ciInf_add_ciInf h

Premises used: le_ciInf_add_ciInf
-- Module: Mathlib.Data.NNReal.Basic
Goal:
α : Type u_2
r : ℝ≥0
s : Finset α
f : α → ℝ≥0
⊢ r * s.sup f = s.sup fun (a : α) ↦ r * f a

Tactic:
Finset.comp_sup_eq_sup_comp _ (NNReal.mul_sup r) (mul_zero r)

Premises used: Finset.comp_sup_eq_sup_comp, NNReal.mul_sup, MulZeroClass.mul_zero
-- Module: Mathlib.Data.NNReal.Basic
Goal:
α : Type u_2
s : Finset α
f : α → ℝ≥0
r : ℝ≥0
⊢ s.sup f * r = s.sup fun (a : α) ↦ f a * r

Tactic:
Finset.comp_sup_eq_sup_comp (· * r) (fun x y => NNReal.sup_mul x y r) (zero_mul r)

Premises used: Finset.comp_sup_eq_sup_comp, HMul.hMul, MulZeroClass.zero_mul, NNReal.sup_mul
-- Module: Mathlib.Data.NNReal.Basic
Goal:
α : Type u_2
f : α → ℝ≥0
s : Finset α
r : ℝ≥0
⊢ s.sup f / r = s.sup fun (a : α) ↦ f a / r

Tactic:
simp only [div_eq_inv_mul, mul_finset_sup]

Premises used: NNReal.mul_finset_sup, div_eq_inv_mul
-- Module: Mathlib.Data.NNReal.Basic
Goal:
s : Set ℕ
⊢ ∀ (a : ℝ≥0), Membership.mem (γ := Set ℝ≥0) (upperBounds (Nat.cast '' s)) a → ⌊a⌋₊ ∈ upperBounds s

Tactic:
simp [upperBounds, Nat.le_floor_iff]

Premises used: upperBounds, Nat.le_floor_iff
-- Module: Mathlib.Data.NNReal.Basic
Goal:
s : Set ℕ
⊢ ∀ a ∈ upperBounds s, Membership.mem (γ := Set ℝ≥0) (upperBounds (Nat.cast '' s)) (↑a : ℝ≥0)

Tactic:
simp [upperBounds]

Premises used: upperBounds
-- Module: Mathlib.Data.NNReal.Basic
Goal:
ι : Sort u_2
f : ι → ℕ
rw : BddAbove (α := ℝ≥0) (range fun (x : ι) ↦ (↑(f x) : ℝ≥0)) ↔ BddAbove (α := ℝ≥0) (range (Nat.cast ∘ f))
⊢ BddAbove (α := ℝ≥0) (range fun (x : ι) ↦ (↑(f x) : ℝ≥0)) ↔ BddAbove (range f)

Tactic:
rw [← bddAbove_natCast_image_iff, ← Set.range_comp]

Premises used: Set.range_comp, NNReal.bddAbove_natCast_image_iff
-- Module: Mathlib.Data.NNReal.Basic
Goal:
ι : Sort u_2
f : ι → ℕ
⊢ BddAbove (α := ℝ≥0) (range fun (x : ι) ↦ (↑(f x) : ℝ≥0)) ↔ BddAbove (α := ℝ≥0) (range (Nat.cast ∘ f))

Tactic:
rfl
-- Module: Mathlib.Data.NNReal.Basic
Goal:
a b c : ℝ≥0
⊢ (a - b) / c = a / c - b / c

Tactic:
tsub_div _ _ _

Premises used: tsub_div
-- Module: Mathlib.Data.NNReal.Basic
Goal:
a b : ℝ≥0
h : a < b
⊢ (↑(b - a) : ℝ) = (↑b : ℝ) - (↑a : ℝ)

Tactic:
NNReal.coe_sub h.le

Premises used: LT.lt.le, NNReal.coe_sub
-- Module: Mathlib.Data.NNReal.Basic
Goal:
ι : Sort u_2
f : ι → ℝ≥0
a : ℝ≥0
rw : (⨅ (i : ι), (↑(f i) : ℝ)) * (↑a : ℝ) = ⨅ (i : ι), (↑(f i * a) : ℝ)
⊢ iInf f * a = ⨅ (i : ι), f i * a

Tactic:
rw [← coe_inj, NNReal.coe_mul, coe_iInf, coe_iInf]

Premises used: NNReal.coe_iInf, NNReal.coe_mul, NNReal.coe_inj
-- Module: Mathlib.Data.NNReal.Basic
Goal:
ι : Sort u_2
f : ι → ℝ≥0
a : ℝ≥0
⊢ (⨅ (i : ι), (↑(f i) : ℝ)) * (↑a : ℝ) = ⨅ (i : ι), (↑(f i * a) : ℝ)

Tactic:
Real.iInf_mul_of_nonneg (NNReal.coe_nonneg _) _

Premises used: Real.iInf_mul_of_nonneg, NNReal.coe_nonneg, NNReal.toReal
-- Module: Mathlib.Data.NNReal.Basic
Goal:
ι : Sort u_2
f : ι → ℝ≥0
a : ℝ≥0
⊢ (⨅ (i : ι), (↑(f i) : ℝ)) * (↑a : ℝ) = ⨅ (i : ι), (↑(f i * a) : ℝ)

Tactic:
exact Real.iInf_mul_of_nonneg (NNReal.coe_nonneg _) _

Premises used: Real.iInf_mul_of_nonneg, NNReal.coe_nonneg
-- Module: Mathlib.Data.NNReal.Basic
Goal:
ι : Sort u_2
f : ι → ℝ≥0
a : ℝ≥0
⊢ a * iInf f = ⨅ (i : ι), a * f i

Tactic:
simpa only [mul_comm] using iInf_mul f a

Premises used: mul_comm, NNReal.iInf_mul
-- Module: Mathlib.Data.NNReal.Basic
Goal:
ι : Sort u_2
f : ι → ℝ≥0
a : ℝ≥0
rw : (↑a : ℝ) * ⨆ (i : ι), (↑(f i) : ℝ) = ⨆ (i : ι), (↑(a * f i) : ℝ)
⊢ a * ⨆ (i : ι), f i = ⨆ (i : ι), a * f i

Tactic:
rw [← coe_inj, NNReal.coe_mul, NNReal.coe_iSup, NNReal.coe_iSup]

Premises used: NNReal.coe_iSup, NNReal.coe_mul, NNReal.coe_inj
-- Module: Mathlib.Data.NNReal.Basic
Goal:
ι : Sort u_2
f : ι → ℝ≥0
a : ℝ≥0
⊢ (↑a : ℝ) * ⨆ (i : ι), (↑(f i) : ℝ) = ⨆ (i : ι), (↑(a * f i) : ℝ)

Tactic:
Real.mul_iSup_of_nonneg (NNReal.coe_nonneg _) _

Premises used: NNReal.coe_nonneg, NNReal.toReal, Real.mul_iSup_of_nonneg
-- Module: Mathlib.Data.NNReal.Basic
Goal:
ι : Sort u_2
f : ι → ℝ≥0
a : ℝ≥0
⊢ (↑a : ℝ) * ⨆ (i : ι), (↑(f i) : ℝ) = ⨆ (i : ι), (↑(a * f i) : ℝ)

Tactic:
exact Real.mul_iSup_of_nonneg (NNReal.coe_nonneg _) _

Premises used: NNReal.coe_nonneg, Real.mul_iSup_of_nonneg
-- Module: Mathlib.Data.NNReal.Basic
Goal:
ι : Sort u_2
f : ι → ℝ≥0
a : ℝ≥0
rw : Eq (α := ℝ≥0) (⨆ (i : ι), a * f i) (⨆ (i : ι), f i * a)
⊢ (⨆ (i : ι), f i) * a = ⨆ (i : ι), f i * a

Tactic:
rw [mul_comm, mul_iSup]

Premises used: mul_comm, NNReal.mul_iSup
-- Module: Mathlib.Data.NNReal.Basic
Goal:
ι : Sort u_2
f : ι → ℝ≥0
a : ℝ≥0
⊢ Eq (α := ℝ≥0) (⨆ (i : ι), a * f i) (⨆ (i : ι), f i * a)

Tactic:
simp_rw [mul_comm]

Premises used: mul_comm
-- Module: Mathlib.Data.NNReal.Basic
Goal:
ι : Sort u_2
f : ι → ℝ≥0
a : ℝ≥0
⊢ (⨆ (i : ι), f i) / a = ⨆ (i : ι), f i / a

Tactic:
simp only [div_eq_mul_inv, iSup_mul]

Premises used: div_eq_mul_inv, NNReal.iSup_mul
-- Module: Mathlib.Data.NNReal.Basic
Goal:
ι : Sort u_2
a g : ℝ≥0
h : ι → ℝ≥0
H : ∀ (j : ι), g * h j ≤ a
rw : ⨆ (i : ι), g * h i ≤ a
⊢ g * iSup h ≤ a

Tactic:
rw [mul_iSup]

Premises used: NNReal.mul_iSup
-- Module: Mathlib.Data.NNReal.Basic
Goal:
ι : Sort u_2
a g : ℝ≥0
h : ι → ℝ≥0
H : ∀ (j : ι), g * h j ≤ a
⊢ ⨆ (i : ι), g * h i ≤ a

Tactic:
ciSup_le' H

Premises used: ciSup_le'
-- Module: Mathlib.Data.NNReal.Basic
Goal:
ι : Sort u_2
a g : ℝ≥0
h : ι → ℝ≥0
H : ∀ (j : ι), g * h j ≤ a
⊢ ⨆ (i : ι), g * h i ≤ a

Tactic:
exact ciSup_le' H

Premises used: ciSup_le'
-- Module: Mathlib.Data.NNReal.Basic
Goal:
ι : Sort u_2
a : ℝ≥0
g : ι → ℝ≥0
h : ℝ≥0
H : ∀ (i : ι), g i * h ≤ a
rw : ⨆ (i : ι), g i * h ≤ a
⊢ iSup g * h ≤ a

Tactic:
rw [iSup_mul]

Premises used: NNReal.iSup_mul
-- Module: Mathlib.Data.NNReal.Basic
Goal:
ι : Sort u_2
a : ℝ≥0
g : ι → ℝ≥0
h : ℝ≥0
H : ∀ (i : ι), g i * h ≤ a
⊢ ⨆ (i : ι), g i * h ≤ a

Tactic:
ciSup_le' H

Premises used: ciSup_le'