Documentation

Init.PropLemmas

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.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_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 : 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_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¬(ab)
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 bc (ac) (bc)
@[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)

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) ¬pq
@[simp]
theorem if_true_right {p : Prop} {q : Prop} [h : Decidable p] :
(if p then q else True) pq
@[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) = (¬pq)
@[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) pq
@[deprecated ite_then_self]
theorem ite_true_same (p : Prop) (q : Prop) [Decidable p] :
(if p then p else q) = (¬pq)
@[deprecated ite_else_self]
theorem ite_false_same (p : Prop) (q : Prop) [Decidable p] :
(if p then q else p) = (p q)

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

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 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
theorem exists₂_imp {α : Sort u_1} {p : αProp} {b : Prop} {P : (x : α) → p xProp} :
(∃ (x : α), ∃ (h : p x), P x h)b ∀ (x : α) (h : p x), P x hb
@[simp]
theorem exists_const {b : Prop} (α : Sort u_1) [i : Nonempty α] :
(∃ (x : α), b) b
theorem exists_prop_congr {p : Prop} {p' : Prop} {q : pProp} {q' : pProp} (hq : ∀ (h : p), q h q' h) (hp : p p') :
Exists q ∃ (h : p'), q'
theorem exists_prop_of_true {p : Prop} {q : pProp} (h : p) :
(∃ (h' : p), q h') q h
@[simp]
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} (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' = 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 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 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_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
@[simp]
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 : 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

Nonempty #

@[simp]
theorem nonempty_prop (p : Prop) :

decidable #

@[simp]
theorem Decidable.not_not {p : Prop} [Decidable p] :
@[reducible, inline]

Excluded middle. Added as alias for Decidable.em

Equations
Instances For
    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] :
    (¬pFalse)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₂
    Instances For
      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₁
      Instances For
        instance exists_prop_decidable {p : Prop} (P : pProp) [Decidable p] [(h : p) → Decidable (P h)] :
        Decidable (∃ (h : p), P h)
        Equations
        instance forall_prop_decidable {p : Prop} (P : pProp) [Decidable p] [(h : p) → Decidable (P h)] :
        Decidable (∀ (h : p), P h)
        Equations
        @[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 : ¬(ab)) :
        a
        theorem Decidable.not_imp_symm {a : Prop} {b : Prop} [Decidable a] (h : ¬ab) (hb : ¬b) :
        a
        theorem Decidable.not_imp_comm {a : Prop} {b : Prop} [Decidable a] [Decidable b] :
        ¬ab ¬ba
        theorem Decidable.not_imp_self {a : Prop} [Decidable a] :
        ¬aa a
        theorem Decidable.or_iff_not_imp_left {a : Prop} {b : Prop} [Decidable a] :
        a b ¬ab
        theorem Decidable.or_iff_not_imp_right {b : Prop} {a : Prop} [Decidable b] :
        a b ¬ba
        theorem Decidable.not_imp_not {a : Prop} {b : Prop} [Decidable a] :
        ¬a¬b ba
        theorem Decidable.not_or_of_imp {a : Prop} {b : Prop} [Decidable a] (h : ab) :
        ¬a b
        theorem Decidable.imp_iff_not_or {a : Prop} {b : Prop} [Decidable a] :
        ab ¬a b
        theorem Decidable.imp_iff_or_not {b : Prop} {a : Prop} [Decidable b] :
        ba a ¬b
        theorem Decidable.imp_or {a : Prop} {b : Prop} {c : Prop} [h : Decidable a] :
        ab c (ab) (ac)
        theorem Decidable.imp_or' {b : Prop} {a : Sort u_1} {c : Prop} [Decidable b] :
        ab c (ab) (ac)
        theorem Decidable.not_imp_iff_and_not {a : Prop} {b : Prop} [Decidable a] :
        ¬(ab) a ¬b
        theorem Decidable.peirce (a : Prop) (b : Prop) [Decidable a] :
        ((ab)a)a
        theorem peirce' {a : Prop} (H : ∀ (b : Prop), (ab)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.not_and_not_right {b : Prop} {a : Prop} [Decidable b] :
        ¬(a ¬b) ab
        theorem Decidable.imp_iff_right_iff {a : Prop} {b : Prop} [Decidable a] :
        (ab b) a b
        theorem Decidable.imp_iff_left_iff {a : Prop} {b : Prop} [Decidable a] :
        (b ab) a b
        theorem Decidable.and_or_imp {a : Prop} {b : Prop} {c : Prop} [Decidable a] :
        a b (ac) ab 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
        @[inline]
        def decidable_of_iff {b : Prop} (a : Prop) (h : a b) [Decidable a] :

        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
        Instances For
          @[inline]
          def decidable_of_iff' {a : Prop} (b : Prop) (h : a b) [Decidable 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) [DecidablePred p] :
            CoeDep (αProp) p (αBool)
            Equations
            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
            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.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 (uv)] [du : Decidable u] {dv : uDecidable v} :
              decide (uv) = 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_then {α : 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_else {α : 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_then (p : Prop) [Decidable p] {x : Prop} {y : ¬pProp} :
              ((if h : p then x else y h) x) ∀ (h : ¬p), y h x
              @[simp]
              theorem dite_iff_else (p : Prop) [Decidable p] {x : pProp} {y : Prop} :
              ((if h : p then x h else y) y) ∀ (h : p), x h y
              @[simp]
              theorem ite_eq_then {α : Sort u_1} (p : Prop) [Decidable p] (x : α) (y : α) :
              (if p then x else y) = x ¬py = x
              @[simp]
              theorem ite_eq_else {α : Sort u_1} (p : Prop) [Decidable p] (x : α) (y : α) :
              (if p then x else y) = y px = y
              @[simp]
              theorem ite_iff_then (p : Prop) [Decidable p] (x : Prop) (y : Prop) :
              ((if p then x else y) x) ¬py = x
              @[simp]
              theorem ite_iff_else (p : Prop) [Decidable p] (x : Prop) (y : Prop) :
              ((if p then x else y) y) px = y
              @[simp]
              theorem dite_then_false (p : Prop) [Decidable p] {x : ¬pProp} :
              (if h : p then False else x h) ∃ (h : ¬p), x h
              @[simp]
              theorem dite_else_false (p : Prop) [Decidable p] {x : pProp} :
              (if h : p then x h else False) ∃ (h : p), x h
              @[simp]
              theorem dite_then_true (p : Prop) [Decidable p] {x : ¬pProp} :
              (if h : p then True else x h) ∀ (h : ¬p), x h
              @[simp]
              theorem dite_else_true (p : Prop) [Decidable p] {x : pProp} :
              (if h : p then x h else True) ∀ (h : p), x h