[GOAL]
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
T : Type u_5
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : CommSemiring T
⊢ bind₁ X = AlgHom.id R (MvPolynomial σ R)
[PROOFSTEP]
ext1 i
[GOAL]
case hf
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
T : Type u_5
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : CommSemiring T
i : σ
⊢ ↑(bind₁ X) (X i) = ↑(AlgHom.id R (MvPolynomial σ R)) (X i)
[PROOFSTEP]
simp
[GOAL]
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
T : Type u_5
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : CommSemiring T
f✝ f : σ → MvPolynomial τ R
x : R
⊢ ↑(bind₁ f) (↑C x) = ↑C x
[PROOFSTEP]
simp [bind₁, algebraMap_eq]
[GOAL]
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
T : Type u_5
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : CommSemiring T
f : σ → MvPolynomial τ R
⊢ bind₂ C = RingHom.id (MvPolynomial σ R)
[PROOFSTEP]
ext : 2
[GOAL]
case hC.a
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
T : Type u_5
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : CommSemiring T
f : σ → MvPolynomial τ R
x✝ : R
⊢ ↑(RingHom.comp (bind₂ C) C) x✝ = ↑(RingHom.comp (RingHom.id (MvPolynomial σ R)) C) x✝
[PROOFSTEP]
simp
[GOAL]
case hX.a
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
T : Type u_5
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : CommSemiring T
f : σ → MvPolynomial τ R
i✝ : σ
m✝ : σ →₀ ℕ
⊢ coeff m✝ (↑(bind₂ C) (X i✝)) = coeff m✝ (↑(RingHom.id (MvPolynomial σ R)) (X i✝))
[PROOFSTEP]
simp
[GOAL]
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
T : Type u_5
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : CommSemiring T
f✝ : σ → MvPolynomial τ R
f : R →+* MvPolynomial σ S
φ : MvPolynomial σ R
⊢ ↑join₂ (↑(map f) φ) = ↑(bind₂ f) φ
[PROOFSTEP]
simp only [join₂, bind₂, eval₂Hom_map_hom, RingHom.id_comp]
[GOAL]
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
T : Type u_5
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : CommSemiring T
f✝ f : σ → MvPolynomial τ R
p : MvPolynomial σ R
⊢ ↑(aeval id) (↑(rename f) p) = ↑(aeval f) p
[PROOFSTEP]
rw [aeval_rename, Function.comp.left_id]
[GOAL]
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
T : Type u_5
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : CommSemiring T
f✝ : σ → MvPolynomial τ R
υ : Type u_6
f : σ → MvPolynomial τ R
g : τ → MvPolynomial υ R
φ : MvPolynomial σ R
⊢ ↑(bind₁ g) (↑(bind₁ f) φ) = ↑(bind₁ fun i => ↑(bind₁ g) (f i)) φ
[PROOFSTEP]
simp [bind₁, ← comp_aeval]
[GOAL]
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
T : Type u_5
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : CommSemiring T
f✝ : σ → MvPolynomial τ R
υ : Type u_6
f : σ → MvPolynomial τ R
g : τ → MvPolynomial υ R
⊢ AlgHom.comp (bind₁ g) (bind₁ f) = bind₁ fun i => ↑(bind₁ g) (f i)
[PROOFSTEP]
ext1
[GOAL]
case hf
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
T : Type u_5
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : CommSemiring T
f✝ : σ → MvPolynomial τ R
υ : Type u_6
f : σ → MvPolynomial τ R
g : τ → MvPolynomial υ R
i✝ : σ
⊢ ↑(AlgHom.comp (bind₁ g) (bind₁ f)) (X i✝) = ↑(bind₁ fun i => ↑(bind₁ g) (f i)) (X i✝)
[PROOFSTEP]
apply bind₁_bind₁
[GOAL]
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
T : Type u_5
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : CommSemiring T
f✝ : σ → MvPolynomial τ R
f : R →+* MvPolynomial σ S
g : S →+* MvPolynomial σ T
⊢ RingHom.comp (bind₂ g) (bind₂ f) = bind₂ (RingHom.comp (bind₂ g) f)
[PROOFSTEP]
ext : 2
[GOAL]
case hC.a
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
T : Type u_5
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : CommSemiring T
f✝ : σ → MvPolynomial τ R
f : R →+* MvPolynomial σ S
g : S →+* MvPolynomial σ T
x✝ : R
⊢ ↑(RingHom.comp (RingHom.comp (bind₂ g) (bind₂ f)) C) x✝ = ↑(RingHom.comp (bind₂ (RingHom.comp (bind₂ g) f)) C) x✝
[PROOFSTEP]
simp
[GOAL]
case hX.a
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
T : Type u_5
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : CommSemiring T
f✝ : σ → MvPolynomial τ R
f : R →+* MvPolynomial σ S
g : S →+* MvPolynomial σ T
i✝ : σ
m✝ : σ →₀ ℕ
⊢ coeff m✝ (↑(RingHom.comp (bind₂ g) (bind₂ f)) (X i✝)) = coeff m✝ (↑(bind₂ (RingHom.comp (bind₂ g) f)) (X i✝))
[PROOFSTEP]
simp
[GOAL]
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
T : Type u_5
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : CommSemiring T
f✝ : σ → MvPolynomial τ R
υ : Type u_6
f : σ → MvPolynomial τ R
g : τ → υ
⊢ AlgHom.comp (rename g) (bind₁ f) = bind₁ fun i => ↑(rename g) (f i)
[PROOFSTEP]
ext1 i
[GOAL]
case hf
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
T : Type u_5
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : CommSemiring T
f✝ : σ → MvPolynomial τ R
υ : Type u_6
f : σ → MvPolynomial τ R
g : τ → υ
i : σ
⊢ ↑(AlgHom.comp (rename g) (bind₁ f)) (X i) = ↑(bind₁ fun i => ↑(rename g) (f i)) (X i)
[PROOFSTEP]
simp
[GOAL]
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
T : Type u_5
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : CommSemiring T
f✝ : σ → MvPolynomial τ R
f : R →+* MvPolynomial σ S
g : S →+* T
φ : MvPolynomial σ R
⊢ ↑(map g) (↑(bind₂ f) φ) = ↑(bind₂ (RingHom.comp (map g) f)) φ
[PROOFSTEP]
simp only [bind₂, eval₂_comp_right, coe_eval₂Hom, eval₂_map]
[GOAL]
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
T : Type u_5
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : CommSemiring T
f✝ : σ → MvPolynomial τ R
f : R →+* MvPolynomial σ S
g : S →+* T
φ : MvPolynomial σ R
⊢ eval₂ (RingHom.comp (map g) f) (↑(map g) ∘ X) φ = eval₂ (RingHom.comp (map g) f) X φ
[PROOFSTEP]
congr 1 with : 1
[GOAL]
case e_g.h
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
T : Type u_5
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : CommSemiring T
f✝ : σ → MvPolynomial τ R
f : R →+* MvPolynomial σ S
g : S →+* T
φ : MvPolynomial σ R
x✝ : σ
⊢ (↑(map g) ∘ X) x✝ = X x✝
[PROOFSTEP]
simp only [Function.comp_apply, map_X]
[GOAL]
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
T : Type u_5
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : CommSemiring T
f✝ : σ → MvPolynomial τ R
υ : Type u_6
f : τ → MvPolynomial υ R
g : σ → τ
⊢ AlgHom.comp (bind₁ f) (rename g) = bind₁ (f ∘ g)
[PROOFSTEP]
ext1 i
[GOAL]
case hf
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
T : Type u_5
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : CommSemiring T
f✝ : σ → MvPolynomial τ R
υ : Type u_6
f : τ → MvPolynomial υ R
g : σ → τ
i : σ
⊢ ↑(AlgHom.comp (bind₁ f) (rename g)) (X i) = ↑(bind₁ (f ∘ g)) (X i)
[PROOFSTEP]
simp
[GOAL]
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
T : Type u_5
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : CommSemiring T
f✝ : σ → MvPolynomial τ R
f : S →+* MvPolynomial σ T
g : R →+* S
φ : MvPolynomial σ R
⊢ ↑(bind₂ f) (↑(map g) φ) = ↑(bind₂ (RingHom.comp f g)) φ
[PROOFSTEP]
simp [bind₂]
[GOAL]
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
T : Type u_5
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : CommSemiring T
f✝ : σ → MvPolynomial τ R
f : R →+* S
⊢ RingHom.comp (map f) C = RingHom.comp C f
[PROOFSTEP]
ext1
[GOAL]
case a
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
T : Type u_5
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : CommSemiring T
f✝ : σ → MvPolynomial τ R
f : R →+* S
x✝ : R
⊢ ↑(RingHom.comp (map f) C) x✝ = ↑(RingHom.comp C f) x✝
[PROOFSTEP]
apply map_C
[GOAL]
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
T : Type u_5
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : CommSemiring T
f✝ : σ → MvPolynomial τ R
f : MvPolynomial τ R →+* S
g : σ → MvPolynomial τ R
φ : MvPolynomial σ R
⊢ ↑f (↑(bind₁ g) φ) = ↑(eval₂Hom (RingHom.comp f C) fun i => ↑f (g i)) φ
[PROOFSTEP]
rw [bind₁, map_aeval, algebraMap_eq]
[GOAL]
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
T : Type u_5
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : CommSemiring T
f✝ : σ → MvPolynomial τ R
f : R →+* S
g : σ → MvPolynomial τ R
φ : MvPolynomial σ R
⊢ ↑(map f) (↑(bind₁ g) φ) = ↑(bind₁ fun i => ↑(map f) (g i)) (↑(map f) φ)
[PROOFSTEP]
rw [hom_bind₁, map_comp_C, ← eval₂Hom_map_hom]
[GOAL]
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
T : Type u_5
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : CommSemiring T
f✝ : σ → MvPolynomial τ R
f : R →+* S
g : σ → MvPolynomial τ R
φ : MvPolynomial σ R
⊢ ↑(eval₂Hom C fun i => ↑(map f) (g i)) (↑(map f) φ) = ↑(bind₁ fun i => ↑(map f) (g i)) (↑(map f) φ)
[PROOFSTEP]
rfl
[GOAL]
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
T : Type u_5
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : CommSemiring T
f✝ : σ → MvPolynomial τ R
f : R →+* S
g : σ → S
⊢ RingHom.comp (eval₂Hom f g) C = f
[PROOFSTEP]
ext1 r
[GOAL]
case a
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
T : Type u_5
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : CommSemiring T
f✝ : σ → MvPolynomial τ R
f : R →+* S
g : σ → S
r : R
⊢ ↑(RingHom.comp (eval₂Hom f g) C) r = ↑f r
[PROOFSTEP]
exact eval₂_C f g r
[GOAL]
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
T : Type u_5
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : CommSemiring T
f✝ : σ → MvPolynomial τ R
f : R →+* S
g : τ → S
h : σ → MvPolynomial τ R
φ : MvPolynomial σ R
⊢ ↑(eval₂Hom f g) (↑(bind₁ h) φ) = ↑(eval₂Hom f fun i => ↑(eval₂Hom f g) (h i)) φ
[PROOFSTEP]
rw [hom_bind₁, eval₂Hom_comp_C]
[GOAL]
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
T : Type u_5
inst✝³ : CommSemiring R
inst✝² : CommSemiring S
inst✝¹ : CommSemiring T
f✝ : σ → MvPolynomial τ R
inst✝ : Algebra R S
f : τ → S
g : σ → MvPolynomial τ R
⊢ AlgHom.comp (aeval f) (bind₁ g) = aeval fun i => ↑(aeval f) (g i)
[PROOFSTEP]
ext1
[GOAL]
case hf
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
T : Type u_5
inst✝³ : CommSemiring R
inst✝² : CommSemiring S
inst✝¹ : CommSemiring T
f✝ : σ → MvPolynomial τ R
inst✝ : Algebra R S
f : τ → S
g : σ → MvPolynomial τ R
i✝ : σ
⊢ ↑(AlgHom.comp (aeval f) (bind₁ g)) (X i✝) = ↑(aeval fun i => ↑(aeval f) (g i)) (X i✝)
[PROOFSTEP]
apply aeval_bind₁
[GOAL]
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
T : Type u_5
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : CommSemiring T
f✝ : σ → MvPolynomial τ R
f : S →+* T
g : σ → T
h : R →+* MvPolynomial σ S
⊢ RingHom.comp (eval₂Hom f g) (bind₂ h) = eval₂Hom (RingHom.comp (eval₂Hom f g) h) g
[PROOFSTEP]
ext : 2
[GOAL]
case hC.a
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
T : Type u_5
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : CommSemiring T
f✝ : σ → MvPolynomial τ R
f : S →+* T
g : σ → T
h : R →+* MvPolynomial σ S
x✝ : R
⊢ ↑(RingHom.comp (RingHom.comp (eval₂Hom f g) (bind₂ h)) C) x✝ =
    ↑(RingHom.comp (eval₂Hom (RingHom.comp (eval₂Hom f g) h) g) C) x✝
