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
γ :
  (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)⁻¹
⊢ 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

Premises used: WithVal.equiv, 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
γ :
  (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
⊢ 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

Premises used: WithVal.equiv, 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
γ :
  (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
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 ℤ))
⊢ (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:
rw [Valuation.map_sub_swap, Valuation.restrict_lt_iff_lt_embedding]

Premises used: Valuation.restrict_lt_iff_lt_embedding, Valuation.map_sub_swap
-- 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)ˣ
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
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 ℤ))
⊢ 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:
change Rat.padicValuation p (x' - y') < embedding γ.1

Premises used: Units.val, HSub.hSub, MonoidWithZeroHom.ValueGroup₀.embedding, 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
γ :
  (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
⊢ 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

Premises used: HSub.hSub, padicNorm
-- 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)ˣ
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) :
        ℚ)⁻¹
⊢ (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 ⊢

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
γ :
  (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 ℤ))
neg :
  ∀ (H : ¬x' - y' = 0),
    exp (-padicValRat p (x' - y')) <
      (embedding : (a : MonoidWithZeroHom.ValueGroup₀ Valued.v) → WithZero (Multiplicative ℤ))
        (↑γ : MonoidWithZeroHom.ValueGroup₀ Valued.v)
⊢ (if x' - y' = 0 then 0 else exp (-padicValRat p (x' - y'))) <
    (embedding : (a : MonoidWithZeroHom.ValueGroup₀ Valued.v) → WithZero (Multiplicative ℤ))
      (↑γ : MonoidWithZeroHom.ValueGroup₀ Valued.v)

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
γ :
  (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)⁻¹
H : x' - y' = 0
pos :
  LT.lt (α := WithZero (Multiplicative ℤ)) (0 : WithZero (Multiplicative ℤ))
    ((embedding : (a : MonoidWithZeroHom.ValueGroup₀ Valued.v) → WithZero (Multiplicative ℤ))
        (↑γ : MonoidWithZeroHom.ValueGroup₀ Valued.v) :
      WithZero (Multiplicative ℤ))
⊢ LT.lt (α := WithZero (Multiplicative ℤ)) (0 : WithZero (Multiplicative ℤ))
    ((embedding : (a : MonoidWithZeroHom.ValueGroup₀ Valued.v) → WithZero (Multiplicative ℤ))
        (↑γ : MonoidWithZeroHom.ValueGroup₀ Valued.v) :
      WithZero (Multiplicative ℤ))

Tactic:
simp only [exp_neg]

Premises used: WithZero.exp_neg
-- 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)ˣ
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)⁻¹
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:
embedding_unit_pos _

Premises used: Set.Mem, setOf, MonoidWithZeroHom.ValueGroup₀.embedding_unit_pos
-- 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)ˣ
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)⁻¹
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:
exact embedding_unit_pos _

Premises used: MonoidWithZeroHom.ValueGroup₀.embedding_unit_pos
-- 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)ˣ
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)⁻¹
H : ¬x' - y' = 0
neg :
  -padicValRat p (x' - y') <
    log
      ((embedding : (a : MonoidWithZeroHom.ValueGroup₀ Valued.v) → WithZero (Multiplicative ℤ))
        (↑γ : MonoidWithZeroHom.ValueGroup₀ Valued.v))
⊢ exp (-padicValRat p (x' - y')) <
    (embedding : (a : MonoidWithZeroHom.ValueGroup₀ Valued.v) → WithZero (Multiplicative ℤ))
      (↑γ : MonoidWithZeroHom.ValueGroup₀ Valued.v)

Tactic:
rw [← lt_log_iff_exp_lt (embedding_unit_ne_zero _)]

Premises used: WithZero.lt_log_iff_exp_lt
-- 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)ˣ
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)⁻¹
H : ¬x' - y' = 0
⊢ -padicValRat p (x' - y') <
    log
      ((embedding : (a : MonoidWithZeroHom.ValueGroup₀ Valued.v) → WithZero (Multiplicative ℤ))
        (↑γ : MonoidWithZeroHom.ValueGroup₀ Valued.v))

Tactic:
simp_all [← zpow_natCast, zpow_pos, inv_le_inv₀, zpow_le_zpow_iff_right₀ hp1', abs_le,
          Int.lt_iff_add_one_le]

Premises used: zpow_natCast, abs_le, Int.lt_iff_add_one_le, zpow_le_zpow_iff_right₀, zpow_pos, 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
γ :
  (MonoidWithZeroHom.ValueGroup₀ (F := Valuation (WithVal (Rat.padicValuation p)) (WithZero (Multiplicative ℤ)))
      Valued.v)ˣ
x y : WithVal (Rat.padicValuation p)
h :
  LE.le (α := ℝ)
    (↑(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
⊢ Ne (α := ℝ)
    (↑(Rat.num
          (↑(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) :
            ℚ)) :
      ℝ)
    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)
⊢ IsDenseInducing (α := WithVal (Rat.padicValuation p)) (β := ℚ_[p])
    (⇑(RingHom.comp (Rat.castHom ℚ_[p]) (WithVal.equiv (Rat.padicValuation p)).toRingHom) :
      (a : WithVal (Rat.padicValuation p)) → ℚ_[p])

Tactic:
Padic.isUniformInducing_cast_withVal.isDenseInducing ?_

Premises used: IsUniformInducing.isDenseInducing, Padic.isUniformInducing_cast_withVal
-- Module: Mathlib.NumberTheory.Padics.WithVal
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
refine :
  DenseRange (X := ℚ_[p]) (α := WithVal (Rat.padicValuation p))
    (⇑(RingHom.comp (Rat.castHom ℚ_[p]) (WithVal.equiv (Rat.padicValuation p)).toRingHom) :
      (a : WithVal (Rat.padicValuation p)) → ℚ_[p])
⊢ IsDenseInducing (α := WithVal (Rat.padicValuation p)) (β := ℚ_[p])
    (⇑(RingHom.comp (Rat.castHom ℚ_[p]) (WithVal.equiv (Rat.padicValuation p)).toRingHom) :
      (a : WithVal (Rat.padicValuation p)) → ℚ_[p])

Tactic:
refine Padic.isUniformInducing_cast_withVal.isDenseInducing ?_

Premises used: IsUniformInducing.isDenseInducing, Padic.isUniformInducing_cast_withVal