internlm/Lean-Github huggingface dataset:
Theorem: Nat.digit_gt_log_eq_zero
Proof state before:
b n i : ℕ
P : b > 1
Q : i > log b n
⊢ digit b n i = 0
Tactic:
unfold digit
Proof state after:
b n i : ℕ
P : b > 1
Q : i > log b n
⊢ n / b ^ i % b = 0
Theorem: Nat.digit_gt_log_eq_zero
Proof state before:
b n i : ℕ
P : b > 1
Q : i > log b n
⊢ n / b ^ i % b = 0
Tactic:
convert Nat.zero_mod b
Proof state after:
case e_a.e_a
b n i : ℕ
P : b > 1
Q : i > log b n
⊢ n / b ^ i = 0
Theorem: Nat.digit_gt_log_eq_zero
Proof state before:
case e_a.e_a
b n i : ℕ
P : b > 1
Q : i > log b n
⊢ n / b ^ i = 0
Tactic:
apply Nat.div_eq_of_lt
Proof state after:
case e_a.e_a.h₀
b n i : ℕ
P : b > 1
Q : i > log b n
⊢ n < b ^ i
Theorem: Nat.digit_gt_log_eq_zero
Proof state before:
case e_a.e_a.h₀
b n i : ℕ
P : b > 1
Q : i > log b n
⊢ n < b ^ i
Tactic:
apply Nat.lt_pow_of_log_lt
Proof state after:
case e_a.e_a.h₀.hb
b n i : ℕ
P : b > 1
Q : i > log b n
⊢ 1 < b

case e_a.e_a.h₀.a
b n i : ℕ
P : b > 1
Q : i > log b n
⊢ log b n < i
Theorem: Nat.digit_gt_log_eq_zero
Proof state before:
case e_a.e_a.h₀.hb
b n i : ℕ
P : b > 1
Q : i > log b n
⊢ 1 < b

case e_a.e_a.h₀.a
b n i : ℕ
P : b > 1
Q : i > log b n
⊢ log b n < i
Tactic:
. exact P
Proof state after:
case e_a.e_a.h₀.a
b n i : ℕ
P : b > 1
Q : i > log b n
⊢ log b n < i
Theorem: Nat.digit_gt_log_eq_zero
Proof state before:
case e_a.e_a.h₀.a
b n i : ℕ
P : b > 1
Q : i > log b n
⊢ log b n < i
Tactic:
. exact Q
Proof state after:
no goals
Theorem: List.lastN_zero
Proof state before:
α : Type u_1
l : List α
⊢ lastN 0 l = []
Tactic:
unfold List.lastN
Proof state after:
α : Type u_1
l : List α
⊢ drop (length l - 0) l = []
Theorem: List.lastN_zero
Proof state before:
α : Type u_1
l : List α
⊢ drop (length l - 0) l = []
Tactic:
simp
Proof state after:
no goals
Theorem: List.lastN_length_eq_self
Proof state before:
α : Type u_1
l : List α
⊢ lastN (length l) l = l
Tactic:
unfold List.lastN
Proof state after:
α : Type u_1
l : List α
⊢ drop (length l - length l) l = l
Theorem: List.lastN_length_eq_self
Proof state before:
α : Type u_1
l : List α
⊢ drop (length l - length l) l = l
Tactic:
simp
Proof state after:
no goals
Theorem: List.lastN_length
Proof state before:
α : Type u_1
l : List α
i : ℕ
⊢ length (lastN i l) = min i (length l)
Tactic:
unfold lastN
Proof state after:
α : Type u_1
l : List α
i : ℕ
⊢ length (drop (length l - i) l) = min i (length l)
Theorem: List.lastN_length
Proof state before:
α : Type u_1
l : List α
i : ℕ
⊢ length (drop (length l - i) l) = min i (length l)
Tactic:
simp only [ge_iff_le, length_drop]
Proof state after:
α : Type u_1
l : List α
i : ℕ
⊢ length l - (length l - i) = min i (length l)
Theorem: List.lastN_length
Proof state before:
α : Type u_1
l : List α
i : ℕ
⊢ length l - (length l - i) = min i (length l)
Tactic:
cases h: decide (i ≤  length l) with
| true => 
  simp at h
  rw [Nat.sub_sub_self h, Nat.min_eq_left h]
