internlm/Lean-Github huggingface dataset:
Theorem: List.mem_reverse_iff
Proof state before:
case mpr.cons
α : Type u_1
x y : α
ys : List α
ih : x ∈ reverseSpec ys → x ∈ ys
hb : x ∈ [y] ++ reverseSpec ys
⊢ x ∈ y :: ys
Tactic:
simp only [HAppend.hAppend, Append.append, List.append] at hb
Proof state after:
case mpr.cons
α : Type u_1
x y : α
ys : List α
ih : x ∈ reverseSpec ys → x ∈ ys
hb : x ∈ y :: reverseSpec ys
⊢ x ∈ y :: ys
Theorem: List.mem_reverse_iff
Proof state before:
case mpr.cons
α : Type u_1
x y : α
ys : List α
ih : x ∈ reverseSpec ys → x ∈ ys
hb : x ∈ y :: reverseSpec ys
⊢ x ∈ y :: ys
Tactic:
cases hb with
| head => exact Mem.head _
| tail _ htail => exact Mem.tail _ (ih htail)
Proof state after:
no goals
Theorem: List.mem_reverse_iff
Proof state before:
case mpr.cons.head
α : Type u_1
x : α
ys : List α
ih : x ∈ reverseSpec ys → x ∈ ys
⊢ x ∈ x :: ys
Tactic:
exact Mem.head _
Proof state after:
no goals
Theorem: List.mem_reverse_iff
Proof state before:
case mpr.cons.tail
α : Type u_1
x y : α
ys : List α
ih : x ∈ reverseSpec ys → x ∈ ys
htail : Mem x (reverseSpec ys)
⊢ x ∈ y :: ys
Tactic:
exact Mem.tail _ (ih htail)
Proof state after:
no goals
Theorem: List.all_pred
Proof state before:
α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
xs : List α
⊢ (all xs fun x => decide (p x)) = true ↔ ∀ (x : α), x ∈ xs → p x
Tactic:
simp only [all]
Proof state after:
α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
xs : List α
⊢ foldr (fun a r => decide (p a) && r) true xs = true ↔ ∀ (x : α), x ∈ xs → p x
Theorem: List.all_pred
Proof state before:
α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
xs : List α
⊢ foldr (fun a r => decide (p a) && r) true xs = true ↔ ∀ (x : α), x ∈ xs → p x
Tactic:
apply Iff.intro
Proof state after:
case mp
α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
xs : List α
⊢ foldr (fun a r => decide (p a) && r) true xs = true → ∀ (x : α), x ∈ xs → p x

case mpr
α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
xs : List α
⊢ (∀ (x : α), x ∈ xs → p x) → foldr (fun a r => decide (p a) && r) true xs = true
Theorem: List.all_pred
Proof state before:
case mp
α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
xs : List α
⊢ foldr (fun a r => decide (p a) && r) true xs = true → ∀ (x : α), x ∈ xs → p x

case mpr
α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
xs : List α
⊢ (∀ (x : α), x ∈ xs → p x) → foldr (fun a r => decide (p a) && r) true xs = true
Tactic:
. intros hforward x hx
  induction hx with
  | head as =>
    simp [foldr] at hforward
    apply And.left hforward
  | tail a h ih =>
    apply ih
    simp [foldr] at hforward
    apply And.right hforward
Proof state after:
case mpr
α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
xs : List α
⊢ (∀ (x : α), x ∈ xs → p x) → foldr (fun a r => decide (p a) && r) true xs = true
Theorem: List.all_pred
Proof state before:
case mpr
α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
xs : List α
⊢ (∀ (x : α), x ∈ xs → p x) → foldr (fun a r => decide (p a) && r) true xs = true
Tactic:
. intros hbackward
  induction xs with
  | nil => simp [foldr]
  | cons x xs ih =>
    simp [foldr]
    apply And.intro
    . apply hbackward x (List.Mem.head _)
    . apply ih
      intro x' hx'
      apply hbackward _ $ List.Mem.tail _ hx'
