internlm/Lean-Github huggingface dataset:
Theorem: List.eq_append_of_getRest
Proof state before:
case nil
α : Type u_1
inst✝ : DecidableEq α
l l₂ : List α
P : l = l₂
⊢ l = [] ++ l₂
Tactic:
simp only [P, nil_append]
Proof state after:
no goals
Theorem: List.eq_append_of_getRest
Proof state before:
case cons
α : Type u_1
inst✝ : DecidableEq α
head : α
tail : List α
ih : ∀ {l l₂ : List α}, getRest l tail = some l₂ → l = tail ++ l₂
l l₂ : List α
P : getRest l (head :: tail) = some l₂
⊢ l = head :: tail ++ l₂
Tactic:
unfold getRest at P
Proof state after:
case cons
α : Type u_1
inst✝ : DecidableEq α
head : α
tail : List α
ih : ∀ {l l₂ : List α}, getRest l tail = some l₂ → l = tail ++ l₂
l l₂ : List α
P :
  (match l, head :: tail with
    | l, [] => some l
    | [], x => none
    | x :: l, y :: l₁ => if x = y then getRest l l₁ else none) =
    some l₂
⊢ l = head :: tail ++ l₂
Theorem: List.eq_append_of_getRest
Proof state before:
case cons
α : Type u_1
inst✝ : DecidableEq α
head : α
tail : List α
ih : ∀ {l l₂ : List α}, getRest l tail = some l₂ → l = tail ++ l₂
l l₂ : List α
P :
  (match l, head :: tail with
    | l, [] => some l
    | [], x => none
    | x :: l, y :: l₁ => if x = y then getRest l l₁ else none) =
    some l₂
⊢ l = head :: tail ++ l₂
Tactic:
split at P
Proof state after:
case cons.h_1
α : Type u_1
inst✝ : DecidableEq α
head : α
tail : List α
ih : ∀ {l l₂ : List α}, getRest l tail = some l₂ → l = tail ++ l₂
l₂ x✝² x✝¹ x✝ : List α
heq✝ : head :: tail = []
P : some x✝² = some l₂
⊢ x✝² = head :: tail ++ l₂

case cons.h_2
α : Type u_1
inst✝ : DecidableEq α
head : α
tail : List α
ih : ∀ {l l₂ : List α}, getRest l tail = some l₂ → l = tail ++ l₂
l₂ x✝² x✝¹ : List α
x✝ : head :: tail = [] → False
P : none = some l₂
⊢ [] = head :: tail ++ l₂

case cons.h_3
α : Type u_1
inst✝ : DecidableEq α
head : α
tail : List α
ih : ∀ {l l₂ : List α}, getRest l tail = some l₂ → l = tail ++ l₂
l₂ x✝² x✝¹ : List α
x✝ : α
l✝ : List α
y✝ : α
l₁✝ : List α
heq✝ : head :: tail = y✝ :: l₁✝
P : (if x✝ = y✝ then getRest l✝ l₁✝ else none) = some l₂
⊢ x✝ :: l✝ = head :: tail ++ l₂
Theorem: List.eq_append_of_getRest
Proof state before:
α : Type u_1
inst✝ : DecidableEq α
head : α
tail : List α
ih : ∀ {l l₂ : List α}, getRest l tail = some l₂ → l = tail ++ l₂
l₂ x✝² x✝¹ x✝ : List α
heq : head :: tail = []
P : some x✝² = some l₂
⊢ x✝² = head :: tail ++ l₂
Tactic:
case h_1 heq => simp only at heq
Proof state after:
no goals
Theorem: List.eq_append_of_getRest
Proof state before:
α : Type u_1
inst✝ : DecidableEq α
head : α
tail : List α
ih : ∀ {l l₂ : List α}, getRest l tail = some l₂ → l = tail ++ l₂
l₂ x✝² x✝¹ : List α
x✝ : head :: tail = [] → False
P : none = some l₂
⊢ [] = head :: tail ++ l₂
Tactic:
case h_2 => simp only at P
Proof state after:
no goals
Theorem: List.eq_append_of_getRest
Proof state before:
α : Type u_1
inst✝ : DecidableEq α
head : α
tail : List α
ih : ∀ {l l₂ : List α}, getRest l tail = some l₂ → l = tail ++ l₂
l₂ x✝¹ x✝ : List α
hd : α
tl : List α
y : α
l₁ : List α
heq : head :: tail = y :: l₁
P : (if hd = y then getRest tl l₁ else none) = some l₂
⊢ hd :: tl = head :: tail ++ l₂
Tactic:
case h_3 hd tl y l₁ heq =>
  split at P
  case inr heq₂ => contradiction
  case inl heq₂ =>
    injection heq
    subst hd y l₁
    simp only [cons_append, cons.injEq, true_and]
    apply ih
    apply P
