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
⊢ (∀ (i : ℕ),
      ∃ (j :
        (MonoidWithZeroHom.ValueGroup₀ (F := Valuation (WithVal (Rat.padicValuation p)) (WithZero (Multiplicative ℤ)))
            Valued.v)ˣ),
        ∀ (x y : WithVal (Rat.padicValuation p)),
          (Valuation.restrict Valued.v :
                  (a : WithVal (Rat.padicValuation p)) →
                    MonoidWithZeroHom.ValueGroup₀
                      (↑Valued.v : WithVal (Rat.padicValuation p) →*₀ WithZero (Multiplicative ℤ)))
                (y - x) <
              (↑j : MonoidWithZeroHom.ValueGroup₀ Valued.v) →
            (↑(padicNorm p
                    ((WithVal.equiv (Rat.padicValuation p) : (a : WithVal (Rat.padicValuation p)) → ℚ) (x - y))) :
                ℝ) ≤
              (HPow.hPow (α := ℝ) (↑p : ℝ) i)⁻¹) ∧
    ∀
      (j :
        (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) <
              (↑j : MonoidWithZeroHom.ValueGroup₀ Valued.v)
have left : ∀ (i : ℕ),
  ∃ (j :
    (MonoidWithZeroHom.ValueGroup₀ (F := Valuation (WithVal (Rat.padicValuation p)) (WithZero (Multiplicative ℤ)))
        Valued.v)ˣ),
    ∀ (x y : WithVal (Rat.padicValuation p)),
      (Valuation.restrict Valued.v :
              (a : WithVal (Rat.padicValuation p)) →
                MonoidWithZeroHom.ValueGroup₀
                  (↑Valued.v : WithVal (Rat.padicValuation p) →*₀ WithZero (Multiplicative ℤ)))
            (y - x) <
          (↑j : MonoidWithZeroHom.ValueGroup₀ Valued.v) →
        (↑(padicNorm p ((WithVal.equiv (Rat.padicValuation p) : (a : WithVal (Rat.padicValuation p)) → ℚ) (x - y))) :
            ℝ) ≤
          (HPow.hPow (α := ℝ) (↑p : ℝ) i)⁻¹
Tactic: constructor
-- 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 : ℕ
⊢ ∃ (j :
    (MonoidWithZeroHom.ValueGroup₀ (F := Valuation (WithVal (Rat.padicValuation p)) (WithZero (Multiplicative ℤ)))
        Valued.v)ˣ),
    ∀ (x y : WithVal (Rat.padicValuation p)),
      (Valuation.restrict Valued.v :
              (a : WithVal (Rat.padicValuation p)) →
                MonoidWithZeroHom.ValueGroup₀
                  (↑Valued.v : WithVal (Rat.padicValuation p) →*₀ WithZero (Multiplicative ℤ)))
            (y - x) <
          (↑j : MonoidWithZeroHom.ValueGroup₀ Valued.v) →
        (↑(padicNorm p ((WithVal.equiv (Rat.padicValuation p) : (a : WithVal (Rat.padicValuation p)) → ℚ) (x - y))) :
            ℝ) ≤
          (HPow.hPow (α := ℝ) (↑p : ℝ) n)⁻¹
have 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 ℤ))
Tactic: have hn : Valued.v (R := (WithVal (Rat.padicValuation p))) (p ^ n) =
      exp (-n : ℤ) := by
      simp only [← WithVal.val_apply_equiv, map_pow, map_natCast, Rat.padicValuation_self,
        Int.reduceNeg, exp_neg, inv_pow, ← exp_nsmul, nsmul_eq_mul, mul_one]
