Basics

This is the stem file (imported by every other file in this project). This file provides notation used throughout the project, some very basic lemmas, and a little bit of configuration.

Notation

@[reducible, inline]

abbrev Z2 : Type

The finite field on 2 elements; write Z2 for "value" type but Fin 2 for "indexing" type.

Equations

• Z2 = ZMod 2

@[reducible, inline]

abbrev Z3 : Type

The finite field on 3 elements; write Z3 for "value" type but Fin 3 for "indexing" type.

Equations

• Z3 = ZMod 3

def «term_ᕃ_» : Lean.TrailingParserDescr

Roughly speaking a ᕃ A is A ∪ {a}.

Equations

• «term_ᕃ_» = Lean.ParserDescr.trailingNode `«term_ᕃ_» 66 67 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ᕃ ") (Lean.ParserDescr.cat `term 66))

def «term_⫗_» : Lean.TrailingParserDescr

Writing X ⫗ Y is slightly more general than writing X ∩ Y = ∅.

Equations

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

def «term_.→» : Lean.TrailingParserDescr

The left-to-right direction of ↔.

Equations

• «term_.→» = Lean.ParserDescr.trailingNode `«term_.→» 1024 1024 (Lean.ParserDescr.symbol ".→")

def «term_.←» : Lean.TrailingParserDescr

The right-to-left direction of ↔.

Equations

• «term_.←» = Lean.ParserDescr.trailingNode `«term_.←» 1024 1024 (Lean.ParserDescr.symbol ".←")

def «term↓_» : Lean.ParserDescr

Writing ↓t is slightly more general than writing Function.const _ t.

Equations

• «term↓_» = Lean.ParserDescr.node `«term↓_» 1024 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "↓") (Lean.ParserDescr.cat `term 1023))

def «term#_» : Lean.ParserDescr

We denote the cardinality of a Fintype the same way the cardinality of a Finset is denoted.

Equations

• «term#_» = Lean.ParserDescr.node `«term#_» 1024 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "#") (Lean.ParserDescr.cat `term 1024))

def «term_.≃» : Lean.TrailingParserDescr

Canonical bijection between subtypes corresponding to equal sets.

Equations

• «term_.≃» = Lean.ParserDescr.trailingNode `«term_.≃» 1024 1024 (Lean.ParserDescr.symbol ".≃")

def «term◩_» : Lean.ParserDescr

The "left" or "top" variant.

Equations

• «term◩_» = Lean.ParserDescr.node `«term◩_» 1024 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "◩") (Lean.ParserDescr.cat `term 1024))

def «term◪_» : Lean.ParserDescr

The "right" or "bottom" variant.

Equations

• «term◪_» = Lean.ParserDescr.node `«term◪_» 1024 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "◪") (Lean.ParserDescr.cat `term 1024))

def «term_⊟_» : Lean.TrailingParserDescr

Glue rows of two matrices.

Equations

• «term_⊟_» = Lean.ParserDescr.trailingNode `«term_⊟_» 63 63 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⊟ ") (Lean.ParserDescr.cat `term 64))

def «term_◫_» : Lean.TrailingParserDescr

Glue cols of two matrices.

Equations

• «term_◫_» = Lean.ParserDescr.trailingNode `«term_◫_» 63 63 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ◫ ") (Lean.ParserDescr.cat `term 64))

def «term⊞» : Lean.ParserDescr

Glue four matrices into one block matrix.

Equations

