Documentation

Mathlib.Logic.Basic

Basic logic properties #

This file is one of the earliest imports in mathlib.

Implementation notes #

Theorems that require decidability hypotheses are in the namespace Decidable. Classical versions are in the namespace Classical.

@[reducible, inline]
abbrev hidden {α : Sort u_1} {a : α} :
α

An identity function with its main argument implicit. This will be printed as hidden even if it is applied to a large term, so it can be used for elision, as done in the elide and unelide tactics.

Equations
  • hidden = a
Instances For
    @[instance 10]
    Equations
    instance instSubsingletonSubtype_mathlib {α : Sort u_1} [Subsingleton α] (p : αProp) :
    Equations
    • =
    theorem congr_heq {α : Sort u_2} {β : Sort u_2} {γ : Sort u_3} {f : αγ} {g : βγ} {x : α} {y : β} (h₁ : HEq f g) (h₂ : HEq x y) :
    f x = g y
    theorem congr_arg_heq {α : Sort u_1} {β : αSort u_2} (f : (a : α) → β a) {a₁ : α} {a₂ : α} :
    a₁ = a₂HEq (f a₁) (f a₂)
    theorem ULift.down_injective {α : Type u_2} :
    @[simp]
    theorem ULift.down_inj {α : Type u_2} {a : ULift.{u_3, u_2} α} {b : ULift.{u_3, u_2} α} :
    a.down = b.down a = b
    theorem PLift.down_injective {α : Sort u_1} :
    @[simp]
    theorem PLift.down_inj {α : Sort u_1} {a : PLift α} {b : PLift α} :
    a.down = b.down a = b
    @[simp]
    theorem eq_iff_eq_cancel_left {α : Sort u_1} {b : α} {c : α} :
    (∀ {a : α}, a = b a = c) b = c
    @[simp]
    theorem eq_iff_eq_cancel_right {α : Sort u_1} {a : α} {b : α} :
    (∀ {c : α}, a = c b = c) a = b
    theorem ne_and_eq_iff_right {α : Sort u_1} {a : α} {b : α} {c : α} (h : b c) :
    a b a = c a = c
    class Fact (p : Prop) :

    Wrapper for adding elementary propositions to the type class systems. Warning: this can easily be abused. See the rest of this docstring for details.

    Certain propositions should not be treated as a class globally, but sometimes it is very convenient to be able to use the type class system in specific circumstances.

    For example, ZMod p is a field if and only if p is a prime number. In order to be able to find this field instance automatically by type class search, we have to turn p.prime into an instance implicit assumption.

    On the other hand, making Nat.prime a class would require a major refactoring of the library, and it is questionable whether making Nat.prime a class is desirable at all. The compromise is to add the assumption [Fact p.prime] to ZMod.field.

    In particular, this class is not intended for turning the type class system into an automated theorem prover for first order logic.

    • out : p

      Fact.out contains the unwrapped witness for the fact represented by the instance of Fact p.

    Instances
      theorem Fact.out {p : Prop} [self : Fact p] :
      p

      Fact.out contains the unwrapped witness for the fact represented by the instance of Fact p.

      theorem Fact.elim {p : Prop} (h : Fact p) :
      p
      theorem fact_iff {p : Prop} :
      Fact p p
      Equations
      @[reducible, inline]
      abbrev Function.swap₂ {ι₁ : Sort u_2} {ι₂ : Sort u_3} {κ₁ : ι₁Sort u_4} {κ₂ : ι₂Sort u_5} {φ : (i₁ : ι₁) → κ₁ i₁(i₂ : ι₂) → κ₂ i₂Sort u_6} (f : (i₁ : ι₁) → (j₁ : κ₁ i₁) → (i₂ : ι₂) → (j₂ : κ₂ i₂) → φ i₁ j₁ i₂ j₂) (i₂ : ι₂) (j₂ : κ₂ i₂) (i₁ : ι₁) (j₁ : κ₁ i₁) :
      φ i₁ j₁ i₂ j₂

      Swaps two pairs of arguments to a function.

      Equations
      Instances For

        Declarations about propositional connectives #

        Declarations about implies #

        theorem Iff.imp {a : Prop} {b : Prop} {c : Prop} {d : Prop} (h₁ : a c) (h₂ : b d) :
        ab cd

        Alias of imp_congr.

        theorem imp_iff_right_iff {a : Prop} {b : Prop} :
        (ab b) a b
        theorem and_or_imp {a : Prop} {b : Prop} {c : Prop} :
        a b (ac) ab c
        theorem Function.mt {a : Prop} {b : Prop} :
        (ab)¬b¬a

        Provide modus tollens (mt) as dot notation for implications.

        Declarations about not #

        theorem dec_em (p : Prop) [Decidable p] :
        p ¬p

        Alias of Decidable.em.

        theorem dec_em' (p : Prop) [Decidable p] :
        ¬p p
        theorem em (p : Prop) :
        p ¬p

        Alias of Classical.em.


        Diaconescu's theorem: excluded middle from choice, Function extensionality and propositional extensionality.

        theorem em' (p : Prop) :
        ¬p p
        theorem or_not {p : Prop} :
        p ¬p
        theorem Decidable.eq_or_ne {α : Sort u_1} (x : α) (y : α) [Decidable (x = y)] :
        x = y x y
        theorem Decidable.ne_or_eq {α : Sort u_1} (x : α) (y : α) [Decidable (x = y)] :
        x y x = y
        theorem eq_or_ne {α : Sort u_1} (x : α) (y : α) :
        x = y x y
        theorem ne_or_eq {α : Sort u_1} (x : α) (y : α) :
        x y x = y
        theorem by_contradiction {p : Prop} :
        (¬pFalse)p
        theorem by_cases {p : Prop} {q : Prop} (hpq : pq) (hnpq : ¬pq) :
        q
        theorem by_contra {p : Prop} :
        (¬pFalse)p

        Alias of by_contradiction.

        theorem of_not_not {a : Prop} :
        ¬¬aa
        theorem not_ne_iff {α : Sort u_1} {a : α} {b : α} :
        ¬a b a = b
        theorem of_not_imp {a : Prop} {b : Prop} :
        ¬(ab)a
        theorem Not.decidable_imp_symm {a : Prop} {b : Prop} [Decidable a] (h : ¬ab) (hb : ¬b) :
        a

        Alias of Decidable.not_imp_symm.

        theorem Not.imp_symm {a : Prop} {b : Prop} :
        (¬ab)¬ba
        theorem not_imp_comm {a : Prop} {b : Prop} :
        ¬ab ¬ba
        @[simp]
        theorem not_imp_self {a : Prop} :
        ¬aa a
        theorem Imp.swap {a : Sort u_1} {b : Sort u_2} {c : Prop} :
        abc bac
        theorem Iff.not {a : Prop} {b : Prop} (h : a b) :

        Alias of not_congr.

        theorem Iff.not_left {a : Prop} {b : Prop} (h : a ¬b) :
        ¬a b
        theorem Iff.not_right {a : Prop} {b : Prop} (h : ¬a b) :
        a ¬b
        theorem Iff.ne {α : Sort u_1} {β : Sort u_2} {a : α} {b : α} {c : β} {d : β} :
        (a = b c = d)(a b c d)
        theorem Iff.ne_left {α : Sort u_1} {β : Sort u_2} {a : α} {b : α} {c : β} {d : β} :
        (a = b c d)(a b c = d)
        theorem Iff.ne_right {α : Sort u_1} {β : Sort u_2} {a : α} {b : α} {c : β} {d : β} :
        (a b c = d)(a = b c d)

        Declarations about Xor' #

        @[simp]
        @[simp]
        theorem xor_false :
        theorem xor_comm (a : Prop) (b : Prop) :
        Xor' a b = Xor' b a
        @[simp]
        theorem xor_self (a : Prop) :
        @[simp]
        theorem xor_not_left {a : Prop} {b : Prop} :
        Xor' (¬a) b (a b)
        @[simp]
        theorem xor_not_right {a : Prop} {b : Prop} :
        Xor' a ¬b (a b)
        theorem xor_not_not {a : Prop} {b : Prop} :
        Xor' (¬a) ¬b Xor' a b
        theorem Xor'.or {a : Prop} {b : Prop} (h : Xor' a b) :
        a b

        Declarations about and #

        theorem Iff.and {a : Prop} {c : Prop} {b : Prop} {d : Prop} (h₁ : a c) (h₂ : b d) :
        a b c d

        Alias of and_congr.

        theorem And.rotate {a : Prop} {b : Prop} {c : Prop} :
        a b cb c a

        Alias of the forward direction of and_rotate.

        theorem and_symm_right {α : Sort u_1} (a : α) (b : α) (p : Prop) :
        p a = b p b = a
        theorem and_symm_left {α : Sort u_1} (a : α) (b : α) (p : Prop) :
        a = b p b = a p

        Declarations about or #

        theorem Iff.or {a : Prop} {c : Prop} {b : Prop} {d : Prop} (h₁ : a c) (h₂ : b d) :
        a b c d

        Alias of or_congr.

        theorem Or.rotate {a : Prop} {b : Prop} {c : Prop} :
        a b cb c a

        Alias of the forward direction of or_rotate.

        theorem Or.elim3 {a : Prop} {b : Prop} {c : Prop} {d : Prop} (h : a b c) (ha : ad) (hb : bd) (hc : cd) :
        d
        theorem Or.imp3 {a : Prop} {b : Prop} {d : Prop} {e : Prop} {c : Prop} {f : Prop} (had : ad) (hbe : be) (hcf : cf) :
        a b cd e f
        theorem not_or_of_imp {a : Prop} {b : Prop} :
        (ab)¬a b
        theorem Decidable.or_not_of_imp {a : Prop} {b : Prop} [Decidable a] (h : ab) :
        b ¬a
        theorem or_not_of_imp {a : Prop} {b : Prop} :
        (ab)b ¬a
        theorem imp_iff_not_or {a : Prop} {b : Prop} :
        ab ¬a b
        theorem imp_iff_or_not {b : Prop} {a : Prop} :
        ba a ¬b
        theorem not_imp_not {a : Prop} {b : Prop} :
        ¬a¬b ba
        theorem imp_and_neg_imp_iff (p : Prop) (q : Prop) :
        (pq) (¬pq) q
        theorem Function.mtr {a : Prop} {b : Prop} :
        (¬a¬b)ba

        Provide the reverse of modus tollens (mt) as dot notation for implications.

        theorem or_congr_left' {c : Prop} {a : Prop} {b : Prop} (h : ¬c(a b)) :
        a c b c
        theorem or_congr_right' {a : Prop} {b : Prop} {c : Prop} (h : ¬a(b c)) :
        a b a c

        Declarations about distributivity #

        Declarations about iff

        theorem Iff.iff {p₁ : Prop} {p₂ : Prop} {q₁ : Prop} {q₂ : Prop} (h₁ : p₁ p₂) (h₂ : q₁ q₂) :
        (p₁ q₁) (p₂ q₂)

        Alias of iff_congr.

        theorem iff_mpr_iff_true_intro {P : Prop} (h : P) :
        = h
        theorem imp_or {a : Prop} {b : Prop} {c : Prop} :
        ab c (ab) (ac)
        theorem imp_or' {a : Sort u_1} {b : Prop} {c : Prop} :
        ab c (ab) (ac)
        theorem not_imp {a : Prop} {b : Prop} :
        ¬(ab) a ¬b
        theorem peirce (a : Prop) (b : Prop) :
        ((ab)a)a
        theorem not_iff_not {a : Prop} {b : Prop} :
        (¬a ¬b) (a b)
        theorem not_iff_comm {a : Prop} {b : Prop} :
        (¬a b) (¬b a)
        theorem not_iff {a : Prop} {b : Prop} :
        ¬(a b) (¬a b)
        theorem iff_not_comm {a : Prop} {b : Prop} :
        (a ¬b) (b ¬a)
        theorem iff_iff_and_or_not_and_not {a : Prop} {b : Prop} :
        (a b) a b ¬a ¬b
        theorem iff_iff_not_or_and_or_not {a : Prop} {b : Prop} :
        (a b) (¬a b) (a ¬b)
        theorem not_and_not_right {a : Prop} {b : Prop} :
        ¬(a ¬b) ab

        De Morgan's laws #

        theorem not_and_or {a : Prop} {b : Prop} :
        ¬(a b) ¬a ¬b

        One of de Morgan's laws: the negation of a conjunction is logically equivalent to the disjunction of the negations.

        theorem or_iff_not_and_not {a : Prop} {b : Prop} :
        a b ¬(¬a ¬b)
        theorem and_iff_not_or_not {a : Prop} {b : Prop} :
        a b ¬(¬a ¬b)
        @[simp]
        theorem not_xor (P : Prop) (Q : Prop) :
        ¬Xor' P Q (P Q)
        theorem xor_iff_not_iff (P : Prop) (Q : Prop) :
        Xor' P Q ¬(P Q)
        theorem xor_iff_iff_not {a : Prop} {b : Prop} :
        Xor' a b (a ¬b)
        theorem xor_iff_not_iff' {a : Prop} {b : Prop} :
        Xor' a b (¬a b)

        Declarations about equality #

        theorem Membership.mem.ne_of_not_mem {α : Type u_1} {β : Type u_2} [Membership α β] {s : β} {a : α} {b : α} (h : a s) :
        ¬b sa b

        Alias of ne_of_mem_of_not_mem.

        theorem Membership.mem.ne_of_not_mem' {α : Type u_1} {β : Type u_2} [Membership α β] {s : β} {t : β} {a : α} (h : a s) :
        ¬a ts t

        Alias of ne_of_mem_of_not_mem'.

        theorem forall_cond_comm {α : Sort u_1} {s : αProp} {p : ααProp} :
        (∀ (a : α), s a∀ (b : α), s bp a b) ∀ (a b : α), s as bp a b
        theorem forall_mem_comm {α : Type u_1} {β : Type u_2} [Membership α β] {s : β} {p : ααProp} :
        (∀ (a : α), a s∀ (b : α), b sp a b) ∀ (a b : α), a sb sp a b
        @[deprecated forall_cond_comm]
        theorem ball_cond_comm {α : Sort u_1} {s : αProp} {p : ααProp} :
        (∀ (a : α), s a∀ (b : α), s bp a b) ∀ (a b : α), s as bp a b

        Alias of forall_cond_comm.

        @[deprecated forall_mem_comm]
        theorem ball_mem_comm {α : Type u_1} {β : Type u_2} [Membership α β] {s : β} {p : ααProp} :
        (∀ (a : α), a s∀ (b : α), b sp a b) ∀ (a b : α), a sb sp a b

        Alias of forall_mem_comm.

        theorem ne_of_eq_of_ne {α : Sort u_1} {a : α} {b : α} {c : α} (h₁ : a = b) (h₂ : b c) :
        a c
        theorem ne_of_ne_of_eq {α : Sort u_1} {a : α} {b : α} {c : α} (h₁ : a b) (h₂ : b = c) :
        a c
        theorem Eq.trans_ne {α : Sort u_1} {a : α} {b : α} {c : α} (h₁ : a = b) (h₂ : b c) :
        a c

        Alias of ne_of_eq_of_ne.

        theorem Ne.trans_eq {α : Sort u_1} {a : α} {b : α} {c : α} (h₁ : a b) (h₂ : b = c) :
        a c

        Alias of ne_of_ne_of_eq.

        theorem eq_equivalence {α : Sort u_1} :
        theorem congr_refl_left {α : Sort u_1} {β : Sort u_2} (f : αβ) {a : α} {b : α} (h : a = b) :
        =
        theorem congr_refl_right {α : Sort u_1} {β : Sort u_2} {f : αβ} {g : αβ} (h : f = g) (a : α) :
        =
        theorem congr_arg_refl {α : Sort u_1} {β : Sort u_2} (f : αβ) (a : α) :
        =
        theorem congr_fun_rfl {α : Sort u_1} {β : Sort u_2} (f : αβ) (a : α) :
        =
        theorem congr_fun_congr_arg {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} (f : αβγ) {a : α} {a' : α} (p : a = a') (b : β) :
        =
        theorem Eq.rec_eq_cast {α : Sort u_1} {P : αSort u_2} {x : α} {y : α} (h : x = y) (z : P x) :
        hz = cast z
        theorem eqRec_heq' {α : Sort u_1} {a' : α} {motive : (a : α) → a' = aSort u_2} (p : motive a' ) {a : α} (t : a' = a) :
        HEq (tp) p
        theorem rec_heq_of_heq {α : Sort u_2} {a : α} {β : Sort u_1} {b : α} {C : αSort u_1} {x : C a} {y : β} (e : a = b) (h : HEq x y) :
        HEq (ex) y
        theorem rec_heq_iff_heq {α : Sort u_2} {a : α} {β : Sort u_1} {b : α} {C : αSort u_1} {x : C a} {y : β} {e : a = b} :
        HEq (ex) y HEq x y
        theorem heq_rec_iff_heq {α : Sort u_2} {β : Sort u_1} {a : α} {b : α} {C : αSort u_1} {x : β} {y : C a} {e : a = b} :
        HEq x (ey) HEq x y

        Declarations about quantifiers #

        theorem pi_congr {α : Sort u_1} {β : αSort u_2} {β' : αSort u_2} (h : ∀ (a : α), β a = β' a) :
        ((a : α) → β a) = ((a : α) → β' a)
        theorem forall₂_imp {α : Sort u_1} {β : αSort u_2} {p : (a : α) → β aProp} {q : (a : α) → β aProp} (h : ∀ (a : α) (b : β a), p a bq a b) :
        (∀ (a : α) (b : β a), p a b)∀ (a : α) (b : β a), q a b
        theorem forall₃_imp {α : 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 cq 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₂.imp {α : Sort u_1} {β : αSort u_2} {p : (a : α) → β aProp} {q : (a : α) → β aProp} (h : ∀ (a : α) (b : β a), p a bq a b) :
        (∃ (a : α), ∃ (b : β a), p a b)∃ (a : α), ∃ (b : β a), q a b
        theorem Exists₃.imp {α : 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 cq 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_swap {α : Sort u_1} {β : Sort u_2} {p : αβProp} :
        (∀ (x : α) (y : β), p x y) ∀ (y : β) (x : α), p x y
        theorem forall₂_swap {ι₁ : Sort u_3} {ι₂ : Sort u_4} {κ₁ : ι₁Sort u_5} {κ₂ : ι₂Sort u_6} {p : (i₁ : ι₁) → κ₁ i₁(i₂ : ι₂) → κ₂ i₂Prop} :
        (∀ (i₁ : ι₁) (j₁ : κ₁ i₁) (i₂ : ι₂) (j₂ : κ₂ i₂), p i₁ j₁ i₂ j₂) ∀ (i₂ : ι₂) (j₂ : κ₂ i₂) (i₁ : ι₁) (j₁ : κ₁ i₁), p i₁ j₁ i₂ j₂
        theorem imp_forall_iff {α : Type u_3} {p : Prop} {q : αProp} :
        (p∀ (x : α), q x) ∀ (x : α), pq x

        We intentionally restrict the type of α in this lemma so that this is a safer to use in simp than forall_swap.

        theorem exists_swap {α : Sort u_1} {β : Sort u_2} {p : αβProp} :
        (∃ (x : α), ∃ (y : β), p x y) ∃ (y : β), ∃ (x : α), p x y
        theorem not_forall_not {α : Sort u_1} {p : αProp} :
        (¬∀ (x : α), ¬p x) ∃ (x : α), p x
        theorem forall_or_exists_not {α : Sort u_1} (P : αProp) :
        (∀ (a : α), P a) ∃ (a : α), ¬P a
        theorem exists_or_forall_not {α : Sort u_1} (P : αProp) :
        (∃ (a : α), P a) ∀ (a : α), ¬P a
        theorem forall_imp_iff_exists_imp {α : Sort u_3} {p : αProp} {b : Prop} [ha : Nonempty α] :
        (∀ (x : α), p x)b ∃ (x : α), p xb
        theorem forall_true_iff {α : Sort u_1} :
        αTrue True
        theorem forall_true_iff' {α : Sort u_1} {p : αProp} (h : ∀ (a : α), p a True) :
        (∀ (a : α), p a) True
        theorem forall₂_true_iff {α : Sort u_1} {β : αSort u_3} :
        (∀ (a : α), β aTrue) True
        theorem forall₃_true_iff {α : Sort u_1} {β : αSort u_3} {γ : (a : α) → β aSort u_4} :
        (∀ (a : α) (b : β a), γ a bTrue) True
        @[simp]
        theorem exists_unique_iff_exists {α : Sort u_1} [Subsingleton α] {p : αProp} :
        (∃! x : α, p x) ∃ (x : α), p x
        theorem exists_unique_const {b : Prop} (α : Sort u_3) [i : Nonempty α] [Subsingleton α] :
        (∃! x : α, b) b
        theorem Decidable.and_forall_ne {α : Sort u_1} [DecidableEq α] (a : α) {p : αProp} :
        (p a ∀ (b : α), b ap b) ∀ (b : α), p b
        theorem and_forall_ne {α : Sort u_1} {p : αProp} (a : α) :
        (p a ∀ (b : α), b ap b) ∀ (b : α), p b
        theorem Ne.ne_or_ne {α : Sort u_1} {x : α} {y : α} (z : α) (h : x y) :
        x z y z
        @[simp]
        theorem exists_unique_eq {α : Sort u_1} {a' : α} :
        ∃! a : α, a = a'
        @[simp]
        theorem exists_unique_eq' {α : Sort u_1} {a' : α} :
        ∃! a : α, a' = a
        @[simp]
        theorem exists_apply_eq_apply' {α : Sort u_1} {β : Sort u_2} (f : αβ) (a' : α) :
        ∃ (a : α), f a' = f a
        @[simp]
        theorem exists_apply_eq_apply2 {α : Sort u_3} {β : Sort u_4} {γ : Sort u_5} {f : αβγ} {a : α} {b : β} :
        ∃ (x : α), ∃ (y : β), f x y = f a b
        @[simp]
        theorem exists_apply_eq_apply2' {α : Sort u_3} {β : Sort u_4} {γ : Sort u_5} {f : αβγ} {a : α} {b : β} :
        ∃ (x : α), ∃ (y : β), f a b = f x y
        @[simp]
        theorem exists_apply_eq_apply3 {α : Sort u_3} {β : Sort u_4} {γ : Sort u_5} {δ : Sort u_6} {f : αβγδ} {a : α} {b : β} {c : γ} :
        ∃ (x : α), ∃ (y : β), ∃ (z : γ), f x y z = f a b c
        @[simp]
        theorem exists_apply_eq_apply3' {α : Sort u_3} {β : Sort u_4} {γ : Sort u_5} {δ : Sort u_6} {f : αβγδ} {a : α} {b : β} {c : γ} :
        ∃ (x : α), ∃ (y : β), ∃ (z : γ), f a b c = f x y z
        theorem exists_apply_eq {α : Sort u_1} {β : Sort u_2} (a : α) (b : β) :
        ∃ (f : αβ), f a = b
        @[simp]
        theorem exists_exists_and_eq_and {α : Sort u_1} {β : Sort u_2} {f : αβ} {p : αProp} {q : βProp} :
        (∃ (b : β), (∃ (a : α), p a f a = b) q b) ∃ (a : α), p a q (f a)
        @[simp]
        theorem exists_exists_eq_and {α : Sort u_1} {β : Sort u_2} {f : αβ} {p : βProp} :
        (∃ (b : β), (∃ (a : α), f a = b) p b) ∃ (a : α), p (f a)
        @[simp]
        theorem exists_exists_and_exists_and_eq_and {α : Type u_3} {β : Type u_4} {γ : Type u_5} {f : αβγ} {p : αProp} {q : βProp} {r : γProp} :
        (∃ (c : γ), (∃ (a : α), p a ∃ (b : β), q b f a b = c) r c) ∃ (a : α), p a ∃ (b : β), q b r (f a b)
        @[simp]
        theorem exists_exists_exists_and_eq {α : Type u_3} {β : Type u_4} {γ : Type u_5} {f : αβγ} {p : γProp} :
        (∃ (c : γ), (∃ (a : α), ∃ (b : β), f a b = c) p c) ∃ (a : α), ∃ (b : β), p (f a b)
        @[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 forall_apply_eq_imp_iff' {α : Sort u_1} {β : Sort u_2} {f : αβ} {p : βProp} :
        (∀ (a : α) (b : β), f a = bp b) ∀ (a : α), p (f a)
        theorem forall_eq_apply_imp_iff' {α : Sort u_1} {β : Sort u_2} {f : αβ} {p : βProp} :
        (∀ (a : α) (b : β), b = f ap b) ∀ (a : α), p (f a)
        @[simp]
        theorem exists_eq_right' {α : Sort u_1} {p : αProp} {a' : α} :
        (∃ (a : α), p a a' = a) p a'
        theorem exists₂_comm {ι₁ : Sort u_3} {ι₂ : Sort u_4} {κ₁ : ι₁Sort u_5} {κ₂ : ι₂Sort u_6} {p : (i₁ : ι₁) → κ₁ i₁(i₂ : ι₂) → κ₂ i₂Prop} :
        (∃ (i₁ : ι₁), ∃ (j₁ : κ₁ i₁), ∃ (i₂ : ι₂), ∃ (j₂ : κ₂ i₂), p i₁ j₁ i₂ j₂) ∃ (i₂ : ι₂), ∃ (j₂ : κ₂ i₂), ∃ (i₁ : ι₁), ∃ (j₁ : κ₁ i₁), p i₁ j₁ i₂ j₂
        theorem And.exists {p : Prop} {q : Prop} {f : p qProp} :
        (∃ (h : p q), f h) ∃ (hp : p), ∃ (hq : q), f
        theorem forall_or_of_or_forall {α : Sort u_3} {p : αProp} {b : Prop} (h : b ∀ (x : α), p x) (x : α) :
        b p x
        theorem Decidable.forall_or_left {α : Sort u_1} {q : Prop} {p : αProp} [Decidable q] :
        (∀ (x : α), q p x) q ∀ (x : α), p x
        theorem forall_or_left {α : Sort u_1} {q : Prop} {p : αProp} :
        (∀ (x : α), q p x) q ∀ (x : α), p x
        theorem Decidable.forall_or_right {α : Sort u_1} {q : Prop} {p : αProp} [Decidable q] :
        (∀ (x : α), p x q) (∀ (x : α), p x) q
        theorem forall_or_right {α : Sort u_1} {q : Prop} {p : αProp} :
        (∀ (x : α), p x q) (∀ (x : α), p x) q
        theorem exists_unique_prop {p : Prop} {q : Prop} :
        (∃! x : p, q) p q
        @[simp]
        theorem exists_unique_false {α : Sort u_1} :
        ¬∃! x : α, False
        theorem Exists.fst {b : Prop} {p : bProp} :
        Exists pb
        theorem Exists.snd {b : Prop} {p : bProp} (h : Exists p) :
        p
        theorem Prop.exists_iff {p : PropProp} :
        (∃ (h : Prop), p h) p False p True
        theorem Prop.forall_iff {p : PropProp} :
        (∀ (h : Prop), p h) p False p True
        theorem exists_prop_of_true {p : Prop} {q : pProp} (h : p) :
        (∃ (h' : p), q h') q h
        theorem exists_iff_of_forall {p : Prop} {q : pProp} (h : ∀ (h : p), q h) :
        (∃ (h : p), q h) p
        theorem exists_unique_prop_of_true {p : Prop} {q : pProp} (h : p) :
        (∃! h' : p, q h') q h
        theorem exists_prop_of_false {p : Prop} {q : pProp} :
        ¬p¬∃ (h' : p), q h'
        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'
        @[simp]
        theorem exists_true_left (p : TrueProp) :
        (∃ (x : True), p x) p True.intro

        See IsEmpty.exists_iff for the False version.

        theorem forall_prop_congr {p : Prop} {p' : Prop} {q : pProp} {q' : pProp} (hq : ∀ (h : p), q h q' h) (hp : p p') :
        (∀ (h : p), q h) ∀ (h : p'), q'
        theorem forall_prop_congr' {p : Prop} {p' : Prop} {q : pProp} {q' : pProp} (hq : ∀ (h : p), q h q' h) (hp : p p') :
        (∀ (h : p), q h) = ∀ (h : p'), q'
        theorem imp_congr_eq {a : Prop} {b : Prop} {c : Prop} {d : Prop} (h₁ : a = c) (h₂ : b = d) :
        (ab) = (cd)
        theorem imp_congr_ctx_eq {a : Prop} {b : Prop} {c : Prop} {d : Prop} (h₁ : a = c) (h₂ : cb = d) :
        (ab) = (cd)
        theorem eq_true_intro {a : Prop} (h : a) :
        theorem eq_false_intro {a : Prop} (h : ¬a) :
        def Iff.eq {a : Prop} {b : Prop} :
        (a b)a = b

        Alias of propext.


        The axiom of propositional extensionality. It asserts that if propositions a and b are logically equivalent (i.e. we can prove a from b and vice versa), then a and b are equal, meaning that we can replace a with b in all contexts.

        For simple expressions like a ∧ c ∨ d → e we can prove that because all the logical connectives respect logical equivalence, we can replace a with b in this expression without using propext. However, for higher order expressions like P a where P : Prop → Prop is unknown, or indeed for a = b itself, we cannot replace a with b without an axiom which says exactly this.

        This is a relatively uncontroversial axiom, which is intuitionistically valid. It does however block computation when using #reduce to reduce proofs directly (which is not recommended), meaning that canonicity, the property that all closed terms of type Nat normalize to numerals, fails to hold when this (or any) axiom is used:

        set_option pp.proofs true
        
        def foo : Nat := by
          have : (True → True) ↔ True := ⟨λ _ => trivial, λ _ _ => trivial⟩
          have := propext this ▸ (2 : Nat)
          exact this
        
        #reduce foo
        -- propext { mp := fun x x => True.intro, mpr := fun x => True.intro } ▸ 2
        
        #eval foo -- 2
        

        #eval can evaluate it to a numeral because the compiler erases casts and does not evaluate proofs, so propext, whose return type is a proposition, can never block it.

        Equations
        Instances For
          theorem iff_eq_eq {a : Prop} {b : Prop} :
          (a b) = (a = b)
          @[simp]
          theorem forall_true_left (p : TrueProp) :
          (∀ (x : True), p x) p True.intro

          See IsEmpty.forall_iff for the False version.

          theorem ExistsUnique.elim₂ {α : Sort u_3} {p : αSort u_4} [∀ (x : α), Subsingleton (p x)] {q : (x : α) → p xProp} {b : Prop} (h₂ : ∃! x : α, ∃! h : p x, q x h) (h₁ : ∀ (x : α) (h : p x), q x h(∀ (y : α) (hy : p y), q y hyy = x)b) :
          b
          theorem ExistsUnique.intro₂ {α : Sort u_3} {p : αSort u_4} [∀ (x : α), Subsingleton (p x)] {q : (x : α) → p xProp} (w : α) (hp : p w) (hq : q w hp) (H : ∀ (y : α) (hy : p y), q y hyy = w) :
          ∃! x : α, ∃! hx : p x, q x hx
          theorem ExistsUnique.exists₂ {α : Sort u_3} {p : αSort u_4} {q : (x : α) → p xProp} (h : ∃! x : α, ∃! hx : p x, q x hx) :
          ∃ (x : α), ∃ (hx : p x), q x hx
          theorem ExistsUnique.unique₂ {α : Sort u_3} {p : αSort u_4} [∀ (x : α), Subsingleton (p x)] {q : (x : α) → p xProp} (h : ∃! x : α, ∃! hx : p x, q x hx) {y₁ : α} {y₂ : α} (hpy₁ : p y₁) (hqy₁ : q y₁ hpy₁) (hpy₂ : p y₂) (hqy₂ : q y₂ hpy₂) :
          y₁ = y₂

          Classical lemmas #

          noncomputable def Classical.dec (p : Prop) :

          Any prop p is decidable classically. A shorthand for Classical.propDecidable.

          Equations
          Instances For
            noncomputable def Classical.decPred {α : Sort u_1} (p : αProp) :

            Any predicate p is decidable classically.

            Equations
            Instances For
              noncomputable def Classical.decRel {α : Sort u_1} (p : ααProp) :

              Any relation p is decidable classically.

              Equations
              Instances For
                noncomputable def Classical.decEq (α : Sort u_2) :

                Any type α has decidable equality classically.

                Equations
                Instances For
                  noncomputable def Classical.existsCases {α : Sort u_2} {C : Sort u_3} {p : αProp} (H0 : C) (H : (a : α) → p aC) :
                  C

                  Construct a function from a default value H0, and a function to use if there exists a value satisfying the predicate.

                  Equations
                  Instances For
                    theorem Classical.some_spec₂ {α : Sort u_2} {p : αProp} {h : ∃ (a : α), p a} (q : αProp) (hpq : ∀ (a : α), p aq a) :
                    noncomputable def Classical.subtype_of_exists {α : Type u_2} {P : αProp} (h : ∃ (x : α), P x) :
                    { x : α // P x }

                    A version of Classical.indefiniteDescription which is definitionally equal to a pair

                    Equations
                    Instances For
                      noncomputable def Classical.byContradiction' {α : Sort u_2} (H : ¬(αFalse)) :
                      α

                      A version of byContradiction that uses types instead of propositions.

                      Equations
                      Instances For
                        def Classical.choice_of_byContradiction' {α : Sort u_2} (contra : ¬(αFalse)α) :
                        Nonempty αα

                        classical.byContradiction' is equivalent to lean's axiom classical.choice.

                        Equations
                        Instances For
                          noncomputable def Exists.classicalRecOn {α : Sort u_1} {p : αProp} (h : ∃ (a : α), p a) {C : Sort u_2} (H : (a : α) → p aC) :
                          C

                          This function has the same type as Exists.recOn, and can be used to case on an equality, but Exists.recOn can only eliminate into Prop, while this version eliminates into any universe using the axiom of choice.

                          Equations
                          Instances For

                            Declarations about bounded quantifiers #

                            theorem bex_def {α : Sort u_1} {p : αProp} {q : αProp} :
                            (∃ (x : α), ∃ (x_1 : p x), q x) ∃ (x : α), p x q x
                            theorem BEx.elim {α : Sort u_1} {p : αProp} {P : (x : α) → p xProp} {b : Prop} :
                            (∃ (x : α), ∃ (h : p x), P x h)(∀ (a : α) (h : p a), P a hb)b
                            theorem BEx.intro {α : Sort u_1} {p : αProp} {P : (x : α) → p xProp} (a : α) (h₁ : p a) (h₂ : P a h₁) :
                            ∃ (x : α), ∃ (h : p x), P x h
                            @[deprecated exists_eq_left]
                            theorem bex_eq_left {α : Sort u_1} {p : αProp} {a : α} :
                            (∃ (x : α), ∃ (x_1 : x = a), p x) p a
                            @[deprecated forall₂_congr]
                            theorem ball_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

                            Alias of forall₂_congr.

                            @[deprecated exists₂_congr]
                            theorem bex_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

                            Alias of exists₂_congr.

                            theorem BAll.imp_right {α : Sort u_1} {p : αProp} {P : (x : α) → p xProp} {Q : (x : α) → p xProp} (H : ∀ (x : α) (h : p x), P x hQ x h) (h₁ : ∀ (x : α) (h : p x), P x h) (x : α) (h : p x) :
                            Q x h
                            theorem BEx.imp_right {α : Sort u_1} {p : αProp} {P : (x : α) → p xProp} {Q : (x : α) → p xProp} (H : ∀ (x : α) (h : p x), P x hQ x h) :
                            (∃ (x : α), ∃ (h : p x), P x h)∃ (x : α), ∃ (h : p x), Q x h
                            theorem BAll.imp_left {α : Sort u_1} {r : αProp} {p : αProp} {q : αProp} (H : ∀ (x : α), p xq x) (h₁ : ∀ (x : α), q xr x) (x : α) (h : p x) :
                            r x
                            theorem BEx.imp_left {α : Sort u_1} {r : αProp} {p : αProp} {q : αProp} (H : ∀ (x : α), p xq x) :
                            (∃ (x : α), ∃ (x_1 : p x), r x)∃ (x : α), ∃ (x_1 : q x), r x
                            @[deprecated id]
                            theorem ball_of_forall {α : Sort u_1} {p : αProp} (h : ∀ (x : α), p x) (x : α) :
                            p x
                            @[deprecated forall_imp]
                            theorem forall_of_ball {α : Sort u_1} {p : αProp} {q : αProp} (H : ∀ (x : α), p x) (h : ∀ (x : α), p xq x) (x : α) :
                            q x
                            theorem exists_mem_of_exists {α : Sort u_1} {p : αProp} {q : αProp} (H : ∀ (x : α), p x) :
                            (∃ (x : α), q x)∃ (x : α), ∃ (x_1 : p x), q x
                            theorem exists_of_exists_mem {α : Sort u_1} {p : αProp} {q : αProp} :
                            (∃ (x : α), ∃ (x_1 : p x), q x)∃ (x : α), q x
                            theorem exists₂_imp {α : Sort u_1} {p : αProp} {P : (x : α) → p xProp} {b : Prop} :
                            (∃ (x : α), ∃ (h : p x), P x h)b ∀ (x : α) (h : p x), P x hb
                            @[deprecated exists_mem_of_exists]
                            theorem bex_of_exists {α : Sort u_1} {p : αProp} {q : αProp} (H : ∀ (x : α), p x) :
                            (∃ (x : α), q x)∃ (x : α), ∃ (x_1 : p x), q x

                            Alias of exists_mem_of_exists.

                            @[deprecated exists_of_exists_mem]
                            theorem exists_of_bex {α : Sort u_1} {p : αProp} {q : αProp} :
                            (∃ (x : α), ∃ (x_1 : p x), q x)∃ (x : α), q x

                            Alias of exists_of_exists_mem.

                            @[deprecated exists₂_imp]
                            theorem bex_imp {α : Sort u_1} {p : αProp} {P : (x : α) → p xProp} {b : Prop} :
                            (∃ (x : α), ∃ (h : p x), P x h)b ∀ (x : α) (h : p x), P x hb

                            Alias of exists₂_imp.

                            theorem not_exists_mem {α : Sort u_1} {p : αProp} {P : (x : α) → p xProp} :
                            (¬∃ (x : α), ∃ (h : p x), P x h) ∀ (x : α) (h : p x), ¬P x h
                            theorem not_forall₂_of_exists₂_not {α : Sort u_1} {p : αProp} {P : (x : α) → p xProp} :
                            (∃ (x : α), ∃ (h : p x), ¬P x h)¬∀ (x : α) (h : p x), P x h
                            theorem Decidable.not_forall₂ {α : Sort u_1} {p : αProp} {P : (x : α) → p xProp} [Decidable (∃ (x : α), ∃ (h : p x), ¬P x h)] [(x : α) → (h : p x) → Decidable (P x h)] :
                            (¬∀ (x : α) (h : p x), P x h) ∃ (x : α), ∃ (h : p x), ¬P x h
                            theorem not_forall₂ {α : Sort u_1} {p : αProp} {P : (x : α) → p xProp} :
                            (¬∀ (x : α) (h : p x), P x h) ∃ (x : α), ∃ (h : p x), ¬P x h
                            theorem forall₂_and {α : Sort u_1} {p : αProp} {P : (x : α) → p xProp} {Q : (x : α) → p xProp} :
                            (∀ (x : α) (h : p x), P x h Q x h) (∀ (x : α) (h : p x), P x h) ∀ (x : α) (h : p x), Q x h
                            theorem forall_and_left {α : Sort u_1} [Nonempty α] (q : Prop) (p : αProp) :
                            (∀ (x : α), q p x) q ∀ (x : α), p x
                            theorem forall_and_right {α : Sort u_1} [Nonempty α] (p : αProp) (q : Prop) :
                            (∀ (x : α), p x q) (∀ (x : α), p x) q
                            theorem exists_mem_or {α : Sort u_1} {p : αProp} {P : (x : α) → p xProp} {Q : (x : α) → p xProp} :
                            (∃ (x : α), ∃ (h : p x), P x h Q x h) (∃ (x : α), ∃ (h : p x), P x h) ∃ (x : α), ∃ (h : p x), Q x h
                            theorem forall₂_or_left {α : Sort u_1} {r : αProp} {p : αProp} {q : αProp} :
                            (∀ (x : α), p x q xr x) (∀ (x : α), p xr x) ∀ (x : α), q xr x
                            theorem exists_mem_or_left {α : Sort u_1} {r : αProp} {p : αProp} {q : αProp} :
                            (∃ (x : α), ∃ (x_1 : p x q x), r x) (∃ (x : α), ∃ (x_1 : p x), r x) ∃ (x : α), ∃ (x_1 : q x), r x
                            theorem dite_eq_iff {α : Sort u_1} {P : Prop} [Decidable P] {c : α} {A : Pα} {B : ¬Pα} :
                            dite P A B = c (∃ (h : P), A h = c) ∃ (h : ¬P), B h = c
                            theorem ite_eq_iff {α : Sort u_1} {P : Prop} [Decidable P] {a : α} {b : α} {c : α} :
                            (if P then a else b) = c P a = c ¬P b = c
                            theorem eq_ite_iff {α : Sort u_1} {P : Prop} [Decidable P] {a : α} {b : α} {c : α} :
                            (a = if P then b else c) P a = b ¬P a = c
                            theorem dite_eq_iff' {α : Sort u_1} {P : Prop} [Decidable P] {c : α} {A : Pα} {B : ¬Pα} :
                            dite P A B = c (∀ (h : P), A h = c) ∀ (h : ¬P), B h = c
                            theorem ite_eq_iff' {α : Sort u_1} {P : Prop} [Decidable P] {a : α} {b : α} {c : α} :
                            (if P then a else b) = c (Pa = c) (¬Pb = c)
                            theorem dite_ne_left_iff {α : Sort u_1} {P : Prop} [Decidable P] {a : α} {B : ¬Pα} :
                            dite P (fun (x : P) => a) B a ∃ (h : ¬P), a B h
                            theorem dite_ne_right_iff {α : Sort u_1} {P : Prop} [Decidable P] {b : α} {A : Pα} :
                            (dite P A fun (x : ¬P) => b) b ∃ (h : P), A h b
                            theorem ite_ne_left_iff {α : Sort u_1} {P : Prop} [Decidable P] {a : α} {b : α} :
                            (if P then a else b) a ¬P a b
                            theorem ite_ne_right_iff {α : Sort u_1} {P : Prop} [Decidable P] {a : α} {b : α} :
                            (if P then a else b) b P a b
                            theorem Ne.dite_eq_left_iff {α : Sort u_1} {P : Prop} [Decidable P] {a : α} {B : ¬Pα} (h : ∀ (h : ¬P), a B h) :
                            dite P (fun (x : P) => a) B = a P
                            theorem Ne.dite_eq_right_iff {α : Sort u_1} {P : Prop} [Decidable P] {b : α} {A : Pα} (h : ∀ (h : P), A h b) :
                            (dite P A fun (x : ¬P) => b) = b ¬P
                            theorem Ne.ite_eq_left_iff {α : Sort u_1} {P : Prop} [Decidable P] {a : α} {b : α} (h : a b) :
                            (if P then a else b) = a P
                            theorem Ne.ite_eq_right_iff {α : Sort u_1} {P : Prop} [Decidable P] {a : α} {b : α} (h : a b) :
                            (if P then a else b) = b ¬P
                            theorem Ne.dite_ne_left_iff {α : Sort u_1} {P : Prop} [Decidable P] {a : α} {B : ¬Pα} (h : ∀ (h : ¬P), a B h) :
                            dite P (fun (x : P) => a) B a ¬P
                            theorem Ne.dite_ne_right_iff {α : Sort u_1} {P : Prop} [Decidable P] {b : α} {A : Pα} (h : ∀ (h : P), A h b) :
                            (dite P A fun (x : ¬P) => b) b P
                            theorem Ne.ite_ne_left_iff {α : Sort u_1} {P : Prop} [Decidable P] {a : α} {b : α} (h : a b) :
                            (if P then a else b) a ¬P
                            theorem Ne.ite_ne_right_iff {α : Sort u_1} {P : Prop} [Decidable P] {a : α} {b : α} (h : a b) :
                            (if P then a else b) b P
                            theorem dite_eq_or_eq {α : Sort u_1} (P : Prop) [Decidable P] {A : Pα} {B : ¬Pα} :
                            (∃ (h : P), dite P A B = A h) ∃ (h : ¬P), dite P A B = B h
                            theorem ite_eq_or_eq {α : Sort u_1} (P : Prop) [Decidable P] (a : α) (b : α) :
                            (if P then a else b) = a (if P then a else b) = b
                            theorem apply_dite₂ {α : Sort u_3} {β : Sort u_4} {γ : Sort u_5} (f : αβγ) (P : Prop) [Decidable P] (a : Pα) (b : ¬Pα) (c : Pβ) (d : ¬Pβ) :
                            f (dite P a b) (dite P c d) = if h : P then f (a h) (c h) else f (b h) (d h)

                            A two-argument function applied to two dites is a dite of that two-argument function applied to each of the branches.

                            theorem apply_ite₂ {α : Sort u_3} {β : Sort u_4} {γ : Sort u_5} (f : αβγ) (P : Prop) [Decidable P] (a : α) (b : α) (c : β) (d : β) :
                            f (if P then a else b) (if P then c else d) = if P then f a c else f b d

                            A two-argument function applied to two ites is a ite of that two-argument function applied to each of the branches.

                            theorem dite_apply {α : Sort u_1} {σ : αSort u_2} (P : Prop) [Decidable P] (f : P(a : α) → σ a) (g : ¬P(a : α) → σ a) (a : α) :
                            dite P f g a = if h : P then f h a else g h a

                            A 'dite' producing a Pi type Π a, σ a, applied to a value a : α is a dite that applies either branch to a.

                            theorem ite_apply {α : Sort u_1} {σ : αSort u_2} (P : Prop) [Decidable P] (f : (a : α) → σ a) (g : (a : α) → σ a) (a : α) :
                            (if P then f else g) a = if P then f a else g a

                            A 'ite' producing a Pi type Π a, σ a, applied to a value a : α is a ite that applies either branch to a.

                            theorem ite_and {α : Sort u_1} (P : Prop) (Q : Prop) [Decidable P] [Decidable Q] (a : α) (b : α) :
                            (if P Q then a else b) = if P then if Q then a else b else b
                            theorem dite_dite_comm {α : Sort u_1} (P : Prop) (Q : Prop) [Decidable P] [Decidable Q] {A : Pα} {B : Qα} {C : ¬P¬Qα} (h : P¬Q) :
                            (if p : P then A p else if q : Q then B q else C p q) = if q : Q then B q else if p : P then A p else C p q
                            theorem ite_ite_comm {α : Sort u_1} (P : Prop) (Q : Prop) [Decidable P] [Decidable Q] (a : α) (b : α) {c : α} (h : P¬Q) :
                            (if P then a else if Q then b else c) = if Q then b else if P then a else c
                            theorem ite_prop_iff_or {P : Prop} {Q : Prop} {R : Prop} [Decidable P] :
                            (if P then Q else R) P Q ¬P R
                            theorem dite_prop_iff_or {P : Prop} {Q : PProp} {R : ¬PProp} [Decidable P] :
                            dite P Q R (∃ (p : P), Q p) ∃ (p : ¬P), R p
                            theorem ite_prop_iff_and {P : Prop} {Q : Prop} {R : Prop} [Decidable P] :
                            (if P then Q else R) (PQ) (¬PR)
                            theorem dite_prop_iff_and {P : Prop} {Q : PProp} {R : ¬PProp} [Decidable P] :
                            dite P Q R (∀ (h : P), Q h) ∀ (h : ¬P), R h
                            theorem not_beq_of_ne {α : Type u_1} [BEq α] [LawfulBEq α] {a : α} {b : α} (ne : a b) :
                            ¬(a == b) = true
                            theorem beq_eq_decide {α : Type u_1} [BEq α] [LawfulBEq α] {a : α} {b : α} :
                            (a == b) = decide (a = b)
                            theorem beq_ext {α : Type u_1} (inst1 : BEq α) (inst2 : BEq α) (h : ∀ (x y : α), (x == y) = (x == y)) :
                            inst1 = inst2
                            theorem lawful_beq_subsingleton {α : Type u_1} (inst1 : BEq α) (inst2 : BEq α) [LawfulBEq α] [LawfulBEq α] :
                            inst1 = inst2