-- 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 ι
Q' : Generators S T ι'
f : Q.Hom Q'
this_1 : AddCommGroup (T ⊗[S] Ω[S⁄R]) := inferInstance
this : IsScalarTower Q.Ring Q.Ring T
p : MvPolynomial ι S
n : ι
IH :
  (δAux R Q' : (a : Q'.Ring) → T ⊗[S] Ω[S⁄R]) ((f.toAlgHom : (a : Q.Ring) → Q'.Ring) p) =
    HAdd.hAdd (α := T ⊗[S] Ω[S⁄R]) (β := T ⊗[S] Ω[S⁄R]) ((δAux R Q : (a : Q.Ring) → T ⊗[S] Ω[S⁄R]) p : T ⊗[S] Ω[S⁄R])
      ((Finsupp.linearCombination T ((⇑(δAux R Q') : (a : Q'.Ring) → T ⊗[S] Ω[S⁄R]) ∘ f.val) :
            (a : ι →₀ T) → T ⊗[S] Ω[S⁄R])
          ((Q.cotangentSpaceBasis.repr : (a : Q.toExtension.CotangentSpace) → ι →₀ T)
            (1 ⊗ₜ[Q.Ring] (D S Q.Ring : (a : Q.Ring) → Ω[Q.Ring⁄S]) p)) :
        T ⊗[S] Ω[S⁄R])
⊢ HSMul.hSMul (β := T ⊗[S] Ω[S⁄R]) (eval₂ (algebraMap S T) (fun (i : ι) ↦ Q.val i) p)
        ((δAux R Q' : (a : Q'.Ring) → T ⊗[S] Ω[S⁄R]) (f.val n) : T ⊗[S] Ω[S⁄R]) +
      (HSMul.hSMul (β := T ⊗[S] Ω[S⁄R]) (Q.val n) ((δAux R Q : (a : Q.Ring) → T ⊗[S] Ω[S⁄R]) p : T ⊗[S] Ω[S⁄R]) +
        HSMul.hSMul (β := T ⊗[S] Ω[S⁄R]) (Q.val n)
          ((Finsupp.linearCombination T ((⇑(δAux R Q') : (a : Q'.Ring) → T ⊗[S] Ω[S⁄R]) ∘ f.val) :
                (a : ι →₀ T) → T ⊗[S] Ω[S⁄R])
              ((Q.cotangentSpaceBasis.repr : (a : Q.toExtension.CotangentSpace) → ι →₀ T)
                (1 ⊗ₜ[Q.Ring] (D S Q.Ring : (a : Q.Ring) → Ω[Q.Ring⁄S]) p)) :
            T ⊗[S] Ω[S⁄R])) =
    HSMul.hSMul (β := T ⊗[S] Ω[S⁄R]) (Q.val n) ((δAux R Q : (a : Q.Ring) → T ⊗[S] Ω[S⁄R]) p : T ⊗[S] Ω[S⁄R]) +
      (HSMul.hSMul (α := T) (β := T ⊗[S] Ω[S⁄R]) ((aeval Q.val : (a : MvPolynomial ι S) → T) p : T)
          ((δAux R Q' : (a : Q'.Ring) → T ⊗[S] Ω[S⁄R]) (f.val n) : T ⊗[S] Ω[S⁄R]) +
        HSMul.hSMul (β := T ⊗[S] Ω[S⁄R]) (Q.val n)
          ((Finsupp.linearCombination T ((⇑(δAux R Q') : (a : Q'.Ring) → T ⊗[S] Ω[S⁄R]) ∘ f.val) :
                (a : ι →₀ T) → T ⊗[S] Ω[S⁄R])
              ((Q.cotangentSpaceBasis.repr : (a : Q.toExtension.CotangentSpace) → ι →₀ T)
                (1 ⊗ₜ[Q.Ring] (D S Q.Ring : (a : Q.Ring) → Ω[Q.Ring⁄S]) p)) :
            T ⊗[S] Ω[S⁄R]))
have mul_X : HSMul.hSMul (β := T ⊗[S] Ω[S⁄R]) (Q.val n) ((δAux R Q : (a : Q.Ring) → T ⊗[S] Ω[S⁄R]) p : T ⊗[S] Ω[S⁄R]) +
    (HSMul.hSMul (β := T ⊗[S] Ω[S⁄R]) (eval₂ (algebraMap S T) (fun (i : ι) ↦ Q.val i) p)
        ((δAux R Q' : (a : Q'.Ring) → T ⊗[S] Ω[S⁄R]) (f.val n) : T ⊗[S] Ω[S⁄R]) +
      HSMul.hSMul (β := T ⊗[S] Ω[S⁄R]) (Q.val n)
        ((Finsupp.linearCombination T ((⇑(δAux R Q') : (a : Q'.Ring) → T ⊗[S] Ω[S⁄R]) ∘ f.val) :
              (a : ι →₀ T) → T ⊗[S] Ω[S⁄R])
            ((Q.cotangentSpaceBasis.repr : (a : Q.toExtension.CotangentSpace) → ι →₀ T)
              (1 ⊗ₜ[Q.Ring] (D S Q.Ring : (a : Q.Ring) → Ω[Q.Ring⁄S]) p)) :
          T ⊗[S] Ω[S⁄R])) =
  HSMul.hSMul (β := T ⊗[S] Ω[S⁄R]) (Q.val n) ((δAux R Q : (a : Q.Ring) → T ⊗[S] Ω[S⁄R]) p : T ⊗[S] Ω[S⁄R]) +
    (HSMul.hSMul (α := T) (β := T ⊗[S] Ω[S⁄R]) ((aeval Q.val : (a : MvPolynomial ι S) → T) p : T)
        ((δAux R Q' : (a : Q'.Ring) → T ⊗[S] Ω[S⁄R]) (f.val n) : T ⊗[S] Ω[S⁄R]) +
      HSMul.hSMul (β := T ⊗[S] Ω[S⁄R]) (Q.val n)
        ((Finsupp.linearCombination T ((⇑(δAux R Q') : (a : Q'.Ring) → T ⊗[S] Ω[S⁄R]) ∘ f.val) :
              (a : ι →₀ T) → T ⊗[S] Ω[S⁄R])
            ((Q.cotangentSpaceBasis.repr : (a : Q.toExtension.CotangentSpace) → ι →₀ T)
              (1 ⊗ₜ[Q.Ring] (D S Q.Ring : (a : Q.Ring) → Ω[Q.Ring⁄S]) p)) :
          T ⊗[S] Ω[S⁄R]))
Tactic: rw [add_left_comm]