Stuff that seems like it should be in std or mathlib.

def «term_⇔_» : Lean.TrailingParserDescr

Add bi-implication notation for Lattices. See Mathlib.Order.Notation.

Equations

• «term_⇔_» = Lean.ParserDescr.trailingNode `«term_⇔_» 60 61 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⇔ ") (Lean.ParserDescr.cat `term 60))

theorem biImpl_eq {α : Type u} [BooleanAlgebra α] (a b : α) : (fun (φ₁ φ₂ : α) => (φ₁ ⇨ φ₂) ⊓ (φ₂ ⇨ φ₁)) a b = (a ⇨ b) ⊓ (b ⇨ a)

class SemanticEntails (α : Type u) (β : outParam (Type v)) : Type (max u v)

Notation typeclass for semantic entailment ⊨.

• entails : α → β → Prop

def «term_⊨_» : Lean.TrailingParserDescr

Equations

• «term_⊨_» = Lean.ParserDescr.trailingNode `«term_⊨_» 51 52 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⊨ ") (Lean.ParserDescr.cat `term 52))

def «term_⊭_» : Lean.TrailingParserDescr

Equations

• «term_⊭_» = Lean.ParserDescr.trailingNode `«term_⊭_» 51 52 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⊭ ") (Lean.ParserDescr.cat `term 52))

Nat

theorem Nat.eq_or_lt_of_lt_succ {m n : ℕ} : m < n + 1 → m = n ∨ m < n

instance instHAddPNatNat_trestle : HAdd ℕ+ ℕ ℕ+

Equations

• instHAddPNatNat_trestle = { hAdd := fun (x : ℕ+) (x_1 : ℕ) => match x, x_1 with | ⟨a, h⟩, b => ⟨a + b, ⋯⟩ }

