-- 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
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 ℤ))
⊢ 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 :
    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
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