[PROOFSTEP]
simp
[GOAL]
case hX
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
T : Type u_5
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : CommSemiring T
f✝ : σ → MvPolynomial τ R
f : S →+* T
g : σ → T
h : R →+* MvPolynomial σ S
i✝ : σ
⊢ ↑(RingHom.comp (eval₂Hom f g) (bind₂ h)) (X i✝) = ↑(eval₂Hom (RingHom.comp (eval₂Hom f g) h) g) (X i✝)
[PROOFSTEP]
simp
[GOAL]
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
T : Type u_5
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : CommSemiring T
f✝ f : σ → MvPolynomial τ R
d : σ →₀ ℕ
r : R
⊢ ↑(bind₁ f) (↑(monomial d) r) = ↑C r * ∏ i in d.support, f i ^ ↑d i
[PROOFSTEP]
simp only [monomial_eq, AlgHom.map_mul, bind₁_C_right, Finsupp.prod, AlgHom.map_prod, AlgHom.map_pow, bind₁_X_right]
[GOAL]
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
T : Type u_5
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : CommSemiring T
f✝ : σ → MvPolynomial τ R
f : R →+* MvPolynomial σ S
d : σ →₀ ℕ
r : R
⊢ ↑(bind₂ f) (↑(monomial d) r) = ↑f r * ↑(monomial d) 1
[PROOFSTEP]
simp only [monomial_eq, RingHom.map_mul, bind₂_C_right, Finsupp.prod, map_prod, map_pow, bind₂_X_right, C_1, one_mul]
[GOAL]
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
T : Type u_5
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : CommSemiring T
f✝ : σ → MvPolynomial τ R
f : R →+* MvPolynomial σ S
d : σ →₀ ℕ
⊢ ↑(bind₂ f) (↑(monomial d) 1) = ↑(monomial d) 1
[PROOFSTEP]
rw [bind₂_monomial, f.map_one, one_mul]
[GOAL]
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
T : Type u_5
inst✝³ : CommSemiring R
inst✝² : CommSemiring S
inst✝¹ : CommSemiring T
f✝ : σ → MvPolynomial τ R
inst✝ : DecidableEq τ
f : σ → MvPolynomial τ R
φ : MvPolynomial σ R
⊢ vars (↑(bind₁ f) φ) ⊆ Finset.biUnion (vars φ) fun i => vars (f i)
[PROOFSTEP]
calc
  (bind₁ f φ).vars = (φ.support.sum fun x : σ →₀ ℕ => (bind₁ f) (monomial x (coeff x φ))).vars := by
    rw [← AlgHom.map_sum, ← φ.as_sum]
  _ ≤ φ.support.biUnion fun i : σ →₀ ℕ => ((bind₁ f) (monomial i (coeff i φ))).vars := (vars_sum_subset _ _)
  _ = φ.support.biUnion fun d : σ →₀ ℕ => vars (C (coeff d φ) * ∏ i in d.support, f i ^ d i) := by
    simp only [bind₁_monomial]
  _ ≤ φ.support.biUnion fun d : σ →₀ ℕ => d.support.biUnion fun i => vars (f i) :=
    ?_
      -- proof below
  _ ≤ φ.vars.biUnion fun i : σ => vars (f i) :=
    ?_
      -- proof below
