awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Subobject.Lattice
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : LocallySmall.{w, v₁, u₁} C
inst_3 : WellPowered.{w, v₁, u₁} C
A : C
s : Set (Subobject.{v₁, u₁} A)
f : Subobject.{v₁, u₁} A
k : ∀ g ∈ s, f ≤ g
g : Subobject.{v₁, u₁} A
m : g ∈ s
⊢ Membership.mem (α := Subobject.{v₁, u₁} A) s
    ((Equiv.symm (equivShrink (Subobject.{v₁, u₁} A)) : (a : Shrink.{w, max u₁ v₁} (Subobject A)) → Subobject A)
        (↑(Subtype.mk (p := fun (x : Shrink.{w, max u₁ v₁} (Subobject.{v₁, u₁} A)) ↦
              Membership.mem (γ := Set (Shrink.{w, max u₁ v₁} (Subobject.{v₁, u₁} A)))
                ((⇑(equivShrink (Subobject.{v₁, u₁} A)) : (a : Subobject A) → Shrink.{w, max u₁ v₁} (Subobject A)) '' s)
                x)
              ((equivShrink (Subobject.{v₁, u₁} A) : (a : Subobject A) → Shrink.{w, max u₁ v₁} (Subobject A)) g) ⋯) :
          Shrink.{w, max u₁ v₁} (Subobject A)) :
      Subobject.{v₁, u₁} A)

Tactic:
simpa using m
-- Module: Mathlib.CategoryTheory.Subobject.Lattice
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : LocallySmall.{w, v₁, u₁} C
inst_3 : WellPowered.{w, v₁, u₁} C
A : C
s : Set (Subobject.{v₁, u₁} A)
f : Subobject.{v₁, u₁} A
k : ∀ g ∈ s, f ≤ g
⊢ ∀
    (j :
      (↑((⇑(equivShrink (Subobject.{v₁, u₁} A)) : (a : Subobject A) → Shrink.{w, max u₁ v₁} (Subobject A)) '' s) :
        Type w)),
    CategoryStruct.comp (Y :=
        Functor.obj
          (wideCospan s :
            Functor.{w, v₁, w, u₁}
              (WidePullbackShape
                (↑((⇑(equivShrink (Subobject.{v₁, u₁} A)) : (a : Subobject A) → Shrink.{w, max u₁ v₁} (Subobject A)) ''
                      s) :
                  Type w))
              C)
          (some j))
        ((fun
                (j :
                  (↑((⇑(equivShrink (Subobject.{v₁, u₁} A)) :
                          (a : Subobject A) → Shrink.{w, max u₁ v₁} (Subobject A)) ''
                        s) :
                    Type w)) ↦
              (Functor.map underlying (homOfLE ⋯) :
                Functor.obj underlying f ⟶
                  Functor.obj (C := Subobject.{v₁, u₁} A) underlying
                    ((Equiv.symm (equivShrink (Subobject.{v₁, u₁} A)) :
                        (a : Shrink.{w, max u₁ v₁} (Subobject A)) → Subobject A)
                      (↑j : Shrink.{w, max u₁ v₁} (Subobject A)))))
            j :
          Functor.obj underlying f ⟶
            Functor.obj (C := Subobject.{v₁, u₁} A) underlying
              ((Equiv.symm (equivShrink (Subobject.{v₁, u₁} A)) :
                  (a : Shrink.{w, max u₁ v₁} (Subobject A)) → Subobject A)
                (↑j : Shrink.{w, max u₁ v₁} (Subobject A))))
        (Functor.map (wideCospan s) (WidePullbackShape.Hom.term j) :
          Functor.obj
              (wideCospan s :
                Functor.{w, v₁, w, u₁}
                  (WidePullbackShape
                    (↑((⇑(equivShrink (Subobject.{v₁, u₁} A)) :
                            (a : Subobject A) → Shrink.{w, max u₁ v₁} (Subobject A)) ''
                          s) :
                      Type w))
                  C)
              (some j) ⟶
            Functor.obj.{w, v₁, w, u₁} (C :=
              WidePullbackShape
                (↑((⇑(equivShrink (Subobject.{v₁, u₁} A)) : (a : Subobject A) → Shrink.{w, max u₁ v₁} (Subobject A)) ''
                      s) :
                  Type w))
              (wideCospan s :
                Functor.{w, v₁, w, u₁}
                  (WidePullbackShape
                    (↑((⇑(equivShrink (Subobject.{v₁, u₁} A)) :
                            (a : Subobject A) → Shrink.{w, max u₁ v₁} (Subobject A)) ''
                          s) :
                      Type w))
                  C)
              (none :
                Option
                  (↑((⇑(equivShrink (Subobject.{v₁, u₁} A)) :
                          (a : Subobject A) → Shrink.{w, max u₁ v₁} (Subobject A)) ''
                        s) :
                    Type w))) =
      f.arrow

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Subobject.Lattice
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : LocallySmall.{w, v₁, u₁} C
inst_2 : WellPowered.{w, v₁, u₁} C
A : C
s : Set (Subobject.{v₁, u₁} A)
f : Subobject.{v₁, u₁} A
k : ∀ g ∈ s, f ≤ g
⊢ NatTrans.app (Cone.π (leInfCone s f k)) none = f.arrow

