awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace β
m₀ : MeasurableSpace α
μ : Measure α
inst_1 : Preorder β
inst_2 : OrderClosedTopology β
inst_3 : PseudoMetrizableSpace β
f g : α → β
hf : AEStronglyMeasurable f μ
hg : AEStronglyMeasurable g μ
⊢ NullMeasurableSet {a : α | f a < g a} μ
have this : {a : α | AEStronglyMeasurable.mk f hf a < AEStronglyMeasurable.mk g hg a} =ᶠ[ae μ] {a : α | f a < g a}
Tactic: apply
    (hf.stronglyMeasurable_mk.measurableSet_lt hg.stronglyMeasurable_mk).nullMeasurableSet.congr
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace β
m₀ : MeasurableSpace α
μ : Measure α
inst_1 : Preorder β
inst_2 : OrderClosedTopology β
inst_3 : PseudoMetrizableSpace β
f g : α → β
hf : AEStronglyMeasurable f μ
hg : AEStronglyMeasurable g μ
⊢ {a : α | AEStronglyMeasurable.mk f hf a < AEStronglyMeasurable.mk g hg a} =ᶠ[ae μ] {a : α | f a < g a}
have h : ∀ (x : α) (hfx : f x = AEStronglyMeasurable.mk f hf x) (hgx : g x = AEStronglyMeasurable.mk g hg x),
  {a : α | AEStronglyMeasurable.mk f hf a < AEStronglyMeasurable.mk g hg a} x = {a : α | f a < g a} x
Tactic: filter_upwards [hf.ae_eq_mk, hg.ae_eq_mk] with x hfx hgx
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace β
m₀ : MeasurableSpace α
μ : Measure α
inst_1 : Preorder β
inst_2 : OrderClosedTopology β
inst_3 : PseudoMetrizableSpace β
f g : α → β
hf : AEStronglyMeasurable f μ
hg : AEStronglyMeasurable g μ
x : α
hfx : f x = AEStronglyMeasurable.mk f hf x
hgx : g x = AEStronglyMeasurable.mk g hg x
⊢ {a : α | AEStronglyMeasurable.mk f hf a < AEStronglyMeasurable.mk g hg a} x = {a : α | f a < g a} x
have h : (AEStronglyMeasurable.mk f hf x < AEStronglyMeasurable.mk g hg x) = (f x < g x)
Tactic: change (hf.mk f x < hg.mk g x) = (f x < g x)
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace β
m₀ : MeasurableSpace α
μ : Measure α
inst_1 : Preorder β
inst_2 : OrderClosedTopology β
inst_3 : PseudoMetrizableSpace β
f g : α → β
hf : AEStronglyMeasurable f μ
hg : AEStronglyMeasurable g μ
⊢ NullMeasurableSet {a : α | f a ≤ g a} μ
have this : {a : α | AEStronglyMeasurable.mk f hf a ≤ AEStronglyMeasurable.mk g hg a} =ᶠ[ae μ] {a : α | f a ≤ g a}
Tactic: apply
    (hf.stronglyMeasurable_mk.measurableSet_le hg.stronglyMeasurable_mk).nullMeasurableSet.congr
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace β
m₀ : MeasurableSpace α
μ : Measure α
inst_1 : Preorder β
inst_2 : OrderClosedTopology β
inst_3 : PseudoMetrizableSpace β
f g : α → β
hf : AEStronglyMeasurable f μ
hg : AEStronglyMeasurable g μ
⊢ {a : α | AEStronglyMeasurable.mk f hf a ≤ AEStronglyMeasurable.mk g hg a} =ᶠ[ae μ] {a : α | f a ≤ g a}
have h : ∀ (x : α) (hfx : f x = AEStronglyMeasurable.mk f hf x) (hgx : g x = AEStronglyMeasurable.mk g hg x),
  {a : α | AEStronglyMeasurable.mk f hf a ≤ AEStronglyMeasurable.mk g hg a} x = {a : α | f a ≤ g a} x
