-- Mathlib/Algebra/Order/BigOperators/Group/List.lean
/-- See also `List.le_prod_of_mem`. -/
@[to_additive "See also `List.le_sum_of_mem`."]
lemma single_le_prod [OrderedCommMonoid M] {l : List M} (hl₁ : ∀ x ∈ l, (1 : M) ≤ x) :
    ∀ x ∈ l, x ≤ l.prod

Proof state:
case cons
M : Type u_3
inst✝ : OrderedCommMonoid M
head✝ : M
tail✝ : List M
tail_ih✝ : (∀ (x : M), x ∈ tail✝ → 1 ≤ x) → ∀ (x : M), x ∈ tail✝ → x ≤ tail✝.prod
hl₁ : 1 ≤ head✝ ∧ ∀ (x : M), x ∈ tail✝ → 1 ≤ x
⊢ head✝ ≤ head✝ * tail✝.prod ∧ ∀ (x : M), x ∈ tail✝ → x ≤ head✝ * tail✝.prod

Tactic:
constructor

Result:
case cons.left
M : Type u_3
inst✝ : OrderedCommMonoid M
head✝ : M
tail✝ : List M
tail_ih✝ : (∀ (x : M), x ∈ tail✝ → 1 ≤ x) → ∀ (x : M), x ∈ tail✝ → x ≤ tail✝.prod
hl₁ : 1 ≤ head✝ ∧ ∀ (x : M), x ∈ tail✝ → 1 ≤ x
⊢ head✝ ≤ head✝ * tail✝.prod

case cons.right
M : Type u_3
inst✝ : OrderedCommMonoid M
head✝ : M
tail✝ : List M
tail_ih✝ : (∀ (x : M), x ∈ tail✝ → 1 ≤ x) → ∀ (x : M), x ∈ tail✝ → x ≤ tail✝.prod
hl₁ : 1 ≤ head✝ ∧ ∀ (x : M), x ∈ tail✝ → 1 ≤ x
⊢ ∀ (x : M), x ∈ tail✝ → x ≤ head✝ * tail✝.prod

Proof state:
M : Type u_3
inst✝ : OrderedCommMonoid M
l : List M
hl₁ : ∀ (x : M), x ∈ l → 1 ≤ x
⊢ ∀ (x : M), x ∈ l → x ≤ l.prod

Tactic:
induction l

Result:
case nil
M : Type u_3
inst✝ : OrderedCommMonoid M
hl₁ : ∀ (x : M), x ∈ [] → 1 ≤ x
⊢ ∀ (x : M), x ∈ [] → x ≤ [].prod

case cons
M : Type u_3
inst✝ : OrderedCommMonoid M
head✝ : M
tail✝ : List M
tail_ih✝ : (∀ (x : M), x ∈ tail✝ → 1 ≤ x) → ∀ (x : M), x ∈ tail✝ → x ≤ tail✝.prod
hl₁ : ∀ (x : M), x ∈ head✝ :: tail✝ → 1 ≤ x
⊢ ∀ (x : M), x ∈ head✝ :: tail✝ → x ≤ (head✝ :: tail✝).prod

Proof state:
case cons.left
M : Type u_3
inst✝ : OrderedCommMonoid M
head✝ : M
tail✝ : List M
tail_ih✝ : (∀ (x : M), x ∈ tail✝ → 1 ≤ x) → ∀ (x : M), x ∈ tail✝ → x ≤ tail✝.prod
hl₁ : 1 ≤ head✝ ∧ ∀ (x : M), x ∈ tail✝ → 1 ≤ x
⊢ head✝ ≤ head✝ * tail✝.prod

case cons.right
M : Type u_3
inst✝ : OrderedCommMonoid M
head✝ : M
tail✝ : List M
tail_ih✝ : (∀ (x : M), x ∈ tail✝ → 1 ≤ x) → ∀ (x : M), x ∈ tail✝ → x ≤ tail✝.prod
hl₁ : 1 ≤ head✝ ∧ ∀ (x : M), x ∈ tail✝ → 1 ≤ x
⊢ ∀ (x : M), x ∈ tail✝ → x ≤ head✝ * tail✝.prod

