K : Type u_2
inst✝¹ : DivisionRing K
Γ₀ : Type u_1
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation K Γ₀
x y : K
γ : Γ₀ˣ
y_ne : y ≠ 0
h : ↑v (x - y) < min (↑γ * (↑v y * ↑v y)) (↑v y)
hyp1 : ↑v (x - y) < ↑γ * (↑v y * ↑v y)
⊢ ↑v (x⁻¹ - y⁻¹) < ↑γ
K : Type u_2
inst✝¹ : DivisionRing K
Γ₀ : Type u_1
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation K Γ₀
x y : K
γ : Γ₀ˣ
y_ne : y ≠ 0
h : ↑v (x - y) < min (↑γ * (↑v y * ↑v y)) (↑v y)
⊢ ↑v (x⁻¹ - y⁻¹) < ↑γ
have hyp1 : v (x - y) < γ * (v y * v y) := lt_of_lt_of_le h (min_le_left _ _)
K : Type u_2
inst✝¹ : DivisionRing K
Γ₀ : Type u_1
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation K Γ₀
x y : K
γ : Γ₀ˣ
y_ne : y ≠ 0
h : ↑v (x - y) < min (↑γ * (↑v y * ↑v y)) (↑v y)
hyp1 : ↑v (x - y) < ↑γ * (↑v y * ↑v y)
hyp1' : ↑v (x - y) * (↑v y * ↑v y)⁻¹ < ↑γ
⊢ ↑v (x⁻¹ - y⁻¹) < ↑γ
K : Type u_2
inst✝¹ : DivisionRing K
Γ₀ : Type u_1
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation K Γ₀
x y : K
γ : Γ₀ˣ
y_ne : y ≠ 0
h : ↑v (x - y) < min (↑γ * (↑v y * ↑v y)) (↑v y)
hyp1 : ↑v (x - y) < ↑γ * (↑v y * ↑v y)
⊢ ↑v (x⁻¹ - y⁻¹) < ↑γ
have hyp1' : v (x - y) * (v y * v y)⁻¹ < γ := mul_inv_lt_of_lt_mul₀ hyp1
K : Type u_2
inst✝¹ : DivisionRing K
Γ₀ : Type u_1
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation K Γ₀
x y : K
γ : Γ₀ˣ
y_ne : y ≠ 0
h : ↑v (x - y) < min (↑γ * (↑v y * ↑v y)) (↑v y)
hyp1 : ↑v (x - y) < ↑γ * (↑v y * ↑v y)
hyp1' : ↑v (x - y) * (↑v y * ↑v y)⁻¹ < ↑γ
hyp2 : ↑v (x - y) < ↑v y
⊢ ↑v (x⁻¹ - y⁻¹) < ↑γ
K : Type u_2
inst✝¹ : DivisionRing K
Γ₀ : Type u_1
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation K Γ₀
x y : K
γ : Γ₀ˣ
y_ne : y ≠ 0
h : ↑v (x - y) < min (↑γ * (↑v y * ↑v y)) (↑v y)
hyp1 : ↑v (x - y) < ↑γ * (↑v y * ↑v y)
hyp1' : ↑v (x - y) * (↑v y * ↑v y)⁻¹ < ↑γ
⊢ ↑v (x⁻¹ - y⁻¹) < ↑γ
have hyp2 : v (x - y) < v y := lt_of_lt_of_le h (min_le_right _ _)
K : Type u_2
inst✝¹ : DivisionRing K
Γ₀ : Type u_1
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation K Γ₀
x y : K
γ : Γ₀ˣ
y_ne : y ≠ 0
h : ↑v (x - y) < min (↑γ * (↑v y * ↑v y)) (↑v y)
hyp1 : ↑v (x - y) < ↑γ * (↑v y * ↑v y)
hyp1' : ↑v (x - y) * (↑v y * ↑v y)⁻¹ < ↑γ
hyp2 : ↑v (x - y) < ↑v y
key : ↑v x = ↑v y
⊢ ↑v (x⁻¹ - y⁻¹) < ↑γ
K : Type u_2
inst✝¹ : DivisionRing K
Γ₀ : Type u_1
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation K Γ₀
x y : K
γ : Γ₀ˣ
y_ne : y ≠ 0
h : ↑v (x - y) < min (↑γ * (↑v y * ↑v y)) (↑v y)
hyp1 : ↑v (x - y) < ↑γ * (↑v y * ↑v y)
hyp1' : ↑v (x - y) * (↑v y * ↑v y)⁻¹ < ↑γ
hyp2 : ↑v (x - y) < ↑v y
⊢ ↑v (x⁻¹ - y⁻¹) < ↑γ
have key : v x = v y := Valuation.map_eq_of_sub_lt v hyp2
K : Type u_2
inst✝¹ : DivisionRing K
Γ₀ : Type u_1
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation K Γ₀
x y : K
γ : Γ₀ˣ
y_ne : y ≠ 0
h : ↑v (x - y) < min (↑γ * (↑v y * ↑v y)) (↑v y)
hyp1 : ↑v (x - y) < ↑γ * (↑v y * ↑v y)
hyp1' : ↑v (x - y) * (↑v y * ↑v y)⁻¹ < ↑γ
hyp2 : ↑v (x - y) < ↑v y
key : ↑v x = ↑v y
x_ne : x ≠ 0
⊢ ↑v (x⁻¹ - y⁻¹) < ↑γ
K : Type u_2
inst✝¹ : DivisionRing K
Γ₀ : Type u_1
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation K Γ₀
x y : K
γ : Γ₀ˣ
y_ne : y ≠ 0
h : ↑v (x - y) < min (↑γ * (↑v y * ↑v y)) (↑v y)
hyp1 : ↑v (x - y) < ↑γ * (↑v y * ↑v y)
hyp1' : ↑v (x - y) * (↑v y * ↑v y)⁻¹ < ↑γ
hyp2 : ↑v (x - y) < ↑v y
key : ↑v x = ↑v y
⊢ ↑v (x⁻¹ - y⁻¹) < ↑γ
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
K : Type u_2
inst✝¹ : DivisionRing K
Γ₀ : Type u_1
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation K Γ₀
x y : K
γ : Γ₀ˣ
y_ne : y ≠ 0
h : ↑v (x - y) < min (↑γ * (↑v y * ↑v y)) (↑v y)
hyp1 : ↑v (x - y) < ↑γ * (↑v y * ↑v y)
hyp1' : ↑v (x - y) * (↑v y * ↑v y)⁻¹ < ↑γ
hyp2 : ↑v (x - y) < ↑v y
key : ↑v x = ↑v y
x_ne : x ≠ 0
decomp : x⁻¹ - y⁻¹ = x⁻¹ * (y - x) * y⁻¹
⊢ ↑v (x⁻¹ - y⁻¹) < ↑γ
K : Type u_2
inst✝¹ : DivisionRing K
Γ₀ : Type u_1
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation K Γ₀
x y : K
γ : Γ₀ˣ
y_ne : y ≠ 0
h : ↑v (x - y) < min (↑γ * (↑v y * ↑v y)) (↑v y)
hyp1 : ↑v (x - y) < ↑γ * (↑v y * ↑v y)
hyp1' : ↑v (x - y) * (↑v y * ↑v y)⁻¹ < ↑γ
hyp2 : ↑v (x - y) < ↑v y
key : ↑v x = ↑v y
x_ne : x ≠ 0
⊢ ↑v (x⁻¹ - y⁻¹) < ↑γ
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]
no goals
K : Type u_2
inst✝¹ : DivisionRing K
Γ₀ : Type u_1
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation K Γ₀
x y : K
γ : Γ₀ˣ
y_ne : y ≠ 0
h : ↑v (x - y) < min (↑γ * (↑v y * ↑v y)) (↑v y)
hyp1 : ↑v (x - y) < ↑γ * (↑v y * ↑v y)
hyp1' : ↑v (x - y) * (↑v y * ↑v y)⁻¹ < ↑γ
hyp2 : ↑v (x - y) < ↑v y
key : ↑v x = ↑v y
x_ne : x ≠ 0
decomp : x⁻¹ - y⁻¹ = x⁻¹ * (y - x) * y⁻¹
⊢ ↑v (x⁻¹ - y⁻¹) < ↑γ
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'
K : Type u_2
inst✝¹ : DivisionRing K
Γ₀ : Type u_1
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation K Γ₀
x y : K
γ : Γ₀ˣ
y_ne : y ≠ 0
h✝ : ↑v (x - y) < min (↑γ * (↑v y * ↑v y)) (↑v y)
hyp1 : ↑v (x - y) < ↑γ * (↑v y * ↑v y)
hyp1' : ↑v (x - y) * (↑v y * ↑v y)⁻¹ < ↑γ
hyp2 : ↑v (x - y) < ↑v y
key : ↑v x = ↑v y
h : x = 0
⊢ False
K : Type u_2
inst✝¹ : DivisionRing K
Γ₀ : Type u_1
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation K Γ₀
x y : K
γ : Γ₀ˣ
y_ne : y ≠ 0
h : ↑v (x - y) < min (↑γ * (↑v y * ↑v y)) (↑v y)
hyp1 : ↑v (x - y) < ↑γ * (↑v y * ↑v y)
hyp1' : ↑v (x - y) * (↑v y * ↑v y)⁻¹ < ↑γ
hyp2 : ↑v (x - y) < ↑v y
key : ↑v x = ↑v y
⊢ x ≠ 0
intro h
K : Type u_2
inst✝¹ : DivisionRing K
Γ₀ : Type u_1
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation K Γ₀
x y : K
γ : Γ₀ˣ
y_ne : y ≠ 0
h✝ : ↑v (x - y) < min (↑γ * (↑v y * ↑v y)) (↑v y)
hyp1 : ↑v (x - y) < ↑γ * (↑v y * ↑v y)
hyp1' : ↑v (x - y) * (↑v y * ↑v y)⁻¹ < ↑γ
hyp2 : ↑v (x - y) < ↑v y
key : ↑v x = ↑v y
h : x = 0
⊢ y = 0
K : Type u_2
inst✝¹ : DivisionRing K
Γ₀ : Type u_1
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation K Γ₀
x y : K
γ : Γ₀ˣ
y_ne : y ≠ 0
h✝ : ↑v (x - y) < min (↑γ * (↑v y * ↑v y)) (↑v y)
hyp1 : ↑v (x - y) < ↑γ * (↑v y * ↑v y)
hyp1' : ↑v (x - y) * (↑v y * ↑v y)⁻¹ < ↑γ
hyp2 : ↑v (x - y) < ↑v y
key : ↑v x = ↑v y
h : x = 0
⊢ False
apply y_ne
K : Type u_2
inst✝¹ : DivisionRing K
Γ₀ : Type u_1
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation K Γ₀
x y : K
γ : Γ₀ˣ
y_ne : y ≠ 0
h✝ : ↑v (x - y) < min (↑γ * (↑v y * ↑v y)) (↑v y)
hyp1 : ↑v (x - y) < ↑γ * (↑v y * ↑v y)
hyp1' : ↑v (x - y) * (↑v y * ↑v y)⁻¹ < ↑γ
hyp2 : ↑v (x - y) < ↑v y
key : 0 = ↑v y
h : x = 0
⊢ y = 0
K : Type u_2
inst✝¹ : DivisionRing K
Γ₀ : Type u_1
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation K Γ₀
x y : K
γ : Γ₀ˣ
y_ne : y ≠ 0
h✝ : ↑v (x - y) < min (↑γ * (↑v y * ↑v y)) (↑v y)
hyp1 : ↑v (x - y) < ↑γ * (↑v y * ↑v y)
hyp1' : ↑v (x - y) * (↑v y * ↑v y)⁻¹ < ↑γ
hyp2 : ↑v (x - y) < ↑v y
key : ↑v x = ↑v y
h : x = 0
⊢ y = 0
rw [h, v.map_zero] at key
no goals
K : Type u_2
inst✝¹ : DivisionRing K
Γ₀ : Type u_1
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation K Γ₀
x y : K
γ : Γ₀ˣ
y_ne : y ≠ 0
h✝ : ↑v (x - y) < min (↑γ * (↑v y * ↑v y)) (↑v y)
hyp1 : ↑v (x - y) < ↑γ * (↑v y * ↑v y)
hyp1' : ↑v (x - y) * (↑v y * ↑v y)⁻¹ < ↑γ
hyp2 : ↑v (x - y) < ↑v y
key : 0 = ↑v y
h : x = 0
⊢ y = 0
exact v.zero_iff.1 key.symm
no goals
K : Type u_2
inst✝¹ : DivisionRing K
Γ₀ : Type u_1
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation K Γ₀
x y : K
γ : Γ₀ˣ
y_ne : y ≠ 0
h : ↑v (x - y) < min (↑γ * (↑v y * ↑v y)) (↑v y)
hyp1 : ↑v (x - y) < ↑γ * (↑v y * ↑v y)
hyp1' : ↑v (x - y) * (↑v y * ↑v y)⁻¹ < ↑γ
hyp2 : ↑v (x - y) < ↑v y
key : ↑v x = ↑v y
x_ne : x ≠ 0
⊢ x⁻¹ - y⁻¹ = x⁻¹ * (y - x) * y⁻¹
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]
no goals
K : Type u_2
inst✝¹ : DivisionRing K
Γ₀ : Type u_1
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation K Γ₀
x y : K
γ : Γ₀ˣ
y_ne : y ≠ 0
h : ↑v (x - y) < min (↑γ * (↑v y * ↑v y)) (↑v y)
hyp1 : ↑v (x - y) < ↑γ * (↑v y * ↑v y)
hyp1' : ↑v (x - y) * (↑v y * ↑v y)⁻¹ < ↑γ
hyp2 : ↑v (x - y) < ↑v y
key : ↑v x = ↑v y
x_ne : x ≠ 0
decomp : x⁻¹ - y⁻¹ = x⁻¹ * (y - x) * y⁻¹
⊢ ↑v (x⁻¹ - y⁻¹) = ↑v (x⁻¹ * (y - x) * y⁻¹)
rw [decomp]
no goals
K : Type u_2
inst✝¹ : DivisionRing K
Γ₀ : Type u_1
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation K Γ₀
x y : K
γ : Γ₀ˣ
y_ne : y ≠ 0
h : ↑v (x - y) < min (↑γ * (↑v y * ↑v y)) (↑v y)
hyp1 : ↑v (x - y) < ↑γ * (↑v y * ↑v y)
hyp1' : ↑v (x - y) * (↑v y * ↑v y)⁻¹ < ↑γ
hyp2 : ↑v (x - y) < ↑v y
key : ↑v x = ↑v y
x_ne : x ≠ 0
decomp : x⁻¹ - y⁻¹ = x⁻¹ * (y - x) * y⁻¹
⊢ ↑v (x⁻¹ * (y - x) * y⁻¹) = ↑v x⁻¹ * ↑v (y - x) * ↑v y⁻¹
repeat' rw [Valuation.map_mul]
no goals
K : Type u_2
inst✝¹ : DivisionRing K
Γ₀ : Type u_1
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation K Γ₀
x y : K
γ : Γ₀ˣ
y_ne : y ≠ 0
h : ↑v (x - y) < min (↑γ * (↑v y * ↑v y)) (↑v y)
hyp1 : ↑v (x - y) < ↑γ * (↑v y * ↑v y)
hyp1' : ↑v (x - y) * (↑v y * ↑v y)⁻¹ < ↑γ
hyp2 : ↑v (x - y) < ↑v y
key : ↑v x = ↑v y
x_ne : x ≠ 0
decomp : x⁻¹ - y⁻¹ = x⁻¹ * (y - x) * y⁻¹
⊢ ↑v (x⁻¹ * (y - x)) * ↑v y⁻¹ = ↑v x⁻¹ * ↑v (y - x) * ↑v y⁻¹
rw [Valuation.map_mul]
no goals
K : Type u_2
inst✝¹ : DivisionRing K
Γ₀ : Type u_1
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation K Γ₀
x y : K
γ : Γ₀ˣ
y_ne : y ≠ 0
h : ↑v (x - y) < min (↑γ * (↑v y * ↑v y)) (↑v y)
hyp1 : ↑v (x - y) < ↑γ * (↑v y * ↑v y)
hyp1' : ↑v (x - y) * (↑v y * ↑v y)⁻¹ < ↑γ
hyp2 : ↑v (x - y) < ↑v y
key : ↑v x = ↑v y
x_ne : x ≠ 0
decomp : x⁻¹ - y⁻¹ = x⁻¹ * (y - x) * y⁻¹
⊢ ↑v x⁻¹ * ↑v (y - x) * ↑v y⁻¹ = (↑v x)⁻¹ * ↑v (y - x) * (↑v y)⁻¹
rw [map_inv₀, map_inv₀]
no goals
K : Type u_2
inst✝¹ : DivisionRing K
Γ₀ : Type u_1
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation K Γ₀
x y : K
γ : Γ₀ˣ
y_ne : y ≠ 0
h : ↑v (x - y) < min (↑γ * (↑v y * ↑v y)) (↑v y)
hyp1 : ↑v (x - y) < ↑γ * (↑v y * ↑v y)
hyp1' : ↑v (x - y) * (↑v y * ↑v y)⁻¹ < ↑γ
hyp2 : ↑v (x - y) < ↑v y
key : ↑v x = ↑v y
x_ne : x ≠ 0
decomp : x⁻¹ - y⁻¹ = x⁻¹ * (y - x) * y⁻¹
⊢ (↑v x)⁻¹ * ↑v (y - x) * (↑v y)⁻¹ = ↑v (y - x) * (↑v y * ↑v y)⁻¹
rw [mul_assoc, mul_comm, key, mul_assoc, mul_inv_rev]
no goals
K : Type u_2
inst✝¹ : DivisionRing K
Γ₀ : Type u_1
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation K Γ₀
x y : K
γ : Γ₀ˣ
y_ne : y ≠ 0
h : ↑v (x - y) < min (↑γ * (↑v y * ↑v y)) (↑v y)
hyp1 : ↑v (x - y) < ↑γ * (↑v y * ↑v y)
hyp1' : ↑v (x - y) * (↑v y * ↑v y)⁻¹ < ↑γ
hyp2 : ↑v (x - y) < ↑v y
key : ↑v x = ↑v y
x_ne : x ≠ 0
decomp : x⁻¹ - y⁻¹ = x⁻¹ * (y - x) * y⁻¹
⊢ ↑v (y - x) * (↑v y * ↑v y)⁻¹ = ↑v (x - y) * (↑v y * ↑v y)⁻¹
rw [Valuation.map_sub_swap]