awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Algebra.Valued.ValuationTopology
Goal:
R : Type u
inst : Ring R
Γ₀ : Type v
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
x : R
γ : (ValueGroup₀ v)ˣ
γx : Γ₀ˣ
Hx : (v : (a : R) → Γ₀) x = (↑γx : Γ₀)
u : (ValueGroup₀ v)ˣ :=
  Units.mk0 (((restrict₀ v : MonoidWithZeroHom.{u, v} R (ValueGroup₀ v)) : (a : R) → ValueGroup₀ v) x) ⋯
hu_def : u = Units.mk0 (((restrict₀ v : MonoidWithZeroHom.{u, v} R (ValueGroup₀ v)) : (a : R) → ValueGroup₀ v) x) ⋯
⊢ (embedding : (a : ValueGroup₀ v) → Γ₀) (↑u⁻¹ : ValueGroup₀ v) = (↑γx⁻¹ : Γ₀)

Tactic:
simp [restrict₀_apply, embedding_apply,
          hu_def, Hx]

Premises used: MonoidWithZeroHom.ValueGroup₀.embedding_apply, MonoidWithZeroHom.ValueGroup₀.restrict₀_apply
-- Module: Mathlib.Topology.Algebra.Valued.ValuationTopology
Goal:
R : Type u
inst : Ring R
Γ₀ : Type v
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
x : R
γ : (ValueGroup₀ v)ˣ
γx : Γ₀ˣ
Hx : (v : (a : R) → Γ₀) x = (↑γx : Γ₀)
u : (ValueGroup₀ v)ˣ :=
  Units.mk0 (((restrict₀ v : MonoidWithZeroHom.{u, v} R (ValueGroup₀ v)) : (a : R) → ValueGroup₀ v) x) ⋯
hu_def : u = Units.mk0 (((restrict₀ v : MonoidWithZeroHom.{u, v} R (ValueGroup₀ v)) : (a : R) → ValueGroup₀ v) x) ⋯
⊢ (embedding : (a : ValueGroup₀ v) → Γ₀) (↑u⁻¹ : ValueGroup₀ v) = (↑γx⁻¹ : Γ₀)

Tactic:
have hu : ValueGroup₀.embedding u⁻¹.1 = γx⁻¹ := by simp [restrict₀_apply, embedding_apply,
          hu_def, Hx]
-- Module: Mathlib.Topology.Algebra.Valued.ValuationTopology
Goal:
R : Type u
inst : Ring R
Γ₀ : Type v
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
x : R
γ : (ValueGroup₀ v)ˣ
γx : Γ₀ˣ
Hx : (v : (a : R) → Γ₀) x = (↑γx : Γ₀)
u : (ValueGroup₀ v)ˣ :=
  Units.mk0 (((restrict₀ v : MonoidWithZeroHom.{u, v} R (ValueGroup₀ v)) : (a : R) → ValueGroup₀ v) x) ⋯
hu_def : u = Units.mk0 (((restrict₀ v : MonoidWithZeroHom.{u, v} R (ValueGroup₀ v)) : (a : R) → ValueGroup₀ v) x) ⋯
hu : (embedding : (a : ValueGroup₀ v) → Γ₀) (↑u⁻¹ : ValueGroup₀ v) = (↑γx⁻¹ : Γ₀)
h :
  (↑(v.ltAddSubgroup ((Units.map (↑embedding : ValueGroup₀ v →* Γ₀) : (a : (ValueGroup₀ v)ˣ) → Γ₀ˣ) (u⁻¹ * γ))) :
      Set R) ⊆
    (fun (x_1 : R) ↦ x_1 * x) ⁻¹'
      (↑(v.ltAddSubgroup ((Units.map (↑embedding : ValueGroup₀ v →* Γ₀) : (a : (ValueGroup₀ v)ˣ) → Γ₀ˣ) γ)) : Set R)
⊢ ∃ (j : (ValueGroup₀ v)ˣ),
    (↑(v.ltAddSubgroup ((Units.map (↑embedding : ValueGroup₀ v →* Γ₀) : (a : (ValueGroup₀ v)ˣ) → Γ₀ˣ) j)) : Set R) ⊆
      (fun (x_1 : R) ↦ x_1 * x) ⁻¹'
        (↑(v.ltAddSubgroup ((Units.map (↑embedding : ValueGroup₀ v →* Γ₀) : (a : (ValueGroup₀ v)ˣ) → Γ₀ˣ) γ)) : Set R)

