α : Type u_1
β : Type ?u.852920
γ : Type ?u.852923
δ : Type ?u.852926
ι : Type ?u.852929
R : Type ?u.852932
R' : Type ?u.852935
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
f g : Filter α
⊢ FiniteAtFilter μ (f ⊓ ae μ) → FiniteAtFilter μ f
α : Type u_1
β : Type ?u.852920
γ : Type ?u.852923
δ : Type ?u.852926
ι : Type ?u.852929
R : Type ?u.852932
R' : Type ?u.852935
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
f g : Filter α
⊢ FiniteAtFilter μ (f ⊓ ae μ) ↔ FiniteAtFilter μ f
refine' ⟨_, fun h => h.filter_mono inf_le_left⟩
case intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type ?u.852920
γ : Type ?u.852923
δ : Type ?u.852926
ι : Type ?u.852929
R : Type ?u.852932
R' : Type ?u.852935
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t✝ : Set α
f g : Filter α
t : Set α
ht : t ∈ f
u : Set α
hu : u ∈ ae μ
hμ : ↑↑μ (t ∩ u) < ⊤
⊢ FiniteAtFilter μ f
α : Type u_1
β : Type ?u.852920
γ : Type ?u.852923
δ : Type ?u.852926
ι : Type ?u.852929
R : Type ?u.852932
R' : Type ?u.852935
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
f g : Filter α
⊢ FiniteAtFilter μ (f ⊓ ae μ) → FiniteAtFilter μ f
rintro ⟨s, ⟨t, ht, u, hu, rfl⟩, hμ⟩
case intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type ?u.852920
γ : Type ?u.852923
δ : Type ?u.852926
ι : Type ?u.852929
R : Type ?u.852932
R' : Type ?u.852935
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t✝ : Set α
f g : Filter α
t : Set α
ht : t ∈ f
u : Set α
hu : u ∈ ae μ
hμ : ↑↑μ (t ∩ u) < ⊤
this : ↑↑μ t ≤ ↑↑μ (t ∩ u)
⊢ FiniteAtFilter μ f

case this
α : Type u_1
β : Type ?u.852920
γ : Type ?u.852923
δ : Type ?u.852926
ι : Type ?u.852929
R : Type ?u.852932
R' : Type ?u.852935
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t✝ : Set α
f g : Filter α
t : Set α
ht : t ∈ f
u : Set α
hu : u ∈ ae μ
hμ : ↑↑μ (t ∩ u) < ⊤
⊢ ↑↑μ t ≤ ↑↑μ (t ∩ u)
case intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type ?u.852920
γ : Type ?u.852923
δ : Type ?u.852926
ι : Type ?u.852929
R : Type ?u.852932
R' : Type ?u.852935
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t✝ : Set α
f g : Filter α
t : Set α
ht : t ∈ f
u : Set α
hu : u ∈ ae μ
hμ : ↑↑μ (t ∩ u) < ⊤
⊢ FiniteAtFilter μ f
suffices : μ t ≤ μ (t ∩ u)
case this
α : Type u_1
β : Type ?u.852920
γ : Type ?u.852923
δ : Type ?u.852926
ι : Type ?u.852929
R : Type ?u.852932
R' : Type ?u.852935
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t✝ : Set α
f g : Filter α
t : Set α
ht : t ∈ f
u : Set α
hu : u ∈ ae μ
hμ : ↑↑μ (t ∩ u) < ⊤
⊢ ↑↑μ t ≤ ↑↑μ (t ∩ u)
case intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type ?u.852920
γ : Type ?u.852923
δ : Type ?u.852926
ι : Type ?u.852929
R : Type ?u.852932
R' : Type ?u.852935
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t✝ : Set α
f g : Filter α
t : Set α
ht : t ∈ f
u : Set α
hu : u ∈ ae μ
hμ : ↑↑μ (t ∩ u) < ⊤
this : ↑↑μ t ≤ ↑↑μ (t ∩ u)
⊢ FiniteAtFilter μ f

case this
α : Type u_1
β : Type ?u.852920
γ : Type ?u.852923
δ : Type ?u.852926
ι : Type ?u.852929
R : Type ?u.852932
R' : Type ?u.852935
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t✝ : Set α
f g : Filter α
t : Set α
ht : t ∈ f
u : Set α
hu : u ∈ ae μ
hμ : ↑↑μ (t ∩ u) < ⊤
⊢ ↑↑μ t ≤ ↑↑μ (t ∩ u)
exact ⟨t, ht, this.trans_lt hμ⟩
no goals
case this
α : Type u_1
β : Type ?u.852920
γ : Type ?u.852923
δ : Type ?u.852926
ι : Type ?u.852929
R : Type ?u.852932
R' : Type ?u.852935
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t✝ : Set α
f g : Filter α
t : Set α
ht : t ∈ f
u : Set α
hu : u ∈ ae μ
hμ : ↑↑μ (t ∩ u) < ⊤
⊢ ↑↑μ t ≤ ↑↑μ (t ∩ u)
exact measure_mono_ae (mem_of_superset hu fun x hu ht => ⟨ht, hu⟩)