-- Mathlib/MeasureTheory/Function/StronglyMeasurable/Basic.lean
theorem _root_.MeasurableEmbedding.stronglyMeasurable_extend {f : α → β} {g : α → γ} {g' : γ → β}
    {mα : MeasurableSpace α} {mγ : MeasurableSpace γ} [TopologicalSpace β]
    (hg : MeasurableEmbedding g) (hf : StronglyMeasurable f) (hg' : StronglyMeasurable g') :
    StronglyMeasurable (Function.extend g f g')

Proof state:
case pos.intro
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
g : α → γ
g' : γ → β
mα : MeasurableSpace α
mγ : MeasurableSpace γ
inst✝ : TopologicalSpace β
hg : MeasurableEmbedding g
hf : StronglyMeasurable f
hg' : StronglyMeasurable g'
y : α
⊢ Tendsto (fun n => ((fun n => (hf.approx n).extend g hg (hg'.approx n)) n) (g y)) atTop
    (𝓝 (Function.extend g f g' (g y)))

Tactic:
simpa only [SimpleFunc.extend_apply, hg.injective, Injective.extend_apply] using
  hf.tendsto_approx y

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
g : α → γ
g' : γ → β
mα : MeasurableSpace α
mγ : MeasurableSpace γ
inst✝ : TopologicalSpace β
hg : MeasurableEmbedding g
hf : StronglyMeasurable f
hg' : StronglyMeasurable g'
⊢ ∀ (x : γ),
    Tendsto (fun n => ((fun n => (hf.approx n).extend g hg (hg'.approx n)) n) x) atTop (𝓝 (Function.extend g f g' x))

Tactic:
intro x

Result:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
g : α → γ
g' : γ → β
mα : MeasurableSpace α
mγ : MeasurableSpace γ
inst✝ : TopologicalSpace β
hg : MeasurableEmbedding g
hf : StronglyMeasurable f
hg' : StronglyMeasurable g'
x : γ
⊢ Tendsto (fun n => ((fun n => (hf.approx n).extend g hg (hg'.approx n)) n) x) atTop (𝓝 (Function.extend g f g' x))

Proof state:
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
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 => (hf.approx n).extend g hg (hg'.approx n)) n) x) atTop (𝓝 (Function.extend g f g' x))

Tactic:
rcases hx with ⟨y, rfl⟩

Result:
case pos.intro
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
g : α → γ
g' : γ → β
mα : MeasurableSpace α
mγ : MeasurableSpace γ
inst✝ : TopologicalSpace β
hg : MeasurableEmbedding g
hf : StronglyMeasurable f
hg' : StronglyMeasurable g'
y : α
⊢ Tendsto (fun n => ((fun n => (hf.approx n).extend g hg (hg'.approx n)) n) (g y)) atTop
    (𝓝 (Function.extend g f g' (g y)))

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
g : α → γ
g' : γ → β
mα : MeasurableSpace α
mγ : MeasurableSpace γ
inst✝ : TopologicalSpace β
hg : MeasurableEmbedding g
hf : StronglyMeasurable f
hg' : StronglyMeasurable g'
⊢ StronglyMeasurable (Function.extend g f g')

Tactic:
refine ⟨fun n => SimpleFunc.extend (hf.approx n) g hg (hg'.approx n), ?_⟩

Result:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
g : α → γ
g' : γ → β
mα : MeasurableSpace α
mγ : MeasurableSpace γ
inst✝ : TopologicalSpace β
hg : MeasurableEmbedding g
hf : StronglyMeasurable f
hg' : StronglyMeasurable g'
⊢ ∀ (x : γ),
    Tendsto (fun n => ((fun n => (hf.approx n).extend g hg (hg'.approx n)) n) x) atTop (𝓝 (Function.extend g f g' x))

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
g : α → γ
g' : γ → β
mα : MeasurableSpace α
mγ : MeasurableSpace γ
inst✝ : TopologicalSpace β
hg : MeasurableEmbedding g
hf : StronglyMeasurable f
hg' : StronglyMeasurable g'
x : γ
⊢ Tendsto (fun n => ((fun n => (hf.approx n).extend g hg (hg'.approx n)) n) x) atTop (𝓝 (Function.extend g f g' x))

Tactic:
by_cases hx : ∃ y, g y = x

Result:
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
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 => (hf.approx n).extend g hg (hg'.approx n)) n) x) atTop (𝓝 (Function.extend g f g' x))

case neg
α : Type u_1
β : Type u_2
γ : Type u_3
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 => (hf.approx n).extend g hg (hg'.approx n)) n) x) atTop (𝓝 (Function.extend g f g' x))

Proof state:
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
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 => (hf.approx n).extend g hg (hg'.approx n)) n) x) atTop (𝓝 (Function.extend g f g' x))

Tactic:
simpa only [hx, SimpleFunc.extend_apply', not_false_iff, extend_apply'] using
  hg'.tendsto_approx x

Result:
no goals