awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Algebra.Valued.ValuedField (goal)
Goal:
K : Type u_1
inst : Field K
Γ₀ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
s : Set (hat K)
this :
  HasBasis.{u_1, u_2 + 1} (α := hat K) (𝓝 0) (fun (x : (ValueGroup₀ (F := Valuation K Γ₀) v)ˣ) ↦ True)
    fun (γ : (ValueGroup₀ (F := Valuation K Γ₀) v)ˣ) ↦
    {x : hat K |
      LT.lt.{u_2} (α := Γ₀) ((extensionValuation : (a : hat K) → Γ₀) x : Γ₀)
        ((↑((Units.map (↑embedding : ValueGroup₀ v →* Γ₀) : (a : (ValueGroup₀ v)ˣ) → Γ₀ˣ) γ) : Γ₀) : Γ₀)}
x : hat K
γ : (ValueGroup₀ (F := Valuation K Γ₀) v)ˣ
hx0 : ¬x = 0
y : K :=
  Exists.choose (p := fun (a : K) ↦
    ((restrict₀ v : MonoidWithZeroHom.{u_1, u_2} K (ValueGroup₀ (F := Valuation K Γ₀) v)) : (a : K) → ValueGroup₀ v) a =
      (↑γ : ValueGroup₀ v))
    ⋯
hy_def :
  y =
    Exists.choose (p := fun (a : K) ↦
      ((restrict₀ v : MonoidWithZeroHom.{u_1, u_2} K (ValueGroup₀ (F := Valuation K Γ₀) v)) : (a : K) → ValueGroup₀ v)
          a =
        (↑γ : ValueGroup₀ v))
      ⋯
hy : ((restrict₀ v : MonoidWithZeroHom.{u_1, u_2} K (ValueGroup₀ (F := Valuation K Γ₀) v)) : (a : K) → ValueGroup₀ v)
    (Exists.choose (p := fun (a : K) ↦
      ((restrict₀ v : MonoidWithZeroHom.{u_1, u_2} K (ValueGroup₀ (F := Valuation K Γ₀) v)) : (a : K) → ValueGroup₀ v)
          a =
        (↑γ : ValueGroup₀ v))
      ⋯) =
  (↑γ : ValueGroup₀ v) :=
  ⋯
neg :
  extension x < (Valuation.restrict v : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀)) y ↔ extension x < (↑γ : ValueGroup₀ v)
⊢ LT.lt (α := Γ₀) ((embedding : (a : ValueGroup₀ v) → Γ₀) (extension x) : Γ₀)
      ((embedding : (a : ValueGroup₀ v) → Γ₀)
          ((Valuation.restrict v : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀)) y :
            ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀)) :
        Γ₀) ↔
    extension x < (↑γ : ValueGroup₀ v)
have neg₁ : extension x <
    ((restrict₀ v : MonoidWithZeroHom.{u_1, u_2} K (ValueGroup₀ (F := Valuation K Γ₀) v)) : (a : K) → ValueGroup₀ v) y ↔
  extension x < (↑γ : ValueGroup₀ v)
Tactic: rw [embedding_strictMono.lt_iff_lt, v.restrict_def, hy]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Valued.ValuedField (goal)
Goal:
K : Type u_1
inst : Field K
Γ₀ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
s : Set (hat K)
this :
  HasBasis.{u_1, u_2 + 1} (α := hat K) (𝓝 0) (fun (x : (ValueGroup₀ (F := Valuation K Γ₀) v)ˣ) ↦ True)
    fun (γ : (ValueGroup₀ (F := Valuation K Γ₀) v)ˣ) ↦
    {x : hat K |
      LT.lt.{u_2} (α := Γ₀) ((extensionValuation : (a : hat K) → Γ₀) x : Γ₀)
        ((↑((Units.map (↑embedding : ValueGroup₀ v →* Γ₀) : (a : (ValueGroup₀ v)ˣ) → Γ₀ˣ) γ) : Γ₀) : Γ₀)}
x : hat K
γ : (ValueGroup₀ (F := Valuation K Γ₀) v)ˣ
hx0 : ¬x = 0
y : K :=
  Exists.choose (p := fun (a : K) ↦
    ((restrict₀ v : MonoidWithZeroHom.{u_1, u_2} K (ValueGroup₀ (F := Valuation K Γ₀) v)) : (a : K) → ValueGroup₀ v) a =
      (↑γ : ValueGroup₀ v))
    ⋯
hy_def :
  y =
    Exists.choose (p := fun (a : K) ↦
      ((restrict₀ v : MonoidWithZeroHom.{u_1, u_2} K (ValueGroup₀ (F := Valuation K Γ₀) v)) : (a : K) → ValueGroup₀ v)
          a =
        (↑γ : ValueGroup₀ v))
      ⋯