Tactic:
use u⁻¹ * γ
-- Module: Mathlib.Topology.Algebra.Valued.ValuationTopology
Goal:
R : Type u
inst : Ring R
Γ₀ : Type v
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
x : R
γ : (ValueGroup₀ v)ˣ
γx : Γ₀ˣ
Hx : (v : (a : R) → Γ₀) x = (↑γx : Γ₀)
u : (ValueGroup₀ v)ˣ :=
  Units.mk0 (((restrict₀ v : MonoidWithZeroHom.{u, v} R (ValueGroup₀ v)) : (a : R) → ValueGroup₀ v) x) ⋯
hu_def : u = Units.mk0 (((restrict₀ v : MonoidWithZeroHom.{u, v} R (ValueGroup₀ v)) : (a : R) → ValueGroup₀ v) x) ⋯
hu : (embedding : (a : ValueGroup₀ v) → Γ₀) (↑u⁻¹ : ValueGroup₀ v) = (↑γx⁻¹ : Γ₀)
y : R
vy_lt :
  LT.lt.{v} (α := Γ₀) ((v : (a : R) → Γ₀) y : Γ₀)
    ((embedding : (a : ValueGroup₀ v) → Γ₀) (↑(u⁻¹ * γ) : ValueGroup₀ v) : Γ₀)
h :
  HMul.hMul (α := Γ₀) ((v : (a : R) → Γ₀) y : Γ₀) (↑γx : Γ₀) <
    (↑((Units.map (↑embedding : ValueGroup₀ v →* Γ₀) : (a : (ValueGroup₀ v)ˣ) → Γ₀ˣ) γ) : Γ₀)
⊢ Membership.mem (γ := Set R)
    ((fun (x_1 : R) ↦ x_1 * x) ⁻¹'
      (↑(v.ltAddSubgroup ((Units.map (↑embedding : ValueGroup₀ v →* Γ₀) : (a : (ValueGroup₀ v)ˣ) → Γ₀ˣ) γ)) : Set R))
    y

Tactic:
simp only [coe_ltAddSubgroup, preimage_setOf_eq, mem_setOf_eq, Valuation.map_mul, Hx]

Premises used: Set.mem_setOf_eq, Valuation.map_mul, Set.preimage_setOf_eq, Valuation.coe_ltAddSubgroup
-- Module: Mathlib.Topology.Algebra.Valued.ValuationTopology
Goal:
R K : Type u
inst : Ring R
inst_1 : DivisionRing K
Γ₀ : Type v
inst_2 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
this : UniformSpace R := IsTopologicalAddGroup.rightUniformSpace R
s : Set R
rw :
  (∃ (i : (ValueGroup₀ v)ˣ),
      True ∧
        (↑(v.ltAddSubgroup ((Units.map (↑embedding : ValueGroup₀ v →* Γ₀) : (a : (ValueGroup₀ v)ˣ) → Γ₀ˣ) i)) : Set R) ⊆
          s) ↔
    ∃ (γ : (ValueGroup₀ v)ˣ),
      {x : R | (v.restrict : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) x < (↑γ : ValueGroup₀ v)} ⊆ s
⊢ Membership.mem (γ := Filter R) (𝓝 0) s ↔
    ∃ (γ : (ValueGroup₀ v)ˣ),
      {x : R | (v.restrict : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) x < (↑γ : ValueGroup₀ v)} ⊆ s

Tactic:
rw [Filter.hasBasis_iff.mp v.subgroups_basis.hasBasis_nhds_zero s]

