# Documentation

## Std.Logic

instance instDecidablePredCompProp {α : Sort u_1} {β : Sort u_2} {p : βProp} {f : αβ} [] :
Equations
theorem Function.comp_def {α : Sort u_1} {β : Sort u_2} {δ : Sort u_3} (f : βδ) (g : αβ) :
f g = fun (x : α) => f (g x)

## not #

theorem Not.intro {a : Prop} (h : aFalse) :
def Not.elim {a : Prop} {α : Sort u_1} (H1 : ¬a) (H2 : a) :
α

Ex falso for negation. From ¬a and a anything follows. This is the same as absurd with the arguments flipped, but it is in the not namespace so that projection notation can be used.

Equations
Instances For
theorem Not.imp {a : Prop} {b : Prop} (H2 : ¬b) (H1 : ab) :
theorem not_congr {a : Prop} {b : Prop} (h : a b) :
theorem not_not_of_not_imp {a : Prop} {b : Prop} :
¬(ab)¬¬a
theorem not_of_not_imp {b : Prop} {a : Prop} :
¬(ab)¬b
@[simp]
theorem imp_not_self {a : Prop} :
a¬a ¬a

## iff #

instance instTransPropIff :
Equations
theorem iff_def {a : Prop} {b : Prop} :
(a b) (ab) (ba)
theorem iff_def' {a : Prop} {b : Prop} :
(a b) (ba) (ab)
def Iff.elim {a : Prop} {b : Prop} {α : Sort u_1} (f : (ab)(ba)α) (h : a b) :
α

Non-dependent eliminator for Iff.

Equations
Instances For
theorem Eq.to_iff {a : Prop} {b : Prop} :
a = b(a b)
theorem iff_of_eq {a : Prop} {b : Prop} :
a = b(a b)
theorem neq_of_not_iff {a : Prop} {b : Prop} :
¬(a b)a b
theorem iff_iff_eq {a : Prop} {b : Prop} :
(a b) a = b
@[simp]
theorem eq_iff_iff {p : Prop} {q : Prop} :
p = q (p q)
theorem of_iff_true {a : Prop} (h : ) :
a
theorem not_of_iff_false {a : Prop} :
()¬a
theorem iff_of_true {a : Prop} {b : Prop} (ha : a) (hb : b) :
a b
theorem iff_of_false {a : Prop} {b : Prop} (ha : ¬a) (hb : ¬b) :
a b
theorem iff_true_left {a : Prop} {b : Prop} (ha : a) :
(a b) b
theorem iff_true_right {a : Prop} {b : Prop} (ha : a) :
(b a) b
theorem iff_false_left {a : Prop} {b : Prop} (ha : ¬a) :
(a b) ¬b
theorem iff_false_right {a : Prop} {b : Prop} (ha : ¬a) :
(b a) ¬b
theorem iff_true_intro {a : Prop} (h : a) :
theorem iff_false_intro {a : Prop} (h : ¬a) :
theorem not_iff_false_intro {a : Prop} (h : a) :
theorem iff_congr {a : Prop} {c : Prop} {b : Prop} {d : Prop} (h₁ : a c) (h₂ : b d) :
(a b) (c d)
theorem not_true :
theorem ne_self_iff_false {α : Sort u_1} (a : α) :
theorem eq_self_iff_true {α : Sort u_1} (a : α) :
a = a True
theorem heq_self_iff_true {α : Sort u_1} (a : α) :
theorem iff_not_self {a : Prop} :
¬(a ¬a)
@[simp]
theorem not_iff_self {a : Prop} :
¬(¬a a)
theorem eq_comm {α : Sort u_1} {a : α} {b : α} :
a = b b = a

## implies #

