awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Algebra.Nonarchimedean.AdicTopology
Goal:
A : Type u_2
inst : CommRing A
inst_1 : TopologicalSpace A
inst_2 : IsTopologicalRing A
mp :
  ((∀ (n : ℕ), IsOpen[inst_1] (↑(HPow.hPow (α := Ideal A) ⊥ n) : Set A)) ∧
      ∀ (s : Set A),
        Membership.mem (γ := Filter A) (𝓝 0) s → ∃ (n : ℕ), (↑(HPow.hPow (α := Ideal A) ⊥ n) : Set A) ⊆ s) →
    DiscreteTopology A
mpr :
  DiscreteTopology A →
    (∀ (n : ℕ), IsOpen[inst_1] (↑(HPow.hPow (α := Ideal A) ⊥ n) : Set A)) ∧
      ∀ (s : Set A), Membership.mem (γ := Filter A) (𝓝 0) s → ∃ (n : ℕ), (↑(HPow.hPow (α := Ideal A) ⊥ n) : Set A) ⊆ s
⊢ ((∀ (n : ℕ), IsOpen[inst_1] (↑(HPow.hPow (α := Ideal A) ⊥ n) : Set A)) ∧
      ∀ (s : Set A),
        Membership.mem (γ := Filter A) (𝓝 0) s → ∃ (n : ℕ), (↑(HPow.hPow (α := Ideal A) ⊥ n) : Set A) ⊆ s) ↔
    DiscreteTopology A

Tactic:
constructor
-- Module: Mathlib.Topology.Algebra.Nonarchimedean.AdicTopology
Goal:
A : Type u_2
inst : CommRing A
inst_1 : TopologicalSpace A
inst_2 : IsTopologicalRing A
h : ∀ (n : ℕ), IsOpen[inst_1] (↑(HPow.hPow (α := Ideal A) ⊥ n) : Set A)
_h' : ∀ (s : Set A), Membership.mem (γ := Filter A) (𝓝 0) s → ∃ (n : ℕ), (↑(HPow.hPow (α := Ideal A) ⊥ n) : Set A) ⊆ s
mp : IsOpen[inst_1] {0}
⊢ DiscreteTopology A

Tactic:
rw [discreteTopology_iff_isOpen_singleton_zero]

Premises used: discreteTopology_iff_isOpen_singleton_zero
-- Module: Mathlib.Topology.Algebra.Nonarchimedean.AdicTopology
Goal:
A : Type u_2
inst : CommRing A
inst_1 : TopologicalSpace A
inst_2 : IsTopologicalRing A
h : ∀ (n : ℕ), IsOpen[inst_1] (↑(HPow.hPow (α := Ideal A) ⊥ n) : Set A)
_h' : ∀ (s : Set A), Membership.mem (γ := Filter A) (𝓝 0) s → ∃ (n : ℕ), (↑(HPow.hPow (α := Ideal A) ⊥ n) : Set A) ⊆ s
⊢ IsOpen[inst_1] {0}

Tactic:
simpa using h 1

Premises used: OfNat.ofNat
-- Module: Mathlib.Topology.Algebra.Nonarchimedean.AdicTopology
Goal:
A : Type u_2
inst : CommRing A
inst_1 : TopologicalSpace A
inst_2 : IsTopologicalRing A
h : DiscreteTopology A
mpr : ∀ (n : ℕ), IsOpen[inst_1] (↑(HPow.hPow (α := Ideal A) ⊥ n) : Set A)
mpr₁ : ∀ (s : Set A), Membership.mem (γ := Filter A) (𝓝 0) s → ∃ (n : ℕ), (↑(HPow.hPow (α := Ideal A) ⊥ n) : Set A) ⊆ s
⊢ (∀ (n : ℕ), IsOpen[inst_1] (↑(HPow.hPow (α := Ideal A) ⊥ n) : Set A)) ∧
    ∀ (s : Set A), Membership.mem (γ := Filter A) (𝓝 0) s → ∃ (n : ℕ), (↑(HPow.hPow (α := Ideal A) ⊥ n) : Set A) ⊆ s

