awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Algebra.Valued.ValuationTopology (goal)
Goal:
R : Type u
inst : Ring R
Γ₀ : Type v
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
x : R
γ : (ValueGroup₀ v)ˣ
γx : Γ₀ˣ
Hx : (v : (a : R) → Γ₀) x = (↑γx : Γ₀)
u : (ValueGroup₀ v)ˣ :=
  Units.mk0 (((restrict₀ v : MonoidWithZeroHom.{u, v} R (ValueGroup₀ v)) : (a : R) → ValueGroup₀ v) x) ⋯
hu_def : u = Units.mk0 (((restrict₀ v : MonoidWithZeroHom.{u, v} R (ValueGroup₀ v)) : (a : R) → ValueGroup₀ v) x) ⋯
hu : (embedding : (a : ValueGroup₀ v) → Γ₀) (↑u⁻¹ : ValueGroup₀ v) = (↑γx⁻¹ : Γ₀)
⊢ ∃ (j : (ValueGroup₀ v)ˣ),
    (↑(v.ltAddSubgroup ((Units.map (↑embedding : ValueGroup₀ v →* Γ₀) : (a : (ValueGroup₀ v)ˣ) → Γ₀ˣ) j)) : Set R) ⊆
      (fun (x_1 : R) ↦ x_1 * x) ⁻¹'
        (↑(v.ltAddSubgroup ((Units.map (↑embedding : ValueGroup₀ v →* Γ₀) : (a : (ValueGroup₀ v)ˣ) → Γ₀ˣ) γ)) : Set R)
have h : (↑(v.ltAddSubgroup ((Units.map (↑embedding : ValueGroup₀ v →* Γ₀) : (a : (ValueGroup₀ v)ˣ) → Γ₀ˣ) (u⁻¹ * γ))) : Set R) ⊆
  (fun (x_1 : R) ↦ x_1 * x) ⁻¹'
    (↑(v.ltAddSubgroup ((Units.map (↑embedding : ValueGroup₀ v →* Γ₀) : (a : (ValueGroup₀ v)ˣ) → Γ₀ˣ) γ)) : Set R)
Tactic: use u⁻¹ * γ
-- Lean 4 proof step from Mathlib.Topology.Algebra.Valued.ValuationTopology (goal)
Goal:
R : Type u
inst : Ring R
Γ₀ : Type v
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
x : R
γ : (ValueGroup₀ v)ˣ
γx : Γ₀ˣ
Hx : (v : (a : R) → Γ₀) x = (↑γx : Γ₀)
u : (ValueGroup₀ v)ˣ :=
  Units.mk0 (((restrict₀ v : MonoidWithZeroHom.{u, v} R (ValueGroup₀ v)) : (a : R) → ValueGroup₀ v) x) ⋯
hu_def : u = Units.mk0 (((restrict₀ v : MonoidWithZeroHom.{u, v} R (ValueGroup₀ v)) : (a : R) → ValueGroup₀ v) x) ⋯
hu : (embedding : (a : ValueGroup₀ v) → Γ₀) (↑u⁻¹ : ValueGroup₀ v) = (↑γx⁻¹ : Γ₀)
y : R
vy_lt :
  LT.lt.{v} (α := Γ₀) ((v : (a : R) → Γ₀) y : Γ₀)
    ((embedding : (a : ValueGroup₀ v) → Γ₀) (↑(u⁻¹ * γ) : ValueGroup₀ v) : Γ₀)
⊢ Membership.mem (γ := Set R)
    ((fun (x_1 : R) ↦ x_1 * x) ⁻¹'
      (↑(v.ltAddSubgroup ((Units.map (↑embedding : ValueGroup₀ v →* Γ₀) : (a : (ValueGroup₀ v)ˣ) → Γ₀ˣ) γ)) : Set R))
    y
