-- 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 σ
apply apply₁ :
  ∀ (i : ι ⊕ σ),
    Eq (α := Q.toExtension.CotangentSpace)
      ((LinearMap.fst T Q.toExtension.CotangentSpace (T ⊗[S] P.toExtension.CotangentSpace) ∘ₗ
              (↑(compEquiv Q P) :
                (Q.comp P).toExtension.CotangentSpace →ₗ[T]
                  Q.toExtension.CotangentSpace × T ⊗[S] P.toExtension.CotangentSpace) :
            (a : (Q.comp P).toExtension.CotangentSpace) → Q.toExtension.CotangentSpace)
          ((cotangentSpaceBasis (Q.comp P) : (a : ι ⊕ σ) → (Q.comp P).toExtension.CotangentSpace) i) :
        Q.toExtension.CotangentSpace)
      ((Extension.CotangentSpace.map (Hom.toExtensionHom (Q.ofComp P)) :
            (a : (Q.comp P).toExtension.CotangentSpace) → Q.toExtension.CotangentSpace)
          ((cotangentSpaceBasis (Q.comp P) : (a : ι ⊕ σ) → (Q.comp P).toExtension.CotangentSpace) i) :
        Q.toExtension.CotangentSpace)
a :
  ∀ (i : ι ⊕ σ),
    Eq (α := ι →₀ T)
      ((Q.cotangentSpaceBasis.repr : (a : Q.toExtension.CotangentSpace) → ι →₀ T)
          ((LinearMap.fst T Q.toExtension.CotangentSpace (T ⊗[S] P.toExtension.CotangentSpace) ∘ₗ
                (↑(compEquiv Q P) :
                  (Q.comp P).toExtension.CotangentSpace →ₗ[T]
                    Q.toExtension.CotangentSpace × T ⊗[S] P.toExtension.CotangentSpace) :
              (a : (Q.comp P).toExtension.CotangentSpace) → Q.toExtension.CotangentSpace)
            ((cotangentSpaceBasis (Q.comp P) : (a : ι ⊕ σ) → (Q.comp P).toExtension.CotangentSpace) i)) :
        ι →₀ T)
      ((Q.cotangentSpaceBasis.repr : (a : Q.toExtension.CotangentSpace) → ι →₀ T)
          ((Extension.CotangentSpace.map (Hom.toExtensionHom (Q.ofComp P)) :
              (a : (Q.comp P).toExtension.CotangentSpace) → Q.toExtension.CotangentSpace)
            ((cotangentSpaceBasis (Q.comp P) : (a : ι ⊕ σ) → (Q.comp P).toExtension.CotangentSpace) i)) :
        ι →₀ T)
⊢ Eq (α := Extension.CotangentSpace (toExtension (Q.comp P)) →ₗ[T] Q.toExtension.CotangentSpace)
    (LinearMap.fst T Q.toExtension.CotangentSpace (T ⊗[S] P.toExtension.CotangentSpace) ∘ₗ
      (↑(compEquiv Q P) :
        (Q.comp P).toExtension.CotangentSpace →ₗ[T] Q.toExtension.CotangentSpace × T ⊗[S] P.toExtension.CotangentSpace))
    (Extension.CotangentSpace.map (Hom.toExtensionHom (Q.ofComp P)))
have a₁ : ∀ (i : ι ⊕ σ) (j : ι),
  Eq.{u₃ + 1} (α := T)
    ((((Q.cotangentSpaceBasis.repr : (a : Q.toExtension.CotangentSpace) → ι →₀ T)
              ((LinearMap.fst T Q.toExtension.CotangentSpace (T ⊗[S] P.toExtension.CotangentSpace) ∘ₗ
                    (↑(compEquiv Q P) :
                      (Q.comp P).toExtension.CotangentSpace →ₗ[T]
                        Q.toExtension.CotangentSpace × T ⊗[S] P.toExtension.CotangentSpace) :
                  (a : (Q.comp P).toExtension.CotangentSpace) → Q.toExtension.CotangentSpace)
                ((cotangentSpaceBasis (Q.comp P) : (a : ι ⊕ σ) → (Q.comp P).toExtension.CotangentSpace) i)) :
            ι →₀ T) :
          (a : ι) → T)
        j :
      T)
    ((((Q.cotangentSpaceBasis.repr : (a : Q.toExtension.CotangentSpace) → ι →₀ T)
              ((Extension.CotangentSpace.map (Hom.toExtensionHom (Q.ofComp P)) :
                  (a : (Q.comp P).toExtension.CotangentSpace) → Q.toExtension.CotangentSpace)
                ((cotangentSpaceBasis (Q.comp P) : (a : ι ⊕ σ) → (Q.comp P).toExtension.CotangentSpace) i)) :
            ι →₀ T) :
          (a : ι) → T)
        j :
      T)
Tactic: classical
  apply (Q.comp P).cotangentSpaceBasis.ext
  intro i
  apply Q.cotangentSpaceBasis.repr.injective
  ext j
  simp only [compEquiv, LinearMap.coe_comp, LinearEquiv.coe_coe, Function.comp_apply, ofComp_val,
    LinearEquiv.trans_apply, Basis.repr_self, LinearMap.fst_apply, repr_CotangentSpaceMap]
  obtain (i | i) := i <;>
    simp only [Basis.repr_symm_apply, Finsupp.linearCombination_single, Basis.prod_apply,
      LinearMap.coe_inl, LinearMap.coe_inr, Sum.elim_inl, Function.comp_apply, one_smul,
      Basis.repr_self, Finsupp.single_apply, pderiv_X, Pi.single_apply,
      Sum.elim_inr, Function.comp_apply, Basis.baseChange_apply, one_smul,
      MonoidWithZeroHom.map_ite_one_zero, map_zero, Finsupp.coe_zero, Pi.zero_apply, derivation_C]