Point To Iterate Quotient Index q Map total fiber eq self

lemma pointToIterateQuotientIndex_qMap_total_fiber_eq_self (i : Fin ℓ) (steps : ℕ)    (h_i_add_steps : i.val + steps ≤ ℓ)    (y : (sDomain 𝔽q β h_ℓ_add_R_rate) (i := ⟨i + steps, by omega⟩)) (k : Fin (2 ^ steps)) :    pointToIterateQuotientIndex (i := ⟨i, by omega⟩) (steps := steps) (h_i_add_steps := by omega)      (x := ((qMap_total_fiber 𝔽q β (i := ⟨i, by omega⟩) (steps := steps)        (h_i_add_steps := by apply Nat.lt_add_of_pos_right_of_le; omega) (y := y) k):          sDomain 𝔽q β h_ℓ_add_R_rate (i := ⟨i, by omega⟩))) = k := by  apply Fin.eq_mk_iff_val_eq.mpr  apply eq_iff_eq_all_getBits.mpr  intro j -- bit index j  simp only [pointToIterateQuotientIndex, qMap_total_fiber]  rw [Nat.getBit_of_binaryFinMapToNat]  simp only [Nat.add_zero, Nat.pow_zero, eq_mp_eq_cast, cast_eq, Module.Basis.repr_symm_apply]  by_cases h_j : j < steps  · simp only [h_j, ↓reduceDIte];    by_cases hsteps : steps = 0    · simp only [hsteps, ↓reduceDIte, eqRec_eq_cast, Nat.add_zero, Nat.pow_zero]      omega    · simp only [hsteps, ↓reduceDIte, Module.Basis.repr_linearCombination,      Finsupp.equivFunOnFinite_symm_apply_apply, h_j, ite_eq_left_iff, one_ne_zero,      imp_false, Decidable.not_not]      -- ⊢ (if j.getBit ↑k = 0 then 0 else 1) = j.getBit ↑k      have h := Nat.getBit_eq_zero_or_one (k := j) (n := k)      by_cases h_j_getBit_k_eq_0 : j.getBit ↑k = 0      · simp only [h_j_getBit_k_eq_0, ↓reduceIte]      · simp only [h_j_getBit_k_eq_0, false_or, ↓reduceIte] at h ⊢        exact id (Eq.symm h)  · rw [Nat.getBit_of_lt_two_pow];    simp only [h_j, ↓reduceDIte, ↓reduceIte];