awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Function.EssSup
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst : CompleteLattice β
inst_1 : MeasurableSingletonClass α
f : α → β
⊢ ∀ (a : α), Ne (α := ℝ≥0∞) (((Measure.count : Measure α) : (a : Set α) → ℝ≥0∞) {a} : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Function.EssSup
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
s : Set α
inst : DecidablePred fun (x : α) ↦ x ∈ s
g : (i : α) → ℝ≥0∞
hs : MeasurableSet s
simp :
  max (limsup f (ae μ ⊓ 𝓟 {x : α | x ∈ s})) (limsup g (ae μ ⊓ 𝓟 {x : α | x ∉ s})) =
    max (limsup f (ae μ ⊓ 𝓟 s)) (limsup g (ae μ ⊓ 𝓟 sᶜ))
⊢ essSup (s.piecewise (β := fun (a : α) ↦ ℝ≥0∞) f g) μ = max (essSup f (μ.restrict s)) (essSup g (μ.restrict sᶜ))

Tactic:
simp only [essSup, limsup_piecewise, blimsup_eq_limsup, ae_restrict_eq, hs, hs.compl]

Premises used: Filter.blimsup_eq_limsup, MeasurableSet.compl, MeasureTheory.ae_restrict_eq, Filter.limsup_piecewise, essSup
-- Module: Mathlib.MeasureTheory.Function.EssSup
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
s : Set α
inst : DecidablePred fun (x : α) ↦ x ∈ s
g : (i : α) → ℝ≥0∞
hs : MeasurableSet s
⊢ max (limsup f (ae μ ⊓ 𝓟 {x : α | x ∈ s})) (limsup g (ae μ ⊓ 𝓟 {x : α | x ∉ s})) =
    max (limsup f (ae μ ⊓ 𝓟 s)) (limsup g (ae μ ⊓ 𝓟 sᶜ))

Tactic:
rfl
-- Module: Mathlib.MeasureTheory.Function.EssSup
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : Set α
f : α → ℝ≥0∞
hs : MeasurableSet s
simp : essSup 0 (μ.restrict sᶜ) ≤ essSup f (μ.restrict s)
⊢ essSup (s.indicator f) μ = essSup f (μ.restrict s)

Tactic:
simp only [← piecewise_eq_indicator, essSup_piecewise hs, max_eq_left_iff]

Premises used: ENNReal.essSup_piecewise, max_eq_left_iff, Set.piecewise_eq_indicator
-- Module: Mathlib.MeasureTheory.Function.EssSup
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : Set α
f : α → ℝ≥0∞
hs : MeasurableSet s
⊢ essSup 0 (μ.restrict sᶜ) ≤ essSup f (μ.restrict s)

Tactic:
limsup_const_bot.trans_le zero_le

Premises used: zero_le, Eq.trans_le, Filter.limsup_const_bot, essSup
-- Module: Mathlib.MeasureTheory.Function.EssSup
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : Set α
f : α → ℝ≥0∞
hs : MeasurableSet s
⊢ essSup 0 (μ.restrict sᶜ) ≤ essSup f (μ.restrict s)

Tactic:
exact limsup_const_bot.trans_le zero_le

Premises used: Eq.trans_le, Filter.limsup_const_bot
-- Module: Mathlib.MeasureTheory.Function.EssSup
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : Set α
f : α → ℝ≥0∞
hs : MeasurableSet s
simp : essSup 0 (μ.restrict sᶜ) ≤ essSup f (μ.restrict s)
⊢ essSup (s.indicator f) μ = 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

Premises used: max_eq_left_iff, Eq.trans_le, Filter.limsup_const_bot, Set.piecewise_eq_indicator
-- Module: Mathlib.MeasureTheory.Function.EssSup
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
⊢ ∀ᵐ (y : α) ∂μ, f y ≤ essSup f μ

Tactic:
eventually_le_limsup f

Premises used: ENNReal.eventually_le_limsup, essSup
-- Module: Mathlib.MeasureTheory.Function.EssSup
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
⊢ essSup f μ = 0 ↔ f =ᶠ[ae μ] 0

Tactic:
limsup_eq_zero_iff

Premises used: ENNReal.limsup_eq_zero_iff, essSup
-- Module: Mathlib.MeasureTheory.Function.EssSup
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
a : ℝ≥0∞
⊢ essSup (fun (x : α) ↦ a * f x) μ = a * essSup f μ

Tactic:
limsup_const_mul

Premises used: ENNReal.limsup_const_mul, essSup
-- Module: Mathlib.MeasureTheory.Function.EssSup
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
⊢ essSup (f * g) μ ≤ essSup f μ * essSup g μ

Tactic:
limsup_mul_le f g

Premises used: ENNReal.limsup_mul_le, essSup
-- Module: Mathlib.MeasureTheory.Function.EssSup
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
⊢ essSup (f + g) μ ≤ essSup f μ + essSup g μ

Tactic:
limsup_add_le f g

Premises used: ENNReal.limsup_add_le, essSup
-- Module: Mathlib.MeasureTheory.Function.EssSup
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ι : Type u_3
inst : Countable ι
inst_1 : Preorder ι
f : ι → α → ℝ≥0∞
⊢ LE.le (α := ℝ≥0∞) (limsup (fun (x : α) ↦ liminf (fun (n : ι) ↦ f n x) atTop) (ae μ))
    (liminf (fun (n : ι) ↦ limsup (fun (x : α) ↦ f n x) (ae μ)) atTop)

Tactic:
ENNReal.limsup_liminf_le_liminf_limsup fun a b => f b a

Premises used: ENNReal.limsup_liminf_le_liminf_limsup
-- Module: Mathlib.MeasureTheory.Function.EssSup
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ι : Type u_3
inst : Countable ι
inst_1 : Preorder ι
f : ι → α → ℝ≥0∞
⊢ LE.le (α := ℝ≥0∞) (limsup (fun (x : α) ↦ liminf (fun (n : ι) ↦ f n x) atTop) (ae μ))
    (liminf (fun (n : ι) ↦ limsup (fun (x : α) ↦ f n x) (ae μ)) atTop)

Tactic:
exact ENNReal.limsup_liminf_le_liminf_limsup fun a b => f b a

Premises used: ENNReal.limsup_liminf_le_liminf_limsup
-- Module: Mathlib.MeasureTheory.Function.EssSup
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0
hf : IsBoundedUnder (fun (x1 x2 : ℝ≥0) ↦ x1 ≤ x2) (ae μ) f
r : ℝ≥0∞
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∞)
⊢ 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∞)) μ

