chore(CategoryTheory/FiberedCategory/HomLift): Unify IsHomLift and IsHomLiftAux (#31125)

The definition `IsHomLiftAux` is not necessary, as inductives can be classes themselves. (see for example `Decidable`).
This PR makes `Functor.IsHomLift` itself an inductive, taking out the middle man.

Co-authored-by: Edward van de Meent <edwardvdmeent@gmail.com>

Author: edegeltje

Mathlib/CategoryTheory/FiberedCategory/Cartesian.lean

@@ -54,9 +54,11 @@ morphisms `φ' : a' ⟶ b`, also lying over `f`, there exists a unique morphism
 `𝟙 R` such that `φ' = χ ≫ φ`.
 
 See SGA 1 VI 5.1. -/
-class IsCartesian : Prop extends IsHomLift p f φ where
+class IsCartesian : Prop where
+  [toIsHomLift : IsHomLift p f φ]
   universal_property {a' : 𝒳} (φ' : a' ⟶ b) [IsHomLift p f φ'] :
       ∃! χ : a' ⟶ a, IsHomLift p (𝟙 R) χ ∧ χ ≫ φ = φ'
+attribute [instance] IsCartesian.toIsHomLift
 
 /-- A morphism `φ : a ⟶ b` in `𝒳` lying over `f : R ⟶ S` in `𝒮` is strongly Cartesian if for
 all morphisms `φ' : a' ⟶ b` and all diagrams of the form
@@ -68,9 +70,11 @@ R' --g--> R --f--> S
 ```
 such that `φ'` lifts `g ≫ f`, there exists a lift `χ` of `g` such that `φ' = χ ≫ φ`. -/
 @[stacks 02XK]
-class IsStronglyCartesian : Prop extends IsHomLift p f φ where
+class IsStronglyCartesian : Prop where
+  [toIsHomLift : IsHomLift p f φ]
   universal_property' {a' : 𝒳} (g : p.obj a' ⟶ R) (φ' : a' ⟶ b) [IsHomLift p (g ≫ f) φ'] :
       ∃! χ : a' ⟶ a, IsHomLift p g χ ∧ χ ≫ φ = φ'
+attribute [instance] IsStronglyCartesian.toIsHomLift
 
 end
 

Mathlib/CategoryTheory/FiberedCategory/Cocartesian.lean

@@ -49,10 +49,12 @@ variable {R S : 𝒮} {a b : 𝒳} (f : R ⟶ S) (φ : a ⟶ b)
 /-- A morphism `φ : a ⟶ b` in `𝒳` lying over `f : R ⟶ S` in `𝒮` is co-Cartesian if for all
 morphisms `φ' : a ⟶ b'`, also lying over `f`, there exists a unique morphism `χ : b ⟶ b'` lifting
 `𝟙 S` such that `φ' = φ ≫ χ`. -/
-class IsCocartesian : Prop extends IsHomLift p f φ where
+class IsCocartesian : Prop where
+  [toIsHomLift : IsHomLift p f φ]
   universal_property {b' : 𝒳} (φ' : a ⟶ b') [IsHomLift p f φ'] :
       ∃! χ : b ⟶ b', IsHomLift p (𝟙 S) χ ∧ φ ≫ χ = φ'
 
+attribute [instance] IsCocartesian.toIsHomLift
 /-- A morphism `φ : a ⟶ b` in `𝒳` lying over `f : R ⟶ S` in `𝒮` is strongly co-Cartesian if for
 all morphisms `φ' : a ⟶ b'` and all diagrams of the form
 ```
@@ -63,9 +65,11 @@ R --f--> S --g--> S'
 ```
 such that `φ'` lifts `f ≫ g`, there exists a lift `χ` of `g` such that `φ' = χ ≫ φ`. -/
 @[stacks 02XK]
-class IsStronglyCocartesian : Prop extends IsHomLift p f φ where
+class IsStronglyCocartesian : Prop where
+  [toIsHomLift : IsHomLift p f φ]
   universal_property' {b' : 𝒳} (g : S ⟶ p.obj b') (φ' : a ⟶ b') [IsHomLift p (f ≫ g) φ'] :
       ∃! χ : b ⟶ b', IsHomLift p g χ ∧ φ ≫ χ = φ'
