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 Γ₀
_i : Valued R Γ₀
h : ∀ (x : R), x ≠ 0 → Eq.{v + 1} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) (1 : Γ₀)
h₁ :
  ∀
    (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),
    ∃ (x : R), x ≠ 0 ∧ Ne.{v + 1} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) (1 : Γ₀)
⊢ ∀ (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

Tactic:
contrapose! h
-- Module: Mathlib.Topology.Algebra.Valued.ValuationTopology
Goal:
R : Type u
inst : Ring R
Γ₀ : Type v
inst_1 : LinearOrderedCommGroupWithZero Γ₀
_i : Valued R Γ₀
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
h₁ :
  ∀ (x : R)
    (hx :
      LT.lt.{v} (α := ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
        ((Valuation.restrict v : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) x : ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
        ((↑1 : ValueGroup₀ (F := Valuation R Γ₀) v) : ValueGroup₀ (F := Valuation R Γ₀) v))
    (hx' : x ≠ 0), ∃ (x : R), x ≠ 0 ∧ Ne.{v + 1} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) (1 : Γ₀)
⊢ ∃ (x : R), x ≠ 0 ∧ Ne.{v + 1} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) (1 : Γ₀)

Tactic:
obtain ⟨x, hx, hx'⟩ := h
-- Module: Mathlib.Topology.Algebra.Valued.ValuationTopology
Goal:
R : Type u
inst : Ring R
Γ₀ : Type v
inst_1 : LinearOrderedCommGroupWithZero Γ₀
_i : Valued R Γ₀
x : R
hx :
  LT.lt.{v} (α := ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
    ((Valuation.restrict v : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) x : ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
    ((↑1 : ValueGroup₀ (F := Valuation R Γ₀) v) : ValueGroup₀ (F := Valuation R Γ₀) v)
hx' : x ≠ 0
⊢ LT.lt.{v} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) (1 : Γ₀)

Tactic:
rw [restrict_lt_iff_lt_embedding, Units.val_one, map_one] at hx

Premises used: Valuation.restrict_lt_iff_lt_embedding, map_one, Units.val_one
-- Module: Mathlib.Topology.Algebra.Valued.ValuationTopology
Goal:
R : Type u
inst : Ring R
Γ₀ : Type v
inst_1 : LinearOrderedCommGroupWithZero Γ₀
_i : Valued R Γ₀
x : R
hx :
  LT.lt.{v} (α := ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
    ((Valuation.restrict v : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) x : ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
    ((↑1 : ValueGroup₀ (F := Valuation R Γ₀) v) : ValueGroup₀ (F := Valuation R Γ₀) v)
hx' : x ≠ 0
hx₁ : LT.lt.{v} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) (1 : Γ₀)
⊢ x ≠ 0

Tactic:
rw [restrict_lt_iff_lt_embedding, Units.val_one, map_one] at hx

Premises used: Valuation.restrict_lt_iff_lt_embedding, map_one, Units.val_one
-- Module: Mathlib.Topology.Algebra.Valued.ValuationTopology
Goal:
R : Type u
inst : Ring R
Γ₀ : Type v
inst_1 : LinearOrderedCommGroupWithZero Γ₀
_i : Valued R Γ₀
x : R
hx : LT.lt.{v} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) (1 : Γ₀)
hx' : x ≠ 0
⊢ ∃ (x : R), x ≠ 0 ∧ Ne.{v + 1} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) (1 : Γ₀)

Tactic:
⟨x, hx', hx.ne⟩

Premises used: And.intro, Exists.intro, LT.lt.ne
-- Module: Mathlib.Topology.Algebra.Valued.ValuationTopology
Goal:
R : Type u
inst : Ring R
Γ₀ : Type v
inst_1 : LinearOrderedCommGroupWithZero Γ₀
_i : Valued R Γ₀
x : R
hx : LT.lt.{v} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) (1 : Γ₀)
hx' : x ≠ 0
⊢ ∃ (x : R), x ≠ 0 ∧ Ne.{v + 1} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) (1 : Γ₀)

Tactic:
exact ⟨x, hx', hx.ne⟩
-- Module: Mathlib.Topology.Algebra.Valued.ValuationTopology
Goal:
K : Type u
inst : DivisionRing K
Γ₀ : Type v
inst_1 : LinearOrderedCommGroupWithZero Γ₀
inst_2 : MulArchimedean Γ₀
inst_3 : Valued K Γ₀
r : Γ₀
hr : r ≠ 0
h : ∀ (x : K), Ne.{v + 1} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (0 : Γ₀) → r < (v : (a : K) → Γ₀) x
⊢ ∀ (x : K), x ≠ 0 → Eq.{v + 1} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀)