hy : ((restrict₀ v : MonoidWithZeroHom.{u_1, u_2} K (ValueGroup₀ (F := Valuation K Γ₀) v)) : (a : K) → ValueGroup₀ v)
    (Exists.choose (p := fun (a : K) ↦
      ((restrict₀ v : MonoidWithZeroHom.{u_1, u_2} K (ValueGroup₀ (F := Valuation K Γ₀) v)) : (a : K) → ValueGroup₀ v)
          a =
        (↑γ : ValueGroup₀ v))
      ⋯) =
  (↑γ : ValueGroup₀ v) :=
  ⋯
neg :
  extension x < (Valuation.restrict v : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀)) y ↔ extension x < (↑γ : ValueGroup₀ v)
neg₁ :
  extension x <
      ((restrict₀ v : MonoidWithZeroHom.{u_1, u_2} K (ValueGroup₀ (F := Valuation K Γ₀) v)) : (a : K) → ValueGroup₀ v)
        y ↔
    extension x < (↑γ : ValueGroup₀ v)
⊢ LT.lt (α := Γ₀) ((embedding : (a : ValueGroup₀ v) → Γ₀) (extension x) : Γ₀)
      ((embedding : (a : ValueGroup₀ v) → Γ₀)
          ((Valuation.restrict v : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀)) y :
            ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀)) :
        Γ₀) ↔
    extension x < (↑γ : ValueGroup₀ v)
have neg₂ : extension x < (↑γ : ValueGroup₀ v) ↔ extension x < (↑γ : ValueGroup₀ v)
Tactic: rw [embedding_strictMono.lt_iff_lt, v.restrict_def, hy]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Valued.ValuedField (goal)
Goal:
K : Type u_1
inst : Field K
Γ₀ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
s : Set (hat K)
this :
  HasBasis.{u_1, u_2 + 1} (α := hat K) (𝓝 0) (fun (x : (ValueGroup₀ (F := Valuation K Γ₀) v)ˣ) ↦ True)
    fun (γ : (ValueGroup₀ (F := Valuation K Γ₀) v)ˣ) ↦
    {x : hat K |
      LT.lt.{u_2} (α := Γ₀) ((extensionValuation : (a : hat K) → Γ₀) x : Γ₀)
        ((↑((Units.map (↑embedding : ValueGroup₀ v →* Γ₀) : (a : (ValueGroup₀ v)ˣ) → Γ₀ˣ) γ) : Γ₀) : Γ₀)}
x : hat K
γ : (ValueGroup₀ (F := Valuation K Γ₀) v)ˣ
hx0 : ¬x = 0
y : K :=
  Exists.choose (p := fun (a : K) ↦
    ((restrict₀ v : MonoidWithZeroHom.{u_1, u_2} K (ValueGroup₀ (F := Valuation K Γ₀) v)) : (a : K) → ValueGroup₀ v) a =
      (↑γ : ValueGroup₀ v))
    ⋯
hy_def :
  y =
    Exists.choose (p := fun (a : K) ↦
      ((restrict₀ v : MonoidWithZeroHom.{u_1, u_2} K (ValueGroup₀ (F := Valuation K Γ₀) v)) : (a : K) → ValueGroup₀ v)
          a =
        (↑γ : ValueGroup₀ v))
      ⋯
hy : ((restrict₀ v : MonoidWithZeroHom.{u_1, u_2} K (ValueGroup₀ (F := Valuation K Γ₀) v)) : (a : K) → ValueGroup₀ v)
    (Exists.choose (p := fun (a : K) ↦
      ((restrict₀ v : MonoidWithZeroHom.{u_1, u_2} K (ValueGroup₀ (F := Valuation K Γ₀) v)) : (a : K) → ValueGroup₀ v)
          a =
        (↑γ : ValueGroup₀ v))
      ⋯) =
  (↑γ : ValueGroup₀ v) :=
  ⋯
