. exact Finset.prod_mono_set_of_one_le' hf hs
s t₁ t₂ : Finset ℕ
f : ℕ → ℕ
hs : s ⊆ t₁ ∪ t₂
hf : ∀ (y : ℕ), 1 ≤ f y
⊢ ∏ x in s, f x ≤ ∏ x in t₁ ∪ t₂, f x

s t₁ t₂ : Finset ℕ
f : ℕ → ℕ
hs : s ⊆ t₁ ∪ t₂
hf : ∀ (y : ℕ), 1 ≤ f y
⊢ 0 < ∏ x in t₁ ∩ t₂, f x
s t₁ t₂ : Finset ℕ
f : ℕ → ℕ
hs : s ⊆ t₁ ∪ t₂
hf : ∀ (y : ℕ), 1 ≤ f y
⊢ 0 < ∏ x in t₁ ∩ t₂, f x