Module: Mathlib.RingTheory.Smooth.Kaehler

Goal state before:
pp: R : Type u_1
P : Type u_2
S : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing P
inst✝⁴ : CommRing S
inst✝³ : Algebra R P
inst✝² : Algebra P S
inst✝¹ : Algebra R S
inst✝ : IsScalarTower R P S
hf' : RingHom.ker (algebraMap P S) ^ 2 = ⊥
hf : Surjective ⇑(algebraMap P S)
f₁ : Ω[P ⧸ RingHom.ker (algebraMap P S) ^ 2⁄R] →ₗ[P ⧸ RingHom.ker (algebraMap P S) ^ 2] S ⊗[P] Ω[P⁄R] :=
  (derivationQuotKerSq R P S).liftKaehlerDifferential
f₂ : S ⊗[P ⧸ RingHom.ker (algebraMap P S) ^ 2] Ω[P ⧸ RingHom.ker (algebraMap P S) ^ 2⁄R] →ₗ[S] S ⊗[P] Ω[P⁄R] :=
  AlgebraTensorModule.lift
    ((LinearMap.ringLmapEquivSelf S S
          (Ω[P ⧸ RingHom.ker (algebraMap P S) ^ 2⁄R] →ₗ[P ⧸ RingHom.ker (algebraMap P S) ^ 2] S ⊗[P] Ω[P⁄R])).symm
      f₁)
f₃ : Ω[P⁄R] →ₗ[P] Ω[P ⧸ RingHom.ker (algebraMap P S) ^ 2⁄R] :=
  KaehlerDifferential.map R R P (P ⧸ RingHom.ker (algebraMap P S) ^ 2)
f₄ : Ω[P⁄R] →ₗ[P] S ⊗[P ⧸ RingHom.ker (algebraMap P S) ^ 2] Ω[P ⧸ RingHom.ker (algebraMap P S) ^ 2⁄R] :=
  ↑P ((mk (P ⧸ RingHom.ker (algebraMap P S) ^ 2) S Ω[P ⧸ RingHom.ker (algebraMap P S) ^ 2⁄R]) 1) ∘ₗ f₃
f₅ : S ⊗[P] Ω[P⁄R] →ₗ[S] S ⊗[P ⧸ RingHom.ker (algebraMap P S) ^ 2] Ω[P ⧸ RingHom.ker (algebraMap P S) ^ 2⁄R] :=
  AlgebraTensorModule.lift
    ((LinearMap.ringLmapEquivSelf S S
          (Ω[P⁄R] →ₗ[P] S ⊗[P ⧸ RingHom.ker (algebraMap P S) ^ 2] Ω[P ⧸ RingHom.ker (algebraMap P S) ^ 2⁄R])).symm
      f₄)
a : P ⧸ RingHom.ker (algebraMap P S) ^ 2
⊢ (((AlgebraTensorModule.curry (f₅ ∘ₗ f₂)) 1).compDer (D R (P ⧸ RingHom.ker (algebraMap P S) ^ 2))) a =
    (((AlgebraTensorModule.curry LinearMap.id) 1).compDer (D R (P ⧸ RingHom.ker (algebraMap P S) ^ 2))) a

Tactic:
obtain ⟨a, rfl⟩ := Ideal.Quotient.mk_surjective a

Goal state after:
R : Type u_1
P : Type u_2
S : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing P
inst✝⁴ : CommRing S
inst✝³ : Algebra R P
inst✝² : Algebra P S
inst✝¹ : Algebra R S
inst✝ : IsScalarTower R P S
hf' : RingHom.ker (algebraMap P S) ^ 2 = ⊥
hf : Surjective ⇑(algebraMap P S)
f₁ : Ω[P ⧸ RingHom.ker (algebraMap P S) ^ 2⁄R] →ₗ[P ⧸ RingHom.ker (algebraMap P S) ^ 2] S ⊗[P] Ω[P⁄R] :=
  (derivationQuotKerSq R P S).liftKaehlerDifferential
f₂ : S ⊗[P ⧸ RingHom.ker (algebraMap P S) ^ 2] Ω[P ⧸ RingHom.ker (algebraMap P S) ^ 2⁄R] →ₗ[S] S ⊗[P] Ω[P⁄R] :=
  AlgebraTensorModule.lift
    ((LinearMap.ringLmapEquivSelf S S
          (Ω[P ⧸ RingHom.ker (algebraMap P S) ^ 2⁄R] →ₗ[P ⧸ RingHom.ker (algebraMap P S) ^ 2] S ⊗[P] Ω[P⁄R])).symm
      f₁)
f₃ : Ω[P⁄R] →ₗ[P] Ω[P ⧸ RingHom.ker (algebraMap P S) ^ 2⁄R] :=
  KaehlerDifferential.map R R P (P ⧸ RingHom.ker (algebraMap P S) ^ 2)
f₄ : Ω[P⁄R] →ₗ[P] S ⊗[P ⧸ RingHom.ker (algebraMap P S) ^ 2] Ω[P ⧸ RingHom.ker (algebraMap P S) ^ 2⁄R] :=
  ↑P ((mk (P ⧸ RingHom.ker (algebraMap P S) ^ 2) S Ω[P ⧸ RingHom.ker (algebraMap P S) ^ 2⁄R]) 1) ∘ₗ f₃
f₅ : S ⊗[P] Ω[P⁄R] →ₗ[S] S ⊗[P ⧸ RingHom.ker (algebraMap P S) ^ 2] Ω[P ⧸ RingHom.ker (algebraMap P S) ^ 2⁄R] :=
  AlgebraTensorModule.lift
    ((LinearMap.ringLmapEquivSelf S S
          (Ω[P⁄R] →ₗ[P] S ⊗[P ⧸ RingHom.ker (algebraMap P S) ^ 2] Ω[P ⧸ RingHom.ker (algebraMap P S) ^ 2⁄R])).symm
      f₄)
a : P
⊢ (((AlgebraTensorModule.curry (f₅ ∘ₗ f₂)) 1).compDer (D R (P ⧸ RingHom.ker (algebraMap P S) ^ 2)))
      ((Ideal.Quotient.mk (RingHom.ker (algebraMap P S) ^ 2)) a) =
    (((AlgebraTensorModule.curry LinearMap.id) 1).compDer (D R (P ⧸ RingHom.ker (algebraMap P S) ^ 2)))
      ((Ideal.Quotient.mk (RingHom.ker (algebraMap P S) ^ 2)) a)