awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.WithVal (goal)
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
hp0' : LT.lt (α := ℚ) 0 (↑p : ℚ)
hp0 : LT.lt (α := ℝ) 0 (↑p : ℝ)⁻¹
hp1' : LT.lt (α := ℚ) 1 (↑p : ℚ)
hp1 : LT.lt (α := ℝ) (↑p : ℝ)⁻¹ 1
n : ℕ
hn :
  Eq (α := WithZero (Multiplicative ℤ))
    ((Valued.v : (a : WithVal (Rat.padicValuation p)) → WithZero (Multiplicative ℤ))
        (HPow.hPow (α := WithVal (Rat.padicValuation p)) (↑p : WithVal (Rat.padicValuation p)) n) :
      WithZero (Multiplicative ℤ))
    (exp (-(↑n : ℤ)) : WithZero (Multiplicative ℤ))
x y : WithVal (Rat.padicValuation p)
x' : ℚ := (WithVal.equiv (Rat.padicValuation p) : (a : WithVal (Rat.padicValuation p)) → ℚ) x
hx : x' = (WithVal.equiv (Rat.padicValuation p) : (a : WithVal (Rat.padicValuation p)) → ℚ) x
y' : ℚ := (WithVal.equiv (Rat.padicValuation p) : (a : WithVal (Rat.padicValuation p)) → ℚ) y
hy : y' = (WithVal.equiv (Rat.padicValuation p) : (a : WithVal (Rat.padicValuation p)) → ℚ) y
h : (if x' - y' = 0 then 0 else exp (-padicValRat p (x' - y'))) < exp (-(↑n : ℤ))
⊢ (if x' - y' = 0 then 0 else (HPow.hPow (α := ℚ) (↑p : ℚ) (padicValRat p (x' - y')))⁻¹) ≤
    (HPow.hPow (α := ℚ) (↑p : ℚ) n)⁻¹
have pos : ∀ (H : x' - y' = 0), 0 ≤ (HPow.hPow (α := ℚ) (↑p : ℚ) n)⁻¹
Tactic: split_ifs with H
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.WithVal (goal)
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
hp0' : LT.lt (α := ℚ) 0 (↑p : ℚ)
hp0 : LT.lt (α := ℝ) 0 (↑p : ℝ)⁻¹
hp1' : LT.lt (α := ℚ) 1 (↑p : ℚ)
hp1 : LT.lt (α := ℝ) (↑p : ℝ)⁻¹ 1
n : ℕ
hn :
  Eq (α := WithZero (Multiplicative ℤ))
    ((Valued.v : (a : WithVal (Rat.padicValuation p)) → WithZero (Multiplicative ℤ))
        (HPow.hPow (α := WithVal (Rat.padicValuation p)) (↑p : WithVal (Rat.padicValuation p)) n) :
      WithZero (Multiplicative ℤ))
    (exp (-(↑n : ℤ)) : WithZero (Multiplicative ℤ))
x y : WithVal (Rat.padicValuation p)
x' : ℚ := (WithVal.equiv (Rat.padicValuation p) : (a : WithVal (Rat.padicValuation p)) → ℚ) x
hx : x' = (WithVal.equiv (Rat.padicValuation p) : (a : WithVal (Rat.padicValuation p)) → ℚ) x
y' : ℚ := (WithVal.equiv (Rat.padicValuation p) : (a : WithVal (Rat.padicValuation p)) → ℚ) y
hy : y' = (WithVal.equiv (Rat.padicValuation p) : (a : WithVal (Rat.padicValuation p)) → ℚ) y
h : (if x' - y' = 0 then 0 else exp (-padicValRat p (x' - y'))) < exp (-(↑n : ℤ))
pos : ∀ (H : x' - y' = 0), 0 ≤ (HPow.hPow (α := ℚ) (↑p : ℚ) n)⁻¹
⊢ (if x' - y' = 0 then 0 else (HPow.hPow (α := ℚ) (↑p : ℚ) (padicValRat p (x' - y')))⁻¹) ≤
    (HPow.hPow (α := ℚ) (↑p : ℚ) n)⁻¹
