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_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:
have h' : v.restrict x ≠ 0 := by simp [h]
-- 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 : Γ₀)
h' :
  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 →*₀ Γ₀))
h₁ :
  Subset.{u_1} (α := Set R)
    {z : R |
      LT.lt.{u_3} (α := ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
        ((v.restrict : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) (z - x) : ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
        ((↑(Units.mk0 ((v.restrict : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) x) h') : ValueGroup₀ v) : ValueGroup₀ v)}
    {y : R | Eq.{u_3 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) y : Γ₀) ((v : (a : R) → Γ₀) x : Γ₀)}
⊢ ∃ (γ : (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 : Γ₀)}

Tactic:
use Units.mk0 _ h'

Premises used: Units.mk0
-- 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 : Γ₀)
h' :
  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 →*₀ Γ₀))
y : R
y_in :
  Membership.mem (γ := Set R)
    {z : R |
      LT.lt.{u_3} (α := ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
        ((v.restrict : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) (z - x) : ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
        ((v.restrict : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) x : ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))}
    y
⊢ Membership.mem (γ := Set R) {y : R | Eq.{u_3 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) y : Γ₀) ((v : (a : R) → Γ₀) x : Γ₀)} y

Tactic:
Valuation.map_eq_of_sub_lt _ (v.restrict_lt_iff.mp y_in)

Premises used: Set.Mem, setOf, Iff.mp, Valuation.map_eq_of_sub_lt, Valuation.restrict_lt_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 : Γ₀)
h' :
  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 →*₀ Γ₀))
y : R
y_in :
  Membership.mem (γ := Set R)
    {z : R |
      LT.lt.{u_3} (α := ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
        ((v.restrict : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) (z - x) : ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
        ((v.restrict : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) x : ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))}
    y
⊢ Membership.mem (γ := Set R) {y : R | Eq.{u_3 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) y : Γ₀) ((v : (a : R) → Γ₀) x : Γ₀)} y

Tactic:
exact Valuation.map_eq_of_sub_lt _ (v.restrict_lt_iff.mp y_in)

Premises used: Iff.mp, Valuation.map_eq_of_sub_lt, Valuation.restrict_lt_iff
-- Module: Mathlib.Topology.Algebra.ValuativeRel.ValuativeTopology
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
K : Type u_2
inst_2 : Field K
inst_3 : ValuativeRel K
Γ₀ : Type u_3
inst_4 : LinearOrderedCommGroupWithZero Γ₀
inst_5 : TopologicalSpace R
inst_6 : IsValuativeTopology R
v : Valuation R Γ₀
inst_7 : v.Compatible
x z : R
γ : (ValueGroup₀ (F := Valuation R (ValueGroupWithZero R)) (valuation R))ˣ
h : True
y : R
hy :
  Membership.mem (γ := Set R)
    {z_1 : R |
      (Valuation.restrict (valuation R) : (a : R) → ValueGroup₀ (↑(valuation R) : R →*₀ ValueGroupWithZero R))
          (z_1 - z) <
        (↑γ : ValueGroup₀ (valuation R))}
    y
⊢ Membership.mem (γ := Set R)
    {z_1 : R |
      (Valuation.restrict (valuation R) : (a : R) → ValueGroup₀ (↑(valuation R) : R →*₀ ValueGroupWithZero R))
          (z_1 - (x + z)) <
        (↑γ : ValueGroup₀ (valuation R))}
    (x +ᵥ y)

Tactic:
simpa using hy
-- Module: Mathlib.Topology.Algebra.ValuativeRel.ValuativeTopology
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
K : Type u_2
inst_2 : Field K
inst_3 : ValuativeRel K
Γ₀ : Type u_3
inst_4 : LinearOrderedCommGroupWithZero Γ₀
inst_5 : TopologicalSpace R
inst_6 : IsValuativeTopology R
v : Valuation R Γ₀
inst_7 : v.Compatible
⊢ ContinuousConstVAdd R R

Tactic:
have cts_add : ContinuousConstVAdd R R :=
    ⟨fun x ↦ continuous_iff_continuousAt.2 fun z ↦
      (((valuation R).hasBasis_nhds z).tendsto_iff ((valuation R).hasBasis_nhds (x + z))).2
        fun γ _ ↦ ⟨γ, trivial, fun y hy ↦ by simpa using hy⟩⟩
