[GOAL]
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)
[PROOFSTEP]
obtain ⟨_, b⟩ := Module.Free.exists_basis (R := F) (M := K)
[GOAL]
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)
[PROOFSTEP]
obtain ⟨_, c⟩ := Module.Free.exists_basis (R := K) (M := A)
[GOAL]
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)
[PROOFSTEP]
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}]
[GOAL]
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
[PROOFSTEP]
convert lift_rank_mul_lift_rank F K A
[GOAL]
case h.e'_2.h.e'_5
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 = lift (Module.rank F K)
[PROOFSTEP]
rw [lift_id]
[GOAL]
case h.e'_2.h.e'_6
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 K A = lift (Module.rank K A)
[PROOFSTEP]
rw [lift_id]
[GOAL]
case h.e'_3
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 A = lift (Module.rank F A)
[PROOFSTEP]
rw [lift_id]
[GOAL]
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
inst✝¹ : Module.Finite F K
inst✝ : Module.Finite K A
⊢ finrank F K * finrank K A = finrank F A
[PROOFSTEP]
letI := nontrivial_of_invariantBasisNumber F
[GOAL]
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
inst✝¹ : Module.Finite F K
inst✝ : Module.Finite K A
this : Nontrivial F := nontrivial_of_invariantBasisNumber F
⊢ finrank F K * finrank K A = finrank F A
[PROOFSTEP]
let b := Module.Free.chooseBasis F K
[GOAL]
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
inst✝¹ : Module.Finite F K
inst✝ : Module.Finite K A
this : Nontrivial F := nontrivial_of_invariantBasisNumber F
b : Basis (Module.Free.ChooseBasisIndex F K) F K := Module.Free.chooseBasis F K
⊢ finrank F K * finrank K A = finrank F A
[PROOFSTEP]
let c := Module.Free.chooseBasis K A
[GOAL]
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
inst✝¹ : Module.Finite F K
inst✝ : Module.Finite K A
this : Nontrivial F := nontrivial_of_invariantBasisNumber F
b : Basis (Module.Free.ChooseBasisIndex F K) F K := Module.Free.chooseBasis F K
c : Basis (Module.Free.ChooseBasisIndex K A) K A := Module.Free.chooseBasis K A
⊢ finrank F K * finrank K A = finrank F A
[PROOFSTEP]
rw [finrank_eq_card_basis b, finrank_eq_card_basis c, finrank_eq_card_basis (b.smul c), Fintype.card_prod]
[GOAL]
F : Type u
K : Type v
A : Type w
inst✝⁶ : Field F
inst✝⁵ : DivisionRing K
inst✝⁴ : AddCommGroup A
inst✝³ : Algebra F K
inst✝² : Module K A
inst✝¹ : Module F A
inst✝ : IsScalarTower F K A
hf : FiniteDimensional F A
b : Finset A
hb : span F ↑b = ⊤
⊢ restrictScalars F (span K ↑b) = restrictScalars F ⊤
[PROOFSTEP]
rw [Submodule.restrictScalars_top, eq_top_iff, ← hb, Submodule.span_le]
[GOAL]
F : Type u
K : Type v
A : Type w
inst✝⁶ : Field F
inst✝⁵ : DivisionRing K
inst✝⁴ : AddCommGroup A
inst✝³ : Algebra F K
inst✝² : Module K A
inst✝¹ : Module F A
inst✝ : IsScalarTower F K A
hf : FiniteDimensional F A
b : Finset A
hb : span F ↑b = ⊤
⊢ ↑b ⊆ ↑(restrictScalars F (span K ↑b))
[PROOFSTEP]
exact Submodule.subset_span
[GOAL]
F : Type u
K : Type v
A : Type w
inst✝⁷ : Field F
inst✝⁶ : DivisionRing K
inst✝⁵ : AddCommGroup A
inst✝⁴ : Algebra F K
inst✝³ : Module K A
inst✝² : Module F A
inst✝¹ : IsScalarTower F K A
inst✝ : FiniteDimensional F K
⊢ finrank F K * finrank K A = finrank F A
[PROOFSTEP]
by_cases hA : FiniteDimensional K A
[GOAL]
case pos
F : Type u
K : Type v
A : Type w
inst✝⁷ : Field F
inst✝⁶ : DivisionRing K
inst✝⁵ : AddCommGroup A
inst✝⁴ : Algebra F K
inst✝³ : Module K A
inst✝² : Module F A
inst✝¹ : IsScalarTower F K A
inst✝ : FiniteDimensional F K
hA : FiniteDimensional K A
⊢ finrank F K * finrank K A = finrank F A
[PROOFSTEP]
replace hA : FiniteDimensional K A := hA
[GOAL]
case pos
F : Type u
K : Type v
A : Type w
inst✝⁷ : Field F
inst✝⁶ : DivisionRing K
inst✝⁵ : AddCommGroup A
inst✝⁴ : Algebra F K
inst✝³ : Module K A
inst✝² : Module F A
inst✝¹ : IsScalarTower F K A
inst✝ : FiniteDimensional F K
hA : FiniteDimensional K A
⊢ finrank F K * finrank K A = finrank F A
[PROOFSTEP]
rw [finrank_mul_finrank']
[GOAL]
case neg
F : Type u
K : Type v
A : Type w
inst✝⁷ : Field F
inst✝⁶ : DivisionRing K
inst✝⁵ : AddCommGroup A
inst✝⁴ : Algebra F K
inst✝³ : Module K A
inst✝² : Module F A
inst✝¹ : IsScalarTower F K A
inst✝ : FiniteDimensional F K
hA : ¬FiniteDimensional K A
⊢ finrank F K * finrank K A = finrank F A
[PROOFSTEP]
rw [finrank_of_infinite_dimensional hA, mul_zero, finrank_of_infinite_dimensional]
[GOAL]
case neg
F : Type u
K : Type v
A : Type w
inst✝⁷ : Field F
inst✝⁶ : DivisionRing K
inst✝⁵ : AddCommGroup A
inst✝⁴ : Algebra F K
inst✝³ : Module K A
inst✝² : Module F A
inst✝¹ : IsScalarTower F K A
inst✝ : FiniteDimensional F K
hA : ¬FiniteDimensional K A
⊢ ¬FiniteDimensional F A
[PROOFSTEP]
exact mt (@right F K A _ _ _ _ _ _ _) hA
[GOAL]
F : Type u
K✝ : Type v
A✝ : Type w
inst✝⁹ : Field F
inst✝⁸ : DivisionRing K✝
inst✝⁷ : AddCommGroup A✝
inst✝⁶ : Algebra F K✝
inst✝⁵ : Module K✝ A✝
inst✝⁴ : Module F A✝
inst✝³ : IsScalarTower F K✝ A✝
A : Type u_1
inst✝² : Ring A
inst✝¹ : IsDomain A
inst✝ : Algebra F A
hp : Nat.Prime (finrank F A)
K : Subalgebra F A
⊢ K = ⊥ ∨ K = ⊤
[PROOFSTEP]
haveI : FiniteDimensional _ _ := finiteDimensional_of_finrank hp.pos
[GOAL]
F : Type u
K✝ : Type v
A✝ : Type w
inst✝⁹ : Field F
inst✝⁸ : DivisionRing K✝
inst✝⁷ : AddCommGroup A✝
inst✝⁶ : Algebra F K✝
inst✝⁵ : Module K✝ A✝
inst✝⁴ : Module F A✝
inst✝³ : IsScalarTower F K✝ A✝
A : Type u_1
inst✝² : Ring A
inst✝¹ : IsDomain A
inst✝ : Algebra F A
hp : Nat.Prime (finrank F A)
K : Subalgebra F A
this : FiniteDimensional F A
⊢ K = ⊥ ∨ K = ⊤
[PROOFSTEP]
letI := divisionRingOfFiniteDimensional F K
[GOAL]
F : Type u
K✝ : Type v
A✝ : Type w
inst✝⁹ : Field F
inst✝⁸ : DivisionRing K✝
inst✝⁷ : AddCommGroup A✝
inst✝⁶ : Algebra F K✝
inst✝⁵ : Module K✝ A✝
inst✝⁴ : Module F A✝
inst✝³ : IsScalarTower F K✝ A✝
A : Type u_1
inst✝² : Ring A
inst✝¹ : IsDomain A
inst✝ : Algebra F A
hp : Nat.Prime (finrank F A)
K : Subalgebra F A
this✝ : FiniteDimensional F A
this : DivisionRing { x // x ∈ K } := divisionRingOfFiniteDimensional F { x // x ∈ K }
⊢ K = ⊥ ∨ K = ⊤
[PROOFSTEP]
refine' (hp.eq_one_or_self_of_dvd _ ⟨_, (finrank_mul_finrank F K A).symm⟩).imp _ fun h => _
[GOAL]
case refine'_1
F : Type u
K✝ : Type v
A✝ : Type w
inst✝⁹ : Field F
inst✝⁸ : DivisionRing K✝
inst✝⁷ : AddCommGroup A✝
inst✝⁶ : Algebra F K✝
inst✝⁵ : Module K✝ A✝
inst✝⁴ : Module F A✝
inst✝³ : IsScalarTower F K✝ A✝
A : Type u_1
inst✝² : Ring A
inst✝¹ : IsDomain A
inst✝ : Algebra F A
hp : Nat.Prime (finrank F A)
K : Subalgebra F A
this✝ : FiniteDimensional F A
this : DivisionRing { x // x ∈ K } := divisionRingOfFiniteDimensional F { x // x ∈ K }
⊢ finrank F { x // x ∈ K } = 1 → K = ⊥
[PROOFSTEP]
exact Subalgebra.eq_bot_of_finrank_one
[GOAL]
case refine'_2
F : Type u
K✝ : Type v
A✝ : Type w
inst✝⁹ : Field F
inst✝⁸ : DivisionRing K✝
inst✝⁷ : AddCommGroup A✝
inst✝⁶ : Algebra F K✝
inst✝⁵ : Module K✝ A✝
inst✝⁴ : Module F A✝
inst✝³ : IsScalarTower F K✝ A✝
A : Type u_1
inst✝² : Ring A
inst✝¹ : IsDomain A
inst✝ : Algebra F A
hp : Nat.Prime (finrank F A)
K : Subalgebra F A
this✝ : FiniteDimensional F A
this : DivisionRing { x // x ∈ K } := divisionRingOfFiniteDimensional F { x // x ∈ K }
h : finrank F { x // x ∈ K } = finrank F A
⊢ K = ⊤
[PROOFSTEP]
exact Algebra.toSubmodule_eq_top.1 (eq_top_of_finrank_eq <| K.finrank_toSubmodule.trans h)
