cast and equality

@[simp]

theorem eq_mp_eq_cast {α : Sort u_1} {β : Sort u_1} (h : α = β) : h.mp = cast h

@[simp]

theorem eq_mpr_eq_cast {α : Sort u_1} {β : Sort u_1} (h : α = β) : h.mpr = cast ⋯

@[simp]

theorem cast_cast {α : Sort u_1} {β : Sort u_1} {γ : Sort u_1} (ha : α = β) (hb : β = γ) (a : α) : cast hb (cast ha a) = cast ⋯ a

@[simp]

theorem eq_true_eq_id : Eq True = id

theorem proof_irrel_heq {p : Prop} {q : Prop} (hp : p) (hq : q) : HEq hp hq

not

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

and

theorem and_self_iff {a : Prop} : a ∧ a ↔ a

theorem and_not_self_iff (a : Prop) : a ∧ ¬a ↔ False

theorem not_and_self_iff (a : Prop) : ¬a ∧ a ↔ False

theorem And.imp {a : Prop} {c : Prop} {b : Prop} {d : Prop} (f : a → c) (g : b → d) (h : a ∧ b) : c ∧ d

theorem And.imp_left {a : Prop} {b : Prop} {c : Prop} (h : a → b) : a ∧ c → b ∧ c

theorem And.imp_right {a : Prop} {b : Prop} {c : Prop} (h : a → b) : c ∧ a → c ∧ b

theorem and_congr {a : Prop} {c : Prop} {b : Prop} {d : Prop} (h₁ : a ↔ c) (h₂ : b ↔ d) : a ∧ b ↔ c ∧ d

theorem and_congr_left' {a : Prop} {b : Prop} {c : Prop} (h : a ↔ b) : a ∧ c ↔ b ∧ c

theorem and_congr_right' {b : Prop} {c : Prop} {a : Prop} (h : b ↔ c) : a ∧ b ↔ a ∧ c

theorem not_and_of_not_left {a : Prop} (b : Prop) : ¬a → ¬(a ∧ b)

theorem not_and_of_not_right (a : Prop) {b : Prop} : ¬b → ¬(a ∧ b)

theorem and_congr_right_eq {a : Prop} {b : Prop} {c : Prop} (h : a → b = c) : (a ∧ b) = (a ∧ c)

theorem and_congr_left_eq {c : Prop} {a : Prop} {b : Prop} (h : c → a = b) : (a ∧ c) = (b ∧ c)

theorem and_left_comm {a : Prop} {b : Prop} {c : Prop} : a ∧ b ∧ c ↔ b ∧ a ∧ c

theorem and_right_comm {a : Prop} {b : Prop} {c : Prop} : (a ∧ b) ∧ c ↔ (a ∧ c) ∧ b

theorem and_rotate {a : Prop} {b : Prop} {c : Prop} : a ∧ b ∧ c ↔ b ∧ c ∧ a

theorem and_and_and_comm {a : Prop} {b : Prop} {c : Prop} {d : Prop} : (a ∧ b) ∧ c ∧ d ↔ (a ∧ c) ∧ b ∧ d

theorem and_and_left {a : Prop} {b : Prop} {c : Prop} : a ∧ b ∧ c ↔ (a ∧ b) ∧ a ∧ c

theorem and_and_right {a : Prop} {b : Prop} {c : Prop} : (a ∧ b) ∧ c ↔ (a ∧ c) ∧ b ∧ c

theorem and_iff_left {b : Prop} {a : Prop} (hb : b) : a ∧ b ↔ a

theorem and_iff_right {a : Prop} {b : Prop} (ha : a) : a ∧ b ↔ b

or

theorem or_self_iff {a : Prop} : a ∨ a ↔ a

theorem not_or_intro {a : Prop} {b : Prop} (ha : ¬a) (hb : ¬b) : ¬(a ∨ b)

theorem or_congr {a : Prop} {c : Prop} {b : Prop} {d : Prop} (h₁ : a ↔ c) (h₂ : b ↔ d) : a ∨ b ↔ c ∨ d

theorem or_congr_left {a : Prop} {b : Prop} {c : Prop} (h : a ↔ b) : a ∨ c ↔ b ∨ c

theorem or_congr_right {b : Prop} {c : Prop} {a : Prop} (h : b ↔ c) : a ∨ b ↔ a ∨ c

theorem or_left_comm {a : Prop} {b : Prop} {c : Prop} : a ∨ b ∨ c ↔ b ∨ a ∨ c