-- Module: Mathlib.Topology.Algebra.ValuativeRel.ValuativeTopology
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
K : Type u_2
inst_2 : Field K
inst_3 : ValuativeRel K
Γ₀ : Type u_3
inst_4 : LinearOrderedCommGroupWithZero Γ₀
inst_5 : TopologicalSpace R
inst_6 : IsValuativeTopology R
v : Valuation R Γ₀
inst_7 : v.Compatible
cts_add : ContinuousConstVAdd R R
⊢ HasBasis (α := R) (𝓝 0) (fun (x : (ValueGroup₀ (F := Valuation R (ValueGroupWithZero R)) (valuation R))ˣ) ↦ True)
    fun (γ : (ValueGroup₀ (F := Valuation R (ValueGroupWithZero R)) (valuation R))ˣ) ↦
    {x : R |
      (Valuation.restrict (valuation R) : (a : R) → ValueGroup₀ (↑(valuation R) : R →*₀ ValueGroupWithZero R)) x <
        (↑γ : ValueGroup₀ (valuation R))}

Tactic:
have basis := (valuation R).hasBasis_nhds_zero
-- Module: Mathlib.Topology.Algebra.ValuativeRel.ValuativeTopology
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
K : Type u_2
inst_2 : Field K
inst_3 : ValuativeRel K
Γ₀ : Type u_3
inst_4 : LinearOrderedCommGroupWithZero Γ₀
inst_5 : TopologicalSpace R
inst_6 : IsValuativeTopology R
v : Valuation R Γ₀
inst_7 : v.Compatible
cts_add : ContinuousConstVAdd R R
basis :
  HasBasis (α := R) (𝓝 0) (fun (x : (ValueGroup₀ (F := Valuation R (ValueGroupWithZero R)) (valuation R))ˣ) ↦ True)
    fun (γ : (ValueGroup₀ (F := Valuation R (ValueGroupWithZero R)) (valuation R))ˣ) ↦
    {x : R |
      (Valuation.restrict (valuation R) : (a : R) → ValueGroup₀ (↑(valuation R) : R →*₀ ValueGroupWithZero R)) x <
        (↑γ : ValueGroup₀ (valuation R))}
⊢ IsTopologicalAddGroup R

Tactic:
.of_comm_of_nhds_zero ?_ ?_ fun x₀ ↦ (map_eq_of_inverse (-x₀ + ·) ?_ ?_ ?_).symm

Premises used: IsTopologicalAddGroup.of_comm_of_nhds_zero, Filter.map_eq_of_inverse, HAdd.hAdd, Eq.symm, Neg.neg
-- Module: Mathlib.Topology.Algebra.ValuativeRel.ValuativeTopology
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
K : Type u_2
inst_2 : Field K
inst_3 : ValuativeRel K
Γ₀ : Type u_3
inst_4 : LinearOrderedCommGroupWithZero Γ₀
inst_5 : TopologicalSpace R
inst_6 : IsValuativeTopology R
v : Valuation R Γ₀
inst_7 : v.Compatible
cts_add : ContinuousConstVAdd R R
basis :
  HasBasis (α := R) (𝓝 0) (fun (x : (ValueGroup₀ (F := Valuation R (ValueGroupWithZero R)) (valuation R))ˣ) ↦ True)
    fun (γ : (ValueGroup₀ (F := Valuation R (ValueGroupWithZero R)) (valuation R))ˣ) ↦
    {x : R |
      (Valuation.restrict (valuation R) : (a : R) → ValueGroup₀ (↑(valuation R) : R →*₀ ValueGroupWithZero R)) x <
        (↑γ : ValueGroup₀ (valuation R))}
refine_1 :
  Tendsto (β := R) (Function.uncurry fun (x1 x2 : R) ↦ x1 + x2)
    (SProd.sprod (α := Filter R) (β := Filter R) (𝓝 0) (𝓝 0)) (𝓝 0)