| false =>
  simp at h
  have h₂: length l ≤ i := Nat.le_of_lt h
  simp [h₂]
Proof state after:
no goals
Theorem: List.lastN_length
Proof state before:
case true
α : Type u_1
l : List α
i : ℕ
h : decide (i ≤ length l) = true
⊢ length l - (length l - i) = min i (length l)
Tactic:
simp at h
Proof state after:
case true
α : Type u_1
l : List α
i : ℕ
h : i ≤ length l
⊢ length l - (length l - i) = min i (length l)
Theorem: List.lastN_length
Proof state before:
case true
α : Type u_1
l : List α
i : ℕ
h : i ≤ length l
⊢ length l - (length l - i) = min i (length l)
Tactic:
rw [Nat.sub_sub_self h, Nat.min_eq_left h]
Proof state after:
no goals
Theorem: List.lastN_length
Proof state before:
case false
α : Type u_1
l : List α
i : ℕ
h : decide (i ≤ length l) = false
⊢ length l - (length l - i) = min i (length l)
Tactic:
simp at h
Proof state after:
case false
α : Type u_1
l : List α
i : ℕ
h : length l < i
⊢ length l - (length l - i) = min i (length l)
Theorem: List.lastN_length
Proof state before:
case false
α : Type u_1
l : List α
i : ℕ
h : length l < i
⊢ length l - (length l - i) = min i (length l)
Tactic:
have h₂: length l ≤ i := Nat.le_of_lt h
Proof state after:
case false
α : Type u_1
l : List α
i : ℕ
h : length l < i
h₂ : length l ≤ i
⊢ length l - (length l - i) = min i (length l)
Theorem: List.lastN_length
Proof state before:
case false
α : Type u_1
l : List α
i : ℕ
h : length l < i
h₂ : length l ≤ i
⊢ length l - (length l - i) = min i (length l)
Tactic:
simp [h₂]
Proof state after:
no goals
Theorem: List.lastN_cons
Proof state before:
α : Type u_1
head : α
tail : List α
i : ℕ
⊢ lastN i (head :: tail) = if length (head :: tail) > i then lastN i tail else head :: tail
Tactic:
unfold lastN
Proof state after:
α : Type u_1
head : α
tail : List α
i : ℕ
⊢ drop (length (head :: tail) - i) (head :: tail) =
    if length (head :: tail) > i then drop (length tail - i) tail else head :: tail
Theorem: List.lastN_cons
Proof state before:
α : Type u_1
head : α
tail : List α
i : ℕ
⊢ drop (length (head :: tail) - i) (head :: tail) =
    if length (head :: tail) > i then drop (length tail - i) tail else head :: tail
Tactic:
induction tail with
| nil => 
  split
  case inl heq => simp_all
  case inr heq => 
    simp only [length_singleton, gt_iff_lt, Nat.lt_one_iff, ← ne_eq] at heq
    simp only [length_singleton, ge_iff_le, Nat.sub_eq_zero_of_le (Nat.succ_le_of_lt (Nat.pos_of_ne_zero heq)), drop]
| cons mid tail _ih=>
  split
  case inl heq =>
    simp [Nat.succ_eq_one_add]
    rw [Nat.add_sub_assoc, ←Nat.succ_eq_one_add, drop._eq_3]
    simp_all only [Nat.le_of_lt_succ, length_cons, Nat.succ_eq_one_add, ge_iff_le, gt_iff_lt]
  case inr heq =>
    simp only [length_cons, gt_iff_lt, not_lt] at heq
    simp only [length_cons, ge_iff_le, Nat.sub_eq_zero_of_le heq, drop]
Proof state after:
no goals
Theorem: List.lastN_cons
Proof state before:
case nil
α : Type u_1
head : α
i : ℕ
⊢ drop (length [head] - i) [head] = if length [head] > i then drop (length [] - i) [] else [head]
Tactic:
split
Proof state after:
case nil.inl
α : Type u_1
head : α
i : ℕ
h✝ : length [head] > i
⊢ drop (length [head] - i) [head] = drop (length [] - i) []