have neg : ∀ (H : ¬x' - y' = 0), (HPow.hPow (α := ℚ) (↑p : ℚ) (padicValRat p (x' - y')))⁻¹ ≤ (HPow.hPow (α := ℚ) (↑p : ℚ) n)⁻¹
Tactic: split_ifs with H
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.WithVal (hypothesis)
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
hp0' : LT.lt (α := ℚ) 0 (↑p : ℚ)
hp0 : LT.lt (α := ℝ) 0 (↑p : ℝ)⁻¹
hp1' : LT.lt (α := ℚ) 1 (↑p : ℚ)
hp1 : LT.lt (α := ℝ) (↑p : ℝ)⁻¹ 1
n : ℕ
hn :
  Eq (α := WithZero (Multiplicative ℤ))
    ((Valued.v : (a : WithVal (Rat.padicValuation p)) → WithZero (Multiplicative ℤ))
        (HPow.hPow (α := WithVal (Rat.padicValuation p)) (↑p : WithVal (Rat.padicValuation p)) n) :
      WithZero (Multiplicative ℤ))
    (exp (-(↑n : ℤ)) : WithZero (Multiplicative ℤ))
x y : WithVal (Rat.padicValuation p)
x' : ℚ := (WithVal.equiv (Rat.padicValuation p) : (a : WithVal (Rat.padicValuation p)) → ℚ) x
hx : x' = (WithVal.equiv (Rat.padicValuation p) : (a : WithVal (Rat.padicValuation p)) → ℚ) x
y' : ℚ := (WithVal.equiv (Rat.padicValuation p) : (a : WithVal (Rat.padicValuation p)) → ℚ) y
hy : y' = (WithVal.equiv (Rat.padicValuation p) : (a : WithVal (Rat.padicValuation p)) → ℚ) y
h : (if x' - y' = 0 then 0 else exp (-padicValRat p (x' - y'))) < exp (-(↑n : ℤ))
H : ¬x' - y' = 0
⊢ (HPow.hPow (α := ℚ) (↑p : ℚ) (padicValRat p (x' - y')))⁻¹ ≤ (HPow.hPow (α := ℚ) (↑p : ℚ) n)⁻¹
have h₁ : (↑n : ℤ) < padicValRat p (x' - y')
Tactic: simp only [H, ↓reduceIte, exp_lt_exp, neg_lt_neg_iff] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.WithVal (goal)
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
hp0' : LT.lt (α := ℚ) 0 (↑p : ℚ)
hp0 : LT.lt (α := ℝ) 0 (↑p : ℝ)⁻¹
hp1' : LT.lt (α := ℚ) 1 (↑p : ℚ)
hp1 : LT.lt (α := ℝ) (↑p : ℝ)⁻¹ 1
γ :
  (MonoidWithZeroHom.ValueGroup₀ (F := Valuation (WithVal (Rat.padicValuation p)) (WithZero (Multiplicative ℤ)))
      Valued.v)ˣ
⊢ ∃ (i : ℕ),
    ∀ (x y : WithVal (Rat.padicValuation p)),
      (↑(padicNorm p ((WithVal.equiv (Rat.padicValuation p) : (a : WithVal (Rat.padicValuation p)) → ℚ) (x - y))) : ℝ) ≤
          (HPow.hPow (α := ℝ) (↑p : ℝ) i)⁻¹ →
        (Valuation.restrict Valued.v :
              (a : WithVal (Rat.padicValuation p)) →
                MonoidWithZeroHom.ValueGroup₀
                  (↑Valued.v : WithVal (Rat.padicValuation p) →*₀ WithZero (Multiplicative ℤ)))
            (y - x) <
          (↑γ : MonoidWithZeroHom.ValueGroup₀ Valued.v)
have h : ∀ (x y : WithVal (Rat.padicValuation p)),
  (↑(padicNorm p ((WithVal.equiv (Rat.padicValuation p) : (a : WithVal (Rat.padicValuation p)) → ℚ) (x - y))) : ℝ) ≤
      (HPow.hPow (α := ℝ) (↑p : ℝ)
          (HMul.hMul (α := WithZero (Multiplicative ℤ)) (β := WithZero (Multiplicative ℤ))
                ((embedding : (a : MonoidWithZeroHom.ValueGroup₀ Valued.v) → WithZero (Multiplicative ℤ))
                    (↑γ : MonoidWithZeroHom.ValueGroup₀ Valued.v) :
                  WithZero (Multiplicative ℤ))
                (exp (-1))).log.natAbs)⁻¹ →
    (Valuation.restrict Valued.v :
          (a : WithVal (Rat.padicValuation p)) →
            MonoidWithZeroHom.ValueGroup₀ (↑Valued.v : WithVal (Rat.padicValuation p) →*₀ WithZero (Multiplicative ℤ)))
        (y - x) <
      (↑γ : MonoidWithZeroHom.ValueGroup₀ Valued.v)
