import Mathlib.FieldTheory.Adjoin
import Mathlib.LinearAlgebra.TensorProduct.Subalgebra
import Mathlib.Algebra.MvPolynomial.Cardinal
import Mathlib.RingTheory.Localization.Cardinality
import Mathlib.RingTheory.AlgebraicIndependent
import Mathlib.Data.Fin.Tuple.Reflection

open scoped Classical TensorProduct

open FiniteDimensional IntermediateField

noncomputable section

universe u v w

variable {F : Type u} {E : Type v} [Field F] [Field E] [Algebra F E]

variable {A B : IntermediateField F E}

variable (L : Type w) [Field L] [Algebra F L] [Algebra L E] [IsScalarTower F L E]

-- already in mathlib
variable (A B) in
private lemma _root_.IntermediateField.rank_sup_le_of_isAlgebraic
    (halg : Algebra.IsAlgebraic F A ∨ Algebra.IsAlgebraic F B) :
    Module.rank F ↥(A ⊔ B) ≤ Module.rank F A * Module.rank F B := by
  have := A.toSubalgebra.rank_sup_le_of_free B.toSubalgebra
  rwa [← sup_toSubalgebra_of_isAlgebraic A B halg] at this

-- already in mathlib with different name
theorem _root_.FractionRing.card (R : Type u) [CommRing R] :
    Cardinal.mk (FractionRing R) = Cardinal.mk R :=
  (IsLocalization.card (FractionRing R) (nonZeroDivisors R) (le_refl _)).symm

-- TODO: move to suitable place
theorem _root_.rank_fractionRing_mvPolynomial_eq {σ : Type u} {F : Type v} [Field F] [Nonempty σ] :
    Module.rank F (FractionRing (MvPolynomial σ F)) =
      max (max (Cardinal.lift.{u} (Cardinal.mk F)) (Cardinal.lift.{v} (Cardinal.mk σ)))
        Cardinal.aleph0 := by
  refine le_antisymm ?_ ?_
  · refine (rank_le_card _ _).trans ?_
    rw [FractionRing.card, MvPolynomial.cardinal_mk_eq_max_lift]
  · have hinj := NoZeroSMulDivisors.algebraMap_injective (MvPolynomial σ F)
      (FractionRing (MvPolynomial σ F))
    have h1 := IsScalarTower.toAlgHom F (MvPolynomial σ F) (FractionRing (MvPolynomial σ F))
      |>.toLinearMap.rank_le_of_injective hinj
    simp_rw [Cardinal.lift_id'.{u, v} _ ▸ (MvPolynomial.basisMonomials σ F).mk_eq_rank.symm] at h1
    rw [Cardinal.lift_umax.{u, v}, Cardinal.mk_finsupp_nat, Cardinal.lift_max,
      Cardinal.lift_aleph0, max_le_iff] at h1
    obtain ⟨i⟩ := ‹Nonempty σ›
    let x := algebraMap (MvPolynomial σ F) (FractionRing (MvPolynomial σ F)) (MvPolynomial.X i)
    have hx : Transcendental F x := (transcendental_algebraMap_iff hinj).2
      (MvPolynomial.transcendental_X F i)
    have h2 := hx.linearIndependent_sub_inv.cardinal_lift_le_rank
    rw [Cardinal.lift_id'.{v, u} _, Cardinal.lift_umax.{v, u}] at h2
    exact max_le_iff.2 ⟨max_le_iff.2 ⟨h2, h1.1⟩, h1.2⟩