awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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:
exact ⟨_, NatTrans.naturality_apply p i x⟩
-- Module: Mathlib.CategoryTheory.Subfunctor.Image
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{v, w, u, w + 1} C (Type w)
⊢ range (𝟙 F) = ⊤

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

Tactic:
aesop
-- 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)
f : F' ⟶ F
G : Subfunctor F
hf : range f ≤ G
U : C
x : F'.obj U
⊢ Membership.mem (α := F.obj U) ((range f).obj U)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.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:
simp
-- 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)
f : F' ⟶ F
G : Subfunctor F
hf : range f ≤ G
x x_1 : C
g : x ⟶ x_1
h :
  ∀ (x_2 : F'.obj x),
    TypeCat.Fun.toFun
        (ConcreteCategory.hom (FC := TypeCat.Fun)
          (F'.map g ≫
            ↾fun (x : F'.obj x_1) ↦
              Subtype.mk (p := fun (x : F.obj x_1) ↦ x ∈ G.obj x_1)
                ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app x_1) :
                    (a : (fun (X : Type w) ↦ X) (F'.obj x_1)) → (fun (X : Type w) ↦ X) (F.obj x_1))
                  x)
                ⋯))
        x_2 =
      TypeCat.Fun.toFun
        (ConcreteCategory.hom (FC := TypeCat.Fun)
          ((↾fun (x_3 : F'.obj x) ↦
              Subtype.mk (p := fun (x_4 : F.obj x) ↦ x_4 ∈ G.obj x)
                ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app x) :
                    (a : (fun (X : Type w) ↦ X) (F'.obj x)) → (fun (X : Type w) ↦ X) (F.obj x))
                  x_3)
                ⋯) ≫
            G.toFunctor.map g))
        x_2
⊢ (F'.map g ≫
      ↾fun (x : F'.obj x_1) ↦
        Subtype.mk (p := fun (x : F.obj x_1) ↦ x ∈ G.obj x_1)
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app x_1) :
              (a : (fun (X : Type w) ↦ X) (F'.obj x_1)) → (fun (X : Type w) ↦ X) (F.obj x_1))
            x)
          ⋯) =
    (↾fun (x_2 : F'.obj x) ↦
        Subtype.mk (p := fun (x_3 : F.obj x) ↦ x_3 ∈ G.obj x)
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app x) :
              (a : (fun (X : Type w) ↦ X) (F'.obj x)) → (fun (X : Type w) ↦ X) (F.obj x))
            x_2)
          ⋯) ≫
      G.toFunctor.map g

Tactic:
ext x
-- 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)
f : F' ⟶ F
G : Subfunctor F
hf : range f ≤ G
x_1 x_2 : C
g : x_1 ⟶ x_2
x : F'.obj x_1
⊢ TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (F'.map g ≫
          ↾fun (x : F'.obj x_2) ↦
            Subtype.mk (p := fun (x : F.obj x_2) ↦ x ∈ G.obj x_2)
              ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app x_2) :
                  (a : (fun (X : Type w) ↦ X) (F'.obj x_2)) → (fun (X : Type w) ↦ X) (F.obj x_2))
                x)
              ⋯))
      x =
    TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        ((↾fun (x : F'.obj x_1) ↦
            Subtype.mk (p := fun (x : F.obj x_1) ↦ x ∈ G.obj x_1)
              ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app x_1) :
                  (a : (fun (X : Type w) ↦ X) (F'.obj x_1)) → (fun (X : Type w) ↦ X) (F.obj x_1))
                x)
              ⋯) ≫
          G.toFunctor.map g))
      x

Tactic:
simpa [Subtype.ext_iff, -NatTrans.naturality_apply] using NatTrans.naturality_apply f g x

Premises used: CategoryTheory.NatTrans.naturality_apply, Subtype.ext_iff
-- Module: Mathlib.CategoryTheory.Subfunctor.Image
Goal:
C : Type u
inst : Category.{v, u} C
F F' : Functor.{v, w, u, w + 1} C (Type w)
f : F' ⟶ F
G : Subfunctor F
hf : range f ≤ G
⊢ lift f hf ≫ G.ι = f

Tactic:
rfl

Premises used: CategoryTheory.NatTrans.vcomp, TypeCat.Fun.comp, rfl
-- 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
⊢ range p ≤ range p

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Subfunctor.Image
Goal:
C : Type u
inst : Category.{v, u} C
F F' : Functor.{v, w, u, w + 1} C (Type w)
p : F' ⟶ F
⊢ toRange p ≫ (range p).ι = p

Tactic:
rfl

Premises used: CategoryTheory.NatTrans.vcomp, TypeCat.Fun.comp, rfl
-- Module: Mathlib.CategoryTheory.Subfunctor.Image
Goal:
C : Type u
inst : Category.{v, u} C
F F' : Functor.{v, w, u, w + 1} C (Type w)
p : F' ⟶ F
i : C
x : F'.obj i
⊢ Eq (α := F.obj i)
    ((↑((ConcreteCategory.hom (FC := TypeCat.Fun) ((toRange p).app i) :
              (a : (fun (X : Type w) ↦ X) (F'.obj i)) → (fun (X : Type w) ↦ X) ((range p).toFunctor.obj i))
            x) :
        F.obj i) :
      F.obj i)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (p.app i) :
          (a : (fun (X : Type w) ↦ X) (F'.obj i)) → (fun (X : Type w) ↦ X) (F.obj i))
        x :
      (fun (X : Type w) ↦ X) (F.obj i))

Tactic:
simp [toRange]

Premises used: CategoryTheory.Subfunctor.toRange
-- Module: Mathlib.CategoryTheory.Subfunctor.Image
Goal:
C : Type u
inst : Category.{v, u} C
F F' : Functor.{v, w, u, w + 1} C (Type w)
p : F' ⟶ F
obj :
  ∀ (i : C) (x : F.obj i) (hx : x ∈ (range p).obj i),
    Subtype.mk (p := fun (x : F.obj i) ↦ x ∈ (range p).obj i) x hx ∈ (range (toRange p)).obj i ↔
      Membership.mem (γ := Set ((range p).toFunctor.obj i)) (Subfunctor.obj ⊤ i)
        (Subtype.mk (p := fun (x : F.obj i) ↦ x ∈ (range p).obj i) x hx)
⊢ range (toRange p) = ⊤

Tactic:
ext i ⟨x, hx⟩
-- Module: Mathlib.CategoryTheory.Subfunctor.Image
Goal:
C : Type u
inst : Category.{v, u} C
F F' : Functor.{v, w, u, w + 1} C (Type w)
p : F' ⟶ F
i : C
x : F.obj i
hx :
  Membership.mem (γ := Set (F.obj i))
    (Set.range (ι := F'.obj i) (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (p.app i)) : (a : F'.obj i) → F.obj i)) x
obj :
  ∃ (y : F'.obj i),
    (ConcreteCategory.hom (FC := TypeCat.Fun) ((toRange p).app i) :
          (a : F'.obj i) → (↑(Set.range (⇑(ConcreteCategory.hom (p.app i)) : (a : F'.obj i) → F.obj i)) : Type w))
        y =
      Subtype.mk (p := fun (x : F.obj i) ↦
        Membership.mem (γ := Set (F.obj i))
          (Set.range (ι := F'.obj i) (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (p.app i)) : (a : F'.obj i) → F.obj i))
          x)
        x hx
⊢ Membership.mem (γ :=
      Set
        (↑(Set.range (ι := F'.obj i)
              (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (p.app i)) : (a : F'.obj i) → F.obj i)) :
          Type w))
      (Set.range (ι := F'.obj i)
        (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) ((toRange p).app i)) :
          (a : F'.obj i) → (↑(Set.range (⇑(ConcreteCategory.hom (p.app i)) : (a : F'.obj i) → F.obj i)) : Type w)))
      (Subtype.mk (p := fun (x : F.obj i) ↦
        Membership.mem (γ := Set (F.obj i))
          (Set.range (ι := F'.obj i) (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (p.app i)) : (a : F'.obj i) → F.obj i))
          x)
        x hx) ↔
    Membership.mem (γ :=
      Set
        (↑(Set.range (ι := F'.obj i)
              (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (p.app i)) : (a : F'.obj i) → F.obj i)) :
          Type w))
      Set.univ
      (Subtype.mk (p := fun (x : F.obj i) ↦
        Membership.mem (γ := Set (F.obj i))
          (Set.range (ι := F'.obj i) (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (p.app i)) : (a : F'.obj i) → F.obj i))
          x)
        x hx)

Tactic:
simp only [Set.mem_range, Set.mem_univ, iff_true]

Premises used: Set.mem_range, iff_true, Set.mem_univ
-- Module: Mathlib.CategoryTheory.Subfunctor.Image
Goal:
C : Type u
inst : Category.{v, u} C
F F' : Functor.{v, w, u, w + 1} C (Type w)
p : F' ⟶ F
i : C
x : F.obj i
hx :
  Membership.mem (γ := Set (F.obj i))
    {x : F.obj i |
      ∃ (y : F'.obj i), (ConcreteCategory.hom (FC := TypeCat.Fun) (p.app i) : (a : F'.obj i) → F.obj i) y = x}
    x
obj :
  ∀ (y : F'.obj i),
    ∃ (y_1 : F'.obj i),
      Eq (α :=
        (↑(Set.range (ι := F'.obj i)
              (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (p.app i)) : (a : F'.obj i) → F.obj i)) :
          Type w))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) ((toRange p).app i) :
              (a : F'.obj i) → (↑(Set.range (⇑(ConcreteCategory.hom (p.app i)) : (a : F'.obj i) → F.obj i)) : Type w))
            y_1 :
          (↑(Set.range (ι := F'.obj i)
                (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (p.app i)) : (a : F'.obj i) → F.obj i)) :
            Type w))
        (Subtype.mk (p := fun (x : F.obj i) ↦
            Membership.mem (γ := Set (F.obj i))
              (Set.range (ι := F'.obj i)
                (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (p.app i)) : (a : F'.obj i) → F.obj i))
              x)
            ((ConcreteCategory.hom (FC := TypeCat.Fun) (p.app i) : (a : F'.obj i) → F.obj i) y) ⋯ :
          { x : F.obj i //
            Membership.mem (γ := Set (F.obj i))
              (Set.range (ι := F'.obj i)
                (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (p.app i)) : (a : F'.obj i) → F.obj i))
              x })
⊢ ∃ (y : F'.obj i),
    (ConcreteCategory.hom (FC := TypeCat.Fun) ((toRange p).app i) :
          (a : F'.obj i) → (↑(Set.range (⇑(ConcreteCategory.hom (p.app i)) : (a : F'.obj i) → F.obj i)) : Type w))
        y =
      Subtype.mk (p := fun (x : F.obj i) ↦
        Membership.mem (γ := Set (F.obj i))
          (Set.range (ι := F'.obj i) (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (p.app i)) : (a : F'.obj i) → F.obj i))
          x)
        x hx

Tactic:
obtain ⟨y, rfl⟩ := hx

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Subfunctor.Image
Goal:
C : Type u
inst : Category.{v, u} C
F F' : Functor.{v, w, u, w + 1} C (Type w)
p : F' ⟶ F
i : C
y : F'.obj i
⊢ ∃ (y_1 : F'.obj i),
    Eq (α :=
      (↑(Set.range (ι := F'.obj i) (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (p.app i)) : (a : F'.obj i) → F.obj i)) :
        Type w))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) ((toRange p).app i) :
            (a : F'.obj i) → (↑(Set.range (⇑(ConcreteCategory.hom (p.app i)) : (a : F'.obj i) → F.obj i)) : Type w))
          y_1 :
        (↑(Set.range (ι := F'.obj i)
              (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (p.app i)) : (a : F'.obj i) → F.obj i)) :
          Type w))
      (Subtype.mk (p := fun (x : F.obj i) ↦
          Membership.mem (γ := Set (F.obj i))
            (Set.range (ι := F'.obj i)
              (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (p.app i)) : (a : F'.obj i) → F.obj i))
            x)
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (p.app i) : (a : F'.obj i) → F.obj i) y) ⋯ :
        { x : F.obj i //
          Membership.mem (γ := Set (F.obj i))
            (Set.range (ι := F'.obj i)
              (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (p.app i)) : (a : F'.obj i) → F.obj i))
            x })

Tactic:
⟨y, rfl⟩

Premises used: Exists.intro, rfl
-- Module: Mathlib.CategoryTheory.Subfunctor.Image
Goal:
C : Type u
inst : Category.{v, u} C
F F' : Functor.{v, w, u, w + 1} C (Type w)
p : F' ⟶ F
i : C
y : F'.obj i
⊢ ∃ (y_1 : F'.obj i),
    Eq (α :=
      (↑(Set.range (ι := F'.obj i) (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (p.app i)) : (a : F'.obj i) → F.obj i)) :
        Type w))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) ((toRange p).app i) :
            (a : F'.obj i) → (↑(Set.range (⇑(ConcreteCategory.hom (p.app i)) : (a : F'.obj i) → F.obj i)) : Type w))
          y_1 :
        (↑(Set.range (ι := F'.obj i)
              (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (p.app i)) : (a : F'.obj i) → F.obj i)) :
          Type w))
      (Subtype.mk (p := fun (x : F.obj i) ↦
          Membership.mem (γ := Set (F.obj i))
            (Set.range (ι := F'.obj i)
              (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (p.app i)) : (a : F'.obj i) → F.obj i))
            x)
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (p.app i) : (a : F'.obj i) → F.obj i) y) ⋯ :
        { x : F.obj i //
          Membership.mem (γ := Set (F.obj i))
            (Set.range (ι := F'.obj i)
              (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (p.app i)) : (a : F'.obj i) → F.obj i))
            x })

Tactic:
exact ⟨y, rfl⟩
-- Module: Mathlib.CategoryTheory.Subfunctor.Image
Goal:
C : Type u
inst : Category.{v, u} C
F F' : Functor.{v, w, u, w + 1} C (Type w)
p : F' ⟶ F
⊢ Epi p ↔ range p = ⊤

Tactic:
simp [NatTrans.epi_iff_epi_app, epi_iff_surjective, Subfunctor.ext_iff, funext_iff,
    Set.range_eq_univ]

Premises used: Set.range_eq_univ, CategoryTheory.NatTrans.epi_iff_epi_app, CategoryTheory.epi_iff_surjective, funext_iff, CategoryTheory.Subfunctor.ext_iff
-- Module: Mathlib.CategoryTheory.Subfunctor.Image
Goal:
C : Type u
inst : Category.{v, u} C
F F' : Functor.{v, w, u, w + 1} C (Type w)
p : F' ⟶ F
inst_1 rwa rwa₁ rwa₂ rwa₃ : Epi p
⊢ range p = ⊤

Tactic:
rwa [← epi_iff_range_eq_top]

Premises used: CategoryTheory.Subfunctor.epi_iff_range_eq_top
-- 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
⊢ Epi (toRange p)

Tactic:
simp [epi_iff_range_eq_top]

Premises used: CategoryTheory.Subfunctor.epi_iff_range_eq_top
-- 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
inst_1 : Mono p
⊢ Mono (toRange p)

Tactic:
have := mono_of_mono_fac (toRange_ι p)
-- 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
inst_1 : Mono p
this : Mono (toRange p)
rw : ∀ (X : C), IsIso ((toRange p).app X)
⊢ IsIso (toRange p)

Tactic:
rw [NatTrans.isIso_iff_isIso_app]

Premises used: CategoryTheory.NatTrans.isIso_iff_isIso_app
-- 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
inst_1 : Mono p
this : Mono (toRange p)
i : C
rw :
  Function.Bijective (α := (fun (X : Type w) ↦ X) (F'.obj i)) (β := (fun (X : Type w) ↦ X) ((range p).toFunctor.obj i))
    (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) ((toRange p).app i)) :
      (a : (fun (X : Type w) ↦ X) (F'.obj i)) → (fun (X : Type w) ↦ X) ((range p).toFunctor.obj i))
⊢ IsIso ((toRange p).app i)

Tactic:
rw [isIso_iff_bijective]

Premises used: CategoryTheory.isIso_iff_bijective
-- 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
inst_1 : Mono p
this : Mono (toRange p)
i : C
left :
  Function.Injective (α := (fun (X : Type w) ↦ X) (F'.obj i)) (β := (fun (X : Type w) ↦ X) ((range p).toFunctor.obj i))
    (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) ((toRange p).app i)) :
      (a : (fun (X : Type w) ↦ X) (F'.obj i)) → (fun (X : Type w) ↦ X) ((range p).toFunctor.obj i))
right :
  Function.Surjective (α := (fun (X : Type w) ↦ X) (F'.obj i)) (β := (fun (X : Type w) ↦ X) ((range p).toFunctor.obj i))
    (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) ((toRange p).app i)) :
      (a : (fun (X : Type w) ↦ X) (F'.obj i)) → (fun (X : Type w) ↦ X) ((range p).toFunctor.obj i))
⊢ Function.Bijective (α := (fun (X : Type w) ↦ X) (F'.obj i)) (β := (fun (X : Type w) ↦ X) ((range p).toFunctor.obj i))
    (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) ((toRange p).app i)) :
      (a : (fun (X : Type w) ↦ X) (F'.obj i)) → (fun (X : Type w) ↦ X) ((range p).toFunctor.obj i))

Tactic:
constructor
-- 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
inst_1 : Mono p
this : Mono (toRange p)
i : C
left : Mono ((toRange p).app i)
⊢ Function.Injective (α := (fun (X : Type w) ↦ X) (F'.obj i)) (β := (fun (X : Type w) ↦ X) ((range p).toFunctor.obj i))
    (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) ((toRange p).app i)) :
      (a : (fun (X : Type w) ↦ X) (F'.obj i)) → (fun (X : Type w) ↦ X) ((range p).toFunctor.obj i))

Tactic:
rw [← mono_iff_injective]

Premises used: CategoryTheory.mono_iff_injective
-- 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
inst_1 : Mono p
this : Mono (toRange p)
i : C
⊢ Mono ((toRange p).app i)

Tactic:
infer_instance
-- 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
inst_1 : Mono p
this : Mono (toRange p)
i : C
right : Epi ((toRange p).app i)
⊢ Function.Surjective (α := (fun (X : Type w) ↦ X) (F'.obj i)) (β := (fun (X : Type w) ↦ X) ((range p).toFunctor.obj i))
    (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) ((toRange p).app i)) :
      (a : (fun (X : Type w) ↦ X) (F'.obj i)) → (fun (X : Type w) ↦ X) ((range p).toFunctor.obj i))

Tactic:
rw [← epi_iff_surjective]

Premises used: CategoryTheory.epi_iff_surjective
-- 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
inst_1 : Mono p
this : Mono (toRange p)
i : C
⊢ Epi ((toRange p).app i)

Tactic:
infer_instance
-- 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)
f : F ⟶ F'
g : F' ⟶ F''
x : C
x_1 : F''.obj x
h : x_1 ∈ (range (f ≫ g)).obj x
⊢ x_1 ∈ (range g).obj x

Tactic:
aesop
-- 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)
G : Subfunctor F
f : F ⟶ F'
Δ Δ' : C
φ : Δ ⟶ Δ'
x : F.obj Δ
hx : x ∈ G.obj Δ
⊢ Eq (α := F'.obj Δ')
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app Δ') :
          (a : (fun (X : Type w) ↦ X) (F.obj Δ')) → (fun (X : Type w) ↦ X) (F'.obj Δ'))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map φ) :
              (a : (fun (X : Type w) ↦ X) (F.obj Δ)) → (fun (X : Type w) ↦ X) (F.obj Δ'))
            x :
          (fun (X : Type w) ↦ X) (F.obj Δ')) :
      (fun (X : Type w) ↦ X) (F'.obj Δ'))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F'.map φ) :
          (a : (fun (X : Type w) ↦ X) (F'.obj Δ)) → (fun (X : Type w) ↦ X) (F'.obj Δ'))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app Δ) :
              (a : (fun (X : Type w) ↦ X) (F.obj Δ)) → (fun (X : Type w) ↦ X) (F'.obj Δ))
            x :
          (fun (X : Type w) ↦ X) (F'.obj Δ)) :
      (fun (X : Type w) ↦ X) (F'.obj Δ'))

Tactic:
apply NatTrans.naturality_apply

Premises used: CategoryTheory.NatTrans.naturality_apply
-- 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)
G : Subfunctor F
f : F ⟶ F'
Δ Δ' : C
φ : Δ ⟶ Δ'
x : F.obj Δ
hx : x ∈ G.obj Δ
⊢ Membership.mem (α := F'.obj Δ) (γ := Set (F'.obj Δ))
    (Set.preimage (β := (fun (X : Type w) ↦ X) (F'.obj Δ'))
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F'.map φ)) :
        (a : (fun (X : Type w) ↦ X) (F'.obj Δ)) → (fun (X : Type w) ↦ X) (F'.obj Δ'))
      ((⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (f.app Δ')) :
          (a : (fun (X : Type w) ↦ X) (F.obj Δ')) → (fun (X : Type w) ↦ X) (F'.obj Δ')) ''
        G.obj Δ'))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app Δ) :
          (a : (fun (X : Type w) ↦ X) (F.obj Δ)) → (fun (X : Type w) ↦ X) (F'.obj Δ))
        x :
      (fun (X : Type w) ↦ X) (F'.obj Δ))

Tactic:
exact ⟨F.map φ x, G.map φ hx, by apply NatTrans.naturality_apply⟩
-- Module: Mathlib.CategoryTheory.Subfunctor.Image
Goal:
C : Type u
inst : Category.{v, u} C
F F' : Functor.{v, w, u, w + 1} C (Type w)
f : F ⟶ F'
⊢ image ⊤ f = range f

Tactic:
aesop
-- Module: Mathlib.CategoryTheory.Subfunctor.Image
Goal:
C : Type u
inst : Category.{v, u} C
F F' : Functor.{v, w, u, w + 1} C (Type w)
ι : Type u_1
G : ι → Subfunctor F
f : F ⟶ F'
⊢ image (⨆ (i : ι), G i) f = ⨆ (i : ι), (G i).image f

Tactic:
aesop
-- 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)
G : Subfunctor F
f : F ⟶ F'
g : F' ⟶ F''
⊢ G.image (f ≫ g) = (G.image f).image g

Tactic:
aesop
-- 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)
f : F ⟶ F'
g : F' ⟶ F''
⊢ range (f ≫ g) = (range f).image g

Tactic:
aesop
-- 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)
G : Subfunctor F
p : F' ⟶ F
U V : C
f : U ⟶ V
simp :
  Subset (α := Set (F'.obj U))
    ((fun (x : F'.obj U) ↦
        (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f) : (a : F.obj U) → F.obj V)
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (p.app U) : (a : F'.obj U) → F.obj U) x : F.obj U)) ⁻¹'
      G.obj V)
    ((fun (x : F'.obj U) ↦
        (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f) : (a : F.obj U) → F.obj V)
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (p.app U) : (a : F'.obj U) → F.obj U) x : F.obj U)) ⁻¹'
      G.obj V)
⊢ Subset (α := Set (F'.obj U))
    (Set.preimage (β := F.obj U)
      (⇑(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))
      ((⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f)) :
          (a : (fun (X : Type w) ↦ X) (F.obj U)) → (fun (X : Type w) ↦ X) (F.obj V)) ⁻¹'
        G.obj V))
    (Set.preimage (β := (fun (X : Type w) ↦ X) (F'.obj V))
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F'.map f)) :
        (a : (fun (X : Type w) ↦ X) (F'.obj U)) → (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)) ⁻¹'
        G.obj V))

Tactic:
simp only [Set.preimage_preimage, NatTrans.naturality_apply]

Premises used: CategoryTheory.NatTrans.naturality_apply, Set.preimage_preimage
-- 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)
G : Subfunctor F
p : F' ⟶ F
U V : C
f : U ⟶ V
⊢ Subset (α := Set (F'.obj U))
    ((fun (x : F'.obj U) ↦
        (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f) : (a : F.obj U) → F.obj V)
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (p.app U) : (a : F'.obj U) → F.obj U) x : F.obj U)) ⁻¹'
      G.obj V)
    ((fun (x : F'.obj U) ↦
        (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f) : (a : F.obj U) → F.obj V)
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (p.app U) : (a : F'.obj U) → F.obj U) x : F.obj U)) ⁻¹'
      G.obj V)

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Subfunctor.Image
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{v, w, u, w + 1} C (Type w)
G : Subfunctor F
⊢ G.preimage (𝟙 F) = G

Tactic:
aesop
-- 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)
G : Subfunctor F
f : F'' ⟶ F'
g : F' ⟶ F
⊢ G.preimage (f ≫ g) = (G.preimage g).preimage f

Tactic:
aesop
-- Module: Mathlib.CategoryTheory.Subfunctor.Image
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 ⟶ F'
G' : Subfunctor F'
⊢ G.image f ≤ G' ↔ G ≤ G'.preimage f

Tactic:
simp [Subfunctor.le_def]

Premises used: CategoryTheory.Subfunctor.le_def