Order Of q mod two pow

theorem orderOf_q_mod_two_pow (hq5 : q % 8 = 5) (α : ℕ) (hα : 1 ≤ α) :    orderOf (ZMod.unitOfCoprime q (coprime_q_two_pow hq5 (α + 1))) = 2 ^ (α - 1) := by  rcases Nat.lt_or_ge α 2 with hlt | hge  · have hα1 : α = 1 := by omega    subst hα1    simp only [Nat.sub_self, pow_zero]    rw [orderOf_eq_one_iff, ← pow_one (ZMod.unitOfCoprime q _), unit_pow_eq_one_iff hq5 1 1]    simpa using four_dvd_q_sub_one hq5  · have key := orderOf_eq_prime_pow (x := ZMod.unitOfCoprime q (coprime_q_two_pow hq5 (α + 1)))      (p := 2) (n := α - 2) ?_ ?_    · rw [key]; congr 1; omega    · rw [unit_pow_eq_one_iff hq5 α]      have h3 := not_two_pow_dvd (q := q) hq5 (α - 2)      have he : (α - 2) + 3 = α + 1 := by omega      rwa [he] at h3    · rw [unit_pow_eq_one_iff hq5 α]      have h2 := two_pow_dvd (q := q) hq5 (α - 1)      have he : (α - 1) + 2 = α + 1 := by omega      have he2 : (α - 2) + 1 = α - 1 := by omega      rw [he2]; rwa [he] at h2