-- Mathlib/MeasureTheory/Measure/Typeclasses.lean
theorem ae_of_forall_measure_lt_top_ae_restrict' {μ : Measure α} (ν : Measure α) [SigmaFinite μ]
    [SigmaFinite ν] (P : α → Prop)
    (h : ∀ s, MeasurableSet s → μ s < ∞ → ν s < ∞ → ∀ᵐ x ∂μ.restrict s, P x) : ∀ᵐ x ∂μ, P x

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
P : α → Prop
h : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ν s < ⊤ → ∀ᵐ (x : α) ∂μ.restrict s, P x
n : ℕ
this : ∀ᵐ (x : α) ∂μ.restrict (spanningSets (μ + ν) n), P x
⊢ ∀ᵐ (x : α) ∂μ, x ∈ spanningSets (μ + ν) n → P x

Tactic:
exact (ae_restrict_iff' (measurableSet_spanningSets _ _)).mp this

Result:
no goals

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
P : α → Prop
h : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ν s < ⊤ → ∀ᵐ (x : α) ∂μ.restrict s, P x
⊢ ∀ (n : ℕ), ∀ᵐ (x : α) ∂μ, x ∈ spanningSets (μ + ν) n → P x

Tactic:
intro n

Result:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
P : α → Prop
h : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ν s < ⊤ → ∀ᵐ (x : α) ∂μ.restrict s, P x
n : ℕ
⊢ ∀ᵐ (x : α) ∂μ, x ∈ spanningSets (μ + ν) n → P x

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
P : α → Prop
h : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ν s < ⊤ → ∀ᵐ (x : α) ∂μ.restrict s, P x
⊢ ∀ᵐ (x : α) ∂μ, P x

Tactic:
have : ∀ n, ∀ᵐ x ∂μ, x ∈ spanningSets (μ + ν) n → P x := by
  intro n
  have := h
    (spanningSets (μ + ν) n) (measurableSet_spanningSets _ _)
    ((self_le_add_right _ _).trans_lt (measure_spanningSets_lt_top (μ + ν) _))
    ((self_le_add_left _ _).trans_lt (measure_spanningSets_lt_top (μ + ν) _))
  exact (ae_restrict_iff' (measurableSet_spanningSets _ _)).mp this

Result:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
P : α → Prop
h : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ν s < ⊤ → ∀ᵐ (x : α) ∂μ.restrict s, P x
this : ∀ (n : ℕ), ∀ᵐ (x : α) ∂μ, x ∈ spanningSets (μ + ν) n → P x
⊢ ∀ᵐ (x : α) ∂μ, P x

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
P : α → Prop
h : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ν s < ⊤ → ∀ᵐ (x : α) ∂μ.restrict s, P x
this : ∀ (n : ℕ), ∀ᵐ (x : α) ∂μ, x ∈ spanningSets (μ + ν) n → P x
⊢ ∀ᵐ (x : α) ∂μ, P x

Tactic:
filter_upwards [ae_all_iff.2 this] with _ hx using hx _ (mem_spanningSetsIndex _ _)

Result:
no goals

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
P : α → Prop
h : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ν s < ⊤ → ∀ᵐ (x : α) ∂μ.restrict s, P x
n : ℕ
⊢ ∀ᵐ (x : α) ∂μ, x ∈ spanningSets (μ + ν) n → P x

Tactic:
have := h
  (spanningSets (μ + ν) n) (measurableSet_spanningSets _ _)
  ((self_le_add_right _ _).trans_lt (measure_spanningSets_lt_top (μ + ν) _))
  ((self_le_add_left _ _).trans_lt (measure_spanningSets_lt_top (μ + ν) _))

Result:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
P : α → Prop
h : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ν s < ⊤ → ∀ᵐ (x : α) ∂μ.restrict s, P x
n : ℕ
this : ∀ᵐ (x : α) ∂μ.restrict (spanningSets (μ + ν) n), P x
⊢ ∀ᵐ (x : α) ∂μ, x ∈ spanningSets (μ + ν) n → P x