Tactic: use (log ((embedding γ.val) * exp (-1))).natAbs
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.WithVal (hypothesis)
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
hp0' : LT.lt (α := ℚ) 0 (↑p : ℚ)
hp0 : LT.lt (α := ℝ) 0 (↑p : ℝ)⁻¹
hp1' : LT.lt (α := ℚ) 1 (↑p : ℚ)
hp1 : LT.lt (α := ℝ) (↑p : ℝ)⁻¹ 1
γ :
  (MonoidWithZeroHom.ValueGroup₀ (F := Valuation (WithVal (Rat.padicValuation p)) (WithZero (Multiplicative ℤ)))
      Valued.v)ˣ
x y : WithVal (Rat.padicValuation p)
h :
  (↑(padicNorm p ((WithVal.equiv (Rat.padicValuation p) : (a : WithVal (Rat.padicValuation p)) → ℚ) (x - y))) : ℝ) ≤
    (HPow.hPow (α := ℝ) (↑p : ℝ)
        (HMul.hMul (α := WithZero (Multiplicative ℤ)) (β := WithZero (Multiplicative ℤ))
              ((embedding : (a : MonoidWithZeroHom.ValueGroup₀ Valued.v) → WithZero (Multiplicative ℤ))
                  (↑γ : MonoidWithZeroHom.ValueGroup₀ Valued.v) :
                WithZero (Multiplicative ℤ))
              (exp (-1))).log.natAbs)⁻¹
⊢ (Valuation.restrict Valued.v :
        (a : WithVal (Rat.padicValuation p)) →
          MonoidWithZeroHom.ValueGroup₀ (↑Valued.v : WithVal (Rat.padicValuation p) →*₀ WithZero (Multiplicative ℤ)))
      (y - x) <
    (↑γ : MonoidWithZeroHom.ValueGroup₀ Valued.v)
have hx : let x' : ℚ := (WithVal.equiv (Rat.padicValuation p) : (a : WithVal (Rat.padicValuation p)) → ℚ) x;
x' = (WithVal.equiv (Rat.padicValuation p) : (a : WithVal (Rat.padicValuation p)) → ℚ) x
Tactic: set x' := (WithVal.equiv (Rat.padicValuation p)) x with hx
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.WithVal (hypothesis)
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
hp0' : LT.lt (α := ℚ) 0 (↑p : ℚ)
hp0 : LT.lt (α := ℝ) 0 (↑p : ℝ)⁻¹
hp1' : LT.lt (α := ℚ) 1 (↑p : ℚ)
hp1 : LT.lt (α := ℝ) (↑p : ℝ)⁻¹ 1
γ :
  (MonoidWithZeroHom.ValueGroup₀ (F := Valuation (WithVal (Rat.padicValuation p)) (WithZero (Multiplicative ℤ)))
      Valued.v)ˣ
x y : WithVal (Rat.padicValuation p)
h :
  (↑(padicNorm p ((WithVal.equiv (Rat.padicValuation p) : (a : WithVal (Rat.padicValuation p)) → ℚ) (x - y))) : ℝ) ≤
    (HPow.hPow (α := ℝ) (↑p : ℝ)
        (HMul.hMul (α := WithZero (Multiplicative ℤ)) (β := WithZero (Multiplicative ℤ))
              ((embedding : (a : MonoidWithZeroHom.ValueGroup₀ Valued.v) → WithZero (Multiplicative ℤ))
                  (↑γ : MonoidWithZeroHom.ValueGroup₀ Valued.v) :
                WithZero (Multiplicative ℤ))
              (exp (-1))).log.natAbs)⁻¹
x' : ℚ := (WithVal.equiv (Rat.padicValuation p) : (a : WithVal (Rat.padicValuation p)) → ℚ) x
hx : x' = (WithVal.equiv (Rat.padicValuation p) : (a : WithVal (Rat.padicValuation p)) → ℚ) x
⊢ (Valuation.restrict Valued.v :
        (a : WithVal (Rat.padicValuation p)) →
          MonoidWithZeroHom.ValueGroup₀ (↑Valued.v : WithVal (Rat.padicValuation p) →*₀ WithZero (Multiplicative ℤ)))
      (y - x) <
    (↑γ : MonoidWithZeroHom.ValueGroup₀ Valued.v)
