case mk'.intro
p : ℕ
R S : Type u
σ : Type ?u.528965
idx : Type ?u.528968
inst✝¹ : CommRing R
inst✝ : CommRing S
g f : ⦃R : Type u_1⦄ → [inst : CommRing R] → 𝕎 R → 𝕎 R
hg : IsPoly p g
φ : ℕ → MvPolynomial ℕ ℤ
hf : ∀ ⦃R : Type u_1⦄ [inst : CommRing R] (x : 𝕎 R), (f x).coeff = fun n => ↑(aeval x.coeff) (φ n)
⊢ IsPoly p fun R _Rcr => g ∘ f
p : ℕ
R S : Type u
σ : Type ?u.528965
idx : Type ?u.528968
inst✝¹ : CommRing R
inst✝ : CommRing S
g f : ⦃R : Type u_1⦄ → [inst : CommRing R] → 𝕎 R → 𝕎 R
hg : IsPoly p g
hf : IsPoly p f
⊢ IsPoly p fun R _Rcr => g ∘ f
obtain ⟨φ, hf⟩ := hf
case mk'.intro.mk'.intro
p : ℕ
R S : Type u
σ : Type ?u.528965
idx : Type ?u.528968
inst✝¹ : CommRing R
inst✝ : CommRing S
g f : ⦃R : Type u_1⦄ → [inst : CommRing R] → 𝕎 R → 𝕎 R
φ : ℕ → MvPolynomial ℕ ℤ
hf : ∀ ⦃R : Type u_1⦄ [inst : CommRing R] (x : 𝕎 R), (f x).coeff = fun n => ↑(aeval x.coeff) (φ n)
ψ : ℕ → MvPolynomial ℕ ℤ
hg : ∀ ⦃R : Type u_1⦄ [inst : CommRing R] (x : 𝕎 R), (g x).coeff = fun n => ↑(aeval x.coeff) (ψ n)
⊢ IsPoly p fun R _Rcr => g ∘ f
case mk'.intro
p : ℕ
R S : Type u
σ : Type ?u.528965
idx : Type ?u.528968
inst✝¹ : CommRing R
inst✝ : CommRing S
g f : ⦃R : Type u_1⦄ → [inst : CommRing R] → 𝕎 R → 𝕎 R
hg : IsPoly p g
φ : ℕ → MvPolynomial ℕ ℤ
hf : ∀ ⦃R : Type u_1⦄ [inst : CommRing R] (x : 𝕎 R), (f x).coeff = fun n => ↑(aeval x.coeff) (φ n)
⊢ IsPoly p fun R _Rcr => g ∘ f
obtain ⟨ψ, hg⟩ := hg
case mk'.intro.mk'.intro
p : ℕ
R S : Type u
σ : Type ?u.528965
idx : Type ?u.528968
inst✝¹ : CommRing R
inst✝ : CommRing S
g f : ⦃R : Type u_1⦄ → [inst : CommRing R] → 𝕎 R → 𝕎 R
φ : ℕ → MvPolynomial ℕ ℤ
hf : ∀ ⦃R : Type u_1⦄ [inst : CommRing R] (x : 𝕎 R), (f x).coeff = fun n => ↑(aeval x.coeff) (φ n)
ψ : ℕ → MvPolynomial ℕ ℤ
hg : ∀ ⦃R : Type u_1⦄ [inst : CommRing R] (x : 𝕎 R), (g x).coeff = fun n => ↑(aeval x.coeff) (ψ n)
⊢ ∀ ⦃R : Type u_1⦄ [inst : CommRing R] (x : 𝕎 R),
    ((g ∘ f) x).coeff = fun n => ↑(aeval x.coeff) ((fun n => ↑(bind₁ φ) (ψ n)) n)
