case mk'.intro
p : ℕ
R S : Type u
σ : Type ?u.597461
idx : Type ?u.597464
inst✝¹ : CommRing R
inst✝ : CommRing S
g : ⦃R : Type u_1⦄ → [inst : CommRing R] → 𝕎 R → 𝕎 R
f : ⦃R : Type u_1⦄ → [inst : CommRing R] → 𝕎 R → 𝕎 R → 𝕎 R
hg : IsPoly p g
φ : ℕ → MvPolynomial (Fin 2 × ℕ) ℤ
hf : ∀ ⦃R : Type u_1⦄ [inst : CommRing R] (x y : 𝕎 R), (f x y).coeff = fun n => peval (φ n) ![x.coeff, y.coeff]
⊢ IsPoly₂ p fun R _Rcr x y => g (f x y)
p : ℕ
R S : Type u
σ : Type ?u.597461
idx : Type ?u.597464
inst✝¹ : CommRing R
inst✝ : CommRing S
g : ⦃R : Type u_1⦄ → [inst : CommRing R] → 𝕎 R → 𝕎 R
f : ⦃R : Type u_1⦄ → [inst : CommRing R] → 𝕎 R → 𝕎 R → 𝕎 R
hg : IsPoly p g
hf : IsPoly₂ p f
⊢ IsPoly₂ p fun R _Rcr x y => g (f x y)
obtain ⟨φ, hf⟩ := hf
case mk'.intro.mk'.intro
p : ℕ
R S : Type u
σ : Type ?u.597461
idx : Type ?u.597464
inst✝¹ : CommRing R
inst✝ : CommRing S
g : ⦃R : Type u_1⦄ → [inst : CommRing R] → 𝕎 R → 𝕎 R
f : ⦃R : Type u_1⦄ → [inst : CommRing R] → 𝕎 R → 𝕎 R → 𝕎 R
φ : ℕ → MvPolynomial (Fin 2 × ℕ) ℤ
hf : ∀ ⦃R : Type u_1⦄ [inst : CommRing R] (x y : 𝕎 R), (f x y).coeff = fun n => peval (φ n) ![x.coeff, y.coeff]
ψ : ℕ → 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 x y => g (f x y)
case mk'.intro
p : ℕ
R S : Type u
σ : Type ?u.597461
idx : Type ?u.597464
inst✝¹ : CommRing R
inst✝ : CommRing S
g : ⦃R : Type u_1⦄ → [inst : CommRing R] → 𝕎 R → 𝕎 R
f : ⦃R : Type u_1⦄ → [inst : CommRing R] → 𝕎 R → 𝕎 R → 𝕎 R
hg : IsPoly p g
φ : ℕ → MvPolynomial (Fin 2 × ℕ) ℤ
hf : ∀ ⦃R : Type u_1⦄ [inst : CommRing R] (x y : 𝕎 R), (f x y).coeff = fun n => peval (φ n) ![x.coeff, y.coeff]
⊢ IsPoly₂ p fun R _Rcr x y => g (f x y)
obtain ⟨ψ, hg⟩ := hg
case mk'.intro.mk'.intro
p : ℕ
R S : Type u
σ : Type ?u.597461
idx : Type ?u.597464
inst✝¹ : CommRing R
inst✝ : CommRing S
g : ⦃R : Type u_1⦄ → [inst : CommRing R] → 𝕎 R → 𝕎 R
f : ⦃R : Type u_1⦄ → [inst : CommRing R] → 𝕎 R → 𝕎 R → 𝕎 R
φ : ℕ → MvPolynomial (Fin 2 × ℕ) ℤ
hf : ∀ ⦃R : Type u_1⦄ [inst : CommRing R] (x y : 𝕎 R), (f x y).coeff = fun n => peval (φ n) ![x.coeff, y.coeff]
ψ : ℕ → 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 y : 𝕎 R),
    (g (f x y)).coeff = fun n => peval ((fun n => ↑(bind₁ φ) (ψ n)) n) ![x.coeff, y.coeff]
