internlm/Lean-Github huggingface dataset:
Theorem: List.split_length_fst
Proof state before:
case h.a.a
α : Type u_1
x₁ x₂ x x' : α
xs : List α
ih : length xs + 1 + 1 ≤ 1 ∨ length (split xs).fst + 1 < length xs + 1 + 1
⊢ length (split xs).fst + 1 < length xs + 2
Tactic:
cases ih with
| inl _ => contradiction
| inr h => apply h
Proof state after:
no goals
Theorem: List.split_length_fst
Proof state before:
case h.a.a.inl
α : Type u_1
x₁ x₂ x x' : α
xs : List α
h✝ : length xs + 1 + 1 ≤ 1
⊢ length (split xs).fst + 1 < length xs + 2
Tactic:
contradiction
Proof state after:
no goals
Theorem: List.split_length_fst
Proof state before:
case h.a.a.inr
α : Type u_1
x₁ x₂ x x' : α
xs : List α
h : length (split xs).fst + 1 < length xs + 1 + 1
⊢ length (split xs).fst + 1 < length xs + 2
Tactic:
apply h
Proof state after:
no goals
Theorem: List.split_length_snd
Proof state before:
α : Type u_1
x₁ x₂ x : α
xs : List α
ih : x :: xs = [] ∨ length (split (x :: xs)).snd < length (x :: xs)
⊢ x₁ :: x₂ :: x :: xs = [] ∨ length (split (x₁ :: x₂ :: x :: xs)).snd < length (x₁ :: x₂ :: x :: xs)
Tactic:
simp only [split, length]
Proof state after:
α : Type u_1
x₁ x₂ x : α
xs : List α
ih : x :: xs = [] ∨ length (split (x :: xs)).snd < length (x :: xs)
⊢ False ∨ length (split (x :: xs)).snd + 1 < length xs + 1 + 1 + 1
Theorem: List.split_length_snd
Proof state before:
α : Type u_1
x₁ x₂ x : α
xs : List α
ih : x :: xs = [] ∨ length (split (x :: xs)).snd < length (x :: xs)
⊢ False ∨ length (split (x :: xs)).snd + 1 < length xs + 1 + 1 + 1
Tactic:
apply Or.intro_right
Proof state after:
case h
α : Type u_1
x₁ x₂ x : α
xs : List α
ih : x :: xs = [] ∨ length (split (x :: xs)).snd < length (x :: xs)
⊢ length (split (x :: xs)).snd + 1 < length xs + 1 + 1 + 1
Theorem: List.split_length_snd
Proof state before:
case h
α : Type u_1
x₁ x₂ x : α
xs : List α
ih : x :: xs = [] ∨ length (split (x :: xs)).snd < length (x :: xs)
⊢ length (split (x :: xs)).snd + 1 < length xs + 1 + 1 + 1
Tactic:
apply Nat.succ_lt_succ
Proof state after:
case h.a
α : Type u_1
x₁ x₂ x : α
xs : List α
ih : x :: xs = [] ∨ length (split (x :: xs)).snd < length (x :: xs)
⊢ length (split (x :: xs)).snd < length xs + 2
Theorem: List.split_length_snd
Proof state before:
case h.a
α : Type u_1
x₁ x₂ x : α
xs : List α
ih : x :: xs = [] ∨ length (split (x :: xs)).snd < length (x :: xs)
⊢ length (split (x :: xs)).snd < length xs + 2
Tactic:
simp at ih
Proof state after:
case h.a
α : Type u_1
x₁ x₂ x : α
xs : List α
ih : length (split (x :: xs)).snd < Nat.succ (length xs)
⊢ length (split (x :: xs)).snd < length xs + 2
Theorem: List.split_length_snd
Proof state before:
case h.a
α : Type u_1
x₁ x₂ x : α
xs : List α
ih : length (split (x :: xs)).snd < Nat.succ (length xs)
⊢ length (split (x :: xs)).snd < length xs + 2
Tactic:
apply Nat.lt.step
Proof state after:
case h.a.a
α : Type u_1
x₁ x₂ x : α
xs : List α
ih : length (split (x :: xs)).snd < Nat.succ (length xs)
⊢ length (split (x :: xs)).snd < length xs + 1
Theorem: List.split_length_snd
Proof state before:
case h.a.a
α : Type u_1
x₁ x₂ x : α
xs : List α
ih : length (split (x :: xs)).snd < Nat.succ (length xs)
⊢ length (split (x :: xs)).snd < length xs + 1
Tactic:
apply ih
Proof state after:
no goals
Theorem: List.split_length_snd'
Proof state before:
α : Type u_1
x₁ x₂ : α
xs : List α
ih : length (split xs).snd ≤ length xs
⊢ length (split (x₁ :: x₂ :: xs)).snd ≤ length (x₁ :: x₂ :: xs)
Tactic:
simp only [split, length]
Proof state after:
α : Type u_1
x₁ x₂ : α
xs : List α
ih : length (split xs).snd ≤ length xs
⊢ length (split xs).snd + 1 ≤ length xs + 1 + 1
Theorem: List.split_length_snd'
Proof state before:
α : Type u_1
x₁ x₂ : α
xs : List α
ih : length (split xs).snd ≤ length xs
⊢ length (split xs).snd + 1 ≤ length xs + 1 + 1
Tactic:
apply Nat.le.step
Proof state after:
case a
α : Type u_1
x₁ x₂ : α
xs : List α
ih : length (split xs).snd ≤ length xs
⊢ Nat.le (length (split xs).snd + 1) (length xs + 1)
Theorem: List.split_length_snd'
Proof state before:
case a
α : Type u_1
x₁ x₂ : α
xs : List α
ih : length (split xs).snd ≤ length xs
⊢ Nat.le (length (split xs).snd + 1) (length xs + 1)
Tactic:
apply Nat.succ_le_succ
Proof state after:
case a.a
α : Type u_1
x₁ x₂ : α
xs : List α
ih : length (split xs).snd ≤ length xs
⊢ length (split xs).snd ≤ length xs
Theorem: List.split_length_snd'
Proof state before:
case a.a
α : Type u_1
x₁ x₂ : α
xs : List α
ih : length (split xs).snd ≤ length xs
⊢ length (split xs).snd ≤ length xs
Tactic:
apply ih
Proof state after:
no goals
Theorem: List.zip_length_eq_of_length_eq
Proof state before:
α : Type u_1
β : Type u_2
x : α
xs : List α
y : β
ys : List β
h : length (x :: xs) = length (y :: ys)
⊢ length xs = length ys
Tactic:
simp only [List.length] at h
Proof state after:
α : Type u_1
β : Type u_2
x : α
xs : List α
y : β
ys : List β
h : length xs + 1 = length ys + 1
⊢ length xs = length ys
Theorem: List.zip_length_eq_of_length_eq
Proof state before:
α : Type u_1
β : Type u_2
x : α
xs : List α
y : β
ys : List β
h : length xs + 1 = length ys + 1
⊢ length xs = length ys
Tactic:
apply Nat.succ.inj
Proof state after:
case x
α : Type u_1
β : Type u_2
x : α
xs : List α
y : β
ys : List β
h : length xs + 1 = length ys + 1
⊢ Nat.succ (length xs) = Nat.succ (length ys)
Theorem: List.zip_length_eq_of_length_eq
Proof state before:
case x
α : Type u_1
β : Type u_2
x : α
xs : List α
y : β
ys : List β
h : length xs + 1 = length ys + 1
⊢ Nat.succ (length xs) = Nat.succ (length ys)
Tactic:
apply h
Proof state after:
no goals
Theorem: List.length_prod
Proof state before:
α : Type u_1
β : Type u_2
x✝ : List β
⊢ length (prod [] x✝) = length [] * length x✝
Tactic:
simp [prod, length]
Proof state after:
no goals
Theorem: List.length_prod
Proof state before:
α : Type u_1
β : Type u_2
x : α
xs : List α
⊢ length (prod (x :: xs) []) = length (x :: xs) * length []
Tactic:
simp [prod, length]
Proof state after:
no goals
Theorem: List.length_prod
Proof state before:
α : Type u_1
β : Type u_2
x : α
y : β
ys : List β
ih : length (prod [x] ys) = length [x] * length ys
⊢ length (prod [x] (y :: ys)) = length [x] * length (y :: ys)
Tactic:
simp only [prod]
Proof state after:
α : Type u_1
β : Type u_2
x : α
y : β
ys : List β
ih : length (prod [x] ys) = length [x] * length ys
⊢ length ((x, y) :: prod [x] ys) = length [x] * length (y :: ys)
Theorem: List.length_prod
Proof state before:
α : Type u_1
β : Type u_2
x : α
y : β
ys : List β
ih : length (prod [x] ys) = length [x] * length ys
⊢ length ((x, y) :: prod [x] ys) = length [x] * length (y :: ys)
Tactic:
unfold length
Proof state after:
α : Type u_1
β : Type u_2
x : α
y : β
ys : List β
ih : length (prod [x] ys) = length [x] * length ys
⊢ length (prod [x] ys) + 1 = (length [] + 1) * (length ys + 1)
Theorem: List.length_prod
Proof state before:
α : Type u_1
β : Type u_2
x : α
y : β
ys : List β
ih : length (prod [x] ys) = length [x] * length ys
⊢ length (prod [x] ys) + 1 = (length [] + 1) * (length ys + 1)
Tactic:
rw [ih]
Proof state after:
α : Type u_1
β : Type u_2
x : α
y : β
ys : List β
ih : length (prod [x] ys) = length [x] * length ys
⊢ length [x] * length ys + 1 = (length [] + 1) * (length ys + 1)
Theorem: List.length_prod
Proof state before:
α : Type u_1
β : Type u_2
x : α
y : β
ys : List β
ih : length (prod [x] ys) = length [x] * length ys
⊢ length [x] * length ys + 1 = (length [] + 1) * (length ys + 1)
Tactic:
simp only [length]
Proof state after:
α : Type u_1
β : Type u_2
x : α
y : β
ys : List β
ih : length (prod [x] ys) = length [x] * length ys
⊢ (0 + 1) * length ys + 1 = (0 + 1) * (length ys + 1)
Theorem: List.length_prod
Proof state before:
α : Type u_1
β : Type u_2
x : α
y : β
ys : List β
ih : length (prod [x] ys) = length [x] * length ys
⊢ (0 + 1) * length ys + 1 = (0 + 1) * (length ys + 1)
Tactic:
rw [Nat.one_mul, Nat.one_mul]
Proof state after:
no goals
Theorem: List.length_prod
Proof state before:
α : Type u_1
β : Type u_2
x x' : α
xs : List α
y : β
ys : List β
⊢ Nat.succ 0 + Nat.succ (length ys) < Nat.succ (Nat.succ (length xs)) + Nat.succ (length ys)
Tactic:
apply Nat.add_lt_add_of_lt
Proof state after:
case a
α : Type u_1
β : Type u_2
x x' : α
xs : List α
y : β
ys : List β
⊢ Nat.succ 0 < Nat.succ (Nat.succ (length xs))
Theorem: List.length_prod
Proof state before:
case a
α : Type u_1
β : Type u_2
x x' : α
xs : List α
y : β
ys : List β
⊢ Nat.succ 0 < Nat.succ (Nat.succ (length xs))
Tactic:
apply Nat.succ_lt_succ $ Nat.succ_pos (length xs)
Proof state after:
no goals
Theorem: List.length_prod
Proof state before:
α : Type u_1
β : Type u_2
x x' : α
xs : List α
y : β
ys : List β
h_term₁ : Nat.succ 0 + Nat.succ (length ys) < Nat.succ (Nat.succ (length xs)) + Nat.succ (length ys)
⊢ Nat.succ (length xs) + Nat.succ (length ys) < Nat.succ (Nat.succ (length xs)) + Nat.succ (length ys)
Tactic:
apply Nat.add_lt_add_of_lt
Proof state after:
case a
α : Type u_1
β : Type u_2
x x' : α
xs : List α
y : β
ys : List β
h_term₁ : Nat.succ 0 + Nat.succ (length ys) < Nat.succ (Nat.succ (length xs)) + Nat.succ (length ys)
⊢ Nat.succ (length xs) < Nat.succ (Nat.succ (length xs))
Theorem: List.length_prod
Proof state before:
case a
α : Type u_1
β : Type u_2
x x' : α
xs : List α
y : β
ys : List β
h_term₁ : Nat.succ 0 + Nat.succ (length ys) < Nat.succ (Nat.succ (length xs)) + Nat.succ (length ys)
⊢ Nat.succ (length xs) < Nat.succ (Nat.succ (length xs))
Tactic:
apply Nat.succ_lt_succ
Proof state after:
case a.a
α : Type u_1
β : Type u_2
x x' : α
xs : List α
y : β
ys : List β
h_term₁ : Nat.succ 0 + Nat.succ (length ys) < Nat.succ (Nat.succ (length xs)) + Nat.succ (length ys)
⊢ length xs < length xs + 1
Theorem: List.length_prod
Proof state before:
case a.a
α : Type u_1
β : Type u_2
x x' : α
xs : List α
y : β
ys : List β
h_term₁ : Nat.succ 0 + Nat.succ (length ys) < Nat.succ (Nat.succ (length xs)) + Nat.succ (length ys)
⊢ length xs < length xs + 1
Tactic:
apply Nat.lt.base
Proof state after:
no goals
Theorem: List.length_prod
Proof state before:
α : Type u_1
β : Type u_2
x x' : α
xs : List α
y : β
ys : List β
h_term₁ : Nat.succ 0 + Nat.succ (length ys) < Nat.succ (Nat.succ (length xs)) + Nat.succ (length ys)
h_term₂ : Nat.succ (length xs) + Nat.succ (length ys) < Nat.succ (Nat.succ (length xs)) + Nat.succ (length ys)
ih₁ : length (prod [x] (y :: ys)) = length [x] * length (y :: ys)
ih₂ : length (prod (x' :: xs) (y :: ys)) = length (x' :: xs) * length (y :: ys)
⊢ length (prod (x :: x' :: xs) (y :: ys)) = length (x :: x' :: xs) * length (y :: ys)
Tactic:
unfold prod
Proof state after:
α : Type u_1
β : Type u_2
x x' : α
xs : List α
y : β
ys : List β
h_term₁ : Nat.succ 0 + Nat.succ (length ys) < Nat.succ (Nat.succ (length xs)) + Nat.succ (length ys)
h_term₂ : Nat.succ (length xs) + Nat.succ (length ys) < Nat.succ (Nat.succ (length xs)) + Nat.succ (length ys)
ih₁ : length (prod [x] (y :: ys)) = length [x] * length (y :: ys)
ih₂ : length (prod (x' :: xs) (y :: ys)) = length (x' :: xs) * length (y :: ys)
⊢ length
      (let_fun h₁ := (_ : Nat.succ 0 + length (y :: ys) < Nat.succ (Nat.succ (length xs)) + length (y :: ys));
      let_fun h₂ := (_ : Nat.succ (length xs) + length (y :: ys) < Nat.succ (Nat.succ (length xs)) + length (y :: ys));
      prod [x] (y :: ys) ++ prod (x' :: xs) (y :: ys)) =
    length (x :: x' :: xs) * length (y :: ys)
Theorem: List.length_prod
Proof state before:
α : Type u_1
β : Type u_2
x x' : α
xs : List α
y : β
ys : List β
h_term₁ : Nat.succ 0 + Nat.succ (length ys) < Nat.succ (Nat.succ (length xs)) + Nat.succ (length ys)
h_term₂ : Nat.succ (length xs) + Nat.succ (length ys) < Nat.succ (Nat.succ (length xs)) + Nat.succ (length ys)
ih₁ : length (prod [x] (y :: ys)) = length [x] * length (y :: ys)
ih₂ : length (prod (x' :: xs) (y :: ys)) = length (x' :: xs) * length (y :: ys)
⊢ length
      (let_fun h₁ := (_ : Nat.succ 0 + length (y :: ys) < Nat.succ (Nat.succ (length xs)) + length (y :: ys));
      let_fun h₂ := (_ : Nat.succ (length xs) + length (y :: ys) < Nat.succ (Nat.succ (length xs)) + length (y :: ys));
      prod [x] (y :: ys) ++ prod (x' :: xs) (y :: ys)) =
    length (x :: x' :: xs) * length (y :: ys)
Tactic:
simp only
Proof state after:
α : Type u_1
β : Type u_2
x x' : α
xs : List α
y : β
ys : List β
h_term₁ : Nat.succ 0 + Nat.succ (length ys) < Nat.succ (Nat.succ (length xs)) + Nat.succ (length ys)
h_term₂ : Nat.succ (length xs) + Nat.succ (length ys) < Nat.succ (Nat.succ (length xs)) + Nat.succ (length ys)
ih₁ : length (prod [x] (y :: ys)) = length [x] * length (y :: ys)
ih₂ : length (prod (x' :: xs) (y :: ys)) = length (x' :: xs) * length (y :: ys)
⊢ length (prod [x] (y :: ys) ++ prod (x' :: xs) (y :: ys)) = length (x :: x' :: xs) * length (y :: ys)
Theorem: List.length_prod
Proof state before:
α : Type u_1
β : Type u_2
x x' : α
xs : List α
y : β
ys : List β
h_term₁ : Nat.succ 0 + Nat.succ (length ys) < Nat.succ (Nat.succ (length xs)) + Nat.succ (length ys)
h_term₂ : Nat.succ (length xs) + Nat.succ (length ys) < Nat.succ (Nat.succ (length xs)) + Nat.succ (length ys)
ih₁ : length (prod [x] (y :: ys)) = length [x] * length (y :: ys)
ih₂ : length (prod (x' :: xs) (y :: ys)) = length (x' :: xs) * length (y :: ys)
⊢ length (prod [x] (y :: ys) ++ prod (x' :: xs) (y :: ys)) = length (x :: x' :: xs) * length (y :: ys)
Tactic:
rw [List.length_append, ih₁, ih₂]
Proof state after:
α : Type u_1
β : Type u_2
x x' : α
xs : List α
y : β
ys : List β
h_term₁ : Nat.succ 0 + Nat.succ (length ys) < Nat.succ (Nat.succ (length xs)) + Nat.succ (length ys)
h_term₂ : Nat.succ (length xs) + Nat.succ (length ys) < Nat.succ (Nat.succ (length xs)) + Nat.succ (length ys)
ih₁ : length (prod [x] (y :: ys)) = length [x] * length (y :: ys)
ih₂ : length (prod (x' :: xs) (y :: ys)) = length (x' :: xs) * length (y :: ys)
⊢ length [x] * length (y :: ys) + length (x' :: xs) * length (y :: ys) = length (x :: x' :: xs) * length (y :: ys)
Theorem: List.length_prod
Proof state before:
α : Type u_1
β : Type u_2
x x' : α
xs : List α
y : β
ys : List β
h_term₁ : Nat.succ 0 + Nat.succ (length ys) < Nat.succ (Nat.succ (length xs)) + Nat.succ (length ys)
h_term₂ : Nat.succ (length xs) + Nat.succ (length ys) < Nat.succ (Nat.succ (length xs)) + Nat.succ (length ys)
ih₁ : length (prod [x] (y :: ys)) = length [x] * length (y :: ys)
ih₂ : length (prod (x' :: xs) (y :: ys)) = length (x' :: xs) * length (y :: ys)
⊢ length [x] * length (y :: ys) + length (x' :: xs) * length (y :: ys) = length (x :: x' :: xs) * length (y :: ys)
Tactic:
simp only [length]
Proof state after:
α : Type u_1
β : Type u_2
x x' : α
xs : List α
y : β
ys : List β
h_term₁ : Nat.succ 0 + Nat.succ (length ys) < Nat.succ (Nat.succ (length xs)) + Nat.succ (length ys)
h_term₂ : Nat.succ (length xs) + Nat.succ (length ys) < Nat.succ (Nat.succ (length xs)) + Nat.succ (length ys)
ih₁ : length (prod [x] (y :: ys)) = length [x] * length (y :: ys)
ih₂ : length (prod (x' :: xs) (y :: ys)) = length (x' :: xs) * length (y :: ys)
⊢ (0 + 1) * (length ys + 1) + (length xs + 1) * (length ys + 1) = (length xs + 1 + 1) * (length ys + 1)
Theorem: List.length_prod
Proof state before:
α : Type u_1
β : Type u_2
x x' : α
xs : List α
y : β
ys : List β
h_term₁ : Nat.succ 0 + Nat.succ (length ys) < Nat.succ (Nat.succ (length xs)) + Nat.succ (length ys)
h_term₂ : Nat.succ (length xs) + Nat.succ (length ys) < Nat.succ (Nat.succ (length xs)) + Nat.succ (length ys)
ih₁ : length (prod [x] (y :: ys)) = length [x] * length (y :: ys)
ih₂ : length (prod (x' :: xs) (y :: ys)) = length (x' :: xs) * length (y :: ys)
⊢ (0 + 1) * (length ys + 1) + (length xs + 1) * (length ys + 1) = (length xs + 1 + 1) * (length ys + 1)
Tactic:
rw [←Nat.add_mul, Nat.zero_add, Nat.add_comm 1]
Proof state after:
no goals
Theorem: List.length_drop
Proof state before:
α : Type u_1
x✝¹ : List α
x✝ : 0 < length x✝¹
⊢ length (drop 0 x✝¹) = length x✝¹ - 0
Tactic:
simp only [drop, Nat.sub_zero]
Proof state after:
no goals
Theorem: List.length_drop
Proof state before:
α : Type u_1
n : Nat
x : α
xs : List α
h : n + 1 < length (x :: xs)
ih : length (drop n xs) = length xs - n
⊢ length (drop (n + 1) (x :: xs)) = length (x :: xs) - (n + 1)
Tactic:
simp only [drop, Nat.add, length]
Proof state after:
α : Type u_1
n : Nat
x : α
xs : List α
h : n + 1 < length (x :: xs)
ih : length (drop n xs) = length xs - n
⊢ length (drop n xs) = length xs + 1 - (n + 1)
Theorem: List.length_drop
Proof state before:
α : Type u_1
n : Nat
x : α
xs : List α
h : n + 1 < length (x :: xs)
ih : length (drop n xs) = length xs - n
⊢ length (drop n xs) = length xs + 1 - (n + 1)
Tactic:
rw [Nat.succ_sub_succ_eq_sub]
Proof state after:
α : Type u_1
n : Nat
x : α
xs : List α
h : n + 1 < length (x :: xs)
ih : length (drop n xs) = length xs - n
⊢ length (drop n xs) = length xs - n
Theorem: List.length_drop
Proof state before:
α : Type u_1
n : Nat
x : α
xs : List α
h : n + 1 < length (x :: xs)
ih : length (drop n xs) = length xs - n
⊢ length (drop n xs) = length xs - n
Tactic:
exact ih
Proof state after:
no goals
Theorem: List.length_take
Proof state before:
α : Type u_1
x✝ : Nat
h : x✝ < length []
⊢ length (take x✝ []) = x✝
Tactic:
cases h
Proof state after:
no goals
Theorem: List.length_take
Proof state before:
α : Type u_1
x✝¹ : List α
x✝ : 0 < length x✝¹
⊢ length (take 0 x✝¹) = 0
Tactic:
simp only [take, length]
Proof state after:
no goals
Theorem: List.length_take
Proof state before:
α : Type u_1
n : Nat
x : α
xs : List α
h : Nat.succ n < length (x :: xs)
ih : length (take n xs) = n
⊢ length (take (Nat.succ n) (x :: xs)) = Nat.succ n
Tactic:
simp only [take, length]
Proof state after:
α : Type u_1
n : Nat
x : α
xs : List α
h : Nat.succ n < length (x :: xs)
ih : length (take n xs) = n
⊢ length (take n xs) + 1 = Nat.succ n
Theorem: List.length_take
Proof state before:
α : Type u_1
n : Nat
x : α
xs : List α
h : Nat.succ n < length (x :: xs)
ih : length (take n xs) = n
⊢ length (take n xs) + 1 = Nat.succ n
Tactic:
apply congrArg Nat.succ ih
Proof state after:
no goals
Theorem: List.filter_eq_filterSpec
Proof state before:
α✝ : Type u_1
p : α✝ → Bool
xs : List α✝
⊢ filter p xs = filterSpec p xs
Tactic:
induction xs with
| nil => simp [filter, filterSpec]
| cons x xs ih =>
  simp only [filter, filterSpec]
  cases p x with
  | true => simp only [ite_true, ih]
  | false => simp only [ite_false, ih]
Proof state after:
no goals
Theorem: List.filter_eq_filterSpec
Proof state before:
case nil
α✝ : Type u_1
p : α✝ → Bool
⊢ filter p [] = filterSpec p []
Tactic:
simp [filter, filterSpec]
Proof state after:
no goals
Theorem: List.filter_eq_filterSpec
Proof state before:
case cons
α✝ : Type u_1
p : α✝ → Bool
x : α✝
xs : List α✝
ih : filter p xs = filterSpec p xs
⊢ filter p (x :: xs) = filterSpec p (x :: xs)
Tactic:
simp only [filter, filterSpec]
Proof state after:
case cons
α✝ : Type u_1
p : α✝ → Bool
x : α✝
xs : List α✝
ih : filter p xs = filterSpec p xs
⊢ (match p x with
    | true => x :: filter p xs
    | false => filter p xs) =
    if p x = true then x :: filterSpec p xs else filterSpec p xs
Theorem: List.filter_eq_filterSpec
Proof state before:
case cons
α✝ : Type u_1
p : α✝ → Bool
x : α✝
xs : List α✝
ih : filter p xs = filterSpec p xs
⊢ (match p x with
    | true => x :: filter p xs
    | false => filter p xs) =
    if p x = true then x :: filterSpec p xs else filterSpec p xs
Tactic:
cases p x with
| true => simp only [ite_true, ih]
| false => simp only [ite_false, ih]
Proof state after:
no goals
Theorem: List.filter_eq_filterSpec
Proof state before:
case cons.true
α✝ : Type u_1
p : α✝ → Bool
x : α✝
xs : List α✝
ih : filter p xs = filterSpec p xs
⊢ (match true with
    | true => x :: filter p xs
    | false => filter p xs) =
    if true = true then x :: filterSpec p xs else filterSpec p xs
Tactic:
simp only [ite_true, ih]
Proof state after:
no goals
Theorem: List.filter_eq_filterSpec
Proof state before:
case cons.false
α✝ : Type u_1
p : α✝ → Bool
x : α✝
xs : List α✝
ih : filter p xs = filterSpec p xs
⊢ (match false with
    | true => x :: filter p xs
    | false => filter p xs) =
    if false = true then x :: filterSpec p xs else filterSpec p xs
Tactic:
simp only [ite_false, ih]
Proof state after:
no goals
Theorem: List.reverseAux_spec
Proof state before:
α : Type u_1
xs acc : List α
⊢ reverseAux xs acc = reverse xs ++ acc
Tactic:
induction xs generalizing acc with
| nil => simp [reverse, reverseAux]
| cons x xs ih =>
  simp only [reverse, reverseAux]
  simp only [ih]
  rw [←singleton_append, append_assoc]
Proof state after:
no goals
Theorem: List.reverseAux_spec
Proof state before:
case nil
α : Type u_1
acc : List α
⊢ reverseAux [] acc = reverse [] ++ acc
Tactic:
simp [reverse, reverseAux]
Proof state after:
no goals
Theorem: List.reverseAux_spec
Proof state before:
case cons
α : Type u_1
x : α
xs : List α
ih : ∀ (acc : List α), reverseAux xs acc = reverse xs ++ acc
acc : List α
⊢ reverseAux (x :: xs) acc = reverse (x :: xs) ++ acc
Tactic:
simp only [reverse, reverseAux]
Proof state after:
case cons
α : Type u_1
x : α
xs : List α
ih : ∀ (acc : List α), reverseAux xs acc = reverse xs ++ acc
acc : List α
⊢ reverseAux xs (x :: acc) = reverseAux xs [x] ++ acc
Theorem: List.reverseAux_spec
Proof state before:
case cons
α : Type u_1
x : α
xs : List α
ih : ∀ (acc : List α), reverseAux xs acc = reverse xs ++ acc
acc : List α
⊢ reverseAux xs (x :: acc) = reverseAux xs [x] ++ acc
Tactic:
simp only [ih]
Proof state after:
case cons
α : Type u_1
x : α
xs : List α
ih : ∀ (acc : List α), reverseAux xs acc = reverse xs ++ acc
acc : List α
⊢ reverse xs ++ x :: acc = reverse xs ++ [x] ++ acc
Theorem: List.reverseAux_spec
Proof state before:
case cons
α : Type u_1
x : α
xs : List α
ih : ∀ (acc : List α), reverseAux xs acc = reverse xs ++ acc
acc : List α
⊢ reverse xs ++ x :: acc = reverse xs ++ [x] ++ acc
Tactic:
rw [←singleton_append, append_assoc]
Proof state after:
no goals
Theorem: List.reverse_eq_reverseSpec
Proof state before:
case nil
α : Type u_1
⊢ reverse [] = reverseSpec []
Tactic:
simp [reverse, reverseAux, reverseSpec]
Proof state after:
no goals
Theorem: List.reverse_eq_reverseSpec
Proof state before:
case cons
α : Type u_1
x : α
xs : List α
ih : reverse xs = reverseSpec xs
⊢ reverse (x :: xs) = reverseSpec (x :: xs)
Tactic:
simp only [reverse, reverseSpec, reverseAux]
Proof state after:
case cons
α : Type u_1
x : α
xs : List α
ih : reverse xs = reverseSpec xs
⊢ reverseAux xs [x] = reverseSpec xs ++ [x]
Theorem: List.reverse_eq_reverseSpec
Proof state before:
case cons
α : Type u_1
x : α
xs : List α
ih : reverse xs = reverseSpec xs
⊢ reverseAux xs [x] = reverseSpec xs ++ [x]
Tactic:
rw [reverseAux_spec]
Proof state after:
case cons
α : Type u_1
x : α
xs : List α
ih : reverse xs = reverseSpec xs
⊢ reverse xs ++ [x] = reverseSpec xs ++ [x]
Theorem: List.removeAll_singleton_hd_neq
Proof state before:
α : Type u_1
inst✝ : BEq α
⊢ ∀ (x y : α) (xs : List α), (x == y) = false → removeAll (x :: xs) [y] = x :: removeAll xs [y]
Tactic:
intros x y xs hneq
Proof state after:
α : Type u_1
inst✝ : BEq α
x y : α
xs : List α
hneq : (x == y) = false
⊢ removeAll (x :: xs) [y] = x :: removeAll xs [y]
Theorem: List.removeAll_singleton_hd_neq
Proof state before:
α : Type u_1
inst✝ : BEq α
x y : α
xs : List α
hneq : (x == y) = false
⊢ removeAll (x :: xs) [y] = x :: removeAll xs [y]
Tactic:
simp only [removeAll, filter, notElem, elem, hneq, not]
Proof state after:
no goals
Theorem: List.removeAll_singleton_hd_eq
Proof state before:
α : Type u_1
inst✝ : DecidableEq α
⊢ ∀ (x : α) (xs : List α), removeAll (x :: xs) [x] = removeAll xs [x]
Tactic:
intros x xs
Proof state after:
α : Type u_1
inst✝ : DecidableEq α
x : α
xs : List α
⊢ removeAll (x :: xs) [x] = removeAll xs [x]
Theorem: List.removeAll_singleton_hd_eq
Proof state before:
α : Type u_1
inst✝ : DecidableEq α
x : α
xs : List α
⊢ removeAll (x :: xs) [x] = removeAll xs [x]
Tactic:
simp [removeAll, filter, notElem, elem]
Proof state after:
no goals
Theorem: List.mem_singleton_iff
Proof state before:
α : Type u_1
x y : α
⊢ x ∈ [y] ↔ x = y
Tactic:
apply Iff.intro
Proof state after:
case mp
α : Type u_1
x y : α
⊢ x ∈ [y] → x = y

case mpr
α : Type u_1
x y : α
⊢ x = y → x ∈ [y]
Theorem: List.mem_singleton_iff
Proof state before:
case mp
α : Type u_1
x y : α
⊢ x ∈ [y] → x = y

case mpr
α : Type u_1
x y : α
⊢ x = y → x ∈ [y]
Tactic:
. intro hmem
  cases hmem
  . rfl
  . contradiction
Proof state after:
case mpr
α : Type u_1
x y : α
⊢ x = y → x ∈ [y]
Theorem: List.mem_singleton_iff
Proof state before:
case mpr
α : Type u_1
x y : α
⊢ x = y → x ∈ [y]
Tactic:
. intro heq
  rw [heq]
  constructor
Proof state after:
no goals