Theorem: PolynomialMap.generize_comp_equiv' (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 ι
κ : Type u_1
inst✝¹ : Fintype κ
inst✝ : DecidableEq κ
e : ι ≃ κ
m : κ → M
f : M →ₚ[R] N
⊢ (generize fun x => m (e x)) f = (LinearMap.rTensor N (aeval fun i => X (e.symm i)).toLinearMap) ((generize m) f)
Tactic:
let hf' := f.isCompat_apply
  (aeval (fun i ↦ X (e.symm i)) : MvPolynomial κ R →ₐ[R] MvPolynomial ι R)
  (univ.sum (fun i ↦ X i ⊗ₜ[R] (m 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 ι
κ : Type u_1
inst✝¹ : Fintype κ
inst✝ : DecidableEq κ
e : ι ≃ κ
m : κ → M
f : M →ₚ[R] N
hf' : (LinearMap.rTensor N (aeval fun i => X (e.symm i)).toLinearMap)
    (f.toFun (MvPolynomial κ R) (∑ i : κ, X i ⊗ₜ[R] m i)) =
  f.toFun (MvPolynomial ι R)
    ((LinearMap.rTensor M (aeval fun i => X (e.symm i)).toLinearMap) (∑ i : κ, X i ⊗ₜ[R] m i)) :=
  isCompat_apply f (aeval fun i => X (e.symm i)) (∑ i : κ, X i ⊗ₜ[R] m i)
⊢ (generize fun x => m (e x)) f = (LinearMap.rTensor N (aeval fun i => X (e.symm i)).toLinearMap) ((generize m) f)

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 ι
κ : Type u_1
inst✝¹ : Fintype κ
inst✝ : DecidableEq κ
e : ι ≃ κ
m : κ → M
f : M →ₚ[R] N
hf' : (LinearMap.rTensor N (aeval fun i => X (e.symm i)).toLinearMap)
    (f.toFun (MvPolynomial κ R) (∑ i : κ, X i ⊗ₜ[R] m i)) =
  f.toFun (MvPolynomial ι R)
    ((LinearMap.rTensor M (aeval fun i => X (e.symm i)).toLinearMap) (∑ i : κ, X i ⊗ₜ[R] m i)) :=
  isCompat_apply f (aeval fun i => X (e.symm i)) (∑ i : κ, X i ⊗ₜ[R] m i)
⊢ (generize fun x => m (e x)) f = (LinearMap.rTensor N (aeval fun i => X (e.symm i)).toLinearMap) ((generize m) f)
Tactic:
simp only [map_sum, rTensor_tmul, AlgHom.toLinearMap_apply, aeval_X] at hf'
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 ι
κ : Type u_1
inst✝¹ : Fintype κ
inst✝ : DecidableEq κ
e : ι ≃ κ
m : κ → M
f : M →ₚ[R] N
hf' :
  (LinearMap.rTensor N (aeval fun i => X (e.symm i)).toLinearMap)
      (f.toFun (MvPolynomial κ R) (∑ i : κ, X i ⊗ₜ[R] m i)) =
    f.toFun (MvPolynomial ι R) (∑ x : κ, X (e.symm x) ⊗ₜ[R] m x)
⊢ (generize fun x => m (e x)) f = (LinearMap.rTensor N (aeval fun i => X (e.symm i)).toLinearMap) ((generize m) f)

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 ι
κ : Type u_1
inst✝¹ : Fintype κ
inst✝ : DecidableEq κ
e : ι ≃ κ
m : κ → M
f : M →ₚ[R] N
hf' :
  (LinearMap.rTensor N (aeval fun i => X (e.symm i)).toLinearMap)
      (f.toFun (MvPolynomial κ R) (∑ i : κ, X i ⊗ₜ[R] m i)) =
    f.toFun (MvPolynomial ι R) (∑ x : κ, X (e.symm x) ⊗ₜ[R] m x)
⊢ (generize fun x => m (e x)) f = (LinearMap.rTensor N (aeval fun i => X (e.symm i)).toLinearMap) ((generize m) f)
Tactic:
simp only [generize, coe_mk, AddHom.coe_mk, hf']
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 ι
κ : Type u_1
inst✝¹ : Fintype κ
inst✝ : DecidableEq κ
e : ι ≃ κ
m : κ → M
f : M →ₚ[R] N
hf' :
  (LinearMap.rTensor N (aeval fun i => X (e.symm i)).toLinearMap)
      (f.toFun (MvPolynomial κ R) (∑ i : κ, X i ⊗ₜ[R] m i)) =
    f.toFun (MvPolynomial ι R) (∑ x : κ, X (e.symm x) ⊗ₜ[R] m x)
⊢ f.toFun (MvPolynomial ι R) (∑ x : ι, X x ⊗ₜ[R] m (e x)) = f.toFun (MvPolynomial ι R) (∑ x : κ, X (e.symm x) ⊗ₜ[R] m 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 ι
κ : Type u_1
inst✝¹ : Fintype κ
inst✝ : DecidableEq κ
e : ι ≃ κ
m : κ → M
f : M →ₚ[R] N
hf' :
  (LinearMap.rTensor N (aeval fun i => X (e.symm i)).toLinearMap)
      (f.toFun (MvPolynomial κ R) (∑ i : κ, X i ⊗ₜ[R] m i)) =
    f.toFun (MvPolynomial ι R) (∑ x : κ, X (e.symm x) ⊗ₜ[R] m x)
⊢ f.toFun (MvPolynomial ι R) (∑ x : ι, X x ⊗ₜ[R] m (e x)) = f.toFun (MvPolynomial ι R) (∑ x : κ, X (e.symm x) ⊗ₜ[R] m x)
Tactic:
apply congr_arg
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 ι
κ : Type u_1
inst✝¹ : Fintype κ
inst✝ : DecidableEq κ
e : ι ≃ κ
m : κ → M
f : M →ₚ[R] N
hf' :
  (LinearMap.rTensor N (aeval fun i => X (e.symm i)).toLinearMap)
      (f.toFun (MvPolynomial κ R) (∑ i : κ, X i ⊗ₜ[R] m i)) =
    f.toFun (MvPolynomial ι R) (∑ x : κ, X (e.symm x) ⊗ₜ[R] m x)
⊢ ∑ x : ι, X x ⊗ₜ[R] m (e x) = ∑ x : κ, X (e.symm x) ⊗ₜ[R] m 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 ι
κ : Type u_1
inst✝¹ : Fintype κ
inst✝ : DecidableEq κ
e : ι ≃ κ
m : κ → M
f : M →ₚ[R] N
hf' :
  (LinearMap.rTensor N (aeval fun i => X (e.symm i)).toLinearMap)
      (f.toFun (MvPolynomial κ R) (∑ i : κ, X i ⊗ₜ[R] m i)) =
    f.toFun (MvPolynomial ι R) (∑ x : κ, X (e.symm x) ⊗ₜ[R] m x)
⊢ ∑ x : ι, X x ⊗ₜ[R] m (e x) = ∑ x : κ, X (e.symm x) ⊗ₜ[R] m x
Tactic:
simp only [sum_congr_equiv e, map_univ_equiv]
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 ι
κ : Type u_1
inst✝¹ : Fintype κ
inst✝ : DecidableEq κ
e : ι ≃ κ
m : κ → M
f : M →ₚ[R] N
hf' :
  (LinearMap.rTensor N (aeval fun i => X (e.symm i)).toLinearMap)
      (f.toFun (MvPolynomial κ R) (∑ i : κ, X i ⊗ₜ[R] m i)) =
    f.toFun (MvPolynomial ι R) (∑ x : κ, X (e.symm x) ⊗ₜ[R] m x)
⊢ ∑ x : κ, ((fun x => X x ⊗ₜ[R] m (e x)) ∘ ⇑e.symm) x = ∑ x : κ, X (e.symm x) ⊗ₜ[R] m 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 ι
κ : Type u_1
inst✝¹ : Fintype κ
inst✝ : DecidableEq κ
e : ι ≃ κ
m : κ → M
f : M →ₚ[R] N
hf' :
  (LinearMap.rTensor N (aeval fun i => X (e.symm i)).toLinearMap)
      (f.toFun (MvPolynomial κ R) (∑ i : κ, X i ⊗ₜ[R] m i)) =
    f.toFun (MvPolynomial ι R) (∑ x : κ, X (e.symm x) ⊗ₜ[R] m x)
⊢ ∑ x : κ, ((fun x => X x ⊗ₜ[R] m (e x)) ∘ ⇑e.symm) x = ∑ x : κ, X (e.symm x) ⊗ₜ[R] m x
Tactic:
exact sum_congr rfl (fun k _ => by rw [Function.comp_apply, Equiv.apply_symm_apply])
State after:
no goals

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 ι
κ : Type u_1
inst✝¹ : Fintype κ
inst✝ : DecidableEq κ
e : ι ≃ κ
m : κ → M
f : M →ₚ[R] N
hf' :
  (LinearMap.rTensor N (aeval fun i => X (e.symm i)).toLinearMap)
      (f.toFun (MvPolynomial κ R) (∑ i : κ, X i ⊗ₜ[R] m i)) =
    f.toFun (MvPolynomial ι R) (∑ x : κ, X (e.symm x) ⊗ₜ[R] m x)
k : κ
x✝ : k ∈ univ
⊢ ((fun x => X x ⊗ₜ[R] m (e x)) ∘ ⇑e.symm) k = X (e.symm k) ⊗ₜ[R] m k
Tactic:
rw [Function.comp_apply, Equiv.apply_symm_apply]
State after:
no goals