awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Smooth.NoetherianDescent
Goal:
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 : DescentAux A B
inst_5 : Finite D.vars
inst_6 : Finite D.rels
i : D.rels
⊢ Set.Finite.{u} (α := A) (⋃ x ∈ (D.p i).coeffs, (↑x.coeffs : Set A))

Tactic:
exact Set.Finite.biUnion (Finset.finite_toSet _) (fun i hi ↦ Finset.finite_toSet _)

Premises used: Finset.finite_toSet, Set.Finite.biUnion
-- Module: Mathlib.RingTheory.Smooth.NoetherianDescent
Goal:
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 : DescentAux A B
rw : D.P.coeffs ⊆ (↑(subalgebra R D) : Set A)
⊢ D.P.coeffs ⊆ Set.range (ι := ↥(subalgebra R D)) (⇑(algebraMap (↥(subalgebra R D)) A) : (a : ↥(subalgebra R D)) → A)

Tactic:
rw [Subalgebra.setRange_algebraMap]

Premises used: Subalgebra.setRange_algebraMap
-- Module: Mathlib.RingTheory.Smooth.NoetherianDescent
Goal:
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 : DescentAux A B
⊢ D.P.coeffs ⊆ (↑(subalgebra R D) : Set A)

Tactic:
grind [subalgebra, Algebra.subset_adjoin]

Premises used: Algebra.subset_adjoin, _private.0.Algebra.Smooth.DescentAux.subalgebra
-- Module: Mathlib.RingTheory.Smooth.NoetherianDescent
Goal:
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 : DescentAux A B
i : D.vars
⊢ (↑(D.h i).coeffs : Set A) ⊆ ⋃ (i : D.vars), (↑(D.h i).coeffs : Set A)

Tactic:
have : ((D.h i).coeffs : Set _) ⊆ ⋃ i, ((D.h i).coeffs : Set A) :=
    Set.subset_iUnion_of_subset i subset_rfl
-- Module: Mathlib.RingTheory.Smooth.NoetherianDescent
Goal:
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 : DescentAux A B
i : D.vars
this : (↑(D.h i).coeffs : Set A) ⊆ ⋃ (i : D.vars), (↑(D.h i).coeffs : Set A)
rw : (↑(D.h i).coeffs : Set A) ⊆ (↑(subalgebra R D) : Set A)
⊢ (↑(D.h i).coeffs : Set A) ⊆
    Set.range (ι := ↥(subalgebra R D)) (⇑(algebraMap (↥(subalgebra R D)) A) : (a : ↥(subalgebra R D)) → A)

Tactic:
rw [Subalgebra.setRange_algebraMap]

Premises used: Subalgebra.setRange_algebraMap
-- Module: Mathlib.RingTheory.Smooth.NoetherianDescent
Goal:
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 : DescentAux A B
i : D.vars
this : (↑(D.h i).coeffs : Set A) ⊆ ⋃ (i : D.vars), (↑(D.h i).coeffs : Set A)
⊢ (↑(D.h i).coeffs : Set A) ⊆ (↑(subalgebra R D) : Set A)

Tactic:
grind [subalgebra, Algebra.subset_adjoin]

Premises used: Algebra.subset_adjoin, _private.0.Algebra.Smooth.DescentAux.subalgebra
-- Module: Mathlib.RingTheory.Smooth.NoetherianDescent
Goal:
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 : DescentAux A B
i : D.rels
p : MvPolynomial D.vars A
hp : p ∈ (↑(D.p i).coeffs : Set (MvPolynomial D.vars A))
⊢ (↑p.coeffs : Set A) ⊆ ⋃ (i : D.rels), ⋃ x ∈ (D.p i).coeffs, (↑x.coeffs : Set A)

Tactic:
have : (p.coeffs : Set A) ⊆ ⋃ i, ⋃ x ∈ (D.p i).coeffs, ↑x.coeffs :=
    Set.subset_iUnion_of_subset i (Set.subset_iUnion₂_of_subset p hp subset_rfl)
