α✝ : Type u
β✝ : α✝ → Type v
l l₁ l₂ : List (Sigma β✝)
inst✝² : DecidableEq α✝
α : Type u_1
β : α → Type u_2
inst✝¹ : DecidableEq α
inst✝ : SizeOf (Sigma β)
xs : List (Sigma β)
⊢ rec 1 (fun head tail tail_ih => 1 + sizeOf head + tail_ih) (dedupKeys xs) ≤
    rec 1 (fun head tail tail_ih => 1 + sizeOf head + tail_ih) xs
α✝ : Type u
β✝ : α✝ → Type v
l l₁ l₂ : List (Sigma β✝)
inst✝² : DecidableEq α✝
α : Type u_1
β : α → Type u_2
inst✝¹ : DecidableEq α
inst✝ : SizeOf (Sigma β)
xs : List (Sigma β)
⊢ sizeOf (dedupKeys xs) ≤ sizeOf xs
simp only [SizeOf.sizeOf, _sizeOf_1]
case nil
α✝ : Type u
β✝ : α✝ → Type v
l l₁ l₂ : List (Sigma β✝)
inst✝² : DecidableEq α✝
α : Type u_1
β : α → Type u_2
inst✝¹ : DecidableEq α
inst✝ : SizeOf (Sigma β)
⊢ rec 1 (fun head tail tail_ih => 1 + sizeOf head + tail_ih) (dedupKeys []) ≤
    rec 1 (fun head tail tail_ih => 1 + sizeOf head + tail_ih) []

case cons
α✝ : Type u
β✝ : α✝ → Type v
l l₁ l₂ : List (Sigma β✝)
inst✝² : DecidableEq α✝
α : Type u_1
β : α → Type u_2
inst✝¹ : DecidableEq α
inst✝ : SizeOf (Sigma β)
x : Sigma β
xs : List (Sigma β)
tail_ih✝ :
  rec 1 (fun head tail tail_ih => 1 + sizeOf head + tail_ih) (dedupKeys xs) ≤
    rec 1 (fun head tail tail_ih => 1 + sizeOf head + tail_ih) xs
⊢ rec 1 (fun head tail tail_ih => 1 + sizeOf head + tail_ih) (dedupKeys (x :: xs)) ≤
    rec 1 (fun head tail tail_ih => 1 + sizeOf head + tail_ih) (x :: xs)
α✝ : Type u
β✝ : α✝ → Type v
l l₁ l₂ : List (Sigma β✝)
inst✝² : DecidableEq α✝
α : Type u_1
β : α → Type u_2
inst✝¹ : DecidableEq α
inst✝ : SizeOf (Sigma β)
xs : List (Sigma β)
⊢ rec 1 (fun head tail tail_ih => 1 + sizeOf head + tail_ih) (dedupKeys xs) ≤
    rec 1 (fun head tail tail_ih => 1 + sizeOf head + tail_ih) xs
induction' xs with x xs
no goals
case nil
α✝ : Type u
β✝ : α✝ → Type v
l l₁ l₂ : List (Sigma β✝)
inst✝² : DecidableEq α✝
α : Type u_1
β : α → Type u_2
inst✝¹ : DecidableEq α
inst✝ : SizeOf (Sigma β)
⊢ rec 1 (fun head tail tail_ih => 1 + sizeOf head + tail_ih) (dedupKeys []) ≤
    rec 1 (fun head tail tail_ih => 1 + sizeOf head + tail_ih) []
simp [dedupKeys]
case cons
α✝ : Type u
β✝ : α✝ → Type v
l l₁ l₂ : List (Sigma β✝)
inst✝² : DecidableEq α✝
α : Type u_1
β : α → Type u_2
inst✝¹ : DecidableEq α
inst✝ : SizeOf (Sigma β)
x : Sigma β
xs : List (Sigma β)
tail_ih✝ :
  rec 1 (fun head tail tail_ih => 1 + sizeOf head + tail_ih) (dedupKeys xs) ≤
    rec 1 (fun head tail tail_ih => 1 + sizeOf head + tail_ih) xs
