-- Mathlib/MeasureTheory/Function/StronglyMeasurable/Basic.lean
theorem _root_.Measurable.add_stronglyMeasurable
    {α E : Type*} {_ : MeasurableSpace α} [AddGroup E] [TopologicalSpace E]
    [MeasurableSpace E] [BorelSpace E] [ContinuousAdd E] [PseudoMetrizableSpace E]
    {g f : α → E} (hg : Measurable g) (hf : StronglyMeasurable f) :
    Measurable (g + f)

Proof state:
case intro
α : Type u_5
E : Type u_6
x✝ : MeasurableSpace α
inst✝⁵ : AddGroup E
inst✝⁴ : TopologicalSpace E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : ContinuousAdd E
inst✝ : PseudoMetrizableSpace E
g f : α → E
hg : Measurable g
φ : ℕ → α →ₛ E
hφ : ∀ (x : α), Tendsto (fun n => (φ n) x) atTop (𝓝 (f x))
⊢ Measurable (g + f)

Tactic:
have : Tendsto (fun n x ↦ g x + φ n x) atTop (𝓝 (g + f)) :=
  tendsto_pi_nhds.2 (fun x ↦ tendsto_const_nhds.add (hφ x))

Result:
case intro
α : Type u_5
E : Type u_6
x✝ : MeasurableSpace α
inst✝⁵ : AddGroup E
inst✝⁴ : TopologicalSpace E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : ContinuousAdd E
inst✝ : PseudoMetrizableSpace E
g f : α → E
hg : Measurable g
φ : ℕ → α →ₛ E
hφ : ∀ (x : α), Tendsto (fun n => (φ n) x) atTop (𝓝 (f x))
this : Tendsto (fun n x => g x + (φ n) x) atTop (𝓝 (g + f))
⊢ Measurable (g + f)

Proof state:
α : Type u_5
E : Type u_6
x✝ : MeasurableSpace α
inst✝⁵ : AddGroup E
inst✝⁴ : TopologicalSpace E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : ContinuousAdd E
inst✝ : PseudoMetrizableSpace E
g f : α → E
hg : Measurable g
φ : ℕ → α →ₛ E
hφ : ∀ (x : α), Tendsto (fun n => (φ n) x) atTop (𝓝 (f x))
this : Tendsto (fun n x => g x + (φ n) x) atTop (𝓝 (g + f))
n : ℕ
⊢ Measurable fun x => g x + (φ n) x

Tactic:
exact hg.add_simpleFunc _

Result:
no goals

Proof state:
α : Type u_5
E : Type u_6
x✝ : MeasurableSpace α
inst✝⁵ : AddGroup E
inst✝⁴ : TopologicalSpace E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : ContinuousAdd E
inst✝ : PseudoMetrizableSpace E
g f : α → E
hg : Measurable g
hf : StronglyMeasurable f
⊢ Measurable (g + f)

Tactic:
rcases hf with ⟨φ, hφ⟩

Result:
case intro
α : Type u_5
E : Type u_6
x✝ : MeasurableSpace α
inst✝⁵ : AddGroup E
inst✝⁴ : TopologicalSpace E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : ContinuousAdd E
inst✝ : PseudoMetrizableSpace E
g f : α → E
hg : Measurable g
φ : ℕ → α →ₛ E
hφ : ∀ (x : α), Tendsto (fun n => (φ n) x) atTop (𝓝 (f x))
⊢ Measurable (g + f)

Proof state:
case intro
α : Type u_5
E : Type u_6
x✝ : MeasurableSpace α
inst✝⁵ : AddGroup E
inst✝⁴ : TopologicalSpace E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : ContinuousAdd E
inst✝ : PseudoMetrizableSpace E
g f : α → E
hg : Measurable g
φ : ℕ → α →ₛ E
hφ : ∀ (x : α), Tendsto (fun n => (φ n) x) atTop (𝓝 (f x))
this : Tendsto (fun n x => g x + (φ n) x) atTop (𝓝 (g + f))
⊢ Measurable (g + f)

Tactic:
apply measurable_of_tendsto_metrizable (fun n ↦ ?_) this

Result:
α : Type u_5
E : Type u_6
x✝ : MeasurableSpace α
inst✝⁵ : AddGroup E
inst✝⁴ : TopologicalSpace E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : ContinuousAdd E
inst✝ : PseudoMetrizableSpace E
g f : α → E
hg : Measurable g
φ : ℕ → α →ₛ E
hφ : ∀ (x : α), Tendsto (fun n => (φ n) x) atTop (𝓝 (f x))
this : Tendsto (fun n x => g x + (φ n) x) atTop (𝓝 (g + f))
n : ℕ
⊢ Measurable fun x => g x + (φ n) x