-- Mathlib/MeasureTheory/Covering/Differentiation.lean
theorem ae_tendsto_measure_inter_div (s : Set α) :
    ∀ᵐ x ∂μ.restrict s, Tendsto (fun a => μ (s ∩ a) / μ a) (v.filterAt x) (𝓝 1)

Proof state:
α : Type u_1
inst✝³ : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst✝² : SecondCountableTopology α
inst✝¹ : BorelSpace α
inst✝ : IsLocallyFiniteMeasure μ
s : Set α
⊢ ∀ᵐ (x : α) ∂μ.restrict s, Tendsto (fun a => μ (s ∩ a) / μ a) (v.filterAt x) (𝓝 1)

Tactic:
let t := toMeasurable μ s

Result:
α : Type u_1
inst✝³ : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst✝² : SecondCountableTopology α
inst✝¹ : BorelSpace α
inst✝ : IsLocallyFiniteMeasure μ
s : Set α
t : Set α := toMeasurable μ s
⊢ ∀ᵐ (x : α) ∂μ.restrict s, Tendsto (fun a => μ (s ∩ a) / μ a) (v.filterAt x) (𝓝 1)

Proof state:
α : Type u_1
inst✝³ : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst✝² : SecondCountableTopology α
inst✝¹ : BorelSpace α
inst✝ : IsLocallyFiniteMeasure μ
s : Set α
t : Set α := toMeasurable μ s
A : ∀ᵐ (x : α) ∂μ.restrict s, Tendsto (fun a => μ (t ∩ a) / μ a) (v.filterAt x) (𝓝 (t.indicator 1 x))
B : ∀ᵐ (x : α) ∂μ.restrict s, t.indicator 1 x = 1
x : α
hx : Tendsto (fun a => μ (t ∩ a) / μ a) (v.filterAt x) (𝓝 1)
h'x : t.indicator 1 x = 1
⊢ (fun a => μ (t ∩ a) / μ a) =ᶠ[v.filterAt x] fun a => μ (s ∩ a) / μ a

Tactic:
filter_upwards [v.eventually_filterAt_measurableSet x] with _ ha

Result:
case h
α : Type u_1
inst✝³ : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst✝² : SecondCountableTopology α
inst✝¹ : BorelSpace α
inst✝ : IsLocallyFiniteMeasure μ
s : Set α
t : Set α := toMeasurable μ s
A : ∀ᵐ (x : α) ∂μ.restrict s, Tendsto (fun a => μ (t ∩ a) / μ a) (v.filterAt x) (𝓝 (t.indicator 1 x))
B : ∀ᵐ (x : α) ∂μ.restrict s, t.indicator 1 x = 1
x : α
hx : Tendsto (fun a => μ (t ∩ a) / μ a) (v.filterAt x) (𝓝 1)
h'x : t.indicator 1 x = 1
a✝ : Set α
ha : MeasurableSet a✝
⊢ μ (t ∩ a✝) / μ a✝ = μ (s ∩ a✝) / μ a✝

Proof state:
case h
α : Type u_1
inst✝³ : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst✝² : SecondCountableTopology α
inst✝¹ : BorelSpace α
inst✝ : IsLocallyFiniteMeasure μ
s : Set α
t : Set α := toMeasurable μ s
A : ∀ᵐ (x : α) ∂μ.restrict s, Tendsto (fun a => μ (t ∩ a) / μ a) (v.filterAt x) (𝓝 (t.indicator 1 x))
B : ∀ᵐ (x : α) ∂μ.restrict s, t.indicator 1 x = 1
x : α
hx : Tendsto (fun a => μ (t ∩ a) / μ a) (v.filterAt x) (𝓝 1)
h'x : t.indicator 1 x = 1
⊢ Tendsto (fun a => μ (s ∩ a) / μ a) (v.filterAt x) (𝓝 1)

Tactic:
apply hx.congr' _

Result:
α : Type u_1
inst✝³ : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst✝² : SecondCountableTopology α
inst✝¹ : BorelSpace α
inst✝ : IsLocallyFiniteMeasure μ
s : Set α
t : Set α := toMeasurable μ s
A : ∀ᵐ (x : α) ∂μ.restrict s, Tendsto (fun a => μ (t ∩ a) / μ a) (v.filterAt x) (𝓝 (t.indicator 1 x))
B : ∀ᵐ (x : α) ∂μ.restrict s, t.indicator 1 x = 1
x : α
hx : Tendsto (fun a => μ (t ∩ a) / μ a) (v.filterAt x) (𝓝 1)
h'x : t.indicator 1 x = 1
⊢ (fun a => μ (t ∩ a) / μ a) =ᶠ[v.filterAt x] fun a => μ (s ∩ a) / μ a

Proof state:
case h
α : Type u_1
inst✝³ : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst✝² : SecondCountableTopology α
inst✝¹ : BorelSpace α
inst✝ : IsLocallyFiniteMeasure μ
s : Set α
t : Set α := toMeasurable μ s
A : ∀ᵐ (x : α) ∂μ.restrict s, Tendsto (fun a => μ (t ∩ a) / μ a) (v.filterAt x) (𝓝 (t.indicator 1 x))
a✝ : α
hx : a✝ ∈ toMeasurable μ s
⊢ t.indicator 1 a✝ = 1

