Theorem: ExceptT.errorOrApply_val (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
⊢ errorOrApply Subtype.val = Subtype.val ∘ toSubtype
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)
⊢ errorOrApply Subtype.val x = (Subtype.val ∘ toSubtype) 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)
⊢ errorOrApply Subtype.val x = (Subtype.val ∘ toSubtype) x
Tactic:
cases x <;> rfl
State after:
no goals