awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace β
g : α → β
γ : Type u_5
x : MeasurableSpace γ
x_1 : MeasurableSpace α
f : γ → α
μ : Measure γ
ν : Measure α
hg : AEStronglyMeasurable g ν
hf : QuasiMeasurePreserving f μ ν
⊢ AEStronglyMeasurable (g ∘ f) μ

Tactic:
(hg.mono_ac hf.absolutelyContinuous).comp_measurable hf.measurable

Premises used: MeasureTheory.AEStronglyMeasurable.comp_measurable, MeasureTheory.AEStronglyMeasurable.mono_ac, MeasureTheory.Measure.QuasiMeasurePreserving.absolutelyContinuous, MeasureTheory.Measure.QuasiMeasurePreserving.measurable
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace β
m₀ : MeasurableSpace α
μ : Measure α
f : α → β
hf : AEStronglyMeasurable f μ
⊢ ∃ (t : Set β), IsSeparable t ∧ ∀ᵐ (x : α) ∂μ, f x ∈ t

Tactic:
⟨range (hf.mk f), hf.stronglyMeasurable_mk.isSeparable_range, ?_⟩

Premises used: MeasureTheory.StronglyMeasurable.isSeparable_range, MeasureTheory.AEStronglyMeasurable.stronglyMeasurable_mk, MeasureTheory.AEStronglyMeasurable.mk, And.intro, Exists.intro, Set.range
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace β
m₀ : MeasurableSpace α
μ : Measure α
f : α → β
hf : AEStronglyMeasurable f μ
refine : ∀ᵐ (x : α) ∂μ, f x ∈ range (AEStronglyMeasurable.mk f hf)
⊢ ∃ (t : Set β), IsSeparable t ∧ ∀ᵐ (x : α) ∂μ, f x ∈ t

Tactic:
refine ⟨range (hf.mk f), hf.stronglyMeasurable_mk.isSeparable_range, ?_⟩
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace β
m₀ : MeasurableSpace α
μ : Measure α
f : α → β
hf : AEStronglyMeasurable f μ
h : ∀ (x : α) (hx : f x = AEStronglyMeasurable.mk f hf x), f x ∈ range (AEStronglyMeasurable.mk f hf)
⊢ ∀ᵐ (x : α) ∂μ, f x ∈ range (AEStronglyMeasurable.mk f hf)

Tactic:
filter_upwards [hf.ae_eq_mk] with x hx

Premises used: MeasureTheory.AEStronglyMeasurable.ae_eq_mk
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace β
m₀ : MeasurableSpace α
μ : Measure α
f : α → β
hf : AEStronglyMeasurable f μ
x : α
hx : f x = AEStronglyMeasurable.mk f hf x
⊢ f x ∈ range (AEStronglyMeasurable.mk f hf)

Tactic:
simp [hx]
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace β
m₀ : MeasurableSpace α
μ : Measure α
mβ : MeasurableSpace β
inst_1 : PseudoMetrizableSpace β
inst_2 : BorelSpace β
f : α → β
hf : AEStronglyMeasurable f μ
obtain :
  ∀ (t : Set β) (ht1 : IsSeparable t) (ht2 : ∀ᵐ (x : α) ∂μ, f x ∈ t),
    AEStronglyMeasurable (m₀ := mβ) id (Measure.map f μ)
⊢ AEStronglyMeasurable (m₀ := mβ) id (Measure.map f μ)

Tactic:
obtain ⟨t, ht1, ht2⟩ := hf.isSeparable_ae_range

Premises used: MeasureTheory.AEStronglyMeasurable.isSeparable_ae_range
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
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 μ)

Tactic:
aestronglyMeasurable_id_of_isSeparable ht1.closure ?_