[GOAL]
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
T : Type u_5
inst✝³ : CommSemiring R
inst✝² : CommSemiring S
inst✝¹ : CommSemiring T
f✝ : σ → MvPolynomial τ R
inst✝ : DecidableEq τ
f : σ → MvPolynomial τ R
φ : MvPolynomial σ R
⊢ vars (↑(bind₁ f) φ) = vars (∑ x in support φ, ↑(bind₁ f) (↑(monomial x) (coeff x φ)))
[PROOFSTEP]
rw [← AlgHom.map_sum, ← φ.as_sum]
[GOAL]
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
T : Type u_5
inst✝³ : CommSemiring R
inst✝² : CommSemiring S
inst✝¹ : CommSemiring T
f✝ : σ → MvPolynomial τ R
inst✝ : DecidableEq τ
f : σ → MvPolynomial τ R
φ : MvPolynomial σ R
⊢ (Finset.biUnion (support φ) fun i => vars (↑(bind₁ f) (↑(monomial i) (coeff i φ)))) =
    Finset.biUnion (support φ) fun d => vars (↑C (coeff d φ) * ∏ i in d.support, f i ^ ↑d i)
[PROOFSTEP]
simp only [bind₁_monomial]
[GOAL]
case calc_1
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
T : Type u_5
inst✝³ : CommSemiring R
inst✝² : CommSemiring S
inst✝¹ : CommSemiring T
f✝ : σ → MvPolynomial τ R
inst✝ : DecidableEq τ
f : σ → MvPolynomial τ R
φ : MvPolynomial σ R
⊢ (Finset.biUnion (support φ) fun d => vars (↑C (coeff d φ) * ∏ i in d.support, f i ^ ↑d i)) ≤
    Finset.biUnion (support φ) fun d => Finset.biUnion d.support fun i => vars (f i)
