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

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

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

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