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 Γ₀
a b : ValueGroup₀ (F := Valuation K Γ₀) v
hab :
  Eq.{u_2 + 1} (α := ValueGroup₀ (F := Valuation.{u_1, u_2} (hat K) Γ₀) extensionValuation)
    ((Valuation.restrict extensionValuation : (a : hat K) → ValueGroup₀ (↑extensionValuation : hat K →*₀ Γ₀))
        (↑(⋯.choose (p := fun (a_1 : K) ↦
              ((restrict₀ v : MonoidWithZeroHom.{u_1, u_2} K (ValueGroup₀ (F := Valuation K Γ₀) v)) :
                    (a : K) → ValueGroup₀ v)
                  a_1 =
                a)) :
          hat K) :
      ValueGroup₀ (F := MonoidWithZeroHom.{u_1, u_2} (hat K) Γ₀) (↑extensionValuation : hat K →*₀ Γ₀))
    ((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 =
                b)) :
          hat K) :
      ValueGroup₀ (F := MonoidWithZeroHom.{u_1, u_2} (hat K) Γ₀) (↑extensionValuation : hat K →*₀ Γ₀))
x : K :=
  Exists.choose (p := fun (a_1 : K) ↦
    ((restrict₀ v : MonoidWithZeroHom.{u_1, u_2} K (ValueGroup₀ (F := Valuation K Γ₀) v)) : (a : K) → ValueGroup₀ v)
        a_1 =
      a)
    ⋯
hx_def :
  x =
    Exists.choose (p := fun (a_1 : K) ↦
      ((restrict₀ v : MonoidWithZeroHom.{u_1, u_2} K (ValueGroup₀ (F := Valuation K Γ₀) v)) : (a : K) → ValueGroup₀ v)
          a_1 =
        a)
      ⋯
hx : ((restrict₀ v : MonoidWithZeroHom.{u_1, u_2} K (ValueGroup₀ (F := Valuation K Γ₀) v)) : (a : K) → ValueGroup₀ v)
    (Exists.choose (p := fun (a_1 : K) ↦
      ((restrict₀ v : MonoidWithZeroHom.{u_1, u_2} K (ValueGroup₀ (F := Valuation K Γ₀) v)) : (a : K) → ValueGroup₀ v)
          a_1 =
        a)
      ⋯) =
  a :=
  ⋯
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 =
      b)
    ⋯
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 =
        b)
      ⋯
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 =
        b)
      ⋯) =
  b :=
  ⋯
ha0 : a = 0
h0 : Eq (α := ValueGroup₀ (F := Valuation K Γ₀) v) (extension ((algebraMap K (hat K) : (a : K) → hat K) x)) 0
this : y = 0
⊢ a = b
have pos : ∀ (hy : 0 = b) (ha0 : a = 0)
  (h0 : Eq (α := ValueGroup₀ (F := Valuation K Γ₀) v) (extension ((algebraMap K (hat K) : (a : K) → hat K) x)) 0)
  (this : y = 0), a = b
Tactic: rw [restrict₀_apply, dif_pos] at hy
Cleared hypotheses: hy, ha0, h0, this
-- 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 Γ₀
a b : ValueGroup₀ (F := Valuation K Γ₀) v
hab :
  Eq.{u_2 + 1} (α := ValueGroup₀ (F := Valuation.{u_1, u_2} (hat K) Γ₀) extensionValuation)
    ((Valuation.restrict extensionValuation : (a : hat K) → ValueGroup₀ (↑extensionValuation : hat K →*₀ Γ₀))
        (↑(⋯.choose (p := fun (a_1 : K) ↦
              ((restrict₀ v : MonoidWithZeroHom.{u_1, u_2} K (ValueGroup₀ (F := Valuation K Γ₀) v)) :
                    (a : K) → ValueGroup₀ v)
                  a_1 =
                a)) :
          hat K) :
      ValueGroup₀ (F := MonoidWithZeroHom.{u_1, u_2} (hat K) Γ₀) (↑extensionValuation : hat K →*₀ Γ₀))
    ((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 =
                b)) :
          hat K) :
      ValueGroup₀ (F := MonoidWithZeroHom.{u_1, u_2} (hat K) Γ₀) (↑extensionValuation : hat K →*₀ Γ₀))