Tactic: filter_upwards [hf.ae_eq_mk, hg.ae_eq_mk] with x hfx hgx
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace β
m₀ : MeasurableSpace α
μ : Measure α
inst_1 : Preorder β
inst_2 : OrderClosedTopology β
inst_3 : PseudoMetrizableSpace β
f g : α → β
hf : AEStronglyMeasurable f μ
hg : AEStronglyMeasurable g μ
x : α
hfx : f x = AEStronglyMeasurable.mk f hf x
hgx : g x = AEStronglyMeasurable.mk g hg x
⊢ {a : α | AEStronglyMeasurable.mk f hf a ≤ AEStronglyMeasurable.mk g hg a} x = {a : α | f a ≤ g a} x
have h : (AEStronglyMeasurable.mk f hf x ≤ AEStronglyMeasurable.mk g hg x) = (f x ≤ g x)
Tactic: change (hf.mk f x ≤ hg.mk g x) = (f x ≤ g x)
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace β
m₀ : MeasurableSpace α
μ : Measure α
f : α → β
hf : AEStronglyMeasurable f μ
⊢ ∃ (t : Set β), IsSeparable t ∧ ∀ᵐ (x : α) ∂μ, f x ∈ t
have refine : ∀ᵐ (x : α) ∂μ, f x ∈ range (AEStronglyMeasurable.mk f hf)
Tactic: refine ⟨range (hf.mk f), hf.stronglyMeasurable_mk.isSeparable_range, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace β
m₀ : MeasurableSpace α
μ : Measure α
f : α → β
hf : AEStronglyMeasurable f μ
⊢ ∀ᵐ (x : α) ∂μ, f x ∈ range (AEStronglyMeasurable.mk f hf)
have h : ∀ (x : α) (hx : f x = AEStronglyMeasurable.mk f hf x), f x ∈ range (AEStronglyMeasurable.mk f hf)
Tactic: filter_upwards [hf.ae_eq_mk] with x hx
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace β
m₀ : MeasurableSpace α
μ : Measure α
mβ : MeasurableSpace β
inst_1 : PseudoMetrizableSpace β
inst_2 : BorelSpace β
f : α → β
hf : AEStronglyMeasurable f μ
⊢ AEStronglyMeasurable (m₀ := mβ) id (Measure.map f μ)
have obtain : ∀ (t : Set β) (ht1 : IsSeparable t) (ht2 : ∀ᵐ (x : α) ∂μ, f x ∈ t), AEStronglyMeasurable (m₀ := mβ) id (Measure.map f μ)
Tactic: obtain ⟨t, ht1, ht2⟩ := hf.isSeparable_ae_range
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace β
m₀ : MeasurableSpace α
μ : Measure α
mβ : MeasurableSpace β
inst_1 : PseudoMetrizableSpace β
inst_2 : BorelSpace β
f : α → β
hf : AEStronglyMeasurable f μ
t : Set β
ht1 : IsSeparable t
ht2 : ∀ᵐ (x : α) ∂μ, f x ∈ t
⊢ AEStronglyMeasurable (m₀ := mβ) id (Measure.map f μ)
have refine : Eq (α := ℝ≥0∞) (((Measure.map f μ : Measure β) : (a : Set β) → ℝ≥0∞) (closure[inst] t)ᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: refine aestronglyMeasurable_id_of_isSeparable ht1.closure ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace β
m₀ : MeasurableSpace α
μ : Measure α
mβ : MeasurableSpace β
inst_1 : PseudoMetrizableSpace β
inst_2 : BorelSpace β
f : α → β
hf : AEStronglyMeasurable f μ
t : Set β
ht1 : IsSeparable t
ht2 : ∀ᵐ (x : α) ∂μ, f x ∈ t
⊢ Eq (α := ℝ≥0∞) (((Measure.map f μ : Measure β) : (a : Set β) → ℝ≥0∞) (closure[inst] t)ᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
have refine : ∀ᵐ (x : α) ∂μ, (⋂₀ {t_1 : Set β | IsClosed[inst] t_1 ∧ t ⊆ t_1}) (f x)
Tactic: refine ae_map_iff hf.aemeasurable isClosed_closure.measurableSet |>.2 ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace β
m₀ : MeasurableSpace α
μ : Measure α
mβ : MeasurableSpace β
inst_1 : PseudoMetrizableSpace β
inst_2 : BorelSpace β
f : α → β
hf : AEStronglyMeasurable f μ
t : Set β
ht1 : IsSeparable t
ht2 : ∀ᵐ (x : α) ∂μ, f x ∈ t
⊢ ∀ᵐ (x : α) ∂μ, (⋂₀ {t_1 : Set β | IsClosed[inst] t_1 ∧ t ⊆ t_1}) (f x)
have h : ∀ (a : α),
  Membership.mem (γ := Set α)
    {x : α |
      Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ f x ∈ t) x} x →
        Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ (⋂₀ {t_1 : Set β | IsClosed[inst] t_1 ∧ t ⊆ t_1}) (f x)) x}
          x}
    a
