## 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
@[deprecated Exists.nonempty (since := "2025-05-19")]
theorem nonempty_of_exists {α : Sort u} {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

Equations

- Decidable.or_not_self = 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.

Equations

- h.by_cases h₁ h₂ = if hp : p then h₁ hp else h₂ ⋯

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.

Equations

- h.by_cases' h₁ h₂ = if hq : q then h₂ hq else h₁ ⋯

Instances For

source
instance exists_prop_decidable {p : Prop} (P : p → Prop) [Decidable p] [(h : p) → Decidable (P h)] :
Decidable (∃ (h : p), P h)
Equations

- exists_prop_decidable P = if h : p then decidable_of_decidable_of_iff ⋯ else isFalse ⋯

source
instance forall_prop_decidable {p : Prop} (P : p → Prop) [Decidable p] [(h : p) → Decidable (P h)] :
Decidable (∀ (h : p), P h)
Equations

- forall_prop_decidable P = if h : p then decidable_of_decidable_of_iff ⋯ else isTrue ⋯

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
@[reducible, inline, deprecated Decidable.not_and_iff_not_or_not (since := "2025-03-18")]
abbrev Decidable.not_and_iff_or_not_not {a b : Prop} [Decidable a] :
¬(a ∧ b) ↔ ¬a ∨ ¬b
Equations

- @Decidable.not_and_iff_or_not_not = @Decidable.not_and_iff_not_or_not

Instances For

source
theorem Decidable.not_and_iff_not_or_not' {b a : Prop} [Decidable b] :
¬(a ∧ b) ↔ ¬a ∨ ¬b
source
@[reducible, inline, deprecated Decidable.not_and_iff_not_or_not' (since := "2025-03-18")]
abbrev Decidable.not_and_iff_or_not_not' {b a : Prop} [Decidable b] :
¬(a ∧ b) ↔ ¬a ∨ ¬b
Equations

- @Decidable.not_and_iff_or_not_not' = @Decidable.not_and_iff_not_or_not'

Instances For

source
theorem Decidable.or_iff_not_not_and_not {a b : Prop} [Decidable a] [Decidable b] :
a ∨ b ↔ ¬(¬a ∧ ¬b)
source
@[reducible, inline, deprecated Decidable.or_iff_not_not_and_not (since := "2025-03-18")]
abbrev Decidable.or_iff_not_and_not {a b : Prop} [Decidable a] [Decidable b] :
a ∨ b ↔ ¬(¬a ∧ ¬b)
Equations

- @Decidable.or_iff_not_and_not = @Decidable.or_iff_not_not_and_not

Instances For

source
theorem Decidable.and_iff_not_not_or_not {a b : Prop} [Decidable a] [Decidable b] :
a ∧ b ↔ ¬(¬a ∨ ¬b)
source
@[reducible, inline, deprecated Decidable.and_iff_not_not_or_not (since := "2025-03-18")]
abbrev Decidable.and_iff_not_or_not {a b : Prop} [Decidable a] [Decidable b] :
a ∧ b ↔ ¬(¬a ∨ ¬b)
Equations

- @Decidable.and_iff_not_or_not = @Decidable.and_iff_not_not_or_not

Instances For

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.

Equations

- decidable_of_iff a h = decidable_of_decidable_of_iff h

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.

Equations

- decidable_of_iff' b h = decidable_of_decidable_of_iff ⋯

Instances For

source
instance Decidable.predToBool {α : Sort u_1} (p : α → Prop) [DecidablePred p] :
CoeDep (α → Prop) p (α → Bool)
Equations

- Decidable.predToBool p = { coe := fun (b : α) => decide (p b) }

source
instance instDecidablePredComp {α✝ : Sort u_1} {p : α✝ → Prop} {α✝¹ : Sort u_2} {f : α✝¹ → α✝} [DecidablePred p] :
DecidablePred (p ∘ f)
Equations

- instDecidablePredComp x = inferInstanceAs (Decidable (p (f x)))

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

Equations

- decidable_of_bool true h = isTrue ⋯
- decidable_of_bool false h = isFalse ⋯

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