awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Algebra.Nonarchimedean.Bases (goal)
Goal:
A : Type u_1
ι : Type u_2
inst : Ring A
inst_1 : Nonempty ι
B : ι → AddSubgroup A
hB : RingSubgroupsBasis B
i j k : ι
hk : B k ≤ B i ⊓ B j
h : Membership.mem (γ := Set (Set A)) {U : Set A | ∃ (i : ι), U = (↑(B i) : Set A)} (↑(B k) : Set A)
⊢ Membership.mem (γ := Set (Set A)) {U : Set A | ∃ (i : ι), U = (↑(B i) : Set A)} (↑(B k) : Set A) ∧
    (↑(B k) : Set A) ⊆ (↑(B i) : Set A) ∩ (↑(B j) : Set A)
have h₁ : (↑(B k) : Set A) ⊆ (↑(B i) : Set A) ∩ (↑(B j) : Set A)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Algebra.Nonarchimedean.Bases (goal)
Goal:
A : Type u_1
ι : Type u_2
inst : Ring A
inst_1 : Nonempty ι
B : ι → AddSubgroup A
hB : RingSubgroupsBasis B
i j k : ι
hk : B k ≤ B i ⊓ B j
w : ι
⊢ Membership.mem (γ := Set (Set A)) {U : Set A | ∃ (i : ι), U = (↑(B i) : Set A)} (↑(B k) : Set A)
have h : (↑(B k) : Set A) = (↑(B k) : Set A)
Tactic: use k
-- Lean 4 proof step from Mathlib.Topology.Algebra.Nonarchimedean.Bases (goal)
Goal:
A : Type u_1
ι : Type u_2
inst : Ring A
inst_1 : Nonempty ι
B : ι → AddSubgroup A
hB : RingSubgroupsBasis B
i : ι
⊢ ∃ (V : Set A),
    Membership.mem (γ := Set (Set A)) {U : Set A | ∃ (i : ι), U = (↑(B i) : Set A)} V ∧ V + V ⊆ (↑(B i) : Set A)
have h : Membership.mem (γ := Set (Set A)) {U : Set A | ∃ (i : ι), U = (↑(B i) : Set A)} (↑(B i) : Set A) ∧
  (↑(B i) : Set A) + (↑(B i) : Set A) ⊆ (↑(B i) : Set A)
Tactic: use B i
-- Lean 4 proof step from Mathlib.Topology.Algebra.Nonarchimedean.Bases (goal)
Goal:
A : Type u_1
ι : Type u_2
inst : Ring A
inst_1 : Nonempty ι
B : ι → AddSubgroup A
hB : RingSubgroupsBasis B
i : ι
⊢ Membership.mem (γ := Set (Set A)) {U : Set A | ∃ (i : ι), U = (↑(B i) : Set A)} (↑(B i) : Set A) ∧
    (↑(B i) : Set A) + (↑(B i) : Set A) ⊆ (↑(B i) : Set A)
have h : Membership.mem (γ := Set (Set A)) {U : Set A | ∃ (i : ι), U = (↑(B i) : Set A)} (↑(B i) : Set A)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Algebra.Nonarchimedean.Bases (goal)
Goal:
A : Type u_1
ι : Type u_2
inst : Ring A
inst_1 : Nonempty ι
B : ι → AddSubgroup A
hB : RingSubgroupsBasis B
i : ι
h : Membership.mem (γ := Set (Set A)) {U : Set A | ∃ (i : ι), U = (↑(B i) : Set A)} (↑(B i) : Set A)
⊢ Membership.mem (γ := Set (Set A)) {U : Set A | ∃ (i : ι), U = (↑(B i) : Set A)} (↑(B i) : Set A) ∧
    (↑(B i) : Set A) + (↑(B i) : Set A) ⊆ (↑(B i) : Set A)