Proof state after:
no goals
Theorem: List.all_pred
Proof state before:
case mp
α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
xs : List α
⊢ foldr (fun a r => decide (p a) && r) true xs = true → ∀ (x : α), x ∈ xs → p x
Tactic:
intros hforward x hx
Proof state after:
case mp
α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
xs : List α
hforward : foldr (fun a r => decide (p a) && r) true xs = true
x : α
hx : x ∈ xs
⊢ p x
Theorem: List.all_pred
Proof state before:
case mp
α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
xs : List α
hforward : foldr (fun a r => decide (p a) && r) true xs = true
x : α
hx : x ∈ xs
⊢ p x
Tactic:
induction hx with
| head as =>
  simp [foldr] at hforward
  apply And.left hforward
| tail a h ih =>
  apply ih
  simp [foldr] at hforward
  apply And.right hforward
Proof state after:
no goals
Theorem: List.all_pred
Proof state before:
case mp.head
α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
xs : List α
x : α
as : List α
hforward : foldr (fun a r => decide (p a) && r) true (x :: as) = true
⊢ p x
Tactic:
simp [foldr] at hforward
Proof state after:
case mp.head
α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
xs : List α
x : α
as : List α
hforward : p x ∧ foldr (fun a r => decide (p a) && r) true as = true
⊢ p x
Theorem: List.all_pred
Proof state before:
case mp.head
α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
xs : List α
x : α
as : List α
hforward : p x ∧ foldr (fun a r => decide (p a) && r) true as = true
⊢ p x
Tactic:
apply And.left hforward
Proof state after:
no goals
Theorem: List.all_pred
Proof state before:
case mp.tail
α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
xs : List α
x a : α
as✝ : List α
h : Mem x as✝
ih : foldr (fun a r => decide (p a) && r) true as✝ = true → p x
hforward : foldr (fun a r => decide (p a) && r) true (a :: as✝) = true
⊢ p x
Tactic:
apply ih
Proof state after:
case mp.tail
α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
xs : List α
x a : α
as✝ : List α
h : Mem x as✝
ih : foldr (fun a r => decide (p a) && r) true as✝ = true → p x
hforward : foldr (fun a r => decide (p a) && r) true (a :: as✝) = true
⊢ foldr (fun a r => decide (p a) && r) true as✝ = true
Theorem: List.all_pred
Proof state before:
case mp.tail
α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
xs : List α
x a : α
as✝ : List α
h : Mem x as✝
ih : foldr (fun a r => decide (p a) && r) true as✝ = true → p x
hforward : foldr (fun a r => decide (p a) && r) true (a :: as✝) = true
⊢ foldr (fun a r => decide (p a) && r) true as✝ = true
Tactic:
simp [foldr] at hforward
Proof state after:
case mp.tail
α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
xs : List α
x a : α
as✝ : List α
h : Mem x as✝
ih : foldr (fun a r => decide (p a) && r) true as✝ = true → p x
hforward : p a ∧ foldr (fun a r => decide (p a) && r) true as✝ = true
⊢ foldr (fun a r => decide (p a) && r) true as✝ = true
Theorem: List.all_pred
Proof state before:
case mp.tail
α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
xs : List α
x a : α
as✝ : List α
h : Mem x as✝
ih : foldr (fun a r => decide (p a) && r) true as✝ = true → p x
hforward : p a ∧ foldr (fun a r => decide (p a) && r) true as✝ = true
⊢ foldr (fun a r => decide (p a) && r) true as✝ = true
Tactic:
apply And.right hforward
Proof state after:
no goals
Theorem: List.all_pred
Proof state before:
case mpr
α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
xs : List α
⊢ (∀ (x : α), x ∈ xs → p x) → foldr (fun a r => decide (p a) && r) true xs = true
Tactic:
intros hbackward
Proof state after:
case mpr
α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
xs : List α
hbackward : ∀ (x : α), x ∈ xs → p x
⊢ foldr (fun a r => decide (p a) && r) true xs = true
Theorem: List.all_pred
Proof state before:
case mpr
α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
xs : List α
hbackward : ∀ (x : α), x ∈ xs → p x
⊢ foldr (fun a r => decide (p a) && r) true xs = true
Tactic:
induction xs with
| nil => simp [foldr]
| cons x xs ih =>
  simp [foldr]
  apply And.intro
  . apply hbackward x (List.Mem.head _)
  . apply ih
    intro x' hx'
    apply hbackward _ $ List.Mem.tail _ hx'
