Theorem: List.sizeOf_getRest (One.lean)

State before:
α : Type u_1
inst✝ : DecidableEq α
l l₁ l₂ : List α
h : getRest l l₁ = some l₂
⊢ sizeOf l₂ = 1 + sizeOf l - sizeOf l₁
Tactic:
induction l generalizing l₁ l₂ with
| nil => 
  unfold getRest at h
  cases l₁
  . simp only [Option.some.injEq] at h
    subst h
    simp only [nil.sizeOf_spec, add_tsub_cancel_right, ge_iff_le]
  . simp only at h
| cons head tail ih =>
  unfold getRest at h
  split at h <;> try contradiction
  case h_1 heq => injection h; simp_all only [tsub_le_iff_right, ge_iff_le, nil.sizeOf_spec, add_tsub_cancel_left, add_le_iff_nonpos_right,
     nonpos_iff_eq_zero, zero_le]
  case h_3 heq =>
    split at h <;> try contradiction
    case inl heq₂ =>
      injection heq
      subst_vars
      simp only [ih h, tsub_le_iff_right, ge_iff_le, cons.sizeOf_spec, sizeOf_default, add_zero, zero_le,
        nonpos_iff_eq_zero, Nat.add_sub_add_left, add_le_add_iff_left]
State after:
no goals

State before:
case nil
α : Type u_1
inst✝ : DecidableEq α
l₁ l₂ : List α
h : getRest [] l₁ = some l₂
⊢ sizeOf l₂ = 1 + sizeOf [] - sizeOf l₁
Tactic:
unfold getRest at h
State after:
case nil
α : Type u_1
inst✝ : DecidableEq α
l₁ l₂ : List α
h :
  (match [], l₁ with
    | l, [] => some l
    | [], x => none
    | x :: l, y :: l₁ => if x = y then getRest l l₁ else none) =
    some l₂
⊢ sizeOf l₂ = 1 + sizeOf [] - sizeOf l₁

State before:
case nil
α : Type u_1
inst✝ : DecidableEq α
l₁ l₂ : List α
h :
  (match [], l₁ with
    | l, [] => some l
    | [], x => none
    | x :: l, y :: l₁ => if x = y then getRest l l₁ else none) =
    some l₂
⊢ sizeOf l₂ = 1 + sizeOf [] - sizeOf l₁
Tactic:
cases l₁
State after:
case nil.nil
α : Type u_1
inst✝ : DecidableEq α
l₂ : List α
h :
  (match [], [] with
    | l, [] => some l
    | [], x => none
    | x :: l, y :: l₁ => if x = y then getRest l l₁ else none) =
    some l₂
⊢ sizeOf l₂ = 1 + sizeOf [] - sizeOf []

case nil.cons
α : Type u_1
inst✝ : DecidableEq α
l₂ : List α
head✝ : α
tail✝ : List α
h :
  (match [], head✝ :: tail✝ with
    | l, [] => some l
    | [], x => none
    | x :: l, y :: l₁ => if x = y then getRest l l₁ else none) =
    some l₂
⊢ sizeOf l₂ = 1 + sizeOf [] - sizeOf (head✝ :: tail✝)

State before:
case nil.nil
α : Type u_1
inst✝ : DecidableEq α
l₂ : List α
h :
  (match [], [] with
    | l, [] => some l
    | [], x => none
    | x :: l, y :: l₁ => if x = y then getRest l l₁ else none) =
    some l₂
⊢ sizeOf l₂ = 1 + sizeOf [] - sizeOf []

case nil.cons
α : Type u_1
inst✝ : DecidableEq α
l₂ : List α
head✝ : α
tail✝ : List α
h :
  (match [], head✝ :: tail✝ with
    | l, [] => some l
    | [], x => none
    | x :: l, y :: l₁ => if x = y then getRest l l₁ else none) =
    some l₂
⊢ sizeOf l₂ = 1 + sizeOf [] - sizeOf (head✝ :: tail✝)
Tactic:
. simp only [Option.some.injEq] at h
  subst h
  simp only [nil.sizeOf_spec, add_tsub_cancel_right, ge_iff_le]
State after:
case nil.cons
α : Type u_1
inst✝ : DecidableEq α
l₂ : List α
head✝ : α
tail✝ : List α
h :
  (match [], head✝ :: tail✝ with
    | l, [] => some l
    | [], x => none
    | x :: l, y :: l₁ => if x = y then getRest l l₁ else none) =
    some l₂
⊢ sizeOf l₂ = 1 + sizeOf [] - sizeOf (head✝ :: tail✝)

