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 : hat K
γ₀' : ValueGroup₀ (F := Valuation K Γ₀) v := extension x
hγ₀'_def : γ₀' = extension x
γ₀ : Γ₀ := (extensionValuation : (a : hat K) → Γ₀) x
hγ₀_def : γ₀ = (extensionValuation : (a : hat K) → Γ₀) x
heq : γ₀ = (embedding : (a : ValueGroup₀ v) → Γ₀) γ₀'
h : γ₀ ≠ 0
h' : γ₀' ≠ 0
hγ₀ : extension ⁻¹' {γ₀'} ∈ 𝓝 x
s : Set (hat K)
hs : s ∈ 𝓝 x
y : K
hx : (v : (a : K) → Γ₀) y < (↑γ : Γ₀)
hy₂ : (↑y : hat K) ∈ s
hy₁ : (v : (a : K) → Γ₀) y = γ₀
⊢ ∃ (y : (↑(Completion.coe' '' {x : K | (v : (a : K) → Γ₀) x < (↑γ : Γ₀)}) : Type u_1)), (↑y : hat K) ∈ s

Tactic:
exact ⟨⟨y, ⟨y, hx, rfl⟩⟩, hy₂⟩
-- Module: Mathlib.Topology.Algebra.Valued.ValuedField
Goal:
K : Type u_1
inst : Field K
Γ₀ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
r s : K
hr : r ≠ 0
hs : s ≠ 0
⊢ HDiv.hDiv (α := Γ₀) (β := Γ₀) ((v : (a : K) → Γ₀) s : Γ₀) ((v : (a : K) → Γ₀) r : Γ₀) ≠ 0

Tactic:
simp [hr, hs]
-- Module: Mathlib.Topology.Algebra.Valued.ValuedField
Goal:
K : Type u_1
inst : Field K
Γ₀ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
r s : K
hr : r ≠ 0
hs : s ≠ 0
⊢ HDiv.hDiv (α := Γ₀) (β := Γ₀) ((v : (a : K) → Γ₀) s : Γ₀) ((v : (a : K) → Γ₀) r : Γ₀) ≠ 0

Tactic:
have hrs : v s / v r ≠ 0 := by simp [hr, hs]
-- Module: Mathlib.Topology.Algebra.Valued.ValuedField
Goal:
K : Type u_1
inst : Field K
Γ₀ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
r s : K
hr : r ≠ 0
hs : s ≠ 0
hrs : HDiv.hDiv (α := Γ₀) (β := Γ₀) ((v : (a : K) → Γ₀) s : Γ₀) ((v : (a : K) → Γ₀) r : Γ₀) ≠ 0
⊢ Eq.{u_1 + 1} (α := Set (hat K))
    (closure
      (Completion.coe' ''
        {x : K |
          (v : (a : K) → Γ₀) x <
            (↑(Units.mk0 (HDiv.hDiv (α := Γ₀) (β := Γ₀) ((v : (a : K) → Γ₀) s : Γ₀) ((v : (a : K) → Γ₀) r : Γ₀)) hrs) :
              Γ₀)}))
    {x : hat K |
      (extensionValuation : (a : hat K) → Γ₀) x <
        (↑(Units.mk0 (HDiv.hDiv (α := Γ₀) (β := Γ₀) ((v : (a : K) → Γ₀) s : Γ₀) ((v : (a : K) → Γ₀) r : Γ₀)) hrs) : Γ₀)}

Tactic:
closure_coe_completion_v_lt (γ := .mk0 _ hrs)

Premises used: 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 Γ₀
r s : K
hr : r ≠ 0
hs : s ≠ 0
hrs : HDiv.hDiv (α := Γ₀) (β := Γ₀) ((v : (a : K) → Γ₀) s : Γ₀) ((v : (a : K) → Γ₀) r : Γ₀) ≠ 0
h :
  Eq.{u_1 + 1} (α := Set K)
    {x : K |
      HMul.hMul (α := Γ₀) (β := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) ((v : (a : K) → Γ₀) r : Γ₀) < (v : (a : K) → Γ₀) s}
    {x : K |
      (v : (a : K) → Γ₀) x <
        (↑(Units.mk0 (HDiv.hDiv (α := Γ₀) (β := Γ₀) ((v : (a : K) → Γ₀) s : Γ₀) ((v : (a : K) → Γ₀) r : Γ₀)) hrs) : Γ₀)}
h₁ :
  ∀ (x : hat K),
    HMul.hMul (α := Γ₀) (β := Γ₀) ((extensionValuation : (a : hat K) → Γ₀) x : Γ₀) ((v : (a : K) → Γ₀) r : Γ₀) <
        (v : (a : K) → Γ₀) s ↔
      (extensionValuation : (a : hat K) → Γ₀) x <
        (↑(Units.mk0 (HDiv.hDiv (α := Γ₀) (β := Γ₀) ((v : (a : K) → Γ₀) s : Γ₀) ((v : (a : K) → Γ₀) r : Γ₀)) hrs) : Γ₀)
⊢ Eq.{u_1 + 1} (α := Set (hat K))
    (closure
      (Completion.coe' ''
        {x : K |
          HMul.hMul (α := Γ₀) (β := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) ((v : (a : K) → Γ₀) r : Γ₀) <
            (v : (a : K) → Γ₀) s}))
    {x : hat K |
      HMul.hMul (α := Γ₀) (β := Γ₀) ((extensionValuation : (a : hat K) → Γ₀) x : Γ₀) ((v : (a : K) → Γ₀) r : Γ₀) <
        (v : (a : K) → Γ₀) s}

Tactic:
convert! closure_coe_completion_v_lt (γ := .mk0 _ hrs) using 3

Premises used: 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 Γ₀
r s : K
hr : r ≠ 0
hs : s ≠ 0
hrs : HDiv.hDiv (α := Γ₀) (β := Γ₀) ((v : (a : K) → Γ₀) s : Γ₀) ((v : (a : K) → Γ₀) r : Γ₀) ≠ 0
⊢ Eq.{u_1 + 1} (α := Set K)
    {x : K |
      HMul.hMul (α := Γ₀) (β := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) ((v : (a : K) → Γ₀) r : Γ₀) < (v : (a : K) → Γ₀) s}
    {x : K |
      (v : (a : K) → Γ₀) x <
        (↑(Units.mk0 (HDiv.hDiv (α := Γ₀) (β := Γ₀) ((v : (a : K) → Γ₀) s : Γ₀) ((v : (a : K) → Γ₀) r : Γ₀)) hrs) : Γ₀)}

Tactic:
simp [← lt_div_iff₀, zero_lt_iff, hr]

Premises used: lt_div_iff₀, zero_lt_iff
-- Module: Mathlib.Topology.Algebra.Valued.ValuedField
Goal:
K : Type u_1
inst : Field K
Γ₀ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
r s : K
hr : r ≠ 0
hs : s ≠ 0
hrs : HDiv.hDiv (α := Γ₀) (β := Γ₀) ((v : (a : K) → Γ₀) s : Γ₀) ((v : (a : K) → Γ₀) r : Γ₀) ≠ 0
x : hat K
⊢ HMul.hMul (α := Γ₀) (β := Γ₀) ((extensionValuation : (a : hat K) → Γ₀) x : Γ₀) ((v : (a : K) → Γ₀) r : Γ₀) <
      (v : (a : K) → Γ₀) s ↔
    (extensionValuation : (a : hat K) → Γ₀) x <
      (↑(Units.mk0 (HDiv.hDiv (α := Γ₀) (β := Γ₀) ((v : (a : K) → Γ₀) s : Γ₀) ((v : (a : K) → Γ₀) r : Γ₀)) hrs) : Γ₀)

Tactic:
simp [← lt_div_iff₀, zero_lt_iff, hr]

Premises used: lt_div_iff₀, zero_lt_iff
-- Module: Mathlib.Topology.Algebra.Valued.ValuedField
Goal:
K : Type u_1
inst : Field K
Γ₀ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
⊢ Eq.{u_2 + 1} (α := ValueGroup₀ (F := Valuation.{u_1, u_2} (hat K) Γ₀) extensionValuation)
    ((Valuation.restrict extensionValuation : (a : hat K) → ValueGroup₀ (↑extensionValuation : hat K →*₀ Γ₀))
        (↑(Exists.choose (p := fun (a : K) ↦
              Eq.{u_2 + 1} (α := ValueGroup₀ (F := Valuation K Γ₀) v)
                (((restrict₀ v : MonoidWithZeroHom.{u_1, u_2} K (ValueGroup₀ (F := Valuation K Γ₀) v)) :
                      (a : K) → ValueGroup₀ v)
                    a :
                  ValueGroup₀ (F := Valuation K Γ₀) v)
                (0 : ValueGroup₀ (F := Valuation K Γ₀) v))
              ⋯) :
          hat K) :
      ValueGroup₀ (F := MonoidWithZeroHom.{u_1, u_2} (hat K) Γ₀) (↑extensionValuation : hat K →*₀ Γ₀))
    (0 : ValueGroup₀ (F := Valuation.{u_1, u_2} (hat K) Γ₀) extensionValuation)

Tactic:
simp [Valuation.restrict_def]

Premises used: Valuation.restrict_def
-- Module: Mathlib.Topology.Algebra.Valued.ValuedField
Goal:
K : Type u_1
inst : Field K
Γ₀ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
rw :
  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)
            (↑(Exists.choose (p := fun (a : K) ↦
                  Eq.{u_2 + 1} (α := ValueGroup₀ (F := Valuation K Γ₀) v)
                    (((restrict₀ v : MonoidWithZeroHom.{u_1, u_2} K (ValueGroup₀ (F := Valuation K Γ₀) v)) :
                          (a : K) → ValueGroup₀ v)
                        a :
                      ValueGroup₀ (F := Valuation K Γ₀) v)
                    (1 : ValueGroup₀ (F := Valuation K Γ₀) v))
                  ⋯) :
              hat K) :
          ValueGroup₀ (F := Valuation.{u_1, u_2} (hat K) Γ₀) extensionValuation) :
      Γ₀)
    (1 : Γ₀)
