internlm/Lean-Github huggingface dataset:
Theorem: List.getLast?_some
Proof state before:
α : Type u_1
l : List α
a : α
h : getLast? l = some a
h₂ : Option.isSome (getLast? l) = Option.isSome (some a)
⊢ getLast l (_ : ¬l = []) = a
Tactic:
simp only [Option.isSome_some, getLast?_isSome, ne_eq] at h₂
Proof state after:
α : Type u_1
l : List α
a : α
h : getLast? l = some a
h₂ : ¬l = []
⊢ getLast l (_ : ¬l = []) = a
Theorem: List.getLast?_some
Proof state before:
α : Type u_1
l : List α
a : α
h : getLast? l = some a
h₂ : ¬l = []
⊢ getLast l (_ : ¬l = []) = a
Tactic:
rw [ List.getLast?_eq_getLast l h₂] at h
Proof state after:
α : Type u_1
l : List α
a : α
h✝ : getLast? l = some a
h₂ : ¬l = []
h : some (getLast l h₂) = some a
⊢ getLast l (_ : ¬l = []) = a
Theorem: List.getLast?_some
Proof state before:
α : Type u_1
l : List α
a : α
h✝ : getLast? l = some a
h₂ : ¬l = []
h : some (getLast l h₂) = some a
⊢ getLast l (_ : ¬l = []) = a
Tactic:
simp_all only [Option.some.injEq]
Proof state after:
no goals
Theorem: List.getLastD_ne_nil
Proof state before:
α✝ : Type u_1
l : List α✝
a : α✝
h : l ≠ []
⊢ getLastD l a = getLast l h
Tactic:
cases l with
| nil => contradiction
| cons hd tl =>
  rw [List.getLastD_cons, List.getLast_eq_getLastD]
Proof state after:
no goals
Theorem: List.getLastD_ne_nil
Proof state before:
case nil
α✝ : Type u_1
a : α✝
h : [] ≠ []
⊢ getLastD [] a = getLast [] h
Tactic:
contradiction
Proof state after:
no goals
Theorem: List.getLastD_ne_nil
Proof state before:
case cons
α✝ : Type u_1
a hd : α✝
tl : List α✝
h : hd :: tl ≠ []
⊢ getLastD (hd :: tl) a = getLast (hd :: tl) h
Tactic:
rw [List.getLastD_cons, List.getLast_eq_getLastD]
Proof state after:
no goals
Theorem: List.get_zero_cons_tail
Proof state before:
α : Type u_1
l : List α
h : 0 < length l
⊢ get l { val := 0, isLt := h } :: tail l = l
Tactic:
cases l with
| nil => simp only [zero_le, ge_iff_le, nonpos_iff_eq_zero, length_nil, lt_self_iff_false] at h
| cons => simp only [get, tail_cons]
Proof state after:
no goals
Theorem: List.get_zero_cons_tail
Proof state before:
case nil
α : Type u_1
h : 0 < length []
⊢ get [] { val := 0, isLt := h } :: tail [] = []
Tactic:
simp only [zero_le, ge_iff_le, nonpos_iff_eq_zero, length_nil, lt_self_iff_false] at h
Proof state after:
no goals
Theorem: List.get_zero_cons_tail
Proof state before:
case cons
α : Type u_1
head✝ : α
tail✝ : List α
h : 0 < length (head✝ :: tail✝)
⊢ get (head✝ :: tail✝) { val := 0, isLt := h } :: tail (head✝ :: tail✝) = head✝ :: tail✝
Tactic:
simp only [get, tail_cons]
Proof state after:
no goals
Theorem: List.lastN_eq_cons_lastN
Proof state before:
α : Type u_1
n : ℕ
l : List α
P : n < length l
⊢ get l { val := length l - 1 - n, isLt := (_ : length l - 1 - n < length l) } :: lastN n l = lastN (n + 1) l
Tactic:
unfold lastN
Proof state after:
α : Type u_1
n : ℕ
l : List α
P : n < length l
⊢ get l { val := length l - 1 - n, isLt := (_ : length l - 1 - n < length l) } :: drop (length l - n) l =
    drop (length l - (n + 1)) l