Tactic:
constructor
-- Module: Mathlib.Topology.Algebra.Nonarchimedean.AdicTopology
Goal:
A : Type u_2
inst : CommRing A
inst_1 : TopologicalSpace A
inst_2 : IsTopologicalRing A
h : DiscreteTopology A
⊢ ∀ (n : ℕ), IsOpen[inst_1] (↑(HPow.hPow (α := Ideal A) ⊥ n) : Set A)

Tactic:
simp
-- Module: Mathlib.Topology.Algebra.Nonarchimedean.AdicTopology
Goal:
A : Type u_2
inst : CommRing A
inst_1 : TopologicalSpace A
inst_2 : IsTopologicalRing A
h_1 : DiscreteTopology A
U : Set A
U_nhds : Membership.mem (γ := Filter A) (𝓝 0) U
h : (↑(HPow.hPow (α := Ideal A) (β := ℕ) ⊥ 1) : Set A) ⊆ U
⊢ ∃ (n : ℕ), (↑(HPow.hPow (α := Ideal A) ⊥ n) : Set A) ⊆ U

Tactic:
use 1
-- Module: Mathlib.Topology.Algebra.Nonarchimedean.AdicTopology
Goal:
A : Type u_2
inst : CommRing A
inst_1 : TopologicalSpace A
inst_2 : IsTopologicalRing A
h : DiscreteTopology A
U : Set A
U_nhds : Membership.mem (γ := Filter A) (𝓝 0) U
⊢ (↑(HPow.hPow (α := Ideal A) (β := ℕ) ⊥ 1) : Set A) ⊆ U

Tactic:
simp [mem_of_mem_nhds U_nhds]

Premises used: mem_of_mem_nhds
-- Module: Mathlib.Topology.Algebra.Nonarchimedean.AdicTopology
Goal:
R : Type u_1
inst : CommRing R
inst_1 : TopologicalSpace R
I : Ideal R
hI : IsAdic I
⊢ HasBasis.{u_1, 1} (α := R) (𝓝 0) (fun (x : ℕ) ↦ True) fun (n : ℕ) ↦ (↑(I ^ n) : Set R)

Tactic:
hI ▸ Ideal.hasBasis_nhds_zero_adic I

Premises used: Eq.rec, Ideal.hasBasis_nhds_zero_adic, Eq.symm
-- Module: Mathlib.Topology.Algebra.Nonarchimedean.AdicTopology
Goal:
R : Type u_1
inst : CommRing R
inst_1 : TopologicalSpace R
I : Ideal R
hI : IsAdic I
x : R
⊢ (𝓝 x).HasBasis (fun (x : ℕ) ↦ True) fun (n : ℕ) ↦ (fun (x_1 : R) ↦ x + x_1) '' (↑(I ^ n) : Set R)

Tactic:
hI ▸ Ideal.hasBasis_nhds_adic I x

Premises used: Eq.rec, Eq.symm, Ideal.hasBasis_nhds_adic
-- Module: Mathlib.Topology.Algebra.Nonarchimedean.AdicTopology
Goal:
R : Type u_1
inst : CommRing R
inst_1 : WithIdeal R
⊢ NonarchimedeanRing R

Tactic:
RingSubgroupsBasis.nonarchimedean _

Premises used: RingSubgroupsBasis.nonarchimedean
-- Module: Mathlib.Topology.Algebra.Nonarchimedean.AdicTopology
Goal:
R : Type u_1
inst : CommRing R
inst_1 : WithIdeal R
⊢ IsUniformAddGroup R

Tactic:
isUniformAddGroup_of_addCommGroup

Premises used: isUniformAddGroup_of_addCommGroup
-- Module: Mathlib.Topology.Algebra.Nonarchimedean.AdicTopology
Goal:
R : Type u_1
inst : CommRing R
inst_1 : WithIdeal R
⊢ IsLinearTopology R R

Tactic:
i.isLinearTopology

Premises used: Ideal.isLinearTopology, WithIdeal.i
-- Module: Mathlib.Topology.Algebra.Nonarchimedean.AdicTopology
Goal:
R : Type u_1
inst : CommRing R
inst_1 : WithIdeal R
S : Type u_2
inst_2 : CommRing S
inst_3 : WithIdeal S
f : R →+* S
hf : LE.le.{u_2} (α := Ideal S) (Ideal.map (R := R) f i) i
rw :
  ∀ (ib : ℕ),
    True →
      ∃ (ia : ℕ),
        True ∧
          ∀ x ∈ (↑(HPow.hPow (α := Ideal R) i ia) : Set R),
            Membership.mem (α := S) (↑(HPow.hPow (α := Ideal S) i ib) : Set S) ((f : (a : R) → S) x : S)
