no goals
ι : Type u_1
α : Type ?u.125163
β : Type ?u.125166
M : Type u_2
N : Type ?u.125172
G : Type ?u.125175
k : Type ?u.125178
R : Type ?u.125181
inst✝ : OrderedCancelCommMonoid M
f g : ι → M
s t : Finset ι
Hle : ∀ (i : ι), i ∈ s → f i ≤ g i
Hlt : ∃ i, i ∈ s ∧ f i < g i
⊢ ∏ i in s, f i < ∏ i in s, g i
classical
  rcases Hlt with ⟨i, hi, hlt⟩
  rw [← insert_erase hi, prod_insert (not_mem_erase _ _), prod_insert (not_mem_erase _ _)]
  exact mul_lt_mul_of_lt_of_le hlt (prod_le_prod' fun j hj ↦ Hle j <| mem_of_mem_erase hj)
case intro.intro
ι : Type u_1
α : Type ?u.125163
β : Type ?u.125166
M : Type u_2
N : Type ?u.125172
G : Type ?u.125175
k : Type ?u.125178
R : Type ?u.125181
inst✝ : OrderedCancelCommMonoid M
f g : ι → M
s t : Finset ι
Hle : ∀ (i : ι), i ∈ s → f i ≤ g i
i : ι
hi : i ∈ s
hlt : f i < g i
⊢ ∏ i in s, f i < ∏ i in s, g i
ι : Type u_1
α : Type ?u.125163
β : Type ?u.125166
M : Type u_2
N : Type ?u.125172
G : Type ?u.125175
k : Type ?u.125178
R : Type ?u.125181
inst✝ : OrderedCancelCommMonoid M
f g : ι → M
s t : Finset ι
Hle : ∀ (i : ι), i ∈ s → f i ≤ g i
Hlt : ∃ i, i ∈ s ∧ f i < g i
⊢ ∏ i in s, f i < ∏ i in s, g i
rcases Hlt with ⟨i, hi, hlt⟩
case intro.intro
ι : Type u_1
α : Type ?u.125163
β : Type ?u.125166
M : Type u_2
N : Type ?u.125172
G : Type ?u.125175
k : Type ?u.125178
R : Type ?u.125181
inst✝ : OrderedCancelCommMonoid M
f g : ι → M
s t : Finset ι
Hle : ∀ (i : ι), i ∈ s → f i ≤ g i
i : ι
hi : i ∈ s
hlt : f i < g i
⊢ f i * ∏ x in erase s i, f x < g i * ∏ x in erase s i, g x
case intro.intro
ι : Type u_1
α : Type ?u.125163
β : Type ?u.125166
M : Type u_2
N : Type ?u.125172
G : Type ?u.125175
k : Type ?u.125178
R : Type ?u.125181
inst✝ : OrderedCancelCommMonoid M
f g : ι → M
s t : Finset ι
Hle : ∀ (i : ι), i ∈ s → f i ≤ g i
i : ι
hi : i ∈ s
hlt : f i < g i
⊢ ∏ i in s, f i < ∏ i in s, g i
rw [← insert_erase hi, prod_insert (not_mem_erase _ _), prod_insert (not_mem_erase _ _)]
no goals
case intro.intro
ι : Type u_1
α : Type ?u.125163
β : Type ?u.125166
M : Type u_2
N : Type ?u.125172
G : Type ?u.125175
k : Type ?u.125178
R : Type ?u.125181
inst✝ : OrderedCancelCommMonoid M
f g : ι → M
s t : Finset ι
Hle : ∀ (i : ι), i ∈ s → f i ≤ g i
i : ι
hi : i ∈ s
hlt : f i < g i
⊢ f i * ∏ x in erase s i, f x < g i * ∏ x in erase s i, g x
exact mul_lt_mul_of_lt_of_le hlt (prod_le_prod' fun j hj ↦ Hle j <| mem_of_mem_erase hj)