α : Type u_2
β : Type u_3
γ : Type u_1
ι : Type ?u.142814
inst✝¹ : CompleteLattice α
f g : Filter β
p q : β → Prop
u v : β → α
inst✝ : CompleteLattice γ
e : α ≃o γ
⊢ sInf ((fun a => ↑e a) '' {a | ∀ᶠ (x : β) in f, p x → u x ≤ a}) = sInf {a | ∀ᶠ (x : β) in f, p x → ↑e (u x) ≤ a}
α : Type u_2
β : Type u_3
γ : Type u_1
ι : Type ?u.142814
inst✝¹ : CompleteLattice α
f g : Filter β
p q : β → Prop
u v : β → α
inst✝ : CompleteLattice γ
e : α ≃o γ
⊢ ↑e (blimsup u f p) = blimsup (↑e ∘ u) f p
simp only [blimsup_eq, map_sInf, Function.comp_apply]
case e_a
α : Type u_2
β : Type u_3
γ : Type u_1
ι : Type ?u.142814
inst✝¹ : CompleteLattice α
f g : Filter β
p q : β → Prop
u v : β → α
inst✝ : CompleteLattice γ
e : α ≃o γ
⊢ (fun a => ↑e a) '' {a | ∀ᶠ (x : β) in f, p x → u x ≤ a} = {a | ∀ᶠ (x : β) in f, p x → ↑e (u x) ≤ a}
α : Type u_2
β : Type u_3
γ : Type u_1
ι : Type ?u.142814
inst✝¹ : CompleteLattice α
f g : Filter β
p q : β → Prop
u v : β → α
inst✝ : CompleteLattice γ
e : α ≃o γ
⊢ sInf ((fun a => ↑e a) '' {a | ∀ᶠ (x : β) in f, p x → u x ≤ a}) = sInf {a | ∀ᶠ (x : β) in f, p x → ↑e (u x) ≤ a}
congr
case e_a.h
α : Type u_2
β : Type u_3
γ : Type u_1
ι : Type ?u.142814
inst✝¹ : CompleteLattice α
f g : Filter β
p q : β → Prop
u v : β → α
inst✝ : CompleteLattice γ
e : α ≃o γ
c : γ
⊢ c ∈ (fun a => ↑e a) '' {a | ∀ᶠ (x : β) in f, p x → u x ≤ a} ↔ c ∈ {a | ∀ᶠ (x : β) in f, p x → ↑e (u x) ≤ a}
case e_a
α : Type u_2
β : Type u_3
γ : Type u_1
ι : Type ?u.142814
inst✝¹ : CompleteLattice α
f g : Filter β
p q : β → Prop
u v : β → α
inst✝ : CompleteLattice γ
e : α ≃o γ
⊢ (fun a => ↑e a) '' {a | ∀ᶠ (x : β) in f, p x → u x ≤ a} = {a | ∀ᶠ (x : β) in f, p x → ↑e (u x) ≤ a}
ext c
case e_a.h.intro
α : Type u_2
β : Type u_3
γ : Type u_1
ι : Type ?u.142814
inst✝¹ : CompleteLattice α
f g : Filter β
p q : β → Prop
u v : β → α
inst✝ : CompleteLattice γ
e : α ≃o γ
a : α
⊢ ↑e a ∈ (fun a => ↑e a) '' {a | ∀ᶠ (x : β) in f, p x → u x ≤ a} ↔ ↑e a ∈ {a | ∀ᶠ (x : β) in f, p x → ↑e (u x) ≤ a}
case e_a.h
α : Type u_2
β : Type u_3
γ : Type u_1
ι : Type ?u.142814
inst✝¹ : CompleteLattice α
f g : Filter β
p q : β → Prop
u v : β → α
inst✝ : CompleteLattice γ
e : α ≃o γ
c : γ
⊢ c ∈ (fun a => ↑e a) '' {a | ∀ᶠ (x : β) in f, p x → u x ≤ a} ↔ c ∈ {a | ∀ᶠ (x : β) in f, p x → ↑e (u x) ≤ a}
obtain ⟨a, rfl⟩ := e.surjective c
no goals
case e_a.h.intro
α : Type u_2
β : Type u_3
γ : Type u_1
ι : Type ?u.142814
inst✝¹ : CompleteLattice α
f g : Filter β
p q : β → Prop
u v : β → α
inst✝ : CompleteLattice γ
e : α ≃o γ
a : α
⊢ ↑e a ∈ (fun a => ↑e a) '' {a | ∀ᶠ (x : β) in f, p x → u x ≤ a} ↔ ↑e a ∈ {a | ∀ᶠ (x : β) in f, p x → ↑e (u x) ≤ a}
simp