case intro.mk
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
fst✝ : Type v
b : Basis fst✝ F K
⊢ lift (Module.rank F K) * lift (Module.rank K A) = lift (Module.rank F A)
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
⊢ lift (Module.rank F K) * lift (Module.rank K A) = lift (Module.rank F A)
obtain ⟨_, b⟩ := Module.Free.exists_basis (R := F) (M := K)
case intro.mk.intro.mk
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
fst✝¹ : Type v
b : Basis fst✝¹ F K
fst✝ : Type w
c : Basis fst✝ K A
⊢ lift (Module.rank F K) * lift (Module.rank K A) = lift (Module.rank F A)
case intro.mk
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
fst✝ : Type v
b : Basis fst✝ F K
⊢ lift (Module.rank F K) * lift (Module.rank K A) = lift (Module.rank F A)
obtain ⟨_, c⟩ := Module.Free.exists_basis (R := K) (M := A)
no goals
case intro.mk.intro.mk
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
fst✝¹ : Type v
b : Basis fst✝¹ F K
fst✝ : Type w
c : Basis fst✝ K A
⊢ lift (Module.rank F K) * lift (Module.rank K A) = lift (Module.rank F A)
rw [← (Module.rank F K).lift_id, ← b.mk_eq_rank, ← (Module.rank K A).lift_id, ← c.mk_eq_rank, ←
  lift_umax.{w, v}, ← (b.smul c).mk_eq_rank, mk_prod, lift_mul, lift_lift, lift_lift, lift_lift,
  lift_lift, lift_umax.{v, w}]