Theorem: base_change_module_rank_preserved (AntLorentz/BaseChange.lean)

State before:
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)
Tactic:
obtain ⟨⟨_, bM⟩⟩ := Module.Free.exists_basis (R := k) (M := M)
State after:
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)

State before:
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)
Tactic:
rw [← bM.mk_eq_rank'', (bM.base_change (A := A)).mk_eq_rank'']
State after:
no goals