Proof state after:
no goals
Theorem: List.eq_append_of_getRest
Proof state before:
α : Type u_1
inst✝ : DecidableEq α
head : α
tail : List α
ih : ∀ {l l₂ : List α}, getRest l tail = some l₂ → l = tail ++ l₂
l₂ x✝² x✝¹ x✝ : List α
heq : head :: tail = []
P : some x✝² = some l₂
⊢ x✝² = head :: tail ++ l₂
Tactic:
simp only at heq
Proof state after:
no goals
Theorem: List.eq_append_of_getRest
Proof state before:
α : Type u_1
inst✝ : DecidableEq α
head : α
tail : List α
ih : ∀ {l l₂ : List α}, getRest l tail = some l₂ → l = tail ++ l₂
l₂ x✝² x✝¹ : List α
x✝ : head :: tail = [] → False
P : none = some l₂
⊢ [] = head :: tail ++ l₂
Tactic:
simp only at P
Proof state after:
no goals
Theorem: List.eq_append_of_getRest
Proof state before:
α : Type u_1
inst✝ : DecidableEq α
head : α
tail : List α
ih : ∀ {l l₂ : List α}, getRest l tail = some l₂ → l = tail ++ l₂
l₂ x✝¹ x✝ : List α
hd : α
tl : List α
y : α
l₁ : List α
heq : head :: tail = y :: l₁
P : (if hd = y then getRest tl l₁ else none) = some l₂
⊢ hd :: tl = head :: tail ++ l₂
Tactic:
split at P
Proof state after:
case inl
α : Type u_1
inst✝ : DecidableEq α
head : α
tail : List α
ih : ∀ {l l₂ : List α}, getRest l tail = some l₂ → l = tail ++ l₂
l₂ x✝¹ x✝ : List α
hd : α
tl : List α
y : α
l₁ : List α
heq : head :: tail = y :: l₁
h✝ : hd = y
P : getRest tl l₁ = some l₂
⊢ hd :: tl = head :: tail ++ l₂

case inr
α : Type u_1
inst✝ : DecidableEq α
head : α
tail : List α
ih : ∀ {l l₂ : List α}, getRest l tail = some l₂ → l = tail ++ l₂
l₂ x✝¹ x✝ : List α
hd : α
tl : List α
y : α
l₁ : List α
heq : head :: tail = y :: l₁
h✝ : ¬hd = y
P : False
⊢ hd :: tl = head :: tail ++ l₂
Theorem: List.eq_append_of_getRest
Proof state before:
α : Type u_1
inst✝ : DecidableEq α
head : α
tail : List α
ih : ∀ {l l₂ : List α}, getRest l tail = some l₂ → l = tail ++ l₂
l₂ x✝¹ x✝ : List α
hd : α
tl : List α
y : α
l₁ : List α
heq : head :: tail = y :: l₁
heq₂ : ¬hd = y
P : False
⊢ hd :: tl = head :: tail ++ l₂
Tactic:
case inr heq₂ => contradiction
Proof state after:
no goals
Theorem: List.eq_append_of_getRest
Proof state before:
α : Type u_1
inst✝ : DecidableEq α
head : α
tail : List α
ih : ∀ {l l₂ : List α}, getRest l tail = some l₂ → l = tail ++ l₂
l₂ x✝¹ x✝ : List α
hd : α
tl : List α
y : α
l₁ : List α
heq : head :: tail = y :: l₁
heq₂ : hd = y
P : getRest tl l₁ = some l₂
⊢ hd :: tl = head :: tail ++ l₂
Tactic:
case inl heq₂ =>
  injection heq
  subst hd y l₁
  simp only [cons_append, cons.injEq, true_and]
  apply ih
  apply P