Tactic:
rfl

Premises used: CategoryTheory.Subobject.arrow, rfl
-- Module: Mathlib.CategoryTheory.Subobject.Lattice
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : LocallySmall.{w, v₁, u₁} C
inst_3 : WellPowered.{w, v₁, u₁} C
inst_4 : HasWidePullbacks.{w, v₁, u₁} C
A : C
s : Set (Subobject.{v₁, u₁} A)
Z_1 : C
u v : Z_1 ⟶ widePullback.{w, v₁, u₁} s
h : u ≫ widePullbackι s = v ≫ widePullbackι s
⊢ Eq (α :=
    Z_1 ⟶
      Functor.obj.{w, v₁, w, u₁} (C :=
        WidePullbackShape
          (↑((⇑(equivShrink (Subobject.{v₁, u₁} A)) : (a : Subobject A) → Shrink.{w, max u₁ v₁} (Subobject A)) '' s) :
            Type w))
        (wideCospan s :
          Functor.{w, v₁, w, u₁}
            (WidePullbackShape
              (↑((⇑(equivShrink (Subobject.{v₁, u₁} A)) : (a : Subobject A) → Shrink.{w, max u₁ v₁} (Subobject A)) ''
                    s) :
                Type w))
            C)
        (none :
          Option
            (↑((⇑(equivShrink (Subobject.{v₁, u₁} A)) : (a : Subobject A) → Shrink.{w, max u₁ v₁} (Subobject A)) '' s) :
              Type w)))
    (u ≫ limit.π (wideCospan s) none :
      Z_1 ⟶
        Functor.obj.{w, v₁, w, u₁} (C :=
          WidePullbackShape
            (↑((⇑(equivShrink (Subobject.{v₁, u₁} A)) : (a : Subobject A) → Shrink.{w, max u₁ v₁} (Subobject A)) '' s) :
              Type w))
          (wideCospan s :
            Functor.{w, v₁, w, u₁}
              (WidePullbackShape
                (↑((⇑(equivShrink (Subobject.{v₁, u₁} A)) : (a : Subobject A) → Shrink.{w, max u₁ v₁} (Subobject A)) ''
                      s) :
                  Type w))
              C)
          (none :
            Option
              (↑((⇑(equivShrink (Subobject.{v₁, u₁} A)) : (a : Subobject A) → Shrink.{w, max u₁ v₁} (Subobject A)) ''
                    s) :
                Type w)))
    (v ≫ limit.π (wideCospan s) none :
      Z_1 ⟶
        Functor.obj.{w, v₁, w, u₁} (C :=
          WidePullbackShape
            (↑((⇑(equivShrink (Subobject.{v₁, u₁} A)) : (a : Subobject A) → Shrink.{w, max u₁ v₁} (Subobject A)) '' s) :
              Type w))
          (wideCospan s :
            Functor.{w, v₁, w, u₁}
              (WidePullbackShape
                (↑((⇑(equivShrink (Subobject.{v₁, u₁} A)) : (a : Subobject A) → Shrink.{w, max u₁ v₁} (Subobject A)) ''
                      s) :
                  Type w))
              C)
          (none :
            Option
              (↑((⇑(equivShrink (Subobject.{v₁, u₁} A)) : (a : Subobject A) → Shrink.{w, max u₁ v₁} (Subobject A)) ''
                    s) :
                Type w)))

