-- Mathlib/MeasureTheory/Function/SimpleFunc.lean
theorem eapprox_lt_top (f : α → ℝ≥0∞) (n : ℕ) (a : α) : eapprox f n a < ∞

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
f : α → ℝ≥0∞
n : ℕ
a : α
⊢ ∀ b ∈ Finset.range n,
    (if hs : MeasurableSet {a | ennrealRatEmbed b ≤ f a} then
          piecewise {a | ennrealRatEmbed b ≤ f a} hs (const α (ennrealRatEmbed b)) 0
        else 0)
        a <
      ⊤

Tactic:
intro b _

Result:
α : Type u_1
inst✝ : MeasurableSpace α
f : α → ℝ≥0∞
n : ℕ
a : α
b : ℕ
a✝ : b ∈ Finset.range n
⊢ (if hs : MeasurableSet {a | ennrealRatEmbed b ≤ f a} then
        piecewise {a | ennrealRatEmbed b ≤ f a} hs (const α (ennrealRatEmbed b)) 0
      else 0)
      a <
    ⊤

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
f : α → ℝ≥0∞
n : ℕ
a : α
⊢ ((Finset.range n).sup fun c =>
      (if hs : MeasurableSet {a | ennrealRatEmbed c ≤ f a} then
          piecewise {a | ennrealRatEmbed c ≤ f a} hs (const α (ennrealRatEmbed c)) 0
        else 0)
        a) <
    ⊤

Tactic:
rw [Finset.sup_lt_iff (α := ℝ≥0∞) WithTop.top_pos]

Result:
α : Type u_1
inst✝ : MeasurableSpace α
f : α → ℝ≥0∞
n : ℕ
a : α
⊢ ∀ b ∈ Finset.range n,
    (if hs : MeasurableSet {a | ennrealRatEmbed b ≤ f a} then
          piecewise {a | ennrealRatEmbed b ≤ f a} hs (const α (ennrealRatEmbed b)) 0
        else 0)
        a <
      ⊤

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
f : α → ℝ≥0∞
n : ℕ
a : α
b : ℕ
a✝ : b ∈ Finset.range n
⊢ (if hs : MeasurableSet {a | ennrealRatEmbed b ≤ f a} then
        piecewise {a | ennrealRatEmbed b ≤ f a} hs (const α (ennrealRatEmbed b)) 0
      else 0)
      a <
    ⊤

Tactic:
split_ifs

Result:
case pos
α : Type u_1
inst✝ : MeasurableSpace α
f : α → ℝ≥0∞
n : ℕ
a : α
b : ℕ
a✝ : b ∈ Finset.range n
h✝ : MeasurableSet {a | ennrealRatEmbed b ≤ f a}
⊢ (piecewise {a | ennrealRatEmbed b ≤ f a} h✝ (const α (ennrealRatEmbed b)) 0) a < ⊤

case neg
α : Type u_1
inst✝ : MeasurableSpace α
f : α → ℝ≥0∞
n : ℕ
a : α
b : ℕ
a✝ : b ∈ Finset.range n
h✝ : ¬MeasurableSet {a | ennrealRatEmbed b ≤ f a}
⊢ 0 a < ⊤

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
f : α → ℝ≥0∞
n : ℕ
a : α
⊢ (eapprox f n) a < ⊤

Tactic:
simp only [eapprox, approx, finset_sup_apply, Finset.mem_range, ENNReal.bot_eq_zero, restrict]

Result:
α : Type u_1
inst✝ : MeasurableSpace α
f : α → ℝ≥0∞
n : ℕ
a : α
⊢ ((Finset.range n).sup fun c =>
      (if hs : MeasurableSet {a | ennrealRatEmbed c ≤ f a} then
          piecewise {a | ennrealRatEmbed c ≤ f a} hs (const α (ennrealRatEmbed c)) 0
        else 0)
        a) <
    ⊤

Proof state:
case neg
α : Type u_1
inst✝ : MeasurableSpace α
f : α → ℝ≥0∞
n : ℕ
a : α
b : ℕ
a✝ : b ∈ Finset.range n
h✝ : ¬MeasurableSet {a | ennrealRatEmbed b ≤ f a}
⊢ 0 a < ⊤

Tactic:
exact WithTop.top_pos

Result:
no goals

Proof state:
case pos
α : Type u_1
inst✝ : MeasurableSpace α
f : α → ℝ≥0∞
n : ℕ
a : α
b : ℕ
a✝ : b ∈ Finset.range n
h✝ : MeasurableSet {a | ennrealRatEmbed b ≤ f a}
⊢ (piecewise {a | ennrealRatEmbed b ≤ f a} h✝ (const α (ennrealRatEmbed b)) 0) a < ⊤

Tactic:
simp only [coe_zero, coe_piecewise, piecewise_eq_indicator, coe_const]

Result:
case pos
α : Type u_1
inst✝ : MeasurableSpace α
f : α → ℝ≥0∞
n : ℕ
a : α
b : ℕ
a✝ : b ∈ Finset.range n
h✝ : MeasurableSet {a | ennrealRatEmbed b ≤ f a}
⊢ {a | ennrealRatEmbed b ≤ f a}.indicator (Function.const α (ennrealRatEmbed b)) a < ⊤

Proof state:
case pos
α : Type u_1
inst✝ : MeasurableSpace α
f : α → ℝ≥0∞
n : ℕ
a : α
b : ℕ
a✝ : b ∈ Finset.range n
h✝ : MeasurableSet {a | ennrealRatEmbed b ≤ f a}
⊢ {a | ennrealRatEmbed b ≤ f a}.indicator (Function.const α (ennrealRatEmbed b)) a < ⊤

Tactic:
calc
  { a : α | ennrealRatEmbed b ≤ f a }.indicator (fun _ => ennrealRatEmbed b) a ≤
      ennrealRatEmbed b :=
    indicator_le_self _ _ a
  _ < ⊤ := ENNReal.coe_lt_top

Result:
no goals