case refine_1
α✝ : Type u
β✝ : Type v
γ : Type w
α : Type u_1
β : Type u_2
inst✝² : LinearOrder α
inst✝¹ : LinearOrder β
t : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
hf : StrictMono f
hc : OrdConnected (range f)
a✝ : α
b✝ : β
x✝ : α
h₁ : b✝ < f a✝
h₂ : ¬b✝ < f x✝
⊢ ∃ y, y < a✝ ∧ b✝ ≤ f y

case refine_2
α✝ : Type u
β✝ : Type v
γ : Type w
α : Type u_1
β : Type u_2
inst✝² : LinearOrder α
inst✝¹ : LinearOrder β
t : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
hf : StrictMono f
hc : OrdConnected (range f)
a✝ : α
b✝ : β
x✝ : α
h₁ : f a✝ < b✝
h₂ : ¬f x✝ < b✝
⊢ ∃ y, a✝ < y ∧ f y ≤ b✝
α✝ : Type u
β✝ : Type v
γ : Type w
α : Type u_1
β : Type u_2
inst✝² : LinearOrder α
inst✝¹ : LinearOrder β
t : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
hf : StrictMono f
hc : OrdConnected (range f)
⊢ induced f t = Preorder.topology α
refine induced_topology_eq_preorder hf.lt_iff_lt (fun h₁ h₂ => ?_) fun h₁ h₂ => ?_
case refine_1.intro
α✝ : Type u
β✝ : Type v
γ : Type w
α : Type u_1
β : Type u_2
inst✝² : LinearOrder α
inst✝¹ : LinearOrder β
t : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
hf : StrictMono f
hc : OrdConnected (range f)
a✝ x✝ y : α
h₁ : f y < f a✝
h₂ : ¬f y < f x✝
⊢ ∃ y_1, y_1 < a✝ ∧ f y ≤ f y_1
case refine_1
α✝ : Type u
β✝ : Type v
γ : Type w
α : Type u_1
β : Type u_2
inst✝² : LinearOrder α
inst✝¹ : LinearOrder β
t : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
hf : StrictMono f
hc : OrdConnected (range f)
a✝ : α
b✝ : β
x✝ : α
h₁ : b✝ < f a✝
h₂ : ¬b✝ < f x✝
⊢ ∃ y, y < a✝ ∧ b✝ ≤ f y
rcases hc.out (mem_range_self _) (mem_range_self _) ⟨not_lt.1 h₂, h₁.le⟩ with ⟨y, rfl⟩
no goals
case refine_1.intro
α✝ : Type u
β✝ : Type v
γ : Type w
α : Type u_1
β : Type u_2
inst✝² : LinearOrder α
inst✝¹ : LinearOrder β
t : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
hf : StrictMono f
hc : OrdConnected (range f)
a✝ x✝ y : α
h₁ : f y < f a✝
h₂ : ¬f y < f x✝
⊢ ∃ y_1, y_1 < a✝ ∧ f y ≤ f y_1
exact ⟨y, hf.lt_iff_lt.1 h₁, le_rfl⟩
case refine_2.intro
α✝ : Type u
β✝ : Type v
γ : Type w
α : Type u_1
β : Type u_2
inst✝² : LinearOrder α
inst✝¹ : LinearOrder β
t : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
hf : StrictMono f
hc : OrdConnected (range f)
a✝ x✝ y : α
h₁ : f a✝ < f y
h₂ : ¬f x✝ < f y
⊢ ∃ y_1, a✝ < y_1 ∧ f y_1 ≤ f y
case refine_2
α✝ : Type u
β✝ : Type v
γ : Type w
α : Type u_1
β : Type u_2
inst✝² : LinearOrder α
inst✝¹ : LinearOrder β
t : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
hf : StrictMono f
hc : OrdConnected (range f)
a✝ : α
b✝ : β
x✝ : α
h₁ : f a✝ < b✝
h₂ : ¬f x✝ < b✝
⊢ ∃ y, a✝ < y ∧ f y ≤ b✝
rcases hc.out (mem_range_self _) (mem_range_self _) ⟨h₁.le, not_lt.1 h₂⟩ with ⟨y, rfl⟩
no goals
case refine_2.intro
α✝ : Type u
β✝ : Type v
γ : Type w
α : Type u_1
β : Type u_2
inst✝² : LinearOrder α
inst✝¹ : LinearOrder β
t : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
hf : StrictMono f
hc : OrdConnected (range f)
a✝ x✝ y : α
h₁ : f a✝ < f y
h₂ : ¬f x✝ < f y
⊢ ∃ y_1, a✝ < y_1 ∧ f y_1 ≤ f y
exact ⟨y, hf.lt_iff_lt.1 h₁, le_rfl⟩