Documentation

Init.PropLemmas

cast and equality #

source
@[simp]
theorem eq_mp_eq_cast {α β : Sort u_1} (h : α = β) :
h.mp = cast h
source
@[simp]
theorem eq_mpr_eq_cast {α β : Sort u_1} (h : α = β) :
h.mpr = cast ⋯
source
@[simp]
theorem cast_cast {α β γ : Sort u_1} (ha : α = β) (hb : β = γ) (a : α) :
cast hb (cast ha a) = cast ⋯ a
source
@[simp]
theorem eq_true_eq_id :
Eq True = id
source
theorem proof_irrel_heq {p q : Prop} (hp : p) (hq : q) :
hp ≍ hq

not #

source
theorem not_not_em (a : Prop) :
¬¬(a ∨ ¬a)

and #

source
theorem and_self_iff {a : Prop} :
a ∧ a ↔ a
source
theorem and_not_self_iff (a : Prop) :
a ∧ ¬a ↔ False
source
theorem not_and_self_iff (a : Prop) :
¬a ∧ a ↔ False
source
theorem And.imp {a c b d : Prop} (f : a → c) (g : b → d) (h : a ∧ b) :
c ∧ d
source
theorem And.imp_left {a b c : Prop} (h : a → b) :
a ∧ c → b ∧ c
source
theorem And.imp_right {a b c : Prop} (h : a → b) :
c ∧ a → c ∧ b
source
theorem and_congr {a c b d : Prop} (h₁ : a ↔ c) (h₂ : b ↔ d) :
a ∧ b ↔ c ∧ d
source
theorem and_congr_left' {a b c : Prop} (h : a ↔ b) :
a ∧ c ↔ b ∧ c
source
theorem and_congr_right' {b c a : Prop} (h : b ↔ c) :
a ∧ b ↔ a ∧ c
source
theorem not_and_of_not_left {a : Prop} (b : Prop) :
¬a → ¬(a ∧ b)
source
theorem not_and_of_not_right (a : Prop) {b : Prop} :
¬b → ¬(a ∧ b)
source
theorem and_congr_right_eq {a b c : Prop} (h : a → b = c) :
(a ∧ b) = (a ∧ c)
source
theorem and_congr_left_eq {c a b : Prop} (h : c → a = b) :
(a ∧ c) = (b ∧ c)
source
theorem and_left_comm {a b c : Prop} :
a ∧ b ∧ c ↔ b ∧ a ∧ c
source
theorem and_right_comm {a b c : Prop} :
(a ∧ b) ∧ c ↔ (a ∧ c) ∧ b
source
theorem and_rotate {a b c : Prop} :
a ∧ b ∧ c ↔ b ∧ c ∧ a
source
theorem and_and_and_comm {a b c d : Prop} :
(a ∧ b) ∧ c ∧ d ↔ (a ∧ c) ∧ b ∧ d
source
theorem and_and_left {a b c : Prop} :
a ∧ b ∧ c ↔ (a ∧ b) ∧ a ∧ c
source
theorem and_and_right {a b c : Prop} :
(a ∧ b) ∧ c ↔ (a ∧ c) ∧ b ∧ c
source
theorem and_iff_left {b a : Prop} (hb : b) :
a ∧ b ↔ a
source
theorem and_iff_right {a b : Prop} (ha : a) :
a ∧ b ↔ b

or #

source
theorem or_self_iff {a : Prop} :
a ∨ a ↔ a
source
theorem not_or_intro {a b : Prop} (ha : ¬a) (hb : ¬b) :
¬(a ∨ b)
source
theorem or_congr {a c b d : Prop} (h₁ : a ↔ c) (h₂ : b ↔ d) :
a ∨ b ↔ c ∨ d
source
theorem or_congr_left {a b c : Prop} (h : a ↔ b) :
a ∨ c ↔ b ∨ c
source
theorem or_congr_right {b c a : Prop} (h : b ↔ c) :
a ∨ b ↔ a ∨ c
source
theorem or_left_comm {a b c : Prop} :
a ∨ b ∨ c ↔ b ∨ a ∨ c
source
theorem or_right_comm {a b c : Prop} :
(a ∨ b) ∨ c ↔ (a ∨ c) ∨ b
source
theorem or_or_or_comm {a b c d : Prop} :
(a ∨ b) ∨ c ∨ d ↔ (a ∨ c) ∨ b ∨ d
source
theorem or_or_distrib_left {a b c : Prop} :
a ∨ b ∨ c ↔ (a ∨ b) ∨ a ∨ c
source
theorem or_or_distrib_right {a b c : Prop} :
(a ∨ b) ∨ c ↔ (a ∨ c) ∨ b ∨ c
source
theorem or_rotate {a b c : Prop} :
a ∨ b ∨ c ↔ b ∨ c ∨ a
source
theorem or_iff_left {b a : Prop} (hb : ¬b) :
a ∨ b ↔ a
source
theorem or_iff_right {a b : Prop} (ha : ¬a) :
a ∨ b ↔ b

distributivity #

source
theorem not_imp_of_and_not {a b : Prop} :
a ∧ ¬b → ¬(a → b)
source
theorem imp_and {b c : Prop} {α : Sort u_1} :
(∀ (a : α), b ∧ c) ↔ (∀ (a : α), b) ∧ ∀ (a : α), c
source
theorem not_and' {a b : Prop} :
¬(a ∧ b) ↔ b → ¬a
source
theorem and_or_left {a b c : Prop} :
a ∧ (b ∨ c) ↔ a ∧ b ∨ a ∧ c

