α : Type u_2
β : Type u_1
γ : Type ?u.61523
ι : Type ?u.61526
inst✝ : ConditionallyCompleteLattice α
f : Filter β
u : β → α
p : β → Prop
⊢ sInf {a | ∀ᶠ (x : β) in f, p x → u x ≤ a} = sInf {a | ∀ᶠ (b : β) in f, ∀ (a_1 : { x // p x }), ↑a_1 = b → u ↑a_1 ≤ a}
α : Type u_2
β : Type u_1
γ : Type ?u.61523
ι : Type ?u.61526
inst✝ : ConditionallyCompleteLattice α
f : Filter β
u : β → α
p : β → Prop
⊢ blimsup u f p = limsup (u ∘ Subtype.val) (comap Subtype.val f)
simp only [blimsup_eq, limsup_eq, Function.comp_apply, eventually_comap, SetCoe.forall,
  Subtype.coe_mk, mem_setOf_eq]
case e_a
α : Type u_2
β : Type u_1
γ : Type ?u.61523
ι : Type ?u.61526
inst✝ : ConditionallyCompleteLattice α
f : Filter β
u : β → α
p : β → Prop
⊢ {a | ∀ᶠ (x : β) in f, p x → u x ≤ a} = {a | ∀ᶠ (b : β) in f, ∀ (a_1 : { x // p x }), ↑a_1 = b → u ↑a_1 ≤ a}
α : Type u_2
β : Type u_1
γ : Type ?u.61523
ι : Type ?u.61526
inst✝ : ConditionallyCompleteLattice α
f : Filter β
u : β → α
p : β → Prop
⊢ sInf {a | ∀ᶠ (x : β) in f, p x → u x ≤ a} = sInf {a | ∀ᶠ (b : β) in f, ∀ (a_1 : { x // p x }), ↑a_1 = b → u ↑a_1 ≤ a}
congr
case e_a.h
α : Type u_2
β : Type u_1
γ : Type ?u.61523
ι : Type ?u.61526
inst✝ : ConditionallyCompleteLattice α
f : Filter β
u : β → α
p : β → Prop
a : α
⊢ a ∈ {a | ∀ᶠ (x : β) in f, p x → u x ≤ a} ↔ a ∈ {a | ∀ᶠ (b : β) in f, ∀ (a_1 : { x // p x }), ↑a_1 = b → u ↑a_1 ≤ a}
case e_a
α : Type u_2
β : Type u_1
γ : Type ?u.61523
ι : Type ?u.61526
inst✝ : ConditionallyCompleteLattice α
f : Filter β
u : β → α
p : β → Prop
⊢ {a | ∀ᶠ (x : β) in f, p x → u x ≤ a} = {a | ∀ᶠ (b : β) in f, ∀ (a_1 : { x // p x }), ↑a_1 = b → u ↑a_1 ≤ a}
ext a
case e_a.h
α : Type u_2
β : Type u_1
γ : Type ?u.61523
ι : Type ?u.61526
inst✝ : ConditionallyCompleteLattice α
f : Filter β
u : β → α
p : β → Prop
a : α
⊢ a ∈ {a | ∀ᶠ (x : β) in f, p x → u x ≤ a} ↔ a ∈ {a | ∀ᶠ (b : β) in f, ∀ (a_1 : β), p a_1 → a_1 = b → u a_1 ≤ a}
case e_a.h
α : Type u_2
β : Type u_1
γ : Type ?u.61523
ι : Type ?u.61526
inst✝ : ConditionallyCompleteLattice α
f : Filter β
u : β → α
p : β → Prop
a : α
⊢ a ∈ {a | ∀ᶠ (x : β) in f, p x → u x ≤ a} ↔ a ∈ {a | ∀ᶠ (b : β) in f, ∀ (a_1 : { x // p x }), ↑a_1 = b → u ↑a_1 ≤ a}
simp_rw [Subtype.forall]
no goals
case e_a.h
α : Type u_2
β : Type u_1
γ : Type ?u.61523
ι : Type ?u.61526
inst✝ : ConditionallyCompleteLattice α
f : Filter β
u : β → α
p : β → Prop
a : α
⊢ a ∈ {a | ∀ᶠ (x : β) in f, p x → u x ≤ a} ↔ a ∈ {a | ∀ᶠ (b : β) in f, ∀ (a_1 : β), p a_1 → a_1 = b → u a_1 ≤ a}
exact eventually_congr (
     eventually_of_forall
      fun x => ⟨fun hx y hy hxy => hxy.symm ▸ hx (hxy ▸ hy), fun hx hx' => hx x hx' rfl⟩)