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

@[instance 10]

instance decidableEq_of_subsingleton {α : Sort u_1} [Subsingleton α] : DecidableEq α

Equations

• decidableEq_of_subsingleton a b = isTrue ⋯

instance instSubsingletonSubtype_mathlib {α : Sort u_1} [Subsingleton α] (p : α → Prop) : Subsingleton (Subtype p)

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} : Function.Injective ULift.down

@[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} : Function.Injective PLift.down

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

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

instance instDecidableFact {p : Prop} [Decidable p] : Decidable (Fact p)

Equations

• instDecidableFact = decidable_of_iff p ⋯

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

• Function.swap₂ f i₂ j₂ i₁ j₁ = f i₁ j₁ i₂ j₂

Declarations about propositional connectives

Declarations about implies

instance instIsReflPropIff : IsRefl Prop Iff

Equations

• instIsReflPropIff = ⋯

instance instIsTransPropIff : IsTrans Prop Iff

Equations

• instIsTransPropIff = ⋯

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

Alias of imp_congr.

theorem imp_iff_right_iff {a : Prop} {b : Prop} : (a → b ↔ b) ↔ a ∨ b

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

theorem Function.mt {a : Prop} {b : Prop} : (a → b) → ¬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} : (¬p → False) → p

theorem by_cases {p : Prop} {q : Prop} (hpq : p → q) (hnpq : ¬p → q) : q

theorem by_contra {p : Prop} : (¬p → False) → p

Alias of by_contradiction.

theorem of_not_not {a : Prop} : ¬¬a → a

theorem not_ne_iff {α : Sort u_1} {a : α} {b : α} : ¬a ≠ b ↔ a = b

theorem of_not_imp {a : Prop} {b : Prop} : ¬(a → b) → a

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

Alias of Decidable.not_imp_symm.

theorem Not.imp_symm {a : Prop} {b : Prop} : (¬a → b) → ¬b → a

theorem not_imp_comm {a : Prop} {b : Prop} : ¬a → b ↔ ¬b → a

@[simp]

theorem not_imp_self {a : Prop} : ¬a → a ↔ a

theorem Imp.swap {a : Sort u_1} {b : Sort u_2} {c : Prop} : a → b → c ↔ b → a → c

theorem Iff.not {a : Prop} {b : Prop} (h : a ↔ b) : ¬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]

theorem xor_true : Xor' True = Not

@[simp]

theorem xor_false : Xor' False = id

theorem xor_comm (a : Prop) (b : Prop) : Xor' a b = Xor' b a

instance instCommutativeXor' : Std.Commutative Xor'

Equations

• instCommutativeXor' = ⋯

@[simp]

theorem xor_self (a : Prop) : Xor' a a = False

@[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 ∧ c → b ∧ 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 ∨ c → b ∨ 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 : a → d) (hb : b → d) (hc : c → d) : d

theorem Or.imp3 {a : Prop} {b : Prop} {d : Prop} {e : Prop} {c : Prop} {f : Prop} (had : a → d) (hbe : b → e) (hcf : c → f) : a ∨ b ∨ c → d ∨ e ∨ f

theorem not_or_of_imp {a : Prop} {b : Prop} : (a → b) → ¬a ∨ b

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

theorem or_not_of_imp {a : Prop} {b : Prop} : (a → b) → b ∨ ¬a

theorem imp_iff_not_or {a : Prop} {b : Prop} : a → b ↔ ¬a ∨ b

theorem imp_iff_or_not {b : Prop} {a : Prop} : b → a ↔ a ∨ ¬b

theorem not_imp_not {a : Prop} {b : Prop} : ¬a → ¬b ↔ b → a

theorem imp_and_neg_imp_iff (p : Prop) (q : Prop) : (p → q) ∧ (¬p → q) ↔ q

theorem Function.mtr {a : Prop} {b : Prop} : (¬a → ¬b) → b → a

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} : a → b ∨ c ↔ (a → b) ∨ (a → c)

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

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

theorem peirce (a : Prop) (b : Prop) : ((a → b) → 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) ↔ a → b

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 ∈ s → a ≠ 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 ∈ t → s ≠ 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 b → p a b) ↔ ∀ (a b : α), s a → s b → p a b

theorem forall_mem_comm {α : Type u_1} {β : Type u_2} [Membership α β] {s : β} {p : α → α → Prop} : (∀ (a : α), a ∈ s → ∀ (b : α), b ∈ s → p a b) ↔ ∀ (a b : α), a ∈ s → b ∈ s → p a b

@[deprecated forall_cond_comm]

