-- Mathlib/Algebra/Module/Presentation/Differentials.lean
lemma comm₁₂_single (r : pres.rels) :
    pres.toExtension.cotangentComplex (hom₁ pres (Finsupp.single r 1)) =
      pres.cotangentSpaceBasis.repr.symm ((differentialsRelations pres).relation r)

Proof state:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
pres : Presentation R S
r : pres.rels
⊢ pres.cotangentSpaceBasis.repr (1 ⊗ₜ[pres.toExtension.Ring] (D R pres.toExtension.Ring) (pres.relation r)) =
    pres.cotangentSpaceBasis.repr
      ((Finsupp.linearCombination S ⇑pres.cotangentSpaceBasis)
        (Finsupp.mapRange ⇑(algebraMap pres.Ring S) ⋯
          ((mvPolynomialBasis R pres.vars).repr ((D R (MvPolynomial pres.vars R)) (pres.relation r)))))

Tactic:
ext

Result:
case h
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
pres : Presentation R S
r : pres.rels
a✝ : pres.vars
⊢ (pres.cotangentSpaceBasis.repr (1 ⊗ₜ[pres.toExtension.Ring] (D R pres.toExtension.Ring) (pres.relation r))) a✝ =
    (pres.cotangentSpaceBasis.repr
        ((Finsupp.linearCombination S ⇑pres.cotangentSpaceBasis)
          (Finsupp.mapRange ⇑(algebraMap pres.Ring S) ⋯
            ((mvPolynomialBasis R pres.vars).repr ((D R (MvPolynomial pres.vars R)) (pres.relation r))))))
      a✝

Proof state:
case h
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
pres : Presentation R S
r : pres.rels
a✝ : pres.vars
⊢ (pres.cotangentSpaceBasis.repr (1 ⊗ₜ[pres.toExtension.Ring] (D R pres.toExtension.Ring) (pres.relation r))) a✝ =
    (pres.cotangentSpaceBasis.repr
        ((Finsupp.linearCombination S ⇑pres.cotangentSpaceBasis)
          (Finsupp.mapRange ⇑(algebraMap pres.Ring S) ⋯
            ((mvPolynomialBasis R pres.vars).repr ((D R (MvPolynomial pres.vars R)) (pres.relation r))))))
      a✝

Tactic:
simp

Result:
no goals

Proof state:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
pres : Presentation R S
r : pres.rels
⊢ 1 ⊗ₜ[pres.toExtension.Ring] (D R pres.toExtension.Ring) (pres.relation r) =
    (Finsupp.linearCombination S ⇑pres.cotangentSpaceBasis)
      (Finsupp.mapRange ⇑(algebraMap pres.Ring S) ⋯
        ((mvPolynomialBasis R pres.vars).repr ((D R (MvPolynomial pres.vars R)) (pres.relation r))))

Tactic:
exact pres.cotangentSpaceBasis.repr.injective (by ext; simp)

Result:
no goals

Proof state:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
pres : Presentation R S
r : pres.rels
⊢ pres.toExtension.cotangentComplex ((hom₁ pres) (Finsupp.single r 1)) =
    pres.cotangentSpaceBasis.repr.symm (pres.differentialsRelations.relation r)

Tactic:
simp only [hom₁, Finsupp.linearCombination_single, one_smul, differentialsRelations,
  Basis.repr_symm_apply, Extension.cotangentComplex_mk]

Result:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
pres : Presentation R S
r : pres.rels
⊢ 1 ⊗ₜ[pres.toExtension.Ring] (D R pres.toExtension.Ring) (pres.relation r) =
    (Finsupp.linearCombination S ⇑pres.cotangentSpaceBasis)
      (Finsupp.mapRange ⇑(algebraMap pres.Ring S) ⋯
        ((mvPolynomialBasis R pres.vars).repr ((D R (MvPolynomial pres.vars R)) (pres.relation r))))