⊢ ¬Eq.{u_2 + 1} (α := Γ₀) ((extensionValuation : (a : hat K) → Γ₀) (↑y : hat K) : Γ₀) (0 : Γ₀)
have neg : ¬(↑γ : ValueGroup₀ v) = 0
Tactic: rw [extensionValuation_apply_coe, ← restrict₀_eq_zero_iff, hy]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Valued.ValuedField (goal)
Goal:
K : Type u_1
inst : Field K
Γ₀ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
s : Set (hat K)
this_1 :
  HasBasis.{u_1, u_2 + 1} (α := hat K) (𝓝 0) (fun (x : (ValueGroup₀ (F := Valuation K Γ₀) v)ˣ) ↦ True)
    fun (γ : (ValueGroup₀ (F := Valuation K Γ₀) v)ˣ) ↦
    {x : hat K |
      LT.lt.{u_2} (α := Γ₀) ((extensionValuation : (a : hat K) → Γ₀) x : Γ₀)
        ((↑((Units.map (↑embedding : ValueGroup₀ v →* Γ₀) : (a : (ValueGroup₀ v)ˣ) → Γ₀ˣ) γ) : Γ₀) : Γ₀)}
this :
  ∀ (x : hat K) (γ : (ValueGroup₀ (F := Valuation K Γ₀) v)ˣ),
    LT.lt.{u_2} (α := ValueGroup₀ (F := MonoidWithZeroHom.{u_1, u_2} (hat K) Γ₀) (↑extensionValuation : hat K →*₀ Γ₀))
        ((Valuation.restrict extensionValuation : (a : hat K) → ValueGroup₀ (↑extensionValuation : hat K →*₀ Γ₀)) x :
          ValueGroup₀ (F := MonoidWithZeroHom.{u_1, u_2} (hat K) Γ₀) (↑extensionValuation : hat K →*₀ Γ₀))
        ((↑((Units.map (MulEquiv.toMonoidHom valueGroup₀_equiv_extensionValuation) :
                  (a : (ValueGroup₀ v)ˣ) → (ValueGroup₀ extensionValuation)ˣ)
                γ) :
            ValueGroup₀ (F := Valuation.{u_1, u_2} (hat K) Γ₀) extensionValuation) :
          ValueGroup₀ (F := Valuation.{u_1, u_2} (hat K) Γ₀) extensionValuation) ↔
      LT.lt (α := Γ₀) ((embedding : (a : ValueGroup₀ v) → Γ₀) (extension x) : Γ₀)
        ((embedding : (a : ValueGroup₀ v) → Γ₀) (↑γ : ValueGroup₀ v) : Γ₀)
⊢ (∃ (i : (ValueGroup₀ (F := Valuation K Γ₀) v)ˣ),
      {x : hat K |
          LT.lt (α := Γ₀) ((embedding : (a : ValueGroup₀ v) → Γ₀) (extension x) : Γ₀)
            ((embedding : (a : ValueGroup₀ v) → Γ₀) (↑i : ValueGroup₀ v) : Γ₀)} ⊆
        s) ↔
    ∃ (γ : (ValueGroup₀ (F := Valuation.{u_1, u_2} (hat K) Γ₀) extensionValuation)ˣ),
      {x : hat K |
          (Valuation.restrict extensionValuation : (a : hat K) → ValueGroup₀ (↑extensionValuation : hat K →*₀ Γ₀)) x <
            (↑γ : ValueGroup₀ extensionValuation)} ⊆
        s
have refine_1 : (∃ (i : (ValueGroup₀ (F := Valuation K Γ₀) v)ˣ),
    {x : hat K |
        LT.lt (α := Γ₀) ((embedding : (a : ValueGroup₀ v) → Γ₀) (extension x) : Γ₀)
          ((embedding : (a : ValueGroup₀ v) → Γ₀) (↑i : ValueGroup₀ v) : Γ₀)} ⊆
      s) →
  ∀ (γ : (ValueGroup₀ (F := Valuation K Γ₀) v)ˣ)
    (h :
      {x : hat K |
          LT.lt (α := Γ₀) ((embedding : (a : ValueGroup₀ v) → Γ₀) (extension x) : Γ₀)
            ((embedding : (a : ValueGroup₀ v) → Γ₀) (↑γ : ValueGroup₀ v) : Γ₀)} ⊆
        s),
    ∃ (γ : (ValueGroup₀ (F := Valuation.{u_1, u_2} (hat K) Γ₀) extensionValuation)ˣ),
      {x : hat K |
          (Valuation.restrict extensionValuation : (a : hat K) → ValueGroup₀ (↑extensionValuation : hat K →*₀ Γ₀)) x <
            (↑γ : ValueGroup₀ extensionValuation)} ⊆
        s
