α : Type uu
β : Type vv
l₁ l₂ : List α
s : l₁ ~ l₂
p p' : α → Bool
hp : ∀ (x : α), x ∈ l₁ → p x = p' x
⊢ countp p l₁ = countp p' l₁
α : Type uu
β : Type vv
l₁ l₂ : List α
s : l₁ ~ l₂
p p' : α → Bool
hp : ∀ (x : α), x ∈ l₁ → p x = p' x
⊢ countp p l₁ = countp p' l₂
rw [← s.countp_eq p']
α : Type uu
β : Type vv
l₁ l₂ : List α
p p' : α → Bool
hp : ∀ (x : α), x ∈ l₁ → p x = p' x
⊢ countp p l₁ = countp p' l₁
α : Type uu
β : Type vv
l₁ l₂ : List α
s : l₁ ~ l₂
p p' : α → Bool
hp : ∀ (x : α), x ∈ l₁ → p x = p' x
⊢ countp p l₁ = countp p' l₁
clear s
case nil
α : Type uu
β : Type vv
l₁ l₂ : List α
p p' : α → Bool
hp✝ : ∀ (x : α), x ∈ l₁ → p x = p' x
hp : ∀ (x : α), x ∈ [] → p x = p' x
⊢ countp p [] = countp p' []

case cons
α : Type uu
β : Type vv
l₁ l₂ : List α
p p' : α → Bool
hp✝ : ∀ (x : α), x ∈ l₁ → p x = p' x
y : α
s : List α
hs : (∀ (x : α), x ∈ s → p x = p' x) → countp p s = countp p' s
hp : ∀ (x : α), x ∈ y :: s → p x = p' x
⊢ countp p (y :: s) = countp p' (y :: s)
α : Type uu
β : Type vv
l₁ l₂ : List α
p p' : α → Bool
hp : ∀ (x : α), x ∈ l₁ → p x = p' x
⊢ countp p l₁ = countp p' l₁
induction' l₁ with y s hs
no goals
case nil
α : Type uu
β : Type vv
l₁ l₂ : List α
p p' : α → Bool
hp✝ : ∀ (x : α), x ∈ l₁ → p x = p' x
hp : ∀ (x : α), x ∈ [] → p x = p' x
⊢ countp p [] = countp p' []
rfl
case cons
α : Type uu
β : Type vv
l₁ l₂ : List α
p p' : α → Bool
hp✝ : ∀ (x : α), x ∈ l₁ → p x = p' x
y : α
s : List α
hs : (∀ (x : α), x ∈ s → p x = p' x) → countp p s = countp p' s
hp : p y = p' y ∧ ∀ (a : α), a ∈ s → p a = p' a
⊢ countp p (y :: s) = countp p' (y :: s)
case cons
α : Type uu
β : Type vv
l₁ l₂ : List α
p p' : α → Bool
hp✝ : ∀ (x : α), x ∈ l₁ → p x = p' x
y : α
s : List α
hs : (∀ (x : α), x ∈ s → p x = p' x) → countp p s = countp p' s
hp : ∀ (x : α), x ∈ y :: s → p x = p' x
⊢ countp p (y :: s) = countp p' (y :: s)
simp only [mem_cons, forall_eq_or_imp] at hp
no goals
case cons
α : Type uu
β : Type vv
l₁ l₂ : List α
p p' : α → Bool
hp✝ : ∀ (x : α), x ∈ l₁ → p x = p' x
y : α
s : List α
hs : (∀ (x : α), x ∈ s → p x = p' x) → countp p s = countp p' s
hp : p y = p' y ∧ ∀ (a : α), a ∈ s → p a = p' a
⊢ countp p (y :: s) = countp p' (y :: s)
simp only [countp_cons, hs hp.2, hp.1]