awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Algebra.Nonarchimedean.Bases
Goal:
ι : Type u_1
R : Type u_2
A : Type u_3
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
M : Type u_4
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : TopologicalSpace R
inst_6 : Nonempty ι
B : ι → Submodule R M
hB : SubmodulesBasis B
i : ι
x : TopologicalSpace M := hB.topology
this : TopologicalSpace M := hB.topology
a : M
a_in : a ∈ (B i).toAddSubgroup.carrier
b : M
b_in : b ∈ (↑(B i) : Set M)
⊢ (fun (y : M) ↦ a + y) b ∈ (B i).toAddSubgroup.carrier

Tactic:
(B i).add_mem a_in b_in

Premises used: Set.Mem, Submodule.add_mem
-- Module: Mathlib.Topology.Algebra.Nonarchimedean.Bases
Goal:
ι : Type u_1
R : Type u_2
A : Type u_3
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
M : Type u_4
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : TopologicalSpace R
inst_6 : Nonempty ι
B : ι → Submodule R M
hB : SubmodulesBasis B
i : ι
x : TopologicalSpace M := hB.topology
this : TopologicalSpace M := hB.topology
a : M
a_in : a ∈ (B i).toAddSubgroup.carrier
b : M
b_in : b ∈ (↑(B i) : Set M)
⊢ (fun (y : M) ↦ a + y) b ∈ (B i).toAddSubgroup.carrier

Tactic:
exact (B i).add_mem a_in b_in

Premises used: Submodule.add_mem
-- Module: Mathlib.Topology.Algebra.Nonarchimedean.Bases
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
is_nonarchimedean : ∀ (U : Set M), Membership.mem (γ := Filter M) (𝓝 0) U → ∃ (V : OpenAddSubgroup M), (↑V : Set M) ⊆ U
⊢ NonarchimedeanAddGroup M