• «term⊞» = Lean.ParserDescr.node `«term⊞» 1024 (Lean.ParserDescr.symbol "⊞ ")

def «term▬_» : Lean.ParserDescr

Convert vector to a single-row matrix.

Equations

• «term▬_» = Lean.ParserDescr.node `«term▬_» 64 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "▬") (Lean.ParserDescr.cat `term 81))

def «term▮_» : Lean.ParserDescr

Convert vector to a single-col matrix.

Equations

• «term▮_» = Lean.ParserDescr.node `«term▮_» 64 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "▮") (Lean.ParserDescr.cat `term 81))

def «term_⊗_» : Lean.TrailingParserDescr

Outer product of two vectors (the column vector comes on left; the row vector comes on right).

Equations

• «term_⊗_» = Lean.ParserDescr.trailingNode `«term_⊗_» 67 68 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⊗ ") (Lean.ParserDescr.cat `term 68))

def «term_⊡_» : Lean.TrailingParserDescr

Element-wise product of two matrices (rarely used).

Equations

• «term_⊡_» = Lean.ParserDescr.trailingNode `«term_⊡_» 66 67 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⊡ ") (Lean.ParserDescr.cat `term 66))

@[reducible, inline]

abbrev Function.range {α ι : Type} (f : ι → α) : Set α

The set of possible outputs of a function.

Equations

• f.range = Set.range f

def Function.range_unexpand : Lean.PrettyPrinter.Unexpander

Equations

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

def Function.support_unexpand : Lean.PrettyPrinter.Unexpander

Equations

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

Basic lemmas

theorem and_congr_l {P₁ P₂ : Prop} (hP : P₁ ↔ P₂) (Q : Prop) : P₁ ∧ Q ↔ P₂ ∧ Q

theorem and_congr_r {P₁ P₂ : Prop} (hP : P₁ ↔ P₂) (Q : Prop) : Q ∧ P₁ ↔ Q ∧ P₂

theorem Int.neg_one_ne_zero : -1 ≠ 0

theorem exists_minimal_nat_le_of_exists {n : ℕ} (P : ↑{a : ℕ | a ≤ n} → Prop) (hP : P ⟨n, ⋯⟩) : ∃ (n_1 : ↑{a : ℕ | a ≤ n}), Minimal P n_1

theorem exists_minimal_nat_of_exists {P : ℕ → Prop} (hP : ∃ (n : ℕ), P n) : ∃ (n : ℕ), Minimal P n

theorem dite_of_true {α : Type} {P : Prop} [Decidable P] (p : P) {f : P → α} {a : α} : (if hp : P then f hp else a) = f p

theorem dite_of_false {α : Type} {P : Prop} [Decidable P] (p : ¬P) {f : P → α} {a : α} : (if hp : P then f hp else a) = a

theorem Function.range_eq {α ι : Type} (f : ι → α) : f.range = {a : α | ∃ (i : ι), f i = a}

theorem Sum.swap_inj {α β : Type} : Function.Injective swap

theorem Finset.sum_of_single_nonzero {α ι : Type} (s : Finset ι) [AddCommMonoid α] (f : ι → α) (a : ι) (ha : a ∈ s) (hf : ∀ i ∈ s, i ≠ a → f i = 0) : s.sum f = f a

theorem fintype_sum_of_single_nonzero {α ι : Type} [Fintype ι] [AddCommMonoid α] (f : ι → α) (a : ι) (hf : ∀ (i : ι), i ≠ a → f i = 0) : Finset.univ.sum f = f a

theorem sum_elem_of_single_nonzero {α ι : Type} [AddCommMonoid α] {f : ι → α} {S : Set ι} [Fintype ↑S] {a : ι} (haS : a ∈ S) (hf : ∀ (i : ι), i ≠ a → f i = 0) : ∑ i : ↑S, f ↑i = f a

theorem sum_insert_elem {α ι : Type} [DecidableEq ι] [AddCommMonoid α] {S : Set ι} [Fintype ↑S] {a : ι} (ha : a ∉ S) (f : ι → α) : ∑ i : ↑(a ᕃ S), f ↑i = f a + ∑ i : ↑S, f ↑i

theorem finset_toSet_sum {α ι : Type} [AddCommMonoid α] {s : Finset ι} {S : Set ι} [Fintype ↑S] (hsS : ↑s = S) (f : ι → α) : ∑ i : ↑↑s, f ↑i = ∑ i : ↑S, f ↑i