∧ distributes over ∨ (on the left).

source
theorem or_and_right {a b c : Prop} :
(a ∨ b) ∧ c ↔ a ∧ c ∨ b ∧ c

∧ distributes over ∨ (on the right).

source
theorem or_and_left {a b c : Prop} :
a ∨ b ∧ c ↔ (a ∨ b) ∧ (a ∨ c)

∨ distributes over ∧ (on the left).

source
theorem and_or_right {a b c : Prop} :
a ∧ b ∨ c ↔ (a ∨ c) ∧ (b ∨ c)

∨ distributes over ∧ (on the right).

source
theorem or_imp {a b c : Prop} :
a ∨ b → c ↔ (a → c) ∧ (b → c)
source
@[simp]
theorem not_or {p q : Prop} :
¬(p ∨ q) ↔ ¬p ∧ ¬q
source
theorem not_and_of_not_or_not {a b : Prop} (h : ¬a ∨ ¬b) :
¬(a ∧ b)

not equal #

source
theorem ne_of_apply_ne {α : Sort u_1} {β : Sort u_2} (f : α → β) {x y : α} :
f x ≠ f y → x ≠ y

Ite #

source
@[simp]
theorem if_false_left {p q : Prop} [h : Decidable p] :
(if p then False else q) ↔ ¬p ∧ q
source
@[simp]
theorem if_false_right {p q : Prop} [h : Decidable p] :
(if p then q else False) ↔ p ∧ q
source
@[simp]
theorem if_true_left {p q : Prop} [h : Decidable p] :
(if p then True else q) ↔ ¬p → q
source
@[simp]
theorem if_true_right {p q : Prop} [h : Decidable p] :
(if p then q else True) ↔ p → q
source
@[simp]
theorem dite_not {p : Prop} {α : Sort u_1} [hn : Decidable ¬p] [h : Decidable p] (x : ¬p → α) (y : ¬¬p → α) :
dite (¬p) x y = dite p (fun (h : p) => y ⋯) x

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) [Decidable p] (x y : α) :
(if ¬p then x else y) = if p then y else x

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

