Rq eq zero of l1Norm eq zero

theorem Rq.eq_zero_of_l1Norm_eq_zero {x : Rq Φ} (h : ‖x‖₁ = 0) : x = 0 := by  unfold Rq.l1Norm at h  -- Each centered coefficient below `deg φ` is zero.  have hlt : ∀ k, k < Φ.φ.natDegree → x.1.coeff k = 0 := by    intro k hk    have hz0 : (x.1.coeff k).valMinAbs.natAbs = 0 :=      (Finset.sum_eq_zero_iff.mp h) k (Finset.mem_range.mpr hk)    rw [← ZMod.valMinAbs_eq_zero, ← Int.natAbs_eq_zero]    exact hz0  -- Hence the underlying polynomial is `0` (coeffs below `deg φ` by the above, coeffs at or  -- above `deg φ` by reducedness).  have htoP : x.1.toPoly = 0 := by    apply Polynomial.ext    intro k    rw [Polynomial.coeff_zero]    by_cases hk : k < Φ.φ.natDegree    · rw [← CompPoly.CPolynomial.coeff_toPoly]; exact hlt k hk    · rw [not_lt] at hk      have hdeg : x.1.toPoly.degree < Φ.φ.toPoly.degree := Φ.degree_toPoly_lt_of_reduced x.2      have hφne : Φ.φ.toPoly ≠ 0 := (IsCyclotomic.monic (Φ := Φ)).ne_zero      have hdegφ : Φ.φ.toPoly.degree = (Φ.φ.natDegree : WithBot ℕ) := by        rw [Polynomial.degree_eq_natDegree hφne, CompPoly.CPolynomial.natDegree_toPoly]      have hle' : Φ.φ.toPoly.degree ≤ (k : WithBot ℕ) := by        rw [hdegφ]; exact_mod_cast hk      exact Polynomial.coeff_eq_zero_of_degree_lt (lt_of_lt_of_le hdeg hle')  have hx1 : x.1 = 0 := (CompPoly.CPolynomial.toPoly_eq_zero_iff x.1).mp htoP  exact Subtype.ext (by rw [Rq.zero_val]; exact hx1)