Proof state after:
no goals
Theorem: List.eq_append_of_getRest
Proof state before:
α : Type u_1
inst✝ : DecidableEq α
head : α
tail : List α
ih : ∀ {l l₂ : List α}, getRest l tail = some l₂ → l = tail ++ l₂
l₂ x✝¹ x✝ : List α
hd : α
tl : List α
y : α
l₁ : List α
heq : head :: tail = y :: l₁
heq₂ : ¬hd = y
P : False
⊢ hd :: tl = head :: tail ++ l₂
Tactic:
contradiction
Proof state after:
no goals
Theorem: List.eq_append_of_getRest
Proof state before:
α : Type u_1
inst✝ : DecidableEq α
head : α
tail : List α
ih : ∀ {l l₂ : List α}, getRest l tail = some l₂ → l = tail ++ l₂
l₂ x✝¹ x✝ : List α
hd : α
tl : List α
y : α
l₁ : List α
heq : head :: tail = y :: l₁
heq₂ : hd = y
P : getRest tl l₁ = some l₂
⊢ hd :: tl = head :: tail ++ l₂
Tactic:
injection heq
Proof state after:
α : Type u_1
inst✝ : DecidableEq α
head : α
tail : List α
ih : ∀ {l l₂ : List α}, getRest l tail = some l₂ → l = tail ++ l₂
l₂ x✝¹ x✝ : List α
hd : α
tl : List α
y : α
l₁ : List α
heq₂ : hd = y
P : getRest tl l₁ = some l₂
head_eq✝ : head = y
tail_eq✝ : tail = l₁
⊢ hd :: tl = head :: tail ++ l₂
Theorem: List.eq_append_of_getRest
Proof state before:
α : Type u_1
inst✝ : DecidableEq α
head : α
tail : List α
ih : ∀ {l l₂ : List α}, getRest l tail = some l₂ → l = tail ++ l₂
l₂ x✝¹ x✝ : List α
hd : α
tl : List α
y : α
l₁ : List α
heq₂ : hd = y
P : getRest tl l₁ = some l₂
head_eq✝ : head = y
tail_eq✝ : tail = l₁
⊢ hd :: tl = head :: tail ++ l₂
Tactic:
subst hd y l₁
Proof state after:
α : Type u_1
inst✝ : DecidableEq α
head : α
tail : List α
ih : ∀ {l l₂ : List α}, getRest l tail = some l₂ → l = tail ++ l₂
l₂ x✝¹ x✝ tl : List α
P : getRest tl tail = some l₂
⊢ head :: tl = head :: tail ++ l₂
Theorem: List.eq_append_of_getRest
Proof state before:
α : Type u_1
inst✝ : DecidableEq α
head : α
tail : List α
ih : ∀ {l l₂ : List α}, getRest l tail = some l₂ → l = tail ++ l₂
l₂ x✝¹ x✝ tl : List α
P : getRest tl tail = some l₂
⊢ head :: tl = head :: tail ++ l₂
Tactic:
simp only [cons_append, cons.injEq, true_and]
Proof state after:
α : Type u_1
inst✝ : DecidableEq α
head : α
tail : List α
ih : ∀ {l l₂ : List α}, getRest l tail = some l₂ → l = tail ++ l₂
l₂ x✝¹ x✝ tl : List α
P : getRest tl tail = some l₂
⊢ tl = tail ++ l₂
Theorem: List.eq_append_of_getRest
Proof state before:
α : Type u_1
inst✝ : DecidableEq α
head : α
tail : List α
ih : ∀ {l l₂ : List α}, getRest l tail = some l₂ → l = tail ++ l₂
l₂ x✝¹ x✝ tl : List α
P : getRest tl tail = some l₂
⊢ tl = tail ++ l₂
Tactic:
apply ih
Proof state after:
case P
α : Type u_1
inst✝ : DecidableEq α
head : α
tail : List α
ih : ∀ {l l₂ : List α}, getRest l tail = some l₂ → l = tail ++ l₂
l₂ x✝¹ x✝ tl : List α
P : getRest tl tail = some l₂
⊢ getRest tl tail = some l₂
Theorem: List.eq_append_of_getRest
Proof state before:
case P
α : Type u_1
inst✝ : DecidableEq α
head : α
tail : List α
ih : ∀ {l l₂ : List α}, getRest l tail = some l₂ → l = tail ++ l₂
l₂ x✝¹ x✝ tl : List α
P : getRest tl tail = some l₂
⊢ getRest tl tail = some l₂
Tactic:
apply P
Proof state after:
no goals
Theorem: List.getRest_nil
Proof state before:
α : Type u_1
inst✝ : DecidableEq α
l : List α
⊢ getRest l [] = some l
Tactic:
unfold getRest
Proof state after:
α : Type u_1
inst✝ : DecidableEq α
l : List α
⊢ (match l, [] with
    | l, [] => some l
    | [], x => none
    | x :: l, y :: l₁ => if x = y then getRest l l₁ else none) =
    some l