refine_2 : Tendsto (β := R) (fun (x : R) ↦ -x) (𝓝 0) (𝓝 0)
refine_3 : ∀ (x₀ : R), Eq.{u_1 + 1} (α := R → R) ((fun (x : R) ↦ x₀ + x) ∘ fun (x : R) ↦ -x₀ + x) _root_.id
refine_4 : ∀ (x₀ : R), Tendsto (fun (x : R) ↦ x₀ + x) (𝓝 0) (𝓝 x₀)
refine_5 : ∀ (x₀ : R), Tendsto (β := R) (fun (x : R) ↦ -x₀ + x) (𝓝 x₀) (𝓝 0)
⊢ IsTopologicalAddGroup R

Tactic:
refine .of_comm_of_nhds_zero ?_ ?_ fun x₀ ↦ (map_eq_of_inverse (-x₀ + ·) ?_ ?_ ?_).symm
-- Module: Mathlib.Topology.Algebra.ValuativeRel.ValuativeTopology
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
K : Type u_2
inst_2 : Field K
inst_3 : ValuativeRel K
Γ₀ : Type u_3
inst_4 : LinearOrderedCommGroupWithZero Γ₀
inst_5 : TopologicalSpace R
inst_6 : IsValuativeTopology R
v : Valuation R Γ₀
inst_7 : v.Compatible
cts_add : ContinuousConstVAdd R R
basis :
  HasBasis (α := R) (𝓝 0) (fun (x : (ValueGroup₀ (F := Valuation R (ValueGroupWithZero R)) (valuation R))ˣ) ↦ True)
    fun (γ : (ValueGroup₀ (F := Valuation R (ValueGroupWithZero R)) (valuation R))ˣ) ↦
    {x : R |
      (Valuation.restrict (valuation R) : (a : R) → ValueGroup₀ (↑(valuation R) : R →*₀ ValueGroupWithZero R)) x <
        (↑γ : ValueGroup₀ (valuation R))}
⊢ Tendsto (β := R) (Function.uncurry fun (x1 x2 : R) ↦ x1 + x2)
    (SProd.sprod (α := Filter R) (β := Filter R) (𝓝 0) (𝓝 0)) (𝓝 0)

Tactic:
(basis.prod_self.tendsto_iff basis).2 fun γ _ ↦
      ⟨γ, trivial, fun ⟨_, _⟩ hx ↦ (valuation R).restrict.map_add_lt hx.left hx.right⟩

Premises used: _private.0.IsValuativeTopology.instIsTopologicalAddGroup.match_1, Iff.mpr, Units.val, trivial, Filter.HasBasis.tendsto_iff, Set.Mem, Filter.HasBasis.prod_self, setOf, Membership.mem, Valuation.map_add_lt, And.right, And.left, HAdd.hAdd, And.intro, LT.lt, Exists.intro, ValuativeRel.valuation, Function.uncurry, DFunLike.coe, Valuation.restrict
-- Module: Mathlib.Topology.Algebra.ValuativeRel.ValuativeTopology
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
K : Type u_2
inst_2 : Field K
inst_3 : ValuativeRel K
Γ₀ : Type u_3
inst_4 : LinearOrderedCommGroupWithZero Γ₀
inst_5 : TopologicalSpace R
inst_6 : IsValuativeTopology R
v : Valuation R Γ₀
inst_7 : v.Compatible
cts_add : ContinuousConstVAdd R R
basis :
  HasBasis (α := R) (𝓝 0) (fun (x : (ValueGroup₀ (F := Valuation R (ValueGroupWithZero R)) (valuation R))ˣ) ↦ True)
    fun (γ : (ValueGroup₀ (F := Valuation R (ValueGroupWithZero R)) (valuation R))ˣ) ↦
    {x : R |
      (Valuation.restrict (valuation R) : (a : R) → ValueGroup₀ (↑(valuation R) : R →*₀ ValueGroupWithZero R)) x <
        (↑γ : ValueGroup₀ (valuation R))}
⊢ Tendsto (β := R) (Function.uncurry fun (x1 x2 : R) ↦ x1 + x2)
    (SProd.sprod (α := Filter R) (β := Filter R) (𝓝 0) (𝓝 0)) (𝓝 0)

Tactic:
exact (basis.prod_self.tendsto_iff basis).2 fun γ _ ↦
      ⟨γ, trivial, fun ⟨_, _⟩ hx ↦ (valuation R).restrict.map_add_lt hx.left hx.right⟩