Tactic: filter_upwards [ht2] with ω hω using subset_closure hω
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace β
m₀ : MeasurableSpace α
μ : Measure α
mβ : MeasurableSpace β
inst_1 : PseudoMetrizableSpace β
inst_2 : BorelSpace β
f : α → β
hf : AEStronglyMeasurable f μ
t : Set β
ht1 : IsSeparable t
ht2 : ∀ᵐ (x : α) ∂μ, f x ∈ t
h :
  ∀ (a : α),
    Membership.mem (γ := Set α)
      {x : α |
        Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ f x ∈ t) x} x →
          Membership.mem (γ := Set α)
            {x : α | (fun (x : α) ↦ (⋂₀ {t_1 : Set β | IsClosed[inst] t_1 ∧ t ⊆ t_1}) (f x)) x} x}
      a
⊢ ∀ᵐ (x : α) ∂μ, (⋂₀ {t_1 : Set β | IsClosed[inst] t_1 ∧ t ⊆ t_1}) (f x)
have h₁ : ∀ (a : α), f a ∈ t → (⋂₀ {t_1 : Set β | IsClosed[inst] t_1 ∧ t ⊆ t_1}) (f a)
Tactic: filter_upwards [ht2] with ω hω using subset_closure hω
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace β
m₀ : MeasurableSpace α
μ : Measure α
f : α → β
inst_1 : PseudoMetrizableSpace β
inst_2 : MeasurableSpace β
inst_3 : BorelSpace β
⊢ AEStronglyMeasurable f μ ↔ AEMeasurable f μ ∧ ∃ (t : Set β), IsSeparable t ∧ ∀ᵐ (x : α) ∂μ, f x ∈ t
have refine : (AEMeasurable f μ ∧ ∃ (t : Set β), IsSeparable t ∧ ∀ᵐ (x : α) ∂μ, f x ∈ t) → AEStronglyMeasurable f μ
Tactic: refine ⟨fun H => ⟨H.aemeasurable, H.isSeparable_ae_range⟩, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace β
m₀ : MeasurableSpace α
μ : Measure α
f : α → β
inst_1 : PseudoMetrizableSpace β
inst_2 : MeasurableSpace β
inst_3 : BorelSpace β
H : AEMeasurable f μ
t : Set β
t_sep : IsSeparable t
ht : ∀ᵐ (x : α) ∂μ, f x ∈ t
⊢ AEStronglyMeasurable f μ
have inl : ∀ (t_sep : IsSeparable.{u_2} (α := β) ∅) (ht : ∀ᵐ (x : α) ∂μ, Membership.mem (γ := Set β) ∅ (f x)),
  AEStronglyMeasurable f μ
Tactic: rcases eq_empty_or_nonempty t with (rfl | h₀)
Cleared hypotheses: t, t_sep, ht
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace β
m₀ : MeasurableSpace α
μ : Measure α
f : α → β
inst_1 : PseudoMetrizableSpace β
inst_2 : MeasurableSpace β
inst_3 : BorelSpace β
H : AEMeasurable f μ
t : Set β
t_sep : IsSeparable t
ht : ∀ᵐ (x : α) ∂μ, f x ∈ t
inl :
  ∀ (t_sep : IsSeparable.{u_2} (α := β) ∅) (ht : ∀ᵐ (x : α) ∂μ, Membership.mem (γ := Set β) ∅ (f x)),
    AEStronglyMeasurable f μ
