awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_1
inst : MeasurableSpace α
f : α → ℝ≥0∞
n : ℕ
a : α
simp :
  LT.lt (α := ℝ≥0∞)
    ((Finset.range n).sup fun (c : ℕ) ↦
      ((if hs : MeasurableSet.{u_1} (α := α) {a : α | ennrealRatEmbed c ≤ f a} then
              piecewise {a : α | ennrealRatEmbed c ≤ f a} hs (const α (ennrealRatEmbed c)) 0
            else 0 :
            α →ₛ ℝ≥0∞) :
          (a : α) → ℝ≥0∞)
        a)
    ∞
⊢ LT.lt (α := ℝ≥0∞) (((eapprox f n : α →ₛ ℝ≥0∞) : (a : α) → ℝ≥0∞) a : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
simp only [eapprox, approx, finset_sup_apply, restrict]

Premises used: MeasureTheory.SimpleFunc.approx, MeasureTheory.SimpleFunc.eapprox, MeasureTheory.SimpleFunc.restrict, MeasureTheory.SimpleFunc.finset_sup_apply
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_1
inst : MeasurableSpace α
f : α → ℝ≥0∞
n : ℕ
a : α
rw :
  ∀ b ∈ Finset.range n,
    LT.lt (α := ℝ≥0∞)
      (((if hs : MeasurableSet.{u_1} (α := α) {a : α | ennrealRatEmbed b ≤ f a} then
                piecewise {a : α | ennrealRatEmbed b ≤ f a} hs (const α (ennrealRatEmbed b)) 0
              else 0 :
              α →ₛ ℝ≥0∞) :
            (a : α) → ℝ≥0∞)
          a :
        ℝ≥0∞)
      (⊤ : WithTop ℝ≥0)
⊢ LT.lt (α := ℝ≥0∞)
    ((Finset.range n).sup fun (c : ℕ) ↦
      ((if hs : MeasurableSet.{u_1} (α := α) {a : α | ennrealRatEmbed c ≤ f a} then
              piecewise {a : α | ennrealRatEmbed c ≤ f a} hs (const α (ennrealRatEmbed c)) 0
            else 0 :
            α →ₛ ℝ≥0∞) :
          (a : α) → ℝ≥0∞)
        a)
    ∞

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

Premises used: Finset.sup_lt_iff, WithTop.top_pos
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_1
inst : MeasurableSpace α
f : α → ℝ≥0∞
n : ℕ
a : α
b : ℕ
_ :
  b ∈ Finset.range n →
    LT.lt (α := ℝ≥0∞)
      (((if hs : MeasurableSet.{u_1} (α := α) {a : α | ennrealRatEmbed b ≤ f a} then
                piecewise {a : α | ennrealRatEmbed b ≤ f a} hs (const α (ennrealRatEmbed b)) 0
              else 0 :
              α →ₛ ℝ≥0∞) :
            (a : α) → ℝ≥0∞)
          a :
        ℝ≥0∞)
      (⊤ : WithTop ℝ≥0)
⊢ b ∈ Finset.range n →
    LT.lt (α := ℝ≥0∞)
      (((if hs : MeasurableSet.{u_1} (α := α) {a : α | ennrealRatEmbed b ≤ f a} then
                piecewise {a : α | ennrealRatEmbed b ≤ f a} hs (const α (ennrealRatEmbed b)) 0
              else 0 :
              α →ₛ ℝ≥0∞) :
            (a : α) → ℝ≥0∞)
          a :
        ℝ≥0∞)
      (⊤ : WithTop ℝ≥0)

Tactic:
_
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_1
inst : MeasurableSpace α
f : α → ℝ≥0∞
n : ℕ
a : α
b : ℕ
h : b ∈ Finset.range n
pos :
  ∀ (h : MeasurableSet.{u_1} (α := α) {a : α | ennrealRatEmbed b ≤ f a}),
    LT.lt (α := ℝ≥0∞)
      ((piecewise {a : α | ennrealRatEmbed b ≤ f a} h (const α (ennrealRatEmbed b)) 0 : (a : α) → ℝ≥0∞) a : ℝ≥0∞)
      (⊤ : WithTop ℝ≥0)
neg :
  ¬MeasurableSet.{u_1} (α := α) {a : α | ennrealRatEmbed b ≤ f a} →
    LT.lt (α := ℝ≥0∞) (((0 : α →ₛ ℝ≥0∞) : (a : α) → ℝ≥0∞) a : ℝ≥0∞) (⊤ : WithTop ℝ≥0)
⊢ LT.lt (α := ℝ≥0∞)
    (((if hs : MeasurableSet.{u_1} (α := α) {a : α | ennrealRatEmbed b ≤ f a} then
              piecewise {a : α | ennrealRatEmbed b ≤ f a} hs (const α (ennrealRatEmbed b)) 0
            else 0 :
            α →ₛ ℝ≥0∞) :
          (a : α) → ℝ≥0∞)
        a :
      ℝ≥0∞)
    (⊤ : WithTop ℝ≥0)

Tactic:
split_ifs
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_1
inst : MeasurableSpace α
f : α → ℝ≥0∞
n : ℕ
a : α
b : ℕ
h : b ∈ Finset.range n
h_1 : MeasurableSet.{u_1} (α := α) {a : α | ennrealRatEmbed b ≤ f a}
⊢ indicator {a : α | ennrealRatEmbed b ≤ f a} (fun (x : α) ↦ ennrealRatEmbed b) a ≤ ennrealRatEmbed b

Tactic:
indicator_le_self _ _ a

Premises used: Set.indicator_le_self
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_1
inst : MeasurableSpace α
f : α → ℝ≥0∞
n : ℕ
a : α
b : ℕ
h : b ∈ Finset.range n
h_1 : MeasurableSet.{u_1} (α := α) {a : α | ennrealRatEmbed b ≤ f a}
⊢ ennrealRatEmbed b < ∞

Tactic:
ENNReal.coe_lt_top

Premises used: ENNReal.ofReal, MeasureTheory.SimpleFunc.ennrealRatEmbed, ENNReal.coe_lt_top
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_1
inst : MeasurableSpace α
f : α → ℝ≥0∞
n : ℕ
a : α
b : ℕ
h : b ∈ Finset.range n
h_1 : MeasurableSet.{u_1} (α := α) {a : α | ennrealRatEmbed b ≤ f a}
⊢ indicator {a : α | ennrealRatEmbed b ≤ f a} (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

Premises used: Set.indicator, setOf, LE.le, Set.indicator_le_self, MeasureTheory.SimpleFunc.ennrealRatEmbed, ENNReal.coe_lt_top
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_1
inst : MeasurableSpace α
f : α → ℝ≥0∞
n : ℕ
a : α
b : ℕ
h : b ∈ Finset.range n
h_1 : ¬MeasurableSet.{u_1} (α := α) {a : α | ennrealRatEmbed b ≤ f a}
⊢ LT.lt (α := ℝ≥0∞) (((0 : α →ₛ ℝ≥0∞) : (a : α) → ℝ≥0∞) a : ℝ≥0∞) (⊤ : WithTop ℝ≥0)

Tactic:
WithTop.top_pos

Premises used: ENNReal.ofNNReal, WithTop.top_pos
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_1
inst : MeasurableSpace α
f : α → ℝ≥0∞
n : ℕ
a : α
b : ℕ
h : b ∈ Finset.range n
h_1 : ¬MeasurableSet.{u_1} (α := α) {a : α | ennrealRatEmbed b ≤ f a}
⊢ LT.lt (α := ℝ≥0∞) (((0 : α →ₛ ℝ≥0∞) : (a : α) → ℝ≥0∞) a : ℝ≥0∞) (⊤ : WithTop ℝ≥0)

Tactic:
exact WithTop.top_pos

Premises used: WithTop.top_pos
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_1
inst : MeasurableSpace α
f : α → ℝ≥0∞
⊢ Monotone (β := α →ₛ ℝ≥0∞) (eapprox f)

Tactic:
monotone_approx _ f

Premises used: MeasureTheory.SimpleFunc.eapprox, MeasureTheory.SimpleFunc.monotone_approx
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_1
inst : MeasurableSpace α
f : α → ℝ≥0∞
hf : Measurable f
a : α
rw : ⨆ (k : ℕ), ⨆ (_ : ennrealRatEmbed k ≤ f a), ennrealRatEmbed k = f a
⊢ ⨆ (n : ℕ), ((eapprox f n : α →ₛ ℝ≥0∞) : (a : α) → ℝ≥0∞) a = f a

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

Premises used: MeasureTheory.SimpleFunc.eapprox, MeasureTheory.SimpleFunc.ennrealRatEmbed, MeasureTheory.SimpleFunc.iSup_approx_apply, rfl
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_1
inst : MeasurableSpace α
f : α → ℝ≥0∞
hf : Measurable f
a : α
⊢ ⨆ (k : ℕ), ⨆ (_ : ennrealRatEmbed k ≤ f a), ennrealRatEmbed k = f a

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

Premises used: le_of_not_gt, le_antisymm, iSup_le
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_1
inst : MeasurableSpace α
f : α → ℝ≥0∞
hf : Measurable f
a : α
refine : ¬⨆ (k : ℕ), ⨆ (_ : ennrealRatEmbed k ≤ f a), ennrealRatEmbed k < 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 ?_)

Premises used: le_antisymm, iSup_le
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_1
inst : MeasurableSpace α
f : α → ℝ≥0∞
hf : Measurable f
a : α
h : ⨆ (k : ℕ), ⨆ (_ : ennrealRatEmbed k ≤ f a), ennrealRatEmbed k < f a
rcases :
  ∀ (q : ℚ),
    0 ≤ q →
      ∀ (lt_q : ⨆ (k : ℕ), ⨆ (_ : ennrealRatEmbed k ≤ f a), ennrealRatEmbed k < (↑(Real.toNNReal (↑q : ℝ)) : ℝ≥0∞))
        (q_lt : (↑(Real.toNNReal (↑q : ℝ)) : ℝ≥0∞) < f a), False
⊢ False

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

Premises used: Iff.mp, ENNReal.lt_iff_exists_rat_btwn
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_1
inst : MeasurableSpace α
f : α → ℝ≥0∞
hf : Measurable f
a : α
h : ⨆ (k : ℕ), ⨆ (_ : ennrealRatEmbed k ≤ f a), ennrealRatEmbed k < f a
q : ℚ
left : 0 ≤ q
lt_q : ⨆ (k : ℕ), ⨆ (_ : ennrealRatEmbed k ≤ f a), ennrealRatEmbed k < (↑(Real.toNNReal (↑q : ℝ)) : ℝ≥0∞)
q_lt : (↑(Real.toNNReal (↑q : ℝ)) : ℝ≥0∞) < f a
⊢ (↑(Real.toNNReal (↑q : ℝ)) : ℝ≥0∞) ≤ ⨆ (k : ℕ), ⨆ (_ : ennrealRatEmbed k ≤ f a), ennrealRatEmbed k

Tactic:
le_iSup_of_le (Encodable.encode q) ?_

Premises used: le_iSup_of_le, Encodable.encode
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_1
inst : MeasurableSpace α
f : α → ℝ≥0∞
hf : Measurable f
a : α
h : ⨆ (k : ℕ), ⨆ (_ : ennrealRatEmbed k ≤ f a), ennrealRatEmbed k < f a
q : ℚ
left : 0 ≤ q
lt_q : ⨆ (k : ℕ), ⨆ (_ : ennrealRatEmbed k ≤ f a), ennrealRatEmbed k < (↑(Real.toNNReal (↑q : ℝ)) : ℝ≥0∞)
q_lt : (↑(Real.toNNReal (↑q : ℝ)) : ℝ≥0∞) < f a
refine :
  (↑(Real.toNNReal (↑q : ℝ)) : ℝ≥0∞) ≤
    ⨆ (_ : ennrealRatEmbed (Encodable.encode q) ≤ f a), ennrealRatEmbed (Encodable.encode q)
⊢ (↑(Real.toNNReal (↑q : ℝ)) : ℝ≥0∞) ≤ ⨆ (k : ℕ), ⨆ (_ : ennrealRatEmbed k ≤ f a), ennrealRatEmbed k

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

Premises used: le_iSup_of_le, Encodable.encode
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_1
inst : MeasurableSpace α
f : α → ℝ≥0∞
hf : Measurable f
a : α
h : ⨆ (k : ℕ), ⨆ (_ : ennrealRatEmbed k ≤ f a), ennrealRatEmbed k < f a
q : ℚ
left : 0 ≤ q
lt_q : ⨆ (k : ℕ), ⨆ (_ : ennrealRatEmbed k ≤ f a), ennrealRatEmbed k < (↑(Real.toNNReal (↑q : ℝ)) : ℝ≥0∞)
q_lt : (↑(Real.toNNReal (↑q : ℝ)) : ℝ≥0∞) < f a
rw :
  (↑(Real.toNNReal (↑q : ℝ)) : ℝ≥0∞) ≤
    ⨆ (_ : (↑(Real.toNNReal (↑q : ℝ)) : ℝ≥0∞) ≤ f a), (↑(Real.toNNReal (↑q : ℝ)) : ℝ≥0∞)
⊢ (↑(Real.toNNReal (↑q : ℝ)) : ℝ≥0∞) ≤
    ⨆ (_ : ennrealRatEmbed (Encodable.encode q) ≤ f a), ennrealRatEmbed (Encodable.encode q)

Tactic:
rw [ennrealRatEmbed_encode q]

Premises used: MeasureTheory.SimpleFunc.ennrealRatEmbed_encode
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_1
inst : MeasurableSpace α
f : α → ℝ≥0∞
hf : Measurable f
a : α
h : ⨆ (k : ℕ), ⨆ (_ : ennrealRatEmbed k ≤ f a), ennrealRatEmbed k < f a
q : ℚ
left : 0 ≤ q
lt_q : ⨆ (k : ℕ), ⨆ (_ : ennrealRatEmbed k ≤ f a), ennrealRatEmbed k < (↑(Real.toNNReal (↑q : ℝ)) : ℝ≥0∞)
q_lt : (↑(Real.toNNReal (↑q : ℝ)) : ℝ≥0∞) < f a
⊢ (↑(Real.toNNReal (↑q : ℝ)) : ℝ≥0∞) ≤
    ⨆ (_ : (↑(Real.toNNReal (↑q : ℝ)) : ℝ≥0∞) ≤ f a), (↑(Real.toNNReal (↑q : ℝ)) : ℝ≥0∞)

Tactic:
le_iSup_of_le (le_of_lt q_lt) le_rfl

Premises used: le_rfl, le_of_lt, le_iSup_of_le
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_1
inst : MeasurableSpace α
f : α → ℝ≥0∞
hf : Measurable f
a : α
h : ⨆ (k : ℕ), ⨆ (_ : ennrealRatEmbed k ≤ f a), ennrealRatEmbed k < f a
q : ℚ
left : 0 ≤ q
lt_q : ⨆ (k : ℕ), ⨆ (_ : ennrealRatEmbed k ≤ f a), ennrealRatEmbed k < (↑(Real.toNNReal (↑q : ℝ)) : ℝ≥0∞)
q_lt : (↑(Real.toNNReal (↑q : ℝ)) : ℝ≥0∞) < f a
⊢ (↑(Real.toNNReal (↑q : ℝ)) : ℝ≥0∞) ≤
    ⨆ (_ : (↑(Real.toNNReal (↑q : ℝ)) : ℝ≥0∞) ≤ f a), (↑(Real.toNNReal (↑q : ℝ)) : ℝ≥0∞)

Tactic:
exact le_iSup_of_le (le_of_lt q_lt) le_rfl

Premises used: le_rfl, le_of_lt, le_iSup_of_le
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_1
inst : MeasurableSpace α
f : α → ℝ≥0∞
hf : Measurable f
a : α
h : ⨆ (k : ℕ), ⨆ (_ : ennrealRatEmbed k ≤ f a), ennrealRatEmbed k < f a
q : ℚ
left : 0 ≤ q
lt_q : ⨆ (k : ℕ), ⨆ (_ : ennrealRatEmbed k ≤ f a), ennrealRatEmbed k < (↑(Real.toNNReal (↑q : ℝ)) : ℝ≥0∞)
q_lt : (↑(Real.toNNReal (↑q : ℝ)) : ℝ≥0∞) < f a
⊢ (↑(Real.toNNReal (↑q : ℝ)) : ℝ≥0∞) ≤ ⨆ (k : ℕ), ⨆ (_ : ennrealRatEmbed k ≤ f a), ennrealRatEmbed k

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
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_1
inst : MeasurableSpace α
f : α → ℝ≥0∞
hf : Measurable f
a : α
h : ⨆ (k : ℕ), ⨆ (_ : ennrealRatEmbed k ≤ f a), ennrealRatEmbed k < f a
q : ℚ
left : 0 ≤ q
lt_q : ⨆ (k : ℕ), ⨆ (_ : ennrealRatEmbed k ≤ f a), ennrealRatEmbed k < (↑(Real.toNNReal (↑q : ℝ)) : ℝ≥0∞)
q_lt : (↑(Real.toNNReal (↑q : ℝ)) : ℝ≥0∞) < f a
this : (↑(Real.toNNReal (↑q : ℝ)) : ℝ≥0∞) ≤ ⨆ (k : ℕ), ⨆ (_ : ennrealRatEmbed k ≤ f a), ennrealRatEmbed k
⊢ False

Tactic:
lt_irrefl _ (lt_of_le_of_lt this lt_q)

Premises used: lt_of_le_of_lt, lt_irrefl
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_1
inst : MeasurableSpace α
f : α → ℝ≥0∞
hf : Measurable f
a : α
h : ⨆ (k : ℕ), ⨆ (_ : ennrealRatEmbed k ≤ f a), ennrealRatEmbed k < f a
q : ℚ
left : 0 ≤ q
lt_q : ⨆ (k : ℕ), ⨆ (_ : ennrealRatEmbed k ≤ f a), ennrealRatEmbed k < (↑(Real.toNNReal (↑q : ℝ)) : ℝ≥0∞)
q_lt : (↑(Real.toNNReal (↑q : ℝ)) : ℝ≥0∞) < f a
this : (↑(Real.toNNReal (↑q : ℝ)) : ℝ≥0∞) ≤ ⨆ (k : ℕ), ⨆ (_ : ennrealRatEmbed k ≤ f a), ennrealRatEmbed k
⊢ False

Tactic:
exact lt_irrefl _ (lt_of_le_of_lt this lt_q)

Premises used: lt_of_le_of_lt, lt_irrefl
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_1
inst : MeasurableSpace α
f : α → ℝ≥0∞
hf : Measurable f
⊢ ⨆ (n : ℕ), (⇑(eapprox f n) : (a : α) → ℝ≥0∞) = f

Tactic:
simpa [funext_iff] using iSup_eapprox_apply hf

Premises used: funext_iff, MeasureTheory.SimpleFunc.iSup_eapprox_apply
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_1
γ : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace γ
f : γ → ℝ≥0∞
g : α → γ
n : ℕ
hf : Measurable f
hg : Measurable g
⊢ Eq (α := (a : α) → ℝ≥0∞) (⇑(eapprox (f ∘ g) n) : (a : α) → ℝ≥0∞) ((⇑(eapprox f n) : (a : γ) → ℝ≥0∞) ∘ g)

Tactic:
funext fun a => approx_comp a hf hg

Premises used: funext, MeasureTheory.SimpleFunc.approx_comp
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_1
inst : MeasurableSpace α
f : α → ℝ≥0∞
hf_meas : Measurable f
a : α
nth_rw :
  Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ ((eapprox f n : α →ₛ ℝ≥0∞) : (a : α) → ℝ≥0∞) a) atTop
    (𝓝 ((⨆ (n : ℕ), (⇑(eapprox f n) : (a : α) → ℝ≥0∞)) a))