theorem ball_cond_comm {α : Sort u_1} {s : α → Prop} {p : α → α → Prop} : (∀ (a : α), s a → ∀ (b : α), s b → p a b) ↔ ∀ (a b : α), s a → s b → p 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 ∈ s → p a b) ↔ ∀ (a b : α), a ∈ s → b ∈ s → p 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} : Equivalence Eq

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) : h ▸ z = cast ⋯ z

theorem eqRec_heq' {α : Sort u_1} {a' : α} {motive : (a : α) → a' = a → Sort u_2} (p : motive a' ⋯) {a : α} (t : a' = a) : HEq (t ▸ p) 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 (e ▸ x) 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 (e ▸ x) 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 (e ▸ y) ↔ 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 : α) → β a → Prop} {q : (a : α) → β a → Prop} (h : ∀ (a : α) (b : β a), p a b → q a b) : (∀ (a : α) (b : β a), p a b) → ∀ (a : α) (b : β a), q a b

theorem forall₃_imp {α : Sort u_1} {β : α → Sort u_2} {γ : (a : α) → β a → Sort u_3} {p : (a : α) → (b : β a) → γ a b → Prop} {q : (a : α) → (b : β a) → γ a b → Prop} (h : ∀ (a : α) (b : β a) (c : γ a b), p a b c → q a b c) : (∀ (a : α) (b : β a) (c : γ a b), p a b c) → ∀ (a : α) (b : β a) (c : γ a b), q a b c

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

theorem Exists₃.imp {α : Sort u_1} {β : α → Sort u_2} {γ : (a : α) → β a → Sort u_3} {p : (a : α) → (b : β a) → γ a b → Prop} {q : (a : α) → (b : β a) → γ a b → Prop} (h : ∀ (a : α) (b : β a) (c : γ a b), p a b c → q a b c) : (∃ (a : α), ∃ (b : β a), ∃ (c : γ a b), p a b c) → ∃ (a : α), ∃ (b : β a), ∃ (c : γ a b), q a b c

theorem forall_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 : α), p → q 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 x → b

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 : α), β a → True) ↔ True

theorem forall₃_true_iff {α : Sort u_1} {β : α → Sort u_3} {γ : (a : α) → β a → Sort u_4} : (∀ (a : α) (b : β a), γ a b → True) ↔ 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 ≠ a → p b) ↔ ∀ (b : α), p b

theorem and_forall_ne {α : Sort u_1} {p : α → Prop} (a : α) : (p a ∧ ∀ (b : α), b ≠ a → p 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 = b → p b) ↔ ∀ (a : α), p (f a)

theorem forall_eq_apply_imp_iff' {α : Sort u_1} {β : Sort u_2} {f : α → β} {p : β → Prop} : (∀ (a : α) (b : β), b = f a → p 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 ∧ q → Prop} : (∃ (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 : b → Prop} : Exists p → b

theorem Exists.snd {b : Prop} {p : b → Prop} (h : Exists p) : p ⋯

theorem Prop.exists_iff {p : Prop → Prop} : (∃ (h : Prop), p h) ↔ p False ∨ p True

theorem Prop.forall_iff {p : Prop → Prop} : (∀ (h : Prop), p h) ↔ p False ∧ p True

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

theorem exists_iff_of_forall {p : Prop} {q : p → Prop} (h : ∀ (h : p), q h) : (∃ (h : p), q h) ↔ p

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

