awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Subfunctor.Basic
Goal:
C : Type u
inst : Category.{v, u} C
F_1 F' F'' : Functor.{v, w, u, w + 1} C (Type w)
G_1 G' F G H : Subfunctor F_1
h₁ : F ≤ H
h₂ : G ≤ H
U : C
x : F_1.obj U
h : x ∈ F.obj U
⊢ x ∈ H.obj U

Tactic:
h₁ _ h
-- Module: Mathlib.CategoryTheory.Subfunctor.Basic
Goal:
C : Type u
inst : Category.{v, u} C
F_1 F' F'' : Functor.{v, w, u, w + 1} C (Type w)
G_1 G' F G H : Subfunctor F_1
h₁ : F ≤ H
h₂ : G ≤ H
U : C
x : F_1.obj U
h : x ∈ F.obj U
⊢ x ∈ H.obj U

Tactic:
exact h₁ _ h
-- Module: Mathlib.CategoryTheory.Subfunctor.Basic
Goal:
C : Type u
inst : Category.{v, u} C
F_1 F' F'' : Functor.{v, w, u, w + 1} C (Type w)
G_1 G' F G H : Subfunctor F_1
h₁ : F ≤ H
h₂ : G ≤ H
U : C
x : F_1.obj U
h : x ∈ G.obj U
⊢ x ∈ H.obj U

Tactic:
h₂ _ h
-- Module: Mathlib.CategoryTheory.Subfunctor.Basic
Goal:
C : Type u
inst : Category.{v, u} C
F_1 F' F'' : Functor.{v, w, u, w + 1} C (Type w)
G_1 G' F G H : Subfunctor F_1
h₁ : F ≤ H
h₂ : G ≤ H
U : C
x : F_1.obj U
h : x ∈ G.obj U
⊢ x ∈ H.obj U

