awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Algebra.Valued.ValuedField
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
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) ↔
    LT.lt (α := Γ₀) ((embedding : (a : ValueGroup₀ v) → Γ₀) (extension x) : Γ₀)
      ((embedding : (a : ValueGroup₀ v) → Γ₀) (↑γ : ValueGroup₀ v) : Γ₀)

Tactic:
apply this
-- Module: Mathlib.Topology.Algebra.Valued.ValuedField
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
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
⊢ ∃ (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

Tactic:
use Units.map valueGroup₀_equiv_extensionValuation.symm.toMonoidHom γ

Premises used: Valued.valueGroup₀_equiv_extensionValuation, MulEquiv.toMonoidHom, MulEquiv.symm, DFunLike.coe, Units.map
-- Module: Mathlib.Topology.Algebra.Valued.ValuedField
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 |
      (Valuation.restrict extensionValuation : (a : hat K) → ValueGroup₀ (↑extensionValuation : hat K →*₀ Γ₀)) x <
        (↑γ : ValueGroup₀ extensionValuation)} ⊆
    s

Tactic:
h
-- Module: Mathlib.Topology.Algebra.Valued.ValuedField
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
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)
⊢ {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:
convert! h
-- Module: Mathlib.Topology.Algebra.Valued.ValuedField
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.{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)ˣ)
              ((Units.map (MulEquiv.toMonoidHom (MulEquiv.symm valueGroup₀_equiv_extensionValuation)) :
                  (a : (ValueGroup₀ extensionValuation)ˣ) → (ValueGroup₀ v)ˣ)
                γ)) :
          ValueGroup₀ (F := Valuation.{u_1, u_2} (hat K) Γ₀) extensionValuation) :
        ValueGroup₀ (F := Valuation.{u_1, u_2} (hat K) Γ₀) extensionValuation) ↔
    (Valuation.restrict extensionValuation : (a : hat K) → ValueGroup₀ (↑extensionValuation : hat K →*₀ Γ₀)) x <
      (↑γ : ValueGroup₀ extensionValuation)

Tactic:
simp [Valuation.restrict_def, restrict₀_apply]

Premises used: Valuation.restrict_def, MonoidWithZeroHom.ValueGroup₀.restrict₀_apply
-- Module: Mathlib.Topology.Algebra.Valued.ValuedField
Goal:
K : Type u_1
inst : Field K
Γ₀ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
s : Set (hat K)
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) : Γ₀)})
⊢ 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)ˣ) → Γ₀ˣ) γ) : Γ₀) : Γ₀)}

Tactic:
simp_rw [← closure_coe_completion_v_lt, Units.coe_map]

Premises used: Units.coe_map, Valued.closure_coe_completion_v_lt
-- Module: Mathlib.Topology.Algebra.Valued.ValuedField
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 : hat K)) (fun (x : (ValueGroup₀ (F := Valuation K Γ₀) v)ˣ) ↦ True)
    fun (i : (ValueGroup₀ (F := Valuation K Γ₀) v)ˣ) ↦
    closure
      (Completion.coe' ''
        {x : K | (Valuation.restrict v : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀)) x < (↑i : ValueGroup₀ v)})

Tactic:
(hasBasis_nhds_zero K Γ₀).hasBasis_of_isDenseInducing Completion.isDenseInducing_coe

Premises used: Filter.HasBasis.hasBasis_of_isDenseInducing, Valued.hasBasis_nhds_zero, UniformSpace.Completion.isDenseInducing_coe
-- Module: Mathlib.Topology.Algebra.Valued.ValuedField
Goal:
K : Type u_1
inst : Field K
Γ₀ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
s : Set (hat K)
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)
⊢ 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:
convert! (hasBasis_nhds_zero K Γ₀).hasBasis_of_isDenseInducing Completion.isDenseInducing_coe

Premises used: Filter.HasBasis.hasBasis_of_isDenseInducing, Valued.hasBasis_nhds_zero, UniformSpace.Completion.isDenseInducing_coe
-- Module: Mathlib.Topology.Algebra.Valued.ValuedField
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
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) : Γ₀)
⊢ 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:
rw [Valuation.restrict_lt_iff_lt_embedding]

Premises used: Valuation.restrict_lt_iff_lt_embedding
-- Module: Mathlib.Topology.Algebra.Valued.ValuedField
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) : Γ₀) ↔
    LT.lt.{u_2} (α := Γ₀) ((v : (a : K) → Γ₀) x_1 : Γ₀)
      ((embedding : (a : ValueGroup₀ v) → Γ₀) (↑x : ValueGroup₀ v) : Γ₀)

Tactic:
rfl
-- Module: Mathlib.Topology.Algebra.Valued.ValuedField
Goal:
K : Type u_1
inst : Field K
Γ₀ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
x : K
simp : Eq (α := Γ₀) ((embedding : (a : ValueGroup₀ v) → Γ₀) (extension (↑x : hat K)) : Γ₀) ((v : (a : K) → Γ₀) x : Γ₀)
⊢ Eq.{u_2 + 1} (α := Γ₀) ((v : (a : hat K) → Γ₀) (↑x : hat K) : Γ₀) ((v : (a : K) → Γ₀) x : Γ₀)

Tactic:
simp only [Valued.v, extensionValuation_toFun]

Premises used: Valued.v, Valued.extensionValuation_toFun
-- Module: Mathlib.Topology.Algebra.Valued.ValuedField
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) :
      Γ₀)
rw₂ 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) :
      Γ₀)
⊢ Eq (α := Γ₀) ((embedding : (a : ValueGroup₀ v) → Γ₀) (extension (↑x : hat K)) : Γ₀) ((v : (a : K) → Γ₀) x : Γ₀)