Premises used: _private.0.IsValuativeTopology.instIsTopologicalAddGroup.match_1, Iff.mpr, Units.val, trivial, Filter.HasBasis.tendsto_iff, Filter.HasBasis.prod_self, setOf, Membership.mem, And.intro, LT.lt, Exists.intro, ValuativeRel.valuation, DFunLike.coe, Valuation.restrict
-- Module: Mathlib.Topology.Algebra.ValuativeRel.ValuativeTopology
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
K : Type u_2
inst_2 : Field K
inst_3 : ValuativeRel K
Γ₀ : Type u_3
inst_4 : LinearOrderedCommGroupWithZero Γ₀
inst_5 : TopologicalSpace R
inst_6 : IsValuativeTopology R
v : Valuation R Γ₀
inst_7 : v.Compatible
cts_add : ContinuousConstVAdd R R
basis :
  HasBasis (α := R) (𝓝 0) (fun (x : (ValueGroup₀ (F := Valuation R (ValueGroupWithZero R)) (valuation R))ˣ) ↦ True)
    fun (γ : (ValueGroup₀ (F := Valuation R (ValueGroupWithZero R)) (valuation R))ˣ) ↦
    {x : R |
      (Valuation.restrict (valuation R) : (a : R) → ValueGroup₀ (↑(valuation R) : R →*₀ ValueGroupWithZero R)) x <
        (↑γ : ValueGroup₀ (valuation R))}
γ : (ValueGroup₀ (F := Valuation R (ValueGroupWithZero R)) (valuation R))ˣ
h : True
y : R
hy :
  Membership.mem (γ := Set R)
    {x : R |
      (Valuation.restrict (valuation R) : (a : R) → ValueGroup₀ (↑(valuation R) : R →*₀ ValueGroupWithZero R)) x <
        (↑γ : ValueGroup₀ (valuation R))}
    y
⊢ Membership.mem (γ := Set R)
    {x : R |
      (Valuation.restrict (valuation R) : (a : R) → ValueGroup₀ (↑(valuation R) : R →*₀ ValueGroupWithZero R)) x <
        (↑γ : ValueGroup₀ (valuation R))}
    (-y)

Tactic:
simpa using hy
-- Module: Mathlib.Topology.Algebra.ValuativeRel.ValuativeTopology
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
K : Type u_2
inst_2 : Field K
inst_3 : ValuativeRel K
Γ₀ : Type u_3
inst_4 : LinearOrderedCommGroupWithZero Γ₀
inst_5 : TopologicalSpace R
inst_6 : IsValuativeTopology R
v : Valuation R Γ₀
inst_7 : v.Compatible
cts_add : ContinuousConstVAdd R R
basis :
  HasBasis (α := R) (𝓝 0) (fun (x : (ValueGroup₀ (F := Valuation R (ValueGroupWithZero R)) (valuation R))ˣ) ↦ True)
    fun (γ : (ValueGroup₀ (F := Valuation R (ValueGroupWithZero R)) (valuation R))ˣ) ↦
    {x : R |
      (Valuation.restrict (valuation R) : (a : R) → ValueGroup₀ (↑(valuation R) : R →*₀ ValueGroupWithZero R)) x <
        (↑γ : ValueGroup₀ (valuation R))}
⊢ Tendsto (β := R) (fun (x : R) ↦ -x) (𝓝 0) (𝓝 0)

Tactic:
exact (basis.tendsto_iff basis).2 fun γ _ ↦ ⟨γ, trivial, fun y hy ↦ by simpa using hy⟩

Premises used: Iff.mpr, trivial, Filter.HasBasis.tendsto_iff, And.intro, Exists.intro
-- Module: Mathlib.Topology.Algebra.ValuativeRel.ValuativeTopology
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
K : Type u_2
inst_2 : Field K
inst_3 : ValuativeRel K
Γ₀ : Type u_3
inst_4 : LinearOrderedCommGroupWithZero Γ₀
inst_5 : TopologicalSpace R
inst_6 : IsValuativeTopology R
v : Valuation R Γ₀
inst_7 : v.Compatible
cts_add : ContinuousConstVAdd R R
basis :
  HasBasis (α := R) (𝓝 0) (fun (x : (ValueGroup₀ (F := Valuation R (ValueGroupWithZero R)) (valuation R))ˣ) ↦ True)
    fun (γ : (ValueGroup₀ (F := Valuation R (ValueGroupWithZero R)) (valuation R))ˣ) ↦
    {x : R |
      (Valuation.restrict (valuation R) : (a : R) → ValueGroup₀ (↑(valuation R) : R →*₀ ValueGroupWithZero R)) x <
        (↑γ : ValueGroup₀ (valuation R))}
