ι : Type u_1
α : Type ?u.129835
β : Type ?u.129838
M : Type u_2
N : Type ?u.129844
G : Type ?u.129847
k : Type ?u.129850
R : Type ?u.129853
inst✝ : OrderedCancelCommMonoid M
f g : ι → M
s t : Finset ι
h : s ⊆ t
i : ι
ht : i ∈ t
hs : ¬i ∈ s
hlt : 1 < f i
hle : ∀ (j : ι), j ∈ t → ¬j ∈ s → 1 ≤ f j
⊢ ∏ j in s, f j < f i * ∏ x in s, f x
ι : Type u_1
α : Type ?u.129835
β : Type ?u.129838
M : Type u_2
N : Type ?u.129844
G : Type ?u.129847
k : Type ?u.129850
R : Type ?u.129853
inst✝ : OrderedCancelCommMonoid M
f g : ι → M
s t : Finset ι
h : s ⊆ t
i : ι
ht : i ∈ t
hs : ¬i ∈ s
hlt : 1 < f i
hle : ∀ (j : ι), j ∈ t → ¬j ∈ s → 1 ≤ f j
⊢ ∏ j in s, f j < ∏ j in insert i s, f j
rw [prod_insert hs]
no goals
ι : Type u_1
α : Type ?u.129835
β : Type ?u.129838
M : Type u_2
N : Type ?u.129844
G : Type ?u.129847
k : Type ?u.129850
R : Type ?u.129853
inst✝ : OrderedCancelCommMonoid M
f g : ι → M
s t : Finset ι
h : s ⊆ t
i : ι
ht : i ∈ t
hs : ¬i ∈ s
hlt : 1 < f i
hle : ∀ (j : ι), j ∈ t → ¬j ∈ s → 1 ≤ f j
⊢ ∏ j in s, f j < f i * ∏ x in s, f x
exact lt_mul_of_one_lt_left' (∏ j in s, f j) hlt
case h
ι : Type u_1
α : Type ?u.129835
β : Type ?u.129838
M : Type u_2
N : Type ?u.129844
G : Type ?u.129847
k : Type ?u.129850
R : Type ?u.129853
inst✝ : OrderedCancelCommMonoid M
f g : ι → M
s t : Finset ι
h : s ⊆ t
i : ι
ht : i ∈ t
hs : ¬i ∈ s
hlt : 1 < f i
hle : ∀ (j : ι), j ∈ t → ¬j ∈ s → 1 ≤ f j
⊢ insert i s ⊆ t

