Theorem: PolynomialMap.isCompat_apply_ground (DividedPowers/PolynomialMap/Basic.lean)

State before:
R✝ : Type u
inst✝¹¹ : CommRing R✝
M✝ : Type u_1
inst✝¹⁰ : AddCommGroup M✝
inst✝⁹ : Module R✝ M✝
N✝ : Type u_2
inst✝⁸ : AddCommGroup N✝
inst✝⁷ : Module R✝ N✝
f✝ : M✝ →ₚ[R✝] N✝
R : Type u
inst✝⁶ : CommRing R
M : Type u_3
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
N : Type u_4
inst✝³ : AddCommGroup N
inst✝² : Module R N
f : M →ₚ[R] N
S : Type u_5
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : M
⊢ 1 ⊗ₜ[R] f.ground x = f.toFun S (1 ⊗ₜ[R] x)
Tactic:
simp only [ground, ← toFun_eq_toFun']
State after:
R✝ : Type u
inst✝¹¹ : CommRing R✝
M✝ : Type u_1
inst✝¹⁰ : AddCommGroup M✝
inst✝⁹ : Module R✝ M✝
N✝ : Type u_2
inst✝⁸ : AddCommGroup N✝
inst✝⁷ : Module R✝ N✝
f✝ : M✝ →ₚ[R✝] N✝
R : Type u
inst✝⁶ : CommRing R
M : Type u_3
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
N : Type u_4
inst✝³ : AddCommGroup N
inst✝² : Module R N
f : M →ₚ[R] N
S : Type u_5
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : M
⊢ 1 ⊗ₜ[R] (⇑(TensorProduct.lid R N) ∘ f.toFun R ∘ ⇑(TensorProduct.lid R M).symm) x = f.toFun S (1 ⊗ₜ[R] x)

State before:
R✝ : Type u
inst✝¹¹ : CommRing R✝
M✝ : Type u_1
inst✝¹⁰ : AddCommGroup M✝
inst✝⁹ : Module R✝ M✝
N✝ : Type u_2
inst✝⁸ : AddCommGroup N✝
inst✝⁷ : Module R✝ N✝
f✝ : M✝ →ₚ[R✝] N✝
R : Type u
inst✝⁶ : CommRing R
M : Type u_3
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
N : Type u_4
inst✝³ : AddCommGroup N
inst✝² : Module R N
f : M →ₚ[R] N
S : Type u_5
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : M
⊢ 1 ⊗ₜ[R] (⇑(TensorProduct.lid R N) ∘ f.toFun R ∘ ⇑(TensorProduct.lid R M).symm) x = f.toFun S (1 ⊗ₜ[R] x)
Tactic:
convert f.isCompat_apply (algebraMap' R S) (1 ⊗ₜ[R] x)
State after:
case h.e'_2
R✝ : Type u
inst✝¹¹ : CommRing R✝
M✝ : Type u_1
inst✝¹⁰ : AddCommGroup M✝
inst✝⁹ : Module R✝ M✝
N✝ : Type u_2
inst✝⁸ : AddCommGroup N✝
inst✝⁷ : Module R✝ N✝
f✝ : M✝ →ₚ[R✝] N✝
R : Type u
inst✝⁶ : CommRing R
M : Type u_3
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
N : Type u_4
inst✝³ : AddCommGroup N
inst✝² : Module R N
f : M →ₚ[R] N
S : Type u_5
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : M
⊢ 1 ⊗ₜ[R] (⇑(TensorProduct.lid R N) ∘ f.toFun R ∘ ⇑(TensorProduct.lid R M).symm) x =
    (LinearMap.rTensor N (algebraMap' R S).toLinearMap) (f.toFun R (1 ⊗ₜ[R] x))

case h.e'_3.h.e'_13
R✝ : Type u
inst✝¹¹ : CommRing R✝
M✝ : Type u_1
inst✝¹⁰ : AddCommGroup M✝
inst✝⁹ : Module R✝ M✝
N✝ : Type u_2
inst✝⁸ : AddCommGroup N✝
inst✝⁷ : Module R✝ N✝
f✝ : M✝ →ₚ[R✝] N✝
R : Type u
inst✝⁶ : CommRing R
M : Type u_3
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
N : Type u_4
inst✝³ : AddCommGroup N
inst✝² : Module R N
f : M →ₚ[R] N
S : Type u_5
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : M
⊢ 1 ⊗ₜ[R] x = (LinearMap.rTensor M (algebraMap' R S).toLinearMap) (1 ⊗ₜ[R] x)

State before:
case h.e'_2
R✝ : Type u
inst✝¹¹ : CommRing R✝
M✝ : Type u_1
inst✝¹⁰ : AddCommGroup M✝
inst✝⁹ : Module R✝ M✝
N✝ : Type u_2
inst✝⁸ : AddCommGroup N✝
inst✝⁷ : Module R✝ N✝
f✝ : M✝ →ₚ[R✝] N✝
R : Type u
inst✝⁶ : CommRing R
M : Type u_3
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
N : Type u_4
inst✝³ : AddCommGroup N
inst✝² : Module R N
f : M →ₚ[R] N
S : Type u_5
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : M
⊢ 1 ⊗ₜ[R] (⇑(TensorProduct.lid R N) ∘ f.toFun R ∘ ⇑(TensorProduct.lid R M).symm) x =
    (LinearMap.rTensor N (algebraMap' R S).toLinearMap) (f.toFun R (1 ⊗ₜ[R] x))

case h.e'_3.h.e'_13
R✝ : Type u
inst✝¹¹ : CommRing R✝
M✝ : Type u_1
inst✝¹⁰ : AddCommGroup M✝
inst✝⁹ : Module R✝ M✝
N✝ : Type u_2
inst✝⁸ : AddCommGroup N✝
inst✝⁷ : Module R✝ N✝
f✝ : M✝ →ₚ[R✝] N✝
R : Type u
inst✝⁶ : CommRing R
M : Type u_3
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
N : Type u_4
inst✝³ : AddCommGroup N
inst✝² : Module R N
f : M →ₚ[R] N
S : Type u_5
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : M
⊢ 1 ⊗ₜ[R] x = (LinearMap.rTensor M (algebraMap' R S).toLinearMap) (1 ⊗ₜ[R] x)
Tactic:
simp only [Function.comp_apply, TensorProduct.lid_symm_apply, TensorProduct.includeRight_lid]
State after:
case h.e'_3.h.e'_13
R✝ : Type u
inst✝¹¹ : CommRing R✝
M✝ : Type u_1
inst✝¹⁰ : AddCommGroup M✝
inst✝⁹ : Module R✝ M✝
N✝ : Type u_2
inst✝⁸ : AddCommGroup N✝
inst✝⁷ : Module R✝ N✝
f✝ : M✝ →ₚ[R✝] N✝
R : Type u
inst✝⁶ : CommRing R
M : Type u_3
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
N : Type u_4
inst✝³ : AddCommGroup N
inst✝² : Module R N
f : M →ₚ[R] N
S : Type u_5
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : M
⊢ 1 ⊗ₜ[R] x = (LinearMap.rTensor M (algebraMap' R S).toLinearMap) (1 ⊗ₜ[R] x)

State before:
case h.e'_3.h.e'_13
R✝ : Type u
inst✝¹¹ : CommRing R✝
M✝ : Type u_1
inst✝¹⁰ : AddCommGroup M✝
inst✝⁹ : Module R✝ M✝
N✝ : Type u_2
inst✝⁸ : AddCommGroup N✝
inst✝⁷ : Module R✝ N✝
f✝ : M✝ →ₚ[R✝] N✝
R : Type u
inst✝⁶ : CommRing R
M : Type u_3
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
N : Type u_4
inst✝³ : AddCommGroup N
inst✝² : Module R N
f : M →ₚ[R] N
S : Type u_5
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : M
⊢ 1 ⊗ₜ[R] x = (LinearMap.rTensor M (algebraMap' R S).toLinearMap) (1 ⊗ₜ[R] x)
Tactic:
rw [rTensor_tmul, toLinearMap_apply, _root_.map_one]
State after:
no goals