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.

@[implicit_reducible, instance 10]

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

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

theorem congr_heq {α β : Sort u_2} {γ : Sort u_3} {f : α → γ} {g : β → γ} {x : α} {y : β} (h₁ : f ≍ g) (h₂ : x ≍ y) : f x = g y

theorem congr_arg_heq {α : Sort u_1} {β : α → Sort u_2} (f : (a : α) → β a) {a₁ a₂ : α} : a₁ = a₂ → f a₁ ≍ f a₂

theorem dcongr_heq {α₁ α₂ : Sort u} {β₁ : α₁ → Sort v} {β₂ : α₂ → Sort v} {f₁ : (a : α₁) → β₁ a} {f₂ : (a : α₂) → β₂ a} {a₁ : α₁} {a₂ : α₂} (hargs : a₁ ≍ a₂) (ht : ∀ (t₁ : α₁) (t₂ : α₂), t₁ ≍ t₂ → β₁ t₁ = β₂ t₂) (hf : α₁ = α₂ → β₁ ≍ β₂ → f₁ ≍ f₂) : f₁ a₁ ≍ f₂ a₂

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

def LibraryNote.«fact_non-instances» : Batteries.Util.LibraryNote

In most cases, we should not have global instances of Fact; typeclass search is not an advanced proof search engine, and adding any such instance has the potential to cause slowdowns everywhere. We instead declare them as lemmata and make them local instances as required.

theorem Fact.elim {p : Prop} (h : Fact p) : p

theorem fact_iff {p : Prop} : Fact p ↔ p

@[implicit_reducible]

instance instDecidableFact {p : Prop} [Decidable p] : Decidable (Fact 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.

Declarations about propositional connectives

Declarations about implies

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

Alias of imp_congr.

@[deprecated Classical.imp_iff_right_iff (since := "2026-01-30")]

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

Alias of Classical.imp_iff_right_iff.

@[deprecated Classical.and_or_imp (since := "2026-01-30")]

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

Alias of Classical.and_or_imp.

theorem Function.mt {a 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.

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 q : Prop} (hpq : p → q) (hnpq : ¬p → q) : q

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

Alias of by_contradiction.

def LibraryNote.decidable_namespace : Batteries.Util.LibraryNote

In most of mathlib, we use the law of excluded middle (LEM) and the axiom of choice (AC) freely. The Decidable namespace contains versions of lemmas from the root namespace that explicitly attempt to avoid the axiom of choice, usually by adding decidability assumptions on the inputs.

You can check if a lemma uses the axiom of choice by using #print axioms foo and seeing if Classical.choice appears in the list.

def LibraryNote.decidable_arguments : Batteries.Util.LibraryNote

As mathlib is primarily classical, if the type signature of a def or lemma does not require any Decidable instances to state, it is preferable not to introduce any Decidable instances that are needed in the proof as arguments, but rather to use the classical tactic as needed.

In the other direction, when Decidable instances do appear in the type signature, it is better to use explicitly introduced ones rather than allowing Lean to automatically infer classical ones, as these may cause instance mismatch errors later.

Various types that (almost) never have provable decidability, such as ℝ, Set α or Ideal R, are given global DecidableEq instances, so that no decidable arguments have to be provided.

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 b : Prop} : ¬(a → b) → a

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

Alias of Decidable.not_imp_symm.

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

theorem not_imp_comm {a 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 : a) (a : b), c) ↔ ∀ (a_1 : b) (a : a), c

theorem Iff.not {a b : Prop} (h : a ↔ b) : ¬a ↔ ¬b

Alias of not_congr.

theorem Iff.not_left {a b : Prop} (h : a ↔ ¬b) : ¬a ↔ b

theorem Iff.not_right {a 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'

def Xor' (a b : Prop) : Prop

Xor' a b is the exclusive-or of propositions.

theorem xor_def {a b : Prop} : Xor' a b ↔ a ∧ ¬b ∨ b ∧ ¬a

@[implicit_reducible]

instance instDecidableXor' {a b : Prop} [Decidable a] [Decidable b] : Decidable (Xor' a b)

@[simp]

theorem xor_true : Xor' True = Not

@[simp]

theorem xor_false : Xor' False = id

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

instance instCommutativeXor' : Std.Commutative Xor'

@[simp]

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

@[simp]

