internlm/Lean-Github huggingface dataset:
Theorem: List.length_mergeWith
Proof state before:
case lt
α : Type u_1
cmp : α → α → Ordering
x : α
xs : List α
y : α
ys : List α
ih₁ : length (mergeWith cmp (y :: ys, xs)) = length (y :: ys) + length xs
ih₂ : length (mergeWith cmp (ys, x :: xs)) = length ys + length (x :: xs)
h₁ : length (x :: mergeWith cmp (y :: ys, xs)) = length (mergeWith cmp (y :: ys, xs)) + 1
⊢ length (x :: mergeWith cmp (y :: ys, xs)) = length (x :: xs) + length (y :: ys)
Tactic:
have h₂ : length (x :: xs) = length xs + 1 := rfl
Proof state after:
case lt
α : Type u_1
cmp : α → α → Ordering
x : α
xs : List α
y : α
ys : List α
ih₁ : length (mergeWith cmp (y :: ys, xs)) = length (y :: ys) + length xs
ih₂ : length (mergeWith cmp (ys, x :: xs)) = length ys + length (x :: xs)
h₁ : length (x :: mergeWith cmp (y :: ys, xs)) = length (mergeWith cmp (y :: ys, xs)) + 1
h₂ : length (x :: xs) = length xs + 1
⊢ length (x :: mergeWith cmp (y :: ys, xs)) = length (x :: xs) + length (y :: ys)
Theorem: List.length_mergeWith
Proof state before:
case lt
α : Type u_1
cmp : α → α → Ordering
x : α
xs : List α
y : α
ys : List α
ih₁ : length (mergeWith cmp (y :: ys, xs)) = length (y :: ys) + length xs
ih₂ : length (mergeWith cmp (ys, x :: xs)) = length ys + length (x :: xs)
h₁ : length (x :: mergeWith cmp (y :: ys, xs)) = length (mergeWith cmp (y :: ys, xs)) + 1
h₂ : length (x :: xs) = length xs + 1
⊢ length (x :: mergeWith cmp (y :: ys, xs)) = length (x :: xs) + length (y :: ys)
Tactic:
rw [h₁, h₂, Nat.add_comm (length xs + 1), ←Nat.add_assoc]
Proof state after:
case lt
α : Type u_1
cmp : α → α → Ordering
x : α
xs : List α
y : α
ys : List α
ih₁ : length (mergeWith cmp (y :: ys, xs)) = length (y :: ys) + length xs
ih₂ : length (mergeWith cmp (ys, x :: xs)) = length ys + length (x :: xs)
h₁ : length (x :: mergeWith cmp (y :: ys, xs)) = length (mergeWith cmp (y :: ys, xs)) + 1
h₂ : length (x :: xs) = length xs + 1
⊢ length (mergeWith cmp (y :: ys, xs)) + 1 = length (y :: ys) + length xs + 1
Theorem: List.length_mergeWith
Proof state before:
case lt
α : Type u_1
cmp : α → α → Ordering
x : α
xs : List α
y : α
ys : List α
ih₁ : length (mergeWith cmp (y :: ys, xs)) = length (y :: ys) + length xs
ih₂ : length (mergeWith cmp (ys, x :: xs)) = length ys + length (x :: xs)
h₁ : length (x :: mergeWith cmp (y :: ys, xs)) = length (mergeWith cmp (y :: ys, xs)) + 1
h₂ : length (x :: xs) = length xs + 1
⊢ length (mergeWith cmp (y :: ys, xs)) + 1 = length (y :: ys) + length xs + 1
Tactic:
apply congrArg (λ x => x + 1)
Proof state after:
case lt
α : Type u_1
cmp : α → α → Ordering
x : α
xs : List α
y : α
ys : List α
ih₁ : length (mergeWith cmp (y :: ys, xs)) = length (y :: ys) + length xs
ih₂ : length (mergeWith cmp (ys, x :: xs)) = length ys + length (x :: xs)
h₁ : length (x :: mergeWith cmp (y :: ys, xs)) = length (mergeWith cmp (y :: ys, xs)) + 1
h₂ : length (x :: xs) = length xs + 1
⊢ length (mergeWith cmp (y :: ys, xs)) = length (y :: ys) + length xs
Theorem: List.length_mergeWith
Proof state before:
case lt
α : Type u_1
cmp : α → α → Ordering
x : α
xs : List α
y : α
ys : List α
ih₁ : length (mergeWith cmp (y :: ys, xs)) = length (y :: ys) + length xs
ih₂ : length (mergeWith cmp (ys, x :: xs)) = length ys + length (x :: xs)
h₁ : length (x :: mergeWith cmp (y :: ys, xs)) = length (mergeWith cmp (y :: ys, xs)) + 1
h₂ : length (x :: xs) = length xs + 1
⊢ length (mergeWith cmp (y :: ys, xs)) = length (y :: ys) + length xs
Tactic:
exact ih₁
Proof state after:
no goals
Theorem: List.length_mergeWith
Proof state before:
case eq
α : Type u_1
cmp : α → α → Ordering
x : α
xs : List α
y : α
ys : List α
ih₁ : length (mergeWith cmp (y :: ys, xs)) = length (y :: ys) + length xs
ih₂ : length (mergeWith cmp (ys, x :: xs)) = length ys + length (x :: xs)
⊢ length
      (match Ordering.eq with
      | Ordering.gt => y :: mergeWith cmp (ys, x :: xs)
      | x_1 => x :: mergeWith cmp (y :: ys, xs)) =
    length (x :: xs) + length (y :: ys)
