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 Γ₀
x : ValueGroup₀ (F := Valuation.{u_1, u_2} (hat K) Γ₀) extensionValuation
k' : hat K
hk' :
  ((restrict₀ extensionValuation :
          MonoidWithZeroHom.{u_1, u_2} (hat K)
            (ValueGroup₀ (F := Valuation.{u_1, u_2} (hat K) Γ₀) extensionValuation)) :
        (a : hat K) → ValueGroup₀ extensionValuation)
      k' =
    x
k : K
hk :
  ((restrict₀ v : MonoidWithZeroHom.{u_1, u_2} K (ValueGroup₀ (F := Valuation K Γ₀) v)) : (a : K) → ValueGroup₀ v) k =
    extension k'
h :
  Eq (α := Γ₀)
    ((embedding : (a : ValueGroup₀ v) → Γ₀)
        ((Valuation.restrict v : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀))
            (⋯.choose (p := fun (a : K) ↦
              ((restrict₀ v : MonoidWithZeroHom.{u_1, u_2} K (ValueGroup₀ (F := Valuation K Γ₀) v)) :
                    (a : K) → ValueGroup₀ v)
                  a =
                extension k')) :
          ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀)) :
      Γ₀)
    ((embedding : (a : ValueGroup₀ v) → Γ₀) (extension k') : Γ₀)
⊢ Eq.{u_2 + 1} (α := Γ₀)
    ((Valuation.toMonoidWithZeroHom extensionValuation : (a : hat K) → Γ₀)
        (↑(⋯.choose (p := fun (a : K) ↦
              ((restrict₀ v : MonoidWithZeroHom.{u_1, u_2} K (ValueGroup₀ (F := Valuation K Γ₀) v)) :
                    (a : K) → ValueGroup₀ v)
                  a =
                extension k')) :
          hat K) :
      Γ₀)
    ((Valuation.toMonoidWithZeroHom extensionValuation : (a : hat K) → Γ₀) k' : Γ₀)

Tactic:
simp only [Valuation.toMonoidWithZeroHom_coe_eq_coe,
      extensionValuation_toFun, extension_extends]

Premises used: Valued.extension_extends, Valuation.toMonoidWithZeroHom_coe_eq_coe, 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 : ValueGroup₀ (F := Valuation.{u_1, u_2} (hat K) Γ₀) extensionValuation
k' : hat K
hk' :
  ((restrict₀ extensionValuation :
          MonoidWithZeroHom.{u_1, u_2} (hat K)
            (ValueGroup₀ (F := Valuation.{u_1, u_2} (hat K) Γ₀) extensionValuation)) :
        (a : hat K) → ValueGroup₀ extensionValuation)
      k' =
    x
k : K
hk :
  ((restrict₀ v : MonoidWithZeroHom.{u_1, u_2} K (ValueGroup₀ (F := Valuation K Γ₀) v)) : (a : K) → ValueGroup₀ v) k =
    extension k'
h :
  (Valuation.restrict v : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀))
      (⋯.choose (p := fun (a : K) ↦
        ((restrict₀ v : MonoidWithZeroHom.{u_1, u_2} K (ValueGroup₀ (F := Valuation K Γ₀) v)) : (a : K) → ValueGroup₀ v)
            a =
          extension k')) =
    extension k'
⊢ Eq (α := Γ₀)
    ((embedding : (a : ValueGroup₀ v) → Γ₀)
        ((Valuation.restrict v : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀))
            (⋯.choose (p := fun (a : K) ↦
              ((restrict₀ v : MonoidWithZeroHom.{u_1, u_2} K (ValueGroup₀ (F := Valuation K Γ₀) v)) :
                    (a : K) → ValueGroup₀ v)
                  a =
                extension k')) :
          ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀)) :
      Γ₀)
    ((embedding : (a : ValueGroup₀ v) → Γ₀) (extension k') : Γ₀)

Tactic:
rw [embedding_strictMono.injective.eq_iff]

Premises used: Function.Injective.eq_iff, StrictMono.injective
-- Module: Mathlib.Topology.Algebra.Valued.ValuedField
Goal:
K : Type u_1
inst : Field K
Γ₀ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
x : ValueGroup₀ (F := Valuation.{u_1, u_2} (hat K) Γ₀) extensionValuation
k' : hat K
hk' :
  ((restrict₀ extensionValuation :
          MonoidWithZeroHom.{u_1, u_2} (hat K)
            (ValueGroup₀ (F := Valuation.{u_1, u_2} (hat K) Γ₀) extensionValuation)) :
        (a : hat K) → ValueGroup₀ extensionValuation)
      k' =
    x
k : K
hk :
  ((restrict₀ v : MonoidWithZeroHom.{u_1, u_2} K (ValueGroup₀ (F := Valuation K Γ₀) v)) : (a : K) → ValueGroup₀ v) k =
    extension k'
⊢ (Valuation.restrict v : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀))
      (⋯.choose (p := fun (a : K) ↦
        ((restrict₀ v : MonoidWithZeroHom.{u_1, u_2} K (ValueGroup₀ (F := Valuation K Γ₀) v)) : (a : K) → ValueGroup₀ v)
            a =
          extension k')) =
    extension k'

Tactic:
(restrict₀_surjective hv.v _).choose_spec

Premises used: Exists.choose_spec, Set.Mem, Valued.v, setOf, MonoidWithZeroHom.ValueGroup₀.restrict₀_surjective
-- Module: Mathlib.Topology.Algebra.Valued.ValuedField
Goal:
K : Type u_1
inst : Field K
Γ₀ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
x : ValueGroup₀ (F := Valuation.{u_1, u_2} (hat K) Γ₀) extensionValuation
k' : hat K
hk' :
  ((restrict₀ extensionValuation :
          MonoidWithZeroHom.{u_1, u_2} (hat K)
            (ValueGroup₀ (F := Valuation.{u_1, u_2} (hat K) Γ₀) extensionValuation)) :
        (a : hat K) → ValueGroup₀ extensionValuation)
      k' =
    x
k : K
hk :
  ((restrict₀ v : MonoidWithZeroHom.{u_1, u_2} K (ValueGroup₀ (F := Valuation K Γ₀) v)) : (a : K) → ValueGroup₀ v) k =
    extension k'
⊢ (Valuation.restrict v : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀))
      (⋯.choose (p := fun (a : K) ↦
        ((restrict₀ v : MonoidWithZeroHom.{u_1, u_2} K (ValueGroup₀ (F := Valuation K Γ₀) v)) : (a : K) → ValueGroup₀ v)
            a =
          extension k')) =
    extension k'

Tactic:
exact (restrict₀_surjective hv.v _).choose_spec

Premises used: Exists.choose_spec, Valued.v, MonoidWithZeroHom.ValueGroup₀.restrict₀_surjective
-- 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 :
  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)ˣ) → Γ₀ˣ) γ) : Γ₀) : Γ₀)}
rw :
  (∃ (i : (ValueGroup₀ (F := Valuation K Γ₀) v)ˣ),
      True ∧
        {x : hat K |
            LT.lt.{u_2} (α := Γ₀) ((extensionValuation : (a : hat K) → Γ₀) x : Γ₀)
              ((↑((Units.map (↑embedding : ValueGroup₀ v →* Γ₀) : (a : (ValueGroup₀ v)ˣ) → Γ₀ˣ) i) : Γ₀) : Γ₀)} ⊆
          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
⊢ Membership.mem (γ := Filter (hat K)) (𝓝 0) 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:
rw [this.mem_iff]

Premises used: Filter.HasBasis.mem_iff
-- 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 :
  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)ˣ) → Γ₀ˣ) γ) : Γ₀) : Γ₀)}