⊢ Tendsto (fun (n : ℕ) ↦ ((eapprox f n : α →ₛ ℝ≥0∞) : (a : α) → ℝ≥0∞) a) atTop (𝓝 (f a))

Tactic:
nth_rw 2 [← iSup_coe_eapprox hf_meas]

Premises used: MeasureTheory.SimpleFunc.iSup_coe_eapprox
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_1
inst : MeasurableSpace α
f : α → ℝ≥0∞
hf_meas : Measurable f
a : α
rw :
  Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ ((eapprox f n : α →ₛ ℝ≥0∞) : (a : α) → ℝ≥0∞) a) atTop
    (𝓝 (⨆ (i : ℕ), ((eapprox f i : α →ₛ ℝ≥0∞) : (a : α) → ℝ≥0∞) a))
⊢ Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ ((eapprox f n : α →ₛ ℝ≥0∞) : (a : α) → ℝ≥0∞) a) atTop
    (𝓝 ((⨆ (n : ℕ), (⇑(eapprox f n) : (a : α) → ℝ≥0∞)) a))

Tactic:
rw [iSup_apply]

Premises used: iSup_apply
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_1
inst : MeasurableSpace α
f : α → ℝ≥0∞
hf_meas : Measurable f
a : α
⊢ Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ ((eapprox f n : α →ₛ ℝ≥0∞) : (a : α) → ℝ≥0∞) a) atTop
    (𝓝 (⨆ (i : ℕ), ((eapprox f i : α →ₛ ℝ≥0∞) : (a : α) → ℝ≥0∞) a))