have h₁ : (↑(B i) : Set A) + (↑(B i) : Set A) ⊆ (↑(B i) : Set A)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Algebra.Nonarchimedean.Bases (goal)
Goal:
A : Type u_1
ι : Type u_2
inst : Ring A
inst_1 : Nonempty ι
B : ι → AddSubgroup A
hB : RingSubgroupsBasis B
i w : ι
⊢ Membership.mem (γ := Set (Set A)) {U : Set A | ∃ (i : ι), U = (↑(B i) : Set A)} (↑(B i) : Set A)
have h : (↑(B i) : Set A) = (↑(B i) : Set A)
Tactic: use i
-- Lean 4 proof step from Mathlib.Topology.Algebra.Nonarchimedean.Bases (goal)
Goal:
A : Type u_1
ι : Type u_2
inst : Ring A
inst_1 : Nonempty ι
B : ι → AddSubgroup A
hB : RingSubgroupsBasis B
i : ι
⊢ ∃ (V : Set A),
    Membership.mem (γ := Set (Set A)) {U : Set A | ∃ (i : ι), U = (↑(B i) : Set A)} V ∧
      V ⊆ (fun (x : A) ↦ -x) ⁻¹' (↑(B i) : Set A)
have h : Membership.mem (γ := Set (Set A)) {U : Set A | ∃ (i : ι), U = (↑(B i) : Set A)} (↑(B i) : Set A) ∧
  (↑(B i) : Set A) ⊆ (fun (x : A) ↦ -x) ⁻¹' (↑(B i) : Set A)
Tactic: use B i
-- Lean 4 proof step from Mathlib.Topology.Algebra.Nonarchimedean.Bases (goal)
Goal:
A : Type u_1
ι : Type u_2
inst : Ring A
inst_1 : Nonempty ι
B : ι → AddSubgroup A
hB : RingSubgroupsBasis B
i : ι
⊢ Membership.mem (γ := Set (Set A)) {U : Set A | ∃ (i : ι), U = (↑(B i) : Set A)} (↑(B i) : Set A) ∧
    (↑(B i) : Set A) ⊆ (fun (x : A) ↦ -x) ⁻¹' (↑(B i) : Set A)
have h : Membership.mem (γ := Set (Set A)) {U : Set A | ∃ (i : ι), U = (↑(B i) : Set A)} (↑(B i) : Set A)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Algebra.Nonarchimedean.Bases (goal)
Goal:
A : Type u_1
ι : Type u_2
inst : Ring A
inst_1 : Nonempty ι
B : ι → AddSubgroup A
hB : RingSubgroupsBasis B
i : ι
h : Membership.mem (γ := Set (Set A)) {U : Set A | ∃ (i : ι), U = (↑(B i) : Set A)} (↑(B i) : Set A)
⊢ Membership.mem (γ := Set (Set A)) {U : Set A | ∃ (i : ι), U = (↑(B i) : Set A)} (↑(B i) : Set A) ∧
    (↑(B i) : Set A) ⊆ (fun (x : A) ↦ -x) ⁻¹' (↑(B i) : Set A)
have h₁ : (↑(B i) : Set A) ⊆ (fun (x : A) ↦ -x) ⁻¹' (↑(B i) : Set A)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Algebra.Nonarchimedean.Bases (goal)
Goal:
A : Type u_1
ι : Type u_2
inst : Ring A
inst_1 : Nonempty ι
B : ι → AddSubgroup A
hB : RingSubgroupsBasis B
x₀ : A
i : ι
⊢ ∃ (V : Set A),
    Membership.mem (γ := Set (Set A)) {U : Set A | ∃ (i : ι), U = (↑(B i) : Set A)} V ∧
      V ⊆ (fun (x : A) ↦ x₀ + x + -x₀) ⁻¹' (↑(B i) : Set A)
have h : Membership.mem (γ := Set (Set A)) {U : Set A | ∃ (i : ι), U = (↑(B i) : Set A)} (↑(B i) : Set A) ∧
  (↑(B i) : Set A) ⊆ (fun (x : A) ↦ x₀ + x + -x₀) ⁻¹' (↑(B i) : Set A)