-- 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 ℤ))
⊢ Ne (α :=
    MonoidWithZeroHom.ValueGroup₀ (F := Valuation (WithVal (Rat.padicValuation p)) (WithZero (Multiplicative ℤ)))
      Valued.v)
    ((Valuation.restrict Valued.v :
          (a : WithVal (Rat.padicValuation p)) →
            MonoidWithZeroHom.ValueGroup₀ (↑Valued.v : WithVal (Rat.padicValuation p) →*₀ WithZero (Multiplicative ℤ)))
        (HPow.hPow (α := WithVal (Rat.padicValuation p)) (↑p : WithVal (Rat.padicValuation p)) n) :
      MonoidWithZeroHom.ValueGroup₀ (F := WithVal (Rat.padicValuation p) →*₀ WithZero (Multiplicative ℤ))
        (↑Valued.v : WithVal (Rat.padicValuation p) →*₀ WithZero (Multiplicative ℤ)))
    (0 :
      MonoidWithZeroHom.ValueGroup₀ (F := Valuation (WithVal (Rat.padicValuation p)) (WithZero (Multiplicative ℤ)))
        Valued.v)
have rw : ¬Eq (α := WithZero (Multiplicative ℤ)) (exp (-(↑n : ℤ))) 0
Tactic: rw [ne_eq, Valuation.restrict_def, restrict₀_eq_zero_iff, hn]
-- 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 ℤ))
⊢ ∃ (j :
    (MonoidWithZeroHom.ValueGroup₀ (F := Valuation (WithVal (Rat.padicValuation p)) (WithZero (Multiplicative ℤ)))
        Valued.v)ˣ),
    ∀ (x y : WithVal (Rat.padicValuation p)),
      (Valuation.restrict Valued.v :
              (a : WithVal (Rat.padicValuation p)) →
                MonoidWithZeroHom.ValueGroup₀
                  (↑Valued.v : WithVal (Rat.padicValuation p) →*₀ WithZero (Multiplicative ℤ)))
            (y - x) <
          (↑j : MonoidWithZeroHom.ValueGroup₀ Valued.v) →
        (↑(padicNorm p ((WithVal.equiv (Rat.padicValuation p) : (a : WithVal (Rat.padicValuation p)) → ℚ) (x - y))) :
            ℝ) ≤
          (HPow.hPow (α := ℝ) (↑p : ℝ) n)⁻¹
have h : ∀ (x y : WithVal (Rat.padicValuation p)),
  LT.lt (α :=
      MonoidWithZeroHom.ValueGroup₀ (F := WithVal (Rat.padicValuation p) →*₀ WithZero (Multiplicative ℤ))
        (↑Valued.v : WithVal (Rat.padicValuation p) →*₀ WithZero (Multiplicative ℤ)))
      ((Valuation.restrict Valued.v :
            (a : WithVal (Rat.padicValuation p)) →
              MonoidWithZeroHom.ValueGroup₀
                (↑Valued.v : WithVal (Rat.padicValuation p) →*₀ WithZero (Multiplicative ℤ)))
          (y - x) :
        MonoidWithZeroHom.ValueGroup₀ (F := WithVal (Rat.padicValuation p) →*₀ WithZero (Multiplicative ℤ))
          (↑Valued.v : WithVal (Rat.padicValuation p) →*₀ WithZero (Multiplicative ℤ)))
      ((↑(Units.mk0
              ((Valuation.restrict Valued.v :
                  (a : WithVal (Rat.padicValuation p)) →
                    MonoidWithZeroHom.ValueGroup₀
                      (↑Valued.v : WithVal (Rat.padicValuation p) →*₀ WithZero (Multiplicative ℤ)))
                (HPow.hPow (α := WithVal (Rat.padicValuation p)) (↑p : WithVal (Rat.padicValuation p)) n))
              sorry) :
          MonoidWithZeroHom.ValueGroup₀ (F := Valuation (WithVal (Rat.padicValuation p)) (WithZero (Multiplicative ℤ)))
            Valued.v) :
        MonoidWithZeroHom.ValueGroup₀ (F := Valuation (WithVal (Rat.padicValuation p)) (WithZero (Multiplicative ℤ)))
          Valued.v) →
    (↑(padicNorm p ((WithVal.equiv (Rat.padicValuation p) : (a : WithVal (Rat.padicValuation p)) → ℚ) (x - y))) : ℝ) ≤
      (HPow.hPow (α := ℝ) (↑p : ℝ) n)⁻¹