Tactic: refine ⟨fun ⟨γ, h⟩ ↦ ?_, fun ⟨γ, h⟩ ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Algebra.Valued.ValuedField (goal)
Goal:
K : Type u_1
inst : Field K
Γ₀ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
s : Set (hat K)
this_1 :
  HasBasis.{u_1, u_2 + 1} (α := hat K) (𝓝 0) (fun (x : (ValueGroup₀ (F := Valuation K Γ₀) v)ˣ) ↦ True)
    fun (γ : (ValueGroup₀ (F := Valuation K Γ₀) v)ˣ) ↦
    {x : hat K |
      LT.lt.{u_2} (α := Γ₀) ((extensionValuation : (a : hat K) → Γ₀) x : Γ₀)
        ((↑((Units.map (↑embedding : ValueGroup₀ v →* Γ₀) : (a : (ValueGroup₀ v)ˣ) → Γ₀ˣ) γ) : Γ₀) : Γ₀)}
this :
  ∀ (x : hat K) (γ : (ValueGroup₀ (F := Valuation K Γ₀) v)ˣ),
    LT.lt.{u_2} (α := ValueGroup₀ (F := MonoidWithZeroHom.{u_1, u_2} (hat K) Γ₀) (↑extensionValuation : hat K →*₀ Γ₀))
        ((Valuation.restrict extensionValuation : (a : hat K) → ValueGroup₀ (↑extensionValuation : hat K →*₀ Γ₀)) x :
          ValueGroup₀ (F := MonoidWithZeroHom.{u_1, u_2} (hat K) Γ₀) (↑extensionValuation : hat K →*₀ Γ₀))
        ((↑((Units.map (MulEquiv.toMonoidHom valueGroup₀_equiv_extensionValuation) :
                  (a : (ValueGroup₀ v)ˣ) → (ValueGroup₀ extensionValuation)ˣ)
                γ) :
            ValueGroup₀ (F := Valuation.{u_1, u_2} (hat K) Γ₀) extensionValuation) :
          ValueGroup₀ (F := Valuation.{u_1, u_2} (hat K) Γ₀) extensionValuation) ↔
      LT.lt (α := Γ₀) ((embedding : (a : ValueGroup₀ v) → Γ₀) (extension x) : Γ₀)
        ((embedding : (a : ValueGroup₀ v) → Γ₀) (↑γ : ValueGroup₀ v) : Γ₀)
h_1 :
  ∃ (i : (ValueGroup₀ (F := Valuation K Γ₀) v)ˣ),
    {x : hat K |
        LT.lt (α := Γ₀) ((embedding : (a : ValueGroup₀ v) → Γ₀) (extension x) : Γ₀)
          ((embedding : (a : ValueGroup₀ v) → Γ₀) (↑i : ValueGroup₀ v) : Γ₀)} ⊆
      s
γ : (ValueGroup₀ (F := Valuation K Γ₀) v)ˣ
h :
  {x : hat K |
      LT.lt (α := Γ₀) ((embedding : (a : ValueGroup₀ v) → Γ₀) (extension x) : Γ₀)
        ((embedding : (a : ValueGroup₀ v) → Γ₀) (↑γ : ValueGroup₀ v) : Γ₀)} ⊆
    s
⊢ ∃ (γ : (ValueGroup₀ (F := Valuation.{u_1, u_2} (hat K) Γ₀) extensionValuation)ˣ),
    {x : hat K |
        (Valuation.restrict extensionValuation : (a : hat K) → ValueGroup₀ (↑extensionValuation : hat K →*₀ Γ₀)) x <
          (↑γ : ValueGroup₀ extensionValuation)} ⊆
      s
have h₁ : {x : hat K |
    LT.lt.{u_2} (α := ValueGroup₀ (F := MonoidWithZeroHom.{u_1, u_2} (hat K) Γ₀) (↑extensionValuation : hat K →*₀ Γ₀))
      ((Valuation.restrict extensionValuation : (a : hat K) → ValueGroup₀ (↑extensionValuation : hat K →*₀ Γ₀)) x :
        ValueGroup₀ (F := MonoidWithZeroHom.{u_1, u_2} (hat K) Γ₀) (↑extensionValuation : hat K →*₀ Γ₀))
      ((↑((Units.map (MulEquiv.toMonoidHom valueGroup₀_equiv_extensionValuation) :
                (a : (ValueGroup₀ v)ˣ) → (ValueGroup₀ extensionValuation)ˣ)
              γ) :
          ValueGroup₀ (F := Valuation.{u_1, u_2} (hat K) Γ₀) extensionValuation) :
        ValueGroup₀ (F := Valuation.{u_1, u_2} (hat K) Γ₀) extensionValuation)} ⊆
  s