theorem sum_over_fin_succ_of_only_zeroth_nonzero {α : Type} {n : ℕ} [AddCommMonoid α] {f : Fin n.succ → α} (hf : ∀ (i : Fin n.succ), i ≠ 0 → f i = 0) : Finset.univ.sum f = f 0

Conversion between set-based notions and type-based notions

def HasSubset.Subset.elem {α : Type} {X Y : Set α} (hXY : X ⊆ Y) (x : ↑X) : ↑Y

Given X ⊆ Y cast an element of X as an element of Y.

Equations

• hXY.elem x = ⟨↑x, ⋯⟩

theorem HasSubset.Subset.elem_injective {α : Type} {X Y : Set α} (hXY : X ⊆ Y) : Function.Injective hXY.elem

theorem HasSubset.Subset.elem_range {α : Type} {X Y : Set α} (hXY : X ⊆ Y) : hXY.elem.range = {a : ↑Y | ↑a ∈ X}

def Subtype.toSum {α : Type} {X Y : Set α} [(a : α) → Decidable (a ∈ X)] [(a : α) → Decidable (a ∈ Y)] (i : ↑(X ∪ Y)) : ↑X ⊕ ↑Y

Convert (X ∪ Y).Elem to X.Elem ⊕ Y.Elem.

Equations

• i.toSum = if hiX : ↑i ∈ X then ◩⟨↑i, hiX⟩ else if hiY : ↑i ∈ Y then ◪⟨↑i, hiY⟩ else ⋯.elim

def Subtype.toSum_unexpand : Lean.PrettyPrinter.Unexpander

Equations

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

@[simp]

theorem toSum_left {α : Type} {X Y : Set α} [(a : α) → Decidable (a ∈ X)] [(a : α) → Decidable (a ∈ Y)] {i : ↑(X ∪ Y)} (hi : ↑i ∈ X) : i.toSum = ◩⟨↑i, hi⟩

@[simp]

theorem toSum_right {α : Type} {X Y : Set α} [(a : α) → Decidable (a ∈ X)] [(a : α) → Decidable (a ∈ Y)] {i : ↑(X ∪ Y)} (hiX : ↑i ∉ X) (hiY : ↑i ∈ Y) : i.toSum = ◪⟨↑i, hiY⟩

def Sum.toUnion {α : Type} {X Y : Set α} (i : ↑X ⊕ ↑Y) : ↑(X ∪ Y)

Convert X.Elem ⊕ Y.Elem to (X ∪ Y).Elem.

Equations

• i.toUnion = Sum.casesOn i ⋯.elem ⋯.elem

@[simp]

theorem toUnion_left {α : Type} {X Y : Set α} (x : ↑X) : (◩x).toUnion = ⟨↑x, ⋯⟩

@[simp]

theorem toUnion_right {α : Type} {X Y : Set α} (y : ↑Y) : (◪y).toUnion = ⟨↑y, ⋯⟩

@[simp]

theorem toSum_toUnion {α : Type} {X Y : Set α} [(a : α) → Decidable (a ∈ X)] [(a : α) → Decidable (a ∈ Y)] (i : ↑(X ∪ Y)) : i.toSum.toUnion = i

Converting (X ∪ Y).Elem to X.Elem ⊕ Y.Elem and back to (X ∪ Y).Elem gives the original element.

@[simp]

theorem toUnion_toSum {α : Type} {X Y : Set α} [(a : α) → Decidable (a ∈ X)] [(a : α) → Decidable (a ∈ Y)] (hXY : X ⫗ Y) (i : ↑X ⊕ ↑Y) : i.toUnion.toSum = i

Converting X.Elem ⊕ Y.Elem to (X ∪ Y).Elem and back to X.Elem ⊕ Y.Elem gives the original element, assuming that X and Y are disjoint.

Aesop modifiers

def tacticAesopnt : Lean.ParserDescr

Nonterminal aesop (dangerous).

Equations

• tacticAesopnt = Lean.ParserDescr.node `tacticAesopnt 1024 (Lean.ParserDescr.nonReservedSymbol "aesopnt" false)