Proof state after:
no goals
Theorem: List.all_pred
Proof state before:
case mpr.nil
α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
hbackward : ∀ (x : α), x ∈ [] → p x
⊢ foldr (fun a r => decide (p a) && r) true [] = true
Tactic:
simp [foldr]
Proof state after:
no goals
Theorem: List.all_pred
Proof state before:
case mpr.cons
α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
x : α
xs : List α
ih : (∀ (x : α), x ∈ xs → p x) → foldr (fun a r => decide (p a) && r) true xs = true
hbackward : ∀ (x_1 : α), x_1 ∈ x :: xs → p x_1
⊢ foldr (fun a r => decide (p a) && r) true (x :: xs) = true
Tactic:
simp [foldr]
Proof state after:
case mpr.cons
α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
x : α
xs : List α
ih : (∀ (x : α), x ∈ xs → p x) → foldr (fun a r => decide (p a) && r) true xs = true
hbackward : ∀ (x_1 : α), x_1 ∈ x :: xs → p x_1
⊢ p x ∧ foldr (fun a r => decide (p a) && r) true xs = true
Theorem: List.all_pred
Proof state before:
case mpr.cons
α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
x : α
xs : List α
ih : (∀ (x : α), x ∈ xs → p x) → foldr (fun a r => decide (p a) && r) true xs = true
hbackward : ∀ (x_1 : α), x_1 ∈ x :: xs → p x_1
⊢ p x ∧ foldr (fun a r => decide (p a) && r) true xs = true
Tactic:
apply And.intro
Proof state after:
case mpr.cons.left
α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
x : α
xs : List α
ih : (∀ (x : α), x ∈ xs → p x) → foldr (fun a r => decide (p a) && r) true xs = true
hbackward : ∀ (x_1 : α), x_1 ∈ x :: xs → p x_1
⊢ p x

case mpr.cons.right
α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
x : α
xs : List α
ih : (∀ (x : α), x ∈ xs → p x) → foldr (fun a r => decide (p a) && r) true xs = true
hbackward : ∀ (x_1 : α), x_1 ∈ x :: xs → p x_1
⊢ foldr (fun a r => decide (p a) && r) true xs = true
Theorem: List.all_pred
Proof state before:
case mpr.cons.left
α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
x : α
xs : List α
ih : (∀ (x : α), x ∈ xs → p x) → foldr (fun a r => decide (p a) && r) true xs = true
hbackward : ∀ (x_1 : α), x_1 ∈ x :: xs → p x_1
⊢ p x

case mpr.cons.right
α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
x : α
xs : List α
ih : (∀ (x : α), x ∈ xs → p x) → foldr (fun a r => decide (p a) && r) true xs = true
hbackward : ∀ (x_1 : α), x_1 ∈ x :: xs → p x_1
⊢ foldr (fun a r => decide (p a) && r) true xs = true
Tactic:
. apply hbackward x (List.Mem.head _)
Proof state after:
case mpr.cons.right
α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
x : α
xs : List α
ih : (∀ (x : α), x ∈ xs → p x) → foldr (fun a r => decide (p a) && r) true xs = true
hbackward : ∀ (x_1 : α), x_1 ∈ x :: xs → p x_1
⊢ foldr (fun a r => decide (p a) && r) true xs = true
Theorem: List.all_pred
Proof state before:
case mpr.cons.right
α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
x : α
xs : List α
ih : (∀ (x : α), x ∈ xs → p x) → foldr (fun a r => decide (p a) && r) true xs = true
hbackward : ∀ (x_1 : α), x_1 ∈ x :: xs → p x_1
⊢ foldr (fun a r => decide (p a) && r) true xs = true
Tactic:
. apply ih
  intro x' hx'
  apply hbackward _ $ List.Mem.tail _ hx'
