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 Γ₀
_u : UniformSpace R
inst_3 : IsUniformAddGroup R
inst_4 : IsValuativeTopology R
v : Valuation R Γ₀
inst_5 : v.Compatible
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₀ v)ˣ),
        ∃ M ∈ F, ∀ x ∈ M, ∀ y ∈ M, (v.restrict : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) (y - x) < (↑γ : ValueGroup₀ v)
⊢ Cauchy F ↔
    F.NeBot ∧
      ∀ (γ : (ValueGroup₀ v)ˣ),
        ∃ M ∈ F, ∀ x ∈ M, ∀ y ∈ M, (v.restrict : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) (y - x) < (↑γ : ValueGroup₀ v)

Tactic:
rw [v.toUniformSpace_eq, AddGroupFilterBasis.cauchy_iff]

Premises used: Valuation.toUniformSpace_eq, AddGroupFilterBasis.cauchy_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 Γ₀
_u : UniformSpace R
inst_3 : IsUniformAddGroup R
inst_4 : IsValuativeTopology R
v : Valuation R Γ₀
inst_5 : v.Compatible
F : Filter R
apply :
  (∀ (U : Set R),
      Membership.mem (γ := AddGroupFilterBasis R) RingFilterBasis.toAddGroupFilterBasis U →
        ∃ M ∈ F, ∀ x ∈ M, ∀ y ∈ M, y - x ∈ U) ↔
    ∀ (γ : (ValueGroup₀ v)ˣ),
      ∃ M ∈ F, ∀ x ∈ M, ∀ y ∈ M, (v.restrict : (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₀ v)ˣ),
        ∃ M ∈ F, ∀ x ∈ M, ∀ y ∈ M, (v.restrict : (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.ValuativeRel.ValuativeTopology
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
Γ₀ : Type u_3
inst_2 : LinearOrderedCommGroupWithZero Γ₀
_u : UniformSpace R
inst_3 : IsUniformAddGroup R
inst_4 : IsValuativeTopology R
v : Valuation R Γ₀
inst_5 : v.Compatible
F : Filter R
mp :
  (∀ (U : Set R),
      (∃ (i : (ValueGroup₀ v)ˣ),
          U =
            (↑(v.ltAddSubgroup ((Units.map (↑embedding : ValueGroup₀ v →* Γ₀) : (a : (ValueGroup₀ v)ˣ) → Γ₀ˣ) i)) :
              Set R)) →
        ∃ M ∈ F, ∀ x ∈ M, ∀ y ∈ M, y - x ∈ U) →
    ∀ (γ : (ValueGroup₀ v)ˣ),
      ∃ M ∈ F, ∀ x ∈ M, ∀ y ∈ M, (v.restrict : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) (y - x) < (↑γ : ValueGroup₀ v)
mpr :
  (∀ (γ : (ValueGroup₀ v)ˣ),
      ∃ M ∈ F, ∀ x ∈ M, ∀ y ∈ M, (v.restrict : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) (y - x) < (↑γ : ValueGroup₀ v)) →
    ∀ (U : Set R),
      (∃ (i : (ValueGroup₀ v)ˣ),
          U =
            (↑(v.ltAddSubgroup ((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₀ v)ˣ),
          U =
            (↑(v.ltAddSubgroup ((Units.map (↑embedding : ValueGroup₀ v →* Γ₀) : (a : (ValueGroup₀ v)ˣ) → Γ₀ˣ) i)) :
              Set R)) →
        ∃ M ∈ F, ∀ x ∈ M, ∀ y ∈ M, y - x ∈ U) ↔
    ∀ (γ : (ValueGroup₀ v)ˣ),
      ∃ M ∈ F, ∀ x ∈ M, ∀ y ∈ M, (v.restrict : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) (y - x) < (↑γ : ValueGroup₀ v)

Tactic:
constructor
-- Module: Mathlib.Topology.Algebra.ValuativeRel.ValuativeTopology
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
Γ₀ : Type u_3
inst_2 : LinearOrderedCommGroupWithZero Γ₀
_u : UniformSpace R
inst_3 : IsUniformAddGroup R
inst_4 : IsValuativeTopology R
v : Valuation R Γ₀
inst_5 : v.Compatible
F : Filter R
h :
  ∀ (U : Set R),
    (∃ (i : (ValueGroup₀ v)ˣ),
        U =
          (↑(v.ltAddSubgroup ((Units.map (↑embedding : ValueGroup₀ v →* Γ₀) : (a : (ValueGroup₀ v)ˣ) → Γ₀ˣ) i)) :
            Set R)) →
      ∃ M ∈ F, ∀ x ∈ M, ∀ y ∈ M, y - x ∈ U
γ : (ValueGroup₀ v)ˣ
mp :
  ∃ M ∈ F,
    ∀ x ∈ M,
      ∀ y ∈ M,
        LT.lt.{u_3} (α := Γ₀) ((v : (a : R) → Γ₀) (y - x) : Γ₀)
          ((embedding : (a : ValueGroup₀ v) → Γ₀) (↑γ : ValueGroup₀ v) : Γ₀)
⊢ ∃ M ∈ F, ∀ x ∈ M, ∀ y ∈ M, (v.restrict : (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.ValuativeRel.ValuativeTopology
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
Γ₀ : Type u_3
inst_2 : LinearOrderedCommGroupWithZero Γ₀
_u : UniformSpace R
inst_3 : IsUniformAddGroup R
inst_4 : IsValuativeTopology R
v : Valuation R Γ₀
inst_5 : v.Compatible
F : Filter R
h :
  ∀ (U : Set R),
    (∃ (i : (ValueGroup₀ v)ˣ),
        U =
          (↑(v.ltAddSubgroup ((Units.map (↑embedding : ValueGroup₀ v →* Γ₀) : (a : (ValueGroup₀ v)ˣ) → Γ₀ˣ) i)) :
            Set R)) →
      ∃ M ∈ F, ∀ x ∈ M, ∀ y ∈ M, y - x ∈ U
γ : (ValueGroup₀ v)ˣ
⊢ ∃ M ∈ F,
    ∀ x ∈ M,
      ∀ y ∈ M,
        LT.lt.{u_3} (α := Γ₀) ((v : (a : R) → Γ₀) (y - x) : Γ₀)
          ((embedding : (a : ValueGroup₀ v) → Γ₀) (↑γ : ValueGroup₀ v) : Γ₀)

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

Premises used: Set.Mem, setOf, Valuation.subgroups_basis, RingSubgroupsBasis.mem_addGroupFilterBasis
-- Module: Mathlib.Topology.Algebra.ValuativeRel.ValuativeTopology
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
Γ₀ : Type u_3
inst_2 : LinearOrderedCommGroupWithZero Γ₀
_u : UniformSpace R
inst_3 : IsUniformAddGroup R
inst_4 : IsValuativeTopology R
v : Valuation R Γ₀
inst_5 : v.Compatible
F : Filter R
h :
  ∀ (U : Set R),
    (∃ (i : (ValueGroup₀ v)ˣ),
        U =
          (↑(v.ltAddSubgroup ((Units.map (↑embedding : ValueGroup₀ v →* Γ₀) : (a : (ValueGroup₀ v)ˣ) → Γ₀ˣ) i)) :
            Set R)) →
      ∃ M ∈ F, ∀ x ∈ M, ∀ y ∈ M, y - x ∈ U
γ : (ValueGroup₀ v)ˣ
⊢ ∃ M ∈ F,
    ∀ x ∈ M,
      ∀ y ∈ M,
        LT.lt.{u_3} (α := Γ₀) ((v : (a : R) → Γ₀) (y - x) : Γ₀)
          ((embedding : (a : ValueGroup₀ v) → Γ₀) (↑γ : ValueGroup₀ v) : Γ₀)

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

Premises used: Valuation.subgroups_basis, RingSubgroupsBasis.mem_addGroupFilterBasis
-- Module: Mathlib.Topology.Algebra.ValuativeRel.ValuativeTopology
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
Γ₀ : Type u_3
inst_2 : LinearOrderedCommGroupWithZero Γ₀
_u : UniformSpace R
inst_3 : IsUniformAddGroup R
inst_4 : IsValuativeTopology R
v : Valuation R Γ₀
inst_5 : v.Compatible
F : Filter R
h :
  ∀ (γ : (ValueGroup₀ v)ˣ),
    ∃ M ∈ F, ∀ x ∈ M, ∀ y ∈ M, (v.restrict : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) (y - x) < (↑γ : ValueGroup₀ v)
γ : (ValueGroup₀ v)ˣ
⊢ ∀ (γ : (ValueGroup₀ v)ˣ),
    ∃ M ∈ F,
      ∀ x ∈ M,
        ∀ y ∈ M,
          LT.lt.{u_3} (α := Γ₀) ((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.ValuativeRel.ValuativeTopology
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
Γ₀ : Type u_3
inst_2 : LinearOrderedCommGroupWithZero Γ₀
_u : UniformSpace R
inst_3 : IsUniformAddGroup R
inst_4 : IsValuativeTopology R
v : Valuation R Γ₀
inst_5 : v.Compatible
F : Filter R
γ : (ValueGroup₀ v)ˣ
h :
  ∀ (γ : (ValueGroup₀ v)ˣ),
    ∃ M ∈ F,
      ∀ x ∈ M,
        ∀ y ∈ M,
          LT.lt.{u_3} (α := Γ₀) ((v : (a : R) → Γ₀) (y - x) : Γ₀)
            ((embedding : (a : ValueGroup₀ v) → Γ₀) (↑γ : ValueGroup₀ v) : Γ₀)
⊢ ∃ M ∈ F,
    ∀ x ∈ M,
      ∀ y ∈ M,
        y - x ∈
          (↑(v.ltAddSubgroup ((Units.map (↑embedding : ValueGroup₀ v →* Γ₀) : (a : (ValueGroup₀ v)ˣ) → Γ₀ˣ) γ)) : Set R)

Tactic:
h γ

Premises used: Set.Mem, setOf
-- Module: Mathlib.Topology.Algebra.ValuativeRel.ValuativeTopology
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
Γ₀ : Type u_3
inst_2 : LinearOrderedCommGroupWithZero Γ₀
_u : UniformSpace R
inst_3 : IsUniformAddGroup R
inst_4 : IsValuativeTopology R
v : Valuation R Γ₀
inst_5 : v.Compatible
F : Filter R
γ : (ValueGroup₀ v)ˣ
h :
  ∀ (γ : (ValueGroup₀ v)ˣ),
    ∃ M ∈ F,
      ∀ x ∈ M,
        ∀ y ∈ M,
          LT.lt.{u_3} (α := Γ₀) ((v : (a : R) → Γ₀) (y - x) : Γ₀)
            ((embedding : (a : ValueGroup₀ v) → Γ₀) (↑γ : ValueGroup₀ v) : Γ₀)
⊢ ∃ M ∈ F,
    ∀ x ∈ M,
      ∀ y ∈ M,
        y - x ∈
          (↑(v.ltAddSubgroup ((Units.map (↑embedding : ValueGroup₀ v →* Γ₀) : (a : (ValueGroup₀ v)ˣ) → Γ₀ˣ) γ)) : Set R)

Tactic:
exact 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
u : UniformSpace R := IsTopologicalAddGroup.rightUniformSpace R
this : IsUniformAddGroup R := ⋯
⊢ _t = ⋯.topology

Tactic:
congrArg (fun u ↦ @UniformSpace.toTopologicalSpace R u) v.toUniformSpace_eq

Premises used: congrArg, Valuation.toUniformSpace_eq, UniformSpace.toTopologicalSpace
-- 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
u : UniformSpace R := IsTopologicalAddGroup.rightUniformSpace R
this : IsUniformAddGroup R := ⋯
⊢ _t = ⋯.topology

Tactic:
exact congrArg (fun u ↦ @UniformSpace.toTopologicalSpace R u) v.toUniformSpace_eq

Premises used: congrArg, Valuation.toUniformSpace_eq, UniformSpace.toTopologicalSpace
-- Module: Mathlib.Topology.Algebra.ValuativeRel.ValuativeTopology
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
K : Type u_2
inst_2 : Field K
inst_3 : ValuativeRel K
Γ₀ : Type u_3
inst_4 : LinearOrderedCommGroupWithZero Γ₀
_t : TopologicalSpace R
inst_5 : IsValuativeTopology R
v : Valuation R Γ₀
inst_6 : v.Compatible
inst_7 : TopologicalSpace K
inst_8 : IsValuativeTopology K
⊢ IsTopologicalRing R

Tactic:
(ValuativeRel.nonarchimedeanRing R).toIsTopologicalRing

Premises used: NonarchimedeanRing.toIsTopologicalRing
-- Module: Mathlib.Topology.Algebra.ValuativeRel.ValuativeTopology
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
K : Type u_2
inst_2 : Field K
inst_3 : ValuativeRel K
Γ₀ : Type u_3
inst_4 : LinearOrderedCommGroupWithZero Γ₀
_t : TopologicalSpace R
inst_5 : IsValuativeTopology R
v : Valuation R Γ₀
inst_6 : v.Compatible
inst_7 : TopologicalSpace K
inst_8 : IsValuativeTopology K
h : _t = topologicalSpace R
⊢ IsTopologicalRing R

Tactic:
convert! (ValuativeRel.nonarchimedeanRing R).toIsTopologicalRing

Premises used: NonarchimedeanRing.toIsTopologicalRing
-- Module: Mathlib.Topology.Algebra.ValuativeRel.ValuativeTopology
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
K : Type u_2
inst_2 : Field K
inst_3 : ValuativeRel K
Γ₀ : Type u_3
inst_4 : LinearOrderedCommGroupWithZero Γ₀
_t : TopologicalSpace R
inst_5 : IsValuativeTopology R
v : Valuation R Γ₀
inst_6 : v.Compatible
inst_7 : TopologicalSpace K
inst_8 : IsValuativeTopology K
⊢ _t = topologicalSpace R

Tactic:
toTopologicalSpace_eq _

Premises used: Set.Mem, setOf, Valuation.toTopologicalSpace_eq
-- Module: Mathlib.Topology.Algebra.ValuativeRel.ValuativeTopology
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
K : Type u_2
inst_2 : Field K
inst_3 : ValuativeRel K
Γ₀ : Type u_3
inst_4 : LinearOrderedCommGroupWithZero Γ₀
_t : TopologicalSpace R
inst_5 : IsValuativeTopology R
v : Valuation R Γ₀
inst_6 : v.Compatible
inst_7 : TopologicalSpace K
inst_8 : IsValuativeTopology K
⊢ _t = topologicalSpace R

Tactic:
exact toTopologicalSpace_eq _

Premises used: Valuation.toTopologicalSpace_eq
-- 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), x ≠ 0 → Eq.{u_3 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) (1 : Γ₀)
simp :
  ∃ (γ : (ValueGroup₀ v)ˣ),
    ∀ (y : R), (v.restrict : (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, v.mem_nhds_zero_iff, subset_singleton_iff, mem_setOf_eq]

Premises used: Valuation.mem_nhds_zero_iff, Set.subset_singleton_iff, forall_eq, Set.mem_setOf_eq, Set.mem_singleton_iff, isOpen_iff_mem_nhds, discreteTopology_iff_isOpen_singleton_zero
-- Module: Mathlib.Topology.Algebra.ValuativeRel.ValuativeTopology
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
Γ₀ : Type u_3
inst_2 : LinearOrderedCommGroupWithZero Γ₀
_t : TopologicalSpace R
inst_3 : IsValuativeTopology R
v : Valuation R Γ₀
inst_4 : v.Compatible
h : ∀ (x : R), x ≠ 0 → Eq.{u_3 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) (1 : Γ₀)
h₁ :
  ∀ (y : R),
    LT.lt.{u_3} (α := ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
        ((v.restrict : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) y : ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
        ((↑1 : ValueGroup₀ v) : ValueGroup₀ v) →
      y = 0
⊢ ∃ (γ : (ValueGroup₀ v)ˣ),
    ∀ (y : R), (v.restrict : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) y < (↑γ : ValueGroup₀ v) → y = 0

Tactic:
use 1
-- 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), x ≠ 0 → Eq.{u_3 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) (1 : Γ₀)
h₁ :
  ∀
    (h :
      ∃ (y : R),
        LT.lt.{u_3} (α := ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
            ((v.restrict : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) y : ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
            ((↑1 : ValueGroup₀ v) : ValueGroup₀ v) ∧
          y ≠ 0),
    ∃ (x : R), x ≠ 0 ∧ Ne.{u_3 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) (1 : Γ₀)
⊢ ∀ (y : R),
    LT.lt.{u_3} (α := ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
        ((v.restrict : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) y : ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
        ((↑1 : ValueGroup₀ v) : ValueGroup₀ v) →
      y = 0

Tactic:
contrapose! 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
h :
  ∃ (y : R),
    LT.lt.{u_3} (α := ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
        ((v.restrict : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) y : ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
        ((↑1 : ValueGroup₀ v) : ValueGroup₀ v) ∧
      y ≠ 0
h₁ :
  ∀ (x : R)
    (hx :
      LT.lt.{u_3} (α := ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
        ((v.restrict : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) x : ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
        ((↑1 : ValueGroup₀ v) : ValueGroup₀ v))
    (hx' : x ≠ 0), ∃ (x : R), x ≠ 0 ∧ Ne.{u_3 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) (1 : Γ₀)
⊢ ∃ (x : R), x ≠ 0 ∧ Ne.{u_3 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) (1 : Γ₀)

Tactic:
obtain ⟨x, hx, hx'⟩ := 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
x : R
hx :
  LT.lt.{u_3} (α := ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
    ((v.restrict : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) x : ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
    ((↑1 : ValueGroup₀ v) : ValueGroup₀ v)
hx' : x ≠ 0
⊢ LT.lt.{u_3} (α := Γ₀) ((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.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
hx :
  LT.lt.{u_3} (α := ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
    ((v.restrict : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) x : ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
    ((↑1 : ValueGroup₀ v) : ValueGroup₀ v)
hx' : x ≠ 0
hx₁ : LT.lt.{u_3} (α := Γ₀) ((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.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
hx : LT.lt.{u_3} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) (1 : Γ₀)
hx' : x ≠ 0
⊢ ∃ (x : R), x ≠ 0 ∧ Ne.{u_3 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) (1 : Γ₀)

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

Premises used: And.intro, Exists.intro, LT.lt.ne
-- 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
hx : LT.lt.{u_3} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) (1 : Γ₀)
hx' : x ≠ 0
⊢ ∃ (x : R), x ≠ 0 ∧ Ne.{u_3 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) (1 : Γ₀)

Tactic:
exact ⟨x, hx', hx.ne⟩
-- Module: Mathlib.Topology.Algebra.ValuativeRel.ValuativeTopology
Goal:
K : Type u_2
inst : Field K
inst_1 : ValuativeRel K
Γ₀ : Type u_3
inst_2 : LinearOrderedCommGroupWithZero Γ₀
inst_3 : TopologicalSpace K
inst_4 : IsValuativeTopology K
inst_5 : MulArchimedean Γ₀
v : Valuation K Γ₀
inst_6 : v.Compatible
r : Γ₀
hr : r ≠ 0
h : ∀ (x : K), Ne.{u_3 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (0 : Γ₀) → r < (v : (a : K) → Γ₀) x
⊢ ∀ (x : K), x ≠ 0 → Eq.{u_3 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀)

Tactic:
simpa using v.map_eq_one_of_forall_lt hr h

Premises used: Valuation.map_eq_one_of_forall_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
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
inl :
  ∀ (x : R),
    Membership.mem (γ := Set R)
        {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)}
        x →
      {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)} ∈
        𝓝 x
inr :
  ∀ (hr : r ≠ 0) (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
⊢ ∀ (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

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
⊢ ∀ (x : R),
    Membership.mem (γ := Set R)
        {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)}
        x →
      {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)} ∈
        𝓝 x

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
x : R
hx : Membership.mem (γ := Set R) {x : R | (v.restrict : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) x < r} x
inr :
  ∃ (γ : (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
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 ▸ (v.restrict.map_add _ x).trans_lt (max_lt hy hx)⟩

Premises used: Valuation.map_add, 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.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 ▸ (v.restrict.map_add _ x).trans_lt (max_lt hy hx)⟩