feat(ConnectedComponents): new proofs by jjdishere · Pull Request #28 · chrisflav/proetale

jjdishere · 2026-03-24T07:35:41Z

No description provided.

jjdishere

Review of feat(ConnectedComponents): new proofs

The PR fills 3 sorry placeholders across 2 files. The mathematical content is correct — Prespectral.of_profinite, t2Space_connectedComponent, and lift_bijective_of_isPullback all follow sound proof strategies.

Main suggestions:

Several have blocks can be shortened significantly (see inline comments)
lift_bijective_of_isPullback at ~157 lines should be decomposed into helper lemmas
Check whether open Limits is actually needed
Commit message "AI progress" should be more descriptive

Overall the mathematics is solid — the style just needs tightening.

jjdishere · 2026-03-24T08:08:35Z

    SpectralSpace Y := pb.spectralSpace

+omit [SpectralSpace X] in
 theorem ConnectedComponents.lift_bijective_of_isPullback {Y T : Type u} [TopologicalSpace Y]


This proof is ~157 lines, well past the 100-line guideline. Consider extracting standalone helper lemmas:

hg_surj → a lemma like Function.Surjective_fst_of_isPullback (surjectivity of g from the pullback structure)

hFib → a lemma like IsPreconnected_fiber_of_isPullback (preconnectedness of fibers of g)

This would make the main proof much more readable and the helpers independently reusable.

- Shorten hxdata using `by ext z; simp` - Shorten hxU0/hyU0 using Set.mem_iInter₂ - Clean up inline `by simpa` in isClosed_and_iUnion_connectedComponent_eq_iff - Extract surjective_fst_of_isPullback and isPreconnected_fiber_of_isPullback as standalone helper lemmas from the 157-line lift_bijective_of_isPullback - Simplify φ definition and hsetY proof Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>

jjdishere · 2026-03-24T08:55:41Z

+        have : x ∈ T := (hSat z hxz) hxmem
+        exact hxT this


merge these in one line

- Inline single-use term-mode `have`s (hEq, hxy, hTcomp, hVT, hyCpt) - Fix `rw [show ... from ...]` → use named `have` instead - Merge consecutive single-use term-mode `have`s where possible Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>

Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>