-- Module: Mathlib.RingTheory.Smooth.NoetherianDescent
Goal:
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 : DescentAux A B
i : D.rels
p : MvPolynomial D.vars A
hp : p ∈ (↑(D.p i).coeffs : Set (MvPolynomial D.vars A))
this : (↑p.coeffs : Set A) ⊆ ⋃ (i : D.rels), ⋃ x ∈ (D.p i).coeffs, (↑x.coeffs : Set A)
rw : (↑p.coeffs : Set A) ⊆ (↑(subalgebra R D) : Set A)
⊢ Membership.mem (γ := Set (MvPolynomial D.vars A))
    (Set.range (ι := MvPolynomial D.vars ↥(subalgebra R D))
      (⇑(MvPolynomial.map (algebraMap (↥(subalgebra R D)) A)) :
        (a : MvPolynomial D.vars ↥(subalgebra R D)) → MvPolynomial D.vars A))
    p

Tactic:
rw [MvPolynomial.mem_range_map_iff_coeffs_subset, Subalgebra.setRange_algebraMap]

Premises used: MvPolynomial.mem_range_map_iff_coeffs_subset, Subalgebra.setRange_algebraMap
-- Module: Mathlib.RingTheory.Smooth.NoetherianDescent
Goal:
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 : DescentAux A B
i : D.rels
p : MvPolynomial D.vars A
hp : p ∈ (↑(D.p i).coeffs : Set (MvPolynomial D.vars A))
this : (↑p.coeffs : Set A) ⊆ ⋃ (i : D.rels), ⋃ x ∈ (D.p i).coeffs, (↑x.coeffs : Set A)
⊢ (↑p.coeffs : Set A) ⊆ (↑(subalgebra R D) : Set A)

Tactic:
grind [subalgebra, Algebra.subset_adjoin]

Premises used: Algebra.subset_adjoin, _private.0.Algebra.Smooth.DescentAux.subalgebra
-- Module: Mathlib.RingTheory.Smooth.NoetherianDescent
Goal:
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 : DescentAux A B
i : D.vars
q : MvPolynomial D.vars A
hq : q ∈ (↑(D.q i).coeffs : Set (MvPolynomial D.vars A))
⊢ (↑q.coeffs : Set A) ⊆ ⋃ (i : D.vars), ⋃ x ∈ (D.q i).coeffs, (↑(coeffs x) : Set A)

Tactic:
have : (q.coeffs : Set A) ⊆ ⋃ i, ⋃ x ∈ (D.q i).coeffs, ↑(coeffs x) :=
    Set.subset_iUnion_of_subset i (Set.subset_iUnion₂_of_subset q hq subset_rfl)
-- Module: Mathlib.RingTheory.Smooth.NoetherianDescent
Goal:
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 : DescentAux A B
i : D.vars
q : MvPolynomial D.vars A
hq : q ∈ (↑(D.q i).coeffs : Set (MvPolynomial D.vars A))
this : (↑q.coeffs : Set A) ⊆ ⋃ (i : D.vars), ⋃ x ∈ (D.q i).coeffs, (↑(coeffs x) : Set A)
rw : (↑q.coeffs : Set A) ⊆ (↑(subalgebra R D) : Set A)
⊢ Membership.mem (γ := Set (MvPolynomial D.vars A))
    (Set.range (ι := MvPolynomial D.vars ↥(subalgebra R D))
      (⇑(MvPolynomial.map (algebraMap (↥(subalgebra R D)) A)) :
        (a : MvPolynomial D.vars ↥(subalgebra R D)) → MvPolynomial D.vars A))
    q

Tactic:
rw [MvPolynomial.mem_range_map_iff_coeffs_subset, Subalgebra.setRange_algebraMap]

Premises used: MvPolynomial.mem_range_map_iff_coeffs_subset, Subalgebra.setRange_algebraMap
-- Module: Mathlib.RingTheory.Smooth.NoetherianDescent
Goal:
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 : DescentAux A B
i : D.vars
q : MvPolynomial D.vars A
hq : q ∈ (↑(D.q i).coeffs : Set (MvPolynomial D.vars A))
this : (↑q.coeffs : Set A) ⊆ ⋃ (i : D.vars), ⋃ x ∈ (D.q i).coeffs, (↑(coeffs x) : Set A)
⊢ (↑q.coeffs : Set A) ⊆ (↑(subalgebra R D) : Set A)

Tactic:
grind [subalgebra, Algebra.subset_adjoin]

