Theorem: Prod.map_val_id (Dijkstra/Control/Functor/Subreg.lean)

State before:
α σ : Type u
p : α → Prop
⊢ map Subtype.val id = Subtype.val ∘ fstToSubtype
Tactic:
funext x
State after:
case h
α σ : Type u
p : α → Prop
x : Subtype p × σ
⊢ map Subtype.val id x = (Subtype.val ∘ fstToSubtype) x

State before:
case h
α σ : Type u
p : α → Prop
x : Subtype p × σ
⊢ map Subtype.val id x = (Subtype.val ∘ fstToSubtype) x
Tactic:
cases x
State after:
case h.mk
α σ : Type u
p : α → Prop
fst✝ : Subtype p
snd✝ : σ
⊢ map Subtype.val id (fst✝, snd✝) = (Subtype.val ∘ fstToSubtype) (fst✝, snd✝)

State before:
case h.mk
α σ : Type u
p : α → Prop
fst✝ : Subtype p
snd✝ : σ
⊢ map Subtype.val id (fst✝, snd✝) = (Subtype.val ∘ fstToSubtype) (fst✝, snd✝)
Tactic:
rfl
State after:
no goals