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 Γ₀
refine_1 :
  Function.Injective (α := ValueGroup₀ (F := Valuation K Γ₀) v) (β :=
    ValueGroup₀ (F := Valuation.{u_1, u_2} (hat K) Γ₀) extensionValuation)
    (⇑valueGroup₀_hom_extensionValuation : (a : ValueGroup₀ v) → ValueGroup₀ extensionValuation)
refine_2 :
  Function.Surjective (α := ValueGroup₀ (F := Valuation K Γ₀) v) (β :=
    ValueGroup₀ (F := Valuation.{u_1, u_2} (hat K) Γ₀) extensionValuation)
    (⇑valueGroup₀_hom_extensionValuation : (a : ValueGroup₀ v) → ValueGroup₀ extensionValuation)
⊢ ValueGroup₀ (F := Valuation K Γ₀) v ≃* ValueGroup₀ (F := Valuation.{u_1, u_2} (hat K) Γ₀) extensionValuation

Tactic:
refine MulEquiv.ofBijective (valueGroup₀_hom_extensionValuation (hv := hv)) ⟨?_, ?_⟩

Premises used: And.intro, MulEquiv.ofBijective, Valued.valueGroup₀_hom_extensionValuation
-- Module: Mathlib.Topology.Algebra.Valued.ValuedField
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 (α := ValueGroup₀ (F := Valuation.{u_1, u_2} (hat K) Γ₀) extensionValuation)
    ((valueGroup₀_hom_extensionValuation : (a : ValueGroup₀ v) → ValueGroup₀ extensionValuation) a :
      ValueGroup₀ (F := Valuation.{u_1, u_2} (hat K) Γ₀) extensionValuation)
    ((valueGroup₀_hom_extensionValuation : (a : ValueGroup₀ v) → ValueGroup₀ extensionValuation) b :
      ValueGroup₀ (F := Valuation.{u_1, u_2} (hat K) Γ₀) extensionValuation)
⊢ let 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)
      ⋯;
  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)
      ⋯

Tactic:
set x := (restrict₀_surjective hv.v a).choose with hx_def

Premises used: Valued.v, MonoidWithZeroHom.ValueGroup₀.restrict₀_surjective, Exists.choose
-- Module: Mathlib.Topology.Algebra.Valued.ValuedField
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 (α := ValueGroup₀ (F := Valuation.{u_1, u_2} (hat K) Γ₀) extensionValuation)
    ((valueGroup₀_hom_extensionValuation : (a : ValueGroup₀ v) → ValueGroup₀ extensionValuation) a :
      ValueGroup₀ (F := Valuation.{u_1, u_2} (hat K) Γ₀) extensionValuation)
    ((valueGroup₀_hom_extensionValuation : (a : ValueGroup₀ v) → ValueGroup₀ extensionValuation) b :
      ValueGroup₀ (F := Valuation.{u_1, u_2} (hat K) Γ₀) extensionValuation)
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 :=
  ⋯
⊢ let 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)
      ⋯;
  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)
      ⋯

Tactic:
set y := (restrict₀_surjective hv.v b).choose with hy_def

Premises used: Valued.v, MonoidWithZeroHom.ValueGroup₀.restrict₀_surjective, Exists.choose
-- Module: Mathlib.Topology.Algebra.Valued.ValuedField
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
pos₁ pos₂ : b = b
⊢ a = b

Tactic:
rw [ha0, hy]
-- Module: Mathlib.Topology.Algebra.Valued.ValuedField
Goal:
K : Type u_1
inst : Field K
Γ₀ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
a b : ValueGroup₀ (F := Valuation K Γ₀) v
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)
    ⋯
hab : 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 :=
  ⋯
this :
  Eq.{u_2 + 1} (α := ValueGroup₀ (F := MonoidWithZeroHom.{u_1, u_2} (hat K) Γ₀) (↑extensionValuation : hat K →*₀ Γ₀))
    (if h :
        Eq (α := ValueGroup₀ (F := Valuation K Γ₀) v) (extension ((algebraMap K (hat K) : (a : K) → 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 ((embedding : (a : ValueGroup₀ v) → Γ₀) (extension ((algebraMap K (hat K) : (a : K) → hat K) x)))
              ⋯)
            ⋯) :
        WithZero ↥(valueGroup extensionValuation)))
    (if h :
        Eq (α := ValueGroup₀ (F := Valuation K Γ₀) v) (extension ((algebraMap K (hat K) : (a : K) → hat K) y)) 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 ((embedding : (a : ValueGroup₀ v) → Γ₀) (extension ((algebraMap K (hat K) : (a : K) → hat K) y)))
              ⋯)
            ⋯) :
        WithZero ↥(valueGroup extensionValuation)))
ha0 : ¬a = 0
h0 : Ne (α := ValueGroup₀ (F := Valuation K Γ₀) v) (extension ((algebraMap K (hat K) : (a : K) → hat K) x)) 0
⊢ b ≠ 0

Tactic:
simpa [hab] using ha0
-- Module: Mathlib.Topology.Algebra.Valued.ValuedField
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 : Ne (α := ValueGroup₀ (F := Valuation K Γ₀) v) (extension ((algebraMap K (hat K) : (a : K) → hat K) x)) 0
h0' : Ne (α := ValueGroup₀ (F := Valuation K Γ₀) v) (extension ((algebraMap K (hat K) : (a : K) → hat K) y)) 0
this : a = b
⊢ a = b

Tactic:
this
-- Module: Mathlib.Topology.Algebra.Valued.ValuedField
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 : Ne (α := ValueGroup₀ (F := Valuation K Γ₀) v) (extension ((algebraMap K (hat K) : (a : K) → hat K) x)) 0
h0' : Ne (α := ValueGroup₀ (F := Valuation K Γ₀) v) (extension ((algebraMap K (hat K) : (a : K) → hat K) y)) 0
this : a = b
⊢ a = b

Tactic:
exact this
-- 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
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
⊢ ∃ (a : ValueGroup₀ (F := Valuation K Γ₀) v),
    (valueGroup₀_hom_extensionValuation : (a : ValueGroup₀ v) → ValueGroup₀ extensionValuation) a = x

Tactic:
obtain ⟨k', hk'⟩ := restrict₀_surjective extensionValuation x

Premises used: MonoidWithZeroHom.ValueGroup₀.restrict₀_surjective, Valued.extensionValuation
-- 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
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
⊢ ∃ (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')

Premises used: Valued.v, MonoidWithZeroHom.ValueGroup₀.restrict₀_surjective, Valued.extension
-- 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 : (valueGroup₀_hom_extensionValuation : (a : ValueGroup₀ v) → ValueGroup₀ extensionValuation) (extension k') = x
⊢ ∃ (a : ValueGroup₀ (F := Valuation K Γ₀) v),
    (valueGroup₀_hom_extensionValuation : (a : ValueGroup₀ v) → ValueGroup₀ extensionValuation) a = x

Tactic:
use extension k'

Premises used: Valued.extension
-- 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₀ 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) :
      Γ₀)
⊢ ((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

Tactic:
rw [← hk', ← 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'
h :
  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' : Γ₀)
⊢ 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) :
      Γ₀)

Tactic:
erw [embedding_restrict₀, embedding_restrict₀]

Premises used: MonoidWithZeroHom.ValueGroup₀.embedding_restrict₀