awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Algebra.FilterBasis
Goal:
G : Type u
inst : Group G
B : GroupFilterBasis G
x₀ a : G
U : Set G
U_in : Membership.mem (γ := FilterBasis G) (@toFilterBasis _ inst _) U
V : Set G
V_in : V ∈ B
hVU : V * V ⊆ U
x : G
hx : x ∈ V
⊢ (a * x) • V ∈ HSMul.hSMul (β := Filter G) (a * x) (FilterBasis.filter (@toFilterBasis _ inst _))

Tactic:
smul_set_mem_smul_filter <| B.mem_filter_of_mem V_in

Premises used: FilterBasis.mem_filter_of_mem, GroupFilterBasis.toFilterBasis, Filter.smul_set_mem_smul_filter
-- Module: Mathlib.Topology.Algebra.FilterBasis
Goal:
G : Type u
inst : Group G
B : GroupFilterBasis G
x₀ a : G
U : Set G
U_in : Membership.mem (γ := FilterBasis G) (@toFilterBasis _ inst _) U
V : Set G
V_in : V ∈ B
hVU : V * V ⊆ U
x : G
hx : x ∈ V
⊢ (a * x) • V = a • x • V

Tactic:
smul_smul .. |>.symm

Premises used: smul_smul, Eq.symm
-- Module: Mathlib.Topology.Algebra.FilterBasis
Goal:
G : Type u
inst : Group G
B : GroupFilterBasis G
x₀ a : G
U : Set G
U_in : Membership.mem (γ := FilterBasis G) (@toFilterBasis _ inst _) U
V : Set G
V_in : V ∈ B
hVU : V * V ⊆ U
x : G
hx : x ∈ V
⊢ a • x • V ⊆ a • (V * V)

Tactic:
smul_set_mono <| smul_set_subset_smul hx

Premises used: Set.smul_set_mono, Set.smul_set_subset_smul
-- Module: Mathlib.Topology.Algebra.FilterBasis
Goal:
G : Type u
inst : Group G
B : GroupFilterBasis G
x₀ a : G
U : Set G
U_in : Membership.mem (γ := FilterBasis G) (@toFilterBasis _ inst _) U
V : Set G
V_in : V ∈ B
hVU : V * V ⊆ U
x : G
hx : x ∈ V
⊢ a • (V * V) ⊆ a • U

Tactic:
smul_set_mono hVU

Premises used: Set.smul_set_mono
-- Module: Mathlib.Topology.Algebra.FilterBasis
Goal:
G : Type u
inst : Group G
B : GroupFilterBasis G
x₀ a : G
U : Set G
U_in : Membership.mem (γ := FilterBasis G) (@toFilterBasis _ inst _) U
V : Set G
V_in : V ∈ B
hVU : V * V ⊆ U
x : G
hx : x ∈ V
⊢ Membership.mem (γ := Filter G)
    (map (fun (y : G) ↦ (fun (y : G) ↦ a * y) x * y) (FilterBasis.filter (@toFilterBasis _ inst _)))
    ((fun (y : G) ↦ a * y) '' id U)

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

Premises used: HMul.hMul, FilterBasis.mem_filter_of_mem, smul_smul, Set.smul_set_mono, Set.smul_set_subset_smul, GroupFilterBasis.toFilterBasis, Eq.symm, Filter.smul_set_mem_smul_filter, FilterBasis.filter
-- Module: Mathlib.Topology.Algebra.FilterBasis
Goal:
G : Type u
inst : Group G
B : GroupFilterBasis G
rw : B.N 1 = FilterBasis.filter (@toFilterBasis _ inst _)
⊢ Eq.{u + 1} (α := Filter G) (𝓝 1) (FilterBasis.filter (@toFilterBasis _ inst _))

Tactic:
rw [B.nhds_eq]

Premises used: GroupFilterBasis.nhds_eq
-- Module: Mathlib.Topology.Algebra.FilterBasis
Goal:
G : Type u
inst : Group G
B : GroupFilterBasis G
simp :
  Eq.{u + 1} (α := Filter G) (map (fun (y : G) ↦ y) (FilterBasis.filter (@toFilterBasis _ inst _)))
    (FilterBasis.filter (@toFilterBasis _ inst _))
⊢ B.N 1 = FilterBasis.filter (@toFilterBasis _ inst _)

Tactic:
simp only [N, one_mul]

Premises used: GroupFilterBasis.N, one_mul
-- Module: Mathlib.Topology.Algebra.FilterBasis
Goal:
G : Type u
inst : Group G
B : GroupFilterBasis G
⊢ Eq.{u + 1} (α := Filter G) (map (fun (y : G) ↦ y) (FilterBasis.filter (@toFilterBasis _ inst _)))
    (FilterBasis.filter (@toFilterBasis _ inst _))

Tactic:
map_id

