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
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 :
  Eq (α := MvPolynomial D.vars A)
    ((aeval D.h : (a : MvPolynomial D.vars A) → MvPolynomial D.vars A) (D.P.relation i) : MvPolynomial D.vars A)
    ((eval₂Hom
            (RingHom.comp (β := MvPolynomial D.vars ↥(subalgebra R D))
              (MvPolynomial.map (algebraMap (↥(subalgebra R D)) A))
              (algebraMap (↥(subalgebra R D)) (MvPolynomial D.vars ↥(subalgebra R D))))
            fun (i : D.vars) ↦ D.h i :
          (a : MvPolynomial D.vars ↥(subalgebra R D)) → MvPolynomial D.vars A)
        (Presentation.relationOfHasCoeffs.{u, u_2, 0, 0, u} (R := A) (S := B) (P := D.P) (↥(subalgebra R D)) i) :
      MvPolynomial D.vars A)
⊢ 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)

Tactic:
simp_rw [map_eval, Function.comp_def, Presentation.map_relationOfHasCoeffs,
        hq, D.hp, MvPolynomial.map_aeval, hp]

Premises used: MvPolynomial.map_aeval, Algebra.Presentation.map_relationOfHasCoeffs, Function.comp_def, _private.0.Algebra.Smooth.DescentAux.hp, MvPolynomial.map_eval
-- 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
⊢ Eq (α := MvPolynomial D.vars A)
    ((aeval D.h : (a : MvPolynomial D.vars A) → MvPolynomial D.vars A) (D.P.relation i) : MvPolynomial D.vars A)
    ((eval₂Hom
            (RingHom.comp (β := MvPolynomial D.vars ↥(subalgebra R D))
              (MvPolynomial.map (algebraMap (↥(subalgebra R D)) A))
              (algebraMap (↥(subalgebra R D)) (MvPolynomial D.vars ↥(subalgebra R D))))
            fun (i : D.vars) ↦ D.h i :
          (a : MvPolynomial D.vars ↥(subalgebra R D)) → MvPolynomial D.vars A)
        (Presentation.relationOfHasCoeffs.{u, u_2, 0, 0, u} (R := A) (S := B) (P := D.P) (↥(subalgebra R D)) i) :
      MvPolynomial D.vars A)

Tactic:
simp [MvPolynomial.eval₂_map_comp_C, Presentation.map_relationOfHasCoeffs, aeval_def]

Premises used: Algebra.Presentation.map_relationOfHasCoeffs, MvPolynomial.aeval_def, MvPolynomial.eval₂_map_comp_C
-- 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
⊢ Function.Surjective.{u + 1, u + 1} (α := MvPolynomial D.vars ↥(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))))) :
      (a : MvPolynomial D.vars ↥(subalgebra R D)) →
        MvPolynomial D.vars ↥(subalgebra R D) ⧸
          Ideal.span (Set.range (Presentation.relationOfHasCoeffs ↥(subalgebra R D))))

Tactic:
have hf₀ : Function.Surjective f₀ := Ideal.Quotient.mk_surjective
-- 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
hf₀ :
  Function.Surjective.{u + 1, u + 1} (α := MvPolynomial D.vars ↥(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))))) :
      (a : MvPolynomial D.vars ↥(subalgebra R D)) →
        MvPolynomial D.vars ↥(subalgebra R D) ⧸
          Ideal.span (Set.range (Presentation.relationOfHasCoeffs ↥(subalgebra R D))))
i : D.vars
h :
  ∃ (p' : MvPolynomial D.rels (MvPolynomial D.vars ↥(subalgebra R D))),
    p'.IsHomogeneous 1 ∧
      (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' =
        p i - X i
⊢ Membership.mem (γ := 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))))
    (HSub.hSub (α := MvPolynomial D.vars ↥(subalgebra R D)) (β := MvPolynomial D.vars ↥(subalgebra R D))
      (((↑(aeval p) : MvPolynomial D.vars ↥(subalgebra R D) →+* MvPolynomial D.vars ↥(subalgebra R D)) :
            (a : MvPolynomial D.vars ↥(subalgebra R D)) → MvPolynomial D.vars ↥(subalgebra R D))
          (X i) :
        MvPolynomial D.vars ↥(subalgebra R D))
      (X i))

