Module: Mathlib.RingTheory.Smooth.Quotient

Goal state before:
pp: R : Type u_1
inst✝¹¹ : CommRing R
S : Type u_2
inst✝¹⁰ : CommRing S
R' : Type u_3
S' : Type u_4
inst✝⁹ : CommRing R'
inst✝⁸ : CommRing S'
inst✝⁷ : Algebra R S
inst✝⁶ : Algebra R R'
inst✝⁵ : Algebra R' S'
inst✝⁴ : Algebra S S'
inst✝³ : Algebra R S'
inst✝² : IsScalarTower R S S'
inst✝¹ : IsScalarTower R R' S'
inst✝ : Module.Flat R S
surj : Function.Surjective ⇑(algebraMap R R')
surjS : Function.Surjective ⇑(algebraMap S S')
eqmap : RingHom.ker (algebraMap S S') = Ideal.map (algebraMap R S) (RingHom.ker (algebraMap R R'))
sq0 : RingHom.ker (algebraMap R R') ^ 2 = ⊥
smoothq : FormallySmooth R' S'
P : Extension R S := (Generators.self R S).toExtension
this✝² : FormallySmooth R P.Ring := instFormallySmoothMvPolynomial S
IP : Ideal P.Ring := Ideal.map (algebraMap R P.Ring) (RingHom.ker (algebraMap R R'))
Gen : Generators R' S' S :=
  { val := ⇑(algebraMap S S'), σ' := fun s' ↦ MvPolynomial.X (Classical.choose ⋯), aeval_val_σ' := ⋯,
    algebraMap_eq := ⋯ }
P' : Extension R' S' := Gen.toExtension
this✝¹ : FormallySmooth R' P'.Ring := instFormallySmoothMvPolynomial S
this✝ : Algebra P.Ring P'.Ring := MvPolynomial.algebraMvPolynomial
this : IsScalarTower R P.Ring P'.Ring :=
  IsScalarTower.of_algebraMap_eq fun x ↦ Eq.symm (MvPolynomial.map_C (algebraMap R R') x)
algInst✝ : Algebra P.Ring S' := ((algebraMap S S').comp (algebraMap P.Ring S)).toAlgebra
scalarTowerInst✝ : IsScalarTower P.Ring S S' := IsScalarTower.of_algebraMap_eq' (Eq.refl (algebraMap P.Ring S'))
⊢ FormallySmooth R S

Tactic:
have : IsScalarTower P.Ring P'.Ring S' := by
    refine IsScalarTower.of_algebraMap_eq (fun x ↦ ?_)
    change (algebraMap S S') (MvPolynomial.aeval _root_.id x) =
      MvPolynomial.aeval Gen.val (MvPolynomial.map (algebraMap R R') x)
    rw [← MvPolynomial.aeval_algebraMap_apply]
    simp [MvPolynomial.aeval_map_algebraMap, Gen]

Goal state after:
R : Type u_1
inst✝¹¹ : CommRing R
S : Type u_2
inst✝¹⁰ : CommRing S
R' : Type u_3
S' : Type u_4
inst✝⁹ : CommRing R'
inst✝⁸ : CommRing S'
inst✝⁷ : Algebra R S
inst✝⁶ : Algebra R R'
inst✝⁵ : Algebra R' S'
inst✝⁴ : Algebra S S'
inst✝³ : Algebra R S'
inst✝² : IsScalarTower R S S'
inst✝¹ : IsScalarTower R R' S'
inst✝ : Module.Flat R S
surj : Function.Surjective ⇑(algebraMap R R')
surjS : Function.Surjective ⇑(algebraMap S S')
eqmap : RingHom.ker (algebraMap S S') = Ideal.map (algebraMap R S) (RingHom.ker (algebraMap R R'))
sq0 : RingHom.ker (algebraMap R R') ^ 2 = ⊥
smoothq : FormallySmooth R' S'
P : Extension R S := (Generators.self R S).toExtension
this✝³ : FormallySmooth R P.Ring := instFormallySmoothMvPolynomial S
IP : Ideal P.Ring := Ideal.map (algebraMap R P.Ring) (RingHom.ker (algebraMap R R'))
Gen : Generators R' S' S :=
  { val := ⇑(algebraMap S S'), σ' := fun s' ↦ MvPolynomial.X (Classical.choose ⋯), aeval_val_σ' := ⋯,
    algebraMap_eq := ⋯ }
P' : Extension R' S' := Gen.toExtension
this✝² : FormallySmooth R' P'.Ring := instFormallySmoothMvPolynomial S
this✝¹ : Algebra P.Ring P'.Ring := MvPolynomial.algebraMvPolynomial
this✝ : IsScalarTower R P.Ring P'.Ring :=
  IsScalarTower.of_algebraMap_eq fun x ↦ Eq.symm (MvPolynomial.map_C (algebraMap R R') x)
algInst✝ : Algebra P.Ring S' := ((algebraMap S S').comp (algebraMap P.Ring S)).toAlgebra
scalarTowerInst✝ : IsScalarTower P.Ring S S' := IsScalarTower.of_algebraMap_eq' (Eq.refl (algebraMap P.Ring S'))
this : IsScalarTower P.Ring P'.Ring S'
⊢ FormallySmooth R S