awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Functor.EpiMono
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F G : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : F.ReflectsMonomorphisms
α : F ≅ G
X Y : C
f : X ⟶ Y
h : Mono (G.map f)
⊢ F.map f = (α.app X).hom ≫ G.map f ≫ (α.app Y).inv

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Functor.EpiMono
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F G : Functor.{v₁, v₂, u₁, u₂} C D
α : F ≅ G
⊢ F.ReflectsMonomorphisms ↔ G.ReflectsMonomorphisms

Tactic:
⟨fun _ => reflectsMonomorphisms.of_iso α, fun _ => reflectsMonomorphisms.of_iso α.symm⟩

Premises used: CategoryTheory.Functor.reflectsMonomorphisms.of_iso, Iff.intro, CategoryTheory.Iso.symm
-- Module: Mathlib.CategoryTheory.Functor.EpiMono
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F G : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : F.ReflectsEpimorphisms
α : F ≅ G
X Y : C
f : X ⟶ Y
h : Epi (G.map f)
apply : Epi (F.map f)
⊢ Epi f

Tactic:
apply F.epi_of_epi_map

Premises used: CategoryTheory.Functor.epi_of_epi_map
-- Module: Mathlib.CategoryTheory.Functor.EpiMono
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F G : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : F.ReflectsEpimorphisms
α : F ≅ G
X Y : C
f : X ⟶ Y
h : Epi (G.map f)
suffices : F.map f = (α.app X).hom ≫ G.map f ≫ (α.app Y).inv
⊢ Epi (F.map f)

Tactic:
suffices F.map f = (α.app X).hom ≫ G.map f ≫ (α.app Y).inv from this ▸ epi_comp _ _
-- Module: Mathlib.CategoryTheory.Functor.EpiMono
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F G : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : F.ReflectsEpimorphisms
α : F ≅ G
X Y : C
f : X ⟶ Y
h : Epi (G.map f)
⊢ F.map f = (α.app X).hom ≫ G.map f ≫ (α.app Y).inv

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Functor.EpiMono
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F G : Functor.{v₁, v₂, u₁, u₂} C D
α : F ≅ G
⊢ F.ReflectsEpimorphisms ↔ G.ReflectsEpimorphisms

Tactic:
⟨fun _ => reflectsEpimorphisms.of_iso α, fun _ => reflectsEpimorphisms.of_iso α.symm⟩

Premises used: Iff.intro, CategoryTheory.Iso.symm, CategoryTheory.Functor.reflectsEpimorphisms.of_iso
-- Module: Mathlib.CategoryTheory.Functor.EpiMono
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₁, u₂, u₁} D C
adj : F ⊣ G
X Y : C
f : X ⟶ Y
hf : Epi f
Z : D
g h : F.obj Y ⟶ Z
H : F.map f ≫ g = F.map f ≫ h
⊢ Eq.{v₁ + 1} (α := X ⟶ G.obj Z) ((adj.homEquiv X Z : (a : F.obj X ⟶ Z) → X ⟶ G.obj Z) (F.map f ≫ g) : X ⟶ G.obj Z)
    ((adj.homEquiv X Z : (a : F.obj X ⟶ Z) → X ⟶ G.obj Z) (F.map f ≫ h) : X ⟶ G.obj Z)

Tactic:
replace H := congr_arg (adj.homEquiv X Z) H
-- Module: Mathlib.CategoryTheory.Functor.EpiMono
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₁, u₂, u₁} D C
adj : F ⊣ G
X Y : C
f : X ⟶ Y
hf : Epi f
Z : D
g h : F.obj Y ⟶ Z
H :
  Eq.{v₁ + 1} (α := X ⟶ G.obj Z) ((adj.homEquiv X Z : (a : F.obj X ⟶ Z) → X ⟶ G.obj Z) (F.map f ≫ g) : X ⟶ G.obj Z)
    ((adj.homEquiv X Z : (a : F.obj X ⟶ Z) → X ⟶ G.obj Z) (F.map f ≫ h) : X ⟶ G.obj Z)