⊢ rec 1 (fun head tail tail_ih => 1 + sizeOf head + tail_ih) (kerase x.fst (dedupKeys xs)) ≤
    rec 1 (fun head tail tail_ih => 1 + sizeOf head + tail_ih) xs
case cons
α✝ : Type u
β✝ : α✝ → Type v
l l₁ l₂ : List (Sigma β✝)
inst✝² : DecidableEq α✝
α : Type u_1
β : α → Type u_2
inst✝¹ : DecidableEq α
inst✝ : SizeOf (Sigma β)
x : Sigma β
xs : List (Sigma β)
tail_ih✝ :
  rec 1 (fun head tail tail_ih => 1 + sizeOf head + tail_ih) (dedupKeys xs) ≤
    rec 1 (fun head tail tail_ih => 1 + sizeOf head + tail_ih) xs
⊢ rec 1 (fun head tail tail_ih => 1 + sizeOf head + tail_ih) (dedupKeys (x :: xs)) ≤
    rec 1 (fun head tail tail_ih => 1 + sizeOf head + tail_ih) (x :: xs)
simp only [dedupKeys_cons, kinsert_def, add_le_add_iff_left, Sigma.eta]
α✝ : Type u
β✝ : α✝ → Type v
l l₁ l₂ : List (Sigma β✝)
inst✝² : DecidableEq α✝
α : Type u_1
β : α → Type u_2
inst✝¹ : DecidableEq α
inst✝ : SizeOf (Sigma β)
x : Sigma β
xs : List (Sigma β)
tail_ih✝ :
  rec 1 (fun head tail tail_ih => 1 + sizeOf head + tail_ih) (dedupKeys xs) ≤
    rec 1 (fun head tail tail_ih => 1 + sizeOf head + tail_ih) xs
⊢ rec 1 (fun head tail tail_ih => 1 + sizeOf head + tail_ih) (kerase x.fst (dedupKeys xs)) ≤ ?m.358104

α✝ : Type u
β✝ : α✝ → Type v
l l₁ l₂ : List (Sigma β✝)
inst✝² : DecidableEq α✝
α : Type u_1
β : α → Type u_2
inst✝¹ : DecidableEq α
inst✝ : SizeOf (Sigma β)
x : Sigma β
xs : List (Sigma β)
tail_ih✝ :
  rec 1 (fun head tail tail_ih => 1 + sizeOf head + tail_ih) (dedupKeys xs) ≤
    rec 1 (fun head tail tail_ih => 1 + sizeOf head + tail_ih) xs
⊢ ?m.358104 ≤ rec 1 (fun head tail tail_ih => 1 + sizeOf head + tail_ih) xs

α✝ : Type u
β✝ : α✝ → Type v
l l₁ l₂ : List (Sigma β✝)
inst✝² : DecidableEq α✝
α : Type u_1
β : α → Type u_2
inst✝¹ : DecidableEq α
inst✝ : SizeOf (Sigma β)
x : Sigma β
xs : List (Sigma β)
tail_ih✝ :
  rec 1 (fun head tail tail_ih => 1 + sizeOf head + tail_ih) (dedupKeys xs) ≤
    rec 1 (fun head tail tail_ih => 1 + sizeOf head + tail_ih) xs
⊢ ℕ
case cons
α✝ : Type u
β✝ : α✝ → Type v
l l₁ l₂ : List (Sigma β✝)
inst✝² : DecidableEq α✝
α : Type u_1
β : α → Type u_2
inst✝¹ : DecidableEq α
inst✝ : SizeOf (Sigma β)
x : Sigma β
xs : List (Sigma β)
tail_ih✝ :
  rec 1 (fun head tail tail_ih => 1 + sizeOf head + tail_ih) (dedupKeys xs) ≤
    rec 1 (fun head tail tail_ih => 1 + sizeOf head + tail_ih) xs