⊢ AEStronglyMeasurable f μ
have inr : ∀ (h₀ : t.Nonempty), AEStronglyMeasurable f μ
Tactic: rcases eq_empty_or_nonempty t with (rfl | h₀)
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable (hypothesis)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace β
m₀ : MeasurableSpace α
μ : Measure α
f : α → β
inst_1 : PseudoMetrizableSpace β
inst_2 : MeasurableSpace β
inst_3 : BorelSpace β
H : AEMeasurable f μ
t_sep : IsSeparable.{u_2} (α := β) ∅
ht : ∀ᵐ (x : α) ∂μ, Membership.mem (γ := Set β) ∅ (f x)
⊢ AEStronglyMeasurable f μ
have ht₁ : μ = 0
Tactic: simp only [mem_empty_iff_false, eventually_false_iff_eq_bot, ae_eq_bot] at ht
Cleared hypotheses: ht
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace β
m₀ : MeasurableSpace α
μ : Measure α
f : α → β
inst_1 : PseudoMetrizableSpace β
inst_2 : MeasurableSpace β
inst_3 : BorelSpace β
H : AEMeasurable f μ
t_sep : IsSeparable.{u_2} (α := β) ∅
ht : μ = 0
⊢ AEStronglyMeasurable f μ
have inl : AEStronglyMeasurable (m₀ := m₀) f 0
Tactic: rw [ht]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace β
m₀ : MeasurableSpace α
μ : Measure α
f : α → β
inst_1 : PseudoMetrizableSpace β
inst_2 : MeasurableSpace β
inst_3 : BorelSpace β
H : AEMeasurable f μ
t : Set β
t_sep : IsSeparable t
ht : ∀ᵐ (x : α) ∂μ, f x ∈ t
h₀ : t.Nonempty
⊢ AEStronglyMeasurable f μ
have inr : ∀ (g : α → β) (g_meas : Measurable g) (gt : range g ⊆ t) (fg : f =ᶠ[ae μ] g), AEStronglyMeasurable f μ
Tactic: obtain ⟨g, g_meas, gt, fg⟩ : ∃ g : α → β, Measurable g ∧ range g ⊆ t ∧ f =ᵐ[μ] g :=
      H.exists_ae_eq_range_subset ht h₀
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace β
m₀ : MeasurableSpace α
μ : Measure α
f : α → β
inst_1 : PseudoMetrizableSpace β
inst_2 : MeasurableSpace β
inst_3 : BorelSpace β
H : AEMeasurable f μ
t : Set β
t_sep : IsSeparable t
ht : ∀ᵐ (x : α) ∂μ, f x ∈ t
h₀ : t.Nonempty
g : α → β
g_meas : Measurable g
gt : range g ⊆ t
fg : f =ᶠ[ae μ] g
⊢ AEStronglyMeasurable f μ
have inr : StronglyMeasurable g
Tactic: refine ⟨g, ?_, fg⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace β
γ : Type u_5
mγ : MeasurableSpace γ
mα : MeasurableSpace α
f : γ → α
μ : Measure γ
hf : MeasurableEmbedding f
g : α → β
⊢ AEStronglyMeasurable (m₀ := mα) g (Measure.map f μ) ↔ AEStronglyMeasurable (g ∘ f) μ
have refine : AEStronglyMeasurable (g ∘ f) μ → AEStronglyMeasurable (m₀ := mα) g (Measure.map f μ)
Tactic: refine ⟨fun H => H.comp_measurable hf.measurable, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace β
γ : Type u_5
mγ : MeasurableSpace γ
mα : MeasurableSpace α
f : γ → α
μ : Measure γ
hf : MeasurableEmbedding f
g : α → β
g₁ : γ → β
hgm₁ : StronglyMeasurable g₁
heq : g ∘ f =ᶠ[ae μ] g₁
⊢ AEStronglyMeasurable (m₀ := mα) g (Measure.map f μ)
have rcases : ∀ (g₂ : α → β) (hgm₂ : StronglyMeasurable g₂) (hgm₁ : StronglyMeasurable (g₂ ∘ f)) (heq : g ∘ f =ᶠ[ae μ] g₂ ∘ f),
  AEStronglyMeasurable (m₀ := mα) g (Measure.map f μ)
