awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Algebra.Valued.ValuedField
Goal:
K : Type u_1
inst : DivisionRing K
Γ₀ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation K Γ₀
x y : K
γ : Γ₀ˣ
y_ne : y ≠ 0
h_1 :
  (v : (a : K) → Γ₀) (x - y) <
    min ((↑γ : Γ₀) * HMul.hMul (α := Γ₀) (β := Γ₀) ((v : (a : K) → Γ₀) y : Γ₀) ((v : (a : K) → Γ₀) y : Γ₀))
      ((v : (a : K) → Γ₀) y)
hyp1 :
  (v : (a : K) → Γ₀) (x - y) <
    (↑γ : Γ₀) * HMul.hMul (α := Γ₀) (β := Γ₀) ((v : (a : K) → Γ₀) y : Γ₀) ((v : (a : K) → Γ₀) y : Γ₀)
hyp1' :
  HMul.hMul (α := Γ₀) ((v : (a : K) → Γ₀) (x - y) : Γ₀)
      (HMul.hMul (α := Γ₀) (β := Γ₀) ((v : (a : K) → Γ₀) y : Γ₀) ((v : (a : K) → Γ₀) y : Γ₀))⁻¹ <
    (↑γ : Γ₀)
hyp2 : LT.lt.{u_2} (α := Γ₀) ((v : (a : K) → Γ₀) (x - y) : Γ₀) ((v : (a : K) → Γ₀) y : Γ₀)
key : Eq.{u_2 + 1} (α := Γ₀) (0 : Γ₀) ((v : (a : K) → Γ₀) y : Γ₀)
h : x = 0
⊢ y = 0

Tactic:
exact v.zero_iff.1 key.symm

Premises used: Valuation.zero_iff, Iff.mp, Eq.symm
-- Module: Mathlib.Topology.Algebra.Valued.ValuedField
Goal:
K : Type u_1
inst : DivisionRing K
Γ₀ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation K Γ₀
x y : K
γ : Γ₀ˣ
y_ne : y ≠ 0
h :
  (v : (a : K) → Γ₀) (x - y) <
    min ((↑γ : Γ₀) * HMul.hMul (α := Γ₀) (β := Γ₀) ((v : (a : K) → Γ₀) y : Γ₀) ((v : (a : K) → Γ₀) y : Γ₀))
      ((v : (a : K) → Γ₀) y)
hyp1 :
  (v : (a : K) → Γ₀) (x - y) <
    (↑γ : Γ₀) * HMul.hMul (α := Γ₀) (β := Γ₀) ((v : (a : K) → Γ₀) y : Γ₀) ((v : (a : K) → Γ₀) y : Γ₀)
hyp1' :
  HMul.hMul (α := Γ₀) ((v : (a : K) → Γ₀) (x - y) : Γ₀)
      (HMul.hMul (α := Γ₀) (β := Γ₀) ((v : (a : K) → Γ₀) y : Γ₀) ((v : (a : K) → Γ₀) y : Γ₀))⁻¹ <
    (↑γ : Γ₀)
hyp2 : LT.lt.{u_2} (α := Γ₀) ((v : (a : K) → Γ₀) (x - y) : Γ₀) ((v : (a : K) → Γ₀) y : Γ₀)
key : Eq.{u_2 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) ((v : (a : K) → Γ₀) y : Γ₀)
⊢ x ≠ 0

Tactic:
have x_ne : x ≠ 0 := by
    intro h
    apply y_ne
    rw [h, v.map_zero] at key
    exact v.zero_iff.1 key.symm
-- Module: Mathlib.Topology.Algebra.Valued.ValuedField
Goal:
K : Type u_1
inst : DivisionRing K
Γ₀ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation K Γ₀
x y : K
γ : Γ₀ˣ
y_ne : y ≠ 0
h :
  (v : (a : K) → Γ₀) (x - y) <
    min ((↑γ : Γ₀) * HMul.hMul (α := Γ₀) (β := Γ₀) ((v : (a : K) → Γ₀) y : Γ₀) ((v : (a : K) → Γ₀) y : Γ₀))
      ((v : (a : K) → Γ₀) y)
hyp1 :
  (v : (a : K) → Γ₀) (x - y) <
    (↑γ : Γ₀) * HMul.hMul (α := Γ₀) (β := Γ₀) ((v : (a : K) → Γ₀) y : Γ₀) ((v : (a : K) → Γ₀) y : Γ₀)
hyp1' :
  HMul.hMul (α := Γ₀) ((v : (a : K) → Γ₀) (x - y) : Γ₀)
      (HMul.hMul (α := Γ₀) (β := Γ₀) ((v : (a : K) → Γ₀) y : Γ₀) ((v : (a : K) → Γ₀) y : Γ₀))⁻¹ <
    (↑γ : Γ₀)
hyp2 : LT.lt.{u_2} (α := Γ₀) ((v : (a : K) → Γ₀) (x - y) : Γ₀) ((v : (a : K) → Γ₀) y : Γ₀)
key : Eq.{u_2 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) ((v : (a : K) → Γ₀) y : Γ₀)
x_ne : x ≠ 0
rw : x⁻¹ - y⁻¹ = (x⁻¹ * y - x⁻¹ * x) * y⁻¹
rw₁ : x⁻¹ - y⁻¹ = x⁻¹ * y * y⁻¹ - x⁻¹ * x * y⁻¹
rw₂ : x⁻¹ - y⁻¹ = x⁻¹ * (y * y⁻¹) - x⁻¹ * x * y⁻¹
rw₃ : x⁻¹ - y⁻¹ = x⁻¹ * 1 - x⁻¹ * x * y⁻¹
rw₄ : x⁻¹ - y⁻¹ = x⁻¹ * 1 - 1 * y⁻¹
rw₅ : x⁻¹ - y⁻¹ = x⁻¹ - 1 * y⁻¹
rw₆ rw₇ : x⁻¹ - y⁻¹ = x⁻¹ - y⁻¹
⊢ x⁻¹ - y⁻¹ = x⁻¹ * (y - x) * y⁻¹