State before:
case nil.cons
α : Type u_1
inst✝ : DecidableEq α
l₂ : List α
head✝ : α
tail✝ : List α
h :
  (match [], head✝ :: tail✝ with
    | l, [] => some l
    | [], x => none
    | x :: l, y :: l₁ => if x = y then getRest l l₁ else none) =
    some l₂
⊢ sizeOf l₂ = 1 + sizeOf [] - sizeOf (head✝ :: tail✝)
Tactic:
. simp only at h
State after:
no goals

State before:
case cons
α : Type u_1
inst✝ : DecidableEq α
head : α
tail : List α
ih : ∀ {l₁ l₂ : List α}, getRest tail l₁ = some l₂ → sizeOf l₂ = 1 + sizeOf tail - sizeOf l₁
l₁ l₂ : List α
h : getRest (head :: tail) l₁ = some l₂
⊢ sizeOf l₂ = 1 + sizeOf (head :: tail) - sizeOf l₁
Tactic:
unfold getRest at h
State after:
case cons
α : Type u_1
inst✝ : DecidableEq α
head : α
tail : List α
ih : ∀ {l₁ l₂ : List α}, getRest tail l₁ = some l₂ → sizeOf l₂ = 1 + sizeOf tail - sizeOf l₁
l₁ l₂ : List α
h :
  (match head :: tail, l₁ with
    | l, [] => some l
    | [], x => none
    | x :: l, y :: l₁ => if x = y then getRest l l₁ else none) =
    some l₂
⊢ sizeOf l₂ = 1 + sizeOf (head :: tail) - sizeOf l₁

State before:
case cons
α : Type u_1
inst✝ : DecidableEq α
head : α
tail : List α
ih : ∀ {l₁ l₂ : List α}, getRest tail l₁ = some l₂ → sizeOf l₂ = 1 + sizeOf tail - sizeOf l₁
l₁ l₂ : List α
h :
  (match head :: tail, l₁ with
    | l, [] => some l
    | [], x => none
    | x :: l, y :: l₁ => if x = y then getRest l l₁ else none) =
    some l₂
⊢ sizeOf l₂ = 1 + sizeOf (head :: tail) - sizeOf l₁
Tactic:
split at h <;> try contradiction
State after:
case cons.h_1
α : Type u_1
inst✝ : DecidableEq α
head : α
tail : List α
ih : ∀ {l₁ l₂ : List α}, getRest tail l₁ = some l₂ → sizeOf l₂ = 1 + sizeOf tail - sizeOf l₁
l₂ x✝¹ x✝ : List α
h : some (head :: tail) = some l₂
⊢ sizeOf l₂ = 1 + sizeOf (head :: tail) - sizeOf []

case cons.h_3
α : Type u_1
inst✝ : DecidableEq α
head : α
tail : List α
ih : ∀ {l₁ l₂ : List α}, getRest tail l₁ = some l₂ → sizeOf l₂ = 1 + sizeOf tail - sizeOf l₁
l₂ x✝² x✝¹ : List α
x✝ : α
l✝ : List α
y✝ : α
l₁✝ : List α
heq✝ : head :: tail = x✝ :: l✝
h : (if x✝ = y✝ then getRest l✝ l₁✝ else none) = some l₂
⊢ sizeOf l₂ = 1 + sizeOf (head :: tail) - sizeOf (y✝ :: l₁✝)

State before:
α : Type u_1
inst✝ : DecidableEq α
head : α
tail : List α
ih : ∀ {l₁ l₂ : List α}, getRest tail l₁ = some l₂ → sizeOf l₂ = 1 + sizeOf tail - sizeOf l₁
l₂ x✝ heq : List α
h : some (head :: tail) = some l₂
⊢ sizeOf l₂ = 1 + sizeOf (head :: tail) - sizeOf []
Tactic:
case h_1 heq => injection h; simp_all only [tsub_le_iff_right, ge_iff_le, nil.sizeOf_spec, add_tsub_cancel_left, add_le_iff_nonpos_right,
   nonpos_iff_eq_zero, zero_le]
State after:
no goals

