awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.Egorov (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
inst : PseudoEMetricSpace β
μ : Measure α
s : Set α
ε : ℝ
f : ι → α → β
g : α → β
inst_1 : SemilatticeSup ι
inst_2 : Nonempty ι
inst_3 : Countable ι
hε : 0 < ε
hf : ∀ (n : ι), Measurable (β := ℝ≥0∞) fun (a : α) ↦ edist (f n a) (g a)
hsm : MeasurableSet s
hs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hfg : ∀ᵐ (x : α) ∂μ, x ∈ s → Tendsto (fun (n : ι) ↦ f n x) atTop (𝓝 (g x))
⊢ Summable (HPow.hPow (α := ℝ) 2⁻¹)
have hf₁ : Summable (HPow.hPow (1 / 2))
Tactic: rw [inv_eq_one_div]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.Egorov (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
inst : PseudoEMetricSpace β
μ : Measure α
s : Set α
ε : ℝ
f : ι → α → β
g : α → β
inst_1 : SemilatticeSup ι
inst_2 : Nonempty ι
inst_3 : Countable ι
hε : 0 < ε
hf : ∀ (n : ι), Measurable (β := ℝ≥0∞) fun (a : α) ↦ edist (f n a) (g a)
hsm : MeasurableSet s
hs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hfg : ∀ᵐ (x : α) ∂μ, x ∈ s → Tendsto (fun (n : ι) ↦ f n x) atTop (𝓝 (g x))
⊢ iUnionNotConvergentSeq (s := s) hε hf hsm hs hfg ⊆ s
have rw : s ∩ ⋃ (i : ℕ), notConvergentSeq f g i (notConvergentSeqLTIndex (s := s) sorry hf hsm hs hfg i) ⊆ s
Tactic: rw [iUnionNotConvergentSeq, ← Set.inter_iUnion]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.Egorov (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
inst : PseudoEMetricSpace β
μ : Measure α
s : Set α
ε : ℝ
f : ι → α → β
g : α → β
inst_1 : SemilatticeSup ι
inst_2 : Nonempty ι
inst_3 : Countable ι
hε : 0 < ε
hf : ∀ (n : ι), Measurable (β := ℝ≥0∞) fun (a : α) ↦ edist (f n a) (g a)
hsm : MeasurableSet s
hs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hfg : ∀ᵐ (x : α) ∂μ, x ∈ s → Tendsto (fun (n : ι) ↦ f n x) atTop (𝓝 (g x))
⊢ TendstoUniformlyOn f g atTop (s \ iUnionNotConvergentSeq (s := s) hε hf hsm hs hfg)
have rw : ∀ ε_1 > 0, ∀ᶠ (n : ι) in atTop, ∀ x ∈ s \ iUnionNotConvergentSeq (s := s) hε hf hsm hs hfg, edist (g x) (f n x) < ε_1
Tactic: rw [EMetric.tendstoUniformlyOn_iff]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.Egorov (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
inst : PseudoEMetricSpace β
μ : Measure α
s : Set α
ε : ℝ
f : ι → α → β
g : α → β
inst_1 : SemilatticeSup ι
inst_2 : Nonempty ι
inst_3 : Countable ι
hε : 0 < ε
hf : ∀ (n : ι), Measurable (β := ℝ≥0∞) fun (a : α) ↦ edist (f n a) (g a)
hsm : MeasurableSet s
hs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hfg : ∀ᵐ (x : α) ∂μ, x ∈ s → Tendsto (fun (n : ι) ↦ f n x) atTop (𝓝 (g x))
δ : ℝ≥0∞
hδ : δ > 0
⊢ ∀ᶠ (n : ι) in atTop, ∀ x ∈ s \ iUnionNotConvergentSeq (s := s) hε hf hsm hs hfg, edist (g x) (f n x) < δ
have obtain : ∀ (N : ℕ) (hN : (↑N : ℝ≥0∞)⁻¹ < δ),
  ∀ᶠ (n : ι) in atTop, ∀ x ∈ s \ iUnionNotConvergentSeq (s := s) hε hf hsm hs hfg, edist (g x) (f n x) < δ
Tactic: obtain ⟨N, hN⟩ := ENNReal.exists_inv_nat_lt hδ.ne'
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.Egorov (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
inst : PseudoEMetricSpace β
μ : Measure α
s : Set α
ε : ℝ
f : ι → α → β
g : α → β
inst_1 : SemilatticeSup ι
inst_2 : Nonempty ι
inst_3 : Countable ι
hε : 0 < ε
hf : ∀ (n : ι), Measurable (β := ℝ≥0∞) fun (a : α) ↦ edist (f n a) (g a)
hsm : MeasurableSet s
hs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hfg : ∀ᵐ (x : α) ∂μ, x ∈ s → Tendsto (fun (n : ι) ↦ f n x) atTop (𝓝 (g x))
δ : ℝ≥0∞
hδ : δ > 0
N : ℕ
hN : (↑N : ℝ≥0∞)⁻¹ < δ
⊢ ∀ᶠ (n : ι) in atTop, ∀ x ∈ s \ iUnionNotConvergentSeq (s := s) hε hf hsm hs hfg, edist (g x) (f n x) < δ
have rw : ∃ (a : ι), ∀ b ≥ a, ∀ x ∈ s \ iUnionNotConvergentSeq (s := s) hε hf hsm hs hfg, edist (g x) (f b x) < δ
Tactic: rw [eventually_atTop]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.Egorov (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
inst : PseudoEMetricSpace β
μ : Measure α
s : Set α
ε : ℝ
f : ι → α → β
g : α → β
inst_1 : SemilatticeSup ι
inst_2 : Nonempty ι
inst_3 : Countable ι
hε : 0 < ε
hf : ∀ (n : ι), Measurable (β := ℝ≥0∞) fun (a : α) ↦ edist (f n a) (g a)
hsm : MeasurableSet s
hs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hfg : ∀ᵐ (x : α) ∂μ, x ∈ s → Tendsto (fun (n : ι) ↦ f n x) atTop (𝓝 (g x))
δ : ℝ≥0∞
hδ : δ > 0
N : ℕ
hN : (↑N : ℝ≥0∞)⁻¹ < δ
⊢ ∃ (a : ι), ∀ b ≥ a, ∀ x ∈ s \ iUnionNotConvergentSeq (s := s) hε hf hsm hs hfg, edist (g x) (f b x) < δ
have refine : ∀ (n : ι) (hn : n ≥ notConvergentSeqLTIndex (s := s) sorry hf hsm hs hfg N) (x : α)
  (hx : x ∈ s \ iUnionNotConvergentSeq (s := s) hε hf hsm hs hfg), edist (g x) (f n x) < δ
Tactic: refine ⟨Egorov.notConvergentSeqLTIndex (half_pos hε) hf hsm hs hfg N, fun n hn x hx => ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.Egorov (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
inst : PseudoEMetricSpace β
μ : Measure α
s : Set α
ε : ℝ
f : ι → α → β
g : α → β
inst_1 : SemilatticeSup ι
inst_2 : Nonempty ι
inst_3 : Countable ι
hε : 0 < ε
hf : ∀ (n : ι), Measurable (β := ℝ≥0∞) fun (a : α) ↦ edist (f n a) (g a)
hsm : MeasurableSet s
hs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hfg : ∀ᵐ (x : α) ∂μ, x ∈ s → Tendsto (fun (n : ι) ↦ f n x) atTop (𝓝 (g x))
δ : ℝ≥0∞
hδ : δ > 0
N : ℕ
hN : (↑N : ℝ≥0∞)⁻¹ < δ
n : ι
hn : n ≥ notConvergentSeqLTIndex (s := s) ⋯ hf hsm hs hfg N
x : α
hx : x ∈ s \ iUnionNotConvergentSeq (s := s) hε hf hsm hs hfg
⊢ edist (g x) (f n x) < δ
have refine : edist (g x) (f n x) ≤ (↑N : ℝ≥0∞)⁻¹
Tactic: refine lt_of_le_of_lt ?_ hN
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.Egorov (hypothesis)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
inst : PseudoEMetricSpace β
μ : Measure α
s : Set α
ε : ℝ
f : ι → α → β
g : α → β
inst_1 : SemilatticeSup ι
inst_2 : Nonempty ι
inst_3 : Countable ι
hε : 0 < ε
hf : ∀ (n : ι), Measurable (β := ℝ≥0∞) fun (a : α) ↦ edist (f n a) (g a)
hsm : MeasurableSet s
hs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hfg : ∀ᵐ (x : α) ∂μ, x ∈ s → Tendsto (fun (n : ι) ↦ f n x) atTop (𝓝 (g x))
δ : ℝ≥0∞
hδ : δ > 0
N : ℕ
hN : (↑N : ℝ≥0∞)⁻¹ < δ
n : ι
hn : n ≥ notConvergentSeqLTIndex (s := s) ⋯ hf hsm hs hfg N
x : α
hx : x ∈ s \ iUnionNotConvergentSeq (s := s) hε hf hsm hs hfg
⊢ edist (g x) (f n x) ≤ (↑N : ℝ≥0∞)⁻¹
have this : edist (f n x) (g x) ≤ (↑N : ℝ≥0∞)⁻¹
Tactic: have : edist (f n x) (g x) ≤ (N : ℝ≥0∞)⁻¹ :=
    not_lt.mp fun h ↦ hx.2 <| Set.mem_iUnion.2 ⟨N, hx.1, mem_notConvergentSeq_iff.2 ⟨n, hn, h⟩⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.Egorov (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
inst : PseudoEMetricSpace β
μ : Measure α
inst_1 : SemilatticeSup ι
inst_2 : Nonempty ι
inst_3 : Countable ι
f : ι → α → β
g : α → β
inst_4 : IsFiniteMeasure μ
hf : ∀ (n : ι), Measurable (β := ℝ≥0∞) fun (a : α) ↦ edist (f n a) (g a)
hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ι) ↦ f n x) atTop (𝓝 (g x))
ε : ℝ
hε : 0 < ε
⊢ ∀ᵐ (x : α) ∂μ, Membership.mem (γ := Set α) univ x → Tendsto (fun (n : ι) ↦ f n x) atTop (𝓝 (g x))
have h : ∀ (a : α),
  Membership.mem (γ := Set α)
    {x : α |
      Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ Tendsto (fun (n : ι) ↦ f n x) atTop (𝓝 (g x))) x} x →
        Membership.mem (γ := Set α)
          {x : α | (fun (x : α) ↦ Membership.mem (γ := Set α) univ x → Tendsto (fun (n : ι) ↦ f n x) atTop (𝓝 (g x))) x}
          x}
    a
Tactic: filter_upwards [hfg] with _ htendsto _ using htendsto
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.Egorov (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
inst : PseudoEMetricSpace β
μ : Measure α
inst_1 : SemilatticeSup ι
inst_2 : Nonempty ι
inst_3 : Countable ι
f : ι → α → β
g : α → β
inst_4 : IsFiniteMeasure μ
hf : ∀ (n : ι), Measurable (β := ℝ≥0∞) fun (a : α) ↦ edist (f n a) (g a)
hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ι) ↦ f n x) atTop (𝓝 (g x))
ε : ℝ
hε : 0 < ε
h :
  ∀ (a : α),
    Membership.mem (γ := Set α)
      {x : α |
        Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ Tendsto (fun (n : ι) ↦ f n x) atTop (𝓝 (g x))) x} x →
          Membership.mem (γ := Set α)
            {x : α |
              (fun (x : α) ↦ Membership.mem (γ := Set α) univ x → Tendsto (fun (n : ι) ↦ f n x) atTop (𝓝 (g x))) x}
            x}
      a
⊢ ∀ᵐ (x : α) ∂μ, Membership.mem (γ := Set α) univ x → Tendsto (fun (n : ι) ↦ f n x) atTop (𝓝 (g x))
have h₁ : ∀ (a : α),
  Tendsto (fun (n : ι) ↦ f n a) atTop (𝓝 (g a)) →
    Membership.mem (γ := Set α) univ a → Tendsto (fun (n : ι) ↦ f n a) atTop (𝓝 (g a))
Tactic: filter_upwards [hfg] with _ htendsto _ using htendsto
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.Egorov (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
inst : PseudoEMetricSpace β
μ : Measure α
inst_1 : SemilatticeSup ι
inst_2 : Nonempty ι
inst_3 : Countable ι
f : ι → α → β
g : α → β
inst_4 : IsFiniteMeasure μ
hf : ∀ (n : ι), Measurable (β := ℝ≥0∞) fun (a : α) ↦ edist (f n a) (g a)
hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ι) ↦ f n x) atTop (𝓝 (g x))
ε : ℝ
hε : 0 < ε
⊢ ∃ (t : Set α), MeasurableSet t ∧ (μ : (a : Set α) → ℝ≥0∞) t ≤ ENNReal.ofReal ε ∧ TendstoUniformlyOn f g atTop tᶜ
have have : ∀ t ⊆ univ,
  ∀ (ht : MeasurableSet t)
    (htendsto : (μ : (a : Set α) → ℝ≥0∞) t ≤ ENNReal.ofReal ε ∧ TendstoUniformlyOn f g atTop (univ \ t)),
    ∃ (t : Set α), MeasurableSet t ∧ (μ : (a : Set α) → ℝ≥0∞) t ≤ ENNReal.ofReal ε ∧ TendstoUniformlyOn f g atTop tᶜ
