Ultra Product exists alg Equiv of bdd Above card

lemma UltraProduct.exists_algEquiv_of_bddAbove_card    [TopologicalSpace R₀]    [IsTopologicalRing R₀]    [Algebra.TopologicallyFG ℤ R₀]    [∀ i, TopologicalSpace (R i)]    [∀ i, T2Space (R i)] (F : Ultrafilter ι)    (N : ℕ) (H : ∀ᶠ i in F, Finite (R i) ∧ Nat.card (R i) < N)    (hcont : ∀ᶠ i in F, ContinuousSMul R₀ (R i)) :    ∀ᶠ i in F, Nonempty (UltraProduct R F ≃ₐ[R₀] R i) := by  classical  have : ∀ᶠ i in F, ∃ (α : TopologicalAlgebraTypeCardLT R₀ N)    (e : R i ≃ₐ[R₀] Fin α.1), IsHomeomorph e := by    filter_upwards [H, hcont] with i ⟨h₁, h₂⟩ h₃    exact ⟨_, TopologicalAlgebraTypeCardLT.equivOfAlgebra N _ h₂,      TopologicalAlgebraTypeCardLT.isHomeomorph_equivOfAlgebra N _ h₂⟩  obtain ⟨a, ha⟩ := Ultrafilter.eventually_exists_iff.mp this  let g (i) := if h : Nonempty (R i ≃ₐ[R₀] Fin a.1) then h.some.symm.toLinearMap else 0  let e := LinearEquiv.ofBijective _    (UltraProduct.bijective_of_eventually_bijective (R₀ := R₀) (M := R) (M₀ := Fin a.1) g F    (by filter_upwards [ha] with i hi; unfold g;        rw [dif_pos ⟨hi.choose⟩]; exact AlgEquiv.bijective _))  let e' : Fin ↑a.fst ≃ₐ[R₀] UltraProduct R F := by    refine AlgEquiv.ofLinearEquiv e ?_ ?_    · rw [← (π R F).map_one]      refine UltraProduct.πₗ_eq_iff.mpr ?_      filter_upwards [ha] with i hi      simp only [g, LinearMap.pi_apply, Pi.one_apply, dif_pos (Nonempty.intro (hi.choose)),        AlgEquiv.toLinearMap_apply, map_one]    · intro x y      change _ = π R F _ * π R F _      rw [← map_mul]      refine UltraProduct.πₗ_eq_iff.mpr ?_      filter_upwards [ha] with i hi      simp only [LinearMap.pi_apply, dif_pos (Nonempty.intro (hi.choose)),        AlgEquiv.toLinearMap_apply, map_mul, Pi.mul_apply, g]  filter_upwards [ha] with i ⟨e, he⟩  exact ⟨e'.symm.trans e.symm⟩