awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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))
⊢ Membership.mem (γ := Set (F₁.obj U))
    (Set.preimage (β := (fun (X : Type w) ↦ X) (F₁.obj V))
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F₁.map φ)) :
        (a : (fun (X : Type w) ↦ X) (F₁.obj U)) → (fun (X : Type w) ↦ X) (F₁.obj V))
      {x : F₁.obj V |
        ∃ (hx : x ∈ A.obj V),
          Eq (α := (fun (X : Type w) ↦ X) (F₂.obj V))
            ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app V) :
                  (a : (fun (X : Type w) ↦ X) (A.toFunctor.obj V)) → (fun (X : Type w) ↦ X) (F₂.obj V))
                (Subtype.mk (p := fun (x : F₁.obj V) ↦ x ∈ A.obj V) x hx) :
              (fun (X : Type w) ↦ X) (F₂.obj V))
            ((ConcreteCategory.hom (FC := TypeCat.Fun) (g.app V) :
                  (a : (fun (X : Type w) ↦ X) (A.toFunctor.obj V)) → (fun (X : Type w) ↦ X) (F₂.obj V))
                (Subtype.mk (p := fun (x : F₁.obj V) ↦ x ∈ A.obj V) x hx) :
              (fun (X : Type w) ↦ X) (F₂.obj V))})
    x

Tactic:
exact ⟨A.map _ hx,
      (NatTrans.naturality_apply f φ ⟨x, hx⟩).trans (Eq.trans (by rw [h])
        (NatTrans.naturality_apply g φ ⟨x, hx⟩).symm)⟩
-- 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₂
⊢ Subfunctor.equalizer f g ≤ A

Tactic:
fun _ _ h ↦ h.1

Premises used: Set.Subset
-- 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 : A.toFunctor ⟶ F₂
⊢ Subfunctor.equalizer f f = A

Tactic:
aesop
-- 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₂
i : C
x : A.toFunctor.obj i
⊢ (↑x : F₁.obj i) ∈ (Subfunctor.equalizer f g).obj i ↔
    Eq (α := (fun (X : Type w) ↦ X) (F₂.obj i))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app i) :
            (a : (fun (X : Type w) ↦ X) (A.toFunctor.obj i)) → (fun (X : Type w) ↦ X) (F₂.obj i))
          x :
        (fun (X : Type w) ↦ X) (F₂.obj i))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (g.app i) :
            (a : (fun (X : Type w) ↦ X) (A.toFunctor.obj i)) → (fun (X : Type w) ↦ X) (F₂.obj i))
          x :
        (fun (X : Type w) ↦ X) (F₂.obj i))

Tactic:
simp
-- 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₂
G : Functor.{v, w, u, w + 1} C (Type w)
φ : G ⟶ A.toFunctor
rw : range (φ ≫ A.ι) ≤ Subfunctor.equalizer f g ↔ (φ ≫ f).app = (φ ≫ g).app
⊢ range (φ ≫ A.ι) ≤ Subfunctor.equalizer f g ↔ φ ≫ f = φ ≫ g

Tactic:
rw [NatTrans.ext_iff]

Premises used: CategoryTheory.NatTrans.ext_iff
-- 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₂
G : Functor.{v, w, u, w + 1} C (Type w)
φ : G ⟶ A.toFunctor
⊢ range (φ ≫ A.ι) ≤ Subfunctor.equalizer f g ↔ (φ ≫ f).app = (φ ≫ g).app

Tactic:
simp [le_def, Set.subset_def, ConcreteCategory.hom_ext_iff, funext_iff]

Premises used: Set.subset_def, funext_iff, CategoryTheory.Subfunctor.le_def, CategoryTheory.ConcreteCategory.hom_ext_iff
-- 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₂
⊢ range (𝟙 A.toFunctor ≫ A.ι) ≤ Subfunctor.equalizer f g ↔ 𝟙 A.toFunctor ≫ f = 𝟙 A.toFunctor ≫ g

