Theorem: List.forAll_map_eq (Algdata/Data/List/Prop.lean)

State before:
α : Type u_1
β : Type u_2
p : β → Prop
f : α → β
as : List α
⊢ forAll p (map f as) = forAll (p ∘ f) as
Tactic:
induction as
State after:
case nil
α : Type u_1
β : Type u_2
p : β → Prop
f : α → β
⊢ forAll p (map f []) = forAll (p ∘ f) []

case cons
α : Type u_1
β : Type u_2
p : β → Prop
f : α → β
head✝ : α
tail✝ : List α
tail_ih✝ : forAll p (map f tail✝) = forAll (p ∘ f) tail✝
⊢ forAll p (map f (head✝ :: tail✝)) = forAll (p ∘ f) (head✝ :: tail✝)

State before:
α : Type u_1
β : Type u_2
p : β → Prop
f : α → β
⊢ forAll p (map f []) = forAll (p ∘ f) []
Tactic:
case nil => exact rfl
State after:
no goals

State before:
α : Type u_1
β : Type u_2
p : β → Prop
f : α → β
a : α
as : List α
h_ind : forAll p (map f as) = forAll (p ∘ f) as
⊢ forAll p (map f (a :: as)) = forAll (p ∘ f) (a :: as)
Tactic:
case cons a as h_ind =>
  dsimp [List.forAll]
  rw [h_ind]
State after:
no goals

State before:
α : Type u_1
β : Type u_2
p : β → Prop
f : α → β
⊢ forAll p (map f []) = forAll (p ∘ f) []
Tactic:
exact rfl
State after:
no goals

State before:
α : Type u_1
β : Type u_2
p : β → Prop
f : α → β
a : α
as : List α
h_ind : forAll p (map f as) = forAll (p ∘ f) as
⊢ forAll p (map f (a :: as)) = forAll (p ∘ f) (a :: as)
Tactic:
dsimp [List.forAll]
State after:
α : Type u_1
β : Type u_2
p : β → Prop
f : α → β
a : α
as : List α
h_ind : forAll p (map f as) = forAll (p ∘ f) as
⊢ (p (f a) ∧ forAll p (map f as)) = (p (f a) ∧ forAll (p ∘ f) as)

State before:
α : Type u_1
β : Type u_2
p : β → Prop
f : α → β
a : α
as : List α
h_ind : forAll p (map f as) = forAll (p ∘ f) as
⊢ (p (f a) ∧ forAll p (map f as)) = (p (f a) ∧ forAll (p ∘ f) as)
Tactic:
rw [h_ind]
State after:
no goals