theorem imp_intro {α : Prop} {β : Prop} (h : α) :
βα
theorem imp_imp_imp {a : Prop} {b : Prop} {c : Prop} {d : Prop} (h₀ : ca) (h₁ : bd) :
(ab)cd
theorem imp_iff_right {b : Prop} {a : Prop} (ha : a) :
ab b
theorem imp_true_iff (α : Sort u) :
αTrue True
theorem false_imp_iff (a : Prop) :
Falsea True
theorem true_imp_iff (α : Prop) :
Trueα α
@[simp]
theorem imp_self {a : Prop} :
aa True
theorem imp_false {a : Prop} :
aFalse ¬a
theorem imp.swap {a : Sort u_1} {b : Sort u_2} {c : Prop} :
abc bac
theorem imp_not_comm {a : Prop} {b : Prop} :
a¬b b¬a
theorem imp_congr_left {a : Prop} {b : Prop} {c : Prop} (h : a b) :
ac bc
theorem imp_congr_right {a : Sort u_1} {b : Prop} {c : Prop} (h : a(b c)) :
ab ac
theorem imp_congr_ctx {a : Prop} {c : Prop} {b : Prop} {d : Prop} (h₁ : a c) (h₂ : c(b d)) :
ab cd
theorem imp_congr {a : Prop} {c : Prop} {b : Prop} {d : Prop} (h₁ : a c) (h₂ : b d) :
ab cd
theorem imp_iff_not {b : Prop} {a : Prop} (hb : ¬b) :
ab ¬a

## and #

@[inline, reducible]
abbrev And.elim {a : Prop} {b : Prop} {α : Sort u_1} (f : abα) (h : a b) :
α

Non-dependent eliminator for And.

Equations
Instances For
theorem and_self_iff {a : Prop} :
a a a
theorem And.symm {a : Prop} {b : Prop} :
a bb a
theorem And.imp {a : Prop} {c : Prop} {b : Prop} {d : Prop} (f : ac) (g : bd) (h : a b) :
c d
theorem And.imp_left {a : Prop} {b : Prop} {c : Prop} (h : ab) :
a cb c
theorem And.imp_right {a : Prop} {b : Prop} {c : Prop} (h : ab) :
c ac b
theorem and_congr {a : Prop} {c : Prop} {b : Prop} {d : Prop} (h₁ : a c) (h₂ : b d) :
a b c d
theorem and_comm {a : Prop} {b : Prop} :
a b b a
theorem and_congr_right {a : Prop} {b : Prop} {c : Prop} (h : a(b c)) :
a b a c
theorem and_congr_left {c : Prop} {a : Prop} {b : Prop} (h : c(a b)) :
a c b c
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 and_congr_right_eq {a : Prop} {b : Prop} {c : Prop} (h : ab = c) :
(a b) = (a c)
theorem and_congr_left_eq {c : Prop} {a : Prop} {b : Prop} (h : ca = b) :
(a c) = (b c)
theorem and_assoc {a : Prop} {b : Prop} {c : Prop} :
(a b) c a 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_of_imp {a : Prop} {b : Prop} (h : ab) :
a b a
theorem and_iff_right_of_imp {b : Prop} {a : Prop} (h : ba) :
a b b
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
@[simp]
theorem and_iff_left_iff_imp {a : Prop} {b : Prop} :
(a b a) ab
@[simp]
theorem and_iff_right_iff_imp {a : Prop} {b : Prop} :
(a b b) ba
@[simp]
theorem iff_self_and {p : Prop} {q : Prop} :
(p p q) pq
@[simp]
theorem iff_and_self {p : Prop} {q : Prop} :
(p q p) pq
@[simp]
theorem and_congr_right_iff {a : Prop} {b : Prop} {c : Prop} :
(a b a c) a(b c)
@[simp]
theorem and_congr_left_iff {a : Prop} {c : Prop} {b : Prop} :
(a c b c) c(a b)
@[simp]
theorem and_self_left {a : Prop} {b : Prop} :
a a b a b
@[simp]
theorem and_self_right {a : Prop} {b : Prop} :
(a b) b a b
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)
@[simp]
theorem and_not_self {a : Prop} :
¬(a ¬a)
@[simp]
theorem not_and_self {a : Prop} :
¬(¬a a)

## or #

