[GOAL]
α : Type u_1
β : Type u_2
a✝ b c d : ℝ≥0∞
r p q : ℝ≥0
a : AddUnits ℝ≥0∞
⊢ ↑a ≤ 0
[PROOFSTEP]
rw [← a.add_neg]
[GOAL]
α : Type u_1
β : Type u_2
a✝ b c d : ℝ≥0∞
r p q : ℝ≥0
a : AddUnits ℝ≥0∞
⊢ ↑a ≤ ↑a + ↑(-a)
[PROOFSTEP]
exact le_self_add
[GOAL]
α : Type u_1
β : Type u_2
a✝ b c d : ℝ≥0∞
r p q : ℝ≥0
a : ℝ≥0∞
h : a ≠ ⊤
⊢ ENNReal.ofReal (ENNReal.toReal a) = a
[PROOFSTEP]
simp [ENNReal.toReal, ENNReal.ofReal, h]
[GOAL]
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r✝ p q r : ℝ≥0
⊢ ↑(ENNReal.toNNReal ↑r) ≤ ↑r
[PROOFSTEP]
rw [toNNReal_coe]
[GOAL]
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r✝ p q r : ℝ≥0
⊢ ↑r = ENNReal.ofReal ↑r
[PROOFSTEP]
rw [ENNReal.ofReal, Real.toNNReal_coe]
[GOAL]
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p q : ℝ≥0
⊢ ENNReal.ofReal 0 = 0
[PROOFSTEP]
simp [ENNReal.ofReal]
[GOAL]
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p q : ℝ≥0
⊢ ENNReal.ofReal 1 = 1
[PROOFSTEP]
simp [ENNReal.ofReal]
[GOAL]
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p✝ q : ℝ≥0
p : ℝ≥0∞ → Prop
⊢ (∃ a, a ≠ ⊤ ∧ p a) ↔ ∃ r, p ↑r
[PROOFSTEP]
simp only [exists_ne_top', ← exists_prop]
[GOAL]
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p q : ℝ≥0
x : ℝ≥0∞
⊢ ENNReal.toReal x = 0 ↔ x = 0 ∨ x = ⊤
[PROOFSTEP]
simp [ENNReal.toReal, toNNReal_eq_zero_iff]
[GOAL]
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p q : ℝ≥0
x : ℝ≥0∞
⊢ x = ↑1 ∨ x = ⊤ ∧ 1 = 0 ↔ x = 1
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p q : ℝ≥0
x : ℝ≥0∞
⊢ ENNReal.toReal x = 1 ↔ x = 1
[PROOFSTEP]
rw [ENNReal.toReal, NNReal.coe_eq_one, ENNReal.toNNReal_eq_one_iff]
[GOAL]
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p q : ℝ≥0
h : ENNReal.ofReal (ENNReal.toReal a) = a
⊢ a ≠ ⊤
[PROOFSTEP]
rw [← h]
[GOAL]
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p q : ℝ≥0
h : ENNReal.ofReal (ENNReal.toReal a) = a
⊢ ENNReal.ofReal (ENNReal.toReal a) ≠ ⊤
[PROOFSTEP]
exact ofReal_ne_top
[GOAL]
α : Type u_1
β : Type u_2
a✝ b c d : ℝ≥0∞
r p q : ℝ≥0
a : ℝ
h : ENNReal.toReal (ENNReal.ofReal a) = a
⊢ 0 ≤ a
[PROOFSTEP]
rw [← h]
[GOAL]
α : Type u_1
β : Type u_2
a✝ b c d : ℝ≥0∞
r p q : ℝ≥0
a : ℝ
h : ENNReal.toReal (ENNReal.ofReal a) = a
⊢ 0 ≤ ENNReal.toReal (ENNReal.ofReal a)
[PROOFSTEP]
exact toReal_nonneg
[GOAL]
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p q : ℝ≥0
x y : ℝ≥0∞
⊢ ENNReal.toReal x = ENNReal.toReal y ↔ x = y ∨ x = 0 ∧ y = ⊤ ∨ x = ⊤ ∧ y = 0
[PROOFSTEP]
simp only [ENNReal.toReal, NNReal.coe_eq, toNNReal_eq_toNNReal_iff]
[GOAL]
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p q : ℝ≥0
x y : ℝ≥0∞
hx : x ≠ ⊤
hy : y ≠ ⊤
⊢ ENNReal.toNNReal x = ENNReal.toNNReal y ↔ x = y
[PROOFSTEP]
simp only [ENNReal.toNNReal_eq_toNNReal_iff x y, hx, hy, and_false, false_and, or_false]
[GOAL]
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p q : ℝ≥0
x y : ℝ≥0∞
hx : x ≠ ⊤
hy : y ≠ ⊤
⊢ ENNReal.toReal x = ENNReal.toReal y ↔ x = y
[PROOFSTEP]
simp only [ENNReal.toReal, NNReal.coe_eq, toNNReal_eq_toNNReal_iff' hx hy]
[GOAL]
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p q : ℝ≥0
⊢ ↑1 < ↑2
[PROOFSTEP]
exact_mod_cast (one_lt_two : 1 < 2)
[GOAL]
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p q : ℝ≥0
inst✝ : CompleteLattice α
f : ℝ≥0∞ → α
⊢ ⨅ (x : ℝ≥0∞) (_ : x ≠ ⊤), f x = ⨅ (x : ℝ≥0), f ↑x
[PROOFSTEP]
rw [iInf_subtype', cinfi_ne_top]
[GOAL]
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r✝ p q : ℝ≥0
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra ℝ≥0∞ A
r : ℝ≥0
x : (fun x => A) r
⊢ ↑(RingHom.comp (algebraMap ℝ≥0∞ A) ofNNRealHom) r * x = x * ↑(RingHom.comp (algebraMap ℝ≥0∞ A) ofNNRealHom) r
[PROOFSTEP]
simp [Algebra.commutes]
[GOAL]
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r✝ p q : ℝ≥0
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra ℝ≥0∞ A
r : ℝ≥0
x : (fun x => A) r
⊢ r • x = ↑(RingHom.comp (algebraMap ℝ≥0∞ A) ofNNRealHom) r * x
[PROOFSTEP]
simp [← Algebra.smul_def (r : ℝ≥0∞) x, smul_def]
[GOAL]
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r✝ p q : ℝ≥0
R : Type u_3
r : R
s : ℝ≥0
inst✝³ : SMul R ℝ≥0
inst✝² : SMul R ℝ≥0∞
inst✝¹ : IsScalarTower R ℝ≥0 ℝ≥0
inst✝ : IsScalarTower R ℝ≥0 ℝ≥0∞
⊢ ↑(r • s) = r • ↑s
[PROOFSTEP]
rw [← smul_one_smul ℝ≥0 r (s : ℝ≥0∞), smul_def, smul_eq_mul, ← ENNReal.coe_mul, smul_mul_assoc, one_mul]
[GOAL]
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p q : ℝ≥0
r₁ r₂ : ℝ≥0∞
h₁ : r₁ ≠ ⊤
h₂ : r₂ ≠ ⊤
⊢ ENNReal.toNNReal (r₁ + r₂) = ENNReal.toNNReal r₁ + ENNReal.toNNReal r₂
[PROOFSTEP]
lift r₁ to ℝ≥0 using h₁
[GOAL]
case intro
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p q : ℝ≥0
r₂ : ℝ≥0∞
h₂ : r₂ ≠ ⊤
r₁ : ℝ≥0
⊢ ENNReal.toNNReal (↑r₁ + r₂) = ENNReal.toNNReal ↑r₁ + ENNReal.toNNReal r₂
[PROOFSTEP]
lift r₂ to ℝ≥0 using h₂
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p q r₁ r₂ : ℝ≥0
⊢ ENNReal.toNNReal (↑r₁ + ↑r₂) = ENNReal.toNNReal ↑r₁ + ENNReal.toNNReal ↑r₂
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p q : ℝ≥0
x : ℝ≥0∞
⊢ ¬x < ⊤ ↔ x = ⊤
[PROOFSTEP]
rw [lt_top_iff_ne_top, Classical.not_not]
[GOAL]
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p q : ℝ≥0
⊢ a + b ≠ ⊤ ↔ a ≠ ⊤ ∧ b ≠ ⊤
[PROOFSTEP]
simpa only [lt_top_iff_ne_top] using add_lt_top
[GOAL]
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p q : ℝ≥0
⊢ a * ⊤ = if a = 0 then 0 else ⊤
[PROOFSTEP]
convert WithTop.mul_top' a
[GOAL]
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p q : ℝ≥0
⊢ ⊤ * a = if a = 0 then 0 else ⊤
[PROOFSTEP]
convert WithTop.top_mul' a
[GOAL]
α : Type u_1
β : Type u_2
a b c✝ d : ℝ≥0∞
r p q : ℝ≥0
R : Type u_3
inst✝⁴ : Zero R
inst✝³ : SMulWithZero R ℝ≥0∞
inst✝² : IsScalarTower R ℝ≥0∞ ℝ≥0∞
inst✝¹ : NoZeroSMulDivisors R ℝ≥0∞
inst✝ : DecidableEq R
c : R
⊢ c • ⊤ = if c = 0 then 0 else ⊤
[PROOFSTEP]
rw [← smul_one_mul, mul_top']
  -- porting note: need the primed version of `one_ne_zero` now
[GOAL]
α : Type u_1
β : Type u_2
a b c✝ d : ℝ≥0∞
r p q : ℝ≥0
R : Type u_3
inst✝⁴ : Zero R
inst✝³ : SMulWithZero R ℝ≥0∞
inst✝² : IsScalarTower R ℝ≥0∞ ℝ≥0∞
inst✝¹ : NoZeroSMulDivisors R ℝ≥0∞
inst✝ : DecidableEq R
c : R
⊢ (if c • 1 = 0 then 0 else ⊤) = if c = 0 then 0 else ⊤
[PROOFSTEP]
simp_rw [smul_eq_zero, or_iff_left (one_ne_zero' ℝ≥0∞)]
[GOAL]
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p q : ℝ≥0
n : ℕ
h : 0 < n
m : ℕ
x✝ : Nat.succ 0 ≤ m
hm : ⊤ ^ m = ⊤
⊢ ⊤ ^ (m + 1) = ⊤
[PROOFSTEP]
rw [pow_succ, hm, top_mul_top]
[GOAL]
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p q : ℝ≥0
⊢ a ≠ ⊤ → b ≠ ⊤ → a * b ≠ ⊤
[PROOFSTEP]
simpa only [lt_top_iff_ne_top] using mul_lt_top
[GOAL]
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p q : ℝ≥0
h : a * b ≠ ⊤
ha : a ≠ 0
⊢ b * a ≠ ⊤
[PROOFSTEP]
rwa [mul_comm]
[GOAL]
α : Type u_1
β : Type u_2
a✝ b✝ c d : ℝ≥0∞
r p q : ℝ≥0
a b : ℝ≥0∞
⊢ a * b < ⊤ ↔ a < ⊤ ∧ b < ⊤ ∨ a = 0 ∨ b = 0
[PROOFSTEP]
constructor
[GOAL]
case mp
α : Type u_1
β : Type u_2
a✝ b✝ c d : ℝ≥0∞
r p q : ℝ≥0
a b : ℝ≥0∞
⊢ a * b < ⊤ → a < ⊤ ∧ b < ⊤ ∨ a = 0 ∨ b = 0
[PROOFSTEP]
intro h
[GOAL]
case mp
α : Type u_1
β : Type u_2
a✝ b✝ c d : ℝ≥0∞
r p q : ℝ≥0
a b : ℝ≥0∞
h : a * b < ⊤
⊢ a < ⊤ ∧ b < ⊤ ∨ a = 0 ∨ b = 0
[PROOFSTEP]
rw [← or_assoc, or_iff_not_imp_right, or_iff_not_imp_right]
[GOAL]
case mp
α : Type u_1
β : Type u_2
a✝ b✝ c d : ℝ≥0∞
r p q : ℝ≥0
a b : ℝ≥0∞
h : a * b < ⊤
⊢ ¬b = 0 → ¬a = 0 → a < ⊤ ∧ b < ⊤
[PROOFSTEP]
intro hb ha
[GOAL]
case mp
α : Type u_1
β : Type u_2
a✝ b✝ c d : ℝ≥0∞
r p q : ℝ≥0
a b : ℝ≥0∞
h : a * b < ⊤
hb : ¬b = 0
ha : ¬a = 0
⊢ a < ⊤ ∧ b < ⊤
[PROOFSTEP]
exact ⟨lt_top_of_mul_ne_top_left h.ne hb, lt_top_of_mul_ne_top_right h.ne ha⟩
[GOAL]
case mpr
α : Type u_1
β : Type u_2
a✝ b✝ c d : ℝ≥0∞
r p q : ℝ≥0
a b : ℝ≥0∞
⊢ a < ⊤ ∧ b < ⊤ ∨ a = 0 ∨ b = 0 → a * b < ⊤
[PROOFSTEP]
rintro (⟨ha, hb⟩ | rfl | rfl) <;> [exact mul_lt_top ha.ne hb.ne; simp; simp]
[GOAL]
case mpr
α : Type u_1
β : Type u_2
a✝ b✝ c d : ℝ≥0∞
r p q : ℝ≥0
a b : ℝ≥0∞
⊢ a < ⊤ ∧ b < ⊤ ∨ a = 0 ∨ b = 0 → a * b < ⊤
[PROOFSTEP]
rintro (⟨ha, hb⟩ | rfl | rfl)
[GOAL]
case mpr.inl.intro
α : Type u_1
β : Type u_2
a✝ b✝ c d : ℝ≥0∞
r p q : ℝ≥0
a b : ℝ≥0∞
ha : a < ⊤
hb : b < ⊤
⊢ a * b < ⊤
[PROOFSTEP]
exact mul_lt_top ha.ne hb.ne
[GOAL]
case mpr.inr.inl
α : Type u_1
β : Type u_2
a b✝ c d : ℝ≥0∞
r p q : ℝ≥0
b : ℝ≥0∞
⊢ 0 * b < ⊤
[PROOFSTEP]
simp
[GOAL]
case mpr.inr.inr
α : Type u_1
β : Type u_2
a✝ b c d : ℝ≥0∞
r p q : ℝ≥0
a : ℝ≥0∞
⊢ a * 0 < ⊤
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
a✝ b c d : ℝ≥0∞
r p q : ℝ≥0
a : ℝ≥0∞
⊢ a * a < ⊤ ↔ a < ⊤
[PROOFSTEP]
rw [ENNReal.mul_lt_top_iff, and_self, or_self, or_iff_left_iff_imp]
[GOAL]
α : Type u_1
β : Type u_2
a✝ b c d : ℝ≥0∞
r p q : ℝ≥0
a : ℝ≥0∞
⊢ a = 0 → a < ⊤
[PROOFSTEP]
rintro rfl
[GOAL]
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p q : ℝ≥0
⊢ 0 < ⊤
[PROOFSTEP]
norm_num
[GOAL]
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p q : ℝ≥0
n : ℕ
⊢ a ^ n = ⊤ ↔ a = ⊤ ∧ n ≠ 0
[PROOFSTEP]
rcases n.eq_zero_or_pos with rfl | (hn : 0 < n)
[GOAL]
case inl
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p q : ℝ≥0
⊢ a ^ 0 = ⊤ ↔ a = ⊤ ∧ 0 ≠ 0
[PROOFSTEP]
simp
[GOAL]
case inr
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p q : ℝ≥0
n : ℕ
hn : 0 < n
⊢ a ^ n = ⊤ ↔ a = ⊤ ∧ n ≠ 0
[PROOFSTEP]
induction a using recTopCoe
[GOAL]
case inr.top
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p q : ℝ≥0
n : ℕ
hn : 0 < n
⊢ ⊤ ^ n = ⊤ ↔ ⊤ = ⊤ ∧ n ≠ 0
[PROOFSTEP]
simp only [Ne.def, hn.ne', top_pow hn]
[GOAL]
case inr.coe
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p q : ℝ≥0
n : ℕ
hn : 0 < n
x✝ : ℝ≥0
⊢ ↑x✝ ^ n = ⊤ ↔ ↑x✝ = ⊤ ∧ n ≠ 0
[PROOFSTEP]
simp only [← coe_pow, coe_ne_top, false_and]
[GOAL]
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p q : ℝ≥0
⊢ a < ⊤ → ∀ (n : ℕ), a ^ n < ⊤
[PROOFSTEP]
simpa only [lt_top_iff_ne_top] using pow_ne_top
[GOAL]
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p q : ℝ≥0
n : ℕ
⊢ ENNReal.ofReal ↑n = ↑n
[PROOFSTEP]
simp [ENNReal.ofReal]
[GOAL]
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p q : ℝ≥0
n : ℕ
⊢ ENNReal.toNNReal ↑n = ↑n
[PROOFSTEP]
rw [← ENNReal.coe_nat n, ENNReal.toNNReal_coe]
[GOAL]
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p q : ℝ≥0
n : ℕ
⊢ ENNReal.toReal ↑n = ↑n
[PROOFSTEP]
rw [← ENNReal.ofReal_coe_nat n, ENNReal.toReal_ofReal (Nat.cast_nonneg _)]
[GOAL]
α : Type u_1
β : Type u_2
a✝ b✝ c d : ℝ≥0∞
r p q : ℝ≥0
a : ℝ≥0∞
b : ℝ≥0
h : a ≤ ↑b
⊢ ENNReal.toReal a ≤ ↑b
[PROOFSTEP]
lift a to ℝ≥0 using ne_top_of_le_ne_top coe_ne_top h
[GOAL]
case intro
α : Type u_1
β : Type u_2
a✝ b✝ c d : ℝ≥0∞
r p q b a : ℝ≥0
h : ↑a ≤ ↑b
⊢ ENNReal.toReal ↑a ≤ ↑b
[PROOFSTEP]
simpa using h
[GOAL]
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p q : ℝ≥0
⊢ a ≠ 0 → ∀ (n : ℕ), a ^ n ≠ 0
[PROOFSTEP]
simpa only [pos_iff_ne_zero] using ENNReal.pow_pos
[GOAL]
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p q : ℝ≥0
⊢ ¬a < 0
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p q : ℝ≥0
ha : a ≠ ⊤
hb : b ≠ 0
⊢ a < a + b
[PROOFSTEP]
rwa [← pos_iff_ne_zero, ← ENNReal.add_lt_add_iff_left ha, add_zero] at hb 
[GOAL]
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p q : ℝ≥0
h : a < b
⊢ ∃ q, 0 ≤ q ∧ a < ↑(Real.toNNReal ↑q) ∧ ↑(Real.toNNReal ↑q) < b
[PROOFSTEP]
rcases lt_iff_exists_coe.1 h with ⟨p, rfl, _⟩
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
b c d : ℝ≥0∞
r p✝ q p : ℝ≥0
right✝ h : ↑p < b
⊢ ∃ q, 0 ≤ q ∧ ↑p < ↑(Real.toNNReal ↑q) ∧ ↑(Real.toNNReal ↑q) < b
[PROOFSTEP]
rcases exists_between h with ⟨c, pc, cb⟩
[GOAL]
case intro.intro.intro.intro
α : Type u_1
β : Type u_2
b c✝ d : ℝ≥0∞
r p✝ q p : ℝ≥0
right✝ h : ↑p < b
c : ℝ≥0∞
pc : ↑p < c
cb : c < b
⊢ ∃ q, 0 ≤ q ∧ ↑p < ↑(Real.toNNReal ↑q) ∧ ↑(Real.toNNReal ↑q) < b
[PROOFSTEP]
rcases lt_iff_exists_coe.1 cb with ⟨r, rfl, _⟩
[GOAL]
case intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
b c d : ℝ≥0∞
r✝ p✝ q p : ℝ≥0
right✝¹ h : ↑p < b
r : ℝ≥0
right✝ : ↑r < b
pc : ↑p < ↑r
cb : ↑r < b
⊢ ∃ q, 0 ≤ q ∧ ↑p < ↑(Real.toNNReal ↑q) ∧ ↑(Real.toNNReal ↑q) < b
[PROOFSTEP]
rcases(NNReal.lt_iff_exists_rat_btwn _ _).1 (coe_lt_coe.1 pc) with ⟨q, hq0, pq, qr⟩
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
b c d : ℝ≥0∞
r✝ p✝ q✝ p : ℝ≥0
right✝¹ h : ↑p < b
r : ℝ≥0
right✝ : ↑r < b
pc : ↑p < ↑r
cb : ↑r < b
q : ℚ
hq0 : 0 ≤ q
pq : p < Real.toNNReal ↑q
qr : Real.toNNReal ↑q < r
⊢ ∃ q, 0 ≤ q ∧ ↑p < ↑(Real.toNNReal ↑q) ∧ ↑(Real.toNNReal ↑q) < b
[PROOFSTEP]
exact ⟨q, hq0, coe_lt_coe.2 pq, lt_trans (coe_lt_coe.2 qr) cb⟩
[GOAL]
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p q : ℝ≥0
⊢ a < b ↔ ∃ r, 0 < r ∧ a + ↑r < b
[PROOFSTEP]
refine' ⟨fun hab => _, fun ⟨r, _, hr⟩ => lt_of_le_of_lt le_self_add hr⟩
[GOAL]
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p q : ℝ≥0
hab : a < b
⊢ ∃ r, 0 < r ∧ a + ↑r < b
[PROOFSTEP]
rcases lt_iff_exists_nnreal_btwn.1 hab with ⟨c, ac, cb⟩
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
a b c✝ d : ℝ≥0∞
r p q : ℝ≥0
hab : a < b
c : ℝ≥0
ac : a < ↑c
cb : ↑c < b
⊢ ∃ r, 0 < r ∧ a + ↑r < b
[PROOFSTEP]
lift a to ℝ≥0 using ac.ne_top
[GOAL]
case intro.intro.intro
α : Type u_1
β : Type u_2
b c✝ d : ℝ≥0∞
r p q c : ℝ≥0
cb : ↑c < b
a : ℝ≥0
hab : ↑a < b
ac : ↑a < ↑c
⊢ ∃ r, 0 < r ∧ ↑a + ↑r < b
[PROOFSTEP]
rw [coe_lt_coe] at ac 
[GOAL]
case intro.intro.intro
α : Type u_1
β : Type u_2
b c✝ d : ℝ≥0∞
r p q c : ℝ≥0
cb : ↑c < b
a : ℝ≥0
hab : ↑a < b
ac : a < c
⊢ ∃ r, 0 < r ∧ ↑a + ↑r < b
[PROOFSTEP]
refine ⟨c - a, tsub_pos_iff_lt.2 ac, ?_⟩
[GOAL]
case intro.intro.intro
α : Type u_1
β : Type u_2
b c✝ d : ℝ≥0∞
r p q c : ℝ≥0
cb : ↑c < b
a : ℝ≥0
hab : ↑a < b
ac : a < c
⊢ ↑a + ↑(c - a) < b
[PROOFSTEP]
rwa [← coe_add, add_tsub_cancel_of_le ac.le]
[GOAL]
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p q : ℝ≥0
h : ∀ (ε : ℝ≥0), 0 < ε → b < ⊤ → a ≤ b + ↑ε
⊢ a ≤ b
[PROOFSTEP]
contrapose! h
[GOAL]
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p q : ℝ≥0
h : b < a
⊢ ∃ ε, 0 < ε ∧ b < ⊤ ∧ b + ↑ε < a
[PROOFSTEP]
rcases lt_iff_exists_add_pos_lt.1 h with ⟨r, hr0, hr⟩
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r✝ p q : ℝ≥0
h : b < a
r : ℝ≥0
hr0 : 0 < r
hr : b + ↑r < a
⊢ ∃ ε, 0 < ε ∧ b < ⊤ ∧ b + ↑ε < a
[PROOFSTEP]
exact ⟨r, hr0, h.trans_le le_top, hr⟩
[GOAL]
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r✝ p q : ℝ≥0
r : ℝ≥0∞
h : r ≠ ⊤
⊢ ∃ n, r < ↑n
[PROOFSTEP]
lift r to ℝ≥0 using h
[GOAL]
case intro
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r✝ p q r : ℝ≥0
⊢ ∃ n, ↑r < ↑n
[PROOFSTEP]
rcases exists_nat_gt r with ⟨n, hn⟩
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r✝ p q r : ℝ≥0
n : ℕ
hn : r < ↑n
⊢ ∃ n, ↑r < ↑n
[PROOFSTEP]
exact ⟨n, coe_lt_coe_nat.2 hn⟩
[GOAL]
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p q : ℝ≥0
⊢ ⋃ (n : ℕ), Iio ↑n = {⊤}ᶜ
[PROOFSTEP]
ext x
[GOAL]
case h
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p q : ℝ≥0
x : ℝ≥0∞
⊢ x ∈ ⋃ (n : ℕ), Iio ↑n ↔ x ∈ {⊤}ᶜ
[PROOFSTEP]
rw [mem_iUnion]
[GOAL]
case h
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p q : ℝ≥0
x : ℝ≥0∞
⊢ (∃ i, x ∈ Iio ↑i) ↔ x ∈ {⊤}ᶜ
[PROOFSTEP]
exact ⟨fun ⟨n, hn⟩ => ne_top_of_lt hn, ENNReal.exists_nat_gt⟩
[GOAL]
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p q : ℝ≥0
⊢ ⋃ (n : ℕ), Ioc a ↑n = Ioi a \ {⊤}
[PROOFSTEP]
simp only [← Ioi_inter_Iic, ← inter_iUnion, iUnion_Iic_coe_nat, diff_eq]
[GOAL]
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p q : ℝ≥0
⊢ ⋃ (n : ℕ), Ioo a ↑n = Ioi a \ {⊤}
[PROOFSTEP]
simp only [← Ioi_inter_Iio, ← inter_iUnion, iUnion_Iio_coe_nat, diff_eq]
[GOAL]
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p q : ℝ≥0
⊢ ⋃ (n : ℕ), Icc a ↑n = Ici a \ {⊤}
[PROOFSTEP]
simp only [← Ici_inter_Iic, ← inter_iUnion, iUnion_Iic_coe_nat, diff_eq]
[GOAL]
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p q : ℝ≥0
⊢ ⋃ (n : ℕ), Ico a ↑n = Ici a \ {⊤}
[PROOFSTEP]
simp only [← Ici_inter_Iio, ← inter_iUnion, iUnion_Iio_coe_nat, diff_eq]
[GOAL]
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p q : ℝ≥0
⊢ ⋂ (n : ℕ), Ici ↑n = {⊤}
[PROOFSTEP]
simp only [← compl_Iio, ← compl_iUnion, iUnion_Iio_coe_nat, compl_compl]
[GOAL]
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p q : ℝ≥0
⊢ ⋂ (n : ℕ), Ioi ↑n = {⊤}
[PROOFSTEP]
simp only [← compl_Iic, ← compl_iUnion, iUnion_Iic_coe_nat, compl_compl]
[GOAL]
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p q : ℝ≥0
ac : a < c
bd : b < d
⊢ a + b < c + d
[PROOFSTEP]
lift a to ℝ≥0 using ac.ne_top
[GOAL]
case intro
α : Type u_1
β : Type u_2
b c d : ℝ≥0∞
r p q : ℝ≥0
bd : b < d
a : ℝ≥0
ac : ↑a < c
⊢ ↑a + b < c + d
[PROOFSTEP]
lift b to ℝ≥0 using bd.ne_top
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
c d : ℝ≥0∞
r p q a : ℝ≥0
ac : ↑a < c
b : ℝ≥0
bd : ↑b < d
⊢ ↑a + ↑b < c + d
[PROOFSTEP]
cases c
[GOAL]
case intro.intro.none
α : Type u_1
β : Type u_2
d : ℝ≥0∞
r p q a b : ℝ≥0
bd : ↑b < d
ac : ↑a < none
⊢ ↑a + ↑b < none + d
[PROOFSTEP]
simp
[GOAL]
case intro.intro.some
α : Type u_1
β : Type u_2
d : ℝ≥0∞
r p q a b : ℝ≥0
bd : ↑b < d
val✝ : ℝ≥0
ac : ↑a < Option.some val✝
⊢ ↑a + ↑b < Option.some val✝ + d
[PROOFSTEP]
cases d
[GOAL]
case intro.intro.some.none
α : Type u_1
β : Type u_2
r p q a b val✝ : ℝ≥0
ac : ↑a < Option.some val✝
bd : ↑b < none
⊢ ↑a + ↑b < Option.some val✝ + none
[PROOFSTEP]
simp
[GOAL]
case intro.intro.some.some
α : Type u_1
β : Type u_2
r p q a b val✝¹ : ℝ≥0
ac : ↑a < Option.some val✝¹
val✝ : ℝ≥0
bd : ↑b < Option.some val✝
⊢ ↑a + ↑b < Option.some val✝¹ + Option.some val✝
[PROOFSTEP]
simp only [← coe_add, some_eq_coe, coe_lt_coe] at *
[GOAL]
case intro.intro.some.some
α : Type u_1
β : Type u_2
r p q a b val✝¹ val✝ : ℝ≥0
ac : a < val✝¹
bd : b < val✝
⊢ a + b < val✝¹ + val✝
[PROOFSTEP]
exact add_lt_add ac bd
[GOAL]
α : Type u_1
β : Type u_2
a✝ b✝ c d : ℝ≥0∞
r p q : ℝ≥0
a b : ℝ≥0∞
h : a = ⊤ → b = ⊤
h_nnreal : a ≠ ⊤ → b ≠ ⊤ → ENNReal.toNNReal a ≤ ENNReal.toNNReal b
⊢ a ≤ b
[PROOFSTEP]
by_contra' hlt
[GOAL]
α : Type u_1
β : Type u_2
a✝ b✝ c d : ℝ≥0∞
r p q : ℝ≥0
a b : ℝ≥0∞
h : a = ⊤ → b = ⊤
h_nnreal : a ≠ ⊤ → b ≠ ⊤ → ENNReal.toNNReal a ≤ ENNReal.toNNReal b
hlt : b < a
⊢ False
[PROOFSTEP]
lift b to ℝ≥0 using hlt.ne_top
[GOAL]
case intro
α : Type u_1
β : Type u_2
a✝ b✝ c d : ℝ≥0∞
r p q : ℝ≥0
a : ℝ≥0∞
b : ℝ≥0
h : a = ⊤ → ↑b = ⊤
h_nnreal : a ≠ ⊤ → ↑b ≠ ⊤ → ENNReal.toNNReal a ≤ ENNReal.toNNReal ↑b
hlt : ↑b < a
⊢ False
[PROOFSTEP]
lift a to ℝ≥0 using mt h coe_ne_top
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
a✝ b✝ c d : ℝ≥0∞
r p q b a : ℝ≥0
h : ↑a = ⊤ → ↑b = ⊤
h_nnreal : ↑a ≠ ⊤ → ↑b ≠ ⊤ → ENNReal.toNNReal ↑a ≤ ENNReal.toNNReal ↑b
hlt : ↑b < ↑a
⊢ False
[PROOFSTEP]
refine hlt.not_le ?_
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
a✝ b✝ c d : ℝ≥0∞
r p q b a : ℝ≥0
h : ↑a = ⊤ → ↑b = ⊤
h_nnreal : ↑a ≠ ⊤ → ↑b ≠ ⊤ → ENNReal.toNNReal ↑a ≤ ENNReal.toNNReal ↑b
hlt : ↑b < ↑a
⊢ ↑a ≤ ↑b
[PROOFSTEP]
simpa using h_nnreal
[GOAL]
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p q : ℝ≥0
x : ℝ≥0∞
⊢ |ENNReal.toReal x| = ENNReal.toReal x
[PROOFSTEP]
cases x
[GOAL]
case none
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p q : ℝ≥0
⊢ |ENNReal.toReal none| = ENNReal.toReal none
[PROOFSTEP]
simp
[GOAL]
case some
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p q val✝ : ℝ≥0
⊢ |ENNReal.toReal (Option.some val✝)| = ENNReal.toReal (Option.some val✝)
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p q : ℝ≥0
s : Set ℝ≥0
⊢ ↑r ∈ upperBounds (some '' s) ↔ r ∈ upperBounds s
[PROOFSTEP]
simp (config := { contextual := true }) [upperBounds, ball_image_iff, -mem_image, *]
[GOAL]
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p q : ℝ≥0
ac : a < c
bd : b < d
⊢ a * b < c * d
[PROOFSTEP]
rcases lt_iff_exists_nnreal_btwn.1 ac with ⟨a', aa', a'c⟩
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p q : ℝ≥0
ac : a < c
bd : b < d
a' : ℝ≥0
aa' : a < ↑a'
a'c : ↑a' < c
⊢ a * b < c * d
[PROOFSTEP]
lift a to ℝ≥0 using ne_top_of_lt aa'
[GOAL]
case intro.intro.intro
α : Type u_1
β : Type u_2
b c d : ℝ≥0∞
r p q : ℝ≥0
bd : b < d
a' : ℝ≥0
a'c : ↑a' < c
a : ℝ≥0
ac : ↑a < c
aa' : ↑a < ↑a'
⊢ ↑a * b < c * d
[PROOFSTEP]
rcases lt_iff_exists_nnreal_btwn.1 bd with ⟨b', bb', b'd⟩
[GOAL]
case intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
b c d : ℝ≥0∞
r p q : ℝ≥0
bd : b < d
a' : ℝ≥0
a'c : ↑a' < c
a : ℝ≥0
ac : ↑a < c
aa' : ↑a < ↑a'
b' : ℝ≥0
bb' : b < ↑b'
b'd : ↑b' < d
⊢ ↑a * b < c * d
[PROOFSTEP]
lift b to ℝ≥0 using ne_top_of_lt bb'
[GOAL]
case intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
c d : ℝ≥0∞
r p q a' : ℝ≥0
a'c : ↑a' < c
a : ℝ≥0
ac : ↑a < c
aa' : ↑a < ↑a'
b' : ℝ≥0
b'd : ↑b' < d
b : ℝ≥0
bd : ↑b < d
bb' : ↑b < ↑b'
⊢ ↑a * ↑b < c * d
[PROOFSTEP]
norm_cast at *
[GOAL]
case intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
c d : ℝ≥0∞
r p q a' : ℝ≥0
a'c : ↑a' < c
a : ℝ≥0
ac : ↑a < c
b' : ℝ≥0
b'd : ↑b' < d
b : ℝ≥0
bd : ↑b < d
aa' : a < a'
bb' : b < b'
⊢ ↑(a * b) < c * d
[PROOFSTEP]
calc
  ↑(a * b) < ↑(a' * b') := coe_lt_coe.2 (mul_lt_mul₀ aa' bb')
  _ = ↑a' * ↑b' := coe_mul
  _ ≤ c * d := mul_le_mul' a'c.le b'd.le
[GOAL]
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p q : ℝ≥0
x✝ : 1 ≠ 0
⊢ StrictMono fun x => x ^ 1
[PROOFSTEP]
simpa only [pow_one] using strictMono_id
[GOAL]
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p q : ℝ≥0
h0 : a ≠ 0
hinf : a ≠ ⊤
⊢ StrictMono fun x => a * x
[PROOFSTEP]
lift a to ℝ≥0 using hinf
[GOAL]
case intro
α : Type u_1
β : Type u_2
b c d : ℝ≥0∞
r p q a : ℝ≥0
h0 : ↑a ≠ 0
⊢ StrictMono fun x => ↑a * x
[PROOFSTEP]
rw [coe_ne_zero] at h0 
[GOAL]
case intro
α : Type u_1
β : Type u_2
b c d : ℝ≥0∞
r p q a : ℝ≥0
h0 : a ≠ 0
⊢ StrictMono fun x => ↑a * x
[PROOFSTEP]
intro x y h
[GOAL]
case intro
α : Type u_1
β : Type u_2
b c d : ℝ≥0∞
r p q a : ℝ≥0
h0 : a ≠ 0
x y : ℝ≥0∞
h : x < y
⊢ (fun x => ↑a * x) x < (fun x => ↑a * x) y
[PROOFSTEP]
contrapose! h
[GOAL]
case intro
α : Type u_1
β : Type u_2
b c d : ℝ≥0∞
r p q a : ℝ≥0
h0 : a ≠ 0
x y : ℝ≥0∞
h : ↑a * y ≤ ↑a * x
⊢ y ≤ x
[PROOFSTEP]
simpa only [← mul_assoc, ← coe_mul, inv_mul_cancel h0, coe_one, one_mul] using mul_le_mul_left' h (↑a⁻¹)
[GOAL]
α : Type u_1
β : Type u_2
a✝ b c d : ℝ≥0∞
r p q : ℝ≥0
a : ℝ≥0∞
⊢ AddLECancellable a ↔ a ≠ ⊤
[PROOFSTEP]
constructor
[GOAL]
case mp
α : Type u_1
β : Type u_2
a✝ b c d : ℝ≥0∞
r p q : ℝ≥0
a : ℝ≥0∞
⊢ AddLECancellable a → a ≠ ⊤
[PROOFSTEP]
rintro h rfl
[GOAL]
case mp
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p q : ℝ≥0
h : AddLECancellable ⊤
⊢ False
[PROOFSTEP]
refine' zero_lt_one.not_le (h _)
[GOAL]
case mp
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p q : ℝ≥0
h : AddLECancellable ⊤
⊢ ⊤ + 1 ≤ ⊤ + 0
[PROOFSTEP]
simp
[GOAL]
case mpr
α : Type u_1
β : Type u_2
a✝ b c d : ℝ≥0∞
r p q : ℝ≥0
a : ℝ≥0∞
⊢ a ≠ ⊤ → AddLECancellable a
[PROOFSTEP]
rintro h b c hbc
[GOAL]
case mpr
α : Type u_1
β : Type u_2
a✝ b✝ c✝ d : ℝ≥0∞
r p q : ℝ≥0
a : ℝ≥0∞
h : a ≠ ⊤
b c : ℝ≥0∞
hbc : a + b ≤ a + c
⊢ b ≤ c
[PROOFSTEP]
apply ENNReal.le_of_add_le_add_left h hbc
[GOAL]
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p q : ℝ≥0
m n : ℕ
⊢ ↑(m - n) = ↑m - ↑n
[PROOFSTEP]
rw [← coe_nat, Nat.cast_tsub, coe_sub, coe_nat, coe_nat]
[GOAL]
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p q : ℝ≥0
h : a ≠ ⊤ ∨ b ≠ ⊤
⊢ a - b < c → a < b + c
[PROOFSTEP]
obtain rfl | hb := eq_or_ne b ∞
[GOAL]
case inl
α : Type u_1
β : Type u_2
a c d : ℝ≥0∞
r p q : ℝ≥0
h : a ≠ ⊤ ∨ ⊤ ≠ ⊤
⊢ a - ⊤ < c → a < ⊤ + c
[PROOFSTEP]
rw [top_add, lt_top_iff_ne_top]
[GOAL]
case inl
α : Type u_1
β : Type u_2
a c d : ℝ≥0∞
r p q : ℝ≥0
h : a ≠ ⊤ ∨ ⊤ ≠ ⊤
⊢ a - ⊤ < c → a ≠ ⊤
[PROOFSTEP]
exact fun _ => h.resolve_right (Classical.not_not.2 rfl)
[GOAL]
case inr
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p q : ℝ≥0
h : a ≠ ⊤ ∨ b ≠ ⊤
hb : b ≠ ⊤
⊢ a - b < c → a < b + c
[PROOFSTEP]
exact (cancel_of_ne hb).lt_add_of_tsub_lt_left
[GOAL]
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p q : ℝ≥0
h : 0 < b → b < a → c ≠ ⊤
⊢ (a - b) * c = a * c - b * c
[PROOFSTEP]
cases' le_or_lt a b with hab hab
[GOAL]
case inl
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p q : ℝ≥0
h : 0 < b → b < a → c ≠ ⊤
hab : a ≤ b
⊢ (a - b) * c = a * c - b * c
[PROOFSTEP]
simp [hab, mul_right_mono hab]
[GOAL]
case inr
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p q : ℝ≥0
h : 0 < b → b < a → c ≠ ⊤
hab : b < a
⊢ (a - b) * c = a * c - b * c
[PROOFSTEP]
rcases eq_or_lt_of_le (zero_le b) with (rfl | hb)
[GOAL]
case inr.inl
α : Type u_1
β : Type u_2
a c d : ℝ≥0∞
r p q : ℝ≥0
h : 0 < 0 → 0 < a → c ≠ ⊤
hab : 0 < a
⊢ (a - 0) * c = a * c - 0 * c
[PROOFSTEP]
simp
[GOAL]
case inr.inr
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p q : ℝ≥0
h : 0 < b → b < a → c ≠ ⊤
hab : b < a
hb : 0 < b
⊢ (a - b) * c = a * c - b * c
[PROOFSTEP]
exact (cancel_of_ne <| mul_ne_top hab.ne_top (h hb hab)).tsub_mul
[GOAL]
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p q : ℝ≥0
h : 0 < c → c < b → a ≠ ⊤
⊢ a * (b - c) = a * b - a * c
[PROOFSTEP]
simp only [mul_comm a]
[GOAL]
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p q : ℝ≥0
h : 0 < c → c < b → a ≠ ⊤
⊢ (b - c) * a = b * a - c * a
[PROOFSTEP]
exact sub_mul h
[GOAL]
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p q : ℝ≥0
s : Finset α
f : α → ℝ≥0∞
hf : ∀ (a : α), a ∈ s → f a ≠ ⊤
⊢ ENNReal.toNNReal (∑ a in s, f a) = ∑ a in s, ENNReal.toNNReal (f a)
[PROOFSTEP]
rw [← coe_eq_coe, coe_toNNReal, coe_finset_sum, sum_congr rfl]
[GOAL]
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p q : ℝ≥0
s : Finset α
f : α → ℝ≥0∞
hf : ∀ (a : α), a ∈ s → f a ≠ ⊤
⊢ ∀ (x : α), x ∈ s → f x = ↑(ENNReal.toNNReal (f x))
[PROOFSTEP]
intro x hx
[GOAL]
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p q : ℝ≥0
s : Finset α
f : α → ℝ≥0∞
hf : ∀ (a : α), a ∈ s → f a ≠ ⊤
x : α
hx : x ∈ s
⊢ f x = ↑(ENNReal.toNNReal (f x))
[PROOFSTEP]
exact (coe_toNNReal (hf x hx)).symm
[GOAL]
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p q : ℝ≥0
s : Finset α
f : α → ℝ≥0∞
hf : ∀ (a : α), a ∈ s → f a ≠ ⊤
⊢ ∑ a in s, f a ≠ ⊤
[PROOFSTEP]
exact (sum_lt_top hf).ne
[GOAL]
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p q : ℝ≥0
s : Finset α
f : α → ℝ≥0∞
hf : ∀ (a : α), a ∈ s → f a ≠ ⊤
⊢ ENNReal.toReal (∑ a in s, f a) = ∑ a in s, ENNReal.toReal (f a)
[PROOFSTEP]
rw [ENNReal.toReal, toNNReal_sum hf, NNReal.coe_sum]
[GOAL]
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p q : ℝ≥0
s : Finset α
f : α → ℝ≥0∞
hf : ∀ (a : α), a ∈ s → f a ≠ ⊤
⊢ ∑ a in s, ↑(ENNReal.toNNReal (f a)) = ∑ a in s, ENNReal.toReal (f a)
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p q : ℝ≥0
s : Finset α
f : α → ℝ
hf : ∀ (i : α), i ∈ s → 0 ≤ f i
⊢ ENNReal.ofReal (∑ i in s, f i) = ∑ i in s, ENNReal.ofReal (f i)
[PROOFSTEP]
simp_rw [ENNReal.ofReal, ← coe_finset_sum, coe_eq_coe]
[GOAL]
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p q : ℝ≥0
s : Finset α
f : α → ℝ
hf : ∀ (i : α), i ∈ s → 0 ≤ f i
⊢ Real.toNNReal (∑ i in s, f i) = ∑ a in s, Real.toNNReal (f a)
[PROOFSTEP]
exact Real.toNNReal_sum_of_nonneg hf
[GOAL]
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p q : ℝ≥0
s : Finset α
hs : Finset.Nonempty s
f g : α → ℝ≥0∞
Hlt : ∀ (i : α), i ∈ s → f i < g i
⊢ ∑ i in s, f i < ∑ i in s, g i
[PROOFSTEP]
induction' hs using Finset.Nonempty.cons_induction with a a s as _ IH
[GOAL]
case h₀
α : Type u_1
β : Type u_2
a✝ b c d : ℝ≥0∞
r p q : ℝ≥0
s : Finset α
f g : α → ℝ≥0∞
Hlt✝ : ∀ (i : α), i ∈ s → f i < g i
a : α
Hlt : ∀ (i : α), i ∈ {a} → f i < g i
⊢ ∑ i in {a}, f i < ∑ i in {a}, g i
[PROOFSTEP]
simp [Hlt _ (Finset.mem_singleton_self _)]
[GOAL]
case h₁
α : Type u_1
β : Type u_2
a✝ b c d : ℝ≥0∞
r p q : ℝ≥0
s✝ : Finset α
f g : α → ℝ≥0∞
Hlt✝ : ∀ (i : α), i ∈ s✝ → f i < g i
a : α
s : Finset α
as : ¬a ∈ s
hs✝ : Finset.Nonempty s
IH : (∀ (i : α), i ∈ s → f i < g i) → ∑ i in s, f i < ∑ i in s, g i
Hlt : ∀ (i : α), i ∈ cons a s as → f i < g i
⊢ ∑ i in cons a s as, f i < ∑ i in cons a s as, g i
[PROOFSTEP]
simp only [as, Finset.sum_cons, not_false_iff]
[GOAL]
case h₁
α : Type u_1
β : Type u_2
a✝ b c d : ℝ≥0∞
r p q : ℝ≥0
s✝ : Finset α
f g : α → ℝ≥0∞
Hlt✝ : ∀ (i : α), i ∈ s✝ → f i < g i
a : α
s : Finset α
as : ¬a ∈ s
hs✝ : Finset.Nonempty s
IH : (∀ (i : α), i ∈ s → f i < g i) → ∑ i in s, f i < ∑ i in s, g i
Hlt : ∀ (i : α), i ∈ cons a s as → f i < g i
⊢ f a + ∑ i in s, f i < g a + ∑ i in s, g i
[PROOFSTEP]
exact ENNReal.add_lt_add (Hlt _ (Finset.mem_cons_self _ _)) (IH fun i hi => Hlt _ (Finset.mem_cons.2 <| Or.inr hi))
[GOAL]
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p q : ℝ≥0
s : Finset α
hs : Finset.Nonempty s
f g : α → ℝ≥0∞
Hle : ∑ i in s, f i ≤ ∑ i in s, g i
⊢ ∃ i, i ∈ s ∧ f i ≤ g i
[PROOFSTEP]
contrapose! Hle
[GOAL]
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p q : ℝ≥0
s : Finset α
hs : Finset.Nonempty s
f g : α → ℝ≥0∞
Hle : ∀ (i : α), i ∈ s → g i < f i
⊢ ∑ i in s, g i < ∑ i in s, f i
[PROOFSTEP]
apply ENNReal.sum_lt_sum_of_nonempty hs Hle
[GOAL]
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p q : ℝ≥0
⊢ a / b = b⁻¹ * a
[PROOFSTEP]
rw [div_eq_mul_inv, mul_comm]
[GOAL]
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p q : ℝ≥0
⊢ sInf {b | 1 ≤ 0 * b} = ⊤
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
a✝ b c d : ℝ≥0∞
r p q : ℝ≥0
a : ℝ≥0∞
h : 0 < a
⊢ a ∈ {b | 1 ≤ ⊤ * b}
[PROOFSTEP]
simp [*, h.ne', top_mul]
[GOAL]
α : Type u_1
β : Type u_2
a b✝ c d : ℝ≥0∞
r p q : ℝ≥0
b : ℝ≥0∞
hb : 1 ≤ ↑r * b
⊢ ∀ (p : ℝ≥0), b = ↑p → r⁻¹ ≤ p
[PROOFSTEP]
rintro b rfl
[GOAL]
α : Type u_1
β : Type u_2
a b✝ c d : ℝ≥0∞
r p q b : ℝ≥0
hb : 1 ≤ ↑r * ↑b
⊢ r⁻¹ ≤ b
[PROOFSTEP]
apply NNReal.inv_le_of_le_mul
[GOAL]
case h
α : Type u_1
β : Type u_2
a b✝ c d : ℝ≥0∞
r p q b : ℝ≥0
hb : 1 ≤ ↑r * ↑b
⊢ 1 ≤ r * b
[PROOFSTEP]
rwa [← coe_mul, ← coe_one, coe_le_coe] at hb 
[GOAL]
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p q : ℝ≥0
hr : r ≠ 0
⊢ 1 ≤ ↑r * ↑r⁻¹
[PROOFSTEP]
rw [← coe_mul, mul_inv_cancel hr, coe_one]
[GOAL]
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p q : ℝ≥0
⊢ ↑2⁻¹ = 2⁻¹
[PROOFSTEP]
rw [coe_inv _root_.two_ne_zero, coe_two]
[GOAL]
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p q : ℝ≥0
hr : r ≠ 0
⊢ ↑(p / r) = ↑p / ↑r
[PROOFSTEP]
rw [div_eq_mul_inv, div_eq_mul_inv, coe_mul, coe_inv hr]
[GOAL]
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p q : ℝ≥0
h : a ≠ 0
⊢ a / 0 = ⊤
[PROOFSTEP]
simp [div_eq_mul_inv, h]
[GOAL]
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p q : ℝ≥0
src✝ : DivInvMonoid ℝ≥0∞ := inferInstanceAs (DivInvMonoid ℝ≥0∞)
⊢ 1⁻¹ = 1
[PROOFSTEP]
simpa only [coe_inv one_ne_zero, coe_one] using coe_eq_coe.2 inv_one
[GOAL]
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p q : ℝ≥0
x✝ : ℝ≥0∞
⊢ (x✝ ^ 0)⁻¹ = x✝⁻¹ ^ 0
[PROOFSTEP]
simp only [pow_zero, inv_one]
[GOAL]
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p q : ℝ≥0
n : ℕ
⊢ (⊤ ^ (n + 1))⁻¹ = ⊤⁻¹ ^ (n + 1)
[PROOFSTEP]
simp [top_pow]
[GOAL]
α : Type u_1
β : Type u_2
a✝ b c d : ℝ≥0∞
r p q a : ℝ≥0
n : ℕ
⊢ (↑a ^ (n + 1))⁻¹ = (↑a)⁻¹ ^ (n + 1)
[PROOFSTEP]
rcases eq_or_ne a 0 with (rfl | ha)
[GOAL]
case inl
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p q : ℝ≥0
n : ℕ
⊢ (↑0 ^ (n + 1))⁻¹ = (↑0)⁻¹ ^ (n + 1)
[PROOFSTEP]
simp [top_pow]
[GOAL]
case inr
α : Type u_1
β : Type u_2
a✝ b c d : ℝ≥0∞
r p q a : ℝ≥0
n : ℕ
ha : a ≠ 0
⊢ (↑a ^ (n + 1))⁻¹ = (↑a)⁻¹ ^ (n + 1)
[PROOFSTEP]
have := pow_ne_zero (n + 1) ha
[GOAL]
case inr
α : Type u_1
β : Type u_2
a✝ b c d : ℝ≥0∞
r p q a : ℝ≥0
n : ℕ
ha : a ≠ 0
this : a ^ (n + 1) ≠ 0
⊢ (↑a ^ (n + 1))⁻¹ = (↑a)⁻¹ ^ (n + 1)
[PROOFSTEP]
norm_cast
[GOAL]
case inr
α : Type u_1
β : Type u_2
a✝ b c d : ℝ≥0∞
r p q a : ℝ≥0
n : ℕ
ha : a ≠ 0
this : a ^ (n + 1) ≠ 0
⊢ (a ^ (n + 1))⁻¹ = a⁻¹ ^ (n + 1)
[PROOFSTEP]
rw [inv_pow]
[GOAL]
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p q : ℝ≥0
h0 : a ≠ 0
ht : a ≠ ⊤
⊢ a * a⁻¹ = 1
[PROOFSTEP]
lift a to ℝ≥0 using ht
[GOAL]
case intro
α : Type u_1
β : Type u_2
b c d : ℝ≥0∞
r p q a : ℝ≥0
h0 : ↑a ≠ 0
⊢ ↑a * (↑a)⁻¹ = 1
[PROOFSTEP]
norm_cast at h0 
[GOAL]
case intro
α : Type u_1
β : Type u_2
b c d : ℝ≥0∞
r p q a : ℝ≥0
h0 : ¬a = 0
⊢ ↑a * (↑a)⁻¹ = 1
[PROOFSTEP]
norm_cast
[GOAL]
case intro
α : Type u_1
β : Type u_2
b c d : ℝ≥0∞
r p q a : ℝ≥0
h0 : ¬a = 0
⊢ a * a⁻¹ = 1
[PROOFSTEP]
exact mul_inv_cancel h0
[GOAL]
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p q : ℝ≥0
h0 : a ≠ 0
hI : a ≠ ⊤
⊢ b / a * a = b
[PROOFSTEP]
rw [div_eq_mul_inv, mul_assoc, ENNReal.inv_mul_cancel h0 hI, mul_one]
[GOAL]
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p q : ℝ≥0
h0 : a ≠ 0
hI : a ≠ ⊤
⊢ a * (b / a) = b
[PROOFSTEP]
rw [mul_comm, ENNReal.div_mul_cancel h0 hI]
[GOAL]
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p q : ℝ≥0
⊢ a / b * c = a * (c / b)
[PROOFSTEP]
simp only [div_eq_mul_inv, mul_right_comm, ← mul_assoc]
[GOAL]
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p q : ℝ≥0
⊢ a * b / c = a / c * b
[PROOFSTEP]
simp only [div_eq_mul_inv, mul_right_comm]
[GOAL]
α : Type u_1
β : Type u_2
a✝ b c d : ℝ≥0∞
r p q : ℝ≥0
a : ℝ≥0∞
⊢ a⁻¹⁻¹ = a
[PROOFSTEP]
by_cases a = 0
[GOAL]
α : Type u_1
β : Type u_2
a✝ b c d : ℝ≥0∞
r p q : ℝ≥0
a : ℝ≥0∞
⊢ a⁻¹⁻¹ = a
[PROOFSTEP]
by_cases a = 0
[GOAL]
case pos
α : Type u_1
β : Type u_2
a✝ b c d : ℝ≥0∞
r p q : ℝ≥0
a : ℝ≥0∞
h : a = 0
⊢ a⁻¹⁻¹ = a
[PROOFSTEP]
cases a
[GOAL]
case neg
α : Type u_1
β : Type u_2
a✝ b c d : ℝ≥0∞
r p q : ℝ≥0
a : ℝ≥0∞
h : ¬a = 0
⊢ a⁻¹⁻¹ = a
[PROOFSTEP]
cases a
[GOAL]
case pos.none
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p q : ℝ≥0
h : none = 0
⊢ none⁻¹⁻¹ = none
[PROOFSTEP]
simp_all [none_eq_top, some_eq_coe, -coe_inv, (coe_inv _).symm]
[GOAL]
case pos.some
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p q val✝ : ℝ≥0
h : Option.some val✝ = 0
⊢ (Option.some val✝)⁻¹⁻¹ = Option.some val✝
[PROOFSTEP]
simp_all [none_eq_top, some_eq_coe, -coe_inv, (coe_inv _).symm]
[GOAL]
case neg.none
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p q : ℝ≥0
h : ¬none = 0
⊢ none⁻¹⁻¹ = none
[PROOFSTEP]
simp_all [none_eq_top, some_eq_coe, -coe_inv, (coe_inv _).symm]
[GOAL]
case neg.some
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p q val✝ : ℝ≥0
h : ¬Option.some val✝ = 0
⊢ (Option.some val✝)⁻¹⁻¹ = Option.some val✝
[PROOFSTEP]
simp_all [none_eq_top, some_eq_coe, -coe_inv, (coe_inv _).symm]
[GOAL]
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p q : ℝ≥0
⊢ a⁻¹ ≠ ⊤ ↔ a ≠ 0
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p q : ℝ≥0
x : ℝ≥0∞
⊢ x⁻¹ < ⊤ ↔ 0 < x
[PROOFSTEP]
simp only [lt_top_iff_ne_top, inv_ne_top, pos_iff_ne_zero]
[GOAL]
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p q : ℝ≥0
⊢ a⁻¹ ≠ 0 ↔ a ≠ ⊤
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
a✝ b✝ c d : ℝ≥0∞
r p q : ℝ≥0
a b : ℝ≥0∞
ha : a ≠ 0 ∨ b ≠ ⊤
hb : a ≠ ⊤ ∨ b ≠ 0
⊢ (a * b)⁻¹ = a⁻¹ * b⁻¹
[PROOFSTEP]
induction' b using recTopCoe with b
[GOAL]
case top
α : Type u_1
β : Type u_2
a✝ b✝ c d : ℝ≥0∞
r p q : ℝ≥0
a b : ℝ≥0∞
ha✝ : a ≠ 0 ∨ b ≠ ⊤
hb✝ : a ≠ ⊤ ∨ b ≠ 0
ha : a ≠ 0 ∨ ⊤ ≠ ⊤
hb : a ≠ ⊤ ∨ ⊤ ≠ 0
⊢ (a * ⊤)⁻¹ = a⁻¹ * ⊤⁻¹
[PROOFSTEP]
replace ha : a ≠ 0 := ha.neg_resolve_right rfl
[GOAL]
case top
α : Type u_1
β : Type u_2
a✝ b✝ c d : ℝ≥0∞
r p q : ℝ≥0
a b : ℝ≥0∞
ha✝ : a ≠ 0 ∨ b ≠ ⊤
hb✝ : a ≠ ⊤ ∨ b ≠ 0
hb : a ≠ ⊤ ∨ ⊤ ≠ 0
ha : a ≠ 0
⊢ (a * ⊤)⁻¹ = a⁻¹ * ⊤⁻¹
[PROOFSTEP]
simp [ha]
[GOAL]
case coe
α : Type u_1
β : Type u_2
a✝ b✝¹ c d : ℝ≥0∞
r p q : ℝ≥0
a b✝ : ℝ≥0∞
ha✝ : a ≠ 0 ∨ b✝ ≠ ⊤
hb✝ : a ≠ ⊤ ∨ b✝ ≠ 0
b : ℝ≥0
ha : a ≠ 0 ∨ ↑b ≠ ⊤
hb : a ≠ ⊤ ∨ ↑b ≠ 0
⊢ (a * ↑b)⁻¹ = a⁻¹ * (↑b)⁻¹
[PROOFSTEP]
induction' a using recTopCoe with a
[GOAL]
case coe.top
α : Type u_1
β : Type u_2
a✝ b✝¹ c d : ℝ≥0∞
r p q : ℝ≥0
a b✝ : ℝ≥0∞
ha✝² : a ≠ 0 ∨ b✝ ≠ ⊤
hb✝² : a ≠ ⊤ ∨ b✝ ≠ 0
b : ℝ≥0
ha✝¹ : a ≠ 0 ∨ ↑b ≠ ⊤
hb✝¹ : a ≠ ⊤ ∨ ↑b ≠ 0
ha✝ : ⊤ ≠ 0 ∨ b✝ ≠ ⊤
hb✝ : ⊤ ≠ ⊤ ∨ b✝ ≠ 0
ha : ⊤ ≠ 0 ∨ ↑b ≠ ⊤
hb : ⊤ ≠ ⊤ ∨ ↑b ≠ 0
⊢ (⊤ * ↑b)⁻¹ = ⊤⁻¹ * (↑b)⁻¹
[PROOFSTEP]
replace hb : b ≠ 0 := coe_ne_zero.1 (hb.neg_resolve_left rfl)
[GOAL]
case coe.top
α : Type u_1
β : Type u_2
a✝ b✝¹ c d : ℝ≥0∞
r p q : ℝ≥0
a b✝ : ℝ≥0∞
ha✝² : a ≠ 0 ∨ b✝ ≠ ⊤
hb✝² : a ≠ ⊤ ∨ b✝ ≠ 0
b : ℝ≥0
ha✝¹ : a ≠ 0 ∨ ↑b ≠ ⊤
hb✝¹ : a ≠ ⊤ ∨ ↑b ≠ 0
ha✝ : ⊤ ≠ 0 ∨ b✝ ≠ ⊤
hb✝ : ⊤ ≠ ⊤ ∨ b✝ ≠ 0
ha : ⊤ ≠ 0 ∨ ↑b ≠ ⊤
hb : b ≠ 0
⊢ (⊤ * ↑b)⁻¹ = ⊤⁻¹ * (↑b)⁻¹
[PROOFSTEP]
simp [hb]
[GOAL]
case coe.coe
α : Type u_1
β : Type u_2
a✝¹ b✝¹ c d : ℝ≥0∞
r p q : ℝ≥0
a✝ b✝ : ℝ≥0∞
ha✝² : a✝ ≠ 0 ∨ b✝ ≠ ⊤
hb✝² : a✝ ≠ ⊤ ∨ b✝ ≠ 0
b : ℝ≥0
ha✝¹ : a✝ ≠ 0 ∨ ↑b ≠ ⊤
hb✝¹ : a✝ ≠ ⊤ ∨ ↑b ≠ 0
a : ℝ≥0
ha✝ : ↑a ≠ 0 ∨ b✝ ≠ ⊤
hb✝ : ↑a ≠ ⊤ ∨ b✝ ≠ 0
ha : ↑a ≠ 0 ∨ ↑b ≠ ⊤
hb : ↑a ≠ ⊤ ∨ ↑b ≠ 0
⊢ (↑a * ↑b)⁻¹ = (↑a)⁻¹ * (↑b)⁻¹
[PROOFSTEP]
by_cases h'a : a = 0
[GOAL]
case pos
α : Type u_1
β : Type u_2
a✝¹ b✝¹ c d : ℝ≥0∞
r p q : ℝ≥0
a✝ b✝ : ℝ≥0∞
ha✝² : a✝ ≠ 0 ∨ b✝ ≠ ⊤
hb✝² : a✝ ≠ ⊤ ∨ b✝ ≠ 0
b : ℝ≥0
ha✝¹ : a✝ ≠ 0 ∨ ↑b ≠ ⊤
hb✝¹ : a✝ ≠ ⊤ ∨ ↑b ≠ 0
a : ℝ≥0
ha✝ : ↑a ≠ 0 ∨ b✝ ≠ ⊤
hb✝ : ↑a ≠ ⊤ ∨ b✝ ≠ 0
ha : ↑a ≠ 0 ∨ ↑b ≠ ⊤
hb : ↑a ≠ ⊤ ∨ ↑b ≠ 0
h'a : a = 0
⊢ (↑a * ↑b)⁻¹ = (↑a)⁻¹ * (↑b)⁻¹
[PROOFSTEP]
simp only [h'a, top_mul, ENNReal.inv_zero, ENNReal.coe_ne_top, zero_mul, Ne.def, not_false_iff, ENNReal.coe_zero,
  ENNReal.inv_eq_zero]
[GOAL]
case neg
α : Type u_1
β : Type u_2
a✝¹ b✝¹ c d : ℝ≥0∞
r p q : ℝ≥0
a✝ b✝ : ℝ≥0∞
ha✝² : a✝ ≠ 0 ∨ b✝ ≠ ⊤
hb✝² : a✝ ≠ ⊤ ∨ b✝ ≠ 0
b : ℝ≥0
ha✝¹ : a✝ ≠ 0 ∨ ↑b ≠ ⊤
hb✝¹ : a✝ ≠ ⊤ ∨ ↑b ≠ 0
a : ℝ≥0
ha✝ : ↑a ≠ 0 ∨ b✝ ≠ ⊤
hb✝ : ↑a ≠ ⊤ ∨ b✝ ≠ 0
ha : ↑a ≠ 0 ∨ ↑b ≠ ⊤
hb : ↑a ≠ ⊤ ∨ ↑b ≠ 0
h'a : ¬a = 0
⊢ (↑a * ↑b)⁻¹ = (↑a)⁻¹ * (↑b)⁻¹
[PROOFSTEP]
by_cases h'b : b = 0
[GOAL]
case pos
α : Type u_1
β : Type u_2
a✝¹ b✝¹ c d : ℝ≥0∞
r p q : ℝ≥0
a✝ b✝ : ℝ≥0∞
ha✝² : a✝ ≠ 0 ∨ b✝ ≠ ⊤
hb✝² : a✝ ≠ ⊤ ∨ b✝ ≠ 0
b : ℝ≥0
ha✝¹ : a✝ ≠ 0 ∨ ↑b ≠ ⊤
hb✝¹ : a✝ ≠ ⊤ ∨ ↑b ≠ 0
a : ℝ≥0
ha✝ : ↑a ≠ 0 ∨ b✝ ≠ ⊤
hb✝ : ↑a ≠ ⊤ ∨ b✝ ≠ 0
ha : ↑a ≠ 0 ∨ ↑b ≠ ⊤
hb : ↑a ≠ ⊤ ∨ ↑b ≠ 0
h'a : ¬a = 0
h'b : b = 0
⊢ (↑a * ↑b)⁻¹ = (↑a)⁻¹ * (↑b)⁻¹
[PROOFSTEP]
simp only [h'b, ENNReal.inv_zero, ENNReal.coe_ne_top, mul_top, Ne.def, not_false_iff, mul_zero, ENNReal.coe_zero,
  ENNReal.inv_eq_zero]
[GOAL]
case neg
α : Type u_1
β : Type u_2
a✝¹ b✝¹ c d : ℝ≥0∞
r p q : ℝ≥0
a✝ b✝ : ℝ≥0∞
ha✝² : a✝ ≠ 0 ∨ b✝ ≠ ⊤
hb✝² : a✝ ≠ ⊤ ∨ b✝ ≠ 0
b : ℝ≥0
ha✝¹ : a✝ ≠ 0 ∨ ↑b ≠ ⊤
hb✝¹ : a✝ ≠ ⊤ ∨ ↑b ≠ 0
a : ℝ≥0
ha✝ : ↑a ≠ 0 ∨ b✝ ≠ ⊤
hb✝ : ↑a ≠ ⊤ ∨ b✝ ≠ 0
ha : ↑a ≠ 0 ∨ ↑b ≠ ⊤
hb : ↑a ≠ ⊤ ∨ ↑b ≠ 0
h'a : ¬a = 0
h'b : ¬b = 0
⊢ (↑a * ↑b)⁻¹ = (↑a)⁻¹ * (↑b)⁻¹
[PROOFSTEP]
rw [← ENNReal.coe_mul, ← ENNReal.coe_inv, ← ENNReal.coe_inv h'a, ← ENNReal.coe_inv h'b, ← ENNReal.coe_mul, mul_inv_rev,
  mul_comm]
[GOAL]
case neg
α : Type u_1
β : Type u_2
a✝¹ b✝¹ c d : ℝ≥0∞
r p q : ℝ≥0
a✝ b✝ : ℝ≥0∞
ha✝² : a✝ ≠ 0 ∨ b✝ ≠ ⊤
hb✝² : a✝ ≠ ⊤ ∨ b✝ ≠ 0
b : ℝ≥0
ha✝¹ : a✝ ≠ 0 ∨ ↑b ≠ ⊤
hb✝¹ : a✝ ≠ ⊤ ∨ ↑b ≠ 0
a : ℝ≥0
ha✝ : ↑a ≠ 0 ∨ b✝ ≠ ⊤
hb✝ : ↑a ≠ ⊤ ∨ b✝ ≠ 0
ha : ↑a ≠ 0 ∨ ↑b ≠ ⊤
hb : ↑a ≠ ⊤ ∨ ↑b ≠ 0
h'a : ¬a = 0
h'b : ¬b = 0
⊢ a * b ≠ 0
[PROOFSTEP]
simp [h'a, h'b]
[GOAL]
α : Type u_1
β : Type u_2
a✝ b✝ c d : ℝ≥0∞
r p q : ℝ≥0
a b : ℝ≥0∞
hc : c ≠ 0
hc' : c ≠ ⊤
⊢ c * a / (c * b) = a / b
[PROOFSTEP]
rw [div_eq_mul_inv, div_eq_mul_inv, ENNReal.mul_inv (Or.inl hc) (Or.inl hc'), mul_mul_mul_comm,
  ENNReal.mul_inv_cancel hc hc', one_mul]
[GOAL]
α : Type u_1
β : Type u_2
a✝ b✝ c d : ℝ≥0∞
r p q : ℝ≥0
a b : ℝ≥0∞
hc : c ≠ 0
hc' : c ≠ ⊤
⊢ a * c / (b * c) = a / b
[PROOFSTEP]
rw [div_eq_mul_inv, div_eq_mul_inv, ENNReal.mul_inv (Or.inr hc') (Or.inr hc), mul_mul_mul_comm,
  ENNReal.mul_inv_cancel hc hc', mul_one]
[GOAL]
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p q : ℝ≥0
h : 0 < b → b < a → c ≠ 0
⊢ (a - b) / c = a / c - b / c
[PROOFSTEP]
simp_rw [div_eq_mul_inv]
[GOAL]
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p q : ℝ≥0
h : 0 < b → b < a → c ≠ 0
⊢ (a - b) * c⁻¹ = a * c⁻¹ - b * c⁻¹
[PROOFSTEP]
exact ENNReal.sub_mul (by simpa using h)
[GOAL]
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p q : ℝ≥0
h : 0 < b → b < a → c ≠ 0
⊢ 0 < b → b < a → c⁻¹ ≠ ⊤
[PROOFSTEP]
simpa using h
[GOAL]
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p q : ℝ≥0
⊢ StrictAnti Inv.inv
[PROOFSTEP]
intro a b h
[GOAL]
α : Type u_1
β : Type u_2
a✝ b✝ c d : ℝ≥0∞
r p q : ℝ≥0
a b : ℝ≥0∞
h : a < b
⊢ b⁻¹ < a⁻¹
[PROOFSTEP]
lift a to ℝ≥0 using h.ne_top
[GOAL]
case intro
α : Type u_1
β : Type u_2
a✝ b✝ c d : ℝ≥0∞
r p q : ℝ≥0
b : ℝ≥0∞
a : ℝ≥0
h : ↑a < b
⊢ b⁻¹ < (↑a)⁻¹
[PROOFSTEP]
induction b using recTopCoe
[GOAL]
case intro.top
α : Type u_1
β : Type u_2
a✝ b c d : ℝ≥0∞
r p q a : ℝ≥0
h : ↑a < ⊤
⊢ ⊤⁻¹ < (↑a)⁻¹
[PROOFSTEP]
simp
[GOAL]
case intro.coe
α : Type u_1
β : Type u_2
a✝ b c d : ℝ≥0∞
r p q a x✝ : ℝ≥0
h : ↑a < ↑x✝
⊢ (↑x✝)⁻¹ < (↑a)⁻¹
[PROOFSTEP]
rw [coe_lt_coe] at h 
[GOAL]
case intro.coe
α : Type u_1
β : Type u_2
a✝ b c d : ℝ≥0∞
r p q a x✝ : ℝ≥0
h : a < x✝
⊢ (↑x✝)⁻¹ < (↑a)⁻¹
[PROOFSTEP]
rcases eq_or_ne a 0 with (rfl | ha)
[GOAL]
case intro.coe.inl
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p q x✝ : ℝ≥0
h : 0 < x✝
⊢ (↑x✝)⁻¹ < (↑0)⁻¹
[PROOFSTEP]
simp [h]
[GOAL]
case intro.coe.inr
α : Type u_1
β : Type u_2
a✝ b c d : ℝ≥0∞
r p q a x✝ : ℝ≥0
h : a < x✝
ha : a ≠ 0
⊢ (↑x✝)⁻¹ < (↑a)⁻¹
[PROOFSTEP]
rw [← coe_inv h.ne_bot, ← coe_inv ha, coe_lt_coe]
[GOAL]
case intro.coe.inr
α : Type u_1
β : Type u_2
a✝ b c d : ℝ≥0∞
r p q a x✝ : ℝ≥0
h : a < x✝
ha : a ≠ 0
⊢ x✝⁻¹ < a⁻¹
[PROOFSTEP]
exact NNReal.inv_lt_inv ha h
[GOAL]
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p q : ℝ≥0
⊢ a⁻¹ < b ↔ b⁻¹ < a
[PROOFSTEP]
simpa only [inv_inv] using @ENNReal.inv_lt_inv a b⁻¹
[GOAL]
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p q : ℝ≥0
⊢ a < b⁻¹ ↔ b < a⁻¹
[PROOFSTEP]
simpa only [inv_inv] using @ENNReal.inv_lt_inv a⁻¹ b
[GOAL]
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p q : ℝ≥0
⊢ a⁻¹ ≤ b ↔ b⁻¹ ≤ a
[PROOFSTEP]
simpa only [inv_inv] using @ENNReal.inv_le_inv a b⁻¹
[GOAL]
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p q : ℝ≥0
⊢ a ≤ b⁻¹ ↔ b ≤ a⁻¹
[PROOFSTEP]
simpa only [inv_inv] using @ENNReal.inv_le_inv a⁻¹ b
[GOAL]
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p q : ℝ≥0
⊢ a⁻¹ ≤ 1 ↔ 1 ≤ a
[PROOFSTEP]
rw [inv_le_iff_inv_le, inv_one]
[GOAL]
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p q : ℝ≥0
⊢ 1 ≤ a⁻¹ ↔ a ≤ 1
[PROOFSTEP]
rw [le_inv_iff_le_inv, inv_one]
[GOAL]
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p q : ℝ≥0
⊢ a⁻¹ < 1 ↔ 1 < a
[PROOFSTEP]
rw [inv_lt_iff_inv_lt, inv_one]
[GOAL]
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p q : ℝ≥0
⊢ 1 < a⁻¹ ↔ a < 1
[PROOFSTEP]
rw [lt_inv_iff_lt_inv, inv_one]
[GOAL]
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p q : ℝ≥0
⊢ a / ⊤ = 0
[PROOFSTEP]
rw [div_eq_mul_inv, inv_top, mul_zero]
[GOAL]
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p q : ℝ≥0
⊢ ⊤ / a = if a = ⊤ then 0 else ⊤
[PROOFSTEP]
simp [div_eq_mul_inv, top_mul']
[GOAL]
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p q : ℝ≥0
h : a ≠ ⊤
⊢ ⊤ / a = ⊤
[PROOFSTEP]
simp [top_div, h]
[GOAL]
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p q : ℝ≥0
⊢ a / b = ⊤ ↔ a ≠ 0 ∧ b = 0 ∨ a = ⊤ ∧ b ≠ ⊤
[PROOFSTEP]
simp [div_eq_mul_inv, ENNReal.mul_eq_top]
[GOAL]
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p q : ℝ≥0
h0 : b ≠ 0 ∨ c ≠ 0
ht : b ≠ ⊤ ∨ c ≠ ⊤
⊢ a ≤ c / b ↔ a * b ≤ c
[PROOFSTEP]
induction' b using recTopCoe with b
[GOAL]
case top
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p q : ℝ≥0
h0✝ : b ≠ 0 ∨ c ≠ 0
ht✝ : b ≠ ⊤ ∨ c ≠ ⊤
h0 : ⊤ ≠ 0 ∨ c ≠ 0
ht : ⊤ ≠ ⊤ ∨ c ≠ ⊤
⊢ a ≤ c / ⊤ ↔ a * ⊤ ≤ c
[PROOFSTEP]
lift c to ℝ≥0 using ht.neg_resolve_left rfl
[GOAL]
case top.intro
α : Type u_1
β : Type u_2
a b d : ℝ≥0∞
r p q c : ℝ≥0
h0✝ : b ≠ 0 ∨ ↑c ≠ 0
ht✝ : b ≠ ⊤ ∨ ↑c ≠ ⊤
h0 : ⊤ ≠ 0 ∨ ↑c ≠ 0
ht : ⊤ ≠ ⊤ ∨ ↑c ≠ ⊤
⊢ a ≤ ↑c / ⊤ ↔ a * ⊤ ≤ ↑c
[PROOFSTEP]
rw [div_top, nonpos_iff_eq_zero]
[GOAL]
case top.intro
α : Type u_1
β : Type u_2
a b d : ℝ≥0∞
r p q c : ℝ≥0
h0✝ : b ≠ 0 ∨ ↑c ≠ 0
ht✝ : b ≠ ⊤ ∨ ↑c ≠ ⊤
h0 : ⊤ ≠ 0 ∨ ↑c ≠ 0
ht : ⊤ ≠ ⊤ ∨ ↑c ≠ ⊤
⊢ a = 0 ↔ a * ⊤ ≤ ↑c
[PROOFSTEP]
rcases eq_or_ne a 0 with (rfl | ha)
[GOAL]
case top.intro.inl
α : Type u_1
β : Type u_2
b d : ℝ≥0∞
r p q c : ℝ≥0
h0✝ : b ≠ 0 ∨ ↑c ≠ 0
ht✝ : b ≠ ⊤ ∨ ↑c ≠ ⊤
h0 : ⊤ ≠ 0 ∨ ↑c ≠ 0
ht : ⊤ ≠ ⊤ ∨ ↑c ≠ ⊤
⊢ 0 = 0 ↔ 0 * ⊤ ≤ ↑c
[PROOFSTEP]
simp [*]
[GOAL]
case top.intro.inr
α : Type u_1
β : Type u_2
a b d : ℝ≥0∞
r p q c : ℝ≥0
h0✝ : b ≠ 0 ∨ ↑c ≠ 0
ht✝ : b ≠ ⊤ ∨ ↑c ≠ ⊤
h0 : ⊤ ≠ 0 ∨ ↑c ≠ 0
ht : ⊤ ≠ ⊤ ∨ ↑c ≠ ⊤
ha : a ≠ 0
⊢ a = 0 ↔ a * ⊤ ≤ ↑c
[PROOFSTEP]
simp [*]
[GOAL]
case coe
α : Type u_1
β : Type u_2
a b✝ c d : ℝ≥0∞
r p q : ℝ≥0
h0✝ : b✝ ≠ 0 ∨ c ≠ 0
ht✝ : b✝ ≠ ⊤ ∨ c ≠ ⊤
b : ℝ≥0
h0 : ↑b ≠ 0 ∨ c ≠ 0
ht : ↑b ≠ ⊤ ∨ c ≠ ⊤
⊢ a ≤ c / ↑b ↔ a * ↑b ≤ c
[PROOFSTEP]
rcases eq_or_ne b 0 with (rfl | hb)
[GOAL]
case coe.inl
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p q : ℝ≥0
h0✝ : b ≠ 0 ∨ c ≠ 0
ht✝ : b ≠ ⊤ ∨ c ≠ ⊤
h0 : ↑0 ≠ 0 ∨ c ≠ 0
ht : ↑0 ≠ ⊤ ∨ c ≠ ⊤
⊢ a ≤ c / ↑0 ↔ a * ↑0 ≤ c
[PROOFSTEP]
have hc : c ≠ 0 := h0.neg_resolve_left rfl
[GOAL]
case coe.inl
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p q : ℝ≥0
h0✝ : b ≠ 0 ∨ c ≠ 0
ht✝ : b ≠ ⊤ ∨ c ≠ ⊤
h0 : ↑0 ≠ 0 ∨ c ≠ 0
ht : ↑0 ≠ ⊤ ∨ c ≠ ⊤
hc : c ≠ 0
⊢ a ≤ c / ↑0 ↔ a * ↑0 ≤ c
[PROOFSTEP]
simp [div_zero hc]
[GOAL]
case coe.inr
α : Type u_1
β : Type u_2
a b✝ c d : ℝ≥0∞
r p q : ℝ≥0
h0✝ : b✝ ≠ 0 ∨ c ≠ 0
ht✝ : b✝ ≠ ⊤ ∨ c ≠ ⊤
b : ℝ≥0
h0 : ↑b ≠ 0 ∨ c ≠ 0
ht : ↑b ≠ ⊤ ∨ c ≠ ⊤
hb : b ≠ 0
⊢ a ≤ c / ↑b ↔ a * ↑b ≤ c
[PROOFSTEP]
rw [← coe_ne_zero] at hb 
[GOAL]
case coe.inr
α : Type u_1
β : Type u_2
a b✝ c d : ℝ≥0∞
r p q : ℝ≥0
h0✝ : b✝ ≠ 0 ∨ c ≠ 0
ht✝ : b✝ ≠ ⊤ ∨ c ≠ ⊤
b : ℝ≥0
h0 : ↑b ≠ 0 ∨ c ≠ 0
ht : ↑b ≠ ⊤ ∨ c ≠ ⊤
hb : ↑b ≠ 0
⊢ a ≤ c / ↑b ↔ a * ↑b ≤ c
[PROOFSTEP]
rw [← ENNReal.mul_le_mul_right hb coe_ne_top, ENNReal.div_mul_cancel hb coe_ne_top]
[GOAL]
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p q : ℝ≥0
hb0 : b ≠ 0 ∨ c ≠ ⊤
hbt : b ≠ ⊤ ∨ c ≠ 0
⊢ a / b ≤ c ↔ a ≤ c * b
[PROOFSTEP]
suffices a * b⁻¹ ≤ c ↔ a ≤ c / b⁻¹ by simpa [div_eq_mul_inv]
[GOAL]
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p q : ℝ≥0
hb0 : b ≠ 0 ∨ c ≠ ⊤
hbt : b ≠ ⊤ ∨ c ≠ 0
this : a * b⁻¹ ≤ c ↔ a ≤ c / b⁻¹
⊢ a / b ≤ c ↔ a ≤ c * b
[PROOFSTEP]
simpa [div_eq_mul_inv]
[GOAL]
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p q : ℝ≥0
hb0 : b ≠ 0 ∨ c ≠ ⊤
hbt : b ≠ ⊤ ∨ c ≠ 0
⊢ a * b⁻¹ ≤ c ↔ a ≤ c / b⁻¹
[PROOFSTEP]
refine' (ENNReal.le_div_iff_mul_le _ _).symm
[GOAL]
case refine'_1
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p q : ℝ≥0
hb0 : b ≠ 0 ∨ c ≠ ⊤
hbt : b ≠ ⊤ ∨ c ≠ 0
⊢ b⁻¹ ≠ 0 ∨ c ≠ 0
[PROOFSTEP]
simpa
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p q : ℝ≥0
hb0 : b ≠ 0 ∨ c ≠ ⊤
hbt : b ≠ ⊤ ∨ c ≠ 0
⊢ b⁻¹ ≠ ⊤ ∨ c ≠ ⊤
[PROOFSTEP]
simpa
[GOAL]
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p q : ℝ≥0
h : a ≤ b * c
⊢ a / c ≤ b
[PROOFSTEP]
by_cases h0 : c = 0
[GOAL]
case pos
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p q : ℝ≥0
h : a ≤ b * c
h0 : c = 0
⊢ a / c ≤ b
[PROOFSTEP]
have : a = 0 := by simpa [h0] using h
[GOAL]
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p q : ℝ≥0
h : a ≤ b * c
h0 : c = 0
⊢ a = 0
[PROOFSTEP]
simpa [h0] using h
[GOAL]
case pos
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p q : ℝ≥0
h : a ≤ b * c
h0 : c = 0
this : a = 0
⊢ a / c ≤ b
[PROOFSTEP]
simp [*]
[GOAL]
case neg
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p q : ℝ≥0
h : a ≤ b * c
h0 : ¬c = 0
⊢ a / c ≤ b
[PROOFSTEP]
by_cases hinf : c = ∞
[GOAL]
case pos
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p q : ℝ≥0
h : a ≤ b * c
h0 : ¬c = 0
hinf : c = ⊤
⊢ a / c ≤ b
[PROOFSTEP]
simp [hinf]
[GOAL]
case neg
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p q : ℝ≥0
h : a ≤ b * c
h0 : ¬c = 0
hinf : ¬c = ⊤
⊢ a / c ≤ b
[PROOFSTEP]
exact (ENNReal.div_le_iff_le_mul (Or.inl h0) (Or.inl hinf)).2 h
[GOAL]
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p q : ℝ≥0
⊢ a ≤ 1 * a
[PROOFSTEP]
rw [one_mul]
[GOAL]
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p q : ℝ≥0
h : a ≤ b / c
⊢ a * c ≤ b
[PROOFSTEP]
rw [← inv_inv c]
[GOAL]
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p q : ℝ≥0
h : a ≤ b / c
⊢ a * c⁻¹⁻¹ ≤ b
[PROOFSTEP]
exact div_le_of_le_mul h
[GOAL]
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p q : ℝ≥0
h : a < b / c
⊢ a * c < b
[PROOFSTEP]
contrapose! h
[GOAL]
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p q : ℝ≥0
h : b ≤ a * c
⊢ b / c ≤ a
[PROOFSTEP]
exact ENNReal.div_le_of_le_mul h
[GOAL]
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p q : ℝ≥0
h : a < b * c
⊢ a < b / c⁻¹
[PROOFSTEP]
rwa [div_eq_mul_inv, inv_inv]
[GOAL]
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p q : ℝ≥0
h : a < b * c
⊢ a < c * b
[PROOFSTEP]
rwa [mul_comm]
[GOAL]
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p q : ℝ≥0
h₁ : b = ⊤ → a ≠ 0
h₂ : a = ⊤ → b ≠ 0
⊢ a⁻¹ ≤ b ↔ 1 ≤ a * b
[PROOFSTEP]
rw [← one_div, ENNReal.div_le_iff_le_mul, mul_comm]
[GOAL]
case hb0
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p q : ℝ≥0
h₁ : b = ⊤ → a ≠ 0
h₂ : a = ⊤ → b ≠ 0
⊢ a ≠ 0 ∨ b ≠ ⊤
case hbt α : Type u_1 β : Type u_2 a b c d : ℝ≥0∞ r p q : ℝ≥0 h₁ : b = ⊤ → a ≠ 0 h₂ : a = ⊤ → b ≠ 0 ⊢ a ≠ ⊤ ∨ b ≠ 0
[PROOFSTEP]
exacts [or_not_of_imp h₁, not_or_of_imp h₂]
[GOAL]
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p q : ℝ≥0
⊢ a ≤ b⁻¹ ↔ a * b ≤ 1
[PROOFSTEP]
rw [← one_div, ENNReal.le_div_iff_mul_le]
[GOAL]
case h0
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p q : ℝ≥0
⊢ b ≠ 0 ∨ 1 ≠ 0
[PROOFSTEP]
right
[GOAL]
case h0.h
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p q : ℝ≥0
⊢ 1 ≠ 0
[PROOFSTEP]
simp
[GOAL]
case ht
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p q : ℝ≥0
⊢ b ≠ ⊤ ∨ 1 ≠ ⊤
[PROOFSTEP]
right
[GOAL]
case ht.h
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p q : ℝ≥0
⊢ 1 ≠ ⊤
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p q : ℝ≥0
h : a * b = 1
⊢ a = b⁻¹
[PROOFSTEP]
rw [← mul_one a, ← ENNReal.mul_inv_cancel (right_ne_zero_of_mul_eq_one h), ← mul_assoc, h, one_mul]
[GOAL]
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p q : ℝ≥0
h : a * b = 1
⊢ b ≠ ⊤
[PROOFSTEP]
rintro rfl
[GOAL]
α : Type u_1
β : Type u_2
a c d : ℝ≥0∞
r p q : ℝ≥0
h : a * ⊤ = 1
⊢ False
[PROOFSTEP]
simp [left_ne_zero_of_mul_eq_one h] at h 
[GOAL]
α : Type u_1
β : Type u_2
a✝ b✝ c d : ℝ≥0∞
r✝ p q : ℝ≥0
a b r : ℝ≥0∞
hr₀ : r ≠ 0
hr₁ : r ≠ ⊤
⊢ r * a ≤ b ↔ a ≤ r⁻¹ * b
[PROOFSTEP]
rw [← @ENNReal.mul_le_mul_left _ a _ hr₀ hr₁, ← mul_assoc, ENNReal.mul_inv_cancel hr₀ hr₁, one_mul]
[GOAL]
α : Type u_1
β : Type u_2
a✝ b✝ c d : ℝ≥0∞
r✝ p q : ℝ≥0
a b : ℝ≥0∞
r : ℝ≥0
hr₀ : r ≠ 0
⊢ a ≤ r⁻¹ • b ↔ r • a ≤ b
[PROOFSTEP]
simpa [hr₀, ENNReal.smul_def] using (mul_le_iff_le_inv (coe_ne_zero.mpr hr₀) coe_ne_top).symm
[GOAL]
α : Type u_1
β : Type u_2
a✝ b✝ c d : ℝ≥0∞
r✝ p q : ℝ≥0
a b : ℝ≥0∞
r : ℝ≥0
hr₀ : r ≠ 0
⊢ r⁻¹ • a ≤ b ↔ a ≤ r • b
[PROOFSTEP]
simpa only [inv_inv] using (ENNReal.le_inv_smul_iff (inv_ne_zero hr₀)).symm
[GOAL]
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p q : ℝ≥0
x y : ℝ≥0∞
h : ∀ (r : ℝ≥0), ↑r < x → ↑r ≤ y
⊢ x ≤ y
[PROOFSTEP]
refine' le_of_forall_ge_of_dense fun r hr => _
[GOAL]
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r✝ p q : ℝ≥0
x y : ℝ≥0∞
h : ∀ (r : ℝ≥0), ↑r < x → ↑r ≤ y
r : ℝ≥0∞
hr : r < x
⊢ r ≤ y
[PROOFSTEP]
lift r to ℝ≥0 using ne_top_of_lt hr
[GOAL]
case intro
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r✝ p q : ℝ≥0
x y : ℝ≥0∞
h : ∀ (r : ℝ≥0), ↑r < x → ↑r ≤ y
r : ℝ≥0
hr : ↑r < x
⊢ ↑r ≤ y
[PROOFSTEP]
exact h r hr
[GOAL]
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p q : ℝ≥0
ha : a ≠ 0
ha' : a ≠ ⊤
h : b = c / a
⊢ a * b = c
[PROOFSTEP]
rw [h, ENNReal.mul_div_cancel' ha ha']
[GOAL]
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p q : ℝ≥0
ha : a ≠ 0
ha' : a ≠ ⊤
h : a * b = c
⊢ b = c / a
[PROOFSTEP]
rw [← h, mul_div_assoc, ENNReal.mul_div_cancel' ha ha']
[GOAL]
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p q : ℝ≥0
ha : a ≠ 0
ha' : a ≠ ⊤
hb : b ≠ 0
hb' : b ≠ ⊤
⊢ c / b = d / a ↔ a * c = b * d
[PROOFSTEP]
rw [eq_div_iff ha ha']
[GOAL]
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p q : ℝ≥0
ha : a ≠ 0
ha' : a ≠ ⊤
hb : b ≠ 0
hb' : b ≠ ⊤
⊢ a * (c / b) = d ↔ a * c = b * d
[PROOFSTEP]
conv_rhs => rw [eq_comm]
[GOAL]
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p q : ℝ≥0
ha : a ≠ 0
ha' : a ≠ ⊤
hb : b ≠ 0
hb' : b ≠ ⊤
| a * c = b * d
[PROOFSTEP]
rw [eq_comm]
[GOAL]
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p q : ℝ≥0
ha : a ≠ 0
ha' : a ≠ ⊤
hb : b ≠ 0
hb' : b ≠ ⊤
| a * c = b * d
[PROOFSTEP]
rw [eq_comm]
[GOAL]
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p q : ℝ≥0
ha : a ≠ 0
ha' : a ≠ ⊤
hb : b ≠ 0
hb' : b ≠ ⊤
| a * c = b * d
[PROOFSTEP]
rw [eq_comm]
[GOAL]
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p q : ℝ≥0
ha : a ≠ 0
ha' : a ≠ ⊤
hb : b ≠ 0
hb' : b ≠ ⊤
⊢ a * (c / b) = d ↔ b * d = a * c
[PROOFSTEP]
rw [← eq_div_iff hb hb', mul_div_assoc, eq_comm]
[GOAL]
α : Type u_1
β : Type u_2
a✝ b✝ c d : ℝ≥0∞
r p q : ℝ≥0
a b : ℝ≥0∞
hb₀ : b ≠ 0
hb₁ : b ≠ ⊤
h : a / b = 1
⊢ a = b
[PROOFSTEP]
rw [← (eq_div_iff hb₀ hb₁).mp h.symm, mul_one]
[GOAL]
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p q : ℝ≥0
⊢ 2⁻¹ + 2⁻¹ = 1
[PROOFSTEP]
rw [← two_mul, ← div_eq_mul_inv, ENNReal.div_self two_ne_zero two_ne_top]
[GOAL]
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p q : ℝ≥0
⊢ 3⁻¹ + 3⁻¹ + 3⁻¹ = 3 * 3⁻¹
[PROOFSTEP]
ring
[GOAL]
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p q : ℝ≥0
⊢ 3 ≠ 0
[PROOFSTEP]
decide
[GOAL]
α : Type u_1
β : Type u_2
a✝ b c d : ℝ≥0∞
r p q : ℝ≥0
a : ℝ≥0∞
⊢ a / 2 + a / 2 = a
[PROOFSTEP]
rw [div_eq_mul_inv, ← mul_add, inv_two_add_inv_two, mul_one]
[GOAL]
α : Type u_1
β : Type u_2
a✝ b c d : ℝ≥0∞
r p q : ℝ≥0
a : ℝ≥0∞
⊢ a / 3 + a / 3 + a / 3 = a
[PROOFSTEP]
rw [div_eq_mul_inv, ← mul_add, ← mul_add, inv_three_add_inv_three, mul_one]
[GOAL]
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p q : ℝ≥0
⊢ a / b = 0 ↔ a = 0 ∨ b = ⊤
[PROOFSTEP]
simp [div_eq_mul_inv]
[GOAL]
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p q : ℝ≥0
⊢ 0 < a / b ↔ a ≠ 0 ∧ b ≠ ⊤
[PROOFSTEP]
simp [pos_iff_ne_zero, not_or]
[GOAL]
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p q : ℝ≥0
h : a ≠ 0
⊢ 0 < a / 2
[PROOFSTEP]
simp [h]
[GOAL]
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p q : ℝ≥0
hz : a ≠ 0
ht : a ≠ ⊤
⊢ a / 2 < a
[PROOFSTEP]
lift a to ℝ≥0 using ht
[GOAL]
case intro
α : Type u_1
β : Type u_2
b c d : ℝ≥0∞
r p q a : ℝ≥0
hz : ↑a ≠ 0
⊢ ↑a / 2 < ↑a
[PROOFSTEP]
rw [coe_ne_zero] at hz 
[GOAL]
case intro
α : Type u_1
β : Type u_2
b c d : ℝ≥0∞
r p q a : ℝ≥0
hz : a ≠ 0
⊢ ↑a / 2 < ↑a
[PROOFSTEP]
rw [← coe_two, ← coe_div, coe_lt_coe]
[GOAL]
case intro
α : Type u_1
β : Type u_2
b c d : ℝ≥0∞
r p q a : ℝ≥0
hz : a ≠ 0
⊢ a / 2 < a
case intro α : Type u_1 β : Type u_2 b c d : ℝ≥0∞ r p q a : ℝ≥0 hz : a ≠ 0 ⊢ 2 ≠ 0
[PROOFSTEP]
exacts [NNReal.half_lt_self hz, two_ne_zero' _]
[GOAL]
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p q : ℝ≥0
h : a ≠ ⊤
⊢ a - a / 2 = a / 2
[PROOFSTEP]
lift a to ℝ≥0 using h
[GOAL]
case intro
α : Type u_1
β : Type u_2
b c d : ℝ≥0∞
r p q a : ℝ≥0
⊢ ↑a - ↑a / 2 = ↑a / 2
[PROOFSTEP]
exact sub_eq_of_add_eq (mul_ne_top coe_ne_top <| by simp) (ENNReal.add_halves a)
[GOAL]
α : Type u_1
β : Type u_2
b c d : ℝ≥0∞
r p q a : ℝ≥0
⊢ 2⁻¹ ≠ ⊤
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p q : ℝ≥0
⊢ 1 - 2⁻¹ = 2⁻¹
[PROOFSTEP]
simpa only [div_eq_mul_inv, one_mul] using sub_half one_ne_top
[GOAL]
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p q : ℝ≥0
⊢ ℝ≥0∞ ≃o ↑(Iic 1)
[PROOFSTEP]
refine
  StrictMono.orderIsoOfRightInverse (fun x => ⟨(x⁻¹ + 1)⁻¹, ENNReal.inv_le_one.2 <| le_add_self⟩) (fun x y hxy => ?_)
    (fun x => (x.1⁻¹ - 1)⁻¹) fun x => Subtype.ext ?_
[GOAL]
case refine_1
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p q : ℝ≥0
x y : ℝ≥0∞
hxy : x < y
⊢ (fun x => { val := (x⁻¹ + 1)⁻¹, property := (_ : (x⁻¹ + 1)⁻¹ ≤ 1) }) x <
    (fun x => { val := (x⁻¹ + 1)⁻¹, property := (_ : (x⁻¹ + 1)⁻¹ ≤ 1) }) y
[PROOFSTEP]
simpa only [Subtype.mk_lt_mk, ENNReal.inv_lt_inv, ENNReal.add_lt_add_iff_right one_ne_top]
[GOAL]
case refine_2
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p q : ℝ≥0
x : ↑(Iic 1)
⊢ ↑((fun x => { val := (x⁻¹ + 1)⁻¹, property := (_ : (x⁻¹ + 1)⁻¹ ≤ 1) }) ((fun x => ((↑x)⁻¹ - 1)⁻¹) x)) = ↑x
[PROOFSTEP]
have : (1 : ℝ≥0∞) ≤ x.1⁻¹ := ENNReal.one_le_inv.2 x.2
[GOAL]
case refine_2
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p q : ℝ≥0
x : ↑(Iic 1)
this : 1 ≤ (↑x)⁻¹
⊢ ↑((fun x => { val := (x⁻¹ + 1)⁻¹, property := (_ : (x⁻¹ + 1)⁻¹ ≤ 1) }) ((fun x => ((↑x)⁻¹ - 1)⁻¹) x)) = ↑x
[PROOFSTEP]
simp only [inv_inv, Subtype.coe_mk, tsub_add_cancel_of_le this]
[GOAL]
α : Type u_1
β : Type u_2
a✝ b c d : ℝ≥0∞
r p q a : ℝ≥0
x✝¹ x✝ : ↑(Iic a)
⊢ ↑{ toFun := fun x => { val := ↑↑x, property := (_ : ↑↑x ≤ ↑a) },
            invFun := fun x => { val := ENNReal.toNNReal ↑x, property := (_ : ENNReal.toNNReal ↑x ≤ a) },
            left_inv :=
              (_ :
                ∀ (x : ↑(Iic a)),
                  (fun x => { val := ENNReal.toNNReal ↑x, property := (_ : ENNReal.toNNReal ↑x ≤ a) })
                      ((fun x => { val := ↑↑x, property := (_ : ↑↑x ≤ ↑a) }) x) =
                    x),
            right_inv :=
              (_ :
                ∀ (x : ↑(Iic ↑a)),
                  (fun x => { val := ↑↑x, property := (_ : ↑↑x ≤ ↑a) })
                      ((fun x => { val := ENNReal.toNNReal ↑x, property := (_ : ENNReal.toNNReal ↑x ≤ a) }) x) =
                    x) }
        x✝¹ ≤
      ↑{ toFun := fun x => { val := ↑↑x, property := (_ : ↑↑x ≤ ↑a) },
            invFun := fun x => { val := ENNReal.toNNReal ↑x, property := (_ : ENNReal.toNNReal ↑x ≤ a) },
            left_inv :=
              (_ :
                ∀ (x : ↑(Iic a)),
                  (fun x => { val := ENNReal.toNNReal ↑x, property := (_ : ENNReal.toNNReal ↑x ≤ a) })
                      ((fun x => { val := ↑↑x, property := (_ : ↑↑x ≤ ↑a) }) x) =
                    x),
            right_inv :=
              (_ :
                ∀ (x : ↑(Iic ↑a)),
                  (fun x => { val := ↑↑x, property := (_ : ↑↑x ≤ ↑a) })
                      ((fun x => { val := ENNReal.toNNReal ↑x, property := (_ : ENNReal.toNNReal ↑x ≤ a) }) x) =
                    x) }
        x✝ ↔
    x✝¹ ≤ x✝
[PROOFSTEP]
simp only [Equiv.coe_fn_mk, Subtype.mk_le_mk, coe_le_coe, Subtype.coe_le_coe]
[GOAL]
α : Type u_1
β : Type u_2
a✝ b c d : ℝ≥0∞
r p q : ℝ≥0
a : ℝ≥0∞
h : a ≠ 0
⊢ ∃ n, (↑n)⁻¹ < a⁻¹⁻¹
[PROOFSTEP]
simp only [ENNReal.inv_lt_inv, ENNReal.exists_nat_gt (inv_ne_top.2 h)]
[GOAL]
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p q : ℝ≥0
ha : a ≠ 0
hb : b ≠ ⊤
n : ℕ
hn : b / a < ↑n
⊢ b < ↑n * a
[PROOFSTEP]
rwa [← ENNReal.div_lt_iff (Or.inl ha) (Or.inr hb)]
[GOAL]
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p q : ℝ≥0
ha : a ≠ ⊤
hb : b ≠ 0
⊢ ∃ n, n > 0 ∧ (↑n)⁻¹ * a < b
[PROOFSTEP]
rcases exists_nat_pos_mul_gt hb ha with ⟨n, npos, hn⟩
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p q : ℝ≥0
ha : a ≠ ⊤
hb : b ≠ 0
n : ℕ
npos : n > 0
hn : a < ↑n * b
⊢ ∃ n, n > 0 ∧ (↑n)⁻¹ * a < b
[PROOFSTEP]
use n, npos
[GOAL]
case right
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p q : ℝ≥0
ha : a ≠ ⊤
hb : b ≠ 0
n : ℕ
npos : n > 0
hn : a < ↑n * b
⊢ (↑n)⁻¹ * a < b
[PROOFSTEP]
rw [← ENNReal.div_eq_inv_mul]
[GOAL]
case right
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p q : ℝ≥0
ha : a ≠ ⊤
hb : b ≠ 0
n : ℕ
npos : n > 0
hn : a < ↑n * b
⊢ a / ↑n < b
[PROOFSTEP]
exact div_lt_of_lt_mul' hn
[GOAL]
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p q : ℝ≥0
ha : a ≠ ⊤
hb : b ≠ 0
⊢ ∃ n, n > 0 ∧ ↑n * a < b
[PROOFSTEP]
rcases exists_nat_pos_inv_mul_lt ha hb with ⟨n, npos : 0 < n, hn⟩
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p q : ℝ≥0
ha : a ≠ ⊤
hb : b ≠ 0
n : ℕ
npos : 0 < n
hn : (↑n)⁻¹ * a < b
⊢ ∃ n, n > 0 ∧ ↑n * a < b
[PROOFSTEP]
use(n : ℝ≥0)⁻¹
[GOAL]
case h
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p q : ℝ≥0
ha : a ≠ ⊤
hb : b ≠ 0
n : ℕ
npos : 0 < n
hn : (↑n)⁻¹ * a < b
⊢ (↑n)⁻¹ > 0 ∧ ↑(↑n)⁻¹ * a < b
[PROOFSTEP]
simp [*, npos.ne', zero_lt_one]
[GOAL]
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p q : ℝ≥0
ha : a ≠ 0
⊢ ∃ n, 2⁻¹ ^ n < a
[PROOFSTEP]
rcases exists_inv_nat_lt ha with ⟨n, hn⟩
[GOAL]
case intro
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p q : ℝ≥0
ha : a ≠ 0
n : ℕ
hn : (↑n)⁻¹ < a
⊢ ∃ n, 2⁻¹ ^ n < a
[PROOFSTEP]
refine' ⟨n, lt_trans _ hn⟩
[GOAL]
case intro
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p q : ℝ≥0
ha : a ≠ 0
n : ℕ
hn : (↑n)⁻¹ < a
⊢ 2⁻¹ ^ n < (↑n)⁻¹
[PROOFSTEP]
rw [← ENNReal.inv_pow, ENNReal.inv_lt_inv]
[GOAL]
case intro
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p q : ℝ≥0
ha : a ≠ 0
n : ℕ
hn : (↑n)⁻¹ < a
⊢ ↑n < 2 ^ n
[PROOFSTEP]
norm_cast
[GOAL]
case intro
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p q : ℝ≥0
ha : a ≠ 0
n : ℕ
hn : (↑n)⁻¹ < a
⊢ n < 2 ^ n
[PROOFSTEP]
exact n.lt_two_pow
[GOAL]
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p q : ℝ≥0
hr : r ≠ 0
n : ℤ
⊢ ↑(r ^ n) = ↑r ^ n
[PROOFSTEP]
cases' n with n n
[GOAL]
case ofNat
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p q : ℝ≥0
hr : r ≠ 0
n : ℕ
⊢ ↑(r ^ Int.ofNat n) = ↑r ^ Int.ofNat n
[PROOFSTEP]
simp only [Int.ofNat_eq_coe, coe_pow, zpow_ofNat]
[GOAL]
case negSucc
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p q : ℝ≥0
hr : r ≠ 0
n : ℕ
⊢ ↑(r ^ Int.negSucc n) = ↑r ^ Int.negSucc n
[PROOFSTEP]
have : r ^ n.succ ≠ 0 := pow_ne_zero (n + 1) hr
[GOAL]
case negSucc
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p q : ℝ≥0
hr : r ≠ 0
n : ℕ
this : r ^ Nat.succ n ≠ 0
⊢ ↑(r ^ Int.negSucc n) = ↑r ^ Int.negSucc n
[PROOFSTEP]
simp only [zpow_negSucc, coe_inv this, coe_pow]
[GOAL]
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p q : ℝ≥0
ha : a ≠ 0
h'a : a ≠ ⊤
n : ℤ
⊢ 0 < a ^ n
[PROOFSTEP]
cases n
[GOAL]
case ofNat
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p q : ℝ≥0
ha : a ≠ 0
h'a : a ≠ ⊤
a✝ : ℕ
⊢ 0 < a ^ Int.ofNat a✝
[PROOFSTEP]
exact ENNReal.pow_pos ha.bot_lt _
[GOAL]
case negSucc
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p q : ℝ≥0
ha : a ≠ 0
h'a : a ≠ ⊤
a✝ : ℕ
⊢ 0 < a ^ Int.negSucc a✝
[PROOFSTEP]
simp only [h'a, pow_eq_top_iff, zpow_negSucc, Ne.def, not_false, ENNReal.inv_pos, false_and]
[GOAL]
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p q : ℝ≥0
ha : a ≠ 0
h'a : a ≠ ⊤
n : ℤ
⊢ a ^ n < ⊤
[PROOFSTEP]
cases n
[GOAL]
case ofNat
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p q : ℝ≥0
ha : a ≠ 0
h'a : a ≠ ⊤
a✝ : ℕ
⊢ a ^ Int.ofNat a✝ < ⊤
[PROOFSTEP]
exact ENNReal.pow_lt_top h'a.lt_top _
[GOAL]
case negSucc
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p q : ℝ≥0
ha : a ≠ 0
h'a : a ≠ ⊤
a✝ : ℕ
⊢ a ^ Int.negSucc a✝ < ⊤
[PROOFSTEP]
simp only [ENNReal.pow_pos ha.bot_lt, zpow_negSucc, inv_lt_top]
[GOAL]
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p q : ℝ≥0
x y : ℝ≥0∞
hx : x ≠ 0
h'x : x ≠ ⊤
hy : 1 < y
h'y : y ≠ ⊤
⊢ ∃ n, x ∈ Ico (y ^ n) (y ^ (n + 1))
[PROOFSTEP]
lift x to ℝ≥0 using h'x
[GOAL]
case intro
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p q : ℝ≥0
y : ℝ≥0∞
hy : 1 < y
h'y : y ≠ ⊤
x : ℝ≥0
hx : ↑x ≠ 0
⊢ ∃ n, ↑x ∈ Ico (y ^ n) (y ^ (n + 1))
[PROOFSTEP]
lift y to ℝ≥0 using h'y
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p q x : ℝ≥0
hx : ↑x ≠ 0
y : ℝ≥0
hy : 1 < ↑y
⊢ ∃ n, ↑x ∈ Ico (↑y ^ n) (↑y ^ (n + 1))
[PROOFSTEP]
have A : y ≠ 0 := by simpa only [Ne.def, coe_eq_zero] using (zero_lt_one.trans hy).ne'
[GOAL]
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p q x : ℝ≥0
hx : ↑x ≠ 0
y : ℝ≥0
hy : 1 < ↑y
⊢ y ≠ 0
[PROOFSTEP]
simpa only [Ne.def, coe_eq_zero] using (zero_lt_one.trans hy).ne'
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p q x : ℝ≥0
hx : ↑x ≠ 0
y : ℝ≥0
hy : 1 < ↑y
A : y ≠ 0
⊢ ∃ n, ↑x ∈ Ico (↑y ^ n) (↑y ^ (n + 1))
[PROOFSTEP]
obtain ⟨n, hn, h'n⟩ : ∃ n : ℤ, y ^ n ≤ x ∧ x < y ^ (n + 1) :=
  by
  refine' NNReal.exists_mem_Ico_zpow _ (one_lt_coe_iff.1 hy)
  simpa only [Ne.def, coe_eq_zero] using hx
[GOAL]
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p q x : ℝ≥0
hx : ↑x ≠ 0
y : ℝ≥0
hy : 1 < ↑y
A : y ≠ 0
⊢ ∃ n, y ^ n ≤ x ∧ x < y ^ (n + 1)
[PROOFSTEP]
refine' NNReal.exists_mem_Ico_zpow _ (one_lt_coe_iff.1 hy)
[GOAL]
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p q x : ℝ≥0
hx : ↑x ≠ 0
y : ℝ≥0
hy : 1 < ↑y
A : y ≠ 0
⊢ x ≠ 0
[PROOFSTEP]
simpa only [Ne.def, coe_eq_zero] using hx
[GOAL]
case intro.intro.intro.intro
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p q x : ℝ≥0
hx : ↑x ≠ 0
y : ℝ≥0
hy : 1 < ↑y
A : y ≠ 0
n : ℤ
hn : y ^ n ≤ x
h'n : x < y ^ (n + 1)
⊢ ∃ n, ↑x ∈ Ico (↑y ^ n) (↑y ^ (n + 1))
[PROOFSTEP]
refine' ⟨n, _, _⟩
[GOAL]
case intro.intro.intro.intro.refine'_1
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p q x : ℝ≥0
hx : ↑x ≠ 0
y : ℝ≥0
hy : 1 < ↑y
A : y ≠ 0
n : ℤ
hn : y ^ n ≤ x
h'n : x < y ^ (n + 1)
⊢ ↑y ^ n ≤ ↑x
[PROOFSTEP]
rwa [← ENNReal.coe_zpow A, ENNReal.coe_le_coe]
[GOAL]
case intro.intro.intro.intro.refine'_2
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p q x : ℝ≥0
hx : ↑x ≠ 0
y : ℝ≥0
hy : 1 < ↑y
A : y ≠ 0
n : ℤ
hn : y ^ n ≤ x
h'n : x < y ^ (n + 1)
⊢ ↑x < ↑y ^ (n + 1)
[PROOFSTEP]
rwa [← ENNReal.coe_zpow A, ENNReal.coe_lt_coe]
[GOAL]
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p q : ℝ≥0
x y : ℝ≥0∞
hx : x ≠ 0
h'x : x ≠ ⊤
hy : 1 < y
h'y : y ≠ ⊤
⊢ ∃ n, x ∈ Ioc (y ^ n) (y ^ (n + 1))
[PROOFSTEP]
lift x to ℝ≥0 using h'x
[GOAL]
case intro
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p q : ℝ≥0
y : ℝ≥0∞
hy : 1 < y
h'y : y ≠ ⊤
x : ℝ≥0
hx : ↑x ≠ 0
⊢ ∃ n, ↑x ∈ Ioc (y ^ n) (y ^ (n + 1))
[PROOFSTEP]
lift y to ℝ≥0 using h'y
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p q x : ℝ≥0
hx : ↑x ≠ 0
y : ℝ≥0
hy : 1 < ↑y
⊢ ∃ n, ↑x ∈ Ioc (↑y ^ n) (↑y ^ (n + 1))
[PROOFSTEP]
have A : y ≠ 0 := by simpa only [Ne.def, coe_eq_zero] using (zero_lt_one.trans hy).ne'
[GOAL]
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p q x : ℝ≥0
hx : ↑x ≠ 0
y : ℝ≥0
hy : 1 < ↑y
⊢ y ≠ 0
[PROOFSTEP]
simpa only [Ne.def, coe_eq_zero] using (zero_lt_one.trans hy).ne'
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p q x : ℝ≥0
hx : ↑x ≠ 0
y : ℝ≥0
hy : 1 < ↑y
A : y ≠ 0
⊢ ∃ n, ↑x ∈ Ioc (↑y ^ n) (↑y ^ (n + 1))
[PROOFSTEP]
obtain ⟨n, hn, h'n⟩ : ∃ n : ℤ, y ^ n < x ∧ x ≤ y ^ (n + 1) :=
  by
  refine' NNReal.exists_mem_Ioc_zpow _ (one_lt_coe_iff.1 hy)
  simpa only [Ne.def, coe_eq_zero] using hx
[GOAL]
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p q x : ℝ≥0
hx : ↑x ≠ 0
y : ℝ≥0
hy : 1 < ↑y
A : y ≠ 0
⊢ ∃ n, y ^ n < x ∧ x ≤ y ^ (n + 1)
[PROOFSTEP]
refine' NNReal.exists_mem_Ioc_zpow _ (one_lt_coe_iff.1 hy)
[GOAL]
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p q x : ℝ≥0
hx : ↑x ≠ 0
y : ℝ≥0
hy : 1 < ↑y
A : y ≠ 0
⊢ x ≠ 0
[PROOFSTEP]
simpa only [Ne.def, coe_eq_zero] using hx
[GOAL]
case intro.intro.intro.intro
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p q x : ℝ≥0
hx : ↑x ≠ 0
y : ℝ≥0
hy : 1 < ↑y
A : y ≠ 0
n : ℤ
hn : y ^ n < x
h'n : x ≤ y ^ (n + 1)
⊢ ∃ n, ↑x ∈ Ioc (↑y ^ n) (↑y ^ (n + 1))
[PROOFSTEP]
refine' ⟨n, _, _⟩
[GOAL]
case intro.intro.intro.intro.refine'_1
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p q x : ℝ≥0
hx : ↑x ≠ 0
y : ℝ≥0
hy : 1 < ↑y
A : y ≠ 0
n : ℤ
hn : y ^ n < x
h'n : x ≤ y ^ (n + 1)
⊢ ↑y ^ n < ↑x
[PROOFSTEP]
rwa [← ENNReal.coe_zpow A, ENNReal.coe_lt_coe]
[GOAL]
case intro.intro.intro.intro.refine'_2
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p q x : ℝ≥0
hx : ↑x ≠ 0
y : ℝ≥0
hy : 1 < ↑y
A : y ≠ 0
n : ℤ
hn : y ^ n < x
h'n : x ≤ y ^ (n + 1)
⊢ ↑x ≤ ↑y ^ (n + 1)
[PROOFSTEP]
rwa [← ENNReal.coe_zpow A, ENNReal.coe_le_coe]
[GOAL]
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p q : ℝ≥0
y : ℝ≥0∞
hy : 1 < y
h'y : y ≠ ⊤
⊢ Ioo 0 ⊤ = ⋃ (n : ℤ), Ico (y ^ n) (y ^ (n + 1))
[PROOFSTEP]
ext x
[GOAL]
case h
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p q : ℝ≥0
y : ℝ≥0∞
hy : 1 < y
h'y : y ≠ ⊤
x : ℝ≥0∞
⊢ x ∈ Ioo 0 ⊤ ↔ x ∈ ⋃ (n : ℤ), Ico (y ^ n) (y ^ (n + 1))
[PROOFSTEP]
simp only [mem_iUnion, mem_Ioo, mem_Ico]
[GOAL]
case h
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p q : ℝ≥0
y : ℝ≥0∞
hy : 1 < y
h'y : y ≠ ⊤
x : ℝ≥0∞
⊢ 0 < x ∧ x < ⊤ ↔ ∃ i, y ^ i ≤ x ∧ x < y ^ (i + 1)
[PROOFSTEP]
constructor
[GOAL]
case h.mp
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p q : ℝ≥0
y : ℝ≥0∞
hy : 1 < y
h'y : y ≠ ⊤
x : ℝ≥0∞
⊢ 0 < x ∧ x < ⊤ → ∃ i, y ^ i ≤ x ∧ x < y ^ (i + 1)
[PROOFSTEP]
rintro ⟨hx, h'x⟩
[GOAL]
case h.mp.intro
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p q : ℝ≥0
y : ℝ≥0∞
hy : 1 < y
h'y : y ≠ ⊤
x : ℝ≥0∞
hx : 0 < x
h'x : x < ⊤
⊢ ∃ i, y ^ i ≤ x ∧ x < y ^ (i + 1)
[PROOFSTEP]
exact exists_mem_Ico_zpow hx.ne' h'x.ne hy h'y
[GOAL]
case h.mpr
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p q : ℝ≥0
y : ℝ≥0∞
hy : 1 < y
h'y : y ≠ ⊤
x : ℝ≥0∞
⊢ (∃ i, y ^ i ≤ x ∧ x < y ^ (i + 1)) → 0 < x ∧ x < ⊤
[PROOFSTEP]
rintro ⟨n, hn, h'n⟩
[GOAL]
case h.mpr.intro.intro
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p q : ℝ≥0
y : ℝ≥0∞
hy : 1 < y
h'y : y ≠ ⊤
x : ℝ≥0∞
n : ℤ
hn : y ^ n ≤ x
h'n : x < y ^ (n + 1)
⊢ 0 < x ∧ x < ⊤
[PROOFSTEP]
constructor
[GOAL]
case h.mpr.intro.intro.left
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p q : ℝ≥0
y : ℝ≥0∞
hy : 1 < y
h'y : y ≠ ⊤
x : ℝ≥0∞
n : ℤ
hn : y ^ n ≤ x
h'n : x < y ^ (n + 1)
⊢ 0 < x
[PROOFSTEP]
apply lt_of_lt_of_le _ hn
[GOAL]
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p q : ℝ≥0
y : ℝ≥0∞
hy : 1 < y
h'y : y ≠ ⊤
x : ℝ≥0∞
n : ℤ
hn : y ^ n ≤ x
h'n : x < y ^ (n + 1)
⊢ 0 < y ^ n
[PROOFSTEP]
exact ENNReal.zpow_pos (zero_lt_one.trans hy).ne' h'y _
[GOAL]
case h.mpr.intro.intro.right
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p q : ℝ≥0
y : ℝ≥0∞
hy : 1 < y
h'y : y ≠ ⊤
x : ℝ≥0∞
n : ℤ
hn : y ^ n ≤ x
h'n : x < y ^ (n + 1)
⊢ x < ⊤
[PROOFSTEP]
apply lt_trans h'n _
[GOAL]
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p q : ℝ≥0
y : ℝ≥0∞
hy : 1 < y
h'y : y ≠ ⊤
x : ℝ≥0∞
n : ℤ
hn : y ^ n ≤ x
h'n : x < y ^ (n + 1)
⊢ y ^ (n + 1) < ⊤
[PROOFSTEP]
exact ENNReal.zpow_lt_top (zero_lt_one.trans hy).ne' h'y _
[GOAL]
α : Type u_1
β : Type u_2
a✝ b✝ c d : ℝ≥0∞
r p q : ℝ≥0
x : ℝ≥0∞
hx : 1 ≤ x
a b : ℤ
h : a ≤ b
⊢ x ^ a ≤ x ^ b
[PROOFSTEP]
induction' a with a a
[GOAL]
case ofNat
α : Type u_1
β : Type u_2
a✝¹ b✝ c d : ℝ≥0∞
r p q : ℝ≥0
x : ℝ≥0∞
hx : 1 ≤ x
a✝ b : ℤ
h✝ : a✝ ≤ b
a : ℕ
h : Int.ofNat a ≤ b
⊢ x ^ Int.ofNat a ≤ x ^ b
[PROOFSTEP]
induction' b with b b
[GOAL]
case negSucc
α : Type u_1
β : Type u_2
a✝¹ b✝ c d : ℝ≥0∞
r p q : ℝ≥0
x : ℝ≥0∞
hx : 1 ≤ x
a✝ b : ℤ
h✝ : a✝ ≤ b
a : ℕ
h : Int.negSucc a ≤ b
⊢ x ^ Int.negSucc a ≤ x ^ b
[PROOFSTEP]
induction' b with b b
[GOAL]
case ofNat.ofNat
α : Type u_1
β : Type u_2
a✝¹ b✝¹ c d : ℝ≥0∞
r p q : ℝ≥0
x : ℝ≥0∞
hx : 1 ≤ x
a✝ b✝ : ℤ
h✝² : a✝ ≤ b✝
a : ℕ
h✝¹ : Int.ofNat a ≤ b✝
b : ℕ
h✝ : a✝ ≤ Int.ofNat b
h : Int.ofNat a ≤ Int.ofNat b
⊢ x ^ Int.ofNat a ≤ x ^ Int.ofNat b
[PROOFSTEP]
simp only [Int.ofNat_eq_coe, zpow_ofNat]
[GOAL]
case ofNat.ofNat
α : Type u_1
β : Type u_2
a✝¹ b✝¹ c d : ℝ≥0∞
r p q : ℝ≥0
x : ℝ≥0∞
hx : 1 ≤ x
a✝ b✝ : ℤ
h✝² : a✝ ≤ b✝
a : ℕ
h✝¹ : Int.ofNat a ≤ b✝
b : ℕ
h✝ : a✝ ≤ Int.ofNat b
h : Int.ofNat a ≤ Int.ofNat b
⊢ x ^ a ≤ x ^ b
[PROOFSTEP]
exact pow_le_pow hx (Int.le_of_ofNat_le_ofNat h)
[GOAL]
case ofNat.negSucc
α : Type u_1
β : Type u_2
a✝¹ b✝¹ c d : ℝ≥0∞
r p q : ℝ≥0
x : ℝ≥0∞
hx : 1 ≤ x
a✝ b✝ : ℤ
h✝² : a✝ ≤ b✝
a : ℕ
h✝¹ : Int.ofNat a ≤ b✝
b : ℕ
h✝ : a✝ ≤ Int.negSucc b
h : Int.ofNat a ≤ Int.negSucc b
⊢ x ^ Int.ofNat a ≤ x ^ Int.negSucc b
[PROOFSTEP]
apply absurd h (not_le_of_gt _)
[GOAL]
α : Type u_1
β : Type u_2
a✝¹ b✝¹ c d : ℝ≥0∞
r p q : ℝ≥0
x : ℝ≥0∞
hx : 1 ≤ x
a✝ b✝ : ℤ
h✝² : a✝ ≤ b✝
a : ℕ
h✝¹ : Int.ofNat a ≤ b✝
b : ℕ
h✝ : a✝ ≤ Int.negSucc b
h : Int.ofNat a ≤ Int.negSucc b
⊢ Int.ofNat a > Int.negSucc b
[PROOFSTEP]
exact lt_of_lt_of_le (Int.negSucc_lt_zero _) (Int.ofNat_nonneg _)
[GOAL]
case negSucc.ofNat
α : Type u_1
β : Type u_2
a✝¹ b✝¹ c d : ℝ≥0∞
r p q : ℝ≥0
x : ℝ≥0∞
hx : 1 ≤ x
a✝ b✝ : ℤ
h✝² : a✝ ≤ b✝
a : ℕ
h✝¹ : Int.negSucc a ≤ b✝
b : ℕ
h✝ : a✝ ≤ Int.ofNat b
h : Int.negSucc a ≤ Int.ofNat b
⊢ x ^ Int.negSucc a ≤ x ^ Int.ofNat b
[PROOFSTEP]
simp only [zpow_negSucc, Int.ofNat_eq_coe, zpow_ofNat]
[GOAL]
case negSucc.ofNat
α : Type u_1
β : Type u_2
a✝¹ b✝¹ c d : ℝ≥0∞
r p q : ℝ≥0
x : ℝ≥0∞
hx : 1 ≤ x
a✝ b✝ : ℤ
h✝² : a✝ ≤ b✝
a : ℕ
h✝¹ : Int.negSucc a ≤ b✝
b : ℕ
h✝ : a✝ ≤ Int.ofNat b
h : Int.negSucc a ≤ Int.ofNat b
⊢ (x ^ (a + 1))⁻¹ ≤ x ^ b
[PROOFSTEP]
refine' (ENNReal.inv_le_one.2 _).trans _
[GOAL]
case negSucc.ofNat.refine'_1
α : Type u_1
β : Type u_2
a✝¹ b✝¹ c d : ℝ≥0∞
r p q : ℝ≥0
x : ℝ≥0∞
hx : 1 ≤ x
a✝ b✝ : ℤ
h✝² : a✝ ≤ b✝
a : ℕ
h✝¹ : Int.negSucc a ≤ b✝
b : ℕ
h✝ : a✝ ≤ Int.ofNat b
h : Int.negSucc a ≤ Int.ofNat b
⊢ 1 ≤ x ^ (a + 1)
[PROOFSTEP]
exact one_le_pow_of_one_le' hx _
[GOAL]
case negSucc.ofNat.refine'_2
α : Type u_1
β : Type u_2
a✝¹ b✝¹ c d : ℝ≥0∞
r p q : ℝ≥0
x : ℝ≥0∞
hx : 1 ≤ x
a✝ b✝ : ℤ
h✝² : a✝ ≤ b✝
a : ℕ
h✝¹ : Int.negSucc a ≤ b✝
b : ℕ
h✝ : a✝ ≤ Int.ofNat b
h : Int.negSucc a ≤ Int.ofNat b
⊢ 1 ≤ x ^ b
[PROOFSTEP]
exact one_le_pow_of_one_le' hx _
[GOAL]
case negSucc.negSucc
α : Type u_1
β : Type u_2
a✝¹ b✝¹ c d : ℝ≥0∞
r p q : ℝ≥0
x : ℝ≥0∞
hx : 1 ≤ x
a✝ b✝ : ℤ
h✝² : a✝ ≤ b✝
a : ℕ
h✝¹ : Int.negSucc a ≤ b✝
b : ℕ
h✝ : a✝ ≤ Int.negSucc b
h : Int.negSucc a ≤ Int.negSucc b
⊢ x ^ Int.negSucc a ≤ x ^ Int.negSucc b
[PROOFSTEP]
simp only [zpow_negSucc, ENNReal.inv_le_inv]
[GOAL]
case negSucc.negSucc
α : Type u_1
β : Type u_2
a✝¹ b✝¹ c d : ℝ≥0∞
r p q : ℝ≥0
x : ℝ≥0∞
hx : 1 ≤ x
a✝ b✝ : ℤ
h✝² : a✝ ≤ b✝
a : ℕ
h✝¹ : Int.negSucc a ≤ b✝
b : ℕ
h✝ : a✝ ≤ Int.negSucc b
h : Int.negSucc a ≤ Int.negSucc b
⊢ x ^ (b + 1) ≤ x ^ (a + 1)
[PROOFSTEP]
apply pow_le_pow hx
[GOAL]
case negSucc.negSucc
α : Type u_1
β : Type u_2
a✝¹ b✝¹ c d : ℝ≥0∞
r p q : ℝ≥0
x : ℝ≥0∞
hx : 1 ≤ x
a✝ b✝ : ℤ
h✝² : a✝ ≤ b✝
a : ℕ
h✝¹ : Int.negSucc a ≤ b✝
b : ℕ
h✝ : a✝ ≤ Int.negSucc b
h : Int.negSucc a ≤ Int.negSucc b
⊢ b + 1 ≤ a + 1
[PROOFSTEP]
simpa only [← Int.ofNat_le, neg_le_neg_iff, Int.ofNat_add, Int.ofNat_one, Int.negSucc_eq] using h
[GOAL]
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p q : ℝ≥0
x : ℝ≥0∞
hx : x ≠ 0
h'x : x ≠ ⊤
m n : ℤ
⊢ x ^ (m + n) = x ^ m * x ^ n
[PROOFSTEP]
lift x to ℝ≥0 using h'x
[GOAL]
case intro
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p q : ℝ≥0
m n : ℤ
x : ℝ≥0
hx : ↑x ≠ 0
⊢ ↑x ^ (m + n) = ↑x ^ m * ↑x ^ n
[PROOFSTEP]
replace hx : x ≠ 0
[GOAL]
case hx
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p q : ℝ≥0
m n : ℤ
x : ℝ≥0
hx : ↑x ≠ 0
⊢ x ≠ 0
[PROOFSTEP]
simpa only [Ne.def, coe_eq_zero] using hx
[GOAL]
case intro
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p q : ℝ≥0
m n : ℤ
x : ℝ≥0
hx : x ≠ 0
⊢ ↑x ^ (m + n) = ↑x ^ m * ↑x ^ n
[PROOFSTEP]
simp only [← coe_zpow hx, zpow_add₀ hx, coe_mul]
[GOAL]
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p q : ℝ≥0
ha : a ≠ ⊤
hb : b ≠ ⊤
⊢ ENNReal.toReal (a + b) = ENNReal.toReal a + ENNReal.toReal b
[PROOFSTEP]
lift a to ℝ≥0 using ha
[GOAL]
case intro
α : Type u_1
β : Type u_2
b c d : ℝ≥0∞
r p q : ℝ≥0
hb : b ≠ ⊤
a : ℝ≥0
⊢ ENNReal.toReal (↑a + b) = ENNReal.toReal ↑a + ENNReal.toReal b
[PROOFSTEP]
lift b to ℝ≥0 using hb
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
c d : ℝ≥0∞
r p q a b : ℝ≥0
⊢ ENNReal.toReal (↑a + ↑b) = ENNReal.toReal ↑a + ENNReal.toReal ↑b
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
a✝ b✝ c d : ℝ≥0∞
r p q : ℝ≥0
a b : ℝ≥0∞
h : b ≤ a
ha : a ≠ ⊤
⊢ ENNReal.toReal (a - b) = ENNReal.toReal a - ENNReal.toReal b
[PROOFSTEP]
lift b to ℝ≥0 using ne_top_of_le_ne_top ha h
[GOAL]
case intro
α : Type u_1
β : Type u_2
a✝ b✝ c d : ℝ≥0∞
r p q : ℝ≥0
a : ℝ≥0∞
ha : a ≠ ⊤
b : ℝ≥0
h : ↑b ≤ a
⊢ ENNReal.toReal (a - ↑b) = ENNReal.toReal a - ENNReal.toReal ↑b
[PROOFSTEP]
lift a to ℝ≥0 using ha
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
a✝ b✝ c d : ℝ≥0∞
r p q b a : ℝ≥0
h : ↑b ≤ ↑a
⊢ ENNReal.toReal (↑a - ↑b) = ENNReal.toReal ↑a - ENNReal.toReal ↑b
[PROOFSTEP]
simp only [← ENNReal.coe_sub, ENNReal.coe_toReal, NNReal.coe_sub (ENNReal.coe_le_coe.mp h)]
[GOAL]
α : Type u_1
β : Type u_2
a✝ b✝ c d : ℝ≥0∞
r p q : ℝ≥0
a b : ℝ≥0∞
hb : b ≠ ⊤
⊢ ENNReal.toReal a - ENNReal.toReal b ≤ ENNReal.toReal (a - b)
[PROOFSTEP]
lift b to ℝ≥0 using hb
[GOAL]
case intro
α : Type u_1
β : Type u_2
a✝ b✝ c d : ℝ≥0∞
r p q : ℝ≥0
a : ℝ≥0∞
b : ℝ≥0
⊢ ENNReal.toReal a - ENNReal.toReal ↑b ≤ ENNReal.toReal (a - ↑b)
[PROOFSTEP]
induction a using recTopCoe
[GOAL]
case intro.top
α : Type u_1
β : Type u_2
a b✝ c d : ℝ≥0∞
r p q b : ℝ≥0
⊢ ENNReal.toReal ⊤ - ENNReal.toReal ↑b ≤ ENNReal.toReal (⊤ - ↑b)
[PROOFSTEP]
simp
[GOAL]
case intro.coe
α : Type u_1
β : Type u_2
a b✝ c d : ℝ≥0∞
r p q b x✝ : ℝ≥0
⊢ ENNReal.toReal ↑x✝ - ENNReal.toReal ↑b ≤ ENNReal.toReal (↑x✝ - ↑b)
[PROOFSTEP]
simp only [← coe_sub, NNReal.sub_def, Real.coe_toNNReal', coe_toReal]
[GOAL]
case intro.coe
α : Type u_1
β : Type u_2
a b✝ c d : ℝ≥0∞
r p q b x✝ : ℝ≥0
⊢ ↑x✝ - ↑b ≤ max (↑x✝ - ↑b) 0
[PROOFSTEP]
exact le_max_left _ _
[GOAL]
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p q : ℝ≥0
ha : a = ⊤
⊢ ENNReal.toReal (a + b) ≤ ENNReal.toReal a + ENNReal.toReal b
[PROOFSTEP]
simp only [ha, top_add, top_toReal, zero_add, toReal_nonneg]
[GOAL]
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p q : ℝ≥0
ha : ¬a = ⊤
hb : b = ⊤
⊢ ENNReal.toReal (a + b) ≤ ENNReal.toReal a + ENNReal.toReal b
[PROOFSTEP]
simp only [hb, add_top, top_toReal, add_zero, toReal_nonneg]
[GOAL]
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p✝ q✝ : ℝ≥0
p q : ℝ
hp : 0 ≤ p
hq : 0 ≤ q
⊢ ENNReal.ofReal (p + q) = ENNReal.ofReal p + ENNReal.ofReal q
[PROOFSTEP]
rw [ENNReal.ofReal, ENNReal.ofReal, ENNReal.ofReal, ← coe_add, coe_eq_coe, Real.toNNReal_add hp hq]
[GOAL]
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p q : ℝ≥0
ha : a ≠ ⊤
hb : b ≠ ⊤
⊢ ENNReal.toReal a ≤ ENNReal.toReal b ↔ a ≤ b
[PROOFSTEP]
lift a to ℝ≥0 using ha
[GOAL]
case intro
α : Type u_1
β : Type u_2
b c d : ℝ≥0∞
r p q : ℝ≥0
hb : b ≠ ⊤
a : ℝ≥0
⊢ ENNReal.toReal ↑a ≤ ENNReal.toReal b ↔ ↑a ≤ b
[PROOFSTEP]
lift b to ℝ≥0 using hb
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
c d : ℝ≥0∞
r p q a b : ℝ≥0
⊢ ENNReal.toReal ↑a ≤ ENNReal.toReal ↑b ↔ ↑a ≤ ↑b
[PROOFSTEP]
norm_cast
[GOAL]
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p q : ℝ≥0
h : a ≤ b
ht : b = ⊤ → a = ⊤
⊢ ENNReal.toReal a ≤ ENNReal.toReal b
[PROOFSTEP]
rcases eq_or_ne a ∞ with rfl | ha
[GOAL]
case inl
α : Type u_1
β : Type u_2
b c d : ℝ≥0∞
r p q : ℝ≥0
h : ⊤ ≤ b
ht : b = ⊤ → ⊤ = ⊤
⊢ ENNReal.toReal ⊤ ≤ ENNReal.toReal b
[PROOFSTEP]
exact toReal_nonneg
[GOAL]
case inr
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p q : ℝ≥0
h : a ≤ b
ht : b = ⊤ → a = ⊤
ha : a ≠ ⊤
⊢ ENNReal.toReal a ≤ ENNReal.toReal b
[PROOFSTEP]
exact toReal_mono (mt ht ha) h
[GOAL]
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p q : ℝ≥0
ha : a ≠ ⊤
hb : b ≠ ⊤
⊢ ENNReal.toReal a < ENNReal.toReal b ↔ a < b
[PROOFSTEP]
lift a to ℝ≥0 using ha
[GOAL]
case intro
α : Type u_1
β : Type u_2
b c d : ℝ≥0∞
r p q : ℝ≥0
hb : b ≠ ⊤
a : ℝ≥0
⊢ ENNReal.toReal ↑a < ENNReal.toReal b ↔ ↑a < b
[PROOFSTEP]
lift b to ℝ≥0 using hb
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
c d : ℝ≥0∞
r p q a b : ℝ≥0
⊢ ENNReal.toReal ↑a < ENNReal.toReal ↑b ↔ ↑a < ↑b
[PROOFSTEP]
norm_cast
[GOAL]
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p q : ℝ≥0
hle : a ≤ b + c
hb : b = ⊤ → a = ⊤
hc : c = ⊤ → a = ⊤
⊢ ENNReal.toReal a ≤ ENNReal.toReal b + ENNReal.toReal c
[PROOFSTEP]
refine le_trans (toReal_mono' hle ?_) toReal_add_le
[GOAL]
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p q : ℝ≥0
hle : a ≤ b + c
hb : b = ⊤ → a = ⊤
hc : c = ⊤ → a = ⊤
⊢ b + c = ⊤ → a = ⊤
[PROOFSTEP]
simpa only [add_eq_top, or_imp] using And.intro hb hc
[GOAL]
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p q : ℝ≥0
ha : a ≠ ⊤
hb : b ≠ ⊤
h : ENNReal.toNNReal a ≤ ENNReal.toNNReal b
⊢ a ≤ b
[PROOFSTEP]
rwa [← coe_toNNReal ha, ← coe_toNNReal hb, coe_le_coe]
[GOAL]
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p q : ℝ≥0
hb : b ≠ ⊤
h : a < b
⊢ ENNReal.toNNReal a < ENNReal.toNNReal b
[PROOFSTEP]
simpa [← ENNReal.coe_lt_coe, hb, h.ne_top]
[GOAL]
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p q : ℝ≥0
ha : a ≠ ⊤
hb : b ≠ ⊤
h : ENNReal.toNNReal a < ENNReal.toNNReal b
⊢ a < b
[PROOFSTEP]
rwa [← coe_toNNReal ha, ← coe_toNNReal hb, coe_lt_coe]
[GOAL]
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p q : ℝ≥0
hr : a ≠ ⊤
hp : b ≠ ⊤
h : a ≤ b
⊢ ENNReal.toReal (max a b) = max (ENNReal.toReal a) (ENNReal.toReal b)
[PROOFSTEP]
simp only [h, (ENNReal.toReal_le_toReal hr hp).2 h, max_eq_right]
[GOAL]
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p q : ℝ≥0
hr : a ≠ ⊤
hp : b ≠ ⊤
h : b ≤ a
⊢ ENNReal.toReal (max a b) = max (ENNReal.toReal a) (ENNReal.toReal b)
[PROOFSTEP]
simp only [h, (ENNReal.toReal_le_toReal hp hr).2 h, max_eq_left]
[GOAL]
α : Type u_1
β : Type u_2
a✝ b✝ c d : ℝ≥0∞
r p q : ℝ≥0
a b : ℝ≥0∞
hr : a ≠ ⊤
hp : b ≠ ⊤
h : a ≤ b
⊢ ENNReal.toReal (min a b) = min (ENNReal.toReal a) (ENNReal.toReal b)
[PROOFSTEP]
simp only [h, (ENNReal.toReal_le_toReal hr hp).2 h, min_eq_left]
[GOAL]
α : Type u_1
β : Type u_2
a✝ b✝ c d : ℝ≥0∞
r p q : ℝ≥0
a b : ℝ≥0∞
hr : a ≠ ⊤
hp : b ≠ ⊤
h : b ≤ a
⊢ ENNReal.toReal (min a b) = min (ENNReal.toReal a) (ENNReal.toReal b)
[PROOFSTEP]
simp only [h, (ENNReal.toReal_le_toReal hp hr).2 h, min_eq_right]
[GOAL]
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p q : ℝ≥0
⊢ 0 < ENNReal.toNNReal a ↔ 0 < a ∧ a < ⊤
[PROOFSTEP]
induction a using recTopCoe
[GOAL]
case top
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p q : ℝ≥0
⊢ 0 < ENNReal.toNNReal ⊤ ↔ 0 < ⊤ ∧ ⊤ < ⊤
[PROOFSTEP]
simp
[GOAL]
case coe
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p q x✝ : ℝ≥0
⊢ 0 < ENNReal.toNNReal ↑x✝ ↔ 0 < ↑x✝ ∧ ↑x✝ < ⊤
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p✝ q✝ : ℝ≥0
p q : ℝ
h : p ≤ q
⊢ ENNReal.ofReal p ≤ ENNReal.ofReal q
[PROOFSTEP]
simp [ENNReal.ofReal, Real.toNNReal_le_toNNReal h]
[GOAL]
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p✝ q✝ : ℝ≥0
p q : ℝ
h : 0 ≤ q
⊢ ENNReal.ofReal p ≤ ENNReal.ofReal q ↔ p ≤ q
[PROOFSTEP]
rw [ENNReal.ofReal, ENNReal.ofReal, coe_le_coe, Real.toNNReal_le_toNNReal_iff h]
[GOAL]
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p✝ q✝ : ℝ≥0
p q : ℝ
hp : 0 ≤ p
hq : 0 ≤ q
⊢ ENNReal.ofReal p = ENNReal.ofReal q ↔ p = q
[PROOFSTEP]
rw [ENNReal.ofReal, ENNReal.ofReal, coe_eq_coe, Real.toNNReal_eq_toNNReal_iff hp hq]
[GOAL]
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p✝ q✝ : ℝ≥0
p q : ℝ
h : 0 < q
⊢ ENNReal.ofReal p < ENNReal.ofReal q ↔ p < q
[PROOFSTEP]
rw [ENNReal.ofReal, ENNReal.ofReal, coe_lt_coe, Real.toNNReal_lt_toNNReal_iff h]
[GOAL]
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p✝ q✝ : ℝ≥0
p q : ℝ
hp : 0 ≤ p
⊢ ENNReal.ofReal p < ENNReal.ofReal q ↔ p < q
[PROOFSTEP]
rw [ENNReal.ofReal, ENNReal.ofReal, coe_lt_coe, Real.toNNReal_lt_toNNReal_iff_of_nonneg hp]
[GOAL]
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p✝ q : ℝ≥0
p : ℝ
⊢ 0 < ENNReal.ofReal p ↔ 0 < p
[PROOFSTEP]
simp [ENNReal.ofReal]
[GOAL]
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p✝ q : ℝ≥0
p : ℝ
⊢ ENNReal.ofReal p = 0 ↔ p ≤ 0
[PROOFSTEP]
simp [ENNReal.ofReal]
[GOAL]
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p✝ q✝ : ℝ≥0
p q : ℝ
hq : 0 ≤ q
⊢ ENNReal.ofReal (p - q) = ENNReal.ofReal p - ENNReal.ofReal q
[PROOFSTEP]
obtain h | h := le_total p q
[GOAL]
case inl
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p✝ q✝ : ℝ≥0
p q : ℝ
hq : 0 ≤ q
h : p ≤ q
⊢ ENNReal.ofReal (p - q) = ENNReal.ofReal p - ENNReal.ofReal q
[PROOFSTEP]
rw [ofReal_of_nonpos (sub_nonpos_of_le h), tsub_eq_zero_of_le (ofReal_le_ofReal h)]
[GOAL]
case inr
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p✝ q✝ : ℝ≥0
p q : ℝ
hq : 0 ≤ q
h : q ≤ p
⊢ ENNReal.ofReal (p - q) = ENNReal.ofReal p - ENNReal.ofReal q
[PROOFSTEP]
refine' ENNReal.eq_sub_of_add_eq ofReal_ne_top _
[GOAL]
case inr
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p✝ q✝ : ℝ≥0
p q : ℝ
hq : 0 ≤ q
h : q ≤ p
⊢ ENNReal.ofReal (p - q) + ENNReal.ofReal q = ENNReal.ofReal p
[PROOFSTEP]
rw [← ofReal_add (sub_nonneg_of_le h) hq, sub_add_cancel]
[GOAL]
α : Type u_1
β : Type u_2
a✝ b✝ c d : ℝ≥0∞
r p q : ℝ≥0
a : ℝ
b : ℝ≥0∞
hb : b ≠ ⊤
⊢ ENNReal.ofReal a ≤ b ↔ a ≤ ENNReal.toReal b
[PROOFSTEP]
lift b to ℝ≥0 using hb
[GOAL]
case intro
α : Type u_1
β : Type u_2
a✝ b✝ c d : ℝ≥0∞
r p q : ℝ≥0
a : ℝ
b : ℝ≥0
⊢ ENNReal.ofReal a ≤ ↑b ↔ a ≤ ENNReal.toReal ↑b
[PROOFSTEP]
simpa [ENNReal.ofReal, ENNReal.toReal] using Real.toNNReal_le_iff_le_coe
[GOAL]
α : Type u_1
β : Type u_2
a✝ b✝ c d : ℝ≥0∞
r p q : ℝ≥0
a : ℝ
b : ℝ≥0∞
ha : 0 ≤ a
hb : b ≠ ⊤
⊢ ENNReal.ofReal a < b ↔ a < ENNReal.toReal b
[PROOFSTEP]
lift b to ℝ≥0 using hb
[GOAL]
case intro
α : Type u_1
β : Type u_2
a✝ b✝ c d : ℝ≥0∞
r p q : ℝ≥0
a : ℝ
ha : 0 ≤ a
b : ℝ≥0
⊢ ENNReal.ofReal a < ↑b ↔ a < ENNReal.toReal ↑b
[PROOFSTEP]
simpa [ENNReal.ofReal, ENNReal.toReal] using Real.toNNReal_lt_iff_lt_coe ha
[GOAL]
α : Type u_1
β : Type u_2
a✝ b✝ c d : ℝ≥0∞
r p q : ℝ≥0
a : ℝ≥0∞
b : ℝ
ha : a ≠ ⊤
hb : 0 ≤ b
⊢ a ≤ ENNReal.ofReal b ↔ ENNReal.toReal a ≤ b
[PROOFSTEP]
lift a to ℝ≥0 using ha
[GOAL]
case intro
α : Type u_1
β : Type u_2
a✝ b✝ c d : ℝ≥0∞
r p q : ℝ≥0
b : ℝ
hb : 0 ≤ b
a : ℝ≥0
⊢ ↑a ≤ ENNReal.ofReal b ↔ ENNReal.toReal ↑a ≤ b
[PROOFSTEP]
simpa [ENNReal.ofReal, ENNReal.toReal] using Real.le_toNNReal_iff_coe_le hb
[GOAL]
α : Type u_1
β : Type u_2
a✝ b✝ c d : ℝ≥0∞
r p q : ℝ≥0
a : ℝ≥0∞
b : ℝ
ha : a ≠ ⊤
⊢ a < ENNReal.ofReal b ↔ ENNReal.toReal a < b
[PROOFSTEP]
lift a to ℝ≥0 using ha
[GOAL]
case intro
α : Type u_1
β : Type u_2
a✝ b✝ c d : ℝ≥0∞
r p q : ℝ≥0
b : ℝ
a : ℝ≥0
⊢ ↑a < ENNReal.ofReal b ↔ ENNReal.toReal ↑a < b
[PROOFSTEP]
simpa [ENNReal.ofReal, ENNReal.toReal] using Real.lt_toNNReal_iff_coe_lt
[GOAL]
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p✝ q✝ : ℝ≥0
p q : ℝ
hp : 0 ≤ p
⊢ ENNReal.ofReal (p * q) = ENNReal.ofReal p * ENNReal.ofReal q
[PROOFSTEP]
simp only [ENNReal.ofReal, ← coe_mul, Real.toNNReal_mul hp]
[GOAL]
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p✝ q✝ : ℝ≥0
p q : ℝ
hq : 0 ≤ q
⊢ ENNReal.ofReal (p * q) = ENNReal.ofReal p * ENNReal.ofReal q
[PROOFSTEP]
rw [mul_comm, ofReal_mul hq, mul_comm]
[GOAL]
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p✝ q : ℝ≥0
p : ℝ
hp : 0 ≤ p
n : ℕ
⊢ ENNReal.ofReal (p ^ n) = ENNReal.ofReal p ^ n
[PROOFSTEP]
rw [ofReal_eq_coe_nnreal hp, ← coe_pow, ← ofReal_coe_nnreal, NNReal.coe_pow, NNReal.coe_mk]
[GOAL]
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p q : ℝ≥0
x : ℝ
n : ℕ
⊢ ENNReal.ofReal (n • x) = n • ENNReal.ofReal x
[PROOFSTEP]
simp only [nsmul_eq_mul, ← ofReal_coe_nat n, ← ofReal_mul n.cast_nonneg]
[GOAL]
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p q : ℝ≥0
x : ℝ
hx : 0 < x
⊢ (ENNReal.ofReal x)⁻¹ = ENNReal.ofReal x⁻¹
[PROOFSTEP]
rw [ENNReal.ofReal, ENNReal.ofReal, ← @coe_inv (Real.toNNReal x) (by simp [hx]), coe_eq_coe, ← Real.toNNReal_inv]
[GOAL]
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p q : ℝ≥0
x : ℝ
hx : 0 < x
⊢ Real.toNNReal x ≠ 0
[PROOFSTEP]
simp [hx]
[GOAL]
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p q : ℝ≥0
x y : ℝ
hy : 0 < y
⊢ ENNReal.ofReal (x / y) = ENNReal.ofReal x / ENNReal.ofReal y
[PROOFSTEP]
rw [div_eq_mul_inv, div_eq_mul_inv, ofReal_mul' (inv_nonneg.2 hy.le), ofReal_inv_of_pos hy]
[GOAL]
α : Type u_1
β : Type u_2
a✝ b c d : ℝ≥0∞
r p q : ℝ≥0
a : ℝ≥0∞
⊢ ENNReal.toNNReal (a * ⊤) = 0
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
a✝ b c d : ℝ≥0∞
r p q : ℝ≥0
a : ℝ≥0∞
⊢ ENNReal.toNNReal (⊤ * a) = 0
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
a✝ b✝ c d : ℝ≥0∞
r p q a : ℝ≥0
b : ℝ≥0∞
⊢ ENNReal.toNNReal (a • b) = a * ENNReal.toNNReal b
[PROOFSTEP]
change ((a : ℝ≥0∞) * b).toNNReal = a * b.toNNReal
[GOAL]
α : Type u_1
β : Type u_2
a✝ b✝ c d : ℝ≥0∞
r p q a : ℝ≥0
b : ℝ≥0∞
⊢ ENNReal.toNNReal (↑a * b) = a * ENNReal.toNNReal b
[PROOFSTEP]
simp only [ENNReal.toNNReal_mul, ENNReal.toNNReal_coe]
[GOAL]
α : Type u_1
β : Type u_2
a✝ b c d : ℝ≥0∞
r p q : ℝ≥0
a : ℝ≥0∞
n : ℕ
⊢ ENNReal.toReal (n • a) = n • ENNReal.toReal a
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
a✝ b c✝ d : ℝ≥0∞
r p q : ℝ≥0
c : ℝ
a : ℝ≥0∞
h : 0 ≤ c
⊢ ENNReal.toReal (ENNReal.ofReal c * a) = c * ENNReal.toReal a
[PROOFSTEP]
rw [ENNReal.toReal_mul, ENNReal.toReal_ofReal h]
[GOAL]
α : Type u_1
β : Type u_2
a✝ b c d : ℝ≥0∞
r p q : ℝ≥0
a : ℝ≥0∞
⊢ ENNReal.toReal (a * ⊤) = 0
[PROOFSTEP]
rw [toReal_mul, top_toReal, mul_zero]
[GOAL]
α : Type u_1
β : Type u_2
a✝ b c d : ℝ≥0∞
r p q : ℝ≥0
a : ℝ≥0∞
⊢ ENNReal.toReal (⊤ * a) = 0
[PROOFSTEP]
rw [mul_comm]
[GOAL]
α : Type u_1
β : Type u_2
a✝ b c d : ℝ≥0∞
r p q : ℝ≥0
a : ℝ≥0∞
⊢ ENNReal.toReal (a * ⊤) = 0
[PROOFSTEP]
exact toReal_mul_top _
[GOAL]
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p q : ℝ≥0
ha : a ≠ ⊤
hb : b ≠ ⊤
⊢ ENNReal.toReal a = ENNReal.toReal b ↔ a = b
[PROOFSTEP]
lift a to ℝ≥0 using ha
[GOAL]
case intro
α : Type u_1
β : Type u_2
b c d : ℝ≥0∞
r p q : ℝ≥0
hb : b ≠ ⊤
a : ℝ≥0
⊢ ENNReal.toReal ↑a = ENNReal.toReal b ↔ ↑a = b
[PROOFSTEP]
lift b to ℝ≥0 using hb
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
c d : ℝ≥0∞
r p q a b : ℝ≥0
⊢ ENNReal.toReal ↑a = ENNReal.toReal ↑b ↔ ↑a = ↑b
[PROOFSTEP]
simp only [coe_eq_coe, NNReal.coe_eq, coe_toReal]
[GOAL]
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r✝ p q r : ℝ≥0
s : ℝ≥0∞
⊢ ENNReal.toReal (r • s) = r • ENNReal.toReal s
[PROOFSTEP]
rw [ENNReal.smul_def, smul_eq_mul, toReal_mul, coe_toReal]
[GOAL]
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r✝ p q r : ℝ≥0
s : ℝ≥0∞
⊢ ↑r * ENNReal.toReal s = r • ENNReal.toReal s
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p✝ q : ℝ≥0
p : ℝ≥0∞
⊢ p = 0 ∨ p = ⊤ ∨ 0 < ENNReal.toReal p
[PROOFSTEP]
simpa only [or_iff_not_imp_left] using toReal_pos
[GOAL]
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p✝ q✝ : ℝ≥0
p q : ℝ≥0∞
hpq : p ≤ q
⊢ p = 0 ∧ q = 0 ∨
    p = 0 ∧ q = ⊤ ∨
      p = 0 ∧ 0 < ENNReal.toReal q ∨
        p = ⊤ ∧ q = ⊤ ∨
          0 < ENNReal.toReal p ∧ q = ⊤ ∨
            0 < ENNReal.toReal p ∧ 0 < ENNReal.toReal q ∧ ENNReal.toReal p ≤ ENNReal.toReal q
[PROOFSTEP]
rcases eq_or_lt_of_le (bot_le : 0 ≤ p) with ((rfl : 0 = p) | (hp : 0 < p))
[GOAL]
case inl
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p q✝ : ℝ≥0
q : ℝ≥0∞
hpq : 0 ≤ q
⊢ 0 = 0 ∧ q = 0 ∨
    0 = 0 ∧ q = ⊤ ∨
      0 = 0 ∧ 0 < ENNReal.toReal q ∨
        0 = ⊤ ∧ q = ⊤ ∨
          0 < ENNReal.toReal 0 ∧ q = ⊤ ∨
            0 < ENNReal.toReal 0 ∧ 0 < ENNReal.toReal q ∧ ENNReal.toReal 0 ≤ ENNReal.toReal q
[PROOFSTEP]
simpa using q.trichotomy
[GOAL]
case inr
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p✝ q✝ : ℝ≥0
p q : ℝ≥0∞
hpq : p ≤ q
hp : 0 < p
⊢ p = 0 ∧ q = 0 ∨
    p = 0 ∧ q = ⊤ ∨
      p = 0 ∧ 0 < ENNReal.toReal q ∨
        p = ⊤ ∧ q = ⊤ ∨
          0 < ENNReal.toReal p ∧ q = ⊤ ∨
            0 < ENNReal.toReal p ∧ 0 < ENNReal.toReal q ∧ ENNReal.toReal p ≤ ENNReal.toReal q
[PROOFSTEP]
rcases eq_or_lt_of_le (le_top : q ≤ ∞) with (rfl | hq)
[GOAL]
case inr.inl
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p✝ q : ℝ≥0
p : ℝ≥0∞
hp : 0 < p
hpq : p ≤ ⊤
⊢ p = 0 ∧ ⊤ = 0 ∨
    p = 0 ∧ ⊤ = ⊤ ∨
      p = 0 ∧ 0 < ENNReal.toReal ⊤ ∨
        p = ⊤ ∧ ⊤ = ⊤ ∨
          0 < ENNReal.toReal p ∧ ⊤ = ⊤ ∨
            0 < ENNReal.toReal p ∧ 0 < ENNReal.toReal ⊤ ∧ ENNReal.toReal p ≤ ENNReal.toReal ⊤
[PROOFSTEP]
simpa using p.trichotomy
[GOAL]
case inr.inr
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p✝ q✝ : ℝ≥0
p q : ℝ≥0∞
hpq : p ≤ q
hp : 0 < p
hq : q < ⊤
⊢ p = 0 ∧ q = 0 ∨
    p = 0 ∧ q = ⊤ ∨
      p = 0 ∧ 0 < ENNReal.toReal q ∨
        p = ⊤ ∧ q = ⊤ ∨
          0 < ENNReal.toReal p ∧ q = ⊤ ∨
            0 < ENNReal.toReal p ∧ 0 < ENNReal.toReal q ∧ ENNReal.toReal p ≤ ENNReal.toReal q
[PROOFSTEP]
repeat' right
[GOAL]
case inr.inr
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p✝ q✝ : ℝ≥0
p q : ℝ≥0∞
hpq : p ≤ q
hp : 0 < p
hq : q < ⊤
⊢ p = 0 ∧ q = 0 ∨
    p = 0 ∧ q = ⊤ ∨
      p = 0 ∧ 0 < ENNReal.toReal q ∨
        p = ⊤ ∧ q = ⊤ ∨
          0 < ENNReal.toReal p ∧ q = ⊤ ∨
            0 < ENNReal.toReal p ∧ 0 < ENNReal.toReal q ∧ ENNReal.toReal p ≤ ENNReal.toReal q
[PROOFSTEP]
right
[GOAL]
case inr.inr.h
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p✝ q✝ : ℝ≥0
p q : ℝ≥0∞
hpq : p ≤ q
hp : 0 < p
hq : q < ⊤
⊢ p = 0 ∧ q = ⊤ ∨
    p = 0 ∧ 0 < ENNReal.toReal q ∨
      p = ⊤ ∧ q = ⊤ ∨
        0 < ENNReal.toReal p ∧ q = ⊤ ∨ 0 < ENNReal.toReal p ∧ 0 < ENNReal.toReal q ∧ ENNReal.toReal p ≤ ENNReal.toReal q
[PROOFSTEP]
right
[GOAL]
case inr.inr.h.h
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p✝ q✝ : ℝ≥0
p q : ℝ≥0∞
hpq : p ≤ q
hp : 0 < p
hq : q < ⊤
⊢ p = 0 ∧ 0 < ENNReal.toReal q ∨
    p = ⊤ ∧ q = ⊤ ∨
      0 < ENNReal.toReal p ∧ q = ⊤ ∨ 0 < ENNReal.toReal p ∧ 0 < ENNReal.toReal q ∧ ENNReal.toReal p ≤ ENNReal.toReal q
[PROOFSTEP]
right
[GOAL]
case inr.inr.h.h.h
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p✝ q✝ : ℝ≥0
p q : ℝ≥0∞
hpq : p ≤ q
hp : 0 < p
hq : q < ⊤
⊢ p = ⊤ ∧ q = ⊤ ∨
    0 < ENNReal.toReal p ∧ q = ⊤ ∨ 0 < ENNReal.toReal p ∧ 0 < ENNReal.toReal q ∧ ENNReal.toReal p ≤ ENNReal.toReal q
[PROOFSTEP]
right
[GOAL]
case inr.inr.h.h.h.h
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p✝ q✝ : ℝ≥0
p q : ℝ≥0∞
hpq : p ≤ q
hp : 0 < p
hq : q < ⊤
⊢ 0 < ENNReal.toReal p ∧ q = ⊤ ∨ 0 < ENNReal.toReal p ∧ 0 < ENNReal.toReal q ∧ ENNReal.toReal p ≤ ENNReal.toReal q
[PROOFSTEP]
right
[GOAL]
case inr.inr.h.h.h.h.h
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p✝ q✝ : ℝ≥0
p q : ℝ≥0∞
hpq : p ≤ q
hp : 0 < p
hq : q < ⊤
⊢ 0 < ENNReal.toReal p ∧ 0 < ENNReal.toReal q ∧ ENNReal.toReal p ≤ ENNReal.toReal q
[PROOFSTEP]
right
[GOAL]
case inr.inr.h.h.h.h.h
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p✝ q✝ : ℝ≥0
p q : ℝ≥0∞
hpq : p ≤ q
hp : 0 < p
hq : q < ⊤
⊢ 0 < ENNReal.toReal p ∧ 0 < ENNReal.toReal q ∧ ENNReal.toReal p ≤ ENNReal.toReal q
[PROOFSTEP]
have hq' : 0 < q := lt_of_lt_of_le hp hpq
[GOAL]
case inr.inr.h.h.h.h.h
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p✝ q✝ : ℝ≥0
p q : ℝ≥0∞
hpq : p ≤ q
hp : 0 < p
hq : q < ⊤
hq' : 0 < q
⊢ 0 < ENNReal.toReal p ∧ 0 < ENNReal.toReal q ∧ ENNReal.toReal p ≤ ENNReal.toReal q
[PROOFSTEP]
have hp' : p < ∞ := lt_of_le_of_lt hpq hq
[GOAL]
case inr.inr.h.h.h.h.h
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p✝ q✝ : ℝ≥0
p q : ℝ≥0∞
hpq : p ≤ q
hp : 0 < p
hq : q < ⊤
hq' : 0 < q
hp' : p < ⊤
⊢ 0 < ENNReal.toReal p ∧ 0 < ENNReal.toReal q ∧ ENNReal.toReal p ≤ ENNReal.toReal q
[PROOFSTEP]
simp [ENNReal.toReal_le_toReal hp'.ne hq.ne, ENNReal.toReal_pos_iff, hpq, hp, hp', hq', hq]
[GOAL]
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p✝ q : ℝ≥0
p : ℝ≥0∞
inst✝ : Fact (1 ≤ p)
⊢ p = ⊤ ∨ 0 < ENNReal.toReal p ∧ 1 ≤ ENNReal.toReal p
[PROOFSTEP]
simpa using ENNReal.trichotomy₂ (Fact.out : 1 ≤ p)
[GOAL]
α : Type u_1
β : Type u_2
a✝ b c d : ℝ≥0∞
r p q : ℝ≥0
a : ℝ≥0∞
⊢ ENNReal.toNNReal a⁻¹ = (ENNReal.toNNReal a)⁻¹
[PROOFSTEP]
induction' a using recTopCoe with a
[GOAL]
case top
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p q : ℝ≥0
⊢ ENNReal.toNNReal ⊤⁻¹ = (ENNReal.toNNReal ⊤)⁻¹
[PROOFSTEP]
simp
[GOAL]
case coe
α : Type u_1
β : Type u_2
a✝ b c d : ℝ≥0∞
r p q a : ℝ≥0
⊢ ENNReal.toNNReal (↑a)⁻¹ = (ENNReal.toNNReal ↑a)⁻¹
[PROOFSTEP]
rcases eq_or_ne a 0 with (rfl | ha)
[GOAL]
case coe.inl
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p q : ℝ≥0
⊢ ENNReal.toNNReal (↑0)⁻¹ = (ENNReal.toNNReal ↑0)⁻¹
[PROOFSTEP]
simp
[GOAL]
case coe.inr
α : Type u_1
β : Type u_2
a✝ b c d : ℝ≥0∞
r p q a : ℝ≥0
ha : a ≠ 0
⊢ ENNReal.toNNReal (↑a)⁻¹ = (ENNReal.toNNReal ↑a)⁻¹
[PROOFSTEP]
rw [← coe_inv ha, toNNReal_coe, toNNReal_coe]
[GOAL]
α : Type u_1
β : Type u_2
a✝ b✝ c d : ℝ≥0∞
r p q : ℝ≥0
a b : ℝ≥0∞
⊢ ENNReal.toNNReal (a / b) = ENNReal.toNNReal a / ENNReal.toNNReal b
[PROOFSTEP]
rw [div_eq_mul_inv, toNNReal_mul, toNNReal_inv, div_eq_mul_inv]
[GOAL]
α : Type u_1
β : Type u_2
a✝ b c d : ℝ≥0∞
r p q : ℝ≥0
a : ℝ≥0∞
⊢ ENNReal.toReal a⁻¹ = (ENNReal.toReal a)⁻¹
[PROOFSTEP]
simp only [ENNReal.toReal, toNNReal_inv, NNReal.coe_inv]
[GOAL]
α : Type u_1
β : Type u_2
a✝ b✝ c d : ℝ≥0∞
r p q : ℝ≥0
a b : ℝ≥0∞
⊢ ENNReal.toReal (a / b) = ENNReal.toReal a / ENNReal.toReal b
[PROOFSTEP]
rw [div_eq_mul_inv, toReal_mul, toReal_inv, div_eq_mul_inv]
[GOAL]
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p q : ℝ≥0
s : Finset α
f : α → ℝ
hf : ∀ (i : α), i ∈ s → 0 ≤ f i
⊢ ENNReal.ofReal (∏ i in s, f i) = ∏ i in s, ENNReal.ofReal (f i)
[PROOFSTEP]
simp_rw [ENNReal.ofReal, ← coe_finset_prod, coe_eq_coe]
[GOAL]
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p q : ℝ≥0
s : Finset α
f : α → ℝ
hf : ∀ (i : α), i ∈ s → 0 ≤ f i
⊢ Real.toNNReal (∏ i in s, f i) = ∏ a in s, Real.toNNReal (f a)
[PROOFSTEP]
exact Real.toNNReal_prod_of_nonneg hf
[GOAL]
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p q : ℝ≥0
ι : Sort u_3
f g : ι → ℝ≥0∞
hf : ∀ (i : ι), f i ≠ ⊤
⊢ ENNReal.toNNReal (iInf f) = ⨅ (i : ι), ENNReal.toNNReal (f i)
[PROOFSTEP]
cases isEmpty_or_nonempty ι
[GOAL]
case inl
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p q : ℝ≥0
ι : Sort u_3
f g : ι → ℝ≥0∞
hf : ∀ (i : ι), f i ≠ ⊤
h✝ : IsEmpty ι
⊢ ENNReal.toNNReal (iInf f) = ⨅ (i : ι), ENNReal.toNNReal (f i)
[PROOFSTEP]
rw [iInf_of_empty, top_toNNReal, NNReal.iInf_empty]
[GOAL]
case inr
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p q : ℝ≥0
ι : Sort u_3
f g : ι → ℝ≥0∞
hf : ∀ (i : ι), f i ≠ ⊤
h✝ : Nonempty ι
⊢ ENNReal.toNNReal (iInf f) = ⨅ (i : ι), ENNReal.toNNReal (f i)
[PROOFSTEP]
lift f to ι → ℝ≥0 using hf
[GOAL]
case inr.intro
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p q : ℝ≥0
ι : Sort u_3
g : ι → ℝ≥0∞
h✝ : Nonempty ι
f : ι → ℝ≥0
⊢ ENNReal.toNNReal (⨅ (i : ι), ↑(f i)) = ⨅ (i : ι), ENNReal.toNNReal ((fun i => ↑(f i)) i)
[PROOFSTEP]
simp_rw [← coe_iInf, toNNReal_coe]
[GOAL]
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p q : ℝ≥0
ι : Sort u_3
f g : ι → ℝ≥0∞
s : Set ℝ≥0∞
hs : ∀ (r : ℝ≥0∞), r ∈ s → r ≠ ⊤
⊢ ENNReal.toNNReal (sInf s) = sInf (ENNReal.toNNReal '' s)
[PROOFSTEP]
have hf : ∀ i, ((↑) : s → ℝ≥0∞) i ≠ ∞ := fun ⟨r, rs⟩ => hs r rs
[GOAL]
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p q : ℝ≥0
ι : Sort u_3
f g : ι → ℝ≥0∞
s : Set ℝ≥0∞
hs : ∀ (r : ℝ≥0∞), r ∈ s → r ≠ ⊤
hf : ∀ (i : { x // x ∈ s }), ↑i ≠ ⊤
⊢ ENNReal.toNNReal (sInf s) = sInf (ENNReal.toNNReal '' s)
[PROOFSTEP]
simpa only [← sInf_range, ← image_eq_range, Subtype.range_coe_subtype] using (toNNReal_iInf hf)
[GOAL]
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p q : ℝ≥0
ι : Sort u_3
f g : ι → ℝ≥0∞
hf : ∀ (i : ι), f i ≠ ⊤
⊢ ENNReal.toNNReal (iSup f) = ⨆ (i : ι), ENNReal.toNNReal (f i)
[PROOFSTEP]
lift f to ι → ℝ≥0 using hf
[GOAL]
case intro
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p q : ℝ≥0
ι : Sort u_3
g : ι → ℝ≥0∞
f : ι → ℝ≥0
⊢ ENNReal.toNNReal (⨆ (i : ι), ↑(f i)) = ⨆ (i : ι), ENNReal.toNNReal ((fun i => ↑(f i)) i)
[PROOFSTEP]
simp_rw [toNNReal_coe]
[GOAL]
case intro
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p q : ℝ≥0
ι : Sort u_3
g : ι → ℝ≥0∞
f : ι → ℝ≥0
⊢ ENNReal.toNNReal (⨆ (i : ι), ↑(f i)) = ⨆ (i : ι), f i
[PROOFSTEP]
by_cases h : BddAbove (range f)
[GOAL]
case pos
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p q : ℝ≥0
ι : Sort u_3
g : ι → ℝ≥0∞
f : ι → ℝ≥0
h : BddAbove (range f)
⊢ ENNReal.toNNReal (⨆ (i : ι), ↑(f i)) = ⨆ (i : ι), f i
[PROOFSTEP]
rw [← coe_iSup h, toNNReal_coe]
[GOAL]
case neg
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p q : ℝ≥0
ι : Sort u_3
g : ι → ℝ≥0∞
f : ι → ℝ≥0
h : ¬BddAbove (range f)
⊢ ENNReal.toNNReal (⨆ (i : ι), ↑(f i)) = ⨆ (i : ι), f i
[PROOFSTEP]
erw [NNReal.iSup_of_not_bddAbove h, (WithTop.iSup_coe_eq_top f).mpr h, top_toNNReal]
[GOAL]
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p q : ℝ≥0
ι : Sort u_3
f g : ι → ℝ≥0∞
s : Set ℝ≥0∞
hs : ∀ (r : ℝ≥0∞), r ∈ s → r ≠ ⊤
⊢ ENNReal.toNNReal (sSup s) = sSup (ENNReal.toNNReal '' s)
[PROOFSTEP]
have hf : ∀ i, ((↑) : s → ℝ≥0∞) i ≠ ∞ := fun ⟨r, rs⟩ => hs r rs
[GOAL]
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p q : ℝ≥0
ι : Sort u_3
f g : ι → ℝ≥0∞
s : Set ℝ≥0∞
hs : ∀ (r : ℝ≥0∞), r ∈ s → r ≠ ⊤
hf : ∀ (i : { x // x ∈ s }), ↑i ≠ ⊤
⊢ ENNReal.toNNReal (sSup s) = sSup (ENNReal.toNNReal '' s)
[PROOFSTEP]
simpa only [← sSup_range, ← image_eq_range, Subtype.range_coe_subtype] using (toNNReal_iSup hf)
[GOAL]
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p q : ℝ≥0
ι : Sort u_3
f g : ι → ℝ≥0∞
hf : ∀ (i : ι), f i ≠ ⊤
⊢ ENNReal.toReal (iInf f) = ⨅ (i : ι), ENNReal.toReal (f i)
[PROOFSTEP]
simp only [ENNReal.toReal, toNNReal_iInf hf, NNReal.coe_iInf]
[GOAL]
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p q : ℝ≥0
ι : Sort u_3
f g : ι → ℝ≥0∞
s : Set ℝ≥0∞
hf : ∀ (r : ℝ≥0∞), r ∈ s → r ≠ ⊤
⊢ ENNReal.toReal (sInf s) = sInf (ENNReal.toReal '' s)
[PROOFSTEP]
simp only [ENNReal.toReal, toNNReal_sInf s hf, NNReal.coe_sInf, Set.image_image]
[GOAL]
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p q : ℝ≥0
ι : Sort u_3
f g : ι → ℝ≥0∞
hf : ∀ (i : ι), f i ≠ ⊤
⊢ ENNReal.toReal (iSup f) = ⨆ (i : ι), ENNReal.toReal (f i)
[PROOFSTEP]
simp only [ENNReal.toReal, toNNReal_iSup hf, NNReal.coe_iSup]
[GOAL]
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p q : ℝ≥0
ι : Sort u_3
f g : ι → ℝ≥0∞
s : Set ℝ≥0∞
hf : ∀ (r : ℝ≥0∞), r ∈ s → r ≠ ⊤
⊢ ENNReal.toReal (sSup s) = sSup (ENNReal.toReal '' s)
[PROOFSTEP]
simp only [ENNReal.toReal, toNNReal_sSup s hf, NNReal.coe_sSup, Set.image_image]
[GOAL]
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p q : ℝ≥0
ι : Sort u_3
f g : ι → ℝ≥0∞
⊢ a - ⨅ (i : ι), f i = ⨆ (i : ι), a - f i
[PROOFSTEP]
refine' eq_of_forall_ge_iff fun c => _
[GOAL]
α : Type u_1
β : Type u_2
a b c✝ d : ℝ≥0∞
r p q : ℝ≥0
ι : Sort u_3
f g : ι → ℝ≥0∞
c : ℝ≥0∞
⊢ a - ⨅ (i : ι), f i ≤ c ↔ ⨆ (i : ι), a - f i ≤ c
[PROOFSTEP]
rw [tsub_le_iff_right, add_comm, iInf_add]
[GOAL]
α : Type u_1
β : Type u_2
a b c✝ d : ℝ≥0∞
r p q : ℝ≥0
ι : Sort u_3
f g : ι → ℝ≥0∞
c : ℝ≥0∞
⊢ a ≤ ⨅ (i : ι), f i + c ↔ ⨆ (i : ι), a - f i ≤ c
[PROOFSTEP]
simp [tsub_le_iff_right, sub_eq_add_neg, add_comm]
[GOAL]
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p q : ℝ≥0
ι : Sort u_3
f g : ι → ℝ≥0∞
s : Set ℝ≥0∞
⊢ sInf s + a = ⨅ (b : ℝ≥0∞) (_ : b ∈ s), b + a
[PROOFSTEP]
simp [sInf_eq_iInf, iInf_add]
[GOAL]
α : Type u_1
β : Type u_2
a✝ b c d : ℝ≥0∞
r p q : ℝ≥0
ι : Sort u_3
f g : ι → ℝ≥0∞
a : ℝ≥0∞
⊢ a + iInf f = ⨅ (b : ι), a + f b
[PROOFSTEP]
rw [add_comm, iInf_add]
[GOAL]
α : Type u_1
β : Type u_2
a✝ b c d : ℝ≥0∞
r p q : ℝ≥0
ι : Sort u_3
f g : ι → ℝ≥0∞
a : ℝ≥0∞
⊢ ⨅ (i : ι), f i + a = ⨅ (b : ι), a + f b
[PROOFSTEP]
simp [add_comm]
[GOAL]
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p q : ℝ≥0
ι : Sort u_3
f g : ι → ℝ≥0∞
h : ∀ (i j : ι), ∃ k, f k + g k ≤ f i + g j
⊢ ⨅ (a : ι) (a' : ι), f a + g a' = iInf f + iInf g
[PROOFSTEP]
simp_rw [iInf_add, add_iInf]
[GOAL]
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p q : ℝ≥0
ι : Sort u_3
f✝ g : ι → ℝ≥0∞
f : ι → α → ℝ≥0∞
s : Finset α
inst✝ : Nonempty ι
h : ∀ (t : Finset α) (i j : ι), ∃ k, ∀ (a : α), a ∈ t → f k a ≤ f i a ∧ f k a ≤ f j a
⊢ ⨅ (i : ι), ∑ a in s, f i a = ∑ a in s, ⨅ (i : ι), f i a
[PROOFSTEP]
induction' s using Finset.cons_induction_on with a s ha ih
[GOAL]
case h₁
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p q : ℝ≥0
ι : Sort u_3
f✝ g : ι → ℝ≥0∞
f : ι → α → ℝ≥0∞
inst✝ : Nonempty ι
h : ∀ (t : Finset α) (i j : ι), ∃ k, ∀ (a : α), a ∈ t → f k a ≤ f i a ∧ f k a ≤ f j a
⊢ ⨅ (i : ι), ∑ a in ∅, f i a = ∑ a in ∅, ⨅ (i : ι), f i a
[PROOFSTEP]
simp only [Finset.sum_empty, ciInf_const]
[GOAL]
case h₂
α : Type u_1
β : Type u_2
a✝ b c d : ℝ≥0∞
r p q : ℝ≥0
ι : Sort u_3
f✝ g : ι → ℝ≥0∞
f : ι → α → ℝ≥0∞
inst✝ : Nonempty ι
h : ∀ (t : Finset α) (i j : ι), ∃ k, ∀ (a : α), a ∈ t → f k a ≤ f i a ∧ f k a ≤ f j a
a : α
s : Finset α
ha : ¬a ∈ s
ih : ⨅ (i : ι), ∑ a in s, f i a = ∑ a in s, ⨅ (i : ι), f i a
⊢ ⨅ (i : ι), ∑ a in Finset.cons a s ha, f i a = ∑ a in Finset.cons a s ha, ⨅ (i : ι), f i a
[PROOFSTEP]
simp only [Finset.sum_cons, ← ih]
[GOAL]
case h₂
α : Type u_1
β : Type u_2
a✝ b c d : ℝ≥0∞
r p q : ℝ≥0
ι : Sort u_3
f✝ g : ι → ℝ≥0∞
f : ι → α → ℝ≥0∞
inst✝ : Nonempty ι
h : ∀ (t : Finset α) (i j : ι), ∃ k, ∀ (a : α), a ∈ t → f k a ≤ f i a ∧ f k a ≤ f j a
a : α
s : Finset α
ha : ¬a ∈ s
ih : ⨅ (i : ι), ∑ a in s, f i a = ∑ a in s, ⨅ (i : ι), f i a
⊢ ⨅ (i : ι), f i a + ∑ a in s, f i a = (⨅ (i : ι), f i a) + ⨅ (i : ι), ∑ a in s, f i a
[PROOFSTEP]
refine (iInf_add_iInf fun i j => ?_).symm
[GOAL]
case h₂
α : Type u_1
β : Type u_2
a✝ b c d : ℝ≥0∞
r p q : ℝ≥0
ι : Sort u_3
f✝ g : ι → ℝ≥0∞
f : ι → α → ℝ≥0∞
inst✝ : Nonempty ι
h : ∀ (t : Finset α) (i j : ι), ∃ k, ∀ (a : α), a ∈ t → f k a ≤ f i a ∧ f k a ≤ f j a
a : α
s : Finset α
ha : ¬a ∈ s
ih : ⨅ (i : ι), ∑ a in s, f i a = ∑ a in s, ⨅ (i : ι), f i a
i j : ι
⊢ ∃ k, f k a + ∑ a in s, f k a ≤ f i a + ∑ a in s, f j a
[PROOFSTEP]
refine (h (Finset.cons a s ha) i j).imp fun k hk => ?_
[GOAL]
case h₂
α : Type u_1
β : Type u_2
a✝ b c d : ℝ≥0∞
r p q : ℝ≥0
ι : Sort u_3
f✝ g : ι → ℝ≥0∞
f : ι → α → ℝ≥0∞
inst✝ : Nonempty ι
h : ∀ (t : Finset α) (i j : ι), ∃ k, ∀ (a : α), a ∈ t → f k a ≤ f i a ∧ f k a ≤ f j a
a : α
s : Finset α
ha : ¬a ∈ s
ih : ⨅ (i : ι), ∑ a in s, f i a = ∑ a in s, ⨅ (i : ι), f i a
i j k : ι
hk : ∀ (a_1 : α), a_1 ∈ Finset.cons a s ha → f k a_1 ≤ f i a_1 ∧ f k a_1 ≤ f j a_1
⊢ f k a + ∑ a in s, f k a ≤ f i a + ∑ a in s, f j a
[PROOFSTEP]
rw [Finset.forall_mem_cons] at hk 
[GOAL]
case h₂
α : Type u_1
β : Type u_2
a✝ b c d : ℝ≥0∞
r p q : ℝ≥0
ι : Sort u_3
f✝ g : ι → ℝ≥0∞
f : ι → α → ℝ≥0∞
inst✝ : Nonempty ι
h : ∀ (t : Finset α) (i j : ι), ∃ k, ∀ (a : α), a ∈ t → f k a ≤ f i a ∧ f k a ≤ f j a
a : α
s : Finset α
ha : ¬a ∈ s
ih : ⨅ (i : ι), ∑ a in s, f i a = ∑ a in s, ⨅ (i : ι), f i a
i j k : ι
hk : (f k a ≤ f i a ∧ f k a ≤ f j a) ∧ ∀ (x : α), x ∈ s → f k x ≤ f i x ∧ f k x ≤ f j x
⊢ f k a + ∑ a in s, f k a ≤ f i a + ∑ a in s, f j a
[PROOFSTEP]
exact add_le_add hk.1.1 (Finset.sum_le_sum fun a ha => (hk.2 a ha).2)
[GOAL]
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p q : ℝ≥0
ι✝ : Sort u_3
f✝ g : ι✝ → ℝ≥0∞
ι : Sort u_4
inst✝ : Nonempty ι
f : ι → ℝ≥0∞
x : ℝ≥0∞
h : x ≠ ⊤
⊢ iInf f * x = ⨅ (i : ι), f i * x
[PROOFSTEP]
by_cases h0 : x = 0
[GOAL]
case pos
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p q : ℝ≥0
ι✝ : Sort u_3
f✝ g : ι✝ → ℝ≥0∞
ι : Sort u_4
inst✝ : Nonempty ι
f : ι → ℝ≥0∞
x : ℝ≥0∞
h : x ≠ ⊤
h0 : x = 0
⊢ iInf f * x = ⨅ (i : ι), f i * x
[PROOFSTEP]
simp only [h0, mul_zero, iInf_const]
[GOAL]
case neg
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p q : ℝ≥0
ι✝ : Sort u_3
f✝ g : ι✝ → ℝ≥0∞
ι : Sort u_4
inst✝ : Nonempty ι
f : ι → ℝ≥0∞
x : ℝ≥0∞
h : x ≠ ⊤
h0 : ¬x = 0
⊢ iInf f * x = ⨅ (i : ι), f i * x
[PROOFSTEP]
exact iInf_mul_of_ne h0 h
[GOAL]
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p q : ℝ≥0
ι✝ : Sort u_3
f✝ g : ι✝ → ℝ≥0∞
ι : Sort u_4
inst✝ : Nonempty ι
f : ι → ℝ≥0∞
x : ℝ≥0∞
h : x ≠ ⊤
⊢ x * iInf f = ⨅ (i : ι), x * f i
[PROOFSTEP]
simpa only [mul_comm] using iInf_mul h
[GOAL]
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p q : ℝ≥0
ι✝ : Sort u_3
f✝ g : ι✝ → ℝ≥0∞
ι : Sort u_4
f : ι → ℝ≥0∞
x : ℝ≥0∞
h0 : x ≠ 0
h : x ≠ ⊤
⊢ x * iInf f = ⨅ (i : ι), x * f i
[PROOFSTEP]
simpa only [mul_comm] using iInf_mul_of_ne h0 h
[GOAL]
α : Type u_1
β : Type u_2
a b c d : ℝ≥0∞
r p q : ℝ≥0
ι : Sort u_3
⊢ ⨆ (x : ι), 0 = 0
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
s : Set ℝ
t : Set ℝ≥0
u : Set ℝ≥0∞
h : OrdConnected t
⊢ OrdConnected (ENNReal.some '' t)
[PROOFSTEP]
refine' ⟨ball_image_iff.2 fun x hx => ball_image_iff.2 fun y hy z hz => _⟩
[GOAL]
α : Type u_1
β : Type u_2
s : Set ℝ
t : Set ℝ≥0
u : Set ℝ≥0∞
h : OrdConnected t
x : ℝ≥0
hx : x ∈ t
y : ℝ≥0
hy : y ∈ t
z : ℝ≥0∞
hz : z ∈ Icc ↑x ↑y
⊢ z ∈ ENNReal.some '' t
[PROOFSTEP]
rcases ENNReal.le_coe_iff.1 hz.2 with ⟨z, rfl, -⟩
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
s : Set ℝ
t : Set ℝ≥0
u : Set ℝ≥0∞
h : OrdConnected t
x : ℝ≥0
hx : x ∈ t
y : ℝ≥0
hy : y ∈ t
z : ℝ≥0
hz : ↑z ∈ Icc ↑x ↑y
⊢ ↑z ∈ ENNReal.some '' t
[PROOFSTEP]
exact mem_image_of_mem _ (h.out hx hy ⟨ENNReal.coe_le_coe.1 hz.1, ENNReal.coe_le_coe.1 hz.2⟩)
[GOAL]
α : Type u_1
β : Type u_2
s : Set ℝ
t : Set ℝ≥0
u : Set ℝ≥0∞
h : OrdConnected s
⊢ OrdConnected (ENNReal.ofReal '' s)
[PROOFSTEP]
simpa only [image_image] using h.image_real_toNNReal.image_coe_nnreal_ennreal
