-- Mathlib/Topology/Order/Basic.lean
theorem induced_topology_le_preorder [Preorder α] [Preorder β] [TopologicalSpace β]
    [OrderTopology β] {f : α → β} (hf : ∀ {x y}, f x < f y ↔ x < y) :
    induced f ‹TopologicalSpace β› ≤ Preorder.topology α

Proof state:
α : Type u
β : Type v
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
hf : ∀ {x y : α}, f x < f y ↔ x < y
x✝ : TopologicalSpace α := Preorder.topology α
⊢ induced f inst✝¹ ≤ Preorder.topology α

Tactic:
have : OrderTopology α := ⟨rfl⟩

Result:
α : Type u
β : Type v
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
hf : ∀ {x y : α}, f x < f y ↔ x < y
x✝ : TopologicalSpace α := Preorder.topology α
this : OrderTopology α
⊢ induced f inst✝¹ ≤ Preorder.topology α

Proof state:
case refine_1
α : Type u
β : Type v
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
hf : ∀ {x y : α}, f x < f y ↔ x < y
x✝ : TopologicalSpace α := Preorder.topology α
this : OrderTopology α
x a : α
ha : a ∈ {x_1 | f x_1 < f x}
⊢ ⨅ i ∈ {x_1 | x_1 < f x}, 𝓟 (f ⁻¹' {x | i < x}) ≤ 𝓟 {x | f a < f x}

case refine_2
α : Type u
β : Type v
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
hf : ∀ {x y : α}, f x < f y ↔ x < y
x✝ : TopologicalSpace α := Preorder.topology α
this : OrderTopology α
x a : α
ha : a ∈ {x_1 | f x < f x_1}
⊢ ⨅ i ∈ {x_1 | f x < x_1}, 𝓟 (f ⁻¹' {x | x < i}) ≤ 𝓟 {x | f x < f a}

Tactic:
exacts [iInf₂_le (f a) ha, iInf₂_le (f a) ha]

Result:
no goals

Proof state:
α : Type u
β : Type v
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
hf : ∀ {x y : α}, f x < f y ↔ x < y
x✝ : TopologicalSpace α := Preorder.topology α
this : OrderTopology α
x : α
⊢ 𝓝 x ≤ 𝓝 x

Tactic:
simp only [nhds_eq_order, nhds_induced, comap_inf, comap_iInf, comap_principal, Ioi, Iio, ← hf]

Result:
α : Type u
β : Type v
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
hf : ∀ {x y : α}, f x < f y ↔ x < y
x✝ : TopologicalSpace α := Preorder.topology α
this : OrderTopology α
x : α
⊢ (⨅ i ∈ {x_1 | x_1 < f x}, 𝓟 (f ⁻¹' {x | i < x})) ⊓ ⨅ i ∈ {x_1 | f x < x_1}, 𝓟 (f ⁻¹' {x | x < i}) ≤
    (⨅ b ∈ {x_1 | f x_1 < f x}, 𝓟 {x | f b < f x}) ⊓ ⨅ b ∈ {x_1 | f x < f x_1}, 𝓟 {x | f x < f b}

Proof state:
α : Type u
β : Type v
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
hf : ∀ {x y : α}, f x < f y ↔ x < y
x✝ : TopologicalSpace α := Preorder.topology α
this : OrderTopology α
x : α
⊢ (⨅ i ∈ {x_1 | x_1 < f x}, 𝓟 (f ⁻¹' {x | i < x})) ⊓ ⨅ i ∈ {x_1 | f x < x_1}, 𝓟 (f ⁻¹' {x | x < i}) ≤
    (⨅ b ∈ {x_1 | f x_1 < f x}, 𝓟 {x | f b < f x}) ⊓ ⨅ b ∈ {x_1 | f x < f x_1}, 𝓟 {x | f x < f b}

Tactic:
refine inf_le_inf (le_iInf₂ fun a ha => ?_) (le_iInf₂ fun a ha => ?_)

Result:
case refine_1
α : Type u
β : Type v
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
hf : ∀ {x y : α}, f x < f y ↔ x < y
x✝ : TopologicalSpace α := Preorder.topology α
this : OrderTopology α
x a : α
ha : a ∈ {x_1 | f x_1 < f x}
⊢ ⨅ i ∈ {x_1 | x_1 < f x}, 𝓟 (f ⁻¹' {x | i < x}) ≤ 𝓟 {x | f a < f x}

case refine_2
α : Type u
β : Type v
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
hf : ∀ {x y : α}, f x < f y ↔ x < y
x✝ : TopologicalSpace α := Preorder.topology α
this : OrderTopology α
x a : α
ha : a ∈ {x_1 | f x < f x_1}
⊢ ⨅ i ∈ {x_1 | f x < x_1}, 𝓟 (f ⁻¹' {x | x < i}) ≤ 𝓟 {x | f x < f a}

Proof state:
α : Type u
β : Type v
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
hf : ∀ {x y : α}, f x < f y ↔ x < y
x✝ : TopologicalSpace α := Preorder.topology α
this : OrderTopology α
⊢ induced f inst✝¹ ≤ Preorder.topology α

Tactic:
refine le_of_nhds_le_nhds fun x => ?_

Result:
α : Type u
β : Type v
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
hf : ∀ {x y : α}, f x < f y ↔ x < y
x✝ : TopologicalSpace α := Preorder.topology α
this : OrderTopology α
x : α
⊢ 𝓝 x ≤ 𝓝 x

Proof state:
α : Type u
β : Type v
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
hf : ∀ {x y : α}, f x < f y ↔ x < y
⊢ induced f inst✝¹ ≤ Preorder.topology α

Tactic:
let _ := Preorder.topology α

Result:
α : Type u
β : Type v
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
hf : ∀ {x y : α}, f x < f y ↔ x < y
x✝ : TopologicalSpace α := Preorder.topology α
⊢ induced f inst✝¹ ≤ Preorder.topology α