Theorem: List.lastN_eq_cons_lastN
Proof state before:
α : Type u_1
n : ℕ
l : List α
P : n < length l
⊢ get l { val := length l - 1 - n, isLt := (_ : length l - 1 - n < length l) } :: drop (length l - n) l =
    drop (length l - (n + 1)) l
Tactic:
have h:  length l - (n + 1) < length l := by
  apply Nat.sub_lt_self
  . simp only [zero_le, ge_iff_le, nonpos_iff_eq_zero, add_pos_iff, or_true]
  . simp only [Nat.succ_eq_add_one, P, Nat.succ_le_of_lt]
Proof state after:
α : Type u_1
n : ℕ
l : List α
P : n < length l
h : length l - (n + 1) < length l
⊢ get l { val := length l - 1 - n, isLt := (_ : length l - 1 - n < length l) } :: drop (length l - n) l =
    drop (length l - (n + 1)) l
Theorem: List.lastN_eq_cons_lastN
Proof state before:
α : Type u_1
n : ℕ
l : List α
P : n < length l
h : length l - (n + 1) < length l
⊢ get l { val := length l - 1 - n, isLt := (_ : length l - 1 - n < length l) } :: drop (length l - n) l =
    drop (length l - (n + 1)) l
Tactic:
conv => 
  right
  rw [List.drop_eq_get_cons  (h:=h)]
Proof state after:
α : Type u_1
n : ℕ
l : List α
P : n < length l
h : length l - (n + 1) < length l
⊢ get l { val := length l - 1 - n, isLt := (_ : length l - 1 - n < length l) } :: drop (length l - n) l =
    get l { val := length l - (n + 1), isLt := h } :: drop (length l - (n + 1) + 1) l
Theorem: List.lastN_eq_cons_lastN
Proof state before:
α : Type u_1
n : ℕ
l : List α
P : n < length l
h : length l - (n + 1) < length l
⊢ get l { val := length l - 1 - n, isLt := (_ : length l - 1 - n < length l) } :: drop (length l - n) l =
    get l { val := length l - (n + 1), isLt := h } :: drop (length l - (n + 1) + 1) l
Tactic:
congr 2
Proof state after:
case e_head.e_a
α : Type u_1
n : ℕ
l : List α
P : n < length l
h : length l - (n + 1) < length l
⊢ { val := length l - 1 - n, isLt := (_ : length l - 1 - n < length l) } = { val := length l - (n + 1), isLt := h }

case e_tail.e_a
α : Type u_1
n : ℕ
l : List α
P : n < length l
h : length l - (n + 1) < length l
⊢ length l - n = length l - (n + 1) + 1
Theorem: List.lastN_eq_cons_lastN
Proof state before:
case e_head.e_a
α : Type u_1
n : ℕ
l : List α
P : n < length l
h : length l - (n + 1) < length l
⊢ { val := length l - 1 - n, isLt := (_ : length l - 1 - n < length l) } = { val := length l - (n + 1), isLt := h }

case e_tail.e_a
α : Type u_1
n : ℕ
l : List α
P : n < length l
h : length l - (n + 1) < length l
⊢ length l - n = length l - (n + 1) + 1
Tactic:
. congr 1
  rw [Nat.sub_sub, Nat.add_comm]
Proof state after:
case e_tail.e_a
α : Type u_1
n : ℕ
l : List α
P : n < length l
h : length l - (n + 1) < length l
⊢ length l - n = length l - (n + 1) + 1
Theorem: List.lastN_eq_cons_lastN
Proof state before:
case e_tail.e_a
α : Type u_1
n : ℕ
l : List α
P : n < length l
h : length l - (n + 1) < length l
⊢ length l - n = length l - (n + 1) + 1
Tactic:
. rw [← Nat.sub_sub, Nat.sub_add_cancel]
  apply Nat.le_of_add_le_add_right (b:=n)
  rw [Nat.sub_add_cancel]
  . rw [Nat.add_comm, ← Nat.succ_eq_add_one]
    apply Nat.succ_le_of_lt P
  . simp only [P, Nat.le_of_lt]
