Theorem: PolynomialMap.Finsupp.polynomialMap_isCompat (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
S : Type u_1
inst✝³ : CommRing S
inst✝² : Algebra R S
S' : Type u_2
inst✝¹ : CommRing S'
inst✝ : Algebra R S'
φ : S →ₐ[R] S'
⊢ ⇑(LinearMap.rTensor N φ.toLinearMap) ∘ polynomialMap_toFun b h S =
    polynomialMap_toFun b h S' ∘ ⇑(LinearMap.rTensor M φ.toLinearMap)
Tactic:
ext m
State after:
case 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
S : Type u_1
inst✝³ : CommRing S
inst✝² : Algebra R S
S' : Type u_2
inst✝¹ : CommRing S'
inst✝ : Algebra R S'
φ : S →ₐ[R] S'
m : S ⊗[R] M
⊢ (⇑(LinearMap.rTensor N φ.toLinearMap) ∘ polynomialMap_toFun b h S) m =
    (polynomialMap_toFun b h S' ∘ ⇑(LinearMap.rTensor M φ.toLinearMap)) m

State before:
case 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
S : Type u_1
inst✝³ : CommRing S
inst✝² : Algebra R S
S' : Type u_2
inst✝¹ : CommRing S'
inst✝ : Algebra R S'
φ : S →ₐ[R] S'
m : S ⊗[R] M
⊢ (⇑(LinearMap.rTensor N φ.toLinearMap) ∘ polynomialMap_toFun b h S) m =
    (polynomialMap_toFun b h S' ∘ ⇑(LinearMap.rTensor M φ.toLinearMap)) m
Tactic:
rw [Function.comp_apply, polynomialMap_toFun, Finsupp.sum, _root_.map_sum]
State after:
case 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
S : Type u_1
inst✝³ : CommRing S
inst✝² : Algebra R S
S' : Type u_2
inst✝¹ : CommRing S'
inst✝ : Algebra R S'
φ : S →ₐ[R] S'
m : S ⊗[R] M
⊢ ∑ x ∈ h.support,
      (LinearMap.rTensor N φ.toLinearMap) ((∏ i : ι, (LinearForm.baseChange R S M (b.coord i)) m ^ x i) ⊗ₜ[R] h x) =
    (polynomialMap_toFun b h S' ∘ ⇑(LinearMap.rTensor M φ.toLinearMap)) m

State before:
case 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
S : Type u_1
inst✝³ : CommRing S
inst✝² : Algebra R S
S' : Type u_2
inst✝¹ : CommRing S'
inst✝ : Algebra R S'
φ : S →ₐ[R] S'
m : S ⊗[R] M
⊢ ∑ x ∈ h.support,
      (LinearMap.rTensor N φ.toLinearMap) ((∏ i : ι, (LinearForm.baseChange R S M (b.coord i)) m ^ x i) ⊗ₜ[R] h x) =
    (polynomialMap_toFun b h S' ∘ ⇑(LinearMap.rTensor M φ.toLinearMap)) m
Tactic:
apply sum_congr rfl
State after:
case 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
S : Type u_1
inst✝³ : CommRing S
inst✝² : Algebra R S
S' : Type u_2
inst✝¹ : CommRing S'
inst✝ : Algebra R S'
φ : S →ₐ[R] S'
m : S ⊗[R] M
⊢ ∀ x ∈ h.support,
    (LinearMap.rTensor N φ.toLinearMap) ((∏ i : ι, (LinearForm.baseChange R S M (b.coord i)) m ^ x i) ⊗ₜ[R] h x) =
      (fun k n =>
          (∏ i : ι, (LinearForm.baseChange R S' M (b.coord i)) ((LinearMap.rTensor M φ.toLinearMap) m) ^ k i) ⊗ₜ[R] n)
        x (h x)

State before:
case 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
S : Type u_1
inst✝³ : CommRing S
inst✝² : Algebra R S
S' : Type u_2
inst✝¹ : CommRing S'
inst✝ : Algebra R S'
φ : S →ₐ[R] S'
m : S ⊗[R] M
⊢ ∀ x ∈ h.support,
    (LinearMap.rTensor N φ.toLinearMap) ((∏ i : ι, (LinearForm.baseChange R S M (b.coord i)) m ^ x i) ⊗ₜ[R] h x) =
      (fun k n =>
          (∏ i : ι, (LinearForm.baseChange R S' M (b.coord i)) ((LinearMap.rTensor M φ.toLinearMap) m) ^ k i) ⊗ₜ[R] n)
        x (h x)
Tactic:
intro k _
State after:
case 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
S : Type u_1
inst✝³ : CommRing S
inst✝² : Algebra R S
S' : Type u_2
inst✝¹ : CommRing S'
inst✝ : Algebra R S'
φ : S →ₐ[R] S'
m : S ⊗[R] M
k : ι →₀ ℕ
a✝ : k ∈ h.support
⊢ (LinearMap.rTensor N φ.toLinearMap) ((∏ i : ι, (LinearForm.baseChange R S M (b.coord i)) m ^ k i) ⊗ₜ[R] h k) =
    (fun k n =>
        (∏ i : ι, (LinearForm.baseChange R S' M (b.coord i)) ((LinearMap.rTensor M φ.toLinearMap) m) ^ k i) ⊗ₜ[R] n)
      k (h k)

State before:
case 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
S : Type u_1
inst✝³ : CommRing S
inst✝² : Algebra R S
S' : Type u_2
inst✝¹ : CommRing S'
inst✝ : Algebra R S'
φ : S →ₐ[R] S'
m : S ⊗[R] M
k : ι →₀ ℕ
a✝ : k ∈ h.support
⊢ (LinearMap.rTensor N φ.toLinearMap) ((∏ i : ι, (LinearForm.baseChange R S M (b.coord i)) m ^ k i) ⊗ₜ[R] h k) =
    (fun k n =>
        (∏ i : ι, (LinearForm.baseChange R S' M (b.coord i)) ((LinearMap.rTensor M φ.toLinearMap) m) ^ k i) ⊗ₜ[R] n)
      k (h k)
Tactic:
simp only [LinearMap.rTensor_tmul, AlgHom.toLinearMap_apply]
State after:
case 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
S : Type u_1
inst✝³ : CommRing S
inst✝² : Algebra R S
S' : Type u_2
inst✝¹ : CommRing S'
inst✝ : Algebra R S'
φ : S →ₐ[R] S'
m : S ⊗[R] M
k : ι →₀ ℕ
a✝ : k ∈ h.support
⊢ φ (∏ i : ι, (LinearForm.baseChange R S M (b.coord i)) m ^ k i) ⊗ₜ[R] h k =
    (∏ i : ι, (LinearForm.baseChange R S' M (b.coord i)) ((LinearMap.rTensor M φ.toLinearMap) m) ^ k i) ⊗ₜ[R] h k

State before:
case 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
S : Type u_1
inst✝³ : CommRing S
inst✝² : Algebra R S
S' : Type u_2
inst✝¹ : CommRing S'
inst✝ : Algebra R S'
φ : S →ₐ[R] S'
m : S ⊗[R] M
k : ι →₀ ℕ
a✝ : k ∈ h.support
⊢ φ (∏ i : ι, (LinearForm.baseChange R S M (b.coord i)) m ^ k i) ⊗ₜ[R] h k =
    (∏ i : ι, (LinearForm.baseChange R S' M (b.coord i)) ((LinearMap.rTensor M φ.toLinearMap) m) ^ k i) ⊗ₜ[R] h k
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
S : Type u_1
inst✝³ : CommRing S
inst✝² : Algebra R S
S' : Type u_2
inst✝¹ : CommRing S'
inst✝ : Algebra R S'
φ : S →ₐ[R] S'
m : S ⊗[R] M
k : ι →₀ ℕ
a✝ : k ∈ h.support
⊢ φ (∏ i : ι, (LinearForm.baseChange R S M (b.coord i)) m ^ k i) =
    ∏ i : ι, (LinearForm.baseChange R S' M (b.coord i)) ((LinearMap.rTensor M φ.toLinearMap) m) ^ k i

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
S : Type u_1
inst✝³ : CommRing S
inst✝² : Algebra R S
S' : Type u_2
inst✝¹ : CommRing S'
inst✝ : Algebra R S'
φ : S →ₐ[R] S'
m : S ⊗[R] M
k : ι →₀ ℕ
a✝ : k ∈ h.support
⊢ φ (∏ i : ι, (LinearForm.baseChange R S M (b.coord i)) m ^ k i) =
    ∏ i : ι, (LinearForm.baseChange R S' M (b.coord i)) ((LinearMap.rTensor M φ.toLinearMap) m) ^ k i
Tactic:
rw [map_prod φ]
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
S : Type u_1
inst✝³ : CommRing S
inst✝² : Algebra R S
S' : Type u_2
inst✝¹ : CommRing S'
inst✝ : Algebra R S'
φ : S →ₐ[R] S'
m : S ⊗[R] M
k : ι →₀ ℕ
a✝ : k ∈ h.support
⊢ ∏ x : ι, φ ((LinearForm.baseChange R S M (b.coord x)) m ^ k x) =
    ∏ i : ι, (LinearForm.baseChange R S' M (b.coord i)) ((LinearMap.rTensor M φ.toLinearMap) m) ^ k i

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
S : Type u_1
inst✝³ : CommRing S
inst✝² : Algebra R S
S' : Type u_2
inst✝¹ : CommRing S'
inst✝ : Algebra R S'
φ : S →ₐ[R] S'
m : S ⊗[R] M
k : ι →₀ ℕ
a✝ : k ∈ h.support
⊢ ∏ x : ι, φ ((LinearForm.baseChange R S M (b.coord x)) m ^ k x) =
    ∏ i : ι, (LinearForm.baseChange R S' M (b.coord i)) ((LinearMap.rTensor M φ.toLinearMap) m) ^ k i
Tactic:
apply prod_congr 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
S : Type u_1
inst✝³ : CommRing S
inst✝² : Algebra R S
S' : Type u_2
inst✝¹ : CommRing S'
inst✝ : Algebra R S'
φ : S →ₐ[R] S'
m : S ⊗[R] M
k : ι →₀ ℕ
a✝ : k ∈ h.support
⊢ ∀ x ∈ univ,
    φ ((LinearForm.baseChange R S M (b.coord x)) m ^ k x) =
      (LinearForm.baseChange R S' M (b.coord x)) ((LinearMap.rTensor M φ.toLinearMap) m) ^ k x

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
S : Type u_1
inst✝³ : CommRing S
inst✝² : Algebra R S
S' : Type u_2
inst✝¹ : CommRing S'
inst✝ : Algebra R S'
φ : S →ₐ[R] S'
m : S ⊗[R] M
k : ι →₀ ℕ
a✝ : k ∈ h.support
⊢ ∀ x ∈ univ,
    φ ((LinearForm.baseChange R S M (b.coord x)) m ^ k x) =
      (LinearForm.baseChange R S' M (b.coord x)) ((LinearMap.rTensor M φ.toLinearMap) m) ^ k x
Tactic:
intro i _
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
S : Type u_1
inst✝³ : CommRing S
inst✝² : Algebra R S
S' : Type u_2
inst✝¹ : CommRing S'
inst✝ : Algebra R S'
φ : S →ₐ[R] S'
m : S ⊗[R] M
k : ι →₀ ℕ
a✝¹ : k ∈ h.support
i : ι
a✝ : i ∈ univ
⊢ φ ((LinearForm.baseChange R S M (b.coord i)) m ^ k i) =
    (LinearForm.baseChange R S' M (b.coord i)) ((LinearMap.rTensor M φ.toLinearMap) m) ^ k i

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
S : Type u_1
inst✝³ : CommRing S
inst✝² : Algebra R S
S' : Type u_2
inst✝¹ : CommRing S'
inst✝ : Algebra R S'
φ : S →ₐ[R] S'
m : S ⊗[R] M
k : ι →₀ ℕ
a✝¹ : k ∈ h.support
i : ι
a✝ : i ∈ univ
⊢ φ ((LinearForm.baseChange R S M (b.coord i)) m ^ k i) =
    (LinearForm.baseChange R S' M (b.coord i)) ((LinearMap.rTensor M φ.toLinearMap) m) ^ k i
Tactic:
rw [map_pow]
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
S : Type u_1
inst✝³ : CommRing S
inst✝² : Algebra R S
S' : Type u_2
inst✝¹ : CommRing S'
inst✝ : Algebra R S'
φ : S →ₐ[R] S'
m : S ⊗[R] M
k : ι →₀ ℕ
a✝¹ : k ∈ h.support
i : ι
a✝ : i ∈ univ
⊢ φ ((LinearForm.baseChange R S M (b.coord i)) m) ^ k i =
    (LinearForm.baseChange R S' M (b.coord i)) ((LinearMap.rTensor M φ.toLinearMap) m) ^ k i

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
S : Type u_1
inst✝³ : CommRing S
inst✝² : Algebra R S
S' : Type u_2
inst✝¹ : CommRing S'
inst✝ : Algebra R S'
φ : S →ₐ[R] S'
m : S ⊗[R] M
k : ι →₀ ℕ
a✝¹ : k ∈ h.support
i : ι
a✝ : i ∈ univ
⊢ φ ((LinearForm.baseChange R S M (b.coord i)) m) ^ k i =
    (LinearForm.baseChange R S' M (b.coord i)) ((LinearMap.rTensor M φ.toLinearMap) m) ^ 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
S : Type u_1
inst✝³ : CommRing S
inst✝² : Algebra R S
S' : Type u_2
inst✝¹ : CommRing S'
inst✝ : Algebra R S'
φ : S →ₐ[R] S'
m : S ⊗[R] M
k : ι →₀ ℕ
a✝¹ : k ∈ h.support
i : ι
a✝ : i ∈ univ
⊢ φ ((LinearForm.baseChange R S M (b.coord i)) m) =
    (LinearForm.baseChange R S' M (b.coord i)) ((LinearMap.rTensor M φ.toLinearMap) m)

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
S : Type u_1
inst✝³ : CommRing S
inst✝² : Algebra R S
S' : Type u_2
inst✝¹ : CommRing S'
inst✝ : Algebra R S'
φ : S →ₐ[R] S'
m : S ⊗[R] M
k : ι →₀ ℕ
a✝¹ : k ∈ h.support
i : ι
a✝ : i ∈ univ
⊢ φ ((LinearForm.baseChange R S M (b.coord i)) m) =
    (LinearForm.baseChange R S' M (b.coord i)) ((LinearMap.rTensor M φ.toLinearMap) m)
Tactic:
rw [LinearForm.baseChange_compat_apply]
State after:
no goals