Proof state after:
no goals
Theorem: List.all_pred
Proof state before:
case mpr.cons.left
α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
x : α
xs : List α
ih : (∀ (x : α), x ∈ xs → p x) → foldr (fun a r => decide (p a) && r) true xs = true
hbackward : ∀ (x_1 : α), x_1 ∈ x :: xs → p x_1
⊢ p x
Tactic:
apply hbackward x (List.Mem.head _)
Proof state after:
no goals
Theorem: List.all_pred
Proof state before:
case mpr.cons.right
α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
x : α
xs : List α
ih : (∀ (x : α), x ∈ xs → p x) → foldr (fun a r => decide (p a) && r) true xs = true
hbackward : ∀ (x_1 : α), x_1 ∈ x :: xs → p x_1
⊢ foldr (fun a r => decide (p a) && r) true xs = true
Tactic:
apply ih
Proof state after:
case mpr.cons.right
α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
x : α
xs : List α
ih : (∀ (x : α), x ∈ xs → p x) → foldr (fun a r => decide (p a) && r) true xs = true
hbackward : ∀ (x_1 : α), x_1 ∈ x :: xs → p x_1
⊢ ∀ (x : α), x ∈ xs → p x
Theorem: List.all_pred
Proof state before:
case mpr.cons.right
α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
x : α
xs : List α
ih : (∀ (x : α), x ∈ xs → p x) → foldr (fun a r => decide (p a) && r) true xs = true
hbackward : ∀ (x_1 : α), x_1 ∈ x :: xs → p x_1
⊢ ∀ (x : α), x ∈ xs → p x
Tactic:
intro x' hx'
Proof state after:
case mpr.cons.right
α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
x : α
xs : List α
ih : (∀ (x : α), x ∈ xs → p x) → foldr (fun a r => decide (p a) && r) true xs = true
hbackward : ∀ (x_1 : α), x_1 ∈ x :: xs → p x_1
x' : α
hx' : x' ∈ xs
⊢ p x'
Theorem: List.all_pred
Proof state before:
case mpr.cons.right
α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
x : α
xs : List α
ih : (∀ (x : α), x ∈ xs → p x) → foldr (fun a r => decide (p a) && r) true xs = true
hbackward : ∀ (x_1 : α), x_1 ∈ x :: xs → p x_1
x' : α
hx' : x' ∈ xs
⊢ p x'
Tactic:
apply hbackward _ $ List.Mem.tail _ hx'
Proof state after:
no goals
Theorem: List.mem_cons_iff_mem_singleton_or_tail
Proof state before:
α : Type u_1
y : α
ys : List α
x : α
⊢ x ∈ y :: ys ↔ x ∈ [y] ∨ x ∈ ys
Tactic:
apply Iff.intro
Proof state after:
case mp
α : Type u_1
y : α
ys : List α
x : α
⊢ x ∈ y :: ys → x ∈ [y] ∨ x ∈ ys

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

case mpr
α : Type u_1
y : α
ys : List α
x : α
⊢ x ∈ [y] ∨ x ∈ ys → x ∈ y :: ys
Tactic:
. intro hf
  cases hf with
  | head => apply Or.intro_left _ (Mem.head _)
  | tail _ h => apply Or.intro_right _ h
