by_cases tactic and if-then-else support

def «tacticBy_cases_:_» : Lean.ParserDescr

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

• One or more equations did not get rendered due to their size.

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 : α} [inst : 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.

@[deprecated]

theorem ite_some_none_eq_none {P : Prop} : ∀ {α : Type u_1} {x : α} [inst : Decidable P], (if P then some x else none) = none ↔ ¬P

@[deprecated]

theorem ite_some_none_eq_some {P : Prop} : ∀ {α : Type u_1} {x y : α} [inst : Decidable P], (if P then some x else none) = some y ↔ P ∧ x = y

@[deprecated]

theorem dite_some_none_eq_none {P : Prop} {α : Type u_1} [Decidable P] {x : P → α} : (if h : P then some (x h) else none) = none ↔ ¬P

@[deprecated]

theorem dite_some_none_eq_some {P : Prop} {α : Type u_1} [Decidable P] {x : P → α} {y : α} : (if h : P then some (x h) else none) = some y ↔ ∃ (h : P), x h = y