Premises used: Filter.map_id
-- Module: Mathlib.Topology.Algebra.FilterBasis
Goal:
G : Type u
inst : Group G
B : GroupFilterBasis G
⊢ Eq.{u + 1} (α := Filter G) (map (fun (y : G) ↦ y) (FilterBasis.filter (@toFilterBasis _ inst _)))
    (FilterBasis.filter (@toFilterBasis _ inst _))

Tactic:
exact map_id

Premises used: Filter.map_id
-- Module: Mathlib.Topology.Algebra.FilterBasis
Goal:
G : Type u
inst : Group G
B : GroupFilterBasis G
x₀ : G
rw : (B.N x₀).HasBasis (fun (V : Set G) ↦ V ∈ B) fun (V : Set G) ↦ (fun (y : G) ↦ x₀ * y) '' V
⊢ (𝓝 x₀).HasBasis (fun (V : Set G) ↦ V ∈ B) fun (V : Set G) ↦ (fun (y : G) ↦ x₀ * y) '' V

Tactic:
rw [B.nhds_eq]

Premises used: GroupFilterBasis.nhds_eq
-- Module: Mathlib.Topology.Algebra.FilterBasis
Goal:
G : Type u
inst : Group G
B : GroupFilterBasis G
x₀ : G
⊢ (B.N x₀).HasBasis (fun (V : Set G) ↦ V ∈ B) fun (V : Set G) ↦ (fun (y : G) ↦ x₀ * y) '' V

Tactic:
apply B.hasBasis

Premises used: GroupFilterBasis.hasBasis
-- Module: Mathlib.Topology.Algebra.FilterBasis
Goal:
G : Type u
inst : Group G
B : GroupFilterBasis G
rw : HasBasis (FilterBasis.filter (@toFilterBasis _ inst _)) (fun (V : Set G) ↦ V ∈ B) id
⊢ HasBasis (𝓝 1) (fun (V : Set G) ↦ V ∈ B) id

Tactic:
rw [B.nhds_one_eq]

Premises used: GroupFilterBasis.nhds_one_eq
-- Module: Mathlib.Topology.Algebra.FilterBasis
Goal:
G : Type u
inst : Group G
B : GroupFilterBasis G
⊢ HasBasis (FilterBasis.filter (@toFilterBasis _ inst _)) (fun (V : Set G) ↦ V ∈ B) id

Tactic:
B.toFilterBasis.hasBasis

Premises used: FilterBasis.hasBasis, GroupFilterBasis.toFilterBasis
-- Module: Mathlib.Topology.Algebra.FilterBasis
Goal:
G : Type u
inst : Group G
B : GroupFilterBasis G
⊢ HasBasis (FilterBasis.filter (@toFilterBasis _ inst _)) (fun (V : Set G) ↦ V ∈ B) id

Tactic:
exact B.toFilterBasis.hasBasis

Premises used: FilterBasis.hasBasis, GroupFilterBasis.toFilterBasis
-- Module: Mathlib.Topology.Algebra.FilterBasis
Goal:
G : Type u
inst : Group G
B : GroupFilterBasis G
U : Set G
hU : U ∈ B
rw : ∃ i ∈ B, id i ⊆ U
⊢ Membership.mem (γ := Filter G) (𝓝 1) U

Tactic:
rw [B.nhds_one_hasBasis.mem_iff]

Premises used: Filter.HasBasis.mem_iff, GroupFilterBasis.nhds_one_hasBasis
-- Module: Mathlib.Topology.Algebra.FilterBasis
Goal:
G : Type u
inst : Group G
B : GroupFilterBasis G
U : Set G
hU : U ∈ B
⊢ ∃ i ∈ B, id i ⊆ U

Tactic:
⟨U, hU, rfl.subset⟩

Premises used: Eq.subset, And.intro, Exists.intro, rfl
-- Module: Mathlib.Topology.Algebra.FilterBasis
Goal:
G : Type u
inst : Group G
B : GroupFilterBasis G
U : Set G
hU : U ∈ B
⊢ ∃ i ∈ B, id i ⊆ U

Tactic:
exact ⟨U, hU, rfl.subset⟩
-- Module: Mathlib.Topology.Algebra.FilterBasis
Goal:
G : Type u
inst : Group G
B_1 B : GroupFilterBasis G
this : TopologicalSpace G := B.topology
⊢ HasBasis (𝓝 1) (fun (V : Set G) ↦ V ∈ B) id

Tactic:
have basis := B.nhds_one_hasBasis
-- Module: Mathlib.Topology.Algebra.FilterBasis
Goal:
G : Type u
inst : Group G
B_1 B : GroupFilterBasis G
this : TopologicalSpace G := B.topology
basis : HasBasis (𝓝 1) (fun (V : Set G) ↦ V ∈ B) id
⊢ (SProd.sprod (α := Filter G) (β := Filter G) (𝓝 1) (𝓝 1)).HasBasis (fun (i : Set G × Set G) ↦ i.1 ∈ B ∧ i.2 ∈ B)
    fun (i : Set G × Set G) ↦ id i.1 ×ˢ id i.2