Premises used: Algebra.subset_adjoin, _private.0.Algebra.Smooth.DescentAux.subalgebra
-- Module: Mathlib.RingTheory.Smooth.NoetherianDescent
Goal:
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 : DescentAux A B
p : (i : D.vars) → MvPolynomial D.vars ↥(subalgebra R D)
hp :
  ∀ (i : D.vars),
    (MvPolynomial.map (algebraMap (↥(subalgebra R D)) A) :
          (a : MvPolynomial D.vars ↥(subalgebra R D)) → MvPolynomial D.vars A)
        (p i) =
      D.h i
⊢ ∃ (σ₀ :
    Presentation.ModelOfHasCoeffs.{u, u_2, 0, 0, u} (R := A) (S := B) (ι := D.vars) (σ := D.rels) (P := D.P)
        ↥(subalgebra R D) →ₐ[↥(subalgebra R D)]
      MvPolynomial D.vars ↥(subalgebra R D) ⧸
        HPow.hPow (α := Ideal (MvPolynomial D.vars ↥(subalgebra R D))) (β := ℕ)
          (RingHom.ker (F :=
            MvPolynomial D.vars ↥(subalgebra R D) →ₐ[↥(subalgebra R D)]
              HasQuotient.Quotient (MvPolynomial D.vars ↥(subalgebra R D)) (B :=
                Ideal (MvPolynomial D.vars ↥(subalgebra R D)))
                (Ideal.span
                  (Set.range (ι := D.rels)
                    (Presentation.relationOfHasCoeffs.{u, u_2, 0, 0, u} (R := A) (S := B) (P := D.P)
                      ↥(subalgebra R D)))))
            (Ideal.Quotient.mkₐ (↥(subalgebra R D))
              (Ideal.span
                (Set.range (ι := D.rels)
                  (Presentation.relationOfHasCoeffs.{u, u_2, 0, 0, u} (R := A) (S := B) (P := D.P)
                    ↥(subalgebra R D))))))
          2),
    AlgHom.comp
        (AlgHom.kerSquareLift
          (Ideal.Quotient.mkₐ (↥(subalgebra R D))
            (Ideal.span
              (Set.range (ι := D.rels)
                (Presentation.relationOfHasCoeffs.{u, u_2, 0, 0, u} (R := A) (S := B) (P := D.P) ↥(subalgebra R D))))))
        σ₀ =
      AlgHom.id (↥(subalgebra R D))
        (Presentation.ModelOfHasCoeffs.{u, u_2, 0, 0, u} (R := A) (S := B) (ι := D.vars) (σ := D.rels) (P := D.P)
          ↥(subalgebra R D))

Tactic:
⟨?_, ?_⟩

Premises used: Exists.intro
-- Module: Mathlib.RingTheory.Smooth.NoetherianDescent
Goal:
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 : DescentAux A B
p : (i : D.vars) → MvPolynomial D.vars ↥(subalgebra R D)
hp :
  ∀ (i : D.vars),
    (MvPolynomial.map (algebraMap (↥(subalgebra R D)) A) :
          (a : MvPolynomial D.vars ↥(subalgebra R D)) → MvPolynomial D.vars A)
        (p i) =
      D.h i
i : D.rels
⊢ Function.Injective (α := MvPolynomial D.vars ↥(subalgebra R D)) (β := MvPolynomial D.vars A)
    (⇑(MvPolynomial.map (algebraMap (↥(subalgebra R D)) A)) :
      (a : MvPolynomial D.vars ↥(subalgebra R D)) → MvPolynomial D.vars A)

Tactic:
have hinj : Function.Injective
        (MvPolynomial.map (σ := D.vars) (algebraMap (D.subalgebra R) A)) :=
      map_injective _ (FaithfulSMul.algebraMap_injective (D.subalgebra R) A)
-- Module: Mathlib.RingTheory.Smooth.NoetherianDescent
Goal:
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 : DescentAux A B
p : (i : D.vars) → MvPolynomial D.vars ↥(subalgebra R D)
hp :
  ∀ (i : D.vars),
    (MvPolynomial.map (algebraMap (↥(subalgebra R D)) A) :
          (a : MvPolynomial D.vars ↥(subalgebra R D)) → MvPolynomial D.vars A)
        (p i) =
      D.h i
i : D.rels
hinj :
  Function.Injective (α := MvPolynomial D.vars ↥(subalgebra R D)) (β := MvPolynomial D.vars A)
    (⇑(MvPolynomial.map (algebraMap (↥(subalgebra R D)) A)) :
      (a : MvPolynomial D.vars ↥(subalgebra R D)) → MvPolynomial D.vars A)