case nil.inr
α : Type u_1
head : α
i : ℕ
h✝ : ¬length [head] > i
⊢ drop (length [head] - i) [head] = [head]
Theorem: List.lastN_cons
Proof state before:
α : Type u_1
head : α
i : ℕ
heq : length [head] > i
⊢ drop (length [head] - i) [head] = drop (length [] - i) []
Tactic:
case inl heq => simp_all
Proof state after:
no goals
Theorem: List.lastN_cons
Proof state before:
α : Type u_1
head : α
i : ℕ
heq : ¬length [head] > i
⊢ drop (length [head] - i) [head] = [head]
Tactic:
case inr heq => 
  simp only [length_singleton, gt_iff_lt, Nat.lt_one_iff, ← ne_eq] at heq
  simp only [length_singleton, ge_iff_le, Nat.sub_eq_zero_of_le (Nat.succ_le_of_lt (Nat.pos_of_ne_zero heq)), drop]
Proof state after:
no goals
Theorem: List.lastN_cons
Proof state before:
α : Type u_1
head : α
i : ℕ
heq : length [head] > i
⊢ drop (length [head] - i) [head] = drop (length [] - i) []
Tactic:
simp_all
Proof state after:
no goals
Theorem: List.lastN_cons
Proof state before:
α : Type u_1
head : α
i : ℕ
heq : ¬length [head] > i
⊢ drop (length [head] - i) [head] = [head]
Tactic:
simp only [length_singleton, gt_iff_lt, Nat.lt_one_iff, ← ne_eq] at heq
Proof state after:
α : Type u_1
head : α
i : ℕ
heq : i ≠ 0
⊢ drop (length [head] - i) [head] = [head]
Theorem: List.lastN_cons
Proof state before:
α : Type u_1
head : α
i : ℕ
heq : i ≠ 0
⊢ drop (length [head] - i) [head] = [head]
Tactic:
simp only [length_singleton, ge_iff_le, Nat.sub_eq_zero_of_le (Nat.succ_le_of_lt (Nat.pos_of_ne_zero heq)), drop]
Proof state after:
no goals
Theorem: List.lastN_cons
Proof state before:
case cons
α : Type u_1
head : α
i : ℕ
mid : α
tail : List α
_ih :
  drop (length (head :: tail) - i) (head :: tail) =
    if length (head :: tail) > i then drop (length tail - i) tail else head :: tail
⊢ drop (length (head :: mid :: tail) - i) (head :: mid :: tail) =
    if length (head :: mid :: tail) > i then drop (length (mid :: tail) - i) (mid :: tail) else head :: mid :: tail
Tactic:
split
Proof state after:
case cons.inl
α : Type u_1
head : α
i : ℕ
mid : α
tail : List α
_ih :
  drop (length (head :: tail) - i) (head :: tail) =
    if length (head :: tail) > i then drop (length tail - i) tail else head :: tail
h✝ : length (head :: mid :: tail) > i
⊢ drop (length (head :: mid :: tail) - i) (head :: mid :: tail) = drop (length (mid :: tail) - i) (mid :: tail)

case cons.inr
α : Type u_1
head : α
i : ℕ
mid : α
tail : List α
_ih :
  drop (length (head :: tail) - i) (head :: tail) =
    if length (head :: tail) > i then drop (length tail - i) tail else head :: tail
h✝ : ¬length (head :: mid :: tail) > i
⊢ drop (length (head :: mid :: tail) - i) (head :: mid :: tail) = head :: mid :: tail
Theorem: List.lastN_cons
Proof state before:
α : Type u_1
head : α
i : ℕ
mid : α
tail : List α
_ih :
  drop (length (head :: tail) - i) (head :: tail) =
    if length (head :: tail) > i then drop (length tail - i) tail else head :: tail