Premises used: RingSubgroupsBasis.hasBasis_nhds_zero, Valuation.subgroups_basis, Filter.hasBasis_iff, Iff.mp
-- Module: Mathlib.Topology.Algebra.Valued.ValuationTopology
Goal:
R K : Type u
inst : Ring R
inst_1 : DivisionRing K
Γ₀ : Type v
inst_2 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
this : UniformSpace R := IsTopologicalAddGroup.rightUniformSpace R
s : Set R
simp_rw :
  (∃ (i : (ValueGroup₀ v)ˣ),
      True ∧
        (↑(v.ltAddSubgroup ((Units.map (↑embedding : ValueGroup₀ v →* Γ₀) : (a : (ValueGroup₀ v)ˣ) → Γ₀ˣ) i)) : Set R) ⊆
          s) ↔
    ∃ (γ : (ValueGroup₀ v)ˣ),
      {x : R |
          LT.lt.{v} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀)
            ((embedding : (a : ValueGroup₀ v) → Γ₀) (↑γ : ValueGroup₀ v) : Γ₀)} ⊆
        s
⊢ (∃ (i : (ValueGroup₀ v)ˣ),
      True ∧
        (↑(v.ltAddSubgroup ((Units.map (↑embedding : ValueGroup₀ v →* Γ₀) : (a : (ValueGroup₀ v)ˣ) → Γ₀ˣ) i)) : Set R) ⊆
          s) ↔
    ∃ (γ : (ValueGroup₀ v)ˣ),
      {x : R | (v.restrict : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) x < (↑γ : ValueGroup₀ v)} ⊆ s

Tactic:
simp_rw [restrict_lt_iff_lt_embedding]

Premises used: Valuation.restrict_lt_iff_lt_embedding
-- Module: Mathlib.Topology.Algebra.Valued.ValuationTopology
Goal:
R K : Type u
inst : Ring R
inst_1 : DivisionRing K
Γ₀ : Type v
inst_2 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
this : UniformSpace R := IsTopologicalAddGroup.rightUniformSpace R
s : Set R
γ : (ValueGroup₀ v)ˣ
rw :
  (↑(v.ltAddSubgroup ((Units.map (↑embedding : ValueGroup₀ v →* Γ₀) : (a : (ValueGroup₀ v)ˣ) → Γ₀ˣ) γ)) : Set R) ⊆ s ↔
    {x : R |
        LT.lt.{v} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀)
          ((embedding : (a : ValueGroup₀ v) → Γ₀) (↑γ : ValueGroup₀ v) : Γ₀)} ⊆
      s
⊢ True ∧
      (↑(v.ltAddSubgroup ((Units.map (↑embedding : ValueGroup₀ v →* Γ₀) : (a : (ValueGroup₀ v)ˣ) → Γ₀ˣ) γ)) : Set R) ⊆
        s ↔
    {x : R |
        LT.lt.{v} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀)
          ((embedding : (a : ValueGroup₀ v) → Γ₀) (↑γ : ValueGroup₀ v) : Γ₀)} ⊆
      s

Tactic:
rw [true_and]

Premises used: true_and
-- Module: Mathlib.Topology.Algebra.Valued.ValuationTopology
Goal:
R K : Type u
inst : Ring R
inst_1 : DivisionRing K
Γ₀ : Type v
inst_2 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
this : UniformSpace R := IsTopologicalAddGroup.rightUniformSpace R
s : Set R
γ : (ValueGroup₀ v)ˣ
⊢ (↑(v.ltAddSubgroup ((Units.map (↑embedding : ValueGroup₀ v →* Γ₀) : (a : (ValueGroup₀ v)ˣ) → Γ₀ˣ) γ)) : Set R) ⊆ s ↔
    {x : R |
        LT.lt.{v} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀)
          ((embedding : (a : ValueGroup₀ v) → Γ₀) (↑γ : ValueGroup₀ v) : Γ₀)} ⊆
      s

Tactic:
rfl
-- Module: Mathlib.Topology.Algebra.Valued.ValuationTopology
Goal:
R K : Type u
inst : Ring R
inst_1 : DivisionRing K
Γ₀ : Type v
inst_2 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
this : UniformSpace R := IsTopologicalAddGroup.rightUniformSpace R
s : Set R
⊢ (∃ (i : (ValueGroup₀ v)ˣ),
      True ∧
        (↑(v.ltAddSubgroup ((Units.map (↑embedding : ValueGroup₀ v →* Γ₀) : (a : (ValueGroup₀ v)ˣ) → Γ₀ˣ) i)) : Set R) ⊆
          s) ↔
    ∃ (γ : (ValueGroup₀ v)ˣ),
      {x : R |
          LT.lt.{v} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀)
            ((embedding : (a : ValueGroup₀ v) → Γ₀) (↑γ : ValueGroup₀ v) : Γ₀)} ⊆
        s