rwa :
  ∀
    (H :
      Eq (α := X ⟶ G.obj Z) (f ≫ (adj.homEquiv Y Z : (a : F.obj Y ⟶ Z) → Y ⟶ G.obj Z) g)
        ((adj.homEquiv X Z : (a : F.obj X ⟶ Z) → X ⟶ G.obj Z) (F.map f ≫ h))),
    g = h
rwa₁ :
  ∀
    (H :
      Eq (α := X ⟶ G.obj Z) (f ≫ (adj.homEquiv Y Z : (a : F.obj Y ⟶ Z) → Y ⟶ G.obj Z) g)
        (f ≫ (adj.homEquiv Y Z : (a : F.obj Y ⟶ Z) → Y ⟶ G.obj Z) h)),
    g = h
rwa₂ :
  ∀
    (H :
      Eq.{v₁ + 1} (α := Y ⟶ G.obj Z) ((adj.homEquiv Y Z : (a : F.obj Y ⟶ Z) → Y ⟶ G.obj Z) g : Y ⟶ G.obj Z)
        ((adj.homEquiv Y Z : (a : F.obj Y ⟶ Z) → Y ⟶ G.obj Z) h : Y ⟶ G.obj Z)),
    g = h
rwa₃ rwa₄ rwa₅ rwa₆ : ∀ (H : g = h), g = h
⊢ g = h

Tactic:
rwa [adj.homEquiv_naturality_left, adj.homEquiv_naturality_left, cancel_epi,
          Equiv.apply_eq_iff_eq] at H

Premises used: Equiv.apply_eq_iff_eq, CategoryTheory.cancel_epi, CategoryTheory.Adjunction.homEquiv_naturality_left
-- Module: Mathlib.CategoryTheory.Functor.EpiMono
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_3 : F.IsLeftAdjoint
⊢ F.PreservesEpimorphisms

Tactic:
preservesEpimorphisms_of_adjunction (Adjunction.ofIsLeftAdjoint F)

Premises used: CategoryTheory.Adjunction.ofIsLeftAdjoint, CategoryTheory.Functor.preservesEpimorphisms_of_adjunction
-- Module: Mathlib.CategoryTheory.Functor.EpiMono
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₁, u₂, u₁} D C
adj : F ⊣ G
X Y : D
f : X ⟶ Y
hf : Mono f
Z : C
g h : Z ⟶ G.obj X
H : g ≫ G.map f = h ≫ G.map f
⊢ Eq.{v₂ + 1} (α := F.obj Z ⟶ Y)
    (((adj.homEquiv Z Y).symm : (a : Z ⟶ G.obj Y) → F.obj Z ⟶ Y) (g ≫ G.map f) : F.obj Z ⟶ Y)
    (((adj.homEquiv Z Y).symm : (a : Z ⟶ G.obj Y) → F.obj Z ⟶ Y) (h ≫ G.map f) : F.obj Z ⟶ Y)

Tactic:
replace H := congr_arg (adj.homEquiv Z Y).symm H
-- Module: Mathlib.CategoryTheory.Functor.EpiMono
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₁, u₂, u₁} D C
adj : F ⊣ G
X Y : D
f : X ⟶ Y
hf : Mono f
Z : C
g h : Z ⟶ G.obj X
H :
  Eq.{v₂ + 1} (α := F.obj Z ⟶ Y)
    (((adj.homEquiv Z Y).symm : (a : Z ⟶ G.obj Y) → F.obj Z ⟶ Y) (g ≫ G.map f) : F.obj Z ⟶ Y)
    (((adj.homEquiv Z Y).symm : (a : Z ⟶ G.obj Y) → F.obj Z ⟶ Y) (h ≫ G.map f) : F.obj Z ⟶ Y)
rwa :
  ∀
    (H :
      Eq.{v₂ + 1} (α := F.obj Z ⟶ Y) (((adj.homEquiv Z X).symm : (a : Z ⟶ G.obj X) → F.obj Z ⟶ X) g ≫ f : F.obj Z ⟶ Y)
        (((adj.homEquiv Z Y).symm : (a : Z ⟶ G.obj Y) → F.obj Z ⟶ Y) (h ≫ G.map f) : F.obj Z ⟶ Y)),
    g = h