theorem xor_not_left {a b : Prop} : Xor' (¬a) b ↔ (a ↔ b)

@[simp]

theorem xor_not_right {a b : Prop} : Xor' a ¬b ↔ (a ↔ b)

theorem xor_not_not {a b : Prop} : Xor' (¬a) ¬b ↔ Xor' a b

theorem Xor'.or {a b : Prop} (h : Xor' a b) : a ∨ b

Declarations about and

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

Alias of and_congr.

theorem And.rotate {a b 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 c b d : Prop} (h₁ : a ↔ c) (h₂ : b ↔ d) : a ∨ b ↔ c ∨ d

Alias of or_congr.

theorem Or.rotate {a b c : Prop} : a ∨ b ∨ c → b ∨ c ∨ a

Alias of the forward direction of or_rotate.

theorem Or.elim3 {a b c d : Prop} (h : a ∨ b ∨ c) (ha : a → d) (hb : b → d) (hc : c → d) : d

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

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

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

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

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

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

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

@[deprecated Classical.imp_and_neg_imp_iff (since := "2026-01-30")]

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

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

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

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

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

Declarations about distributivity

Declarations about iff

theorem Iff.iff {p₁ p₂ q₁ 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 b c : Prop} : a → b ∨ c ↔ (a → b) ∨ (a → c)

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

@[deprecated Classical.not_imp (since := "2026-01-30")]

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

Alias of Classical.not_imp.

theorem peirce (a b : Prop) : ((a → b) → a) → a

theorem not_iff_not {a b : Prop} : (¬a ↔ ¬b) ↔ (a ↔ b)

theorem not_iff_comm {a b : Prop} : (¬a ↔ b) ↔ (¬b ↔ a)

theorem not_iff {a b : Prop} : ¬(a ↔ b) ↔ (¬a ↔ b)

theorem iff_not_comm {a b : Prop} : (a ↔ ¬b) ↔ (b ↔ ¬a)

theorem iff_iff_and_or_not_and_not {a b : Prop} : (a ↔ b) ↔ a ∧ b ∨ ¬a ∧ ¬b

theorem iff_iff_not_or_and_or_not {a b : Prop} : (a ↔ b) ↔ (¬a ∨ b) ∧ (a ∨ ¬b)

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

De Morgan's laws

theorem not_and_or {a 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 b : Prop} : a ∨ b ↔ ¬(¬a ∧ ¬b)

theorem and_iff_not_or_not {a b : Prop} : a ∧ b ↔ ¬(¬a ∨ ¬b)

@[simp]

theorem not_xor (P Q : Prop) : ¬Xor' P Q ↔ (P ↔ Q)

theorem xor_iff_not_iff (P Q : Prop) : Xor' P Q ↔ ¬(P ↔ Q)

theorem xor_iff_iff_not {a b : Prop} : Xor' a b ↔ (a ↔ ¬b)

theorem xor_iff_not_iff' {a b : Prop} : Xor' a b ↔ (¬a ↔ b)

theorem xor_iff_or_and_not_and (a b : Prop) : Xor' a b ↔ (a ∨ b) ∧ ¬(a ∧ b)

Declarations about equality

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

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 rec_heq_of_heq {α : Sort u_2} {β : Sort u_1} {a b : α} {C : α → Sort u_1} {x : C a} {y : β} (e : a = b) (h : x ≍ y) : e ▸ x ≍ y

@[simp]

theorem cast_heq_iff_heq {α β γ : Sort u_1} (e : α = β) (a : α) (c : γ) : cast e a ≍ c ↔ a ≍ c

@[simp]

theorem heq_cast_iff_heq {α β γ : Sort u_1} (e : β = γ) (a : α) (b : β) : a ≍ cast e b ↔ a ≍ b

theorem heq_of_eq_cast {α β : Sort u} {a : α} {b : β} (e : β = α) : a = cast e b → a ≍ b

theorem eq_cast_iff_heq {α β : Sort u} {e : β = α} {a : α} {b : β} : a = cast e b ↔ a ≍ b

theorem heq_iff_exists_eq_cast {α β : Sort u} {a : α} {b : β} : a ≍ b ↔ ∃ (h : β = α), a = cast h b

theorem heq_iff_exists_cast_eq {α β : Sort u} {a : α} {b : β} : a ≍ b ↔ ∃ (h : α = β), cast h a = b

Declarations about quantifiers

