Heap

definition abbreviation theorem
legend
structure Mereology (Place : Type) : Type
  • parts : Place → Finset Place
Show details

Outer dependencies: (none)

Mathlib dependencies: Finset

Lean core dependencies: Eq, HEq, Nat, SizeOf, eq_of_heq

Used by: Mereology.Irreflexive, Mereology.PartOf, Mereology.ProperPart, Mereology.combine

def Mereology.PartOf {Place : Type} (M : Mereology Place) (x y : Place) : Prop
Show details 
| M.PartOf x y = (x ∈ M.parts y)

Complexity: 39 (size of the value term)

Outer dependencies: Mereology

Mathlib dependencies: Finset

Used by: Mereology.ProperPart

def Mereology.ProperPart {Place : Type} (M : Mereology Place) : Place → Place → Prop
Show details 
| M.ProperPart = Relation.TransGen M.PartOf

Complexity: 15 (size of the value term)

Outer dependencies: Mereology

Inner dependencies: Mereology.PartOf

Lean core dependencies: Relation.TransGen

Used by: Mereology.Irreflexive

def Mereology.Irreflexive {Place : Type} (M : Mereology Place) : Prop
Show details 
| M.Irreflexive = ∀ (p : Place), ¬M.ProperPart p p

Complexity: 19 (size of the value term)

Outer dependencies: Mereology

Inner dependencies: Mereology.ProperPart

Lean core dependencies: Not

Used by: (none)

def Mereology.combine {Place : Type} [DecidableEq Place] (G1 G2 : Mereology Place) : Mereology Place
Show details 
| G1.combine G2 = { parts := fun p => G1.parts p ∪ G2.parts p }

Complexity: 47 (size of the value term)

Outer dependencies: Mereology

Mathlib dependencies: Finset

Lean core dependencies: DecidableEq

Used by: (none)

structure Heap (Place Value : Type) [TopologicalSpace Place] : Type
  • domain : Set Place
  • at_ : (p : Place) → p ∈ Heap.domain Value → Value
Show details

Outer dependencies: (none)

Mathlib dependencies: Set, TopologicalSpace

Lean core dependencies: Eq, HEq, eq_of_heq

Used by: Heap.combine, Heap.combine_at_left, Heap.combine_at_right, Heap.combine_domain, Heap.create, Heap.create_delete, Heap.create_domain, Heap.delete, Heap.delete_domain, Heap.dematerialize, Heap.empty, Heap.materialize, Heap.materialize_dematerialize, Heap.mem_reachable, Heap.reachable, HeapCover, HeapCover.whole, Object, Object.state, Tower, Tower.heapBot, Tower.heapTop, Tower.wholeHeap, doorHeap

def Heap.empty (Place Value : Type) [TopologicalSpace Place] [Nonempty Value] : Heap Place Value
Show details 
| Heap.empty Place Value = { domain := ∅, at_ := fun p hp => absurd hp ⋯ }

Complexity: 91 (size of the value term)

Outer dependencies: Heap

Mathlib dependencies: Set, Set.notMem_empty, TopologicalSpace

Lean core dependencies: Nonempty, absurd

Used by: (none)

def Heap.reachable {Place Value : Type} [TopologicalSpace Place] (h : Heap Place Value) : Set Value
Show details 
| h.reachable = {v | ∃ p, ∃ (hp : p ∈ Heap.domain Value), Heap.at_ p hp = v}

Complexity: 97 (size of the value term)

Outer dependencies: Heap

Mathlib dependencies: Set, TopologicalSpace, setOf

Lean core dependencies: Eq, Exists

Used by: Heap.mem_reachable, Object, Object.state, doorBehavior, doorClass, doorHeap.closedVal, doorHeap.closed_reachable, doorHeap.openedVal, doorHeap.opened_reachable, doorInterface, doorObject, instNonemptyElemDoorStateReachableBoolDoorHeapStateDoorClass, instStructureDoorLanguageElemDoorStateReachableBoolDoorHeap

theorem Heap.mem_reachable {Place Value : Type} [TopologicalSpace Place] (h : Heap Place Value) (p : Place)
  (hp : p ∈ Heap.domain Value) : Heap.at_ p hp ∈ h.reachable
Show details 
fun {Place Value} [TopologicalSpace Place] h p hp => Exists.intro p (Exists.intro hp rfl)

Complexity: 233 (size of the value term)

Dependencies: Heap, Heap.reachable

Mathlib dependencies: Set, TopologicalSpace

Lean core dependencies: Eq, Exists, rfl

Used by: Object, Object.state

def Heap.grothendieckTopology (Place : Type) [TopologicalSpace Place] :
  CategoryTheory.GrothendieckTopology (TopologicalSpace.Opens Place)
Show details 
| Heap.grothendieckTopology Place = Opens.grothendieckTopology Place

Complexity: 11 (size of the value term)

Outer dependencies: (none)

Mathlib dependencies: CategoryTheory.GrothendieckTopology, Opens.grothendieckTopology, TopologicalSpace, TopologicalSpace.Opens

Used by: Tower.grothendieckTopology

def Heap.combine {Place Value : Type} [TopologicalSpace Place] [DecidableEq Place]
  (h1 h2 : Heap Place Value)
  (_hagree :
    ∀ (p : Place) (hp1 : p ∈ Heap.domain Value) (hp2 : p ∈ Heap.domain Value),
      Heap.at_ p hp1 = Heap.at_ p hp2) :
  Heap Place Value
Show details 
| h1.combine h2 _hagree =
  { domain := Heap.domain Value ∪ Heap.domain Value,
    at_ := fun p hp => if h1p : p ∈ Heap.domain Value then Heap.at_ p h1p else Heap.at_ p ⋯ }

Complexity: 341 (size of the value term)

Outer dependencies: Heap

Mathlib dependencies: Set, Set.mem_union, TopologicalSpace

Lean core dependencies: DecidableEq, Eq, Not, Or, Or.resolve_left, dite

Used by: Heap.combine_at_left, Heap.combine_at_right, Heap.combine_domain

theorem Heap.combine_domain {Place Value : Type} [TopologicalSpace Place] [DecidableEq Place]
  (h1 h2 : Heap Place Value)
  (_hagree :
    ∀ (p : Place) (hp1 : p ∈ Heap.domain Value) (hp2 : p ∈ Heap.domain Value),
      Heap.at_ p hp1 = Heap.at_ p hp2) :
  Heap.domain Value = Heap.domain Value ∪ Heap.domain Value
Show details 
fun {Place Value} [TopologicalSpace Place] [DecidableEq Place] h1 h2 _hagree => rfl

Complexity: 139 (size of the value term)

Dependencies: Heap, Heap.combine

Mathlib dependencies: Set, TopologicalSpace

Lean core dependencies: DecidableEq, Eq, rfl

Used by: (none)

theorem Heap.combine_at_left {Place Value : Type} [TopologicalSpace Place] [DecidableEq Place]
  (h1 h2 : Heap Place Value)
  (hagree :
    ∀ (p : Place) (hp1 : p ∈ Heap.domain Value) (hp2 : p ∈ Heap.domain Value),
      Heap.at_ p hp1 = Heap.at_ p hp2)
  (p : Place) (hp1 : p ∈ Heap.domain Value) : Heap.at_ p ⋯ = Heap.at_ p hp1
Show details 
fun {Place Value} [TopologicalSpace Place] [DecidableEq Place] h1 h2 hagree p hp1 =>
  id
    (Eq.mpr (id (congrArg (fun _a => _a = Heap.at_ p hp1) (dif_pos hp1)))
      (Eq.refl (Heap.at_ p hp1)))

Complexity: 1075 (size of the value term)

Dependencies: Heap, Heap.combine

Mathlib dependencies: Set, Set.mem_union_left, TopologicalSpace

Lean core dependencies: DecidableEq, Eq, Eq.mpr, Not, congrArg, dif_pos, dite, id

Used by: (none)

theorem Heap.combine_at_right {Place Value : Type} [TopologicalSpace Place] [DecidableEq Place]
  (h1 h2 : Heap Place Value)
  (hagree :
    ∀ (p : Place) (hp1 : p ∈ Heap.domain Value) (hp2 : p ∈ Heap.domain Value),
      Heap.at_ p hp1 = Heap.at_ p hp2)
  (p : Place) (hp2 : p ∈ Heap.domain Value) : Heap.at_ p ⋯ = Heap.at_ p hp2
Show details 
fun {Place Value} [TopologicalSpace Place] [DecidableEq Place] h1 h2 hagree p hp2 =>
  if hp1 : p ∈ Heap.domain Value then
    id (Eq.mpr (id (congrArg (fun _a => _a = Heap.at_ p hp2) (dif_pos hp1))) (hagree p hp1 hp2))
  else
    id
      (Eq.mpr (id (congrArg (fun _a => _a = Heap.at_ p hp2) (dif_neg hp1)))
        (Eq.refl
          (Heap.at_ p
            (Heap.combine._proof_1 h1 h2 p (Set.mem_union_right (Heap.domain Value) hp2) hp1))))

Complexity: 2347 (size of the value term)

Dependencies: Heap, Heap.combine

Mathlib dependencies: Set, Set.mem_union_right, TopologicalSpace

Lean core dependencies: DecidableEq, Eq, Eq.mpr, Not, congrArg, dif_neg, dif_pos, dite, id

Used by: (none)

structure HeapCover (Place Value : Type) [TopologicalSpace Place] : Type 1
  • Block : Type
  • piece : self.Block → Heap Place Value
Show details

Outer dependencies: (none)

Inner dependencies: Heap

Mathlib dependencies: TopologicalSpace

Lean core dependencies: Eq, HEq, Nat, SizeOf, eq_of_heq

Used by: HeapCover.agree, HeapCover.whole, HeapCover.whole_at, HeapCover.whole_domain, HeapCover.whole_domain_isOpen

def HeapCover.agree {Place Value : Type} [TopologicalSpace Place] (HC : HeapCover Place Value) : Prop
Show details 
| HC.agree =
  ∀ (b c : HC.Block) (p : Place) (hb : p ∈ Heap.domain Value) (hc : p ∈ Heap.domain Value),
    Heap.at_ p hb = Heap.at_ p hc

Complexity: 157 (size of the value term)

Outer dependencies: HeapCover

Mathlib dependencies: Set, TopologicalSpace

Lean core dependencies: Eq

Used by: HeapCover.whole, HeapCover.whole_at, HeapCover.whole_domain

def HeapCover.whole {Place Value : Type} [TopologicalSpace Place] [DecidableEq Place]
  (HC : HeapCover Place Value) [Fintype HC.Block] (_hagree : HC.agree) : Heap Place Value
Show details 
| HC.whole _hagree = { domain := ⋃ b, Heap.domain Value, at_ := fun p hp => Heap.at_ p ⋯ }

Complexity: 257 (size of the value term)

Outer dependencies: Heap, HeapCover, HeapCover.agree

Mathlib dependencies: Fintype, Set, Set.iUnion, Set.mem_iUnion, TopologicalSpace

Lean core dependencies: DecidableEq, Exists, Exists.choose, Exists.choose_spec

Used by: HeapCover.whole_at, HeapCover.whole_domain

theorem HeapCover.whole_domain {Place Value : Type} [TopologicalSpace Place] [DecidableEq Place]
  (HC : HeapCover Place Value) [Fintype HC.Block] (hagree : HC.agree) :
  Heap.domain Value = ⋃ b, Heap.domain Value
Show details 
fun {Place Value} [TopologicalSpace Place] [DecidableEq Place] HC [Fintype HC.Block] hagree => rfl

Complexity: 71 (size of the value term)

Dependencies: HeapCover, HeapCover.agree, HeapCover.whole

Mathlib dependencies: Fintype, Set, Set.iUnion, TopologicalSpace

Lean core dependencies: DecidableEq, Eq, rfl

Used by: (none)

theorem HeapCover.whole_at {Place Value : Type} [TopologicalSpace Place] [DecidableEq Place]
  (HC : HeapCover Place Value) [Fintype HC.Block] (hagree : HC.agree) {b : HC.Block} {p : Place}
  (hb : p ∈ Heap.domain Value) : Heap.at_ p ⋯ = Heap.at_ p hb
Show details 
fun {Place Value} [TopologicalSpace Place] [DecidableEq Place] HC [Fintype HC.Block] hagree {b} {p}
    hb =>
  id
    (hagree (Set.mem_iUnion.mp (Set.mem_iUnion.mpr (Exists.intro b hb))).choose b p
      (Exists.choose_spec (Set.mem_iUnion.mp (Set.mem_iUnion.mpr (Exists.intro b hb)))) hb)

Complexity: 1253 (size of the value term)

Dependencies: HeapCover, HeapCover.agree, HeapCover.whole

Mathlib dependencies: Fintype, Set, Set.iUnion, Set.mem_iUnion, TopologicalSpace

Lean core dependencies: DecidableEq, Eq, Exists, Exists.choose, Exists.choose_spec, id

Used by: (none)

theorem HeapCover.whole_domain_isOpen {Place Value : Type} [TopologicalSpace Place]
  (HC : HeapCover Place Value) (hopen : ∀ (b : HC.Block), IsOpen (Heap.domain Value)) :
  IsOpen (⋃ b, Heap.domain Value)
Show details 
fun {Place Value} [TopologicalSpace Place] HC hopen => isOpen_iUnion hopen

Complexity: 99 (size of the value term)

Dependencies: HeapCover

Mathlib dependencies: IsOpen, Set.iUnion, TopologicalSpace, isOpen_iUnion

Used by: (none)

inductive Kind : Type
  • virtual : Kind
  • material : Kind
Show details

Outer dependencies: (none)

Lean core dependencies: Eq, Nat, Nat.ble, PULift, cond, noConfusionEnum, noConfusionTypeEnum

Used by: (none)

def Heap.create {Place Value : Type} [TopologicalSpace Place] (h : Heap Place Value) (p : Place)
  (s : Value) (_hfresh : p ∉ Heap.domain Value) : Heap Place Value
Show details 
| h.create p s _hfresh =
  { domain := insert p (Heap.domain Value),
    at_ := fun q hq => if heq : q = p then s else Heap.at_ q ⋯ }

Complexity: 189 (size of the value term)

Outer dependencies: Heap

Mathlib dependencies: Set, Set.mem_insert_iff, TopologicalSpace

Lean core dependencies: Eq, Not, Or, Or.resolve_left, dite

Used by: Heap.create_delete, Heap.create_domain, Heap.materialize

def Heap.delete {Place Value : Type} [TopologicalSpace Place] (h : Heap Place Value) (p : Place)
  (_hmem : p ∈ Heap.domain Value) : Heap Place Value
Show details 
| h.delete p _hmem = { domain := Heap.domain Value \ {p}, at_ := fun q hq => Heap.at_ q ⋯ }

Complexity: 161 (size of the value term)

Outer dependencies: Heap

Mathlib dependencies: Set, TopologicalSpace

Lean core dependencies: Not

Used by: Heap.create_delete, Heap.delete_domain, Heap.dematerialize

abbrev Heap.materialize {Place Value : Type} [TopologicalSpace Place] (h : Heap Place Value) (p : Place)
  (s : Value) (hfresh : p ∉ Heap.domain Value) : Heap Place Value
Show details 
| h.materialize p s hfresh = h.create p s hfresh

Complexity: 61 (size of the value term)

Outer dependencies: Heap

Inner dependencies: Heap.create

Mathlib dependencies: Set, TopologicalSpace

Lean core dependencies: Not

Used by: Heap.materialize_dematerialize

abbrev Heap.dematerialize {Place Value : Type} [TopologicalSpace Place] (h : Heap Place Value) (p : Place)
  (hmem : p ∈ Heap.domain Value) : Heap Place Value
Show details 
| h.dematerialize p hmem = h.delete p hmem

Complexity: 55 (size of the value term)

Outer dependencies: Heap

Inner dependencies: Heap.delete

Mathlib dependencies: Set, TopologicalSpace

Used by: Heap.materialize_dematerialize

theorem Heap.create_domain {Place Value : Type} [TopologicalSpace Place] (h : Heap Place Value) (p : Place)
  (s : Value) (hfresh : p ∉ Heap.domain Value) : Heap.domain Value = insert p (Heap.domain Value)
Show details 
fun {Place Value} [TopologicalSpace Place] h p s hfresh => rfl

Complexity: 75 (size of the value term)

Dependencies: Heap, Heap.create

Mathlib dependencies: Set, TopologicalSpace

Lean core dependencies: Eq, Not, rfl

Used by: (none)

theorem Heap.delete_domain {Place Value : Type} [TopologicalSpace Place] (h : Heap Place Value) (p : Place)
  (hmem : p ∈ Heap.domain Value) : Heap.domain Value = Heap.domain Value \ {p}
Show details 
fun {Place Value} [TopologicalSpace Place] h p hmem => rfl

Complexity: 69 (size of the value term)

Dependencies: Heap, Heap.delete

Mathlib dependencies: Set, TopologicalSpace

Lean core dependencies: Eq, rfl

Used by: (none)

theorem Heap.create_delete {Place Value : Type} [TopologicalSpace Place] (h : Heap Place Value) (p : Place)
  (s : Value) (hfresh : p ∉ Heap.domain Value) : Heap.domain Value = Heap.domain Value
Show details 
fun {Place Value} [TopologicalSpace Place] h p s hfresh =>
  id
    (Set.ext fun q =>
      Eq.mpr
        (id
          (congrFun'
            (congrArg Iff
              (Eq.trans (Heap.create_delete._simp_1_1 q)
                (congr (congrArg And Heap.create_delete._simp_1_2)
                  (congrArg Not Heap.create_delete._simp_1_3))))
            (q ∈ Heap.domain Value)))
        {
          mp := fun a =>
            And.casesOn a fun left hne => Or.casesOn left (fun hq => absurd hq hne) fun hq => hq,
          mpr := fun hq => ⟨Or.inr hq, fun heq => hfresh (heq ▸ hq)⟩ })