Tactic: use Units.map valueGroup₀_equiv_extensionValuation.toMonoidHom γ
-- Lean 4 proof step from Mathlib.Topology.Algebra.Valued.ValuedField (goal)
Goal:
K : Type u_1
inst : Field K
Γ₀ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
s : Set (hat K)
this_1 :
  HasBasis.{u_1, u_2 + 1} (α := hat K) (𝓝 0) (fun (x : (ValueGroup₀ (F := Valuation K Γ₀) v)ˣ) ↦ True)
    fun (γ : (ValueGroup₀ (F := Valuation K Γ₀) v)ˣ) ↦
    {x : hat K |
      LT.lt.{u_2} (α := Γ₀) ((extensionValuation : (a : hat K) → Γ₀) x : Γ₀)
        ((↑((Units.map (↑embedding : ValueGroup₀ v →* Γ₀) : (a : (ValueGroup₀ v)ˣ) → Γ₀ˣ) γ) : Γ₀) : Γ₀)}
this :
  ∀ (x : hat K) (γ : (ValueGroup₀ (F := Valuation K Γ₀) v)ˣ),
    LT.lt.{u_2} (α := ValueGroup₀ (F := MonoidWithZeroHom.{u_1, u_2} (hat K) Γ₀) (↑extensionValuation : hat K →*₀ Γ₀))
        ((Valuation.restrict extensionValuation : (a : hat K) → ValueGroup₀ (↑extensionValuation : hat K →*₀ Γ₀)) x :
          ValueGroup₀ (F := MonoidWithZeroHom.{u_1, u_2} (hat K) Γ₀) (↑extensionValuation : hat K →*₀ Γ₀))
        ((↑((Units.map (MulEquiv.toMonoidHom valueGroup₀_equiv_extensionValuation) :
                  (a : (ValueGroup₀ v)ˣ) → (ValueGroup₀ extensionValuation)ˣ)
                γ) :
            ValueGroup₀ (F := Valuation.{u_1, u_2} (hat K) Γ₀) extensionValuation) :
          ValueGroup₀ (F := Valuation.{u_1, u_2} (hat K) Γ₀) extensionValuation) ↔
      LT.lt (α := Γ₀) ((embedding : (a : ValueGroup₀ v) → Γ₀) (extension x) : Γ₀)
        ((embedding : (a : ValueGroup₀ v) → Γ₀) (↑γ : ValueGroup₀ v) : Γ₀)
h_1 :
  ∃ (γ : (ValueGroup₀ (F := Valuation.{u_1, u_2} (hat K) Γ₀) extensionValuation)ˣ),
    {x : hat K |
        (Valuation.restrict extensionValuation : (a : hat K) → ValueGroup₀ (↑extensionValuation : hat K →*₀ Γ₀)) x <
          (↑γ : ValueGroup₀ extensionValuation)} ⊆
      s
γ : (ValueGroup₀ (F := Valuation.{u_1, u_2} (hat K) Γ₀) extensionValuation)ˣ
h :
  {x : hat K |
      (Valuation.restrict extensionValuation : (a : hat K) → ValueGroup₀ (↑extensionValuation : hat K →*₀ Γ₀)) x <
        (↑γ : ValueGroup₀ extensionValuation)} ⊆
    s
⊢ ∃ (i : (ValueGroup₀ (F := Valuation K Γ₀) v)ˣ),
    {x : hat K |
        LT.lt (α := Γ₀) ((embedding : (a : ValueGroup₀ v) → Γ₀) (extension x) : Γ₀)
          ((embedding : (a : ValueGroup₀ v) → Γ₀) (↑i : ValueGroup₀ v) : Γ₀)} ⊆
      s
have h₁ : {x : hat K |
    LT.lt (α := Γ₀) ((embedding : (a : ValueGroup₀ v) → Γ₀) (extension x) : Γ₀)
      ((embedding : (a : ValueGroup₀ v) → Γ₀)
          (↑((Units.map (MulEquiv.toMonoidHom (MulEquiv.symm valueGroup₀_equiv_extensionValuation)) :
                  (a : (ValueGroup₀ extensionValuation)ˣ) → (ValueGroup₀ v)ˣ)
                γ) :
            ValueGroup₀ v) :
        Γ₀)} ⊆
  s
Tactic: use Units.map valueGroup₀_equiv_extensionValuation.symm.toMonoidHom γ
-- Lean 4 proof step from Mathlib.Topology.Algebra.Valued.ValuedField (goal)
Goal:
K : Type u_1
inst : Field K
Γ₀ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
s : Set (hat K)
this_1 :
  HasBasis.{u_1, u_2 + 1} (α := hat K) (𝓝 0) (fun (x : (ValueGroup₀ (F := Valuation K Γ₀) v)ˣ) ↦ True)
    fun (γ : (ValueGroup₀ (F := Valuation K Γ₀) v)ˣ) ↦
    {x : hat K |
      LT.lt.{u_2} (α := Γ₀) ((extensionValuation : (a : hat K) → Γ₀) x : Γ₀)
        ((↑((Units.map (↑embedding : ValueGroup₀ v →* Γ₀) : (a : (ValueGroup₀ v)ˣ) → Γ₀ˣ) γ) : Γ₀) : Γ₀)}
