-- Mathlib/Order/Filter/AtTopBot/Basic.lean
theorem map_atTop_eq_of_gc_preorder
    [Preorder α] [IsDirected α (· ≤ ·)] [Preorder β] [IsDirected β (· ≤ ·)] {f : α → β}
    (hf : Monotone f) (b : β)
    (hgi : ∀ c ≥ b, ∃ x, f x = c ∧ ∀ a, f a ≤ c ↔ a ≤ x) : map f atTop = atTop

Proof state:
α : Type u_3
β : Type u_4
inst✝³ : Preorder α
inst✝² : IsDirected α fun x1 x2 => x1 ≤ x2
inst✝¹ : Preorder β
inst✝ : IsDirected β fun x1 x2 => x1 ≤ x2
f : α → β
hf : Monotone f
b : β
hgi : ∀ c ≥ b, ∃ x, f x = c ∧ ∀ (a : α), f a ≤ c ↔ a ≤ x
⊢ map f atTop = atTop

Tactic:
have : Nonempty α := (hgi b le_rfl).nonempty

Result:
α : Type u_3
β : Type u_4
inst✝³ : Preorder α
inst✝² : IsDirected α fun x1 x2 => x1 ≤ x2
inst✝¹ : Preorder β
inst✝ : IsDirected β fun x1 x2 => x1 ≤ x2
f : α → β
hf : Monotone f
b : β
hgi : ∀ c ≥ b, ∃ x, f x = c ∧ ∀ (a : α), f a ≤ c ↔ a ≤ x
this : Nonempty α
⊢ map f atTop = atTop

Proof state:
α : Type u_3
β : Type u_4
inst✝³ : Preorder α
inst✝² : IsDirected α fun x1 x2 => x1 ≤ x2
inst✝¹ : Preorder β
inst✝ : IsDirected β fun x1 x2 => x1 ≤ x2
f : α → β
hf : Monotone f
b : β
this : Nonempty α
g : β → α
hfg : ∀ c ≥ b, f (g c) = c
hgle : ∀ c ≥ b, ∀ (a : α), f a ≤ c ↔ a ≤ g c
⊢ map f atTop = atTop

Tactic:
refine le_antisymm (hf.tendsto_atTop_atTop fun c ↦ ?_) ?_

Result:
case refine_1
α : Type u_3
β : Type u_4
inst✝³ : Preorder α
inst✝² : IsDirected α fun x1 x2 => x1 ≤ x2
inst✝¹ : Preorder β
inst✝ : IsDirected β fun x1 x2 => x1 ≤ x2
f : α → β
hf : Monotone f
b : β
this : Nonempty α
g : β → α
hfg : ∀ c ≥ b, f (g c) = c
hgle : ∀ c ≥ b, ∀ (a : α), f a ≤ c ↔ a ≤ g c
c : β
⊢ ∃ a, c ≤ f a

case refine_2
α : Type u_3
β : Type u_4
inst✝³ : Preorder α
inst✝² : IsDirected α fun x1 x2 => x1 ≤ x2
inst✝¹ : Preorder β
inst✝ : IsDirected β fun x1 x2 => x1 ≤ x2
f : α → β
hf : Monotone f
b : β
this : Nonempty α
g : β → α
hfg : ∀ c ≥ b, f (g c) = c
hgle : ∀ c ≥ b, ∀ (a : α), f a ≤ c ↔ a ≤ g c
⊢ atTop ≤ map f atTop

Proof state:
α : Type u_3
β : Type u_4
inst✝³ : Preorder α
inst✝² : IsDirected α fun x1 x2 => x1 ≤ x2
inst✝¹ : Preorder β
inst✝ : IsDirected β fun x1 x2 => x1 ≤ x2
f : α → β
hf : Monotone f
b : β
hgi : ∀ c ≥ b, ∃ x, f x = c ∧ ∀ (a : α), f a ≤ c ↔ a ≤ x
this : Nonempty α
⊢ map f atTop = atTop

Tactic:
choose! g hfg hgle using hgi

Result:
α : Type u_3
β : Type u_4
inst✝³ : Preorder α
inst✝² : IsDirected α fun x1 x2 => x1 ≤ x2
inst✝¹ : Preorder β
inst✝ : IsDirected β fun x1 x2 => x1 ≤ x2
f : α → β
hf : Monotone f
b : β
this : Nonempty α
g : β → α
hfg : ∀ c ≥ b, f (g c) = c
hgle : ∀ c ≥ b, ∀ (a : α), f a ≤ c ↔ a ≤ g c
⊢ map f atTop = atTop