Theorem: List.getRest_nil
Proof state before:
α : Type u_1
inst✝ : DecidableEq α
l : List α
⊢ (match l, [] with
    | l, [] => some l
    | [], x => none
    | x :: l, y :: l₁ => if x = y then getRest l l₁ else none) =
    some l
Tactic:
simp only
Proof state after:
no goals
Theorem: List.getRest_delim_append
Proof state before:
α : Type u_1
inst✝ : DecidableEq α
l₁ l₂ : List α
⊢ getRest (l₁ ++ l₂) l₁ = some l₂
Tactic:
induction l₁ with
| nil => simp only [nil_append, getRest_nil]
| cons head tail ih =>
  unfold getRest
  simp only [cons_append, ih, ite_true]
Proof state after:
no goals
Theorem: List.getRest_delim_append
Proof state before:
case nil
α : Type u_1
inst✝ : DecidableEq α
l₂ : List α
⊢ getRest ([] ++ l₂) [] = some l₂
Tactic:
simp only [nil_append, getRest_nil]
Proof state after:
no goals
Theorem: List.getRest_delim_append
Proof state before:
case cons
α : Type u_1
inst✝ : DecidableEq α
l₂ : List α
head : α
tail : List α
ih : getRest (tail ++ l₂) tail = some l₂
⊢ getRest (head :: tail ++ l₂) (head :: tail) = some l₂
Tactic:
unfold getRest
Proof state after:
case cons
α : Type u_1
inst✝ : DecidableEq α
l₂ : List α
head : α
tail : List α
ih : getRest (tail ++ l₂) tail = some l₂
⊢ (match head :: tail ++ l₂, head :: tail with
    | l, [] => some l
    | [], x => none
    | x :: l, y :: l₁ => if x = y then getRest l l₁ else none) =
    some l₂
Theorem: List.getRest_delim_append
Proof state before:
case cons
α : Type u_1
inst✝ : DecidableEq α
l₂ : List α
head : α
tail : List α
ih : getRest (tail ++ l₂) tail = some l₂
⊢ (match head :: tail ++ l₂, head :: tail with
    | l, [] => some l
    | [], x => none
    | x :: l, y :: l₁ => if x = y then getRest l l₁ else none) =
    some l₂