Tactic:
simp only
Proof state after:
case eq
α : Type u_1
cmp : α → α → Ordering
x : α
xs : List α
y : α
ys : List α
ih₁ : length (mergeWith cmp (y :: ys, xs)) = length (y :: ys) + length xs
ih₂ : length (mergeWith cmp (ys, x :: xs)) = length ys + length (x :: xs)
⊢ length (x :: mergeWith cmp (y :: ys, xs)) = length (x :: xs) + length (y :: ys)
Theorem: List.length_mergeWith
Proof state before:
case eq
α : Type u_1
cmp : α → α → Ordering
x : α
xs : List α
y : α
ys : List α
ih₁ : length (mergeWith cmp (y :: ys, xs)) = length (y :: ys) + length xs
ih₂ : length (mergeWith cmp (ys, x :: xs)) = length ys + length (x :: xs)
⊢ length (x :: mergeWith cmp (y :: ys, xs)) = length (x :: xs) + length (y :: ys)
Tactic:
have h₁ : length (x :: mergeWith cmp (y :: ys, xs)) =
          length (mergeWith cmp (y :: ys, xs)) + 1 := rfl
Proof state after:
case eq
α : Type u_1
cmp : α → α → Ordering
x : α
xs : List α
y : α
ys : List α
ih₁ : length (mergeWith cmp (y :: ys, xs)) = length (y :: ys) + length xs
ih₂ : length (mergeWith cmp (ys, x :: xs)) = length ys + length (x :: xs)
h₁ : length (x :: mergeWith cmp (y :: ys, xs)) = length (mergeWith cmp (y :: ys, xs)) + 1
⊢ length (x :: mergeWith cmp (y :: ys, xs)) = length (x :: xs) + length (y :: ys)
Theorem: List.length_mergeWith
Proof state before:
case eq
α : Type u_1
cmp : α → α → Ordering
x : α
xs : List α
y : α
ys : List α
ih₁ : length (mergeWith cmp (y :: ys, xs)) = length (y :: ys) + length xs
ih₂ : length (mergeWith cmp (ys, x :: xs)) = length ys + length (x :: xs)
h₁ : length (x :: mergeWith cmp (y :: ys, xs)) = length (mergeWith cmp (y :: ys, xs)) + 1
⊢ length (x :: mergeWith cmp (y :: ys, xs)) = length (x :: xs) + length (y :: ys)
Tactic:
have h₂ : length (x :: xs) = length xs + 1 := rfl
Proof state after:
case eq
α : Type u_1
cmp : α → α → Ordering
x : α
xs : List α
y : α
ys : List α
ih₁ : length (mergeWith cmp (y :: ys, xs)) = length (y :: ys) + length xs
ih₂ : length (mergeWith cmp (ys, x :: xs)) = length ys + length (x :: xs)
h₁ : length (x :: mergeWith cmp (y :: ys, xs)) = length (mergeWith cmp (y :: ys, xs)) + 1
h₂ : length (x :: xs) = length xs + 1
⊢ length (x :: mergeWith cmp (y :: ys, xs)) = length (x :: xs) + length (y :: ys)
Theorem: List.length_mergeWith
Proof state before:
case eq
α : Type u_1
cmp : α → α → Ordering
x : α
xs : List α
y : α
ys : List α
ih₁ : length (mergeWith cmp (y :: ys, xs)) = length (y :: ys) + length xs
ih₂ : length (mergeWith cmp (ys, x :: xs)) = length ys + length (x :: xs)
h₁ : length (x :: mergeWith cmp (y :: ys, xs)) = length (mergeWith cmp (y :: ys, xs)) + 1
h₂ : length (x :: xs) = length xs + 1
⊢ length (x :: mergeWith cmp (y :: ys, xs)) = length (x :: xs) + length (y :: ys)
Tactic:
rw [h₁, h₂, Nat.add_comm (length xs + 1), ←Nat.add_assoc]
Proof state after:
case eq
α : Type u_1
cmp : α → α → Ordering
x : α
xs : List α
y : α
ys : List α
ih₁ : length (mergeWith cmp (y :: ys, xs)) = length (y :: ys) + length xs
ih₂ : length (mergeWith cmp (ys, x :: xs)) = length ys + length (x :: xs)
h₁ : length (x :: mergeWith cmp (y :: ys, xs)) = length (mergeWith cmp (y :: ys, xs)) + 1
h₂ : length (x :: xs) = length xs + 1
⊢ length (mergeWith cmp (y :: ys, xs)) + 1 = length (y :: ys) + length xs + 1
Theorem: List.length_mergeWith
Proof state before:
case eq
α : Type u_1
cmp : α → α → Ordering
x : α
xs : List α
y : α
ys : List α
ih₁ : length (mergeWith cmp (y :: ys, xs)) = length (y :: ys) + length xs
ih₂ : length (mergeWith cmp (ys, x :: xs)) = length ys + length (x :: xs)
h₁ : length (x :: mergeWith cmp (y :: ys, xs)) = length (mergeWith cmp (y :: ys, xs)) + 1
h₂ : length (x :: xs) = length xs + 1
⊢ length (mergeWith cmp (y :: ys, xs)) + 1 = length (y :: ys) + length xs + 1
Tactic:
apply congrArg (λ x => x + 1)
Proof state after:
case eq
α : Type u_1
cmp : α → α → Ordering
x : α
xs : List α
y : α
ys : List α
ih₁ : length (mergeWith cmp (y :: ys, xs)) = length (y :: ys) + length xs
ih₂ : length (mergeWith cmp (ys, x :: xs)) = length ys + length (x :: xs)
h₁ : length (x :: mergeWith cmp (y :: ys, xs)) = length (mergeWith cmp (y :: ys, xs)) + 1
h₂ : length (x :: xs) = length xs + 1
⊢ length (mergeWith cmp (y :: ys, xs)) = length (y :: ys) + length xs
Theorem: List.length_mergeWith
Proof state before:
case eq
α : Type u_1
cmp : α → α → Ordering
x : α
xs : List α
y : α
ys : List α
ih₁ : length (mergeWith cmp (y :: ys, xs)) = length (y :: ys) + length xs
ih₂ : length (mergeWith cmp (ys, x :: xs)) = length ys + length (x :: xs)
h₁ : length (x :: mergeWith cmp (y :: ys, xs)) = length (mergeWith cmp (y :: ys, xs)) + 1
h₂ : length (x :: xs) = length xs + 1
⊢ length (mergeWith cmp (y :: ys, xs)) = length (y :: ys) + length xs
Tactic:
exact ih₁
Proof state after:
no goals
Theorem: List.length_mergeWith
Proof state before:
case gt
α : Type u_1
cmp : α → α → Ordering
x : α
xs : List α
y : α
ys : List α
ih₁ : length (mergeWith cmp (y :: ys, xs)) = length (y :: ys) + length xs
ih₂ : length (mergeWith cmp (ys, x :: xs)) = length ys + length (x :: xs)
⊢ length
      (match Ordering.gt with
      | Ordering.gt => y :: mergeWith cmp (ys, x :: xs)
      | x_1 => x :: mergeWith cmp (y :: ys, xs)) =
    length (x :: xs) + length (y :: ys)
