α : Type u_1
β : Type ?u.838044
γ : Type ?u.838047
δ : Type ?u.838050
inst✝ : MeasurableSpace α
K : Type ?u.838056
f : α → ℝ≥0∞
hf : Measurable f
a : α
⊢ (⨆ (k : ℕ) (_ : ennrealRatEmbed k ≤ f a), ennrealRatEmbed k) = f a
α : Type u_1
β : Type ?u.838044
γ : Type ?u.838047
δ : Type ?u.838050
inst✝ : MeasurableSpace α
K : Type ?u.838056
f : α → ℝ≥0∞
hf : Measurable f
a : α
⊢ (⨆ (n : ℕ), ↑(eapprox f n) a) = f a
rw [eapprox, iSup_approx_apply ennrealRatEmbed f a hf rfl]
α : Type u_1
β : Type ?u.838044
γ : Type ?u.838047
δ : Type ?u.838050
inst✝ : MeasurableSpace α
K : Type ?u.838056
f : α → ℝ≥0∞
hf : Measurable f
a : α
⊢ ¬f a > ⨆ (k : ℕ) (_ : ennrealRatEmbed k ≤ f a), ennrealRatEmbed k
α : Type u_1
β : Type ?u.838044
γ : Type ?u.838047
δ : Type ?u.838050
inst✝ : MeasurableSpace α
K : Type ?u.838056
f : α → ℝ≥0∞
hf : Measurable f
a : α
⊢ (⨆ (k : ℕ) (_ : ennrealRatEmbed k ≤ f a), ennrealRatEmbed k) = f a
refine' le_antisymm (iSup_le fun i => iSup_le fun hi => hi) (le_of_not_gt _)
α : Type u_1
β : Type ?u.838044
γ : Type ?u.838047
δ : Type ?u.838050
inst✝ : MeasurableSpace α
K : Type ?u.838056
f : α → ℝ≥0∞
hf : Measurable f
a : α
h : f a > ⨆ (k : ℕ) (_ : ennrealRatEmbed k ≤ f a), ennrealRatEmbed k
⊢ False
α : Type u_1
β : Type ?u.838044
γ : Type ?u.838047
δ : Type ?u.838050
inst✝ : MeasurableSpace α
K : Type ?u.838056
f : α → ℝ≥0∞
hf : Measurable f
a : α
⊢ ¬f a > ⨆ (k : ℕ) (_ : ennrealRatEmbed k ≤ f a), ennrealRatEmbed k
intro h
case intro.intro.intro
α : Type u_1
β : Type ?u.838044
γ : Type ?u.838047
δ : Type ?u.838050
inst✝ : MeasurableSpace α
K : Type ?u.838056
f : α → ℝ≥0∞
hf : Measurable f
a : α
h : f a > ⨆ (k : ℕ) (_ : ennrealRatEmbed k ≤ f a), ennrealRatEmbed k
q : ℚ
left✝ : 0 ≤ q
lt_q : (⨆ (k : ℕ) (_ : ennrealRatEmbed k ≤ f a), ennrealRatEmbed k) < ↑(Real.toNNReal ↑q)
q_lt : ↑(Real.toNNReal ↑q) < f a
⊢ False
α : Type u_1
β : Type ?u.838044
γ : Type ?u.838047
δ : Type ?u.838050
inst✝ : MeasurableSpace α
K : Type ?u.838056
f : α → ℝ≥0∞
hf : Measurable f
a : α
h : f a > ⨆ (k : ℕ) (_ : ennrealRatEmbed k ≤ f a), ennrealRatEmbed k
⊢ False
rcases ENNReal.lt_iff_exists_rat_btwn.1 h with ⟨q, _, lt_q, q_lt⟩
case intro.intro.intro
α : Type u_1
β : Type ?u.838044
γ : Type ?u.838047
δ : Type ?u.838050
inst✝ : MeasurableSpace α
K : Type ?u.838056
f : α → ℝ≥0∞
hf : Measurable f
a : α
h : f a > ⨆ (k : ℕ) (_ : ennrealRatEmbed k ≤ f a), ennrealRatEmbed k
q : ℚ
left✝ : 0 ≤ q
lt_q : (⨆ (k : ℕ) (_ : ennrealRatEmbed k ≤ f a), ennrealRatEmbed k) < ↑(Real.toNNReal ↑q)
q_lt : ↑(Real.toNNReal ↑q) < f a
this : ↑(Real.toNNReal ↑q) ≤ ⨆ (k : ℕ) (_ : ennrealRatEmbed k ≤ f a), ennrealRatEmbed k
⊢ False
case intro.intro.intro
α : Type u_1
β : Type ?u.838044
γ : Type ?u.838047
δ : Type ?u.838050
inst✝ : MeasurableSpace α
K : Type ?u.838056
f : α → ℝ≥0∞
hf : Measurable f
a : α
h : f a > ⨆ (k : ℕ) (_ : ennrealRatEmbed k ≤ f a), ennrealRatEmbed k
q : ℚ
left✝ : 0 ≤ q
lt_q : (⨆ (k : ℕ) (_ : ennrealRatEmbed k ≤ f a), ennrealRatEmbed k) < ↑(Real.toNNReal ↑q)
q_lt : ↑(Real.toNNReal ↑q) < f a
⊢ False
have :
  (Real.toNNReal q : ℝ≥0∞) ≤ ⨆ (k : ℕ) (_ : ennrealRatEmbed k ≤ f a), ennrealRatEmbed k := by
  refine' le_iSup_of_le (Encodable.encode q) _
  rw [ennrealRatEmbed_encode q]
  refine' le_iSup_of_le (le_of_lt q_lt) _
  exact le_rfl