rwa₁ :
  ∀
    (H :
      Eq.{v₂ + 1} (α := F.obj Z ⟶ Y) (((adj.homEquiv Z X).symm : (a : Z ⟶ G.obj X) → F.obj Z ⟶ X) g ≫ f : F.obj Z ⟶ Y)
        (((adj.homEquiv Z X).symm : (a : Z ⟶ G.obj X) → F.obj Z ⟶ X) h ≫ f : F.obj Z ⟶ Y)),
    g = h
rwa₂ :
  ∀
    (H :
      Eq.{v₂ + 1} (α := F.obj Z ⟶ X) (((adj.homEquiv Z X).symm : (a : Z ⟶ G.obj X) → F.obj Z ⟶ X) g : F.obj Z ⟶ X)
        (((adj.homEquiv Z X).symm : (a : Z ⟶ G.obj X) → F.obj Z ⟶ X) h : F.obj Z ⟶ X)),
    g = h
rwa₃ rwa₄ rwa₅ rwa₆ : ∀ (H : g = h), g = h
⊢ g = h

Tactic:
rwa [adj.homEquiv_naturality_right_symm, adj.homEquiv_naturality_right_symm, cancel_mono,
          Equiv.apply_eq_iff_eq] at H

Premises used: CategoryTheory.cancel_mono, CategoryTheory.Adjunction.homEquiv_naturality_right_symm, Equiv.apply_eq_iff_eq
-- Module: Mathlib.CategoryTheory.Functor.EpiMono
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_3 : F.IsRightAdjoint
⊢ F.PreservesMonomorphisms

Tactic:
preservesMonomorphisms_of_adjunction (Adjunction.ofIsRightAdjoint F)

Premises used: CategoryTheory.Functor.preservesMonomorphisms_of_adjunction, CategoryTheory.Adjunction.ofIsRightAdjoint
-- Module: Mathlib.CategoryTheory.Functor.EpiMono
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_3 : F.Faithful
X Y : C
f : X ⟶ Y
h_1 : Mono (F.map f)
Z : C
g h : Z ⟶ X
hgh : g ≫ f = h ≫ f
rw : F.map (g ≫ f) = F.map h ≫ F.map f
rw₁ : F.map (h ≫ f) = F.map h ≫ F.map f
rw₂ rw₃ : F.map h ≫ F.map f = F.map h ≫ F.map f
⊢ F.map g ≫ F.map f = F.map h ≫ F.map f

Tactic:
rw [← F.map_comp, hgh, F.map_comp]

Premises used: CategoryTheory.Functor.map_comp
-- Module: Mathlib.CategoryTheory.Functor.EpiMono
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_3 : F.Faithful
X Y : C
f : X ⟶ Y
h_1 : Epi (F.map f)
Z : C
g h : Y ⟶ Z
hgh : f ≫ g = f ≫ h
rw : F.map (f ≫ g) = F.map f ≫ F.map h
rw₁ : F.map (f ≫ h) = F.map f ≫ F.map h
rw₂ rw₃ : F.map f ≫ F.map h = F.map f ≫ F.map h
⊢ F.map f ≫ F.map g = F.map f ≫ F.map h

Tactic:
rw [← F.map_comp, hgh, F.map_comp]

Premises used: CategoryTheory.Functor.map_comp
-- Module: Mathlib.CategoryTheory.Functor.EpiMono
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
F G : Functor.{v₁, v₂, u₁, u₂} C D
f : F ⟶ G
inst_3 : IsSplitEpi f
X : C
⊢ IsSplitEpi (f.app X)

Tactic:
inferInstanceAs (IsSplitEpi (((evaluation C D).obj X).map f))

Premises used: _private.0.CategoryTheory.Functor.instIsSplitEpiApp._proof_1
-- Module: Mathlib.CategoryTheory.Functor.EpiMono
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
F G : Functor.{v₁, v₂, u₁, u₂} C D
f : F ⟶ G
inst_3 : IsSplitMono f
X : C
⊢ IsSplitMono (f.app X)

Tactic:
inferInstanceAs (IsSplitMono (((evaluation C D).obj X).map f))

