❌ Latest Build Failed: Hochster

Project build failed

Build Log

✖ [2412/2419] Building Hochster.Section2 (2.5s)
trace: .> LEAN_PATH=/home/nfr/actions-runner/_work/doc-verification-bridge/doc-verification-bridge/experiments/repos/Hochster/.lake/packages/Cli/.lake/build/lib/lean:/home/nfr/actions-runner/_work/doc-verification-bridge/doc-verification-bridge/experiments/repos/Hochster/.lake/packages/batteries/.lake/build/lib/lean:/home/nfr/actions-runner/_work/doc-verification-bridge/doc-verification-bridge/experiments/repos/Hochster/.lake/packages/Qq/.lake/build/lib/lean:/home/nfr/actions-runner/_work/doc-verification-bridge/doc-verification-bridge/experiments/repos/Hochster/.lake/packages/aesop/.lake/build/lib/lean:/home/nfr/actions-runner/_work/doc-verification-bridge/doc-verification-bridge/experiments/repos/Hochster/.lake/packages/proofwidgets/.lake/build/lib/lean:/home/nfr/actions-runner/_work/doc-verification-bridge/doc-verification-bridge/experiments/repos/Hochster/.lake/packages/importGraph/.lake/build/lib/lean:/home/nfr/actions-runner/_work/doc-verification-bridge/doc-verification-bridge/experiments/repos/Hochster/.lake/packages/LeanSearchClient/.lake/build/lib/lean:/home/nfr/actions-runner/_work/doc-verification-bridge/doc-verification-bridge/experiments/repos/Hochster/.lake/packages/plausible/.lake/build/lib/lean:/home/nfr/actions-runner/_work/doc-verification-bridge/doc-verification-bridge/experiments/repos/Hochster/.lake/packages/mathlib/.lake/build/lib/lean:/home/nfr/actions-runner/_work/doc-verification-bridge/doc-verification-bridge/experiments/repos/Hochster/.lake/packages/checkdecls/.lake/build/lib/lean:/home/nfr/actions-runner/_work/doc-verification-bridge/doc-verification-bridge/experiments/repos/Hochster/.lake/build/lib/lean /home/nfr/.elan/toolchains/leanprover--lean4---v4.29.0/bin/lean /home/nfr/actions-runner/_work/doc-verification-bridge/doc-verification-bridge/experiments/repos/Hochster/Hochster/Section2.lean -o /home/nfr/actions-runner/_work/doc-verification-bridge/doc-verification-bridge/experiments/repos/Hochster/.lake/build/lib/lean/Hochster/Section2.olean -i /home/nfr/actions-runner/_work/doc-verification-bridge/doc-verification-bridge/experiments/repos/Hochster/.lake/build/lib/lean/Hochster/Section2.ilean -c /home/nfr/actions-runner/_work/doc-verification-bridge/doc-verification-bridge/experiments/repos/Hochster/.lake/build/ir/Hochster/Section2.c --setup /home/nfr/actions-runner/_work/doc-verification-bridge/doc-verification-bridge/experiments/repos/Hochster/.lake/build/ir/Hochster/Section2.setup.json --json
error: Hochster/Section2.lean:127:28: Tactic `rewrite` failed: Did not find an occurrence of the pattern
  generateFrom {s | IsConstructible s}
in the target expression
  generateFrom {s | IsConstructible s} =
    generateFrom ({s | IsOpen s ∧ IsCompact s} ∪ compl '' {s | IsOpen s ∧ IsCompact s})

X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : CompactSpace X
inst✝ : QuasiSeparatedSpace X
⊢ generateFrom {s | IsConstructible s} =
    generateFrom ({s | IsOpen s ∧ IsCompact s} ∪ compl '' {s | IsOpen s ∧ IsCompact s})
error: Hochster/Section2.lean:150:28: Tactic `rewrite` failed: Did not find an occurrence of the pattern
  generateFrom {s | IsConstructible s}
in the target expression
  generateFrom {s | IsConstructible s} ≤ T