Tactic:
have := range_le_equalizer_iff f g (𝟙 _)
-- 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₂
this : range (𝟙 A.toFunctor ≫ A.ι) ≤ Subfunctor.equalizer f g ↔ 𝟙 A.toFunctor ≫ f = 𝟙 A.toFunctor ≫ g
⊢ A ≤ Subfunctor.equalizer f g ↔ f = g

Tactic:
simp only [Category.id_comp, range_ι] at this

Premises used: CategoryTheory.Subfunctor.range_ι, CategoryTheory.Category.id_comp
-- 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₂
this : A ≤ Subfunctor.equalizer f g ↔ f = g
rw : Subfunctor.equalizer f g = A ↔ A ≤ Subfunctor.equalizer f g
⊢ Subfunctor.equalizer f g = A ↔ f = g

Tactic:
rw [← this]
-- 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₂
this : A ≤ Subfunctor.equalizer f g ↔ f = g
mp : Subfunctor.equalizer f g = A → A ≤ Subfunctor.equalizer f g
mpr : A ≤ Subfunctor.equalizer f g → Subfunctor.equalizer f g = A
⊢ Subfunctor.equalizer f g = A ↔ A ≤ Subfunctor.equalizer f g

Tactic:
constructor
-- 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₂
this : A ≤ Subfunctor.equalizer f g ↔ f = g
h : Subfunctor.equalizer f g = A
mp mp₁ : A ≤ A
⊢ A ≤ Subfunctor.equalizer f g

Tactic:
rw [h]
-- 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₂
this : A ≤ Subfunctor.equalizer f g ↔ f = g
h : A ≤ Subfunctor.equalizer f g
⊢ Subfunctor.equalizer f g = A

Tactic:
le_antisymm (equalizer_le f g) h

Premises used: CategoryTheory.Subfunctor.equalizer_le, le_antisymm
-- 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₂
this : A ≤ Subfunctor.equalizer f g ↔ f = g
h : A ≤ Subfunctor.equalizer f g
⊢ Subfunctor.equalizer f g = A

Tactic:
exact le_antisymm (equalizer_le f g) h

Premises used: CategoryTheory.Subfunctor.equalizer_le, le_antisymm
-- 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₂
⊢ Mono (homOfLe ⋯)

Tactic:
infer_instance
-- 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₂
⊢ ι f g ≫ A.ι = (Subfunctor.equalizer f g).ι

Tactic:
rfl

Premises used: CategoryTheory.NatTrans.vcomp, Set.Mem, setOf, TypeCat.Fun.comp, CategoryTheory.Subfunctor.ι, rfl
-- 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₂
⊢ ι f g ≫ f = ι f g ≫ g

Tactic:
simp [← range_le_equalizer_iff]

Premises used: CategoryTheory.Subfunctor.range_le_equalizer_iff
-- 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₂
G : Functor.{v, w, u, w + 1} C (Type w)
φ : G ⟶ A.toFunctor
w : φ ≫ f = φ ≫ g
⊢ range (φ ≫ A.ι) ≤ Subfunctor.equalizer f g

Tactic:
simpa only [range_le_equalizer_iff] using w

Premises used: CategoryTheory.Subfunctor.range_le_equalizer_iff
-- 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₂
G : Functor.{v, w, u, w + 1} C (Type w)
φ : G ⟶ A.toFunctor
w : φ ≫ f = φ ≫ g
⊢ lift f g φ w ≫ (Subfunctor.equalizer f g).ι = φ ≫ A.ι

Tactic:
rfl

Premises used: CategoryTheory.NatTrans.vcomp, CategoryTheory.Subfunctor.equalizer.lift, Set.Mem, setOf, CategoryTheory.Subfunctor.equalizer, TypeCat.Fun.comp, CategoryTheory.Subfunctor.toFunctor, CategoryTheory.Subfunctor.lift, rfl
-- 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₂
G : Functor.{v, w, u, w + 1} C (Type w)
φ : G ⟶ A.toFunctor
w : φ ≫ f = φ ≫ g
⊢ lift f g φ w ≫ ι f g = φ