theorem not_not_em (a : Prop) :
¬¬(a ¬a)
theorem or_self_iff {a : Prop} :
a a a
theorem Or.symm {a : Prop} {b : Prop} :
a bb a
theorem Or.imp {a : Prop} {c : Prop} {b : Prop} {d : Prop} (f : ac) (g : bd) (h : a b) :
c d
theorem Or.imp_left {a : Prop} {b : Prop} {c : Prop} (f : ab) :
a cb c
theorem Or.imp_right {b : Prop} {c : Prop} {a : Prop} (f : bc) :
a ba c
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.comm {a : Prop} {b : Prop} :
a b b a
theorem or_comm {a : Prop} {b : Prop} :
a b b a
theorem or_assoc {a : Prop} {b : Prop} {c : Prop} :
(a b) c a b c
theorem Or.resolve_left {a : Prop} {b : Prop} (h : a b) (na : ¬a) :
b
theorem Or.neg_resolve_left {a : Prop} {b : Prop} (h : ¬a b) (ha : a) :
b
theorem Or.resolve_right {a : Prop} {b : Prop} (h : a b) (nb : ¬b) :
a
theorem Or.neg_resolve_right {a : Prop} {b : Prop} (h : a ¬b) (nb : b) :
a
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_right_of_imp {a : Prop} {b : Prop} (ha : ab) :
a b b
theorem or_iff_left_of_imp {b : Prop} {a : Prop} (hb : ba) :
a b a
theorem not_or_intro {a : Prop} {b : Prop} (ha : ¬a) (hb : ¬b) :
¬(a b)
@[simp]
theorem or_iff_left_iff_imp {a : Prop} {b : Prop} :
(a b a) ba
@[simp]
theorem or_iff_right_iff_imp {a : Prop} {b : Prop} :
(a b b) ab
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¬(ab)
theorem imp_and {b : Prop} {c : Prop} {α : Sort u_1} :
αb c (αb) (αc)
@[simp]
theorem and_imp {a : Prop} {b : Prop} {c : Prop} :
a bc abc
@[simp]
theorem not_and {a : Prop} {b : Prop} :
¬(a b) a¬b
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 bc (ac) (bc)
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)
@[simp]
theorem or_self_left {a : Prop} {b : Prop} :
a a b a b
@[simp]
theorem or_self_right {a : Prop} {b : Prop} :
(a b) b a b

## exists and forall #

theorem forall_imp {α : Sort u_1} {p : αProp} {q : αProp} (h : ∀ (a : α), p aq 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 (_ : ∃ (x : α), p x)
theorem Exists.imp {α : Sort u_1} {p : αProp} {q : αProp} (h : ∀ (a : α), p aq a) :
(∃ (a : α), p a)∃ (a : α), q a
theorem Exists.imp' {α : Sort u_2} {p : αProp} {β : Sort u_1} {q : βProp} (f : αβ) (hpq : ∀ (a : α), p aq (f a)) :
(∃ (a : α), p a)∃ (b : β), q b
theorem exists_imp {α : Sort u_1} {p : αProp} {b : Prop} :
(∃ (x : α), p x)b ∀ (x : α), p xb
@[simp]
theorem exists_const {b : Prop} (α : Sort u_1) [i : ] :
(∃ (x : α), b) b
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 : α) → β aProp} {q : (a : α) → β aProp} (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 : α) → β aProp} {q : (a : α) → β aProp} (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 : α) → β aSort u_3} {p : (a : α) → (b : β a) → γ a bProp} {q : (a : α) → (b : β a) → γ a bProp} (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 : α) → β aSort u_3} {p : (a : α) → (b : β a) → γ a bProp} {q : (a : α) → (b : β a) → γ a bProp} (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 : α) → β aSort u_3} {δ : (a : α) → (b : β a) → γ a bSort u_4} {p : (a : α) → (b : β a) → (c : γ a b) → δ a b cProp} {q : (a : α) → (b : β a) → (c : γ a b) → δ a b cProp} (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 : α) → β aSort u_3} {δ : (a : α) → (b : β a) → γ a bSort u_4} {p : (a : α) → (b : β a) → (c : γ a b) → δ a b cProp} {q : (a : α) → (b : β a) → (c : γ a b) → δ a b cProp} (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 : α) → β aSort u_3} {δ : (a : α) → (b : β a) → γ a bSort u_4} {ε : (a : α) → (b : β a) → (c : γ a b) → δ a b cSort u_5} {p : (a : α) → (b : β a) → (c : γ a b) → (d : δ a b c) → ε a b c dProp} {q : (a : α) → (b : β a) → (c : γ a b) → (d : δ a b c) → ε a b c dProp} (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 : α) → β aSort u_3} {δ : (a : α) → (b : β a) → γ a bSort u_4} {ε : (a : α) → (b : β a) → (c : γ a b) → δ a b cSort u_5} {p : (a : α) → (b : β a) → (c : γ a b) → (d : δ a b c) → ε a b c dProp} {q : (a : α) → (b : β a) → (c : γ a b) → (d : δ a b c) → ε a b c dProp} (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} :
(¬∃ (x : α), p x)∀ (x : α), ¬p x

