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

State before:
α : Type
f : α → α → Bool
r : α → α → Prop
a : α
l : List α
⊢ List.length (insert f a l) = List.length l + 1
Tactic:
match l with 
| [] => simp [insert]
| a'::as =>
  match h : f a a' with 
  | true => simp [insert, h]
  | false => simp [insert, h]; apply len_insert_eq_succ_len
State after:
no goals

State before:
α : Type
f : α → α → Bool
r : α → α → Prop
a : α
l : List α
⊢ List.length (insert f a []) = List.length [] + 1
Tactic:
simp [insert]
State after:
no goals

State before:
α : Type
f : α → α → Bool
r : α → α → Prop
a : α
l : List α
a' : α
as : List α
⊢ List.length (insert f a (a' :: as)) = List.length (a' :: as) + 1
Tactic:
match h : f a a' with 
| true => simp [insert, h]
| false => simp [insert, h]; apply len_insert_eq_succ_len
State after:
no goals

State before:
α : Type
f : α → α → Bool
r : α → α → Prop
a : α
l : List α
a' : α
as : List α
h : f a a' = true
⊢ List.length (insert f a (a' :: as)) = List.length (a' :: as) + 1
Tactic:
simp [insert, h]
State after:
no goals

State before:
α : Type
f : α → α → Bool
r : α → α → Prop
a : α
l : List α
a' : α
as : List α
h : f a a' = false
⊢ List.length (insert f a (a' :: as)) = List.length (a' :: as) + 1
Tactic:
simp [insert, h]
State after:
α : Type
f : α → α → Bool
r : α → α → Prop
a : α
l : List α
a' : α
as : List α
h : f a a' = false
⊢ List.length (insert f a as) = List.length as + 1

State before:
α : Type
f : α → α → Bool
r : α → α → Prop
a : α
l : List α
a' : α
as : List α
h : f a a' = false
⊢ List.length (insert f a as) = List.length as + 1
Tactic:
apply len_insert_eq_succ_len
State after:
no goals