Tactic: have ⟨t, _, ht, htendsto⟩ :=
    tendstoUniformlyOn_of_ae_tendsto_of_measurable_edist hf MeasurableSet.univ
    (measure_ne_top μ Set.univ) (by filter_upwards [hfg] with _ htendsto _ using htendsto) hε
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.Egorov (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
inst : PseudoEMetricSpace β
μ : Measure α
inst_1 : SemilatticeSup ι
inst_2 : Nonempty ι
inst_3 : Countable ι
f : ι → α → β
g : α → β
inst_4 : IsFiniteMeasure μ
hf : ∀ (n : ι), Measurable (β := ℝ≥0∞) fun (a : α) ↦ edist (f n a) (g a)
hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ι) ↦ f n x) atTop (𝓝 (g x))
ε : ℝ
hε : 0 < ε
t : Set α
left : t ⊆ univ
ht : MeasurableSet t
htendsto : (μ : (a : Set α) → ℝ≥0∞) t ≤ ENNReal.ofReal ε ∧ TendstoUniformlyOn f g atTop (univ \ t)
⊢ ∃ (t : Set α), MeasurableSet t ∧ (μ : (a : Set α) → ℝ≥0∞) t ≤ ENNReal.ofReal ε ∧ TendstoUniformlyOn f g atTop tᶜ
have refine : (μ : (a : Set α) → ℝ≥0∞) t ≤ ENNReal.ofReal ε ∧ TendstoUniformlyOn f g atTop tᶜ
Tactic: refine ⟨_, ht, ?_⟩
-- 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 : γ → β
hf : AEMeasurable f μ
hgf : IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) (ae μ) (g ∘ f)
hg : IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) (ae (F := Measure γ) (Measure.map f μ)) g
⊢ essSup (g ∘ f) μ ≤ @essSup _ _ _ mγ g (Measure.map f μ)
have refine : map (g ∘ f) (ae μ) ≤ map g (ae (F := Measure γ) (Measure.map f μ))
Tactic: refine limsSup_le_limsSup_of_le ?_ hgf hg
-- 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 : γ → β
hf : AEMeasurable f μ
hgf : IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) (ae μ) (g ∘ f)
hg : IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) (ae (F := Measure γ) (Measure.map f μ)) g
⊢ map (g ∘ f) (ae μ) ≤ map g (ae (F := Measure γ) (Measure.map f μ))
have rw : map g (map f (ae μ)) ≤ map g (ae (F := Measure γ) (Measure.map f μ))
Tactic: rw [← map_map]
-- 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 : γ → β
hf : MeasurableEmbedding 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 : IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) (ae (F := Measure γ) (Measure.map f μ)) g
⊢ @essSup _ _ _ mγ g (Measure.map f μ) = essSup (g ∘ f) μ
have refine : @essSup _ _ _ mγ g (Measure.map f μ) ≤ essSup (g ∘ f) μ
Tactic: refine le_antisymm ?_ (essSup_comp_le_essSup_map_measure hf.measurable.aemeasurable hgf_co hg)
-- 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 : γ → β
hf : MeasurableEmbedding 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 : IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) (ae (F := Measure γ) (Measure.map f μ)) g
⊢ @essSup _ _ _ mγ g (Measure.map f μ) ≤ essSup (g ∘ f) μ
have refine : ∀ (c : β) (h_le : ∀ᶠ (n : β) in map (g ∘ f) (ae μ), n ≤ c),
  ∀ᶠ (n : β) in map g (ae (F := Measure γ) (Measure.map f μ)), n ≤ c
