IntermediateField_finiteDimensional_adjoin_of_linearDisjoint_of_transcendental.lean

theorem linearIndependent_pow_mul {ι : Type*} [Finite ι] {x : F₀} (hx : Transcendental K₀ x)
    {y : ι → F₀} (hy : LinearIndependent K₀⟮x⟯ y) (d : ℕ) :
    LinearIndependent K₀ (fun q : ι × Fin d => x ^ (q.2 : ℕ) * y q.1) := by
  classical
  let _ : Fintype ι := Fintype.ofFinite ι
  rw [Fintype.linearIndependent_iff]
  intro c hc
  set Pp : ι → K₀[X] := fun i => ∑ k : Fin d, C (c (i, k)) * X ^ (k : ℕ) with hPp
  have hmem : ∀ i, aeval x (Pp i) ∈ K₀⟮x⟯ := fun i => by
    apply algebra_adjoin_le_adjoin K₀ _
    rw [Algebra.adjoin_singleton_eq_range_aeval]
    exact ⟨Pp i, rfl⟩
  set r : ι → K₀⟮x⟯ := fun i => ⟨aeval x (Pp i), hmem i⟩ with hr
  have hexp : ∀ i, (r i • y i : F₀) = ∑ k : Fin d, c (i, k) • (x ^ (k : ℕ) * y i) := by
    intro i
    change aeval x (Pp i) * y i = _
    simp only [hPp, map_sum, map_mul, aeval_C, map_pow, aeval_X, Finset.sum_mul]
    refine Finset.sum_congr rfl fun k _ => ?_
    rw [Algebra.smul_def, mul_assoc]
  have hsum : ∑ i, r i • y i = 0 := by
    rw [Finset.sum_congr rfl fun i _ => hexp i, ← hc, Fintype.sum_prod_type]
  rw [Fintype.linearIndependent_iff] at hy
  have hr0 := hy r hsum
  intro q
  obtain ⟨i, k⟩ := q
  have hPi : Pp i = 0 := by
    have h1 : aeval x (Pp i) = 0 := by
      have := congrArg (fun z : K₀⟮x⟯ => (z : F₀)) (hr0 i)
      exact this
    exact (transcendental_iff.mp hx) _ h1
  have hcoeff : (Pp i).coeff k = c (i, k) := by
    simp only [hPp, finsetSum_coeff, coeff_C_mul_X_pow]
    rw [Finset.sum_eq_single k]
    · simp
    · intro k' _ hk'
      rw [ite_eq_right]
      intro h
      exact hk' (Fin.ext h).symm
    · intro h; exact absurd (Finset.mem_univ k) h
  rw [← hcoeff, hPi, coeff_zero]

theorem finiteDimensional_adjoin_of_linearIndependent
    (hld : ∀ (n : ℕ) (b : Fin n → F₀), LinearIndependent K₀ b →
      LinearIndependent L (fun i => algebraMap F₀ F (b i)))
    (x : F₀) (hx : Transcendental K₀ x) (x' : F) (hx' : algebraMap F₀ F x = x')
    [hfd : FiniteDimensional L⟮x'⟯ F] :
    FiniteDimensional K₀⟮x⟯ F₀ := by
  classical
  set m := Module.finrank L⟮x'⟯ F with hm
  suffices h : Module.rank K₀⟮x⟯ F₀ ≤ m by
    have := lt_of_le_of_lt h (Cardinal.natCast_lt_aleph0 (n := m))
    exact Module.rank_lt_aleph0_iff.mp this
  apply rank_le
  intro s hs
  suffices hL : LinearIndependent L⟮x'⟯ (fun i : s => algebraMap F₀ F (i : F₀)) by
    have := hL.fintype_card_le_finrank
    simpa using this
  rw [← LinearIndependent.iff_fractionRing (Algebra.adjoin L {x'}) L⟮x'⟯,
    Fintype.linearIndependent_iff]
  intro g hg
  have hgi : ∀ i, ∃ p : L[X], aeval x' p = (g i : F) := fun i => by
    have h2 : (g i : F) ∈ (aeval x' : L[X] →ₐ[L] F).range := by
      rw [← Algebra.adjoin_singleton_eq_range_aeval]; exact (g i).2
    obtain ⟨p, hp⟩ := h2
    exact ⟨p, hp⟩
  choose p hp using hgi
  set d := Finset.univ.sup (fun i : s => (p i).natDegree) + 1 with hd
  have hdeg : ∀ i, (p i).natDegree < d := fun i =>
    Nat.lt_succ_of_le (Finset.le_sup (f := fun i : s => (p i).natDegree) (Finset.mem_univ i))
  have hK := linearIndependent_pow_mul (K₀ := K₀) hx hs d
  have hLind : LinearIndependent L (fun q : s × Fin d => algebraMap F₀ F (x ^ (q.2 : ℕ) * (q.1 :
    F₀))) := by
    set e := Fintype.equivFin (↥s × Fin d) with he
    have h1 := hK.comp e.symm e.symm.injective
    have h2 := hld _ _ h1
    have h3 := h2.comp e e.injective
    convert h3 using 1
    ext q
    simp [Function.comp, Equiv.symm_apply_apply]
  rw [Fintype.linearIndependent_iff] at hLind
  have hrel : ∑ q : s × Fin d, (p q.1).coeff q.2 • algebraMap F₀ F (x ^ (q.2 : ℕ) * (q.1 : F₀)) = 0
    := by
    rw [Fintype.sum_prod_type]
    have hi : ∀ i : s, ∑ k : Fin d, (p i).coeff k • algebraMap F₀ F (x ^ (k : ℕ) * (i : F₀)) =
        (g i : F) * algebraMap F₀ F i := by
      intro i
      rw [← hp i, aeval_eq_sum_range' (hdeg i), Finset.sum_mul,
        ← Fin.sum_univ_eq_sum_range (fun k => (p i).coeff k • x' ^ k * algebraMap F₀ F i)]
      refine Finset.sum_congr rfl fun k _ => ?_
      rw [map_mul, map_pow, hx', Algebra.smul_def, Algebra.smul_def, mul_assoc]
    rw [Finset.sum_congr rfl fun i _ => hi i, ← hg]
    refine Finset.sum_congr rfl fun i _ => ?_
    rw [Subalgebra.smul_def, smul_eq_mul]
  have hcoeff := hLind _ hrel
  intro i
  apply Subtype.ext
  change (g i : F) = 0
  rw [← hp i]
  have : p i = 0 := by
    ext k
    rw [coeff_zero]
    by_cases hk : k < d
    · exact hcoeff (i, ⟨k, hk⟩)
    · exact coeff_eq_zero_of_natDegree_lt (lt_of_lt_of_le (hdeg i) (not_lt.mp hk))
  rw [this, map_zero]

theorem _root_.IntermediateField.finiteDimensional_adjoin_of_linearDisjoint_of_transcendental
    {K₀ L F₀ F : Type*} [Field K₀] [Field L] [Field F₀] [Field F]
    [Algebra K₀ F₀] [Algebra L F] [Algebra F₀ F]
    (hld : ∀ (n : ℕ) (b : Fin n → F₀), LinearIndependent K₀ b →
      LinearIndependent L (fun i => algebraMap F₀ F (b i)))
    (x : F₀) (hx : Transcendental K₀ x)
    [FiniteDimensional (IntermediateField.adjoin L ({algebraMap F₀ F x} : Set F)) F] :
    FiniteDimensional (IntermediateField.adjoin K₀ ({x} : Set F₀)) F₀ :=
  R1AF8LD.finiteDimensional_adjoin_of_linearIndependent hld x hx (algebraMap F₀ F x) rfl