α : Type u_1
β : Type u_3
γ : Type u_2
ι : Type ?u.221813
inst✝¹ : Countable ι
f✝ g✝ f : α → β
g : α → γ
g' : γ → β
mα : MeasurableSpace α
mγ : MeasurableSpace γ
inst✝ : TopologicalSpace β
hg : MeasurableEmbedding g
hf : StronglyMeasurable f
hg' : StronglyMeasurable g'
⊢ ∀ (x : γ),
    Tendsto
      (fun n =>
        ↑((fun n => SimpleFunc.extend (StronglyMeasurable.approx hf n) g hg (StronglyMeasurable.approx hg' n)) n) x)
      atTop (𝓝 (Function.extend g f g' x))
α : Type u_1
β : Type u_3
γ : Type u_2
ι : Type ?u.221813
inst✝¹ : Countable ι
f✝ g✝ f : α → β
g : α → γ
g' : γ → β
mα : MeasurableSpace α
mγ : MeasurableSpace γ
inst✝ : TopologicalSpace β
hg : MeasurableEmbedding g
hf : StronglyMeasurable f
hg' : StronglyMeasurable g'
⊢ StronglyMeasurable (Function.extend g f g')
refine' ⟨fun n => SimpleFunc.extend (hf.approx n) g hg (hg'.approx n), _⟩
α : Type u_1
β : Type u_3
γ : Type u_2
ι : Type ?u.221813
inst✝¹ : Countable ι
f✝ g✝ f : α → β
g : α → γ
g' : γ → β
mα : MeasurableSpace α
mγ : MeasurableSpace γ
inst✝ : TopologicalSpace β
hg : MeasurableEmbedding g
hf : StronglyMeasurable f
hg' : StronglyMeasurable g'
x : γ
⊢ Tendsto
    (fun n =>
      ↑((fun n => SimpleFunc.extend (StronglyMeasurable.approx hf n) g hg (StronglyMeasurable.approx hg' n)) n) x)
    atTop (𝓝 (Function.extend g f g' x))
α : Type u_1
β : Type u_3
γ : Type u_2
ι : Type ?u.221813
inst✝¹ : Countable ι
f✝ g✝ f : α → β
g : α → γ
g' : γ → β
mα : MeasurableSpace α
mγ : MeasurableSpace γ
inst✝ : TopologicalSpace β
hg : MeasurableEmbedding g
hf : StronglyMeasurable f
hg' : StronglyMeasurable g'
⊢ ∀ (x : γ),
    Tendsto
      (fun n =>
        ↑((fun n => SimpleFunc.extend (StronglyMeasurable.approx hf n) g hg (StronglyMeasurable.approx hg' n)) n) x)
      atTop (𝓝 (Function.extend g f g' x))
intro x
case pos
α : Type u_1
β : Type u_3
γ : Type u_2
ι : Type ?u.221813
inst✝¹ : Countable ι
f✝ g✝ f : α → β
g : α → γ
g' : γ → β
mα : MeasurableSpace α
mγ : MeasurableSpace γ
inst✝ : TopologicalSpace β
hg : MeasurableEmbedding g
hf : StronglyMeasurable f
hg' : StronglyMeasurable g'
x : γ
hx : ∃ y, g y = x
⊢ Tendsto
    (fun n =>
      ↑((fun n => SimpleFunc.extend (StronglyMeasurable.approx hf n) g hg (StronglyMeasurable.approx hg' n)) n) x)
    atTop (𝓝 (Function.extend g f g' x))

case neg
α : Type u_1
β : Type u_3
γ : Type u_2
ι : Type ?u.221813
inst✝¹ : Countable ι
f✝ g✝ f : α → β
g : α → γ
g' : γ → β
mα : MeasurableSpace α
mγ : MeasurableSpace γ
inst✝ : TopologicalSpace β
hg : MeasurableEmbedding g
hf : StronglyMeasurable f
hg' : StronglyMeasurable g'
x : γ
hx : ¬∃ y, g y = x
⊢ Tendsto
    (fun n =>
      ↑((fun n => SimpleFunc.extend (StronglyMeasurable.approx hf n) g hg (StronglyMeasurable.approx hg' n)) n) x)
    atTop (𝓝 (Function.extend g f g' x))
α : Type u_1
β : Type u_3
γ : Type u_2
ι : Type ?u.221813
inst✝¹ : Countable ι
f✝ g✝ f : α → β
g : α → γ
g' : γ → β
mα : MeasurableSpace α
mγ : MeasurableSpace γ
inst✝ : TopologicalSpace β
hg : MeasurableEmbedding g
hf : StronglyMeasurable f
hg' : StronglyMeasurable g'
x : γ
⊢ Tendsto
    (fun n =>
      ↑((fun n => SimpleFunc.extend (StronglyMeasurable.approx hf n) g hg (StronglyMeasurable.approx hg' n)) n) x)
    atTop (𝓝 (Function.extend g f g' x))
by_cases hx : ∃ y, g y = x
case pos.intro
α : Type u_1
β : Type u_3
γ : Type u_2
ι : Type ?u.221813
inst✝¹ : Countable ι
f✝ g✝ f : α → β
g : α → γ
g' : γ → β
mα : MeasurableSpace α
mγ : MeasurableSpace γ
inst✝ : TopologicalSpace β
hg : MeasurableEmbedding g
hf : StronglyMeasurable f
hg' : StronglyMeasurable g'
y : α
⊢ Tendsto
    (fun n =>
      ↑((fun n => SimpleFunc.extend (StronglyMeasurable.approx hf n) g hg (StronglyMeasurable.approx hg' n)) n) (g y))
    atTop (𝓝 (Function.extend g f g' (g y)))
case pos
α : Type u_1
β : Type u_3
γ : Type u_2
ι : Type ?u.221813
inst✝¹ : Countable ι
f✝ g✝ f : α → β
g : α → γ
g' : γ → β
mα : MeasurableSpace α
mγ : MeasurableSpace γ
inst✝ : TopologicalSpace β
hg : MeasurableEmbedding g
hf : StronglyMeasurable f
hg' : StronglyMeasurable g'
x : γ
hx : ∃ y, g y = x
⊢ Tendsto
    (fun n =>
      ↑((fun n => SimpleFunc.extend (StronglyMeasurable.approx hf n) g hg (StronglyMeasurable.approx hg' n)) n) x)
    atTop (𝓝 (Function.extend g f g' x))
rcases hx with ⟨y, rfl⟩
no goals
case pos.intro
α : Type u_1
β : Type u_3
γ : Type u_2
ι : Type ?u.221813
inst✝¹ : Countable ι
f✝ g✝ f : α → β
g : α → γ
g' : γ → β
mα : MeasurableSpace α
mγ : MeasurableSpace γ
inst✝ : TopologicalSpace β
hg : MeasurableEmbedding g
hf : StronglyMeasurable f
hg' : StronglyMeasurable g'
y : α
⊢ Tendsto
    (fun n =>
      ↑((fun n => SimpleFunc.extend (StronglyMeasurable.approx hf n) g hg (StronglyMeasurable.approx hg' n)) n) (g y))
    atTop (𝓝 (Function.extend g f g' (g y)))
simpa only [SimpleFunc.extend_apply, hg.injective, Injective.extend_apply] using
  hf.tendsto_approx y
no goals
case neg
α : Type u_1
β : Type u_3
γ : Type u_2
ι : Type ?u.221813
inst✝¹ : Countable ι
f✝ g✝ f : α → β
g : α → γ
g' : γ → β
mα : MeasurableSpace α
mγ : MeasurableSpace γ
inst✝ : TopologicalSpace β
hg : MeasurableEmbedding g
hf : StronglyMeasurable f
hg' : StronglyMeasurable g'
x : γ
hx : ¬∃ y, g y = x
⊢ Tendsto
    (fun n =>
      ↑((fun n => SimpleFunc.extend (StronglyMeasurable.approx hf n) g hg (StronglyMeasurable.approx hg' n)) n) x)
    atTop (𝓝 (Function.extend g f g' x))
simpa only [hx, SimpleFunc.extend_apply', not_false_iff, extend_apply'] using
  hg'.tendsto_approx x