+attribute [instance] IsStronglyCocartesian.toIsHomLift
 
 end
 

Mathlib/CategoryTheory/FiberedCategory/HomLift.lean

@@ -17,13 +17,18 @@ does not make sense when the domain and/or codomain of `φ` and `f` are not defi
 
 ## Main definition
 
-Given morphism `φ : a ⟶ b` in `𝒳` and `f : R ⟶ S` in `𝒮`, `p.IsHomLift f φ` is a class, defined
-using the auxiliary inductive type `IsHomLiftAux` which expresses the fact that `f = p(φ)`.
+Given morphism `φ : a ⟶ b` in `𝒳` and `f : R ⟶ S` in `𝒮`, `p.IsHomLift f φ` is a class
+which expresses the fact that `f = p(φ)`.
 
 We also define a macro `subst_hom_lift p f φ` which can be used to substitute `f` with `p(φ)` in a
-goal, this tactic is just short for `obtain ⟨⟩ := Functor.IsHomLift.cond (p:=p) (f:=f) (φ:=φ)`, and
+goal, this tactic is just short for `obtain ⟨⟩ := inferInstanceAs (p.IsHomLift f φ)`, and
 it is used to make the code more readable.
 
+## Implementation
+The class `IsHomLift` is defined as an inductive with the single constructor
+`.map (φ : a ⟶ b) : IsHomLift p (p.map φ) φ`, similar to how `Eq a b` has the single constructor
+`.rfl (a : α) : Eq a a`.
+
 -/
 
 universe u₁ v₁ u₂ v₂
@@ -34,10 +39,6 @@ variable {𝒮 : Type u₁} {𝒳 : Type u₂} [Category.{v₁} 𝒳] [Category.
 
 namespace CategoryTheory
 
-/-- Helper-type for defining `IsHomLift`. -/
-inductive IsHomLiftAux : ∀ {R S : 𝒮} {a b : 𝒳} (_ : R ⟶ S) (_ : a ⟶ b), Prop
-  | map {a b : 𝒳} (φ : a ⟶ b) : IsHomLiftAux (p.map φ) φ
-
 /-- Given a functor `p : 𝒳 ⥤ 𝒮`, an arrow `φ : a ⟶ b` in `𝒳` and an arrow `f : R ⟶ S` in `𝒮`,
 `p.IsHomLift f φ` expresses the fact that `φ` lifts `f` through `p`.
 This is often drawn as:
@@ -48,19 +49,18 @@ This is often drawn as:
   v        v
   R --f--> S
 ``` -/
-class Functor.IsHomLift {R S : 𝒮} {a b : 𝒳} (f : R ⟶ S) (φ : a ⟶ b) : Prop where
-  cond : IsHomLiftAux p f φ
+class inductive Functor.IsHomLift : ∀ {R S : 𝒮} {a b : 𝒳} (_ : R ⟶ S) (_ : a ⟶ b), Prop
+  | map {a b : 𝒳} (φ : a ⟶ b) : IsHomLift (p.map φ) φ
 
 /-- `subst_hom_lift p f φ` tries to substitute `f` with `p(φ)` by using `p.IsHomLift f φ` -/
 macro "subst_hom_lift" p:term:max f:term:max φ:term:max : tactic =>
-  `(tactic| obtain ⟨⟩ := Functor.IsHomLift.cond (p := $p) (f := $f) (φ := $φ))
+  `(tactic| obtain ⟨⟩ := inferInstanceAs (Functor.IsHomLift $p $f $φ))
 
 namespace IsHomLift
 
 /-- For any arrow `φ : a ⟶ b` in `𝒳`, `φ` lifts the arrow `p.map φ` in the base `𝒮`. -/
 @[simp]
-instance map {a b : 𝒳} (φ : a ⟶ b) : p.IsHomLift (p.map φ) φ where
-  cond := by constructor
+instance map {a b : 𝒳} (φ : a ⟶ b) : p.IsHomLift (p.map φ) φ := .map φ
 
 @[simp]
 instance (a : 𝒳) : p.IsHomLift (𝟙 (p.obj a)) (𝟙 a) := by