α : Type u_3
β : Type u_1
γ : Type u_2
ι : Type ?u.351271
inst✝⁴ : Countable ι
m : MeasurableSpace α
μ : Measure α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace γ
f✝ g✝ : α → β
inst✝¹ : PseudoMetrizableSpace β
inst✝ : PseudoMetrizableSpace γ
g : β → γ
f : α → β
hg : _root_.Embedding g
this : PseudoMetricSpace γ := pseudoMetrizableSpacePseudoMetric γ
⊢ AEStronglyMeasurable (fun x => g (f x)) μ ↔ AEStronglyMeasurable f μ
α : Type u_3
β : Type u_1
γ : Type u_2
ι : Type ?u.351271
inst✝⁴ : Countable ι
m : MeasurableSpace α
μ : Measure α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace γ
f✝ g✝ : α → β
inst✝¹ : PseudoMetrizableSpace β
inst✝ : PseudoMetrizableSpace γ
g : β → γ
f : α → β
hg : _root_.Embedding g
⊢ AEStronglyMeasurable (fun x => g (f x)) μ ↔ AEStronglyMeasurable f μ
letI := pseudoMetrizableSpacePseudoMetric γ
α : Type u_3
β : Type u_1
γ : Type u_2
ι : Type ?u.351271
inst✝⁴ : Countable ι
m : MeasurableSpace α
μ : Measure α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace γ
f✝ g✝ : α → β
inst✝¹ : PseudoMetrizableSpace β
inst✝ : PseudoMetrizableSpace γ
g : β → γ
f : α → β
hg : _root_.Embedding g
this : PseudoMetricSpace γ := pseudoMetrizableSpacePseudoMetric γ
this✝³ : MeasurableSpace β := borel β
this✝² : BorelSpace β
this✝¹ : MeasurableSpace γ := borel γ
this✝ : BorelSpace γ
⊢ AEStronglyMeasurable (fun x => g (f x)) μ ↔ AEStronglyMeasurable f μ
α : Type u_3
β : Type u_1
γ : Type u_2
ι : Type ?u.351271
inst✝⁴ : Countable ι
m : MeasurableSpace α
μ : Measure α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace γ
f✝ g✝ : α → β
inst✝¹ : PseudoMetrizableSpace β
inst✝ : PseudoMetrizableSpace γ
g : β → γ
f : α → β
hg : _root_.Embedding g
this : PseudoMetricSpace γ := pseudoMetrizableSpacePseudoMetric γ
⊢ AEStronglyMeasurable (fun x => g (f x)) μ ↔ AEStronglyMeasurable f μ
borelize β γ
case refine'_1
α : Type u_3
β : Type u_1
γ : Type u_2
ι : Type ?u.351271
inst✝⁴ : Countable ι
m : MeasurableSpace α
μ : Measure α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace γ
f✝ g✝ : α → β
inst✝¹ : PseudoMetrizableSpace β
inst✝ : PseudoMetrizableSpace γ
g : β → γ
f : α → β
hg : _root_.Embedding g
this : PseudoMetricSpace γ := pseudoMetrizableSpacePseudoMetric γ
this✝³ : MeasurableSpace β := borel β
this✝² : BorelSpace β
this✝¹ : MeasurableSpace γ := borel γ
this✝ : BorelSpace γ
H : AEStronglyMeasurable (fun x => g (f x)) μ
⊢ AEMeasurable f