Tactic:
case cons.left => exact le_mul_of_one_le_right' (one_le_prod_of_one_le hl₁.2)

Result:
case cons.right
M : Type u_3
inst✝ : OrderedCommMonoid M
head✝ : M
tail✝ : List M
tail_ih✝ : (∀ (x : M), x ∈ tail✝ → 1 ≤ x) → ∀ (x : M), x ∈ tail✝ → x ≤ tail✝.prod
hl₁ : 1 ≤ head✝ ∧ ∀ (x : M), x ∈ tail✝ → 1 ≤ x
⊢ ∀ (x : M), x ∈ tail✝ → x ≤ head✝ * tail✝.prod

Proof state:
M : Type u_3
inst✝ : OrderedCommMonoid M
head✝ : M
tail✝ : List M
tail_ih✝ : (∀ (x : M), x ∈ tail✝ → 1 ≤ x) → ∀ (x : M), x ∈ tail✝ → x ≤ tail✝.prod
hl₁ : 1 ≤ head✝ ∧ ∀ (x : M), x ∈ tail✝ → 1 ≤ x
⊢ head✝ ≤ head✝ * tail✝.prod

Tactic:
exact le_mul_of_one_le_right' (one_le_prod_of_one_le hl₁.2)

Result:
no goals

Proof state:
M : Type u_3
inst✝ : OrderedCommMonoid M
hd : M
tl : List M
ih : (∀ (x : M), x ∈ tl → 1 ≤ x) → ∀ (x : M), x ∈ tl → x ≤ tl.prod
hl₁ : 1 ≤ hd ∧ ∀ (x : M), x ∈ tl → 1 ≤ x
⊢ ∀ (x : M), x ∈ tl → x ≤ hd * tl.prod

Tactic:
exact fun x H => le_mul_of_one_le_of_le hl₁.1 (ih hl₁.right x H)

Result:
no goals

Proof state:
case cons.right
M : Type u_3
inst✝ : OrderedCommMonoid M
head✝ : M
tail✝ : List M
tail_ih✝ : (∀ (x : M), x ∈ tail✝ → 1 ≤ x) → ∀ (x : M), x ∈ tail✝ → x ≤ tail✝.prod
hl₁ : 1 ≤ head✝ ∧ ∀ (x : M), x ∈ tail✝ → 1 ≤ x
⊢ ∀ (x : M), x ∈ tail✝ → x ≤ head✝ * tail✝.prod

Tactic:
case cons.right hd tl ih => exact fun x H => le_mul_of_one_le_of_le hl₁.1 (ih hl₁.right x H)

Result:
no goals

Proof state:
case nil
M : Type u_3
inst✝ : OrderedCommMonoid M
hl₁ : ∀ (x : M), x ∈ [] → 1 ≤ x
⊢ ∀ (x : M), x ∈ [] → x ≤ [].prod

Tactic:
simp

Result:
no goals

Proof state:
case cons
M : Type u_3
inst✝ : OrderedCommMonoid M
head✝ : M
tail✝ : List M
tail_ih✝ : (∀ (x : M), x ∈ tail✝ → 1 ≤ x) → ∀ (x : M), x ∈ tail✝ → x ≤ tail✝.prod
hl₁ : ∀ (x : M), x ∈ head✝ :: tail✝ → 1 ≤ x
⊢ ∀ (x : M), x ∈ head✝ :: tail✝ → x ≤ (head✝ :: tail✝).prod

Tactic:
simp_rw [prod_cons, forall_mem_cons] at hl₁ ⊢

Result:
case cons
M : Type u_3
inst✝ : OrderedCommMonoid M
head✝ : M
tail✝ : List M
tail_ih✝ : (∀ (x : M), x ∈ tail✝ → 1 ≤ x) → ∀ (x : M), x ∈ tail✝ → x ≤ tail✝.prod
hl₁ : 1 ≤ head✝ ∧ ∀ (x : M), x ∈ tail✝ → 1 ≤ x
⊢ head✝ ≤ head✝ * tail✝.prod ∧ ∀ (x : M), x ∈ tail✝ → x ≤ head✝ * tail✝.prod