{
  "command": "cd \"D:/Python/Quantum/research/lean/NguyenRH1\" && export PATH=\"$HOME/.elan/bin:$PATH\" && lake build NguyenRH1.LiDigamma 2>&1 | tail -3 && lake env lean NguyenRH1/LiArchimedean.lean 2>&1 | grep -v \"^$\" | head -30",
  "description": "Build LiDigamma olean then compile LiArchimedean",
  "timeout": 600000
}

  Note that `ring` works primarily in *commutative* rings. If you have a noncommutative ring, abelian group or module, consider using `noncomm_ring`, `abel` or `module` instead.
Build completed successfully (8738 jobs).
NguyenRH1/LiArchimedean.lean:154:26: error: numerals are data in Lean, but the expected type is a proposition
  ContinuousAt (HDiv.hDiv (1 + 0)) 2 : Prop
NguyenRH1/LiArchimedean.lean:171:10: error: Application type mismatch: The argument
  Continuous.div (Continuous.add continuous_id continuous_const) continuous_const
has type
  (∀ (x : ?m.426), ?m.429 ≠ 0) → Continuous[?m.428, ?m.428] ((id + fun x => ?m.415) / fun x => ?m.429)
but is expected to have type
  Continuous fun s => (1 + s) / 2
in the application
  Continuous.comp continuous_re (Continuous.div (Continuous.add continuous_id continuous_const) continuous_const)
NguyenRH1/LiArchimedean.lean:215:8: error: Type mismatch
  AnalyticAt.div (AnalyticAt.add analyticAt_const analyticAt_id) analyticAt_const
has type
  ?m.442 ≠ 0 → AnalyticAt ?m.434 (((fun x => ?m.404) + id) / fun x => ?m.442) ?m.443
but is expected to have type
  AnalyticAt ℂ (fun s => (1 + s) / 2) 0
NguyenRH1/LiArchimedean.lean:216:21: error: Application type mismatch: The argument
  h2
has type
  AnalyticAt ℂ (fun s => (1 + s) / 2) 0
but is expected to have type
  AnalyticAt ℂ (HDiv.hDiv (1 + 0)) 2
in the application
  AnalyticAt.comp h1 h2
NguyenRH1/LiArchimedean.lean:219:8: error: Tactic `rewrite` failed: Did not find an occurrence of the pattern
  iteratedDeriv j (fun x => ?m.537 * (1 / 2 * ((1 + x) / 2).digamma)) 0
in the target expression
  iteratedDeriv j (fun s => 1 / 2 * ((1 + s) / 2).digamma) 0 = (-1) ^ (j + 1) * ↑j ! * ↑(lagariasA (j + 1))
case inr
j : ℕ