-- 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'
x : Q.Ring
this_1 : AddCommGroup (T ⊗[S] Ω[S⁄R]) := inferInstance
this : IsScalarTower Q.Ring Q.Ring T
C :
  ∀ (s : S),
    (δAux R Q' : (a : Q'.Ring) → T ⊗[S] Ω[S⁄R])
        ((f.toAlgHom : (a : Q.Ring) → Q'.Ring) ((MvPolynomial.C : (a : S) → MvPolynomial ι S) s)) =
      HAdd.hAdd (α := T ⊗[S] Ω[S⁄R]) (β := T ⊗[S] Ω[S⁄R])
        ((δAux R Q : (a : Q.Ring) → T ⊗[S] Ω[S⁄R]) ((MvPolynomial.C : (a : S) → MvPolynomial ι S) s) : 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]) ((MvPolynomial.C : (a : S) → MvPolynomial ι S) s))) :
          T ⊗[S] Ω[S⁄R])
add :
  ∀ (x₁ x₂ : MvPolynomial ι S)
    (hx₁ :
      (δAux R Q' : (a : Q'.Ring) → T ⊗[S] Ω[S⁄R]) ((f.toAlgHom : (a : Q.Ring) → Q'.Ring) x₁) =
        HAdd.hAdd (α := T ⊗[S] Ω[S⁄R]) (β := T ⊗[S] Ω[S⁄R])
          ((δAux R Q : (a : Q.Ring) → T ⊗[S] Ω[S⁄R]) x₁ : 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]) x₁)) :
            T ⊗[S] Ω[S⁄R]))
    (hx₂ :
      (δAux R Q' : (a : Q'.Ring) → T ⊗[S] Ω[S⁄R]) ((f.toAlgHom : (a : Q.Ring) → Q'.Ring) x₂) =
        HAdd.hAdd (α := T ⊗[S] Ω[S⁄R]) (β := T ⊗[S] Ω[S⁄R])
          ((δAux R Q : (a : Q.Ring) → T ⊗[S] Ω[S⁄R]) x₂ : 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]) x₂)) :
            T ⊗[S] Ω[S⁄R])),
    (δAux R Q' : (a : Q'.Ring) → T ⊗[S] Ω[S⁄R]) ((f.toAlgHom : (a : Q.Ring) → Q'.Ring) (x₁ + x₂)) =
      HAdd.hAdd (α := T ⊗[S] Ω[S⁄R]) (β := T ⊗[S] Ω[S⁄R])
        ((δAux R Q : (a : Q.Ring) → T ⊗[S] Ω[S⁄R]) (x₁ + x₂) : 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]) (x₁ + x₂))) :
          T ⊗[S] Ω[S⁄R])
⊢ (δAux R Q' : (a : Q'.Ring) → T ⊗[S] Ω[S⁄R]) ((f.toAlgHom : (a : Q.Ring) → Q'.Ring) x) =
    HAdd.hAdd (α := T ⊗[S] Ω[S⁄R]) (β := T ⊗[S] Ω[S⁄R]) ((δAux R Q : (a : Q.Ring) → T ⊗[S] Ω[S⁄R]) x : 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]) x)) :
        T ⊗[S] Ω[S⁄R])
have mul_X : ∀ (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])),
  (δAux R Q' : (a : Q'.Ring) → T ⊗[S] Ω[S⁄R]) ((f.toAlgHom : (a : Q.Ring) → Q'.Ring) (p * X n)) =
    HAdd.hAdd (α := T ⊗[S] Ω[S⁄R]) (β := T ⊗[S] Ω[S⁄R])
      ((δAux R Q : (a : Q.Ring) → T ⊗[S] Ω[S⁄R]) (p * X n) : 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 * X n))) :
        T ⊗[S] Ω[S⁄R])
Tactic: induction x using MvPolynomial.induction_on with
  | C s => simp [MvPolynomial.algebraMap_eq, δAux_C]
  | add x₁ x₂ hx₁ hx₂ =>
    simp only [map_add, hx₁, hx₂, tmul_add]
    rw [add_add_add_comm]
  | mul_X p n IH =>
    simp only [map_mul, Hom.toAlgHom_X, δAux_mul, algebraMap_apply, Hom.algebraMap_toAlgHom,
      ← @IsScalarTower.algebraMap_smul Q'.Ring T, algebraMap_self, δAux_X,
      RingHom.id_apply, coe_eval₂Hom, IH, Hom.aeval_val, smul_add, map_aeval, tmul_add, tmul_smul,
      ← @IsScalarTower.algebraMap_smul Q.Ring T, smul_zero, aeval_X, zero_add, Derivation.leibniz,
      Basis.repr_self, map_add, one_smul, map_smul, Finsupp.linearCombination_single,
      RingHomCompTriple.comp_eq, Function.comp_apply, ← cotangentSpaceBasis_apply]
    rw [add_left_comm]
    rfl
Cleared hypotheses: x