Complexity: 1873 (size of the value term)

Dependencies: Heap, Heap.create, Heap.delete

Mathlib dependencies: Set, Set.ext, Set.mem_insert, Set.mem_insert_iff, Set.mem_sdiff, Set.mem_singleton_iff, TopologicalSpace

Lean core dependencies: And, Eq, Eq.mpr, Eq.trans, Iff, Not, Or, absurd, congr, congrArg, congrFun', id

Used by: Heap.materialize_dematerialize

theorem Heap.materialize_dematerialize {Place Value : Type} [TopologicalSpace Place] (h : Heap Place Value)
  (p : Place) (s : Value) (hfresh : p ∉ Heap.domain Value) : Heap.domain Value = Heap.domain Value
Show details 
fun {Place Value} [TopologicalSpace Place] h p s hfresh => Heap.create_delete h p s hfresh

Complexity: 61 (size of the value term)

Dependencies: Heap, Heap.dematerialize, Heap.materialize

Proof dependencies: Heap.create_delete

Mathlib dependencies: Set, Set.mem_insert, TopologicalSpace

Lean core dependencies: Eq, Not

Used by: (none)

structure Tower : Type 1
  • Level : ℤ → Type
  • Lang : ℤ → FirstOrder.Language
  • struct : (n : ℤ) → (self.Lang n).Structure (self.Level n)
  • finite : ∀ (n : ℤ), Finite (self.Level n)
  • stepPos : (n : ℕ) → self.Level ↑n → self.Level (↑n + 1)
  • stepNeg : (n : ℕ) → self.Level (-↑n) → self.Level (-↑(n + 1))
  • stepPos_injective : ∀ (n : ℕ), Function.Injective (self.stepPos n)
  • stepNeg_injective : ∀ (n : ℕ), Function.Injective (self.stepNeg n)
  • stepPos_not_surjective : ∀ (n : ℕ), ¬Function.Surjective (self.stepPos n)
  • stepNeg_not_surjective : ∀ (n : ℕ), ¬Function.Surjective (self.stepNeg n)
  • translatePos : (n : ℕ) → self.Lang ↑n →ᴸ self.Lang (↑n + 1)
  • translateNeg : (n : ℕ) → self.Lang (-↑n) →ᴸ self.Lang (-↑(n + 1))
  • stepPos_preserves_relation : ∀ (n : ℕ) {k : ℕ} (r : (self.Lang ↑n).Relations k) (x : Fin k → self.Level ↑n),
FirstOrder.Language.Structure.RelMap r x ↔
  FirstOrder.Language.Structure.RelMap ((self.translatePos n).onRelation r) (self.stepPos n ∘ x)
  • stepNeg_preserves_relation : ∀ (n : ℕ) {k : ℕ} (r : (self.Lang (-↑n)).Relations k) (x : Fin k → self.Level (-↑n)),
FirstOrder.Language.Structure.RelMap r x ↔
  FirstOrder.Language.Structure.RelMap ((self.translateNeg n).onRelation r) (self.stepNeg n ∘ x)
  • stepPos_preserves_function : ∀ (n : ℕ) {k : ℕ} (f : (self.Lang ↑n).Functions k) (x : Fin k → self.Level ↑n),
self.stepPos n (FirstOrder.Language.Structure.funMap f x) =
  FirstOrder.Language.Structure.funMap ((self.translatePos n).onFunction f) (self.stepPos n ∘ x)
  • stepNeg_preserves_function : ∀ (n : ℕ) {k : ℕ} (f : (self.Lang (-↑n)).Functions k) (x : Fin k → self.Level (-↑n)),
self.stepNeg n (FirstOrder.Language.Structure.funMap f x) =
  FirstOrder.Language.Structure.funMap ((self.translateNeg n).onFunction f) (self.stepNeg n ∘ x)
  • heap : (n : ℤ) → Heap (self.Level n) (self.Level n)
  • pointsTo : (n : ℤ) → (self.Lang n).Relations 2
  • reads_heap : ∀ (n : ℤ) (p q : self.Level n),
FirstOrder.Language.Structure.RelMap (self.pointsTo n) ![p, q] ↔
  ∃ (hp : p ∈ Heap.domain (self.Level n)), Heap.at_ p hp = q
  • lift : (n : ℤ) → self.Level (n - 1) → self.Level n
  • heap_from_below : ∀ (n : ℤ) (p : self.Level n) (hp : p ∈ Heap.domain (self.Level n)),
∃ v, Heap.at_ p hp = self.lift n v
  • stepPos_heap_domain : ∀ (n : ℕ), ∀ p ∈ Heap.domain (self.Level ↑n), self.stepPos n p ∈ Heap.domain (self.Level (↑n + 1))
  • stepPos_heap_at : ∀ (n : ℕ) (p : self.Level ↑n) (hp : p ∈ Heap.domain (self.Level ↑n)),
Heap.at_ (self.stepPos n p) ⋯ = self.stepPos n (Heap.at_ p hp)
  • stepNeg_heap_domain : ∀ (n : ℕ),
∀ p ∈ Heap.domain (self.Level (-↑n)), self.stepNeg n p ∈ Heap.domain (self.Level (-↑(n + 1)))
  • stepNeg_heap_at : ∀ (n : ℕ) (p : self.Level (-↑n)) (hp : p ∈ Heap.domain (self.Level (-↑n))),
Heap.at_ (self.stepNeg n p) ⋯ = self.stepNeg n (Heap.at_ p hp)
Show details

Outer dependencies: (none)

Inner dependencies: Heap

Mathlib dependencies: Finite, FirstOrder.Language, FirstOrder.Language.LHom, FirstOrder.Language.Structure, Matrix.vecCons, Matrix.vecEmpty, Set, TopologicalSpace

Lean core dependencies: Eq, Exists, Fin, Function.Injective, Function.Surjective, Function.comp, HEq, Iff, Int, Nat, Nat.cast, Not

Used by: Tower.LangBot, Tower.LangTop, Tower.LevelBot, Tower.LevelTop, Tower.Place, Tower.card_lt_stepNeg, Tower.card_lt_stepPos, Tower.card_zero_le_neg, Tower.card_zero_le_pos, Tower.grothendieckTopology, Tower.heapBot, Tower.heapTop, Tower.instInfiniteLevelBot, Tower.instInfiniteLevelTop, Tower.lang0ToBot, Tower.lang0ToTop, Tower.structBot, Tower.structTop, Tower.wholeHeap, arithTower, instNonemptyTower

def SeqColimit.stepTo {G : ℕ → Type} (step : (n : ℕ) → G n → G (n + 1)) (m n : ℕ) (h : m ≤ n) :
  G m → G n
Show details 
| SeqColimit.stepTo step m n h a✝ = Nat.leRecOn h (fun k => step k) a✝

Complexity: 73 (size of the value term)

Outer dependencies: (none)

Mathlib dependencies: Nat.leRecOn

Lean core dependencies: Nat

Used by: SeqColimit.Rel, SeqColimit.Rel.refl, SeqColimit.Rel.symm, SeqColimit.Rel.trans, SeqColimit.freshSeq_lt_ne, SeqColimit.mk_injective, SeqColimit.mk_stepTo, SeqColimit.stepTo_self, SeqColimit.stepTo_succ, SeqColimit.stepTo_trans, Tower.structBot, Tower.structTop, arithFromNat_toNat, arithPlus_iff, arithPlus_mk_eq, arithStepTo_val, arithSucc_iff, arithSucc_mk_eq, arithToNat, arithTranslatePos_stepTo_eq

theorem SeqColimit.stepTo_succ {G : ℕ → Type} (step : (n : ℕ) → G n → G (n + 1)) {n m : ℕ} (h : n ≤ m)
  (x : G n) : SeqColimit.stepTo step n (m + 1) ⋯ x = step m (SeqColimit.stepTo step n m h x)
Show details 
fun {G} step {n m} h x => Nat.leRecOn_succ h x

Complexity: 115 (size of the value term)

Dependencies: SeqColimit.stepTo

Mathlib dependencies: Nat.leRecOn_succ

Lean core dependencies: Eq, Nat, Nat.le_succ

Used by: SeqColimit.freshSeq_lt_ne, arithStepTo_val, arithTranslatePos_stepTo_eq

theorem SeqColimit.stepTo_trans {G : ℕ → Type} (step : (n : ℕ) → G n → G (n + 1)) {n m k : ℕ} (h1 : n ≤ m)
  (h2 : m ≤ k) (x : G n) :
  SeqColimit.stepTo step n k ⋯ x = SeqColimit.stepTo step m k h2 (SeqColimit.stepTo step n m h1 x)
Show details 
fun {G} step {n m k} h1 h2 x => Nat.leRecOn_trans h1 h2 x

Complexity: 89 (size of the value term)

Dependencies: SeqColimit.stepTo

Mathlib dependencies: Nat.leRecOn_trans

Lean core dependencies: Eq, Nat

Used by: SeqColimit.Rel.trans, SeqColimit.freshSeq_lt_ne

def SeqColimit.Rel {G : ℕ → Type} (step : (n : ℕ) → G n → G (n + 1)) :
  (n : ℕ) × G n → (n : ℕ) × G n → Prop
Show details 
| SeqColimit.Rel step a b =
  ∃ k,
    ∃ (ha : a.fst ≤ k) (hb : b.fst ≤ k),
      SeqColimit.stepTo step a.fst k ha a.snd = SeqColimit.stepTo step b.fst k hb b.snd

Complexity: 221 (size of the value term)

Outer dependencies: (none)

Inner dependencies: SeqColimit.stepTo

Lean core dependencies: Eq, Exists, Nat, Sigma

Used by: SeqColimit.Rel.refl, SeqColimit.Rel.symm, SeqColimit.Rel.trans, SeqColimit.setoid

theorem SeqColimit.Rel.refl {G : ℕ → Type} (step : (n : ℕ) → G n → G (n + 1)) (a : (n : ℕ) × G n) :
  SeqColimit.Rel step a a
Show details 
fun {G} step a => Exists.intro a.fst (Exists.intro le_rfl (Exists.intro le_rfl rfl))

Complexity: 745 (size of the value term)

Dependencies: SeqColimit.Rel

Proof dependencies: SeqColimit.stepTo

Mathlib dependencies: le_rfl

Lean core dependencies: Eq, Exists, Nat, Sigma, rfl

Used by: SeqColimit.setoid

theorem SeqColimit.Rel.symm {G : ℕ → Type} (step : (n : ℕ) → G n → G (n + 1)) {a b : (n : ℕ) × G n}
  (h : SeqColimit.Rel step a b) : SeqColimit.Rel step b a
Show details 
fun {G} step {a b} h =>
  match h with
  | Exists.intro k (Exists.intro ha (Exists.intro hb heq)) =>
    Exists.intro k (Exists.intro hb (Exists.intro ha (Eq.symm heq)))

Complexity: 735 (size of the value term)

Dependencies: SeqColimit.Rel

Proof dependencies: SeqColimit.stepTo

Lean core dependencies: Eq, Eq.symm, Exists, Nat, Sigma

Used by: SeqColimit.setoid

theorem SeqColimit.Rel.trans {G : ℕ → Type} (step : (n : ℕ) → G n → G (n + 1)) {a b c : (n : ℕ) × G n}
  (hab : SeqColimit.Rel step a b) (hbc : SeqColimit.Rel step b c) : SeqColimit.Rel step a c
Show details 
fun {G} step {a b c} hab hbc =>
  Exists.casesOn hab fun k1 h =>
    Exists.casesOn h fun ha1 h =>
      Exists.casesOn h fun hb1 heq1 =>
        Exists.casesOn hbc fun k2 h =>
          Exists.casesOn h fun hb2 h =>
            Exists.casesOn h fun hc2 heq2 =>
              Exists.intro (max k1 k2)
                (Exists.intro (LE.le.trans ha1 (le_max_left k1 k2))
                  (Exists.intro (LE.le.trans hc2 (le_max_right k1 k2))
                    (have step1 :=
                      Eq.mpr
                        (id
                          (congrArg
                            (fun _a =>
                              _a =
                                SeqColimit.stepTo step b.fst (max k1 k2)
                                  (LE.le.trans hb1 (le_max_left k1 k2)) b.snd)
                            (SeqColimit.stepTo_trans step ha1 (le_max_left k1 k2) a.snd)))
                        (Eq.mpr
                          (id
                            (congrArg
                              (fun _a =>
                                SeqColimit.stepTo step k1 (max k1 k2) (le_max_left k1 k2)
                                    (SeqColimit.stepTo step a.fst k1 ha1 a.snd) =
                                  _a)
                              (SeqColimit.stepTo_trans step hb1 (le_max_left k1 k2) b.snd)))
                          (Eq.mpr
                            (id
                              (congrArg
                                (fun _a =>
                                  SeqColimit.stepTo step k1 (max k1 k2) (le_max_left k1 k2) _a =
                                    SeqColimit.stepTo step k1 (max k1 k2) (le_max_left k1 k2)
                                      (SeqColimit.stepTo step b.fst k1 hb1 b.snd))
                                heq1))
                            (Eq.refl
                              (SeqColimit.stepTo step k1 (max k1 k2) (le_max_left k1 k2)
                                (SeqColimit.stepTo step b.fst k1 hb1 b.snd)))));
                    have step2 :=
                      Eq.mpr
                        (id
                          (congrArg
                            (fun _a =>
                              _a =
                                SeqColimit.stepTo step c.fst (max k1 k2)
                                  (LE.le.trans hc2 (le_max_right k1 k2)) c.snd)
                            (SeqColimit.stepTo_trans step hb2 (le_max_right k1 k2) b.snd)))
                        (Eq.mpr
                          (id
                            (congrArg
                              (fun _a =>
                                SeqColimit.stepTo step k2 (max k1 k2) (le_max_right k1 k2)
                                    (SeqColimit.stepTo step b.fst k2 hb2 b.snd) =
                                  _a)
                              (SeqColimit.stepTo_trans step hc2 (le_max_right k1 k2) c.snd)))
                          (Eq.mpr
                            (id
                              (congrArg
                                (fun _a =>
                                  SeqColimit.stepTo step k2 (max k1 k2) (le_max_right k1 k2) _a =
                                    SeqColimit.stepTo step k2 (max k1 k2) (le_max_right k1 k2)
                                      (SeqColimit.stepTo step c.fst k2 hc2 c.snd))
                                heq2))
                            (Eq.refl
                              (SeqColimit.stepTo step k2 (max k1 k2) (le_max_right k1 k2)
                                (SeqColimit.stepTo step c.fst k2 hc2 c.snd)))));
                    Eq.trans step1 step2)))

Complexity: 9389 (size of the value term)

Dependencies: SeqColimit.Rel

Proof dependencies: SeqColimit.stepTo, SeqColimit.stepTo_trans

Mathlib dependencies: le_max_left, le_max_right

Lean core dependencies: Eq, Eq.mpr, Eq.trans, Exists, Nat, Sigma, congrArg, id

Used by: SeqColimit.setoid

def SeqColimit.setoid {G : ℕ → Type} (step : (n : ℕ) → G n → G (n + 1)) : Setoid ((n : ℕ) × G n)
Show details 
| SeqColimit.setoid step = { r := SeqColimit.Rel step, iseqv := ⋯ }

Complexity: 61 (size of the value term)

Outer dependencies: (none)

Inner dependencies: SeqColimit.Rel, SeqColimit.Rel.refl, SeqColimit.Rel.symm, SeqColimit.Rel.trans

Lean core dependencies: Nat, Setoid, Sigma

Used by: SeqColimit, SeqColimit.freshSeq_lt_ne, SeqColimit.mk, SeqColimit.mk_injective, SeqColimit.mk_stepTo, Tower.structBot, Tower.structTop, arithFromNat_toNat, arithPlus_iff, arithSucc_iff, arithToNat

def SeqColimit {G : ℕ → Type} (step : (n : ℕ) → G n → G (n + 1)) : Type
Show details 
| SeqColimit step = Quotient (SeqColimit.setoid step)

Complexity: 55 (size of the value term)

Outer dependencies: (none)

Inner dependencies: SeqColimit.setoid

Lean core dependencies: Nat, Quotient, Sigma

Used by: SeqColimit.freshSeq, SeqColimit.freshSeq_injective, SeqColimit.freshSeq_lt_ne, SeqColimit.infinite, SeqColimit.mk, SeqColimit.mk_injective, SeqColimit.mk_stepTo, Tower.LangBot, Tower.LangTop, Tower.LevelBot, Tower.LevelTop, arithPlus_iff, arithPlus_mk_eq, arithSucc_iff, arithSucc_mk_eq

def SeqColimit.mk {G : ℕ → Type} (step : (n : ℕ) → G n → G (n + 1)) (n : ℕ) (x : G n) : SeqColimit step
Show details 
| SeqColimit.mk step n x = ⟦⟨n, x⟩⟧

Complexity: 75 (size of the value term)

Outer dependencies: SeqColimit

Inner dependencies: SeqColimit.setoid

Lean core dependencies: Nat, Quotient.mk, Sigma

Used by: SeqColimit.freshSeq, SeqColimit.mk_injective, SeqColimit.mk_stepTo, Tower.heapBot, Tower.heapTop, Tower.lang0ToBot, Tower.lang0ToTop, Tower.structBot, Tower.structTop, arithFromNat, arithPlus, arithPlus_iff, arithPlus_mk_eq, arithSucc, arithSucc_iff, arithSucc_mk_eq, arithToNat_mk

theorem SeqColimit.stepTo_self {G : ℕ → Type} (step : (n : ℕ) → G n → G (n + 1)) (n : ℕ) (x : G n) :
  SeqColimit.stepTo step n n ⋯ x = x
Show details 
fun {G} step n x => Nat.leRecOn_self x

Complexity: 53 (size of the value term)

Dependencies: SeqColimit.stepTo

Mathlib dependencies: Nat.leRecOn_self, le_refl

Lean core dependencies: Eq, Nat

