ι : Type ?u.308510
ι' : Type ?u.308513
α : Type u_1
β : Type u_2
γ : Type ?u.308522
inst✝¹ : SemilatticeSup α
inst✝ : SemilatticeSup β
f : α → β
g : β → α
b' : β
hf : Monotone f
gc : ∀ (a : α) (b : β), b ≥ b' → (f a ≤ b ↔ a ≤ g b)
hgi : ∀ (b : β), b ≥ b' → b ≤ f (g b)
⊢ atTop ≤ map f atTop
ι : Type ?u.308510
ι' : Type ?u.308513
α : Type u_1
β : Type u_2
γ : Type ?u.308522
inst✝¹ : SemilatticeSup α
inst✝ : SemilatticeSup β
f : α → β
g : β → α
b' : β
hf : Monotone f
gc : ∀ (a : α) (b : β), b ≥ b' → (f a ≤ b ↔ a ≤ g b)
hgi : ∀ (b : β), b ≥ b' → b ≤ f (g b)
⊢ map f atTop = atTop
refine'
  le_antisymm
    (hf.tendsto_atTop_atTop fun b => ⟨g (b ⊔ b'), le_sup_left.trans <| hgi _ le_sup_right⟩) _
ι : Type ?u.308510
ι' : Type ?u.308513
α : Type u_1
β : Type u_2
γ : Type ?u.308522
inst✝¹ : SemilatticeSup α
inst✝ : SemilatticeSup β
f : α → β
g : β → α
b' : β
hf : Monotone f
gc : ∀ (a : α) (b : β), b ≥ b' → (f a ≤ b ↔ a ≤ g b)
hgi : ∀ (b : β), b ≥ b' → b ≤ f (g b)
⊢ atTop ≤ ⨅ (a : α), 𝓟 (f '' {a' | a ≤ a'})
ι : Type ?u.308510
ι' : Type ?u.308513
α : Type u_1
β : Type u_2
γ : Type ?u.308522
inst✝¹ : SemilatticeSup α
inst✝ : SemilatticeSup β
f : α → β
g : β → α
b' : β
hf : Monotone f
gc : ∀ (a : α) (b : β), b ≥ b' → (f a ≤ b ↔ a ≤ g b)
hgi : ∀ (b : β), b ≥ b' → b ≤ f (g b)
⊢ atTop ≤ map f atTop
rw [@map_atTop_eq _ _ ⟨g b'⟩]
ι : Type ?u.308510
ι' : Type ?u.308513
α : Type u_1
β : Type u_2
γ : Type ?u.308522
inst✝¹ : SemilatticeSup α
inst✝ : SemilatticeSup β
f : α → β
g : β → α
b' : β
hf : Monotone f
gc : ∀ (a : α) (b : β), b ≥ b' → (f a ≤ b ↔ a ≤ g b)
hgi : ∀ (b : β), b ≥ b' → b ≤ f (g b)
a : α
b : β
hb : b ∈ Ici (f a ⊔ b')
⊢ b ∈ f '' {a' | a ≤ a'}
ι : Type ?u.308510
ι' : Type ?u.308513
α : Type u_1
β : Type u_2
γ : Type ?u.308522
inst✝¹ : SemilatticeSup α
inst✝ : SemilatticeSup β
f : α → β
g : β → α
b' : β
hf : Monotone f
gc : ∀ (a : α) (b : β), b ≥ b' → (f a ≤ b ↔ a ≤ g b)
hgi : ∀ (b : β), b ≥ b' → b ≤ f (g b)
⊢ atTop ≤ ⨅ (a : α), 𝓟 (f '' {a' | a ≤ a'})
refine' le_iInf fun a => iInf_le_of_le (f a ⊔ b') <| principal_mono.2 fun b hb => _
ι : Type ?u.308510
ι' : Type ?u.308513
α : Type u_1
β : Type u_2
γ : Type ?u.308522
inst✝¹ : SemilatticeSup α
inst✝ : SemilatticeSup β
f : α → β
g : β → α
b' : β
hf : Monotone f
gc : ∀ (a : α) (b : β), b ≥ b' → (f a ≤ b ↔ a ≤ g b)
hgi : ∀ (b : β), b ≥ b' → b ≤ f (g b)
a : α
b : β
hb : f a ≤ b ∧ b' ≤ b
⊢ b ∈ f '' {a' | a ≤ a'}
ι : Type ?u.308510
ι' : Type ?u.308513
α : Type u_1
β : Type u_2
γ : Type ?u.308522
inst✝¹ : SemilatticeSup α
inst✝ : SemilatticeSup β
f : α → β
g : β → α
b' : β
hf : Monotone f
gc : ∀ (a : α) (b : β), b ≥ b' → (f a ≤ b ↔ a ≤ g b)
hgi : ∀ (b : β), b ≥ b' → b ≤ f (g b)
a : α
b : β
hb : b ∈ Ici (f a ⊔ b')
⊢ b ∈ f '' {a' | a ≤ a'}
rw [mem_Ici, sup_le_iff] at hb
no goals
ι : Type ?u.308510
ι' : Type ?u.308513
α : Type u_1
β : Type u_2
γ : Type ?u.308522
inst✝¹ : SemilatticeSup α
inst✝ : SemilatticeSup β
f : α → β
g : β → α
b' : β
hf : Monotone f
gc : ∀ (a : α) (b : β), b ≥ b' → (f a ≤ b ↔ a ≤ g b)
hgi : ∀ (b : β), b ≥ b' → b ≤ f (g b)
a : α
b : β
hb : f a ≤ b ∧ b' ≤ b
⊢ b ∈ f '' {a' | a ≤ a'}
exact ⟨g b, (gc _ _ hb.2).1 hb.1, le_antisymm ((gc _ _ hb.2).2 le_rfl) (hgi _ hb.2)⟩