refine_1 :
  ∃ (p_1 : MvPolynomial D.rels (MvPolynomial D.vars ↥(subalgebra R D))),
    p_1.IsHomogeneous 2 ∧
      Eq (α := MvPolynomial D.vars ↥(subalgebra R D))
        ((eval (Presentation.relationOfHasCoeffs.{u, u_2, 0, 0, u} (R := A) (S := B) (P := D.P) ↥(subalgebra R D)) :
              (a : MvPolynomial D.rels (MvPolynomial D.vars ↥(subalgebra R D))) → MvPolynomial D.vars ↥(subalgebra R D))
            p_1 :
          MvPolynomial D.vars ↥(subalgebra R D))
        ((aeval p : (a : MvPolynomial D.vars ↥(subalgebra R D)) → MvPolynomial D.vars ↥(subalgebra R D))
            (Presentation.relationOfHasCoeffs.{u, u_2, 0, 0, u} (R := A) (S := B) (P := D.P) (↥(subalgebra R D)) i) :
          MvPolynomial D.vars ↥(subalgebra R D))
⊢ Membership.mem (α := MvPolynomial D.vars ↥(subalgebra R D))
    (HPow.hPow (α := Ideal (MvPolynomial D.vars ↥(subalgebra R D))) (β := ℕ)
      (Ideal.span
        (Set.range (ι := D.rels)
          (Presentation.relationOfHasCoeffs.{u, u_2, 0, 0, u} (R := A) (S := B) (P := D.P) ↥(subalgebra R D))))
      2)
    ((aeval p : (a : MvPolynomial D.vars ↥(subalgebra R D)) → MvPolynomial D.vars ↥(subalgebra R D))
        (Presentation.relationOfHasCoeffs.{u, u_2, 0, 0, u} (R := A) (S := B) (P := D.P) (↥(subalgebra R D)) i) :
      MvPolynomial D.vars ↥(subalgebra R D))

Tactic:
rw [Ideal.mem_span_pow_iff_exists_isHomogeneous]

Premises used: Ideal.mem_span_pow_iff_exists_isHomogeneous
-- Module: Mathlib.RingTheory.Smooth.NoetherianDescent
Goal:
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 : DescentAux A B
p : (i : D.vars) → MvPolynomial D.vars ↥(subalgebra R D)
hp :
  ∀ (i : D.vars),
    (MvPolynomial.map (algebraMap (↥(subalgebra R D)) A) :
          (a : MvPolynomial D.vars ↥(subalgebra R D)) → MvPolynomial D.vars A)
        (p i) =
      D.h i
i : D.rels
hinj :
  Function.Injective (α := MvPolynomial D.vars ↥(subalgebra R D)) (β := MvPolynomial D.vars A)
    (⇑(MvPolynomial.map (algebraMap (↥(subalgebra R D)) A)) :
      (a : MvPolynomial D.vars ↥(subalgebra R D)) → MvPolynomial D.vars A)
refine_1 :
  ∀ (q : MvPolynomial D.rels (MvPolynomial D.vars ↥(subalgebra R D)))
    (hq :
      (MvPolynomial.map (MvPolynomial.map (algebraMap (↥(subalgebra R D)) A)) :
            (a : MvPolynomial D.rels (MvPolynomial D.vars ↥(subalgebra R D))) →
              MvPolynomial D.rels (MvPolynomial D.vars A))
          q =
        D.p i),
    ∃ (p_1 : MvPolynomial D.rels (MvPolynomial D.vars ↥(subalgebra R D))),
      p_1.IsHomogeneous 2 ∧
        Eq (α := MvPolynomial D.vars ↥(subalgebra R D))
          ((eval (Presentation.relationOfHasCoeffs.{u, u_2, 0, 0, u} (R := A) (S := B) (P := D.P) ↥(subalgebra R D)) :
                (a : MvPolynomial D.rels (MvPolynomial D.vars ↥(subalgebra R D))) →
                  MvPolynomial D.vars ↥(subalgebra R D))
              p_1 :
            MvPolynomial D.vars ↥(subalgebra R D))
          ((aeval p : (a : MvPolynomial D.vars ↥(subalgebra R D)) → MvPolynomial D.vars ↥(subalgebra R D))
              (Presentation.relationOfHasCoeffs.{u, u_2, 0, 0, u} (R := A) (S := B) (P := D.P) (↥(subalgebra R D)) i) :
            MvPolynomial D.vars ↥(subalgebra R D))