Tactic:
tendsto_atTop_iSup fun _ _ hnm ↦ monotone_eapprox f hnm a

Premises used: MeasureTheory.SimpleFunc.monotone_eapprox, tendsto_atTop_iSup
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_1
inst : MeasurableSpace α
f : α → ℝ≥0∞
hf_meas : Measurable f
a : α
⊢ Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ ((eapprox f n : α →ₛ ℝ≥0∞) : (a : α) → ℝ≥0∞) a) atTop
    (𝓝 (⨆ (i : ℕ), ((eapprox f i : α →ₛ ℝ≥0∞) : (a : α) → ℝ≥0∞) a))

Tactic:
exact tendsto_atTop_iSup fun _ _ hnm ↦ monotone_eapprox f hnm a

Premises used: MeasureTheory.SimpleFunc.monotone_eapprox, tendsto_atTop_iSup
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_1
inst : MeasurableSpace α
f : α → ℝ≥0∞
a : α
⊢ Eq (α := ℝ≥0∞)
    (∑ k ∈ Finset.range (HAdd.hAdd (α := ℕ) 0 1), (↑(((eapproxDiff f k : α →ₛ ℝ≥0) : (a : α) → ℝ≥0) a) : ℝ≥0∞) : ℝ≥0∞)
    (((eapprox f 0 : α →ₛ ℝ≥0∞) : (a : α) → ℝ≥0∞) a : ℝ≥0∞)

