obtain ⟨⟨_, bM⟩⟩ := Module.Free.exists_basis (R := k) (M := M)
k : Type u_3
M : Type (max u_1 u_2)
A : Type u_1
inst✝¹⁰ : Field k
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module k M
inst✝⁷ : Ring A
inst✝⁶ : Algebra k A
inst✝⁵ : Module A M
inst✝⁴ : IsScalarTower k A M
inst✝³ : StrongRankCondition A
inst✝² : Module.Free k M
inst✝¹ : Module.Free A M
inst✝ : Module.Free k A
⊢ Module.rank k M = Module.rank A (A ⊗[k] M)
case intro.mk
k : Type u_3
M : Type (max u_1 u_2)
A : Type u_1
inst✝¹⁰ : Field k
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module k M
inst✝⁷ : Ring A
inst✝⁶ : Algebra k A
inst✝⁵ : Module A M
inst✝⁴ : IsScalarTower k A M
inst✝³ : StrongRankCondition A
inst✝² : Module.Free k M
inst✝¹ : Module.Free A M
inst✝ : Module.Free k A
fst✝ : Type (max u_1 u_2)
bM : Basis fst✝ k M
⊢ Module.rank k M = Module.rank A (A ⊗[k] M)