case refine'_2
α : Type u_3
β : Type u_1
γ : Type u_2
ι : Type ?u.351271
inst✝⁴ : Countable ι
m : MeasurableSpace α
μ : Measure α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace γ
f✝ g✝ : α → β
inst✝¹ : PseudoMetrizableSpace β
inst✝ : PseudoMetrizableSpace γ
g : β → γ
f : α → β
hg : _root_.Embedding g
this : PseudoMetricSpace γ := pseudoMetrizableSpacePseudoMetric γ
this✝³ : MeasurableSpace β := borel β
this✝² : BorelSpace β
this✝¹ : MeasurableSpace γ := borel γ
this✝ : BorelSpace γ
H : AEStronglyMeasurable (fun x => g (f x)) μ
⊢ ∃ t, IsSeparable t ∧ ∀ᵐ (x : α) ∂μ, f x ∈ t
α : Type u_3
β : Type u_1
γ : Type u_2
ι : Type ?u.351271
inst✝⁴ : Countable ι
m : MeasurableSpace α
μ : Measure α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace γ
f✝ g✝ : α → β
inst✝¹ : PseudoMetrizableSpace β
inst✝ : PseudoMetrizableSpace γ
g : β → γ
f : α → β
hg : _root_.Embedding g
this : PseudoMetricSpace γ := pseudoMetrizableSpacePseudoMetric γ
this✝³ : MeasurableSpace β := borel β
this✝² : BorelSpace β
this✝¹ : MeasurableSpace γ := borel γ
this✝ : BorelSpace γ
⊢ AEStronglyMeasurable (fun x => g (f x)) μ ↔ AEStronglyMeasurable f μ
refine'
  ⟨fun H => aestronglyMeasurable_iff_aemeasurable_separable.2 ⟨_, _⟩, fun H =>
    hg.continuous.comp_aestronglyMeasurable H⟩
case refine'_1
α : Type u_3
β : Type u_1
γ : Type u_2
ι : Type ?u.351271
inst✝⁴ : Countable ι
m : MeasurableSpace α
μ : Measure α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace γ
f✝ g✝ : α → β
inst✝¹ : PseudoMetrizableSpace β
inst✝ : PseudoMetrizableSpace γ
g : β → γ
f : α → β
hg : _root_.Embedding g
this : PseudoMetricSpace γ := pseudoMetrizableSpacePseudoMetric γ
this✝³ : MeasurableSpace β := borel β
this✝² : BorelSpace β
this✝¹ : MeasurableSpace γ := borel γ
this✝ : BorelSpace γ
H : AEStronglyMeasurable (fun x => g (f x)) μ
G : β → ↑(range g) := codRestrict g (range g) (_ : ∀ (i : β), g i ∈ range fun x => g x)
⊢ AEMeasurable f
case refine'_1
α : Type u_3
β : Type u_1
γ : Type u_2
ι : Type ?u.351271
inst✝⁴ : Countable ι
m : MeasurableSpace α
μ : Measure α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace γ
f✝ g✝ : α → β
inst✝¹ : PseudoMetrizableSpace β
inst✝ : PseudoMetrizableSpace γ
g : β → γ
f : α → β
hg : _root_.Embedding g
this : PseudoMetricSpace γ := pseudoMetrizableSpacePseudoMetric γ
this✝³ : MeasurableSpace β := borel β
this✝² : BorelSpace β
this✝¹ : MeasurableSpace γ := borel γ
this✝ : BorelSpace γ
H : AEStronglyMeasurable (fun x => g (f x)) μ
⊢ AEMeasurable f
let G : β → range g := codRestrict g (range g) mem_range_self
case refine'_1
α : Type u_3
β : Type u_1
γ : Type u_2
ι : Type ?u.351271
inst✝⁴ : Countable ι
m : MeasurableSpace α
μ : Measure α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace γ
f✝ g✝ : α → β
inst✝¹ : PseudoMetrizableSpace β
inst✝ : PseudoMetrizableSpace γ
g : β → γ
f : α → β
hg : _root_.Embedding g
this : PseudoMetricSpace γ := pseudoMetrizableSpacePseudoMetric γ
this✝³ : MeasurableSpace β := borel β
this✝² : BorelSpace β
this✝¹ : MeasurableSpace γ := borel γ
this✝ : BorelSpace γ
H : AEStronglyMeasurable (fun x => g (f x)) μ
G : β → ↑(range g) := codRestrict g (range g) (_ : ∀ (i : β), g i ∈ range fun x => g x)
hG : ClosedEmbedding G
⊢ AEMeasurable f
case refine'_1
α : Type u_3
β : Type u_1
γ : Type u_2
ι : Type ?u.351271
inst✝⁴ : Countable ι
m : MeasurableSpace α
μ : Measure α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace γ
f✝ g✝ : α → β
inst✝¹ : PseudoMetrizableSpace β
inst✝ : PseudoMetrizableSpace γ
g : β → γ
f : α → β
hg : _root_.Embedding g
this : PseudoMetricSpace γ := pseudoMetrizableSpacePseudoMetric γ
this✝³ : MeasurableSpace β := borel β
this✝² : BorelSpace β
this✝¹ : MeasurableSpace γ := borel γ
this✝ : BorelSpace γ
H : AEStronglyMeasurable (fun x => g (f x)) μ
G : β → ↑(range g) := codRestrict g (range g) (_ : ∀ (i : β), g i ∈ range fun x => g x)
⊢ AEMeasurable f
have hG : ClosedEmbedding G :=
  { hg.codRestrict _ _ with
    closed_range := by
      convert isClosed_univ (α := ↥(range g))
      apply eq_univ_of_forall
      rintro ⟨-, ⟨x, rfl⟩⟩
      exact mem_range_self x }