Tactic:
simpa using Valued.v.map_eq_one_of_forall_lt hr h

Premises used: Valuation.map_eq_one_of_forall_lt
-- Module: Mathlib.Topology.Algebra.Valued.ValuationTopology
Goal:
R : Type u
inst : Ring R
Γ₀ : Type v
inst_1 : LinearOrderedCommGroupWithZero Γ₀
_i : Valued R Γ₀
F : Filter R
rw :
  (F.NeBot ∧
      ∀ (U : Set R),
        Membership.mem (γ := AddGroupFilterBasis R) RingFilterBasis.toAddGroupFilterBasis U →
          ∃ M ∈ F, ∀ x ∈ M, ∀ y ∈ M, y - x ∈ U) ↔
    F.NeBot ∧
      ∀ (γ : (ValueGroup₀ (F := Valuation R Γ₀) v)ˣ),
        ∃ M ∈ F,
          ∀ x ∈ M,
            ∀ y ∈ M, (Valuation.restrict v : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) (y - x) < (↑γ : ValueGroup₀ v)
⊢ Cauchy F ↔
    F.NeBot ∧
      ∀ (γ : (ValueGroup₀ (F := Valuation R Γ₀) v)ˣ),
        ∃ M ∈ F,
          ∀ x ∈ M,
            ∀ y ∈ M, (Valuation.restrict v : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) (y - x) < (↑γ : ValueGroup₀ v)

Tactic:
rw [toUniformSpace_eq, AddGroupFilterBasis.cauchy_iff]

Premises used: Valued.toUniformSpace_eq, AddGroupFilterBasis.cauchy_iff
-- Module: Mathlib.Topology.Algebra.Valued.ValuationTopology
Goal:
R : Type u
inst : Ring R
Γ₀ : Type v
inst_1 : LinearOrderedCommGroupWithZero Γ₀
_i : Valued R Γ₀
F : Filter R
apply :
  (∀ (U : Set R),
      Membership.mem (γ := AddGroupFilterBasis R) RingFilterBasis.toAddGroupFilterBasis U →
        ∃ M ∈ F, ∀ x ∈ M, ∀ y ∈ M, y - x ∈ U) ↔
    ∀ (γ : (ValueGroup₀ (F := Valuation R Γ₀) v)ˣ),
      ∃ M ∈ F,
        ∀ x ∈ M, ∀ y ∈ M, (Valuation.restrict v : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) (y - x) < (↑γ : ValueGroup₀ v)
⊢ (F.NeBot ∧
      ∀ (U : Set R),
        Membership.mem (γ := AddGroupFilterBasis R) RingFilterBasis.toAddGroupFilterBasis U →
          ∃ M ∈ F, ∀ x ∈ M, ∀ y ∈ M, y - x ∈ U) ↔
    F.NeBot ∧
      ∀ (γ : (ValueGroup₀ (F := Valuation R Γ₀) v)ˣ),
        ∃ M ∈ F,
          ∀ x ∈ M,
            ∀ y ∈ M, (Valuation.restrict v : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) (y - x) < (↑γ : ValueGroup₀ v)

Tactic:
apply and_congr Iff.rfl

