-- Mathlib/Data/List/Sigma.lean
theorem sizeOf_dedupKeys [SizeOf (Sigma β)]
    (xs : List (Sigma β)) : SizeOf.sizeOf (dedupKeys xs) ≤ SizeOf.sizeOf xs

Proof state:
α : Type u
β : α → Type v
inst✝¹ : DecidableEq α
inst✝ : SizeOf (Sigma β)
xs : List (Sigma β)
⊢ rec 1 (fun head tail tail_ih => 1 + sizeOf head + tail_ih) xs.dedupKeys ≤
    rec 1 (fun head tail tail_ih => 1 + sizeOf head + tail_ih) xs

Tactic:
induction' xs with x xs

Result:
case nil
α : Type u
β : α → Type v
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
inst✝¹ : DecidableEq α
inst✝ : SizeOf (Sigma β)
x : Sigma β
xs : List (Sigma β)
tail_ih✝ :
  rec 1 (fun head tail tail_ih => 1 + sizeOf head + tail_ih) xs.dedupKeys ≤
    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) (x :: xs).dedupKeys ≤
    rec 1 (fun head tail tail_ih => 1 + sizeOf head + tail_ih) (x :: xs)

Proof state:
case cons
α : Type u
β : α → Type v
inst✝¹ : DecidableEq α
inst✝ : SizeOf (Sigma β)
x : Sigma β
xs : List (Sigma β)
tail_ih✝ :
  rec 1 (fun head tail tail_ih => 1 + sizeOf head + tail_ih) xs.dedupKeys ≤
    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) (x :: xs).dedupKeys ≤
    rec 1 (fun head tail tail_ih => 1 + sizeOf head + tail_ih) (x :: xs)

Tactic:
simp only [dedupKeys_cons, kinsert_def, Nat.add_le_add_iff_left, Sigma.eta]

Result:
case cons
α : Type u
β : α → Type v
inst✝¹ : DecidableEq α
inst✝ : SizeOf (Sigma β)
x : Sigma β
xs : List (Sigma β)
tail_ih✝ :
  rec 1 (fun head tail tail_ih => 1 + sizeOf head + tail_ih) xs.dedupKeys ≤
    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 xs.dedupKeys) ≤
    rec 1 (fun head tail tail_ih => 1 + sizeOf head + tail_ih) xs

Proof state:
α : Type u
β : α → Type v
inst✝¹ : DecidableEq α
inst✝ : SizeOf (Sigma β)
x : Sigma β
xs : List (Sigma β)
tail_ih✝ :
  rec 1 (fun head tail tail_ih => 1 + sizeOf head + tail_ih) xs.dedupKeys ≤
    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 xs.dedupKeys) ≤ ?m.97968

Tactic:
apply sizeOf_kerase

Result:
no goals

Proof state:
case cons
α : Type u
β : α → Type v
inst✝¹ : DecidableEq α
inst✝ : SizeOf (Sigma β)
x : Sigma β
xs : List (Sigma β)
tail_ih✝ :
  rec 1 (fun head tail tail_ih => 1 + sizeOf head + tail_ih) xs.dedupKeys ≤
    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 xs.dedupKeys) ≤
    rec 1 (fun head tail tail_ih => 1 + sizeOf head + tail_ih) xs

Tactic:
trans

Result:
α : Type u
β : α → Type v
inst✝¹ : DecidableEq α
inst✝ : SizeOf (Sigma β)
x : Sigma β
xs : List (Sigma β)
tail_ih✝ :
  rec 1 (fun head tail tail_ih => 1 + sizeOf head + tail_ih) xs.dedupKeys ≤
    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 xs.dedupKeys) ≤ ?m.97968

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

α : Type u
β : α → Type v
inst✝¹ : DecidableEq α
inst✝ : SizeOf (Sigma β)
x : Sigma β
xs : List (Sigma β)
tail_ih✝ :
  rec 1 (fun head tail tail_ih => 1 + sizeOf head + tail_ih) xs.dedupKeys ≤
    rec 1 (fun head tail tail_ih => 1 + sizeOf head + tail_ih) xs
⊢ ℕ

Proof state:
α : Type u
β : α → Type v
inst✝¹ : DecidableEq α
inst✝ : SizeOf (Sigma β)
xs : List (Sigma β)
⊢ sizeOf xs.dedupKeys ≤ sizeOf xs

Tactic:
simp only [SizeOf.sizeOf, _sizeOf_1]

Result:
α : Type u
β : α → Type v
inst✝¹ : DecidableEq α
inst✝ : SizeOf (Sigma β)
xs : List (Sigma β)
⊢ rec 1 (fun head tail tail_ih => 1 + sizeOf head + tail_ih) xs.dedupKeys ≤
    rec 1 (fun head tail tail_ih => 1 + sizeOf head + tail_ih) xs

Proof state:
case nil
α : Type u
β : α → Type v
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) []

Tactic:
simp [dedupKeys]

Result:
no goals

Proof state:
α : Type u
β : α → Type v
inst✝¹ : DecidableEq α
inst✝ : SizeOf (Sigma β)
x : Sigma β
xs : List (Sigma β)
tail_ih✝ :
  rec 1 (fun head tail tail_ih => 1 + sizeOf head + tail_ih) xs.dedupKeys ≤
    rec 1 (fun head tail tail_ih => 1 + sizeOf head + tail_ih) xs
⊢ sizeOf xs.dedupKeys ≤ rec 1 (fun head tail tail_ih => 1 + sizeOf head + tail_ih) xs

Tactic:
assumption

Result:
no goals