α : Type u_1
p : Option α → Prop
h : ∀ (x : α), p (some x)
x : Option α
hx : x ≠ none
this : p (some (get x (_ : isSome x = true)))
⊢ p x
α : Type u_1
p : Option α → Prop
h : ∀ (x : α), p (some x)
x : Option α
hx : x ≠ none
⊢ p x
have := h <| x.get <| ne_none_iff_isSome.1 hx
α : Type u_1
p : Option α → Prop
h : ∀ (x : α), p (some x)
x : Option α
hx : x ≠ none
this : p x
⊢ p x
α : Type u_1
p : Option α → Prop
h : ∀ (x : α), p (some x)
x : Option α
hx : x ≠ none
this : p (some (get x (_ : isSome x = true)))
⊢ p x
simp [some_get] at this ⊢
no goals
α : Type u_1
p : Option α → Prop
h : ∀ (x : α), p (some x)
x : Option α
hx : x ≠ none
this : p x
⊢ p x
exact this