Proof state after:
no goals
Theorem: List.lastN_eq_cons_lastN
Proof state before:
α : Type u_1
n : ℕ
l : List α
P : n < length l
⊢ length l - (n + 1) < length l
Tactic:
apply Nat.sub_lt_self
Proof state after:
case h₀
α : Type u_1
n : ℕ
l : List α
P : n < length l
⊢ 0 < n + 1

case h₁
α : Type u_1
n : ℕ
l : List α
P : n < length l
⊢ n + 1 ≤ length l
Theorem: List.lastN_eq_cons_lastN
Proof state before:
case h₀
α : Type u_1
n : ℕ
l : List α
P : n < length l
⊢ 0 < n + 1

case h₁
α : Type u_1
n : ℕ
l : List α
P : n < length l
⊢ n + 1 ≤ length l
Tactic:
. simp only [zero_le, ge_iff_le, nonpos_iff_eq_zero, add_pos_iff, or_true]
Proof state after:
case h₁
α : Type u_1
n : ℕ
l : List α
P : n < length l
⊢ n + 1 ≤ length l
Theorem: List.lastN_eq_cons_lastN
Proof state before:
case h₁
α : Type u_1
n : ℕ
l : List α
P : n < length l
⊢ n + 1 ≤ length l
Tactic:
. simp only [Nat.succ_eq_add_one, P, Nat.succ_le_of_lt]
Proof state after:
no goals
Theorem: List.drop_cons
Proof state before:
α : Type u_1
n : ℕ
head : α
tail : List α
⊢ drop (n + 1) (head :: tail) = drop n tail
Tactic:
simp only [drop, zero_le, ge_iff_le, nonpos_iff_eq_zero, Nat.add_eq, add_zero]
Proof state after:
no goals
Theorem: List.lastN_eq_reverse_take
Proof state before:
α : Type u_1
n : ℕ
l : List α
⊢ lastN n l = reverse (take n (reverse l))
Tactic:
unfold List.lastN
Proof state after:
α : Type u_1
n : ℕ
l : List α
⊢ drop (length l - n) l = reverse (take n (reverse l))
Theorem: List.lastN_eq_reverse_take
Proof state before:
α : Type u_1
n : ℕ
l : List α
⊢ drop (length l - n) l = reverse (take n (reverse l))
Tactic:
induction l generalizing n with
| nil => simp only [length_nil, zero_le, ge_iff_le, nonpos_iff_eq_zero, Nat.zero_sub, tsub_eq_zero_of_le, drop_nil,
reverse_nil, take_nil]
| cons head tail ih =>
  simp only [length_cons, tsub_le_iff_right, ge_iff_le, reverse_cons, length_reverse]
  cases h: decide (n ≤ length tail) with
  | false => 
    simp only [decide_eq_false_iff_not, not_le] at h
    rw [Nat.succ_eq_add_one, Nat.add_comm]
    rw [List.take_length_le, List.reverse_append, List.reverse_reverse]
    simp only [tsub_le_iff_right, ge_iff_le, reverse_cons, reverse_nil, nil_append, singleton_append]
    have heq : 1 + length tail - n = 0 := by 
      simp only [tsub_le_iff_right, ge_iff_le, zero_le, nonpos_iff_eq_zero, tsub_eq_zero_iff_le]
      rw [Nat.add_comm]
      apply Nat.le_of_lt_succ
      rw [Nat.succ_eq_add_one]
      simp only [add_lt_add_iff_right, h]
    rw [heq]
    simp only [drop]
    rw [List.length_append, List.length_reverse]
    simp only [length_singleton]
    exact h
  | true =>
    simp only [decide_eq_true_eq] at h
    rw [Nat.succ_eq_add_one, Nat.add_comm, Nat.add_sub_assoc, Nat.add_comm, List.drop_cons, ih]
    congr 1
    rw [List.take_append_of_le_length]
    . simp only [length_reverse]; apply h
    . apply h
