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

State before:
α : Type u_1
inst✝ : DecidableEq α
xs : List α
⊢ ∀ (as : List α), length (uniqueAux xs as) ≤ length xs + length as
Tactic:
induction xs with
| nil => simp [uniqueAux]
| cons x xs ih =>
  intros as
  cases Decidable.em (x ∈ as) with
  | inl h =>
    simp only [length, uniqueAux, h, ite_true]
    apply Nat.le_trans
    apply ih
    rw [Nat.add_assoc, Nat.add_comm 1, ←Nat.add_assoc]
    apply Nat.le_step
    simp
  | inr h =>
    simp only [length, uniqueAux, h, ite_false]
    apply Nat.le_trans
    apply ih
    simp only [length]
    rw [Nat.add_comm _ 1, Nat.add_assoc]
    apply Nat.le_refl
State after:
no goals

State before:
case nil
α : Type u_1
inst✝ : DecidableEq α
⊢ ∀ (as : List α), length (uniqueAux [] as) ≤ length [] + length as
Tactic:
simp [uniqueAux]
State after:
no goals

State before:
case cons
α : Type u_1
inst✝ : DecidableEq α
x : α
xs : List α
ih : ∀ (as : List α), length (uniqueAux xs as) ≤ length xs + length as
⊢ ∀ (as : List α), length (uniqueAux (x :: xs) as) ≤ length (x :: xs) + length as
Tactic:
intros as
State after:
case cons
α : Type u_1
inst✝ : DecidableEq α
x : α
xs : List α
ih : ∀ (as : List α), length (uniqueAux xs as) ≤ length xs + length as
as : List α
⊢ length (uniqueAux (x :: xs) as) ≤ length (x :: xs) + length as

State before:
case cons
α : Type u_1
inst✝ : DecidableEq α
x : α
xs : List α
ih : ∀ (as : List α), length (uniqueAux xs as) ≤ length xs + length as
as : List α
⊢ length (uniqueAux (x :: xs) as) ≤ length (x :: xs) + length as
Tactic:
cases Decidable.em (x ∈ as) with
| inl h =>
  simp only [length, uniqueAux, h, ite_true]
  apply Nat.le_trans
  apply ih
  rw [Nat.add_assoc, Nat.add_comm 1, ←Nat.add_assoc]
  apply Nat.le_step
  simp
| inr h =>
  simp only [length, uniqueAux, h, ite_false]
  apply Nat.le_trans
  apply ih
  simp only [length]
  rw [Nat.add_comm _ 1, Nat.add_assoc]
  apply Nat.le_refl
State after:
no goals

State before:
case cons.inl
α : Type u_1
inst✝ : DecidableEq α
x : α
xs : List α
ih : ∀ (as : List α), length (uniqueAux xs as) ≤ length xs + length as
as : List α
h : x ∈ as
⊢ length (uniqueAux (x :: xs) as) ≤ length (x :: xs) + length as
Tactic:
simp only [length, uniqueAux, h, ite_true]
State after:
case cons.inl
α : Type u_1
inst✝ : DecidableEq α
x : α
xs : List α
ih : ∀ (as : List α), length (uniqueAux xs as) ≤ length xs + length as
as : List α
h : x ∈ as
⊢ length (uniqueAux xs as) ≤ length xs + 1 + length as

State before:
case cons.inl
α : Type u_1
inst✝ : DecidableEq α
x : α
xs : List α
ih : ∀ (as : List α), length (uniqueAux xs as) ≤ length xs + length as
as : List α
h : x ∈ as
⊢ length (uniqueAux xs as) ≤ length xs + 1 + length as
Tactic:
apply Nat.le_trans
State after:
case cons.inl.a
α : Type u_1
inst✝ : DecidableEq α
x : α
xs : List α
ih : ∀ (as : List α), length (uniqueAux xs as) ≤ length xs + length as
as : List α
h : x ∈ as
⊢ length (uniqueAux xs as) ≤ ?cons.inl.m

case cons.inl.a
α : Type u_1
inst✝ : DecidableEq α
x : α
xs : List α
ih : ∀ (as : List α), length (uniqueAux xs as) ≤ length xs + length as
as : List α
h : x ∈ as
⊢ ?cons.inl.m ≤ length xs + 1 + length as

