Theorem: decideEq_and (Algdata/Init/Logic.lean)

State before:
α : Sort u
inst✝ : DecidableEq α
f : α → Bool
a b : α
⊢ (decide (a = b) && f a) = (decide (a = b) && f b)
Tactic:
apply Decidable.byCases (p:=a=b) <;> (intro h; simp [h])
State after:
no goals

State before:
case h2
α : Sort u
inst✝ : DecidableEq α
f : α → Bool
a b : α
⊢ ¬a = b → (decide (a = b) && f a) = (decide (a = b) && f b)
Tactic:
intro h
State after:
case h2
α : Sort u
inst✝ : DecidableEq α
f : α → Bool
a b : α
h : ¬a = b
⊢ (decide (a = b) && f a) = (decide (a = b) && f b)

State before:
case h2
α : Sort u
inst✝ : DecidableEq α
f : α → Bool
a b : α
h : ¬a = b
⊢ (decide (a = b) && f a) = (decide (a = b) && f b)
Tactic:
simp [h]
State after:
no goals