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 m) f = (LinearMap.rTensor N (aeval fun i => X (e i)).toLinearMap) ((generize fun x => m (e x)) f)
Tactic:
let hf := f.isCompat_apply (aeval (fun i ↦ X (e i)) : MvPolynomial ι R →ₐ[R] MvPolynomial κ R)
  (univ.sum (fun i ↦ X i ⊗ₜ[R] (m (e 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 i)).toLinearMap)
    (f.toFun (MvPolynomial ι R) (∑ i : ι, X i ⊗ₜ[R] m (e i))) =
  f.toFun (MvPolynomial κ R)
    ((LinearMap.rTensor M (aeval fun i => X (e i)).toLinearMap) (∑ i : ι, X i ⊗ₜ[R] m (e i))) :=
  isCompat_apply f (aeval fun i => X (e i)) (∑ i : ι, X i ⊗ₜ[R] m (e i))
⊢ (generize m) f = (LinearMap.rTensor N (aeval fun i => X (e i)).toLinearMap) ((generize fun x => m (e x)) 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 i)).toLinearMap)
    (f.toFun (MvPolynomial ι R) (∑ i : ι, X i ⊗ₜ[R] m (e i))) =
  f.toFun (MvPolynomial κ R)
    ((LinearMap.rTensor M (aeval fun i => X (e i)).toLinearMap) (∑ i : ι, X i ⊗ₜ[R] m (e i))) :=
  isCompat_apply f (aeval fun i => X (e i)) (∑ i : ι, X i ⊗ₜ[R] m (e i))
⊢ (generize m) f = (LinearMap.rTensor N (aeval fun i => X (e i)).toLinearMap) ((generize fun x => m (e x)) 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 i)).toLinearMap) (f.toFun (MvPolynomial ι R) (∑ i : ι, X i ⊗ₜ[R] m (e i))) =
    f.toFun (MvPolynomial κ R) (∑ x : ι, X (e x) ⊗ₜ[R] m (e x))
⊢ (generize m) f = (LinearMap.rTensor N (aeval fun i => X (e i)).toLinearMap) ((generize fun x => m (e x)) 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 i)).toLinearMap) (f.toFun (MvPolynomial ι R) (∑ i : ι, X i ⊗ₜ[R] m (e i))) =
    f.toFun (MvPolynomial κ R) (∑ x : ι, X (e x) ⊗ₜ[R] m (e x))
⊢ (generize m) f = (LinearMap.rTensor N (aeval fun i => X (e i)).toLinearMap) ((generize fun x => m (e x)) f)
Tactic:
simp only [generize, coe_mk, AddHom.coe_mk, comp_apply, 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 i)).toLinearMap) (f.toFun (MvPolynomial ι R) (∑ i : ι, X i ⊗ₜ[R] m (e i))) =
    f.toFun (MvPolynomial κ R) (∑ x : ι, X (e x) ⊗ₜ[R] m (e x))
⊢ f.toFun (MvPolynomial κ R) (∑ i : κ, X i ⊗ₜ[R] m i) = f.toFun (MvPolynomial κ R) (∑ x : ι, X (e x) ⊗ₜ[R] m (e 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 i)).toLinearMap) (f.toFun (MvPolynomial ι R) (∑ i : ι, X i ⊗ₜ[R] m (e i))) =
    f.toFun (MvPolynomial κ R) (∑ x : ι, X (e x) ⊗ₜ[R] m (e x))
⊢ f.toFun (MvPolynomial κ R) (∑ i : κ, X i ⊗ₜ[R] m i) = f.toFun (MvPolynomial κ R) (∑ x : ι, X (e x) ⊗ₜ[R] m (e 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 i)).toLinearMap) (f.toFun (MvPolynomial ι R) (∑ i : ι, X i ⊗ₜ[R] m (e i))) =
    f.toFun (MvPolynomial κ R) (∑ x : ι, X (e x) ⊗ₜ[R] m (e x))
⊢ ∑ i : κ, X i ⊗ₜ[R] m i = ∑ x : ι, X (e x) ⊗ₜ[R] m (e 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 i)).toLinearMap) (f.toFun (MvPolynomial ι R) (∑ i : ι, X i ⊗ₜ[R] m (e i))) =
    f.toFun (MvPolynomial κ R) (∑ x : ι, X (e x) ⊗ₜ[R] m (e x))
⊢ ∑ i : κ, X i ⊗ₜ[R] m i = ∑ x : ι, X (e x) ⊗ₜ[R] m (e 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 i)).toLinearMap) (f.toFun (MvPolynomial ι R) (∑ i : ι, X i ⊗ₜ[R] m (e i))) =
    f.toFun (MvPolynomial κ R) (∑ x : ι, X (e x) ⊗ₜ[R] m (e x))
⊢ ∑ i : κ, X i ⊗ₜ[R] m i = ∑ x : κ, ((fun x => X (e x) ⊗ₜ[R] m (e x)) ∘ ⇑e.symm) 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 i)).toLinearMap) (f.toFun (MvPolynomial ι R) (∑ i : ι, X i ⊗ₜ[R] m (e i))) =
    f.toFun (MvPolynomial κ R) (∑ x : ι, X (e x) ⊗ₜ[R] m (e x))
⊢ ∑ i : κ, X i ⊗ₜ[R] m i = ∑ x : κ, ((fun x => X (e x) ⊗ₜ[R] m (e x)) ∘ ⇑e.symm) 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 i)).toLinearMap) (f.toFun (MvPolynomial ι R) (∑ i : ι, X i ⊗ₜ[R] m (e i))) =
    f.toFun (MvPolynomial κ R) (∑ x : ι, X (e x) ⊗ₜ[R] m (e x))
k : κ
x✝ : k ∈ univ
⊢ X k ⊗ₜ[R] m k = ((fun x => X (e x) ⊗ₜ[R] m (e x)) ∘ ⇑e.symm) k
Tactic:
rw [Function.comp_apply, Equiv.apply_symm_apply]
State after:
no goals