Q Map total fiber disjoint

theorem qMap_total_fiber_disjoint  (i : Fin ℓ) (steps : ℕ) (h_i_add_steps : i + steps ≤ ℓ)  {y₁ y₂ : sDomain 𝔽q β h_ℓ_add_R_rate ⟨i.val + steps, by omega⟩}  (hy_ne : y₁ ≠ y₂) :  Disjoint    ((qMap_total_fiber 𝔽q β (i := ⟨i, by omega⟩) (steps := steps)      (h_i_add_steps := fin_ℓ_steps_lt_ℓ_add_R i steps h_i_add_steps) y₁ '' Set.univ).toFinset)    ((qMap_total_fiber 𝔽q β (i := ⟨i, by omega⟩) (steps := steps)      (h_i_add_steps := fin_ℓ_steps_lt_ℓ_add_R i steps h_i_add_steps) y₂ '' Set.univ).toFinset)    := by -- Proof by contradiction. Assume the intersection is non-empty.  rw [Finset.disjoint_iff_inter_eq_empty]  by_contra h_nonempty  -- Let `x` be an element in the intersection of the two fiber sets.  obtain ⟨x, h_x_mem_inter⟩ := Finset.nonempty_of_ne_empty h_nonempty  have hx₁ := Finset.mem_of_mem_inter_left h_x_mem_inter  have hx₂ := Finset.mem_of_mem_inter_right h_x_mem_inter  -- A helper lemma : applying the forward map to a point in a generated fiber returns  -- the original quotient point.  have iteratedQuotientMap_of_qMap_total_fiber_eq_self    (y : sDomain 𝔽q β h_ℓ_add_R_rate ⟨i.val + steps, by omega⟩)    (k : Fin (2 ^ steps)) :    iteratedQuotientMap 𝔽q β h_ℓ_add_R_rate (i := ⟨i, by omega⟩) (k := steps)      (h_bound := by omega)      (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) = y := by      have h := generates_quotient_point_if_is_fiber_of_y        (h_i_add_steps := h_i_add_steps) (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⟩))      ) (y := y) (hx_is_fiber := by use k)      exact h.symm  have h_exists_k₁ : ∃ k, 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₁ k := by    -- convert (x ∈ Finset of the image of the fiber) to statement    -- about membership in the Set.    rw [Set.mem_toFinset] at hx₁    rw [Set.mem_image] at hx₁ -- Set.mem_image gives us t an index that maps to x    -- ⊢ `∃ (k : Fin (2 ^ steps)), k ∈ Set.univ ∧ qMap_total_fiber ... y₁ k = x`.    rcases hx₁ with ⟨k, _, h_eq⟩    use k; exact h_eq.symm   have h_exists_k₂ : ∃ k, 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₂ k := by    rw [Set.mem_toFinset] at hx₂    rw [Set.mem_image] at hx₂ -- Set.mem_image gives us t an index that maps to x    rcases hx₂ with ⟨k, _, h_eq⟩    use k; exact h_eq.symm   have h_y₁_eq_quotient_x : y₁ =      iteratedQuotientMap 𝔽q β h_ℓ_add_R_rate i steps h_i_add_steps x := by    apply generates_quotient_point_if_is_fiber_of_y (hx_is_fiber := by exact h_exists_k₁)   have h_y₂_eq_quotient_x : y₂ =      iteratedQuotientMap 𝔽q β h_ℓ_add_R_rate i steps h_i_add_steps x := by    apply generates_quotient_point_if_is_fiber_of_y (hx_is_fiber := by exact h_exists_k₂)   let kQuotientIndex := pointToIterateQuotientIndex (i := ⟨i, by omega⟩) (steps := steps)    (h_i_add_steps := by omega) (x := x)   -- Since `x` is in the fiber of `y₁`, applying the forward map to `x` yields `y₁`.  have h_map_x_eq_y₁ : iteratedQuotientMap 𝔽q β h_ℓ_add_R_rate (i := ⟨i, by omega⟩)      (k := steps) (h_bound := by omega) x = y₁ := by    have h := iteratedQuotientMap_of_qMap_total_fiber_eq_self (y := y₁) (k := kQuotientIndex)    have hx₁ : 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₁ kQuotientIndex := by      have h_res := is_fiber_iff_generates_quotient_point 𝔽q β i steps (by omega)        (x := x) (y := y₁).mp (h_y₁_eq_quotient_x)      exact h_res.symm    rw [hx₁]    exact iteratedQuotientMap_of_qMap_total_fiber_eq_self y₁ kQuotientIndex   -- Similarly, since `x` is in the fiber of `y₂`, applying the forward map yields `y₂`.  have h_map_x_eq_y₂ : iteratedQuotientMap 𝔽q β h_ℓ_add_R_rate (i := ⟨i, by omega⟩)      (k := steps) (h_bound := by omega) x = y₂ := by    -- have h := iteratedQuotientMap_of_qMap_total_fiber_eq_self (y := y₂) (k := kQuotientIndex)    have hx₂ : 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₂ kQuotientIndex := by      have h_res := is_fiber_iff_generates_quotient_point 𝔽q β i steps (by omega)        (x := x) (y := y₂).mp (h_y₂_eq_quotient_x)      exact h_res.symm    rw [hx₂]    exact iteratedQuotientMap_of_qMap_total_fiber_eq_self y₂ kQuotientIndex   exact hy_ne (h_map_x_eq_y₁.symm.trans h_map_x_eq_y₂)