∀ (R : Type u_1) [inst : CommRing R] {A : Type u} {B : Type u_2} [inst_1 : CommRing A] [inst_2 : Algebra R A]
  [inst_3 : CommRing B] [inst_4 : Algebra A B] (D : Algebra.Smooth.DescentAux✝ A B),
  Algebra.Smooth.DescentAux.subalgebra✝ R D =
    Algebra.adjoin R
      ((Algebra.Smooth.DescentAux.P✝ D).coeffs ∪
        (((⋃ i, ↑(Algebra.Smooth.DescentAux.h✝ D i).coeffs) ∪
            ⋃ i, ⋃ x ∈ (Algebra.Smooth.DescentAux.q✝ D i).coeffs, ↑(MvPolynomial.coeffs x)) ∪
          ⋃ i, ⋃ x ∈ (Algebra.Smooth.DescentAux.p✝ D i).coeffs, ↑x.coeffs))