Tactic:
simp [essSup, limsup, limsSup, eventually_map, ENNReal.forall_ennreal]

Premises used: Filter.limsSup, Filter.eventually_map, Filter.limsup, essSup, ENNReal.forall_ennreal
-- Module: Mathlib.MeasureTheory.Function.EssSup
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0
hf : IsBoundedUnder (fun (x1 x2 : ℝ≥0) ↦ x1 ≤ x2) (ae μ) f
r : ℝ≥0∞
⊢ (∀ (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:
rfl
-- Module: Mathlib.MeasureTheory.Function.EssSup
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
h₁ : IsCoboundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) (ae μ) f
h₂ : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) (ae μ) f
⊢ ENNReal.ofReal (essSup f μ) = essSup (fun (a : α) ↦ ENNReal.ofReal (f a)) μ

Tactic:
ENNReal.ofReal_limsup

Premises used: ENNReal.ofReal_limsup, essSup
-- Module: Mathlib.MeasureTheory.Function.EssSup
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
inr : ∀ (hμ : NeZero μ), (essSup f μ).toReal = essSup (fun (a : α) ↦ (f a).toReal) μ
⊢ (essSup f μ).toReal = essSup (fun (a : α) ↦ (f a).toReal) μ

Tactic:
obtain rfl | hμ := eq_zero_or_neZero μ