Tactic:
simp only [cons_append, ih, ite_true]
Proof state after:
no goals
Theorem: List.nil_isInfix
Proof state before:
α✝ : Type u_1
l : List α✝
⊢ [] <:+: l
Tactic:
unfold List.isInfix
Proof state after:
α✝ : Type u_1
l : List α✝
⊢ ∃ s t, s ++ [] ++ t = l
Theorem: List.nil_isInfix
Proof state before:
α✝ : Type u_1
l : List α✝
⊢ ∃ s t, s ++ [] ++ t = l
Tactic:
exists []
Proof state after:
α✝ : Type u_1
l : List α✝
⊢ ∃ t, [] ++ [] ++ t = l
Theorem: List.nil_isInfix
Proof state before:
α✝ : Type u_1
l : List α✝
⊢ ∃ t, [] ++ [] ++ t = l
Tactic:
exists l
Proof state after:
no goals
Theorem: List.nil_isPrefix
Proof state before:
α✝ : Type u_1
l : List α✝
⊢ [] <+: l
Tactic:
unfold List.isPrefix
Proof state after:
α✝ : Type u_1
l : List α✝
⊢ ∃ t, [] ++ t = l
Theorem: List.nil_isPrefix
Proof state before:
α✝ : Type u_1
l : List α✝
⊢ ∃ t, [] ++ t = l
Tactic:
exists l
Proof state after:
no goals
Theorem: List.nil_isSuffix
Proof state before:
α✝ : Type u_1
l : List α✝
⊢ [] <:+ l
Tactic:
unfold List.isSuffix
Proof state after:
α✝ : Type u_1
l : List α✝
⊢ ∃ t, t ++ [] = l
Theorem: List.nil_isSuffix
Proof state before:
α✝ : Type u_1
l : List α✝
⊢ ∃ t, t ++ [] = l
Tactic:
simp only [append_nil, exists_eq]
Proof state after:
no goals
Theorem: List.isInfix_cons
Proof state before:
α : Type u_1
head : α
l tail : List α
h : l <:+: tail
⊢ l <:+: head :: tail
Tactic:
unfold List.isInfix at *
Proof state after:
α : Type u_1
head : α
l tail : List α
h : ∃ s t, s ++ l ++ t = tail
⊢ ∃ s t, s ++ l ++ t = head :: tail
Theorem: List.isInfix_cons
Proof state before:
α : Type u_1
head : α
l tail : List α
h : ∃ s t, s ++ l ++ t = tail
⊢ ∃ s t, s ++ l ++ t = head :: tail
Tactic:
match h with
| ⟨s,  t, P⟩ =>
  exists head::s,  t
  simp only [cons_append, append_assoc, ← P]