Alias of the forward direction of not_exists.

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

Alias of the reverse direction of not_exists.

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 : ] :
αb b
theorem Exists.nonempty {α : Sort u_1} {p : αProp} :
(∃ (x : α), p x)
@[reducible]
noncomputable def Exists.choose {α : Sort u_1} {p : αProp} (P : ∃ (a : α), p a) :
α

Extract an element from a existential statement, using Classical.choose.

Equations
Instances For
theorem Exists.choose_spec {α : Sort u_1} {p : αProp} (P : ∃ (a : α), p a) :
p ()

Show that an element extracted from P : ∃ a, p a using P.choose satisfies p.

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' = ap 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 forall_eq_or_imp {α : Sort u_1} {p : αProp} {q : αProp} {a' : α} :
(∀ (a : α), a = a' q ap a) p a' ∀ (a : α), q ap 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_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 : pProp} (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 = bp 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 ap 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 af a = bq b) ∀ (a : α), p aq (f a)
theorem forall_prop_of_false {p : Prop} {q : pProp} (hn : ¬p) :
(∀ (h' : p), q h') True

## decidable #

theorem Decidable.not_not {p : Prop} [] :
theorem Decidable.by_contra {p : Prop} [] :
(¬pFalse)p
def Or.by_cases {p : Prop} {q : Prop} [] {α : 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
• Or.by_cases h h₁ h₂ = if hp : p then h₁ hp else h₂ (_ : q)
Instances For
def Or.by_cases' {q : Prop} {p : Prop} [] {α : 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
• Or.by_cases' h h₁ h₂ = if hq : q then h₂ hq else h₁ (_ : p)
Instances For
instance exists_prop_decidable {p : Prop} (P : pProp) [] [(h : p) → Decidable (P h)] :
Decidable (∃ (h : p), P h)
Equations
instance forall_prop_decidable {p : Prop} (P : pProp) [] [(h : p) → Decidable (P h)] :
Decidable (∀ (h : p), P h)
Equations
theorem decide_eq_true_iff (p : Prop) [] :
p
@[simp]
theorem decide_eq_false_iff_not (p : Prop) :
∀ {x : }, ¬p
@[simp]
theorem decide_eq_decide {p : Prop} {q : Prop} :
∀ {x : } {x_1 : }, = (p q)
theorem Decidable.of_not_imp {a : Prop} {b : Prop} [] (h : ¬(ab)) :
a
theorem Decidable.not_imp_symm {a : Prop} {b : Prop} [] (h : ¬ab) (hb : ¬b) :
a
theorem Decidable.not_imp_comm {a : Prop} {b : Prop} [] [] :
¬ab ¬ba
theorem Decidable.not_imp_self {a : Prop} [] :
¬aa a
theorem Decidable.or_iff_not_imp_left {a : Prop} {b : Prop} [] :
a b ¬ab
theorem Decidable.or_iff_not_imp_right {b : Prop} {a : Prop} [] :
a b ¬ba
theorem Decidable.not_imp_not {a : Prop} {b : Prop} [] :
¬a¬b ba
theorem Decidable.not_or_of_imp {a : Prop} {b : Prop} [] (h : ab) :
¬a b
theorem Decidable.imp_iff_not_or {a : Prop} {b : Prop} [] :
ab ¬a b
theorem Decidable.imp_iff_or_not {b : Prop} {a : Prop} [] :
ba a ¬b
theorem Decidable.imp_or {a : Prop} {b : Prop} {c : Prop} [] :
ab c (ab) (ac)
theorem Decidable.imp_or' {b : Prop} {a : Sort u_1} {c : Prop} [] :
ab c (ab) (ac)
theorem Decidable.not_imp_iff_and_not {a : Prop} {b : Prop} [] :
¬(ab) a ¬b
theorem Decidable.peirce (a : Prop) (b : Prop) [] :
((ab)a)a
theorem peirce' {a : Prop} (H : ∀ (b : Prop), (ab)a) :
a
theorem Decidable.not_iff_not {a : Prop} {b : Prop} [] [] :
(¬a ¬b) (a b)
theorem Decidable.not_iff_comm {a : Prop} {b : Prop} [] [] :
(¬a b) (¬b a)
theorem Decidable.not_iff {b : Prop} {a : Prop} [] :
¬(a b) (¬a b)
theorem Decidable.iff_not_comm {a : Prop} {b : Prop} [] [] :
(a ¬b) (b ¬a)
theorem Decidable.iff_iff_not_or_and_or_not {a : Prop} {b : Prop} [] [] :
(a b) (¬a b) (a ¬b)
theorem Decidable.not_and_not_right {b : Prop} {a : Prop} [] :
¬(a ¬b) ab
theorem Decidable.or_iff_not_and_not {a : Prop} {b : Prop} [] [] :
a b ¬(¬a ¬b)
theorem Decidable.and_iff_not_or_not {a : Prop} {b : Prop} [] [] :
a b ¬(¬a ¬b)
theorem Decidable.imp_iff_right_iff {a : Prop} {b : Prop} [] :
(ab b) a b
theorem Decidable.and_or_imp {a : Prop} {b : Prop} {c : Prop} [] :
a b (ac) ab c
theorem Decidable.or_congr_left' {c : Prop} {a : Prop} {b : Prop} [] (h : ¬c(a b)) :
a c b c
theorem Decidable.or_congr_right' {a : Prop} {b : Prop} {c : Prop} [] (h : ¬a(b c)) :
a b a c
@[inline]
def decidable_of_iff {b : Prop} (a : Prop) (h : a 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 dec_trivial will not work.

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

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
Instances For
instance Decidable.predToBool {α : Sort u_1} (p : αProp) [] :
CoeDep (αProp) p (αBool)
Equations
• = { coe := fun (b : α) => decide (p b) }
def decidable_of_bool {a : Prop} (b : Bool) :
( 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
Instances For
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.exists_not_of_not_forall {α : Sort u_1} {p : αProp} [Decidable (∃ (x : α), ¬p x)] [(x : α) → Decidable (p x)] :
(¬∀ (x : α), p x)∃ (x : α), ¬p x

Alias of the forward direction of Decidable.not_forall.

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

## classical logic #

theorem Classical.not_not {a : Prop} :

The Double Negation Theorem: ¬¬P is equivalent to P. The left-to-right direction, double negation elimination (DNE), is classically true but not constructively.

@[simp]
theorem Classical.not_forall {α : Sort u_1} {p : αProp} :
(¬∀ (x : α), p x) ∃ (x : α), ¬p x
theorem Classical.exists_not_of_not_forall {α : Sort u_1} {p : αProp} :
(¬∀ (x : α), p x)∃ (x : α), ¬p x

Alias of the forward direction of Classical.not_forall.

theorem Classical.not_forall_not {α : Sort u_1} {p : αProp} :
(¬∀ (x : α), ¬p x) ∃ (x : α), p x
theorem Classical.not_exists_not {α : Sort u_1} {p : αProp} :
(¬∃ (x : α), ¬p x) ∀ (x : α), p x
theorem Classical.forall_or_exists_not {α : Sort u_1} (P : αProp) :
(∀ (a : α), P a) ∃ (a : α), ¬P a
theorem Classical.exists_or_forall_not {α : Sort u_1} (P : αProp) :
(∃ (a : α), P a) ∀ (a : α), ¬P a
theorem Classical.or_iff_not_imp_left {a : Prop} {b : Prop} :
a b ¬ab
theorem Classical.or_iff_not_imp_right {a : Prop} {b : Prop} :
a b ¬ba
theorem Classical.not_imp_iff_and_not {a : Prop} {b : Prop} :
¬(ab) a ¬b
theorem Classical.not_iff {a : Prop} {b : Prop} :
¬(a b) (¬a b)

## equality #

theorem heq_iff_eq :
∀ {α : Sort u_1} {a b : α}, HEq a b a = b
theorem proof_irrel_heq {p : Prop} {q : Prop} (hp : p) (hq : q) :
HEq hp hq
@[simp]
theorem eq_rec_constant {α : Sort u_1} {a : α} {a' : α} {β : Sort u_2} (y : β) (h : a = a') :
hy = y
theorem congrArg₂ {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} (f : αβγ) {x : α} {x' : α} {y : β} {y' : β} (hx : x = x') (hy : y = y') :
f x y = f x' y'
theorem congrFun₂ {α : Sort u_1} {β : αSort u_2} {γ : (a : α) → β aSort u_3} {f : (a : α) → (b : β a) → γ a b} {g : (a : α) → (b : β a) → γ a b} (h : f = g) (a : α) (b : β a) :
f a b = g a b
theorem congrFun₃ {α : Sort u_1} {β : αSort u_2} {γ : (a : α) → β aSort u_3} {δ : (a : α) → (b : β a) → γ a bSort u_4} {f : (a : α) → (b : β a) → (c : γ a b) → δ a b c} {g : (a : α) → (b : β a) → (c : γ a b) → δ a b c} (h : f = g) (a : α) (b : β a) (c : γ a b) :
f a b c = g a b c
theorem funext₂ {α : Sort u_1} {β : αSort u_2} {γ : (a : α) → β aSort u_3} {f : (a : α) → (b : β a) → γ a b} {g : (a : α) → (b : β a) → γ a b} (h : ∀ (a : α) (b : β a), f a b = g a b) :
f = g
theorem funext₃ {α : Sort u_1} {β : αSort u_2} {γ : (a : α) → β aSort u_3} {δ : (a : α) → (b : β a) → γ a bSort u_4} {f : (a : α) → (b : β a) → (c : γ a b) → δ a b c} {g : (a : α) → (b : β a) → (c : γ a b) → δ a b c} (h : ∀ (a : α) (b : β a) (c : γ a b), f a b c = g a b c) :
f = g
theorem ne_of_apply_ne {α : Sort u_1} {β : Sort u_2} (f : αβ) {x : α} {y : α} :
f x f yx y
theorem Eq.congr :
∀ {α : Sort u_1} {x₁ y₁ x₂ y₂ : α}, x₁ = y₁x₂ = y₂(x₁ = x₂ y₁ = y₂)
theorem Eq.congr_left {α : Sort u_1} {x : α} {y : α} {z : α} (h : x = y) :
x = z y = z
theorem Eq.congr_right {α : Sort u_1} {x : α} {y : α} {z : α} (h : x = y) :
z = x z = y
theorem congr_arg {α : Sort u} {β : Sort v} {a₁ : α} {a₂ : α} (f : αβ) (h : a₁ = a₂) :
f a₁ = f a₂

Alias of congrArg.

Congruence in the function argument: if a₁ = a₂ then f a₁ = f a₂ for any (nondependent) function f. This is more powerful than it might look at first, because you can also use a lambda expression for f to prove that <something containing a₁> = <something containing a₂>. This function is used internally by tactics like congr and simp to apply equalities inside subterms.

theorem congr_arg₂ {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} (f : αβγ) {x : α} {x' : α} {y : β} {y' : β} (hx : x = x') (hy : y = y') :
f x y = f x' y'

Alias of congrArg₂.

theorem congr_fun {α : Sort u} {β : αSort v} {f : (x : α) → β x} {g : (x : α) → β x} (h : f = g) (a : α) :
f a = g a

Alias of congrFun.

Congruence in the function part of an application: If f = g then f a = g a.

theorem congr_fun₂ {α : Sort u_1} {β : αSort u_2} {γ : (a : α) → β aSort u_3} {f : (a : α) → (b : β a) → γ a b} {g : (a : α) → (b : β a) → γ a b} (h : f = g) (a : α) (b : β a) :
f a b = g a b

Alias of congrFun₂.

theorem congr_fun₃ {α : Sort u_1} {β : αSort u_2} {γ : (a : α) → β aSort u_3} {δ : (a : α) → (b : β a) → γ a bSort u_4} {f : (a : α) → (b : β a) → (c : γ a b) → δ a b c} {g : (a : α) → (b : β a) → (c : γ a b) → δ a b c} (h : f = g) (a : α) (b : β a) (c : γ a b) :
f a b c = g a b c

Alias of congrFun₃.

theorem eq_mp_eq_cast {α : Sort u_1} {β : Sort u_1} (h : α = β) :
= cast h
theorem eq_mpr_eq_cast {α : Sort u_1} {β : Sort u_1} (h : α = β) :
= cast (_ : β = α)
@[simp]
theorem cast_cast {α : Sort u_1} {β : Sort u_1} {γ : Sort u_1} (ha : α = β) (hb : β = γ) (a : α) :
cast hb (cast ha a) = cast (_ : α = γ) a
theorem heq_of_cast_eq {α : Sort u_1} {β : Sort u_1} {a : α} {a' : β} (e : α = β) :
cast e a = a'HEq a a'
theorem cast_eq_iff_heq :
∀ {a a_1 : Sort u_1} {e : a = a_1} {a_2 : a} {a' : a_1}, cast e a_2 = a' HEq a_2 a'
theorem eqRec_eq_cast {α : Sort u_1} {a : α} {motive : (a' : α) → a = a'Sort u_2} (x : motive a (_ : a = a)) {a' : α} (e : a = a') :
ex = cast (_ : motive a (_ : a = a) = motive a' e) x
theorem eqRec_heq_self {α : Sort u_1} {a : α} {motive : (a' : α) → a = a'Sort u_2} (x : motive a (_ : a = a)) {a' : α} (e : a = a') :
HEq (ex) x
@[simp]
theorem eqRec_heq_iff_heq {α : Sort u_1} {a : α} {motive : (a' : α) → a = a'Sort u_2} (x : motive a (_ : a = a)) {a' : α} (e : a = a') {β : Sort u_2} (y : β) :
HEq (ex) y HEq x y
@[simp]
theorem heq_eqRec_iff_heq {α : Sort u_1} {a : α} {motive : (a' : α) → a = a'Sort u_2} (x : motive a (_ : a = a)) {a' : α} (e : a = a') {β : Sort u_2} (y : β) :
HEq y (ex) HEq y x

## membership #

theorem ne_of_mem_of_not_mem {α : Type u_1} {β : Type u_2} [] {s : β} {a : α} {b : α} (h : a s) :
¬b sa b
theorem ne_of_mem_of_not_mem' {α : Type u_1} {β : Type u_2} [] {s : β} {t : β} {a : α} (h : a s) :
¬a ts t

## if-then-else #

@[simp]
theorem if_true {α : Sort u_1} {h : } (t : α) (e : α) :
(if True then t else e) = t
@[simp]
theorem if_false {α : Sort u_1} {h : } (t : α) (e : α) :
(if False then t else e) = e
theorem ite_id {c : Prop} [] {α : Sort u_1} (t : α) :
(if c then t else t) = t
theorem apply_dite {α : Sort u_1} {β : Sort u_2} (f : αβ) (P : Prop) [] (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) [] (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_not {α : Sort u_1} (P : Prop) :
∀ {x : } (x_1 : ¬Pα) (y : ¬¬Pα), dite (¬P) x_1 y = dite P (fun (h : P) => y (_ : ¬¬P)) x_1

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) :
∀ {x : } (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.

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

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

## miscellaneous #

def Empty.elim {C : Sort u_1} :
EmptyC

Ex falso, the nondependent eliminator for the Empty type.

Equations
• = nomatch a
Instances For
Equations
Equations
def PEmpty.elim {C : Sort u_1} :
PEmptyC

Ex falso, the nondependent eliminator for the PEmpty type.

Equations
• = nomatch a
Instances For
Equations
Equations
@[simp]
@[simp]
instance instSubsingletonProd {α : Type u_1} {β : Type u_2} [] [] :
Equations
Equations
instance instInhabitedPSum {α : Sort u_1} {β : Sort u_2} [] :
Inhabited (α ⊕' β)
Equations
• instInhabitedPSum = { default := PSum.inl default }
instance instInhabitedPSum_1 {α : Sort u_1} {β : Sort u_2} [] :
Inhabited (α ⊕' β)
Equations
• instInhabitedPSum_1 = { default := PSum.inr default }
theorem eq_iff_true_of_subsingleton {α : Sort u_1} [] (x : α) (y : α) :
x = y True
theorem subsingleton_of_forall_eq {α : Sort u_1} (x : α) (h : ∀ (y : α), y = x) :

If all points are equal to a given point x, then α is a subsingleton.

theorem subsingleton_iff_forall_eq {α : Sort u_1} (x : α) :
∀ (y : α), y = x
theorem Bool.eq_iff_iff {a : Bool} {b : Bool} :
a = b ( )
theorem ne_comm {α : Sort u_1} {a : α} {b : α} :
a b b a
theorem congr_eqRec {α : Sort u_1} {γ : Sort u_2} {x : α} {x' : α} {β : αSort u_3} (f : (x : α) → β xγ) (h : x = x') (y : β x) :
f x' (hy) = f x y