x : K :=
  Exists.choose (p := fun (a_1 : K) ↦
    ((restrict₀ v : MonoidWithZeroHom.{u_1, u_2} K (ValueGroup₀ (F := Valuation K Γ₀) v)) : (a : K) → ValueGroup₀ v)
        a_1 =
      a)
    ⋯
hx_def :
  x =
    Exists.choose (p := fun (a_1 : K) ↦
      ((restrict₀ v : MonoidWithZeroHom.{u_1, u_2} K (ValueGroup₀ (F := Valuation K Γ₀) v)) : (a : K) → ValueGroup₀ v)
          a_1 =
        a)
      ⋯
hx : ((restrict₀ v : MonoidWithZeroHom.{u_1, u_2} K (ValueGroup₀ (F := Valuation K Γ₀) v)) : (a : K) → ValueGroup₀ v)
    (Exists.choose (p := fun (a_1 : K) ↦
      ((restrict₀ v : MonoidWithZeroHom.{u_1, u_2} K (ValueGroup₀ (F := Valuation K Γ₀) v)) : (a : K) → ValueGroup₀ v)
          a_1 =
        a)
      ⋯) =
  a :=
  ⋯
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 =
      b)
    ⋯
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 =
        b)
      ⋯
hy : 0 = b
ha0 : a = 0
h0 : Eq (α := ValueGroup₀ (F := Valuation K Γ₀) v) (extension ((algebraMap K (hat K) : (a : K) → hat K) x)) 0
this : y = 0
pos : 0 = b
⊢ a = b
have pos₁ : b = b
Tactic: rw [ha0, 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 Γ₀
x : ValueGroup₀ (F := Valuation.{u_1, u_2} (hat K) Γ₀) extensionValuation
⊢ ∃ (a : ValueGroup₀ (F := Valuation K Γ₀) v),
    (valueGroup₀_hom_extensionValuation : (a : ValueGroup₀ v) → ValueGroup₀ extensionValuation) a = x
have refine_2 : ∀ (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),
  ∃ (a : ValueGroup₀ (F := Valuation K Γ₀) v),
    (valueGroup₀_hom_extensionValuation : (a : ValueGroup₀ v) → ValueGroup₀ extensionValuation) a = x
Tactic: obtain ⟨k', hk'⟩ := restrict₀_surjective extensionValuation x
-- 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 : 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
⊢ ∃ (a : ValueGroup₀ (F := Valuation K Γ₀) v),
    (valueGroup₀_hom_extensionValuation : (a : ValueGroup₀ v) → ValueGroup₀ extensionValuation) a = x
have refine_2 : ∀ (k : K)
  (hk :
    ((restrict₀ v : MonoidWithZeroHom.{u_1, u_2} K (ValueGroup₀ (F := Valuation K Γ₀) v)) : (a : K) → ValueGroup₀ v) k =
      extension k'),
  ∃ (a : ValueGroup₀ (F := Valuation K Γ₀) v),
    (valueGroup₀_hom_extensionValuation : (a : ValueGroup₀ v) → ValueGroup₀ extensionValuation) a = x
Tactic: obtain ⟨k, hk⟩ := restrict₀_surjective Valued.v (extension k')
-- 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 : 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'
⊢ ∃ (a : ValueGroup₀ (F := Valuation K Γ₀) v),
    (valueGroup₀_hom_extensionValuation : (a : ValueGroup₀ v) → ValueGroup₀ extensionValuation) a = x
have h : (valueGroup₀_hom_extensionValuation : (a : ValueGroup₀ v) → ValueGroup₀ extensionValuation) (extension k') = x
Tactic: use extension k'
-- 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 : 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'
⊢ ((restrict₀ extensionValuation :
          MonoidWithZeroHom.{u_1, u_2} (hat K)
            (ValueGroup₀ (F := Valuation.{u_1, u_2} (hat K) Γ₀) extensionValuation)) :
        (a : hat K) → ValueGroup₀ extensionValuation)
      (↑(⋯.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) =
    x
have h : Eq (α := Γ₀)
  ((embedding : (a : ValueGroup₀ extensionValuation.toMonoidWithZeroHom) → Γ₀)
      (((restrict₀ extensionValuation :
              MonoidWithZeroHom.{u_1, u_2} (hat K)
                (ValueGroup₀ (F := Valuation.{u_1, u_2} (hat K) Γ₀) extensionValuation)) :
            (a : hat K) → ValueGroup₀ extensionValuation)
          (↑(sorry.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) :
        ValueGroup₀ (F := Valuation.{u_1, u_2} (hat K) Γ₀) extensionValuation) :
    Γ₀)
  ((embedding : (a : ValueGroup₀ extensionValuation.toMonoidWithZeroHom) → Γ₀)
      (((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' :
        ValueGroup₀ (F := Valuation.{u_1, u_2} (hat K) Γ₀) extensionValuation) :
    Γ₀)
Tactic: rw [← hk', ← embedding_strictMono.injective.eq_iff]
-- 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 : 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'
⊢ Eq (α := Γ₀)
    ((embedding : (a : ValueGroup₀ extensionValuation.toMonoidWithZeroHom) → Γ₀)
        (((restrict₀ extensionValuation :
                MonoidWithZeroHom.{u_1, u_2} (hat K)
                  (ValueGroup₀ (F := Valuation.{u_1, u_2} (hat K) Γ₀) extensionValuation)) :
              (a : hat K) → ValueGroup₀ extensionValuation)
            (↑(⋯.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) :
          ValueGroup₀ (F := Valuation.{u_1, u_2} (hat K) Γ₀) extensionValuation) :
      Γ₀)
    ((embedding : (a : ValueGroup₀ extensionValuation.toMonoidWithZeroHom) → Γ₀)
        (((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' :
          ValueGroup₀ (F := Valuation.{u_1, u_2} (hat K) Γ₀) extensionValuation) :
      Γ₀)
have h : Eq.{u_2 + 1} (α := Γ₀)
  ((Valuation.toMonoidWithZeroHom extensionValuation : (a : hat K) → Γ₀)
      (↑(sorry.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: erw [embedding_restrict₀, embedding_restrict₀]
-- 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 : 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'
⊢ 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' : Γ₀)
have h : Eq (α := Γ₀)
  ((embedding : (a : ValueGroup₀ v) → Γ₀)
      ((Valuation.restrict v : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀))
          (sorry.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: simp only [Valuation.toMonoidWithZeroHom_coe_eq_coe,
      extensionValuation_toFun, extension_extends]
-- 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 : 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'
⊢ 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') : Γ₀)
have h : (Valuation.restrict v : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀))
    (sorry.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: rw [embedding_strictMono.injective.eq_iff]
-- 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)ˣ) → Γ₀ˣ) γ) : Γ₀) : Γ₀)}
⊢ 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
have 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
Tactic: rw [this.mem_iff]
-- 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)ˣ) → Γ₀ˣ) γ) : Γ₀) : Γ₀)}
⊢ (∃ (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
have 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
Tactic: simp only [extensionValuation_toFun, Units.coe_map, MonoidHom.coe_coe, true_and]
-- 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)ˣ
⊢ 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) : Γ₀)
have 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) sorry) :
          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: rw [embedding_strictMono.lt_iff_lt, Valuation.restrict_def, restrict₀_apply]