Tactic:
rw [← embedding_restrict₀ x, extension_extends x, v.restrict_def]

Premises used: Valued.extension_extends, Valued.v, Valuation.restrict_def, MonoidWithZeroHom.ValueGroup₀.embedding_restrict₀
-- Module: Mathlib.Topology.Algebra.Valued.ValuedField
Goal:
K : Type u_1
inst : Field K
Γ₀ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
mp :
  Function.Surjective.{u_1 + 1, u_2 + 1} (α := hat K) (β := Γ₀) (⇑v : (a : hat K) → Γ₀) →
    Function.Surjective.{u_1 + 1, u_2 + 1} (α := K) (β := Γ₀) (⇑v : (a : K) → Γ₀)
mpr :
  Function.Surjective.{u_1 + 1, u_2 + 1} (α := K) (β := Γ₀) (⇑v : (a : K) → Γ₀) →
    Function.Surjective.{u_1 + 1, u_2 + 1} (α := hat K) (β := Γ₀) (⇑v : (a : hat K) → Γ₀)
⊢ Function.Surjective.{u_1 + 1, u_2 + 1} (α := hat K) (β := Γ₀) (⇑v : (a : hat K) → Γ₀) ↔
    Function.Surjective.{u_1 + 1, u_2 + 1} (α := K) (β := Γ₀) (⇑v : (a : K) → Γ₀)

Tactic:
constructor
-- Module: Mathlib.Topology.Algebra.Valued.ValuedField
Goal:
K : Type u_1
inst : Field K
Γ₀ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
h : Function.Surjective.{u_1 + 1, u_2 + 1} (α := hat K) (β := Γ₀) (⇑v : (a : hat K) → Γ₀)
γ : Γ₀
mp : ∀ (a : hat K) (ha : (v : (a : hat K) → Γ₀) a = γ), ∃ (a : K), (v : (a : K) → Γ₀) a = γ
⊢ ∃ (a : K), (v : (a : K) → Γ₀) a = γ

Tactic:
obtain ⟨a, ha⟩ := h γ
-- Module: Mathlib.Topology.Algebra.Valued.ValuedField
Goal:
K : Type u_1
inst : Field K
Γ₀ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
h : Function.Surjective.{u_1 + 1, u_2 + 1} (α := K) (β := Γ₀) (⇑v : (a : K) → Γ₀)
γ : Γ₀
mpr : ∀ (a : K) (ha : (v : (a : K) → Γ₀) a = γ), ∃ (a : hat K), (v : (a : hat K) → Γ₀) a = γ
⊢ ∃ (a : hat K), (v : (a : hat K) → Γ₀) a = γ

Tactic:
obtain ⟨a, ha⟩ := h γ
-- Module: Mathlib.Topology.Algebra.Valued.ValuedField
Goal:
K : Type u_1
inst : Field K
Γ₀ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
h : Function.Surjective.{u_1 + 1, u_2 + 1} (α := hat K) (β := Γ₀) (⇑v : (a : hat K) → Γ₀)
γ : Γ₀
a : hat K
ha : (v : (a : hat K) → Γ₀) a = γ
mp :
  IsClosed.{u_1} (X := hat K) {a : hat K | ∀ (ha : (v : (a : hat K) → Γ₀) a = γ), ∃ (a : K), (v : (a : K) → Γ₀) a = γ}
mp₁ : ∀ (a : K) (ha : (v : (a : hat K) → Γ₀) (↑a : hat K) = γ), ∃ (a : K), (v : (a : K) → Γ₀) a = γ
⊢ ∃ (a : K), (v : (a : K) → Γ₀) a = γ

Tactic:
induction a using Completion.induction_on
-- Module: Mathlib.Topology.Algebra.Valued.ValuedField
Goal:
K : Type u_1
inst : Field K
Γ₀ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
h : Function.Surjective.{u_1 + 1, u_2 + 1} (α := hat K) (β := Γ₀) (⇑v : (a : hat K) → Γ₀)
γ : Γ₀
pos :
  ∀ (H : ∃ (x : K), (v : (a : K) → Γ₀) x = γ),
    IsClosed.{u_1} (X := hat K) {a : hat K | ∀ (ha : (v : (a : hat K) → Γ₀) a = γ), ∃ (a : K), (v : (a : K) → Γ₀) a = γ}
neg :
  ∀ (H : ¬∃ (x : K), (v : (a : K) → Γ₀) x = γ),
    IsClosed.{u_1} (X := hat K) {a : hat K | ∀ (ha : (v : (a : hat K) → Γ₀) a = γ), ∃ (a : K), (v : (a : K) → Γ₀) a = γ}
⊢ IsClosed.{u_1} (X := hat K) {a : hat K | ∀ (ha : (v : (a : hat K) → Γ₀) a = γ), ∃ (a : K), (v : (a : K) → Γ₀) a = γ}

Tactic:
by_cases H : ∃ x : K, (v : K → Γ₀) x = γ
-- Module: Mathlib.Topology.Algebra.Valued.ValuedField
Goal:
K : Type u_1
inst : Field K
Γ₀ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
h : Function.Surjective.{u_1 + 1, u_2 + 1} (α := hat K) (β := Γ₀) (⇑v : (a : hat K) → Γ₀)
γ : Γ₀
H : ∃ (x : K), (v : (a : K) → Γ₀) x = γ
⊢ IsClosed.{u_1} (X := hat K) {a : hat K | ∀ (ha : (v : (a : hat K) → Γ₀) a = γ), ∃ (a : K), (v : (a : K) → Γ₀) a = γ}

Tactic:
simp [H]