Premises used: eq_zero_or_neZero, rfl
-- Module: Mathlib.MeasureTheory.Function.EssSup
Goal:
α : Type u_1
m : MeasurableSpace α
f : α → ℝ≥0∞
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:
simp [essSup, limsup, limsSup]

Premises used: Filter.limsSup, Filter.limsup, essSup
-- Module: Mathlib.MeasureTheory.Function.EssSup
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
hμ : NeZero μ
⊢ (essSup f μ).toReal = essSup (fun (a : α) ↦ (f a).toReal) μ

Tactic:
ENNReal.toReal_limsup h₁

Premises used: ENNReal.toReal_limsup, essSup
-- Module: Mathlib.MeasureTheory.Function.EssSup
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
hμ : NeZero μ
⊢ (essSup f μ).toReal = essSup (fun (a : α) ↦ (f a).toReal) μ

Tactic:
exact ENNReal.toReal_limsup h₁

Premises used: ENNReal.toReal_limsup
-- Module: Mathlib.MeasureTheory.Function.EssSup
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : Set α
f : α → ℝ≥0∞
hsf : Function.support f ⊆ s
apply : essSup f μ ≤ essSup f (μ.restrict s)
⊢ essSup f (μ.restrict s) = essSup f μ

Tactic:
apply le_antisymm (essSup_mono_measure' Measure.restrict_le_self)

Premises used: le_antisymm, MeasureTheory.Measure.restrict_le_self, essSup_mono_measure'
-- Module: Mathlib.MeasureTheory.Function.EssSup
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : Set α
f : α → ℝ≥0∞
hsf : Function.support f ⊆ s
apply : ∀ (c : ℝ≥0∞) (hc : c < essSup f μ), c < essSup f (μ.restrict s)
⊢ essSup f μ ≤ essSup f (μ.restrict s)

Tactic:
apply le_of_forall_lt (fun c hc ↦ ?_)

Premises used: le_of_forall_lt
-- Module: Mathlib.MeasureTheory.Function.EssSup
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : Set α
f : α → ℝ≥0∞
hsf : Function.support f ⊆ s
c : ℝ≥0∞
hc : c < essSup f μ
⊢ ∃ (d : ℝ≥0∞), c < d ∧ d < essSup f μ

Tactic:
exists_between hc

Premises used: exists_between
-- Module: Mathlib.MeasureTheory.Function.EssSup
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : Set α
f : α → ℝ≥0∞
hsf : Function.support f ⊆ s
c : ℝ≥0∞
hc : c < essSup f μ
obtain : ∀ (d : ℝ≥0∞) (cd : c < d) (hd : d < essSup f μ), c < essSup f (μ.restrict s)
⊢ c < essSup f (μ.restrict s)

Tactic:
obtain ⟨d, cd, hd⟩ : ∃ d, c < d ∧ d < essSup f μ := exists_between hc

Premises used: exists_between, essSup
-- Module: Mathlib.MeasureTheory.Function.EssSup
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}
simp : LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
⊢ LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ.restrict t : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)

Tactic:
simp only [Measure.restrict_apply_self]

Premises used: MeasureTheory.Measure.restrict_apply_self
-- Module: Mathlib.MeasureTheory.Function.EssSup
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}
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∞)
⊢ LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)

Tactic:
rw [essSup_eq_sInf] at hd

Premises used: essSup_eq_sInf
-- Module: Mathlib.MeasureTheory.Function.EssSup
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}
⊢ 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 _)
-- Module: Mathlib.MeasureTheory.Function.EssSup
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}
this : d ∉ {a : ℝ≥0∞ | Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | a < f x} : ℝ≥0∞) (0 : ℝ≥0∞)}
⊢ LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)

Tactic:
bot_lt_iff_ne_bot.2 this

Premises used: Iff.mpr, bot_lt_iff_ne_bot
-- Module: Mathlib.MeasureTheory.Function.EssSup
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}
this : d ∉ {a : ℝ≥0∞ | Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | a < f x} : ℝ≥0∞) (0 : ℝ≥0∞)}
⊢ LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)