Tactic:
simpa [Ideal.mem_span_iff_exists_isHomogeneous, hp]

Premises used: Ideal.mem_span_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
hf₀ :
  Function.Surjective.{u + 1, u + 1} (α := MvPolynomial D.vars ↥(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))))) :
      (a : MvPolynomial D.vars ↥(subalgebra R D)) →
        MvPolynomial D.vars ↥(subalgebra R D) ⧸
          Ideal.span (Set.range (Presentation.relationOfHasCoeffs ↥(subalgebra R D))))
i : D.vars
⊢ 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
hf₀ :
  Function.Surjective.{u + 1, u + 1} (α := MvPolynomial D.vars ↥(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))))) :
      (a : MvPolynomial D.vars ↥(subalgebra R D)) →
        MvPolynomial D.vars ↥(subalgebra R D) ⧸
          Ideal.span (Set.range (Presentation.relationOfHasCoeffs ↥(subalgebra R D))))
i : D.vars
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_2 :
  ∀ (t : MvPolynomial D.rels (MvPolynomial D.vars ↥(subalgebra R D)))
    (ht :
      (MvPolynomial.map (MvPolynomial.map (algebraMap (↥(subalgebra R D)) A)) :
            (a : MvPolynomial D.rels (MvPolynomial D.vars ↥(subalgebra R D))) → MvPolynomial D.rels D.P.Ring)
          t =
        D.q i),
    ∃ (p' : MvPolynomial D.rels (MvPolynomial D.vars ↥(subalgebra R D))),
      p'.IsHomogeneous 1 ∧
        (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' =
          p i - X i
⊢ ∃ (p' : MvPolynomial D.rels (MvPolynomial D.vars ↥(subalgebra R D))),
    p'.IsHomogeneous 1 ∧
      (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' =
        p i - X i

Tactic:
obtain ⟨t, ht⟩ := (D.q i).mem_range_map_iff_coeffs_subset.mpr (D.coeffs_q_subset R i)

Premises used: Iff.mpr, MvPolynomial.mem_range_map_iff_coeffs_subset, _private.0.Algebra.Smooth.DescentAux.coeffs_q_subset
-- 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
hf₀ :
  Function.Surjective.{u + 1, u + 1} (α := MvPolynomial D.vars ↥(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))))) :
      (a : MvPolynomial D.vars ↥(subalgebra R D)) →
        MvPolynomial D.vars ↥(subalgebra R D) ⧸
          Ideal.span (Set.range (Presentation.relationOfHasCoeffs ↥(subalgebra R D))))
i : D.vars
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)
t : MvPolynomial D.rels (MvPolynomial D.vars ↥(subalgebra R D))
ht :
  (MvPolynomial.map (MvPolynomial.map (algebraMap (↥(subalgebra R D)) A)) :
        (a : MvPolynomial D.rels (MvPolynomial D.vars ↥(subalgebra R D))) → MvPolynomial D.rels D.P.Ring)
      t =
    D.q i
⊢ ∃ (p' : MvPolynomial D.rels (MvPolynomial D.vars ↥(subalgebra R D))),
    p'.IsHomogeneous 1 ∧
      (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' =
        p i - X i

Tactic:
⟨t, .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
hf₀ :
  Function.Surjective.{u + 1, u + 1} (α := MvPolynomial D.vars ↥(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))))) :
      (a : MvPolynomial D.vars ↥(subalgebra R D)) →
        MvPolynomial D.vars ↥(subalgebra R D) ⧸
          Ideal.span (Set.range (Presentation.relationOfHasCoeffs ↥(subalgebra R D))))
