Documentation

Init.ByCases

by_cases tactic and if-then-else support #

by_cases (h :)? p splits the main goal into two cases, assuming h : p in the first branch, and h : ¬ p in the second branch.

Equations
    Instances For

      if-then-else #

      @[simp]
      theorem if_true {α : Sort u_1} {x✝ : Decidable True} (t e : α) :
      (if True then t else e) = t
      @[simp]
      theorem if_false {α : Sort u_1} {x✝ : Decidable False} (t e : α) :
      (if False then t else e) = e
      theorem ite_id {c : Prop} [Decidable c] {α : Sort u_1} (t : α) :
      (if c then t else t) = t
      theorem apply_dite {α : Sort u_1} {β : Sort u_2} (f : αβ) (P : Prop) [Decidable P] (x : Pα) (y : ¬Pα) :
      f (dite P x y) = if h : P then f (x h) else f (y h)

      A function applied to a dite is a dite of that function applied to each of the branches.

      theorem apply_ite {α : Sort u_1} {β : Sort u_2} (f : αβ) (P : Prop) [Decidable P] (x y : α) :
      f (if P then x else y) = if P then f x else f y

      A function applied to a ite is a ite of that function applied to each of the branches.

      @[simp]
      theorem dite_eq_ite {P : Prop} {α✝ : Sort u_1} {a b : α✝} [Decidable P] :
      (if x : P then a else b) = if P then a else b

      A dite whose results do not actually depend on the condition may be reduced to an ite.