this :
  ∀ (x : hat K) (γ : (ValueGroup₀ (F := Valuation K Γ₀) v)ˣ),
    LT.lt.{u_2} (α := ValueGroup₀ (F := MonoidWithZeroHom.{u_1, u_2} (hat K) Γ₀) (↑extensionValuation : hat K →*₀ Γ₀))
        ((Valuation.restrict extensionValuation : (a : hat K) → ValueGroup₀ (↑extensionValuation : hat K →*₀ Γ₀)) x :
          ValueGroup₀ (F := MonoidWithZeroHom.{u_1, u_2} (hat K) Γ₀) (↑extensionValuation : hat K →*₀ Γ₀))
        ((↑((Units.map (MulEquiv.toMonoidHom valueGroup₀_equiv_extensionValuation) :
                  (a : (ValueGroup₀ v)ˣ) → (ValueGroup₀ extensionValuation)ˣ)
                γ) :
            ValueGroup₀ (F := Valuation.{u_1, u_2} (hat K) Γ₀) extensionValuation) :
          ValueGroup₀ (F := Valuation.{u_1, u_2} (hat K) Γ₀) extensionValuation) ↔
      LT.lt (α := Γ₀) ((embedding : (a : ValueGroup₀ v) → Γ₀) (extension x) : Γ₀)
        ((embedding : (a : ValueGroup₀ v) → Γ₀) (↑γ : ValueGroup₀ v) : Γ₀)
h_1 :
  ∃ (γ : (ValueGroup₀ (F := Valuation.{u_1, u_2} (hat K) Γ₀) extensionValuation)ˣ),
    {x : hat K |
        (Valuation.restrict extensionValuation : (a : hat K) → ValueGroup₀ (↑extensionValuation : hat K →*₀ Γ₀)) x <
          (↑γ : ValueGroup₀ extensionValuation)} ⊆
      s
γ : (ValueGroup₀ (F := Valuation.{u_1, u_2} (hat K) Γ₀) extensionValuation)ˣ
h :
  {x : hat K |
      (Valuation.restrict extensionValuation : (a : hat K) → ValueGroup₀ (↑extensionValuation : hat K →*₀ Γ₀)) x <
        (↑γ : ValueGroup₀ extensionValuation)} ⊆
    s
⊢ {x : hat K |
      LT.lt (α := Γ₀) ((embedding : (a : ValueGroup₀ v) → Γ₀) (extension x) : Γ₀)
        ((embedding : (a : ValueGroup₀ v) → Γ₀)
            (↑((Units.map (MulEquiv.toMonoidHom (MulEquiv.symm valueGroup₀_equiv_extensionValuation)) :
                    (a : (ValueGroup₀ extensionValuation)ˣ) → (ValueGroup₀ v)ˣ)
                  γ) :
              ValueGroup₀ v) :
          Γ₀)} ⊆
    s
have h₁ : ∀ (x : hat K),
  LT.lt (α := Γ₀) ((embedding : (a : ValueGroup₀ v) → Γ₀) (extension x) : Γ₀)
      ((embedding : (a : ValueGroup₀ v) → Γ₀)
          (↑((Units.map (MulEquiv.toMonoidHom (MulEquiv.symm valueGroup₀_equiv_extensionValuation)) :
                  (a : (ValueGroup₀ extensionValuation)ˣ) → (ValueGroup₀ v)ˣ)
                γ) :
            ValueGroup₀ v) :
        Γ₀) ↔
    (Valuation.restrict extensionValuation : (a : hat K) → ValueGroup₀ (↑extensionValuation : hat K →*₀ Γ₀)) x <
      (↑γ : ValueGroup₀ extensionValuation)
Tactic: convert! h
-- Lean 4 proof step from Mathlib.Topology.Algebra.Valued.ValuedField (goal)
Goal:
K : Type u_1
inst : Field K
Γ₀ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
s : Set (hat K)
⊢ HasBasis.{u_1, u_2 + 1} (α := hat K) (𝓝 0) (fun (x : (ValueGroup₀ (F := Valuation K Γ₀) v)ˣ) ↦ True)
    fun (γ : (ValueGroup₀ (F := Valuation K Γ₀) v)ˣ) ↦
    {x : hat K |
      LT.lt.{u_2} (α := Γ₀) ((extensionValuation : (a : hat K) → Γ₀) x : Γ₀)
        ((↑((Units.map (↑embedding : ValueGroup₀ v →* Γ₀) : (a : (ValueGroup₀ v)ˣ) → Γ₀ˣ) γ) : Γ₀) : Γ₀)}