heq : length (head :: mid :: tail) > i
⊢ drop (length (head :: mid :: tail) - i) (head :: mid :: tail) = drop (length (mid :: tail) - i) (mid :: tail)
Tactic:
case inl heq =>
  simp [Nat.succ_eq_one_add]
  rw [Nat.add_sub_assoc, ←Nat.succ_eq_one_add, drop._eq_3]
  simp_all only [Nat.le_of_lt_succ, length_cons, Nat.succ_eq_one_add, ge_iff_le, gt_iff_lt]
Proof state after:
no goals
Theorem: List.lastN_cons
Proof state before:
α : Type u_1
head : α
i : ℕ
mid : α
tail : List α
_ih :
  drop (length (head :: tail) - i) (head :: tail) =
    if length (head :: tail) > i then drop (length tail - i) tail else head :: tail
heq : ¬length (head :: mid :: tail) > i
⊢ drop (length (head :: mid :: tail) - i) (head :: mid :: tail) = head :: mid :: tail
Tactic:
case inr heq =>
  simp only [length_cons, gt_iff_lt, not_lt] at heq
  simp only [length_cons, ge_iff_le, Nat.sub_eq_zero_of_le heq, drop]
Proof state after:
no goals
Theorem: List.lastN_cons
Proof state before:
α : Type u_1
head : α
i : ℕ
mid : α
tail : List α
_ih :
  drop (length (head :: tail) - i) (head :: tail) =
    if length (head :: tail) > i then drop (length tail - i) tail else head :: tail
heq : length (head :: mid :: tail) > i
⊢ drop (length (head :: mid :: tail) - i) (head :: mid :: tail) = drop (length (mid :: tail) - i) (mid :: tail)
Tactic:
simp [Nat.succ_eq_one_add]
Proof state after:
α : Type u_1
head : α
i : ℕ
mid : α
tail : List α
_ih :
  drop (length (head :: tail) - i) (head :: tail) =
    if length (head :: tail) > i then drop (length tail - i) tail else head :: tail
heq : length (head :: mid :: tail) > i
⊢ drop (1 + (1 + length tail) - i) (head :: mid :: tail) = drop (1 + length tail - i) (mid :: tail)
Theorem: List.lastN_cons
Proof state before:
α : Type u_1
head : α
i : ℕ
mid : α
tail : List α
_ih :
  drop (length (head :: tail) - i) (head :: tail) =
    if length (head :: tail) > i then drop (length tail - i) tail else head :: tail
heq : length (head :: mid :: tail) > i
⊢ drop (1 + (1 + length tail) - i) (head :: mid :: tail) = drop (1 + length tail - i) (mid :: tail)
Tactic:
rw [Nat.add_sub_assoc, ←Nat.succ_eq_one_add, drop._eq_3]
Proof state after:
case h
α : Type u_1
head : α
i : ℕ
mid : α
tail : List α
_ih :
  drop (length (head :: tail) - i) (head :: tail) =
    if length (head :: tail) > i then drop (length tail - i) tail else head :: tail
heq : length (head :: mid :: tail) > i
⊢ i ≤ 1 + length tail
Theorem: List.lastN_cons
Proof state before:
case h
α : Type u_1
head : α
i : ℕ
mid : α
tail : List α
_ih :
  drop (length (head :: tail) - i) (head :: tail) =
    if length (head :: tail) > i then drop (length tail - i) tail else head :: tail
heq : length (head :: mid :: tail) > i
⊢ i ≤ 1 + length tail
Tactic:
simp_all only [Nat.le_of_lt_succ, length_cons, Nat.succ_eq_one_add, ge_iff_le, gt_iff_lt]
Proof state after:
no goals
Theorem: List.lastN_cons
Proof state before:
α : Type u_1
head : α
i : ℕ
mid : α
tail : List α
_ih :
  drop (length (head :: tail) - i) (head :: tail) =
    if length (head :: tail) > i then drop (length tail - i) tail else head :: tail
heq : ¬length (head :: mid :: tail) > i
⊢ drop (length (head :: mid :: tail) - i) (head :: mid :: tail) = head :: mid :: tail
Tactic:
simp only [length_cons, gt_iff_lt, not_lt] at heq
Proof state after:
α : Type u_1
head : α
i : ℕ
mid : α
tail : List α
_ih :
  drop (length (head :: tail) - i) (head :: tail) =
    if length (head :: tail) > i then drop (length tail - i) tail else head :: tail
