Theorem: Misc.dite_eq_right_iff (LeanSAT/Util/Misc.lean)

State before:
P : Prop
α✝ : Sort u_1
A : P → α✝
b : α✝
inst✝ : Decidable P
⊢ (dite P A fun x => b) = b ↔ ∀ (h : P), A h = b
Tactic:
by_cases P <;> simp [*, forall_prop_of_true, forall_prop_of_false]
State after:
no goals