Tactic: use B i
-- Lean 4 proof step from Mathlib.Topology.Algebra.Nonarchimedean.Bases (goal)
Goal:
A : Type u_1
ι : Type u_2
inst : Ring A
inst_1 : Nonempty ι
B : ι → AddSubgroup A
hB : RingSubgroupsBasis B
x₀ : A
i : ι
⊢ Membership.mem (γ := Set (Set A)) {U : Set A | ∃ (i : ι), U = (↑(B i) : Set A)} (↑(B i) : Set A) ∧
    (↑(B i) : Set A) ⊆ (fun (x : A) ↦ x₀ + x + -x₀) ⁻¹' (↑(B i) : Set A)
have h : Membership.mem (γ := Set (Set A)) {U : Set A | ∃ (i : ι), U = (↑(B i) : Set A)} (↑(B i) : Set A)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Algebra.Nonarchimedean.Bases (goal)
Goal:
A : Type u_1
ι : Type u_2
inst : Ring A
inst_1 : Nonempty ι
B : ι → AddSubgroup A
hB : RingSubgroupsBasis B
x₀ : A
i : ι
h : Membership.mem (γ := Set (Set A)) {U : Set A | ∃ (i : ι), U = (↑(B i) : Set A)} (↑(B i) : Set A)
⊢ Membership.mem (γ := Set (Set A)) {U : Set A | ∃ (i : ι), U = (↑(B i) : Set A)} (↑(B i) : Set A) ∧
    (↑(B i) : Set A) ⊆ (fun (x : A) ↦ x₀ + x + -x₀) ⁻¹' (↑(B i) : Set A)
have h₁ : (↑(B i) : Set A) ⊆ (fun (x : A) ↦ x₀ + x + -x₀) ⁻¹' (↑(B i) : Set A)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Algebra.Nonarchimedean.Bases (goal)
Goal:
A : Type u_1
ι : Type u_2
inst : Ring A
inst_1 : Nonempty ι
B : ι → AddSubgroup A
hB : RingSubgroupsBasis B
x₀ : A
i w : ι
⊢ Membership.mem (γ := Set (Set A)) {U : Set A | ∃ (i : ι), U = (↑(B i) : Set A)} (↑(B i) : Set A)
have h : (↑(B i) : Set A) = (↑(B i) : Set A)
Tactic: use i
-- Lean 4 proof step from Mathlib.Topology.Algebra.Nonarchimedean.Bases (goal)
Goal:
A : Type u_1
ι : Type u_2
inst : Ring A
inst_1 : Nonempty ι
B : ι → AddSubgroup A
hB : RingSubgroupsBasis B
i : ι
⊢ ∃ (V : Set A),
    Membership.mem (γ := Set (Set A)) {U : Set A | ∃ (i : ι), U = (↑(B i) : Set A)} V ∧ V * V ⊆ (↑(B i) : Set A)
have obtain : ∀ (k : ι) (hk : (↑(B k) : Set A) * (↑(B k) : Set A) ⊆ (↑(B i) : Set A)),
  ∃ (V : Set A),
    Membership.mem (γ := Set (Set A)) {U : Set A | ∃ (i : ι), U = (↑(B i) : Set A)} V ∧ V * V ⊆ (↑(B i) : Set A)
Tactic: obtain ⟨k, hk⟩ := hB.mul i
-- Lean 4 proof step from Mathlib.Topology.Algebra.Nonarchimedean.Bases (goal)
Goal:
A : Type u_1
ι : Type u_2
inst : Ring A
inst_1 : Nonempty ι
B : ι → AddSubgroup A
hB : RingSubgroupsBasis B
i k : ι
hk : (↑(B k) : Set A) * (↑(B k) : Set A) ⊆ (↑(B i) : Set A)
⊢ ∃ (V : Set A),
    Membership.mem (γ := Set (Set A)) {U : Set A | ∃ (i : ι), U = (↑(B i) : Set A)} V ∧ V * V ⊆ (↑(B i) : Set A)
have h : Membership.mem (γ := Set (Set A)) {U : Set A | ∃ (i : ι), U = (↑(B i) : Set A)} (↑(B k) : Set A) ∧
  (↑(B k) : Set A) * (↑(B k) : Set A) ⊆ (↑(B i) : Set A)