Premises used: Iff.rfl, and_congr
-- Module: Mathlib.Topology.Algebra.Valued.ValuationTopology
Goal:
R : Type u
inst : Ring R
Γ₀ : Type v
inst_1 : LinearOrderedCommGroupWithZero Γ₀
_i : Valued R Γ₀
F : Filter R
mp :
  (∀ (U : Set R),
      (∃ (i : (ValueGroup₀ (F := Valuation R Γ₀) v)ˣ),
          U =
            (↑(ltAddSubgroup v ((Units.map (↑embedding : ValueGroup₀ v →* Γ₀) : (a : (ValueGroup₀ v)ˣ) → Γ₀ˣ) i)) :
              Set R)) →
        ∃ M ∈ F, ∀ x ∈ M, ∀ y ∈ M, y - x ∈ U) →
    ∀ (γ : (ValueGroup₀ (F := Valuation R Γ₀) v)ˣ),
      ∃ M ∈ F,
        ∀ x ∈ M, ∀ y ∈ M, (Valuation.restrict v : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) (y - x) < (↑γ : ValueGroup₀ v)
mpr :
  (∀ (γ : (ValueGroup₀ (F := Valuation R Γ₀) v)ˣ),
      ∃ M ∈ F,
        ∀ x ∈ M,
          ∀ y ∈ M, (Valuation.restrict v : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) (y - x) < (↑γ : ValueGroup₀ v)) →
    ∀ (U : Set R),
      (∃ (i : (ValueGroup₀ (F := Valuation R Γ₀) v)ˣ),
          U =
            (↑(ltAddSubgroup v ((Units.map (↑embedding : ValueGroup₀ v →* Γ₀) : (a : (ValueGroup₀ v)ˣ) → Γ₀ˣ) i)) :
              Set R)) →
        ∃ M ∈ F, ∀ x ∈ M, ∀ y ∈ M, y - x ∈ U
⊢ (∀ (U : Set R),
      (∃ (i : (ValueGroup₀ (F := Valuation R Γ₀) v)ˣ),
          U =
            (↑(ltAddSubgroup v ((Units.map (↑embedding : ValueGroup₀ v →* Γ₀) : (a : (ValueGroup₀ v)ˣ) → Γ₀ˣ) i)) :
              Set R)) →
        ∃ M ∈ F, ∀ x ∈ M, ∀ y ∈ M, y - x ∈ U) ↔
    ∀ (γ : (ValueGroup₀ (F := Valuation R Γ₀) v)ˣ),
      ∃ M ∈ F,
        ∀ x ∈ M, ∀ y ∈ M, (Valuation.restrict v : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) (y - x) < (↑γ : ValueGroup₀ v)

Tactic:
constructor
-- Module: Mathlib.Topology.Algebra.Valued.ValuationTopology
Goal:
R : Type u
inst : Ring R
Γ₀ : Type v
inst_1 : LinearOrderedCommGroupWithZero Γ₀
_i : Valued R Γ₀
F : Filter R
h :
  ∀ (U : Set R),
    (∃ (i : (ValueGroup₀ (F := Valuation R Γ₀) v)ˣ),
        U =
          (↑(ltAddSubgroup v ((Units.map (↑embedding : ValueGroup₀ v →* Γ₀) : (a : (ValueGroup₀ v)ˣ) → Γ₀ˣ) i)) :
            Set R)) →
      ∃ M ∈ F, ∀ x ∈ M, ∀ y ∈ M, y - x ∈ U
γ : (ValueGroup₀ (F := Valuation R Γ₀) v)ˣ
mp :
  ∃ M ∈ F,
    ∀ x ∈ M,
      ∀ y ∈ M,
        LT.lt.{v} (α := Γ₀) ((v : (a : R) → Γ₀) (y - x) : Γ₀)
          ((embedding : (a : ValueGroup₀ v) → Γ₀) (↑γ : ValueGroup₀ v) : Γ₀)
⊢ ∃ M ∈ F,
    ∀ x ∈ M, ∀ y ∈ M, (Valuation.restrict v : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) (y - x) < (↑γ : ValueGroup₀ v)

Tactic:
simp_rw [restrict_lt_iff_lt_embedding]