[PROOFSTEP]
apply Finset.biUnion_mono
[GOAL]
case calc_1.h
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
T : Type u_5
inst✝³ : CommSemiring R
inst✝² : CommSemiring S
inst✝¹ : CommSemiring T
f✝ : σ → MvPolynomial τ R
inst✝ : DecidableEq τ
f : σ → MvPolynomial τ R
φ : MvPolynomial σ R
⊢ ∀ (a : σ →₀ ℕ),
    a ∈ support φ → vars (↑C (coeff a φ) * ∏ i in a.support, f i ^ ↑a i) ⊆ Finset.biUnion a.support fun i => vars (f i)
[PROOFSTEP]
intro d _hd
[GOAL]
case calc_1.h
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
T : Type u_5
inst✝³ : CommSemiring R
inst✝² : CommSemiring S
inst✝¹ : CommSemiring T
f✝ : σ → MvPolynomial τ R
inst✝ : DecidableEq τ
f : σ → MvPolynomial τ R
φ : MvPolynomial σ R
d : σ →₀ ℕ
_hd : d ∈ support φ
⊢ vars (↑C (coeff d φ) * ∏ i in d.support, f i ^ ↑d i) ⊆ Finset.biUnion d.support fun i => vars (f i)
[PROOFSTEP]
calc
  vars (C (coeff d φ) * ∏ i : σ in d.support, f i ^ d i) ≤
      (C (coeff d φ)).vars ∪ (∏ i : σ in d.support, f i ^ d i).vars :=
    vars_mul _ _
  _ ≤ (∏ i : σ in d.support, f i ^ d i).vars := by
    simp only [Finset.empty_union, vars_C, Finset.le_iff_subset, Finset.Subset.refl]
  _ ≤ d.support.biUnion fun i : σ => vars (f i ^ d i) := (vars_prod _)
  _ ≤ d.support.biUnion fun i : σ => (f i).vars := ?_