Tactic:
h

Premises used: CategoryTheory.Subobject.widePullbackι, CategoryTheory.Subobject.widePullback
-- Module: Mathlib.CategoryTheory.Subobject.Lattice
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : LocallySmall.{w, v₁, u₁} C
inst_3 : WellPowered.{w, v₁, u₁} C
inst_4 : HasWidePullbacks.{w, v₁, u₁} C
A : C
s : Set (Subobject.{v₁, u₁} A)
Z_1 : C
u v : Z_1 ⟶ widePullback.{w, v₁, u₁} s
h : u ≫ widePullbackι s = v ≫ widePullbackι s
⊢ Eq (α :=
    Z_1 ⟶
      Functor.obj.{w, v₁, w, u₁} (C :=
        WidePullbackShape
          (↑((⇑(equivShrink (Subobject.{v₁, u₁} A)) : (a : Subobject A) → Shrink.{w, max u₁ v₁} (Subobject A)) '' s) :
            Type w))
        (wideCospan s :
          Functor.{w, v₁, w, u₁}
            (WidePullbackShape
              (↑((⇑(equivShrink (Subobject.{v₁, u₁} A)) : (a : Subobject A) → Shrink.{w, max u₁ v₁} (Subobject A)) ''
                    s) :
                Type w))
            C)
        (none :
          Option
            (↑((⇑(equivShrink (Subobject.{v₁, u₁} A)) : (a : Subobject A) → Shrink.{w, max u₁ v₁} (Subobject A)) '' s) :
              Type w)))
    (u ≫ limit.π (wideCospan s) none :
      Z_1 ⟶
        Functor.obj.{w, v₁, w, u₁} (C :=
          WidePullbackShape
            (↑((⇑(equivShrink (Subobject.{v₁, u₁} A)) : (a : Subobject A) → Shrink.{w, max u₁ v₁} (Subobject A)) '' s) :
              Type w))
          (wideCospan s :
            Functor.{w, v₁, w, u₁}
              (WidePullbackShape
                (↑((⇑(equivShrink (Subobject.{v₁, u₁} A)) : (a : Subobject A) → Shrink.{w, max u₁ v₁} (Subobject A)) ''
                      s) :
                  Type w))
              C)
          (none :
            Option
              (↑((⇑(equivShrink (Subobject.{v₁, u₁} A)) : (a : Subobject A) → Shrink.{w, max u₁ v₁} (Subobject A)) ''
                    s) :
                Type w)))
    (v ≫ limit.π (wideCospan s) none :
      Z_1 ⟶
        Functor.obj.{w, v₁, w, u₁} (C :=
          WidePullbackShape
            (↑((⇑(equivShrink (Subobject.{v₁, u₁} A)) : (a : Subobject A) → Shrink.{w, max u₁ v₁} (Subobject A)) '' s) :
              Type w))
          (wideCospan s :
            Functor.{w, v₁, w, u₁}
              (WidePullbackShape
                (↑((⇑(equivShrink (Subobject.{v₁, u₁} A)) : (a : Subobject A) → Shrink.{w, max u₁ v₁} (Subobject A)) ''
                      s) :
                  Type w))
              C)
          (none :
            Option
              (↑((⇑(equivShrink (Subobject.{v₁, u₁} A)) : (a : Subobject A) → Shrink.{w, max u₁ v₁} (Subobject A)) ''
                    s) :
                Type w)))

Tactic:
exact h
-- Module: Mathlib.CategoryTheory.Subobject.Lattice
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : LocallySmall.{w, v₁, u₁} C
inst_3 : WellPowered.{w, v₁, u₁} C
inst_4 : HasWidePullbacks.{w, v₁, u₁} C
A : C
s : Set (Subobject.{v₁, u₁} A)
Z_1 : C
u v : Z_1 ⟶ widePullback.{w, v₁, u₁} s
h : u ≫ widePullbackι s = v ≫ widePullbackι s
val :
  (↑((⇑(equivShrink (Subobject.{v₁, u₁} A)) : (a : Subobject A) → Shrink.{w, max u₁ v₁} (Subobject A)) '' s) : Type w)
