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'))
this : IsScalarTower P.Ring P'.Ring S'
J : Ideal P.Ring := RingHom.ker (algebraMap P.Ring S)
J' : Ideal P'.Ring := RingHom.ker (algebraMap P'.Ring S')
I : Ideal R := RingHom.ker (algebraMap R R')
IS : Ideal S := Ideal.map (algebraMap R S) I
kerS : RingHom.ker (algebraMap S S') = IS
IP : Ideal P.Ring := Ideal.map (algebraMap R P.Ring) I
kerP : RingHom.ker (algebraMap P.Ring P'.Ring) = IP
surjPP' : Function.Surjective ⇑(algebraMap P.Ring P'.Ring)
ISeq : IS = Ideal.map (algebraMap P.Ring S) IP
surjP : Function.Surjective ⇑(algebraMap P.Ring S)
surjP' : Function.Surjective ⇑(algebraMap P'.Ring S')
σ : TensorProduct P'.Ring S' Ω[P'.Ring⁄R'] →ₗ[P'.Ring] (RingHom.ker (algebraMap P'.Ring S')).Cotangent
hσ : σ ∘ₗ KaehlerDifferential.kerCotangentToTensor R' P'.Ring S' = LinearMap.id
⊢ ∃ l, l ∘ₗ KaehlerDifferential.kerCotangentToTensor R P.Ring S = LinearMap.id

Tactic:
have infeq : IP ⊓ J = IP * J := by
    refine le_antisymm (fun x hx ↦ ?_) Ideal.mul_le_inf
    have : x ∈ I • (J.restrictScalars R) := by
      change x ∈ I • (IsScalarTower.toAlgHom R P.Ring S).toLinearMap.ker
      rw [← LinearMap.ker_inf_smul_top_eq_smul_of_flat I _ surjP]
      simpa using! ⟨hx.2, hx.1⟩
    simpa [← Ideal.smul_restrictScalars I J, Submodule.restrictScalars_mem] using! this

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'
J : Ideal P.Ring := RingHom.ker (algebraMap P.Ring S)
J' : Ideal P'.Ring := RingHom.ker (algebraMap P'.Ring S')
I : Ideal R := RingHom.ker (algebraMap R R')
IS : Ideal S := Ideal.map (algebraMap R S) I
kerS : RingHom.ker (algebraMap S S') = IS
IP : Ideal P.Ring := Ideal.map (algebraMap R P.Ring) I
kerP : RingHom.ker (algebraMap P.Ring P'.Ring) = IP
surjPP' : Function.Surjective ⇑(algebraMap P.Ring P'.Ring)
ISeq : IS = Ideal.map (algebraMap P.Ring S) IP
surjP : Function.Surjective ⇑(algebraMap P.Ring S)
surjP' : Function.Surjective ⇑(algebraMap P'.Ring S')
σ : TensorProduct P'.Ring S' Ω[P'.Ring⁄R'] →ₗ[P'.Ring] (RingHom.ker (algebraMap P'.Ring S')).Cotangent
hσ : σ ∘ₗ KaehlerDifferential.kerCotangentToTensor R' P'.Ring S' = LinearMap.id
infeq : IP ⊓ J = IP * J
⊢ ∃ l, l ∘ₗ KaehlerDifferential.kerCotangentToTensor R P.Ring S = LinearMap.id