case mk'.intro.mk'.intro
p : ℕ
R S : Type u
σ : Type ?u.528965
idx : Type ?u.528968
inst✝¹ : CommRing R
inst✝ : CommRing S
g f : ⦃R : Type u_1⦄ → [inst : CommRing R] → 𝕎 R → 𝕎 R
φ : ℕ → MvPolynomial ℕ ℤ
hf : ∀ ⦃R : Type u_1⦄ [inst : CommRing R] (x : 𝕎 R), (f x).coeff = fun n => ↑(aeval x.coeff) (φ n)
ψ : ℕ → MvPolynomial ℕ ℤ
hg : ∀ ⦃R : Type u_1⦄ [inst : CommRing R] (x : 𝕎 R), (g x).coeff = fun n => ↑(aeval x.coeff) (ψ n)
⊢ IsPoly p fun R _Rcr => g ∘ f
use fun n => bind₁ φ (ψ n)
case mk'.intro.mk'.intro
p : ℕ
R S : Type u
σ : Type ?u.528965
idx : Type ?u.528968
inst✝² : CommRing R
inst✝¹ : CommRing S
g f : ⦃R : Type u_1⦄ → [inst : CommRing R] → 𝕎 R → 𝕎 R
φ : ℕ → MvPolynomial ℕ ℤ
hf : ∀ ⦃R : Type u_1⦄ [inst : CommRing R] (x : 𝕎 R), (f x).coeff = fun n => ↑(aeval x.coeff) (φ n)
ψ : ℕ → MvPolynomial ℕ ℤ
hg : ∀ ⦃R : Type u_1⦄ [inst : CommRing R] (x : 𝕎 R), (g x).coeff = fun n => ↑(aeval x.coeff) (ψ n)
R✝ : Type u_1
inst✝ : CommRing R✝
x✝ : 𝕎 R✝
⊢ ((g ∘ f) x✝).coeff = fun n => ↑(aeval x✝.coeff) ((fun n => ↑(bind₁ φ) (ψ n)) n)
case mk'.intro.mk'.intro
p : ℕ
R S : Type u
σ : Type ?u.528965
idx : Type ?u.528968
inst✝¹ : CommRing R
inst✝ : CommRing S
g f : ⦃R : Type u_1⦄ → [inst : CommRing R] → 𝕎 R → 𝕎 R
φ : ℕ → MvPolynomial ℕ ℤ
hf : ∀ ⦃R : Type u_1⦄ [inst : CommRing R] (x : 𝕎 R), (f x).coeff = fun n => ↑(aeval x.coeff) (φ n)
ψ : ℕ → MvPolynomial ℕ ℤ
hg : ∀ ⦃R : Type u_1⦄ [inst : CommRing R] (x : 𝕎 R), (g x).coeff = fun n => ↑(aeval x.coeff) (ψ n)
⊢ ∀ ⦃R : Type u_1⦄ [inst : CommRing R] (x : 𝕎 R),
    ((g ∘ f) x).coeff = fun n => ↑(aeval x.coeff) ((fun n => ↑(bind₁ φ) (ψ n)) n)
intros
no goals
case mk'.intro.mk'.intro
p : ℕ
R S : Type u
σ : Type ?u.528965
idx : Type ?u.528968
inst✝² : CommRing R
inst✝¹ : CommRing S
g f : ⦃R : Type u_1⦄ → [inst : CommRing R] → 𝕎 R → 𝕎 R
φ : ℕ → MvPolynomial ℕ ℤ
hf : ∀ ⦃R : Type u_1⦄ [inst : CommRing R] (x : 𝕎 R), (f x).coeff = fun n => ↑(aeval x.coeff) (φ n)
ψ : ℕ → MvPolynomial ℕ ℤ
hg : ∀ ⦃R : Type u_1⦄ [inst : CommRing R] (x : 𝕎 R), (g x).coeff = fun n => ↑(aeval x.coeff) (ψ n)
R✝ : Type u_1
inst✝ : CommRing R✝
x✝ : 𝕎 R✝
⊢ ((g ∘ f) x✝).coeff = fun n => ↑(aeval x✝.coeff) ((fun n => ↑(bind₁ φ) (ψ n)) n)
simp only [aeval_bind₁, Function.comp, hg, hf]