[GOAL]
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
T : Type u_5
inst✝³ : CommSemiring R
inst✝² : CommSemiring S
inst✝¹ : CommSemiring T
f✝ : σ → MvPolynomial τ R
inst✝ : DecidableEq τ
f : σ → MvPolynomial τ R
φ : MvPolynomial σ R
d : σ →₀ ℕ
_hd : d ∈ support φ
⊢ vars (↑C (coeff d φ)) ∪ vars (∏ i in d.support, f i ^ ↑d i) ≤ vars (∏ i in d.support, f i ^ ↑d i)
[PROOFSTEP]
simp only [Finset.empty_union, vars_C, Finset.le_iff_subset, Finset.Subset.refl]
[GOAL]
case calc_1.h
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
T : Type u_5
inst✝³ : CommSemiring R
inst✝² : CommSemiring S
inst✝¹ : CommSemiring T
f✝ : σ → MvPolynomial τ R
inst✝ : DecidableEq τ
f : σ → MvPolynomial τ R
φ : MvPolynomial σ R
d : σ →₀ ℕ
_hd : d ∈ support φ
⊢ (Finset.biUnion d.support fun i => vars (f i ^ ↑d i)) ≤ Finset.biUnion d.support fun i => vars (f i)
[PROOFSTEP]
apply Finset.biUnion_mono
[GOAL]
case calc_1.h.h
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
T : Type u_5
inst✝³ : CommSemiring R
inst✝² : CommSemiring S
inst✝¹ : CommSemiring T
f✝ : σ → MvPolynomial τ R
inst✝ : DecidableEq τ
f : σ → MvPolynomial τ R
φ : MvPolynomial σ R
d : σ →₀ ℕ
_hd : d ∈ support φ
⊢ ∀ (a : σ), a ∈ d.support → vars (f a ^ ↑d a) ⊆ vars (f a)
[PROOFSTEP]
intro i _hi
[GOAL]
case calc_1.h.h
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
T : Type u_5
inst✝³ : CommSemiring R
inst✝² : CommSemiring S
inst✝¹ : CommSemiring T
f✝ : σ → MvPolynomial τ R
inst✝ : DecidableEq τ
f : σ → MvPolynomial τ R
φ : MvPolynomial σ R
d : σ →₀ ℕ
_hd : d ∈ support φ
i : σ
_hi : i ∈ d.support
⊢ vars (f i ^ ↑d i) ⊆ vars (f i)
[PROOFSTEP]
apply vars_pow
[GOAL]
case calc_2
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
T : Type u_5
inst✝³ : CommSemiring R
inst✝² : CommSemiring S
inst✝¹ : CommSemiring T
f✝ : σ → MvPolynomial τ R
inst✝ : DecidableEq τ
f : σ → MvPolynomial τ R
φ : MvPolynomial σ R
⊢ (Finset.biUnion (support φ) fun d => Finset.biUnion d.support fun i => vars (f i)) ≤
    Finset.biUnion (vars φ) fun i => vars (f i)