Tactic:
simp only [length]
Proof state after:
case gt
α : Type u_1
cmp : α → α → Ordering
x : α
xs : List α
y : α
ys : List α
ih₁ : length (mergeWith cmp (y :: ys, xs)) = length (y :: ys) + length xs
ih₂ : length (mergeWith cmp (ys, x :: xs)) = length ys + length (x :: xs)
⊢ length (mergeWith cmp (ys, x :: xs)) + 1 = length xs + 1 + (length ys + 1)
Theorem: List.length_mergeWith
Proof state before:
case gt
α : Type u_1
cmp : α → α → Ordering
x : α
xs : List α
y : α
ys : List α
ih₁ : length (mergeWith cmp (y :: ys, xs)) = length (y :: ys) + length xs
ih₂ : length (mergeWith cmp (ys, x :: xs)) = length ys + length (x :: xs)
⊢ length (mergeWith cmp (ys, x :: xs)) + 1 = length xs + 1 + (length ys + 1)
Tactic:
simp only [length] at ih₂
Proof state after:
case gt
α : Type u_1
cmp : α → α → Ordering
x : α
xs : List α
y : α
ys : List α
ih₁ : length (mergeWith cmp (y :: ys, xs)) = length (y :: ys) + length xs
ih₂ : length (mergeWith cmp (ys, x :: xs)) = length ys + (length xs + 1)
⊢ length (mergeWith cmp (ys, x :: xs)) + 1 = length xs + 1 + (length ys + 1)
Theorem: List.length_mergeWith
Proof state before:
case gt
α : Type u_1
cmp : α → α → Ordering
x : α
xs : List α
y : α
ys : List α
ih₁ : length (mergeWith cmp (y :: ys, xs)) = length (y :: ys) + length xs
ih₂ : length (mergeWith cmp (ys, x :: xs)) = length ys + (length xs + 1)
⊢ length (mergeWith cmp (ys, x :: xs)) + 1 = length xs + 1 + (length ys + 1)
Tactic:
rw [←Nat.add_assoc]
Proof state after:
case gt
α : Type u_1
cmp : α → α → Ordering
x : α
xs : List α
y : α
ys : List α
ih₁ : length (mergeWith cmp (y :: ys, xs)) = length (y :: ys) + length xs
ih₂ : length (mergeWith cmp (ys, x :: xs)) = length ys + (length xs + 1)
⊢ length (mergeWith cmp (ys, x :: xs)) + 1 = length xs + 1 + length ys + 1
Theorem: List.length_mergeWith
Proof state before:
case gt
α : Type u_1
cmp : α → α → Ordering
x : α
xs : List α
y : α
ys : List α
ih₁ : length (mergeWith cmp (y :: ys, xs)) = length (y :: ys) + length xs
ih₂ : length (mergeWith cmp (ys, x :: xs)) = length ys + (length xs + 1)
⊢ length (mergeWith cmp (ys, x :: xs)) + 1 = length xs + 1 + length ys + 1
Tactic:
apply congrArg (λ x => x + 1)
Proof state after:
case gt
α : Type u_1
cmp : α → α → Ordering
x : α
xs : List α
y : α
ys : List α
ih₁ : length (mergeWith cmp (y :: ys, xs)) = length (y :: ys) + length xs
ih₂ : length (mergeWith cmp (ys, x :: xs)) = length ys + (length xs + 1)
⊢ length (mergeWith cmp (ys, x :: xs)) = length xs + 1 + length ys
Theorem: List.length_mergeWith
Proof state before:
case gt
α : Type u_1
cmp : α → α → Ordering
x : α
xs : List α
y : α
ys : List α
ih₁ : length (mergeWith cmp (y :: ys, xs)) = length (y :: ys) + length xs
ih₂ : length (mergeWith cmp (ys, x :: xs)) = length ys + (length xs + 1)
⊢ length (mergeWith cmp (ys, x :: xs)) = length xs + 1 + length ys
Tactic:
rw [Nat.add_comm]
Proof state after:
case gt
α : Type u_1
cmp : α → α → Ordering
x : α
xs : List α
y : α
ys : List α
ih₁ : length (mergeWith cmp (y :: ys, xs)) = length (y :: ys) + length xs
ih₂ : length (mergeWith cmp (ys, x :: xs)) = length ys + (length xs + 1)
⊢ length (mergeWith cmp (ys, x :: xs)) = length ys + (length xs + 1)
Theorem: List.length_mergeWith
Proof state before:
case gt
α : Type u_1
cmp : α → α → Ordering
x : α
xs : List α
y : α
ys : List α
ih₁ : length (mergeWith cmp (y :: ys, xs)) = length (y :: ys) + length xs
ih₂ : length (mergeWith cmp (ys, x :: xs)) = length ys + (length xs + 1)
⊢ length (mergeWith cmp (ys, x :: xs)) = length ys + (length xs + 1)
Tactic:
exact ih₂
Proof state after:
no goals
Theorem: List.length_split
Proof state before:
α : Type u_1
x y : α
xs : List α
ih : length (split xs).fst + length (split xs).snd = length xs
⊢ length (split (x :: y :: xs)).fst + length (split (x :: y :: xs)).snd = length (x :: y :: xs)
Tactic:
simp only [split, length]
Proof state after:
α : Type u_1
x y : α
xs : List α
ih : length (split xs).fst + length (split xs).snd = length xs
⊢ length (split xs).fst + 1 + (length (split xs).snd + 1) = length xs + 1 + 1
Theorem: List.length_split
Proof state before:
α : Type u_1
x y : α
xs : List α
ih : length (split xs).fst + length (split xs).snd = length xs
⊢ length (split xs).fst + 1 + (length (split xs).snd + 1) = length xs + 1 + 1
Tactic:
rw [Nat.add_assoc (length xs),
    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)]