Proof state after:
no goals
Theorem: List.lastN_eq_reverse_take
Proof state before:
case nil
α : Type u_1
n : ℕ
⊢ drop (length [] - n) [] = reverse (take n (reverse []))
Tactic:
simp only [length_nil, zero_le, ge_iff_le, nonpos_iff_eq_zero, Nat.zero_sub, tsub_eq_zero_of_le, drop_nil,
reverse_nil, take_nil]
Proof state after:
no goals
Theorem: List.lastN_eq_reverse_take
Proof state before:
case cons
α : Type u_1
head : α
tail : List α
ih : ∀ (n : ℕ), drop (length tail - n) tail = reverse (take n (reverse tail))
n : ℕ
⊢ drop (length (head :: tail) - n) (head :: tail) = reverse (take n (reverse (head :: tail)))
Tactic:
simp only [length_cons, tsub_le_iff_right, ge_iff_le, reverse_cons, length_reverse]
Proof state after:
case cons
α : Type u_1
head : α
tail : List α
ih : ∀ (n : ℕ), drop (length tail - n) tail = reverse (take n (reverse tail))
n : ℕ
⊢ drop (Nat.succ (length tail) - n) (head :: tail) = reverse (take n (reverse tail ++ [head]))
Theorem: List.lastN_eq_reverse_take
Proof state before:
case cons
α : Type u_1
head : α
tail : List α
ih : ∀ (n : ℕ), drop (length tail - n) tail = reverse (take n (reverse tail))
n : ℕ
⊢ drop (Nat.succ (length tail) - n) (head :: tail) = reverse (take n (reverse tail ++ [head]))
Tactic:
cases h: decide (n ≤ length tail) with
| false => 
  simp only [decide_eq_false_iff_not, not_le] at h
  rw [Nat.succ_eq_add_one, Nat.add_comm]
  rw [List.take_length_le, List.reverse_append, List.reverse_reverse]
  simp only [tsub_le_iff_right, ge_iff_le, reverse_cons, reverse_nil, nil_append, singleton_append]
  have heq : 1 + length tail - n = 0 := by 
    simp only [tsub_le_iff_right, ge_iff_le, zero_le, nonpos_iff_eq_zero, tsub_eq_zero_iff_le]
    rw [Nat.add_comm]
    apply Nat.le_of_lt_succ
    rw [Nat.succ_eq_add_one]
    simp only [add_lt_add_iff_right, h]
  rw [heq]
  simp only [drop]
  rw [List.length_append, List.length_reverse]
  simp only [length_singleton]
  exact h
| true =>
  simp only [decide_eq_true_eq] at h
  rw [Nat.succ_eq_add_one, Nat.add_comm, Nat.add_sub_assoc, Nat.add_comm, List.drop_cons, ih]
  congr 1
  rw [List.take_append_of_le_length]
  . simp only [length_reverse]; apply h
  . apply h
Proof state after:
no goals
Theorem: List.lastN_eq_reverse_take
Proof state before:
case cons.false
α : Type u_1
head : α
tail : List α
ih : ∀ (n : ℕ), drop (length tail - n) tail = reverse (take n (reverse tail))
n : ℕ
h : decide (n ≤ length tail) = false
⊢ drop (Nat.succ (length tail) - n) (head :: tail) = reverse (take n (reverse tail ++ [head]))
Tactic:
simp only [decide_eq_false_iff_not, not_le] at h
Proof state after:
case cons.false
α : Type u_1
head : α
tail : List α
ih : ∀ (n : ℕ), drop (length tail - n) tail = reverse (take n (reverse tail))
n : ℕ
h : length tail < n
⊢ drop (Nat.succ (length tail) - n) (head :: tail) = reverse (take n (reverse tail ++ [head]))
Theorem: List.lastN_eq_reverse_take
Proof state before:
case cons.false
α : Type u_1
head : α
tail : List α
ih : ∀ (n : ℕ), drop (length tail - n) tail = reverse (take n (reverse tail))
n : ℕ
h : length tail < n
⊢ drop (Nat.succ (length tail) - n) (head :: tail) = reverse (take n (reverse tail ++ [head]))
Tactic:
rw [Nat.succ_eq_add_one, Nat.add_comm]
Proof state after:
case cons.false
α : Type u_1
head : α
tail : List α
ih : ∀ (n : ℕ), drop (length tail - n) tail = reverse (take n (reverse tail))
n : ℕ
h : length tail < n
⊢ drop (1 + length tail - n) (head :: tail) = reverse (take n (reverse tail ++ [head]))
Theorem: List.lastN_eq_reverse_take
Proof state before:
case cons.false
α : Type u_1
head : α
tail : List α
ih : ∀ (n : ℕ), drop (length tail - n) tail = reverse (take n (reverse tail))
n : ℕ
h : length tail < n
⊢ drop (1 + length tail - n) (head :: tail) = reverse (take n (reverse tail ++ [head]))
Tactic:
rw [List.take_length_le, List.reverse_append, List.reverse_reverse]
Proof state after:
case cons.false
α : Type u_1
head : α
tail : List α
ih : ∀ (n : ℕ), drop (length tail - n) tail = reverse (take n (reverse tail))
n : ℕ
h : length tail < n
⊢ drop (1 + length tail - n) (head :: tail) = reverse [head] ++ tail

