[GOAL]
r : ℝ
hr : 0 ≤ r
⊢ Real.toNNReal r = { val := r, property := hr }
[PROOFSTEP]
simp_rw [Real.toNNReal, max_eq_left hr]
[GOAL]
⊢ Zero ℝ≥0
[PROOFSTEP]
infer_instance
[GOAL]
⊢ One ℝ≥0
[PROOFSTEP]
infer_instance
[GOAL]
⊢ Add ℝ≥0
[PROOFSTEP]
infer_instance
[GOAL]
⊢ Sub ℝ≥0
[PROOFSTEP]
infer_instance
[GOAL]
⊢ Mul ℝ≥0
[PROOFSTEP]
infer_instance
[GOAL]
⊢ Inv ℝ≥0
[PROOFSTEP]
infer_instance
[GOAL]
⊢ Div ℝ≥0
[PROOFSTEP]
infer_instance
[GOAL]
⊢ LE ℝ≥0
[PROOFSTEP]
infer_instance
[GOAL]
⊢ Bot ℝ≥0
[PROOFSTEP]
infer_instance
[GOAL]
⊢ Inhabited ℝ≥0
[PROOFSTEP]
infer_instance
[GOAL]
⊢ Nontrivial ℝ≥0
[PROOFSTEP]
infer_instance
[GOAL]
r₁ r₂ : ℝ≥0
h : r₂ ≤ r₁
⊢ ↑r₂ ≤ ↑r₁ - 0
[PROOFSTEP]
simp [show (r₂ : ℝ) ≤ r₁ from h]
[GOAL]
r : ℝ≥0
⊢ ↑r = 0 ↔ r = 0
[PROOFSTEP]
rw [← NNReal.coe_zero, NNReal.coe_eq]
[GOAL]
r : ℝ≥0
⊢ ↑r = 1 ↔ r = 1
[PROOFSTEP]
rw [← NNReal.coe_one, NNReal.coe_eq]
[GOAL]
⊢ CommSemiring ℝ≥0
[PROOFSTEP]
infer_instance
[GOAL]
A : Type u_1
inst✝¹ : Semiring A
inst✝ : Algebra ℝ A
r : ℝ≥0
x : (fun x => A) r
⊢ ↑(RingHom.comp (algebraMap ℝ A) toRealHom) r * x = x * ↑(RingHom.comp (algebraMap ℝ A) toRealHom) r
[PROOFSTEP]
simp [Algebra.commutes]
[GOAL]
A : Type u_1
inst✝¹ : Semiring A
inst✝ : Algebra ℝ A
r : ℝ≥0
x : (fun x => A) r
⊢ r • x = ↑(RingHom.comp (algebraMap ℝ A) toRealHom) r * x
[PROOFSTEP]
simp [← Algebra.smul_def (r : ℝ) x, smul_def]
[GOAL]
⊢ Algebra ℝ≥0 ℝ
[PROOFSTEP]
infer_instance
[GOAL]
⊢ DistribMulAction ℝ≥0ˣ ℝ
[PROOFSTEP]
infer_instance
[GOAL]
⊢ MonoidWithZero ℝ≥0
[PROOFSTEP]
infer_instance
[GOAL]
⊢ CommMonoidWithZero ℝ≥0
[PROOFSTEP]
infer_instance
[GOAL]
⊢ CommGroupWithZero ℝ≥0
[PROOFSTEP]
infer_instance
[GOAL]
α : Type u_1
s : Finset α
f : α → ℝ
hf : ∀ (a : α), a ∈ s → 0 ≤ f a
⊢ Real.toNNReal (∑ a in s, f a) = ∑ a in s, Real.toNNReal (f a)
[PROOFSTEP]
rw [← NNReal.coe_eq, NNReal.coe_sum, Real.coe_toNNReal _ (Finset.sum_nonneg hf)]
[GOAL]
α : Type u_1
s : Finset α
f : α → ℝ
hf : ∀ (a : α), a ∈ s → 0 ≤ f a
⊢ ∑ i in s, f i = ∑ a in s, ↑(Real.toNNReal (f a))
[PROOFSTEP]
exact Finset.sum_congr rfl fun x hxs => by rw [Real.coe_toNNReal _ (hf x hxs)]
[GOAL]
α : Type u_1
s : Finset α
f : α → ℝ
hf : ∀ (a : α), a ∈ s → 0 ≤ f a
x : α
hxs : x ∈ s
⊢ f x = ↑(Real.toNNReal (f x))
[PROOFSTEP]
rw [Real.coe_toNNReal _ (hf x hxs)]
[GOAL]
α : Type u_1
s : Finset α
f : α → ℝ
hf : ∀ (a : α), a ∈ s → 0 ≤ f a
⊢ Real.toNNReal (∏ a in s, f a) = ∏ a in s, Real.toNNReal (f a)
[PROOFSTEP]
rw [← NNReal.coe_eq, NNReal.coe_prod, Real.coe_toNNReal _ (Finset.prod_nonneg hf)]
[GOAL]
α : Type u_1
s : Finset α
f : α → ℝ
hf : ∀ (a : α), a ∈ s → 0 ≤ f a
⊢ ∏ i in s, f i = ∏ a in s, ↑(Real.toNNReal (f a))
[PROOFSTEP]
exact Finset.prod_congr rfl fun x hxs => by rw [Real.coe_toNNReal _ (hf x hxs)]
[GOAL]
α : Type u_1
s : Finset α
f : α → ℝ
hf : ∀ (a : α), a ∈ s → 0 ≤ f a
x : α
hxs : x ∈ s
⊢ f x = ↑(Real.toNNReal (f x))
[PROOFSTEP]
rw [Real.coe_toNNReal _ (hf x hxs)]
[GOAL]
⊢ LinearOrder ℝ≥0
[PROOFSTEP]
infer_instance
[GOAL]
n : ℕ
⊢ ↑(Real.toNNReal ↑n) = ↑↑n
[PROOFSTEP]
simp [Real.coe_toNNReal]
[GOAL]
⊢ OrderBot ℝ≥0
[PROOFSTEP]
infer_instance
[GOAL]
⊢ PartialOrder ℝ≥0
[PROOFSTEP]
infer_instance
[GOAL]
⊢ CanonicallyLinearOrderedAddMonoid ℝ≥0
[PROOFSTEP]
infer_instance
[GOAL]
⊢ LinearOrderedAddCommMonoid ℝ≥0
[PROOFSTEP]
infer_instance
[GOAL]
⊢ DistribLattice ℝ≥0
[PROOFSTEP]
infer_instance
[GOAL]
⊢ SemilatticeInf ℝ≥0
[PROOFSTEP]
infer_instance
[GOAL]
⊢ SemilatticeSup ℝ≥0
[PROOFSTEP]
infer_instance
[GOAL]
⊢ LinearOrderedSemiring ℝ≥0
[PROOFSTEP]
infer_instance
[GOAL]
⊢ OrderedCommSemiring ℝ≥0
[PROOFSTEP]
infer_instance
[GOAL]
⊢ LinearOrderedCommMonoid ℝ≥0
[PROOFSTEP]
infer_instance
[GOAL]
⊢ LinearOrderedCommMonoidWithZero ℝ≥0
[PROOFSTEP]
infer_instance
[GOAL]
⊢ LinearOrderedCommGroupWithZero ℝ≥0
[PROOFSTEP]
infer_instance
[GOAL]
⊢ CanonicallyOrderedCommSemiring ℝ≥0
[PROOFSTEP]
infer_instance
[GOAL]
⊢ DenselyOrdered ℝ≥0
[PROOFSTEP]
infer_instance
[GOAL]
⊢ NoMaxOrder ℝ≥0
[PROOFSTEP]
infer_instance
[GOAL]
ι : Sort u_1
s : ι → ℝ≥0
⊢ ↑(⨆ (i : ι), s i) = ⨆ (i : ι), ↑(s i)
[PROOFSTEP]
rw [iSup, iSup, coe_sSup, ← Set.range_comp]
[GOAL]
ι : Sort u_1
s : ι → ℝ≥0
⊢ sSup (Set.range (toReal ∘ fun i => s i)) = sSup (Set.range fun i => ↑(s i))
[PROOFSTEP]
rfl
[GOAL]
⊢ sInf ∅ = 0
[PROOFSTEP]
rw [← NNReal.coe_eq_zero, coe_sInf, Set.image_empty, Real.sInf_empty]
[GOAL]
ι : Sort u_1
s : ι → ℝ≥0
⊢ ↑(⨅ (i : ι), s i) = ⨅ (i : ι), ↑(s i)
[PROOFSTEP]
rw [iInf, iInf, coe_sInf, ← Set.range_comp]
[GOAL]
ι : Sort u_1
s : ι → ℝ≥0
⊢ sInf (Set.range (toReal ∘ fun i => s i)) = sInf (Set.range fun i => ↑(s i))
[PROOFSTEP]
rfl
[GOAL]
ι : Sort u_1
ι' : Sort u_2
inst✝¹ : Nonempty ι
inst✝ : Nonempty ι'
f : ι → ℝ≥0
g : ι' → ℝ≥0
a : ℝ≥0
h : ∀ (i : ι) (j : ι'), a ≤ f i + g j
⊢ a ≤ (⨅ (i : ι), f i) + ⨅ (j : ι'), g j
[PROOFSTEP]
rw [← NNReal.coe_le_coe, NNReal.coe_add, coe_iInf, coe_iInf]
[GOAL]
ι : Sort u_1
ι' : Sort u_2
inst✝¹ : Nonempty ι
inst✝ : Nonempty ι'
f : ι → ℝ≥0
g : ι' → ℝ≥0
a : ℝ≥0
h : ∀ (i : ι) (j : ι'), a ≤ f i + g j
⊢ ↑a ≤ (⨅ (i : ι), ↑(f i)) + ⨅ (i : ι'), ↑(g i)
[PROOFSTEP]
exact le_ciInf_add_ciInf h
[GOAL]
⊢ Archimedean ℝ≥0
[PROOFSTEP]
infer_instance
  -- porting note: TODO: remove?
[GOAL]
a b : ℝ≥0
h : ↑a < ↑b
q : ℚ
haq : ↑a < ↑q
hqb : ↑q < ↑b
this : 0 ≤ ↑q
⊢ a < Real.toNNReal ↑q ∧ Real.toNNReal ↑q < b
[PROOFSTEP]
simp [Real.coe_toNNReal _ this, NNReal.coe_lt_coe.symm, haq, hqb]
[GOAL]
α : Type u_1
f : α → ℝ≥0
s : Finset α
r : ℝ≥0
⊢ Finset.sup s f / r = Finset.sup s fun a => f a / r
[PROOFSTEP]
simp only [div_eq_inv_mul, mul_finset_sup]
[GOAL]
r : ℝ
⊢ 0 < toNNReal r ↔ 0 < r
[PROOFSTEP]
simp [← NNReal.coe_lt_coe, lt_irrefl]
[GOAL]
r : ℝ
⊢ toNNReal r = 0 ↔ r ≤ 0
[PROOFSTEP]
simpa [-toNNReal_pos] using not_iff_not.2 (@toNNReal_pos r)
[GOAL]
r p : ℝ
hp : 0 ≤ p
⊢ toNNReal r ≤ toNNReal p ↔ r ≤ p
[PROOFSTEP]
simp [← NNReal.coe_le_coe, hp]
[GOAL]
r p : ℝ
hr : 0 ≤ r
hp : 0 ≤ p
⊢ toNNReal r = toNNReal p ↔ r = p
[PROOFSTEP]
simp [← NNReal.coe_eq, coe_toNNReal, hr, hp]
[GOAL]
r p : ℝ
hr : 0 ≤ r
hp : 0 ≤ p
⊢ ↑(toNNReal (r + p)) = ↑(toNNReal r + toNNReal p)
[PROOFSTEP]
simp [hr, hp, add_nonneg]
[GOAL]
r : ℝ≥0
p : ℝ
hp : 0 ≤ p
⊢ r ≤ toNNReal p ↔ ↑r ≤ p
[PROOFSTEP]
rw [← NNReal.coe_le_coe, Real.coe_toNNReal p hp]
[GOAL]
r : ℝ≥0
p : ℝ
hr : 0 < r
hp : p < 0
⊢ r ≤ toNNReal p ↔ ↑r ≤ p
[PROOFSTEP]
simp only [(hp.trans_le r.coe_nonneg).not_le, toNNReal_eq_zero.2 hp.le, hr.not_le]
[GOAL]
r : ℝ
p : ℝ≥0
ha : 0 ≤ r
⊢ toNNReal r < p ↔ r < ↑p
[PROOFSTEP]
rw [← NNReal.coe_lt_coe, Real.coe_toNNReal r ha]
[GOAL]
x : ℝ
hx : 0 ≤ x
n : ℕ
⊢ toNNReal (x ^ n) = toNNReal x ^ n
[PROOFSTEP]
rw [← NNReal.coe_eq, NNReal.coe_pow, Real.coe_toNNReal _ (pow_nonneg hx _), Real.coe_toNNReal x hx]
[GOAL]
p q : ℝ
hp : 0 ≤ p
⊢ ↑(toNNReal (p * q)) = ↑(toNNReal p * toNNReal q)
[PROOFSTEP]
simp [mul_max_of_nonneg, hp]
[GOAL]
a b c : ℝ≥0
h : a ≠ 0
⊢ a * b = a * c ↔ b = c
[PROOFSTEP]
rw [mul_eq_mul_left_iff, or_iff_left h]
[GOAL]
a b : ℝ≥0
ha : 0 < a
hb : b < 1
⊢ ∃ n, b ^ n < a
[PROOFSTEP]
simpa only [← coe_pow, NNReal.coe_lt_coe] using exists_pow_lt_of_lt_one (NNReal.coe_pos.2 ha) (NNReal.coe_lt_coe.2 hb)
[GOAL]
⊢ OrderedSub ℝ≥0
[PROOFSTEP]
infer_instance
[GOAL]
r p : ℝ≥0
h : r ≠ 0
⊢ r⁻¹ ≤ p ↔ 1 ≤ r * p
[PROOFSTEP]
rw [← mul_le_mul_left (pos_iff_ne_zero.2 h), mul_inv_cancel h]
[GOAL]
r p : ℝ≥0
h : 1 ≤ r * p
⊢ r⁻¹ ≤ p
[PROOFSTEP]
by_cases r = 0
[GOAL]
r p : ℝ≥0
h : 1 ≤ r * p
⊢ r⁻¹ ≤ p
[PROOFSTEP]
by_cases r = 0
[GOAL]
case pos
r p : ℝ≥0
h✝ : 1 ≤ r * p
h : r = 0
⊢ r⁻¹ ≤ p
[PROOFSTEP]
simp [*, inv_le]
[GOAL]
case neg
r p : ℝ≥0
h✝ : 1 ≤ r * p
h : ¬r = 0
⊢ r⁻¹ ≤ p
[PROOFSTEP]
simp [*, inv_le]
[GOAL]
r p : ℝ≥0
h : p ≠ 0
⊢ r ≤ p⁻¹ ↔ r * p ≤ 1
[PROOFSTEP]
rw [← mul_le_mul_left (pos_iff_ne_zero.2 h), mul_inv_cancel h, mul_comm]
[GOAL]
r p : ℝ≥0
h : p ≠ 0
⊢ r < p⁻¹ ↔ r * p < 1
[PROOFSTEP]
rw [← mul_lt_mul_left (pos_iff_ne_zero.2 h), mul_inv_cancel h, mul_comm]
[GOAL]
a b r : ℝ≥0
hr : r ≠ 0
⊢ r * a ≤ b ↔ a ≤ r⁻¹ * b
[PROOFSTEP]
have : 0 < r := lt_of_le_of_ne (zero_le r) hr.symm
[GOAL]
a b r : ℝ≥0
hr : r ≠ 0
this : 0 < r
⊢ r * a ≤ b ↔ a ≤ r⁻¹ * b
[PROOFSTEP]
rw [← mul_le_mul_left (inv_pos.mpr this), ← mul_assoc, inv_mul_cancel hr, one_mul]
[GOAL]
a b c : ℝ≥0
h : a ≤ b * c
h0 : c = 0
⊢ a / c ≤ b
[PROOFSTEP]
simp [h0]
[GOAL]
a b r : ℝ≥0
h : a < b / r
hr : r = 0
⊢ False
[PROOFSTEP]
simp [hr] at h 
[GOAL]
x y : ℝ≥0
h : ∀ (a : ℝ≥0), a < 1 → a * x ≤ y
a : ℝ≥0
ha : a < x
⊢ a ≤ y
[PROOFSTEP]
have hx : x ≠ 0 := pos_iff_ne_zero.1 (lt_of_le_of_lt (zero_le _) ha)
[GOAL]
x y : ℝ≥0
h : ∀ (a : ℝ≥0), a < 1 → a * x ≤ y
a : ℝ≥0
ha : a < x
hx : x ≠ 0
⊢ a ≤ y
[PROOFSTEP]
have hx' : x⁻¹ ≠ 0 := by rwa [Ne.def, inv_eq_zero]
[GOAL]
x y : ℝ≥0
h : ∀ (a : ℝ≥0), a < 1 → a * x ≤ y
a : ℝ≥0
ha : a < x
hx : x ≠ 0
⊢ x⁻¹ ≠ 0
[PROOFSTEP]
rwa [Ne.def, inv_eq_zero]
[GOAL]
x y : ℝ≥0
h : ∀ (a : ℝ≥0), a < 1 → a * x ≤ y
a : ℝ≥0
ha : a < x
hx : x ≠ 0
hx' : x⁻¹ ≠ 0
⊢ a ≤ y
[PROOFSTEP]
have : a * x⁻¹ < 1 := by rwa [← lt_inv_iff_mul_lt hx', inv_inv]
[GOAL]
x y : ℝ≥0
h : ∀ (a : ℝ≥0), a < 1 → a * x ≤ y
a : ℝ≥0
ha : a < x
hx : x ≠ 0
hx' : x⁻¹ ≠ 0
⊢ a * x⁻¹ < 1
[PROOFSTEP]
rwa [← lt_inv_iff_mul_lt hx', inv_inv]
[GOAL]
x y : ℝ≥0
h : ∀ (a : ℝ≥0), a < 1 → a * x ≤ y
a : ℝ≥0
ha : a < x
hx : x ≠ 0
hx' : x⁻¹ ≠ 0
this : a * x⁻¹ < 1
⊢ a ≤ y
[PROOFSTEP]
have : a * x⁻¹ * x ≤ y := h _ this
[GOAL]
x y : ℝ≥0
h : ∀ (a : ℝ≥0), a < 1 → a * x ≤ y
a : ℝ≥0
ha : a < x
hx : x ≠ 0
hx' : x⁻¹ ≠ 0
this✝ : a * x⁻¹ < 1
this : a * x⁻¹ * x ≤ y
⊢ a ≤ y
[PROOFSTEP]
rwa [mul_assoc, inv_mul_cancel hx, mul_one] at this 
[GOAL]
a b : ℝ≥0
h : a < b
⊢ a / b < 1
[PROOFSTEP]
rwa [div_lt_iff, one_mul]
[GOAL]
a b : ℝ≥0
h : a < b
⊢ b ≠ 0
[PROOFSTEP]
exact ne_of_gt (lt_of_le_of_lt (zero_le _) h)
[GOAL]
x : ℝ
⊢ toNNReal x⁻¹ = (toNNReal x)⁻¹
[PROOFSTEP]
cases' le_total 0 x with hx hx
[GOAL]
case inl
x : ℝ
hx : 0 ≤ x
⊢ toNNReal x⁻¹ = (toNNReal x)⁻¹
[PROOFSTEP]
nth_rw 1 [← Real.coe_toNNReal x hx]
[GOAL]
case inl
x : ℝ
hx : 0 ≤ x
⊢ toNNReal (↑(toNNReal x))⁻¹ = (toNNReal x)⁻¹
[PROOFSTEP]
rw [← NNReal.coe_inv, Real.toNNReal_coe]
[GOAL]
case inr
x : ℝ
hx : x ≤ 0
⊢ toNNReal x⁻¹ = (toNNReal x)⁻¹
[PROOFSTEP]
rw [toNNReal_eq_zero.mpr hx, inv_zero, toNNReal_eq_zero.mpr (inv_nonpos.mpr hx)]
[GOAL]
x y : ℝ
hx : 0 ≤ x
⊢ toNNReal (x / y) = toNNReal x / toNNReal y
[PROOFSTEP]
rw [div_eq_mul_inv, div_eq_mul_inv, ← Real.toNNReal_inv, ← Real.toNNReal_mul hx]
[GOAL]
x y : ℝ
hy : 0 ≤ y
⊢ toNNReal (x / y) = toNNReal x / toNNReal y
[PROOFSTEP]
rw [div_eq_inv_mul, div_eq_inv_mul, Real.toNNReal_mul (inv_nonneg.2 hy), Real.toNNReal_inv]
[GOAL]
x : ℝ≥0
hx : x ≠ 0
⊢ x⁻¹ < 1 ↔ 1 < x
[PROOFSTEP]
rw [← one_div, div_lt_iff hx, one_mul]
[GOAL]
ι : Sort u_1
f : ι → ℝ≥0
s : Set ℝ≥0
hs : ¬BddAbove s
⊢ sSup s = 0
[PROOFSTEP]
rw [← bddAbove_coe] at hs 
[GOAL]
ι : Sort u_1
f : ι → ℝ≥0
s : Set ℝ≥0
hs : ¬BddAbove (toReal '' s)
⊢ sSup s = 0
[PROOFSTEP]
rw [← NNReal.coe_eq, coe_sSup, NNReal.coe_zero]
[GOAL]
ι : Sort u_1
f : ι → ℝ≥0
s : Set ℝ≥0
hs : ¬BddAbove (toReal '' s)
⊢ sSup (toReal '' s) = 0
[PROOFSTEP]
exact sSup_of_not_bddAbove hs
[GOAL]
ι : Sort u_1
f✝ : ι → ℝ≥0
inst✝ : IsEmpty ι
f : ι → ℝ≥0
⊢ ⨅ (i : ι), f i = 0
[PROOFSTEP]
rw [iInf_of_empty', sInf_empty]
[GOAL]
ι : Sort u_1
f : ι → ℝ≥0
α : Sort u_2
⊢ ⨅ (x : α), 0 = 0
[PROOFSTEP]
rw [← NNReal.coe_eq, coe_iInf]
[GOAL]
ι : Sort u_1
f : ι → ℝ≥0
α : Sort u_2
⊢ ⨅ (i : α), ↑0 = ↑0
[PROOFSTEP]
exact Real.ciInf_const_zero
[GOAL]
ι : Sort u_1
f✝ f : ι → ℝ≥0
a : ℝ≥0
⊢ iInf f * a = ⨅ (i : ι), f i * a
[PROOFSTEP]
rw [← NNReal.coe_eq, NNReal.coe_mul, coe_iInf, coe_iInf]
[GOAL]
ι : Sort u_1
f✝ f : ι → ℝ≥0
a : ℝ≥0
⊢ (⨅ (i : ι), ↑(f i)) * ↑a = ⨅ (i : ι), ↑(f i * a)
[PROOFSTEP]
exact Real.iInf_mul_of_nonneg (NNReal.coe_nonneg _) _
[GOAL]
ι : Sort u_1
f✝ f : ι → ℝ≥0
a : ℝ≥0
⊢ a * iInf f = ⨅ (i : ι), a * f i
[PROOFSTEP]
simpa only [mul_comm] using iInf_mul f a
[GOAL]
ι : Sort u_1
f✝ f : ι → ℝ≥0
a : ℝ≥0
⊢ a * ⨆ (i : ι), f i = ⨆ (i : ι), a * f i
[PROOFSTEP]
rw [← NNReal.coe_eq, NNReal.coe_mul, NNReal.coe_iSup, NNReal.coe_iSup]
[GOAL]
ι : Sort u_1
f✝ f : ι → ℝ≥0
a : ℝ≥0
⊢ ↑a * ⨆ (i : ι), ↑(f i) = ⨆ (i : ι), ↑(a * f i)
[PROOFSTEP]
exact Real.mul_iSup_of_nonneg (NNReal.coe_nonneg _) _
[GOAL]
ι : Sort u_1
f✝ f : ι → ℝ≥0
a : ℝ≥0
⊢ (⨆ (i : ι), f i) * a = ⨆ (i : ι), f i * a
[PROOFSTEP]
rw [mul_comm, mul_iSup]
[GOAL]
ι : Sort u_1
f✝ f : ι → ℝ≥0
a : ℝ≥0
⊢ ⨆ (i : ι), a * f i = ⨆ (i : ι), f i * a
[PROOFSTEP]
simp_rw [mul_comm]
[GOAL]
ι : Sort u_1
f✝ f : ι → ℝ≥0
a : ℝ≥0
⊢ (⨆ (i : ι), f i) / a = ⨆ (i : ι), f i / a
[PROOFSTEP]
simp only [div_eq_mul_inv, iSup_mul]
[GOAL]
ι : Sort u_1
f : ι → ℝ≥0
a g : ℝ≥0
h : ι → ℝ≥0
H : ∀ (j : ι), g * h j ≤ a
⊢ g * iSup h ≤ a
[PROOFSTEP]
rw [mul_iSup]
[GOAL]
ι : Sort u_1
f : ι → ℝ≥0
a g : ℝ≥0
h : ι → ℝ≥0
H : ∀ (j : ι), g * h j ≤ a
⊢ ⨆ (i : ι), g * h i ≤ a
[PROOFSTEP]
exact ciSup_le' H
[GOAL]
ι : Sort u_1
f : ι → ℝ≥0
a : ℝ≥0
g : ι → ℝ≥0
h : ℝ≥0
H : ∀ (i : ι), g i * h ≤ a
⊢ iSup g * h ≤ a
[PROOFSTEP]
rw [iSup_mul]
[GOAL]
ι : Sort u_1
f : ι → ℝ≥0
a : ℝ≥0
g : ι → ℝ≥0
h : ℝ≥0
H : ∀ (i : ι), g i * h ≤ a
⊢ ⨆ (i : ι), g i * h ≤ a
[PROOFSTEP]
exact ciSup_le' H
[GOAL]
ι : Sort u_1
f : ι → ℝ≥0
inst✝ : Nonempty ι
a g : ℝ≥0
h : ι → ℝ≥0
H : ∀ (j : ι), a ≤ g * h j
⊢ a ≤ g * iInf h
[PROOFSTEP]
rw [mul_iInf]
[GOAL]
ι : Sort u_1
f : ι → ℝ≥0
inst✝ : Nonempty ι
a g : ℝ≥0
h : ι → ℝ≥0
H : ∀ (j : ι), a ≤ g * h j
⊢ a ≤ ⨅ (i : ι), g * h i
[PROOFSTEP]
exact le_ciInf H
[GOAL]
ι : Sort u_1
f : ι → ℝ≥0
inst✝ : Nonempty ι
a : ℝ≥0
g : ι → ℝ≥0
h : ℝ≥0
H : ∀ (i : ι), a ≤ g i * h
⊢ a ≤ iInf g * h
[PROOFSTEP]
rw [iInf_mul]
[GOAL]
ι : Sort u_1
f : ι → ℝ≥0
inst✝ : Nonempty ι
a : ℝ≥0
g : ι → ℝ≥0
h : ℝ≥0
H : ∀ (i : ι), a ≤ g i * h
⊢ a ≤ ⨅ (i : ι), g i * h
[PROOFSTEP]
exact le_ciInf H
[GOAL]
s : Set ℝ
t : Set ℝ≥0
h : OrdConnected s
⊢ OrdConnected (toNNReal '' s)
[PROOFSTEP]
refine' ⟨ball_image_iff.2 fun x hx => ball_image_iff.2 fun y hy z hz => _⟩
[GOAL]
s : Set ℝ
t : Set ℝ≥0
h : OrdConnected s
x : ℝ
hx : x ∈ s
y : ℝ
hy : y ∈ s
z : ℝ≥0
hz : z ∈ Icc (toNNReal x) (toNNReal y)
⊢ z ∈ toNNReal '' s
[PROOFSTEP]
cases' le_total y 0 with hy₀ hy₀
[GOAL]
case inl
s : Set ℝ
t : Set ℝ≥0
h : OrdConnected s
x : ℝ
hx : x ∈ s
y : ℝ
hy : y ∈ s
z : ℝ≥0
hz : z ∈ Icc (toNNReal x) (toNNReal y)
hy₀ : y ≤ 0
⊢ z ∈ toNNReal '' s
[PROOFSTEP]
rw [mem_Icc, Real.toNNReal_of_nonpos hy₀, nonpos_iff_eq_zero] at hz 
[GOAL]
case inl
s : Set ℝ
t : Set ℝ≥0
h : OrdConnected s
x : ℝ
hx : x ∈ s
y : ℝ
hy : y ∈ s
z : ℝ≥0
hz : toNNReal x ≤ z ∧ z = 0
hy₀ : y ≤ 0
⊢ z ∈ toNNReal '' s
[PROOFSTEP]
exact ⟨y, hy, (toNNReal_of_nonpos hy₀).trans hz.2.symm⟩
[GOAL]
case inr
s : Set ℝ
t : Set ℝ≥0
h : OrdConnected s
x : ℝ
hx : x ∈ s
y : ℝ
hy : y ∈ s
z : ℝ≥0
hz : z ∈ Icc (toNNReal x) (toNNReal y)
hy₀ : 0 ≤ y
⊢ z ∈ toNNReal '' s
[PROOFSTEP]
lift y to ℝ≥0 using hy₀
[GOAL]
case inr.intro
s : Set ℝ
t : Set ℝ≥0
h : OrdConnected s
x : ℝ
hx : x ∈ s
z y : ℝ≥0
hy : ↑y ∈ s
hz : z ∈ Icc (toNNReal x) (toNNReal ↑y)
⊢ z ∈ toNNReal '' s
[PROOFSTEP]
rw [toNNReal_coe] at hz 
[GOAL]
case inr.intro
s : Set ℝ
t : Set ℝ≥0
h : OrdConnected s
x : ℝ
hx : x ∈ s
z y : ℝ≥0
hy : ↑y ∈ s
hz : z ∈ Icc (toNNReal x) y
⊢ z ∈ toNNReal '' s
[PROOFSTEP]
exact ⟨z, h.out hx hy ⟨toNNReal_le_iff_le_coe.1 hz.1, hz.2⟩, toNNReal_coe⟩
[GOAL]
⊢ (fun x => { val := |x|, property := (_ : 0 ≤ |x|) }) 0 = 0
[PROOFSTEP]
ext
[GOAL]
case a
⊢ ↑((fun x => { val := |x|, property := (_ : 0 ≤ |x|) }) 0) = ↑0
[PROOFSTEP]
simp
[GOAL]
⊢ ZeroHom.toFun
      { toFun := fun x => { val := |x|, property := (_ : 0 ≤ |x|) },
        map_zero' := (_ : (fun x => { val := |x|, property := (_ : 0 ≤ |x|) }) 0 = 0) }
      1 =
    1
[PROOFSTEP]
ext
[GOAL]
case a
⊢ ↑(ZeroHom.toFun
        { toFun := fun x => { val := |x|, property := (_ : 0 ≤ |x|) },
          map_zero' := (_ : (fun x => { val := |x|, property := (_ : 0 ≤ |x|) }) 0 = 0) }
        1) =
    ↑1
[PROOFSTEP]
simp
[GOAL]
x y : ℝ
⊢ ZeroHom.toFun
      { toFun := fun x => { val := |x|, property := (_ : 0 ≤ |x|) },
        map_zero' := (_ : (fun x => { val := |x|, property := (_ : 0 ≤ |x|) }) 0 = 0) }
      (x * y) =
    ZeroHom.toFun
        { toFun := fun x => { val := |x|, property := (_ : 0 ≤ |x|) },
          map_zero' := (_ : (fun x => { val := |x|, property := (_ : 0 ≤ |x|) }) 0 = 0) }
        x *
      ZeroHom.toFun
        { toFun := fun x => { val := |x|, property := (_ : 0 ≤ |x|) },
          map_zero' := (_ : (fun x => { val := |x|, property := (_ : 0 ≤ |x|) }) 0 = 0) }
        y
[PROOFSTEP]
ext
[GOAL]
case a
x y : ℝ
⊢ ↑(ZeroHom.toFun
        { toFun := fun x => { val := |x|, property := (_ : 0 ≤ |x|) },
          map_zero' := (_ : (fun x => { val := |x|, property := (_ : 0 ≤ |x|) }) 0 = 0) }
        (x * y)) =
    ↑(ZeroHom.toFun
          { toFun := fun x => { val := |x|, property := (_ : 0 ≤ |x|) },
            map_zero' := (_ : (fun x => { val := |x|, property := (_ : 0 ≤ |x|) }) 0 = 0) }
          x *
        ZeroHom.toFun
          { toFun := fun x => { val := |x|, property := (_ : 0 ≤ |x|) },
            map_zero' := (_ : (fun x => { val := |x|, property := (_ : 0 ≤ |x|) }) 0 = 0) }
          y)
[PROOFSTEP]
simp [abs_mul]
[GOAL]
x : ℝ
h : 0 ≤ x
⊢ ↑nnabs x = toNNReal x
[PROOFSTEP]
ext
[GOAL]
case a
x : ℝ
h : 0 ≤ x
⊢ ↑(↑nnabs x) = ↑(toNNReal x)
[PROOFSTEP]
rw [coe_toNNReal x h, coe_nnabs, abs_of_nonneg h]
[GOAL]
x : ℝ≥0
⊢ ↑nnabs ↑x = x
[PROOFSTEP]
simp
[GOAL]
n : ℤ
⊢ ↑(Int.natAbs n) = ↑nnabs ↑n
[PROOFSTEP]
ext
[GOAL]
case a
n : ℤ
⊢ ↑↑(Int.natAbs n) = ↑(↑nnabs ↑n)
[PROOFSTEP]
rw [NNReal.coe_nat_cast, Int.cast_natAbs, Real.coe_nnabs, Int.cast_abs]
