golf

LeanCondensed/LightCondensed/SequentialLimit.lean

@@ -17,6 +17,9 @@ This file proves that a sequential limit of epimorhpisms is epimorphic in `Light
 In other words, given epis
 `⋯ ⟶ Sₙ₊₁ ⟶ Sₙ ⟶ ⋯ ⟶ S₀`,
 the projection map `lim Sₙ ⟶ S₀` is surjective.
+
+This should be generalised to light condensed objects in concrete categories for which
+`epi_iff_locallySurjective` holds.
 -/
 
 open CategoryTheory Limits

LeanCondensed/LightCondensed/Yoneda.lean

@@ -9,7 +9,8 @@ open CategoryTheory
 
 namespace LightCondensed
 
-variable (R : Type _) [Ring R] -- might need some more assumptions
+-- This should be done for all concrete categories with a left adjoint to types.
+variable (R : Type _) [Ring R]
 
 @[simps! apply]
 def yoneda (S : LightProfinite.{u}) (A : LightCondSet) :

LeanCondensed/Projects/AB.lean

@@ -154,9 +154,7 @@ lemma abStar_iff_preserves_epi [HasLimitsOfShape I A] :
       apply left_exact_of_left_exact
       exact fun i ↦ ⟨(hh i).mono_f, (hh i).1⟩
     · exact h _ hh
-  · intro h F hh
-    have := h F hh
-    exact this.epi_g
+  · exact fun h F hh ↦ (h F hh).epi_g
 
 lemma ab_iff_preserves_mono [HasColimitsOfShape I A] :
     ((∀ (F : I ⥤ ShortComplex A),
@@ -166,16 +164,13 @@ lemma ab_iff_preserves_mono [HasColimitsOfShape I A] :
   constructor
   · intro h F hh
     have := ShortExact.mk' (S := (colimitCocone F).pt)
-    rw [Imp.swap (a := Mono (colimitCocone F).pt.f) ] at this
-    rw [← and_imp] at this
+    rw [Imp.swap (a := Mono (colimitCocone F).pt.f), ← and_imp] at this
     apply this
     · rw [and_comm]
       apply right_exact_of_right_exact
       exact fun i ↦ ⟨(hh i).epi_g, (hh i).1⟩
     · exact h _ hh
-  · intro h F hh
-    have := h F hh
-    exact this.mono_f
+  · exact fun h F hh ↦ (h F hh).mono_f
 
 lemma finite_abStar (I : Type) [Finite I] : HasExactLimitsOfShape (Discrete I) A := by sorry