[PROOFSTEP]
intro j
[GOAL]
case calc_2
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
T : Type u_5
inst✝³ : CommSemiring R
inst✝² : CommSemiring S
inst✝¹ : CommSemiring T
f✝ : σ → MvPolynomial τ R
inst✝ : DecidableEq τ
f : σ → MvPolynomial τ R
φ : MvPolynomial σ R
j : τ
⊢ (j ∈ Finset.biUnion (support φ) fun d => Finset.biUnion d.support fun i => vars (f i)) →
    j ∈ Finset.biUnion (vars φ) fun i => vars (f i)
[PROOFSTEP]
simp_rw [Finset.mem_biUnion]
[GOAL]
case calc_2
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
T : Type u_5
inst✝³ : CommSemiring R
inst✝² : CommSemiring S
inst✝¹ : CommSemiring T
f✝ : σ → MvPolynomial τ R
inst✝ : DecidableEq τ
f : σ → MvPolynomial τ R
φ : MvPolynomial σ R
j : τ
⊢ (∃ a, a ∈ support φ ∧ ∃ a_1, a_1 ∈ a.support ∧ j ∈ vars (f a_1)) → ∃ a, a ∈ vars φ ∧ j ∈ vars (f a)
[PROOFSTEP]
rintro ⟨d, hd, ⟨i, hi, hj⟩⟩
[GOAL]
case calc_2.intro.intro.intro.intro
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
T : Type u_5
inst✝³ : CommSemiring R
inst✝² : CommSemiring S
inst✝¹ : CommSemiring T
f✝ : σ → MvPolynomial τ R
inst✝ : DecidableEq τ
f : σ → MvPolynomial τ R
φ : MvPolynomial σ R
j : τ
d : σ →₀ ℕ
hd : d ∈ support φ
i : σ
hi : i ∈ d.support
hj : j ∈ vars (f i)
⊢ ∃ a, a ∈ vars φ ∧ j ∈ vars (f a)
[PROOFSTEP]
exact ⟨i, (mem_vars _).mpr ⟨d, hd, hi⟩, hj⟩
[GOAL]
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
T : Type u_5
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : CommSemiring T
f✝ f : σ → MvPolynomial τ R
φ : MvPolynomial σ R
j : τ
h : j ∈ vars (↑(bind₁ f) φ)
⊢ ∃ i, i ∈ vars φ ∧ j ∈ vars (f i)
[PROOFSTEP]
classical simpa only [exists_prop, Finset.mem_biUnion, mem_support_iff, Ne.def] using vars_bind₁ f φ h
[GOAL]
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
T : Type u_5
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : CommSemiring T
f✝ f : σ → MvPolynomial τ R
φ : MvPolynomial σ R
j : τ
h : j ∈ vars (↑(bind₁ f) φ)
⊢ ∃ i, i ∈ vars φ ∧ j ∈ vars (f i)
[PROOFSTEP]
simpa only [exists_prop, Finset.mem_biUnion, mem_support_iff, Ne.def] using vars_bind₁ f φ h
[GOAL]
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
T : Type u_5
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : CommSemiring T
f : σ → MvPolynomial τ R
⊢ ∀ {α β : Type ?u.1605153}, Functor.mapConst = Functor.map ∘ Function.const β
[PROOFSTEP]
intros
[GOAL]
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
T : Type u_5
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : CommSemiring T
f : σ → MvPolynomial τ R
α✝ β✝ : Type ?u.1605153
⊢ Functor.mapConst = Functor.map ∘ Function.const β✝
[PROOFSTEP]
rfl
  -- porting note: I guess `map_const` no longer has a default implementation?