Used by: SeqColimit.mk_stepTo, arithTranslatePos_stepTo_eq

theorem SeqColimit.mk_stepTo {G : ℕ → Type} (step : (n : ℕ) → G n → G (n + 1)) {n m : ℕ} (h : n ≤ m)
  (x : G n) : SeqColimit.mk step m (SeqColimit.stepTo step n m h x) = SeqColimit.mk step n x
Show details 
fun {G} step {n m} h x =>
  Quotient.sound
    (Exists.intro m
      (Exists.intro le_rfl
        (Exists.intro h
          (Eq.mpr
            (id
              (congrArg (fun _a => _a = SeqColimit.stepTo step ⟨n, x⟩.fst m h ⟨n, x⟩.snd)
                (SeqColimit.stepTo_self step ⟨m, SeqColimit.stepTo step n m h x⟩.fst
                  ⟨m, SeqColimit.stepTo step n m h x⟩.snd)))
            (Eq.refl ⟨m, SeqColimit.stepTo step n m h x⟩.snd)))))

Complexity: 2059 (size of the value term)

Dependencies: SeqColimit, SeqColimit.mk, SeqColimit.stepTo

Proof dependencies: SeqColimit.setoid, SeqColimit.stepTo_self

Mathlib dependencies: le_refl, le_rfl

Lean core dependencies: Eq, Eq.mpr, Exists, Nat, Quotient.sound, Sigma, congrArg, id

Used by: arithPlus_iff, arithPlus_mk_eq, arithSucc_iff, arithSucc_mk_eq

theorem SeqColimit.mk_injective {G : ℕ → Type} (step : (n : ℕ) → G n → G (n + 1))
  (step_inj : ∀ (n : ℕ), Function.Injective (step n)) (n : ℕ) :
  Function.Injective (SeqColimit.mk step n)
Show details 
fun {G} step step_inj n ⦃x y⦄ hxy =>
  Exists.casesOn (Quotient.exact hxy) fun k h =>
    Exists.casesOn h fun hx h =>
      Exists.casesOn h fun hy heq => Nat.leRecOn_injective hx (fun j => step j) step_inj heq

Complexity: 2075 (size of the value term)

Dependencies: SeqColimit, SeqColimit.mk

Proof dependencies: SeqColimit.setoid, SeqColimit.stepTo

Mathlib dependencies: Nat.leRecOn_injective

Lean core dependencies: Eq, Exists, Function.Injective, Nat, Quotient.exact, Sigma

Used by: (none)

theorem SeqColimit.exists_not_mem_range {G : ℕ → Type} (step : (n : ℕ) → G n → G (n + 1)) (n : ℕ)
  (hns : ¬Function.Surjective (step n)) : ∃ y, ∀ (x : G n), step n x ≠ y
Show details 
fun {G} step n hns =>
  Exists.casesOn (not_forall.mp hns) fun y hy => Exists.intro y fun x hx => hy (Exists.intro x hx)

Complexity: 967 (size of the value term)

Dependencies: (none)

Lean core dependencies: Classical.not_forall, Eq, Exists, Function.Surjective, Nat, Ne, Not

Used by: SeqColimit.fresh, SeqColimit.fresh_spec

def SeqColimit.fresh {G : ℕ → Type} (step : (n : ℕ) → G n → G (n + 1))
  (not_surj : ∀ (n : ℕ), ¬Function.Surjective (step n)) (n : ℕ) : G (n + 1)
Show details 
| SeqColimit.fresh step not_surj n = ⋯.choose

Complexity: 191 (size of the value term)

Outer dependencies: (none)

Inner dependencies: SeqColimit.exists_not_mem_range

Lean core dependencies: Exists.choose, Function.Surjective, Nat, Ne, Not

Used by: SeqColimit.freshSeq, SeqColimit.freshSeq_lt_ne, SeqColimit.fresh_spec

theorem SeqColimit.fresh_spec {G : ℕ → Type} (step : (n : ℕ) → G n → G (n + 1))
  (not_surj : ∀ (n : ℕ), ¬Function.Surjective (step n)) (n : ℕ) (x : G n) :
  step n x ≠ SeqColimit.fresh step not_surj n
Show details 
fun {G} step not_surj n x =>
  Exists.choose_spec (SeqColimit.exists_not_mem_range step n (not_surj n)) x

Complexity: 199 (size of the value term)

Dependencies: SeqColimit.fresh

Proof dependencies: SeqColimit.exists_not_mem_range

Lean core dependencies: Exists.choose_spec, Function.Surjective, Nat, Ne, Not

Used by: SeqColimit.freshSeq_lt_ne

def SeqColimit.freshSeq {G : ℕ → Type} (step : (n : ℕ) → G n → G (n + 1))
  (not_surj : ∀ (n : ℕ), ¬Function.Surjective (step n)) (n : ℕ) : SeqColimit step
Show details 
| SeqColimit.freshSeq step not_surj n = SeqColimit.mk step (n + 1) (SeqColimit.fresh step not_surj n)

Complexity: 123 (size of the value term)

Outer dependencies: SeqColimit

Inner dependencies: SeqColimit.fresh, SeqColimit.mk

Lean core dependencies: Function.Surjective, Nat, Not

Used by: SeqColimit.freshSeq_injective, SeqColimit.freshSeq_lt_ne, SeqColimit.infinite

theorem SeqColimit.freshSeq_lt_ne {G : ℕ → Type} (step : (n : ℕ) → G n → G (n + 1))
  (not_surj : ∀ (n : ℕ), ¬Function.Surjective (step n))
  (step_inj : ∀ (n : ℕ), Function.Injective (step n)) {n m : ℕ} (hlt : n < m) :
  SeqColimit.freshSeq step not_surj n ≠ SeqColimit.freshSeq step not_surj m
Show details 
fun {G} step not_surj step_inj {n m} hlt heq =>
  have hnm := hlt;
  Exists.casesOn (Quotient.exact heq) fun k h =>
    Exists.casesOn h fun hnk h =>
      Exists.casesOn h fun hmk hk =>
        have h' := LE.le.trans hnm (Nat.le_succ m);
        have e1 := SeqColimit.stepTo_trans step h' hmk (SeqColimit.fresh step not_surj n);
        have hinj := Nat.leRecOn_injective hmk (fun j => step j) step_inj;
        have e2 :=
          hinj
            (Eq.mp
              (congrArg
                (fun _a =>
                  _a =
                    SeqColimit.stepTo step ⟨m + 1, SeqColimit.fresh step not_surj m⟩.fst k hmk
                      ⟨m + 1, SeqColimit.fresh step not_surj m⟩.snd)
                e1)
              hk);
        have e3 := SeqColimit.stepTo_succ step hnm (SeqColimit.fresh step not_surj n);
        SeqColimit.fresh_spec step not_surj m
          (SeqColimit.stepTo step (n + 1) m hnm (SeqColimit.fresh step not_surj n))
          (Eq.mp (congrArg (fun _a => _a = SeqColimit.fresh step not_surj m) e3) e2)

Complexity: 6079 (size of the value term)

Dependencies: SeqColimit, SeqColimit.freshSeq

Proof dependencies: SeqColimit.fresh, SeqColimit.fresh_spec, SeqColimit.setoid, SeqColimit.stepTo, SeqColimit.stepTo_succ, SeqColimit.stepTo_trans

Mathlib dependencies: Nat.leRecOn_injective

Lean core dependencies: Eq, Eq.mp, Exists, False, Function.Injective, Function.Surjective, Nat, Nat.le_succ, Ne, Not, Quotient.exact, Sigma, congrArg

Used by: SeqColimit.freshSeq_injective

theorem SeqColimit.freshSeq_injective {G : ℕ → Type} (step : (n : ℕ) → G n → G (n + 1))
  (not_surj : ∀ (n : ℕ), ¬Function.Surjective (step n))
  (step_inj : ∀ (n : ℕ), Function.Injective (step n)) :
  Function.Injective (SeqColimit.freshSeq step not_surj)
Show details 
fun {G} step not_surj step_inj ⦃n m⦄ heq =>
  Or.casesOn (lt_trichotomy n m)
    (fun h => absurd heq (SeqColimit.freshSeq_lt_ne step not_surj step_inj h)) fun h =>
    Or.casesOn h (fun h => h) fun h =>
      absurd (Eq.symm heq) (SeqColimit.freshSeq_lt_ne step not_surj step_inj h)

Complexity: 581 (size of the value term)

Dependencies: SeqColimit, SeqColimit.freshSeq

Proof dependencies: SeqColimit.freshSeq_lt_ne

Mathlib dependencies: lt_trichotomy

Lean core dependencies: Eq, Eq.symm, Function.Injective, Function.Surjective, Nat, Not, Or, absurd

Used by: SeqColimit.infinite

theorem SeqColimit.infinite {G : ℕ → Type} (step : (n : ℕ) → G n → G (n + 1))
  (not_surj : ∀ (n : ℕ), ¬Function.Surjective (step n))
  (step_inj : ∀ (n : ℕ), Function.Injective (step n)) : Infinite (SeqColimit step)
Show details 
fun {G} step not_surj step_inj =>
  Infinite.of_injective (SeqColimit.freshSeq step not_surj)
    (SeqColimit.freshSeq_injective step not_surj step_inj)

Complexity: 149 (size of the value term)

Dependencies: SeqColimit

Proof dependencies: SeqColimit.freshSeq, SeqColimit.freshSeq_injective

Mathlib dependencies: Infinite, Infinite.of_injective

Lean core dependencies: Function.Injective, Function.Surjective, Nat, Not

Used by: Tower.instInfiniteLevelBot, Tower.instInfiniteLevelTop

def Tower.LevelBot (T : Tower) : Type
Show details 
| T.LevelBot = SeqColimit T.stepNeg

Complexity: 27 (size of the value term)

Outer dependencies: Tower

Inner dependencies: SeqColimit

Lean core dependencies: Int, Nat, Nat.cast

Used by: Tower.heapBot, Tower.instInfiniteLevelBot, Tower.structBot

instance Tower.instInfiniteLevelTop (T : Tower) : Infinite T.LevelTop
Show details 
fun T => SeqColimit.infinite T.stepPos T.stepPos_not_surjective T.stepPos_injective

Complexity: 29 (size of the value term)

Outer dependencies: Tower, Tower.LevelTop

Inner dependencies: SeqColimit.infinite

Mathlib dependencies: Infinite

Lean core dependencies: Int, Nat, Nat.cast

Used by: (none)

instance Tower.instInfiniteLevelBot (T : Tower) : Infinite T.LevelBot
Show details 
fun T => SeqColimit.infinite T.stepNeg T.stepNeg_not_surjective T.stepNeg_injective

Complexity: 35 (size of the value term)

Outer dependencies: Tower, Tower.LevelBot

Inner dependencies: SeqColimit.infinite

Mathlib dependencies: Infinite

Lean core dependencies: Int, Nat, Nat.cast

Used by: (none)

def Tower.LangTop (T : Tower) : FirstOrder.Language
Show details 
| T.LangTop =
  { Functions := fun k => SeqColimit fun n f => (T.translatePos n).onFunction f,
    Relations := fun k => SeqColimit fun n r => (T.translatePos n).onRelation r }

Complexity: 203 (size of the value term)

Outer dependencies: Tower

Inner dependencies: SeqColimit

Mathlib dependencies: FirstOrder.Language

Lean core dependencies: Int, Nat, Nat.cast

Used by: Tower.lang0ToTop, Tower.structTop, arithPlus, arithPlus_iff, arithPlus_succ, arithPlus_zero, arithSucc, arithSucc_functional, arithSucc_iff, arithSucc_iff_eq_succFun, arithSucc_no_fixed_point, arithSucc_total, arithZero_not_succ, arithZero_unique

def Tower.LangBot (T : Tower) : FirstOrder.Language
Show details 
| T.LangBot =
  { Functions := fun k => SeqColimit fun n f => (T.translateNeg n).onFunction f,
    Relations := fun k => SeqColimit fun n r => (T.translateNeg n).onRelation r }

Complexity: 251 (size of the value term)

Outer dependencies: Tower

Inner dependencies: SeqColimit

Mathlib dependencies: FirstOrder.Language

Lean core dependencies: Int, Nat, Nat.cast

Used by: Tower.lang0ToBot, Tower.structBot

