-- Mathlib/MeasureTheory/Function/SimpleFunc.lean
lemma iSup_eapprox_apply (hf : Measurable f) (a : α) : ⨆ n, (eapprox f n : α →ₛ ℝ≥0∞) a = f a

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
f : α → ℝ≥0∞
hf : Measurable f
a : α
⊢ ¬f a > ⨆ k, ⨆ (_ : ennrealRatEmbed k ≤ f a), ennrealRatEmbed k

Tactic:
intro h

Result:
α : Type u_1
inst✝ : MeasurableSpace α
f : α → ℝ≥0∞
hf : Measurable f
a : α
h : f a > ⨆ k, ⨆ (_ : ennrealRatEmbed k ≤ f a), ennrealRatEmbed k
⊢ False

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
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 < ↑(↑q).toNNReal
q_lt : ↑(↑q).toNNReal < f a
⊢ ↑(↑q).toNNReal ≤ ⨆ k, ⨆ (_ : ennrealRatEmbed k ≤ f a), ennrealRatEmbed k

Tactic:
refine le_iSup_of_le (Encodable.encode q) ?_

Result:
α : Type u_1
inst✝ : MeasurableSpace α
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 < ↑(↑q).toNNReal
q_lt : ↑(↑q).toNNReal < f a
⊢ ↑(↑q).toNNReal ≤ ⨆ (_ : ennrealRatEmbed (Encodable.encode q) ≤ f a), ennrealRatEmbed (Encodable.encode q)

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
f : α → ℝ≥0∞
hf : Measurable f
a : α
⊢ ⨆ n, (eapprox f n) a = f a

Tactic:
rw [eapprox, iSup_approx_apply ennrealRatEmbed f a hf rfl]

Result:
α : Type u_1
inst✝ : MeasurableSpace α
f : α → ℝ≥0∞
hf : Measurable f
a : α
⊢ ⨆ k, ⨆ (_ : ennrealRatEmbed k ≤ f a), ennrealRatEmbed k = f a

Proof state:
case intro.intro.intro
α : Type u_1
inst✝ : MeasurableSpace α
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 < ↑(↑q).toNNReal
q_lt : ↑(↑q).toNNReal < f a
⊢ False

Tactic:
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]
  exact le_iSup_of_le (le_of_lt q_lt) le_rfl

Result:
case intro.intro.intro
α : Type u_1
inst✝ : MeasurableSpace α
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 < ↑(↑q).toNNReal
q_lt : ↑(↑q).toNNReal < f a
this : ↑(↑q).toNNReal ≤ ⨆ k, ⨆ (_ : ennrealRatEmbed k ≤ f a), ennrealRatEmbed k
⊢ False

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
f : α → ℝ≥0∞
hf : Measurable f
a : α
h : f a > ⨆ k, ⨆ (_ : ennrealRatEmbed k ≤ f a), ennrealRatEmbed k
⊢ False

Tactic:
rcases ENNReal.lt_iff_exists_rat_btwn.1 h with ⟨q, _, lt_q, q_lt⟩

Result:
case intro.intro.intro
α : Type u_1
inst✝ : MeasurableSpace α
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 < ↑(↑q).toNNReal
q_lt : ↑(↑q).toNNReal < f a
⊢ False

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
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 < ↑(↑q).toNNReal
q_lt : ↑(↑q).toNNReal < f a
⊢ ↑(↑q).toNNReal ≤ ⨆ (_ : ↑(↑q).toNNReal ≤ f a), ↑(↑q).toNNReal

Tactic:
exact le_iSup_of_le (le_of_lt q_lt) le_rfl

Result:
no goals

Proof state:
case intro.intro.intro
α : Type u_1
inst✝ : MeasurableSpace α
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 < ↑(↑q).toNNReal
q_lt : ↑(↑q).toNNReal < f a
this : ↑(↑q).toNNReal ≤ ⨆ k, ⨆ (_ : ennrealRatEmbed k ≤ f a), ennrealRatEmbed k
⊢ False

Tactic:
exact lt_irrefl _ (lt_of_le_of_lt this lt_q)

Result:
no goals

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
f : α → ℝ≥0∞
hf : Measurable f
a : α
⊢ ⨆ k, ⨆ (_ : ennrealRatEmbed k ≤ f a), ennrealRatEmbed k = f a

Tactic:
refine le_antisymm (iSup_le fun i => iSup_le fun hi => hi) (le_of_not_gt ?_)

Result:
α : Type u_1
inst✝ : MeasurableSpace α
f : α → ℝ≥0∞
hf : Measurable f
a : α
⊢ ¬f a > ⨆ k, ⨆ (_ : ennrealRatEmbed k ≤ f a), ennrealRatEmbed k

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
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 < ↑(↑q).toNNReal
q_lt : ↑(↑q).toNNReal < f a
⊢ ↑(↑q).toNNReal ≤ ⨆ (_ : ennrealRatEmbed (Encodable.encode q) ≤ f a), ennrealRatEmbed (Encodable.encode q)

Tactic:
rw [ennrealRatEmbed_encode q]

Result:
α : Type u_1
inst✝ : MeasurableSpace α
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 < ↑(↑q).toNNReal
q_lt : ↑(↑q).toNNReal < f a
⊢ ↑(↑q).toNNReal ≤ ⨆ (_ : ↑(↑q).toNNReal ≤ f a), ↑(↑q).toNNReal