Theorem: prodLeProdMulProdOfUnionOfOneLe (FromTheBook/Ch02/Bertrand/CentralBinom.lean)

State before:
s t₁ t₂ : Finset ℕ
f : ℕ → ℕ
hs : s ⊆ t₁ ∪ t₂
hf : ∀ (y : ℕ), 1 ≤ f y
⊢ ∏ x in s, f x ≤ (∏ x in t₁, f x) * ∏ x in t₂, f x
Tactic:
rw [← Finset.prod_union_inter]
State after:
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) * ∏ x in t₁ ∩ t₂, f x

State before:
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) * ∏ x in t₁ ∩ t₂, f x
Tactic:
apply le_trans _ (Nat.le_mul_of_pos_right _)
State after:
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

State before:
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
Tactic:
. exact Finset.prod_mono_set_of_one_le' hf hs
State after:
s t₁ t₂ : Finset ℕ
f : ℕ → ℕ
hs : s ⊆ t₁ ∪ t₂
hf : ∀ (y : ℕ), 1 ≤ f y
⊢ 0 < ∏ x in t₁ ∩ t₂, f x

State before:
s t₁ t₂ : Finset ℕ
f : ℕ → ℕ
hs : s ⊆ t₁ ∪ t₂
hf : ∀ (y : ℕ), 1 ≤ f y
⊢ 0 < ∏ x in t₁ ∩ t₂, f x
Tactic:
. apply Finset.prod_pos
  intro x _
  apply hf
State after:
no goals

State before:
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
Tactic:
exact Finset.prod_mono_set_of_one_le' hf hs
State after:
no goals

State before:
s t₁ t₂ : Finset ℕ
f : ℕ → ℕ
hs : s ⊆ t₁ ∪ t₂
hf : ∀ (y : ℕ), 1 ≤ f y
⊢ 0 < ∏ x in t₁ ∩ t₂, f x
Tactic:
apply Finset.prod_pos
State after:
case h0
s t₁ t₂ : Finset ℕ
f : ℕ → ℕ
hs : s ⊆ t₁ ∪ t₂
hf : ∀ (y : ℕ), 1 ≤ f y
⊢ ∀ (i : ℕ), i ∈ t₁ ∩ t₂ → 0 < f i

State before:
case h0
s t₁ t₂ : Finset ℕ
f : ℕ → ℕ
hs : s ⊆ t₁ ∪ t₂
hf : ∀ (y : ℕ), 1 ≤ f y
⊢ ∀ (i : ℕ), i ∈ t₁ ∩ t₂ → 0 < f i
Tactic:
intro x _
State after:
case h0
s t₁ t₂ : Finset ℕ
f : ℕ → ℕ
hs : s ⊆ t₁ ∪ t₂
hf : ∀ (y : ℕ), 1 ≤ f y
x : ℕ
a✝ : x ∈ t₁ ∩ t₂
⊢ 0 < f x

State before:
case h0
s t₁ t₂ : Finset ℕ
f : ℕ → ℕ
hs : s ⊆ t₁ ∪ t₂
hf : ∀ (y : ℕ), 1 ≤ f y
x : ℕ
a✝ : x ∈ t₁ ∩ t₂
⊢ 0 < f x
Tactic:
apply hf
State after:
no goals