Tactic:
constructor
-- Module: Mathlib.Topology.Algebra.Nonarchimedean.Bases
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
is_nonarchimedean : ∀ (i : ι) (hi : (↑(B i) : Set M) ⊆ U), ∃ (V : OpenAddSubgroup M), (↑V : 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

Premises used: Filter.HasBasis.mem_iff, ModuleFilterBasis.toAddGroupFilterBasis, AddGroupFilterBasis.nhds_zero_hasBasis, SubmodulesBasis.toModuleFilterBasis, Iff.mp, rfl
-- Module: Mathlib.Topology.Algebra.Nonarchimedean.Bases
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
i : ι
hi : (↑(B i) : Set M) ⊆ U
⊢ ∃ (V : OpenAddSubgroup M), (↑V : Set M) ⊆ U

Tactic:
⟨hB.openAddSubgroup i, hi⟩

Premises used: SubmodulesBasis.openAddSubgroup, Exists.intro
-- Module: Mathlib.Topology.Algebra.Nonarchimedean.Bases
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
i : ι
hi : (↑(B i) : Set M) ⊆ U
⊢ ∃ (V : OpenAddSubgroup M), (↑V : Set M) ⊆ U

Tactic:
exact ⟨hB.openAddSubgroup i, hi⟩
-- Module: Mathlib.Topology.Algebra.Nonarchimedean.Bases
Goal:
ι : Type u_1
R : Type u_2
A : Type u_3
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : TopologicalSpace R
B : ι → Submodule R A
hB : SubmodulesRingBasis B
hsmul : ∀ (m : A) (i : ι), ∀ᶠ (a : R) in 𝓝 0, a • m ∈ B i
⊢ SubmodulesBasis.{u_1, u_2, u_3} (ι := ι) (R := R) (M := A) B

Tactic:
{ inter := hB.inter
    smul := hsmul }

Premises used: SubmodulesBasis.mk, SubmodulesRingBasis.inter
-- Module: Mathlib.Topology.Algebra.Nonarchimedean.Bases
Goal:
ι : Type u_1
R : Type u_2
A : Type u_3
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
M : Type u_4
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : TopologicalSpace R
B : ι → Submodule R A
hB : SubmodulesRingBasis B
hsmul : ∀ (m : A) (i : ι), ∀ᶠ (a : R) in 𝓝 0, a • m ∈ B i
inst_6 : Nonempty ι
⊢ hB.topology = ⋯.topology

Tactic:
rfl

Premises used: setOf, rfl
-- Module: Mathlib.Topology.Algebra.Nonarchimedean.Bases
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 : ι
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
⊢ ∀ᶠ (a : R) in 𝓝 0, a • m ∈ B i

Tactic:
rcases hB.smul m i with ⟨V, V_in, hV⟩

Premises used: RingFilterBasis.SubmodulesBasis.smul
-- Module: Mathlib.Topology.Algebra.Nonarchimedean.Bases
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 : ι
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:
mem_of_superset (BR.toAddGroupFilterBasis.mem_nhds_zero V_in) hV

Premises used: Filter.Eventually, AddGroupFilterBasis.mem_nhds_zero, RingFilterBasis.toAddGroupFilterBasis, Filter.mem_of_superset
-- Module: Mathlib.Topology.Algebra.Nonarchimedean.Bases
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 : ι
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:
exact mem_of_superset (BR.toAddGroupFilterBasis.mem_nhds_zero V_in) hV

Premises used: AddGroupFilterBasis.mem_nhds_zero, RingFilterBasis.toAddGroupFilterBasis, Filter.mem_of_superset
-- Module: Mathlib.Topology.Algebra.Nonarchimedean.Basic
Goal:
R : Type u_1
inst : Ring R
inst_1 : TopologicalSpace R
t : NonarchimedeanRing R
⊢ NonarchimedeanAddGroup R

Tactic:
{ t with }

Premises used: NonarchimedeanAddGroup.mk, NonarchimedeanRing.is_nonarchimedean
-- Module: Mathlib.Topology.Algebra.Nonarchimedean.Basic
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
a : Membership.mem (γ := Filter H) (𝓝 ((f : (a : G) → H) 1) : Filter H) U
⊢ Membership.mem (γ := Filter G) (𝓝 1) ((⇑f : (a : G) → H) ⁻¹' U)

Tactic:
apply emb.continuous.tendsto

Premises used: Topology.IsOpenEmbedding.continuous, Continuous.tendsto
-- Module: Mathlib.Topology.Algebra.Nonarchimedean.Basic
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
a a₁ a₂ a₃ : Membership.mem (γ := Filter H) (𝓝 1) U
⊢ Membership.mem (γ := Filter H) (𝓝 ((f : (a : G) → H) 1) : Filter H) U

Tactic:
rwa [f.map_one]

Premises used: MonoidHom.map_one
-- Module: Mathlib.Topology.Algebra.Nonarchimedean.Basic
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
⊢ ∃ (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

Premises used: nhds_prod_eq, Filter.mem_prod_iff
-- Module: Mathlib.Topology.Algebra.Nonarchimedean.Basic
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
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
⊢ ∃ (V : OpenSubgroup G) (W : OpenSubgroup K), (↑V : Set G) ×ˢ (↑W : Set K) ⊆ U

Tactic:
rcases hU with ⟨U₁, hU₁, U₂, hU₂, h⟩
-- Module: Mathlib.Topology.Algebra.Nonarchimedean.Basic
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
obtain :
  ∀ (V : OpenSubgroup G) (hV : (↑V : Set G) ⊆ U₁),
    ∃ (V : OpenSubgroup G) (W : OpenSubgroup K), (↑V : Set G) ×ˢ (↑W : Set K) ⊆ U
⊢ ∃ (V : OpenSubgroup G) (W : OpenSubgroup K), (↑V : Set G) ×ˢ (↑W : Set K) ⊆ U

Tactic:
obtain ⟨V, hV⟩ := is_nonarchimedean _ hU₁

Premises used: NonarchimedeanGroup.is_nonarchimedean
-- Module: Mathlib.Topology.Algebra.Nonarchimedean.Basic
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₁
obtain :
  ∀ (W : OpenSubgroup K) (hW : (↑W : Set K) ⊆ U₂),
    ∃ (V : OpenSubgroup G) (W : OpenSubgroup K), (↑V : Set G) ×ˢ (↑W : Set K) ⊆ U
⊢ ∃ (V : OpenSubgroup G) (W : OpenSubgroup K), (↑V : Set G) ×ˢ (↑W : Set K) ⊆ U

Tactic:
obtain ⟨W, hW⟩ := is_nonarchimedean _ hU₂

Premises used: NonarchimedeanGroup.is_nonarchimedean
-- Module: Mathlib.Topology.Algebra.Nonarchimedean.Basic
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₂
h₁ : ∃ (W : OpenSubgroup K), (↑V : Set G) ×ˢ (↑W : Set K) ⊆ U
⊢ ∃ (V : OpenSubgroup G) (W : OpenSubgroup K), (↑V : Set G) ×ˢ (↑W : Set K) ⊆ U

Tactic:
use V
-- Module: Mathlib.Topology.Algebra.Nonarchimedean.Basic
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₂
⊢ ∃ (W : OpenSubgroup K), (↑V : Set G) ×ˢ (↑W : Set K) ⊆ U

Tactic:
grind
-- Module: Mathlib.Topology.Algebra.Nonarchimedean.Basic
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

Tactic:
Set.Subset.trans (Set.prod_mono ?_ ?_) ‹_›

Premises used: Set.Subset.trans, Set.prod_mono
-- Module: Mathlib.Topology.Algebra.Nonarchimedean.Basic
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)
refine_2 : (↑(V ⊓ W) : Set G) ⊆ (↑W : Set G)
⊢ (↑(V ⊓ W) : Set G) ×ˢ (↑(V ⊓ W) : Set G) ⊆ U

Tactic:
refine Set.Subset.trans (Set.prod_mono ?_ ?_) ‹_›

Premises used: Set.Subset.trans, Set.prod_mono
-- Module: Mathlib.Topology.Algebra.Nonarchimedean.Basic
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 : Set G)

Tactic:
simp
-- Module: Mathlib.Topology.Algebra.Nonarchimedean.Basic
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) ⊆ (↑W : Set G)

