-- Mathlib/MeasureTheory/Function/StronglyMeasurable/Basic.lean
theorem _root_.Measurable.stronglyMeasurable_add
    {α 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 (f + g)

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 => (φ n) x + g x) atTop (𝓝 (f + g))
n : ℕ
⊢ Measurable fun x => (φ n) x + g x

Tactic:
exact hg.simpleFunc_add _

Result:
no goals

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 (f + g)

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

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 => (φ n) x + g x) atTop (𝓝 (f + g))
⊢ Measurable (f + g)

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 => (φ n) x + g x) atTop (𝓝 (f + g))
⊢ Measurable (f + g)

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 => (φ n) x + g x) atTop (𝓝 (f + g))
n : ℕ
⊢ Measurable fun x => (φ n) x + g x

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 (f + g)

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 (f + g)