Skip to content

Import monlib4 formalization - #76

Merged
Vilin97 merged 64 commits into
mainfrom
import/monlib4
Jun 1, 2026
Merged

Import monlib4 formalization#76
Vilin97 merged 64 commits into
mainfrom
import/monlib4

Conversation

@Vilin97

@Vilin97 Vilin97 commented May 16, 2026

Copy link
Copy Markdown
Collaborator

Imported from https://github.com/themathqueen/monlib4.

Slug: monlib4
Toolchain target: leanprover/lean4:v4.30.0-rc2
Branch: import/monlib4 (auto-generated by scripts/import-formalization.sh)
Agent: claude using claude-opus-4-7 at effort max, exited with code 0.

Commits on this branch:

  • 8fddf55 Vendor monlib4 utility subset

Import notes (from agent)

monlib4 import notes

Upstream: https://github.com/themathqueen/monlib4 (Lean v4.21.0-rc3).
Target: Lean Pool, Lean v4.30.0-rc2 / Mathlib v4.30.0-rc2.
License: Apache-2.0 (compatible with Lean Pool).
Author: Monica Omar.

What was vendored

A small foundational subset that builds warning-free under Lean Pool's
toolchain. Twelve content files (plus directory indices and the entry
module):

  • Other/Sonia.lean — base-(b+1) divisibility tests, sum mod helpers
  • Preq/Set.lean — passthrough; upstream definitions are now in Mathlib
  • Preq/Ites.lean — star/coe/TensorProduct.map push-through ite
  • Preq/Finset.lean — sum-rotation / sum-comm lemmas over Finsets
  • Preq/Dite.lean — star/Mul/TensorProduct.tmul push-through dite
  • Preq/RCLikeLe.lean — ≤ / < characterisations on RCLike fields
  • LinearAlgebra/End.lean — minor LinearMap.comp_one / LinearMap.one_comp
  • LinearAlgebra/LinearMapOp.lean — LinearMap.op / LinearMap.unop
    through the multiplicative opposite, plus AlgEquiv.op_toLinearMap
  • LinearAlgebra/DirectSumFromTo.lean — directSumFromTo projection
    between summands of a dependent direct sum
  • LinearAlgebra/MySpec.lean — isUnit_comm, spectrum.comm for
    finite-dimensional endomorphisms
  • LinearAlgebra/Matrix/Conj.lean — entrywise matrix conjugate with
    postfix notation ᴴᵀ
  • LinearAlgebra/Matrix/Reshape.lean — Matrix.reshape linear
    equivalence between Mₙₓₘ(R) and n × m → R

What was excluded, and why

The upstream library is large (~100k LOC, 77 active modules) and was
written for Lean v4.21.0-rc3. Across nine Mathlib minor versions the
following Mathlib API changes propagated into the core stack and
required deeper porting work than fits a single autonomous import pass:

  • Submodule.isCompl_orthogonal_of_completeSpace and related orthogonal-
    complement projection lemmas (Submodule.linear_proj_add_linearProjOfIsCompl_eq_self,
    Submodule.orthogonalProjection_eq_linear_proj,
    linearProjOfIsCompl_idempotent) were renamed / split out. This blocks
    LinearAlgebra/IsProj'.lean, LinearAlgebra/Ips/MinimalProj.lean,
    LinearAlgebra/Ips/RankOne.lean and almost everything downstream.
  • Set.mapsTo' was renamed/removed, used in
    LinearAlgebra/InvariantSubmodule.lean.
  • Basis is now exposed under Module for many constructions, and
    Basis.ofVectorSpace was renamed. LinearAlgebra/TensorProduct/BasicLemmas.lean
    and LinearAlgebra/Ips/MulOp.lean rely on the old names.
  • PiLp 2 vs (i : ι) → B i instance handling changed; many
    NormedAddCommGroupOfRing instance definitions and simp rewrites
    in LinearAlgebra/Nacgor.lean and LinearAlgebra/PiStarOrderedRing.lean
    no longer apply.
  • StarAlgEquiv.toAlgEquiv, StarAlgEquiv.ofAlgEquiv,
    AlgEquiv.self_trans_symm, AlgEquiv.symm_trans_self are now in
    Mathlib with slightly different signatures, and
    Submodule.map_coe / Submodule.map_span rewrites no longer match
    in the bare-MulEquiv setting used in Preq/StarAlgEquiv.lean. Most of
    RepTheory/AutMat.lean, LinearAlgebra/IsReal.lean,
    LinearAlgebra/Coalgebra/MulOpposite.lean cascade from this.
  • Upstream relies heavily on set_option maxHeartbeats and
    set_option synthInstance.maxHeartbeats (29 occurrences in
    QuantumGraph/PiMat.lean alone), forbidden by lean-pool. The
    quantum-graph / quantum-set proofs would need to be split into much
    smaller lemmas to fit the default heartbeat budget.
  • Style-linter violations are extensive (long-line, λ vs fun,
    refine' vs refine, induction' vs induction with, isolated
    central dots, etc.); auto-rewriting these without breaking the
    underlying proofs is non-trivial across thousands of declarations.

Excluded modules

Every active upstream module other than the twelve listed above is
excluded for the reasons above. The dependency chain means that even
modules with relatively shallow breakage (e.g. LinearAlgebra/IsReal.lean)
cannot land before their imports are fixed. The largest blocks are the
QuantumGraph (8 modules) and QuantumSet (11 modules) subsystems and
the Ips inner-product-space machinery (13 modules), which together
constitute the namesake non-commutative-graph-theory content.

Toolchain bump

