Mathlib.Logic.Basic

hidden abbrev

{α : Sort*} {a : α}

Full source

/-- 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. -/
abbrev hidden {α : Sort*} {a : α} := a

Implicit Identity Function

Informal description

Given a type `α` and an element `a : α`, the function `hidden` returns `a` unchanged, with its main argument `a` being implicit in the function definition.

decidableEq_of_subsingleton instance

[Subsingleton α] : DecidableEq α

Full source

instance (priority := 10) decidableEq_of_subsingleton [Subsingleton α] : DecidableEq α :=
  fun a b ↦ isTrue (Subsingleton.elim a b)

Decidable Equality for Subsingleton Types

Informal description

For any type $\alpha$ with at most one element (i.e., a subsingleton), the equality relation on $\alpha$ is decidable.

instSubsingletonSubtype_mathlib instance

[Subsingleton α] (p : α → Prop) : Subsingleton (Subtype p)

Full source

instance [Subsingleton α] (p : α → Prop) : Subsingleton (Subtype p) :=
  ⟨fun ⟨x, _⟩ ⟨y, _⟩ ↦ by cases Subsingleton.elim x y; rfl⟩

Subsingleton Property of Subtypes of a Subsingleton

Informal description

For any type $\alpha$ with at most one element (i.e., a subsingleton) and any predicate $p$ on $\alpha$, the subtype $\{x : \alpha \mid p(x)\}$ is also a subsingleton.

congr_heq theorem

{α β γ : Sort _} {f : α → γ} {g : β → γ} {x : α} {y : β} (h₁ : HEq f g) (h₂ : HEq x y) : f x = g y

Full source

theorem congr_heq {α β γ : Sort _} {f : α → γ} {g : β → γ} {x : α} {y : β}
    (h₁ : HEq f g) (h₂ : HEq x y) : f x = g y := by
  cases h₂; cases h₁; rfl

Heterogeneous Congruence for Function Application

Informal description

For any types $\alpha$, $\beta$, $\gamma$, functions $f : \alpha \to \gamma$ and $g : \beta \to \gamma$, and elements $x : \alpha$ and $y : \beta$, if $f$ is heterogeneously equal to $g$ and $x$ is heterogeneously equal to $y$, then $f(x) = g(y)$.

congr_arg_heq theorem

{β : α → Sort*} (f : ∀ a, β a) : ∀ {a₁ a₂ : α}, a₁ = a₂ → HEq (f a₁) (f a₂)

Full source

theorem congr_arg_heq {β : α → Sort*} (f : ∀ a, β a) :
    ∀ {a₁ a₂ : α}, a₁ = a₂ → HEq (f a₁) (f a₂)
  | _, _, rfl => HEq.rfl

Heterogeneous Equality of Function Values at Equal Arguments

Informal description

For any type family $\beta : \alpha \to \text{Sort}^*$ and any dependent function $f : \forall a, \beta a$, if $a_1 = a_2$ for $a_1, a_2 : \alpha$, then the values $f a_1$ and $f a_2$ are heterogeneously equal (denoted as $f a_1 \approx f a_2$).

ne_and_eq_iff_right theorem

{a b c : α} (h : b ≠ c) : a ≠ b ∧ a = c ↔ a = c

Full source

lemma ne_and_eq_iff_right {a b c : α} (h : b ≠ c) : a ≠ ba ≠ b ∧ a = ca ≠ b ∧ a = c ↔ a = c :=
  and_iff_right_of_imp (fun h2 => h2.symm ▸ h.symm)

Equivalence of Inequality and Equality Condition: $a \neq b \land a = c \leftrightarrow a = c$ when $b \neq c$

Informal description

For any elements $a, b, c$ of a type $\alpha$ with $b \neq c$, the conjunction "$a \neq b$ and $a = c$" is equivalent to "$a = c$".

Fact structure

(p : Prop)

Full source

/-- 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. -/
class Fact (p : Prop) : Prop where
  /-- `Fact.out` contains the unwrapped witness for the fact represented by the instance of
  `Fact p`. -/
  out : p

Implicit Proposition Wrapper (`Fact`)

Informal description

The structure `Fact` is a wrapper that allows a proposition `p` to be treated as a type class instance. This is useful in situations where certain propositions need to be passed implicitly to type class resolution, but making the proposition a global class would be undesirable or require significant refactoring. For example, if `p` is the proposition that a natural number is prime, `Fact p` can be used to implicitly pass this information to type class search when needed (e.g., to infer that `ZMod p` is a field), without making `Nat.Prime` a class globally.

Fact.elim theorem

{p : Prop} (h : Fact p) : p

Full source

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

Extraction of Fact-Wrapped Proposition

Informal description

Given a proposition $p$ and a proof $h$ that $p$ holds (wrapped in the `Fact` structure), we can extract the proof that $p$ is true.

fact_iff theorem

{p : Prop} : Fact p ↔ p

Full source

theorem fact_iff {p : Prop} : FactFact p ↔ p := ⟨fun h ↦ h.1, fun h ↦ ⟨h⟩⟩

Equivalence of Fact Wrapper and Proposition

Informal description

For any proposition $p$, the wrapper `Fact p` is equivalent to $p$ itself, i.e., $\text{Fact}(p) \leftrightarrow p$.

instDecidableFact instance

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

Full source

instance {p : Prop} [Decidable p] : Decidable (Fact p) :=
  decidable_of_iff _ fact_iff.symm

Decidability of Fact Wrapper for Decidable Propositions

Informal description

For any proposition $p$ with a decidable instance, the wrapper `Fact p` is also decidable.

Function.swap₂ abbrev

 {ι₁ ι₂ : Sort*} {κ₁ : ι₁ → Sort*} {κ₂ : ι₂ → Sort*} {φ : ∀ i₁, κ₁ i₁ → ∀ i₂, κ₂ i₂ → Sort*}
  (f : ∀ i₁ j₁ i₂ j₂, φ i₁ j₁ i₂ j₂) (i₂ j₂ i₁ j₁) : φ i₁ j₁ i₂ j₂

Full source

/-- Swaps two pairs of arguments to a function. -/
abbrev Function.swap₂ {ι₁ ι₂ : Sort*} {κ₁ : ι₁ → Sort*} {κ₂ : ι₂ → Sort*}
    {φ : ∀ i₁, κ₁ i₁ → ∀ i₂, κ₂ i₂ → Sort*} (f : ∀ i₁ j₁ i₂ j₂, φ i₁ j₁ i₂ j₂)
    (i₂ j₂ i₁ j₁) : φ i₁ j₁ i₂ j₂ := f i₁ j₁ i₂ j₂

Argument Pair Swapping Operation

Informal description

Given a function $f$ that takes four arguments of types $i₁$, $j₁$, $i₂$, $j₂$ (where $j₁$ depends on $i₁$ and $j₂$ depends on $i₂$) and returns a value in type $φ(i₁, j₁, i₂, j₂)$, the operation `Function.swap₂` swaps the first two argument pairs, producing a new function that takes $i₂$, $j₂$, $i₁$, $j₁$ as arguments and returns $φ(i₁, j₁, i₂, j₂)$.

imp_iff_right_iff theorem

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

Full source

theorem imp_iff_right_iff {a b : Prop} : (a → b ↔ b) ↔ a ∨ b :=
  open scoped Classical in Decidable.imp_iff_right_iff

Implication Equivalence: $(a \to b \leftrightarrow b) \leftrightarrow (a \lor b)$

Informal description

For any propositions $a$ and $b$, the equivalence $(a \to b) \leftrightarrow b$ holds if and only if $a \lor b$ holds.

and_or_imp theorem

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

Full source

theorem and_or_imp {a b c : Prop} : a ∧ ba ∧ b ∨ (a → c)a ∧ b ∨ (a → c) ↔ a → b ∨ c :=
  open scoped Classical in Decidable.and_or_imp

Equivalence between $(a ∧ b) ∨ (a → c)$ and $a → (b ∨ c)$

Informal description

For any propositions $a$, $b$, and $c$, the statement $a ∧ b ∨ (a → c)$ is equivalent to $a → b ∨ c$.

Function.mt theorem

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

Full source

/-- Provide modus tollens (`mt`) as dot notation for implications. -/
protected theorem Function.mt {a b : Prop} : (a → b) → ¬b → ¬a := mt

Modus Tollens: $(a \to b) \to (\neg b \to \neg a)$

Informal description

For any propositions $a$ and $b$, if $a$ implies $b$ and $b$ is false, then $a$ is false. In other words, $(a \to b) \to (\neg b \to \neg a)$.

dec_em' theorem

(p : Prop) [Decidable p] : ¬p ∨ p

Full source

theorem dec_em' (p : Prop) [Decidable p] : ¬p¬p ∨ p := (dec_em p).symm

Decidable Law of Excluded Middle: $\neg p \lor p$ for decidable $p$

Informal description

For any decidable proposition $p$, either $p$ is false or $p$ is true.

em' theorem

(p : Prop) : ¬p ∨ p

Full source

theorem em' (p : Prop) : ¬p¬p ∨ p := (em p).symm

Law of Excluded Middle: $\neg p \lor p$

Informal description

For any proposition $p$, either $p$ is false or $p$ is true.

or_not theorem

{p : Prop} : p ∨ ¬p

Full source

theorem or_not {p : Prop} : p ∨ ¬p := em _

Law of Excluded Middle for Proposition $p$

Informal description

For any proposition $p$, either $p$ holds or $\neg p$ holds.

Decidable.ne_or_eq theorem

{α : Sort*} (x y : α) [Decidable (x = y)] : x ≠ y ∨ x = y

Full source

theorem Decidable.ne_or_eq {α : Sort*} (x y : α) [Decidable (x = y)] : x ≠ yx ≠ y ∨ x = y :=
  dec_em' <| x = y

Decidable Law of Excluded Middle for Equality: $x \neq y \lor x = y$

Informal description

For any two elements $x$ and $y$ of a type $\alpha$ where the equality $x = y$ is decidable, either $x$ is not equal to $y$ or $x$ is equal to $y$.

ne_or_eq theorem

{α : Sort*} (x y : α) : x ≠ y ∨ x = y

Full source

theorem ne_or_eq {α : Sort*} (x y : α) : x ≠ yx ≠ y ∨ x = y := em' <| x = y

Law of Excluded Middle for Equality: $x \neq y \lor x = y$

Informal description

For any two elements $x$ and $y$ of a type $\alpha$, either $x$ is not equal to $y$ or $x$ is equal to $y$.

by_contradiction theorem

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

Full source

theorem by_contradiction {p : Prop} : (¬p → False) → p :=
  open scoped Classical in Decidable.byContradiction

Proof by Contradiction: $\neg p \to \text{False}$ implies $p$

Informal description

For any proposition $p$, if assuming $\neg p$ leads to a contradiction (i.e., $\neg p \to \text{False}$), then $p$ holds.

by_cases theorem

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

Full source

theorem by_cases {p q : Prop} (hpq : p → q) (hnpq : ¬p → q) : q :=
  open scoped Classical in if hp : p then hpq hp else hnpq hp

Proof by Cases: $q$ holds whether $p$ or $\neg p$ holds

Informal description

For any propositions $p$ and $q$, if $p$ implies $q$ and $\neg p$ also implies $q$, then $q$ holds.

of_not_not theorem

{a : Prop} : ¬¬a → a

Full source

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

Double Negation Elimination

Informal description

For any proposition $a$, the double negation of $a$ implies $a$, i.e., $\neg \neg a \to a$.

not_ne_iff theorem

{α : Sort*} {a b : α} : ¬a ≠ b ↔ a = b

Full source

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

Double Negation of Inequality is Equality

Informal description

For any elements $a$ and $b$ of a type $\alpha$, the statement "$a$ is not not equal to $b$" is equivalent to "$a$ equals $b$". In other words, $\neg (a \neq b) \leftrightarrow a = b$.

of_not_imp theorem

: ¬(a → b) → a

Full source

theorem of_not_imp : ¬(a → b) → a := open scoped Classical in Decidable.of_not_imp

Negation of Implication Implies Antecedent

Informal description

For any propositions $a$ and $b$, if the implication $a \to b$ does not hold, then $a$ must be true.

Not.imp_symm theorem

: (¬a → b) → ¬b → a

Full source

theorem Not.imp_symm : (¬a → b) → ¬b → a := open scoped Classical in Not.decidable_imp_symm

Contrapositive of Negated Implication: $(\neg a \to b) \to (\neg b \to a)$

Informal description

For any propositions $a$ and $b$, if the implication $\neg a \to b$ holds, then $\neg b$ implies $a$. In other words, $(\neg a \to b) \to (\neg b \to a)$.

not_imp_comm theorem

: ¬a → b ↔ ¬b → a

Full source

theorem not_imp_comm : ¬a¬a → b ↔ ¬b → a := open scoped Classical in Decidable.not_imp_comm

Commutativity of Negated Implications: $\neg a \to b \leftrightarrow \neg b \to a$

Informal description

For any propositions $a$ and $b$, the implication $\neg a \to b$ holds if and only if the implication $\neg b \to a$ holds.

not_imp_self theorem

: ¬a → a ↔ a

Full source

@[simp] theorem not_imp_self : ¬a¬a → a ↔ a := open scoped Classical in Decidable.not_imp_self

Equivalence of Implication and Proposition: $(\neg a \to a) \leftrightarrow a$

Informal description

For any proposition $a$, the statement "if not $a$ then $a$" is equivalent to $a$ itself, i.e., $(\neg a \to a) \leftrightarrow a$.

Imp.swap theorem

{a b : Sort*} {c : Prop} : a → b → c ↔ b → a → c

Full source

theorem Imp.swap {a b : Sort*} {c : Prop} : a → b → c ↔ b → a → c :=
  ⟨fun h x y ↦ h y x, fun h x y ↦ h y x⟩

Swapping Premises in Nested Implication

Informal description

For any propositions $a$, $b$, and $c$, the implication $a \to b \to c$ holds if and only if the implication $b \to a \to c$ holds. In other words, the order of the premises in a nested implication can be swapped without changing the truth value of the implication.

Iff.not_left theorem

(h : a ↔ ¬b) : ¬a ↔ b

Full source

theorem Iff.not_left (h : a ↔ ¬b) : ¬a¬a ↔ b := h.not.trans not_not

Negation of Equivalent to Not Implies Equivalent to Original

Informal description

For any propositions $a$ and $b$, if $a$ is equivalent to $\neg b$, then $\neg a$ is equivalent to $b$, i.e., $(a \leftrightarrow \neg b) \rightarrow (\neg a \leftrightarrow b)$.

Iff.not_right theorem

(h : ¬a ↔ b) : a ↔ ¬b

Full source

theorem Iff.not_right (h : ¬a¬a ↔ b) : a ↔ ¬b := not_not.symm.trans h.not

Negation Equivalence Swap: $(\neg a \leftrightarrow b) \rightarrow (a \leftrightarrow \neg b)$

Informal description

For any propositions $a$ and $b$, if $\neg a$ is equivalent to $b$, then $a$ is equivalent to $\neg b$.

Iff.ne theorem

{α β : Sort*} {a b : α} {c d : β} : (a = b ↔ c = d) → (a ≠ b ↔ c ≠ d)

Full source

protected lemma Iff.ne {α β : Sort*} {a b : α} {c d : β} : (a = b ↔ c = d) → (a ≠ ba ≠ b ↔ c ≠ d) :=
  Iff.not

Equivalence of Inequalities under Equivalence of Equalities

Informal description

For any types $\alpha$ and $\beta$, and elements $a, b \in \alpha$ and $c, d \in \beta$, if the equality $a = b$ is equivalent to $c = d$, then the inequality $a \neq b$ is equivalent to $c \neq d$.

Iff.ne_left theorem

{α β : Sort*} {a b : α} {c d : β} : (a = b ↔ c ≠ d) → (a ≠ b ↔ c = d)

Full source

lemma Iff.ne_left {α β : Sort*} {a b : α} {c d : β} : (a = b ↔ c ≠ d) → (a ≠ ba ≠ b ↔ c = d) :=
  Iff.not_left

Equivalence of Equality and Inequality: $(a = b \leftrightarrow c \neq d) \rightarrow (a \neq b \leftrightarrow c = d)$

Informal description

For any types $\alpha$ and $\beta$, and elements $a, b \in \alpha$ and $c, d \in \beta$, if the equality $a = b$ is equivalent to the inequality $c \neq d$, then the inequality $a \neq b$ is equivalent to the equality $c = d$.

Iff.ne_right theorem

{α β : Sort*} {a b : α} {c d : β} : (a ≠ b ↔ c = d) → (a = b ↔ c ≠ d)

Full source

lemma Iff.ne_right {α β : Sort*} {a b : α} {c d : β} : (a ≠ ba ≠ b ↔ c = d) → (a = b ↔ c ≠ d) :=
  Iff.not_right

Equivalence of Equality and Inequality under Equivalence of Inequality and Equality: $(a \neq b \leftrightarrow c = d) \rightarrow (a = b \leftrightarrow c \neq d)$

Informal description

For any types $\alpha$ and $\beta$, and elements $a, b \in \alpha$ and $c, d \in \beta$, if the inequality $a \neq b$ is equivalent to the equality $c = d$, then the equality $a = b$ is equivalent to the inequality $c \neq d$.

Xor' definition

(a b : Prop)

Full source

/-- `Xor' a b` is the exclusive-or of propositions. -/
def Xor' (a b : Prop) := (a ∧ ¬b) ∨ (b ∧ ¬a)

Exclusive-or of propositions

Informal description

The exclusive-or of two propositions $ a $ and $ b $, denoted $ \text{Xor}'\,a\,b $, is defined as $(a \land \neg b) \lor (b \land \neg a)$. This means that exactly one of $ a $ or $ b $ is true, but not both.

instDecidableXor' instance

