-- 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 σ
apply apply₁ :
  ∀ (i : σ),
    Eq (α := Extension.CotangentSpace (toExtension (Q.comp P)))
      (((↑(LinearEquiv.symm (compEquiv Q P)) :
                Q.toExtension.CotangentSpace × T ⊗[S] P.toExtension.CotangentSpace →ₗ[T]
                  (Q.comp P).toExtension.CotangentSpace) ∘ₗ
              LinearMap.inr T Q.toExtension.CotangentSpace (T ⊗[S] P.toExtension.CotangentSpace) :
            (a : T ⊗[S] P.toExtension.CotangentSpace) → (Q.comp P).toExtension.CotangentSpace)
          ((Basis.baseChange T P.cotangentSpaceBasis : (a : σ) → T ⊗[S] P.toExtension.CotangentSpace) i) :
        Extension.CotangentSpace (toExtension (Q.comp P)))
      ((LinearMap.liftBaseChange T (Extension.CotangentSpace.map (Hom.toExtensionHom (Q.toComp P))) :
            (a : T ⊗[S] P.toExtension.CotangentSpace) → (Q.comp P).toExtension.CotangentSpace)
          ((Basis.baseChange T P.cotangentSpaceBasis : (a : σ) → T ⊗[S] P.toExtension.CotangentSpace) i) :
        Extension.CotangentSpace (toExtension (Q.comp P)))
a :
  ∀ (i : σ),
    Eq (α := ι ⊕ σ →₀ T)
      ((Basis.repr (cotangentSpaceBasis (Q.comp P)) : (a : (Q.comp P).toExtension.CotangentSpace) → ι ⊕ σ →₀ T)
          (((↑(LinearEquiv.symm (compEquiv Q P)) :
                  Q.toExtension.CotangentSpace × T ⊗[S] P.toExtension.CotangentSpace →ₗ[T]
                    (Q.comp P).toExtension.CotangentSpace) ∘ₗ
                LinearMap.inr T Q.toExtension.CotangentSpace (T ⊗[S] P.toExtension.CotangentSpace) :
              (a : T ⊗[S] P.toExtension.CotangentSpace) → (Q.comp P).toExtension.CotangentSpace)
            ((Basis.baseChange T P.cotangentSpaceBasis : (a : σ) → T ⊗[S] P.toExtension.CotangentSpace) i)) :
        ι ⊕ σ →₀ T)
      ((Basis.repr (cotangentSpaceBasis (Q.comp P)) : (a : (Q.comp P).toExtension.CotangentSpace) → ι ⊕ σ →₀ T)
          ((LinearMap.liftBaseChange T (Extension.CotangentSpace.map (Hom.toExtensionHom (Q.toComp P))) :
              (a : T ⊗[S] P.toExtension.CotangentSpace) → (Q.comp P).toExtension.CotangentSpace)
            ((Basis.baseChange T P.cotangentSpaceBasis : (a : σ) → T ⊗[S] P.toExtension.CotangentSpace) i)) :
        ι ⊕ σ →₀ T)
a₁ :
  ∀ (i : σ) (j : ι ⊕ σ),
    Eq.{u₃ + 1} (α := T)
      ((((Basis.repr (cotangentSpaceBasis (Q.comp P)) : (a : (Q.comp P).toExtension.CotangentSpace) → ι ⊕ σ →₀ T)
                (((↑(LinearEquiv.symm (compEquiv Q P)) :
                        Q.toExtension.CotangentSpace × T ⊗[S] P.toExtension.CotangentSpace →ₗ[T]
                          (Q.comp P).toExtension.CotangentSpace) ∘ₗ
                      LinearMap.inr T Q.toExtension.CotangentSpace (T ⊗[S] P.toExtension.CotangentSpace) :
                    (a : T ⊗[S] P.toExtension.CotangentSpace) → (Q.comp P).toExtension.CotangentSpace)
                  ((Basis.baseChange T P.cotangentSpaceBasis : (a : σ) → T ⊗[S] P.toExtension.CotangentSpace) i)) :
              ι ⊕ σ →₀ T) :
            (a : ι ⊕ σ) → T)
          j :
        T)
      ((((Basis.repr (cotangentSpaceBasis (Q.comp P)) : (a : (Q.comp P).toExtension.CotangentSpace) → ι ⊕ σ →₀ T)
                ((LinearMap.liftBaseChange T (Extension.CotangentSpace.map (Hom.toExtensionHom (Q.toComp P))) :
                    (a : T ⊗[S] P.toExtension.CotangentSpace) → (Q.comp P).toExtension.CotangentSpace)
                  ((Basis.baseChange T P.cotangentSpaceBasis : (a : σ) → T ⊗[S] P.toExtension.CotangentSpace) i)) :
              ι ⊕ σ →₀ T) :
            (a : ι ⊕ σ) → T)
          j :
        T)