case cons.inl.m
α : Type u_1
inst✝ : DecidableEq α
x : α
xs : List α
ih : ∀ (as : List α), length (uniqueAux xs as) ≤ length xs + length as
as : List α
h : x ∈ as
⊢ Nat

State before:
case cons.inl.a
α : Type u_1
inst✝ : DecidableEq α
x : α
xs : List α
ih : ∀ (as : List α), length (uniqueAux xs as) ≤ length xs + length as
as : List α
h : x ∈ as
⊢ length (uniqueAux xs as) ≤ ?cons.inl.m

case cons.inl.a
α : Type u_1
inst✝ : DecidableEq α
x : α
xs : List α
ih : ∀ (as : List α), length (uniqueAux xs as) ≤ length xs + length as
as : List α
h : x ∈ as
⊢ ?cons.inl.m ≤ length xs + 1 + length as

case cons.inl.m
α : Type u_1
inst✝ : DecidableEq α
x : α
xs : List α
ih : ∀ (as : List α), length (uniqueAux xs as) ≤ length xs + length as
as : List α
h : x ∈ as
⊢ Nat
Tactic:
apply ih
State after:
case cons.inl.a
α : Type u_1
inst✝ : DecidableEq α
x : α
xs : List α
ih : ∀ (as : List α), length (uniqueAux xs as) ≤ length xs + length as
as : List α
h : x ∈ as
⊢ length xs + length as ≤ length xs + 1 + length as

State before:
case cons.inl.a
α : Type u_1
inst✝ : DecidableEq α
x : α
xs : List α
ih : ∀ (as : List α), length (uniqueAux xs as) ≤ length xs + length as
as : List α
h : x ∈ as
⊢ length xs + length as ≤ length xs + 1 + length as
Tactic:
rw [Nat.add_assoc, Nat.add_comm 1, ←Nat.add_assoc]
State after:
case cons.inl.a
α : Type u_1
inst✝ : DecidableEq α
x : α
xs : List α
ih : ∀ (as : List α), length (uniqueAux xs as) ≤ length xs + length as
as : List α
h : x ∈ as
⊢ length xs + length as ≤ length xs + length as + 1

State before:
case cons.inl.a
α : Type u_1
inst✝ : DecidableEq α
x : α
xs : List α
ih : ∀ (as : List α), length (uniqueAux xs as) ≤ length xs + length as
as : List α
h : x ∈ as
⊢ length xs + length as ≤ length xs + length as + 1
Tactic:
apply Nat.le_step
State after:
case cons.inl.a.h
α : Type u_1
inst✝ : DecidableEq α
x : α
xs : List α
ih : ∀ (as : List α), length (uniqueAux xs as) ≤ length xs + length as
as : List α
h : x ∈ as
⊢ length xs + length as ≤ length xs + length as

State before:
case cons.inl.a.h
α : Type u_1
inst✝ : DecidableEq α
x : α
xs : List α
ih : ∀ (as : List α), length (uniqueAux xs as) ≤ length xs + length as
as : List α
h : x ∈ as
⊢ length xs + length as ≤ length xs + length as
Tactic:
simp
State after:
no goals

State before:
case cons.inr
α : Type u_1
inst✝ : DecidableEq α
x : α
xs : List α
ih : ∀ (as : List α), length (uniqueAux xs as) ≤ length xs + length as
as : List α
h : ¬x ∈ as
⊢ length (uniqueAux (x :: xs) as) ≤ length (x :: xs) + length as
Tactic:
simp only [length, uniqueAux, h, ite_false]
State after:
case cons.inr
α : Type u_1
inst✝ : DecidableEq α
x : α
xs : List α
ih : ∀ (as : List α), length (uniqueAux xs as) ≤ length xs + length as
as : List α
h : ¬x ∈ as
⊢ length (uniqueAux xs (x :: as)) ≤ length xs + 1 + length as