Premises used: _private.0.CategoryTheory.Functor.instIsSplitMonoApp._proof_1
-- Module: Mathlib.CategoryTheory.Functor.EpiMono
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
F : Functor.{v₁, v₂, u₁, u₂} C D
X Y : C
f : X ⟶ Y
inst_3 : F.Full
inst_4 : F.Faithful
s : SplitEpi (F.map f)
a : F.map (F.preimage s.section_ ≫ f) = F.map (𝟙 Y)
⊢ F.preimage s.section_ ≫ f = 𝟙 Y

Tactic:
apply F.map_injective

Premises used: CategoryTheory.Functor.map_injective
-- Module: Mathlib.CategoryTheory.Functor.EpiMono
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
F : Functor.{v₁, v₂, u₁, u₂} C D
X Y : C
f : X ⟶ Y
inst_3 : F.Full
inst_4 : F.Faithful
s : SplitEpi (F.map f)
a : s.section_ ≫ F.map f = 𝟙 (F.obj Y)
⊢ F.map (F.preimage s.section_ ≫ f) = F.map (𝟙 Y)

Tactic:
simp only [map_comp, map_preimage, map_id]

Premises used: CategoryTheory.Functor.map_id, CategoryTheory.Functor.map_comp, CategoryTheory.Functor.map_preimage
-- Module: Mathlib.CategoryTheory.Functor.EpiMono
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
F : Functor.{v₁, v₂, u₁, u₂} C D
X Y : C
f : X ⟶ Y
inst_3 : F.Full
inst_4 : F.Faithful
s : SplitEpi (F.map f)
⊢ s.section_ ≫ F.map f = 𝟙 (F.obj Y)

Tactic:
apply SplitEpi.id

Premises used: CategoryTheory.SplitEpi.id
-- Module: Mathlib.CategoryTheory.Functor.EpiMono
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
X Y : C
f : X ⟶ Y
inst_2 : F.Full
inst_3 : F.Faithful
mp : IsSplitEpi (F.map f) → IsSplitEpi f
mpr : IsSplitEpi f → IsSplitEpi (F.map f)
⊢ IsSplitEpi (F.map f) ↔ IsSplitEpi f

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.Functor.EpiMono
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
X Y : C
f : X ⟶ Y
inst_2 : F.Full
inst_3 : F.Faithful
h : IsSplitEpi (F.map f)
⊢ IsSplitEpi f

Tactic:
IsSplitEpi.mk' ((splitEpiEquiv F f).invFun h.exists_splitEpi.some)

Premises used: Nonempty.some, CategoryTheory.Functor.splitEpiEquiv, CategoryTheory.IsSplitEpi.exists_splitEpi, Equiv.invFun, CategoryTheory.IsSplitEpi.mk'
-- Module: Mathlib.CategoryTheory.Functor.EpiMono
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
X Y : C
f : X ⟶ Y
inst_2 : F.Full
inst_3 : F.Faithful
h : IsSplitEpi (F.map f)
⊢ IsSplitEpi f

Tactic:
exact IsSplitEpi.mk' ((splitEpiEquiv F f).invFun h.exists_splitEpi.some)

Premises used: Nonempty.some, CategoryTheory.Functor.splitEpiEquiv, CategoryTheory.IsSplitEpi.exists_splitEpi, Equiv.invFun, CategoryTheory.IsSplitEpi.mk'
-- Module: Mathlib.CategoryTheory.Functor.EpiMono
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
X Y : C
f : X ⟶ Y
inst_2 : F.Full
inst_3 : F.Faithful
h : IsSplitEpi f
⊢ IsSplitEpi (F.map f)

Tactic:
IsSplitEpi.mk' ((splitEpiEquiv F f).toFun h.exists_splitEpi.some)

Premises used: Nonempty.some, Equiv.toFun, CategoryTheory.Functor.splitEpiEquiv, CategoryTheory.IsSplitEpi.exists_splitEpi, CategoryTheory.IsSplitEpi.mk'
-- Module: Mathlib.CategoryTheory.Functor.EpiMono
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
X Y : C
f : X ⟶ Y
inst_2 : F.Full
inst_3 : F.Faithful
h : IsSplitEpi f
⊢ IsSplitEpi (F.map f)

Tactic:
exact IsSplitEpi.mk' ((splitEpiEquiv F f).toFun h.exists_splitEpi.some)

