no goals
F✝ : Type u
K✝ : Type v
A✝ : Type w
inst✝²¹ : CommRing F✝
inst✝²⁰ : Ring K✝
inst✝¹⁹ : AddCommGroup A✝
inst✝¹⁸ : Algebra F✝ K✝
inst✝¹⁷ : Module K✝ A✝
inst✝¹⁶ : Module F✝ A✝
inst✝¹⁵ : IsScalarTower F✝ K✝ A✝
inst✝¹⁴ : StrongRankCondition F✝
inst✝¹³ : StrongRankCondition K✝
inst✝¹² : Module.Free F✝ K✝
inst✝¹¹ : Module.Free K✝ A✝
F : Type u
K A : Type v
inst✝¹⁰ : CommRing F
inst✝⁹ : Ring K
inst✝⁸ : AddCommGroup A
inst✝⁷ : Algebra F K
inst✝⁶ : Module K A
inst✝⁵ : Module F A
inst✝⁴ : IsScalarTower F K A
inst✝³ : StrongRankCondition F
inst✝² : StrongRankCondition K
inst✝¹ : Module.Free F K
inst✝ : Module.Free K A
⊢ Module.rank F K * Module.rank K A = Module.rank F A
convert lift_rank_mul_lift_rank F K A <;> rw [lift_id]