Proof state after:
no goals
Theorem: List.isInfix_cons
Proof state before:
α : Type u_1
head : α
l tail : List α
h : ∃ s t, s ++ l ++ t = tail
s t : List α
P : s ++ l ++ t = tail
⊢ ∃ s t, s ++ l ++ t = head :: tail
Tactic:
exists head::s,  t
Proof state after:
α : Type u_1
head : α
l tail : List α
h : ∃ s t, s ++ l ++ t = tail
s t : List α
P : s ++ l ++ t = tail
⊢ head :: s ++ l ++ t = head :: tail
Theorem: List.isInfix_cons
Proof state before:
α : Type u_1
head : α
l tail : List α
h : ∃ s t, s ++ l ++ t = tail
s t : List α
P : s ++ l ++ t = tail
⊢ head :: s ++ l ++ t = head :: tail
Tactic:
simp only [cons_append, append_assoc, ← P]
Proof state after:
no goals
Theorem: List.isInfix_append_left
Proof state before:
α : Type u_1
l₁ l₂ : List α
⊢ l₁ <:+: l₁ ++ l₂
Tactic:
exact ⟨ [], l₂, rfl⟩
Proof state after:
no goals
Theorem: List.isInfix_append_right
Proof state before:
α : Type u_1
l₁ l₂ : List α
⊢ l₂ <:+: l₁ ++ l₂
Tactic:
exact ⟨ l₁, [], List.append_nil _⟩
Proof state after:
no goals
Theorem: List.isInfix_self
Proof state before:
α✝ : Type u_1
l : List α✝
⊢ l <:+: l
Tactic:
exact ⟨[], [], List.append_nil _⟩
Proof state after:
no goals
Theorem: List.getRest_none
Proof state before:
α : Type u_1
inst✝ : DecidableEq α
l₁ l₂ : List α
⊢ getRest l₁ l₂ = none ↔ ¬l₂ <+: l₁
Tactic:
apply iff_not_comm.1
Proof state after:
α : Type u_1
inst✝ : DecidableEq α
l₁ l₂ : List α
⊢ l₂ <+: l₁ ↔ ¬getRest l₁ l₂ = none
Theorem: List.getRest_none
Proof state before:
α : Type u_1
inst✝ : DecidableEq α
l₁ l₂ : List α
⊢ l₂ <+: l₁ ↔ ¬getRest l₁ l₂ = none
Tactic:
rw [← ne_eq, Option.ne_none_iff_exists]
Proof state after:
α : Type u_1
inst✝ : DecidableEq α
l₁ l₂ : List α
⊢ l₂ <+: l₁ ↔ ∃ x, some x = getRest l₁ l₂
Theorem: List.getRest_none
Proof state before:
α : Type u_1
inst✝ : DecidableEq α
l₁ l₂ : List α
⊢ l₂ <+: l₁ ↔ ∃ x, some x = getRest l₁ l₂
Tactic:
apply Iff.intro
Proof state after:
case mp
α : Type u_1
inst✝ : DecidableEq α
l₁ l₂ : List α
⊢ l₂ <+: l₁ → ∃ x, some x = getRest l₁ l₂

case mpr
α : Type u_1
inst✝ : DecidableEq α
l₁ l₂ : List α
⊢ (∃ x, some x = getRest l₁ l₂) → l₂ <+: l₁
Theorem: List.getRest_none
Proof state before:
case mp
α : Type u_1
inst✝ : DecidableEq α
l₁ l₂ : List α
⊢ l₂ <+: l₁ → ∃ x, some x = getRest l₁ l₂

case mpr
α : Type u_1
inst✝ : DecidableEq α
l₁ l₂ : List α
⊢ (∃ x, some x = getRest l₁ l₂) → l₂ <+: l₁
Tactic:
. intro ⟨l₃, h⟩
  subst h
  exists l₃
  exact Eq.symm getRest_delim_append
Proof state after:
case mpr
α : Type u_1
inst✝ : DecidableEq α
l₁ l₂ : List α
⊢ (∃ x, some x = getRest l₁ l₂) → l₂ <+: l₁
Theorem: List.getRest_none
Proof state before:
case mpr
α : Type u_1
inst✝ : DecidableEq α
l₁ l₂ : List α
⊢ (∃ x, some x = getRest l₁ l₂) → l₂ <+: l₁
Tactic:
. intro ⟨l₃, h⟩
  exists l₃
  exact Eq.symm (eq_append_of_getRest (Eq.symm h))
Proof state after:
no goals
Theorem: List.sizeOf_getRest
Proof 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]
Proof state after:
no goals
Theorem: List.sizeOf_getRest
Proof 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
Proof 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₁
Theorem: List.sizeOf_getRest
Proof 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₁
Proof 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✝)
Theorem: List.sizeOf_getRest
Proof 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]
Proof 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✝)
Theorem: List.sizeOf_getRest
Proof 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
Proof state after:
no goals
Theorem: List.sizeOf_getRest
Proof 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
Proof 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₁
Theorem: List.sizeOf_getRest
Proof 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
Proof 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₁✝)
Theorem: List.sizeOf_getRest
Proof 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]
Proof state after:
no goals
Theorem: List.sizeOf_getRest
Proof 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]
Proof state after:
no goals
Theorem: List.sizeOf_getRest
Proof 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
Proof state after:
no goals
Theorem: List.sizeOf_getRest
Proof 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
Proof 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 []
Theorem: List.sizeOf_getRest
Proof 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]
Proof state after:
no goals