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
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⁻¹
⊢ x⁻¹ - y⁻¹ = x⁻¹ * (y - x) * y⁻¹
have rw₃ : x⁻¹ - y⁻¹ = x⁻¹ * 1 - x⁻¹ * 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]
-- 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
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⁻¹
⊢ x⁻¹ - y⁻¹ = x⁻¹ * (y - x) * y⁻¹
have rw₄ : x⁻¹ - y⁻¹ = x⁻¹ * 1 - 1 * 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]
-- 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
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⁻¹
⊢ x⁻¹ - y⁻¹ = x⁻¹ * (y - x) * y⁻¹
have rw₅ : x⁻¹ - y⁻¹ = x⁻¹ - 1 * 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]
-- 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
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⁻¹
⊢ x⁻¹ - y⁻¹ = x⁻¹ * (y - x) * y⁻¹
have rw₆ : 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]
-- 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 : 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
⊢ (v : (a : K) → Γ₀) (x⁻¹ - y⁻¹) < (↑γ : Γ₀)
have decomp : 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]
-- 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⁻¹
⊢ Eq.{u_2 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) (x⁻¹ - y⁻¹) : Γ₀) ((v : (a : K) → Γ₀) (x⁻¹ * (y - x) * y⁻¹) : Γ₀)
have rw : Eq.{u_2 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) (x⁻¹ * (y - x) * y⁻¹) : Γ₀) ((v : (a : K) → Γ₀) (x⁻¹ * (y - x) * y⁻¹) : Γ₀)
Tactic: rw [decomp]
-- 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 - x) * y⁻¹) =
    HMul.hMul (β := Γ₀) (HMul.hMul (α := Γ₀) (β := Γ₀) ((v : (a : K) → Γ₀) x⁻¹ : Γ₀) ((v : (a : K) → Γ₀) (y - x) : Γ₀))
      ((v : (a : K) → Γ₀) y⁻¹ : Γ₀)
have 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⁻¹ : Γ₀)
Tactic: rw [Valuation.map_mul]
-- 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) → Γ₀) (x⁻¹ * (y - x)) : Γ₀) ((v : (a : K) → Γ₀) y⁻¹ : Γ₀) =
    HMul.hMul (β := Γ₀) (HMul.hMul (α := Γ₀) (β := Γ₀) ((v : (a : K) → Γ₀) x⁻¹ : Γ₀) ((v : (a : K) → Γ₀) (y - x) : Γ₀))
      ((v : (a : K) → Γ₀) y⁻¹ : Γ₀)
have 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⁻¹ : Γ₀)
Tactic: rw [Valuation.map_mul]
-- 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 - x) * y⁻¹) =
    HMul.hMul (β := Γ₀) (HMul.hMul (α := Γ₀) (β := Γ₀) ((v : (a : K) → Γ₀) x⁻¹ : Γ₀) ((v : (a : K) → Γ₀) (y - x) : Γ₀))
      ((v : (a : K) → Γ₀) y⁻¹ : Γ₀)
have 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⁻¹ : Γ₀)
Tactic: repeat' rw [Valuation.map_mul]
-- 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 (β := Γ₀) (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)⁻¹ : Γ₀)
have 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)⁻¹ : Γ₀)
Tactic: rw [map_inv₀, map_inv₀]
-- 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 (β := Γ₀) (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)⁻¹ : Γ₀)
have 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)⁻¹ : Γ₀)
Tactic: rw [map_inv₀, map_inv₀]
-- 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 (β := Γ₀) (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) → Γ₀) 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 : Γ₀))⁻¹
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⁻¹
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 : Γ₀))⁻¹
⊢ 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 (β := Γ₀) (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 : Γ₀))⁻¹
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⁻¹
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 : Γ₀))⁻¹
⊢ 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 (β := Γ₀) (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 : Γ₀))⁻¹
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⁻¹
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 : Γ₀))⁻¹
⊢ 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]