Tactic:
simp
-- Module: Mathlib.Topology.Algebra.Nonarchimedean.Basic
Goal:
R : Type u_1
inst : Ring R
inst_1 : TopologicalSpace R
inst_2 : NonarchimedeanRing R
U : OpenAddSubgroup R
r : R
⊢ ∃ (V : OpenAddSubgroup R), r • (↑V : Set R) ⊆ (↑U : Set R)

Tactic:
⟨U.comap (AddMonoidHom.mulLeft r) (continuous_const_mul r), (U : Set R).image_preimage_subset _⟩

Premises used: OpenAddSubgroup.comap, continuous_const_mul, SetLike.coe, Set.image_preimage_subset, Exists.intro, AddMonoidHom.mulLeft
-- Module: Mathlib.Topology.Algebra.Nonarchimedean.Basic
Goal:
R : Type u_1
inst : Ring R
inst_1 : TopologicalSpace R
inst_2 : NonarchimedeanRing R
U : OpenAddSubgroup R
⊢ Membership.mem (γ := Set (R × R)) ((fun (p : R × R) ↦ p.1 * p.2) ⁻¹' (↑U : Set R)) 0

Tactic:
simpa only [Set.mem_preimage, Prod.snd_zero, mul_zero] using U.zero_mem

Premises used: OpenAddSubgroup.toAddSubgroup, MulZeroClass.mul_zero, AddSubgroup.zero_mem, Set.mem_preimage, Prod.snd_zero
-- Module: Mathlib.Topology.Algebra.Nonarchimedean.Basic
Goal:
R : Type u_1
inst : Ring R
inst_1 : TopologicalSpace R
inst_2 : NonarchimedeanRing R
U : OpenAddSubgroup R
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)
⊢ ∃ (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
-- Module: Mathlib.Topology.Algebra.Nonarchimedean.Basic
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)
h : (↑V : Set R) * (↑V : Set R) ⊆ (↑U : Set R)
⊢ ∃ (V : OpenAddSubgroup R), (↑V : Set R) * (↑V : Set R) ⊆ (↑U : Set R)