have simp_rw : HasBasis.{u_1, u_2 + 1} (α := hat K) (𝓝 0) (fun (x : (ValueGroup₀ (F := Valuation K Γ₀) v)ˣ) ↦ True)
  fun (γ : (ValueGroup₀ (F := Valuation K Γ₀) v)ˣ) ↦
  closure
    (Completion.coe' ''
      {x : K |
        LT.lt.{u_2} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀)
          (((↑embedding : ValueGroup₀ v →* Γ₀) : (a : ValueGroup₀ v) → Γ₀) (↑γ : ValueGroup₀ v) : Γ₀)})
Tactic: simp_rw [← closure_coe_completion_v_lt, Units.coe_map]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Valued.ValuedField (goal)
Goal:
K : Type u_1
inst : Field K
Γ₀ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
s : Set (hat K)
⊢ HasBasis.{u_1, u_2 + 1} (α := hat K) (𝓝 0) (fun (x : (ValueGroup₀ (F := Valuation K Γ₀) v)ˣ) ↦ True)
    fun (γ : (ValueGroup₀ (F := Valuation K Γ₀) v)ˣ) ↦
    closure
      (Completion.coe' ''
        {x : K |
          LT.lt.{u_2} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀)
            (((↑embedding : ValueGroup₀ v →* Γ₀) : (a : ValueGroup₀ v) → Γ₀) (↑γ : ValueGroup₀ v) : Γ₀)})
have h : ∀ (x : (ValueGroup₀ (F := Valuation K Γ₀) v)ˣ) (x_1 : K),
  LT.lt.{u_2} (α := Γ₀) ((v : (a : K) → Γ₀) x_1 : Γ₀)
      (((↑embedding : ValueGroup₀ v →* Γ₀) : (a : ValueGroup₀ v) → Γ₀) (↑x : ValueGroup₀ v) : Γ₀) ↔
    (Valuation.restrict v : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀)) x_1 < (↑x : ValueGroup₀ v)
Tactic: convert! (hasBasis_nhds_zero K Γ₀).hasBasis_of_isDenseInducing Completion.isDenseInducing_coe
-- Lean 4 proof step from Mathlib.Topology.Algebra.Valued.ValuedField (goal)
Goal:
K : Type u_1
inst : Field K
Γ₀ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
s : Set (hat K)
x : (ValueGroup₀ (F := Valuation K Γ₀) v)ˣ
x_1 : K
⊢ LT.lt.{u_2} (α := Γ₀) ((v : (a : K) → Γ₀) x_1 : Γ₀)
      (((↑embedding : ValueGroup₀ v →* Γ₀) : (a : ValueGroup₀ v) → Γ₀) (↑x : ValueGroup₀ v) : Γ₀) ↔
    (Valuation.restrict v : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀)) x_1 < (↑x : ValueGroup₀ v)
have h : LT.lt.{u_2} (α := Γ₀) ((v : (a : K) → Γ₀) x_1 : Γ₀)
    (((↑embedding : ValueGroup₀ v →* Γ₀) : (a : ValueGroup₀ v) → Γ₀) (↑x : ValueGroup₀ v) : Γ₀) ↔
  LT.lt.{u_2} (α := Γ₀) ((v : (a : K) → Γ₀) x_1 : Γ₀) ((embedding : (a : ValueGroup₀ v) → Γ₀) (↑x : ValueGroup₀ v) : Γ₀)
Tactic: rw [Valuation.restrict_lt_iff_lt_embedding]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Valued.ValuedField (goal)
Goal:
K : Type u_1
inst : Field K
Γ₀ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
x : K
⊢ Eq.{u_2 + 1} (α := Γ₀) ((v : (a : hat K) → Γ₀) (↑x : hat K) : Γ₀) ((v : (a : K) → Γ₀) x : Γ₀)
have simp : Eq (α := Γ₀) ((embedding : (a : ValueGroup₀ v) → Γ₀) (extension (↑x : hat K)) : Γ₀) ((v : (a : K) → Γ₀) x : Γ₀)
Tactic: simp only [Valued.v, extensionValuation_toFun]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Valued.ValuedField (goal)
Goal:
K : Type u_1
inst : Field K
Γ₀ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
x : K
⊢ Eq (α := Γ₀) ((embedding : (a : ValueGroup₀ v) → Γ₀) (extension (↑x : hat K)) : Γ₀) ((v : (a : K) → Γ₀) x : Γ₀)
have rw : Eq (α := Γ₀) ((embedding : (a : ValueGroup₀ v) → Γ₀) (extension (↑x : hat K)) : Γ₀)
  ((embedding : (a : ValueGroup₀ v) → Γ₀)
      (((restrict₀ v : MonoidWithZeroHom.{u_1, u_2} K (ValueGroup₀ (F := Valuation K Γ₀) v)) : (a : K) → ValueGroup₀ v)
          x :
        ValueGroup₀ (F := Valuation K Γ₀) v) :
    Γ₀)