Proof state after:
α : Type u_1
x y : α
xs : List α
ih : length (split xs).fst + length (split xs).snd = length xs
⊢ length (split xs).fst + length (split xs).snd + (1 + 1) = length xs + (1 + 1)
Theorem: List.length_split
Proof state before:
α : Type u_1
x y : α
xs : List α
ih : length (split xs).fst + length (split xs).snd = length xs
⊢ length (split xs).fst + length (split xs).snd + (1 + 1) = length xs + (1 + 1)
Tactic:
apply congrArg (λ x => x + (1 + 1))
Proof state after:
α : Type u_1
x y : α
xs : List α
ih : length (split xs).fst + length (split xs).snd = length xs
⊢ length (split xs).fst + length (split xs).snd = length xs
Theorem: List.length_split
Proof state before:
α : Type u_1
x y : α
xs : List α
ih : length (split xs).fst + length (split xs).snd = length xs
⊢ length (split xs).fst + length (split xs).snd = length xs
Tactic:
exact ih
Proof state after:
no goals
Theorem: List.length_mergeSortWith
Proof 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]
Proof 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
Theorem: List.length_mergeSortWith
Proof 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₂]
Proof 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
Theorem: List.length_mergeSortWith
Proof 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]
Proof 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
Theorem: List.length_mergeSortWith
Proof 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)]
Proof 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)
Theorem: List.length_mergeSortWith
Proof 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))
Proof 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
Theorem: List.length_mergeSortWith
Proof 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
Proof state after:
no goals
Theorem: Nat.sub_le_iff_left
Proof state before:
a b c : Nat
⊢ a - b ≤ c ↔ a ≤ b + c
Tactic:
apply Iff.intro
Proof state after:
case mp
a b c : Nat
⊢ a - b ≤ c → a ≤ b + c

