Theorem: cons_le_is_ordered (Dictionary.lean)

State before:
α : Type
inst✝ : LE α
a : α
xs : List α
h : IsOrdered xs
hle : ∀ x ∈ xs, a ≤ x
⊢ IsOrdered (a :: xs)
Tactic:
simp only [IsOrdered, List.pairwise_cons] at *
State after:
α : Type
inst✝ : LE α
a : α
xs : List α
h : List.Pairwise LE.le xs
hle : ∀ x ∈ xs, a ≤ x
⊢ (∀ a' ∈ xs, a ≤ a') ∧ List.Pairwise LE.le xs

State before:
α : Type
inst✝ : LE α
a : α
xs : List α
h : List.Pairwise LE.le xs
hle : ∀ x ∈ xs, a ≤ x
⊢ (∀ a' ∈ xs, a ≤ a') ∧ List.Pairwise LE.le xs
Tactic:
exact ⟨hle, h⟩
State after:
no goals