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

State before:
α : Sort u
inst✝ : DecidableEq α
f : α → Bool
a b : α
⊢ (f a && decide (a = b)) = (f b && decide (a = 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 → (f a && decide (a = b)) = (f b && decide (a = b))
Tactic:
intro h
State after:
case h2
α : Sort u
inst✝ : DecidableEq α
f : α → Bool
a b : α
h : ¬a = b
⊢ (f a && decide (a = b)) = (f b && decide (a = b))

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