Tactic: use Units.mk0 (Valued.v.restrict (p ^ n)) (by
      rw [ne_eq, Valuation.restrict_def, restrict₀_eq_zero_iff, hn]; simp)
-- 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)
h :
  LT.lt (α :=
    MonoidWithZeroHom.ValueGroup₀ (F := WithVal (Rat.padicValuation p) →*₀ WithZero (Multiplicative ℤ))
      (↑Valued.v : WithVal (Rat.padicValuation p) →*₀ WithZero (Multiplicative ℤ)))
    ((Valuation.restrict Valued.v :
          (a : WithVal (Rat.padicValuation p)) →
            MonoidWithZeroHom.ValueGroup₀ (↑Valued.v : WithVal (Rat.padicValuation p) →*₀ WithZero (Multiplicative ℤ)))
        (y - x) :
      MonoidWithZeroHom.ValueGroup₀ (F := WithVal (Rat.padicValuation p) →*₀ WithZero (Multiplicative ℤ))
        (↑Valued.v : WithVal (Rat.padicValuation p) →*₀ WithZero (Multiplicative ℤ)))
    ((↑(Units.mk0
            ((Valuation.restrict Valued.v :
                (a : WithVal (Rat.padicValuation p)) →
                  MonoidWithZeroHom.ValueGroup₀
                    (↑Valued.v : WithVal (Rat.padicValuation p) →*₀ WithZero (Multiplicative ℤ)))
              (HPow.hPow (α := WithVal (Rat.padicValuation p)) (↑p : WithVal (Rat.padicValuation p)) n))
            ⋯) :
        MonoidWithZeroHom.ValueGroup₀ (F := Valuation (WithVal (Rat.padicValuation p)) (WithZero (Multiplicative ℤ)))
          Valued.v) :
      MonoidWithZeroHom.ValueGroup₀ (F := Valuation (WithVal (Rat.padicValuation p)) (WithZero (Multiplicative ℤ)))
        Valued.v)
