J valuation of bad prime

lemma j_valuation_of_bad_prime (P : FreyPackage) {q : ℕ} (hqPrime : q.Prime)    (hqbad : (q : ℤ) ∣ P.a * P.b * P.c) (hqodd : 2 < q) :    (P.p : ℤ) ∣ padicValRat q P.freyCurve.j := by  have := Fact.mk hqPrime  have hqPrime' := Nat.prime_iff_prime_int.mp hqPrime  have h₀ : ((P.c ^ (2 * P.p) - (P.a * P.b) ^ P.p) ^ 3 : ℚ) ≠ 0 := by    rw_mod_cast [pow_mul', ← P.hFLT, mul_pow]    exact pow_ne_zero _ <| ne_of_gt <| j_pos_aux _ _ (pow_ne_zero _ P.hb0)  have h₁ : P.a * P.b * P.c ≠ 0 := mul_ne_zero (mul_ne_zero P.ha0 P.hb0) P.hc0  rw [FreyCurve.j, padicValRat.div (mul_ne_zero (by norm_num) h₀) (pow_ne_zero _ (mod_cast h₁)),    padicValRat.mul (by norm_num) h₀, padicValRat.pow, ← Nat.cast_two,    ← padicValRat_of_nat, padicValNat_primes hqodd.ne', Nat.cast_zero, mul_zero, zero_add]  have : ¬ (q : ℤ) ∣ (P.c^(2*P.p)-(P.a*P.b)^P.p) ^ 3 := by    rw [hqPrime'.dvd_pow_iff_dvd three_ne_zero]    have hq' : Xor ((q : ℤ) ∣ P.a * P.b) ((q : ℤ) ∣ P.c) := by      rw [xor_iff_not_iff, iff_iff_and_or_not_and_not]      rintro (⟨hab, hc⟩ | ⟨hab, hc⟩)      · rw [hqPrime'.dvd_mul] at hab        apply hqPrime'.not_dvd_one        cases hab with        | inl ha => rw [← P.hgcdac]; exact dvd_gcd ha hc        | inr hb => rw [← P.hgcdbc]; exact dvd_gcd hb hc      · rw [hqPrime'.dvd_mul] at hqbad        exact hqbad.rec hab hc    have h2p0 := mul_ne_zero two_ne_zero P.hp0    cases hq' with    | inl h =>      rw [dvd_sub_left (dvd_pow h.1 P.hp0), hqPrime'.dvd_pow_iff_dvd h2p0]      exact h.2    | inr h =>      rw [dvd_sub_right (dvd_pow h.1 h2p0), hqPrime'.dvd_pow_iff_dvd P.hp0]      exact h.2  norm_cast  rw [padicValRat.of_int, padicValInt.eq_zero_of_not_dvd this, Nat.cast_zero, zero_sub,    Int.cast_pow, padicValRat.pow, dvd_neg, Nat.cast_mul]  exact dvd_mul_of_dvd_left (dvd_mul_left _ _) _