-- Mathlib/Algebra/Order/BigOperators/Group/Finset.lean
theorem prod_lt_prod_of_subset' (h : s ⊆ t) {i : ι} (ht : i ∈ t) (hs : i ∉ s) (hlt : 1 < f i)
    (hle : ∀ j ∈ t, j ∉ s → 1 ≤ f j) : ∏ j ∈ s, f j < ∏ j ∈ t, f j

Proof state:
case hf
ι : Type u_1
M : Type u_4
inst✝ : OrderedCancelCommMonoid M
f : ι → M
s t : Finset ι
h : s ⊆ t
i : ι
ht : i ∈ t
hs : i ∉ s
hlt : 1 < f i
hle : ∀ j ∈ t, j ∉ s → 1 ≤ f j
x : ι
hx : x ∈ t
h'x : ¬x = i ∧ x ∉ s
⊢ 1 ≤ f x

Tactic:
exact hle x hx h'x.2

Result:
no goals

Proof state:
ι : Type u_1
M : Type u_4
inst✝ : OrderedCancelCommMonoid M
f : ι → M
s t : Finset ι
h : s ⊆ t
i : ι
ht : i ∈ t
hs : i ∉ s
hlt : 1 < f i
hle : ∀ j ∈ t, j ∉ s → 1 ≤ f j
⊢ ∏ j ∈ s, f j < ∏ j ∈ insert i s, f j

Tactic:
rw [prod_insert hs]

Result:
ι : Type u_1
M : Type u_4
inst✝ : OrderedCancelCommMonoid M
f : ι → M
s t : Finset ι
h : s ⊆ t
i : ι
ht : i ∈ t
hs : i ∉ s
hlt : 1 < f i
hle : ∀ j ∈ t, j ∉ s → 1 ≤ f j
⊢ ∏ j ∈ s, f j < f i * ∏ x ∈ s, f x

Proof state:
ι : Type u_1
M : Type u_4
inst✝ : OrderedCancelCommMonoid M
f : ι → M
s t : Finset ι
h : s ⊆ t
i : ι
ht : i ∈ t
hs : i ∉ s
hlt : 1 < f i
hle : ∀ j ∈ t, j ∉ s → 1 ≤ f j
⊢ ∏ j ∈ insert i s, f j ≤ ∏ j ∈ t, f j

Tactic:
apply prod_le_prod_of_subset_of_one_le'

Result:
case h
ι : Type u_1
M : Type u_4
inst✝ : OrderedCancelCommMonoid M
f : ι → M
s t : Finset ι
h : s ⊆ t
i : ι
ht : i ∈ t
hs : i ∉ s
hlt : 1 < f i
hle : ∀ j ∈ t, j ∉ s → 1 ≤ f j
⊢ insert i s ⊆ t

case hf
ι : Type u_1
M : Type u_4
inst✝ : OrderedCancelCommMonoid M
f : ι → M
s t : Finset ι
h : s ⊆ t
i : ι
ht : i ∈ t
hs : i ∉ s
hlt : 1 < f i
hle : ∀ j ∈ t, j ∉ s → 1 ≤ f j
⊢ ∀ i_1 ∈ t, i_1 ∉ insert i s → 1 ≤ f i_1

Proof state:
ι : Type u_1
M : Type u_4
inst✝ : OrderedCancelCommMonoid M
f : ι → M
s t : Finset ι
h : s ⊆ t
i : ι
ht : i ∈ t
hs : i ∉ s
hlt : 1 < f i
hle : ∀ j ∈ t, j ∉ s → 1 ≤ f j
⊢ ∏ j ∈ s, f j < f i * ∏ x ∈ s, f x

Tactic:
exact lt_mul_of_one_lt_left' (∏ j ∈ s, f j) hlt

Result:
no goals

Proof state:
case hf
ι : Type u_1
M : Type u_4
inst✝ : OrderedCancelCommMonoid M
f : ι → M
s t : Finset ι
h : s ⊆ t
i : ι
ht : i ∈ t
hs : i ∉ s
hlt : 1 < f i
hle : ∀ j ∈ t, j ∉ s → 1 ≤ f j
⊢ ∀ i_1 ∈ t, i_1 ∉ insert i s → 1 ≤ f i_1

Tactic:
intro x hx h'x

Result:
case hf
ι : Type u_1
M : Type u_4
inst✝ : OrderedCancelCommMonoid M
f : ι → M
s t : Finset ι
h : s ⊆ t
i : ι
ht : i ∈ t
hs : i ∉ s
hlt : 1 < f i
hle : ∀ j ∈ t, j ∉ s → 1 ≤ f j
x : ι
hx : x ∈ t
h'x : x ∉ insert i s
⊢ 1 ≤ f x

Proof state:
case hf
ι : Type u_1
M : Type u_4
inst✝ : OrderedCancelCommMonoid M
f : ι → M
s t : Finset ι
h : s ⊆ t
i : ι
ht : i ∈ t
hs : i ∉ s
hlt : 1 < f i
hle : ∀ j ∈ t, j ∉ s → 1 ≤ f j
x : ι
hx : x ∈ t
h'x : x ∉ insert i s
⊢ 1 ≤ f x

Tactic:
simp only [mem_insert, not_or] at h'x

Result:
case hf
ι : Type u_1
M : Type u_4
inst✝ : OrderedCancelCommMonoid M
f : ι → M
s t : Finset ι
h : s ⊆ t
i : ι
ht : i ∈ t
hs : i ∉ s
hlt : 1 < f i
hle : ∀ j ∈ t, j ∉ s → 1 ≤ f j
x : ι
hx : x ∈ t
h'x : ¬x = i ∧ x ∉ s
⊢ 1 ≤ f x

Proof state:
case h
ι : Type u_1
M : Type u_4
inst✝ : OrderedCancelCommMonoid M
f : ι → M
s t : Finset ι
h : s ⊆ t
i : ι
ht : i ∈ t
hs : i ∉ s
hlt : 1 < f i
hle : ∀ j ∈ t, j ∉ s → 1 ≤ f j
⊢ insert i s ⊆ t

Tactic:
simp [Finset.insert_subset_iff, h, ht]

Result:
no goals