Theorem: PolynomialMap.coeff_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✝¹ : DecidableEq κ
inst✝ : Fintype κ
e : ι ≃ κ
m : κ → M
k : κ →₀ ℕ
f : M →ₚ[R] N
⊢ ((coeff m) f) k = ((coeff (m ∘ ⇑e)) f) (Finsupp.equivMapDomain e.symm k)
Tactic:
rw [coeff_comp_equiv]
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✝¹ : DecidableEq κ
inst✝ : Fintype κ
e : ι ≃ κ
m : κ → M
k : κ →₀ ℕ
f : M →ₚ[R] N
⊢ ((coeff m) f) k = ((coeff ((m ∘ ⇑e) ∘ ⇑e.symm)) f) k

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✝¹ : DecidableEq κ
inst✝ : Fintype κ
e : ι ≃ κ
m : κ → M
k : κ →₀ ℕ
f : M →ₚ[R] N
⊢ ((coeff m) f) k = ((coeff ((m ∘ ⇑e) ∘ ⇑e.symm)) f) k
Tactic:
congr
State after:
case e_a.e_a.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 ι
κ : Type u_1
inst✝¹ : DecidableEq κ
inst✝ : Fintype κ
e : ι ≃ κ
m : κ → M
k : κ →₀ ℕ
f : M →ₚ[R] N
⊢ m = (m ∘ ⇑e) ∘ ⇑e.symm

State before:
case e_a.e_a.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 ι
κ : Type u_1
inst✝¹ : DecidableEq κ
inst✝ : Fintype κ
e : ι ≃ κ
m : κ → M
k : κ →₀ ℕ
f : M →ₚ[R] N
⊢ m = (m ∘ ⇑e) ∘ ⇑e.symm
Tactic:
ext k
State after:
case e_a.e_a.e_m.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✝¹ : DecidableEq κ
inst✝ : Fintype κ
e : ι ≃ κ
m : κ → M
k✝ : κ →₀ ℕ
f : M →ₚ[R] N
k : κ
⊢ m k = ((m ∘ ⇑e) ∘ ⇑e.symm) k

State before:
case e_a.e_a.e_m.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✝¹ : DecidableEq κ
inst✝ : Fintype κ
e : ι ≃ κ
m : κ → M
k✝ : κ →₀ ℕ
f : M →ₚ[R] N
k : κ
⊢ m k = ((m ∘ ⇑e) ∘ ⇑e.symm) k
Tactic:
simp only [Function.comp_apply, Equiv.apply_symm_apply]
State after:
no goals