Tactic: rw [← embedding_restrict₀ x, extension_extends x, v.restrict_def]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Valued.ValuedField (goal)
Goal:
K : Type u_1
inst : Field K
Γ₀ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
x : K
rw :
  Eq (α := Γ₀) ((embedding : (a : ValueGroup₀ v) → Γ₀) (extension (↑x : hat K)) : Γ₀)
    ((embedding : (a : ValueGroup₀ v) → Γ₀)
        (((restrict₀ v : MonoidWithZeroHom.{u_1, u_2} K (ValueGroup₀ (F := Valuation K Γ₀) v)) :
              (a : K) → ValueGroup₀ v)
            x :
          ValueGroup₀ (F := Valuation K Γ₀) v) :
      Γ₀)
⊢ Eq (α := Γ₀) ((embedding : (a : ValueGroup₀ v) → Γ₀) (extension (↑x : hat K)) : Γ₀) ((v : (a : K) → Γ₀) x : Γ₀)
have rw₁ : Eq (α := Γ₀)
  ((embedding : (a : ValueGroup₀ v) → Γ₀)
      ((Valuation.restrict v : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀)) x : ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀)) :
    Γ₀)
  ((embedding : (a : ValueGroup₀ v) → Γ₀)
      (((restrict₀ v : MonoidWithZeroHom.{u_1, u_2} K (ValueGroup₀ (F := Valuation K Γ₀) v)) : (a : K) → ValueGroup₀ v)
          x :
        ValueGroup₀ (F := Valuation K Γ₀) v) :
    Γ₀)
Tactic: rw [← embedding_restrict₀ x, extension_extends x, v.restrict_def]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Valued.ValuedField (goal)
Goal:
K : Type u_1
inst : Field K
Γ₀ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
x : K
rw :
  Eq (α := Γ₀) ((embedding : (a : ValueGroup₀ v) → Γ₀) (extension (↑x : hat K)) : Γ₀)
    ((embedding : (a : ValueGroup₀ v) → Γ₀)
        (((restrict₀ v : MonoidWithZeroHom.{u_1, u_2} K (ValueGroup₀ (F := Valuation K Γ₀) v)) :
              (a : K) → ValueGroup₀ v)
            x :
          ValueGroup₀ (F := Valuation K Γ₀) v) :
      Γ₀)
rw₁ :
  Eq (α := Γ₀)
    ((embedding : (a : ValueGroup₀ v) → Γ₀)
        ((Valuation.restrict v : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀)) x :
          ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀)) :
      Γ₀)
    ((embedding : (a : ValueGroup₀ v) → Γ₀)
        (((restrict₀ v : MonoidWithZeroHom.{u_1, u_2} K (ValueGroup₀ (F := Valuation K Γ₀) v)) :
              (a : K) → ValueGroup₀ v)
            x :
          ValueGroup₀ (F := Valuation K Γ₀) v) :
      Γ₀)
⊢ Eq (α := Γ₀) ((embedding : (a : ValueGroup₀ v) → Γ₀) (extension (↑x : hat K)) : Γ₀) ((v : (a : K) → Γ₀) x : Γ₀)
have rw₂ : Eq (α := Γ₀)
  ((embedding : (a : ValueGroup₀ v) → Γ₀)
      (((restrict₀ v : MonoidWithZeroHom.{u_1, u_2} K (ValueGroup₀ (F := Valuation K Γ₀) v)) : (a : K) → ValueGroup₀ v)
          x :
        ValueGroup₀ (F := Valuation K Γ₀) v) :
    Γ₀)
  ((embedding : (a : ValueGroup₀ v) → Γ₀)
      (((restrict₀ v : MonoidWithZeroHom.{u_1, u_2} K (ValueGroup₀ (F := Valuation K Γ₀) v)) : (a : K) → ValueGroup₀ v)
          x :
        ValueGroup₀ (F := Valuation K Γ₀) v) :
    Γ₀)
Tactic: rw [← embedding_restrict₀ x, extension_extends x, v.restrict_def]