State before:
α : Type u_1
inst✝ : DecidableEq α
head : α
tail : List α
ih : ∀ {l₁ l₂ : List α}, getRest tail l₁ = some l₂ → sizeOf l₂ = 1 + sizeOf tail - sizeOf l₁
l₂ x✝² x✝¹ : List α
x✝ : α
l✝ : List α
y✝ : α
l₁✝ : List α
heq : head :: tail = x✝ :: l✝
h : (if x✝ = y✝ then getRest l✝ l₁✝ else none) = some l₂
⊢ sizeOf l₂ = 1 + sizeOf (head :: tail) - sizeOf (y✝ :: l₁✝)
Tactic:
case h_3 heq =>
  split at h <;> try contradiction
  case inl heq₂ =>
    injection heq
    subst_vars
    simp only [ih h, tsub_le_iff_right, ge_iff_le, cons.sizeOf_spec, sizeOf_default, add_zero, zero_le,
      nonpos_iff_eq_zero, Nat.add_sub_add_left, add_le_add_iff_left]
State after:
no goals

State before:
case cons.h_2
α : Type u_1
inst✝ : DecidableEq α
head : α
tail : List α
ih : ∀ {l₁ l₂ : List α}, getRest tail l₁ = some l₂ → sizeOf l₂ = 1 + sizeOf tail - sizeOf l₁
l₂ x✝³ x✝² x✝¹ : List α
heq✝ : head :: tail = []
x✝ : x✝³ = [] → False
h : none = some l₂
⊢ sizeOf l₂ = 1 + sizeOf (head :: tail) - sizeOf x✝³
Tactic:
contradiction
State after:
no goals

State before:
α : Type u_1
inst✝ : DecidableEq α
head : α
tail : List α
ih : ∀ {l₁ l₂ : List α}, getRest tail l₁ = some l₂ → sizeOf l₂ = 1 + sizeOf tail - sizeOf l₁
l₂ x✝ heq : List α
h : some (head :: tail) = some l₂
⊢ sizeOf l₂ = 1 + sizeOf (head :: tail) - sizeOf []
Tactic:
injection h
State after:
α : Type u_1
inst✝ : DecidableEq α
head : α
tail : List α
ih : ∀ {l₁ l₂ : List α}, getRest tail l₁ = some l₂ → sizeOf l₂ = 1 + sizeOf tail - sizeOf l₁
l₂ x✝ heq : List α
val_eq✝ : head :: tail = l₂
⊢ sizeOf l₂ = 1 + sizeOf (head :: tail) - sizeOf []

State before:
α : Type u_1
inst✝ : DecidableEq α
head : α
tail : List α
ih : ∀ {l₁ l₂ : List α}, getRest tail l₁ = some l₂ → sizeOf l₂ = 1 + sizeOf tail - sizeOf l₁
l₂ x✝ heq : List α
val_eq✝ : head :: tail = l₂
⊢ sizeOf l₂ = 1 + sizeOf (head :: tail) - sizeOf []
Tactic:
simp_all only [tsub_le_iff_right, ge_iff_le, nil.sizeOf_spec, add_tsub_cancel_left, add_le_iff_nonpos_right,
nonpos_iff_eq_zero, zero_le]
State after:
no goals

State before:
α : Type u_1
inst✝ : DecidableEq α
head : α
tail : List α
ih : ∀ {l₁ l₂ : List α}, getRest tail l₁ = some l₂ → sizeOf l₂ = 1 + sizeOf tail - sizeOf l₁
l₂ x✝² x✝¹ : List α
x✝ : α
l✝ : List α
y✝ : α
l₁✝ : List α
heq : head :: tail = x✝ :: l✝
h : (if x✝ = y✝ then getRest l✝ l₁✝ else none) = some l₂
⊢ sizeOf l₂ = 1 + sizeOf (head :: tail) - sizeOf (y✝ :: l₁✝)
Tactic:
split at h <;> try contradiction
State after:
case inl
α : Type u_1
inst✝ : DecidableEq α
head : α
tail : List α
ih : ∀ {l₁ l₂ : List α}, getRest tail l₁ = some l₂ → sizeOf l₂ = 1 + sizeOf tail - sizeOf l₁
l₂ x✝² x✝¹ : List α
x✝ : α
l✝ : List α
y✝ : α
l₁✝ : List α
heq : head :: tail = x✝ :: l✝
h✝ : x✝ = y✝
h : getRest l✝ l₁✝ = some l₂
⊢ sizeOf l₂ = 1 + sizeOf (head :: tail) - sizeOf (y✝ :: l₁✝)

State before:
α : Type u_1
inst✝ : DecidableEq α
head : α
tail : List α
ih : ∀ {l₁ l₂ : List α}, getRest tail l₁ = some l₂ → sizeOf l₂ = 1 + sizeOf tail - sizeOf l₁
l₂ x✝² x✝¹ : List α
x✝ : α
l✝ : List α
y✝ : α
l₁✝ : List α
heq : head :: tail = x✝ :: l✝
heq₂ : x✝ = y✝
h : getRest l✝ l₁✝ = some l₂
⊢ sizeOf l₂ = 1 + sizeOf (head :: tail) - sizeOf (y✝ :: l₁✝)
Tactic:
case inl heq₂ =>
  injection heq
  subst_vars
  simp only [ih h, tsub_le_iff_right, ge_iff_le, cons.sizeOf_spec, sizeOf_default, add_zero, zero_le,
    nonpos_iff_eq_zero, Nat.add_sub_add_left, add_le_add_iff_left]