Proof state after:
case mpr
α : Type u_1
y : α
ys : List α
x : α
⊢ x ∈ [y] ∨ x ∈ ys → x ∈ y :: ys
Theorem: List.mem_cons_iff_mem_singleton_or_tail
Proof state before:
case mpr
α : Type u_1
y : α
ys : List α
x : α
⊢ x ∈ [y] ∨ x ∈ ys → x ∈ y :: ys
Tactic:
. intro hb
  cases hb with
  | inl h => rw [(mem_singleton_iff x y).mp h]; apply Mem.head
  | inr h => apply Mem.tail _ h
Proof state after:
no goals
Theorem: List.mem_cons_iff_mem_singleton_or_tail
Proof state before:
case mp
α : Type u_1
y : α
ys : List α
x : α
⊢ x ∈ y :: ys → x ∈ [y] ∨ x ∈ ys
Tactic:
intro hf
Proof state after:
case mp
α : Type u_1
y : α
ys : List α
x : α
hf : x ∈ y :: ys
⊢ x ∈ [y] ∨ x ∈ ys
Theorem: List.mem_cons_iff_mem_singleton_or_tail
Proof state before:
case mp
α : Type u_1
y : α
ys : List α
x : α
hf : x ∈ y :: ys
⊢ x ∈ [y] ∨ x ∈ ys
Tactic:
cases hf with
| head => apply Or.intro_left _ (Mem.head _)
| tail _ h => apply Or.intro_right _ h
Proof state after:
no goals
Theorem: List.mem_cons_iff_mem_singleton_or_tail
Proof state before:
case mp.head
α : Type u_1
y : α
ys : List α
⊢ y ∈ [y] ∨ y ∈ ys
Tactic:
apply Or.intro_left _ (Mem.head _)
Proof state after:
no goals
Theorem: List.mem_cons_iff_mem_singleton_or_tail
Proof state before:
case mp.tail
α : Type u_1
y : α
ys : List α
x : α
h : Mem x ys
⊢ x ∈ [y] ∨ x ∈ ys
Tactic:
apply Or.intro_right _ h
Proof state after:
no goals
Theorem: List.mem_cons_iff_mem_singleton_or_tail
Proof state before:
case mpr
α : Type u_1
y : α
ys : List α
x : α
⊢ x ∈ [y] ∨ x ∈ ys → x ∈ y :: ys
Tactic:
intro hb
Proof state after:
case mpr
α : Type u_1
y : α
ys : List α
x : α
hb : x ∈ [y] ∨ x ∈ ys
⊢ x ∈ y :: ys
Theorem: List.mem_cons_iff_mem_singleton_or_tail
Proof state before:
case mpr
α : Type u_1
y : α
ys : List α
x : α
hb : x ∈ [y] ∨ x ∈ ys
⊢ x ∈ y :: ys
Tactic:
cases hb with
| inl h => rw [(mem_singleton_iff x y).mp h]; apply Mem.head
| inr h => apply Mem.tail _ h
Proof state after:
no goals
Theorem: List.mem_cons_iff_mem_singleton_or_tail
Proof state before:
case mpr.inl
α : Type u_1
y : α
ys : List α
x : α
h : x ∈ [y]
⊢ x ∈ y :: ys
Tactic:
rw [(mem_singleton_iff x y).mp h]
Proof state after:
case mpr.inl
α : Type u_1
y : α
ys : List α
x : α
h : x ∈ [y]
⊢ y ∈ y :: ys
Theorem: List.mem_cons_iff_mem_singleton_or_tail
Proof state before:
case mpr.inl
α : Type u_1
y : α
ys : List α
x : α
h : x ∈ [y]
⊢ y ∈ y :: ys
Tactic:
apply Mem.head
Proof state after:
no goals
Theorem: List.mem_cons_iff_mem_singleton_or_tail
Proof state before:
case mpr.inr
α : Type u_1
y : α
ys : List α
x : α
h : x ∈ ys
⊢ x ∈ y :: ys
Tactic:
apply Mem.tail _ h
Proof state after:
no goals
Theorem: List.filter_filter
Proof state before:
α : Type u_1
p₁ p₂ : α → Bool
xs : List α
⊢ filter p₁ (filter p₂ xs) = filter (fun x => decide (p₂ x = true ∧ p₁ x = true)) xs
Tactic:
rw [filter_eq_filterSpec, filter_eq_filterSpec, filter_eq_filterSpec]
Proof state after:
α : Type u_1
p₁ p₂ : α → Bool
xs : List α
⊢ filterSpec p₁ (filterSpec p₂ xs) = filterSpec (fun x => decide (p₂ x = true ∧ p₁ x = true)) xs
Theorem: List.filter_filter
Proof state before:
α : Type u_1
p₁ p₂ : α → Bool
xs : List α
⊢ filterSpec p₁ (filterSpec p₂ xs) = filterSpec (fun x => decide (p₂ x = true ∧ p₁ x = true)) xs
Tactic:
induction xs with
| nil => simp [filterSpec]
| cons x xs ih =>
  cases h₂ : p₂ x with
  | false =>
    simp only [filterSpec, h₂, ite_false]
    exact ih
  | true =>
    simp only [filterSpec, h₂, ite_true]
    cases h₁ : p₁ x with
    | false =>
      simp only [filterSpec, h₁, h₂, ite_false]
      exact ih
    | true =>
      simp only [filterSpec, h₁, h₂, ite_true]
      exact congrArg _ ih
