does lean know?

Stream: general

[Sean Leather]

Is this in the standard library or mathlib?

theorem if_distrib {c : Prop} [decidable c] {α β : Type} {f : α → β} {a b : α}:
  f (if c then a else b) = if c then f a else f b :=
by by_cases h : c; [simp [if_pos h], simp [if_neg h]]

[Sean Leather]

@Kenny Lau: FYI, the topic title is in homage to your questions. :simple_smile:

[Kenny Lau]

:D