-- Mathlib/MeasureTheory/Covering/Differentiation.lean
theorem ae_tendsto_div : ∀ᵐ x ∂μ, ∃ c, Tendsto (fun a => ρ a / μ a) (v.filterAt x) (𝓝 c)

Proof state:
case intro.intro.hc
α : Type u_1
inst✝⁴ : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
w : Set ℝ≥0∞
w_count : w.Countable
w_dense : Dense w
left✝ : 0 ∉ w
w_top : ⊤ ∉ w
I : ∀ x ∈ w, x ≠ ⊤
c : ℝ≥0
hc : ↑c ∈ w
d : ℝ≥0
hd : ↑d ∈ w
hcd : ↑c < ↑d
x : α
h1x : ∃ᶠ (a : Set α) in v.filterAt x, ρ a / μ a < ↑c
a✝ : ∃ᶠ (x : Set α) in v.filterAt x, ↑d < ρ x / μ x
⊢ ∃ᶠ (a : Set α) in v.filterAt x, ρ a ≤ ↑c * μ a

Tactic:
apply h1x.mono fun a ha => ?_

Result:
α : Type u_1
inst✝⁴ : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
w : Set ℝ≥0∞
w_count : w.Countable
w_dense : Dense w
left✝ : 0 ∉ w
w_top : ⊤ ∉ w
I : ∀ x ∈ w, x ≠ ⊤
c : ℝ≥0
hc : ↑c ∈ w
d : ℝ≥0
hd : ↑d ∈ w
hcd : ↑c < ↑d
x : α
h1x : ∃ᶠ (a : Set α) in v.filterAt x, ρ a / μ a < ↑c
a✝ : ∃ᶠ (x : Set α) in v.filterAt x, ↑d < ρ x / μ x
a : Set α
ha : ρ a / μ a < ↑c
⊢ ρ a ≤ ↑c * μ a

Proof state:
α : Type u_1
inst✝⁴ : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
⊢ ∀ᵐ (x : α) ∂μ, ∃ c, Tendsto (fun a => ρ a / μ a) (v.filterAt x) (𝓝 c)

Tactic:
obtain ⟨w, w_count, w_dense, _, w_top⟩ :
  ∃ w : Set ℝ≥0∞, w.Countable ∧ Dense w ∧ 0 ∉ w ∧ ∞ ∉ w :=
  ENNReal.exists_countable_dense_no_zero_top

Result:
case intro.intro.intro.intro
α : Type u_1
inst✝⁴ : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
w : Set ℝ≥0∞
w_count : w.Countable
w_dense : Dense w
left✝ : 0 ∉ w
w_top : ⊤ ∉ w
⊢ ∀ᵐ (x : α) ∂μ, ∃ c, Tendsto (fun a => ρ a / μ a) (v.filterAt x) (𝓝 c)

Proof state:
α : Type u_1
inst✝⁴ : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
w : Set ℝ≥0∞
w_count : w.Countable
w_dense : Dense w
left✝ : 0 ∉ w
w_top : ⊤ ∉ w
I : ∀ x ∈ w, x ≠ ⊤
A :
  ∀ c ∈ w,
    ∀ d ∈ w,
      c < d →
        ∀ᵐ (x : α) ∂μ,
          ¬((∃ᶠ (a : Set α) in v.filterAt x, ρ a / μ a < c) ∧ ∃ᶠ (a : Set α) in v.filterAt x, d < ρ a / μ a)
x : ℝ≥0∞
hx : x ∈ w
⊢ ∀ i ∈ w,
    ∀ᵐ (x_1 : α) ∂μ,
      x < i → ¬((∃ᶠ (a : Set α) in v.filterAt x_1, ρ a / μ a < x) ∧ ∃ᶠ (a : Set α) in v.filterAt x_1, i < ρ a / μ a)

Tactic:
revert x

Result:
α : Type u_1
inst✝⁴ : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
w : Set ℝ≥0∞
w_count : w.Countable
w_dense : Dense w
left✝ : 0 ∉ w
w_top : ⊤ ∉ w
I : ∀ x ∈ w, x ≠ ⊤
A :
  ∀ c ∈ w,
    ∀ d ∈ w,
      c < d →
        ∀ᵐ (x : α) ∂μ,
          ¬((∃ᶠ (a : Set α) in v.filterAt x, ρ a / μ a < c) ∧ ∃ᶠ (a : Set α) in v.filterAt x, d < ρ a / μ a)
⊢ ∀ x ∈ w,
    ∀ i ∈ w,
      ∀ᵐ (x_1 : α) ∂μ,
        x < i → ¬((∃ᶠ (a : Set α) in v.filterAt x_1, ρ a / μ a < x) ∧ ∃ᶠ (a : Set α) in v.filterAt x_1, i < ρ a / μ a)

