awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.EssSup (hypothesis)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : ConditionallyCompleteLattice β
γ : Type u_3
mγ : MeasurableSpace γ
f : α → γ
g : γ → β
inst_1 : MeasurableSpace β
inst_2 : TopologicalSpace β
inst_3 : SecondCountableTopology β
inst_4 : OrderClosedTopology β
inst_5 : OpensMeasurableSpace β
hg : AEMeasurable (_m := mγ) g (Measure.map f μ)
hf : AEMeasurable f μ
hg_co : IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) (ae (F := Measure γ) (Measure.map f μ)) g
hgf : IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) (ae μ) (g ∘ f)
hgf_co : IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) (ae μ) (g ∘ f)
hg_bdd : IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) (ae (F := Measure γ) (Measure.map f μ)) g
hg_mk_co : IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) (ae (F := Measure γ) (Measure.map f μ)) (AEMeasurable.mk g hg)
hg_mk_bdd : IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) (ae (F := Measure γ) (Measure.map f μ)) (AEMeasurable.mk g hg)
h_eq : g ∘ f =ᶠ[ae μ] AEMeasurable.mk g hg ∘ f
hg_mk_f : IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) (ae μ) (AEMeasurable.mk g hg ∘ f)
⊢ @essSup _ _ _ mγ g (Measure.map f μ) = essSup (g ∘ f) μ
have hg_mk_f_co : IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) (ae μ) (AEMeasurable.mk g hg ∘ f)
Tactic: have hg_mk_f_co : IsCoboundedUnder (· ≤ ·) (ae μ) ((hg.mk g) ∘ f) := by
    simpa [IsCoboundedUnder, ← map_congr h_eq]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.EssSup (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : ConditionallyCompleteLattice β
γ : Type u_3
mγ : MeasurableSpace γ
f : α → γ
g : γ → β
inst_1 : MeasurableSpace β
inst_2 : TopologicalSpace β
inst_3 : SecondCountableTopology β
inst_4 : OrderClosedTopology β
inst_5 : OpensMeasurableSpace β
hg : AEMeasurable (_m := mγ) g (Measure.map f μ)
hf : AEMeasurable f μ
hg_co : IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) (ae (F := Measure γ) (Measure.map f μ)) g
hgf : IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) (ae μ) (g ∘ f)
hgf_co : IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) (ae μ) (g ∘ f)
hg_bdd : IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) (ae (F := Measure γ) (Measure.map f μ)) g
hg_mk_co : IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) (ae (F := Measure γ) (Measure.map f μ)) (AEMeasurable.mk g hg)
hg_mk_bdd : IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) (ae (F := Measure γ) (Measure.map f μ)) (AEMeasurable.mk g hg)
h_eq : g ∘ f =ᶠ[ae μ] AEMeasurable.mk g hg ∘ f
hg_mk_f : IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) (ae μ) (AEMeasurable.mk g hg ∘ f)
hg_mk_f_co : IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) (ae μ) (AEMeasurable.mk g hg ∘ f)
⊢ @essSup _ _ _ mγ g (Measure.map f μ) = essSup (g ∘ f) μ
have rw : essSup (AEMeasurable.mk g hg ∘ f) μ = essSup (g ∘ f) μ
Tactic: rw [essSup_congr_ae hg.ae_eq_mk,
    essSup_map_measure_of_measurable hg.measurable_mk hf hg_mk_co hg_mk_f hg_mk_f_co hg_mk_bdd]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.EssSup (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : ConditionallyCompleteLattice β
f : α → β
inst_1 : Nonempty α
hμ : ∀ (a : α), Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a} : ℝ≥0∞) (0 : ℝ≥0∞)
hf : BddAbove (range f)
⊢ essSup f μ = ⨆ (a : α), f a
have rw : limsup f (ae μ) = ⨆ (a : α), f a
Tactic: rw [essSup, ae_eq_top.2 hμ, limsup_top_eq_ciSup hf]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.EssSup (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : ConditionallyCompleteLattice β
f : α → β
inst_1 : Nonempty α
hμ : ∀ (a : α), Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a} : ℝ≥0∞) (0 : ℝ≥0∞)
hf : BddAbove (range f)
rw : limsup f (ae μ) = ⨆ (a : α), f a
⊢ essSup f μ = ⨆ (a : α), f a
have rw₁ : limsup f ⊤ = ⨆ (a : α), f a
Tactic: rw [essSup, ae_eq_top.2 hμ, limsup_top_eq_ciSup hf]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.EssSup (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : ConditionallyCompleteLattice β
f : α → β
inst_1 : Nonempty α
hμ : ∀ (a : α), Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a} : ℝ≥0∞) (0 : ℝ≥0∞)
hf : BddAbove (range f)
rw : limsup f (ae μ) = ⨆ (a : α), f a
rw₁ : limsup f ⊤ = ⨆ (a : α), f a
⊢ essSup f μ = ⨆ (a : α), f a
have rw₂ : Eq.{u_2 + 1} (α := β) (⨆ (i : α), f i) (⨆ (a : α), f a)
Tactic: rw [essSup, ae_eq_top.2 hμ, limsup_top_eq_ciSup hf]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.EssSup (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : ConditionallyCompleteLattice β
f : α → β
inst_1 : Nonempty α
hμ : ∀ (a : α), Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a} : ℝ≥0∞) (0 : ℝ≥0∞)
hf : BddBelow (range f)
⊢ essInf f μ = ⨅ (a : α), f a
have rw : liminf f (ae μ) = ⨅ (a : α), f a
Tactic: rw [essInf, ae_eq_top.2 hμ, liminf_top_eq_ciInf hf]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.EssSup (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : ConditionallyCompleteLattice β
f : α → β
inst_1 : Nonempty α
hμ : ∀ (a : α), Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a} : ℝ≥0∞) (0 : ℝ≥0∞)
hf : BddBelow (range f)
rw : liminf f (ae μ) = ⨅ (a : α), f a
⊢ essInf f μ = ⨅ (a : α), f a
have rw₁ : liminf f ⊤ = ⨅ (a : α), f a
Tactic: rw [essInf, ae_eq_top.2 hμ, liminf_top_eq_ciInf hf]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.EssSup (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : ConditionallyCompleteLattice β
f : α → β
inst_1 : Nonempty α
hμ : ∀ (a : α), Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a} : ℝ≥0∞) (0 : ℝ≥0∞)
hf : BddBelow (range f)
rw : liminf f (ae μ) = ⨅ (a : α), f a
rw₁ : liminf f ⊤ = ⨅ (a : α), f a
⊢ essInf f μ = ⨅ (a : α), f a
have rw₂ : Eq.{u_2 + 1} (α := β) (⨅ (i : α), f i) (⨅ (a : α), f a)
Tactic: rw [essInf, ae_eq_top.2 hμ, liminf_top_eq_ciInf hf]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.EssSup (goal)
Goal:
α : Type u_1
β : Type u_2
inst : ConditionallyCompleteLinearOrder β
m : MeasurableSpace α
μ : Measure α
f : α → β
⊢ essSup f μ = sInf {a : β | Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | a < f x} : ℝ≥0∞) (0 : ℝ≥0∞)}
have dsimp : Eq.{u_2 + 1} (α := β) (sInf {a : β | ∀ᶠ (n : β) in map f (ae μ), n ≤ a})
  (sInf {a : β | Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | a < f x} : ℝ≥0∞) (0 : ℝ≥0∞)})