theorem or_right_comm {a : Prop} {b : Prop} {c : Prop} : (a ∨ b) ∨ c ↔ (a ∨ c) ∨ b

theorem or_or_or_comm {a : Prop} {b : Prop} {c : Prop} {d : Prop} : (a ∨ b) ∨ c ∨ d ↔ (a ∨ c) ∨ b ∨ d

theorem or_or_distrib_left {a : Prop} {b : Prop} {c : Prop} : a ∨ b ∨ c ↔ (a ∨ b) ∨ a ∨ c

theorem or_or_distrib_right {a : Prop} {b : Prop} {c : Prop} : (a ∨ b) ∨ c ↔ (a ∨ c) ∨ b ∨ c

theorem or_rotate {a : Prop} {b : Prop} {c : Prop} : a ∨ b ∨ c ↔ b ∨ c ∨ a

theorem or_iff_left {b : Prop} {a : Prop} (hb : ¬b) : a ∨ b ↔ a

theorem or_iff_right {a : Prop} {b : Prop} (ha : ¬a) : a ∨ b ↔ b

distributivity

theorem not_imp_of_and_not {a : Prop} {b : Prop} : a ∧ ¬b → ¬(a → b)

theorem imp_and {b : Prop} {c : Prop} {α : Sort u_1} : α → b ∧ c ↔ (α → b) ∧ (α → c)

theorem not_and' {a : Prop} {b : Prop} : ¬(a ∧ b) ↔ b → ¬a

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

∧ distributes over ∨ (on the left).

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

∧ distributes over ∨ (on the right).

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

∨ distributes over ∧ (on the left).

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

∨ distributes over ∧ (on the right).

theorem or_imp {a : Prop} {b : Prop} {c : Prop} : a ∨ b → c ↔ (a → c) ∧ (b → c)

@[simp]

theorem not_or {p : Prop} {q : Prop} : ¬(p ∨ q) ↔ ¬p ∧ ¬q

theorem not_and_of_not_or_not {a : Prop} {b : Prop} (h : ¬a ∨ ¬b) : ¬(a ∧ b)

not equal

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

Ite

@[simp]

theorem if_false_left {p : Prop} {q : Prop} [h : Decidable p] : (if p then False else q) ↔ ¬p ∧ q

@[simp]

theorem if_false_right {p : Prop} {q : Prop} [h : Decidable p] : (if p then q else False) ↔ p ∧ q

@[simp]

theorem if_true_left {p : Prop} {q : Prop} [h : Decidable p] : (if p then True else q) ↔ ¬p → q

@[simp]

theorem if_true_right {p : Prop} {q : Prop} [h : Decidable p] : (if p then q else True) ↔ p → q