Tactic:
rw [mul_sub_left_distrib, sub_mul, mul_assoc, show y * y⁻¹ = 1 from mul_inv_cancel₀ y_ne,
      show x⁻¹ * x = 1 from inv_mul_cancel₀ x_ne, mul_one, one_mul]

Premises used: mul_inv_cancel₀, mul_assoc, mul_sub_left_distrib, sub_mul, mul_one, inv_mul_cancel₀, one_mul
-- Module: Mathlib.Topology.Algebra.Valued.ValuedField
Goal:
K : Type u_1
inst : DivisionRing K
Γ₀ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation K Γ₀
x y : K
γ : Γ₀ˣ
y_ne : y ≠ 0
h :
  (v : (a : K) → Γ₀) (x - y) <
    min ((↑γ : Γ₀) * HMul.hMul (α := Γ₀) (β := Γ₀) ((v : (a : K) → Γ₀) y : Γ₀) ((v : (a : K) → Γ₀) y : Γ₀))
      ((v : (a : K) → Γ₀) y)
hyp1 :
  (v : (a : K) → Γ₀) (x - y) <
    (↑γ : Γ₀) * HMul.hMul (α := Γ₀) (β := Γ₀) ((v : (a : K) → Γ₀) y : Γ₀) ((v : (a : K) → Γ₀) y : Γ₀)
hyp1' :
  HMul.hMul (α := Γ₀) ((v : (a : K) → Γ₀) (x - y) : Γ₀)
      (HMul.hMul (α := Γ₀) (β := Γ₀) ((v : (a : K) → Γ₀) y : Γ₀) ((v : (a : K) → Γ₀) y : Γ₀))⁻¹ <
    (↑γ : Γ₀)
hyp2 : LT.lt.{u_2} (α := Γ₀) ((v : (a : K) → Γ₀) (x - y) : Γ₀) ((v : (a : K) → Γ₀) y : Γ₀)
key : Eq.{u_2 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) ((v : (a : K) → Γ₀) y : Γ₀)
x_ne : x ≠ 0
⊢ x⁻¹ - y⁻¹ = x⁻¹ * (y - x) * y⁻¹

Tactic:
have decomp : x⁻¹ - y⁻¹ = x⁻¹ * (y - x) * y⁻¹ := by
    rw [mul_sub_left_distrib, sub_mul, mul_assoc, show y * y⁻¹ = 1 from mul_inv_cancel₀ y_ne,
      show x⁻¹ * x = 1 from inv_mul_cancel₀ x_ne, mul_one, one_mul]
-- Module: Mathlib.Topology.Algebra.Valued.ValuedField
Goal:
K : Type u_1
inst : DivisionRing K
Γ₀ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation K Γ₀
x y : K
γ : Γ₀ˣ
y_ne : y ≠ 0
h :
  (v : (a : K) → Γ₀) (x - y) <
    min ((↑γ : Γ₀) * HMul.hMul (α := Γ₀) (β := Γ₀) ((v : (a : K) → Γ₀) y : Γ₀) ((v : (a : K) → Γ₀) y : Γ₀))
      ((v : (a : K) → Γ₀) y)
hyp1 :
  (v : (a : K) → Γ₀) (x - y) <
    (↑γ : Γ₀) * HMul.hMul (α := Γ₀) (β := Γ₀) ((v : (a : K) → Γ₀) y : Γ₀) ((v : (a : K) → Γ₀) y : Γ₀)
hyp1' :
  HMul.hMul (α := Γ₀) ((v : (a : K) → Γ₀) (x - y) : Γ₀)
      (HMul.hMul (α := Γ₀) (β := Γ₀) ((v : (a : K) → Γ₀) y : Γ₀) ((v : (a : K) → Γ₀) y : Γ₀))⁻¹ <
    (↑γ : Γ₀)
hyp2 : LT.lt.{u_2} (α := Γ₀) ((v : (a : K) → Γ₀) (x - y) : Γ₀) ((v : (a : K) → Γ₀) y : Γ₀)
key : Eq.{u_2 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) ((v : (a : K) → Γ₀) y : Γ₀)
x_ne : x ≠ 0
decomp : x⁻¹ - y⁻¹ = x⁻¹ * (y - x) * y⁻¹
rw rw₁ :
  Eq.{u_2 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) (x⁻¹ * (y - x) * y⁻¹) : Γ₀) ((v : (a : K) → Γ₀) (x⁻¹ * (y - x) * y⁻¹) : Γ₀)
⊢ Eq.{u_2 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) (x⁻¹ - y⁻¹) : Γ₀) ((v : (a : K) → Γ₀) (x⁻¹ * (y - x) * y⁻¹) : Γ₀)

Tactic:
rw [decomp]
-- Module: Mathlib.Topology.Algebra.Valued.ValuedField
Goal:
K : Type u_1
inst : DivisionRing K
Γ₀ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation K Γ₀
x y : K
γ : Γ₀ˣ
y_ne : y ≠ 0
h :
  (v : (a : K) → Γ₀) (x - y) <
    min ((↑γ : Γ₀) * HMul.hMul (α := Γ₀) (β := Γ₀) ((v : (a : K) → Γ₀) y : Γ₀) ((v : (a : K) → Γ₀) y : Γ₀))
      ((v : (a : K) → Γ₀) y)