case cons.false
α : Type u_1
head : α
tail : List α
ih : ∀ (n : ℕ), drop (length tail - n) tail = reverse (take n (reverse tail))
n : ℕ
h : length tail < n
⊢ length (reverse tail ++ [head]) ≤ n
Theorem: List.lastN_eq_reverse_take
Proof state before:
case cons.false
α : Type u_1
head : α
tail : List α
ih : ∀ (n : ℕ), drop (length tail - n) tail = reverse (take n (reverse tail))
n : ℕ
h : length tail < n
⊢ drop (1 + length tail - n) (head :: tail) = reverse [head] ++ tail

case cons.false
α : Type u_1
head : α
tail : List α
ih : ∀ (n : ℕ), drop (length tail - n) tail = reverse (take n (reverse tail))
n : ℕ
h : length tail < n
⊢ length (reverse tail ++ [head]) ≤ n
Tactic:
simp only [tsub_le_iff_right, ge_iff_le, reverse_cons, reverse_nil, nil_append, singleton_append]
Proof state after:
case cons.false
α : Type u_1
head : α
tail : List α
ih : ∀ (n : ℕ), drop (length tail - n) tail = reverse (take n (reverse tail))
n : ℕ
h : length tail < n
⊢ drop (1 + length tail - n) (head :: tail) = head :: tail

case cons.false
α : Type u_1
head : α
tail : List α
ih : ∀ (n : ℕ), drop (length tail - n) tail = reverse (take n (reverse tail))
n : ℕ
h : length tail < n
⊢ length (reverse tail ++ [head]) ≤ n
Theorem: List.lastN_eq_reverse_take
Proof state before:
case cons.false
α : Type u_1
head : α
tail : List α
ih : ∀ (n : ℕ), drop (length tail - n) tail = reverse (take n (reverse tail))
n : ℕ
h : length tail < n
⊢ drop (1 + length tail - n) (head :: tail) = head :: tail

case cons.false
α : Type u_1
head : α
tail : List α
ih : ∀ (n : ℕ), drop (length tail - n) tail = reverse (take n (reverse tail))
n : ℕ
h : length tail < n
⊢ length (reverse tail ++ [head]) ≤ n
Tactic:
have heq : 1 + length tail - n = 0 := by 
  simp only [tsub_le_iff_right, ge_iff_le, zero_le, nonpos_iff_eq_zero, tsub_eq_zero_iff_le]
  rw [Nat.add_comm]
  apply Nat.le_of_lt_succ
  rw [Nat.succ_eq_add_one]
  simp only [add_lt_add_iff_right, h]
Proof state after:
case cons.false
α : Type u_1
head : α
tail : List α
ih : ∀ (n : ℕ), drop (length tail - n) tail = reverse (take n (reverse tail))
n : ℕ
h : length tail < n
heq : 1 + length tail - n = 0
⊢ drop (1 + length tail - n) (head :: tail) = head :: tail