⊢ ContinuousAt.{u_1, u_2} (X := R) (Y := S) (⇑f : (a : R) → S) 0

Tactic:
rw [ContinuousAt, map_zero, i.hasBasis_nhds_zero_adic.tendsto_iff i.hasBasis_nhds_zero_adic]

Premises used: Filter.HasBasis.tendsto_iff, ContinuousAt, WithIdeal.i, map_zero, Ideal.hasBasis_nhds_zero_adic
-- Module: Mathlib.Topology.Algebra.Nonarchimedean.AdicTopology
Goal:
R : Type u_1
inst : CommRing R
inst_1 : WithIdeal R
S : Type u_2
inst_2 : CommRing S
inst_3 : WithIdeal S
f : R →+* S
hf : LE.le.{u_2} (α := Ideal S) (Ideal.map (R := R) f i) i
⊢ ∀ (ib : ℕ),
    True →
      ∃ (ia : ℕ),
        True ∧
          ∀ x ∈ (↑(HPow.hPow (α := Ideal R) i ia) : Set R),
            Membership.mem (α := S) (↑(HPow.hPow (α := Ideal S) i ib) : Set S) ((f : (a : R) → S) x : S)

Tactic:
fun n _ ↦ ⟨n, trivial, Ideal.map_le_iff_le_comap.mp ?_⟩

Premises used: trivial, Ideal.map_le_iff_le_comap, And.intro, Exists.intro, Iff.mp
-- Module: Mathlib.Topology.Algebra.Nonarchimedean.AdicTopology
Goal:
R : Type u_1
inst : CommRing R
inst_1 : WithIdeal R
S : Type u_2
inst_2 : CommRing S
inst_3 : WithIdeal S
f : R →+* S
hf : LE.le.{u_2} (α := Ideal S) (Ideal.map (R := R) f i) i
refine : ∀ (n : ℕ), True → Ideal.map f (HPow.hPow (α := Ideal R) i n) ≤ HPow.hPow (α := Ideal S) i n
⊢ ∀ (ib : ℕ),
    True →
      ∃ (ia : ℕ),
        True ∧
          ∀ x ∈ (↑(HPow.hPow (α := Ideal R) i ia) : Set R),
            Membership.mem (α := S) (↑(HPow.hPow (α := Ideal S) i ib) : Set S) ((f : (a : R) → S) x : S)

Tactic:
refine fun n _ ↦ ⟨n, trivial, Ideal.map_le_iff_le_comap.mp ?_⟩
-- Module: Mathlib.Topology.Algebra.Nonarchimedean.AdicTopology
Goal:
R : Type u_1
inst : CommRing R
inst_1 : WithIdeal R
S : Type u_2
inst_2 : CommRing S
inst_3 : WithIdeal S
f : R →+* S
hf : LE.le.{u_2} (α := Ideal S) (Ideal.map (R := R) f i) i
n : ℕ
h : True
⊢ Ideal.map f (HPow.hPow (α := Ideal R) i n) ≤ HPow.hPow (α := Ideal S) i n

Tactic:
simpa [Ideal.map_pow] using Ideal.pow_right_mono hf n

Premises used: Ideal.pow_right_mono, Ideal.map_pow
-- Module: Mathlib.Topology.Algebra.Nonarchimedean.AdicTopology
Goal:
R : Type u_1
inst : CommRing R
inst_1 : WithIdeal R
S : Type u_2
inst_2 : CommRing S
inst_3 : WithIdeal S
e : R ≃+* S
h : Eq.{u_2 + 1} (α := Ideal S) (Ideal.map (R := R) e.toRingHom i) i
rw rw₁ : LE.le.{u_2} (α := Ideal S) i i
⊢ LE.le.{u_2} (α := Ideal S) (Ideal.map (R := R) e.toRingHom i) i

