case calc_1
σ : Type u_3
τ : Type u_1
R : Type u_2
S : Type ?u.1324347
T : Type ?u.1324350
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)

case calc_2
σ : Type u_3
τ : Type u_1
R : Type u_2
S : Type ?u.1324347
T : Type ?u.1324350
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)
σ : Type u_3
τ : Type u_1
R : Type u_2
S : Type ?u.1324347
T : Type ?u.1324350
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)
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) := ?_
  _ ≤ φ.vars.biUnion fun i : σ => vars (f i) := ?_
no goals
σ : Type u_3
τ : Type u_1
R : Type u_2
S : Type ?u.1324347
T : Type ?u.1324350
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 φ)))
rw [← AlgHom.map_sum, ← φ.as_sum]
no goals
σ : Type u_3
τ : Type u_1
R : Type u_2
S : Type ?u.1324347
T : Type ?u.1324350
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)
simp only [bind₁_monomial]
case calc_1.h
σ : Type u_3
τ : Type u_1
R : Type u_2
S : Type ?u.1324347
T : Type ?u.1324350
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)
case calc_1
σ : Type u_3
τ : Type u_1
R : Type u_2
S : Type ?u.1324347
T : Type ?u.1324350
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)
apply Finset.biUnion_mono
case calc_1.h
σ : Type u_3
τ : Type u_1
R : Type u_2
S : Type ?u.1324347
T : Type ?u.1324350
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)
case calc_1.h
σ : Type u_3
τ : Type u_1
R : Type u_2
S : Type ?u.1324347
T : Type ?u.1324350
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)
intro d _hd
case calc_1.h
σ : Type u_3
τ : Type u_1
R : Type u_2
S : Type ?u.1324347
T : Type ?u.1324350
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)
case calc_1.h
σ : Type u_3
τ : Type u_1
R : Type u_2
S : Type ?u.1324347
T : Type ?u.1324350
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)
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 := ?_
case calc_1.h.h
σ : Type u_3
τ : Type u_1
R : Type u_2
S : Type ?u.1324347
T : Type ?u.1324350
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)
case calc_1.h
σ : Type u_3
τ : Type u_1
R : Type u_2
S : Type ?u.1324347
T : Type ?u.1324350
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)
apply Finset.biUnion_mono
case calc_1.h.h
σ : Type u_3
τ : Type u_1
R : Type u_2
S : Type ?u.1324347
T : Type ?u.1324350
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)
case calc_1.h.h
σ : Type u_3
τ : Type u_1
R : Type u_2
S : Type ?u.1324347
T : Type ?u.1324350
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)
intro i _hi
no goals
case calc_1.h.h
σ : Type u_3
τ : Type u_1
R : Type u_2
S : Type ?u.1324347
T : Type ?u.1324350
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)
apply vars_pow
no goals
σ : Type u_3
τ : Type u_1
R : Type u_2
S : Type ?u.1324347
T : Type ?u.1324350
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)
simp only [Finset.empty_union, vars_C, Finset.le_iff_subset, Finset.Subset.refl]
case calc_2
σ : Type u_3
τ : Type u_1
R : Type u_2
S : Type ?u.1324347
T : Type ?u.1324350
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)
case calc_2
σ : Type u_3
τ : Type u_1
R : Type u_2
S : Type ?u.1324347
T : Type ?u.1324350
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)
intro j
case calc_2
σ : Type u_3
τ : Type u_1
R : Type u_2
S : Type ?u.1324347
T : Type ?u.1324350
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)
case calc_2
σ : Type u_3
τ : Type u_1
R : Type u_2
S : Type ?u.1324347
T : Type ?u.1324350
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)
simp_rw [Finset.mem_biUnion]
case calc_2.intro.intro.intro.intro
σ : Type u_3
τ : Type u_1
R : Type u_2
S : Type ?u.1324347
T : Type ?u.1324350
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)
case calc_2
σ : Type u_3
τ : Type u_1
R : Type u_2
S : Type ?u.1324347
T : Type ?u.1324350
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)
rintro ⟨d, hd, ⟨i, hi, hj⟩⟩
no goals
case calc_2.intro.intro.intro.intro
σ : Type u_3
τ : Type u_1
R : Type u_2
S : Type ?u.1324347
T : Type ?u.1324350
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)
exact ⟨i, (mem_vars _).mpr ⟨d, hd, hi⟩, hj⟩