Module: Mathlib.RingTheory.Smooth.Fiber

Goal state before:
pp: case tmul
R : Type u_1
S : Type u_2
P : Type u_3
inst✝¹⁴ : CommRing R
inst✝¹³ : CommRing S
inst✝¹² : Algebra R S
inst✝¹¹ : Module.Flat R S
inst✝¹⁰ : CommRing P
inst✝⁹ : Algebra R P
inst✝⁸ : Algebra P S
inst✝⁷ : IsScalarTower R P S
inst✝⁶ : IsLocalRing R
inst✝⁵ : IsLocalRing S
inst✝⁴ : IsLocalHom (algebraMap R S)
inst✝³ : FormallySmooth 𝓀[R] (𝓀[R] ⊗[R] S)
inst✝² : FormallySmooth R P
inst✝¹ : Module.Free P Ω[P⁄R]
inst✝ : Module.Finite P Ω[P⁄R]
h₁ : Function.Surjective ⇑(algebraMap P S)
h₂ : (RingHom.ker (algebraMap P S)).FG
Sp : Type (max u_1 u_2) := 𝓀[R] ⊗[R] S
Pp : Type (max u_1 u_3) := 𝓀[R] ⊗[R] P
φ : Pp →ₐ[𝓀[R]] Sp := TensorProduct.map (AlgHom.id 𝓀[R] 𝓀[R]) (IsScalarTower.toAlgHom R P S)
ψ : Sp →ₐ[R] 𝓀[S] := TensorProduct.lift (IsScalarTower.toAlgHom R 𝓀[R] 𝓀[S]) (IsScalarTower.toAlgHom R S 𝓀[S]) ⋯
algInst✝³ : Algebra Pp Sp := φ.toAlgebra
algInst✝² : Algebra P Sp := (φ.comp (algebraMap P Pp)).toAlgebra
algInst✝¹ : Algebra Sp 𝓀[S] := ψ.toAlgebra
algInst✝ : Algebra Pp 𝓀[S] := (ψ.comp φ.toRingHom).toAlgebra
scalarTowerInst✝¹ : IsScalarTower P Pp Sp := IsScalarTower.of_algebraMap_eq' (Eq.refl (algebraMap P Sp))
scalarTowerInst✝ : IsScalarTower Pp Sp 𝓀[S] := IsScalarTower.of_algebraMap_eq' (Eq.refl (algebraMap Pp 𝓀[S]))
this✝⁷ : IsScalarTower 𝓀[R] Pp Sp
this✝⁶ : IsScalarTower R Sp 𝓀[S]
this✝⁵ : IsScalarTower P S Sp
this✝⁴ : IsScalarTower S Sp 𝓀[S]
this✝³ : IsScalarTower P Sp 𝓀[S]
this✝² : IsScalarTower P Pp 𝓀[S]
ePp : Pp ≃ₐ[P] P ⊗[R] 𝓀[R] :=
  let __spread.0 := TensorProduct.comm R 𝓀[R] P;
  { toEquiv := __spread.0.toEquiv, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }
e₀ : Ω[Pp⁄𝓀[R]] ≃ₗ[Pp] Pp ⊗[P] Ω[P⁄R] := (KaehlerDifferential.tensorKaehlerEquiv R 𝓀[R] P Pp).symm
this✝¹ : Module.Free Pp Ω[Pp⁄𝓀[R]]
this✝ : Module.Finite Pp Ω[Pp⁄𝓀[R]]
e₁ : ↥(RingHom.ker φ) ≃ₗ[Pp] Pp ⊗[P] ↥(RingHom.ker (algebraMap P S)) := kerTensorProductMapIdToAlgHomEquiv R P S 𝓀[R] h₁
h₁' : Function.Surjective ⇑φ
h₂' : (RingHom.ker φ).FG
h₃ : 𝓂[Sp] ≤ RingHom.ker ψ
this : Function.Injective ⇑(KaehlerDifferential.cotangentComplexBaseChange 𝓀[R] Sp Pp 𝓀[S])
eᵣ : 𝓀[S] ⊗[Pp] Ω[Pp⁄𝓀[R]] ≃ₗ[S] 𝓀[S] ⊗[P] Ω[P⁄R] :=
  LinearEquiv.restrictScalars S (AlgebraTensorModule.congr (LinearEquiv.refl 𝓀[S] 𝓀[S]) e₀) ≪≫ₗ
    LinearEquiv.restrictScalars S (AlgebraTensorModule.cancelBaseChange P Pp Sp 𝓀[S] Ω[P⁄R])
