Theorem: variable_mem_supported (DividedPowers/DPAlgebra/Misc.lean)

State before:
R : Type u_2
M : Type u_1
inst✝ : CommSemiring R
nm : ℕ × M
hn : 0 < nm.1
⊢ X nm ∈ supported R {nm | 0 < nm.1}
Tactic:
rw [mem_supported]
State after:
R : Type u_2
M : Type u_1
inst✝ : CommSemiring R
nm : ℕ × M
hn : 0 < nm.1
⊢ ↑(X nm).vars ⊆ {nm | 0 < nm.1}

State before:
R : Type u_2
M : Type u_1
inst✝ : CommSemiring R
nm : ℕ × M
hn : 0 < nm.1
⊢ ↑(X nm).vars ⊆ {nm | 0 < nm.1}
Tactic:
refine' Set.Subset.trans (Finset.coe_subset.mpr (vars_X_subset nm)) _
State after:
R : Type u_2
M : Type u_1
inst✝ : CommSemiring R
nm : ℕ × M
hn : 0 < nm.1
⊢ ↑{nm} ⊆ {nm | 0 < nm.1}

State before:
R : Type u_2
M : Type u_1
inst✝ : CommSemiring R
nm : ℕ × M
hn : 0 < nm.1
⊢ ↑{nm} ⊆ {nm | 0 < nm.1}
Tactic:
rw [coe_singleton, Set.singleton_subset_iff, Set.mem_setOf_eq]
State after:
R : Type u_2
M : Type u_1
inst✝ : CommSemiring R
nm : ℕ × M
hn : 0 < nm.1
⊢ 0 < nm.1

State before:
R : Type u_2
M : Type u_1
inst✝ : CommSemiring R
nm : ℕ × M
hn : 0 < nm.1
⊢ 0 < nm.1
Tactic:
exact hn
State after:
no goals