awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Algebra.Valued.ValuedField (goal)
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 : Γ₀))⁻¹
⊢ 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 : Γ₀))⁻¹
have 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)⁻¹ : Γ₀))
Tactic: rw [mul_assoc, mul_comm, key, mul_assoc, mul_inv_rev]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Valued.ValuedField (goal)
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) → Γ₀) (x - y) : Γ₀)
      (HMul.hMul (α := Γ₀) (β := Γ₀) ((v : (a : K) → Γ₀) y : Γ₀) ((v : (a : K) → Γ₀) y : Γ₀))⁻¹
have 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 : Γ₀))⁻¹
Tactic: rw [Valuation.map_sub_swap]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Valued.ValuedField (goal)
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 : (a : K) → Γ₀) (x⁻¹ - y⁻¹) < (↑γ : Γ₀)
have v₁ : Eq.{u_2 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) (x⁻¹ - y⁻¹) : Γ₀) ((v : (a : K) → Γ₀) (x⁻¹ * (y - 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'
-- Lean 4 proof step from Mathlib.Topology.Algebra.Valued.ValuedField (goal)
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 : (a : K) → Γ₀) (x⁻¹ - y⁻¹) < (↑γ : Γ₀)
have 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⁻¹ : Γ₀)
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'
-- Lean 4 proof step from Mathlib.Topology.Algebra.Valued.ValuedField (goal)
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 : (a : K) → Γ₀) (x⁻¹ - y⁻¹) < (↑γ : Γ₀)
have 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)⁻¹ : Γ₀)
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'
-- Lean 4 proof step from Mathlib.Topology.Algebra.Valued.ValuedField (goal)
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 : (a : K) → Γ₀) (x⁻¹ - y⁻¹) < (↑γ : Γ₀)
have 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 : Γ₀))⁻¹
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'
-- Lean 4 proof step from Mathlib.Topology.Algebra.Valued.ValuedField (goal)
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 : (a : K) → Γ₀) (x⁻¹ - y⁻¹) < (↑γ : Γ₀)
have 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 : Γ₀))⁻¹
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'
-- Lean 4 proof step from Mathlib.Topology.Algebra.Valued.ValuedField (hypothesis)
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)
⊢ HMul.hMul (α := Γ₀) (β := Γ₀) ((v : (a : K) → Γ₀) (x⁻¹ - y⁻¹) : Γ₀) ((v : (a : K) → Γ₀) r : Γ₀) < (v : (a : K) → Γ₀) s
have hr' : LT.lt.{u_2} (α := Γ₀) (0 : Γ₀) ((v : (a : K) → Γ₀) r : Γ₀)
Tactic: have hr' : 0 < v r := by simp [zero_lt_iff, hr]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Valued.ValuedField (goal)
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 : Γ₀)
γ : Γ₀ˣ := Units.mk0 (HDiv.hDiv (α := Γ₀) (β := Γ₀) ((v : (a : K) → Γ₀) s : Γ₀) ((v : (a : K) → Γ₀) r : Γ₀)) ⋯
⊢ HMul.hMul (α := Γ₀) (β := Γ₀) ((v : (a : K) → Γ₀) (x⁻¹ - y⁻¹) : Γ₀) ((v : (a : K) → Γ₀) r : Γ₀) <
    HMul.hMul (β := Γ₀) (↑γ : Γ₀) ((v : (a : K) → Γ₀) r : Γ₀)
have hbc : (v : (a : K) → Γ₀) (x⁻¹ - y⁻¹) < (↑γ : Γ₀)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Topology.Algebra.Valued.ValuedField (goal)
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 : Γ₀)
γ : Γ₀ˣ := Units.mk0 (HDiv.hDiv (α := Γ₀) (β := Γ₀) ((v : (a : K) → Γ₀) s : Γ₀) ((v : (a : K) → Γ₀) r : Γ₀)) ⋯
⊢ HMul.hMul (α := Γ₀) (β := Γ₀) ((v : (a : K) → Γ₀) (x⁻¹ - y⁻¹) : Γ₀) ((v : (a : K) → Γ₀) r : Γ₀) < (v : (a : K) → Γ₀) s
have v₁ : HMul.hMul (α := Γ₀) (β := Γ₀) ((v : (a : K) → Γ₀) (x⁻¹ - y⁻¹) : Γ₀) ((v : (a : K) → Γ₀) r : Γ₀) <
  HMul.hMul (β := Γ₀) (↑γ : Γ₀) ((v : (a : K) → Γ₀) r : Γ₀)