⊢ Eq.{u_2 + 1} (α := ValueGroup₀ (F := Valuation.{u_1, u_2} (hat K) Γ₀) extensionValuation)
    ((Valuation.restrict extensionValuation : (a : hat K) → ValueGroup₀ (↑extensionValuation : hat K →*₀ Γ₀))
        (↑(Exists.choose (p := fun (a : K) ↦
              Eq.{u_2 + 1} (α := ValueGroup₀ (F := Valuation K Γ₀) v)
                (((restrict₀ v : MonoidWithZeroHom.{u_1, u_2} K (ValueGroup₀ (F := Valuation K Γ₀) v)) :
                      (a : K) → ValueGroup₀ v)
                    a :
                  ValueGroup₀ (F := Valuation K Γ₀) v)
                (1 : ValueGroup₀ (F := Valuation K Γ₀) v))
              ⋯) :
          hat K) :
      ValueGroup₀ (F := MonoidWithZeroHom.{u_1, u_2} (hat K) Γ₀) (↑extensionValuation : hat K →*₀ Γ₀))
    (1 : ValueGroup₀ (F := Valuation.{u_1, u_2} (hat K) Γ₀) extensionValuation)

Tactic:
rw [← embedding_strictMono.injective.eq_iff, Valuation.restrict_def, map_one]

