awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Algebra.Field (goal)
Goal:
α : Type u_2
𝕜 : Type u_3
f g : α → 𝕜
S : Set α
inst : TopologicalSpace α
inst_1 : TopologicalSpace 𝕜
inst_2 : T1Space 𝕜
inst_3 : Field 𝕜
inst_4 : ContinuousInv₀ 𝕜
inst_5 : ContinuousMul 𝕜
hS : IsPreconnected S
hf : ContinuousOn f S
hg : ContinuousOn g S
hsq : EqOn (HPow.hPow (β := ℕ) f 2) (HPow.hPow (β := ℕ) g 2) S
hg_ne : ∀ {x : α}, x ∈ S → g x ≠ 0
y : α
hy : y ∈ S
hy' : f y = g y
x : α
hx : x ∈ S
h : EqOn f (-g) S
inr :
  ∀ (hy' : Eq.{u_3 + 1} (α := 𝕜) 2 0 ∨ False) (x : α) (hx : x ∈ S) (h : EqOn f (-g) S),
    Eq.{u_3 + 1} (α := 𝕜) 2 0 ∨ False
rw : ∀ (hy' : Eq.{u_3 + 1} (α := 𝕜) 2 0 ∨ False) (x : α) (hx : x ∈ S) (h : EqOn f (-g) S), x ∈ S
⊢ f x = g x
have rw₁ : ∀ (hy' : Eq.{u_3 + 1} (α := 𝕜) 2 0 ∨ g y = 0) (x : α) (hx : x ∈ S) (h : EqOn f (-g) S), y ∈ S
Tactic: rw [h _, Pi.neg_apply, neg_eq_iff_add_eq_zero, ← two_mul, mul_eq_zero,
      (iff_of_eq (iff_false _)).2 (hg_ne _)] at hy' ⊢
Cleared hypotheses: hy', x, hx, h
-- Lean 4 proof step from Mathlib.Topology.Algebra.Field (goal)
Goal:
α : Type u_2
𝕜 : Type u_3
f g : α → 𝕜
S : Set α
inst : TopologicalSpace α
inst_1 : TopologicalSpace 𝕜
inst_2 : T1Space 𝕜
inst_3 : Field 𝕜
inst_4 : ContinuousInv₀ 𝕜
inst_5 : ContinuousMul 𝕜
hS : IsPreconnected S
hf : ContinuousOn f S
hg : ContinuousOn g S
hsq : EqOn (HPow.hPow (β := ℕ) f 2) (HPow.hPow (β := ℕ) g 2) S
hg_ne : ∀ {x : α}, x ∈ S → g x ≠ 0
y : α
hy : y ∈ S
hy' : f y = g y
x : α
hx : x ∈ S
h : EqOn f (-g) S
inr :
  ∀ (hy' : Eq.{u_3 + 1} (α := 𝕜) 2 0 ∨ False) (x : α) (hx : x ∈ S) (h : EqOn f (-g) S),
    Eq.{u_3 + 1} (α := 𝕜) 2 0 ∨ False
rw : ∀ (hy' : Eq.{u_3 + 1} (α := 𝕜) 2 0 ∨ False) (x : α) (hx : x ∈ S) (h : EqOn f (-g) S), x ∈ S
rw₁ : ∀ (hy' : Eq.{u_3 + 1} (α := 𝕜) 2 0 ∨ g y = 0) (x : α) (hx : x ∈ S) (h : EqOn f (-g) S), y ∈ S
⊢ f x = g x
have rw₂ : ∀ (hy' : (-g) y = g y) (x : α) (hx : x ∈ S) (h : EqOn f (-g) S), x ∈ S
Tactic: rw [h _, Pi.neg_apply, neg_eq_iff_add_eq_zero, ← two_mul, mul_eq_zero,
      (iff_of_eq (iff_false _)).2 (hg_ne _)] at hy' ⊢
Cleared hypotheses: hy', x, hx, h
-- Lean 4 proof step from Mathlib.Topology.Algebra.FilterBasis (goal)
Goal:
G : Type u_1
inst : CommGroup G
sets : Set (Set G)
nonempty : sets.Nonempty
inter_sets : ∀ (x y : Set G), x ∈ sets → y ∈ sets → ∃ z ∈ sets, z ⊆ x ∩ y
one : ∀ U ∈ sets, 1 ∈ U
mul : ∀ U ∈ sets, ∃ V ∈ sets, V * V ⊆ U
inv : ∀ U ∈ sets, ∃ V ∈ sets, V ⊆ (fun (x : G) ↦ x⁻¹) ⁻¹' U
x : G
U : Set G
U_in : U ∈ sets
⊢ U ⊆ (fun (x_1 : G) ↦ x * x_1 * x⁻¹) ⁻¹' U
have simp : U ⊆ U
Tactic: simp only [mul_inv_cancel_comm, preimage_id']
-- Lean 4 proof step from Mathlib.Topology.Algebra.FilterBasis (goal)
Goal:
G : Type u
inst : Group G
B : GroupFilterBasis G
x₀ : G
⊢ 𝓝 x₀ = B.N x₀
have hpure : ∀ (a : G) (i : Set G),
  Membership.mem (γ := FilterBasis G) (@toFilterBasis _ inst _) i →
    Membership.mem (γ := Set G) ((fun (y : G) ↦ a * y) '' id i) a
Tactic: apply TopologicalSpace.nhds_mkOfNhds_of_hasBasis (fun x ↦ (FilterBasis.hasBasis _).map _)
-- Lean 4 proof step from Mathlib.Topology.Algebra.FilterBasis (goal)
Goal:
G : Type u
inst : Group G
B : GroupFilterBasis G
x₀ : G
hpure :
  ∀ (a : G) (i : Set G),
    Membership.mem (γ := FilterBasis G) (@toFilterBasis _ inst _) i →
      Membership.mem (γ := Set G) ((fun (y : G) ↦ a * y) '' id i) a
⊢ 𝓝 x₀ = B.N x₀
have hopen : ∀ (a : G) (i : Set G),
  Membership.mem (γ := FilterBasis G) (@toFilterBasis _ inst _) i →
    ∀ᶠ (x : G) in map (fun (y : G) ↦ a * y) (FilterBasis.filter (@toFilterBasis _ inst _)),
      Membership.mem (γ := Filter G) (map (fun (y : G) ↦ x * y) (FilterBasis.filter (@toFilterBasis _ inst _)))
        ((fun (y : G) ↦ a * y) '' id i)
Tactic: apply TopologicalSpace.nhds_mkOfNhds_of_hasBasis (fun x ↦ (FilterBasis.hasBasis _).map _)
-- Lean 4 proof step from Mathlib.Topology.Algebra.FilterBasis (goal)
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
⊢ ∀ᶠ (x : G) in map (fun (y : G) ↦ a * y) (FilterBasis.filter (@toFilterBasis _ inst _)),
    Membership.mem (γ := Filter G) (map (fun (y : G) ↦ x * y) (FilterBasis.filter (@toFilterBasis _ inst _)))
      ((fun (y : G) ↦ a * y) '' id U)
have hopen : ∀ (V : Set G) (V_in : V ∈ B) (hVU : V * V ⊆ U),
  ∀ᶠ (x : G) in map (fun (y : G) ↦ a * y) (FilterBasis.filter (@toFilterBasis _ inst _)),
    Membership.mem (γ := Filter G) (map (fun (y : G) ↦ x * y) (FilterBasis.filter (@toFilterBasis _ inst _)))
      ((fun (y : G) ↦ a * y) '' id U)
Tactic: rcases GroupFilterBasis.mul U_in with ⟨V, V_in, hVU⟩
-- Lean 4 proof step from Mathlib.Topology.Algebra.FilterBasis (goal)
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) in map (fun (y : G) ↦ a * y) (FilterBasis.filter (@toFilterBasis _ inst _)),
    Membership.mem (γ := Filter G) (map (fun (y : G) ↦ x * y) (FilterBasis.filter (@toFilterBasis _ inst _)))
      ((fun (y : G) ↦ a * y) '' id U)
have h : ∀ (a_1 : G),
  Membership.mem (γ := Set G) ((fun (y : G) ↦ a * y) '' V) a_1 →
    Membership.mem (γ := Filter G) (map (fun (y : G) ↦ a_1 * y) (FilterBasis.filter (@toFilterBasis _ inst _)))
      ((fun (y : G) ↦ a * y) '' id U)
Tactic: filter_upwards [image_mem_map (B.mem_filter_of_mem V_in)]
-- Lean 4 proof step from Mathlib.Topology.Algebra.FilterBasis (goal)
Goal:
G : Type u
inst : Group G
B : GroupFilterBasis G
⊢ Eq.{u + 1} (α := Filter G) (𝓝 1) (FilterBasis.filter (@toFilterBasis _ inst _))
have rw : B.N 1 = FilterBasis.filter (@toFilterBasis _ inst _)
Tactic: rw [B.nhds_eq]
-- Lean 4 proof step from Mathlib.Topology.Algebra.FilterBasis (goal)
Goal:
G : Type u
inst : Group G
B : GroupFilterBasis G
⊢ B.N 1 = FilterBasis.filter (@toFilterBasis _ inst _)
have simp : Eq.{u + 1} (α := Filter G) (map (fun (y : G) ↦ y) (FilterBasis.filter (@toFilterBasis _ inst _)))
  (FilterBasis.filter (@toFilterBasis _ inst _))
Tactic: simp only [N, one_mul]
-- Lean 4 proof step from Mathlib.Topology.Algebra.FilterBasis (goal)
Goal:
G : Type u
inst : Group G
B : GroupFilterBasis G
x₀ : G
⊢ (𝓝 x₀).HasBasis (fun (V : Set G) ↦ V ∈ B) fun (V : Set G) ↦ (fun (y : G) ↦ x₀ * y) '' V
have rw : (B.N x₀).HasBasis (fun (V : Set G) ↦ V ∈ B) fun (V : Set G) ↦ (fun (y : G) ↦ x₀ * y) '' V
Tactic: rw [B.nhds_eq]
-- Lean 4 proof step from Mathlib.Topology.Algebra.FilterBasis (goal)
Goal:
G : Type u
inst : Group G
B : GroupFilterBasis G
⊢ HasBasis (𝓝 1) (fun (V : Set G) ↦ V ∈ B) id
have rw : HasBasis (FilterBasis.filter (@toFilterBasis _ inst _)) (fun (V : Set G) ↦ V ∈ B) id
Tactic: rw [B.nhds_one_eq]
-- Lean 4 proof step from Mathlib.Topology.Algebra.FilterBasis (goal)
Goal:
G : Type u
inst : Group G
B : GroupFilterBasis G
U : Set G
hU : U ∈ B
⊢ Membership.mem (γ := Filter G) (𝓝 1) U
have rw : ∃ i ∈ B, id i ⊆ U
Tactic: rw [B.nhds_one_hasBasis.mem_iff]
-- Lean 4 proof step from Mathlib.Topology.Algebra.FilterBasis (hypothesis)
Goal:
G : Type u
inst : Group G
B_1 B : GroupFilterBasis G
this : TopologicalSpace G := B.topology
⊢ IsTopologicalGroup G
have basis : HasBasis (𝓝 1) (fun (V : Set G) ↦ V ∈ B) id
Tactic: have basis := B.nhds_one_hasBasis
-- Lean 4 proof step from Mathlib.Topology.Algebra.FilterBasis (hypothesis)
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
⊢ IsTopologicalGroup G
have 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
Tactic: have basis' := basis.prod basis
-- Lean 4 proof step from Mathlib.Topology.Algebra.FilterBasis (goal)
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
have refine_1 : Tendsto (β := G) (uncurry fun (x1 x2 : G) ↦ x1 * x2) (SProd.sprod (α := Filter G) (β := Filter G) (𝓝 1) (𝓝 1)) (𝓝 1)
Tactic: refine IsTopologicalGroup.of_nhds_one ?_ ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.Topology.Algebra.FilterBasis (goal)
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)
⊢ IsTopologicalGroup G
have refine_2 : Tendsto (β := G) (fun (x : G) ↦ x⁻¹) (𝓝 1) (𝓝 1)
Tactic: refine IsTopologicalGroup.of_nhds_one ?_ ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.Topology.Algebra.FilterBasis (goal)
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)
⊢ IsTopologicalGroup G
have refine_3 : ∀ (x₀ : G), 𝓝 x₀ = map (fun (x : G) ↦ x₀ * x) (𝓝 1)
Tactic: refine IsTopologicalGroup.of_nhds_one ?_ ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.Topology.Algebra.FilterBasis (goal)
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)
⊢ IsTopologicalGroup G
have refine_4 : ∀ (x₀ : G), Tendsto (β := G) (fun (x : G) ↦ x₀ * x * x₀⁻¹) (𝓝 1) (𝓝 1)
Tactic: refine IsTopologicalGroup.of_nhds_one ?_ ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.Topology.Algebra.FilterBasis (goal)
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
⊢ Tendsto (β := G) (uncurry fun (x1 x2 : G) ↦ x1 * x2) (SProd.sprod (α := Filter G) (β := Filter G) (𝓝 1) (𝓝 1)) (𝓝 1)
have 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
Tactic: rw [basis'.tendsto_iff basis]
-- Lean 4 proof step from Mathlib.Topology.Algebra.FilterBasis (goal)
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
⊢ ∀ 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
have refine_1 : ∀ U ∈ B, ∃ (V : Set G) (W : Set G), (V ∈ B ∧ W ∈ B) ∧ ∀ (a b : G), a ∈ V → b ∈ W → a * b ∈ U
Tactic: suffices ∀ U ∈ B, ∃ V W, (V ∈ B ∧ W ∈ B) ∧ ∀ a b, a ∈ V → b ∈ W → a * b ∈ U by simpa
-- Lean 4 proof step from Mathlib.Topology.Algebra.FilterBasis (goal)
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) (W : Set G), (V ∈ B ∧ W ∈ B) ∧ ∀ (a b : G), a ∈ V → b ∈ W → a * b ∈ U
have 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
Tactic: rcases mul U_in with ⟨V, V_in, hV⟩
-- Lean 4 proof step from Mathlib.Topology.Algebra.FilterBasis (goal)
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
have refine_1 : ∀ (a b : G), a ∈ V → b ∈ V → a * b ∈ U
Tactic: refine ⟨V, V, ⟨V_in, V_in⟩, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Algebra.FilterBasis (goal)
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
⊢ Tendsto (β := G) (fun (x : G) ↦ x⁻¹) (𝓝 1) (𝓝 1)
have refine_2 : ∀ ib ∈ B, ∃ ia ∈ B, ∀ x ∈ id ia, x⁻¹ ∈ id ib
Tactic: rw [basis.tendsto_iff basis]
-- Lean 4 proof step from Mathlib.Topology.Algebra.FilterBasis (goal)
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
⊢ 𝓝 x₀ = map (fun (x : G) ↦ x₀ * x) (𝓝 1)
have refine_3 : B.N x₀ = map (fun (x : G) ↦ x₀ * x) (FilterBasis.filter (@toFilterBasis _ inst _))
Tactic: rw [nhds_eq, nhds_one_eq]
-- Lean 4 proof step from Mathlib.Topology.Algebra.FilterBasis (goal)
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
⊢ Tendsto (β := G) (fun (x : G) ↦ x₀ * x * x₀⁻¹) (𝓝 1) (𝓝 1)
have refine_4 : ∀ ib ∈ B, ∃ ia ∈ B, ∀ x ∈ id ia, x₀ * x * x₀⁻¹ ∈ id ib
Tactic: rw [basis.tendsto_iff basis]
-- Lean 4 proof step from Mathlib.Topology.Algebra.FilterBasis (hypothesis)
Goal:
G : Type u
inst : Group G
t : TopologicalSpace G
F : GroupFilterBasis G
hG : F.topology = t
⊢ T2Space G ↔ Eq (α := Set G) (⋂₀ FilterBasis.sets (@toFilterBasis _ inst _)) {1}
have this : IsTopologicalGroup G
Tactic: have : IsTopologicalGroup G := hG ▸ F.isTopologicalGroup
-- Lean 4 proof step from Mathlib.Topology.Algebra.FilterBasis (goal)
Goal:
G : Type u
inst : Group G
t : TopologicalSpace G
F : GroupFilterBasis G
hG : F.topology = t
this : IsTopologicalGroup G
⊢ T2Space G ↔ Eq (α := Set G) (⋂₀ FilterBasis.sets (@toFilterBasis _ inst _)) {1}
have rw : IsClosed[t] {1} ↔ 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]
-- Lean 4 proof step from Mathlib.Topology.Algebra.FilterBasis (goal)
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}
⊢ T2Space G ↔ Eq (α := Set G) (⋂₀ FilterBasis.sets (@toFilterBasis _ inst _)) {1}
have rw₁ : Eq (α := Set G) (closure[t] {1}) {1} ↔ 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]
-- Lean 4 proof step from Mathlib.Topology.Algebra.FilterBasis (goal)
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}
⊢ T2Space G ↔ Eq (α := Set G) (⋂₀ FilterBasis.sets (@toFilterBasis _ inst _)) {1}
have rw₂ : Eq (α := Set G) (ker (𝓝 1)) {1} ↔ 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]
-- Lean 4 proof step from Mathlib.Topology.Algebra.FilterBasis (goal)
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}
⊢ T2Space G ↔ Eq (α := Set G) (⋂₀ FilterBasis.sets (@toFilterBasis _ inst _)) {1}
have rw₃ : Eq (α := Set G) (ker (𝓝 1)) {1} ↔ 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]
-- Lean 4 proof step from Mathlib.Topology.Algebra.FilterBasis (goal)
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}
⊢ T2Space G ↔ Eq (α := Set G) (⋂₀ FilterBasis.sets (@toFilterBasis _ inst _)) {1}
have rw₄ : Eq (α := Set G) (ker (FilterBasis.filter (@toFilterBasis _ inst _))) {1} ↔
  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]
