-- Lean 4 proof step from Mathlib.RingTheory.Kaehler.JacobiZariski (goal)
Goal:
R : Type u₁
S : Type u₂
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
T : Type u₃
inst_3 : CommRing T
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
ι : Type w₁
σ : Type w₂
Q : Generators S T ι
P : Generators R S σ
this_1 : AddCommGroup (T ⊗[S] Ω[S⁄R]) := inferInstance
this : IsScalarTower (Generators.Ring (Q.comp P)) (Generators.Ring (Q.comp P)) T
p : MvPolynomial (ι ⊕ σ) R
n : ι ⊕ σ
IH :
  Eq (α := T ⊗[S] Ω[S⁄R])
    ((δAux R Q : (a : Q.Ring) → T ⊗[S] Ω[S⁄R]) ((Hom.toAlgHom (Q.ofComp P) : (a : (Q.comp P).Ring) → Q.Ring) p) :
      T ⊗[S] Ω[S⁄R])
    ((LinearMap.baseChange T P.toExtension.toKaehler : (a : T ⊗[S] P.toExtension.CotangentSpace) → T ⊗[S] Ω[S⁄R])
        ((CotangentSpace.compEquiv Q P :
              (a : (Q.comp P).toExtension.CotangentSpace) →
                Q.toExtension.CotangentSpace × T ⊗[S] P.toExtension.CotangentSpace)
            (1 ⊗ₜ[Generators.Ring (Q.comp P)]
              (D R (Generators.Ring (Q.comp P)) : (a : (Q.comp P).Ring) → Ω[(Q.comp P).Ring⁄R]) p)).2 :
      T ⊗[S] Ω[S⁄R])
⊢ HSMul.hSMul (β := T ⊗[S] Ω[S⁄R])
        (eval₂ (algebraMap R T) (fun (i : ι ⊕ σ) ↦ Sum.elim Q.val ((⇑(algebraMap S T) : (a : S) → T) ∘ P.val) i) p)
        ((δAux R Q : (a : Q.Ring) → T ⊗[S] Ω[S⁄R]) (Sum.elim X ((⇑C : (a : S) → MvPolynomial ι S) ∘ P.val) n) :
          T ⊗[S] Ω[S⁄R]) +
      HSMul.hSMul (α := T) (β := T ⊗[S] Ω[S⁄R])
        ((aeval Q.val : (a : MvPolynomial ι S) → T) (Sum.elim X ((⇑C : (a : S) → MvPolynomial ι S) ∘ P.val) n) : T)
        ((LinearMap.baseChange T P.toExtension.toKaehler : (a : T ⊗[S] P.toExtension.CotangentSpace) → T ⊗[S] Ω[S⁄R])
          ((CotangentSpace.compEquiv Q P :
                (a : (Q.comp P).toExtension.CotangentSpace) →
                  Q.toExtension.CotangentSpace × T ⊗[S] P.toExtension.CotangentSpace)
              (1 ⊗ₜ[Generators.Ring (Q.comp P)]
                (D R (Generators.Ring (Q.comp P)) : (a : (Q.comp P).Ring) → Ω[(Q.comp P).Ring⁄R]) p)).2) =
    HSMul.hSMul (α := T) (β := T ⊗[S] Ω[S⁄R]) ((aeval (val (Q.comp P)) : (a : MvPolynomial (ι ⊕ σ) R) → T) p : T)
        ((LinearMap.baseChange T P.toExtension.toKaehler : (a : T ⊗[S] P.toExtension.CotangentSpace) → T ⊗[S] Ω[S⁄R])
          ((CotangentSpace.compEquiv Q P :
                (a : (Q.comp P).toExtension.CotangentSpace) →
                  Q.toExtension.CotangentSpace × T ⊗[S] P.toExtension.CotangentSpace)
              ((cotangentSpaceBasis (Q.comp P) : (a : ι ⊕ σ) → (Q.comp P).toExtension.CotangentSpace) n)).2) +
      HSMul.hSMul (β := T ⊗[S] Ω[S⁄R]) (Sum.elim Q.val ((⇑(algebraMap S T) : (a : S) → T) ∘ P.val) n)
        ((LinearMap.baseChange T P.toExtension.toKaehler : (a : T ⊗[S] P.toExtension.CotangentSpace) → T ⊗[S] Ω[S⁄R])
          ((CotangentSpace.compEquiv Q P :
                (a : (Q.comp P).toExtension.CotangentSpace) →
                  Q.toExtension.CotangentSpace × T ⊗[S] P.toExtension.CotangentSpace)
              (1 ⊗ₜ[Generators.Ring (Q.comp P)]
                (D R (Generators.Ring (Q.comp P)) : (a : (Q.comp P).Ring) → Ω[(Q.comp P).Ring⁄R]) p)).2)