Tactic:
exact exists_congr fun γ ↦ by rw [true_and]; rfl

Premises used: exists_congr
-- Module: Mathlib.Topology.Algebra.Valued.ValuationTopology
Goal:
R : Type u
inst : Ring R
Γ₀ : Type v
inst_1 : LinearOrderedCommGroupWithZero Γ₀
_i : Valued R Γ₀
⊢ Filter.HasBasis.{u, v + 1} (α := R) (𝓝 0) (fun (x : (ValueGroup₀ (F := Valuation R Γ₀) v)ˣ) ↦ True)
    fun (γ : (ValueGroup₀ (F := Valuation R Γ₀) v)ˣ) ↦
    {x : R | (Valuation.restrict v : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) x < (↑γ : ValueGroup₀ v)}

Tactic:
simp [Filter.hasBasis_iff, is_topological_valuation]

Premises used: Valued.is_topological_valuation, Filter.hasBasis_iff
-- Module: Mathlib.Topology.Algebra.Valued.ValuationTopology
Goal:
R : Type u
inst : Ring R
Γ₀ : Type v
inst_1 : LinearOrderedCommGroupWithZero Γ₀
_i : Valued R Γ₀
rw :
  Filter.HasBasis.{u, v + 1} (α := R × R) (Filter.comap (β := R) (fun (x : R × R) ↦ x.2 - x.1) (𝓝 0))
    (fun (x : (ValueGroup₀ (F := Valuation R Γ₀) v)ˣ) ↦ True) fun (γ : (ValueGroup₀ (F := Valuation R Γ₀) v)ˣ) ↦
    {p : R × R | (Valuation.restrict v : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) (p.2 - p.1) < (↑γ : ValueGroup₀ v)}