⊢ (↑(padicNorm p ((WithVal.equiv (Rat.padicValuation p) : (a : WithVal (Rat.padicValuation p)) → ℚ) (x - y))) : ℝ) ≤
    (HPow.hPow (α := ℝ) (↑p : ℝ) n)⁻¹
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
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)
h :
  LT.lt (α :=
    MonoidWithZeroHom.ValueGroup₀ (F := WithVal (Rat.padicValuation p) →*₀ WithZero (Multiplicative ℤ))
      (↑Valued.v : WithVal (Rat.padicValuation p) →*₀ WithZero (Multiplicative ℤ)))
    ((Valuation.restrict Valued.v :
          (a : WithVal (Rat.padicValuation p)) →
            MonoidWithZeroHom.ValueGroup₀ (↑Valued.v : WithVal (Rat.padicValuation p) →*₀ WithZero (Multiplicative ℤ)))
        (y - x) :
      MonoidWithZeroHom.ValueGroup₀ (F := WithVal (Rat.padicValuation p) →*₀ WithZero (Multiplicative ℤ))
        (↑Valued.v : WithVal (Rat.padicValuation p) →*₀ WithZero (Multiplicative ℤ)))
    ((↑(Units.mk0
            ((Valuation.restrict Valued.v :
                (a : WithVal (Rat.padicValuation p)) →
                  MonoidWithZeroHom.ValueGroup₀
                    (↑Valued.v : WithVal (Rat.padicValuation p) →*₀ WithZero (Multiplicative ℤ)))
              (HPow.hPow (α := WithVal (Rat.padicValuation p)) (↑p : WithVal (Rat.padicValuation p)) n))
            ⋯) :
        MonoidWithZeroHom.ValueGroup₀ (F := Valuation (WithVal (Rat.padicValuation p)) (WithZero (Multiplicative ℤ)))
          Valued.v) :
      MonoidWithZeroHom.ValueGroup₀ (F := Valuation (WithVal (Rat.padicValuation p)) (WithZero (Multiplicative ℤ)))
        Valued.v)
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
⊢ (↑(padicNorm p ((WithVal.equiv (Rat.padicValuation p) : (a : WithVal (Rat.padicValuation p)) → ℚ) (x - y))) : ℝ) ≤
    (HPow.hPow (α := ℝ) (↑p : ℝ) n)⁻¹
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 (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)
h :
  LT.lt (α :=
    MonoidWithZeroHom.ValueGroup₀ (F := WithVal (Rat.padicValuation p) →*₀ WithZero (Multiplicative ℤ))
      (↑Valued.v : WithVal (Rat.padicValuation p) →*₀ WithZero (Multiplicative ℤ)))
    ((Valuation.restrict Valued.v :
          (a : WithVal (Rat.padicValuation p)) →
            MonoidWithZeroHom.ValueGroup₀ (↑Valued.v : WithVal (Rat.padicValuation p) →*₀ WithZero (Multiplicative ℤ)))
        (y - x) :
      MonoidWithZeroHom.ValueGroup₀ (F := WithVal (Rat.padicValuation p) →*₀ WithZero (Multiplicative ℤ))
        (↑Valued.v : WithVal (Rat.padicValuation p) →*₀ WithZero (Multiplicative ℤ)))
    ((↑(Units.mk0
            ((Valuation.restrict Valued.v :
                (a : WithVal (Rat.padicValuation p)) →
                  MonoidWithZeroHom.ValueGroup₀
                    (↑Valued.v : WithVal (Rat.padicValuation p) →*₀ WithZero (Multiplicative ℤ)))
              (HPow.hPow (α := WithVal (Rat.padicValuation p)) (↑p : WithVal (Rat.padicValuation p)) n))
            ⋯) :
        MonoidWithZeroHom.ValueGroup₀ (F := Valuation (WithVal (Rat.padicValuation p)) (WithZero (Multiplicative ℤ)))
          Valued.v) :
      MonoidWithZeroHom.ValueGroup₀ (F := Valuation (WithVal (Rat.padicValuation p)) (WithZero (Multiplicative ℤ)))
        Valued.v)
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
⊢ (↑(padicNorm p ((WithVal.equiv (Rat.padicValuation p) : (a : WithVal (Rat.padicValuation p)) → ℚ) (x - y))) : ℝ) ≤
    (HPow.hPow (α := ℝ) (↑p : ℝ) n)⁻¹
have h₁ : LT.lt (α := WithZero (Multiplicative ℤ))
  ((Valued.v : (a : WithVal (Rat.padicValuation p)) → WithZero (Multiplicative ℤ)) (x - y) :
    WithZero (Multiplicative ℤ))
  (exp (-(↑n : ℤ)) : WithZero (Multiplicative ℤ))
Tactic: rw [Valuation.map_sub_swap, Units.val_mk0, Valuation.restrict_lt_iff, hn] 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
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)
h :
  LT.lt (α := WithZero (Multiplicative ℤ))
    ((Valued.v : (a : WithVal (Rat.padicValuation p)) → WithZero (Multiplicative ℤ)) (x - y) :
      WithZero (Multiplicative ℤ))
    (exp (-(↑n : ℤ)) : WithZero (Multiplicative ℤ))
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
⊢ (↑(padicNorm p ((WithVal.equiv (Rat.padicValuation p) : (a : WithVal (Rat.padicValuation p)) → ℚ) (x - y))) : ℝ) ≤
    (HPow.hPow (α := ℝ) (↑p : ℝ) n)⁻¹
have h₁ : LT.lt (α := WithZero (Multiplicative ℤ))
  ((Rat.padicValuation p : (a : ℚ) → WithZero (Multiplicative ℤ)) (x' - y') : WithZero (Multiplicative ℤ))
  (exp (-(↑n : ℤ)) : WithZero (Multiplicative ℤ))
