Feedback
Difficulty: hard — 4 definitions, 0 abbreviations, 1 lemmas, 6 theorems, 0 examples.
definition lemma theorem
legend
Note
Layer.trace
Layer.trace {I J K : InterfaceOld} (f : Layer (I.tensor K) (J.tensor K)) : Layer I J
Show details
fun {I J K} f v => ∃ w, f ((v.left.join w).join (v.right.join w))
Complexity: 85 (size of the value term)
Outer dependencies: InterfaceOld, InterfaceOld.tensor, Layer
Inner dependencies: InterfaceOld.Value, InterfaceOld.Value.join, InterfaceOld.Value.left, InterfaceOld.Value.right
Lean core dependencies: Exists
Note
Layer.loop
Layer.loop {K : InterfaceOld} (f : Layer K K) : Layer InterfaceOld.unit InterfaceOld.unit
Show details
fun {K} f x => ∃ w, f.rel w w
Complexity: 37 (size of the value term)
Outer dependencies: InterfaceOld, InterfaceOld.unit, Layer
Inner dependencies: InterfaceOld.Value, InterfaceOld.tensor, Layer.rel
Lean core dependencies: Exists
Used by: Layer.trace_yanking
Note
Layer.symmetry
Layer.symmetry (I J : InterfaceOld) : Layer (I.tensor J) (J.tensor I)
Show details
fun I J v => v.left.left = v.right.right ∧ v.left.right = v.right.left
Complexity: 121 (size of the value term)
Outer dependencies: InterfaceOld, InterfaceOld.tensor, Layer
Inner dependencies: InterfaceOld.Value, InterfaceOld.Value.left, InterfaceOld.Value.right
Used by: Layer.trace_yanking
Important
Layer.trace_naturality_left
Layer.trace_naturality_left {I I' J K : InterfaceOld} (g : Layer I' I) (f : Layer (I.tensor K) (J.tensor K)) : g.sequential f.trace = ((g.parallel (Layer.id K)).sequential f).trace
Show details
fun {I I' J K} g f => funext fun v => Eq.mpr (id (congr (congrArg Eq (congrArg Exists (funext fun w => congrArg (And (g (v.left.join w))) (congrArg Exists (funext fun w_1 => congrArg f (congr (congrArg InterfaceOld.Value.join (congrFun' (congrArg InterfaceOld.Value.join (InterfaceOld.Value.left_join w v.right)) w_1)) (congrFun' (congrArg InterfaceOld.Value.join (InterfaceOld.Value.right_join w v.right)) w_1))))))) (congrArg Exists (funext fun w => congrArg Exists (funext fun w_1 => congr (congrArg And (congr (congrArg And (congrArg g (congr (congrArg InterfaceOld.Value.join (Eq.trans (congrArg InterfaceOld.Value.left (Eq.trans (congrArg InterfaceOld.Value.left (congrFun' (congrArg InterfaceOld.Value.join (InterfaceOld.Value.left_join (v.left.join w) (v.right.join w))) w_1)) (InterfaceOld.Value.left_join (v.left.join w) w_1))) (InterfaceOld.Value.left_join v.left w))) (congrArg InterfaceOld.Value.left (Eq.trans (congrArg InterfaceOld.Value.right (congrFun' (congrArg InterfaceOld.Value.join (InterfaceOld.Value.left_join (v.left.join w) (v.right.join w))) w_1)) (InterfaceOld.Value.right_join (v.left.join w) w_1)))))) (congr (congrArg Eq (Eq.trans (congrArg InterfaceOld.Value.left (congr (congrArg InterfaceOld.Value.join (Eq.trans (congrArg InterfaceOld.Value.right (Eq.trans (congrArg InterfaceOld.Value.left (congrFun' (congrArg InterfaceOld.Value.join (InterfaceOld.Value.left_join (v.left.join w) (v.right.join w))) w_1)) (InterfaceOld.Value.left_join (v.left.join w) w_1))) (InterfaceOld.Value.right_join v.left w))) (congrArg InterfaceOld.Value.right (Eq.trans (congrArg InterfaceOld.Value.right (congrFun' (congrArg InterfaceOld.Value.join (InterfaceOld.Value.left_join (v.left.join w) (v.right.join w))) w_1)) (InterfaceOld.Value.right_join (v.left.join w) w_1))))) (InterfaceOld.Value.left_join w w_1.right))) (Eq.trans (congrArg InterfaceOld.Value.right (congr (congrArg InterfaceOld.Value.join (Eq.trans (congrArg InterfaceOld.Value.right (Eq.trans (congrArg InterfaceOld.Value.left (congrFun' (congrArg InterfaceOld.Value.join (InterfaceOld.Value.left_join (v.left.join w) (v.right.join w))) w_1)) (InterfaceOld.Value.left_join (v.left.join w) w_1))) (InterfaceOld.Value.right_join v.left w))) (congrArg InterfaceOld.Value.right (Eq.trans (congrArg InterfaceOld.Value.right (congrFun' (congrArg InterfaceOld.Value.join (InterfaceOld.Value.left_join (v.left.join w) (v.right.join w))) w_1)) (InterfaceOld.Value.right_join (v.left.join w) w_1))))) (InterfaceOld.Value.right_join w w_1.right))))) (congrArg f (congrArg w_1.join (InterfaceOld.Value.right_join (v.left.join w) (v.right.join w))))))))) (propext { mp := fun a => Exists.casesOn a fun i h => And.casesOn h fun hg right => Exists.casesOn right fun w hf => Exists.intro w (Exists.intro (i.join w) ⟨⟨Eq.mpr (id (congrArg g (congrArg v.left.join (InterfaceOld.Value.left_join i w)))) hg, of_eq_true (Eq.trans (congrArg (Eq w) (InterfaceOld.Value.right_join i w)) (eq_self w))⟩, hf⟩), mpr := fun a => Exists.casesOn a fun w h => Exists.casesOn h fun mid h => And.casesOn h fun left hf => And.casesOn left fun hg hid => Exists.intro mid.left ⟨hg, Exists.intro w (have heq := Eq.mpr (id (congrArg (fun _a => mid.left.join _a = mid) hid)) (Eq.mpr (id (congrArg (fun _a => _a = mid) (InterfaceOld.Value.join_left_right mid))) (Eq.refl mid)); Eq.mpr (id (congrArg (fun _a => f (_a.join (v.right.join w))) heq)) hf)⟩ })
Complexity: 17082 (size of the value term)
Dependencies: InterfaceOld, InterfaceOld.tensor, Layer, Layer.id, Layer.parallel, Layer.sequential, Layer.trace
Proof dependencies: InterfaceOld.Value, InterfaceOld.Value.join, InterfaceOld.Value.join_left_right, InterfaceOld.Value.left, InterfaceOld.Value.left_join, InterfaceOld.Value.right, InterfaceOld.Value.right_join
Lean core dependencies: And, Eq, Eq.mpr, Eq.trans, Exists, True, congr, congrArg, congrFun', eq_self, funext, id, of_eq_true
Used by: (none)
Important
Layer.trace_naturality_right
Layer.trace_naturality_right {I J J' K : InterfaceOld} (f : Layer (I.tensor K) (J.tensor K)) (h : Layer J J') : f.trace.sequential h = (f.sequential (h.parallel (Layer.id K))).trace
Show details
fun {I J J' K} f h => funext fun v => Eq.mpr (id (congr (congrArg Eq (congrArg Exists (funext fun w => congrFun' (congrArg And (congrArg Exists (funext fun w_1 => congrArg f (congr (congrArg InterfaceOld.Value.join (congrFun' (congrArg InterfaceOld.Value.join (InterfaceOld.Value.left_join v.left w)) w_1)) (congrFun' (congrArg InterfaceOld.Value.join (InterfaceOld.Value.right_join v.left w)) w_1))))) (h (w.join v.right))))) (congrArg Exists (funext fun w => congrArg Exists (funext fun w_1 => congr (congrArg And (congrArg f (congrFun' (congrArg InterfaceOld.Value.join (InterfaceOld.Value.left_join (v.left.join w) (v.right.join w))) w_1))) (congr (congrArg And (congrArg h (congr (congrArg InterfaceOld.Value.join (congrArg InterfaceOld.Value.left (Eq.trans (congrArg InterfaceOld.Value.left (congrArg w_1.join (InterfaceOld.Value.right_join (v.left.join w) (v.right.join w)))) (InterfaceOld.Value.left_join w_1 (v.right.join w))))) (Eq.trans (congrArg InterfaceOld.Value.left (Eq.trans (congrArg InterfaceOld.Value.right (congrArg w_1.join (InterfaceOld.Value.right_join (v.left.join w) (v.right.join w)))) (InterfaceOld.Value.right_join w_1 (v.right.join w)))) (InterfaceOld.Value.left_join v.right w))))) (congr (congrArg Eq (Eq.trans (congrArg InterfaceOld.Value.left (congr (congrArg InterfaceOld.Value.join (congrArg InterfaceOld.Value.right (Eq.trans (congrArg InterfaceOld.Value.left (congrArg w_1.join (InterfaceOld.Value.right_join (v.left.join w) (v.right.join w)))) (InterfaceOld.Value.left_join w_1 (v.right.join w))))) (Eq.trans (congrArg InterfaceOld.Value.right (Eq.trans (congrArg InterfaceOld.Value.right (congrArg w_1.join (InterfaceOld.Value.right_join (v.left.join w) (v.right.join w)))) (InterfaceOld.Value.right_join w_1 (v.right.join w)))) (InterfaceOld.Value.right_join v.right w)))) (InterfaceOld.Value.left_join w_1.right w))) (Eq.trans (congrArg InterfaceOld.Value.right (congr (congrArg InterfaceOld.Value.join (congrArg InterfaceOld.Value.right (Eq.trans (congrArg InterfaceOld.Value.left (congrArg w_1.join (InterfaceOld.Value.right_join (v.left.join w) (v.right.join w)))) (InterfaceOld.Value.left_join w_1 (v.right.join w))))) (Eq.trans (congrArg InterfaceOld.Value.right (Eq.trans (congrArg InterfaceOld.Value.right (congrArg w_1.join (InterfaceOld.Value.right_join (v.left.join w) (v.right.join w)))) (InterfaceOld.Value.right_join w_1 (v.right.join w)))) (InterfaceOld.Value.right_join v.right w)))) (InterfaceOld.Value.right_join w_1.right w))))))))) (propext { mp := fun a => Exists.casesOn a fun j h_1 => And.casesOn h_1 fun left hh => Exists.casesOn left fun w hf => Exists.intro w (Exists.intro (j.join w) ⟨hf, ⟨Eq.mpr (id (congrArg h (congrFun' (congrArg InterfaceOld.Value.join (InterfaceOld.Value.left_join j w)) v.right))) hh, of_eq_true (Eq.trans (congrFun' (congrArg Eq (InterfaceOld.Value.right_join j w)) w) (eq_self w))⟩⟩), mpr := fun a => Exists.casesOn a fun w h_1 => Exists.casesOn h_1 fun mid h_2 => And.casesOn h_2 fun hf right => And.casesOn right fun hh hid => Exists.intro mid.left ⟨Exists.intro w (have heq := Eq.mpr (id (congrArg (fun _a => mid.left.join _a = mid) (Eq.symm hid))) (Eq.mpr (id (congrArg (fun _a => _a = mid) (InterfaceOld.Value.join_left_right mid))) (Eq.refl mid)); Eq.mpr (id (congrArg (fun _a => f ((v.left.join w).join _a)) heq)) hf), hh⟩ })
Complexity: 16590 (size of the value term)
Dependencies: InterfaceOld, InterfaceOld.tensor, Layer, Layer.id, Layer.parallel, Layer.sequential, Layer.trace
Proof dependencies: InterfaceOld.Value, InterfaceOld.Value.join, InterfaceOld.Value.join_left_right, InterfaceOld.Value.left, InterfaceOld.Value.left_join, InterfaceOld.Value.right, InterfaceOld.Value.right_join
Lean core dependencies: And, Eq, Eq.mpr, Eq.symm, Eq.trans, Exists, True, congr, congrArg, congrFun', eq_self, funext, id, of_eq_true
Used by: (none)
Important
Layer.trace_vanishing
Layer.trace_vanishing {I J : InterfaceOld} (f : Layer I J) : (f.parallel (Layer.id InterfaceOld.unit)).trace = f
Show details
fun {I J} f => funext fun v => Eq.mpr (id (congrFun' (congrArg Eq (congrArg Exists (funext fun w => congr (congrArg And (congrArg f (congr (congrArg InterfaceOld.Value.join (Eq.trans (congrArg InterfaceOld.Value.left (InterfaceOld.Value.left_join (v.left.join w) (v.right.join w))) (InterfaceOld.Value.left_join v.left w))) (Eq.trans (congrArg InterfaceOld.Value.left (InterfaceOld.Value.right_join (v.left.join w) (v.right.join w))) (InterfaceOld.Value.left_join v.right w))))) (Eq.trans (congr (congrArg Eq (Eq.trans (congrArg InterfaceOld.Value.left (congr (congrArg InterfaceOld.Value.join (Eq.trans (congrArg InterfaceOld.Value.right (InterfaceOld.Value.left_join (v.left.join w) (v.right.join w))) (InterfaceOld.Value.right_join v.left w))) (Eq.trans (congrArg InterfaceOld.Value.right (InterfaceOld.Value.right_join (v.left.join w) (v.right.join w))) (InterfaceOld.Value.right_join v.right w)))) (InterfaceOld.Value.left_join w w))) (Eq.trans (congrArg InterfaceOld.Value.right (congr (congrArg InterfaceOld.Value.join (Eq.trans (congrArg InterfaceOld.Value.right (InterfaceOld.Value.left_join (v.left.join w) (v.right.join w))) (InterfaceOld.Value.right_join v.left w))) (Eq.trans (congrArg InterfaceOld.Value.right (InterfaceOld.Value.right_join (v.left.join w) (v.right.join w))) (InterfaceOld.Value.right_join v.right w)))) (InterfaceOld.Value.right_join w w))) (eq_self w))))) (f v))) (propext { mp := fun a => Exists.casesOn a fun w h => And.casesOn h fun hf right => Eq.mp (congrArg (fun _a => f _a) (InterfaceOld.Value.join_left_right v)) hf, mpr := fun hf => Exists.intro (Classical.arbitrary InterfaceOld.unit.Value) ⟨Eq.mpr (id (congrArg (fun _a => f _a) (InterfaceOld.Value.join_left_right v))) hf, trivial⟩ })
Complexity: 5927 (size of the value term)
Dependencies: InterfaceOld, InterfaceOld.unit, Layer, Layer.id, Layer.parallel, Layer.trace
Proof dependencies: InterfaceOld.Value, InterfaceOld.Value.join, InterfaceOld.Value.join_left_right, InterfaceOld.Value.left, InterfaceOld.Value.left_join, InterfaceOld.Value.right, InterfaceOld.Value.right_join, InterfaceOld.tensor, instNonemptyValue
Mathlib dependencies: Classical.arbitrary
Lean core dependencies: And, Eq, Eq.mp, Eq.mpr, Eq.trans, Exists, True, congr, congrArg, congrFun', eq_self, funext, id, trivial
Used by: (none)
Tip
InterfaceOld.unit.Value.subsingleton
InterfaceOld.unit.Value.subsingleton : Subsingleton InterfaceOld.unit.Value
Show details
{ allEq := fun a b => InterfaceOld.Value.eq_of_heq (Eq.mpr (id (congrArg (fun _a => _a = b.fired) (Finset.eq_empty_of_isEmpty a.fired))) (Eq.mpr (id (congrArg (fun _a => ∅ = _a) (Finset.eq_empty_of_isEmpty b.fired))) (Eq.refl ∅))) (Function.hfunext (Eq.mpr (id (congrArg (fun _a => ↥_a = ↥b.fired) (Finset.eq_empty_of_isEmpty a.fired))) (Eq.mpr (id (congrArg (fun _a => ↥∅ = ↥_a) (Finset.eq_empty_of_isEmpty b.fired))) (Eq.refl ↥∅))) fun p a' a_1 => absurd p.property (of_eq_true (Eq.trans (congrArg Not (Eq.trans (congrFun' (congrArg Membership.mem (Finset.eq_empty_of_isEmpty a.fired)) ↑p) (Finset.notMem_empty._simp_1 ↑p))) not_false_eq_true))) }
Complexity: 3183 (size of the value term)
Dependencies: InterfaceOld.Value, InterfaceOld.unit
Proof dependencies: InterfaceOld.Value.eq_of_heq
Mathlib dependencies: Finset, Finset.eq_empty_of_isEmpty, Function.hfunext
Lean core dependencies: Eq, Eq.mpr, Eq.trans, False, HEq, Not, Subsingleton, Subtype, True, absurd, congrArg, congrFun', id, not_false_eq_true, of_eq_true
Used by: Layer.trace_yanking
Important
Layer.trace_yanking
Layer.trace_yanking (K : InterfaceOld) : (Layer.symmetry K K).loop = Layer.id InterfaceOld.unit
Show details
fun K => funext fun v => Eq.mpr (id (congrFun' (congrArg Eq (congrArg Exists (funext fun w => Layer.symmetry.eq_1 K K (w.join w)))) (v.left = v.right))) (propext { mp := fun a => Subsingleton.allEq v.left v.right, mpr := fun a => Exists.intro ((Classical.arbitrary K.Value).join (Classical.arbitrary K.Value)) ⟨of_eq_true (Eq.trans (congr (congrArg Eq (Eq.trans (congrArg InterfaceOld.Value.left (InterfaceOld.Value.left_join ((Classical.arbitrary K.Value).join (Classical.arbitrary K.Value)) ((Classical.arbitrary K.Value).join (Classical.arbitrary K.Value)))) (InterfaceOld.Value.left_join (Classical.arbitrary K.Value) (Classical.arbitrary K.Value)))) (Eq.trans (congrArg InterfaceOld.Value.right (InterfaceOld.Value.right_join ((Classical.arbitrary K.Value).join (Classical.arbitrary K.Value)) ((Classical.arbitrary K.Value).join (Classical.arbitrary K.Value)))) (InterfaceOld.Value.right_join (Classical.arbitrary K.Value) (Classical.arbitrary K.Value)))) (eq_self (Classical.arbitrary K.Value))), of_eq_true (Eq.trans (congr (congrArg Eq (Eq.trans (congrArg InterfaceOld.Value.right (InterfaceOld.Value.left_join ((Classical.arbitrary K.Value).join (Classical.arbitrary K.Value)) ((Classical.arbitrary K.Value).join (Classical.arbitrary K.Value)))) (InterfaceOld.Value.right_join (Classical.arbitrary K.Value) (Classical.arbitrary K.Value)))) (Eq.trans (congrArg InterfaceOld.Value.left (InterfaceOld.Value.right_join ((Classical.arbitrary K.Value).join (Classical.arbitrary K.Value)) ((Classical.arbitrary K.Value).join (Classical.arbitrary K.Value)))) (InterfaceOld.Value.left_join (Classical.arbitrary K.Value) (Classical.arbitrary K.Value)))) (eq_self (Classical.arbitrary K.Value)))⟩ })
Complexity: 5549 (size of the value term)
Dependencies: InterfaceOld, InterfaceOld.tensor, InterfaceOld.unit, Layer, Layer.id, Layer.loop, Layer.symmetry
Proof dependencies: InterfaceOld.Value, InterfaceOld.Value.join, InterfaceOld.Value.left, InterfaceOld.Value.left_join, InterfaceOld.Value.right, InterfaceOld.Value.right_join, InterfaceOld.unit.Value.subsingleton, Layer.rel, instNonemptyValue
Mathlib dependencies: Classical.arbitrary
Lean core dependencies: And, Eq, Eq.mpr, Eq.trans, Exists, True, congr, congrArg, congrFun', eq_self, funext, id, of_eq_true
Used by: (none)
Important
Layer.trace_sliding
Layer.trace_sliding {I J K : InterfaceOld} (f : Layer (I.tensor K) (J.tensor K)) (g : Layer K K) : (f.sequential ((Layer.id J).parallel g)).trace = (((Layer.id I).parallel g).sequential f).trace
Show details
fun {I J K} f g => funext fun v => Eq.mpr (id (congr (congrArg Eq (congrArg Exists (funext fun w => congrArg Exists (funext fun w_1 => congr (congrArg And (congrArg f (congrFun' (congrArg InterfaceOld.Value.join (InterfaceOld.Value.left_join (v.left.join w) (v.right.join w))) w_1))) (congr (congrArg And (congr (congrArg Eq (Eq.trans (congrArg InterfaceOld.Value.left (congr (congrArg InterfaceOld.Value.join (congrArg InterfaceOld.Value.left (Eq.trans (congrArg InterfaceOld.Value.left (congrArg w_1.join (InterfaceOld.Value.right_join (v.left.join w) (v.right.join w)))) (InterfaceOld.Value.left_join w_1 (v.right.join w))))) (Eq.trans (congrArg InterfaceOld.Value.left (Eq.trans (congrArg InterfaceOld.Value.right (congrArg w_1.join (InterfaceOld.Value.right_join (v.left.join w) (v.right.join w)))) (InterfaceOld.Value.right_join w_1 (v.right.join w)))) (InterfaceOld.Value.left_join v.right w)))) (InterfaceOld.Value.left_join w_1.left v.right))) (Eq.trans (congrArg InterfaceOld.Value.right (congr (congrArg InterfaceOld.Value.join (congrArg InterfaceOld.Value.left (Eq.trans (congrArg InterfaceOld.Value.left (congrArg w_1.join (InterfaceOld.Value.right_join (v.left.join w) (v.right.join w)))) (InterfaceOld.Value.left_join w_1 (v.right.join w))))) (Eq.trans (congrArg InterfaceOld.Value.left (Eq.trans (congrArg InterfaceOld.Value.right (congrArg w_1.join (InterfaceOld.Value.right_join (v.left.join w) (v.right.join w)))) (InterfaceOld.Value.right_join w_1 (v.right.join w)))) (InterfaceOld.Value.left_join v.right w)))) (InterfaceOld.Value.right_join w_1.left v.right)))) (congrArg g (congr (congrArg InterfaceOld.Value.join (congrArg InterfaceOld.Value.right (Eq.trans (congrArg InterfaceOld.Value.left (congrArg w_1.join (InterfaceOld.Value.right_join (v.left.join w) (v.right.join w)))) (InterfaceOld.Value.left_join w_1 (v.right.join w))))) (Eq.trans (congrArg InterfaceOld.Value.right (Eq.trans (congrArg InterfaceOld.Value.right (congrArg w_1.join (InterfaceOld.Value.right_join (v.left.join w) (v.right.join w)))) (InterfaceOld.Value.right_join w_1 (v.right.join w)))) (InterfaceOld.Value.right_join v.right w))))))))) (congrArg Exists (funext fun w => congrArg Exists (funext fun w_1 => congr (congrArg And (congr (congrArg And (congr (congrArg Eq (Eq.trans (congrArg InterfaceOld.Value.left (congr (congrArg InterfaceOld.Value.join (Eq.trans (congrArg InterfaceOld.Value.left (Eq.trans (congrArg InterfaceOld.Value.left (congrFun' (congrArg InterfaceOld.Value.join (InterfaceOld.Value.left_join (v.left.join w) (v.right.join w))) w_1)) (InterfaceOld.Value.left_join (v.left.join w) w_1))) (InterfaceOld.Value.left_join v.left w))) (congrArg InterfaceOld.Value.left (Eq.trans (congrArg InterfaceOld.Value.right (congrFun' (congrArg InterfaceOld.Value.join (InterfaceOld.Value.left_join (v.left.join w) (v.right.join w))) w_1)) (InterfaceOld.Value.right_join (v.left.join w) w_1))))) (InterfaceOld.Value.left_join v.left w_1.left))) (Eq.trans (congrArg InterfaceOld.Value.right (congr (congrArg InterfaceOld.Value.join (Eq.trans (congrArg InterfaceOld.Value.left (Eq.trans (congrArg InterfaceOld.Value.left (congrFun' (congrArg InterfaceOld.Value.join (InterfaceOld.Value.left_join (v.left.join w) (v.right.join w))) w_1)) (InterfaceOld.Value.left_join (v.left.join w) w_1))) (InterfaceOld.Value.left_join v.left w))) (congrArg InterfaceOld.Value.left (Eq.trans (congrArg InterfaceOld.Value.right (congrFun' (congrArg InterfaceOld.Value.join (InterfaceOld.Value.left_join (v.left.join w) (v.right.join w))) w_1)) (InterfaceOld.Value.right_join (v.left.join w) w_1))))) (InterfaceOld.Value.right_join v.left w_1.left)))) (congrArg g (congr (congrArg InterfaceOld.Value.join (Eq.trans (congrArg InterfaceOld.Value.right (Eq.trans (congrArg InterfaceOld.Value.left (congrFun' (congrArg InterfaceOld.Value.join (InterfaceOld.Value.left_join (v.left.join w) (v.right.join w))) w_1)) (InterfaceOld.Value.left_join (v.left.join w) w_1))) (InterfaceOld.Value.right_join v.left w))) (congrArg InterfaceOld.Value.right (Eq.trans (congrArg InterfaceOld.Value.right (congrFun' (congrArg InterfaceOld.Value.join (InterfaceOld.Value.left_join (v.left.join w) (v.right.join w))) w_1)) (InterfaceOld.Value.right_join (v.left.join w) w_1))))))) (congrArg f (congrArg w_1.join (InterfaceOld.Value.right_join (v.left.join w) (v.right.join w))))))))) (propext { mp := fun a => Exists.casesOn a fun w h => Exists.casesOn h fun mid h => And.casesOn h fun hf hg => And.casesOn hg fun hw hg2 => Exists.intro mid.right (Exists.intro (v.left.join w) ⟨⟨of_eq_true (Eq.trans (congrArg (Eq v.left) (InterfaceOld.Value.left_join v.left w)) (eq_self v.left)), Eq.mpr (id (congrArg g (congrArg mid.right.join (InterfaceOld.Value.right_join v.left w)))) hg2⟩, have heq := Eq.mpr (id (congrArg (fun _a => _a.join mid.right = mid) (Eq.symm hw))) (Eq.mpr (id (congrArg (fun _a => _a = mid) (InterfaceOld.Value.join_left_right mid))) (Eq.refl mid)); Eq.mpr (id (congrArg (fun _a => f ((v.left.join w).join _a)) heq)) hf⟩), mpr := fun a => Exists.casesOn a fun w h => Exists.casesOn h fun mid h => And.casesOn h fun hg hf => And.casesOn hg fun hw hg2 => Exists.intro mid.right (Exists.intro (v.right.join w) ⟨have heq := Eq.mpr (id (congrArg (fun _a => _a.join mid.right = mid) hw)) (Eq.mpr (id (congrArg (fun _a => _a = mid) (InterfaceOld.Value.join_left_right mid))) (Eq.refl mid)); Eq.mpr (id (congrArg (fun _a => f (_a.join (v.right.join w))) heq)) hf, ⟨of_eq_true (Eq.trans (congrFun' (congrArg Eq (InterfaceOld.Value.left_join v.right w)) v.right) (eq_self v.right)), Eq.mpr (id (congrArg g (congrFun' (congrArg InterfaceOld.Value.join (InterfaceOld.Value.right_join v.right w)) mid.right))) hg2⟩⟩) })
Complexity: 28119 (size of the value term)
Dependencies: InterfaceOld, InterfaceOld.tensor, Layer, Layer.id, Layer.parallel, Layer.sequential, Layer.trace
Proof dependencies: InterfaceOld.Value, InterfaceOld.Value.join, InterfaceOld.Value.join_left_right, InterfaceOld.Value.left, InterfaceOld.Value.left_join, InterfaceOld.Value.right, InterfaceOld.Value.right_join
Lean core dependencies: And, Eq, Eq.mpr, Eq.symm, Eq.trans, Exists, True, congr, congrArg, congrFun', eq_self, funext, id, of_eq_true
Used by: (none)
Note
InterfaceOld.Value.assocLR
InterfaceOld.Value.assocLR {I J K : InterfaceOld} (v : (I.tensor (J.tensor K)).Value) : ((I.tensor J).tensor K).Value
Show details
fun {I J K} v => (v.left.join v.right.left).join v.right.right
Complexity: 81 (size of the value term)
Outer dependencies: InterfaceOld, InterfaceOld.Value, InterfaceOld.tensor
Inner dependencies: InterfaceOld.Value.join, InterfaceOld.Value.left, InterfaceOld.Value.right
Used by: Layer.trace_superposing
Important
Layer.trace_superposing
Layer.trace_superposing {I J K1 K2 : InterfaceOld} (f : Layer ((I.tensor K1).tensor K2) ((J.tensor K1).tensor K2)) : f.trace.trace = Layer.trace fun v => f (v.left.assocLR.join v.right.assocLR)
Show details
fun {I J K1 K2} f => funext fun v => Eq.mpr (id (congr (congrArg Eq (congrArg Exists (funext fun w => congrArg Exists (funext fun w_1 => congrArg f (congr (congrArg InterfaceOld.Value.join (congrFun' (congrArg InterfaceOld.Value.join (InterfaceOld.Value.left_join (v.left.join w) (v.right.join w))) w_1)) (congrFun' (congrArg InterfaceOld.Value.join (InterfaceOld.Value.right_join (v.left.join w) (v.right.join w))) w_1)))))) (congrArg Exists (funext fun w => congrArg f (congr (congrArg InterfaceOld.Value.join (congrArg InterfaceOld.Value.assocLR (InterfaceOld.Value.left_join (v.left.join w) (v.right.join w)))) (congrArg InterfaceOld.Value.assocLR (InterfaceOld.Value.right_join (v.left.join w) (v.right.join w)))))))) (propext { mp := fun a => Exists.casesOn a fun w1 h => Exists.casesOn h fun w2 hf => Exists.intro (w1.join w2) (have hi := id (of_eq_true (Eq.trans (congrFun' (congrArg Eq (congr (congrArg InterfaceOld.Value.join (congr (congrArg InterfaceOld.Value.join (InterfaceOld.Value.left_join v.left (w1.join w2))) (Eq.trans (congrArg InterfaceOld.Value.left (InterfaceOld.Value.right_join v.left (w1.join w2))) (InterfaceOld.Value.left_join w1 w2)))) (Eq.trans (congrArg InterfaceOld.Value.right (InterfaceOld.Value.right_join v.left (w1.join w2))) (InterfaceOld.Value.right_join w1 w2)))) ((v.left.join w1).join w2)) (eq_self ((v.left.join w1).join w2)))); have hj := id (of_eq_true (Eq.trans (congrFun' (congrArg Eq (congr (congrArg InterfaceOld.Value.join (congr (congrArg InterfaceOld.Value.join (InterfaceOld.Value.left_join v.right (w1.join w2))) (Eq.trans (congrArg InterfaceOld.Value.left (InterfaceOld.Value.right_join v.right (w1.join w2))) (InterfaceOld.Value.left_join w1 w2)))) (Eq.trans (congrArg InterfaceOld.Value.right (InterfaceOld.Value.right_join v.right (w1.join w2))) (InterfaceOld.Value.right_join w1 w2)))) ((v.right.join w1).join w2)) (eq_self ((v.right.join w1).join w2)))); Eq.mpr (id (congrArg (fun _a => f (_a.join (v.right.join (w1.join w2)).assocLR)) hi)) (Eq.mpr (id (congrArg (fun _a => f (((v.left.join w1).join w2).join _a)) hj)) hf)), mpr := fun a => Exists.casesOn a fun w hf => Exists.intro w.left (Exists.intro w.right (have hi := id (of_eq_true (Eq.trans (congrFun' (congrArg Eq (congr (congrArg InterfaceOld.Value.join (congr (congrArg InterfaceOld.Value.join (InterfaceOld.Value.left_join v.left w)) (congrArg InterfaceOld.Value.left (InterfaceOld.Value.right_join v.left w)))) (congrArg InterfaceOld.Value.right (InterfaceOld.Value.right_join v.left w)))) ((v.left.join w.left).join w.right)) (eq_self ((v.left.join w.left).join w.right)))); have hj := id (of_eq_true (Eq.trans (congrFun' (congrArg Eq (congr (congrArg InterfaceOld.Value.join (congr (congrArg InterfaceOld.Value.join (InterfaceOld.Value.left_join v.right w)) (congrArg InterfaceOld.Value.left (InterfaceOld.Value.right_join v.right w)))) (congrArg InterfaceOld.Value.right (InterfaceOld.Value.right_join v.right w)))) ((v.right.join w.left).join w.right)) (eq_self ((v.right.join w.left).join w.right)))); Eq.mp (congrArg (fun _a => f (((v.left.join w.left).join w.right).join _a)) hj) (Eq.mp (congrArg (fun _a => f (_a.join (v.right.join w).assocLR)) hi) hf))) })
Complexity: 16845 (size of the value term)
Dependencies: InterfaceOld, InterfaceOld.Value, InterfaceOld.Value.assocLR, InterfaceOld.Value.join, InterfaceOld.Value.left, InterfaceOld.Value.right, InterfaceOld.tensor, Layer, Layer.trace
Proof dependencies: InterfaceOld.Value.left_join, InterfaceOld.Value.right_join
Lean core dependencies: Eq, Eq.mp, Eq.mpr, Eq.trans, Exists, True, congr, congrArg, congrFun', eq_self, funext, id, of_eq_true
Used by: (none)
Dependency diagram
Drag to pan, Ctrl+scroll (or Cmd+scroll, or pinch on a touch screen) to zoom, click a node to jump to it.
definitionlemmatheoremdeclared elsewheredependencyproof dependency
legend