⊢ ∃ (p_1 : MvPolynomial D.rels (MvPolynomial D.vars ↥(subalgebra R D))),
    p_1.IsHomogeneous 2 ∧
      Eq (α := MvPolynomial D.vars ↥(subalgebra R D))
        ((eval (Presentation.relationOfHasCoeffs.{u, u_2, 0, 0, u} (R := A) (S := B) (P := D.P) ↥(subalgebra R D)) :
              (a : MvPolynomial D.rels (MvPolynomial D.vars ↥(subalgebra R D))) → MvPolynomial D.vars ↥(subalgebra R D))
            p_1 :
          MvPolynomial D.vars ↥(subalgebra R D))
        ((aeval p : (a : MvPolynomial D.vars ↥(subalgebra R D)) → MvPolynomial D.vars ↥(subalgebra R D))
            (Presentation.relationOfHasCoeffs.{u, u_2, 0, 0, u} (R := A) (S := B) (P := D.P) (↥(subalgebra R D)) i) :
          MvPolynomial D.vars ↥(subalgebra R D))

Tactic:
obtain ⟨q, hq⟩ := (D.p i).mem_range_map_iff_coeffs_subset.mpr (D.coeffs_p_subset R i)

Premises used: Iff.mpr, MvPolynomial.mem_range_map_iff_coeffs_subset, _private.0.Algebra.Smooth.DescentAux.hq, _private.0.Algebra.Smooth.DescentAux.coeffs_p_subset, _private.0.Algebra.Smooth.DescentAux.q
-- Module: Mathlib.RingTheory.Smooth.NoetherianDescent
Goal:
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 : DescentAux A B
p : (i : D.vars) → MvPolynomial D.vars ↥(subalgebra R D)
hp :
  ∀ (i : D.vars),
    (MvPolynomial.map (algebraMap (↥(subalgebra R D)) A) :
          (a : MvPolynomial D.vars ↥(subalgebra R D)) → MvPolynomial D.vars A)
        (p i) =
      D.h i
i : D.rels
hinj :
  Function.Injective (α := MvPolynomial D.vars ↥(subalgebra R D)) (β := MvPolynomial D.vars A)
    (⇑(MvPolynomial.map (algebraMap (↥(subalgebra R D)) A)) :
      (a : MvPolynomial D.vars ↥(subalgebra R D)) → MvPolynomial D.vars A)
q : MvPolynomial D.rels (MvPolynomial D.vars ↥(subalgebra R D))
hq :
  (MvPolynomial.map (MvPolynomial.map (algebraMap (↥(subalgebra R D)) A)) :
        (a : MvPolynomial D.rels (MvPolynomial D.vars ↥(subalgebra R D))) → MvPolynomial D.rels (MvPolynomial D.vars A))
      q =
    D.p i
⊢ ∃ (p_1 : MvPolynomial D.rels (MvPolynomial D.vars ↥(subalgebra R D))),
    p_1.IsHomogeneous 2 ∧
      Eq (α := MvPolynomial D.vars ↥(subalgebra R D))
        ((eval (Presentation.relationOfHasCoeffs.{u, u_2, 0, 0, u} (R := A) (S := B) (P := D.P) ↥(subalgebra R D)) :
              (a : MvPolynomial D.rels (MvPolynomial D.vars ↥(subalgebra R D))) → MvPolynomial D.vars ↥(subalgebra R D))
            p_1 :
          MvPolynomial D.vars ↥(subalgebra R D))
        ((aeval p : (a : MvPolynomial D.vars ↥(subalgebra R D)) → MvPolynomial D.vars ↥(subalgebra R D))
            (Presentation.relationOfHasCoeffs.{u, u_2, 0, 0, u} (R := A) (S := B) (P := D.P) (↥(subalgebra R D)) i) :
          MvPolynomial D.vars ↥(subalgebra R D))

Tactic:
⟨q, .of_map hinj ?_, hinj ?_⟩