Proof state:
case intro.intro.intro.intro
α : Type u_1
inst✝⁴ : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
w : Set ℝ≥0∞
w_count : w.Countable
w_dense : Dense w
left✝ : 0 ∉ w
w_top : ⊤ ∉ w
I : ∀ x ∈ w, x ≠ ⊤
A :
  ∀ c ∈ w,
    ∀ d ∈ w,
      c < d →
        ∀ᵐ (x : α) ∂μ,
          ¬((∃ᶠ (a : Set α) in v.filterAt x, ρ a / μ a < c) ∧ ∃ᶠ (a : Set α) in v.filterAt x, d < ρ a / μ a)
B :
  ∀ᵐ (x : α) ∂μ,
    ∀ c ∈ w,
      ∀ d ∈ w,
        c < d → ¬((∃ᶠ (a : Set α) in v.filterAt x, ρ a / μ a < c) ∧ ∃ᶠ (a : Set α) in v.filterAt x, d < ρ a / μ a)
⊢ ∀ᵐ (x : α) ∂μ, ∃ c, Tendsto (fun a => ρ a / μ a) (v.filterAt x) (𝓝 c)

Tactic:
filter_upwards [B]

Result:
case h
α : Type u_1
inst✝⁴ : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
w : Set ℝ≥0∞
w_count : w.Countable
w_dense : Dense w
left✝ : 0 ∉ w
w_top : ⊤ ∉ w
I : ∀ x ∈ w, x ≠ ⊤
A :
  ∀ c ∈ w,
    ∀ d ∈ w,
      c < d →
        ∀ᵐ (x : α) ∂μ,
          ¬((∃ᶠ (a : Set α) in v.filterAt x, ρ a / μ a < c) ∧ ∃ᶠ (a : Set α) in v.filterAt x, d < ρ a / μ a)
B :
  ∀ᵐ (x : α) ∂μ,
    ∀ c ∈ w,
      ∀ d ∈ w,
        c < d → ¬((∃ᶠ (a : Set α) in v.filterAt x, ρ a / μ a < c) ∧ ∃ᶠ (a : Set α) in v.filterAt x, d < ρ a / μ a)
⊢ ∀ (a : α),
    (∀ c ∈ w,
        ∀ d ∈ w,
          c < d → ¬((∃ᶠ (a : Set α) in v.filterAt a, ρ a / μ a < c) ∧ ∃ᶠ (a : Set α) in v.filterAt a, d < ρ a / μ a)) →
      ∃ c, Tendsto (fun a => ρ a / μ a) (v.filterAt a) (𝓝 c)

Proof state:
α : Type u_1
inst✝⁴ : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
w : Set ℝ≥0∞
w_count : w.Countable
w_dense : Dense w
left✝ : 0 ∉ w
w_top : ⊤ ∉ w
I : ∀ x ∈ w, x ≠ ⊤
c : ℝ≥0
hc : ↑c ∈ w
d : ℝ≥0
hd : ↑d ∈ w
hcd : ↑c < ↑d
x : α
h1x : ∃ᶠ (a : Set α) in v.filterAt x, ρ a / μ a < ↑c
a✝ : ∃ᶠ (x : Set α) in v.filterAt x, ↑d < ρ x / μ x
a : Set α
ha : ρ a / μ a < ↑c
⊢ ρ a ≤ ↑c * μ a

Tactic:
refine (ENNReal.div_le_iff_le_mul ?_ (Or.inr (bot_le.trans_lt ha).ne')).1 ha.le

Result:
α : Type u_1
inst✝⁴ : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
w : Set ℝ≥0∞
w_count : w.Countable
w_dense : Dense w
left✝ : 0 ∉ w
w_top : ⊤ ∉ w
I : ∀ x ∈ w, x ≠ ⊤
c : ℝ≥0
hc : ↑c ∈ w
d : ℝ≥0
hd : ↑d ∈ w
hcd : ↑c < ↑d
x : α
h1x : ∃ᶠ (a : Set α) in v.filterAt x, ρ a / μ a < ↑c
a✝ : ∃ᶠ (x : Set α) in v.filterAt x, ↑d < ρ x / μ x
a : Set α
ha : ρ a / μ a < ↑c
⊢ μ a ≠ 0 ∨ ↑c ≠ ⊤

Proof state:
α : Type u_1
inst✝⁴ : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
w : Set ℝ≥0∞
w_count : w.Countable
w_dense : Dense w
left✝ : 0 ∉ w
w_top : ⊤ ∉ w
I : ∀ x ∈ w, x ≠ ⊤
c : ℝ≥0
hc : ↑c ∈ w
d : ℝ≥0
hd : ↑d ∈ w
hcd : ↑c < ↑d
x : α
a✝ : ∃ᶠ (a : Set α) in v.filterAt x, ρ a / μ a < ↑c
h2x : ∃ᶠ (x : Set α) in v.filterAt x, ↑d < ρ x / μ x
a : Set α
ha : ↑d < ρ a / μ a
⊢ ↑d * μ a ≤ ρ a

Tactic:
exact ENNReal.mul_le_of_le_div ha.le

Result:
no goals