-- Lean 4 proof step from Mathlib.Topology.Algebra.FilterBasis (goal)
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}
⊢ T2Space G ↔ Eq (α := Set G) (⋂₀ FilterBasis.sets (@toFilterBasis _ inst _)) {1}
have rw₅ : Eq (α := Set G) (⋂₀ FilterBasis.sets (@toFilterBasis _ inst _)) {1} ↔
  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]
-- Lean 4 proof step from Mathlib.Topology.Algebra.FilterBasis (goal)
Goal:
G : Type u
inst : Group G
t : TopologicalSpace G
F : GroupFilterBasis G
hG : F.topology = t
⊢ T2Space G ↔ Subset (α := Set G) (⋂₀ FilterBasis.sets (@toFilterBasis _ inst _)) {1}
have rw : Subset (α := Set G) (⋂₀ FilterBasis.sets (@toFilterBasis _ inst _)) {1} →
  Subset (α := Set G) {1} (⋂₀ FilterBasis.sets (@toFilterBasis _ inst _))
Tactic: rw [F.t2Space_iff hG, subset_antisymm_iff, and_iff_left_iff_imp]
-- Lean 4 proof step from Mathlib.Topology.Algebra.FilterBasis (hypothesis)
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
⊢ IsTopologicalRing R
have basis : HasBasis (𝓝 0) (fun (V : Set R) ↦ V ∈ B') id
Tactic: have basis := B'.nhds_zero_hasBasis
-- Lean 4 proof step from Mathlib.Topology.Algebra.FilterBasis (hypothesis)
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
⊢ IsTopologicalRing R
have 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
Tactic: have basis' := basis.prod basis
-- Lean 4 proof step from Mathlib.Topology.Algebra.FilterBasis (hypothesis)
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
⊢ IsTopologicalRing R
have this₁ : IsTopologicalAddGroup R
Tactic: haveI := B'.isTopologicalAddGroup
-- Lean 4 proof step from Mathlib.Topology.Algebra.FilterBasis (goal)
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
⊢ IsTopologicalRing R
have hmul : Tendsto (β := R) (uncurry fun (x1 x2 : R) ↦ x1 * x2) (SProd.sprod (α := Filter R) (β := Filter R) (𝓝 0) (𝓝 0)) (𝓝 0)
Tactic: apply IsTopologicalRing.of_addGroup_of_nhds_zero
-- Lean 4 proof step from Mathlib.Topology.Algebra.FilterBasis (goal)
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)
⊢ IsTopologicalRing R
have hmul_left : ∀ (x₀ : R), Tendsto (β := R) (fun (x : R) ↦ x₀ * x) (𝓝 0) (𝓝 0)
Tactic: apply IsTopologicalRing.of_addGroup_of_nhds_zero