-- Mathlib/Topology/Algebra/FilterBasis.lean
theorem nhds_eq (B : GroupFilterBasis G) {x₀ : G} : @nhds G B.topology x₀ = B.N x₀

Proof state:
G : Type u
inst✝ : Group G
B : GroupFilterBasis G
x₀ : G
⊢ 𝓝 x₀ = B.N x₀

Tactic:
apply TopologicalSpace.nhds_mkOfNhds_of_hasBasis (fun x ↦ (FilterBasis.hasBasis _).map _)

Result:
case hpure
G : Type u
inst✝ : Group G
B : GroupFilterBasis G
x₀ : G
⊢ ∀ (a : G), ∀ i ∈ toFilterBasis, a ∈ (fun y => a * y) '' id i

case hopen
G : Type u
inst✝ : Group G
B : GroupFilterBasis G
x₀ : G
⊢ ∀ (a : G),
    ∀ i ∈ toFilterBasis,
      ∀ᶠ (x : G) in map (fun y => a * y) toFilterBasis.filter,
        (fun y => a * y) '' id i ∈ map (fun y => x * y) toFilterBasis.filter

Proof state:
case hpure
G : Type u
inst✝ : Group G
B : GroupFilterBasis G
x₀ : G
⊢ ∀ (a : G), ∀ i ∈ toFilterBasis, a ∈ (fun y => a * y) '' id i

Tactic:
intro a U U_in

Result:
case hpure
G : Type u
inst✝ : Group G
B : GroupFilterBasis G
x₀ a : G
U : Set G
U_in : U ∈ toFilterBasis
⊢ a ∈ (fun y => a * y) '' id U

Proof state:
case hpure
G : Type u
inst✝ : Group G
B : GroupFilterBasis G
x₀ a : G
U : Set G
U_in : U ∈ toFilterBasis
⊢ a ∈ (fun y => a * y) '' id U

Tactic:
exact ⟨1, B.one U_in, mul_one a⟩

Result:
no goals

Proof state:
case hopen
G : Type u
inst✝ : Group G
B : GroupFilterBasis G
x₀ a : G
U : Set G
U_in : U ∈ toFilterBasis
⊢ ∀ᶠ (x : G) in map (fun y => a * y) toFilterBasis.filter,
    (fun y => a * y) '' id U ∈ map (fun y => x * y) toFilterBasis.filter

Tactic:
rcases GroupFilterBasis.mul U_in with ⟨V, V_in, hVU⟩

Result:
case hopen.intro.intro
G : Type u
inst✝ : Group G
B : GroupFilterBasis G
x₀ a : G
U : Set G
U_in : U ∈ toFilterBasis
V : Set G
V_in : V ∈ B
hVU : V * V ⊆ U
⊢ ∀ᶠ (x : G) in map (fun y => a * y) toFilterBasis.filter,
    (fun y => a * y) '' id U ∈ map (fun y => x * y) toFilterBasis.filter

Proof state:
case h.intro.intro
G : Type u
inst✝ : Group G
B : GroupFilterBasis G
x₀ a : G
U : Set G
U_in : U ∈ toFilterBasis
V : Set G
V_in : V ∈ B
hVU : V * V ⊆ U
x : G
hx : x ∈ V
⊢ (fun y => a * y) '' id U ∈ map (fun y => (fun y => a * y) x * y) toFilterBasis.filter

Tactic:
calc
  (a * x) • V ∈ (a * x) • B.filter := smul_set_mem_smul_filter <| B.mem_filter_of_mem V_in
  _ = a • x • V := smul_smul .. |>.symm
  _ ⊆ a • (V * V) := smul_set_mono <| smul_set_subset_smul hx
  _ ⊆ a • U := smul_set_mono hVU

Result:
no goals

Proof state:
case hopen.intro.intro
G : Type u
inst✝ : Group G
B : GroupFilterBasis G
x₀ a : G
U : Set G
U_in : U ∈ toFilterBasis
V : Set G
V_in : V ∈ B
hVU : V * V ⊆ U
⊢ ∀ᶠ (x : G) in map (fun y => a * y) toFilterBasis.filter,
    (fun y => a * y) '' id U ∈ map (fun y => x * y) toFilterBasis.filter

Tactic:
filter_upwards [image_mem_map (B.mem_filter_of_mem V_in)]

Result:
case h
G : Type u
inst✝ : Group G
B : GroupFilterBasis G
x₀ a : G
U : Set G
U_in : U ∈ toFilterBasis
V : Set G
V_in : V ∈ B
hVU : V * V ⊆ U
⊢ ∀ a_1 ∈ (fun y => a * y) '' V, (fun y => a * y) '' id U ∈ map (fun y => a_1 * y) toFilterBasis.filter

Proof state:
case hopen
G : Type u
inst✝ : Group G
B : GroupFilterBasis G
x₀ : G
⊢ ∀ (a : G),
    ∀ i ∈ toFilterBasis,
      ∀ᶠ (x : G) in map (fun y => a * y) toFilterBasis.filter,
        (fun y => a * y) '' id i ∈ map (fun y => x * y) toFilterBasis.filter

Tactic:
intro a U U_in

Result:
case hopen
G : Type u
inst✝ : Group G
B : GroupFilterBasis G
x₀ a : G
U : Set G
U_in : U ∈ toFilterBasis
⊢ ∀ᶠ (x : G) in map (fun y => a * y) toFilterBasis.filter,
    (fun y => a * y) '' id U ∈ map (fun y => x * y) toFilterBasis.filter

Proof state:
case h
G : Type u
inst✝ : Group G
B : GroupFilterBasis G
x₀ a : G
U : Set G
U_in : U ∈ toFilterBasis
V : Set G
V_in : V ∈ B
hVU : V * V ⊆ U
⊢ ∀ a_1 ∈ (fun y => a * y) '' V, (fun y => a * y) '' id U ∈ map (fun y => a_1 * y) toFilterBasis.filter

Tactic:
rintro _ ⟨x, hx, rfl⟩

Result:
case h.intro.intro
G : Type u
inst✝ : Group G
B : GroupFilterBasis G
x₀ a : G
U : Set G
U_in : U ∈ toFilterBasis
V : Set G
V_in : V ∈ B
hVU : V * V ⊆ U
x : G
hx : x ∈ V
⊢ (fun y => a * y) '' id U ∈ map (fun y => (fun y => a * y) x * y) toFilterBasis.filter