-- 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
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)
⊢ IsUniformInducing (α := WithVal (Rat.padicValuation p)) (β := ℚ_[p])
    (⇑(RingHom.comp (Rat.castHom ℚ_[p]) (WithVal.equiv (Rat.padicValuation p)).toRingHom) :
      (a : WithVal (Rat.padicValuation p)) → ℚ_[p])

Tactic:
rw [Filter.HasBasis.isUniformInducing_iff (Valued.hasBasis_uniformity _ _)
    (Metric.uniformity_basis_dist_le_pow hp0 hp1)]

Premises used: Filter.HasBasis.isUniformInducing_iff, Valued.hasBasis_uniformity, Metric.uniformity_basis_dist_le_pow