Tactic:
simp [eapproxDiff, (eapprox_lt_top f 0 a).ne]

Premises used: MeasureTheory.SimpleFunc.eapproxDiff, MeasureTheory.SimpleFunc.eapprox_lt_top, OfNat.ofNat, LT.lt.ne
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_1
inst : MeasurableSpace α
f : α → ℝ≥0∞
a : α
n : ℕ
IH :
  Eq (α := ℝ≥0∞) (∑ k ∈ Finset.range (n + 1), (↑(((eapproxDiff f k : α →ₛ ℝ≥0) : (a : α) → ℝ≥0) a) : ℝ≥0∞) : ℝ≥0∞)
    (((eapprox f n : α →ₛ ℝ≥0∞) : (a : α) → ℝ≥0∞) a : ℝ≥0∞)
succ :
  HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) (((eapprox f (n + 1) : α →ₛ ℝ≥0∞) : (a : α) → ℝ≥0∞) a : ℝ≥0∞)
      (((eapprox f n : α →ₛ ℝ≥0∞) : (a : α) → ℝ≥0∞) a : ℝ≥0∞) ≠
    ∞
⊢ Eq (α := ℝ≥0∞) (∑ k ∈ Finset.range (n + 1 + 1), (↑(((eapproxDiff f k : α →ₛ ℝ≥0) : (a : α) → ℝ≥0) a) : ℝ≥0∞) : ℝ≥0∞)
    (((eapprox f (n + 1) : α →ₛ ℝ≥0∞) : (a : α) → ℝ≥0∞) a : ℝ≥0∞)

