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 Γ₀
_t : TopologicalSpace R
inst_3 : IsValuativeTopology R
v : Valuation R Γ₀
inst_4 : v.Compatible
r : ValueGroup₀ v
inl :
  IsClosed[_t]
    {x : R |
      LT.lt.{u_3} (α := ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
        ((v.restrict : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) x : ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
        (0 : ValueGroup₀ v)}
inr : ∀ (hr : r ≠ 0), IsClosed[_t] {x : R | (v.restrict : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) x < r}
⊢ IsClosed[_t] {x : R | (v.restrict : (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.ValuativeRel.ValuativeTopology
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
Γ₀ : Type u_3
inst_2 : LinearOrderedCommGroupWithZero Γ₀
_t : TopologicalSpace R
inst_3 : IsValuativeTopology R
v : Valuation R Γ₀
inst_4 : v.Compatible
⊢ IsClosed[_t]
    {x : R |
      LT.lt.{u_3} (α := ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
        ((v.restrict : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) x : ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
        (0 : ValueGroup₀ v)}

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 Γ₀
_t : TopologicalSpace R
inst_3 : IsValuativeTopology R
v : Valuation R Γ₀
inst_4 : v.Compatible
r : ValueGroup₀ v
hr : r ≠ 0
⊢ IsClosed[_t] {x : R | (v.restrict : (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, setOf, AddSubgroup.isClosed_of_isOpen, Units.mk0, Valuation.isOpen_ball, Valuation.ltAddSubgroup, Valuation.restrict
-- Module: Mathlib.Topology.Algebra.ValuativeRel.ValuativeTopology
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
Γ₀ : Type u_3
inst_2 : LinearOrderedCommGroupWithZero Γ₀
_t : TopologicalSpace R
inst_3 : IsValuativeTopology R
v : Valuation R Γ₀
inst_4 : v.Compatible
r : ValueGroup₀ v
hr : r ≠ 0
⊢ IsClosed[_t] {x : R | (v.restrict : (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: AddSubgroup.isClosed_of_isOpen, Units.mk0, Valuation.isOpen_ball, Valuation.ltAddSubgroup, Valuation.restrict
-- Module: Mathlib.Topology.Algebra.ValuativeRel.ValuativeTopology
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
Γ₀ : Type u_3
inst_2 : LinearOrderedCommGroupWithZero Γ₀
_t : TopologicalSpace R
inst_3 : IsValuativeTopology R
v : Valuation R Γ₀
inst_4 : v.Compatible
r : ValueGroup₀ v
⊢ IsClopen.{u_1} (X := R) {x : R | (v.restrict : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) x < r}

Tactic:
⟨isClosed_ball _, isOpen_ball _⟩

Premises used: And.intro, Valuation.isOpen_ball, Valuation.isClosed_ball, IsClopen
-- Module: Mathlib.Topology.Algebra.ValuativeRel.ValuativeTopology
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
Γ₀ : Type u_3
inst_2 : LinearOrderedCommGroupWithZero Γ₀
_t : TopologicalSpace R
inst_3 : IsValuativeTopology R
v : Valuation R Γ₀
inst_4 : v.Compatible
r : ValueGroup₀ v
hr : r ≠ 0
rw :
  ∀ (x : R),
    Membership.mem (γ := Set R) {x : R | (v.restrict : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) x ≤ r} x →
      {x : R | (v.restrict : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) x ≤ r} ∈ 𝓝 x
⊢ IsOpen[_t] {x : R | (v.restrict : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) x ≤ r}

Tactic:
rw [isOpen_iff_mem_nhds]

Premises used: isOpen_iff_mem_nhds
-- Module: Mathlib.Topology.Algebra.ValuativeRel.ValuativeTopology
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
Γ₀ : Type u_3
inst_2 : LinearOrderedCommGroupWithZero Γ₀
_t : TopologicalSpace R
inst_3 : IsValuativeTopology R
v : Valuation R Γ₀
inst_4 : v.Compatible
r : ValueGroup₀ v
hr : r ≠ 0
x : R
hx : Membership.mem (γ := Set R) {x : R | (v.restrict : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) x ≤ r} x
simp :
  ∃ (γ : (ValueGroup₀ v)ˣ),
    ∀ (a : R),
      (v.restrict : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) (a - x) < (↑γ : ValueGroup₀ v) →
        (v.restrict : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) a ≤ r
⊢ {x : R | (v.restrict : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) x ≤ r} ∈ 𝓝 x

Tactic:
simp only [v.mem_nhds_iff, setOf_subset_setOf]

Premises used: Set.setOf_subset_setOf, 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 Γ₀
_t : TopologicalSpace R
inst_3 : IsValuativeTopology R
v : Valuation R Γ₀
inst_4 : v.Compatible
r : ValueGroup₀ v
hr : r ≠ 0
x : R
hx : Membership.mem (γ := Set R) {x : R | (v.restrict : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) x ≤ r} x
⊢ ∃ (γ : (ValueGroup₀ v)ˣ),
    ∀ (a : R),
      (v.restrict : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) (a - x) < (↑γ : ValueGroup₀ v) →
        (v.restrict : (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, 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.ValuativeRel.ValuativeTopology
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
Γ₀ : Type u_3
inst_2 : LinearOrderedCommGroupWithZero Γ₀
_t : TopologicalSpace R
inst_3 : IsValuativeTopology R
v : Valuation R Γ₀
inst_4 : v.Compatible
r : ValueGroup₀ v
hr : r ≠ 0
x : R
hx : Membership.mem (γ := Set R) {x : R | (v.restrict : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) x ≤ r} x
⊢ ∃ (γ : (ValueGroup₀ v)ˣ),
    ∀ (a : R),
      (v.restrict : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) (a - x) < (↑γ : ValueGroup₀ v) →
        (v.restrict : (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.ValuativeRel.ValuativeTopology
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
Γ₀ : Type u_3
inst_2 : LinearOrderedCommGroupWithZero Γ₀
_t : TopologicalSpace R
inst_3 : IsValuativeTopology R
v : Valuation R Γ₀
inst_4 : v.Compatible
r : ValueGroup₀ v
rw :
  ∀ (x : R),
    Membership.mem (γ := Set R) {x : R | (v.restrict : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) x ≤ r}ᶜ x →
      {x : R | (v.restrict : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) x ≤ r}ᶜ ∈ 𝓝 x
⊢ IsClosed[_t] {x : R | (v.restrict : (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
-- Module: Mathlib.Topology.Algebra.ValuativeRel.ValuativeTopology
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
Γ₀ : Type u_3
inst_2 : LinearOrderedCommGroupWithZero Γ₀
_t : TopologicalSpace R
inst_3 : IsValuativeTopology R
v : Valuation R Γ₀
inst_4 : v.Compatible
r : ValueGroup₀ v
x : R
hx : Membership.mem (γ := Set R) {x : R | (v.restrict : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) x ≤ r}ᶜ x
⊢ r < (v.restrict : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) x

Tactic:
simp only [mem_compl_iff, mem_setOf_eq, not_le] at hx

Premises used: not_le, Set.mem_setOf_eq, Set.mem_compl_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 Γ₀
_t : TopologicalSpace R
inst_3 : IsValuativeTopology R
v : Valuation R Γ₀
inst_4 : v.Compatible
r : ValueGroup₀ v
x : R
hx : r < (v.restrict : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) x
rw :
  ∃ (γ : (ValueGroup₀ v)ˣ),
    Subset.{u_1} (α := Set R)
      {z : R | (v.restrict : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) (z - x) < (↑γ : ValueGroup₀ v)}
      {x : R | (v.restrict : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) x ≤ r}ᶜ
⊢ {x : R | (v.restrict : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) x ≤ r}ᶜ ∈ 𝓝 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 Γ₀
_t : TopologicalSpace R
inst_3 : IsValuativeTopology R
v : Valuation R Γ₀
inst_4 : v.Compatible
r : ValueGroup₀ v
x : R
hx : r < (v.restrict : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) x
⊢ 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 hx' : v.restrict x ≠ 0 := ne_of_gt <| lt_of_le_of_lt zero_le' <| hx
-- Module: Mathlib.Topology.Algebra.ValuativeRel.ValuativeTopology
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
Γ₀ : Type u_3
inst_2 : LinearOrderedCommGroupWithZero Γ₀
_t : TopologicalSpace R
inst_3 : IsValuativeTopology R
v : Valuation R Γ₀
inst_4 : v.Compatible
r : ValueGroup₀ v
x : R
hx : r < (v.restrict : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) x
hx' :
  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 →*₀ Γ₀))
⊢ ∃ (γ : (ValueGroup₀ v)ˣ),
    Subset.{u_1} (α := Set R)
      {z : R | (v.restrict : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) (z - x) < (↑γ : ValueGroup₀ v)}
      {x : R | (v.restrict : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) x ≤ r}ᶜ

Tactic:
⟨Units.mk0 _ hx', fun y hy hy' ↦ ne_of_lt hy <| map_sub_swap v.restrict x y ▸
      (Valuation.map_sub_eq_of_lt_left _ <| lt_of_le_of_lt hy' hx)⟩

Premises used: Units.mk0, Exists.intro, ne_of_lt
-- Module: Mathlib.Topology.Algebra.ValuativeRel.ValuativeTopology
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
Γ₀ : Type u_3
inst_2 : LinearOrderedCommGroupWithZero Γ₀
_t : TopologicalSpace R
inst_3 : IsValuativeTopology R
v : Valuation R Γ₀
inst_4 : v.Compatible
r : ValueGroup₀ v
x : R
hx : r < (v.restrict : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) x
hx' :
  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 →*₀ Γ₀))
⊢ ∃ (γ : (ValueGroup₀ v)ˣ),
    Subset.{u_1} (α := Set R)
      {z : R | (v.restrict : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) (z - x) < (↑γ : ValueGroup₀ v)}
      {x : R | (v.restrict : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) x ≤ r}ᶜ

Tactic:
exact ⟨Units.mk0 _ hx', fun y hy hy' ↦ ne_of_lt hy <| map_sub_swap v.restrict x y ▸
      (Valuation.map_sub_eq_of_lt_left _ <| lt_of_le_of_lt hy' hx)⟩
-- Module: Mathlib.Topology.Algebra.ValuativeRel.ValuativeTopology
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
Γ₀ : Type u_3
inst_2 : LinearOrderedCommGroupWithZero Γ₀
_t : TopologicalSpace R
inst_3 : IsValuativeTopology R
v : Valuation R Γ₀
inst_4 : v.Compatible
r : ValueGroup₀ v
hr : r ≠ 0
⊢ IsClopen.{u_1} (X := R) {x : R | (v.restrict : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) x ≤ r}

Tactic:
⟨isClosed_closedBall _, isOpen_closedBall hr⟩

Premises used: Valuation.isClosed_closedBall, And.intro, Valuation.isOpen_closedBall, IsClopen
-- Module: Mathlib.Topology.Algebra.ValuativeRel.ValuativeTopology
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
Γ₀ : Type u_3
inst_2 : LinearOrderedCommGroupWithZero Γ₀
_t : TopologicalSpace R
inst_3 : IsValuativeTopology R
v : Valuation R Γ₀
inst_4 : v.Compatible
r : ValueGroup₀ v
hr : r ≠ 0
h :
  ∀ (x : R),
    Membership.mem (γ := Set R) {x : R | (v.restrict : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) x = r} x ↔
      Membership.mem (γ := Set R)
        ({x : R | (v.restrict : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) x ≤ r} \
          {x : R | (v.restrict : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) x < r})
        x
⊢ Eq.{u_1 + 1} (α := Set R) {x : R | (v.restrict : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) x = r}
    ({x : R | (v.restrict : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) x ≤ r} \
      {x : R | (v.restrict : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) x < r})

Tactic:
ext x
-- Module: Mathlib.Topology.Algebra.ValuativeRel.ValuativeTopology
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
Γ₀ : Type u_3
inst_2 : LinearOrderedCommGroupWithZero Γ₀
_t : TopologicalSpace R
inst_3 : IsValuativeTopology R
v : Valuation R Γ₀
inst_4 : v.Compatible
r : ValueGroup₀ v
hr : r ≠ 0
x : R
⊢ Membership.mem (γ := Set R) {x : R | (v.restrict : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) x = r} x ↔
    Membership.mem (γ := Set R)
      ({x : R | (v.restrict : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) x ≤ r} \
        {x : R | (v.restrict : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) x < r})
      x

Tactic:
simp [← le_antisymm_iff]

Premises used: le_antisymm_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 Γ₀
_t : TopologicalSpace R
inst_3 : IsValuativeTopology R
v : Valuation R Γ₀
inst_4 : v.Compatible
r : ValueGroup₀ v
hr : r ≠ 0
⊢ Eq.{u_1 + 1} (α := Set R) {x : R | (v.restrict : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) x = r}
    ({x : R | (v.restrict : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) x ≤ r} \
      {x : R | (v.restrict : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) x < r})

Tactic:
have h : {x : R | v.restrict x = r} = {x | v.restrict x ≤ r} \ {x | v.restrict x < r} := by
    ext x
    simp [← le_antisymm_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 Γ₀
_t : TopologicalSpace R
inst_3 : IsValuativeTopology R
v : Valuation R Γ₀
inst_4 : v.Compatible
r : ValueGroup₀ v
hr : r ≠ 0
h :
  Eq.{u_1 + 1} (α := Set R) {x : R | (v.restrict : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) x = r}
    ({x : R | (v.restrict : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) x ≤ r} \
      {x : R | (v.restrict : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) x < r})
rw :
  IsClopen.{u_1} (X := R)
    ({x : R | (v.restrict : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) x ≤ r} \
      {x : R | (v.restrict : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) x < r})
⊢ IsClopen.{u_1} (X := R) {x : R | (v.restrict : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) x = r}

Tactic:
rw [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 Γ₀
_t : TopologicalSpace R
inst_3 : IsValuativeTopology R
v : Valuation R Γ₀
inst_4 : v.Compatible
r : ValueGroup₀ v
hr : r ≠ 0
h :
  Eq.{u_1 + 1} (α := Set R) {x : R | (v.restrict : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) x = r}
    ({x : R | (v.restrict : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) x ≤ r} \
      {x : R | (v.restrict : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) x < r})
⊢ IsClopen.{u_1} (X := R)
    ({x : R | (v.restrict : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) x ≤ r} \
      {x : R | (v.restrict : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) x < r})

Tactic:
IsClopen.diff (isClopen_closedBall hr) (isClopen_ball _)

Premises used: Valuation.isClopen_closedBall, IsClopen.diff, Valuation.isClopen_ball
-- Module: Mathlib.Topology.Algebra.ValuativeRel.ValuativeTopology
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
Γ₀ : Type u_3
inst_2 : LinearOrderedCommGroupWithZero Γ₀
_t : TopologicalSpace R
inst_3 : IsValuativeTopology R
v : Valuation R Γ₀
inst_4 : v.Compatible
r : ValueGroup₀ v
hr : r ≠ 0
h :
  Eq.{u_1 + 1} (α := Set R) {x : R | (v.restrict : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) x = r}
    ({x : R | (v.restrict : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) x ≤ r} \
      {x : R | (v.restrict : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) x < r})
⊢ IsClopen.{u_1} (X := R)
    ({x : R | (v.restrict : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) x ≤ r} \
      {x : R | (v.restrict : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) x < r})

Tactic:
exact IsClopen.diff (isClopen_closedBall hr) (isClopen_ball _)

Premises used: Valuation.isClopen_closedBall, IsClopen.diff, Valuation.isClopen_ball
-- Module: Mathlib.Topology.Algebra.ValuativeRel.ValuativeTopology
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
Γ₀ : Type u_3
inst_2 : LinearOrderedCommGroupWithZero Γ₀
_t : TopologicalSpace R
inst_3 : IsValuativeTopology R
v : Valuation R Γ₀
inst_4 : v.Compatible
r : ValueGroup₀ v
hr : r ≠ 0
⊢ IsOpen[_t] {x : R | (v.restrict : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) x = r}

Tactic:
isClopen_sphere hr |>.isOpen

Premises used: IsClopen.isOpen, Valuation.isClopen_sphere
-- Module: Mathlib.Topology.Algebra.ValuativeRel.ValuativeTopology
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
Γ₀ : Type u_3
inst_2 : LinearOrderedCommGroupWithZero Γ₀
_t : TopologicalSpace R
inst_3 : IsValuativeTopology R
v : Valuation R Γ₀
inst_4 : v.Compatible
r : ValueGroup₀ v
inl :
  IsClosed[_t]
    {x : R |
      Eq.{u_3 + 1} (α := ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
        ((v.restrict : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) x : ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
        (0 : ValueGroup₀ v)}
inr : ∀ (hr : r ≠ 0), IsClosed[_t] {x : R | (v.restrict : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) x = r}
⊢ IsClosed[_t] {x : R | (v.restrict : (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.ValuativeRel.ValuativeTopology
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
Γ₀ : Type u_3
inst_2 : LinearOrderedCommGroupWithZero Γ₀
_t : TopologicalSpace R
inst_3 : IsValuativeTopology R
v : Valuation R Γ₀
inst_4 : v.Compatible
⊢ IsClosed[_t]
    {x : R |
      LE.le.{u_3} (α := ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
        ((v.restrict : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) x : ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
        (0 : ValueGroup₀ v)}

Tactic:
v.isClosed_closedBall 0

Premises used: Valuation.isClosed_closedBall, OfNat.ofNat
-- Module: Mathlib.Topology.Algebra.ValuativeRel.ValuativeTopology
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
Γ₀ : Type u_3
inst_2 : LinearOrderedCommGroupWithZero Γ₀
_t : TopologicalSpace R
inst_3 : IsValuativeTopology R
v : Valuation R Γ₀
inst_4 : v.Compatible
h :
  ∀ (x : R),
    Eq.{u_3 + 1} (α := ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
        ((v.restrict : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) x : ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
        (0 : ValueGroup₀ v) ↔
      LE.le.{u_3} (α := ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
        ((v.restrict : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) x : ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
        (0 : ValueGroup₀ v)
⊢ IsClosed[_t]
    {x : R |
      Eq.{u_3 + 1} (α := ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
        ((v.restrict : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) x : ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
        (0 : ValueGroup₀ v)}

Tactic:
convert! v.isClosed_closedBall 0 using 3

Premises used: Valuation.isClosed_closedBall, OfNat.ofNat
-- Module: Mathlib.Topology.Algebra.ValuativeRel.ValuativeTopology
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
Γ₀ : Type u_3
inst_2 : LinearOrderedCommGroupWithZero Γ₀
_t : TopologicalSpace R
inst_3 : IsValuativeTopology R
v : Valuation R Γ₀
inst_4 : v.Compatible
x : R
⊢ Eq.{u_3 + 1} (α := ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
      ((v.restrict : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) x : ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
      (0 : ValueGroup₀ v) ↔
    LE.le.{u_3} (α := ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
      ((v.restrict : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) x : ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
      (0 : ValueGroup₀ v)

Tactic:
(le_zero_iff (α := ValueGroup₀ v)).symm

Premises used: le_zero_iff, Set.Mem, setOf, Iff.symm
-- Module: Mathlib.Topology.Algebra.ValuativeRel.ValuativeTopology
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
Γ₀ : Type u_3
inst_2 : LinearOrderedCommGroupWithZero Γ₀
_t : TopologicalSpace R
inst_3 : IsValuativeTopology R
v : Valuation R Γ₀
inst_4 : v.Compatible
x : R
⊢ Eq.{u_3 + 1} (α := ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
      ((v.restrict : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) x : ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
      (0 : ValueGroup₀ v) ↔
    LE.le.{u_3} (α := ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
      ((v.restrict : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) x : ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
      (0 : ValueGroup₀ v)

Tactic:
exact (le_zero_iff (α := ValueGroup₀ v)).symm

Premises used: le_zero_iff, Iff.symm
-- Module: Mathlib.Topology.Algebra.ValuativeRel.ValuativeTopology
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
Γ₀ : Type u_3
inst_2 : LinearOrderedCommGroupWithZero Γ₀
_t : TopologicalSpace R
inst_3 : IsValuativeTopology R
v : Valuation R Γ₀
inst_4 : v.Compatible
r : ValueGroup₀ v
hr : r ≠ 0
⊢ IsClosed[_t] {x : R | (v.restrict : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) x = r}

Tactic:
isClopen_sphere hr |>.isClosed

Premises used: IsClopen.isClosed, Valuation.isClopen_sphere
-- Module: Mathlib.Topology.Algebra.ValuativeRel.ValuativeTopology
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
Γ₀ : Type u_3
inst_2 : LinearOrderedCommGroupWithZero Γ₀
_t : TopologicalSpace R
inst_3 : IsValuativeTopology R
v : Valuation R Γ₀
inst_4 : v.Compatible
r : ValueGroup₀ v
hr : r ≠ 0
⊢ IsClosed[_t] {x : R | (v.restrict : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) x = r}

Tactic:
exact isClopen_sphere hr |>.isClosed

Premises used: IsClopen.isClosed, Valuation.isClopen_sphere
-- Module: Mathlib.Topology.Algebra.ValuativeRel.ValuativeTopology
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
Γ₀ : Type u_3
inst_2 : LinearOrderedCommGroupWithZero Γ₀
_t : TopologicalSpace R
inst_3 : IsValuativeTopology R
v : Valuation R Γ₀
inst_4 : v.Compatible
simp :
  IsOpen[_t]
    {x : R |
      LE.le.{u_3} (α := ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
        ((v.restrict : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) x : ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
        (1 : ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))}
⊢ IsOpen[_t] (↑v.integer : Set R)

Tactic:
simp only [integer, Subring.coe_set_mk, Subsemiring.coe_set_mk, Submonoid.coe_set_mk,
    Subsemigroup.coe_set_mk, ← v.restrict_le_one_iff]

Premises used: Subring.coe_set_mk, Subsemigroup.coe_set_mk, Valuation.restrict_le_one_iff, Subsemiring.coe_set_mk, Valuation.integer, Submonoid.coe_set_mk
-- Module: Mathlib.Topology.Algebra.ValuativeRel.ValuativeTopology
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
Γ₀ : Type u_3
inst_2 : LinearOrderedCommGroupWithZero Γ₀
_t : TopologicalSpace R
inst_3 : IsValuativeTopology R
v : Valuation R Γ₀
inst_4 : v.Compatible
⊢ IsOpen[_t]
    {x : R |
      LE.le.{u_3} (α := ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
        ((v.restrict : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) x : ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
        (1 : ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))}

Tactic:
apply isOpen_closedBall one_ne_zero

Premises used: Valuation.isOpen_closedBall, one_ne_zero