no goals
σ : Type u_3
τ : Type u_1
R : Type u_2
S : Type ?u.1454752
T : Type ?u.1454755
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)
classical
simpa only [exists_prop, Finset.mem_biUnion, mem_support_iff, Ne.def] using vars_bind₁ f φ h
no goals
σ : Type u_3
τ : Type u_1
R : Type u_2
S : Type ?u.1454752
T : Type ?u.1454755
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)
simpa only [exists_prop, Finset.mem_biUnion, mem_support_iff, Ne.def] using vars_bind₁ f φ h