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

State before:
α : Type u_1
p : α → Prop
as : List α
⊢ forAll p (reverse as) = forAll p as
Tactic:
induction as <;> simp
State after:
case cons
α : Type u_1
p : α → Prop
head✝ : α
tail✝ : List α
tail_ih✝ : forAll p (reverse tail✝) = forAll p tail✝
⊢ forAll p (reverse tail✝) ∧ forAll p [head✝] ↔ forAll p (head✝ :: tail✝)

State before:
α : Type u_1
p : α → Prop
a : α
as : List α
h_ind : forAll p (reverse as) = forAll p as
⊢ forAll p (reverse as) ∧ forAll p [a] ↔ forAll p (a :: as)
Tactic:
case cons a as h_ind =>
  dsimp [forAll]
  rw [h_ind, And.comm, and_true]
State after:
no goals

State before:
α : Type u_1
p : α → Prop
a : α
as : List α
h_ind : forAll p (reverse as) = forAll p as
⊢ forAll p (reverse as) ∧ forAll p [a] ↔ forAll p (a :: as)
Tactic:
dsimp [forAll]
State after:
α : Type u_1
p : α → Prop
a : α
as : List α
h_ind : forAll p (reverse as) = forAll p as
⊢ forAll p (reverse as) ∧ p a ∧ True ↔ p a ∧ forAll p as

State before:
α : Type u_1
p : α → Prop
a : α
as : List α
h_ind : forAll p (reverse as) = forAll p as
⊢ forAll p (reverse as) ∧ p a ∧ True ↔ p a ∧ forAll p as
Tactic:
rw [h_ind, And.comm, and_true]
State after:
no goals