-- Mathlib/Algebra/Order/BigOperators/Group/List.lean
@[to_additive sum_pos]
lemma one_lt_prod_of_one_lt [OrderedCommMonoid M] :
    ∀ l : List M, (∀ x ∈ l, (1 : M) < x) → l ≠ [] → 1 < l.prod
  | [], _, h => (h rfl).elim
  | [b], h, _ => by simpa using h
  | a :: b :: l, hl₁, _ => by
    simp only [forall_eq_or_imp, List.mem_cons] at hl₁
    rw [List.prod_cons]
    apply one_lt_mul_of_lt_of_le' hl₁.1
    apply le_of_lt ((b :: l).one_lt_prod_of_one_lt _ (l.cons_ne_nil b))
    intro x hx; cases hx
    · exact hl₁.2.1
    · exact hl₁.2.2 _ ‹_›

Proof state:
M : Type u_3
inst✝ : OrderedCommMonoid M
a b : M
l : List M
hl₁ : ∀ (x : M), x ∈ a :: b :: l → 1 < x
x✝ : a :: b :: l ≠ []
⊢ 1 < (a :: b :: l).prod

Tactic:
simp only [forall_eq_or_imp, List.mem_cons] at hl₁

Result:
M : Type u_3
inst✝ : OrderedCommMonoid M
a b : M
l : List M
x✝ : a :: b :: l ≠ []
hl₁ : 1 < a ∧ 1 < b ∧ ∀ (a : M), a ∈ l → 1 < a
⊢ 1 < (a :: b :: l).prod

Proof state:
case head
M : Type u_3
inst✝ : OrderedCommMonoid M
a b : M
l : List M
x✝ : a :: b :: l ≠ []
hl₁ : 1 < a ∧ 1 < b ∧ ∀ (a : M), a ∈ l → 1 < a
⊢ 1 < b

Tactic:
exact hl₁.2.1

Result:
no goals

Proof state:
M : Type u_3
inst✝ : OrderedCommMonoid M
a b : M
l : List M
x✝ : a :: b :: l ≠ []
hl₁ : 1 < a ∧ 1 < b ∧ ∀ (a : M), a ∈ l → 1 < a
x : M
hx : x ∈ b :: l
⊢ 1 < x

Tactic:
cases hx

Result:
case head
M : Type u_3
inst✝ : OrderedCommMonoid M
a b : M
l : List M
x✝ : a :: b :: l ≠ []
hl₁ : 1 < a ∧ 1 < b ∧ ∀ (a : M), a ∈ l → 1 < a
⊢ 1 < b

case tail
M : Type u_3
inst✝ : OrderedCommMonoid M
a b : M
l : List M
x✝ : a :: b :: l ≠ []
hl₁ : 1 < a ∧ 1 < b ∧ ∀ (a : M), a ∈ l → 1 < a
x : M
a✝ : Mem x l
⊢ 1 < x

Proof state:
M : Type u_3
inst✝ : OrderedCommMonoid M
a b : M
l : List M
x✝ : a :: b :: l ≠ []
hl₁ : 1 < a ∧ 1 < b ∧ ∀ (a : M), a ∈ l → 1 < a
⊢ 1 ≤ (b :: l).prod

Tactic:
apply le_of_lt ((b :: l).one_lt_prod_of_one_lt _ (l.cons_ne_nil b))

Result:
M : Type u_3
inst✝ : OrderedCommMonoid M
a b : M
l : List M
x✝ : a :: b :: l ≠ []
hl₁ : 1 < a ∧ 1 < b ∧ ∀ (a : M), a ∈ l → 1 < a
⊢ ∀ (x : M), x ∈ b :: l → 1 < x

Proof state:
M : Type u_3
inst✝ : OrderedCommMonoid M
a b : M
l : List M
x✝ : a :: b :: l ≠ []
hl₁ : 1 < a ∧ 1 < b ∧ ∀ (a : M), a ∈ l → 1 < a
⊢ 1 < a * (b :: l).prod

Tactic:
apply one_lt_mul_of_lt_of_le' hl₁.1

Result:
M : Type u_3
inst✝ : OrderedCommMonoid M
a b : M
l : List M
x✝ : a :: b :: l ≠ []
hl₁ : 1 < a ∧ 1 < b ∧ ∀ (a : M), a ∈ l → 1 < a
⊢ 1 ≤ (b :: l).prod

Proof state:
M : Type u_3
inst✝ : OrderedCommMonoid M
a b : M
l : List M
x✝ : a :: b :: l ≠ []
hl₁ : 1 < a ∧ 1 < b ∧ ∀ (a : M), a ∈ l → 1 < a
⊢ ∀ (x : M), x ∈ b :: l → 1 < x

Tactic:
intro x hx

Result:
M : Type u_3
inst✝ : OrderedCommMonoid M
a b : M
l : List M
x✝ : a :: b :: l ≠ []
hl₁ : 1 < a ∧ 1 < b ∧ ∀ (a : M), a ∈ l → 1 < a
x : M
hx : x ∈ b :: l
⊢ 1 < x

Proof state:
case tail
M : Type u_3
inst✝ : OrderedCommMonoid M
a b : M
l : List M
x✝ : a :: b :: l ≠ []
hl₁ : 1 < a ∧ 1 < b ∧ ∀ (a : M), a ∈ l → 1 < a
x : M
a✝ : Mem x l
⊢ 1 < x

Tactic:
exact hl₁.2.2 _ ‹_›

Result:
no goals

Proof state:
M : Type u_3
inst✝ : OrderedCommMonoid M
a b : M
l : List M
x✝ : a :: b :: l ≠ []
hl₁ : 1 < a ∧ 1 < b ∧ ∀ (a : M), a ∈ l → 1 < a
⊢ 1 < (a :: b :: l).prod

Tactic:
rw [List.prod_cons]

Result:
M : Type u_3
inst✝ : OrderedCommMonoid M
a b : M
l : List M
x✝ : a :: b :: l ≠ []
hl₁ : 1 < a ∧ 1 < b ∧ ∀ (a : M), a ∈ l → 1 < a
⊢ 1 < a * (b :: l).prod

Proof state:
M : Type u_3
inst✝ : OrderedCommMonoid M
b : M
h : ∀ (x : M), x ∈ [b] → 1 < x
x✝ : [b] ≠ []
⊢ 1 < [b].prod

Tactic:
simpa using h

Result:
no goals