-- Mathlib/RingTheory/Kaehler/CotangentComplex.lean
@[simp]
lemma repr_CotangentSpaceMap (f : Hom P P') (i j) :
    P'.cotangentSpaceBasis.repr (CotangentSpace.map f.toExtensionHom (P.cotangentSpaceBasis i)) j =
      aeval P'.val (pderiv j (f.val i))

Proof state:
R : Type u
S : Type v
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : Algebra R S
P : Generators R S
R' : Type u'
S' : Type v'
inst✝⁷ : CommRing R'
inst✝⁶ : CommRing S'
inst✝⁵ : Algebra R' S'
P' : Generators R' S'
inst✝⁴ : Algebra R R'
inst✝³ : Algebra S S'
inst✝² : Algebra R S'
inst✝¹ : IsScalarTower R R' S'
inst✝ : IsScalarTower R S S'
f : P.Hom P'
i : P.vars
j : P'.vars
⊢ (P'.cotangentSpaceBasis.repr ((CotangentSpace.map f.toExtensionHom) (P.cotangentSpaceBasis i))) j =
    (aeval P'.val) ((pderiv j) (f.val i))

Tactic:
rw [cotangentSpaceBasis_apply]

Result:
R : Type u
S : Type v
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : Algebra R S
P : Generators R S
R' : Type u'
S' : Type v'
inst✝⁷ : CommRing R'
inst✝⁶ : CommRing S'
inst✝⁵ : Algebra R' S'
P' : Generators R' S'
inst✝⁴ : Algebra R R'
inst✝³ : Algebra S S'
inst✝² : Algebra R S'
inst✝¹ : IsScalarTower R R' S'
inst✝ : IsScalarTower R S S'
f : P.Hom P'
i : P.vars
j : P'.vars
⊢ (P'.cotangentSpaceBasis.repr ((CotangentSpace.map f.toExtensionHom) (1 ⊗ₜ[P.Ring] (D R P.Ring) (X i)))) j =
    (aeval P'.val) ((pderiv j) (f.val i))

Proof state:
R : Type u
S : Type v
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : Algebra R S
P : Generators R S
R' : Type u'
S' : Type v'
inst✝⁷ : CommRing R'
inst✝⁶ : CommRing S'
inst✝⁵ : Algebra R' S'
P' : Generators R' S'
inst✝⁴ : Algebra R R'
inst✝³ : Algebra S S'
inst✝² : Algebra R S'
inst✝¹ : IsScalarTower R R' S'
inst✝ : IsScalarTower R S S'
f : P.Hom P'
i : P.vars
j : P'.vars
⊢ (P'.cotangentSpaceBasis.repr ((CotangentSpace.map f.toExtensionHom) (1 ⊗ₜ[P.Ring] (D R P.Ring) (X i)))) j =
    (aeval P'.val) ((pderiv j) (f.val i))

Tactic:
rw [CotangentSpace.map_tmul, map_one]

Result:
R : Type u
S : Type v
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : Algebra R S
P : Generators R S
R' : Type u'
S' : Type v'
inst✝⁷ : CommRing R'
inst✝⁶ : CommRing S'
inst✝⁵ : Algebra R' S'
P' : Generators R' S'
inst✝⁴ : Algebra R R'
inst✝³ : Algebra S S'
inst✝² : Algebra R S'
inst✝¹ : IsScalarTower R R' S'
inst✝ : IsScalarTower R S S'
f : P.Hom P'
i : P.vars
j : P'.vars
⊢ (P'.cotangentSpaceBasis.repr
        (1 ⊗ₜ[(Extension.mk P'.Ring P'.σ ⋯).Ring]
          (D R' (Extension.mk P'.Ring P'.σ ⋯).Ring) (f.toExtensionHom.toAlgHom (X i))))
      j =
    (aeval P'.val) ((pderiv j) (f.val i))

Proof state:
R : Type u
S : Type v
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : Algebra R S
P : Generators R S
R' : Type u'
S' : Type v'
inst✝⁷ : CommRing R'
inst✝⁶ : CommRing S'
inst✝⁵ : Algebra R' S'
P' : Generators R' S'
inst✝⁴ : Algebra R R'
inst✝³ : Algebra S S'
inst✝² : Algebra R S'
inst✝¹ : IsScalarTower R R' S'
inst✝ : IsScalarTower R S S'
f : P.Hom P'
i : P.vars
j : P'.vars
⊢ (P'.cotangentSpaceBasis.repr
        (1 ⊗ₜ[(Extension.mk P'.Ring P'.σ ⋯).Ring]
          (D R' (Extension.mk P'.Ring P'.σ ⋯).Ring) (f.toExtensionHom.toAlgHom (X i))))
      j =
    (aeval P'.val) ((pderiv j) (f.val i))

Tactic:
erw [cotangentSpaceBasis_repr_one_tmul, Hom.toAlgHom_X]

Result:
no goals