Tactic:
have basis' := basis.prod basis
-- Module: Mathlib.Topology.Algebra.FilterBasis
Goal:
G : Type u
inst : Group G
B_1 B : GroupFilterBasis G
this : TopologicalSpace G := B.topology
basis : HasBasis (𝓝 1) (fun (V : Set G) ↦ V ∈ B) id
basis' :
  (SProd.sprod (α := Filter G) (β := Filter G) (𝓝 1) (𝓝 1)).HasBasis (fun (i : Set G × Set G) ↦ i.1 ∈ B ∧ i.2 ∈ B)
    fun (i : Set G × Set G) ↦ id i.1 ×ˢ id i.2
⊢ IsTopologicalGroup G

Tactic:
IsTopologicalGroup.of_nhds_one ?_ ?_ ?_ ?_

Premises used: IsTopologicalGroup.of_nhds_one
-- Module: Mathlib.Topology.Algebra.FilterBasis
Goal:
G : Type u
inst : Group G
B_1 B : GroupFilterBasis G
this : TopologicalSpace G := B.topology
basis : HasBasis (𝓝 1) (fun (V : Set G) ↦ V ∈ B) id
basis' :
  (SProd.sprod (α := Filter G) (β := Filter G) (𝓝 1) (𝓝 1)).HasBasis (fun (i : Set G × Set G) ↦ i.1 ∈ B ∧ i.2 ∈ B)
    fun (i : Set G × Set G) ↦ id i.1 ×ˢ id i.2
refine_1 :
  Tendsto (β := G) (uncurry fun (x1 x2 : G) ↦ x1 * x2) (SProd.sprod (α := Filter G) (β := Filter G) (𝓝 1) (𝓝 1)) (𝓝 1)
refine_2 : Tendsto (β := G) (fun (x : G) ↦ x⁻¹) (𝓝 1) (𝓝 1)
refine_3 : ∀ (x₀ : G), 𝓝 x₀ = map (fun (x : G) ↦ x₀ * x) (𝓝 1)
refine_4 : ∀ (x₀ : G), Tendsto (β := G) (fun (x : G) ↦ x₀ * x * x₀⁻¹) (𝓝 1) (𝓝 1)
⊢ IsTopologicalGroup G

Tactic:
refine IsTopologicalGroup.of_nhds_one ?_ ?_ ?_ ?_

Premises used: IsTopologicalGroup.of_nhds_one
-- Module: Mathlib.Topology.Algebra.FilterBasis
Goal:
G : Type u
inst : Group G
B_1 B : GroupFilterBasis G
this : TopologicalSpace G := B.topology
basis : HasBasis (𝓝 1) (fun (V : Set G) ↦ V ∈ B) id
basis' :
  (SProd.sprod (α := Filter G) (β := Filter G) (𝓝 1) (𝓝 1)).HasBasis (fun (i : Set G × Set G) ↦ i.1 ∈ B ∧ i.2 ∈ B)
    fun (i : Set G × Set G) ↦ id i.1 ×ˢ id i.2
refine_1 :
  ∀ ib ∈ B,
    ∃ (ia : Set G × Set G),
      (ia.1 ∈ B ∧ ia.2 ∈ B) ∧ ∀ x ∈ id ia.1 ×ˢ id ia.2, uncurry (fun (x1 x2 : G) ↦ x1 * x2) x ∈ id ib
⊢ Tendsto (β := G) (uncurry fun (x1 x2 : G) ↦ x1 * x2) (SProd.sprod (α := Filter G) (β := Filter G) (𝓝 1) (𝓝 1)) (𝓝 1)