theorem forall₂_imp {α : Sort u_1} {β : α → Sort u_2} {p 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 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 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 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

@[deprecated forall_comm (since := "2026-03-25")]

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

Alias of forall_comm.

theorem forall₂_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₂

@[deprecated forall₂_comm (since := "2026-03-25")]

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₂

Alias of forall₂_comm.

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_comm.

theorem imp_forall_iff_forall (A : Prop) (B : A → Prop) : (A → ∀ (h : A), B h) ↔ ∀ (h : A), B h

@[deprecated exists_comm (since := "2026-03-25")]

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

Alias of exists_comm.

theorem exists_and_exists_comm {α : Sort u_1} {β : Sort u_2} {P : α → Prop} {Q : β → Prop} : ((∃ (a : α), P a) ∧ ∃ (b : β), Q b) ↔ ∃ (a : α) (b : β), P a ∧ Q b

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

theorem forall₃_true_iff {α : Sort u_1} {β : α → Sort u_3} {γ : (a : α) → β a → Sort u_4} : (∀ (a : α) (b : β a) (a : γ a b), True) ↔ True

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_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

The constant function witnesses that there exists a function sending a given term to a given term.

This is sometimes useful in simp to discharge side conditions.

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

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)

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

@[simp]

theorem forall_and_index {p q : Prop} {r : p ∧ q → Prop} : (∀ (h : p ∧ q), r h) ↔ ∀ (hp : p) (hq : q), r ⋯

theorem forall_and_index' {p q : Prop} {r : p → q → Prop} : (∀ (hp : p) (hq : q), r hp hq) ↔ ∀ (h : p ∧ q), r ⋯ ⋯

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_iff_of_forall {p : Prop} {q : p → Prop} (h : ∀ (h : p), q h) : (∃ (h : p), q h) ↔ p

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

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

theorem imp_congr_ctx_eq {a b c 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 b : Prop} : (a ↔ b) → a = b

Alias of propext.