hyp1 :
  (v : (a : K) → Γ₀) (x - y) <
    (↑γ : Γ₀) * HMul.hMul (α := Γ₀) (β := Γ₀) ((v : (a : K) → Γ₀) y : Γ₀) ((v : (a : K) → Γ₀) y : Γ₀)
hyp1' :
  HMul.hMul (α := Γ₀) ((v : (a : K) → Γ₀) (x - y) : Γ₀)
      (HMul.hMul (α := Γ₀) (β := Γ₀) ((v : (a : K) → Γ₀) y : Γ₀) ((v : (a : K) → Γ₀) y : Γ₀))⁻¹ <
    (↑γ : Γ₀)
hyp2 : LT.lt.{u_2} (α := Γ₀) ((v : (a : K) → Γ₀) (x - y) : Γ₀) ((v : (a : K) → Γ₀) y : Γ₀)
key : Eq.{u_2 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) ((v : (a : K) → Γ₀) y : Γ₀)
x_ne : x ≠ 0
decomp : x⁻¹ - y⁻¹ = x⁻¹ * (y - x) * y⁻¹
rw :
  HMul.hMul (α := Γ₀) (β := Γ₀) ((v : (a : K) → Γ₀) (x⁻¹ * (y - x)) : Γ₀) ((v : (a : K) → Γ₀) y⁻¹ : Γ₀) =
    HMul.hMul (β := Γ₀) (HMul.hMul (α := Γ₀) (β := Γ₀) ((v : (a : K) → Γ₀) x⁻¹ : Γ₀) ((v : (a : K) → Γ₀) (y - x) : Γ₀))
      ((v : (a : K) → Γ₀) y⁻¹ : Γ₀)
⊢ (v : (a : K) → Γ₀) (x⁻¹ * (y - x) * y⁻¹) =
    HMul.hMul (β := Γ₀) (HMul.hMul (α := Γ₀) (β := Γ₀) ((v : (a : K) → Γ₀) x⁻¹ : Γ₀) ((v : (a : K) → Γ₀) (y - x) : Γ₀))
      ((v : (a : K) → Γ₀) y⁻¹ : Γ₀)

Tactic:
rw [Valuation.map_mul]

Premises used: Valuation.map_mul
-- Module: Mathlib.Topology.Algebra.Valued.ValuedField
Goal:
K : Type u_1
inst : DivisionRing K
Γ₀ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation K Γ₀
x y : K
γ : Γ₀ˣ
y_ne : y ≠ 0
h :
  (v : (a : K) → Γ₀) (x - y) <
    min ((↑γ : Γ₀) * HMul.hMul (α := Γ₀) (β := Γ₀) ((v : (a : K) → Γ₀) y : Γ₀) ((v : (a : K) → Γ₀) y : Γ₀))
      ((v : (a : K) → Γ₀) y)
hyp1 :
  (v : (a : K) → Γ₀) (x - y) <
    (↑γ : Γ₀) * HMul.hMul (α := Γ₀) (β := Γ₀) ((v : (a : K) → Γ₀) y : Γ₀) ((v : (a : K) → Γ₀) y : Γ₀)
hyp1' :
  HMul.hMul (α := Γ₀) ((v : (a : K) → Γ₀) (x - y) : Γ₀)
      (HMul.hMul (α := Γ₀) (β := Γ₀) ((v : (a : K) → Γ₀) y : Γ₀) ((v : (a : K) → Γ₀) y : Γ₀))⁻¹ <
    (↑γ : Γ₀)
hyp2 : LT.lt.{u_2} (α := Γ₀) ((v : (a : K) → Γ₀) (x - y) : Γ₀) ((v : (a : K) → Γ₀) y : Γ₀)
key : Eq.{u_2 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) ((v : (a : K) → Γ₀) y : Γ₀)
x_ne : x ≠ 0
decomp : x⁻¹ - y⁻¹ = x⁻¹ * (y - x) * y⁻¹
rw rw₁ :
  HMul.hMul (β := Γ₀) (HMul.hMul (α := Γ₀) (β := Γ₀) ((v : (a : K) → Γ₀) x⁻¹ : Γ₀) ((v : (a : K) → Γ₀) (y - x) : Γ₀))
      ((v : (a : K) → Γ₀) y⁻¹ : Γ₀) =
    HMul.hMul (β := Γ₀) (HMul.hMul (α := Γ₀) (β := Γ₀) ((v : (a : K) → Γ₀) x⁻¹ : Γ₀) ((v : (a : K) → Γ₀) (y - x) : Γ₀))
      ((v : (a : K) → Γ₀) y⁻¹ : Γ₀)
⊢ HMul.hMul (α := Γ₀) (β := Γ₀) ((v : (a : K) → Γ₀) (x⁻¹ * (y - x)) : Γ₀) ((v : (a : K) → Γ₀) y⁻¹ : Γ₀) =
    HMul.hMul (β := Γ₀) (HMul.hMul (α := Γ₀) (β := Γ₀) ((v : (a : K) → Γ₀) x⁻¹ : Γ₀) ((v : (a : K) → Γ₀) (y - x) : Γ₀))
      ((v : (a : K) → Γ₀) y⁻¹ : Γ₀)

Tactic:
rw [Valuation.map_mul]

Premises used: Valuation.map_mul
-- Module: Mathlib.Topology.Algebra.Valued.ValuedField
Goal:
K : Type u_1
inst : DivisionRing K
Γ₀ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation K Γ₀
x y : K
γ : Γ₀ˣ
y_ne : y ≠ 0
h :
  (v : (a : K) → Γ₀) (x - y) <
    min ((↑γ : Γ₀) * HMul.hMul (α := Γ₀) (β := Γ₀) ((v : (a : K) → Γ₀) y : Γ₀) ((v : (a : K) → Γ₀) y : Γ₀))
      ((v : (a : K) → Γ₀) y)