Tactic: dsimp [essSup, limsup, limsSup]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.EssSup (goal)
Goal:
α : Type u_1
β : Type u_2
inst : ConditionallyCompleteLinearOrder β
m : MeasurableSpace α
μ : Measure α
f : α → β
⊢ essInf f μ = sSup {a : β | Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | f x < a} : ℝ≥0∞) (0 : ℝ≥0∞)}
have dsimp : Eq.{u_2 + 1} (α := β) (sSup {a : β | ∀ᶠ (n : β) in map f (ae μ), a ≤ n})
  (sSup {a : β | Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | f x < a} : ℝ≥0∞) (0 : ℝ≥0∞)})
Tactic: dsimp [essInf, liminf, limsInf]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.EssSup (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : ConditionallyCompleteLinearOrder β
f : α → β
inst_1 : TopologicalSpace β
inst_2 : FirstCountableTopology β
inst_3 : OrderTopology β
hf : IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) (ae μ) f
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {y : α | essSup f μ < f y} : ℝ≥0∞) (0 : ℝ≥0∞)
have simp_rw : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {y : α | ¬f y ≤ essSup f μ} : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: simp_rw [← not_le]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.EssSup (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : ConditionallyCompleteLinearOrder β
f : α → β
inst_1 : TopologicalSpace β
inst_2 : FirstCountableTopology β
inst_3 : OrderTopology β
hf : IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≥ x2) (ae μ) f
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {y : α | f y < essInf f μ} : ℝ≥0∞) (0 : ℝ≥0∞)
have simp_rw : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {y : α | ¬essInf f μ ≤ f y} : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: simp_rw [← not_le]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.EssSup (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : CompleteLattice β
hμ : ∀ (a : α), Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a} : ℝ≥0∞) (0 : ℝ≥0∞)
f : α → β
⊢ essSup f μ = ⨆ (i : α), f i
have rw : limsup f (ae μ) = ⨆ (i : α), f i
Tactic: rw [essSup, ae_eq_top.2 hμ, limsup_top_eq_iSup]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.EssSup (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : CompleteLattice β
hμ : ∀ (a : α), Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a} : ℝ≥0∞) (0 : ℝ≥0∞)
f : α → β
rw : limsup f (ae μ) = ⨆ (i : α), f i
⊢ essSup f μ = ⨆ (i : α), f i
have rw₁ : limsup f ⊤ = ⨆ (i : α), f i
Tactic: rw [essSup, ae_eq_top.2 hμ, limsup_top_eq_iSup]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.EssSup (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : CompleteLattice β
hμ : ∀ (a : α), Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a} : ℝ≥0∞) (0 : ℝ≥0∞)
f : α → β
rw : limsup f (ae μ) = ⨆ (i : α), f i
rw₁ : limsup f ⊤ = ⨆ (i : α), f i
⊢ essSup f μ = ⨆ (i : α), f i
have rw₂ : Eq.{u_2 + 1} (α := β) (⨆ (i : α), f i) (⨆ (i : α), f i)
Tactic: rw [essSup, ae_eq_top.2 hμ, limsup_top_eq_iSup]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.EssSup (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : CompleteLattice β
hμ : ∀ (a : α), Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a} : ℝ≥0∞) (0 : ℝ≥0∞)
f : α → β
⊢ essInf f μ = ⨅ (i : α), f i
have rw : liminf f (ae μ) = ⨅ (i : α), f i
Tactic: rw [essInf, ae_eq_top.2 hμ, liminf_top_eq_iInf]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.EssSup (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : CompleteLattice β
hμ : ∀ (a : α), Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a} : ℝ≥0∞) (0 : ℝ≥0∞)
f : α → β
rw : liminf f (ae μ) = ⨅ (i : α), f i
⊢ essInf f μ = ⨅ (i : α), f i
have rw₁ : liminf f ⊤ = ⨅ (i : α), f i
Tactic: rw [essInf, ae_eq_top.2 hμ, liminf_top_eq_iInf]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.EssSup (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : CompleteLattice β
hμ : ∀ (a : α), Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a} : ℝ≥0∞) (0 : ℝ≥0∞)
f : α → β
rw : liminf f (ae μ) = ⨅ (i : α), f i
rw₁ : liminf f ⊤ = ⨅ (i : α), f i
⊢ essInf f μ = ⨅ (i : α), f i
have rw₂ : Eq.{u_2 + 1} (α := β) (⨅ (i : α), f i) (⨅ (i : α), f i)
Tactic: rw [essInf, ae_eq_top.2 hμ, liminf_top_eq_iInf]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.EssSup (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
s : Set α
inst : DecidablePred fun (x : α) ↦ x ∈ s
g : (i : α) → ℝ≥0∞
hs : MeasurableSet s
⊢ essSup (s.piecewise (β := fun (a : α) ↦ ℝ≥0∞) f g) μ = max (essSup f (μ.restrict s)) (essSup g (μ.restrict sᶜ))
have simp : max (limsup f (ae μ ⊓ 𝓟 {x : α | x ∈ s})) (limsup g (ae μ ⊓ 𝓟 {x : α | x ∉ s})) =
  max (limsup f (ae μ ⊓ 𝓟 s)) (limsup g (ae μ ⊓ 𝓟 sᶜ))
Tactic: simp only [essSup, limsup_piecewise, blimsup_eq_limsup, ae_restrict_eq, hs, hs.compl]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.EssSup (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : Set α
f : α → ℝ≥0∞
hs : MeasurableSet s
⊢ essSup (s.indicator f) μ = essSup f (μ.restrict s)
have simp : essSup 0 (μ.restrict sᶜ) ≤ essSup f (μ.restrict s)
Tactic: simp only [← piecewise_eq_indicator, essSup_piecewise hs, max_eq_left_iff]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.EssSup (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : Set α
f : α → ℝ≥0∞
hs : MeasurableSet s
⊢ essSup (s.indicator f) μ = essSup f (μ.restrict s)
have simp : essSup 0 (μ.restrict sᶜ) ≤ essSup f (μ.restrict s)
Tactic: classical
  simp only [← piecewise_eq_indicator, essSup_piecewise hs, max_eq_left_iff]
  exact limsup_const_bot.trans_le zero_le
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.EssSup (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0
hf : IsBoundedUnder (fun (x1 x2 : ℝ≥0) ↦ x1 ≤ x2) (ae μ) f
r : ℝ≥0∞
⊢ r ≤
      ⨅ (a : ℝ≥0),
        ⨅ (_ :
          Membership.mem (γ := Set ℝ≥0)
            (fun (x : ℝ≥0) ↦
              (map f (ae μ)).sets {x_1 : ℝ≥0 | (fun (x_2 : ℝ≥0) ↦ ((fun (x1 x2 : ℝ≥0) ↦ x1 ≤ x2) x_2 x : Prop)) x_1})
            a),
          (↑a : ℝ≥0∞) ↔
    r ≤ essSup (fun (x : α) ↦ (↑(f x) : ℝ≥0∞)) μ
have simp : (∀ (i : ℝ≥0) (i_1 : Membership.mem (γ := Set ℝ≥0) (fun (x : ℝ≥0) ↦ (map f (ae μ)).sets {x_1 : ℝ≥0 | x_1 ≤ x}) i),
    r ≤ (↑i : ℝ≥0∞)) ↔
  ∀ (r_1 : ℝ≥0), (∀ᵐ (a : α) ∂μ, f a ≤ r_1) → r ≤ (↑r_1 : ℝ≥0∞)
Tactic: simp [essSup, limsup, limsSup, eventually_map, ENNReal.forall_ennreal]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.EssSup (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
h₁ : ∀ᵐ (a : α) ∂μ, f a ≠ ∞
h₂ : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) (ae μ) fun (i : α) ↦ (f i).toReal
⊢ (essSup f μ).toReal = essSup (fun (a : α) ↦ (f a).toReal) μ
have inl : ∀ (h₁ : ∀ᵐ (a : α) ∂0, f a ≠ ∞)
  (h₂ : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) (ae (F := Measure α) 0) fun (i : α) ↦ (f i).toReal),
  (@essSup _ _ _ m f 0).toReal = @essSup _ _ _ m (fun (a : α) ↦ (f a).toReal) 0
Tactic: obtain rfl | hμ := eq_zero_or_neZero μ
Cleared hypotheses: μ, h₁, h₂
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.EssSup (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
h₁ : ∀ᵐ (a : α) ∂μ, f a ≠ ∞
h₂ : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) (ae μ) fun (i : α) ↦ (f i).toReal
inl :
  ∀ (h₁ : ∀ᵐ (a : α) ∂0, f a ≠ ∞)
    (h₂ : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) (ae (F := Measure α) 0) fun (i : α) ↦ (f i).toReal),
    (@essSup _ _ _ m f 0).toReal = @essSup _ _ _ m (fun (a : α) ↦ (f a).toReal) 0
⊢ (essSup f μ).toReal = essSup (fun (a : α) ↦ (f a).toReal) μ
have inr : ∀ (hμ : NeZero μ), (essSup f μ).toReal = essSup (fun (a : α) ↦ (f a).toReal) μ
Tactic: obtain rfl | hμ := eq_zero_or_neZero μ
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.EssSup (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : Set α
f : α → ℝ≥0∞
hsf : Function.support f ⊆ s
⊢ essSup f (μ.restrict s) = essSup f μ
have apply : essSup f μ ≤ essSup f (μ.restrict s)
Tactic: apply le_antisymm (essSup_mono_measure' Measure.restrict_le_self)
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.EssSup (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : Set α
f : α → ℝ≥0∞
hsf : Function.support f ⊆ s
⊢ essSup f μ ≤ essSup f (μ.restrict s)
have apply : ∀ (c : ℝ≥0∞) (hc : c < essSup f μ), c < essSup f (μ.restrict s)
Tactic: apply le_of_forall_lt (fun c hc ↦ ?_)
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.EssSup (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : Set α
f : α → ℝ≥0∞
hsf : Function.support f ⊆ s
c : ℝ≥0∞
hc : c < essSup f μ
⊢ c < essSup f (μ.restrict s)
have obtain : ∀ (d : ℝ≥0∞) (cd : c < d) (hd : d < essSup f μ), c < essSup f (μ.restrict s)
Tactic: obtain ⟨d, cd, hd⟩ : ∃ d, c < d ∧ d < essSup f μ := exists_between hc
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.EssSup (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : Set α
f : α → ℝ≥0∞
hsf : Function.support f ⊆ s
c : ℝ≥0∞
hc : c < essSup f μ
d : ℝ≥0∞
cd : c < d
hd : d < essSup f μ
t : Set α := {x : α | d < f x}
⊢ LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ.restrict t : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
have simp : LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
Tactic: simp only [Measure.restrict_apply_self]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.EssSup (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : Set α
f : α → ℝ≥0∞
hsf : Function.support f ⊆ s
c : ℝ≥0∞
hc : c < essSup f μ
d : ℝ≥0∞
cd : c < d
hd : d < essSup f μ
t : Set α := {x : α | d < f x}
⊢ LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
have rw : ∀ (hd : d < sInf {a : ℝ≥0∞ | Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | a < f x} : ℝ≥0∞) (0 : ℝ≥0∞)}),
  let t : Set α := {x : α | d < f x};
  LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
Tactic: rw [essSup_eq_sInf] at hd
Cleared hypotheses: hd, t
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.EssSup (hypothesis)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : Set α
f : α → ℝ≥0∞
hsf : Function.support f ⊆ s
c : ℝ≥0∞
hc : c < essSup f μ
d : ℝ≥0∞
cd : c < d
hd : d < sInf {a : ℝ≥0∞ | Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | a < f x} : ℝ≥0∞) (0 : ℝ≥0∞)}
t : Set α := {x : α | d < f x}
⊢ LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
have this : d ∉ {a : ℝ≥0∞ | Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | a < f x} : ℝ≥0∞) (0 : ℝ≥0∞)}
Tactic: have : d ∉ {a | μ {x | a < f x} = 0} := notMem_of_lt_csInf hd (OrderBot.bddBelow _)
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.EssSup (hypothesis)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : Set α
f : α → ℝ≥0∞
hsf : Function.support f ⊆ s
c : ℝ≥0∞
hc : c < essSup f μ
d : ℝ≥0∞
cd : c < d
hd : d < essSup f μ
t : Set α := {x : α | d < f x}
⊢ c < essSup f (μ.restrict s)
have A : LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ.restrict t : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
Tactic: have A : 0 < (μ.restrict t) t := by
    simp only [Measure.restrict_apply_self]
    rw [essSup_eq_sInf] at hd
    have : d ∉ {a | μ {x | a < f x} = 0} := notMem_of_lt_csInf hd (OrderBot.bddBelow _)
    exact bot_lt_iff_ne_bot.2 this
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.EssSup (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : Set α
f : α → ℝ≥0∞
hsf : Function.support f ⊆ s
c : ℝ≥0∞
hc : c < essSup f μ
d : ℝ≥0∞
cd : c < d
hd : d < essSup f μ
t : Set α := {x : α | d < f x}
A : LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ.restrict t : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
⊢ μ.restrict t ≤ μ.restrict s
have apply : t ⊆ s
Tactic: apply Measure.restrict_mono _ le_rfl
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.EssSup (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : Set α
f : α → ℝ≥0∞
hsf : Function.support f ⊆ s
c : ℝ≥0∞
hc : c < essSup f μ
d : ℝ≥0∞
cd : c < d
hd : d < essSup f μ
t : Set α := {x : α | d < f x}
A : LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ.restrict t : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
⊢ t ⊆ s
have apply : t ⊆ Function.support f
Tactic: apply subset_trans _ hsf
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.EssSup (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : Set α
f : α → ℝ≥0∞
hsf : Function.support f ⊆ s
c : ℝ≥0∞
hc : c < essSup f μ
d : ℝ≥0∞
cd : c < d
hd : d < essSup f μ
t : Set α := {x : α | d < f x}
A : LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ.restrict t : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
x : α
⊢ x ∈ t → x ∈ Function.support f
have d₁ : ∀ (hx : d < f x), x ∈ Function.support f
Tactic: (hx : d < f x)
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.EssSup (hypothesis)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : Set α
f : α → ℝ≥0∞
hsf : Function.support f ⊆ s
c : ℝ≥0∞
hc : c < essSup f μ
d : ℝ≥0∞
cd : c < d
hd : d < essSup f μ
t : Set α := {x : α | d < f x}
A : LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ.restrict t : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
⊢ LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ.restrict s : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
have this : μ.restrict t ≤ μ.restrict s
Tactic: have : μ.restrict t ≤ μ.restrict s := by
      apply Measure.restrict_mono _ le_rfl
      apply subset_trans _ hsf
      intro x (hx : d < f x)
      exact (lt_of_le_of_lt bot_le hx).ne'
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.EssSup (hypothesis)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : Set α
f : α → ℝ≥0∞
hsf : Function.support f ⊆ s
c : ℝ≥0∞
hc : c < essSup f μ
d : ℝ≥0∞
cd : c < d
hd : d < essSup f μ
t : Set α := {x : α | d < f x}
A : LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ.restrict t : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
⊢ c < essSup f (μ.restrict s)
have B : LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ.restrict s : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
Tactic: have B : 0 < (μ.restrict s) t := by
    have : μ.restrict t ≤ μ.restrict s := by
      apply Measure.restrict_mono _ le_rfl
      apply subset_trans _ hsf
      intro x (hx : d < f x)
      exact (lt_of_le_of_lt bot_le hx).ne'
    exact lt_of_lt_of_le A (this _)
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.EssSup (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : Set α
f : α → ℝ≥0∞
hsf : Function.support f ⊆ s
c : ℝ≥0∞
hc : c < essSup f μ
d : ℝ≥0∞
cd : c < d
hd : d < essSup f μ
t : Set α := {x : α | d < f x}
A : LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ.restrict t : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
B : LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ.restrict s : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
⊢ c < essSup f (μ.restrict s)
have apply : d ≤ essSup f (μ.restrict s)
Tactic: apply cd.trans_le
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.EssSup (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : Set α
f : α → ℝ≥0∞
hsf : Function.support f ⊆ s
c : ℝ≥0∞
hc : c < essSup f μ
d : ℝ≥0∞
cd : c < d
hd : d < essSup f μ
t : Set α := {x : α | d < f x}
A : LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ.restrict t : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
B : LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ.restrict s : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
⊢ d ≤ essSup f (μ.restrict s)
have rw : d ≤ sInf {a : ℝ≥0∞ | Eq (α := ℝ≥0∞) ((μ.restrict s : (a : Set α) → ℝ≥0∞) {x : α | a < f x} : ℝ≥0∞) (0 : ℝ≥0∞)}
Tactic: rw [essSup_eq_sInf]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.EssSup (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : Set α
f : α → ℝ≥0∞
hsf : Function.support f ⊆ s
c : ℝ≥0∞
hc : c < essSup f μ
d : ℝ≥0∞
cd : c < d
hd : d < essSup f μ
t : Set α := {x : α | d < f x}
A : LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ.restrict t : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
B : LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ.restrict s : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
⊢ d ≤ sInf {a : ℝ≥0∞ | Eq (α := ℝ≥0∞) ((μ.restrict s : (a : Set α) → ℝ≥0∞) {x : α | a < f x} : ℝ≥0∞) (0 : ℝ≥0∞)}
have apply : ∀ (b : ℝ≥0∞)
  (hb :
    Membership.mem (γ := Set ℝ≥0∞)
      {a : ℝ≥0∞ | Eq (α := ℝ≥0∞) ((μ.restrict s : (a : Set α) → ℝ≥0∞) {x : α | a < f x} : ℝ≥0∞) (0 : ℝ≥0∞)} b),
  d ≤ b
Tactic: apply le_sInf (fun b hb ↦ ?_)
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.EssSup (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : Set α
f : α → ℝ≥0∞
hsf : Function.support f ⊆ s
c : ℝ≥0∞
hc : c < essSup f μ
d : ℝ≥0∞
cd : c < d
hd : d < essSup f μ
t : Set α := {x : α | d < f x}
A : LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ.restrict t : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
B : LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ.restrict s : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
b : ℝ≥0∞
hb :
  Membership.mem (γ := Set ℝ≥0∞)
    {a : ℝ≥0∞ | Eq (α := ℝ≥0∞) ((μ.restrict s : (a : Set α) → ℝ≥0∞) {x : α | a < f x} : ℝ≥0∞) (0 : ℝ≥0∞)} b
⊢ d ≤ b
have contrapose! : ∀ (hb : b < d),
  b ∉ {a : ℝ≥0∞ | Eq (α := ℝ≥0∞) ((μ.restrict s : (a : Set α) → ℝ≥0∞) {x : α | a < f x} : ℝ≥0∞) (0 : ℝ≥0∞)}
Tactic: contrapose! hb
Cleared hypotheses: hb
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.FactorsThrough (goal)
Goal:
X : Type u_1
Y : Type u_2
Z : Type u_3
mY : MeasurableSpace Y
f : X → Y
g : X → Z
inst : MeasurableSpace Z
inst_1 : MeasurableSingletonClass Z
hg : Measurable g
⊢ Function.FactorsThrough g f
have refine : ∀ (x₁ x₂ : X) (h : f x₁ = f x₂), Membership.mem (γ := Set Z) {g x₂} (g x₁)
Tactic: refine fun x₁ x₂ h ↦ eq_of_mem_singleton ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.FactorsThrough (goal)
Goal:
X : Type u_1
Y : Type u_2
Z : Type u_3
mY : MeasurableSpace Y
f : X → Y
g : X → Z
inst : MeasurableSpace Z
inst_1 : MeasurableSingletonClass Z
hg : Measurable g
x₁ x₂ : X
h : f x₁ = f x₂
⊢ Membership.mem (γ := Set Z) {g x₂} (g x₁)
have obtain : ∀ (s : Set Y) (hs : f ⁻¹' s = g ⁻¹' {g x₂}), Membership.mem (γ := Set Z) {g x₂} (g x₁)
Tactic: obtain ⟨s, -, hs⟩ := hg (measurableSet_singleton (g x₂))
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.FactorsThrough (goal)
Goal:
X : Type u_1
Y : Type u_2
Z : Type u_3
mY : MeasurableSpace Y
f : X → Y
g : X → Z
inst : MeasurableSpace Z
inst_1 : MeasurableSingletonClass Z
hg : Measurable g
x₁ x₂ : X
h : f x₁ = f x₂
s : Set Y
hs : f ⁻¹' s = g ⁻¹' {g x₂}
⊢ Membership.mem (γ := Set Z) {g x₂} (g x₁)
have rw : x₁ ∈ g ⁻¹' {g x₂}
Tactic: rw [← mem_preimage, ← hs, mem_preimage, h, ← mem_preimage, hs, mem_preimage, mem_singleton_iff]