Proof state after:
no goals
Theorem: List.filter_filter
Proof state before:
case nil
α : Type u_1
p₁ p₂ : α → Bool
⊢ filterSpec p₁ (filterSpec p₂ []) = filterSpec (fun x => decide (p₂ x = true ∧ p₁ x = true)) []
Tactic:
simp [filterSpec]
Proof state after:
no goals
Theorem: List.filter_filter
Proof state before:
case cons
α : Type u_1
p₁ p₂ : α → Bool
x : α
xs : List α
ih : filterSpec p₁ (filterSpec p₂ xs) = filterSpec (fun x => decide (p₂ x = true ∧ p₁ x = true)) xs
⊢ filterSpec p₁ (filterSpec p₂ (x :: xs)) = filterSpec (fun x => decide (p₂ x = true ∧ p₁ x = true)) (x :: xs)
Tactic:
cases h₂ : p₂ x with
| false =>
  simp only [filterSpec, h₂, ite_false]
  exact ih
| true =>
  simp only [filterSpec, h₂, ite_true]
  cases h₁ : p₁ x with
  | false =>
    simp only [filterSpec, h₁, h₂, ite_false]
    exact ih
  | true =>
    simp only [filterSpec, h₁, h₂, ite_true]
    exact congrArg _ ih
Proof state after:
no goals
Theorem: List.filter_filter
Proof state before:
case cons.false
α : Type u_1
p₁ p₂ : α → Bool
x : α
xs : List α
ih : filterSpec p₁ (filterSpec p₂ xs) = filterSpec (fun x => decide (p₂ x = true ∧ p₁ x = true)) xs
h₂ : p₂ x = false
⊢ filterSpec p₁ (filterSpec p₂ (x :: xs)) = filterSpec (fun x => decide (p₂ x = true ∧ p₁ x = true)) (x :: xs)
Tactic:
simp only [filterSpec, h₂, ite_false]
Proof state after:
case cons.false
α : Type u_1
p₁ p₂ : α → Bool
x : α
xs : List α
ih : filterSpec p₁ (filterSpec p₂ xs) = filterSpec (fun x => decide (p₂ x = true ∧ p₁ x = true)) xs
h₂ : p₂ x = false
⊢ filterSpec p₁ (filterSpec p₂ xs) =
    if decide (False ∧ p₁ x = true) = true then x :: filterSpec (fun x => decide (p₂ x = true ∧ p₁ x = true)) xs
    else filterSpec (fun x => decide (p₂ x = true ∧ p₁ x = true)) xs
