Note about deprecated files

This file is deprecated, and is no longer imported by anything in mathlib other than other deprecated files, and test files. You should not need to import it.

@[deprecated Std.Commutative (since := "2024-09-13")]

def Commutative {α : Type u} (f : α → α → α) : Prop

Equations

• Commutative f = ∀ (a b : α), f a b = f b a

@[deprecated Std.Associative (since := "2024-09-13")]

def Associative {α : Type u} (f : α → α → α) : Prop

Equations

• Associative f = ∀ (a b c : α), f (f a b) c = f a (f b c)

@[deprecated "No deprecation message was provided." (since := "2024-09-03")]

def LeftIdentity {α : Type u} (f : α → α → α) (one : α) : Prop

Equations

• LeftIdentity f one = ∀ (a : α), f one a = a

@[deprecated "No deprecation message was provided." (since := "2024-09-03")]

def RightIdentity {α : Type u} (f : α → α → α) (one : α) : Prop

Equations

• RightIdentity f one = ∀ (a : α), f a one = a

@[deprecated "No deprecation message was provided." (since := "2024-09-03")]

def RightInverse {α : Type u} (f : α → α → α) (inv : α → α) (one : α) : Prop

Equations

• RightInverse f inv one = ∀ (a : α), f a (inv a) = one

@[deprecated "No deprecation message was provided." (since := "2024-09-03")]

def LeftCancelative {α : Type u} (f : α → α → α) : Prop

Equations

• LeftCancelative f = ∀ (a b c : α), f a b = f a c → b = c

@[deprecated "No deprecation message was provided." (since := "2024-09-03")]

def RightCancelative {α : Type u} (f : α → α → α) : Prop

Equations

• RightCancelative f = ∀ (a b c : α), f a b = f c b → a = c

@[deprecated "No deprecation message was provided." (since := "2024-09-03")]

def LeftDistributive {α : Type u} (f g : α → α → α) : Prop

Equations

• LeftDistributive f g = ∀ (a b c : α), f a (g b c) = g (f a b) (f a c)

@[deprecated "No deprecation message was provided." (since := "2024-09-03")]

def RightDistributive {α : Type u} (f g : α → α → α) : Prop

Equations

• RightDistributive f g = ∀ (a b c : α), f (g a b) c = g (f a c) (f b c)

@[deprecated of_eq_false (since := "2024-09-03")]

theorem not_of_eq_false {p : Prop} (h : p = False) : ¬p

Alias of of_eq_false.

@[deprecated "No deprecation message was provided." (since := "2024-09-03")]

theorem cast_proof_irrel {α β : Sort u} (h₁ h₂ : α = β) (a : α) : cast h₁ a = cast h₂ a

@[deprecated eqRec_heq (since := "2024-09-03")]

theorem eq_rec_heq {α : Sort u} {φ : α → Sort v} {a a' : α} (h : a = a') (p : φ a) : HEq (Eq.recOn h p) p

Alias of eqRec_heq.

@[deprecated proof_irrel_heq (since := "2024-09-03")]

theorem heq_prop {p q : Prop} (hp : p) (hq : q) : HEq hp hq

Alias of proof_irrel_heq.

@[deprecated "No deprecation message was provided." (since := "2024-09-03")]