Tactic: refine limsSup_le_limsSup hg_co hgf (fun c h_le => ?_)
-- 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 : γ → β
hf : MeasurableEmbedding 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 : IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) (ae (F := Measure γ) (Measure.map f μ)) g
c : β
h_le : ∀ᶠ (n : β) in map (g ∘ f) (ae μ), n ≤ c
⊢ ∀ᶠ (n : β) in map g (ae (F := Measure γ) (Measure.map f μ)), n ≤ c
have rw : ∀ (h_le : ∀ᵐ (a : α) ∂μ, (g ∘ f) a ≤ c), ∀ᵐ (a : γ) ∂Measure.map f μ, g a ≤ c
Tactic: rw [eventually_map] at h_le ⊢
Cleared hypotheses: h_le
-- 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 : Measurable g
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
⊢ @essSup _ _ _ mγ g (Measure.map f μ) = essSup (g ∘ f) μ
have refine : @essSup _ _ _ mγ g (Measure.map f μ) ≤ essSup (g ∘ f) μ
Tactic: refine le_antisymm ?_ (essSup_comp_le_essSup_map_measure hf hgf_co hg_bdd)
-- 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 : Measurable g
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
⊢ @essSup _ _ _ mγ g (Measure.map f μ) ≤ essSup (g ∘ f) μ
have refine : ∀ (c : β) (h_le : ∀ᶠ (n : β) in map (g ∘ f) (ae μ), n ≤ c),
  ∀ᶠ (n : β) in map g (ae (F := Measure γ) (Measure.map f μ)), n ≤ c