Tactic:
exact h₂ _ h
-- Module: Mathlib.CategoryTheory.Subfunctor.Basic
Goal:
C : Type u
inst : Category.{v, u} C
F F' F'' : Functor.{v, w, u, w + 1} C (Type w)
G G' : Subfunctor F
S : Set (Subfunctor F)
U V : C
f : U ⟶ V
x : F.obj U
hx : Membership.mem (γ := Set (F.obj U)) (sSup ((fun (T : Subfunctor F) ↦ T.obj U) '' S)) x
obtain :
  ∀ (F_1 : Subfunctor F) (h : F_1 ∈ S)
    (h' : Membership.mem (γ := Set (F.obj U)) ((fun (T : Subfunctor F) ↦ T.obj U) F_1) x),
    Membership.mem (γ := Set (F.obj U))
      (Set.preimage (β := (fun (X : Type w) ↦ X) (F.obj V))
        (⇑(hom (FC := TypeCat.Fun) (F.map f)) :
          (a : (fun (X : Type w) ↦ X) (F.obj U)) → (fun (X : Type w) ↦ X) (F.obj V))
        (sSup ((fun (T : Subfunctor F) ↦ T.obj V) '' S)))
      x
⊢ Membership.mem (γ := Set (F.obj U))
    (Set.preimage (β := (fun (X : Type w) ↦ X) (F.obj V))
      (⇑(hom (FC := TypeCat.Fun) (F.map f)) : (a : (fun (X : Type w) ↦ X) (F.obj U)) → (fun (X : Type w) ↦ X) (F.obj V))
      (sSup ((fun (T : Subfunctor F) ↦ T.obj V) '' S)))
    x

Tactic:
obtain ⟨_, ⟨F, h, rfl⟩, h'⟩ := hx

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Subfunctor.Basic
Goal:
C : Type u
inst : Category.{v, u} C
F_1 F' F'' : Functor.{v, w, u, w + 1} C (Type w)
G G' : Subfunctor F_1
S : Set (Subfunctor F_1)
U V : C
f : U ⟶ V
x : F_1.obj U
F : Subfunctor F_1
h : F ∈ S
h' : Membership.mem (γ := Set (F_1.obj U)) ((fun (T : Subfunctor F_1) ↦ T.obj U) F) x
simp :
  ∃ i ∈ S,
    Membership.mem (α := F_1.obj V) (i.obj V)
      ((hom (FC := TypeCat.Fun) (F_1.map f) : (a : F_1.obj U) → F_1.obj V) x : F_1.obj V)
⊢ Membership.mem (γ := Set (F_1.obj U))
    (Set.preimage (β := (fun (X : Type w) ↦ X) (F_1.obj V))
      (⇑(hom (FC := TypeCat.Fun) (F_1.map f)) :
        (a : (fun (X : Type w) ↦ X) (F_1.obj U)) → (fun (X : Type w) ↦ X) (F_1.obj V))
      (sSup ((fun (T : Subfunctor F_1) ↦ T.obj V) '' S)))
    x

Tactic:
simp only [Set.sSup_eq_sUnion, Set.sUnion_image, Set.preimage_iUnion,
          Set.mem_iUnion, Set.mem_preimage, exists_prop]

Premises used: Set.mem_iUnion, exists_prop, Set.sSup_eq_sUnion, Set.sUnion_image, Set.preimage_iUnion, Set.mem_preimage
-- Module: Mathlib.CategoryTheory.Subfunctor.Basic
Goal:
C : Type u
inst : Category.{v, u} C
F_1 F' F'' : Functor.{v, w, u, w + 1} C (Type w)
G G' : Subfunctor F_1
S : Set (Subfunctor F_1)
U V : C
f : U ⟶ V
x : F_1.obj U
F : Subfunctor F_1
h : F ∈ S
h' : Membership.mem (γ := Set (F_1.obj U)) ((fun (T : Subfunctor F_1) ↦ T.obj U) F) x
⊢ ∃ i ∈ S,
    Membership.mem (α := F_1.obj V) (i.obj V)
      ((hom (FC := TypeCat.Fun) (F_1.map f) : (a : F_1.obj U) → F_1.obj V) x : F_1.obj V)

Tactic:
⟨_, h, F.map f h'⟩

Premises used: CategoryTheory.Subfunctor.map, And.intro, Exists.intro
-- Module: Mathlib.CategoryTheory.Subfunctor.Basic
Goal:
C : Type u
inst : Category.{v, u} C
F_1 F' F'' : Functor.{v, w, u, w + 1} C (Type w)
G G' : Subfunctor F_1
S : Set (Subfunctor F_1)
U V : C
f : U ⟶ V
x : F_1.obj U
F : Subfunctor F_1
h : F ∈ S
h' : Membership.mem (γ := Set (F_1.obj U)) ((fun (T : Subfunctor F_1) ↦ T.obj U) F) x
⊢ ∃ i ∈ S,
    Membership.mem (α := F_1.obj V) (i.obj V)
      ((hom (FC := TypeCat.Fun) (F_1.map f) : (a : F_1.obj U) → F_1.obj V) x : F_1.obj V)

Tactic:
exact ⟨_, h, F.map f h'⟩
-- Module: Mathlib.CategoryTheory.Subfunctor.Basic
Goal:
C : Type u
inst : Category.{v, u} C
F F' F'' : Functor.{v, w, u, w + 1} C (Type w)
G G' : Subfunctor F
x : Set (Subfunctor F)
x_1 : Subfunctor F
h : x_1 ∈ x
x_2 : C
x_3 : F.obj x_2
⊢ x_3 ∈ x_1.obj x_2 →
    Membership.mem (γ := Set (F.obj x_2))
      (Subfunctor.obj { obj := fun (U : C) ↦ sSup ((fun (T : Subfunctor F) ↦ T.obj U) '' x), map := ⋯ } x_2) x_3

Tactic:
aesop
-- Module: Mathlib.CategoryTheory.Subfunctor.Basic
Goal:
C : Type u
inst : Category.{v, u} C
F F' F'' : Functor.{v, w, u, w + 1} C (Type w)
G G' : Subfunctor F
x : Set (Subfunctor F)
x_1 : Subfunctor F
h : x_1 ∈ upperBounds x
x_2 : C
⊢ Subfunctor.obj { obj := fun (U : C) ↦ sSup ((fun (T : Subfunctor F) ↦ T.obj U) '' x), map := ⋯ } x_2 ≤ x_1.obj x_2

Tactic:
aesop
-- Module: Mathlib.CategoryTheory.Subfunctor.Basic
Goal:
C : Type u
inst : Category.{v, u} C
F_1 F' F'' : Functor.{v, w, u, w + 1} C (Type w)
G G' : Subfunctor F_1
S : Set (Subfunctor F_1)
U V : C
f : U ⟶ V
x : F_1.obj U
hx : Membership.mem (γ := Set (F_1.obj U)) (sInf ((fun (T : Subfunctor F_1) ↦ T.obj U) '' S)) x
F : Subfunctor F_1
h : F ∈ S
⊢ Membership.mem (α := F_1.obj V) (γ := Set (F_1.obj V)) ((fun (T : Subfunctor F_1) ↦ T.obj V) F)
    ((hom (FC := TypeCat.Fun) (F_1.map f) :
          (a : (fun (X : Type w) ↦ X) (F_1.obj U)) → (fun (X : Type w) ↦ X) (F_1.obj V))
        x :
      (fun (X : Type w) ↦ X) (F_1.obj V))

Tactic:
F.map f (hx _ ⟨_, h, rfl⟩)

Premises used: Set.Mem, setOf, CategoryTheory.Subfunctor.map, Set.preimage, And.intro, Exists.intro, rfl
-- Module: Mathlib.CategoryTheory.Subfunctor.Basic
Goal:
C : Type u
inst : Category.{v, u} C
F_1 F' F'' : Functor.{v, w, u, w + 1} C (Type w)
G G' : Subfunctor F_1
S : Set (Subfunctor F_1)
U V : C
f : U ⟶ V
x : F_1.obj U
hx : Membership.mem (γ := Set (F_1.obj U)) (sInf ((fun (T : Subfunctor F_1) ↦ T.obj U) '' S)) x
F : Subfunctor F_1
h : F ∈ S
⊢ Membership.mem (α := F_1.obj V) (γ := Set (F_1.obj V)) ((fun (T : Subfunctor F_1) ↦ T.obj V) F)
    ((hom (FC := TypeCat.Fun) (F_1.map f) :
          (a : (fun (X : Type w) ↦ X) (F_1.obj U)) → (fun (X : Type w) ↦ X) (F_1.obj V))
        x :
      (fun (X : Type w) ↦ X) (F_1.obj V))

Tactic:
exact F.map f (hx _ ⟨_, h, rfl⟩)

Premises used: CategoryTheory.Subfunctor.map, And.intro, Exists.intro, rfl
-- Module: Mathlib.CategoryTheory.Subfunctor.Basic
Goal:
C : Type u
inst : Category.{v, u} C
F F' F'' : Functor.{v, w, u, w + 1} C (Type w)
G G' : Subfunctor F
x : Set (Subfunctor F)
x_1 : Subfunctor F
h : x_1 ∈ x
x_2 : C
x_3 : F.obj x_2
⊢ Membership.mem (γ := Set (F.obj x_2))
      (Subfunctor.obj { obj := fun (U : C) ↦ sInf ((fun (T : Subfunctor F) ↦ T.obj U) '' x), map := ⋯ } x_2) x_3 →
    x_3 ∈ x_1.obj x_2

Tactic:
aesop
-- Module: Mathlib.CategoryTheory.Subfunctor.Basic
Goal:
C : Type u
inst : Category.{v, u} C
F F' F'' : Functor.{v, w, u, w + 1} C (Type w)
G G' : Subfunctor F
x : Set (Subfunctor F)
x_1 : Subfunctor F
h : x_1 ∈ lowerBounds x
x_2 : C
⊢ x_1.obj x_2 ≤ Subfunctor.obj { obj := fun (U : C) ↦ sInf ((fun (T : Subfunctor F) ↦ T.obj U) '' x), map := ⋯ } x_2

Tactic:
aesop
-- Module: Mathlib.CategoryTheory.Subfunctor.Basic
Goal:
C : Type u
inst : Category.{v, u} C
F F' F'' : Functor.{v, w, u, w + 1} C (Type w)
G G' : Subfunctor F
⊢ ∀ {U V : C} (i : U ⟶ V),
    Subset (α := Set (F.obj U)) ⊤
      (Set.preimage (β := (fun (X : Type w) ↦ X) (F.obj V))
        (⇑(hom (FC := TypeCat.Fun) (F.map i)) :
          (a : (fun (X : Type w) ↦ X) (F.obj U)) → (fun (X : Type w) ↦ X) (F.obj V))
        ⊤)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Subfunctor.Basic
Goal:
C : Type u
inst : Category.{v, u} C
F F' F'' : Functor.{v, w, u, w + 1} C (Type w)
G G' : Subfunctor F
⊢ ∀ {U V : C} (i : U ⟶ V),
    Subset (α := Set (F.obj U)) ⊥
      (Set.preimage (β := (fun (X : Type w) ↦ X) (F.obj V))
        (⇑(hom (FC := TypeCat.Fun) (F.map i)) :
          (a : (fun (X : Type w) ↦ X) (F.obj U)) → (fun (X : Type w) ↦ X) (F.obj V))
        ⊥)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Subfunctor.Basic
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{v, w, u, w + 1} C (Type w)
S T : Subfunctor F
⊢ S ≤ T ↔ ∀ (U : C), S.obj U ≤ T.obj U

Tactic:
Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.CategoryTheory.Subfunctor.Basic
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{v, w, u, w + 1} C (Type w)
i : C
⊢ Eq.{w + 1} (α := Set (F.obj i)) (obj ⊤ i) ⊤

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Subfunctor.Basic
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{v, w, u, w + 1} C (Type w)
i : C
⊢ Eq.{w + 1} (α := Set (F.obj i)) (obj ⊥ i) ⊥

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Subfunctor.Basic
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{v, w, u, w + 1} C (Type w)
S : Set (Subfunctor F)
U : C
⊢ (sSup S).obj U = sSup ((fun (T : Subfunctor F) ↦ T.obj U) '' S)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Subfunctor.Basic
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{v, w, u, w + 1} C (Type w)
S : Set (Subfunctor F)
U : C
⊢ (sInf S).obj U = sInf ((fun (T : Subfunctor F) ↦ T.obj U) '' S)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Subfunctor.Basic
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{v, w, u, w + 1} C (Type w)
ι : Sort u_1
S : ι → Subfunctor F
U : C
⊢ Eq.{w + 1} (α := Set (F.obj U)) (obj (⨆ (i : ι), S i) U) (⋃ (i : ι), (S i).obj U)

Tactic:
simp [iSup, sSup_obj]

Premises used: iSup, CategoryTheory.Subfunctor.sSup_obj
-- Module: Mathlib.CategoryTheory.Subfunctor.Basic
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{v, w, u, w + 1} C (Type w)
ι : Sort u_1
S : ι → Subfunctor F
U : C
⊢ Eq.{w + 1} (α := Set (F.obj U)) (obj (⨅ (i : ι), S i) U) (⋂ (i : ι), (S i).obj U)

Tactic:
simp [iInf, sInf_obj]

Premises used: iInf, CategoryTheory.Subfunctor.sInf_obj
-- Module: Mathlib.CategoryTheory.Subfunctor.Basic
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{v, w, u, w + 1} C (Type w)
S T : Subfunctor F
i : C
⊢ (S ⊔ T).obj i = S.obj i ∪ T.obj i

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Subfunctor.Basic
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{v, w, u, w + 1} C (Type w)
S T : Subfunctor F
i : C
⊢ (S ⊓ T).obj i = S.obj i ∩ T.obj i

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Subfunctor.Basic
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{v, w, u, w + 1} C (Type w)
S₁ S₂ T : Subfunctor F
⊢ (S₁ ⊔ S₂) ⊓ T = S₁ ⊓ T ⊔ S₂ ⊓ T

Tactic:
aesop
-- Module: Mathlib.CategoryTheory.Subfunctor.Basic
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{v, w, u, w + 1} C (Type w)
ι : Sort u_1
S : ι → Subfunctor F
T : Subfunctor F
⊢ (⨆ (i : ι), S i) ⊓ T = ⨆ (i : ι), S i ⊓ T

Tactic:
aesop
-- Module: Mathlib.CategoryTheory.Subfunctor.Basic
Goal:
C : Type u
inst : Category.{v, u} C
F F' F'' : Functor.{v, w, u, w + 1} C (Type w)
G G' : Subfunctor F
⊢ Nonempty (Subfunctor F)

Tactic:
inferInstance

Premises used: inferInstance
-- Module: Mathlib.CategoryTheory.Subfunctor.Basic
Goal:
C : Type u
inst : Category.{v, u} C
F F' F'' : Functor.{v, w, u, w + 1} C (Type w)
G G' : Subfunctor F
⊢ Mono G.ι

Tactic:
⟨@fun _ _ _ e =>
    NatTrans.ext <| funext fun U => hom_ext _ _ fun x => Subtype.ext <| congr_hom (congr_app e U) x⟩

Premises used: CategoryTheory.NatTrans.ext, funext, CategoryTheory.Mono.mk, CategoryTheory.ConcreteCategory.hom_ext, CategoryTheory.NatTrans.app
-- Module: Mathlib.CategoryTheory.Subfunctor.Basic
Goal:
C : Type u
inst : Category.{v, u} C
F F' F'' : Functor.{v, w, u, w + 1} C (Type w)
G_1 G'_1 G G' : Subfunctor F
h : G ≤ G'
Z : Functor.{v, w, u, w + 1} C (Type w)
x_1 x_2 : Z ⟶ G.toFunctor
e : x_1 ≫ homOfLe h = x_2 ≫ homOfLe h
U : C
x : Z.obj U
⊢ Eq (α := G.toFunctor.obj U)
    ((hom (FC := TypeCat.Fun) (x_1.app U) : (a : Z.obj U) → G.toFunctor.obj U) x : G.toFunctor.obj U)
    ((hom (FC := TypeCat.Fun) (x_2.app U) : (a : Z.obj U) → G.toFunctor.obj U) x : G.toFunctor.obj U)

Tactic:
Subtype.ext (congr_arg Subtype.val <| (congr_hom (congr_app e U) x) :)

Premises used: congr_arg, CategoryTheory.ConcreteCategory.congr_hom, Subtype.val, CategoryTheory.congr_app, Subtype.ext
-- Module: Mathlib.CategoryTheory.Subfunctor.Basic
Goal:
C : Type u
inst : Category.{v, u} C
F F' F'' : Functor.{v, w, u, w + 1} C (Type w)
G_1 G'_1 G G' : Subfunctor F
h : G ≤ G'
Z : Functor.{v, w, u, w + 1} C (Type w)
x_1 x_2 : Z ⟶ G.toFunctor
e : x_1 ≫ homOfLe h = x_2 ≫ homOfLe h
U : C
x : Z.obj U
⊢ Eq (α := G.toFunctor.obj U)
    ((hom (FC := TypeCat.Fun) (x_1.app U) : (a : Z.obj U) → G.toFunctor.obj U) x : G.toFunctor.obj U)
    ((hom (FC := TypeCat.Fun) (x_2.app U) : (a : Z.obj U) → G.toFunctor.obj U) x : G.toFunctor.obj U)

Tactic:
exact Subtype.ext (congr_arg Subtype.val <| (congr_hom (congr_app e U) x) :)

Premises used: congr_arg, CategoryTheory.ConcreteCategory.congr_hom, Subtype.val, CategoryTheory.congr_app, Subtype.ext
-- Module: Mathlib.CategoryTheory.Subfunctor.Basic
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{v, w, u, w + 1} C (Type w)
G G' : Subfunctor F
h : G ≤ G'
w :
  ∀ (x : C) (x_1 : G.toFunctor.obj x),
    (hom (FC := TypeCat.Fun) ((homOfLe h ≫ G'.ι).app x)).toFun x_1 = (hom (FC := TypeCat.Fun) (G.ι.app x)).toFun x_1
⊢ homOfLe h ≫ G'.ι = G.ι

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Subfunctor.Basic
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{v, w, u, w + 1} C (Type w)
G G' : Subfunctor F
h : G ≤ G'
x : C
x_1 : G.toFunctor.obj x
⊢ (hom (FC := TypeCat.Fun) ((homOfLe h ≫ G'.ι).app x)).toFun x_1 = (hom (FC := TypeCat.Fun) (G.ι.app x)).toFun x_1

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Subfunctor.Basic
Goal:
C : Type u
inst : Category.{v, u} C
F F' F'' : Functor.{v, w, u, w + 1} C (Type w)
G G' : Subfunctor F
⊢ IsIso (C := Functor.{v, w, u, w + 1} C (Type w)) (X := toFunctor (F := F) ⊤) (ι ⊤)

Tactic:
@NatIso.isIso_of_isIso_app _ _ _ _ _ _ _ ?_

Premises used: CategoryTheory.NatIso.isIso_of_isIso_app
-- Module: Mathlib.CategoryTheory.Subfunctor.Basic
Goal:
C : Type u
inst : Category.{v, u} C
F F' F'' : Functor.{v, w, u, w + 1} C (Type w)
G G' : Subfunctor F
refine : ∀ (X : C), IsIso.{w, w + 1} (X := Functor.obj.{v, w, u, w + 1} (toFunctor (F := F) ⊤) X) (NatTrans.app (ι ⊤) X)
⊢ IsIso (C := Functor.{v, w, u, w + 1} C (Type w)) (X := toFunctor (F := F) ⊤) (ι ⊤)

Tactic:
refine @NatIso.isIso_of_isIso_app _ _ _ _ _ _ _ ?_

Premises used: CategoryTheory.NatIso.isIso_of_isIso_app
-- Module: Mathlib.CategoryTheory.Subfunctor.Basic
Goal:
C : Type u
inst : Category.{v, u} C
F F' F'' : Functor.{v, w, u, w + 1} C (Type w)
G G' : Subfunctor F
X : C
rw :
  Function.Bijective (α := (fun (X : Type w) ↦ X) (Functor.obj.{v, w, u, w + 1} (toFunctor (F := F) ⊤) X)) (β :=
    (fun (X : Type w) ↦ X) (F.obj X))
    (⇑(hom (FC := TypeCat.Fun) (NatTrans.app (ι ⊤) X)) :
      (a : (fun (X : Type w) ↦ X) (⊤.toFunctor.obj X)) → (fun (X : Type w) ↦ X) (F.obj X))
⊢ IsIso.{w, w + 1} (X := Functor.obj.{v, w, u, w + 1} (toFunctor (F := F) ⊤) X) (NatTrans.app (ι ⊤) X)

Tactic:
rw [isIso_iff_bijective]

Premises used: CategoryTheory.isIso_iff_bijective
-- Module: Mathlib.CategoryTheory.Subfunctor.Basic
Goal:
C : Type u
inst : Category.{v, u} C
F F' F'' : Functor.{v, w, u, w + 1} C (Type w)
G G' : Subfunctor F
X : C
⊢ Function.Bijective (α := (fun (X : Type w) ↦ X) (Functor.obj.{v, w, u, w + 1} (toFunctor (F := F) ⊤) X)) (β :=
    (fun (X : Type w) ↦ X) (F.obj X))
    (⇑(hom (FC := TypeCat.Fun) (NatTrans.app (ι ⊤) X)) :
      (a : (fun (X : Type w) ↦ X) (⊤.toFunctor.obj X)) → (fun (X : Type w) ↦ X) (F.obj X))

Tactic:
⟨Subtype.coe_injective, fun x => ⟨⟨x, _root_.trivial⟩, rfl⟩⟩

Premises used: trivial, Subtype.coe_injective, Subtype.mk, And.intro, Exists.intro, Function.Bijective, rfl
-- Module: Mathlib.CategoryTheory.Subfunctor.Basic
Goal:
C : Type u
inst : Category.{v, u} C
F F' F'' : Functor.{v, w, u, w + 1} C (Type w)
G G' : Subfunctor F
X : C
⊢ Function.Bijective (α := (fun (X : Type w) ↦ X) (Functor.obj.{v, w, u, w + 1} (toFunctor (F := F) ⊤) X)) (β :=
    (fun (X : Type w) ↦ X) (F.obj X))
    (⇑(hom (FC := TypeCat.Fun) (NatTrans.app (ι ⊤) X)) :
      (a : (fun (X : Type w) ↦ X) (⊤.toFunctor.obj X)) → (fun (X : Type w) ↦ X) (F.obj X))

Tactic:
exact ⟨Subtype.coe_injective, fun x => ⟨⟨x, _root_.trivial⟩, rfl⟩⟩
-- Module: Mathlib.CategoryTheory.Subfunctor.Basic
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{v, w, u, w + 1} C (Type w)
G : Subfunctor F
mp : G = ⊤ → IsIso G.ι
mpr : IsIso G.ι → G = ⊤
⊢ G = ⊤ ↔ IsIso G.ι

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.Subfunctor.Basic
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{v, w, u, w + 1} C (Type w)
⊢ IsIso (C := Functor.{v, w, u, w + 1} C (Type w)) (X := toFunctor (F := F) ⊤) (ι ⊤)

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Subfunctor.Basic
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{v, w, u, w + 1} C (Type w)
G : Subfunctor F
H : IsIso G.ι
mpr : ∀ (U : C) (x : F.obj U), x ∈ G.obj U ↔ Membership.mem (γ := Set (F.obj U)) (obj ⊤ U) x
⊢ G = ⊤

Tactic:
ext U x
-- Module: Mathlib.CategoryTheory.Subfunctor.Basic
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{v, w, u, w + 1} C (Type w)
G : Subfunctor F
H : IsIso G.ι
U : C
x : F.obj U
mpr : x ∈ G.obj U
⊢ x ∈ G.obj U ↔ Membership.mem (γ := Set (F.obj U)) (obj ⊤ U) x

Tactic:
apply (iff_of_eq (iff_true _)).mpr

Premises used: Iff.mpr, iff_true, iff_of_eq
-- Module: Mathlib.CategoryTheory.Subfunctor.Basic
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{v, w, u, w + 1} C (Type w)
G : Subfunctor F
H : IsIso G.ι
U : C
x : F.obj U
mpr :
  Membership.mem (α := F.obj U) (G.obj U)
    ((hom (FC := TypeCat.Fun) (G.ι.app U) : (a : G.toFunctor.obj U) → F.obj U)
        ((hom (FC := TypeCat.Fun) (inv (G.ι.app U)) : (a : F.obj U) → G.toFunctor.obj U) x : G.toFunctor.obj U) :
      F.obj U)
⊢ x ∈ G.obj U

Tactic:
rw [← IsIso.inv_hom_id_apply (G.ι.app U) x]

Premises used: CategoryTheory.Subfunctor.ι, CategoryTheory.IsIso.inv_hom_id_apply, CategoryTheory.NatTrans.app
-- Module: Mathlib.CategoryTheory.Subfunctor.Basic
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{v, w, u, w + 1} C (Type w)
G : Subfunctor F
H : IsIso G.ι
U : C
x : F.obj U
⊢ Membership.mem (α := F.obj U) (G.obj U)
    ((hom (FC := TypeCat.Fun) (G.ι.app U) : (a : G.toFunctor.obj U) → F.obj U)
        ((hom (FC := TypeCat.Fun) (inv (G.ι.app U)) : (a : F.obj U) → G.toFunctor.obj U) x : G.toFunctor.obj U) :
      F.obj U)

Tactic:
((inv (G.ι.app U)) x).2

Premises used: CategoryTheory.ConcreteCategory.hom, Set.Mem, CategoryTheory.Subfunctor.ι, CategoryTheory.inv, DFunLike.coe, CategoryTheory.NatTrans.app, Subtype.property
-- Module: Mathlib.CategoryTheory.Subfunctor.Basic
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{v, w, u, w + 1} C (Type w)
G : Subfunctor F
H : IsIso G.ι
U : C
x : F.obj U
⊢ Membership.mem (α := F.obj U) (G.obj U)
    ((hom (FC := TypeCat.Fun) (G.ι.app U) : (a : G.toFunctor.obj U) → F.obj U)
        ((hom (FC := TypeCat.Fun) (inv (G.ι.app U)) : (a : F.obj U) → G.toFunctor.obj U) x : G.toFunctor.obj U) :
      F.obj U)

Tactic:
exact ((inv (G.ι.app U)) x).2

Premises used: CategoryTheory.ConcreteCategory.hom, CategoryTheory.Subfunctor.ι, CategoryTheory.inv, DFunLike.coe, CategoryTheory.NatTrans.app, Subtype.property
-- Module: Mathlib.CategoryTheory.Subfunctor.Basic
Goal:
C : Type u
inst : Category.{v, u} C
F F' : Functor.{v, w, u, w + 1} C (Type w)
G : Subfunctor F
f : F' ⟶ G.toFunctor
U V : C
i : U ⟶ V
x : F'.obj U
⊢ Eq (α := F.obj V)
    ((↑((hom (FC := TypeCat.Fun) (f.app V) :
              (a : (fun (X : Type w) ↦ X) (F'.obj V)) → (fun (X : Type w) ↦ X) (G.toFunctor.obj V))
            ((hom (FC := TypeCat.Fun) (F'.map i) :
                (a : (fun (X : Type w) ↦ X) (F'.obj U)) → (fun (X : Type w) ↦ X) (F'.obj V))
              x)) :
        F.obj V) :
      F.obj V)
    ((hom (FC := TypeCat.Fun) (F.map i) : (a : (fun (X : Type w) ↦ X) (F.obj U)) → (fun (X : Type w) ↦ X) (F.obj V))
        (↑((hom (FC := TypeCat.Fun) (f.app U) :
                (a : (fun (X : Type w) ↦ X) (F'.obj U)) → (fun (X : Type w) ↦ X) (G.toFunctor.obj U))
              x) :
          F.obj U) :
      (fun (X : Type w) ↦ X) (F.obj V))

Tactic:
congrArg Subtype.val (NatTrans.naturality_apply f i x)

Premises used: CategoryTheory.NatTrans.naturality_apply, congrArg, Subtype.val
-- Module: Mathlib.CategoryTheory.Subfunctor.Equalizer
Goal:
C : Type u
inst : Category.{v, u} C
F₁ F₂ : Functor.{v, w, u, w + 1} C (Type w)
A : Subfunctor F₁
f g : A.toFunctor ⟶ F₂
U V : C
φ : U ⟶ V
x : F₁.obj U
hx : x ∈ A.obj U
h :
  Eq (α := (fun (X : Type w) ↦ X) (F₂.obj U))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app U) :
          (a : (fun (X : Type w) ↦ X) (A.toFunctor.obj U)) → (fun (X : Type w) ↦ X) (F₂.obj U))
        (Subtype.mk (p := fun (x : F₁.obj U) ↦ x ∈ A.obj U) x hx) :
      (fun (X : Type w) ↦ X) (F₂.obj U))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (g.app U) :
          (a : (fun (X : Type w) ↦ X) (A.toFunctor.obj U)) → (fun (X : Type w) ↦ X) (F₂.obj U))
        (Subtype.mk (p := fun (x : F₁.obj U) ↦ x ∈ A.obj U) x hx) :
      (fun (X : Type w) ↦ X) (F₂.obj U))
rw rw₁ :
  Eq (α := F₂.obj V)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F₂.map φ) : (a : F₂.obj U) → F₂.obj V)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (g.app U) :
              (a : (fun (X : Type w) ↦ X) (A.toFunctor.obj U)) → (fun (X : Type w) ↦ X) (F₂.obj U))
            (Subtype.mk (p := fun (x : F₁.obj U) ↦ x ∈ A.obj U) x hx) :
          (fun (X : Type w) ↦ X) (F₂.obj U)) :
      F₂.obj V)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F₂.map φ) : (a : F₂.obj U) → F₂.obj V)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (g.app U) : (a : A.toFunctor.obj U) → F₂.obj U)
            (Subtype.mk (p := fun (x : F₁.obj U) ↦ x ∈ A.obj U) x hx) :
          F₂.obj U) :
      F₂.obj V)
⊢ Eq (α := F₂.obj V)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F₂.map φ) : (a : F₂.obj U) → F₂.obj V)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app U) : (a : A.toFunctor.obj U) → F₂.obj U)
            (Subtype.mk (p := fun (x : F₁.obj U) ↦ x ∈ A.obj U) x hx) :
          F₂.obj U) :
      F₂.obj V)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F₂.map φ) : (a : F₂.obj U) → F₂.obj V)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (g.app U) : (a : A.toFunctor.obj U) → F₂.obj U)
            (Subtype.mk (p := fun (x : F₁.obj U) ↦ x ∈ A.obj U) x hx) :
          F₂.obj U) :
      F₂.obj V)

Tactic:
rw [h]