hyp1 :
  (v : (a : K) → Γ₀) (x - y) <
    (↑γ : Γ₀) * HMul.hMul (α := Γ₀) (β := Γ₀) ((v : (a : K) → Γ₀) y : Γ₀) ((v : (a : K) → Γ₀) y : Γ₀)
hyp1' :
  HMul.hMul (α := Γ₀) ((v : (a : K) → Γ₀) (x - y) : Γ₀)
      (HMul.hMul (α := Γ₀) (β := Γ₀) ((v : (a : K) → Γ₀) y : Γ₀) ((v : (a : K) → Γ₀) y : Γ₀))⁻¹ <
    (↑γ : Γ₀)
hyp2 : LT.lt.{u_2} (α := Γ₀) ((v : (a : K) → Γ₀) (x - y) : Γ₀) ((v : (a : K) → Γ₀) y : Γ₀)
key : Eq.{u_2 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) ((v : (a : K) → Γ₀) y : Γ₀)
x_ne : x ≠ 0
decomp : x⁻¹ - y⁻¹ = x⁻¹ * (y - x) * y⁻¹
repeat' repeat'₁ repeat'₂ :
  HMul.hMul (α := Γ₀) (β := Γ₀) ((v : (a : K) → Γ₀) (x⁻¹ * (y - x)) : Γ₀) ((v : (a : K) → Γ₀) y⁻¹ : Γ₀) =
    HMul.hMul (β := Γ₀) (HMul.hMul (α := Γ₀) (β := Γ₀) ((v : (a : K) → Γ₀) x⁻¹ : Γ₀) ((v : (a : K) → Γ₀) (y - x) : Γ₀))
      ((v : (a : K) → Γ₀) y⁻¹ : Γ₀)
⊢ (v : (a : K) → Γ₀) (x⁻¹ * (y - x) * y⁻¹) =
    HMul.hMul (β := Γ₀) (HMul.hMul (α := Γ₀) (β := Γ₀) ((v : (a : K) → Γ₀) x⁻¹ : Γ₀) ((v : (a : K) → Γ₀) (y - x) : Γ₀))
      ((v : (a : K) → Γ₀) y⁻¹ : Γ₀)

Tactic:
repeat' rw [Valuation.map_mul]

Premises used: Valuation.map_mul
-- Module: Mathlib.Topology.Algebra.Valued.ValuedField
Goal:
K : Type u_1
inst : DivisionRing K
Γ₀ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation K Γ₀
x y : K
γ : Γ₀ˣ
y_ne : y ≠ 0
h :
  (v : (a : K) → Γ₀) (x - y) <
    min ((↑γ : Γ₀) * HMul.hMul (α := Γ₀) (β := Γ₀) ((v : (a : K) → Γ₀) y : Γ₀) ((v : (a : K) → Γ₀) y : Γ₀))
      ((v : (a : K) → Γ₀) y)
hyp1 :
  (v : (a : K) → Γ₀) (x - y) <
    (↑γ : Γ₀) * HMul.hMul (α := Γ₀) (β := Γ₀) ((v : (a : K) → Γ₀) y : Γ₀) ((v : (a : K) → Γ₀) y : Γ₀)
hyp1' :
  HMul.hMul (α := Γ₀) ((v : (a : K) → Γ₀) (x - y) : Γ₀)
      (HMul.hMul (α := Γ₀) (β := Γ₀) ((v : (a : K) → Γ₀) y : Γ₀) ((v : (a : K) → Γ₀) y : Γ₀))⁻¹ <
    (↑γ : Γ₀)
hyp2 : LT.lt.{u_2} (α := Γ₀) ((v : (a : K) → Γ₀) (x - y) : Γ₀) ((v : (a : K) → Γ₀) y : Γ₀)
key : Eq.{u_2 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) ((v : (a : K) → Γ₀) y : Γ₀)
x_ne : x ≠ 0
decomp : x⁻¹ - y⁻¹ = x⁻¹ * (y - x) * y⁻¹
rw :
  HMul.hMul (β := Γ₀) (HMul.hMul (α := Γ₀) (β := Γ₀) (((v : (a : K) → Γ₀) x)⁻¹ : Γ₀) ((v : (a : K) → Γ₀) (y - x) : Γ₀))
      ((v : (a : K) → Γ₀) y⁻¹ : Γ₀) =
    HMul.hMul (β := Γ₀)
      (HMul.hMul (α := Γ₀) (β := Γ₀) (((v : (a : K) → Γ₀) x)⁻¹ : Γ₀) ((v : (a : K) → Γ₀) (y - x) : Γ₀))
      (((v : (a : K) → Γ₀) y)⁻¹ : Γ₀)
rw₁ rw₂ :
  HMul.hMul (β := Γ₀) (HMul.hMul (α := Γ₀) (β := Γ₀) (((v : (a : K) → Γ₀) x)⁻¹ : Γ₀) ((v : (a : K) → Γ₀) (y - x) : Γ₀))
      (((v : (a : K) → Γ₀) y)⁻¹ : Γ₀) =
    HMul.hMul (β := Γ₀)
      (HMul.hMul (α := Γ₀) (β := Γ₀) (((v : (a : K) → Γ₀) x)⁻¹ : Γ₀) ((v : (a : K) → Γ₀) (y - x) : Γ₀))
      (((v : (a : K) → Γ₀) y)⁻¹ : Γ₀)
