no goals
ι : Type ?u.131727
α : Type ?u.131730
M : Type u_1
N : Type ?u.131736
P : Type ?u.131739
M₀ : Type ?u.131742
G : Type ?u.131745
R : Type ?u.131748
inst✝ : OrderedCommMonoid M
b : M
h : ∀ (x : M), x ∈ [b] → 1 < x
x✝ : [b] ≠ []
⊢ 1 < prod [b]
simpa using h
ι : Type ?u.131727
α : Type ?u.131730
M : Type u_1
N : Type ?u.131736
P : Type ?u.131739
M₀ : Type ?u.131742
G : Type ?u.131745
R : Type ?u.131748
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 < prod (a :: b :: l)
ι : Type ?u.131727
α : Type ?u.131730
M : Type u_1
N : Type ?u.131736
P : Type ?u.131739
M₀ : Type ?u.131742
G : Type ?u.131745
R : Type ?u.131748
inst✝ : OrderedCommMonoid M
a b : M
l : List M
hl₁ : ∀ (x : M), x ∈ a :: b :: l → 1 < x
x✝ : a :: b :: l ≠ []
⊢ 1 < prod (a :: b :: l)
simp only [forall_eq_or_imp, List.mem_cons] at hl₁
ι : Type ?u.131727
α : Type ?u.131730
M : Type u_1
N : Type ?u.131736
P : Type ?u.131739
M₀ : Type ?u.131742
G : Type ?u.131745
R : Type ?u.131748
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 * prod (b :: l)
ι : Type ?u.131727
α : Type ?u.131730
M : Type u_1
N : Type ?u.131736
P : Type ?u.131739
M₀ : Type ?u.131742
G : Type ?u.131745
R : Type ?u.131748
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 < prod (a :: b :: l)
rw [List.prod_cons]
ι : Type ?u.131727
α : Type ?u.131730
M : Type u_1
N : Type ?u.131736
P : Type ?u.131739
M₀ : Type ?u.131742
G : Type ?u.131745
R : Type ?u.131748
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 ≤ prod (b :: l)
ι : Type ?u.131727
α : Type ?u.131730
M : Type u_1
N : Type ?u.131736
P : Type ?u.131739
M₀ : Type ?u.131742
G : Type ?u.131745
R : Type ?u.131748
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 * prod (b :: l)
apply one_lt_mul_of_lt_of_le' hl₁.1
ι : Type ?u.131727
α : Type ?u.131730
M : Type u_1
N : Type ?u.131736
P : Type ?u.131739
M₀ : Type ?u.131742
G : Type ?u.131745
R : Type ?u.131748
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
ι : Type ?u.131727
α : Type ?u.131730
M : Type u_1
N : Type ?u.131736
P : Type ?u.131739
M₀ : Type ?u.131742
G : Type ?u.131745
R : Type ?u.131748
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 ≤ prod (b :: l)
apply le_of_lt ((b :: l).one_lt_prod_of_one_lt _ (l.cons_ne_nil b))
ι : Type ?u.131727
α : Type ?u.131730
M : Type u_1
N : Type ?u.131736
P : Type ?u.131739
M₀ : Type ?u.131742
G : Type ?u.131745
R : Type ?u.131748
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
ι : Type ?u.131727
α : Type ?u.131730
M : Type u_1
N : Type ?u.131736
P : Type ?u.131739
M₀ : Type ?u.131742
G : Type ?u.131745
R : Type ?u.131748
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
intro x hx
case head
ι : Type ?u.131727
α : Type ?u.131730
M : Type u_1
N : Type ?u.131736
P : Type ?u.131739
M₀ : Type ?u.131742
G : Type ?u.131745
R : Type ?u.131748
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
ι : Type ?u.131727
α : Type ?u.131730
M : Type u_1
N : Type ?u.131736
P : Type ?u.131739
M₀ : Type ?u.131742
G : Type ?u.131745
R : Type ?u.131748
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
ι : Type ?u.131727
α : Type ?u.131730
M : Type u_1
N : Type ?u.131736
P : Type ?u.131739
M₀ : Type ?u.131742
G : Type ?u.131745
R : Type ?u.131748
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
cases hx
no goals
case head
ι : Type ?u.131727
α : Type ?u.131730
M : Type u_1
N : Type ?u.131736
P : Type ?u.131739
M₀ : Type ?u.131742
G : Type ?u.131745
R : Type ?u.131748
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
exact hl₁.2.1
no goals
case tail
ι : Type ?u.131727
α : Type ?u.131730
M : Type u_1
N : Type ?u.131736
P : Type ?u.131739
M₀ : Type ?u.131742
G : Type ?u.131745
R : Type ?u.131748
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
exact hl₁.2.2 _ ‹_›