X : Type u_1
T : TopologicalSpace X
inst✝² : CompactSpace X
inst✝¹ : QuasiSeparatedSpace X
inst✝ : PrespectralSpace X
⊢ generateFrom {s | IsConstructible s} ≤ T
error: Hochster/Section2.lean:252:45: Application type mismatch: The argument
  Set.mem_union_left ?m.119 ht1
has type
  t ∈ {U | IsOpen U ∧ IsCompact U} ∪ ?m.119
but is expected to have type
  t ∈ {s | IsConstructible s}
in the application
  isOpen_generateFrom_of_mem (Set.mem_union_left ?m.119 ht1)
error: Hochster/Section2.lean:258:68: Invalid `⟨...⟩` notation: The expected type of this term could not be determined
warning: Hochster/Section2.lean:245:4: This simp argument is unused:
  instTopologicalSpace_eq_generateFrom_isOpen_isCompact_union_compl_image

Hint: Omit it from the simp argument list.
  simp only [t2Space_iff, exists_and_left,̵
  ̵ ̵ ̵ ̵ ̵i̵n̵s̵t̵T̵o̵p̵o̵l̵o̵g̵i̵c̵a̵l̵S̵p̵a̵c̵e̵_̵e̵q̵_̵g̵e̵n̵e̵r̵a̵t̵e̵F̵r̵o̵m̵_̵i̵s̵O̵p̵e̵n̵_̵i̵s̵C̵o̵m̵p̵a̵c̵t̵_̵u̵n̵i̵o̵n̵_̵c̵o̵m̵p̵l̵_̵i̵m̵a̵g̵e̵]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
error: Hochster/Section2.lean:270:4: Type mismatch: After simplification, term
  h
 has type
  ∀ (x : ConstructibleTop X), ¬↑F ≤ 𝓝 x
but is expected to have type
  ∀ (x : X), ∃ t, x ∈ t ∧ (IsOpen t ∧ IsCompact t ∨ ∃ x, (IsOpen x ∧ IsCompact x) ∧ xᶜ = t) ∧ t ∉ F
error: Hochster/Section2.lean:590:65: Application type mismatch: The argument
  h
has type
  ¬(Y ∩ ⋂₀ {s | IsOpen s ∧ IsCompact s ∧ x ∈ s}).Nonempty
but is expected to have type
  ¬(Y ∩ ⋂ i, ↑i).Nonempty
in the application
  Set.not_nonempty_iff_eq_empty.mp h
warning: Hochster/Section2.lean:589:20: This simp argument is unused:
  ← Set.sInter_eq_iInter

Hint: Omit it from the simp argument list.
  simp only [t,̵ ̵←̵ ̵S̵e̵t̵.̵s̵I̵n̵t̵e̵r̵_̵e̵q̵_̵i̵I̵n̵t̵e̵r̵] at this

Note: Simp arguments with `←` have the additional effect of removing the other direction from the simp set, even if the simp argument itself is unused. If the hint above does not work, try replacing `←` with `-` to only get that effect and silence this warning.

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
error: Hochster/Section2.lean:628:64: Application type mismatch: The argument
  h'
has type
  ¬(⋂₀ ({s | IsOpen s ∧ IsCompact s ∧ x ∈ s} ∪ {s | IsOpen s ∧ IsCompact s ∧ y ∈ s})).Nonempty
but is expected to have type
  ¬(⋂ i, ↑i).Nonempty
in the application
  Set.not_nonempty_iff_eq_empty.mp h'
warning: Hochster/Section2.lean:627:36: This simp argument is unused:
  ← Set.sInter_eq_iInter

Hint: Omit it from the simp argument list.
  simp only [Set.univ_inter, t,̵ ̵←̵ ̵S̵e̵t̵.̵s̵I̵n̵t̵e̵r̵_̵e̵q̵_̵i̵I̵n̵t̵e̵r̵] at this

Note: Simp arguments with `←` have the additional effect of removing the other direction from the simp set, even if the simp argument itself is unused. If the hint above does not work, try replacing `←` with `-` to only get that effect and silence this warning.

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
error: Lean exited with code 1
Some required targets logged failures:
- Hochster.Section2
error: build failed

📋 View full command log (YAML)

← Back to Summary