-- Mathlib/MeasureTheory/Covering/Differentiation.lean
theorem ae_tendsto_lintegral_enorm_sub_div'_of_integrable {f : α → E} (hf : Integrable f μ)
    (h'f : StronglyMeasurable f) :
    ∀ᵐ x ∂μ, Tendsto (fun a => (∫⁻ y in a, ‖f y - f x‖ₑ ∂μ) / μ a) (v.filterAt x) (𝓝 0)

Proof state:
case intro
α : Type u_1
inst✝⁴ : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : SecondCountableTopology α
inst✝¹ : BorelSpace α
inst✝ : IsLocallyFiniteMeasure μ
f : α → E
hf : Integrable f μ
h'f : StronglyMeasurable f
A : μ.FiniteSpanningSetsIn {K | IsOpen K} := μ.finiteSpanningSetsInOpen'
t : Set E
t_count : t.Countable
ht : range f ⊆ closure t
main :
  ∀ᵐ (x : α) ∂μ,
    ∀ (n : ℕ),
      ∀ c ∈ t,
        Tendsto (fun a => (∫⁻ (y : α) in a, ‖f y - (A.set n).indicator (fun x => c) y‖ₑ ∂μ) / μ a) (v.filterAt x)
          (𝓝 ‖f x - (A.set n).indicator (fun x => c) x‖ₑ)
x : α
hx :
  ∀ (n : ℕ),
    ∀ c ∈ t,
      Tendsto (fun a => (∫⁻ (y : α) in a, ‖f y - (A.set n).indicator (fun x => c) y‖ₑ ∂μ) / μ a) (v.filterAt x)
        (𝓝 ‖f x - (A.set n).indicator (fun x => c) x‖ₑ)
h'x : ∀ᶠ (a : Set α) in v.filterAt x, 0 < μ a
c : E
hc : c ∈ t
n : ℕ
xn : x ∈ A.set n
⊢ Tendsto (fun a => (∫⁻ (y : α) in a, ‖f y - c‖ₑ ∂μ) / μ a) (v.filterAt x) (𝓝 ‖f x - c‖ₑ)

Tactic:
specialize hx n c hc

Result:
case intro
α : Type u_1
inst✝⁴ : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : SecondCountableTopology α
inst✝¹ : BorelSpace α
inst✝ : IsLocallyFiniteMeasure μ
f : α → E
hf : Integrable f μ
h'f : StronglyMeasurable f
A : μ.FiniteSpanningSetsIn {K | IsOpen K} := μ.finiteSpanningSetsInOpen'
t : Set E
t_count : t.Countable
ht : range f ⊆ closure t
main :
  ∀ᵐ (x : α) ∂μ,
    ∀ (n : ℕ),
      ∀ c ∈ t,
        Tendsto (fun a => (∫⁻ (y : α) in a, ‖f y - (A.set n).indicator (fun x => c) y‖ₑ ∂μ) / μ a) (v.filterAt x)
          (𝓝 ‖f x - (A.set n).indicator (fun x => c) x‖ₑ)
x : α
h'x : ∀ᶠ (a : Set α) in v.filterAt x, 0 < μ a
c : E
hc : c ∈ t
n : ℕ
xn : x ∈ A.set n
hx :
  Tendsto (fun a => (∫⁻ (y : α) in a, ‖f y - (A.set n).indicator (fun x => c) y‖ₑ ∂μ) / μ a) (v.filterAt x)
    (𝓝 ‖f x - (A.set n).indicator (fun x => c) x‖ₑ)
⊢ Tendsto (fun a => (∫⁻ (y : α) in a, ‖f y - c‖ₑ ∂μ) / μ a) (v.filterAt x) (𝓝 ‖f x - c‖ₑ)

Proof state:
α : Type u_1
inst✝⁴ : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : SecondCountableTopology α
inst✝¹ : BorelSpace α
inst✝ : IsLocallyFiniteMeasure μ
f : α → E
hf : Integrable f μ
h'f : StronglyMeasurable f
A : μ.FiniteSpanningSetsIn {K | IsOpen K} := μ.finiteSpanningSetsInOpen'
t : Set E
t_count : t.Countable
ht : range f ⊆ closure t
main :
  ∀ᵐ (x : α) ∂μ,
    ∀ (n : ℕ),
      ∀ c ∈ t,
        Tendsto (fun a => (∫⁻ (y : α) in a, ‖f y - (A.set n).indicator (fun x => c) y‖ₑ ∂μ) / μ a) (v.filterAt x)
          (𝓝 ‖f x - (A.set n).indicator (fun x => c) x‖ₑ)
x : α
hx :
  ∀ (n : ℕ),
    ∀ c ∈ t,
      Tendsto (fun a => (∫⁻ (y : α) in a, ‖f y - (A.set n).indicator (fun x => c) y‖ₑ ∂μ) / μ a) (v.filterAt x)
        (𝓝 ‖f x - (A.set n).indicator (fun x => c) x‖ₑ)
h'x : ∀ᶠ (a : Set α) in v.filterAt x, 0 < μ a
c : E
hc : c ∈ t
⊢ ∃ n, x ∈ A.set n

Tactic:
simpa [← A.spanning] using mem_univ x

Result:
no goals

Proof state:
α : Type u_1
inst✝⁴ : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : SecondCountableTopology α
inst✝¹ : BorelSpace α
inst✝ : IsLocallyFiniteMeasure μ
f : α → E
hf : Integrable f μ
h'f : StronglyMeasurable f
A : μ.FiniteSpanningSetsIn {K | IsOpen K} := μ.finiteSpanningSetsInOpen'
t : Set E
t_count : t.Countable
ht : range f ⊆ closure t
main :
  ∀ᵐ (x : α) ∂μ,
    ∀ (n : ℕ),
      ∀ c ∈ t,
        Tendsto (fun a => (∫⁻ (y : α) in a, ‖f y - (A.set n).indicator (fun x => c) y‖ₑ ∂μ) / μ a) (v.filterAt x)
          (𝓝 ‖f x - (A.set n).indicator (fun x => c) x‖ₑ)
x : α
hx :
  ∀ (n : ℕ),
    ∀ c ∈ t,
      Tendsto (fun a => (∫⁻ (y : α) in a, ‖f y - (A.set n).indicator (fun x => c) y‖ₑ ∂μ) / μ a) (v.filterAt x)
        (𝓝 ‖f x - (A.set n).indicator (fun x => c) x‖ₑ)
h'x : ∀ᶠ (a : Set α) in v.filterAt x, 0 < μ a
M : ∀ c ∈ t, Tendsto (fun a => (∫⁻ (y : α) in a, ‖f y - c‖ₑ ∂μ) / μ a) (v.filterAt x) (𝓝 ‖f x - c‖ₑ)
ε : ℝ≥0∞
εpos : ε > 0
c : E
ct : c ∈ t
xc : ‖f x - c‖ₑ < ε / 2
a : Set α
ha : (∫⁻ (y : α) in a, ‖f y - c‖ₑ ∂μ) / μ a < ε / 2
h'a : 0 < μ a
h''a : μ a < ⊤
⊢ ∫⁻ (y : α) in a, ‖f y - c‖ₑ ∂μ + ∫⁻ (x_1 : α) in a, ‖f x - c‖ₑ ∂μ ≤ ε / 2 * μ a + ε / 2 * μ a

Tactic:
gcongr

Result:
case h₁
α : Type u_1
inst✝⁴ : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : SecondCountableTopology α
inst✝¹ : BorelSpace α
inst✝ : IsLocallyFiniteMeasure μ
f : α → E
hf : Integrable f μ
h'f : StronglyMeasurable f
A : μ.FiniteSpanningSetsIn {K | IsOpen K} := μ.finiteSpanningSetsInOpen'
t : Set E
t_count : t.Countable
ht : range f ⊆ closure t
main :
  ∀ᵐ (x : α) ∂μ,
    ∀ (n : ℕ),
      ∀ c ∈ t,
        Tendsto (fun a => (∫⁻ (y : α) in a, ‖f y - (A.set n).indicator (fun x => c) y‖ₑ ∂μ) / μ a) (v.filterAt x)
          (𝓝 ‖f x - (A.set n).indicator (fun x => c) x‖ₑ)
x : α
hx :
  ∀ (n : ℕ),
    ∀ c ∈ t,
      Tendsto (fun a => (∫⁻ (y : α) in a, ‖f y - (A.set n).indicator (fun x => c) y‖ₑ ∂μ) / μ a) (v.filterAt x)
        (𝓝 ‖f x - (A.set n).indicator (fun x => c) x‖ₑ)
h'x : ∀ᶠ (a : Set α) in v.filterAt x, 0 < μ a
M : ∀ c ∈ t, Tendsto (fun a => (∫⁻ (y : α) in a, ‖f y - c‖ₑ ∂μ) / μ a) (v.filterAt x) (𝓝 ‖f x - c‖ₑ)
ε : ℝ≥0∞
εpos : ε > 0
c : E
ct : c ∈ t
xc : ‖f x - c‖ₑ < ε / 2
a : Set α
ha : (∫⁻ (y : α) in a, ‖f y - c‖ₑ ∂μ) / μ a < ε / 2
h'a : 0 < μ a
h''a : μ a < ⊤
⊢ ∫⁻ (y : α) in a, ‖f y - c‖ₑ ∂μ ≤ ε / 2 * μ a

case h₂
α : Type u_1
inst✝⁴ : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : SecondCountableTopology α
inst✝¹ : BorelSpace α
inst✝ : IsLocallyFiniteMeasure μ
f : α → E
hf : Integrable f μ
h'f : StronglyMeasurable f
A : μ.FiniteSpanningSetsIn {K | IsOpen K} := μ.finiteSpanningSetsInOpen'
t : Set E
t_count : t.Countable
ht : range f ⊆ closure t
main :
  ∀ᵐ (x : α) ∂μ,
    ∀ (n : ℕ),
      ∀ c ∈ t,
        Tendsto (fun a => (∫⁻ (y : α) in a, ‖f y - (A.set n).indicator (fun x => c) y‖ₑ ∂μ) / μ a) (v.filterAt x)
          (𝓝 ‖f x - (A.set n).indicator (fun x => c) x‖ₑ)
x : α
hx :
  ∀ (n : ℕ),
    ∀ c ∈ t,
      Tendsto (fun a => (∫⁻ (y : α) in a, ‖f y - (A.set n).indicator (fun x => c) y‖ₑ ∂μ) / μ a) (v.filterAt x)
        (𝓝 ‖f x - (A.set n).indicator (fun x => c) x‖ₑ)
h'x : ∀ᶠ (a : Set α) in v.filterAt x, 0 < μ a
M : ∀ c ∈ t, Tendsto (fun a => (∫⁻ (y : α) in a, ‖f y - c‖ₑ ∂μ) / μ a) (v.filterAt x) (𝓝 ‖f x - c‖ₑ)
ε : ℝ≥0∞
εpos : ε > 0
c : E
ct : c ∈ t
xc : ‖f x - c‖ₑ < ε / 2
a : Set α
ha : (∫⁻ (y : α) in a, ‖f y - c‖ₑ ∂μ) / μ a < ε / 2
h'a : 0 < μ a
h''a : μ a < ⊤
⊢ ∫⁻ (x_1 : α) in a, ‖f x - c‖ₑ ∂μ ≤ ε / 2 * μ a