Tactic: use B k
-- Lean 4 proof step from Mathlib.Topology.Algebra.Nonarchimedean.Bases (goal)
Goal:
A : Type u_1
ι : Type u_2
inst : Ring A
inst_1 : Nonempty ι
B : ι → AddSubgroup A
hB : RingSubgroupsBasis B
i k : ι
hk : (↑(B k) : Set A) * (↑(B k) : Set A) ⊆ (↑(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) * (↑(B k) : Set A) ⊆ (↑(B i) : Set A)
have h : Membership.mem (γ := Set (Set A)) {U : Set A | ∃ (i : ι), U = (↑(B i) : Set A)} (↑(B k) : Set A)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Algebra.Nonarchimedean.Bases (goal)
Goal:
A : Type u_1
ι : Type u_2
inst : Ring A
inst_1 : Nonempty ι
B : ι → AddSubgroup A
hB : RingSubgroupsBasis B
i k : ι
hk : (↑(B k) : Set A) * (↑(B k) : Set A) ⊆ (↑(B i) : Set A)
w : ι
⊢ Membership.mem (γ := Set (Set A)) {U : Set A | ∃ (i : ι), U = (↑(B i) : Set A)} (↑(B k) : Set A)
have h : (↑(B k) : Set A) = (↑(B k) : Set A)
Tactic: use k
-- Lean 4 proof step from Mathlib.Topology.Algebra.Nonarchimedean.Bases (goal)
Goal:
A : Type u_1
ι : Type u_2
inst : Ring A
inst_1 : Nonempty ι
B : ι → AddSubgroup A
hB : RingSubgroupsBasis B
x₀ : A
i : ι
⊢ ∃ (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)
have 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)
Tactic: obtain ⟨k, hk⟩ := hB.leftMul x₀ i
-- Lean 4 proof step from Mathlib.Topology.Algebra.Nonarchimedean.Bases (goal)
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)
⊢ ∃ (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)
have 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)
Tactic: use B k
-- Lean 4 proof step from Mathlib.Topology.Algebra.Nonarchimedean.Bases (goal)
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)
⊢ 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)
have h : Membership.mem (γ := Set (Set A)) {U : Set A | ∃ (i : ι), U = (↑(B i) : Set A)} (↑(B k) : Set A)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Algebra.Nonarchimedean.Bases (goal)
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 : ι
⊢ Membership.mem (γ := Set (Set A)) {U : Set A | ∃ (i : ι), U = (↑(B i) : Set A)} (↑(B k) : Set A)
have h : (↑(B k) : Set A) = (↑(B k) : Set A)
Tactic: use k
-- Lean 4 proof step from Mathlib.Topology.Algebra.Nonarchimedean.Bases (goal)
Goal:
A : Type u_1
ι : Type u_2
inst : Ring A
inst_1 : Nonempty ι
B : ι → AddSubgroup A
hB : RingSubgroupsBasis B
x₀ : A
i : ι
⊢ ∃ (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)
have 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)
Tactic: obtain ⟨k, hk⟩ := hB.rightMul x₀ i
-- Lean 4 proof step from Mathlib.Topology.Algebra.Nonarchimedean.Bases (goal)
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)
⊢ ∃ (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)
have 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)
Tactic: use B k
-- Lean 4 proof step from Mathlib.Topology.Algebra.Nonarchimedean.Bases (goal)
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)
⊢ 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)
have h : Membership.mem (γ := Set (Set A)) {U : Set A | ∃ (i : ι), U = (↑(B i) : Set A)} (↑(B k) : Set A)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Algebra.Nonarchimedean.Bases (goal)
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 : ι
⊢ Membership.mem (γ := Set (Set A)) {U : Set A | ∃ (i : ι), U = (↑(B i) : Set A)} (↑(B k) : Set A)
have h : (↑(B k) : Set A) = (↑(B k) : Set A)
Tactic: use k
-- Lean 4 proof step from Mathlib.Topology.Algebra.Nonarchimedean.Bases (goal)
Goal:
A : Type u_1
ι : Type u_2
inst : Ring A
inst_1 : Nonempty ι
B : ι → AddSubgroup A
hB : RingSubgroupsBasis B
s : Set A
⊢ Membership.mem (γ := Filter A) (𝓝 0) s ↔ ∃ (i : ι), True ∧ (↑(B i) : Set A) ⊆ s
have rw : (∃ (i : Set A), Membership.mem (γ := AddGroupFilterBasis A) RingFilterBasis.toAddGroupFilterBasis i ∧ id i ⊆ s) ↔
  ∃ (i : ι), True ∧ (↑(B i) : Set A) ⊆ s