Tactic: rcases hf.exists_stronglyMeasurable_extend hgm₁ fun x => ⟨g x⟩ with ⟨g₂, hgm₂, rfl⟩
Cleared hypotheses: g₁, hgm₁, heq
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable (hypothesis)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : TopologicalSpace β
inst_1 : TopologicalSpace γ
m₀ : MeasurableSpace α
μ : Measure α
inst_2 : PseudoMetrizableSpace β
inst_3 : PseudoMetrizableSpace γ
g : β → γ
f : α → β
hg : IsEmbedding g
this : PseudoMetricSpace γ := pseudoMetrizableSpacePseudoMetric γ
⊢ AEStronglyMeasurable.{u_1, u_3} (β := γ) (fun (x : α) ↦ g (f x)) μ ↔ AEStronglyMeasurable f μ
have this₁ : let this := borel β;
BorelSpace β
Tactic: borelize β γ
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable (hypothesis)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : TopologicalSpace β
inst_1 : TopologicalSpace γ
m₀ : MeasurableSpace α
μ : Measure α
inst_2 : PseudoMetrizableSpace β
inst_3 : PseudoMetrizableSpace γ
g : β → γ
f : α → β
hg : IsEmbedding g
this : PseudoMetricSpace γ := pseudoMetrizableSpacePseudoMetric γ
this₁ :
  let this := borel β;
  BorelSpace β
⊢ AEStronglyMeasurable.{u_1, u_3} (β := γ) (fun (x : α) ↦ g (f x)) μ ↔ AEStronglyMeasurable f μ
have this₂ : let this := borel γ;
BorelSpace γ
Tactic: borelize β γ
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : TopologicalSpace β
inst_1 : TopologicalSpace γ
m₀ : MeasurableSpace α
μ : Measure α
inst_2 : PseudoMetrizableSpace β
inst_3 : PseudoMetrizableSpace γ
g : β → γ
f : α → β
hg : IsEmbedding g
this : PseudoMetricSpace γ := pseudoMetrizableSpacePseudoMetric γ
this_1 : MeasurableSpace β := borel β
this_2 : BorelSpace β
this_3 : MeasurableSpace γ := borel γ
this_4 : BorelSpace γ
⊢ AEStronglyMeasurable.{u_1, u_3} (β := γ) (fun (x : α) ↦ g (f x)) μ ↔ AEStronglyMeasurable f μ
have refine_1 : ∀ (H : AEStronglyMeasurable.{u_1, u_3} (β := γ) (fun (x : α) ↦ g (f x)) μ), AEMeasurable f μ
Tactic: refine
    ⟨fun H => aestronglyMeasurable_iff_aemeasurable_separable.2 ⟨?_, ?_⟩, fun H =>
      hg.continuous.comp_aestronglyMeasurable H⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : TopologicalSpace β
inst_1 : TopologicalSpace γ
m₀ : MeasurableSpace α
μ : Measure α
inst_2 : PseudoMetrizableSpace β
inst_3 : PseudoMetrizableSpace γ
g : β → γ
f : α → β
hg : IsEmbedding g
this : PseudoMetricSpace γ := pseudoMetrizableSpacePseudoMetric γ
this_1 : MeasurableSpace β := borel β
this_2 : BorelSpace β
this_3 : MeasurableSpace γ := borel γ
this_4 : BorelSpace γ
refine_1 : ∀ (H : AEStronglyMeasurable.{u_1, u_3} (β := γ) (fun (x : α) ↦ g (f x)) μ), AEMeasurable f μ
⊢ AEStronglyMeasurable.{u_1, u_3} (β := γ) (fun (x : α) ↦ g (f x)) μ ↔ AEStronglyMeasurable f μ
have refine_2 : ∀ (H : AEStronglyMeasurable.{u_1, u_3} (β := γ) (fun (x : α) ↦ g (f x)) μ),
  ∃ (t : Set β), IsSeparable t ∧ ∀ᵐ (x : α) ∂μ, f x ∈ t
Tactic: refine
    ⟨fun H => aestronglyMeasurable_iff_aemeasurable_separable.2 ⟨?_, ?_⟩, fun H =>
      hg.continuous.comp_aestronglyMeasurable H⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : TopologicalSpace β
