Theorem: Option.guardProp_isSome (Etch/Verification/Misc.lean)

State before:
m : Type u → Type v
inst✝¹ : Monad m
α : Type u_1
p : Prop
inst✝ : Decidable p
x : α
⊢ isSome (guardProp p x) = true ↔ p
Tactic:
dsimp only [Option.guardProp]
State after:
m : Type u → Type v
inst✝¹ : Monad m
α : Type u_1
p : Prop
inst✝ : Decidable p
x : α
⊢ isSome (if p then some x else none) = true ↔ p

State before:
m : Type u → Type v
inst✝¹ : Monad m
α : Type u_1
p : Prop
inst✝ : Decidable p
x : α
⊢ isSome (if p then some x else none) = true ↔ p
Tactic:
split_ifs <;> simpa
State after:
no goals