Tactic: change Rat.padicValuation p (x' - y') < exp _ 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
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 :
  LT.lt (α := WithZero (Multiplicative ℤ))
    ((Rat.padicValuation p : (a : ℚ) → WithZero (Multiplicative ℤ)) (x' - y') : WithZero (Multiplicative ℤ))
    (exp (-(↑n : ℤ)) : WithZero (Multiplicative ℤ))
⊢ (↑(padicNorm p ((WithVal.equiv (Rat.padicValuation p) : (a : WithVal (Rat.padicValuation p)) → ℚ) (x - y))) : ℝ) ≤
    (HPow.hPow (α := ℝ) (↑p : ℝ) n)⁻¹
have h₁ : padicNorm p ((WithVal.equiv (Rat.padicValuation p) : (a : WithVal (Rat.padicValuation p)) → ℚ) (x - y)) ≤
  (↑(p ^ n) : ℚ)⁻¹
Tactic: rw [← Nat.cast_pow, ← Rat.cast_natCast, ← Rat.cast_inv_of_ne_zero, Rat.cast_le]
-- 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 :
  LT.lt (α := WithZero (Multiplicative ℤ))
    ((Rat.padicValuation p : (a : ℚ) → WithZero (Multiplicative ℤ)) (x' - y') : WithZero (Multiplicative ℤ))
    (exp (-(↑n : ℤ)) : WithZero (Multiplicative ℤ))
h₁ :
  padicNorm p ((WithVal.equiv (Rat.padicValuation p) : (a : WithVal (Rat.padicValuation p)) → ℚ) (x - y)) ≤
    (↑(p ^ n) : ℚ)⁻¹
⊢ (↑(padicNorm p ((WithVal.equiv (Rat.padicValuation p) : (a : WithVal (Rat.padicValuation p)) → ℚ) (x - y))) : ℝ) ≤
    (HPow.hPow (α := ℝ) (↑p : ℝ) n)⁻¹
have h₂ : Ne (α := ℝ) (↑(Rat.num (↑(p ^ n) : ℚ)) : ℝ) 0
Tactic: rw [← Nat.cast_pow, ← Rat.cast_natCast, ← Rat.cast_inv_of_ne_zero, Rat.cast_le]
-- 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 :
  LT.lt (α := WithZero (Multiplicative ℤ))
    ((Rat.padicValuation p : (a : ℚ) → WithZero (Multiplicative ℤ)) (x' - y') : WithZero (Multiplicative ℤ))
    (exp (-(↑n : ℤ)) : WithZero (Multiplicative ℤ))
⊢ padicNorm p ((WithVal.equiv (Rat.padicValuation p) : (a : WithVal (Rat.padicValuation p)) → ℚ) (x - y)) ≤
    (↑(p ^ n) : ℚ)⁻¹
have h₁ : padicNorm p (x' - y') ≤ (↑(p ^ n) : ℚ)⁻¹
Tactic: rw [map_sub, ← hx, ← 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
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 :
  LT.lt (α := WithZero (Multiplicative ℤ))
    ((Rat.padicValuation p : (a : ℚ) → WithZero (Multiplicative ℤ)) (x' - y') : WithZero (Multiplicative ℤ))
    (exp (-(↑n : ℤ)) : WithZero (Multiplicative ℤ))
⊢ padicNorm p (x' - y') ≤ (↑(p ^ n) : ℚ)⁻¹
have h₁ : (if x' - y' = 0 then 0 else (HPow.hPow (α := ℚ) (↑p : ℚ) (padicValRat p (x' - y')))⁻¹) ≤
  (HPow.hPow (α := ℚ) (↑p : ℚ) n)⁻¹
Tactic: simp only [Rat.padicValuation, Valuation.coe_mk, MonoidWithZeroHom.coe_mk, ZeroHom.coe_mk,
        padicNorm, zpow_neg, Nat.cast_pow] at h ⊢