-- 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
⊢ IsUniformInducing (α := WithVal (Rat.padicValuation p)) (β := ℚ_[p])
    (⇑(RingHom.comp (Rat.castHom ℚ_[p]) (WithVal.equiv (Rat.padicValuation p)).toRingHom) :
      (a : WithVal (Rat.padicValuation p)) → ℚ_[p])
have rw : (∀ (i : ℕ),
    True →
      ∃ (j :
        (MonoidWithZeroHom.ValueGroup₀ (F := Valuation (WithVal (Rat.padicValuation p)) (WithZero (Multiplicative ℤ)))
            Valued.v)ˣ),
        True ∧
          ∀ (x y : WithVal (Rat.padicValuation p)),
            Membership.mem (γ := Set (WithVal (Rat.padicValuation p) × WithVal (Rat.padicValuation p)))
                {p_1 : WithVal (Rat.padicValuation p) × WithVal (Rat.padicValuation p) |
                  (Valuation.restrict Valued.v :
                        (a : WithVal (Rat.padicValuation p)) →
                          MonoidWithZeroHom.ValueGroup₀
                            (↑Valued.v : WithVal (Rat.padicValuation p) →*₀ WithZero (Multiplicative ℤ)))
                      (p_1.2 - p_1.1) <
                    (↑j : MonoidWithZeroHom.ValueGroup₀ Valued.v)}
                (x, y) →
              Membership.mem (α := ℚ_[p] × ℚ_[p]) (γ := Set (ℚ_[p] × ℚ_[p]))
                {p_1 : ℚ_[p] × ℚ_[p] | dist p_1.1 p_1.2 ≤ HPow.hPow (α := ℝ) (↑p : ℝ)⁻¹ i}
                (((RingHom.comp (Rat.castHom ℚ_[p]) (WithVal.equiv (Rat.padicValuation p)).toRingHom :
                        (a : WithVal (Rat.padicValuation p)) → ℚ_[p])
                      x,
                    (RingHom.comp (Rat.castHom ℚ_[p]) (WithVal.equiv (Rat.padicValuation p)).toRingHom :
                        (a : WithVal (Rat.padicValuation p)) → ℚ_[p])
                      y) :
                  ℚ_[p] × ℚ_[p])) ∧
  ∀
    (j :
      (MonoidWithZeroHom.ValueGroup₀ (F := Valuation (WithVal (Rat.padicValuation p)) (WithZero (Multiplicative ℤ)))
          Valued.v)ˣ),
    True →
      ∃ (i : ℕ),
        True ∧
          ∀ (x y : WithVal (Rat.padicValuation p)),
            Membership.mem (α := ℚ_[p] × ℚ_[p]) (γ := Set (ℚ_[p] × ℚ_[p]))
                {p_1 : ℚ_[p] × ℚ_[p] | dist p_1.1 p_1.2 ≤ HPow.hPow (α := ℝ) (↑p : ℝ)⁻¹ i}
                (((RingHom.comp (Rat.castHom ℚ_[p]) (WithVal.equiv (Rat.padicValuation p)).toRingHom :
                        (a : WithVal (Rat.padicValuation p)) → ℚ_[p])
                      x,
                    (RingHom.comp (Rat.castHom ℚ_[p]) (WithVal.equiv (Rat.padicValuation p)).toRingHom :
                        (a : WithVal (Rat.padicValuation p)) → ℚ_[p])
                      y) :
                  ℚ_[p] × ℚ_[p]) →
              Membership.mem (γ := Set (WithVal (Rat.padicValuation p) × WithVal (Rat.padicValuation p)))
                {p_1 : WithVal (Rat.padicValuation p) × WithVal (Rat.padicValuation p) |
                  (Valuation.restrict Valued.v :
                        (a : WithVal (Rat.padicValuation p)) →
                          MonoidWithZeroHom.ValueGroup₀
                            (↑Valued.v : WithVal (Rat.padicValuation p) →*₀ WithZero (Multiplicative ℤ)))
                      (p_1.2 - p_1.1) <
                    (↑j : MonoidWithZeroHom.ValueGroup₀ Valued.v)}
                (x, y)
Tactic: rw [Filter.HasBasis.isUniformInducing_iff (Valued.hasBasis_uniformity _ _)
    (Metric.uniformity_basis_dist_le_pow hp0 hp1)]