@[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.

@[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.

@[simp]

theorem ite_then_self {p : Prop} {q : Prop} [h : Decidable p] : (if p then p else q) ↔ ¬p → q

@[simp]

theorem ite_else_self {p : Prop} {q : Prop} [h : Decidable p] : (if p then q else p) ↔ p ∧ q

@[simp]

theorem ite_then_not_self {p : Prop} [Decidable p] {q : Prop} : (if p then ¬p else q) ↔ ¬p ∧ q

@[simp]

theorem ite_else_not_self {p : Prop} [Decidable p] {q : Prop} : (if p then q else ¬p) ↔ p → q

@[deprecated ite_then_self]

theorem ite_true_same {p : Prop} {q : Prop} [Decidable p] : (if p then p else q) ↔ ¬p → q

@[deprecated ite_else_self]

theorem ite_false_same {p : Prop} {q : Prop} [Decidable p] : (if p then q else p) ↔ p ∧ q

@[simp]

theorem ite_eq_ite {α : Sort u_1} (p : Prop) {h : Decidable p} {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.

@[simp]

theorem ite_iff_ite (p : Prop) {h : Decidable p} {h' : Decidable p} (x : Prop) (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

theorem forall_imp {α : Sort u_1} {p : α → Prop} {q : α → Prop} (h : ∀ (a : α), p a → q a) : (∀ (a : α), p a) → ∀ (a : α), q a

@[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.

theorem Exists.imp {α : Sort u_1} {p : α → Prop} {q : α → Prop} (h : ∀ (a : α), p a → q a) : (∃ (a : α), p a) → ∃ (a : α), q a

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

theorem exists_imp {α : Sort u_1} {p : α → Prop} {b : Prop} : (∃ (x : α), p x) → b ↔ ∀ (x : α), p x → b

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

@[simp]

theorem exists_const {b : Prop} (α : Sort u_1) [i : Nonempty α] : (∃ (x : α), b) ↔ b

theorem exists_prop_congr {p : Prop} {p' : Prop} {q : p → Prop} {q' : p → Prop} (hq : ∀ (h : p), q h ↔ q' h) (hp : p ↔ p') : Exists q ↔ ∃ (h : p'), q' ⋯

theorem exists_prop_of_true {p : Prop} {q : p → Prop} (h : p) : (∃ (h' : p), q h') ↔ q h

@[simp]

theorem exists_true_left {p : True → Prop} : Exists p ↔ p True.intro

theorem forall_congr' {α : Sort u_1} {p : α → Prop} {q : α → Prop} (h : ∀ (a : α), p a ↔ q a) : (∀ (a : α), p a) ↔ ∀ (a : α), q a

theorem exists_congr {α : Sort u_1} {p : α → Prop} {q : α → Prop} (h : ∀ (a : α), p a ↔ q a) : (∃ (a : α), p a) ↔ ∃ (a : α), q a

theorem forall₂_congr {α : Sort u_1} {β : α → Sort u_2} {p : (a : α) → β a → Prop} {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

theorem exists₂_congr {α : Sort u_1} {β : α → Sort u_2} {p : (a : α) → β a → Prop} {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

theorem forall₃_congr {α : Sort u_1} {β : α → Sort u_2} {γ : (a : α) → β a → Sort u_3} {p : (a : α) → (b : β a) → γ a b → Prop} {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

theorem exists₃_congr {α : Sort u_1} {β : α → Sort u_2} {γ : (a : α) → β a → Sort u_3} {p : (a : α) → (b : β a) → γ a b → Prop} {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

theorem forall₄_congr {α : Sort u_1} {β : α → Sort u_2} {γ : (a : α) → β a → Sort u_3} {δ : (a : α) → (b : β a) → γ a b → Sort u_4} {p : (a : α) → (b : β a) → (c : γ a b) → δ a b c → Prop} {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

theorem exists₄_congr {α : Sort u_1} {β : α → Sort u_2} {γ : (a : α) → β a → Sort u_3} {δ : (a : α) → (b : β a) → γ a b → Sort u_4} {p : (a : α) → (b : β a) → (c : γ a b) → δ a b c → Prop} {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

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 : (a : α) → (b : β a) → (c : γ a b) → (d : δ a b c) → ε a b c d → Prop} {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

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 : (a : α) → (b : β a) → (c : γ a b) → (d : δ a b c) → ε a b c d → Prop} {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

@[simp]

theorem not_exists {α : Sort u_1} {p : α → Prop} : (¬∃ (x : α), p x) ↔ ∀ (x : α), ¬p x

theorem forall_not_of_not_exists {α : Sort u_1} {p : α → Prop} (h : ¬∃ (x : α), p x) (x : α) : ¬p x

theorem not_exists_of_forall_not {α : Sort u_1} {p : α → Prop} (h : ∀ (x : α), ¬p x) : ¬∃ (x : α), p x

theorem forall_and {α : Sort u_1} {p : α → Prop} {q : α → Prop} : (∀ (x : α), p x ∧ q x) ↔ (∀ (x : α), p x) ∧ ∀ (x : α), q x

theorem exists_or {α : Sort u_1} {p : α → Prop} {q : α → Prop} : (∃ (x : α), p x ∨ q x) ↔ (∃ (x : α), p x) ∨ ∃ (x : α), q x

@[simp]

theorem exists_false {α : Sort u_1} : ¬∃ (_a : α), False

@[simp]

theorem forall_const {b : Prop} (α : Sort u_1) [i : Nonempty α] : α → b ↔ b

theorem Exists.nonempty {α : Sort u_1} {p : α → Prop} : (∃ (x : α), p x) → Nonempty α

theorem not_forall_of_exists_not {α : Sort u_1} {p : α → Prop} : (∃ (x : α), ¬p x) → ¬∀ (x : α), p x

@[simp]

theorem forall_eq {α : Sort u_1} {p : α → Prop} {a' : α} : (∀ (a : α), a = a' → p a) ↔ p a'

@[simp]

theorem forall_eq' {α : Sort u_1} {p : α → Prop} {a' : α} : (∀ (a : α), a' = a → p a) ↔ p a'

@[simp]

theorem exists_eq : ∀ {α : Sort u_1} {a' : α}, ∃ (a : α), a = a'

@[simp]

theorem exists_eq' : ∀ {α : Sort u_1} {a' : α}, ∃ (a : α), a' = a

@[simp]

theorem exists_eq_left {α : Sort u_1} {p : α → Prop} {a' : α} : (∃ (a : α), a = a' ∧ p a) ↔ p a'

@[simp]

theorem exists_eq_right {α : Sort u_1} {p : α → Prop} {a' : α} : (∃ (a : α), p a ∧ a = a') ↔ p a'

@[simp]

theorem exists_and_left {α : Sort u_1} {p : α → Prop} {b : Prop} : (∃ (x : α), b ∧ p x) ↔ b ∧ ∃ (x : α), p x

@[simp]

theorem exists_and_right {α : Sort u_1} {p : α → Prop} {b : Prop} : (∃ (x : α), p x ∧ b) ↔ (∃ (x : α), p x) ∧ b

@[simp]

theorem exists_eq_left' {α : Sort u_1} {p : α → Prop} {a' : α} : (∃ (a : α), a' = a ∧ p a) ↔ p a'

@[simp]

theorem exists_eq_right' {α : Sort u_1} {p : α → Prop} {a' : α} : (∃ (a : α), p a ∧ a' = a) ↔ p a'

@[simp]

theorem forall_eq_or_imp {α : Sort u_1} {p : α → Prop} {q : α → Prop} {a' : α} : (∀ (a : α), a = a' ∨ q a → p a) ↔ p a' ∧ ∀ (a : α), q a → p a

@[simp]

theorem exists_eq_or_imp {α : Sort u_1} {p : α → Prop} {q : α → Prop} {a' : α} : (∃ (a : α), (a = a' ∨ q a) ∧ p a) ↔ p a' ∨ ∃ (a : α), q a ∧ p a

@[simp]

theorem exists_eq_right_right {α : Sort u_1} {p : α → Prop} {q : α → Prop} {a' : α} : (∃ (a : α), p a ∧ q a ∧ a = a') ↔ p a' ∧ q a'

@[simp]

theorem exists_eq_right_right' {α : Sort u_1} {p : α → Prop} {q : α → Prop} {a' : α} : (∃ (a : α), p a ∧ q a ∧ a' = a) ↔ p a' ∧ q a'

@[simp]

theorem exists_or_eq_left {α : Sort u_1} (y : α) (p : α → Prop) : ∃ (x : α), x = y ∨ p x

@[simp]

theorem exists_or_eq_right {α : Sort u_1} (y : α) (p : α → Prop) : ∃ (x : α), p x ∨ x = y

@[simp]

theorem exists_or_eq_left' {α : Sort u_1} (y : α) (p : α → Prop) : ∃ (x : α), y = x ∨ p x

@[simp]

theorem exists_or_eq_right' {α : Sort u_1} (y : α) (p : α → Prop) : ∃ (x : α), p x ∨ y = x

theorem exists_prop' {α : Sort u_1} {p : Prop} : (∃ (x : α), p) ↔ Nonempty α ∧ p

@[simp]

theorem exists_prop {b : Prop} {a : Prop} : (∃ (_h : a), b) ↔ a ∧ b

@[simp]

theorem exists_apply_eq_apply {α : Sort u_2} {β : Sort u_1} (f : α → β) (a' : α) : ∃ (a : α), f a = f a'

theorem forall_prop_of_true {p : Prop} {q : p → Prop} (h : p) : (∀ (h' : p), q h') ↔ q h

theorem forall_comm {α : Sort u_2} {β : Sort u_1} {p : α → β → Prop} : (∀ (a : α) (b : β), p a b) ↔ ∀ (b : β) (a : α), p a b

theorem exists_comm {α : Sort u_2} {β : Sort u_1} {p : α → β → Prop} : (∃ (a : α), ∃ (b : β), p a b) ↔ ∃ (b : β), ∃ (a : α), p a b

@[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)

@[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)

@[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)

theorem forall_prop_of_false {p : Prop} {q : p → Prop} (hn : ¬p) : (∀ (h' : p), q h') ↔ True

membership

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

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

@[simp]

theorem nonempty_prop {p : Prop} : Nonempty p ↔ p

decidable

@[simp]

theorem Decidable.not_not {p : Prop} [Decidable p] : ¬¬p ↔ p

@[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

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

Excluded middle commuted. Added as alias for Decidable.em

theorem Decidable.by_contra {p : Prop} [Decidable p] : (¬p → False) → p

def Or.by_cases {p : Prop} {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₂ ⋯

def Or.by_cases' {q : Prop} {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₁ ⋯

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 ⋯

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 ⋯

theorem decide_eq_true_iff {p : Prop} [Decidable p] : decide p = true ↔ p

@[simp]

theorem decide_eq_decide {p : Prop} {q : Prop} : ∀ {x : Decidable p} {x_1 : Decidable q}, decide p = decide q ↔ (p ↔ q)

theorem Decidable.of_not_imp {a : Prop} {b : Prop} [Decidable a] (h : ¬(a → b)) : a

theorem Decidable.not_imp_symm {a : Prop} {b : Prop} [Decidable a] (h : ¬a → b) (hb : ¬b) : a

theorem Decidable.not_imp_comm {a : Prop} {b : Prop} [Decidable a] [Decidable b] : ¬a → b ↔ ¬b → a

theorem Decidable.not_imp_self {a : Prop} [Decidable a] : ¬a → a ↔ a

theorem Decidable.or_iff_not_imp_left {a : Prop} {b : Prop} [Decidable a] : a ∨ b ↔ ¬a → b

theorem Decidable.or_iff_not_imp_right {b : Prop} {a : Prop} [Decidable b] : a ∨ b ↔ ¬b → a

theorem Decidable.not_imp_not {a : Prop} {b : Prop} [Decidable a] : ¬a → ¬b ↔ b → a

theorem Decidable.not_or_of_imp {a : Prop} {b : Prop} [Decidable a] (h : a → b) : ¬a ∨ b

theorem Decidable.imp_iff_not_or {a : Prop} {b : Prop} [Decidable a] : a → b ↔ ¬a ∨ b

theorem Decidable.imp_iff_or_not {b : Prop} {a : Prop} [Decidable b] : b → a ↔ a ∨ ¬b

theorem Decidable.imp_or {a : Prop} {b : Prop} {c : Prop} [Decidable a] : a → b ∨ c ↔ (a → b) ∨ (a → c)

theorem Decidable.imp_or' {b : Prop} {a : Sort u_1} {c : Prop} [Decidable b] : a → b ∨ c ↔ (a → b) ∨ (a → c)

theorem Decidable.not_imp_iff_and_not {a : Prop} {b : Prop} [Decidable a] : ¬(a → b) ↔ a ∧ ¬b

theorem Decidable.peirce (a : Prop) (b : Prop) [Decidable a] : ((a → b) → a) → a

theorem peirce' {a : Prop} (H : ∀ (b : Prop), (a → b) → a) : a

theorem Decidable.not_iff_not {a : Prop} {b : Prop} [Decidable a] [Decidable b] : (¬a ↔ ¬b) ↔ (a ↔ b)

theorem Decidable.not_iff_comm {a : Prop} {b : Prop} [Decidable a] [Decidable b] : (¬a ↔ b) ↔ (¬b ↔ a)

theorem Decidable.not_iff {b : Prop} {a : Prop} [Decidable b] : ¬(a ↔ b) ↔ (¬a ↔ b)

theorem Decidable.iff_not_comm {a : Prop} {b : Prop} [Decidable a] [Decidable b] : (a ↔ ¬b) ↔ (b ↔ ¬a)

theorem Decidable.iff_iff_and_or_not_and_not {a : Prop} {b : Prop} [Decidable b] : (a ↔ b) ↔ a ∧ b ∨ ¬a ∧ ¬b

theorem Decidable.iff_iff_not_or_and_or_not {a : Prop} {b : Prop} [Decidable a] [Decidable b] : (a ↔ b) ↔ (¬a ∨ b) ∧ (a ∨ ¬b)

theorem Decidable.not_and_not_right {b : Prop} {a : Prop} [Decidable b] : ¬(a ∧ ¬b) ↔ a → b

theorem Decidable.not_and_iff_or_not_not {a : Prop} {b : Prop} [Decidable a] : ¬(a ∧ b) ↔ ¬a ∨ ¬b

theorem Decidable.not_and_iff_or_not_not' {b : Prop} {a : Prop} [Decidable b] : ¬(a ∧ b) ↔ ¬a ∨ ¬b

theorem Decidable.or_iff_not_and_not {a : Prop} {b : Prop} [Decidable a] [Decidable b] : a ∨ b ↔ ¬(¬a ∧ ¬b)

theorem Decidable.and_iff_not_or_not {a : Prop} {b : Prop} [Decidable a] [Decidable b] : a ∧ b ↔ ¬(¬a ∨ ¬b)

theorem Decidable.imp_iff_right_iff {a : Prop} {b : Prop} [Decidable a] : (a → b ↔ b) ↔ a ∨ b

theorem Decidable.imp_iff_left_iff {a : Prop} {b : Prop} [Decidable a] : (b ↔ a → b) ↔ a ∨ b

theorem Decidable.and_or_imp {a : Prop} {b : Prop} {c : Prop} [Decidable a] : a ∧ b ∨ (a → c) ↔ a → b ∨ c

theorem Decidable.or_congr_left' {c : Prop} {a : Prop} {b : Prop} [Decidable c] (h : ¬c → (a ↔ b)) : a ∨ c ↔ b ∨ c

theorem Decidable.or_congr_right' {a : Prop} {b : Prop} {c : Prop} [Decidable a] (h : ¬a → (b ↔ c)) : a ∨ b ↔ a ∨ c

@[simp]

theorem Decidable.iff_congr_left {P : Prop} {Q : Prop} {R : Prop} [Decidable P] [Decidable Q] [Decidable R] : ((P ↔ R) ↔ (Q ↔ R)) ↔ (P ↔ Q)

@[simp]

theorem Decidable.iff_congr_right {P : Prop} {Q : Prop} {R : Prop} [Decidable P] [Decidable Q] [Decidable R] : ((P ↔ Q) ↔ (P ↔ R)) ↔ (Q ↔ R)

@[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

@[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 ⋯

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

Equations

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

instance instDecidablePredComp : {α : Sort u_1} → {p : α → Prop} → {α_1 : Sort u_2} → {f : α_1 → α} → [inst : DecidablePred p] → DecidablePred (p ∘ f)

Equations

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

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 ⋯

theorem Decidable.not_forall {α : Sort u_1} {p : α → Prop} [Decidable (∃ (x : α), ¬p x)] [(x : α) → Decidable (p x)] : (¬∀ (x : α), p x) ↔ ∃ (x : α), ¬p x

theorem Decidable.not_forall_not {α : Sort u_1} {p : α → Prop} [Decidable (∃ (x : α), p x)] : (¬∀ (x : α), ¬p x) ↔ ∃ (x : α), p x

theorem Decidable.not_exists_not {α : Sort u_1} {p : α → Prop} [(x : α) → Decidable (p x)] : (¬∃ (x : α), ¬p x) ↔ ∀ (x : α), p x

@[simp]

theorem decide_implies (u : Prop) (v : Prop) [duv : Decidable (u → v)] [du : Decidable u] {dv : u → Decidable v} : decide (u → v) = if h : u then decide v else true

@[simp]

theorem decide_ite (u : Prop) [du : Decidable u] (p : Prop) (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

@[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)

@[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)

@[deprecated ite_then_decide_self]

theorem ite_true_decide_same (p : Prop) [Decidable p] (b : Bool) : (if p then decide p else b) = (decide p || b)

@[deprecated ite_false_decide_same]

theorem ite_false_decide_same (p : Prop) [Decidable p] (b : Bool) : (if p then b else decide p) = (decide p && b)

@[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)

@[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)

@[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

@[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

@[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

@[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

@[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

@[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

@[simp]

theorem ite_iff_left_iff {p : Prop} [Decidable p] {x : Prop} {y : Prop} : ((if p then x else y) ↔ x) ↔ ¬p → y = x

@[simp]

theorem ite_iff_right_iff {p : Prop} [Decidable p] {x : Prop} {y : Prop} : ((if p then x else y) ↔ y) ↔ p → x = y

@[simp]

theorem dite_then_false {p : Prop} [Decidable p] {x : ¬p → Prop} : (if h : p then False else x h) ↔ ∃ (h : ¬p), x h

@[simp]

theorem dite_else_false {p : Prop} [Decidable p] {x : p → Prop} : (if h : p then x h else False) ↔ ∃ (h : p), x h

@[simp]

theorem dite_then_true {p : Prop} [Decidable p] {x : ¬p → Prop} : (if h : p then True else x h) ↔ ∀ (h : ¬p), x h

@[simp]

theorem dite_else_true {p : Prop} [Decidable p] {x : p → Prop} : (if h : p then x h else True) ↔ ∀ (h : p), x h