case refine'_1
α : Type u_3
β : Type u_1
γ : Type u_2
ι : Type ?u.351271
inst✝⁴ : Countable ι
m : MeasurableSpace α
μ : Measure α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace γ
f✝ g✝ : α → β
inst✝¹ : PseudoMetrizableSpace β
inst✝ : PseudoMetrizableSpace γ
g : β → γ
f : α → β
hg : _root_.Embedding g
this✝⁴ : PseudoMetricSpace γ := pseudoMetrizableSpacePseudoMetric γ
this✝³ : MeasurableSpace β := borel β
this✝² : BorelSpace β
this✝¹ : MeasurableSpace γ := borel γ
this✝ : BorelSpace γ
H : AEStronglyMeasurable (fun x => g (f x)) μ
G : β → ↑(range g) := codRestrict g (range g) (_ : ∀ (i : β), g i ∈ range fun x => g x)
hG : ClosedEmbedding G
this : AEMeasurable (G ∘ f)
⊢ AEMeasurable f
case refine'_1
α : Type u_3
β : Type u_1
γ : Type u_2
ι : Type ?u.351271
inst✝⁴ : Countable ι
m : MeasurableSpace α
μ : Measure α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace γ
f✝ g✝ : α → β
inst✝¹ : PseudoMetrizableSpace β
inst✝ : PseudoMetrizableSpace γ
g : β → γ
f : α → β
hg : _root_.Embedding g
this : PseudoMetricSpace γ := pseudoMetrizableSpacePseudoMetric γ
this✝³ : MeasurableSpace β := borel β
this✝² : BorelSpace β
this✝¹ : MeasurableSpace γ := borel γ
this✝ : BorelSpace γ
H : AEStronglyMeasurable (fun x => g (f x)) μ
G : β → ↑(range g) := codRestrict g (range g) (_ : ∀ (i : β), g i ∈ range fun x => g x)
hG : ClosedEmbedding G
⊢ AEMeasurable f
have : AEMeasurable (G ∘ f) μ := AEMeasurable.subtype_mk H.aemeasurable
no goals
case refine'_1
α : Type u_3
β : Type u_1
γ : Type u_2
ι : Type ?u.351271
inst✝⁴ : Countable ι
m : MeasurableSpace α
μ : Measure α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace γ
f✝ g✝ : α → β
inst✝¹ : PseudoMetrizableSpace β
inst✝ : PseudoMetrizableSpace γ
g : β → γ
f : α → β
hg : _root_.Embedding g
this✝⁴ : PseudoMetricSpace γ := pseudoMetrizableSpacePseudoMetric γ
this✝³ : MeasurableSpace β := borel β
this✝² : BorelSpace β
this✝¹ : MeasurableSpace γ := borel γ
this✝ : BorelSpace γ
H : AEStronglyMeasurable (fun x => g (f x)) μ
G : β → ↑(range g) := codRestrict g (range g) (_ : ∀ (i : β), g i ∈ range fun x => g x)
hG : ClosedEmbedding G
this : AEMeasurable (G ∘ f)
⊢ AEMeasurable f
exact hG.measurableEmbedding.aemeasurable_comp_iff.1 this
case h.e'_3
α : Type u_3
β : Type u_1
γ : Type u_2
ι : Type ?u.351271
inst✝⁴ : Countable ι
m : MeasurableSpace α
μ : Measure α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace γ
f✝ g✝ : α → β
inst✝¹ : PseudoMetrizableSpace β
inst✝ : PseudoMetrizableSpace γ
g : β → γ
f : α → β
hg : _root_.Embedding g
this : PseudoMetricSpace γ := pseudoMetrizableSpacePseudoMetric γ
this✝³ : MeasurableSpace β := borel β
this✝² : BorelSpace β
this✝¹ : MeasurableSpace γ := borel γ
this✝ : BorelSpace γ
H : AEStronglyMeasurable (fun x => g (f x)) μ
G : β → ↑(range g) := codRestrict g (range g) (_ : ∀ (i : β), g i ∈ range fun x => g x)
src✝ : _root_.Embedding (codRestrict g (range g) (_ : ∀ (i : β), g i ∈ range fun x => g x)) :=
  Embedding.codRestrict hg (range g) mem_range_self