have hy : let y' : ℚ := (WithVal.equiv (Rat.padicValuation p) : (a : WithVal (Rat.padicValuation p)) → ℚ) y;
y' = (WithVal.equiv (Rat.padicValuation p) : (a : WithVal (Rat.padicValuation p)) → ℚ) y
Tactic: set y' := (WithVal.equiv (Rat.padicValuation p)) y with hy
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.WithVal (goal)
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
hp0' : LT.lt (α := ℚ) 0 (↑p : ℚ)
hp0 : LT.lt (α := ℝ) 0 (↑p : ℝ)⁻¹
hp1' : LT.lt (α := ℚ) 1 (↑p : ℚ)
hp1 : LT.lt (α := ℝ) (↑p : ℝ)⁻¹ 1
γ :
  (MonoidWithZeroHom.ValueGroup₀ (F := Valuation (WithVal (Rat.padicValuation p)) (WithZero (Multiplicative ℤ)))
      Valued.v)ˣ
x y : WithVal (Rat.padicValuation p)
h :
  (↑(padicNorm p ((WithVal.equiv (Rat.padicValuation p) : (a : WithVal (Rat.padicValuation p)) → ℚ) (x - y))) : ℝ) ≤
    (HPow.hPow (α := ℝ) (↑p : ℝ)
        (HMul.hMul (α := WithZero (Multiplicative ℤ)) (β := WithZero (Multiplicative ℤ))
              ((embedding : (a : MonoidWithZeroHom.ValueGroup₀ Valued.v) → WithZero (Multiplicative ℤ))
                  (↑γ : MonoidWithZeroHom.ValueGroup₀ Valued.v) :
                WithZero (Multiplicative ℤ))
              (exp (-1))).log.natAbs)⁻¹
x' : ℚ := (WithVal.equiv (Rat.padicValuation p) : (a : WithVal (Rat.padicValuation p)) → ℚ) x
hx : x' = (WithVal.equiv (Rat.padicValuation p) : (a : WithVal (Rat.padicValuation p)) → ℚ) x
y' : ℚ := (WithVal.equiv (Rat.padicValuation p) : (a : WithVal (Rat.padicValuation p)) → ℚ) y
hy : y' = (WithVal.equiv (Rat.padicValuation p) : (a : WithVal (Rat.padicValuation p)) → ℚ) y
⊢ (Valuation.restrict Valued.v :
        (a : WithVal (Rat.padicValuation p)) →
          MonoidWithZeroHom.ValueGroup₀ (↑Valued.v : WithVal (Rat.padicValuation p) →*₀ WithZero (Multiplicative ℤ)))
      (y - x) <
    (↑γ : MonoidWithZeroHom.ValueGroup₀ Valued.v)
have h₁ : LT.lt (α := WithZero (Multiplicative ℤ))
  ((Valued.v : (a : WithVal (Rat.padicValuation p)) → WithZero (Multiplicative ℤ)) (x - y) :
    WithZero (Multiplicative ℤ))
  ((embedding : (a : MonoidWithZeroHom.ValueGroup₀ Valued.v) → WithZero (Multiplicative ℤ))
      (↑γ : MonoidWithZeroHom.ValueGroup₀ Valued.v) :
    WithZero (Multiplicative ℤ))
Tactic: rw [Valuation.map_sub_swap, Valuation.restrict_lt_iff_lt_embedding]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.WithVal (goal)
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
hp0' : LT.lt (α := ℚ) 0 (↑p : ℚ)
hp0 : LT.lt (α := ℝ) 0 (↑p : ℝ)⁻¹
hp1' : LT.lt (α := ℚ) 1 (↑p : ℚ)
hp1 : LT.lt (α := ℝ) (↑p : ℝ)⁻¹ 1
γ :
  (MonoidWithZeroHom.ValueGroup₀ (F := Valuation (WithVal (Rat.padicValuation p)) (WithZero (Multiplicative ℤ)))
      Valued.v)ˣ
x y : WithVal (Rat.padicValuation p)
h :
  (↑(padicNorm p ((WithVal.equiv (Rat.padicValuation p) : (a : WithVal (Rat.padicValuation p)) → ℚ) (x - y))) : ℝ) ≤
    (HPow.hPow (α := ℝ) (↑p : ℝ)
        (HMul.hMul (α := WithZero (Multiplicative ℤ)) (β := WithZero (Multiplicative ℤ))
              ((embedding : (a : MonoidWithZeroHom.ValueGroup₀ Valued.v) → WithZero (Multiplicative ℤ))
                  (↑γ : MonoidWithZeroHom.ValueGroup₀ Valued.v) :
                WithZero (Multiplicative ℤ))
              (exp (-1))).log.natAbs)⁻¹