Tactic:
rw [h]
-- Module: Mathlib.Topology.Algebra.Nonarchimedean.AdicTopology
Goal:
R : Type u_1
inst : CommRing R
inst_1 : WithIdeal R
S : Type u_2
inst_2 : CommRing S
inst_3 : WithIdeal S
e : R ≃+* S
h : Eq.{u_2 + 1} (α := Ideal S) (Ideal.map (R := R) e.toRingHom i) i
⊢ LE.le.{u_1} (α := Ideal R) (Ideal.map (R := S) e.symm.toRingHom i) i

Tactic:
simp [← h]
-- Module: Mathlib.Topology.Algebra.Nonarchimedean.AdicTopology
Goal:
R : Type u_1
inst : CommRing R
inst_1 : WithIdeal R
a : R
ha : Membership.mem (γ := Ideal R) i a
this : ∀ (m : ℕ), ∃ (n₀ : ℕ), ∀ (n : ℕ), n₀ ≤ n → a ^ n ∈ HPow.hPow (α := Ideal R) i m
⊢ IsTopologicallyNilpotent a

Tactic:
simpa [IsTopologicallyNilpotent, i.hasBasis_nhds_zero_adic.tendsto_right_iff]

Premises used: IsTopologicallyNilpotent, WithIdeal.i, Ideal.hasBasis_nhds_zero_adic, Filter.HasBasis.tendsto_right_iff
-- Module: Mathlib.Topology.Algebra.Nonarchimedean.AdicTopology
Goal:
R : Type u_1
inst : CommRing R
inst_1 : WithIdeal R
a : R
ha : Membership.mem (γ := Ideal R) i a
suffices : ∀ (m : ℕ), ∃ (n₀ : ℕ), ∀ (n : ℕ), n₀ ≤ n → a ^ n ∈ HPow.hPow (α := Ideal R) i m
⊢ IsTopologicallyNilpotent a

Tactic:
suffices ∀ m : ℕ, ∃ n₀, ∀ n, n₀ ≤ n → a ^ n ∈ i ^ m by
    simpa [IsTopologicallyNilpotent, i.hasBasis_nhds_zero_adic.tendsto_right_iff]
-- Module: Mathlib.Topology.Algebra.Nonarchimedean.AdicTopology
Goal:
R : Type u_1
inst : CommRing R
inst_1 : WithIdeal R
a : R
ha : Membership.mem (γ := Ideal R) i a
⊢ ∀ (m : ℕ), ∃ (n₀ : ℕ), ∀ (n : ℕ), n₀ ≤ n → a ^ n ∈ HPow.hPow (α := Ideal R) i m

Tactic:
fun m ↦ ⟨m, fun n hn ↦ Ideal.pow_le_pow_right hn (Ideal.pow_mem_pow ha _)⟩

Premises used: Ideal.pow_le_pow_right, Exists.intro, Ideal.pow_mem_pow
-- Module: Mathlib.Topology.Algebra.Nonarchimedean.AdicTopology
Goal:
R : Type u_1
inst : CommRing R
inst_1 : WithIdeal R
a : R
ha : Membership.mem (γ := Ideal R) i a
⊢ ∀ (m : ℕ), ∃ (n₀ : ℕ), ∀ (n : ℕ), n₀ ≤ n → a ^ n ∈ HPow.hPow (α := Ideal R) i m

Tactic:
exact fun m ↦ ⟨m, fun n hn ↦ Ideal.pow_le_pow_right hn (Ideal.pow_mem_pow ha _)⟩
-- Module: Mathlib.Topology.Algebra.Nonarchimedean.AdicTopology
Goal:
R : Type u_1
inst : CommRing R
inst_1 : WithIdeal R
⊢ NonarchimedeanRing R

Tactic:
infer_instance
-- Module: Mathlib.Topology.Algebra.Nonarchimedean.AdicTopology
Goal:
R : Type u_1
inst : CommRing R
inst_1 : WithIdeal R
⊢ IsTopologicalRing.{u_1} (UniformSpace.Completion R)

Tactic:
infer_instance
-- Module: Mathlib.Topology.Algebra.Nonarchimedean.AdicTopology
Goal:
R : Type u_1
inst : CommRing R
inst_1 : WithIdeal R
M : Type u_2
inst_2 : AddCommGroup M
inst_3 : Module R M
⊢ IsTopologicalAddGroup M

