case intro
ι : Type ?u.350259
ι' : Type ?u.350262
α : Type u_1
β : Type u_2
γ : Type ?u.350271
inst✝³ : Nonempty α
inst✝² : SemilatticeSup α
inst✝¹ : Preorder β
inst✝ : NoMaxOrder β
f : α → β
h : Tendsto f atTop atTop
M : β
hM : M ∈ upperBounds (range f)
⊢ False
ι : Type ?u.350259
ι' : Type ?u.350262
α : Type u_1
β : Type u_2
γ : Type ?u.350271
inst✝³ : Nonempty α
inst✝² : SemilatticeSup α
inst✝¹ : Preorder β
inst✝ : NoMaxOrder β
f : α → β
h : Tendsto f atTop atTop
⊢ ¬BddAbove (range f)
rintro ⟨M, hM⟩
case intro.intro
ι : Type ?u.350259
ι' : Type ?u.350262
α : Type u_1
β : Type u_2
γ : Type ?u.350271
inst✝³ : Nonempty α
inst✝² : SemilatticeSup α
inst✝¹ : Preorder β
inst✝ : NoMaxOrder β
f : α → β
h : Tendsto f atTop atTop
M : β
hM : M ∈ upperBounds (range f)
a : α
ha : ∀ (b : α), b ≥ a → b ∈ f ⁻¹' Ioi M
⊢ False
case intro
ι : Type ?u.350259
ι' : Type ?u.350262
α : Type u_1
β : Type u_2
γ : Type ?u.350271
inst✝³ : Nonempty α
inst✝² : SemilatticeSup α
inst✝¹ : Preorder β
inst✝ : NoMaxOrder β
f : α → β
h : Tendsto f atTop atTop
M : β
hM : M ∈ upperBounds (range f)
⊢ False
cases' mem_atTop_sets.mp (h <| Ioi_mem_atTop M) with a ha
case intro.intro
ι : Type ?u.350259
ι' : Type ?u.350262
α : Type u_1
β : Type u_2
γ : Type ?u.350271
inst✝³ : Nonempty α
inst✝² : SemilatticeSup α
inst✝¹ : Preorder β
inst✝ : NoMaxOrder β
f : α → β
h : Tendsto f atTop atTop
M : β
hM : M ∈ upperBounds (range f)
a : α
ha : ∀ (b : α), b ≥ a → b ∈ f ⁻¹' Ioi M
⊢ M < M
case intro.intro
ι : Type ?u.350259
ι' : Type ?u.350262
α : Type u_1
β : Type u_2
γ : Type ?u.350271
inst✝³ : Nonempty α
inst✝² : SemilatticeSup α
inst✝¹ : Preorder β
inst✝ : NoMaxOrder β
f : α → β
h : Tendsto f atTop atTop
M : β
hM : M ∈ upperBounds (range f)
a : α
ha : ∀ (b : α), b ≥ a → b ∈ f ⁻¹' Ioi M
⊢ False
apply lt_irrefl M
no goals
case intro.intro
ι : Type ?u.350259
ι' : Type ?u.350262
α : Type u_1
β : Type u_2
γ : Type ?u.350271
inst✝³ : Nonempty α
inst✝² : SemilatticeSup α
inst✝¹ : Preorder β
inst✝ : NoMaxOrder β
f : α → β
h : Tendsto f atTop atTop
M : β
hM : M ∈ upperBounds (range f)
a : α
ha : ∀ (b : α), b ≥ a → b ∈ f ⁻¹' Ioi M
⊢ M < M
calc
  M < f a := ha a le_rfl
  _ ≤ M := hM (Set.mem_range_self a)