case cons.false
α : Type u_1
head : α
tail : List α
ih : ∀ (n : ℕ), drop (length tail - n) tail = reverse (take n (reverse tail))
n : ℕ
h : length tail < n
⊢ length (reverse tail ++ [head]) ≤ n
Theorem: List.lastN_eq_reverse_take
Proof state before:
case cons.false
α : Type u_1
head : α
tail : List α
ih : ∀ (n : ℕ), drop (length tail - n) tail = reverse (take n (reverse tail))
n : ℕ
h : length tail < n
heq : 1 + length tail - n = 0
⊢ drop (1 + length tail - n) (head :: tail) = head :: tail

case cons.false
α : Type u_1
head : α
tail : List α
ih : ∀ (n : ℕ), drop (length tail - n) tail = reverse (take n (reverse tail))
n : ℕ
h : length tail < n
⊢ length (reverse tail ++ [head]) ≤ n
Tactic:
rw [heq]
Proof state after:
case cons.false
α : Type u_1
head : α
tail : List α
ih : ∀ (n : ℕ), drop (length tail - n) tail = reverse (take n (reverse tail))
n : ℕ
h : length tail < n
heq : 1 + length tail - n = 0
⊢ drop 0 (head :: tail) = head :: tail

case cons.false
α : Type u_1
head : α
tail : List α
ih : ∀ (n : ℕ), drop (length tail - n) tail = reverse (take n (reverse tail))
n : ℕ
h : length tail < n
⊢ length (reverse tail ++ [head]) ≤ n
Theorem: List.lastN_eq_reverse_take
Proof state before:
case cons.false
α : Type u_1
head : α
tail : List α
ih : ∀ (n : ℕ), drop (length tail - n) tail = reverse (take n (reverse tail))
n : ℕ
h : length tail < n
heq : 1 + length tail - n = 0
⊢ drop 0 (head :: tail) = head :: tail

