awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Algebra.UniformRing (goal)
Goal:
α : Type u_1
inst : UniformSpace α
inst_1 : Semiring α
β : Type u_2
inst_2 : UniformSpace β
inst_3 : Semiring β
inst_4 : IsTopologicalSemiring β
γ : Type u_3
inst_5 : UniformSpace γ
inst_6 : Semiring γ
inst_7 : IsTopologicalSemiring γ
inst_8 : T2Space γ
inst_9 : CompleteSpace γ
i : α →+* β
f : α →+* γ
ue : IsUniformInducing.{u_1, u_2} (α := α) (β := β) (⇑i : (a : α) → β)
dr : DenseRange.{u_2, u_1} (X := β) (α := α) (⇑i : (a : α) → β)
hf : UniformContinuous.{u_1, u_3} (α := α) (β := γ) (⇑f : (a : α) → γ)
h : Continuous.{u_2, u_3} (Y := γ) (⋯.extend (⇑f : (a : α) → γ))
x y : β
a b : α
refine_2 :
  ⋯.extend (⇑f : (a : α) → γ) ((i : (a : α) → β) (a + b)) =
    HAdd.hAdd (α := γ) (⋯.extend (⇑f : (a : α) → γ) ((i : (a : α) → β) a))
      (⋯.extend (⇑f : (a : α) → γ) ((i : (a : α) → β) b))
⊢ ⋯.extend (⇑f : (a : α) → γ) (HAdd.hAdd (α := β) (β := β) ((i : (a : α) → β) a : β) ((i : (a : α) → β) b : β)) =
    HAdd.hAdd (α := γ) (⋯.extend (⇑f : (a : α) → γ) ((i : (a : α) → β) a))
      (⋯.extend (⇑f : (a : α) → γ) ((i : (a : α) → β) b))
have refine_2₁ : (f : (a : α) → γ) (a + b) = HAdd.hAdd (α := γ) (β := γ) ((f : (a : α) → γ) a : γ) ((f : (a : α) → γ) b : γ)
Tactic: simp_rw [← i.map_add, IsDenseInducing.extend_eq (ue.isDenseInducing dr) hf.continuous _,
        ← f.map_add]
-- 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_2
inst_2 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
inst_3 : v.Compatible
x : R
s : Set R
⊢ (∃ (γ : (ValueGroup₀ v)ˣ),
      {z : R | (v.restrict : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) (z - x) < (↑γ : ValueGroup₀ v)} ⊆ s) ↔
    ∃ (γ : (ValueGroupWithZero R)ˣ),
      {a : R | (valuation R : (a : R) → ValueGroupWithZero R) (a - x) < (↑γ : ValueGroupWithZero R)} ⊆ s
have refine_1 : (∃ (γ : (ValueGroup₀ v)ˣ),
    {z : R | (v.restrict : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) (z - x) < (↑γ : ValueGroup₀ v)} ⊆ s) →
  ∀ (r : (ValueGroup₀ v)ˣ)
    (hr : {z : R | (v.restrict : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) (z - x) < (↑r : ValueGroup₀ v)} ⊆ s),
    {a : R |
        LT.lt (α := ValueGroupWithZero R)
          ((valuation R : (a : R) → ValueGroupWithZero R) (a - x) : ValueGroupWithZero R)
          ((↑(((Units.mapEquiv (↑(OrderMonoidIso.symm (orderMonoidIso v)) : ValueGroup₀ v ≃* ValueGroupWithZero R) :
                      MulEquiv.{u_2, u_1} (ValueGroup₀ v)ˣ (ValueGroupWithZero R)ˣ) :
                    (a : (ValueGroup₀ v)ˣ) → (ValueGroupWithZero R)ˣ)
                  r) :
              ValueGroupWithZero R) :
            ValueGroupWithZero R)} ⊆
      s
Tactic: refine ⟨fun ⟨r, hr⟩ ↦ ⟨r.mapEquiv (orderMonoidIso v).symm, ?_⟩,
    fun ⟨r, hr⟩ ↦ ⟨r.mapEquiv (orderMonoidIso v), ?_⟩⟩