Tactic:
infer_instance
-- Module: Mathlib.Topology.Algebra.Nonarchimedean.AdicTopology
Goal:
R : Type u_1
inst : CommRing R
inst_1 : WithIdeal R
M : Type u_2
inst_2 : AddCommGroup M
inst_3 : Module R M
⊢ ContinuousSMul R M

Tactic:
infer_instance
-- Module: Mathlib.Topology.Algebra.Nonarchimedean.AdicTopology
Goal:
R : Type u_1
inst : CommRing R
inst_1 : WithIdeal R
M : Type u_2
inst_2 : AddCommGroup M
inst_3 : Module R M
⊢ NonarchimedeanAddGroup M

Tactic:
SubmodulesBasis.nonarchimedean _

Premises used: setOf, SubmodulesBasis.nonarchimedean
-- Module: Mathlib.Topology.Algebra.Nonarchimedean.Bases
Goal:
A : Type u_3
ι : Type u_4
inst : CommRing A
B : ι → AddSubgroup A
inter : ∀ (i j : ι), ∃ (k : ι), B k ≤ B i ⊓ B j
mul : ∀ (i : ι), ∃ (j : ι), (↑(B j) : Set A) * (↑(B j) : Set A) ⊆ (↑(B i) : Set A)
leftMul : ∀ (x : A) (i : ι), ∃ (j : ι), (↑(B j) : Set A) ⊆ (fun (y : A) ↦ x * y) ⁻¹' (↑(B i) : Set A)
x : A
i j : ι
hj : (↑(B j) : Set A) ⊆ (fun (y : A) ↦ x * y) ⁻¹' (↑(B i) : Set A)
⊢ (↑(B j) : Set A) ⊆ (fun (x_1 : A) ↦ x_1 * x) ⁻¹' (↑(B i) : Set A)

Tactic:
simpa only [mul_comm] using hj

Premises used: mul_comm
-- 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
inhabit : ∀ (inhabited_h : Inhabited ι), Set.Nonempty.{u_1} (α := Set A) {U : Set A | ∃ (i : ι), U = (↑(B i) : Set A)}
⊢ Set.Nonempty.{u_1} (α := Set A) {U : Set A | ∃ (i : ι), U = (↑(B i) : Set A)}

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

Tactic:
⟨B default, default, rfl⟩

Premises used: Inhabited.default, Set.Nonempty, SetLike.coe, 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
inhabited_h : Inhabited ι
⊢ Set.Nonempty.{u_1} (α := Set A) {U : Set A | ∃ (i : ι), U = (↑(B i) : Set A)}

Tactic:
exact ⟨B default, default, 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
i j : ι
obtain :
  ∀ (k : ι) (hk : B k ≤ B i ⊓ B j),
    ∃ (z : Set A),
      Membership.mem (γ := Set (Set A)) {U : Set A | ∃ (i : ι), U = (↑(B i) : Set A)} z ∧
        z ⊆ (↑(B i) : Set A) ∩ (↑(B j) : Set A)
⊢ ∃ (z : Set A),
    Membership.mem (γ := Set (Set A)) {U : Set A | ∃ (i : ι), U = (↑(B i) : Set A)} z ∧
      z ⊆ (↑(B i) : Set A) ∩ (↑(B j) : Set A)

Tactic:
obtain ⟨k, hk⟩ := hB.inter i j

Premises used: RingSubgroupsBasis.inter
-- 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 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) ∧
    (↑(B k) : Set A) ⊆ (↑(B i) : Set A) ∩ (↑(B j) : Set A)
⊢ ∃ (z : Set A),
    Membership.mem (γ := Set (Set A)) {U : Set A | ∃ (i : ι), U = (↑(B i) : Set A)} z ∧
      z ⊆ (↑(B i) : Set A) ∩ (↑(B j) : 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
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)
h₁ : (↑(B k) : Set A) ⊆ (↑(B i) : Set A) ∩ (↑(B j) : 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)

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
i j k : ι
hk : B k ≤ B i ⊓ B j
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
i j k : ι
hk : B k ≤ B i ⊓ B j
⊢ (↑(B k) : Set A) ⊆ (↑(B i) : Set A) ∩ (↑(B j) : Set A)

Tactic:
hk