Premises used: MvPolynomial.IsHomogeneous.of_map, And.intro, Exists.intro
-- Module: Mathlib.RingTheory.Smooth.NoetherianDescent
Goal:
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 : DescentAux A B
p : (i : D.vars) → MvPolynomial D.vars ↥(subalgebra R D)
hp :
  ∀ (i : D.vars),
    (MvPolynomial.map (algebraMap (↥(subalgebra R D)) A) :
          (a : MvPolynomial D.vars ↥(subalgebra R D)) → MvPolynomial D.vars A)
        (p i) =
      D.h i
i : D.rels
hinj :
  Function.Injective (α := MvPolynomial D.vars ↥(subalgebra R D)) (β := MvPolynomial D.vars A)
    (⇑(MvPolynomial.map (algebraMap (↥(subalgebra R D)) A)) :
      (a : MvPolynomial D.vars ↥(subalgebra R D)) → MvPolynomial D.vars A)
q : MvPolynomial D.rels (MvPolynomial D.vars ↥(subalgebra R D))
hq :
  (MvPolynomial.map (MvPolynomial.map (algebraMap (↥(subalgebra R D)) A)) :
        (a : MvPolynomial D.rels (MvPolynomial D.vars ↥(subalgebra R D))) → MvPolynomial D.rels (MvPolynomial D.vars A))
      q =
    D.p i
refine_1 :
  IsHomogeneous.{0, u} (σ := D.rels) (R := MvPolynomial D.vars A)
    ((MvPolynomial.map (MvPolynomial.map (algebraMap (↥(subalgebra R D)) A)) :
        (a : MvPolynomial D.rels (MvPolynomial D.vars ↥(subalgebra R D))) → MvPolynomial D.rels (MvPolynomial D.vars A))
      q)
    2
refine_1₁ :
  Eq (α := MvPolynomial D.vars A)
    ((MvPolynomial.map (algebraMap (↥(subalgebra R D)) A) :
          (a : MvPolynomial D.vars ↥(subalgebra R D)) → MvPolynomial D.vars A)
        ((eval (Presentation.relationOfHasCoeffs.{u, u_2, 0, 0, u} (R := A) (S := B) (P := D.P) ↥(subalgebra R D)) :
            (a : MvPolynomial D.rels (MvPolynomial D.vars ↥(subalgebra R D))) → MvPolynomial D.vars ↥(subalgebra R D))
          q) :
      MvPolynomial D.vars A)
    ((MvPolynomial.map (algebraMap (↥(subalgebra R D)) A) :
          (a : MvPolynomial D.vars ↥(subalgebra R D)) → MvPolynomial D.vars A)
        ((aeval p : (a : MvPolynomial D.vars ↥(subalgebra R D)) → MvPolynomial D.vars ↥(subalgebra R D))
          (Presentation.relationOfHasCoeffs.{u, u_2, 0, 0, u} (R := A) (S := B) (P := D.P) (↥(subalgebra R D)) i)) :
      MvPolynomial D.vars A)
⊢ ∃ (p_1 : MvPolynomial D.rels (MvPolynomial D.vars ↥(subalgebra R D))),
    p_1.IsHomogeneous 2 ∧
      Eq (α := MvPolynomial D.vars ↥(subalgebra R D))
        ((eval (Presentation.relationOfHasCoeffs.{u, u_2, 0, 0, u} (R := A) (S := B) (P := D.P) ↥(subalgebra R D)) :
              (a : MvPolynomial D.rels (MvPolynomial D.vars ↥(subalgebra R D))) → MvPolynomial D.vars ↥(subalgebra R D))
            p_1 :
          MvPolynomial D.vars ↥(subalgebra R D))
        ((aeval p : (a : MvPolynomial D.vars ↥(subalgebra R D)) → MvPolynomial D.vars ↥(subalgebra R D))
            (Presentation.relationOfHasCoeffs.{u, u_2, 0, 0, u} (R := A) (S := B) (P := D.P) (↥(subalgebra R D)) i) :
          MvPolynomial D.vars ↥(subalgebra R D))

Tactic:
refine ⟨q, .of_map hinj ?_, hinj ?_⟩
-- Module: Mathlib.RingTheory.Smooth.NoetherianDescent
Goal:
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 : DescentAux A B
p : (i : D.vars) → MvPolynomial D.vars ↥(subalgebra R D)
hp :
  ∀ (i : D.vars),
    (MvPolynomial.map (algebraMap (↥(subalgebra R D)) A) :
          (a : MvPolynomial D.vars ↥(subalgebra R D)) → MvPolynomial D.vars A)
        (p i) =
      D.h i
