Algebra_trdeg_quotient_lt.lean

theorem algebraicIndependent_option_elim {ι : Type*} (I : Ideal R) {y : ι → R}
    (hy : AlgebraicIndependent K (Ideal.Quotient.mk I ∘ y)) {a : R} (haI : a ∈ I) (ha : a ≠ 0) :
    AlgebraicIndependent K (fun o : Option ι => o.elim a y) := by
  have hy' : AlgebraicIndependent K y := hy.of_comp (Ideal.Quotient.mkₐ K I)
  rw [hy'.option_iff_transcendental]
  have hinj : ∀ b : Algebra.adjoin K (Set.range y), (b : R) ∈ I → b = 0 := by
    rintro ⟨b, hb⟩ hbI
    obtain ⟨P, hPb⟩ : ∃ P : MvPolynomial ι K, MvPolynomial.aeval y P = b := by
      have hb' := hb
      rwa [Algebra.adjoin_range_eq_range_aeval] at hb'
    have h0 : MvPolynomial.aeval (Ideal.Quotient.mk I ∘ y) P = 0 := by
      change MvPolynomial.aeval (fun i => Ideal.Quotient.mkₐ K I (y i)) P = 0
      rw [← MvPolynomial.comp_aeval (f := y) (φ := Ideal.Quotient.mkₐ K I), AlgHom.comp_apply,
        Ideal.Quotient.mkₐ_eq_mk, Ideal.Quotient.eq_zero_iff_mem, hPb]
      exact hbI
    have hP : P = 0 := hy (by rw [h0, map_zero])
    exact Subtype.ext (show b = 0 by rw [← hPb, hP, map_zero])
  rintro ⟨q, hq0, hqa⟩
  obtain ⟨q', hq, hndvd⟩ := q.exists_eq_pow_rootMultiplicity_mul_and_not_dvd hq0 0
  rw [map_zero, sub_zero] at hq hndvd
  have hq'a : aeval a q' = 0 := by
    rw [hq, map_mul, map_pow, aeval_X] at hqa
    exact (mul_eq_zero.mp hqa).resolve_left (pow_ne_zero _ ha)
  have hc : algebraMap (Algebra.adjoin K (Set.range y)) R (q'.coeff 0) = -(a * aeval a q'.divX) :=
    by
    have := congrArg (aeval a) q'.X_mul_divX_add
    rw [map_add, map_mul, aeval_X, aeval_C, hq'a, ← eq_sub_iff_add_eq', zero_sub] at this
    exact this
  have hcI : ((q'.coeff 0 : Algebra.adjoin K (Set.range y)) : R) ∈ I := by
    rw [show ((q'.coeff 0 : Algebra.adjoin K (Set.range y)) : R) =
      algebraMap (Algebra.adjoin K (Set.range y)) R (q'.coeff 0) from rfl, hc]
    exact I.neg_mem (I.mul_mem_right _ haI)
  exact hndvd (X_dvd_iff.mpr (hinj _ hcI))

theorem _root_.Algebra.trdeg_quotient_lt {K : Type u} {R : Type v} [Field K] [CommRing R] [IsDomain
  R] [Algebra K R]
    [Algebra.FiniteType K R] (I : Ideal R) (hI : I ≠ ⊥) (hI' : I ≠ ⊤) :
    Algebra.trdeg K (R ⧸ I) < Algebra.trdeg K R