State after:
no goals

State before:
case inr
α : Type u_1
inst✝ : DecidableEq α
head : α
tail : List α
ih : ∀ {l₁ l₂ : List α}, getRest tail l₁ = some l₂ → sizeOf l₂ = 1 + sizeOf tail - sizeOf l₁
l₂ x✝² x✝¹ : List α
x✝ : α
l✝ : List α
y✝ : α
l₁✝ : List α
heq : head :: tail = x✝ :: l✝
h✝ : ¬x✝ = y✝
h : False
⊢ sizeOf l₂ = 1 + sizeOf (head :: tail) - sizeOf (y✝ :: l₁✝)
Tactic:
contradiction
State after:
no goals

State before:
α : Type u_1
inst✝ : DecidableEq α
head : α
tail : List α
ih : ∀ {l₁ l₂ : List α}, getRest tail l₁ = some l₂ → sizeOf l₂ = 1 + sizeOf tail - sizeOf l₁
l₂ x✝² x✝¹ : List α
x✝ : α
l✝ : List α
y✝ : α
l₁✝ : List α
heq : head :: tail = x✝ :: l✝
heq₂ : x✝ = y✝
h : getRest l✝ l₁✝ = some l₂
⊢ sizeOf l₂ = 1 + sizeOf (head :: tail) - sizeOf (y✝ :: l₁✝)
Tactic:
injection heq
State after:
α : Type u_1
inst✝ : DecidableEq α
head : α
tail : List α
ih : ∀ {l₁ l₂ : List α}, getRest tail l₁ = some l₂ → sizeOf l₂ = 1 + sizeOf tail - sizeOf l₁
l₂ x✝² x✝¹ : List α
x✝ : α
l✝ : List α
y✝ : α
l₁✝ : List α
heq₂ : x✝ = y✝
h : getRest l✝ l₁✝ = some l₂
head_eq✝ : head = x✝
tail_eq✝ : tail = l✝
⊢ sizeOf l₂ = 1 + sizeOf (head :: tail) - sizeOf (y✝ :: l₁✝)

State before:
α : Type u_1
inst✝ : DecidableEq α
head : α
tail : List α
ih : ∀ {l₁ l₂ : List α}, getRest tail l₁ = some l₂ → sizeOf l₂ = 1 + sizeOf tail - sizeOf l₁
l₂ x✝² x✝¹ : List α
x✝ : α
l✝ : List α
y✝ : α
l₁✝ : List α
heq₂ : x✝ = y✝
h : getRest l✝ l₁✝ = some l₂
head_eq✝ : head = x✝
tail_eq✝ : tail = l✝
⊢ sizeOf l₂ = 1 + sizeOf (head :: tail) - sizeOf (y✝ :: l₁✝)
Tactic:
subst_vars
State after:
α : Type u_1
inst✝ : DecidableEq α
l₂ x✝¹ x✝ l✝ : List α
y✝ : α
l₁✝ : List α
h : getRest l✝ l₁✝ = some l₂
ih : ∀ {l₁ l₂ : List α}, getRest l✝ l₁ = some l₂ → sizeOf l₂ = 1 + sizeOf l✝ - sizeOf l₁
⊢ sizeOf l₂ = 1 + sizeOf (y✝ :: l✝) - sizeOf (y✝ :: l₁✝)

State before:
α : Type u_1
inst✝ : DecidableEq α
l₂ x✝¹ x✝ l✝ : List α
y✝ : α
l₁✝ : List α
h : getRest l✝ l₁✝ = some l₂
ih : ∀ {l₁ l₂ : List α}, getRest l✝ l₁ = some l₂ → sizeOf l₂ = 1 + sizeOf l✝ - sizeOf l₁
⊢ sizeOf l₂ = 1 + sizeOf (y✝ :: l✝) - sizeOf (y✝ :: l₁✝)
Tactic:
simp only [ih h, tsub_le_iff_right, ge_iff_le, cons.sizeOf_spec, sizeOf_default, add_zero, zero_le,
  nonpos_iff_eq_zero, Nat.add_sub_add_left, add_le_add_iff_left]
State after:
no goals