-- Mathlib/Algebra/MvPolynomial/Monad.lean
theorem vars_bind₁ [DecidableEq τ] (f : σ → MvPolynomial τ R) (φ : MvPolynomial σ R) :
    (bind₁ f φ).vars ⊆ φ.vars.biUnion fun i => (f i).vars

Proof state:
case calc_1
σ : Type u_1
τ : Type u_2
R : Type u_3
inst✝¹ : CommSemiring R
inst✝ : DecidableEq τ
f : σ → MvPolynomial τ R
φ : MvPolynomial σ R
⊢ (φ.support.biUnion fun d => (C (coeff d φ) * ∏ i ∈ d.support, f i ^ d i).vars) ≤
    φ.support.biUnion fun d => d.support.biUnion fun i => (f i).vars

Tactic:
apply Finset.biUnion_mono

Result:
case calc_1.h
σ : Type u_1
τ : Type u_2
R : Type u_3
inst✝¹ : CommSemiring R
inst✝ : DecidableEq τ
f : σ → MvPolynomial τ R
φ : MvPolynomial σ R
⊢ ∀ a ∈ φ.support, (C (coeff a φ) * ∏ i ∈ a.support, f i ^ a i).vars ⊆ a.support.biUnion fun i => (f i).vars

Proof state:
case calc_1.h.h
σ : Type u_1
τ : Type u_2
R : Type u_3
inst✝¹ : CommSemiring R
inst✝ : DecidableEq τ
f : σ → MvPolynomial τ R
φ : MvPolynomial σ R
d : σ →₀ ℕ
_hd : d ∈ φ.support
⊢ ∀ a ∈ d.support, (f a ^ d a).vars ⊆ (f a).vars

Tactic:
intro i _hi

Result:
case calc_1.h.h
σ : Type u_1
τ : Type u_2
R : Type u_3
inst✝¹ : CommSemiring R
inst✝ : DecidableEq τ
f : σ → MvPolynomial τ R
φ : MvPolynomial σ R
d : σ →₀ ℕ
_hd : d ∈ φ.support
i : σ
_hi : i ∈ d.support
⊢ (f i ^ d i).vars ⊆ (f i).vars

Proof state:
σ : Type u_1
τ : Type u_2
R : Type u_3
inst✝¹ : CommSemiring R
inst✝ : DecidableEq τ
f : σ → MvPolynomial τ R
φ : MvPolynomial σ R
⊢ ((bind₁ f) φ).vars ⊆ φ.vars.biUnion fun i => (f i).vars

Tactic:
calc (bind₁ f φ).vars
  _ = (φ.support.sum fun x : σ →₀ ℕ => (bind₁ f) (monomial x (coeff x φ))).vars := by
    rw [← 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 ∈ 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) := ?_

Result:
case calc_1
σ : Type u_1
τ : Type u_2
R : Type u_3
inst✝¹ : CommSemiring R
inst✝ : DecidableEq τ
f : σ → MvPolynomial τ R
φ : MvPolynomial σ R
⊢ (φ.support.biUnion fun d => (C (coeff d φ) * ∏ i ∈ d.support, f i ^ d i).vars) ≤
    φ.support.biUnion fun d => d.support.biUnion fun i => (f i).vars

case calc_2
σ : Type u_1
τ : Type u_2
R : Type u_3
inst✝¹ : CommSemiring R
inst✝ : DecidableEq τ
f : σ → MvPolynomial τ R
φ : MvPolynomial σ R
⊢ (φ.support.biUnion fun d => d.support.biUnion fun i => (f i).vars) ≤ φ.vars.biUnion fun i => (f i).vars

Proof state:
case calc_2.intro.intro.intro.intro
σ : Type u_1
τ : Type u_2
R : Type u_3
inst✝¹ : CommSemiring R
inst✝ : DecidableEq τ
f : σ → MvPolynomial τ R
φ : MvPolynomial σ R
j : τ
d : σ →₀ ℕ
hd : d ∈ φ.support
i : σ
hi : i ∈ d.support
hj : j ∈ (f i).vars
⊢ ∃ a ∈ φ.vars, j ∈ (f a).vars