Theorem: List.filter_filter
Proof state before:
case cons.false
α : Type u_1
p₁ p₂ : α → Bool
x : α
xs : List α
ih : filterSpec p₁ (filterSpec p₂ xs) = filterSpec (fun x => decide (p₂ x = true ∧ p₁ x = true)) xs
h₂ : p₂ x = false
⊢ filterSpec p₁ (filterSpec p₂ xs) =
    if decide (False ∧ p₁ x = true) = true then x :: filterSpec (fun x => decide (p₂ x = true ∧ p₁ x = true)) xs
    else filterSpec (fun x => decide (p₂ x = true ∧ p₁ x = true)) xs
Tactic:
exact ih
Proof state after:
no goals
Theorem: List.filter_filter
Proof state before:
case cons.true
α : Type u_1
p₁ p₂ : α → Bool
x : α
xs : List α
ih : filterSpec p₁ (filterSpec p₂ xs) = filterSpec (fun x => decide (p₂ x = true ∧ p₁ x = true)) xs
h₂ : p₂ x = true
⊢ filterSpec p₁ (filterSpec p₂ (x :: xs)) = filterSpec (fun x => decide (p₂ x = true ∧ p₁ x = true)) (x :: xs)
Tactic:
simp only [filterSpec, h₂, ite_true]
Proof state after:
case cons.true
α : Type u_1
p₁ p₂ : α → Bool
x : α
xs : List α
ih : filterSpec p₁ (filterSpec p₂ xs) = filterSpec (fun x => decide (p₂ x = true ∧ p₁ x = true)) xs
h₂ : p₂ x = true
⊢ (if p₁ x = true then x :: filterSpec p₁ (filterSpec p₂ xs) else filterSpec p₁ (filterSpec p₂ xs)) =
    if decide (True ∧ p₁ x = true) = true then x :: filterSpec (fun x => decide (p₂ x = true ∧ p₁ x = true)) xs
    else filterSpec (fun x => decide (p₂ x = true ∧ p₁ x = true)) xs
Theorem: List.filter_filter
Proof state before:
case cons.true
α : Type u_1
p₁ p₂ : α → Bool
x : α
xs : List α
ih : filterSpec p₁ (filterSpec p₂ xs) = filterSpec (fun x => decide (p₂ x = true ∧ p₁ x = true)) xs
h₂ : p₂ x = true
⊢ (if p₁ x = true then x :: filterSpec p₁ (filterSpec p₂ xs) else filterSpec p₁ (filterSpec p₂ xs)) =
    if decide (True ∧ p₁ x = true) = true then x :: filterSpec (fun x => decide (p₂ x = true ∧ p₁ x = true)) xs
    else filterSpec (fun x => decide (p₂ x = true ∧ p₁ x = true)) xs
Tactic:
cases h₁ : p₁ x with
| false =>
  simp only [filterSpec, h₁, h₂, ite_false]
  exact ih
| true =>
  simp only [filterSpec, h₁, h₂, ite_true]
  exact congrArg _ ih
Proof state after:
no goals
Theorem: List.filter_filter
Proof state before:
case cons.true.false
α : Type u_1
p₁ p₂ : α → Bool
x : α
xs : List α
ih : filterSpec p₁ (filterSpec p₂ xs) = filterSpec (fun x => decide (p₂ x = true ∧ p₁ x = true)) xs
h₂ : p₂ x = true
h₁ : p₁ x = false
⊢ (if false = true then x :: filterSpec p₁ (filterSpec p₂ xs) else filterSpec p₁ (filterSpec p₂ xs)) =
    if decide (True ∧ false = true) = true then x :: filterSpec (fun x => decide (p₂ x = true ∧ p₁ x = true)) xs
    else filterSpec (fun x => decide (p₂ x = true ∧ p₁ x = true)) xs