Tactic: rw [hB.toRingFilterBasis.toAddGroupFilterBasis.nhds_zero_hasBasis.mem_iff]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Nonarchimedean.Bases (goal)
Goal:
A : Type u_1
ι : Type u_2
inst : Ring A
inst_1 : Nonempty ι
B : ι → AddSubgroup A
hB : RingSubgroupsBasis B
s : Set A
⊢ (∃ (i : Set A), Membership.mem (γ := AddGroupFilterBasis A) RingFilterBasis.toAddGroupFilterBasis i ∧ id i ⊆ s) ↔
    ∃ (i : ι), True ∧ (↑(B i) : Set A) ⊆ s
have mp : (∃ (i : Set A), Membership.mem (γ := AddGroupFilterBasis A) RingFilterBasis.toAddGroupFilterBasis i ∧ id i ⊆ s) →
  ∃ (i : ι), True ∧ (↑(B i) : Set A) ⊆ s
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Algebra.Nonarchimedean.Bases (goal)
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
⊢ (∃ (i : Set A), Membership.mem (γ := AddGroupFilterBasis A) RingFilterBasis.toAddGroupFilterBasis i ∧ id i ⊆ s) ↔
    ∃ (i : ι), True ∧ (↑(B i) : Set A) ⊆ s
have mpr : (∃ (i : ι), True ∧ (↑(B i) : Set A) ⊆ s) →
  ∃ (i : Set A), Membership.mem (γ := AddGroupFilterBasis A) RingFilterBasis.toAddGroupFilterBasis i ∧ id i ⊆ s
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Algebra.Nonarchimedean.Bases (goal)
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
⊢ s ∈ 𝓝 a ↔ ∃ (i : ι), True ∧ {b : A | b - a ∈ B i} ⊆ s
have 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
Tactic: rw [(hB.toRingFilterBasis.toAddGroupFilterBasis.nhds_hasBasis a).mem_iff]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Nonarchimedean.Bases (goal)
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 : 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
have 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
Tactic: simp only [true_and]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Nonarchimedean.Bases (goal)
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 : Set A),
      Membership.mem (γ := AddGroupFilterBasis A) RingFilterBasis.toAddGroupFilterBasis i ∧
        (fun (y : A) ↦ a + y) '' i ⊆ s) ↔
    ∃ (i : ι), {b : A | b - a ∈ B i} ⊆ s