heq : Nat.succ (Nat.succ (length tail)) ≤ i
⊢ drop (length (head :: mid :: tail) - i) (head :: mid :: tail) = head :: mid :: tail
Theorem: List.lastN_cons
Proof state before:
α : Type u_1
head : α
i : ℕ
mid : α
tail : List α
_ih :
  drop (length (head :: tail) - i) (head :: tail) =
    if length (head :: tail) > i then drop (length tail - i) tail else head :: tail
heq : Nat.succ (Nat.succ (length tail)) ≤ i
⊢ drop (length (head :: mid :: tail) - i) (head :: mid :: tail) = head :: mid :: tail
Tactic:
simp only [length_cons, ge_iff_le, Nat.sub_eq_zero_of_le heq, drop]
Proof state after:
no goals
Theorem: List.lastN_ge_length
Proof state before:
α : Type u_1
n : ℕ
l : List α
h : n ≥ length l
⊢ lastN n l = l
Tactic:
unfold List.lastN
Proof state after:
α : Type u_1
n : ℕ
l : List α
h : n ≥ length l
⊢ drop (length l - n) l = l
Theorem: List.lastN_ge_length
Proof state before:
α : Type u_1
n : ℕ
l : List α
h : n ≥ length l
⊢ drop (length l - n) l = l
Tactic:
simp [h]
Proof state after:
no goals
Theorem: List.lastN_one_eq_getLast
Proof state before:
α : Type u_1
l : List α
⊢ lastN 1 l = Option.toList (getLast? l)
Tactic:
induction l with
| nil => simp only [length_nil, ge_iff_le, lastN_ge_length, getLast?_nil, Option.to_list_none]
| cons head tail ih=> 
  rw [lastN_cons]
  simp only [length_cons, gt_iff_lt, ge_iff_le]
  split
  case inl heq =>
    have hne: tail ≠ [] := by
      apply List.ne_nil_of_length_pos
      apply Nat.succ_lt_succ_iff.1 heq
    rw [getLast?_cons, ih, getLast?_eq_getLast _ hne, List.getLastD]
    split
    . contradiction
    . simp
  case inr heq =>
    simp at heq
    have hnil: tail = [] := List.eq_nil_of_length_eq_zero (Nat.eq_zero_of_le_zero (Nat.le_of_succ_le_succ heq))
    subst tail
    simp only [getLast?_singleton, Option.to_list_some]
Proof state after:
no goals
Theorem: List.lastN_one_eq_getLast
Proof state before:
case nil
α : Type u_1
⊢ lastN 1 [] = Option.toList (getLast? [])
Tactic:
simp only [length_nil, ge_iff_le, lastN_ge_length, getLast?_nil, Option.to_list_none]
Proof state after:
no goals
Theorem: List.lastN_one_eq_getLast
Proof state before:
case cons
α : Type u_1
head : α
tail : List α
ih : lastN 1 tail = Option.toList (getLast? tail)
⊢ lastN 1 (head :: tail) = Option.toList (getLast? (head :: tail))
Tactic:
rw [lastN_cons]
Proof state after:
case cons
α : Type u_1
head : α
tail : List α
ih : lastN 1 tail = Option.toList (getLast? tail)
⊢ (if length (head :: tail) > 1 then lastN 1 tail else head :: tail) = Option.toList (getLast? (head :: tail))
Theorem: List.lastN_one_eq_getLast
Proof state before:
case cons
α : Type u_1
head : α
tail : List α
ih : lastN 1 tail = Option.toList (getLast? tail)
⊢ (if length (head :: tail) > 1 then lastN 1 tail else head :: tail) = Option.toList (getLast? (head :: tail))
Tactic:
simp only [length_cons, gt_iff_lt, ge_iff_le]
Proof state after:
case cons
α : Type u_1
head : α
tail : List α
ih : lastN 1 tail = Option.toList (getLast? tail)
⊢ (if 1 < Nat.succ (length tail) then lastN 1 tail else head :: tail) = Option.toList (getLast? (head :: tail))
Theorem: List.lastN_one_eq_getLast
Proof state before:
case cons
α : Type u_1
head : α
tail : List α
ih : lastN 1 tail = Option.toList (getLast? tail)
⊢ (if 1 < Nat.succ (length tail) then lastN 1 tail else head :: tail) = Option.toList (getLast? (head :: tail))
Tactic:
split
Proof state after:
case cons.inl
α : Type u_1
head : α
tail : List α
ih : lastN 1 tail = Option.toList (getLast? tail)
h✝ : 1 < Nat.succ (length tail)
⊢ lastN 1 tail = Option.toList (getLast? (head :: tail))

