-- Mathlib/RingTheory/Kaehler/Polynomial.lean
@[simp]
lemma KaehlerDifferential.mvPolynomialBasis_repr_apply (σ) (x) (i) :
    (mvPolynomialBasis R σ).repr (D _ _ x) i = MvPolynomial.pderiv i x

Proof state:
R : Type u
inst✝ : CommRing R
σ : Type u_1
x : MvPolynomial σ R
i : σ
this : (Finsupp.lapply i ∘ₗ ↑(mvPolynomialBasis R σ).repr).compDer (D R (MvPolynomial σ R)) = MvPolynomial.pderiv i
⊢ ((mvPolynomialBasis R σ).repr ((D R (MvPolynomial σ R)) x)) i =
    ((Finsupp.lapply i ∘ₗ ↑(mvPolynomialBasis R σ).repr).compDer (D R (MvPolynomial σ R))) x

Tactic:
rfl

Result:
no goals

Proof state:
case h
R : Type u
inst✝ : CommRing R
σ : Type u_1
x : MvPolynomial σ R
i j : σ
⊢ ((Finsupp.lapply i ∘ₗ ↑(mvPolynomialBasis R σ).repr).compDer (D R (MvPolynomial σ R))) (MvPolynomial.X j) =
    (MvPolynomial.pderiv i) (MvPolynomial.X j)

Tactic:
simp [Finsupp.single_apply, Pi.single_apply]

Result:
no goals

Proof state:
case h
R : Type u
inst✝ : CommRing R
σ : Type u_1
x : MvPolynomial σ R
i : σ
⊢ ∀ (i_1 : σ),
    ((Finsupp.lapply i ∘ₗ ↑(mvPolynomialBasis R σ).repr).compDer (D R (MvPolynomial σ R))) (MvPolynomial.X i_1) =
      (MvPolynomial.pderiv i) (MvPolynomial.X i_1)

Tactic:
intro j

Result:
case h
R : Type u
inst✝ : CommRing R
σ : Type u_1
x : MvPolynomial σ R
i j : σ
⊢ ((Finsupp.lapply i ∘ₗ ↑(mvPolynomialBasis R σ).repr).compDer (D R (MvPolynomial σ R))) (MvPolynomial.X j) =
    (MvPolynomial.pderiv i) (MvPolynomial.X j)

Proof state:
R : Type u
inst✝ : CommRing R
σ : Type u_1
x : MvPolynomial σ R
i : σ
⊢ ((mvPolynomialBasis R σ).repr ((D R (MvPolynomial σ R)) x)) i = (MvPolynomial.pderiv i) x

Tactic:
classical
suffices ((Finsupp.lapply i).comp
  (mvPolynomialBasis R σ).repr.toLinearMap).compDer (D _ _) = MvPolynomial.pderiv i by
  rw [← this]; rfl
apply MvPolynomial.derivation_ext
intro j
simp [Finsupp.single_apply, Pi.single_apply]

Result:
no goals

Proof state:
R : Type u
inst✝ : CommRing R
σ : Type u_1
x : MvPolynomial σ R
i : σ
this : (Finsupp.lapply i ∘ₗ ↑(mvPolynomialBasis R σ).repr).compDer (D R (MvPolynomial σ R)) = MvPolynomial.pderiv i
⊢ ((mvPolynomialBasis R σ).repr ((D R (MvPolynomial σ R)) x)) i = (MvPolynomial.pderiv i) x

Tactic:
rw [← this]

Result:
R : Type u
inst✝ : CommRing R
σ : Type u_1
x : MvPolynomial σ R
i : σ
this : (Finsupp.lapply i ∘ₗ ↑(mvPolynomialBasis R σ).repr).compDer (D R (MvPolynomial σ R)) = MvPolynomial.pderiv i
⊢ ((mvPolynomialBasis R σ).repr ((D R (MvPolynomial σ R)) x)) i =
    ((Finsupp.lapply i ∘ₗ ↑(mvPolynomialBasis R σ).repr).compDer (D R (MvPolynomial σ R))) x

Proof state:
R : Type u
inst✝ : CommRing R
σ : Type u_1
x : MvPolynomial σ R
i : σ
⊢ ((mvPolynomialBasis R σ).repr ((D R (MvPolynomial σ R)) x)) i = (MvPolynomial.pderiv i) x

Tactic:
suffices ((Finsupp.lapply i).comp
  (mvPolynomialBasis R σ).repr.toLinearMap).compDer (D _ _) = MvPolynomial.pderiv i by
  rw [← this]; rfl

Result:
R : Type u
inst✝ : CommRing R
σ : Type u_1
x : MvPolynomial σ R
i : σ
⊢ (Finsupp.lapply i ∘ₗ ↑(mvPolynomialBasis R σ).repr).compDer (D R (MvPolynomial σ R)) = MvPolynomial.pderiv i

Proof state:
R : Type u
inst✝ : CommRing R
σ : Type u_1
x : MvPolynomial σ R
i : σ
⊢ (Finsupp.lapply i ∘ₗ ↑(mvPolynomialBasis R σ).repr).compDer (D R (MvPolynomial σ R)) = MvPolynomial.pderiv i

Tactic:
apply MvPolynomial.derivation_ext

Result:
case h
R : Type u
inst✝ : CommRing R
σ : Type u_1
x : MvPolynomial σ R
i : σ
⊢ ∀ (i_1 : σ),
    ((Finsupp.lapply i ∘ₗ ↑(mvPolynomialBasis R σ).repr).compDer (D R (MvPolynomial σ R))) (MvPolynomial.X i_1) =
      (MvPolynomial.pderiv i) (MvPolynomial.X i_1)