awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Algebra.Nonarchimedean.Bases (goal)
Goal:
ι : Type u_1
R : Type u_2
inst : CommRing R
M : Type u_4
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : TopologicalSpace R
inst_4 : Nonempty ι
B : ι → Submodule R M
hB : SubmodulesBasis B
this : TopologicalSpace M := hB.topology
U : Set M
hU : Membership.mem (γ := Filter M) (𝓝 0) U
⊢ ∃ (V : OpenAddSubgroup M), (↑V : Set M) ⊆ U
have is_nonarchimedean : ∀ (i : ι) (hi : (↑(B i) : Set M) ⊆ U), ∃ (V : OpenAddSubgroup M), (↑V : Set M) ⊆ U
Tactic: obtain ⟨-, ⟨i, rfl⟩, hi : (B i : Set M) ⊆ U⟩ :=
    hB.toModuleFilterBasis.toAddGroupFilterBasis.nhds_zero_hasBasis.mem_iff.mp hU
-- Lean 4 proof step from Mathlib.Topology.Algebra.Nonarchimedean.Bases (goal)
Goal:
ι : Type u_1
R : Type u_2
inst : CommRing R
M : Type u_4
inst_1 : AddCommGroup M
inst_2 : Module R M
BR : RingFilterBasis R
B : ι → Submodule R M
hB : BR.SubmodulesBasis B
x : TopologicalSpace R := BR.topology
this : TopologicalSpace R := BR.topology
m : M
i : ι
⊢ ∀ᶠ (a : R) in 𝓝 0, a • m ∈ B i
have rcases : ∀ (V : Set R) (V_in : V ∈ BR) (hV : V ⊆ (fun (x : R) ↦ x • m) ⁻¹' (↑(B i) : Set M)), ∀ᶠ (a : R) in 𝓝 0, a • m ∈ B i
Tactic: rcases hB.smul m i with ⟨V, V_in, hV⟩
-- Lean 4 proof step from Mathlib.Topology.Algebra.Nonarchimedean.Basic (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : NonarchimedeanGroup G
H : Type u_2
inst_3 : Group H
inst_4 : TopologicalSpace H
inst_5 : IsTopologicalGroup H
f : G →* H
emb : IsOpenEmbedding.{u_1, u_2} (X := G) (Y := H) (⇑f : (a : G) → H)
U : Set H
hU : Membership.mem (γ := Filter H) (𝓝 1) U
⊢ Membership.mem (γ := Filter G) (𝓝 1) ((⇑f : (a : G) → H) ⁻¹' U)
have a : Membership.mem (γ := Filter H) (𝓝 ((f : (a : G) → H) 1) : Filter H) U
Tactic: apply emb.continuous.tendsto
-- Lean 4 proof step from Mathlib.Topology.Algebra.Nonarchimedean.Basic (hypothesis)
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : NonarchimedeanGroup G
K : Type u_3
inst_3 : Group K
inst_4 : TopologicalSpace K
inst_5 : NonarchimedeanGroup K
U : Set (G × K)
hU : Membership.mem (γ := Filter (G × K)) (𝓝 1) U
⊢ ∃ (V : OpenSubgroup G) (W : OpenSubgroup K), (↑V : Set G) ×ˢ (↑W : Set K) ⊆ U
have hU₁ : ∃ (t₁ : Set G),
  Membership.mem (γ := Filter G) (𝓝 1.1) t₁ ∧ ∃ (t₂ : Set K), Membership.mem (γ := Filter K) (𝓝 1.2) t₂ ∧ t₁ ×ˢ t₂ ⊆ U
Tactic: rw [nhds_prod_eq, Filter.mem_prod_iff] at hU
Cleared hypotheses: hU
-- Lean 4 proof step from Mathlib.Topology.Algebra.Nonarchimedean.Basic (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : NonarchimedeanGroup G
K : Type u_3
inst_3 : Group K
inst_4 : TopologicalSpace K
inst_5 : NonarchimedeanGroup K
U : Set (G × K)
hU :
  ∃ (t₁ : Set G),
    Membership.mem (γ := Filter G) (𝓝 1.1) t₁ ∧ ∃ (t₂ : Set K), Membership.mem (γ := Filter K) (𝓝 1.2) t₂ ∧ t₁ ×ˢ t₂ ⊆ U
⊢ ∃ (V : OpenSubgroup G) (W : OpenSubgroup K), (↑V : Set G) ×ˢ (↑W : Set K) ⊆ U
have rcases : ∀ (U₁ : Set G) (hU₁ : Membership.mem (γ := Filter G) (𝓝 1.1) U₁) (U₂ : Set K)
  (hU₂ : Membership.mem (γ := Filter K) (𝓝 1.2) U₂) (h : U₁ ×ˢ U₂ ⊆ U),
  ∃ (V : OpenSubgroup G) (W : OpenSubgroup K), (↑V : Set G) ×ˢ (↑W : Set K) ⊆ U
Tactic: rcases hU with ⟨U₁, hU₁, U₂, hU₂, h⟩
Cleared hypotheses: hU
-- Lean 4 proof step from Mathlib.Topology.Algebra.Nonarchimedean.Basic (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : NonarchimedeanGroup G
K : Type u_3
inst_3 : Group K
inst_4 : TopologicalSpace K
inst_5 : NonarchimedeanGroup K
U : Set (G × K)
U₁ : Set G
hU₁ : Membership.mem (γ := Filter G) (𝓝 1.1) U₁
U₂ : Set K
hU₂ : Membership.mem (γ := Filter K) (𝓝 1.2) U₂
h : U₁ ×ˢ U₂ ⊆ U
⊢ ∃ (V : OpenSubgroup G) (W : OpenSubgroup K), (↑V : Set G) ×ˢ (↑W : Set K) ⊆ U
have obtain : ∀ (V : OpenSubgroup G) (hV : (↑V : Set G) ⊆ U₁),
  ∃ (V : OpenSubgroup G) (W : OpenSubgroup K), (↑V : Set G) ×ˢ (↑W : Set K) ⊆ U
Tactic: obtain ⟨V, hV⟩ := is_nonarchimedean _ hU₁
-- Lean 4 proof step from Mathlib.Topology.Algebra.Nonarchimedean.Basic (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : NonarchimedeanGroup G
K : Type u_3
inst_3 : Group K
inst_4 : TopologicalSpace K
inst_5 : NonarchimedeanGroup K
U : Set (G × K)
U₁ : Set G
hU₁ : Membership.mem (γ := Filter G) (𝓝 1.1) U₁
U₂ : Set K
hU₂ : Membership.mem (γ := Filter K) (𝓝 1.2) U₂
h : U₁ ×ˢ U₂ ⊆ U
V : OpenSubgroup G
hV : (↑V : Set G) ⊆ U₁
⊢ ∃ (V : OpenSubgroup G) (W : OpenSubgroup K), (↑V : Set G) ×ˢ (↑W : Set K) ⊆ U
have obtain : ∀ (W : OpenSubgroup K) (hW : (↑W : Set K) ⊆ U₂),
  ∃ (V : OpenSubgroup G) (W : OpenSubgroup K), (↑V : Set G) ×ˢ (↑W : Set K) ⊆ U
Tactic: obtain ⟨W, hW⟩ := is_nonarchimedean _ hU₂
-- Lean 4 proof step from Mathlib.Topology.Algebra.Nonarchimedean.Basic (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : NonarchimedeanGroup G
K : Type u_3
inst_3 : Group K
inst_4 : TopologicalSpace K
inst_5 : NonarchimedeanGroup K
U : Set (G × K)
U₁ : Set G
hU₁ : Membership.mem (γ := Filter G) (𝓝 1.1) U₁
U₂ : Set K
hU₂ : Membership.mem (γ := Filter K) (𝓝 1.2) U₂
h : U₁ ×ˢ U₂ ⊆ U
V : OpenSubgroup G
hV : (↑V : Set G) ⊆ U₁
W : OpenSubgroup K
hW : (↑W : Set K) ⊆ U₂
⊢ ∃ (V : OpenSubgroup G) (W : OpenSubgroup K), (↑V : Set G) ×ˢ (↑W : Set K) ⊆ U
have h₁ : ∃ (W : OpenSubgroup K), (↑V : Set G) ×ˢ (↑W : Set K) ⊆ U
Tactic: use V
-- Lean 4 proof step from Mathlib.Topology.Algebra.Nonarchimedean.Basic (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : NonarchimedeanGroup G
U : Set (G × G)
hU : Membership.mem (γ := Filter (G × G)) (𝓝 1) U
V W : OpenSubgroup G
h : (↑V : Set G) ×ˢ (↑W : Set G) ⊆ U
⊢ (↑(V ⊓ W) : Set G) ×ˢ (↑(V ⊓ W) : Set G) ⊆ U
have refine_1 : (↑(V ⊓ W) : Set G) ⊆ (↑V : Set G)
Tactic: refine Set.Subset.trans (Set.prod_mono ?_ ?_) ‹_›
-- Lean 4 proof step from Mathlib.Topology.Algebra.Nonarchimedean.Basic (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : NonarchimedeanGroup G
U : Set (G × G)
hU : Membership.mem (γ := Filter (G × G)) (𝓝 1) U
V W : OpenSubgroup G
h : (↑V : Set G) ×ˢ (↑W : Set G) ⊆ U
refine_1 : (↑(V ⊓ W) : Set G) ⊆ (↑V : Set G)
⊢ (↑(V ⊓ W) : Set G) ×ˢ (↑(V ⊓ W) : Set G) ⊆ U
have refine_2 : (↑(V ⊓ W) : Set G) ⊆ (↑W : Set G)
Tactic: refine Set.Subset.trans (Set.prod_mono ?_ ?_) ‹_›
-- Lean 4 proof step from Mathlib.Topology.Algebra.Nonarchimedean.Basic (goal)
Goal:
R : Type u_1
inst : Ring R
inst_1 : TopologicalSpace R
inst_2 : NonarchimedeanRing R
U : OpenAddSubgroup R
⊢ ∃ (V : OpenAddSubgroup R), (↑V : Set R) * (↑V : Set R) ⊆ (↑U : Set R)
have let : ∀ (V : OpenAddSubgroup R) (H : (↑V : Set R) ×ˢ (↑V : Set R) ⊆ (fun (p : R × R) ↦ p.1 * p.2) ⁻¹' (↑U : Set R)),
  ∃ (V : OpenAddSubgroup R), (↑V : Set R) * (↑V : Set R) ⊆ (↑U : Set R)
Tactic: let ⟨V, H⟩ := prod_self_subset <| (U.isOpen.preimage continuous_mul).mem_nhds <| by
    simpa only [Set.mem_preimage, Prod.snd_zero, mul_zero] using U.zero_mem
-- Lean 4 proof step from Mathlib.Topology.Algebra.Nonarchimedean.Basic (goal)
Goal:
R : Type u_1
inst : Ring R
inst_1 : TopologicalSpace R
inst_2 : NonarchimedeanRing R
U V : OpenAddSubgroup R
H : (↑V : Set R) ×ˢ (↑V : Set R) ⊆ (fun (p : R × R) ↦ p.1 * p.2) ⁻¹' (↑U : Set R)
⊢ ∃ (V : OpenAddSubgroup R), (↑V : Set R) * (↑V : Set R) ⊆ (↑U : Set R)
have h : (↑V : Set R) * (↑V : Set R) ⊆ (↑U : Set R)
Tactic: use V
-- Lean 4 proof step from Mathlib.Topology.Algebra.Nonarchimedean.Basic (hypothesis)
Goal:
R : Type u_1
inst : Ring R
inst_1 : TopologicalSpace R
inst_2 : NonarchimedeanRing R
U V : OpenAddSubgroup R
H : (↑V : Set R) ×ˢ (↑V : Set R) ⊆ (fun (p : R × R) ↦ p.1 * p.2) ⁻¹' (↑U : Set R)
v a : R
ha : a ∈ (↑V : Set R)
b : R
hb : b ∈ (↑V : Set R)
hv : (fun (x1 x2 : R) ↦ x1 * x2) a b = v
⊢ v ∈ (↑U : Set R)
have hy : Membership.mem (γ := Set (R × R)) ((fun (p : R × R) ↦ p.1 * p.2) ⁻¹' (↑U : Set R)) (a, b)
Tactic: have hy := H (Set.mk_mem_prod ha hb)
-- Lean 4 proof step from Mathlib.Topology.Algebra.Nonarchimedean.Basic (hypothesis)
Goal:
R : Type u_1
inst : Ring R
inst_1 : TopologicalSpace R
inst_2 : NonarchimedeanRing R
U V : OpenAddSubgroup R
H : (↑V : Set R) ×ˢ (↑V : Set R) ⊆ (fun (p : R × R) ↦ p.1 * p.2) ⁻¹' (↑U : Set R)
v a : R
ha : a ∈ (↑V : Set R)
b : R
hb : b ∈ (↑V : Set R)
hv : (fun (x1 x2 : R) ↦ x1 * x2) a b = v
hy : Membership.mem (γ := Set (R × R)) ((fun (p : R × R) ↦ p.1 * p.2) ⁻¹' (↑U : Set R)) (a, b)
⊢ v ∈ (↑U : Set R)
have hy₁ : v ∈ U
Tactic: simp only [Set.mem_preimage, SetLike.mem_coe, hv] at hy
Cleared hypotheses: hy
-- Lean 4 proof step from Mathlib.Topology.Algebra.Nonarchimedean.Completion (goal)
Goal:
G : Type u_1
inst : AddGroup G
inst_1 : UniformSpace G
inst_2 : IsUniformAddGroup G
inst_3 : NonarchimedeanAddGroup G
U : Set (Completion G)
hU : Membership.mem (γ := Filter (Completion G)) (𝓝 0) U
⊢ ∃ (V : OpenAddSubgroup (Completion G)), (↑V : Set (Completion G)) ⊆ U
have obtain : ∀ (C : Set (Completion G)) (C_subset_U : id C ⊆ U) (hC : Membership.mem (γ := Filter (Completion G)) (𝓝 0) C)
  (C_closed : IsClosed C), ∃ (V : OpenAddSubgroup (Completion G)), (↑V : Set (Completion G)) ⊆ U
Tactic: obtain ⟨C, ⟨hC, C_closed⟩, C_subset_U⟩ := (closed_nhds_basis 0).mem_iff.mp hU
-- Lean 4 proof step from Mathlib.Topology.Algebra.Nonarchimedean.Completion (hypothesis)
Goal:
G : Type u_1
inst : AddGroup G
inst_1 : UniformSpace G
inst_2 : IsUniformAddGroup G
inst_3 : NonarchimedeanAddGroup G
U : Set (Completion G)
hU : Membership.mem (γ := Filter (Completion G)) (𝓝 0) U
C : Set (Completion G)
C_subset_U : id C ⊆ U
hC : Membership.mem (γ := Filter (Completion G)) (𝓝 0) C
C_closed : IsClosed C
⊢ ∃ (V : OpenAddSubgroup (Completion G)), (↑V : Set (Completion G)) ⊆ U
have this : Membership.mem (γ := Filter G) (𝓝 0) ((⇑toCompl : (a : G) → Completion G) ⁻¹' C)
Tactic: have : toCompl ⁻¹' C ∈ 𝓝 0 :=
      continuous_toCompl.continuousAt.preimage_mem_nhds (by rwa [map_zero])
-- Lean 4 proof step from Mathlib.Topology.Algebra.Nonarchimedean.Completion (goal)
Goal:
G : Type u_1
inst : AddGroup G
inst_1 : UniformSpace G
inst_2 : IsUniformAddGroup G
inst_3 : NonarchimedeanAddGroup G
U : Set (Completion G)
hU : Membership.mem (γ := Filter (Completion G)) (𝓝 0) U
C : Set (Completion G)
C_subset_U : id C ⊆ U
hC : Membership.mem (γ := Filter (Completion G)) (𝓝 0) C
C_closed : IsClosed C
this : Membership.mem (γ := Filter G) (𝓝 0) ((⇑toCompl : (a : G) → Completion G) ⁻¹' C)
⊢ ∃ (V : OpenAddSubgroup (Completion G)), (↑V : Set (Completion G)) ⊆ U
have obtain : ∀ (W : OpenAddSubgroup G) (hCW : (↑W : Set G) ⊆ (⇑toCompl : (a : G) → Completion G) ⁻¹' C),
  ∃ (V : OpenAddSubgroup (Completion G)), (↑V : Set (Completion G)) ⊆ U
Tactic: obtain ⟨W, hCW⟩ := NonarchimedeanAddGroup.is_nonarchimedean (toCompl ⁻¹' C) this
-- Lean 4 proof step from Mathlib.Topology.Algebra.Nonarchimedean.Completion (goal)
Goal:
G : Type u_1
inst : AddGroup G
inst_1 : UniformSpace G
inst_2 : IsUniformAddGroup G
inst_3 : NonarchimedeanAddGroup G
U : Set (Completion G)
hU : Membership.mem (γ := Filter (Completion G)) (𝓝 0) U
C : Set (Completion G)
C_subset_U : id C ⊆ U
hC : Membership.mem (γ := Filter (Completion G)) (𝓝 0) C
C_closed : IsClosed C
this : Membership.mem (γ := Filter G) (𝓝 0) ((⇑toCompl : (a : G) → Completion G) ⁻¹' C)
W : OpenAddSubgroup G
hCW : (↑W : Set G) ⊆ (⇑toCompl : (a : G) → Completion G) ⁻¹' C
V : Set (Completion G) := (↑(topologicalClosure (map toCompl (↑W : AddSubgroup G))) : Set (Completion G))
⊢ IsOpen V
have hg : Membership.mem (γ := Filter (Completion G)) (𝓝 0)
  (↑(topologicalClosure (map toCompl (↑W : AddSubgroup G))) : Set (Completion G))
Tactic: apply isOpen_of_mem_nhds (g := 0)
-- Lean 4 proof step from Mathlib.Topology.Algebra.Nonarchimedean.Completion (goal)
Goal:
G : Type u_1
inst : AddGroup G
inst_1 : UniformSpace G
inst_2 : IsUniformAddGroup G
inst_3 : NonarchimedeanAddGroup G
U : Set (Completion G)
hU : Membership.mem (γ := Filter (Completion G)) (𝓝 0) U
C : Set (Completion G)
C_subset_U : id C ⊆ U
hC : Membership.mem (γ := Filter (Completion G)) (𝓝 0) C
C_closed : IsClosed C
this : Membership.mem (γ := Filter G) (𝓝 0) ((⇑toCompl : (a : G) → Completion G) ⁻¹' C)
W : OpenAddSubgroup G
hCW : (↑W : Set G) ⊆ (⇑toCompl : (a : G) → Completion G) ⁻¹' C
V : Set (Completion G) := (↑(topologicalClosure (map toCompl (↑W : AddSubgroup G))) : Set (Completion G))
⊢ Membership.mem (γ := Filter (Completion G)) (𝓝 0)
    (↑(topologicalClosure (map toCompl (↑W : AddSubgroup G))) : Set (Completion G))
have hg : Membership.mem (γ := Filter G) (𝓝 0) (↑(↑W : AddSubgroup G) : Set G)
Tactic: apply (isDenseInducing_toCompl _).closure_image_mem_nhds
-- Lean 4 proof step from Mathlib.Topology.Algebra.Nonarchimedean.Completion (hypothesis)
Goal:
G : Type u_1
inst : AddGroup G
inst_1 : UniformSpace G
inst_2 : IsUniformAddGroup G
inst_3 : NonarchimedeanAddGroup G
U : Set (Completion G)
hU : Membership.mem (γ := Filter (Completion G)) (𝓝 0) U
C : Set (Completion G)
C_subset_U : id C ⊆ U
hC : Membership.mem (γ := Filter (Completion G)) (𝓝 0) C
C_closed : IsClosed C
this : Membership.mem (γ := Filter G) (𝓝 0) ((⇑toCompl : (a : G) → Completion G) ⁻¹' C)
W : OpenAddSubgroup G
hCW : (↑W : Set G) ⊆ (⇑toCompl : (a : G) → Completion G) ⁻¹' C
V : Set (Completion G) := (↑(topologicalClosure (map toCompl (↑W : AddSubgroup G))) : Set (Completion G))
⊢ ∃ (V : OpenAddSubgroup (Completion G)), (↑V : Set (Completion G)) ⊆ U
have this₁ : IsOpen V
Tactic: have : IsOpen V := by
      /- Since `V` is a subgroup of `Completion G`, it suffices to show that it is a neighborhood of
      `0` in `Completion G`. This follows from the fact that `toCompl : G → Completion G` is dense
      inducing and `W` is a neighborhood of `0` in `G`. -/
      apply isOpen_of_mem_nhds (g := 0)
      apply (isDenseInducing_toCompl _).closure_image_mem_nhds
      exact mem_nhds_zero W
-- Lean 4 proof step from Mathlib.Topology.Algebra.Nonarchimedean.Completion (goal)
Goal:
G : Type u_1
inst : AddGroup G
inst_1 : UniformSpace G
inst_2 : IsUniformAddGroup G
inst_3 : NonarchimedeanAddGroup G
U : Set (Completion G)
hU : Membership.mem (γ := Filter (Completion G)) (𝓝 0) U
C : Set (Completion G)
C_subset_U : id C ⊆ U
hC : Membership.mem (γ := Filter (Completion G)) (𝓝 0) C
C_closed : IsClosed C
this_1 : Membership.mem (γ := Filter G) (𝓝 0) ((⇑toCompl : (a : G) → Completion G) ⁻¹' C)
W : OpenAddSubgroup G
hCW : (↑W : Set G) ⊆ (⇑toCompl : (a : G) → Completion G) ⁻¹' C
V : Set (Completion G) := (↑(topologicalClosure (map toCompl (↑W : AddSubgroup G))) : Set (Completion G))
this : IsOpen V
⊢ ∃ (V : OpenAddSubgroup (Completion G)), (↑V : Set (Completion G)) ⊆ U
have h : (↑{ toAddSubgroup := topologicalClosure (map toCompl (↑W : AddSubgroup G)), isOpen' := this :
        OpenAddSubgroup (Completion G) } :
    Set (Completion G)) ⊆
  U
Tactic: use ⟨_, this⟩
-- Lean 4 proof step from Mathlib.Topology.Algebra.Nonarchimedean.Completion (goal)
Goal:
G : Type u_1
inst : AddGroup G
inst_1 : UniformSpace G
inst_2 : IsUniformAddGroup G
inst_3 : NonarchimedeanAddGroup G
U : Set (Completion G)
hU : Membership.mem (γ := Filter (Completion G)) (𝓝 0) U
C : Set (Completion G)
C_subset_U : id C ⊆ U
hC : Membership.mem (γ := Filter (Completion G)) (𝓝 0) C
C_closed : IsClosed C
this_1 : Membership.mem (γ := Filter G) (𝓝 0) ((⇑toCompl : (a : G) → Completion G) ⁻¹' C)
W : OpenAddSubgroup G
hCW : (↑W : Set G) ⊆ (⇑toCompl : (a : G) → Completion G) ⁻¹' C
V : Set (Completion G) := (↑(topologicalClosure (map toCompl (↑W : AddSubgroup G))) : Set (Completion G))
this : IsOpen V
⊢ (↑{ toAddSubgroup := topologicalClosure (map toCompl (↑W : AddSubgroup G)), isOpen' := this :
          OpenAddSubgroup (Completion G) } :
      Set (Completion G)) ⊆
    U
have h : V ⊆ C
Tactic: suffices V ⊆ C from this.trans C_subset_U
-- Lean 4 proof step from Mathlib.Topology.Algebra.Nonarchimedean.TotallyDisconnected (goal)
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : NonarchimedeanGroup G
inst_3 : T2Space G
a b : G
h : a ≠ b
⊢ ∃ (V : OpenSubgroup G), Disjoint (a • (↑V : Set G)) (b • (↑V : Set G))
have obtain : ∀ (u v : Set G),
  IsOpen u →
    ∀ (open_v : IsOpen v) (mem_u : a⁻¹ * b ∈ u) (mem_v : 1 ∈ v) (dis : Disjoint u v),
      ∃ (V : OpenSubgroup G), Disjoint (a • (↑V : Set G)) (b • (↑V : Set G))
Tactic: obtain ⟨u, v, _, open_v, mem_u, mem_v, dis⟩ := t2_separation (h ∘ inv_mul_eq_one.mp)
-- Lean 4 proof step from Mathlib.Topology.Algebra.Nonarchimedean.TotallyDisconnected (goal)
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : NonarchimedeanGroup G
inst_3 : T2Space G
a b : G
h : a ≠ b
u v : Set G
left : IsOpen u
open_v : IsOpen v
mem_u : a⁻¹ * b ∈ u
mem_v : 1 ∈ v
dis : Disjoint u v
⊢ ∃ (V : OpenSubgroup G), Disjoint (a • (↑V : Set G)) (b • (↑V : Set G))
have obtain : ∀ (V : OpenSubgroup G) (hV : (↑V : Set G) ⊆ v), ∃ (V : OpenSubgroup G), Disjoint (a • (↑V : Set G)) (b • (↑V : Set G))
Tactic: obtain ⟨V, hV⟩ := is_nonarchimedean v (open_v.mem_nhds mem_v)
-- Lean 4 proof step from Mathlib.Topology.Algebra.Nonarchimedean.TotallyDisconnected (goal)
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : NonarchimedeanGroup G
inst_3 : T2Space G
a b : G
h : a ≠ b
u v : Set G
left : IsOpen u
open_v : IsOpen v
mem_u : a⁻¹ * b ∈ u
mem_v : 1 ∈ v
dis : Disjoint u v
V : OpenSubgroup G
hV : (↑V : Set G) ⊆ v
⊢ ∃ (V : OpenSubgroup G), Disjoint (a • (↑V : Set G)) (b • (↑V : Set G))
have h₁ : Disjoint (a • (↑V : Set G)) (b • (↑V : Set G))
Tactic: use V
-- Lean 4 proof step from Mathlib.Topology.Algebra.Nonarchimedean.TotallyDisconnected (goal)
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : NonarchimedeanGroup G
inst_3 : T2Space G
a b : G
h : a ≠ b
u v : Set G
left : IsOpen u
open_v : IsOpen v
mem_u : a⁻¹ * b ∈ u
mem_v : 1 ∈ v
dis : Disjoint u v
V : OpenSubgroup G
hV : (↑V : Set G) ⊆ v
⊢ Disjoint (a • (↑V : Set G)) (b • (↑V : Set G))
have h₁ : ∀ ⦃x : Set G⦄, x ⊆ a • (↑V : Set G) → x ⊆ b • (↑V : Set G) → x = ∅
Tactic: simp only [Disjoint, Set.le_eq_subset, Set.bot_eq_empty, Set.subset_empty_iff]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Nonarchimedean.TotallyDisconnected (goal)
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : NonarchimedeanGroup G
inst_3 : T2Space G
a b : G
h : a ≠ b
u v : Set G
left : IsOpen u
open_v : IsOpen v
mem_u : a⁻¹ * b ∈ u
mem_v : 1 ∈ v
dis : Disjoint u v
V : OpenSubgroup G
hV : (↑V : Set G) ⊆ v
x : Set G
mem_aV : x ⊆ a • (↑V : Set G)
mem_bV : x ⊆ b • (↑V : Set G)
⊢ x = ∅
have h₁ : ∀ (s : G) (hs : s ∈ x), False
Tactic: by_contra! ⟨s, hs⟩
-- Lean 4 proof step from Mathlib.Topology.Algebra.Nonarchimedean.TotallyDisconnected (hypothesis)
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : NonarchimedeanGroup G
inst_3 : T2Space G
a b : G
h : a ≠ b
u v : Set G
left : IsOpen u
open_v : IsOpen v
mem_u : a⁻¹ * b ∈ u
mem_v : 1 ∈ v
dis : Disjoint u v
V : OpenSubgroup G
hV : (↑V : Set G) ⊆ v
x : Set G
mem_aV : x ⊆ a • (↑V : Set G)
mem_bV : x ⊆ b • (↑V : Set G)
s : G
hs : s ∈ x
⊢ False
have hsa : s ∈ a • (↑V : Set G)
Tactic: have hsa : s ∈ a • (V : Set G) := mem_aV hs
-- Lean 4 proof step from Mathlib.Topology.Algebra.Nonarchimedean.TotallyDisconnected (hypothesis)
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : NonarchimedeanGroup G
inst_3 : T2Space G
a b : G
h : a ≠ b
u v : Set G
left : IsOpen u
open_v : IsOpen v
mem_u : a⁻¹ * b ∈ u
mem_v : 1 ∈ v
dis : Disjoint u v
V : OpenSubgroup G
hV : (↑V : Set G) ⊆ v
x : Set G
mem_aV : x ⊆ a • (↑V : Set G)
mem_bV : x ⊆ b • (↑V : Set G)
s : G
hs : s ∈ x
hsa : s ∈ a • (↑V : Set G)
⊢ False
have hsb : s ∈ b • (↑V : Set G)
Tactic: have hsb : s ∈ b • (V : Set G) := mem_bV hs
-- Lean 4 proof step from Mathlib.Topology.Algebra.Nonarchimedean.TotallyDisconnected (hypothesis)
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : NonarchimedeanGroup G
inst_3 : T2Space G
a b : G
h : a ≠ b
u v : Set G
left : IsOpen u
open_v : IsOpen v
mem_u : a⁻¹ * b ∈ u
mem_v : 1 ∈ v
dis : Disjoint u v
V : OpenSubgroup G
hV : (↑V : Set G) ⊆ v
x : Set G
mem_aV : x ⊆ a • (↑V : Set G)
mem_bV : x ⊆ b • (↑V : Set G)
s : G
hs : s ∈ x
hsa : s ∈ a • (↑V : Set G)
hsb : s ∈ b • (↑V : Set G)
⊢ False
have hsa₁ : a⁻¹ * s ∈ (↑V : Set G)
Tactic: rw [mem_leftCoset_iff] at hsa hsb
Cleared hypotheses: hsa, hsb
-- Lean 4 proof step from Mathlib.Topology.Algebra.Nonarchimedean.TotallyDisconnected (hypothesis)
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : NonarchimedeanGroup G
inst_3 : T2Space G
a b : G
h : a ≠ b
u v : Set G
left : IsOpen u
open_v : IsOpen v
mem_u : a⁻¹ * b ∈ u
mem_v : 1 ∈ v
dis : Disjoint u v
V : OpenSubgroup G
hV : (↑V : Set G) ⊆ v
x : Set G
mem_aV : x ⊆ a • (↑V : Set G)
mem_bV : x ⊆ b • (↑V : Set G)
s : G
hs : s ∈ x
hsa : s ∈ a • (↑V : Set G)
hsb : s ∈ b • (↑V : Set G)
hsa₁ : a⁻¹ * s ∈ (↑V : Set G)
⊢ False
have hsb₁ : b⁻¹ * s ∈ (↑V : Set G)
Tactic: rw [mem_leftCoset_iff] at hsa hsb
Cleared hypotheses: hsa, hsb
-- Lean 4 proof step from Mathlib.Topology.Algebra.Nonarchimedean.TotallyDisconnected (goal)
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : NonarchimedeanGroup G
inst_3 : T2Space G
a b : G
h : a ≠ b
u v : Set G
left : IsOpen u
open_v : IsOpen v
mem_u : a⁻¹ * b ∈ u
mem_v : 1 ∈ v
dis : Disjoint u v
V : OpenSubgroup G
hV : (↑V : Set G) ⊆ v
x : Set G
mem_aV : x ⊆ a • (↑V : Set G)
mem_bV : x ⊆ b • (↑V : Set G)
s : G
hs : s ∈ x
hsa : a⁻¹ * s ∈ (↑V : Set G)
hsb : b⁻¹ * s ∈ (↑V : Set G)
⊢ False
have h₁ : a⁻¹ * b ∈ (↑V : Set G)
Tactic: refine dis.subset_compl_right mem_u (hV ?_)
-- Lean 4 proof step from Mathlib.Topology.Algebra.Nonarchimedean.TotallyDisconnected (goal)
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : NonarchimedeanGroup G
inst_3 : T2Space G
x : G
h : Membership.mem (γ := Set G) Set.univ x
y : G
h_1 : Membership.mem (γ := Set G) Set.univ y
hxy : x ≠ y
⊢ (fun (x y : G) ↦ ∃ (u : Set G) (v : Set G), IsOpen u ∧ IsOpen v ∧ x ∈ u ∧ y ∈ v ∧ Set.univ ⊆ u ∪ v ∧ Disjoint u v) x y
have obtain : ∀ (V : OpenSubgroup G) (dxy : Disjoint (x • (↑V : Set G)) (y • (↑V : Set G))),
  ∃ (u : Set G) (v : Set G), IsOpen u ∧ IsOpen v ∧ x ∈ u ∧ y ∈ v ∧ Set.univ ⊆ u ∪ v ∧ Disjoint u v
Tactic: obtain ⟨V, dxy⟩ := exists_openSubgroup_separating hxy
-- Lean 4 proof step from Mathlib.Topology.Algebra.OpenSubgroup (hypothesis)
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : SeparatelyContinuousMul G
U : OpenSubgroup G
⊢ IsClosed[inst_1] (↑U : Set G)
have this : DiscreteTopology.{u_1} (G ⧸ (↑U : Subgroup G))
Tactic: have := QuotientGroup.discreteTopology U.isOpen
-- Lean 4 proof step from Mathlib.Topology.Algebra.OpenSubgroup (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : SeparatelyContinuousMul G
H : Subgroup G
g : G
hg : (↑H : Set G) ∈ 𝓝 g
⊢ IsOpen[inst_1] (↑H : Set G)
have refine : ∀ (x : G) (hx : x ∈ (↑H : Set G)), (↑H : Set G) ∈ 𝓝 x
Tactic: refine isOpen_iff_mem_nhds.2 fun x hx ↦ ?_
-- Lean 4 proof step from Mathlib.Topology.Algebra.OpenSubgroup (hypothesis)
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : SeparatelyContinuousMul G
H : Subgroup G
g : G
hg : (↑H : Set G) ∈ 𝓝 g
x : G
hx : x ∈ (↑H : Set G)
⊢ (↑H : Set G) ∈ 𝓝 x
have hg' : g ∈ H
Tactic: have hg' : g ∈ H := SetLike.mem_coe.1 (mem_of_mem_nhds hg)
-- Lean 4 proof step from Mathlib.Topology.Algebra.OpenSubgroup (hypothesis)
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : SeparatelyContinuousMul G
H : Subgroup G
g : G
hg : (↑H : Set G) ∈ 𝓝 g
x : G
hx : x ∈ (↑H : Set G)
hg' : g ∈ H
⊢ (↑H : Set G) ∈ 𝓝 x
have this : Filter.Tendsto (fun (y : G) ↦ y * (x⁻¹ * g)) (𝓝 x) (𝓝 g)
Tactic: have : Filter.Tendsto (fun y ↦ y * (x⁻¹ * g)) (𝓝 x) (𝓝 g) :=
    (continuous_id.mul_const _).tendsto' _ _ (mul_inv_cancel_left _ _)
-- Lean 4 proof step from Mathlib.Topology.Algebra.OpenSubgroup (goal)
Goal:
G : Type u
inst : Group G
inst_1 : TopologicalSpace G
A B : OpenNormalSubgroup G
h :
  Eq.{u + 1} (α := Subgroup G) ((fun (H : OpenNormalSubgroup G) ↦ (↑H.toOpenSubgroup : Subgroup G)) A)
    ((fun (H : OpenNormalSubgroup G) ↦ (↑H.toOpenSubgroup : Subgroup G)) B)
⊢ A = B
have carrier : ∀ (x : G), x ∈ (↑A.toOpenSubgroup : Subgroup G).carrier ↔ x ∈ (↑B.toOpenSubgroup : Subgroup G).carrier
Tactic: ext