Tactic:
rw [Finset.sum_range_succ, IH, eapproxDiff, coe_map, Function.comp_apply,
      coe_sub, Pi.sub_apply, ENNReal.coe_toNNReal,
      add_tsub_cancel_of_le (monotone_eapprox f (Nat.le_succ _) _)]

Premises used: ENNReal.coe_toNNReal, MeasureTheory.SimpleFunc.coe_map, Nat.le_succ, MeasureTheory.SimpleFunc.eapproxDiff, MeasureTheory.SimpleFunc.monotone_eapprox, MeasureTheory.SimpleFunc.coe_sub, Function.comp_apply, Finset.sum_range_succ, add_tsub_cancel_of_le, Pi.sub_apply
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_1
inst : MeasurableSpace α
f : α → ℝ≥0∞
a : α
n : ℕ
IH :
  Eq (α := ℝ≥0∞) (∑ k ∈ Finset.range (n + 1), (↑(((eapproxDiff f k : α →ₛ ℝ≥0) : (a : α) → ℝ≥0) a) : ℝ≥0∞) : ℝ≥0∞)
    (((eapprox f n : α →ₛ ℝ≥0∞) : (a : α) → ℝ≥0∞) a : ℝ≥0∞)
apply :
  HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) (((eapprox f (n + 1) : α →ₛ ℝ≥0∞) : (a : α) → ℝ≥0∞) a : ℝ≥0∞)
      (((eapprox f n : α →ₛ ℝ≥0∞) : (a : α) → ℝ≥0∞) a : ℝ≥0∞) ≤
    ((eapprox f (n + 1) : α →ₛ ℝ≥0∞) : (a : α) → ℝ≥0∞) a
