α : Type u_1
β : Type ?u.834539
γ : Type ?u.834542
δ : Type ?u.834545
inst✝ : MeasurableSpace α
K : Type ?u.834551
f : α → ℝ≥0∞
n : ℕ
a : α
⊢ (Finset.sup (Finset.range n) 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) <
    ⊤
α : Type u_1
β : Type ?u.834539
γ : Type ?u.834542
δ : Type ?u.834545
inst✝ : MeasurableSpace α
K : Type ?u.834551
f : α → ℝ≥0∞
n : ℕ
a : α
⊢ ↑(eapprox f n) a < ⊤
simp only [eapprox, approx, finset_sup_apply, Finset.mem_range, ENNReal.bot_eq_zero, restrict]
α : Type u_1
β : Type ?u.834539
γ : Type ?u.834542
δ : Type ?u.834545
inst✝ : MeasurableSpace α
K : Type ?u.834551
f : α → ℝ≥0∞
n : ℕ
a : α
⊢ ∀ (b : ℕ),
    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 <
        ⊤
α : Type u_1
β : Type ?u.834539
γ : Type ?u.834542
δ : Type ?u.834545
inst✝ : MeasurableSpace α
K : Type ?u.834551
f : α → ℝ≥0∞
n : ℕ
a : α
⊢ (Finset.sup (Finset.range n) 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) <
    ⊤
rw [Finset.sup_lt_iff (α := ℝ≥0∞) WithTop.zero_lt_top]
α : Type u_1
β : Type ?u.834539
γ : Type ?u.834542
δ : Type ?u.834545
inst✝ : MeasurableSpace α
K : Type ?u.834551
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 <
    ⊤
α : Type u_1
β : Type ?u.834539
γ : Type ?u.834542
δ : Type ?u.834545
inst✝ : MeasurableSpace α
K : Type ?u.834551
f : α → ℝ≥0∞
n : ℕ
a : α
⊢ ∀ (b : ℕ),
    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 <
        ⊤
intro b _
case inl
α : Type u_1
β : Type ?u.834539
γ : Type ?u.834542
δ : Type ?u.834545
inst✝ : MeasurableSpace α
K : Type ?u.834551
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 inr
α : Type u_1
β : Type ?u.834539
γ : Type ?u.834542
δ : Type ?u.834545
inst✝ : MeasurableSpace α
K : Type ?u.834551
f : α → ℝ≥0∞
n : ℕ
a : α
b : ℕ
a✝ : b ∈ Finset.range n
h✝ : ¬MeasurableSet {a | ennrealRatEmbed b ≤ f a}
⊢ ↑0 a < ⊤
α : Type u_1
β : Type ?u.834539
γ : Type ?u.834542
δ : Type ?u.834545
inst✝ : MeasurableSpace α
K : Type ?u.834551
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 <
    ⊤
split_ifs
case inl
α : Type u_1
β : Type ?u.834539
γ : Type ?u.834542
δ : Type ?u.834545
inst✝ : MeasurableSpace α
K : Type ?u.834551
f : α → ℝ≥0∞
n : ℕ
a : α
b : ℕ
a✝ : b ∈ Finset.range n
h✝ : MeasurableSet {a | ennrealRatEmbed b ≤ f a}
⊢ Set.piecewise {a | ennrealRatEmbed b ≤ f a} (Function.const α (ennrealRatEmbed b)) 0 a < ⊤
case inl
α : Type u_1
β : Type ?u.834539
γ : Type ?u.834542
δ : Type ?u.834545
inst✝ : MeasurableSpace α
K : Type ?u.834551
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 < ⊤
simp only [coe_zero, coe_piecewise, piecewise_eq_indicator, coe_const]
no goals
case inl
α : Type u_1
β : Type ?u.834539
γ : Type ?u.834542
δ : Type ?u.834545
inst✝ : MeasurableSpace α
K : Type ?u.834551
f : α → ℝ≥0∞
n : ℕ
a : α
b : ℕ
a✝ : b ∈ Finset.range n
h✝ : MeasurableSet {a | ennrealRatEmbed b ≤ f a}
⊢ Set.piecewise {a | ennrealRatEmbed b ≤ f a} (Function.const α (ennrealRatEmbed b)) 0 a < ⊤
calc
  { a : α | ennrealRatEmbed b ≤ f a }.indicator (fun _ => ennrealRatEmbed b) a ≤
      ennrealRatEmbed b :=
    indicator_le_self _ _ a
  _ < ⊤ := ENNReal.coe_lt_top
no goals
case inr
α : Type u_1
β : Type ?u.834539
γ : Type ?u.834542
δ : Type ?u.834545
inst✝ : MeasurableSpace α
K : Type ?u.834551
f : α → ℝ≥0∞
n : ℕ
a : α
b : ℕ
a✝ : b ∈ Finset.range n
h✝ : ¬MeasurableSet {a | ennrealRatEmbed b ≤ f a}
⊢ ↑0 a < ⊤
exact WithTop.zero_lt_top