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 Γ₀
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:
have h0 : xy = 0 := by
          simp [← v.restrict.zero_iff, v.restrict_def, hxy, ← hy, hy0]
-- 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
neg :
  Units.mk0 ((v : (a : K) → Γ₀) xy) ⋯ =
    Units.mk0 (HMul.hMul (α := Γ₀) (β := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) ((v : (a : K) → Γ₀) y : Γ₀)) ⋯
neg₁ : HMul.hMul (α := Γ₀) (β := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) ((v : (a : K) → Γ₀) y : Γ₀) ≠ 0
⊢ Units.mk0 ((v : (a : K) → Γ₀) xy) ⋯ =
    HMul.hMul (α := Γ₀ˣ) (β := Γ₀ˣ) (Units.mk0 ((v : (a : K) → Γ₀) x) ⋯ : Γ₀ˣ)
      (Units.mk0 ((v : (a : K) → Γ₀) y) ⋯ : Γ₀ˣ)

Tactic:
rw [← Units.mk0_mul]

Premises used: Units.mk0_mul
-- 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
neg :
  (↑(Units.mk0 ((v : (a : K) → Γ₀) xy) ⋯) : Γ₀) =
    (↑(Units.mk0 (HMul.hMul (α := Γ₀) (β := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) ((v : (a : K) → Γ₀) y : Γ₀)) ⋯) : Γ₀)
⊢ Units.mk0 ((v : (a : K) → Γ₀) xy) ⋯ =
    Units.mk0 (HMul.hMul (α := Γ₀) (β := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) ((v : (a : K) → Γ₀) y : Γ₀)) ⋯

Tactic:
ext
-- 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
neg :
  (v : (a : K) → Γ₀) xy =
    (↑(Units.mk0 (HMul.hMul (α := Γ₀) (β := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) ((v : (a : K) → Γ₀) y : Γ₀)) ⋯) : Γ₀)
⊢ (↑(Units.mk0 ((v : (a : K) → Γ₀) xy) ⋯) : Γ₀) =
    (↑(Units.mk0 (HMul.hMul (α := Γ₀) (β := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) ((v : (a : K) → Γ₀) y : Γ₀)) ⋯) : Γ₀)

Tactic:
simp only [Units.val_mk0]

Premises used: Units.val_mk0
-- 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
neg :
  (Valuation.restrict v : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀)) xy =
    HMul.hMul (α := ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀)) (β := ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀))
      ((Valuation.restrict v : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀)) x : ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀))
      ((Valuation.restrict v : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀)) y : ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀))
⊢ (v : (a : K) → Γ₀) xy =
    (↑(Units.mk0 (HMul.hMul (α := Γ₀) (β := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) ((v : (a : K) → Γ₀) y : Γ₀)) ⋯) : Γ₀)

Tactic:
rw [Units.val_mk0, ← map_mul, ← v.restrict_inj, map_mul]

Premises used: Valued.v, Valuation.restrict_inj, map_mul, Units.val_mk0
-- 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
⊢ (Valuation.restrict v : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀)) xy =
    HMul.hMul (α := ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀)) (β := ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀))
      ((Valuation.restrict v : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀)) x : ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀))
      ((Valuation.restrict v : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀)) y : ValueGroup₀ (F := K →*₀ Γ₀) (↑v : K →*₀ Γ₀))

Tactic:
simp [v.restrict_def, hx, hy, hxy]

Premises used: Valued.v, 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 Γ₀
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
⊢ HMul.hMul (α := Γ₀) (β := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) ((v : (a : K) → Γ₀) y : Γ₀) ≠ 0

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

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

Tactic:
simp [hy0]
-- 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
neg :
  ¬HMul.hMul (α := ValueGroup₀ (F := Valuation K Γ₀) v) (β := ValueGroup₀ (F := Valuation K Γ₀) v)
        (((restrict₀ v : MonoidWithZeroHom.{u_1, u_2} K (ValueGroup₀ (F := Valuation K Γ₀) v)) :
              (a : K) → ValueGroup₀ v)
            x :
          ValueGroup₀ (F := Valuation K Γ₀) v)
        (((restrict₀ v : MonoidWithZeroHom.{u_1, u_2} K (ValueGroup₀ (F := Valuation K Γ₀) v)) :
              (a : K) → ValueGroup₀ v)
            y :
          ValueGroup₀ (F := Valuation K Γ₀) v) =
      0
⊢ ¬Eq.{u_2 + 1} (α := Γ₀) ((extensionValuation : (a : hat K) → Γ₀) (↑xy : hat K) : Γ₀) (0 : Γ₀)

Tactic:
rw [extensionValuation_apply_coe, ← restrict₀_eq_zero_iff, hxy, ← hx, ← hy]

Premises used: MonoidWithZeroHom.ValueGroup₀.restrict₀_eq_zero_iff, Valued.extensionValuation_apply_coe
-- 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
⊢ ¬HMul.hMul (α := ValueGroup₀ (F := Valuation K Γ₀) v) (β := ValueGroup₀ (F := Valuation K Γ₀) v)
        (((restrict₀ v : MonoidWithZeroHom.{u_1, u_2} K (ValueGroup₀ (F := Valuation K Γ₀) v)) :
              (a : K) → ValueGroup₀ v)
            x :
          ValueGroup₀ (F := Valuation K Γ₀) v)
        (((restrict₀ v : MonoidWithZeroHom.{u_1, u_2} K (ValueGroup₀ (F := Valuation K Γ₀) v)) :
              (a : K) → ValueGroup₀ v)
            y :
          ValueGroup₀ (F := Valuation K Γ₀) v) =
      0

Tactic:
simp [hx0, hy0]