awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Algebra.ValuativeRel.ValuativeTopology
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
Γ₀ : Type u_2
inst_2 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
inst_3 : v.Compatible
x : R
s : Set R
⊢ (∃ (γ : (ValueGroup₀ v)ˣ),
      {z : R | (v.restrict : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) (z - x) < (↑γ : ValueGroup₀ v)} ⊆ s) ↔
    ∃ (γ : (ValueGroupWithZero R)ˣ),
      {a : R | (valuation R : (a : R) → ValueGroupWithZero R) (a - x) < (↑γ : ValueGroupWithZero R)} ⊆ s

Tactic:
⟨fun ⟨r, hr⟩ ↦ ⟨r.mapEquiv (orderMonoidIso v).symm, ?_⟩,
    fun ⟨r, hr⟩ ↦ ⟨r.mapEquiv (orderMonoidIso v), ?_⟩⟩

Premises used: Units.val, setOf, HSub.hSub, Exists, _private.0.Valuation.exists_setOf_restrict_le_iff.match_1, HasSubset.Subset, Units.mapEquiv, LT.lt, Iff.intro, Exists.intro, _private.0.Valuation.exists_setOf_restrict_le_iff.match_2, ValuativeRel.valuation, DFunLike.coe, Valuation.restrict
-- Module: Mathlib.Topology.Algebra.ValuativeRel.ValuativeTopology
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
Γ₀ : Type u_2
inst_2 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
inst_3 : v.Compatible
x : R
s : Set R
refine_1 :
  (∃ (γ : (ValueGroup₀ v)ˣ),
      {z : R | (v.restrict : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) (z - x) < (↑γ : ValueGroup₀ v)} ⊆ s) →
    ∀ (r : (ValueGroup₀ v)ˣ)
      (hr : {z : R | (v.restrict : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) (z - x) < (↑r : ValueGroup₀ v)} ⊆ s),
      {a : R |
          LT.lt (α := ValueGroupWithZero R)
            ((valuation R : (a : R) → ValueGroupWithZero R) (a - x) : ValueGroupWithZero R)
            ((↑(((Units.mapEquiv (↑(OrderMonoidIso.symm (orderMonoidIso v)) : ValueGroup₀ v ≃* ValueGroupWithZero R) :
                        MulEquiv.{u_2, u_1} (ValueGroup₀ v)ˣ (ValueGroupWithZero R)ˣ) :
                      (a : (ValueGroup₀ v)ˣ) → (ValueGroupWithZero R)ˣ)
                    r) :
                ValueGroupWithZero R) :
              ValueGroupWithZero R)} ⊆
        s