case cons.inr
α : Type u_1
head : α
tail : List α
ih : lastN 1 tail = Option.toList (getLast? tail)
h✝ : ¬1 < Nat.succ (length tail)
⊢ head :: tail = Option.toList (getLast? (head :: tail))
Theorem: List.lastN_one_eq_getLast
Proof state before:
α : Type u_1
head : α
tail : List α
ih : lastN 1 tail = Option.toList (getLast? tail)
heq : 1 < Nat.succ (length tail)
⊢ lastN 1 tail = Option.toList (getLast? (head :: tail))
Tactic:
case inl heq =>
  have hne: tail ≠ [] := by
    apply List.ne_nil_of_length_pos
    apply Nat.succ_lt_succ_iff.1 heq
  rw [getLast?_cons, ih, getLast?_eq_getLast _ hne, List.getLastD]
  split
  . contradiction
  . simp
Proof state after:
no goals
Theorem: List.lastN_one_eq_getLast
Proof state before:
α : Type u_1
head : α
tail : List α
ih : lastN 1 tail = Option.toList (getLast? tail)
heq : ¬1 < Nat.succ (length tail)
⊢ head :: tail = Option.toList (getLast? (head :: tail))
Tactic:
case inr heq =>
  simp at heq
  have hnil: tail = [] := List.eq_nil_of_length_eq_zero (Nat.eq_zero_of_le_zero (Nat.le_of_succ_le_succ heq))
  subst tail
  simp only [getLast?_singleton, Option.to_list_some]
Proof state after:
no goals
Theorem: List.lastN_one_eq_getLast
Proof state before:
α : Type u_1
head : α
tail : List α
ih : lastN 1 tail = Option.toList (getLast? tail)
heq : 1 < Nat.succ (length tail)
⊢ lastN 1 tail = Option.toList (getLast? (head :: tail))
Tactic:
have hne: tail ≠ [] := by
  apply List.ne_nil_of_length_pos
  apply Nat.succ_lt_succ_iff.1 heq
Proof state after:
α : Type u_1
head : α
tail : List α
ih : lastN 1 tail = Option.toList (getLast? tail)
heq : 1 < Nat.succ (length tail)
hne : tail ≠ []
⊢ lastN 1 tail = Option.toList (getLast? (head :: tail))
Theorem: List.lastN_one_eq_getLast
Proof state before:
α : Type u_1
head : α
tail : List α
ih : lastN 1 tail = Option.toList (getLast? tail)
heq : 1 < Nat.succ (length tail)
hne : tail ≠ []
⊢ lastN 1 tail = Option.toList (getLast? (head :: tail))
Tactic:
rw [getLast?_cons, ih, getLast?_eq_getLast _ hne, List.getLastD]
Proof state after:
α : Type u_1
head : α
tail : List α
ih : lastN 1 tail = Option.toList (getLast? tail)
heq : 1 < Nat.succ (length tail)
hne : tail ≠ []
⊢ Option.toList (some (getLast tail hne)) =
    Option.toList
      (some
        (match tail, head with
        | [], a₀ => a₀
        | a :: as, x => getLast (a :: as) (_ : a :: as = [] → List.noConfusionType False (a :: as) [])))
Theorem: List.lastN_one_eq_getLast
Proof state before:
α : Type u_1
head : α
tail : List α
ih : lastN 1 tail = Option.toList (getLast? tail)
heq : 1 < Nat.succ (length tail)
hne : tail ≠ []
⊢ Option.toList (some (getLast tail hne)) =
    Option.toList
      (some
        (match tail, head with
        | [], a₀ => a₀
        | a :: as, x => getLast (a :: as) (_ : a :: as = [] → List.noConfusionType False (a :: as) [])))
