Hexp card

theorem Hexp_card (α k : ℕ) (hk2pow : ∃ κ, k = 2 ^ κ) (hk : 2 * k ∣ 2 ^ α) :    (Hexp α k).card = 2 ^ α / k := by  obtain ⟨κ, rfl⟩ := hk2pow  have hκ : κ + 1 ≤ α :=    (Nat.pow_dvd_pow_iff_le_right (by norm_num : (1 : ℕ) < 2)).mp      (by rw [pow_succ, mul_comm]; exact hk)  have hm4 : (4 : ℕ) ∣ 2 ^ (α + 1) := by    rw [show (4 : ℕ) = 2 ^ 2 from rfl]; exact pow_dvd_pow 2 (by omega)  have hm40 : 2 ^ (α + 1) % 4 = 0 := by obtain ⟨c, hc⟩ := hm4; omega  have hmpos : 0 < 2 ^ (α + 1) := by positivity  have hp4 : ∀ a, (4 * 2 ^ κ + 1) ^ a % 2 ^ (α + 1) % 4 = 1 := fun a => by    rw [Nat.mod_mod_of_dvd _ hm4, Nat.pow_mod]    norm_num [show (4 * 2 ^ κ + 1) % 4 = 1 from by omega]  have hplt : ∀ a, (4 * 2 ^ κ + 1) ^ a % 2 ^ (α + 1) < 2 ^ (α + 1) := fun a => Nat.mod_lt _ hmpos  have hrange : 2 ^ α / (2 * 2 ^ κ) = 2 ^ (α - κ - 1) := by    rw [show 2 * 2 ^ κ = 2 ^ (κ + 1) from by rw [pow_succ]; ring, Nat.pow_div hκ (by norm_num),      Nat.sub_sub]  have hpinj : Set.InjOn (fun a => (4 * 2 ^ κ + 1) ^ a % 2 ^ (α + 1))      ↑(Finset.range (2 ^ (α - κ - 1))) := four_pow_injOn κ α hκ  have hqeq : ∀ a, (2 ^ (α + 1) - (4 * 2 ^ κ + 1) ^ a % 2 ^ (α + 1)) % 2 ^ (α + 1)      = 2 ^ (α + 1) - (4 * 2 ^ κ + 1) ^ a % 2 ^ (α + 1) := fun a =>    Nat.mod_eq_of_lt (by have := hplt a; have := hp4 a; omega)  rw [Hexp, hrange, Finset.card_biUnion]  · have hc2 : ∀ a ∈ Finset.range (2 ^ (α - κ - 1)),        ({(4 * 2 ^ κ + 1) ^ a % 2 ^ (α + 1),          (2 ^ (α + 1) - (4 * 2 ^ κ + 1) ^ a % 2 ^ (α + 1)) % 2 ^ (α + 1)} : Finset ℕ).card = 2 :=      fun a _ => Finset.card_pair (by rw [hqeq a]; have := hp4 a; have := hplt a; omega)    have hmul : 2 ^ (α - κ - 1) * 2 = 2 ^ (α - κ) := by      rw [← pow_succ, show α - κ - 1 + 1 = α - κ from by omega]    rw [Finset.sum_congr rfl hc2, Finset.sum_const, Finset.card_range, smul_eq_mul, hmul,      Nat.pow_div (by omega) (by norm_num)]  · intro a ha b hb hab    simp only [Function.onFun]    rw [Finset.disjoint_left]    have hla := hplt a; have hlb := hplt b; have h1a := hp4 a; have h1b := hp4 b    have hpab : (4 * 2 ^ κ + 1) ^ a % 2 ^ (α + 1) ≠ (4 * 2 ^ κ + 1) ^ b % 2 ^ (α + 1) := fun h =>      hab (hpinj ha hb h)    intro x hx hx'    rw [hqeq a] at hx; rw [hqeq b] at hx'    simp only [Finset.mem_insert, Finset.mem_singleton] at hx hx'    rcases hx with rfl | rfl <;> rcases hx' with h' | h' <;> omega