⊢ HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) (((eapprox f (n + 1) : α →ₛ ℝ≥0∞) : (a : α) → ℝ≥0∞) a : ℝ≥0∞)
      (((eapprox f n : α →ₛ ℝ≥0∞) : (a : α) → ℝ≥0∞) a : ℝ≥0∞) ≠
    ∞

Tactic:
apply (lt_of_le_of_lt _ (eapprox_lt_top f (n + 1) a)).ne

Premises used: lt_of_le_of_lt, HAdd.hAdd, MeasureTheory.SimpleFunc.eapprox_lt_top, OfNat.ofNat, LT.lt.ne
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_1
inst : MeasurableSpace α
f : α → ℝ≥0∞
a : α
n : ℕ
IH :
  Eq (α := ℝ≥0∞) (∑ k ∈ Finset.range (n + 1), (↑(((eapproxDiff f k : α →ₛ ℝ≥0) : (a : α) → ℝ≥0) a) : ℝ≥0∞) : ℝ≥0∞)
    (((eapprox f n : α →ₛ ℝ≥0∞) : (a : α) → ℝ≥0∞) a : ℝ≥0∞)
rw :
  ((eapprox f (n + 1) : α →ₛ ℝ≥0∞) : (a : α) → ℝ≥0∞) a ≤
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) (((eapprox f (n + 1) : α →ₛ ℝ≥0∞) : (a : α) → ℝ≥0∞) a : ℝ≥0∞)
      (((eapprox f n : α →ₛ ℝ≥0∞) : (a : α) → ℝ≥0∞) a : ℝ≥0∞)
⊢ HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) (((eapprox f (n + 1) : α →ₛ ℝ≥0∞) : (a : α) → ℝ≥0∞) a : ℝ≥0∞)
      (((eapprox f n : α →ₛ ℝ≥0∞) : (a : α) → ℝ≥0∞) a : ℝ≥0∞) ≤
    ((eapprox f (n + 1) : α →ₛ ℝ≥0∞) : (a : α) → ℝ≥0∞) a