Premises used: MeasureTheory.aestronglyMeasurable_id_of_isSeparable, TopologicalSpace.IsSeparable.closure
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
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
refine : Eq (α := ℝ≥0∞) (((Measure.map f μ : Measure β) : (a : Set β) → ℝ≥0∞) (closure[inst] t)ᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ AEStronglyMeasurable (m₀ := mβ) id (Measure.map f μ)

Tactic:
refine aestronglyMeasurable_id_of_isSeparable ht1.closure ?_

Premises used: MeasureTheory.aestronglyMeasurable_id_of_isSeparable, TopologicalSpace.IsSeparable.closure
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
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∞)

Tactic:
ae_map_iff hf.aemeasurable isClosed_closure.measurableSet |>.2 ?_

Premises used: Iff.mpr, MeasureTheory.AEStronglyMeasurable.aemeasurable, Set.Mem, Filter.Eventually, setOf, MeasureTheory.ae_map_iff, IsClosed.measurableSet, closure, isClosed_closure, Set.sInter
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
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
refine : ∀ᵐ (x : α) ∂μ, (⋂₀ {t_1 : Set β | IsClosed[inst] t_1 ∧ t ⊆ t_1}) (f x)
⊢ Eq (α := ℝ≥0∞) (((Measure.map f μ : Measure β) : (a : Set β) → ℝ≥0∞) (closure[inst] t)ᶜ : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
refine ae_map_iff hf.aemeasurable isClosed_closure.measurableSet |>.2 ?_

Premises used: Iff.mpr, MeasureTheory.AEStronglyMeasurable.aemeasurable, MeasureTheory.ae_map_iff, IsClosed.measurableSet, isClosed_closure
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
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ω : f ω ∈ t
⊢ (⋂₀ {t_1 : Set β | IsClosed[inst] t_1 ∧ t ⊆ t_1}) (f ω)

Tactic:
subset_closure hω

Premises used: Set.Mem, subset_closure, closure, Set.sInter
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
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
h₁ h₂ : ∀ (ω : α) (hω : f ω ∈ t), (⋂₀ {t_1 : Set β | IsClosed[inst] t_1 ∧ t ⊆ t_1}) (f ω)
⊢ ∀ᵐ (x : α) ∂μ, (⋂₀ {t_1 : Set β | IsClosed[inst] t_1 ∧ t ⊆ t_1}) (f x)

Tactic:
filter_upwards [ht2] with ω hω using subset_closure hω
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
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

Tactic:
⟨fun H => ⟨H.aemeasurable, H.isSeparable_ae_range⟩, ?_⟩

Premises used: MeasureTheory.AEStronglyMeasurable.aemeasurable, And.intro, Iff.intro, MeasureTheory.AEStronglyMeasurable.isSeparable_ae_range
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace β
m₀ : MeasurableSpace α
μ : Measure α
f : α → β
inst_1 : PseudoMetrizableSpace β
inst_2 : MeasurableSpace β
inst_3 : BorelSpace β
refine : (AEMeasurable f μ ∧ ∃ (t : Set β), IsSeparable t ∧ ∀ᵐ (x : α) ∂μ, f x ∈ t) → AEStronglyMeasurable f μ
⊢ AEStronglyMeasurable f μ ↔ AEMeasurable f μ ∧ ∃ (t : Set β), IsSeparable t ∧ ∀ᵐ (x : α) ∂μ, f x ∈ t

Tactic:
refine ⟨fun H => ⟨H.aemeasurable, H.isSeparable_ae_range⟩, ?_⟩
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
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 μ
inr : ∀ (h₀ : t.Nonempty), AEStronglyMeasurable f μ
⊢ AEStronglyMeasurable f μ

Tactic:
rcases eq_empty_or_nonempty t with (rfl | h₀)

Premises used: Set.eq_empty_or_nonempty, rfl
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
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)
⊢ μ = 0

Tactic:
simp only [mem_empty_iff_false, eventually_false_iff_eq_bot, ae_eq_bot] at ht