refine_2 :
  (∃ (γ : (ValueGroupWithZero R)ˣ),
      {a : R | (valuation R : (a : R) → ValueGroupWithZero R) (a - x) < (↑γ : ValueGroupWithZero R)} ⊆ s) →
    ∀ (r : (ValueGroupWithZero R)ˣ)
      (hr : {a : R | (valuation R : (a : R) → ValueGroupWithZero R) (a - x) < (↑r : ValueGroupWithZero R)} ⊆ s),
      {z : R |
          LT.lt.{u_2} (α := ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
            ((v.restrict : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) (z - x) : ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
            ((↑(((Units.mapEquiv (↑(orderMonoidIso v) : ValueGroupWithZero R ≃* ValueGroup₀ v) :
                        MulEquiv.{u_1, u_2} (ValueGroupWithZero R)ˣ (ValueGroup₀ v)ˣ) :
                      (a : (ValueGroupWithZero R)ˣ) → (ValueGroup₀ v)ˣ)
                    r) :
                ValueGroup₀ v) :
              ValueGroup₀ v)} ⊆
        s
⊢ (∃ (γ : (ValueGroup₀ v)ˣ),
      {z : R | (v.restrict : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) (z - x) < (↑γ : ValueGroup₀ v)} ⊆ s) ↔
    ∃ (γ : (ValueGroupWithZero R)ˣ),
      {a : R | (valuation R : (a : R) → ValueGroupWithZero R) (a - x) < (↑γ : ValueGroupWithZero R)} ⊆ s

Tactic:
refine ⟨fun ⟨r, hr⟩ ↦ ⟨r.mapEquiv (orderMonoidIso v).symm, ?_⟩,
    fun ⟨r, hr⟩ ↦ ⟨r.mapEquiv (orderMonoidIso v), ?_⟩⟩
-- Module: Mathlib.Topology.Algebra.ValuativeRel.ValuativeTopology
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
Γ₀ : Type u_2
inst_2 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
inst_3 : v.Compatible
x : R
s : Set R
h :
  ∃ (γ : (ValueGroup₀ v)ˣ),
    {z : R | (v.restrict : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) (z - x) < (↑γ : ValueGroup₀ v)} ⊆ s
r : (ValueGroup₀ v)ˣ
hr : {z : R | (v.restrict : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) (z - x) < (↑r : ValueGroup₀ v)} ⊆ s
⊢ {z : R | (v.restrict : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) (z - x) < (↑r : ValueGroup₀ v)} ⊆ s

Tactic:
hr
-- Module: Mathlib.Topology.Algebra.ValuativeRel.ValuativeTopology
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
Γ₀ : Type u_2
inst_2 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
inst_3 : v.Compatible
x : R
s : Set R
h_1 :
  ∃ (γ : (ValueGroup₀ v)ˣ),
    {z : R | (v.restrict : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) (z - x) < (↑γ : ValueGroup₀ v)} ⊆ s
r : (ValueGroup₀ v)ˣ
hr : {z : R | (v.restrict : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) (z - x) < (↑r : ValueGroup₀ v)} ⊆ s
h :
  ∀ (x_1 : R),
    LT.lt (α := ValueGroupWithZero R) ((valuation R : (a : R) → ValueGroupWithZero R) (x_1 - x) : ValueGroupWithZero R)
        ((↑(((Units.mapEquiv (↑(OrderMonoidIso.symm (orderMonoidIso v)) : ValueGroup₀ v ≃* ValueGroupWithZero R) :
                    MulEquiv.{u_2, u_1} (ValueGroup₀ v)ˣ (ValueGroupWithZero R)ˣ) :
                  (a : (ValueGroup₀ v)ˣ) → (ValueGroupWithZero R)ˣ)
                r) :
            ValueGroupWithZero R) :
          ValueGroupWithZero R) ↔
      (v.restrict : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) (x_1 - x) < (↑r : ValueGroup₀ v)
⊢ {a : R |
      LT.lt (α := ValueGroupWithZero R) ((valuation R : (a : R) → ValueGroupWithZero R) (a - x) : ValueGroupWithZero R)
        ((↑(((Units.mapEquiv (↑(OrderMonoidIso.symm (orderMonoidIso v)) : ValueGroup₀ v ≃* ValueGroupWithZero R) :
                    MulEquiv.{u_2, u_1} (ValueGroup₀ v)ˣ (ValueGroupWithZero R)ˣ) :
                  (a : (ValueGroup₀ v)ˣ) → (ValueGroupWithZero R)ˣ)
                r) :
            ValueGroupWithZero R) :
          ValueGroupWithZero R)} ⊆
    s

Tactic:
convert! hr
-- Module: Mathlib.Topology.Algebra.ValuativeRel.ValuativeTopology
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
Γ₀ : Type u_2
inst_2 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
inst_3 : v.Compatible
x : R
s : Set R
h :
  ∃ (γ : (ValueGroup₀ v)ˣ),
    {z : R | (v.restrict : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) (z - x) < (↑γ : ValueGroup₀ v)} ⊆ s
r : (ValueGroup₀ v)ˣ
hr : {z : R | (v.restrict : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) (z - x) < (↑r : ValueGroup₀ v)} ⊆ s
x_1 : R
⊢ LT.lt (α := ValueGroupWithZero R) ((valuation R : (a : R) → ValueGroupWithZero R) (x_1 - x) : ValueGroupWithZero R)
      ((↑(((Units.mapEquiv (↑(OrderMonoidIso.symm (orderMonoidIso v)) : ValueGroup₀ v ≃* ValueGroupWithZero R) :
                  MulEquiv.{u_2, u_1} (ValueGroup₀ v)ˣ (ValueGroupWithZero R)ˣ) :
                (a : (ValueGroup₀ v)ˣ) → (ValueGroupWithZero R)ˣ)
              r) :
          ValueGroupWithZero R) :
        ValueGroupWithZero R) ↔
    (v.restrict : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) (x_1 - x) < (↑r : ValueGroup₀ v)

Tactic:
simp
-- Module: Mathlib.Topology.Algebra.ValuativeRel.ValuativeTopology
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
Γ₀ : Type u_2
inst_2 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
inst_3 : v.Compatible
x : R
s : Set R
h :
  ∃ (γ : (ValueGroupWithZero R)ˣ),
    {a : R | (valuation R : (a : R) → ValueGroupWithZero R) (a - x) < (↑γ : ValueGroupWithZero R)} ⊆ s
r : (ValueGroupWithZero R)ˣ
hr : {a : R | (valuation R : (a : R) → ValueGroupWithZero R) (a - x) < (↑r : ValueGroupWithZero R)} ⊆ s
⊢ {a : R | (valuation R : (a : R) → ValueGroupWithZero R) (a - x) < (↑r : ValueGroupWithZero R)} ⊆ s

Tactic:
hr
-- Module: Mathlib.Topology.Algebra.ValuativeRel.ValuativeTopology
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
Γ₀ : Type u_2
inst_2 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
inst_3 : v.Compatible
x : R
s : Set R
h_1 :
  ∃ (γ : (ValueGroupWithZero R)ˣ),
    {a : R | (valuation R : (a : R) → ValueGroupWithZero R) (a - x) < (↑γ : ValueGroupWithZero R)} ⊆ s
r : (ValueGroupWithZero R)ˣ
hr : {a : R | (valuation R : (a : R) → ValueGroupWithZero R) (a - x) < (↑r : ValueGroupWithZero R)} ⊆ s
h :
  ∀ (x_1 : R),
    LT.lt.{u_2} (α := ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
        ((v.restrict : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) (x_1 - x) : ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
        ((↑(((Units.mapEquiv (↑(orderMonoidIso v) : ValueGroupWithZero R ≃* ValueGroup₀ v) :
                    MulEquiv.{u_1, u_2} (ValueGroupWithZero R)ˣ (ValueGroup₀ v)ˣ) :
                  (a : (ValueGroupWithZero R)ˣ) → (ValueGroup₀ v)ˣ)
                r) :
            ValueGroup₀ v) :
          ValueGroup₀ v) ↔
      (valuation R : (a : R) → ValueGroupWithZero R) (x_1 - x) < (↑r : ValueGroupWithZero R)
⊢ {z : R |
      LT.lt.{u_2} (α := ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
        ((v.restrict : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) (z - x) : ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
        ((↑(((Units.mapEquiv (↑(orderMonoidIso v) : ValueGroupWithZero R ≃* ValueGroup₀ v) :
                    MulEquiv.{u_1, u_2} (ValueGroupWithZero R)ˣ (ValueGroup₀ v)ˣ) :
                  (a : (ValueGroupWithZero R)ˣ) → (ValueGroup₀ v)ˣ)
                r) :
            ValueGroup₀ v) :
          ValueGroup₀ v)} ⊆
    s

Tactic:
convert! hr
-- Module: Mathlib.Topology.Algebra.ValuativeRel.ValuativeTopology
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
Γ₀ : Type u_2
inst_2 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
inst_3 : v.Compatible
x : R
s : Set R
h :
  ∃ (γ : (ValueGroupWithZero R)ˣ),
    {a : R | (valuation R : (a : R) → ValueGroupWithZero R) (a - x) < (↑γ : ValueGroupWithZero R)} ⊆ s
r : (ValueGroupWithZero R)ˣ
hr : {a : R | (valuation R : (a : R) → ValueGroupWithZero R) (a - x) < (↑r : ValueGroupWithZero R)} ⊆ s
x_1 : R
⊢ LT.lt.{u_2} (α := ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
      ((v.restrict : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) (x_1 - x) : ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
      ((↑(((Units.mapEquiv (↑(orderMonoidIso v) : ValueGroupWithZero R ≃* ValueGroup₀ v) :
                  MulEquiv.{u_1, u_2} (ValueGroupWithZero R)ˣ (ValueGroup₀ v)ˣ) :
                (a : (ValueGroupWithZero R)ˣ) → (ValueGroup₀ v)ˣ)
              r) :
          ValueGroup₀ v) :
        ValueGroup₀ v) ↔
    (valuation R : (a : R) → ValueGroupWithZero R) (x_1 - x) < (↑r : ValueGroupWithZero R)

Tactic:
simp
-- Module: Mathlib.Topology.Algebra.ValuativeRel.ValuativeTopology
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
⊢ NonarchimedeanRing R

Tactic:
(valuation R).subgroups_basis.nonarchimedean

Premises used: Set.Mem, setOf, Valuation.subgroups_basis, ValuativeRel.valuation, RingSubgroupsBasis.nonarchimedean
-- Module: Mathlib.Topology.Algebra.ValuativeRel.ValuativeTopology
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
s : Set R
x : R
rw :
  (∃ (i : (ValueGroup₀ (F := Valuation R (ValueGroupWithZero R)) (valuation R))ˣ),
      True ∧
        {b : R |
            Membership.mem (γ := AddSubgroup R)
              (ltAddSubgroup (Γ₀ := ValueGroupWithZero R) (valuation R)
                ((Units.map (↑embedding : ValueGroup₀ (valuation R) →* ValueGroupWithZero R) :
                    (a : (ValueGroup₀ (valuation R))ˣ) → (ValueGroupWithZero R)ˣ)
                  i))
              (b - x)} ⊆
          s) ↔
    ∃ (γ : (ValueGroupWithZero R)ˣ),
      (fun (x_1 : R) ↦ x + x_1) ''
          {z : R | (valuation R : (a : R) → ValueGroupWithZero R) z < (↑γ : ValueGroupWithZero R)} ⊆
        s
⊢ s ∈ 𝓝 x ↔
    ∃ (γ : (ValueGroupWithZero R)ˣ),
      (fun (x_1 : R) ↦ x + x_1) ''
          {z : R | (valuation R : (a : R) → ValueGroupWithZero R) z < (↑γ : ValueGroupWithZero R)} ⊆
        s

Tactic:
rw [Filter.hasBasis_iff.mp ((valuation R).subgroups_basis.hasBasis_nhds x) s]

Premises used: Valuation.subgroups_basis, Filter.hasBasis_iff, RingSubgroupsBasis.hasBasis_nhds, Iff.mp, ValuativeRel.valuation
-- Module: Mathlib.Topology.Algebra.ValuativeRel.ValuativeTopology
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
s : Set R
x : R
⊢ (∃ (i : (ValueGroup₀ (F := Valuation R (ValueGroupWithZero R)) (valuation R))ˣ),
      True ∧
        {b : R |
            Membership.mem (γ := AddSubgroup R)
              (ltAddSubgroup (Γ₀ := ValueGroupWithZero R) (valuation R)
                ((Units.map (↑embedding : ValueGroup₀ (valuation R) →* ValueGroupWithZero R) :
                    (a : (ValueGroup₀ (valuation R))ˣ) → (ValueGroupWithZero R)ˣ)
                  i))
              (b - x)} ⊆
          s) ↔
    ∃ (γ : (ValueGroupWithZero R)ˣ),
      (fun (x_1 : R) ↦ x + x_1) ''
          {z : R | (valuation R : (a : R) → ValueGroupWithZero R) z < (↑γ : ValueGroupWithZero R)} ⊆
        s

Tactic:
simp [neg_add_eq_sub, ← (valuation R).exists_setOf_restrict_le_iff,
      ← restrict_lt_iff_lt_embedding]

Premises used: neg_add_eq_sub, Valuation.restrict_lt_iff_lt_embedding, ValuativeRel.valuation, Valuation.exists_setOf_restrict_le_iff
-- Module: Mathlib.Topology.Algebra.ValuativeRel.ValuativeTopology
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
⊢ IsUniformAddGroup R

Tactic:
isUniformAddGroup_of_addCommGroup

Premises used: isUniformAddGroup_of_addCommGroup
-- Module: Mathlib.Topology.Algebra.ValuativeRel.ValuativeTopology
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
inst_2 : TopologicalSpace R
inst_3 : IsValuativeTopology R
s : Set R
x : R
⊢ s ∈ 𝓝 x ↔
    ∃ (γ : (ValueGroupWithZero R)ˣ),
      (fun (x_1 : R) ↦ x + x_1) ''
          {z : R | (valuation R : (a : R) → ValueGroupWithZero R) z < (↑γ : ValueGroupWithZero R)} ⊆
        s

Tactic:
mem_nhds_iff (s := s)

Premises used: IsValuativeTopology.mem_nhds_iff
-- Module: Mathlib.Topology.Algebra.ValuativeRel.ValuativeTopology
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
inst_2 : TopologicalSpace R
inst_3 : IsValuativeTopology R
s : Set R
x : R
h :
  ∀ (x_1 : (ValueGroupWithZero R)ˣ),
    Eq.{u_1 + 1} (α := Set R)
      {z : R | (valuation R : (a : R) → ValueGroupWithZero R) (z - x) < (↑x_1 : ValueGroupWithZero R)}
      ((fun (x_2 : R) ↦ x + x_2) ''
        {z : R | (valuation R : (a : R) → ValueGroupWithZero R) z < (↑x_1 : ValueGroupWithZero R)})
⊢ s ∈ 𝓝 x ↔
    ∃ (γ : (ValueGroupWithZero R)ˣ),
      {z : R | (valuation R : (a : R) → ValueGroupWithZero R) (z - x) < (↑γ : ValueGroupWithZero R)} ⊆ s

Tactic:
convert! mem_nhds_iff (s := s) using 4

Premises used: IsValuativeTopology.mem_nhds_iff
-- Module: Mathlib.Topology.Algebra.ValuativeRel.ValuativeTopology
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
inst_2 : TopologicalSpace R
inst_3 : IsValuativeTopology R
s : Set R
x : R
x_1 : (ValueGroupWithZero R)ˣ
⊢ Eq.{u_1 + 1} (α := Set R)
    {z : R | (valuation R : (a : R) → ValueGroupWithZero R) (z - x) < (↑x_1 : ValueGroupWithZero R)}
    ((fun (x_2 : R) ↦ x + x_2) ''
      {z : R | (valuation R : (a : R) → ValueGroupWithZero R) z < (↑x_1 : ValueGroupWithZero R)})

Tactic:
simp [neg_add_eq_sub]

Premises used: neg_add_eq_sub
-- Module: Mathlib.Topology.Algebra.ValuativeRel.ValuativeTopology
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
inst_2 : TopologicalSpace R
inst_3 : IsValuativeTopology R
s : Set R
⊢ Membership.mem (γ := Filter R) (𝓝 0) s ↔
    ∃ (γ : (ValueGroupWithZero R)ˣ),
      {x : R | (valuation R : (a : R) → ValueGroupWithZero R) x < (↑γ : ValueGroupWithZero R)} ⊆ s

Tactic:
simp [mem_nhds_iff']

Premises used: IsValuativeTopology.mem_nhds_iff'
-- Module: Mathlib.Topology.Algebra.ValuativeRel.ValuativeTopology
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
inst_2 : TopologicalSpace R
inst_3 : IsValuativeTopology R
x : R
⊢ (𝓝 x).HasBasis (fun (x : (ValueGroupWithZero R)ˣ) ↦ True) fun (γ : (ValueGroupWithZero R)ˣ) ↦
    {z : R | (valuation R : (a : R) → ValueGroupWithZero R) (z - x) < (↑γ : ValueGroupWithZero R)}

Tactic:
simp [Filter.hasBasis_iff, mem_nhds_iff']

Premises used: IsValuativeTopology.mem_nhds_iff', Filter.hasBasis_iff
-- Module: Mathlib.Topology.Algebra.ValuativeRel.ValuativeTopology
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
inst_2 : TopologicalSpace R
inst_3 : IsValuativeTopology R
x : R
γ : (ValueGroupWithZero R)ˣ
h : True
⊢ (↑γ : ValueGroupWithZero R) ≠ 0 ∧
    Subset.{u_1} (α := Set R)
      {y : R | (valuation R : (a : R) → ValueGroupWithZero R) (y - x) < (↑γ : ValueGroupWithZero R)}
      {z : R | (valuation R : (a : R) → ValueGroupWithZero R) (z - x) < (↑γ : ValueGroupWithZero R)}

Tactic:
simp
-- Module: Mathlib.Topology.Algebra.ValuativeRel.ValuativeTopology
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
inst_2 : TopologicalSpace R
inst_3 : IsValuativeTopology R
x : R
γ : ValueGroupWithZero R
hγ : γ ≠ 0
⊢ True ∧
    Subset.{u_1} (α := Set R)
      {z : R | (valuation R : (a : R) → ValueGroupWithZero R) (z - x) < (↑(Units.mk0 γ hγ) : ValueGroupWithZero R)}
      {y : R | (valuation R : (a : R) → ValueGroupWithZero R) (y - x) < γ}

Tactic:
simp
-- Module: Mathlib.Topology.Algebra.ValuativeRel.ValuativeTopology
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
inst_2 : TopologicalSpace R
inst_3 : IsValuativeTopology R
⊢ HasBasis (α := R) (𝓝 0) (fun (x : (ValueGroupWithZero R)ˣ) ↦ True) fun (γ : (ValueGroupWithZero R)ˣ) ↦
    {z : R | (valuation R : (a : R) → ValueGroupWithZero R) (z - 0) < (↑γ : ValueGroupWithZero R)}

Tactic:
hasBasis_nhds (0 : R)

Premises used: IsValuativeTopology.hasBasis_nhds, OfNat.ofNat
-- Module: Mathlib.Topology.Algebra.ValuativeRel.ValuativeTopology
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
inst_2 : TopologicalSpace R
inst_3 : IsValuativeTopology R
h : ∀ (x : (ValueGroupWithZero R)ˣ) (x : R), x = x - 0
⊢ HasBasis (α := R) (𝓝 0) (fun (x : (ValueGroupWithZero R)ˣ) ↦ True) fun (γ : (ValueGroupWithZero R)ˣ) ↦
    {x : R | (valuation R : (a : R) → ValueGroupWithZero R) x < (↑γ : ValueGroupWithZero R)}

Tactic:
convert! hasBasis_nhds (0 : R)

Premises used: IsValuativeTopology.hasBasis_nhds, OfNat.ofNat
-- Module: Mathlib.Topology.Algebra.ValuativeRel.ValuativeTopology
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
inst_2 : TopologicalSpace R
inst_3 : IsValuativeTopology R
x : (ValueGroupWithZero R)ˣ
x_1 : R
h h₁ : x_1 = x_1
⊢ x_1 = x_1 - 0

Tactic:
rw [sub_zero]

Premises used: sub_zero
-- Module: Mathlib.Topology.Algebra.ValuativeRel.ValuativeTopology
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
inst_2 : TopologicalSpace R
inst_3 : IsValuativeTopology R
γ : (ValueGroupWithZero R)ˣ
h : True
⊢ (↑γ : ValueGroupWithZero R) ≠ 0 ∧
    Subset.{u_1} (α := Set R) {x : R | (valuation R : (a : R) → ValueGroupWithZero R) x < (↑γ : ValueGroupWithZero R)}
      {x : R | (valuation R : (a : R) → ValueGroupWithZero R) x < (↑γ : ValueGroupWithZero R)}

Tactic:
simp
-- Module: Mathlib.Topology.Algebra.ValuativeRel.ValuativeTopology
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
inst_2 : TopologicalSpace R
inst_3 : IsValuativeTopology R
γ : ValueGroupWithZero R
hγ : γ ≠ 0
⊢ True ∧
    Subset.{u_1} (α := Set R)
      {x : R | (valuation R : (a : R) → ValueGroupWithZero R) x < (↑(Units.mk0 γ hγ) : ValueGroupWithZero R)}
      {x : R | (valuation R : (a : R) → ValueGroupWithZero R) x < γ}

Tactic:
simp
-- Module: Mathlib.Topology.Algebra.ValuativeRel.ValuativeTopology
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
Γ₀ : Type u_3
inst_2 : LinearOrderedCommGroupWithZero Γ₀
inst_3 : TopologicalSpace R
inst_4 : IsValuativeTopology R
v : Valuation R Γ₀
inst_5 : v.Compatible
s : Set R
x : R
⊢ s ∈ 𝓝 x ↔
    ∃ (γ : (ValueGroupWithZero R)ˣ),
      (fun (x_1 : R) ↦ x + x_1) ''
          {z : R | (valuation R : (a : R) → ValueGroupWithZero R) z < (↑γ : ValueGroupWithZero R)} ⊆
        s

Tactic:
IsValuativeTopology.mem_nhds_iff (s := s)

Premises used: IsValuativeTopology.mem_nhds_iff
-- Module: Mathlib.Topology.Algebra.ValuativeRel.ValuativeTopology
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
Γ₀ : Type u_3
inst_2 : LinearOrderedCommGroupWithZero Γ₀
inst_3 : TopologicalSpace R
inst_4 : IsValuativeTopology R
v : Valuation R Γ₀
inst_5 : v.Compatible
s : Set R
x : R
h :
  (∃ (γ : (ValueGroup₀ v)ˣ),
      {z : R | (v.restrict : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) (z - x) < (↑γ : ValueGroup₀ v)} ⊆ s) ↔
    ∃ (γ : (ValueGroupWithZero R)ˣ),
      (fun (x_1 : R) ↦ x + x_1) ''
          {z : R | (valuation R : (a : R) → ValueGroupWithZero R) z < (↑γ : ValueGroupWithZero R)} ⊆
        s
⊢ s ∈ 𝓝 x ↔
    ∃ (γ : (ValueGroup₀ v)ˣ),
      {z : R | (v.restrict : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) (z - x) < (↑γ : ValueGroup₀ v)} ⊆ s

Tactic:
convert! IsValuativeTopology.mem_nhds_iff (s := s) using 4

Premises used: IsValuativeTopology.mem_nhds_iff
-- Module: Mathlib.Topology.Algebra.ValuativeRel.ValuativeTopology
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
Γ₀ : Type u_3
inst_2 : LinearOrderedCommGroupWithZero Γ₀
inst_3 : TopologicalSpace R
inst_4 : IsValuativeTopology R
v : Valuation R Γ₀
inst_5 : v.Compatible
s : Set R
x : R
⊢ (∃ (γ : (ValueGroup₀ v)ˣ),
      {z : R | (v.restrict : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) (z - x) < (↑γ : ValueGroup₀ v)} ⊆ s) ↔
    ∃ (γ : (ValueGroupWithZero R)ˣ),
      (fun (x_1 : R) ↦ x + x_1) ''
          {z : R | (valuation R : (a : R) → ValueGroupWithZero R) z < (↑γ : ValueGroupWithZero R)} ⊆
        s

Tactic:
simpa [neg_add_eq_sub] using v.exists_setOf_restrict_le_iff _ _

Premises used: neg_add_eq_sub, Valuation.exists_setOf_restrict_le_iff
-- Module: Mathlib.Topology.Algebra.ValuativeRel.ValuativeTopology
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
Γ₀ : Type u_3
inst_2 : LinearOrderedCommGroupWithZero Γ₀
inst_3 : TopologicalSpace R
inst_4 : IsValuativeTopology R
v : Valuation R Γ₀
inst_5 : v.Compatible
s : Set R
⊢ Membership.mem (γ := Filter R) (𝓝 0) s ↔
    ∃ (γ : (ValueGroup₀ v)ˣ),
      {x : R | (v.restrict : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) x < (↑γ : ValueGroup₀ v)} ⊆ s

Tactic:
simp [v.mem_nhds_iff]

Premises used: Valuation.mem_nhds_iff
-- Module: Mathlib.Topology.Algebra.ValuativeRel.ValuativeTopology
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
Γ₀ : Type u_3
inst_2 : LinearOrderedCommGroupWithZero Γ₀
inst_3 : TopologicalSpace R
inst_4 : IsValuativeTopology R
v : Valuation R Γ₀
inst_5 : v.Compatible
x : R
⊢ (𝓝 x).HasBasis (fun (x : (ValueGroup₀ v)ˣ) ↦ True) fun (γ : (ValueGroup₀ v)ˣ) ↦
    {z : R | (v.restrict : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) (z - x) < (↑γ : ValueGroup₀ v)}

Tactic:
simp [Filter.hasBasis_iff, v.mem_nhds_iff]

Premises used: Filter.hasBasis_iff, Valuation.mem_nhds_iff
-- Module: Mathlib.Topology.Algebra.ValuativeRel.ValuativeTopology
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
Γ₀ : Type u_3
inst_2 : LinearOrderedCommGroupWithZero Γ₀
inst_3 : TopologicalSpace R
inst_4 : IsValuativeTopology R
v : Valuation R Γ₀
inst_5 : v.Compatible
⊢ HasBasis.{u_1, u_3 + 1} (α := R) (𝓝 0) (fun (x : (ValueGroup₀ v)ˣ) ↦ True) fun (γ : (ValueGroup₀ v)ˣ) ↦
    {x : R | (v.restrict : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) x < (↑γ : ValueGroup₀ v)}

Tactic:
simp [Filter.hasBasis_iff, v.is_topological_valuation]

Premises used: Filter.hasBasis_iff, Valuation.is_topological_valuation
-- Module: Mathlib.Topology.Algebra.ValuativeRel.ValuativeTopology
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
Γ₀ : Type u_3
inst_2 : LinearOrderedCommGroupWithZero Γ₀
inst_3 : TopologicalSpace R
inst_4 : IsValuativeTopology R
v : Valuation R Γ₀
inst_5 : v.Compatible
x : R
h : Ne.{u_3 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) (0 : Γ₀)
rw :
  ∃ (γ : (ValueGroup₀ v)ˣ),
    Subset.{u_1} (α := Set R)
      {z : R | (v.restrict : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) (z - x) < (↑γ : ValueGroup₀ v)}
      {y : R | Eq.{u_3 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) y : Γ₀) ((v : (a : R) → Γ₀) x : Γ₀)}
⊢ {y : R | Eq.{u_3 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) y : Γ₀) ((v : (a : R) → Γ₀) x : Γ₀)} ∈ 𝓝 x

Tactic:
rw [v.mem_nhds_iff]

Premises used: Valuation.mem_nhds_iff
-- Module: Mathlib.Topology.Algebra.ValuativeRel.ValuativeTopology
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
Γ₀ : Type u_3
inst_2 : LinearOrderedCommGroupWithZero Γ₀
inst_3 : TopologicalSpace R
inst_4 : IsValuativeTopology R
v : Valuation R Γ₀
inst_5 : v.Compatible
x : R
h : Ne.{u_3 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) (0 : Γ₀)
⊢ Ne.{u_3 + 1} (α := ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
    ((v.restrict : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) x : ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
    (0 : ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))

Tactic:
simp [h]