Premises used: Set.Mem, setOf, Set.inter, Set.Subset
-- 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 j k : ι
hk : B k ≤ B i ⊓ B j
⊢ (↑(B k) : Set A) ⊆ (↑(B i) : Set A) ∩ (↑(B j) : 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
i : ι
⊢ 0 ∈ (↑(B i) : Set A)

Tactic:
(B i).zero_mem

Premises used: AddSubgroup.zero_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
i : ι
⊢ 0 ∈ (↑(B i) : Set A)

Tactic:
exact (B i).zero_mem

Premises used: AddSubgroup.zero_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
i : ι
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)
⊢ ∃ (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:
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
i : ι
h : Membership.mem (γ := Set (Set A)) {U : Set A | ∃ (i : ι), U = (↑(B i) : Set A)} (↑(B i) : Set A)
h₁ : (↑(B i) : Set A) + (↑(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)

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
i w : ι
h : (↑(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)

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
i : ι
y : A
y_in : y ∈ (↑(B i) : Set A)
z : A
z_in : z ∈ (↑(B i) : Set A)
⊢ (fun (x1 x2 : A) ↦ x1 + x2) y z ∈ (↑(B i) : Set A)

Tactic:
(B i).add_mem y_in z_in

Premises used: Set.Mem, 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
i : ι
y : A
y_in : y ∈ (↑(B i) : Set A)
z : A
z_in : z ∈ (↑(B i) : Set A)
⊢ (fun (x1 x2 : A) ↦ x1 + x2) y z ∈ (↑(B i) : Set A)

Tactic:
exact (B i).add_mem y_in z_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
i : ι
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)
⊢ ∃ (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)

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
i : ι
h : Membership.mem (γ := Set (Set A)) {U : Set A | ∃ (i : ι), U = (↑(B i) : Set A)} (↑(B i) : Set A)
h₁ : (↑(B i) : Set A) ⊆ (fun (x : A) ↦ -x) ⁻¹' (↑(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)

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
i : ι
x : A
x_in : x ∈ (↑(B i) : Set A)
⊢ Membership.mem (γ := Set A) ((fun (x : A) ↦ -x) ⁻¹' (↑(B i) : Set A)) x

Tactic:
(B i).neg_mem x_in

Premises used: Set.Mem, setOf, Set.preimage, AddSubgroup.neg_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
i : ι
x : A
x_in : x ∈ (↑(B i) : Set A)
⊢ Membership.mem (γ := Set A) ((fun (x : A) ↦ -x) ⁻¹' (↑(B i) : Set A)) x

Tactic:
exact (B i).neg_mem x_in

Premises used: AddSubgroup.neg_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
x₀ : A
i : ι
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)
⊢ ∃ (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)

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
x₀ : A
i : ι
h : Membership.mem (γ := Set (Set A)) {U : Set A | ∃ (i : ι), U = (↑(B i) : Set A)} (↑(B i) : Set A)
h₁ : (↑(B i) : Set A) ⊆ (fun (x : A) ↦ x₀ + x + -x₀) ⁻¹' (↑(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)

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 w : ι
h : (↑(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)

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
x₀ : A
i : ι
⊢ (↑(B i) : Set A) ⊆ (fun (x : A) ↦ x₀ + x + -x₀) ⁻¹' (↑(B i) : Set A)

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
i : ι
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)
⊢ ∃ (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

Premises used: RingSubgroupsBasis.mul
-- 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 k : ι
hk : (↑(B k) : Set A) * (↑(B k) : Set A) ⊆ (↑(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) * (↑(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:
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
i k : ι
hk : (↑(B k) : Set A) * (↑(B k) : Set A) ⊆ (↑(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) * (↑(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)

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
i k : ι
hk : (↑(B k) : Set A) * (↑(B k) : Set A) ⊆ (↑(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
i k : ι
hk : (↑(B k) : Set A) * (↑(B k) : Set A) ⊆ (↑(B i) : Set A)
⊢ (↑(B k) : Set A) * (↑(B k) : Set A) ⊆ (↑(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
i k : ι
hk : (↑(B k) : Set A) * (↑(B k) : Set A) ⊆ (↑(B i) : Set A)
⊢ (↑(B k) : Set A) * (↑(B k) : Set A) ⊆ (↑(B i) : Set A)

Tactic:
exact hk