Theorem: Cpdt.Chapter7.split_wf_match (Cpdt/Chapter7/Wellfounded.lean)

State before:
α : Type
inst✝¹ : LE α
inst✝ : DecidableRel LE.le
x y : α
zs : List α
⊢ let spl := split [x, y];
  List.length spl.fst < List.length [] + 2 ∧ List.length spl.snd < List.length [] + 2
Tactic:
simp[split]
State after:
no goals

State before:
α : Type
inst✝¹ : LE α
inst✝ : DecidableRel LE.le
x y : α
zs : List α
a : α
⊢ let spl := split [x, y, a];
  List.length spl.fst < List.length [a] + 2 ∧ List.length spl.snd < List.length [a] + 2
Tactic:
simp[split]
State after:
no goals

State before:
α : Type
inst✝¹ : LE α
inst✝ : DecidableRel LE.le
x y : α
zs : List α
a b : α
cs : List α
⊢ let spl := split (x :: y :: a :: b :: cs);
  List.length spl.fst < List.length (a :: b :: cs) + 2 ∧ List.length spl.snd < List.length (a :: b :: cs) + 2
Tactic:
have helper := split_wf_match a b cs
State after:
α : Type
inst✝¹ : LE α
inst✝ : DecidableRel LE.le
x y : α
zs : List α
a b : α
cs : List α
helper :
  let spl := split (a :: b :: cs);
  List.length spl.fst < List.length cs + 2 ∧ List.length spl.snd < List.length cs + 2
⊢ let spl := split (x :: y :: a :: b :: cs);
  List.length spl.fst < List.length (a :: b :: cs) + 2 ∧ List.length spl.snd < List.length (a :: b :: cs) + 2

State before:
α : Type
inst✝¹ : LE α
inst✝ : DecidableRel LE.le
x y : α
zs : List α
a b : α
cs : List α
helper :
  let spl := split (a :: b :: cs);
  List.length spl.fst < List.length cs + 2 ∧ List.length spl.snd < List.length cs + 2
⊢ let spl := split (x :: y :: a :: b :: cs);
  List.length spl.fst < List.length (a :: b :: cs) + 2 ∧ List.length spl.snd < List.length (a :: b :: cs) + 2
Tactic:
simp_all_arith[split]
State after:
α : Type
inst✝¹ : LE α
inst✝ : DecidableRel LE.le
x y : α
zs : List α
a b : α
cs : List α
helper : List.length (split cs).fst ≤ List.length cs ∧ List.length (split cs).snd ≤ List.length cs
⊢ List.length (split cs).fst ≤ List.length cs + 1 ∧ List.length (split cs).snd ≤ List.length cs + 1

State before:
α : Type
inst✝¹ : LE α
inst✝ : DecidableRel LE.le
x y : α
zs : List α
a b : α
cs : List α
helper : List.length (split cs).fst ≤ List.length cs ∧ List.length (split cs).snd ≤ List.length cs
⊢ List.length (split cs).fst ≤ List.length cs + 1 ∧ List.length (split cs).snd ≤ List.length cs + 1
Tactic:
constructor
State after:
case left
α : Type
inst✝¹ : LE α
inst✝ : DecidableRel LE.le
x y : α
zs : List α
a b : α
cs : List α
helper : List.length (split cs).fst ≤ List.length cs ∧ List.length (split cs).snd ≤ List.length cs
⊢ List.length (split cs).fst ≤ List.length cs + 1

case right
α : Type
inst✝¹ : LE α
inst✝ : DecidableRel LE.le
x y : α
zs : List α
a b : α
cs : List α
helper : List.length (split cs).fst ≤ List.length cs ∧ List.length (split cs).snd ≤ List.length cs
⊢ List.length (split cs).snd ≤ List.length cs + 1

State before:
case left
α : Type
inst✝¹ : LE α
inst✝ : DecidableRel LE.le
x y : α
zs : List α
a b : α
cs : List α
helper : List.length (split cs).fst ≤ List.length cs ∧ List.length (split cs).snd ≤ List.length cs
⊢ List.length (split cs).fst ≤ List.length cs + 1

case right
α : Type
inst✝¹ : LE α
inst✝ : DecidableRel LE.le
x y : α
zs : List α
a b : α
cs : List α
helper : List.length (split cs).fst ≤ List.length cs ∧ List.length (split cs).snd ≤ List.length cs
⊢ List.length (split cs).snd ≤ List.length cs + 1
Tactic:
apply Nat.le_trans helper.left
State after:
case left
α : Type
inst✝¹ : LE α
inst✝ : DecidableRel LE.le
x y : α
zs : List α
a b : α
cs : List α
helper : List.length (split cs).fst ≤ List.length cs ∧ List.length (split cs).snd ≤ List.length cs
⊢ List.length cs ≤ List.length cs + 1

case right
α : Type
inst✝¹ : LE α
inst✝ : DecidableRel LE.le
x y : α
zs : List α
a b : α
cs : List α
helper : List.length (split cs).fst ≤ List.length cs ∧ List.length (split cs).snd ≤ List.length cs
⊢ List.length (split cs).snd ≤ List.length cs + 1

State before:
case left
α : Type
inst✝¹ : LE α
inst✝ : DecidableRel LE.le
x y : α
zs : List α
a b : α
cs : List α
helper : List.length (split cs).fst ≤ List.length cs ∧ List.length (split cs).snd ≤ List.length cs
⊢ List.length cs ≤ List.length cs + 1

case right
α : Type
inst✝¹ : LE α
inst✝ : DecidableRel LE.le
x y : α
zs : List α
a b : α
cs : List α
helper : List.length (split cs).fst ≤ List.length cs ∧ List.length (split cs).snd ≤ List.length cs
⊢ List.length (split cs).snd ≤ List.length cs + 1
Tactic:
simp_arith
State after:
case right
α : Type
inst✝¹ : LE α
inst✝ : DecidableRel LE.le
x y : α
zs : List α
a b : α
cs : List α
helper : List.length (split cs).fst ≤ List.length cs ∧ List.length (split cs).snd ≤ List.length cs
⊢ List.length (split cs).snd ≤ List.length cs + 1

State before:
case right
α : Type
inst✝¹ : LE α
inst✝ : DecidableRel LE.le
x y : α
zs : List α
a b : α
cs : List α
helper : List.length (split cs).fst ≤ List.length cs ∧ List.length (split cs).snd ≤ List.length cs
⊢ List.length (split cs).snd ≤ List.length cs + 1
Tactic:
apply Nat.le_trans helper.right
State after:
case right
α : Type
inst✝¹ : LE α
inst✝ : DecidableRel LE.le
x y : α
zs : List α
a b : α
cs : List α
helper : List.length (split cs).fst ≤ List.length cs ∧ List.length (split cs).snd ≤ List.length cs
⊢ List.length cs ≤ List.length cs + 1

State before:
case right
α : Type
inst✝¹ : LE α
inst✝ : DecidableRel LE.le
x y : α
zs : List α
a b : α
cs : List α
helper : List.length (split cs).fst ≤ List.length cs ∧ List.length (split cs).snd ≤ List.length cs
⊢ List.length cs ≤ List.length cs + 1
Tactic:
simp_arith
State after:
no goals