awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Algebra.ValuativeRel.ValuativeTopology (goal)
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
⊢ _u = IsTopologicalAddGroup.rightUniformSpace R
have refine : (𝓤 R).HasBasis (fun (x : (ValueGroup₀ v)ˣ) ↦ True) fun (γ : (ValueGroup₀ v)ˣ) ↦
  {p : R × R | (v.restrict : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) (p.2 - p.1) < (↑γ : ValueGroup₀ v)}
Tactic: refine UniformSpace.ext (v.hasBasis_uniformity.eq_of_same_basis ?_)
-- Lean 4 proof step from Mathlib.Topology.Algebra.ValuativeRel.ValuativeTopology (goal)
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
⊢ (𝓤 R).HasBasis (fun (x : (ValueGroup₀ v)ˣ) ↦ True) fun (γ : (ValueGroup₀ v)ˣ) ↦
    {p : R × R | (v.restrict : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) (p.2 - p.1) < (↑γ : ValueGroup₀ v)}
have h : ∀ (x : (ValueGroup₀ v)ˣ),
  Eq (α := Set (R × R))
    {p : R × R | (v.restrict : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) (p.2 - p.1) < (↑x : ValueGroup₀ v)}
    ((fun (p : R × R) ↦ p.2 + -p.1) ⁻¹'
      (↑(v.ltAddSubgroup ((Units.map (↑embedding : ValueGroup₀ v →* Γ₀) : (a : (ValueGroup₀ v)ˣ) → Γ₀ˣ) x)) : Set R))
Tactic: convert! v.subgroups_basis.hasBasis_nhds_zero.comap _
-- Lean 4 proof step from Mathlib.Topology.Algebra.ValuativeRel.ValuativeTopology (goal)
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
⊢ Cauchy F ↔
    F.NeBot ∧
      ∀ (γ : (ValueGroup₀ v)ˣ),
        ∃ M ∈ F, ∀ x ∈ M, ∀ y ∈ M, (v.restrict : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) (y - x) < (↑γ : ValueGroup₀ v)
have 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)
Tactic: rw [v.toUniformSpace_eq, AddGroupFilterBasis.cauchy_iff]
-- Lean 4 proof step from Mathlib.Topology.Algebra.ValuativeRel.ValuativeTopology (goal)
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
⊢ (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)
have 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)
Tactic: apply and_congr Iff.rfl
-- Lean 4 proof step from Mathlib.Topology.Algebra.ValuativeRel.ValuativeTopology (goal)
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
⊢ (∀ (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)
have 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)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Algebra.ValuativeRel.ValuativeTopology (goal)
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)
⊢ (∀ (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)
have 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
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Algebra.ValuativeRel.ValuativeTopology (goal)
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, (v.restrict : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) (y - x) < (↑γ : ValueGroup₀ v)
have mp : ∃ 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]
-- Lean 4 proof step from Mathlib.Topology.Algebra.ValuativeRel.ValuativeTopology (hypothesis)
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)ˣ
⊢ ∃ M ∈ F,
    ∀ x ∈ M,
      ∀ y ∈ M,
        y - x ∈
          (↑(v.ltAddSubgroup ((Units.map (↑embedding : ValueGroup₀ v →* Γ₀) : (a : (ValueGroup₀ v)ˣ) → Γ₀ˣ) γ)) : Set R)
have h₁ : ∀ (γ : (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
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Topology.Algebra.ValuativeRel.ValuativeTopology (goal)
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
have h : _t = topologicalSpace R
Tactic: convert! (ValuativeRel.nonarchimedeanRing R).toIsTopologicalRing
-- Lean 4 proof step from Mathlib.Topology.Algebra.ValuativeRel.ValuativeTopology (goal)
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 : Γ₀)
⊢ DiscreteTopology R
have simp : ∃ (γ : (ValueGroup₀ v)ˣ),
  ∀ (y : R), (v.restrict : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) y < (↑γ : ValueGroup₀ v) → y = 0
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]
-- Lean 4 proof step from Mathlib.Topology.Algebra.ValuativeRel.ValuativeTopology (goal)
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 : Γ₀)
⊢ ∃ (γ : (ValueGroup₀ v)ˣ),
    ∀ (y : R), (v.restrict : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) y < (↑γ : ValueGroup₀ v) → y = 0