case cons.false
α : Type u_1
head : α
tail : List α
ih : ∀ (n : ℕ), drop (length tail - n) tail = reverse (take n (reverse tail))
n : ℕ
h : length tail < n
⊢ length (reverse tail ++ [head]) ≤ n
Tactic:
simp only [drop]
Proof state after:
case cons.false
α : Type u_1
head : α
tail : List α
ih : ∀ (n : ℕ), drop (length tail - n) tail = reverse (take n (reverse tail))
n : ℕ
h : length tail < n
⊢ length (reverse tail ++ [head]) ≤ n
Theorem: List.lastN_eq_reverse_take
Proof state before:
case cons.false
α : Type u_1
head : α
tail : List α
ih : ∀ (n : ℕ), drop (length tail - n) tail = reverse (take n (reverse tail))
n : ℕ
h : length tail < n
⊢ length (reverse tail ++ [head]) ≤ n
Tactic:
rw [List.length_append, List.length_reverse]
Proof state after:
case cons.false
α : Type u_1
head : α
tail : List α
ih : ∀ (n : ℕ), drop (length tail - n) tail = reverse (take n (reverse tail))
n : ℕ
h : length tail < n
⊢ length tail + length [head] ≤ n
Theorem: List.lastN_eq_reverse_take
Proof state before:
case cons.false
α : Type u_1
head : α
tail : List α
ih : ∀ (n : ℕ), drop (length tail - n) tail = reverse (take n (reverse tail))
n : ℕ
h : length tail < n
⊢ length tail + length [head] ≤ n
Tactic:
simp only [length_singleton]
Proof state after:
case cons.false
α : Type u_1
head : α
tail : List α
ih : ∀ (n : ℕ), drop (length tail - n) tail = reverse (take n (reverse tail))
n : ℕ
h : length tail < n
⊢ length tail + 1 ≤ n
Theorem: List.lastN_eq_reverse_take
Proof state before:
case cons.false
α : Type u_1
head : α
tail : List α
ih : ∀ (n : ℕ), drop (length tail - n) tail = reverse (take n (reverse tail))
n : ℕ
h : length tail < n
⊢ length tail + 1 ≤ n
Tactic:
exact h
Proof state after:
no goals
Theorem: List.lastN_eq_reverse_take
Proof state before:
α : Type u_1
head : α
tail : List α
ih : ∀ (n : ℕ), drop (length tail - n) tail = reverse (take n (reverse tail))
n : ℕ
h : length tail < n
⊢ 1 + length tail - n = 0
Tactic:
simp only [tsub_le_iff_right, ge_iff_le, zero_le, nonpos_iff_eq_zero, tsub_eq_zero_iff_le]
Proof state after:
α : Type u_1
head : α
tail : List α
ih : ∀ (n : ℕ), drop (length tail - n) tail = reverse (take n (reverse tail))
n : ℕ
h : length tail < n
⊢ 1 + length tail ≤ n
Theorem: List.lastN_eq_reverse_take
Proof state before:
α : Type u_1
head : α
tail : List α
ih : ∀ (n : ℕ), drop (length tail - n) tail = reverse (take n (reverse tail))
n : ℕ
h : length tail < n
⊢ 1 + length tail ≤ n
Tactic:
rw [Nat.add_comm]
Proof state after:
α : Type u_1
head : α
tail : List α
ih : ∀ (n : ℕ), drop (length tail - n) tail = reverse (take n (reverse tail))
n : ℕ
h : length tail < n
⊢ length tail + 1 ≤ n
Theorem: List.lastN_eq_reverse_take
Proof state before:
α : Type u_1
head : α
tail : List α
ih : ∀ (n : ℕ), drop (length tail - n) tail = reverse (take n (reverse tail))
n : ℕ
h : length tail < n
⊢ length tail + 1 ≤ n
Tactic:
apply Nat.le_of_lt_succ
Proof state after:
case a
α : Type u_1
head : α
tail : List α
ih : ∀ (n : ℕ), drop (length tail - n) tail = reverse (take n (reverse tail))
n : ℕ
h : length tail < n
⊢ length tail + 1 < Nat.succ n
Theorem: List.lastN_eq_reverse_take
Proof state before:
case a
α : Type u_1
head : α
tail : List α
ih : ∀ (n : ℕ), drop (length tail - n) tail = reverse (take n (reverse tail))
n : ℕ
h : length tail < n
⊢ length tail + 1 < Nat.succ n
Tactic:
rw [Nat.succ_eq_add_one]
Proof state after:
case a
α : Type u_1
head : α
tail : List α
ih : ∀ (n : ℕ), drop (length tail - n) tail = reverse (take n (reverse tail))
n : ℕ
h : length tail < n
⊢ length tail + 1 < n + 1
Theorem: List.lastN_eq_reverse_take
Proof state before:
case a
α : Type u_1
head : α
tail : List α
ih : ∀ (n : ℕ), drop (length tail - n) tail = reverse (take n (reverse tail))
n : ℕ
h : length tail < n
⊢ length tail + 1 < n + 1
Tactic:
simp only [add_lt_add_iff_right, h]
Proof state after:
no goals
Theorem: List.lastN_eq_reverse_take
Proof state before:
case cons.true
α : Type u_1
head : α
tail : List α
ih : ∀ (n : ℕ), drop (length tail - n) tail = reverse (take n (reverse tail))
n : ℕ
h : decide (n ≤ length tail) = true
⊢ drop (Nat.succ (length tail) - n) (head :: tail) = reverse (take n (reverse tail ++ [head]))
Tactic:
simp only [decide_eq_true_eq] at h
Proof state after:
case cons.true
α : Type u_1
head : α
tail : List α
ih : ∀ (n : ℕ), drop (length tail - n) tail = reverse (take n (reverse tail))
n : ℕ
h : n ≤ length tail
⊢ drop (Nat.succ (length tail) - n) (head :: tail) = reverse (take n (reverse tail ++ [head]))
Theorem: List.lastN_eq_reverse_take
Proof state before:
case cons.true
α : Type u_1
head : α
tail : List α
ih : ∀ (n : ℕ), drop (length tail - n) tail = reverse (take n (reverse tail))
n : ℕ
h : n ≤ length tail
⊢ drop (Nat.succ (length tail) - n) (head :: tail) = reverse (take n (reverse tail ++ [head]))
Tactic:
rw [Nat.succ_eq_add_one, Nat.add_comm, Nat.add_sub_assoc, Nat.add_comm, List.drop_cons, ih]
Proof state after:
case cons.true
α : Type u_1
head : α
tail : List α
ih : ∀ (n : ℕ), drop (length tail - n) tail = reverse (take n (reverse tail))
n : ℕ
h : n ≤ length tail
⊢ reverse (take n (reverse tail)) = reverse (take n (reverse tail ++ [head]))