Tactic: calc
    v (x⁻¹ - y⁻¹) * v r < γ * v r := by gcongr; exact Valuation.inversion_estimate v y_ne h
    _ = v s := div_mul_cancel₀ _ (by simpa)
-- Lean 4 proof step from Mathlib.Topology.Algebra.Valued.ValuedField (goal)
Goal:
K : Type u_1
inst : DivisionRing K
Γ₀ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ₀
inst_2 : Valued K Γ₀
x : K
x_ne : x ≠ 0
s : Set K
s_in : s ∈ 𝓝 x⁻¹
⊢ s ∈ map Inv.inv (𝓝 x)
have obtain : ∀ (γ : (ValueGroup₀ (F := Valuation K Γ₀) v)ˣ)
  (hs : {y : K | (Valuation.restrict v : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀)) (y - x⁻¹) < (↑γ : ValueGroup₀ v)} ⊆ s),
  s ∈ map Inv.inv (𝓝 x)
Tactic: obtain ⟨γ, hs⟩ := Valued.mem_nhds.mp s_in
-- Lean 4 proof step from Mathlib.Topology.Algebra.Valued.ValuedField (goal)
Goal:
K : Type u_1
inst : DivisionRing K
Γ₀ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ₀
inst_2 : Valued K Γ₀
x : K
x_ne : x ≠ 0
s : Set K
γ : (ValueGroup₀ (F := Valuation K Γ₀) v)ˣ
hs : {y : K | (Valuation.restrict v : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀)) (y - x⁻¹) < (↑γ : ValueGroup₀ v)} ⊆ s
⊢ s ∈ map Inv.inv (𝓝 x)
have rw : ∃ (γ : (ValueGroup₀ (F := Valuation K Γ₀) v)ˣ),
  {y : K | (Valuation.restrict v : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀)) (y - x) < (↑γ : ValueGroup₀ v)} ⊆
    Inv.inv ⁻¹' s
Tactic: rw [mem_map, Valued.mem_nhds]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Valued.ValuedField (goal)
Goal:
K : Type u_1
inst : DivisionRing K
Γ₀ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ₀
inst_2 : Valued K Γ₀
x : K
x_ne : x ≠ 0
s : Set K
γ : (ValueGroup₀ (F := Valuation K Γ₀) v)ˣ
hs : {y : K | (Valuation.restrict v : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀)) (y - x⁻¹) < (↑γ : ValueGroup₀ v)} ⊆ s
γ' : (ValueGroup₀ (F := Valuation K Γ₀) v)ˣ :=
  Units.mk0
    (((restrict₀ v : MonoidWithZeroHom.{u_1, u_2} K (ValueGroup₀ (F := Valuation K Γ₀) v)) : (a : K) → ValueGroup₀ v) x)
    ⋯
⊢ ∃ (γ : (ValueGroup₀ (F := Valuation K Γ₀) v)ˣ),
    {y : K | (Valuation.restrict v : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀)) (y - x) < (↑γ : ValueGroup₀ v)} ⊆
      Inv.inv ⁻¹' s
