ε : Type u_1
α✝ : Type u_2
p : α✝ → Prop
⊢ ∀ {x : Except ε α✝}, SatisfiesM p x → ∀ (a : α✝), x = Except.ok a → p a
ε : Type u_1
α✝ : Type u_2
p : α✝ → Prop
x : Except ε α✝
⊢ SatisfiesM p x → ∀ (a : α✝), x = Except.ok a → p a
revert x
no goals
ε : Type u_1
α✝ : Type u_2
p : α✝ → Prop
⊢ ∀ {x : Except ε α✝}, SatisfiesM p x → ∀ (a : α✝), x = Except.ok a → p a
intro | .ok _, ⟨.ok ⟨_, h⟩, rfl⟩, _, rfl => exact h
no goals
ε : Type u_1
α✝ : Type u_2
p : α✝ → Prop
x✝³ : Except ε α✝
x✝² : SatisfiesM p x✝³
x✝¹ : α✝
x✝ : x✝³ = Except.ok x✝¹
val✝ : α✝
h : p val✝
⊢ p { val := val✝, property := h }.val
exact h