⊢ range G = univ
α : Type u_3
β : Type u_1
γ : Type u_2
ι : Type ?u.351271
inst✝⁴ : Countable ι
m : MeasurableSpace α
μ : Measure α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace γ
f✝ g✝ : α → β
inst✝¹ : PseudoMetrizableSpace β
inst✝ : PseudoMetrizableSpace γ
g : β → γ
f : α → β
hg : _root_.Embedding g
this : PseudoMetricSpace γ := pseudoMetrizableSpacePseudoMetric γ
this✝³ : MeasurableSpace β := borel β
this✝² : BorelSpace β
this✝¹ : MeasurableSpace γ := borel γ
this✝ : BorelSpace γ
H : AEStronglyMeasurable (fun x => g (f x)) μ
G : β → ↑(range g) := codRestrict g (range g) (_ : ∀ (i : β), g i ∈ range fun x => g x)
src✝ : _root_.Embedding (codRestrict g (range g) (_ : ∀ (i : β), g i ∈ range fun x => g x)) :=
  Embedding.codRestrict hg (range g) mem_range_self
⊢ IsClosed (range G)
convert isClosed_univ (α := ↥(range g))
case h.e'_3.a
α : Type u_3
β : Type u_1
γ : Type u_2
ι : Type ?u.351271
inst✝⁴ : Countable ι
m : MeasurableSpace α
μ : Measure α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace γ
f✝ g✝ : α → β
inst✝¹ : PseudoMetrizableSpace β
inst✝ : PseudoMetrizableSpace γ
g : β → γ
f : α → β
hg : _root_.Embedding g
this : PseudoMetricSpace γ := pseudoMetrizableSpacePseudoMetric γ
this✝³ : MeasurableSpace β := borel β
this✝² : BorelSpace β
this✝¹ : MeasurableSpace γ := borel γ
this✝ : BorelSpace γ
H : AEStronglyMeasurable (fun x => g (f x)) μ
G : β → ↑(range g) := codRestrict g (range g) (_ : ∀ (i : β), g i ∈ range fun x => g x)
src✝ : _root_.Embedding (codRestrict g (range g) (_ : ∀ (i : β), g i ∈ range fun x => g x)) :=
  Embedding.codRestrict hg (range g) mem_range_self
