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 Γ₀
r : ValueGroup₀ (F := Valuation R Γ₀) v
x : R
hx : Membership.mem (γ := Set R) {x : R | (Valuation.restrict v : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) x ≤ r}ᶜ x
⊢ r < (Valuation.restrict v : (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.Valued.ValuationTopology
Goal:
R : Type u
inst : Ring R
Γ₀ : Type v
inst_1 : LinearOrderedCommGroupWithZero Γ₀
_i : Valued R Γ₀
r : ValueGroup₀ (F := Valuation R Γ₀) v
x : R
hx : r < (Valuation.restrict v : (a : R) → ValueGroup₀ (↑v : 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
x : R
hx : r < (Valuation.restrict v : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) x
⊢ 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 hx' : v.restrict x ≠ 0 := ne_of_gt <| lt_of_le_of_lt zero_le' <| 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
x : R
hx : r < (Valuation.restrict v : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) x
hx' :
  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 →*₀ Γ₀))
⊢ ∃ (γ : (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}ᶜ

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.Valued.ValuationTopology
Goal:
R : Type u
inst : Ring R
Γ₀ : Type v
inst_1 : LinearOrderedCommGroupWithZero Γ₀
_i : Valued R Γ₀
r : ValueGroup₀ (F := Valuation R Γ₀) v
x : R
hx : r < (Valuation.restrict v : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) x
hx' :
  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 →*₀ Γ₀))
⊢ ∃ (γ : (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}ᶜ

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.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
⊢ IsClopen.{u} (X := R) {x : R | (Valuation.restrict v : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) x ≤ r}

Tactic:
⟨isClosed_closedBall _ _, isOpen_closedBall _ hr⟩

Premises used: Valued.isOpen_closedBall, And.intro, Valued.isClosed_closedBall, 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
h :
  ∀ (x : R),
    Membership.mem (γ := Set R) {x : R | (Valuation.restrict v : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) x = r} x ↔
      Membership.mem (γ := Set R)
        ({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
⊢ Eq.{u + 1} (α := Set R) {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 : R | (Valuation.restrict v : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) x < r})

Tactic:
ext x
-- 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
⊢ Membership.mem (γ := Set R) {x : R | (Valuation.restrict v : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) x = r} x ↔
    Membership.mem (γ := Set R)
      ({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:
simp [← le_antisymm_iff]

Premises used: le_antisymm_iff
-- 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
⊢ Eq.{u + 1} (α := Set R) {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 : R | (Valuation.restrict v : (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.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
h :
  Eq.{u + 1} (α := Set R) {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 : R | (Valuation.restrict v : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) x < r})
rw :
  IsClopen.{u} (X := R)
    ({x : R | (Valuation.restrict v : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) x ≤ r} \
      {x : R | (Valuation.restrict v : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) x < r})
⊢ IsClopen.{u} (X := R) {x : R | (Valuation.restrict v : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) x = r}

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

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

Premises used: Valued.isClopen_ball, IsClopen.diff, Valued.isClopen_closedBall
-- 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
h :
  Eq.{u + 1} (α := Set R) {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 : R | (Valuation.restrict v : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) x < r})
⊢ IsClopen.{u} (X := R)
    ({x : R | (Valuation.restrict v : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) x ≤ r} \
      {x : R | (Valuation.restrict v : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) x < r})

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

Premises used: Valued.isClopen_ball, IsClopen.diff, Valued.isClopen_closedBall
-- 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
⊢ IsOpen[_i.toTopologicalSpace] {x : R | (Valuation.restrict v : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) x = r}

Tactic:
isClopen_sphere _ hr |>.isOpen

Premises used: Valued.isClopen_sphere, IsClopen.isOpen
-- 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 |
      Eq.{v + 1} (α := 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 |
      Eq.{v + 1} (α := 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:
simpa using isClosed_closedBall R 0

Premises used: Valued.isClosed_closedBall, OfNat.ofNat
-- 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:
isClopen_sphere _ hr |>.isClosed

Premises used: Valued.isClopen_sphere, IsClopen.isClosed
-- 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 isClopen_sphere _ hr |>.isClosed

Premises used: Valued.isClopen_sphere, IsClopen.isClosed
-- Module: Mathlib.Topology.Algebra.Valued.ValuationTopology
Goal:
R : Type u
inst : Ring R
Γ₀ : Type v
inst_1 : LinearOrderedCommGroupWithZero Γ₀
_i : Valued R Γ₀
simp :
  IsOpen[_i.toTopologicalSpace]
    {x : R |
      LE.le.{v} (α := ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
        ((Valuation.restrict v : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) x : ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
        (1 : ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))}
⊢ IsOpen[_i.toTopologicalSpace] (↑(integer v) : 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: Valued.v, 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.Valued.ValuationTopology
Goal:
R : Type u
inst : Ring R
Γ₀ : Type v
inst_1 : LinearOrderedCommGroupWithZero Γ₀
_i : Valued R Γ₀
⊢ IsOpen[_i.toTopologicalSpace]
    {x : R |
      LE.le.{v} (α := ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
        ((Valuation.restrict v : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) x : ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
        (1 : ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))}

Tactic:
isOpen_closedBall _ one_ne_zero

Premises used: setOf, Valued.isOpen_closedBall, one_ne_zero
-- Module: Mathlib.Topology.Algebra.Valued.ValuationTopology
Goal:
R : Type u
inst : Ring R
Γ₀ : Type v
inst_1 : LinearOrderedCommGroupWithZero Γ₀
_i : Valued R Γ₀
⊢ IsOpen[_i.toTopologicalSpace]
    {x : R |
      LE.le.{v} (α := ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
        ((Valuation.restrict v : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) x : ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
        (1 : ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))}

Tactic:
exact isOpen_closedBall _ one_ne_zero

Premises used: Valued.isOpen_closedBall, one_ne_zero
-- Module: Mathlib.Topology.Algebra.Valued.ValuationTopology
Goal:
R : Type u
inst : Ring R
Γ₀ : Type v
inst_1 : LinearOrderedCommGroupWithZero Γ₀
_i : Valued R Γ₀
simp :
  IsClosed[_i.toTopologicalSpace]
    {x : R |
      LE.le.{v} (α := ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
        ((Valuation.restrict v : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) x : ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
        (1 : ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))}
⊢ IsClosed[_i.toTopologicalSpace] (↑(integer v) : 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: Valued.v, 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.Valued.ValuationTopology
Goal:
R : Type u
inst : Ring R
Γ₀ : Type v
inst_1 : LinearOrderedCommGroupWithZero Γ₀
_i : Valued R Γ₀
⊢ IsClosed[_i.toTopologicalSpace]
    {x : R |
      LE.le.{v} (α := ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
        ((Valuation.restrict v : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) x : ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
        (1 : ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))}

Tactic:
isClosed_closedBall _ _

Premises used: setOf, Valued.isClosed_closedBall
-- 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 |
      LE.le.{v} (α := ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
        ((Valuation.restrict v : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) x : ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
        (1 : ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))}

Tactic:
exact isClosed_closedBall _ _

Premises used: Valued.isClosed_closedBall
-- Module: Mathlib.Topology.Algebra.Valued.ValuationTopology
Goal:
R : Type u
inst : Ring R
Γ₀ : Type v
inst_1 : LinearOrderedCommGroupWithZero Γ₀
_i : Valued R Γ₀
⊢ IsClopen (↑(integer v) : Set R)

Tactic:
⟨isClosed_integer _, isOpen_integer _⟩

Premises used: Valued.isClosed_integer, And.intro, Valued.isOpen_integer, IsClopen
-- Module: Mathlib.Topology.Algebra.Valued.ValuationTopology
Goal:
Γ₀ : Type v
inst : LinearOrderedCommGroupWithZero Γ₀
K : Type u
inst_1 : Field K
hv : Valued K Γ₀
⊢ IsOpen[hv.toTopologicalSpace] (↑(valuationSubring v) : Set K)

Tactic:
isOpen_integer K

Premises used: Valued.isOpen_integer
-- Module: Mathlib.Topology.Algebra.Valued.ValuationTopology
Goal:
Γ₀ : Type v
inst : LinearOrderedCommGroupWithZero Γ₀
K : Type u
inst_1 : Field K
hv : Valued K Γ₀
⊢ IsClosed[hv.toTopologicalSpace] (↑(valuationSubring v) : Set K)

Tactic:
isClosed_integer K

Premises used: Valued.isClosed_integer
-- Module: Mathlib.Topology.Algebra.Valued.ValuationTopology
Goal:
Γ₀ : Type v
inst : LinearOrderedCommGroupWithZero Γ₀
K : Type u
inst_1 : Field K
hv : Valued K Γ₀
⊢ IsClopen (↑(valuationSubring v) : Set K)

Tactic:
isClopen_integer K

Premises used: Valued.isClopen_integer
-- Module: Mathlib.Topology.Algebra.Valued.ValuedField
Goal:
K : Type u_1
inst : DivisionRing K
Γ₀ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation K Γ₀
x y : K
γ : Γ₀ˣ
y_ne : y ≠ 0
h :
  (v : (a : K) → Γ₀) (x - y) <
    min ((↑γ : Γ₀) * HMul.hMul (α := Γ₀) (β := Γ₀) ((v : (a : K) → Γ₀) y : Γ₀) ((v : (a : K) → Γ₀) y : Γ₀))
      ((v : (a : K) → Γ₀) y)
⊢ (v : (a : K) → Γ₀) (x - y) <
    (↑γ : Γ₀) * HMul.hMul (α := Γ₀) (β := Γ₀) ((v : (a : K) → Γ₀) y : Γ₀) ((v : (a : K) → Γ₀) y : Γ₀)

Tactic:
have hyp1 : v (x - y) < γ * (v y * v y) := lt_of_lt_of_le h (min_le_left _ _)
-- Module: Mathlib.Topology.Algebra.Valued.ValuedField
Goal:
K : Type u_1
inst : DivisionRing K
Γ₀ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation K Γ₀
x y : K
γ : Γ₀ˣ
y_ne : y ≠ 0
h :
  (v : (a : K) → Γ₀) (x - y) <
    min ((↑γ : Γ₀) * HMul.hMul (α := Γ₀) (β := Γ₀) ((v : (a : K) → Γ₀) y : Γ₀) ((v : (a : K) → Γ₀) y : Γ₀))
      ((v : (a : K) → Γ₀) y)
hyp1 :
  (v : (a : K) → Γ₀) (x - y) <
    (↑γ : Γ₀) * HMul.hMul (α := Γ₀) (β := Γ₀) ((v : (a : K) → Γ₀) y : Γ₀) ((v : (a : K) → Γ₀) y : Γ₀)
⊢ HMul.hMul (α := Γ₀) ((v : (a : K) → Γ₀) (x - y) : Γ₀)
      (HMul.hMul (α := Γ₀) (β := Γ₀) ((v : (a : K) → Γ₀) y : Γ₀) ((v : (a : K) → Γ₀) y : Γ₀))⁻¹ <
    (↑γ : Γ₀)

Tactic:
have hyp1' : v (x - y) * (v y * v y)⁻¹ < γ := mul_inv_lt_of_lt_mul₀ hyp1
-- Module: Mathlib.Topology.Algebra.Valued.ValuedField
Goal:
K : Type u_1
inst : DivisionRing K
Γ₀ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation K Γ₀
x y : K
γ : Γ₀ˣ
y_ne : y ≠ 0
h :
  (v : (a : K) → Γ₀) (x - y) <
    min ((↑γ : Γ₀) * HMul.hMul (α := Γ₀) (β := Γ₀) ((v : (a : K) → Γ₀) y : Γ₀) ((v : (a : K) → Γ₀) y : Γ₀))
      ((v : (a : K) → Γ₀) y)
hyp1 :
  (v : (a : K) → Γ₀) (x - y) <
    (↑γ : Γ₀) * HMul.hMul (α := Γ₀) (β := Γ₀) ((v : (a : K) → Γ₀) y : Γ₀) ((v : (a : K) → Γ₀) y : Γ₀)
hyp1' :
  HMul.hMul (α := Γ₀) ((v : (a : K) → Γ₀) (x - y) : Γ₀)
      (HMul.hMul (α := Γ₀) (β := Γ₀) ((v : (a : K) → Γ₀) y : Γ₀) ((v : (a : K) → Γ₀) y : Γ₀))⁻¹ <
    (↑γ : Γ₀)
⊢ LT.lt.{u_2} (α := Γ₀) ((v : (a : K) → Γ₀) (x - y) : Γ₀) ((v : (a : K) → Γ₀) y : Γ₀)

Tactic:
have hyp2 : v (x - y) < v y := lt_of_lt_of_le h (min_le_right _ _)
-- Module: Mathlib.Topology.Algebra.Valued.ValuedField
Goal:
K : Type u_1
inst : DivisionRing K
Γ₀ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation K Γ₀
x y : K
γ : Γ₀ˣ
y_ne : y ≠ 0
h :
  (v : (a : K) → Γ₀) (x - y) <
    min ((↑γ : Γ₀) * HMul.hMul (α := Γ₀) (β := Γ₀) ((v : (a : K) → Γ₀) y : Γ₀) ((v : (a : K) → Γ₀) y : Γ₀))
      ((v : (a : K) → Γ₀) y)
hyp1 :
  (v : (a : K) → Γ₀) (x - y) <
    (↑γ : Γ₀) * HMul.hMul (α := Γ₀) (β := Γ₀) ((v : (a : K) → Γ₀) y : Γ₀) ((v : (a : K) → Γ₀) y : Γ₀)
hyp1' :
  HMul.hMul (α := Γ₀) ((v : (a : K) → Γ₀) (x - y) : Γ₀)
      (HMul.hMul (α := Γ₀) (β := Γ₀) ((v : (a : K) → Γ₀) y : Γ₀) ((v : (a : K) → Γ₀) y : Γ₀))⁻¹ <
    (↑γ : Γ₀)
hyp2 : LT.lt.{u_2} (α := Γ₀) ((v : (a : K) → Γ₀) (x - y) : Γ₀) ((v : (a : K) → Γ₀) y : Γ₀)
⊢ Eq.{u_2 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) ((v : (a : K) → Γ₀) y : Γ₀)

Tactic:
have key : v x = v y := Valuation.map_eq_of_sub_lt v hyp2
-- Module: Mathlib.Topology.Algebra.Valued.ValuedField
Goal:
K : Type u_1
inst : DivisionRing K
Γ₀ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation K Γ₀
x y : K
γ : Γ₀ˣ
y_ne : y ≠ 0
h_1 :
  (v : (a : K) → Γ₀) (x - y) <
    min ((↑γ : Γ₀) * HMul.hMul (α := Γ₀) (β := Γ₀) ((v : (a : K) → Γ₀) y : Γ₀) ((v : (a : K) → Γ₀) y : Γ₀))
      ((v : (a : K) → Γ₀) y)
hyp1 :
  (v : (a : K) → Γ₀) (x - y) <
    (↑γ : Γ₀) * HMul.hMul (α := Γ₀) (β := Γ₀) ((v : (a : K) → Γ₀) y : Γ₀) ((v : (a : K) → Γ₀) y : Γ₀)
hyp1' :
  HMul.hMul (α := Γ₀) ((v : (a : K) → Γ₀) (x - y) : Γ₀)
      (HMul.hMul (α := Γ₀) (β := Γ₀) ((v : (a : K) → Γ₀) y : Γ₀) ((v : (a : K) → Γ₀) y : Γ₀))⁻¹ <
    (↑γ : Γ₀)
hyp2 : LT.lt.{u_2} (α := Γ₀) ((v : (a : K) → Γ₀) (x - y) : Γ₀) ((v : (a : K) → Γ₀) y : Γ₀)
key : Eq.{u_2 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) ((v : (a : K) → Γ₀) y : Γ₀)
h : x = 0
apply : y = 0
⊢ False

Tactic:
apply y_ne
-- Module: Mathlib.Topology.Algebra.Valued.ValuedField
Goal:
K : Type u_1
inst : DivisionRing K
Γ₀ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation K Γ₀
x y : K
γ : Γ₀ˣ
y_ne : y ≠ 0
h_1 :
  (v : (a : K) → Γ₀) (x - y) <
    min ((↑γ : Γ₀) * HMul.hMul (α := Γ₀) (β := Γ₀) ((v : (a : K) → Γ₀) y : Γ₀) ((v : (a : K) → Γ₀) y : Γ₀))
      ((v : (a : K) → Γ₀) y)
hyp1 :
  (v : (a : K) → Γ₀) (x - y) <
    (↑γ : Γ₀) * HMul.hMul (α := Γ₀) (β := Γ₀) ((v : (a : K) → Γ₀) y : Γ₀) ((v : (a : K) → Γ₀) y : Γ₀)
hyp1' :
  HMul.hMul (α := Γ₀) ((v : (a : K) → Γ₀) (x - y) : Γ₀)
      (HMul.hMul (α := Γ₀) (β := Γ₀) ((v : (a : K) → Γ₀) y : Γ₀) ((v : (a : K) → Γ₀) y : Γ₀))⁻¹ <
    (↑γ : Γ₀)
hyp2 : LT.lt.{u_2} (α := Γ₀) ((v : (a : K) → Γ₀) (x - y) : Γ₀) ((v : (a : K) → Γ₀) y : Γ₀)
key : Eq.{u_2 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) ((v : (a : K) → Γ₀) y : Γ₀)
h : x = 0
⊢ Eq.{u_2 + 1} (α := Γ₀) (0 : Γ₀) ((v : (a : K) → Γ₀) y : Γ₀)

Tactic:
rw [h, v.map_zero] at key

Premises used: Valuation.map_zero
-- Module: Mathlib.Topology.Algebra.Valued.ValuedField
Goal:
K : Type u_1
inst : DivisionRing K
Γ₀ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation K Γ₀
x y : K
γ : Γ₀ˣ
y_ne : y ≠ 0
h_1 :
  (v : (a : K) → Γ₀) (x - y) <
    min ((↑γ : Γ₀) * HMul.hMul (α := Γ₀) (β := Γ₀) ((v : (a : K) → Γ₀) y : Γ₀) ((v : (a : K) → Γ₀) y : Γ₀))
      ((v : (a : K) → Γ₀) y)
hyp1 :
  (v : (a : K) → Γ₀) (x - y) <
    (↑γ : Γ₀) * HMul.hMul (α := Γ₀) (β := Γ₀) ((v : (a : K) → Γ₀) y : Γ₀) ((v : (a : K) → Γ₀) y : Γ₀)
hyp1' :
  HMul.hMul (α := Γ₀) ((v : (a : K) → Γ₀) (x - y) : Γ₀)
      (HMul.hMul (α := Γ₀) (β := Γ₀) ((v : (a : K) → Γ₀) y : Γ₀) ((v : (a : K) → Γ₀) y : Γ₀))⁻¹ <
    (↑γ : Γ₀)
hyp2 : LT.lt.{u_2} (α := Γ₀) ((v : (a : K) → Γ₀) (x - y) : Γ₀) ((v : (a : K) → Γ₀) y : Γ₀)
key : Eq.{u_2 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) ((v : (a : K) → Γ₀) y : Γ₀)
h : x = 0
key₁ : Eq.{u_2 + 1} (α := Γ₀) (0 : Γ₀) ((v : (a : K) → Γ₀) y : Γ₀)
⊢ x = 0

Tactic:
rw [h, v.map_zero] at key

Premises used: Valuation.map_zero
-- Module: Mathlib.Topology.Algebra.Valued.ValuedField
Goal:
K : Type u_1
inst : DivisionRing K
Γ₀ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation K Γ₀
x y : K
γ : Γ₀ˣ
y_ne : y ≠ 0
h_1 :
  (v : (a : K) → Γ₀) (x - y) <
    min ((↑γ : Γ₀) * HMul.hMul (α := Γ₀) (β := Γ₀) ((v : (a : K) → Γ₀) y : Γ₀) ((v : (a : K) → Γ₀) y : Γ₀))
      ((v : (a : K) → Γ₀) y)
hyp1 :
  (v : (a : K) → Γ₀) (x - y) <
    (↑γ : Γ₀) * HMul.hMul (α := Γ₀) (β := Γ₀) ((v : (a : K) → Γ₀) y : Γ₀) ((v : (a : K) → Γ₀) y : Γ₀)
hyp1' :
  HMul.hMul (α := Γ₀) ((v : (a : K) → Γ₀) (x - y) : Γ₀)
      (HMul.hMul (α := Γ₀) (β := Γ₀) ((v : (a : K) → Γ₀) y : Γ₀) ((v : (a : K) → Γ₀) y : Γ₀))⁻¹ <
    (↑γ : Γ₀)
hyp2 : LT.lt.{u_2} (α := Γ₀) ((v : (a : K) → Γ₀) (x - y) : Γ₀) ((v : (a : K) → Γ₀) y : Γ₀)
key : Eq.{u_2 + 1} (α := Γ₀) (0 : Γ₀) ((v : (a : K) → Γ₀) y : Γ₀)
h : x = 0
⊢ y = 0

Tactic:
v.zero_iff.1 key.symm

Premises used: Valuation.zero_iff, Iff.mp, Eq.symm