Premises used: Nonempty.some, Equiv.toFun, CategoryTheory.Functor.splitEpiEquiv, CategoryTheory.IsSplitEpi.exists_splitEpi, CategoryTheory.IsSplitEpi.mk'
-- Module: Mathlib.CategoryTheory.Functor.EpiMono
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
F : Functor.{v₁, v₂, u₁, u₂} C D
X Y : C
f : X ⟶ Y
inst_3 : F.Full
inst_4 : F.Faithful
s : SplitMono (F.map f)
a : F.map (f ≫ F.preimage s.retraction) = F.map (𝟙 X)
⊢ f ≫ F.preimage s.retraction = 𝟙 X

Tactic:
apply F.map_injective

Premises used: CategoryTheory.Functor.map_injective
-- Module: Mathlib.CategoryTheory.Functor.EpiMono
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
F : Functor.{v₁, v₂, u₁, u₂} C D
X Y : C
f : X ⟶ Y
inst_3 : F.Full
inst_4 : F.Faithful
s : SplitMono (F.map f)
a : F.map f ≫ s.retraction = 𝟙 (F.obj X)
⊢ F.map (f ≫ F.preimage s.retraction) = F.map (𝟙 X)

Tactic:
simp only [map_comp, map_preimage, map_id]

Premises used: CategoryTheory.Functor.map_id, CategoryTheory.Functor.map_comp, CategoryTheory.Functor.map_preimage
-- Module: Mathlib.CategoryTheory.Functor.EpiMono
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
F : Functor.{v₁, v₂, u₁, u₂} C D
X Y : C
f : X ⟶ Y
inst_3 : F.Full
inst_4 : F.Faithful
s : SplitMono (F.map f)
⊢ F.map f ≫ s.retraction = 𝟙 (F.obj X)

Tactic:
apply SplitMono.id

Premises used: CategoryTheory.SplitMono.id
-- Module: Mathlib.CategoryTheory.Functor.EpiMono
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
X Y : C
f : X ⟶ Y
inst_2 : F.Full
inst_3 : F.Faithful
mp : IsSplitMono (F.map f) → IsSplitMono f
mpr : IsSplitMono f → IsSplitMono (F.map f)
⊢ IsSplitMono (F.map f) ↔ IsSplitMono f

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.Functor.EpiMono
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
X Y : C
f : X ⟶ Y
inst_2 : F.Full
inst_3 : F.Faithful
h : IsSplitMono (F.map f)
⊢ IsSplitMono f

Tactic:
IsSplitMono.mk' ((splitMonoEquiv F f).invFun h.exists_splitMono.some)

Premises used: Nonempty.some, CategoryTheory.IsSplitMono.exists_splitMono, CategoryTheory.Functor.splitMonoEquiv, CategoryTheory.IsSplitMono.mk', Equiv.invFun
-- Module: Mathlib.CategoryTheory.Functor.EpiMono
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
X Y : C
f : X ⟶ Y
inst_2 : F.Full
inst_3 : F.Faithful
h : IsSplitMono (F.map f)
⊢ IsSplitMono f

Tactic:
exact IsSplitMono.mk' ((splitMonoEquiv F f).invFun h.exists_splitMono.some)

Premises used: Nonempty.some, CategoryTheory.IsSplitMono.exists_splitMono, CategoryTheory.Functor.splitMonoEquiv, CategoryTheory.IsSplitMono.mk', Equiv.invFun
-- Module: Mathlib.CategoryTheory.Functor.EpiMono
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
X Y : C
f : X ⟶ Y
inst_2 : F.Full
inst_3 : F.Faithful
h : IsSplitMono f
⊢ IsSplitMono (F.map f)

Tactic:
IsSplitMono.mk' ((splitMonoEquiv F f).toFun h.exists_splitMono.some)

Premises used: Nonempty.some, CategoryTheory.IsSplitMono.exists_splitMono, Equiv.toFun, CategoryTheory.Functor.splitMonoEquiv, CategoryTheory.IsSplitMono.mk'
-- Module: Mathlib.CategoryTheory.Functor.EpiMono
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
X Y : C
f : X ⟶ Y
inst_2 : F.Full
inst_3 : F.Faithful
h : IsSplitMono f
⊢ IsSplitMono (F.map f)

Tactic:
exact IsSplitMono.mk' ((splitMonoEquiv F f).toFun h.exists_splitMono.some)