have h : HMul.hMul (α := Γ₀) ((v : (a : R) → Γ₀) y : Γ₀) (↑γx : Γ₀) <
  (↑((Units.map (↑embedding : ValueGroup₀ v →* Γ₀) : (a : (ValueGroup₀ v)ˣ) → Γ₀ˣ) γ) : Γ₀)
Tactic: simp only [coe_ltAddSubgroup, preimage_setOf_eq, mem_setOf_eq, Valuation.map_mul, Hx]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Valued.ValuationTopology (goal)
Goal:
R K : Type u
inst : Ring R
inst_1 : DivisionRing K
Γ₀ : Type v
inst_2 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
this : UniformSpace R := IsTopologicalAddGroup.rightUniformSpace R
s : Set R
⊢ Membership.mem (γ := Filter R) (𝓝 0) s ↔
    ∃ (γ : (ValueGroup₀ v)ˣ),
      {x : R | (v.restrict : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) x < (↑γ : ValueGroup₀ v)} ⊆ s
have rw : (∃ (i : (ValueGroup₀ v)ˣ),
    True ∧
      (↑(v.ltAddSubgroup ((Units.map (↑embedding : ValueGroup₀ v →* Γ₀) : (a : (ValueGroup₀ v)ˣ) → Γ₀ˣ) i)) : Set R) ⊆
        s) ↔
  ∃ (γ : (ValueGroup₀ v)ˣ), {x : R | (v.restrict : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) x < (↑γ : ValueGroup₀ v)} ⊆ s
Tactic: rw [Filter.hasBasis_iff.mp v.subgroups_basis.hasBasis_nhds_zero s]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Valued.ValuationTopology (goal)
Goal:
R K : Type u
inst : Ring R
inst_1 : DivisionRing K
Γ₀ : Type v
inst_2 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
this : UniformSpace R := IsTopologicalAddGroup.rightUniformSpace R
s : Set R
⊢ (∃ (i : (ValueGroup₀ v)ˣ),
      True ∧
        (↑(v.ltAddSubgroup ((Units.map (↑embedding : ValueGroup₀ v →* Γ₀) : (a : (ValueGroup₀ v)ˣ) → Γ₀ˣ) i)) : Set R) ⊆
          s) ↔
    ∃ (γ : (ValueGroup₀ v)ˣ),
      {x : R | (v.restrict : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) x < (↑γ : ValueGroup₀ v)} ⊆ s
have simp_rw : (∃ (i : (ValueGroup₀ v)ˣ),
    True ∧
      (↑(v.ltAddSubgroup ((Units.map (↑embedding : ValueGroup₀ v →* Γ₀) : (a : (ValueGroup₀ v)ˣ) → Γ₀ˣ) i)) : Set R) ⊆
        s) ↔
  ∃ (γ : (ValueGroup₀ v)ˣ),
    {x : R |
        LT.lt.{v} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀)
          ((embedding : (a : ValueGroup₀ v) → Γ₀) (↑γ : ValueGroup₀ v) : Γ₀)} ⊆
      s
Tactic: simp_rw [restrict_lt_iff_lt_embedding]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Valued.ValuationTopology (goal)
Goal:
R K : Type u
inst : Ring R
inst_1 : DivisionRing K
Γ₀ : Type v
inst_2 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
this : UniformSpace R := IsTopologicalAddGroup.rightUniformSpace R
s : Set R
γ : (ValueGroup₀ v)ˣ
⊢ True ∧
      (↑(v.ltAddSubgroup ((Units.map (↑embedding : ValueGroup₀ v →* Γ₀) : (a : (ValueGroup₀ v)ˣ) → Γ₀ˣ) γ)) : Set R) ⊆
        s ↔
    {x : R |
        LT.lt.{v} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀)
          ((embedding : (a : ValueGroup₀ v) → Γ₀) (↑γ : ValueGroup₀ v) : Γ₀)} ⊆
      s