Tactic:
exact bot_lt_iff_ne_bot.2 this

Premises used: Iff.mpr, bot_lt_iff_ne_bot
-- Module: Mathlib.MeasureTheory.Function.EssSup
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∞)

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
-- Module: Mathlib.MeasureTheory.Function.EssSup
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∞)
apply : t ⊆ s
⊢ μ.restrict t ≤ μ.restrict s

Tactic:
apply Measure.restrict_mono _ le_rfl

Premises used: le_rfl, MeasureTheory.Measure.restrict_mono
-- Module: Mathlib.MeasureTheory.Function.EssSup
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∞)
apply : t ⊆ Function.support f
⊢ t ⊆ s

Tactic:
apply subset_trans _ hsf

Premises used: subset_trans
-- Module: Mathlib.MeasureTheory.Function.EssSup
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 : α
d₁ : ∀ (hx : d < f x), x ∈ Function.support f
⊢ x ∈ t → x ∈ Function.support f

Tactic:
(hx : d < f x)
-- Module: Mathlib.MeasureTheory.Function.EssSup
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 : α
hx : d < f x
⊢ x ∈ Function.support f

Tactic:
(lt_of_le_of_lt bot_le hx).ne'

Premises used: lt_of_le_of_lt, Set.Mem, setOf, LT.lt.ne', Function.support, bot_le, Not
-- Module: Mathlib.MeasureTheory.Function.EssSup
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 : α
hx : d < f x
⊢ x ∈ Function.support f

Tactic:
exact (lt_of_le_of_lt bot_le hx).ne'

Premises used: lt_of_le_of_lt, LT.lt.ne', bot_le
-- Module: Mathlib.MeasureTheory.Function.EssSup
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

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'
-- Module: Mathlib.MeasureTheory.Function.EssSup
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∞)
this : μ.restrict t ≤ μ.restrict s
⊢ LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ.restrict s : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)

Tactic:
lt_of_lt_of_le A (this _)

Premises used: lt_of_lt_of_le
-- Module: Mathlib.MeasureTheory.Function.EssSup
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∞)
this : μ.restrict t ≤ μ.restrict s
⊢ LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ.restrict s : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)

Tactic:
exact lt_of_lt_of_le A (this _)

Premises used: lt_of_lt_of_le
-- Module: Mathlib.MeasureTheory.Function.EssSup
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∞)

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 _)
-- Module: Mathlib.MeasureTheory.Function.EssSup
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∞)
apply : d ≤ essSup f (μ.restrict s)
⊢ c < essSup f (μ.restrict s)

Tactic:
apply cd.trans_le

Premises used: LT.lt.trans_le
-- Module: Mathlib.MeasureTheory.Function.EssSup
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∞)
rw : d ≤ sInf {a : ℝ≥0∞ | Eq (α := ℝ≥0∞) ((μ.restrict s : (a : Set α) → ℝ≥0∞) {x : α | a < f x} : ℝ≥0∞) (0 : ℝ≥0∞)}
⊢ d ≤ essSup f (μ.restrict s)

Tactic:
rw [essSup_eq_sInf]

Premises used: essSup_eq_sInf
-- Module: Mathlib.MeasureTheory.Function.EssSup
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∞)
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
⊢ d ≤ sInf {a : ℝ≥0∞ | Eq (α := ℝ≥0∞) ((μ.restrict s : (a : Set α) → ℝ≥0∞) {x : α | a < f x} : ℝ≥0∞) (0 : ℝ≥0∞)}

Tactic:
apply le_sInf (fun b hb ↦ ?_)

Premises used: le_sInf
-- Module: Mathlib.MeasureTheory.Function.EssSup
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
contrapose! :
  ∀ (hb : b < d),
    b ∉ {a : ℝ≥0∞ | Eq (α := ℝ≥0∞) ((μ.restrict s : (a : Set α) → ℝ≥0∞) {x : α | a < f x} : ℝ≥0∞) (0 : ℝ≥0∞)}