x₀ : R
refine_3 : ∀ (x : R), ((fun (x : R) ↦ x₀ + x) ∘ fun (x : R) ↦ -x₀ + x) x = _root_.id x
⊢ Eq.{u_1 + 1} (α := R → R) ((fun (x : R) ↦ x₀ + x) ∘ fun (x : R) ↦ -x₀ + x) _root_.id

Tactic:
ext
-- Module: Mathlib.Topology.Algebra.ValuativeRel.ValuativeTopology
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
K : Type u_2
inst_2 : Field K
inst_3 : ValuativeRel K
Γ₀ : Type u_3
inst_4 : LinearOrderedCommGroupWithZero Γ₀
inst_5 : TopologicalSpace R
inst_6 : IsValuativeTopology R
v : Valuation R Γ₀
inst_7 : v.Compatible
cts_add : ContinuousConstVAdd R R
basis :
  HasBasis (α := R) (𝓝 0) (fun (x : (ValueGroup₀ (F := Valuation R (ValueGroupWithZero R)) (valuation R))ˣ) ↦ True)
    fun (γ : (ValueGroup₀ (F := Valuation R (ValueGroupWithZero R)) (valuation R))ˣ) ↦
    {x : R |
      (Valuation.restrict (valuation R) : (a : R) → ValueGroup₀ (↑(valuation R) : R →*₀ ValueGroupWithZero R)) x <
        (↑γ : ValueGroup₀ (valuation R))}
x₀ x : R
⊢ ((fun (x : R) ↦ x₀ + x) ∘ fun (x : R) ↦ -x₀ + x) x = _root_.id x

Tactic:
simp
-- Module: Mathlib.Topology.Algebra.ValuativeRel.ValuativeTopology
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
K : Type u_2
inst_2 : Field K
inst_3 : ValuativeRel K
Γ₀ : Type u_3
inst_4 : LinearOrderedCommGroupWithZero Γ₀
inst_5 : TopologicalSpace R
inst_6 : IsValuativeTopology R
v : Valuation R Γ₀
inst_7 : v.Compatible
cts_add : ContinuousConstVAdd R R
basis :
  HasBasis (α := R) (𝓝 0) (fun (x : (ValueGroup₀ (F := Valuation R (ValueGroupWithZero R)) (valuation R))ˣ) ↦ True)
    fun (γ : (ValueGroup₀ (F := Valuation R (ValueGroupWithZero R)) (valuation R))ˣ) ↦
    {x : R |
      (Valuation.restrict (valuation R) : (a : R) → ValueGroup₀ (↑(valuation R) : R →*₀ ValueGroupWithZero R)) x <
        (↑γ : ValueGroup₀ (valuation R))}
x₀ : R
⊢ Tendsto (fun (x : R) ↦ x₀ + x) (𝓝 0) (𝓝 x₀)

Tactic:
simpa [ContinuousAt] using (cts_add.1 x₀).continuousAt (x := 0)

Premises used: ContinuousAt, ContinuousConstVAdd.continuous_const_vadd, Continuous.continuousAt
-- Module: Mathlib.Topology.Algebra.ValuativeRel.ValuativeTopology
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
K : Type u_2
inst_2 : Field K
inst_3 : ValuativeRel K
Γ₀ : Type u_3
inst_4 : LinearOrderedCommGroupWithZero Γ₀
inst_5 : TopologicalSpace R
inst_6 : IsValuativeTopology R
v : Valuation R Γ₀
inst_7 : v.Compatible
cts_add : ContinuousConstVAdd R R
basis :
  HasBasis (α := R) (𝓝 0) (fun (x : (ValueGroup₀ (F := Valuation R (ValueGroupWithZero R)) (valuation R))ˣ) ↦ True)
    fun (γ : (ValueGroup₀ (F := Valuation R (ValueGroupWithZero R)) (valuation R))ˣ) ↦
    {x : R |
      (Valuation.restrict (valuation R) : (a : R) → ValueGroup₀ (↑(valuation R) : R →*₀ ValueGroupWithZero R)) x <
        (↑γ : ValueGroup₀ (valuation R))}