have mul_X : ∀ (n : ι),
  HSMul.hSMul (β := T ⊗[S] Ω[S⁄R])
        (eval₂ (algebraMap R T) (fun (i : ι ⊕ σ) ↦ Sum.elim Q.val ((⇑(algebraMap S T) : (a : S) → T) ∘ P.val) i) p)
        ((δAux R Q : (a : Q.Ring) → T ⊗[S] Ω[S⁄R])
            (Sum.elim X ((⇑C : (a : S) → MvPolynomial ι S) ∘ P.val) (Sum.inl n)) :
          T ⊗[S] Ω[S⁄R]) +
      HSMul.hSMul (α := T) (β := T ⊗[S] Ω[S⁄R])
        ((aeval Q.val : (a : MvPolynomial ι S) → T)
            (Sum.elim X ((⇑C : (a : S) → MvPolynomial ι S) ∘ P.val) (Sum.inl n)) :
          T)
        ((LinearMap.baseChange T P.toExtension.toKaehler : (a : T ⊗[S] P.toExtension.CotangentSpace) → T ⊗[S] Ω[S⁄R])
          ((CotangentSpace.compEquiv Q P :
                (a : (Q.comp P).toExtension.CotangentSpace) →
                  Q.toExtension.CotangentSpace × T ⊗[S] P.toExtension.CotangentSpace)
              (1 ⊗ₜ[Generators.Ring (Q.comp P)]
                (D R (Generators.Ring (Q.comp P)) : (a : (Q.comp P).Ring) → Ω[(Q.comp P).Ring⁄R]) p)).2) =
    HSMul.hSMul (α := T) (β := T ⊗[S] Ω[S⁄R]) ((aeval (val (Q.comp P)) : (a : MvPolynomial (ι ⊕ σ) R) → T) p : T)
        ((LinearMap.baseChange T P.toExtension.toKaehler : (a : T ⊗[S] P.toExtension.CotangentSpace) → T ⊗[S] Ω[S⁄R])
          ((CotangentSpace.compEquiv Q P :
                (a : (Q.comp P).toExtension.CotangentSpace) →
                  Q.toExtension.CotangentSpace × T ⊗[S] P.toExtension.CotangentSpace)
              ((cotangentSpaceBasis (Q.comp P) : (a : ι ⊕ σ) → (Q.comp P).toExtension.CotangentSpace) (Sum.inl n))).2) +
      HSMul.hSMul (β := T ⊗[S] Ω[S⁄R]) (Sum.elim Q.val ((⇑(algebraMap S T) : (a : S) → T) ∘ P.val) (Sum.inl n))
        ((LinearMap.baseChange T P.toExtension.toKaehler : (a : T ⊗[S] P.toExtension.CotangentSpace) → T ⊗[S] Ω[S⁄R])
          ((CotangentSpace.compEquiv Q P :
                (a : (Q.comp P).toExtension.CotangentSpace) →
                  Q.toExtension.CotangentSpace × T ⊗[S] P.toExtension.CotangentSpace)
              (1 ⊗ₜ[Generators.Ring (Q.comp P)]
                (D R (Generators.Ring (Q.comp P)) : (a : (Q.comp P).Ring) → Ω[(Q.comp P).Ring⁄R]) p)).2)
Tactic: obtain (n | n) := n
Cleared hypotheses: n