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

State before:
α : Type u_1
cmp : α → α → Ordering
ys : List α
⊢ length (mergeWith cmp ([], ys)) = length [] + length ys
Tactic:
simp only [mergeWith, length, Nat.zero_add]
State after:
no goals

State before:
α : 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 (x :: xs, y :: ys)) = length (x :: xs) + length (y :: ys)
Tactic:
simp only [mergeWith]
State after:
α : 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 cmp x y with
      | Ordering.gt => y :: mergeWith cmp (ys, x :: xs)
      | x_1 => x :: mergeWith cmp (y :: ys, xs)) =
    length (x :: xs) + length (y :: ys)

State before:
α : 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 cmp x y with
      | Ordering.gt => y :: mergeWith cmp (ys, x :: xs)
      | x_1 => x :: mergeWith cmp (y :: ys, xs)) =
    length (x :: xs) + length (y :: ys)
Tactic:
cases cmp x y with
| lt =>
  simp only
  have h₁ : length (x :: mergeWith cmp (y :: ys, xs)) =
            length (mergeWith cmp (y :: ys, xs)) + 1 := rfl
  have h₂ : length (x :: xs) = length xs + 1 := rfl
  rw [h₁, h₂, Nat.add_comm (length xs + 1), ←Nat.add_assoc]
  apply congrArg (λ x => x + 1)
  exact ih₁
| eq =>
  simp only
  have h₁ : length (x :: mergeWith cmp (y :: ys, xs)) =
            length (mergeWith cmp (y :: ys, xs)) + 1 := rfl
  have h₂ : length (x :: xs) = length xs + 1 := rfl
  rw [h₁, h₂, Nat.add_comm (length xs + 1), ←Nat.add_assoc]
  apply congrArg (λ x => x + 1)
  exact ih₁
| gt =>
  simp only [length]
  simp only [length] at ih₂
  rw [←Nat.add_assoc]
  apply congrArg (λ x => x + 1)
  rw [Nat.add_comm]
  exact ih₂
State after:
no goals

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)
⊢ length
      (match Ordering.lt 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
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)
⊢ length (x :: mergeWith cmp (y :: ys, xs)) = length (x :: xs) + length (y :: ys)

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)
⊢ 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
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
⊢ length (x :: mergeWith cmp (y :: ys, xs)) = length (x :: xs) + length (y :: ys)

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
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)

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]
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

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)
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

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₁
State after:
no goals

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
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)

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
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)

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
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)

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]
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

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)
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

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₁
State after:
no goals

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]
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)

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₂
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)

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]
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

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)
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

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]
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)

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₂
State after:
no goals