Premises used: Function.Injective.eq_iff, Valuation.restrict_def, StrictMono.injective, map_one
-- Module: Mathlib.Topology.Algebra.Valued.ValuedField
Goal:
K : Type u_1
inst : Field K
Γ₀ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
erw :
  Eq.{u_2 + 1} (α := Γ₀)
    ((Valuation.toMonoidWithZeroHom extensionValuation : (a : hat K) → Γ₀)
        (↑(Exists.choose (p := fun (a : K) ↦
              Eq.{u_2 + 1} (α := ValueGroup₀ (F := Valuation K Γ₀) v)
                (((restrict₀ v : MonoidWithZeroHom.{u_1, u_2} K (ValueGroup₀ (F := Valuation K Γ₀) v)) :
                      (a : K) → ValueGroup₀ v)
                    a :
                  ValueGroup₀ (F := Valuation K Γ₀) v)
                (1 : ValueGroup₀ (F := Valuation K Γ₀) v))
              ⋯) :
          hat K) :
      Γ₀)
    (1 : Γ₀)
⊢ 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)
            (↑(Exists.choose (p := fun (a : K) ↦
                  Eq.{u_2 + 1} (α := ValueGroup₀ (F := Valuation K Γ₀) v)
                    (((restrict₀ v : MonoidWithZeroHom.{u_1, u_2} K (ValueGroup₀ (F := Valuation K Γ₀) v)) :
                          (a : K) → ValueGroup₀ v)
                        a :
                      ValueGroup₀ (F := Valuation K Γ₀) v)
                    (1 : ValueGroup₀ (F := Valuation K Γ₀) v))
                  ⋯) :
              hat K) :
          ValueGroup₀ (F := Valuation.{u_1, u_2} (hat K) Γ₀) extensionValuation) :
      Γ₀)
    (1 : Γ₀)

