Hexp generator smul

theorem Hexp_generator_smul (α k g : ℕ) (hk2pow : ∃ κ, k = 2 ^ κ) (hk : 2 * k ∣ 2 ^ α)    (hg : g = conjExp α ∨ g = genExp k) :    (Hexp α k).image (fun i => (g * i) % 2 ^ (α + 1)) = Hexp α 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 hmpos : 0 < 2 ^ (α + 1) := by positivity  have hopos : 0 < 2 ^ (α - κ - 1) := by positivity  have hm2 : 2 ≤ 2 ^ (α + 1) := by    calc 2 = 2 ^ 1 := rfl      _ ≤ 2 ^ (α + 1) := Nat.pow_le_pow_right (by norm_num) (by omega)  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 hplt : ∀ a, (4 * 2 ^ κ + 1) ^ a % 2 ^ (α + 1) < 2 ^ (α + 1) := fun a => Nat.mod_lt _ hmpos  have hcop1 : Nat.Coprime (4 * 2 ^ κ + 1) (2 ^ (α + 1)) :=    (Nat.coprime_two_right.mpr ⟨2 * 2 ^ κ, by ring⟩).pow_right _  have hp1 : ∀ a, 1 ≤ (4 * 2 ^ κ + 1) ^ a % 2 ^ (α + 1) := fun a => by    rcases Nat.eq_zero_or_pos ((4 * 2 ^ κ + 1) ^ a % 2 ^ (α + 1)) with h | h    · have hco : Nat.Coprime (2 ^ (α + 1)) ((4 * 2 ^ κ + 1) ^ a) := (hcop1.pow_left _).symm      rw [Nat.Coprime, Nat.gcd_eq_left (Nat.dvd_of_mod_eq_zero h)] at hco; omega    · exact h  -- general modular negation: `c·y ≡ -(c·z)` when `y + z = 2^{α+1}`  have hgen_neg : ∀ c y z : ℕ, y + z = 2 ^ (α + 1) →      (c * y) % 2 ^ (α + 1) = (2 ^ (α + 1) - (c * z) % 2 ^ (α + 1)) % 2 ^ (α + 1) := by    intro c y z hyz    have h1 : c * y + (c * z) % 2 ^ (α + 1) ≡ 0 [MOD 2 ^ (α + 1)] :=      calc c * y + (c * z) % 2 ^ (α + 1) ≡ c * y + c * z [MOD 2 ^ (α + 1)] :=            Nat.ModEq.add_left _ (Nat.mod_modEq _ _)        _ = c * 2 ^ (α + 1) := by rw [← Nat.mul_add, hyz]        _ ≡ 0 [MOD 2 ^ (α + 1)] := (Nat.modEq_zero_iff_dvd).mpr ⟨c, by ring⟩    have h2 : (2 ^ (α + 1) - (c * z) % 2 ^ (α + 1)) % 2 ^ (α + 1) + (c * z) % 2 ^ (α + 1)        ≡ 0 [MOD 2 ^ (α + 1)] :=      calc (2 ^ (α + 1) - (c * z) % 2 ^ (α + 1)) % 2 ^ (α + 1) + (c * z) % 2 ^ (α + 1)            ≡ (2 ^ (α + 1) - (c * z) % 2 ^ (α + 1)) + (c * z) % 2 ^ (α + 1) [MOD 2 ^ (α + 1)] :=            Nat.ModEq.add_right _ (Nat.mod_modEq _ _)        _ = 2 ^ (α + 1) := Nat.sub_add_cancel (Nat.le_of_lt (Nat.mod_lt _ hmpos))        _ ≡ 0 [MOD 2 ^ (α + 1)] := (Nat.modEq_zero_iff_dvd).mpr (dvd_refl _)    have key := Nat.ModEq.add_right_cancel' ((c * z) % 2 ^ (α + 1)) (h1.trans h2.symm)    rw [Nat.ModEq, Nat.mod_mod] at key; exact key  -- `genExp · pₐ ≡ p_{(a+1) mod o}` (cyclic shift via the order)  have hmulP : ∀ a, (genExp (2 ^ κ) * ((4 * 2 ^ κ + 1) ^ a % 2 ^ (α + 1))) % 2 ^ (α + 1)      = (4 * 2 ^ κ + 1) ^ ((a + 1) % 2 ^ (α - κ - 1)) % 2 ^ (α + 1) := fun a => by    change (4 * 2 ^ κ + 1) * ((4 * 2 ^ κ + 1) ^ a % 2 ^ (α + 1)) % 2 ^ (α + 1) = _    calc (4 * 2 ^ κ + 1) * ((4 * 2 ^ κ + 1) ^ a % 2 ^ (α + 1))          ≡ (4 * 2 ^ κ + 1) * (4 * 2 ^ κ + 1) ^ a [MOD 2 ^ (α + 1)] :=          Nat.ModEq.mul_left _ (Nat.mod_modEq _ _)      _ = (4 * 2 ^ κ + 1) ^ (a + 1) := (pow_succ' _ _).symm      _ ≡ (4 * 2 ^ κ + 1) ^ ((a + 1) % 2 ^ (α - κ - 1)) [MOD 2 ^ (α + 1)] :=          four_pow_mod_period κ α (a + 1) hκ  have hHlt : ∀ i ∈ Hexp α (2 ^ κ), i < 2 ^ (α + 1) := by    intro i hi    rw [Hexp, Finset.mem_biUnion] at hi    obtain ⟨a, _, hia⟩ := hi    rw [Finset.mem_insert, Finset.mem_singleton] at hia    rcases hia with rfl | rfl <;> exact Nat.mod_lt _ hmpos  have hcop : Nat.Coprime g (2 ^ (α + 1)) := by    rcases hg with rfl | rfl    · refine (Nat.coprime_two_right.mpr ?_).pow_right _      rw [conjExp]      exact Nat.Even.sub_odd Nat.one_le_two_pow ⟨2 ^ α, by rw [pow_succ]; ring⟩ odd_one    · exact (Nat.coprime_two_right.mpr ⟨2 * 2 ^ κ, by rw [genExp]; ring⟩).pow_right _  have hinj : Set.InjOn (fun i => (g * i) % 2 ^ (α + 1)) ↑(Hexp α (2 ^ κ)) := by    intro i hi j hj hij    rw [Finset.mem_coe] at hi hj    have h := Nat.ModEq.cancel_left_of_coprime hcop.symm      (hij : g * i ≡ g * j [MOD 2 ^ (α + 1)])    rwa [Nat.ModEq, Nat.mod_eq_of_lt (hHlt i hi), Nat.mod_eq_of_lt (hHlt j hj)] at h  have hsub : (Hexp α (2 ^ κ)).image (fun i => (g * i) % 2 ^ (α + 1)) ⊆ Hexp α (2 ^ κ) := by    intro y hy    rw [Finset.mem_image] at hy    obtain ⟨i, hi, rfl⟩ := hy    rw [Hexp, hrange, Finset.mem_biUnion] at hi    rw [Hexp, hrange, Finset.mem_biUnion]    obtain ⟨a, ha, hia⟩ := hi    rw [Finset.mem_range] at ha    rw [Finset.mem_insert, Finset.mem_singleton] at hia    rcases hg with rfl | rfl    · rcases hia with rfl | rfl      · refine ⟨a, Finset.mem_range.mpr ha, ?_⟩        rw [Finset.mem_insert, Finset.mem_singleton]; right        rw [conjExp, mul_comm (2 ^ (α + 1) - 1) ((4 * 2 ^ κ + 1) ^ a % 2 ^ (α + 1)),          hgen_neg _ (2 ^ (α + 1) - 1) 1 (by omega), mul_one, Nat.mod_mod]      · refine ⟨a, Finset.mem_range.mpr ha, ?_⟩        rw [Finset.mem_insert]; left        have hpm := hplt a; have hp1a := hp1 a        have hqv : (2 ^ (α + 1) - (4 * 2 ^ κ + 1) ^ a % 2 ^ (α + 1)) % 2 ^ (α + 1)            = 2 ^ (α + 1) - (4 * 2 ^ κ + 1) ^ a % 2 ^ (α + 1) := Nat.mod_eq_of_lt (by omega)        rw [hqv, conjExp, mul_comm (2 ^ (α + 1) - 1) _,          hgen_neg _ (2 ^ (α + 1) - 1) 1 (by omega), mul_one, hqv,          Nat.sub_sub_self (by omega), Nat.mod_eq_of_lt hpm]    · rcases hia with rfl | rfl      · refine ⟨(a + 1) % 2 ^ (α - κ - 1), Finset.mem_range.mpr (Nat.mod_lt _ hopos), ?_⟩        rw [Finset.mem_insert]; left; exact hmulP a      · refine ⟨(a + 1) % 2 ^ (α - κ - 1), Finset.mem_range.mpr (Nat.mod_lt _ hopos), ?_⟩        rw [Finset.mem_insert, Finset.mem_singleton]; right        have hpm := hplt a; have hp1a := hp1 a        have hsum : (2 ^ (α + 1) - (4 * 2 ^ κ + 1) ^ a % 2 ^ (α + 1)) % 2 ^ (α + 1)            + (4 * 2 ^ κ + 1) ^ a % 2 ^ (α + 1) = 2 ^ (α + 1) := by          rw [Nat.mod_eq_of_lt (by omega)]; omega        rw [hgen_neg (genExp (2 ^ κ)) _ ((4 * 2 ^ κ + 1) ^ a % 2 ^ (α + 1)) hsum, hmulP a]  exact Finset.eq_of_subset_of_card_le hsub (le_of_eq (Finset.card_image_of_injOn hinj).symm)