theorem exists_prop_of_false {p : Prop} {q : p → Prop} : ¬p → ¬∃ (h' : p), q h'

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

@[simp]

theorem exists_true_left (p : True → Prop) : (∃ (x : True), p x) ↔ p True.intro

See IsEmpty.exists_iff for the False version.

theorem forall_prop_congr {p : Prop} {p' : Prop} {q : p → Prop} {q' : p → Prop} (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 : p → Prop} {q' : p → Prop} (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) : (a → b) = (c → d)

theorem imp_congr_ctx_eq {a : Prop} {b : Prop} {c : Prop} {d : Prop} (h₁ : a = c) (h₂ : c → b = d) : (a → b) = (c → d)

theorem eq_true_intro {a : Prop} (h : a) : a = True

theorem eq_false_intro {a : Prop} (h : ¬a) : a = False

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

• @Iff.eq = @propext

theorem iff_eq_eq {a : Prop} {b : Prop} : (a ↔ b) = (a = b)

@[simp]

theorem forall_true_left (p : True → Prop) : (∀ (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 x → Prop} {b : Prop} (h₂ : ∃! x : α, ∃! h : p x, q x h) (h₁ : ∀ (x : α) (h : p x), q x h → (∀ (y : α) (hy : p y), q y hy → y = x) → b) : b

theorem ExistsUnique.intro₂ {α : Sort u_3} {p : α → Sort u_4} [∀ (x : α), Subsingleton (p x)] {q : (x : α) → p x → Prop} (w : α) (hp : p w) (hq : q w hp) (H : ∀ (y : α) (hy : p y), q y hy → y = w) : ∃! x : α, ∃! hx : p x, q x hx

theorem ExistsUnique.exists₂ {α : Sort u_3} {p : α → Sort u_4} {q : (x : α) → p x → Prop} (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 x → Prop} (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) : Decidable p

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

Equations

• Classical.dec p = inferInstance

noncomputable def Classical.decPred {α : Sort u_1} (p : α → Prop) : DecidablePred p

Any predicate p is decidable classically.

Equations

• Classical.decPred p = inferInstance

noncomputable def Classical.decRel {α : Sort u_1} (p : α → α → Prop) : DecidableRel p

Any relation p is decidable classically.

Equations

• Classical.decRel p = inferInstance

noncomputable def Classical.decEq (α : Sort u_2) : DecidableEq α

Any type α has decidable equality classically.

Equations

• Classical.decEq α = inferInstance

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

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

Equations

• Classical.existsCases H0 H = if h : ∃ (a : α), p a then H (Classical.choose h) ⋯ else H0

theorem Classical.some_spec₂ {α : Sort u_2} {p : α → Prop} {h : ∃ (a : α), p a} (q : α → Prop) (hpq : ∀ (a : α), p a → q a) : q (Classical.choose h)

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

• Classical.subtype_of_exists h = ⟨Classical.choose h, ⋯⟩

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

A version of byContradiction that uses types instead of propositions.

Equations

• Classical.byContradiction' H = Classical.choice ⋯

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

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

Equations

• Classical.choice_of_byContradiction' contra H = contra ⋯

noncomputable def Exists.classicalRecOn {α : Sort u_1} {p : α → Prop} (h : ∃ (a : α), p a) {C : Sort u_2} (H : (a : α) → p a → C) : 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

• h.classicalRecOn H = H (Classical.choose h) ⋯

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 x → Prop} {b : Prop} : (∃ (x : α), ∃ (h : p x), P x h) → (∀ (a : α) (h : p a), P a h → b) → b

theorem BEx.intro {α : Sort u_1} {p : α → Prop} {P : (x : α) → p x → Prop} (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 : α) → β a → Prop} {q : (a : α) → β a → Prop} (h : ∀ (a : α) (b : β a), p a b ↔ q a b) : (∀ (a : α) (b : β a), p a b) ↔ ∀ (a : α) (b : β a), q a b

Alias of forall₂_congr.

@[deprecated exists₂_congr]

theorem bex_congr {α : Sort u_1} {β : α → Sort u_2} {p : (a : α) → β a → Prop} {q : (a : α) → β a → Prop} (h : ∀ (a : α) (b : β a), p a b ↔ q a b) : (∃ (a : α), ∃ (b : β a), p a b) ↔ ∃ (a : α), ∃ (b : β a), q a b

Alias of exists₂_congr.

theorem BAll.imp_right {α : Sort u_1} {p : α → Prop} {P : (x : α) → p x → Prop} {Q : (x : α) → p x → Prop} (H : ∀ (x : α) (h : p x), P x h → Q 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 x → Prop} {Q : (x : α) → p x → Prop} (H : ∀ (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 BAll.imp_left {α : Sort u_1} {r : α → Prop} {p : α → Prop} {q : α → Prop} (H : ∀ (x : α), p x → q x) (h₁ : ∀ (x : α), q x → r x) (x : α) (h : p x) : r x

theorem BEx.imp_left {α : Sort u_1} {r : α → Prop} {p : α → Prop} {q : α → Prop} (H : ∀ (x : α), p x → q 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 x → q 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 x → Prop} {b : Prop} : (∃ (x : α), ∃ (h : p x), P x h) → b ↔ ∀ (x : α) (h : p x), P x h → b

@[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 x → Prop} {b : Prop} : (∃ (x : α), ∃ (h : p x), P x h) → b ↔ ∀ (x : α) (h : p x), P x h → b

Alias of exists₂_imp.

theorem not_exists_mem {α : Sort u_1} {p : α → Prop} {P : (x : α) → p x → Prop} : (¬∃ (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 x → Prop} : (∃ (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 x → Prop} [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 x → Prop} : (¬∀ (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 x → Prop} {Q : (x : α) → p x → Prop} : (∀ (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 x → Prop} {Q : (x : α) → p x → Prop} : (∃ (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 x → r x) ↔ (∀ (x : α), p x → r x) ∧ ∀ (x : α), q x → r 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 ↔ (P → a = c) ∧ (¬P → b = 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 : P → Prop} {R : ¬P → Prop} [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) ↔ (P → Q) ∧ (¬P → R)

theorem dite_prop_iff_and {P : Prop} {Q : P → Prop} {R : ¬P → Prop} [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