Tactic:
erw [embedding_restrict₀]

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

Tactic:
simp only [Valuation.toMonoidWithZeroHom_coe_eq_coe,
      extensionValuation_toFun, extension_extends, ← map_one (embedding (f := hv.v))]

Premises used: Valued.extension_extends, map_one, Valuation.toMonoidWithZeroHom_coe_eq_coe, MonoidWithZeroHom.ValueGroup₀.embedding, 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 Γ₀
rw :
  Eq.{u_2 + 1} (α := ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀))
    ((Valuation.restrict v : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀))
        (Exists.choose (p := fun (a : K) ↦
          Eq.{u_2 + 1} (α := ValueGroup₀ (F := Valuation K Γ₀) v)
            (((restrict₀ v : MonoidWithZeroHom.{u_1, u_2} K (ValueGroup₀ (F := Valuation K Γ₀) v)) :
                  (a : K) → ValueGroup₀ v)
                a :
              ValueGroup₀ (F := Valuation K Γ₀) v)
            (1 : ValueGroup₀ (F := Valuation K Γ₀) v))
          ⋯) :
      ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀))
    (1 : ValueGroup₀ (F := Valuation K Γ₀) v)
⊢ Eq (α := Γ₀)
    ((embedding : (a : ValueGroup₀ v) → Γ₀)
        ((Valuation.restrict v : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀))
            (Exists.choose (p := fun (a : K) ↦
              Eq.{u_2 + 1} (α := ValueGroup₀ (F := Valuation K Γ₀) v)
                (((restrict₀ v : MonoidWithZeroHom.{u_1, u_2} K (ValueGroup₀ (F := Valuation K Γ₀) v)) :
                      (a : K) → ValueGroup₀ v)
                    a :
                  ValueGroup₀ (F := Valuation K Γ₀) v)
                (1 : ValueGroup₀ (F := Valuation K Γ₀) v))
              ⋯) :
          ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀)) :
      Γ₀)
    ((embedding : (a : ValueGroup₀ v) → Γ₀) 1 : Γ₀)

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 Γ₀
⊢ Eq.{u_2 + 1} (α := ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀))
    ((Valuation.restrict v : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀))
        (Exists.choose (p := fun (a : K) ↦
          Eq.{u_2 + 1} (α := ValueGroup₀ (F := Valuation K Γ₀) v)
            (((restrict₀ v : MonoidWithZeroHom.{u_1, u_2} K (ValueGroup₀ (F := Valuation K Γ₀) v)) :
                  (a : K) → ValueGroup₀ v)
                a :
              ValueGroup₀ (F := Valuation K Γ₀) v)
            (1 : ValueGroup₀ (F := Valuation K Γ₀) v))
          ⋯) :
      ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀))
    (1 : ValueGroup₀ (F := Valuation K Γ₀) v)

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