theorem iff_eq_eq {a 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.

Classical lemmas

@[implicit_reducible]

noncomputable def Classical.dec (p : Prop) : Decidable p

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

@[implicit_reducible]

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

Any predicate p is decidable classically.

@[implicit_reducible]

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

Any relation p is decidable classically.

@[implicit_reducible]

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

Any type α has decidable equality classically.

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.

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

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

A version of byContradiction that uses types instead of propositions.

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

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

@[simp]

theorem Classical.choose_eq {α : Sort u_1} (a : α) : ⋯.choose = a

@[simp]

theorem Classical.choose_eq' {α : Sort u_1} (a : α) : ⋯.choose = a

theorem Classical.axiom_of_choice {α : Sort u} {β : α → Sort v} {r : (x : α) → β x → Prop} (h : ∀ (x : α), ∃ (y : β x), r x y) : ∃ (f : (x : α) → β x), ∀ (x : α), r x (f x)

Alias of Classical.axiomOfChoice.

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

Alias of Classical.byCases.

theorem Classical.by_contradiction {p : Prop} (h : ¬p → False) : p

Alias of Classical.byContradiction.

theorem Classical.prop_complete (a : Prop) : a = True ∨ a = False

Alias of Classical.propComplete.

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.

Declarations about bounded quantifiers

theorem bex_def {α : Sort u_1} {p q : α → Prop} : (∃ (x : α) (_ : 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

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

theorem exists_mem_of_exists {α : Sort u_1} {p q : α → Prop} (H : ∀ (x : α), p x) : (∃ (x : α), q x) → ∃ (x : α) (_ : p x), q x

theorem exists_of_exists_mem {α : Sort u_1} {p q : α → Prop} : (∃ (x : α) (_ : p x), q x) → ∃ (x : α), q x

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 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 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 p 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 p q : α → Prop} : (∃ (x : α) (_ : p x ∨ q x), r x) ↔ (∃ (x : α) (_ : p x), r x) ∨ ∃ (x : α) (_ : 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 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 apply_ite_left {α : Sort u_3} {β : Sort u_4} {γ : Sort u_5} (f : α → β → γ) (P : Prop) [Decidable P] (x y : α) (z : β) : f (if P then x else y) z = if P then f x z else f y z

theorem ite_and {α : Sort u_1} (P Q : Prop) [Decidable P] (a b : α) [Decidable Q] : (if P ∧ Q then a else b) = if P then if Q then a else b else b

theorem ite_or {α : Sort u_1} (P Q : Prop) [Decidable P] (a b : α) [Decidable Q] : (if P ∨ Q then a else b) = if P then a else if Q then a else b

theorem dite_dite_comm {α : Sort u_1} (P Q : Prop) [Decidable P] {A : P → α} [Decidable Q] {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 Q : Prop) [Decidable P] (a b : α) {c : α} [Decidable Q] (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 Q R : Prop} [Decidable P] : (if P then Q else R) ↔ P ∧ Q ∨ ¬P ∧ R

theorem dite_prop_iff_or {P : Prop} [Decidable P] {Q : P → Prop} {R : ¬P → Prop} : dite P Q R ↔ (∃ (p : P), Q p) ∨ ∃ (p : ¬P), R p

theorem ite_prop_iff_and {P Q R : Prop} [Decidable P] : (if P then Q else R) ↔ (P → Q) ∧ (¬P → R)

theorem dite_prop_iff_and {P : Prop} [Decidable P] {Q : P → Prop} {R : ¬P → Prop} : dite P Q R ↔ (∀ (h : P), Q h) ∧ ∀ (h : ¬P), R h

theorem if_ctx_congr {α : Sort u_1} {P Q : Prop} [Decidable P] [Decidable Q] {x y u v : α} (h_c : P ↔ Q) (h_t : Q → x = u) (h_e : ¬Q → y = v) : (if P then x else y) = if Q then u else v

theorem if_congr {α : Sort u_1} {P Q : Prop} [Decidable P] [Decidable Q] {x y u v : α} (h_c : P ↔ Q) (h_t : x = u) (h_e : y = v) : (if P then x else y) = if Q then u else v

theorem Function.Injective.ite {α : Sort u_3} {β : Sort u_4} {p : β → Prop} [DecidablePred p] {g : β → α} (hg : Injective g) {f : β → α} (hf : Injective f) (h : ∀ (x y : β), g x = f y → x = y) : Injective fun (x : β) => if p x then g x else f x

Membership

theorem Membership.mem.ne_of_notMem {α : 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_notMem' {α : 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 mem_dite {α : Type u_1} {β : Type u_2} [Membership α β] {p : Prop} [Decidable p] {a : α} {s : p → β} {t : ¬p → β} : (a ∈ if h : p then s h else t h) ↔ (∀ (h : p), a ∈ s h) ∧ ∀ (h : ¬p), a ∈ t h

theorem dite_mem {α : Type u_1} {β : Type u_2} [Membership α β] {p : Prop} [Decidable p] {a : p → α} {b : ¬p → α} {s : β} : (if h : p then a h else b h) ∈ s ↔ (∀ (h : p), a h ∈ s) ∧ ∀ (h : ¬p), b h ∈ s

theorem mem_ite {α : Type u_1} {β : Type u_2} [Membership α β] {p : Prop} [Decidable p] {a : α} {s t : β} : (a ∈ if p then s else t) ↔ (p → a ∈ s) ∧ (¬p → a ∈ t)

theorem ite_mem {α : Type u_1} {β : Type u_2} [Membership α β] {p : Prop} [Decidable p] {a b : α} {s : β} : (if p then a else b) ∈ s ↔ (p → a ∈ s) ∧ (¬p → b ∈ s)

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 α] [DecidableEq α] (a b : α) : (a == b) = decide (a = b)

Alias of Bool.beq_eq_decide_eq.

@[simp]

theorem beq_eq_beq {α : Type u_1} {β : Type u_2} [BEq α] [LawfulBEq α] [BEq β] [LawfulBEq β] {a₁ a₂ : α} {b₁ b₂ : β} : (a₁ == a₂) = (b₁ == b₂) ↔ (a₁ = a₂ ↔ b₁ = b₂)

theorem beq_ext {α : Type u_1} (inst1 inst2 : BEq α) (h : ∀ (x y : α), (x == y) = (x == y)) : inst1 = inst2

theorem beq_ext_iff {α : Type u_1} {inst1 inst2 : BEq α} : inst1 = inst2 ↔ ∀ (x y : α), (x == y) = (x == y)

theorem lawful_beq_subsingleton {α : Type u_1} (inst1 inst2 : BEq α) [LawfulBEq α] [LawfulBEq α] : inst1 = inst2