Theorem: ExceptT.from_toSubtype (Dijkstra/Control/Functor/Subreg.lean)

State before:
α β ε : Type u
m : Type u → Type v
inst✝² : Monad m
inst✝¹ : LawfulMonad m
inst✝ : SubregFunctor m
p : α → Prop
⊢ fromSubtype ∘ toSubtype = id
Tactic:
funext x
State after:
case h
α β ε : Type u
m : Type u → Type v
inst✝² : Monad m
inst✝¹ : LawfulMonad m
inst✝ : SubregFunctor m
p : α → Prop
x : Except ε (Subtype p)
⊢ (fromSubtype ∘ toSubtype) x = id x

State before:
case h
α β ε : Type u
m : Type u → Type v
inst✝² : Monad m
inst✝¹ : LawfulMonad m
inst✝ : SubregFunctor m
p : α → Prop
x : Except ε (Subtype p)
⊢ (fromSubtype ∘ toSubtype) x = id x
Tactic:
cases x <;> rfl
State after:
no goals