-- 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_2
inst_2 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
inst_3 : v.Compatible
x : R
s : Set R
refine_1 :
  (∃ (γ : (ValueGroup₀ v)ˣ),
      {z : R | (v.restrict : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) (z - x) < (↑γ : ValueGroup₀ v)} ⊆ s) →
    ∀ (r : (ValueGroup₀ v)ˣ)
      (hr : {z : R | (v.restrict : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) (z - x) < (↑r : ValueGroup₀ v)} ⊆ s),
      {a : R |
          LT.lt (α := ValueGroupWithZero R)
            ((valuation R : (a : R) → ValueGroupWithZero R) (a - x) : ValueGroupWithZero R)
            ((↑(((Units.mapEquiv (↑(OrderMonoidIso.symm (orderMonoidIso v)) : ValueGroup₀ v ≃* ValueGroupWithZero R) :
                        MulEquiv.{u_2, u_1} (ValueGroup₀ v)ˣ (ValueGroupWithZero R)ˣ) :
                      (a : (ValueGroup₀ v)ˣ) → (ValueGroupWithZero R)ˣ)
                    r) :
                ValueGroupWithZero R) :
              ValueGroupWithZero R)} ⊆
        s
⊢ (∃ (γ : (ValueGroup₀ v)ˣ),
      {z : R | (v.restrict : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) (z - x) < (↑γ : ValueGroup₀ v)} ⊆ s) ↔
    ∃ (γ : (ValueGroupWithZero R)ˣ),
      {a : R | (valuation R : (a : R) → ValueGroupWithZero R) (a - x) < (↑γ : ValueGroupWithZero R)} ⊆ s