Tactic:
simp only [filterSpec, h₁, h₂, ite_false]
Proof state after:
case cons.true.false
α : Type u_1
p₁ p₂ : α → Bool
x : α
xs : List α
ih : filterSpec p₁ (filterSpec p₂ xs) = filterSpec (fun x => decide (p₂ x = true ∧ p₁ x = true)) xs
h₂ : p₂ x = true
h₁ : p₁ x = false
⊢ filterSpec p₁ (filterSpec p₂ xs) =
    if decide (True ∧ False) = true then x :: filterSpec (fun x => decide (p₂ x = true ∧ p₁ x = true)) xs
    else filterSpec (fun x => decide (p₂ x = true ∧ p₁ x = true)) xs
Theorem: List.filter_filter
Proof state before:
case cons.true.false
α : Type u_1
p₁ p₂ : α → Bool
x : α
xs : List α
ih : filterSpec p₁ (filterSpec p₂ xs) = filterSpec (fun x => decide (p₂ x = true ∧ p₁ x = true)) xs
h₂ : p₂ x = true
h₁ : p₁ x = false
⊢ filterSpec p₁ (filterSpec p₂ xs) =
    if decide (True ∧ False) = true then x :: filterSpec (fun x => decide (p₂ x = true ∧ p₁ x = true)) xs
    else filterSpec (fun x => decide (p₂ x = true ∧ p₁ x = true)) xs
Tactic:
exact ih
Proof state after:
no goals
Theorem: List.filter_filter
Proof state before:
case cons.true.true
α : Type u_1
p₁ p₂ : α → Bool
x : α
xs : List α
ih : filterSpec p₁ (filterSpec p₂ xs) = filterSpec (fun x => decide (p₂ x = true ∧ p₁ x = true)) xs
h₂ : p₂ x = true
h₁ : p₁ x = true
⊢ (if true = true then x :: filterSpec p₁ (filterSpec p₂ xs) else filterSpec p₁ (filterSpec p₂ xs)) =
    if decide (True ∧ true = true) = true then x :: filterSpec (fun x => decide (p₂ x = true ∧ p₁ x = true)) xs
    else filterSpec (fun x => decide (p₂ x = true ∧ p₁ x = true)) xs
Tactic:
simp only [filterSpec, h₁, h₂, ite_true]
Proof state after:
case cons.true.true
α : Type u_1
p₁ p₂ : α → Bool
x : α
xs : List α
ih : filterSpec p₁ (filterSpec p₂ xs) = filterSpec (fun x => decide (p₂ x = true ∧ p₁ x = true)) xs
h₂ : p₂ x = true
h₁ : p₁ x = true
⊢ x :: filterSpec p₁ (filterSpec p₂ xs) =
    if decide (True ∧ True) = true then x :: filterSpec (fun x => decide (p₂ x = true ∧ p₁ x = true)) xs
    else filterSpec (fun x => decide (p₂ x = true ∧ p₁ x = true)) xs
Theorem: List.filter_filter
Proof state before:
case cons.true.true
α : Type u_1
p₁ p₂ : α → Bool
x : α
xs : List α
ih : filterSpec p₁ (filterSpec p₂ xs) = filterSpec (fun x => decide (p₂ x = true ∧ p₁ x = true)) xs
h₂ : p₂ x = true
h₁ : p₁ x = true
⊢ x :: filterSpec p₁ (filterSpec p₂ xs) =
    if decide (True ∧ True) = true then x :: filterSpec (fun x => decide (p₂ x = true ∧ p₁ x = true)) xs
    else filterSpec (fun x => decide (p₂ x = true ∧ p₁ x = true)) xs
Tactic:
exact congrArg _ ih
Proof state after:
no goals
Theorem: List.uniqueAux_acc_append_filter
Proof state before:
α : Type u_1
inst✝ : DecidableEq α
acc : List α
⊢ uniqueAux [] acc = reverse acc ++ unique (filter (fun x => decide ¬x ∈ acc) [])
Tactic:
simp [uniqueAux, reverse, reverseAux, unique]
Proof state after:
no goals