Tactic:
exact ⟨i, (mem_vars _).mpr ⟨d, hd, hi⟩, hj⟩

Result:
no goals

Proof state:
case calc_1.h.h
σ : Type u_1
τ : Type u_2
R : Type u_3
inst✝¹ : CommSemiring R
inst✝ : DecidableEq τ
f : σ → MvPolynomial τ R
φ : MvPolynomial σ R
d : σ →₀ ℕ
_hd : d ∈ φ.support
i : σ
_hi : i ∈ d.support
⊢ (f i ^ d i).vars ⊆ (f i).vars

Tactic:
apply vars_pow

Result:
no goals

Proof state:
case calc_1.h
σ : Type u_1
τ : Type u_2
R : Type u_3
inst✝¹ : CommSemiring R
inst✝ : DecidableEq τ
f : σ → MvPolynomial τ R
φ : MvPolynomial σ R
d : σ →₀ ℕ
_hd : d ∈ φ.support
⊢ (d.support.biUnion fun i => (f i ^ d i).vars) ≤ d.support.biUnion fun i => (f i).vars

Tactic:
apply Finset.biUnion_mono

Result:
case calc_1.h.h
σ : Type u_1
τ : Type u_2
R : Type u_3
inst✝¹ : CommSemiring R
inst✝ : DecidableEq τ
f : σ → MvPolynomial τ R
φ : MvPolynomial σ R
d : σ →₀ ℕ
_hd : d ∈ φ.support
⊢ ∀ a ∈ d.support, (f a ^ d a).vars ⊆ (f a).vars

Proof state:
case calc_1.h
σ : Type u_1
τ : Type u_2
R : Type u_3
inst✝¹ : CommSemiring R
inst✝ : DecidableEq τ
f : σ → MvPolynomial τ R
φ : MvPolynomial σ R
d : σ →₀ ℕ
_hd : d ∈ φ.support
⊢ (C (coeff d φ) * ∏ i ∈ d.support, f i ^ d i).vars ⊆ d.support.biUnion fun i => (f i).vars