Premises used: Filter.eventually_false_iff_eq_bot, MeasureTheory.ae_eq_bot, Set.mem_empty_iff_false
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
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
inl : AEStronglyMeasurable (m₀ := m₀) f 0
⊢ AEStronglyMeasurable f μ

Tactic:
rw [ht]
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
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 (m₀ := m₀) f 0

Tactic:
aestronglyMeasurable_zero_measure f

Premises used: MeasureTheory.aestronglyMeasurable_zero_measure
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
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 (m₀ := m₀) f 0

Tactic:
exact aestronglyMeasurable_zero_measure f

Premises used: MeasureTheory.aestronglyMeasurable_zero_measure
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
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 : α → β), Measurable g ∧ range g ⊆ t ∧ f =ᶠ[ae μ] g

Tactic:
H.exists_ae_eq_range_subset ht h₀

Premises used: AEMeasurable.exists_ae_eq_range_subset
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
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
inr : ∀ (g : α → β) (g_meas : Measurable g) (gt : range g ⊆ t) (fg : f =ᶠ[ae μ] g), AEStronglyMeasurable f μ
⊢ 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₀

Premises used: AEMeasurable.exists_ae_eq_range_subset
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
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 μ

Tactic:
⟨g, ?_, fg⟩

Premises used: And.intro, Exists.intro, MeasureTheory.AEStronglyMeasurable
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
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
inr : StronglyMeasurable g
⊢ AEStronglyMeasurable f μ

Tactic:
refine ⟨g, ?_, fg⟩
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
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
⊢ StronglyMeasurable g

Tactic:
stronglyMeasurable_iff_measurable_separable.2 ⟨g_meas, t_sep.mono gt⟩

Premises used: Iff.mpr, stronglyMeasurable_iff_measurable_separable, And.intro, TopologicalSpace.IsSeparable.mono
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
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
⊢ StronglyMeasurable g

Tactic:
exact stronglyMeasurable_iff_measurable_separable.2 ⟨g_meas, t_sep.mono gt⟩

Premises used: Iff.mpr, stronglyMeasurable_iff_measurable_separable, And.intro, TopologicalSpace.IsSeparable.mono
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace β
m₀ : MeasurableSpace α
μ : Measure α
f : α → β
inst_1 : PseudoMetrizableSpace β
inst_2 : MeasurableSpace β
inst_3 : BorelSpace β
⊢ AEStronglyMeasurable f μ ↔ NullMeasurable f μ ∧ ∃ (t : Set β), IsSeparable t ∧ ∀ᵐ (x : α) ∂μ, f x ∈ t

Tactic:
aestronglyMeasurable_iff_aemeasurable_separable.trans <| and_congr_left fun ⟨_, hsep, h⟩ ↦
    have := hsep.secondCountableTopology
    ⟨AEMeasurable.nullMeasurable, fun hf ↦ hf.aemeasurable_of_aerange h⟩

Premises used: AEMeasurable.nullMeasurable, AEMeasurable, aestronglyMeasurable_iff_aemeasurable_separable, TopologicalSpace.IsSeparable.secondCountableTopology, _private.0.aestronglyMeasurable_iff_nullMeasurable_separable.match_1, MeasureTheory.NullMeasurable.aemeasurable_of_aerange, and_congr_left, Iff, Iff.intro, Iff.trans, MeasureTheory.NullMeasurable
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
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) μ

Tactic:
⟨fun H => H.comp_measurable hf.measurable, ?_⟩

Premises used: MeasureTheory.AEStronglyMeasurable.comp_measurable, Iff.intro, MeasurableEmbedding.measurable
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace β
γ : Type u_5
mγ : MeasurableSpace γ
mα : MeasurableSpace α
f : γ → α
μ : Measure γ
hf : MeasurableEmbedding f
g : α → β
refine : AEStronglyMeasurable (g ∘ f) μ → AEStronglyMeasurable (m₀ := mα) g (Measure.map f μ)
⊢ AEStronglyMeasurable (m₀ := mα) g (Measure.map f μ) ↔ AEStronglyMeasurable (g ∘ f) μ