Tactic:
use V
-- Module: Mathlib.Topology.Algebra.Nonarchimedean.Basic
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
⊢ 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)
-- Module: Mathlib.Topology.Algebra.Nonarchimedean.Basic
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

Tactic:
simp only [Set.mem_preimage, SetLike.mem_coe, hv] at hy

Premises used: SetLike.mem_coe, Set.mem_preimage
-- Module: Mathlib.Topology.Algebra.Nonarchimedean.Basic
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 : v ∈ U
⊢ v ∈ U

Tactic:
hy
-- Module: Mathlib.Topology.Algebra.Nonarchimedean.Basic
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 : v ∈ U
⊢ v ∈ U

Tactic:
exact hy
-- Module: Mathlib.Topology.Algebra.Nonarchimedean.Completion
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
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
⊢ ∃ (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

Premises used: Filter.HasBasis.mem_iff, closed_nhds_basis, Iff.mp, OfNat.ofNat
-- Module: Mathlib.Topology.Algebra.Nonarchimedean.Completion
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
rwa rwa₁ rwa₂ rwa₃ : Membership.mem (γ := Filter (Completion G)) (𝓝 0) C
⊢ Membership.mem (γ := Filter (Completion G)) (𝓝 ((toCompl : (a : G) → Completion G) 0)) C

Tactic:
rwa [map_zero]

Premises used: map_zero
-- Module: Mathlib.Topology.Algebra.Nonarchimedean.Completion
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
⊢ 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])
-- Module: Mathlib.Topology.Algebra.Nonarchimedean.Completion
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)
obtain :
  ∀ (W : OpenAddSubgroup G) (hCW : (↑W : Set G) ⊆ (⇑toCompl : (a : G) → Completion G) ⁻¹' C),
    ∃ (V : OpenAddSubgroup (Completion G)), (↑V : Set (Completion G)) ⊆ U
⊢ ∃ (V : OpenAddSubgroup (Completion G)), (↑V : Set (Completion G)) ⊆ U

Tactic:
obtain ⟨W, hCW⟩ := NonarchimedeanAddGroup.is_nonarchimedean (toCompl ⁻¹' C) this

Premises used: Set.preimage, UniformSpace.Completion.toCompl, NonarchimedeanAddGroup.is_nonarchimedean, DFunLike.coe
-- Module: Mathlib.Topology.Algebra.Nonarchimedean.Completion
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))
hg :
  Membership.mem (γ := Filter (Completion G)) (𝓝 0)
    (↑(topologicalClosure (map toCompl (↑W : AddSubgroup G))) : Set (Completion G))
⊢ IsOpen V

Tactic:
apply isOpen_of_mem_nhds (g := 0)

Premises used: AddSubgroup.isOpen_of_mem_nhds
-- Module: Mathlib.Topology.Algebra.Nonarchimedean.Completion
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))
hg : Membership.mem (γ := Filter G) (𝓝 0) (↑(↑W : AddSubgroup G) : Set G)
⊢ Membership.mem (γ := Filter (Completion G)) (𝓝 0)
    (↑(topologicalClosure (map toCompl (↑W : AddSubgroup G))) : Set (Completion G))

Tactic:
apply (isDenseInducing_toCompl _).closure_image_mem_nhds

Premises used: IsDenseInducing.closure_image_mem_nhds, UniformSpace.Completion.isDenseInducing_toCompl
-- Module: Mathlib.Topology.Algebra.Nonarchimedean.Completion
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 G) (𝓝 0) (↑(↑W : AddSubgroup G) : Set G)

Tactic:
mem_nhds_zero W

Premises used: Set.Mem, OpenAddSubgroup.mem_nhds_zero
-- Module: Mathlib.Topology.Algebra.Nonarchimedean.Completion
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 G) (𝓝 0) (↑(↑W : AddSubgroup G) : Set G)

Tactic:
exact mem_nhds_zero W

Premises used: OpenAddSubgroup.mem_nhds_zero