case hf
ι : Type u_1
α : Type ?u.129835
β : Type ?u.129838
M : Type u_2
N : Type ?u.129844
G : Type ?u.129847
k : Type ?u.129850
R : Type ?u.129853
inst✝ : OrderedCancelCommMonoid M
f g : ι → M
s t : Finset ι
h : s ⊆ t
i : ι
ht : i ∈ t
hs : ¬i ∈ s
hlt : 1 < f i
hle : ∀ (j : ι), j ∈ t → ¬j ∈ s → 1 ≤ f j
⊢ ∀ (i_1 : ι), i_1 ∈ t → ¬i_1 ∈ insert i s → 1 ≤ f i_1
ι : Type u_1
α : Type ?u.129835
β : Type ?u.129838
M : Type u_2
N : Type ?u.129844
G : Type ?u.129847
k : Type ?u.129850
R : Type ?u.129853
inst✝ : OrderedCancelCommMonoid M
f g : ι → M
s t : Finset ι
h : s ⊆ t
i : ι
ht : i ∈ t
hs : ¬i ∈ s
hlt : 1 < f i
hle : ∀ (j : ι), j ∈ t → ¬j ∈ s → 1 ≤ f j
⊢ ∏ j in insert i s, f j ≤ ∏ j in t, f j
apply prod_le_prod_of_subset_of_one_le'
no goals
case h
ι : Type u_1
α : Type ?u.129835
β : Type ?u.129838
M : Type u_2
N : Type ?u.129844
G : Type ?u.129847
k : Type ?u.129850
R : Type ?u.129853
inst✝ : OrderedCancelCommMonoid M
f g : ι → M
s t : Finset ι
h : s ⊆ t
i : ι
ht : i ∈ t
hs : ¬i ∈ s
hlt : 1 < f i
hle : ∀ (j : ι), j ∈ t → ¬j ∈ s → 1 ≤ f j
⊢ insert i s ⊆ t
simp [Finset.insert_subset, h, ht]
case hf
ι : Type u_1
α : Type ?u.129835
β : Type ?u.129838
M : Type u_2
N : Type ?u.129844
G : Type ?u.129847
k : Type ?u.129850
R : Type ?u.129853
inst✝ : OrderedCancelCommMonoid M
f g : ι → M
s t : Finset ι
h : s ⊆ t
i : ι
ht : i ∈ t
hs : ¬i ∈ s
hlt : 1 < f i
hle : ∀ (j : ι), j ∈ t → ¬j ∈ s → 1 ≤ f j
x : ι
hx : x ∈ t
h'x : ¬x ∈ insert i s
⊢ 1 ≤ f x
case hf
ι : Type u_1
α : Type ?u.129835
β : Type ?u.129838
M : Type u_2
N : Type ?u.129844
G : Type ?u.129847
k : Type ?u.129850
R : Type ?u.129853
inst✝ : OrderedCancelCommMonoid M
f g : ι → M
s t : Finset ι
h : s ⊆ t
i : ι
ht : i ∈ t
hs : ¬i ∈ s
hlt : 1 < f i
hle : ∀ (j : ι), j ∈ t → ¬j ∈ s → 1 ≤ f j
⊢ ∀ (i_1 : ι), i_1 ∈ t → ¬i_1 ∈ insert i s → 1 ≤ f i_1
intro x hx h'x
case hf
ι : Type u_1
α : Type ?u.129835
β : Type ?u.129838
M : Type u_2
N : Type ?u.129844
G : Type ?u.129847
k : Type ?u.129850
R : Type ?u.129853
inst✝ : OrderedCancelCommMonoid M
f g : ι → M
s t : Finset ι
h : s ⊆ t
i : ι
ht : i ∈ t
hs : ¬i ∈ s
hlt : 1 < f i
hle : ∀ (j : ι), j ∈ t → ¬j ∈ s → 1 ≤ f j
x : ι
hx : x ∈ t
h'x : ¬x = i ∧ ¬x ∈ s
⊢ 1 ≤ f x
case hf
ι : Type u_1
α : Type ?u.129835
β : Type ?u.129838
M : Type u_2
N : Type ?u.129844
G : Type ?u.129847
k : Type ?u.129850
R : Type ?u.129853
inst✝ : OrderedCancelCommMonoid M
f g : ι → M
s t : Finset ι
h : s ⊆ t
i : ι
ht : i ∈ t
hs : ¬i ∈ s
hlt : 1 < f i
hle : ∀ (j : ι), j ∈ t → ¬j ∈ s → 1 ≤ f j
x : ι
hx : x ∈ t
h'x : ¬x ∈ insert i s
⊢ 1 ≤ f x
simp only [mem_insert, not_or] at h'x
no goals
case hf
ι : Type u_1
α : Type ?u.129835
β : Type ?u.129838
M : Type u_2
N : Type ?u.129844
G : Type ?u.129847
k : Type ?u.129850
R : Type ?u.129853
inst✝ : OrderedCancelCommMonoid M
f g : ι → M
s t : Finset ι
h : s ⊆ t
i : ι
ht : i ∈ t
hs : ¬i ∈ s
hlt : 1 < f i
hle : ∀ (j : ι), j ∈ t → ¬j ∈ s → 1 ≤ f j
x : ι
hx : x ∈ t
h'x : ¬x = i ∧ ¬x ∈ s
⊢ 1 ≤ f x
exact hle x hx h'x.2