inst_1 : TopologicalSpace γ
m₀ : MeasurableSpace α
μ : Measure α
inst_2 : PseudoMetrizableSpace β
inst_3 : PseudoMetrizableSpace γ
g : β → γ
f : α → β
hg : IsEmbedding g
this : PseudoMetricSpace γ := pseudoMetrizableSpacePseudoMetric γ
this_1 : MeasurableSpace β := borel β
this_2 : BorelSpace β
this_3 : MeasurableSpace γ := borel γ
this_4 : BorelSpace γ
H : AEStronglyMeasurable.{u_1, u_3} (β := γ) (fun (x : α) ↦ g (f x)) μ
G : β → (↑(range g) : Type u_3) := rangeFactorization g
⊢ IsClosed[instTopologicalSpaceSubtype] (range G)
have rw : IsClosed[instTopologicalSpaceSubtype] univ
Tactic: rw [rangeFactorization_surjective.range_eq]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable (hypothesis)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : TopologicalSpace β
inst_1 : TopologicalSpace γ
m₀ : MeasurableSpace α
μ : Measure α
inst_2 : PseudoMetrizableSpace β
inst_3 : PseudoMetrizableSpace γ
g : β → γ
f : α → β
hg : IsEmbedding g
this : PseudoMetricSpace γ := pseudoMetrizableSpacePseudoMetric γ
this_1 : MeasurableSpace β := borel β
this_2 : BorelSpace β
this_3 : MeasurableSpace γ := borel γ
this_4 : BorelSpace γ
H : AEStronglyMeasurable.{u_1, u_3} (β := γ) (fun (x : α) ↦ g (f x)) μ
G : β → (↑(range g) : Type u_3) := rangeFactorization g
⊢ AEMeasurable f μ
have hG : IsClosedEmbedding G
Tactic: have hG : IsClosedEmbedding G :=
      { hg.codRestrict _ _ with
        isClosed_range := by rw [rangeFactorization_surjective.range_eq]; exact isClosed_univ }
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable (hypothesis)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : TopologicalSpace β
inst_1 : TopologicalSpace γ
m₀ : MeasurableSpace α
μ : Measure α
inst_2 : PseudoMetrizableSpace β
inst_3 : PseudoMetrizableSpace γ
g : β → γ
f : α → β
hg : IsEmbedding g
this : PseudoMetricSpace γ := pseudoMetrizableSpacePseudoMetric γ
this_1 : MeasurableSpace β := borel β
this_2 : BorelSpace β
this_3 : MeasurableSpace γ := borel γ
this_4 : BorelSpace γ
H : AEStronglyMeasurable.{u_1, u_3} (β := γ) (fun (x : α) ↦ g (f x)) μ
G : β → (↑(range g) : Type u_3) := rangeFactorization g
hG : IsClosedEmbedding G
⊢ AEMeasurable f μ
have this₁ : AEMeasurable (G ∘ f) μ
Tactic: have : AEMeasurable (G ∘ f) μ := AEMeasurable.subtype_mk H.aemeasurable
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : TopologicalSpace β
inst_1 : TopologicalSpace γ
m₀ : MeasurableSpace α
μ : Measure α
inst_2 : PseudoMetrizableSpace β
inst_3 : PseudoMetrizableSpace γ
g : β → γ
f : α → β
hg : IsEmbedding g
this : PseudoMetricSpace γ := pseudoMetrizableSpacePseudoMetric γ
this_1 : MeasurableSpace β := borel β
this_2 : BorelSpace β
this_3 : MeasurableSpace γ := borel γ
this_4 : BorelSpace γ
H : AEStronglyMeasurable.{u_1, u_3} (β := γ) (fun (x : α) ↦ g (f x)) μ
⊢ ∃ (t : Set β), IsSeparable t ∧ ∀ᵐ (x : α) ∂μ, f x ∈ t
have refine_2 : ∀ (t : Set γ) (ht : IsSeparable t) (h't : ∀ᵐ (x : α) ∂μ, g (f x) ∈ t),
  ∃ (t : Set β), IsSeparable t ∧ ∀ᵐ (x : α) ∂μ, f x ∈ t
Tactic: rcases (aestronglyMeasurable_iff_aemeasurable_separable.1 H).2 with ⟨t, ht, h't⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable (hypothesis)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace β
m₀ : MeasurableSpace α
μ : Measure α
ι : Type u_5
inst_1 : PseudoMetrizableSpace β
u : Filter ι
inst_2 : u.NeBot
inst_3 : u.IsCountablyGenerated
f : ι → α → β
g : α → β
hf : ∀ (i : ι), AEStronglyMeasurable (f i) μ
lim : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ι) ↦ f n x) u (𝓝 (g x))
⊢ AEStronglyMeasurable g μ
have this : let this := borel β;
BorelSpace β
Tactic: borelize β
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace β
m₀ : MeasurableSpace α
μ : Measure α
ι : Type u_5
inst_1 : PseudoMetrizableSpace β
u : Filter ι
inst_2 : u.NeBot
inst_3 : u.IsCountablyGenerated
f : ι → α → β
g : α → β
hf : ∀ (i : ι), AEStronglyMeasurable (f i) μ
lim : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ι) ↦ f n x) u (𝓝 (g x))
this : MeasurableSpace β := borel β
this_1 : BorelSpace β
⊢ AEStronglyMeasurable g μ
have refine_1 : AEMeasurable g μ
Tactic: refine aestronglyMeasurable_iff_aemeasurable_separable.2 ⟨?_, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace β
m₀ : MeasurableSpace α
μ : Measure α
ι : Type u_5
inst_1 : PseudoMetrizableSpace β
u : Filter ι
inst_2 : u.NeBot
inst_3 : u.IsCountablyGenerated
f : ι → α → β
g : α → β
hf : ∀ (i : ι), AEStronglyMeasurable (f i) μ
lim : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ι) ↦ f n x) u (𝓝 (g x))
this : MeasurableSpace β := borel β
this_1 : BorelSpace β
refine_1 : AEMeasurable g μ
⊢ AEStronglyMeasurable g μ
have refine_2 : ∃ (t : Set β), IsSeparable t ∧ ∀ᵐ (x : α) ∂μ, g x ∈ t
Tactic: refine aestronglyMeasurable_iff_aemeasurable_separable.2 ⟨?_, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace β
m₀ : MeasurableSpace α
μ : Measure α
ι : Type u_5
inst_1 : PseudoMetrizableSpace β
u : Filter ι
inst_2 : u.NeBot
inst_3 : u.IsCountablyGenerated
f : ι → α → β
g : α → β
hf : ∀ (i : ι), AEStronglyMeasurable (f i) μ
lim : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ι) ↦ f n x) u (𝓝 (g x))
this : MeasurableSpace β := borel β
this_1 : BorelSpace β
⊢ ∃ (t : Set β), IsSeparable t ∧ ∀ᵐ (x : α) ∂μ, g x ∈ t
have refine_2 : ∀ (v : ℕ → ι) (hv : Tendsto v atTop u), ∃ (t : Set β), IsSeparable t ∧ ∀ᵐ (x : α) ∂μ, g x ∈ t
Tactic: rcases u.exists_seq_tendsto with ⟨v, hv⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable (hypothesis)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace β
m₀ : MeasurableSpace α
μ : Measure α
ι : Type u_5
inst_1 : PseudoMetrizableSpace β
u : Filter ι
inst_2 : u.NeBot
inst_3 : u.IsCountablyGenerated
f : ι → α → β
g : α → β
hf : ∀ (i : ι), AEStronglyMeasurable (f i) μ
lim : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ι) ↦ f n x) u (𝓝 (g x))
this : MeasurableSpace β := borel β
this_1 : BorelSpace β
v : ℕ → ι
hv : Tendsto v atTop u
⊢ ∃ (t : Set β), IsSeparable t ∧ ∀ᵐ (x : α) ∂μ, g x ∈ t
have this : ∀ (n : ℕ), ∃ (t : Set β), IsSeparable t ∧ f (v n) ⁻¹' t ∈ ae μ
Tactic: have : ∀ n : ℕ, ∃ t : Set β, IsSeparable t ∧ f (v n) ⁻¹' t ∈ ae μ := fun n =>
      (aestronglyMeasurable_iff_aemeasurable_separable.1 (hf (v n))).2