Documentation

Init.ByCases

by_cases tactic and if-then-else support #

source
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.
Instances For

    if-then-else #

    source
    @[simp]
    theorem if_true {α : Sort u_1} {h : Decidable True} (t : α) (e : α) :
    (if True then t else e) = t
    source
    @[simp]
    theorem if_false {α : Sort u_1} {h : Decidable False} (t : α) (e : α) :
    (if False then t else e) = e
    source
    theorem ite_id {c : Prop} [Decidable c] {α : Sort u_1} (t : α) :
    (if c then t else t) = t
    source
    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.

    source
    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.

    source
    @[simp]
    theorem dite_not {α : Sort u_1} (P : Prop) :
    ∀ {x : Decidable P} (x_1 : ¬P → α) (y : ¬¬P → α), dite (¬P) x_1 y = dite P (fun (h : P) => y ⋯) x_1

    Negation of the condition P : Prop in a dite is the same as swapping the branches.

    source
    @[simp]
    theorem ite_not {α : Sort u_1} (P : Prop) :
    ∀ {x : Decidable P} (x_1 y : α), (if ¬P then x_1 else y) = if P then y else x_1

    Negation of the condition P : Prop in a ite is the same as swapping the branches.

    source
    @[simp]
    theorem dite_eq_left_iff {α : Sort u_1} {a : α} {P : Prop} [Decidable P] {B : ¬P → α} :
    dite P (fun (x : P) => a) B = a ↔ ∀ (h : ¬P), B h = a
    source
    @[simp]
    theorem dite_eq_right_iff {α : Sort u_1} {b : α} {P : Prop} [Decidable P] {A : P → α} :
    (dite P A fun (x : ¬P) => b) = b ↔ ∀ (h : P), A h = b
    source
    @[simp]
    theorem ite_eq_left_iff :
    ∀ {α : Sort u_1} {a b : α} {P : Prop} [inst : Decidable P], (if P then a else b) = a ↔ ¬P → b = a
    source
    @[simp]
    theorem ite_eq_right_iff :
    ∀ {α : Sort u_1} {a b : α} {P : Prop} [inst : Decidable P], (if P then a else b) = b ↔ P → a = b
    source
    @[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.

    source
    theorem ite_some_none_eq_none {P : Prop} :
    ∀ {α : Type u_1} {x : α} [inst : Decidable P], (if P then some x else none) = none ↔ ¬P
    source
    @[simp]
    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