x' : ℚ := (WithVal.equiv (Rat.padicValuation p) : (a : WithVal (Rat.padicValuation p)) → ℚ) x
hx : x' = (WithVal.equiv (Rat.padicValuation p) : (a : WithVal (Rat.padicValuation p)) → ℚ) x
y' : ℚ := (WithVal.equiv (Rat.padicValuation p) : (a : WithVal (Rat.padicValuation p)) → ℚ) y
hy : y' = (WithVal.equiv (Rat.padicValuation p) : (a : WithVal (Rat.padicValuation p)) → ℚ) y
⊢ LT.lt (α := WithZero (Multiplicative ℤ))
    ((Valued.v : (a : WithVal (Rat.padicValuation p)) → WithZero (Multiplicative ℤ)) (x - y) :
      WithZero (Multiplicative ℤ))
    ((embedding : (a : MonoidWithZeroHom.ValueGroup₀ Valued.v) → WithZero (Multiplicative ℤ))
        (↑γ : MonoidWithZeroHom.ValueGroup₀ Valued.v) :
      WithZero (Multiplicative ℤ))
have h₁ : LT.lt (α := WithZero (Multiplicative ℤ))
  ((Rat.padicValuation p : (a : ℚ) → WithZero (Multiplicative ℤ)) (x' - y') : WithZero (Multiplicative ℤ))
  ((embedding : (a : MonoidWithZeroHom.ValueGroup₀ Valued.v) → WithZero (Multiplicative ℤ))
      (↑γ : MonoidWithZeroHom.ValueGroup₀ Valued.v) :
    WithZero (Multiplicative ℤ))
Tactic: change Rat.padicValuation p (x' - y') < embedding γ.1
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.WithVal (goal)
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
hp0' : LT.lt (α := ℚ) 0 (↑p : ℚ)
hp0 : LT.lt (α := ℝ) 0 (↑p : ℝ)⁻¹
hp1' : LT.lt (α := ℚ) 1 (↑p : ℚ)
hp1 : LT.lt (α := ℝ) (↑p : ℝ)⁻¹ 1
γ :
  (MonoidWithZeroHom.ValueGroup₀ (F := Valuation (WithVal (Rat.padicValuation p)) (WithZero (Multiplicative ℤ)))
      Valued.v)ˣ
x y : WithVal (Rat.padicValuation p)
h :
  (↑(padicNorm p ((WithVal.equiv (Rat.padicValuation p) : (a : WithVal (Rat.padicValuation p)) → ℚ) (x - y))) : ℝ) ≤
    (HPow.hPow (α := ℝ) (↑p : ℝ)
        (HMul.hMul (α := WithZero (Multiplicative ℤ)) (β := WithZero (Multiplicative ℤ))
              ((embedding : (a : MonoidWithZeroHom.ValueGroup₀ Valued.v) → WithZero (Multiplicative ℤ))
                  (↑γ : MonoidWithZeroHom.ValueGroup₀ Valued.v) :
                WithZero (Multiplicative ℤ))
              (exp (-1))).log.natAbs)⁻¹
x' : ℚ := (WithVal.equiv (Rat.padicValuation p) : (a : WithVal (Rat.padicValuation p)) → ℚ) x
hx : x' = (WithVal.equiv (Rat.padicValuation p) : (a : WithVal (Rat.padicValuation p)) → ℚ) x
y' : ℚ := (WithVal.equiv (Rat.padicValuation p) : (a : WithVal (Rat.padicValuation p)) → ℚ) y
hy : y' = (WithVal.equiv (Rat.padicValuation p) : (a : WithVal (Rat.padicValuation p)) → ℚ) y
⊢ LT.lt (α := WithZero (Multiplicative ℤ))
    ((Rat.padicValuation p : (a : ℚ) → WithZero (Multiplicative ℤ)) (x' - y') : WithZero (Multiplicative ℤ))
    ((embedding : (a : MonoidWithZeroHom.ValueGroup₀ Valued.v) → WithZero (Multiplicative ℤ))
        (↑γ : MonoidWithZeroHom.ValueGroup₀ Valued.v) :
      WithZero (Multiplicative ℤ))