have 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
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Algebra.Nonarchimedean.Bases (goal)
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
⊢ (∃ (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
have 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
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Algebra.Nonarchimedean.Bases (goal)
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
⊢ ∃ (i : ι), {b : A | b - a ∈ B i} ⊆ s
have h : {b : A | b - a ∈ B i} ⊆ s
Tactic: use i
-- Lean 4 proof step from Mathlib.Topology.Algebra.Nonarchimedean.Bases (goal)
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 | b - a ∈ B i} ⊆ s
have h : Eq (α := Set A) {b : A | b - a ∈ B i} ((fun (y : A) ↦ a + y) '' (↑(B i) : Set A))
Tactic: suffices h : { b : A | b - a ∈ B i } = (fun y => a + y) '' ↑(B i) by
        rw [h]
        assumption
-- Lean 4 proof step from Mathlib.Topology.Algebra.Nonarchimedean.Bases (goal)
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
⊢ Eq (α := Set A) {b : A | b - a ∈ B i} ((fun (y : A) ↦ a + y) '' (↑(B i) : Set A))
have h : Eq (α := Set A) {b : A | b - a ∈ B i} ((fun (x : A) ↦ x - a) ⁻¹' (↑(B i) : Set A))
Tactic: simp only [image_add_left, neg_add_eq_sub]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Nonarchimedean.Bases (goal)
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
⊢ Eq (α := Set A) {b : A | b - a ∈ B i} ((fun (x : A) ↦ x - a) ⁻¹' (↑(B i) : Set A))
have 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
Tactic: ext b
-- Lean 4 proof step from Mathlib.Topology.Algebra.Nonarchimedean.Bases (goal)
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
⊢ ∃ (i : Set A),
    Membership.mem (γ := AddGroupFilterBasis A) RingFilterBasis.toAddGroupFilterBasis i ∧ (fun (y : A) ↦ a + y) '' i ⊆ s
have h : Membership.mem (γ := AddGroupFilterBasis A) RingFilterBasis.toAddGroupFilterBasis (↑(B i) : Set A) ∧
  (fun (y : A) ↦ a + y) '' (↑(B i) : Set A) ⊆ s
Tactic: use B i
-- Lean 4 proof step from Mathlib.Topology.Algebra.Nonarchimedean.Bases (goal)
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
⊢ Membership.mem (γ := AddGroupFilterBasis A) RingFilterBasis.toAddGroupFilterBasis (↑(B i) : Set A) ∧
    (fun (y : A) ↦ a + y) '' (↑(B i) : Set A) ⊆ s
have h : Membership.mem (γ := AddGroupFilterBasis A) RingFilterBasis.toAddGroupFilterBasis (↑(B i) : Set A)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Algebra.Nonarchimedean.Bases (goal)
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)
⊢ Membership.mem (γ := AddGroupFilterBasis A) RingFilterBasis.toAddGroupFilterBasis (↑(B i) : Set A) ∧
    (fun (y : A) ↦ a + y) '' (↑(B i) : Set A) ⊆ s
have h₁ : (fun (y : A) ↦ a + y) '' (↑(B i) : Set A) ⊆ s
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Algebra.Nonarchimedean.Bases (goal)
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 : ι
⊢ Membership.mem (γ := AddGroupFilterBasis A) RingFilterBasis.toAddGroupFilterBasis (↑(B i) : Set A)
have h : (↑(B i) : Set A) = (↑(B i) : Set A)
Tactic: use i
-- Lean 4 proof step from Mathlib.Topology.Algebra.Nonarchimedean.Bases (goal)
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
⊢ (fun (y : A) ↦ a + y) '' (↑(B i) : Set A) ⊆ s
have h : (↑(B i) : Set A) ⊆ (fun (y : A) ↦ a + y) ⁻¹' s
Tactic: rw [image_subset_iff]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Nonarchimedean.Bases (goal)
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) ((fun (y : A) ↦ a + y) ⁻¹' s) b
have h : Membership.mem (γ := Set A) {b : A | b - a ∈ B i} ((fun (y : A) ↦ a + y) b)
Tactic: apply hi
-- Lean 4 proof step from Mathlib.Topology.Algebra.Nonarchimedean.Bases (goal)
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
⊢ IsOpen[hB.topology] (B i).carrier
have rw : ∀ x ∈ (B i).carrier, (B i).carrier ∈ 𝓝 x
Tactic: rw [isOpen_iff_mem_nhds]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Nonarchimedean.Bases (goal)
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 i).carrier ∈ 𝓝 a
have rw : ∃ (i_1 : ι), True ∧ {b : A | b - a ∈ B i_1} ⊆ (B i).carrier
Tactic: rw [(hB.hasBasis_nhds a).mem_iff]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Nonarchimedean.Bases (goal)
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
⊢ ∃ (i_1 : ι), True ∧ {b : A | b - a ∈ B i_1} ⊆ (B i).carrier
have right : {b : A | b - a ∈ B i} ⊆ (B i).carrier
Tactic: use i, trivial
-- Lean 4 proof step from Mathlib.Topology.Algebra.Nonarchimedean.Bases (goal)
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
⊢ NonarchimedeanRing A
have is_nonarchimedean : ∀ (U : Set A), Membership.mem (γ := Filter A) (𝓝 0) U → ∃ (V : OpenAddSubgroup A), (↑V : Set A) ⊆ U
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Algebra.Nonarchimedean.Bases (goal)
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
⊢ ∃ (V : OpenAddSubgroup A), (↑V : Set A) ⊆ U
have is_nonarchimedean : ∀ (i : ι) (hi : (↑(B i) : 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