simp :
  (∃ (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
⊢ (∃ (i : (ValueGroup₀ (F := Valuation K Γ₀) v)ˣ),
      True ∧
        {x : hat K |
            LT.lt.{u_2} (α := Γ₀) ((extensionValuation : (a : hat K) → Γ₀) x : Γ₀)
              ((↑((Units.map (↑embedding : ValueGroup₀ v →* Γ₀) : (a : (ValueGroup₀ v)ˣ) → Γ₀ˣ) i) : Γ₀) : Γ₀)} ⊆
          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:
simp only [extensionValuation_toFun, Units.coe_map, MonoidHom.coe_coe, true_and]

Premises used: Units.coe_map, MonoidHom.coe_coe, true_and, 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 Γ₀
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)ˣ
rw :
  LT.lt (α := ValueGroup₀ (F := MonoidWithZeroHom.{u_1, u_2} (hat K) Γ₀) (↑extensionValuation : hat K →*₀ Γ₀))
      (if h : Eq.{u_2 + 1} (α := Γ₀) ((extensionValuation : (a : hat K) → Γ₀) x : Γ₀) (0 : Γ₀) then 0
        else
          (↑(Subtype.mk (p := fun (x : Γ₀ˣ) ↦
                Membership.mem (γ := Subgroup Γ₀ˣ)
                  (valueGroup (F := Valuation.{u_1, u_2} (hat K) Γ₀) extensionValuation) x)
                (Units.mk0 ((extensionValuation : (a : hat K) → Γ₀) x) h) ⋯) :
            WithZero ↥(valueGroup extensionValuation)) :
        ValueGroup₀ (F := Valuation.{u_1, u_2} (hat K) Γ₀) extensionValuation)
      ((valueGroup₀_equiv_extensionValuation : (a : ValueGroup₀ v) → ValueGroup₀ extensionValuation)
          (↑γ : ValueGroup₀ v) :
        ValueGroup₀ (F := Valuation.{u_1, u_2} (hat K) Γ₀) extensionValuation) ↔
    extension x < (↑γ : ValueGroup₀ 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 →*₀ Γ₀))
      ((valueGroup₀_equiv_extensionValuation : (a : ValueGroup₀ v) → ValueGroup₀ extensionValuation)
          (↑γ : ValueGroup₀ v) :
        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:
rw [embedding_strictMono.lt_iff_lt, Valuation.restrict_def, restrict₀_apply]

Premises used: StrictMono.lt_iff_lt, 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)
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
pos :
  LT.lt (α := ValueGroup₀ (F := MonoidWithZeroHom.{u_1, u_2} (hat K) Γ₀) (↑extensionValuation : hat K →*₀ Γ₀))
      (if h : Eq.{u_2 + 1} (α := Γ₀) ((extensionValuation : (a : hat K) → Γ₀) 0 : Γ₀) (0 : Γ₀) then 0
        else
          (↑(Subtype.mk (p := fun (x : Γ₀ˣ) ↦
                Membership.mem (γ := Subgroup Γ₀ˣ)
                  (valueGroup (F := Valuation.{u_1, u_2} (hat K) Γ₀) extensionValuation) x)
                (Units.mk0 ((extensionValuation : (a : hat K) → Γ₀) 0) ⋯) ⋯) :
            WithZero ↥(valueGroup extensionValuation)) :
        ValueGroup₀ (F := Valuation.{u_1, u_2} (hat K) Γ₀) extensionValuation)
      ((valueGroup₀_equiv_extensionValuation : (a : ValueGroup₀ v) → ValueGroup₀ extensionValuation)
          (↑γ : ValueGroup₀ v) :
        ValueGroup₀ (F := Valuation.{u_1, u_2} (hat K) Γ₀) extensionValuation) ↔
    extension 0 < (↑γ : ValueGroup₀ v)
⊢ LT.lt (α := ValueGroup₀ (F := MonoidWithZeroHom.{u_1, u_2} (hat K) Γ₀) (↑extensionValuation : hat K →*₀ Γ₀))
      (if h : Eq.{u_2 + 1} (α := Γ₀) ((extensionValuation : (a : hat K) → Γ₀) x : Γ₀) (0 : Γ₀) then 0
        else
          (↑(Subtype.mk (p := fun (x : Γ₀ˣ) ↦
                Membership.mem (γ := Subgroup Γ₀ˣ)
                  (valueGroup (F := Valuation.{u_1, u_2} (hat K) Γ₀) extensionValuation) x)
                (Units.mk0 ((extensionValuation : (a : hat K) → Γ₀) x) h) ⋯) :
            WithZero ↥(valueGroup extensionValuation)) :
        ValueGroup₀ (F := Valuation.{u_1, u_2} (hat K) Γ₀) extensionValuation)
      ((valueGroup₀_equiv_extensionValuation : (a : ValueGroup₀ v) → ValueGroup₀ extensionValuation)
          (↑γ : ValueGroup₀ v) :
        ValueGroup₀ (F := Valuation.{u_1, u_2} (hat K) Γ₀) extensionValuation) ↔
    extension x < (↑γ : ValueGroup₀ v)

Tactic:
simp only [hx0]
-- 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 :
  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
pos :
  LT.lt (α := ValueGroup₀ (F := MonoidWithZeroHom.{u_1, u_2} (hat K) Γ₀) (↑extensionValuation : hat K →*₀ Γ₀))
      (0 : ValueGroup₀ (F := Valuation.{u_1, u_2} (hat K) Γ₀) extensionValuation)
      ((valueGroup₀_equiv_extensionValuation : (a : ValueGroup₀ v) → ValueGroup₀ extensionValuation)
          (↑γ : ValueGroup₀ v) :
        ValueGroup₀ (F := Valuation.{u_1, u_2} (hat K) Γ₀) extensionValuation) ↔
    extension 0 < (↑γ : ValueGroup₀ v)
⊢ LT.lt (α := ValueGroup₀ (F := MonoidWithZeroHom.{u_1, u_2} (hat K) Γ₀) (↑extensionValuation : hat K →*₀ Γ₀))
      (if h : Eq.{u_2 + 1} (α := Γ₀) ((extensionValuation : (a : hat K) → Γ₀) 0 : Γ₀) (0 : Γ₀) then 0
        else
          (↑(Subtype.mk (p := fun (x : Γ₀ˣ) ↦
                Membership.mem (γ := Subgroup Γ₀ˣ)
                  (valueGroup (F := Valuation.{u_1, u_2} (hat K) Γ₀) extensionValuation) x)
                (Units.mk0 ((extensionValuation : (a : hat K) → Γ₀) 0) ⋯) ⋯) :
            WithZero ↥(valueGroup extensionValuation)) :
        ValueGroup₀ (F := Valuation.{u_1, u_2} (hat K) Γ₀) extensionValuation)
      ((valueGroup₀_equiv_extensionValuation : (a : ValueGroup₀ v) → ValueGroup₀ extensionValuation)
          (↑γ : ValueGroup₀ v) :
        ValueGroup₀ (F := Valuation.{u_1, u_2} (hat K) Γ₀) extensionValuation) ↔
    extension 0 < (↑γ : ValueGroup₀ v)

Tactic:
rw [dif_pos (map_zero _)]

Premises used: map_zero, dif_pos
-- 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 :
  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
pos :
  LT.lt.{u_2} (α := ValueGroup₀ (F := MonoidWithZeroHom.{u_1, u_2} (hat K) Γ₀) (↑extensionValuation : hat K →*₀ Γ₀))
      (0 : ValueGroup₀ (F := Valuation.{u_1, u_2} (hat K) Γ₀) extensionValuation)
      ((↑(Subtype.mk (p := fun (x : Γ₀ˣ) ↦
              Membership.mem (γ := Subgroup Γ₀ˣ) (valueGroup (F := Valuation.{u_1, u_2} (hat K) Γ₀) extensionValuation)
                x)
              (Units.mk0
                ((extensionValuation : (a : hat K) → Γ₀)
                  (↑(⋯.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))) :
                    hat K))
                ⋯)
              ⋯) :
          WithZero ↥(valueGroup (F := Valuation.{u_1, u_2} (hat K) Γ₀) extensionValuation)) :
        WithZero ↥(valueGroup (F := Valuation.{u_1, u_2} (hat K) Γ₀) extensionValuation)) ↔
    extension 0 < (↑γ : ValueGroup₀ v)