have 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
Tactic: use 1
-- Lean 4 proof step from Mathlib.Topology.Algebra.ValuativeRel.ValuativeTopology (goal)
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 : Γ₀)
⊢ ∀ (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
have 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 : Γ₀)
Tactic: contrapose! h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Topology.Algebra.ValuativeRel.ValuativeTopology (goal)
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
⊢ ∃ (x : R), x ≠ 0 ∧ Ne.{u_3 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) (1 : Γ₀)
have 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 : Γ₀)
Tactic: obtain ⟨x, hx, hx'⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Topology.Algebra.ValuativeRel.ValuativeTopology (hypothesis)
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
⊢ ∃ (x : R), x ≠ 0 ∧ Ne.{u_3 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) (1 : Γ₀)
have hx₁ : LT.lt.{u_3} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) (1 : Γ₀)
Tactic: rw [restrict_lt_iff_lt_embedding, Units.val_one, map_one] at hx
Cleared hypotheses: hx, hx'
-- Lean 4 proof step from Mathlib.Topology.Algebra.ValuativeRel.ValuativeTopology (goal)
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
⊢ IsOpen[_t] {x : R | (v.restrict : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) x < r}
have 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
Tactic: rw [isOpen_iff_mem_nhds]
-- Lean 4 proof step from Mathlib.Topology.Algebra.ValuativeRel.ValuativeTopology (goal)
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),
    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
have 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
Tactic: rcases eq_or_ne r 0 with rfl | hr
Cleared hypotheses: r
-- Lean 4 proof step from Mathlib.Topology.Algebra.ValuativeRel.ValuativeTopology (goal)
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
⊢ ∀ (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
have 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
Tactic: rcases eq_or_ne r 0 with rfl | hr
-- Lean 4 proof step from Mathlib.Topology.Algebra.ValuativeRel.ValuativeTopology (goal)
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
⊢ {x : R | (v.restrict : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) x < r} ∈ 𝓝 x
have 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}
Tactic: rw [v.mem_nhds_iff]
-- Lean 4 proof step from Mathlib.Topology.Algebra.ValuativeRel.ValuativeTopology (goal)
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
⊢ IsClosed[_t] {x : R | (v.restrict : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) x < r}
have 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)}
Tactic: rcases eq_or_ne r 0 with rfl | hr
Cleared hypotheses: r
-- Lean 4 proof step from Mathlib.Topology.Algebra.ValuativeRel.ValuativeTopology (goal)
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)}
⊢ IsClosed[_t] {x : R | (v.restrict : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) x < r}
have inr : ∀ (hr : r ≠ 0), IsClosed[_t] {x : R | (v.restrict : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) x < r}
Tactic: rcases eq_or_ne r 0 with rfl | hr
-- Lean 4 proof step from Mathlib.Topology.Algebra.ValuativeRel.ValuativeTopology (goal)
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}
have 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
Tactic: rw [isOpen_iff_mem_nhds]
-- Lean 4 proof step from Mathlib.Topology.Algebra.ValuativeRel.ValuativeTopology (goal)
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
⊢ {x : R | (v.restrict : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) x ≤ r} ∈ 𝓝 x
have 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
Tactic: simp only [v.mem_nhds_iff, setOf_subset_setOf]
-- Lean 4 proof step from Mathlib.Topology.Algebra.ValuativeRel.ValuativeTopology (goal)
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
⊢ IsClosed[_t] {x : R | (v.restrict : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) x ≤ r}
have 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
Tactic: rw [← isOpen_compl_iff, isOpen_iff_mem_nhds]
-- Lean 4 proof step from Mathlib.Topology.Algebra.ValuativeRel.ValuativeTopology (hypothesis)
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
⊢ {x : R | (v.restrict : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) x ≤ r}ᶜ ∈ 𝓝 x
have hx₁ : r < (v.restrict : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) x
Tactic: simp only [mem_compl_iff, mem_setOf_eq, not_le] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Topology.Algebra.ValuativeRel.ValuativeTopology (goal)
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
⊢ {x : R | (v.restrict : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) x ≤ r}ᶜ ∈ 𝓝 x
have 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}ᶜ
Tactic: rw [v.mem_nhds_iff]
-- Lean 4 proof step from Mathlib.Topology.Algebra.ValuativeRel.ValuativeTopology (hypothesis)
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
⊢ ∃ (γ : (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}ᶜ
have 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 →*₀ Γ₀))
Tactic: have hx' : v.restrict x ≠ 0 := ne_of_gt <| lt_of_le_of_lt zero_le' <| hx
-- Lean 4 proof step from Mathlib.Topology.Algebra.ValuativeRel.ValuativeTopology (goal)
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})
have 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
Tactic: ext x