case cons.true.h
α : Type u_1
head : α
tail : List α
ih : ∀ (n : ℕ), drop (length tail - n) tail = reverse (take n (reverse tail))
n : ℕ
h : n ≤ length tail
⊢ n ≤ length tail
Theorem: List.lastN_eq_reverse_take
Proof state before:
case cons.true
α : Type u_1
head : α
tail : List α
ih : ∀ (n : ℕ), drop (length tail - n) tail = reverse (take n (reverse tail))
n : ℕ
h : n ≤ length tail
⊢ reverse (take n (reverse tail)) = reverse (take n (reverse tail ++ [head]))

case cons.true.h
α : Type u_1
head : α
tail : List α
ih : ∀ (n : ℕ), drop (length tail - n) tail = reverse (take n (reverse tail))
n : ℕ
h : n ≤ length tail
⊢ n ≤ length tail
Tactic:
congr 1
Proof state after:
case cons.true.e_as
α : Type u_1
head : α
tail : List α
ih : ∀ (n : ℕ), drop (length tail - n) tail = reverse (take n (reverse tail))
n : ℕ
h : n ≤ length tail
⊢ take n (reverse tail) = take n (reverse tail ++ [head])

case cons.true.h
α : Type u_1
head : α
tail : List α
ih : ∀ (n : ℕ), drop (length tail - n) tail = reverse (take n (reverse tail))
n : ℕ
h : n ≤ length tail
⊢ n ≤ length tail
Theorem: List.lastN_eq_reverse_take
Proof state before:
case cons.true.e_as
α : Type u_1
head : α
tail : List α
ih : ∀ (n : ℕ), drop (length tail - n) tail = reverse (take n (reverse tail))
n : ℕ
h : n ≤ length tail
⊢ take n (reverse tail) = take n (reverse tail ++ [head])

case cons.true.h
α : Type u_1
head : α
tail : List α
ih : ∀ (n : ℕ), drop (length tail - n) tail = reverse (take n (reverse tail))
n : ℕ
h : n ≤ length tail
⊢ n ≤ length tail
Tactic:
rw [List.take_append_of_le_length]
Proof state after:
case cons.true.e_as
α : Type u_1
head : α
tail : List α
ih : ∀ (n : ℕ), drop (length tail - n) tail = reverse (take n (reverse tail))
n : ℕ
h : n ≤ length tail
⊢ n ≤ length (reverse tail)

case cons.true.h
α : Type u_1
head : α
tail : List α
ih : ∀ (n : ℕ), drop (length tail - n) tail = reverse (take n (reverse tail))
n : ℕ
h : n ≤ length tail
⊢ n ≤ length tail
Theorem: List.lastN_eq_reverse_take
Proof state before:
case cons.true.e_as
α : Type u_1
head : α
tail : List α
ih : ∀ (n : ℕ), drop (length tail - n) tail = reverse (take n (reverse tail))
n : ℕ
h : n ≤ length tail
⊢ n ≤ length (reverse tail)

case cons.true.h
α : Type u_1
head : α
tail : List α
ih : ∀ (n : ℕ), drop (length tail - n) tail = reverse (take n (reverse tail))
n : ℕ
h : n ≤ length tail
⊢ n ≤ length tail
Tactic:
. simp only [length_reverse]; apply h
Proof state after:
case cons.true.h
α : Type u_1
head : α
tail : List α
ih : ∀ (n : ℕ), drop (length tail - n) tail = reverse (take n (reverse tail))
n : ℕ
h : n ≤ length tail
⊢ n ≤ length tail