-- Mathlib/RingTheory/Kaehler/JacobiZariski.lean
lemma CotangentSpace.fst_compEquiv :
    LinearMap.fst T Q.toExtension.CotangentSpace (T ⊗[S] P.toExtension.CotangentSpace) ∘ₗ
      (compEquiv Q P).toLinearMap = Extension.CotangentSpace.map (Q.ofComp P).toExtensionHom

Proof state:
R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
T : Type uT
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
Q : Generators S T
P : Generators R S
⊢ LinearMap.fst T Q.toExtension.CotangentSpace (T ⊗[S] P.toExtension.CotangentSpace) ∘ₗ ↑(compEquiv Q P) =
    Extension.CotangentSpace.map (Q.ofComp P).toExtensionHom

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 [comp_vars, 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, RingHom.map_ite_one_zero,
    Sum.elim_inr, Function.comp_apply, Basis.baseChange_apply, one_smul,
    map_zero, Finsupp.coe_zero, Pi.zero_apply, derivation_C]

Result:
no goals

Proof state:
R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
T : Type uT
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
Q : Generators S T
P : Generators R S
⊢ LinearMap.fst T Q.toExtension.CotangentSpace (T ⊗[S] P.toExtension.CotangentSpace) ∘ₗ ↑(compEquiv Q P) =
    Extension.CotangentSpace.map (Q.ofComp P).toExtensionHom

Tactic:
apply (Q.comp P).cotangentSpaceBasis.ext

Result:
R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
T : Type uT
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
Q : Generators S T
P : Generators R S
⊢ ∀ (i : (Q.comp P).vars),
    (LinearMap.fst T Q.toExtension.CotangentSpace (T ⊗[S] P.toExtension.CotangentSpace) ∘ₗ ↑(compEquiv Q P))
        ((Q.comp P).cotangentSpaceBasis i) =
      (Extension.CotangentSpace.map (Q.ofComp P).toExtensionHom) ((Q.comp P).cotangentSpaceBasis i)

Proof state:
case a.h
R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
T : Type uT
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
Q : Generators S T
P : Generators R S
i : (Q.comp P).vars
j : Q.vars
⊢ (Q.cotangentSpaceBasis.repr
        ((Q.cotangentSpaceBasis.prod (Basis.baseChange T P.cotangentSpaceBasis)).repr.symm (Finsupp.single i 1)).1)
      j =
    (aeval Q.val) ((pderiv j) (Sum.elim X (⇑C ∘ P.val) i))

Tactic:
obtain (i | i) := i <;>
  simp only [comp_vars, 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, RingHom.map_ite_one_zero,
    Sum.elim_inr, Function.comp_apply, Basis.baseChange_apply, one_smul,
    map_zero, Finsupp.coe_zero, Pi.zero_apply, derivation_C]

Result:
no goals

Proof state:
case a
R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
T : Type uT
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
Q : Generators S T
P : Generators R S
i : (Q.comp P).vars
⊢ Q.cotangentSpaceBasis.repr
      ((LinearMap.fst T Q.toExtension.CotangentSpace (T ⊗[S] P.toExtension.CotangentSpace) ∘ₗ ↑(compEquiv Q P))
        ((Q.comp P).cotangentSpaceBasis i)) =
    Q.cotangentSpaceBasis.repr
      ((Extension.CotangentSpace.map (Q.ofComp P).toExtensionHom) ((Q.comp P).cotangentSpaceBasis i))

Tactic:
ext j

Result:
case a.h
R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
T : Type uT
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
Q : Generators S T
P : Generators R S
i : (Q.comp P).vars
j : Q.vars
⊢ (Q.cotangentSpaceBasis.repr
        ((LinearMap.fst T Q.toExtension.CotangentSpace (T ⊗[S] P.toExtension.CotangentSpace) ∘ₗ ↑(compEquiv Q P))
          ((Q.comp P).cotangentSpaceBasis i)))
      j =
    (Q.cotangentSpaceBasis.repr
        ((Extension.CotangentSpace.map (Q.ofComp P).toExtensionHom) ((Q.comp P).cotangentSpaceBasis i)))
      j

Proof state:
R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
T : Type uT
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
Q : Generators S T
P : Generators R S
⊢ ∀ (i : (Q.comp P).vars),
    (LinearMap.fst T Q.toExtension.CotangentSpace (T ⊗[S] P.toExtension.CotangentSpace) ∘ₗ ↑(compEquiv Q P))
        ((Q.comp P).cotangentSpaceBasis i) =
      (Extension.CotangentSpace.map (Q.ofComp P).toExtensionHom) ((Q.comp P).cotangentSpaceBasis i)

Tactic:
intro i

Result:
R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
T : Type uT
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
Q : Generators S T
P : Generators R S
i : (Q.comp P).vars
⊢ (LinearMap.fst T Q.toExtension.CotangentSpace (T ⊗[S] P.toExtension.CotangentSpace) ∘ₗ ↑(compEquiv Q P))
      ((Q.comp P).cotangentSpaceBasis i) =
    (Extension.CotangentSpace.map (Q.ofComp P).toExtensionHom) ((Q.comp P).cotangentSpaceBasis i)

Proof state:
R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
T : Type uT
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
Q : Generators S T
P : Generators R S
i : (Q.comp P).vars
⊢ (LinearMap.fst T Q.toExtension.CotangentSpace (T ⊗[S] P.toExtension.CotangentSpace) ∘ₗ ↑(compEquiv Q P))
      ((Q.comp P).cotangentSpaceBasis i) =
    (Extension.CotangentSpace.map (Q.ofComp P).toExtensionHom) ((Q.comp P).cotangentSpaceBasis i)

Tactic:
apply Q.cotangentSpaceBasis.repr.injective

Result:
case a
R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
T : Type uT
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
Q : Generators S T
P : Generators R S
i : (Q.comp P).vars
⊢ Q.cotangentSpaceBasis.repr
      ((LinearMap.fst T Q.toExtension.CotangentSpace (T ⊗[S] P.toExtension.CotangentSpace) ∘ₗ ↑(compEquiv Q P))
        ((Q.comp P).cotangentSpaceBasis i)) =
    Q.cotangentSpaceBasis.repr
      ((Extension.CotangentSpace.map (Q.ofComp P).toExtensionHom) ((Q.comp P).cotangentSpaceBasis i))