chore(category_theory/comma): removed obviously tactic for data fields (

#18440)

For some `comma` categories like `structured_arrow`, `over`, `under`, the definition of some data fields could be obtained automatically by the obviously tactic. This PR removes this behaviour. Instead, specialized constructors like `structured_arrow.mk` or `structured_arrow.hom_mk` are used more systematically.

counterexamples/pseudoelement.lean

@@ -37,17 +37,11 @@ namespace category_theory.abelian.pseudoelement
 
 /-- `x` is given by `t ↦ (t, 2 * t)`. -/
 def x : over ((of ℤ ℚ) ⊞ (of ℤ ℚ)) :=
-begin
-  constructor,
-  exact biprod.lift (of_hom id) (of_hom (2 * id)),
-end
+over.mk (biprod.lift (of_hom id) (of_hom (2 * id)))
 
 /-- `y` is given by `t ↦ (t, t)`. -/
 def y : over ((of ℤ ℚ) ⊞ (of ℤ ℚ)) :=
-begin
-  constructor,
-  exact biprod.lift (of_hom id) (of_hom id),
-end
+over.mk (biprod.lift (of_hom id) (of_hom id))
 
 /-- `biprod.fst ≫ x` is pseudoequal to `biprod.fst y`. -/
 lemma fst_x_pseudo_eq_fst_y : pseudo_equal _ (app biprod.fst x) (app biprod.fst y) :=

src/category_theory/adjunction/comma.lean

@@ -53,7 +53,7 @@ def left_adjoint_of_structured_arrow_initials_aux (A : C) (B : D) :
   end,
   right_inv := λ f,
   begin
-    let B' : structured_arrow A G := { right := B, hom := f },
+    let B' : structured_arrow A G := structured_arrow.mk f,
     apply (comma_morphism.w (initial.to B')).symm.trans (category.id_comp _),
   end }
 

src/category_theory/comma.lean

@@ -58,8 +58,8 @@ variables {T : Type u₃} [category.{v₃} T]
 /-- The objects of the comma category are triples of an object `left : A`, an object
    `right : B` and a morphism `hom : L.obj left ⟶ R.obj right`.  -/
 structure comma (L : A ⥤ T) (R : B ⥤ T) : Type (max u₁ u₂ v₃) :=
-(left : A . obviously)
-(right : B . obviously)
+(left : A)
+(right : B)
 (hom : L.obj left ⟶ R.obj right)
 
 -- Satisfying the inhabited linter
@@ -75,8 +75,8 @@ variables {L : A ⥤ T} {R : B ⥤ T}
     morphisms coming from the two objects using morphisms in the image of the functors `L` and `R`.
 -/
 @[ext] structure comma_morphism (X Y : comma L R) :=
-(left : X.left ⟶ Y.left . obviously)
-(right : X.right ⟶ Y.right . obviously)
+(left : X.left ⟶ Y.left)
+(right : X.right ⟶ Y.right)
 (w' : L.map left ≫ Y.hom = X.hom ≫ R.map right . obviously)
 
 -- Satisfying the inhabited linter

src/category_theory/elements.lean

@@ -120,7 +120,7 @@ def structured_arrow_equivalence : F.elements ≌ structured_arrow punit F :=
 equivalence.mk (to_structured_arrow F) (from_structured_arrow F)
   (nat_iso.of_components (λ X, eq_to_iso (by tidy)) (by tidy))
   (nat_iso.of_components
-    (λ X, { hom := { right := 𝟙 _ }, inv := { right := 𝟙 _ } })
+    (λ X, structured_arrow.iso_mk (iso.refl _) (by tidy))
     (by tidy))
 
 open opposite

src/category_theory/limits/final.lean

@@ -173,7 +173,7 @@ def induction {d : D} (Z : Π (X : C) (k : d ⟶ F.obj X), Sort*)
 begin
   apply nonempty.some,
   apply @is_preconnected_induction _ _ _
-    (λ (Y : structured_arrow d F), Z Y.right Y.hom) _ _ { right := X₀, hom := k₀, } z,
+    (λ (Y : structured_arrow d F), Z Y.right Y.hom) _ _ (structured_arrow.mk k₀) z,
   { intros j₁ j₂ f a, fapply h₁ _ _ _ _ f.right _ a, convert f.w.symm, dsimp, simp, },
   { intros j₁ j₂ f a, fapply h₂ _ _ _ _ f.right _ a, convert f.w.symm, dsimp, simp, },
 end
@@ -351,7 +351,7 @@ begin
     fconstructor,
     swap 2, fconstructor,
     left, fsplit,
-    exact { right := f, } },
+    exact structured_arrow.hom_mk f (by tidy), },
   case eqv_gen.refl
   { fconstructor, },
   case eqv_gen.symm : x y h ih
@@ -426,7 +426,7 @@ def induction {d : D} (Z : Π (X : C) (k : F.obj X ⟶ d), Sort*)
 begin
   apply nonempty.some,
   apply @is_preconnected_induction _ _ _
-    (λ Y : costructured_arrow F d, Z Y.left Y.hom) _ _ { left := X₀, hom := k₀ } z,
+    (λ Y : costructured_arrow F d, Z Y.left Y.hom) _ _ (costructured_arrow.mk k₀) z,
   { intros j₁ j₂ f a, fapply h₁ _ _ _ _ f.left _ a, convert f.w, dsimp, simp, },
   { intros j₁ j₂ f a, fapply h₂ _ _ _ _ f.left _ a, convert f.w, dsimp, simp, },
 end

src/category_theory/over.lean

@@ -40,6 +40,7 @@ def over (X : T) := costructured_arrow (𝟭 T) X
 instance over.inhabited [inhabited T] : inhabited (over (default : T)) :=
 { default :=
   { left := default,
+    right := default,
     hom := 𝟙 _ } }
 
 namespace over
@@ -222,9 +223,7 @@ variables {D : Type u₂} [category.{v₂} D]
 @[simps]
 def post (F : T ⥤ D) : over X ⥤ over (F.obj X) :=
 { obj := λ Y, mk $ F.map Y.hom,
-  map := λ Y₁ Y₂ f,
-  { left := F.map f.left,
-    w' := by tidy; erw [← F.map_comp, w] } }
+  map := λ Y₁ Y₂ f, over.hom_mk (F.map f.left) (by tidy; erw [← F.map_comp, w]) }
 
 end
 
@@ -238,7 +237,8 @@ def under (X : T) := structured_arrow X (𝟭 T)
 -- Satisfying the inhabited linter
 instance under.inhabited [inhabited T] : inhabited (under (default : T)) :=
 { default :=
-  { right := default,
+  { left := default,
+    right := default,
     hom := 𝟙 _ } }
 
 namespace under
@@ -369,9 +369,7 @@ variables {D : Type u₂} [category.{v₂} D]
 @[simps]
 def post {X : T} (F : T ⥤ D) : under X ⥤ under (F.obj X) :=
 { obj := λ Y, mk $ F.map Y.hom,
-  map := λ Y₁ Y₂ f,
-  { right := F.map f.right,
-    w' := by tidy; erw [← F.map_comp, w] } }
+  map := λ Y₁ Y₂ f, under.hom_mk (F.map f.right) (by tidy; erw [← F.map_comp, w]), }
 
 end
 

src/category_theory/structured_arrow.lean

@@ -69,7 +69,7 @@ structured arrow given by `(X ⟶ F(U)) ⟶ (X ⟶ F(U) ⟶ F(Y))`.
 -/
 def hom_mk' {F : C ⥤ D} {X : D} {Y : C}
 (U : structured_arrow X F) (f : U.right ⟶ Y) :
-U ⟶ mk (U.hom ≫ F.map f) := { right := f }
+U ⟶ mk (U.hom ≫ F.map f) := { left := eq_to_hom (by ext), right := f }
 
 /--
 To construct an isomorphism of structured arrows,
@@ -165,9 +165,9 @@ comma.pre_right _ F G
 /-- The functor `(S, F) ⥤ (G(S), F ⋙ G)`. -/
 @[simps] def post (S : C) (F : B ⥤ C) (G : C ⥤ D) :
   structured_arrow S F ⥤ structured_arrow (G.obj S) (F ⋙ G) :=
-{ obj := λ X, { right := X.right, hom := G.map X.hom },
-  map := λ X Y f, { right := f.right, w' :=
-    by { simp [functor.comp_map, ←G.map_comp, ← f.w] } } }
+{ obj := λ X, structured_arrow.mk (G.map X.hom),
+  map := λ X Y f, structured_arrow.hom_mk f.right
+    (by simp [functor.comp_map, ←G.map_comp, ← f.w]) }
 
 instance small_proj_preimage_of_locally_small {𝒢 : set C} [small.{v₁} 𝒢] [locally_small.{v₁} D] :
   small.{v₁} ((proj S T).obj ⁻¹' 𝒢) :=
@@ -315,9 +315,9 @@ comma.pre_left F G _
 /-- The functor `(F, S) ⥤ (F ⋙ G, G(S))`. -/
 @[simps] def post (F : B ⥤ C) (G : C ⥤ D) (S : C) :
   costructured_arrow F S ⥤ costructured_arrow (F ⋙ G) (G.obj S) :=
-{ obj := λ X, { left := X.left, hom := G.map X.hom },
-  map := λ X Y f, { left := f.left, w' :=
-    by { simp [functor.comp_map, ←G.map_comp, ← f.w] } } }
+{ obj := λ X, costructured_arrow.mk (G.map X.hom),
+  map := λ X Y f, costructured_arrow.hom_mk f.left
+    (by simp [functor.comp_map, ←G.map_comp, ← f.w]), }
 
 instance small_proj_preimage_of_locally_small {𝒢 : set C} [small.{v₁} 𝒢] [locally_small.{v₁} D] :
   small.{v₁} ((proj S T).obj ⁻¹' 𝒢) :=

src/topology/sheaves/presheaf.lean

@@ -241,10 +241,10 @@ def pullback_map {X Y : Top.{v}} (f : X ⟶ Y) {ℱ 𝒢 : Y.presheaf C} (α : 
 def pullback_obj_obj_of_image_open {X Y : Top.{v}} (f : X ⟶ Y) (ℱ : Y.presheaf C) (U : opens X)
   (H : is_open (f '' U)) : (pullback_obj f ℱ).obj (op U) ≅ ℱ.obj (op ⟨_, H⟩) :=
 begin
-  let x : costructured_arrow (opens.map f).op (op U) :=
-  { left := op ⟨f '' U, H⟩,
-    hom := ((@hom_of_le _ _ _ ((opens.map f).obj ⟨_, H⟩) (set.image_preimage.le_u_l _)).op :
-    op ((opens.map f).obj (⟨⇑f '' ↑U, H⟩)) ⟶ op U) },
+  let x : costructured_arrow (opens.map f).op (op U) := begin
+    refine @costructured_arrow.mk _ _ _ _ _ (op (opens.mk (f '' U) H)) _ _,
+    exact ((@hom_of_le _ _ _ ((opens.map f).obj ⟨_, H⟩) (set.image_preimage.le_u_l _)).op),
+  end,
   have hx : is_terminal x :=
   { lift := λ s,
     begin

src/topology/sheaves/sheaf_condition/pairwise_intersections.lean

@@ -113,7 +113,7 @@ def pairwise_to_opens_le_cover : pairwise ι ⥤ opens_le_cover U :=
 
 instance (V : opens_le_cover U) :
   nonempty (structured_arrow V (pairwise_to_opens_le_cover U)) :=
-⟨{ right := single (V.index), hom := V.hom_to_index }⟩
+⟨@structured_arrow.mk _ _ _ _ _ (single (V.index)) _ (by exact V.hom_to_index)⟩
 
 /--
 The diagram consisting of the `U i` and `U i ⊓ U j` is cofinal in the diagram