source
@[simp]
theorem ite_then_self {p q : Prop} [h : Decidable p] :
(if p then p else q) ↔ ¬p → q
source
@[simp]
theorem ite_else_self {p q : Prop} [h : Decidable p] :
(if p then q else p) ↔ p ∧ q
source
@[simp]
theorem ite_then_not_self {p : Prop} [Decidable p] {q : Prop} :
(if p then ¬p else q) ↔ ¬p ∧ q
source
@[simp]
theorem ite_else_not_self {p : Prop} [Decidable p] {q : Prop} :
(if p then q else ¬p) ↔ p → q
source
@[simp]
theorem ite_eq_ite {α : Sort u_1} (p : Prop) {h h' : Decidable p} (x y : α) :
((if p then x else y) = if p then x else y) ↔ True

If two if-then-else statements only differ by the Decidable instances, they are equal.

source
@[simp]
theorem ite_iff_ite (p : Prop) {h h' : Decidable p} (x y : Prop) :
((if p then x else y) ↔ if p then x else y) ↔ True

If two if-then-else statements only differ by the Decidable instances, they are equal.

exists and forall #

source
theorem forall_imp {α : Sort u_1} {p q : α → Prop} (h : ∀ (a : α), p a → q a) :
(∀ (a : α), p a) → ∀ (a : α), q a
source
@[simp]
theorem forall_exists_index {α : Sort u_1} {p : α → Prop} {q : (∃ (x : α), p x) → Prop} :
(∀ (h : ∃ (x : α), p x), q h) ↔ ∀ (x : α) (h : p x), q ⋯

As simp does not index foralls, this @[simp] lemma is tried on every forall expression. This is not ideal, and likely a performance issue, but it is difficult to remove this attribute at this time.

source
theorem Exists.imp {α : Sort u_1} {p q : α → Prop} (h : ∀ (a : α), p a → q a) :
(∃ (a : α), p a) → ∃ (a : α), q a
source
theorem Exists.imp' {α : Sort u_2} {p : α → Prop} {β : Sort u_1} {q : β → Prop} (f : α → β) (hpq : ∀ (a : α), p a → q (f a)) :
(∃ (a : α), p a) → ∃ (b : β), q b
source
theorem exists_imp {α : Sort u_1} {p : α → Prop} {b : Prop} :
(∃ (x : α), p x) → b ↔ ∀ (x : α), p x → b
source
theorem exists₂_imp {α : Sort u_1} {p : α → Prop} {b : Prop} {P : (x : α) → p x → Prop} :
(∃ (x : α), ∃ (h : p x), P x h) → b ↔ ∀ (x : α) (h : p x), P x h → b
source
@[simp]
theorem exists_const {b : Prop} (α : Sort u_1) [i : Nonempty α] :
(∃ (x : α), b) ↔ b
source
theorem exists_prop_congr {p p' : Prop} {q q' : p → Prop} (hq : ∀ (h : p), q h ↔ q' h) (hp : p ↔ p') :
Exists q ↔ ∃ (h : p'), q' ⋯
source
theorem exists_prop_of_true {p : Prop} {q : p → Prop} (h : p) :
(∃ (h' : p), q h') ↔ q h
source
@[simp]
theorem exists_true_left {p : True → Prop} :
Exists p ↔ p True.intro
source
theorem forall_congr' {α : Sort u_1} {p q : α → Prop} (h : ∀ (a : α), p a ↔ q a) :
(∀ (a : α), p a) ↔ ∀ (a : α), q a
source
theorem exists_congr {α : Sort u_1} {p q : α → Prop} (h : ∀ (a : α), p a ↔ q a) :
(∃ (a : α), p a) ↔ ∃ (a : α), q a
source
theorem forall₂_congr {α : Sort u_1} {β : α → Sort u_2} {p q : (a : α) → β a → Prop} (h : ∀ (a : α) (b : β a), p a b ↔ q a b) :
(∀ (a : α) (b : β a), p a b) ↔ ∀ (a : α) (b : β a), q a b
source
theorem exists₂_congr {α : Sort u_1} {β : α → Sort u_2} {p q : (a : α) → β a → Prop} (h : ∀ (a : α) (b : β a), p a b ↔ q a b) :
(∃ (a : α), ∃ (b : β a), p a b) ↔ ∃ (a : α), ∃ (b : β a), q a b
source
theorem forall₃_congr {α : Sort u_1} {β : α → Sort u_2} {γ : (a : α) → β a → Sort u_3} {p q : (a : α) → (b : β a) → γ a b → Prop} (h : ∀ (a : α) (b : β a) (c : γ a b), p a b c ↔ q a b c) :
(∀ (a : α) (b : β a) (c : γ a b), p a b c) ↔ ∀ (a : α) (b : β a) (c : γ a b), q a b c
source
theorem exists₃_congr {α : Sort u_1} {β : α → Sort u_2} {γ : (a : α) → β a → Sort u_3} {p q : (a : α) → (b : β a) → γ a b → Prop} (h : ∀ (a : α) (b : β a) (c : γ a b), p a b c ↔ q a b c) :
(∃ (a : α), ∃ (b : β a), ∃ (c : γ a b), p a b c) ↔ ∃ (a : α), ∃ (b : β a), ∃ (c : γ a b), q a b c
source
theorem forall₄_congr {α : Sort u_1} {β : α → Sort u_2} {γ : (a : α) → β a → Sort u_3} {δ : (a : α) → (b : β a) → γ a b → Sort u_4} {p q : (a : α) → (b : β a) → (c : γ a b) → δ a b c → Prop} (h : ∀ (a : α) (b : β a) (c : γ a b) (d : δ a b c), p a b c d ↔ q a b c d) :
(∀ (a : α) (b : β a) (c : γ a b) (d : δ a b c), p a b c d) ↔ ∀ (a : α) (b : β a) (c : γ a b) (d : δ a b c), q a b c d
source
theorem exists₄_congr {α : Sort u_1} {β : α → Sort u_2} {γ : (a : α) → β a → Sort u_3} {δ : (a : α) → (b : β a) → γ a b → Sort u_4} {p q : (a : α) → (b : β a) → (c : γ a b) → δ a b c → Prop} (h : ∀ (a : α) (b : β a) (c : γ a b) (d : δ a b c), p a b c d ↔ q a b c d) :
(∃ (a : α), ∃ (b : β a), ∃ (c : γ a b), ∃ (d : δ a b c), p a b c d) ↔ ∃ (a : α), ∃ (b : β a), ∃ (c : γ a b), ∃ (d : δ a b c), q a b c d
source
theorem forall₅_congr {α : Sort u_1} {β : α → Sort u_2} {γ : (a : α) → β a → Sort u_3} {δ : (a : α) → (b : β a) → γ a b → Sort u_4} {ε : (a : α) → (b : β a) → (c : γ a b) → δ a b c → Sort u_5} {p q : (a : α) → (b : β a) → (c : γ a b) → (d : δ a b c) → ε a b c d → Prop} (h : ∀ (a : α) (b : β a) (c : γ a b) (d : δ a b c) (e : ε a b c d), p a b c d e ↔ q a b c d e) :
(∀ (a : α) (b : β a) (c : γ a b) (d : δ a b c) (e : ε a b c d), p a b c d e) ↔ ∀ (a : α) (b : β a) (c : γ a b) (d : δ a b c) (e : ε a b c d), q a b c d e
source
theorem exists₅_congr {α : Sort u_1} {β : α → Sort u_2} {γ : (a : α) → β a → Sort u_3} {δ : (a : α) → (b : β a) → γ a b → Sort u_4} {ε : (a : α) → (b : β a) → (c : γ a b) → δ a b c → Sort u_5} {p q : (a : α) → (b : β a) → (c : γ a b) → (d : δ a b c) → ε a b c d → Prop} (h : ∀ (a : α) (b : β a) (c : γ a b) (d : δ a b c) (e : ε a b c d), p a b c d e ↔ q a b c d e) :
(∃ (a : α), ∃ (b : β a), ∃ (c : γ a b), ∃ (d : δ a b c), ∃ (e : ε a b c d), p a b c d e) ↔ ∃ (a : α), ∃ (b : β a), ∃ (c : γ a b), ∃ (d : δ a b c), ∃ (e : ε a b c d), q a b c d e
source
@[simp]
theorem not_exists {α : Sort u_1} {p : α → Prop} :
(¬∃ (x : α), p x) ↔ ∀ (x : α), ¬p x
source
theorem forall_not_of_not_exists {α : Sort u_1} {p : α → Prop} (h : ¬∃ (x : α), p x) (x : α) :
¬p x
source
theorem not_exists_of_forall_not {α : Sort u_1} {p : α → Prop} (h : ∀ (x : α), ¬p x) :
¬∃ (x : α), p x
source
theorem forall_and {α : Sort u_1} {p q : α → Prop} :
(∀ (x : α), p x ∧ q x) ↔ (∀ (x : α), p x) ∧ ∀ (x : α), q x
source
theorem exists_or {α : Sort u_1} {p q : α → Prop} :
(∃ (x : α), p x ∨ q x) ↔ (∃ (x : α), p x) ∨ ∃ (x : α), q x
source
@[simp]
theorem exists_false {α : Sort u_1} :
¬∃ (_a : α), False
source
@[simp]
theorem forall_const {b : Prop} (α : Sort u_1) [i : Nonempty α] :
(∀ (a : α), b) ↔ b
source
theorem Exists.nonempty {α : Sort u_1} {p : α → Prop} :
(∃ (x : α), p x) → Nonempty α
source
theorem not_forall_of_exists_not {α : Sort u_1} {p : α → Prop} :
(∃ (x : α), ¬p x) → ¬∀ (x : α), p x
source
@[simp]
theorem forall_eq {α : Sort u_1} {p : α → Prop} {a' : α} :
(∀ (a : α), a = a' → p a) ↔ p a'
source
@[simp]
theorem forall_eq' {α : Sort u_1} {p : α → Prop} {a' : α} :
(∀ (a : α), a' = a → p a) ↔ p a'
source
@[simp]
theorem exists_eq {α✝ : Sort u_1} {a' : α✝} :
∃ (a : α✝), a = a'
source
@[simp]
theorem exists_eq' {α✝ : Sort u_1} {a' : α✝} :
∃ (a : α✝), a' = a
source
@[simp]
theorem exists_eq_left {α : Sort u_1} {p : α → Prop} {a' : α} :
(∃ (a : α), a = a' ∧ p a) ↔ p a'
source
@[simp]
theorem exists_eq_right {α : Sort u_1} {p : α → Prop} {a' : α} :
(∃ (a : α), p a ∧ a = a') ↔ p a'
source
@[simp]
theorem exists_and_left {α : Sort u_1} {p : α → Prop} {b : Prop} :
(∃ (x : α), b ∧ p x) ↔ b ∧ ∃ (x : α), p x
source
@[simp]
theorem exists_and_right {α : Sort u_1} {p : α → Prop} {b : Prop} :
(∃ (x : α), p x ∧ b) ↔ (∃ (x : α), p x) ∧ b
source
@[simp]
theorem exists_eq_left' {α : Sort u_1} {p : α → Prop} {a' : α} :
(∃ (a : α), a' = a ∧ p a) ↔ p a'
source
@[simp]
theorem exists_eq_right' {α : Sort u_1} {p : α → Prop} {a' : α} :
(∃ (a : α), p a ∧ a' = a) ↔ p a'
source
@[simp]
theorem exists_prop_eq {α : Sort u_1} {a' : α} {p : (a : α) → a = a' → Prop} :
(∃ (a : α), ∃ (h : a = a'), p a h) ↔ p a' ⋯
source
@[simp]
theorem exists_prop_eq' {α : Sort u_1} {a' : α} {p : (a : α) → a' = a → Prop} :
(∃ (a : α), ∃ (h : a' = a), p a h) ↔ p a' ⋯
source
@[simp]
theorem forall_eq_or_imp {α : Sort u_1} {p q : α → Prop} {a' : α} :
(∀ (a : α), a = a' ∨ q a → p a) ↔ p a' ∧ ∀ (a : α), q a → p a
source
@[simp]
theorem exists_eq_or_imp {α : Sort u_1} {p q : α → Prop} {a' : α} :
(∃ (a : α), (a = a' ∨ q a) ∧ p a) ↔ p a' ∨ ∃ (a : α), q a ∧ p a
source
@[simp]
theorem exists_eq_right_right {α : Sort u_1} {p q : α → Prop} {a' : α} :
(∃ (a : α), p a ∧ q a ∧ a = a') ↔ p a' ∧ q a'
source
@[simp]
theorem exists_eq_right_right' {α : Sort u_1} {p q : α → Prop} {a' : α} :
(∃ (a : α), p a ∧ q a ∧ a' = a) ↔ p a' ∧ q a'
source
@[simp]
theorem exists_or_eq_left {α : Sort u_1} (y : α) (p : α → Prop) :
∃ (x : α), x = y ∨ p x
source
@[simp]
theorem exists_or_eq_right {α : Sort u_1} (y : α) (p : α → Prop) :
∃ (x : α), p x ∨ x = y
source
@[simp]
theorem exists_or_eq_left' {α : Sort u_1} (y : α) (p : α → Prop) :
∃ (x : α), y = x ∨ p x
source
@[simp]
theorem exists_or_eq_right' {α : Sort u_1} (y : α) (p : α → Prop) :
∃ (x : α), p x ∨ y = x
source
theorem exists_prop' {α : Sort u_1} {p : Prop} :
(∃ (x : α), p) ↔ Nonempty α ∧ p
source
@[simp]
theorem exists_prop {b a : Prop} :
(∃ (_h : a), b) ↔ a ∧ b
source
@[simp]
theorem exists_idem {P : Prop} (f : P → P → Prop) :
(∃ (p₁ : P), ∃ (p₂ : P), f p₁ p₂) ↔ ∃ (p : P), f p p
source
@[simp]
theorem exists_apply_eq_apply {α : Sort u_2} {β : Sort u_1} (f : α → β) (a' : α) :
∃ (a : α), f a = f a'
source
theorem forall_prop_of_true {p : Prop} {q : p → Prop} (h : p) :
(∀ (h' : p), q h') ↔ q h
source
theorem forall_comm {α : Sort u_2} {β : Sort u_1} {p : α → β → Prop} :
(∀ (a : α) (b : β), p a b) ↔ ∀ (b : β) (a : α), p a b
source
theorem exists_comm {α : Sort u_2} {β : Sort u_1} {p : α → β → Prop} :
(∃ (a : α), ∃ (b : β), p a b) ↔ ∃ (b : β), ∃ (a : α), p a b
source
@[simp]
theorem forall_apply_eq_imp_iff {α : Sort u_2} {β : Sort u_1} {f : α → β} {p : β → Prop} :
(∀ (b : β) (a : α), f a = b → p b) ↔ ∀ (a : α), p (f a)
source
@[simp]
theorem forall_eq_apply_imp_iff {α : Sort u_2} {β : Sort u_1} {f : α → β} {p : β → Prop} :
(∀ (b : β) (a : α), b = f a → p b) ↔ ∀ (a : α), p (f a)
source
@[simp]
theorem forall_apply_eq_imp_iff₂ {α : Sort u_2} {β : Sort u_1} {f : α → β} {p : α → Prop} {q : β → Prop} :
(∀ (b : β) (a : α), p a → f a = b → q b) ↔ ∀ (a : α), p a → q (f a)
source
theorem forall_prop_of_false {p : Prop} {q : p → Prop} (hn : ¬p) :
(∀ (h' : p), q h') ↔ True
source
@[simp]
theorem and_exists_self (P : Prop) (Q : P → Prop) :
(P ∧ ∃ (p : P), Q p) ↔ ∃ (p : P), Q p
source
@[simp]
theorem exists_and_self (P : Prop) (Q : P → Prop) :
(∃ (p : P), Q p) ∧ P ↔ ∃ (p : P), Q p
source
@[simp]
theorem forall_self_imp (P : Prop) (Q : P → Prop) :
(∀ (p : P), P → Q p) ↔ ∀ (p : P), Q p

membership #

source
theorem ne_of_mem_of_not_mem {α : Type u_1} {β : Type u_2} [Membership α β] {s : β} {a b : α} (h : a ∈ s) :
¬b ∈ s → a ≠ b
source
theorem ne_of_mem_of_not_mem' {α : Type u_1} {β : Type u_2} [Membership α β] {s t : β} {a : α} (h : a ∈ s) :
¬a ∈ t → s ≠ t

Nonempty #

source
@[simp]
theorem nonempty_prop {p : Prop} :
Nonempty p ↔ p

decidable #

source
@[simp]
theorem Decidable.not_not {p : Prop} [Decidable p] :
¬¬p ↔ p
source
@[reducible, inline]
abbrev Decidable.or_not_self (p : Prop) [Decidable p] :
p ∨ ¬p

Excluded middle. Added as alias for Decidable.em

Instances For
    source
    theorem Decidable.not_or_self (p : Prop) [h : Decidable p] :
    ¬p ∨ p

    Excluded middle commuted. Added as alias for Decidable.em

    source
    theorem Decidable.by_contra {p : Prop} [Decidable p] :
    (¬p → False) → p
    source
    def Or.by_cases {p q : Prop} [Decidable p] {α : Sort u} (h : p ∨ q) (h₁ : p → α) (h₂ : q → α) :
    α

    Construct a non-Prop by cases on an Or, when the left conjunct is decidable.

    Instances For
      source
      def Or.by_cases' {q p : Prop} [Decidable q] {α : Sort u} (h : p ∨ q) (h₁ : p → α) (h₂ : q → α) :
      α

      Construct a non-Prop by cases on an Or, when the right conjunct is decidable.

      Instances For
        source
        @[implicit_reducible, inline]
        instance exists_prop_decidable {p : Prop} (P : p → Prop) [Decidable p] [(h : p) → Decidable (P h)] :
        Decidable (∃ (h : p), P h)
        source
        @[implicit_reducible, inline]
        instance forall_prop_decidable {p : Prop} (P : p → Prop) [Decidable p] [(h : p) → Decidable (P h)] :
        Decidable (∀ (h : p), P h)
        source
        theorem decide_eq_true_iff {p : Prop} [Decidable p] :
        decide p = true ↔ p
        source
        @[simp]
        theorem decide_eq_decide {p q : Prop} {x✝ : Decidable p} {x✝¹ : Decidable q} :
        decide p = decide q ↔ (p ↔ q)
        source
        theorem Decidable.of_not_imp {a b : Prop} [Decidable a] (h : ¬(a → b)) :
        a
        source
        theorem Decidable.not_imp_symm {a b : Prop} [Decidable a] (h : ¬a → b) (hb : ¬b) :
        a
        source
        theorem Decidable.not_imp_comm {a b : Prop} [Decidable a] [Decidable b] :
        ¬a → b ↔ ¬b → a
        source
        theorem Decidable.not_imp_self {a : Prop} [Decidable a] :
        ¬a → a ↔ a
        source
        theorem Decidable.or_iff_not_imp_left {a b : Prop} [Decidable a] :
        a ∨ b ↔ ¬a → b
        source
        theorem Decidable.or_iff_not_imp_right {b a : Prop} [Decidable b] :
        a ∨ b ↔ ¬b → a
        source
        theorem Decidable.not_imp_not {a b : Prop} [Decidable a] :
        ¬a → ¬b ↔ b → a
        source
        theorem Decidable.not_or_of_imp {a b : Prop} [Decidable a] (h : a → b) :
        ¬a ∨ b
        source
        theorem Decidable.imp_iff_not_or {a b : Prop} [Decidable a] :
        a → b ↔ ¬a ∨ b
        source
        theorem Decidable.imp_iff_or_not {b a : Prop} [Decidable b] :
        b → a ↔ a ∨ ¬b
        source
        theorem Decidable.imp_or {a b c : Prop} [Decidable a] :
        a → b ∨ c ↔ (a → b) ∨ (a → c)
        source
        theorem Decidable.imp_or' {b : Prop} {a : Sort u_1} {c : Prop} [Decidable b] :
        (∀ (a : a), b ∨ c) ↔ (∀ (a : a), b) ∨ ∀ (a : a), c
        source
        theorem Decidable.not_imp_iff_and_not {a b : Prop} [Decidable a] :
        ¬(a → b) ↔ a ∧ ¬b
        source
        theorem Decidable.peirce (a b : Prop) [Decidable a] :
        ((a → b) → a) → a
        source
        theorem peirce' {a : Prop} (H : ∀ (b : Prop), (a → b) → a) :
        a
        source
        theorem Decidable.not_iff_not {a b : Prop} [Decidable a] [Decidable b] :
        (¬a ↔ ¬b) ↔ (a ↔ b)
        source
        theorem Decidable.not_iff_comm {a b : Prop} [Decidable a] [Decidable b] :
        (¬a ↔ b) ↔ (¬b ↔ a)
        source
        theorem Decidable.not_iff {b a : Prop} [Decidable b] :
        ¬(a ↔ b) ↔ (¬a ↔ b)
        source
        theorem Decidable.iff_not_comm {a b : Prop} [Decidable a] [Decidable b] :
        (a ↔ ¬b) ↔ (b ↔ ¬a)
        source
        theorem Decidable.iff_iff_and_or_not_and_not {a b : Prop} [Decidable b] :
        (a ↔ b) ↔ a ∧ b ∨ ¬a ∧ ¬b
        source
        theorem Decidable.iff_iff_not_or_and_or_not {a b : Prop} [Decidable a] [Decidable b] :
        (a ↔ b) ↔ (¬a ∨ b) ∧ (a ∨ ¬b)
        source
        theorem Decidable.not_and_not_right {b a : Prop} [Decidable b] :
        ¬(a ∧ ¬b) ↔ a → b
        source
        theorem Decidable.not_and_iff_not_or_not {a b : Prop} [Decidable a] :
        ¬(a ∧ b) ↔ ¬a ∨ ¬b
        source
        theorem Decidable.not_and_iff_not_or_not' {b a : Prop} [Decidable b] :
        ¬(a ∧ b) ↔ ¬a ∨ ¬b
        source
        theorem Decidable.or_iff_not_not_and_not {a b : Prop} [Decidable a] [Decidable b] :
        a ∨ b ↔ ¬(¬a ∧ ¬b)
        source
        theorem Decidable.and_iff_not_not_or_not {a b : Prop} [Decidable a] [Decidable b] :
        a ∧ b ↔ ¬(¬a ∨ ¬b)
        source
        theorem Decidable.imp_iff_right_iff {a b : Prop} [Decidable a] :
        (a → b ↔ b) ↔ a ∨ b
        source
        theorem Decidable.imp_iff_left_iff {a b : Prop} [Decidable a] :
        (b ↔ a → b) ↔ a ∨ b
        source
        theorem Decidable.and_or_imp {a b c : Prop} [Decidable a] :
        a ∧ b ∨ (a → c) ↔ a → b ∨ c
        source
        theorem Decidable.or_congr_left' {c a b : Prop} [Decidable c] (h : ¬c → (a ↔ b)) :
        a ∨ c ↔ b ∨ c
        source
        theorem Decidable.or_congr_right' {a b c : Prop} [Decidable a] (h : ¬a → (b ↔ c)) :
        a ∨ b ↔ a ∨ c
        source
        @[simp]
        theorem Decidable.iff_congr_left {P Q R : Prop} [Decidable P] [Decidable Q] [Decidable R] :
        ((P ↔ R) ↔ (Q ↔ R)) ↔ (P ↔ Q)
        source
        @[simp]
        theorem Decidable.iff_congr_right {P Q R : Prop} [Decidable P] [Decidable Q] [Decidable R] :
        ((P ↔ Q) ↔ (P ↔ R)) ↔ (Q ↔ R)
        source
        @[inline]
        def decidable_of_iff {b : Prop} (a : Prop) (h : a ↔ b) [Decidable a] :
        Decidable b

        Transfer decidability of a to decidability of b, if the propositions are equivalent. Important: this function should be used instead of rw on Decidable b, because the kernel will get stuck reducing the usage of propext otherwise, and decide will not work.

        Instances For
          source
          @[inline]
          def decidable_of_iff' {a : Prop} (b : Prop) (h : a ↔ b) [Decidable b] :
          Decidable a

          Transfer decidability of b to decidability of a, if the propositions are equivalent. This is the same as decidable_of_iff but the iff is flipped.

          Instances For
            source
            @[implicit_reducible]
            instance Decidable.predToBool {α : Sort u_1} (p : α → Prop) [DecidablePred p] :
            CoeDep (α → Prop) p (α → Bool)
            source
            @[implicit_reducible]
            instance instDecidablePredComp {α✝ : Sort u_1} {p : α✝ → Prop} {α✝¹ : Sort u_2} {f : α✝¹ → α✝} [DecidablePred p] :
            DecidablePred (p ∘ f)
            source
            def decidable_of_bool {a : Prop} (b : Bool) :
            (b = true ↔ a) → Decidable a

            Prove that a is decidable by constructing a boolean b and a proof that b ↔ a. (This is sometimes taken as an alternate definition of decidability.)

            Instances For
              source
              theorem Decidable.not_forall {α : Sort u_1} {p : α → Prop} [Decidable (∃ (x : α), ¬p x)] [(x : α) → Decidable (p x)] :
              (¬∀ (x : α), p x) ↔ ∃ (x : α), ¬p x
              source
              theorem Decidable.not_forall_not {α : Sort u_1} {p : α → Prop} [Decidable (∃ (x : α), p x)] :
              (¬∀ (x : α), ¬p x) ↔ ∃ (x : α), p x
              source
              theorem Decidable.not_exists_not {α : Sort u_1} {p : α → Prop} [(x : α) → Decidable (p x)] :
              (¬∃ (x : α), ¬p x) ↔ ∀ (x : α), p x
              source
              @[simp]
              theorem decide_implies (u v : Prop) [duv : Decidable (u → v)] [du : Decidable u] {dv : u → Decidable v} :
              decide (u → v) = if h : u then decide v else true
              source
              @[simp]
              theorem decide_ite (u : Prop) [du : Decidable u] (p q : Prop) [dpq : Decidable (if u then p else q)] [dp : Decidable p] [dq : Decidable q] :
              decide (if u then p else q) = if u then decide p else decide q
              source
              @[simp]
              theorem ite_then_decide_self (p : Prop) [h : Decidable p] {w : Decidable p} (q : Bool) :
              (if p then decide p else q) = (decide p || q)
              source
              @[simp]
              theorem ite_else_decide_self (p : Prop) [h : Decidable p] {w : Decidable p} (q : Bool) :
              (if p then q else decide p) = (decide p && q)
              source
              @[simp]
              theorem ite_then_decide_not_self (p : Prop) [h : Decidable p] {w : Decidable p} (q : Bool) :
              (if p then !decide p else q) = (!decide p && q)
              source
              @[simp]
              theorem ite_else_decide_not_self (p : Prop) [h : Decidable p] {w : Decidable p} (q : Bool) :
              (if p then q else !decide p) = (!decide p || q)
              source
              @[simp]
              theorem dite_eq_left_iff {α : Sort u_1} {p : Prop} [Decidable p] {x : α} {y : ¬p → α} :
              (if h : p then x else y h) = x ↔ ∀ (h : ¬p), y h = x
              source
              @[simp]
              theorem dite_eq_right_iff {α : Sort u_1} {p : Prop} [Decidable p] {x : p → α} {y : α} :
              (if h : p then x h else y) = y ↔ ∀ (h : p), x h = y
              source
              @[simp]
              theorem left_eq_dite_iff {α : Sort u_1} {p : Prop} [Decidable p] {x : α} {y : ¬p → α} :
              (x = if h : p then x else y h) ↔ ∀ (h : ¬p), x = y h
              source
              @[simp]
              theorem right_eq_dite_iff {α : Sort u_1} {p : Prop} [Decidable p] {x : p → α} {y : α} :
              (y = if h : p then x h else y) ↔ ∀ (h : p), y = x h
              source
              @[simp]
              theorem dite_iff_left_iff {p : Prop} [Decidable p] {x : Prop} {y : ¬p → Prop} :
              ((if h : p then x else y h) ↔ x) ↔ ∀ (h : ¬p), y h ↔ x
              source
              @[simp]
              theorem dite_iff_right_iff {p : Prop} [Decidable p] {x : p → Prop} {y : Prop} :
              ((if h : p then x h else y) ↔ y) ↔ ∀ (h : p), x h ↔ y
              source
              @[simp]
              theorem left_iff_dite_iff {p : Prop} [Decidable p] {x : Prop} {y : ¬p → Prop} :
              (x ↔ if h : p then x else y h) ↔ ∀ (h : ¬p), x ↔ y h
              source
              @[simp]
              theorem right_iff_dite_iff {p : Prop} [Decidable p] {x : p → Prop} {y : Prop} :
              (y ↔ if h : p then x h else y) ↔ ∀ (h : p), y ↔ x h
              source
              @[simp]
              theorem ite_eq_left_iff {α : Sort u_1} {p : Prop} [Decidable p] {x y : α} :
              (if p then x else y) = x ↔ ¬p → y = x
              source
              @[simp]
              theorem ite_eq_right_iff {α : Sort u_1} {p : Prop} [Decidable p] {x y : α} :
              (if p then x else y) = y ↔ p → x = y
              source
              @[simp]
              theorem left_eq_ite_iff {α : Sort u_1} {p : Prop} [Decidable p] {x y : α} :
              (x = if p then x else y) ↔ ¬p → x = y
              source
              @[simp]
              theorem right_eq_ite_iff {α : Sort u_1} {p : Prop} [Decidable p] {x y : α} :
              (y = if p then x else y) ↔ p → y = x
              source
              @[simp]
              theorem ite_iff_left_iff {p : Prop} [Decidable p] {x y : Prop} :
              ((if p then x else y) ↔ x) ↔ ¬p → y = x
              source
              @[simp]
              theorem ite_iff_right_iff {p : Prop} [Decidable p] {x y : Prop} :
              ((if p then x else y) ↔ y) ↔ p → x = y
              source
              @[simp]
              theorem left_iff_ite_iff {p : Prop} [Decidable p] {x y : Prop} :
              (x ↔ if p then x else y) ↔ ¬p → x = y
              source
              @[simp]
              theorem right_iff_ite_iff {p : Prop} [Decidable p] {x y : Prop} :
              (y ↔ if p then x else y) ↔ p → y = x
              source
              @[simp]
              theorem dite_then_false {p : Prop} [Decidable p] {x : ¬p → Prop} :
              (if h : p then False else x h) ↔ ∃ (h : ¬p), x h
              source
              @[simp]
              theorem dite_else_false {p : Prop} [Decidable p] {x : p → Prop} :
              (if h : p then x h else False) ↔ ∃ (h : p), x h
              source
              @[simp]
              theorem dite_then_true {p : Prop} [Decidable p] {x : ¬p → Prop} :
              (if h : p then True else x h) ↔ ∀ (h : ¬p), x h
              source
              @[simp]
              theorem dite_else_true {p : Prop} [Decidable p] {x : p → Prop} :
              (if h : p then x h else True) ↔ ∀ (h : p), x h
              source
              @[simp]
              theorem Bool.ite_then_false {p : Prop} [Decidable p] {x : Bool} :
              (if p then false else x) = true ↔ ¬p ∧ x = true
              source
              @[simp]
              theorem Bool.ite_then_true_eq_false {p : Prop} [Decidable p] {x : Bool} :
              (if p then true else x) = false ↔ ¬p ∧ x = false
              source
              @[simp]
              theorem Bool.ite_else_false {p : Prop} [Decidable p] {x : Bool} :
              (if p then x else false) = true ↔ p ∧ x = true
              source
              @[simp]
              theorem Bool.ite_else_true_eq_false {p : Prop} [Decidable p] {x : Bool} :
              (if p then x else true) = false ↔ p ∧ x = false
              source
              @[simp]
              theorem Bool.ite_then_true {p : Prop} [Decidable p] {x : Bool} :
              (if p then true else x) = true ↔ p ∨ x = true
              source
              @[simp]
              theorem Bool.ite_then_false_eq_false {p : Prop} [Decidable p] {x : Bool} :
              (if p then false else x) = false ↔ p ∨ x = false
              source
              @[simp]
              theorem Bool.ite_else_true {p : Prop} [Decidable p] {x : Bool} :
              (if p then x else true) = true ↔ ¬p ∨ x = true
              source
              @[simp]
              theorem Bool.ite_else_false_eq_false {p : Prop} [Decidable p] {x : Bool} :
              (if p then x else false) = false ↔ ¬p ∨ x = false
              source
              @[simp]
              theorem Bool.dite_then_false {p : Prop} [Decidable p] {x : ¬p → Bool} :
              (if h : p then false else x h) = true ↔ ∃ (h : ¬p), x h = true
              source
              @[simp]
              theorem Bool.dite_then_true_eq_false {p : Prop} [Decidable p] {x : ¬p → Bool} :
              (if h : p then true else x h) = false ↔ ∃ (h : ¬p), x h = false
              source
              @[simp]
              theorem Bool.dite_else_false {p : Prop} [Decidable p] {x : p → Bool} :
              (if h : p then x h else false) = true ↔ ∃ (h : p), x h = true
              source
              @[simp]
              theorem Bool.dite_else_true_eq_false {p : Prop} [Decidable p] {x : p → Bool} :
              (if h : p then x h else true) = false ↔ ∃ (h : p), x h = false
              source
              @[simp]
              theorem Bool.dite_then_true {p : Prop} [Decidable p] {x : ¬p → Bool} :
              (if h : p then true else x h) = true ↔ ∀ (h : ¬p), x h = true
              source
              @[simp]
              theorem Bool.dite_then_false_eq_false {p : Prop} [Decidable p] {x : ¬p → Bool} :
              (if h : p then false else x h) = false ↔ ∀ (h : ¬p), x h = false
              source
              @[simp]
              theorem Bool.dite_else_true {p : Prop} [Decidable p] {x : p → Bool} :
              (if h : p then x h else true) = true ↔ ∀ (h : p), x h = true
              source
              @[simp]
              theorem Bool.dite_else_false_eq_false {p : Prop} [Decidable p] {x : p → Bool} :
              (if h : p then x h else false) = false ↔ ∀ (h : p), x h = false