i : D.rels
hinj :
  Function.Injective (α := MvPolynomial D.vars ↥(subalgebra R D)) (β := MvPolynomial D.vars A)
    (⇑(MvPolynomial.map (algebraMap (↥(subalgebra R D)) A)) :
      (a : MvPolynomial D.vars ↥(subalgebra R D)) → MvPolynomial D.vars A)
q : MvPolynomial D.rels (MvPolynomial D.vars ↥(subalgebra R D))
hq :
  (MvPolynomial.map (MvPolynomial.map (algebraMap (↥(subalgebra R D)) A)) :
        (a : MvPolynomial D.rels (MvPolynomial D.vars ↥(subalgebra R D))) → MvPolynomial D.rels (MvPolynomial D.vars A))
      q =
    D.p i
refine_1 : (D.p i).IsHomogeneous 2
⊢ IsHomogeneous.{0, u} (σ := D.rels) (R := MvPolynomial D.vars A)
    ((MvPolynomial.map (MvPolynomial.map (algebraMap (↥(subalgebra R D)) A)) :
        (a : MvPolynomial D.rels (MvPolynomial D.vars ↥(subalgebra R D))) → MvPolynomial D.rels (MvPolynomial D.vars A))
      q)
    2

Tactic:
rw [hq]
-- Module: Mathlib.RingTheory.Smooth.NoetherianDescent
Goal:
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 : DescentAux A B
p : (i : D.vars) → MvPolynomial D.vars ↥(subalgebra R D)
hp :
  ∀ (i : D.vars),
    (MvPolynomial.map (algebraMap (↥(subalgebra R D)) A) :
          (a : MvPolynomial D.vars ↥(subalgebra R D)) → MvPolynomial D.vars A)
        (p i) =
      D.h i
i : D.rels
hinj :
  Function.Injective (α := MvPolynomial D.vars ↥(subalgebra R D)) (β := MvPolynomial D.vars A)
    (⇑(MvPolynomial.map (algebraMap (↥(subalgebra R D)) A)) :
      (a : MvPolynomial D.vars ↥(subalgebra R D)) → MvPolynomial D.vars A)
q : MvPolynomial D.rels (MvPolynomial D.vars ↥(subalgebra R D))
hq :
  (MvPolynomial.map (MvPolynomial.map (algebraMap (↥(subalgebra R D)) A)) :
        (a : MvPolynomial D.rels (MvPolynomial D.vars ↥(subalgebra R D))) → MvPolynomial D.rels (MvPolynomial D.vars A))
      q =
    D.p i
⊢ (D.p i).IsHomogeneous 2

Tactic:
D.hphom i

Premises used: _private.0.Algebra.Smooth.DescentAux.hphom
-- Module: Mathlib.RingTheory.Smooth.NoetherianDescent
Goal:
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 : DescentAux A B
p : (i : D.vars) → MvPolynomial D.vars ↥(subalgebra R D)
hp :
  ∀ (i : D.vars),
    (MvPolynomial.map (algebraMap (↥(subalgebra R D)) A) :
          (a : MvPolynomial D.vars ↥(subalgebra R D)) → MvPolynomial D.vars A)
        (p i) =
      D.h i
i : D.rels
hinj :
  Function.Injective (α := MvPolynomial D.vars ↥(subalgebra R D)) (β := MvPolynomial D.vars A)
    (⇑(MvPolynomial.map (algebraMap (↥(subalgebra R D)) A)) :
      (a : MvPolynomial D.vars ↥(subalgebra R D)) → MvPolynomial D.vars A)
q : MvPolynomial D.rels (MvPolynomial D.vars ↥(subalgebra R D))
hq :
  (MvPolynomial.map (MvPolynomial.map (algebraMap (↥(subalgebra R D)) A)) :
        (a : MvPolynomial D.rels (MvPolynomial D.vars ↥(subalgebra R D))) → MvPolynomial D.rels (MvPolynomial D.vars A))
      q =
    D.p i
⊢ (D.p i).IsHomogeneous 2

Tactic:
exact D.hphom i

Premises used: _private.0.Algebra.Smooth.DescentAux.hphom