Tactic:
rw [basis'.tendsto_iff basis]

Premises used: Filter.HasBasis.tendsto_iff
-- Module: Mathlib.Topology.Algebra.FilterBasis
Goal:
G : Type u
inst : Group G
B_1 B : GroupFilterBasis G
this_1 : TopologicalSpace G := B.topology
basis : HasBasis (𝓝 1) (fun (V : Set G) ↦ V ∈ B) id
basis' :
  (SProd.sprod (α := Filter G) (β := Filter G) (𝓝 1) (𝓝 1)).HasBasis (fun (i : Set G × Set G) ↦ i.1 ∈ B ∧ i.2 ∈ B)
    fun (i : Set G × Set G) ↦ id i.1 ×ˢ id i.2
this : ∀ U ∈ B, ∃ (V : Set G) (W : Set G), (V ∈ B ∧ W ∈ B) ∧ ∀ (a b : G), a ∈ V → b ∈ W → a * b ∈ U
⊢ ∀ ib ∈ B,
    ∃ (ia : Set G × Set G),
      (ia.1 ∈ B ∧ ia.2 ∈ B) ∧ ∀ x ∈ id ia.1 ×ˢ id ia.2, uncurry (fun (x1 x2 : G) ↦ x1 * x2) x ∈ id ib

Tactic:
simpa
-- Module: Mathlib.Topology.Algebra.FilterBasis
Goal:
G : Type u
inst : Group G
B_1 B : GroupFilterBasis G
this : TopologicalSpace G := B.topology
basis : HasBasis (𝓝 1) (fun (V : Set G) ↦ V ∈ B) id
basis' :
  (SProd.sprod (α := Filter G) (β := Filter G) (𝓝 1) (𝓝 1)).HasBasis (fun (i : Set G × Set G) ↦ i.1 ∈ B ∧ i.2 ∈ B)
    fun (i : Set G × Set G) ↦ id i.1 ×ˢ id i.2
refine_1 : ∀ U ∈ B, ∃ (V : Set G) (W : Set G), (V ∈ B ∧ W ∈ B) ∧ ∀ (a b : G), a ∈ V → b ∈ W → a * b ∈ U
⊢ ∀ ib ∈ B,
    ∃ (ia : Set G × Set G),
      (ia.1 ∈ B ∧ ia.2 ∈ B) ∧ ∀ x ∈ id ia.1 ×ˢ id ia.2, uncurry (fun (x1 x2 : G) ↦ x1 * x2) x ∈ id ib

Tactic:
suffices ∀ U ∈ B, ∃ V W, (V ∈ B ∧ W ∈ B) ∧ ∀ a b, a ∈ V → b ∈ W → a * b ∈ U by simpa
-- Module: Mathlib.Topology.Algebra.FilterBasis
Goal:
G : Type u
inst : Group G
B_1 B : GroupFilterBasis G
this : TopologicalSpace G := B.topology
basis : HasBasis (𝓝 1) (fun (V : Set G) ↦ V ∈ B) id
basis' :
  (SProd.sprod (α := Filter G) (β := Filter G) (𝓝 1) (𝓝 1)).HasBasis (fun (i : Set G × Set G) ↦ i.1 ∈ B ∧ i.2 ∈ B)
    fun (i : Set G × Set G) ↦ id i.1 ×ˢ id i.2
U : Set G
U_in : U ∈ B
refine_1 :
  ∀ (V : Set G) (V_in : V ∈ B) (hV : V * V ⊆ U),
    ∃ (V : Set G) (W : Set G), (V ∈ B ∧ W ∈ B) ∧ ∀ (a b : G), a ∈ V → b ∈ W → a * b ∈ U
⊢ ∃ (V : Set G) (W : Set G), (V ∈ B ∧ W ∈ B) ∧ ∀ (a b : G), a ∈ V → b ∈ W → a * b ∈ U

Tactic:
rcases mul U_in with ⟨V, V_in, hV⟩

Premises used: GroupFilterBasis.mul
-- Module: Mathlib.Topology.Algebra.FilterBasis
Goal:
G : Type u
inst : Group G
B_1 B : GroupFilterBasis G
this : TopologicalSpace G := B.topology
basis : HasBasis (𝓝 1) (fun (V : Set G) ↦ V ∈ B) id
basis' :
  (SProd.sprod (α := Filter G) (β := Filter G) (𝓝 1) (𝓝 1)).HasBasis (fun (i : Set G × Set G) ↦ i.1 ∈ B ∧ i.2 ∈ B)
    fun (i : Set G × Set G) ↦ id i.1 ×ˢ id i.2
U : Set G
U_in : U ∈ B
V : Set G
V_in : V ∈ B
hV : V * V ⊆ U
⊢ ∃ (V : Set G) (W : Set G), (V ∈ B ∧ W ∈ B) ∧ ∀ (a b : G), a ∈ V → b ∈ W → a * b ∈ U

Tactic:
⟨V, V, ⟨V_in, V_in⟩, ?_⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.Topology.Algebra.FilterBasis
Goal:
G : Type u
inst : Group G
B_1 B : GroupFilterBasis G
this : TopologicalSpace G := B.topology
basis : HasBasis (𝓝 1) (fun (V : Set G) ↦ V ∈ B) id
basis' :
  (SProd.sprod (α := Filter G) (β := Filter G) (𝓝 1) (𝓝 1)).HasBasis (fun (i : Set G × Set G) ↦ i.1 ∈ B ∧ i.2 ∈ B)
    fun (i : Set G × Set G) ↦ id i.1 ×ˢ id i.2
U : Set G
U_in : U ∈ B
V : Set G
V_in : V ∈ B
hV : V * V ⊆ U
refine_1 : ∀ (a b : G), a ∈ V → b ∈ V → a * b ∈ U
⊢ ∃ (V : Set G) (W : Set G), (V ∈ B ∧ W ∈ B) ∧ ∀ (a b : G), a ∈ V → b ∈ W → a * b ∈ U

Tactic:
refine ⟨V, V, ⟨V_in, V_in⟩, ?_⟩
-- Module: Mathlib.Topology.Algebra.FilterBasis
Goal:
G : Type u
inst : Group G
B_1 B : GroupFilterBasis G
this : TopologicalSpace G := B.topology
basis : HasBasis (𝓝 1) (fun (V : Set G) ↦ V ∈ B) id
basis' :
  (SProd.sprod (α := Filter G) (β := Filter G) (𝓝 1) (𝓝 1)).HasBasis (fun (i : Set G × Set G) ↦ i.1 ∈ B ∧ i.2 ∈ B)
    fun (i : Set G × Set G) ↦ id i.1 ×ˢ id i.2
U : Set G
U_in : U ∈ B
V : Set G
V_in : V ∈ B
hV : V * V ⊆ U
a b : G
a_in : a ∈ V
b_in : b ∈ V
⊢ a * b ∈ U

Tactic:
hV <| mul_mem_mul a_in b_in

Premises used: Set.mul_mem_mul
-- Module: Mathlib.Topology.Algebra.FilterBasis
Goal:
G : Type u
inst : Group G
B_1 B : GroupFilterBasis G
this : TopologicalSpace G := B.topology
basis : HasBasis (𝓝 1) (fun (V : Set G) ↦ V ∈ B) id
basis' :
  (SProd.sprod (α := Filter G) (β := Filter G) (𝓝 1) (𝓝 1)).HasBasis (fun (i : Set G × Set G) ↦ i.1 ∈ B ∧ i.2 ∈ B)
    fun (i : Set G × Set G) ↦ id i.1 ×ˢ id i.2
U : Set G
U_in : U ∈ B
V : Set G
V_in : V ∈ B
hV : V * V ⊆ U
a b : G
a_in : a ∈ V
b_in : b ∈ V
⊢ a * b ∈ U

Tactic:
exact hV <| mul_mem_mul a_in b_in

Premises used: Set.mul_mem_mul
-- Module: Mathlib.Topology.Algebra.FilterBasis
Goal:
G : Type u
inst : Group G
B_1 B : GroupFilterBasis G
this : TopologicalSpace G := B.topology
basis : HasBasis (𝓝 1) (fun (V : Set G) ↦ V ∈ B) id
basis' :
  (SProd.sprod (α := Filter G) (β := Filter G) (𝓝 1) (𝓝 1)).HasBasis (fun (i : Set G × Set G) ↦ i.1 ∈ B ∧ i.2 ∈ B)
    fun (i : Set G × Set G) ↦ id i.1 ×ˢ id i.2
refine_2 : ∀ ib ∈ B, ∃ ia ∈ B, ∀ x ∈ id ia, x⁻¹ ∈ id ib
⊢ Tendsto (β := G) (fun (x : G) ↦ x⁻¹) (𝓝 1) (𝓝 1)

Tactic:
rw [basis.tendsto_iff basis]

Premises used: Filter.HasBasis.tendsto_iff
-- Module: Mathlib.Topology.Algebra.FilterBasis
Goal:
G : Type u
inst : Group G
B_1 B : GroupFilterBasis G
this : TopologicalSpace G := B.topology
basis : HasBasis (𝓝 1) (fun (V : Set G) ↦ V ∈ B) id
basis' :
  (SProd.sprod (α := Filter G) (β := Filter G) (𝓝 1) (𝓝 1)).HasBasis (fun (i : Set G × Set G) ↦ i.1 ∈ B ∧ i.2 ∈ B)
    fun (i : Set G × Set G) ↦ id i.1 ×ˢ id i.2
U : Set G
U_in : U ∈ B
⊢ ∃ ia ∈ B, ∀ x ∈ id ia, x⁻¹ ∈ id U

Tactic:
simpa using inv U_in

Premises used: GroupFilterBasis.inv
-- Module: Mathlib.Topology.Algebra.FilterBasis
Goal:
G : Type u
inst : Group G
B_1 B : GroupFilterBasis G
this : TopologicalSpace G := B.topology
basis : HasBasis (𝓝 1) (fun (V : Set G) ↦ V ∈ B) id
basis' :
  (SProd.sprod (α := Filter G) (β := Filter G) (𝓝 1) (𝓝 1)).HasBasis (fun (i : Set G × Set G) ↦ i.1 ∈ B ∧ i.2 ∈ B)
    fun (i : Set G × Set G) ↦ id i.1 ×ˢ id i.2
x₀ : G
refine_3 : B.N x₀ = map (fun (x : G) ↦ x₀ * x) (FilterBasis.filter (@toFilterBasis _ inst _))
⊢ 𝓝 x₀ = map (fun (x : G) ↦ x₀ * x) (𝓝 1)

Tactic:
rw [nhds_eq, nhds_one_eq]

Premises used: GroupFilterBasis.nhds_one_eq, GroupFilterBasis.nhds_eq
-- Module: Mathlib.Topology.Algebra.FilterBasis
Goal:
G : Type u
inst : Group G
B_1 B : GroupFilterBasis G
this : TopologicalSpace G := B.topology
basis : HasBasis (𝓝 1) (fun (V : Set G) ↦ V ∈ B) id
basis' :
  (SProd.sprod (α := Filter G) (β := Filter G) (𝓝 1) (𝓝 1)).HasBasis (fun (i : Set G × Set G) ↦ i.1 ∈ B ∧ i.2 ∈ B)
    fun (i : Set G × Set G) ↦ id i.1 ×ˢ id i.2
x₀ : G
⊢ B.N x₀ = map (fun (x : G) ↦ x₀ * x) (FilterBasis.filter (@toFilterBasis _ inst _))

Tactic:
rfl
-- Module: Mathlib.Topology.Algebra.FilterBasis
Goal:
G : Type u
inst : Group G
B_1 B : GroupFilterBasis G
this : TopologicalSpace G := B.topology
basis : HasBasis (𝓝 1) (fun (V : Set G) ↦ V ∈ B) id
basis' :
  (SProd.sprod (α := Filter G) (β := Filter G) (𝓝 1) (𝓝 1)).HasBasis (fun (i : Set G × Set G) ↦ i.1 ∈ B ∧ i.2 ∈ B)
    fun (i : Set G × Set G) ↦ id i.1 ×ˢ id i.2
x₀ : G
refine_4 : ∀ ib ∈ B, ∃ ia ∈ B, ∀ x ∈ id ia, x₀ * x * x₀⁻¹ ∈ id ib
⊢ Tendsto (β := G) (fun (x : G) ↦ x₀ * x * x₀⁻¹) (𝓝 1) (𝓝 1)

Tactic:
rw [basis.tendsto_iff basis]

Premises used: Filter.HasBasis.tendsto_iff
-- Module: Mathlib.Topology.Algebra.FilterBasis
Goal:
G : Type u
inst : Group G
B_1 B : GroupFilterBasis G
this : TopologicalSpace G := B.topology
basis : HasBasis (𝓝 1) (fun (V : Set G) ↦ V ∈ B) id
basis' :
  (SProd.sprod (α := Filter G) (β := Filter G) (𝓝 1) (𝓝 1)).HasBasis (fun (i : Set G × Set G) ↦ i.1 ∈ B ∧ i.2 ∈ B)
    fun (i : Set G × Set G) ↦ id i.1 ×ˢ id i.2
x₀ : G
U : Set G
U_in : U ∈ B
⊢ ∃ ia ∈ B, ∀ x ∈ id ia, x₀ * x * x₀⁻¹ ∈ id U

Tactic:
conj x₀ U_in

Premises used: GroupFilterBasis.conj, Set.Mem, Set.Subset, Set.preimage
-- Module: Mathlib.Topology.Algebra.FilterBasis
Goal:
G : Type u
inst : Group G
B_1 B : GroupFilterBasis G
this : TopologicalSpace G := B.topology
basis : HasBasis (𝓝 1) (fun (V : Set G) ↦ V ∈ B) id
basis' :
  (SProd.sprod (α := Filter G) (β := Filter G) (𝓝 1) (𝓝 1)).HasBasis (fun (i : Set G × Set G) ↦ i.1 ∈ B ∧ i.2 ∈ B)
    fun (i : Set G × Set G) ↦ id i.1 ×ˢ id i.2
x₀ : G
U : Set G
U_in : U ∈ B
⊢ ∃ ia ∈ B, ∀ x ∈ id ia, x₀ * x * x₀⁻¹ ∈ id U

Tactic:
exact conj x₀ U_in

Premises used: GroupFilterBasis.conj
-- Module: Mathlib.Topology.Algebra.FilterBasis
Goal:
G : Type u
inst : Group G
t : TopologicalSpace G
F : GroupFilterBasis G
hG : F.topology = t
⊢ IsTopologicalGroup G

Tactic:
have : IsTopologicalGroup G := hG ▸ F.isTopologicalGroup
-- Module: Mathlib.Topology.Algebra.FilterBasis
Goal:
G : Type u
inst : Group G
t : TopologicalSpace G
F : GroupFilterBasis G
hG : F.topology = t
this : IsTopologicalGroup G
rw : IsClosed[t] {1} ↔ Eq (α := Set G) (⋂₀ FilterBasis.sets (@toFilterBasis _ inst _)) {1}
rw₁ : Eq (α := Set G) (closure[t] {1}) {1} ↔ Eq (α := Set G) (⋂₀ FilterBasis.sets (@toFilterBasis _ inst _)) {1}
rw₂ : Eq (α := Set G) (ker (𝓝 1)) {1} ↔ Eq (α := Set G) (⋂₀ FilterBasis.sets (@toFilterBasis _ inst _)) {1}
rw₃ : Eq (α := Set G) (ker (𝓝 1)) {1} ↔ Eq (α := Set G) (⋂₀ FilterBasis.sets (@toFilterBasis _ inst _)) {1}
rw₄ :
  Eq (α := Set G) (ker (FilterBasis.filter (@toFilterBasis _ inst _))) {1} ↔
    Eq (α := Set G) (⋂₀ FilterBasis.sets (@toFilterBasis _ inst _)) {1}
rw₅ rw₆ :
  Eq (α := Set G) (⋂₀ FilterBasis.sets (@toFilterBasis _ inst _)) {1} ↔
    Eq (α := Set G) (⋂₀ FilterBasis.sets (@toFilterBasis _ inst _)) {1}
⊢ T2Space G ↔ Eq (α := Set G) (⋂₀ FilterBasis.sets (@toFilterBasis _ inst _)) {1}

Tactic:
rw [IsTopologicalGroup.t2Space_iff_one_closed, ← closure_eq_iff_isClosed,
    R0Space.closure_singleton, ← hG, F.nhds_one_eq, FilterBasis.ker_filter]

Premises used: GroupFilterBasis.nhds_one_eq, FilterBasis.ker_filter, R0Space.closure_singleton, closure_eq_iff_isClosed, IsTopologicalGroup.t2Space_iff_one_closed
-- Module: Mathlib.Topology.Algebra.FilterBasis
Goal:
G : Type u
inst : Group G
t : TopologicalSpace G
F : GroupFilterBasis G
hG : F.topology = t
rw :
  Subset (α := Set G) (⋂₀ FilterBasis.sets (@toFilterBasis _ inst _)) {1} →
    Subset (α := Set G) {1} (⋂₀ FilterBasis.sets (@toFilterBasis _ inst _))
⊢ T2Space G ↔ Subset (α := Set G) (⋂₀ FilterBasis.sets (@toFilterBasis _ inst _)) {1}

Tactic:
rw [F.t2Space_iff hG, subset_antisymm_iff, and_iff_left_iff_imp]

Premises used: subset_antisymm_iff, and_iff_left_iff_imp, GroupFilterBasis.t2Space_iff
-- Module: Mathlib.Topology.Algebra.FilterBasis
Goal:
G : Type u
inst : Group G
t : TopologicalSpace G
F : GroupFilterBasis G
hG : F.topology = t
⊢ Subset (α := Set G) {1} (⋂₀ FilterBasis.sets (@toFilterBasis _ inst _))

Tactic:
simpa using fun _ ↦ F.one

Premises used: GroupFilterBasis.one
-- Module: Mathlib.Topology.Algebra.FilterBasis
Goal:
R : Type u
inst : Ring R
B : RingFilterBasis R
U : Set R
hU : U ∈ B
⊢ ∃ V ∈ B, V * V ⊆ U

Tactic:
mul' hU

Premises used: RingFilterBasis.mul'
-- Module: Mathlib.Topology.Algebra.FilterBasis
Goal:
R : Type u
inst : Ring R
B : RingFilterBasis R
x₀ : R
U : Set R
hU : U ∈ B
⊢ ∃ V ∈ B, V ⊆ (fun (x : R) ↦ x₀ * x) ⁻¹' U

Tactic:
mul_left' x₀ hU

Premises used: RingFilterBasis.mul_left'
-- Module: Mathlib.Topology.Algebra.FilterBasis
Goal:
R : Type u
inst : Ring R
B : RingFilterBasis R
x₀ : R
U : Set R
hU : U ∈ B
⊢ ∃ V ∈ B, V ⊆ (fun (x : R) ↦ x * x₀) ⁻¹' U

Tactic:
mul_right' x₀ hU

Premises used: RingFilterBasis.mul_right'
-- Module: Mathlib.Topology.Algebra.FilterBasis
Goal:
R_1 : Type u
inst : Ring R_1
B_1 : RingFilterBasis R_1
R : Type u
inst_1 : Ring R
B : RingFilterBasis R
B' : AddGroupFilterBasis R := toAddGroupFilterBasis
this : TopologicalSpace R := B'.topology
⊢ HasBasis (𝓝 0) (fun (V : Set R) ↦ V ∈ B') id

Tactic:
have basis := B'.nhds_zero_hasBasis
-- Module: Mathlib.Topology.Algebra.FilterBasis
Goal:
R_1 : Type u
inst : Ring R_1
B_1 : RingFilterBasis R_1
R : Type u
inst_1 : Ring R
B : RingFilterBasis R
B' : AddGroupFilterBasis R := toAddGroupFilterBasis
this : TopologicalSpace R := B'.topology
basis : HasBasis (𝓝 0) (fun (V : Set R) ↦ V ∈ B') id
⊢ (SProd.sprod (α := Filter R) (β := Filter R) (𝓝 0) (𝓝 0)).HasBasis (fun (i : Set R × Set R) ↦ i.1 ∈ B' ∧ i.2 ∈ B')
    fun (i : Set R × Set R) ↦ id i.1 ×ˢ id i.2

Tactic:
have basis' := basis.prod basis
-- Module: Mathlib.Topology.Algebra.FilterBasis
Goal:
R_1 : Type u
inst : Ring R_1
B_1 : RingFilterBasis R_1
R : Type u
inst_1 : Ring R
B : RingFilterBasis R
B' : AddGroupFilterBasis R := toAddGroupFilterBasis
this : TopologicalSpace R := B'.topology
basis : HasBasis (𝓝 0) (fun (V : Set R) ↦ V ∈ B') id
basis' :
  (SProd.sprod (α := Filter R) (β := Filter R) (𝓝 0) (𝓝 0)).HasBasis (fun (i : Set R × Set R) ↦ i.1 ∈ B' ∧ i.2 ∈ B')
    fun (i : Set R × Set R) ↦ id i.1 ×ˢ id i.2
⊢ IsTopologicalAddGroup R

Tactic:
haveI := B'.isTopologicalAddGroup
-- Module: Mathlib.Topology.Algebra.FilterBasis
Goal:
R_1 : Type u
inst : Ring R_1
B_1 : RingFilterBasis R_1
R : Type u
inst_1 : Ring R
B : RingFilterBasis R
B' : AddGroupFilterBasis R := toAddGroupFilterBasis
this_1 : TopologicalSpace R := B'.topology
basis : HasBasis (𝓝 0) (fun (V : Set R) ↦ V ∈ B') id
basis' :
  (SProd.sprod (α := Filter R) (β := Filter R) (𝓝 0) (𝓝 0)).HasBasis (fun (i : Set R × Set R) ↦ i.1 ∈ B' ∧ i.2 ∈ B')
    fun (i : Set R × Set R) ↦ id i.1 ×ˢ id i.2
this : IsTopologicalAddGroup R
hmul :
  Tendsto (β := R) (uncurry fun (x1 x2 : R) ↦ x1 * x2) (SProd.sprod (α := Filter R) (β := Filter R) (𝓝 0) (𝓝 0)) (𝓝 0)
hmul_left : ∀ (x₀ : R), Tendsto (β := R) (fun (x : R) ↦ x₀ * x) (𝓝 0) (𝓝 0)
hmul_right : ∀ (x₀ : R), Tendsto (β := R) (fun (x : R) ↦ x * x₀) (𝓝 0) (𝓝 0)
⊢ IsTopologicalRing R

Tactic:
apply IsTopologicalRing.of_addGroup_of_nhds_zero

Premises used: IsTopologicalRing.of_addGroup_of_nhds_zero
-- Module: Mathlib.Topology.Algebra.FilterBasis
Goal:
R_1 : Type u
inst : Ring R_1
B_1 : RingFilterBasis R_1
R : Type u
inst_1 : Ring R
B : RingFilterBasis R
B' : AddGroupFilterBasis R := toAddGroupFilterBasis
this_1 : TopologicalSpace R := B'.topology
basis : HasBasis (𝓝 0) (fun (V : Set R) ↦ V ∈ B') id
basis' :
  (SProd.sprod (α := Filter R) (β := Filter R) (𝓝 0) (𝓝 0)).HasBasis (fun (i : Set R × Set R) ↦ i.1 ∈ B' ∧ i.2 ∈ B')
    fun (i : Set R × Set R) ↦ id i.1 ×ˢ id i.2
this : IsTopologicalAddGroup R
hmul :
  ∀ ib ∈ B',
    ∃ (ia : Set R × Set R),
      (ia.1 ∈ B' ∧ ia.2 ∈ B') ∧ ∀ x ∈ id ia.1 ×ˢ id ia.2, uncurry (fun (x1 x2 : R) ↦ x1 * x2) x ∈ id ib
⊢ Tendsto (β := R) (uncurry fun (x1 x2 : R) ↦ x1 * x2) (SProd.sprod (α := Filter R) (β := Filter R) (𝓝 0) (𝓝 0)) (𝓝 0)

Tactic:
rw [basis'.tendsto_iff basis]

Premises used: Filter.HasBasis.tendsto_iff
-- Module: Mathlib.Topology.Algebra.FilterBasis
Goal:
R_1 : Type u
inst : Ring R_1
B_1 : RingFilterBasis R_1
R : Type u
inst_1 : Ring R
B : RingFilterBasis R
B' : AddGroupFilterBasis R := toAddGroupFilterBasis
this_1 : TopologicalSpace R := B'.topology
basis : HasBasis (𝓝 0) (fun (V : Set R) ↦ V ∈ B') id
basis' :
  (SProd.sprod (α := Filter R) (β := Filter R) (𝓝 0) (𝓝 0)).HasBasis (fun (i : Set R × Set R) ↦ i.1 ∈ B' ∧ i.2 ∈ B')
    fun (i : Set R × Set R) ↦ id i.1 ×ˢ id i.2
this_2 : IsTopologicalAddGroup R
this : ∀ U ∈ B', ∃ (V : Set R) (W : Set R), (V ∈ B' ∧ W ∈ B') ∧ ∀ (a b : R), a ∈ V → b ∈ W → a * b ∈ U
⊢ ∀ ib ∈ B',
    ∃ (ia : Set R × Set R),
      (ia.1 ∈ B' ∧ ia.2 ∈ B') ∧ ∀ x ∈ id ia.1 ×ˢ id ia.2, uncurry (fun (x1 x2 : R) ↦ x1 * x2) x ∈ id ib

Tactic:
simpa