Theorem: TopologicalSpace.le_iff_nhds_le (DividedPowers/ForMathlib/Topology/LinearTopology.lean)

State before:
α : Type u_1
τ τ' : TopologicalSpace α
⊢ τ ≤ τ' ↔ ∀ (s : Set α), ∀ a ∈ s, s ∈ nhds a → s ∈ nhds a
Tactic:
rw [le_iff_nhds]
State after:
α : Type u_1
τ τ' : TopologicalSpace α
⊢ (∀ (x : α), nhds x ≤ nhds x) ↔ ∀ (s : Set α), ∀ a ∈ s, s ∈ nhds a → s ∈ nhds a

State before:
α : Type u_1
τ τ' : TopologicalSpace α
⊢ (∀ (x : α), nhds x ≤ nhds x) ↔ ∀ (s : Set α), ∀ a ∈ s, s ∈ nhds a → s ∈ nhds a
Tactic:
rw [forall_comm]
State after:
α : Type u_1
τ τ' : TopologicalSpace α
⊢ (∀ (x : α), nhds x ≤ nhds x) ↔ ∀ (b : α) (a : Set α), b ∈ a → a ∈ nhds b → a ∈ nhds b

State before:
α : Type u_1
τ τ' : TopologicalSpace α
⊢ (∀ (x : α), nhds x ≤ nhds x) ↔ ∀ (b : α) (a : Set α), b ∈ a → a ∈ nhds b → a ∈ nhds b
Tactic:
apply forall_congr'
State after:
case h
α : Type u_1
τ τ' : TopologicalSpace α
⊢ ∀ (a : α), nhds a ≤ nhds a ↔ ∀ (a_1 : Set α), a ∈ a_1 → a_1 ∈ nhds a → a_1 ∈ nhds a

State before:
case h
α : Type u_1
τ τ' : TopologicalSpace α
⊢ ∀ (a : α), nhds a ≤ nhds a ↔ ∀ (a_1 : Set α), a ∈ a_1 → a_1 ∈ nhds a → a_1 ∈ nhds a
Tactic:
intro a
State after:
case h
α : Type u_1
τ τ' : TopologicalSpace α
a : α
⊢ nhds a ≤ nhds a ↔ ∀ (a_1 : Set α), a ∈ a_1 → a_1 ∈ nhds a → a_1 ∈ nhds a

State before:
case h
α : Type u_1
τ τ' : TopologicalSpace α
a : α
⊢ nhds a ≤ nhds a ↔ ∀ (a_1 : Set α), a ∈ a_1 → a_1 ∈ nhds a → a_1 ∈ nhds a
Tactic:
rw [Filter.le_def]
State after:
case h
α : Type u_1
τ τ' : TopologicalSpace α
a : α
⊢ (∀ x ∈ nhds a, x ∈ nhds a) ↔ ∀ (a_1 : Set α), a ∈ a_1 → a_1 ∈ nhds a → a_1 ∈ nhds a

State before:
case h
α : Type u_1
τ τ' : TopologicalSpace α
a : α
⊢ (∀ x ∈ nhds a, x ∈ nhds a) ↔ ∀ (a_1 : Set α), a ∈ a_1 → a_1 ∈ nhds a → a_1 ∈ nhds a
Tactic:
apply forall_congr'
State after:
case h.h
α : Type u_1
τ τ' : TopologicalSpace α
a : α
⊢ ∀ (a_1 : Set α), a_1 ∈ nhds a → a_1 ∈ nhds a ↔ a ∈ a_1 → a_1 ∈ nhds a → a_1 ∈ nhds a

State before:
case h.h
α : Type u_1
τ τ' : TopologicalSpace α
a : α
⊢ ∀ (a_1 : Set α), a_1 ∈ nhds a → a_1 ∈ nhds a ↔ a ∈ a_1 → a_1 ∈ nhds a → a_1 ∈ nhds a
Tactic:
intro s
State after:
case h.h
α : Type u_1
τ τ' : TopologicalSpace α
a : α
s : Set α
⊢ s ∈ nhds a → s ∈ nhds a ↔ a ∈ s → s ∈ nhds a → s ∈ nhds a

State before:
case h.h
α : Type u_1
τ τ' : TopologicalSpace α
a : α
s : Set α
⊢ s ∈ nhds a → s ∈ nhds a ↔ a ∈ s → s ∈ nhds a → s ∈ nhds a
Tactic:
constructor
State after:
case h.h.mp
α : Type u_1
τ τ' : TopologicalSpace α
a : α
s : Set α
⊢ (s ∈ nhds a → s ∈ nhds a) → a ∈ s → s ∈ nhds a → s ∈ nhds a

case h.h.mpr
α : Type u_1
τ τ' : TopologicalSpace α
a : α
s : Set α
⊢ (a ∈ s → s ∈ nhds a → s ∈ nhds a) → s ∈ nhds a → s ∈ nhds a

State before:
case h.h.mp
α : Type u_1
τ τ' : TopologicalSpace α
a : α
s : Set α
⊢ (s ∈ nhds a → s ∈ nhds a) → a ∈ s → s ∈ nhds a → s ∈ nhds a
Tactic:
exact fun h _ ↦ h
State after:
no goals

State before:
case h.h.mpr
α : Type u_1
τ τ' : TopologicalSpace α
a : α
s : Set α
⊢ (a ∈ s → s ∈ nhds a → s ∈ nhds a) → s ∈ nhds a → s ∈ nhds a
Tactic:
intro h
State after:
case h.h.mpr
α : Type u_1
τ τ' : TopologicalSpace α
a : α
s : Set α
h : a ∈ s → s ∈ nhds a → s ∈ nhds a
⊢ s ∈ nhds a → s ∈ nhds a

State before:
case h.h.mpr
α : Type u_1
τ τ' : TopologicalSpace α
a : α
s : Set α
h : a ∈ s → s ∈ nhds a → s ∈ nhds a
⊢ s ∈ nhds a → s ∈ nhds a
Tactic:
by_cases ha : a ∈ s
State after:
case pos
α : Type u_1
τ τ' : TopologicalSpace α
a : α
s : Set α
h : a ∈ s → s ∈ nhds a → s ∈ nhds a
ha : a ∈ s
⊢ s ∈ nhds a → s ∈ nhds a

case neg
α : Type u_1
τ τ' : TopologicalSpace α
a : α
s : Set α
h : a ∈ s → s ∈ nhds a → s ∈ nhds a
ha : a ∉ s
⊢ s ∈ nhds a → s ∈ nhds a

State before:
case pos
α : Type u_1
τ τ' : TopologicalSpace α
a : α
s : Set α
h : a ∈ s → s ∈ nhds a → s ∈ nhds a
ha : a ∈ s
⊢ s ∈ nhds a → s ∈ nhds a
Tactic:
exact h ha
State after:
no goals

State before:
case neg
α : Type u_1
τ τ' : TopologicalSpace α
a : α
s : Set α
h : a ∈ s → s ∈ nhds a → s ∈ nhds a
ha : a ∉ s
⊢ s ∈ nhds a → s ∈ nhds a
Tactic:
exact fun hs ↦ False.elim (ha (mem_of_mem_nhds hs))
State after:
no goals