chore: tidy various files (#3584)

Author: Ruben-VandeVelde

Mathlib/Algebra/Algebra/Equiv.lean

@@ -296,9 +296,9 @@ instance : Inhabited (A₁ ≃ₐ[R] A₁) :=
   ⟨refl⟩
 
 @[simp]
-theorem refl_to_algHom : ↑(refl : A₁ ≃ₐ[R] A₁) = AlgHom.id R A₁ :=
+theorem refl_toAlgHom : ↑(refl : A₁ ≃ₐ[R] A₁) = AlgHom.id R A₁ :=
   rfl
-#align alg_equiv.refl_to_alg_hom AlgEquiv.refl_to_algHom
+#align alg_equiv.refl_to_alg_hom AlgEquiv.refl_toAlgHom
 
 @[simp]
 theorem coe_refl : ⇑(refl : A₁ ≃ₐ[R] A₁) = id :=
@@ -309,8 +309,7 @@ theorem coe_refl : ⇑(refl : A₁ ≃ₐ[R] A₁) = id :=
 @[symm]
 def symm (e : A₁ ≃ₐ[R] A₂) : A₂ ≃ₐ[R] A₁ :=
   { e.toRingEquiv.symm with
-    commutes' := fun r =>
-      by
+    commutes' := fun r => by
       rw [← e.toRingEquiv.symm_apply_apply (algebraMap R A₁ r)]
       congr
       change _ = e _
@@ -376,14 +375,14 @@ theorem refl_symm : (AlgEquiv.refl : A₁ ≃ₐ[R] A₁).symm = AlgEquiv.refl :
 #align alg_equiv.refl_symm AlgEquiv.refl_symm
 
 --this should be a simp lemma but causes a lint timeout
-theorem to_ringEquiv_symm (f : A₁ ≃ₐ[R] A₁) : (f : A₁ ≃+* A₁).symm = f.symm :=
+theorem toRingEquiv_symm (f : A₁ ≃ₐ[R] A₁) : (f : A₁ ≃+* A₁).symm = f.symm :=
   rfl
-#align alg_equiv.to_ring_equiv_symm AlgEquiv.to_ringEquiv_symm
+#align alg_equiv.to_ring_equiv_symm AlgEquiv.toRingEquiv_symm
 
 @[simp]
-theorem symm_to_ringEquiv : (e.symm : A₂ ≃+* A₁) = (e : A₁ ≃+* A₂).symm :=
+theorem symm_toRingEquiv : (e.symm : A₂ ≃+* A₁) = (e : A₁ ≃+* A₂).symm :=
   rfl
-#align alg_equiv.symm_to_ring_equiv AlgEquiv.symm_to_ringEquiv
+#align alg_equiv.symm_to_ring_equiv AlgEquiv.symm_toRingEquiv
 
 /-- Algebra equivalences are transitive. -/
 @[trans]
@@ -571,9 +570,9 @@ def toLinearMap : A₁ →ₗ[R] A₂ :=
 #align alg_equiv.to_linear_map AlgEquiv.toLinearMap
 
 @[simp]
-theorem to_algHom_toLinearMap : (e : A₁ →ₐ[R] A₂).toLinearMap = e.toLinearMap :=
+theorem toAlgHom_toLinearMap : (e : A₁ →ₐ[R] A₂).toLinearMap = e.toLinearMap :=
   rfl
-#align alg_equiv.to_alg_hom_to_linear_map AlgEquiv.to_algHom_toLinearMap
+#align alg_equiv.to_alg_hom_to_linear_map AlgEquiv.toAlgHom_toLinearMap
 
 @[simp]
 theorem toLinearEquiv_toLinearMap : e.toLinearEquiv.toLinearMap = e.toLinearMap :=
@@ -679,8 +678,7 @@ theorem mul_apply (e₁ e₂ : A₁ ≃ₐ[R] A₁) (x : A₁) : (e₁ * e₂) x
 
 /-- An algebra isomorphism induces a group isomorphism between automorphism groups -/
 @[simps apply]
-def autCongr (ϕ : A₁ ≃ₐ[R] A₂) : (A₁ ≃ₐ[R] A₁) ≃* A₂ ≃ₐ[R] A₂
-    where
+def autCongr (ϕ : A₁ ≃ₐ[R] A₂) : (A₁ ≃ₐ[R] A₁) ≃* A₂ ≃ₐ[R] A₂ where
   toFun ψ := ϕ.symm.trans (ψ.trans ϕ)
   invFun ψ := ϕ.trans (ψ.trans ϕ.symm)
   left_inv ψ := by
@@ -713,9 +711,8 @@ theorem autCongr_trans (ϕ : A₁ ≃ₐ[R] A₂) (ψ : A₂ ≃ₐ[R] A₃) :
 
 /-- The tautological action by `A₁ ≃ₐ[R] A₁` on `A₁`.
 
-This generalizes `function.End.apply_mul_action`. -/
-instance applyMulSemiringAction : MulSemiringAction (A₁ ≃ₐ[R] A₁) A₁
-    where
+This generalizes `Function.End.applyMulAction`. -/
+instance applyMulSemiringAction : MulSemiringAction (A₁ ≃ₐ[R] A₁) A₁ where
   smul := (· <| ·)
   smul_zero := AlgEquiv.map_zero
   smul_add := AlgEquiv.map_add

Mathlib/CategoryTheory/Filtered.lean

@@ -103,8 +103,7 @@ instance (priority := 100) isFiltered_of_semilatticeSup_nonempty (α : Type u) [
 #align category_theory.is_filtered_of_semilattice_sup_nonempty CategoryTheory.isFiltered_of_semilatticeSup_nonempty
 
 instance (priority := 100) isFilteredOrEmpty_of_directed_le (α : Type u) [Preorder α]
-    [IsDirected α (· ≤ ·)] : IsFilteredOrEmpty α
-    where
+    [IsDirected α (· ≤ ·)] : IsFilteredOrEmpty α where
   cocone_objs X Y :=
     let ⟨Z, h1, h2⟩ := exists_ge_ge X Y
     ⟨Z, homOfLE h1, homOfLE h2, trivial⟩
@@ -154,41 +153,41 @@ noncomputable def max (j j' : C) : C :=
   (IsFilteredOrEmpty.cocone_objs j j').choose
 #align category_theory.is_filtered.max CategoryTheory.IsFiltered.max
 
-/-- `left_to_max j j'` is an arbitrary choice of morphism from `j` to `max j j'`,
-whose existence is ensured by `is_filtered`.
+/-- `leftToMax j j'` is an arbitrary choice of morphism from `j` to `max j j'`,
+whose existence is ensured by `IsFiltered`.
 -/
 noncomputable def leftToMax (j j' : C) : j ⟶ max j j' :=
   (IsFilteredOrEmpty.cocone_objs j j').choose_spec.choose
 #align category_theory.is_filtered.left_to_max CategoryTheory.IsFiltered.leftToMax
 
-/-- `right_to_max j j'` is an arbitrary choice of morphism from `j'` to `max j j'`,
-whose existence is ensured by `is_filtered`.
+/-- `rightToMax j j'` is an arbitrary choice of morphism from `j'` to `max j j'`,
+whose existence is ensured by `IsFiltered`.
 -/
 noncomputable def rightToMax (j j' : C) : j' ⟶ max j j' :=
   (IsFilteredOrEmpty.cocone_objs j j').choose_spec.choose_spec.choose
 #align category_theory.is_filtered.right_to_max CategoryTheory.IsFiltered.rightToMax
 
 /-- `coeq f f'`, for morphisms `f f' : j ⟶ j'`, is an arbitrary choice of object
-which admits a morphism `coeq_hom f f' : j' ⟶ coeq f f'` such that
-`coeq_condition : f ≫ coeq_hom f f' = f' ≫ coeq_hom f f'`.
-Its existence is ensured by `is_filtered`.
+which admits a morphism `coeqHom f f' : j' ⟶ coeq f f'` such that
+`coeq_condition : f ≫ coeqHom f f' = f' ≫ coeqHom f f'`.
+Its existence is ensured by `IsFiltered`.
 -/
 noncomputable def coeq {j j' : C} (f f' : j ⟶ j') : C :=
   (IsFilteredOrEmpty.cocone_maps f f').choose
 #align category_theory.is_filtered.coeq CategoryTheory.IsFiltered.coeq
 
-/-- `coeq_hom f f'`, for morphisms `f f' : j ⟶ j'`, is an arbitrary choice of morphism
-`coeq_hom f f' : j' ⟶ coeq f f'` such that
-`coeq_condition : f ≫ coeq_hom f f' = f' ≫ coeq_hom f f'`.
-Its existence is ensured by `is_filtered`.
+/-- `coeqHom f f'`, for morphisms `f f' : j ⟶ j'`, is an arbitrary choice of morphism
+`coeqHom f f' : j' ⟶ coeq f f'` such that
+`coeq_condition : f ≫ coeqHom f f' = f' ≫ coeqHom f f'`.
+Its existence is ensured by `IsFiltered`.
 -/
 noncomputable def coeqHom {j j' : C} (f f' : j ⟶ j') : j' ⟶ coeq f f' :=
   (IsFilteredOrEmpty.cocone_maps f f').choose_spec.choose
 #align category_theory.is_filtered.coeq_hom CategoryTheory.IsFiltered.coeqHom
 
 -- porting note: the simp tag has been removed as the linter complained
 /-- `coeq_condition f f'`, for morphisms `f f' : j ⟶ j'`, is the proof that
-`f ≫ coeq_hom f f' = f' ≫ coeq_hom f f'`.
+`f ≫ coeqHom f f' = f' ≫ coeqHom f f'`.
 -/
 @[reassoc]
 theorem coeq_condition {j j' : C} (f f' : j ⟶ j') : f ≫ coeqHom f f' = f' ≫ coeqHom f f' :=
@@ -280,7 +279,7 @@ theorem toSup_commutes {X Y : C} (mX : X ∈ O) (mY : Y ∈ O) {f : X ⟶ Y}
 
 variable {J : Type v} [SmallCategory J] [FinCategory J]
 
-/-- If we have `is_filtered C`, then for any functor `F : J ⥤ C` with `fin_category J`,
+/-- If we have `IsFiltered C`, then for any functor `F : J ⥤ C` with `FinCategory J`,
 there exists a cocone over `F`.
 -/
 theorem cocone_nonempty (F : J ⥤ C) : _root_.Nonempty (Cocone F) := by
@@ -301,7 +300,7 @@ theorem cocone_nonempty (F : J ⥤ C) : _root_.Nonempty (Cocone F) := by
   exact ⟨j, rfl, j', g, by simp⟩
 #align category_theory.is_filtered.cocone_nonempty CategoryTheory.IsFiltered.cocone_nonempty
 
-/-- An arbitrary choice of cocone over `F : J ⥤ C`, for `fin_category J` and `is_filtered C`.
+/-- An arbitrary choice of cocone over `F : J ⥤ C`, for `FinCategory J` and `IsFiltered C`.
 -/
 noncomputable def cocone (F : J ⥤ C) : Cocone F :=
   (cocone_nonempty F).some
@@ -338,46 +337,46 @@ variable {C}
 variable [IsFilteredOrEmpty C]
 
 /-- `max₃ j₁ j₂ j₃` is an arbitrary choice of object to the right of `j₁`, `j₂` and `j₃`,
-whose existence is ensured by `is_filtered`.
+whose existence is ensured by `IsFiltered`.
 -/
 noncomputable def max₃ (j₁ j₂ j₃ : C) : C :=
   max (max j₁ j₂) j₃
 #align category_theory.is_filtered.max₃ CategoryTheory.IsFiltered.max₃
 
-/-- `first_to_max₃ j₁ j₂ j₃` is an arbitrary choice of morphism from `j₁` to `max₃ j₁ j₂ j₃`,
-whose existence is ensured by `is_filtered`.
+/-- `firstToMax₃ j₁ j₂ j₃` is an arbitrary choice of morphism from `j₁` to `max₃ j₁ j₂ j₃`,
+whose existence is ensured by `IsFiltered`.
 -/
 noncomputable def firstToMax₃ (j₁ j₂ j₃ : C) : j₁ ⟶ max₃ j₁ j₂ j₃ :=
   leftToMax j₁ j₂ ≫ leftToMax (max j₁ j₂) j₃
 #align category_theory.is_filtered.first_to_max₃ CategoryTheory.IsFiltered.firstToMax₃
 
-/-- `second_to_max₃ j₁ j₂ j₃` is an arbitrary choice of morphism from `j₂` to `max₃ j₁ j₂ j₃`,
-whose existence is ensured by `is_filtered`.
+/-- `secondToMax₃ j₁ j₂ j₃` is an arbitrary choice of morphism from `j₂` to `max₃ j₁ j₂ j₃`,
+whose existence is ensured by `IsFiltered`.
 -/
 noncomputable def secondToMax₃ (j₁ j₂ j₃ : C) : j₂ ⟶ max₃ j₁ j₂ j₃ :=
   rightToMax j₁ j₂ ≫ leftToMax (max j₁ j₂) j₃
 #align category_theory.is_filtered.second_to_max₃ CategoryTheory.IsFiltered.secondToMax₃
 
-/-- `third_to_max₃ j₁ j₂ j₃` is an arbitrary choice of morphism from `j₃` to `max₃ j₁ j₂ j₃`,
-whose existence is ensured by `is_filtered`.
+/-- `thirdToMax₃ j₁ j₂ j₃` is an arbitrary choice of morphism from `j₃` to `max₃ j₁ j₂ j₃`,
+whose existence is ensured by `IsFiltered`.
 -/
 noncomputable def thirdToMax₃ (j₁ j₂ j₃ : C) : j₃ ⟶ max₃ j₁ j₂ j₃ :=
   rightToMax (max j₁ j₂) j₃
 #align category_theory.is_filtered.third_to_max₃ CategoryTheory.IsFiltered.thirdToMax₃
 
 /-- `coeq₃ f g h`, for morphisms `f g h : j₁ ⟶ j₂`, is an arbitrary choice of object
-which admits a morphism `coeq₃_hom f g h : j₂ ⟶ coeq₃ f g h` such that
+which admits a morphism `coeq₃Hom f g h : j₂ ⟶ coeq₃ f g h` such that
 `coeq₃_condition₁`, `coeq₃_condition₂` and `coeq₃_condition₃` are satisfied.
-Its existence is ensured by `is_filtered`.
+Its existence is ensured by `IsFiltered`.
 -/
 noncomputable def coeq₃ {j₁ j₂ : C} (f g h : j₁ ⟶ j₂) : C :=
   coeq (coeqHom f g ≫ leftToMax (coeq f g) (coeq g h))
     (coeqHom g h ≫ rightToMax (coeq f g) (coeq g h))
 #align category_theory.is_filtered.coeq₃ CategoryTheory.IsFiltered.coeq₃
 
-/-- `coeq₃_hom f g h`, for morphisms `f g h : j₁ ⟶ j₂`, is an arbitrary choice of morphism
+/-- `coeq₃Hom f g h`, for morphisms `f g h : j₁ ⟶ j₂`, is an arbitrary choice of morphism
 `j₂ ⟶ coeq₃ f g h` such that `coeq₃_condition₁`, `coeq₃_condition₂` and `coeq₃_condition₃`
-are satisfied. Its existence is ensured by `is_filtered`.
+are satisfied. Its existence is ensured by `IsFiltered`.
 -/
 noncomputable def coeq₃Hom {j₁ j₂ : C} (f g h : j₁ ⟶ j₂) : j₂ ⟶ coeq₃ f g h :=
   coeqHom f g ≫
@@ -464,7 +463,7 @@ end SpecialShapes
 
 end IsFiltered
 
-/-- A category `is_cofiltered_or_empty` if
+/-- A category `IsCofilteredOrEmpty` if
 1. for every pair of objects there exists another object "to the left", and
 2. for every pair of parallel morphisms there exists a morphism to the left so the compositions
    are equal.
@@ -477,7 +476,7 @@ class IsCofilteredOrEmpty : Prop where
   cone_maps : ∀ ⦃X Y : C⦄ (f g : X ⟶ Y), ∃ (W : _)(h : W ⟶ X), h ≫ f = h ≫ g
 #align category_theory.is_cofiltered_or_empty CategoryTheory.IsCofilteredOrEmpty
 
-/-- A category `is_cofiltered` if
+/-- A category `IsCofiltered` if
 1. for every pair of objects there exists another object "to the left",
 2. for every pair of parallel morphisms there exists a morphism to the left so the compositions
    are equal, and
@@ -491,8 +490,7 @@ class IsCofiltered extends IsCofilteredOrEmpty C : Prop where
 #align category_theory.is_cofiltered CategoryTheory.IsCofiltered
 
 instance (priority := 100) isCofilteredOrEmpty_of_semilatticeInf (α : Type u) [SemilatticeInf α] :
-    IsCofilteredOrEmpty α
-    where
+    IsCofilteredOrEmpty α where
   cone_objs X Y := ⟨X ⊓ Y, homOfLE inf_le_left, homOfLE inf_le_right, trivial⟩
   cone_maps X Y f g := ⟨X, 𝟙 _, by
     apply ULift.ext
@@ -504,8 +502,7 @@ instance (priority := 100) isCofiltered_of_semilatticeInf_nonempty (α : Type u)
 #align category_theory.is_cofiltered_of_semilattice_inf_nonempty CategoryTheory.isCofiltered_of_semilatticeInf_nonempty
 
 instance (priority := 100) isCofilteredOrEmpty_of_directed_ge (α : Type u) [Preorder α]
-    [IsDirected α (· ≥ ·)] : IsCofilteredOrEmpty α
-    where
+    [IsDirected α (· ≥ ·)] : IsCofilteredOrEmpty α where
   cone_objs X Y :=
     let ⟨Z, hX, hY⟩ := exists_le_le X Y
     ⟨Z, homOfLE hX, homOfLE hY, trivial⟩
@@ -523,8 +520,7 @@ example (α : Type u) [SemilatticeInf α] [OrderBot α] : IsCofiltered α := by
 
 example (α : Type u) [SemilatticeInf α] [OrderTop α] : IsCofiltered α := by infer_instance
 
-instance : IsCofiltered (Discrete PUnit)
-    where
+instance : IsCofiltered (Discrete PUnit) where
   cone_objs X Y := ⟨⟨PUnit.unit⟩, ⟨⟨by trivial⟩⟩, ⟨⟨Subsingleton.elim _ _⟩⟩, trivial⟩
   cone_maps X Y f g := ⟨⟨PUnit.unit⟩, ⟨⟨by trivial⟩⟩, by
     apply ULift.ext
@@ -550,47 +546,47 @@ variable [IsCofilteredOrEmpty C]
 --#align category_theory.is_cofiltered.cone_maps CategoryTheory.IsCofiltered.cone_maps
 
 /-- `min j j'` is an arbitrary choice of object to the left of both `j` and `j'`,
-whose existence is ensured by `is_cofiltered`.
+whose existence is ensured by `IsCofiltered`.
 -/
 noncomputable def min (j j' : C) : C :=
   (IsCofilteredOrEmpty.cone_objs j j').choose
 #align category_theory.is_cofiltered.min CategoryTheory.IsCofiltered.min
 
 /-- `min_to_left j j'` is an arbitrary choice of morphism from `min j j'` to `j`,
-whose existence is ensured by `is_cofiltered`.
+whose existence is ensured by `IsCofiltered`.
 -/
 noncomputable def minToLeft (j j' : C) : min j j' ⟶ j :=
   (IsCofilteredOrEmpty.cone_objs j j').choose_spec.choose
 #align category_theory.is_cofiltered.min_to_left CategoryTheory.IsCofiltered.minToLeft
 
 /-- `min_to_right j j'` is an arbitrary choice of morphism from `min j j'` to `j'`,
-whose existence is ensured by `is_cofiltered`.
+whose existence is ensured by `IsCofiltered`.
 -/
 noncomputable def minToRight (j j' : C) : min j j' ⟶ j' :=
   (IsCofilteredOrEmpty.cone_objs j j').choose_spec.choose_spec.choose
 #align category_theory.is_cofiltered.min_to_right CategoryTheory.IsCofiltered.minToRight
 
 /-- `eq f f'`, for morphisms `f f' : j ⟶ j'`, is an arbitrary choice of object
-which admits a morphism `eq_hom f f' : eq f f' ⟶ j` such that
-`eq_condition : eq_hom f f' ≫ f = eq_hom f f' ≫ f'`.
-Its existence is ensured by `is_cofiltered`.
+which admits a morphism `eqHom f f' : eq f f' ⟶ j` such that
+`eq_condition : eqHom f f' ≫ f = eqHom f f' ≫ f'`.
+Its existence is ensured by `IsCofiltered`.
 -/
 noncomputable def eq {j j' : C} (f f' : j ⟶ j') : C :=
   (IsCofilteredOrEmpty.cone_maps f f').choose
 #align category_theory.is_cofiltered.eq CategoryTheory.IsCofiltered.eq
 
-/-- `eq_hom f f'`, for morphisms `f f' : j ⟶ j'`, is an arbitrary choice of morphism
-`eq_hom f f' : eq f f' ⟶ j` such that
-`eq_condition : eq_hom f f' ≫ f = eq_hom f f' ≫ f'`.
-Its existence is ensured by `is_cofiltered`.
+/-- `eqHom f f'`, for morphisms `f f' : j ⟶ j'`, is an arbitrary choice of morphism
+`eqHom f f' : eq f f' ⟶ j` such that
+`eq_condition : eqHom f f' ≫ f = eqHom f f' ≫ f'`.
+Its existence is ensured by `IsCofiltered`.
 -/
 noncomputable def eqHom {j j' : C} (f f' : j ⟶ j') : eq f f' ⟶ j :=
   (IsCofilteredOrEmpty.cone_maps f f').choose_spec.choose
 #align category_theory.is_cofiltered.eq_hom CategoryTheory.IsCofiltered.eqHom
 
 -- porting note: the simp tag has been removed as the linter complained
 /-- `eq_condition f f'`, for morphisms `f f' : j ⟶ j'`, is the proof that
-`eq_hom f f' ≫ f = eq_hom f f' ≫ f'`.
+`eqHom f f' ≫ f = eqHom f f' ≫ f'`.
 -/
 @[reassoc]
 theorem eq_condition {j j' : C} (f f' : j ⟶ j') : eqHom f f' ≫ f = eqHom f f' ≫ f' :=
@@ -697,7 +693,7 @@ theorem infTo_commutes {X Y : C} (mX : X ∈ O) (mY : Y ∈ O) {f : X ⟶ Y}
 
 variable {J : Type w} [SmallCategory J] [FinCategory J]
 
-/-- If we have `is_cofiltered C`, then for any functor `F : J ⥤ C` with `fin_category J`,
+/-- If we have `IsCofiltered C`, then for any functor `F : J ⥤ C` with `FinCategory J`,
 there exists a cone over `F`.
 -/
 theorem cone_nonempty (F : J ⥤ C) : _root_.Nonempty (Cone F) := by
@@ -719,7 +715,7 @@ theorem cone_nonempty (F : J ⥤ C) : _root_.Nonempty (Cone F) := by
   exact ⟨j, rfl, j', g, by simp⟩
 #align category_theory.is_cofiltered.cone_nonempty CategoryTheory.IsCofiltered.cone_nonempty
 
-/-- An arbitrary choice of cone over `F : J ⥤ C`, for `fin_category J` and `is_cofiltered C`.
+/-- An arbitrary choice of cone over `F : J ⥤ C`, for `FinCategory J` and `IsCofiltered C`.
 -/
 noncomputable def cone (F : J ⥤ C) : Cone F :=
   (cone_nonempty F).some
@@ -758,28 +754,24 @@ section Opposite
 
 open Opposite
 
-instance isCofiltered_op_of_isFiltered [IsFiltered C] : IsCofiltered Cᵒᵖ
-    where
+instance isCofiltered_op_of_isFiltered [IsFiltered C] : IsCofiltered Cᵒᵖ where
   cone_objs X Y :=
     ⟨op (IsFiltered.max X.unop Y.unop), (IsFiltered.leftToMax _ _).op,
       (IsFiltered.rightToMax _ _).op, trivial⟩
   cone_maps X Y f g :=
-    ⟨op (IsFiltered.coeq f.unop g.unop), (IsFiltered.coeqHom _ _).op,
-      by
+    ⟨op (IsFiltered.coeq f.unop g.unop), (IsFiltered.coeqHom _ _).op, by
       rw [show f = f.unop.op by simp, show g = g.unop.op by simp, ← op_comp, ← op_comp]
       congr 1
       exact IsFiltered.coeq_condition f.unop g.unop⟩
   Nonempty := ⟨op IsFiltered.Nonempty.some⟩
 #align category_theory.is_cofiltered_op_of_is_filtered CategoryTheory.isCofiltered_op_of_isFiltered
 
-instance isFiltered_op_of_isCofiltered [IsCofiltered C] : IsFiltered Cᵒᵖ
-    where
+instance isFiltered_op_of_isCofiltered [IsCofiltered C] : IsFiltered Cᵒᵖ where
   cocone_objs X Y :=
     ⟨op (IsCofiltered.min X.unop Y.unop), (IsCofiltered.minToLeft X.unop Y.unop).op,
       (IsCofiltered.minToRight X.unop Y.unop).op, trivial⟩
   cocone_maps X Y f g :=
-    ⟨op (IsCofiltered.eq f.unop g.unop), (IsCofiltered.eqHom f.unop g.unop).op,
-      by
+    ⟨op (IsCofiltered.eq f.unop g.unop), (IsCofiltered.eqHom f.unop g.unop).op, by
       rw [show f = f.unop.op by simp, show g = g.unop.op by simp, ← op_comp, ← op_comp]
       congr 1
       exact IsCofiltered.eq_condition f.unop g.unop⟩