Theorem: List.SatisfiesM_List_eq (Dijkstra/Control/Functor/Subreg.lean)

State before:
α : Type u
p : α → Prop
as : List α
h : SatisfiesM p as
⊢ forAll p as
Tactic:
cases h with | intro xs hx =>
cases hx
induction xs
case nil => exact True.intro
case cons a as h_ind =>
  exact ⟨a.property, h_ind⟩
State after:
no goals

State before:
case intro
α : Type u
p : α → Prop
as : List α
xs : List { a // p a }
hx : Subtype.val <$> xs = as
⊢ forAll p as
Tactic:
cases hx
State after:
case intro.refl
α : Type u
p : α → Prop
xs : List { a // p a }
⊢ forAll p (Subtype.val <$> xs)

State before:
case intro.refl
α : Type u
p : α → Prop
xs : List { a // p a }
⊢ forAll p (Subtype.val <$> xs)
Tactic:
induction xs
State after:
case intro.refl.nil
α : Type u
p : α → Prop
⊢ forAll p (Subtype.val <$> [])

case intro.refl.cons
α : Type u
p : α → Prop
head✝ : { a // p a }
tail✝ : List { a // p a }
tail_ih✝ : forAll p (Subtype.val <$> tail✝)
⊢ forAll p (Subtype.val <$> (head✝ :: tail✝))

State before:
α : Type u
p : α → Prop
⊢ forAll p (Subtype.val <$> [])
Tactic:
case nil => exact True.intro
State after:
no goals

State before:
α : Type u
p : α → Prop
a : { a // p a }
as : List { a // p a }
h_ind : forAll p (Subtype.val <$> as)
⊢ forAll p (Subtype.val <$> (a :: as))
Tactic:
case cons a as h_ind =>
  exact ⟨a.property, h_ind⟩
State after:
no goals

State before:
α : Type u
p : α → Prop
⊢ forAll p (Subtype.val <$> [])
Tactic:
exact True.intro
State after:
no goals

State before:
α : Type u
p : α → Prop
a : { a // p a }
as : List { a // p a }
h_ind : forAll p (Subtype.val <$> as)
⊢ forAll p (Subtype.val <$> (a :: as))
Tactic:
exact ⟨a.property, h_ind⟩
State after:
no goals

State before:
α : Type u
p : α → Prop
as : List α
h : forAll p as
⊢ SatisfiesM p as
Tactic:
exists zipProof as h
State after:
α : Type u
p : α → Prop
as : List α
h : forAll p as
⊢ Subtype.val <$> zipProof as h = as

State before:
α : Type u
p : α → Prop
as : List α
h : forAll p as
⊢ Subtype.val <$> zipProof as h = as
Tactic:
exact val_zipProof as
State after:
no goals