a₂ :
  ∀ (i : σ) (j : ι ⊕ σ),
    Eq.{u₃ + 1} (α := T)
      ((((Basis.repr (Q.cotangentSpaceBasis.prod (Basis.baseChange T P.cotangentSpaceBasis)) :
                  (a : Q.toExtension.CotangentSpace × T ⊗[S] P.toExtension.CotangentSpace) → ι ⊕ σ →₀ T)
                (0, 1 ⊗ₜ[S] (P.cotangentSpaceBasis : (a : σ) → P.toExtension.CotangentSpace) i) :
              ι ⊕ σ →₀ T) :
            (a : ι ⊕ σ) → T)
          j :
        T)
      ((aeval (val (Q.comp P)) : (a : MvPolynomial (ι ⊕ σ) R) → T)
          (Pi.single (M := fun (x : ι ⊕ σ) ↦ MvPolynomial (ι ⊕ σ) R) j
              (1 : (fun (x : ι ⊕ σ) ↦ MvPolynomial (ι ⊕ σ) R) j) (Sum.inr i) :
            MvPolynomial (ι ⊕ σ) R) :
        T)
⊢ Eq (α := T ⊗[S] P.toExtension.CotangentSpace →ₗ[T] Extension.CotangentSpace (toExtension (Q.comp P)))
    ((↑(LinearEquiv.symm (compEquiv Q P)) :
        Q.toExtension.CotangentSpace × T ⊗[S] P.toExtension.CotangentSpace →ₗ[T]
          (Q.comp P).toExtension.CotangentSpace) ∘ₗ
      LinearMap.inr T Q.toExtension.CotangentSpace (T ⊗[S] P.toExtension.CotangentSpace))
    (LinearMap.liftBaseChange T (Extension.CotangentSpace.map (Hom.toExtensionHom (Q.toComp P))))

Tactic:
classical
  apply (P.cotangentSpaceBasis.baseChange T).ext
  intro i
  apply (Q.comp P).cotangentSpaceBasis.repr.injective
  ext j
  simp only [compEquiv, LinearEquiv.trans_symm, LinearEquiv.symm_symm,
    Basis.baseChange_apply, LinearMap.coe_comp, LinearEquiv.coe_coe, LinearMap.coe_inr,
    Function.comp_apply, LinearEquiv.trans_apply, Basis.repr_symm_apply, pderiv_X, toComp_val,
    Basis.repr_linearCombination, LinearMap.liftBaseChange_tmul, one_smul, repr_CotangentSpaceMap]
  obtain (j | j) := j <;>
    simp only [Basis.prod_repr_inr, Basis.baseChange_repr_tmul,
      Basis.repr_self, Basis.prod_repr_inl, map_zero, Finsupp.coe_zero,
      Pi.zero_apply, ne_eq, not_false_eq_true, Pi.single_eq_of_ne, Pi.single_apply,
      Finsupp.single_apply, ite_smul, one_smul, zero_smul, Sum.inr.injEq,
      MonoidWithZeroHom.map_ite_one_zero, reduceCtorEq]

Premises used: reduceCtorEq, Algebra.Generators.CotangentSpace.compEquiv, Module.Basis.prod_repr_inl, Algebra.Generators.comp, LinearMap.coe_inr, Sum.inr.injEq, Algebra.Generators.toComp_val, Pi.single_apply, Module.Basis.repr_linearCombination, MvPolynomial.pderiv_X, Pi.zero_apply, map_zero, Pi.single_eq_of_ne, LinearEquiv.trans_apply, Algebra.Generators.cotangentSpaceBasis, Module.Basis.baseChange_apply, Module.Basis.repr, ne_eq, LinearEquiv.symm_symm, one_smul, zero_smul, LinearMap.liftBaseChange_tmul, Module.Basis.baseChange, LinearMap.coe_comp, Algebra.Generators.repr_CotangentSpaceMap, MonoidWithZeroHom.map_ite_one_zero, Module.Basis.baseChange_repr_tmul, Finsupp.single_apply, ite_smul, Function.comp_apply, LinearEquiv.trans_symm, Module.Basis.prod_repr_inr, LinearEquiv.injective, Module.Basis.repr_symm_apply, not_false_eq_true, Module.Basis.ext, Module.Basis.repr_self, Finsupp.coe_zero, LinearEquiv.coe_coe