ImplementationCategory
Difficulty: optional — 10 definitions, 5 abbreviations, 29 lemmas, 4 theorems, 0 examples.
Component.Arrow
structure Component.Arrow (Wire : Type) [Nonempty Wire] [Norm Wire] (n m : ℕ) : Type 1
State : Type
nonempty : Nonempty self.State
size : Norm self.State
component : Component self.State Wire Wire n m
state : self.State
Show details
Outer dependencies: (none)
Inner dependencies: Component, instNonemptyForallFin_computerNetworks, instNormForallFin_computerNetworks
Mathlib dependencies: Norm
Used by: Component.Arrow.Equiv, Component.Arrow.setoid, Component.Hom, Component.Hom.comp, Component.Hom.comp_assoc, Component.Hom.comp_eqToHom, Component.Hom.comp_id, Component.Hom.eqToHom_comp, Component.Hom.hexagon_forward, Component.Hom.hexagon_reverse, Component.Hom.id, Component.Hom.id_comp, Component.Hom.recast, Component.Hom.recast_recast, Component.Hom.symmetry, Component.Hom.symmetry_symmetry, Component.Hom.tensor, Component.Hom.tensorUnit, Component.Hom.tensor_assoc, Component.Hom.tensor_comm, Component.Hom.tensor_comp_tensor, Component.Hom.tensor_empty, Component.Hom.tensor_id_id, Component.Hom.tensor_recast_left, Component.Hom.tensor_recast_right, Component.monoidalCategory
Component.Arrow.Equiv
abbrev Component.Arrow.Equiv (Wire : Type) [Nonempty Wire] [Norm Wire] (n m : ℕ) (f g : Component.Arrow Wire n m) : Prop
Show details
| Component.Arrow.Equiv Wire n m f g = InformationSystem.equivalent f.component g.component f.state g.state
Complexity: 223 (size of the value term)
Outer dependencies: Component.Arrow
Inner dependencies: InformationSystem.equivalent, instNonemptyForallFin_computerNetworks, instNormForallFin_computerNetworks
Mathlib dependencies: Norm
Used by: Component.Arrow.setoid
Component.Arrow.setoid
instance Component.Arrow.setoid (Wire : Type) [Nonempty Wire] [Norm Wire] (n m : ℕ) : Setoid (Component.Arrow Wire n m)
Show details
| Component.Arrow.setoid Wire n m = { r := Component.Arrow.Equiv Wire n m, iseqv := ⋯ }
Complexity: 51 (size of the value term)
Outer dependencies: Component.Arrow
Inner dependencies: Component.Arrow.Equiv, InformationSystem.eval, instNonemptyForallFin_computerNetworks, instNormForallFin_computerNetworks
Mathlib dependencies: Norm
Used by: Component.Hom, Component.Hom.comp, Component.Hom.comp_assoc, Component.Hom.comp_eqToHom, Component.Hom.comp_id, Component.Hom.eqToHom_comp, Component.Hom.hexagon_forward, Component.Hom.hexagon_reverse, Component.Hom.id, Component.Hom.id_comp, Component.Hom.recast, Component.Hom.recast_recast, Component.Hom.symmetry, Component.Hom.symmetry_symmetry, Component.Hom.tensor, Component.Hom.tensorUnit, Component.Hom.tensor_assoc, Component.Hom.tensor_comm, Component.Hom.tensor_comp_tensor, Component.Hom.tensor_empty, Component.Hom.tensor_id_id, Component.Hom.tensor_recast_left, Component.Hom.tensor_recast_right, Component.monoidalCategory
Component.Hom
abbrev Component.Hom (Wire : Type) [Nonempty Wire] [Norm Wire] (n m : ℕ) : Type 1
Show details
| Component.Hom Wire n m = Quotient (Component.Arrow.setoid Wire n m)
Complexity: 39 (size of the value term)
Outer dependencies: (none)
Inner dependencies: Component.Arrow, Component.Arrow.setoid
Mathlib dependencies: Norm
Used by: Component.Hom.comp, Component.Hom.comp_assoc, Component.Hom.comp_eqToHom, Component.Hom.comp_id, Component.Hom.eqToHom_comp, Component.Hom.hexagon_forward, Component.Hom.hexagon_reverse, Component.Hom.id, Component.Hom.id_comp, Component.Hom.recast, Component.Hom.recast_eqToHom, Component.Hom.recast_recast, Component.Hom.symmetry, Component.Hom.symmetry_symmetry, Component.Hom.tensor, Component.Hom.tensorUnit, Component.Hom.tensor_assoc, Component.Hom.tensor_comm, Component.Hom.tensor_comp_tensor, Component.Hom.tensor_empty, Component.Hom.tensor_id_id, Component.Hom.tensor_recast_left, Component.Hom.tensor_recast_right, Component.braidedCategory, Component.braiding_naturality_left, Component.braiding_naturality_right, Component.category, Component.monoidalCategory
Component.Hom.id
abbrev Component.Hom.id (Wire : Type) [Nonempty Wire] [Norm Wire] (n : ℕ) : Component.Hom Wire n n
Show details
| Component.Hom.id Wire n = ⟦{ State := Unit, nonempty := Component.Hom.id._proof_1, size := inferInstance, component := Component.id Wire n, state := () }⟧
Complexity: 73 (size of the value term)
Outer dependencies: Component.Hom
Inner dependencies: Component.Arrow, Component.Arrow.setoid, Component.id, instNormUnit_computerNetworks
Mathlib dependencies: Norm
Lean core dependencies: Nat, Nonempty, Quotient.mk, Unit, Unit.unit, inferInstance
Used by: Component.Hom.comp_eqToHom, Component.Hom.comp_id, Component.Hom.eqToHom_comp, Component.Hom.eqToHom_eq_recast_id, Component.Hom.hexagon_forward, Component.Hom.hexagon_reverse, Component.Hom.id_comp, Component.Hom.symmetry_symmetry, Component.Hom.tensor_empty, Component.Hom.tensor_id_id, Component.braidedCategory, Component.braiding_naturality_left, Component.braiding_naturality_right, Component.category, Component.monoidalCategory, Component.monoidalCategoryStruct
Component.Hom.comp
def Component.Hom.comp {Wire : Type} [Nonempty Wire] [Norm Wire] {n m p : ℕ} : Component.Hom Wire n m → Component.Hom Wire m p → Component.Hom Wire n p
Show details
| Component.Hom.comp = Quotient.map₂ (fun f g => { State := f.State × g.State, nonempty := ⋯, size := inferInstance, component := f.component.sequential g.component, state := (f.state, g.state) }) ⋯
Complexity: 475 (size of the value term)
Outer dependencies: Component.Hom
Inner dependencies: Component.Arrow, Component.Arrow.setoid, Component.sequential, Component.sequential_congr, instNormProd_computerNetworks
Mathlib dependencies: Norm, Quotient.map₂
Lean core dependencies: Nat, Nonempty, Prod, inferInstance
Used by: Component.Hom.comp_assoc, Component.Hom.comp_eqToHom, Component.Hom.comp_id, Component.Hom.eqToHom_comp, Component.Hom.hexagon_forward, Component.Hom.hexagon_reverse, Component.Hom.id_comp, Component.Hom.symmetry_symmetry, Component.Hom.tensor_comm, Component.Hom.tensor_comp_tensor, Component.braidedCategory, Component.braiding_naturality_left, Component.braiding_naturality_right, Component.category, Component.monoidalCategory
Component.Hom.tensor
def Component.Hom.tensor {Wire : Type} [Nonempty Wire] [Norm Wire] {n1 m1 n2 m2 : ℕ} : Component.Hom Wire n1 m1 → Component.Hom Wire n2 m2 → Component.Hom Wire (n1 + n2) (m1 + m2)
Show details
| Component.Hom.tensor = Quotient.map₂ (fun f g => { State := f.State × g.State, nonempty := ⋯, size := inferInstance, component := f.component.parallel g.component, state := (f.state, g.state) }) ⋯
Complexity: 573 (size of the value term)
Outer dependencies: Component.Hom
Inner dependencies: Component.Arrow, Component.Arrow.setoid, Component.parallel, Component.parallel_congr, instNonemptyForallFin_computerNetworks, instNormProd_computerNetworks
Mathlib dependencies: Norm, Quotient.map₂
Lean core dependencies: Nat, Nonempty, Prod, inferInstance
Used by: Component.Hom.hexagon_forward, Component.Hom.hexagon_reverse, Component.Hom.tensor_assoc, Component.Hom.tensor_comm, Component.Hom.tensor_comp_tensor, Component.Hom.tensor_empty, Component.Hom.tensor_id_id, Component.Hom.tensor_recast_left, Component.Hom.tensor_recast_right, Component.braidedCategory, Component.braiding_naturality_left, Component.braiding_naturality_right, Component.monoidalCategory, Component.monoidalCategoryStruct
Component.Hom.recast
def Component.Hom.recast {Wire : Type} [Nonempty Wire] [Norm Wire] {n n' m m' : ℕ} (hn : n = n') (hm : m = m') : Component.Hom Wire n m → Component.Hom Wire n' m'
Show details
| Component.Hom.recast hn hm = Quotient.map (fun f => { State := f.State, nonempty := ⋯, size := inferInstance, component := Component.recast hn hm f.component, state := f.state }) ⋯
Complexity: 301 (size of the value term)
Outer dependencies: Component.Hom
Inner dependencies: Component.Arrow, Component.Arrow.setoid, Component.recast, Component.recast_congr
Mathlib dependencies: Norm, Quotient.map
Lean core dependencies: Eq, Nat, Nonempty, inferInstance
Used by: Component.Hom.comp_eqToHom, Component.Hom.eqToHom_comp, Component.Hom.eqToHom_eq_recast_id, Component.Hom.hexagon_forward, Component.Hom.hexagon_reverse, Component.Hom.recast_eqToHom, Component.Hom.recast_recast, Component.Hom.tensor_assoc, Component.Hom.tensor_empty, Component.Hom.tensor_recast_left, Component.Hom.tensor_recast_right, Component.braidedCategory, Component.monoidalCategory
Component.Hom.tensorUnit
abbrev Component.Hom.tensorUnit (Wire : Type) [Nonempty Wire] [Norm Wire] : Component.Hom Wire 0 0
Show details
| Component.Hom.tensorUnit Wire = ⟦{ State := Unit, nonempty := Component.Hom.id._proof_1, size := inferInstance, component := Component.empty Wire Wire, state := () }⟧
Complexity: 123 (size of the value term)
Outer dependencies: Component.Hom
Inner dependencies: Component.Arrow, Component.Arrow.setoid, Component.empty, instNormUnit_computerNetworks
Mathlib dependencies: Norm
Lean core dependencies: Nat, Nonempty, Quotient.mk, Unit, Unit.unit, inferInstance
Used by: (none)
Component.Hom.symmetry
abbrev Component.Hom.symmetry (Wire : Type) [Nonempty Wire] [Norm Wire] (n m : ℕ) : Component.Hom Wire (n + m) (m + n)
Show details
| Component.Hom.symmetry Wire n m = ⟦{ State := Unit, nonempty := Component.Hom.id._proof_1, size := inferInstance, component := Component.symmetry Wire n m, state := () }⟧
Complexity: 173 (size of the value term)
Outer dependencies: Component.Hom
Inner dependencies: Component.Arrow, Component.Arrow.setoid, Component.symmetry, instNormUnit_computerNetworks
Mathlib dependencies: Norm
Lean core dependencies: Nat, Nonempty, Quotient.mk, Unit, Unit.unit, inferInstance
Component.Hom.id_comp
theorem Component.Hom.id_comp {Wire : Type} [Nonempty Wire] [Norm Wire] {n m : ℕ} (f : Component.Hom Wire n m) : (Component.Hom.id Wire n).comp f = f
Show details
fun {Wire} [Nonempty Wire] [Norm Wire] {n m} f => Quotient.ind (fun f => Quotient.sound (Component.id_sequential f.component f.state)) f
Complexity: 645 (size of the value term)
Dependencies: Component.Hom, Component.Hom.comp, Component.Hom.id
Proof dependencies: Component.Arrow, Component.Arrow.setoid, Component.id, Component.id_sequential, Component.sequential, instNormProd_computerNetworks, instNormUnit_computerNetworks
Mathlib dependencies: Norm
Lean core dependencies: Eq, Nat, Nonempty, Prod, Quotient.ind, Quotient.sound, Unit, Unit.unit, inferInstance
Used by: Component.Hom.eqToHom_comp, Component.category
Component.Hom.comp_id
theorem Component.Hom.comp_id {Wire : Type} [Nonempty Wire] [Norm Wire] {n m : ℕ} (f : Component.Hom Wire n m) : f.comp (Component.Hom.id Wire m) = f
Show details
fun {Wire} [Nonempty Wire] [Norm Wire] {n m} f => Quotient.ind (fun f => Quotient.sound (Component.sequential_id f.component f.state)) f
Complexity: 645 (size of the value term)
Dependencies: Component.Hom, Component.Hom.comp, Component.Hom.id
Proof dependencies: Component.Arrow, Component.Arrow.setoid, Component.id, Component.sequential, Component.sequential_id, instNormProd_computerNetworks, instNormUnit_computerNetworks
Mathlib dependencies: Norm
Lean core dependencies: Eq, Nat, Nonempty, Prod, Quotient.ind, Quotient.sound, Unit, Unit.unit, inferInstance
Component.Hom.comp_assoc
theorem Component.Hom.comp_assoc {Wire : Type} [Nonempty Wire] [Norm Wire] {n m p q : ℕ} (f : Component.Hom Wire n m) (g : Component.Hom Wire m p) (h : Component.Hom Wire p q) : (f.comp g).comp h = f.comp (g.comp h)
Show details
fun {Wire} [Nonempty Wire] [Norm Wire] {n m p q} f g h => Quotient.ind (fun f => Quotient.ind (fun g => Quotient.ind (fun h => Quotient.sound (Component.sequential_assoc f.component g.component h.component f.state g.state h.state)) h) g) f
Complexity: 2381 (size of the value term)
Dependencies: Component.Hom, Component.Hom.comp
Proof dependencies: Component.Arrow, Component.Arrow.setoid, Component.sequential, Component.sequential_assoc, instNormProd_computerNetworks
Mathlib dependencies: Norm
Lean core dependencies: Eq, Nat, Nonempty, Prod, Quotient.ind, Quotient.mk, Quotient.sound, inferInstance
Component.category
def Component.category (Wire : Type) [Nonempty Wire] [Norm Wire] : CategoryTheory.Category.{1, 0} ℕ
Show details
| Component.category Wire = { Hom := fun n m => Component.Hom Wire n m, id := fun n => Component.Hom.id Wire n, comp := fun {X Y Z} f g => f.comp g, id_comp := ⋯, comp_id := ⋯, assoc := ⋯ }
Complexity: 153 (size of the value term)
Outer dependencies: (none)
Inner dependencies: Component.Hom, Component.Hom.comp, Component.Hom.comp_assoc, Component.Hom.comp_id, Component.Hom.id, Component.Hom.id_comp
Mathlib dependencies: CategoryTheory.Category, Norm
Used by: Component.Hom.comp_eqToHom, Component.Hom.eqToHom_comp, Component.Hom.eqToHom_eq_recast_id, Component.Hom.recast_eqToHom, Component.braidedCategory, Component.braiding, Component.braiding_naturality_left, Component.braiding_naturality_right, Component.monoidalCategory, Component.monoidalCategoryStruct, instCategoryPROP
Component.interchange
theorem Component.interchange {Wire : Type} [Nonempty Wire] [Norm Wire] {StateA StateB StateC StateD : Type} [Nonempty StateA] [Norm StateA] [Nonempty StateB] [Norm StateB] [Nonempty StateC] [Norm StateC] [Nonempty StateD] [Norm StateD] {n1 m1 n2 m2 p1 p2 : ℕ} (f1 : Component StateA Wire Wire n1 m1) (f2 : Component StateB Wire Wire n2 m2) (g1 : Component StateC Wire Wire m1 p1) (g2 : Component StateD Wire Wire m2 p2) (sa : StateA) (sb : StateB) (sc : StateC) (sd : StateD) : InformationSystem.equivalent ((f1.parallel f2).sequential (g1.parallel g2)) ((f1.sequential g1).parallel (f2.sequential g2)) ((sa, sb), sc, sd) ((sa, sc), sb, sd)
Show details
fun {Wire} [Nonempty Wire] [Norm Wire] {StateA StateB StateC StateD} [Nonempty StateA] [Norm StateA] [Nonempty StateB] [Norm StateB] [Nonempty StateC] [Norm StateC] [Nonempty StateD] [Norm StateD] {n1 m1 n2 m2 p1 p2} f1 f2 g1 g2 sa sb sc sd is => List.rec (motive := fun is => ∀ (sa : StateA) (sb : StateB) (sc : StateC) (sd : StateD), (InformationSystem.eval ((f1.parallel f2).sequential (g1.parallel g2)) ((sa, sb), sc, sd) is).2 = (InformationSystem.eval ((f1.sequential g1).parallel (f2.sequential g2)) ((sa, sc), sb, sd) is).2) (fun sa sb sc sd => Eq.refl (InformationSystem.eval ((f1.parallel f2).sequential (g1.parallel g2)) ((sa, sb), sc, sd) []).2) (fun iv is ih sa sb sc sd => have e1 := funext fun k => Eq.mpr (id (congrArg (fun _a => _a = (f1.step sa fun k => iv (Fin.castAdd n2 k)).2 k) (Fin.append_left (f1.step sa fun k => iv (Fin.castAdd n2 k)).2 (f2.step sb fun k => iv (Fin.natAdd n1 k)).2 k))) (Eq.refl ((f1.step sa fun k => iv (Fin.castAdd n2 k)).2 k)); have e2 := funext fun k => Eq.mpr (id (congrArg (fun _a => _a = (f2.step sb fun k => iv (Fin.natAdd n1 k)).2 k) (Fin.append_right (f1.step sa fun k => iv (Fin.castAdd n2 k)).2 (f2.step sb fun k => iv (Fin.natAdd n1 k)).2 k))) (Eq.refl ((f2.step sb fun k => iv (Fin.natAdd n1 k)).2 k)); have hnextA := ih (f1.step sa fun k => iv (Fin.castAdd n2 k)).1 (f2.step sb fun k => iv (Fin.natAdd n1 k)).1 (g1.step sc (f1.step sa fun k => iv (Fin.castAdd n2 k)).2).1 (g2.step sd (f2.step sb fun k => iv (Fin.natAdd n1 k)).2).1; have hstepL := id (Eq.mpr (id (congrArg (fun _a => ((((f1.step sa fun k => iv (Fin.castAdd n2 k)).1, (f2.step sb fun k => iv (Fin.natAdd n1 k)).1), (g1.step sc _a).1, (g2.step sd fun k => Fin.append (f1.step sa fun k => iv (Fin.castAdd n2 k)).2 (f2.step sb fun k => iv (Fin.natAdd n1 k)).2 (Fin.natAdd m1 k)).1), Fin.append (g1.step sc _a).2 (g2.step sd fun k => Fin.append (f1.step sa fun k => iv (Fin.castAdd n2 k)).2 (f2.step sb fun k => iv (Fin.natAdd n1 k)).2 (Fin.natAdd m1 k)).2) = ((((f1.step sa fun k => iv (Fin.castAdd n2 k)).1, (f2.step sb fun k => iv (Fin.natAdd n1 k)).1), (g1.step sc (f1.step sa fun k => iv (Fin.castAdd n2 k)).2).1, (g2.step sd (f2.step sb fun k => iv (Fin.natAdd n1 k)).2).1), Fin.append (g1.step sc (f1.step sa fun k => iv (Fin.castAdd n2 k)).2).2 (g2.step sd (f2.step sb fun k => iv (Fin.natAdd n1 k)).2).2)) e1)) (Eq.mpr (id (congrArg (fun _a => ((((f1.step sa fun k => iv (Fin.castAdd n2 k)).1, (f2.step sb fun k => iv (Fin.natAdd n1 k)).1), (g1.step sc (f1.step sa fun k => iv (Fin.castAdd n2 k)).2).1, (g2.step sd _a).1), Fin.append (g1.step sc (f1.step sa fun k => iv (Fin.castAdd n2 k)).2).2 (g2.step sd _a).2) = ((((f1.step sa fun k => iv (Fin.castAdd n2 k)).1, (f2.step sb fun k => iv (Fin.natAdd n1 k)).1), (g1.step sc (f1.step sa fun k => iv (Fin.castAdd n2 k)).2).1, (g2.step sd (f2.step sb fun k => iv (Fin.natAdd n1 k)).2).1), Fin.append (g1.step sc (f1.step sa fun k => iv (Fin.castAdd n2 k)).2).2 (g2.step sd (f2.step sb fun k => iv (Fin.natAdd n1 k)).2).2)) e2)) (Eq.refl ((((f1.step sa fun k => iv (Fin.castAdd n2 k)).1, (f2.step sb fun k => iv (Fin.natAdd n1 k)).1), (g1.step sc (f1.step sa fun k => iv (Fin.castAdd n2 k)).2).1, (g2.step sd (f2.step sb fun k => iv (Fin.natAdd n1 k)).2).1), Fin.append (g1.step sc (f1.step sa fun k => iv (Fin.castAdd n2 k)).2).2 (g2.step sd (f2.step sb fun k => iv (Fin.natAdd n1 k)).2).2)))); have hstepR := rfl; id (Eq.mpr (id (congrArg (fun _a => _a.2 :: (InformationSystem.eval ((f1.parallel f2).sequential (g1.parallel g2)) _a.1 is).2 = (((f1.sequential g1).parallel (f2.sequential g2)).step ((sa, sc), sb, sd) iv).2 :: (InformationSystem.eval ((f1.sequential g1).parallel (f2.sequential g2)) (((f1.sequential g1).parallel (f2.sequential g2)).step ((sa, sc), sb, sd) iv).1 is).2) hstepL)) (Eq.mpr (id (congrArg (fun _a => ((((f1.step sa fun k => iv (Fin.castAdd n2 k)).1, (f2.step sb fun k => iv (Fin.natAdd n1 k)).1), (g1.step sc (f1.step sa fun k => iv (Fin.castAdd n2 k)).2).1, (g2.step sd (f2.step sb fun k => iv (Fin.natAdd n1 k)).2).1), Fin.append (g1.step sc (f1.step sa fun k => iv (Fin.castAdd n2 k)).2).2 (g2.step sd (f2.step sb fun k => iv (Fin.natAdd n1 k)).2).2).2 :: (InformationSystem.eval ((f1.parallel f2).sequential (g1.parallel g2)) ((((f1.step sa fun k => iv (Fin.castAdd n2 k)).1, (f2.step sb fun k => iv (Fin.natAdd n1 k)).1), (g1.step sc (f1.step sa fun k => iv (Fin.castAdd n2 k)).2).1, (g2.step sd (f2.step sb fun k => iv (Fin.natAdd n1 k)).2).1), Fin.append (g1.step sc (f1.step sa fun k => iv (Fin.castAdd n2 k)).2).2 (g2.step sd (f2.step sb fun k => iv (Fin.natAdd n1 k)).2).2).1 is).2 = _a.2 :: (InformationSystem.eval ((f1.sequential g1).parallel (f2.sequential g2)) _a.1 is).2) hstepR)) (congrArg (List.cons ((((f1.step sa fun k => iv (Fin.castAdd n2 k)).1, (f2.step sb fun k => iv (Fin.natAdd n1 k)).1), (g1.step sc (f1.step sa fun k => iv (Fin.castAdd n2 k)).2).1, (g2.step sd (f2.step sb fun k => iv (Fin.natAdd n1 k)).2).1), Fin.append (g1.step sc (f1.step sa fun k => iv (Fin.castAdd n2 k)).2).2 (g2.step sd (f2.step sb fun k => iv (Fin.natAdd n1 k)).2).2).2) hnextA)))) is sa sb sc sd
Complexity: 74058 (size of the value term)
Dependencies: Component, Component.parallel, Component.sequential, InformationSystem.equivalent, instNonemptyForallFin_computerNetworks, instNormForallFin_computerNetworks, instNormProd_computerNetworks
Proof dependencies: InformationSystem.eval
Mathlib dependencies: Fin.append, Fin.append_left, Fin.append_right, Norm
Lean core dependencies: Eq, Eq.mpr, Fin, Fin.castAdd, Fin.natAdd, List, Nat, Nonempty, Prod, congrArg, funext, id, rfl
Used by: Component.Hom.tensor_comp_tensor
Component.recast_recast
theorem Component.recast_recast {Wire : Type} [Nonempty Wire] [Norm Wire] {State : Type} [Nonempty State] [Norm State] {n n' n'' m m' m'' : ℕ} (h1 : n = n') (h2 : m = m') (h1' : n' = n'') (h2' : m' = m'') (c : Component State Wire Wire n m) : Component.recast h1' h2' (Component.recast h1 h2 c) = Component.recast ⋯ ⋯ c
Show details
fun {Wire} [Nonempty Wire] [Norm Wire] {State} [Nonempty State] [Norm State] {n n' n'' m m' m''} h1 h2 h1' h2' c => Eq.rec (motive := fun {n'} h1 => ∀ (h1' : n' = n''), Component.recast h1' h2' (Component.recast h1 h2 c) = Component.recast (Eq.trans h1 h1') (Eq.trans h2 h2') c) (fun h1' => Eq.rec (motive := fun {m'} h2 => ∀ (h2' : m' = m''), Component.recast h1' h2' (Component.recast (Eq.refl n) h2 c) = Component.recast (Eq.trans (Eq.refl n) h1') (Eq.trans h2 h2') c) (fun h2' => h1' ▸ h2' ▸ Eq.refl (Component.recast (Eq.refl n) (Eq.refl m) (Component.recast (Eq.refl n) (Eq.refl m) c))) h2 h2') h1 h1'
Complexity: 959 (size of the value term)
Dependencies: Component, Component.recast
Mathlib dependencies: Norm
Used by: Component.Hom.recast_recast
Component.Hom.recast_recast
theorem Component.Hom.recast_recast {Wire : Type} [Nonempty Wire] [Norm Wire] {n n' n'' m m' m'' : ℕ} (h1 : n = n') (h2 : m = m') (h1' : n' = n'') (h2' : m' = m'') (f : Component.Hom Wire n m) : Component.Hom.recast h1' h2' (Component.Hom.recast h1 h2 f) = Component.Hom.recast ⋯ ⋯ f
Show details
fun {Wire} [Nonempty Wire] [Norm Wire] {n n' n'' m m' m''} h1 h2 h1' h2' f => Quotient.ind (fun f => id (Eq.mpr (id (congrArg (fun _a => ⟦{ State := f.State, nonempty := inferInstance, size := inferInstance, component := _a, state := f.state }⟧ = ⟦{ State := f.State, nonempty := inferInstance, size := inferInstance, component := Component.recast (Eq.trans h1 h1') (Eq.trans h2 h2') f.component, state := f.state }⟧) (Component.recast_recast h1 h2 h1' h2' f.component))) (Eq.refl ⟦{ State := f.State, nonempty := inferInstance, size := inferInstance, component := Component.recast (Eq.trans h1 h1') (Eq.trans h2 h2') f.component, state := f.state }⟧))) f
Complexity: 4243 (size of the value term)
Dependencies: Component.Hom, Component.Hom.recast
Proof dependencies: Component, Component.Arrow, Component.Arrow.setoid, Component.recast, Component.recast_recast
Mathlib dependencies: Norm
Lean core dependencies: Eq, Eq.mpr, Eq.trans, Nat, Nonempty, Quotient, Quotient.ind, Quotient.mk, congrArg, id, inferInstance
Used by: Component.monoidalCategory
Component.Hom.eqToHom_eq_recast_id
theorem Component.Hom.eqToHom_eq_recast_id {Wire : Type} [Nonempty Wire] [Norm Wire] {n m : ℕ} (h : n = m) : CategoryTheory.eqToHom h = Component.Hom.recast ⋯ h (Component.Hom.id Wire n)
Show details
fun {Wire} [Nonempty Wire] [Norm Wire] {n m} h => h ▸ Eq.refl (CategoryTheory.eqToHom (Eq.refl n))
Complexity: 175 (size of the value term)
Dependencies: Component.Hom.id, Component.Hom.recast, Component.category
Mathlib dependencies: CategoryTheory.eqToHom, Norm
Component.Hom.comp_eqToHom
theorem Component.Hom.comp_eqToHom {Wire : Type} [Nonempty Wire] [Norm Wire] {n m p : ℕ} (h : m = p) (f : Component.Hom Wire n m) : f.comp (CategoryTheory.eqToHom h) = Component.Hom.recast ⋯ h f
Show details
fun {Wire} [Nonempty Wire] [Norm Wire] {n m p} h f => h ▸ id (Eq.mpr (id (congrArg (fun _a => _a = Component.Hom.recast rfl rfl f) (Component.Hom.comp_id f))) (Quotient.ind (fun f => Eq.refl ⟦f⟧) f))
Complexity: 717 (size of the value term)
Dependencies: Component.Hom, Component.Hom.comp, Component.Hom.recast, Component.category
Proof dependencies: Component.Arrow, Component.Arrow.setoid, Component.Hom.comp_id, Component.Hom.id
Mathlib dependencies: CategoryTheory.eqToHom, Norm
Lean core dependencies: Eq, Eq.mpr, Nat, Nonempty, Quotient.ind, Quotient.mk, congrArg, id, rfl
Used by: Component.monoidalCategory
Component.Hom.eqToHom_comp
theorem Component.Hom.eqToHom_comp {Wire : Type} [Nonempty Wire] [Norm Wire] {n m p : ℕ} (h : n = m) (f : Component.Hom Wire m p) : Component.Hom.comp (CategoryTheory.eqToHom h) f = Component.Hom.recast ⋯ ⋯ f
Show details
fun {Wire} [Nonempty Wire] [Norm Wire] {n m p} h f => Eq.rec (motive := fun {m} h => ∀ (f : Component.Hom Wire m p), Component.Hom.comp (CategoryTheory.eqToHom h) f = Component.Hom.recast (Eq.symm h) rfl f) (fun f => id (Eq.mpr (id (congrArg (fun _a => _a = Component.Hom.recast rfl rfl f) (Component.Hom.id_comp f))) (Quotient.ind (fun f => Eq.refl ⟦f⟧) f))) h f
Complexity: 759 (size of the value term)
Dependencies: Component.Hom, Component.Hom.comp, Component.Hom.recast, Component.category
Proof dependencies: Component.Arrow, Component.Arrow.setoid, Component.Hom.id, Component.Hom.id_comp
Mathlib dependencies: CategoryTheory.eqToHom, Norm
Lean core dependencies: Eq, Eq.mpr, Eq.symm, Nat, Nonempty, Quotient.ind, Quotient.mk, congrArg, id, rfl
Used by: Component.monoidalCategory
Component.Hom.recast_eqToHom
theorem Component.Hom.recast_eqToHom {Wire : Type} [Nonempty Wire] [Norm Wire] {a b c d : ℕ} (hn : b = a) (h : b = c) (hm : c = d) : Component.Hom.recast hn hm (CategoryTheory.eqToHom h) = CategoryTheory.eqToHom ⋯
Show details
fun {Wire} [Nonempty Wire] [Norm Wire] {a b c d} hn h hm => hn ▸ Eq.rec (motive := fun {c} h => ∀ (hm : c = d), Component.Hom.recast (Eq.refl b) hm (CategoryTheory.eqToHom h) = CategoryTheory.eqToHom (Eq.trans (Eq.symm (Eq.refl b)) (Eq.trans h hm))) (fun hm => hm ▸ Eq.refl (Component.Hom.recast (Eq.refl b) (Eq.refl b) (CategoryTheory.eqToHom (Eq.refl b)))) h hm
Complexity: 541 (size of the value term)
Dependencies: Component.Hom, Component.Hom.recast, Component.category
Mathlib dependencies: CategoryTheory.eqToHom, Norm
Used by: Component.monoidalCategory
Component.recast_parallel_left
theorem Component.recast_parallel_left {Wire : Type} [Nonempty Wire] [Norm Wire] {State1 State2 : Type} [Nonempty State1] [Norm State1] [Nonempty State2] [Norm State2] {n1 n1' m1 m1' n2 m2 : ℕ} (hn : n1 = n1') (hm : m1 = m1') (c1 : Component State1 Wire Wire n1 m1) (c2 : Component State2 Wire Wire n2 m2) : (Component.recast hn hm c1).parallel c2 = Component.recast ⋯ ⋯ (c1.parallel c2)
Show details
fun {Wire} [Nonempty Wire] [Norm Wire] {State1 State2} [Nonempty State1] [Norm State1] [Nonempty State2] [Norm State2] {n1 n1' m1 m1' n2 m2} hn hm c1 c2 => hn ▸ hm ▸ Eq.refl ((Component.recast (Eq.refl n1) (Eq.refl m1) c1).parallel c2)
Complexity: 1033 (size of the value term)
Dependencies: Component, Component.parallel, Component.recast, instNormProd_computerNetworks
Mathlib dependencies: Norm
Used by: Component.Hom.tensor_recast_left
Component.recast_parallel_right
theorem Component.recast_parallel_right {Wire : Type} [Nonempty Wire] [Norm Wire] {State1 State2 : Type} [Nonempty State1] [Norm State1] [Nonempty State2] [Norm State2] {n1 m1 n2 n2' m2 m2' : ℕ} (hn : n2 = n2') (hm : m2 = m2') (c1 : Component State1 Wire Wire n1 m1) (c2 : Component State2 Wire Wire n2 m2) : c1.parallel (Component.recast hn hm c2) = Component.recast ⋯ ⋯ (c1.parallel c2)
Show details
fun {Wire} [Nonempty Wire] [Norm Wire] {State1 State2} [Nonempty State1] [Norm State1] [Nonempty State2] [Norm State2] {n1 m1 n2 n2' m2 m2'} hn hm c1 c2 => hn ▸ hm ▸ Eq.refl (c1.parallel (Component.recast (Eq.refl n2) (Eq.refl m2) c2))
Complexity: 1033 (size of the value term)
Dependencies: Component, Component.parallel, Component.recast, instNormProd_computerNetworks
Mathlib dependencies: Norm
Used by: Component.Hom.tensor_recast_right
Component.Hom.tensor_recast_left
theorem Component.Hom.tensor_recast_left {Wire : Type} [Nonempty Wire] [Norm Wire] {n1 n1' m1 m1' n2 m2 : ℕ} (hn : n1 = n1') (hm : m1 = m1') (f1 : Component.Hom Wire n1 m1) (f2 : Component.Hom Wire n2 m2) : (Component.Hom.recast hn hm f1).tensor f2 = Component.Hom.recast ⋯ ⋯ (f1.tensor f2)
Show details
fun {Wire} [Nonempty Wire] [Norm Wire] {n1 n1' m1 m1' n2 m2} hn hm f1 f2 => Quotient.ind (fun f1 => Quotient.ind (fun f2 => id (Eq.mpr (id (congrArg (fun _a => ⟦{ State := f1.State × f2.State, nonempty := inferInstance, size := inferInstance, component := _a, state := (f1.state, f2.state) }⟧ = ⟦{ State := f1.State × f2.State, nonempty := inferInstance, size := inferInstance, component := Component.recast (congrArg (fun x => x + n2) hn) (congrArg (fun x => x + m2) hm) (f1.component.parallel f2.component), state := (f1.state, f2.state) }⟧) (Component.recast_parallel_left hn hm f1.component f2.component))) (Eq.refl ⟦{ State := f1.State × f2.State, nonempty := inferInstance, size := inferInstance, component := Component.recast (congrArg (fun x => x + n2) hn) (congrArg (fun x => x + m2) hm) (f1.component.parallel f2.component), state := (f1.state, f2.state) }⟧))) f2) f1
Complexity: 11449 (size of the value term)
Dependencies: Component.Hom, Component.Hom.recast, Component.Hom.tensor
Proof dependencies: Component, Component.Arrow, Component.Arrow.setoid, Component.parallel, Component.recast, Component.recast_parallel_left, instNormProd_computerNetworks
Mathlib dependencies: Norm
Lean core dependencies: Eq, Eq.mpr, Nat, Nonempty, Prod, Quotient, Quotient.ind, Quotient.mk, congrArg, id, inferInstance
Used by: Component.monoidalCategory
Component.Hom.tensor_recast_right
theorem Component.Hom.tensor_recast_right {Wire : Type} [Nonempty Wire] [Norm Wire] {n1 m1 n2 n2' m2 m2' : ℕ} (hn : n2 = n2') (hm : m2 = m2') (f1 : Component.Hom Wire n1 m1) (f2 : Component.Hom Wire n2 m2) : f1.tensor (Component.Hom.recast hn hm f2) = Component.Hom.recast ⋯ ⋯ (f1.tensor f2)
Show details
fun {Wire} [Nonempty Wire] [Norm Wire] {n1 m1 n2 n2' m2 m2'} hn hm f1 f2 => Quotient.ind (fun f1 => Quotient.ind (fun f2 => id (Eq.mpr (id (congrArg (fun _a => ⟦{ State := f1.State × f2.State, nonempty := inferInstance, size := inferInstance, component := _a, state := (f1.state, f2.state) }⟧ = ⟦{ State := f1.State × f2.State, nonempty := inferInstance, size := inferInstance, component := Component.recast (congrArg (fun x => n1 + x) hn) (congrArg (fun x => m1 + x) hm) (f1.component.parallel f2.component), state := (f1.state, f2.state) }⟧) (Component.recast_parallel_right hn hm f1.component f2.component))) (Eq.refl ⟦{ State := f1.State × f2.State, nonempty := inferInstance, size := inferInstance, component := Component.recast (congrArg (fun x => n1 + x) hn) (congrArg (fun x => m1 + x) hm) (f1.component.parallel f2.component), state := (f1.state, f2.state) }⟧))) f2) f1
Complexity: 11449 (size of the value term)
Dependencies: Component.Hom, Component.Hom.recast, Component.Hom.tensor
Proof dependencies: Component, Component.Arrow, Component.Arrow.setoid, Component.parallel, Component.recast, Component.recast_parallel_right, instNormProd_computerNetworks
Mathlib dependencies: Norm
Lean core dependencies: Eq, Eq.mpr, Nat, Nonempty, Prod, Quotient, Quotient.ind, Quotient.mk, congrArg, id, inferInstance
Used by: Component.monoidalCategory
Component.Hom.tensor_id_id
theorem Component.Hom.tensor_id_id {Wire : Type} [Nonempty Wire] [Norm Wire] (n m : ℕ) : (Component.Hom.id Wire n).tensor (Component.Hom.id Wire m) = Component.Hom.id Wire (n + m)
Show details
fun {Wire} [Nonempty Wire] [Norm Wire] n m => Quotient.sound fun is => List.rec (Eq.refl (InformationSystem.eval ((fun f g => { State := f.State × g.State, nonempty := Component.Hom.tensor._proof_1 f g, size := inferInstance, component := f.component.parallel g.component, state := (f.state, g.state) }) { State := Unit, nonempty := Component.Hom.id._proof_1, size := inferInstance, component := Component.id Wire n, state := () } { State := Unit, nonempty := Component.Hom.id._proof_1, size := inferInstance, component := Component.id Wire m, state := () }).component ((fun f g => { State := f.State × g.State, nonempty := Component.Hom.tensor._proof_1 f g, size := inferInstance, component := f.component.parallel g.component, state := (f.state, g.state) }) { State := Unit, nonempty := Component.Hom.id._proof_1, size := inferInstance, component := Component.id Wire n, state := () } { State := Unit, nonempty := Component.Hom.id._proof_1, size := inferInstance, component := Component.id Wire m, state := () }).state []).2) (fun iv is ih => have hstep := id ((fun {α β} fst fst_1 e_fst => Eq.rec (motive := fun fst_2 e_fst => ∀ (snd snd_1 : β), snd = snd_1 → (fst, snd) = (fst_2, snd_1)) (fun snd snd_1 e_snd => e_snd ▸ Eq.refl (fst, snd)) e_fst) ((), ()) ((), ()) (Eq.refl ((), ())) (Fin.append (fun k => iv (Fin.castAdd m k)) fun k => iv (Fin.natAdd n k)) iv Fin.append_castAdd_natAdd); id (Eq.mpr (id (congrFun' (congrArg Eq (congrArg Prod.snd (congr (congrArg Prod.mk (congrArg Prod.fst (congrFun' (congrArg (InformationSystem.eval ((Component.id Wire n).parallel (Component.id Wire m))) (congrArg Prod.fst hstep)) is))) (congr (congrArg List.cons (congrArg Prod.snd hstep)) (congrArg Prod.snd (congrFun' (congrArg (InformationSystem.eval ((Component.id Wire n).parallel (Component.id Wire m))) (congrArg Prod.fst hstep)) is)))))) (((Component.id Wire (n + m)).1 () iv).2 :: (InformationSystem.eval (Component.id Wire (n + m)) ((Component.id Wire (n + m)).1 () iv).1 is).2))) (congrArg (List.cons iv) ih))) is
Complexity: 31143 (size of the value term)
Dependencies: Component.Hom, Component.Hom.id, Component.Hom.tensor
Proof dependencies: Component.Arrow, Component.Arrow.setoid, Component.id, Component.parallel, InformationSystem.eval, instNonemptyForallFin_computerNetworks, instNormForallFin_computerNetworks, instNormProd_computerNetworks, instNormUnit_computerNetworks
Mathlib dependencies: Fin.append, Fin.append_castAdd_natAdd, Norm
Lean core dependencies: Eq, Eq.mpr, Fin, Fin.castAdd, Fin.natAdd, List, Nat, Nonempty, Prod, Quotient.sound, Unit, Unit.unit, congr, congrArg, congrFun', id, inferInstance
Used by: Component.monoidalCategory
Component.Hom.tensor_empty
theorem Component.Hom.tensor_empty {Wire : Type} [Nonempty Wire] [Norm Wire] {n m : ℕ} (f : Component.Hom Wire n m) : Component.Hom.recast ⋯ ⋯ ((Component.Hom.id Wire 0).tensor f) = f
Show details
fun {Wire} [Nonempty Wire] [Norm Wire] {n m} f => Quotient.ind (fun f => Quotient.sound (Component.empty_parallel f.component f.state)) f
Complexity: 1799 (size of the value term)
Dependencies: Component.Hom, Component.Hom.id, Component.Hom.recast, Component.Hom.tensor
Proof dependencies: Component.Arrow, Component.Arrow.setoid, Component.empty_parallel, Component.id, Component.parallel, Component.recast, instNormProd_computerNetworks, instNormUnit_computerNetworks
Mathlib dependencies: Norm
Lean core dependencies: Eq, Nat, Nat.zero_add, Nonempty, Prod, Quotient.ind, Quotient.sound, Unit, Unit.unit, inferInstance
Used by: Component.monoidalCategory
Component.Hom.tensor_assoc
theorem Component.Hom.tensor_assoc {Wire : Type} [Nonempty Wire] [Norm Wire] {n1 m1 n2 m2 n3 m3 : ℕ} (f1 : Component.Hom Wire n1 m1) (f2 : Component.Hom Wire n2 m2) (f3 : Component.Hom Wire n3 m3) : Component.Hom.recast ⋯ ⋯ ((f1.tensor f2).tensor f3) = f1.tensor (f2.tensor f3)
Show details
fun {Wire} [Nonempty Wire] [Norm Wire] {n1 m1 n2 m2 n3 m3} f1 f2 f3 => Quotient.ind (fun f1 => Quotient.ind (fun f2 => Quotient.ind (fun f3 => Quotient.sound (Component.parallel_assoc f1.component f2.component f3.component f1.state f2.state f3.state)) f3) f2) f1
Complexity: 5515 (size of the value term)
Dependencies: Component.Hom, Component.Hom.recast, Component.Hom.tensor
Proof dependencies: Component.Arrow, Component.Arrow.setoid, Component.parallel, Component.parallel_assoc, Component.recast, instNormProd_computerNetworks
Mathlib dependencies: Norm
Lean core dependencies: Eq, Nat, Nat.add_assoc, Nonempty, Prod, Quotient.ind, Quotient.mk, Quotient.sound, inferInstance
Used by: Component.monoidalCategory
Component.Hom.tensor_comp_tensor
theorem Component.Hom.tensor_comp_tensor {Wire : Type} [Nonempty Wire] [Norm Wire] {n1 m1 p1 n2 m2 p2 : ℕ} (f1 : Component.Hom Wire n1 m1) (f2 : Component.Hom Wire n2 m2) (g1 : Component.Hom Wire m1 p1) (g2 : Component.Hom Wire m2 p2) : (f1.tensor f2).comp (g1.tensor g2) = (f1.comp g1).tensor (f2.comp g2)
Show details
fun {Wire} [Nonempty Wire] [Norm Wire] {n1 m1 p1 n2 m2 p2} f1 f2 g1 g2 => Quotient.ind (fun f1 => Quotient.ind (fun f2 => Quotient.ind (fun g1 => Quotient.ind (fun g2 => Quotient.sound (Component.interchange f1.component f2.component g1.component g2.component f1.state f2.state g1.state g2.state)) g2) g1) f2) f1
Complexity: 4949 (size of the value term)
Dependencies: Component.Hom, Component.Hom.comp, Component.Hom.tensor
Proof dependencies: Component.Arrow, Component.Arrow.setoid, Component.interchange, Component.parallel, Component.sequential, instNormProd_computerNetworks
Mathlib dependencies: Norm
Lean core dependencies: Eq, Nat, Nonempty, Prod, Quotient.ind, Quotient.mk, Quotient.sound, inferInstance
Used by: Component.monoidalCategory
Component.monoidalCategoryStruct
def Component.monoidalCategoryStruct (Wire : Type) [Nonempty Wire] [Norm Wire] : CategoryTheory.MonoidalCategoryStruct ℕ
Show details
| Component.monoidalCategoryStruct Wire = { tensorObj := fun n m => n + m, whiskerLeft := fun n {x x_1} f => (Component.Hom.id Wire n).tensor f, whiskerRight := fun {x x_1} f m => Component.Hom.tensor f (Component.Hom.id Wire m), tensorHom := fun {X₁ Y₁ X₂ Y₂} f g => Component.Hom.tensor f g, tensorUnit := 0, associator := fun n m p => CategoryTheory.eqToIso ⋯, leftUnitor := fun n => CategoryTheory.eqToIso ⋯, rightUnitor := fun n => CategoryTheory.eqToIso ⋯ }
Complexity: 431 (size of the value term)
Outer dependencies: Component.category
Inner dependencies: Component.Hom.id, Component.Hom.tensor
Mathlib dependencies: CategoryTheory.MonoidalCategoryStruct, CategoryTheory.eqToIso, Norm
Lean core dependencies: Nat, Nat.add_assoc, Nat.add_zero, Nat.zero_add, Nonempty
Component.monoidalCategory
def Component.monoidalCategory (Wire : Type) [Nonempty Wire] [Norm Wire] : CategoryTheory.MonoidalCategory ℕ
Show details
| Component.monoidalCategory Wire = CategoryTheory.MonoidalCategory.ofTensorHom ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯
Complexity: 237 (size of the value term)
Outer dependencies: Component.category
Inner dependencies: Component.Arrow, Component.Arrow.setoid, Component.Hom, Component.Hom.comp, Component.Hom.comp_eqToHom, Component.Hom.eqToHom_comp, Component.Hom.eqToHom_eq_recast_id, Component.Hom.id, Component.Hom.recast, Component.Hom.recast_eqToHom, Component.Hom.recast_recast, Component.Hom.tensor, Component.Hom.tensor_assoc, Component.Hom.tensor_comp_tensor, Component.Hom.tensor_empty, Component.Hom.tensor_id_id, Component.Hom.tensor_recast_left, Component.Hom.tensor_recast_right, Component.empty, Component.id, Component.monoidalCategoryStruct, Component.parallel, Component.parallel_congr, Component.parallel_empty, InformationSystem.equivalent, InformationSystem.eval, instNonemptyForallFin_computerNetworks, instNormForallFin_computerNetworks, instNormProd_computerNetworks, instNormUnit_computerNetworks
Mathlib dependencies: CategoryTheory.MonoidalCategory, CategoryTheory.MonoidalCategory.ofTensorHom, CategoryTheory.eqToHom, CategoryTheory.eqToIso, CategoryTheory.eqToIso.hom, Norm
Lean core dependencies: Eq, Eq.mp, Eq.mpr, Eq.symm, Eq.trans, Fin, Fin.elim0, List, Nat, Nat.add_assoc, Nat.add_zero, Nat.zero_add, Nonempty, Prod, Quotient.ind, Quotient.sound, True, Unit, Unit.unit, congr, congrArg, congrFun', eq_self, funext, id, inferInstance, of_eq_true, rfl
Component.symmetry_symmetry
theorem Component.symmetry_symmetry {Wire : Type} [Nonempty Wire] [Norm Wire] (n m : ℕ) : InformationSystem.equivalent ((Component.symmetry Wire n m).sequential (Component.symmetry Wire m n)) (Component.id Wire (n + m)) ((), ()) ()
Show details
fun {Wire} [Nonempty Wire] [Norm Wire] n m is => List.rec (Eq.refl (InformationSystem.eval ((Component.symmetry Wire n m).sequential (Component.symmetry Wire m n)) ((), ()) []).2) (fun iv is ih => have hstep := id ((fun {α β} fst fst_1 e_fst => Eq.rec (motive := fun fst_2 e_fst => ∀ (snd snd_1 : β), snd = snd_1 → (fst, snd) = (fst_2, snd_1)) (fun snd snd_1 e_snd => e_snd ▸ Eq.refl (fst, snd)) e_fst) ((), ()) ((), ()) (Eq.refl ((), ())) (Fin.append (fun k => Fin.append (fun k => iv (Fin.natAdd n k)) (fun k => iv (Fin.castAdd m k)) (Fin.natAdd m k)) fun k => Fin.append (fun k => iv (Fin.natAdd n k)) (fun k => iv (Fin.castAdd m k)) (Fin.castAdd n k)) iv (Eq.mpr (id (congrFun' (congrArg Eq (congr (congrArg Fin.append (funext fun k => Fin.append_right (fun k => iv (Fin.natAdd n k)) (fun k => iv (Fin.castAdd m k)) k)) (funext fun k => Fin.append_left (fun k => iv (Fin.natAdd n k)) (fun k => iv (Fin.castAdd m k)) k))) iv)) Fin.append_castAdd_natAdd)); id (Eq.mpr (id (congrFun' (congrArg Eq (congrArg Prod.snd (congr (congrArg Prod.mk (congrArg Prod.fst (congrFun' (congrArg (InformationSystem.eval ((Component.symmetry Wire n m).sequential (Component.symmetry Wire m n))) (congrArg Prod.fst hstep)) is))) (congr (congrArg List.cons (congrArg Prod.snd hstep)) (congrArg Prod.snd (congrFun' (congrArg (InformationSystem.eval ((Component.symmetry Wire n m).sequential (Component.symmetry Wire m n))) (congrArg Prod.fst hstep)) is)))))) (((Component.id Wire (n + m)).1 () iv).2 :: (InformationSystem.eval (Component.id Wire (n + m)) ((Component.id Wire (n + m)).1 () iv).1 is).2))) (congrArg (List.cons iv) ih))) is
Complexity: 20635 (size of the value term)
Dependencies: Component.id, Component.sequential, Component.symmetry, InformationSystem.equivalent, instNonemptyForallFin_computerNetworks, instNormForallFin_computerNetworks, instNormProd_computerNetworks, instNormUnit_computerNetworks
Proof dependencies: InformationSystem.eval
Mathlib dependencies: Fin.append, Fin.append_castAdd_natAdd, Fin.append_left, Fin.append_right, Norm
Lean core dependencies: Eq, Eq.mpr, Fin, Fin.castAdd, Fin.natAdd, List, Nat, Nonempty, Prod, Unit, Unit.unit, congr, congrArg, congrFun', funext, id
Used by: Component.Hom.symmetry_symmetry
Component.Hom.symmetry_symmetry
theorem Component.Hom.symmetry_symmetry {Wire : Type} [Nonempty Wire] [Norm Wire] (n m : ℕ) : (Component.Hom.symmetry Wire n m).comp (Component.Hom.symmetry Wire m n) = Component.Hom.id Wire (n + m)
Show details
fun {Wire} [Nonempty Wire] [Norm Wire] n m => Quotient.sound (Component.symmetry_symmetry n m)
Complexity: 1543 (size of the value term)
Dependencies: Component.Hom, Component.Hom.comp, Component.Hom.id, Component.Hom.symmetry
Proof dependencies: Component.Arrow, Component.Arrow.setoid, Component.id, Component.sequential, Component.symmetry, Component.symmetry_symmetry, instNormProd_computerNetworks, instNormUnit_computerNetworks
Mathlib dependencies: Norm
Lean core dependencies: Eq, Nat, Nonempty, Prod, Quotient.sound, Unit, Unit.unit, inferInstance
Component.braiding
def Component.braiding (Wire : Type) [Nonempty Wire] [Norm Wire] (n m : ℕ) : n + m ≅ m + n
Show details
| Component.braiding Wire n m = { hom := Component.Hom.symmetry Wire n m, inv := Component.Hom.symmetry Wire m n, hom_inv_id := ⋯, inv_hom_id := ⋯ }
Complexity: 109 (size of the value term)
Outer dependencies: Component.category
Inner dependencies: Component.Hom.symmetry, Component.Hom.symmetry_symmetry
Mathlib dependencies: CategoryTheory.Iso, Norm
Component.Hom.tensor_comm
theorem Component.Hom.tensor_comm {Wire : Type} [Nonempty Wire] [Norm Wire] {n1 m1 n2 m2 : ℕ} (f1 : Component.Hom Wire n1 m1) (f2 : Component.Hom Wire n2 m2) : f1.tensor f2 = ((Component.Hom.symmetry Wire n1 n2).comp (f2.tensor f1)).comp (Component.Hom.symmetry Wire m2 m1)
Show details
fun {Wire} [Nonempty Wire] [Norm Wire] {n1 m1 n2 m2} f1 f2 => Quotient.ind (fun f1 => Quotient.ind (fun f2 => Quotient.sound (Component.parallel_comm f1.component f2.component f1.state f2.state)) f2) f1
Complexity: 4277 (size of the value term)
Dependencies: Component.Hom, Component.Hom.comp, Component.Hom.symmetry, Component.Hom.tensor
Proof dependencies: Component.Arrow, Component.Arrow.setoid, Component.parallel, Component.parallel_comm, Component.sequential, Component.symmetry, instNormProd_computerNetworks, instNormUnit_computerNetworks
Mathlib dependencies: Norm
Lean core dependencies: Eq, Nat, Nonempty, Prod, Quotient.ind, Quotient.mk, Quotient.sound, Unit, Unit.unit, inferInstance
Component.braiding_naturality_right
theorem Component.braiding_naturality_right {Wire : Type} [Nonempty Wire] [Norm Wire] {X Y Z : ℕ} (f : Component.Hom Wire Y Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X f) (Component.braiding Wire X Z).hom = CategoryTheory.CategoryStruct.comp (Component.braiding Wire X Y).hom (CategoryTheory.MonoidalCategoryStruct.whiskerRight f X)
Show details
fun {Wire} [Nonempty Wire] [Norm Wire] {X Y Z} f => id (Eq.mpr (id (congrArg (fun _a => _a.comp (Component.Hom.symmetry Wire X Z) = (Component.Hom.symmetry Wire X Y).comp (f.tensor (Component.Hom.id Wire X))) (Component.Hom.tensor_comm (Component.Hom.id Wire X) f))) (Eq.mpr (id (congrArg (fun _a => _a = (Component.Hom.symmetry Wire X Y).comp (f.tensor (Component.Hom.id Wire X))) (Component.Hom.comp_assoc ((Component.Hom.symmetry Wire X Y).comp (f.tensor (Component.Hom.id Wire X))) (Component.Hom.symmetry Wire Z X) (Component.Hom.symmetry Wire X Z)))) (Eq.mpr (id (congrArg (fun _a => ((Component.Hom.symmetry Wire X Y).comp (f.tensor (Component.Hom.id Wire X))).comp _a = (Component.Hom.symmetry Wire X Y).comp (f.tensor (Component.Hom.id Wire X))) (Component.Hom.symmetry_symmetry Z X))) (Eq.mpr (id (congrArg (fun _a => _a = (Component.Hom.symmetry Wire X Y).comp (f.tensor (Component.Hom.id Wire X))) (Component.Hom.comp_id ((Component.Hom.symmetry Wire X Y).comp (f.tensor (Component.Hom.id Wire X)))))) (Eq.refl ((Component.Hom.symmetry Wire X Y).comp (f.tensor (Component.Hom.id Wire X))))))))
Complexity: 8849 (size of the value term)
Dependencies: Component.Hom, Component.braiding, Component.category, Component.monoidalCategoryStruct
Proof dependencies: Component.Hom.comp, Component.Hom.comp_assoc, Component.Hom.comp_id, Component.Hom.id, Component.Hom.symmetry, Component.Hom.symmetry_symmetry, Component.Hom.tensor, Component.Hom.tensor_comm
Mathlib dependencies: Norm
Used by: Component.braidedCategory
Component.braiding_naturality_left
theorem Component.braiding_naturality_left {Wire : Type} [Nonempty Wire] [Norm Wire] {X Y Z : ℕ} (f : Component.Hom Wire X Y) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight f Z) (Component.braiding Wire Y Z).hom = CategoryTheory.CategoryStruct.comp (Component.braiding Wire X Z).hom (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Z f)
Show details
fun {Wire} [Nonempty Wire] [Norm Wire] {X Y Z} f => id (Eq.mpr (id (congrArg (fun _a => _a.comp (Component.Hom.symmetry Wire Y Z) = (Component.Hom.symmetry Wire X Z).comp ((Component.Hom.id Wire Z).tensor f)) (Component.Hom.tensor_comm f (Component.Hom.id Wire Z)))) (Eq.mpr (id (congrArg (fun _a => _a = (Component.Hom.symmetry Wire X Z).comp ((Component.Hom.id Wire Z).tensor f)) (Component.Hom.comp_assoc ((Component.Hom.symmetry Wire X Z).comp ((Component.Hom.id Wire Z).tensor f)) (Component.Hom.symmetry Wire Z Y) (Component.Hom.symmetry Wire Y Z)))) (Eq.mpr (id (congrArg (fun _a => ((Component.Hom.symmetry Wire X Z).comp ((Component.Hom.id Wire Z).tensor f)).comp _a = (Component.Hom.symmetry Wire X Z).comp ((Component.Hom.id Wire Z).tensor f)) (Component.Hom.symmetry_symmetry Z Y))) (Eq.mpr (id (congrArg (fun _a => _a = (Component.Hom.symmetry Wire X Z).comp ((Component.Hom.id Wire Z).tensor f)) (Component.Hom.comp_id ((Component.Hom.symmetry Wire X Z).comp ((Component.Hom.id Wire Z).tensor f))))) (Eq.refl ((Component.Hom.symmetry Wire X Z).comp ((Component.Hom.id Wire Z).tensor f)))))))
Complexity: 8849 (size of the value term)
Dependencies: Component.Hom, Component.braiding, Component.category, Component.monoidalCategoryStruct
Proof dependencies: Component.Hom.comp, Component.Hom.comp_assoc, Component.Hom.comp_id, Component.Hom.id, Component.Hom.symmetry, Component.Hom.symmetry_symmetry, Component.Hom.tensor, Component.Hom.tensor_comm
Mathlib dependencies: Norm
Used by: Component.braidedCategory
Component.equivalent_of_stationary
theorem Component.equivalent_of_stationary {Wire : Type} [Nonempty Wire] [Norm Wire] {State1 State2 : Type} [Nonempty State1] [Norm State1] [Nonempty State2] [Norm State2] {n m : ℕ} {c1 : Component State1 Wire Wire n m} {c2 : Component State2 Wire Wire n m} (s1 : State1) (s2 : State2) (stationary1 : ∀ (i : Fin n → Wire), (c1.step s1 i).1 = s1) (stationary2 : ∀ (i : Fin n → Wire), (c2.step s2 i).1 = s2) (hout : ∀ (i : Fin n → Wire), (c1.step s1 i).2 = (c2.step s2 i).2) : InformationSystem.equivalent c1 c2 s1 s2
Show details
fun {Wire} [Nonempty Wire] [Norm Wire] {State1 State2} [Nonempty State1] [Norm State1] [Nonempty State2] [Norm State2] {n m} {c1} {c2} s1 s2 stationary1 stationary2 hout is => List.rec (Eq.refl (InformationSystem.eval c1 s1 []).2) (fun iv is ih => Eq.mpr (id (congr (congrArg Eq (congrArg Prod.snd (congr (congrArg Prod.mk (congrArg Prod.fst (congrFun' (congrArg (InformationSystem.eval c1) (stationary1 iv)) is))) (congr (congrArg List.cons (hout iv)) (congrArg Prod.snd (congrFun' (congrArg (InformationSystem.eval c1) (stationary1 iv)) is)))))) (congrArg Prod.snd (congr (congrArg Prod.mk (congrArg Prod.fst (congrFun' (congrArg (InformationSystem.eval c2) (stationary2 iv)) is))) (congrArg (List.cons (c2.1 s2 iv).2) (congrArg Prod.snd (congrFun' (congrArg (InformationSystem.eval c2) (stationary2 iv)) is))))))) (congrArg (List.cons (c2.step s2 iv).2) ih)) is
Complexity: 6699 (size of the value term)
Dependencies: Component, InformationSystem.equivalent, instNonemptyForallFin_computerNetworks, instNormForallFin_computerNetworks
Proof dependencies: InformationSystem.eval
Mathlib dependencies: Norm
Fin.append_eval
theorem Fin.append_eval {a b : ℕ} {α : Type} (A : Fin a → α) (B : Fin b → α) (x : Fin (a + b)) : Fin.append A B x = if h : ↑x < a then A ⟨↑x, h⟩ else B ⟨↑x - a, ⋯⟩
Show details
fun {a b} {α} A B x => Or.casesOn (Nat.lt_or_ge (↑x) a) (fun h => Eq.mpr (id (congrArg (fun _a => Fin.append A B x = _a) (dif_pos h))) (have hx := Fin.ext (of_eq_true (eq_self ↑x)); Eq.trans (congrArg (Fin.append A B) hx) (Fin.append_left A B ⟨↑x, h⟩))) fun h => Eq.mpr (id (congrArg (fun _a => Fin.append A B x = _a) (dif_neg fun a_1 => Fin.append_eval._proof_1_1 x h a_1))) (have hx := Fin.ext (id (Decidable.byContradiction fun a_1 => Fin.append_eval._proof_1_3 x h a_1)); Eq.trans (congrArg (Fin.append A B) hx) (Fin.append_right A B ⟨↑x - a, Decidable.byContradiction fun a_1 => Fin.append_eval._proof_1_4 x h hx a_1⟩))
Complexity: 6675 (size of the value term)
Dependencies: (none)
Mathlib dependencies: Fin.append, Fin.append_left, Fin.append_right
Lean core dependencies: And, Bool, Decidable.byContradiction, Decidable.decide, Eq, Eq.mpr, Eq.symm, Eq.trans, False, Fin, Fin.castAdd, Fin.ext, Fin.natAdd, Fin.val_congr, GE.ge, GT.gt, 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.combine_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.ofNat_le_of_le, Lean.Omega.Int.ofNat_lt_of_lt, Lean.Omega.Int.ofNat_sub_dichotomy, 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.coordinate_eval_3, Lean.Omega.LinearCombo.coordinate_eval_4, Lean.Omega.LinearCombo.eval, Lean.Omega.LinearCombo.sub_eval, Lean.Omega.combo_sat', Lean.Omega.tidy_sat, Nat, Nat.cast, Nat.le_of_not_lt, Nat.lt_or_ge, Nat.lt_or_gt_of_ne, Not, Or, Or.elim, congrArg, dif_neg, dif_pos, dite, eq_self, id, le_of_le_of_eq, of_decide_eq_true, of_eq_true
Component.hexagon_forward_arrow
theorem Component.hexagon_forward_arrow {Wire : Type} [Nonempty Wire] [Norm Wire] (X Y Z : ℕ) : InformationSystem.equivalent (((Component.recast ⋯ ⋯ (Component.id Wire (X + Y + Z))).sequential (Component.symmetry Wire X (Y + Z))).sequential (Component.recast ⋯ ⋯ (Component.id Wire (Y + Z + X)))) ((((Component.symmetry Wire X Y).parallel (Component.id Wire Z)).sequential (Component.recast ⋯ ⋯ (Component.id Wire (Y + X + Z)))).sequential ((Component.id Wire Y).parallel (Component.symmetry Wire X Z))) (((), ()), ()) ((((), ()), ()), (), ())
Show details
fun {Wire} [⋯] [⋯] X Y Z => Component.equivalent_of_stationary (((), ()), ()) ((((), ()), ()), (), ()) (fun x => rfl) (fun x => rfl) fun iv => id (id (id (id (id (funext fun j => Eq.mpr (id (congr (congrArg Eq (Eq.trans (Fin.append_eval (fun k => iv (Fin.cast rfl (Fin.cast (Eq.symm (Nat.add_assoc X Y Z)) (Fin.natAdd X k)))) (fun k => iv (Fin.cast rfl (Fin.cast (Eq.symm (Nat.add_assoc X Y Z)) (Fin.castAdd (Y + Z) k)))) (Fin.cast rfl (Fin.cast (Eq.symm (Nat.add_assoc Y Z X)) j))) (dite_congr (Eq.refl (↑j < Y + Z)) (fun h => Eq.refl (iv (Fin.cast rfl (Fin.cast (Eq.symm (Nat.add_assoc X Y Z)) (Fin.natAdd X ⟨↑j, id (Eq.refl ↑j) ▸ Eq.mpr_prop (Eq.refl (↑j < Y + Z)) h⟩))))) fun h => Eq.refl (iv (Fin.cast rfl (Fin.cast (Eq.symm (Nat.add_assoc X Y Z)) (Fin.castAdd (Y + Z) ⟨↑j - (Y + Z), id (Eq.refl (↑j - (Y + Z))) ▸ Decidable.byContradiction fun a => Fin.append_eval._proof_1 (Fin.cast rfl (Fin.cast (Eq.symm (Nat.add_assoc Y Z X)) j)) (Eq.mpr_not (Eq.refl (↑j < Y + Z)) h) a⟩))))))) (Eq.trans (Eq.trans (congrFun' (congr (congrArg Fin.append (funext fun k => Eq.trans (Fin.append_eval (Fin.append (fun k => iv (Fin.castAdd Z (Fin.natAdd X k))) fun k => iv (Fin.castAdd Z (Fin.castAdd Y k))) (fun k => iv (Fin.natAdd (X + Y) k)) (Fin.cast rfl (Fin.cast (Eq.symm (Nat.add_assoc Y X Z)) (Fin.castAdd (X + Z) k)))) (dite_congr (Eq.refl (↑k < Y + X)) (fun h => Eq.trans (Fin.append_eval (fun k => iv (Fin.castAdd Z (Fin.natAdd X k))) (fun k => iv (Fin.castAdd Z (Fin.castAdd Y k))) ⟨↑k, id (Eq.refl ↑k) ▸ Eq.mpr_prop (Eq.refl (↑k < Y + X)) h⟩) (dite_congr (Eq.refl (↑k < Y)) (fun h_1 => Eq.refl (iv (Fin.castAdd Z (Fin.natAdd X ⟨↑k, Eq.mpr_prop (Eq.refl (↑k < Y)) h_1⟩)))) fun h_1 => Eq.refl (iv (Fin.castAdd Z (Fin.castAdd Y ⟨↑k - Y, Decidable.byContradiction fun a => Fin.append_eval._proof_1 ⟨↑k, id (Eq.refl ↑k) ▸ Eq.mpr_prop (Eq.refl (↑k < Y + X)) h⟩ (Eq.mpr_not (Eq.refl (↑k < Y)) h_1) a⟩))))) fun h => Eq.refl (iv (Fin.natAdd (X + Y) ⟨↑k - (Y + X), id (Eq.refl (↑k - (Y + X))) ▸ Decidable.byContradiction fun a => Fin.append_eval._proof_1 (Fin.cast rfl (Fin.cast (Eq.symm (Nat.add_assoc Y X Z)) (Fin.castAdd (X + Z) k))) (Eq.mpr_not (Eq.refl (↑k < Y + X)) h) a⟩))))) (congr (congrArg Fin.append (funext fun k => Eq.trans (Fin.append_eval (Fin.append (fun k => iv (Fin.castAdd Z (Fin.natAdd X k))) fun k => iv (Fin.castAdd Z (Fin.castAdd Y k))) (fun k => iv (Fin.natAdd (X + Y) k)) (Fin.cast rfl (Fin.cast (Eq.symm (Nat.add_assoc Y X Z)) (Fin.natAdd Y (Fin.natAdd X k))))) (dite_congr (Eq.refl (Y + (X + ↑k) < Y + X)) (fun h => Eq.trans (Fin.append_eval (fun k => iv (Fin.castAdd Z (Fin.natAdd X k))) (fun k => iv (Fin.castAdd Z (Fin.castAdd Y k))) ⟨Y + (X + ↑k), id (Eq.refl (Y + (X + ↑k))) ▸ Eq.mpr_prop (Eq.refl (Y + (X + ↑k) < Y + X)) h⟩) (dite_congr (Eq.refl (Y + (X + ↑k) < Y)) (fun h_1 => Eq.refl (iv (Fin.castAdd Z (Fin.natAdd X ⟨Y + (X + ↑k), Eq.mpr_prop (Eq.refl (Y + (X + ↑k) < Y)) h_1⟩)))) fun h_1 => Eq.refl (iv (Fin.castAdd Z (Fin.castAdd Y ⟨Y + (X + ↑k) - Y, Decidable.byContradiction fun a => Fin.append_eval._proof_1 ⟨Y + (X + ↑k), id (Eq.refl (Y + (X + ↑k))) ▸ Eq.mpr_prop (Eq.refl (Y + (X + ↑k) < Y + X)) h⟩ (Eq.mpr_not (Eq.refl (Y + (X + ↑k) < Y)) h_1) a⟩))))) fun h => Eq.refl (iv (Fin.natAdd (X + Y) ⟨Y + (X + ↑k) - (Y + X), id (Eq.refl (Y + (X + ↑k) - (Y + X))) ▸ Decidable.byContradiction fun a => Fin.append_eval._proof_1 (Fin.cast rfl (Fin.cast (Eq.symm (Nat.add_assoc Y X Z)) (Fin.natAdd Y (Fin.natAdd X k)))) (Eq.mpr_not (Eq.refl (Y + (X + ↑k) < Y + X)) h) a⟩))))) (funext fun k => Eq.trans (Fin.append_eval (Fin.append (fun k => iv (Fin.castAdd Z (Fin.natAdd X k))) fun k => iv (Fin.castAdd Z (Fin.castAdd Y k))) (fun k => iv (Fin.natAdd (X + Y) k)) (Fin.cast rfl (Fin.cast (Eq.symm (Nat.add_assoc Y X Z)) (Fin.natAdd Y (Fin.castAdd Z k))))) (dite_congr (Eq.refl (Y + ↑k < Y + X)) (fun h => Eq.trans (Fin.append_eval (fun k => iv (Fin.castAdd Z (Fin.natAdd X k))) (fun k => iv (Fin.castAdd Z (Fin.castAdd Y k))) ⟨Y + ↑k, id (Eq.refl (Y + ↑k)) ▸ Eq.mpr_prop (Eq.refl (Y + ↑k < Y + X)) h⟩) (dite_congr (Eq.refl (Y + ↑k < Y)) (fun h_1 => Eq.refl (iv (Fin.castAdd Z (Fin.natAdd X ⟨Y + ↑k, Eq.mpr_prop (Eq.refl (Y + ↑k < Y)) h_1⟩)))) fun h_1 => Eq.refl (iv (Fin.castAdd Z (Fin.castAdd Y ⟨Y + ↑k - Y, Decidable.byContradiction fun a => Fin.append_eval._proof_1 ⟨Y + ↑k, id (Eq.refl (Y + ↑k)) ▸ Eq.mpr_prop (Eq.refl (Y + ↑k < Y + X)) h⟩ (Eq.mpr_not (Eq.refl (Y + ↑k < Y)) h_1) a⟩))))) fun h => Eq.refl (iv (Fin.natAdd (X + Y) ⟨Y + ↑k - (Y + X), id (Eq.refl (Y + ↑k - (Y + X))) ▸ Decidable.byContradiction fun a => Fin.append_eval._proof_1 (Fin.cast rfl (Fin.cast (Eq.symm (Nat.add_assoc Y X Z)) (Fin.natAdd Y (Fin.castAdd Z k)))) (Eq.mpr_not (Eq.refl (Y + ↑k < Y + X)) h) a⟩)))))) j) (Fin.append_eval (fun k => if h : ↑k < Y + X then if h_1 : ↑k < Y then iv (Fin.castAdd Z (Fin.natAdd X ⟨↑k, Eq.mpr_prop (Eq.refl (↑k < Y)) h_1⟩)) else iv (Fin.castAdd Z (Fin.castAdd Y ⟨↑k - Y, Decidable.byContradiction fun a => Fin.append_eval._proof_1 ⟨↑k, id (Eq.refl ↑k) ▸ Eq.mpr_prop (Eq.refl (↑k < Y + X)) h⟩ (Eq.mpr_not (Eq.refl (↑k < Y)) h_1) a⟩)) else iv (Fin.natAdd (X + Y) ⟨↑k - (Y + X), id (Eq.refl (↑k - (Y + X))) ▸ Decidable.byContradiction fun a => Fin.append_eval._proof_1 (Fin.cast rfl (Fin.cast (Eq.symm (Nat.add_assoc Y X Z)) (Fin.castAdd (X + Z) k))) (Eq.mpr_not (Eq.refl (↑k < Y + X)) h) a⟩)) (Fin.append (fun k => if h : Y + (X + ↑k) < Y + X then if h_1 : Y + (X + ↑k) < Y then iv (Fin.castAdd Z (Fin.natAdd X ⟨Y + (X + ↑k), Eq.mpr_prop (Eq.refl (Y + (X + ↑k) < Y)) h_1⟩)) else iv (Fin.castAdd Z (Fin.castAdd Y ⟨Y + (X + ↑k) - Y, Decidable.byContradiction fun a => Fin.append_eval._proof_1 ⟨Y + (X + ↑k), id (Eq.refl (Y + (X + ↑k))) ▸ Eq.mpr_prop (Eq.refl (Y + (X + ↑k) < Y + X)) h⟩ (Eq.mpr_not (Eq.refl (Y + (X + ↑k) < Y)) h_1) a⟩)) else iv (Fin.natAdd (X + Y) ⟨Y + (X + ↑k) - (Y + X), id (Eq.refl (Y + (X + ↑k) - (Y + X))) ▸ Decidable.byContradiction fun a => Fin.append_eval._proof_1 (Fin.cast rfl (Fin.cast (Eq.symm (Nat.add_assoc Y X Z)) (Fin.natAdd Y (Fin.natAdd X k)))) (Eq.mpr_not (Eq.refl (Y + (X + ↑k) < Y + X)) h) a⟩)) fun k => if h : Y + ↑k < Y + X then if h_1 : Y + ↑k < Y then iv (Fin.castAdd Z (Fin.natAdd X ⟨Y + ↑k, Eq.mpr_prop (Eq.refl (Y + ↑k < Y)) h_1⟩)) else iv (Fin.castAdd Z (Fin.castAdd Y ⟨Y + ↑k - Y, Decidable.byContradiction fun a => Fin.append_eval._proof_1 ⟨Y + ↑k, id (Eq.refl (Y + ↑k)) ▸ Eq.mpr_prop (Eq.refl (Y + ↑k < Y + X)) h⟩ (Eq.mpr_not (Eq.refl (Y + ↑k < Y)) h_1) a⟩)) else iv (Fin.natAdd (X + Y) ⟨Y + ↑k - (Y + X), id (Eq.refl (Y + ↑k - (Y + X))) ▸ Decidable.byContradiction fun a => Fin.append_eval._proof_1 (Fin.cast rfl (Fin.cast (Eq.symm (Nat.add_assoc Y X Z)) (Fin.natAdd Y (Fin.castAdd Z k)))) (Eq.mpr_not (Eq.refl (Y + ↑k < Y + X)) h) a⟩)) j)) (dite_congr (Eq.refl (↑j < Y)) (fun h => dite_congr (Eq.refl (↑j < Y + X)) (fun h_1 => dite_congr (Eq.refl (↑j < Y)) (fun h_2 => Eq.refl (iv (Fin.castAdd Z (Fin.natAdd X ⟨↑j, Eq.mpr_prop (Eq.refl (↑⟨↑j, Eq.mpr_prop (Eq.refl (↑j < Y)) h⟩ < Y)) (Eq.mpr_prop (Eq.refl (↑j < Y)) h_2)⟩)))) fun h_2 => Eq.refl (iv (Fin.castAdd Z (Fin.castAdd Y ⟨↑j - Y, Decidable.byContradiction fun a => Fin.append_eval._proof_1 ⟨↑⟨↑j, Eq.mpr_prop (Eq.refl (↑j < Y)) h⟩, id (Eq.refl ↑⟨↑j, Eq.mpr_prop (Eq.refl (↑j < Y)) h⟩) ▸ Eq.mpr_prop (Eq.refl (↑⟨↑j, Eq.mpr_prop (Eq.refl (↑j < Y)) h⟩ < Y + X)) (Eq.mpr_prop (Eq.refl (↑j < Y + X)) h_1)⟩ (Eq.mpr_not (Eq.refl (↑⟨↑j, Eq.mpr_prop (Eq.refl (↑j < Y)) h⟩ < Y)) (Eq.mpr_not (Eq.refl (↑j < Y)) h_2)) a⟩)))) fun h_1 => Eq.refl (iv (Fin.natAdd (X + Y) ⟨↑j - (Y + X), id (Eq.refl (↑⟨↑j, Eq.mpr_prop (Eq.refl (↑j < Y)) h⟩ - (Y + X))) ▸ Decidable.byContradiction fun a => Fin.append_eval._proof_1 (Fin.cast rfl (Fin.cast (Eq.symm (Nat.add_assoc Y X Z)) (Fin.castAdd (X + Z) ⟨↑j, Eq.mpr_prop (Eq.refl (↑j < Y)) h⟩))) (Eq.mpr_not (Eq.refl (↑⟨↑j, Eq.mpr_prop (Eq.refl (↑j < Y)) h⟩ < Y + X)) (Eq.mpr_not (Eq.refl (↑j < Y + X)) h_1)) a⟩))) fun h => Eq.trans (Fin.append_eval (fun k => if h : Y + (X + ↑k) < Y + X then if h_1 : Y + (X + ↑k) < Y then iv (Fin.castAdd Z (Fin.natAdd X ⟨Y + (X + ↑k), Eq.mpr_prop (Eq.refl (Y + (X + ↑k) < Y)) h_1⟩)) else iv (Fin.castAdd Z (Fin.castAdd Y ⟨Y + (X + ↑k) - Y, Decidable.byContradiction fun a => Fin.append_eval._proof_1 ⟨Y + (X + ↑k), id (Eq.refl (Y + (X + ↑k))) ▸ Eq.mpr_prop (Eq.refl (Y + (X + ↑k) < Y + X)) h⟩ (Eq.mpr_not (Eq.refl (Y + (X + ↑k) < Y)) h_1) a⟩)) else iv (Fin.natAdd (X + Y) ⟨Y + (X + ↑k) - (Y + X), id (Eq.refl (Y + (X + ↑k) - (Y + X))) ▸ Decidable.byContradiction fun a => Fin.append_eval._proof_1 (Fin.cast rfl (Fin.cast (Eq.symm (Nat.add_assoc Y X Z)) (Fin.natAdd Y (Fin.natAdd X k)))) (Eq.mpr_not (Eq.refl (Y + (X + ↑k) < Y + X)) h) a⟩)) (fun k => if h : Y + ↑k < Y + X then if h_1 : Y + ↑k < Y then iv (Fin.castAdd Z (Fin.natAdd X ⟨Y + ↑k, Eq.mpr_prop (Eq.refl (Y + ↑k < Y)) h_1⟩)) else iv (Fin.castAdd Z (Fin.castAdd Y ⟨Y + ↑k - Y, Decidable.byContradiction fun a => Fin.append_eval._proof_1 ⟨Y + ↑k, id (Eq.refl (Y + ↑k)) ▸ Eq.mpr_prop (Eq.refl (Y + ↑k < Y + X)) h⟩ (Eq.mpr_not (Eq.refl (Y + ↑k < Y)) h_1) a⟩)) else iv (Fin.natAdd (X + Y) ⟨Y + ↑k - (Y + X), id (Eq.refl (Y + ↑k - (Y + X))) ▸ Decidable.byContradiction fun a => Fin.append_eval._proof_1 (Fin.cast rfl (Fin.cast (Eq.symm (Nat.add_assoc Y X Z)) (Fin.natAdd Y (Fin.castAdd Z k)))) (Eq.mpr_not (Eq.refl (Y + ↑k < Y + X)) h) a⟩)) ⟨↑j - Y, Decidable.byContradiction fun a => Fin.append_eval._proof_1 j (Eq.mpr_not (Eq.refl (↑j < Y)) h) a⟩) (dite_congr (Eq.refl (↑j - Y < Z)) (fun h_1 => dite_congr (Eq.refl (Y + (X + (↑j - Y)) < Y + X)) (fun h_2 => dite_congr (Eq.refl (Y + (X + (↑j - Y)) < Y)) (fun h_3 => Eq.refl (iv (Fin.castAdd Z (Fin.natAdd X ⟨Y + (X + (↑j - Y)), Eq.mpr_prop (Eq.refl (Y + (X + ↑⟨↑⟨↑j - Y, Decidable.byContradiction fun a => Fin.append_eval._proof_1 j (Eq.mpr_not (Eq.refl (↑j < Y)) h) a⟩, Eq.mpr_prop (Eq.refl (↑j - Y < Z)) h_1⟩) < Y)) (Eq.mpr_prop (Eq.refl (Y + (X + (↑j - Y)) < Y)) h_3)⟩)))) fun h_3 => Eq.refl (iv (Fin.castAdd Z (Fin.castAdd Y ⟨Y + (X + (↑j - Y)) - Y, Decidable.byContradiction fun a => Fin.append_eval._proof_1 ⟨Y + (X + ↑⟨↑⟨↑j - Y, Decidable.byContradiction fun a => Fin.append_eval._proof_1 j (Eq.mpr_not (Eq.refl (↑j < Y)) h) a⟩, Eq.mpr_prop (Eq.refl (↑j - Y < Z)) h_1⟩), id (Eq.refl (Y + (X + ↑⟨↑⟨↑j - Y, Decidable.byContradiction fun a => Fin.append_eval._proof_1 j (Eq.mpr_not (Eq.refl (↑j < Y)) h) a⟩, Eq.mpr_prop (Eq.refl (↑j - Y < Z)) h_1⟩))) ▸ Eq.mpr_prop (Eq.refl (Y + (X + ↑⟨↑⟨↑j - Y, Decidable.byContradiction fun a => Fin.append_eval._proof_1 j (Eq.mpr_not (Eq.refl (↑j < Y)) h) a⟩, Eq.mpr_prop (Eq.refl (↑j - Y < Z)) h_1⟩) < Y + X)) (Eq.mpr_prop (Eq.refl (Y + (X + (↑j - Y)) < Y + X)) h_2)⟩ (Eq.mpr_not (Eq.refl (Y + (X + ↑⟨↑⟨↑j - Y, Decidable.byContradiction fun a => Fin.append_eval._proof_1 j (Eq.mpr_not (Eq.refl (↑j < Y)) h) a⟩, Eq.mpr_prop (Eq.refl (↑j - Y < Z)) h_1⟩) < Y)) (Eq.mpr_not (Eq.refl (Y + (X + (↑j - Y)) < Y)) h_3)) a⟩)))) fun h_2 => Eq.refl (iv (Fin.natAdd (X + Y) ⟨Y + (X + (↑j - Y)) - (Y + X), id (Eq.refl (Y + (X + ↑⟨↑⟨↑j - Y, Decidable.byContradiction fun a => Fin.append_eval._proof_1 j (Eq.mpr_not (Eq.refl (↑j < Y)) h) a⟩, Eq.mpr_prop (Eq.refl (↑j - Y < Z)) h_1⟩) - (Y + X))) ▸ Decidable.byContradiction fun a => Fin.append_eval._proof_1 (Fin.cast rfl (Fin.cast (Eq.symm (Nat.add_assoc Y X Z)) (Fin.natAdd Y (Fin.natAdd X ⟨↑⟨↑j - Y, Decidable.byContradiction fun a => Fin.append_eval._proof_1 j (Eq.mpr_not (Eq.refl (↑j < Y)) h) a⟩, Eq.mpr_prop (Eq.refl (↑j - Y < Z)) h_1⟩)))) (Eq.mpr_not (Eq.refl (Y + (X + ↑⟨↑⟨↑j - Y, Decidable.byContradiction fun a => Fin.append_eval._proof_1 j (Eq.mpr_not (Eq.refl (↑j < Y)) h) a⟩, Eq.mpr_prop (Eq.refl (↑j - Y < Z)) h_1⟩) < Y + X)) (Eq.mpr_not (Eq.refl (Y + (X + (↑j - Y)) < Y + X)) h_2)) a⟩))) fun h_1 => dite_congr (Eq.refl (Y + (↑j - Y - Z) < Y + X)) (fun h_2 => dite_congr (Eq.refl (Y + (↑j - Y - Z) < Y)) (fun h_3 => Eq.refl (iv (Fin.castAdd Z (Fin.natAdd X ⟨Y + (↑j - Y - Z), Eq.mpr_prop (Eq.refl (Y + ↑⟨↑⟨↑j - Y, Decidable.byContradiction fun a => Fin.append_eval._proof_1 j (Eq.mpr_not (Eq.refl (↑j < Y)) h) a⟩ - Z, Decidable.byContradiction fun a => Fin.append_eval._proof_1 ⟨↑j - Y, Decidable.byContradiction fun a => Fin.append_eval._proof_1 j (Eq.mpr_not (Eq.refl (↑j < Y)) h) a⟩ (Eq.mpr_not (Eq.refl (↑j - Y < Z)) h_1) a⟩ < Y)) (Eq.mpr_prop (Eq.refl (Y + (↑j - Y - Z) < Y)) h_3)⟩)))) fun h_3 => Eq.refl (iv (Fin.castAdd Z (Fin.castAdd Y ⟨Y + (↑j - Y - Z) - Y, Decidable.byContradiction fun a => Fin.append_eval._proof_1 ⟨Y + ↑⟨↑⟨↑j - Y, Decidable.byContradiction fun a => Fin.append_eval._proof_1 j (Eq.mpr_not (Eq.refl (↑j < Y)) h) a⟩ - Z, Decidable.byContradiction fun a => Fin.append_eval._proof_1 ⟨↑j - Y, Decidable.byContradiction fun a => Fin.append_eval._proof_1 j (Eq.mpr_not (Eq.refl (↑j < Y)) h) a⟩ (Eq.mpr_not (Eq.refl (↑j - Y < Z)) h_1) a⟩, id (Eq.refl (Y + ↑⟨↑⟨↑j - Y, Decidable.byContradiction fun a => Fin.append_eval._proof_1 j (Eq.mpr_not (Eq.refl (↑j < Y)) h) a⟩ - Z, Decidable.byContradiction fun a => Fin.append_eval._proof_1 ⟨↑j - Y, Decidable.byContradiction fun a => Fin.append_eval._proof_1 j (Eq.mpr_not (Eq.refl (↑j < Y)) h) a⟩ (Eq.mpr_not (Eq.refl (↑j - Y < Z)) h_1) a⟩)) ▸ Eq.mpr_prop (Eq.refl (Y + ↑⟨↑⟨↑j - Y, Decidable.byContradiction fun a => Fin.append_eval._proof_1 j (Eq.mpr_not (Eq.refl (↑j < Y)) h) a⟩ - Z, Decidable.byContradiction fun a => Fin.append_eval._proof_1 ⟨↑j - Y, Decidable.byContradiction fun a => Fin.append_eval._proof_1 j (Eq.mpr_not (Eq.refl (↑j < Y)) h) a⟩ (Eq.mpr_not (Eq.refl (↑j - Y < Z)) h_1) a⟩ < Y + X)) (Eq.mpr_prop (Eq.refl (Y + (↑j - Y - Z) < Y + X)) h_2)⟩ (Eq.mpr_not (Eq.refl (Y + ↑⟨↑⟨↑j - Y, Decidable.byContradiction fun a => Fin.append_eval._proof_1 j (Eq.mpr_not (Eq.refl (↑j < Y)) h) a⟩ - Z, Decidable.byContradiction fun a => Fin.append_eval._proof_1 ⟨↑j - Y, Decidable.byContradiction fun a => Fin.append_eval._proof_1 j (Eq.mpr_not (Eq.refl (↑j < Y)) h) a⟩ (Eq.mpr_not (Eq.refl (↑j - Y < Z)) h_1) a⟩ < Y)) (Eq.mpr_not (Eq.refl (Y + (↑j - Y - Z) < Y)) h_3)) a⟩)))) fun h_2 => Eq.refl (iv (Fin.natAdd (X + Y) ⟨Y + (↑j - Y - Z) - (Y + X), id (Eq.refl (Y + ↑⟨↑⟨↑j - Y, Decidable.byContradiction fun a => Fin.append_eval._proof_1 j (Eq.mpr_not (Eq.refl (↑j < Y)) h) a⟩ - Z, Decidable.byContradiction fun a => Fin.append_eval._proof_1 ⟨↑j - Y, Decidable.byContradiction fun a => Fin.append_eval._proof_1 j (Eq.mpr_not (Eq.refl (↑j < Y)) h) a⟩ (Eq.mpr_not (Eq.refl (↑j - Y < Z)) h_1) a⟩ - (Y + X))) ▸ Decidable.byContradiction fun a => Fin.append_eval._proof_1 (Fin.cast rfl (Fin.cast (Eq.symm (Nat.add_assoc Y X Z)) (Fin.natAdd Y (Fin.castAdd Z ⟨↑⟨↑j - Y, Decidable.byContradiction fun a => Fin.append_eval._proof_1 j (Eq.mpr_not (Eq.refl (↑j < Y)) h) a⟩ - Z, Decidable.byContradiction fun a => Fin.append_eval._proof_1 ⟨↑j - Y, Decidable.byContradiction fun a => Fin.append_eval._proof_1 j (Eq.mpr_not (Eq.refl (↑j < Y)) h) a⟩ (Eq.mpr_not (Eq.refl (↑j - Y < Z)) h_1) a⟩)))) (Eq.mpr_not (Eq.refl (Y + ↑⟨↑⟨↑j - Y, Decidable.byContradiction fun a => Fin.append_eval._proof_1 j (Eq.mpr_not (Eq.refl (↑j < Y)) h) a⟩ - Z, Decidable.byContradiction fun a => Fin.append_eval._proof_1 ⟨↑j - Y, Decidable.byContradiction fun a => Fin.append_eval._proof_1 j (Eq.mpr_not (Eq.refl (↑j < Y)) h) a⟩ (Eq.mpr_not (Eq.refl (↑j - Y < Z)) h_1) a⟩ < Y + X)) (Eq.mpr_not (Eq.refl (Y + (↑j - Y - Z) < Y + X)) h_2)) a⟩))))))) (if h : ↑j < Y + Z then Eq.mpr (id (congr (congrArg Eq (dif_pos h)) (dite_congr (Eq.refl (↑j < Y)) (fun h => dite_congr (Eq.refl (↑j < Y + X)) (fun h_1 => dif_pos h) fun h_1 => Eq.refl (iv (Fin.natAdd (X + Y) ⟨↑j - (Y + X), id (Eq.refl (↑⟨↑j, Eq.mpr_prop (Eq.refl (↑j < Y)) (Eq.mpr_prop (Eq.refl (↑j < Y)) h)⟩ - (Y + X))) ▸ Decidable.byContradiction fun a => Fin.append_eval._proof_1 (Fin.cast rfl (Fin.cast (Eq.symm (Nat.add_assoc Y X Z)) (Fin.castAdd (X + Z) ⟨↑j, Eq.mpr_prop (Eq.refl (↑j < Y)) (Eq.mpr_prop (Eq.refl (↑j < Y)) h)⟩))) (Eq.mpr_not (Eq.refl (↑⟨↑j, Eq.mpr_prop (Eq.refl (↑j < Y)) (Eq.mpr_prop (Eq.refl (↑j < Y)) h)⟩ < Y + X)) (Eq.mpr_not (Eq.refl (↑j < Y + X)) (Eq.mpr_not (Eq.refl (↑j < Y + X)) h_1))) a⟩))) fun h => Eq.refl (if h_1 : ↑j - Y < Z then if h_2 : Y + (X + (↑j - Y)) < Y + X then if h_3 : Y + (X + (↑j - Y)) < Y then iv (Fin.castAdd Z (Fin.natAdd X ⟨Y + (X + (↑j - Y)), Eq.mpr_prop (Eq.refl (Y + (X + ↑⟨↑⟨↑j - Y, Decidable.byContradiction fun a => Fin.append_eval._proof_1 j (Eq.mpr_not (Eq.refl (↑j < Y)) (Eq.mpr_not (Eq.refl (↑j < Y)) h)) a⟩, Eq.mpr_prop (Eq.refl (↑j - Y < Z)) h_1⟩) < Y)) (Eq.mpr_prop (Eq.refl (Y + (X + (↑j - Y)) < Y)) h_3)⟩)) else iv (Fin.castAdd Z (Fin.castAdd Y ⟨Y + (X + (↑j - Y)) - Y, Decidable.byContradiction fun a => Fin.append_eval._proof_1 ⟨Y + (X + ↑⟨↑⟨↑j - Y, Decidable.byContradiction fun a => Fin.append_eval._proof_1 j (Eq.mpr_not (Eq.refl (↑j < Y)) (Eq.mpr_not (Eq.refl (↑j < Y)) h)) a⟩, Eq.mpr_prop (Eq.refl (↑j - Y < Z)) h_1⟩), id (Eq.refl (Y + (X + ↑⟨↑⟨↑j - Y, Decidable.byContradiction fun a => Fin.append_eval._proof_1 j (Eq.mpr_not (Eq.refl (↑j < Y)) (Eq.mpr_not (Eq.refl (↑j < Y)) h)) a⟩, Eq.mpr_prop (Eq.refl (↑j - Y < Z)) h_1⟩))) ▸ Eq.mpr_prop (Eq.refl (Y + (X + ↑⟨↑⟨↑j - Y, Decidable.byContradiction fun a => Fin.append_eval._proof_1 j (Eq.mpr_not (Eq.refl (↑j < Y)) (Eq.mpr_not (Eq.refl (↑j < Y)) h)) a⟩, Eq.mpr_prop (Eq.refl (↑j - Y < Z)) h_1⟩) < Y + X)) (Eq.mpr_prop (Eq.refl (Y + (X + (↑j - Y)) < Y + X)) h_2)⟩ (Eq.mpr_not (Eq.refl (Y + (X + ↑⟨↑⟨↑j - Y, Decidable.byContradiction fun a => Fin.append_eval._proof_1 j (Eq.mpr_not (Eq.refl (↑j < Y)) (Eq.mpr_not (Eq.refl (↑j < Y)) h)) a⟩, Eq.mpr_prop (Eq.refl (↑j - Y < Z)) h_1⟩) < Y)) (Eq.mpr_not (Eq.refl (Y + (X + (↑j - Y)) < Y)) h_3)) a⟩)) else iv (Fin.natAdd (X + Y) ⟨Y + (X + (↑j - Y)) - (Y + X), id (Eq.refl (Y + (X + ↑⟨↑⟨↑j - Y, Decidable.byContradiction fun a => Fin.append_eval._proof_1 j (Eq.mpr_not (Eq.refl (↑j < Y)) (Eq.mpr_not (Eq.refl (↑j < Y)) h)) a⟩, Eq.mpr_prop (Eq.refl (↑j - Y < Z)) h_1⟩) - (Y + X))) ▸ Decidable.byContradiction fun a => Fin.append_eval._proof_1 (Fin.cast rfl (Fin.cast (Eq.symm (Nat.add_assoc Y X Z)) (Fin.natAdd Y (Fin.natAdd X ⟨↑⟨↑j - Y, Decidable.byContradiction fun a => Fin.append_eval._proof_1 j (Eq.mpr_not (Eq.refl (↑j < Y)) (Eq.mpr_not (Eq.refl (↑j < Y)) h)) a⟩, Eq.mpr_prop (Eq.refl (↑j - Y < Z)) h_1⟩)))) (Eq.mpr_not (Eq.refl (Y + (X + ↑⟨↑⟨↑j - Y, Decidable.byContradiction fun a => Fin.append_eval._proof_1 j (Eq.mpr_not (Eq.refl (↑j < Y)) (Eq.mpr_not (Eq.refl (↑j < Y)) h)) a⟩, Eq.mpr_prop (Eq.refl (↑j - Y < Z)) h_1⟩) < Y + X)) (Eq.mpr_not (Eq.refl (Y + (X + (↑j - Y)) < Y + X)) h_2)) a⟩) else if h_2 : Y + (↑j - Y - Z) < Y + X then if h_3 : Y + (↑j - Y - Z) < Y then iv (Fin.castAdd Z (Fin.natAdd X ⟨Y + (↑j - Y - Z), Eq.mpr_prop (Eq.refl (Y + ↑⟨↑⟨↑j - Y, Decidable.byContradiction fun a => Fin.append_eval._proof_1 j (Eq.mpr_not (Eq.refl (↑j < Y)) (Eq.mpr_not (Eq.refl (↑j < Y)) h)) a⟩ - Z, Decidable.byContradiction fun a => Fin.append_eval._proof_1 ⟨↑j - Y, Decidable.byContradiction fun a => Fin.append_eval._proof_1 j (Eq.mpr_not (Eq.refl (↑j < Y)) (Eq.mpr_not (Eq.refl (↑j < Y)) h)) a⟩ (Eq.mpr_not (Eq.refl (↑j - Y < Z)) h_1) a⟩ < Y)) (Eq.mpr_prop (Eq.refl (Y + (↑j - Y - Z) < Y)) h_3)⟩)) else iv (Fin.castAdd Z (Fin.castAdd Y ⟨Y + (↑j - Y - Z) - Y, Decidable.byContradiction fun a => Fin.append_eval._proof_1 ⟨Y + ↑⟨↑⟨↑j - Y, Decidable.byContradiction fun a => Fin.append_eval._proof_1 j (Eq.mpr_not (Eq.refl (↑j < Y)) (Eq.mpr_not (Eq.refl (↑j < Y)) h)) a⟩ - Z, Decidable.byContradiction fun a => Fin.append_eval._proof_1 ⟨↑j - Y, Decidable.byContradiction fun a => Fin.append_eval._proof_1 j (Eq.mpr_not (Eq.refl (↑j < Y)) (Eq.mpr_not (Eq.refl (↑j < Y)) h)) a⟩ (Eq.mpr_not (Eq.refl (↑j - Y < Z)) h_1) a⟩, id (Eq.refl (Y + ↑⟨↑⟨↑j - Y, Decidable.byContradiction fun a => Fin.append_eval._proof_1 j (Eq.mpr_not (Eq.refl (↑j < Y)) (Eq.mpr_not (Eq.refl (↑j < Y)) h)) a⟩ - Z, Decidable.byContradiction fun a => Fin.append_eval._proof_1 ⟨↑j - Y, Decidable.byContradiction fun a => Fin.append_eval._proof_1 j (Eq.mpr_not (Eq.refl (↑j < Y)) (Eq.mpr_not (Eq.refl (↑j < Y)) h)) a⟩ (Eq.mpr_not (Eq.refl (↑j - Y < Z)) h_1) a⟩)) ▸ Eq.mpr_prop (Eq.refl (Y + ↑⟨↑⟨↑j - Y, Decidable.byContradiction fun a => Fin.append_eval._proof_1 j (Eq.mpr_not (Eq.refl (↑j < Y)) (Eq.mpr_not (Eq.refl (↑j < Y)) h)) a⟩ - Z, Decidable.byContradiction fun a => Fin.append_eval._proof_1 ⟨↑j - Y, Decidable.byContradiction fun a => Fin.append_eval._proof_1 j (Eq.mpr_not (Eq.refl (↑j < Y)) (Eq.mpr_not (Eq.refl (↑j < Y)) h)) a⟩ (Eq.mpr_not (Eq.refl (↑j - Y < Z)) h_1) a⟩ < Y + X)) (Eq.mpr_prop (Eq.refl (Y + (↑j - Y - Z) < Y + X)) h_2)⟩ (Eq.mpr_not (Eq.refl (Y + ↑⟨↑⟨↑j - Y, Decidable.byContradiction fun a => Fin.append_eval._proof_1 j (Eq.mpr_not (Eq.refl (↑j < Y)) (Eq.mpr_not (Eq.refl (↑j < Y)) h)) a⟩ - Z, Decidable.byContradiction fun a => Fin.append_eval._proof_1 ⟨↑j - Y, Decidable.byContradiction fun a => Fin.append_eval._proof_1 j (Eq.mpr_not (Eq.refl (↑j < Y)) (Eq.mpr_not (Eq.refl (↑j < Y)) h)) a⟩ (Eq.mpr_not (Eq.refl (↑j - Y < Z)) h_1) a⟩ < Y)) (Eq.mpr_not (Eq.refl (Y + (↑j - Y - Z) < Y)) h_3)) a⟩)) else iv (Fin.natAdd (X + Y) ⟨Y + (↑j - Y - Z) - (Y + X), id (Eq.refl (Y + ↑⟨↑⟨↑j - Y, Decidable.byContradiction fun a => Fin.append_eval._proof_1 j (Eq.mpr_not (Eq.refl (↑j < Y)) (Eq.mpr_not (Eq.refl (↑j < Y)) h)) a⟩ - Z, Decidable.byContradiction fun a => Fin.append_eval._proof_1 ⟨↑j - Y, Decidable.byContradiction fun a => Fin.append_eval._proof_1 j (Eq.mpr_not (Eq.refl (↑j < Y)) (Eq.mpr_not (Eq.refl (↑j < Y)) h)) a⟩ (Eq.mpr_not (Eq.refl (↑j - Y < Z)) h_1) a⟩ - (Y + X))) ▸ Decidable.byContradiction fun a => Fin.append_eval._proof_1 (Fin.cast rfl (Fin.cast (Eq.symm (Nat.add_assoc Y X Z)) (Fin.natAdd Y (Fin.castAdd Z ⟨↑⟨↑j - Y, Decidable.byContradiction fun a => Fin.append_eval._proof_1 j (Eq.mpr_not (Eq.refl (↑j < Y)) (Eq.mpr_not (Eq.refl (↑j < Y)) h)) a⟩ - Z, Decidable.byContradiction fun a => Fin.append_eval._proof_1 ⟨↑j - Y, Decidable.byContradiction fun a => Fin.append_eval._proof_1 j (Eq.mpr_not (Eq.refl (↑j < Y)) (Eq.mpr_not (Eq.refl (↑j < Y)) h)) a⟩ (Eq.mpr_not (Eq.refl (↑j - Y < Z)) h_1) a⟩)))) (Eq.mpr_not (Eq.refl (Y + ↑⟨↑⟨↑j - Y, Decidable.byContradiction fun a => Fin.append_eval._proof_1 j (Eq.mpr_not (Eq.refl (↑j < Y)) (Eq.mpr_not (Eq.refl (↑j < Y)) h)) a⟩ - Z, Decidable.byContradiction fun a => Fin.append_eval._proof_1 ⟨↑j - Y, Decidable.byContradiction fun a => Fin.append_eval._proof_1 j (Eq.mpr_not (Eq.refl (↑j < Y)) (Eq.mpr_not (Eq.refl (↑j < Y)) h)) a⟩ (Eq.mpr_not (Eq.refl (↑j - Y < Z)) h_1) a⟩ < Y + X)) (Eq.mpr_not (Eq.refl (Y + (↑j - Y - Z) < Y + X)) h_2)) a⟩))))) (if h_1 : ↑j < Y then Eq.mpr (id (congrArg (Eq (iv (Fin.cast rfl (Fin.cast (Eq.symm (Nat.add_assoc X Y Z)) (Fin.natAdd X ⟨↑j, id (Eq.refl ↑j) ▸ Eq.mpr_prop (Eq.refl (↑j < Y + Z)) h⟩))))) (dif_pos h_1))) (if h_2 : ↑j < Y + X then Eq.mpr (id (congrArg (Eq (iv (Fin.cast rfl (Fin.cast (Eq.symm (Nat.add_assoc X Y Z)) (Fin.natAdd X ⟨↑j, id (Eq.refl ↑j) ▸ Eq.mpr_prop (Eq.refl (↑j < Y + Z)) h⟩))))) (dif_pos h_2))) (Eq.refl (iv (Fin.cast rfl (Fin.cast (Eq.symm (Nat.add_assoc X Y Z)) (Fin.natAdd X ⟨↑j, id (Eq.refl ↑j) ▸ Eq.mpr_prop (Eq.refl (↑j < Y + Z)) h⟩))))) else Eq.mpr (id (congrArg (Eq (iv (Fin.cast rfl (Fin.cast (Eq.symm (Nat.add_assoc X Y Z)) (Fin.natAdd X ⟨↑j, id (Eq.refl ↑j) ▸ Eq.mpr_prop (Eq.refl (↑j < Y + Z)) h⟩))))) (dif_neg h_2))) (False.elim (Component.hexagon_forward_arrow._proof_1_1 X Y Z j h_1 h_2))) else Eq.mpr (id (congrArg (Eq (iv (Fin.cast rfl (Fin.cast (Eq.symm (Nat.add_assoc X Y Z)) (Fin.natAdd X ⟨↑j, id (Eq.refl ↑j) ▸ Eq.mpr_prop (Eq.refl (↑j < Y + Z)) h⟩))))) (dif_neg h_1))) (if h_2 : ↑j - Y < Z then Eq.mpr (id (congrArg (Eq (iv (Fin.cast rfl (Fin.cast (Eq.symm (Nat.add_assoc X Y Z)) (Fin.natAdd X ⟨↑j, id (Eq.refl ↑j) ▸ Eq.mpr_prop (Eq.refl (↑j < Y + Z)) h⟩))))) (dif_pos h_2))) (if h_3 : Y + (X + (↑j - Y)) < Y + X then Eq.mpr (id (congrArg (Eq (iv (Fin.cast rfl (Fin.cast (Eq.symm (Nat.add_assoc X Y Z)) (Fin.natAdd X ⟨↑j, id (Eq.refl ↑j) ▸ Eq.mpr_prop (Eq.refl (↑j < Y + Z)) h⟩))))) (dif_pos h_3))) (if h_4 : Y + (X + (↑j - Y)) < Y then Eq.mpr (id (congrArg (Eq (iv (Fin.cast rfl (Fin.cast (Eq.symm (Nat.add_assoc X Y Z)) (Fin.natAdd X ⟨↑j, id (Eq.refl ↑j) ▸ Eq.mpr_prop (Eq.refl (↑j < Y + Z)) h⟩))))) (dif_pos h_4))) (False.elim (Component.hexagon_forward_arrow._proof_1_2 X Y Z j h_3)) else Eq.mpr (id (congrArg (Eq (iv (Fin.cast rfl (Fin.cast (Eq.symm (Nat.add_assoc X Y Z)) (Fin.natAdd X ⟨↑j, id (Eq.refl ↑j) ▸ Eq.mpr_prop (Eq.refl (↑j < Y + Z)) h⟩))))) (dif_neg h_4))) (False.elim (Component.hexagon_forward_arrow._proof_1_2 X Y Z j h_3))) else Eq.mpr (id (congrArg (Eq (iv (Fin.cast rfl (Fin.cast (Eq.symm (Nat.add_assoc X Y Z)) (Fin.natAdd X ⟨↑j, id (Eq.refl ↑j) ▸ Eq.mpr_prop (Eq.refl (↑j < Y + Z)) h⟩))))) (dif_neg h_3))) ((fun a a_1 e_a => e_a ▸ Eq.refl (iv a)) (Fin.cast rfl (Fin.cast (Eq.symm (Nat.add_assoc X Y Z)) (Fin.natAdd X ⟨↑j, id (Eq.refl ↑j) ▸ Eq.mpr_prop (Eq.refl (↑j < Y + Z)) h⟩))) (Fin.natAdd (X + Y) ⟨Y + (X + (↑j - Y)) - (Y + X), id (Eq.refl (Y + (X + ↑⟨↑⟨↑j - Y, Decidable.byContradiction fun a => Fin.append_eval._proof_1 j (Eq.mpr_not (Eq.refl (↑j < Y)) (Eq.mpr_not (Eq.refl (↑j < Y)) h_1)) a⟩, Eq.mpr_prop (Eq.refl (↑j - Y < Z)) h_2⟩) - (Y + X))) ▸ Decidable.byContradiction fun a => Fin.append_eval._proof_1 (Fin.cast rfl (Fin.cast (Eq.symm (Nat.add_assoc Y X Z)) (Fin.natAdd Y (Fin.natAdd X ⟨↑⟨↑j - Y, Decidable.byContradiction fun a => Fin.append_eval._proof_1 j (Eq.mpr_not (Eq.refl (↑j < Y)) (Eq.mpr_not (Eq.refl (↑j < Y)) h_1)) a⟩, Eq.mpr_prop (Eq.refl (↑j - Y < Z)) h_2⟩)))) (Eq.mpr_not (Eq.refl (Y + (X + ↑⟨↑⟨↑j - Y, Decidable.byContradiction fun a => Fin.append_eval._proof_1 j (Eq.mpr_not (Eq.refl (↑j < Y)) (Eq.mpr_not (Eq.refl (↑j < Y)) h_1)) a⟩, Eq.mpr_prop (Eq.refl (↑j - Y < Z)) h_2⟩) < Y + X)) (Eq.mpr_not (Eq.refl (Y + (X + (↑j - Y)) < Y + X)) h_3)) a⟩) (Fin.ext (id (Decidable.byContradiction fun a => Component.hexagon_forward_arrow._proof_1_3 X Y Z j h_1 a))))) else Eq.mpr (id (congrArg (Eq (iv (Fin.cast rfl (Fin.cast (Eq.symm (Nat.add_assoc X Y Z)) (Fin.natAdd X ⟨↑j, id (Eq.refl ↑j) ▸ Eq.mpr_prop (Eq.refl (↑j < Y + Z)) h⟩))))) (dif_neg h_2))) (if h_3 : Y + (↑j - Y - Z) < Y + X then Eq.mpr (id (congrArg (Eq (iv (Fin.cast rfl (Fin.cast (Eq.symm (Nat.add_assoc X Y Z)) (Fin.natAdd X ⟨↑j, id (Eq.refl ↑j) ▸ Eq.mpr_prop (Eq.refl (↑j < Y + Z)) h⟩))))) (dif_pos h_3))) (if h_4 : Y + (↑j - Y - Z) < Y then Eq.mpr ⋯ ⋯ else ⋯) else ⋯))) else ⋯))))))
Complexity: 61996159 (size of the value term)
Dependencies: Component.id, Component.parallel, Component.recast, Component.sequential, Component.symmetry, InformationSystem.equivalent, instNonemptyForallFin_computerNetworks, instNormForallFin_computerNetworks, instNormProd_computerNetworks, instNormUnit_computerNetworks
Proof dependencies: Component.equivalent_of_stationary, Fin.append_eval
Mathlib dependencies: Fin.append, Norm, add_tsub_cancel_left
Lean core dependencies: And, Bool, Decidable.byContradiction, Decidable.decide, Eq, Eq.mpr, Eq.mpr_not, Eq.mpr_prop, Eq.symm, Eq.trans, False, False.elim, Fin, Fin.cast, Fin.castAdd, Fin.ext, Fin.natAdd, Function.comp, GT.gt, Int, Int.add_one_le_of_lt, Int.natCast_add, Int.natCast_nonneg, 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.combine_sat', Lean.Omega.Constraint.isImpossible, Lean.Omega.Constraint.not_sat'_of_isImpossible, Lean.Omega.Int.add_congr, Lean.Omega.Int.ofNat_le_of_le, Lean.Omega.Int.ofNat_lt_of_lt, Lean.Omega.Int.ofNat_sub_dichotomy, Lean.Omega.Int.ofNat_sub_sub, 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.coordinate_eval_3, Lean.Omega.LinearCombo.coordinate_eval_4, Lean.Omega.LinearCombo.coordinate_eval_5, Lean.Omega.LinearCombo.eval, Lean.Omega.LinearCombo.sub_eval, Lean.Omega.combo_sat', Lean.Omega.tidy_sat, Nat, Nat.add_assoc, Nat.cast, Nat.le_of_not_lt, Nat.lt_add_right, Nat.lt_or_gt_of_ne, Nonempty, Not, Or.elim, Prod, Unit, Unit.unit, congr, congrArg, congrFun', dif_neg, dif_pos, dite, dite_congr, funext, id, le_of_le_of_eq, of_decide_eq_true, rfl
Used by: Component.Hom.hexagon_forward
Component.hexagon_reverse_arrow
theorem Component.hexagon_reverse_arrow {Wire : Type} [Nonempty Wire] [Norm Wire] (X Y Z : ℕ) : InformationSystem.equivalent (((Component.recast ⋯ ⋯ (Component.id Wire (X + (Y + Z)))).sequential (Component.symmetry Wire (X + Y) Z)).sequential (Component.recast ⋯ ⋯ (Component.id Wire (Z + (X + Y))))) ((((Component.id Wire X).parallel (Component.symmetry Wire Y Z)).sequential (Component.recast ⋯ ⋯ (Component.id Wire (X + (Z + Y))))).sequential ((Component.symmetry Wire X Z).parallel (Component.id Wire Y))) (((), ()), ()) ((((), ()), ()), (), ())
Show details
fun {Wire} [⋯] [⋯] X Y Z => Component.equivalent_of_stationary (((), ()), ()) ((((), ()), ()), (), ()) (fun x => rfl) (fun x => rfl) fun iv => id (id (id (id (id (funext fun j => Eq.mpr (id (congr (congrArg Eq (Eq.trans (Fin.append_eval (fun k => iv (Fin.cast rfl (Fin.cast (Eq.symm (Eq.symm (Nat.add_assoc X Y Z))) (Fin.natAdd (X + Y) k)))) (fun k => iv (Fin.cast rfl (Fin.cast (Eq.symm (Eq.symm (Nat.add_assoc X Y Z))) (Fin.castAdd Z k)))) (Fin.cast rfl (Fin.cast (Eq.symm (Eq.symm (Nat.add_assoc Z X Y))) j))) (dite_congr (Eq.refl (↑j < Z)) (fun h => Eq.refl (iv (Fin.cast rfl (Fin.cast (Eq.symm (Eq.symm (Nat.add_assoc X Y Z))) (Fin.natAdd (X + Y) ⟨↑j, id (Eq.refl ↑j) ▸ Eq.mpr_prop (Eq.refl (↑j < Z)) h⟩))))) fun h => Eq.refl (iv (Fin.cast rfl (Fin.cast (Eq.symm (Eq.symm (Nat.add_assoc X Y Z))) (Fin.castAdd Z ⟨↑j - Z, id (Eq.refl (↑j - Z)) ▸ Decidable.byContradiction fun a => Fin.append_eval._proof_1 (Fin.cast rfl (Fin.cast (Eq.symm (Eq.symm (Nat.add_assoc Z X Y))) j)) (Eq.mpr_not (Eq.refl (↑j < Z)) h) a⟩))))))) (Eq.trans (Eq.trans (congrFun' (congr (congrArg Fin.append (congr (congrArg Fin.append (funext fun k => Eq.trans (Fin.append_eval (fun k => iv (Fin.castAdd (Y + Z) k)) (Fin.append (fun k => iv (Fin.natAdd X (Fin.natAdd Y k))) fun k => iv (Fin.natAdd X (Fin.castAdd Z k))) (Fin.cast rfl (Fin.cast (Eq.symm (Eq.symm (Nat.add_assoc X Z Y))) (Fin.castAdd Y (Fin.natAdd X k))))) (dite_congr (Eq.refl (X + ↑k < X)) (fun h => Eq.refl (iv (Fin.castAdd (Y + Z) ⟨X + ↑k, id (Eq.refl (X + ↑k)) ▸ Eq.mpr_prop (Eq.refl (X + ↑k < X)) h⟩))) fun h => Eq.trans (Fin.append_eval (fun k => iv (Fin.natAdd X (Fin.natAdd Y k))) (fun k => iv (Fin.natAdd X (Fin.castAdd Z k))) ⟨X + ↑k - X, id (Eq.refl (X + ↑k - X)) ▸ Decidable.byContradiction fun a => Fin.append_eval._proof_1 (Fin.cast rfl (Fin.cast (Eq.symm (Eq.symm (Nat.add_assoc X Z Y))) (Fin.castAdd Y (Fin.natAdd X k)))) (Eq.mpr_not (Eq.refl (X + ↑k < X)) h) a⟩) (dite_congr (Eq.refl (X + ↑k - X < Z)) (fun h_1 => Eq.refl (iv (Fin.natAdd X (Fin.natAdd Y ⟨X + ↑k - X, Eq.mpr_prop (Eq.refl (X + ↑k - X < Z)) h_1⟩)))) fun h_1 => Eq.refl (iv (Fin.natAdd X (Fin.castAdd Z ⟨X + ↑k - X - Z, Decidable.byContradiction fun a => Fin.append_eval._proof_1 ⟨X + ↑k - X, id (Eq.refl (X + ↑k - X)) ▸ Decidable.byContradiction fun a => Fin.append_eval._proof_1 (Fin.cast rfl (Fin.cast (Eq.symm (Eq.symm (Nat.add_assoc X Z Y))) (Fin.castAdd Y (Fin.natAdd X k)))) (Eq.mpr_not (Eq.refl (X + ↑k < X)) h) a⟩ (Eq.mpr_not (Eq.refl (X + ↑k - X < Z)) h_1) a⟩))))))) (funext fun k => Eq.trans (Fin.append_eval (fun k => iv (Fin.castAdd (Y + Z) k)) (Fin.append (fun k => iv (Fin.natAdd X (Fin.natAdd Y k))) fun k => iv (Fin.natAdd X (Fin.castAdd Z k))) (Fin.cast rfl (Fin.cast (Eq.symm (Eq.symm (Nat.add_assoc X Z Y))) (Fin.castAdd Y (Fin.castAdd Z k))))) (dite_congr (Eq.refl (↑k < X)) (fun h => Eq.refl (iv (Fin.castAdd (Y + Z) ⟨↑k, id (Eq.refl ↑k) ▸ Eq.mpr_prop (Eq.refl (↑k < X)) h⟩))) fun h => Eq.trans (Fin.append_eval (fun k => iv (Fin.natAdd X (Fin.natAdd Y k))) (fun k => iv (Fin.natAdd X (Fin.castAdd Z k))) ⟨↑k - X, id (Eq.refl (↑k - X)) ▸ Decidable.byContradiction fun a => Fin.append_eval._proof_1 (Fin.cast rfl (Fin.cast (Eq.symm (Eq.symm (Nat.add_assoc X Z Y))) (Fin.castAdd Y (Fin.castAdd Z k)))) (Eq.mpr_not (Eq.refl (↑k < X)) h) a⟩) (dite_congr (Eq.refl (↑k - X < Z)) (fun h_1 => Eq.refl (iv (Fin.natAdd X (Fin.natAdd Y ⟨↑k - X, Eq.mpr_prop (Eq.refl (↑k - X < Z)) h_1⟩)))) fun h_1 => Eq.refl (iv (Fin.natAdd X (Fin.castAdd Z ⟨↑k - X - Z, Decidable.byContradiction fun a => Fin.append_eval._proof_1 ⟨↑k - X, id (Eq.refl (↑k - X)) ▸ Decidable.byContradiction fun a => Fin.append_eval._proof_1 (Fin.cast rfl (Fin.cast (Eq.symm (Eq.symm (Nat.add_assoc X Z Y))) (Fin.castAdd Y (Fin.castAdd Z k)))) (Eq.mpr_not (Eq.refl (↑k < X)) h) a⟩ (Eq.mpr_not (Eq.refl (↑k - X < Z)) h_1) a⟩)))))))) (funext fun k => Eq.trans (Fin.append_eval (fun k => iv (Fin.castAdd (Y + Z) k)) (Fin.append (fun k => iv (Fin.natAdd X (Fin.natAdd Y k))) fun k => iv (Fin.natAdd X (Fin.castAdd Z k))) (Fin.cast rfl (Fin.cast (Eq.symm (Eq.symm (Nat.add_assoc X Z Y))) (Fin.natAdd (X + Z) k)))) (dite_congr (Eq.refl (X + Z + ↑k < X)) (fun h => Eq.refl (iv (Fin.castAdd (Y + Z) ⟨X + Z + ↑k, id (Eq.refl (X + Z + ↑k)) ▸ Eq.mpr_prop (Eq.refl (X + Z + ↑k < X)) h⟩))) fun h => Eq.trans (Fin.append_eval (fun k => iv (Fin.natAdd X (Fin.natAdd Y k))) (fun k => iv (Fin.natAdd X (Fin.castAdd Z k))) ⟨X + Z + ↑k - X, id (Eq.refl (X + Z + ↑k - X)) ▸ Decidable.byContradiction fun a => Fin.append_eval._proof_1 (Fin.cast rfl (Fin.cast (Eq.symm (Eq.symm (Nat.add_assoc X Z Y))) (Fin.natAdd (X + Z) k))) (Eq.mpr_not (Eq.refl (X + Z + ↑k < X)) h) a⟩) (dite_congr (Eq.refl (X + Z + ↑k - X < Z)) (fun h_1 => Eq.refl (iv (Fin.natAdd X (Fin.natAdd Y ⟨X + Z + ↑k - X, Eq.mpr_prop (Eq.refl (X + Z + ↑k - X < Z)) h_1⟩)))) fun h_1 => Eq.refl (iv (Fin.natAdd X (Fin.castAdd Z ⟨X + Z + ↑k - X - Z, Decidable.byContradiction fun a => Fin.append_eval._proof_1 ⟨X + Z + ↑k - X, id (Eq.refl (X + Z + ↑k - X)) ▸ Decidable.byContradiction fun a => Fin.append_eval._proof_1 (Fin.cast rfl (Fin.cast (Eq.symm (Eq.symm (Nat.add_assoc X Z Y))) (Fin.natAdd (X + Z) k))) (Eq.mpr_not (Eq.refl (X + Z + ↑k < X)) h) a⟩ (Eq.mpr_not (Eq.refl (X + Z + ↑k - X < Z)) h_1) a⟩))))))) j) (Fin.append_eval (Fin.append (fun k => if h : X + ↑k < X then iv (Fin.castAdd (Y + Z) ⟨X + ↑k, id (Eq.refl (X + ↑k)) ▸ Eq.mpr_prop (Eq.refl (X + ↑k < X)) h⟩) else if h_1 : X + ↑k - X < Z then iv (Fin.natAdd X (Fin.natAdd Y ⟨X + ↑k - X, Eq.mpr_prop (Eq.refl (X + ↑k - X < Z)) h_1⟩)) else iv (Fin.natAdd X (Fin.castAdd Z ⟨X + ↑k - X - Z, Decidable.byContradiction fun a => Fin.append_eval._proof_1 ⟨X + ↑k - X, id (Eq.refl (X + ↑k - X)) ▸ Decidable.byContradiction fun a => Fin.append_eval._proof_1 (Fin.cast rfl (Fin.cast (Eq.symm (Eq.symm (Nat.add_assoc X Z Y))) (Fin.castAdd Y (Fin.natAdd X k)))) (Eq.mpr_not (Eq.refl (X + ↑k < X)) h) a⟩ (Eq.mpr_not (Eq.refl (X + ↑k - X < Z)) h_1) a⟩))) fun k => if h : ↑k < X then iv (Fin.castAdd (Y + Z) ⟨↑k, id (Eq.refl ↑k) ▸ Eq.mpr_prop (Eq.refl (↑k < X)) h⟩) else if h_1 : ↑k - X < Z then iv (Fin.natAdd X (Fin.natAdd Y ⟨↑k - X, Eq.mpr_prop (Eq.refl (↑k - X < Z)) h_1⟩)) else iv (Fin.natAdd X (Fin.castAdd Z ⟨↑k - X - Z, Decidable.byContradiction fun a => Fin.append_eval._proof_1 ⟨↑k - X, id (Eq.refl (↑k - X)) ▸ Decidable.byContradiction fun a => Fin.append_eval._proof_1 (Fin.cast rfl (Fin.cast (Eq.symm (Eq.symm (Nat.add_assoc X Z Y))) (Fin.castAdd Y (Fin.castAdd Z k)))) (Eq.mpr_not (Eq.refl (↑k < X)) h) a⟩ (Eq.mpr_not (Eq.refl (↑k - X < Z)) h_1) a⟩))) (fun k => if h : X + Z + ↑k < X then iv (Fin.castAdd (Y + Z) ⟨X + Z + ↑k, id (Eq.refl (X + Z + ↑k)) ▸ Eq.mpr_prop (Eq.refl (X + Z + ↑k < X)) h⟩) else if h_1 : X + Z + ↑k - X < Z then iv (Fin.natAdd X (Fin.natAdd Y ⟨X + Z + ↑k - X, Eq.mpr_prop (Eq.refl (X + Z + ↑k - X < Z)) h_1⟩)) else iv (Fin.natAdd X (Fin.castAdd Z ⟨X + Z + ↑k - X - Z, Decidable.byContradiction fun a => Fin.append_eval._proof_1 ⟨X + Z + ↑k - X, id (Eq.refl (X + Z + ↑k - X)) ▸ Decidable.byContradiction fun a => Fin.append_eval._proof_1 (Fin.cast rfl (Fin.cast (Eq.symm (Eq.symm (Nat.add_assoc X Z Y))) (Fin.natAdd (X + Z) k))) (Eq.mpr_not (Eq.refl (X + Z + ↑k < X)) h) a⟩ (Eq.mpr_not (Eq.refl (X + Z + ↑k - X < Z)) h_1) a⟩))) j)) (dite_congr (Eq.refl (↑j < Z + X)) (fun h => Eq.trans (Fin.append_eval (fun k => if h : X + ↑k < X then iv (Fin.castAdd (Y + Z) ⟨X + ↑k, id (Eq.refl (X + ↑k)) ▸ Eq.mpr_prop (Eq.refl (X + ↑k < X)) h⟩) else if h_1 : X + ↑k - X < Z then iv (Fin.natAdd X (Fin.natAdd Y ⟨X + ↑k - X, Eq.mpr_prop (Eq.refl (X + ↑k - X < Z)) h_1⟩)) else iv (Fin.natAdd X (Fin.castAdd Z ⟨X + ↑k - X - Z, Decidable.byContradiction fun a => Fin.append_eval._proof_1 ⟨X + ↑k - X, id (Eq.refl (X + ↑k - X)) ▸ Decidable.byContradiction fun a => Fin.append_eval._proof_1 (Fin.cast rfl (Fin.cast (Eq.symm (Eq.symm (Nat.add_assoc X Z Y))) (Fin.castAdd Y (Fin.natAdd X k)))) (Eq.mpr_not (Eq.refl (X + ↑k < X)) h) a⟩ (Eq.mpr_not (Eq.refl (X + ↑k - X < Z)) h_1) a⟩))) (fun k => if h : ↑k < X then iv (Fin.castAdd (Y + Z) ⟨↑k, id (Eq.refl ↑k) ▸ Eq.mpr_prop (Eq.refl (↑k < X)) h⟩) else if h_1 : ↑k - X < Z then iv (Fin.natAdd X (Fin.natAdd Y ⟨↑k - X, Eq.mpr_prop (Eq.refl (↑k - X < Z)) h_1⟩)) else iv (Fin.natAdd X (Fin.castAdd Z ⟨↑k - X - Z, Decidable.byContradiction fun a => Fin.append_eval._proof_1 ⟨↑k - X, id (Eq.refl (↑k - X)) ▸ Decidable.byContradiction fun a => Fin.append_eval._proof_1 (Fin.cast rfl (Fin.cast (Eq.symm (Eq.symm (Nat.add_assoc X Z Y))) (Fin.castAdd Y (Fin.castAdd Z k)))) (Eq.mpr_not (Eq.refl (↑k < X)) h) a⟩ (Eq.mpr_not (Eq.refl (↑k - X < Z)) h_1) a⟩))) ⟨↑j, Eq.mpr_prop (Eq.refl (↑j < Z + X)) h⟩) (dite_congr (Eq.refl (↑j < Z)) (fun h_1 => dite_congr (Eq.refl (X + ↑j < X)) (fun h_2 => Eq.refl (iv (Fin.castAdd (Y + Z) ⟨X + ↑j, id (Eq.refl (X + ↑⟨↑⟨↑j, Eq.mpr_prop (Eq.refl (↑j < Z + X)) h⟩, Eq.mpr_prop (Eq.refl (↑j < Z)) h_1⟩)) ▸ Eq.mpr_prop (Eq.refl (X + ↑⟨↑⟨↑j, Eq.mpr_prop (Eq.refl (↑j < Z + X)) h⟩, Eq.mpr_prop (Eq.refl (↑j < Z)) h_1⟩ < X)) (Eq.mpr_prop (Eq.refl (X + ↑j < X)) h_2)⟩))) fun h_2 => dite_congr (Eq.refl (X + ↑j - X < Z)) (fun h_3 => Eq.refl (iv (Fin.natAdd X (Fin.natAdd Y ⟨X + ↑j - X, Eq.mpr_prop (Eq.refl (X + ↑⟨↑⟨↑j, Eq.mpr_prop (Eq.refl (↑j < Z + X)) h⟩, Eq.mpr_prop (Eq.refl (↑j < Z)) h_1⟩ - X < Z)) (Eq.mpr_prop (Eq.refl (X + ↑j - X < Z)) h_3)⟩)))) fun h_3 => Eq.refl (iv (Fin.natAdd X (Fin.castAdd Z ⟨X + ↑j - X - Z, Decidable.byContradiction fun a => Fin.append_eval._proof_1 ⟨X + ↑⟨↑⟨↑j, Eq.mpr_prop (Eq.refl (↑j < Z + X)) h⟩, Eq.mpr_prop (Eq.refl (↑j < Z)) h_1⟩ - X, id (Eq.refl (X + ↑⟨↑⟨↑j, Eq.mpr_prop (Eq.refl (↑j < Z + X)) h⟩, Eq.mpr_prop (Eq.refl (↑j < Z)) h_1⟩ - X)) ▸ Decidable.byContradiction fun a => Fin.append_eval._proof_1 (Fin.cast rfl (Fin.cast (Eq.symm (Eq.symm (Nat.add_assoc X Z Y))) (Fin.castAdd Y (Fin.natAdd X ⟨↑⟨↑j, Eq.mpr_prop (Eq.refl (↑j < Z + X)) h⟩, Eq.mpr_prop (Eq.refl (↑j < Z)) h_1⟩)))) (Eq.mpr_not (Eq.refl (X + ↑⟨↑⟨↑j, Eq.mpr_prop (Eq.refl (↑j < Z + X)) h⟩, Eq.mpr_prop (Eq.refl (↑j < Z)) h_1⟩ < X)) (Eq.mpr_not (Eq.refl (X + ↑j < X)) h_2)) a⟩ (Eq.mpr_not (Eq.refl (X + ↑⟨↑⟨↑j, Eq.mpr_prop (Eq.refl (↑j < Z + X)) h⟩, Eq.mpr_prop (Eq.refl (↑j < Z)) h_1⟩ - X < Z)) (Eq.mpr_not (Eq.refl (X + ↑j - X < Z)) h_3)) a⟩)))) fun h_1 => dite_congr (Eq.refl (↑j - Z < X)) (fun h_2 => Eq.refl (iv (Fin.castAdd (Y + Z) ⟨↑j - Z, id (Eq.refl ↑⟨↑⟨↑j, Eq.mpr_prop (Eq.refl (↑j < Z + X)) h⟩ - Z, Decidable.byContradiction fun a => Fin.append_eval._proof_1 ⟨↑j, Eq.mpr_prop (Eq.refl (↑j < Z + X)) h⟩ (Eq.mpr_not (Eq.refl (↑j < Z)) h_1) a⟩) ▸ Eq.mpr_prop (Eq.refl (↑⟨↑⟨↑j, Eq.mpr_prop (Eq.refl (↑j < Z + X)) h⟩ - Z, Decidable.byContradiction fun a => Fin.append_eval._proof_1 ⟨↑j, Eq.mpr_prop (Eq.refl (↑j < Z + X)) h⟩ (Eq.mpr_not (Eq.refl (↑j < Z)) h_1) a⟩ < X)) (Eq.mpr_prop (Eq.refl (↑j - Z < X)) h_2)⟩))) fun h_2 => dite_congr (Eq.refl (↑j - Z - X < Z)) (fun h_3 => Eq.refl (iv (Fin.natAdd X (Fin.natAdd Y ⟨↑j - Z - X, Eq.mpr_prop (Eq.refl (↑⟨↑⟨↑j, Eq.mpr_prop (Eq.refl (↑j < Z + X)) h⟩ - Z, Decidable.byContradiction fun a => Fin.append_eval._proof_1 ⟨↑j, Eq.mpr_prop (Eq.refl (↑j < Z + X)) h⟩ (Eq.mpr_not (Eq.refl (↑j < Z)) h_1) a⟩ - X < Z)) (Eq.mpr_prop (Eq.refl (↑j - Z - X < Z)) h_3)⟩)))) fun h_3 => Eq.refl (iv (Fin.natAdd X (Fin.castAdd Z ⟨↑j - Z - X - Z, Decidable.byContradiction fun a => Fin.append_eval._proof_1 ⟨↑⟨↑⟨↑j, Eq.mpr_prop (Eq.refl (↑j < Z + X)) h⟩ - Z, Decidable.byContradiction fun a => Fin.append_eval._proof_1 ⟨↑j, Eq.mpr_prop (Eq.refl (↑j < Z + X)) h⟩ (Eq.mpr_not (Eq.refl (↑j < Z)) h_1) a⟩ - X, id (Eq.refl (↑⟨↑⟨↑j, Eq.mpr_prop (Eq.refl (↑j < Z + X)) h⟩ - Z, Decidable.byContradiction fun a => Fin.append_eval._proof_1 ⟨↑j, Eq.mpr_prop (Eq.refl (↑j < Z + X)) h⟩ (Eq.mpr_not (Eq.refl (↑j < Z)) h_1) a⟩ - X)) ▸ Decidable.byContradiction fun a => Fin.append_eval._proof_1 (Fin.cast rfl (Fin.cast (Eq.symm (Eq.symm (Nat.add_assoc X Z Y))) (Fin.castAdd Y (Fin.castAdd Z ⟨↑⟨↑j, Eq.mpr_prop (Eq.refl (↑j < Z + X)) h⟩ - Z, Decidable.byContradiction fun a => Fin.append_eval._proof_1 ⟨↑j, Eq.mpr_prop (Eq.refl (↑j < Z + X)) h⟩ (Eq.mpr_not (Eq.refl (↑j < Z)) h_1) a⟩)))) (Eq.mpr_not (Eq.refl (↑⟨↑⟨↑j, Eq.mpr_prop (Eq.refl (↑j < Z + X)) h⟩ - Z, Decidable.byContradiction fun a => Fin.append_eval._proof_1 ⟨↑j, Eq.mpr_prop (Eq.refl (↑j < Z + X)) h⟩ (Eq.mpr_not (Eq.refl (↑j < Z)) h_1) a⟩ < X)) (Eq.mpr_not (Eq.refl (↑j - Z < X)) h_2)) a⟩ (Eq.mpr_not (Eq.refl (↑⟨↑⟨↑j, Eq.mpr_prop (Eq.refl (↑j < Z + X)) h⟩ - Z, Decidable.byContradiction fun a => Fin.append_eval._proof_1 ⟨↑j, Eq.mpr_prop (Eq.refl (↑j < Z + X)) h⟩ (Eq.mpr_not (Eq.refl (↑j < Z)) h_1) a⟩ - X < Z)) (Eq.mpr_not (Eq.refl (↑j - Z - X < Z)) h_3)) a⟩))))) fun h => dite_congr (Eq.refl (X + Z + (↑j - (Z + X)) < X)) (fun h_1 => Eq.refl (iv (Fin.castAdd (Y + Z) ⟨X + Z + (↑j - (Z + X)), id (Eq.refl (X + Z + ↑⟨↑j - (Z + X), Decidable.byContradiction fun a => Fin.append_eval._proof_1 j (Eq.mpr_not (Eq.refl (↑j < Z + X)) h) a⟩)) ▸ Eq.mpr_prop (Eq.refl (X + Z + ↑⟨↑j - (Z + X), Decidable.byContradiction fun a => Fin.append_eval._proof_1 j (Eq.mpr_not (Eq.refl (↑j < Z + X)) h) a⟩ < X)) (Eq.mpr_prop (Eq.refl (X + Z + (↑j - (Z + X)) < X)) h_1)⟩))) fun h_1 => dite_congr (Eq.refl (X + Z + (↑j - (Z + X)) - X < Z)) (fun h_2 => Eq.refl (iv (Fin.natAdd X (Fin.natAdd Y ⟨X + Z + (↑j - (Z + X)) - X, Eq.mpr_prop (Eq.refl (X + Z + ↑⟨↑j - (Z + X), Decidable.byContradiction fun a => Fin.append_eval._proof_1 j (Eq.mpr_not (Eq.refl (↑j < Z + X)) h) a⟩ - X < Z)) (Eq.mpr_prop (Eq.refl (X + Z + (↑j - (Z + X)) - X < Z)) h_2)⟩)))) fun h_2 => Eq.refl (iv (Fin.natAdd X (Fin.castAdd Z ⟨X + Z + (↑j - (Z + X)) - X - Z, Decidable.byContradiction fun a => Fin.append_eval._proof_1 ⟨X + Z + ↑⟨↑j - (Z + X), Decidable.byContradiction fun a => Fin.append_eval._proof_1 j (Eq.mpr_not (Eq.refl (↑j < Z + X)) h) a⟩ - X, id (Eq.refl (X + Z + ↑⟨↑j - (Z + X), Decidable.byContradiction fun a => Fin.append_eval._proof_1 j (Eq.mpr_not (Eq.refl (↑j < Z + X)) h) a⟩ - X)) ▸ Decidable.byContradiction fun a => Fin.append_eval._proof_1 (Fin.cast rfl (Fin.cast (Eq.symm (Eq.symm (Nat.add_assoc X Z Y))) (Fin.natAdd (X + Z) ⟨↑j - (Z + X), Decidable.byContradiction fun a => Fin.append_eval._proof_1 j (Eq.mpr_not (Eq.refl (↑j < Z + X)) h) a⟩))) (Eq.mpr_not (Eq.refl (X + Z + ↑⟨↑j - (Z + X), Decidable.byContradiction fun a => Fin.append_eval._proof_1 j (Eq.mpr_not (Eq.refl (↑j < Z + X)) h) a⟩ < X)) (Eq.mpr_not (Eq.refl (X + Z + (↑j - (Z + X)) < X)) h_1)) a⟩ (Eq.mpr_not (Eq.refl (X + Z + ↑⟨↑j - (Z + X), Decidable.byContradiction fun a => Fin.append_eval._proof_1 j (Eq.mpr_not (Eq.refl (↑j < Z + X)) h) a⟩ - X < Z)) (Eq.mpr_not (Eq.refl (X + Z + (↑j - (Z + X)) - X < Z)) h_2)) a⟩))))))) (if h : ↑j < Z then Eq.mpr (id (congr (congrArg Eq (dif_pos h)) (dite_congr (Eq.refl (↑j < Z + X)) (fun h_1 => dif_pos h) fun h => Eq.refl (if h_1 : X + Z + (↑j - (Z + X)) < X then iv (Fin.castAdd (Y + Z) ⟨X + Z + (↑j - (Z + X)), id (Eq.refl (X + Z + ↑⟨↑j - (Z + X), Decidable.byContradiction fun a => Fin.append_eval._proof_1 j (Eq.mpr_not (Eq.refl (↑j < Z + X)) (Eq.mpr_not (Eq.refl (↑j < Z + X)) h)) a⟩)) ▸ Eq.mpr_prop (Eq.refl (X + Z + ↑⟨↑j - (Z + X), Decidable.byContradiction fun a => Fin.append_eval._proof_1 j (Eq.mpr_not (Eq.refl (↑j < Z + X)) (Eq.mpr_not (Eq.refl (↑j < Z + X)) h)) a⟩ < X)) (Eq.mpr_prop (Eq.refl (X + Z + (↑j - (Z + X)) < X)) h_1)⟩) else if h_2 : X + Z + (↑j - (Z + X)) - X < Z then iv (Fin.natAdd X (Fin.natAdd Y ⟨X + Z + (↑j - (Z + X)) - X, Eq.mpr_prop (Eq.refl (X + Z + ↑⟨↑j - (Z + X), Decidable.byContradiction fun a => Fin.append_eval._proof_1 j (Eq.mpr_not (Eq.refl (↑j < Z + X)) (Eq.mpr_not (Eq.refl (↑j < Z + X)) h)) a⟩ - X < Z)) (Eq.mpr_prop (Eq.refl (X + Z + (↑j - (Z + X)) - X < Z)) h_2)⟩)) else iv (Fin.natAdd X (Fin.castAdd Z ⟨X + Z + (↑j - (Z + X)) - X - Z, Decidable.byContradiction fun a => Fin.append_eval._proof_1 ⟨X + Z + ↑⟨↑j - (Z + X), Decidable.byContradiction fun a => Fin.append_eval._proof_1 j (Eq.mpr_not (Eq.refl (↑j < Z + X)) (Eq.mpr_not (Eq.refl (↑j < Z + X)) h)) a⟩ - X, id (Eq.refl (X + Z + ↑⟨↑j - (Z + X), Decidable.byContradiction fun a => Fin.append_eval._proof_1 j (Eq.mpr_not (Eq.refl (↑j < Z + X)) (Eq.mpr_not (Eq.refl (↑j < Z + X)) h)) a⟩ - X)) ▸ Decidable.byContradiction fun a => Fin.append_eval._proof_1 (Fin.cast rfl (Fin.cast (Eq.symm (Eq.symm (Nat.add_assoc X Z Y))) (Fin.natAdd (X + Z) ⟨↑j - (Z + X), Decidable.byContradiction fun a => Fin.append_eval._proof_1 j (Eq.mpr_not (Eq.refl (↑j < Z + X)) (Eq.mpr_not (Eq.refl (↑j < Z + X)) h)) a⟩))) (Eq.mpr_not (Eq.refl (X + Z + ↑⟨↑j - (Z + X), Decidable.byContradiction fun a => Fin.append_eval._proof_1 j (Eq.mpr_not (Eq.refl (↑j < Z + X)) (Eq.mpr_not (Eq.refl (↑j < Z + X)) h)) a⟩ < X)) (Eq.mpr_not (Eq.refl (X + Z + (↑j - (Z + X)) < X)) h_1)) a⟩ (Eq.mpr_not (Eq.refl (X + Z + ↑⟨↑j - (Z + X), Decidable.byContradiction fun a => Fin.append_eval._proof_1 j (Eq.mpr_not (Eq.refl (↑j < Z + X)) (Eq.mpr_not (Eq.refl (↑j < Z + X)) h)) a⟩ - X < Z)) (Eq.mpr_not (Eq.refl (X + Z + (↑j - (Z + X)) - X < Z)) h_2)) a⟩)))))) (if h_1 : ↑j < Z + X then Eq.mpr (id (congrArg (Eq (iv (Fin.cast rfl (Fin.cast (Eq.symm (Eq.symm (Nat.add_assoc X Y Z))) (Fin.natAdd (X + Y) ⟨↑j, id (Eq.refl ↑j) ▸ Eq.mpr_prop (Eq.refl (↑j < Z)) h⟩))))) (dif_pos h_1))) (if h_2 : X + ↑j < X then Eq.mpr (id (congrArg (Eq (iv (Fin.cast rfl (Fin.cast (Eq.symm (Eq.symm (Nat.add_assoc X Y Z))) (Fin.natAdd (X + Y) ⟨↑j, id (Eq.refl ↑j) ▸ Eq.mpr_prop (Eq.refl (↑j < Z)) h⟩))))) (dif_pos h_2))) (False.elim (Component.hexagon_reverse_arrow._proof_1_1 X Y Z j h_2)) else Eq.mpr (id (congrArg (Eq (iv (Fin.cast rfl (Fin.cast (Eq.symm (Eq.symm (Nat.add_assoc X Y Z))) (Fin.natAdd (X + Y) ⟨↑j, id (Eq.refl ↑j) ▸ Eq.mpr_prop (Eq.refl (↑j < Z)) h⟩))))) (dif_neg h_2))) (if h_3 : X + ↑j - X < Z then Eq.mpr (id (congrArg (Eq (iv (Fin.cast rfl (Fin.cast (Eq.symm (Eq.symm (Nat.add_assoc X Y Z))) (Fin.natAdd (X + Y) ⟨↑j, id (Eq.refl ↑j) ▸ Eq.mpr_prop (Eq.refl (↑j < Z)) h⟩))))) (dif_pos h_3))) ((fun a a_1 e_a => e_a ▸ Eq.refl (iv a)) (Fin.cast rfl (Fin.cast (Eq.symm (Eq.symm (Nat.add_assoc X Y Z))) (Fin.natAdd (X + Y) ⟨↑j, id (Eq.refl ↑j) ▸ Eq.mpr_prop (Eq.refl (↑j < Z)) h⟩))) (Fin.natAdd X (Fin.natAdd Y ⟨X + ↑j - X, Eq.mpr_prop (Eq.refl (X + ↑⟨↑⟨↑j, Eq.mpr_prop (Eq.refl (↑j < Z + X)) (Eq.mpr_prop (Eq.refl (↑j < Z + X)) h_1)⟩, Eq.mpr_prop (Eq.refl (↑j < Z)) h⟩ - X < Z)) (Eq.mpr_prop (Eq.refl (X + ↑j - X < Z)) h_3)⟩)) (Fin.ext (Eq.mpr (id (congrArg (Eq (X + Y + ↑j)) (congrArg Fin.val (congrArg (Fin.natAdd X) (congrArg (Fin.natAdd Y) (Fin.mk.congr_simp (X + ↑j - X) (↑j) (add_tsub_cancel_left X ↑j) (Eq.mpr_prop (Eq.refl (X + ↑⟨↑⟨↑j, Eq.mpr_prop (Eq.refl (↑j < Z + X)) (Eq.mpr_prop (Eq.refl (↑j < Z + X)) h_1)⟩, Eq.mpr_prop (Eq.refl (↑j < Z)) h⟩ - X < Z)) (Eq.mpr_prop (Eq.refl (X + ↑j - X < Z)) h_3)))))))) (Decidable.byContradiction fun a => Component.hexagon_reverse_arrow._proof_1_2 X Y Z j a)))) else Eq.mpr (id (congrArg (Eq (iv (Fin.cast rfl (Fin.cast (Eq.symm (Eq.symm (Nat.add_assoc X Y Z))) (Fin.natAdd (X + Y) ⟨↑j, id (Eq.refl ↑j) ▸ Eq.mpr_prop (Eq.refl (↑j < Z)) h⟩))))) (dif_neg h_3))) (False.elim (Component.hexagon_reverse_arrow._proof_1_3 X Y Z j h h_2 h_3)))) else Eq.mpr (id (congrArg (Eq (iv (Fin.cast rfl (Fin.cast (Eq.symm (Eq.symm (Nat.add_assoc X Y Z))) (Fin.natAdd (X + Y) ⟨↑j, id (Eq.refl ↑j) ▸ Eq.mpr_prop (Eq.refl (↑j < Z)) h⟩))))) (dif_neg h_1))) (if h_2 : X + Z + (↑j - (Z + X)) < X then Eq.mpr (id (congrArg (Eq (iv (Fin.cast rfl (Fin.cast (Eq.symm (Eq.symm (Nat.add_assoc X Y Z))) (Fin.natAdd (X + Y) ⟨↑j, id (Eq.refl ↑j) ▸ Eq.mpr_prop (Eq.refl (↑j < Z)) h⟩))))) (dif_pos h_2))) (False.elim (Component.hexagon_reverse_arrow._proof_1_4 X Y Z j h h_1)) else Eq.mpr (id (congrArg (Eq (iv (Fin.cast rfl (Fin.cast (Eq.symm (Eq.symm (Nat.add_assoc X Y Z))) (Fin.natAdd (X + Y) ⟨↑j, id (Eq.refl ↑j) ▸ Eq.mpr_prop (Eq.refl (↑j < Z)) h⟩))))) (dif_neg h_2))) (if h_3 : X + Z + (↑j - (Z + X)) - X < Z then Eq.mpr (id (congrArg (Eq (iv (Fin.cast rfl (Fin.cast (Eq.symm (Eq.symm (Nat.add_assoc X Y Z))) (Fin.natAdd (X + Y) ⟨↑j, id (Eq.refl ↑j) ▸ Eq.mpr_prop (Eq.refl (↑j < Z)) h⟩))))) (dif_pos h_3))) (False.elim (Component.hexagon_reverse_arrow._proof_1_4 X Y Z j h h_1)) else Eq.mpr (id (congrArg (Eq (iv (Fin.cast rfl (Fin.cast (Eq.symm (Eq.symm (Nat.add_assoc X Y Z))) (Fin.natAdd (X + Y) ⟨↑j, id (Eq.refl ↑j) ▸ Eq.mpr_prop (Eq.refl (↑j < Z)) h⟩))))) (dif_neg h_3))) (False.elim (Component.hexagon_reverse_arrow._proof_1_4 X Y Z j h h_1))))) else Eq.mpr (id (congr (congrArg Eq (dif_neg h)) (dite_congr (Eq.refl (↑j < Z + X)) (fun h_1 => dif_neg h) fun h => Eq.refl (if h_1 : X + Z + (↑j - (Z + X)) < X then iv (Fin.castAdd (Y + Z) ⟨X + Z + (↑j - (Z + X)), id (Eq.refl (X + Z + ↑⟨↑j - (Z + X), Decidable.byContradiction fun a => Fin.append_eval._proof_1 j (Eq.mpr_not (Eq.refl (↑j < Z + X)) (Eq.mpr_not (Eq.refl (↑j < Z + X)) h)) a⟩)) ▸ Eq.mpr_prop (Eq.refl (X + Z + ↑⟨↑j - (Z + X), Decidable.byContradiction fun a => Fin.append_eval._proof_1 j (Eq.mpr_not (Eq.refl (↑j < Z + X)) (Eq.mpr_not (Eq.refl (↑j < Z + X)) h)) a⟩ < X)) (Eq.mpr_prop (Eq.refl (X + Z + (↑j - (Z + X)) < X)) h_1)⟩) else if h_2 : X + Z + (↑j - (Z + X)) - X < Z then iv (Fin.natAdd X (Fin.natAdd Y ⟨X + Z + (↑j - (Z + X)) - X, Eq.mpr_prop (Eq.refl (X + Z + ↑⟨↑j - (Z + X), Decidable.byContradiction fun a => Fin.append_eval._proof_1 j (Eq.mpr_not (Eq.refl (↑j < Z + X)) (Eq.mpr_not (Eq.refl (↑j < Z + X)) h)) a⟩ - X < Z)) (Eq.mpr_prop (Eq.refl (X + Z + (↑j - (Z + X)) - X < Z)) h_2)⟩)) else iv (Fin.natAdd X (Fin.castAdd Z ⟨X + Z + (↑j - (Z + X)) - X - Z, Decidable.byContradiction fun a => Fin.append_eval._proof_1 ⟨X + Z + ↑⟨↑j - (Z + X), Decidable.byContradiction fun a => Fin.append_eval._proof_1 j (Eq.mpr_not (Eq.refl (↑j < Z + X)) (Eq.mpr_not (Eq.refl (↑j < Z + X)) h)) a⟩ - X, id (Eq.refl (X + Z + ↑⟨↑j - (Z + X), Decidable.byContradiction fun a => Fin.append_eval._proof_1 j (Eq.mpr_not (Eq.refl (↑j < Z + X)) (Eq.mpr_not (Eq.refl (↑j < Z + X)) h)) a⟩ - X)) ▸ Decidable.byContradiction fun a => Fin.append_eval._proof_1 (Fin.cast rfl (Fin.cast (Eq.symm (Eq.symm (Nat.add_assoc X Z Y))) (Fin.natAdd (X + Z) ⟨↑j - (Z + X), Decidable.byContradiction fun a => Fin.append_eval._proof_1 j (Eq.mpr_not (Eq.refl (↑j < Z + X)) (Eq.mpr_not (Eq.refl (↑j < Z + X)) h)) a⟩))) (Eq.mpr_not (Eq.refl (X + Z + ↑⟨↑j - (Z + X), Decidable.byContradiction fun a => Fin.append_eval._proof_1 j (Eq.mpr_not (Eq.refl (↑j < Z + X)) (Eq.mpr_not (Eq.refl (↑j < Z + X)) h)) a⟩ < X)) (Eq.mpr_not (Eq.refl (X + Z + (↑j - (Z + X)) < X)) h_1)) a⟩ (Eq.mpr_not (Eq.refl (X + Z + ↑⟨↑j - (Z + X), Decidable.byContradiction fun a => Fin.append_eval._proof_1 j (Eq.mpr_not (Eq.refl (↑j < Z + X)) (Eq.mpr_not (Eq.refl (↑j < Z + X)) h)) a⟩ - X < Z)) (Eq.mpr_not (Eq.refl (X + Z + (↑j - (Z + X)) - X < Z)) h_2)) a⟩)))))) (if h_1 : ↑j < Z + X then Eq.mpr (id (congrArg (Eq (iv (Fin.cast rfl (Fin.cast (Eq.symm (Eq.symm (Nat.add_assoc X Y Z))) (Fin.castAdd Z ⟨↑j - Z, id (Eq.refl (↑j - Z)) ▸ Decidable.byContradiction fun a => Fin.append_eval._proof_1 (Fin.cast rfl (Fin.cast (Eq.symm (Eq.symm (Nat.add_assoc Z X Y))) j)) (Eq.mpr_not (Eq.refl (↑j < Z)) h) a⟩))))) (dif_pos h_1))) (if h_2 : ↑j - Z < X then Eq.mpr (id (congrArg (Eq (iv (Fin.cast rfl (Fin.cast (Eq.symm (Eq.symm (Nat.add_assoc X Y Z))) (Fin.castAdd Z ⟨↑j - Z, id (Eq.refl (↑j - Z)) ▸ Decidable.byContradiction fun a => Fin.append_eval._proof_1 (Fin.cast rfl (Fin.cast (Eq.symm (Eq.symm (Nat.add_assoc Z X Y))) j)) (Eq.mpr_not (Eq.refl (↑j < Z)) h) a⟩))))) (dif_pos h_2))) (Eq.refl (iv (Fin.cast rfl (Fin.cast (Eq.symm (Eq.symm (Nat.add_assoc X Y Z))) (Fin.castAdd Z ⟨↑j - Z, id (Eq.refl (↑j - Z)) ▸ Decidable.byContradiction fun a => Fin.append_eval._proof_1 (Fin.cast rfl (Fin.cast (Eq.symm (Eq.symm (Nat.add_assoc Z X Y))) j)) (Eq.mpr_not (Eq.refl (↑j < Z)) h) a⟩))))) else Eq.mpr (id (congrArg (Eq (iv (Fin.cast rfl (Fin.cast (Eq.symm (Eq.symm (Nat.add_assoc X Y Z))) (Fin.castAdd Z ⟨↑j - Z, id (Eq.refl (↑j - Z)) ▸ Decidable.byContradiction fun a => Fin.append_eval._proof_1 (Fin.cast rfl (Fin.cast (Eq.symm (Eq.symm (Nat.add_assoc Z X Y))) j)) (Eq.mpr_not (Eq.refl (↑j < Z)) h) a⟩))))) (dif_neg h_2))) (if h_3 : ↑j - Z - X < Z then Eq.mpr (id (congrArg (Eq (iv (Fin.cast rfl (Fin.cast (Eq.symm (Eq.symm (Nat.add_assoc X Y Z))) (Fin.castAdd Z ⟨↑j - Z, id (Eq.refl (↑j - Z)) ▸ Decidable.byContradiction fun a => Fin.append_eval._proof_1 (Fin.cast rfl (Fin.cast (Eq.symm (Eq.symm (Nat.add_assoc Z X Y))) j)) (Eq.mpr_not (Eq.refl (↑j < Z)) h) a⟩))))) (dif_pos h_3))) (False.elim (Component.hexagon_reverse_arrow._proof_1_5 X Y Z j h h_1 h_2)) else Eq.mpr (id (congrArg (Eq (iv (Fin.cast rfl (Fin.cast (Eq.symm (Eq.symm (Nat.add_assoc X Y Z))) (Fin.castAdd Z ⟨↑j - Z, id (Eq.refl (↑j - Z)) ▸ Decidable.byContradiction fun a => Fin.append_eval._proof_1 (Fin.cast rfl (Fin.cast (Eq.symm (Eq.symm (Nat.add_assoc Z X Y))) j)) (Eq.mpr_not (Eq.refl (↑j < Z)) h) a⟩))))) (dif_neg h_3))) (False.elim (Component.hexagon_reverse_arrow._proof_1_5 X Y Z j h h_1 h_2)))) else Eq.mpr (id (congrArg (Eq (iv (Fin.cast rfl (Fin.cast (Eq.symm (Eq.symm (Nat.add_assoc X Y Z))) (Fin.castAdd Z ⟨↑j - Z, id (Eq.refl (↑j - Z)) ▸ Decidable.byContradiction fun a => Fin.append_eval._proof_1 (Fin.cast rfl (Fin.cast (Eq.symm (Eq.symm (Nat.add_assoc Z X Y))) j)) (Eq.mpr_not (Eq.refl (↑j < Z)) h) a⟩))))) (dif_neg h_1))) (if h_2 : X + Z + (↑j - (Z + X)) < X then Eq.mpr (id (congrArg (Eq (iv (Fin.cast rfl (Fin.cast (Eq.symm (Eq.symm (Nat.add_assoc X Y Z))) (Fin.castAdd Z ⟨↑j - Z, id (Eq.refl (↑j - Z)) ▸ Decidable.byContradiction fun a => Fin.append_eval._proof_1 (Fin.cast rfl (Fin.cast (Eq.symm (Eq.symm (Nat.add_assoc Z X Y))) j)) (Eq.mpr_not (Eq.refl (↑j < Z)) h) a⟩))))) (dif_pos h_2))) (False.elim (Component.hexagon_reverse_arrow._proof_1_6 X Y Z j h_2)) else Eq.mpr (id (congrArg (Eq (iv (Fin.cast rfl (Fin.cast (Eq.symm (Eq.symm (Nat.add_assoc X Y Z))) (Fin.castAdd Z ⟨↑j - Z, ⋯ ▸ Decidable.byContradiction fun a => Fin.append_eval._proof_1 (Fin.cast rfl (Fin.cast (Eq.symm ⋯) ⋯)) ⋯ ⋯⟩))))) ⋯)) ⋯))))))))
Complexity: 36898121 (size of the value term)
Dependencies: Component.id, Component.parallel, Component.recast, Component.sequential, Component.symmetry, InformationSystem.equivalent, instNonemptyForallFin_computerNetworks, instNormForallFin_computerNetworks, instNormProd_computerNetworks, instNormUnit_computerNetworks
Proof dependencies: Component.equivalent_of_stationary, Fin.append_eval
Mathlib dependencies: Fin.append, Norm, add_tsub_cancel_left
Lean core dependencies: And, Bool, Decidable.byContradiction, Decidable.decide, Eq, Eq.mpr, Eq.mpr_not, Eq.mpr_prop, Eq.symm, Eq.trans, False, False.elim, Fin, Fin.cast, Fin.castAdd, Fin.ext, Fin.natAdd, Function.comp, GT.gt, Int, Int.add_one_le_of_lt, Int.natCast_add, Int.natCast_nonneg, 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.combine_sat', Lean.Omega.Constraint.isImpossible, Lean.Omega.Constraint.not_sat'_of_isImpossible, Lean.Omega.Int.add_congr, Lean.Omega.Int.ofNat_le_of_le, Lean.Omega.Int.ofNat_lt_of_lt, Lean.Omega.Int.ofNat_sub_dichotomy, Lean.Omega.Int.ofNat_sub_sub, 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.coordinate_eval_3, Lean.Omega.LinearCombo.coordinate_eval_4, Lean.Omega.LinearCombo.coordinate_eval_5, Lean.Omega.LinearCombo.coordinate_eval_6, Lean.Omega.LinearCombo.coordinate_eval_7, Lean.Omega.LinearCombo.eval, Lean.Omega.LinearCombo.sub_eval, Lean.Omega.combo_sat', Lean.Omega.tidy_sat, Nat, Nat.add_assoc, Nat.add_lt_add_left, Nat.cast, Nat.le_of_not_lt, Nat.lt_or_gt_of_ne, Nonempty, Not, Or.elim, Prod, Unit, Unit.unit, congr, congrArg, congrFun', dif_neg, dif_pos, dite, dite_congr, funext, id, le_of_le_of_eq, of_decide_eq_true, rfl
Used by: Component.Hom.hexagon_reverse
Component.Hom.hexagon_forward
theorem Component.Hom.hexagon_forward {Wire : Type} [Nonempty Wire] [Norm Wire] (X Y Z : ℕ) : ((Component.Hom.recast ⋯ ⋯ (Component.Hom.id Wire (X + Y + Z))).comp (Component.Hom.symmetry Wire X (Y + Z))).comp (Component.Hom.recast ⋯ ⋯ (Component.Hom.id Wire (Y + Z + X))) = (((Component.Hom.symmetry Wire X Y).tensor (Component.Hom.id Wire Z)).comp (Component.Hom.recast ⋯ ⋯ (Component.Hom.id Wire (Y + X + Z)))).comp ((Component.Hom.id Wire Y).tensor (Component.Hom.symmetry Wire X Z))
Show details
fun {Wire} [Nonempty Wire] [Norm Wire] X Y Z => Quotient.sound (Component.hexagon_forward_arrow X Y Z)
Complexity: 14161 (size of the value term)
Dependencies: Component.Hom, Component.Hom.comp, Component.Hom.id, Component.Hom.recast, Component.Hom.symmetry, Component.Hom.tensor
Proof dependencies: Component.Arrow, Component.Arrow.setoid, Component.hexagon_forward_arrow, Component.id, Component.parallel, Component.recast, Component.sequential, Component.symmetry, instNormProd_computerNetworks, instNormUnit_computerNetworks
Mathlib dependencies: Norm
Lean core dependencies: Eq, Nat, Nat.add_assoc, Nonempty, Prod, Quotient.sound, Unit, Unit.unit, inferInstance, rfl
Used by: Component.braidedCategory
Component.Hom.hexagon_reverse
theorem Component.Hom.hexagon_reverse {Wire : Type} [Nonempty Wire] [Norm Wire] (X Y Z : ℕ) : ((Component.Hom.recast ⋯ ⋯ (Component.Hom.id Wire (X + (Y + Z)))).comp (Component.Hom.symmetry Wire (X + Y) Z)).comp (Component.Hom.recast ⋯ ⋯ (Component.Hom.id Wire (Z + (X + Y)))) = (((Component.Hom.id Wire X).tensor (Component.Hom.symmetry Wire Y Z)).comp (Component.Hom.recast ⋯ ⋯ (Component.Hom.id Wire (X + (Z + Y))))).comp ((Component.Hom.symmetry Wire X Z).tensor (Component.Hom.id Wire Y))
Show details
fun {Wire} [Nonempty Wire] [Norm Wire] X Y Z => Quotient.sound (Component.hexagon_reverse_arrow X Y Z)
Complexity: 14377 (size of the value term)
Dependencies: Component.Hom, Component.Hom.comp, Component.Hom.id, Component.Hom.recast, Component.Hom.symmetry, Component.Hom.tensor
Proof dependencies: Component.Arrow, Component.Arrow.setoid, Component.hexagon_reverse_arrow, Component.id, Component.parallel, Component.recast, Component.sequential, Component.symmetry, instNormProd_computerNetworks, instNormUnit_computerNetworks
Mathlib dependencies: Norm
Lean core dependencies: Eq, Eq.symm, Nat, Nat.add_assoc, Nonempty, Prod, Quotient.sound, Unit, Unit.unit, inferInstance, rfl
Used by: Component.braidedCategory
Component.braidedCategory
def Component.braidedCategory (Wire : Type) [Nonempty Wire] [Norm Wire] : CategoryTheory.BraidedCategory ℕ
Show details
| Component.braidedCategory Wire = { braiding := Component.braiding Wire, braiding_naturality_right := ⋯, braiding_naturality_left := ⋯, hexagon_forward := ⋯, hexagon_reverse := ⋯ }
Complexity: 145 (size of the value term)
Outer dependencies: Component.category, Component.monoidalCategory
Inner dependencies: Component.Hom, Component.Hom.comp, Component.Hom.comp_assoc, Component.Hom.eqToHom_eq_recast_id, Component.Hom.hexagon_forward, Component.Hom.hexagon_reverse, Component.Hom.id, Component.Hom.recast, Component.Hom.tensor, Component.braiding, Component.braiding_naturality_left, Component.braiding_naturality_right
Mathlib dependencies: CategoryTheory.BraidedCategory, CategoryTheory.eqToHom, CategoryTheory.eqToIso, CategoryTheory.eqToIso.hom, CategoryTheory.eqToIso.inv, Norm
Used by: instBraidedCategoryPROP
Component.PROP
def Component.PROP (Wire : Type) [Nonempty Wire] [Norm Wire] : Type
Show details
| Component.PROP Wire = ℕ
Complexity: 11 (size of the value term)
Outer dependencies: (none)
Mathlib dependencies: Norm
instCategoryPROP
instance instCategoryPROP {Wire : Type} [Nonempty Wire] [Norm Wire] : CategoryTheory.Category.{1, 0} (Component.PROP Wire)
Show details
| instCategoryPROP = Component.category Wire
Complexity: 17 (size of the value term)
Outer dependencies: Component.PROP
Inner dependencies: Component.category
Mathlib dependencies: CategoryTheory.Category, Norm
Lean core dependencies: Nonempty
instMonoidalCategoryPROP
instance instMonoidalCategoryPROP {Wire : Type} [Nonempty Wire] [Norm Wire] : CategoryTheory.MonoidalCategory (Component.PROP Wire)
Show details
| instMonoidalCategoryPROP = Component.monoidalCategory Wire
Complexity: 17 (size of the value term)
Outer dependencies: Component.PROP, instCategoryPROP
Inner dependencies: Component.monoidalCategory
Mathlib dependencies: CategoryTheory.MonoidalCategory, Norm
Lean core dependencies: Nonempty
Used by: instBraidedCategoryPROP
instBraidedCategoryPROP
instance instBraidedCategoryPROP {Wire : Type} [Nonempty Wire] [Norm Wire] : CategoryTheory.BraidedCategory (Component.PROP Wire)
Show details
| instBraidedCategoryPROP = Component.braidedCategory Wire
Complexity: 17 (size of the value term)
Outer dependencies: Component.PROP, instCategoryPROP, instMonoidalCategoryPROP
Inner dependencies: Component.braidedCategory
Mathlib dependencies: CategoryTheory.BraidedCategory, Norm
Lean core dependencies: Nonempty
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.