Hexp odd mem

theorem Hexp_odd_mem (α k : ℕ) : ∀ i ∈ Hexp α k, Odd i := by  intro i hi  have hm : (2 : ℕ) ∣ 2 ^ (α + 1) := dvd_pow_self 2 (Nat.succ_ne_zero α)  have hmpos : 0 < 2 ^ (α + 1) := pow_pos (by norm_num) _  have hmeven : Even (2 ^ (α + 1)) := ⟨2 ^ α, by rw [pow_succ]; ring⟩  have hbase : Odd (4 * k + 1) := ⟨2 * k, by ring⟩  rw [Hexp, Finset.mem_biUnion] at hi  obtain ⟨a, _, hi⟩ := hi  rw [Finset.mem_insert, Finset.mem_singleton] at hi  have hxodd : Odd ((4 * k + 1) ^ a % 2 ^ (α + 1)) := by    rw [Nat.odd_iff, Nat.mod_mod_of_dvd _ hm, ← Nat.odd_iff]; exact hbase.pow  rcases hi with h | h  · exact h ▸ hxodd  · rw [h, Nat.odd_iff, Nat.mod_mod_of_dvd _ hm, ← Nat.odd_iff]    exact Nat.Even.sub_odd (Nat.le_of_lt (Nat.mod_lt _ hmpos)) hmeven hxodd