pos₁ :
  ¬Eq.{u_2 + 1} (α := Γ₀)
      ((extensionValuation : (a : hat K) → Γ₀)
          (↑(⋯.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))) :
            hat K) :
        Γ₀)
      (0 : Γ₀)
⊢ LT.lt.{u_2} (α := ValueGroup₀ (F := MonoidWithZeroHom.{u_1, u_2} (hat K) Γ₀) (↑extensionValuation : hat K →*₀ Γ₀))
      (0 : ValueGroup₀ (F := Valuation.{u_1, u_2} (hat K) Γ₀) extensionValuation)
      ((Valuation.restrict extensionValuation : (a : hat K) → ValueGroup₀ (↑extensionValuation : hat K →*₀ Γ₀))
          (↑(⋯.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))) :
            hat K) :
        ValueGroup₀ (F := MonoidWithZeroHom.{u_1, u_2} (hat K) Γ₀) (↑extensionValuation : hat K →*₀ Γ₀)) ↔
    extension 0 < (↑γ : ValueGroup₀ v)

Tactic:
rw [Valuation.restrict_def, restrict₀_apply, dif_neg]

Premises used: dif_neg, 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)
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
rw rw₁ : Eq.{u_1 + 1} (α := hat K) 0 0
⊢ Eq (α := ValueGroup₀ (F := Valuation K Γ₀) v) (extension 0) 0

