Theorem: PolynomialMap.Finsupp.polynomialMap_toFun_apply (DividedPowers/PolynomialMap/Coeff.lean)

State before:
R : Type u
inst✝⁸ : CommRing R
M : Type uM
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
N : Type uN
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
ι : Type uι
inst✝³ : DecidableEq ι
inst✝² : Fintype ι
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
b✝ : Basis ι R M
h✝ : (ι →₀ ℕ) →₀ N
b : Basis ι R M
h : (ι →₀ ℕ) →₀ N
m : S ⊗[R] M
⊢ (polynomialMap b h).toFun S m = h.sum fun k n => (∏ i : ι, (LinearForm.baseChange R S M (b.coord i)) m ^ k i) ⊗ₜ[R] n
Tactic:
obtain ⟨n, ψ, p, rfl⟩ := PolynomialMap.exists_lift m
State after:
case intro.intro.intro
R : Type u
inst✝⁸ : CommRing R
M : Type uM
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
N : Type uN
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
ι : Type uι
inst✝³ : DecidableEq ι
inst✝² : Fintype ι
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
b✝ : Basis ι R M
h✝ : (ι →₀ ℕ) →₀ N
b : Basis ι R M
h : (ι →₀ ℕ) →₀ N
n : ℕ
ψ : MvPolynomial (Fin n) R →ₐ[R] S
p : MvPolynomial (Fin n) R ⊗[R] M
⊢ (polynomialMap b h).toFun S ((LinearMap.rTensor M ψ.toLinearMap) p) =
    h.sum fun k n_1 =>
      (∏ i : ι, (LinearForm.baseChange R S M (b.coord i)) ((LinearMap.rTensor M ψ.toLinearMap) p) ^ k i) ⊗ₜ[R] n_1

State before:
case intro.intro.intro
R : Type u
inst✝⁸ : CommRing R
M : Type uM
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
N : Type uN
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
ι : Type uι
inst✝³ : DecidableEq ι
inst✝² : Fintype ι
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
b✝ : Basis ι R M
h✝ : (ι →₀ ℕ) →₀ N
b : Basis ι R M
h : (ι →₀ ℕ) →₀ N
n : ℕ
ψ : MvPolynomial (Fin n) R →ₐ[R] S
p : MvPolynomial (Fin n) R ⊗[R] M
⊢ (polynomialMap b h).toFun S ((LinearMap.rTensor M ψ.toLinearMap) p) =
    h.sum fun k n_1 =>
      (∏ i : ι, (LinearForm.baseChange R S M (b.coord i)) ((LinearMap.rTensor M ψ.toLinearMap) p) ^ k i) ⊗ₜ[R] n_1