[GOAL]
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
T : Type u_5
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : CommSemiring T
f : σ → MvPolynomial τ R
⊢ ∀ {α : Type ?u.1605153} (x : MvPolynomial α R), id <$> x = x
[PROOFSTEP]
intros
[GOAL]
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
T : Type u_5
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : CommSemiring T
f : σ → MvPolynomial τ R
α✝ : Type ?u.1605153
x✝ : MvPolynomial α✝ R
⊢ id <$> x✝ = x✝
[PROOFSTEP]
simp [(· <$> ·)]
[GOAL]
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
T : Type u_5
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : CommSemiring T
f : σ → MvPolynomial τ R
⊢ ∀ {α β γ : Type ?u.1605153} (g : α → β) (h : β → γ) (x : MvPolynomial α R), (h ∘ g) <$> x = h <$> g <$> x
[PROOFSTEP]
intros
[GOAL]
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
T : Type u_5
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : CommSemiring T
f : σ → MvPolynomial τ R
α✝ β✝ γ✝ : Type ?u.1605153
g✝ : α✝ → β✝
h✝ : β✝ → γ✝
x✝ : MvPolynomial α✝ R
⊢ (h✝ ∘ g✝) <$> x✝ = h✝ <$> g✝ <$> x✝
[PROOFSTEP]
simp [(· <$> ·)]
[GOAL]
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
T : Type u_5
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : CommSemiring T
f : σ → MvPolynomial τ R
⊢ ∀ {α β : Type ?u.1607152} (x : MvPolynomial α R) (y : MvPolynomial β R),
    (SeqLeft.seqLeft x fun x => y) = Seq.seq (Function.const β <$> x) fun x => y
[PROOFSTEP]
intros
[GOAL]
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
T : Type u_5
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : CommSemiring T
f : σ → MvPolynomial τ R
α✝ β✝ : Type ?u.1607152
x✝ : MvPolynomial α✝ R
y✝ : MvPolynomial β✝ R
⊢ (SeqLeft.seqLeft x✝ fun x => y✝) = Seq.seq (Function.const β✝ <$> x✝) fun x => y✝
[PROOFSTEP]
simp [SeqLeft.seqLeft, Seq.seq, (· <$> ·), bind₁_rename]
[GOAL]
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
T : Type u_5
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : CommSemiring T
f : σ → MvPolynomial τ R
α✝ β✝ : Type ?u.1607152
x✝ : MvPolynomial α✝ R
y✝ : MvPolynomial β✝ R
⊢ ↑(bind₁ fun a => ↑(bind₁ fun x => X a) y✝) x✝ = ↑(bind₁ ((fun y => ↑(rename y) y✝) ∘ Function.const β✝)) x✝
[PROOFSTEP]
rfl
[GOAL]
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
T : Type u_5
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : CommSemiring T
f : σ → MvPolynomial τ R
⊢ ∀ {α β : Type ?u.1607152} (x : MvPolynomial α R) (y : MvPolynomial β R),
    (SeqRight.seqRight x fun x => y) = Seq.seq (Function.const α id <$> x) fun x => y