theorem heq_of_eq_rec_left {α : Sort u} {φ : α → Sort v} {a a' : α} {p₁ : φ a} {p₂ : φ a'} (e : a = a') (h₂ : e ▸ p₁ = p₂) : HEq p₁ p₂

@[deprecated "No deprecation message was provided." (since := "2024-09-03")]

theorem heq_of_eq_rec_right {α : Sort u} {φ : α → Sort v} {a a' : α} {p₁ : φ a} {p₂ : φ a'} (e : a' = a) (h₂ : p₁ = e ▸ p₂) : HEq p₁ p₂

@[deprecated "No deprecation message was provided." (since := "2024-09-03")]

theorem of_heq_true {a : Prop} (h : HEq a True) : a

@[deprecated "No deprecation message was provided." (since := "2024-09-03")]

theorem eq_rec_compose {α β φ : Sort u} (p₁ : β = φ) (p₂ : α = β) (a : α) : Eq.recOn p₁ (Eq.recOn p₂ a) = Eq.recOn ⋯ a

@[deprecated not_not_not (since := "2024-09-11")]

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

Alias of the forward direction of not_not_not.

@[deprecated and_true (since := "2024-09-12")]

theorem and_true_iff (p : Prop) : p ∧ True ↔ p

@[deprecated true_and (since := "2024-09-12")]

theorem true_and_iff (p : Prop) : True ∧ p ↔ p

@[deprecated and_false (since := "2024-09-12")]

theorem and_false_iff (p : Prop) : p ∧ False ↔ False

@[deprecated false_and (since := "2024-09-12")]

theorem false_and_iff (p : Prop) : False ∧ p ↔ False

@[deprecated or_true (since := "2024-09-12")]

theorem or_true_iff (p : Prop) : p ∨ True ↔ True

@[deprecated true_or (since := "2024-09-12")]

theorem true_or_iff (p : Prop) : True ∨ p ↔ True

@[deprecated or_false (since := "2024-09-12")]

theorem or_false_iff (p : Prop) : p ∨ False ↔ p

@[deprecated false_or (since := "2024-09-12")]

theorem false_or_iff (p : Prop) : False ∨ p ↔ p

@[deprecated iff_true (since := "2024-09-12")]

theorem iff_true_iff {a : Prop} : (a ↔ True) ↔ a

@[deprecated true_iff (since := "2024-09-12")]

theorem true_iff_iff {a : Prop} : (True ↔ a) ↔ a

@[deprecated iff_false (since := "2024-09-12")]

theorem iff_false_iff {a : Prop} : (a ↔ False) ↔ ¬a

@[deprecated false_iff (since := "2024-09-12")]

theorem false_iff_iff {a : Prop} : (False ↔ a) ↔ ¬a

@[deprecated iff_self (since := "2024-09-12")]

theorem iff_self_iff (a : Prop) : (a ↔ a) ↔ True

@[deprecated not_or_intro (since := "2024-09-12")]

theorem not_or_of_not {a b : Prop} (ha : ¬a) (hb : ¬b) : ¬(a ∨ b)

Alias of not_or_intro.

@[deprecated "No deprecation message was provided." (since := "2024-09-03")]

theorem decide_True' (h : Decidable True) : decide True = true

@[deprecated "No deprecation message was provided." (since := "2024-09-03")]

theorem decide_False' (h : Decidable False) : decide False = false

@[deprecated "No deprecation message was provided." (since := "2024-09-03")]

def Decidable.recOn_true (p : Prop) [h : Decidable p] {h₁ : p → Sort u} {h₂ : ¬p → Sort u} (h₃ : p) (h₄ : h₁ h₃) : Decidable.recOn h h₂ h₁

Equations

• Decidable.recOn_true p h₃ h₄ = cast ⋯ h₄

@[deprecated "No deprecation message was provided." (since := "2024-09-03")]

def Decidable.recOn_false (p : Prop) [h : Decidable p] {h₁ : p → Sort u} {h₂ : ¬p → Sort u} (h₃ : ¬p) (h₄ : h₂ h₃) : Decidable.recOn h h₂ h₁

Equations

• Decidable.recOn_false p h₃ h₄ = cast ⋯ h₄

@[deprecated Decidable.byCases (since := "2024-09-03")]

def Decidable.by_cases {p : Prop} {q : Sort u} [dec : Decidable p] (h1 : p → q) (h2 : ¬p → q) : q

Alias of Decidable.byCases.

---

Synonym for dite (dependent if-then-else). We can construct an element q (of any sort, not just a proposition) by cases on whether p is true or false, provided p is decidable.

Equations

• @Decidable.by_cases = @Decidable.byCases

@[deprecated Decidable.byContradiction (since := "2024-09-03")]

theorem Decidable.by_contradiction {p : Prop} [dec : Decidable p] (h : ¬p → False) : p

Alias of Decidable.byContradiction.

@[deprecated Decidable.not_not (since := "2024-07-27")]

theorem Decidable.not_not_iff {p : Prop} [Decidable p] : ¬¬p ↔ p

Alias of Decidable.not_not.

@[deprecated instDecidableOr (since := "2024-09-03")]

def Or.decidable {p q : Prop} [dp : Decidable p] [dq : Decidable q] : Decidable (p ∨ q)

Alias of instDecidableOr.

Equations

• @Or.decidable = @instDecidableOr

@[deprecated instDecidableAnd (since := "2024-09-03")]

def And.decidable {p q : Prop} [dp : Decidable p] [dq : Decidable q] : Decidable (p ∧ q)

Alias of instDecidableAnd.

Equations

• @And.decidable = @instDecidableAnd

@[deprecated instDecidableNot (since := "2024-09-03")]

def Not.decidable {p : Prop} [dp : Decidable p] : Decidable ¬p

Alias of instDecidableNot.

Equations

• @Not.decidable = @instDecidableNot

@[deprecated instDecidableIff (since := "2024-09-03")]

def Iff.decidable {p q : Prop} [Decidable p] [Decidable q] : Decidable (p ↔ q)

Alias of instDecidableIff.

Equations

• @Iff.decidable = @instDecidableIff

@[deprecated instDecidableTrue (since := "2024-09-03")]

def decidableTrue : Decidable True

Alias of instDecidableTrue.

Equations

• decidableTrue = instDecidableTrue

@[deprecated instDecidableFalse (since := "2024-09-03")]

def decidableFalse : Decidable False

Alias of instDecidableFalse.

Equations

• decidableFalse = instDecidableFalse

@[deprecated "No deprecation message was provided." (since := "2024-09-03")]

def IsDecEq {α : Sort u} (p : α → α → Bool) : Prop

Equations

• IsDecEq p = ∀ ⦃x y : α⦄, p x y = true → x = y

@[deprecated "No deprecation message was provided." (since := "2024-09-03")]

def IsDecRefl {α : Sort u} (p : α → α → Bool) : Prop

Equations

• IsDecRefl p = ∀ (x : α), p x x = true

@[deprecated "No deprecation message was provided." (since := "2024-09-03")]

def decidableEq_of_bool_pred {α : Sort u} {p : α → α → Bool} (h₁ : IsDecEq p) (h₂ : IsDecRefl p) : DecidableEq α

Equations

• decidableEq_of_bool_pred h₁ h₂ x✝¹ x✝ = if hp : p x✝¹ x✝ = true then isTrue ⋯ else isFalse ⋯

@[deprecated "No deprecation message was provided." (since := "2024-09-03")]

theorem decidableEq_inl_refl {α : Sort u} [h : DecidableEq α] (a : α) : h a a = isTrue ⋯

@[deprecated "No deprecation message was provided." (since := "2024-09-03")]

theorem decidableEq_inr_neg {α : Sort u} [h : DecidableEq α] {a b : α} (n : a ≠ b) : h a b = isFalse n

@[deprecated "No deprecation message was provided." (since := "2024-09-03")]

theorem rec_subsingleton {p : Prop} [h : Decidable p] {h₁ : p → Sort u} {h₂ : ¬p → Sort u} [h₃ : ∀ (h : p), Subsingleton (h₁ h)] [h₄ : ∀ (h : ¬p), Subsingleton (h₂ h)] : Subsingleton (Decidable.recOn h h₂ h₁)

@[deprecated "No deprecation message was provided." (since := "2024-09-03")]

theorem imp_of_if_pos {c t e : Prop} [Decidable c] (h : if c then t else e) (hc : c) : t

@[deprecated "No deprecation message was provided." (since := "2024-09-03")]

theorem imp_of_if_neg {c t e : Prop} [Decidable c] (h : if c then t else e) (hnc : ¬c) : e

@[deprecated "No deprecation message was provided." (since := "2024-09-11")]

theorem dif_ctx_congr {α : Sort u} {b c : Prop} [dec_b : Decidable b] [dec_c : Decidable c] {x : b → α} {u : c → α} {y : ¬b → α} {v : ¬c → α} (h_c : b ↔ c) (h_t : ∀ (h : c), x ⋯ = u h) (h_e : ∀ (h : ¬c), y ⋯ = v h) : dite b x y = dite c u v

@[deprecated "No deprecation message was provided." (since := "2024-09-03")]

theorem if_ctx_congr_prop {b c x y u v : Prop} [dec_b : Decidable b] [dec_c : Decidable c] (h_c : b ↔ c) (h_t : c → (x ↔ u)) (h_e : ¬c → (y ↔ v)) : (if b then x else y) ↔ if c then u else v

@[deprecated "No deprecation message was provided." (since := "2024-09-03")]

theorem if_congr_prop {b c x y u v : Prop} [Decidable b] [Decidable c] (h_c : b ↔ c) (h_t : x ↔ u) (h_e : y ↔ v) : (if b then x else y) ↔ if c then u else v

@[deprecated "No deprecation message was provided." (since := "2024-09-03")]

theorem if_ctx_simp_congr_prop {b c x y u v : Prop} [Decidable b] (h_c : b ↔ c) (h_t : c → (x ↔ u)) (h_e : ¬c → (y ↔ v)) : (if b then x else y) ↔ if c then u else v

@[deprecated "No deprecation message was provided." (since := "2024-09-03")]

theorem if_simp_congr_prop {b c x y u v : Prop} [Decidable b] (h_c : b ↔ c) (h_t : x ↔ u) (h_e : y ↔ v) : (if b then x else y) ↔ if c then u else v

@[deprecated "No deprecation message was provided." (since := "2024-09-03")]

theorem dif_ctx_simp_congr {α : Sort u} {b c : Prop} [Decidable b] {x : b → α} {u : c → α} {y : ¬b → α} {v : ¬c → α} (h_c : b ↔ c) (h_t : ∀ (h : c), x ⋯ = u h) (h_e : ∀ (h : ¬c), y ⋯ = v h) : dite b x y = dite c u v

@[deprecated "No deprecation message was provided." (since := "2024-09-03")]

def AsTrue (c : Prop) [Decidable c] : Prop

Equations

• AsTrue c = if c then True else False

@[deprecated "No deprecation message was provided." (since := "2024-09-03")]

def AsFalse (c : Prop) [Decidable c] : Prop

Equations

• AsFalse c = if c then False else True

@[deprecated "No deprecation message was provided." (since := "2024-09-03")]

theorem AsTrue.get {c : Prop} [h₁ : Decidable c] : AsTrue c → c

@[deprecated "No deprecation message was provided." (since := "2024-09-03")]

theorem let_value_eq {α : Sort u} {β : Sort v} {a₁ a₂ : α} (b : α → β) (h : a₁ = a₂) : (let x := a₁; b x) = let x := a₂; b x

@[deprecated "No deprecation message was provided." (since := "2024-09-03")]

theorem let_value_heq {α : Sort v} {β : α → Sort u} {a₁ a₂ : α} (b : (x : α) → β x) (h : a₁ = a₂) : HEq (let x := a₁; b x) (let x := a₂; b x)

@[deprecated "No deprecation message was provided." (since := "2024-09-03")]

theorem let_body_eq {α : Sort v} {β : α → Sort u} (a : α) {b₁ b₂ : (x : α) → β x} (h : ∀ (x : α), b₁ x = b₂ x) : (let x := a; b₁ x) = let x := a; b₂ x

@[deprecated "No deprecation message was provided." (since := "2024-09-03")]

theorem let_eq {α : Sort v} {β : Sort u} {a₁ a₂ : α} {b₁ b₂ : α → β} (h₁ : a₁ = a₂) (h₂ : ∀ (x : α), b₁ x = b₂ x) : (let x := a₁; b₁ x) = let x := a₂; b₂ x