⊢ Eq (α := Z_1 ⟶ A) (u ≫ limit.π (wideCospan s) none : Z_1 ⟶ A) (v ≫ limit.π (wideCospan s) none : Z_1 ⟶ A)

Tactic:
h

Premises used: CategoryTheory.Subobject.widePullbackι, CategoryTheory.Subobject.widePullback
-- Module: Mathlib.CategoryTheory.Subobject.Lattice
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : LocallySmall.{w, v₁, u₁} C
inst_3 : WellPowered.{w, v₁, u₁} C
inst_4 : HasWidePullbacks.{w, v₁, u₁} C
A : C
s : Set (Subobject.{v₁, u₁} A)
Z_1 : C
u v : Z_1 ⟶ widePullback.{w, v₁, u₁} s
h : u ≫ widePullbackι s = v ≫ widePullbackι s
val :
  (↑((⇑(equivShrink (Subobject.{v₁, u₁} A)) : (a : Subobject A) → Shrink.{w, max u₁ v₁} (Subobject A)) '' s) : Type w)
⊢ Eq (α := Z_1 ⟶ A) (u ≫ limit.π (wideCospan s) none : Z_1 ⟶ A) (v ≫ limit.π (wideCospan s) none : Z_1 ⟶ A)

Tactic:
exact h
-- Module: Mathlib.CategoryTheory.Subobject.Lattice
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : LocallySmall.{w, v₁, u₁} C
inst_2 : WellPowered.{w, v₁, u₁} C
inst_3 : HasWidePullbacks.{w, v₁, u₁} C
A : C
s : Set (Subobject.{v₁, u₁} A)
f : Subobject.{v₁, u₁} A
hf : f ∈ s
⊢ Functor.obj underlying (sInf.{w, v₁, u₁} s) ⟶ Functor.obj underlying 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 _ _))

Premises used: CategoryTheory.Limits.limit.π, CategoryTheory.Subobject.underlying, Equiv.symm_apply_apply, CategoryTheory.eqToHom, Option.some, CategoryTheory.Subobject.underlyingIso, Subtype.mk, congr_arg, Set.mem_image_of_mem, CategoryTheory.Subobject.wideCospan, equivShrink, CategoryTheory.Iso.hom, DFunLike.coe, CategoryTheory.Functor.obj, CategoryTheory.Subobject
-- Module: Mathlib.CategoryTheory.Subobject.Lattice
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : LocallySmall.{w, v₁, u₁} C
inst_2 : WellPowered.{w, v₁, u₁} C
inst_3 : HasWidePullbacks.{w, v₁, u₁} C
A : C
s : Set (Subobject.{v₁, u₁} A)
f : Subobject.{v₁, u₁} A
k : ∀ g ∈ s, f ≤ g
f₁ : Functor.obj underlying f ⟶ Functor.obj underlying (sInf.{w, v₁, u₁} s)
w :
  (limit.lift (wideCospan s) (leInfCone s f k) ≫ Iso.inv (underlyingIso (widePullbackι s))) ≫
      (sInf.{w, v₁, u₁} s).arrow =
    f.arrow
⊢ f ≤ sInf.{w, v₁, u₁} s

Tactic:
fapply le_of_comm

Premises used: CategoryTheory.Subobject.le_of_comm
-- Module: Mathlib.CategoryTheory.Subobject.Lattice
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : LocallySmall.{w, v₁, u₁} C
inst_2 : WellPowered.{w, v₁, u₁} C
inst_3 : HasWidePullbacks.{w, v₁, u₁} C
A : C
s : Set (Subobject.{v₁, u₁} A)
f : Subobject.{v₁, u₁} A
k : ∀ g ∈ s, f ≤ g
⊢ Functor.obj underlying f ⟶ Functor.obj underlying (sInf.{w, v₁, u₁} s)

Tactic:
exact Limits.limit.lift _ (leInfCone s f k) ≫ (underlyingIso _).inv