⊢ HMul.hMul (β := Γ₀) (HMul.hMul (α := Γ₀) (β := Γ₀) ((v : (a : K) → Γ₀) x⁻¹ : Γ₀) ((v : (a : K) → Γ₀) (y - x) : Γ₀))
      ((v : (a : K) → Γ₀) y⁻¹ : Γ₀) =
    HMul.hMul (β := Γ₀)
      (HMul.hMul (α := Γ₀) (β := Γ₀) (((v : (a : K) → Γ₀) x)⁻¹ : Γ₀) ((v : (a : K) → Γ₀) (y - x) : Γ₀))
      (((v : (a : K) → Γ₀) y)⁻¹ : Γ₀)

Tactic:
rw [map_inv₀, map_inv₀]

Premises used: map_inv₀
-- Module: Mathlib.Topology.Algebra.Valued.ValuedField
Goal:
K : Type u_1
inst : DivisionRing K
Γ₀ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation K Γ₀
x y : K
γ : Γ₀ˣ
y_ne : y ≠ 0
h :
  (v : (a : K) → Γ₀) (x - y) <
    min ((↑γ : Γ₀) * HMul.hMul (α := Γ₀) (β := Γ₀) ((v : (a : K) → Γ₀) y : Γ₀) ((v : (a : K) → Γ₀) y : Γ₀))
      ((v : (a : K) → Γ₀) y)
hyp1 :
  (v : (a : K) → Γ₀) (x - y) <
    (↑γ : Γ₀) * HMul.hMul (α := Γ₀) (β := Γ₀) ((v : (a : K) → Γ₀) y : Γ₀) ((v : (a : K) → Γ₀) y : Γ₀)
hyp1' :
  HMul.hMul (α := Γ₀) ((v : (a : K) → Γ₀) (x - y) : Γ₀)
      (HMul.hMul (α := Γ₀) (β := Γ₀) ((v : (a : K) → Γ₀) y : Γ₀) ((v : (a : K) → Γ₀) y : Γ₀))⁻¹ <
    (↑γ : Γ₀)
hyp2 : LT.lt.{u_2} (α := Γ₀) ((v : (a : K) → Γ₀) (x - y) : Γ₀) ((v : (a : K) → Γ₀) y : Γ₀)
key : Eq.{u_2 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) ((v : (a : K) → Γ₀) y : Γ₀)
x_ne : x ≠ 0
decomp : x⁻¹ - y⁻¹ = x⁻¹ * (y - x) * y⁻¹
rw :
  HMul.hMul (α := Γ₀) (((v : (a : K) → Γ₀) x)⁻¹ : Γ₀)
      (HMul.hMul (α := Γ₀) (β := Γ₀) ((v : (a : K) → Γ₀) (y - x) : Γ₀) (((v : (a : K) → Γ₀) y)⁻¹ : Γ₀)) =
    HMul.hMul (α := Γ₀) ((v : (a : K) → Γ₀) (y - x) : Γ₀)
      (HMul.hMul (α := Γ₀) (β := Γ₀) ((v : (a : K) → Γ₀) y : Γ₀) ((v : (a : K) → Γ₀) y : Γ₀))⁻¹
rw₁ :
  HMul.hMul (β := Γ₀) (HMul.hMul (α := Γ₀) (β := Γ₀) ((v : (a : K) → Γ₀) (y - x) : Γ₀) (((v : (a : K) → Γ₀) y)⁻¹ : Γ₀))
      (((v : (a : K) → Γ₀) x)⁻¹ : Γ₀) =
    HMul.hMul (α := Γ₀) ((v : (a : K) → Γ₀) (y - x) : Γ₀)
      (HMul.hMul (α := Γ₀) (β := Γ₀) ((v : (a : K) → Γ₀) y : Γ₀) ((v : (a : K) → Γ₀) y : Γ₀))⁻¹
rw₂ :
  HMul.hMul (β := Γ₀) (HMul.hMul (α := Γ₀) (β := Γ₀) ((v : (a : K) → Γ₀) (y - x) : Γ₀) (((v : (a : K) → Γ₀) y)⁻¹ : Γ₀))
      (((v : (a : K) → Γ₀) y)⁻¹ : Γ₀) =
    HMul.hMul (α := Γ₀) ((v : (a : K) → Γ₀) (y - x) : Γ₀)
      (HMul.hMul (α := Γ₀) (β := Γ₀) ((v : (a : K) → Γ₀) y : Γ₀) ((v : (a : K) → Γ₀) y : Γ₀))⁻¹
rw₃ :
  HMul.hMul (α := Γ₀) ((v : (a : K) → Γ₀) (y - x) : Γ₀)
      (HMul.hMul (α := Γ₀) (β := Γ₀) (((v : (a : K) → Γ₀) y)⁻¹ : Γ₀) (((v : (a : K) → Γ₀) y)⁻¹ : Γ₀)) =
    HMul.hMul (α := Γ₀) ((v : (a : K) → Γ₀) (y - x) : Γ₀)
      (HMul.hMul (α := Γ₀) (β := Γ₀) ((v : (a : K) → Γ₀) y : Γ₀) ((v : (a : K) → Γ₀) y : Γ₀))⁻¹
rw₄ rw₅ :
  HMul.hMul (α := Γ₀) ((v : (a : K) → Γ₀) (y - x) : Γ₀)
      (HMul.hMul (α := Γ₀) (β := Γ₀) (((v : (a : K) → Γ₀) y)⁻¹ : Γ₀) (((v : (a : K) → Γ₀) y)⁻¹ : Γ₀)) =
    HMul.hMul (α := Γ₀) ((v : (a : K) → Γ₀) (y - x) : Γ₀)
      (HMul.hMul (α := Γ₀) (β := Γ₀) (((v : (a : K) → Γ₀) y)⁻¹ : Γ₀) (((v : (a : K) → Γ₀) y)⁻¹ : Γ₀))