have rw : (↑(v.ltAddSubgroup ((Units.map (↑embedding : ValueGroup₀ v →* Γ₀) : (a : (ValueGroup₀ v)ˣ) → Γ₀ˣ) γ)) : Set R) ⊆ s ↔
  {x : R |
      LT.lt.{v} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀)
        ((embedding : (a : ValueGroup₀ v) → Γ₀) (↑γ : ValueGroup₀ v) : Γ₀)} ⊆
    s
Tactic: rw [true_and]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Valued.ValuationTopology (goal)
Goal:
R : Type u
inst : Ring R
Γ₀ : Type v
inst_1 : LinearOrderedCommGroupWithZero Γ₀
_i : Valued R Γ₀
⊢ (𝓤 R).HasBasis (fun (x : (ValueGroup₀ (F := Valuation R Γ₀) v)ˣ) ↦ True)
    fun (γ : (ValueGroup₀ (F := Valuation R Γ₀) v)ˣ) ↦
    {p : R × R | (Valuation.restrict v : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) (p.2 - p.1) < (↑γ : ValueGroup₀ v)}
have rw : Filter.HasBasis.{u, v + 1} (α := R × R) (Filter.comap (β := R) (fun (x : R × R) ↦ x.2 - x.1) (𝓝 0))
  (fun (x : (ValueGroup₀ (F := Valuation R Γ₀) v)ˣ) ↦ True) fun (γ : (ValueGroup₀ (F := Valuation R Γ₀) v)ˣ) ↦
  {p : R × R | (Valuation.restrict v : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) (p.2 - p.1) < (↑γ : ValueGroup₀ v)}
Tactic: rw [uniformity_eq_comap_nhds_zero]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Valued.ValuationTopology (goal)
Goal:
R : Type u
inst : Ring R
Γ₀ : Type v
inst_1 : LinearOrderedCommGroupWithZero Γ₀
_i : Valued R Γ₀
⊢ @toUniformSpace _ inst _ inst_1 _ = IsTopologicalAddGroup.rightUniformSpace R
have refine : (uniformity R).HasBasis (fun (x : (ValueGroup₀ (F := Valuation R Γ₀) v)ˣ) ↦ True)
  fun (γ : (ValueGroup₀ (F := Valuation R Γ₀) v)ˣ) ↦
  {p : R × R | (Valuation.restrict v : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) (p.2 - p.1) < (↑γ : ValueGroup₀ v)}
Tactic: refine UniformSpace.ext ((hasBasis_uniformity R Γ₀).eq_of_same_basis ?_)
-- Lean 4 proof step from Mathlib.Topology.Algebra.Valued.ValuationTopology (goal)
Goal:
R : Type u
inst : Ring R
Γ₀ : Type v
inst_1 : LinearOrderedCommGroupWithZero Γ₀
_i : Valued R Γ₀
⊢ (uniformity R).HasBasis (fun (x : (ValueGroup₀ (F := Valuation R Γ₀) v)ˣ) ↦ True)
    fun (γ : (ValueGroup₀ (F := Valuation R Γ₀) v)ˣ) ↦
    {p : R × R | (Valuation.restrict v : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) (p.2 - p.1) < (↑γ : ValueGroup₀ v)}