⊢ d ≤ b

Tactic:
contrapose! hb
-- Module: Mathlib.MeasureTheory.Function.EssSup
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 : b < d
⊢ b ∉ {a : ℝ≥0∞ | Eq (α := ℝ≥0∞) ((μ.restrict s : (a : Set α) → ℝ≥0∞) {x : α | a < f x} : ℝ≥0∞) (0 : ℝ≥0∞)}

Tactic:
ne_of_gt (B.trans_le (measure_mono (fun x hx ↦ hb.trans hx)))

Premises used: Set.Mem, setOf, ne_of_gt, LT.lt.trans_le, MeasureTheory.measure_mono, LT.lt.trans
-- Module: Mathlib.MeasureTheory.Function.EssSup
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 : b < d
⊢ b ∉ {a : ℝ≥0∞ | Eq (α := ℝ≥0∞) ((μ.restrict s : (a : Set α) → ℝ≥0∞) {x : α | a < f x} : ℝ≥0∞) (0 : ℝ≥0∞)}

Tactic:
exact ne_of_gt (B.trans_le (measure_mono (fun x hx ↦ hb.trans hx)))

Premises used: ne_of_gt, LT.lt.trans_le, MeasureTheory.measure_mono, LT.lt.trans
-- Module: Mathlib.MeasureTheory.Function.FactorsThrough
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

Tactic:
fun x₁ x₂ h ↦ eq_of_mem_singleton ?_

Premises used: Set.eq_of_mem_singleton, Function.FactorsThrough
-- Module: Mathlib.MeasureTheory.Function.FactorsThrough
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
refine : ∀ (x₁ x₂ : X) (h : f x₁ = f x₂), Membership.mem (γ := Set Z) {g x₂} (g x₁)
⊢ Function.FactorsThrough g f

Tactic:
refine fun x₁ x₂ h ↦ eq_of_mem_singleton ?_

Premises used: Set.eq_of_mem_singleton
-- Module: Mathlib.MeasureTheory.Function.FactorsThrough
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₂
obtain : ∀ (s : Set Y) (hs : f ⁻¹' s = g ⁻¹' {g x₂}), Membership.mem (γ := Set Z) {g x₂} (g x₁)
⊢ Membership.mem (γ := Set Z) {g x₂} (g x₁)

Tactic:
obtain ⟨s, -, hs⟩ := hg (measurableSet_singleton (g x₂))

Premises used: MeasurableSingletonClass.measurableSet_singleton
-- Module: Mathlib.MeasureTheory.Function.FactorsThrough
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₂}
rw : x₁ ∈ g ⁻¹' {g x₂}
rw₁ : x₁ ∈ f ⁻¹' s
rw₂ : f x₁ ∈ s
rw₃ : f x₂ ∈ s
rw₄ : x₂ ∈ f ⁻¹' s
rw₅ : x₂ ∈ g ⁻¹' {g x₂}
rw₆ : Membership.mem (γ := Set Z) {g x₂} (g x₂)
rw₇ rw₈ : g x₂ = g x₂
⊢ Membership.mem (γ := Set Z) {g x₂} (g x₁)

Tactic:
rw [← mem_preimage, ← hs, mem_preimage, h, ← mem_preimage, hs, mem_preimage, mem_singleton_iff]

Premises used: Set.mem_singleton_iff, Set.mem_preimage
-- Module: Mathlib.MeasureTheory.Function.FactorsThrough
Goal:
X : Type u_1
Y : Type u_2
Z : Type u_3
mY : MeasurableSpace Y
f : X → Y
g : X → Z
inst : TopologicalSpace Z
inst_1 : PseudoMetrizableSpace Z
inst_2 : T1Space Z
hg : StronglyMeasurable g
⊢ let this := borel Z;
  BorelSpace Z

Tactic:
borelize Z