⊢ HMul.hMul (β := Γ₀) (HMul.hMul (α := Γ₀) (β := Γ₀) (((v : (a : K) → Γ₀) x)⁻¹ : Γ₀) ((v : (a : K) → Γ₀) (y - x) : Γ₀))
      (((v : (a : K) → Γ₀) y)⁻¹ : Γ₀) =
    HMul.hMul (α := Γ₀) ((v : (a : K) → Γ₀) (y - x) : Γ₀)
      (HMul.hMul (α := Γ₀) (β := Γ₀) ((v : (a : K) → Γ₀) y : Γ₀) ((v : (a : K) → Γ₀) y : Γ₀))⁻¹

Tactic:
rw [mul_assoc, mul_comm, key, mul_assoc, mul_inv_rev]

Premises used: mul_assoc, mul_comm, mul_inv_rev
-- Module: Mathlib.Topology.Algebra.Valued.ValuedField
Goal:
K : Type u_1
inst : DivisionRing K
Γ₀ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation K Γ₀
x y : K
γ : Γ₀ˣ
y_ne : y ≠ 0
h :
  (v : (a : K) → Γ₀) (x - y) <
    min ((↑γ : Γ₀) * HMul.hMul (α := Γ₀) (β := Γ₀) ((v : (a : K) → Γ₀) y : Γ₀) ((v : (a : K) → Γ₀) y : Γ₀))
      ((v : (a : K) → Γ₀) y)
hyp1 :
  (v : (a : K) → Γ₀) (x - y) <
    (↑γ : Γ₀) * HMul.hMul (α := Γ₀) (β := Γ₀) ((v : (a : K) → Γ₀) y : Γ₀) ((v : (a : K) → Γ₀) y : Γ₀)
hyp1' :
  HMul.hMul (α := Γ₀) ((v : (a : K) → Γ₀) (x - y) : Γ₀)
      (HMul.hMul (α := Γ₀) (β := Γ₀) ((v : (a : K) → Γ₀) y : Γ₀) ((v : (a : K) → Γ₀) y : Γ₀))⁻¹ <
    (↑γ : Γ₀)
hyp2 : LT.lt.{u_2} (α := Γ₀) ((v : (a : K) → Γ₀) (x - y) : Γ₀) ((v : (a : K) → Γ₀) y : Γ₀)
key : Eq.{u_2 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) ((v : (a : K) → Γ₀) y : Γ₀)
x_ne : x ≠ 0
decomp : x⁻¹ - y⁻¹ = x⁻¹ * (y - x) * y⁻¹
⊢ HMul.hMul (α := Γ₀) ((v : (a : K) → Γ₀) (y - x) : Γ₀)
      (HMul.hMul (α := Γ₀) (β := Γ₀) ((v : (a : K) → Γ₀) y : Γ₀) ((v : (a : K) → Γ₀) y : Γ₀))⁻¹ =
    HMul.hMul (α := Γ₀) ((v : (a : K) → Γ₀) (y - x) : Γ₀)
      (HMul.hMul (α := Γ₀) (β := Γ₀) ((v : (a : K) → Γ₀) y : Γ₀) ((v : (a : K) → Γ₀) y : Γ₀))⁻¹

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.Valued.ValuedField
Goal:
K : Type u_1
inst : DivisionRing K
Γ₀ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation K Γ₀
x y : K
γ : Γ₀ˣ
y_ne : y ≠ 0
h :
  (v : (a : K) → Γ₀) (x - y) <
    min ((↑γ : Γ₀) * HMul.hMul (α := Γ₀) (β := Γ₀) ((v : (a : K) → Γ₀) y : Γ₀) ((v : (a : K) → Γ₀) y : Γ₀))
      ((v : (a : K) → Γ₀) y)
hyp1 :
  (v : (a : K) → Γ₀) (x - y) <
    (↑γ : Γ₀) * HMul.hMul (α := Γ₀) (β := Γ₀) ((v : (a : K) → Γ₀) y : Γ₀) ((v : (a : K) → Γ₀) y : Γ₀)
hyp1' :
  HMul.hMul (α := Γ₀) ((v : (a : K) → Γ₀) (x - y) : Γ₀)
      (HMul.hMul (α := Γ₀) (β := Γ₀) ((v : (a : K) → Γ₀) y : Γ₀) ((v : (a : K) → Γ₀) y : Γ₀))⁻¹ <
    (↑γ : Γ₀)
hyp2 : LT.lt.{u_2} (α := Γ₀) ((v : (a : K) → Γ₀) (x - y) : Γ₀) ((v : (a : K) → Γ₀) y : Γ₀)
key : Eq.{u_2 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) ((v : (a : K) → Γ₀) y : Γ₀)
x_ne : x ≠ 0
decomp : x⁻¹ - y⁻¹ = x⁻¹ * (y - x) * y⁻¹
rw rw₁ :
  HMul.hMul (α := Γ₀) ((v : (a : K) → Γ₀) (x - y) : Γ₀)
      (HMul.hMul (α := Γ₀) (β := Γ₀) ((v : (a : K) → Γ₀) y : Γ₀) ((v : (a : K) → Γ₀) y : Γ₀))⁻¹ =
    HMul.hMul (α := Γ₀) ((v : (a : K) → Γ₀) (x - y) : Γ₀)
      (HMul.hMul (α := Γ₀) (β := Γ₀) ((v : (a : K) → Γ₀) y : Γ₀) ((v : (a : K) → Γ₀) y : Γ₀))⁻¹