Tactic:
calc
  vars (C (coeff d φ) * ∏ i ∈ d.support, f i ^ d i) ≤
      (C (coeff d φ)).vars ∪ (∏ i ∈ d.support, f i ^ d i).vars :=
    vars_mul _ _
  _ ≤ (∏ i ∈ 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 := ?_

Result:
case calc_1.h
σ : Type u_1
τ : Type u_2
R : Type u_3
inst✝¹ : CommSemiring R
inst✝ : DecidableEq τ
f : σ → MvPolynomial τ R
φ : MvPolynomial σ R
d : σ →₀ ℕ
_hd : d ∈ φ.support
⊢ (d.support.biUnion fun i => (f i ^ d i).vars) ≤ d.support.biUnion fun i => (f i).vars

Proof state:
σ : Type u_1
τ : Type u_2
R : Type u_3
inst✝¹ : CommSemiring R
inst✝ : DecidableEq τ
f : σ → MvPolynomial τ R
φ : MvPolynomial σ R
d : σ →₀ ℕ
_hd : d ∈ φ.support
⊢ (C (coeff d φ)).vars ∪ (∏ i ∈ d.support, f i ^ d i).vars ≤ (∏ i ∈ d.support, f i ^ d i).vars

Tactic:
simp only [Finset.empty_union, vars_C, Finset.le_iff_subset, Finset.Subset.refl]

Result:
no goals

Proof state:
σ : Type u_1
τ : Type u_2
R : Type u_3
inst✝¹ : CommSemiring R
inst✝ : DecidableEq τ
f : σ → MvPolynomial τ R
φ : MvPolynomial σ R
⊢ ((bind₁ f) φ).vars = (∑ x ∈ φ.support, (bind₁ f) ((monomial x) (coeff x φ))).vars

Tactic:
rw [← map_sum, ← φ.as_sum]

Result:
no goals

Proof state:
case calc_2
σ : Type u_1
τ : Type u_2
R : Type u_3
inst✝¹ : CommSemiring R
inst✝ : DecidableEq τ
f : σ → MvPolynomial τ R
φ : MvPolynomial σ R
j : τ
⊢ (j ∈ φ.support.biUnion fun d => d.support.biUnion fun i => (f i).vars) → j ∈ φ.vars.biUnion fun i => (f i).vars

Tactic:
simp_rw [Finset.mem_biUnion]

Result:
case calc_2
σ : Type u_1
τ : Type u_2
R : Type u_3
inst✝¹ : CommSemiring R
inst✝ : DecidableEq τ
f : σ → MvPolynomial τ R
φ : MvPolynomial σ R
j : τ
⊢ (∃ a ∈ φ.support, ∃ a_1 ∈ a.support, j ∈ (f a_1).vars) → ∃ a ∈ φ.vars, j ∈ (f a).vars

Proof state:
case calc_1.h
σ : Type u_1
τ : Type u_2
R : Type u_3
inst✝¹ : CommSemiring R
inst✝ : DecidableEq τ
f : σ → MvPolynomial τ R
φ : MvPolynomial σ R
⊢ ∀ a ∈ φ.support, (C (coeff a φ) * ∏ i ∈ a.support, f i ^ a i).vars ⊆ a.support.biUnion fun i => (f i).vars

Tactic:
intro d _hd

Result:
case calc_1.h
σ : Type u_1
τ : Type u_2
R : Type u_3
inst✝¹ : CommSemiring R
inst✝ : DecidableEq τ
f : σ → MvPolynomial τ R
φ : MvPolynomial σ R
d : σ →₀ ℕ
_hd : d ∈ φ.support
⊢ (C (coeff d φ) * ∏ i ∈ d.support, f i ^ d i).vars ⊆ d.support.biUnion fun i => (f i).vars

Proof state:
case calc_2
σ : Type u_1
τ : Type u_2
R : Type u_3
inst✝¹ : CommSemiring R
inst✝ : DecidableEq τ
f : σ → MvPolynomial τ R
φ : MvPolynomial σ R
j : τ
⊢ (∃ a ∈ φ.support, ∃ a_1 ∈ a.support, j ∈ (f a_1).vars) → ∃ a ∈ φ.vars, j ∈ (f a).vars

Tactic:
rintro ⟨d, hd, ⟨i, hi, hj⟩⟩

Result:
case calc_2.intro.intro.intro.intro
σ : Type u_1
τ : Type u_2
R : Type u_3
inst✝¹ : CommSemiring R
inst✝ : DecidableEq τ
f : σ → MvPolynomial τ R
φ : MvPolynomial σ R
j : τ
d : σ →₀ ℕ
hd : d ∈ φ.support
i : σ
hi : i ∈ d.support
hj : j ∈ (f i).vars
⊢ ∃ a ∈ φ.vars, j ∈ (f a).vars

Proof state:
case calc_2
σ : Type u_1
τ : Type u_2
R : Type u_3
inst✝¹ : CommSemiring R
inst✝ : DecidableEq τ
f : σ → MvPolynomial τ R
φ : MvPolynomial σ R
⊢ (φ.support.biUnion fun d => d.support.biUnion fun i => (f i).vars) ≤ φ.vars.biUnion fun i => (f i).vars

Tactic:
intro j

Result:
case calc_2
σ : Type u_1
τ : Type u_2
R : Type u_3
inst✝¹ : CommSemiring R
inst✝ : DecidableEq τ
f : σ → MvPolynomial τ R
φ : MvPolynomial σ R
j : τ
⊢ (j ∈ φ.support.biUnion fun d => d.support.biUnion fun i => (f i).vars) → j ∈ φ.vars.biUnion fun i => (f i).vars