awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.Padics.WithVal
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
⊢ 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

Premises used: Valuation.map_sub_swap, Valuation.restrict_lt_iff, Units.val_mk0
-- Module: Mathlib.NumberTheory.Padics.WithVal
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
h₁ :
  LT.lt (α := WithZero (Multiplicative ℤ))
    ((Valued.v : (a : WithVal (Rat.padicValuation p)) → WithZero (Multiplicative ℤ)) (x - y) :
      WithZero (Multiplicative ℤ))
    (exp (-(↑n : ℤ)) : WithZero (Multiplicative ℤ))
⊢ 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:
rw [Valuation.map_sub_swap, Units.val_mk0, Valuation.restrict_lt_iff, hn] at h

Premises used: Valuation.map_sub_swap, Valuation.restrict_lt_iff, Units.val_mk0
-- Module: Mathlib.NumberTheory.Padics.WithVal
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
h₁ :
  LT.lt (α := WithZero (Multiplicative ℤ))
    ((Valued.v : (a : WithVal (Rat.padicValuation p)) → WithZero (Multiplicative ℤ)) (x - y) :
      WithZero (Multiplicative ℤ))
    (exp (-(↑n : ℤ)) : WithZero (Multiplicative ℤ))
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
⊢ 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:
rw [Valuation.map_sub_swap, Units.val_mk0, Valuation.restrict_lt_iff, hn] at h

Premises used: Valuation.map_sub_swap, Valuation.restrict_lt_iff, Units.val_mk0
-- Module: Mathlib.NumberTheory.Padics.WithVal
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
⊢ 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

Premises used: HSub.hSub, WithZero.exp, Rat.padicValuation, DFunLike.coe
-- Module: Mathlib.NumberTheory.Padics.WithVal
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) : ℚ)⁻¹
h₂ : Ne (α := ℝ) (↑(Rat.num (↑(p ^ n) : ℚ)) : ℝ) 0
⊢ (↑(padicNorm p ((WithVal.equiv (Rat.padicValuation p) : (a : WithVal (Rat.padicValuation p)) → ℚ) (x - y))) : ℝ) ≤
    (HPow.hPow (α := ℝ) (↑p : ℝ) n)⁻¹

Tactic:
rw [← Nat.cast_pow, ← Rat.cast_natCast, ← Rat.cast_inv_of_ne_zero, Rat.cast_le]

Premises used: Rat.cast_inv_of_ne_zero, Rat.cast_natCast, Nat.cast_pow, Rat.cast_le
-- Module: Mathlib.NumberTheory.Padics.WithVal
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 (x' - y') ≤ (↑(p ^ n) : ℚ)⁻¹
⊢ padicNorm p ((WithVal.equiv (Rat.padicValuation p) : (a : WithVal (Rat.padicValuation p)) → ℚ) (x - y)) ≤
    (↑(p ^ n) : ℚ)⁻¹

Tactic:
rw [map_sub, ← hx, ← hy]

Premises used: map_sub
-- Module: Mathlib.NumberTheory.Padics.WithVal
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₁ :
  (if x' - y' = 0 then 0 else (HPow.hPow (α := ℚ) (↑p : ℚ) (padicValRat p (x' - y')))⁻¹) ≤
    (HPow.hPow (α := ℚ) (↑p : ℚ) n)⁻¹
⊢ padicNorm p (x' - y') ≤ (↑(p ^ n) : ℚ)⁻¹

Tactic:
simp only [Rat.padicValuation, Valuation.coe_mk, MonoidWithZeroHom.coe_mk, ZeroHom.coe_mk,
        padicNorm, zpow_neg, Nat.cast_pow] at h ⊢

Premises used: MonoidWithZeroHom.coe_mk, ZeroHom.coe_mk, zpow_neg, Rat.padicValuation, Nat.cast_pow, padicNorm, Valuation.coe_mk
-- Module: Mathlib.NumberTheory.Padics.WithVal
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)⁻¹
neg :
  ∀ (H : ¬x' - y' = 0), (HPow.hPow (α := ℚ) (↑p : ℚ) (padicValRat p (x' - y')))⁻¹ ≤ (HPow.hPow (α := ℚ) (↑p : ℚ) n)⁻¹
⊢ (if x' - y' = 0 then 0 else (HPow.hPow (α := ℚ) (↑p : ℚ) (padicValRat p (x' - y')))⁻¹) ≤
    (HPow.hPow (α := ℚ) (↑p : ℚ) n)⁻¹

Tactic:
split_ifs with H
-- Module: Mathlib.NumberTheory.Padics.WithVal
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
⊢ 0 ≤ (HPow.hPow (α := ℚ) (↑p : ℚ) n)⁻¹

Tactic:
simp
-- Module: Mathlib.NumberTheory.Padics.WithVal
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
⊢ (↑n : ℤ) < padicValRat p (x' - y')

Tactic:
simp only [H, ↓reduceIte, exp_lt_exp, neg_lt_neg_iff] at h

Premises used: neg_lt_neg_iff, WithZero.exp_lt_exp, reduceIte
-- Module: Mathlib.NumberTheory.Padics.WithVal
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 : ¬x' - y' = 0
h : (↑n : ℤ) < padicValRat p (x' - y')
⊢ LE.le (α := ℚ) 1 (↑p : ℚ)

Tactic:
exact_mod_cast (Nat.Prime.one_le Fact.out)

Premises used: Nat.Prime.one_le, Fact.out
-- Module: Mathlib.NumberTheory.Padics.WithVal
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 : ¬x' - y' = 0
h : (↑n : ℤ) < padicValRat p (x' - y')
⊢ (HPow.hPow (α := ℚ) (↑p : ℚ) (padicValRat p (x' - y')))⁻¹ ≤ (HPow.hPow (α := ℚ) (↑p : ℚ) n)⁻¹

Tactic:
simpa [hp0', zpow_pos, pow_pos, inv_le_inv₀] using
          zpow_right_mono₀ (by exact_mod_cast (Nat.Prime.one_le Fact.out)) h.le

Premises used: pow_pos, LT.lt.le, zpow_pos, zpow_right_mono₀, inv_le_inv₀
-- Module: Mathlib.NumberTheory.Padics.WithVal
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 ℤ))
⊢ Ne (α := ℝ) (↑(Rat.num (↑(p ^ n) : ℚ)) : ℝ) 0

Tactic:
simp [Nat.Prime.ne_zero Fact.out]

Premises used: Nat.Prime.ne_zero, Fact.out
-- Module: Mathlib.NumberTheory.Padics.WithVal
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)ˣ
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)
⊢ ∃ (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)

Tactic:
use (log ((embedding γ.val) * exp (-1))).natAbs