spatialRadius_coordRay_ne_zero

formal source

 236      gives `spatialNormSq > 0` and hence `spatialRadius ≠ 0`.
 237
 238    Closes one of the §XXIII.B′ Mathlib calculus axioms. -/
 239theorem spatialRadius_coordRay_ne_zero (x : Fin 4 → ℝ) (ν : Fin 4) (s : ℝ)
 240    (hx : spatialRadius x ≠ 0) (hs : |s| < spatialRadius x / 2) :
 241    spatialRadius (coordRay x ν s) ≠ 0 := by
 242  rw [spatialRadius_ne_zero_iff]
 243  have hr_pos : 0 < spatialRadius x := spatialRadius_pos_of_ne_zero x hx
 244  have hr_sq : spatialRadius x ^ 2 = spatialNormSq x := by
 245    unfold spatialRadius; rw [Real.sq_sqrt (spatialNormSq_nonneg x)]
 246  have h_s_lo : -(spatialRadius x / 2) < s := (abs_lt.mp hs).1
 247  have h_s_hi : s < spatialRadius x / 2 := (abs_lt.mp hs).2
 248  have h_x1_le : x 1 ^ 2 ≤ spatialRadius x ^ 2 := hr_sq ▸ sq_le_spatialNormSq_1 x
 249  have h_x2_le : x 2 ^ 2 ≤ spatialRadius x ^ 2 := hr_sq ▸ sq_le_spatialNormSq_2 x
 250  have h_x3_le : x 3 ^ 2 ≤ spatialRadius x ^ 2 := hr_sq ▸ sq_le_spatialNormSq_3 x
 251  -- Case split on ν using its underlying ℕ.
 252  obtain ⟨k, hk⟩ := ν
 253  match k, hk with
 254  | 0, _ =>
 255    rw [show ((⟨0, by decide⟩ : Fin 4) = (0 : Fin 4)) from rfl,
 256        spatialNormSq_coordRay_temporal]
 257    exact (spatialRadius_ne_zero_iff x).mp hx
 258  | 1, _ =>
 259    rw [show ((⟨1, by decide⟩ : Fin 4) = (1 : Fin 4)) from rfl,
 260        spatialNormSq_coordRay_spatial_1]
 261    intro h_zero
 262    have h_sq1 : (x 1 + s) ^ 2 = 0 := by
 263      nlinarith [sq_nonneg (x 1 + s), sq_nonneg (x 2), sq_nonneg (x 3)]
 264    have h_sq2 : x 2 ^ 2 = 0 := by
 265      nlinarith [sq_nonneg (x 1 + s), sq_nonneg (x 2), sq_nonneg (x 3)]
 266    have h_sq3 : x 3 ^ 2 = 0 := by
 267      nlinarith [sq_nonneg (x 1 + s), sq_nonneg (x 2), sq_nonneg (x 3)]
 268    have h_eq1 : x 1 + s = 0 := sq_eq_zero_iff.mp h_sq1
 269    have h_eq2 : x 2 = 0 := sq_eq_zero_iff.mp h_sq2