Tactic:
simp only [← isCompat_apply, toFun_eq_toFun', polynomialMap, polynomialMap_toFun, map_finsupp_sum]
State after:
case intro.intro.intro
R : Type u
inst✝⁸ : CommRing R
M : Type uM
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
N : Type uN
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
ι : Type uι
inst✝³ : DecidableEq ι
inst✝² : Fintype ι
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
b✝ : Basis ι R M
h✝ : (ι →₀ ℕ) →₀ N
b : Basis ι R M
h : (ι →₀ ℕ) →₀ N
n : ℕ
ψ : MvPolynomial (Fin n) R →ₐ[R] S
p : MvPolynomial (Fin n) R ⊗[R] M
⊢ (h.sum fun a b_1 =>
      (LinearMap.rTensor N ψ.toLinearMap)
        ((∏ i : ι, (LinearForm.baseChange R (MvPolynomial (Fin n) R) M (b.coord i)) p ^ a i) ⊗ₜ[R] b_1)) =
    h.sum fun k n_1 =>
      (∏ i : ι, (LinearForm.baseChange R S M (b.coord i)) ((LinearMap.rTensor M ψ.toLinearMap) p) ^ k i) ⊗ₜ[R] n_1

State before:
case intro.intro.intro
R : Type u
inst✝⁸ : CommRing R
M : Type uM
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
N : Type uN
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
ι : Type uι
inst✝³ : DecidableEq ι
inst✝² : Fintype ι
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
b✝ : Basis ι R M
h✝ : (ι →₀ ℕ) →₀ N
b : Basis ι R M
h : (ι →₀ ℕ) →₀ N
n : ℕ
ψ : MvPolynomial (Fin n) R →ₐ[R] S
p : MvPolynomial (Fin n) R ⊗[R] M
⊢ (h.sum fun a b_1 =>
      (LinearMap.rTensor N ψ.toLinearMap)
        ((∏ i : ι, (LinearForm.baseChange R (MvPolynomial (Fin n) R) M (b.coord i)) p ^ a i) ⊗ₜ[R] b_1)) =
    h.sum fun k n_1 =>
      (∏ i : ι, (LinearForm.baseChange R S M (b.coord i)) ((LinearMap.rTensor M ψ.toLinearMap) p) ^ k i) ⊗ₜ[R] n_1
Tactic:
apply Finsupp.sum_congr
State after:
case intro.intro.intro.h
R : Type u
inst✝⁸ : CommRing R
M : Type uM
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
N : Type uN
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
ι : Type uι
inst✝³ : DecidableEq ι
inst✝² : Fintype ι
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
b✝ : Basis ι R M
h✝ : (ι →₀ ℕ) →₀ N
b : Basis ι R M
h : (ι →₀ ℕ) →₀ N
n : ℕ
ψ : MvPolynomial (Fin n) R →ₐ[R] S
p : MvPolynomial (Fin n) R ⊗[R] M
⊢ ∀ x ∈ h.support,
    (LinearMap.rTensor N ψ.toLinearMap)
        ((∏ i : ι, (LinearForm.baseChange R (MvPolynomial (Fin n) R) M (b.coord i)) p ^ x i) ⊗ₜ[R] h x) =
      (∏ i : ι, (LinearForm.baseChange R S M (b.coord i)) ((LinearMap.rTensor M ψ.toLinearMap) p) ^ x i) ⊗ₜ[R] h x

State before:
case intro.intro.intro.h
R : Type u
inst✝⁸ : CommRing R
M : Type uM
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
N : Type uN
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
ι : Type uι
inst✝³ : DecidableEq ι
inst✝² : Fintype ι
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
b✝ : Basis ι R M
h✝ : (ι →₀ ℕ) →₀ N
b : Basis ι R M
h : (ι →₀ ℕ) →₀ N
n : ℕ
ψ : MvPolynomial (Fin n) R →ₐ[R] S
p : MvPolynomial (Fin n) R ⊗[R] M
⊢ ∀ x ∈ h.support,
    (LinearMap.rTensor N ψ.toLinearMap)
        ((∏ i : ι, (LinearForm.baseChange R (MvPolynomial (Fin n) R) M (b.coord i)) p ^ x i) ⊗ₜ[R] h x) =
      (∏ i : ι, (LinearForm.baseChange R S M (b.coord i)) ((LinearMap.rTensor M ψ.toLinearMap) p) ^ x i) ⊗ₜ[R] h x
Tactic:
intro k _
State after:
case intro.intro.intro.h
R : Type u
inst✝⁸ : CommRing R
M : Type uM
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
N : Type uN
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
ι : Type uι
inst✝³ : DecidableEq ι
inst✝² : Fintype ι
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
b✝ : Basis ι R M
h✝ : (ι →₀ ℕ) →₀ N
b : Basis ι R M
h : (ι →₀ ℕ) →₀ N
n : ℕ
ψ : MvPolynomial (Fin n) R →ₐ[R] S
p : MvPolynomial (Fin n) R ⊗[R] M
k : ι →₀ ℕ
a✝ : k ∈ h.support
⊢ (LinearMap.rTensor N ψ.toLinearMap)
      ((∏ i : ι, (LinearForm.baseChange R (MvPolynomial (Fin n) R) M (b.coord i)) p ^ k i) ⊗ₜ[R] h k) =
    (∏ i : ι, (LinearForm.baseChange R S M (b.coord i)) ((LinearMap.rTensor M ψ.toLinearMap) p) ^ k i) ⊗ₜ[R] h k

State before:
case intro.intro.intro.h
R : Type u
inst✝⁸ : CommRing R
M : Type uM
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
N : Type uN
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
ι : Type uι
inst✝³ : DecidableEq ι
inst✝² : Fintype ι
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
b✝ : Basis ι R M
h✝ : (ι →₀ ℕ) →₀ N
b : Basis ι R M
h : (ι →₀ ℕ) →₀ N
n : ℕ
ψ : MvPolynomial (Fin n) R →ₐ[R] S
p : MvPolynomial (Fin n) R ⊗[R] M
k : ι →₀ ℕ
a✝ : k ∈ h.support
⊢ (LinearMap.rTensor N ψ.toLinearMap)
      ((∏ i : ι, (LinearForm.baseChange R (MvPolynomial (Fin n) R) M (b.coord i)) p ^ k i) ⊗ₜ[R] h k) =
    (∏ i : ι, (LinearForm.baseChange R S M (b.coord i)) ((LinearMap.rTensor M ψ.toLinearMap) p) ^ k i) ⊗ₜ[R] h k
Tactic:
rw [LinearMap.rTensor_tmul]
State after:
case intro.intro.intro.h
R : Type u
inst✝⁸ : CommRing R
M : Type uM
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
N : Type uN
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
ι : Type uι
inst✝³ : DecidableEq ι
inst✝² : Fintype ι
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
b✝ : Basis ι R M
h✝ : (ι →₀ ℕ) →₀ N
b : Basis ι R M
h : (ι →₀ ℕ) →₀ N
n : ℕ
ψ : MvPolynomial (Fin n) R →ₐ[R] S
p : MvPolynomial (Fin n) R ⊗[R] M
k : ι →₀ ℕ
a✝ : k ∈ h.support
⊢ ψ.toLinearMap (∏ i : ι, (LinearForm.baseChange R (MvPolynomial (Fin n) R) M (b.coord i)) p ^ k i) ⊗ₜ[R] h k =
    (∏ i : ι, (LinearForm.baseChange R S M (b.coord i)) ((LinearMap.rTensor M ψ.toLinearMap) p) ^ k i) ⊗ₜ[R] h k

State before:
case intro.intro.intro.h
R : Type u
inst✝⁸ : CommRing R
M : Type uM
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
N : Type uN
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
ι : Type uι
inst✝³ : DecidableEq ι
inst✝² : Fintype ι
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
b✝ : Basis ι R M
h✝ : (ι →₀ ℕ) →₀ N
b : Basis ι R M
h : (ι →₀ ℕ) →₀ N
n : ℕ
ψ : MvPolynomial (Fin n) R →ₐ[R] S
p : MvPolynomial (Fin n) R ⊗[R] M
k : ι →₀ ℕ
a✝ : k ∈ h.support
⊢ ψ.toLinearMap (∏ i : ι, (LinearForm.baseChange R (MvPolynomial (Fin n) R) M (b.coord i)) p ^ k i) ⊗ₜ[R] h k =
    (∏ i : ι, (LinearForm.baseChange R S M (b.coord i)) ((LinearMap.rTensor M ψ.toLinearMap) p) ^ k i) ⊗ₜ[R] h k
Tactic:
congr
State after:
case intro.intro.intro.h.e_m
R : Type u
inst✝⁸ : CommRing R
M : Type uM
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
N : Type uN
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
ι : Type uι
inst✝³ : DecidableEq ι
inst✝² : Fintype ι
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
b✝ : Basis ι R M
h✝ : (ι →₀ ℕ) →₀ N
b : Basis ι R M
h : (ι →₀ ℕ) →₀ N
n : ℕ
ψ : MvPolynomial (Fin n) R →ₐ[R] S
p : MvPolynomial (Fin n) R ⊗[R] M
k : ι →₀ ℕ
a✝ : k ∈ h.support
⊢ ψ.toLinearMap (∏ i : ι, (LinearForm.baseChange R (MvPolynomial (Fin n) R) M (b.coord i)) p ^ k i) =
    ∏ i : ι, (LinearForm.baseChange R S M (b.coord i)) ((LinearMap.rTensor M ψ.toLinearMap) p) ^ k i

State before:
case intro.intro.intro.h.e_m
R : Type u
inst✝⁸ : CommRing R
M : Type uM
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
N : Type uN
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
ι : Type uι
inst✝³ : DecidableEq ι
inst✝² : Fintype ι
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
b✝ : Basis ι R M
h✝ : (ι →₀ ℕ) →₀ N
b : Basis ι R M
h : (ι →₀ ℕ) →₀ N
n : ℕ
ψ : MvPolynomial (Fin n) R →ₐ[R] S
p : MvPolynomial (Fin n) R ⊗[R] M
k : ι →₀ ℕ
a✝ : k ∈ h.support
⊢ ψ.toLinearMap (∏ i : ι, (LinearForm.baseChange R (MvPolynomial (Fin n) R) M (b.coord i)) p ^ k i) =
    ∏ i : ι, (LinearForm.baseChange R S M (b.coord i)) ((LinearMap.rTensor M ψ.toLinearMap) p) ^ k i
Tactic:
simp only [AlgHom.toLinearMap_apply, map_prod, map_pow]
State after:
case intro.intro.intro.h.e_m
R : Type u
inst✝⁸ : CommRing R
M : Type uM
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
N : Type uN
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
ι : Type uι
inst✝³ : DecidableEq ι
inst✝² : Fintype ι
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
b✝ : Basis ι R M
h✝ : (ι →₀ ℕ) →₀ N
b : Basis ι R M
h : (ι →₀ ℕ) →₀ N
n : ℕ
ψ : MvPolynomial (Fin n) R →ₐ[R] S
p : MvPolynomial (Fin n) R ⊗[R] M
k : ι →₀ ℕ
a✝ : k ∈ h.support
⊢ ∏ x : ι, ψ ((LinearForm.baseChange R (MvPolynomial (Fin n) R) M (b.coord x)) p) ^ k x =
    ∏ i : ι, (LinearForm.baseChange R S M (b.coord i)) ((LinearMap.rTensor M ψ.toLinearMap) p) ^ k i

State before:
case intro.intro.intro.h.e_m
R : Type u
inst✝⁸ : CommRing R
M : Type uM
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
N : Type uN
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
ι : Type uι
inst✝³ : DecidableEq ι
inst✝² : Fintype ι
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
b✝ : Basis ι R M
h✝ : (ι →₀ ℕ) →₀ N
b : Basis ι R M
h : (ι →₀ ℕ) →₀ N
n : ℕ
ψ : MvPolynomial (Fin n) R →ₐ[R] S
p : MvPolynomial (Fin n) R ⊗[R] M
k : ι →₀ ℕ
a✝ : k ∈ h.support
⊢ ∏ x : ι, ψ ((LinearForm.baseChange R (MvPolynomial (Fin n) R) M (b.coord x)) p) ^ k x =
    ∏ i : ι, (LinearForm.baseChange R S M (b.coord i)) ((LinearMap.rTensor M ψ.toLinearMap) p) ^ k i
Tactic:
apply prod_congr rfl
State after:
case intro.intro.intro.h.e_m
R : Type u
inst✝⁸ : CommRing R
M : Type uM
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
N : Type uN
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
ι : Type uι
inst✝³ : DecidableEq ι
inst✝² : Fintype ι
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
b✝ : Basis ι R M
h✝ : (ι →₀ ℕ) →₀ N
b : Basis ι R M
h : (ι →₀ ℕ) →₀ N
n : ℕ
ψ : MvPolynomial (Fin n) R →ₐ[R] S
p : MvPolynomial (Fin n) R ⊗[R] M
k : ι →₀ ℕ
a✝ : k ∈ h.support
⊢ ∀ x ∈ univ,
    ψ ((LinearForm.baseChange R (MvPolynomial (Fin n) R) M (b.coord x)) p) ^ k x =
      (LinearForm.baseChange R S M (b.coord x)) ((LinearMap.rTensor M ψ.toLinearMap) p) ^ k x

State before:
case intro.intro.intro.h.e_m
R : Type u
inst✝⁸ : CommRing R
M : Type uM
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
N : Type uN
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
ι : Type uι
inst✝³ : DecidableEq ι
inst✝² : Fintype ι
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
b✝ : Basis ι R M
h✝ : (ι →₀ ℕ) →₀ N
b : Basis ι R M
h : (ι →₀ ℕ) →₀ N
n : ℕ
ψ : MvPolynomial (Fin n) R →ₐ[R] S
p : MvPolynomial (Fin n) R ⊗[R] M
k : ι →₀ ℕ
a✝ : k ∈ h.support
⊢ ∀ x ∈ univ,
    ψ ((LinearForm.baseChange R (MvPolynomial (Fin n) R) M (b.coord x)) p) ^ k x =
      (LinearForm.baseChange R S M (b.coord x)) ((LinearMap.rTensor M ψ.toLinearMap) p) ^ k x
Tactic:
intro i _
State after:
case intro.intro.intro.h.e_m
R : Type u
inst✝⁸ : CommRing R
M : Type uM
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
N : Type uN
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
ι : Type uι
inst✝³ : DecidableEq ι
inst✝² : Fintype ι
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
b✝ : Basis ι R M
h✝ : (ι →₀ ℕ) →₀ N
b : Basis ι R M
h : (ι →₀ ℕ) →₀ N
n : ℕ
ψ : MvPolynomial (Fin n) R →ₐ[R] S
p : MvPolynomial (Fin n) R ⊗[R] M
k : ι →₀ ℕ
a✝¹ : k ∈ h.support
i : ι
a✝ : i ∈ univ
⊢ ψ ((LinearForm.baseChange R (MvPolynomial (Fin n) R) M (b.coord i)) p) ^ k i =
    (LinearForm.baseChange R S M (b.coord i)) ((LinearMap.rTensor M ψ.toLinearMap) p) ^ k i

State before:
case intro.intro.intro.h.e_m
R : Type u
inst✝⁸ : CommRing R
M : Type uM
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
N : Type uN
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
ι : Type uι
inst✝³ : DecidableEq ι
inst✝² : Fintype ι
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
b✝ : Basis ι R M
h✝ : (ι →₀ ℕ) →₀ N
b : Basis ι R M
h : (ι →₀ ℕ) →₀ N
n : ℕ
ψ : MvPolynomial (Fin n) R →ₐ[R] S
p : MvPolynomial (Fin n) R ⊗[R] M
k : ι →₀ ℕ
a✝¹ : k ∈ h.support
i : ι
a✝ : i ∈ univ
⊢ ψ ((LinearForm.baseChange R (MvPolynomial (Fin n) R) M (b.coord i)) p) ^ k i =
    (LinearForm.baseChange R S M (b.coord i)) ((LinearMap.rTensor M ψ.toLinearMap) p) ^ k i
Tactic:
apply congr_arg₂ _ _ rfl
State after:
R : Type u
inst✝⁸ : CommRing R
M : Type uM
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
N : Type uN
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
ι : Type uι
inst✝³ : DecidableEq ι
inst✝² : Fintype ι
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
b✝ : Basis ι R M
h✝ : (ι →₀ ℕ) →₀ N
b : Basis ι R M
h : (ι →₀ ℕ) →₀ N
n : ℕ
ψ : MvPolynomial (Fin n) R →ₐ[R] S
p : MvPolynomial (Fin n) R ⊗[R] M
k : ι →₀ ℕ
a✝¹ : k ∈ h.support
i : ι
a✝ : i ∈ univ
⊢ ψ ((LinearForm.baseChange R (MvPolynomial (Fin n) R) M (b.coord i)) p) =
    (LinearForm.baseChange R S M (b.coord i)) ((LinearMap.rTensor M ψ.toLinearMap) p)

State before:
R : Type u
inst✝⁸ : CommRing R
M : Type uM
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
N : Type uN
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
ι : Type uι
inst✝³ : DecidableEq ι
inst✝² : Fintype ι
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
b✝ : Basis ι R M
h✝ : (ι →₀ ℕ) →₀ N
b : Basis ι R M
h : (ι →₀ ℕ) →₀ N
n : ℕ
ψ : MvPolynomial (Fin n) R →ₐ[R] S
p : MvPolynomial (Fin n) R ⊗[R] M
k : ι →₀ ℕ
a✝¹ : k ∈ h.support
i : ι
a✝ : i ∈ univ
⊢ ψ ((LinearForm.baseChange R (MvPolynomial (Fin n) R) M (b.coord i)) p) =
    (LinearForm.baseChange R S M (b.coord i)) ((LinearMap.rTensor M ψ.toLinearMap) p)
Tactic:
rw [LinearForm.baseChange_compat_apply]
State after:
no goals