jjdishere · 2026-03-24T09:39:21Z

 theorem isClosed_and_iUnion_connectedComponent_eq_iff {T : Set X} :
    (IsClosed T ∧ ∃ I : Set X, ⋃ x ∈ I, connectedComponent x = T) ↔
    ∃ J : Set ({U : Set X // IsClopen U}), ⋂ (U : J), U = T := by
+  classical


is this needed?

jjdishere · 2026-03-24T09:40:03Z

+    let J : Set ({U : Set X // IsClopen U}) := {U | T ⊆ U}
+    refine ⟨J, ?_⟩
+    refine Set.Subset.antisymm ?_ ?_


Suggested change

let J : Set ({U : Set X // IsClopen U}) := {U | T ⊆ U}

refine ⟨J, ?_⟩

refine Set.Subset.antisymm ?_ ?_

refine ⟨{U | T ⊆ U}, Set.Subset.antisymm ?_ ?_⟩

jjdishere · 2026-03-24T09:41:04Z

-        · exact hx
-        · exact mem_connectedComponent
+      by_contra hxT
+      have hSat : ∀ z, z ∈ T → connectedComponent z ⊆ T := by


This should be separated as a lemma

jjdishere · 2026-03-24T09:44:45Z

+        rw [(connectedComponent_eq hzw).symm]
+        intro u hu
+        simpa [hI] using (Set.mem_iUnion₂.mpr ⟨w, hwI, hu⟩ : u ∈ ⋃ x ∈ I, connectedComponent x)
+      have hdis : Disjoint (connectedComponent x) T := by


This should be separated as a lemma

jjdishere · 2026-03-24T09:46:55Z

+      let K : Type u := {U : Set X // IsClopen U ∧ x ∈ U}
+      have hInter : (⋂ U : K, (U : Set X)) = connectedComponent x :=


This could also be a lemma

jjdishere · 2026-03-24T09:54:02Z

+      have hcover : T ⊆ ⋃ U : K, (U : Set X)ᶜ := by
+        intro z hz
+        have hznot : z ∉ connectedComponent x := by
+          intro hz'
+          exact (Set.disjoint_left.mp hdis) hz' hz
+        have : z ∉ ⋂ U : K, (U : Set X) := by rwa [hInter]
+        simp only [Set.mem_iInter, not_forall] at this
+        exact Set.mem_iUnion.mpr this


instead of using have ... exact, you should use apply without using have.

jjdishere · 2026-03-24T09:54:31Z

+      obtain ⟨s, hs⟩ :=
+        hT.isCompact.elim_finite_subcover
+          (U := fun U : K => (U : Set X)ᶜ)
+          (fun U => U.2.1.1.isOpen_compl) hcover


these does not need to take 4 lines

jjdishere · 2026-03-24T09:57:14Z

+    · have : IsClosed (⋂ U : J, (U : Set X)) := isClosed_iInter fun U => (U.1.2).1
+      simpa [hJ] using this


have a term proof, merge into one line

jjdishere · 2026-03-24T09:58:05Z

+    · refine ⟨T, ?_⟩
+      refine Set.Subset.antisymm ?_ ?_
+      · intro z hz


refine ⟨T, Set.Subset.antisymm (fun z hz \maspto ?) (fun z hz \maspto ?)⟩

- Extract connectedComponent_subset_of_iUnion_eq and disjoint_connectedComponent_of_not_mem as standalone lemmas - Inline let J, merge consecutive refine calls - Remove unnecessary classical - Shorten hVcl, use apply instead of have...exact - Merge refine ⟨T, ?_⟩ + refine Set.Subset.antisymm into one refine - Inline hzInter as term-mode Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>

jjdishere

Second review pass (full style checklist)

Going through every item in the style/naming/quality checklist.

Issues found

1. by alone on its own line (L215-216)

    [PrespectralSpace X] : T2Space (ConnectedComponents X) :=
  by

Should be ... := by on one line.

2. Double space (L214)

instance t2Space_connectedComponent {X : Type u} [TopologicalSpace X]  [CompactSpace X]

Extra space before [CompactSpace X].

3. Lines exceeding 100 characters

L148 (101 chars): simpa [hI] using (Set.mem_iUnion₂.mpr ⟨w, hwI, hu⟩ : ...)
L231 (103 chars): comment -- Use compactness of ...
L422 (161 chars): (isHomeomorph_iff_continuous_bijective ...).mpr ⟨...⟩

4. show ... by ... inside simp (L398)

simp [fiberP, this, show (p : T × X).fst = t by simpa [FSt] using hp]

This is effectively the banned show ... from pattern. Extract as a named have.

Items that pass

No λ, no semicolons, no change, no open Classical, no show ... from in rw
No haveI, no unused let bindings, no unnecessary type annotations
Naming conventions followed (snake_case for propositions, UpperCamelCase for types)
Docstrings present on new helper lemmas
No sorry, no axiom, no set_option maxHeartbeats
Helper lemmas use weakest hypotheses (with omit for section vars)
No duplicate declarations

AI progress

cee7906

jjdishere commented Mar 24, 2026

View reviewed changes

jjdishere and others added 2 commits March 24, 2026 17:18

refactor: merge have + simpa into rw + direct proof in hSat

9e73682

Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>

jjdishere commented Mar 24, 2026

View reviewed changes

		let K : Type u := {U : Set X // IsClopen U ∧ x ∈ U}
		have hInter : (⋂ U : K, (U : Set X)) = connectedComponent x :=

		· have : IsClosed (⋂ U : J, (U : Set X)) := isClosed_iInter fun U => (U.1.2).1
		simpa [hJ] using this

Conversation

jjdishere commented Mar 24, 2026

Uh oh!

jjdishere left a comment

Choose a reason for hiding this comment

Review of feat(ConnectedComponents): new proofs

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

jjdishere left a comment

Choose a reason for hiding this comment

Second review pass (full style checklist)

Issues found

Items that pass

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant