awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Algebra.Nonarchimedean.Bases
Goal:
A : Type u_1
ι : Type u_2
inst : Ring A
inst_1 : Nonempty ι
B : ι → AddSubgroup A
hB : RingSubgroupsBasis B
x₀ : A
i : ι
obtain :
  ∀ (k : ι) (hk : (↑(B k) : Set A) ⊆ (fun (x : A) ↦ x₀ * x) ⁻¹' (↑(B i) : Set A)),
    ∃ (V : Set A),
      Membership.mem (γ := Set (Set A)) {U : Set A | ∃ (i : ι), U = (↑(B i) : Set A)} V ∧
        V ⊆ (fun (x : A) ↦ x₀ * x) ⁻¹' (↑(B i) : Set A)
⊢ ∃ (V : Set A),
    Membership.mem (γ := Set (Set A)) {U : Set A | ∃ (i : ι), U = (↑(B i) : Set A)} V ∧
      V ⊆ (fun (x : A) ↦ x₀ * x) ⁻¹' (↑(B i) : Set A)

Tactic:
obtain ⟨k, hk⟩ := hB.leftMul x₀ i

Premises used: RingSubgroupsBasis.leftMul
-- Module: Mathlib.Topology.Algebra.Nonarchimedean.Bases
Goal:
A : Type u_1
ι : Type u_2
inst : Ring A
inst_1 : Nonempty ι
B : ι → AddSubgroup A
hB : RingSubgroupsBasis B
x₀ : A
i k : ι
hk : (↑(B k) : Set A) ⊆ (fun (x : A) ↦ x₀ * x) ⁻¹' (↑(B i) : Set A)
h :
  Membership.mem (γ := Set (Set A)) {U : Set A | ∃ (i : ι), U = (↑(B i) : Set A)} (↑(B k) : Set A) ∧
    (↑(B k) : Set A) ⊆ (fun (x : A) ↦ x₀ * x) ⁻¹' (↑(B i) : Set A)
⊢ ∃ (V : Set A),
    Membership.mem (γ := Set (Set A)) {U : Set A | ∃ (i : ι), U = (↑(B i) : Set A)} V ∧
      V ⊆ (fun (x : A) ↦ x₀ * x) ⁻¹' (↑(B i) : Set A)

Tactic:
use B k
-- Module: Mathlib.Topology.Algebra.Nonarchimedean.Bases
Goal:
A : Type u_1
ι : Type u_2
inst : Ring A
inst_1 : Nonempty ι
B : ι → AddSubgroup A
hB : RingSubgroupsBasis B
x₀ : A
i k : ι
hk : (↑(B k) : Set A) ⊆ (fun (x : A) ↦ x₀ * x) ⁻¹' (↑(B i) : Set A)
h : Membership.mem (γ := Set (Set A)) {U : Set A | ∃ (i : ι), U = (↑(B i) : Set A)} (↑(B k) : Set A)
h₁ : (↑(B k) : Set A) ⊆ (fun (x : A) ↦ x₀ * x) ⁻¹' (↑(B i) : Set A)
⊢ Membership.mem (γ := Set (Set A)) {U : Set A | ∃ (i : ι), U = (↑(B i) : Set A)} (↑(B k) : Set A) ∧
    (↑(B k) : Set A) ⊆ (fun (x : A) ↦ x₀ * x) ⁻¹' (↑(B i) : Set A)

Tactic:
constructor
-- Module: Mathlib.Topology.Algebra.Nonarchimedean.Bases
Goal:
A : Type u_1
ι : Type u_2
inst : Ring A
inst_1 : Nonempty ι
B : ι → AddSubgroup A
hB : RingSubgroupsBasis B
x₀ : A
i k : ι
hk : (↑(B k) : Set A) ⊆ (fun (x : A) ↦ x₀ * x) ⁻¹' (↑(B i) : Set A)
w : ι
h : (↑(B k) : Set A) = (↑(B k) : Set A)
⊢ Membership.mem (γ := Set (Set A)) {U : Set A | ∃ (i : ι), U = (↑(B i) : Set A)} (↑(B k) : Set A)

Tactic:
use k
-- Module: Mathlib.Topology.Algebra.Nonarchimedean.Bases
Goal:
A : Type u_1
ι : Type u_2
inst : Ring A
inst_1 : Nonempty ι
B : ι → AddSubgroup A
hB : RingSubgroupsBasis B
x₀ : A
i k : ι
hk : (↑(B k) : Set A) ⊆ (fun (x : A) ↦ x₀ * x) ⁻¹' (↑(B i) : Set A)
⊢ (↑(B k) : Set A) ⊆ (fun (x : A) ↦ x₀ * x) ⁻¹' (↑(B i) : Set A)

Tactic:
hk
-- Module: Mathlib.Topology.Algebra.Nonarchimedean.Bases
Goal:
A : Type u_1
ι : Type u_2
inst : Ring A
inst_1 : Nonempty ι
B : ι → AddSubgroup A
hB : RingSubgroupsBasis B
x₀ : A
i k : ι
hk : (↑(B k) : Set A) ⊆ (fun (x : A) ↦ x₀ * x) ⁻¹' (↑(B i) : Set A)
⊢ (↑(B k) : Set A) ⊆ (fun (x : A) ↦ x₀ * x) ⁻¹' (↑(B i) : Set A)

Tactic:
exact hk
-- Module: Mathlib.Topology.Algebra.Nonarchimedean.Bases
Goal:
A : Type u_1
ι : Type u_2
inst : Ring A
inst_1 : Nonempty ι
B : ι → AddSubgroup A
hB : RingSubgroupsBasis B
x₀ : A
i : ι
obtain :
  ∀ (k : ι) (hk : (↑(B k) : Set A) ⊆ (fun (x : A) ↦ x * x₀) ⁻¹' (↑(B i) : Set A)),
    ∃ (V : Set A),
      Membership.mem (γ := Set (Set A)) {U : Set A | ∃ (i : ι), U = (↑(B i) : Set A)} V ∧
        V ⊆ (fun (x : A) ↦ x * x₀) ⁻¹' (↑(B i) : Set A)
⊢ ∃ (V : Set A),
    Membership.mem (γ := Set (Set A)) {U : Set A | ∃ (i : ι), U = (↑(B i) : Set A)} V ∧
      V ⊆ (fun (x : A) ↦ x * x₀) ⁻¹' (↑(B i) : Set A)

Tactic:
obtain ⟨k, hk⟩ := hB.rightMul x₀ i

Premises used: RingSubgroupsBasis.rightMul
-- Module: Mathlib.Topology.Algebra.Nonarchimedean.Bases
Goal:
A : Type u_1
ι : Type u_2
inst : Ring A
inst_1 : Nonempty ι
B : ι → AddSubgroup A
hB : RingSubgroupsBasis B
x₀ : A
i k : ι
hk : (↑(B k) : Set A) ⊆ (fun (x : A) ↦ x * x₀) ⁻¹' (↑(B i) : Set A)
h :
  Membership.mem (γ := Set (Set A)) {U : Set A | ∃ (i : ι), U = (↑(B i) : Set A)} (↑(B k) : Set A) ∧
    (↑(B k) : Set A) ⊆ (fun (x : A) ↦ x * x₀) ⁻¹' (↑(B i) : Set A)
⊢ ∃ (V : Set A),
    Membership.mem (γ := Set (Set A)) {U : Set A | ∃ (i : ι), U = (↑(B i) : Set A)} V ∧
      V ⊆ (fun (x : A) ↦ x * x₀) ⁻¹' (↑(B i) : Set A)

Tactic:
use B k
-- Module: Mathlib.Topology.Algebra.Nonarchimedean.Bases
Goal:
A : Type u_1
ι : Type u_2
inst : Ring A
inst_1 : Nonempty ι
B : ι → AddSubgroup A
hB : RingSubgroupsBasis B
x₀ : A
i k : ι
hk : (↑(B k) : Set A) ⊆ (fun (x : A) ↦ x * x₀) ⁻¹' (↑(B i) : Set A)
h : Membership.mem (γ := Set (Set A)) {U : Set A | ∃ (i : ι), U = (↑(B i) : Set A)} (↑(B k) : Set A)
h₁ : (↑(B k) : Set A) ⊆ (fun (x : A) ↦ x * x₀) ⁻¹' (↑(B i) : Set A)
⊢ Membership.mem (γ := Set (Set A)) {U : Set A | ∃ (i : ι), U = (↑(B i) : Set A)} (↑(B k) : Set A) ∧
    (↑(B k) : Set A) ⊆ (fun (x : A) ↦ x * x₀) ⁻¹' (↑(B i) : Set A)

Tactic:
constructor
-- Module: Mathlib.Topology.Algebra.Nonarchimedean.Bases
Goal:
A : Type u_1
ι : Type u_2
inst : Ring A
inst_1 : Nonempty ι
B : ι → AddSubgroup A
hB : RingSubgroupsBasis B
x₀ : A
i k : ι
hk : (↑(B k) : Set A) ⊆ (fun (x : A) ↦ x * x₀) ⁻¹' (↑(B i) : Set A)
w : ι
h : (↑(B k) : Set A) = (↑(B k) : Set A)
⊢ Membership.mem (γ := Set (Set A)) {U : Set A | ∃ (i : ι), U = (↑(B i) : Set A)} (↑(B k) : Set A)

Tactic:
use k
-- Module: Mathlib.Topology.Algebra.Nonarchimedean.Bases
Goal:
A : Type u_1
ι : Type u_2
inst : Ring A
inst_1 : Nonempty ι
B : ι → AddSubgroup A
hB : RingSubgroupsBasis B
x₀ : A
i k : ι
hk : (↑(B k) : Set A) ⊆ (fun (x : A) ↦ x * x₀) ⁻¹' (↑(B i) : Set A)
⊢ (↑(B k) : Set A) ⊆ (fun (x : A) ↦ x * x₀) ⁻¹' (↑(B i) : Set A)

Tactic:
hk
-- Module: Mathlib.Topology.Algebra.Nonarchimedean.Bases
Goal:
A : Type u_1
ι : Type u_2
inst : Ring A
inst_1 : Nonempty ι
B : ι → AddSubgroup A
hB : RingSubgroupsBasis B
x₀ : A
i k : ι
hk : (↑(B k) : Set A) ⊆ (fun (x : A) ↦ x * x₀) ⁻¹' (↑(B i) : Set A)
⊢ (↑(B k) : Set A) ⊆ (fun (x : A) ↦ x * x₀) ⁻¹' (↑(B i) : Set A)

Tactic:
exact hk
-- Module: Mathlib.Topology.Algebra.Nonarchimedean.Bases
Goal:
A : Type u_1
ι : Type u_2
inst : Ring A
inst_1 : Nonempty ι
B : ι → AddSubgroup A
hB : RingSubgroupsBasis B
V : Set A
⊢ Membership.mem (γ := AddGroupFilterBasis A) RingFilterBasis.toAddGroupFilterBasis V ↔ ∃ (i : ι), V = (↑(B i) : Set A)

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf
-- Module: Mathlib.Topology.Algebra.Nonarchimedean.Bases
Goal:
A : Type u_1
ι : Type u_2
inst : Ring A
inst_1 : Nonempty ι
B : ι → AddSubgroup A
hB : RingSubgroupsBasis B
i : ι
⊢ Membership.mem (γ := AddGroupFilterBasis A) RingFilterBasis.toAddGroupFilterBasis (↑(B i) : Set A)

Tactic:
⟨i, rfl⟩

Premises used: Set.Mem, setOf, Exists.intro, rfl
-- Module: Mathlib.Topology.Algebra.Nonarchimedean.Bases
Goal:
A : Type u_1
ι : Type u_2
inst : Ring A
inst_1 : Nonempty ι
B : ι → AddSubgroup A
hB : RingSubgroupsBasis B
s : Set A
rw :
  (∃ (i : Set A), Membership.mem (γ := AddGroupFilterBasis A) RingFilterBasis.toAddGroupFilterBasis i ∧ id i ⊆ s) ↔
    ∃ (i : ι), True ∧ (↑(B i) : Set A) ⊆ s
⊢ Membership.mem (γ := Filter A) (𝓝 0) s ↔ ∃ (i : ι), True ∧ (↑(B i) : Set A) ⊆ s

Tactic:
rw [hB.toRingFilterBasis.toAddGroupFilterBasis.nhds_zero_hasBasis.mem_iff]

Premises used: Filter.HasBasis.mem_iff, AddGroupFilterBasis.nhds_zero_hasBasis, RingFilterBasis.toAddGroupFilterBasis
-- Module: Mathlib.Topology.Algebra.Nonarchimedean.Bases
Goal:
A : Type u_1
ι : Type u_2
inst : Ring A
inst_1 : Nonempty ι
B : ι → AddSubgroup A
hB : RingSubgroupsBasis B
s : Set A
mp :
  (∃ (i : Set A), Membership.mem (γ := AddGroupFilterBasis A) RingFilterBasis.toAddGroupFilterBasis i ∧ id i ⊆ s) →
    ∃ (i : ι), True ∧ (↑(B i) : Set A) ⊆ s
mpr :
  (∃ (i : ι), True ∧ (↑(B i) : Set A) ⊆ s) →
    ∃ (i : Set A), Membership.mem (γ := AddGroupFilterBasis A) RingFilterBasis.toAddGroupFilterBasis i ∧ id i ⊆ s
⊢ (∃ (i : Set A), Membership.mem (γ := AddGroupFilterBasis A) RingFilterBasis.toAddGroupFilterBasis i ∧ id i ⊆ s) ↔
    ∃ (i : ι), True ∧ (↑(B i) : Set A) ⊆ s

Tactic:
constructor
-- Module: Mathlib.Topology.Algebra.Nonarchimedean.Bases
Goal:
A : Type u_1
ι : Type u_2
inst : Ring A
inst_1 : Nonempty ι
B : ι → AddSubgroup A
hB : RingSubgroupsBasis B
s : Set A
i : ι
hi : id (↑(B i) : Set A) ⊆ s
⊢ ∃ (i : ι), True ∧ (↑(B i) : Set A) ⊆ s

Tactic:
⟨i, trivial, hi⟩

Premises used: trivial, And.intro, Exists.intro
-- Module: Mathlib.Topology.Algebra.Nonarchimedean.Bases
Goal:
A : Type u_1
ι : Type u_2
inst : Ring A
inst_1 : Nonempty ι
B : ι → AddSubgroup A
hB : RingSubgroupsBasis B
s : Set A
i : ι
hi : id (↑(B i) : Set A) ⊆ s
⊢ ∃ (i : ι), True ∧ (↑(B i) : Set A) ⊆ s

Tactic:
exact ⟨i, trivial, hi⟩
-- Module: Mathlib.Topology.Algebra.Nonarchimedean.Bases
Goal:
A : Type u_1
ι : Type u_2
inst : Ring A
inst_1 : Nonempty ι
B : ι → AddSubgroup A
hB : RingSubgroupsBasis B
s : Set A
i : ι
hi : (↑(B i) : Set A) ⊆ s
⊢ ∃ (i : Set A), Membership.mem (γ := AddGroupFilterBasis A) RingFilterBasis.toAddGroupFilterBasis i ∧ id i ⊆ s

Tactic:
⟨B i, ⟨i, rfl⟩, hi⟩

Premises used: SetLike.coe, And.intro, Exists.intro, rfl
-- Module: Mathlib.Topology.Algebra.Nonarchimedean.Bases
Goal:
A : Type u_1
ι : Type u_2
inst : Ring A
inst_1 : Nonempty ι
B : ι → AddSubgroup A
hB : RingSubgroupsBasis B
s : Set A
i : ι
hi : (↑(B i) : Set A) ⊆ s
⊢ ∃ (i : Set A), Membership.mem (γ := AddGroupFilterBasis A) RingFilterBasis.toAddGroupFilterBasis i ∧ id i ⊆ s

Tactic:
exact ⟨B i, ⟨i, rfl⟩, hi⟩
-- Module: Mathlib.Topology.Algebra.Nonarchimedean.Bases
Goal:
A : Type u_1
ι : Type u_2
inst : Ring A
inst_1 : Nonempty ι
B : ι → AddSubgroup A
hB : RingSubgroupsBasis B
a : A
s : Set A
rw :
  (∃ (i : Set A),
      Membership.mem (γ := AddGroupFilterBasis A) RingFilterBasis.toAddGroupFilterBasis i ∧
        (fun (y : A) ↦ a + y) '' i ⊆ s) ↔
    ∃ (i : ι), True ∧ {b : A | b - a ∈ B i} ⊆ s
⊢ s ∈ 𝓝 a ↔ ∃ (i : ι), True ∧ {b : A | b - a ∈ B i} ⊆ s

Tactic:
rw [(hB.toRingFilterBasis.toAddGroupFilterBasis.nhds_hasBasis a).mem_iff]

Premises used: AddGroupFilterBasis.nhds_hasBasis, Filter.HasBasis.mem_iff, RingFilterBasis.toAddGroupFilterBasis
-- Module: Mathlib.Topology.Algebra.Nonarchimedean.Bases
Goal:
A : Type u_1
ι : Type u_2
inst : Ring A
inst_1 : Nonempty ι
B : ι → AddSubgroup A
hB : RingSubgroupsBasis B
a : A
s : Set A
simp :
  (∃ (i : Set A),
      Membership.mem (γ := AddGroupFilterBasis A) RingFilterBasis.toAddGroupFilterBasis i ∧
        (fun (y : A) ↦ a + y) '' i ⊆ s) ↔
    ∃ (i : ι), {b : A | b - a ∈ B i} ⊆ s
⊢ (∃ (i : Set A),
      Membership.mem (γ := AddGroupFilterBasis A) RingFilterBasis.toAddGroupFilterBasis i ∧
        (fun (y : A) ↦ a + y) '' i ⊆ s) ↔
    ∃ (i : ι), True ∧ {b : A | b - a ∈ B i} ⊆ s

Tactic:
simp only [true_and]

Premises used: true_and
-- Module: Mathlib.Topology.Algebra.Nonarchimedean.Bases
Goal:
A : Type u_1
ι : Type u_2
inst : Ring A
inst_1 : Nonempty ι
B : ι → AddSubgroup A
hB : RingSubgroupsBasis B
a : A
s : Set A
mp :
  (∃ (i : Set A),
      Membership.mem (γ := AddGroupFilterBasis A) RingFilterBasis.toAddGroupFilterBasis i ∧
        (fun (y : A) ↦ a + y) '' i ⊆ s) →
    ∃ (i : ι), {b : A | b - a ∈ B i} ⊆ s
mpr :
  (∃ (i : ι), {b : A | b - a ∈ B i} ⊆ s) →
    ∃ (i : Set A),
      Membership.mem (γ := AddGroupFilterBasis A) RingFilterBasis.toAddGroupFilterBasis i ∧
        (fun (y : A) ↦ a + y) '' i ⊆ s
⊢ (∃ (i : Set A),
      Membership.mem (γ := AddGroupFilterBasis A) RingFilterBasis.toAddGroupFilterBasis i ∧
        (fun (y : A) ↦ a + y) '' i ⊆ s) ↔
    ∃ (i : ι), {b : A | b - a ∈ B i} ⊆ s

Tactic:
constructor
-- Module: Mathlib.Topology.Algebra.Nonarchimedean.Bases
Goal:
A : Type u_1
ι : Type u_2
inst : Ring A
inst_1 : Nonempty ι
B : ι → AddSubgroup A
hB : RingSubgroupsBasis B
a : A
s : Set A
i : ι
hi : (fun (y : A) ↦ a + y) '' (↑(B i) : Set A) ⊆ s
h : {b : A | b - a ∈ B i} ⊆ s
⊢ ∃ (i : ι), {b : A | b - a ∈ B i} ⊆ s

Tactic:
use i
-- Module: Mathlib.Topology.Algebra.Nonarchimedean.Bases
Goal:
A : Type u_1
ι : Type u_2
inst : Ring A
inst_1 : Nonempty ι
B : ι → AddSubgroup A
hB : RingSubgroupsBasis B
a : A
s : Set A
i : ι
hi : (fun (y : A) ↦ a + y) '' (↑(B i) : Set A) ⊆ s
h : Eq (α := Set A) {b : A | b - a ∈ B i} ((fun (y : A) ↦ a + y) '' (↑(B i) : Set A))
rw : (fun (y : A) ↦ a + y) '' (↑(B i) : Set A) ⊆ s
⊢ {b : A | b - a ∈ B i} ⊆ s

Tactic:
rw [h]
-- Module: Mathlib.Topology.Algebra.Nonarchimedean.Bases
Goal:
A : Type u_1
ι : Type u_2
inst : Ring A
inst_1 : Nonempty ι
B : ι → AddSubgroup A
hB : RingSubgroupsBasis B
a : A
s : Set A
i : ι
hi : (fun (y : A) ↦ a + y) '' (↑(B i) : Set A) ⊆ s
h : Eq (α := Set A) {b : A | b - a ∈ B i} ((fun (y : A) ↦ a + y) '' (↑(B i) : Set A))
⊢ (fun (y : A) ↦ a + y) '' (↑(B i) : Set A) ⊆ s

Tactic:
assumption
-- Module: Mathlib.Topology.Algebra.Nonarchimedean.Bases
Goal:
A : Type u_1
ι : Type u_2
inst : Ring A
inst_1 : Nonempty ι
B : ι → AddSubgroup A
hB : RingSubgroupsBasis B
a : A
s : Set A
i : ι
hi : (fun (y : A) ↦ a + y) '' (↑(B i) : Set A) ⊆ s
h : Eq (α := Set A) {b : A | b - a ∈ B i} ((fun (y : A) ↦ a + y) '' (↑(B i) : Set A))
⊢ {b : A | b - a ∈ B i} ⊆ s

Tactic:
suffices h : { b : A | b - a ∈ B i } = (fun y => a + y) '' ↑(B i) by
        rw [h]
        assumption
-- Module: Mathlib.Topology.Algebra.Nonarchimedean.Bases
Goal:
A : Type u_1
ι : Type u_2
inst : Ring A
inst_1 : Nonempty ι
B : ι → AddSubgroup A
hB : RingSubgroupsBasis B
a : A
s : Set A
i : ι
hi : (fun (y : A) ↦ a + y) '' (↑(B i) : Set A) ⊆ s
h : Eq (α := Set A) {b : A | b - a ∈ B i} ((fun (x : A) ↦ x - a) ⁻¹' (↑(B i) : Set A))
⊢ Eq (α := Set A) {b : A | b - a ∈ B i} ((fun (y : A) ↦ a + y) '' (↑(B i) : Set A))

Tactic:
simp only [image_add_left, neg_add_eq_sub]

Premises used: neg_add_eq_sub, Set.image_add_left
-- Module: Mathlib.Topology.Algebra.Nonarchimedean.Bases
Goal:
A : Type u_1
ι : Type u_2
inst : Ring A
inst_1 : Nonempty ι
B : ι → AddSubgroup A
hB : RingSubgroupsBasis B
a : A
s : Set A
i : ι
hi : (fun (y : A) ↦ a + y) '' (↑(B i) : Set A) ⊆ s
h :
  ∀ (b : A),
    Membership.mem (γ := Set A) {b : A | b - a ∈ B i} b ↔
      Membership.mem (γ := Set A) ((fun (x : A) ↦ x - a) ⁻¹' (↑(B i) : Set A)) b
⊢ Eq (α := Set A) {b : A | b - a ∈ B i} ((fun (x : A) ↦ x - a) ⁻¹' (↑(B i) : Set A))

Tactic:
ext b
-- Module: Mathlib.Topology.Algebra.Nonarchimedean.Bases
Goal:
A : Type u_1
ι : Type u_2
inst : Ring A
inst_1 : Nonempty ι
B : ι → AddSubgroup A
hB : RingSubgroupsBasis B
a : A
s : Set A
i : ι
hi : (fun (y : A) ↦ a + y) '' (↑(B i) : Set A) ⊆ s
b : A
⊢ Membership.mem (γ := Set A) {b : A | b - a ∈ B i} b ↔
    Membership.mem (γ := Set A) ((fun (x : A) ↦ x - a) ⁻¹' (↑(B i) : Set A)) b

Tactic:
simp
-- Module: Mathlib.Topology.Algebra.Nonarchimedean.Bases
Goal:
A : Type u_1
ι : Type u_2
inst : Ring A
inst_1 : Nonempty ι
B : ι → AddSubgroup A
hB : RingSubgroupsBasis B
a : A
s : Set A
i : ι
hi : {b : A | b - a ∈ B i} ⊆ s
h :
  Membership.mem (γ := AddGroupFilterBasis A) RingFilterBasis.toAddGroupFilterBasis (↑(B i) : Set A) ∧
    (fun (y : A) ↦ a + y) '' (↑(B i) : Set A) ⊆ s
⊢ ∃ (i : Set A),
    Membership.mem (γ := AddGroupFilterBasis A) RingFilterBasis.toAddGroupFilterBasis i ∧ (fun (y : A) ↦ a + y) '' i ⊆ s

Tactic:
use B i
-- Module: Mathlib.Topology.Algebra.Nonarchimedean.Bases
Goal:
A : Type u_1
ι : Type u_2
inst : Ring A
inst_1 : Nonempty ι
B : ι → AddSubgroup A
hB : RingSubgroupsBasis B
a : A
s : Set A
i : ι
hi : {b : A | b - a ∈ B i} ⊆ s
h : Membership.mem (γ := AddGroupFilterBasis A) RingFilterBasis.toAddGroupFilterBasis (↑(B i) : Set A)
h₁ : (fun (y : A) ↦ a + y) '' (↑(B i) : Set A) ⊆ s
⊢ Membership.mem (γ := AddGroupFilterBasis A) RingFilterBasis.toAddGroupFilterBasis (↑(B i) : Set A) ∧
    (fun (y : A) ↦ a + y) '' (↑(B i) : Set A) ⊆ s

Tactic:
constructor
-- Module: Mathlib.Topology.Algebra.Nonarchimedean.Bases
Goal:
A : Type u_1
ι : Type u_2
inst : Ring A
inst_1 : Nonempty ι
B : ι → AddSubgroup A
hB : RingSubgroupsBasis B
a : A
s : Set A
i : ι
hi : {b : A | b - a ∈ B i} ⊆ s
w : ι
h : (↑(B i) : Set A) = (↑(B i) : Set A)
⊢ Membership.mem (γ := AddGroupFilterBasis A) RingFilterBasis.toAddGroupFilterBasis (↑(B i) : Set A)

Tactic:
use i
-- Module: Mathlib.Topology.Algebra.Nonarchimedean.Bases
Goal:
A : Type u_1
ι : Type u_2
inst : Ring A
inst_1 : Nonempty ι
B : ι → AddSubgroup A
hB : RingSubgroupsBasis B
a : A
s : Set A
i : ι
hi : {b : A | b - a ∈ B i} ⊆ s
h : (↑(B i) : Set A) ⊆ (fun (y : A) ↦ a + y) ⁻¹' s
⊢ (fun (y : A) ↦ a + y) '' (↑(B i) : Set A) ⊆ s

Tactic:
rw [image_subset_iff]

Premises used: Set.image_subset_iff
-- Module: Mathlib.Topology.Algebra.Nonarchimedean.Bases
Goal:
A : Type u_1
ι : Type u_2
inst : Ring A
inst_1 : Nonempty ι
B : ι → AddSubgroup A
hB : RingSubgroupsBasis B
a : A
s : Set A
i : ι
hi : {b : A | b - a ∈ B i} ⊆ s
b : A
b_in : b ∈ (↑(B i) : Set A)
h : Membership.mem (γ := Set A) {b : A | b - a ∈ B i} ((fun (y : A) ↦ a + y) b)
⊢ Membership.mem (γ := Set A) ((fun (y : A) ↦ a + y) ⁻¹' s) b

Tactic:
apply hi
-- Module: Mathlib.Topology.Algebra.Nonarchimedean.Bases
Goal:
A : Type u_1
ι : Type u_2
inst : Ring A
inst_1 : Nonempty ι
B : ι → AddSubgroup A
hB : RingSubgroupsBasis B
a : A
s : Set A
i : ι
hi : {b : A | b - a ∈ B i} ⊆ s
b : A
b_in : b ∈ (↑(B i) : Set A)
⊢ Membership.mem (γ := Set A) {b : A | b - a ∈ B i} ((fun (y : A) ↦ a + y) b)

Tactic:
simpa using b_in
-- Module: Mathlib.Topology.Algebra.Nonarchimedean.Bases
Goal:
A : Type u_1
ι : Type u_2
inst : Ring A
inst_1 : Nonempty ι
B : ι → AddSubgroup A
hB : RingSubgroupsBasis B
i : ι
x : TopologicalSpace A := hB.topology
rw : ∀ x ∈ (B i).carrier, (B i).carrier ∈ 𝓝 x
⊢ IsOpen[hB.topology] (B i).carrier

Tactic:
rw [isOpen_iff_mem_nhds]

Premises used: isOpen_iff_mem_nhds
-- Module: Mathlib.Topology.Algebra.Nonarchimedean.Bases
Goal:
A : Type u_1
ι : Type u_2
inst : Ring A
inst_1 : Nonempty ι
B : ι → AddSubgroup A
hB : RingSubgroupsBasis B
i : ι
x : TopologicalSpace A := hB.topology
a : A
a_in : a ∈ (B i).carrier
rw : ∃ (i_1 : ι), True ∧ {b : A | b - a ∈ B i_1} ⊆ (B i).carrier
⊢ (B i).carrier ∈ 𝓝 a

Tactic:
rw [(hB.hasBasis_nhds a).mem_iff]

Premises used: Filter.HasBasis.mem_iff, RingSubgroupsBasis.hasBasis_nhds
-- Module: Mathlib.Topology.Algebra.Nonarchimedean.Bases
Goal:
A : Type u_1
ι : Type u_2
inst : Ring A
inst_1 : Nonempty ι
B : ι → AddSubgroup A
hB : RingSubgroupsBasis B
i : ι
x : TopologicalSpace A := hB.topology
a : A
a_in : a ∈ (B i).carrier
right : {b : A | b - a ∈ B i} ⊆ (B i).carrier
⊢ ∃ (i_1 : ι), True ∧ {b : A | b - a ∈ B i_1} ⊆ (B i).carrier

Tactic:
use i, trivial

Premises used: trivial
-- Module: Mathlib.Topology.Algebra.Nonarchimedean.Bases
Goal:
A : Type u_1
ι : Type u_2
inst : Ring A
inst_1 : Nonempty ι
B : ι → AddSubgroup A
hB : RingSubgroupsBasis B
i : ι
x : TopologicalSpace A := hB.topology
a : A
a_in : a ∈ (B i).carrier
b : A
b_in : Membership.mem (γ := Set A) {b : A | b - a ∈ B i} b
⊢ b ∈ (B i).carrier

Tactic:
simpa using (B i).add_mem a_in b_in

Premises used: AddSubgroup.add_mem
-- Module: Mathlib.Topology.Algebra.Nonarchimedean.Bases
Goal:
A : Type u_1
ι : Type u_2
inst : Ring A
inst_1 : Nonempty ι
B : ι → AddSubgroup A
hB : RingSubgroupsBasis B
this : TopologicalSpace A := hB.topology
is_nonarchimedean : ∀ (U : Set A), Membership.mem (γ := Filter A) (𝓝 0) U → ∃ (V : OpenAddSubgroup A), (↑V : Set A) ⊆ U
⊢ NonarchimedeanRing A

Tactic:
constructor
-- Module: Mathlib.Topology.Algebra.Nonarchimedean.Bases
Goal:
A : Type u_1
ι : Type u_2
inst : Ring A
inst_1 : Nonempty ι
B : ι → AddSubgroup A
hB : RingSubgroupsBasis B
this : TopologicalSpace A := hB.topology
U : Set A
hU : Membership.mem (γ := Filter A) (𝓝 0) U
is_nonarchimedean : ∀ (i : ι) (hi : (↑(B i) : Set A) ⊆ U), ∃ (V : OpenAddSubgroup A), (↑V : Set A) ⊆ U
⊢ ∃ (V : OpenAddSubgroup A), (↑V : Set A) ⊆ U

Tactic:
obtain ⟨i, -, hi : (B i : Set A) ⊆ U⟩ := hB.hasBasis_nhds_zero.mem_iff.mp hU

Premises used: Filter.HasBasis.mem_iff, RingSubgroupsBasis.hasBasis_nhds_zero, Iff.mp
-- Module: Mathlib.Topology.Algebra.Nonarchimedean.Bases
Goal:
A : Type u_1
ι : Type u_2
inst : Ring A
inst_1 : Nonempty ι
B : ι → AddSubgroup A
hB : RingSubgroupsBasis B
this : TopologicalSpace A := hB.topology
U : Set A
hU : Membership.mem (γ := Filter A) (𝓝 0) U
i : ι
hi : (↑(B i) : Set A) ⊆ U
⊢ ∃ (V : OpenAddSubgroup A), (↑V : Set A) ⊆ U

Tactic:
⟨hB.openAddSubgroup i, hi⟩

Premises used: RingSubgroupsBasis.openAddSubgroup, Exists.intro
-- Module: Mathlib.Topology.Algebra.Nonarchimedean.Bases
Goal:
A : Type u_1
ι : Type u_2
inst : Ring A
inst_1 : Nonempty ι
B : ι → AddSubgroup A
hB : RingSubgroupsBasis B
this : TopologicalSpace A := hB.topology
U : Set A
hU : Membership.mem (γ := Filter A) (𝓝 0) U
i : ι
hi : (↑(B i) : Set A) ⊆ U
⊢ ∃ (V : OpenAddSubgroup A), (↑V : Set A) ⊆ 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
B : ι → Submodule R A
hB : SubmodulesRingBasis B
apply :
  ∀ (x : A) (i : ι),
    ∃ (j : ι),
      (↑((B j).toAddSubgroup : AddSubgroup A) : Set A) ⊆
        (fun (y : A) ↦ x * y) ⁻¹' (↑((B i).toAddSubgroup : AddSubgroup A) : Set A)
⊢ RingSubgroupsBasis.{u_3, u_1} (A := A) fun (i : ι) ↦ (B i).toAddSubgroup

Tactic:
apply RingSubgroupsBasis.of_comm (fun i => (B i).toAddSubgroup) hB.inter hB.mul

Premises used: Submodule.toAddSubgroup, SubmodulesRingBasis.inter, RingSubgroupsBasis.of_comm, SubmodulesRingBasis.mul
-- 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
B : ι → Submodule R A
hB : SubmodulesRingBasis B
a : A
i : ι
rcases :
  ∀ (j : ι) (hj : a • B j ≤ B i),
    ∃ (j : ι),
      (↑((B j).toAddSubgroup : AddSubgroup A) : Set A) ⊆
        (fun (y : A) ↦ a * y) ⁻¹' (↑((B i).toAddSubgroup : AddSubgroup A) : Set A)
⊢ ∃ (j : ι),
    (↑((B j).toAddSubgroup : AddSubgroup A) : Set A) ⊆
      (fun (y : A) ↦ a * y) ⁻¹' (↑((B i).toAddSubgroup : AddSubgroup A) : Set A)

Tactic:
rcases hB.leftMul a i with ⟨j, hj⟩

Premises used: SubmodulesRingBasis.leftMul
-- 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
B : ι → Submodule R A
hB : SubmodulesRingBasis B
a : A
i j : ι
hj : a • B j ≤ B i
h :
  (↑((B j).toAddSubgroup : AddSubgroup A) : Set A) ⊆
    (fun (y : A) ↦ a * y) ⁻¹' (↑((B i).toAddSubgroup : AddSubgroup A) : Set A)
⊢ ∃ (j : ι),
    (↑((B j).toAddSubgroup : AddSubgroup A) : Set A) ⊆
      (fun (y : A) ↦ a * y) ⁻¹' (↑((B i).toAddSubgroup : AddSubgroup A) : Set A)

Tactic:
use j
-- 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
B : ι → Submodule R A
hB : SubmodulesRingBasis B
a : A
i j : ι
hj : a • B j ≤ B i
b : A
b_in : b ∈ B j
⊢ Membership.mem (γ := Set A) ((fun (y : A) ↦ a * y) ⁻¹' (↑((B i).toAddSubgroup : AddSubgroup A) : Set A)) b

Tactic:
hj ⟨b, b_in, rfl⟩

Premises used: Set.Mem, setOf, Set.preimage, And.intro, Exists.intro, rfl
-- 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
B : ι → Submodule R A
hB : SubmodulesRingBasis B
a : A
i j : ι
hj : a • B j ≤ B i
b : A
b_in : b ∈ B j
⊢ Membership.mem (γ := Set A) ((fun (y : A) ↦ a * y) ⁻¹' (↑((B i).toAddSubgroup : AddSubgroup A) : Set A)) b

Tactic:
exact hj ⟨b, b_in, rfl⟩

Premises used: And.intro, Exists.intro, rfl
-- 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
inhabit : ∀ (inhabited_h : Inhabited ι), Set.Nonempty.{u_4} (α := Set M) {U : Set M | ∃ (i : ι), U = (↑(B i) : Set M)}
⊢ Set.Nonempty.{u_4} (α := Set M) {U : Set M | ∃ (i : ι), U = (↑(B i) : Set M)}

Tactic:
inhabit ι
-- 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
inhabited_h : Inhabited ι
⊢ Set.Nonempty.{u_4} (α := Set M) {U : Set M | ∃ (i : ι), U = (↑(B i) : Set M)}

Tactic:
⟨B default, default, rfl⟩

Premises used: Inhabited.default, Set.Nonempty, SetLike.coe, Exists.intro, rfl