case mk'.intro.mk'.intro
p : ℕ
R S : Type u
σ : Type ?u.597461
idx : Type ?u.597464
inst✝¹ : CommRing R
inst✝ : CommRing S
g : ⦃R : Type u_1⦄ → [inst : CommRing R] → 𝕎 R → 𝕎 R
f : ⦃R : Type u_1⦄ → [inst : CommRing R] → 𝕎 R → 𝕎 R → 𝕎 R
φ : ℕ → MvPolynomial (Fin 2 × ℕ) ℤ
hf : ∀ ⦃R : Type u_1⦄ [inst : CommRing R] (x y : 𝕎 R), (f x y).coeff = fun n => peval (φ n) ![x.coeff, y.coeff]
ψ : ℕ → 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 x y => g (f x y)
use fun n => bind₁ φ (ψ n)
case mk'.intro.mk'.intro
p : ℕ
R S : Type u
σ : Type ?u.597461
idx : Type ?u.597464
inst✝² : CommRing R
inst✝¹ : CommRing S
g : ⦃R : Type u_1⦄ → [inst : CommRing R] → 𝕎 R → 𝕎 R
f : ⦃R : Type u_1⦄ → [inst : CommRing R] → 𝕎 R → 𝕎 R → 𝕎 R
φ : ℕ → MvPolynomial (Fin 2 × ℕ) ℤ
hf : ∀ ⦃R : Type u_1⦄ [inst : CommRing R] (x y : 𝕎 R), (f x y).coeff = fun n => peval (φ n) ![x.coeff, y.coeff]
ψ : ℕ → 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✝ y✝ : 𝕎 R✝
⊢ (g (f x✝ y✝)).coeff = fun n => peval ((fun n => ↑(bind₁ φ) (ψ n)) n) ![x✝.coeff, y✝.coeff]
case mk'.intro.mk'.intro
p : ℕ
R S : Type u
σ : Type ?u.597461
idx : Type ?u.597464
inst✝¹ : CommRing R
inst✝ : CommRing S
g : ⦃R : Type u_1⦄ → [inst : CommRing R] → 𝕎 R → 𝕎 R
f : ⦃R : Type u_1⦄ → [inst : CommRing R] → 𝕎 R → 𝕎 R → 𝕎 R
φ : ℕ → MvPolynomial (Fin 2 × ℕ) ℤ
hf : ∀ ⦃R : Type u_1⦄ [inst : CommRing R] (x y : 𝕎 R), (f x y).coeff = fun n => peval (φ n) ![x.coeff, y.coeff]
ψ : ℕ → 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 y : 𝕎 R),
    (g (f x y)).coeff = fun n => peval ((fun n => ↑(bind₁ φ) (ψ n)) n) ![x.coeff, y.coeff]
intros
no goals
case mk'.intro.mk'.intro
p : ℕ
R S : Type u
σ : Type ?u.597461
idx : Type ?u.597464
inst✝² : CommRing R
inst✝¹ : CommRing S
g : ⦃R : Type u_1⦄ → [inst : CommRing R] → 𝕎 R → 𝕎 R
f : ⦃R : Type u_1⦄ → [inst : CommRing R] → 𝕎 R → 𝕎 R → 𝕎 R
φ : ℕ → MvPolynomial (Fin 2 × ℕ) ℤ
hf : ∀ ⦃R : Type u_1⦄ [inst : CommRing R] (x y : 𝕎 R), (f x y).coeff = fun n => peval (φ n) ![x.coeff, y.coeff]
ψ : ℕ → 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✝ y✝ : 𝕎 R✝
⊢ (g (f x✝ y✝)).coeff = fun n => peval ((fun n => ↑(bind₁ φ) (ψ n)) n) ![x✝.coeff, y✝.coeff]
simp only [peval, aeval_bind₁, Function.comp, hg, hf]