Premises used: Valuation.restrict_lt_iff_lt_embedding
-- Module: Mathlib.Topology.Algebra.Valued.ValuationTopology
Goal:
R : Type u
inst : Ring R
Γ₀ : Type v
inst_1 : LinearOrderedCommGroupWithZero Γ₀
_i : Valued R Γ₀
F : Filter R
h :
  ∀ (U : Set R),
    (∃ (i : (ValueGroup₀ (F := Valuation R Γ₀) v)ˣ),
        U =
          (↑(ltAddSubgroup v ((Units.map (↑embedding : ValueGroup₀ v →* Γ₀) : (a : (ValueGroup₀ v)ˣ) → Γ₀ˣ) i)) :
            Set R)) →
      ∃ M ∈ F, ∀ x ∈ M, ∀ y ∈ M, y - x ∈ U
γ : (ValueGroup₀ (F := Valuation R Γ₀) v)ˣ
⊢ ∃ M ∈ F,
    ∀ x ∈ M,
      ∀ y ∈ M,
        LT.lt.{v} (α := Γ₀) ((v : (a : R) → Γ₀) (y - x) : Γ₀)
          ((embedding : (a : ValueGroup₀ v) → Γ₀) (↑γ : ValueGroup₀ v) : Γ₀)

Tactic:
h _ (Valued.v.subgroups_basis.mem_addGroupFilterBasis γ)

Premises used: Set.Mem, Valued.v, setOf, Valuation.subgroups_basis, RingSubgroupsBasis.mem_addGroupFilterBasis
-- Module: Mathlib.Topology.Algebra.Valued.ValuationTopology
Goal:
R : Type u
inst : Ring R
Γ₀ : Type v
inst_1 : LinearOrderedCommGroupWithZero Γ₀
_i : Valued R Γ₀
F : Filter R
h :
  ∀ (U : Set R),
    (∃ (i : (ValueGroup₀ (F := Valuation R Γ₀) v)ˣ),
        U =
          (↑(ltAddSubgroup v ((Units.map (↑embedding : ValueGroup₀ v →* Γ₀) : (a : (ValueGroup₀ v)ˣ) → Γ₀ˣ) i)) :
            Set R)) →
      ∃ M ∈ F, ∀ x ∈ M, ∀ y ∈ M, y - x ∈ U
γ : (ValueGroup₀ (F := Valuation R Γ₀) v)ˣ
⊢ ∃ M ∈ F,
    ∀ x ∈ M,
      ∀ y ∈ M,
        LT.lt.{v} (α := Γ₀) ((v : (a : R) → Γ₀) (y - x) : Γ₀)
          ((embedding : (a : ValueGroup₀ v) → Γ₀) (↑γ : ValueGroup₀ v) : Γ₀)

Tactic:
exact h _ (Valued.v.subgroups_basis.mem_addGroupFilterBasis γ)

Premises used: Valued.v, Valuation.subgroups_basis, RingSubgroupsBasis.mem_addGroupFilterBasis
-- Module: Mathlib.Topology.Algebra.Valued.ValuationTopology
Goal:
R : Type u
inst : Ring R
Γ₀ : Type v
inst_1 : LinearOrderedCommGroupWithZero Γ₀
_i : Valued R Γ₀
F : Filter R
h :
  ∀ (γ : (ValueGroup₀ (F := Valuation R Γ₀) v)ˣ),
    ∃ M ∈ F,
      ∀ x ∈ M, ∀ y ∈ M, (Valuation.restrict v : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) (y - x) < (↑γ : ValueGroup₀ v)
γ : (ValueGroup₀ (F := Valuation R Γ₀) v)ˣ
⊢ ∀ (γ : (ValueGroup₀ (F := Valuation R Γ₀) v)ˣ),
    ∃ M ∈ F,
      ∀ x ∈ M,
        ∀ y ∈ M,
          LT.lt.{v} (α := Γ₀) ((v : (a : R) → Γ₀) (y - x) : Γ₀)
            ((embedding : (a : ValueGroup₀ v) → Γ₀) (↑γ : ValueGroup₀ v) : Γ₀)

Tactic:
simp_rw [restrict_lt_iff_lt_embedding] at h

