case h
α : Type u
β : Type v
γ : Type w
⊢ ∀ (x : Type u_1), filter = filterTR
α : Type u
β : Type v
γ : Type w
⊢ @filter = @filterTR
apply funext
case h
α✝ : Type u
β : Type v
γ : Type w
α : Type u_1
⊢ filter = filterTR
case h
α : Type u
β : Type v
γ : Type w
⊢ ∀ (x : Type u_1), filter = filterTR
intro α
case h.h
α✝ : Type u
β : Type v
γ : Type w
α : Type u_1
⊢ ∀ (x : α → Bool), filter x = filterTR x
case h
α✝ : Type u
β : Type v
γ : Type w
α : Type u_1
⊢ filter = filterTR
apply funext
case h.h
α✝ : Type u
β : Type v
γ : Type w
α : Type u_1
p : α → Bool
⊢ filter p = filterTR p
case h.h
α✝ : Type u
β : Type v
γ : Type w
α : Type u_1
⊢ ∀ (x : α → Bool), filter x = filterTR x
intro p
case h.h.h
α✝ : Type u
β : Type v
γ : Type w
α : Type u_1
p : α → Bool
⊢ ∀ (x : List α), filter p x = filterTR p x
case h.h
α✝ : Type u
β : Type v
γ : Type w
α : Type u_1
p : α → Bool
⊢ filter p = filterTR p
apply funext
case h.h.h
α✝ : Type u
β : Type v
γ : Type w
α : Type u_1
p : α → Bool
as : List α
⊢ filter p as = filterTR p as
case h.h.h
α✝ : Type u
β : Type v
γ : Type w
α : Type u_1
p : α → Bool
⊢ ∀ (x : List α), filter p x = filterTR p x
intro as
no goals
case h.h.h
α✝ : Type u
β : Type v
γ : Type w
α : Type u_1
p : α → Bool
as : List α
⊢ filter p as = filterTR p as
simp [filterTR, filterTR_loop_eq]