⊢ (𝓤 R).HasBasis (fun (x : (ValueGroup₀ (F := Valuation R Γ₀) v)ˣ) ↦ True)
    fun (γ : (ValueGroup₀ (F := Valuation R Γ₀) v)ˣ) ↦
    {p : R × R | (Valuation.restrict v : (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.Valued.ValuationTopology
Goal:
R : Type u
inst : Ring R
Γ₀ : Type v
inst_1 : LinearOrderedCommGroupWithZero Γ₀
_i : Valued R Γ₀
⊢ Filter.HasBasis.{u, v + 1} (α := R × R) (Filter.comap (β := R) (fun (x : R × R) ↦ x.2 - x.1) (𝓝 0))
    (fun (x : (ValueGroup₀ (F := Valuation R Γ₀) v)ˣ) ↦ True) fun (γ : (ValueGroup₀ (F := Valuation R Γ₀) v)ˣ) ↦
    {p : R × R | (Valuation.restrict v : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) (p.2 - p.1) < (↑γ : ValueGroup₀ v)}

Tactic:
(hasBasis_nhds_zero R Γ₀).comap _

Premises used: Set.Mem, setOf, Valued.hasBasis_nhds_zero, Filter.HasBasis.comap, Set.preimage
-- Module: Mathlib.Topology.Algebra.Valued.ValuationTopology
Goal:
R : Type u
inst : Ring R
Γ₀ : Type v
inst_1 : LinearOrderedCommGroupWithZero Γ₀
_i : Valued R Γ₀
⊢ Filter.HasBasis.{u, v + 1} (α := R × R) (Filter.comap (β := R) (fun (x : R × R) ↦ x.2 - x.1) (𝓝 0))
    (fun (x : (ValueGroup₀ (F := Valuation R Γ₀) v)ˣ) ↦ True) fun (γ : (ValueGroup₀ (F := Valuation R Γ₀) v)ˣ) ↦
    {p : R × R | (Valuation.restrict v : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) (p.2 - p.1) < (↑γ : ValueGroup₀ v)}

Tactic:
exact (hasBasis_nhds_zero R Γ₀).comap _

Premises used: Valued.hasBasis_nhds_zero, Filter.HasBasis.comap
-- Module: Mathlib.Topology.Algebra.Valued.ValuationTopology
Goal:
R : Type u
inst : Ring R
Γ₀ : Type v
inst_1 : LinearOrderedCommGroupWithZero Γ₀
_i : Valued R Γ₀
⊢ @toUniformSpace _ inst _ inst_1 _ = IsTopologicalAddGroup.rightUniformSpace R

Tactic:
UniformSpace.ext ((hasBasis_uniformity R Γ₀).eq_of_same_basis ?_)

Premises used: UniformSpace.ext, Valued.hasBasis_uniformity, Filter.HasBasis.eq_of_same_basis
-- Module: Mathlib.Topology.Algebra.Valued.ValuationTopology
Goal:
R : Type u
inst : Ring R
Γ₀ : Type v
inst_1 : LinearOrderedCommGroupWithZero Γ₀
_i : Valued R Γ₀
refine :
  (uniformity R).HasBasis (fun (x : (ValueGroup₀ (F := Valuation R Γ₀) v)ˣ) ↦ True)
    fun (γ : (ValueGroup₀ (F := Valuation R Γ₀) v)ˣ) ↦
    {p : R × R | (Valuation.restrict v : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) (p.2 - p.1) < (↑γ : ValueGroup₀ v)}
⊢ @toUniformSpace _ inst _ inst_1 _ = IsTopologicalAddGroup.rightUniformSpace R

Tactic:
refine UniformSpace.ext ((hasBasis_uniformity R Γ₀).eq_of_same_basis ?_)

Premises used: UniformSpace.ext, Valued.hasBasis_uniformity, Filter.HasBasis.eq_of_same_basis
-- Module: Mathlib.Topology.Algebra.Valued.ValuationTopology
Goal:
R : Type u
inst : Ring R
Γ₀ : Type v
inst_1 : LinearOrderedCommGroupWithZero Γ₀
_i : Valued R Γ₀
⊢ Filter.HasBasis.{u, v + 1} (α := R × R) (Filter.comap (β := R) (fun (p : R × R) ↦ p.2 + -p.1) (𝓝 0))
    (fun (x : (ValueGroup₀ (F := Valuation R Γ₀) v)ˣ) ↦ True) fun (i : (ValueGroup₀ (F := Valuation R Γ₀) v)ˣ) ↦
    (fun (p : R × R) ↦ p.2 + -p.1) ⁻¹'
      (↑(ltAddSubgroup v ((Units.map (↑embedding : ValueGroup₀ v →* Γ₀) : (a : (ValueGroup₀ v)ˣ) → Γ₀ˣ) i)) : Set R)

Tactic:
v.subgroups_basis.hasBasis_nhds_zero.comap _

Premises used: Valued.v, RingSubgroupsBasis.hasBasis_nhds_zero, Valuation.subgroups_basis, Filter.HasBasis.comap
-- Module: Mathlib.Topology.Algebra.Valued.ValuationTopology
Goal:
R : Type u
inst : Ring R
Γ₀ : Type v
inst_1 : LinearOrderedCommGroupWithZero Γ₀
_i : Valued R Γ₀
h :
  ∀ (x : (ValueGroup₀ (F := Valuation R Γ₀) v)ˣ),
    Eq (α := Set (R × R))
      {p : R × R | (Valuation.restrict v : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) (p.2 - p.1) < (↑x : ValueGroup₀ v)}
      ((fun (p : R × R) ↦ p.2 + -p.1) ⁻¹'
        (↑(ltAddSubgroup v ((Units.map (↑embedding : ValueGroup₀ v →* Γ₀) : (a : (ValueGroup₀ v)ˣ) → Γ₀ˣ) x)) : Set R))
⊢ (uniformity R).HasBasis (fun (x : (ValueGroup₀ (F := Valuation R Γ₀) v)ˣ) ↦ True)
    fun (γ : (ValueGroup₀ (F := Valuation R Γ₀) v)ˣ) ↦
    {p : R × R | (Valuation.restrict v : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) (p.2 - p.1) < (↑γ : ValueGroup₀ v)}

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

Premises used: Valued.v, RingSubgroupsBasis.hasBasis_nhds_zero, Valuation.subgroups_basis, Filter.HasBasis.comap
-- Module: Mathlib.Topology.Algebra.Valued.ValuationTopology
Goal:
R : Type u
inst : Ring R
Γ₀ : Type v
inst_1 : LinearOrderedCommGroupWithZero Γ₀
_i : Valued R Γ₀
x : (ValueGroup₀ (F := Valuation R Γ₀) v)ˣ
h :
  Eq (α := Set (R × R))
    {p : R × R |
      LT.lt.{v} (α := Γ₀) ((v : (a : R) → Γ₀) (p.2 + -p.1) : Γ₀)
        ((embedding : (a : ValueGroup₀ v) → Γ₀) (↑x : ValueGroup₀ v) : Γ₀)}
    ((fun (p : R × R) ↦ p.2 + -p.1) ⁻¹'
      (↑(ltAddSubgroup v ((Units.map (↑embedding : ValueGroup₀ v →* Γ₀) : (a : (ValueGroup₀ v)ˣ) → Γ₀ˣ) x)) : Set R))
⊢ Eq (α := Set (R × R))
    {p : R × R | (Valuation.restrict v : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) (p.2 - p.1) < (↑x : ValueGroup₀ v)}
    ((fun (p : R × R) ↦ p.2 + -p.1) ⁻¹'
      (↑(ltAddSubgroup v ((Units.map (↑embedding : ValueGroup₀ v →* Γ₀) : (a : (ValueGroup₀ v)ˣ) → Γ₀ˣ) x)) : Set R))

Tactic:
simp_rw [restrict_lt_iff_lt_embedding, sub_eq_add_neg]

Premises used: Valuation.restrict_lt_iff_lt_embedding, sub_eq_add_neg
-- Module: Mathlib.Topology.Algebra.Valued.ValuationTopology
Goal:
R : Type u
inst : Ring R
Γ₀ : Type v
inst_1 : LinearOrderedCommGroupWithZero Γ₀
_i : Valued R Γ₀
x : (ValueGroup₀ (F := Valuation R Γ₀) v)ˣ
⊢ Eq (α := Set (R × R))
    {p : R × R |
      LT.lt.{v} (α := Γ₀) ((v : (a : R) → Γ₀) (p.2 + -p.1) : Γ₀)
        ((embedding : (a : ValueGroup₀ v) → Γ₀) (↑x : ValueGroup₀ v) : Γ₀)}
    ((fun (p : R × R) ↦ p.2 + -p.1) ⁻¹'
      (↑(ltAddSubgroup v ((Units.map (↑embedding : ValueGroup₀ v →* Γ₀) : (a : (ValueGroup₀ v)ˣ) → Γ₀ˣ) x)) : Set R))

Tactic:
simp
-- Module: Mathlib.Topology.Algebra.Valued.ValuationTopology
Goal:
R : Type u
inst : Ring R
Γ₀ : Type v
inst_1 : LinearOrderedCommGroupWithZero Γ₀
_i : Valued R Γ₀
s : Set R
x : R
⊢ s ∈ 𝓝 x ↔
    ∃ (γ : (ValueGroup₀ (F := Valuation R Γ₀) v)ˣ),
      {y : R | (Valuation.restrict v : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) (y - x) < (↑γ : ValueGroup₀ v)} ⊆ s

Tactic:
simp only [← nhds_translation_add_neg x, ← sub_eq_add_neg, preimage_setOf_eq, true_and,
    ((hasBasis_nhds_zero R Γ₀).comap fun y ↦ y - x).mem_iff]

Premises used: Filter.HasBasis.mem_iff, sub_eq_add_neg, HSub.hSub, Valued.hasBasis_nhds_zero, Filter.HasBasis.comap, Set.preimage_setOf_eq, nhds_translation_add_neg, true_and
-- Module: Mathlib.Topology.Algebra.Valued.ValuationTopology
Goal:
R : Type u
inst : Ring R
Γ₀ : Type v
inst_1 : LinearOrderedCommGroupWithZero Γ₀
_i : Valued R Γ₀
s : Set R
⊢ Membership.mem (γ := Filter R) (𝓝 0) s ↔
    ∃ (γ : (ValueGroup₀ (F := Valuation R Γ₀) v)ˣ),
      {x : R | (Valuation.restrict v : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) x < (↑γ : ValueGroup₀ v)} ⊆ s

Tactic:
simp only [mem_nhds, sub_zero]

Premises used: sub_zero, Valued.mem_nhds
-- Module: Mathlib.Topology.Algebra.Valued.ValuationTopology
Goal:
R : Type u
inst : Ring R
Γ₀ : Type v
inst_1 : LinearOrderedCommGroupWithZero Γ₀
_i : Valued R Γ₀
x : R
h : Ne.{v + 1} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) (0 : Γ₀)
rw :
  ∃ (γ : (ValueGroup₀ (F := Valuation R Γ₀) v)ˣ),
    Subset.{u} (α := Set R)
      {y : R | (Valuation.restrict v : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) (y - x) < (↑γ : ValueGroup₀ v)}
      {y : R | Eq.{v + 1} (α := Γ₀) ((v : (a : R) → Γ₀) y : Γ₀) ((v : (a : R) → Γ₀) x : Γ₀)}
⊢ {y : R | Eq.{v + 1} (α := Γ₀) ((v : (a : R) → Γ₀) y : Γ₀) ((v : (a : R) → Γ₀) x : Γ₀)} ∈ 𝓝 x

Tactic:
rw [mem_nhds]

Premises used: Valued.mem_nhds
-- Module: Mathlib.Topology.Algebra.Valued.ValuationTopology
Goal:
R : Type u
inst : Ring R
Γ₀ : Type v
inst_1 : LinearOrderedCommGroupWithZero Γ₀
_i : Valued R Γ₀
x : R
h : Ne.{v + 1} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) (0 : Γ₀)
⊢ Ne.{v + 1} (α := ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
    ((Valuation.restrict v : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) x : ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
    (0 : ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))

Tactic:
simp [h]
-- Module: Mathlib.Topology.Algebra.Valued.ValuationTopology
Goal:
R : Type u
inst : Ring R
Γ₀ : Type v
inst_1 : LinearOrderedCommGroupWithZero Γ₀
_i : Valued R Γ₀
x : R
h : Ne.{v + 1} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) (0 : Γ₀)
⊢ Ne.{v + 1} (α := ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
    ((Valuation.restrict v : (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.Valued.ValuationTopology
Goal:
R : Type u
inst : Ring R
Γ₀ : Type v
inst_1 : LinearOrderedCommGroupWithZero Γ₀
_i : Valued R Γ₀
x : R
h : Ne.{v + 1} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) (0 : Γ₀)
h' :
  Ne.{v + 1} (α := ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
    ((Valuation.restrict v : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) x : ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
    (0 : ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
h₁ :
  Subset.{u} (α := Set R)
    {y : R |
      LT.lt.{v} (α := ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
        ((Valuation.restrict v : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) (y - x) :
          ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
        ((↑(Units.mk0 ((Valuation.restrict v : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) x) h') :
            ValueGroup₀ (F := Valuation R Γ₀) v) :
          ValueGroup₀ (F := Valuation R Γ₀) v)}
    {y : R | Eq.{v + 1} (α := Γ₀) ((v : (a : R) → Γ₀) y : Γ₀) ((v : (a : R) → Γ₀) x : Γ₀)}
⊢ ∃ (γ : (ValueGroup₀ (F := Valuation R Γ₀) v)ˣ),
    Subset.{u} (α := Set R)
      {y : R | (Valuation.restrict v : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) (y - x) < (↑γ : ValueGroup₀ v)}
      {y : R | Eq.{v + 1} (α := Γ₀) ((v : (a : R) → Γ₀) y : Γ₀) ((v : (a : R) → Γ₀) x : Γ₀)}

Tactic:
use Units.mk0 _ h'

Premises used: Units.mk0
-- Module: Mathlib.Topology.Algebra.Valued.ValuationTopology
Goal:
R : Type u
inst : Ring R
Γ₀ : Type v
inst_1 : LinearOrderedCommGroupWithZero Γ₀
_i : Valued R Γ₀
x : R
h : Ne.{v + 1} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) (0 : Γ₀)
h' :
  Ne.{v + 1} (α := ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
    ((Valuation.restrict v : (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)
    {y : R |
      LT.lt.{v} (α := ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
        ((Valuation.restrict v : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) (y - x) :
          ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
        ((Valuation.restrict v : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) x :
          ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))}
    y
⊢ Membership.mem (γ := Set R) {y : R | Eq.{v + 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, Valued.v, setOf, Iff.mp, Valuation.map_eq_of_sub_lt, Valuation.restrict_lt_iff
-- Module: Mathlib.Topology.Algebra.Valued.ValuationTopology
Goal:
R : Type u
inst : Ring R
Γ₀ : Type v
inst_1 : LinearOrderedCommGroupWithZero Γ₀
_i : Valued R Γ₀
x : R
h : Ne.{v + 1} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) (0 : Γ₀)
h' :
  Ne.{v + 1} (α := ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
    ((Valuation.restrict v : (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)
    {y : R |
      LT.lt.{v} (α := ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
        ((Valuation.restrict v : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) (y - x) :
          ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
        ((Valuation.restrict v : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) x :
          ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))}
    y
⊢ Membership.mem (γ := Set R) {y : R | Eq.{v + 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: Valued.v, Iff.mp, Valuation.map_eq_of_sub_lt, Valuation.restrict_lt_iff
-- Module: Mathlib.Topology.Algebra.Valued.ValuationTopology
Goal:
R K : Type u
inst : Ring R
inst_1 : DivisionRing K
Γ₀ : Type v
inst_2 : LinearOrderedCommGroupWithZero Γ₀
_i : Valued R Γ₀
⊢ IsTopologicalRing R

Tactic:
(toUniformSpace_eq R Γ₀).symm ▸ v.subgroups_basis.toRingFilterBasis.isTopologicalRing

Premises used: RingFilterBasis.isTopologicalRing, Valued.toUniformSpace_eq, Valued.v, Valuation.subgroups_basis, Eq.rec, RingSubgroupsBasis.toRingFilterBasis, Eq.symm
-- Module: Mathlib.Topology.Algebra.Valued.ValuationTopology
Goal:
R : Type u
inst : Ring R
Γ₀ : Type v
inst_1 : LinearOrderedCommGroupWithZero Γ₀
_i : Valued R Γ₀
h : ∀ (x : R), x ≠ 0 → Eq.{v + 1} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) (1 : Γ₀)
simp :
  ∃ (γ : (ValueGroup₀ (F := Valuation R Γ₀) v)ˣ),
    ∀ (y : R), (Valuation.restrict v : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) y < (↑γ : ValueGroup₀ v) → y = 0
⊢ DiscreteTopology R

Tactic:
simp only [discreteTopology_iff_isOpen_singleton_zero, isOpen_iff_mem_nhds, mem_singleton_iff,
    forall_eq, mem_nhds_zero, subset_singleton_iff, mem_setOf_eq]

Premises used: Set.subset_singleton_iff, forall_eq, Set.mem_setOf_eq, Set.mem_singleton_iff, Valued.mem_nhds_zero, isOpen_iff_mem_nhds, discreteTopology_iff_isOpen_singleton_zero
-- Module: Mathlib.Topology.Algebra.Valued.ValuationTopology
Goal:
R : Type u
inst : Ring R
Γ₀ : Type v
inst_1 : LinearOrderedCommGroupWithZero Γ₀
_i : Valued R Γ₀
h : ∀ (x : R), x ≠ 0 → Eq.{v + 1} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) (1 : Γ₀)
h₁ :
  ∀ (y : R),
    LT.lt.{v} (α := ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
        ((Valuation.restrict v : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) y : ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
        ((↑1 : ValueGroup₀ (F := Valuation R Γ₀) v) : ValueGroup₀ (F := Valuation R Γ₀) v) →
      y = 0
⊢ ∃ (γ : (ValueGroup₀ (F := Valuation R Γ₀) v)ˣ),
    ∀ (y : R), (Valuation.restrict v : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) y < (↑γ : ValueGroup₀ v) → y = 0

Tactic:
use 1