Theorem: Misc.Bool.decide_coe (LeanSAT/Util/Misc.lean)

State before:
b : Bool
h : Decidable (b = true)
⊢ decide (b = true) = b
Tactic:
cases b
State after:
case false
h : Decidable (false = true)
⊢ decide (false = true) = false

case true
h : Decidable (true = true)
⊢ decide (true = true) = true

State before:
case false
h : Decidable (false = true)
⊢ decide (false = true) = false
Tactic:
exact decide_eq_false $ λ j => by cases j
State after:
no goals

State before:
h : Decidable (false = true)
j : false = true
⊢ False
Tactic:
cases j
State after:
no goals

State before:
case true
h : Decidable (true = true)
⊢ decide (true = true) = true
Tactic:
exact decide_eq_true $ rfl
State after:
no goals