-- 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₁ :
  ∀
    (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 ℤ))
h₂ :
  ∀
    (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) :
                ℚ) :
            ℝ)⁻¹),
    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),
        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
⊢ 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

Premises used: Rat.cast_inv_of_ne_zero, Rat.cast_natCast, Nat.cast_pow, Rat.cast_le