Tactic:
simp only [t, hx, Pi.one_apply, indicator_of_mem]

Result:
no goals

Proof state:
α : Type u_1
inst✝³ : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst✝² : SecondCountableTopology α
inst✝¹ : BorelSpace α
inst✝ : IsLocallyFiniteMeasure μ
s : Set α
t : Set α := toMeasurable μ s
A : ∀ᵐ (x : α) ∂μ.restrict s, Tendsto (fun a => μ (t ∩ a) / μ a) (v.filterAt x) (𝓝 (t.indicator 1 x))
⊢ ∀ᵐ (x : α) ∂μ.restrict s, t.indicator 1 x = 1

Tactic:
refine ae_restrict_of_ae_restrict_of_subset (subset_toMeasurable μ s) ?_

Result:
α : Type u_1
inst✝³ : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst✝² : SecondCountableTopology α
inst✝¹ : BorelSpace α
inst✝ : IsLocallyFiniteMeasure μ
s : Set α
t : Set α := toMeasurable μ s
A : ∀ᵐ (x : α) ∂μ.restrict s, Tendsto (fun a => μ (t ∩ a) / μ a) (v.filterAt x) (𝓝 (t.indicator 1 x))
⊢ ∀ᵐ (x : α) ∂μ.restrict (toMeasurable μ s), t.indicator 1 x = 1

Proof state:
α : Type u_1
inst✝³ : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst✝² : SecondCountableTopology α
inst✝¹ : BorelSpace α
inst✝ : IsLocallyFiniteMeasure μ
s : Set α
t : Set α := toMeasurable μ s
A : ∀ᵐ (x : α) ∂μ.restrict s, Tendsto (fun a => μ (t ∩ a) / μ a) (v.filterAt x) (𝓝 (t.indicator 1 x))
⊢ ∀ᵐ (x : α) ∂μ.restrict (toMeasurable μ s), t.indicator 1 x = 1

Tactic:
filter_upwards [ae_restrict_mem (measurableSet_toMeasurable μ s)] with _ hx

Result:
case h
α : Type u_1
inst✝³ : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst✝² : SecondCountableTopology α
inst✝¹ : BorelSpace α
inst✝ : IsLocallyFiniteMeasure μ
s : Set α
t : Set α := toMeasurable μ s
A : ∀ᵐ (x : α) ∂μ.restrict s, Tendsto (fun a => μ (t ∩ a) / μ a) (v.filterAt x) (𝓝 (t.indicator 1 x))
a✝ : α
hx : a✝ ∈ toMeasurable μ s
⊢ t.indicator 1 a✝ = 1

Proof state:
α : Type u_1
inst✝³ : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst✝² : SecondCountableTopology α
inst✝¹ : BorelSpace α
inst✝ : IsLocallyFiniteMeasure μ
s : Set α
t : Set α := toMeasurable μ s
A : ∀ᵐ (x : α) ∂μ.restrict s, Tendsto (fun a => μ (t ∩ a) / μ a) (v.filterAt x) (𝓝 (t.indicator 1 x))
B : ∀ᵐ (x : α) ∂μ.restrict s, t.indicator 1 x = 1
⊢ ∀ᵐ (x : α) ∂μ.restrict s, Tendsto (fun a => μ (s ∩ a) / μ a) (v.filterAt x) (𝓝 1)

Tactic:
filter_upwards [A, B] with x hx h'x

Result:
case h
α : Type u_1
inst✝³ : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst✝² : SecondCountableTopology α
inst✝¹ : BorelSpace α
inst✝ : IsLocallyFiniteMeasure μ
s : Set α
t : Set α := toMeasurable μ s
A : ∀ᵐ (x : α) ∂μ.restrict s, Tendsto (fun a => μ (t ∩ a) / μ a) (v.filterAt x) (𝓝 (t.indicator 1 x))
B : ∀ᵐ (x : α) ∂μ.restrict s, t.indicator 1 x = 1
x : α
hx : Tendsto (fun a => μ (t ∩ a) / μ a) (v.filterAt x) (𝓝 (t.indicator 1 x))
h'x : t.indicator 1 x = 1
⊢ Tendsto (fun a => μ (s ∩ a) / μ a) (v.filterAt x) (𝓝 1)

Proof state:
case h.e_a
α : Type u_1
inst✝³ : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst✝² : SecondCountableTopology α
inst✝¹ : BorelSpace α
inst✝ : IsLocallyFiniteMeasure μ
s : Set α
t : Set α := toMeasurable μ s
A : ∀ᵐ (x : α) ∂μ.restrict s, Tendsto (fun a => μ (t ∩ a) / μ a) (v.filterAt x) (𝓝 (t.indicator 1 x))
B : ∀ᵐ (x : α) ∂μ.restrict s, t.indicator 1 x = 1
x : α
hx : Tendsto (fun a => μ (t ∩ a) / μ a) (v.filterAt x) (𝓝 1)
h'x : t.indicator 1 x = 1
a✝ : Set α
ha : MeasurableSet a✝
⊢ μ (t ∩ a✝) = μ (s ∩ a✝)

Tactic:
exact measure_toMeasurable_inter_of_sFinite ha _

Result:
no goals