Use FiniteDimensional.finrank_mul_finrank for IntermediateFi

Stream: new members

[Ludwig Monnerjahn]

How can I applv FiniteDimensional.finrank_mul_finrank with extendScalars?

open IntermediateField
lemma mulfinrank_help (R K L: IntermediateField ℚ ℂ) (h₁: R ≤ K) (h₂: K ≤ L) : FiniteDimensional.finrank R (extendScalars h₁) *
    FiniteDimensional.finrank (extendScalars h₁) (extendScalars h₂) = FiniteDimensional.finrank R (extendScalars (Trans.trans h₁ h₂)) := by
    sorry