case Hle
ι : Type u_1
α : Type ?u.128549
β : Type ?u.128552
M : Type u_2
N : Type ?u.128558
G : Type ?u.128561
k : Type ?u.128564
R : Type ?u.128567
inst✝ : OrderedCancelCommMonoid M
f g : ι → M
s t : Finset ι
hs : Finset.Nonempty s
Hlt : ∀ (i : ι), i ∈ s → f i < g i
⊢ ∀ (i : ι), i ∈ s → f i ≤ g i

case Hlt
ι : Type u_1
α : Type ?u.128549
β : Type ?u.128552
M : Type u_2
N : Type ?u.128558
G : Type ?u.128561
k : Type ?u.128564
R : Type ?u.128567
inst✝ : OrderedCancelCommMonoid M
f g : ι → M
s t : Finset ι
hs : Finset.Nonempty s
Hlt : ∀ (i : ι), i ∈ s → f i < g i
⊢ ∃ i, i ∈ s ∧ f i < g i
ι : Type u_1
α : Type ?u.128549
β : Type ?u.128552
M : Type u_2
N : Type ?u.128558
G : Type ?u.128561
k : Type ?u.128564
R : Type ?u.128567
inst✝ : OrderedCancelCommMonoid M
f g : ι → M
s t : Finset ι
hs : Finset.Nonempty s
Hlt : ∀ (i : ι), i ∈ s → f i < g i
⊢ ∏ i in s, f i < ∏ i in s, g i
apply prod_lt_prod'
case Hlt.intro
ι : Type u_1
α : Type ?u.128549
β : Type ?u.128552
M : Type u_2
N : Type ?u.128558
G : Type ?u.128561
k : Type ?u.128564
R : Type ?u.128567
inst✝ : OrderedCancelCommMonoid M
f g : ι → M
s t : Finset ι
Hlt : ∀ (i : ι), i ∈ s → f i < g i
i : ι
hi : i ∈ s
⊢ ∃ i, i ∈ s ∧ f i < g i
case Hlt
ι : Type u_1
α : Type ?u.128549
β : Type ?u.128552
M : Type u_2
N : Type ?u.128558
G : Type ?u.128561
k : Type ?u.128564
R : Type ?u.128567
inst✝ : OrderedCancelCommMonoid M
f g : ι → M
s t : Finset ι
hs : Finset.Nonempty s
Hlt : ∀ (i : ι), i ∈ s → f i < g i
⊢ ∃ i, i ∈ s ∧ f i < g i
cases' hs with i hi
no goals
case Hlt.intro
ι : Type u_1
α : Type ?u.128549
β : Type ?u.128552
M : Type u_2
N : Type ?u.128558
G : Type ?u.128561
k : Type ?u.128564
R : Type ?u.128567
inst✝ : OrderedCancelCommMonoid M
f g : ι → M
s t : Finset ι
Hlt : ∀ (i : ι), i ∈ s → f i < g i
i : ι
hi : i ∈ s
⊢ ∃ i, i ∈ s ∧ f i < g i
exact ⟨i, hi, Hlt i hi⟩
case Hle
ι : Type u_1
α : Type ?u.128549
β : Type ?u.128552
M : Type u_2
N : Type ?u.128558
G : Type ?u.128561
k : Type ?u.128564
R : Type ?u.128567
inst✝ : OrderedCancelCommMonoid M
f g : ι → M
s t : Finset ι
hs : Finset.Nonempty s
Hlt : ∀ (i : ι), i ∈ s → f i < g i
i : ι
hi : i ∈ s
⊢ f i ≤ g i
case Hle
ι : Type u_1
α : Type ?u.128549
β : Type ?u.128552
M : Type u_2
N : Type ?u.128558
G : Type ?u.128561
k : Type ?u.128564
R : Type ?u.128567
inst✝ : OrderedCancelCommMonoid M
f g : ι → M
s t : Finset ι
hs : Finset.Nonempty s
Hlt : ∀ (i : ι), i ∈ s → f i < g i
⊢ ∀ (i : ι), i ∈ s → f i ≤ g i
intro i hi
no goals
case Hle
ι : Type u_1
α : Type ?u.128549
β : Type ?u.128552
M : Type u_2
N : Type ?u.128558
G : Type ?u.128561
k : Type ?u.128564
R : Type ?u.128567
inst✝ : OrderedCancelCommMonoid M
f g : ι → M
s t : Finset ι
hs : Finset.Nonempty s
Hlt : ∀ (i : ι), i ∈ s → f i < g i
i : ι
hi : i ∈ s
⊢ f i ≤ g i
apply le_of_lt (Hlt i hi)