def Quotient.toTrunc {α : Sort u_1} [s : Setoid α] (q : Quotient s) : Trunc { a : α // ⟦a⟧ = q }

Equations

• q.toTrunc = Quotient.recOn q (fun (a : α) => Trunc.mk ⟨a, ⋯⟩) ⋯

def Quotient.elim {α : Sort u_1} {β : Sort u_2} [s : Setoid α] (q : Quotient s) (f : (a : α) → ⟦a⟧ = q → β) (h : ∀ (a b : α) (ha : ⟦a⟧ = q) (hb : ⟦b⟧ = q), f a ha = f b hb) : β

Equations

• q.elim f h = Trunc.lift (fun (x : { a : α // ⟦a⟧ = q }) => f ↑x ⋯) ⋯ q.toTrunc

theorem Quotient.elim_mk {α : Sort u_1} {β : Sort u_2} [s : Setoid α] (a : α) (f : (b : α) → ⟦b⟧ = ⟦a⟧ → β) (h : ∀ (a_1 b : α) (ha : ⟦a_1⟧ = ⟦a⟧) (hb : ⟦b⟧ = ⟦a⟧), f a_1 ha = f b hb) : ⟦a⟧.elim f h = f a ⋯

def Multiset.elim {α : Type u_1} {β : Type u_2} (s : Multiset α) (f : (L : List α) → ↑L = s → β) (h : ∀ (a b : List α) (ha : ↑a = s) (hb : ↑b = s), f a ha = f b hb) : β

Equations

• s.elim f h = Quotient.elim s f h

theorem Multiset.elim_mk {α : Type u_1} {β : Type u_2} (L : List α) (f : (L' : List α) → ⟦L'⟧ = ⟦L⟧ → β) (h : ∀ (a b : List α) (ha : ⟦a⟧ = ⟦L⟧) (hb : ⟦b⟧ = ⟦L⟧), f a ha = f b hb) : elim ⟦L⟧ f h = f L ⋯

theorem Multiset.elim_eq_forall {α : Type u_1} {β : Type u_2} {s : Multiset α} {f : (L : List α) → ↑L = s → β} {h : ∀ (a b : List α) (ha : ↑a = s) (hb : ↑b = s), f a ha = f b hb} (motive : Prop) (hmotive : ∀ {L : List α} {hL : ↑L = s}, s.elim f h = f L hL → motive) : motive

theorem Fin.succFin_of_ne {n : ℕ} {i : Fin n} : ↑i + 1 ≠ n → ↑i + 1 < n

@[reducible, inline]

abbrev Finset.elim {α : Type u_1} {β : Type u_2} (s : Finset α) (f : (L : List α) → ↑L = s.val → β) (h : ∀ (a b : List α) (ha : ↑a = s.val) (hb : ↑b = s.val), f a ha = f b hb) : β

Equations

• s.elim f h = s.val.elim f h

theorem Finset.elim_eq_forall {α : Type u_1} {β : Type u_2} {s : Finset α} {f : (L : List α) → ↑L = s.val → β} {h : ∀ (a b : List α) (ha : ↑a = s.val) (hb : ↑b = s.val), f a ha = f b hb} (motive : Prop) (hmotive : ∀ {L : List α} {hL : ↑L = s.val}, s.elim f h = f L hL → motive) : motive

def Fintype.elim_elems {V : Type u_1} {β : Type u_2} [Fintype V] (f : (L : List V) → (∀ (v : V), v ∈ L) → L.Nodup → β) (h : ∀ (L1 : List V) (h1 : ∀ (v : V), v ∈ L1) (h11 : L1.Nodup) (L2 : List V) (h2 : ∀ (v : V), v ∈ L2) (h22 : L2.Nodup), f L1 h1 h11 = f L2 h2 h22) : β

Given a function over the (complete set of distinct) elements of a fintype, and a proof the function is constant, produce the value of that function.

Equations

• Fintype.elim_elems f h = Fintype.elems.elim (fun (L : List V) (hL : ↑L = Fintype.elems.val) => f L ⋯ ⋯) ⋯

theorem Fintype.elim_elems_eq_forall {V : Type u_1} {β : Type u_2} [Fintype V] (f : (L : List V) → (∀ (v : V), v ∈ L) → L.Nodup → β) {h : ∀ (L1 : List V) (h1 : ∀ (v : V), v ∈ L1) (h11 : L1.Nodup) (L2 : List V) (h2 : ∀ (v : V), v ∈ L2) (h22 : L2.Nodup), f L1 h1 h11 = f L2 h2 h22} {C : Prop} (h' : ∀ (L : List V) (h1 : ∀ (v : V), v ∈ L) (h2 : L.Nodup), elim_elems f h = f L h1 h2 → C) : C

theorem Finset.biUnion_union {α : Type u_1} {β : Type u_2} [DecidableEq α] [DecidableEq β] (s1 s2 : Finset α) (f : α → Finset β) : (s1 ∪ s2).biUnion f = s1.biUnion f ∪ s2.biUnion f

def Finset.getUnique {α : Type u_1} (xs : Finset α) (h : ∃ (x : α), xs = {x}) : α

Equations

• xs.getUnique h = xs.elim (fun (L : List α) (_hL : ↑L = xs.val) => match L, _hL with | [], _hL => ⋯.elim | x :: tail, _hL => x) ⋯

@[simp]

theorem Finset.getUnique_eq {α : Type u_1} (xs : Finset α) (h : ∃ (x : α), xs = {x}) (v : α) : xs.getUnique h = v ↔ xs = {v}

@[simp]

theorem Finset.getUnique_mem {α : Type u_1} (xs : Finset α) (h : ∃ (x : α), xs = {x}) (y : Finset α) : xs.getUnique h ∈ y ↔ xs ⊆ y

theorem List.Perm.find?_unique {α : Type u_1} {a b : List α} {f : α → Bool} (hunique : ∀ (a1 a2 : α), f a1 = true → f a2 = true → a1 = a2) (h : a.Perm b) : find? f a = find? f b

def Multiset.find? {α : Type u_1} (f : α → Bool) (xs : Multiset α) (h : ∀ (a1 a2 : α), f a1 = true → f a2 = true → a1 = a2) : Option α

Equations

• Multiset.find? f xs h = Quotient.lift (fun (x : List α) => List.find? f x) ⋯ xs

@[simp]

theorem Multiset.find?_eq_some {α : Type u_1} {f : α → Bool} {h : ∀ (a1 a2 : α), f a1 = true → f a2 = true → a1 = a2} {x : α} (xs : Multiset α) : find? f xs h = some x ↔ x ∈ xs ∧ f x = true

@[simp]

theorem Multiset.find?_eq_none {α : Type u_1} {f : α → Bool} {h : ∀ (a1 a2 : α), f a1 = true → f a2 = true → a1 = a2} (xs : Multiset α) : find? f xs h = none ↔ ∀ x ∈ xs, f x = false

instance instHasEquivProdOfSetoid_trestle {α : Type u_1} {β : Type u_2} [sa : Setoid α] [sb : Setoid β] : HasEquiv (α × β)

Equations

• instHasEquivProdOfSetoid_trestle = { Equiv := ⇑(sa.prod sb) }

@[simp]

theorem Setoid.prod.pair {α : Type u_1} {β : Type u_2} {a1 a2 : α} {b1 b2 : β} [sa : Setoid α] [sb : Setoid β] : (a1, b1) ≈ (a2, b2) ↔ a1 ≈ a2 ∧ b1 ≈ b2

def Quotient.prod {α✝ : Type u_1} {s1 : Setoid α✝} {α✝¹ : Type u_2} {s2 : Setoid α✝¹} (q1 : Quotient s1) (q2 : Quotient s2) : Quotient (s1.prod s2)

Equations

• q1.prod q2 = Quotient.lift (fun (a1 : α✝¹) => Quotient.lift (fun (a2 : α✝) => ⟦(a1, a2)⟧) ⋯ q2) ⋯ q1

@[simp]

theorem Quotient.prod_mk {α : Type u_1} {β : Type u_2} [sa : Setoid α] [sb : Setoid β] (a : α) (b : β) : ⟦a⟧.prod ⟦b⟧ = ⟦(a, b)⟧

@[simp]

theorem Quotient.prod_eq_mk {α : Type u_1} {β : Type u_2} [sa : Setoid α] [sb : Setoid β] (aa : Quotient sa) (bb : Quotient sb) (a : α) (b : β) : aa.prod bb = ⟦(a, b)⟧ ↔ aa = ⟦a⟧ ∧ bb = ⟦b⟧

def Finset.mapEquiv {α' : Type u_1} {α : Type u_2} [DecidableEq α'] (s : Finset α) (f : α ↪ α') : { x : α // x ∈ s } ≃ { x : α' // x ∈ map f s }

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Finset.mapEquiv_app {α' : Type u_1} {α : Type u_2} [DecidableEq α'] (s : Finset α) (f : α ↪ α') (x : { x : α // x ∈ s }) : ↑((s.mapEquiv f) x) = f ↑x

@[simp]

theorem Finset.mapEquiv_symm_eq {α' : Type u_1} {α : Type u_2} [DecidableEq α'] (s : Finset α) (f : α ↪ α') (x : { x : α' // x ∈ map f s }) (y : α) : ↑((s.mapEquiv f).symm x) = y ↔ ↑x = f y

@[simp]

theorem Finset.eq_mapEquiv_symm {α' : Type u_1} {α : Type u_2} [DecidableEq α'] (s : Finset α) (f : α ↪ α') (x : { x : α' // x ∈ map f s }) (y : α) : y = ↑((s.mapEquiv f).symm x) ↔ f y = ↑x

theorem Finset.app_mapEquiv_symm {α' : Type u_1} {α : Type u_2} [DecidableEq α'] (f' : α → α') (s : Finset α) (f : α ↪ α') (x : { x : α' // x ∈ map f s }) : f' = f.toFun → f' ↑((s.mapEquiv f).symm x) = ↑x

@[simp]

theorem Finset.mapEquiv_of_app {α' : Type u_1} {α : Type u_2} [DecidableEq α'] (s : Finset α) (f : α ↪ α') (x : α) (h : f x ∈ map f s) : (s.mapEquiv f).symm ⟨f x, h⟩ = ⟨x, ⋯⟩

@[simp]

theorem Finset.mem_univ' {α : Type u_1} {I : Fintype α} (x : α) : x ∈ univ

def Fintype.invFun {α' : Type u_1} {α : Type u_2} [DecidableEq α'] [Fintype α] (f : α ↪ α') : { x : α' // x ∈ Finset.map f Finset.univ } ≃ α

Equations

• Fintype.invFun f = (Finset.univ.mapEquiv f).symm.trans { toFun := Subtype.val, invFun := fun (x : α) => ⟨x, ⋯⟩, left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem Fintype.invFun_eq {α : Type u_1} {α' : Type u_2} [Fintype α] [DecidableEq α'] (f : α ↪ α') (x : { x : α' // x ∈ Finset.map f Finset.univ }) (y : α) : (invFun f) x = y ↔ ↑x = f y

@[simp]

theorem Fintype.eq_invFun {α : Type u_1} {α' : Type u_2} [Fintype α] [DecidableEq α'] (f : α ↪ α') (x : { x : α' // x ∈ Finset.map f Finset.univ }) (y : α) : y = (invFun f) x ↔ f y = ↑x

@[simp]

theorem Fintype.invFun_app {α : Type u_1} {α' : Type u_2} [Fintype α] [DecidableEq α'] (f : α ↪ α') (f' : α → α') (x : α) (h : f' x ∈ Finset.map f Finset.univ) : f' = f.toFun → (invFun f) ⟨f' x, h⟩ = x

theorem Fintype.app_invFun {α : Type u_1} {α' : Type u_2} [Fintype α] [DecidableEq α'] (f : α ↪ α') (f' : α → α') (x : { x : α' // x ∈ Finset.map f Finset.univ }) : f' = f.toFun → f' ((invFun f) x) = ↑x

@[simp]

theorem Fintype.invFun_val_eq {α : Type u_1} {α' : Type u_2} [Fintype α] [DecidableEq α'] (f : α ↪ α') (x : { x : α' // x ∈ Finset.map f Finset.univ }) (y : α) : (invFun f) x = y ↔ ↑x = f y

theorem Fintype.invFun_eq_invFun {α : Type u_1} {α' : Type u_2} [Fintype α] [DecidableEq α'] (f f' : α ↪ α') (x : { x : α' // x ∈ Finset.map f Finset.univ }) (y : { x : α' // x ∈ Finset.map f' Finset.univ }) : (invFun f) x = (invFun f') y ↔ ∃ (a : α), ↑x = f a ∧ ↑y = f' a

@[simp]

theorem PNat.val_eq_val (x y : ℕ+) : ↑x = ↑y ↔ x = y

@[simp]

theorem PNat.natPred_succ (n : ℕ+) : n.natPred + 1 = ↑n

@[simp]

theorem Array.finRange_data (n : ℕ) : (Array.finRange n).toList = List.finRange n

@[simp]

theorem top : ⊤

@[simp]

theorem not_bot : ¬⊥

theorem BooleanAlgebra.inf_le_iff_le_compl_sup {α : Type u_1} [BooleanAlgebra α] {a b c : α} : a ⊓ b ≤ c ↔ a ≤ bᶜ ⊔ c

theorem BooleanAlgebra.inf_compl_le_iff_le_sup {α : Type u_1} [BooleanAlgebra α] {a b c : α} : a ⊓ bᶜ ≤ c ↔ a ≤ b ⊔ c

theorem BooleanAlgebra.le_iff_inf_compl_le_bot {α : Type u_1} [BooleanAlgebra α] {a b : α} : a ≤ b ↔ a ⊓ bᶜ ≤ ⊥

theorem BooleanAlgebra.le_iff_inf_compl_eq_bot {α : Type u_1} [BooleanAlgebra α] {a b : α} : a ≤ b ↔ a ⊓ bᶜ = ⊥

@[simp]

theorem Function.Embedding.coe_refl {α : Sort u_1} : ⇑(Embedding.refl α) = id