Tactic:
rfl

Premises used: CategoryTheory.NatTrans.vcomp, Set.Mem, setOf, TypeCat.Fun.comp, rfl
-- 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₂
⊢ (fork f g).ι = ι f g

Tactic:
rfl

Premises used: CategoryTheory.Subfunctor.homOfLe, CategoryTheory.Subfunctor.equalizer.ι, CategoryTheory.Limits.Fork.ι, rfl
-- 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₂
s : Limits.Fork f g
⊢ (fun (s : Limits.Fork f g) ↦ lift f g s.ι ⋯) s ≫ (fork f g).ι = s.ι

Tactic:
dsimp
-- 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₂
s : Limits.Fork f g
m : s.pt ⟶ (fork f g).pt
hm : m ≫ (fork f g).ι = s.ι
⊢ m = (fun (s : Limits.Fork f g) ↦ lift f g s.ι ⋯) s

Tactic:
simp [← cancel_mono (Subfunctor.equalizer f g).ι, ← hm]

Premises used: CategoryTheory.Subfunctor.equalizer, CategoryTheory.cancel_mono, CategoryTheory.Subfunctor.ι
-- Module: Mathlib.CategoryTheory.Subfunctor.Finite
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
G : Subfunctor F
ι : Type w'
X : ι → Cᵒᵖ
x : (i : ι) → F.obj (X i)
⊢ G.IsGeneratedBy x ↔ ⨆ (i : ι), ofSection (x i) = G

Tactic:
Iff.rfl

Premises used: Iff.rfl, CategoryTheory.Subfunctor.IsGeneratedBy
-- Module: Mathlib.CategoryTheory.Subfunctor.Finite
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
G : Subfunctor F
ι : Type w'
X : ι → Cᵒᵖ
x : (i : ι) → F.obj (X i)
h : G.IsGeneratedBy x
⊢ ⨆ (i : ι), ofSection (x i) = G

Tactic:
h

Premises used: CategoryTheory.Subfunctor.IsGeneratedBy
-- Module: Mathlib.CategoryTheory.Subfunctor.Finite
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
G : Subfunctor F
ι : Type w'
X : ι → Cᵒᵖ
x : (i : ι) → F.obj (X i)
h : G.IsGeneratedBy x
i : ι
rw : ofSection (x i) ≤ ⨆ (i : ι), ofSection (x i)
⊢ ofSection (x i) ≤ G

Tactic:
rw [← h.iSup_eq]

Premises used: CategoryTheory.Subfunctor.IsGeneratedBy.iSup_eq
-- Module: Mathlib.CategoryTheory.Subfunctor.Finite
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
G : Subfunctor F
ι : Type w'
X : ι → Cᵒᵖ
x : (i : ι) → F.obj (X i)
h : G.IsGeneratedBy x
i : ι
⊢ ofSection (x i) ≤ ⨆ (i : ι), ofSection (x i)

Tactic:
le_iSup (fun i ↦ ofSection (x i)) i

Premises used: le_iSup, CategoryTheory.Subfunctor.ofSection
-- Module: Mathlib.CategoryTheory.Subfunctor.Finite
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
G : Subfunctor F
ι : Type w'
X : ι → Cᵒᵖ
x : (i : ι) → F.obj (X i)
h : G.IsGeneratedBy x
i : ι
⊢ ofSection (x i) ≤ ⨆ (i : ι), ofSection (x i)

Tactic:
exact le_iSup (fun i ↦ ofSection (x i)) i

Premises used: le_iSup, CategoryTheory.Subfunctor.ofSection
-- Module: Mathlib.CategoryTheory.Subfunctor.Finite
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
G : Subfunctor F
ι : Type w'
X : ι → Cᵒᵖ
x : (i : ι) → F.obj (X i)
h : G.IsGeneratedBy x
i : ι
rw : ofSection (x i) ≤ G
⊢ Membership.mem (γ := Set (F.obj (X i))) (G.obj (X i)) (x i)