Tactic:
rw [tsub_le_iff_right]

Premises used: tsub_le_iff_right
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_1
inst : MeasurableSpace α
f : α → ℝ≥0∞
a : α
n : ℕ
IH :
  Eq (α := ℝ≥0∞) (∑ k ∈ Finset.range (n + 1), (↑(((eapproxDiff f k : α →ₛ ℝ≥0) : (a : α) → ℝ≥0) a) : ℝ≥0∞) : ℝ≥0∞)
    (((eapprox f n : α →ₛ ℝ≥0∞) : (a : α) → ℝ≥0∞) a : ℝ≥0∞)
⊢ ((eapprox f (n + 1) : α →ₛ ℝ≥0∞) : (a : α) → ℝ≥0∞) a ≤
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) (((eapprox f (n + 1) : α →ₛ ℝ≥0∞) : (a : α) → ℝ≥0∞) a : ℝ≥0∞)
      (((eapprox f n : α →ₛ ℝ≥0∞) : (a : α) → ℝ≥0∞) a : ℝ≥0∞)

Tactic:
le_self_add

Premises used: le_self_add
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_1
inst : MeasurableSpace α
f : α → ℝ≥0∞
a : α
n : ℕ
IH :
  Eq (α := ℝ≥0∞) (∑ k ∈ Finset.range (n + 1), (↑(((eapproxDiff f k : α →ₛ ℝ≥0) : (a : α) → ℝ≥0) a) : ℝ≥0∞) : ℝ≥0∞)
    (((eapprox f n : α →ₛ ℝ≥0∞) : (a : α) → ℝ≥0∞) a : ℝ≥0∞)
⊢ ((eapprox f (n + 1) : α →ₛ ℝ≥0∞) : (a : α) → ℝ≥0∞) a ≤
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) (((eapprox f (n + 1) : α →ₛ ℝ≥0∞) : (a : α) → ℝ≥0∞) a : ℝ≥0∞)
      (((eapprox f n : α →ₛ ℝ≥0∞) : (a : α) → ℝ≥0∞) a : ℝ≥0∞)

Tactic:
exact le_self_add

Premises used: le_self_add
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_1
inst : MeasurableSpace α
f : α → ℝ≥0∞
n : ℕ
a : α
zero :
  Eq (α := ℝ≥0∞)
    (∑ k ∈ Finset.range (HAdd.hAdd (α := ℕ) 0 1), (↑(((eapproxDiff f k : α →ₛ ℝ≥0) : (a : α) → ℝ≥0) a) : ℝ≥0∞) : ℝ≥0∞)
    (((eapprox f 0 : α →ₛ ℝ≥0∞) : (a : α) → ℝ≥0∞) a : ℝ≥0∞)
succ :
  ∀ (n : ℕ)
    (IH :
      Eq (α := ℝ≥0∞) (∑ k ∈ Finset.range (n + 1), (↑(((eapproxDiff f k : α →ₛ ℝ≥0) : (a : α) → ℝ≥0) a) : ℝ≥0∞) : ℝ≥0∞)
        (((eapprox f n : α →ₛ ℝ≥0∞) : (a : α) → ℝ≥0∞) a : ℝ≥0∞)),
    Eq (α := ℝ≥0∞) (∑ k ∈ Finset.range (n + 1 + 1), (↑(((eapproxDiff f k : α →ₛ ℝ≥0) : (a : α) → ℝ≥0) a) : ℝ≥0∞) : ℝ≥0∞)
      (((eapprox f (n + 1) : α →ₛ ℝ≥0∞) : (a : α) → ℝ≥0∞) a : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) (∑ k ∈ Finset.range (n + 1), (↑(((eapproxDiff f k : α →ₛ ℝ≥0) : (a : α) → ℝ≥0) a) : ℝ≥0∞) : ℝ≥0∞)
    (((eapprox f n : α →ₛ ℝ≥0∞) : (a : α) → ℝ≥0∞) a : ℝ≥0∞)

Tactic:
induction n with
  | zero =>
    simp [eapproxDiff, (eapprox_lt_top f 0 a).ne]
  | succ n IH =>
    rw [Finset.sum_range_succ, IH, eapproxDiff, coe_map, Function.comp_apply,
      coe_sub, Pi.sub_apply, ENNReal.coe_toNNReal,
      add_tsub_cancel_of_le (monotone_eapprox f (Nat.le_succ _) _)]
    apply (lt_of_le_of_lt _ (eapprox_lt_top f (n + 1) a)).ne
    rw [tsub_le_iff_right]
    exact le_self_add

