Generates quotient point if is fiber of y

theorem generates_quotient_point_if_is_fiber_of_y    (i : Fin ℓ) (steps : ℕ) (h_i_add_steps : i.val + steps ≤ ℓ)    (x : sDomain 𝔽q β h_ℓ_add_R_rate (i := ⟨i, by omega⟩))    (y : sDomain 𝔽q β h_ℓ_add_R_rate (i := ⟨i.val + steps, by omega⟩))    (hx_is_fiber : ∃ (k : Fin (2 ^ steps)), x = qMap_total_fiber 𝔽q β (i := ⟨i, by omega⟩)      (steps := steps) (h_i_add_steps := by        simp only; exact fin_ℓ_steps_lt_ℓ_add_R i steps h_i_add_steps) (y := y) k) :    y = iteratedQuotientMap 𝔽q β h_ℓ_add_R_rate i (k := steps) (h_bound := h_i_add_steps) x := by -- Get the fiber index `k` and the equality from the hypothesis.  rcases hx_is_fiber with ⟨k, hx_eq⟩  let basis_y := sDomain_basis 𝔽q β h_ℓ_add_R_rate    (i := ⟨i.val + steps, by omega⟩) (h_i := by apply Nat.lt_add_of_pos_right_of_le; omega)  apply basis_y.repr.injective  ext j  conv_rhs =>    rw [getSDomainBasisCoeff_of_iteratedQuotientMap]  have h_repr_x := qMap_total_fiber_repr_coeff 𝔽q β i (steps := steps)    (h_i_add_steps := by omega) (y := y) (k := k) (j := ⟨j + steps, by simp only; omega⟩)  simp only at h_repr_x  rw [←hx_eq] at h_repr_x  simp only [fiber_coeff, add_lt_iff_neg_right, not_lt_zero', ↓reduceDIte, add_tsub_cancel_right,    Fin.eta] at h_repr_x  exact h_repr_x.symm