Theorem: TopologicalAddGroup.ext_iff_nhds_zero (DividedPowers/ForMathlib/Topology/LinearTopology.lean)

State before:
α : Type u_1
inst✝² : AddCommGroup α
τ : TopologicalSpace α
inst✝¹ : TopologicalAddGroup α
τ' : TopologicalSpace α
inst✝ : TopologicalAddGroup α
⊢ τ = τ' ↔ nhds 0 = nhds 0
Tactic:
rw [TopologicalSpace.ext_iff_nhds]
State after:
α : Type u_1
inst✝² : AddCommGroup α
τ : TopologicalSpace α
inst✝¹ : TopologicalAddGroup α
τ' : TopologicalSpace α
inst✝ : TopologicalAddGroup α
⊢ (∀ (x : α), nhds x = nhds x) ↔ nhds 0 = nhds 0

State before:
α : Type u_1
inst✝² : AddCommGroup α
τ : TopologicalSpace α
inst✝¹ : TopologicalAddGroup α
τ' : TopologicalSpace α
inst✝ : TopologicalAddGroup α
⊢ (∀ (x : α), nhds x = nhds x) ↔ nhds 0 = nhds 0
Tactic:
constructor
State after:
case mp
α : Type u_1
inst✝² : AddCommGroup α
τ : TopologicalSpace α
inst✝¹ : TopologicalAddGroup α
τ' : TopologicalSpace α
inst✝ : TopologicalAddGroup α
⊢ (∀ (x : α), nhds x = nhds x) → nhds 0 = nhds 0

case mpr
α : Type u_1
inst✝² : AddCommGroup α
τ : TopologicalSpace α
inst✝¹ : TopologicalAddGroup α
τ' : TopologicalSpace α
inst✝ : TopologicalAddGroup α
⊢ nhds 0 = nhds 0 → ∀ (x : α), nhds x = nhds x

State before:
case mp
α : Type u_1
inst✝² : AddCommGroup α
τ : TopologicalSpace α
inst✝¹ : TopologicalAddGroup α
τ' : TopologicalSpace α
inst✝ : TopologicalAddGroup α
⊢ (∀ (x : α), nhds x = nhds x) → nhds 0 = nhds 0
Tactic:
intro h
State after:
case mp
α : Type u_1
inst✝² : AddCommGroup α
τ : TopologicalSpace α
inst✝¹ : TopologicalAddGroup α
τ' : TopologicalSpace α
inst✝ : TopologicalAddGroup α
h : ∀ (x : α), nhds x = nhds x
⊢ nhds 0 = nhds 0

State before:
case mp
α : Type u_1
inst✝² : AddCommGroup α
τ : TopologicalSpace α
inst✝¹ : TopologicalAddGroup α
τ' : TopologicalSpace α
inst✝ : TopologicalAddGroup α
h : ∀ (x : α), nhds x = nhds x
⊢ nhds 0 = nhds 0
Tactic:
exact h 0
State after:
no goals

State before:
case mpr
α : Type u_1
inst✝² : AddCommGroup α
τ : TopologicalSpace α
inst✝¹ : TopologicalAddGroup α
τ' : TopologicalSpace α
inst✝ : TopologicalAddGroup α
⊢ nhds 0 = nhds 0 → ∀ (x : α), nhds x = nhds x
Tactic:
intro h a
State after:
case mpr
α : Type u_1
inst✝² : AddCommGroup α
τ : TopologicalSpace α
inst✝¹ : TopologicalAddGroup α
τ' : TopologicalSpace α
inst✝ : TopologicalAddGroup α
h : nhds 0 = nhds 0
a : α
⊢ nhds a = nhds a

State before:
case mpr
α : Type u_1
inst✝² : AddCommGroup α
τ : TopologicalSpace α
inst✝¹ : TopologicalAddGroup α
τ' : TopologicalSpace α
inst✝ : TopologicalAddGroup α
h : nhds 0 = nhds 0
a : α
⊢ nhds a = nhds a
Tactic:
ext s
State after:
case mpr.a
α : Type u_1
inst✝² : AddCommGroup α
τ : TopologicalSpace α
inst✝¹ : TopologicalAddGroup α
τ' : TopologicalSpace α
inst✝ : TopologicalAddGroup α
h : nhds 0 = nhds 0
a : α
s : Set α
⊢ s ∈ nhds a ↔ s ∈ nhds a

State before:
case mpr.a
α : Type u_1
inst✝² : AddCommGroup α
τ : TopologicalSpace α
inst✝¹ : TopologicalAddGroup α
τ' : TopologicalSpace α
inst✝ : TopologicalAddGroup α
h : nhds 0 = nhds 0
a : α
s : Set α
⊢ s ∈ nhds a ↔ s ∈ nhds a
Tactic:
rw [← add_zero a]
State after:
case mpr.a
α : Type u_1
inst✝² : AddCommGroup α
τ : TopologicalSpace α
inst✝¹ : TopologicalAddGroup α
τ' : TopologicalSpace α
inst✝ : TopologicalAddGroup α
h : nhds 0 = nhds 0
a : α
s : Set α
⊢ s ∈ nhds (a + 0) ↔ s ∈ nhds (a + 0)

State before:
case mpr.a
α : Type u_1
inst✝² : AddCommGroup α
τ : TopologicalSpace α
inst✝¹ : TopologicalAddGroup α
τ' : TopologicalSpace α
inst✝ : TopologicalAddGroup α
h : nhds 0 = nhds 0
a : α
s : Set α
⊢ s ∈ nhds (a + 0) ↔ s ∈ nhds (a + 0)
Tactic:
simp only [mem_nhds_add_iff, h]
State after:
no goals