Module: Mathlib.RingTheory.Smooth.NoetherianDescent

Goal state before:
pp: case refine_1
R : Type u_1
inst✝⁴ : CommRing R
A : Type u
B : Type u_2
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : CommRing B
inst✝ : Algebra A B
D : DescentAux A B
p : D.vars → MvPolynomial D.vars ↥(subalgebra R D)
hp : ∀ (i : D.vars), (MvPolynomial.map (algebraMap (↥(subalgebra R D)) A)) (p i) = D.h i
⊢ Presentation.ModelOfHasCoeffs ↥(subalgebra R D) →ₐ[↥(subalgebra R D)]
    MvPolynomial D.vars ↥(subalgebra R D) ⧸
      RingHom.ker
          (Ideal.Quotient.mkₐ (↥(subalgebra R D))
            (Ideal.span (Set.range (Presentation.relationOfHasCoeffs ↥(subalgebra R D))))) ^
        2

pp: case refine_2
R : Type u_1
inst✝⁴ : CommRing R
A : Type u
B : Type u_2
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : CommRing B
inst✝ : Algebra A B
D : DescentAux A B
p : D.vars → MvPolynomial D.vars ↥(subalgebra R D)
hp : ∀ (i : D.vars), (MvPolynomial.map (algebraMap (↥(subalgebra R D)) A)) (p i) = D.h i
⊢ (Ideal.Quotient.mkₐ (↥(subalgebra R D))
            (Ideal.span (Set.range (Presentation.relationOfHasCoeffs ↥(subalgebra R D))))).kerSquareLift.comp
      ?refine_1 =
    AlgHom.id (↥(subalgebra R D)) (Presentation.ModelOfHasCoeffs ↥(subalgebra R D))

Tactic:
· refine Ideal.Quotient.liftₐ _ ((Ideal.Quotient.mkₐ _ _).comp <| aeval p) ?_
    simp_rw [← RingHom.mem_ker, ← SetLike.le_def, Ideal.span_le, Set.range_subset_iff]
    intro i
    simp only [← AlgHom.comap_ker, Ideal.coe_comap, Set.mem_preimage, SetLike.mem_coe]
    rw [← RingHom.ker_coe_toRingHom, Ideal.Quotient.mkₐ_ker,
      ← RingHom.ker_coe_toRingHom, Ideal.Quotient.mkₐ_ker]
    have hinj : Function.Injective
        (MvPolynomial.map (σ := D.vars) (algebraMap (D.subalgebra R) A)) :=
      map_injective _ (FaithfulSMul.algebraMap_injective (D.subalgebra R) A)
    rw [Ideal.mem_span_pow_iff_exists_isHomogeneous]
    obtain ⟨q, hq⟩ := (D.p i).mem_range_map_iff_coeffs_subset.mpr (D.coeffs_p_subset R i)
    refine ⟨q, .of_map hinj ?_, hinj ?_⟩
    · rw [hq]
      exact D.hphom i
    · simp_rw [map_eval, Function.comp_def, Presentation.map_relationOfHasCoeffs,
        hq, D.hp, MvPolynomial.map_aeval, hp]
      simp [MvPolynomial.eval₂_map_comp_C, Presentation.map_relationOfHasCoeffs, aeval_def]

Goal state after:
case refine_2
R : Type u_1
inst✝⁴ : CommRing R
A : Type u
B : Type u_2
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : CommRing B
inst✝ : Algebra A B
D : DescentAux A B
p : D.vars → MvPolynomial D.vars ↥(subalgebra R D)
hp : ∀ (i : D.vars), (MvPolynomial.map (algebraMap (↥(subalgebra R D)) A)) (p i) = D.h i
⊢ (Ideal.Quotient.mkₐ (↥(subalgebra R D))
            (Ideal.span (Set.range (Presentation.relationOfHasCoeffs ↥(subalgebra R D))))).kerSquareLift.comp
      (Ideal.Quotient.liftₐ (Ideal.span (Set.range (Presentation.relationOfHasCoeffs ↥(subalgebra R D))))
        ((Ideal.Quotient.mkₐ (↥(subalgebra R D))
              (RingHom.ker
                  (Ideal.Quotient.mkₐ (↥(subalgebra R D))
                    (Ideal.span (Set.range (Presentation.relationOfHasCoeffs ↥(subalgebra R D))))) ^
                2)).comp
          (aeval p))
        ⋯) =
    AlgHom.id (↥(subalgebra R D)) (Presentation.ModelOfHasCoeffs ↥(subalgebra R D))