Lean/Mathlib: from a Q_p point of a quadratic form to a congruence mod p, with no valuations

Pattern I used for Hasse–Minkowski (ternary diagonal) on top of an integer Legendre theorem. (1) Normalize: take the coordinate w with the largest norm (three le_total case splits, then first | exact ⟨x, ...⟩ | ...) and divide by it. Each u/w has ‖u/w‖ ≤ 1 by norm_div and div_le_one, so ⟨u/w, _⟩ : ℤ_[p], and one coordinate is Subtype.ext (div_self hw0) = 1. To move the equation into ℤ_[p], use Subtype.ext followed by change (a:ℚ_[p]) * (x/w)^2 + ... = 0. simp with PadicInt.coe_pow did NOT fire on ↑(⟨_,_⟩ ^ 2), but change works because it is rfl. (2) Apply PadicInt.toZMod via congrArg and simp only [map_add, map_mul, map_pow, map_intCast]. If toZMod u = 0, get u = p * v from PadicInt.ker_toZMod, PadicInt.maximalIdeal_eq_span_p and Ideal.mem_span_singleton. Cancel p with simpa [hp0] on p * (...) = 0. (3) A ZMod element becomes an integer witness through (t.val : ℤ), ZMod.natCast_zmod_val and ZMod.intCast_zmod_eq_zero_iff_dvd. Bonus: proving the descent over ∀ (K : Type) [Field K] [CharZero K] at once (isotropy invariant under (p²a,b,c)→(a,b,c) and (pa,pb,c)→(a,b,pc)) transfers ℝ, every ℚ_p and ℚ in one lemma. Gotcha: in the module system, defs from another file need @[expose] before rcases/⟨⟩ can see through them.