Proof state:
case refine_2
α : Type u_3
β : Type u_4
inst✝³ : Preorder α
inst✝² : IsDirected α fun x1 x2 => x1 ≤ x2
inst✝¹ : Preorder β
inst✝ : IsDirected β fun x1 x2 => x1 ≤ x2
f : α → β
hf : Monotone f
b : β
this✝ : Nonempty α
g : β → α
hfg : ∀ c ≥ b, f (g c) = c
hgle : ∀ c ≥ b, ∀ (a : α), f a ≤ c ↔ a ≤ g c
this : Nonempty α
a : α
a✝ : True
⊢ f '' Ici a ∈ atTop

Tactic:
filter_upwards [eventually_ge_atTop (f a), eventually_ge_atTop b] with c hac hbc

Result:
case h
α : Type u_3
β : Type u_4
inst✝³ : Preorder α
inst✝² : IsDirected α fun x1 x2 => x1 ≤ x2
inst✝¹ : Preorder β
inst✝ : IsDirected β fun x1 x2 => x1 ≤ x2
f : α → β
hf : Monotone f
b : β
this✝ : Nonempty α
g : β → α
hfg : ∀ c ≥ b, f (g c) = c
hgle : ∀ c ≥ b, ∀ (a : α), f a ≤ c ↔ a ≤ g c
this : Nonempty α
a : α
a✝ : True
c : β
hac : f a ≤ c
hbc : b ≤ c
⊢ c ∈ f '' Ici a