⊢ rec 1 (fun head tail tail_ih => 1 + sizeOf head + tail_ih) (kerase x.fst (dedupKeys xs)) ≤
    rec 1 (fun head tail tail_ih => 1 + sizeOf head + tail_ih) xs
trans
α✝ : Type u
β✝ : α✝ → Type v
l l₁ l₂ : List (Sigma β✝)
inst✝² : DecidableEq α✝
α : Type u_1
β : α → Type u_2
inst✝¹ : DecidableEq α
inst✝ : SizeOf (Sigma β)
x : Sigma β
xs : List (Sigma β)
tail_ih✝ :
  rec 1 (fun head tail tail_ih => 1 + sizeOf head + tail_ih) (dedupKeys xs) ≤
    rec 1 (fun head tail tail_ih => 1 + sizeOf head + tail_ih) xs
⊢ sizeOf (dedupKeys xs) ≤ rec 1 (fun head tail tail_ih => 1 + sizeOf head + tail_ih) xs
α✝ : Type u
β✝ : α✝ → Type v
l l₁ l₂ : List (Sigma β✝)
inst✝² : DecidableEq α✝
α : Type u_1
β : α → Type u_2
inst✝¹ : DecidableEq α
inst✝ : SizeOf (Sigma β)
x : Sigma β
xs : List (Sigma β)
tail_ih✝ :
  rec 1 (fun head tail tail_ih => 1 + sizeOf head + tail_ih) (dedupKeys xs) ≤
    rec 1 (fun head tail tail_ih => 1 + sizeOf head + tail_ih) xs
⊢ rec 1 (fun head tail tail_ih => 1 + sizeOf head + tail_ih) (kerase x.fst (dedupKeys xs)) ≤ ?m.358104

α✝ : Type u
β✝ : α✝ → Type v
l l₁ l₂ : List (Sigma β✝)
inst✝² : DecidableEq α✝
α : Type u_1
β : α → Type u_2
inst✝¹ : DecidableEq α
inst✝ : SizeOf (Sigma β)
x : Sigma β
xs : List (Sigma β)
tail_ih✝ :
  rec 1 (fun head tail tail_ih => 1 + sizeOf head + tail_ih) (dedupKeys xs) ≤
    rec 1 (fun head tail tail_ih => 1 + sizeOf head + tail_ih) xs
⊢ ?m.358104 ≤ rec 1 (fun head tail tail_ih => 1 + sizeOf head + tail_ih) xs

α✝ : Type u
β✝ : α✝ → Type v
l l₁ l₂ : List (Sigma β✝)
inst✝² : DecidableEq α✝
α : Type u_1
β : α → Type u_2
inst✝¹ : DecidableEq α
inst✝ : SizeOf (Sigma β)
x : Sigma β
xs : List (Sigma β)
tail_ih✝ :
  rec 1 (fun head tail tail_ih => 1 + sizeOf head + tail_ih) (dedupKeys xs) ≤
    rec 1 (fun head tail tail_ih => 1 + sizeOf head + tail_ih) xs
⊢ ℕ
apply sizeOf_kerase
no goals
α✝ : Type u
β✝ : α✝ → Type v
l l₁ l₂ : List (Sigma β✝)
inst✝² : DecidableEq α✝
α : Type u_1
β : α → Type u_2
inst✝¹ : DecidableEq α
inst✝ : SizeOf (Sigma β)
x : Sigma β
xs : List (Sigma β)
tail_ih✝ :
  rec 1 (fun head tail tail_ih => 1 + sizeOf head + tail_ih) (dedupKeys xs) ≤
    rec 1 (fun head tail tail_ih => 1 + sizeOf head + tail_ih) xs
⊢ sizeOf (dedupKeys xs) ≤ rec 1 (fun head tail tail_ih => 1 + sizeOf head + tail_ih) xs
assumption