Premises used: ENNReal.coe_toNNReal, lt_of_le_of_lt, MeasureTheory.SimpleFunc.coe_map, Nat.le_succ, tsub_le_iff_right, MeasureTheory.SimpleFunc.eapproxDiff, MeasureTheory.SimpleFunc.monotone_eapprox, HAdd.hAdd, MeasureTheory.SimpleFunc.coe_sub, Function.comp_apply, MeasureTheory.SimpleFunc.eapprox_lt_top, OfNat.ofNat, le_self_add, Finset.sum_range_succ, add_tsub_cancel_of_le, LT.lt.ne, Pi.sub_apply
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_1
inst : MeasurableSpace α
f : α → ℝ≥0∞
hf : Measurable f
a : α
simp_rw : ⨆ (i : ℕ), ∑ n ∈ Finset.range (i + 1), (↑(((eapproxDiff f n : α →ₛ ℝ≥0) : (a : α) → ℝ≥0) a) : ℝ≥0∞) = f a
simp_rw₁ : ⨆ (i : ℕ), ((eapprox f i : α →ₛ ℝ≥0∞) : (a : α) → ℝ≥0∞) a = f a
⊢ ∑' (n : ℕ), (↑(((eapproxDiff f n : α →ₛ ℝ≥0) : (a : α) → ℝ≥0) a) : ℝ≥0∞) = f a

Tactic:
simp_rw [ENNReal.tsum_eq_iSup_nat' (tendsto_add_atTop_nat 1), sum_eapproxDiff,
    iSup_eapprox_apply hf a]

Premises used: ENNReal.tsum_eq_iSup_nat', MeasureTheory.SimpleFunc.sum_eapproxDiff, MeasureTheory.SimpleFunc.iSup_eapprox_apply, Filter.tendsto_add_atTop_nat, OfNat.ofNat
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α →ₛ ℝ≥0∞
s : Finset ℝ≥0∞
hs :
  ∀ (x : α),
    Ne (α := ℝ≥0∞) ((f : (a : α) → ℝ≥0∞) x : ℝ≥0∞) (0 : ℝ≥0∞) →
      Ne (α := ℝ≥0∞)
          ((μ : (a : Set α) → ℝ≥0∞)
              (preimage (β := ℝ≥0∞) (⇑f : (a : α) → ℝ≥0∞) (singleton (α := ℝ≥0∞) ((f : (a : α) → ℝ≥0∞) x : ℝ≥0∞))) :
            ℝ≥0∞)
          (0 : ℝ≥0∞) →
        Membership.mem (α := ℝ≥0∞) s ((f : (a : α) → ℝ≥0∞) x : ℝ≥0∞)
⊢ f.lintegral μ =
    ∑ x ∈ s, HMul.hMul (β := ℝ≥0∞) x ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := ℝ≥0∞) (⇑f : (a : α) → ℝ≥0∞) {x}) : ℝ≥0∞)

Tactic:
Finset.sum_bij_ne_zero (fun r _ _ => r) ?_ ?_ ?_ ?_

Premises used: MeasureTheory.SimpleFunc.lintegral, Finset.sum_bij_ne_zero
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α →ₛ ℝ≥0∞
s : Finset ℝ≥0∞
hs :
  ∀ (x : α),
    Ne (α := ℝ≥0∞) ((f : (a : α) → ℝ≥0∞) x : ℝ≥0∞) (0 : ℝ≥0∞) →
      Ne (α := ℝ≥0∞)
          ((μ : (a : Set α) → ℝ≥0∞)
              (preimage (β := ℝ≥0∞) (⇑f : (a : α) → ℝ≥0∞) (singleton (α := ℝ≥0∞) ((f : (a : α) → ℝ≥0∞) x : ℝ≥0∞))) :
            ℝ≥0∞)
          (0 : ℝ≥0∞) →
        Membership.mem (α := ℝ≥0∞) s ((f : (a : α) → ℝ≥0∞) x : ℝ≥0∞)
⊢ ∀ (a : ℝ≥0∞) (h₁ : a ∈ f.range)
    (h₂ :
      HMul.hMul (β := ℝ≥0∞) a ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := ℝ≥0∞) (⇑f : (a : α) → ℝ≥0∞) {a}) : ℝ≥0∞) ≠ 0),
    (fun (r : ℝ≥0∞) (x : r ∈ f.range)
            (x_1 :
              HMul.hMul (β := ℝ≥0∞) r
                  ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := ℝ≥0∞) (⇑f : (a : α) → ℝ≥0∞) {r}) : ℝ≥0∞) ≠
                0) ↦
          r)
        a h₁ h₂ ∈
      s

Tactic:
simpa only [forall_mem_range, mul_ne_zero_iff, and_imp]

Premises used: MeasureTheory.SimpleFunc.forall_mem_range, and_imp, mul_ne_zero_iff