Premises used: Exists.choose_spec, Set.Mem, Valued.v, setOf, MonoidWithZeroHom.ValueGroup₀.restrict₀_surjective, OfNat.ofNat
-- Module: Mathlib.Topology.Algebra.Valued.ValuedField
Goal:
K : Type u_1
inst : Field K
Γ₀ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
⊢ Eq.{u_2 + 1} (α := ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀))
    ((Valuation.restrict v : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀))
        (Exists.choose (p := fun (a : K) ↦
          Eq.{u_2 + 1} (α := ValueGroup₀ (F := Valuation K Γ₀) v)
            (((restrict₀ v : MonoidWithZeroHom.{u_1, u_2} K (ValueGroup₀ (F := Valuation K Γ₀) v)) :
                  (a : K) → ValueGroup₀ v)
                a :
              ValueGroup₀ (F := Valuation K Γ₀) v)
            (1 : ValueGroup₀ (F := Valuation K Γ₀) v))
          ⋯) :
      ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀))
    (1 : ValueGroup₀ (F := Valuation K Γ₀) v)

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

Premises used: Exists.choose_spec, Valued.v, MonoidWithZeroHom.ValueGroup₀.restrict₀_surjective, OfNat.ofNat
-- 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) x = 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) y = b
xy : 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 * b)
    ⋯
hxy_def :
  xy =
    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 * b)
      ⋯
hxy : ((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 * b)
      ⋯) =
  a * b :=
  ⋯
⊢ ((restrict₀ v : MonoidWithZeroHom.{u_1, u_2} K (ValueGroup₀ (F := Valuation K Γ₀) v)) : (a : K) → ValueGroup₀ v) xy =
    a * b

Tactic:
rw [← hxy_def] at hxy
-- 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) x = 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) y = b
xy : 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 * b)
    ⋯
hxy_def :
  xy =
    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 * b)
      ⋯
hxy :
  ((restrict₀ v : MonoidWithZeroHom.{u_1, u_2} K (ValueGroup₀ (F := Valuation K Γ₀) v)) : (a : K) → ValueGroup₀ v) xy =
    a * b
hx0 : x = 0
⊢ xy = 0

Tactic:
simp [← v.restrict.zero_iff, v.restrict_def, hxy, ← hx, hx0]

Premises used: Valued.v, Valuation.zero_iff, Valuation.restrict_def, 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 Γ₀
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) x = 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) y = b
xy : 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 * b)
    ⋯
hxy_def :
  xy =
    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 * b)
      ⋯
hxy :
  ((restrict₀ v : MonoidWithZeroHom.{u_1, u_2} K (ValueGroup₀ (F := Valuation K Γ₀) v)) : (a : K) → ValueGroup₀ v) xy =
    a * b
hx0 : x = 0
⊢ xy = 0

Tactic:
have h0 : xy = 0 := by
        simp [← v.restrict.zero_iff, v.restrict_def, hxy, ← hx, hx0]
-- 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) x = 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) y = b
xy : 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 * b)
    ⋯
hxy_def :
  xy =
    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 * b)
      ⋯
hxy :
  ((restrict₀ v : MonoidWithZeroHom.{u_1, u_2} K (ValueGroup₀ (F := Valuation K Γ₀) v)) : (a : K) → ValueGroup₀ v) xy =
    a * b
hx0 : ¬x = 0
hy0 : y = 0
⊢ xy = 0

Tactic:
simp [← v.restrict.zero_iff, v.restrict_def, hxy, ← hy, hy0]

Premises used: Valued.v, Valuation.zero_iff, Valuation.restrict_def, Valuation.restrict