-- Module: Mathlib.RingTheory.Kaehler.JacobiZariski
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 σ
x : Generators.Ring (Q.comp P)
this_1 : AddCommGroup (T ⊗[S] Ω[S⁄R]) := inferInstance
this : IsScalarTower (Generators.Ring (Q.comp P)) (Generators.Ring (Q.comp P)) T
C :
  ∀ (s : R),
    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)
            ((MvPolynomial.C : (a : R) → MvPolynomial (ι ⊕ σ) R) s)) :
        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])
                  ((MvPolynomial.C : (a : R) → MvPolynomial (ι ⊕ σ) R) s))).2 :
        T ⊗[S] Ω[S⁄R])
add :
  ∀ (x₁ x₂ : MvPolynomial (ι ⊕ σ) R)
    (hx₁ :
      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) x₁) :
          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]) x₁)).2 :
          T ⊗[S] Ω[S⁄R]))
    (hx₂ :
      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) x₂) :
          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]) x₂)).2 :
          T ⊗[S] Ω[S⁄R])),
    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) (x₁ + x₂)) :
        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]) (x₁ + x₂))).2 :
        T ⊗[S] Ω[S⁄R])
mul_X :
  ∀ (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])),
    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 * X n)) :
        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 * X n))).2 :
        T ⊗[S] Ω[S⁄R])
⊢ 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) x) :
      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]) x)).2 :
      T ⊗[S] Ω[S⁄R])

Tactic:
induction x using MvPolynomial.induction_on with
  | C s =>
    simp only [algHom_C, δAux_C, derivation_C, Derivation.map_algebraMap,
      tmul_zero, map_zero, MvPolynomial.algebraMap_apply, Prod.snd_zero]
  | add x₁ x₂ hx₁ hx₂ =>
    simp only [map_add, hx₁, hx₂, tmul_add, Prod.snd_add]
  | mul_X p n IH =>
    simp only [map_mul, Hom.toAlgHom_X, ofComp_val, δAux_mul,
      ← @IsScalarTower.algebraMap_smul Q.Ring T, algebraMap_apply, Hom.algebraMap_toAlgHom,
      algebraMap_self, map_aeval, RingHomCompTriple.comp_eq, comp_val, RingHom.id_apply,
      IH, Derivation.leibniz, tmul_add, tmul_smul, ← cotangentSpaceBasis_apply, coe_eval₂Hom,
      ← @IsScalarTower.algebraMap_smul (Q.comp P).Ring T, aeval_X, map_smul, Prod.snd_add,
      Prod.smul_snd, map_add]
    obtain (n | n) := n
    · simp only [Sum.elim_inl, δAux_X, smul_zero, aeval_X,
        CotangentSpace.compEquiv, LinearEquiv.trans_apply, Basis.repr_symm_apply, zero_add,
        Basis.repr_self, Finsupp.linearCombination_single, Basis.prod_apply, LinearMap.coe_inl,
        LinearMap.coe_inr, Function.comp_apply, one_smul, map_zero]
    · simp only [Sum.elim_inr, Function.comp_apply, algHom_C, δAux_C,
        CotangentSpace.compEquiv, LinearEquiv.trans_apply, Basis.repr_symm_apply,
        algebraMap_smul, Basis.repr_self, Finsupp.linearCombination_single, Basis.prod_apply,
        LinearMap.coe_inr, Basis.baseChange_apply, one_smul, LinearMap.baseChange_tmul,
        toKaehler_cotangentSpaceBasis, add_left_inj, LinearMap.coe_inl]
      rfl

Premises used: Algebra.Generators.H1Cotangent.δAux_mul, Algebra.Generators.cotangentSpaceBasis_apply, Algebra.Generators.CotangentSpace.compEquiv, MvPolynomial.aeval_X, RingHom.id_apply, Algebra.algebraMap_self, LinearMap.coe_inr, MvPolynomial.map_aeval, RingHomCompTriple.comp_eq, Algebra.Generators.H1Cotangent.δAux_C, Algebra.Generators.ofComp_val, Algebra.Generators.algebraMap_apply, TensorProduct.tmul_smul, smul_zero, Algebra.Generators.comp_val, TensorProduct.tmul_zero, map_zero, Module.Basis.prod_apply, map_add, LinearEquiv.trans_apply, MvPolynomial.algebraMap_apply, algebraMap_smul, Algebra.Generators.Hom.toAlgHom_X, add_left_inj, MvPolynomial.induction_on, Module.Basis.baseChange_apply, MvPolynomial.coe_eval₂Hom, zero_add, MvPolynomial.algHom_C, MvPolynomial.derivation_C, Finsupp.linearCombination_single, one_smul, Derivation.leibniz, Derivation.map_algebraMap, Sum.elim_inr, IsScalarTower.algebraMap_smul, map_mul, LinearMap.coe_inl, Algebra.Generators.H1Cotangent.δAux_X, Algebra.Generators.toKaehler_cotangentSpaceBasis, Prod.smul_snd, TensorProduct.tmul_add, Sum.elim_inl, Function.comp_apply, Module.Basis.repr_symm_apply, LinearMap.baseChange_tmul, MvPolynomial.C, Algebra.Generators.Hom.algebraMap_toAlgHom, Prod.snd_add, Module.Basis.repr_self, map_smul, Prod.snd_zero