v4.21.0-rc3 → v4.30.0-rc2. Beyond the issues above, the only
mechanical sweep applied to the vendored subset was:

  • replace every import Monlib.… with import LeanPool.Monlib4.…
  • replace the upstream copyright header with the lean-pool header
    (year 2026, author preserved as Monica Omar, Apache-2.0)
  • strip set_option directives and diagnostic commands
    (#check/#print/#eval/#reduce/#guard_msgs/#lint)
  • swap renamed Mathlib imports (e.g.
    Mathlib.Data.Matrix.Kronecker → Mathlib.LinearAlgebra.Matrix.Kronecker,
    Mathlib.LinearAlgebra.Matrix.Spectrum → Mathlib.Analysis.Matrix.Spectrum,
    Mathlib.Topology.Algebra.Module.WeakDual → …Module.Spaces.WeakDual,
    Mathlib.Analysis.InnerProductSpace.Projection → …Projection.Basic,
    Mathlib.Data.Complex.Norm → Mathlib.Analysis.Complex.Norm)
  • add import Mathlib.LinearAlgebra.TensorProduct.Map where
    TensorProduct.map is used (it moved out of …TensorProduct.Basic)
  • add import Mathlib.Tactic.Cases where induction' / cases' are
    used (they live there now, not via a transitive default import)
  • per-file fixes: convert one induction' to induction … with in
    Other/Sonia.lean; drop @[simp, norm_cast] on four
    RCLike lemmas in Preq/RCLikeLe.lean (Mathlib's simp set already
    proves them); convert two refine' to refine ⟨_, ?_⟩ in
    LinearAlgebra/MySpec.lean; merge an isolated · and split a final
    exact into two bulleted goals in LinearAlgebra/MySpec.lean; drop
    redundant DecidableEq arguments on Matrix.Conj.conj_zero; reflow
    several over-100-char doc comments; wrap IsHermitian.conj in a
    nested namespace IsHermitian so the lean-pool axiom audit can find
    it.

Further porting work

Picking up where this stops would mean, in order:

  1. Fix the orthogonal-projection rename chain so
    LinearAlgebra/IsProj'.lean builds; this unlocks Ips/RankOne.lean,
    Ips/MinimalProj.lean, and most of LinearAlgebra/Matrix/*.
  2. Fix Preq/StarAlgEquiv.lean (delete the four declarations now in
    Mathlib; salvage NonUnitalAlgEquiv.image_span_center with the
    current Submodule.map_span/MulEquiv.image_center signatures).
  3. Fix LinearAlgebra/InvariantSubmodule.lean (Set.mapsTo' rename).
  4. Iterate up through LinearAlgebra/Nacgor.lean,
    LinearAlgebra/PiStarOrderedRing.lean,
    LinearAlgebra/QuantumSet/*, QuantumGraph/* — repairing
    heartbeats by splitting proofs into lemmas, and addressing
    style-linter regressions as each module lands.

Opened automatically by scripts/import-formalization.sh. Review the diff carefully before merging — the agent ran unattended.

@Vilin97
Vendor monlib4 utility subset
8fddf55 
Imports a foundational subset of themathqueen/monlib4 covering matrix reshape
and conjugate, direct-sum projection, finite-dim spectrum commutativity, and
helper lemmas (finite sums, ites/dites, RCLike order, base-(b+1) divisibility).
Bumped from Lean v4.21.0-rc3 to v4.30.0-rc2.
@github-actions

github-actions Bot commented May 16, 2026 •
edited
Loading

Copy link
Copy Markdown
Contributor

Proof profile (new / modified Lean files)

lake build LeanPool wall time: 643.92 s (= 10.73 min) — user 2100.79 s, sys 98.51 s.

This is the parallel build wall clock and is the compile-time answer for this PR. The serial per-file sums below are useful for ranking slow files, not as a build budget.

Total heartbeats: 395,189 maxHeartbeats units across 98 files (35,331 added LOC).

Sum of lean --profile: 1595644.7 ms (= 1595.64 s). Import-excluded time: 1426530.7 ms (= 1426.53 s).

Count-heartbeats wall-clock total: 891.10 s. Repeated import cost inside lean --profile: 169114.0 ms (= 169.11 s).

Heartbeat values come from Mathlib's linter.countHeartbeats and are already in maxHeartbeats units.

LOC counts added lines in the profiled Lean files from this PR diff.

File LOC Heartbeats (maxHB) Count wall (s) lean --profile (s) Without import (s) Import (s) Decls Errors
LeanPool/Monlib4/LinearAlgebra/QuantumSet/SchurMul.lean 423 156,920 33.26 41.04 39.30 1.74 26 0
LeanPool/Monlib4/QuantumGraph/PiMatFinTwo.lean 1,145 40,044 60.93 110.38 108.24 2.14 54 0
LeanPool/Monlib4/LinearAlgebra/PosMapIsReal.lean 1,207 23,730 21.14 48.86 46.83 2.03 76 0
LeanPool/Monlib4/LinearAlgebra/LmulRmul.lean 244 21,812 6.35 6.55 5.28 1.27 31 0
LeanPool/Monlib4/QuantumGraph/PiMat.lean 2,029 15,559 81.96 249.50 247.30 2.20 96 16
LeanPool/Monlib4/LinearAlgebra/IsReal.lean 247 11,557 5.00 5.14 3.65 1.49 24 0
LeanPool/Monlib4/LinearAlgebra/OfNorm.lean 757 10,249 9.21 16.10 14.40 1.70 57 0
LeanPool/Monlib4/LinearAlgebra/Ips/Pos.lean 582 10,095 9.51 14.00 12.27 1.73 40 0
LeanPool/Monlib4/LinearAlgebra/Ips/MatIps.lean 1,735 9,046 27.06 47.26 45.22 2.04 81 0
LeanPool/Monlib4/LinearAlgebra/Coalgebra/FiniteDimensional.lean 348 8,317 11.47 14.13 12.42 1.71 20 0
LeanPool/Monlib4/LinearAlgebra/TensorProduct/Submodule.lean 427 7,525 12.02 19.37 17.62 1.75 31 0
LeanPool/Monlib4/LinearAlgebra/Ips/MinimalProj.lean 1,073 6,530 10.71 21.23 19.50 1.73 72 0
LeanPool/Monlib4/QuantumGraph/Matrix.lean 1,015 5,771 40.38 87.04 84.88 2.16 47 0
LeanPool/Monlib4/LinearAlgebra/QuantumSet/TensorProduct.lean 232 5,014 9.52 11.89 10.17 1.72 15 0
LeanPool/Monlib4/LinearAlgebra/Ips/Strict.lean 180 4,918 3.44 3.29 2.12 1.17 34 0
LeanPool/Monlib4/LinearAlgebra/Ips/Nontracial.lean 1,255 4,784 22.68 40.91 38.88 2.03 26 0
LeanPool/Monlib4/QuantumGraph/Example.lean 397 4,670 10.34 19.11 17.00 2.11 46 0
LeanPool/Monlib4/LinearAlgebra/Ips/RankOne.lean 747 4,574 18.60 29.78 28.16 1.62 74 0
LeanPool/Monlib4/LinearAlgebra/Ips/TensorHilbert.lean 207 4,304 5.54 6.62 4.99 1.63 19 0
LeanPool/Monlib4/LinearAlgebra/Ips/Frob.lean 433 3,798 6.94 9.50 7.39 2.11 12 4
LeanPool/Monlib4/LinearAlgebra/QuantumSet/QIso.lean 532 3,735 29.14 61.09 59.33 1.76 31 4
LeanPool/Monlib4/LinearAlgebra/QuantumSet/Pi.lean 159 2,455 4.86 4.35 2.62 1.73 17 0
LeanPool/Monlib4/LinearAlgebra/InvariantSubmodule.lean 202 2,378 3.48 4.14 2.72 1.42 18 0
LeanPool/Monlib4/QuantumGraph/ToProjections.lean 918 2,092 22.89 41.06 38.91 2.15 48 6
LeanPool/Monlib4/LinearAlgebra/InnerAut.lean 748 2,029 10.98 20.43 18.39 2.04 95 0
LeanPool/Monlib4/QuantumGraph/QamA.lean 1,198 1,591 22.71 73.65 71.48 2.17 40 10
LeanPool/Monlib4/LinearAlgebra/QuantumSet/Instances.lean 820 1,555 9.96 17.19 15.16 2.03 30 0
LeanPool/Monlib4/QuantumGraph/Basic.lean 1,196 1,461 38.55 83.92 81.77 2.15 88 0
LeanPool/Monlib4/QuantumGraph/Iso.lean 438 1,425 11.09 23.87 21.74 2.13 21 0
LeanPool/Monlib4/LinearAlgebra/Ips/MulOp.lean 120 1,364 3.61 3.59 1.97 1.62 15 0
LeanPool/Monlib4/LinearAlgebra/PiStarOrderedRing.lean 131 1,245 2.36 2.05 0.90 1.15 10 0
LeanPool/Monlib4/LinearAlgebra/QuantumSet/Basic.lean 1,014 1,242 23.60 47.49 45.78 1.71 77 0
LeanPool/Monlib4/LinearAlgebra/QuantumSet/Subset.lean 579 1,076 11.49 16.04 14.29 1.75 53 0
LeanPool/Monlib4/LinearAlgebra/TensorProduct/BasicLemmas.lean 245 947 3.57 4.93 3.66 1.27 24 0
LeanPool/Monlib4/QuantumGraph/Nontracial.lean 303 904 7.44 12.88 10.67 2.21 14 0
LeanPool/Monlib4/LinearAlgebra/TensorProduct/FiniteDimensional.lean 250 877 11.42 12.28 10.62 1.66 8 0
LeanPool/Monlib4/LinearAlgebra/Ips/Functional.lean 1,005 850 7.45 16.39 14.31 2.08 47 0
LeanPool/Monlib4/LinearAlgebra/Matrix/Basic.lean 421 790 5.74 11.21 9.49 1.72 51 0
LeanPool/Monlib4/LinearAlgebra/MyBimodule.lean 362 697 4.40 6.29 4.93 1.36 43 0
LeanPool/Monlib4/LinearAlgebra/IsProj'.lean 93 694 3.22 2.77 1.17 1.60 11 0
LeanPool/Monlib4/LinearAlgebra/Coalgebra/Lemmas.lean 539 690 8.08 13.95 12.66 1.29 37 0
LeanPool/Monlib4/LinearAlgebra/Ips/Ips.lean 357 651 7.36 12.14 10.44 1.70 22 0
LeanPool/Monlib4/Preq/StarAlgEquiv.lean 268 459 3.14 3.30 2.09 1.21 29 0
LeanPool/Monlib4/QuantumGraph/QamAExample.lean 541 421 5.97 11.45 9.36 2.09 48 0
LeanPool/Monlib4/RepTheory/AutMat.lean 1,184 402 11.45 22.66 20.89 1.77 65 0
LeanPool/Monlib4/LinearAlgebra/Matrix/PosEqLinearMapIsPositive.lean 567 372 8.95 17.07 15.34 1.73 52 0
LeanPool/Monlib4/LinearAlgebra/ToMatrixOfEquiv.lean 326 354 8.23 11.11 9.05 2.06 34 0
LeanPool/Monlib4/LinearAlgebra/Ips/OpUnop.lean 105 295 2.40 2.01 0.73 1.28 16 0
LeanPool/Monlib4/LinearAlgebra/Matrix/IncludeBlock.lean 804 292 9.13 12.22 10.20 2.02 72 0
LeanPool/Monlib4/QuantumGraph/Degree.lean 507 281 10.59 28.71 26.60 2.11 35 0
LeanPool/Monlib4/Other/Sonia.lean 115 264 3.25 2.67 0.62 2.05 8 0
LeanPool/Monlib4/LinearAlgebra/KroneckerToTensor.lean 221 178 7.40 10.67 8.97 1.70 17 0
LeanPool/Monlib4/LinearAlgebra/Ips/Vn.lean 116 168 3.38 3.32 1.58 1.74 3 0
LeanPool/Monlib4/LinearAlgebra/Matrix/PosDefRpow.lean 243 156 5.06 6.28 4.26 2.02 26 0
LeanPool/Monlib4/LinearAlgebra/QuantumSet/Symm.lean 436 132 13.70 29.35 27.61 1.74 14 0
LeanPool/Monlib4/LinearAlgebra/PiDirectSum.lean 338 126 5.61 8.08 6.80 1.28 22 0
LeanPool/Monlib4/LinearAlgebra/Ips/Basic.lean 205 125 4.32 5.72 3.99 1.73 20 0
LeanPool/Monlib4/LinearAlgebra/Matrix/Spectra.lean 168 122 3.85 4.23 2.20 2.03 21 0
LeanPool/Monlib4/LinearAlgebra/TensorProduct/Lemmas.lean 171 122 3.52 4.22 2.94 1.28 15 0
LeanPool/Monlib4/LinearAlgebra/Matrix/StarOrderedRing.lean 316 121 5.01 8.88 6.86 2.02 36 0
LeanPool/Monlib4/QuantumGraph/Grad.lean 166 112 9.68 16.25 14.12 2.13 12 0
LeanPool/Monlib4/QuantumGraph/OfClassicalGraph.lean 110 98 5.85 10.02 7.83 2.19 9 0
LeanPool/Monlib4/LinearAlgebra/Coalgebra/MulOpposite.lean 230 69 3.26 3.33 2.05 1.28 12 0
LeanPool/Monlib4/LinearAlgebra/Ips/Symm.lean 51 50 2.71 2.09 0.47 1.62 2 0
LeanPool/Monlib4/Preq/RCLikeLe.lean 59 50 2.47 2.06 0.57 1.49 10 0
LeanPool/Monlib4/LinearAlgebra/Mul''.lean 168 47 6.07 7.57 5.86 1.71 9 0
LeanPool/Monlib4/LinearAlgebra/End.lean 50 37 2.21 1.82 0.46 1.36 5 0
LeanPool/Monlib4/LinearAlgebra/Matrix/Conj.lean 84 36 2.53 2.03 0.63 1.40 12 0
LeanPool/Monlib4/LinearAlgebra/Matrix/IsAlmostHermitian.lean 214 36 3.92 3.83 1.83 2.00 9 0
LeanPool/Monlib4/Preq/Dite.lean 114 36 2.12 1.73 0.52 1.21 11 0
LeanPool/Monlib4/Preq/Finset.lean 108 36 1.84 1.53 0.43 1.10 10 0
LeanPool/Monlib4/LinearAlgebra/LinearMapOp.lean 47 34 2.02 1.45 0.33 1.12 5 0
LeanPool/Monlib4/LinearAlgebra/Matrix/Cast.lean 24 24 2.16 1.49 0.26 1.23 3 0
LeanPool/Monlib4/LinearAlgebra/Matrix/Reshape.lean 50 24 2.41 1.79 0.39 1.40 6 0
LeanPool/Monlib4/LinearAlgebra/Nacgor.lean 50 22 2.70 2.10 0.56 1.54 4 0
LeanPool/Monlib4/Preq/Complex.lean 196 18 3.02 3.61 2.24 1.37 6 0
LeanPool/Monlib4/LinearAlgebra/QuantumSet/SchurMulTensor.lean 54 15 3.90 3.11 1.38 1.73 2 0
LeanPool/Monlib4/Preq/Ites.lean 52 15 2.02 1.63 0.41 1.22 4 0
LeanPool/Monlib4/LinearAlgebra/Matrix/PiMat.lean 19 13 2.04 1.37 0.17 1.20 3 0
LeanPool/Monlib4/LinearAlgebra/MySpec.lean 69 13 2.69 2.55 1.19 1.36 3 0
LeanPool/Monlib4/LinearAlgebra/QuantumSet/DeltaForm.lean 32 13 2.91 2.16 0.44 1.72 2 0
LeanPool/Monlib4/LinearAlgebra/QuantumSet/PhiMap.lean 62 12 3.72 3.47 1.73 1.74 4 0
LeanPool/Monlib4/Preq/Equiv.lean 19 12 2.83 2.17 0.41 1.76 1 0
LeanPool/Monlib4/LinearAlgebra/DirectSumFromTo.lean 40 9 1.99 1.53 0.30 1.23 3 0
LeanPool/Monlib4/LinearAlgebra/TensorProduct/OrthonormalBasis.lean 30 3 2.70 2.03 0.35 1.68 1 0
LeanPool/Monlib4.lean 67 0 3.04 2.34 0.26 2.08 0 0
LeanPool/Monlib4/LinearAlgebra.lean 35 0 2.95 2.30 0.25 2.05 0 0
LeanPool/Monlib4/LinearAlgebra/Coalgebra.lean 16 0 2.57 1.90 0.20 1.70 0 0
LeanPool/Monlib4/LinearAlgebra/Ips.lean 20 0 2.97 2.38 0.24 2.14 0 0
LeanPool/Monlib4/LinearAlgebra/Matrix.lean 23 0 3.18 2.27 0.25 2.02 0 0
LeanPool/Monlib4/LinearAlgebra/QuantumSet.lean 16 0 2.94 2.29 0.23 2.06 0 0
LeanPool/Monlib4/LinearAlgebra/TensorProduct.lean 17 0 2.67 1.97 0.21 1.76 0 0
LeanPool/Monlib4/Monlib.lean 17 0 3.27 2.39 0.25 2.14 0 0
LeanPool/Monlib4/Other.lean 13 0 3.11 2.33 0.25 2.08 0 0
LeanPool/Monlib4/Preq.lean 20 0 2.71 1.94 0.20 1.74 0 0
LeanPool/Monlib4/Preq/Set.lean 14 0 1.68 1.08 0.10 0.97 0 2
LeanPool/Monlib4/QuantumGraph.lean 18 0 3.20 2.41 0.24 2.17 0 0
LeanPool/Monlib4/RepTheory.lean 13 0 2.62 1.98 0.21 1.77 0 0
Total 35,331 395,189 891.10 1595.64 1426.53 169.11 2362 42

Aggregate phase totals

Phase Time
typeclass inference 703139.2 ms (= 703.14 s)
import 169114.0 ms (= 169.11 s)
tactic execution 167424.2 ms (= 167.42 s)
simp 166449.4 ms (= 166.45 s)
type checking 134272.9 ms (= 134.27 s)
elaboration 107054.2 ms (= 107.05 s)
interpretation 67042.6 ms (= 67.04 s)
blocked (unaccounted) 48008.6 ms (= 48.01 s)
process pre-definitions 4072.8 ms (= 4.07 s)
compilation (LCNF base) 3532.2 ms (= 3.53 s)
linting 3471.2 ms (= 3.47 s)
congr simp thm 3415.1 ms (= 3.42 s)

Slowest changed modules (from lake build)

Changed module Lake time
LeanPool.Monlib4.QuantumGraph.PiMat 114.00 s
LeanPool.Monlib4.LinearAlgebra.QuantumSet.SchurMul 101.00 s
LeanPool.Monlib4.QuantumGraph.PiMatFinTwo 68.00 s
LeanPool.Monlib4.LinearAlgebra.QuantumSet.QIso 61.00 s
LeanPool.Monlib4.QuantumGraph.Matrix 59.00 s
LeanPool.Monlib4.QuantumGraph.Iso 54.00 s
LeanPool.Monlib4.QuantumGraph.Basic 47.00 s
LeanPool.Monlib4.LinearAlgebra.Ips.Nontracial 46.00 s
LeanPool.Monlib4.LinearAlgebra.Ips.RankOne 38.00 s
LeanPool.Monlib4.LinearAlgebra.Ips.MatIps 38.00 s
LeanPool.Monlib4.LinearAlgebra.QuantumSet.Basic 37.00 s
LeanPool.Monlib4.QuantumGraph.ToProjections 37.00 s
Per-file `lean --profile` output

LeanPool/Monlib4.lean

import took 2.08s
cumulative profiling times:
	elaboration 0.223ms
	import 2.08s
	initialization 26.8ms
	interpretation 228ms
	linting 0.333ms
	parsing 0.116ms
real 3.05
user 1.77
sys 1.24

LeanPool/Monlib4/LinearAlgebra.lean

import took 2.05s
cumulative profiling times:
	elaboration 0.148ms
	import 2.05s
	initialization 26.6ms
	interpretation 218ms
	linting 0.24ms
	parsing 0.0282ms
real 2.90
user 1.71
sys 1.20

LeanPool/Monlib4/LinearAlgebra/Coalgebra.lean

import took 1.7s
cumulative profiling times:
	elaboration 0.169ms
	import 1.7s
	initialization 26.8ms
	interpretation 176ms
	linting 0.251ms
	parsing 0.0268ms
real 2.49
user 1.47
sys 1.03

LeanPool/Monlib4/LinearAlgebra/Coalgebra/FiniteDimensional.lean

import took 1.71s
tactic execution of Lean.Parser.Tactic.rewriteSeq took 138ms
tactic execution of Lean.Parser.Tactic.rewriteSeq took 201ms
simp took 155ms
simp took 171ms
tactic execution of Lean.Parser.Tactic.eqRefl took 174ms
tactic execution of Lean.Parser.Tactic.rewriteSeq took 181ms
tactic execution of Lean.Parser.Tactic.rewriteSeq took 183ms
tactic execution of Lean.Parser.Tactic.rewriteSeq took 373ms
elaboration took 352ms
tactic execution of Lean.Parser.Tactic.exact took 203ms
cumulative profiling times:
	attribute application 39.8ms
	blocked (unaccounted) 159ms
	compilation (IR) 1.55ms
	compilation (LCNF base) 82ms
	compilation (LCNF impure) 8.91ms
	compilation (LCNF mono) 26ms
	congr simp thm 26.3ms
	elaboration 1.15s
	fix level params 8.44ms
	import 1.71s
	initialization 26.7ms
	instantiate metavars 6.74ms
	interpretation 429ms
	let-to-have transformation 4.45ms
	linting 20.4ms
	parsing 13.8ms
	process pre-definitions 44.5ms
	share common exprs 22ms
	simp 1.18s
	tactic execution 1.82s
	type checking 839ms
	typeclass inference 6.51s
real 11.07
user 13.53
sys 1.12

LeanPool/Monlib4/LinearAlgebra/Coalgebra/Lemmas.lean

import took 1.29s
interpretation of Lean.Elab.Tactic._aux_Mathlib_Tactic_Widget_Calc___elabRules_Lean_calcTactic_1._boxed took 710ms
type checking took 169ms
cumulative profiling times:
	aesop 37.8ms
	attribute application 1.75ms
	blocked (unaccounted) 3.38s
	compilation (IR) 2.12ms
	compilation (LCNF base) 93.5ms
	compilation (LCNF impure) 12ms
	compilation (LCNF mono) 35ms
	congr simp thm 64.3ms
	elaboration 1.06s
	fix level params 9.31ms
	import 1.29s
	initialization 26.8ms
	instantiate metavars 4.83ms
	interpretation 1.36s
	let-to-have transformation 3.01ms
	linting 41.3ms
	parsing 31ms
	process pre-definitions 29.9ms
	share common exprs 23.7ms
	simp 895ms
	tactic execution 1.05s
	type checking 908ms
	typeclass inference 3.59s
real 8.02
user 10.29
sys 0.92

LeanPool/Monlib4/LinearAlgebra/Coalgebra/MulOpposite.lean

import took 1.28s
interpretation of Lean.Elab.Tactic._aux_Mathlib_Tactic_Widget_Calc___elabRules_Lean_calcTactic_1._boxed took 189ms
cumulative profiling times:
	attribute application 33.6ms
	compilation (IR) 0.0999ms
	compilation (LCNF base) 1.25ms
	compilation (LCNF impure) 0.555ms
	compilation (LCNF mono) 1.3ms
	congr simp thm 3.67ms
	elaboration 206ms
	fix level params 2.16ms
	import 1.28s
	initialization 26.5ms
	instantiate metavars 1.19ms
	interpretation 432ms
	let-to-have transformation 1.46ms
	linting 8.25ms
	parsing 8.61ms
	process pre-definitions 12.6ms
	share common exprs 4.67ms
	simp 152ms
	tactic execution 244ms
	type checking 185ms
	typeclass inference 725ms
real 3.30
user 3.08
sys 0.82

LeanPool/Monlib4/LinearAlgebra/DirectSumFromTo.lean

import took 1.23s
cumulative profiling times:
	attribute application 0.0268ms
	compilation (IR) 0.062ms
	compilation (LCNF base) 2.41ms
	compilation (LCNF impure) 0.328ms
	compilation (LCNF mono) 1.36ms
	congr simp thm 1.44ms
	elaboration 13ms
	fix level params 0.178ms
	import 1.23s
	initialization 26.8ms
	instantiate metavars 0.183ms
	interpretation 137ms
	let-to-have transformation 0.0377ms
	linting 1.66ms
	parsing 1.66ms
	process pre-definitions 1.25ms
	share common exprs 0.327ms
	simp 23.4ms
	tactic execution 9.41ms
	type checking 6.36ms
	typeclass inference 75.5ms
real 2.03
user 1.31
sys 0.79

LeanPool/Monlib4/LinearAlgebra/End.lean

import took 1.36s
cumulative profiling times:
	attribute application 2.67ms
	compilation (IR) 0.115ms
	compilation (LCNF base) 1.68ms
	compilation (LCNF impure) 0.636ms
	compilation (LCNF mono) 1.88ms
	congr simp thm 2.47ms
	elaboration 36.5ms
	fix level params 0.78ms
	import 1.36s
	initialization 26.8ms
	instantiate metavars 0.342ms
	interpretation 178ms
	let-to-have transformation 0.2ms
	linting 3.46ms
	parsing 2.31ms
	process pre-definitions 1.53ms
	share common exprs 1.42ms
	simp 62.9ms
	tactic execution 30.1ms
	type checking 18.3ms
	typeclass inference 84.4ms
real 2.22
user 1.51
sys 0.88

LeanPool/Monlib4/LinearAlgebra/InnerAut.lean

import took 2.04s
simp took 104ms
typeclass inference of FiniteDimensional took 112ms
simp took 121ms
typeclass inference of Nonempty took 108ms
cumulative profiling times:
	attribute application 130ms
	compilation (IR) 2.06ms
	compilation (LCNF base) 33.1ms
	compilation (LCNF impure) 11.5ms
	compilation (LCNF mono) 37.8ms
	congr simp thm 40.8ms
	elaboration 1.58s
	fix level params 18ms
	import 2.04s
	initialization 26.6ms
	instantiate metavars 12.9ms
	interpretation 1.08s
	let-to-have transformation 8.02ms
	linting 55.9ms
	norm_num 21.7ms
	parsing 51.6ms
	process pre-definitions 49.8ms
	share common exprs 42.6ms
	simp 2.22s
	tactic execution 1.65s
	type checking 1.12s
	typeclass inference 10.2s
real 10.82
user 19.75
sys 1.36

LeanPool/Monlib4/LinearAlgebra/InvariantSubmodule.lean

import took 1.42s
simp took 100ms
cumulative profiling times:
	attribute application 1.21ms
	blocked (unaccounted) 72.3ms
	compilation (IR) 1.16ms
	compilation (LCNF base) 41.8ms
	compilation (LCNF impure) 6.29ms
	compilation (LCNF mono) 16.7ms
	congr simp thm 9.69ms
	elaboration 256ms
	fix level params 3.9ms
	import 1.42s
	initialization 26.6ms
	instantiate metavars 3.07ms
	interpretation 424ms
	let-to-have transformation 0.874ms
	linting 19.5ms
	parsing 13.6ms
	process pre-definitions 13.5ms
	share common exprs 8.79ms
	simp 402ms
	tactic execution 249ms
	type checking 112ms
	typeclass inference 1.04s
real 3.39
user 3.78
sys 0.90

LeanPool/Monlib4/LinearAlgebra/Ips.lean

import took 2.14s
cumulative profiling times:
	elaboration 0.0633ms
	import 2.14s
	initialization 27.1ms
	interpretation 211ms
	linting 0.123ms
	parsing 0.00163ms
real 3.03
user 1.84
sys 1.20

LeanPool/Monlib4/LinearAlgebra/Ips/Basic.lean

import took 1.73s
cumulative profiling times:
	attribute application 0.769ms
	blocked (unaccounted) 166ms
	compilation (IR) 1.19ms
	compilation (LCNF base) 20.6ms
	compilation (LCNF impure) 6.71ms
	compilation (LCNF mono) 17.9ms
	congr simp thm 13.4ms
	elaboration 233ms
	fix level params 4.08ms
	import 1.73s
	initialization 26.9ms
	instantiate metavars 2.68ms
	interpretation 374ms
	let-to-have transformation 2.56ms
	linting 15.9ms
	parsing 12.6ms
	process pre-definitions 10.3ms
	share common exprs 9.45ms
	simp 287ms
	tactic execution 343ms
	type checking 234ms
	typeclass inference 2.21s
real 4.40
user 5.11
sys 1.08

LeanPool/Monlib4/LinearAlgebra/Ips/Frob.lean

import took 2.11s
LeanPool/Monlib4/LinearAlgebra/Ips/Frob.lean:147:4: error: invalid 'calc' step, left-hand side is
  (starRingEnd ℂ) (a (x_1, x_3) (x_2, x_4)) *
    ⟪kroneckerToTensorProduct
        (kroneckerMap (fun x1 x2 => x1 * x2) (stdBasisMatrix x_1 x_2 1) (stdBasisMatrix x_3 x_4 1)),
      x ⊗ₜ[ℂ] y⟫_ℂ : Complex
but is expected to be
  ⟪a (x_1, x_3) (x_2, x_4) •
      kroneckerToTensorProduct (kroneckerMap (fun x1 x2 => x1 * x2) (single x_1 x_2 1) (single x_3 x_4 1)),
    x ⊗ₜ[ℂ] y⟫_ℂ : Complex
simp took 107ms
simp took 156ms
simp took 104ms
interpretation of Lean.Elab.Tactic._aux_Mathlib_Tactic_Widget_Calc___elabRules_Lean_calcTactic_1._boxed took 137ms
cumulative profiling times:
	aesop 31.3ms
	attribute application 15.3ms
	blocked (unaccounted) 1.17s
	compilation (IR) 1.56ms
	compilation (LCNF base) 58.5ms
	compilation (LCNF impure) 8.67ms
	compilation (LCNF mono) 20.5ms
	congr simp thm 17.5ms
	elaboration 904ms
	fix level params 3.49ms
	import 2.11s
	initialization 27.4ms
	instantiate metavars 2.49ms
	interpretation 636ms
	let-to-have transformation 12ms
	linting 25.9ms
	parsing 22.1ms
	process pre-definitions 21.1ms
	share common exprs 9.52ms
	simp 1.05s
	tactic execution 387ms
	type checking 233ms
	typeclass inference 2.73s
real 7.05
user 7.86
sys 1.26
error: profile command exited with status 1

LeanPool/Monlib4/LinearAlgebra/Ips/Functional.lean

import took 2.08s
typeclass inference of StarRing took 139ms
typeclass inference of StarRing took 143ms
cumulative profiling times:
	aesop 139ms
	attribute application 1.83ms
	blocked (unaccounted) 672ms
	compilation (IR) 2.96ms
	compilation (LCNF base) 48.5ms
	compilation (LCNF impure) 17ms
	compilation (LCNF mono) 51.1ms
	congr simp thm 96ms
	dsimp 3.07ms
	elaboration 728ms
	fix level params 15.8ms
	import 2.08s
	initialization 26.7ms
	instantiate metavars 18.9ms
	interpretation 1.18s
	let-to-have transformation 1.45ms
	linting 68.9ms
	parsing 60.4ms
	process pre-definitions 74.3ms
	share common exprs 44.8ms
	simp 3.41s
	tactic execution 1.31s
	type checking 775ms
	typeclass inference 5.56s
real 7.45
user 14.95
sys 1.37

LeanPool/Monlib4/LinearAlgebra/Ips/Ips.lean

import took 1.7s
tactic execution of Lean.Parser.Tactic.rewriteSeq took 107ms
typeclass inference of CoeFun took 101ms
tactic execution of Lean.Parser.Tactic.rewriteSeq took 220ms
simp took 234ms
typeclass inference of CoeFun took 101ms
typeclass inference of CoeFun took 107ms
cumulative profiling times:
	attribute application 0.503ms
	blocked (unaccounted) 20.9ms
	compilation (IR) 0.583ms
	compilation (LCNF base) 16.5ms
	compilation (LCNF impure) 3.59ms
	compilation (LCNF mono) 10.1ms
	congr simp thm 21.4ms
	elaboration 366ms
	fix level params 10.8ms
	import 1.7s
	initialization 26.7ms
	instantiate metavars 9.69ms
	interpretation 448ms
	let-to-have transformation 1.04ms
	linting 36.6ms
	parsing 19.5ms
	process pre-definitions 22.2ms
	share common exprs 28.3ms
	simp 867ms
	tactic execution 1.58s
	type checking 439ms
	typeclass inference 6.51s
real 7.37
user 11.61
sys 1.12

LeanPool/Monlib4/LinearAlgebra/Ips/MatIps.lean

import took 2.04s
tactic execution of Lean.Parser.Tactic.refine took 131ms
typeclass inference of HSMul took 1.2s
typeclass inference of AddCommMonoid took 965ms
simp took 163ms
simp took 183ms
simp took 102ms
simp took 105ms
simp took 100ms
typeclass inference of HSMul took 1.21s
typeclass inference of AddCommMonoid took 985ms
typeclass inference of HSMul took 1.19s
typeclass inference of AddCommMonoid took 989ms
type checking took 177ms
simp took 106ms
simp took 258ms
simp took 194ms
simp took 188ms
simp took 197ms
simp took 207ms
simp took 191ms
simp took 186ms
simp took 245ms
simp took 1.07s
type checking took 213ms
tactic execution of Lean.Parser.Tactic.rewriteSeq took 280ms
type checking took 595ms
typeclass inference of AddMonoidHomClass took 115ms
simp took 108ms
simp took 110ms
type checking took 131ms
typeclass inference of FiniteDimensional took 105ms
type checking took 152ms
elaboration took 103ms
cumulative profiling times:
	aesop 168ms
	attribute application 51.3ms
	blocked (unaccounted) 3.27s
	compilation (IR) 6.11ms
	compilation (LCNF base) 171ms
	compilation (LCNF impure) 35.8ms
	compilation (LCNF mono) 97.1ms
	congr simp thm 201ms
	elaboration 3.54s
	fix level params 31ms
	import 2.04s
	initialization 26.5ms
	instantiate metavars 32.8ms
	interpretation 2.54s
	let-to-have transformation 13ms
	linting 249ms
	norm_num 0.969ms
	parsing 108ms
	process pre-definitions 115ms
	share common exprs 92.9ms
	simp 9.54s
	tactic execution 3s
	type checking 3.03s
	typeclass inference 18.9s
real 25.80
user 43.44
sys 1.42

LeanPool/Monlib4/LinearAlgebra/Ips/MinimalProj.lean

import took 1.73s
typeclass inference of HSMul took 237ms
typeclass inference of SeminormedAddCommGroup took 676ms
typeclass inference of MulAction took 122ms
typeclass inference of IsLeftCancelMulZero took 298ms
typeclass inference of IsLeftCancelMulZero took 296ms
typeclass inference of IsLeftCancelMulZero took 287ms
typeclass inference of IsLeftCancelMulZero took 183ms
cumulative profiling times:
	attribute application 4.43ms
	blocked (unaccounted) 1.39s
	compilation (IR) 2.75ms
	compilation (LCNF base) 71ms
	compilation (LCNF impure) 16.5ms
	compilation (LCNF mono) 48.6ms
	congr simp thm 45.6ms
	elaboration 987ms
	fix level params 20.1ms
	import 1.73s
	initialization 26.6ms
	instantiate metavars 21.2ms
	interpretation 1.11s
	let-to-have transformation 4.46ms
	linting 86.6ms
	parsing 50.6ms
	process pre-definitions 57.5ms
	share common exprs 49.8ms
	simp 1.04s
	tactic execution 2.19s
	type checking 774ms
	typeclass inference 11.5s
real 10.26
user 19.19
sys 1.23

LeanPool/Monlib4/LinearAlgebra/Ips/MulOp.lean

import took 1.62s
cumulative profiling times:
	attribute application 0.418ms
	compilation (IR) 0.132ms
	compilation (LCNF base) 2.78ms
	compilation (LCNF impure) 0.789ms
	compilation (LCNF mono) 4.86ms
	congr simp thm 2.41ms
	elaboration 185ms
	fix level params 1.31ms
	import 1.62s
	initialization 26.5ms
	instantiate metavars 0.746ms
	interpretation 299ms
	let-to-have transformation 0.837ms
	linting 5.73ms
	parsing 4.86ms
	process pre-definitions 3.39ms
	share common exprs 2.98ms
	simp 57.7ms
	tactic execution 57.2ms
	type checking 99.4ms
	typeclass inference 1.21s
real 3.50
user 3.20
sys 0.98

LeanPool/Monlib4/LinearAlgebra/Ips/Nontracial.lean

import took 2.03s
simp took 152ms
simp took 154ms
simp took 162ms
simp took 216ms
simp took 234ms
simp took 204ms
simp took 167ms
simp took 361ms
simp took 437ms
simp took 289ms
simp took 1.61s
type checking took 126ms
simp took 102ms
simp took 101ms
simp took 109ms
simp took 147ms
typeclass inference of MulActionHomClass took 129ms
type checking took 121ms
elaboration took 181ms
simp took 124ms
simp took 144ms
simp took 179ms
simp took 188ms
simp took 111ms
simp took 104ms
simp took 105ms
simp took 100ms
simp took 716ms
type checking took 127ms
typeclass inference of AddMonoidHomClass took 156ms
simp took 422ms
typeclass inference of AddMonoidHomClass took 161ms
simp took 174ms
type checking took 176ms
elaboration took 101ms
elaboration took 110ms
elaboration took 166ms
type checking took 209ms
elaboration took 548ms
tactic execution of Lean.Parser.Tactic.refine took 480ms
simp took 101ms
cumulative profiling times:
	aesop 85.7ms
	attribute application 51ms
	blocked (unaccounted) 201ms
	compilation (IR) 3.32ms
	compilation (LCNF base) 101ms
	compilation (LCNF impure) 19.2ms
	compilation (LCNF mono) 54.9ms
	congr simp thm 252ms
	elaboration 3.66s
	fix level params 31.1ms
	import 2.03s
	initialization 26.5ms
	instantiate metavars 49.5ms
	interpretation 1.65s
	let-to-have transformation 34.6ms
	linting 149ms
	parsing 72.7ms
	process pre-definitions 137ms
	share common exprs 84.3ms
	simp 13.2s
	tactic execution 2.7s
	type checking 2.62s
	typeclass inference 13.7s
real 21.56
user 40.16
sys 1.43

LeanPool/Monlib4/LinearAlgebra/Ips/OpUnop.lean

import took 1.28s
cumulative profiling times:
	attribute application 34.3ms
	blocked (unaccounted) 0.0515ms
	compilation (IR) 0.113ms
	compilation (LCNF base) 3ms
	compilation (LCNF impure) 0.577ms
	compilation (LCNF mono) 1.96ms
	congr simp thm 1.02ms
	elaboration 129ms
	fix level params 0.746ms
	import 1.28s
	initialization 26.6ms
	instantiate metavars 0.649ms
	interpretation 185ms
	let-to-have transformation 1.45ms
	linting 4.55ms
	parsing 4.6ms
	process pre-definitions 3.46ms
	share common exprs 1.52ms
	simp 14.7ms
	tactic execution 50.7ms
	type checking 71.4ms
	typeclass inference 196ms
real 2.31
user 1.76
sys 0.82

LeanPool/Monlib4/LinearAlgebra/Ips/Pos.lean

import took 1.73s
simp took 158ms
cumulative profiling times:
	attribute application 15.9ms
	blocked (unaccounted) 380ms
	compilation (IR) 2.36ms
	compilation (LCNF base) 70.4ms
	compilation (LCNF impure) 14.4ms
	compilation (LCNF mono) 39.7ms
	congr simp thm 91.1ms
	elaboration 624ms
	fix level params 14.2ms
	import 1.73s
	initialization 26.4ms
	instantiate metavars 18.7ms
	interpretation 706ms
	let-to-have transformation 2.05ms
	linting 61.6ms
	parsing 30ms
	process pre-definitions 52.7ms
	share common exprs 34.1ms
	simp 2.39s
	tactic execution 1.1s
	type checking 614ms
	typeclass inference 5.98s
real 9.17
user 13.13
sys 1.12

LeanPool/Monlib4/LinearAlgebra/Ips/RankOne.lean

import took 1.62s
process pre-definitions took 121ms
tactic execution of Lean.Parser.Tactic.rewriteSeq took 150ms
typeclass inference of CoeFun took 105ms
tactic execution of Lean.Parser.Tactic.obtain took 303ms
elaboration took 367ms
elaboration took 190ms
elaboration took 205ms
cumulative profiling times:
	attribute application 96.9ms
	compilation (IR) 1.47ms
	compilation (LCNF base) 28.8ms
	compilation (LCNF impure) 8.54ms
	compilation (LCNF mono) 28.2ms
	congr simp thm 48.8ms
	dsimp 1.12ms
	elaboration 2s
	fix level params 33.3ms
	import 1.62s
	initialization 26.4ms
	instantiate metavars 31.1ms
	interpretation 980ms
	let-to-have transformation 8.44ms
	linting 62.7ms
	norm_num 0.797ms
	parsing 44.1ms
	process pre-definitions 200ms
	share common exprs 84.3ms
	simp 1.68s
	tactic execution 1.96s
	type checking 1.84s
	typeclass inference 19s
real 18.03
user 29.29
sys 1.12

LeanPool/Monlib4/LinearAlgebra/Ips/Strict.lean

import took 1.17s
cumulative profiling times:
	attribute application 40.4ms
	congr simp thm 6.72ms
	elaboration 289ms
	fix level params 2.53ms
	import 1.17s
	initialization 26.5ms
	instantiate metavars 1.67ms
	interpretation 262ms
	let-to-have transformation 1.76ms
	linting 13.7ms
	parsing 12.4ms
	process pre-definitions 16.7ms
	share common exprs 4.99ms
	simp 66.2ms
	tactic execution 32.5ms
	type checking 132ms
	typeclass inference 1.21s
real 3.26
user 3.04
sys 0.82

LeanPool/Monlib4/LinearAlgebra/Ips/Symm.lean

import took 1.62s
cumulative profiling times:
	attribute application 0.146ms
	blocked (unaccounted) 18.4ms
	compilation (IR) 0.317ms
	compilation (LCNF base) 8.77ms
	compilation (LCNF impure) 2.14ms
	compilation (LCNF mono) 4.67ms
	congr simp thm 0.704ms
	elaboration 31.3ms
	fix level params 0.328ms
	import 1.62s
	initialization 26.7ms
	instantiate metavars 0.141ms
	interpretation 193ms
	let-to-have transformation 0.0834ms
	linting 3.2ms
	parsing 2.23ms
	process pre-definitions 1.6ms
	share common exprs 0.907ms
	simp 17.1ms
	tactic execution 20.3ms
	type checking 12.9ms
	typeclass inference 130ms
real 2.59
user 1.69
sys 0.98

LeanPool/Monlib4/LinearAlgebra/Ips/TensorHilbert.lean

import took 1.63s
cumulative profiling times:
	attribute application 0.334ms
	compilation (IR) 0.035ms
	compilation (LCNF base) 0.477ms
	compilation (LCNF impure) 0.182ms
	compilation (LCNF mono) 0.526ms
	congr simp thm 9.76ms
	elaboration 450ms
	fix level params 3.44ms
	import 1.63s
	initialization 26.6ms
	instantiate metavars 1.79ms
	interpretation 348ms
	let-to-have transformation 2.68ms
	linting 14.7ms
	parsing 12.8ms
	process pre-definitions 7.31ms
	share common exprs 8.25ms
	simp 293ms
	tactic execution 298ms
	type checking 253ms
	typeclass inference 3.26s
real 5.34
user 6.16
sys 1.04

LeanPool/Monlib4/LinearAlgebra/Ips/Vn.lean

import took 1.74s
cumulative profiling times:
	aesop 148ms
	attribute application 0.0307ms
	compilation (IR) 0.186ms
	compilation (LCNF base) 7.12ms
	compilation (LCNF impure) 1ms
	compilation (LCNF mono) 4.24ms
	congr simp thm 3.91ms
	elaboration 41.7ms
	fix level params 1.2ms
	import 1.74s
	initialization 26.6ms
	instantiate metavars 1.57ms
	interpretation 284ms
	let-to-have transformation 0.0608ms
	linting 7.94ms
	parsing 5.11ms
	process pre-definitions 8.36ms
	share common exprs 3.79ms
	simp 176ms
	tactic execution 188ms
	type checking 80.8ms
	typeclass inference 594ms
real 3.26
user 2.85
sys 1.07

LeanPool/Monlib4/LinearAlgebra/IsProj'.lean

import took 1.6s
cumulative profiling times:
	attribute application 4.69ms
	blocked (unaccounted) 40.9ms
	compilation (IR) 0.427ms
	compilation (LCNF base) 24.4ms
	compilation (LCNF impure) 2.43ms
	compilation (LCNF mono) 7.77ms
	congr simp thm 3.93ms
	elaboration 151ms
	fix level params 0.853ms
	import 1.6s
	initialization 26.5ms
	instantiate metavars 0.634ms
	interpretation 232ms
	let-to-have transformation 0.552ms
	linting 5.98ms
	parsing 3.81ms
	process pre-definitions 7.5ms
	share common exprs 2.07ms
	simp 45.8ms
	tactic execution 21.4ms
	type checking 37.8ms
	typeclass inference 553ms
real 3.14
user 2.34
sys 1.01

LeanPool/Monlib4/LinearAlgebra/IsReal.lean

import took 1.49s
cumulative profiling times:
	attribute application 3.3ms
	compilation (IR) 0.489ms
	compilation (LCNF base) 11.2ms
	compilation (LCNF impure) 2.63ms
	compilation (LCNF mono) 8.33ms
	congr simp thm 15.7ms
	dsimp 18ms
	elaboration 210ms
	fix level params 3.23ms
	import 1.49s
	initialization 26.9ms
	instantiate metavars 2.62ms
	interpretation 330ms
	let-to-have transformation 0.602ms
	linting 13.5ms
	parsing 11.8ms
	process pre-definitions 15ms
	share common exprs 6.38ms
	simp 293ms
	tactic execution 146ms
	type checking 120ms
	typeclass inference 2.41s
real 4.69
user 4.80
sys 0.95

LeanPool/Monlib4/LinearAlgebra/KroneckerToTensor.lean

import took 1.7s
typeclass inference of AddHomClass took 206ms
typeclass inference of MulActionHomClass took 198ms
typeclass inference of AddHomClass took 236ms
typeclass inference of MulActionHomClass took 219ms
simp took 188ms
simp took 103ms
typeclass inference of MulZeroClass took 202ms
typeclass inference of Distrib took 137ms
typeclass inference of MulZeroClass took 132ms
typeclass inference of Distrib took 128ms
elaboration took 115ms
elaboration took 111ms
elaboration took 135ms
cumulative profiling times:
	attribute application 20.9ms
	compilation (IR) 0.425ms
	compilation (LCNF base) 6.56ms
	compilation (LCNF impure) 2.49ms
	compilation (LCNF mono) 7.4ms
	congr simp thm 22.8ms
	dsimp 20.9ms
	elaboration 689ms
	fix level params 6.16ms
	import 1.7s
	initialization 26.7ms
	instantiate metavars 6.95ms
	interpretation 522ms
	let-to-have transformation 1.75ms
	linting 18.5ms
	parsing 12ms
	process pre-definitions 25ms
	share common exprs 11.5ms
	simp 1.12s
	tactic execution 177ms
	type checking 469ms
	typeclass inference 5.8s
real 7.17
user 10.17
sys 1.10

LeanPool/Monlib4/LinearAlgebra/LinearMapOp.lean

import took 1.12s
cumulative profiling times:
	attribute application 11.1ms
	compilation (IR) 0.0867ms
	compilation (LCNF base) 3.01ms
	compilation (LCNF impure) 0.404ms
	compilation (LCNF mono) 1.34ms
	congr simp thm 0.885ms
	elaboration 55.5ms
	fix level params 0.35ms
	import 1.12s
	initialization 26.7ms
	instantiate metavars 0.175ms
	interpretation 139ms
	let-to-have transformation 0.394ms
	linting 2.77ms
	parsing 2.37ms
	process pre-definitions 4.04ms
	share common exprs 0.772ms
	simp 13ms
	tactic execution 3.04ms
	type checking 26.7ms
	typeclass inference 41.6ms
real 1.92
user 1.26
sys 0.76

LeanPool/Monlib4/LinearAlgebra/LmulRmul.lean

import took 1.27s
cumulative profiling times:
	attribute application 13.7ms
	blocked (unaccounted) 74.8ms
	compilation (IR) 0.943ms
	compilation (LCNF base) 31.1ms
	compilation (LCNF impure) 5.32ms
	compilation (LCNF mono) 15ms
	congr simp thm 17.7ms
	elaboration 322ms
	fix level params 4.13ms
	import 1.27s
	initialization 26.7ms
	instantiate metavars 2.26ms
	interpretation 357ms
	let-to-have transformation 2.2ms
	linting 18.4ms
	parsing 13.5ms
	process pre-definitions 16.6ms
	share common exprs 8.22ms
	simp 155ms
	tactic execution 120ms
	type checking 172ms
	typeclass inference 3.9s
real 6.10
user 6.23
sys 0.86

LeanPool/Monlib4/LinearAlgebra/Matrix.lean

import took 2.02s
cumulative profiling times:
	elaboration 0.142ms
	import 2.02s
	initialization 26.5ms
	interpretation 219ms
	linting 0.252ms
	parsing 0.0257ms
real 2.87
user 1.69
sys 1.19

LeanPool/Monlib4/LinearAlgebra/Matrix/Basic.lean

import took 1.72s
simp took 124ms
simp took 145ms
simp took 150ms
simp took 142ms
simp took 157ms
simp took 144ms
simp took 207ms
simp took 184ms
simp took 161ms
simp took 111ms
simp took 109ms
simp took 101ms
typeclass inference of Nonempty took 109ms
typeclass inference of Nonempty took 110ms
cumulative profiling times:
	attribute application 1.76ms
	compilation (IR) 1.08ms
	compilation (LCNF base) 20.4ms
	compilation (LCNF impure) 6.74ms
	compilation (LCNF mono) 22.1ms
	congr simp thm 48.9ms
	elaboration 315ms
	fix level params 11.4ms
	import 1.72s
	initialization 26.4ms
	instantiate metavars 4.63ms
	interpretation 608ms
	let-to-have transformation 1.15ms
	linting 33.6ms
	parsing 28.5ms
	process pre-definitions 28.9ms
	share common exprs 26.9ms
	simp 4.3s
	tactic execution 429ms
	type checking 332ms
	typeclass inference 3.24s
real 5.32
user 10.69
sys 1.13

LeanPool/Monlib4/LinearAlgebra/Matrix/Cast.lean

import took 1.23s
cumulative profiling times:
	aesop 52.4ms
	attribute application 0.0302ms
	congr simp thm 0.745ms
	elaboration 11.1ms
	fix level params 0.199ms
	import 1.23s
	initialization 26.5ms
	instantiate metavars 0.0489ms
	interpretation 143ms
	let-to-have transformation 0.0515ms
	linting 2.06ms
	parsing 1.6ms
	process pre-definitions 0.506ms
	share common exprs 0.346ms
	simp 6.71ms
	tactic execution 5ms
	type checking 2.17ms
	typeclass inference 5.36ms
real 1.95
user 1.20
sys 0.82

LeanPool/Monlib4/LinearAlgebra/Matrix/Conj.lean

import took 1.4s
cumulative profiling times:
	attribute application 3.22ms
	blocked (unaccounted) 29ms
	compilation (IR) 0.41ms
	compilation (LCNF base) 14.9ms
	compilation (LCNF impure) 2.39ms
	compilation (LCNF mono) 7.04ms
	congr simp thm 2.9ms
	elaboration 80.4ms
	fix level params 0.551ms
	import 1.4s
	initialization 26.6ms
	instantiate metavars 0.396ms
	interpretation 244ms
	let-to-have transformation 0.433ms
	linting 5.87ms
	parsing 4.01ms
	process pre-definitions 3.41ms
	share common exprs 1.65ms
	simp 59.7ms
	tactic execution 24.7ms
	type checking 16.5ms
	typeclass inference 101ms
real 2.31
user 1.67
sys 0.90

LeanPool/Monlib4/LinearAlgebra/Matrix/IncludeBlock.lean

import took 2.02s
simp took 692ms
typeclass inference of AddHomClass took 135ms
elaboration took 102ms
cumulative profiling times:
	aesop 298ms
	attribute application 10.2ms
	blocked (unaccounted) 58.2ms
	compilation (IR) 2.91ms
	compilation (LCNF base) 59.2ms
	compilation (LCNF impure) 16ms
	compilation (LCNF mono) 44.2ms
	congr simp thm 38.9ms
	dsimp 52.3ms
	elaboration 737ms
	fix level params 11.4ms
	import 2.02s
	initialization 29.1ms
	instantiate metavars 13.8ms
	interpretation 1.09s
	let-to-have transformation 2.35ms
	linting 63.1ms
	parsing 51.6ms
	process pre-definitions 82.6ms
	share common exprs 24.7ms
	simp 2.33s
	tactic execution 450ms
	type checking 465ms
	typeclass inference 4.27s
real 8.40
user 11.58
sys 1.28

LeanPool/Monlib4/LinearAlgebra/Matrix/IsAlmostHermitian.lean

import took 2s
cumulative profiling times:
	attribute application 0.0926ms
	compilation (IR) 0.745ms
	compilation (LCNF base) 12.7ms
	compilation (LCNF impure) 4.62ms
	compilation (LCNF mono) 14.9ms
	congr simp thm 9.92ms
	elaboration 30.3ms
	fix level params 1.79ms
	import 2s
	initialization 26.6ms
	instantiate metavars 2.95ms
	interpretation 392ms
	let-to-have transformation 0.11ms
	linting 12.8ms
	parsing 10.3ms
	process pre-definitions 7.14ms
	share common exprs 5.37ms
	simp 329ms
	tactic execution 263ms
	type checking 62ms
	typeclass inference 642ms
real 3.60
user 3.23
sys 1.20

LeanPool/Monlib4/LinearAlgebra/Matrix/PiMat.lean

import took 1.2s
cumulative profiling times:
	attribute application 0.681ms
	blocked (unaccounted) 1.7ms
	elaboration 5.45ms
	fix level params 0.0435ms
	import 1.2s
	initialization 26.5ms
	instantiate metavars 0.0587ms
	interpretation 127ms
	let-to-have transformation 0.0415ms
	linting 0.968ms
	parsing 1.05ms
	process pre-definitions 0.379ms
	share common exprs 0.0692ms
	tactic execution 3.02ms
	type checking 0.903ms
real 1.90
user 1.13
sys 0.79

LeanPool/Monlib4/LinearAlgebra/Matrix/PosDefRpow.lean

import took 2.02s
cumulative profiling times:
	aesop 38.3ms
	attribute application 11.5ms
	blocked (unaccounted) 0.503ms
	compilation (IR) 0.547ms
	compilation (LCNF base) 7.71ms
	compilation (LCNF impure) 2.88ms
	compilation (LCNF mono) 8.69ms
	congr simp thm 37.8ms
	elaboration 235ms
	fix level params 4.73ms
	import 2.02s
	initialization 26.5ms
	instantiate metavars 3.3ms
	interpretation 438ms
	let-to-have transformation 1.21ms
	linting 19.6ms
	parsing 11.9ms
	process pre-definitions 15.9ms
	share common exprs 10.6ms
	simp 688ms
	tactic execution 368ms
	type checking 338ms
	typeclass inference 1.99s
real 4.68
user 5.68
sys 1.22

LeanPool/Monlib4/LinearAlgebra/Matrix/PosEqLinearMapIsPositive.lean

import took 1.73s
elaboration took 102ms
simp took 135ms
tactic execution of Lean.Parser.Tactic.refine took 109ms
simp took 137ms
elaboration took 194ms
cumulative profiling times:
	attribute application 13.7ms
	blocked (unaccounted) 1.3s
	compilation (IR) 1.23ms
	compilation (LCNF base) 21.2ms
	compilation (LCNF impure) 7.41ms
	compilation (LCNF mono) 19.6ms
	congr simp thm 25.7ms
	elaboration 1.17s
	fix level params 14.1ms
	import 1.73s
	initialization 26.8ms
	instantiate metavars 13.6ms
	interpretation 742ms
	let-to-have transformation 4.93ms
	linting 42.6ms
	parsing 37.7ms
	process pre-definitions 33.7ms
	share common exprs 39.3ms
	simp 1.76s
	tactic execution 1.34s
	type checking 948ms
	typeclass inference 7.78s
real 8.71
user 15.17
sys 1.17

LeanPool/Monlib4/LinearAlgebra/Matrix/Reshape.lean

import took 1.4s
cumulative profiling times:
	attribute application 2.71ms
	compilation (IR) 0.0989ms
	compilation (LCNF base) 3.62ms
	compilation (LCNF impure) 0.583ms
	compilation (LCNF mono) 3.02ms
	congr simp thm 0.942ms
	elaboration 52.7ms
	fix level params 0.345ms
	import 1.4s
	initialization 26.7ms
	instantiate metavars 0.248ms
	interpretation 187ms
	let-to-have transformation 0.268ms
	linting 2.47ms
	parsing 1.77ms
	process pre-definitions 1.33ms
	share common exprs 0.619ms
	simp 12.1ms
	tactic execution 8.38ms
	type checking 17.2ms
	typeclass inference 71.7ms
real 2.24
user 1.45
sys 0.90

LeanPool/Monlib4/LinearAlgebra/Matrix/Spectra.lean

import took 2.03s
cumulative profiling times:
	attribute application 1.15ms
	blocked (unaccounted) 40.5ms
	compilation (IR) 0.116ms
	compilation (LCNF base) 1.24ms
	compilation (LCNF impure) 0.547ms
	compilation (LCNF mono) 1.26ms
	congr simp thm 4.4ms
	elaboration 105ms
	fix level params 2.39ms
	import 2.03s
	initialization 26.6ms
	instantiate metavars 1.98ms
	interpretation 378ms
	let-to-have transformation 0.483ms
	linting 10.6ms
	parsing 9.08ms
	process pre-definitions 10ms
	share common exprs 4.75ms
	simp 136ms
	tactic execution 144ms
	type checking 123ms
	typeclass inference 1.2s
real 3.80
user 3.60
sys 1.25

LeanPool/Monlib4/LinearAlgebra/Matrix/StarOrderedRing.lean

import took 2.02s
typeclass inference of FiniteDimensional took 109ms
cumulative profiling times:
	attribute application 0.887ms
	blocked (unaccounted) 76.7ms
	compilation (IR) 0.659ms
	compilation (LCNF base) 11ms
	compilation (LCNF impure) 4.18ms
	compilation (LCNF mono) 12.6ms
	congr simp thm 14.4ms
	elaboration 210ms
	fix level params 6.83ms
	import 2.02s
	initialization 26.8ms
	instantiate metavars 3.74ms
	interpretation 574ms
	let-to-have transformation 0.784ms
	linting 24.1ms
	norm_num 0.342ms
	parsing 19.8ms
	process pre-definitions 17.4ms
	ring 4.96ms
	share common exprs 16.3ms
	simp 738ms
	tactic execution 636ms
	type checking 370ms
	typeclass inference 4.09s
real 4.93
user 8.09
sys 1.26

LeanPool/Monlib4/LinearAlgebra/Mul''.lean

import took 1.71s
simp took 113ms
typeclass inference of AddCommMonoid took 152ms
typeclass inference of ContinuousMapClass took 159ms
cumulative profiling times:
	attribute application 2.53ms
	blocked (unaccounted) 5.85ms
	compilation (IR) 0.469ms
	compilation (LCNF base) 14ms
	compilation (LCNF impure) 2.64ms
	compilation (LCNF mono) 10.3ms
	congr simp thm 26.6ms
	elaboration 252ms
	fix level params 4.92ms
	import 1.71s
	initialization 27ms
	instantiate metavars 5.22ms
	interpretation 424ms
	let-to-have transformation 0.833ms
	linting 8.56ms
	parsing 7.04ms
	process pre-definitions 32.7ms
	share common exprs 13.3ms
	simp 641ms
	tactic execution 210ms
	type checking 437ms
	typeclass inference 3.73s
real 5.79
user 7.10
sys 1.08

LeanPool/Monlib4/LinearAlgebra/MyBimodule.lean

import took 1.36s
cumulative profiling times:
	attribute application 35.1ms
	blocked (unaccounted) 123ms
	compilation (IR) 1.27ms
	compilation (LCNF base) 49.3ms
	compilation (LCNF impure) 7.49ms
	compilation (LCNF mono) 20.2ms
	congr simp thm 13.1ms
	elaboration 529ms
	fix level params 7.7ms
	import 1.36s
	initialization 26.7ms
	instantiate metavars 6.64ms
	interpretation 536ms
	let-to-have transformation 3.54ms
	linting 35.9ms
	parsing 18.2ms
	process pre-definitions 38.4ms
	share common exprs 18.7ms
	simp 392ms
	tactic execution 538ms
	type checking 438ms
	typeclass inference 2.09s
real 4.32
user 5.83
sys 0.93

LeanPool/Monlib4/LinearAlgebra/MySpec.lean

import took 1.36s
cumulative profiling times:
	attribute application 0.0318ms
	compilation (IR) 0.139ms
	compilation (LCNF base) 2.25ms
	compilation (LCNF impure) 0.821ms
	compilation (LCNF mono) 2.64ms
	congr simp thm 2.34ms
	elaboration 21.1ms
	fix level params 0.961ms
	import 1.36s
	initialization 27ms
	instantiate metavars 1.56ms
	interpretation 173ms
	let-to-have transformation 0.0459ms
	linting 3.68ms
	parsing 2.02ms
	process pre-definitions 2.39ms
	share common exprs 1.92ms
	simp 62ms
	tactic execution 384ms
	type checking 25.4ms
	typeclass inference 479ms
real 2.66
user 2.24
sys 0.89

LeanPool/Monlib4/LinearAlgebra/Nacgor.lean

import took 1.54s
cumulative profiling times:
	attribute application 0.714ms
	blocked (unaccounted) 0.434ms
	compilation (IR) 0.128ms
	compilation (LCNF base) 6.56ms
	compilation (LCNF impure) 0.73ms
	compilation (LCNF mono) 4.54ms
	congr simp thm 0.743ms
	elaboration 118ms
	fix level params 0.139ms
	import 1.54s
	initialization 26.9ms
	instantiate metavars 0.0805ms
	interpretation 193ms
	let-to-have transformation 8.71ms
	linting 1.74ms
	norm_num 1.08ms
	parsing 2.43ms
	process pre-definitions 2.76ms
	share common exprs 0.379ms
	simp 26.6ms
	tactic execution 9.12ms
	type checking 18.8ms
	typeclass inference 137ms
real 2.61
user 1.73
sys 0.97

LeanPool/Monlib4/LinearAlgebra/OfNorm.lean

import took 1.7s
interpretation of Mathlib.Tactic.RingNF._aux_Mathlib_Tactic_Ring_RingNF___elabRules_Mathlib_Tactic_RingNF_ringNF_1._boxed took 112ms
interpretation of Mathlib.Tactic.RingNF._aux_Mathlib_Tactic_Ring_RingNF___elabRules_Mathlib_Tactic_RingNF_ringNF_1._boxed took 163ms
typeclass inference of CoeT took 167ms
typeclass inference of CoeT took 133ms
tactic execution of Lean.Parser.Tactic.exact took 385ms
cumulative profiling times:
	attribute application 1.99ms
	blocked (unaccounted) 82.6ms
	compilation (IR) 1.61ms
	compilation (LCNF base) 33.9ms
	compilation (LCNF impure) 9.42ms
	compilation (LCNF mono) 32.2ms
	congr simp thm 28.4ms
	elaboration 469ms
	fix level params 16.3ms
	import 1.7s
	initialization 26.6ms
	instantiate metavars 16.7ms
	interpretation 1.38s
	let-to-have transformation 1.79ms
	linting 75.4ms
	norm_num 19.1ms
	parsing 53.1ms
	process pre-definitions 72.6ms
	share common exprs 47.5ms
	simp 956ms
	tactic execution 1.68s
	type checking 732ms
	typeclass inference 8.66s
real 8.58
user 15.35
sys 1.19

LeanPool/Monlib4/LinearAlgebra/PiDirectSum.lean

import took 1.28s
elaboration took 150ms
type checking took 189ms
elaboration took 136ms
cumulative profiling times:
	attribute application 22.1ms
	blocked (unaccounted) 27.1ms
	compilation (IR) 0.655ms
	compilation (LCNF base) 28.4ms
	compilation (LCNF impure) 3.45ms
	compilation (LCNF mono) 9.65ms
	congr simp thm 20ms
	dsimp 38ms
	elaboration 597ms
	fix level params 6.8ms
	import 1.28s
	initialization 26.7ms
	instantiate metavars 8.95ms
	interpretation 478ms
	let-to-have transformation 8.22ms
	linting 23.4ms
	parsing 21.4ms
	process pre-definitions 61.4ms
	share common exprs 14.7ms
	simp 671ms
	tactic execution 288ms
	type checking 1.01s
	typeclass inference 3.44s
real 5.44
user 7.80
sys 0.89

LeanPool/Monlib4/LinearAlgebra/PiStarOrderedRing.lean

import took 1.15s
cumulative profiling times:
	attribute application 0.452ms
	compilation (IR) 0.184ms
	compilation (LCNF base) 3.54ms
	compilation (LCNF impure) 1.15ms
	compilation (LCNF mono) 3.42ms
	congr simp thm 7.54ms
	elaboration 46ms
	fix level params 1.33ms
	import 1.15s
	initialization 26.9ms
	instantiate metavars 1.31ms
	interpretation 214ms
	let-to-have transformation 0.129ms
	linting 9.92ms
	parsing 7.79ms
	process pre-definitions 5.01ms
	share common exprs 2.91ms
	simp 70.6ms
	tactic execution 83.2ms
	type checking 47.9ms
	typeclass inference 365ms
real 2.19
user 1.84
sys 0.75

LeanPool/Monlib4/LinearAlgebra/PosMapIsReal.lean

import took 2.03s
typeclass inference of MulHomClass took 164ms
typeclass inference of AddMonoidHomClass took 212ms
typeclass inference of Algebra took 112ms
typeclass inference of OneHomClass took 204ms
typeclass inference of Submodule.HasOrthogonalProjection took 160ms
typeclass inference of CompleteSpace took 126ms
typeclass inference of DistribMulAction took 115ms
typeclass inference of MulHomClass took 229ms
typeclass inference of Algebra took 118ms
typeclass inference of ZeroHomClass took 187ms
typeclass inference of Submodule.HasOrthogonalProjection took 140ms
tactic execution of Lean.Parser.Tactic.rewriteSeq took 163ms
typeclass inference of StarHomClass took 247ms
typeclass inference of DistribMulAction took 108ms
typeclass inference of MulHomClass took 231ms
typeclass inference of ZeroHomClass took 167ms
typeclass inference of MulHomClass took 141ms
tactic execution of Lean.Parser.Tactic.congr took 947ms
tactic execution of Lean.Parser.Tactic.congr took 1.55s
tactic execution of Lean.Parser.Tactic.rewriteSeq took 109ms
tactic execution of Lean.Parser.Tactic.rewriteSeq took 159ms
tactic execution of Lean.Parser.Tactic.rewriteSeq took 113ms
typeclass inference of Star took 102ms
interpretation of Lean.Elab.Tactic._aux_Mathlib_Tactic_Widget_Calc___elabRules_Lean_calcTactic_1._boxed took 152ms
elaboration took 441ms
typeclass inference of StarAddMonoid took 133ms
typeclass inference of StarAddMonoid took 133ms
typeclass inference of StarAddMonoid took 119ms
typeclass inference of StarAddMonoid took 113ms
typeclass inference of StarAddMonoid took 112ms
typeclass inference of StarAddMonoid took 108ms
typeclass inference of StarAddMonoid took 114ms
typeclass inference of StarAddMonoid took 117ms
tactic execution of Lean.Parser.Tactic.rewriteSeq took 220ms
typeclass inference of StarAddMonoid took 132ms
typeclass inference of CoeT took 176ms
tactic execution of Lean.Parser.Tactic.exact took 149ms
typeclass inference of CoeFun took 106ms
typeclass inference of CoeT took 256ms
cumulative profiling times:
	attribute application 30.9ms
	blocked (unaccounted) 4.55s
	compilation (IR) 2.94ms
	compilation (LCNF base) 82.9ms
	compilation (LCNF impure) 16.8ms
	compilation (LCNF mono) 45ms
	congr simp thm 72.5ms
	elaboration 1.82s
	fix level params 27.3ms
	import 2.03s
	initialization 27ms
	instantiate metavars 29.2ms
	interpretation 1.69s
	let-to-have transformation 4.56ms
	linting 141ms
	norm_num 21.5ms
	parsing 71.4ms
	process pre-definitions 93.6ms
	ring 11.6ms
	share common exprs 89.3ms
	simp 2.57s
	tactic execution 7.4s
	type checking 1.73s
	typeclass inference 26.3s
real 20.46
user 43.41
sys 1.47

LeanPool/Monlib4/LinearAlgebra/QuantumSet.lean

import took 2.06s
cumulative profiling times:
	elaboration 0.0755ms
	import 2.06s
	initialization 26.7ms
	interpretation 206ms
	linting 0.0985ms
	parsing 0.00207ms
real 2.90
user 1.74
sys 1.18

LeanPool/Monlib4/LinearAlgebra/QuantumSet/Basic.lean

import took 1.71s
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_NormNum_Core___elabRules_Mathlib_Tactic_normNum_1._boxed took 375ms
typeclass inference of AddHomClass took 600ms
typeclass inference of MulActionHomClass took 591ms
simp took 400ms
typeclass inference of NonUnitalSemiring took 113ms
typeclass inference of AddMonoidHomClass took 146ms
typeclass inference of AddMonoidHomClass took 181ms
typeclass inference of AddMonoidHomClass took 133ms
type checking took 139ms
typeclass inference of NonUnitalNonAssocSemiring took 123ms
typeclass inference of NonUnitalNonAssocSemiring took 110ms
typeclass inference of NonUnitalSemiring took 121ms
typeclass inference of NonUnitalSemiring took 119ms
typeclass inference of AddMonoidHomClass took 201ms
typeclass inference of AddMonoidHomClass took 200ms
typeclass inference of AddMonoidHomClass took 141ms
type checking took 151ms
typeclass inference of CoeT took 217ms
typeclass inference of CoeT took 232ms
typeclass inference of AddMonoidHomClass took 134ms
simp took 110ms
type checking took 106ms
simp took 515ms
tactic execution of Lean.Parser.Tactic.rewriteSeq took 111ms
elaboration took 109ms
typeclass inference of AddMonoidHomClass took 393ms
type checking took 112ms
elaboration took 134ms
type checking took 155ms
typeclass inference of AddMonoidHomClass took 258ms
elaboration took 131ms
tactic execution of Lean.Parser.Tactic.rewriteSeq took 101ms
typeclass inference of NonUnitalNonAssocSemiring took 193ms
typeclass inference of NonUnitalSemiring took 190ms
typeclass inference of AddMonoidHomClass took 277ms
typeclass inference of MulActionHomClass took 262ms
type checking took 154ms
cumulative profiling times:
	aesop 98.1ms
	attribute application 189ms
	blocked (unaccounted) 1.65s
	compilation (IR) 2.19ms
	compilation (LCNF base) 41.7ms
	compilation (LCNF impure) 12.9ms
	compilation (LCNF mono) 35.7ms
	congr simp thm 146ms
	dsimp 48.4ms
	elaboration 2.3s
	fix level params 44.1ms
	import 1.71s
	initialization 26.5ms
	instantiate metavars 42.5ms
	interpretation 1.85s
	let-to-have transformation 16.3ms
	linting 95.2ms
	norm_num 10.8ms
	parsing 60.8ms
	process pre-definitions 161ms
	ring 2.18ms
	share common exprs 117ms
	simp 6.9s
	tactic execution 3.99s
	type checking 3.44s
	typeclass inference 24.5s
real 22.53
user 45.09
sys 1.31

LeanPool/Monlib4/LinearAlgebra/QuantumSet/DeltaForm.lean

import took 1.72s
cumulative profiling times:
	attribute application 0.991ms
	blocked (unaccounted) 5.57ms
	elaboration 25.9ms
	fix level params 0.136ms
	import 1.72s
	initialization 26.6ms
	instantiate metavars 0.134ms
	interpretation 192ms
	let-to-have transformation 0.0223ms
	linting 1.11ms
	parsing 1.05ms
	process pre-definitions 2.25ms
	share common exprs 0.254ms
	tactic execution 20.3ms
	type checking 60.7ms
	typeclass inference 106ms
real 2.68
user 1.65
sys 1.09

LeanPool/Monlib4/LinearAlgebra/QuantumSet/Instances.lean

import took 2.03s
tactic execution of Lean.Parser.Tactic.rewriteSeq took 252ms
tactic execution of Lean.Parser.Tactic.rewriteSeq took 123ms
tactic execution of Lean.Parser.Tactic.rewriteSeq took 298ms
tactic execution of Lean.Parser.Tactic.exact took 128ms
tactic execution of Lean.Parser.Tactic.exact took 156ms
tactic execution of Lean.Parser.Tactic.change took 159ms
tactic execution of Lean.Parser.Tactic.rewriteSeq took 120ms
tactic execution of Lean.Parser.Tactic.change took 152ms
type checking took 104ms
tactic execution of Lean.Parser.Tactic.exact took 162ms
tactic execution of Lean.Parser.Tactic.change took 156ms
tactic execution of Lean.Parser.Tactic.exact took 163ms
cumulative profiling times:
	aesop 36.5ms
	attribute application 4.9ms
	blocked (unaccounted) 799ms
	compilation (IR) 2.32ms
	compilation (LCNF base) 50.3ms
	compilation (LCNF impure) 14.1ms
	compilation (LCNF mono) 36.2ms
	congr simp thm 48.7ms
	elaboration 744ms
	fix level params 12.9ms
	import 2.03s
	initialization 26.7ms
	instantiate metavars 19.9ms
	interpretation 925ms
	let-to-have transformation 18.2ms
	linting 65.6ms
	norm_num 0.388ms
	parsing 50ms
	process pre-definitions 78.3ms
	share common exprs 39.9ms
	simp 1.62s
	tactic execution 3.78s
	type checking 1.07s
	typeclass inference 5.72s
real 8.88
user 15.62
sys 1.35

LeanPool/Monlib4/LinearAlgebra/QuantumSet/PhiMap.lean

import took 1.74s
cumulative profiling times:
	attribute application 5.67ms
	blocked (unaccounted) 0.121ms
	compilation (IR) 0.143ms
	compilation (LCNF base) 1.75ms
	compilation (LCNF impure) 0.653ms
	compilation (LCNF mono) 1.84ms
	congr simp thm 8.06ms
	elaboration 69.9ms
	fix level params 2.11ms
	import 1.74s
	initialization 27.4ms
	instantiate metavars 1.72ms
	interpretation 201ms
	let-to-have transformation 0.477ms
	linting 4.83ms
	parsing 2.18ms
	process pre-definitions 7.87ms
	share common exprs 4.81ms
	simp 230ms
	tactic execution 207ms
	type checking 141ms
	typeclass inference 807ms
real 3.51
user 3.03
sys 1.06

LeanPool/Monlib4/LinearAlgebra/QuantumSet/Pi.lean

import took 1.73s
simp took 404ms
simp took 260ms
simp took 256ms
tactic execution of Lean.Parser.Tactic.exact took 161ms
cumulative profiling times:
	attribute application 14.9ms
	compilation (IR) 0.114ms
	compilation (LCNF base) 3.69ms
	compilation (LCNF impure) 0.449ms
	compilation (LCNF mono) 4.02ms
	congr simp thm 1.49ms
	elaboration 315ms
	fix level params 1.09ms
	import 1.73s
	initialization 26.6ms
	instantiate metavars 1.57ms
	interpretation 308ms
	let-to-have transformation 1.18ms
	linting 8.65ms
	parsing 9ms
	process pre-definitions 19.3ms
	share common exprs 3.14ms
	simp 998ms
	tactic execution 275ms
	type checking 174ms
	typeclass inference 459ms
real 4.64
user 3.89
sys 1.05

LeanPool/Monlib4/LinearAlgebra/QuantumSet/QIso.lean

import took 1.76s
elaboration took 109ms
tactic execution of Lean.Parser.Tactic.rewriteSeq took 113ms
tactic execution of Lean.Parser.Tactic.rewriteSeq took 128ms
tactic execution of Lean.Parser.Tactic.rewriteSeq took 412ms
tactic execution of Lean.Parser.Tactic.rewriteSeq took 448ms
tactic execution of Lean.Parser.Tactic.rewriteSeq took 598ms
tactic execution of Lean.Parser.Tactic.rewriteSeq took 604ms
tactic execution of Lean.Parser.Tactic.rewriteSeq took 662ms
tactic execution of Lean.Parser.Tactic.rewriteSeq took 313ms
simp took 159ms
tactic execution of Lean.Parser.Tactic.rewriteSeq took 248ms
tactic execution of Lean.Parser.Tactic.congr took 1.36s
type checking took 487ms
typeclass inference of AddMonoidHomClass took 112ms
simp took 125ms
simp took 127ms
type checking took 104ms
simp took 119ms
tactic execution of Lean.Parser.Tactic.rewriteSeq took 225ms
tactic execution of Lean.Parser.Tactic.rewriteSeq took 131ms
tactic execution of Lean.Parser.Tactic.rewriteSeq took 280ms
tactic execution of Lean.Parser.Tactic.rewriteSeq took 131ms
tactic execution of Lean.Parser.Tactic.rewriteSeq took 626ms
tactic execution of Lean.Parser.Tactic.rewriteSeq took 210ms
simp took 102ms
typeclass inference of AddMonoidHomClass took 124ms
typeclass inference of AddMonoidHomClass took 113ms
typeclass inference of AddMonoidHomClass took 116ms
simp took 144ms
type checking took 558ms
simp took 126ms
tactic execution of Lean.Parser.Tactic.rewriteSeq took 330ms
tactic execution of Lean.Parser.Tactic.rewriteSeq took 477ms
tactic execution of Lean.Parser.Tactic.rewriteSeq took 278ms
tactic execution of Lean.Parser.Tactic.rewriteSeq took 247ms
tactic execution of Lean.Parser.Tactic.rewriteSeq took 121ms
simp took 115ms
typeclass inference of AddMonoidHomClass took 160ms
typeclass inference of AddMonoidHomClass took 155ms
simp took 344ms
tactic execution of Mathlib.Tactic.convert took 1.48s
tactic execution of Lean.Parser.Tactic.congr took 193ms
simp took 101ms
interpretation of Lean.Elab.Tactic._aux_Mathlib_Tactic_Widget_Calc___elabRules_Lean_calcTactic_1._boxed took 1.12s
type checking took 559ms
tactic execution of Lean.Parser.Tactic.refine took 109ms
simp took 133ms
tactic execution of Lean.Parser.Tactic.congr took 317ms
type checking took 134ms
LeanPool/Monlib4/LinearAlgebra/QuantumSet/QIso.lean:439:2: error: Type mismatch: After simplification, term
  Eq.symm this
 has type
  rT B₂ P ∘ₗ ↑(ϰ B₁ H B₂).symm ∘ₗ lT B₁ P ∘ₗ ↑(ϰ B₁ B₁ H) ∘ₗ rT H (LinearMap.adjoint (LinearMap.mul' ℂ B₁)) =
    LinearMap.adjoint (lT H (LinearMap.mul' ℂ B₂) ∘ₗ ↑(ϰ H B₂ B₂)) ∘ₗ P
but is expected to have type
  rT B₂ P ∘ₗ ↑(ϰ B₁ H B₂).symm ∘ₗ lT B₁ P ∘ₗ ↑(ϰ B₁ B₁ H) ∘ₗ rT H (LinearMap.adjoint (LinearMap.mul' ℂ B₁)) =
    ↑(ϰ H B₂ B₂).symm ∘ₗ lT H (LinearMap.adjoint (LinearMap.mul' ℂ B₂)) ∘ₗ P
tactic execution of Lean.Parser.Tactic.refine took 147ms
tactic execution of Lean.Parser.Tactic.rewriteSeq took 167ms
tactic execution of Lean.Parser.Tactic.rewriteSeq took 434ms
tactic execution of Lean.Parser.Tactic.rewriteSeq took 530ms
tactic execution of Lean.Parser.Tactic.rewriteSeq took 601ms
tactic execution of Lean.Parser.Tactic.rewriteSeq took 589ms
simp took 159ms
tactic execution of Lean.Parser.Tactic.rewriteSeq took 1.05s
tactic execution of Lean.Parser.Tactic.rewriteSeq took 420ms
type checking took 309ms
elaboration took 247ms
tactic execution of Lean.Parser.Tactic.rewriteSeq took 352ms
tactic execution of Lean.Parser.Tactic.congr took 265ms
tactic execution of Lean.Parser.Tactic.rewriteSeq took 316ms
tactic execution of Lean.Parser.Tactic.congr took 142ms
elaboration took 191ms
type checking took 107ms
tactic execution of Lean.Parser.Tactic.rewriteSeq took 269ms
tactic execution of Lean.Parser.Tactic.rewriteSeq took 162ms
cumulative profiling times:
	attribute application 53.3ms
	blocked (unaccounted) 6.56s
	compilation (IR) 2.81ms
	compilation (LCNF base) 154ms
	compilation (LCNF impure) 15.5ms
	compilation (LCNF mono) 44.8ms
	congr simp thm 205ms
	elaboration 2.24s
	fix level params 32.3ms
	import 1.76s
	initialization 26.5ms
	instantiate metavars 24.4ms
	interpretation 1.97s
	let-to-have transformation 4.84ms
	linting 121ms
	parsing 35.3ms
	process pre-definitions 116ms
	share common exprs 84.6ms
	simp 4.54s
	tactic execution 17.9s
	type checking 3.5s
	typeclass inference 21.7s
real 27.40
user 53.91
sys 1.38
error: profile command exited with status 1

LeanPool/Monlib4/LinearAlgebra/QuantumSet/SchurMul.lean

import took 1.74s
tactic execution of Lean.Parser.Tactic.rewriteSeq took 123ms
elaboration took 272ms
tactic execution of Lean.Parser.Tactic.rewriteSeq took 139ms
type checking took 101ms
interpretation of Lean.Elab.Tactic._aux_Mathlib_Tactic_Widget_Calc___elabRules_Lean_calcTactic_1._boxed took 110ms
simp took 125ms
simp took 134ms
tactic execution of Lean.Parser.Tactic.simpa took 140ms
elaboration took 179ms
cumulative profiling times:
	aesop 28.5ms
	attribute application 1.31ms
	blocked (unaccounted) 208ms
	compilation (IR) 1.69ms
	compilation (LCNF base) 55.3ms
	compilation (LCNF impure) 8.59ms
	compilation (LCNF mono) 23ms
	congr simp thm 77.5ms
	elaboration 1.68s
	fix level params 20ms
	import 1.74s
	initialization 26.8ms
	instantiate metavars 14.4ms
	interpretation 971ms
	let-to-have transformation 6.46ms
	linting 36.6ms
	parsing 22.6ms
	process pre-definitions 74.3ms
	share common exprs 55.5ms
	simp 1.9s
	tactic execution 2.47s
	type checking 1.62s
	typeclass inference 30s
real 28.92
user 40.36
sys 1.16

LeanPool/Monlib4/LinearAlgebra/QuantumSet/SchurMulTensor.lean

import took 1.73s
tactic execution of Lean.Parser.Tactic.rewriteSeq took 101ms
cumulative profiling times:
	attribute application 0.0247ms
	compilation (IR) 0.0369ms
	compilation (LCNF base) 0.486ms
	compilation (LCNF impure) 0.207ms
	compilation (LCNF mono) 0.429ms
	congr simp thm 6.94ms
	elaboration 46.5ms
	fix level params 1.09ms
	import 1.73s
	initialization 26.7ms
	instantiate metavars 0.713ms
	interpretation 205ms
	let-to-have transformation 0.16ms
	linting 1.63ms
	parsing 1.68ms
	process pre-definitions 1.96ms
	share common exprs 2.72ms
	simp 50.1ms
	tactic execution 279ms
	type checking 134ms
	typeclass inference 617ms
real 3.56
user 2.67
sys 1.04

LeanPool/Monlib4/LinearAlgebra/QuantumSet/Subset.lean

import took 1.75s
simp took 160ms
tactic execution of Lean.Parser.Tactic.rewriteSeq took 128ms
tactic execution of Lean.Parser.Tactic.rewriteSeq took 121ms
typeclass inference of FiniteDimensional took 128ms
elaboration took 143ms
typeclass inference of FiniteDimensional took 128ms
tactic execution of Lean.Parser.Tactic.refine took 1.61s
simp took 246ms
tactic execution of Lean.Parser.Tactic.change took 321ms
type checking took 160ms
simp took 119ms
tactic execution of Lean.Parser.Tactic.congr took 110ms
simp took 130ms
type checking took 165ms
simp took 119ms
simp took 244ms
tactic execution of Lean.Parser.Tactic.rewriteSeq took 125ms
tactic execution of Lean.Parser.Tactic.exact took 269ms
cumulative profiling times:
	aesop 14.2ms
	attribute application 46.6ms
	compilation (IR) 1.17ms
	compilation (LCNF base) 13.3ms
	compilation (LCNF impure) 5.52ms
	compilation (LCNF mono) 13.5ms
	congr simp thm 42ms
	elaboration 1.01s
	fix level params 10.4ms
	import 1.75s
	initialization 26.8ms
	instantiate metavars 10.6ms
	interpretation 722ms
	let-to-have transformation 39.4ms
	linting 35.7ms
	norm_num 0.715ms
	parsing 34.9ms
	process pre-definitions 45.9ms
	share common exprs 31.1ms
	simp 1.84s
	tactic execution 3.67s
	type checking 1.06s
	typeclass inference 5.62s
real 10.56
user 15.58
sys 1.12

LeanPool/Monlib4/LinearAlgebra/QuantumSet/Symm.lean

import took 1.74s
elaboration took 135ms
typeclass inference of NonUnitalNonAssocSemiring took 216ms
typeclass inference of NonUnitalNonAssocSemiring took 125ms
typeclass inference of NonUnitalSemiring took 298ms
typeclass inference of NonUnitalSemiring took 121ms
typeclass inference of AddMonoidHomClass took 255ms
typeclass inference of AddMonoidHomClass took 140ms
type checking took 278ms
elaboration took 189ms
typeclass inference of NonUnitalNonAssocSemiring took 128ms
typeclass inference of NonUnitalNonAssocSemiring took 305ms
typeclass inference of NonUnitalSemiring took 127ms
typeclass inference of NonUnitalSemiring took 300ms
typeclass inference of AddMonoidHomClass took 436ms
typeclass inference of AddMonoidHomClass took 135ms
type checking took 178ms
typeclass inference of AddMonoidHomClass took 132ms
typeclass inference of AddMonoidHomClass took 123ms
simp took 113ms
typeclass inference of AddMonoidHomClass took 133ms
typeclass inference of AddMonoidHomClass took 134ms
typeclass inference of AddMonoidHomClass took 133ms
typeclass inference of AddMonoidHomClass took 381ms
simp took 131ms
tactic execution of Lean.Parser.Tactic.refine took 181ms
typeclass inference of AddMonoidHomClass took 123ms
typeclass inference of AddMonoidHomClass took 126ms
cumulative profiling times:
	attribute application 131ms
	blocked (unaccounted) 353ms
	compilation (IR) 3.53ms
	compilation (LCNF base) 161ms
	compilation (LCNF impure) 20.8ms
	compilation (LCNF mono) 59.6ms
	congr simp thm 113ms
	elaboration 1.74s
	fix level params 27.9ms
	import 1.74s
	initialization 26.7ms
	instantiate metavars 35.3ms
	interpretation 883ms
	let-to-have transformation 7.34ms
	linting 37.4ms
	norm_num 1.84ms
	parsing 26.1ms
	process pre-definitions 96.5ms
	share common exprs 88.2ms
	simp 4.12s
	tactic execution 2.43s
	type checking 1.65s
	typeclass inference 15.6s
real 12.64
user 28.45
sys 1.20

LeanPool/Monlib4/LinearAlgebra/QuantumSet/TensorProduct.lean

import took 1.72s
typeclass inference of AddHomClass took 109ms
elaboration took 239ms
elaboration took 127ms
tactic execution of Lean.Parser.Tactic.exact took 260ms
typeclass inference of AddHomClass took 341ms
typeclass inference of AddHomClass took 333ms
elaboration took 393ms
tactic execution of Lean.Parser.Tactic.rewriteSeq took 741ms
type checking took 138ms
elaboration took 135ms
attribute application took 259ms
elaboration took 729ms
type checking took 101ms
type checking took 146ms
cumulative profiling times:
	aesop 14.4ms
	attribute application 317ms
	compilation (IR) 0.204ms
	compilation (LCNF base) 2.89ms
	compilation (LCNF impure) 1.14ms
	compilation (LCNF mono) 3.11ms
	congr simp thm 25ms
	elaboration 1.85s
	fix level params 5.72ms
	import 1.72s
	initialization 26.5ms
	instantiate metavars 6.11ms
	interpretation 339ms
	let-to-have transformation 5.43ms
	linting 27.3ms
	parsing 11.8ms
	process pre-definitions 37.3ms
	share common exprs 14ms
	simp 843ms
	tactic execution 1.23s
	type checking 1.11s
	typeclass inference 4.3s
real 9.35
user 11.36
sys 1.13

LeanPool/Monlib4/LinearAlgebra/TensorProduct.lean

import took 1.76s
cumulative profiling times:
	elaboration 0.16ms
	import 1.76s
	initialization 26.7ms
	interpretation 179ms
	linting 0.208ms
	parsing 0.0285ms
real 2.55
user 1.54
sys 1.03

LeanPool/Monlib4/LinearAlgebra/TensorProduct/BasicLemmas.lean

import took 1.27s
cumulative profiling times:
	attribute application 28.5ms
	blocked (unaccounted) 0.148ms
	compilation (IR) 0.511ms
	compilation (LCNF base) 8.5ms
	compilation (LCNF impure) 3.13ms
	compilation (LCNF mono) 10.1ms
	congr simp thm 31.1ms
	elaboration 386ms
	fix level params 6.32ms
	import 1.27s
	initialization 26.5ms
	instantiate metavars 3.44ms
	interpretation 377ms
	let-to-have transformation 1.67ms
	linting 19.8ms
	parsing 16.3ms
	process pre-definitions 11.9ms
	share common exprs 13.1ms
	simp 701ms
	tactic execution 190ms
	type checking 396ms
	typeclass inference 1.43s
real 3.54
user 4.62
sys 0.89

LeanPool/Monlib4/LinearAlgebra/TensorProduct/FiniteDimensional.lean

import took 1.66s
elaboration took 284ms
typeclass inference of AddHomClass took 143ms
typeclass inference of AddHomClass took 131ms
typeclass inference of AddHomClass took 139ms
typeclass inference of AddHomClass took 127ms
cumulative profiling times:
	attribute application 20.6ms
	congr simp thm 20.9ms
	elaboration 819ms
	fix level params 4.74ms
	import 1.66s
	initialization 27.1ms
	instantiate metavars 1.97ms
	interpretation 375ms
	let-to-have transformation 2.38ms
	linting 21.1ms
	parsing 13ms
	process pre-definitions 20.6ms
	share common exprs 9.02ms
	simp 357ms
	tactic execution 78.7ms
	type checking 547ms
	typeclass inference 8.3s
real 11.31
user 11.89
sys 1.04

LeanPool/Monlib4/LinearAlgebra/TensorProduct/Lemmas.lean

import took 1.28s
simp took 104ms
cumulative profiling times:
	attribute application 80.2ms
	blocked (unaccounted) 65.4ms
	compilation (IR) 0.498ms
	compilation (LCNF base) 16.2ms
	compilation (LCNF impure) 2.83ms
	compilation (LCNF mono) 7.53ms
	congr simp thm 42ms
	dsimp 4.68ms
	elaboration 380ms
	fix level params 2.96ms
	import 1.28s
	initialization 26.7ms
	instantiate metavars 2.96ms
	interpretation 269ms
	let-to-have transformation 3.09ms
	linting 17.1ms
	parsing 9.6ms
	process pre-definitions 24.3ms
	share common exprs 6.41ms
	simp 396ms
	tactic execution 89ms
	type checking 469ms
	typeclass inference 1.02s
real 3.45
user 3.89
sys 0.87

LeanPool/Monlib4/LinearAlgebra/TensorProduct/OrthonormalBasis.lean

import took 1.68s
cumulative profiling times:
	attribute application 0.0153ms
	elaboration 58.4ms
	fix level params 0.111ms
	import 1.68s
	initialization 26.8ms
	instantiate metavars 0.0306ms
	interpretation 203ms
	let-to-have transformation 0.606ms
	linting 0.982ms
	parsing 1.12ms
	process pre-definitions 0.164ms
	share common exprs 0.252ms
	type checking 4.96ms
	typeclass inference 52.3ms
real 2.57
user 1.59
sys 1.02

LeanPool/Monlib4/LinearAlgebra/TensorProduct/Submodule.lean

import took 1.75s
tactic execution of Lean.Parser.Tactic.congr took 143ms
simp took 136ms
tactic execution of Lean.Parser.Tactic.rewriteSeq took 475ms
typeclass inference of Submodule.HasOrthogonalProjection took 154ms
typeclass inference of Submodule.HasOrthogonalProjection took 128ms
simp took 146ms
typeclass inference of AddMonoidHomClass took 258ms
let-to-have transformation took 327ms
interpretation of simpsTacFromSyntax._boxed took 113ms
elaboration took 181ms
elaboration took 105ms
elaboration took 114ms
elaboration took 164ms
cumulative profiling times:
	attribute application 1.98ms
	blocked (unaccounted) 320ms
	compilation (IR) 0.711ms
	compilation (LCNF base) 23ms
	compilation (LCNF impure) 4.55ms
	compilation (LCNF mono) 12.1ms
	congr simp thm 38.3ms
	dsimp 149ms
	elaboration 1.3s
	fix level params 13.2ms
	import 1.75s
	initialization 27ms
	instantiate metavars 8.32ms
	interpretation 832ms
	let-to-have transformation 335ms
	linting 33.4ms
	norm_num 2.01ms
	parsing 25.4ms
	process pre-definitions 75.4ms
	share common exprs 28.6ms
	simp 1.55s
	tactic execution 1.39s
	type checking 1.15s
	typeclass inference 10.3s
real 11.35
user 18.65
sys 1.15

LeanPool/Monlib4/LinearAlgebra/ToMatrixOfEquiv.lean

import took 2.06s
simp took 164ms
typeclass inference of FiniteDimensional took 112ms
typeclass inference of Star took 118ms
elaboration took 120ms
tactic execution of Lean.Parser.Tactic.change took 347ms
tactic execution of Lean.Parser.Tactic.rewriteSeq took 134ms
tactic execution of Lean.Parser.Tactic.rewriteSeq took 135ms
type checking took 181ms
elaboration took 129ms
elaboration took 106ms
cumulative profiling times:
	attribute application 140ms
	blocked (unaccounted) 0.391ms
	compilation (IR) 0.615ms
	compilation (LCNF base) 13.7ms
	compilation (LCNF impure) 3.36ms
	compilation (LCNF mono) 11.4ms
	congr simp thm 31.6ms
	elaboration 887ms
	fix level params 7.78ms
	import 2.06s
	initialization 26.8ms
	instantiate metavars 8.83ms
	interpretation 519ms
	let-to-have transformation 5.61ms
	linting 27.9ms
	parsing 17.3ms
	process pre-definitions 37.8ms
	share common exprs 17.7ms
	simp 1.75s
	tactic execution 917ms
	type checking 677ms
	typeclass inference 3.95s
real 7.74
user 10.52
sys 1.23

LeanPool/Monlib4/Monlib.lean

import took 2.14s
cumulative profiling times:
	elaboration 0.135ms
	import 2.14s
	initialization 27ms
	interpretation 224ms
	linting 0.23ms
	parsing 0.0274ms
real 3.01
user 1.80
sys 1.22

LeanPool/Monlib4/Other.lean

import took 2.08s
cumulative profiling times:
	elaboration 0.183ms
	import 2.08s
	initialization 27.1ms
	interpretation 218ms
	linting 0.238ms
	parsing 0.0301ms
real 2.96
user 1.82
sys 1.15

LeanPool/Monlib4/Other/Sonia.lean

import took 2.05s
cumulative profiling times:
	attribute application 0.0786ms
	compilation (IR) 0.276ms
	compilation (LCNF base) 5.17ms
	compilation (LCNF impure) 1.89ms
	compilation (LCNF mono) 6.17ms
	congr simp thm 2.43ms
	elaboration 33.3ms
	fix level params 0.242ms
	import 2.05s
	initialization 27.1ms
	instantiate metavars 0.695ms
	interpretation 303ms
	let-to-have transformation 0.0687ms
	linting 6.88ms
	parsing 5.99ms
	process pre-definitions 2.47ms
	share common exprs 1.55ms
	simp 91.1ms
	tactic execution 62.2ms
	type checking 13.4ms
	typeclass inference 59.4ms
real 3.08
user 2.12
sys 1.19

LeanPool/Monlib4/Preq.lean

import took 1.74s
cumulative profiling times:
	elaboration 0.187ms
	import 1.74s
	initialization 26.5ms
	interpretation 177ms
	linting 0.22ms
	parsing 0.0261ms
real 2.53
user 1.48
sys 1.06

LeanPool/Monlib4/Preq/Complex.lean

import took 1.37s
cumulative profiling times:
	attribute application 0.0839ms
	compilation (IR) 0.974ms
	compilation (LCNF base) 14.3ms
	compilation (LCNF impure) 5.56ms
	compilation (LCNF mono) 16.6ms
	congr simp thm 13.2ms
	elaboration 58.8ms
	fix level params 1.72ms
	import 1.37s
	initialization 26.7ms
	instantiate metavars 4.47ms
	interpretation 425ms
	let-to-have transformation 0.135ms
	linting 12.2ms
	norm_num 1.49ms
	parsing 15.1ms
	process pre-definitions 12.3ms
	share common exprs 12.8ms
	simp 845ms
	tactic execution 289ms
	type checking 79.1ms
	typeclass inference 409ms
real 2.89
user 3.26
sys 0.90

LeanPool/Monlib4/Preq/Dite.lean

import took 1.21s
cumulative profiling times:
	aesop 34ms
	attribute application 0.116ms
	congr simp thm 3.59ms
	elaboration 35ms
	fix level params 0.715ms
	import 1.21s
	initialization 27.2ms
	instantiate metavars 0.729ms
	interpretation 236ms
	let-to-have transformation 0.151ms
	linting 6.36ms
	parsing 6.95ms
	process pre-definitions 2.62ms
	share common exprs 1.68ms
	simp 53.8ms
	tactic execution 21.2ms
	type checking 13ms
	typeclass inference 81.4ms
real 2.08
user 1.50
sys 0.81

LeanPool/Monlib4/Preq/Equiv.lean

import took 1.76s
cumulative profiling times:
	attribute application 0.0111ms
	congr simp thm 1.13ms
	elaboration 4.2ms
	fix level params 0.235ms
	import 1.76s
	initialization 27.5ms
	instantiate metavars 0.338ms
	interpretation 178ms
	let-to-have transformation 0.0153ms
	linting 0.58ms
	parsing 0.438ms
	process pre-definitions 0.602ms
	share common exprs 0.619ms
	simp 58.2ms
	tactic execution 8.29ms
	type checking 5.86ms
	typeclass inference 121ms
real 2.81
user 1.76
sys 1.06

LeanPool/Monlib4/Preq/Finset.lean

import took 1.1s
cumulative profiling times:
	attribute application 0.104ms
	compilation (IR) 0.141ms
	compilation (LCNF base) 3.04ms
	compilation (LCNF impure) 0.982ms
	compilation (LCNF mono) 2.24ms
	elaboration 42.2ms
	fix level params 0.671ms
	import 1.1s
	initialization 26.7ms
	instantiate metavars 0.717ms
	interpretation 245ms
	let-to-have transformation 0.129ms
	linting 7.32ms
	parsing 5.83ms
	process pre-definitions 2.21ms
	share common exprs 1.45ms
	tactic execution 68ms
	type checking 8.45ms
	typeclass inference 10.6ms
real 1.85
user 1.32
sys 0.75

LeanPool/Monlib4/Preq/Ites.lean

import took 1.22s
cumulative profiling times:
	attribute application 0.537ms
	blocked (unaccounted) 48.1ms
	compilation (IR) 0.384ms
	compilation (LCNF base) 14.3ms
	compilation (LCNF impure) 2.42ms
	compilation (LCNF mono) 5.92ms
	congr simp thm 1.31ms
	elaboration 39.3ms
	fix level params 0.36ms
	import 1.22s
	initialization 27.3ms
	instantiate metavars 0.315ms
	interpretation 164ms
	let-to-have transformation 0.0798ms
	linting 3.87ms
	parsing 2.28ms
	process pre-definitions 2.66ms
	share common exprs 0.973ms
	simp 26.2ms
	tactic execution 17.1ms
	type checking 5.24ms
	typeclass inference 47.9ms
real 2.08
user 1.39
sys 0.79

LeanPool/Monlib4/Preq/RCLikeLe.lean

import took 1.49s
cumulative profiling times:
	attribute application 0.123ms
	compilation (IR) 0.115ms
	compilation (LCNF base) 1.99ms
	compilation (LCNF impure) 0.71ms
	compilation (LCNF mono) 2.1ms
	congr simp thm 1.37ms
	elaboration 29.8ms
	fix level params 0.604ms
	import 1.49s
	initialization 26.9ms
	instantiate metavars 0.365ms
	interpretation 251ms
	let-to-have transformation 0.119ms
	linting 4ms
	parsing 3.17ms
	process pre-definitions 2.1ms
	share common exprs 1.83ms
	simp 45.5ms
	tactic execution 30.3ms
	type checking 19.7ms
	typeclass inference 148ms
real 2.42
user 1.69
sys 0.94

LeanPool/Monlib4/Preq/Set.lean

import took 974ms
cumulative profiling times:
	elaboration 0.143ms
	import 974ms
	initialization 27.4ms
	interpretation 73.6ms
	linting 0.183ms
	parsing 0.0297ms
real 1.62
user 0.94
sys 0.69

LeanPool/Monlib4/Preq/StarAlgEquiv.lean

import took 1.21s
cumulative profiling times:
	attribute application 9.53ms
	blocked (unaccounted) 0.329ms
	compilation (IR) 0.415ms
	compilation (LCNF base) 9.2ms
	compilation (LCNF impure) 2.15ms
	compilation (LCNF mono) 6.79ms
	congr simp thm 8.89ms
	elaboration 190ms
	fix level params 2.79ms
	import 1.21s
	initialization 26.8ms
	instantiate metavars 1.56ms
	interpretation 357ms
	let-to-have transformation 1.31ms
	linting 17.8ms
	parsing 17.2ms
	process pre-definitions 16.6ms
	share common exprs 6.34ms
	simp 117ms
	tactic execution 109ms
	type checking 108ms
	typeclass inference 1.08s
real 2.95
user 3.13
sys 0.79

LeanPool/Monlib4/QuantumGraph.lean

import took 2.17s
cumulative profiling times:
	elaboration 0.066ms
	import 2.17s
	initialization 26.9ms
	interpretation 215ms
	linting 0.205ms
	parsing 0.00178ms
real 3.06
user 1.85
sys 1.22

LeanPool/Monlib4/QuantumGraph/Basic.lean

import took 2.15s
tactic execution of Lean.Parser.Tactic.rewriteSeq took 110ms
simp took 117ms
tactic execution of Lean.Parser.Tactic.obtain took 103ms
typeclass inference of AddMonoidHomClass took 139ms
typeclass inference of AddMonoidHomClass took 148ms
simp took 164ms
type checking took 154ms
tactic execution of Lean.Parser.Tactic.rewriteSeq took 371ms
typeclass inference of AddHomClass took 417ms
simp took 158ms
typeclass inference of LinearMapClass took 390ms
type checking took 175ms
type checking took 128ms
elaboration took 190ms
simp took 182ms
type checking took 118ms
interpretation of Lean.Elab.Tactic._aux_Mathlib_Tactic_Widget_Calc___elabRules_Lean_calcTactic_1._boxed took 250ms
tactic execution of Lean.Parser.Tactic.congr took 251ms
typeclass inference of Star took 108ms
simp took 112ms
tactic execution of Lean.Parser.Tactic.rewriteSeq took 311ms
tactic execution of Lean.Parser.Tactic.rewriteSeq took 176ms
typeclass inference of Star took 111ms
typeclass inference of Star took 106ms
typeclass inference of FiniteDimensional took 125ms
elaboration took 262ms
tactic execution of Lean.Parser.Tactic.refine took 125ms
typeclass inference of AddMonoidHomClass took 264ms
typeclass inference of AddMonoidHomClass took 124ms
simp took 181ms
tactic execution of Lean.Parser.Tactic.congr took 282ms
tactic execution of Lean.Parser.Tactic.congr took 153ms
typeclass inference of AddMonoidHomClass took 104ms
interpretation of Lean.Elab.Tactic._aux_Mathlib_Tactic_Widget_Calc___elabRules_Lean_calcTactic_1._boxed took 431ms
simp took 154ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_NormNum_Core___elabRules_Mathlib_Tactic_normNum_1._boxed took 149ms
simp took 153ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_NormNum_Core___elabRules_Mathlib_Tactic_normNum_1._boxed took 151ms
simp took 143ms
tactic execution of Lean.Parser.Tactic.obtain took 129ms
tactic execution of Lean.Parser.Tactic.obtain took 111ms
typeclass inference of AddMonoidHomClass took 134ms
typeclass inference of SeminormedAddCommGroup took 108ms
typeclass inference of AddMonoidHomClass took 376ms
simp took 479ms
type checking took 162ms
elaboration took 253ms
typeclass inference of CompleteSpace took 124ms
tactic execution of Lean.Parser.Tactic.rewriteSeq took 355ms
type checking took 108ms
tactic execution of Lean.Parser.Tactic.rewriteSeq took 157ms
typeclass inference of AddHomClass took 116ms
typeclass inference of CompleteSpace took 111ms
elaboration took 125ms
elaboration took 109ms
elaboration took 133ms
tactic execution of Lean.Parser.Tactic.eqRefl took 138ms
typeclass inference of AddCommMonoid took 585ms
typeclass inference of MulActionHomClass took 125ms
typeclass inference of AddMonoidHomClass took 141ms
typeclass inference of CompleteSpace took 230ms
type checking took 200ms
typeclass inference of AddCommMonoid took 657ms
tactic execution of Lean.Parser.Tactic.rewriteSeq took 102ms
simp took 245ms
typeclass inference of MulActionHomClass took 100ms
typeclass inference of AddCommMonoid took 630ms
typeclass inference of CompleteSpace took 213ms
simp took 149ms
type checking took 155ms
tactic execution of Lean.Parser.Tactic.rewriteSeq took 113ms
simp took 174ms
simp took 138ms
elaboration took 612ms
typeclass inference of AddMonoidHomClass took 144ms
typeclass inference of AddCommMonoid took 606ms
simp took 404ms
simp took 134ms
simp took 134ms
simp took 139ms
typeclass inference of LinearMapClass took 112ms
simp took 128ms
simp took 154ms
simp took 128ms
simp took 113ms
simp took 114ms
simp took 110ms
type checking took 195ms
tactic execution of Lean.Parser.Tactic.rewriteSeq took 171ms
tactic execution of Lean.Parser.Tactic.rewriteSeq took 116ms
tactic execution of Lean.Parser.Tactic.rewriteSeq took 101ms
tactic execution of Lean.Parser.Tactic.congr took 421ms
simp took 153ms
type checking took 169ms
typeclass inference of ZeroHomClass took 285ms
typeclass inference of ZeroHomClass took 277ms
tactic execution of Lean.Parser.Tactic.rewriteSeq took 107ms
typeclass inference of AddHomClass took 146ms
typeclass inference of AddHomClass took 221ms
typeclass inference of AddHomClass took 177ms
type checking took 123ms
typeclass inference of CompleteSpace took 107ms
typeclass inference of CompleteSpace took 283ms
typeclass inference of CompleteSpace took 348ms
tactic execution of Lean.Parser.Tactic.rewriteSeq took 1.08s
tactic execution of Lean.Parser.Tactic.rewriteSeq took 187ms
simp took 126ms
tactic execution of Lean.Parser.Tactic.rewriteSeq took 220ms
interpretation of Lean.Elab.Tactic._aux_Mathlib_Tactic_Widget_Calc___elabRules_Lean_calcTactic_1._boxed took 207ms
type checking took 135ms
elaboration took 219ms
tactic execution of Lean.Parser.Tactic.rewriteSeq took 211ms
tactic execution of Lean.Parser.Tactic.rewriteSeq took 130ms
type checking took 113ms
cumulative profiling times:
	aesop 16.5ms
	attribute application 141ms
	blocked (unaccounted) 4.28s
	compilation (IR) 2.79ms
	compilation (LCNF base) 48.9ms
	compilation (LCNF impure) 14.9ms
	compilation (LCNF mono) 41.6ms
	congr simp thm 185ms
	dsimp 6.65ms
	elaboration 4.74s
	fix level params 56.5ms
	import 2.15s
	initialization 26.6ms
	instantiate metavars 64.7ms
	interpretation 2.92s
	let-to-have transformation 350ms
	linting 164ms
	norm_num 13ms
	parsing 77.7ms
	process pre-definitions 250ms
	share common exprs 186ms
	simp 9.3s
	tactic execution 9.84s
	type checking 4.94s
	typeclass inference 44.1s
real 39.04
user 78.63
sys 1.59

LeanPool/Monlib4/QuantumGraph/Degree.lean

import took 2.11s
typeclass inference of ZeroHomClass took 424ms
type checking took 109ms
typeclass inference of AddMonoidHomClass took 219ms
tactic execution of Lean.Parser.Tactic.rewriteSeq took 115ms
typeclass inference of ZeroHomClass took 361ms
type checking took 170ms
typeclass inference of AddHomClass took 361ms
tactic execution of Lean.Parser.Tactic.rewriteSeq took 137ms
typeclass inference of AddMonoidHomClass took 401ms
tactic execution of Lean.Parser.Tactic.congr took 361ms
simp took 132ms
typeclass inference of AddMonoidHomClass took 407ms
tactic execution of Lean.Parser.Tactic.congr took 364ms
simp took 164ms
type checking took 132ms
typeclass inference of AddMonoidHomClass took 114ms
simp took 407ms
simp took 117ms
type checking took 149ms
typeclass inference of AddMonoidHomClass took 123ms
simp took 451ms
type checking took 101ms
typeclass inference of CompleteSpace took 129ms
tactic execution of Lean.Parser.Tactic.exact took 140ms
interpretation of Lean.Elab.Tactic._aux_Mathlib_Tactic_Widget_Calc___elabRules_Lean_calcTactic_1._boxed took 184ms
interpretation of Lean.Elab.Tactic._aux_Mathlib_Tactic_Widget_Calc___elabRules_Lean_calcTactic_1._boxed took 221ms
tactic execution of Lean.Parser.Tactic.exact took 392ms
cumulative profiling times:
	attribute application 1.22ms
	blocked (unaccounted) 15.3ms
	compilation (IR) 0.644ms
	compilation (LCNF base) 9.02ms
	compilation (LCNF impure) 3.73ms
	compilation (LCNF mono) 9.99ms
	congr simp thm 37ms
	elaboration 913ms
	fix level params 23.3ms
	import 2.11s
	initialization 26.6ms
	instantiate metavars 23.5ms
	interpretation 1.23s
	let-to-have transformation 71ms
	linting 67.9ms
	norm_num 9.72ms
	parsing 34.6ms
	process pre-definitions 64.4ms
	share common exprs 69.2ms
	simp 2.82s
	tactic execution 3.57s
	type checking 1.8s
	typeclass inference 15.8s
real 10.73
user 27.90
sys 1.38

LeanPool/Monlib4/QuantumGraph/Example.lean

import took 2.11s
typeclass inference of IsRightCancelAdd took 258ms
tactic execution of Lean.Parser.Tactic.rewriteSeq took 289ms
tactic execution of Lean.Parser.Tactic.rewriteSeq took 246ms
tactic execution of Lean.Parser.Tactic.rewriteSeq took 102ms
cumulative profiling times:
	attribute application 10.4ms
	blocked (unaccounted) 895ms
	compilation (IR) 4.97ms
	compilation (LCNF base) 233ms
	compilation (LCNF impure) 26.6ms
	compilation (LCNF mono) 71.7ms
	congr simp thm 26.6ms
	elaboration 1.61s
	fix level params 11.9ms
	import 2.11s
	initialization 26.9ms
	instantiate metavars 8.68ms
	interpretation 1.02s
	let-to-have transformation 10.9ms
	linting 84.4ms
	parsing 25.2ms
	process pre-definitions 60.6ms
	share common exprs 33.8ms
	simp 1s
	tactic execution 1.56s
	type checking 1.01s
	typeclass inference 9.27s
real 10.71
user 17.78
sys 1.30

LeanPool/Monlib4/QuantumGraph/Grad.lean

import took 2.13s
typeclass inference of ZeroHomClass took 379ms
typeclass inference of AddHomClass took 326ms
typeclass inference of ZeroHomClass took 285ms
typeclass inference of AddHomClass took 242ms
typeclass inference of AddMonoidHomClass took 225ms
tactic execution of Lean.Parser.Tactic.rewriteSeq took 883ms
simp took 181ms
type checking took 158ms
typeclass inference of AddMonoidHomClass took 202ms
tactic execution of Lean.Parser.Tactic.rewriteSeq took 417ms
typeclass inference of AddMonoidHomClass took 145ms
simp took 194ms
type checking took 132ms
elaboration took 156ms
typeclass inference of AddMonoidHomClass took 176ms
tactic execution of Lean.Parser.Tactic.rewriteSeq took 621ms
simp took 106ms
tactic execution of Lean.Parser.Tactic.rewriteSeq took 102ms
cumulative profiling times:
	attribute application 54.2ms
	blocked (unaccounted) 119ms
	compilation (IR) 1.16ms
	compilation (LCNF base) 61.8ms
	compilation (LCNF impure) 6.67ms
	compilation (LCNF mono) 18.6ms
	congr simp thm 21.6ms
	elaboration 713ms
	fix level params 8.99ms
	import 2.13s
	initialization 27ms
	instantiate metavars 12.4ms
	interpretation 391ms
	let-to-have transformation 4.98ms
	linting 43.8ms
	parsing 10.5ms
	process pre-definitions 45.1ms
	share common exprs 31.7ms
	simp 1.32s
	tactic execution 2.82s
	type checking 789ms
	typeclass inference 7.62s
real 9.72
user 15.49
sys 1.32

LeanPool/Monlib4/QuantumGraph/Iso.lean

import took 2.13s
tactic execution of Lean.Parser.Tactic.change took 225ms
tactic execution of Lean.Parser.Tactic.rewriteSeq took 126ms
tactic execution of Lean.Parser.Tactic.rewriteSeq took 126ms
simp took 163ms
tactic execution of Lean.Parser.Tactic.congr took 2.9s
tactic execution of Lean.Parser.Tactic.change took 143ms
tactic execution of Lean.Parser.Tactic.change took 101ms
tactic execution of Lean.Parser.Tactic.change took 208ms
elaboration took 159ms
tactic execution of Lean.Parser.Tactic.rewriteSeq took 129ms
typeclass inference of FiniteDimensional took 121ms
elaboration took 116ms
tactic execution of Lean.Parser.Tactic.rewriteSeq took 699ms
elaboration took 143ms
tactic execution of Lean.Parser.Tactic.change took 302ms
type checking took 338ms
elaboration took 157ms
tactic execution of Lean.Parser.Tactic.rewriteSeq took 161ms
elaboration took 127ms
cumulative profiling times:
	attribute application 3.1ms
	blocked (unaccounted) 1.76s
	compilation (IR) 4.48ms
	compilation (LCNF base) 204ms
	compilation (LCNF impure) 23.7ms
	compilation (LCNF mono) 68.3ms
	congr simp thm 25.3ms
	elaboration 2.15s
	fix level params 12.5ms
	import 2.13s
	initialization 27.2ms
	instantiate metavars 2.96ms
	interpretation 870ms
	let-to-have transformation 2.37ms
	linting 82.5ms
	parsing 26.5ms
	process pre-definitions 63.6ms
	share common exprs 44.4ms
	simp 1.25s
	tactic execution 6.85s
	type checking 1.15s
	typeclass inference 7.12s
real 11.00
user 21.56
sys 1.31

LeanPool/Monlib4/QuantumGraph/Matrix.lean

import took 2.16s
elaboration took 207ms
simp took 102ms
tactic execution of Lean.Parser.Tactic.rewriteSeq took 149ms
typeclass inference of MulActionHomClass took 111ms
typeclass inference of AddMonoidHomClass took 110ms
typeclass inference of MulActionHomClass took 247ms
typeclass inference of AddMonoidHomClass took 233ms
typeclass inference of MulActionHomClass took 187ms
simp took 461ms
simp took 125ms
simp took 115ms
simp took 159ms
simp took 160ms
simp took 170ms
simp took 164ms
simp took 161ms
simp took 368ms
type checking took 307ms
typeclass inference of Algebra took 103ms
elaboration took 260ms
typeclass inference of FunLike took 119ms
typeclass inference of MulHomClass took 117ms
tactic execution of Lean.Parser.Tactic.rewriteSeq took 508ms
typeclass inference of StarHomClass took 159ms
typeclass inference of StarHomClass took 237ms
tactic execution of Lean.Parser.Tactic.rewriteSeq took 148ms
tactic execution of Lean.Parser.Tactic.congr took 169ms
tactic execution of Lean.Parser.Tactic.simpa took 223ms
type checking took 217ms
type checking took 124ms
type checking took 122ms
type checking took 124ms
typeclass inference of Submodule.HasOrthogonalProjection took 210ms
typeclass inference of Algebra took 145ms
elaboration took 286ms
tactic execution of Lean.Parser.Tactic.rewriteSeq took 146ms
interpretation of Batteries.Tactic._aux_Batteries_Tactic_GeneralizeProofs___elabRules_Batteries_Tactic_generalizeProofsElab_1._boxed took 1.04s
type checking took 186ms
elaboration took 144ms
typeclass inference of InnerProductSpace took 115ms
typeclass inference of CoeFun took 105ms
elaboration took 355ms
typeclass inference of AddMonoidHomClass took 361ms
typeclass inference of CompleteSpace took 111ms
tactic execution of Lean.Parser.Tactic.rewriteSeq took 101ms
simp took 107ms
type checking took 104ms
type checking took 143ms
elaboration took 338ms
typeclass inference of Module.Free took 180ms
typeclass inference of Module.Free took 223ms
elaboration took 247ms
tactic execution of Lean.Parser.Tactic.rewriteSeq took 104ms
typeclass inference of AddMonoidHomClass took 265ms
simp took 185ms
typeclass inference of AddMonoidHomClass took 275ms
tactic execution of Lean.Parser.Tactic.rewriteSeq took 114ms
type checking took 221ms
typeclass inference of MulHomClass took 149ms
typeclass inference of ZeroHomClass took 473ms
type checking took 176ms
elaboration took 241ms
tactic execution of Lean.Parser.Tactic.refine took 152ms
type checking took 102ms
typeclass inference of MulHomClass took 163ms
tactic execution of Lean.Parser.Tactic.rewriteSeq took 158ms
tactic execution of Lean.Parser.Tactic.rewriteSeq took 136ms
tactic execution of Lean.Parser.Tactic.rewriteSeq took 144ms
type checking took 165ms
typeclass inference of Nonempty took 127ms
elaboration took 168ms
tactic execution of Lean.Parser.Tactic.refine took 141ms
tactic execution of Lean.Parser.Tactic.change took 375ms
tactic execution of Lean.Parser.Tactic.change took 118ms
tactic execution of Lean.Parser.Tactic.rewriteSeq took 203ms
tactic execution of Lean.Parser.Tactic.rewriteSeq took 180ms
tactic execution of Lean.Parser.Tactic.congr took 146ms
tactic execution of Lean.Parser.Tactic.change took 122ms
type checking took 160ms
simp took 125ms
typeclass inference of SMul took 154ms
typeclass inference of SMul took 115ms
tactic execution of Lean.Parser.Tactic.rewriteSeq took 211ms
elaboration took 259ms
tactic execution of Lean.Parser.Tactic.refine took 171ms
typeclass inference of QuantumSetDeltaForm took 180ms
tactic execution of Lean.Parser.Tactic.rewriteSeq took 140ms
typeclass inference of QuantumSetDeltaForm took 181ms
typeclass inference of QuantumSetDeltaForm took 175ms
elaboration took 697ms
tactic execution of Lean.Parser.Tactic.refine took 173ms
tactic execution of Lean.Parser.Tactic.rewriteSeq took 109ms
tactic execution of Lean.Parser.Tactic.obtain took 378ms
tactic execution of Lean.Parser.Tactic.refine took 174ms
tactic execution of Lean.Parser.Tactic.simpa took 153ms
tactic execution of Lean.Parser.Tactic.congr took 241ms
tactic execution of Lean.Parser.Tactic.simpa took 142ms
tactic execution of Lean.Parser.Tactic.rewriteSeq took 118ms
tactic execution of Lean.Parser.Tactic.rewriteSeq took 150ms
tactic execution of Lean.Parser.Tactic.refine took 172ms
tactic execution of Lean.Parser.Tactic.simpa took 129ms
tactic execution of Lean.Parser.Tactic.congr took 235ms
tactic execution of Lean.Parser.Tactic.simpa took 135ms
tactic execution of Lean.Parser.Tactic.rewriteSeq took 118ms
tactic execution of Lean.Parser.Tactic.rewriteSeq took 162ms
type checking took 3.84s
elaboration took 100ms
simp took 142ms
simp took 184ms
elaboration took 471ms
elaboration took 471ms
elaboration took 132ms
tactic execution of Lean.Parser.Tactic.rewriteSeq took 246ms
tactic execution of Lean.Parser.Tactic.rewriteSeq took 104ms
interpretation of Lean.Elab.Tactic._aux_Mathlib_Tactic_Widget_Calc___elabRules_Lean_calcTactic_1._boxed took 199ms
simp took 204ms
simp took 317ms
typeclass inference of IsLeftCancelAdd took 380ms
tactic execution of Lean.Parser.Tactic.refine took 558ms
type checking took 5.57s
cumulative profiling times:
	attribute application 105ms
	blocked (unaccounted) 9.73s
	compilation (IR) 2.05ms
	compilation (LCNF base) 40.9ms
	compilation (LCNF impure) 12.1ms
	compilation (LCNF mono) 29.2ms
	congr simp thm 108ms
	elaboration 5.6s
	fix level params 40.9ms
	import 2.16s
	initialization 27ms
	instantiate metavars 65ms
	interpretation 2.72s
	let-to-have transformation 12.3ms
	linting 99.9ms
	norm_num 1.92ms
	parsing 72ms
	process pre-definitions 161ms
	share common exprs 156ms
	simp 7.9s
	tactic execution 12.8s
	type checking 13.1s
	typeclass inference 32.1s
real 40.70
user 76.56
sys 1.61

LeanPool/Monlib4/QuantumGraph/Nontracial.lean

import took 2.21s
tactic execution of Lean.Parser.Tactic.exact took 273ms
type checking took 129ms
typeclass inference of NonUnitalSemiring took 106ms
cumulative profiling times:
	attribute application 4.26ms
	blocked (unaccounted) 627ms
	compilation (IR) 5.85ms
	compilation (LCNF base) 332ms
	compilation (LCNF impure) 30.9ms
	compilation (LCNF mono) 86.2ms
	congr simp thm 20.9ms
	dsimp 30.3ms
	elaboration 1.08s
	fix level params 5.57ms
	import 2.21s
	initialization 27.6ms
	instantiate metavars 2.6ms
	interpretation 887ms
	let-to-have transformation 1.58ms
	linting 54.5ms
	norm_num 9.87ms
	parsing 18ms
	process pre-definitions 55.4ms
	share common exprs 21.1ms
	simp 798ms
	tactic execution 806ms
	type checking 447ms
	typeclass inference 5.32s
real 7.99
user 11.83
sys 1.31

LeanPool/Monlib4/QuantumGraph/OfClassicalGraph.lean

import took 2.19s
simp took 1.29s
simp took 269ms
simp took 311ms
simp took 227ms
elaboration took 184ms
elaboration took 115ms
tactic execution of Lean.Parser.Tactic.rewriteSeq took 156ms
typeclass inference of AddMonoidHomClass took 180ms
typeclass inference of AddMonoidHomClass took 122ms
simp took 133ms
simp took 179ms
cumulative profiling times:
	attribute application 0.474ms
	compilation (IR) 0.0766ms
	compilation (LCNF base) 0.765ms
	compilation (LCNF impure) 0.28ms
	compilation (LCNF mono) 0.829ms
	congr simp thm 12.4ms
	elaboration 504ms
	fix level params 3.79ms
	import 2.19s
	initialization 26.9ms
	instantiate metavars 2.43ms
	interpretation 291ms
	let-to-have transformation 162ms
	linting 5.22ms
	parsing 6.87ms
	process pre-definitions 9.09ms
	share common exprs 10.9ms
	simp 2.93s
	tactic execution 441ms
	type checking 522ms
	typeclass inference 2.9s
real 6.24
user 9.41
sys 1.28

LeanPool/Monlib4/QuantumGraph/PiMat.lean

import took 2.2s
typeclass inference of ZeroHomClass took 176ms
typeclass inference of ZeroHomClass took 164ms
typeclass inference of AddHomClass took 319ms
typeclass inference of AddHomClass took 305ms
elaboration took 143ms
type checking took 265ms
simp took 247ms
simp took 102ms
type checking took 139ms
simp took 100ms
typeclass inference of AddMonoidHomClass took 108ms
simp took 174ms
elaboration took 188ms
type checking took 215ms
typeclass inference of Star took 101ms
typeclass inference of CoeFun took 241ms
elaboration took 188ms
typeclass inference of CoeFun took 238ms
typeclass inference of DistribMulAction took 131ms
typeclass inference of MulEquivClass took 287ms
typeclass inference of MulEquivClass took 150ms
typeclass inference of IsLeftCancelMulZero took 506ms
typeclass inference of IsLeftCancelMulZero took 847ms
tactic execution of Lean.Parser.Tactic.simpa took 285ms
tactic execution of Lean.Parser.Tactic.exact took 211ms
type checking took 595ms
type checking took 161ms
typeclass inference of CoeFun took 251ms
elaboration took 350ms
type checking took 288ms
typeclass inference of CoeFun took 250ms
elaboration took 322ms
type checking took 253ms
typeclass inference of Mul took 115ms
simp took 132ms
elaboration took 302ms
tactic execution of Lean.Parser.Tactic.rewriteSeq took 161ms
simp took 142ms
typeclass inference of Module.Free took 209ms
typeclass inference of AddCommGroup took 249ms
typeclass inference of Module.Free took 352ms
typeclass inference of Module.Finite took 271ms
tactic execution of Lean.Parser.Tactic.rewriteSeq took 127ms
simp took 132ms
type checking took 242ms
typeclass inference of CoalgebraStruct took 118ms
typeclass inference of CoalgebraStruct took 153ms
elaboration took 244ms
typeclass inference of Module.Finite took 141ms
simp took 166ms
tactic execution of Lean.Parser.Tactic.rewriteSeq took 107ms
type checking took 190ms
type checking took 223ms
typeclass inference of CoalgebraStruct took 141ms
type checking took 198ms
elaboration took 123ms
tactic execution of Lean.Parser.Tactic.rewriteSeq took 175ms
tactic execution of Lean.Parser.Tactic.eqRefl took 185ms
type checking took 173ms
elaboration took 155ms
typeclass inference of CoeFun took 295ms
typeclass inference of CoeFun took 362ms
tactic execution of Lean.Parser.Tactic.rewriteSeq took 101ms
typeclass inference of CoeT took 120ms
tactic execution of Lean.Parser.Tactic.rewriteSeq took 170ms
typeclass inference of OneHomClass took 187ms
typeclass inference of OneHomClass took 170ms
typeclass inference of OneHomClass took 386ms
interpretation of Lean.Elab.Tactic._aux_Mathlib_Tactic_Widget_Calc___elabRules_Lean_calcTactic_1._boxed took 461ms
type checking took 1.08s
elaboration took 284ms
elaboration took 169ms
typeclass inference of CoalgebraStruct took 135ms
tactic execution of Lean.Parser.Tactic.refine took 322ms
type checking took 111ms
typeclass inference of CoeFun took 257ms
elaboration took 419ms
tactic execution of Lean.Parser.Tactic.rewriteSeq took 349ms
tactic execution of Lean.Parser.Tactic.rewriteSeq took 312ms
typeclass inference of DistribMulAction took 214ms
typeclass inference of MulHomClass took 453ms
typeclass inference of MulHomClass took 143ms
typeclass inference of MulHomClass took 258ms
typeclass inference of SMul took 106ms
typeclass inference of MulHomClass took 638ms
typeclass inference took 136ms
typeclass inference of StarHomClass took 593ms
typeclass inference of StarHomClass took 172ms
typeclass inference of StarHomClass took 536ms
typeclass inference of StarHomClass took 265ms
simp took 345ms
tactic execution of Lean.Parser.Tactic.simp took 396ms
type checking took 561ms
typeclass inference of CoalgebraStruct took 134ms
tactic execution of Lean.Parser.Tactic.exact took 123ms
type checking took 344ms
type checking took 350ms
typeclass inference of CoalgebraStruct took 132ms
typeclass inference of NormedAddCommGroup took 111ms
typeclass inference of Submodule.HasOrthogonalProjection took 411ms
typeclass inference of CoeFun took 386ms
elaboration took 419ms
tactic execution of Lean.Parser.Tactic.exact took 237ms
type checking took 583ms
typeclass inference of CoalgebraStruct took 129ms
typeclass inference of CoeT took 129ms
typeclass inference of AddCommMonoid took 108ms
typeclass inference of Module took 106ms
typeclass inference of CoeT took 116ms
typeclass inference of InnerProductSpace took 131ms
typeclass inference of FiniteDimensional took 103ms
elaboration took 261ms
type checking took 136ms
type checking took 201ms
typeclass inference of SeminormedAddCommGroup took 784ms
typeclass inference of SeminormedAddCommGroup took 771ms
tactic execution of Lean.Parser.Tactic.obtain took 163ms
typeclass inference of SeminormedAddCommGroup took 798ms
typeclass inference of SeminormedAddCommGroup took 772ms
typeclass inference of AddMonoidHomClass took 996ms
typeclass inference of CoeT took 136ms
typeclass inference of CoeT took 240ms
elaboration took 162ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Convert___elabRules_Mathlib_Tactic_convert_1._boxed took 192ms
type checking took 227ms
elaboration took 506ms
typeclass inference of Trans took 124ms
tactic execution of Lean.Parser.Tactic.rewriteSeq took 269ms
interpretation of Lean.Elab.Tactic._aux_Mathlib_Tactic_Widget_Calc___elabRules_Lean_calcTactic_1._boxed took 830ms
type checking took 229ms
typeclass inference of SeminormedAddCommGroup took 796ms
typeclass inference of SeminormedAddCommGroup took 712ms
let-to-have transformation took 156ms
elaboration took 240ms
typeclass inference of SeminormedAddCommGroup took 817ms
typeclass inference of SeminormedAddCommGroup took 809ms
tactic execution of Lean.Parser.Tactic.refine took 140ms
typeclass inference of SeminormedAddCommGroup took 830ms
typeclass inference of SeminormedAddCommGroup took 770ms
typeclass inference of AddMonoidHomClass took 811ms
typeclass inference of SeminormedAddCommGroup took 533ms
typeclass inference of SeminormedAddCommGroup took 525ms
typeclass inference of SeminormedAddCommGroup took 786ms
typeclass inference of SeminormedAddCommGroup took 804ms
simp took 198ms
tactic execution of Lean.Parser.Tactic.eqRefl took 167ms
type checking took 163ms
elaboration took 321ms
tactic execution of Lean.Parser.Tactic.rewriteSeq took 162ms
typeclass inference of ZeroHomClass took 298ms
typeclass inference of Semiring took 102ms
typeclass inference of NonUnitalSemiring took 167ms
typeclass inference of ZeroHomClass took 597ms
elaboration took 326ms
tactic execution of Lean.Parser.Tactic.rewriteSeq took 168ms
typeclass inference of ZeroHomClass took 328ms
typeclass inference of NonUnitalSemiring took 160ms
typeclass inference of ZeroHomClass took 515ms
typeclass inference of AddCommMonoid took 166ms
elaboration took 335ms
typeclass inference of AddCommMonoid took 167ms
typeclass inference of AddCommMonoid took 108ms
elaboration took 255ms
typeclass inference of AddCommMonoid took 160ms
type checking took 102ms
typeclass inference of CoeFun took 144ms
typeclass inference of CoeT took 193ms
typeclass inference of AddCommMonoid took 145ms
typeclass inference of CoeT took 102ms
elaboration took 272ms
typeclass inference of CoeFun took 142ms
typeclass inference of CoeT took 111ms
typeclass inference of Mul took 195ms
typeclass inference of SMul took 109ms
typeclass inference of Star took 180ms
typeclass inference of CoeFun took 163ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_ApplyFun___elabRules_Mathlib_Tactic_applyFun_1._boxed took 164ms
simp took 373ms
typeclass inference of AddCommMonoid took 152ms
typeclass inference of CompleteSpace took 320ms
tactic execution of Lean.Parser.Tactic.rewriteSeq took 1.04s
typeclass inference of SMul took 109ms
typeclass inference of AddMonoidHomClass took 653ms
typeclass inference of AddMonoidHomClass took 331ms
typeclass inference of AddMonoidHomClass took 350ms
typeclass inference of DistribMulAction took 210ms
typeclass inference of AddMonoidHomClass took 536ms
simp took 3.14s
typeclass inference of AddCommMonoid took 154ms
typeclass inference of Semiring took 145ms
typeclass inference of NonUnitalSemiring took 148ms
typeclass inference of AddMonoidHomClass took 559ms
simp took 1.59s
simp took 284ms
simp took 258ms
simp took 256ms
typeclass inference of AddCommMonoid took 168ms
typeclass inference of AddCommMonoid took 154ms
tactic execution of Lean.Parser.Tactic.rcases took 214ms
typeclass inference of AddCommMonoid took 150ms
typeclass inference of AddCommMonoid took 151ms
simp took 106ms
typeclass inference of AddMonoidHomClass took 112ms
typeclass inference of AddCommMonoid took 165ms
typeclass inference of AddMonoidHomClass took 252ms
simp took 103ms
simp took 189ms
tactic execution of Lean.Parser.Tactic.congr took 3.84s
typeclass inference of AddCommMonoid took 165ms
tactic execution of Lean.Parser.Tactic.rewriteSeq took 191ms
simp took 613ms
type checking took 1.97s
typeclass inference of CoalgebraStruct took 139ms
typeclass inference of CoalgebraStruct took 126ms
typeclass inference of CoalgebraStruct took 123ms
elaboration took 217ms
typeclass inference of CoalgebraStruct took 143ms
tactic execution of Lean.Parser.Tactic.refine took 174ms
typeclass inference of CoalgebraStruct took 129ms
typeclass inference of QuantumSetDeltaForm took 179ms
typeclass inference of CoalgebraStruct took 123ms
tactic execution of Lean.Parser.Tactic.exact took 173ms
type checking took 107ms
typeclass inference of CoalgebraStruct took 141ms
typeclass inference of CoalgebraStruct took 133ms
typeclass inference of CoalgebraStruct took 128ms
elaboration took 416ms
LeanPool/Monlib4/QuantumGraph/PiMat.lean:1107:59: error: unsolved goals
ι : Type u_1
p : ι → Type u_2
inst✝⁵ : Fintype ι
inst✝⁴ : DecidableEq ι
inst✝³ : (i : ι) → Fintype (p i)
inst✝² : (i : ι) → DecidableEq (p i)
φ : (i : ι) → Module.Dual ℂ (Matrix (p i) (p i) ℂ)
hφ : ∀ (i : ι), (φ i).IsFaithfulPosMap
d : ℂ
inst✝¹ : Nonempty ι
hφ₂ : Fact (∀ (i : ι), (φ i).matrix⁻¹.trace = d)
inst✝ : ∀ (i : ι), Nontrivial (p i)
this✝⁵ : starAlgebra (PiMat ℂ ι p) := PiMat.isStarAlgebra
this✝⁴ : QuantumSet (PiMat ℂ ι p) := Module.Dual.pi.IsFaithfulPosMap.quantumSet
this✝³ : NormedAddCommGroup (PiMat ℂ ι p) := Module.Dual.PiNormedAddCommGroup
this✝² : TopologicalSpace (PiMat ℂ ι p) := PseudoMetricSpace.toUniformSpace.toTopologicalSpace
this✝¹ : SeminormedAddCommGroup (PiMat ℂ ι p) := NormedAddCommGroup.toSeminormedAddCommGroup
this✝ : InnerProductSpace ℂ (PiMat ℂ ι p) := Module.Dual.pi.InnerProductSpace
this : QuantumSetDeltaForm (PiMat ℂ ι p) := PiMat.quantumSetDeltaForm
⊢ (QuantumSetDeltaForm.delta (PiMat ℂ ι p))⁻¹ *
      ∑ x, ∑ x_1, ∑ x_2, ⋯.rpow (-(1 / 2)) x_2 x_1 * ⋯.rpow (-(1 / 2)) x_1 x_2 =
    (QuantumSetDeltaForm.delta (PiMat ℂ ι p))⁻¹ *
      ∑ x, ∑ x_1, ∑ x_2, ⋯.rpow (-(1 / 2)) x_2 x_1 * ⋯.rpow (-(1 / 2)) x_1 x_2
LeanPool/Monlib4/QuantumGraph/PiMat.lean:1111:59: error: unsolved goals
ι : Type u_1
p : ι → Type u_2
inst✝⁵ : Fintype ι
inst✝⁴ : DecidableEq ι
inst✝³ : (i : ι) → Fintype (p i)
inst✝² : (i : ι) → DecidableEq (p i)
φ : (i : ι) → Module.Dual ℂ (Matrix (p i) (p i) ℂ)
hφ : ∀ (i : ι), (φ i).IsFaithfulPosMap
d : ℂ
inst✝¹ : Nonempty ι
hφ₂ : Fact (∀ (i : ι), (φ i).matrix⁻¹.trace = d)
inst✝ : ∀ (i : ι), Nontrivial (p i)
this✝⁵ : starAlgebra (PiMat ℂ ι p) := PiMat.isStarAlgebra
this✝⁴ : QuantumSet (PiMat ℂ ι p) := Module.Dual.pi.IsFaithfulPosMap.quantumSet
this✝³ : NormedAddCommGroup (PiMat ℂ ι p) := Module.Dual.PiNormedAddCommGroup
this✝² : TopologicalSpace (PiMat ℂ ι p) := PseudoMetricSpace.toUniformSpace.toTopologicalSpace
this✝¹ : SeminormedAddCommGroup (PiMat ℂ ι p) := NormedAddCommGroup.toSeminormedAddCommGroup
this✝ : InnerProductSpace ℂ (PiMat ℂ ι p) := Module.Dual.pi.InnerProductSpace
this : QuantumSetDeltaForm (PiMat ℂ ι p) := PiMat.quantumSetDeltaForm
⊢ (∑ x, ∑ x_1, ∑ x_2, ⋯.rpow (-(1 / 2)) x_1 x_2 * ⋯.rpow (-(1 / 2)) x_2 x_1) *
      (QuantumSetDeltaForm.delta (PiMat ℂ ι p))⁻¹ =
    (∑ x, ∑ x_1, ∑ x_2, ⋯.rpow (-(1 / 2)) x_1 x_2 * ⋯.rpow (-(1 / 2)) x_2 x_1) *
      (QuantumSetDeltaForm.delta (PiMat ℂ ι p))⁻¹
LeanPool/Monlib4/QuantumGraph/PiMat.lean:1114:58: error: unsolved goals
ι : Type u_1
p : ι → Type u_2
inst✝⁵ : Fintype ι
inst✝⁴ : DecidableEq ι
inst✝³ : (i : ι) → Fintype (p i)
inst✝² : (i : ι) → DecidableEq (p i)
φ : (i : ι) → Module.Dual ℂ (Matrix (p i) (p i) ℂ)
hφ : ∀ (i : ι), (φ i).IsFaithfulPosMap
d : ℂ
inst✝¹ : Nonempty ι
hφ₂ : Fact (∀ (i : ι), (φ i).matrix⁻¹.trace = d)
inst✝ : ∀ (i : ι), Nontrivial (p i)
this✝⁵ : starAlgebra (PiMat ℂ ι p) := PiMat.isStarAlgebra
this✝⁴ : QuantumSet (PiMat ℂ ι p) := Module.Dual.pi.IsFaithfulPosMap.quantumSet
this✝³ : NormedAddCommGroup (PiMat ℂ ι p) := Module.Dual.PiNormedAddCommGroup
this✝² : TopologicalSpace (PiMat ℂ ι p) := PseudoMetricSpace.toUniformSpace.toTopologicalSpace
this✝¹ : SeminormedAddCommGroup (PiMat ℂ ι p) := NormedAddCommGroup.toSeminormedAddCommGroup
this✝ : InnerProductSpace ℂ (PiMat ℂ ι p) := Module.Dual.pi.InnerProductSpace
this : QuantumSetDeltaForm (PiMat ℂ ι p) := PiMat.quantumSetDeltaForm
⊢ (QuantumSetDeltaForm.delta (PiMat ℂ ι p))⁻¹ * ∑ x, ∑ x_1, (⋯.rpow (-(1 / 2)) * ⋯.rpow (-(1 / 2))) x_1 x_1 =
    (QuantumSetDeltaForm.delta (PiMat ℂ ι p))⁻¹ * ∑ x, ∑ x_1, (⋯.rpow (-(1 / 2)) * ⋯.rpow (-(1 / 2))) x_1 x_1
LeanPool/Monlib4/QuantumGraph/PiMat.lean:1123:6: error: (deterministic) timeout at `whnf`, maximum number of heartbeats (200000) has been reached

Note: Use `set_option maxHeartbeats <num>` to set the limit.

Hint: Additional diagnostic information may be available using the `set_option diagnostics true` command.
LeanPool/Monlib4/QuantumGraph/PiMat.lean:1125:6: error: (deterministic) timeout at `«tactic execution»`, maximum number of heartbeats (200000) has been reached

Note: Use `set_option maxHeartbeats <num>` to set the limit.

Hint: Additional diagnostic information may be available using the `set_option diagnostics true` command.
LeanPool/Monlib4/QuantumGraph/PiMat.lean:1105:7: error: (deterministic) timeout at `whnf`, maximum number of heartbeats (200000) has been reached

Note: Use `set_option maxHeartbeats <num>` to set the limit.

Hint: Additional diagnostic information may be available using the `set_option diagnostics true` command.
typeclass inference of CoalgebraStruct took 138ms
tactic execution of Lean.Parser.Tactic.refine took 179ms
typeclass inference of CoalgebraStruct took 123ms
typeclass inference of QuantumSetDeltaForm took 175ms
tactic execution of Lean.Parser.Tactic.rewriteSeq took 216ms
typeclass inference of MulActionHomClass took 531ms
typeclass inference of MulActionHomClass took 710ms
typeclass inference of MulActionHomClass took 385ms
tactic execution of Lean.Parser.Tactic.rewriteSeq took 124ms
typeclass inference of AddMonoidHomClass took 384ms
typeclass inference of AddMonoidHomClass took 197ms
typeclass inference of AddMonoidHomClass took 160ms
simp took 201ms
typeclass inference of CoalgebraStruct took 229ms
typeclass inference took 204ms
typeclass inference of QuantumSetDeltaForm took 198ms
typeclass inference of CoalgebraStruct took 217ms
simp took 244ms
typeclass inference of CoalgebraStruct took 216ms
typeclass inference took 107ms
typeclass inference of CoalgebraStruct took 231ms
typeclass inference took 105ms
typeclass inference of CoalgebraStruct took 225ms
typeclass inference took 207ms
tactic execution of Lean.Parser.Tactic.eqRefl took 346ms
tactic execution of Lean.Parser.Tactic.applyRfl took 348ms
typeclass inference of CoalgebraStruct took 212ms
interpretation of Lean.Elab.Tactic._aux_Mathlib_Tactic_Widget_Calc___elabRules_Lean_calcTactic_1._boxed took 119ms
typeclass inference took 194ms
typeclass inference of QuantumSetDeltaForm took 195ms
typeclass inference of CoalgebraStruct took 212ms
simp took 245ms
typeclass inference of CoalgebraStruct took 222ms
typeclass inference took 103ms
typeclass inference of CoalgebraStruct took 225ms
typeclass inference took 103ms
typeclass inference of CoalgebraStruct took 219ms
typeclass inference took 203ms
tactic execution of Lean.Parser.Tactic.eqRefl took 335ms
tactic execution of Lean.Parser.Tactic.applyRfl took 180ms
tactic execution of Lean.calcTactic took 116ms
type checking took 118ms
tactic execution of Lean.Parser.Tactic.exact took 129ms
elaboration took 109ms
elaboration took 101ms
type checking took 108ms
typeclass inference of CoalgebraStruct took 143ms
typeclass inference of CoalgebraStruct took 120ms
elaboration took 214ms
typeclass inference of CoalgebraStruct took 137ms
tactic execution of Lean.Parser.Tactic.rewriteSeq took 437ms
tactic execution of Lean.Parser.Tactic.change took 109ms
type checking took 144ms
elaboration took 115ms
elaboration took 470ms
elaboration took 135ms
tactic execution of Lean.Parser.Tactic.rewriteSeq took 425ms
elaboration took 122ms
typeclass inference of AddMonoidHomClass took 266ms
elaboration took 155ms
simp took 248ms
simp took 164ms
simp took 222ms
simp took 210ms
typeclass inference of CoalgebraStruct took 140ms
typeclass inference of CoalgebraStruct took 122ms
elaboration took 247ms
typeclass inference of CompleteSpace took 311ms
typeclass inference of CompleteSpace took 288ms
simp took 797ms
simp took 121ms
type checking took 590ms
interpretation of Lean.Elab.Tactic._aux_Mathlib_Tactic_Widget_Calc___elabRules_Lean_calcTactic_1._boxed took 257ms
typeclass inference of CoalgebraStruct took 104ms
type checking took 225ms
typeclass inference of CoalgebraStruct took 139ms
typeclass inference of CoeT took 110ms
typeclass inference of CoeFun took 211ms
typeclass inference of Fintype took 108ms
typeclass inference of AddCommMonoid took 202ms
typeclass inference of CoeT took 166ms
typeclass inference of CoeT took 288ms
let-to-have transformation took 107ms
elaboration took 367ms
tactic execution of Lean.Parser.Tactic.rewriteSeq took 135ms
simp took 491ms
simp took 2.25s
tactic execution of Lean.Parser.Tactic.congr took 651ms
tactic execution of Lean.Parser.Tactic.rewriteSeq took 132ms
tactic execution of Lean.Parser.Tactic.rewriteSeq took 180ms
let-to-have transformation took 103ms
type checking took 617ms
typeclass inference of CoalgebraStruct took 134ms
elaboration took 372ms
typeclass inference of CompleteSpace took 351ms
typeclass inference of CompleteSpace took 409ms
tactic execution of Lean.Parser.Tactic.rewriteSeq took 311ms
typeclass inference of CompleteSpace took 290ms
tactic execution of Lean.Parser.Tactic.rewriteSeq took 285ms
tactic execution of Lean.Parser.Tactic.rewriteSeq took 543ms
typeclass inference of SMul took 105ms
typeclass inference of AddMonoidHomClass took 631ms
typeclass inference of AddMonoidHomClass took 303ms
typeclass inference of AddMonoidHomClass took 175ms
typeclass inference of DistribMulAction took 104ms
typeclass inference of AddMonoidHomClass took 336ms
typeclass inference of AddCommMonoid took 146ms
typeclass inference of Semiring took 142ms
typeclass inference of NonUnitalSemiring took 148ms
typeclass inference of AddMonoidHomClass took 548ms
simp took 5.38s
simp took 233ms
simp took 298ms
simp took 216ms
simp took 842ms
typeclass inference of EquivLike took 104ms
typeclass inference of ZeroHomClass took 207ms
simp took 1.34s
tactic execution of Lean.Parser.Tactic.rewriteSeq took 224ms
simp took 334ms
simp took 298ms
simp took 116ms
simp took 158ms
simp took 224ms
tactic execution of Lean.Parser.Tactic.rcases took 277ms
elaboration took 108ms
type checking took 1.48s
LeanPool/Monlib4/QuantumGraph/PiMat.lean:1726:2: error: failed to synthesize
  ZeroHomClass (EuclideanSpace ℂ n ⊗[ℂ] EuclideanSpace ℂ m ≃ₗ[ℂ] n × m →₀ ℂ) ?m.37 ?m.38
(deterministic) timeout at `typeclass`, maximum number of heartbeats (20000) has been reached

Note: Use `set_option synthInstance.maxHeartbeats <num>` to set the limit.

Hint: Additional diagnostic information may be available using the `set_option diagnostics true` command.

Hint: Additional diagnostic information may be available using the `set_option diagnostics true` command.
typeclass inference of SeminormedAddCommGroup took 138ms
typeclass inference of SMul took 180ms
typeclass inference of NonUnitalNonAssocSemiring took 440ms
typeclass inference of ZeroHomClass took 582ms
typeclass inference of CoalgebraStruct took 140ms
elaboration took 221ms
typeclass inference of CompleteSpace took 327ms
typeclass inference of CompleteSpace took 434ms
tactic execution of Lean.Parser.Tactic.rewriteSeq took 378ms
tactic execution of Lean.Parser.Tactic.obtain took 434ms
typeclass inference of AddMonoidHomClass took 586ms
typeclass inference of AddMonoidHomClass took 301ms
typeclass inference of AddMonoidHomClass took 166ms
typeclass inference of DistribMulAction took 104ms
typeclass inference of AddMonoidHomClass took 324ms
typeclass inference of AddCommMonoid took 151ms
typeclass inference of Semiring took 136ms
typeclass inference of NonUnitalSemiring took 144ms
typeclass inference of AddMonoidHomClass took 536ms
simp took 612ms
typeclass inference of AddCommMonoid took 140ms
typeclass inference of Semiring took 129ms
typeclass inference of NonUnitalSemiring took 136ms
typeclass inference of AddMonoidHomClass took 497ms
typeclass inference of AddCommMonoid took 143ms
typeclass inference of FunLike took 110ms
typeclass inference of DistribMulAction took 102ms
typeclass inference of AddMonoidHomClass took 305ms
typeclass inference of Star took 100ms
tactic execution of Lean.Parser.Tactic.rewriteSeq took 526ms
tactic execution of Lean.Parser.Tactic.rewriteSeq took 110ms
typeclass inference of AddMonoidHomClass took 170ms
typeclass inference of ZeroHomClass took 172ms
typeclass inference of ZeroHomClass took 118ms
simp took 474ms
type checking took 547ms
typeclass inference of CoalgebraStruct took 136ms
elaboration took 228ms
typeclass inference of CompleteSpace took 311ms
typeclass inference of CompleteSpace took 482ms
typeclass inference of CompleteSpace took 247ms
tactic execution of Lean.Parser.Tactic.rewriteSeq took 476ms
tactic execution of Lean.Parser.Tactic.obtain took 469ms
typeclass inference of SMul took 109ms
typeclass inference of AddMonoidHomClass took 616ms
typeclass inference of AddMonoidHomClass took 336ms
typeclass inference of AddMonoidHomClass took 175ms
typeclass inference of DistribMulAction took 124ms
typeclass inference of AddMonoidHomClass took 367ms
typeclass inference of AddCommMonoid took 155ms
typeclass inference of Semiring took 147ms
typeclass inference of NonUnitalSemiring took 152ms
typeclass inference of AddMonoidHomClass took 574ms
simp took 706ms
typeclass inference of AddCommMonoid took 148ms
typeclass inference of Semiring took 136ms
typeclass inference of NonUnitalSemiring took 141ms
typeclass inference of AddMonoidHomClass took 530ms
typeclass inference of Semiring took 156ms
typeclass inference of Algebra took 167ms
typeclass inference of Semiring took 152ms
typeclass inference of OneHomClass took 185ms
typeclass inference of FunLike took 111ms
typeclass inference of DistribMulAction took 105ms
typeclass inference of AddMonoidHomClass took 323ms
typeclass inference of EquivLike took 115ms
typeclass inference of OneHomClass took 301ms
tactic execution of Lean.Parser.Tactic.rewriteSeq took 720ms
tactic execution of Lean.Parser.Tactic.rewriteSeq took 126ms
typeclass inference of AddMonoidHomClass took 175ms
simp took 468ms
type checking took 493ms
elaboration took 126ms
tactic execution of Lean.Parser.Tactic.obtain took 126ms
typeclass inference of AddMonoidHomClass took 313ms
typeclass inference of AddMonoidHomClass took 164ms
typeclass inference of AddMonoidHomClass took 149ms
simp took 111ms
type checking took 130ms
elaboration took 244ms
typeclass inference of AddMonoidHomClass took 158ms
simp took 109ms
type checking took 101ms
typeclass inference of AddMonoidHomClass took 159ms
typeclass inference of AddMonoidHomClass took 110ms
elaboration took 1.75s
tactic execution of Lean.Parser.Tactic.rewriteSeq took 114ms
tactic execution of Lean.Parser.Tactic.rewriteSeq took 256ms
tactic execution of Lean.Parser.Tactic.rewriteSeq took 289ms
typeclass inference of CoalgebraStruct took 134ms
typeclass inference of CoeT took 110ms
typeclass inference of CoeT took 113ms
elaboration took 264ms
simp took 114ms
simp took 353ms
tactic execution of Lean.Parser.Tactic.rewriteSeq took 168ms
tactic execution of Lean.Parser.Tactic.rewriteSeq took 163ms
typeclass inference of StarHomClass took 588ms
typeclass inference of StarHomClass took 257ms
type checking took 459ms
typeclass inference of CoalgebraStruct took 129ms
elaboration took 265ms
typeclass inference of CoalgebraStruct took 130ms
elaboration took 262ms
type checking took 129ms
cumulative profiling times:
	aesop 53.1ms
	attribute application 154ms
	blocked (unaccounted) 57.3ms
	compilation (IR) 2.57ms
	compilation (LCNF base) 52ms
	compilation (LCNF impure) 14.3ms
	compilation (LCNF mono) 37.8ms
	congr simp thm 247ms
	dsimp 134ms
	elaboration 15.8s
	fix level params 105ms
	import 2.2s
	initialization 27.6ms
	instantiate metavars 161ms
	interpretation 5.15s
	let-to-have transformation 509ms
	linting 178ms
	norm_num 2.24ms
	parsing 164ms
	process pre-definitions 474ms
	share common exprs 382ms
	simp 32.2s
	tactic execution 26.7s
	type checking 17.7s
	typeclass inference 147s
real 83.99
user 248.43
sys 2.29
error: profile command exited with status 1

LeanPool/Monlib4/QuantumGraph/PiMatFinTwo.lean

import took 2.14s
typeclass inference of CoeFun took 303ms
simp took 336ms
type checking took 227ms
typeclass inference of CoeT took 112ms
typeclass inference of AddCommMonoid took 102ms
elaboration took 421ms
tactic execution of Lean.Parser.Tactic.rewriteSeq took 168ms
simp took 187ms
tactic execution of Lean.Parser.Tactic.rewriteSeq took 124ms
type checking took 378ms
elaboration took 152ms
elaboration took 158ms
elaboration took 148ms
elaboration took 198ms
type checking took 123ms
elaboration took 251ms
tactic execution of Lean.Parser.Tactic.rewriteSeq took 108ms
simp took 129ms
type checking took 137ms
type checking took 7.31s
elaboration took 372ms
typeclass inference of Module.Finite took 158ms
typeclass inference of Module.Finite took 151ms
typeclass inference of Module.Finite took 150ms
typeclass inference of Module.Finite took 152ms
simp took 341ms
tactic execution of Lean.Parser.Tactic.rcases took 126ms
tactic execution of Lean.Parser.Tactic.obtain took 115ms
tactic execution of Lean.Parser.Tactic.rewriteSeq took 132ms
tactic execution of Lean.Parser.Tactic.obtain took 132ms
tactic execution of Lean.Parser.Tactic.rewriteSeq took 173ms
tactic execution of Lean.Parser.Tactic.rewriteSeq took 162ms
type checking took 278ms
elaboration took 547ms
typeclass inference of Module.Finite took 240ms
simp took 170ms
type checking took 4.39s
elaboration took 637ms
tactic execution of Lean.Parser.Tactic.obtain took 219ms
typeclass inference of CoeT took 165ms
typeclass inference of AddCommMonoid took 148ms
typeclass inference of Module took 152ms
tactic execution of Lean.Parser.Tactic.refine took 127ms
tactic execution of Lean.Parser.Tactic.refine took 138ms
typeclass inference of Module.Finite took 234ms
simp took 170ms
tactic execution of Lean.Parser.Tactic.refine took 123ms
tactic execution of Lean.Parser.Tactic.refine took 114ms
tactic execution of Lean.Parser.Tactic.rewriteSeq took 130ms
tactic execution of Lean.Parser.Tactic.refine took 144ms
tactic execution of Lean.Parser.Tactic.refine took 138ms
type checking took 117ms
type checking took 4.26s
elaboration took 424ms
tactic execution of Lean.Parser.Tactic.obtain took 368ms
tactic execution of Lean.Parser.Tactic.obtain took 249ms
tactic execution of Lean.Parser.Tactic.rcases took 121ms
type checking took 230ms
elaboration took 131ms
tactic execution of Lean.Parser.Tactic.rewriteSeq took 168ms
simp took 125ms
type checking took 3.28s
elaboration took 435ms
type checking took 120ms
elaboration took 206ms
elaboration took 105ms
typeclass inference of FiniteDimensional took 140ms
simp took 175ms
tactic execution of Lean.Parser.Tactic.rewriteSeq took 217ms
typeclass inference of FiniteDimensional took 133ms
typeclass inference of FiniteDimensional took 192ms
tactic execution of Lean.Parser.Tactic.exact took 327ms
interpretation of Lean.Elab.Tactic._aux_Mathlib_Tactic_Widget_Calc___elabRules_Lean_calcTactic_1._boxed took 218ms
type checking took 3.43s
elaboration took 231ms
typeclass inference of FiniteDimensional took 181ms
simp took 177ms
tactic execution of Lean.Parser.Tactic.exact took 162ms
typeclass inference of FiniteDimensional took 139ms
typeclass inference of FiniteDimensional took 183ms
tactic execution of Lean.Parser.Tactic.exact took 319ms
tactic execution of Lean.Parser.Tactic.rewriteSeq took 139ms
tactic execution of Lean.Parser.Tactic.rewriteSeq took 109ms
interpretation of Lean.Elab.Tactic._aux_Mathlib_Tactic_Widget_Calc___elabRules_Lean_calcTactic_1._boxed took 242ms
type checking took 3.58s
elaboration took 250ms
tactic execution of Lean.Parser.Tactic.rewriteSeq took 409ms
tactic execution of Lean.Parser.Tactic.rewriteSeq took 158ms
tactic execution of Lean.Parser.Tactic.rewriteSeq took 227ms
tactic execution of Lean.Parser.Tactic.rewriteSeq took 249ms
tactic execution of Lean.Parser.Tactic.rewriteSeq took 203ms
tactic execution of Lean.Parser.Tactic.rewriteSeq took 137ms
type checking took 3.45s
elaboration took 297ms
tactic execution of Lean.Parser.Tactic.rewriteSeq took 307ms
simp took 134ms
tactic execution of Lean.Parser.Tactic.rewriteSeq took 395ms
simp took 165ms
simp took 111ms
type checking took 3.52s
elaboration took 275ms
type checking took 118ms
elaboration took 115ms
typeclass inference of FiniteDimensional took 102ms
typeclass inference of FiniteDimensional took 144ms
typeclass inference of ZeroHomClass took 191ms
simp took 117ms
tactic execution of Lean.Parser.Tactic.rewriteSeq took 406ms
typeclass inference of FiniteDimensional took 135ms
typeclass inference of FiniteDimensional took 124ms
tactic execution of Lean.Parser.Tactic.exact took 221ms
type checking took 3.52s
elaboration took 288ms
simp took 227ms
typeclass inference of IsLeftCancelAdd took 609ms
simp took 161ms
tactic execution of Lean.Parser.Tactic.rcases took 183ms
simp took 239ms
type checking took 4.17s
elaboration took 147ms
tactic execution of Lean.Parser.Tactic.exact took 401ms
elaboration took 144ms
tactic execution of Lean.Parser.Tactic.exact took 403ms
elaboration took 199ms
tactic execution of Lean.Parser.Tactic.rewriteSeq took 307ms
type checking took 3.28s
cumulative profiling times:
	attribute application 33.9ms
	blocked (unaccounted) 87.5ms
	compilation (IR) 3.27ms
	compilation (LCNF base) 75ms
	compilation (LCNF impure) 17.5ms
	compilation (LCNF mono) 44ms
	congr simp thm 86.4ms
	elaboration 8.09s
	fix level params 38ms
	import 2.14s
	initialization 27.1ms
	instantiate metavars 50.3ms
	interpretation 2.51s
	let-to-have transformation 4.91ms
	linting 152ms
	norm_num 15.1ms
	parsing 79.1ms
	process pre-definitions 127ms
	ring 21.2ms
	share common exprs 116ms
	simp 5.56s
	tactic execution 12.9s
	type checking 46.7s
	typeclass inference 31.5s
real 58.77
user 109.10
sys 1.77

LeanPool/Monlib4/QuantumGraph/QamA.lean

import took 2.17s
typeclass inference of MulActionHomClass took 140ms
typeclass inference of NonUnitalNonAssocSemiring took 287ms
tactic execution of Lean.Parser.Tactic.rewriteSeq took 107ms
typeclass inference of MulActionHomClass took 297ms
typeclass inference of MulActionHomClass took 241ms
typeclass inference of CommMonoid took 141ms
simp took 129ms
typeclass inference of MulActionHomClass took 153ms
typeclass inference of MulActionHomClass took 212ms
type checking took 159ms
LeanPool/Monlib4/QuantumGraph/QamA.lean:211:2: error: failed to synthesize
  AddMonoidHomClass ((ℍ →ₗ[ℂ] ℍ) ≃ₗ[ℂ] ℍ ⊗[ℂ] ℍᵐᵒᵖ) ?m.257 ?m.258
(deterministic) timeout at `typeclass`, maximum number of heartbeats (20000) has been reached

Note: Use `set_option synthInstance.maxHeartbeats <num>` to set the limit.

Hint: Additional diagnostic information may be available using the `set_option diagnostics true` command.

Hint: Additional diagnostic information may be available using the `set_option diagnostics true` command.
typeclass inference of NonUnitalNonAssocSemiring took 284ms
typeclass inference of NonUnitalSemiring took 109ms
typeclass inference of AddMonoidHomClass took 288ms
LeanPool/Monlib4/QuantumGraph/QamA.lean:278:11: error: failed to synthesize
  AddMonoidHomClass ((ℍ →ₗ[ℂ] ℍ) ≃ₗ[ℂ] ℍ ⊗[ℂ] ℍᵐᵒᵖ) ?m.573 ?m.574
(deterministic) timeout at `typeclass`, maximum number of heartbeats (20000) has been reached

Note: Use `set_option synthInstance.maxHeartbeats <num>` to set the limit.

Hint: Additional diagnostic information may be available using the `set_option diagnostics true` command.

Hint: Additional diagnostic information may be available using the `set_option diagnostics true` command.
typeclass inference of NonUnitalNonAssocSemiring took 284ms
typeclass inference of NonUnitalSemiring took 113ms
typeclass inference of AddMonoidHomClass took 292ms
interpretation of Lean.Elab.Tactic._aux_Mathlib_Tactic_Widget_Calc___elabRules_Lean_calcTactic_1._boxed took 104ms
interpretation of Lean.Elab.Tactic._aux_Mathlib_Tactic_Widget_Calc___elabRules_Lean_calcTactic_1._boxed took 106ms
interpretation of Lean.Elab.Tactic._aux_Mathlib_Tactic_Widget_Calc___elabRules_Lean_calcTactic_1._boxed took 142ms
tactic execution of Lean.Parser.Tactic.rewriteSeq took 144ms
tactic execution of Lean.Parser.Tactic.rewriteSeq took 159ms
type checking took 102ms
LeanPool/Monlib4/QuantumGraph/QamA.lean:569:6: error: failed to synthesize
  Module ℂ (ℍ →L[ℂ] ℍ)
(deterministic) timeout at `typeclass`, maximum number of heartbeats (20000) has been reached

Note: Use `set_option synthInstance.maxHeartbeats <num>` to set the limit.

Hint: Additional diagnostic information may be available using the `set_option diagnostics true` command.

Hint: Additional diagnostic information may be available using the `set_option diagnostics true` command.
typeclass inference of HSMul took 135ms
typeclass inference of Module took 147ms
typeclass inference of Module took 132ms
typeclass inference of SeminormedAddCommGroup took 1.41s
typeclass inference of Module took 412ms
typeclass inference of NoZeroDivisors took 102ms
tactic execution of Lean.Parser.Tactic.rewriteSeq took 125ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 205ms
tactic execution of Lean.Parser.Tactic.rewriteSeq took 144ms
tactic execution of Lean.Parser.Tactic.rewriteSeq took 150ms
type checking took 110ms
LeanPool/Monlib4/QuantumGraph/QamA.lean:825:6: error: failed to synthesize
  Module ℂ (ℍ →L[ℂ] ℍ)
(deterministic) timeout at `typeclass`, maximum number of heartbeats (20000) has been reached

Note: Use `set_option synthInstance.maxHeartbeats <num>` to set the limit.

Hint: Additional diagnostic information may be available using the `set_option diagnostics true` command.

Hint: Additional diagnostic information may be available using the `set_option diagnostics true` command.
typeclass inference of MulActionHomClass took 133ms
typeclass inference of MulActionHomClass took 210ms
typeclass inference of MulActionHomClass took 227ms
typeclass inference of MulActionHomClass took 112ms
typeclass inference of ContinuousConstSMul took 108ms
typeclass inference of Module took 148ms
typeclass inference of Module took 138ms
typeclass inference of SeminormedAddCommGroup took 1.43s
typeclass inference of Module took 394ms
typeclass inference of MulActionHomClass took 243ms
typeclass inference of NonUnitalNonAssocSemiring took 278ms
typeclass inference of MulActionHomClass took 257ms
typeclass inference of MulActionHomClass took 135ms
simp took 102ms
type checking took 105ms
typeclass inference of MulActionHomClass took 249ms
typeclass inference of MulActionHomClass took 204ms
typeclass inference of MulActionHomClass took 126ms
type checking took 125ms
elaboration took 5.32s
tactic execution of Lean.Parser.Tactic.refine took 162ms
typeclass inference of QuantumSetDeltaForm took 175ms
tactic execution of Lean.Parser.Tactic.rewriteSeq took 142ms
elaboration took 4.89s
tactic execution of Lean.Parser.Tactic.refine took 150ms
typeclass inference of QuantumSetDeltaForm took 172ms
tactic execution of Lean.Parser.Tactic.exact took 145ms
cumulative profiling times:
	attribute application 4.14ms
	blocked (unaccounted) 333ms
	compilation (IR) 7.35ms
	compilation (LCNF base) 217ms
	compilation (LCNF impure) 40.2ms
	compilation (LCNF mono) 115ms
	congr simp thm 141ms
	elaboration 12.4s
	fix level params 37.5ms
	import 2.17s
	initialization 27.3ms
	instantiate metavars 54.7ms
	interpretation 2.64s
	let-to-have transformation 6.73ms
	linting 151ms
	norm_num 35.1ms
	parsing 92.3ms
	process pre-definitions 147ms
	ring 25.1ms
	share common exprs 135ms
	simp 6.61s
	tactic execution 7.36s
	type checking 2.9s
	typeclass inference 38s
real 23.02
user 72.34
sys 1.57
error: profile command exited with status 1

LeanPool/Monlib4/QuantumGraph/QamAExample.lean

import took 2.09s
simp took 169ms
simp took 298ms
simp took 226ms
simp took 157ms
simp took 217ms
simp took 128ms
simp took 112ms
typeclass inference of MulActionHomClass took 175ms
tactic execution of Lean.Parser.Tactic.exact took 109ms
cumulative profiling times:
	aesop 41.7ms
	attribute application 11.8ms
	blocked (unaccounted) 39.5ms
	compilation (IR) 1.51ms
	compilation (LCNF base) 35.7ms
	compilation (LCNF impure) 9.02ms
	compilation (LCNF mono) 28.1ms
	congr simp thm 71.9ms
	elaboration 664ms
	fix level params 7.97ms
	import 2.09s
	initialization 27.1ms
	instantiate metavars 10.6ms
	interpretation 795ms
	let-to-have transformation 1.51ms
	linting 47.8ms
	parsing 36.3ms
	process pre-definitions 34.9ms
	share common exprs 28.2ms
	simp 3.36s
	tactic execution 976ms
	type checking 472ms
	typeclass inference 2.66s
real 6.15
user 10.74
sys 1.31

LeanPool/Monlib4/QuantumGraph/ToProjections.lean

import took 2.15s
tactic execution of Lean.Parser.Tactic.change took 180ms
elaboration took 119ms
LeanPool/Monlib4/QuantumGraph/ToProjections.lean:298:2: error: failed to synthesize
  AddMonoidHomClass (ℍ ⊗[ℂ] ℍᵐᵒᵖ ≃ₗ[ℂ] ℍ →ₗ[ℂ] ℍ) ?m.557 ?m.558
(deterministic) timeout at `typeclass`, maximum number of heartbeats (20000) has been reached

Note: Use `set_option synthInstance.maxHeartbeats <num>` to set the limit.

Hint: Additional diagnostic information may be available using the `set_option diagnostics true` command.

Hint: Additional diagnostic information may be available using the `set_option diagnostics true` command.
typeclass inference of NonUnitalNonAssocSemiring took 187ms
typeclass inference of AddMonoidHomClass took 194ms
simp took 191ms
typeclass inference of ZeroHomClass took 202ms
simp took 145ms
elaboration took 117ms
tactic execution of Lean.Parser.Tactic.rewriteSeq took 161ms
LeanPool/Monlib4/QuantumGraph/ToProjections.lean:596:50: error: failed to synthesize
  AddMonoidHomClass (ℍ ⊗[ℂ] ℍᵐᵒᵖ ≃ₗ[ℂ] ℍ →ₗ[ℂ] ℍ) ?m.273 ?m.274
(deterministic) timeout at `typeclass`, maximum number of heartbeats (20000) has been reached

Note: Use `set_option synthInstance.maxHeartbeats <num>` to set the limit.

Hint: Additional diagnostic information may be available using the `set_option diagnostics true` command.

Hint: Additional diagnostic information may be available using the `set_option diagnostics true` command.
typeclass inference of NonUnitalNonAssocSemiring took 185ms
typeclass inference of AddMonoidHomClass took 181ms
simp took 415ms
interpretation of Lean.Elab.Tactic._aux_Mathlib_Tactic_Widget_Calc___elabRules_Lean_calcTactic_1._boxed took 159ms
tactic execution of Lean.Parser.Tactic.exact took 174ms
elaboration took 3.52s
tactic execution of Lean.Parser.Tactic.refine took 115ms
typeclass inference of QuantumSetDeltaForm took 119ms
typeclass inference of QuantumSetDeltaForm took 146ms
tactic execution of Lean.Parser.Tactic.exact took 225ms
elaboration took 3.32s
tactic execution of Lean.Parser.Tactic.refine took 173ms
typeclass inference of QuantumSetDeltaForm took 177ms
tactic execution of Lean.Parser.Tactic.rewriteSeq took 125ms
typeclass inference of OneHomClass took 101ms
typeclass inference of CompleteSpace took 119ms
typeclass inference of MulActionHomClass took 110ms
cumulative profiling times:
	attribute application 85.9ms
	blocked (unaccounted) 2.37s
	compilation (IR) 5.4ms
	compilation (LCNF base) 203ms
	compilation (LCNF impure) 28.3ms
	compilation (LCNF mono) 75.6ms
	congr simp thm 113ms
	elaboration 8.98s
	fix level params 19.7ms
	import 2.15s
	initialization 28ms
	instantiate metavars 23.8ms
	interpretation 1.45s
	let-to-have transformation 11.7ms
	linting 96.2ms
	norm_num 16ms
	parsing 60.8ms
	process pre-definitions 127ms
	share common exprs 58.6ms
	simp 2.47s
	tactic execution 3.86s
	type checking 1.93s
	typeclass inference 16.9s
real 24.10
user 38.34
sys 1.41
error: profile command exited with status 1

LeanPool/Monlib4/RepTheory.lean

import took 1.77s
cumulative profiling times:
	elaboration 0.159ms
	import 1.77s
	initialization 27.3ms
	interpretation 178ms
	linting 0.211ms
	parsing 0.0273ms
real 2.60
user 1.57
sys 1.04

LeanPool/Monlib4/RepTheory/AutMat.lean

import took 1.77s
typeclass inference of AddHomClass took 113ms
typeclass inference of AddHomClass took 101ms
typeclass inference of AddHomClass took 120ms
cumulative profiling times:
	aesop 184ms
	attribute application 14.9ms
	blocked (unaccounted) 374ms
	compilation (IR) 7.13ms
	compilation (LCNF base) 112ms
	compilation (LCNF impure) 39ms
	compilation (LCNF mono) 108ms
	congr simp thm 72.7ms
	elaboration 823ms
	fix level params 24ms
	import 1.77s
	initialization 26.8ms
	instantiate metavars 56.2ms
	interpretation 1.52s
	let-to-have transformation 2.84ms
	linting 93.9ms
	parsing 82.1ms
	process pre-definitions 139ms
	share common exprs 67.5ms
	simp 3.5s
	tactic execution 2.42s
	type checking 1.02s
	typeclass inference 10.2s
real 11.08
user 21.72
sys 1.23

Advisory only — never blocks merge. Full log uploaded as the proof-profile artifact.

@github-actions

github-actions Bot commented May 16, 2026 •
edited
Loading

Copy link
Copy Markdown
Contributor

🤖 LLM review (gpt-5.5)

Reviewed head: 0e975f82548b7202855a4eacc1b47448adb9dcbd

Verdict: 🤔 needs_discussion

This PR vendors and ports a large theorem-bearing subset of monlib4: finite-dimensional operator-algebra infrastructure, matrix-algebra inner automorphisms, faithful positive functionals and induced Hilbert structures, quantum sets, Schur products, and quantum-graph predicates/examples. It has a project card and provenance, and it contains named graduate/research-level mathematics rather than isolated lemmas, but it is primarily a library import/port with much of the downstream quantum-graph theorem stack explicitly not included.

Aspect Value
Fit 🟡 borderline
Level research
Branch operator algebras and quantum graph theory
Mode theory_building
Obscure problem no
Code quality 3 / 5

The contribution is a substantial formal operator-algebra/quantum-set library, including innerness of full matrix-algebra automorphisms and the core quantum-set/quantum-graph API, but it is not a single completed theorem project.

Tokens: 335,457 in / 766 out · Tier: flex · Cost: $0.8501
Automated review against .github/REVIEW_RULES.md. Disagree? Reply on the PR; rules can be updated in a PR of their own.

@Vilin97
Vilin97 marked this pull request as ready for review May 18, 2026 01:37
Copilot AI review requested due to automatic review settings May 18, 2026 01:37
Copilot AI reviewed May 18, 2026

Copilot AI left a comment

Copy link
Copy Markdown

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Copilot encountered an error and was unable to review this pull request. You can try again by re-requesting a review.

@Vilin97

Vilin97 commented May 18, 2026

Copy link
Copy Markdown
Collaborator Author

/profile

1 similar comment
@Vilin97

Vilin97 commented May 18, 2026

Copy link
Copy Markdown
Collaborator Author

/profile

@Vilin97

Vilin97 commented May 18, 2026

Copy link
Copy Markdown
Collaborator Author

Closing per the LLM-review decision and follow-up inspection. The submitted monlib4 slice is reusable API/infrastructure rather than a completed project: matrix reshaping, direct-sum maps, helper lemmas, and isolated results. I could not find a downstream monlib4 theorem that would make this a Lean Pool project on its own.

@Vilin97 Vilin97 closed this May 18, 2026
@Vilin97 Vilin97 reopened this May 18, 2026
@Vilin97

Vilin97 commented May 18, 2026

Copy link
Copy Markdown
Collaborator Author

Reopening. The earlier close treated the submitted slice as the final project, but this looks like the same partial-port failure mode: the import contains only a small foundational subset of monlib4. I am dispatching a worker to audit the upstream repository and port the missing substantive downstream theorem/content rather than closing on the fragment.

@Vilin97

Vilin97 commented May 18, 2026

Copy link
Copy Markdown
Collaborator Author

Partial-port audit confirms this one strongly: upstream themathqueen/monlib4 is about 89 Lean files / 27k non-comment LOC, while this PR imports about 18 files / 721 LOC, mostly foundational utility lemmas. The upstream library contains the quantum-set/quantum-graph and operator-algebra theorem layers, so this should remain open as incomplete port work rather than be judged on the current utility subset alone.

@Vilin97

Vilin97 commented May 18, 2026

Copy link
Copy Markdown
Collaborator Author

/review

@Vilin97

Vilin97 commented May 18, 2026

Copy link
Copy Markdown
Collaborator Author

/review

@Vilin97

Vilin97 commented May 18, 2026

Copy link
Copy Markdown
Collaborator Author

/review

@Vilin97 ChatGPT Codex Connector

Vilin97 commented May 19, 2026

Copy link
Copy Markdown
Collaborator Author

/review

@github-actions

github-actions Bot commented May 19, 2026

Copy link
Copy Markdown
Contributor

LLM review skipped: Lean Action CI conclusion was in_progress. Push a fix or comment /review after CI is green.

@Vilin97

Vilin97 commented May 19, 2026

Copy link
Copy Markdown
Collaborator Author

/review

@Vilin97

Vilin97 commented May 19, 2026

Copy link
Copy Markdown
Collaborator Author

Follow-up on the partial-port concern: I pushed 3003a9a, which restores a practical quantum-graph core instead of leaving Monlib4 at only the matrix/quantum-set fragment. The branch now includes LeanPool/Monlib4/LinearAlgebra/QuantumSet/SchurMul.lean, LeanPool/Monlib4/QuantumGraph.lean, and LeanPool/Monlib4/QuantumGraph/Basic.lean, with schurMul, schurProjection, QuantumGraph, QuantumGraph.IsReal, and QuantumGraph.Real registered in the project metadata.

This is still not a full upstream Monlib4 port. The remaining QuantumSet.Symm, QuantumSet.TensorProduct, QuantumSet.Subset, QuantumSet.PhiMap, and most QuantumGraph/* files depend on the unported Ips/tensor-product/MyBimodule/PosMap stack and upstream finite-dimensional Hilbert-algebra coalgebra instances; upstream also uses many heartbeat/linter overrides and has active sorrys in LinearAlgebra/Blackbox.lean. Local checks passed for the pushed slice: lake build LeanPool.Monlib4, lake exe mk_all --check, lake exe runLinter LeanPool.Monlib4, lake exe lint-style LeanPool.Monlib4, and python -m lean_pool.quality --repo ...

@Vilin97

Vilin97 commented May 19, 2026

Copy link
Copy Markdown
Collaborator Author

CI update for 3003a9a: Lean Action CI, doc-gen, and the content guard are green. The new deterministic partial-port audit fails, correctly: it reports LeanPool.Monlib4 imported 26/88 Lean files and 1323/25992 non-comment LOC from themathqueen/monlib4, with largest missing files including Monlib/QuantumGraph/PiMat.lean, Monlib/LinearAlgebra/PosMap_isReal.lean, Monlib/LinearAlgebra/Ips/MatIps.lean, and Monlib/QuantumGraph/QamA.lean. So this branch is now better than the original fragment, but still request-changes for a real full-port gap.

@Vilin97

Vilin97 commented May 19, 2026

Copy link
Copy Markdown
Collaborator Author

/review

@Vilin97

Vilin97 commented May 20, 2026

Copy link
Copy Markdown
Collaborator Author

Progress update after 5e096e7 (Restore Monlib4 matrix star order API).

Restored the upstream Monlib/LinearAlgebra/Matrix/StarOrderedRing.lean compatibility layer as LeanPool/Monlib4/LinearAlgebra/Matrix/StarOrderedRing.lean, adapting it to current Mathlib where the underlying matrix order and some spectrum/eigenvalue facts already exist. This brings back the Monlib-facing API around negative semidefinite/definite matrices, spectral positivity criteria, Matrix.posSemidef_iff_commute, inner-automorphism preservation for negative positivity, Matrix.Pi.le_iff_sub_nonneg, and Matrix.innerAut.map_pow.

Verification passed locally:

  • lake build LeanPool.Monlib4.LinearAlgebra.Matrix.StarOrderedRing
  • lake exe runLinter LeanPool.Monlib4.LinearAlgebra.Matrix.StarOrderedRing
  • lake exe lint-style LeanPool/Monlib4/LinearAlgebra/Matrix/StarOrderedRing.lean
  • lake build LeanPool.Monlib4.LinearAlgebra.Matrix
  • lake build LeanPool.Monlib4
  • lake exe runLinter LeanPool.Monlib4
  • lake exe lint-style LeanPool/Monlib4
  • lake build LeanPool
  • lake exe mk_all --check
  • uv run python -m lean_pool.quality --repo ..
  • git diff --check

Partial-port audit still flags the PR as incomplete: imported 70/87 upstream Lean files and 10103/25889 non-comment LOC. Largest unmatched upstream files currently reported:

  • Monlib/LinearAlgebra/PosMap_isReal.lean
  • Monlib/LinearAlgebra/Ips/MatIps.lean
  • Monlib/QuantumGraph/QamA.lean
  • Monlib/LinearAlgebra/Ips/MinimalProj.lean
  • Monlib/LinearAlgebra/Ips/Nontracial.lean
  • Monlib/LinearAlgebra/Ips/Functional.lean
  • Monlib/QuantumGraph/ToProjections.lean
  • Monlib/LinearAlgebra/QuantumSet/Instances.lean

Continuing with the upstream dependency chain; this is still not review-ready.

@Vilin97

Vilin97 commented May 20, 2026

Copy link
Copy Markdown
Collaborator Author

Progress update after d186445 (Restore Monlib4 positive definite powers).

Restored upstream Monlib/LinearAlgebra/Matrix/PosDefRpow.lean as LeanPool/Monlib4/LinearAlgebra/Matrix/PosDefRpow.lean, adapted to current Mathlib. This brings back:

  • Matrix.IsHermitian.eigenvectorMatrix compatibility names
  • Matrix.IsHermitian.rpow
  • Matrix.PosSemidef.rpow
  • Matrix.PosDef.rpow
  • PosDef.rpow_mul_rpow, rpow_zero, rpow_one_eq_self, rpow_neg_one_eq_inv_self
  • positive semidefinite/definite preservation of rpow
  • CFC square-root compatibility via sqrt_eq_rpow
  • Matrix.posDefOne_rpow

Verification passed locally:

  • lake build LeanPool.Monlib4.LinearAlgebra.Matrix.PosDefRpow
  • lake exe runLinter LeanPool.Monlib4.LinearAlgebra.Matrix.PosDefRpow
  • lake exe lint-style LeanPool/Monlib4/LinearAlgebra/Matrix/PosDefRpow.lean
  • lake build LeanPool.Monlib4.LinearAlgebra.Matrix
  • lake build LeanPool.Monlib4
  • lake exe runLinter LeanPool.Monlib4
  • lake exe lint-style LeanPool/Monlib4
  • lake build LeanPool
  • lake exe mk_all --check
  • uv run python -m lean_pool.quality --repo ..
  • git diff --check

Partial-port audit still flags the PR as incomplete: imported 71/87 upstream Lean files and 10314/25889 non-comment LOC. Largest unmatched upstream files currently reported:

  • Monlib/LinearAlgebra/PosMap_isReal.lean
  • Monlib/LinearAlgebra/Ips/MatIps.lean
  • Monlib/QuantumGraph/QamA.lean
  • Monlib/LinearAlgebra/Ips/MinimalProj.lean
  • Monlib/LinearAlgebra/Ips/Nontracial.lean
  • Monlib/LinearAlgebra/Ips/Functional.lean
  • Monlib/QuantumGraph/ToProjections.lean
  • Monlib/LinearAlgebra/QuantumSet/Instances.lean

Continuing the full-port repair; this PR is still not review-ready.

@Vilin97

Vilin97 commented May 20, 2026

Copy link
Copy Markdown
Collaborator Author

Follow-up partial-port work at 8970235 (Restore Monlib4 quantum set inner algebra coherence).

What changed:

  • Restored the upstream-style InnerProductAlgebra shape in QuantumSet.Basic, so the normed/additive/module structures are built from the existing starAlgebra ring/algebra structure instead of creating a separate incompatible module/additive structure.
  • Restored upstream core declarations QuantumSet.toFinite, QuantumSet.modAut_isSelfAdjoint, and LinearMap.adjoint_real_eq.
  • Updated the finite-product quantum-set instance in QuantumSet.Pi to provide the explicit inner-product algebra fields.

Why this matters for the partial-port audit: the old simplified class was blocking faithful restoration of omitted downstream files such as QuantumSet/TensorProduct.lean, QuantumSet/Symm.lean, and the quantum-graph layer because tensor norms, adjoints, and Module.Finite were using non-defeq module/additive structures. After this fix, QuantumSet/TensorProduct.lean gets past that root coherence failure; it still needs a careful adapted port before it can be added.

Verified locally:

  • lake build LeanPool.Monlib4
  • lake build LeanPool
  • lake exe runLinter LeanPool.Monlib4.LinearAlgebra.QuantumSet.Basic
  • lake exe runLinter LeanPool.Monlib4.LinearAlgebra.QuantumSet.Pi
  • lake exe runLinter LeanPool.Monlib4
  • lake exe lint-style LeanPool/Monlib4/LinearAlgebra/QuantumSet/Basic.lean LeanPool/Monlib4/LinearAlgebra/QuantumSet/Pi.lean
  • lake exe lint-style LeanPool/Monlib4
  • lake exe mk_all --check
  • uv run python -m lean_pool.quality --repo ..
  • git diff --check

Partial-port audit still fails: 71/87 upstream files, 10397/25889 non-comment LOC, LOC ratio 0.4016. The top reported missing files remain:

  • Monlib/LinearAlgebra/PosMap_isReal.lean
  • Monlib/LinearAlgebra/Ips/MatIps.lean
  • Monlib/QuantumGraph/QamA.lean
  • Monlib/LinearAlgebra/Ips/MinimalProj.lean
  • Monlib/LinearAlgebra/Ips/Nontracial.lean
  • Monlib/LinearAlgebra/Ips/Functional.lean
  • Monlib/QuantumGraph/ToProjections.lean
  • Monlib/LinearAlgebra/QuantumSet/Instances.lean

This PR is still incomplete; this commit removes a core blocker for the next missing-file restorations rather than resolving the audit.

@Vilin97

Vilin97 commented May 20, 2026

Copy link
Copy Markdown
Collaborator Author

Restored upstream Monlib/LinearAlgebra/QuantumSet/TensorProduct.lean in commit b26571a and wired it into both the Monlib4 QuantumSet index and LeanPool.lean. This also adds the coalgebra-hom preservation lemma needed by the tensor-product comul_real proof.

Local gates passed after the commit:

  • lake build LeanPool.Monlib4.LinearAlgebra.QuantumSet.TensorProduct
  • lake exe runLinter LeanPool.Monlib4.LinearAlgebra.QuantumSet.TensorProduct
  • lake exe lint-style LeanPool/Monlib4/LinearAlgebra/QuantumSet/TensorProduct.lean LeanPool/Monlib4/LinearAlgebra/QuantumSet.lean LeanPool/Monlib4/LinearAlgebra/QuantumSet/Basic.lean
  • lake build LeanPool.Monlib4
  • lake exe runLinter LeanPool.Monlib4
  • lake exe lint-style LeanPool/Monlib4
  • lake build LeanPool
  • lake exe mk_all --check
  • uv run python -m lean_pool.quality --repo ..
  • git diff --check

This PR is still not complete. The path-aware upstream comparison now has QuantumSet/TensorProduct.lean, but still shows only 61/87 upstream file paths represented, with large missing areas including QuantumGraph/PiMat.lean, LinearAlgebra/PosMap_isReal.lean, LinearAlgebra/Ips/MatIps.lean, QuantumGraph/QamA.lean, LinearAlgebra/Ips/MinimalProj.lean, LinearAlgebra/Ips/Nontracial.lean, QuantumGraph/Matrix.lean, and LinearAlgebra/Ips/Functional.lean. I am continuing the full-port pass rather than rerunning review yet.

@Vilin97

Vilin97 commented May 20, 2026

Copy link
Copy Markdown
Collaborator Author

Restored another upstream Monlib4 layer in commit c42567c:

  • LinearAlgebra/Ips/MinimalProj.lean
  • LinearAlgebra/QuantumSet/PhiMap.lean
  • LinearAlgebra/QuantumSet/QIso.lean
  • LinearAlgebra/QuantumSet/SchurMulTensor.lean
  • LinearAlgebra/QuantumSet/Symm.lean
  • the missing QuantumSet.Basic Psi/Upsilon/Frobenius/helper layer used by those files

Verified locally for this checkpoint:

  • lake build LeanPool.Monlib4
  • lake build LeanPool.Monlib4.LinearAlgebra.Ips
  • lake build LeanPool.Monlib4.LinearAlgebra.QuantumSet
  • lake exe runLinter LeanPool.Monlib4.LinearAlgebra.Ips
  • lake exe runLinter LeanPool.Monlib4.LinearAlgebra.QuantumSet
  • focused lint-style over the changed Ips/QuantumSet files
  • git diff --cached --check
  • forbidden-token scan over the staged files (sorry/admit/unsafe/partial/set_option/waiver text)

I did not rerun mk_all --check yet because the next in-progress files, QuantumSet/Subset.lean and TensorProduct/Submodule.lean, are present in the worktree but not yet repaired/indexed. They remain the next active porting targets.

@Vilin97

Vilin97 commented May 20, 2026

Copy link
Copy Markdown
Collaborator Author

Pushed another Monlib4 checkpoint: 5d9b5e3 Restore Monlib4 tensor submodule helpers.

This restores and indexes:

  • LeanPool/Monlib4/LinearAlgebra/Ips/Vn.lean
  • LeanPool/Monlib4/LinearAlgebra/TensorProduct/Submodule.lean

Verification run locally:

  • lake build LeanPool.Monlib4.LinearAlgebra.TensorProduct LeanPool.Monlib4.LinearAlgebra.Ips
  • lake exe runLinter LeanPool.Monlib4.LinearAlgebra.Ips LeanPool.Monlib4.LinearAlgebra.TensorProduct
  • lake exe lint-style LeanPool/Monlib4/LinearAlgebra/Ips.lean LeanPool/Monlib4/LinearAlgebra/Ips/Vn.lean LeanPool/Monlib4/LinearAlgebra/TensorProduct.lean LeanPool/Monlib4/LinearAlgebra/TensorProduct/Submodule.lean
  • lake build LeanPool.Monlib4
  • lake exe runLinter LeanPool.Monlib4
  • git diff --cached --check before commit, plus a staged scan for forbidden tokens/waiver markers.

QuantumSet/Subset.lean is still being ported and is not included in this checkpoint.

@Vilin97

Vilin97 commented May 20, 2026

Copy link
Copy Markdown
Collaborator Author

Pushed e671d12 Restore Monlib4 quantum set subset transport.

This restores and indexes LeanPool/Monlib4/LinearAlgebra/QuantumSet/Subset.lean, and also fixes missing Lean Pool file headers in the recently restored QIso.lean and TensorProduct/Submodule.lean that the repository quality checker caught.

Verification run locally:

  • lake build LeanPool.Monlib4.LinearAlgebra.QuantumSet.Subset
  • lake exe runLinter LeanPool.Monlib4.LinearAlgebra.QuantumSet.Subset
  • lake exe lint-style LeanPool/Monlib4/LinearAlgebra/QuantumSet/Subset.lean
  • lake build LeanPool.Monlib4.LinearAlgebra.QuantumSet
  • lake exe runLinter LeanPool.Monlib4.LinearAlgebra.QuantumSet
  • lake build LeanPool.Monlib4
  • lake exe runLinter LeanPool.Monlib4
  • lake build LeanPool
  • lake exe mk_all --check
  • uv run python -m lean_pool.quality --repo ..
  • git diff --cached --check and staged forbidden-token/waiver scan before commit.

@Vilin97

Vilin97 commented May 20, 2026

Copy link
Copy Markdown
Collaborator Author

Restored another omitted Monlib4 upstream layer in commit 39961d1:\n\n- Added LeanPool/Monlib4/LinearAlgebra/PosMapIsReal.lean, ported from upstream Monlib/LinearAlgebra/PosMap_isReal.lean.\n- Registered it in LeanPool/Monlib4/LinearAlgebra.lean and LeanPool.lean.\n- Kept the Lean Pool style-compatible module name PosMapIsReal rather than upstream PosMap_isReal.\n\nLocal verification passed:\n\n- lake build LeanPool.Monlib4.LinearAlgebra.PosMapIsReal\n- lake exe runLinter LeanPool.Monlib4.LinearAlgebra.PosMapIsReal\n- lake exe lint-style LeanPool/Monlib4/LinearAlgebra/PosMapIsReal.lean\n- uv run python -m lean_pool.quality --repo ..\n- lake build LeanPool\n- lake exe mk_all --check\n\nThis removes the large missing positive-map realness layer from the partial-port audit; remaining missing upstream Monlib4 files still need to be ported before the PR is complete.

@Vilin97

Vilin97 commented May 20, 2026

Copy link
Copy Markdown
Collaborator Author

Restored the upstream Monlib4 functional inner-product layer in 9439fbb.

This adds LeanPool/Monlib4/LinearAlgebra/Ips/Functional.lean, registers it in the import indices, and restores the matrix compatibility lemmas that the file needs in PosEqLinearMapIsPositive.lean. I avoided the upstream active set_option synthInstance.checkSynthOrder false pattern by constructing the relevant normed/inner-product structures explicitly.

Checks passed locally:

  • lake build LeanPool.Monlib4.LinearAlgebra.Ips.Functional
  • lake exe runLinter LeanPool.Monlib4.LinearAlgebra.Matrix.PosEqLinearMapIsPositive LeanPool.Monlib4.LinearAlgebra.Ips.Functional
  • lake exe lint-style LeanPool/Monlib4/LinearAlgebra/Matrix/PosEqLinearMapIsPositive.lean LeanPool/Monlib4/LinearAlgebra/Ips/Functional.lean LeanPool/Monlib4/LinearAlgebra/Ips.lean
  • lake build LeanPool.Monlib4.LinearAlgebra.Ips
  • lake build LeanPool
  • lake exe mk_all --check
  • uv run python -m lean_pool.quality --repo ..

Post-commit partial-port audit now reports 82/86 imported Lean files and 15,431/25,812 non-comment LOC. The largest remaining unmatched upstream files start with LinearAlgebra/Ips/MatIps.lean, LinearAlgebra/Ips/Nontracial.lean, and the QuantumGraph/* layer; MatIps.lean is the next dependency bottleneck.

@Vilin97

Vilin97 commented May 24, 2026

Copy link
Copy Markdown
Collaborator Author

/review

Pushed a fuller Monlib4 port repair in aca8a15. Local gates pass: lake build LeanPool, lake exe mk_all --check, lake exe runLinter LeanPool, lake exe lint-style LeanPool, and uv run python -m lean_pool.quality --repo ... The only remaining declaration-audit misses are the upstream Blackbox spectral declarations that depend on upstream sorrys, so I did not add axioms or placeholders.

@github-actions

github-actions Bot commented May 24, 2026

Copy link
Copy Markdown
Contributor

LLM review skipped: Lean Action CI conclusion was in_progress. Push a fix or comment /review after CI is green.

@Vilin97

Vilin97 commented May 24, 2026

Copy link
Copy Markdown
Collaborator Author

/review

@Vilin97

Vilin97 commented May 26, 2026

Copy link
Copy Markdown
Collaborator Author

Manual completion audit on the current head aca8a15:

  • Local deterministic audit still reports some same-file LOC gaps, but no missing whole importable upstream files; the branch has 98 imported Lean files against 87 importable upstream files, and 28898/25889 non-comment LOC.
  • I then checked the importable upstream declaration surface directly: after excluding upstream files blocked by active sorry/forbidden constructs and their dependents, all 520 public declaration names from upstream resolve after import LeanPool.Monlib4 on this branch. The Lean check exited 0 with 0 unknown identifiers.
  • The remaining truncated-file warnings are explained by Mathlib-provided declarations, compatibility aliases, namespace/root-name adjustments, and proof compaction/splitting during the port.

So I now consider the earlier partial-port failure mode repaired for #76. Requesting a fresh LLM review on the completed current head.

/review

@Vilin97

Vilin97 commented May 26, 2026

Copy link
Copy Markdown
Collaborator Author

/review

1 similar comment
@Vilin97

Vilin97 commented Jun 1, 2026

Copy link
Copy Markdown
Collaborator Author

/review

@Vilin97

Vilin97 commented Jun 1, 2026

Copy link
Copy Markdown
Collaborator Author

/profile

@Vilin97
Vilin97 merged commit d361ce7 into main Jun 1, 2026
4 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

Copilot code review Copilot
Copilot review effort
Applies to this pull request for everyone.Learn more about Copilot code review.
Copilot left review comments

Assignees

No one assigned

Labels

None yet

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

2 participants

@Vilin97