case intro.mk
R : Type u
M : Type v
N : Type w
inst✝⁷ : CommRing R
inst✝⁶ : StrongRankCondition R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : Module.Free R M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : Module.Free R N
fst✝ : Type v
bM : Basis fst✝ R M
⊢ Module.rank R (M ⊗[R] N) = Cardinal.lift (Module.rank R M) * Cardinal.lift (Module.rank R N)
R : Type u
M : Type v
N : Type w
inst✝⁷ : CommRing R
inst✝⁶ : StrongRankCondition R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : Module.Free R M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : Module.Free R N
⊢ Module.rank R (M ⊗[R] N) = Cardinal.lift (Module.rank R M) * Cardinal.lift (Module.rank R N)
obtain ⟨⟨_, bM⟩⟩ := Module.Free.exists_basis (R := R) (M := M)
case intro.mk.intro.mk
R : Type u
M : Type v
N : Type w
inst✝⁷ : CommRing R
inst✝⁶ : StrongRankCondition R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : Module.Free R M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : Module.Free R N
fst✝¹ : Type v
bM : Basis fst✝¹ R M
fst✝ : Type w
bN : Basis fst✝ R N
⊢ Module.rank R (M ⊗[R] N) = Cardinal.lift (Module.rank R M) * Cardinal.lift (Module.rank R N)
case intro.mk
R : Type u
M : Type v
N : Type w
inst✝⁷ : CommRing R
inst✝⁶ : StrongRankCondition R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : Module.Free R M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : Module.Free R N
fst✝ : Type v
bM : Basis fst✝ R M
⊢ Module.rank R (M ⊗[R] N) = Cardinal.lift (Module.rank R M) * Cardinal.lift (Module.rank R N)
obtain ⟨⟨_, bN⟩⟩ := Module.Free.exists_basis (R := R) (M := N)
no goals
case intro.mk.intro.mk
R : Type u
M : Type v
N : Type w
inst✝⁷ : CommRing R
inst✝⁶ : StrongRankCondition R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : Module.Free R M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : Module.Free R N
fst✝¹ : Type v
bM : Basis fst✝¹ R M
fst✝ : Type w
bN : Basis fst✝ R N
⊢ Module.rank R (M ⊗[R] N) = Cardinal.lift (Module.rank R M) * Cardinal.lift (Module.rank R N)
rw [← bM.mk_eq_rank'', ← bN.mk_eq_rank'', ← (bM.tensorProduct bN).mk_eq_rank'', Cardinal.mk_prod]