Theorem: List.length_mergeSortWith (Table/BuiltinExtensions.lean)

State before:
α : Type u_1
cmp : α → α → Ordering
x y : α
xs : List α
term₁ : Nat.succ (length (split xs).fst) < Nat.succ (Nat.succ (length xs))
term₂ : Nat.succ (length (split xs).snd) < Nat.succ (Nat.succ (length xs))
ih₁ : length (mergeSortWith cmp (x :: (split xs).fst)) = length (x :: (split xs).fst)
ih₂ : length (mergeSortWith cmp (y :: (split xs).snd)) = length (y :: (split xs).snd)
⊢ length (mergeSortWith cmp (x :: y :: xs)) = length (x :: y :: xs)
Tactic:
simp only [mergeSortWith, mergeWith, split, length_mergeWith, length]
State after:
α : Type u_1
cmp : α → α → Ordering
x y : α
xs : List α
term₁ : Nat.succ (length (split xs).fst) < Nat.succ (Nat.succ (length xs))
term₂ : Nat.succ (length (split xs).snd) < Nat.succ (Nat.succ (length xs))
ih₁ : length (mergeSortWith cmp (x :: (split xs).fst)) = length (x :: (split xs).fst)
ih₂ : length (mergeSortWith cmp (y :: (split xs).snd)) = length (y :: (split xs).snd)
⊢ length (mergeSortWith cmp (x :: (split xs).fst)) + length (mergeSortWith cmp (y :: (split xs).snd)) =
    length xs + 1 + 1

State before:
α : Type u_1
cmp : α → α → Ordering
x y : α
xs : List α
term₁ : Nat.succ (length (split xs).fst) < Nat.succ (Nat.succ (length xs))
term₂ : Nat.succ (length (split xs).snd) < Nat.succ (Nat.succ (length xs))
ih₁ : length (mergeSortWith cmp (x :: (split xs).fst)) = length (x :: (split xs).fst)
ih₂ : length (mergeSortWith cmp (y :: (split xs).snd)) = length (y :: (split xs).snd)
⊢ length (mergeSortWith cmp (x :: (split xs).fst)) + length (mergeSortWith cmp (y :: (split xs).snd)) =
    length xs + 1 + 1
Tactic:
rw [ih₁, ih₂]
State after:
α : Type u_1
cmp : α → α → Ordering
x y : α
xs : List α
term₁ : Nat.succ (length (split xs).fst) < Nat.succ (Nat.succ (length xs))
term₂ : Nat.succ (length (split xs).snd) < Nat.succ (Nat.succ (length xs))
ih₁ : length (mergeSortWith cmp (x :: (split xs).fst)) = length (x :: (split xs).fst)
ih₂ : length (mergeSortWith cmp (y :: (split xs).snd)) = length (y :: (split xs).snd)
⊢ length (x :: (split xs).fst) + length (y :: (split xs).snd) = length xs + 1 + 1

State before:
α : Type u_1
cmp : α → α → Ordering
x y : α
xs : List α
term₁ : Nat.succ (length (split xs).fst) < Nat.succ (Nat.succ (length xs))
term₂ : Nat.succ (length (split xs).snd) < Nat.succ (Nat.succ (length xs))
ih₁ : length (mergeSortWith cmp (x :: (split xs).fst)) = length (x :: (split xs).fst)
ih₂ : length (mergeSortWith cmp (y :: (split xs).snd)) = length (y :: (split xs).snd)
⊢ length (x :: (split xs).fst) + length (y :: (split xs).snd) = length xs + 1 + 1
Tactic:
simp only [length]
State after:
α : Type u_1
cmp : α → α → Ordering
x y : α
xs : List α
term₁ : Nat.succ (length (split xs).fst) < Nat.succ (Nat.succ (length xs))
term₂ : Nat.succ (length (split xs).snd) < Nat.succ (Nat.succ (length xs))
ih₁ : length (mergeSortWith cmp (x :: (split xs).fst)) = length (x :: (split xs).fst)
ih₂ : length (mergeSortWith cmp (y :: (split xs).snd)) = length (y :: (split xs).snd)
⊢ length (split xs).fst + 1 + (length (split xs).snd + 1) = length xs + 1 + 1

State before:
α : Type u_1
cmp : α → α → Ordering
x y : α
xs : List α
term₁ : Nat.succ (length (split xs).fst) < Nat.succ (Nat.succ (length xs))
term₂ : Nat.succ (length (split xs).snd) < Nat.succ (Nat.succ (length xs))
ih₁ : length (mergeSortWith cmp (x :: (split xs).fst)) = length (x :: (split xs).fst)
ih₂ : length (mergeSortWith cmp (y :: (split xs).snd)) = length (y :: (split xs).snd)
⊢ length (split xs).fst + 1 + (length (split xs).snd + 1) = length xs + 1 + 1
Tactic:
rw [Nat.add_assoc (length (split xs).1),
    Nat.add_comm 1,
    Nat.add_assoc (length (split xs).2),
    ←Nat.add_assoc (length (split xs).1),
    Nat.add_assoc (length xs)]
State after:
α : Type u_1
cmp : α → α → Ordering
x y : α
xs : List α
term₁ : Nat.succ (length (split xs).fst) < Nat.succ (Nat.succ (length xs))
term₂ : Nat.succ (length (split xs).snd) < Nat.succ (Nat.succ (length xs))
ih₁ : length (mergeSortWith cmp (x :: (split xs).fst)) = length (x :: (split xs).fst)
ih₂ : length (mergeSortWith cmp (y :: (split xs).snd)) = length (y :: (split xs).snd)
⊢ length (split xs).fst + length (split xs).snd + (1 + 1) = length xs + (1 + 1)

State before:
α : Type u_1
cmp : α → α → Ordering
x y : α
xs : List α
term₁ : Nat.succ (length (split xs).fst) < Nat.succ (Nat.succ (length xs))
term₂ : Nat.succ (length (split xs).snd) < Nat.succ (Nat.succ (length xs))
ih₁ : length (mergeSortWith cmp (x :: (split xs).fst)) = length (x :: (split xs).fst)
ih₂ : length (mergeSortWith cmp (y :: (split xs).snd)) = length (y :: (split xs).snd)
⊢ length (split xs).fst + length (split xs).snd + (1 + 1) = length xs + (1 + 1)
Tactic:
apply congrArg (λ x => x + (1 + 1))
State after:
α : Type u_1
cmp : α → α → Ordering
x y : α
xs : List α
term₁ : Nat.succ (length (split xs).fst) < Nat.succ (Nat.succ (length xs))
term₂ : Nat.succ (length (split xs).snd) < Nat.succ (Nat.succ (length xs))
ih₁ : length (mergeSortWith cmp (x :: (split xs).fst)) = length (x :: (split xs).fst)
ih₂ : length (mergeSortWith cmp (y :: (split xs).snd)) = length (y :: (split xs).snd)
⊢ length (split xs).fst + length (split xs).snd = length xs

State before:
α : Type u_1
cmp : α → α → Ordering
x y : α
xs : List α
term₁ : Nat.succ (length (split xs).fst) < Nat.succ (Nat.succ (length xs))
term₂ : Nat.succ (length (split xs).snd) < Nat.succ (Nat.succ (length xs))
ih₁ : length (mergeSortWith cmp (x :: (split xs).fst)) = length (x :: (split xs).fst)
ih₂ : length (mergeSortWith cmp (y :: (split xs).snd)) = length (y :: (split xs).snd)
⊢ length (split xs).fst + length (split xs).snd = length xs
Tactic:
apply length_split
State after:
no goals