have h₁ : ∀
  (h :
    padicNorm p ((WithVal.equiv (Rat.padicValuation p) : (a : WithVal (Rat.padicValuation p)) → ℚ) (x - y)) ≤
      (↑(p ^
              (HMul.hMul (α := WithZero (Multiplicative ℤ)) (β := WithZero (Multiplicative ℤ))
                    ((embedding : (a : MonoidWithZeroHom.ValueGroup₀ Valued.v) → WithZero (Multiplicative ℤ))
                        (↑γ : MonoidWithZeroHom.ValueGroup₀ Valued.v) :
                      WithZero (Multiplicative ℤ))
                    (exp (-1))).log.natAbs) :
          ℚ)⁻¹),
  let x' : ℚ := (WithVal.equiv (Rat.padicValuation p) : (a : WithVal (Rat.padicValuation p)) → ℚ) x;
  ∀ (hx : x' = (WithVal.equiv (Rat.padicValuation p) : (a : WithVal (Rat.padicValuation p)) → ℚ) x),
    let y' : ℚ := (WithVal.equiv (Rat.padicValuation p) : (a : WithVal (Rat.padicValuation p)) → ℚ) y;
    ∀ (hy : y' = (WithVal.equiv (Rat.padicValuation p) : (a : WithVal (Rat.padicValuation p)) → ℚ) y),
      LT.lt (α := WithZero (Multiplicative ℤ))
        ((Rat.padicValuation p : (a : ℚ) → WithZero (Multiplicative ℤ)) (x' - y') : WithZero (Multiplicative ℤ))
        ((embedding : (a : MonoidWithZeroHom.ValueGroup₀ Valued.v) → WithZero (Multiplicative ℤ))
            (↑γ : MonoidWithZeroHom.ValueGroup₀ Valued.v) :
          WithZero (Multiplicative ℤ))
Tactic: rw [← Nat.cast_pow, ← Rat.cast_natCast, ← Rat.cast_inv_of_ne_zero, Rat.cast_le] at h
Cleared hypotheses: h, x', hx, y', hy
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.WithVal (hypothesis)
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
hp0' : LT.lt (α := ℚ) 0 (↑p : ℚ)
hp0 : LT.lt (α := ℝ) 0 (↑p : ℝ)⁻¹
hp1' : LT.lt (α := ℚ) 1 (↑p : ℚ)
hp1 : LT.lt (α := ℝ) (↑p : ℝ)⁻¹ 1
γ :
  (MonoidWithZeroHom.ValueGroup₀ (F := Valuation (WithVal (Rat.padicValuation p)) (WithZero (Multiplicative ℤ)))
      Valued.v)ˣ
x y : WithVal (Rat.padicValuation p)
h :
  padicNorm p ((WithVal.equiv (Rat.padicValuation p) : (a : WithVal (Rat.padicValuation p)) → ℚ) (x - y)) ≤
    (↑(p ^
            (HMul.hMul (α := WithZero (Multiplicative ℤ)) (β := WithZero (Multiplicative ℤ))
                  ((embedding : (a : MonoidWithZeroHom.ValueGroup₀ Valued.v) → WithZero (Multiplicative ℤ))
                      (↑γ : MonoidWithZeroHom.ValueGroup₀ Valued.v) :
                    WithZero (Multiplicative ℤ))
                  (exp (-1))).log.natAbs) :
        ℚ)⁻¹
x' : ℚ := (WithVal.equiv (Rat.padicValuation p) : (a : WithVal (Rat.padicValuation p)) → ℚ) x
hx : x' = (WithVal.equiv (Rat.padicValuation p) : (a : WithVal (Rat.padicValuation p)) → ℚ) x
y' : ℚ := (WithVal.equiv (Rat.padicValuation p) : (a : WithVal (Rat.padicValuation p)) → ℚ) y
hy : y' = (WithVal.equiv (Rat.padicValuation p) : (a : WithVal (Rat.padicValuation p)) → ℚ) y
⊢ LT.lt (α := WithZero (Multiplicative ℤ))
    ((Rat.padicValuation p : (a : ℚ) → WithZero (Multiplicative ℤ)) (x' - y') : WithZero (Multiplicative ℤ))
    ((embedding : (a : MonoidWithZeroHom.ValueGroup₀ Valued.v) → WithZero (Multiplicative ℤ))
        (↑γ : MonoidWithZeroHom.ValueGroup₀ Valued.v) :
      WithZero (Multiplicative ℤ))
have h₁ : padicNorm p (x' - y') ≤
  (↑(p ^
          (HMul.hMul (α := WithZero (Multiplicative ℤ)) (β := WithZero (Multiplicative ℤ))
                ((embedding : (a : MonoidWithZeroHom.ValueGroup₀ Valued.v) → WithZero (Multiplicative ℤ))
                    (↑γ : MonoidWithZeroHom.ValueGroup₀ Valued.v) :
                  WithZero (Multiplicative ℤ))
                (exp (-1))).log.natAbs) :
      ℚ)⁻¹
Tactic: change padicNorm p (x' - y') ≤ _ at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.WithVal (hypothesis)
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
hp0' : LT.lt (α := ℚ) 0 (↑p : ℚ)
hp0 : LT.lt (α := ℝ) 0 (↑p : ℝ)⁻¹
hp1' : LT.lt (α := ℚ) 1 (↑p : ℚ)
hp1 : LT.lt (α := ℝ) (↑p : ℝ)⁻¹ 1
γ :
  (MonoidWithZeroHom.ValueGroup₀ (F := Valuation (WithVal (Rat.padicValuation p)) (WithZero (Multiplicative ℤ)))
      Valued.v)ˣ
x y : WithVal (Rat.padicValuation p)
x' : ℚ := (WithVal.equiv (Rat.padicValuation p) : (a : WithVal (Rat.padicValuation p)) → ℚ) x
hx : x' = (WithVal.equiv (Rat.padicValuation p) : (a : WithVal (Rat.padicValuation p)) → ℚ) x
y' : ℚ := (WithVal.equiv (Rat.padicValuation p) : (a : WithVal (Rat.padicValuation p)) → ℚ) y
hy : y' = (WithVal.equiv (Rat.padicValuation p) : (a : WithVal (Rat.padicValuation p)) → ℚ) y
h :
  padicNorm p (x' - y') ≤
    (↑(p ^
            (HMul.hMul (α := WithZero (Multiplicative ℤ)) (β := WithZero (Multiplicative ℤ))
                  ((embedding : (a : MonoidWithZeroHom.ValueGroup₀ Valued.v) → WithZero (Multiplicative ℤ))
                      (↑γ : MonoidWithZeroHom.ValueGroup₀ Valued.v) :
                    WithZero (Multiplicative ℤ))
                  (exp (-1))).log.natAbs) :
        ℚ)⁻¹
⊢ LT.lt (α := WithZero (Multiplicative ℤ))
    ((Rat.padicValuation p : (a : ℚ) → WithZero (Multiplicative ℤ)) (x' - y') : WithZero (Multiplicative ℤ))
    ((embedding : (a : MonoidWithZeroHom.ValueGroup₀ Valued.v) → WithZero (Multiplicative ℤ))
        (↑γ : MonoidWithZeroHom.ValueGroup₀ Valued.v) :
      WithZero (Multiplicative ℤ))
have h₁ : (if x' - y' = 0 then 0 else (HPow.hPow (α := ℚ) (↑p : ℚ) (padicValRat p (x' - y')))⁻¹) ≤
  (HPow.hPow (α := ℚ) (↑p : ℚ)
      (HMul.hMul (α := WithZero (Multiplicative ℤ)) (β := WithZero (Multiplicative ℤ))
            ((embedding : (a : MonoidWithZeroHom.ValueGroup₀ Valued.v) → WithZero (Multiplicative ℤ))
                (↑γ : MonoidWithZeroHom.ValueGroup₀ Valued.v) :
              WithZero (Multiplicative ℤ))
            (exp (-1))).log.natAbs)⁻¹
Tactic: simp only [Rat.padicValuation, Valuation.coe_mk, MonoidWithZeroHom.coe_mk, ZeroHom.coe_mk,
        padicNorm, zpow_neg, Nat.cast_pow] at h ⊢
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.WithVal (goal)
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
hp0' : LT.lt (α := ℚ) 0 (↑p : ℚ)
hp0 : LT.lt (α := ℝ) 0 (↑p : ℝ)⁻¹
hp1' : LT.lt (α := ℚ) 1 (↑p : ℚ)
hp1 : LT.lt (α := ℝ) (↑p : ℝ)⁻¹ 1
γ :
  (MonoidWithZeroHom.ValueGroup₀ (F := Valuation (WithVal (Rat.padicValuation p)) (WithZero (Multiplicative ℤ)))
      Valued.v)ˣ
x y : WithVal (Rat.padicValuation p)
x' : ℚ := (WithVal.equiv (Rat.padicValuation p) : (a : WithVal (Rat.padicValuation p)) → ℚ) x
hx : x' = (WithVal.equiv (Rat.padicValuation p) : (a : WithVal (Rat.padicValuation p)) → ℚ) x
y' : ℚ := (WithVal.equiv (Rat.padicValuation p) : (a : WithVal (Rat.padicValuation p)) → ℚ) y
hy : y' = (WithVal.equiv (Rat.padicValuation p) : (a : WithVal (Rat.padicValuation p)) → ℚ) y
h :
  (if x' - y' = 0 then 0 else (HPow.hPow (α := ℚ) (↑p : ℚ) (padicValRat p (x' - y')))⁻¹) ≤
    (HPow.hPow (α := ℚ) (↑p : ℚ)
        (HMul.hMul (α := WithZero (Multiplicative ℤ)) (β := WithZero (Multiplicative ℤ))
              ((embedding : (a : MonoidWithZeroHom.ValueGroup₀ Valued.v) → WithZero (Multiplicative ℤ))
                  (↑γ : MonoidWithZeroHom.ValueGroup₀ Valued.v) :
                WithZero (Multiplicative ℤ))
              (exp (-1))).log.natAbs)⁻¹
⊢ (if x' - y' = 0 then 0 else exp (-padicValRat p (x' - y'))) <
    (embedding : (a : MonoidWithZeroHom.ValueGroup₀ Valued.v) → WithZero (Multiplicative ℤ))
      (↑γ : MonoidWithZeroHom.ValueGroup₀ Valued.v)
have pos : ∀ (H : x' - y' = 0),
  LT.lt (α := WithZero (Multiplicative ℤ)) (0 : WithZero (Multiplicative ℤ))
    ((embedding : (a : MonoidWithZeroHom.ValueGroup₀ Valued.v) → WithZero (Multiplicative ℤ))
        (↑γ : MonoidWithZeroHom.ValueGroup₀ Valued.v) :
      WithZero (Multiplicative ℤ))
Tactic: split_ifs with H
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.WithVal (goal)
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
hp0' : LT.lt (α := ℚ) 0 (↑p : ℚ)
hp0 : LT.lt (α := ℝ) 0 (↑p : ℝ)⁻¹
hp1' : LT.lt (α := ℚ) 1 (↑p : ℚ)
hp1 : LT.lt (α := ℝ) (↑p : ℝ)⁻¹ 1
γ :
  (MonoidWithZeroHom.ValueGroup₀ (F := Valuation (WithVal (Rat.padicValuation p)) (WithZero (Multiplicative ℤ)))
      Valued.v)ˣ
x y : WithVal (Rat.padicValuation p)
x' : ℚ := (WithVal.equiv (Rat.padicValuation p) : (a : WithVal (Rat.padicValuation p)) → ℚ) x
hx : x' = (WithVal.equiv (Rat.padicValuation p) : (a : WithVal (Rat.padicValuation p)) → ℚ) x
y' : ℚ := (WithVal.equiv (Rat.padicValuation p) : (a : WithVal (Rat.padicValuation p)) → ℚ) y
hy : y' = (WithVal.equiv (Rat.padicValuation p) : (a : WithVal (Rat.padicValuation p)) → ℚ) y
h :
  (if x' - y' = 0 then 0 else (HPow.hPow (α := ℚ) (↑p : ℚ) (padicValRat p (x' - y')))⁻¹) ≤
    (HPow.hPow (α := ℚ) (↑p : ℚ)
        (HMul.hMul (α := WithZero (Multiplicative ℤ)) (β := WithZero (Multiplicative ℤ))
              ((embedding : (a : MonoidWithZeroHom.ValueGroup₀ Valued.v) → WithZero (Multiplicative ℤ))
                  (↑γ : MonoidWithZeroHom.ValueGroup₀ Valued.v) :
                WithZero (Multiplicative ℤ))
              (exp (-1))).log.natAbs)⁻¹
pos :
  ∀ (H : x' - y' = 0),
    LT.lt (α := WithZero (Multiplicative ℤ)) (0 : WithZero (Multiplicative ℤ))
      ((embedding : (a : MonoidWithZeroHom.ValueGroup₀ Valued.v) → WithZero (Multiplicative ℤ))
          (↑γ : MonoidWithZeroHom.ValueGroup₀ Valued.v) :
        WithZero (Multiplicative ℤ))
⊢ (if x' - y' = 0 then 0 else exp (-padicValRat p (x' - y'))) <
    (embedding : (a : MonoidWithZeroHom.ValueGroup₀ Valued.v) → WithZero (Multiplicative ℤ))
      (↑γ : MonoidWithZeroHom.ValueGroup₀ Valued.v)
have neg : ∀ (H : ¬x' - y' = 0),
  exp (-padicValRat p (x' - y')) <
    (embedding : (a : MonoidWithZeroHom.ValueGroup₀ Valued.v) → WithZero (Multiplicative ℤ))
      (↑γ : MonoidWithZeroHom.ValueGroup₀ Valued.v)
Tactic: split_ifs with H