⊢ ∀ (x : ↑(range g)), x ∈ range G
case h.e'_3
α : Type u_3
β : Type u_1
γ : Type u_2
ι : Type ?u.351271
inst✝⁴ : Countable ι
m : MeasurableSpace α
μ : Measure α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace γ
f✝ g✝ : α → β
inst✝¹ : PseudoMetrizableSpace β
inst✝ : PseudoMetrizableSpace γ
g : β → γ
f : α → β
hg : _root_.Embedding g
this : PseudoMetricSpace γ := pseudoMetrizableSpacePseudoMetric γ
this✝³ : MeasurableSpace β := borel β
this✝² : BorelSpace β
this✝¹ : MeasurableSpace γ := borel γ
this✝ : BorelSpace γ
H : AEStronglyMeasurable (fun x => g (f x)) μ
G : β → ↑(range g) := codRestrict g (range g) (_ : ∀ (i : β), g i ∈ range fun x => g x)
src✝ : _root_.Embedding (codRestrict g (range g) (_ : ∀ (i : β), g i ∈ range fun x => g x)) :=
  Embedding.codRestrict hg (range g) mem_range_self
⊢ range G = univ
apply eq_univ_of_forall
case h.e'_3.a.mk.intro
α : Type u_3
β : Type u_1
γ : Type u_2
ι : Type ?u.351271
inst✝⁴ : Countable ι
m : MeasurableSpace α
μ : Measure α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace γ
f✝ g✝ : α → β
inst✝¹ : PseudoMetrizableSpace β
inst✝ : PseudoMetrizableSpace γ
g : β → γ
f : α → β
hg : _root_.Embedding g
this : PseudoMetricSpace γ := pseudoMetrizableSpacePseudoMetric γ
this✝³ : MeasurableSpace β := borel β
this✝² : BorelSpace β
this✝¹ : MeasurableSpace γ := borel γ
this✝ : BorelSpace γ
H : AEStronglyMeasurable (fun x => g (f x)) μ
G : β → ↑(range g) := codRestrict g (range g) (_ : ∀ (i : β), g i ∈ range fun x => g x)
src✝ : _root_.Embedding (codRestrict g (range g) (_ : ∀ (i : β), g i ∈ range fun x => g x)) :=
  Embedding.codRestrict hg (range g) mem_range_self
x : β
⊢ { val := g x, property := (_ : ∃ y, g y = g x) } ∈ range G
case h.e'_3.a
α : Type u_3
β : Type u_1
γ : Type u_2
ι : Type ?u.351271
inst✝⁴ : Countable ι
m : MeasurableSpace α
μ : Measure α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace γ
f✝ g✝ : α → β
inst✝¹ : PseudoMetrizableSpace β
inst✝ : PseudoMetrizableSpace γ
g : β → γ
f : α → β
hg : _root_.Embedding g
this : PseudoMetricSpace γ := pseudoMetrizableSpacePseudoMetric γ
this✝³ : MeasurableSpace β := borel β
this✝² : BorelSpace β
this✝¹ : MeasurableSpace γ := borel γ
this✝ : BorelSpace γ
H : AEStronglyMeasurable (fun x => g (f x)) μ
G : β → ↑(range g) := codRestrict g (range g) (_ : ∀ (i : β), g i ∈ range fun x => g x)
src✝ : _root_.Embedding (codRestrict g (range g) (_ : ∀ (i : β), g i ∈ range fun x => g x)) :=
  Embedding.codRestrict hg (range g) mem_range_self