Premises used: CategoryTheory.Subobject.underlyingIso, CategoryTheory.Limits.limit.lift, CategoryTheory.Iso.inv, CategoryTheory.Subobject.leInfCone
-- Module: Mathlib.CategoryTheory.Subobject.Lattice
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : LocallySmall.{w, v₁, u₁} C
inst_2 : WellPowered.{w, v₁, u₁} C
inst_3 : HasWidePullbacks.{w, v₁, u₁} C
A : C
s : Set (Subobject.{v₁, u₁} A)
f : Subobject.{v₁, u₁} A
k : ∀ g ∈ s, f ≤ g
w :
  (limit.lift (wideCospan s) (leInfCone s f k) ≫ Iso.inv (underlyingIso (widePullbackι s))) ≫
      (mk (A := widePullback.{w, v₁, u₁} s) (widePullbackι s)).arrow =
    f.arrow
⊢ (limit.lift (wideCospan s) (leInfCone s f k) ≫ Iso.inv (underlyingIso (widePullbackι s))) ≫
      (sInf.{w, v₁, u₁} s).arrow =
    f.arrow

Tactic:
dsimp [sInf]

Premises used: CategoryTheory.Subobject.sInf
-- Module: Mathlib.CategoryTheory.Subobject.Lattice
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : LocallySmall.{w, v₁, u₁} C
inst_2 : WellPowered.{w, v₁, u₁} C
inst_3 : HasCoproducts.{w, v₁, u₁} C
inst_4 : HasImages.{v₁, u₁} C
A : C
s : Set (Subobject.{v₁, u₁} A)
f : Subobject.{v₁, u₁} A
hf : f ∈ s
⊢ Membership.mem.{w, w} (α := Shrink.{w, max u₁ v₁} (Subobject.{v₁, u₁} A)) (γ :=
    Set (Shrink.{w, max u₁ v₁} (Subobject.{v₁, u₁} A)))
    ((⇑(equivShrink (Subobject.{v₁, u₁} A)) : (a : Subobject A) → Shrink.{w, max u₁ v₁} (Subobject A)) '' s)
    ((equivShrink (Subobject.{v₁, u₁} A) : (a : Subobject A) → Shrink.{w, max u₁ v₁} (Subobject A)) f :
      Shrink.{w, max u₁ v₁} (Subobject.{v₁, u₁} A))

Tactic:
simpa [Set.mem_image] using hf

Premises used: Set.mem_image
-- Module: Mathlib.CategoryTheory.Subobject.Lattice
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : LocallySmall.{w, v₁, u₁} C
inst_2 : WellPowered.{w, v₁, u₁} C
inst_3 : HasCoproducts.{w, v₁, u₁} C
inst_4 : HasImages.{v₁, u₁} C
A : C
s : Set (Subobject.{v₁, u₁} A)
f : Subobject.{v₁, u₁} A
hf : f ∈ s
f₁ :
  Functor.obj underlying f =
    Functor.obj (C := Subobject.{v₁, u₁} A) underlying
      ((Equiv.symm (equivShrink (Subobject.{v₁, u₁} A)) : (a : Shrink.{w, max u₁ v₁} (Subobject A)) → Subobject A)
        (↑(Subtype.mk (p := fun (x : Shrink.{w, max u₁ v₁} (Subobject.{v₁, u₁} A)) ↦
              Membership.mem (γ := Set (Shrink.{w, max u₁ v₁} (Subobject.{v₁, u₁} A)))
                ((⇑(equivShrink (Subobject.{v₁, u₁} A)) : (a : Subobject A) → Shrink.{w, max u₁ v₁} (Subobject A)) '' s)
                x)
              ((equivShrink (Subobject.{v₁, u₁} A) : (a : Subobject A) → Shrink.{w, max u₁ v₁} (Subobject A)) f) ⋯) :
          Shrink.{w, max u₁ v₁} (Subobject A)))
⊢ Functor.obj underlying f ⟶ Functor.obj underlying (sSup.{w, v₁, u₁} s)

Tactic:
refine eqToHom ?_ ≫ Sigma.ι _ ⟨equivShrink (Subobject A) f, by simpa [Set.mem_image] using hf⟩
      ≫ factorThruImage _ ≫ (underlyingIso _).inv