i : D.vars
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)
t : MvPolynomial D.rels (MvPolynomial D.vars ↥(subalgebra R D))
ht :
  (MvPolynomial.map (MvPolynomial.map (algebraMap (↥(subalgebra R D)) A)) :
        (a : MvPolynomial D.rels (MvPolynomial D.vars ↥(subalgebra R D))) → MvPolynomial D.rels D.P.Ring)
      t =
    D.q i
refine_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))
      t)
    1
refine_2₁ :
  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))
          t) :
      MvPolynomial D.vars A)
    ((MvPolynomial.map (algebraMap (↥(subalgebra R D)) A) :
          (a : MvPolynomial D.vars ↥(subalgebra R D)) → MvPolynomial D.vars A)
        (p i - X i) :
      MvPolynomial D.vars A)
⊢ ∃ (p' : MvPolynomial D.rels (MvPolynomial D.vars ↥(subalgebra R D))),
    p'.IsHomogeneous 1 ∧
      (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' =
        p i - X i

Tactic:
refine ⟨t, .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
hf₀ :
  Function.Surjective.{u + 1, u + 1} (α := MvPolynomial D.vars ↥(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))))) :
      (a : MvPolynomial D.vars ↥(subalgebra R D)) →
        MvPolynomial D.vars ↥(subalgebra R D) ⧸
          Ideal.span (Set.range (Presentation.relationOfHasCoeffs ↥(subalgebra R D))))
i : D.vars
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)
t : MvPolynomial D.rels (MvPolynomial D.vars ↥(subalgebra R D))
ht :
  (MvPolynomial.map (MvPolynomial.map (algebraMap (↥(subalgebra R D)) A)) :
        (a : MvPolynomial D.rels (MvPolynomial D.vars ↥(subalgebra R D))) → MvPolynomial D.rels D.P.Ring)
      t =
    D.q i
refine_2 : (D.q i).IsHomogeneous 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))
      t)
    1

Tactic:
rw [ht]
-- 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
hf₀ :
  Function.Surjective.{u + 1, u + 1} (α := MvPolynomial D.vars ↥(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))))) :
      (a : MvPolynomial D.vars ↥(subalgebra R D)) →
        MvPolynomial D.vars ↥(subalgebra R D) ⧸
          Ideal.span (Set.range (Presentation.relationOfHasCoeffs ↥(subalgebra R D))))
i : D.vars
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)
t : MvPolynomial D.rels (MvPolynomial D.vars ↥(subalgebra R D))
ht :
  (MvPolynomial.map (MvPolynomial.map (algebraMap (↥(subalgebra R D)) A)) :
        (a : MvPolynomial D.rels (MvPolynomial D.vars ↥(subalgebra R D))) → MvPolynomial D.rels D.P.Ring)
      t =
    D.q i
⊢ (D.q i).IsHomogeneous 1

Tactic:
D.hqhom i

Premises used: _private.0.Algebra.Smooth.DescentAux.hqhom
-- 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
hf₀ :
  Function.Surjective.{u + 1, u + 1} (α := MvPolynomial D.vars ↥(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))))) :
      (a : MvPolynomial D.vars ↥(subalgebra R D)) →
        MvPolynomial D.vars ↥(subalgebra R D) ⧸
          Ideal.span (Set.range (Presentation.relationOfHasCoeffs ↥(subalgebra R D))))
i : D.vars
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)
t : MvPolynomial D.rels (MvPolynomial D.vars ↥(subalgebra R D))
ht :
  (MvPolynomial.map (MvPolynomial.map (algebraMap (↥(subalgebra R D)) A)) :
        (a : MvPolynomial D.rels (MvPolynomial D.vars ↥(subalgebra R D))) → MvPolynomial D.rels D.P.Ring)
      t =
    D.q i
⊢ (D.q i).IsHomogeneous 1

Tactic:
exact D.hqhom i

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