case f
C : Type u₁
inst✝³ : Category C
X Y Z : C
D : Type u₂
inst✝² : Category D
inst✝¹ : WellPowered C
inst✝ : HasWidePullbacks C
A : C
s : Set (Subobject A)
f : Subobject A
k : ∀ (g : Subobject A), g ∈ s → f ≤ g
⊢ underlying.obj f ⟶ underlying.obj (sInf s)

case w
C : Type u₁
inst✝³ : Category C
X Y Z : C
D : Type u₂
inst✝² : Category D
inst✝¹ : WellPowered C
inst✝ : HasWidePullbacks C
A : C
s : Set (Subobject A)
f : Subobject A
k : ∀ (g : Subobject A), g ∈ s → f ≤ g
⊢ ?f ≫ arrow (sInf s) = arrow f
C : Type u₁
inst✝³ : Category C
X Y Z : C
D : Type u₂
inst✝² : Category D
inst✝¹ : WellPowered C
inst✝ : HasWidePullbacks C
A : C
s : Set (Subobject A)
f : Subobject A
k : ∀ (g : Subobject A), g ∈ s → f ≤ g
⊢ f ≤ sInf s
fapply le_of_comm
no goals
case f
C : Type u₁
inst✝³ : Category C
X Y Z : C
D : Type u₂
inst✝² : Category D
inst✝¹ : WellPowered C
inst✝ : HasWidePullbacks C
A : C
s : Set (Subobject A)
f : Subobject A
k : ∀ (g : Subobject A), g ∈ s → f ≤ g
⊢ underlying.obj f ⟶ underlying.obj (sInf s)
exact Limits.limit.lift _ (leInfCone s f k) ≫ (underlyingIso _).inv
case w
C : Type u₁
inst✝³ : Category C
X Y Z : C
D : Type u₂
inst✝² : Category D
inst✝¹ : WellPowered C
inst✝ : HasWidePullbacks C
A : C
s : Set (Subobject A)
f : Subobject A
k : ∀ (g : Subobject A), g ∈ s → f ≤ g
⊢ (limit.lift (wideCospan s) (leInfCone s f k) ≫ (underlyingIso (widePullbackι s)).inv) ≫ arrow (mk (widePullbackι s)) =
    arrow f
case w
C : Type u₁
inst✝³ : Category C
X Y Z : C
D : Type u₂
inst✝² : Category D
inst✝¹ : WellPowered C
inst✝ : HasWidePullbacks C
A : C
s : Set (Subobject A)
f : Subobject A
k : ∀ (g : Subobject A), g ∈ s → f ≤ g
⊢ (limit.lift (wideCospan s) (leInfCone s f k) ≫ (underlyingIso (widePullbackι s)).inv) ≫ arrow (sInf s) = arrow f
dsimp [sInf]
no goals
case w
C : Type u₁
inst✝³ : Category C
X Y Z : C
D : Type u₂
inst✝² : Category D
inst✝¹ : WellPowered C
inst✝ : HasWidePullbacks C
A : C
s : Set (Subobject A)
f : Subobject A
k : ∀ (g : Subobject A), g ∈ s → f ≤ g
⊢ (limit.lift (wideCospan s) (leInfCone s f k) ≫ (underlyingIso (widePullbackι s)).inv) ≫ arrow (mk (widePullbackι s)) =
    arrow f
rw [assoc, underlyingIso_arrow, widePullbackι, limit.lift_π, leInfCone_π_app_none]