Premises used: CategoryTheory.Limits.factorThruImage, CategoryTheory.eqToHom, CategoryTheory.Limits.Sigma.ι, CategoryTheory.Subobject.underlyingIso, CategoryTheory.Iso.inv
-- Module: Mathlib.CategoryTheory.Subobject.Lattice
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : LocallySmall.{w, v₁, u₁} C
inst_2 : WellPowered.{w, v₁, u₁} C
inst_3 : HasCoproducts.{w, v₁, u₁} C
inst_4 : HasImages.{v₁, u₁} C
A : C
s : Set (Subobject.{v₁, u₁} A)
f : Subobject.{v₁, u₁} A
hf : f ∈ s
⊢ Functor.obj underlying f =
    Functor.obj (C := Subobject.{v₁, u₁} A) underlying
      ((Equiv.symm (equivShrink (Subobject.{v₁, u₁} A)) : (a : Shrink.{w, max u₁ v₁} (Subobject A)) → Subobject A)
        (↑(Subtype.mk (p := fun (x : Shrink.{w, max u₁ v₁} (Subobject.{v₁, u₁} A)) ↦
              Membership.mem (γ := Set (Shrink.{w, max u₁ v₁} (Subobject.{v₁, u₁} A)))
                ((⇑(equivShrink (Subobject.{v₁, u₁} A)) : (a : Subobject A) → Shrink.{w, max u₁ v₁} (Subobject A)) '' s)
                x)
              ((equivShrink (Subobject.{v₁, u₁} A) : (a : Subobject A) → Shrink.{w, max u₁ v₁} (Subobject A)) f) ⋯) :
          Shrink.{w, max u₁ v₁} (Subobject A)))

Tactic:
(congr_arg (fun X : Subobject A => (X : C)) (Equiv.symm_apply_apply _ _).symm)

Premises used: CategoryTheory.Subobject.underlying, Equiv.symm_apply_apply, congr_arg, Eq.symm, CategoryTheory.Functor.obj
-- Module: Mathlib.CategoryTheory.Subobject.Lattice
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : LocallySmall.{w, v₁, u₁} C
inst_2 : WellPowered.{w, v₁, u₁} C
inst_3 : HasCoproducts.{w, v₁, u₁} C
inst_4 : HasImages.{v₁, u₁} C
A : C
s : Set (Subobject.{v₁, u₁} A)
f : Subobject.{v₁, u₁} A
hf : f ∈ s
⊢ Functor.obj underlying f =
    Functor.obj (C := Subobject.{v₁, u₁} A) underlying
      ((Equiv.symm (equivShrink (Subobject.{v₁, u₁} A)) : (a : Shrink.{w, max u₁ v₁} (Subobject A)) → Subobject A)
        (↑(Subtype.mk (p := fun (x : Shrink.{w, max u₁ v₁} (Subobject.{v₁, u₁} A)) ↦
              Membership.mem (γ := Set (Shrink.{w, max u₁ v₁} (Subobject.{v₁, u₁} A)))
                ((⇑(equivShrink (Subobject.{v₁, u₁} A)) : (a : Subobject A) → Shrink.{w, max u₁ v₁} (Subobject A)) '' s)
                x)
              ((equivShrink (Subobject.{v₁, u₁} A) : (a : Subobject A) → Shrink.{w, max u₁ v₁} (Subobject A)) f) ⋯) :
          Shrink.{w, max u₁ v₁} (Subobject A)))

Tactic:
exact (congr_arg (fun X : Subobject A => (X : C)) (Equiv.symm_apply_apply _ _).symm)

Premises used: CategoryTheory.Subobject.underlying, Equiv.symm_apply_apply, congr_arg, Eq.symm, CategoryTheory.Functor.obj
-- Module: Mathlib.CategoryTheory.Subobject.Lattice
Goal:
α : Type u_1
β : Type u_2
e : α ≃ β
s : Set α
x : β
h : Membership.mem (α := α) s ((e.symm : (a : β) → α) x : α)
⊢ (e : (a : α) → β) ((e.symm : (a : β) → α) x : α) = x

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Subobject.Lattice
Goal:
α : Type u_1
β : Type u_2
e : α ≃ β
s : Set α
a : α
m : a ∈ s
⊢ Membership.mem (α := α) s ((e.symm : (a : β) → α) ((e : (a : α) → β) a : β) : α)