Tactic: refine limsSup_le_limsSup hg_co hgf (fun c h_le => ?_)
-- 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 : Measurable g
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
c : β
h_le : ∀ᶠ (n : β) in map (g ∘ f) (ae μ), n ≤ c
⊢ ∀ᶠ (n : β) in map g (ae (F := Measure γ) (Measure.map f μ)), n ≤ c
have rw : ∀ (h_le : ∀ᵐ (a : α) ∂μ, (g ∘ f) a ≤ c), ∀ᵐ (a : γ) ∂Measure.map f μ, g a ≤ c
Tactic: rw [eventually_map] at h_le ⊢
Cleared hypotheses: h_le
-- 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 : Measurable g
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
c : β
h_le : ∀ᵐ (a : α) ∂μ, (g ∘ f) a ≤ c
⊢ ∀ᵐ (a : γ) ∂Measure.map f μ, g a ≤ c
have rw : ∀ᵐ (x : α) ∂μ, g (f x) ≤ c
Tactic: rw [ae_map_iff hf (measurableSet_le hg measurable_const)]
-- 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
⊢ @essSup _ _ _ mγ g (Measure.map f μ) = essSup (g ∘ f) μ
have hg_mk_co : IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) (ae (F := Measure γ) (Measure.map f μ)) (AEMeasurable.mk g hg)
Tactic: have hg_mk_co : IsCoboundedUnder (· ≤ ·) (ae (Measure.map f μ)) (hg.mk g) := by
    simpa [IsCoboundedUnder, ← map_congr hg.ae_eq_mk]
-- 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)
⊢ @essSup _ _ _ mγ g (Measure.map f μ) = essSup (g ∘ f) μ
have hg_mk_bdd : IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) (ae (F := Measure γ) (Measure.map f μ)) (AEMeasurable.mk g hg)
Tactic: have hg_mk_bdd : IsBoundedUnder (· ≤ ·) (ae (Measure.map f μ)) (hg.mk g) := by
    simpa [IsBoundedUnder, ← map_congr hg.ae_eq_mk]
-- 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)
⊢ @essSup _ _ _ mγ g (Measure.map f μ) = essSup (g ∘ f) μ
have h_eq : g ∘ f =ᶠ[ae μ] AEMeasurable.mk g hg ∘ f
Tactic: have h_eq := ae_eq_comp hf hg.ae_eq_mk
-- 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
⊢ @essSup _ _ _ mγ g (Measure.map f μ) = essSup (g ∘ f) μ
have hg_mk_f : IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) (ae μ) (AEMeasurable.mk g hg ∘ f)
Tactic: have hg_mk_f : IsBoundedUnder (· ≤ ·) (ae μ) ((hg.mk g) ∘ f) := by
    simpa [IsBoundedUnder, ← map_congr h_eq]