ι : Type ?u.129579
α : Type ?u.129582
M : Type u_1
N : Type ?u.129588
P : Type ?u.129591
M₀ : Type ?u.129594
G : Type ?u.129597
R : Type ?u.129600
inst✝ : CanonicallyOrderedMonoid M
L : List M
n : ℕ
⊢ prod (take n L) ≤ prod (take (n + 1) L)
ι : Type ?u.129579
α : Type ?u.129582
M : Type u_1
N : Type ?u.129588
P : Type ?u.129591
M₀ : Type ?u.129594
G : Type ?u.129597
R : Type ?u.129600
inst✝ : CanonicallyOrderedMonoid M
L : List M
⊢ Monotone fun i => prod (take i L)
refine' monotone_nat_of_le_succ fun n => _
case inl
ι : Type ?u.129579
α : Type ?u.129582
M : Type u_1
N : Type ?u.129588
P : Type ?u.129591
M₀ : Type ?u.129594
G : Type ?u.129597
R : Type ?u.129600
inst✝ : CanonicallyOrderedMonoid M
L : List M
n : ℕ
h : n < length L
⊢ prod (take n L) ≤ prod (take (n + 1) L)

case inr
ι : Type ?u.129579
α : Type ?u.129582
M : Type u_1
N : Type ?u.129588
P : Type ?u.129591
M₀ : Type ?u.129594
G : Type ?u.129597
R : Type ?u.129600
inst✝ : CanonicallyOrderedMonoid M
L : List M
n : ℕ
h : length L ≤ n
⊢ prod (take n L) ≤ prod (take (n + 1) L)
ι : Type ?u.129579
α : Type ?u.129582
M : Type u_1
N : Type ?u.129588
P : Type ?u.129591
M₀ : Type ?u.129594
G : Type ?u.129597
R : Type ?u.129600
inst✝ : CanonicallyOrderedMonoid M
L : List M
n : ℕ
⊢ prod (take n L) ≤ prod (take (n + 1) L)
cases' lt_or_le n L.length with h h
case inl
ι : Type ?u.129579
α : Type ?u.129582
M : Type u_1
N : Type ?u.129588
P : Type ?u.129591
M₀ : Type ?u.129594
G : Type ?u.129597
R : Type ?u.129600
inst✝ : CanonicallyOrderedMonoid M
L : List M
n : ℕ
h : n < length L
⊢ prod (take n L) ≤ prod (take n L) * nthLe L n h
case inl
ι : Type ?u.129579
α : Type ?u.129582
M : Type u_1
N : Type ?u.129588
P : Type ?u.129591
M₀ : Type ?u.129594
G : Type ?u.129597
R : Type ?u.129600
inst✝ : CanonicallyOrderedMonoid M
L : List M
n : ℕ
h : n < length L
⊢ prod (take n L) ≤ prod (take (n + 1) L)
rw [prod_take_succ _ _ h]
no goals
case inl
ι : Type ?u.129579
α : Type ?u.129582
M : Type u_1
N : Type ?u.129588
P : Type ?u.129591
M₀ : Type ?u.129594
G : Type ?u.129597
R : Type ?u.129600
inst✝ : CanonicallyOrderedMonoid M
L : List M
n : ℕ
h : n < length L
⊢ prod (take n L) ≤ prod (take n L) * nthLe L n h
exact le_self_mul
no goals
case inr
ι : Type ?u.129579
α : Type ?u.129582
M : Type u_1
N : Type ?u.129588
P : Type ?u.129591
M₀ : Type ?u.129594
G : Type ?u.129597
R : Type ?u.129600
inst✝ : CanonicallyOrderedMonoid M
L : List M
n : ℕ
h : length L ≤ n
⊢ prod (take n L) ≤ prod (take (n + 1) L)
simp [take_all_of_le h, take_all_of_le (le_trans h (Nat.le_succ _))]