Tactic:
simpa using m
-- Module: Mathlib.CategoryTheory.Subobject.Lattice
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : LocallySmall.{w, v₁, u₁} C
inst_2 : WellPowered.{w, v₁, u₁} C
inst_3 : HasCoproducts.{w, v₁, u₁} C
inst_4 : HasImages.{v₁, u₁} C
A : C
s : Set (Subobject.{v₁, u₁} A)
f : Subobject.{v₁, u₁} A
k : ∀ g ∈ s, g ≤ f
f₁ :
  (b :
      (↑((⇑(equivShrink (Subobject.{v₁, u₁} A)) : (a : Subobject A) → Shrink.{w, max u₁ v₁} (Subobject A)) '' s) :
        Type w)) →
    Functor.obj (C := Subobject.{v₁, u₁} A) underlying
        ((Equiv.symm (equivShrink (Subobject.{v₁, u₁} A)) : (a : Shrink.{w, max u₁ v₁} (Subobject A)) → Subobject A)
          (↑b : Shrink.{w, max u₁ v₁} (Subobject A))) ⟶
      Functor.obj underlying f
⊢ (sigmaObj.{w, v₁, u₁}
      fun
        (j :
          (↑((⇑(equivShrink (Subobject.{v₁, u₁} A)) : (a : Subobject A) → Shrink.{w, max u₁ v₁} (Subobject A)) '' s) :
            Type w)) ↦
      Functor.obj (C := Subobject.{v₁, u₁} A) underlying
        ((Equiv.symm (equivShrink (Subobject.{v₁, u₁} A)) : (a : Shrink.{w, max u₁ v₁} (Subobject A)) → Subobject A)
          (↑j : Shrink.{w, max u₁ v₁} (Subobject A)))) ⟶
    Functor.obj underlying f

Tactic:
refine Sigma.desc ?_

Premises used: CategoryTheory.Limits.Sigma.desc
-- Module: Mathlib.CategoryTheory.Subobject.Lattice
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : LocallySmall.{w, v₁, u₁} C
inst_2 : WellPowered.{w, v₁, u₁} C
inst_3 : HasCoproducts.{w, v₁, u₁} C
inst_4 : HasImages.{v₁, u₁} C
A : C
s : Set (Subobject.{v₁, u₁} A)
f : Subobject.{v₁, u₁} A
k : ∀ g ∈ s, g ≤ f
g : Shrink.{w, max u₁ v₁} (Subobject.{v₁, u₁} A)
m :
  Membership.mem (γ := Set (Shrink.{w, max u₁ v₁} (Subobject.{v₁, u₁} A)))
    ((⇑(equivShrink (Subobject.{v₁, u₁} A)) : (a : Subobject A) → Shrink.{w, max u₁ v₁} (Subobject A)) '' s) g
f₁ :
  Membership.mem (α := Subobject.{v₁, u₁} A) s
    ((Equiv.symm (equivShrink (Subobject.{v₁, u₁} A)) : (a : Shrink.{w, max u₁ v₁} (Subobject A)) → Subobject A)
        (↑(Subtype.mk (p := fun (x : Shrink.{w, max u₁ v₁} (Subobject.{v₁, u₁} A)) ↦
              Membership.mem (γ := Set (Shrink.{w, max u₁ v₁} (Subobject.{v₁, u₁} A)))
                ((⇑(equivShrink (Subobject.{v₁, u₁} A)) : (a : Subobject A) → Shrink.{w, max u₁ v₁} (Subobject A)) '' s)
                x)
              g m) :
          Shrink.{w, max u₁ v₁} (Subobject A)) :
      Subobject.{v₁, u₁} A)
