chore(CategoryTheory/Sites): golf some proofs in the coherent topology file (#9979)

Author: dagurtomas

Mathlib/CategoryTheory/Sites/Coherent/CoherentTopology.lean

@@ -21,29 +21,24 @@ namespace CategoryTheory
 
 variable {C : Type*} [Category C] [Precoherent C] {X : C}
 
-namespace coherentTopology
-
 /--
 For a precoherent category, any sieve that contains an `EffectiveEpiFamily` is a sieve of the
 coherent topology.
 Note: This is one direction of `mem_sieves_iff_hasEffectiveEpiFamily`, but is needed for the proof.
 -/
-theorem mem_sieves_of_hasEffectiveEpiFamily (S : Sieve X) :
+theorem coherentTopology.mem_sieves_of_hasEffectiveEpiFamily (S : Sieve X) :
     (∃ (α : Type) (_ : Fintype α) (Y : α → C) (π : (a : α) → (Y a ⟶ X)),
-        EffectiveEpiFamily Y π ∧ (∀ a : α, (S.arrows) (π a)) ) →
-          (S ∈ GrothendieckTopology.sieves (coherentTopology C) X) := by
-  rintro ⟨α, ⟨h, ⟨Y, ⟨π, hπ⟩⟩⟩⟩
-  have h_le : Sieve.generate (Presieve.ofArrows _ π) ≤ S := by
-    rw [Sieve.sets_iff_generate (Presieve.ofArrows _ π) S]
-    apply Presieve.le_of_factorsThru_sieve (Presieve.ofArrows (fun i => Y i) π) S _
-    intro W g f
-    use W, 𝟙 W
-    rcases f with ⟨i⟩
-    exact ⟨π i, ⟨hπ.2 i,Category.id_comp (π i) ⟩⟩
-  apply Coverage.saturate_of_superset (coherentCoverage C) h_le
-  exact Coverage.saturate.of X _ ⟨α, inferInstance, Y, π, ⟨rfl, hπ.1⟩⟩
-
-end coherentTopology
+      EffectiveEpiFamily Y π ∧ (∀ a : α, (S.arrows) (π a)) ) →
+        (S ∈ GrothendieckTopology.sieves (coherentTopology C) X) := by
+  intro ⟨α, _, Y, π, hπ⟩
+  refine Coverage.saturate_of_superset (coherentCoverage C) ?_
+    (Coverage.saturate.of X _ ⟨α, inferInstance, Y, π, rfl, hπ.1⟩)
+  rw [Sieve.sets_iff_generate]
+  apply Presieve.le_of_factorsThru_sieve (Presieve.ofArrows (fun i => Y i) π) S _
+  intro W g f
+  refine ⟨W, 𝟙 W, ?_⟩
+  rcases f with ⟨i⟩
+  exact ⟨π i, hπ.2 i, by simp⟩
 
 /--
 Effective epi families in a precoherent category are transitive, in the sense that an
@@ -63,12 +58,6 @@ theorem EffectiveEpiFamily.transitive_of_finite {α : Type} [Fintype α] {Y : α
     change Nonempty _
     rw [← Sieve.forallYonedaIsSheaf_iff_colimit]
     exact fun W => coherentTopology.isSheaf_yoneda_obj W _ h₂
-  let h' := h
-  rw [← Sieve.effectiveEpimorphic_family] at h'
-  let H' := H
-  conv at H' =>
-    intro a
-    rw [← Sieve.effectiveEpimorphic_family]
   -- Show that a covering sieve is a colimit, which implies the original set of arrows is regular
   -- epimorphic. We use the transitivity property of saturation
   apply Coverage.saturate.transitive X (Sieve.generate (Presieve.ofArrows Y π))
@@ -80,10 +69,8 @@ theorem EffectiveEpiFamily.transitive_of_finite {α : Type} [Fintype α] {Y : α
     apply coherentTopology.mem_sieves_of_hasEffectiveEpiFamily
     -- Need to show that the pullback of the family `π_n` to a given `Y i` is effective epimorphic
     rcases hY with ⟨i⟩
-    use β i, inferInstance, Y_n i, π_n i, H i
-    intro b
-    use Y_n i b, (𝟙 _), π_n i b ≫ π i, ⟨(⟨i, b⟩ : Σ (i : α), β i)⟩
-    exact Category.id_comp (π_n i b ≫ π i)
+    exact ⟨β i, inferInstance, Y_n i, π_n i, H i, fun b ↦
+      ⟨Y_n i b, (𝟙 _), π_n i b ≫ π i, ⟨(⟨i, b⟩ : Σ (i : α), β i)⟩, by simp⟩⟩
 
 /--
 A sieve belongs to the coherent topology if and only if it contains a finite
@@ -96,22 +83,16 @@ theorem coherentTopology.mem_sieves_iff_hasEffectiveEpiFamily (S : Sieve X) :
   constructor
   · intro h
     induction' h with Y T hS Y Y R S _ _ a b
-    · rcases hS with ⟨a, h, Y', π, h'⟩
-      use a, h, Y', π, by tauto
-      intro a'
+    · rcases hS with ⟨a, h, Y', π, h', _⟩
+      refine ⟨a, h, Y', π, inferInstance, fun a' ↦ ?_⟩
       rcases h' with ⟨rfl, _⟩
-      simp only [Sieve.generate_apply]
-      use Y' a', 𝟙 Y' a', π a', Presieve.ofArrows.mk a'
-      apply Category.id_comp
-    · use Unit, Unit.fintype, fun _ => Y, fun _ => (𝟙 Y)
-      cases' S with arrows downward_closed
-      exact ⟨inferInstance, by simp only [Sieve.top_apply, forall_const]⟩
+      exact ⟨Y' a', 𝟙 Y' a', π a', Presieve.ofArrows.mk a', by simp⟩
+    · exact ⟨Unit, Unit.fintype, fun _ => Y, fun _ => (𝟙 Y), inferInstance, by simp⟩
     · rcases a with ⟨α, w, Y₁, π, ⟨h₁,h₂⟩⟩
       choose β _ Y_n π_n H using fun a => b (h₂ a)
-      use (Σ a, β a), inferInstance, fun ⟨a,b⟩ => Y_n a b, fun ⟨a, b⟩ => (π_n a b) ≫ (π a)
-      constructor
-      · exact EffectiveEpiFamily.transitive_of_finite _ h₁ _ (fun a => (H a).1)
-      · exact fun c => (H c.fst).2 c.snd
+      exact ⟨(Σ a, β a), inferInstance, fun ⟨a,b⟩ => Y_n a b, fun ⟨a, b⟩ => (π_n a b) ≫ (π a),
+        EffectiveEpiFamily.transitive_of_finite _ h₁ _ (fun a => (H a).1),
+        fun c => (H c.fst).2 c.snd⟩
   · exact coherentTopology.mem_sieves_of_hasEffectiveEpiFamily S
 
 end CategoryTheory