⊢ ∀ (x : ↑(range g)), x ∈ range G
rintro ⟨-, ⟨x, rfl⟩⟩
no goals
case h.e'_3.a.mk.intro
α : Type u_3
β : Type u_1
γ : Type u_2
ι : Type ?u.351271
inst✝⁴ : Countable ι
m : MeasurableSpace α
μ : Measure α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace γ
f✝ g✝ : α → β
inst✝¹ : PseudoMetrizableSpace β
inst✝ : PseudoMetrizableSpace γ
g : β → γ
f : α → β
hg : _root_.Embedding g
this : PseudoMetricSpace γ := pseudoMetrizableSpacePseudoMetric γ
this✝³ : MeasurableSpace β := borel β
this✝² : BorelSpace β
this✝¹ : MeasurableSpace γ := borel γ
this✝ : BorelSpace γ
H : AEStronglyMeasurable (fun x => g (f x)) μ
G : β → ↑(range g) := codRestrict g (range g) (_ : ∀ (i : β), g i ∈ range fun x => g x)
src✝ : _root_.Embedding (codRestrict g (range g) (_ : ∀ (i : β), g i ∈ range fun x => g x)) :=
  Embedding.codRestrict hg (range g) mem_range_self
x : β
⊢ { val := g x, property := (_ : ∃ y, g y = g x) } ∈ range G
exact mem_range_self x
case refine'_2.intro.intro
α : Type u_3
β : Type u_1
γ : Type u_2
ι : Type ?u.351271
inst✝⁴ : Countable ι
m : MeasurableSpace α
μ : Measure α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace γ
f✝ g✝ : α → β
inst✝¹ : PseudoMetrizableSpace β
inst✝ : PseudoMetrizableSpace γ
g : β → γ
f : α → β
hg : _root_.Embedding g
this : PseudoMetricSpace γ := pseudoMetrizableSpacePseudoMetric γ
this✝³ : MeasurableSpace β := borel β
this✝² : BorelSpace β
this✝¹ : MeasurableSpace γ := borel γ
this✝ : BorelSpace γ
H : AEStronglyMeasurable (fun x => g (f x)) μ
t : Set γ
ht : IsSeparable t
h't : ∀ᵐ (x : α) ∂μ, g (f x) ∈ t
⊢ ∃ t, IsSeparable t ∧ ∀ᵐ (x : α) ∂μ, f x ∈ t
case refine'_2
α : Type u_3
β : Type u_1
γ : Type u_2
ι : Type ?u.351271
inst✝⁴ : Countable ι
m : MeasurableSpace α
μ : Measure α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace γ
f✝ g✝ : α → β
inst✝¹ : PseudoMetrizableSpace β
inst✝ : PseudoMetrizableSpace γ
g : β → γ
f : α → β
hg : _root_.Embedding g
this : PseudoMetricSpace γ := pseudoMetrizableSpacePseudoMetric γ
this✝³ : MeasurableSpace β := borel β
this✝² : BorelSpace β
this✝¹ : MeasurableSpace γ := borel γ
this✝ : BorelSpace γ
H : AEStronglyMeasurable (fun x => g (f x)) μ
⊢ ∃ t, IsSeparable t ∧ ∀ᵐ (x : α) ∂μ, f x ∈ t
rcases(aestronglyMeasurable_iff_aemeasurable_separable.1 H).2 with ⟨t, ht, h't⟩
no goals
case refine'_2.intro.intro
α : Type u_3
β : Type u_1
γ : Type u_2
ι : Type ?u.351271
inst✝⁴ : Countable ι
m : MeasurableSpace α
μ : Measure α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace γ
f✝ g✝ : α → β
inst✝¹ : PseudoMetrizableSpace β
inst✝ : PseudoMetrizableSpace γ
g : β → γ
f : α → β
hg : _root_.Embedding g
this : PseudoMetricSpace γ := pseudoMetrizableSpacePseudoMetric γ
this✝³ : MeasurableSpace β := borel β
this✝² : BorelSpace β
this✝¹ : MeasurableSpace γ := borel γ
this✝ : BorelSpace γ
H : AEStronglyMeasurable (fun x => g (f x)) μ
t : Set γ
ht : IsSeparable t
h't : ∀ᵐ (x : α) ∂μ, g (f x) ∈ t
⊢ ∃ t, IsSeparable t ∧ ∀ᵐ (x : α) ∂μ, f x ∈ t
exact ⟨g ⁻¹' t, hg.isSeparable_preimage ht, h't⟩