have h : ∀ (x : (ValueGroup₀ (F := Valuation R Γ₀) v)ˣ),
  Eq (α := Set (R × R))
    {p : R × R | (Valuation.restrict v : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) (p.2 - p.1) < (↑x : ValueGroup₀ v)}
    ((fun (p : R × R) ↦ p.2 + -p.1) ⁻¹'
      (↑(ltAddSubgroup v ((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.Valued.ValuationTopology (goal)
Goal:
R : Type u
inst : Ring R
Γ₀ : Type v
inst_1 : LinearOrderedCommGroupWithZero Γ₀
_i : Valued R Γ₀
x : (ValueGroup₀ (F := Valuation R Γ₀) v)ˣ
⊢ Eq (α := Set (R × R))
    {p : R × R | (Valuation.restrict v : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) (p.2 - p.1) < (↑x : ValueGroup₀ v)}
    ((fun (p : R × R) ↦ p.2 + -p.1) ⁻¹'
      (↑(ltAddSubgroup v ((Units.map (↑embedding : ValueGroup₀ v →* Γ₀) : (a : (ValueGroup₀ v)ˣ) → Γ₀ˣ) x)) : Set R))
have h : Eq (α := Set (R × R))
  {p : R × R |
    LT.lt.{v} (α := Γ₀) ((v : (a : R) → Γ₀) (p.2 + -p.1) : Γ₀)
      ((embedding : (a : ValueGroup₀ v) → Γ₀) (↑x : ValueGroup₀ v) : Γ₀)}
  ((fun (p : R × R) ↦ p.2 + -p.1) ⁻¹'
    (↑(ltAddSubgroup v ((Units.map (↑embedding : ValueGroup₀ v →* Γ₀) : (a : (ValueGroup₀ v)ˣ) → Γ₀ˣ) x)) : Set R))
Tactic: simp_rw [restrict_lt_iff_lt_embedding, sub_eq_add_neg]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Valued.ValuationTopology (goal)
Goal:
R : Type u
inst : Ring R
Γ₀ : Type v
inst_1 : LinearOrderedCommGroupWithZero Γ₀
_i : Valued R Γ₀
x : R
h : Ne.{v + 1} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) (0 : Γ₀)
⊢ {y : R | Eq.{v + 1} (α := Γ₀) ((v : (a : R) → Γ₀) y : Γ₀) ((v : (a : R) → Γ₀) x : Γ₀)} ∈ 𝓝 x
have rw : ∃ (γ : (ValueGroup₀ (F := Valuation R Γ₀) v)ˣ),
  Subset.{u} (α := Set R)
    {y : R | (Valuation.restrict v : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) (y - x) < (↑γ : ValueGroup₀ v)}
    {y : R | Eq.{v + 1} (α := Γ₀) ((v : (a : R) → Γ₀) y : Γ₀) ((v : (a : R) → Γ₀) x : Γ₀)}
Tactic: rw [mem_nhds]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Valued.ValuationTopology (hypothesis)
Goal:
R : Type u
inst : Ring R
Γ₀ : Type v
inst_1 : LinearOrderedCommGroupWithZero Γ₀
_i : Valued R Γ₀
x : R
h : Ne.{v + 1} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) (0 : Γ₀)
⊢ ∃ (γ : (ValueGroup₀ (F := Valuation R Γ₀) v)ˣ),
    Subset.{u} (α := Set R)
      {y : R | (Valuation.restrict v : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) (y - x) < (↑γ : ValueGroup₀ v)}
      {y : R | Eq.{v + 1} (α := Γ₀) ((v : (a : R) → Γ₀) y : Γ₀) ((v : (a : R) → Γ₀) x : Γ₀)}
have h' : 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 h' : v.restrict x ≠ 0 := by simp [h]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Valued.ValuationTopology (goal)
Goal:
R : Type u
inst : Ring R
Γ₀ : Type v
inst_1 : LinearOrderedCommGroupWithZero Γ₀
_i : Valued R Γ₀
x : R
h : Ne.{v + 1} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) (0 : Γ₀)
h' :
  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)}
      {y : R | Eq.{v + 1} (α := Γ₀) ((v : (a : R) → Γ₀) y : Γ₀) ((v : (a : R) → Γ₀) x : Γ₀)}