no goals
case intro.intro.intro
α : Type u_1
β : Type ?u.838044
γ : Type ?u.838047
δ : Type ?u.838050
inst✝ : MeasurableSpace α
K : Type ?u.838056
f : α → ℝ≥0∞
hf : Measurable f
a : α
h : f a > ⨆ (k : ℕ) (_ : ennrealRatEmbed k ≤ f a), ennrealRatEmbed k
q : ℚ
left✝ : 0 ≤ q
lt_q : (⨆ (k : ℕ) (_ : ennrealRatEmbed k ≤ f a), ennrealRatEmbed k) < ↑(Real.toNNReal ↑q)
q_lt : ↑(Real.toNNReal ↑q) < f a
this : ↑(Real.toNNReal ↑q) ≤ ⨆ (k : ℕ) (_ : ennrealRatEmbed k ≤ f a), ennrealRatEmbed k
⊢ False
exact lt_irrefl _ (lt_of_le_of_lt this lt_q)
α : Type u_1
β : Type ?u.838044
γ : Type ?u.838047
δ : Type ?u.838050
inst✝ : MeasurableSpace α
K : Type ?u.838056
f : α → ℝ≥0∞
hf : Measurable f
a : α
h : f a > ⨆ (k : ℕ) (_ : ennrealRatEmbed k ≤ f a), ennrealRatEmbed k
q : ℚ
left✝ : 0 ≤ q
lt_q : (⨆ (k : ℕ) (_ : ennrealRatEmbed k ≤ f a), ennrealRatEmbed k) < ↑(Real.toNNReal ↑q)
q_lt : ↑(Real.toNNReal ↑q) < f a
⊢ ↑(Real.toNNReal ↑q) ≤ ⨆ (_ : ennrealRatEmbed (Encodable.encode q) ≤ f a), ennrealRatEmbed (Encodable.encode q)
α : Type u_1
β : Type ?u.838044
γ : Type ?u.838047
δ : Type ?u.838050
inst✝ : MeasurableSpace α
K : Type ?u.838056
f : α → ℝ≥0∞
hf : Measurable f
a : α
h : f a > ⨆ (k : ℕ) (_ : ennrealRatEmbed k ≤ f a), ennrealRatEmbed k
q : ℚ
left✝ : 0 ≤ q
lt_q : (⨆ (k : ℕ) (_ : ennrealRatEmbed k ≤ f a), ennrealRatEmbed k) < ↑(Real.toNNReal ↑q)
q_lt : ↑(Real.toNNReal ↑q) < f a
⊢ ↑(Real.toNNReal ↑q) ≤ ⨆ (k : ℕ) (_ : ennrealRatEmbed k ≤ f a), ennrealRatEmbed k
refine' le_iSup_of_le (Encodable.encode q) _
α : Type u_1
β : Type ?u.838044
γ : Type ?u.838047
δ : Type ?u.838050
inst✝ : MeasurableSpace α
K : Type ?u.838056
f : α → ℝ≥0∞
hf : Measurable f
a : α
h : f a > ⨆ (k : ℕ) (_ : ennrealRatEmbed k ≤ f a), ennrealRatEmbed k
q : ℚ
left✝ : 0 ≤ q
lt_q : (⨆ (k : ℕ) (_ : ennrealRatEmbed k ≤ f a), ennrealRatEmbed k) < ↑(Real.toNNReal ↑q)
q_lt : ↑(Real.toNNReal ↑q) < f a
⊢ ↑(Real.toNNReal ↑q) ≤ ⨆ (_ : ↑(Real.toNNReal ↑q) ≤ f a), ↑(Real.toNNReal ↑q)
α : Type u_1
β : Type ?u.838044
γ : Type ?u.838047
δ : Type ?u.838050
inst✝ : MeasurableSpace α
K : Type ?u.838056
f : α → ℝ≥0∞
hf : Measurable f
a : α
h : f a > ⨆ (k : ℕ) (_ : ennrealRatEmbed k ≤ f a), ennrealRatEmbed k
q : ℚ
left✝ : 0 ≤ q
lt_q : (⨆ (k : ℕ) (_ : ennrealRatEmbed k ≤ f a), ennrealRatEmbed k) < ↑(Real.toNNReal ↑q)
q_lt : ↑(Real.toNNReal ↑q) < f a
⊢ ↑(Real.toNNReal ↑q) ≤ ⨆ (_ : ennrealRatEmbed (Encodable.encode q) ≤ f a), ennrealRatEmbed (Encodable.encode q)
rw [ennrealRatEmbed_encode q]
α : Type u_1
β : Type ?u.838044
γ : Type ?u.838047
δ : Type ?u.838050
inst✝ : MeasurableSpace α
K : Type ?u.838056
f : α → ℝ≥0∞
hf : Measurable f
a : α
h : f a > ⨆ (k : ℕ) (_ : ennrealRatEmbed k ≤ f a), ennrealRatEmbed k
q : ℚ
left✝ : 0 ≤ q
lt_q : (⨆ (k : ℕ) (_ : ennrealRatEmbed k ≤ f a), ennrealRatEmbed k) < ↑(Real.toNNReal ↑q)
q_lt : ↑(Real.toNNReal ↑q) < f a
⊢ ↑(Real.toNNReal ↑q) ≤ ↑(Real.toNNReal ↑q)
α : Type u_1
β : Type ?u.838044
γ : Type ?u.838047
δ : Type ?u.838050
inst✝ : MeasurableSpace α
K : Type ?u.838056
f : α → ℝ≥0∞
hf : Measurable f
a : α
h : f a > ⨆ (k : ℕ) (_ : ennrealRatEmbed k ≤ f a), ennrealRatEmbed k
q : ℚ
left✝ : 0 ≤ q
lt_q : (⨆ (k : ℕ) (_ : ennrealRatEmbed k ≤ f a), ennrealRatEmbed k) < ↑(Real.toNNReal ↑q)
q_lt : ↑(Real.toNNReal ↑q) < f a
⊢ ↑(Real.toNNReal ↑q) ≤ ⨆ (_ : ↑(Real.toNNReal ↑q) ≤ f a), ↑(Real.toNNReal ↑q)
refine' le_iSup_of_le (le_of_lt q_lt) _
no goals
α : Type u_1
β : Type ?u.838044
γ : Type ?u.838047
δ : Type ?u.838050
inst✝ : MeasurableSpace α
K : Type ?u.838056
f : α → ℝ≥0∞
hf : Measurable f
a : α
h : f a > ⨆ (k : ℕ) (_ : ennrealRatEmbed k ≤ f a), ennrealRatEmbed k
q : ℚ
left✝ : 0 ≤ q
lt_q : (⨆ (k : ℕ) (_ : ennrealRatEmbed k ≤ f a), ennrealRatEmbed k) < ↑(Real.toNNReal ↑q)
q_lt : ↑(Real.toNNReal ↑q) < f a
⊢ ↑(Real.toNNReal ↑q) ≤ ↑(Real.toNNReal ↑q)
exact le_rfl