case h.a
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_4
a a' a₁ a₂ : R
e✝ : ℕ
s : σ →₀ ℕ
inst✝⁶ : CommSemiring R
A₁ : Type u_1
A₂ : Type u_2
A₃ : Type u_3
inst✝⁵ : CommSemiring A₁
inst✝⁴ : CommSemiring A₂
inst✝³ : CommSemiring A₃
inst✝² : Algebra R A₁
inst✝¹ : Algebra R A₂
inst✝ : Algebra R A₃
e : A₁ ≃ₐ[R] A₂
f : A₂ ≃ₐ[R] A₃
a✝ : MvPolynomial σ A₁
m✝ : σ →₀ ℕ
⊢ coeff m✝ (↑(AlgEquiv.trans (mapAlgEquiv σ e) (mapAlgEquiv σ f)) a✝) =
    coeff m✝ (↑(mapAlgEquiv σ (AlgEquiv.trans e f)) a✝)
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_4
a a' a₁ a₂ : R
e✝ : ℕ
s : σ →₀ ℕ
inst✝⁶ : CommSemiring R
A₁ : Type u_1
A₂ : Type u_2
A₃ : Type u_3
inst✝⁵ : CommSemiring A₁
inst✝⁴ : CommSemiring A₂
inst✝³ : CommSemiring A₃
inst✝² : Algebra R A₁
inst✝¹ : Algebra R A₂
inst✝ : Algebra R A₃
e : A₁ ≃ₐ[R] A₂
f : A₂ ≃ₐ[R] A₃
⊢ AlgEquiv.trans (mapAlgEquiv σ e) (mapAlgEquiv σ f) = mapAlgEquiv σ (AlgEquiv.trans e f)
ext
case h.a
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_4
a a' a₁ a₂ : R
e✝ : ℕ
s : σ →₀ ℕ
inst✝⁶ : CommSemiring R
A₁ : Type u_1
A₂ : Type u_2
A₃ : Type u_3
inst✝⁵ : CommSemiring A₁
inst✝⁴ : CommSemiring A₂
inst✝³ : CommSemiring A₃
inst✝² : Algebra R A₁
inst✝¹ : Algebra R A₂
inst✝ : Algebra R A₃
e : A₁ ≃ₐ[R] A₂
f : A₂ ≃ₐ[R] A₃
a✝ : MvPolynomial σ A₁
m✝ : σ →₀ ℕ
⊢ coeff m✝ (↑(map (RingHom.comp ↑f ↑e)) a✝) = coeff m✝ (↑(map ↑(AlgEquiv.trans e f)) a✝)
case h.a
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_4
a a' a₁ a₂ : R
e✝ : ℕ
s : σ →₀ ℕ
inst✝⁶ : CommSemiring R
A₁ : Type u_1
A₂ : Type u_2
A₃ : Type u_3
inst✝⁵ : CommSemiring A₁
inst✝⁴ : CommSemiring A₂
inst✝³ : CommSemiring A₃
inst✝² : Algebra R A₁
inst✝¹ : Algebra R A₂
inst✝ : Algebra R A₃
e : A₁ ≃ₐ[R] A₂
f : A₂ ≃ₐ[R] A₃
a✝ : MvPolynomial σ A₁
m✝ : σ →₀ ℕ
⊢ coeff m✝ (↑(AlgEquiv.trans (mapAlgEquiv σ e) (mapAlgEquiv σ f)) a✝) =
    coeff m✝ (↑(mapAlgEquiv σ (AlgEquiv.trans e f)) a✝)
simp only [AlgEquiv.trans_apply, mapAlgEquiv_apply, map_map]
no goals
case h.a
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_4
a a' a₁ a₂ : R
e✝ : ℕ
s : σ →₀ ℕ
inst✝⁶ : CommSemiring R
A₁ : Type u_1
A₂ : Type u_2
A₃ : Type u_3
inst✝⁵ : CommSemiring A₁
inst✝⁴ : CommSemiring A₂
inst✝³ : CommSemiring A₃
inst✝² : Algebra R A₁
inst✝¹ : Algebra R A₂
inst✝ : Algebra R A₃
e : A₁ ≃ₐ[R] A₂
f : A₂ ≃ₐ[R] A₃
a✝ : MvPolynomial σ A₁
m✝ : σ →₀ ℕ
⊢ coeff m✝ (↑(map (RingHom.comp ↑f ↑e)) a✝) = coeff m✝ (↑(map ↑(AlgEquiv.trans e f)) a✝)
rfl