have refine_2 : (∃ (γ : (ValueGroupWithZero R)ˣ),
    {a : R | (valuation R : (a : R) → ValueGroupWithZero R) (a - x) < (↑γ : ValueGroupWithZero R)} ⊆ s) →
  ∀ (r : (ValueGroupWithZero R)ˣ)
    (hr : {a : R | (valuation R : (a : R) → ValueGroupWithZero R) (a - x) < (↑r : ValueGroupWithZero R)} ⊆ s),
    {z : R |
        LT.lt.{u_2} (α := ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
          ((v.restrict : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) (z - x) : ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
          ((↑(((Units.mapEquiv (↑(orderMonoidIso v) : ValueGroupWithZero R ≃* ValueGroup₀ v) :
                      MulEquiv.{u_1, u_2} (ValueGroupWithZero R)ˣ (ValueGroup₀ v)ˣ) :
                    (a : (ValueGroupWithZero R)ˣ) → (ValueGroup₀ v)ˣ)
                  r) :
              ValueGroup₀ v) :
            ValueGroup₀ v)} ⊆
      s
Tactic: refine ⟨fun ⟨r, hr⟩ ↦ ⟨r.mapEquiv (orderMonoidIso v).symm, ?_⟩,
    fun ⟨r, hr⟩ ↦ ⟨r.mapEquiv (orderMonoidIso v), ?_⟩⟩
-- 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_2
inst_2 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
inst_3 : v.Compatible
x : R
s : Set R
h :
  ∃ (γ : (ValueGroup₀ v)ˣ),
    {z : R | (v.restrict : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) (z - x) < (↑γ : ValueGroup₀ v)} ⊆ s
r : (ValueGroup₀ v)ˣ
hr : {z : R | (v.restrict : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) (z - x) < (↑r : ValueGroup₀ v)} ⊆ s
⊢ {a : R |
      LT.lt (α := ValueGroupWithZero R) ((valuation R : (a : R) → ValueGroupWithZero R) (a - x) : ValueGroupWithZero R)
        ((↑(((Units.mapEquiv (↑(OrderMonoidIso.symm (orderMonoidIso v)) : ValueGroup₀ v ≃* ValueGroupWithZero R) :
                    MulEquiv.{u_2, u_1} (ValueGroup₀ v)ˣ (ValueGroupWithZero R)ˣ) :
                  (a : (ValueGroup₀ v)ˣ) → (ValueGroupWithZero R)ˣ)
                r) :
            ValueGroupWithZero R) :
          ValueGroupWithZero R)} ⊆
    s
have h : ∀ (x_1 : R),
  LT.lt (α := ValueGroupWithZero R) ((valuation R : (a : R) → ValueGroupWithZero R) (x_1 - x) : ValueGroupWithZero R)
      ((↑(((Units.mapEquiv (↑(OrderMonoidIso.symm (orderMonoidIso v)) : ValueGroup₀ v ≃* ValueGroupWithZero R) :
                  MulEquiv.{u_2, u_1} (ValueGroup₀ v)ˣ (ValueGroupWithZero R)ˣ) :
                (a : (ValueGroup₀ v)ˣ) → (ValueGroupWithZero R)ˣ)
              r) :
          ValueGroupWithZero R) :
        ValueGroupWithZero R) ↔
    (v.restrict : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) (x_1 - x) < (↑r : ValueGroup₀ v)
Tactic: convert! 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_2
inst_2 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
inst_3 : v.Compatible
x : R
s : Set R
h :
  ∃ (γ : (ValueGroupWithZero R)ˣ),
    {a : R | (valuation R : (a : R) → ValueGroupWithZero R) (a - x) < (↑γ : ValueGroupWithZero R)} ⊆ s
r : (ValueGroupWithZero R)ˣ
hr : {a : R | (valuation R : (a : R) → ValueGroupWithZero R) (a - x) < (↑r : ValueGroupWithZero R)} ⊆ s
⊢ {z : R |
      LT.lt.{u_2} (α := ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
        ((v.restrict : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) (z - x) : ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
        ((↑(((Units.mapEquiv (↑(orderMonoidIso v) : ValueGroupWithZero R ≃* ValueGroup₀ v) :
                    MulEquiv.{u_1, u_2} (ValueGroupWithZero R)ˣ (ValueGroup₀ v)ˣ) :
                  (a : (ValueGroupWithZero R)ˣ) → (ValueGroup₀ v)ˣ)
                r) :
            ValueGroup₀ v) :
          ValueGroup₀ v)} ⊆
    s
have h : ∀ (x_1 : R),
  LT.lt.{u_2} (α := ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
      ((v.restrict : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) (x_1 - x) : ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
      ((↑(((Units.mapEquiv (↑(orderMonoidIso v) : ValueGroupWithZero R ≃* ValueGroup₀ v) :
                  MulEquiv.{u_1, u_2} (ValueGroupWithZero R)ˣ (ValueGroup₀ v)ˣ) :
                (a : (ValueGroupWithZero R)ˣ) → (ValueGroup₀ v)ˣ)
              r) :
          ValueGroup₀ v) :
        ValueGroup₀ v) ↔
    (valuation R : (a : R) → ValueGroupWithZero R) (x_1 - x) < (↑r : ValueGroupWithZero R)
Tactic: convert! hr
-- Lean 4 proof step from Mathlib.Topology.Algebra.ValuativeRel.ValuativeTopology (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
s : Set R
x : R
⊢ s ∈ 𝓝 x ↔
    ∃ (γ : (ValueGroupWithZero R)ˣ),
      (fun (x_1 : R) ↦ x + x_1) ''
          {z : R | (valuation R : (a : R) → ValueGroupWithZero R) z < (↑γ : ValueGroupWithZero R)} ⊆
        s
have rw : (∃ (i : (ValueGroup₀ (F := Valuation R (ValueGroupWithZero R)) (valuation R))ˣ),
    True ∧
      {b : R |
          Membership.mem (γ := AddSubgroup R)
            (ltAddSubgroup (Γ₀ := ValueGroupWithZero R) (valuation R)
              ((Units.map (↑embedding : ValueGroup₀ (valuation R) →* ValueGroupWithZero R) :
                  (a : (ValueGroup₀ (valuation R))ˣ) → (ValueGroupWithZero R)ˣ)
                i))
            (b - x)} ⊆
        s) ↔
  ∃ (γ : (ValueGroupWithZero R)ˣ),
    (fun (x_1 : R) ↦ x + x_1) ''
        {z : R | (valuation R : (a : R) → ValueGroupWithZero R) z < (↑γ : ValueGroupWithZero R)} ⊆
      s
Tactic: rw [Filter.hasBasis_iff.mp ((valuation R).subgroups_basis.hasBasis_nhds x) s]
-- Lean 4 proof step from Mathlib.Topology.Algebra.ValuativeRel.ValuativeTopology (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
inst_2 : TopologicalSpace R
inst_3 : IsValuativeTopology R
s : Set R
x : R
⊢ s ∈ 𝓝 x ↔
    ∃ (γ : (ValueGroupWithZero R)ˣ),
      {z : R | (valuation R : (a : R) → ValueGroupWithZero R) (z - x) < (↑γ : ValueGroupWithZero R)} ⊆ s
have h : ∀ (x_1 : (ValueGroupWithZero R)ˣ),
  Eq.{u_1 + 1} (α := Set R)
    {z : R | (valuation R : (a : R) → ValueGroupWithZero R) (z - x) < (↑x_1 : ValueGroupWithZero R)}
    ((fun (x_2 : R) ↦ x + x_2) ''
      {z : R | (valuation R : (a : R) → ValueGroupWithZero R) z < (↑x_1 : ValueGroupWithZero R)})
Tactic: convert! mem_nhds_iff (s := s) using 4
-- Lean 4 proof step from Mathlib.Topology.Algebra.ValuativeRel.ValuativeTopology (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
inst_2 : TopologicalSpace R
inst_3 : IsValuativeTopology R
⊢ HasBasis (α := R) (𝓝 0) (fun (x : (ValueGroupWithZero R)ˣ) ↦ True) fun (γ : (ValueGroupWithZero R)ˣ) ↦
    {x : R | (valuation R : (a : R) → ValueGroupWithZero R) x < (↑γ : ValueGroupWithZero R)}
have h : ∀ (x : (ValueGroupWithZero R)ˣ) (x : R), x = x - 0
Tactic: convert! hasBasis_nhds (0 : R)
-- Lean 4 proof step from Mathlib.Topology.Algebra.ValuativeRel.ValuativeTopology (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
inst_2 : TopologicalSpace R
inst_3 : IsValuativeTopology R
x : (ValueGroupWithZero R)ˣ
x_1 : R
⊢ x_1 = x_1 - 0
have h : x_1 = x_1
Tactic: rw [sub_zero]
-- 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 Γ₀
inst_3 : TopologicalSpace R
inst_4 : IsValuativeTopology R
v : Valuation R Γ₀
inst_5 : v.Compatible
s : Set R
x : R
⊢ s ∈ 𝓝 x ↔
    ∃ (γ : (ValueGroup₀ v)ˣ),
      {z : R | (v.restrict : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) (z - x) < (↑γ : ValueGroup₀ v)} ⊆ s
have h : (∃ (γ : (ValueGroup₀ v)ˣ),
    {z : R | (v.restrict : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) (z - x) < (↑γ : ValueGroup₀ v)} ⊆ s) ↔
  ∃ (γ : (ValueGroupWithZero R)ˣ),
    (fun (x_1 : R) ↦ x + x_1) ''
        {z : R | (valuation R : (a : R) → ValueGroupWithZero R) z < (↑γ : ValueGroupWithZero R)} ⊆
      s
Tactic: convert! IsValuativeTopology.mem_nhds_iff (s := s) using 4
-- 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 Γ₀
inst_3 : TopologicalSpace R
inst_4 : IsValuativeTopology R
v : Valuation R Γ₀
inst_5 : v.Compatible
x : R
h : Ne.{u_3 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) (0 : Γ₀)
⊢ {y : R | Eq.{u_3 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) y : Γ₀) ((v : (a : R) → Γ₀) x : Γ₀)} ∈ 𝓝 x
have rw : ∃ (γ : (ValueGroup₀ v)ˣ),
  Subset.{u_1} (α := Set R)
    {z : R | (v.restrict : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) (z - x) < (↑γ : ValueGroup₀ v)}
    {y : R | Eq.{u_3 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) y : Γ₀) ((v : (a : R) → Γ₀) x : Γ₀)}
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 Γ₀
inst_3 : TopologicalSpace R
inst_4 : IsValuativeTopology R
v : Valuation R Γ₀
inst_5 : v.Compatible
x : R
h : Ne.{u_3 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) (0 : Γ₀)
⊢ ∃ (γ : (ValueGroup₀ v)ˣ),
    Subset.{u_1} (α := Set R)
      {z : R | (v.restrict : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) (z - x) < (↑γ : ValueGroup₀ v)}
      {y : R | Eq.{u_3 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) y : Γ₀) ((v : (a : R) → Γ₀) x : Γ₀)}
have h' : 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 h' : v.restrict x ≠ 0 := by simp [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 Γ₀
inst_3 : TopologicalSpace R
inst_4 : IsValuativeTopology R
v : Valuation R Γ₀
inst_5 : v.Compatible
x : R
h : Ne.{u_3 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) (0 : Γ₀)
h' :
  Ne.{u_3 + 1} (α := ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
    ((v.restrict : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) x : ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
    (0 : ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
⊢ ∃ (γ : (ValueGroup₀ v)ˣ),
    Subset.{u_1} (α := Set R)
      {z : R | (v.restrict : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) (z - x) < (↑γ : ValueGroup₀ v)}
      {y : R | Eq.{u_3 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) y : Γ₀) ((v : (a : R) → Γ₀) x : Γ₀)}
have h₁ : Subset.{u_1} (α := Set R)
  {z : R |
    LT.lt.{u_3} (α := ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
      ((v.restrict : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) (z - x) : ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
      ((↑(Units.mk0 ((v.restrict : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) x) h') : ValueGroup₀ v) : ValueGroup₀ v)}
  {y : R | Eq.{u_3 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) y : Γ₀) ((v : (a : R) → Γ₀) x : Γ₀)}
Tactic: use Units.mk0 _ h'
-- Lean 4 proof step from Mathlib.Topology.Algebra.ValuativeRel.ValuativeTopology (hypothesis)
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 Γ₀
inst_5 : TopologicalSpace R
inst_6 : IsValuativeTopology R
v : Valuation R Γ₀
inst_7 : v.Compatible
⊢ IsTopologicalAddGroup R
have cts_add : ContinuousConstVAdd R R
Tactic: have cts_add : ContinuousConstVAdd R R :=
    ⟨fun x ↦ continuous_iff_continuousAt.2 fun z ↦
      (((valuation R).hasBasis_nhds z).tendsto_iff ((valuation R).hasBasis_nhds (x + z))).2
        fun γ _ ↦ ⟨γ, trivial, fun y hy ↦ by simpa using hy⟩⟩
-- Lean 4 proof step from Mathlib.Topology.Algebra.ValuativeRel.ValuativeTopology (hypothesis)
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 Γ₀
inst_5 : TopologicalSpace R
inst_6 : IsValuativeTopology R
v : Valuation R Γ₀
inst_7 : v.Compatible
cts_add : ContinuousConstVAdd R R
⊢ IsTopologicalAddGroup R
have basis : HasBasis (α := R) (𝓝 0) (fun (x : (ValueGroup₀ (F := Valuation R (ValueGroupWithZero R)) (valuation R))ˣ) ↦ True)
  fun (γ : (ValueGroup₀ (F := Valuation R (ValueGroupWithZero R)) (valuation R))ˣ) ↦
  {x : R |
    (Valuation.restrict (valuation R) : (a : R) → ValueGroup₀ (↑(valuation R) : R →*₀ ValueGroupWithZero R)) x <
      (↑γ : ValueGroup₀ (valuation R))}
Tactic: have basis := (valuation R).hasBasis_nhds_zero
-- 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 Γ₀
inst_5 : TopologicalSpace R
inst_6 : IsValuativeTopology R
v : Valuation R Γ₀
inst_7 : v.Compatible
cts_add : ContinuousConstVAdd R R
basis :
  HasBasis (α := R) (𝓝 0) (fun (x : (ValueGroup₀ (F := Valuation R (ValueGroupWithZero R)) (valuation R))ˣ) ↦ True)
    fun (γ : (ValueGroup₀ (F := Valuation R (ValueGroupWithZero R)) (valuation R))ˣ) ↦
    {x : R |
      (Valuation.restrict (valuation R) : (a : R) → ValueGroup₀ (↑(valuation R) : R →*₀ ValueGroupWithZero R)) x <
        (↑γ : ValueGroup₀ (valuation R))}
⊢ IsTopologicalAddGroup R
have refine_1 : Tendsto (β := R) (Function.uncurry fun (x1 x2 : R) ↦ x1 + x2) (SProd.sprod (α := Filter R) (β := Filter R) (𝓝 0) (𝓝 0))
  (𝓝 0)
Tactic: refine .of_comm_of_nhds_zero ?_ ?_ fun x₀ ↦ (map_eq_of_inverse (-x₀ + ·) ?_ ?_ ?_).symm
-- 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 Γ₀
inst_5 : TopologicalSpace R
inst_6 : IsValuativeTopology R
v : Valuation R Γ₀
inst_7 : v.Compatible
cts_add : ContinuousConstVAdd R R
basis :
  HasBasis (α := R) (𝓝 0) (fun (x : (ValueGroup₀ (F := Valuation R (ValueGroupWithZero R)) (valuation R))ˣ) ↦ True)
    fun (γ : (ValueGroup₀ (F := Valuation R (ValueGroupWithZero R)) (valuation R))ˣ) ↦
    {x : R |
      (Valuation.restrict (valuation R) : (a : R) → ValueGroup₀ (↑(valuation R) : R →*₀ ValueGroupWithZero R)) x <
        (↑γ : ValueGroup₀ (valuation R))}
refine_1 :
  Tendsto (β := R) (Function.uncurry fun (x1 x2 : R) ↦ x1 + x2)
    (SProd.sprod (α := Filter R) (β := Filter R) (𝓝 0) (𝓝 0)) (𝓝 0)
⊢ IsTopologicalAddGroup R
have refine_2 : Tendsto (β := R) (fun (x : R) ↦ -x) (𝓝 0) (𝓝 0)
Tactic: refine .of_comm_of_nhds_zero ?_ ?_ fun x₀ ↦ (map_eq_of_inverse (-x₀ + ·) ?_ ?_ ?_).symm
-- 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 Γ₀
inst_5 : TopologicalSpace R
inst_6 : IsValuativeTopology R
v : Valuation R Γ₀
inst_7 : v.Compatible
cts_add : ContinuousConstVAdd R R
basis :
  HasBasis (α := R) (𝓝 0) (fun (x : (ValueGroup₀ (F := Valuation R (ValueGroupWithZero R)) (valuation R))ˣ) ↦ True)
    fun (γ : (ValueGroup₀ (F := Valuation R (ValueGroupWithZero R)) (valuation R))ˣ) ↦
    {x : R |
      (Valuation.restrict (valuation R) : (a : R) → ValueGroup₀ (↑(valuation R) : R →*₀ ValueGroupWithZero R)) x <
        (↑γ : ValueGroup₀ (valuation R))}
refine_1 :
  Tendsto (β := R) (Function.uncurry fun (x1 x2 : R) ↦ x1 + x2)
    (SProd.sprod (α := Filter R) (β := Filter R) (𝓝 0) (𝓝 0)) (𝓝 0)
refine_2 : Tendsto (β := R) (fun (x : R) ↦ -x) (𝓝 0) (𝓝 0)
⊢ IsTopologicalAddGroup R
have refine_3 : ∀ (x₀ : R), Eq.{u_1 + 1} (α := R → R) ((fun (x : R) ↦ x₀ + x) ∘ fun (x : R) ↦ -x₀ + x) _root_.id
Tactic: refine .of_comm_of_nhds_zero ?_ ?_ fun x₀ ↦ (map_eq_of_inverse (-x₀ + ·) ?_ ?_ ?_).symm
-- 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 Γ₀
inst_5 : TopologicalSpace R
inst_6 : IsValuativeTopology R
v : Valuation R Γ₀
inst_7 : v.Compatible
cts_add : ContinuousConstVAdd R R
basis :
  HasBasis (α := R) (𝓝 0) (fun (x : (ValueGroup₀ (F := Valuation R (ValueGroupWithZero R)) (valuation R))ˣ) ↦ True)
    fun (γ : (ValueGroup₀ (F := Valuation R (ValueGroupWithZero R)) (valuation R))ˣ) ↦
    {x : R |
      (Valuation.restrict (valuation R) : (a : R) → ValueGroup₀ (↑(valuation R) : R →*₀ ValueGroupWithZero R)) x <
        (↑γ : ValueGroup₀ (valuation R))}
refine_1 :
  Tendsto (β := R) (Function.uncurry fun (x1 x2 : R) ↦ x1 + x2)
    (SProd.sprod (α := Filter R) (β := Filter R) (𝓝 0) (𝓝 0)) (𝓝 0)
refine_2 : Tendsto (β := R) (fun (x : R) ↦ -x) (𝓝 0) (𝓝 0)
refine_3 : ∀ (x₀ : R), Eq.{u_1 + 1} (α := R → R) ((fun (x : R) ↦ x₀ + x) ∘ fun (x : R) ↦ -x₀ + x) _root_.id
⊢ IsTopologicalAddGroup R
have refine_4 : ∀ (x₀ : R), Tendsto (fun (x : R) ↦ x₀ + x) (𝓝 0) (𝓝 x₀)
Tactic: refine .of_comm_of_nhds_zero ?_ ?_ fun x₀ ↦ (map_eq_of_inverse (-x₀ + ·) ?_ ?_ ?_).symm
-- 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 Γ₀
inst_5 : TopologicalSpace R
inst_6 : IsValuativeTopology R
v : Valuation R Γ₀
inst_7 : v.Compatible
cts_add : ContinuousConstVAdd R R
basis :
  HasBasis (α := R) (𝓝 0) (fun (x : (ValueGroup₀ (F := Valuation R (ValueGroupWithZero R)) (valuation R))ˣ) ↦ True)
    fun (γ : (ValueGroup₀ (F := Valuation R (ValueGroupWithZero R)) (valuation R))ˣ) ↦
    {x : R |
      (Valuation.restrict (valuation R) : (a : R) → ValueGroup₀ (↑(valuation R) : R →*₀ ValueGroupWithZero R)) x <
        (↑γ : ValueGroup₀ (valuation R))}
refine_1 :
  Tendsto (β := R) (Function.uncurry fun (x1 x2 : R) ↦ x1 + x2)
    (SProd.sprod (α := Filter R) (β := Filter R) (𝓝 0) (𝓝 0)) (𝓝 0)
refine_2 : Tendsto (β := R) (fun (x : R) ↦ -x) (𝓝 0) (𝓝 0)
refine_3 : ∀ (x₀ : R), Eq.{u_1 + 1} (α := R → R) ((fun (x : R) ↦ x₀ + x) ∘ fun (x : R) ↦ -x₀ + x) _root_.id
refine_4 : ∀ (x₀ : R), Tendsto (fun (x : R) ↦ x₀ + x) (𝓝 0) (𝓝 x₀)
⊢ IsTopologicalAddGroup R
have refine_5 : ∀ (x₀ : R), Tendsto (β := R) (fun (x : R) ↦ -x₀ + x) (𝓝 x₀) (𝓝 0)
Tactic: refine .of_comm_of_nhds_zero ?_ ?_ fun x₀ ↦ (map_eq_of_inverse (-x₀ + ·) ?_ ?_ ?_).symm
-- 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 Γ₀
inst_5 : TopologicalSpace R
inst_6 : IsValuativeTopology R
v : Valuation R Γ₀
inst_7 : v.Compatible
cts_add : ContinuousConstVAdd R R
basis :
  HasBasis (α := R) (𝓝 0) (fun (x : (ValueGroup₀ (F := Valuation R (ValueGroupWithZero R)) (valuation R))ˣ) ↦ True)
    fun (γ : (ValueGroup₀ (F := Valuation R (ValueGroupWithZero R)) (valuation R))ˣ) ↦
    {x : R |
      (Valuation.restrict (valuation R) : (a : R) → ValueGroup₀ (↑(valuation R) : R →*₀ ValueGroupWithZero R)) x <
        (↑γ : ValueGroup₀ (valuation R))}
x₀ : R
⊢ Eq.{u_1 + 1} (α := R → R) ((fun (x : R) ↦ x₀ + x) ∘ fun (x : R) ↦ -x₀ + x) _root_.id
have refine_3 : ∀ (x : R), ((fun (x : R) ↦ x₀ + x) ∘ fun (x : R) ↦ -x₀ + x) x = _root_.id x
Tactic: ext
-- 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 rw : HasBasis.{u_1, u_3 + 1} (α := R × R) (Filter.comap (β := R) (fun (x : R × R) ↦ x.2 - x.1) (𝓝 0))
  (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: rw [uniformity_eq_comap_nhds_zero]