have h : {y : K |
    (Valuation.restrict v : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀)) (y - x) <
      (↑(min (γ * (γ' * γ')) γ') : ValueGroup₀ v)} ⊆
  Inv.inv ⁻¹' s
Tactic: use min (γ * (γ' * γ')) γ'
-- Lean 4 proof step from Mathlib.Topology.Algebra.Valued.ValuedField (goal)
Goal:
K : Type u_1
inst : DivisionRing K
Γ₀ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ₀
inst_2 : Valued K Γ₀
x : K
x_ne : x ≠ 0
s : Set K
γ : (ValueGroup₀ (F := Valuation K Γ₀) v)ˣ
hs : {y : K | (Valuation.restrict v : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀)) (y - x⁻¹) < (↑γ : ValueGroup₀ v)} ⊆ s
γ' : (ValueGroup₀ (F := Valuation K Γ₀) v)ˣ :=
  Units.mk0
    (((restrict₀ v : MonoidWithZeroHom.{u_1, u_2} K (ValueGroup₀ (F := Valuation K Γ₀) v)) : (a : K) → ValueGroup₀ v) x)
    ⋯
y : K
y_in :
  Membership.mem (γ := Set K)
    {y : K |
      (Valuation.restrict v : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀)) (y - x) <
        (↑(min (γ * (γ' * γ')) γ') : ValueGroup₀ v)}
    y
⊢ y ∈ Inv.inv ⁻¹' s
have h : Membership.mem (γ := Set K)
  {y : K | (Valuation.restrict v : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀)) (y - x⁻¹) < (↑γ : ValueGroup₀ v)} y⁻¹
Tactic: apply hs
-- Lean 4 proof step from Mathlib.Topology.Algebra.Valued.ValuedField (hypothesis)
Goal:
K : Type u_1
inst : DivisionRing K
Γ₀ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ₀
inst_2 : Valued K Γ₀
x : K
x_ne : x ≠ 0
s : Set K
γ : (ValueGroup₀ (F := Valuation K Γ₀) v)ˣ
hs : {y : K | (Valuation.restrict v : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀)) (y - x⁻¹) < (↑γ : ValueGroup₀ v)} ⊆ s
γ' : (ValueGroup₀ (F := Valuation K Γ₀) v)ˣ :=
  Units.mk0
    (((restrict₀ v : MonoidWithZeroHom.{u_1, u_2} K (ValueGroup₀ (F := Valuation K Γ₀) v)) : (a : K) → ValueGroup₀ v) x)
    ⋯
y : K
y_in :
  Membership.mem (γ := Set K)
    {y : K |
      (Valuation.restrict v : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀)) (y - x) <
        (↑(min (γ * (γ' * γ')) γ') : ValueGroup₀ v)}
    y
⊢ Membership.mem (γ := Set K)
    {y : K | (Valuation.restrict v : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀)) (y - x⁻¹) < (↑γ : ValueGroup₀ v)} y⁻¹
have y_in₁ : (Valuation.restrict v : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀)) (y - x) <
  min ((↑γ : ValueGroup₀ v) * ((↑γ' : ValueGroup₀ v) * (↑γ' : ValueGroup₀ v))) (↑γ' : ValueGroup₀ v)
Tactic: simp only [mem_setOf_eq, Units.min_val, Units.val_mul] at y_in
Cleared hypotheses: y_in
-- Lean 4 proof step from Mathlib.Topology.Algebra.Valued.ValuedField (goal)
Goal:
K : Type u_1
inst : DivisionRing K
Γ₀ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ₀
inst_2 : Valued K Γ₀
⊢ T0Space K
have suffices : T2Space K
Tactic: suffices T2Space K by infer_instance
-- Lean 4 proof step from Mathlib.Topology.Algebra.Valued.ValuedField (goal)
Goal:
K : Type u_1
inst : DivisionRing K
Γ₀ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ₀
inst_2 : Valued K Γ₀
⊢ T2Space K
have H : ∀ (x : K), x ≠ 0 → ∃ (U : Set K), Membership.mem (γ := Filter K) (𝓝 0) U ∧ x ∉ U
Tactic: apply IsTopologicalAddGroup.t2Space_of_zero_sep
-- Lean 4 proof step from Mathlib.Topology.Algebra.Valued.ValuedField (goal)
Goal:
K : Type u_1
inst : DivisionRing K
Γ₀ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ₀
inst_2 : Valued K Γ₀
x : K
x_ne : x ≠ 0
⊢ ∃ (U : Set K), Membership.mem (γ := Filter K) (𝓝 0) U ∧ x ∉ U
have H : Membership.mem (γ := Filter K) (𝓝 0)
  {k : K | LT.lt.{u_2} (α := Γ₀) ((v : (a : K) → Γ₀) k : Γ₀) ((v : (a : K) → Γ₀) x : Γ₀)}
Tactic: refine ⟨{ k | v k < v x }, ?_, fun h => lt_irrefl _ h⟩
-- Lean 4 proof step from Mathlib.Topology.Algebra.Valued.ValuedField (goal)
Goal:
K : Type u_1
inst : DivisionRing K
Γ₀ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ₀
inst_2 : Valued K Γ₀
x : K
x_ne : x ≠ 0
⊢ Membership.mem (γ := Filter K) (𝓝 0)
    {k : K | LT.lt.{u_2} (α := Γ₀) ((v : (a : K) → Γ₀) k : Γ₀) ((v : (a : K) → Γ₀) x : Γ₀)}
have H : ∃ (γ : (ValueGroup₀ (F := Valuation K Γ₀) v)ˣ),
  Subset.{u_1} (α := Set K)
    {y : K | (Valuation.restrict v : (a : K) → ValueGroup₀ (↑v : K →*₀ Γ₀)) (y - 0) < (↑γ : ValueGroup₀ v)}
    {k : K | LT.lt.{u_2} (α := Γ₀) ((v : (a : K) → Γ₀) k : Γ₀) ((v : (a : K) → Γ₀) x : Γ₀)}
Tactic: rw [Valued.mem_nhds]