Theorem: mem_nhds_add_iff (DividedPowers/ForMathlib/Topology/LinearTopology.lean)

State before:
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalAddGroup α
V : Set α
a b : α
⊢ V ∈ nhds (a + b) ↔ Add.add a ⁻¹' V ∈ nhds b
Tactic:
constructor
State after:
case mp
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalAddGroup α
V : Set α
a b : α
⊢ V ∈ nhds (a + b) → Add.add a ⁻¹' V ∈ nhds b

case mpr
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalAddGroup α
V : Set α
a b : α
⊢ Add.add a ⁻¹' V ∈ nhds b → V ∈ nhds (a + b)

State before:
case mp
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalAddGroup α
V : Set α
a b : α
⊢ V ∈ nhds (a + b) → Add.add a ⁻¹' V ∈ nhds b

case mpr
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalAddGroup α
V : Set α
a b : α
⊢ Add.add a ⁻¹' V ∈ nhds b → V ∈ nhds (a + b)
Tactic:
. exact fun hV => ContinuousAt.preimage_mem_nhds (continuous_add_left a).continuousAt hV
State after:
case mpr
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalAddGroup α
V : Set α
a b : α
⊢ Add.add a ⁻¹' V ∈ nhds b → V ∈ nhds (a + b)

State before:
case mp
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalAddGroup α
V : Set α
a b : α
⊢ V ∈ nhds (a + b) → Add.add a ⁻¹' V ∈ nhds b
Tactic:
exact fun hV => ContinuousAt.preimage_mem_nhds (continuous_add_left a).continuousAt hV
State after:
no goals

State before:
case mpr
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalAddGroup α
V : Set α
a b : α
⊢ Add.add a ⁻¹' V ∈ nhds b → V ∈ nhds (a + b)
Tactic:
intro hV
State after:
case mpr
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalAddGroup α
V : Set α
a b : α
hV : Add.add a ⁻¹' V ∈ nhds b
⊢ V ∈ nhds (a + b)

State before:
case mpr
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalAddGroup α
V : Set α
a b : α
hV : Add.add a ⁻¹' V ∈ nhds b
⊢ V ∈ nhds (a + b)
Tactic:
suffices h : V = Add.add (-a) ⁻¹' (Add.add a ⁻¹' V) by
  rw [h]
  apply ContinuousAt.preimage_mem_nhds (continuous_add_left (-a)).continuousAt
  convert hV
  apply neg_add_cancel_left
State after:
case mpr
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalAddGroup α
V : Set α
a b : α
hV : Add.add a ⁻¹' V ∈ nhds b
⊢ V = Add.add (-a) ⁻¹' (Add.add a ⁻¹' V)

State before:
case mpr
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalAddGroup α
V : Set α
a b : α
hV : Add.add a ⁻¹' V ∈ nhds b
⊢ V = Add.add (-a) ⁻¹' (Add.add a ⁻¹' V)
Tactic:
rw [Set.preimage_preimage, eq_comm]
State after:
case mpr
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalAddGroup α
V : Set α
a b : α
hV : Add.add a ⁻¹' V ∈ nhds b
⊢ (fun x => Add.add a (Add.add (-a) x)) ⁻¹' V = V

State before:
case mpr
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalAddGroup α
V : Set α
a b : α
hV : Add.add a ⁻¹' V ∈ nhds b
⊢ (fun x => Add.add a (Add.add (-a) x)) ⁻¹' V = V
Tactic:
convert Set.preimage_id'
State after:
case h.e'_2.h.e'_3.h
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalAddGroup α
V : Set α
a b : α
hV : Add.add a ⁻¹' V ∈ nhds b
x✝ : α
⊢ Add.add a (Add.add (-a) x✝) = x✝

State before:
case h.e'_2.h.e'_3.h
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalAddGroup α
V : Set α
a b : α
hV : Add.add a ⁻¹' V ∈ nhds b
x✝ : α
⊢ Add.add a (Add.add (-a) x✝) = x✝
Tactic:
apply add_neg_cancel_left a
State after:
no goals

State before:
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalAddGroup α
V : Set α
a b : α
hV : Add.add a ⁻¹' V ∈ nhds b
h : V = Add.add (-a) ⁻¹' (Add.add a ⁻¹' V)
⊢ V ∈ nhds (a + b)
Tactic:
rw [h]
State after:
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalAddGroup α
V : Set α
a b : α
hV : Add.add a ⁻¹' V ∈ nhds b
h : V = Add.add (-a) ⁻¹' (Add.add a ⁻¹' V)
⊢ Add.add (-a) ⁻¹' (Add.add a ⁻¹' V) ∈ nhds (a + b)

State before:
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalAddGroup α
V : Set α
a b : α
hV : Add.add a ⁻¹' V ∈ nhds b
h : V = Add.add (-a) ⁻¹' (Add.add a ⁻¹' V)
⊢ Add.add (-a) ⁻¹' (Add.add a ⁻¹' V) ∈ nhds (a + b)
Tactic:
apply ContinuousAt.preimage_mem_nhds (continuous_add_left (-a)).continuousAt
State after:
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalAddGroup α
V : Set α
a b : α
hV : Add.add a ⁻¹' V ∈ nhds b
h : V = Add.add (-a) ⁻¹' (Add.add a ⁻¹' V)
⊢ Add.add a ⁻¹' V ∈ nhds (-a + (a + b))

State before:
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalAddGroup α
V : Set α
a b : α
hV : Add.add a ⁻¹' V ∈ nhds b
h : V = Add.add (-a) ⁻¹' (Add.add a ⁻¹' V)
⊢ Add.add a ⁻¹' V ∈ nhds (-a + (a + b))
Tactic:
convert hV
State after:
case h.e'_5.h.e'_3
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalAddGroup α
V : Set α
a b : α
hV : Add.add a ⁻¹' V ∈ nhds b
h : V = Add.add (-a) ⁻¹' (Add.add a ⁻¹' V)
⊢ -a + (a + b) = b

State before:
case h.e'_5.h.e'_3
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalAddGroup α
V : Set α
a b : α
hV : Add.add a ⁻¹' V ∈ nhds b
h : V = Add.add (-a) ⁻¹' (Add.add a ⁻¹' V)
⊢ -a + (a + b) = b
Tactic:
apply neg_add_cancel_left
State after:
no goals