def Tower.structTop (T : Tower) : T.LangTop.Structure T.LevelTop
Show details 
| T.structTop =
  {
    funMap := fun {k} f x =>
      let nf := (Quotient.out f).fst;
      have f' := (Quotient.out f).snd;
      let nx := fun i => (Quotient.out (x i)).fst;
      let N := max nf (Finset.univ.sup nx);
      have hnf := ⋯;
      have hx := ⋯;
      SeqColimit.mk T.stepPos N
        (FirstOrder.Language.Structure.funMap
          (SeqColimit.stepTo (fun n f => (T.translatePos n).onFunction f) nf N hnf f') fun i =>
          SeqColimit.stepTo T.stepPos (nx i) N ⋯ (Quotient.out (x i)).snd),
    RelMap := fun {k} r x =>
      ∃ n rn y,
        r = SeqColimit.mk (fun m r => (T.translatePos m).onRelation r) n rn ∧
          (∀ (i : Fin k), x i = SeqColimit.mk T.stepPos n (y i)) ∧
            FirstOrder.Language.Structure.RelMap rn y }

Complexity: 1235 (size of the value term)

Outer dependencies: Tower, Tower.LangTop, Tower.LevelTop

Inner dependencies: SeqColimit.mk, SeqColimit.setoid, SeqColimit.stepTo

Mathlib dependencies: Finset.le_sup, Finset.mem_univ, Finset.sup, Finset.univ, FirstOrder.Language.Structure, Quotient.out, le_max_left, le_max_right

Lean core dependencies: And, Eq, Exists, Fin, Int, Nat, Nat.cast, Sigma

Used by: arithPlus_iff, arithPlus_succ, arithPlus_zero, arithSucc_functional, arithSucc_iff, arithSucc_iff_eq_succFun, arithSucc_no_fixed_point, arithSucc_total, arithZero_not_succ, arithZero_unique

def Tower.structBot (T : Tower) : T.LangBot.Structure T.LevelBot
Show details 
| T.structBot =
  {
    funMap := fun {k} f x =>
      let nf := (Quotient.out f).fst;
      have f' := (Quotient.out f).snd;
      let nx := fun i => (Quotient.out (x i)).fst;
      let N := max nf (Finset.univ.sup nx);
      have hnf := ⋯;
      have hx := ⋯;
      SeqColimit.mk T.stepNeg N
        (FirstOrder.Language.Structure.funMap
          (SeqColimit.stepTo (fun n f => (T.translateNeg n).onFunction f) nf N hnf f') fun i =>
          SeqColimit.stepTo T.stepNeg (nx i) N ⋯ (Quotient.out (x i)).snd),
    RelMap := fun {k} r x =>
      ∃ n rn y,
        r = SeqColimit.mk (fun m r => (T.translateNeg m).onRelation r) n rn ∧
          (∀ (i : Fin k), x i = SeqColimit.mk T.stepNeg n (y i)) ∧
            FirstOrder.Language.Structure.RelMap rn y }

Complexity: 1511 (size of the value term)

Outer dependencies: Tower, Tower.LangBot, Tower.LevelBot

Inner dependencies: SeqColimit.mk, SeqColimit.setoid, SeqColimit.stepTo

Mathlib dependencies: Finset.le_sup, Finset.mem_univ, Finset.sup, Finset.univ, FirstOrder.Language.Structure, Quotient.out, le_max_left, le_max_right

Lean core dependencies: And, Eq, Exists, Fin, Int, Nat, Nat.cast, Sigma

Used by: (none)

theorem Tower.card_lt_stepPos (T : Tower) (n : ℕ) : Nat.card (T.Level ↑n) < Nat.card (T.Level (↑n + 1))
Show details 
fun T n =>
  Eq.mpr
    (id (congrArg (fun _a => _a < Nat.card (T.Level (↑n + 1))) (Eq.symm Fintype.card_eq_nat_card)))
    (Eq.mpr
      (id (congrArg (fun _a => Fintype.card (T.Level ↑n) < _a) (Eq.symm Fintype.card_eq_nat_card)))
      (Fintype.card_lt_of_injective_not_surjective (T.stepPos n) (T.stepPos_injective n)
        (T.stepPos_not_surjective n)))

Complexity: 1633 (size of the value term)

Dependencies: Tower

Mathlib dependencies: Fintype.card, Fintype.card_eq_nat_card, Fintype.card_lt_of_injective_not_surjective, Fintype.ofFinite, Nat.card

Lean core dependencies: Eq, Eq.mpr, Eq.symm, Int, Nat, Nat.cast, congrArg, id

Used by: Tower.card_zero_le_pos

theorem Tower.card_lt_stepNeg (T : Tower) (n : ℕ) :
  Nat.card (T.Level (-↑n)) < Nat.card (T.Level (-↑(n + 1)))
Show details 
fun T n =>
  Eq.mpr
    (id
      (congrArg (fun _a => _a < Nat.card (T.Level (-↑(n + 1)))) (Eq.symm Fintype.card_eq_nat_card)))
    (Eq.mpr
      (id
        (congrArg (fun _a => Fintype.card (T.Level (-↑n)) < _a) (Eq.symm Fintype.card_eq_nat_card)))
      (Fintype.card_lt_of_injective_not_surjective (T.stepNeg n) (T.stepNeg_injective n)
        (T.stepNeg_not_surjective n)))

Complexity: 2017 (size of the value term)

Dependencies: Tower

Mathlib dependencies: Fintype.card, Fintype.card_eq_nat_card, Fintype.card_lt_of_injective_not_surjective, Fintype.ofFinite, Nat.card

Lean core dependencies: Eq, Eq.mpr, Eq.symm, Int, Nat, Nat.cast, congrArg, id

Used by: Tower.card_zero_le_neg

theorem Tower.card_zero_le_pos (T : Tower) (n : ℕ) : Nat.card (T.Level 0) ≤ Nat.card (T.Level ↑n)
Show details 
fun T n =>
  Nat.recAux (le_refl (Nat.card (T.Level 0)))
    (fun n ih => LE.le.trans ih (LT.lt.le (Tower.card_lt_stepPos T n))) n

Complexity: 245 (size of the value term)

Dependencies: Tower

Proof dependencies: Tower.card_lt_stepPos

Mathlib dependencies: Nat.card, le_refl

Lean core dependencies: Int, Nat, Nat.cast, Nat.recAux

Used by: (none)

theorem Tower.card_zero_le_neg (T : Tower) (n : ℕ) : Nat.card (T.Level 0) ≤ Nat.card (T.Level (-↑n))
Show details 
fun T n =>
  Nat.recAux (le_refl (Nat.card (T.Level 0)))
    (fun n ih => LE.le.trans ih (LT.lt.le (Tower.card_lt_stepNeg T n))) n

Complexity: 281 (size of the value term)

Dependencies: Tower

Proof dependencies: Tower.card_lt_stepNeg

Mathlib dependencies: Nat.card, le_refl

Lean core dependencies: Int, Nat, Nat.cast, Nat.recAux

Used by: (none)

def Tower.Place (T : Tower) : Type
Show details 
| T.Place = ((n : ℤ) × T.Level n)

Complexity: 13 (size of the value term)

Outer dependencies: Tower

Lean core dependencies: Int, Sigma

Used by: Tower.wholeHeap

def Tower.wholeHeap (T : Tower) : Heap T.Place T.Place
Show details 
| T.wholeHeap =
  { domain := {p | p.snd ∈ Heap.domain (T.Level p.fst)},
    at_ := fun p hp => ⟨p.fst, Heap.at_ p.snd hp⟩ }

Complexity: 1647 (size of the value term)

Outer dependencies: Heap, Tower, Tower.Place

Mathlib dependencies: Set, TopologicalSpace, setOf

Lean core dependencies: Int

Used by: (none)

def Tower.grothendieckTopology (T : Tower) (n : ℤ) :
  CategoryTheory.GrothendieckTopology (TopologicalSpace.Opens (T.Level n))
Show details 
| T.grothendieckTopology n = Heap.grothendieckTopology (T.Level n)

Complexity: 175 (size of the value term)

Outer dependencies: Tower

Inner dependencies: Heap.grothendieckTopology

Mathlib dependencies: CategoryTheory.GrothendieckTopology, TopologicalSpace, TopologicalSpace.Opens

Lean core dependencies: Int

Used by: (none)

def Tower.heapTop (T : Tower) : Heap T.LevelTop T.LevelTop
Show details 
| T.heapTop =
  { domain := {p | ∃ n p', p = SeqColimit.mk T.stepPos n p' ∧ p' ∈ Heap.domain (T.Level ↑n)},
    at_ := fun x hp => SeqColimit.mk T.stepPos (Exists.choose hp) (Heap.at_ ⋯.choose ⋯) }

Complexity: 21221 (size of the value term)

Outer dependencies: Heap, Tower, Tower.LevelTop

Inner dependencies: SeqColimit.mk

Mathlib dependencies: Set, TopologicalSpace, setOf

Lean core dependencies: And, Eq, Exists, Exists.choose, Exists.choose_spec, Int, Nat, Nat.cast

Used by: (none)

def Tower.heapBot (T : Tower) : Heap T.LevelBot T.LevelBot
Show details 
| T.heapBot =
  { domain := {p | ∃ n p', p = SeqColimit.mk T.stepNeg n p' ∧ p' ∈ Heap.domain (T.Level (-↑n))},
    at_ := fun x hp => SeqColimit.mk T.stepNeg (Exists.choose hp) (Heap.at_ ⋯.choose ⋯) }

Complexity: 29147 (size of the value term)

Outer dependencies: Heap, Tower, Tower.LevelBot

Inner dependencies: SeqColimit.mk

Mathlib dependencies: Set, TopologicalSpace, setOf

Lean core dependencies: And, Eq, Exists, Exists.choose, Exists.choose_spec, Int, Nat, Nat.cast

Used by: (none)

The peoples at the two extremes only understand each other, if at all, through the root language they all grew from.

def Tower.lang0ToTop (T : Tower) : T.Lang 0 →ᴸ T.LangTop
Show details 
| T.lang0ToTop =
  { onFunction := fun {x} f => SeqColimit.mk (fun n f => (T.translatePos n).onFunction f) 0 f,
    onRelation := fun {x} r => SeqColimit.mk (fun n r => (T.translatePos n).onRelation r) 0 r }

Complexity: 281 (size of the value term)

Outer dependencies: Tower, Tower.LangTop

Inner dependencies: SeqColimit.mk

Mathlib dependencies: FirstOrder.Language.LHom

Lean core dependencies: Int, Nat, Nat.cast

Used by: (none)

def Tower.lang0ToBot (T : Tower) : T.Lang 0 →ᴸ T.LangBot
Show details 
| T.lang0ToBot =
  { onFunction := fun {x} f => SeqColimit.mk (fun n f => (T.translateNeg n).onFunction f) 0 f,
    onRelation := fun {x} r => SeqColimit.mk (fun n r => (T.translateNeg n).onRelation r) 0 r }

Complexity: 329 (size of the value term)

Outer dependencies: Tower, Tower.LangBot

Inner dependencies: SeqColimit.mk

Mathlib dependencies: FirstOrder.Language.LHom

Lean core dependencies: Int, Nat, Nat.cast

Used by: (none)

def arithLang : FirstOrder.Language
Show details 
| arithLang =
  { Functions := fun x => Empty,
    Relations := fun x =>
      match x with
      | 2 => Bool
      | 3 => Unit
      | x => Empty }

Complexity: 27 (size of the value term)

Outer dependencies: (none)

Mathlib dependencies: FirstOrder.Language

Lean core dependencies: Bool, Empty, Eq, Eq.ndrec_symm, Nat, Not, Unit, Unit.unit, dite

Used by: arithPlus, arithPlus_iff, arithPlus_mk_eq, arithStruct, arithStruct_congr, arithSucc, arithSucc_iff, arithSucc_mk_eq, arithTower, arithTranslatePos_stepTo_eq

def arithStruct (k : ℕ) : arithLang.Structure (Fin (k + 1))
Show details 
| arithStruct k =
  { funMap := fun {x} f x_1 => Empty.elim f,
    RelMap := fun {m} r x =>
      match m, r, x with
      | 2, true, x => ↑(x 1) = ↑(x 0) + 1
      | 2, false, x => False
      | 3, x, x_1 => ↑(x_1 2) = ↑(x_1 0) + ↑(x_1 1)
      | 0, r, x => Empty.elim r
      | 1, r, x => Empty.elim r
      | n.succ.succ.succ.succ, r, x => Empty.elim r }

Complexity: 903 (size of the value term)

Outer dependencies: arithLang

Mathlib dependencies: FirstOrder.Language.Structure

Lean core dependencies: Empty.elim, Eq, False, Fin, Nat

Used by: arithStruct_congr, arithTower

theorem arithStruct_congr {k1 k2 m : ℕ} (r : arithLang.Relations m) (x1 : Fin m → Fin (k1 + 1))
  (x2 : Fin m → Fin (k2 + 1)) (h : ∀ (i : Fin m), ↑(x1 i) = ↑(x2 i)) :
  FirstOrder.Language.Structure.RelMap r x1 ↔ FirstOrder.Language.Structure.RelMap r x2
Show details 
fun {k1 k2 m} r x1 x2 h =>
  match m, r, x1, x2, h with
  | 2, true, x1, x2, h =>
    id
      (Eq.mpr (id (congrArg (fun _a => _a = ↑(x1 0) + 1 ↔ ↑(x2 1) = ↑(x2 0) + 1) (h 1)))
        (Eq.mpr (id (congrArg (fun _a => ↑(x2 1) = _a + 1 ↔ ↑(x2 1) = ↑(x2 0) + 1) (h 0))) Iff.rfl))
  | 2, false, x1, x2, h => id Iff.rfl
  | 3, PUnit.unit, x1, x2, h =>
    id
      (Eq.mpr (id (congrArg (fun _a => _a = ↑(x1 0) + ↑(x1 1) ↔ ↑(x2 2) = ↑(x2 0) + ↑(x2 1)) (h 2)))
        (Eq.mpr
          (id (congrArg (fun _a => ↑(x2 2) = _a + ↑(x1 1) ↔ ↑(x2 2) = ↑(x2 0) + ↑(x2 1)) (h 0)))
          (Eq.mpr
            (id (congrArg (fun _a => ↑(x2 2) = ↑(x2 0) + _a ↔ ↑(x2 2) = ↑(x2 0) + ↑(x2 1)) (h 1)))
            Iff.rfl)))
  | 0, r, x1, x2, h => Empty.elim r
  | 1, r, x1, x2, h => Empty.elim r
  | n.succ.succ.succ.succ, r, x1, x2, h => Empty.elim r

Complexity: 13717 (size of the value term)

Dependencies: arithLang, arithStruct

Lean core dependencies: Empty.elim, Eq, Eq.mpr, False, Fin, Iff, Iff.rfl, Nat, Unit.unit, congrArg, id

Used by: arithTower

theorem castSucc_not_surjective (k : ℕ) : ¬Function.Surjective Fin.castSucc
Show details 
fun k hsurj =>
  Exists.casesOn (hsurj (Fin.last (k + 1))) fun a ha =>
    absurd ha (LT.lt.ne (Fin.castSucc_lt_last a))

Complexity: 989 (size of the value term)

Dependencies: (none)

Lean core dependencies: Eq, Exists, False, Fin, Fin.castSucc, Fin.castSucc_lt_last, Fin.last, Function.Surjective, Nat, Not, absurd

Used by: arithTower

def arithLevel (n : ℤ) : Type
Show details 
| arithLevel n = Fin (n.natAbs + 1)

Complexity: 31 (size of the value term)

Outer dependencies: (none)

Lean core dependencies: Fin, Int, Int.natAbs, Nat

Used by: arithFromNat, arithFromNat_toNat, arithPlus_iff, arithStepNeg, arithStepNeg_injective, arithStepNeg_not_surjective, arithStepNeg_val, arithStepPos, arithStepPos_val, arithStepTo_val, arithSucc_iff, arithToNat, arithToNat_mk, arithTower

theorem arithLevel_negNatAbs (n : ℕ) : (-↑n).natAbs + 1 = n + 1
Show details 
fun n =>
  of_eq_true
    (Eq.trans
      (Eq.trans
        (congrFun' (congrArg Eq (congrFun' (congrArg HAdd.hAdd (Int.natAbs_neg ↑n)) 1)) (n + 1))
        Nat.add_left_cancel_iff._simp_1)
      (eq_self 1))

Complexity: 661 (size of the value term)

Dependencies: (none)

Lean core dependencies: Eq, Eq.trans, Int, Int.natAbs, Int.natAbs_neg, Nat, Nat.cast, True, congrArg, congrFun', eq_self, of_eq_true

Used by: arithStepNeg, arithStepNeg_injective, arithStepNeg_not_surjective

def arithStepPos (n : ℕ) : arithLevel ↑n → arithLevel (↑n + 1)
Show details 
| arithStepPos n = Fin.castSucc

Complexity: 37 (size of the value term)

Outer dependencies: arithLevel

Lean core dependencies: Fin.castSucc, Int, Int.natAbs, Nat, Nat.cast

Used by: arithFromNat, arithFromNat_toNat, arithPlus_iff, arithStepPos_val, arithStepTo_val, arithSucc_iff, arithToNat, arithToNat_mk, arithTower

def arithStepNeg (n : ℕ) : arithLevel (-↑n) → arithLevel (-↑(n + 1))
Show details 
| arithStepNeg n x = Fin.cast ⋯ (Fin.cast ⋯ x).castSucc

Complexity: 239 (size of the value term)

Outer dependencies: arithLevel

Inner dependencies: arithLevel_negNatAbs

Lean core dependencies: Eq.symm, Fin.cast, Fin.castSucc, Int, Int.natAbs, Nat, Nat.cast

Used by: arithStepNeg_injective, arithStepNeg_not_surjective, arithStepNeg_val, arithTower

theorem arithStepNeg_injective (n : ℕ) : Function.Injective (arithStepNeg n)
Show details 
fun n ⦃a b⦄ hab =>
  have h1 := Fin.cast_injective (arithStepNeg._proof_1 n) hab;
  Fin.cast_injective (arithLevel_negNatAbs n) (Fin.castSucc_injective (n + 1) h1)

Complexity: 924 (size of the value term)

Dependencies: arithLevel, arithStepNeg

Proof dependencies: arithLevel_negNatAbs

Mathlib dependencies: Fin.castSucc_injective, Fin.cast_injective

Lean core dependencies: Eq, Fin, Fin.cast, Fin.castSucc, Function.Injective, Int, Int.natAbs, Nat, Nat.cast

Used by: arithTower

theorem arithStepNeg_not_surjective (n : ℕ) : ¬Function.Surjective (arithStepNeg n)
Show details 
fun n hsurj =>
  Exists.casesOn (hsurj (Fin.cast (Eq.symm (arithLevel_negNatAbs (n + 1))) (Fin.last (n + 1))))
    fun a ha =>
    have h2 := Fin.cast_injective (arithStepNeg._proof_1 n) ha;
    absurd h2 (LT.lt.ne (Fin.castSucc_lt_last (Fin.cast (arithLevel_negNatAbs n) a)))

Complexity: 2472 (size of the value term)

Dependencies: arithLevel, arithStepNeg

Proof dependencies: arithLevel_negNatAbs

Mathlib dependencies: Fin.cast_injective

Lean core dependencies: Eq, Eq.symm, Exists, False, Fin, Fin.cast, Fin.castSucc, Fin.castSucc_lt_last, Fin.last, Function.Surjective, Int, Int.natAbs, Nat, Nat.cast, Not, absurd

Used by: arithTower

theorem arithStepPos_val (n : ℕ) (a : arithLevel ↑n) : ↑(arithStepPos n a) = ↑a
Show details 
fun n a => rfl

Complexity: 81 (size of the value term)

Dependencies: arithLevel, arithStepPos

Lean core dependencies: Eq, Int, Int.natAbs, Nat, Nat.cast, rfl

Used by: arithStepTo_val, arithTower

theorem arithStepNeg_val (n : ℕ) (a : arithLevel (-↑n)) : ↑(arithStepNeg n a) = ↑a
Show details 
fun n a => id (of_eq_true (eq_self ↑a))

Complexity: 281 (size of the value term)

Dependencies: arithLevel, arithStepNeg

Lean core dependencies: Eq, Int, Int.natAbs, Nat, Nat.cast, eq_self, id, of_eq_true

Used by: arithTower

def arithTower : Tower
Show details 
| arithTower =
  { Level := arithLevel, Lang := fun x => arithLang, struct := fun n => arithStruct n.natAbs,
    finite := arithTower._proof_1, stepPos := arithStepPos, stepNeg := arithStepNeg,
    stepPos_injective := arithTower._proof_2, stepNeg_injective := ⋯, stepPos_not_surjective := ⋯,
    stepNeg_not_surjective := ⋯, translatePos := fun x => FirstOrder.Language.LHom.id arithLang,
    translateNeg := fun x => FirstOrder.Language.LHom.id arithLang,
    stepPos_preserves_relation := arithTower._proof_3,
    stepNeg_preserves_relation := arithTower._proof_4,
    stepPos_preserves_function := arithTower._proof_5,
    stepNeg_preserves_function := arithTower._proof_6,
    heap := fun x => { domain := ∅, at_ := fun p hp => absurd hp ⋯ }, pointsTo := fun x => false,
    reads_heap := arithTower._proof_8, lift := fun x x_1 => 0,
    heap_from_below := arithTower._proof_10, stepPos_heap_domain := arithTower._proof_13,
    stepPos_heap_at := arithTower._proof_14, stepNeg_heap_domain := arithTower._proof_17,
    stepNeg_heap_at := arithTower._proof_18 }

Complexity: 393 (size of the value term)

Outer dependencies: Tower

Inner dependencies: arithLang, arithLevel, arithStepNeg, arithStepNeg_injective, arithStepNeg_not_surjective, arithStepNeg_val, arithStepPos, arithStepPos_val, arithStruct, arithStruct_congr, castSucc_not_surjective

Mathlib dependencies: Fin.castSucc_injective, Finite, FirstOrder.Language.LHom.id, Matrix.vecCons, Matrix.vecEmpty, Set, Set.notMem_empty, TopologicalSpace

Lean core dependencies: Empty.elim, Eq, Eq.symm, Eq.trans, Exists, False, Fin, Function.comp, Iff, Iff.of_eq, Int, Int.natAbs, Nat, Nat.cast, Not, True, absurd, congrArg, congrFun', exists_prop_congr, id, iff_self, inferInstance, of_eq_true

Used by: arithFromNat, arithFromNat_toNat, arithLevelTopEquivNat, arithPlus, arithPlus_iff, arithPlus_mk_eq, arithPlus_succ, arithPlus_zero, arithSucc, arithSuccFun, arithSuccFun_injective, arithSucc_functional, arithSucc_iff, arithSucc_iff_eq_succFun, arithSucc_mk_eq, arithSucc_no_fixed_point, arithSucc_total, arithToNat, arithToNat_injective, arithTranslatePos_stepTo_eq, arithZero, arithZero_not_succ, arithZero_unique, instNonemptyTower

instance instNonemptyTower : Nonempty Tower
Show details 
Nonempty.intro arithTower

Complexity: 5 (size of the value term)

Outer dependencies: Tower

Inner dependencies: arithTower

Lean core dependencies: Nonempty

Used by: (none)

arithTower’s colimit is genuinely the natural numbers, and its successor/addition relations are the real thing

theorem arithStepTo_val {n m : ℕ} (h : n ≤ m) (x : Fin (n + 1)) :
  ↑(SeqColimit.stepTo arithStepPos n m h x) = ↑x
Show details 
fun {n m} h x =>
  Nat.le.rec (id (Eq.mpr (id (congrArg (fun _a => ↑_a = ↑x) (Nat.leRecOn_self x))) (Eq.refl ↑x)))
    (fun {m} h ih =>
      Eq.mpr (id (congrArg (fun _a => ↑_a = ↑x) (SeqColimit.stepTo_succ arithStepPos h x)))
        (Eq.mpr
          (id
            (congrArg (fun _a => _a = ↑x)
              (arithStepPos_val m (SeqColimit.stepTo arithStepPos n m h x))))
          (Eq.mpr (id (congrArg (fun _a => _a = ↑x) ih)) (Eq.refl ↑x))))
    h

Complexity: 2777 (size of the value term)

Dependencies: SeqColimit.stepTo, arithLevel, arithStepPos

Proof dependencies: SeqColimit.stepTo_succ, arithStepPos_val

Mathlib dependencies: Nat.leRecOn, Nat.leRecOn_self, le_refl

Lean core dependencies: Eq, Eq.mpr, Fin, Int, Int.natAbs, Nat, Nat.cast, Nat.le, Nat.le_refl, Nat.le_succ, congrArg, id

Used by: arithFromNat_toNat, arithPlus_iff, arithSucc_iff, arithToNat

def arithToNat : arithTower.LevelTop → ℕ
Show details 
| arithToNat = Quotient.lift (fun p => ↑p.snd) arithToNat._proof_1

Complexity: 151 (size of the value term)

Outer dependencies: Tower.LevelTop, arithTower

Inner dependencies: SeqColimit.setoid, SeqColimit.stepTo, arithLevel, arithStepPos, arithStepTo_val

Lean core dependencies: Eq, Eq.mpr, Eq.symm, Exists, Int, Int.natAbs, Nat, Nat.cast, Quotient.lift, Sigma, congrArg, id

Used by: arithFromNat_toNat, arithLevelTopEquivNat, arithPlus_iff, arithPlus_succ, arithPlus_zero, arithSuccFun, arithSuccFun_injective, arithSucc_iff, arithSucc_iff_eq_succFun, arithSucc_no_fixed_point, arithToNat_fromNat, arithToNat_injective, arithToNat_mk, arithZero_not_succ, arithZero_unique

def arithFromNat (k : ℕ) : arithTower.LevelTop
Show details 
| arithFromNat k = SeqColimit.mk arithStepPos k (Fin.last k)

Complexity: 23 (size of the value term)

Outer dependencies: Tower.LevelTop, arithTower

Inner dependencies: SeqColimit.mk, arithLevel, arithStepPos

Lean core dependencies: Fin.last, Int, Nat, Nat.cast

Used by: arithFromNat_toNat, arithLevelTopEquivNat, arithPlus_iff, arithPlus_succ, arithPlus_zero, arithSuccFun, arithSuccFun_injective, arithSucc_iff, arithSucc_iff_eq_succFun, arithToNat_fromNat, arithZero, arithZero_not_succ, arithZero_unique

theorem arithToNat_fromNat (k : ℕ) : arithToNat (arithFromNat k) = k
Show details 
fun k => Fin.val_last k

Complexity: 5 (size of the value term)

Dependencies: arithFromNat, arithToNat

Lean core dependencies: Eq, Fin.val_last, Nat

Used by: arithLevelTopEquivNat, arithPlus_succ, arithPlus_zero, arithSuccFun_injective, arithSucc_iff_eq_succFun, arithZero_not_succ, arithZero_unique

theorem arithFromNat_toNat (p : arithTower.LevelTop) : arithFromNat (arithToNat p) = p
Show details 
fun p =>
  Quotient.ind
    (fun a =>
      Sigma.casesOn a fun n x =>
        id
          (Quotient.sound
            (Exists.intro (max (↑x) n)
              (Exists.intro (le_max_left ⟨↑x, Fin.last ↑x⟩.fst n)
                (Exists.intro (le_max_right ↑x ⟨n, x⟩.fst)
                  (Fin.ext
                    (Eq.mpr
                      (id
                        (congrArg
                          (fun _a =>
                            _a =
                              ↑(SeqColimit.stepTo arithStepPos ⟨n, x⟩.fst (max (↑x) n)
                                  (le_max_right ↑x ⟨n, x⟩.fst) ⟨n, x⟩.snd))
                          (arithStepTo_val (le_max_left ⟨↑x, Fin.last ↑x⟩.fst n)
                            ⟨↑x, Fin.last ↑x⟩.snd)))
                      (Eq.mpr
                        (id
                          (congrArg (fun _a => ↑⟨↑x, Fin.last ↑x⟩.snd = _a)
                            (arithStepTo_val (le_max_right ↑x ⟨n, x⟩.fst) ⟨n, x⟩.snd)))
                        (Eq.mpr (id (congrArg (fun _a => _a = ↑⟨n, x⟩.snd) (Fin.val_last ↑x)))
                          (Eq.refl ↑x))))))))))
    p

Complexity: 12825 (size of the value term)

Dependencies: Tower.LevelTop, arithFromNat, arithToNat, arithTower

Proof dependencies: SeqColimit.setoid, SeqColimit.stepTo, arithLevel, arithStepPos, arithStepTo_val

Mathlib dependencies: le_max_left, le_max_right

Lean core dependencies: Eq, Eq.mpr, Exists, Fin.ext, Fin.last, Fin.val_last, Int, Int.natAbs, Nat, Nat.cast, Quotient.ind, Quotient.mk, Quotient.sound, Sigma, congrArg, id

Used by: arithLevelTopEquivNat, arithPlus_iff, arithSucc_iff, arithSucc_iff_eq_succFun, arithZero_unique

def arithLevelTopEquivNat : arithTower.LevelTop ≃ ℕ
Show details 
| arithLevelTopEquivNat =
  { toFun := arithToNat, invFun := arithFromNat, left_inv := arithFromNat_toNat,
    right_inv := arithToNat_fromNat }

Complexity: 15 (size of the value term)

Outer dependencies: Tower.LevelTop, arithTower

Inner dependencies: arithFromNat, arithFromNat_toNat, arithToNat, arithToNat_fromNat

Mathlib dependencies: Equiv

Lean core dependencies: Nat

Used by: arithToNat_injective

theorem arithTranslatePos_stepTo_eq {k n m : ℕ} (h : n ≤ m) (r : arithLang.Relations k) :
  SeqColimit.stepTo (fun j r => (arithTower.translatePos j).onRelation r) n m h r = r
Show details 
fun {k n m} h r =>
  Nat.le.rec (SeqColimit.stepTo_self (fun j r => (arithTower.translatePos j).onRelation r) n r)
    (fun {m} h ih =>
      Eq.mpr
        (id
          (congrArg (fun _a => _a = r)
            (SeqColimit.stepTo_succ (fun j r => (arithTower.translatePos j).onRelation r) h r)))
        ih)
    h

Complexity: 1257 (size of the value term)

Dependencies: SeqColimit.stepTo, arithLang, arithTower

Proof dependencies: SeqColimit.stepTo_self, SeqColimit.stepTo_succ

Lean core dependencies: Eq, Eq.mpr, Int, Nat, Nat.cast, Nat.le, Nat.le_succ, congrArg, id

Used by: arithPlus_iff, arithPlus_mk_eq, arithSucc_iff, arithSucc_mk_eq

def arithSucc : arithTower.LangTop.Relations 2
Show details 
| arithSucc = SeqColimit.mk (fun n r => (arithTower.translatePos n).onRelation r) 0 true

Complexity: 113 (size of the value term)

Outer dependencies: Tower.LangTop, arithTower

Inner dependencies: SeqColimit.mk, arithLang

Lean core dependencies: Int, Nat, Nat.cast

Used by: arithSucc_functional, arithSucc_iff, arithSucc_iff_eq_succFun, arithSucc_mk_eq, arithSucc_no_fixed_point, arithSucc_total, arithZero_not_succ, arithZero_unique

def arithPlus : arithTower.LangTop.Relations 3
Show details 
| arithPlus = SeqColimit.mk (fun n r => (arithTower.translatePos n).onRelation r) 0 ()

Complexity: 113 (size of the value term)

Outer dependencies: Tower.LangTop, arithTower

Inner dependencies: SeqColimit.mk, arithLang

Lean core dependencies: Int, Nat, Nat.cast, Unit.unit

Used by: arithPlus_iff, arithPlus_mk_eq, arithPlus_succ, arithPlus_zero

theorem arithSucc_mk_eq (n : ℕ) :
  SeqColimit.mk (fun j r => (arithTower.translatePos j).onRelation r) n true = arithSucc
Show details 
fun n =>
  have this :=
    SeqColimit.mk_stepTo (fun j r => (arithTower.translatePos j).onRelation r) (Nat.zero_le n) true;
  Eq.mp
    (congrArg
      (fun _a =>
        SeqColimit.mk (fun j r => (arithTower.translatePos j).onRelation r) n _a =
          SeqColimit.mk (fun j r => (arithTower.translatePos j).onRelation r) 0 true)
      (arithTranslatePos_stepTo_eq (Nat.zero_le n) true))
    this

Complexity: 1840 (size of the value term)

Dependencies: SeqColimit, SeqColimit.mk, arithLang, arithSucc, arithTower

Proof dependencies: SeqColimit.mk_stepTo, SeqColimit.stepTo, arithTranslatePos_stepTo_eq

Lean core dependencies: Eq, Eq.mp, Int, Nat, Nat.cast, Nat.zero_le, congrArg

Used by: arithSucc_iff

theorem arithPlus_mk_eq (n : ℕ) :
  SeqColimit.mk (fun j r => (arithTower.translatePos j).onRelation r) n () = arithPlus
Show details 
fun n =>
  have this :=
    SeqColimit.mk_stepTo (fun j r => (arithTower.translatePos j).onRelation r) (Nat.zero_le n) ();
  Eq.mp
    (congrArg
      (fun _a =>
        SeqColimit.mk (fun j r => (arithTower.translatePos j).onRelation r) n _a =
          SeqColimit.mk (fun j r => (arithTower.translatePos j).onRelation r) 0 ())
      (arithTranslatePos_stepTo_eq (Nat.zero_le n) ()))
    this

Complexity: 1840 (size of the value term)

Dependencies: SeqColimit, SeqColimit.mk, arithLang, arithPlus, arithTower

Proof dependencies: SeqColimit.mk_stepTo, SeqColimit.stepTo, arithTranslatePos_stepTo_eq

Lean core dependencies: Eq, Eq.mp, Int, Nat, Nat.cast, Nat.zero_le, Unit.unit, congrArg

Used by: arithPlus_iff

theorem arithToNat_mk (n : ℕ) (x : Fin (n + 1)) : arithToNat (SeqColimit.mk arithStepPos n x) = ↑x
Show details 
fun n x => rfl

Complexity: 55 (size of the value term)

Dependencies: SeqColimit.mk, arithLevel, arithStepPos, arithToNat

Lean core dependencies: Eq, Fin, Int, Nat, Nat.cast, rfl

Used by: arithPlus_iff, arithSucc_iff

theorem arithSucc_iff (p q : arithTower.LevelTop) :
  FirstOrder.Language.Structure.RelMap arithSucc ![p, q] ↔ arithToNat q = arithToNat p + 1
Show details 
fun p q =>
  {
    mp := fun a =>
      Exists.casesOn a fun n h =>
        Exists.casesOn h fun rn h =>
          Exists.casesOn h fun y h =>
            And.casesOn h fun hrn right =>
              And.casesOn right fun hxy hrel =>
                have hrn' :=
                  have heqrel := Eq.trans (arithSucc_mk_eq n) hrn;
                  Exists.casesOn (Quotient.exact heqrel) fun K h =>
                    Exists.casesOn h fun h1 h =>
                      Exists.casesOn h fun h2 heq =>
                        Eq.symm
                          (Eq.mp
                            (congrArg (fun _a => ⟨n, true⟩.snd = _a)
                              (arithTranslatePos_stepTo_eq h2 ⟨n, rn⟩.snd))
                            (Eq.mp
                              (congrArg
                                (fun _a =>
                                  _a =
                                    SeqColimit.stepTo
                                      (fun j r => (arithTower.translatePos j).onRelation r)
                                      ⟨n, rn⟩.fst K h2 ⟨n, rn⟩.snd)
                                (arithTranslatePos_stepTo_eq h1 ⟨n, true⟩.snd))
                              heq));
                Eq.ndrec (motive := fun rn =>
                  arithSucc =
                      SeqColimit.mk (fun m r => (arithTower.translatePos m).onRelation r) n rn →
                    FirstOrder.Language.Structure.RelMap rn y → arithToNat q = arithToNat p + 1)
                  (fun hrn hrel =>
                    have hp := hxy 0;
                    have hq := hxy 1;
                    Eq.mpr (id (congrArg (fun _a => arithToNat q = arithToNat _a + 1) hp))
                      (Eq.mpr
                        (id
                          (congrArg
                            (fun _a =>
                              arithToNat _a =
                                arithToNat (SeqColimit.mk arithTower.stepPos n (y 0)) + 1)
                            hq))
                        (Eq.mpr
                          (id
                            (congrArg
                              (fun _a =>
                                _a = arithToNat (SeqColimit.mk arithTower.stepPos n (y 0)) + 1)
                              (arithToNat_mk n (y 1))))
                          (Eq.mpr
                            (id (congrArg (fun _a => ↑(y 1) = _a + 1) (arithToNat_mk n (y 0))))
                            hrel))))
                  (Eq.symm hrn') hrn hrel,
    mpr := fun heq =>
      have hp := Eq.symm (arithFromNat_toNat p);
      have hq := Eq.symm (arithFromNat_toNat q);
      Exists.intro (max (arithToNat p) (arithToNat q))
        (Exists.intro true
          (Exists.intro
            ![SeqColimit.stepTo arithStepPos (arithToNat p) (max (arithToNat p) (arithToNat q))
                (le_max_left (arithToNat p) (arithToNat q)) (Fin.last (arithToNat p)),
              SeqColimit.stepTo arithStepPos (arithToNat q) (max (arithToNat p) (arithToNat q))
                (le_max_right (arithToNat p) (arithToNat q)) (Fin.last (arithToNat q))]
            ⟨Eq.symm (arithSucc_mk_eq (max (arithToNat p) (arithToNat q))),
              ⟨fun i =>
                List.Mem.casesOn (motive := fun a x =>
                  List.finRange 2 = a →
                    Fintype.complete i ≍ x →
                      ![p, q] i =
                        SeqColimit.mk arithTower.stepPos (max (arithToNat p) (arithToNat q))
                          (![SeqColimit.stepTo arithStepPos (arithToNat p)
                                (max (arithToNat p) (arithToNat q))
                                (le_max_left (arithToNat p) (arithToNat q))
                                (Fin.last (arithToNat p)),
                              SeqColimit.stepTo arithStepPos (arithToNat q)
                                (max (arithToNat p) (arithToNat q))
                                (le_max_right (arithToNat p) (arithToNat q))
                                (Fin.last (arithToNat q))]
                            i))
                  (Fintype.complete i)
                  (fun as h =>
                    List.cons.noConfusion h fun head_eq =>
                      Eq.ndrec (motive := fun i =>
                        ∀ (this : i ∈ Fintype.elems),
                          (fun x1 x2 => (fun i => i) x1 :: x2) ⟨1, Nat.le_refl 2⟩ [] ≍ as →
                            this ≍ List.Mem.head as →
                              ![p, q] i =
                                SeqColimit.mk arithTower.stepPos (max (arithToNat p) (arithToNat q))
                                  (![SeqColimit.stepTo arithStepPos (arithToNat p)
                                        (max (arithToNat p) (arithToNat q))
                                        (le_max_left (arithToNat p) (arithToNat q))
                                        (Fin.last (arithToNat p)),
                                      SeqColimit.stepTo arithStepPos (arithToNat q)
                                        (max (arithToNat p) (arithToNat q))
                                        (le_max_right (arithToNat p) (arithToNat q))
                                        (Fin.last (arithToNat q))]
                                    i))
                        (fun this tail_eq =>
                          Eq.ndrec (motive := fun as =>
                            this ≍ List.Mem.head as →
                              ![p, q] ((fun i => i) ⟨0, Nat.le_of_lt (Nat.le_refl 2)⟩) =
                                SeqColimit.mk arithTower.stepPos (max (arithToNat p) (arithToNat q))
                                  (![SeqColimit.stepTo arithStepPos (arithToNat p)
                                        (max (arithToNat p) (arithToNat q))
                                        (le_max_left (arithToNat p) (arithToNat q))
                                        (Fin.last (arithToNat p)),
                                      SeqColimit.stepTo arithStepPos (arithToNat q)
                                        (max (arithToNat p) (arithToNat q))
                                        (le_max_right (arithToNat p) (arithToNat q))
                                        (Fin.last (arithToNat q))]
                                    ((fun i => i) ⟨0, Nat.le_of_lt (Nat.le_refl 2)⟩)))
                            (fun h =>
                              Eq.mpr
                                (id
                                  (congrArg
                                    (fun _a =>
                                      ![_a, q] ((fun i => i) ⟨0, Nat.le_of_lt (Nat.le_refl 2)⟩) =
                                        SeqColimit.mk arithTower.stepPos
                                          (max (arithToNat _a) (arithToNat q))
                                          (![SeqColimit.stepTo arithStepPos (arithToNat _a)
                                                (max (arithToNat _a) (arithToNat q))
                                                (le_max_left (arithToNat _a) (arithToNat q))
                                                (Fin.last (arithToNat _a)),
                                              SeqColimit.stepTo arithStepPos (arithToNat q)
                                                (max (arithToNat _a) (arithToNat q))
                                                (le_max_right (arithToNat _a) (arithToNat q))
                                                (Fin.last (arithToNat q))]
                                            ((fun i => i) ⟨0, Nat.le_of_lt (Nat.le_refl 2)⟩)))
                                    hp))
                                (Eq.symm
                                  (SeqColimit.mk_stepTo arithStepPos
                                    (le_max_left
                                      (Quotient.lift (fun p => ↑p.snd) arithToNat._proof_1 p)
                                      (arithToNat q))
                                    (Fin.last (arithToNat p)))))
                            (eq_of_heq tail_eq))
                        (eq_of_heq head_eq) (Fintype.complete i))
                  (fun b {as} a h =>
                    List.cons.noConfusion h fun head_eq =>
                      Eq.ndrec (motive := fun b =>
                        (fun x1 x2 => (fun i => i) x1 :: x2) ⟨1, Nat.le_refl 2⟩ [] ≍ as →
                          Fintype.complete i ≍ List.Mem.tail b a →
                            ![p, q] i =
                              SeqColimit.mk arithTower.stepPos (max (arithToNat p) (arithToNat q))
                                (![SeqColimit.stepTo arithStepPos (arithToNat p)
                                      (max (arithToNat p) (arithToNat q))
                                      (le_max_left (arithToNat p) (arithToNat q))
                                      (Fin.last (arithToNat p)),
                                    SeqColimit.stepTo arithStepPos (arithToNat q)
                                      (max (arithToNat p) (arithToNat q))
                                      (le_max_right (arithToNat p) (arithToNat q))
                                      (Fin.last (arithToNat q))]
                                  i))
                        (fun tail_eq =>
                          Eq.ndrec (motive := fun {as} =>
                            ∀ (a : List.Mem i as),
                              Fintype.complete i ≍
                                  List.Mem.tail ((fun i => i) ⟨0, Nat.le_of_lt (Nat.le_refl 2)⟩) a →
                                ![p, q] i =
                                  SeqColimit.mk arithTower.stepPos
                                    (max (arithToNat p) (arithToNat q))
                                    (![SeqColimit.stepTo arithStepPos (arithToNat p)
                                          (max (arithToNat p) (arithToNat q))
                                          (le_max_left (arithToNat p) (arithToNat q))
                                          (Fin.last (arithToNat p)),
                                        SeqColimit.stepTo arithStepPos (arithToNat q)
                                          (max (arithToNat p) (arithToNat q))
                                          (le_max_right (arithToNat p) (arithToNat q))
                                          (Fin.last (arithToNat q))]
                                      i))
                            (fun a h =>
                              List.Mem.casesOn (motive := fun a_1 x =>
                                (fun x1 x2 => (fun i => i) x1 :: x2) ⟨1, Nat.le_refl 2⟩ [] = a_1 →
                                  a ≍ x →
                                    ![p, q] i =
                                      SeqColimit.mk arithTower.stepPos
                                        (max (arithToNat p) (arithToNat q))
                                        (![SeqColimit.stepTo arithStepPos (arithToNat p)
                                              (max (arithToNat p) (arithToNat q))
                                              (le_max_left (arithToNat p) (arithToNat q))
                                              (Fin.last (arithToNat p)),
                                            SeqColimit.stepTo arithStepPos (arithToNat q)
                                              (max (arithToNat p) (arithToNat q))
                                              (le_max_right (arithToNat p) (arithToNat q))
                                              (Fin.last (arithToNat q))]
                                          i))
                                a
                                (fun as h =>
                                  List.cons.noConfusion h fun head_eq =>
                                    Eq.ndrec (motive := fun i =>
                                      ∀
                                        (a :
                                          List.Mem i
                                            ((fun x1 x2 => (fun i => i) x1 :: x2) ⟨1, Nat.le_refl 2⟩
                                              [])),
                                        [] ≍ as →
                                          a ≍ List.Mem.head as →
                                            ![p, q] i =
                                              SeqColimit.mk arithTower.stepPos
                                                (max (arithToNat p) (arithToNat q))
                                                (![SeqColimit.stepTo arithStepPos (arithToNat p)
                                                      (max (arithToNat p) (arithToNat q))
                                                      (le_max_left (arithToNat p) (arithToNat q))
                                                      (Fin.last (arithToNat p)),
                                                    SeqColimit.stepTo arithStepPos (arithToNat q)
                                                      (max (arithToNat p) (arithToNat q))
                                                      (le_max_right (arithToNat p) (arithToNat q))
                                                      (Fin.last (arithToNat q))]
                                                  i))
                                      (fun a tail_eq =>
                                        Eq.ndrec (motive := fun as =>
                                          a ≍ List.Mem.head as →
                                            ![p, q] ((fun i => i) ⟨1, Nat.le_refl 2⟩) =
                                              SeqColimit.mk arithTower.stepPos
                                                (max (arithToNat p) (arithToNat q))
                                                (![SeqColimit.stepTo arithStepPos (arithToNat p)
                                                      (max (arithToNat p) (arithToNat q))
                                                      (le_max_left (arithToNat p) (arithToNat q))
                                                      (Fin.last (arithToNat p)),
                                                    SeqColimit.stepTo arithStepPos (arithToNat q)
                                                      (max (arithToNat p) (arithToNat q))
                                                      (le_max_right (arithToNat p) (arithToNat q))
                                                      (Fin.last (arithToNat q))]
                                                  ((fun i => i) ⟨1, Nat.le_refl 2⟩)))
                                          (fun h =>
                                            Eq.mpr
                                              (id
                                                (congrArg
                                                  (fun _a =>
                                                    ![p, _a] ((fun i => i) ⟨1, Nat.le_refl 2⟩) =
                                                      SeqColimit.mk arithTower.stepPos
                                                        (max (arithToNat p) (arithToNat _a))
                                                        (![SeqColimit.stepTo arithStepPos
                                                              (arithToNat p)
                                                              (max (arithToNat p) (arithToNat _a))
                                                              (le_max_left (arithToNat p)
                                                                (arithToNat _a))
                                                              (Fin.last (arithToNat p)),
                                                            SeqColimit.stepTo arithStepPos
                                                              (arithToNat _a)
                                                              (max (arithToNat p) (arithToNat _a))
                                                              (le_max_right (arithToNat p)
                                                                (arithToNat _a))
                                                              (Fin.last (arithToNat _a))]
                                                          ((fun i => i) ⟨1, Nat.le_refl 2⟩)))
                                                  hq))
                                              (Eq.symm
                                                (SeqColimit.mk_stepTo arithStepPos
                                                  (le_max_right (arithToNat p)
                                                    (Quotient.lift (fun p => ↑p.snd)
                                                      arithToNat._proof_1 q))
                                                  (Fin.last (arithToNat q)))))
                                          (eq_of_heq tail_eq))
                                      (eq_of_heq head_eq) a)
                                (fun b {as} a_1 h =>
                                  List.cons.noConfusion h fun head_eq =>
                                    Eq.ndrec (motive := fun b =>
                                      [] ≍ as →
                                        a ≍ List.Mem.tail b a_1 →
                                          ![p, q] i =
                                            SeqColimit.mk arithTower.stepPos
                                              (max (arithToNat p) (arithToNat q))
                                              (![SeqColimit.stepTo arithStepPos (arithToNat p)
                                                    (max (arithToNat p) (arithToNat q))
                                                    (le_max_left (arithToNat p) (arithToNat q))
                                                    (Fin.last (arithToNat p)),
                                                  SeqColimit.stepTo arithStepPos (arithToNat q)
                                                    (max (arithToNat p) (arithToNat q))
                                                    (le_max_right (arithToNat p) (arithToNat q))
                                                    (Fin.last (arithToNat q))]
                                                i))
                                      (fun tail_eq =>
                                        Eq.ndrec (motive := fun {as} =>
                                          ∀ (a_2 : List.Mem i as),
                                            a ≍
                                                List.Mem.tail ((fun i => i) ⟨1, Nat.le_refl 2⟩)
                                                  a_2 →
                                              ![p, q] i =
                                                SeqColimit.mk arithTower.stepPos
                                                  (max (arithToNat p) (arithToNat q))
                                                  (![SeqColimit.stepTo arithStepPos (arithToNat p)
                                                        (max (arithToNat p) (arithToNat q))
                                                        (le_max_left (arithToNat p) (arithToNat q))
                                                        (Fin.last (arithToNat p)),
                                                      SeqColimit.stepTo arithStepPos (arithToNat q)
                                                        (max (arithToNat p) (arithToNat q))
                                                        (le_max_right (arithToNat p) (arithToNat q))
                                                        (Fin.last (arithToNat q))]
                                                    i))
                                          (fun a_2 h =>
                                            List.Mem.casesOn (motive := fun a x =>
                                              [] = a →
                                                a_2 ≍ x →
                                                  ![p, q] i =
                                                    SeqColimit.mk arithTower.stepPos
                                                      (max (arithToNat p) (arithToNat q))
                                                      (![SeqColimit.stepTo arithStepPos
                                                            (arithToNat p)
                                                            (max (arithToNat p) (arithToNat q))
                                                            (le_max_left (arithToNat p)
                                                              (arithToNat q))
                                                            (Fin.last (arithToNat p)),
                                                          SeqColimit.stepTo arithStepPos
                                                            (arithToNat q)
                                                            (max (arithToNat p) (arithToNat q))
                                                            (le_max_right (arithToNat p)
                                                              (arithToNat q))
                                                            (Fin.last (arithToNat q))]
                                                        i))
                                              a_2
                                              (fun as h =>
                                                False.elim (noConfusion_of_Nat List.ctorIdx h))
                                              (fun b {as} a h =>
                                                False.elim (noConfusion_of_Nat List.ctorIdx h))
                                              (Eq.refl []) (HEq.refl a_2))
                                          (eq_of_heq tail_eq) a_1)
                                      (eq_of_heq head_eq))
                                (Eq.refl
                                  ((fun x1 x2 => (fun i => i) x1 :: x2) ⟨1, Nat.le_refl 2⟩ []))
                                (HEq.refl a))
                            (eq_of_heq tail_eq) a)
                        (eq_of_heq head_eq))
                  (Eq.refl (List.finRange 2)) (HEq.refl (Fintype.complete i)),
                id
                  (Eq.mpr
                    (id
                      (congrArg
                        (fun _a =>
                          _a =
                            ↑(SeqColimit.stepTo arithStepPos (arithToNat p)
                                  (max (arithToNat p) (arithToNat q))
                                  (le_max_left (arithToNat p) (arithToNat q))
                                  (Fin.last (arithToNat p))) +
                              1)
                        (arithStepTo_val (le_max_right (arithToNat p) (arithToNat q))
                          (Fin.last (arithToNat q)))))
                    (Eq.mpr
                      (id
                        (congrArg (fun _a => ↑(Fin.last (arithToNat q)) = _a + 1)
                          (arithStepTo_val (le_max_left (arithToNat p) (arithToNat q))
                            (Fin.last (arithToNat p)))))
                      (Eq.mpr
                        (id
                          (congrArg (fun _a => _a = ↑(Fin.last (arithToNat p)) + 1)
                            (Fin.val_last (arithToNat q))))
                        (Eq.mpr
                          (id
                            (congrArg (fun _a => arithToNat q = _a + 1)
                              (Fin.val_last (arithToNat p))))
                          heq))))⟩⟩)) }

Complexity: 46097 (size of the value term)

Dependencies: Tower.LangTop, Tower.LevelTop, Tower.structTop, arithSucc, arithToNat, arithTower

Proof dependencies: SeqColimit, SeqColimit.mk, SeqColimit.mk_stepTo, SeqColimit.setoid, SeqColimit.stepTo, arithFromNat, arithFromNat_toNat, arithLang, arithLevel, arithStepPos, arithStepTo_val, arithSucc_mk_eq, arithToNat_mk, arithTranslatePos_stepTo_eq

Mathlib dependencies: Finset, Matrix.vecCons, Matrix.vecEmpty, le_max_left, le_max_right

Lean core dependencies: And, Eq, Eq.mp, Eq.mpr, Eq.symm, Eq.trans, Exists, False.elim, Fin, Fin.last, Fin.val_last, HEq, Iff, Int, Int.natAbs, List, List.Mem, List.finRange, Nat, Nat.cast, Nat.le_of_lt, Nat.le_refl, Quotient.exact, Quotient.lift, Sigma, congrArg, eq_of_heq, id, noConfusion_of_Nat

Used by: arithSucc_iff_eq_succFun, arithSucc_no_fixed_point, arithZero_not_succ, arithZero_unique

theorem arithPlus_iff (p q r : arithTower.LevelTop) :
  FirstOrder.Language.Structure.RelMap arithPlus ![p, q, r] ↔
    arithToNat r = arithToNat p + arithToNat q
Show details 
fun p q r =>
  {
    mp := fun a =>
      Exists.casesOn a fun n h =>
        Exists.casesOn h fun rn h =>
          Exists.casesOn h fun y h =>
            And.casesOn h fun hrn right =>
              And.casesOn right fun hxy hrel =>
                have hrn' :=
                  have heqrel := Eq.trans (arithPlus_mk_eq n) hrn;
                  Exists.casesOn (Quotient.exact heqrel) fun K h =>
                    Exists.casesOn h fun h1 h =>
                      Exists.casesOn h fun h2 heq =>
                        Eq.symm
                          (Eq.mp
                            (congrArg (fun _a => ⟨n, ()⟩.snd = _a)
                              (arithTranslatePos_stepTo_eq h2 ⟨n, rn⟩.snd))
                            (Eq.mp
                              (congrArg
                                (fun _a =>
                                  _a =
                                    SeqColimit.stepTo
                                      (fun j r => (arithTower.translatePos j).onRelation r)
                                      ⟨n, rn⟩.fst K h2 ⟨n, rn⟩.snd)
                                (arithTranslatePos_stepTo_eq h1 ⟨n, ()⟩.snd))
                              heq));
                Eq.ndrec (motive := fun rn =>
                  arithPlus =
                      SeqColimit.mk (fun m r => (arithTower.translatePos m).onRelation r) n rn →
                    FirstOrder.Language.Structure.RelMap rn y →
                      arithToNat r = arithToNat p + arithToNat q)
                  (fun hrn hrel =>
                    have hp := hxy 0;
                    have hq := hxy 1;
                    have hr := hxy 2;
                    Eq.mpr
                      (id (congrArg (fun _a => arithToNat r = arithToNat _a + arithToNat q) hp))
                      (Eq.mpr
                        (id
                          (congrArg
                            (fun _a =>
                              arithToNat r =
                                arithToNat (SeqColimit.mk arithTower.stepPos n (y 0)) +
                                  arithToNat _a)
                            hq))
                        (Eq.mpr
                          (id
                            (congrArg
                              (fun _a =>
                                arithToNat _a =
                                  arithToNat (SeqColimit.mk arithTower.stepPos n (y 0)) +
                                    arithToNat (SeqColimit.mk arithTower.stepPos n (y 1)))
                              hr))
                          (Eq.mpr
                            (id
                              (congrArg
                                (fun _a =>
                                  _a =
                                    arithToNat (SeqColimit.mk arithTower.stepPos n (y 0)) +
                                      arithToNat (SeqColimit.mk arithTower.stepPos n (y 1)))
                                (arithToNat_mk n (y 2))))
                            (Eq.mpr
                              (id
                                (congrArg
                                  (fun _a =>
                                    ↑(y 2) =
                                      _a + arithToNat (SeqColimit.mk arithTower.stepPos n (y 1)))
                                  (arithToNat_mk n (y 0))))
                              (Eq.mpr
                                (id
                                  (congrArg (fun _a => ↑(y 2) = ↑(y 0) + _a)
                                    (arithToNat_mk n (y 1))))
                                hrel))))))
                  (Eq.symm hrn') hrn hrel,
    mpr := fun heq =>
      have hp := Eq.symm (arithFromNat_toNat p);
      have hq := Eq.symm (arithFromNat_toNat q);
      have hr := Eq.symm (arithFromNat_toNat r);
      let M := max (arithToNat p) (max (arithToNat q) (arithToNat r));
      have hM := rfl;
      have hMp := le_max_left (arithToNat p) (max (arithToNat q) (arithToNat r));
      have hMq :=
        LE.le.trans (le_max_left (arithToNat q) (arithToNat r))
          (le_max_right (arithToNat p) (max (arithToNat q) (arithToNat r)));
      have hMr :=
        LE.le.trans (le_max_right (arithToNat q) (arithToNat r))
          (le_max_right (arithToNat p) (max (arithToNat q) (arithToNat r)));
      Exists.intro M
        (Exists.intro ()
          (Exists.intro
            ![SeqColimit.stepTo arithStepPos (arithToNat p) M hMp (Fin.last (arithToNat p)),
              SeqColimit.stepTo arithStepPos (arithToNat q) M hMq (Fin.last (arithToNat q)),
              SeqColimit.stepTo arithStepPos (arithToNat r) M hMr (Fin.last (arithToNat r))]
            ⟨Eq.symm (arithPlus_mk_eq M),
              ⟨fun i =>
                List.Mem.casesOn (motive := fun a x =>
                  List.finRange 3 = a →
                    Fintype.complete i ≍ x →
                      ![p, q, r] i =
                        SeqColimit.mk arithTower.stepPos M
                          (![SeqColimit.stepTo arithStepPos (arithToNat p) M hMp
                                (Fin.last (arithToNat p)),
                              SeqColimit.stepTo arithStepPos (arithToNat q) M hMq
                                (Fin.last (arithToNat q)),
                              SeqColimit.stepTo arithStepPos (arithToNat r) M hMr
                                (Fin.last (arithToNat r))]
                            i))
                  (Fintype.complete i)
                  (fun as h =>
                    List.cons.noConfusion h fun head_eq =>
                      Eq.ndrec (motive := fun i =>
                        ∀ (this : i ∈ Fintype.elems),
                          (fun x1 x2 => (fun i => i) x1 :: x2) ⟨1, Nat.le_of_lt (Nat.le_refl 3)⟩
                                ((fun x1 x2 => (fun i => i) x1 :: x2) ⟨2, Nat.le_refl 3⟩ []) ≍
                              as →
                            this ≍ List.Mem.head as →
                              ![p, q, r] i =
                                SeqColimit.mk arithTower.stepPos M
                                  (![SeqColimit.stepTo arithStepPos (arithToNat p) M hMp
                                        (Fin.last (arithToNat p)),
                                      SeqColimit.stepTo arithStepPos (arithToNat q) M hMq
                                        (Fin.last (arithToNat q)),
                                      SeqColimit.stepTo arithStepPos (arithToNat r) M hMr
                                        (Fin.last (arithToNat r))]
                                    i))
                        (fun this tail_eq =>
                          Eq.ndrec (motive := fun as =>
                            this ≍ List.Mem.head as →
                              ![p, q, r]
                                  ((fun i => i) ⟨0, Nat.le_of_lt (Nat.le_of_lt (Nat.le_refl 3))⟩) =
                                SeqColimit.mk arithTower.stepPos M
                                  (![SeqColimit.stepTo arithStepPos (arithToNat p) M hMp
                                        (Fin.last (arithToNat p)),
                                      SeqColimit.stepTo arithStepPos (arithToNat q) M hMq
                                        (Fin.last (arithToNat q)),
                                      SeqColimit.stepTo arithStepPos (arithToNat r) M hMr
                                        (Fin.last (arithToNat r))]
                                    ((fun i => i)
                                      ⟨0, Nat.le_of_lt (Nat.le_of_lt (Nat.le_refl 3))⟩)))
                            (fun h =>
                              Eq.trans hp
                                (Eq.symm
                                  (SeqColimit.mk_stepTo arithStepPos hMp
                                    (Fin.last (arithToNat p)))))
                            (eq_of_heq tail_eq))
                        (eq_of_heq head_eq) (Fintype.complete i))
                  (fun b {as} a h =>
                    List.cons.noConfusion h fun head_eq =>
                      Eq.ndrec (motive := fun b =>
                        (fun x1 x2 => (fun i => i) x1 :: x2) ⟨1, Nat.le_of_lt (Nat.le_refl 3)⟩
                              ((fun x1 x2 => (fun i => i) x1 :: x2) ⟨2, Nat.le_refl 3⟩ []) ≍
                            as →
                          Fintype.complete i ≍ List.Mem.tail b a →
                            ![p, q, r] i =
                              SeqColimit.mk arithTower.stepPos M
                                (![SeqColimit.stepTo arithStepPos (arithToNat p) M hMp
                                      (Fin.last (arithToNat p)),
                                    SeqColimit.stepTo arithStepPos (arithToNat q) M hMq
                                      (Fin.last (arithToNat q)),
                                    SeqColimit.stepTo arithStepPos (arithToNat r) M hMr
                                      (Fin.last (arithToNat r))]
                                  i))
                        (fun tail_eq =>
                          Eq.ndrec (motive := fun {as} =>
                            ∀ (a : List.Mem i as),
                              Fintype.complete i ≍
                                  List.Mem.tail
                                    ((fun i => i) ⟨0, Nat.le_of_lt (Nat.le_of_lt (Nat.le_refl 3))⟩)
                                    a →
                                ![p, q, r] i =
                                  SeqColimit.mk arithTower.stepPos M
                                    (![SeqColimit.stepTo arithStepPos (arithToNat p) M hMp
                                          (Fin.last (arithToNat p)),
                                        SeqColimit.stepTo arithStepPos (arithToNat q) M hMq
                                          (Fin.last (arithToNat q)),
                                        SeqColimit.stepTo arithStepPos (arithToNat r) M hMr
                                          (Fin.last (arithToNat r))]
                                      i))
                            (fun a h =>
                              List.Mem.casesOn (motive := fun a_1 x =>
                                (fun x1 x2 => (fun i => i) x1 :: x2)
                                      ⟨1, Nat.le_of_lt (Nat.le_refl 3)⟩
                                      ((fun x1 x2 => (fun i => i) x1 :: x2) ⟨2, Nat.le_refl 3⟩ []) =
                                    a_1 →
                                  a ≍ x →
                                    ![p, q, r] i =
                                      SeqColimit.mk arithTower.stepPos M
                                        (![SeqColimit.stepTo arithStepPos (arithToNat p) M hMp
                                              (Fin.last (arithToNat p)),
                                            SeqColimit.stepTo arithStepPos (arithToNat q) M hMq
                                              (Fin.last (arithToNat q)),
                                            SeqColimit.stepTo arithStepPos (arithToNat r) M hMr
                                              (Fin.last (arithToNat r))]
                                          i))
                                a
                                (fun as h =>
                                  List.cons.noConfusion h fun head_eq =>
                                    Eq.ndrec (motive := fun i =>
                                      ∀
                                        (a :
                                          List.Mem i
                                            ((fun x1 x2 => (fun i => i) x1 :: x2)
                                              ⟨1, Nat.le_of_lt (Nat.le_refl 3)⟩
                                              ((fun x1 x2 => (fun i => i) x1 :: x2)
                                                ⟨2, Nat.le_refl 3⟩ []))),
                                        (fun x1 x2 => (fun i => i) x1 :: x2) ⟨2, Nat.le_refl 3⟩ [] ≍
                                            as →
                                          a ≍ List.Mem.head as →
                                            ![p, q, r] i =
                                              SeqColimit.mk arithTower.stepPos M
                                                (![SeqColimit.stepTo arithStepPos (arithToNat p) M
                                                      hMp (Fin.last (arithToNat p)),
                                                    SeqColimit.stepTo arithStepPos (arithToNat q) M
                                                      hMq (Fin.last (arithToNat q)),
                                                    SeqColimit.stepTo arithStepPos (arithToNat r) M
                                                      hMr (Fin.last (arithToNat r))]
                                                  i))
                                      (fun a tail_eq =>
                                        Eq.ndrec (motive := fun as =>
                                          a ≍ List.Mem.head as →
                                            ![p, q, r]
                                                ((fun i => i) ⟨1, Nat.le_of_lt (Nat.le_refl 3)⟩) =
                                              SeqColimit.mk arithTower.stepPos M
                                                (![SeqColimit.stepTo arithStepPos (arithToNat p) M
                                                      hMp (Fin.last (arithToNat p)),
                                                    SeqColimit.stepTo arithStepPos (arithToNat q) M
                                                      hMq (Fin.last (arithToNat q)),
                                                    SeqColimit.stepTo arithStepPos (arithToNat r) M
                                                      hMr (Fin.last (arithToNat r))]
                                                  ((fun i => i) ⟨1, Nat.le_of_lt (Nat.le_refl 3)⟩)))
                                          (fun h =>
                                            Eq.trans hq
                                              (Eq.symm
                                                (SeqColimit.mk_stepTo arithStepPos hMq
                                                  (Fin.last (arithToNat q)))))
                                          (eq_of_heq tail_eq))
                                      (eq_of_heq head_eq) a)
                                (fun b {as} a_1 h =>
                                  List.cons.noConfusion h fun head_eq =>
                                    Eq.ndrec (motive := fun b =>
                                      (fun x1 x2 => (fun i => i) x1 :: x2) ⟨2, Nat.le_refl 3⟩ [] ≍
                                          as →
                                        a ≍ List.Mem.tail b a_1 →
                                          ![p, q, r] i =
                                            SeqColimit.mk arithTower.stepPos M
                                              (![SeqColimit.stepTo arithStepPos (arithToNat p) M hMp
                                                    (Fin.last (arithToNat p)),
                                                  SeqColimit.stepTo arithStepPos (arithToNat q) M
                                                    hMq (Fin.last (arithToNat q)),
                                                  SeqColimit.stepTo arithStepPos (arithToNat r) M
                                                    hMr (Fin.last (arithToNat r))]
                                                i))
                                      (fun tail_eq =>
                                        Eq.ndrec (motive := fun {as} =>
                                          ∀ (a_2 : List.Mem i as),
                                            a ≍
                                                List.Mem.tail
                                                  ((fun i => i) ⟨1, Nat.le_of_lt (Nat.le_refl 3)⟩)
                                                  a_2 →
                                              ![p, q, r] i =
                                                SeqColimit.mk arithTower.stepPos M
                                                  (![SeqColimit.stepTo arithStepPos (arithToNat p) M
                                                        hMp (Fin.last (arithToNat p)),
                                                      SeqColimit.stepTo arithStepPos (arithToNat q)
                                                        M hMq (Fin.last (arithToNat q)),
                                                      SeqColimit.stepTo arithStepPos (arithToNat r)
                                                        M hMr (Fin.last (arithToNat r))]
                                                    i))
                                          (fun a_2 h =>
                                            List.Mem.casesOn (motive := fun a x =>
                                              (fun x1 x2 => (fun i => i) x1 :: x2)
                                                    ⟨2, Nat.le_refl 3⟩ [] =
                                                  a →
                                                a_2 ≍ x →
                                                  ![p, q, r] i =
                                                    SeqColimit.mk arithTower.stepPos M
                                                      (![SeqColimit.stepTo arithStepPos
                                                            (arithToNat p) M hMp
                                                            (Fin.last (arithToNat p)),
                                                          SeqColimit.stepTo arithStepPos
                                                            (arithToNat q) M hMq
                                                            (Fin.last (arithToNat q)),
                                                          SeqColimit.stepTo arithStepPos
                                                            (arithToNat r) M hMr
                                                            (Fin.last (arithToNat r))]
                                                        i))
                                              a_2
                                              (fun as h =>
                                                List.cons.noConfusion h fun head_eq =>
                                                  Eq.ndrec (motive := fun i =>
                                                    ∀
                                                      (a :
                                                        List.Mem i
                                                          ((fun x1 x2 => (fun i => i) x1 :: x2)
                                                            ⟨2, Nat.le_refl 3⟩ [])),
                                                      [] ≍ as →
                                                        a ≍ List.Mem.head as →
                                                          ![p, q, r] i =
                                                            SeqColimit.mk arithTower.stepPos M
                                                              (![SeqColimit.stepTo arithStepPos
                                                                    (arithToNat p) M hMp
                                                                    (Fin.last (arithToNat p)),
                                                                  SeqColimit.stepTo arithStepPos
                                                                    (arithToNat q) M hMq
                                                                    (Fin.last (arithToNat q)),
                                                                  SeqColimit.stepTo arithStepPos
                                                                    (arithToNat r) M hMr
                                                                    (Fin.last (arithToNat r))]
                                                                i))
                                                    (fun a tail_eq =>
                                                      Eq.ndrec (motive := fun as =>
                                                        a ≍ List.Mem.head as →
                                                          ![p, q, r]
                                                              ((fun i => i) ⟨2, Nat.le_refl 3⟩) =
                                                            SeqColimit.mk arithTower.stepPos M
                                                              (![SeqColimit.stepTo arithStepPos
                                                                    (arithToNat p) M hMp
                                                                    (Fin.last (arithToNat p)),
                                                                  SeqColimit.stepTo arithStepPos
                                                                    (arithToNat q) M hMq
                                                                    (Fin.last (arithToNat q)),
                                                                  SeqColimit.stepTo arithStepPos
                                                                    (arithToNat r) M hMr
                                                                    (Fin.last (arithToNat r))]
                                                                ((fun i => i) ⟨2, Nat.le_refl 3⟩)))
                                                        (fun h =>
                                                          Eq.trans hr
                                                            (Eq.symm
                                                              (SeqColimit.mk_stepTo arithStepPos hMr
                                                                (Fin.last (arithToNat r)))))
                                                        (eq_of_heq tail_eq))
                                                    (eq_of_heq head_eq) a_2)
                                              (fun b {as} a h =>
                                                List.cons.noConfusion h fun head_eq =>
                                                  Eq.ndrec (motive := fun b =>
                                                    [] ≍ as →
                                                      a_2 ≍ List.Mem.tail b a →
                                                        ![p, q, r] i =
                                                          SeqColimit.mk arithTower.stepPos M
                                                            (![SeqColimit.stepTo arithStepPos
                                                                  (arithToNat p) M hMp
                                                                  (Fin.last (arithToNat p)),
                                                                SeqColimit.stepTo arithStepPos
                                                                  (arithToNat q) M hMq
                                                                  (Fin.last (arithToNat q)),
                                                                SeqColimit.stepTo arithStepPos
                                                                  (arithToNat r) M hMr
                                                                  (Fin.last (arithToNat r))]
                                                              i))
                                                    (fun tail_eq =>
                                                      Eq.ndrec (motive := fun {as} =>
                                                        ∀ (a : List.Mem i as),
                                                          a_2 ≍
                                                              List.Mem.tail
                                                                ((fun i => i) ⟨2, Nat.le_refl 3⟩)
                                                                a →
                                                            ![p, q, r] i =
                                                              SeqColimit.mk arithTower.stepPos M
                                                                (![SeqColimit.stepTo arithStepPos
                                                                      (arithToNat p) M hMp
                                                                      (Fin.last (arithToNat p)),
                                                                    SeqColimit.stepTo arithStepPos
                                                                      (arithToNat q) M hMq
                                                                      (Fin.last (arithToNat q)),
                                                                    SeqColimit.stepTo arithStepPos
                                                                      (arithToNat r) M hMr
                                                                      (Fin.last (arithToNat r))]
                                                                  i))
                                                        (fun a h =>
                                                          List.Mem.casesOn (motive := fun a_3 x =>
                                                            [] = a_3 →
                                                              a ≍ x →
                                                                ![p, q, r] i =
                                                                  SeqColimit.mk arithTower.stepPos M
                                                                    (![SeqColimit.stepTo
                                                                          arithStepPos
                                                                          (arithToNat p) M hMp
                                                                          (Fin.last (arithToNat p)),
                                                                        SeqColimit.stepTo
                                                                          arithStepPos
                                                                          (arithToNat q) M hMq
                                                                          (Fin.last (arithToNat q)),
                                                                        SeqColimit.stepTo
                                                                          arithStepPos
                                                                          (arithToNat r) M hMr
                                                                          (Fin.last (arithToNat r))]
                                                                      i))
                                                            a
                                                            (fun as h =>
                                                              False.elim
                                                                (noConfusion_of_Nat List.ctorIdx h))
                                                            (fun b {as} a_3 h =>
                                                              False.elim
                                                                (noConfusion_of_Nat List.ctorIdx h))
                                                            (Eq.refl []) (HEq.refl a))
                                                        (eq_of_heq tail_eq) a)
                                                    (eq_of_heq head_eq))
                                              (Eq.refl
                                                ((fun x1 x2 => (fun i => i) x1 :: x2)
                                                  ⟨2, Nat.le_refl 3⟩ []))
                                              (HEq.refl a_2))
                                          (eq_of_heq tail_eq) a_1)
                                      (eq_of_heq head_eq))
                                (Eq.refl
                                  ((fun x1 x2 => (fun i => i) x1 :: x2)
                                    ⟨1, Nat.le_of_lt (Nat.le_refl 3)⟩
                                    ((fun x1 x2 => (fun i => i) x1 :: x2) ⟨2, Nat.le_refl 3⟩ [])))
                                (HEq.refl a))
                            (eq_of_heq tail_eq) a)
                        (eq_of_heq head_eq))
                  (Eq.refl (List.finRange 3)) (HEq.refl (Fintype.complete i)),
                id
                  (Eq.mpr
                    (id
                      (congrArg
                        (fun _a =>
                          _a =
                            ↑(SeqColimit.stepTo arithStepPos (arithToNat p) M hMp
                                  (Fin.last (arithToNat p))) +
                              ↑(SeqColimit.stepTo arithStepPos (arithToNat q) M hMq
                                  (Fin.last (arithToNat q))))
                        (arithStepTo_val hMr (Fin.last (arithToNat r)))))
                    (Eq.mpr
                      (id
                        (congrArg
                          (fun _a =>
                            ↑(Fin.last (arithToNat r)) =
                              _a +
                                ↑(SeqColimit.stepTo arithStepPos (arithToNat q) M hMq
                                    (Fin.last (arithToNat q))))
                          (arithStepTo_val hMp (Fin.last (arithToNat p)))))
                      (Eq.mpr
                        (id
                          (congrArg
                            (fun _a => ↑(Fin.last (arithToNat r)) = ↑(Fin.last (arithToNat p)) + _a)
                            (arithStepTo_val hMq (Fin.last (arithToNat q)))))
                        (Eq.mpr
                          (id
                            (congrArg
                              (fun _a =>
                                _a = ↑(Fin.last (arithToNat p)) + ↑(Fin.last (arithToNat q)))
                              (Fin.val_last (arithToNat r))))
                          (Eq.mpr
                            (id
                              (congrArg (fun _a => arithToNat r = _a + ↑(Fin.last (arithToNat q)))
                                (Fin.val_last (arithToNat p))))
                            (Eq.mpr
                              (id
                                (congrArg (fun _a => arithToNat r = arithToNat p + _a)
                                  (Fin.val_last (arithToNat q))))
                              heq))))))⟩⟩)) }

Complexity: 54686 (size of the value term)

Dependencies: Tower.LangTop, Tower.LevelTop, Tower.structTop, arithPlus, arithToNat, arithTower

Proof dependencies: SeqColimit, SeqColimit.mk, SeqColimit.mk_stepTo, SeqColimit.setoid, SeqColimit.stepTo, arithFromNat, arithFromNat_toNat, arithLang, arithLevel, arithPlus_mk_eq, arithStepPos, arithStepTo_val, arithToNat_mk, arithTranslatePos_stepTo_eq

Mathlib dependencies: Finset, Matrix.vecCons, Matrix.vecEmpty, le_max_left, le_max_right

Lean core dependencies: And, Eq, Eq.mp, Eq.mpr, Eq.symm, Eq.trans, Exists, False.elim, Fin, Fin.last, Fin.val_last, HEq, Iff, Int, Int.natAbs, List, List.Mem, List.finRange, Nat, Nat.cast, Nat.le_of_lt, Nat.le_refl, Quotient.exact, Sigma, Unit.unit, congrArg, eq_of_heq, id, noConfusion_of_Nat, rfl

Used by: arithPlus_succ, arithPlus_zero

theorem arithToNat_injective : Function.Injective arithToNat
Show details 
Equiv.injective arithLevelTopEquivNat

Complexity: 9 (size of the value term)

Dependencies: Tower.LevelTop, arithToNat, arithTower

Proof dependencies: arithLevelTopEquivNat

Mathlib dependencies: Equiv.injective

Lean core dependencies: Function.Injective, Nat

Used by: arithSuccFun_injective

def arithSuccFun (p : arithTower.LevelTop) : arithTower.LevelTop
Show details 
| arithSuccFun p = arithFromNat (arithToNat p + 1)

Complexity: 33 (size of the value term)

Outer dependencies: Tower.LevelTop, arithTower

Inner dependencies: arithFromNat, arithToNat

Lean core dependencies: Nat

Used by: arithPlus_succ, arithSuccFun_injective, arithSucc_functional, arithSucc_iff_eq_succFun, arithSucc_total

theorem arithSucc_iff_eq_succFun (p q : arithTower.LevelTop) :
  FirstOrder.Language.Structure.RelMap arithSucc ![p, q] ↔ q = arithSuccFun p
Show details 
fun p q =>
  Eq.mpr (id (congrArg (fun _a => _a ↔ q = arithSuccFun p) (propext (arithSucc_iff p q))))
    (Eq.mpr
      (id (congrArg (fun _a => arithToNat q = arithToNat p + 1 ↔ q = _a) (arithSuccFun.eq_1 p)))
      {
        mp := fun h =>
          Eq.mpr (id (congrArg (fun _a => q = arithFromNat _a) (Eq.symm h)))
            (Eq.mpr (id (congrArg (fun _a => q = _a) (arithFromNat_toNat q))) (Eq.refl q)),
        mpr := fun h =>
          Eq.mpr (id (congrArg (fun _a => arithToNat _a = arithToNat p + 1) h))
            (Eq.mpr
              (id
                (congrArg (fun _a => _a = arithToNat p + 1)
                  (arithToNat_fromNat (arithToNat p + 1))))
              (Eq.refl (arithToNat p + 1))) })

Complexity: 2037 (size of the value term)

Dependencies: Tower.LangTop, Tower.LevelTop, Tower.structTop, arithSucc, arithSuccFun, arithTower

Proof dependencies: arithFromNat, arithFromNat_toNat, arithSucc_iff, arithToNat, arithToNat_fromNat

Mathlib dependencies: Matrix.vecCons, Matrix.vecEmpty

Lean core dependencies: Eq, Eq.mpr, Eq.symm, Iff, Nat, congrArg, id

Used by: arithSucc_functional, arithSucc_total

theorem arithSucc_total (p : arithTower.LevelTop) :
  FirstOrder.Language.Structure.RelMap arithSucc ![p, arithSuccFun p]
Show details 
fun p => (arithSucc_iff_eq_succFun p (arithSuccFun p)).mpr rfl

Complexity: 107 (size of the value term)

Dependencies: Tower.LangTop, Tower.LevelTop, Tower.structTop, arithSucc, arithSuccFun, arithTower

Proof dependencies: arithSucc_iff_eq_succFun

Mathlib dependencies: Matrix.vecCons, Matrix.vecEmpty

Lean core dependencies: Eq, Nat, rfl

Used by: (none)

theorem arithSucc_functional (p q q' : arithTower.LevelTop)
  (h : FirstOrder.Language.Structure.RelMap arithSucc ![p, q])
  (h' : FirstOrder.Language.Structure.RelMap arithSucc ![p, q']) : q = q'
Show details 
fun p q q' h h' =>
  Eq.mpr
    (id
      (congrArg (fun _a => _a = q')
        (Eq.mp (congrArg (fun _a => _a) (propext (arithSucc_iff_eq_succFun p q))) h)))
    (Eq.mpr
      (id
        (congrArg (fun _a => arithSuccFun p = _a)
          (Eq.mp (congrArg (fun _a => _a) (propext (arithSucc_iff_eq_succFun p q'))) h')))
      (Eq.refl (arithSuccFun p)))

Complexity: 851 (size of the value term)

Dependencies: Tower.LangTop, Tower.LevelTop, Tower.structTop, arithSucc, arithTower

Proof dependencies: arithSuccFun, arithSucc_iff_eq_succFun

Mathlib dependencies: Matrix.vecCons, Matrix.vecEmpty

Lean core dependencies: Eq, Eq.mp, Eq.mpr, Nat, congrArg, id

Used by: (none)

theorem arithSuccFun_injective : Function.Injective arithSuccFun
Show details 
fun ⦃p p'⦄ h =>
  arithToNat_injective
    (have this := congrArg arithToNat h;
    Eq.mp (congrArg (fun _a => _a) (propext Nat.add_right_cancel_iff))
      (Eq.mp (congrArg (fun _a => arithToNat p + 1 = _a) (arithToNat_fromNat (arithToNat p' + 1)))
        (Eq.mp
          (congrArg (fun _a => _a = arithToNat (arithFromNat (arithToNat p' + 1)))
            (arithToNat_fromNat (arithToNat p + 1)))
          (Eq.mp
            (congrArg (fun _a => arithToNat (arithFromNat (arithToNat p + 1)) = arithToNat _a)
              (arithSuccFun.eq_1 p'))
            (Eq.mp
              (congrArg (fun _a => arithToNat _a = arithToNat (arithSuccFun p'))
                (arithSuccFun.eq_1 p))
              this)))))

Complexity: 1168 (size of the value term)

Dependencies: Tower.LevelTop, arithSuccFun, arithTower

Proof dependencies: arithFromNat, arithToNat, arithToNat_fromNat, arithToNat_injective

Lean core dependencies: Eq, Eq.mp, Function.Injective, Nat, Nat.add_right_cancel_iff, congrArg

Used by: (none)

theorem arithSucc_no_fixed_point (p : arithTower.LevelTop) :
  ¬FirstOrder.Language.Structure.RelMap arithSucc ![p, p]
Show details 
fun p =>
  Eq.mpr (id (congrArg (fun _a => ¬_a) (propext (arithSucc_iff p p)))) fun a =>
    arithSucc_no_fixed_point._proof_1_1 p a

Complexity: 497 (size of the value term)

Dependencies: Tower.LangTop, Tower.LevelTop, Tower.structTop, arithSucc, arithTower

Proof dependencies: arithSucc_iff, arithToNat

Mathlib dependencies: Matrix.vecCons, Matrix.vecEmpty

Lean core dependencies: Bool, Decidable.decide, Eq, Eq.mpr, Eq.symm, Eq.trans, Int, Int.natCast_add, Int.sub_eq_zero_of_eq, Lean.Omega.Coeffs.ofList, Lean.Omega.Constraint.addEquality_sat, Lean.Omega.Constraint.isImpossible, Lean.Omega.Constraint.not_sat'_of_isImpossible, Lean.Omega.Int.add_congr, Lean.Omega.Int.ofNat_congr, Lean.Omega.Int.sub_congr, Lean.Omega.LinearCombo, Lean.Omega.LinearCombo.add_eval, Lean.Omega.LinearCombo.coordinate, Lean.Omega.LinearCombo.coordinate_eval_0, Lean.Omega.LinearCombo.eval, Lean.Omega.LinearCombo.sub_eval, Lean.Omega.tidy_sat, Nat, Nat.cast, Not, congrArg, id, of_decide_eq_true

Used by: (none)

def arithZero : arithTower.LevelTop
Show details 
| arithZero = arithFromNat 0

Complexity: 11 (size of the value term)

Outer dependencies: Tower.LevelTop, arithTower

Inner dependencies: arithFromNat

Lean core dependencies: Nat

Used by: arithPlus_zero, arithZero_not_succ, arithZero_unique

theorem arithZero_not_succ (p : arithTower.LevelTop) :
  ¬FirstOrder.Language.Structure.RelMap arithSucc ![p, arithZero]
Show details 
fun p =>
  Eq.mpr (id (congrArg (fun _a => ¬_a) (propext (arithSucc_iff p arithZero))))
    (Eq.mpr (id (congrArg (fun _a => ¬arithToNat _a = arithToNat p + 1) arithZero.eq_1))
      (Eq.mpr (id (congrArg (fun _a => ¬_a = arithToNat p + 1) (arithToNat_fromNat 0))) fun a =>
        arithZero_not_succ._proof_1_2 p a))

Complexity: 1021 (size of the value term)

Dependencies: Tower.LangTop, Tower.LevelTop, Tower.structTop, arithSucc, arithTower, arithZero

Proof dependencies: arithFromNat, arithSucc_iff, arithToNat, arithToNat_fromNat

Mathlib dependencies: Matrix.vecCons, Matrix.vecEmpty

Lean core dependencies: Bool, Decidable.decide, Eq, Eq.mpr, Eq.symm, Eq.trans, Int, Int.natCast_add, Int.natCast_nonneg, Int.sub_eq_zero_of_eq, Lean.Omega.Coeffs.ofList, Lean.Omega.Constraint.addEquality_sat, Lean.Omega.Constraint.addInequality_sat, Lean.Omega.Constraint.isImpossible, Lean.Omega.Constraint.not_sat'_of_isImpossible, Lean.Omega.Int.add_congr, Lean.Omega.Int.ofNat_congr, Lean.Omega.Int.sub_congr, Lean.Omega.LinearCombo, Lean.Omega.LinearCombo.add_eval, Lean.Omega.LinearCombo.coordinate, Lean.Omega.LinearCombo.coordinate_eval_0, Lean.Omega.LinearCombo.eval, Lean.Omega.LinearCombo.sub_eval, Lean.Omega.combo_sat', Lean.Omega.tidy_sat, Nat, Nat.cast, Not, congrArg, id, le_of_le_of_eq, of_decide_eq_true

Used by: (none)

theorem arithZero_unique (z : arithTower.LevelTop)
  (hz : ∀ (p : arithTower.LevelTop), ¬FirstOrder.Language.Structure.RelMap arithSucc ![p, z]) :
  z = arithZero
Show details 
fun z hz =>
  Classical.byContradiction fun hne =>
    hne
      (have hz0 := fun h0 =>
        hne
          (Eq.mpr (id (congrArg (fun _a => _a = arithZero) (Eq.symm (arithFromNat_toNat z))))
            (Eq.mpr (id (congrArg (fun _a => arithFromNat _a = arithZero) h0))
              (Eq.mpr (id (congrArg (fun _a => arithFromNat 0 = _a) arithZero.eq_1))
                (Eq.refl (arithFromNat 0)))));
      Exists.casesOn (Nat.exists_eq_succ_of_ne_zero hz0) fun k hk =>
        absurd
          (Eq.mpr (id (congrArg (fun _a => _a) (propext (arithSucc_iff (arithFromNat k) z))))
            (Eq.mpr (id (congrArg (fun _a => _a = arithToNat (arithFromNat k) + 1) hk))
              (Eq.mpr (id (congrArg (fun _a => k.succ = _a + 1) (arithToNat_fromNat k)))
                (Eq.refl k.succ))))
          (hz (arithFromNat k)))

Complexity: 1574 (size of the value term)

Dependencies: Tower.LangTop, Tower.LevelTop, Tower.structTop, arithSucc, arithTower, arithZero

Proof dependencies: arithFromNat, arithFromNat_toNat, arithSucc_iff, arithToNat, arithToNat_fromNat

Mathlib dependencies: Matrix.vecCons, Matrix.vecEmpty

Lean core dependencies: Classical.byContradiction, Eq, Eq.mpr, Eq.symm, Exists, Nat, Nat.exists_eq_succ_of_ne_zero, Ne, Not, absurd, congrArg, id

Used by: (none)

theorem arithPlus_zero (p : arithTower.LevelTop) :
  FirstOrder.Language.Structure.RelMap arithPlus ![p, arithZero, p]
Show details 
fun p =>
  Eq.mpr (id (congrArg (fun _a => _a) (propext (arithPlus_iff p arithZero p))))
    (Eq.mpr (id (congrArg (fun _a => arithToNat p = arithToNat p + arithToNat _a) arithZero.eq_1))
      (Eq.mpr (id (congrArg (fun _a => arithToNat p = arithToNat p + _a) (arithToNat_fromNat 0)))
        (Decidable.byContradiction fun a => arithPlus_zero._proof_1_2 p a)))

Complexity: 1049 (size of the value term)

Dependencies: Tower.LangTop, Tower.LevelTop, Tower.structTop, arithPlus, arithTower, arithZero

Proof dependencies: arithFromNat, arithPlus_iff, arithToNat, arithToNat_fromNat

Mathlib dependencies: Matrix.vecCons, Matrix.vecEmpty

Lean core dependencies: Bool, Decidable.byContradiction, Decidable.decide, Eq, Eq.mpr, Eq.symm, Eq.trans, False, GT.gt, Int, Int.add_one_le_of_lt, Int.natCast_add, Int.sub_nonneg_of_le, Lean.Omega.Coeffs.ofList, Lean.Omega.Constraint.addInequality_sat, Lean.Omega.Constraint.isImpossible, Lean.Omega.Constraint.not_sat'_of_isImpossible, Lean.Omega.Int.add_congr, Lean.Omega.Int.ofNat_lt_of_lt, Lean.Omega.Int.sub_congr, Lean.Omega.LinearCombo, Lean.Omega.LinearCombo.add_eval, Lean.Omega.LinearCombo.coordinate, Lean.Omega.LinearCombo.coordinate_eval_0, Lean.Omega.LinearCombo.eval, Lean.Omega.LinearCombo.sub_eval, Lean.Omega.tidy_sat, Nat, Nat.cast, Nat.lt_or_gt_of_ne, Not, Or.elim, congrArg, id, le_of_le_of_eq, of_decide_eq_true

Used by: (none)

theorem arithPlus_succ (p q r : arithTower.LevelTop) :
  FirstOrder.Language.Structure.RelMap arithPlus ![p, arithSuccFun q, arithSuccFun r] ↔
    FirstOrder.Language.Structure.RelMap arithPlus ![p, q, r]
Show details 
fun p q r =>
  Eq.mpr
    (id
      (congrArg (fun _a => _a ↔ FirstOrder.Language.Structure.RelMap arithPlus ![p, q, r])
        (propext (arithPlus_iff p (arithSuccFun q) (arithSuccFun r)))))
    (Eq.mpr
      (id
        (congrArg
          (fun _a => arithToNat (arithSuccFun r) = arithToNat p + arithToNat (arithSuccFun q) ↔ _a)
          (propext (arithPlus_iff p q r))))
      (Eq.mpr
        (id
          (congrArg
            (fun _a =>
              arithToNat _a = arithToNat p + arithToNat (arithSuccFun q) ↔
                arithToNat r = arithToNat p + arithToNat q)
            (arithSuccFun.eq_1 r)))
        (Eq.mpr
          (id
            (congrArg
              (fun _a =>
                arithToNat (arithFromNat (arithToNat r + 1)) = arithToNat p + arithToNat _a ↔
                  arithToNat r = arithToNat p + arithToNat q)
              (arithSuccFun.eq_1 q)))
          (Eq.mpr
            (id
              (congrArg
                (fun _a =>
                  _a = arithToNat p + arithToNat (arithFromNat (arithToNat q + 1)) ↔
                    arithToNat r = arithToNat p + arithToNat q)
                (arithToNat_fromNat (arithToNat r + 1))))
            (Eq.mpr
              (id
                (congrArg
                  (fun _a =>
                    arithToNat r + 1 = arithToNat p + _a ↔
                      arithToNat r = arithToNat p + arithToNat q)
                  (arithToNat_fromNat (arithToNat q + 1))))
              (Decidable.byContradiction fun a => arithPlus_succ._proof_1_2 p q r a))))))

Complexity: 4401 (size of the value term)

Dependencies: Tower.LangTop, Tower.LevelTop, Tower.structTop, arithPlus, arithSuccFun, arithTower

Proof dependencies: arithFromNat, arithPlus_iff, arithToNat, arithToNat_fromNat

Mathlib dependencies: Matrix.vecCons, Matrix.vecEmpty

Lean core dependencies: And, Bool, Decidable.byContradiction, Decidable.decide, Eq, Eq.mpr, Eq.symm, Eq.trans, False, GT.gt, Iff, Int, Int.add_one_le_of_lt, Int.natCast_add, Int.sub_eq_zero_of_eq, Int.sub_nonneg_of_le, Lean.Omega.Coeffs.ofList, Lean.Omega.Constraint.addEquality_sat, Lean.Omega.Constraint.addInequality_sat, Lean.Omega.Constraint.isImpossible, Lean.Omega.Constraint.not_sat'_of_isImpossible, Lean.Omega.Decidable.and_not_or_not_and_of_not_iff, Lean.Omega.Int.add_congr, Lean.Omega.Int.ofNat_congr, Lean.Omega.Int.ofNat_lt_of_lt, Lean.Omega.Int.sub_congr, Lean.Omega.LinearCombo, Lean.Omega.LinearCombo.add_eval, Lean.Omega.LinearCombo.coordinate, Lean.Omega.LinearCombo.coordinate_eval_0, Lean.Omega.LinearCombo.coordinate_eval_1, Lean.Omega.LinearCombo.coordinate_eval_2, Lean.Omega.LinearCombo.eval, Lean.Omega.LinearCombo.sub_eval, Lean.Omega.combo_sat', Lean.Omega.tidy_sat, Nat, Nat.cast, Nat.lt_or_gt_of_ne, Not, Or.elim, congrArg, id, le_of_le_of_eq, of_decide_eq_true

Used by: (none)

Dependency diagram

Drag to pan, Ctrl+scroll (or Cmd+scroll, or pinch on a touch screen) to zoom, click a node to jump to it.

definitionabbreviationtheoremdeclared elsewheredependencyproof dependency
legend