⊢ HMul.hMul (α := Γ₀) ((v : (a : K) → Γ₀) (y - x) : Γ₀)
      (HMul.hMul (α := Γ₀) (β := Γ₀) ((v : (a : K) → Γ₀) y : Γ₀) ((v : (a : K) → Γ₀) y : Γ₀))⁻¹ =
    HMul.hMul (α := Γ₀) ((v : (a : K) → Γ₀) (x - y) : Γ₀)
      (HMul.hMul (α := Γ₀) (β := Γ₀) ((v : (a : K) → Γ₀) y : Γ₀) ((v : (a : K) → Γ₀) y : Γ₀))⁻¹

Tactic:
rw [Valuation.map_sub_swap]

Premises used: Valuation.map_sub_swap
-- Module: Mathlib.Topology.Algebra.Valued.ValuedField
Goal:
K : Type u_1
inst : DivisionRing K
Γ₀ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation K Γ₀
x y : K
γ : Γ₀ˣ
y_ne : y ≠ 0
h :
  (v : (a : K) → Γ₀) (x - y) <
    min ((↑γ : Γ₀) * HMul.hMul (α := Γ₀) (β := Γ₀) ((v : (a : K) → Γ₀) y : Γ₀) ((v : (a : K) → Γ₀) y : Γ₀))
      ((v : (a : K) → Γ₀) y)
hyp1 :
  (v : (a : K) → Γ₀) (x - y) <
    (↑γ : Γ₀) * HMul.hMul (α := Γ₀) (β := Γ₀) ((v : (a : K) → Γ₀) y : Γ₀) ((v : (a : K) → Γ₀) y : Γ₀)
hyp1' :
  HMul.hMul (α := Γ₀) ((v : (a : K) → Γ₀) (x - y) : Γ₀)
      (HMul.hMul (α := Γ₀) (β := Γ₀) ((v : (a : K) → Γ₀) y : Γ₀) ((v : (a : K) → Γ₀) y : Γ₀))⁻¹ <
    (↑γ : Γ₀)
hyp2 : LT.lt.{u_2} (α := Γ₀) ((v : (a : K) → Γ₀) (x - y) : Γ₀) ((v : (a : K) → Γ₀) y : Γ₀)
key : Eq.{u_2 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) ((v : (a : K) → Γ₀) y : Γ₀)
x_ne : x ≠ 0
decomp : x⁻¹ - y⁻¹ = x⁻¹ * (y - x) * y⁻¹
⊢ HMul.hMul (α := Γ₀) ((v : (a : K) → Γ₀) (x - y) : Γ₀)
      (HMul.hMul (α := Γ₀) (β := Γ₀) ((v : (a : K) → Γ₀) y : Γ₀) ((v : (a : K) → Γ₀) y : Γ₀))⁻¹ <
    (↑γ : Γ₀)

Tactic:
hyp1'
-- Module: Mathlib.Topology.Algebra.Valued.ValuedField
Goal:
K : Type u_1
inst : DivisionRing K
Γ₀ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation K Γ₀
x y : K
γ : Γ₀ˣ
y_ne : y ≠ 0
h :
  (v : (a : K) → Γ₀) (x - y) <
    min ((↑γ : Γ₀) * HMul.hMul (α := Γ₀) (β := Γ₀) ((v : (a : K) → Γ₀) y : Γ₀) ((v : (a : K) → Γ₀) y : Γ₀))
      ((v : (a : K) → Γ₀) y)
hyp1 :
  (v : (a : K) → Γ₀) (x - y) <
    (↑γ : Γ₀) * HMul.hMul (α := Γ₀) (β := Γ₀) ((v : (a : K) → Γ₀) y : Γ₀) ((v : (a : K) → Γ₀) y : Γ₀)
hyp1' :
  HMul.hMul (α := Γ₀) ((v : (a : K) → Γ₀) (x - y) : Γ₀)
      (HMul.hMul (α := Γ₀) (β := Γ₀) ((v : (a : K) → Γ₀) y : Γ₀) ((v : (a : K) → Γ₀) y : Γ₀))⁻¹ <
    (↑γ : Γ₀)
hyp2 : LT.lt.{u_2} (α := Γ₀) ((v : (a : K) → Γ₀) (x - y) : Γ₀) ((v : (a : K) → Γ₀) y : Γ₀)
key : Eq.{u_2 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) ((v : (a : K) → Γ₀) y : Γ₀)
x_ne : x ≠ 0
decomp : x⁻¹ - y⁻¹ = x⁻¹ * (y - x) * y⁻¹
v₁ : Eq.{u_2 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) (x⁻¹ - y⁻¹) : Γ₀) ((v : (a : K) → Γ₀) (x⁻¹ * (y - x) * y⁻¹) : Γ₀)
v₂ :
  (v : (a : K) → Γ₀) (x⁻¹ * (y - x) * y⁻¹) =
    HMul.hMul (β := Γ₀) (HMul.hMul (α := Γ₀) (β := Γ₀) ((v : (a : K) → Γ₀) x⁻¹ : Γ₀) ((v : (a : K) → Γ₀) (y - x) : Γ₀))
      ((v : (a : K) → Γ₀) y⁻¹ : Γ₀)
v₃ :
  HMul.hMul (β := Γ₀) (HMul.hMul (α := Γ₀) (β := Γ₀) ((v : (a : K) → Γ₀) x⁻¹ : Γ₀) ((v : (a : K) → Γ₀) (y - x) : Γ₀))
      ((v : (a : K) → Γ₀) y⁻¹ : Γ₀) =
    HMul.hMul (β := Γ₀)
      (HMul.hMul (α := Γ₀) (β := Γ₀) (((v : (a : K) → Γ₀) x)⁻¹ : Γ₀) ((v : (a : K) → Γ₀) (y - x) : Γ₀))
      (((v : (a : K) → Γ₀) y)⁻¹ : Γ₀)