State before:
case cons.inr
α : Type u_1
inst✝ : DecidableEq α
x : α
xs : List α
ih : ∀ (as : List α), length (uniqueAux xs as) ≤ length xs + length as
as : List α
h : ¬x ∈ as
⊢ length (uniqueAux xs (x :: as)) ≤ length xs + 1 + length as
Tactic:
apply Nat.le_trans
State after:
case cons.inr.a
α : Type u_1
inst✝ : DecidableEq α
x : α
xs : List α
ih : ∀ (as : List α), length (uniqueAux xs as) ≤ length xs + length as
as : List α
h : ¬x ∈ as
⊢ length (uniqueAux xs (x :: as)) ≤ ?cons.inr.m

case cons.inr.a
α : Type u_1
inst✝ : DecidableEq α
x : α
xs : List α
ih : ∀ (as : List α), length (uniqueAux xs as) ≤ length xs + length as
as : List α
h : ¬x ∈ as
⊢ ?cons.inr.m ≤ length xs + 1 + length as

case cons.inr.m
α : Type u_1
inst✝ : DecidableEq α
x : α
xs : List α
ih : ∀ (as : List α), length (uniqueAux xs as) ≤ length xs + length as
as : List α
h : ¬x ∈ as
⊢ Nat

State before:
case cons.inr.a
α : Type u_1
inst✝ : DecidableEq α
x : α
xs : List α
ih : ∀ (as : List α), length (uniqueAux xs as) ≤ length xs + length as
as : List α
h : ¬x ∈ as
⊢ length (uniqueAux xs (x :: as)) ≤ ?cons.inr.m

case cons.inr.a
α : Type u_1
inst✝ : DecidableEq α
x : α
xs : List α
ih : ∀ (as : List α), length (uniqueAux xs as) ≤ length xs + length as
as : List α
h : ¬x ∈ as
⊢ ?cons.inr.m ≤ length xs + 1 + length as

case cons.inr.m
α : Type u_1
inst✝ : DecidableEq α
x : α
xs : List α
ih : ∀ (as : List α), length (uniqueAux xs as) ≤ length xs + length as
as : List α
h : ¬x ∈ as
⊢ Nat
Tactic:
apply ih
State after:
case cons.inr.a
α : Type u_1
inst✝ : DecidableEq α
x : α
xs : List α
ih : ∀ (as : List α), length (uniqueAux xs as) ≤ length xs + length as
as : List α
h : ¬x ∈ as
⊢ length xs + length (x :: as) ≤ length xs + 1 + length as

State before:
case cons.inr.a
α : Type u_1
inst✝ : DecidableEq α
x : α
xs : List α
ih : ∀ (as : List α), length (uniqueAux xs as) ≤ length xs + length as
as : List α
h : ¬x ∈ as
⊢ length xs + length (x :: as) ≤ length xs + 1 + length as
Tactic:
simp only [length]
State after:
case cons.inr.a
α : Type u_1
inst✝ : DecidableEq α
x : α
xs : List α
ih : ∀ (as : List α), length (uniqueAux xs as) ≤ length xs + length as
as : List α
h : ¬x ∈ as
⊢ length xs + (length as + 1) ≤ length xs + 1 + length as

State before:
case cons.inr.a
α : Type u_1
inst✝ : DecidableEq α
x : α
xs : List α
ih : ∀ (as : List α), length (uniqueAux xs as) ≤ length xs + length as
as : List α
h : ¬x ∈ as
⊢ length xs + (length as + 1) ≤ length xs + 1 + length as
Tactic:
rw [Nat.add_comm _ 1, Nat.add_assoc]
State after:
case cons.inr.a
α : Type u_1
inst✝ : DecidableEq α
x : α
xs : List α
ih : ∀ (as : List α), length (uniqueAux xs as) ≤ length xs + length as
as : List α
h : ¬x ∈ as
⊢ length xs + (1 + length as) ≤ length xs + (1 + length as)

State before:
case cons.inr.a
α : Type u_1
inst✝ : DecidableEq α
x : α
xs : List α
ih : ∀ (as : List α), length (uniqueAux xs as) ≤ length xs + length as
as : List α
h : ¬x ∈ as
⊢ length xs + (1 + length as) ≤ length xs + (1 + length as)
Tactic:
apply Nat.le_refl
State after:
no goals