Premises used: Nonempty.some, CategoryTheory.IsSplitMono.exists_splitMono, Equiv.toFun, CategoryTheory.Functor.splitMonoEquiv, CategoryTheory.IsSplitMono.mk'
-- Module: Mathlib.CategoryTheory.Functor.EpiMono
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
X Y : C
f : X ⟶ Y
hF₁ : F.PreservesEpimorphisms
hF₂ : F.ReflectsEpimorphisms
mp : Epi (F.map f) → Epi f
mpr : Epi f → Epi (F.map f)
⊢ Epi (F.map f) ↔ Epi f

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.Functor.EpiMono
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
X Y : C
f : X ⟶ Y
hF₁ : F.PreservesEpimorphisms
hF₂ : F.ReflectsEpimorphisms
⊢ Epi (F.map f) → Epi f

Tactic:
F.epi_of_epi_map

Premises used: CategoryTheory.Functor.epi_of_epi_map
-- Module: Mathlib.CategoryTheory.Functor.EpiMono
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
X Y : C
f : X ⟶ Y
hF₁ : F.PreservesEpimorphisms
hF₂ : F.ReflectsEpimorphisms
⊢ Epi (F.map f) → Epi f

Tactic:
exact F.epi_of_epi_map

Premises used: CategoryTheory.Functor.epi_of_epi_map
-- Module: Mathlib.CategoryTheory.Functor.EpiMono
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
X Y : C
f : X ⟶ Y
hF₁ : F.PreservesEpimorphisms
hF₂ : F.ReflectsEpimorphisms
h : Epi f
⊢ Epi (F.map f)

Tactic:
F.map_epi f

Premises used: CategoryTheory.Functor.map_epi
-- Module: Mathlib.CategoryTheory.Functor.EpiMono
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
X Y : C
f : X ⟶ Y
hF₁ : F.PreservesEpimorphisms
hF₂ : F.ReflectsEpimorphisms
h : Epi f
⊢ Epi (F.map f)

Tactic:
exact F.map_epi f

Premises used: CategoryTheory.Functor.map_epi
-- Module: Mathlib.CategoryTheory.Functor.EpiMono
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
X Y : C
f : X ⟶ Y
hF₁ : F.PreservesMonomorphisms
hF₂ : F.ReflectsMonomorphisms
mp : Mono (F.map f) → Mono f
mpr : Mono f → Mono (F.map f)
⊢ Mono (F.map f) ↔ Mono f

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.Functor.EpiMono
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
X Y : C
f : X ⟶ Y
hF₁ : F.PreservesMonomorphisms
hF₂ : F.ReflectsMonomorphisms
⊢ Mono (F.map f) → Mono f

Tactic:
F.mono_of_mono_map

Premises used: CategoryTheory.Functor.mono_of_mono_map
-- Module: Mathlib.CategoryTheory.Functor.EpiMono
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
X Y : C
f : X ⟶ Y
hF₁ : F.PreservesMonomorphisms
hF₂ : F.ReflectsMonomorphisms
⊢ Mono (F.map f) → Mono f

Tactic:
exact F.mono_of_mono_map

Premises used: CategoryTheory.Functor.mono_of_mono_map
-- Module: Mathlib.CategoryTheory.Functor.EpiMono
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
X Y : C
f : X ⟶ Y
hF₁ : F.PreservesMonomorphisms
hF₂ : F.ReflectsMonomorphisms
h : Mono f
⊢ Mono (F.map f)

Tactic:
F.map_mono f

Premises used: CategoryTheory.Functor.map_mono
-- Module: Mathlib.CategoryTheory.Functor.EpiMono
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
X Y : C
f : X ⟶ Y
hF₁ : F.PreservesMonomorphisms
hF₂ : F.ReflectsMonomorphisms
h : Mono f
⊢ Mono (F.map f)

Tactic:
exact F.map_mono f

Premises used: CategoryTheory.Functor.map_mono
-- Module: Mathlib.CategoryTheory.Functor.EpiMono
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : F.IsEquivalence
inst_3 : SplitEpiCategory.{v₁, u₁} C
X Y : D
f : X ⟶ Y
inst_4 : Epi f
rw : IsSplitEpi (F.inv.map f)
⊢ IsSplitEpi f