[Decidable a] [Decidable b] : Decidable (Xor' a b)

Full source

instance [Decidable a] [Decidable b] : Decidable (Xor' a b) := inferInstanceAs (Decidable (Or ..))

Decidability of Exclusive-or for Decidable Propositions

Informal description

For any two decidable propositions $a$ and $b$, the exclusive-or $a \mathbin{\text{Xor}'} b$ is also decidable.

xor_true theorem

: Xor' True = Not

Full source

@[simp] theorem xor_true : Xor' True = Not := by
  simp +unfoldPartialApp [Xor']

Exclusive-or with True is Negation

Informal description

The exclusive-or operation with `True` as the first argument is equivalent to the negation function, i.e., $\text{Xor}'(\text{True}, b) = \neg b$ for any proposition $b$.

xor_false theorem

: Xor' False = id

Full source

@[simp] theorem xor_false : Xor' False = id := by ext; simp [Xor']

Exclusive-or with False is the Identity Function

Informal description

The exclusive-or operation with `False` as the first argument is equivalent to the identity function on propositions, i.e., $\text{Xor}'(\text{False}, b) = b$ for any proposition $b$.

xor_comm theorem

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

Full source

theorem xor_comm (a b : Prop) : Xor' a b = Xor' b a := by simp [Xor', and_comm, or_comm]

Commutativity of Exclusive-Or

Informal description

For any two propositions $a$ and $b$, the exclusive-or operation is commutative, i.e., $\text{Xor}'(a, b) = \text{Xor}'(b, a)$.

instCommutativeXor' instance

: Std.Commutative Xor'

Full source

instance : Std.Commutative Xor' := ⟨xor_comm⟩

Commutativity of Exclusive-Or

Informal description

The exclusive-or operation on propositions is commutative.

xor_self theorem

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

Full source

@[simp] theorem xor_self (a : Prop) : Xor' a a = False := by simp [Xor']

Exclusive-or with Self is False

Informal description

For any proposition $a$, the exclusive-or of $a$ with itself is false, i.e., $a \oplus a = \text{False}$.

xor_not_left theorem

: Xor' (¬a) b ↔ (a ↔ b)

Full source

@[simp] theorem xor_not_left : Xor'Xor' (¬a) b ↔ (a ↔ b) := by by_cases a <;> simp [*]

Exclusive-or with Negated Left Operand: $\neg a \oplus b \leftrightarrow (a \leftrightarrow b)$

Informal description

For any propositions $a$ and $b$, the exclusive-or of $\neg a$ and $b$ is equivalent to the biconditional of $a$ and $b$, i.e., $\neg a \oplus b \leftrightarrow (a \leftrightarrow b)$.

xor_not_right theorem

: Xor' a (¬b) ↔ (a ↔ b)

Full source

@[simp] theorem xor_not_right : Xor'Xor' a (¬b) ↔ (a ↔ b) := by by_cases a <;> simp [*]

Exclusive-or with Negated Right Operand: $a \oplus \neg b \leftrightarrow (a \leftrightarrow b)$

Informal description

For any propositions $a$ and $b$, the exclusive-or of $a$ and $\neg b$ is equivalent to the biconditional of $a$ and $b$, i.e., $a \oplus \neg b \leftrightarrow (a \leftrightarrow b)$.

xor_not_not theorem

: Xor' (¬a) (¬b) ↔ Xor' a b

Full source

theorem xor_not_not : Xor'Xor' (¬a) (¬b) ↔ Xor' a b := by simp [Xor', or_comm, and_comm]

Negation Preserves Exclusive-Or: $\neg a \oplus \neg b \leftrightarrow a \oplus b$

Informal description

For any propositions $a$ and $b$, the exclusive-or of $\neg a$ and $\neg b$ is equivalent to the exclusive-or of $a$ and $b$, i.e., $(\neg a \oplus \neg b) \leftrightarrow (a \oplus b)$.

Xor'.or theorem

(h : Xor' a b) : a ∨ b

Full source

protected theorem Xor'.or (h : Xor' a b) : a ∨ b := h.imp And.left And.left

Exclusive-or implies disjunction

Informal description

For any propositions $a$ and $b$, if $a$ and $b$ are in an exclusive-or relationship (i.e., exactly one of them is true), then at least one of $a$ or $b$ is true.

and_symm_right theorem

{α : Sort*} (a b : α) (p : Prop) : p ∧ a = b ↔ p ∧ b = a

Full source

theorem and_symm_right {α : Sort*} (a b : α) (p : Prop) : p ∧ a = bp ∧ a = b ↔ p ∧ b = a := by simp [eq_comm]

Symmetry of equality in conjunction: $p \land (a = b) \leftrightarrow p \land (b = a)$

Informal description

For any type $\alpha$ and elements $a, b \in \alpha$, and any proposition $p$, the conjunction $p \land (a = b)$ is equivalent to $p \land (b = a)$.

and_symm_left theorem

{α : Sort*} (a b : α) (p : Prop) : a = b ∧ p ↔ b = a ∧ p

Full source

theorem and_symm_left {α : Sort*} (a b : α) (p : Prop) : a = b ∧ pa = b ∧ p ↔ b = a ∧ p := by simp [eq_comm]

Symmetry of equality in left conjunction: $(a = b) \land p \leftrightarrow (b = a) \land p$

Informal description

For any type $\alpha$ and elements $a, b \in \alpha$, and any proposition $p$, the conjunction $(a = b) \land p$ is equivalent to $(b = a) \land p$.

Or.elim3 theorem

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

Full source

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

Triple Disjunction Elimination: $(a ∨ b ∨ c) ∧ (a → d) ∧ (b → d) ∧ (c → d) → d$

Informal description

For any propositions $a$, $b$, $c$, and $d$, if $a ∨ b ∨ c$ holds, and $a$ implies $d$, $b$ implies $d$, and $c$ implies $d$, then $d$ holds.

Or.imp3 theorem

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

Full source

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

Implication Preserved Under Triple Disjunction

Informal description

For any propositions $a, b, c, d, e, f$, if there are implications $a \to d$, $b \to e$, and $c \to f$, then the statement $a \lor b \lor c$ implies $d \lor e \lor f$.

not_or_of_imp theorem

: (a → b) → ¬a ∨ b

Full source

theorem not_or_of_imp : (a → b) → ¬a¬a ∨ b := open scoped Classical in Decidable.not_or_of_imp

Implication implies Negation or Conclusion

Informal description

For any propositions $a$ and $b$, if $a$ implies $b$, then either $a$ is false or $b$ is true. In other words, $(a \to b) \to (\neg a \lor b)$.

Decidable.or_not_of_imp theorem

[Decidable a] (h : a → b) : b ∨ ¬a

Full source

protected theorem Decidable.or_not_of_imp [Decidable a] (h : a → b) : b ∨ ¬a :=
  dite _ (Or.inlOr.inl ∘ h) Or.inr

Implication implies Disjunction with Negation for Decidable Propositions

Informal description

For any decidable proposition $a$ and any proposition $b$, if $a$ implies $b$, then either $b$ holds or $a$ does not hold. In other words, $(a \to b) \to (b ∨ ¬a)$.

or_not_of_imp theorem

: (a → b) → b ∨ ¬a

Full source

theorem or_not_of_imp : (a → b) → b ∨ ¬a := open scoped Classical in Decidable.or_not_of_imp

Implication implies Disjunction with Negation: $(a \to b) \to (b \lor \neg a)$

Informal description

For any propositions $a$ and $b$, if $a$ implies $b$, then either $b$ holds or $a$ does not hold. In other words, $(a \to b) \to (b \lor \neg a)$.

imp_iff_not_or theorem

: a → b ↔ ¬a ∨ b

Full source

theorem imp_iff_not_or : a → b ↔ ¬a ∨ b := open scoped Classical in Decidable.imp_iff_not_or

Implication as Disjunction: $a \to b \leftrightarrow \neg a \lor b$

Informal description

For any propositions $a$ and $b$, the implication $a \to b$ is equivalent to $\neg a \lor b$.

imp_iff_or_not theorem

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

Full source

theorem imp_iff_or_not {b a : Prop} : b → a ↔ a ∨ ¬b :=
  open scoped Classical in Decidable.imp_iff_or_not

Implication as Disjunction with Negation: $b \to a \leftrightarrow a \lor \neg b$

Informal description

For any propositions $a$ and $b$, the implication $b \to a$ is equivalent to the disjunction $a \lor \neg b$.

not_imp_not theorem

: ¬a → ¬b ↔ b → a

Full source

theorem not_imp_not : ¬a¬a → ¬b ↔ b → a := open scoped Classical in Decidable.not_imp_not

Contrapositive Equivalence: $\neg a \to \neg b \leftrightarrow b \to a$

Informal description

For any propositions $a$ and $b$, the implication $\neg a \to \neg b$ is equivalent to $b \to a$.

imp_and_neg_imp_iff theorem

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

Full source

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

Equivalence of Implications and Conclusion: $(p \to q) \land (\neg p \to q) \leftrightarrow q$

Informal description

For any propositions $p$ and $q$, the conjunction of $(p \to q)$ and $(\neg p \to q)$ is equivalent to $q$. In other words, $(p \to q) \land (\neg p \to q) \leftrightarrow q$.

Function.mtr theorem

: (¬a → ¬b) → b → a

Full source

/-- Provide the reverse of modus tollens (`mt`) as dot notation for implications. -/
protected theorem Function.mtr : (¬a → ¬b) → b → a := not_imp_not.mp

Reverse Modus Tollens: $(\neg a \to \neg b) \to (b \to a)$

Informal description

For any propositions $a$ and $b$, if the implication $\neg a \to \neg b$ holds, then $b$ implies $a$.

or_congr_left' theorem

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

Full source

theorem or_congr_left' {c a b : Prop} (h : ¬c → (a ↔ b)) : a ∨ ca ∨ c ↔ b ∨ c :=
  open scoped Classical in Decidable.or_congr_left' h

Left Disjunction Equivalence under Implication of Negation

Informal description

For any propositions $a$, $b$, and $c$, if $\neg c$ implies that $a$ is equivalent to $b$, then $a \lor c$ is equivalent to $b \lor c$.

or_congr_right' theorem

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

Full source

theorem or_congr_right' {c : Prop} (h : ¬a → (b ↔ c)) : a ∨ ba ∨ b ↔ a ∨ c :=
  open scoped Classical in Decidable.or_congr_right' h

Right Disjunction Equivalence under Implication

Informal description

For any proposition $c$, if $\neg a$ implies that $b$ is equivalent to $c$, then the disjunction $a \lor b$ is equivalent to $a \lor c$.

iff_mpr_iff_true_intro theorem

{P : Prop} (h : P) : Iff.mpr (iff_true_intro h) True.intro = h

Full source

theorem iff_mpr_iff_true_intro {P : Prop} (h : P) : Iff.mpr (iff_true_intro h) True.intro = h := rfl

Backward Implication of True Equivalence Preserves Proof

Informal description

For any proposition $P$ and a proof $h$ of $P$, the backward implication of the equivalence $(P \leftrightarrow \text{True})$ applied to the trivial proof $\text{True.intro}$ yields $h$ itself. In other words, $\text{Iff.mpr}(P \leftrightarrow \text{True}, \text{True.intro}) = h$.

imp_or theorem

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

Full source

theorem imp_or {a b c : Prop} : a → b ∨ c ↔ (a → b) ∨ (a → c) :=
  open scoped Classical in Decidable.imp_or

Implication Distributes Over Disjunction: $a \to (b \lor c) \leftrightarrow (a \to b) \lor (a \to c)$

Informal description

For any propositions $a$, $b$, and $c$, the implication $a \to (b \lor c)$ is equivalent to $(a \to b) \lor (a \to c)$.

imp_or' theorem

{a : Sort*} {b c : Prop} : a → b ∨ c ↔ (a → b) ∨ (a → c)

Full source

theorem imp_or' {a : Sort*} {b c : Prop} : a → b ∨ c ↔ (a → b) ∨ (a → c) :=
  open scoped Classical in Decidable.imp_or'

Implication Distributes Over Disjunction: $a → (b ∨ c) ↔ (a → b) ∨ (a → c)$

Informal description

For any type `a` and propositions `b` and `c`, the implication `a → b ∨ c` is equivalent to `(a → b) ∨ (a → c)`.

not_imp theorem

: ¬(a → b) ↔ a ∧ ¬b

Full source

theorem not_imp : ¬(a → b)¬(a → b) ↔ a ∧ ¬b := open scoped Classical in Decidable.not_imp_iff_and_not

Negation of Implication is Conjunction of Antecedent and Negation of Consequent

Informal description

For any propositions $a$ and $b$, the negation of the implication $a \to b$ is equivalent to the conjunction of $a$ and the negation of $b$, i.e., $\neg(a \to b) \leftrightarrow (a \land \neg b)$.

peirce theorem

(a b : Prop) : ((a → b) → a) → a

Full source

theorem peirce (a b : Prop) : ((a → b) → a) → a := open scoped Classical in Decidable.peirce _ _

Peirce's Law

Informal description

For any propositions $a$ and $b$, the implication $((a \to b) \to a) \to a$ holds.

not_iff_not theorem

: (¬a ↔ ¬b) ↔ (a ↔ b)

Full source

theorem not_iff_not : (¬a ↔ ¬b) ↔ (a ↔ b) := open scoped Classical in Decidable.not_iff_not

Negation Preserves Equivalence: $(\neg a \leftrightarrow \neg b) \leftrightarrow (a \leftrightarrow b)$

Informal description

For any propositions $a$ and $b$, the equivalence $\neg a \leftrightarrow \neg b$ holds if and only if $a \leftrightarrow b$ holds.

not_iff_comm theorem

: (¬a ↔ b) ↔ (¬b ↔ a)

Full source

theorem not_iff_comm : (¬a ↔ b) ↔ (¬b ↔ a) := open scoped Classical in Decidable.not_iff_comm

Commutativity of Negation in Biconditional: $(\neg a \leftrightarrow b) \leftrightarrow (\neg b \leftrightarrow a)$

Informal description

For any propositions $a$ and $b$, the equivalence $(\neg a \leftrightarrow b)$ holds if and only if $(\neg b \leftrightarrow a)$ holds.

not_iff theorem

: ¬(a ↔ b) ↔ (¬a ↔ b)

Full source

theorem not_iff : ¬(a ↔ b)¬(a ↔ b) ↔ (¬a ↔ b) := open scoped Classical in Decidable.not_iff

Negation of Biconditional Equivalence

Informal description

For any propositions $a$ and $b$, the negation of their biconditional is equivalent to the biconditional of the negation of $a$ and $b$, i.e., $\neg(a \leftrightarrow b) \leftrightarrow (\neg a \leftrightarrow b)$.

iff_not_comm theorem

: (a ↔ ¬b) ↔ (b ↔ ¬a)

Full source

theorem iff_not_comm : (a ↔ ¬b) ↔ (b ↔ ¬a) := open scoped Classical in Decidable.iff_not_comm

Commutativity of Biconditional with Negation: $(a \leftrightarrow \neg b) \leftrightarrow (b \leftrightarrow \neg a)$

Informal description

For any propositions $a$ and $b$, the equivalence $(a \leftrightarrow \neg b)$ holds if and only if $(b \leftrightarrow \neg a)$ holds.

iff_iff_and_or_not_and_not theorem

: (a ↔ b) ↔ a ∧ b ∨ ¬a ∧ ¬b

Full source

theorem iff_iff_and_or_not_and_not : (a ↔ b) ↔ a ∧ b ∨ ¬a ∧ ¬b :=
  open scoped Classical in Decidable.iff_iff_and_or_not_and_not

Biconditional as Conjunction or Negated Conjunction

Informal description

For any propositions $a$ and $b$, the biconditional $a \leftrightarrow b$ is equivalent to the disjunction of $a \land b$ and $\neg a \land \neg b$.

iff_iff_not_or_and_or_not theorem

: (a ↔ b) ↔ (¬a ∨ b) ∧ (a ∨ ¬b)

Full source

theorem iff_iff_not_or_and_or_not : (a ↔ b) ↔ (¬a ∨ b) ∧ (a ∨ ¬b) :=
  open scoped Classical in Decidable.iff_iff_not_or_and_or_not

Equivalence Characterization via Disjunctions: $a \leftrightarrow b \leftrightarrow (\neg a \lor b) \land (a \lor \neg b)$

Informal description

For any propositions $a$ and $b$, the equivalence $a \leftrightarrow b$ holds if and only if both $(\neg a \lor b)$ and $(a \lor \neg b)$ hold.

not_and_not_right theorem

: ¬(a ∧ ¬b) ↔ a → b

Full source

theorem not_and_not_right : ¬(a ∧ ¬b)¬(a ∧ ¬b) ↔ a → b :=
  open scoped Classical in Decidable.not_and_not_right

Negation of Conjunction with Negation is Equivalent to Implication

Informal description

For any propositions $a$ and $b$, the statement $\neg(a \land \neg b)$ is equivalent to $a \to b$.

not_and_or theorem

: ¬(a ∧ b) ↔ ¬a ∨ ¬b

Full source

/-- One of **de Morgan's laws**: the negation of a conjunction is logically equivalent to the
disjunction of the negations. -/
theorem not_and_or : ¬(a ∧ b)¬(a ∧ b) ↔ ¬a ∨ ¬b := open scoped Classical in Decidable.not_and_iff_not_or_not

De Morgan's Law: $\neg(a \land b) \leftrightarrow \neg a \lor \neg b$

Informal description

For any propositions $a$ and $b$, the negation of their conjunction is logically equivalent to the disjunction of their negations. That is, $\neg(a \land b) \leftrightarrow \neg a \lor \neg b$.

or_iff_not_and_not theorem

: a ∨ b ↔ ¬(¬a ∧ ¬b)

Full source

theorem or_iff_not_and_not : a ∨ ba ∨ b ↔ ¬(¬a ∧ ¬b) :=
  open scoped Classical in Decidable.or_iff_not_not_and_not

Disjunction Equivalence to Negated Conjunction of Negations

Informal description

For any propositions $a$ and $b$, the disjunction $a \lor b$ holds if and only if it is not the case that both $\lnot a$ and $\lnot b$ hold, i.e., $a \lor b \leftrightarrow \lnot(\lnot a \land \lnot b)$.

and_iff_not_or_not theorem

: a ∧ b ↔ ¬(¬a ∨ ¬b)

Full source

theorem and_iff_not_or_not : a ∧ ba ∧ b ↔ ¬(¬a ∨ ¬b) :=
  open scoped Classical in Decidable.and_iff_not_not_or_not

Conjunction as Negation of Disjunction of Negations

Informal description

For any propositions $a$ and $b$, the conjunction $a \land b$ holds if and only if it is not the case that either $\neg a$ or $\neg b$ holds, i.e., $a \land b \leftrightarrow \neg(\neg a \lor \neg b)$.

not_xor theorem

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

Full source

@[simp] theorem not_xor (P Q : Prop) : ¬Xor' P Q¬Xor' P Q ↔ (P ↔ Q) := by
  simp only [not_and, Xor', not_or, not_not, ← iff_iff_implies_and_implies]

Negation of Exclusive-or is Equivalent to Biconditional

Informal description

For any propositions $P$ and $Q$, the negation of their exclusive-or is equivalent to their biconditional, i.e., $\neg (P \oplus Q) \leftrightarrow (P \leftrightarrow Q)$.

xor_iff_not_iff theorem

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

Full source

theorem xor_iff_not_iff (P Q : Prop) : Xor'Xor' P Q ↔ ¬ (P ↔ Q) := (not_xor P Q).not_right

Exclusive-or as Negation of Biconditional: $P \oplus Q \leftrightarrow \neg (P \leftrightarrow Q)$

Informal description

For any propositions $P$ and $Q$, the exclusive-or of $P$ and $Q$ is equivalent to the negation of their biconditional, i.e., $P \oplus Q \leftrightarrow \neg (P \leftrightarrow Q)$.

xor_iff_iff_not theorem

: Xor' a b ↔ (a ↔ ¬b)

Full source

theorem xor_iff_iff_not : Xor'Xor' a b ↔ (a ↔ ¬b) := by simp only [← @xor_not_right a, not_not]

Exclusive-or as Biconditional with Negation: $a \oplus b \leftrightarrow (a \leftrightarrow \neg b)$

Informal description

For any propositions $a$ and $b$, the exclusive-or $a \oplus b$ holds if and only if $a$ is equivalent to the negation of $b$, i.e., $a \oplus b \leftrightarrow (a \leftrightarrow \neg b)$.

xor_iff_not_iff' theorem

: Xor' a b ↔ (¬a ↔ b)

Full source

theorem xor_iff_not_iff' : Xor'Xor' a b ↔ (¬a ↔ b) := by simp only [← @xor_not_left _ b, not_not]

Exclusive-or as Negation Equivalence: $a \oplus b \leftrightarrow (\neg a \leftrightarrow b)$

Informal description

For any propositions $a$ and $b$, the exclusive-or $a \oplus b$ holds if and only if the negation of $a$ is equivalent to $b$, i.e., $a \oplus b \leftrightarrow (\neg a \leftrightarrow b)$.

xor_iff_or_and_not_and theorem

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

Full source

theorem xor_iff_or_and_not_and (a b : Prop) : Xor'Xor' a b ↔ (a ∨ b) ∧ (¬ (a ∧ b)) := by
  rw [Xor', or_and_right, not_and_or, and_or_left, and_not_self_iff, false_or,
    and_or_left, and_not_self_iff, or_false]

Exclusive-or as Disjunction with Non-Conjunction: $a \mathbin{\text{Xor}'} b \leftrightarrow (a \lor b) \land \neg(a \land b)$

Informal description

For any propositions $a$ and $b$, the exclusive-or $a \mathbin{\text{Xor}'} b$ holds if and only if either $a$ or $b$ is true but not both, i.e., $(a \lor b) \land \neg(a \land b)$.

mem_dite theorem

 {a : α} {s : p → β} {t : ¬p → β} : (a ∈ if h : p then s h else t h) ↔ (∀ h, a ∈ s h) ∧ (∀ h, a ∈ t h)

Full source

theorem mem_dite {a : α} {s : p → β} {t : ¬p → β} :
    (a ∈ if h : p then s h else t h) ↔ (∀ h, a ∈ s h) ∧ (∀ h, a ∈ t h) := by
  by_cases h : p <;> simp [h]

Membership in Dependent Conditional Set

Informal description

For any element $a$ of type $\alpha$ and any dependent sets $s : p \to \beta$ and $t : \lnot p \to \beta$, the statement that $a$ belongs to the dependent if-then-else set (i.e., $a \in \text{if } h : p \text{ then } s(h) \text{ else } t(h)$) is equivalent to the conjunction of: 1. For all $h$ where $p$ holds, $a$ belongs to $s(h)$ 2. For all $h$ where $\lnot p$ holds, $a$ belongs to $t(h)$

dite_mem theorem

 {a : p → α} {b : ¬p → α} {s : β} : (if h : p then a h else b h) ∈ s ↔ (∀ h, a h ∈ s) ∧ (∀ h, b h ∈ s)

Full source

theorem dite_mem {a : p → α} {b : ¬p → α} {s : β} :
    (if h : p then a h else b h) ∈ s(if h : p then a h else b h) ∈ s ↔ (∀ h, a h ∈ s) ∧ (∀ h, b h ∈ s) := by
  by_cases h : p <;> simp [h]

Membership of Dependent If-Then-Else in Set

Informal description

For any predicate `p`, functions `a : p → α` and `b : ¬p → α`, and set `s : β`, the element `if h : p then a h else b h` belongs to `s` if and only if for all `h : p`, `a h ∈ s` and for all `h : ¬p`, `b h ∈ s`.

mem_ite theorem

{a : α} {s t : β} : (a ∈ if p then s else t) ↔ (p → a ∈ s) ∧ (¬p → a ∈ t)

Full source

theorem mem_ite {a : α} {s t : β} : (a ∈ if p then s else t) ↔ (p → a ∈ s) ∧ (¬p → a ∈ t) :=
  mem_dite

Membership in Conditional Set

Informal description

For any element $a$ of type $\alpha$ and sets $s, t$ of type $\beta$, the statement that $a$ belongs to the if-then-else set (i.e., $a \in \text{if } p \text{ then } s \text{ else } t$) is equivalent to the conjunction of: 1. If $p$ holds, then $a \in s$ 2. If $\lnot p$ holds, then $a \in t$

ite_mem theorem

{a b : α} {s : β} : (if p then a else b) ∈ s ↔ (p → a ∈ s) ∧ (¬p → b ∈ s)

Full source

theorem ite_mem {a b : α} {s : β} : (if p then a else b) ∈ s(if p then a else b) ∈ s ↔ (p → a ∈ s) ∧ (¬p → b ∈ s) :=
  dite_mem

Membership of Conditional Element in Set: $\text{if } p \text{ then } a \text{ else } b \in s \leftrightarrow (p \to a \in s) \land (\neg p \to b \in s)$

Informal description

For any elements $a, b$ of type $\alpha$, any set $s$ of type $\beta$, and any proposition $p$, the element $\text{if } p \text{ then } a \text{ else } b$ belongs to $s$ if and only if $p$ implies $a \in s$ and $\neg p$ implies $b \in s$.

forall_cond_comm theorem

 {α} {s : α → Prop} {p : α → α → Prop} : (∀ a, s a → ∀ b, s b → p a b) ↔ ∀ a b, s a → s b → p a b

Full source

theorem forall_cond_comm {α} {s : α → Prop} {p : α → α → Prop} :
    (∀ a, s a → ∀ b, s b → p a b) ↔ ∀ a b, s a → s b → p a b :=
  ⟨fun h a b ha hb ↦ h a ha b hb, fun h a ha b hb ↦ h a b ha hb⟩

Commutativity of Universal Quantifiers under Condition

Informal description

For any type $\alpha$, predicate $s$ on $\alpha$, and binary relation $p$ on $\alpha$, the following are equivalent: 1. For every $a$ satisfying $s(a)$, and for every $b$ satisfying $s(b)$, the relation $p(a,b)$ holds. 2. For every pair $(a,b)$ where both $s(a)$ and $s(b)$ hold, the relation $p(a,b)$ holds.

forall_mem_comm theorem

 {α β} [Membership α β] {s : β} {p : α → α → Prop} :
  (∀ a (_ : a ∈ s) b (_ : b ∈ s), p a b) ↔ ∀ a b, a ∈ s → b ∈ s → p a b

Full source

theorem forall_mem_comm {α β} [Membership α β] {s : β} {p : α → α → Prop} :
    (∀ a (_ : a ∈ s) b (_ : b ∈ s), p a b) ↔ ∀ a b, a ∈ s → b ∈ s → p a b :=
  forall_cond_comm

Commutativity of Universal Quantifiers over Membership

Informal description

For any types $\alpha$ and $\beta$ with a membership relation $\in$ between them, a set $s$ of type $\beta$, and a binary relation $p$ on $\alpha$, the following are equivalent: 1. For every $a \in s$ and $b \in s$, the relation $p(a,b)$ holds. 2. For every pair $(a,b)$ where both $a \in s$ and $b \in s$, the relation $p(a,b)$ holds.

ne_of_eq_of_ne theorem

{α : Sort*} {a b c : α} (h₁ : a = b) (h₂ : b ≠ c) : a ≠ c

Full source

lemma ne_of_eq_of_ne {α : Sort*} {a b c : α} (h₁ : a = b) (h₂ : b ≠ c) : a ≠ c := h₁.symm ▸ h₂

Transitivity of Equality and Non-Equality: $a = b \land b \neq c \implies a \neq c$

Informal description

For any elements $a, b, c$ of a type $\alpha$, if $a = b$ and $b \neq c$, then $a \neq c$.

ne_of_ne_of_eq theorem

{α : Sort*} {a b c : α} (h₁ : a ≠ b) (h₂ : b = c) : a ≠ c

Full source

lemma ne_of_ne_of_eq {α : Sort*} {a b c : α} (h₁ : a ≠ b) (h₂ : b = c) : a ≠ c := h₂ ▸ h₁

Transitivity of Inequality via Equality: $a \neq b$ and $b = c$ implies $a \neq c$

Informal description

For any elements $a$, $b$, and $c$ of a type $\alpha$, if $a \neq b$ and $b = c$, then $a \neq c$.

congr_refl_left theorem

{α β : Sort*} (f : α → β) {a b : α} (h : a = b) : congr (Eq.refl f) h = congr_arg f h

Full source

theorem congr_refl_left {α β : Sort*} (f : α → β) {a b : α} (h : a = b) :
    congr (Eq.refl f) h = congr_arg f h := rfl

Congruence of Reflexivity Left: $\text{congr}(\text{refl}_f, h) = \text{congr\_arg}(f, h)$

Informal description

For any function $f : \alpha \to \beta$ and elements $a, b \in \alpha$ with $a = b$, the congruence of the reflexivity proof of $f$ with $h$ is equal to the congruence argument of $f$ applied to $h$.

congr_refl_right theorem

{α β : Sort*} {f g : α → β} (h : f = g) (a : α) : congr h (Eq.refl a) = congr_fun h a

Full source

theorem congr_refl_right {α β : Sort*} {f g : α → β} (h : f = g) (a : α) :
    congr h (Eq.refl a) = congr_fun h a := rfl

Congruence of Function Equality with Reflexivity on the Right

Informal description

For any types $\alpha$ and $\beta$, and any functions $f, g : \alpha \to \beta$, given a proof $h$ that $f = g$ and an element $a : \alpha$, the congruence of $h$ with the reflexivity proof of $a$ is equal to the function congruence of $h$ applied to $a$.

congr_arg_refl theorem

{α β : Sort*} (f : α → β) (a : α) : congr_arg f (Eq.refl a) = Eq.refl (f a)

Full source

theorem congr_arg_refl {α β : Sort*} (f : α → β) (a : α) :
    congr_arg f (Eq.refl a) = Eq.refl (f a) :=
  rfl

Congruence Argument of Reflexivity Yields Reflexivity of Function Application

Informal description

For any types $\alpha$ and $\beta$, any function $f : \alpha \to \beta$, and any element $a \in \alpha$, applying the congruence argument function to $f$ and the reflexivity proof of $a$ yields the reflexivity proof of $f(a)$. In other words, $\text{congr\_arg}\, f\, (\text{refl}\, a) = \text{refl}\, (f a)$.

congr_fun_rfl theorem

{α β : Sort*} (f : α → β) (a : α) : congr_fun (Eq.refl f) a = Eq.refl (f a)

Full source

theorem congr_fun_rfl {α β : Sort*} (f : α → β) (a : α) : congr_fun (Eq.refl f) a = Eq.refl (f a) :=
  rfl

Congruence of Function Application with Reflexivity

Informal description

For any types $\alpha$ and $\beta$, any function $f : \alpha \to \beta$, and any element $a \in \alpha$, the application of the congruence function to the reflexivity proof of $f$ at $a$ is equal to the reflexivity proof of $f(a)$.

congr_fun_congr_arg theorem

 {α β γ : Sort*} (f : α → β → γ) {a a' : α} (p : a = a') (b : β) :
  congr_fun (congr_arg f p) b = congr_arg (fun a ↦ f a b) p

Full source

theorem congr_fun_congr_arg {α β γ : Sort*} (f : α → β → γ) {a a' : α} (p : a = a') (b : β) :
    congr_fun (congr_arg f p) b = congr_arg (fun a ↦ f a b) p := rfl

Congruence of Function Application Equals Congruence of Partial Evaluation

Informal description

For any types $\alpha$, $\beta$, $\gamma$ and function $f \colon \alpha \to \beta \to \gamma$, given elements $a, a' \in \alpha$ with equality proof $p \colon a = a'$ and any element $b \in \beta$, we have that applying the congruence of functions to the congruence of arguments equals the congruence of arguments applied to the partially evaluated function: \[ \text{congr\_fun} (\text{congr\_arg} f p) b = \text{congr\_arg} (\lambda a, f a b) p \]

Eq.rec_eq_cast theorem

{α : Sort _} {P : α → Sort _} {x y : α} (h : x = y) (z : P x) : h ▸ z = cast (congr_arg P h) z

Full source

theorem Eq.rec_eq_cast {α : Sort _} {P : α → Sort _} {x y : α} (h : x = y) (z : P x) :
    h ▸ z = cast (congr_arg P h) z := by induction h; rfl

Transport via Equality is Equivalent to Casting via Dependent Type Congruence

Informal description

For any type $\alpha$ and any dependent type $P : \alpha \to \Sort$, given elements $x, y : \alpha$ and a proof $h : x = y$, the transport of $z : P x$ along $h$ is equal to casting $z$ using the proof $\text{congr\_arg}\, P\, h : P x = P y$.

eqRec_heq' theorem

 {α : Sort*} {a' : α} {motive : (a : α) → a' = a → Sort*} (p : motive a' (rfl : a' = a')) {a : α} (t : a' = a) :
  HEq (@Eq.rec α a' motive p a t) p

Full source

theorem eqRec_heq' {α : Sort*} {a' : α} {motive : (a : α) → a' = a → Sort*}
    (p : motive a' (rfl : a' = a')) {a : α} (t : a' = a) :
    HEq (@Eq.rec α a' motive p a t) p := by
  subst t; rfl

Heterogeneous Equality of Recursive Transport Along Identity

Informal description

For any type $\alpha$ and element $a' \in \alpha$, given a dependent type family $\text{motive} : \alpha \to (a' = a) \to \Sort$ and an element $p : \text{motive}\, a'\, \text{rfl}$, then for any $a \in \alpha$ and equality proof $t : a' = a$, the recursively defined element $\text{Eq.rec}\, p\, t$ is heterogeneously equal to $p$.

rec_heq_of_heq theorem

{α β : Sort _} {a b : α} {C : α → Sort*} {x : C a} {y : β} (e : a = b) (h : HEq x y) : HEq (e ▸ x) y

Full source

theorem rec_heq_of_heq {α β : Sort _} {a b : α} {C : α → Sort*} {x : C a} {y : β}
    (e : a = b) (h : HEq x y) : HEq (e ▸ x) y := by subst e; exact h

Transport Preserves Heterogeneous Equality

Informal description

For any types $\alpha$ and $\beta$, elements $a, b \in \alpha$, a dependent type family $C : \alpha \to \Sort$, elements $x \in C(a)$ and $y \in \beta$, given an equality proof $e : a = b$ and a heterogeneous equality proof $h : x \approx y$, the transport of $x$ along $e$ is heterogeneously equal to $y$, i.e., $(e \ ▸ x) \approx y$.

rec_heq_iff_heq theorem

{α β : Sort _} {a b : α} {C : α → Sort*} {x : C a} {y : β} {e : a = b} : HEq (e ▸ x) y ↔ HEq x y

Full source

theorem rec_heq_iff_heq {α β : Sort _} {a b : α} {C : α → Sort*} {x : C a} {y : β} {e : a = b} :
    HEqHEq (e ▸ x) y ↔ HEq x y := by subst e; rfl

Heterogeneous Equality Preservation under Recursor Application

Informal description

For any types $\alpha$ and $\beta$, elements $a, b \in \alpha$, a type family $C : \alpha \to \text{Sort}*$, elements $x \in C(a)$ and $y \in \beta$, and an equality $e : a = b$, the heterogeneous equality $(e \triangleright x) \approx y$ holds if and only if $x \approx y$.

heq_rec_iff_heq theorem

{α β : Sort _} {a b : α} {C : α → Sort*} {x : β} {y : C a} {e : a = b} : HEq x (e ▸ y) ↔ HEq x y

Full source

theorem heq_rec_iff_heq {α β : Sort _} {a b : α} {C : α → Sort*} {x : β} {y : C a} {e : a = b} :
    HEqHEq x (e ▸ y) ↔ HEq x y := by subst e; rfl

Heterogeneous Equality Preservation under Recursor Application

Informal description

For any types $\alpha$ and $\beta$, elements $a, b : \alpha$, a type family $C : \alpha \to \text{Sort}*$, elements $x : \beta$ and $y : C a$, and an equality $e : a = b$, the heterogeneous equality $\text{HEq}~x~(e \triangleright y)$ holds if and only if $\text{HEq}~x~y$ holds.

cast_heq_iff_heq theorem

{α β γ : Sort _} (e : α = β) (a : α) (c : γ) : HEq (cast e a) c ↔ HEq a c

Full source

@[simp]
theorem cast_heq_iff_heq {α β γ : Sort _} (e : α = β) (a : α) (c : γ) :
    HEqHEq (cast e a) c ↔ HEq a c := by subst e; rfl

Heterogeneous Equality Preservation under Type Casting

Informal description

For any types $\alpha$, $\beta$, $\gamma$ and an equality proof $e : \alpha = \beta$, an element $a : \alpha$, and an element $c : \gamma$, the heterogeneous equality $\text{HEq}(\text{cast}(e, a), c)$ holds if and only if $\text{HEq}(a, c)$ holds.

heq_cast_iff_heq theorem

{α β γ : Sort _} (e : β = γ) (a : α) (b : β) : HEq a (cast e b) ↔ HEq a b

Full source

@[simp]
theorem heq_cast_iff_heq {α β γ : Sort _} (e : β = γ) (a : α) (b : β) :
    HEqHEq a (cast e b) ↔ HEq a b := by subst e; rfl

Heterogeneous Equality Preservation under Type Casting

Informal description

For any types $\alpha, \beta, \gamma$ and an equality $e : \beta = \gamma$, given elements $a : \alpha$ and $b : \beta$, the heterogeneous equality $\text{HEq}(a, \text{cast}(e, b))$ holds if and only if $\text{HEq}(a, b)$ holds.

heq_of_eq_cast theorem

(e : β = α) : a = cast e b → HEq a b

Full source

lemma heq_of_eq_cast (e : β = α) : a = cast e b → HEq a b := by rintro rfl; simp

Heterogeneous Equality from Cast Equality

Informal description

Given types $\alpha$ and $\beta$ with an equality $e : \beta = \alpha$, and elements $a : \alpha$ and $b : \beta$, if $a$ equals the cast of $b$ along $e$ (i.e., $a = \text{cast } e\ b$), then $a$ and $b$ are heterogeneously equal (i.e., $\text{HEq } a\ b$).

forall₂_imp theorem

{p q : ∀ a, β a → Prop} (h : ∀ a b, p a b → q a b) : (∀ a b, p a b) → ∀ a b, q a b

Full source

theorem forall₂_imp {p q : ∀ a, β a → Prop} (h : ∀ a b, p a b → q a b) :
    (∀ a b, p a b) → ∀ a b, q a b :=
  forall_imp fun i ↦ forall_imp <| h i

Universal Quantifier Implication Preservation

Informal description

Let $p$ and $q$ be predicates depending on two variables $a$ and $b$ (where $b$ is of type $\beta(a)$). If for all $a$ and $b$, $p(a,b)$ implies $q(a,b)$, then the universal quantification $\forall a b, p(a,b)$ implies $\forall a b, q(a,b)$.

forall₃_imp theorem

{p q : ∀ a b, γ a b → Prop} (h : ∀ a b c, p a b c → q a b c) : (∀ a b c, p a b c) → ∀ a b c, q a b c

Full source

theorem forall₃_imp {p q : ∀ a b, γ a b → Prop} (h : ∀ a b c, p a b c → q a b c) :
    (∀ a b c, p a b c) → ∀ a b c, q a b c :=
  forall_imp fun a ↦ forall₂_imp <| h a

Universal Quantifier Implication Preservation for Three Variables

Informal description

Let $p$ and $q$ be predicates depending on three variables $a$, $b$, and $c$ (where $c$ is of type $\gamma(a,b)$). If for all $a$, $b$, and $c$, $p(a,b,c)$ implies $q(a,b,c)$, then the universal quantification $\forall a\, b\, c, p(a,b,c)$ implies $\forall a\, b\, c, q(a,b,c)$.

Exists₂.imp theorem

{p q : ∀ a, β a → Prop} (h : ∀ a b, p a b → q a b) : (∃ a b, p a b) → ∃ a b, q a b

Full source

theorem Exists₂.imp {p q : ∀ a, β a → Prop} (h : ∀ a b, p a b → q a b) :
    (∃ a b, p a b) → ∃ a b, q a b :=
  Exists.imp fun a ↦ Exists.imp <| h a

Implication Preserves Double Existential Quantification

Informal description

For any two families of propositions $p$ and $q$ indexed by $a$ and $b$, if for all $a$ and $b$ we have $p(a, b)$ implies $q(a, b)$, then the existence of some $a$ and $b$ such that $p(a, b)$ implies the existence of some $a$ and $b$ such that $q(a, b)$. In logical symbols: \[ (\forall a\, b, p(a, b) \to q(a, b)) \to \big((\exists a\, b, p(a, b)) \to (\exists a\, b, q(a, b))\big) \]

Exists₃.imp theorem

{p q : ∀ a b, γ a b → Prop} (h : ∀ a b c, p a b c → q a b c) : (∃ a b c, p a b c) → ∃ a b c, q a b c

Full source

theorem Exists₃.imp {p q : ∀ a b, γ a b → Prop} (h : ∀ a b c, p a b c → q a b c) :
    (∃ a b c, p a b c) → ∃ a b c, q a b c :=
  Exists.imp fun a ↦ Exists₂.imp <| h a

Implication Preserves Triple Existential Quantification

Informal description

For any two families of propositions $p$ and $q$ indexed by $a$, $b$, and $c$, if for all $a$, $b$, and $c$ we have $p(a, b, c)$ implies $q(a, b, c)$, then the existence of some $a$, $b$, and $c$ such that $p(a, b, c)$ implies the existence of some $a$, $b$, and $c$ such that $q(a, b, c)$. In logical symbols: \[ (\forall a\, b\, c, p(a, b, c) \to q(a, b, c)) \to \big((\exists a\, b\, c, p(a, b, c)) \to (\exists a\, b\, c, q(a, b, c))\big) \]

forall_swap theorem

{p : α → β → Prop} : (∀ x y, p x y) ↔ ∀ y x, p x y

Full source

theorem forall_swap {p : α → β → Prop} : (∀ x y, p x y) ↔ ∀ y x, p x y :=
  ⟨fun f x y ↦ f y x, fun f x y ↦ f y x⟩

Swapping Order of Universal Quantifiers

Informal description

For any binary predicate $p$ on types $\alpha$ and $\beta$, the universal quantification over $x$ and then $y$ of $p(x,y)$ is equivalent to the universal quantification over $y$ and then $x$ of $p(x,y)$. In other words, $(\forall x y, p(x,y)) \leftrightarrow (\forall y x, p(x,y))$.

forall₂_swap theorem

 {ι₁ ι₂ : Sort*} {κ₁ : ι₁ → Sort*} {κ₂ : ι₂ → Sort*} {p : ∀ i₁, κ₁ i₁ → ∀ i₂, κ₂ i₂ → Prop} :
  (∀ i₁ j₁ i₂ j₂, p i₁ j₁ i₂ j₂) ↔ ∀ i₂ j₂ i₁ j₁, p i₁ j₁ i₂ j₂

Full source

theorem forall₂_swap
    {ι₁ ι₂ : Sort*} {κ₁ : ι₁ → Sort*} {κ₂ : ι₂ → Sort*} {p : ∀ i₁, κ₁ i₁ → ∀ i₂, κ₂ i₂ → Prop} :
    (∀ i₁ j₁ i₂ j₂, p i₁ j₁ i₂ j₂) ↔ ∀ i₂ j₂ i₁ j₁, p i₁ j₁ i₂ j₂ := ⟨swap₂, swap₂⟩

Swapping Order of Nested Universal Quantifiers

Informal description

For any types $\iota_1$ and $\iota_2$, with dependent types $\kappa_1$ on $\iota_1$ and $\kappa_2$ on $\iota_2$, and for any predicate $p$ depending on elements of $\kappa_1$ and $\kappa_2$, the following equivalence holds: \[ (\forall i_1\, j_1\, i_2\, j_2, p(i_1, j_1, i_2, j_2)) \leftrightarrow (\forall i_2\, j_2\, i_1\, j_1, p(i_1, j_1, i_2, j_2)) \] where $j_1$ is of type $\kappa_1(i_1)$ and $j_2$ is of type $\kappa_2(i_2)$.

imp_forall_iff theorem

{α : Type*} {p : Prop} {q : α → Prop} : (p → ∀ x, q x) ↔ ∀ x, p → q x

Full source

/-- We intentionally restrict the type of `α` in this lemma so that this is a safer to use in simp
than `forall_swap`. -/
theorem imp_forall_iff {α : Type*} {p : Prop} {q : α → Prop} : (p → ∀ x, q x) ↔ ∀ x, p → q x :=
  forall_swap

Implication-Forall Equivalence: $(p \to \forall x, q(x)) \leftrightarrow (\forall x, p \to q(x))$

Informal description

For any type $\alpha$, proposition $p$, and predicate $q$ on $\alpha$, the implication $p \to (\forall x, q(x))$ is equivalent to the universal statement $\forall x, p \to q(x)$.

imp_forall_iff_forall theorem

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

Full source

lemma imp_forall_iff_forall (A : Prop) (B : A → Prop) :
  (A → ∀ h : A, B h) ↔ ∀ h : A, B h := by by_cases h : A <;> simp [h]

Implication-Forall Equivalence for Dependent Predicates

Informal description

For any proposition $A$ and any predicate $B$ depending on $A$, the implication $A \to (\forall h : A, B(h))$ is equivalent to the universal statement $\forall h : A, B(h)$.

exists_swap theorem

{p : α → β → Prop} : (∃ x y, p x y) ↔ ∃ y x, p x y

Full source

theorem exists_swap {p : α → β → Prop} : (∃ x y, p x y) ↔ ∃ y x, p x y :=
  ⟨fun ⟨x, y, h⟩ ↦ ⟨y, x, h⟩, fun ⟨y, x, h⟩ ↦ ⟨x, y, h⟩⟩

Swapping Existential Quantifiers in Binary Relations

Informal description

For any binary relation $p$ on types $\alpha$ and $\beta$, the statement that there exist $x \in \alpha$ and $y \in \beta$ such that $p(x,y)$ holds is equivalent to the statement that there exist $y \in \beta$ and $x \in \alpha$ such that $p(x,y)$ holds. In other words, the existential quantifiers can be swapped: $$(\exists x\ y,\ p(x,y)) \leftrightarrow (\exists y\ x,\ p(x,y))$$

exists_and_exists_comm theorem

{P : α → Prop} {Q : β → Prop} : (∃ a, P a) ∧ (∃ b, Q b) ↔ ∃ a b, P a ∧ Q b

Full source

theorem exists_and_exists_comm {P : α → Prop} {Q : β → Prop} :
    (∃ a, P a) ∧ (∃ b, Q b)(∃ a, P a) ∧ (∃ b, Q b) ↔ ∃ a b, P a ∧ Q b :=
  ⟨fun ⟨⟨a, ha⟩, ⟨b, hb⟩⟩ ↦ ⟨a, b, ⟨ha, hb⟩⟩, fun ⟨a, b, ⟨ha, hb⟩⟩ ↦ ⟨⟨a, ha⟩, ⟨b, hb⟩⟩⟩

Commutativity of Existential Conjunction

Informal description

For any predicates $P$ on a type $\alpha$ and $Q$ on a type $\beta$, the conjunction of the existence of an element in $\alpha$ satisfying $P$ and the existence of an element in $\beta$ satisfying $Q$ is equivalent to the existence of a pair $(a, b) \in \alpha \times \beta$ such that both $P(a)$ and $Q(b)$ hold. In symbols: $$ (\exists a, P(a)) \land (\exists b, Q(b)) \leftrightarrow \exists a\, b, P(a) \land Q(b). $$

not_forall_not theorem

: (¬∀ x, ¬p x) ↔ ∃ x, p x

Full source

theorem not_forall_not : (¬∀ x, ¬p x) ↔ ∃ x, p x :=
  open scoped Classical in Decidable.not_forall_not

Double Negation of Universal Quantifier is Existential Quantifier

Informal description

For any predicate $p$ on a type $\alpha$, the statement "it is not the case that for all $x$, $p(x)$ does not hold" is equivalent to "there exists an $x$ such that $p(x)$ holds". In symbols: $$(\neg \forall x, \neg p(x)) \leftrightarrow (\exists x, p(x))$$

forall_or_exists_not theorem

(P : α → Prop) : (∀ a, P a) ∨ ∃ a, ¬P a

Full source

lemma forall_or_exists_not (P : α → Prop) : (∀ a, P a) ∨ ∃ a, ¬ P a := by
  rw [← not_forall]; exact em _

Universal or Existential Negation of Predicate

Informal description

For any predicate $P$ on a type $\alpha$, either $P(a)$ holds for all $a \in \alpha$, or there exists some $a \in \alpha$ for which $P(a)$ does not hold. In symbols: $$(\forall a, P(a)) \lor (\exists a, \neg P(a))$$

exists_or_forall_not theorem

(P : α → Prop) : (∃ a, P a) ∨ ∀ a, ¬P a

Full source

lemma exists_or_forall_not (P : α → Prop) : (∃ a, P a) ∨ ∀ a, ¬ P a := by
  rw [← not_exists]; exact em _

Existence or Universal Negation of a Predicate

Informal description

For any predicate $P$ on a type $\alpha$, either there exists an element $a$ in $\alpha$ such that $P(a)$ holds, or for all elements $a$ in $\alpha$, $P(a)$ does not hold. In symbols: $$(\exists a, P(a)) \lor (\forall a, \neg P(a))$$

forall_imp_iff_exists_imp theorem

{α : Sort*} {p : α → Prop} {b : Prop} [ha : Nonempty α] : (∀ x, p x) → b ↔ ∃ x, p x → b

Full source

theorem forall_imp_iff_exists_imp {α : Sort*} {p : α → Prop} {b : Prop} [ha : Nonempty α] :
    (∀ x, p x) → b ↔ ∃ x, p x → b := by
  classical
  let ⟨a⟩ := ha
  refine ⟨fun h ↦ not_forall_not.1 fun h' ↦ ?_, fun ⟨x, hx⟩ h ↦ hx (h x)⟩
  exact if hb : b then h' a fun _ ↦ hb else hb <| h fun x ↦ (_root_.not_imp.1 (h' x)).1

Universal Implication is Equivalent to Existential Implication in Nonempty Types

Informal description

For any nonempty type $\alpha$, predicate $p$ on $\alpha$, and proposition $b$, the implication $(\forall x, p(x)) \to b$ holds if and only if there exists an $x$ such that $p(x) \to b$ holds.

forall_true_iff theorem

: (α → True) ↔ True

Full source

@[mfld_simps]
theorem forall_true_iff : (α → True) ↔ True := imp_true_iff _

Universal Quantification over True is Trivially True

Informal description

For any type $\alpha$, the statement "for all $x$ in $\alpha$, $\text{True}$ holds" is equivalent to $\text{True}$.

forall_true_iff' theorem

(h : ∀ a, p a ↔ True) : (∀ a, p a) ↔ True

Full source

theorem forall_true_iff' (h : ∀ a, p a ↔ True) : (∀ a, p a) ↔ True :=
  iff_true_intro fun _ ↦ of_iff_true (h _)

Universal Quantification of Trivial Predicates is Trivial

Informal description

For any predicate $p$ on a type $\alpha$, if for every element $a$ in $\alpha$ the proposition $p(a)$ is equivalent to $\text{True}$, then the universal quantification $\forall a, p(a)$ is also equivalent to $\text{True}$.

forall₂_true_iff theorem

{β : α → Sort*} : (∀ a, β a → True) ↔ True

Full source

theorem forall₂_true_iff {β : α → Sort*} : (∀ a, β a → True) ↔ True := by simp

Universal Quantification over True is Trivially True

Informal description

For any type family $\beta$ indexed by $\alpha$, the universal quantification $(\forall a, \beta a \to \text{True})$ is equivalent to $\text{True}$.

forall₃_true_iff theorem

{β : α → Sort*} {γ : ∀ a, β a → Sort*} : (∀ (a) (b : β a), γ a b → True) ↔ True

Full source

theorem forall₃_true_iff {β : α → Sort*} {γ : ∀ a, β a → Sort*} :
    (∀ (a) (b : β a), γ a b → True) ↔ True := by simp

Universal Quantifier over Three Variables Yields True

Informal description

For any family of types $\beta$ indexed by $\alpha$ and any family of types $\gamma$ indexed by pairs $(a, b)$ where $a : \alpha$ and $b : \beta(a)$, the universal statement $(\forall (a : \alpha) (b : \beta(a)), \gamma(a, b) \to \text{True})$ is equivalent to $\text{True}$.

Decidable.and_forall_ne theorem

[DecidableEq α] (a : α) {p : α → Prop} : (p a ∧ ∀ b, b ≠ a → p b) ↔ ∀ b, p b

Full source

theorem Decidable.and_forall_ne [DecidableEq α] (a : α) {p : α → Prop} :
    (p a ∧ ∀ b, b ≠ a → p b) ↔ ∀ b, p b := by
  simp only [← @forall_eq _ p a, ← forall_and, ← or_imp, Decidable.em, forall_const]

Decidable Universal Quantification via Single Point and Complement

Informal description

Let $\alpha$ be a type with decidable equality, and let $a$ be an element of $\alpha$. For any predicate $p$ on $\alpha$, the statement "$p(a)$ holds and for all $b \neq a$, $p(b)$ holds" is equivalent to "$p(b)$ holds for all $b$".

and_forall_ne theorem

(a : α) : (p a ∧ ∀ b, b ≠ a → p b) ↔ ∀ b, p b

Full source

theorem and_forall_ne (a : α) : (p a ∧ ∀ b, b ≠ a → p b) ↔ ∀ b, p b :=
  open scoped Classical in Decidable.and_forall_ne a

Universal Quantification via Single Point and Complement

Informal description

For any element $a$ of a type $\alpha$ and any predicate $p$ on $\alpha$, the statement "$p(a)$ holds and for all $b \neq a$, $p(b)$ holds" is equivalent to "$p(b)$ holds for all $b \in \alpha$".

Ne.ne_or_ne theorem

{x y : α} (z : α) (h : x ≠ y) : x ≠ z ∨ y ≠ z

Full source

theorem Ne.ne_or_ne {x y : α} (z : α) (h : x ≠ y) : x ≠ zx ≠ z ∨ y ≠ z :=
  not_and_or.1 <| mt (and_imp.2 (· ▸ ·)) h.symm

Disjunction of Inequality: $x \neq y \implies x \neq z \lor y \neq z$

Informal description

For any elements $x, y, z$ of a type $\alpha$, if $x \neq y$, then either $x \neq z$ or $y \neq z$.

exists_apply_eq_apply' theorem

(f : α → β) (a' : α) : ∃ a, f a' = f a

Full source

@[simp]
theorem exists_apply_eq_apply' (f : α → β) (a' : α) : ∃ a, f a' = f a := ⟨a', rfl⟩

Existence of Preimage with Equal Image

Informal description

For any function $f : \alpha \to \beta$ and any element $a' \in \alpha$, there exists an element $a \in \alpha$ such that $f(a') = f(a)$.

exists_apply_eq_apply2 theorem

{α β γ} {f : α → β → γ} {a : α} {b : β} : ∃ x y, f x y = f a b

Full source

@[simp]
lemma exists_apply_eq_apply2 {α β γ} {f : α → β → γ} {a : α} {b : β} : ∃ x y, f x y = f a b :=
  ⟨a, b, rfl⟩

Existence of Inputs Yielding Same Function Value

Informal description

For any function $f : \alpha \to \beta \to \gamma$ and any elements $a \in \alpha$, $b \in \beta$, there exist elements $x \in \alpha$ and $y \in \beta$ such that $f(x, y) = f(a, b)$.

exists_apply_eq_apply2' theorem

{α β γ} {f : α → β → γ} {a : α} {b : β} : ∃ x y, f a b = f x y

Full source

@[simp]
lemma exists_apply_eq_apply2' {α β γ} {f : α → β → γ} {a : α} {b : β} : ∃ x y, f a b = f x y :=
  ⟨a, b, rfl⟩

Existence of Inputs Matching Function Output for Binary Functions

Informal description

For any function $f \colon \alpha \times \beta \to \gamma$ and any elements $a \in \alpha$, $b \in \beta$, there exist elements $x \in \alpha$ and $y \in \beta$ such that $f(a, b) = f(x, y)$.

exists_apply_eq_apply3 theorem

{α β γ δ} {f : α → β → γ → δ} {a : α} {b : β} {c : γ} : ∃ x y z, f x y z = f a b c

Full source

@[simp]
lemma exists_apply_eq_apply3 {α β γ δ} {f : α → β → γ → δ} {a : α} {b : β} {c : γ} :
    ∃ x y z, f x y z = f a b c :=
  ⟨a, b, c, rfl⟩

Existence of Triple Inputs with Equal Output for Ternary Function

Informal description

For any types $\alpha$, $\beta$, $\gamma$, $\delta$ and any function $f \colon \alpha \to \beta \to \gamma \to \delta$, given elements $a \in \alpha$, $b \in \beta$, $c \in \gamma$, there exist elements $x \in \alpha$, $y \in \beta$, $z \in \gamma$ such that $f(x, y, z) = f(a, b, c)$.

exists_apply_eq_apply3' theorem

{α β γ δ} {f : α → β → γ → δ} {a : α} {b : β} {c : γ} : ∃ x y z, f a b c = f x y z

Full source

@[simp]
lemma exists_apply_eq_apply3' {α β γ δ} {f : α → β → γ → δ} {a : α} {b : β} {c : γ} :
    ∃ x y z, f a b c = f x y z :=
  ⟨a, b, c, rfl⟩

Existence of Triple Inputs Matching Function Output

Informal description

For any types $\alpha$, $\beta$, $\gamma$, $\delta$ and any function $f \colon \alpha \to \beta \to \gamma \to \delta$, given elements $a \in \alpha$, $b \in \beta$, $c \in \gamma$, there exist elements $x \in \alpha$, $y \in \beta$, $z \in \gamma$ such that $f(a, b, c) = f(x, y, z)$.

exists_apply_eq theorem

(a : α) (b : β) : ∃ f : α → β, f a = b

Full source

/--
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.
-/
theorem exists_apply_eq (a : α) (b : β) : ∃ f : α → β, f a = b := ⟨fun _ ↦ b, rfl⟩

Existence of Function Mapping Given Input to Given Output

Informal description

For any elements $a \in \alpha$ and $b \in \beta$, there exists a function $f \colon \alpha \to \beta$ such that $f(a) = b$.

exists_exists_and_eq_and theorem

 {f : α → β} {p : α → Prop} {q : β → Prop} : (∃ b, (∃ a, p a ∧ f a = b) ∧ q b) ↔ ∃ a, p a ∧ q (f a)

Full source

@[simp] theorem exists_exists_and_eq_and {f : α → β} {p : α → Prop} {q : β → Prop} :
    (∃ b, (∃ a, p a ∧ f a = b) ∧ q b) ↔ ∃ a, p a ∧ q (f a) :=
  ⟨fun ⟨_, ⟨a, ha, hab⟩, hb⟩ ↦ ⟨a, ha, hab.symm ▸ hb⟩, fun ⟨a, hp, hq⟩ ↦ ⟨f a, ⟨a, hp, rfl⟩, hq⟩⟩

Existential Quantifier Commutation for Function Application and Predicates

Informal description

For any function $f \colon \alpha \to \beta$ and predicates $p$ on $\alpha$ and $q$ on $\beta$, the following are equivalent: 1. There exists $b \in \beta$ such that there exists $a \in \alpha$ with $p(a)$ and $f(a) = b$, and $q(b)$ holds. 2. There exists $a \in \alpha$ such that $p(a)$ holds and $q(f(a))$ holds.

exists_exists_eq_and theorem

{f : α → β} {p : β → Prop} : (∃ b, (∃ a, f a = b) ∧ p b) ↔ ∃ a, p (f a)

Full source

@[simp] theorem exists_exists_eq_and {f : α → β} {p : β → Prop} :
    (∃ b, (∃ a, f a = b) ∧ p b) ↔ ∃ a, p (f a) :=
  ⟨fun ⟨_, ⟨a, ha⟩, hb⟩ ↦ ⟨a, ha.symm ▸ hb⟩, fun ⟨a, ha⟩ ↦ ⟨f a, ⟨a, rfl⟩, ha⟩⟩

Existential Quantifier Commutation for Function Application and Predicate

Informal description

For any function $f \colon \alpha \to \beta$ and any predicate $p$ on $\beta$, there exists $b \in \beta$ such that there exists $a \in \alpha$ with $f(a) = b$ and $p(b)$ holds if and only if there exists $a \in \alpha$ such that $p(f(a))$ holds.

exists_exists_and_exists_and_eq_and theorem

 {α β γ : Type*} {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)

Full source

@[simp] theorem exists_exists_and_exists_and_eq_and {α β γ : Type*}
    {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) :=
  ⟨fun ⟨_, ⟨a, ha, b, hb, hab⟩, hc⟩ ↦ ⟨a, ha, b, hb, hab.symm ▸ hc⟩,
    fun ⟨a, ha, b, hb, hab⟩ ↦ ⟨f a b, ⟨a, ha, b, hb, rfl⟩, hab⟩⟩

Existential Quantifier Distribution over Conjunction and Function Application

Informal description

For any types $\alpha$, $\beta$, $\gamma$, a function $f \colon \alpha \to \beta \to \gamma$, and predicates $p$ on $\alpha$, $q$ on $\beta$, and $r$ on $\gamma$, the following are equivalent: 1. There exists $c \in \gamma$ such that there exists $a \in \alpha$ satisfying $p(a)$ and there exists $b \in \beta$ satisfying $q(b)$ with $f(a,b) = c$, and $r(c)$ holds. 2. There exists $a \in \alpha$ satisfying $p(a)$ and there exists $b \in \beta$ satisfying $q(b)$ such that $r(f(a,b))$ holds.

exists_exists_exists_and_eq theorem

 {α β γ : Type*} {f : α → β → γ} {p : γ → Prop} : (∃ c, (∃ a, ∃ b, f a b = c) ∧ p c) ↔ ∃ a, ∃ b, p (f a b)

Full source

@[simp] theorem exists_exists_exists_and_eq {α β γ : Type*}
    {f : α → β → γ} {p : γ → Prop} :
    (∃ c, (∃ a, ∃ b, f a b = c) ∧ p c) ↔ ∃ a, ∃ b, p (f a b) :=
  ⟨fun ⟨_, ⟨a, b, hab⟩, hc⟩ ↦ ⟨a, b, hab.symm ▸ hc⟩,
    fun ⟨a, b, hab⟩ ↦ ⟨f a b, ⟨a, b, rfl⟩, hab⟩⟩

Existential Quantifier Distribution over Function Application

Informal description

For any types $\alpha$, $\beta$, $\gamma$, a function $f \colon \alpha \to \beta \to \gamma$, and a predicate $p$ on $\gamma$, the following are equivalent: 1. There exists $c \in \gamma$ such that there exist $a \in \alpha$ and $b \in \beta$ with $f(a,b) = c$ and $p(c)$ holds. 2. There exist $a \in \alpha$ and $b \in \beta$ such that $p(f(a,b))$ holds.

forall_apply_eq_imp_iff' theorem

{f : α → β} {p : β → Prop} : (∀ a b, f a = b → p b) ↔ ∀ a, p (f a)

Full source

theorem forall_apply_eq_imp_iff' {f : α → β} {p : β → Prop} :
    (∀ a b, f a = b → p b) ↔ ∀ a, p (f a) := by simp

Universal Quantification over Function Application and Equality

Informal description

For any function $f \colon \alpha \to \beta$ and predicate $p \colon \beta \to \mathrm{Prop}$, the following are equivalent: 1. For all $a \in \alpha$ and $b \in \beta$, if $f(a) = b$ then $p(b)$ holds. 2. For all $a \in \alpha$, $p(f(a))$ holds.

forall_eq_apply_imp_iff' theorem

{f : α → β} {p : β → Prop} : (∀ a b, b = f a → p b) ↔ ∀ a, p (f a)

Full source

theorem forall_eq_apply_imp_iff' {f : α → β} {p : β → Prop} :
    (∀ a b, b = f a → p b) ↔ ∀ a, p (f a) := by simp

Universal Quantifier over Function Application Implication Equivalence

Informal description

For any function $f \colon \alpha \to \beta$ and predicate $p$ on $\beta$, the following are equivalent: 1. For all $a \in \alpha$ and $b \in \beta$, if $b = f(a)$, then $p(b)$ holds. 2. For all $a \in \alpha$, $p(f(a))$ holds. In symbols: \[ (\forall a\, b, b = f(a) \to p(b)) \leftrightarrow (\forall a, p(f(a))) \]

exists₂_comm theorem

 {ι₁ ι₂ : Sort*} {κ₁ : ι₁ → Sort*} {κ₂ : ι₂ → Sort*} {p : ∀ i₁, κ₁ i₁ → ∀ i₂, κ₂ i₂ → Prop} :
  (∃ i₁ j₁ i₂ j₂, p i₁ j₁ i₂ j₂) ↔ ∃ i₂ j₂ i₁ j₁, p i₁ j₁ i₂ j₂

Full source

theorem exists₂_comm
    {ι₁ ι₂ : Sort*} {κ₁ : ι₁ → Sort*} {κ₂ : ι₂ → Sort*} {p : ∀ i₁, κ₁ i₁ → ∀ i₂, κ₂ i₂ → Prop} :
    (∃ i₁ j₁ i₂ j₂, p i₁ j₁ i₂ j₂) ↔ ∃ i₂ j₂ i₁ j₁, p i₁ j₁ i₂ j₂ := by
  simp only [@exists_comm (κ₁ _), @exists_comm ι₁]

Commutation of Nested Existential Quantifiers

Informal description

For any types $ι₁, ι₂$ and families of types $κ₁ : ι₁ → \text{Sort}*$, $κ₂ : ι₂ → \text{Sort}*$, and any predicate $p$ taking arguments from $κ₁$ and $κ₂$, the following equivalence holds: $$(\exists i₁\ j₁\ i₂\ j₂, p\ i₁\ j₁\ i₂\ j₂) \leftrightarrow (\exists i₂\ j₂\ i₁\ j₁, p\ i₁\ j₁\ i₂\ j₂)$$

And.exists theorem

{p q : Prop} {f : p ∧ q → Prop} : (∃ h, f h) ↔ ∃ hp hq, f ⟨hp, hq⟩

Full source

theorem And.exists {p q : Prop} {f : p ∧ q → Prop} : (∃ h, f h) ↔ ∃ hp hq, f ⟨hp, hq⟩ :=
  ⟨fun ⟨h, H⟩ ↦ ⟨h.1, h.2, H⟩, fun ⟨hp, hq, H⟩ ↦ ⟨⟨hp, hq⟩, H⟩⟩

Existential Quantifier Splitting over Conjunction

Informal description

For any propositions $p$ and $q$, and any predicate $f$ on $p \land q$, the existence of a proof $h$ of $p \land q$ such that $f(h)$ holds is equivalent to the existence of proofs $hp$ of $p$ and $hq$ of $q$ such that $f(\langle hp, hq \rangle)$ holds.

forall_or_of_or_forall theorem

{α : Sort*} {p : α → Prop} {b : Prop} (h : b ∨ ∀ x, p x) (x : α) : b ∨ p x

Full source

theorem forall_or_of_or_forall {α : Sort*} {p : α → Prop} {b : Prop} (h : b ∨ ∀ x, p x) (x : α) :
    b ∨ p x :=
  h.imp_right fun h₂ ↦ h₂ x

Distributivity of Universal Quantifier over Disjunction

Informal description

For any type $\alpha$, a proposition $b$, and a predicate $p$ on $\alpha$, if $b$ holds or $p(x)$ holds for all $x \in \alpha$, then for any specific $x \in \alpha$, either $b$ holds or $p(x)$ holds.

Decidable.forall_or_left theorem

{q : Prop} {p : α → Prop} [Decidable q] : (∀ x, q ∨ p x) ↔ q ∨ ∀ x, p x

Full source

protected theorem Decidable.forall_or_left {q : Prop} {p : α → Prop} [Decidable q] :
    (∀ x, q ∨ p x) ↔ q ∨ ∀ x, p x :=
  ⟨fun h ↦ if hq : q then Or.inl hq else
    Or.inr fun x ↦ (h x).resolve_left hq, forall_or_of_or_forall⟩

Universal Quantifier Distributes Over Disjunction (Left)

Informal description

For any proposition $q$ and any predicate $p$ on a type $\alpha$, assuming $q$ is decidable, the following equivalence holds: \[ (\forall x, q \lor p(x)) \leftrightarrow (q \lor \forall x, p(x)) \]

forall_or_left theorem

{q} {p : α → Prop} : (∀ x, q ∨ p x) ↔ q ∨ ∀ x, p x

Full source

theorem forall_or_left {q} {p : α → Prop} : (∀ x, q ∨ p x) ↔ q ∨ ∀ x, p x :=
  open scoped Classical in Decidable.forall_or_left

Universal Quantifier Distributes Over Disjunction (Left)

Informal description

For any proposition $q$ and any predicate $p$ on a type $\alpha$, the following equivalence holds: \[ (\forall x, q \lor p(x)) \leftrightarrow (q \lor \forall x, p(x)) \]

Decidable.forall_or_right theorem

{q} {p : α → Prop} [Decidable q] : (∀ x, p x ∨ q) ↔ (∀ x, p x) ∨ q

Full source

protected theorem Decidable.forall_or_right {q} {p : α → Prop} [Decidable q] :
    (∀ x, p x ∨ q) ↔ (∀ x, p x) ∨ q := by simp [or_comm, Decidable.forall_or_left]

Universal Quantifier Distributes Over Disjunction (Right)

Informal description

For any proposition $q$ and any predicate $p$ on a type $\alpha$, assuming $q$ is decidable, the following equivalence holds: \[ (\forall x, p(x) \lor q) \leftrightarrow ((\forall x, p(x)) \lor q) \]

forall_or_right theorem

{q} {p : α → Prop} : (∀ x, p x ∨ q) ↔ (∀ x, p x) ∨ q

Full source

theorem forall_or_right {q} {p : α → Prop} : (∀ x, p x ∨ q) ↔ (∀ x, p x) ∨ q :=
  open scoped Classical in Decidable.forall_or_right

Universal Quantifier Distributes Over Disjunction (Right)

Informal description

For any proposition $q$ and any predicate $p$ on a type $\alpha$, the following equivalence holds: \[ (\forall x, p(x) \lor q) \leftrightarrow ((\forall x, p(x)) \lor q) \]

Exists.fst theorem

{b : Prop} {p : b → Prop} : Exists p → b

Full source

theorem Exists.fst {b : Prop} {p : b → Prop} : Exists p → b
  | ⟨h, _⟩ => h

First Projection of Existential Quantifier Implies Truth of Proposition

Informal description

For any proposition $b$ and predicate $p$ on $b$, if there exists an element $h$ such that $p(h)$ holds, then $b$ must be true. In other words, the first projection of an existential quantifier $\exists h, p(h)$ implies the truth of the underlying proposition $b$.

Exists.snd theorem

{b : Prop} {p : b → Prop} : ∀ h : Exists p, p h.fst

Full source

theorem Exists.snd {b : Prop} {p : b → Prop} : ∀ h : Exists p, p h.fst
  | ⟨_, h⟩ => h

Second Projection of Existential Quantifier Validates Predicate on Witness

Informal description

For any proposition $b$ and predicate $p$ on $b$, given an existential statement $h : \exists x, p(x)$, the predicate $p$ holds for the witness $h.\text{fst}$ of $h$.

Prop.exists_iff theorem

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

Full source

theorem Prop.exists_iff {p : Prop → Prop} : (∃ h, p h) ↔ p False ∨ p True :=
  ⟨fun ⟨h₁, h₂⟩ ↦ by_cases (fun H : h₁ ↦ .inr <| by simpa only [H] using h₂)
    (fun H ↦ .inl <| by simpa only [H] using h₂), fun h ↦ h.elim (.intro _) (.intro _)⟩

Existential Quantification on Propositions is Equivalent to Disjunction at False and True

Informal description

For any predicate $p$ on the type of propositions, the existential quantification $\exists h, p(h)$ holds if and only if either $p(\text{False})$ or $p(\text{True})$ holds.

Prop.forall_iff theorem

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

Full source

theorem Prop.forall_iff {p : Prop → Prop} : (∀ h, p h) ↔ p False ∧ p True :=
  ⟨fun H ↦ ⟨H _, H _⟩, fun ⟨h₁, h₂⟩ h ↦ by by_cases H : h <;> simpa only [H]⟩

Universal Quantification on Propositions is Equivalent to Conjunction at False and True

Informal description

For any predicate $p$ on the type of propositions, the universal quantification $\forall h, p(h)$ holds if and only if both $p(\text{False})$ and $p(\text{True})$ hold.

exists_iff_of_forall theorem

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

Full source

theorem exists_iff_of_forall {p : Prop} {q : p → Prop} (h : ∀ h, q h) : (∃ h, q h) ↔ p :=
  ⟨Exists.fst, fun H ↦ ⟨H, h H⟩⟩

Existence Under Universal Predicate is Equivalent to Proposition

Informal description

For any proposition $p$ and predicate $q$ on $p$, if $q(h)$ holds for all $h : p$, then the existence of an $h$ such that $q(h)$ holds is equivalent to $p$ itself. In other words, $(\exists h, q(h)) \leftrightarrow p$.

exists_prop_of_false theorem

{p : Prop} {q : p → Prop} : ¬p → ¬∃ h' : p, q h'

Full source

theorem exists_prop_of_false {p : Prop} {q : p → Prop} : ¬p → ¬∃ h' : p, q h' :=
  mt Exists.fst

Nonexistence from False Proposition

Informal description

For any proposition $p$ and predicate $q$ on $p$, if $p$ is false ($\neg p$), then there does not exist an element $h'$ of type $p$ such that $q(h')$ holds ($\neg \exists h' : p, q(h')$).

forall_prop_congr theorem

{p p' : Prop} {q q' : p → Prop} (hq : ∀ h, q h ↔ q' h) (hp : p ↔ p') : (∀ h, q h) ↔ ∀ h : p', q' (hp.2 h)

Full source

theorem forall_prop_congr {p p' : Prop} {q q' : p → Prop} (hq : ∀ h, q h ↔ q' h) (hp : p ↔ p') :
    (∀ h, q h) ↔ ∀ h : p', q' (hp.2 h) :=
  ⟨fun h1 h2 ↦ (hq _).1 (h1 (hp.2 h2)), fun h1 h2 ↦ (hq _).2 (h1 (hp.1 h2))⟩

Universal Quantifier Congruence Under Proposition Equivalence

Informal description

For any propositions $p$ and $p'$, and predicates $q : p \to \text{Prop}$ and $q' : p \to \text{Prop}$, if for all $h : p$ we have $q(h) \leftrightarrow q'(h)$, and $p \leftrightarrow p'$, then the universal quantification $(\forall h : p, q(h))$ is equivalent to $(\forall h : p', q'(h))$ where $h$ is mapped via the implication $p' \to p$.

forall_prop_congr' theorem

{p p' : Prop} {q q' : p → Prop} (hq : ∀ h, q h ↔ q' h) (hp : p ↔ p') : (∀ h, q h) = ∀ h : p', q' (hp.2 h)

Full source

theorem forall_prop_congr' {p p' : Prop} {q q' : p → Prop} (hq : ∀ h, q h ↔ q' h) (hp : p ↔ p') :
    (∀ h, q h) = ∀ h : p', q' (hp.2 h) :=
  propext (forall_prop_congr hq hp)

Equality of Universal Quantifications Under Proposition Equivalence

Informal description

For any propositions $p$ and $p'$, and predicates $q : p \to \text{Prop}$ and $q' : p \to \text{Prop}$, if for all $h : p$ we have $q(h) \leftrightarrow q'(h)$, and $p \leftrightarrow p'$, then the universal quantification $(\forall h, q(h))$ is equal to $(\forall h : p', q'(hp.2 h))$, where $hp.2 : p' \to p$ is the backward implication of $hp$.

imp_congr_eq theorem

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

Full source

lemma imp_congr_eq {a b c d : Prop} (h₁ : a = c) (h₂ : b = d) : (a → b) = (c → d) :=
  propext (imp_congr h₁.to_iff h₂.to_iff)

Implication Congruence Under Equality: $(a \to b) = (c \to d)$ when $a = c$ and $b = d$

Informal description

For any propositions $a, b, c, d$, if $a = c$ and $b = d$, then the implication $(a \to b)$ is equal to the implication $(c \to d)$.

imp_congr_ctx_eq theorem

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

Full source

lemma imp_congr_ctx_eq {a b c d : Prop} (h₁ : a = c) (h₂ : c → b = d) : (a → b) = (c → d) :=
  propext (imp_congr_ctx h₁.to_iff fun hc ↦ (h₂ hc).to_iff)

Contextual Implication Congruence: $(a = c) \land (c \Rightarrow b = d) \Rightarrow (a \to b) = (c \to d)$

Informal description

For any propositions $a, b, c, d$, if $a = c$ and $c$ implies $b = d$, then the implication $a \to b$ is equal to the implication $c \to d$.

iff_eq_eq theorem

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

Full source

lemma iff_eq_eq {a b : Prop} : (a ↔ b) = (a = b) := propext ⟨propext, Eq.to_iff⟩

Equivalence of Logical Equivalence and Propositional Equality

Informal description

For any two propositions $a$ and $b$, the equivalence $(a \leftrightarrow b)$ is equal to the equality $(a = b)$ as propositions.

forall_true_left theorem

(p : True → Prop) : (∀ x, p x) ↔ p True.intro

Full source

/-- See `IsEmpty.forall_iff` for the `False` version. -/
@[simp] theorem forall_true_left (p : True → Prop) : (∀ x, p x) ↔ p True.intro :=
  forall_prop_of_true _

Universal Quantification over True is Equivalent to Evaluation at Canonical Element

Informal description

For any predicate $p$ defined on the type `True`, the universal quantification $(\forall x, p(x))$ is equivalent to $p(\text{True.intro})$, where $\text{True.intro}$ is the canonical element of `True`.

Classical.dec definition

(p : Prop) : Decidable p

Full source

/-- Any prop `p` is decidable classically. A shorthand for `Classical.propDecidable`. -/
noncomputable def dec (p : Prop) : Decidable p := by infer_instance

Classical decidability of propositions

Informal description

For any proposition $ p $, $ p $ is decidable in classical logic. This is a shorthand for the classical decidability instance `Classical.propDecidable`.

Classical.decPred definition

(p : α → Prop) : DecidablePred p

Full source

/-- Any predicate `p` is decidable classically. -/
noncomputable def decPred (p : α → Prop) : DecidablePred p := by infer_instance

Classical decidability of predicates

Informal description

For any predicate $ p $ on a type $ \alpha $, $ p $ is classically decidable. That is, for every $ x \in \alpha $, the proposition $ p(x) $ is decidable in classical logic.

Classical.decRel definition

(p : α → α → Prop) : DecidableRel p

Full source

/-- Any relation `p` is decidable classically. -/
noncomputable def decRel (p : α → α → Prop) : DecidableRel p := by infer_instance

Classical decidability of binary relations

Informal description

For any binary relation $ p $ on a type $ \alpha $, $ p $ is decidable in classical logic. That is, for any $ x, y \in \alpha $, the proposition $ p(x, y) $ is decidable.

Classical.decEq definition

(α : Sort*) : DecidableEq α

Full source

/-- Any type `α` has decidable equality classically. -/
noncomputable def decEq (α : Sort*) : DecidableEq α := by infer_instance

Decidability of equality in classical logic

Informal description

For any type $\alpha$, the equality relation on $\alpha$ is decidable under classical logic.

Classical.existsCases definition

{α C : Sort*} {p : α → Prop} (H0 : C) (H : ∀ a, p a → C) : C

Full source

/-- Construct a function from a default value `H0`, and a function to use if there exists a value
satisfying the predicate. -/
noncomputable def existsCases {α C : Sort*} {p : α → Prop} (H0 : C) (H : ∀ a, p a → C) : C :=
  if h : ∃ a, p a then H (Classical.choose h) (Classical.choose_spec h) else H0

Case analysis on existence

Informal description

Given a default value $H_0$ of type $C$ and a function $H$ that constructs an element of $C$ from any element $a$ of type $\alpha$ satisfying a predicate $p$, the function returns $H_0$ if no such $a$ exists, otherwise applies $H$ to a witness and its proof of satisfying $p$.

Classical.some_spec₂ theorem

{α : Sort*} {p : α → Prop} {h : ∃ a, p a} (q : α → Prop) (hpq : ∀ a, p a → q a) : q (choose h)

Full source

theorem some_spec₂ {α : Sort*} {p : α → Prop} {h : ∃ a, p a} (q : α → Prop)
    (hpq : ∀ a, p a → q a) : q (choose h) := hpq _ <| choose_spec _

Property Preservation for Classical Choice

Informal description

Let $\alpha$ be a type and $p, q$ be predicates on $\alpha$. Given an existential statement $h : \exists a, p\ a$ and a proof $hpq$ that for all $a$, $p\ a$ implies $q\ a$, then the chosen element $\text{choose}\ h$ satisfies $q$.

Classical.byContradiction' definition

{α : Sort*} (H : ¬(α → False)) : α

Full source

/-- A version of `byContradiction` that uses types instead of propositions. -/
protected noncomputable def byContradiction' {α : Sort*} (H : ¬(α → False)) : α :=
  Classical.choice <| (peirce _ False) fun h ↦ (H fun a ↦ h ⟨a⟩).elim

Proof by contradiction (type-theoretic version)

Informal description

Given a type `α`, if the assumption that `α` is empty leads to a contradiction (i.e., `¬(α → False)` holds), then there exists an element of type `α`. This is a type-theoretic version of the classical proof by contradiction principle.

Classical.choice_of_byContradiction' definition

{α : Sort*} (contra : ¬(α → False) → α) : Nonempty α → α

Full source

/-- `Classical.byContradiction'` is equivalent to lean's axiom `Classical.choice`. -/
def choice_of_byContradiction' {α : Sort*} (contra : ¬(α → False) → α) : Nonempty α → α :=
  fun H ↦ contra H.elim

Construction of element from nonemptiness via contradiction

Informal description

Given a type `α` and a function `contra` that constructs an element of `α` from a proof that `α` is not empty (i.e., from a proof that `¬(α → False)`), the function `Classical.choice_of_byContradiction'` produces an element of `α` from a proof that `α` is nonempty (`Nonempty α`).

Classical.choose_eq theorem

(a : α) : @Exists.choose _ (· = a) ⟨a, rfl⟩ = a

Full source

@[simp] lemma choose_eq (a : α) : @Exists.choose _ (· = a) ⟨a, rfl⟩ = a := @choose_spec _ (· = a) _

Classical Choice of Equality Element

Informal description

For any element $a$ of type $\alpha$, the element chosen by the classical choice function from the proof of existence of an element equal to $a$ is $a$ itself.

Classical.choose_eq' theorem

(a : α) : @Exists.choose _ (a = ·) ⟨a, rfl⟩ = a

Full source

@[simp]
lemma choose_eq' (a : α) : @Exists.choose _ (a = ·) ⟨a, rfl⟩ = a :=
  (@choose_spec _ (a = ·) _).symm

Classical Choice Function Returns Equal Element

Informal description

For any element $a$ of type $\alpha$, the classical choice function applied to the existence proof of an element equal to $a$ (with reflexivity as the witness) returns $a$ itself. That is, $\text{choose}(a = \cdot) = a$ when the existence proof is $\langle a, \text{rfl}\rangle$.

Exists.classicalRecOn definition

{α : Sort*} {p : α → Prop} (h : ∃ a, p a) {C : Sort*} (H : ∀ a, p a → C) : C

Full source

/-- 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. -/
noncomputable def Exists.classicalRecOn {α : Sort*} {p : α → Prop} (h : ∃ a, p a)
    {C : Sort*} (H : ∀ a, p a → C) : C :=
  H (Classical.choose h) (Classical.choose_spec h)

Existential Recursion with Choice

Informal description

Given a type $\alpha$ and a predicate $p$ on $\alpha$, if there exists an element $a$ in $\alpha$ such that $p(a)$ holds, then for any type $C$ and any function $H$ that takes an element $a$ of $\alpha$ and a proof that $p(a)$ holds and returns an element of $C$, we can construct an element of $C$ by applying $H$ to the witness provided by the axiom of choice and its corresponding proof. This function generalizes `Exists.recOn` by allowing elimination into any universe, not just `Prop`.

bex_def theorem

: (∃ (x : _) (_ : p x), q x) ↔ ∃ x, p x ∧ q x

Full source

theorem bex_def : (∃ (x : _) (_ : p x), q x) ↔ ∃ x, p x ∧ q x :=
  ⟨fun ⟨x, px, qx⟩ ↦ ⟨x, px, qx⟩, fun ⟨x, px, qx⟩ ↦ ⟨x, px, qx⟩⟩

Bounded Existential Quantifier Definition

Informal description

For any predicates $p$ and $q$ on a type, the statement that there exists an $x$ such that $p(x)$ holds and $q(x)$ holds is equivalent to the statement that there exists an $x$ for which both $p(x)$ and $q(x)$ hold. In symbols: $$ (\exists x, p(x) \land q(x)) \leftrightarrow \exists x, p(x) \land q(x). $$

BEx.elim theorem

{b : Prop} : (∃ x h, P x h) → (∀ a h, P a h → b) → b

Full source

theorem BEx.elim {b : Prop} : (∃ x h, P x h) → (∀ a h, P a h → b) → b
  | ⟨a, h₁, h₂⟩, h' => h' a h₁ h₂

Elimination Rule for Bounded Existential Quantifier

Informal description

For any proposition $b$, if there exists an element $x$ with property $p(x)$ such that $P(x, h)$ holds (where $h$ is a proof of $p(x)$), and if for every element $a$ and proof $h$ of $p(a)$, $P(a, h)$ implies $b$, then $b$ holds.

BEx.intro theorem

(a : α) (h₁ : p a) (h₂ : P a h₁) : ∃ (x : _) (h : p x), P x h

Full source

theorem BEx.intro (a : α) (h₁ : p a) (h₂ : P a h₁) : ∃ (x : _) (h : p x), P x h :=
  ⟨a, h₁, h₂⟩

Introduction Rule for Bounded Existential Quantifier

Informal description

Given an element $a$ of type $\alpha$, a proof $h_1$ that $p(a)$ holds, and a proof $h_2$ that $P(a, h_1)$ holds, then there exists some $x$ in $\alpha$ such that $p(x)$ holds and $P(x, h)$ holds for some proof $h$ of $p(x)$.

BAll.imp_right theorem

(H : ∀ x h, P x h → Q x h) (h₁ : ∀ x h, P x h) (x h) : Q x h

Full source

theorem BAll.imp_right (H : ∀ x h, P x h → Q x h) (h₁ : ∀ x h, P x h) (x h) : Q x h :=
  H _ _ <| h₁ _ _

Implication Preservation Under Universal Quantification

Informal description

Let $P$ and $Q$ be predicates on a type $\alpha$ with a parameter $h$. If for all $x$ and $h$, $P(x, h)$ implies $Q(x, h)$, and if for all $x$ and $h$, $P(x, h)$ holds, then for all $x$ and $h$, $Q(x, h)$ holds.

BEx.imp_right theorem

(H : ∀ x h, P x h → Q x h) : (∃ x h, P x h) → ∃ x h, Q x h

Full source

theorem BEx.imp_right (H : ∀ x h, P x h → Q x h) : (∃ x h, P x h) → ∃ x h, Q x h
  | ⟨_, _, h'⟩ => ⟨_, _, H _ _ h'⟩

Implication Preserves Bounded Existence

Informal description

For any predicates $P$ and $Q$ on elements $x$ of a type $\alpha$ with a condition $h$, if $H$ states that $P(x, h)$ implies $Q(x, h)$ for all $x$ and $h$, then the existence of an $x$ and $h$ such that $P(x, h)$ holds implies the existence of an $x$ and $h$ such that $Q(x, h)$ holds.

BAll.imp_left theorem

(H : ∀ x, p x → q x) (h₁ : ∀ x, q x → r x) (x) (h : p x) : r x

Full source

theorem BAll.imp_left (H : ∀ x, p x → q x) (h₁ : ∀ x, q x → r x) (x) (h : p x) : r x :=
  h₁ _ <| H _ h

Transitivity of Implication for Bounded Universal Quantifiers

Informal description

For all $x$, if $p(x)$ implies $q(x)$ and $q(x)$ implies $r(x)$, then $p(x)$ implies $r(x)$. In other words, if $\forall x, (p(x) \to q(x))$ and $\forall x, (q(x) \to r(x))$ hold, then for any $x$ satisfying $p(x)$, we have $r(x)$.

BEx.imp_left theorem

(H : ∀ x, p x → q x) : (∃ (x : _) (_ : p x), r x) → ∃ (x : _) (_ : q x), r x

Full source

theorem BEx.imp_left (H : ∀ x, p x → q x) : (∃ (x : _) (_ : p x), r x) → ∃ (x : _) (_ : q x), r x
  | ⟨x, hp, hr⟩ => ⟨x, H _ hp, hr⟩

Implication Preserves Bounded Existential Quantifier

Informal description

For any predicates $p$, $q$, and $r$ on a type, if $p(x)$ implies $q(x)$ for all $x$, then the existence of an $x$ satisfying $p(x)$ and $r(x)$ implies the existence of an $x$ satisfying $q(x)$ and $r(x)$. In symbols: \[ (\forall x, p(x) \to q(x)) \to \left((\exists x, p(x) \land r(x)) \to (\exists x, q(x) \land r(x))\right) \]

exists_mem_of_exists theorem

(H : ∀ x, p x) : (∃ x, q x) → ∃ (x : _) (_ : p x), q x

Full source

theorem exists_mem_of_exists (H : ∀ x, p x) : (∃ x, q x) → ∃ (x : _) (_ : p x), q x
  | ⟨x, hq⟩ => ⟨x, H x, hq⟩

Existence Transfer under Universal Condition

Informal description

For any predicate $p$ and $q$, if $\forall x, p(x)$ holds and there exists an $x$ such that $q(x)$ holds, then there exists an $x$ such that both $p(x)$ and $q(x)$ hold.

exists_of_exists_mem theorem

: (∃ (x : _) (_ : p x), q x) → ∃ x, q x

Full source

theorem exists_of_exists_mem : (∃ (x : _) (_ : p x), q x) → ∃ x, q x
  | ⟨x, _, hq⟩ => ⟨x, hq⟩

Existence from Bounded Existence

Informal description

If there exists an element $x$ satisfying property $p(x)$ and also satisfying property $q(x)$, then there exists an element $x$ satisfying $q(x)$.

not_exists_mem theorem

: (¬∃ x h, P x h) ↔ ∀ x h, ¬P x h

Full source

theorem not_exists_mem : (¬∃ x h, P x h) ↔ ∀ x h, ¬P x h := exists₂_imp

Negation of Existential Quantifier with Condition is Equivalent to Universal Negation

Informal description

For any predicate $P$ depending on elements $x$ and conditions $h$, the statement that there does not exist an $x$ with condition $h$ such that $P(x, h)$ holds is equivalent to the statement that for all $x$ and conditions $h$, $P(x, h)$ does not hold. In symbols: $$ \neg (\exists x\ h, P(x, h)) \leftrightarrow \forall x\ h, \neg P(x, h). $$

not_forall₂_of_exists₂_not theorem

: (∃ x h, ¬P x h) → ¬∀ x h, P x h

Full source

theorem not_forall₂_of_exists₂_not : (∃ x h, ¬P x h) → ¬∀ x h, P x h
  | ⟨x, h, hp⟩, al => hp <| al x h

Existence of Counterexample Implies Negation of Universal Statement

Informal description

If there exists an element $x$ with property $h$ such that $P(x, h)$ does not hold, then it is not the case that $P(x, h)$ holds for all $x$ and $h$.

Decidable.not_forall₂ theorem

[Decidable (∃ x h, ¬P x h)] [∀ x h, Decidable (P x h)] : (¬∀ x h, P x h) ↔ ∃ x h, ¬P x h

Full source

protected theorem Decidable.not_forall₂ [Decidable (∃ x h, ¬P x h)] [∀ x h, Decidable (P x h)] :
    (¬∀ x h, P x h) ↔ ∃ x h, ¬P x h :=
  ⟨Not.decidable_imp_symm fun nx x h ↦ nx.decidable_imp_symm
    fun h' ↦ ⟨x, h, h'⟩, not_forall₂_of_exists₂_not⟩

Decidable Equivalence Between Universal Negation and Existential Counterexample

Informal description

For any predicate $P$ depending on elements $x$ and conditions $h$, assuming that both the existence of a counterexample $\exists x h, \neg P(x, h)$ and each individual $P(x, h)$ are decidable, the negation of the universal statement $\neg \forall x h, P(x, h)$ is equivalent to the existence of a counterexample $\exists x h, \neg P(x, h)$. In symbols: $$ \neg (\forall x h, P(x, h)) \leftrightarrow \exists x h, \neg P(x, h). $$

not_forall₂ theorem

: (¬∀ x h, P x h) ↔ ∃ x h, ¬P x h

Full source

theorem not_forall₂ : (¬∀ x h, P x h) ↔ ∃ x h, ¬P x h :=
  open scoped Classical in Decidable.not_forall₂

Negation of Universal Quantifier is Equivalent to Existential Counterexample

Informal description

For any predicate $P$ depending on elements $x$ and conditions $h$, the negation of the universal statement $\neg (\forall x h, P(x, h))$ is equivalent to the existence of a counterexample $\exists x h, \neg P(x, h)$. In symbols: $$ \neg (\forall x h, P(x, h)) \leftrightarrow \exists x h, \neg P(x, h). $$

forall₂_and theorem

: (∀ x h, P x h ∧ Q x h) ↔ (∀ x h, P x h) ∧ ∀ x h, Q x h

Full source

theorem forall₂_and : (∀ x h, P x h ∧ Q x h) ↔ (∀ x h, P x h) ∧ ∀ x h, Q x h :=
  Iff.trans (forall_congr' fun _ ↦ forall_and) forall_and

Universal Quantifier Distributes Over Conjunction

Informal description

For any predicates $P$ and $Q$ depending on variables $x$ and $h$, the universal quantification $\forall x h, P(x, h) \land Q(x, h)$ holds if and only if both $\forall x h, P(x, h)$ and $\forall x h, Q(x, h)$ hold independently.

forall_and_left theorem

[Nonempty α] (q : Prop) (p : α → Prop) : (∀ x, q ∧ p x) ↔ (q ∧ ∀ x, p x)

Full source

theorem forall_and_left [Nonempty α] (q : Prop) (p : α → Prop) :
    (∀ x, q ∧ p x) ↔ (q ∧ ∀ x, p x) := by rw [forall_and, forall_const]

Universal Quantifier Distributes Over Conjunction (Left)

Informal description

For a nonempty type $\alpha$ and propositions $q$ and $p(x)$ for $x \in \alpha$, the following equivalence holds: \[ (\forall x, q \land p(x)) \leftrightarrow (q \land \forall x, p(x)). \]

forall_and_right theorem

[Nonempty α] (p : α → Prop) (q : Prop) : (∀ x, p x ∧ q) ↔ (∀ x, p x) ∧ q

Full source

theorem forall_and_right [Nonempty α] (p : α → Prop) (q : Prop) :
    (∀ x, p x ∧ q) ↔ (∀ x, p x) ∧ q := by rw [forall_and, forall_const]

Universal Quantification Distributes Over Conjunction (Right)

Informal description

For a nonempty type $\alpha$, a predicate $p$ on $\alpha$, and a proposition $q$, the universal quantification $\forall x, p(x) \land q$ holds if and only if both $\forall x, p(x)$ and $q$ hold.

exists_mem_or theorem

: (∃ x h, P x h ∨ Q x h) ↔ (∃ x h, P x h) ∨ ∃ x h, Q x h

Full source

theorem exists_mem_or : (∃ x h, P x h ∨ Q x h) ↔ (∃ x h, P x h) ∨ ∃ x h, Q x h :=
  Iff.trans (exists_congr fun _ ↦ exists_or) exists_or

Existential Quantifier Distributes Over Disjunction in Membership Context

Informal description

For any predicates $P$ and $Q$ depending on elements $x$ and conditions $h$, the following equivalence holds: $$(\exists x\ h,\ P\ x\ h \lor Q\ x\ h) \leftrightarrow (\exists x\ h,\ P\ x\ h) \lor (\exists x\ h,\ Q\ x\ h).$$

forall₂_or_left theorem

: (∀ x, p x ∨ q x → r x) ↔ (∀ x, p x → r x) ∧ ∀ x, q x → r x

Full source

theorem forall₂_or_left : (∀ x, p x ∨ q x → r x) ↔ (∀ x, p x → r x) ∧ ∀ x, q x → r x :=
  Iff.trans (forall_congr' fun _ ↦ or_imp) forall_and

Universal Quantifier Distributes Over Disjunction in Antecedent

Informal description

For all $x$, if either $p(x)$ or $q(x)$ holds, then $r(x)$ holds, if and only if both of the following hold: 1. For all $x$, if $p(x)$ holds then $r(x)$ holds. 2. For all $x$, if $q(x)$ holds then $r(x)$ holds. In symbols: $$(\forall x, p(x) \lor q(x) \to r(x)) \leftrightarrow (\forall x, p(x) \to r(x)) \land (\forall x, q(x) \to r(x))$$

exists_mem_or_left theorem

: (∃ (x : _) (_ : p x ∨ q x), r x) ↔ (∃ (x : _) (_ : p x), r x) ∨ ∃ (x : _) (_ : q x), r x

Full source

theorem exists_mem_or_left :
    (∃ (x : _) (_ : p x ∨ q x), r x) ↔ (∃ (x : _) (_ : p x), r x) ∨ ∃ (x : _) (_ : q x), r x := by
  simp only [exists_prop]
  exact Iff.trans (exists_congr fun x ↦ or_and_right) exists_or

Existential Quantifier Distributes Over Disjunction in Context

Informal description

For any predicates $p$, $q$, and $r$, the statement that there exists an element $x$ such that either $p(x)$ or $q(x)$ holds and $r(x)$ holds is equivalent to the disjunction of the statements that there exists an element $x$ such that $p(x)$ and $r(x)$ hold, or there exists an element $x$ such that $q(x)$ and $r(x)$ hold. In symbols: $$ (\exists x, (p(x) \lor q(x)) \land r(x)) \leftrightarrow (\exists x, p(x) \land r(x)) \lor (\exists x, q(x) \land r(x)) $$

dite_eq_iff theorem

: dite P A B = c ↔ (∃ h, A h = c) ∨ ∃ h, B h = c

Full source

theorem dite_eq_iff : ditedite P A B = c ↔ (∃ h, A h = c) ∨ ∃ h, B h = c := by
  by_cases P <;> simp [*, exists_prop_of_true, exists_prop_of_false]

Characterization of Dependent If-Then-Else Equality: $\mathrm{dite}(P, A, B) = c \leftrightarrow (\exists h, A(h) = c) \lor (\exists h, B(h) = c)$

Informal description

For a proposition $P$, functions $A : P \to \alpha$ and $B : \neg P \to \alpha$, and an element $c \in \alpha$, the dependent if-then-else expression $\mathrm{dite}(P, A, B)$ equals $c$ if and only if either there exists a proof $h$ of $P$ such that $A(h) = c$, or there exists a proof $h$ of $\neg P$ such that $B(h) = c$.

ite_eq_iff theorem

: ite P a b = c ↔ P ∧ a = c ∨ ¬P ∧ b = c

Full source

theorem ite_eq_iff : iteite P a b = c ↔ P ∧ a = c ∨ ¬P ∧ b = c :=
  dite_eq_iff.trans <| by rw [exists_prop, exists_prop]

Characterization of If-Then-Else Equality: $\mathrm{ite}(P, a, b) = c \leftrightarrow (P \land a = c) \lor (\neg P \land b = c)$

Informal description

For any proposition $P$, elements $a, b, c$ of a type $\alpha$, the if-then-else expression $\mathrm{ite}(P, a, b)$ equals $c$ if and only if either $P$ holds and $a = c$, or $\neg P$ holds and $b = c$. In symbols: $$ \mathrm{ite}(P, a, b) = c \leftrightarrow (P \land a = c) \lor (\neg P \land b = c) $$

dite_eq_iff' theorem

: dite P A B = c ↔ (∀ h, A h = c) ∧ ∀ h, B h = c

Full source

theorem dite_eq_iff' : ditedite P A B = c ↔ (∀ h, A h = c) ∧ ∀ h, B h = c :=
  ⟨fun he ↦ ⟨fun h ↦ (dif_pos h).symm.trans he, fun h ↦ (dif_neg h).symm.trans he⟩, fun he ↦
    (em P).elim (fun h ↦ (dif_pos h).trans <| he.1 h) fun h ↦ (dif_neg h).trans <| he.2 h⟩

Dependent If-Then-Else Equality Condition: `dite P A B = c ↔ (∀ h, A h = c) ∧ ∀ h, B h = c`

Informal description

The dependent if-then-else expression `dite P A B` equals `c` if and only if for every proof `h` of `P`, `A h = c` holds, and for every proof `h` of `¬P`, `B h = c` holds.

ite_eq_iff' theorem

: ite P a b = c ↔ (P → a = c) ∧ (¬P → b = c)

Full source

theorem ite_eq_iff' : iteite P a b = c ↔ (P → a = c) ∧ (¬P → b = c) := dite_eq_iff'

If-Then-Else Equality Condition: $\text{ite}(P, a, b) = c \leftrightarrow (P \to a = c) \land (\neg P \to b = c)$

Informal description

The if-then-else expression $\text{ite}(P, a, b) = c$ holds if and only if $a = c$ whenever $P$ is true, and $b = c$ whenever $P$ is false.

dite_ne_left_iff theorem

: dite P (fun _ ↦ a) B ≠ a ↔ ∃ h, a ≠ B h

Full source

theorem dite_ne_left_iff : ditedite P (fun _ ↦ a) B ≠ adite P (fun _ ↦ a) B ≠ a ↔ ∃ h, a ≠ B h := by
  rw [Ne, dite_eq_left_iff, not_forall]
  exact exists_congr fun h ↦ by rw [ne_comm]

Dependent If-Then-Else Inequality Condition: `dite P (fun _ ↦ a) B ≠ a ↔ ∃ h, a ≠ B h`

Informal description

The dependent if-then-else expression `dite P (fun _ ↦ a) B` is not equal to `a` if and only if there exists a proof `h` of `¬P` such that `a ≠ B h`.

dite_ne_right_iff theorem

: (dite P A fun _ ↦ b) ≠ b ↔ ∃ h, A h ≠ b

Full source

theorem dite_ne_right_iff : (dite P A fun _ ↦ b) ≠ b(dite P A fun _ ↦ b) ≠ b ↔ ∃ h, A h ≠ b := by
  simp only [Ne, dite_eq_right_iff, not_forall]

Conditional Term Inequality: $\text{dite}(P, A, \_ \mapsto b) \neq b \leftrightarrow \exists h, A(h) \neq b$

Informal description

For a proposition $P$, a term $b$, and a function $A$ defined when $P$ holds, the conditionally defined term $\text{dite}(P, A, \_ \mapsto b)$ is not equal to $b$ if and only if there exists a proof $h$ of $P$ such that $A(h) \neq b$.

ite_ne_left_iff theorem

: ite P a b ≠ a ↔ ¬P ∧ a ≠ b

Full source

theorem ite_ne_left_iff : iteite P a b ≠ aite P a b ≠ a ↔ ¬P ∧ a ≠ b :=
  dite_ne_left_iff.trans <| by rw [exists_prop]

Inequality Condition for If-Then-Else: $\text{ite}(P, a, b) \neq a \leftrightarrow \neg P \land a \neq b$

Informal description

For a proposition $P$ and elements $a$ and $b$, the if-then-else expression $\text{ite}(P, a, b)$ is not equal to $a$ if and only if $P$ is false and $a \neq b$.

ite_ne_right_iff theorem

: ite P a b ≠ b ↔ P ∧ a ≠ b

Full source

theorem ite_ne_right_iff : iteite P a b ≠ bite P a b ≠ b ↔ P ∧ a ≠ b :=
  dite_ne_right_iff.trans <| by rw [exists_prop]

If-Then-Else Inequality: $\text{ite}(P, a, b) \neq b \leftrightarrow P \land a \neq b$

Informal description

For any proposition $P$ and any terms $a$ and $b$, the if-then-else expression $\text{ite}(P, a, b)$ is not equal to $b$ if and only if $P$ is true and $a \neq b$.

Ne.dite_eq_left_iff theorem

(h : ∀ h, a ≠ B h) : dite P (fun _ ↦ a) B = a ↔ P

Full source

protected theorem Ne.dite_eq_left_iff (h : ∀ h, a ≠ B h) : ditedite P (fun _ ↦ a) B = a ↔ P :=
  dite_eq_left_iff.trans ⟨fun H ↦ of_not_not fun h' ↦ h h' (H h').symm, fun h H ↦ (H h).elim⟩

Dependent If-Then-Else Equals Left Value iff Condition is True

Informal description

For any predicate $P$ and any function $B$ such that $a \neq B(h)$ for all $h$, the dependent if-then-else expression $\text{dite}(P, \lambda \_, a, B)$ equals $a$ if and only if $P$ is true.

Ne.dite_eq_right_iff theorem

(h : ∀ h, A h ≠ b) : (dite P A fun _ ↦ b) = b ↔ ¬P

Full source

protected theorem Ne.dite_eq_right_iff (h : ∀ h, A h ≠ b) : (dite P A fun _ ↦ b) = b ↔ ¬P :=
  dite_eq_right_iff.trans ⟨fun H h' ↦ h h' (H h'), fun h' H ↦ (h' H).elim⟩

Dependent If-Then-Else Equals Right Value iff Condition is False

Informal description

For any predicate $P$ and any function $A$ such that $A(h) \neq b$ for all $h$, the dependent if-then-else expression $\text{dite}(P, A, \lambda \_, b)$ equals $b$ if and only if $P$ is false.

Ne.ite_eq_left_iff theorem

(h : a ≠ b) : ite P a b = a ↔ P

Full source

protected theorem Ne.ite_eq_left_iff (h : a ≠ b) : iteite P a b = a ↔ P :=
  Ne.dite_eq_left_iff fun _ ↦ h

If-then-else equals left value iff condition is true

Informal description

For any elements $a$ and $b$ such that $a \neq b$, the if-then-else expression $\text{ite}(P, a, b)$ equals $a$ if and only if the condition $P$ is true.

Ne.ite_eq_right_iff theorem

(h : a ≠ b) : ite P a b = b ↔ ¬P

Full source

protected theorem Ne.ite_eq_right_iff (h : a ≠ b) : iteite P a b = b ↔ ¬P :=
  Ne.dite_eq_right_iff fun _ ↦ h

If-then-else equals right value iff condition is false

Informal description

For any elements $a$ and $b$ such that $a \neq b$, the if-then-else expression $\text{ite}(P, a, b)$ equals $b$ if and only if the condition $P$ is false.

Ne.dite_ne_left_iff theorem

(h : ∀ h, a ≠ B h) : dite P (fun _ ↦ a) B ≠ a ↔ ¬P

Full source

protected theorem Ne.dite_ne_left_iff (h : ∀ h, a ≠ B h) : ditedite P (fun _ ↦ a) B ≠ adite P (fun _ ↦ a) B ≠ a ↔ ¬P :=
  dite_ne_left_iff.trans <| exists_iff_of_forall h

Dependent If-Then-Else Inequality Condition: $\text{dite}(P, (\_\mapsto a), B) \neq a \leftrightarrow \neg P$

Informal description

For any elements $a$ and $B(h)$ such that $a \neq B(h)$ for all $h$, the dependent if-then-else expression $\text{dite}(P, (\_\mapsto a), B)$ is not equal to $a$ if and only if the condition $P$ is false.

Ne.dite_ne_right_iff theorem

(h : ∀ h, A h ≠ b) : (dite P A fun _ ↦ b) ≠ b ↔ P

Full source

protected theorem Ne.dite_ne_right_iff (h : ∀ h, A h ≠ b) : (dite P A fun _ ↦ b) ≠ b(dite P A fun _ ↦ b) ≠ b ↔ P :=
  dite_ne_right_iff.trans <| exists_iff_of_forall h

Dependent If-Then-Else Inequality Condition: $\text{dite}(P, A, \_ \mapsto b) \neq b \leftrightarrow P$

Informal description

For any term $b$ and function $A$ such that $A(h) \neq b$ for all $h$, the dependent if-then-else expression $\text{dite}(P, A, \_ \mapsto b)$ is not equal to $b$ if and only if the condition $P$ holds.

Ne.ite_ne_left_iff theorem

(h : a ≠ b) : ite P a b ≠ a ↔ ¬P

Full source

protected theorem Ne.ite_ne_left_iff (h : a ≠ b) : iteite P a b ≠ aite P a b ≠ a ↔ ¬P :=
  Ne.dite_ne_left_iff fun _ ↦ h

If-Then-Else Inequality Condition: $\text{ite}(P, a, b) \neq a \leftrightarrow \neg P$

Informal description

For any elements $a$ and $b$ such that $a \neq b$, the if-then-else expression $\text{ite}(P, a, b)$ is not equal to $a$ if and only if the condition $P$ is false.

Ne.ite_ne_right_iff theorem

(h : a ≠ b) : ite P a b ≠ b ↔ P

Full source

protected theorem Ne.ite_ne_right_iff (h : a ≠ b) : iteite P a b ≠ bite P a b ≠ b ↔ P :=
  Ne.dite_ne_right_iff fun _ ↦ h

If-Then-Else Inequality Condition: $\text{ite}(P, a, b) \neq b \leftrightarrow P$

Informal description

For any elements $a$ and $b$ such that $a \neq b$, the if-then-else expression $\text{ite}(P, a, b)$ is not equal to $b$ if and only if the condition $P$ holds.

dite_eq_or_eq theorem

: (∃ h, dite P A B = A h) ∨ ∃ h, dite P A B = B h

Full source

theorem dite_eq_or_eq : (∃ h, dite P A B = A h) ∨ ∃ h, dite P A B = B h :=
  if h : _ then .inl ⟨h, dif_pos h⟩ else .inr ⟨h, dif_neg h⟩

Dependent If-Then-Else Yields Either Branch

Informal description

For any proposition $P$ with a decidability instance, and for any functions $A : P \to \alpha$ and $B : \neg P \to \alpha$, the value of the dependent if-then-else expression $\text{dite}(P, A, B)$ is either equal to $A(h)$ for some proof $h$ of $P$, or equal to $B(h)$ for some proof $h$ of $\neg P$. In other words, $\text{dite}(P, A, B) = A(h)$ for some $h : P$ or $\text{dite}(P, A, B) = B(h)$ for some $h : \neg P$.

ite_eq_or_eq theorem

: ite P a b = a ∨ ite P a b = b

Full source

theorem ite_eq_or_eq : iteite P a b = a ∨ ite P a b = b :=
  if h : _ then .inl (if_pos h) else .inr (if_neg h)

If-Then-Else Output Equals Either Branch

Informal description

For any proposition $P$ (with a decidability instance) and any elements $a$ and $b$ of the same type, the value of the if-then-else expression $\text{ite}(P, a, b)$ is either equal to $a$ or equal to $b$.

apply_dite₂ theorem

 {α β γ : Sort*} (f : α → β → γ) (P : Prop) [Decidable P] (a : P → α) (b : ¬P → α) (c : P → β) (d : ¬P → β) :
  f (dite P a b) (dite P c d) = dite P (fun h ↦ f (a h) (c h)) fun h ↦ f (b h) (d h)

Full source

/-- A two-argument function applied to two `dite`s is a `dite` of that two-argument function
applied to each of the branches. -/
theorem apply_dite₂ {α β γ : Sort*} (f : α → β → γ) (P : Prop) [Decidable P]
    (a : P → α) (b : ¬P → α) (c : P → β) (d : ¬P → β) :
    f (dite P a b) (dite P c d) = dite P (fun h ↦ f (a h) (c h)) fun h ↦ f (b h) (d h) := by
  by_cases h : P <;> simp [h]

Distributivity of Binary Function over Dependent If-Then-Else

Informal description

For any types $\alpha$, $\beta$, $\gamma$, any proposition $P$ with a decidable instance, and any functions $f : \alpha \to \beta \to \gamma$, $a : P \to \alpha$, $b : \neg P \to \alpha$, $c : P \to \beta$, $d : \neg P \to \beta$, the following equality holds: \[ f \left( \text{dite } P \ a \ b \right) \left( \text{dite } P \ c \ d \right) = \text{dite } P \ (\lambda h \mapsto f (a h) (c h)) \ (\lambda h \mapsto f (b h) (d h)) \] where $\text{dite } P \ x \ y$ denotes the dependent if-then-else construct that returns $x(h)$ if $P$ is true (with proof $h$) and $y(h)$ if $P$ is false (with proof $h$).

apply_ite₂ theorem

 {α β γ : Sort*} (f : α → β → γ) (P : Prop) [Decidable P] (a b : α) (c d : β) :
  f (ite P a b) (ite P c d) = ite P (f a c) (f b d)

Full source

/-- A two-argument function applied to two `ite`s is a `ite` of that two-argument function
applied to each of the branches. -/
theorem apply_ite₂ {α β γ : Sort*} (f : α → β → γ) (P : Prop) [Decidable P] (a b : α) (c d : β) :
    f (ite P a b) (ite P c d) = ite P (f a c) (f b d) :=
  apply_dite₂ f P (fun _ ↦ a) (fun _ ↦ b) (fun _ ↦ c) fun _ ↦ d

Distributivity of Binary Function over If-Then-Else: $f(\text{ite } P \ a \ b, \text{ite } P \ c \ d) = \text{ite } P \ (f a c) \ (f b d)$

Informal description

For any types $\alpha$, $\beta$, $\gamma$, any proposition $P$ with a decidable instance, and any function $f : \alpha \to \beta \to \gamma$, the following equality holds: \[ f (\text{ite } P \ a \ b) (\text{ite } P \ c \ d) = \text{ite } P \ (f a c) \ (f b d) \] where $\text{ite } P \ x \ y$ denotes the if-then-else construct that returns $x$ if $P$ is true and $y$ otherwise.

dite_apply theorem

(f : P → ∀ a, σ a) (g : ¬P → ∀ a, σ a) (a : α) : (dite P f g) a = dite P (fun h ↦ f h a) fun h ↦ g h a

Full source

/-- A 'dite' producing a `Pi` type `Π a, σ a`, applied to a value `a : α` is a `dite` that applies
either branch to `a`. -/
theorem dite_apply (f : P → ∀ a, σ a) (g : ¬P → ∀ a, σ a) (a : α) :
    (dite P f g) a = dite P (fun h ↦ f h a) fun h ↦ g h a := by by_cases h : P <;> simp [h]

Dependent If-Then-Else Function Application Rule

Informal description

For any proposition $P$ with a decidability instance, and for any functions $f : P \to \forall a, \sigma a$ and $g : \neg P \to \forall a, \sigma a$, the application of the dependent if-then-else expression $\text{dite}(P, f, g)$ to an element $a : \alpha$ is equal to $\text{dite}(P, \lambda h, f h a, \lambda h, g h a)$. In other words, evaluating a dependent if-then-else function at a point $a$ is equivalent to performing a dependent if-then-else on the evaluations of the branches at $a$.

ite_apply theorem

(f g : ∀ a, σ a) (a : α) : (ite P f g) a = ite P (f a) (g a)

Full source

/-- A 'ite' producing a `Pi` type `Π a, σ a`, applied to a value `a : α` is a `ite` that applies
either branch to `a`. -/
theorem ite_apply (f g : ∀ a, σ a) (a : α) : (ite P f g) a = ite P (f a) (g a) :=
  dite_apply P (fun _ ↦ f) (fun _ ↦ g) a

If-Then-Else Function Application Rule: $(\text{ite } P \ f \ g)(a) = \text{ite } P \ (f a) \ (g a)$

Informal description

For any proposition $P$ with a decidability instance, and for any functions $f, g : \forall a, \sigma a$, the application of the if-then-else expression $\text{ite}(P, f, g)$ to an element $a : \alpha$ is equal to $\text{ite}(P, f a, g a)$. In other words, evaluating an if-then-else function at a point $a$ is equivalent to performing an if-then-else on the evaluations of the branches at $a$.

ite_and theorem

: ite (P ∧ Q) a b = ite P (ite Q a b) b

Full source

theorem ite_and : ite (P ∧ Q) a b = ite P (ite Q a b) b := by
  by_cases hp : P <;> by_cases hq : Q <;> simp [hp, hq]

Conditional Expression Distributivity over Conjunction

Informal description

For any propositions $P$ and $Q$ and any elements $a$ and $b$ of a type $\alpha$, the if-then-else expression $\text{ite}(P \land Q, a, b)$ is equal to $\text{ite}(P, \text{ite}(Q, a, b), b)$.

ite_or theorem

: ite (P ∨ Q) a b = ite P a (ite Q a b)

Full source

theorem ite_or : ite (P ∨ Q) a b = ite P a (ite Q a b) := by
  by_cases hp : P <;> by_cases hq : Q <;> simp [hp, hq]

If-Then-Else Distribution over Disjunction

Informal description

For any propositions $P$ and $Q$ and any elements $a$ and $b$ of a common type, the if-then-else expression $\text{ite}(P \lor Q, a, b)$ is equal to $\text{ite}(P, a, \text{ite}(Q, a, b))$.

dite_dite_comm theorem

 {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

Full source

theorem dite_dite_comm {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 :=
  dite_eq_iff'.2 ⟨
    fun p ↦ by rw [dif_neg (h p), dif_pos p],
    fun np ↦ by congr; funext _; rw [dif_neg np]⟩

Commutativity of Nested Dependent If-Then-Else Statements under Implication Condition

Informal description

Let $P$ and $Q$ be propositions, and let $A : P \to \alpha$, $B : Q \to \alpha$, and $C : \neg P \to \neg Q \to \alpha$ be functions. If $P$ implies $\neg Q$, then the following equality holds: \[ (\text{if } p : P \text{ then } A(p) \text{ else } (\text{if } q : Q \text{ then } B(q) \text{ else } C(p, q))) = (\text{if } q : Q \text{ then } B(q) \text{ else } (\text{if } p : P \text{ then } A(p) \text{ else } C(p, q))) \]

ite_ite_comm theorem

(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

Full source

theorem ite_ite_comm (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 :=
  dite_dite_comm P Q h

Commutativity of Nested If-Then-Else under Implication Condition: $(P \to \neg Q) \to (\text{ite}(P, a, \text{ite}(Q, b, c)) = \text{ite}(Q, b, \text{ite}(P, a, c)))$

Informal description

For any propositions $P$ and $Q$ and any elements $a$, $b$, and $c$ of a common type, if $P$ implies $\neg Q$, then the following equality holds: \[ (\text{if } P \text{ then } a \text{ else } (\text{if } Q \text{ then } b \text{ else } c)) = (\text{if } Q \text{ then } b \text{ else } (\text{if } P \text{ then } a \text{ else } c)) \]

ite_prop_iff_or theorem

: (if P then Q else R) ↔ (P ∧ Q ∨ ¬P ∧ R)

Full source

theorem ite_prop_iff_or : (if P then Q else R) ↔ (P ∧ Q ∨ ¬ P ∧ R) := by
  by_cases p : P <;> simp [p]

Equivalence of Conditional Statement with Disjunctive Form

Informal description

For any propositions $P$, $Q$, and $R$, the statement "if $P$ then $Q$ else $R$" is equivalent to "$(P \land Q) \lor (\lnot P \land R)$".

dite_prop_iff_or theorem

{Q : P → Prop} {R : ¬P → Prop} : dite P Q R ↔ (∃ p, Q p) ∨ (∃ p, R p)

Full source

theorem dite_prop_iff_or {Q : P → Prop} {R : ¬P → Prop} :
    ditedite P Q R ↔ (∃ p, Q p) ∨ (∃ p, R p) := by
  by_cases h : P <;> simp [h, exists_prop_of_false, exists_prop_of_true]

Dependent If-Then-Else as Existential Disjunction

Informal description

For any proposition $P$ and dependent propositions $Q : P \to \text{Prop}$ and $R : \neg P \to \text{Prop}$, the dependent if-then-else expression `dite P Q R` is equivalent to $(\exists p, Q p) \lor (\exists p, R p)$.

ite_prop_iff_and theorem

: (if P then Q else R) ↔ ((P → Q) ∧ (¬P → R))

Full source

theorem ite_prop_iff_and : (if P then Q else R) ↔ ((P → Q) ∧ (¬ P → R)) := by
  by_cases p : P <;> simp [p]

Conditional Statement as Implication Conjunction

Informal description

For any propositions $P$, $Q$, and $R$, the conditional statement "if $P$ then $Q$ else $R$" is equivalent to the conjunction "$(P \to Q) \land (\lnot P \to R)$".

dite_prop_iff_and theorem

{Q : P → Prop} {R : ¬P → Prop} : dite P Q R ↔ (∀ h, Q h) ∧ (∀ h, R h)

Full source

theorem dite_prop_iff_and {Q : P → Prop} {R : ¬P → Prop} :
    ditedite P Q R ↔ (∀ h, Q h) ∧ (∀ h, R h) := by
  by_cases h : P <;> simp [h, forall_prop_of_false, forall_prop_of_true]

Dependent If-Then-Else as Universal Conjunction

Informal description

For any proposition $P$ and any predicates $Q : P \to \text{Prop}$ and $R : \neg P \to \text{Prop}$, the dependent if-then-else expression $\text{dite}(P, Q, R)$ is equivalent to the conjunction $(\forall h : P, Q(h)) \land (\forall h : \neg P, R(h))$.

if_ctx_congr theorem

(h_c : P ↔ Q) (h_t : Q → x = u) (h_e : ¬Q → y = v) : ite P x y = ite Q u v

Full source

theorem if_ctx_congr (h_c : P ↔ Q) (h_t : Q → x = u) (h_e : ¬Q → y = v) : ite P x y = ite Q u v :=
  ite_congr h_c.eq h_t h_e

Contextual Congruence for Conditional Expressions

Informal description

For any propositions $P$ and $Q$ such that $P \leftrightarrow Q$, and for any terms $x, u$ such that $Q \rightarrow x = u$, and any terms $y, v$ such that $\neg Q \rightarrow y = v$, the conditional expression $\text{ite}(P, x, y)$ is equal to $\text{ite}(Q, u, v)$.

if_congr theorem

(h_c : P ↔ Q) (h_t : x = u) (h_e : y = v) : ite P x y = ite Q u v

Full source

theorem if_congr (h_c : P ↔ Q) (h_t : x = u) (h_e : y = v) : ite P x y = ite Q u v :=
  if_ctx_congr h_c (fun _ ↦ h_t) (fun _ ↦ h_e)

Congruence for Conditional Expressions

Informal description

For any propositions $P$ and $Q$ such that $P \leftrightarrow Q$, and for any terms $x, u$ such that $x = u$, and any terms $y, v$ such that $y = v$, the conditional expression $\text{ite}(P, x, y)$ is equal to $\text{ite}(Q, u, v)$.

not_beq_of_ne theorem

{α : Type*} [BEq α] [LawfulBEq α] {a b : α} (ne : a ≠ b) : ¬(a == b)

Full source

theorem not_beq_of_ne {α : Type*} [BEq α] [LawfulBEq α] {a b : α} (ne : a ≠ b) : ¬(a == b) :=
  fun h => ne (eq_of_beq h)

Non-Equality Implies Decidable Non-Equality

Informal description

For any type $\alpha$ with a decidable equality operation `==` that satisfies the lawful equality properties, and for any elements $a, b \in \alpha$ such that $a \neq b$, it follows that $a$ is not equal to $b$ under the decidable equality operation, i.e., $\neg(a == b)$.

beq_eq_beq theorem

 {α β : Type*} [BEq α] [LawfulBEq α] [BEq β] [LawfulBEq β] {a₁ a₂ : α} {b₁ b₂ : β} :
  (a₁ == a₂) = (b₁ == b₂) ↔ (a₁ = a₂ ↔ b₁ = b₂)

Full source

@[simp] lemma beq_eq_beq {α β : Type*} [BEq α] [LawfulBEq α] [BEq β] [LawfulBEq β] {a₁ a₂ : α}
    {b₁ b₂ : β} : (a₁ == a₂) = (b₁ == b₂) ↔ (a₁ = a₂ ↔ b₁ = b₂) := by rw [Bool.eq_iff_iff]; simp

Equivalence of Boolean Equality Comparisons and Logical Equivalence

Informal description

For types $\alpha$ and $\beta$ equipped with boolean equality relations that satisfy the `LawfulBEq` axioms, and for elements $a_1, a_2 \in \alpha$ and $b_1, b_2 \in \beta$, the equality of their boolean comparisons $(a_1 == a_2) = (b_1 == b_2)$ holds if and only if the logical equivalence $(a_1 = a_2) \leftrightarrow (b_1 = b_2)$ holds.

beq_ext theorem

 {α : Type*} (inst1 : BEq α) (inst2 : BEq α) (h : ∀ x y, @BEq.beq _ inst1 x y = @BEq.beq _ inst2 x y) : inst1 = inst2

Full source

@[ext]
theorem beq_ext {α : Type*} (inst1 : BEq α) (inst2 : BEq α)
    (h : ∀ x y, @BEq.beq _ inst1 x y = @BEq.beq _ inst2 x y) :
    inst1 = inst2 := by
  have ⟨beq1⟩ := inst1
  have ⟨beq2⟩ := inst2
  congr
  funext x y
  exact h x y

Extensionality of Boolean Equality Instances

Informal description

For any type $\alpha$, if two boolean equality instances `inst1` and `inst2` on $\alpha$ satisfy that for all elements $x, y \in \alpha$, the boolean equality check `x == y` under `inst1` is equal to the check under `inst2`, then `inst1` and `inst2` are equal as instances.

lawful_beq_subsingleton theorem

{α : Type*} (inst1 : BEq α) (inst2 : BEq α) [@LawfulBEq α inst1] [@LawfulBEq α inst2] : inst1 = inst2

Full source

theorem lawful_beq_subsingleton {α : Type*} (inst1 : BEq α) (inst2 : BEq α)
    [@LawfulBEq α inst1] [@LawfulBEq α inst2] :
    inst1 = inst2 := by
  apply beq_ext
  intro x y
  classical
  simp only [beq_eq_decide]

Uniqueness of Lawful Boolean Equality Instances

Informal description

For any type $\alpha$, if two boolean equality instances `inst1` and `inst2` on $\alpha$ both satisfy the `LawfulBEq` axioms, then `inst1` and `inst2` are equal as instances.

Implementation notes