Proof state:
case refine_2
α : Type u_3
β : Type u_4
inst✝³ : Preorder α
inst✝² : IsDirected α fun x1 x2 => x1 ≤ x2
inst✝¹ : Preorder β
inst✝ : IsDirected β fun x1 x2 => x1 ≤ x2
f : α → β
hf : Monotone f
b : β
this✝ : Nonempty α
g : β → α
hfg : ∀ c ≥ b, f (g c) = c
hgle : ∀ c ≥ b, ∀ (a : α), f a ≤ c ↔ a ≤ g c
this : Nonempty α
⊢ ∀ (i' : α), True → f '' Ici i' ∈ atTop

Tactic:
intro a _

Result:
case refine_2
α : Type u_3
β : Type u_4
inst✝³ : Preorder α
inst✝² : IsDirected α fun x1 x2 => x1 ≤ x2
inst✝¹ : Preorder β
inst✝ : IsDirected β fun x1 x2 => x1 ≤ x2
f : α → β
hf : Monotone f
b : β
this✝ : Nonempty α
g : β → α
hfg : ∀ c ≥ b, f (g c) = c
hgle : ∀ c ≥ b, ∀ (a : α), f a ≤ c ↔ a ≤ g c
this : Nonempty α
a : α
a✝ : True
⊢ f '' Ici a ∈ atTop

Proof state:
case refine_2
α : Type u_3
β : Type u_4
inst✝³ : Preorder α
inst✝² : IsDirected α fun x1 x2 => x1 ≤ x2
inst✝¹ : Preorder β
inst✝ : IsDirected β fun x1 x2 => x1 ≤ x2
f : α → β
hf : Monotone f
b : β
this✝ : Nonempty α
g : β → α
hfg : ∀ c ≥ b, f (g c) = c
hgle : ∀ c ≥ b, ∀ (a : α), f a ≤ c ↔ a ≤ g c
this : Nonempty α
⊢ atTop ≤ map f atTop

Tactic:
rw [(atTop_basis.map f).ge_iff]

Result:
case refine_2
α : Type u_3
β : Type u_4
inst✝³ : Preorder α
inst✝² : IsDirected α fun x1 x2 => x1 ≤ x2
inst✝¹ : Preorder β
inst✝ : IsDirected β fun x1 x2 => x1 ≤ x2
f : α → β
hf : Monotone f
b : β
this✝ : Nonempty α
g : β → α
hfg : ∀ c ≥ b, f (g c) = c
hgle : ∀ c ≥ b, ∀ (a : α), f a ≤ c ↔ a ≤ g c
this : Nonempty α
⊢ ∀ (i' : α), True → f '' Ici i' ∈ atTop

Proof state:
case refine_1.intro.intro
α : Type u_3
β : Type u_4
inst✝³ : Preorder α
inst✝² : IsDirected α fun x1 x2 => x1 ≤ x2
inst✝¹ : Preorder β
inst✝ : IsDirected β fun x1 x2 => x1 ≤ x2
f : α → β
hf : Monotone f
b : β
this : Nonempty α
g : β → α
hfg : ∀ c ≥ b, f (g c) = c
hgle : ∀ c ≥ b, ∀ (a : α), f a ≤ c ↔ a ≤ g c
c d : β
hcd : c ≤ d
hbd : b ≤ d
⊢ ∃ a, c ≤ f a

Tactic:
exact ⟨g d, hcd.trans (hfg d hbd).ge⟩

Result:
no goals

Proof state:
case refine_1
α : Type u_3
β : Type u_4
inst✝³ : Preorder α
inst✝² : IsDirected α fun x1 x2 => x1 ≤ x2
inst✝¹ : Preorder β
inst✝ : IsDirected β fun x1 x2 => x1 ≤ x2
f : α → β
hf : Monotone f
b : β
this : Nonempty α
g : β → α
hfg : ∀ c ≥ b, f (g c) = c
hgle : ∀ c ≥ b, ∀ (a : α), f a ≤ c ↔ a ≤ g c
c : β
⊢ ∃ a, c ≤ f a

Tactic:
rcases exists_ge_ge c b with ⟨d, hcd, hbd⟩

Result:
case refine_1.intro.intro
α : Type u_3
β : Type u_4
inst✝³ : Preorder α
inst✝² : IsDirected α fun x1 x2 => x1 ≤ x2
inst✝¹ : Preorder β
inst✝ : IsDirected β fun x1 x2 => x1 ≤ x2
f : α → β
hf : Monotone f
b : β
this : Nonempty α
g : β → α
hfg : ∀ c ≥ b, f (g c) = c
hgle : ∀ c ≥ b, ∀ (a : α), f a ≤ c ↔ a ≤ g c
c d : β
hcd : c ≤ d
hbd : b ≤ d
⊢ ∃ a, c ≤ f a

Proof state:
case h
α : Type u_3
β : Type u_4
inst✝³ : Preorder α
inst✝² : IsDirected α fun x1 x2 => x1 ≤ x2
inst✝¹ : Preorder β
inst✝ : IsDirected β fun x1 x2 => x1 ≤ x2
f : α → β
hf : Monotone f
b : β
this✝ : Nonempty α
g : β → α
hfg : ∀ c ≥ b, f (g c) = c
hgle : ∀ c ≥ b, ∀ (a : α), f a ≤ c ↔ a ≤ g c
this : Nonempty α
a : α
a✝ : True
c : β
hac : f a ≤ c
hbc : b ≤ c
⊢ c ∈ f '' Ici a

Tactic:
exact ⟨g c, (hgle _ hbc _).1 hac, hfg _ hbc⟩

Result:
no goals

Proof state:
case refine_2
α : Type u_3
β : Type u_4
inst✝³ : Preorder α
inst✝² : IsDirected α fun x1 x2 => x1 ≤ x2
inst✝¹ : Preorder β
inst✝ : IsDirected β fun x1 x2 => x1 ≤ x2
f : α → β
hf : Monotone f
b : β
this : Nonempty α
g : β → α
hfg : ∀ c ≥ b, f (g c) = c
hgle : ∀ c ≥ b, ∀ (a : α), f a ≤ c ↔ a ≤ g c
⊢ atTop ≤ map f atTop

Tactic:
have : Nonempty α := ⟨g b⟩

Result:
case refine_2
α : Type u_3
β : Type u_4
inst✝³ : Preorder α
inst✝² : IsDirected α fun x1 x2 => x1 ≤ x2
inst✝¹ : Preorder β
inst✝ : IsDirected β fun x1 x2 => x1 ≤ x2
f : α → β
hf : Monotone f
b : β
this✝ : Nonempty α
g : β → α
hfg : ∀ c ≥ b, f (g c) = c
hgle : ∀ c ≥ b, ∀ (a : α), f a ≤ c ↔ a ≤ g c
this : Nonempty α
⊢ atTop ≤ map f atTop