Tactic:
refine ⟨fun H => H.comp_measurable hf.measurable, ?_⟩
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
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₁
rcases :
  ∀ (g₂ : α → β) (hgm₂ : StronglyMeasurable g₂) (hgm₁ : StronglyMeasurable (g₂ ∘ f)) (heq : g ∘ f =ᶠ[ae μ] g₂ ∘ f),
    AEStronglyMeasurable (m₀ := mα) g (Measure.map f μ)
⊢ AEStronglyMeasurable (m₀ := mα) g (Measure.map f μ)

Tactic:
rcases hf.exists_stronglyMeasurable_extend hgm₁ fun x => ⟨g x⟩ with ⟨g₂, hgm₂, rfl⟩

Premises used: MeasurableEmbedding.exists_stronglyMeasurable_extend, Nonempty.intro, rfl
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
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₂
hgm₁ : StronglyMeasurable (g₂ ∘ f)
heq : g ∘ f =ᶠ[ae μ] g₂ ∘ f
⊢ AEStronglyMeasurable (m₀ := mα) g (Measure.map f μ)

Tactic:
⟨g₂, hgm₂, hf.ae_map_iff.2 heq⟩

Premises used: Iff.mpr, And.intro, Exists.intro, MeasurableEmbedding.ae_map_iff, MeasureTheory.AEStronglyMeasurable
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
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₂
hgm₁ : StronglyMeasurable (g₂ ∘ f)
heq : g ∘ f =ᶠ[ae μ] g₂ ∘ f
⊢ AEStronglyMeasurable (m₀ := mα) g (Measure.map f μ)

Tactic:
exact ⟨g₂, hgm₂, hf.ae_map_iff.2 heq⟩
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
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 γ
⊢ let this := borel β;
  BorelSpace β

Tactic:
borelize β γ
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
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 β
⊢ let this := borel γ;
  BorelSpace γ

Tactic:
borelize β γ
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
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 μ

Tactic:
⟨fun H => aestronglyMeasurable_iff_aemeasurable_separable.2 ⟨?_, ?_⟩, fun H =>
      hg.continuous.comp_aestronglyMeasurable H⟩

Premises used: Iff.mpr, Continuous.comp_aestronglyMeasurable, aestronglyMeasurable_iff_aemeasurable_separable, And.intro, Iff.intro, Topology.IsEmbedding.continuous
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
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 μ
refine_2 :
  ∀ (H : AEStronglyMeasurable.{u_1, u_3} (β := γ) (fun (x : α) ↦ g (f x)) μ),
    ∃ (t : Set β), IsSeparable t ∧ ∀ᵐ (x : α) ∂μ, f x ∈ t
⊢ AEStronglyMeasurable.{u_1, u_3} (β := γ) (fun (x : α) ↦ g (f x)) μ ↔ AEStronglyMeasurable f μ

Tactic:
refine
    ⟨fun H => aestronglyMeasurable_iff_aemeasurable_separable.2 ⟨?_, ?_⟩, fun H =>
      hg.continuous.comp_aestronglyMeasurable H⟩
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
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
rw : IsClosed[instTopologicalSpaceSubtype] univ
⊢ IsClosed[instTopologicalSpaceSubtype] (range G)

Tactic:
rw [rangeFactorization_surjective.range_eq]

Premises used: Function.Surjective.range_eq, Set.rangeFactorization_surjective
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
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] univ

Tactic:
isClosed_univ

Premises used: isClosed_univ
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
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] univ

Tactic:
exact isClosed_univ

Premises used: isClosed_univ
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
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
⊢ IsClosedEmbedding G

Tactic:
have hG : IsClosedEmbedding G :=
      { hg.codRestrict _ _ with
        isClosed_range := by rw [rangeFactorization_surjective.range_eq]; exact isClosed_univ }