α : Type u_2
β : Type u_1
γ : Type ?u.81206
ι : Type ?u.81209
inst✝ : ConditionallyCompleteLattice α
f : Filter β
u v : β → α
p : β → Prop
h : ∀ᶠ (a : β) in f, p a → u a = v a
⊢ sInf {a | ∀ᶠ (x : β) in f, p x → u x ≤ a} = blimsup v f p
α : Type u_2
β : Type u_1
γ : Type ?u.81206
ι : Type ?u.81209
inst✝ : ConditionallyCompleteLattice α
f : Filter β
u v : β → α
p : β → Prop
h : ∀ᶠ (a : β) in f, p a → u a = v a
⊢ blimsup u f p = blimsup v f p
rw [blimsup_eq]
case e_a.h
α : Type u_2
β : Type u_1
γ : Type ?u.81206
ι : Type ?u.81209
inst✝ : ConditionallyCompleteLattice α
f : Filter β
u v : β → α
p : β → Prop
h : ∀ᶠ (a : β) in f, p a → u a = v a
b : α
⊢ b ∈ {a | ∀ᶠ (x : β) in f, p x → u x ≤ a} ↔ b ∈ {a | ∀ᶠ (x : β) in f, p x → v x ≤ a}
α : Type u_2
β : Type u_1
γ : Type ?u.81206
ι : Type ?u.81209
inst✝ : ConditionallyCompleteLattice α
f : Filter β
u v : β → α
p : β → Prop
h : ∀ᶠ (a : β) in f, p a → u a = v a
⊢ sInf {a | ∀ᶠ (x : β) in f, p x → u x ≤ a} = blimsup v f p
congr with b
case e_a.h.refine'_1
α : Type u_2
β : Type u_1
γ : Type ?u.81206
ι : Type ?u.81209
inst✝ : ConditionallyCompleteLattice α
f : Filter β
u v : β → α
p : β → Prop
h : ∀ᶠ (a : β) in f, p a → u a = v a
b : α
x : β
hx : p x → u x = v x
h₁ : p x → u x ≤ b
h₂ : p x
⊢ v x ≤ b

case e_a.h.refine'_2
α : Type u_2
β : Type u_1
γ : Type ?u.81206
ι : Type ?u.81209
inst✝ : ConditionallyCompleteLattice α
f : Filter β
u v : β → α
p : β → Prop
h : ∀ᶠ (a : β) in f, p a → u a = v a
b : α
x : β
hx : p x → u x = v x
h₁ : p x → v x ≤ b
h₂ : p x
⊢ u x ≤ b
case e_a.h
α : Type u_2
β : Type u_1
γ : Type ?u.81206
ι : Type ?u.81209
inst✝ : ConditionallyCompleteLattice α
f : Filter β
u v : β → α
p : β → Prop
h : ∀ᶠ (a : β) in f, p a → u a = v a
b : α
⊢ b ∈ {a | ∀ᶠ (x : β) in f, p x → u x ≤ a} ↔ b ∈ {a | ∀ᶠ (x : β) in f, p x → v x ≤ a}
refine' eventually_congr (h.mono fun x hx => ⟨fun h₁ h₂ => _, fun h₁ h₂ => _⟩)
case e_a.h.refine'_1
α : Type u_2
β : Type u_1
γ : Type ?u.81206
ι : Type ?u.81209
inst✝ : ConditionallyCompleteLattice α
f : Filter β
u v : β → α
p : β → Prop
h : ∀ᶠ (a : β) in f, p a → u a = v a
b : α
x : β
hx : p x → u x = v x
h₁ : p x → u x ≤ b
h₂ : p x
⊢ u x ≤ b
case e_a.h.refine'_1
α : Type u_2
β : Type u_1
γ : Type ?u.81206
ι : Type ?u.81209
inst✝ : ConditionallyCompleteLattice α
f : Filter β
u v : β → α
p : β → Prop
h : ∀ᶠ (a : β) in f, p a → u a = v a
b : α
x : β
hx : p x → u x = v x
h₁ : p x → u x ≤ b
h₂ : p x
⊢ v x ≤ b
rw [← hx h₂]
no goals
case e_a.h.refine'_1
α : Type u_2
β : Type u_1
γ : Type ?u.81206
ι : Type ?u.81209
inst✝ : ConditionallyCompleteLattice α
f : Filter β
u v : β → α
p : β → Prop
h : ∀ᶠ (a : β) in f, p a → u a = v a
b : α
x : β
hx : p x → u x = v x
h₁ : p x → u x ≤ b
h₂ : p x
⊢ u x ≤ b
exact h₁ h₂
case e_a.h.refine'_2
α : Type u_2
β : Type u_1
γ : Type ?u.81206
ι : Type ?u.81209
inst✝ : ConditionallyCompleteLattice α
f : Filter β
u v : β → α
p : β → Prop
h : ∀ᶠ (a : β) in f, p a → u a = v a
b : α
x : β
hx : p x → u x = v x
h₁ : p x → v x ≤ b
h₂ : p x
⊢ v x ≤ b
case e_a.h.refine'_2
α : Type u_2
β : Type u_1
γ : Type ?u.81206
ι : Type ?u.81209
inst✝ : ConditionallyCompleteLattice α
f : Filter β
u v : β → α
p : β → Prop
h : ∀ᶠ (a : β) in f, p a → u a = v a
b : α
x : β
hx : p x → u x = v x
h₁ : p x → v x ≤ b
h₂ : p x
⊢ u x ≤ b
rw [hx h₂]
no goals
case e_a.h.refine'_2
α : Type u_2
β : Type u_1
γ : Type ?u.81206
ι : Type ?u.81209
inst✝ : ConditionallyCompleteLattice α
f : Filter β
u v : β → α
p : β → Prop
h : ∀ᶠ (a : β) in f, p a → u a = v a
b : α
x : β
hx : p x → u x = v x
h₁ : p x → v x ≤ b
h₂ : p x
⊢ v x ≤ b
exact h₁ h₂