v₄ :
  HMul.hMul (β := Γ₀) (HMul.hMul (α := Γ₀) (β := Γ₀) (((v : (a : K) → Γ₀) x)⁻¹ : Γ₀) ((v : (a : K) → Γ₀) (y - x) : Γ₀))
      (((v : (a : K) → Γ₀) y)⁻¹ : Γ₀) =
    HMul.hMul (α := Γ₀) ((v : (a : K) → Γ₀) (y - x) : Γ₀)
      (HMul.hMul (α := Γ₀) (β := Γ₀) ((v : (a : K) → Γ₀) y : Γ₀) ((v : (a : K) → Γ₀) y : Γ₀))⁻¹
v₅ :
  HMul.hMul (α := Γ₀) ((v : (a : K) → Γ₀) (y - x) : Γ₀)
      (HMul.hMul (α := Γ₀) (β := Γ₀) ((v : (a : K) → Γ₀) y : Γ₀) ((v : (a : K) → Γ₀) y : Γ₀))⁻¹ =
    HMul.hMul (α := Γ₀) ((v : (a : K) → Γ₀) (x - y) : Γ₀)
      (HMul.hMul (α := Γ₀) (β := Γ₀) ((v : (a : K) → Γ₀) y : Γ₀) ((v : (a : K) → Γ₀) y : Γ₀))⁻¹
⊢ (v : (a : K) → Γ₀) (x⁻¹ - y⁻¹) < (↑γ : Γ₀)

Tactic:
calc
    v (x⁻¹ - y⁻¹) = v (x⁻¹ * (y - x) * y⁻¹) := by rw [decomp]
    _ = v x⁻¹ * (v <| y - x) * v y⁻¹ := by repeat' rw [Valuation.map_mul]
    _ = (v x)⁻¹ * (v <| y - x) * (v y)⁻¹ := by rw [map_inv₀, map_inv₀]
    _ = (v <| y - x) * (v y * v y)⁻¹ := by rw [mul_assoc, mul_comm, key, mul_assoc, mul_inv_rev]
    _ = (v <| y - x) * (v y * v y)⁻¹ := rfl
    _ = (v <| x - y) * (v y * v y)⁻¹ := by rw [Valuation.map_sub_swap]
    _ < γ := hyp1'

Premises used: HMul.hMul, HSub.hSub, Inv.inv, DFunLike.coe, rfl
-- Module: Mathlib.Topology.Algebra.Valued.ValuedField
Goal:
K : Type u_1
inst : DivisionRing K
Γ₀ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation K Γ₀
x y r s : K
y_ne : y ≠ 0
hr : r ≠ 0
hs : s ≠ 0
h :
  (v : (a : K) → Γ₀) (x - y) <
    min
      (HDiv.hDiv (α := Γ₀) (β := Γ₀) ((v : (a : K) → Γ₀) s : Γ₀) ((v : (a : K) → Γ₀) r : Γ₀) *
        HMul.hMul (α := Γ₀) (β := Γ₀) ((v : (a : K) → Γ₀) y : Γ₀) ((v : (a : K) → Γ₀) y : Γ₀))
      ((v : (a : K) → Γ₀) y)
⊢ LT.lt.{u_2} (α := Γ₀) (0 : Γ₀) ((v : (a : K) → Γ₀) r : Γ₀)

Tactic:
simp [zero_lt_iff, hr]

Premises used: zero_lt_iff
-- Module: Mathlib.Topology.Algebra.Valued.ValuedField
Goal:
K : Type u_1
inst : DivisionRing K
Γ₀ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation K Γ₀
x y r s : K
y_ne : y ≠ 0
hr : r ≠ 0
hs : s ≠ 0
h :
  (v : (a : K) → Γ₀) (x - y) <
    min
      (HDiv.hDiv (α := Γ₀) (β := Γ₀) ((v : (a : K) → Γ₀) s : Γ₀) ((v : (a : K) → Γ₀) r : Γ₀) *
        HMul.hMul (α := Γ₀) (β := Γ₀) ((v : (a : K) → Γ₀) y : Γ₀) ((v : (a : K) → Γ₀) y : Γ₀))
      ((v : (a : K) → Γ₀) y)
⊢ LT.lt.{u_2} (α := Γ₀) (0 : Γ₀) ((v : (a : K) → Γ₀) r : Γ₀)

Tactic:
have hr' : 0 < v r := by simp [zero_lt_iff, hr]
-- Module: Mathlib.Topology.Algebra.Valued.ValuedField
Goal:
K : Type u_1
inst : DivisionRing K
Γ₀ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation K Γ₀
x y r s : K
y_ne : y ≠ 0
hr : r ≠ 0
hs : s ≠ 0
h :
  (v : (a : K) → Γ₀) (x - y) <
    min
      (HDiv.hDiv (α := Γ₀) (β := Γ₀) ((v : (a : K) → Γ₀) s : Γ₀) ((v : (a : K) → Γ₀) r : Γ₀) *
        HMul.hMul (α := Γ₀) (β := Γ₀) ((v : (a : K) → Γ₀) y : Γ₀) ((v : (a : K) → Γ₀) y : Γ₀))
      ((v : (a : K) → Γ₀) y)
hr' : LT.lt.{u_2} (α := Γ₀) (0 : Γ₀) ((v : (a : K) → Γ₀) r : Γ₀)
⊢ HDiv.hDiv (α := Γ₀) (β := Γ₀) ((v : (a : K) → Γ₀) s : Γ₀) ((v : (a : K) → Γ₀) r : Γ₀) ≠ 0

Tactic:
simp [hs, hr]