case mpr
a b c : Nat
⊢ a ≤ b + c → a - b ≤ c
Theorem: Nat.sub_le_iff_left
Proof state before:
case mp
a b c : Nat
⊢ a - b ≤ c → a ≤ b + c

case mpr
a b c : Nat
⊢ a ≤ b + c → a - b ≤ c
Tactic:
. intros h
  rw [Nat.add_comm]
  apply Nat.le_add_of_sub_le
  exact h
Proof state after:
case mpr
a b c : Nat
⊢ a ≤ b + c → a - b ≤ c
Theorem: Nat.sub_le_iff_left
Proof state before:
case mpr
a b c : Nat
⊢ a ≤ b + c → a - b ≤ c
Tactic:
. intros h
  apply Nat.sub_le_of_le_add
  rw [Nat.add_comm]
  exact h
Proof state after:
no goals
Theorem: Nat.sub_le_iff_left
Proof state before:
case mp
a b c : Nat
⊢ a - b ≤ c → a ≤ b + c
Tactic:
intros h
Proof state after:
case mp
a b c : Nat
h : a - b ≤ c
⊢ a ≤ b + c
Theorem: Nat.sub_le_iff_left
Proof state before:
case mp
a b c : Nat
h : a - b ≤ c
⊢ a ≤ b + c
Tactic:
rw [Nat.add_comm]
Proof state after:
case mp
a b c : Nat
h : a - b ≤ c
⊢ a ≤ c + b
Theorem: Nat.sub_le_iff_left
Proof state before:
case mp
a b c : Nat
h : a - b ≤ c
⊢ a ≤ c + b
Tactic:
apply Nat.le_add_of_sub_le
Proof state after:
case mp.h
a b c : Nat
h : a - b ≤ c
⊢ a - b ≤ c
Theorem: Nat.sub_le_iff_left
Proof state before:
case mp.h
a b c : Nat
h : a - b ≤ c
⊢ a - b ≤ c
Tactic:
exact h
Proof state after:
no goals
Theorem: Nat.sub_le_iff_left
Proof state before:
case mpr
a b c : Nat
⊢ a ≤ b + c → a - b ≤ c
Tactic:
intros h
Proof state after:
case mpr
a b c : Nat
h : a ≤ b + c
⊢ a - b ≤ c
Theorem: Nat.sub_le_iff_left
Proof state before:
case mpr
a b c : Nat
h : a ≤ b + c
⊢ a - b ≤ c
Tactic:
apply Nat.sub_le_of_le_add
Proof state after:
case mpr.h
a b c : Nat
h : a ≤ b + c
⊢ a ≤ c + b
Theorem: Nat.sub_le_iff_left
Proof state before:
case mpr.h
a b c : Nat
h : a ≤ b + c
⊢ a ≤ c + b
Tactic:
rw [Nat.add_comm]
Proof state after:
case mpr.h
a b c : Nat
h : a ≤ b + c
⊢ a ≤ b + c
Theorem: Nat.sub_le_iff_left
Proof state before:
case mpr.h
a b c : Nat
h : a ≤ b + c
⊢ a ≤ b + c
Tactic:
exact h
Proof state after:
no goals
Theorem: Nat.sub_add_eq_sub_sub
Proof state before:
a b c : Nat
⊢ a - (b + c) = a - b - c
Tactic:
apply Nat.le_antisymm (Nat.sub_le_iff_left.mpr _)
                      (Nat.sub_le_iff_left.mpr $ Nat.sub_le_iff_left.mpr _)