Tactic:
split
Proof state after:
case h_1
α : Type u_1
head : α
x✝¹ : List α
x✝ : α
ih : lastN 1 [] = Option.toList (getLast? [])
heq : 1 < Nat.succ (length [])
hne : [] ≠ []
⊢ Option.toList (some (getLast [] hne)) = Option.toList (some head)

case h_2
α : Type u_1
head : α
x✝¹ : List α
x✝ a✝ : α
tail✝ : List α
ih : lastN 1 (a✝ :: tail✝) = Option.toList (getLast? (a✝ :: tail✝))
heq : 1 < Nat.succ (length (a✝ :: tail✝))
hne : a✝ :: tail✝ ≠ []
⊢ Option.toList (some (getLast (a✝ :: tail✝) hne)) =
    Option.toList (some (getLast (a✝ :: tail✝) (_ : a✝ :: tail✝ = [] → List.noConfusionType False (a✝ :: tail✝) [])))
Theorem: List.lastN_one_eq_getLast
Proof state before:
case h_1
α : Type u_1
head : α
x✝¹ : List α
x✝ : α
ih : lastN 1 [] = Option.toList (getLast? [])
heq : 1 < Nat.succ (length [])
hne : [] ≠ []
⊢ Option.toList (some (getLast [] hne)) = Option.toList (some head)

case h_2
α : Type u_1
head : α
x✝¹ : List α
x✝ a✝ : α
tail✝ : List α
ih : lastN 1 (a✝ :: tail✝) = Option.toList (getLast? (a✝ :: tail✝))
heq : 1 < Nat.succ (length (a✝ :: tail✝))
hne : a✝ :: tail✝ ≠ []
⊢ Option.toList (some (getLast (a✝ :: tail✝) hne)) =
    Option.toList (some (getLast (a✝ :: tail✝) (_ : a✝ :: tail✝ = [] → List.noConfusionType False (a✝ :: tail✝) [])))
Tactic:
. contradiction
Proof state after:
case h_2
α : Type u_1
head : α
x✝¹ : List α
x✝ a✝ : α
tail✝ : List α
ih : lastN 1 (a✝ :: tail✝) = Option.toList (getLast? (a✝ :: tail✝))
heq : 1 < Nat.succ (length (a✝ :: tail✝))
hne : a✝ :: tail✝ ≠ []
⊢ Option.toList (some (getLast (a✝ :: tail✝) hne)) =
    Option.toList (some (getLast (a✝ :: tail✝) (_ : a✝ :: tail✝ = [] → List.noConfusionType False (a✝ :: tail✝) [])))
Theorem: List.lastN_one_eq_getLast
Proof state before:
case h_2
α : Type u_1
head : α
x✝¹ : List α
x✝ a✝ : α
tail✝ : List α
ih : lastN 1 (a✝ :: tail✝) = Option.toList (getLast? (a✝ :: tail✝))
heq : 1 < Nat.succ (length (a✝ :: tail✝))
hne : a✝ :: tail✝ ≠ []
⊢ Option.toList (some (getLast (a✝ :: tail✝) hne)) =
    Option.toList (some (getLast (a✝ :: tail✝) (_ : a✝ :: tail✝ = [] → List.noConfusionType False (a✝ :: tail✝) [])))
