-- Mathlib/Algebra/Order/BigOperators/Group/List.lean
/-- If `l₁` is a sublist of `l₂` and all elements of `l₂` are greater than or equal to one, then
`l₁.prod ≤ l₂.prod`. One can prove a stronger version assuming `∀ a ∈ l₂.diff l₁, 1 ≤ a` instead
of `∀ a ∈ l₂, 1 ≤ a` but this lemma is not yet in `mathlib`. -/
@[to_additive sum_le_sum "If `l₁` is a sublist of `l₂` and all elements of `l₂` are nonnegative,
  then `l₁.sum ≤ l₂.sum`.
  One can prove a stronger version assuming `∀ a ∈ l₂.diff l₁, 0 ≤ a` instead of `∀ a ∈ l₂, 0 ≤ a`
  but this lemma is not yet in `mathlib`."]
lemma Sublist.prod_le_prod' [Preorder M] [MulRightMono M]
    [MulLeftMono M] {l₁ l₂ : List M} (h : l₁ <+ l₂)
    (h₁ : ∀ a ∈ l₂, (1 : M) ≤ a) : l₁.prod ≤ l₂.prod

Proof state:
M : Type u_3
inst✝³ : Monoid M
inst✝² : Preorder M
inst✝¹ : MulRightMono M
inst✝ : MulLeftMono M
l₁ l₂ : List M
h : l₁ <+ l₂
h₁ : ∀ (a : M), a ∈ l₂ → 1 ≤ a
⊢ l₁.prod ≤ l₂.prod

Tactic:
induction h with
| slnil => rfl
| cons a _ ih' =>
  simp only [prod_cons, forall_mem_cons] at h₁ ⊢
  exact (ih' h₁.2).trans (le_mul_of_one_le_left' h₁.1)
| cons₂ a _ ih' =>
  simp only [prod_cons, forall_mem_cons] at h₁ ⊢
  exact mul_le_mul_left' (ih' h₁.2) _

Result:
no goals

Proof state:
case slnil
M : Type u_3
inst✝³ : Monoid M
inst✝² : Preorder M
inst✝¹ : MulRightMono M
inst✝ : MulLeftMono M
l₁ l₂ : List M
h₁ : ∀ (a : M), a ∈ [] → 1 ≤ a
⊢ [].prod ≤ [].prod

Tactic:
rfl

Result:
no goals

Proof state:
case cons₂
M : Type u_3
inst✝³ : Monoid M
inst✝² : Preorder M
inst✝¹ : MulRightMono M
inst✝ : MulLeftMono M
l₁ l₂ l₁✝ l₂✝ : List M
a : M
a✝ : l₁✝ <+ l₂✝
ih' : (∀ (a : M), a ∈ l₂✝ → 1 ≤ a) → l₁✝.prod ≤ l₂✝.prod
h₁ : 1 ≤ a ∧ ∀ (x : M), x ∈ l₂✝ → 1 ≤ x
⊢ a * l₁✝.prod ≤ a * l₂✝.prod

Tactic:
exact mul_le_mul_left' (ih' h₁.2) _

Result:
no goals

Proof state:
case cons₂
M : Type u_3
inst✝³ : Monoid M
inst✝² : Preorder M
inst✝¹ : MulRightMono M
inst✝ : MulLeftMono M
l₁ l₂ l₁✝ l₂✝ : List M
a : M
a✝ : l₁✝ <+ l₂✝
ih' : (∀ (a : M), a ∈ l₂✝ → 1 ≤ a) → l₁✝.prod ≤ l₂✝.prod
h₁ : ∀ (a_1 : M), a_1 ∈ a :: l₂✝ → 1 ≤ a_1
⊢ (a :: l₁✝).prod ≤ (a :: l₂✝).prod

Tactic:
simp only [prod_cons, forall_mem_cons] at h₁ ⊢

Result:
case cons₂
M : Type u_3
inst✝³ : Monoid M
inst✝² : Preorder M
inst✝¹ : MulRightMono M
inst✝ : MulLeftMono M
l₁ l₂ l₁✝ l₂✝ : List M
a : M
a✝ : l₁✝ <+ l₂✝
ih' : (∀ (a : M), a ∈ l₂✝ → 1 ≤ a) → l₁✝.prod ≤ l₂✝.prod
h₁ : 1 ≤ a ∧ ∀ (x : M), x ∈ l₂✝ → 1 ≤ x
⊢ a * l₁✝.prod ≤ a * l₂✝.prod

Proof state:
case cons
M : Type u_3
inst✝³ : Monoid M
inst✝² : Preorder M
inst✝¹ : MulRightMono M
inst✝ : MulLeftMono M
l₁ l₂ l₁✝ l₂✝ : List M
a : M
a✝ : l₁✝ <+ l₂✝
ih' : (∀ (a : M), a ∈ l₂✝ → 1 ≤ a) → l₁✝.prod ≤ l₂✝.prod
h₁ : 1 ≤ a ∧ ∀ (x : M), x ∈ l₂✝ → 1 ≤ x
⊢ l₁✝.prod ≤ a * l₂✝.prod

Tactic:
exact (ih' h₁.2).trans (le_mul_of_one_le_left' h₁.1)

Result:
no goals

Proof state:
case cons
M : Type u_3
inst✝³ : Monoid M
inst✝² : Preorder M
inst✝¹ : MulRightMono M
inst✝ : MulLeftMono M
l₁ l₂ l₁✝ l₂✝ : List M
a : M
a✝ : l₁✝ <+ l₂✝
ih' : (∀ (a : M), a ∈ l₂✝ → 1 ≤ a) → l₁✝.prod ≤ l₂✝.prod
h₁ : ∀ (a_1 : M), a_1 ∈ a :: l₂✝ → 1 ≤ a_1
⊢ l₁✝.prod ≤ (a :: l₂✝).prod

Tactic:
simp only [prod_cons, forall_mem_cons] at h₁ ⊢

Result:
case cons
M : Type u_3
inst✝³ : Monoid M
inst✝² : Preorder M
inst✝¹ : MulRightMono M
inst✝ : MulLeftMono M
l₁ l₂ l₁✝ l₂✝ : List M
a : M
a✝ : l₁✝ <+ l₂✝
ih' : (∀ (a : M), a ∈ l₂✝ → 1 ≤ a) → l₁✝.prod ≤ l₂✝.prod
h₁ : 1 ≤ a ∧ ∀ (x : M), x ∈ l₂✝ → 1 ≤ x
⊢ l₁✝.prod ≤ a * l₂✝.prod