Premises used: Valuation.restrict_lt_iff_lt_embedding
-- Module: Mathlib.Topology.Algebra.Valued.ValuationTopology
Goal:
R : Type u
inst : Ring R
Γ₀ : Type v
inst_1 : LinearOrderedCommGroupWithZero Γ₀
_i : Valued R Γ₀
F : Filter R
γ : (ValueGroup₀ (F := Valuation R Γ₀) v)ˣ
h :
  ∀ (γ : (ValueGroup₀ (F := Valuation R Γ₀) v)ˣ),
    ∃ M ∈ F,
      ∀ x ∈ M,
        ∀ y ∈ M,
          LT.lt.{v} (α := Γ₀) ((v : (a : R) → Γ₀) (y - x) : Γ₀)
            ((embedding : (a : ValueGroup₀ v) → Γ₀) (↑γ : ValueGroup₀ v) : Γ₀)
⊢ ∃ M ∈ F,
    ∀ x ∈ M,
      ∀ y ∈ M,
        y - x ∈
          (↑(ltAddSubgroup v ((Units.map (↑embedding : ValueGroup₀ v →* Γ₀) : (a : (ValueGroup₀ v)ˣ) → Γ₀ˣ) γ)) : Set R)

Tactic:
h γ

Premises used: Set.Mem, setOf
-- Module: Mathlib.Topology.Algebra.Valued.ValuationTopology
Goal:
R : Type u
inst : Ring R
Γ₀ : Type v
inst_1 : LinearOrderedCommGroupWithZero Γ₀
_i : Valued R Γ₀
F : Filter R
γ : (ValueGroup₀ (F := Valuation R Γ₀) v)ˣ
h :
  ∀ (γ : (ValueGroup₀ (F := Valuation R Γ₀) v)ˣ),
    ∃ M ∈ F,
      ∀ x ∈ M,
        ∀ y ∈ M,
          LT.lt.{v} (α := Γ₀) ((v : (a : R) → Γ₀) (y - x) : Γ₀)
            ((embedding : (a : ValueGroup₀ v) → Γ₀) (↑γ : ValueGroup₀ v) : Γ₀)
⊢ ∃ M ∈ F,
    ∀ x ∈ M,
      ∀ y ∈ M,
        y - x ∈
          (↑(ltAddSubgroup v ((Units.map (↑embedding : ValueGroup₀ v →* Γ₀) : (a : (ValueGroup₀ v)ˣ) → Γ₀ˣ) γ)) : Set R)

Tactic:
exact h γ
-- Module: Mathlib.Topology.Algebra.Valued.ValuationTopology
Goal:
R : Type u
inst : Ring R
Γ₀ : Type v
inst_1 : LinearOrderedCommGroupWithZero Γ₀
_i : Valued R Γ₀
r : ValueGroup₀ (F := Valuation R Γ₀) v
rw :
  ∀ (x : R),
    Membership.mem (γ := Set R) {x : R | (Valuation.restrict v : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) x < r} x →
      {x : R | (Valuation.restrict v : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) x < r} ∈ 𝓝 x
⊢ IsOpen[_i.toTopologicalSpace] {x : R | (Valuation.restrict v : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) x < r}

Tactic:
rw [isOpen_iff_mem_nhds]