⊢ Functor.obj (C := Subobject.{v₁, u₁} A) underlying
      ((Equiv.symm (equivShrink (Subobject.{v₁, u₁} A)) : (a : Shrink.{w, max u₁ v₁} (Subobject A)) → Subobject A)
        (↑(Subtype.mk (p := fun (x : Shrink.{w, max u₁ v₁} (Subobject.{v₁, u₁} A)) ↦
              Membership.mem (γ := Set (Shrink.{w, max u₁ v₁} (Subobject.{v₁, u₁} A)))
                ((⇑(equivShrink (Subobject.{v₁, u₁} A)) : (a : Subobject A) → Shrink.{w, max u₁ v₁} (Subobject A)) '' s)
                x)
              g m) :
          Shrink.{w, max u₁ v₁} (Subobject A))) ⟶
    Functor.obj underlying f

Tactic:
refine underlying.map (homOfLE (k _ ?_))

Premises used: CategoryTheory.Subobject.underlying, CategoryTheory.Functor.map, CategoryTheory.homOfLE
-- Module: Mathlib.CategoryTheory.Subobject.Lattice
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : LocallySmall.{w, v₁, u₁} C
inst_2 : WellPowered.{w, v₁, u₁} C
inst_3 : HasCoproducts.{w, v₁, u₁} C
inst_4 : HasImages.{v₁, u₁} C
A : C
s : Set (Subobject.{v₁, u₁} A)
f : Subobject.{v₁, u₁} A
k : ∀ g ∈ s, g ≤ f
g : Shrink.{w, max u₁ v₁} (Subobject.{v₁, u₁} A)
m :
  Membership.mem (γ := Set (Shrink.{w, max u₁ v₁} (Subobject.{v₁, u₁} A)))
    ((⇑(equivShrink (Subobject.{v₁, u₁} A)) : (a : Subobject A) → Shrink.{w, max u₁ v₁} (Subobject A)) '' s) g
⊢ Membership.mem (α := Subobject.{v₁, u₁} A) s
    ((Equiv.symm (equivShrink (Subobject.{v₁, u₁} A)) : (a : Shrink.{w, max u₁ v₁} (Subobject A)) → Subobject A)
        (↑(Subtype.mk (p := fun (x : Shrink.{w, max u₁ v₁} (Subobject.{v₁, u₁} A)) ↦
              Membership.mem (γ := Set (Shrink.{w, max u₁ v₁} (Subobject.{v₁, u₁} A)))
                ((⇑(equivShrink (Subobject.{v₁, u₁} A)) : (a : Subobject A) → Shrink.{w, max u₁ v₁} (Subobject A)) '' s)
                x)
              g m) :
          Shrink.{w, max u₁ v₁} (Subobject A)) :
      Subobject.{v₁, u₁} A)

Tactic:
simpa using m
-- Module: Mathlib.CategoryTheory.Subobject.Lattice
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
hX : IsInitial.{v₁, u₁} X
this : ∀ (S : Subobject.{v₁, u₁} X), S = mk (𝟙 X)
⊢ ∀ (a b : Subobject.{v₁, u₁} X), a = b

Tactic:
simp [this]
-- Module: Mathlib.CategoryTheory.Subobject.Lattice
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
hX : IsInitial.{v₁, u₁} X
suffices : ∀ (S : Subobject.{v₁, u₁} X), S = mk (𝟙 X)
⊢ Subsingleton (Subobject.{v₁, u₁} X)

Tactic:
suffices ∀ (S : Subobject X), S = .mk (𝟙 _) from ⟨by simp [this]⟩
-- Module: Mathlib.CategoryTheory.Subobject.Lattice
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
hX : IsInitial.{v₁, u₁} X
S : Subobject.{v₁, u₁} X
obtain : ∀ (A : C) (i : A ⟶ X) (w : Mono i), mk i = mk (𝟙 X)
⊢ S = mk (𝟙 X)

Tactic:
obtain ⟨A, i, _, rfl⟩ := S.mk_surjective

Premises used: CategoryTheory.Subobject.mk_surjective, rfl
-- Module: Mathlib.CategoryTheory.Subobject.Lattice
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
hX : IsInitial.{v₁, u₁} X
A : C
i : A ⟶ X
w : Mono i
⊢ hX.to A ≫ i = 𝟙 X

Tactic:
have fac : hX.to A ≫ i = 𝟙 X := hX.hom_ext _ _