Tactic:
rw [← F.inv.isSplitEpi_iff f]

Premises used: CategoryTheory.Functor.inv, CategoryTheory.Functor.isSplitEpi_iff
-- Module: Mathlib.CategoryTheory.Functor.EpiMono
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : F.IsEquivalence
inst_3 : SplitEpiCategory.{v₁, u₁} C
X Y : D
f : X ⟶ Y
inst_4 : Epi f
⊢ IsSplitEpi (F.inv.map f)

Tactic:
apply isSplitEpi_of_epi

Premises used: CategoryTheory.isSplitEpi_of_epi
-- Module: Mathlib.CategoryTheory.Functor.EpiMono
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
F' : Functor.{v_2, v_1, u_2, u_1} D C
A B : C
adj : F ⊣ F'
f : A ⟶ B
inst_2 : F'.PreservesMonomorphisms
inst_3 : F.PreservesEpimorphisms
inst_4 : StrongEpi f
X Y : D
Z : X ⟶ Y
inst_5 : Mono Z
rw : HasLiftingProperty f (F'.map Z)
⊢ HasLiftingProperty (F.map f) Z

Tactic:
rw [adj.hasLiftingProperty_iff]

Premises used: CategoryTheory.Adjunction.hasLiftingProperty_iff
-- Module: Mathlib.CategoryTheory.Functor.EpiMono
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
F' : Functor.{v_2, v_1, u_2, u_1} D C
A B : C
adj : F ⊣ F'
f : A ⟶ B
inst_2 : F'.PreservesMonomorphisms
inst_3 : F.PreservesEpimorphisms
inst_4 : StrongEpi f
X Y : D
Z : X ⟶ Y
inst_5 : Mono Z
⊢ HasLiftingProperty f (F'.map Z)

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Functor.EpiMono
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
F' : Functor.{v_2, v_1, u_2, u_1} D C
A B : C
inst_2 : F.IsEquivalence
f : A ⟶ B
_h : StrongEpi f
⊢ StrongEpi (F.map f)

Tactic:
F.asEquivalence.toAdjunction.strongEpi_map_of_strongEpi f

Premises used: CategoryTheory.Adjunction.strongEpi_map_of_strongEpi, CategoryTheory.Functor.asEquivalence, CategoryTheory.Equivalence.toAdjunction
-- Module: Mathlib.CategoryTheory.Functor.EpiMono
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
F' : Functor.{v_2, v_1, u_2, u_1} D C
A B : C
adj : F ⊣ F'
X : C
Y : D
f : F.obj X ⟶ Y
hf : Mono f
inst_2 : F.ReflectsMonomorphisms
⊢ Mono.{v_2, u_2} (C := D) (X := F.obj X) (Y := Y)
    (((adj.homEquiv X Y).symm : (a : X ⟶ F'.obj Y) → F.obj X ⟶ Y)
        ((adj.homEquiv X Y : (a : F.obj X ⟶ Y) → X ⟶ F'.obj Y) f) :
      F.obj X ⟶ Y)

Tactic:
rw [← (homEquiv adj X Y).symm_apply_apply f] at hf

Premises used: Equiv.symm_apply_apply, CategoryTheory.Adjunction.homEquiv
-- Module: Mathlib.CategoryTheory.Functor.EpiMono
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
F' : Functor.{v_2, v_1, u_2, u_1} D C
A B : C
adj : F ⊣ F'
X : C
Y : D
f : F.obj X ⟶ Y
hf : Mono f
inst_2 : F.ReflectsMonomorphisms
hf₁ :
  Mono.{v_2, u_2} (C := D) (X := F.obj X) (Y := Y)
    (((adj.homEquiv X Y).symm : (a : X ⟶ F'.obj Y) → F.obj X ⟶ Y)
        ((adj.homEquiv X Y : (a : F.obj X ⟶ Y) → X ⟶ F'.obj Y) f) :
      F.obj X ⟶ Y)
⊢ F.ReflectsMonomorphisms

Tactic:
rw [← (homEquiv adj X Y).symm_apply_apply f] at hf

Premises used: Equiv.symm_apply_apply, CategoryTheory.Adjunction.homEquiv