Proof state after:
a b c : Nat
⊢ a ≤ b + c + (a - b - c)

a b c : Nat
⊢ a ≤ b + (c + (a - (b + c)))
Theorem: Nat.sub_add_eq_sub_sub
Proof state before:
a b c : Nat
⊢ a ≤ b + c + (a - b - c)

a b c : Nat
⊢ a ≤ b + (c + (a - (b + c)))
Tactic:
. rw [Nat.add_assoc]
  apply Nat.le_trans Nat.le_add_sub (Nat.add_le_add_left Nat.le_add_sub _)
Proof state after:
a b c : Nat
⊢ a ≤ b + (c + (a - (b + c)))
Theorem: Nat.sub_add_eq_sub_sub
Proof state before:
a b c : Nat
⊢ a ≤ b + (c + (a - (b + c)))
Tactic:
. rw [←Nat.add_assoc]
  apply Nat.le_add_sub
Proof state after:
no goals
Theorem: Nat.sub_add_eq_sub_sub
Proof state before:
a b c : Nat
⊢ a ≤ b + c + (a - b - c)
Tactic:
rw [Nat.add_assoc]
Proof state after:
a b c : Nat
⊢ a ≤ b + (c + (a - b - c))
Theorem: Nat.sub_add_eq_sub_sub
Proof state before:
a b c : Nat
⊢ a ≤ b + (c + (a - b - c))
Tactic:
apply Nat.le_trans Nat.le_add_sub (Nat.add_le_add_left Nat.le_add_sub _)
Proof state after:
no goals
Theorem: Nat.sub_add_eq_sub_sub
Proof state before:
a b c : Nat
⊢ a ≤ b + (c + (a - (b + c)))
Tactic:
rw [←Nat.add_assoc]
Proof state after:
a b c : Nat
⊢ a ≤ b + c + (a - (b + c))
Theorem: Nat.sub_add_eq_sub_sub
Proof state before:
a b c : Nat
⊢ a ≤ b + c + (a - (b + c))
Tactic:
apply Nat.le_add_sub
Proof state after:
no goals
Theorem: Nat.lt_of_sub_add
Proof state before:
⊢ ∀ (m k n : Nat), k < m → n > 0 → m - (k + n) < m - k
Tactic:
intros m k n hkm hn
Proof state after:
m k n : Nat
hkm : k < m
hn : n > 0
⊢ m - (k + n) < m - k
Theorem: Nat.lt_of_sub_add
Proof state before:
m k n : Nat
hkm : k < m
hn : n > 0
⊢ m - (k + n) < m - k
Tactic:
apply Nat.lt_of_le_of_lt (m := m - k - n)
Proof state after:
case h₁
m k n : Nat
hkm : k < m
hn : n > 0
⊢ m - (k + n) ≤ m - k - n

case h₂
m k n : Nat
hkm : k < m
hn : n > 0
⊢ m - k - n < m - k