case mp
σ : Type u_1
τ : Type ?u.129141
R : Type u
S : Type v
r : R
e : ℕ
n m : σ
inst✝¹ : CommSemiring R
p q : MvPolynomial σ R
s t : Set σ
inst✝ : Nontrivial R
⊢ supported R s ≤ supported R t → s ⊆ t

case mpr
σ : Type u_1
τ : Type ?u.129141
R : Type u
S : Type v
r : R
e : ℕ
n m : σ
inst✝¹ : CommSemiring R
p q : MvPolynomial σ R
s t : Set σ
inst✝ : Nontrivial R
⊢ s ⊆ t → supported R s ≤ supported R t
σ : Type u_1
τ : Type ?u.129141
R : Type u
S : Type v
r : R
e : ℕ
n m : σ
inst✝¹ : CommSemiring R
p q : MvPolynomial σ R
s t : Set σ
inst✝ : Nontrivial R
⊢ supported R s ≤ supported R t ↔ s ⊆ t
constructor
case mp
σ : Type u_1
τ : Type ?u.129141
R : Type u
S : Type v
r : R
e : ℕ
n m : σ
inst✝¹ : CommSemiring R
p q : MvPolynomial σ R
s t : Set σ
inst✝ : Nontrivial R
h : supported R s ≤ supported R t
i : σ
⊢ i ∈ s → i ∈ t
case mp
σ : Type u_1
τ : Type ?u.129141
R : Type u
S : Type v
r : R
e : ℕ
n m : σ
inst✝¹ : CommSemiring R
p q : MvPolynomial σ R
s t : Set σ
inst✝ : Nontrivial R
⊢ supported R s ≤ supported R t → s ⊆ t
intro h i
no goals
case mp
σ : Type u_1
τ : Type ?u.129141
R : Type u
S : Type v
r : R
e : ℕ
n m : σ
inst✝¹ : CommSemiring R
p q : MvPolynomial σ R
s t : Set σ
inst✝ : Nontrivial R
h : supported R s ≤ supported R t
i : σ
⊢ i ∈ s → i ∈ t
simpa using @h (X i)
no goals
case mpr
σ : Type u_1
τ : Type ?u.129141
R : Type u
S : Type v
r : R
e : ℕ
n m : σ
inst✝¹ : CommSemiring R
p q : MvPolynomial σ R
s t : Set σ
inst✝ : Nontrivial R
⊢ s ⊆ t → supported R s ≤ supported R t
exact supported_mono