Theorem: ordered_insert_is_ordered (Dictionary.lean)

State before:
α : Type
hl : LinearOrder α
inst✝ : DecidableRel LE.le
a : α
l : List α
ordered : IsOrdered l
⊢ IsOrdered (insert' a l)
Tactic:
simp at *
State after:
α : Type
hl : LinearOrder α
inst✝ : DecidableRel LE.le
a : α
l : List α
ordered : List.Pairwise LE.le l
⊢ List.Pairwise LE.le (insert' a l)

State before:
α : Type
hl : LinearOrder α
inst✝ : DecidableRel LE.le
a : α
l : List α
ordered : List.Pairwise LE.le l
⊢ List.Pairwise LE.le (insert' a l)
Tactic:
induction' l with x xs ih
State after:
case nil
α : Type
hl : LinearOrder α
inst✝ : DecidableRel LE.le
a : α
ordered : List.Pairwise LE.le []
⊢ List.Pairwise LE.le (insert' a [])

case cons
α : Type
hl : LinearOrder α
inst✝ : DecidableRel LE.le
a x : α
xs : List α
ih : List.Pairwise LE.le xs → List.Pairwise LE.le (insert' a xs)
ordered : List.Pairwise LE.le (x :: xs)
⊢ List.Pairwise LE.le (insert' a (x :: xs))

State before:
case nil
α : Type
hl : LinearOrder α
inst✝ : DecidableRel LE.le
a : α
ordered : List.Pairwise LE.le []
⊢ List.Pairwise LE.le (insert' a [])
Tactic:
rw [insert', List.pairwise_cons]
State after:
case nil
α : Type
hl : LinearOrder α
inst✝ : DecidableRel LE.le
a : α
ordered : List.Pairwise LE.le []
⊢ (∀ a' ∈ [], a ≤ a') ∧ List.Pairwise LE.le []

State before:
case nil
α : Type
hl : LinearOrder α
inst✝ : DecidableRel LE.le
a : α
ordered : List.Pairwise LE.le []
⊢ (∀ a' ∈ [], a ≤ a') ∧ List.Pairwise LE.le []
Tactic:
constructor
State after:
case nil.left
α : Type
hl : LinearOrder α
inst✝ : DecidableRel LE.le
a : α
ordered : List.Pairwise LE.le []
⊢ ∀ a' ∈ [], a ≤ a'

case nil.right
α : Type
hl : LinearOrder α
inst✝ : DecidableRel LE.le
a : α
ordered : List.Pairwise LE.le []
⊢ List.Pairwise LE.le []

State before:
case nil.left
α : Type
hl : LinearOrder α
inst✝ : DecidableRel LE.le
a : α
ordered : List.Pairwise LE.le []
⊢ ∀ a' ∈ [], a ≤ a'
Tactic:
intros y hy
State after:
case nil.left
α : Type
hl : LinearOrder α
inst✝ : DecidableRel LE.le
a : α
ordered : List.Pairwise LE.le []
y : α
hy : y ∈ []
⊢ a ≤ y

State before:
case nil.left
α : Type
hl : LinearOrder α
inst✝ : DecidableRel LE.le
a : α
ordered : List.Pairwise LE.le []
y : α
hy : y ∈ []
⊢ a ≤ y
Tactic:
simp only [List.find?_nil, List.not_mem_nil] at hy
State after:
no goals

State before:
case nil.right
α : Type
hl : LinearOrder α
inst✝ : DecidableRel LE.le
a : α
ordered : List.Pairwise LE.le []
⊢ List.Pairwise LE.le []
Tactic:
exact ordered
State after:
no goals

State before:
case cons
α : Type
hl : LinearOrder α
inst✝ : DecidableRel LE.le
a x : α
xs : List α
ih : List.Pairwise LE.le xs → List.Pairwise LE.le (insert' a xs)
ordered : List.Pairwise LE.le (x :: xs)
⊢ List.Pairwise LE.le (insert' a (x :: xs))
Tactic:
rw [insert']
State after:
case cons
α : Type
hl : LinearOrder α
inst✝ : DecidableRel LE.le
a x : α
xs : List α
ih : List.Pairwise LE.le xs → List.Pairwise LE.le (insert' a xs)
ordered : List.Pairwise LE.le (x :: xs)
⊢ List.Pairwise LE.le (if a ≤ x then a :: x :: xs else x :: insert' a xs)

State before:
case cons
α : Type
hl : LinearOrder α
inst✝ : DecidableRel LE.le
a x : α
xs : List α
ih : List.Pairwise LE.le xs → List.Pairwise LE.le (insert' a xs)
ordered : List.Pairwise LE.le (x :: xs)
⊢ List.Pairwise LE.le (if a ≤ x then a :: x :: xs else x :: insert' a xs)
Tactic:
split_ifs with h
State after:
case pos
α : Type
hl : LinearOrder α
inst✝ : DecidableRel LE.le
a x : α
xs : List α
ih : List.Pairwise LE.le xs → List.Pairwise LE.le (insert' a xs)
ordered : List.Pairwise LE.le (x :: xs)
h : a ≤ x
⊢ List.Pairwise LE.le (a :: x :: xs)

case neg
α : Type
hl : LinearOrder α
inst✝ : DecidableRel LE.le
a x : α
xs : List α
ih : List.Pairwise LE.le xs → List.Pairwise LE.le (insert' a xs)
ordered : List.Pairwise LE.le (x :: xs)
h : ¬a ≤ x
⊢ List.Pairwise LE.le (x :: insert' a xs)

State before:
case pos
α : Type
hl : LinearOrder α
inst✝ : DecidableRel LE.le
a x : α
xs : List α
ih : List.Pairwise LE.le xs → List.Pairwise LE.le (insert' a xs)
ordered : List.Pairwise LE.le (x :: xs)
h : a ≤ x
⊢ List.Pairwise LE.le (a :: x :: xs)
Tactic:
rw [List.pairwise_cons]
State after:
case pos
α : Type
hl : LinearOrder α
inst✝ : DecidableRel LE.le
a x : α
xs : List α
ih : List.Pairwise LE.le xs → List.Pairwise LE.le (insert' a xs)
ordered : List.Pairwise LE.le (x :: xs)
h : a ≤ x
⊢ (∀ a' ∈ x :: xs, a ≤ a') ∧ List.Pairwise LE.le (x :: xs)

State before:
case pos
α : Type
hl : LinearOrder α
inst✝ : DecidableRel LE.le
a x : α
xs : List α
ih : List.Pairwise LE.le xs → List.Pairwise LE.le (insert' a xs)
ordered : List.Pairwise LE.le (x :: xs)
h : a ≤ x
⊢ (∀ a' ∈ x :: xs, a ≤ a') ∧ List.Pairwise LE.le (x :: xs)
Tactic:
constructor
State after:
case pos.left
α : Type
hl : LinearOrder α
inst✝ : DecidableRel LE.le
a x : α
xs : List α
ih : List.Pairwise LE.le xs → List.Pairwise LE.le (insert' a xs)
ordered : List.Pairwise LE.le (x :: xs)
h : a ≤ x
⊢ ∀ a' ∈ x :: xs, a ≤ a'

case pos.right
α : Type
hl : LinearOrder α
inst✝ : DecidableRel LE.le
a x : α
xs : List α
ih : List.Pairwise LE.le xs → List.Pairwise LE.le (insert' a xs)
ordered : List.Pairwise LE.le (x :: xs)
h : a ≤ x
⊢ List.Pairwise LE.le (x :: xs)

State before:
case pos.left
α : Type
hl : LinearOrder α
inst✝ : DecidableRel LE.le
a x : α
xs : List α
ih : List.Pairwise LE.le xs → List.Pairwise LE.le (insert' a xs)
ordered : List.Pairwise LE.le (x :: xs)
h : a ≤ x
⊢ ∀ a' ∈ x :: xs, a ≤ a'
Tactic:
intro y hy
State after:
case pos.left
α : Type
hl : LinearOrder α
inst✝ : DecidableRel LE.le
a x : α
xs : List α
ih : List.Pairwise LE.le xs → List.Pairwise LE.le (insert' a xs)
ordered : List.Pairwise LE.le (x :: xs)
h : a ≤ x
y : α
hy : y ∈ x :: xs
⊢ a ≤ y

State before:
case pos.left
α : Type
hl : LinearOrder α
inst✝ : DecidableRel LE.le
a x : α
xs : List α
ih : List.Pairwise LE.le xs → List.Pairwise LE.le (insert' a xs)
ordered : List.Pairwise LE.le (x :: xs)
h : a ≤ x
y : α
hy : y ∈ x :: xs
⊢ a ≤ y
Tactic:
rw [List.mem_cons] at hy
State after:
case pos.left
α : Type
hl : LinearOrder α
inst✝ : DecidableRel LE.le
a x : α
xs : List α
ih : List.Pairwise LE.le xs → List.Pairwise LE.le (insert' a xs)
ordered : List.Pairwise LE.le (x :: xs)
h : a ≤ x
y : α
hy : y = x ∨ y ∈ xs
⊢ a ≤ y

State before:
case pos.left
α : Type
hl : LinearOrder α
inst✝ : DecidableRel LE.le
a x : α
xs : List α
ih : List.Pairwise LE.le xs → List.Pairwise LE.le (insert' a xs)
ordered : List.Pairwise LE.le (x :: xs)
h : a ≤ x
y : α
hy : y = x ∨ y ∈ xs
⊢ a ≤ y
Tactic:
rcases hy with (heq | hmem)
State after:
case pos.left.inl
α : Type
hl : LinearOrder α
inst✝ : DecidableRel LE.le
a x : α
xs : List α
ih : List.Pairwise LE.le xs → List.Pairwise LE.le (insert' a xs)
ordered : List.Pairwise LE.le (x :: xs)
h : a ≤ x
y : α
heq : y = x
⊢ a ≤ y

case pos.left.inr
α : Type
hl : LinearOrder α
inst✝ : DecidableRel LE.le
a x : α
xs : List α
ih : List.Pairwise LE.le xs → List.Pairwise LE.le (insert' a xs)
ordered : List.Pairwise LE.le (x :: xs)
h : a ≤ x
y : α
hmem : y ∈ xs
⊢ a ≤ y

State before:
case pos.left.inl
α : Type
hl : LinearOrder α
inst✝ : DecidableRel LE.le
a x : α
xs : List α
ih : List.Pairwise LE.le xs → List.Pairwise LE.le (insert' a xs)
ordered : List.Pairwise LE.le (x :: xs)
h : a ≤ x
y : α
heq : y = x
⊢ a ≤ y
Tactic:
rw [heq]
State after:
case pos.left.inl
α : Type
hl : LinearOrder α
inst✝ : DecidableRel LE.le
a x : α
xs : List α
ih : List.Pairwise LE.le xs → List.Pairwise LE.le (insert' a xs)
ordered : List.Pairwise LE.le (x :: xs)
h : a ≤ x
y : α
heq : y = x
⊢ a ≤ x

State before:
case pos.left.inl
α : Type
hl : LinearOrder α
inst✝ : DecidableRel LE.le
a x : α
xs : List α
ih : List.Pairwise LE.le xs → List.Pairwise LE.le (insert' a xs)
ordered : List.Pairwise LE.le (x :: xs)
h : a ≤ x
y : α
heq : y = x
⊢ a ≤ x
Tactic:
exact h
State after:
no goals

State before:
case pos.left.inr
α : Type
hl : LinearOrder α
inst✝ : DecidableRel LE.le
a x : α
xs : List α
ih : List.Pairwise LE.le xs → List.Pairwise LE.le (insert' a xs)
ordered : List.Pairwise LE.le (x :: xs)
h : a ≤ x
y : α
hmem : y ∈ xs
⊢ a ≤ y
Tactic:
rw [List.pairwise_cons] at ordered
State after:
case pos.left.inr
α : Type
hl : LinearOrder α
inst✝ : DecidableRel LE.le
a x : α
xs : List α
ih : List.Pairwise LE.le xs → List.Pairwise LE.le (insert' a xs)
ordered : (∀ a' ∈ xs, x ≤ a') ∧ List.Pairwise LE.le xs
h : a ≤ x
y : α
hmem : y ∈ xs
⊢ a ≤ y

State before:
case pos.left.inr
α : Type
hl : LinearOrder α
inst✝ : DecidableRel LE.le
a x : α
xs : List α
ih : List.Pairwise LE.le xs → List.Pairwise LE.le (insert' a xs)
ordered : (∀ a' ∈ xs, x ≤ a') ∧ List.Pairwise LE.le xs
h : a ≤ x
y : α
hmem : y ∈ xs
⊢ a ≤ y
Tactic:
have hle := ordered.1 y hmem
State after:
case pos.left.inr
α : Type
hl : LinearOrder α
inst✝ : DecidableRel LE.le
a x : α
xs : List α
ih : List.Pairwise LE.le xs → List.Pairwise LE.le (insert' a xs)
ordered : (∀ a' ∈ xs, x ≤ a') ∧ List.Pairwise LE.le xs
h : a ≤ x
y : α
hmem : y ∈ xs
hle : x ≤ y
⊢ a ≤ y

State before:
case pos.left.inr
α : Type
hl : LinearOrder α
inst✝ : DecidableRel LE.le
a x : α
xs : List α
ih : List.Pairwise LE.le xs → List.Pairwise LE.le (insert' a xs)
ordered : (∀ a' ∈ xs, x ≤ a') ∧ List.Pairwise LE.le xs
h : a ≤ x
y : α
hmem : y ∈ xs
hle : x ≤ y
⊢ a ≤ y
Tactic:
exact ge_trans hle h
State after:
no goals

State before:
case pos.right
α : Type
hl : LinearOrder α
inst✝ : DecidableRel LE.le
a x : α
xs : List α
ih : List.Pairwise LE.le xs → List.Pairwise LE.le (insert' a xs)
ordered : List.Pairwise LE.le (x :: xs)
h : a ≤ x
⊢ List.Pairwise LE.le (x :: xs)
Tactic:
exact ordered
State after:
no goals

State before:
case neg
α : Type
hl : LinearOrder α
inst✝ : DecidableRel LE.le
a x : α
xs : List α
ih : List.Pairwise LE.le xs → List.Pairwise LE.le (insert' a xs)
ordered : List.Pairwise LE.le (x :: xs)
h : ¬a ≤ x
⊢ List.Pairwise LE.le (x :: insert' a xs)
Tactic:
rw [List.pairwise_cons]
State after:
case neg
α : Type
hl : LinearOrder α
inst✝ : DecidableRel LE.le
a x : α
xs : List α
ih : List.Pairwise LE.le xs → List.Pairwise LE.le (insert' a xs)
ordered : List.Pairwise LE.le (x :: xs)
h : ¬a ≤ x
⊢ (∀ a' ∈ insert' a xs, x ≤ a') ∧ List.Pairwise LE.le (insert' a xs)

State before:
case neg
α : Type
hl : LinearOrder α
inst✝ : DecidableRel LE.le
a x : α
xs : List α
ih : List.Pairwise LE.le xs → List.Pairwise LE.le (insert' a xs)
ordered : List.Pairwise LE.le (x :: xs)
h : ¬a ≤ x
⊢ (∀ a' ∈ insert' a xs, x ≤ a') ∧ List.Pairwise LE.le (insert' a xs)
Tactic:
rw [List.pairwise_cons] at ordered
State after:
case neg
α : Type
hl : LinearOrder α
inst✝ : DecidableRel LE.le
a x : α
xs : List α
ih : List.Pairwise LE.le xs → List.Pairwise LE.le (insert' a xs)
ordered : (∀ a' ∈ xs, x ≤ a') ∧ List.Pairwise LE.le xs
h : ¬a ≤ x
⊢ (∀ a' ∈ insert' a xs, x ≤ a') ∧ List.Pairwise LE.le (insert' a xs)

State before:
case neg
α : Type
hl : LinearOrder α
inst✝ : DecidableRel LE.le
a x : α
xs : List α
ih : List.Pairwise LE.le xs → List.Pairwise LE.le (insert' a xs)
ordered : (∀ a' ∈ xs, x ≤ a') ∧ List.Pairwise LE.le xs
h : ¬a ≤ x
⊢ (∀ a' ∈ insert' a xs, x ≤ a') ∧ List.Pairwise LE.le (insert' a xs)
Tactic:
constructor
State after:
case neg.left
α : Type
hl : LinearOrder α
inst✝ : DecidableRel LE.le
a x : α
xs : List α
ih : List.Pairwise LE.le xs → List.Pairwise LE.le (insert' a xs)
ordered : (∀ a' ∈ xs, x ≤ a') ∧ List.Pairwise LE.le xs
h : ¬a ≤ x
⊢ ∀ a' ∈ insert' a xs, x ≤ a'

case neg.right
α : Type
hl : LinearOrder α
inst✝ : DecidableRel LE.le
a x : α
xs : List α
ih : List.Pairwise LE.le xs → List.Pairwise LE.le (insert' a xs)
ordered : (∀ a' ∈ xs, x ≤ a') ∧ List.Pairwise LE.le xs
h : ¬a ≤ x
⊢ List.Pairwise LE.le (insert' a xs)

State before:
case neg.left
α : Type
hl : LinearOrder α
inst✝ : DecidableRel LE.le
a x : α
xs : List α
ih : List.Pairwise LE.le xs → List.Pairwise LE.le (insert' a xs)
ordered : (∀ a' ∈ xs, x ≤ a') ∧ List.Pairwise LE.le xs
h : ¬a ≤ x
⊢ ∀ a' ∈ insert' a xs, x ≤ a'
Tactic:
intros y hy
State after:
case neg.left
α : Type
hl : LinearOrder α
inst✝ : DecidableRel LE.le
a x : α
xs : List α
ih : List.Pairwise LE.le xs → List.Pairwise LE.le (insert' a xs)
ordered : (∀ a' ∈ xs, x ≤ a') ∧ List.Pairwise LE.le xs
h : ¬a ≤ x
y : α
hy : y ∈ insert' a xs
⊢ x ≤ y

State before:
case neg.left
α : Type
hl : LinearOrder α
inst✝ : DecidableRel LE.le
a x : α
xs : List α
ih : List.Pairwise LE.le xs → List.Pairwise LE.le (insert' a xs)
ordered : (∀ a' ∈ xs, x ≤ a') ∧ List.Pairwise LE.le xs
h : ¬a ≤ x
y : α
hy : y ∈ insert' a xs
⊢ x ≤ y
Tactic:
rw [insert_mem] at hy
State after:
case neg.left
α : Type
hl : LinearOrder α
inst✝ : DecidableRel LE.le
a x : α
xs : List α
ih : List.Pairwise LE.le xs → List.Pairwise LE.le (insert' a xs)
ordered : (∀ a' ∈ xs, x ≤ a') ∧ List.Pairwise LE.le xs
h : ¬a ≤ x
y : α
hy : y = a ∨ y ∈ xs
⊢ x ≤ y

State before:
case neg.left
α : Type
hl : LinearOrder α
inst✝ : DecidableRel LE.le
a x : α
xs : List α
ih : List.Pairwise LE.le xs → List.Pairwise LE.le (insert' a xs)
ordered : (∀ a' ∈ xs, x ≤ a') ∧ List.Pairwise LE.le xs
h : ¬a ≤ x
y : α
hy : y = a ∨ y ∈ xs
⊢ x ≤ y
Tactic:
rcases hy with (heq | hmem)
State after:
case neg.left.inl
α : Type
hl : LinearOrder α
inst✝ : DecidableRel LE.le
a x : α
xs : List α
ih : List.Pairwise LE.le xs → List.Pairwise LE.le (insert' a xs)
ordered : (∀ a' ∈ xs, x ≤ a') ∧ List.Pairwise LE.le xs
h : ¬a ≤ x
y : α
heq : y = a
⊢ x ≤ y

case neg.left.inr
α : Type
hl : LinearOrder α
inst✝ : DecidableRel LE.le
a x : α
xs : List α
ih : List.Pairwise LE.le xs → List.Pairwise LE.le (insert' a xs)
ordered : (∀ a' ∈ xs, x ≤ a') ∧ List.Pairwise LE.le xs
h : ¬a ≤ x
y : α
hmem : y ∈ xs
⊢ x ≤ y

State before:
case neg.left.inl
α : Type
hl : LinearOrder α
inst✝ : DecidableRel LE.le
a x : α
xs : List α
ih : List.Pairwise LE.le xs → List.Pairwise LE.le (insert' a xs)
ordered : (∀ a' ∈ xs, x ≤ a') ∧ List.Pairwise LE.le xs
h : ¬a ≤ x
y : α
heq : y = a
⊢ x ≤ y
Tactic:
rw [heq]
State after:
case neg.left.inl
α : Type
hl : LinearOrder α
inst✝ : DecidableRel LE.le
a x : α
xs : List α
ih : List.Pairwise LE.le xs → List.Pairwise LE.le (insert' a xs)
ordered : (∀ a' ∈ xs, x ≤ a') ∧ List.Pairwise LE.le xs
h : ¬a ≤ x
y : α
heq : y = a
⊢ x ≤ a

State before:
case neg.left.inl
α : Type
hl : LinearOrder α
inst✝ : DecidableRel LE.le
a x : α
xs : List α
ih : List.Pairwise LE.le xs → List.Pairwise LE.le (insert' a xs)
ordered : (∀ a' ∈ xs, x ≤ a') ∧ List.Pairwise LE.le xs
h : ¬a ≤ x
y : α
heq : y = a
⊢ x ≤ a
Tactic:
rw [not_le] at h
State after:
case neg.left.inl
α : Type
hl : LinearOrder α
inst✝ : DecidableRel LE.le
a x : α
xs : List α
ih : List.Pairwise LE.le xs → List.Pairwise LE.le (insert' a xs)
ordered : (∀ a' ∈ xs, x ≤ a') ∧ List.Pairwise LE.le xs
h : x < a
y : α
heq : y = a
⊢ x ≤ a

State before:
case neg.left.inl
α : Type
hl : LinearOrder α
inst✝ : DecidableRel LE.le
a x : α
xs : List α
ih : List.Pairwise LE.le xs → List.Pairwise LE.le (insert' a xs)
ordered : (∀ a' ∈ xs, x ≤ a') ∧ List.Pairwise LE.le xs
h : x < a
y : α
heq : y = a
⊢ x ≤ a
Tactic:
exact le_of_lt h
State after:
no goals

State before:
case neg.left.inr
α : Type
hl : LinearOrder α
inst✝ : DecidableRel LE.le
a x : α
xs : List α
ih : List.Pairwise LE.le xs → List.Pairwise LE.le (insert' a xs)
ordered : (∀ a' ∈ xs, x ≤ a') ∧ List.Pairwise LE.le xs
h : ¬a ≤ x
y : α
hmem : y ∈ xs
⊢ x ≤ y
Tactic:
exact ordered.1 y hmem
State after:
no goals

State before:
case neg.right
α : Type
hl : LinearOrder α
inst✝ : DecidableRel LE.le
a x : α
xs : List α
ih : List.Pairwise LE.le xs → List.Pairwise LE.le (insert' a xs)
ordered : (∀ a' ∈ xs, x ≤ a') ∧ List.Pairwise LE.le xs
h : ¬a ≤ x
⊢ List.Pairwise LE.le (insert' a xs)
Tactic:
exact ih ordered.2
State after:
no goals