eₗ : 𝓀[S] ⊗[Pp] ↥(RingHom.ker φ) ≃ₗ[S] 𝓀[S] ⊗[P] ↥(RingHom.ker (algebraMap P S)) :=
  LinearEquiv.restrictScalars S (AlgebraTensorModule.congr (LinearEquiv.refl 𝓀[S] 𝓀[S]) e₁) ≪≫ₗ
    LinearEquiv.restrictScalars S (AlgebraTensorModule.cancelBaseChange P Pp Sp 𝓀[S] ↥(RingHom.ker (algebraMap P S)))
x : 𝓀[S]
y : ↥(RingHom.ker (algebraMap P S))
⊢ (x * 1) ⊗ₜ[P] (KaehlerDifferential.D R P) ↑y =
    (AlgebraTensorModule.cancelBaseChange P (𝓀[R] ⊗[R] P) Sp 𝓀[S] Ω[P⁄R])
      ((x * 1) ⊗ₜ[𝓀[R] ⊗[R] P]
        e₀
          ((KaehlerDifferential.D 𝓀[R] (𝓀[R] ⊗[R] P))
            ↑((kerTensorProductMapIdToAlgHomEquiv R P S 𝓀[R] h₁).symm (1 ⊗ₜ[R] 1 ⊗ₜ[P] y))))

Tactic:
rw [kerTensorProductMapIdToAlgHomEquiv_symm_apply]

Goal state after:
case tmul
R : Type u_1
S : Type u_2
P : Type u_3
inst✝¹⁴ : CommRing R
inst✝¹³ : CommRing S
inst✝¹² : Algebra R S
inst✝¹¹ : Module.Flat R S
inst✝¹⁰ : CommRing P
inst✝⁹ : Algebra R P
inst✝⁸ : Algebra P S
inst✝⁷ : IsScalarTower R P S
inst✝⁶ : IsLocalRing R
inst✝⁵ : IsLocalRing S
inst✝⁴ : IsLocalHom (algebraMap R S)
inst✝³ : FormallySmooth 𝓀[R] (𝓀[R] ⊗[R] S)
inst✝² : FormallySmooth R P
inst✝¹ : Module.Free P Ω[P⁄R]
inst✝ : Module.Finite P Ω[P⁄R]
h₁ : Function.Surjective ⇑(algebraMap P S)
h₂ : (RingHom.ker (algebraMap P S)).FG
Sp : Type (max u_1 u_2) := 𝓀[R] ⊗[R] S
Pp : Type (max u_1 u_3) := 𝓀[R] ⊗[R] P
φ : Pp →ₐ[𝓀[R]] Sp := TensorProduct.map (AlgHom.id 𝓀[R] 𝓀[R]) (IsScalarTower.toAlgHom R P S)
ψ : Sp →ₐ[R] 𝓀[S] := TensorProduct.lift (IsScalarTower.toAlgHom R 𝓀[R] 𝓀[S]) (IsScalarTower.toAlgHom R S 𝓀[S]) ⋯
algInst✝³ : Algebra Pp Sp := φ.toAlgebra
algInst✝² : Algebra P Sp := (φ.comp (algebraMap P Pp)).toAlgebra
algInst✝¹ : Algebra Sp 𝓀[S] := ψ.toAlgebra
algInst✝ : Algebra Pp 𝓀[S] := (ψ.comp φ.toRingHom).toAlgebra
scalarTowerInst✝¹ : IsScalarTower P Pp Sp := IsScalarTower.of_algebraMap_eq' (Eq.refl (algebraMap P Sp))
scalarTowerInst✝ : IsScalarTower Pp Sp 𝓀[S] := IsScalarTower.of_algebraMap_eq' (Eq.refl (algebraMap Pp 𝓀[S]))
this✝⁷ : IsScalarTower 𝓀[R] Pp Sp
this✝⁶ : IsScalarTower R Sp 𝓀[S]
this✝⁵ : IsScalarTower P S Sp
this✝⁴ : IsScalarTower S Sp 𝓀[S]
this✝³ : IsScalarTower P Sp 𝓀[S]
this✝² : IsScalarTower P Pp 𝓀[S]
ePp : Pp ≃ₐ[P] P ⊗[R] 𝓀[R] :=
  let __spread.0 := TensorProduct.comm R 𝓀[R] P;
  { toEquiv := __spread.0.toEquiv, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }
e₀ : Ω[Pp⁄𝓀[R]] ≃ₗ[Pp] Pp ⊗[P] Ω[P⁄R] := (KaehlerDifferential.tensorKaehlerEquiv R 𝓀[R] P Pp).symm
this✝¹ : Module.Free Pp Ω[Pp⁄𝓀[R]]
this✝ : Module.Finite Pp Ω[Pp⁄𝓀[R]]
e₁ : ↥(RingHom.ker φ) ≃ₗ[Pp] Pp ⊗[P] ↥(RingHom.ker (algebraMap P S)) := kerTensorProductMapIdToAlgHomEquiv R P S 𝓀[R] h₁
h₁' : Function.Surjective ⇑φ
h₂' : (RingHom.ker φ).FG
h₃ : 𝓂[Sp] ≤ RingHom.ker ψ
this : Function.Injective ⇑(KaehlerDifferential.cotangentComplexBaseChange 𝓀[R] Sp Pp 𝓀[S])
eᵣ : 𝓀[S] ⊗[Pp] Ω[Pp⁄𝓀[R]] ≃ₗ[S] 𝓀[S] ⊗[P] Ω[P⁄R] :=
  LinearEquiv.restrictScalars S (AlgebraTensorModule.congr (LinearEquiv.refl 𝓀[S] 𝓀[S]) e₀) ≪≫ₗ
    LinearEquiv.restrictScalars S (AlgebraTensorModule.cancelBaseChange P Pp Sp 𝓀[S] Ω[P⁄R])
eₗ : 𝓀[S] ⊗[Pp] ↥(RingHom.ker φ) ≃ₗ[S] 𝓀[S] ⊗[P] ↥(RingHom.ker (algebraMap P S)) :=
  LinearEquiv.restrictScalars S (AlgebraTensorModule.congr (LinearEquiv.refl 𝓀[S] 𝓀[S]) e₁) ≪≫ₗ
    LinearEquiv.restrictScalars S (AlgebraTensorModule.cancelBaseChange P Pp Sp 𝓀[S] ↥(RingHom.ker (algebraMap P S)))
x : 𝓀[S]
y : ↥(RingHom.ker (algebraMap P S))
⊢ (x * 1) ⊗ₜ[P] (KaehlerDifferential.D R P) ↑y =
    (AlgebraTensorModule.cancelBaseChange P (𝓀[R] ⊗[R] P) Sp 𝓀[S] Ω[P⁄R])
      ((x * 1) ⊗ₜ[𝓀[R] ⊗[R] P] e₀ ((KaehlerDifferential.D 𝓀[R] (𝓀[R] ⊗[R] P)) (1 ⊗ₜ[R] (1 * ↑y))))