x₀ : R
⊢ Tendsto (β := R) (fun (x : R) ↦ -x₀ + x) (𝓝 x₀) (𝓝 0)

Tactic:
simpa [ContinuousAt] using (cts_add.1 (-x₀)).continuousAt (x := x₀)

Premises used: ContinuousAt, ContinuousConstVAdd.continuous_const_vadd, Continuous.continuousAt, Neg.neg
-- Module: Mathlib.Topology.Algebra.ValuativeRel.ValuativeTopology
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
Γ₀ : Type u_3
inst_2 : LinearOrderedCommGroupWithZero Γ₀
_u : UniformSpace R
inst_3 : IsUniformAddGroup R
inst_4 : IsValuativeTopology R
v : Valuation R Γ₀
inst_5 : v.Compatible
rw :
  HasBasis.{u_1, u_3 + 1} (α := R × R) (Filter.comap (β := R) (fun (x : R × R) ↦ x.2 - x.1) (𝓝 0))
    (fun (x : (ValueGroup₀ v)ˣ) ↦ True) fun (γ : (ValueGroup₀ v)ˣ) ↦
    {p : R × R | (v.restrict : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) (p.2 - p.1) < (↑γ : ValueGroup₀ v)}
⊢ (𝓤 R).HasBasis (fun (x : (ValueGroup₀ v)ˣ) ↦ True) fun (γ : (ValueGroup₀ v)ˣ) ↦
    {p : R × R | (v.restrict : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) (p.2 - p.1) < (↑γ : ValueGroup₀ v)}

Tactic:
rw [uniformity_eq_comap_nhds_zero]

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

Tactic:
v.hasBasis_nhds_zero.comap _

Premises used: Set.Mem, Valuation.hasBasis_nhds_zero, setOf, Filter.HasBasis.comap, Set.preimage
-- Module: Mathlib.Topology.Algebra.ValuativeRel.ValuativeTopology
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
Γ₀ : Type u_3
inst_2 : LinearOrderedCommGroupWithZero Γ₀
_u : UniformSpace R
inst_3 : IsUniformAddGroup R
inst_4 : IsValuativeTopology R
v : Valuation R Γ₀
inst_5 : v.Compatible
⊢ HasBasis.{u_1, u_3 + 1} (α := R × R) (Filter.comap (β := R) (fun (x : R × R) ↦ x.2 - x.1) (𝓝 0))
    (fun (x : (ValueGroup₀ v)ˣ) ↦ True) fun (γ : (ValueGroup₀ v)ˣ) ↦
    {p : R × R | (v.restrict : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) (p.2 - p.1) < (↑γ : ValueGroup₀ v)}

Tactic:
exact v.hasBasis_nhds_zero.comap _

Premises used: Valuation.hasBasis_nhds_zero, Filter.HasBasis.comap
-- Module: Mathlib.Topology.Algebra.ValuativeRel.ValuativeTopology
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
Γ₀ : Type u_3
inst_2 : LinearOrderedCommGroupWithZero Γ₀
_u : UniformSpace R
inst_3 : IsUniformAddGroup R
inst_4 : IsValuativeTopology R
v : Valuation R Γ₀
inst_5 : v.Compatible
⊢ _u = IsTopologicalAddGroup.rightUniformSpace R

Tactic:
UniformSpace.ext (v.hasBasis_uniformity.eq_of_same_basis ?_)

Premises used: UniformSpace.ext, Valuation.hasBasis_uniformity, Filter.HasBasis.eq_of_same_basis
-- Module: Mathlib.Topology.Algebra.ValuativeRel.ValuativeTopology
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
Γ₀ : Type u_3
inst_2 : LinearOrderedCommGroupWithZero Γ₀
_u : UniformSpace R
inst_3 : IsUniformAddGroup R
inst_4 : IsValuativeTopology R
v : Valuation R Γ₀
inst_5 : v.Compatible
refine :
  (𝓤 R).HasBasis (fun (x : (ValueGroup₀ v)ˣ) ↦ True) fun (γ : (ValueGroup₀ v)ˣ) ↦
    {p : R × R | (v.restrict : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) (p.2 - p.1) < (↑γ : ValueGroup₀ v)}
