-- Mathlib/CategoryTheory/Subobject/Lattice.lean
theorem sInf_le {A : C} (s : Set (Subobject A)) (f) (hf : f ∈ s) : sInf s ≤ f

Proof state:
case w
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : LocallySmall.{w, v₁, u₁} C
inst✝¹ : WellPowered.{w, v₁, u₁} C
inst✝ : HasWidePullbacks C
A : C
s : Set (Subobject A)
f : Subobject A
hf : f ∈ s
⊢ ((underlyingIso (widePullbackι s)).hom ≫
        limit.π (wideCospan s) (some ⟨(equivShrink (Subobject A)) f, ⋯⟩) ≫ eqToHom ⋯) ≫
      f.arrow =
    (sInf s).arrow

Tactic:
dsimp [sInf]

Result:
case w
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : LocallySmall.{w, v₁, u₁} C
inst✝¹ : WellPowered.{w, v₁, u₁} C
inst✝ : HasWidePullbacks C
A : C
s : Set (Subobject A)
f : Subobject A
hf : f ∈ s
⊢ ((underlyingIso (widePullbackι s)).hom ≫
        limit.π (wideCospan s) (some ⟨(equivShrink (Subobject A)) f, ⋯⟩) ≫ eqToHom ⋯) ≫
      f.arrow =
    (mk (widePullbackι s)).arrow

Proof state:
case w
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : LocallySmall.{w, v₁, u₁} C
inst✝¹ : WellPowered.{w, v₁, u₁} C
inst✝ : HasWidePullbacks C
A : C
s : Set (Subobject A)
f : Subobject A
hf : f ∈ s
⊢ limit.π (wideCospan s) (some ⟨(equivShrink (Subobject A)) f, ⋯⟩) ≫ eqToHom ⋯ ≫ f.arrow = widePullbackι s

Tactic:
convert limit.w (wideCospan s) (WidePullbackShape.Hom.term _)

Result:
case h.e'_2.h.h.e'_7.h
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : LocallySmall.{w, v₁, u₁} C
inst✝¹ : WellPowered.{w, v₁, u₁} C
inst✝ : HasWidePullbacks C
A : C
s : Set (Subobject A)
f : Subobject A
hf : f ∈ s
e_1✝ : (widePullback s ⟶ A) = (limit (wideCospan s) ⟶ (wideCospan s).obj none)
e_5✝ : A = (wideCospan s).obj none
⊢ eqToHom ⋯ ≫ f.arrow = (wideCospan s).map (WidePullbackShape.Hom.term ⟨(equivShrink (Subobject A)) f, ⋯⟩)

Proof state:
case h.e'_2.h.h.e'_7.h
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : LocallySmall.{w, v₁, u₁} C
inst✝¹ : WellPowered.{w, v₁, u₁} C
inst✝ : HasWidePullbacks C
A : C
s : Set (Subobject A)
f : Subobject A
hf : f ∈ s
e_1✝ : (widePullback s ⟶ A) = (limit (wideCospan s) ⟶ (wideCospan s).obj none)
e_5✝ : A = (wideCospan s).obj none
⊢ eqToHom ⋯ ≫ f.arrow = (wideCospan s).map (WidePullbackShape.Hom.term ⟨(equivShrink (Subobject A)) f, ⋯⟩)

Tactic:
simp

Result:
no goals

Proof state:
case f
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : LocallySmall.{w, v₁, u₁} C
inst✝¹ : WellPowered.{w, v₁, u₁} C
inst✝ : HasWidePullbacks C
A : C
s : Set (Subobject A)
f : Subobject A
hf : f ∈ s
⊢ underlying.obj (sInf s) ⟶ underlying.obj f

Tactic:
exact (underlyingIso _).hom ≫
  Limits.limit.π (wideCospan s)
    (some ⟨equivShrink (Subobject A) f,
      Set.mem_image_of_mem (equivShrink (Subobject A)) hf⟩) ≫
  eqToHom (congr_arg (fun X : Subobject A => (X : C)) (Equiv.symm_apply_apply _ _))

Result:
no goals

Proof state:
case w
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : LocallySmall.{w, v₁, u₁} C
inst✝¹ : WellPowered.{w, v₁, u₁} C
inst✝ : HasWidePullbacks C
A : C
s : Set (Subobject A)
f : Subobject A
hf : f ∈ s
⊢ ((underlyingIso (widePullbackι s)).hom ≫
        limit.π (wideCospan s) (some ⟨(equivShrink (Subobject A)) f, ⋯⟩) ≫ eqToHom ⋯) ≫
      f.arrow =
    (mk (widePullbackι s)).arrow

Tactic:
simp only [Category.comp_id, Category.assoc, ← underlyingIso_hom_comp_eq_mk,
  Subobject.arrow_congr, congrArg_mpr_hom_left, Iso.cancel_iso_hom_left]

Result:
case w
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : LocallySmall.{w, v₁, u₁} C
inst✝¹ : WellPowered.{w, v₁, u₁} C
inst✝ : HasWidePullbacks C
A : C
s : Set (Subobject A)
f : Subobject A
hf : f ∈ s
⊢ limit.π (wideCospan s) (some ⟨(equivShrink (Subobject A)) f, ⋯⟩) ≫ eqToHom ⋯ ≫ f.arrow = widePullbackι s

Proof state:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : LocallySmall.{w, v₁, u₁} C
inst✝¹ : WellPowered.{w, v₁, u₁} C
inst✝ : HasWidePullbacks C
A : C
s : Set (Subobject A)
f : Subobject A
hf : f ∈ s
⊢ sInf s ≤ f

Tactic:
fapply le_of_comm

Result:
case f
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : LocallySmall.{w, v₁, u₁} C
inst✝¹ : WellPowered.{w, v₁, u₁} C
inst✝ : HasWidePullbacks C
A : C
s : Set (Subobject A)
f : Subobject A
hf : f ∈ s
⊢ underlying.obj (sInf s) ⟶ underlying.obj f

case w
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : LocallySmall.{w, v₁, u₁} C
inst✝¹ : WellPowered.{w, v₁, u₁} C
inst✝ : HasWidePullbacks C
A : C
s : Set (Subobject A)
f : Subobject A
hf : f ∈ s
⊢ ?f ≫ f.arrow = (sInf s).arrow