Premises used: isOpen_iff_mem_nhds
-- Module: Mathlib.Topology.Algebra.Valued.ValuationTopology
Goal:
R : Type u
inst : Ring R
Γ₀ : Type v
inst_1 : LinearOrderedCommGroupWithZero Γ₀
_i : Valued R Γ₀
r : ValueGroup₀ (F := Valuation R Γ₀) v
inl :
  ∀ (x : R),
    Membership.mem (γ := Set R)
        {x : R |
          LT.lt.{v} (α := ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
            ((Valuation.restrict v : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) x :
              ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
            (0 : ValueGroup₀ (F := Valuation R Γ₀) v)}
        x →
      {x : R |
          LT.lt.{v} (α := ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
            ((Valuation.restrict v : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) x :
              ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
            (0 : ValueGroup₀ (F := Valuation R Γ₀) v)} ∈
        𝓝 x
inr :
  ∀ (hr : r ≠ 0) (x : R),
    Membership.mem (γ := Set R) {x : R | (Valuation.restrict v : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) x < r} x →
      {x : R | (Valuation.restrict v : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) x < r} ∈ 𝓝 x
⊢ ∀ (x : R),
    Membership.mem (γ := Set R) {x : R | (Valuation.restrict v : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) x < r} x →
      {x : R | (Valuation.restrict v : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) x < r} ∈ 𝓝 x

Tactic:
rcases eq_or_ne r 0 with rfl | hr

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Topology.Algebra.Valued.ValuationTopology
Goal:
R : Type u
inst : Ring R
Γ₀ : Type v
inst_1 : LinearOrderedCommGroupWithZero Γ₀
_i : Valued R Γ₀
⊢ ∀ (x : R),
    Membership.mem (γ := Set R)
        {x : R |
          LT.lt.{v} (α := ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
            ((Valuation.restrict v : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) x :
              ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
            (0 : ValueGroup₀ (F := Valuation R Γ₀) v)}
        x →
      {x : R |
          LT.lt.{v} (α := ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
            ((Valuation.restrict v : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) x :
              ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
            (0 : ValueGroup₀ (F := Valuation R Γ₀) v)} ∈
        𝓝 x

Tactic:
simp
-- Module: Mathlib.Topology.Algebra.Valued.ValuationTopology
Goal:
R : Type u
inst : Ring R
Γ₀ : Type v
inst_1 : LinearOrderedCommGroupWithZero Γ₀
_i : Valued R Γ₀
r : ValueGroup₀ (F := Valuation R Γ₀) v
hr : r ≠ 0
x : R
hx : Membership.mem (γ := Set R) {x : R | (Valuation.restrict v : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) x < r} x
inr :
  ∃ (γ : (ValueGroup₀ (F := Valuation R Γ₀) v)ˣ),
    Subset.{u} (α := Set R)
      {y : R | (Valuation.restrict v : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) (y - x) < (↑γ : ValueGroup₀ v)}
      {x : R | (Valuation.restrict v : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) x < r}
⊢ {x : R | (Valuation.restrict v : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) x < r} ∈ 𝓝 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 Γ₀
r : ValueGroup₀ (F := Valuation R Γ₀) v
hr : r ≠ 0
x : R
hx : Membership.mem (γ := Set R) {x : R | (Valuation.restrict v : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) x < r} x
⊢ ∃ (γ : (ValueGroup₀ (F := Valuation R Γ₀) v)ˣ),
    ∀ (a : R),
      (Valuation.restrict v : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) (a - x) < (↑γ : ValueGroup₀ v) →
        (Valuation.restrict v : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) a < r

Tactic:
⟨Units.mk0 _ hr,
    fun y hy ↦ (sub_add_cancel y x).symm ▸ (v.restrict.map_add _ x).trans_lt (max_lt hy hx)⟩

Premises used: Valuation.map_add, Valued.v, HSub.hSub, Eq.rec, max_lt, Units.mk0, Exists.intro, Eq.symm, LE.le.trans_lt, sub_add_cancel, Valuation.restrict
-- Module: Mathlib.Topology.Algebra.Valued.ValuationTopology
Goal:
R : Type u
inst : Ring R
Γ₀ : Type v
inst_1 : LinearOrderedCommGroupWithZero Γ₀
_i : Valued R Γ₀
r : ValueGroup₀ (F := Valuation R Γ₀) v
hr : r ≠ 0
x : R
hx : Membership.mem (γ := Set R) {x : R | (Valuation.restrict v : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) x < r} x
⊢ ∃ (γ : (ValueGroup₀ (F := Valuation R Γ₀) v)ˣ),
    ∀ (a : R),
      (Valuation.restrict v : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) (a - x) < (↑γ : ValueGroup₀ v) →
        (Valuation.restrict v : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) a < r

Tactic:
exact ⟨Units.mk0 _ hr,
    fun y hy ↦ (sub_add_cancel y x).symm ▸ (v.restrict.map_add _ x).trans_lt (max_lt hy hx)⟩
-- Module: Mathlib.Topology.Algebra.Valued.ValuationTopology
Goal:
R : Type u
inst : Ring R
Γ₀ : Type v
inst_1 : LinearOrderedCommGroupWithZero Γ₀
_i : Valued R Γ₀
r : ValueGroup₀ (F := Valuation R Γ₀) v
inl :
  IsClosed[_i.toTopologicalSpace]
    {x : R |
      LT.lt.{v} (α := ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
        ((Valuation.restrict v : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) x : ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
        (0 : ValueGroup₀ (F := Valuation R Γ₀) v)}
inr :
  ∀ (hr : r ≠ 0),
    IsClosed[_i.toTopologicalSpace] {x : R | (Valuation.restrict v : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) x < r}
⊢ IsClosed[_i.toTopologicalSpace] {x : R | (Valuation.restrict v : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) x < r}

Tactic:
rcases eq_or_ne r 0 with rfl | hr

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Topology.Algebra.Valued.ValuationTopology
Goal:
R : Type u
inst : Ring R
Γ₀ : Type v
inst_1 : LinearOrderedCommGroupWithZero Γ₀
_i : Valued R Γ₀
⊢ IsClosed[_i.toTopologicalSpace]
    {x : R |
      LT.lt.{v} (α := ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
        ((Valuation.restrict v : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) x : ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
        (0 : ValueGroup₀ (F := Valuation R Γ₀) v)}

Tactic:
simp
-- Module: Mathlib.Topology.Algebra.Valued.ValuationTopology
Goal:
R : Type u
inst : Ring R
Γ₀ : Type v
inst_1 : LinearOrderedCommGroupWithZero Γ₀
_i : Valued R Γ₀
r : ValueGroup₀ (F := Valuation R Γ₀) v
hr : r ≠ 0
⊢ IsClosed[_i.toTopologicalSpace] {x : R | (Valuation.restrict v : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) x < r}

Tactic:
AddSubgroup.isClosed_of_isOpen (Valuation.ltAddSubgroup v.restrict (Units.mk0 r hr))
    (isOpen_ball _ _)

Premises used: Set.Mem, Valued.v, setOf, AddSubgroup.isClosed_of_isOpen, Units.mk0, Valued.isOpen_ball, Valuation.ltAddSubgroup, Valuation.restrict
-- Module: Mathlib.Topology.Algebra.Valued.ValuationTopology
Goal:
R : Type u
inst : Ring R
Γ₀ : Type v
inst_1 : LinearOrderedCommGroupWithZero Γ₀
_i : Valued R Γ₀
r : ValueGroup₀ (F := Valuation R Γ₀) v
hr : r ≠ 0
⊢ IsClosed[_i.toTopologicalSpace] {x : R | (Valuation.restrict v : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) x < r}

Tactic:
exact AddSubgroup.isClosed_of_isOpen (Valuation.ltAddSubgroup v.restrict (Units.mk0 r hr))
    (isOpen_ball _ _)

Premises used: Valued.v, AddSubgroup.isClosed_of_isOpen, Units.mk0, Valued.isOpen_ball, Valuation.ltAddSubgroup, Valuation.restrict
-- Module: Mathlib.Topology.Algebra.Valued.ValuationTopology
Goal:
R : Type u
inst : Ring R
Γ₀ : Type v
inst_1 : LinearOrderedCommGroupWithZero Γ₀
_i : Valued R Γ₀
r : ValueGroup₀ (F := Valuation R Γ₀) v
⊢ IsClopen.{u} (X := R) {x : R | (Valuation.restrict v : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) x < r}

Tactic:
⟨isClosed_ball _ _, isOpen_ball _ _⟩

Premises used: Valued.isClosed_ball, Valued.isOpen_ball, And.intro, IsClopen
-- Module: Mathlib.Topology.Algebra.Valued.ValuationTopology
Goal:
R : Type u
inst : Ring R
Γ₀ : Type v
inst_1 : LinearOrderedCommGroupWithZero Γ₀
_i : Valued R Γ₀
r : ValueGroup₀ (F := Valuation R Γ₀) v
hr : r ≠ 0
rw :
  ∀ (x : R),
    Membership.mem (γ := Set R) {x : R | (Valuation.restrict v : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) x ≤ r} x →
      {x : R | (Valuation.restrict v : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) x ≤ r} ∈ 𝓝 x
⊢ IsOpen[_i.toTopologicalSpace] {x : R | (Valuation.restrict v : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) x ≤ r}

Tactic:
rw [isOpen_iff_mem_nhds]

Premises used: isOpen_iff_mem_nhds
-- Module: Mathlib.Topology.Algebra.Valued.ValuationTopology
Goal:
R : Type u
inst : Ring R
Γ₀ : Type v
inst_1 : LinearOrderedCommGroupWithZero Γ₀
_i : Valued R Γ₀
r : ValueGroup₀ (F := Valuation R Γ₀) v
hr : r ≠ 0
x : R
hx : Membership.mem (γ := Set R) {x : R | (Valuation.restrict v : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) x ≤ r} x
rw :
  ∃ (γ : (ValueGroup₀ (F := Valuation R Γ₀) v)ˣ),
    Subset.{u} (α := Set R)
      {y : R | (Valuation.restrict v : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) (y - x) < (↑γ : ValueGroup₀ v)}
      {x : R | (Valuation.restrict v : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) x ≤ r}
⊢ {x : R | (Valuation.restrict v : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) x ≤ r} ∈ 𝓝 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 Γ₀
r : ValueGroup₀ (F := Valuation R Γ₀) v
hr : r ≠ 0
x : R
hx : Membership.mem (γ := Set R) {x : R | (Valuation.restrict v : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) x ≤ r} x
⊢ ∃ (γ : (ValueGroup₀ (F := Valuation R Γ₀) v)ˣ),
    ∀ (a : R),
      (Valuation.restrict v : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) (a - x) < (↑γ : ValueGroup₀ v) →
        (Valuation.restrict v : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) a ≤ r

Tactic:
⟨Units.mk0 _ hr, fun y hy ↦
    (sub_add_cancel y x).symm ▸ le_trans (v.restrict.map_add _ _) (max_le (le_of_lt hy) hx)⟩

Premises used: Valuation.map_add, Valued.v, HSub.hSub, le_of_lt, Eq.rec, Units.mk0, max_le, Exists.intro, Eq.symm, sub_add_cancel, Valuation.restrict, le_trans
-- Module: Mathlib.Topology.Algebra.Valued.ValuationTopology
Goal:
R : Type u
inst : Ring R
Γ₀ : Type v
inst_1 : LinearOrderedCommGroupWithZero Γ₀
_i : Valued R Γ₀
r : ValueGroup₀ (F := Valuation R Γ₀) v
hr : r ≠ 0
x : R
hx : Membership.mem (γ := Set R) {x : R | (Valuation.restrict v : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) x ≤ r} x
⊢ ∃ (γ : (ValueGroup₀ (F := Valuation R Γ₀) v)ˣ),
    ∀ (a : R),
      (Valuation.restrict v : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) (a - x) < (↑γ : ValueGroup₀ v) →
        (Valuation.restrict v : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) a ≤ r

Tactic:
exact ⟨Units.mk0 _ hr, fun y hy ↦
    (sub_add_cancel y x).symm ▸ le_trans (v.restrict.map_add _ _) (max_le (le_of_lt hy) hx)⟩
-- Module: Mathlib.Topology.Algebra.Valued.ValuationTopology
Goal:
R : Type u
inst : Ring R
Γ₀ : Type v
inst_1 : LinearOrderedCommGroupWithZero Γ₀
_i : Valued R Γ₀
r : ValueGroup₀ (F := Valuation R Γ₀) v
rw :
  ∀ (x : R),
    Membership.mem (γ := Set R) {x : R | (Valuation.restrict v : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) x ≤ r}ᶜ x →
      {x : R | (Valuation.restrict v : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) x ≤ r}ᶜ ∈ 𝓝 x
⊢ IsClosed[_i.toTopologicalSpace] {x : R | (Valuation.restrict v : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) x ≤ r}

Tactic:
rw [← isOpen_compl_iff, isOpen_iff_mem_nhds]

Premises used: isOpen_iff_mem_nhds, isOpen_compl_iff