no goals
S : Type ?u.259837
T : Type ?u.259840
R : Type u_1
inst✝¹ : CommRing R
c₁ c₂ r x y z : R
a b c : ℍ[R,c₁,c₂]
inst✝ : StrongRankCondition R
⊢ FiniteDimensional.finrank R ℍ[R,c₁,c₂] = 4
rw [FiniteDimensional.finrank, rank_eq_four, Cardinal.toNat_ofNat]