α : Type u_2
β : Type u_1
γ : Type ?u.110090
ι : Type ?u.110093
inst✝ : CompleteLattice α
f : Filter β
p q : β → Prop
u : β → α
h : ∀ᶠ (x : β) in f, u x ≠ ⊥ → (p x ↔ q x)
⊢ sInf {a | ∀ᶠ (x : β) in f, p x → u x ≤ a} = sInf {a | ∀ᶠ (x : β) in f, q x → u x ≤ a}
α : Type u_2
β : Type u_1
γ : Type ?u.110090
ι : Type ?u.110093
inst✝ : CompleteLattice α
f : Filter β
p q : β → Prop
u : β → α
h : ∀ᶠ (x : β) in f, u x ≠ ⊥ → (p x ↔ q x)
⊢ blimsup u f p = blimsup u f q
simp only [blimsup_eq]
case e_a
α : Type u_2
β : Type u_1
γ : Type ?u.110090
ι : Type ?u.110093
inst✝ : CompleteLattice α
f : Filter β
p q : β → Prop
u : β → α
h : ∀ᶠ (x : β) in f, u x ≠ ⊥ → (p x ↔ q x)
⊢ {a | ∀ᶠ (x : β) in f, p x → u x ≤ a} = {a | ∀ᶠ (x : β) in f, q x → u x ≤ a}
α : Type u_2
β : Type u_1
γ : Type ?u.110090
ι : Type ?u.110093
inst✝ : CompleteLattice α
f : Filter β
p q : β → Prop
u : β → α
h : ∀ᶠ (x : β) in f, u x ≠ ⊥ → (p x ↔ q x)
⊢ sInf {a | ∀ᶠ (x : β) in f, p x → u x ≤ a} = sInf {a | ∀ᶠ (x : β) in f, q x → u x ≤ a}
congr
case e_a.h
α : Type u_2
β : Type u_1
γ : Type ?u.110090
ι : Type ?u.110093
inst✝ : CompleteLattice α
f : Filter β
p q : β → Prop
u : β → α
h : ∀ᶠ (x : β) in f, u x ≠ ⊥ → (p x ↔ q x)
a : α
⊢ a ∈ {a | ∀ᶠ (x : β) in f, p x → u x ≤ a} ↔ a ∈ {a | ∀ᶠ (x : β) in f, q x → u x ≤ a}
case e_a
α : Type u_2
β : Type u_1
γ : Type ?u.110090
ι : Type ?u.110093
inst✝ : CompleteLattice α
f : Filter β
p q : β → Prop
u : β → α
h : ∀ᶠ (x : β) in f, u x ≠ ⊥ → (p x ↔ q x)
⊢ {a | ∀ᶠ (x : β) in f, p x → u x ≤ a} = {a | ∀ᶠ (x : β) in f, q x → u x ≤ a}
ext a
case e_a.h
α : Type u_2
β : Type u_1
γ : Type ?u.110090
ι : Type ?u.110093
inst✝ : CompleteLattice α
f : Filter β
p q : β → Prop
u : β → α
h : ∀ᶠ (x : β) in f, u x ≠ ⊥ → (p x ↔ q x)
a : α
b : β
hb : u b ≠ ⊥ → (p b ↔ q b)
⊢ p b → u b ≤ a ↔ q b → u b ≤ a
case e_a.h
α : Type u_2
β : Type u_1
γ : Type ?u.110090
ι : Type ?u.110093
inst✝ : CompleteLattice α
f : Filter β
p q : β → Prop
u : β → α
h : ∀ᶠ (x : β) in f, u x ≠ ⊥ → (p x ↔ q x)
a : α
⊢ a ∈ {a | ∀ᶠ (x : β) in f, p x → u x ≤ a} ↔ a ∈ {a | ∀ᶠ (x : β) in f, q x → u x ≤ a}
refine' eventually_congr (h.mono fun b hb => _)
case e_a.h.inl
α : Type u_2
β : Type u_1
γ : Type ?u.110090
ι : Type ?u.110093
inst✝ : CompleteLattice α
f : Filter β
p q : β → Prop
u : β → α
h : ∀ᶠ (x : β) in f, u x ≠ ⊥ → (p x ↔ q x)
a : α
b : β
hb : u b ≠ ⊥ → (p b ↔ q b)
hu : u b = ⊥
⊢ p b → u b ≤ a ↔ q b → u b ≤ a

case e_a.h.inr
α : Type u_2
β : Type u_1
γ : Type ?u.110090
ι : Type ?u.110093
inst✝ : CompleteLattice α
f : Filter β
p q : β → Prop
u : β → α
h : ∀ᶠ (x : β) in f, u x ≠ ⊥ → (p x ↔ q x)
a : α
b : β
hb : u b ≠ ⊥ → (p b ↔ q b)
hu : u b ≠ ⊥
⊢ p b → u b ≤ a ↔ q b → u b ≤ a
case e_a.h
α : Type u_2
β : Type u_1
γ : Type ?u.110090
ι : Type ?u.110093
inst✝ : CompleteLattice α
f : Filter β
p q : β → Prop
u : β → α
h : ∀ᶠ (x : β) in f, u x ≠ ⊥ → (p x ↔ q x)
a : α
b : β
hb : u b ≠ ⊥ → (p b ↔ q b)
⊢ p b → u b ≤ a ↔ q b → u b ≤ a
cases' eq_or_ne (u b) ⊥ with hu hu
no goals
case e_a.h.inr
α : Type u_2
β : Type u_1
γ : Type ?u.110090
ι : Type ?u.110093
inst✝ : CompleteLattice α
f : Filter β
p q : β → Prop
u : β → α
h : ∀ᶠ (x : β) in f, u x ≠ ⊥ → (p x ↔ q x)
a : α
b : β
hb : u b ≠ ⊥ → (p b ↔ q b)
hu : u b ≠ ⊥
⊢ p b → u b ≤ a ↔ q b → u b ≤ a
rw [hb hu]
no goals
case e_a.h.inl
α : Type u_2
β : Type u_1
γ : Type ?u.110090
ι : Type ?u.110093
inst✝ : CompleteLattice α
f : Filter β
p q : β → Prop
u : β → α
h : ∀ᶠ (x : β) in f, u x ≠ ⊥ → (p x ↔ q x)
a : α
b : β
hb : u b ≠ ⊥ → (p b ↔ q b)
hu : u b = ⊥
⊢ p b → u b ≤ a ↔ q b → u b ≤ a
simp [hu]