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

State before:
α : Type u
p : α → Prop
as : List α
h : forAll p as
⊢ Subtype.val <$> zipProof as h = as
Tactic:
induction as
State after:
case nil
α : Type u
p : α → Prop
h : forAll p []
⊢ Subtype.val <$> zipProof [] h = []

case cons
α : Type u
p : α → Prop
head✝ : α
tail✝ : List α
tail_ih✝ : ∀ {h : forAll p tail✝}, Subtype.val <$> zipProof tail✝ h = tail✝
h : forAll p (head✝ :: tail✝)
⊢ Subtype.val <$> zipProof (head✝ :: tail✝) h = head✝ :: tail✝

State before:
α : Type u
p : α → Prop
h : forAll p []
⊢ Subtype.val <$> zipProof [] h = []
Tactic:
case nil => rfl
State after:
no goals

State before:
α : Type u
p : α → Prop
a : α
as : List α
h_ind : ∀ {h : forAll p as}, Subtype.val <$> zipProof as h = as
h : forAll p (a :: as)
⊢ Subtype.val <$> zipProof (a :: as) h = a :: as
Tactic:
case cons a as h_ind =>
  cases h with | intro ha has =>
  dsimp [Functor.map, zipProof, List.map] at *
  rw [h_ind]
State after:
no goals

State before:
α : Type u
p : α → Prop
h : forAll p []
⊢ Subtype.val <$> zipProof [] h = []
Tactic:
rfl
State after:
no goals

State before:
α : Type u
p : α → Prop
a : α
as : List α
h_ind : ∀ {h : forAll p as}, Subtype.val <$> zipProof as h = as
h : forAll p (a :: as)
⊢ Subtype.val <$> zipProof (a :: as) h = a :: as
Tactic:
cases h with | intro ha has =>
dsimp [Functor.map, zipProof, List.map] at *
rw [h_ind]
State after:
no goals

State before:
case intro
α : Type u
p : α → Prop
a : α
as : List α
h_ind : ∀ {h : forAll p as}, Subtype.val <$> zipProof as h = as
ha : p a
has : forAll p as
⊢ Subtype.val <$> zipProof (a :: as) (_ : p a ∧ forAll p as) = a :: as
Tactic:
dsimp [Functor.map, zipProof, List.map] at *
State after:
case intro
α : Type u
p : α → Prop
a : α
as : List α
h_ind : ∀ {h : forAll p as}, map Subtype.val (zipProof as h) = as
ha : p a
has : forAll p as
⊢ a :: map Subtype.val (zipProof as has) = a :: as

State before:
case intro
α : Type u
p : α → Prop
a : α
as : List α
h_ind : ∀ {h : forAll p as}, map Subtype.val (zipProof as h) = as
ha : p a
has : forAll p as
⊢ a :: map Subtype.val (zipProof as has) = a :: as
Tactic:
rw [h_ind]
State after:
no goals