Module: Mathlib.RingTheory.Kaehler.JacobiZariski

Goal state before:
pp: case mul_X.inl
R : Type u₁
S : Type u₂
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
T : Type u₃
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
ι : Type w₁
σ : Type w₂
Q : Generators S T ι
P : Generators R S σ
this✝ : AddCommGroup (T ⊗[S] Ω[S⁄R]) := inferInstance
this : IsScalarTower (Q.comp P).Ring (Q.comp P).Ring T
p : MvPolynomial (ι ⊕ σ) R
IH :
  (δAux R Q) ((Q.ofComp P).toAlgHom p) =
    (LinearMap.baseChange T P.toExtension.toKaehler)
      ((CotangentSpace.compEquiv Q P) (1 ⊗ₜ[(Q.comp P).Ring] (D R (Q.comp P).Ring) p)).2
n : ι
⊢ eval₂ (algebraMap R T) (fun i ↦ Sum.elim Q.val (⇑(algebraMap S T) ∘ P.val) i) p •
        (δAux R Q) (Sum.elim X (⇑C ∘ P.val) (Sum.inl n)) +
      (aeval Q.val) (Sum.elim X (⇑C ∘ P.val) (Sum.inl n)) •
        (LinearMap.baseChange T P.toExtension.toKaehler)
          ((CotangentSpace.compEquiv Q P) (1 ⊗ₜ[(Q.comp P).Ring] (D R (Q.comp P).Ring) p)).2 =
    (aeval (Q.comp P).val) p •
        (LinearMap.baseChange T P.toExtension.toKaehler)
          ((CotangentSpace.compEquiv Q P) ((Q.comp P).cotangentSpaceBasis (Sum.inl n))).2 +
      Sum.elim Q.val (⇑(algebraMap S T) ∘ P.val) (Sum.inl n) •
        (LinearMap.baseChange T P.toExtension.toKaehler)
          ((CotangentSpace.compEquiv Q P) (1 ⊗ₜ[(Q.comp P).Ring] (D R (Q.comp P).Ring) p)).2

pp: case mul_X.inr
R : Type u₁
S : Type u₂
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
T : Type u₃
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
ι : Type w₁
σ : Type w₂
Q : Generators S T ι
P : Generators R S σ
this✝ : AddCommGroup (T ⊗[S] Ω[S⁄R]) := inferInstance
this : IsScalarTower (Q.comp P).Ring (Q.comp P).Ring T
p : MvPolynomial (ι ⊕ σ) R
IH :
  (δAux R Q) ((Q.ofComp P).toAlgHom p) =
    (LinearMap.baseChange T P.toExtension.toKaehler)
      ((CotangentSpace.compEquiv Q P) (1 ⊗ₜ[(Q.comp P).Ring] (D R (Q.comp P).Ring) p)).2
n : σ
⊢ eval₂ (algebraMap R T) (fun i ↦ Sum.elim Q.val (⇑(algebraMap S T) ∘ P.val) i) p •
        (δAux R Q) (Sum.elim X (⇑C ∘ P.val) (Sum.inr n)) +
      (aeval Q.val) (Sum.elim X (⇑C ∘ P.val) (Sum.inr n)) •
        (LinearMap.baseChange T P.toExtension.toKaehler)
          ((CotangentSpace.compEquiv Q P) (1 ⊗ₜ[(Q.comp P).Ring] (D R (Q.comp P).Ring) p)).2 =
    (aeval (Q.comp P).val) p •
        (LinearMap.baseChange T P.toExtension.toKaehler)
          ((CotangentSpace.compEquiv Q P) ((Q.comp P).cotangentSpaceBasis (Sum.inr n))).2 +
      Sum.elim Q.val (⇑(algebraMap S T) ∘ P.val) (Sum.inr n) •
        (LinearMap.baseChange T P.toExtension.toKaehler)
          ((CotangentSpace.compEquiv Q P) (1 ⊗ₜ[(Q.comp P).Ring] (D R (Q.comp P).Ring) p)).2

Tactic:
·

Goal state after:
case mul_X.inl
R : Type u₁
S : Type u₂
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
T : Type u₃
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
ι : Type w₁
σ : Type w₂
Q : Generators S T ι
P : Generators R S σ
this✝ : AddCommGroup (T ⊗[S] Ω[S⁄R]) := inferInstance
this : IsScalarTower (Q.comp P).Ring (Q.comp P).Ring T
p : MvPolynomial (ι ⊕ σ) R
IH :
  (δAux R Q) ((Q.ofComp P).toAlgHom p) =
    (LinearMap.baseChange T P.toExtension.toKaehler)
      ((CotangentSpace.compEquiv Q P) (1 ⊗ₜ[(Q.comp P).Ring] (D R (Q.comp P).Ring) p)).2
n : ι
⊢ eval₂ (algebraMap R T) (fun i ↦ Sum.elim Q.val (⇑(algebraMap S T) ∘ P.val) i) p •
        (δAux R Q) (Sum.elim X (⇑C ∘ P.val) (Sum.inl n)) +
      (aeval Q.val) (Sum.elim X (⇑C ∘ P.val) (Sum.inl n)) •
        (LinearMap.baseChange T P.toExtension.toKaehler)
          ((CotangentSpace.compEquiv Q P) (1 ⊗ₜ[(Q.comp P).Ring] (D R (Q.comp P).Ring) p)).2 =
    (aeval (Q.comp P).val) p •
        (LinearMap.baseChange T P.toExtension.toKaehler)
          ((CotangentSpace.compEquiv Q P) ((Q.comp P).cotangentSpaceBasis (Sum.inl n))).2 +
      Sum.elim Q.val (⇑(algebraMap S T) ∘ P.val) (Sum.inl n) •
        (LinearMap.baseChange T P.toExtension.toKaehler)
          ((CotangentSpace.compEquiv Q P) (1 ⊗ₜ[(Q.comp P).Ring] (D R (Q.comp P).Ring) p)).2