Tactic:
rw [← ofSection_le_iff]

Premises used: CategoryTheory.Subfunctor.ofSection_le_iff
-- Module: Mathlib.CategoryTheory.Subfunctor.Finite
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
G : Subfunctor F
ι : Type w'
X : ι → Cᵒᵖ
x : (i : ι) → F.obj (X i)
h : G.IsGeneratedBy x
i : ι
⊢ ofSection (x i) ≤ G

Tactic:
h.ofSection_le i

Premises used: CategoryTheory.Subfunctor.IsGeneratedBy.ofSection_le
-- Module: Mathlib.CategoryTheory.Subfunctor.Finite
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
G : Subfunctor F
ι : Type w'
X : ι → Cᵒᵖ
x : (i : ι) → F.obj (X i)
h : G.IsGeneratedBy x
i : ι
⊢ ofSection (x i) ≤ G

Tactic:
exact h.ofSection_le i

Premises used: CategoryTheory.Subfunctor.IsGeneratedBy.ofSection_le
-- Module: Mathlib.CategoryTheory.Subfunctor.Finite
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
G : Subfunctor F
ι : Type w'
X : ι → Cᵒᵖ
x : (i : ι) → F.obj (X i)
h : G.IsGeneratedBy x
ι' : Type w''
e : ι' ≃ ι
rw :
  Eq (α := Subfunctor F) (⨆ (i : ι'), ofSection (X := X ((e : (a : ι') → ι) i)) (x ((e : (a : ι') → ι) i)))
    (⨆ (i : ι), ofSection (x i))
⊢ G.IsGeneratedBy (X := fun (i' : ι') ↦ X ((e : (a : ι') → ι) i')) fun (i' : ι') ↦ x ((e : (a : ι') → ι) i')

Tactic:
rw [isGeneratedBy_iff, ← h.iSup_eq]

Premises used: CategoryTheory.Subfunctor.isGeneratedBy_iff, CategoryTheory.Subfunctor.IsGeneratedBy.iSup_eq
-- Module: Mathlib.CategoryTheory.Subfunctor.Finite
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
G : Subfunctor F
ι : Type w'
X : ι → Cᵒᵖ
x : (i : ι) → F.obj (X i)
h : G.IsGeneratedBy x
ι' : Type w''
e : ι' ≃ ι
⊢ Eq (α := Subfunctor F) (⨆ (i : ι'), ofSection (X := X ((e : (a : ι') → ι) i)) (x ((e : (a : ι') → ι) i)))
    (⨆ (i : ι), ofSection (x i))

Tactic:
Equiv.iSup_congr e (congrFun rfl)

Premises used: congrFun, Equiv.iSup_congr, rfl
-- Module: Mathlib.CategoryTheory.Subfunctor.Finite
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
G : Subfunctor F
ι : Type w'
X : ι → Cᵒᵖ
x : (i : ι) → F.obj (X i)
h : G.IsGeneratedBy x
ι' : Type w''
e : ι' ≃ ι
⊢ Eq (α := Subfunctor F) (⨆ (i : ι'), ofSection (X := X ((e : (a : ι') → ι) i)) (x ((e : (a : ι') → ι) i)))
    (⨆ (i : ι), ofSection (x i))

Tactic:
exact Equiv.iSup_congr e (congrFun rfl)

Premises used: congrFun, Equiv.iSup_congr, rfl
-- Module: Mathlib.CategoryTheory.Subfunctor.Finite
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
G : Subfunctor F
ι : Type w'
X : ι → Cᵒᵖ
x : (i : ι) → F.obj (X i)
h : G.IsGeneratedBy x
F' : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
f : F ⟶ F'
⊢ (G.image f).IsGeneratedBy (X := X) fun (i : ι) ↦
    (ConcreteCategory.hom (FC := TypeCat.Fun) (f.app (X i)) :
        (a : (fun (X : Type w) ↦ X) (F.obj (X i))) → (fun (X : Type w) ↦ X) (F'.obj (X i)))
      (x i)

Tactic:
simp only [isGeneratedBy_iff, ← h.iSup_eq, image_iSup, ofSection_image]

Premises used: CategoryTheory.Subfunctor.isGeneratedBy_iff, CategoryTheory.Subfunctor.IsGeneratedBy.iSup_eq, CategoryTheory.Subfunctor.ofSection_image, CategoryTheory.Subfunctor.image_iSup
-- Module: Mathlib.CategoryTheory.Subfunctor.Finite
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
G : Subfunctor F
hG : G.IsFinite
⊢ Finite (Index G)

Tactic:
hG.exists_isGeneratedBy.choose_spec.choose

Premises used: Exists.choose_spec, CategoryTheory.Subfunctor.IsFinite.Index, CategoryTheory.Subfunctor.IsFinite.exists_isGeneratedBy, Exists.choose
-- Module: Mathlib.CategoryTheory.Subfunctor.Finite
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
G : Subfunctor F
hG : G.IsFinite
⊢ G.IsGeneratedBy (ι := IsFinite.Index G) IsFinite.x

Tactic:
hG.exists_isGeneratedBy.choose_spec.choose_spec.choose_spec.choose_spec.some

Premises used: Exists.choose_spec, CategoryTheory.Subfunctor.IsFinite.x, Nonempty.some, CategoryTheory.Subfunctor.IsFinite.Index, CategoryTheory.Subfunctor.IsFinite.exists_isGeneratedBy, CategoryTheory.Subfunctor.IsFinite.X
-- Module: Mathlib.CategoryTheory.Subfunctor.Finite
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
G : Subfunctor F
ι : Type w'
inst_1 : Finite ι
X : ι → Cᵒᵖ
x : (i : ι) → F.obj (X i)
h : G.IsGeneratedBy x
obtain : ∀ (n : ℕ) (e : ι ≃ Fin n), G.IsFinite
⊢ G.IsFinite

Tactic:
obtain ⟨n, ⟨e⟩⟩ := Finite.exists_equiv_fin ι

Premises used: Finite.exists_equiv_fin
-- Module: Mathlib.CategoryTheory.Subfunctor.Finite
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
G : Subfunctor F
ι : Type w'
inst_1 : Finite ι
X : ι → Cᵒᵖ
x : (i : ι) → F.obj (X i)
h : G.IsGeneratedBy x
n : ℕ
e : ι ≃ Fin n
⊢ G.IsFinite

Tactic:
⟨Fin n, inferInstance, _, _, ⟨h.of_equiv e.symm⟩⟩

Premises used: CategoryTheory.Subfunctor.IsFinite.mk, inferInstance, Nonempty.intro, CategoryTheory.Subfunctor.IsGeneratedBy.of_equiv, Exists.intro, Equiv.symm, Fin
-- Module: Mathlib.CategoryTheory.Subfunctor.Finite
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
G : Subfunctor F
ι : Type w'
inst_1 : Finite ι
X : ι → Cᵒᵖ
x : (i : ι) → F.obj (X i)
h : G.IsGeneratedBy x
n : ℕ
e : ι ≃ Fin n
⊢ G.IsFinite

Tactic:
exact ⟨Fin n, inferInstance, _, _, ⟨h.of_equiv e.symm⟩⟩
-- Module: Mathlib.CategoryTheory.Subfunctor.Finite
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
G : Subfunctor F
inst_1 : G.IsFinite
F' : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
f : F ⟶ F'
⊢ (G.image f).IsFinite

Tactic:
((isGeneratedBy_of_isFinite G).image f).isFinite

Premises used: CategoryTheory.Subfunctor.isGeneratedBy_of_isFinite, CategoryTheory.Subfunctor.IsGeneratedBy.image, CategoryTheory.Subfunctor.IsGeneratedBy.isFinite
-- Module: Mathlib.CategoryTheory.Subfunctor.Finite
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
ι : Type w'
X : ι → Cᵒᵖ
x : (i : ι) → F.obj (X i)
h : PresheafIsGeneratedBy F x
F' : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
f : F ⟶ F'
⊢ (Subfunctor.range f).IsGeneratedBy (X := X) fun (i : ι) ↦
    (ConcreteCategory.hom (FC := TypeCat.Fun) (f.app (X i)) :
        (a : (fun (X : Type w) ↦ X) (F.obj (X i))) → (fun (X : Type w) ↦ X) (F'.obj (X i)))
      (x i)

Tactic:
simpa only [← Subfunctor.image_top] using h.image f

Premises used: CategoryTheory.Subfunctor.image_top, CategoryTheory.Subfunctor.IsGeneratedBy.image
-- Module: Mathlib.CategoryTheory.Subfunctor.Finite
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
ι : Type w'
X : ι → Cᵒᵖ
x : (i : ι) → F.obj (X i)
h : PresheafIsGeneratedBy F x
F' : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
f : F ⟶ F'
inst_1 : Epi f
⊢ PresheafIsGeneratedBy F' (X := X) fun (i : ι) ↦
    (ConcreteCategory.hom (FC := TypeCat.Fun) (f.app (X i)) :
        (a : (fun (X : Type w) ↦ X) (F.obj (X i))) → (fun (X : Type w) ↦ X) (F'.obj (X i)))
      (x i)

Tactic:
simpa only [Subfunctor.range_eq_top f] using h.range f

Premises used: CategoryTheory.Subfunctor.range_eq_top, CategoryTheory.PresheafIsGeneratedBy.range
-- Module: Mathlib.CategoryTheory.Subfunctor.Finite
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
inst_1 : PresheafIsFinite F
⊢ PresheafIsGeneratedBy F (ι := Subfunctor.IsFinite.Index.{w, v, u} (C := C) (F := F) ⊤) Subfunctor.IsFinite.x

Tactic:
(Subfunctor.isGeneratedBy_of_isFinite (⊤ : Subfunctor F))

Premises used: CategoryTheory.Subfunctor.isGeneratedBy_of_isFinite, Top.top
-- Module: Mathlib.CategoryTheory.Subfunctor.Finite
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
inst_1 : PresheafIsFinite F
F' : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
f : F ⟶ F'
⊢ (range f).IsFinite

Tactic:
((presheafIsGeneratedBy_of_isFinite F).range f).isFinite

Premises used: CategoryTheory.PresheafIsGeneratedBy.range, CategoryTheory.Subfunctor.IsGeneratedBy.isFinite, CategoryTheory.presheafIsGeneratedBy_of_isFinite
-- Module: Mathlib.CategoryTheory.Subfunctor.Finite
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
inst_1 : PresheafIsFinite F
F' : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
f : F ⟶ F'
inst_2 : Epi f
⊢ PresheafIsFinite F'

Tactic:
((presheafIsGeneratedBy_of_isFinite F).of_epi f).isFinite

Premises used: CategoryTheory.PresheafIsGeneratedBy.of_epi, CategoryTheory.Subfunctor.IsGeneratedBy.isFinite, CategoryTheory.presheafIsGeneratedBy_of_isFinite
-- Module: Mathlib.CategoryTheory.Subfunctor.Finite
Goal:
C : Type u
inst : Category.{v, u} C
X : C
obj :
  ∀ (U : Cᵒᵖ) (u : Functor.obj (Functor.obj yoneda X) U),
    Membership.mem (γ := Set (Functor.obj (Functor.obj yoneda X) U))
        (Subfunctor.obj (⨆ (i : Unit), Subfunctor.ofSection (𝟙 X)) U) u ↔
      Membership.mem (γ := Set (Functor.obj (Functor.obj yoneda X) U)) (Subfunctor.obj ⊤ U) u
⊢ Eq (α := Subfunctor.{v, v, u} (Functor.obj yoneda X)) (⨆ (i : Unit), Subfunctor.ofSection (𝟙 X)) ⊤

Tactic:
ext U u
-- Module: Mathlib.CategoryTheory.Subfunctor.Finite
Goal:
C : Type u
inst : Category.{v, u} C
X : C
U : Cᵒᵖ
u : Functor.obj (Functor.obj yoneda X) U
obj :
  Membership.mem (γ := Set (unop U ⟶ X))
    (Subfunctor.obj (Subfunctor.ofSection (𝟙 X)) U : Set (Functor.obj (Functor.obj yoneda X) U)) u
⊢ Membership.mem (γ := Set (Functor.obj (Functor.obj yoneda X) U))
      (Subfunctor.obj (⨆ (i : Unit), Subfunctor.ofSection (𝟙 X)) U) u ↔
    Membership.mem (γ := Set (Functor.obj (Functor.obj yoneda X) U)) (Subfunctor.obj ⊤ U) u

Tactic:
simp only [yoneda_obj_obj, Subfunctor.iSup_obj, Set.mem_iUnion,
    exists_const, Subfunctor.top_obj, Set.top_eq_univ, Set.mem_univ, iff_true]

Premises used: Set.mem_iUnion, iff_true, CategoryTheory.yoneda_obj_obj, Set.top_eq_univ, exists_const, Set.mem_univ, CategoryTheory.Subfunctor.top_obj, CategoryTheory.Subfunctor.iSup_obj
-- Module: Mathlib.CategoryTheory.Subfunctor.Finite
Goal:
C : Type u
inst : Category.{v, u} C
X : C
U : Cᵒᵖ
u : Functor.obj (Functor.obj yoneda X) U
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) (Functor.map (Functor.obj yoneda X) (Quiver.Hom.op u)) :
        (a : (fun (X : Type v) ↦ X) ((yoneda.obj X).obj (op X))) → (fun (X : Type v) ↦ X) ((yoneda.obj X).obj U))
      (𝟙 X) =
    u

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Subfunctor.Finite
Goal:
C : Type u
inst : Category.{v, u} C
X : C
U : Cᵒᵖ
u : Functor.obj (Functor.obj yoneda X) U
⊢ Membership.mem (γ := Set (unop U ⟶ X))
    (Subfunctor.obj (Subfunctor.ofSection (𝟙 X)) U : Set (Functor.obj (Functor.obj yoneda X) U)) u

Tactic:
exact ⟨u.op, by simp⟩
-- Module: Mathlib.CategoryTheory.Subfunctor.Finite
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
X : C
⊢ PresheafIsFinite.{v, v, u} (Functor.obj yoneda X)

Tactic:
(yoneda_obj_isGeneratedBy X).isFinite

Premises used: CategoryTheory.Subfunctor.IsGeneratedBy.isFinite, CategoryTheory.yoneda_obj_isGeneratedBy
-- Module: Mathlib.CategoryTheory.Subfunctor.Image
Goal:
C : Type u
inst : Category.{v, u} C
F F' F'' : Functor.{v, w, u, w + 1} C (Type w)
p : F' ⟶ F
U V : C
i : U ⟶ V
x : F'.obj U
⊢ Membership.mem (α := F.obj U) (γ := Set (F.obj U))
    (Set.preimage (β := (fun (X : Type w) ↦ X) (F.obj V))
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map i)) :
        (a : (fun (X : Type w) ↦ X) (F.obj U)) → (fun (X : Type w) ↦ X) (F.obj V))
      (Set.range (ι := (fun (X : Type w) ↦ X) (F'.obj V))
        (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (p.app V)) :
          (a : (fun (X : Type w) ↦ X) (F'.obj V)) → (fun (X : Type w) ↦ X) (F.obj V))))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (p.app U) :
          (a : (fun (X : Type w) ↦ X) (F'.obj U)) → (fun (X : Type w) ↦ X) (F.obj U))
        x :
      (fun (X : Type w) ↦ X) (F.obj U))

Tactic:
⟨_, NatTrans.naturality_apply p i x⟩

Premises used: Set.Mem, setOf, Set.preimage, Exists.intro, Set.range