have h₁ : Subset.{u} (α := Set R)
  {y : R |
    LT.lt.{v} (α := ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
      ((Valuation.restrict v : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) (y - x) :
        ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
      ((↑(Units.mk0 ((Valuation.restrict v : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) x) h') :
          ValueGroup₀ (F := Valuation R Γ₀) v) :
        ValueGroup₀ (F := Valuation R Γ₀) v)}
  {y : R | Eq.{v + 1} (α := Γ₀) ((v : (a : R) → Γ₀) y : Γ₀) ((v : (a : R) → Γ₀) x : Γ₀)}
Tactic: use Units.mk0 _ h'
-- Lean 4 proof step from Mathlib.Topology.Algebra.Valued.ValuationTopology (goal)
Goal:
R : Type u
inst : Ring R
Γ₀ : Type v
inst_1 : LinearOrderedCommGroupWithZero Γ₀
_i : Valued R Γ₀
h : ∀ (x : R), x ≠ 0 → Eq.{v + 1} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) (1 : Γ₀)
⊢ DiscreteTopology R
have simp : ∃ (γ : (ValueGroup₀ (F := Valuation R Γ₀) v)ˣ),
  ∀ (y : R), (Valuation.restrict v : (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, mem_nhds_zero, subset_singleton_iff, mem_setOf_eq]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Valued.ValuationTopology (goal)
Goal:
R : Type u
inst : Ring R
Γ₀ : Type v
inst_1 : LinearOrderedCommGroupWithZero Γ₀
_i : Valued R Γ₀
h : ∀ (x : R), x ≠ 0 → Eq.{v + 1} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) (1 : Γ₀)
⊢ ∃ (γ : (ValueGroup₀ (F := Valuation R Γ₀) v)ˣ),
    ∀ (y : R), (Valuation.restrict v : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) y < (↑γ : ValueGroup₀ v) → y = 0
have h₁ : ∀ (y : R),
  LT.lt.{v} (α := ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
      ((Valuation.restrict v : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) y : ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
      ((↑1 : ValueGroup₀ (F := Valuation R Γ₀) v) : ValueGroup₀ (F := Valuation R Γ₀) v) →
    y = 0
Tactic: use 1
-- Lean 4 proof step from Mathlib.Topology.Algebra.Valued.ValuationTopology (goal)
Goal:
R : Type u
inst : Ring R
Γ₀ : Type v
inst_1 : LinearOrderedCommGroupWithZero Γ₀
_i : Valued R Γ₀
h : ∀ (x : R), x ≠ 0 → Eq.{v + 1} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) (1 : Γ₀)
⊢ ∀ (y : R),
    LT.lt.{v} (α := ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
        ((Valuation.restrict v : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) y : ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
        ((↑1 : ValueGroup₀ (F := Valuation R Γ₀) v) : ValueGroup₀ (F := Valuation R Γ₀) v) →
      y = 0
have h₁ : ∀
  (h :
    ∃ (y : R),
      LT.lt.{v} (α := ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
          ((Valuation.restrict v : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) y :
            ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
          ((↑1 : ValueGroup₀ (F := Valuation R Γ₀) v) : ValueGroup₀ (F := Valuation R Γ₀) v) ∧
        y ≠ 0),
  ∃ (x : R), x ≠ 0 ∧ Ne.{v + 1} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) (1 : Γ₀)
Tactic: contrapose! h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Topology.Algebra.Valued.ValuationTopology (goal)
Goal:
R : Type u
inst : Ring R
Γ₀ : Type v
inst_1 : LinearOrderedCommGroupWithZero Γ₀
_i : Valued R Γ₀
h :
  ∃ (y : R),
    LT.lt.{v} (α := ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
        ((Valuation.restrict v : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) y : ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
        ((↑1 : ValueGroup₀ (F := Valuation R Γ₀) v) : ValueGroup₀ (F := Valuation R Γ₀) v) ∧
      y ≠ 0
⊢ ∃ (x : R), x ≠ 0 ∧ Ne.{v + 1} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) (1 : Γ₀)
have h₁ : ∀ (x : R)
  (hx :
    LT.lt.{v} (α := ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
      ((Valuation.restrict v : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) x : ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
      ((↑1 : ValueGroup₀ (F := Valuation R Γ₀) v) : ValueGroup₀ (F := Valuation R Γ₀) v))
  (hx' : x ≠ 0), ∃ (x : R), x ≠ 0 ∧ Ne.{v + 1} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) (1 : Γ₀)
Tactic: obtain ⟨x, hx, hx'⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Topology.Algebra.Valued.ValuationTopology (hypothesis)
Goal:
R : Type u
inst : Ring R
Γ₀ : Type v
inst_1 : LinearOrderedCommGroupWithZero Γ₀
_i : Valued R Γ₀
x : R
hx :
  LT.lt.{v} (α := ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
    ((Valuation.restrict v : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) x : ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
    ((↑1 : ValueGroup₀ (F := Valuation R Γ₀) v) : ValueGroup₀ (F := Valuation R Γ₀) v)
hx' : x ≠ 0
⊢ ∃ (x : R), x ≠ 0 ∧ Ne.{v + 1} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) (1 : Γ₀)
have hx₁ : LT.lt.{v} (α := Γ₀) ((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.Valued.ValuationTopology (goal)
Goal:
R : Type u
inst : Ring R
Γ₀ : Type v
inst_1 : LinearOrderedCommGroupWithZero Γ₀
_i : Valued R Γ₀
F : Filter R
⊢ Cauchy F ↔
    F.NeBot ∧
      ∀ (γ : (ValueGroup₀ (F := Valuation R Γ₀) v)ˣ),
        ∃ M ∈ F,
          ∀ x ∈ M,
            ∀ y ∈ M, (Valuation.restrict v : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) (y - x) < (↑γ : ValueGroup₀ v)
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₀ (F := Valuation R Γ₀) v)ˣ),
      ∃ M ∈ F,
        ∀ x ∈ M, ∀ y ∈ M, (Valuation.restrict v : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) (y - x) < (↑γ : ValueGroup₀ v)
Tactic: rw [toUniformSpace_eq, AddGroupFilterBasis.cauchy_iff]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Valued.ValuationTopology (goal)
Goal:
R : Type u
inst : Ring R
Γ₀ : Type v
inst_1 : LinearOrderedCommGroupWithZero Γ₀
_i : Valued R Γ₀
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₀ (F := Valuation R Γ₀) v)ˣ),
        ∃ M ∈ F,
          ∀ x ∈ M,
            ∀ y ∈ M, (Valuation.restrict v : (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₀ (F := Valuation R Γ₀) v)ˣ),
    ∃ M ∈ F,
      ∀ x ∈ M, ∀ y ∈ M, (Valuation.restrict v : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) (y - x) < (↑γ : ValueGroup₀ v)
Tactic: apply and_congr Iff.rfl
-- Lean 4 proof step from Mathlib.Topology.Algebra.Valued.ValuationTopology (goal)
Goal:
R : Type u
inst : Ring R
Γ₀ : Type v
inst_1 : LinearOrderedCommGroupWithZero Γ₀
_i : Valued R Γ₀
F : Filter R
⊢ (∀ (U : Set R),
      (∃ (i : (ValueGroup₀ (F := Valuation R Γ₀) v)ˣ),
          U =
            (↑(ltAddSubgroup v ((Units.map (↑embedding : ValueGroup₀ v →* Γ₀) : (a : (ValueGroup₀ v)ˣ) → Γ₀ˣ) i)) :
              Set R)) →
        ∃ M ∈ F, ∀ x ∈ M, ∀ y ∈ M, y - x ∈ U) ↔
    ∀ (γ : (ValueGroup₀ (F := Valuation R Γ₀) v)ˣ),
      ∃ M ∈ F,
        ∀ x ∈ M, ∀ y ∈ M, (Valuation.restrict v : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) (y - x) < (↑γ : ValueGroup₀ v)
have mp : (∀ (U : Set R),
    (∃ (i : (ValueGroup₀ (F := Valuation R Γ₀) v)ˣ),
        U =
          (↑(ltAddSubgroup v ((Units.map (↑embedding : ValueGroup₀ v →* Γ₀) : (a : (ValueGroup₀ v)ˣ) → Γ₀ˣ) i)) :
            Set R)) →
      ∃ M ∈ F, ∀ x ∈ M, ∀ y ∈ M, y - x ∈ U) →
  ∀ (γ : (ValueGroup₀ (F := Valuation R Γ₀) v)ˣ),
    ∃ M ∈ F,
      ∀ x ∈ M, ∀ y ∈ M, (Valuation.restrict v : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) (y - x) < (↑γ : ValueGroup₀ v)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Algebra.Valued.ValuationTopology (goal)
Goal:
R : Type u
inst : Ring R
Γ₀ : Type v
inst_1 : LinearOrderedCommGroupWithZero Γ₀
_i : Valued R Γ₀
F : Filter R
mp :
  (∀ (U : Set R),
      (∃ (i : (ValueGroup₀ (F := Valuation R Γ₀) v)ˣ),
          U =
            (↑(ltAddSubgroup v ((Units.map (↑embedding : ValueGroup₀ v →* Γ₀) : (a : (ValueGroup₀ v)ˣ) → Γ₀ˣ) i)) :
              Set R)) →
        ∃ M ∈ F, ∀ x ∈ M, ∀ y ∈ M, y - x ∈ U) →
    ∀ (γ : (ValueGroup₀ (F := Valuation R Γ₀) v)ˣ),
      ∃ M ∈ F,
        ∀ x ∈ M, ∀ y ∈ M, (Valuation.restrict v : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) (y - x) < (↑γ : ValueGroup₀ v)
⊢ (∀ (U : Set R),
      (∃ (i : (ValueGroup₀ (F := Valuation R Γ₀) v)ˣ),
          U =
            (↑(ltAddSubgroup v ((Units.map (↑embedding : ValueGroup₀ v →* Γ₀) : (a : (ValueGroup₀ v)ˣ) → Γ₀ˣ) i)) :
              Set R)) →
        ∃ M ∈ F, ∀ x ∈ M, ∀ y ∈ M, y - x ∈ U) ↔
    ∀ (γ : (ValueGroup₀ (F := Valuation R Γ₀) v)ˣ),
      ∃ M ∈ F,
        ∀ x ∈ M, ∀ y ∈ M, (Valuation.restrict v : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) (y - x) < (↑γ : ValueGroup₀ v)
have mpr : (∀ (γ : (ValueGroup₀ (F := Valuation R Γ₀) v)ˣ),
    ∃ M ∈ F,
      ∀ x ∈ M, ∀ y ∈ M, (Valuation.restrict v : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) (y - x) < (↑γ : ValueGroup₀ v)) →
  ∀ (U : Set R),
    (∃ (i : (ValueGroup₀ (F := Valuation R Γ₀) v)ˣ),
        U =
          (↑(ltAddSubgroup v ((Units.map (↑embedding : ValueGroup₀ v →* Γ₀) : (a : (ValueGroup₀ v)ˣ) → Γ₀ˣ) i)) :
            Set R)) →
      ∃ M ∈ F, ∀ x ∈ M, ∀ y ∈ M, y - x ∈ U
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Algebra.Valued.ValuationTopology (goal)
Goal:
R : Type u
inst : Ring R
Γ₀ : Type v
inst_1 : LinearOrderedCommGroupWithZero Γ₀
_i : Valued R Γ₀
F : Filter R
h :
  ∀ (U : Set R),
    (∃ (i : (ValueGroup₀ (F := Valuation R Γ₀) v)ˣ),
        U =
          (↑(ltAddSubgroup v ((Units.map (↑embedding : ValueGroup₀ v →* Γ₀) : (a : (ValueGroup₀ v)ˣ) → Γ₀ˣ) i)) :
            Set R)) →
      ∃ M ∈ F, ∀ x ∈ M, ∀ y ∈ M, y - x ∈ U
γ : (ValueGroup₀ (F := Valuation R Γ₀) v)ˣ
⊢ ∃ M ∈ F,
    ∀ x ∈ M, ∀ y ∈ M, (Valuation.restrict v : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) (y - x) < (↑γ : ValueGroup₀ v)
have mp : ∃ M ∈ F,
  ∀ x ∈ M,
    ∀ y ∈ M,
      LT.lt.{v} (α := Γ₀) ((v : (a : R) → Γ₀) (y - x) : Γ₀)
        ((embedding : (a : ValueGroup₀ v) → Γ₀) (↑γ : ValueGroup₀ v) : Γ₀)
Tactic: simp_rw [restrict_lt_iff_lt_embedding]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Valued.ValuationTopology (hypothesis)
Goal:
R : Type u
inst : Ring R
Γ₀ : Type v
inst_1 : LinearOrderedCommGroupWithZero Γ₀
_i : Valued R Γ₀
F : Filter R
h :
  ∀ (γ : (ValueGroup₀ (F := Valuation R Γ₀) v)ˣ),
    ∃ M ∈ F,
      ∀ x ∈ M, ∀ y ∈ M, (Valuation.restrict v : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) (y - x) < (↑γ : ValueGroup₀ v)
γ : (ValueGroup₀ (F := Valuation R Γ₀) v)ˣ
⊢ ∃ M ∈ F,
    ∀ x ∈ M,
      ∀ y ∈ M,
        y - x ∈
          (↑(ltAddSubgroup v ((Units.map (↑embedding : ValueGroup₀ v →* Γ₀) : (a : (ValueGroup₀ v)ˣ) → Γ₀ˣ) γ)) : Set R)
have h₁ : ∀ (γ : (ValueGroup₀ (F := Valuation R Γ₀) v)ˣ),
  ∃ M ∈ F,
    ∀ x ∈ M,
      ∀ y ∈ M,
        LT.lt.{v} (α := Γ₀) ((v : (a : R) → Γ₀) (y - x) : Γ₀)
          ((embedding : (a : ValueGroup₀ v) → Γ₀) (↑γ : ValueGroup₀ v) : Γ₀)
Tactic: simp_rw [restrict_lt_iff_lt_embedding] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Topology.Algebra.Valued.ValuationTopology (goal)
Goal:
R : Type u
inst : Ring R
Γ₀ : Type v
inst_1 : LinearOrderedCommGroupWithZero Γ₀
_i : Valued R Γ₀
r : ValueGroup₀ (F := Valuation R Γ₀) v
⊢ IsOpen[_i.toTopologicalSpace] {x : R | (Valuation.restrict v : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) x < r}
have rw : ∀ (x : R),
  Membership.mem (γ := Set R) {x : R | (Valuation.restrict v : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) x < r} x →
    {x : R | (Valuation.restrict v : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) x < r} ∈ 𝓝 x
Tactic: rw [isOpen_iff_mem_nhds]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Valued.ValuationTopology (goal)
Goal:
R : Type u
inst : Ring R
Γ₀ : Type v
inst_1 : LinearOrderedCommGroupWithZero Γ₀
_i : Valued R Γ₀
r : ValueGroup₀ (F := Valuation R Γ₀) v
⊢ ∀ (x : R),
    Membership.mem (γ := Set R) {x : R | (Valuation.restrict v : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) x < r} x →
      {x : R | (Valuation.restrict v : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) x < r} ∈ 𝓝 x
have inl : ∀ (x : R),
  Membership.mem (γ := Set R)
      {x : R |
        LT.lt.{v} (α := ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
          ((Valuation.restrict v : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) x :
            ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
          (0 : ValueGroup₀ (F := Valuation R Γ₀) v)}
      x →
    {x : R |
        LT.lt.{v} (α := ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
          ((Valuation.restrict v : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) x :
            ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
          (0 : ValueGroup₀ (F := Valuation R Γ₀) v)} ∈
      𝓝 x
Tactic: rcases eq_or_ne r 0 with rfl | hr
Cleared hypotheses: r