Theorem: Notes.insert_sorted_of_sorted (Notes4/IndPred.lean)

State before:
α : Type
f : α → α → Bool
r : α → α → Prop
a : α
l : List α
inst✝ : Asymmetric f
a' : α
as : List α
h : Sorted f (a' :: as)
h' : f a a' = true
⊢ Sorted f (insert f a (a' :: as))
Tactic:
simp [insert, h']
State after:
α : Type
f : α → α → Bool
r : α → α → Prop
a : α
l : List α
inst✝ : Asymmetric f
a' : α
as : List α
h : Sorted f (a' :: as)
h' : f a a' = true
⊢ Sorted f (a :: a' :: as)

State before:
α : Type
f : α → α → Bool
r : α → α → Prop
a : α
l : List α
inst✝ : Asymmetric f
a' : α
as : List α
h : Sorted f (a' :: as)
h' : f a a' = true
⊢ Sorted f (a :: a' :: as)
Tactic:
apply longer h' h
State after:
no goals

State before:
α : Type
f : α → α → Bool
r : α → α → Prop
a : α
l : List α
inst✝ : Asymmetric f
a' : α
as : List α
h : Sorted f (a' :: as)
h' : f a a' = false
⊢ Sorted f (insert f a (a' :: as))
Tactic:
simp [insert, h']
State after:
α : Type
f : α → α → Bool
r : α → α → Prop
a : α
l : List α
inst✝ : Asymmetric f
a' : α
as : List α
h : Sorted f (a' :: as)
h' : f a a' = false
⊢ Sorted f (a' :: insert f a as)

State before:
α : Type
f : α → α → Bool
r : α → α → Prop
a : α
l : List α
inst✝ : Asymmetric f
a' : α
as : List α
h : Sorted f (a' :: as)
h' : f a a' = false
⊢ Sorted f (a' :: insert f a as)
Tactic:
apply cons f
State after:
case h₁
α : Type
f : α → α → Bool
r : α → α → Prop
a : α
l : List α
inst✝ : Asymmetric f
a' : α
as : List α
h : Sorted f (a' :: as)
h' : f a a' = false
⊢ Sorted f (insert f a as)

case h₃
α : Type
f : α → α → Bool
r : α → α → Prop
a : α
l : List α
inst✝ : Asymmetric f
a' : α
as : List α
h : Sorted f (a' :: as)
h' : f a a' = false
⊢ f a' (insert f a as)[0] = true

case h₂
α : Type
f : α → α → Bool
r : α → α → Prop
a : α
l : List α
inst✝ : Asymmetric f
a' : α
as : List α
h : Sorted f (a' :: as)
h' : f a a' = false
⊢ List.length (insert f a as) > 0

State before:
case h₁
α : Type
f : α → α → Bool
r : α → α → Prop
a : α
l : List α
inst✝ : Asymmetric f
a' : α
as : List α
h : Sorted f (a' :: as)
h' : f a a' = false
⊢ Sorted f (insert f a as)
Tactic:
apply insert_sorted_of_sorted <| sorted_tail_of_sorted f a' as h
State after:
no goals

State before:
case h₃
α : Type
f : α → α → Bool
r : α → α → Prop
a : α
l : List α
inst✝ : Asymmetric f
a' : α
as : List α
h : Sorted f (a' :: as)
h' : f a a' = false
⊢ f a' (insert f a as)[0] = true
Tactic:
apply ordered_cons_insert_of_unordered f h
State after:
case h₃
α : Type
f : α → α → Bool
r : α → α → Prop
a : α
l : List α
inst✝ : Asymmetric f
a' : α
as : List α
h : Sorted f (a' :: as)
h' : f a a' = false
⊢ f a' a = true

State before:
case h₃
α : Type
f : α → α → Bool
r : α → α → Prop
a : α
l : List α
inst✝ : Asymmetric f
a' : α
as : List α
h : Sorted f (a' :: as)
h' : f a a' = false
⊢ f a' a = true
Tactic:
apply asym
State after:
case h₃.a
α : Type
f : α → α → Bool
r : α → α → Prop
a : α
l : List α
inst✝ : Asymmetric f
a' : α
as : List α
h : Sorted f (a' :: as)
h' : f a a' = false
⊢ (!f a a') = true

State before:
case h₃.a
α : Type
f : α → α → Bool
r : α → α → Prop
a : α
l : List α
inst✝ : Asymmetric f
a' : α
as : List α
h : Sorted f (a' :: as)
h' : f a a' = false
⊢ (!f a a') = true
Tactic:
simp
State after:
case h₃.a
α : Type
f : α → α → Bool
r : α → α → Prop
a : α
l : List α
inst✝ : Asymmetric f
a' : α
as : List α
h : Sorted f (a' :: as)
h' : f a a' = false
⊢ f a a' = false

State before:
case h₃.a
α : Type
f : α → α → Bool
r : α → α → Prop
a : α
l : List α
inst✝ : Asymmetric f
a' : α
as : List α
h : Sorted f (a' :: as)
h' : f a a' = false
⊢ f a a' = false
Tactic:
assumption
State after:
no goals