Tactic:
. simp
Proof state after:
no goals
Theorem: List.lastN_one_eq_getLast
Proof state before:
α : Type u_1
head : α
tail : List α
ih : lastN 1 tail = Option.toList (getLast? tail)
heq : 1 < Nat.succ (length tail)
⊢ tail ≠ []
Tactic:
apply List.ne_nil_of_length_pos
Proof state after:
case a
α : Type u_1
head : α
tail : List α
ih : lastN 1 tail = Option.toList (getLast? tail)
heq : 1 < Nat.succ (length tail)
⊢ 0 < length tail
Theorem: List.lastN_one_eq_getLast
Proof state before:
case a
α : Type u_1
head : α
tail : List α
ih : lastN 1 tail = Option.toList (getLast? tail)
heq : 1 < Nat.succ (length tail)
⊢ 0 < length tail
Tactic:
apply Nat.succ_lt_succ_iff.1 heq
Proof state after:
no goals
Theorem: List.lastN_one_eq_getLast
Proof state before:
α : Type u_1
head : α
tail : List α
ih : lastN 1 tail = Option.toList (getLast? tail)
heq : ¬1 < Nat.succ (length tail)
⊢ head :: tail = Option.toList (getLast? (head :: tail))
Tactic:
simp at heq
Proof state after:
α : Type u_1
head : α
tail : List α
ih : lastN 1 tail = Option.toList (getLast? tail)
heq : Nat.succ (length tail) ≤ 1
⊢ head :: tail = Option.toList (getLast? (head :: tail))
Theorem: List.lastN_one_eq_getLast
Proof state before:
α : Type u_1
head : α
tail : List α
ih : lastN 1 tail = Option.toList (getLast? tail)
heq : Nat.succ (length tail) ≤ 1
⊢ head :: tail = Option.toList (getLast? (head :: tail))
Tactic:
have hnil: tail = [] := List.eq_nil_of_length_eq_zero (Nat.eq_zero_of_le_zero (Nat.le_of_succ_le_succ heq))
Proof state after:
α : Type u_1
head : α
tail : List α
ih : lastN 1 tail = Option.toList (getLast? tail)
heq : Nat.succ (length tail) ≤ 1
hnil : tail = []
⊢ head :: tail = Option.toList (getLast? (head :: tail))
Theorem: List.lastN_one_eq_getLast
Proof state before:
α : Type u_1
head : α
tail : List α
ih : lastN 1 tail = Option.toList (getLast? tail)
heq : Nat.succ (length tail) ≤ 1
hnil : tail = []
⊢ head :: tail = Option.toList (getLast? (head :: tail))
Tactic:
subst tail
Proof state after:
α : Type u_1
head : α
ih : lastN 1 [] = Option.toList (getLast? [])
heq : Nat.succ (length []) ≤ 1
⊢ [head] = Option.toList (getLast? [head])
Theorem: List.lastN_one_eq_getLast
Proof state before:
α : Type u_1
head : α
ih : lastN 1 [] = Option.toList (getLast? [])
heq : Nat.succ (length []) ≤ 1
⊢ [head] = Option.toList (getLast? [head])
Tactic:
simp only [getLast?_singleton, Option.to_list_some]
Proof state after:
no goals
Theorem: List.getLast?_some
Proof state before:
α : Type ?u.93833
l : List α
a : α
h : getLast? l = some a
⊢ l ≠ []
Tactic:
have h₂:= congr_arg Option.isSome h
Proof state after:
α : Type ?u.93833
l : List α
a : α
h : getLast? l = some a
h₂ : Option.isSome (getLast? l) = Option.isSome (some a)
⊢ l ≠ []
Theorem: List.getLast?_some
Proof state before:
α : Type ?u.93833
l : List α
a : α
h : getLast? l = some a
h₂ : Option.isSome (getLast? l) = Option.isSome (some a)
⊢ l ≠ []
Tactic:
simp at h₂
Proof state after:
α : Type ?u.93833
l : List α
a : α
h : getLast? l = some a
h₂ : ¬l = []
⊢ l ≠ []
Theorem: List.getLast?_some
Proof state before:
α : Type ?u.93833
l : List α
a : α
h : getLast? l = some a
h₂ : ¬l = []
⊢ l ≠ []
Tactic:
simp [h₂]
Proof state after:
no goals
Theorem: List.getLast?_some
Proof state before:
α : Type u_1
l : List α
a : α
h : getLast? l = some a
⊢ getLast l (_ : ¬l = []) = a
Tactic:
have h₂:= congr_arg Option.isSome h
Proof state after:
α : Type u_1
l : List α
a : α
h : getLast? l = some a
h₂ : Option.isSome (getLast? l) = Option.isSome (some a)
⊢ getLast l (_ : ¬l = []) = a