Tactic:
rw [extension_eq_zero_iff]

Premises used: Valued.extension_eq_zero_iff
-- 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 :
  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
⊢ Eq (α := ValueGroup₀ (F := Valuation K Γ₀) v) (extension 0) 0

Tactic:
have hext : hv.extension 0 = 0 := by rw [extension_eq_zero_iff]
-- 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 :
  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
hext : Eq (α := ValueGroup₀ (F := Valuation K Γ₀) v) (extension 0) 0
⊢ LT.lt.{u_2} (α := ValueGroup₀ (F := MonoidWithZeroHom.{u_1, u_2} (hat K) Γ₀) (↑extensionValuation : hat K →*₀ Γ₀))
      (0 : ValueGroup₀ (F := Valuation.{u_1, u_2} (hat K) Γ₀) extensionValuation)
      ((↑(Subtype.mk (p := fun (x : Γ₀ˣ) ↦
              Membership.mem (γ := Subgroup Γ₀ˣ) (valueGroup (F := Valuation.{u_1, u_2} (hat K) Γ₀) extensionValuation)
                x)
              (Units.mk0
                ((extensionValuation : (a : hat K) → Γ₀)
                  (↑(⋯.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))) :
                    hat K))
                ⋯)
              ⋯) :
          WithZero ↥(valueGroup (F := Valuation.{u_1, u_2} (hat K) Γ₀) extensionValuation)) :
        WithZero ↥(valueGroup (F := Valuation.{u_1, u_2} (hat K) Γ₀) extensionValuation)) ↔
    extension 0 < (↑γ : ValueGroup₀ v)

Tactic:
simp [hext]
-- 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 :
  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
⊢ ¬Eq.{u_2 + 1} (α := Γ₀)
      ((extensionValuation : (a : hat K) → Γ₀)
          (↑(⋯.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))) :
            hat K) :
        Γ₀)
      (0 : Γ₀)

Tactic:
simp [← v.restrict.zero_iff, v.restrict_def,
                (restrict₀_surjective hv.v _).choose_spec]

Premises used: Exists.choose_spec, Valued.v, Valuation.zero_iff, Valuation.restrict_def, MonoidWithZeroHom.ValueGroup₀.restrict₀_surjective, Valuation.restrict
-- 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 :
  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
⊢ ¬Eq.{u_2 + 1} (α := Γ₀) ((extensionValuation : (a : hat K) → Γ₀) x : Γ₀) (0 : Γ₀)

Tactic:
simp [hx0]