⊢ _u = IsTopologicalAddGroup.rightUniformSpace R

Tactic:
refine UniformSpace.ext (v.hasBasis_uniformity.eq_of_same_basis ?_)

Premises used: UniformSpace.ext, Valuation.hasBasis_uniformity, Filter.HasBasis.eq_of_same_basis
-- Module: Mathlib.Topology.Algebra.ValuativeRel.ValuativeTopology
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
Γ₀ : Type u_3
inst_2 : LinearOrderedCommGroupWithZero Γ₀
_u : UniformSpace R
inst_3 : IsUniformAddGroup R
inst_4 : IsValuativeTopology R
v : Valuation R Γ₀
inst_5 : v.Compatible
⊢ HasBasis.{u_1, u_3 + 1} (α := R × R) (Filter.comap (β := R) (fun (p : R × R) ↦ p.2 + -p.1) (𝓝 0))
    (fun (x : (ValueGroup₀ v)ˣ) ↦ True) fun (i : (ValueGroup₀ v)ˣ) ↦
    (fun (p : R × R) ↦ p.2 + -p.1) ⁻¹'
      (↑(v.ltAddSubgroup ((Units.map (↑embedding : ValueGroup₀ v →* Γ₀) : (a : (ValueGroup₀ v)ˣ) → Γ₀ˣ) i)) : Set R)

Tactic:
v.subgroups_basis.hasBasis_nhds_zero.comap _

Premises used: RingSubgroupsBasis.hasBasis_nhds_zero, Valuation.subgroups_basis, Filter.HasBasis.comap
-- Module: Mathlib.Topology.Algebra.ValuativeRel.ValuativeTopology
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
Γ₀ : Type u_3
inst_2 : LinearOrderedCommGroupWithZero Γ₀
_u : UniformSpace R
inst_3 : IsUniformAddGroup R
inst_4 : IsValuativeTopology R
v : Valuation R Γ₀
inst_5 : v.Compatible
h :
  ∀ (x : (ValueGroup₀ v)ˣ),
    Eq (α := Set (R × R))
      {p : R × R | (v.restrict : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) (p.2 - p.1) < (↑x : ValueGroup₀ v)}
      ((fun (p : R × R) ↦ p.2 + -p.1) ⁻¹'
        (↑(v.ltAddSubgroup ((Units.map (↑embedding : ValueGroup₀ v →* Γ₀) : (a : (ValueGroup₀ v)ˣ) → Γ₀ˣ) x)) : Set R))
⊢ (𝓤 R).HasBasis (fun (x : (ValueGroup₀ v)ˣ) ↦ True) fun (γ : (ValueGroup₀ v)ˣ) ↦
    {p : R × R | (v.restrict : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) (p.2 - p.1) < (↑γ : ValueGroup₀ v)}

Tactic:
convert! v.subgroups_basis.hasBasis_nhds_zero.comap _

Premises used: RingSubgroupsBasis.hasBasis_nhds_zero, Valuation.subgroups_basis, Filter.HasBasis.comap
-- Module: Mathlib.Topology.Algebra.ValuativeRel.ValuativeTopology
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
Γ₀ : Type u_3
inst_2 : LinearOrderedCommGroupWithZero Γ₀
_u : UniformSpace R
inst_3 : IsUniformAddGroup R
inst_4 : IsValuativeTopology R
v : Valuation R Γ₀
inst_5 : v.Compatible
x : (ValueGroup₀ v)ˣ
⊢ Eq (α := Set (R × R))
    {p : R × R | (v.restrict : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) (p.2 - p.1) < (↑x : ValueGroup₀ v)}
    ((fun (p : R × R) ↦ p.2 + -p.1) ⁻¹'
      (↑(v.ltAddSubgroup ((Units.map (↑embedding : ValueGroup₀ v →* Γ₀) : (a : (ValueGroup₀ v)ˣ) → Γ₀ˣ) x)) : Set R))

Tactic:
simp [restrict_lt_iff_lt_embedding, sub_eq_add_neg]

Premises used: Valuation.restrict_lt_iff_lt_embedding, sub_eq_add_neg