[PROOFSTEP]
intros
[GOAL]
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
T : Type u_5
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : CommSemiring T
f : σ → MvPolynomial τ R
α✝ β✝ : Type ?u.1607152
x✝ : MvPolynomial α✝ R
y✝ : MvPolynomial β✝ R
⊢ (SeqRight.seqRight x✝ fun x => y✝) = Seq.seq (Function.const α✝ id <$> x✝) fun x => y✝
[PROOFSTEP]
simp [SeqRight.seqRight, Seq.seq, (· <$> ·), bind₁_rename]
[GOAL]
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
T : Type u_5
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : CommSemiring T
f : σ → MvPolynomial τ R
α✝ β✝ : Type ?u.1607152
x✝ : MvPolynomial α✝ R
y✝ : MvPolynomial β✝ R
⊢ ↑(bind₁ fun x => y✝) x✝ = ↑(bind₁ (Function.const α✝ y✝)) x✝
[PROOFSTEP]
rfl
[GOAL]
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
T : Type u_5
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : CommSemiring T
f : σ → MvPolynomial τ R
⊢ ∀ {α β : Type ?u.1607152} (g : α → β) (x : MvPolynomial α R), (Seq.seq (pure g) fun x_1 => x) = g <$> x
[PROOFSTEP]
intros
[GOAL]
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
T : Type u_5
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : CommSemiring T
f : σ → MvPolynomial τ R
α✝ β✝ : Type ?u.1607152
g✝ : α✝ → β✝
x✝ : MvPolynomial α✝ R
⊢ (Seq.seq (pure g✝) fun x => x✝) = g✝ <$> x✝
[PROOFSTEP]
simp [(· <$> ·), pure, Seq.seq]
[GOAL]
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
T : Type u_5
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : CommSemiring T
f : σ → MvPolynomial τ R
⊢ ∀ {α β : Type ?u.1607152} (f : α → β) (x : MvPolynomial α R),
    (do
        let a ← x
        pure (f a)) =
      f <$> x
[PROOFSTEP]
aesop
[GOAL]
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
T : Type u_5
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : CommSemiring T
f : σ → MvPolynomial τ R
⊢ ∀ {α β : Type ?u.1607152} (f : MvPolynomial (α → β) R) (x : MvPolynomial α R),
    (do
        let x_1 ← f
        x_1 <$> x) =
      Seq.seq f fun x_1 => x
[PROOFSTEP]
aesop
[GOAL]
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
T : Type u_5
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : CommSemiring T
f : σ → MvPolynomial τ R
⊢ ∀ {α β : Type ?u.1607152} (x : α) (f : α → MvPolynomial β R), pure x >>= f = f x
[PROOFSTEP]
intros
[GOAL]
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
T : Type u_5
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : CommSemiring T
f : σ → MvPolynomial τ R
α✝ β✝ : Type ?u.1607152
x✝ : α✝
f✝ : α✝ → MvPolynomial β✝ R
⊢ pure x✝ >>= f✝ = f✝ x✝
[PROOFSTEP]
simp [pure, bind]
[GOAL]
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
T : Type u_5
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : CommSemiring T
f : σ → MvPolynomial τ R
⊢ ∀ {α β γ : Type ?u.1607152} (x : MvPolynomial α R) (f : α → MvPolynomial β R) (g : β → MvPolynomial γ R),
    x >>= f >>= g = x >>= fun x => f x >>= g
[PROOFSTEP]
intros
[GOAL]
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
T : Type u_5
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : CommSemiring T
f : σ → MvPolynomial τ R
α✝ β✝ γ✝ : Type ?u.1607152
x✝ : MvPolynomial α✝ R
f✝ : α✝ → MvPolynomial β✝ R
g✝ : β✝ → MvPolynomial γ✝ R
⊢ x✝ >>= f✝ >>= g✝ = x✝ >>= fun x => f✝ x >>= g✝
[PROOFSTEP]
simp [bind, ← bind₁_comp_bind₁]
