awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Functor.Derived.RightDerived
Goal:
C : Type u_1
D : Type u_3
H : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_3, u_3} D
inst_2 : Category.{v_5, u_2} H
RF RF' : Functor.{v_3, v_5, u_3, u_2} D H
F : Functor.{v_1, v_5, u_1, u_2} C H
L : Functor.{v_1, v_3, u_1, u_3} C D
α : F ⟶ L ⋙ RF
α' : F ⟶ L ⋙ RF'
W : MorphismProperty.{v_1, u_1} C
inst_3 : L.IsLocalization W
e : RF ≅ RF'
comm : α ≫ L.whiskerLeft e.hom = α'
⊢ RF.IsLeftKanExtension α ↔ RF'.IsLeftKanExtension α'

Tactic:
exact isLeftKanExtension_iff_of_iso e _ _ comm

Premises used: CategoryTheory.Functor.isLeftKanExtension_iff_of_iso
-- Module: Mathlib.CategoryTheory.Functor.Derived.RightDerived
Goal:
C : Type u_3
D : Type u_1
H : Type u_2
inst : Category.{v_1, u_3} C
inst_1 : Category.{v_3, u_1} D
inst_2 : Category.{v_5, u_2} H
RF : Functor.{v_3, v_5, u_1, u_2} D H
F : Functor.{v_1, v_5, u_3, u_2} C H
L : Functor.{v_1, v_3, u_3, u_1} C D
α : F ⟶ L ⋙ RF
W : MorphismProperty.{v_1, u_3} C
inst_3 : L.IsLocalization W
inst_4 : RF.IsRightDerivedFunctor α W
G : Functor.{v_3, v_5, u_1, u_2} D H
β : F ⟶ L ⋙ G
⊢ α ≫ L.whiskerLeft (RF.rightDerivedDesc α W G β) = β

Tactic:
have := IsRightDerivedFunctor.isLeftKanExtension RF α W
  RF.descOfIsLeftKanExtension_fac α G β

Premises used: CategoryTheory.Functor.IsRightDerivedFunctor.isLeftKanExtension, CategoryTheory.Functor.rightDerivedDesc, CategoryTheory.Functor.descOfIsLeftKanExtension_fac
-- Module: Mathlib.CategoryTheory.Functor.Derived.RightDerived
Goal:
C : Type u_3
D : Type u_1
H : Type u_2
inst : Category.{v_1, u_3} C
inst_1 : Category.{v_3, u_1} D
inst_2 : Category.{v_5, u_2} H
RF : Functor.{v_3, v_5, u_1, u_2} D H
F : Functor.{v_1, v_5, u_3, u_2} C H
L : Functor.{v_1, v_3, u_3, u_1} C D
α : F ⟶ L ⋙ RF
W : MorphismProperty.{v_1, u_3} C
inst_3 : L.IsLocalization W
inst_4 : RF.IsRightDerivedFunctor α W
G : Functor.{v_3, v_5, u_1, u_2} D H
β : F ⟶ L ⋙ G
X : C
⊢ α.app X ≫ (RF.rightDerivedDesc α W G β).app (L.obj X) = β.app X

Tactic:
have := IsRightDerivedFunctor.isLeftKanExtension RF α W
  RF.descOfIsLeftKanExtension_fac_app α G β X

Premises used: CategoryTheory.Functor.IsRightDerivedFunctor.isLeftKanExtension, CategoryTheory.Functor.descOfIsLeftKanExtension_fac_app
-- Module: Mathlib.CategoryTheory.Functor.Derived.RightDerived
Goal:
C : Type u_3
D : Type u_1
H : Type u_2
inst : Category.{v_1, u_3} C
inst_1 : Category.{v_3, u_1} D
inst_2 : Category.{v_5, u_2} H
RF : Functor.{v_3, v_5, u_1, u_2} D H
F : Functor.{v_1, v_5, u_3, u_2} C H
L : Functor.{v_1, v_3, u_3, u_1} C D
α : F ⟶ L ⋙ RF
W : MorphismProperty.{v_1, u_3} C
inst_3 : L.IsLocalization W
inst_4 : RF.IsRightDerivedFunctor α W
G : Functor.{v_3, v_5, u_1, u_2} D H
γ₁ γ₂ : RF ⟶ G
hγ : α ≫ L.whiskerLeft γ₁ = α ≫ L.whiskerLeft γ₂
⊢ γ₁ = γ₂

Tactic:
have := IsRightDerivedFunctor.isLeftKanExtension RF α W
  RF.hom_ext_of_isLeftKanExtension α γ₁ γ₂ hγ

Premises used: CategoryTheory.Functor.IsRightDerivedFunctor.isLeftKanExtension, CategoryTheory.Functor.hom_ext_of_isLeftKanExtension
-- Module: Mathlib.CategoryTheory.Functor.Derived.RightDerived
Goal:
C : Type u_1
D : Type u_3
H : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_3, u_3} D
inst_2 : Category.{v_5, u_2} H
RF RF' : Functor.{v_3, v_5, u_3, u_2} D H
F F' : Functor.{v_1, v_5, u_1, u_2} C H
L : Functor.{v_1, v_3, u_1, u_3} C D
α : F ⟶ L ⋙ RF
α' : F' ⟶ L ⋙ RF'
W : MorphismProperty.{v_1, u_1} C
inst_3 : L.IsLocalization W
inst_4 : RF.IsRightDerivedFunctor α W
τ : F ⟶ F'
⊢ α ≫ L.whiskerLeft (RF.rightDerivedDesc α W RF' (τ ≫ α')) = τ ≫ α'

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Functor.Derived.RightDerived
Goal:
C : Type u_1
D : Type u_3
H : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_3, u_3} D
inst_2 : Category.{v_5, u_2} H
RF RF' : Functor.{v_3, v_5, u_3, u_2} D H
F F' : Functor.{v_1, v_5, u_1, u_2} C H
L : Functor.{v_1, v_3, u_1, u_3} C D
α : F ⟶ L ⋙ RF
α' : F' ⟶ L ⋙ RF'
W : MorphismProperty.{v_1, u_1} C
inst_3 : L.IsLocalization W
inst_4 : RF.IsRightDerivedFunctor α W
τ : F ⟶ F'
X : C
dsimp : α.app X ≫ (RF.rightDerivedDesc α W RF' (τ ≫ α')).app (L.obj X) = τ.app X ≫ α'.app X
⊢ α.app X ≫ (RF.rightDerivedNatTrans RF' α α' W τ).app (L.obj X) = τ.app X ≫ α'.app X

Tactic:
dsimp only [rightDerivedNatTrans]

Premises used: CategoryTheory.Functor.rightDerivedNatTrans
-- Module: Mathlib.CategoryTheory.Functor.Derived.RightDerived
Goal:
C : Type u_1
D : Type u_3
H : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_3, u_3} D
inst_2 : Category.{v_5, u_2} H
RF RF' : Functor.{v_3, v_5, u_3, u_2} D H
F F' : Functor.{v_1, v_5, u_1, u_2} C H
L : Functor.{v_1, v_3, u_1, u_3} C D
α : F ⟶ L ⋙ RF
α' : F' ⟶ L ⋙ RF'
W : MorphismProperty.{v_1, u_1} C
inst_3 : L.IsLocalization W
inst_4 : RF.IsRightDerivedFunctor α W
τ : F ⟶ F'
X : C
⊢ α.app X ≫ (RF.rightDerivedDesc α W RF' (τ ≫ α')).app (L.obj X) = τ.app X ≫ α'.app X

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Functor.Derived.RightDerived
Goal:
C : Type u_3
D : Type u_1
H : Type u_2
inst : Category.{v_1, u_3} C
inst_1 : Category.{v_3, u_1} D
inst_2 : Category.{v_5, u_2} H
RF : Functor.{v_3, v_5, u_1, u_2} D H
F : Functor.{v_1, v_5, u_3, u_2} C H
L : Functor.{v_1, v_3, u_3, u_1} C D
α : F ⟶ L ⋙ RF
W : MorphismProperty.{v_1, u_3} C
inst_3 : L.IsLocalization W
inst_4 : RF.IsRightDerivedFunctor α W
⊢ α ≫ L.whiskerLeft (RF.rightDerivedNatTrans RF α α W (𝟙 F)) = α ≫ L.whiskerLeft (𝟙 RF)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Functor.Derived.RightDerived
Goal:
C : Type u_1
D : Type u_3
H : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_3, u_3} D
inst_2 : Category.{v_5, u_2} H
RF RF' RF'' : Functor.{v_3, v_5, u_3, u_2} D H
F F' F'' : Functor.{v_1, v_5, u_1, u_2} C H
L : Functor.{v_1, v_3, u_1, u_3} C D
α : F ⟶ L ⋙ RF
α' : F' ⟶ L ⋙ RF'
α'' : F'' ⟶ L ⋙ RF''
W : MorphismProperty.{v_1, u_1} C
inst_3 : L.IsLocalization W
inst_4 : RF.IsRightDerivedFunctor α W
inst_5 : RF'.IsRightDerivedFunctor α' W
τ : F ⟶ F'
τ' : F' ⟶ F''
⊢ α ≫ L.whiskerLeft (RF.rightDerivedNatTrans RF' α α' W τ ≫ RF'.rightDerivedNatTrans RF'' α' α'' W τ') =
    α ≫ L.whiskerLeft (RF.rightDerivedNatTrans RF'' α α'' W (τ ≫ τ'))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Functor.Derived.RightDerived
Goal:
C : Type u_3
D : Type u_1
H : Type u_2
inst : Category.{v_1, u_3} C
inst_1 : Category.{v_3, u_1} D
inst_2 : Category.{v_5, u_2} H
RF : Functor.{v_3, v_5, u_1, u_2} D H
F : Functor.{v_1, v_5, u_3, u_2} C H
L : Functor.{v_1, v_3, u_3, u_1} C D
α : F ⟶ L ⋙ RF
W : MorphismProperty.{v_1, u_3} C
inst_3 : L.IsLocalization W
inst_4 : RF.IsRightDerivedFunctor α W
G : Functor.{v_3, v_5, u_1, u_2} D H
β : F ⟶ L ⋙ G
rw : G.IsLeftKanExtension β ↔ IsIso (RF.rightDerivedDesc α W G β)
⊢ G.IsRightDerivedFunctor β W ↔ IsIso (RF.rightDerivedDesc α W G β)

Tactic:
rw [isRightDerivedFunctor_iff_isLeftKanExtension]

Premises used: CategoryTheory.Functor.isRightDerivedFunctor_iff_isLeftKanExtension
-- Module: Mathlib.CategoryTheory.Functor.Derived.RightDerived
Goal:
C : Type u_3
D : Type u_1
H : Type u_2
inst : Category.{v_1, u_3} C
inst_1 : Category.{v_3, u_1} D
inst_2 : Category.{v_5, u_2} H
RF : Functor.{v_3, v_5, u_1, u_2} D H
F : Functor.{v_1, v_5, u_3, u_2} C H
L : Functor.{v_1, v_3, u_3, u_1} C D
α : F ⟶ L ⋙ RF
W : MorphismProperty.{v_1, u_3} C
inst_3 : L.IsLocalization W
inst_4 : RF.IsRightDerivedFunctor α W
G : Functor.{v_3, v_5, u_1, u_2} D H
β : F ⟶ L ⋙ G
⊢ RF.IsLeftKanExtension α

Tactic:
have := IsRightDerivedFunctor.isLeftKanExtension _ α W
-- Module: Mathlib.CategoryTheory.Functor.Derived.RightDerived
Goal:
C : Type u_3
D : Type u_1
H : Type u_2
inst : Category.{v_1, u_3} C
inst_1 : Category.{v_3, u_1} D
inst_2 : Category.{v_5, u_2} H
RF : Functor.{v_3, v_5, u_1, u_2} D H
F : Functor.{v_1, v_5, u_3, u_2} C H
L : Functor.{v_1, v_3, u_3, u_1} C D
α : F ⟶ L ⋙ RF
W : MorphismProperty.{v_1, u_3} C
inst_3 : L.IsLocalization W
inst_4 : RF.IsRightDerivedFunctor α W
G : Functor.{v_3, v_5, u_1, u_2} D H
β : F ⟶ L ⋙ G
this : RF.IsLeftKanExtension α
⊢ α ≫ L.whiskerLeft (RF.rightDerivedDesc α W G β) = β

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Functor.Derived.RightDerived
Goal:
C : Type u_3
D : Type u_1
H : Type u_2
inst : Category.{v_1, u_3} C
inst_1 : Category.{v_3, u_1} D
inst_2 : Category.{v_5, u_2} H
RF : Functor.{v_3, v_5, u_1, u_2} D H
F : Functor.{v_1, v_5, u_3, u_2} C H
L : Functor.{v_1, v_3, u_3, u_1} C D
α : F ⟶ L ⋙ RF
W : MorphismProperty.{v_1, u_3} C
inst_3 : L.IsLocalization W
inst_4 : RF.IsRightDerivedFunctor α W
G : Functor.{v_3, v_5, u_1, u_2} D H
β : F ⟶ L ⋙ G
this : RF.IsLeftKanExtension α
⊢ G.IsLeftKanExtension β ↔ IsIso (RF.rightDerivedDesc α W G β)

Tactic:
exact isLeftKanExtension_iff_isIso _ α _ (by simp)

Premises used: CategoryTheory.Functor.isLeftKanExtension_iff_isIso
-- Module: Mathlib.CategoryTheory.Functor.Derived.RightDerived
Goal:
C : Type u_1
D : Type u_3
H : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_3, u_3} D
inst_2 : Category.{v_5, u_2} H
F : Functor.{v_1, v_5, u_1, u_2} C H
L : Functor.{v_1, v_3, u_1, u_3} C D
W : MorphismProperty.{v_1, u_1} C
inst_3 : L.IsLocalization W
⊢ F.HasRightDerivedFunctor W ↔ W.Q.HasLeftKanExtension F

Tactic:
have : HasRightDerivedFunctor F W ↔ HasLeftKanExtension W.Q F :=
    ⟨fun h => h.hasLeftKanExtension', fun h => ⟨h⟩⟩
-- Module: Mathlib.CategoryTheory.Functor.Derived.RightDerived
Goal:
C : Type u_1
D : Type u_3
H : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_3, u_3} D
inst_2 : Category.{v_5, u_2} H
F : Functor.{v_1, v_5, u_1, u_2} C H
L : Functor.{v_1, v_3, u_1, u_3} C D
W : MorphismProperty.{v_1, u_1} C
inst_3 : L.IsLocalization W
this : F.HasRightDerivedFunctor W ↔ W.Q.HasLeftKanExtension F
rw : W.Q.HasLeftKanExtension F ↔ L.HasLeftKanExtension F
rw₁ rw₂ : W.Q.HasLeftKanExtension F ↔ W.Q.HasLeftKanExtension F
⊢ F.HasRightDerivedFunctor W ↔ L.HasLeftKanExtension F

Tactic:
rw [this, hasLeftExtension_iff_postcomp₁ (Localization.compUniqFunctor W.Q L W) F]

Premises used: CategoryTheory.MorphismProperty.Q, CategoryTheory.Localization.compUniqFunctor, CategoryTheory.Functor.hasLeftExtension_iff_postcomp₁
-- Module: Mathlib.CategoryTheory.Functor.Derived.RightDerived
Goal:
C : Type u_1
H : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_5, u_2} H
F F' : Functor.{v_1, v_5, u_1, u_2} C H
e : F ≅ F'
W : MorphismProperty.{v_1, u_1} C
rw : W.Q.HasLeftKanExtension F ↔ F'.HasRightDerivedFunctor W
rw₁ : W.Q.HasLeftKanExtension F ↔ W.Q.HasLeftKanExtension F'
rw₂ rw₃ : W.Q.HasLeftKanExtension F' ↔ W.Q.HasLeftKanExtension F'
⊢ F.HasRightDerivedFunctor W ↔ F'.HasRightDerivedFunctor W

Tactic:
rw [hasRightDerivedFunctor_iff F W.Q W, hasRightDerivedFunctor_iff F' W.Q W,
    hasLeftExtension_iff_of_iso₂ W.Q e]

Premises used: CategoryTheory.Functor.hasRightDerivedFunctor_iff, CategoryTheory.MorphismProperty.Q, CategoryTheory.Functor.hasLeftExtension_iff_of_iso₂
-- Module: Mathlib.CategoryTheory.Functor.Derived.RightDerived
Goal:
C : Type u_1
D : Type u_3
H : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_3, u_3} D
inst_2 : Category.{v_5, u_2} H
F : Functor.{v_1, v_5, u_1, u_2} C H
L : Functor.{v_1, v_3, u_1, u_3} C D
W : MorphismProperty.{v_1, u_1} C
inst_3 : L.IsLocalization W
inst_4 : F.HasRightDerivedFunctor W
⊢ L.HasLeftKanExtension F

Tactic:
simpa only [← hasRightDerivedFunctor_iff F L W]

Premises used: CategoryTheory.Functor.hasRightDerivedFunctor_iff
-- Module: Mathlib.CategoryTheory.Functor.Derived.RightDerived
Goal:
C : Type u_1
D : Type u_2
H : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_3, u_2} D
inst_2 : Category.{v_5, u_3} H
RF : Functor.{v_3, v_5, u_2, u_3} D H
F : Functor.{v_1, v_5, u_1, u_3} C H
L : Functor.{v_1, v_3, u_1, u_2} C D
α : F ⟶ L ⋙ RF
W : MorphismProperty.{v_1, u_1} C
inst_3 : L.IsLocalization W
inst_4 : RF.IsRightDerivedFunctor α W
⊢ RF.IsLeftKanExtension α

Tactic:
have := IsRightDerivedFunctor.isLeftKanExtension RF α W
-- Module: Mathlib.CategoryTheory.Functor.Derived.RightDerived
Goal:
C : Type u_1
D : Type u_2
H : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_3, u_2} D
inst_2 : Category.{v_5, u_3} H
RF : Functor.{v_3, v_5, u_2, u_3} D H
F : Functor.{v_1, v_5, u_1, u_3} C H
L : Functor.{v_1, v_3, u_1, u_2} C D
α : F ⟶ L ⋙ RF
W : MorphismProperty.{v_1, u_1} C
inst_3 : L.IsLocalization W
inst_4 : RF.IsRightDerivedFunctor α W
this : RF.IsLeftKanExtension α
⊢ F.HasRightDerivedFunctor W

Tactic:
simpa only [hasRightDerivedFunctor_iff F L W] using HasLeftKanExtension.mk RF α

Premises used: CategoryTheory.Functor.hasRightDerivedFunctor_iff, CategoryTheory.Functor.HasLeftKanExtension.mk
-- Module: Mathlib.CategoryTheory.Functor.Derived.RightDerived
Goal:
C : Type u_1
C' : Type ?u.109543
D : Type u_2
D' : Type ?u.109549
H : Type u_3
H' : Type ?u.109555
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, ?u.109543} C'
inst_2 : Category.{v_3, u_2} D
inst_3 : Category.{v_4, ?u.109549} D'
inst_4 : Category.{v_5, u_3} H
inst_5 : Category.{v_6, ?u.109555} H'
RF RF' RF'' : Functor.{v_3, v_5, u_2, u_3} D H
F F' F'' : Functor.{v_1, v_5, u_1, u_3} C H
e : F ≅ F'
L : Functor.{v_1, v_3, u_1, u_2} C D
α : F ⟶ L ⋙ RF
α' : F' ⟶ L ⋙ RF'
α'' : F'' ⟶ L ⋙ RF''
α'₂ : F ⟶ L ⋙ RF'
W : MorphismProperty.{v_1, u_1} C
inst_6 : L.IsLocalization W
inst_7 : F.HasRightDerivedFunctor W
⊢ (L.leftKanExtension F).IsLeftKanExtension (L.leftKanExtensionUnit F)

Tactic:
infer_instance
-- 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.PreservesMonomorphisms
X Y : C
f : X ⟶ Y
inst_4 : Mono f
⊢ Mono (F.map f)

Tactic:
PreservesMonomorphisms.preserves f

Premises used: CategoryTheory.Functor.PreservesMonomorphisms.preserves
-- 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.PreservesEpimorphisms
X Y : C
f : X ⟶ Y
inst_4 : Epi f
⊢ Epi (F.map f)

Tactic:
PreservesEpimorphisms.preserves f

Premises used: CategoryTheory.Functor.PreservesEpimorphisms.preserves
-- 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.ReflectsMonomorphisms
X Y : C
f : X ⟶ Y
h : Mono (F.map f)
⊢ Mono f

Tactic:
ReflectsMonomorphisms.reflects f h

Premises used: CategoryTheory.Functor.ReflectsMonomorphisms.reflects
-- 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.ReflectsEpimorphisms
X Y : C
f : X ⟶ Y
h : Epi (F.map f)
⊢ Epi f

Tactic:
ReflectsEpimorphisms.reflects f h

Premises used: CategoryTheory.Functor.ReflectsEpimorphisms.reflects
-- 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
G : Functor.{v₂, v₃, u₂, u₃} D E
inst_3 : F.PreservesMonomorphisms
inst_4 : G.PreservesMonomorphisms
X Y : C
f : X ⟶ Y
h : Mono f
rw : Mono (G.map (F.map f))
⊢ Mono ((F ⋙ G).map f)

Tactic:
rw [comp_map]

Premises used: CategoryTheory.Functor.comp_map
-- 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
G : Functor.{v₂, v₃, u₂, u₃} D E
inst_3 : F.PreservesMonomorphisms
inst_4 : G.PreservesMonomorphisms
X Y : C
f : X ⟶ Y
h : Mono f
⊢ Mono (G.map (F.map f))

Tactic:
inferInstance

Premises used: inferInstance
-- 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
G : Functor.{v₂, v₃, u₂, u₃} D E
inst_3 : F.PreservesMonomorphisms
inst_4 : G.PreservesMonomorphisms
X Y : C
f : X ⟶ Y
h : Mono f
⊢ Mono (G.map (F.map f))

Tactic:
exact inferInstance
-- 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
G : Functor.{v₂, v₃, u₂, u₃} D E
inst_3 : F.PreservesEpimorphisms
inst_4 : G.PreservesEpimorphisms
X Y : C
f : X ⟶ Y
h : Epi f
rw : Epi (G.map (F.map f))
⊢ Epi ((F ⋙ G).map f)

Tactic:
rw [comp_map]

Premises used: CategoryTheory.Functor.comp_map
-- 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
G : Functor.{v₂, v₃, u₂, u₃} D E
inst_3 : F.PreservesEpimorphisms
inst_4 : G.PreservesEpimorphisms
X Y : C
f : X ⟶ Y
h : Epi f
⊢ Epi (G.map (F.map f))

Tactic:
inferInstance

Premises used: inferInstance
-- 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
G : Functor.{v₂, v₃, u₂, u₃} D E
inst_3 : F.PreservesEpimorphisms
inst_4 : G.PreservesEpimorphisms
X Y : C
f : X ⟶ Y
h : Epi f
⊢ Epi (G.map (F.map f))

Tactic:
exact inferInstance
-- 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
G : Functor.{v₂, v₃, u₂, u₃} D E
inst_3 : (F ⋙ G).PreservesEpimorphisms
inst_4 : G.ReflectsEpimorphisms
⊢ F.PreservesEpimorphisms

Tactic:
⟨fun f _ => G.epi_of_epi_map <| show Epi ((F ⋙ G).map f) from inferInstance⟩

Premises used: inferInstance, CategoryTheory.Functor.PreservesEpimorphisms.mk, 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
E : Type u₃
inst_2 : Category.{v₃, u₃} E
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₃, u₂, u₃} D E
inst_3 : (F ⋙ G).PreservesMonomorphisms
inst_4 : G.ReflectsMonomorphisms
⊢ F.PreservesMonomorphisms

Tactic:
⟨fun f _ => G.mono_of_mono_map <| show Mono ((F ⋙ G).map f) from inferInstance⟩

Premises used: inferInstance, CategoryTheory.Functor.PreservesMonomorphisms.mk, 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
E : Type u₃
inst_2 : Category.{v₃, u₃} E
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₃, u₂, u₃} D E
inst_3 : G.PreservesEpimorphisms
inst_4 : (F ⋙ G).ReflectsEpimorphisms
⊢ F.ReflectsEpimorphisms

Tactic:
⟨fun f _ => (F ⋙ G).epi_of_epi_map <| show Epi (G.map (F.map f)) from inferInstance⟩

Premises used: CategoryTheory.Functor.comp, inferInstance, CategoryTheory.Functor.epi_of_epi_map, CategoryTheory.Functor.ReflectsEpimorphisms.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
G : Functor.{v₂, v₃, u₂, u₃} D E
inst_3 : G.PreservesMonomorphisms
inst_4 : (F ⋙ G).ReflectsMonomorphisms
⊢ F.ReflectsMonomorphisms

Tactic:
⟨fun f _ => (F ⋙ G).mono_of_mono_map <| show Mono (G.map (F.map f)) from inferInstance⟩

Premises used: CategoryTheory.Functor.ReflectsMonomorphisms.mk, CategoryTheory.Functor.comp, inferInstance, 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 G : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : F.PreservesMonomorphisms
f : G ⟶ F
inst_3 : ∀ (X : C), Mono (f.app X)
X Y : C
π : X ⟶ Y
hπ : Mono π
suffices : Mono (G.map π ≫ f.app Y)
⊢ Mono (G.map π)

Tactic:
suffices Mono (G.map π ≫ f.app Y) from mono_of_mono (G.map π) (f.app Y)
-- 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.PreservesMonomorphisms
f : G ⟶ F
inst_3 : ∀ (X : C), Mono (f.app X)
X Y : C
π : X ⟶ Y
hπ : Mono π
rw : Mono (f.app X ≫ F.map π)
⊢ Mono (G.map π ≫ f.app Y)

Tactic:
rw [f.naturality π]

Premises used: CategoryTheory.NatTrans.naturality
-- 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.PreservesMonomorphisms
f : G ⟶ F
inst_3 : ∀ (X : C), Mono (f.app X)
X Y : C
π : X ⟶ Y
hπ : Mono π
⊢ Mono (f.app X ≫ F.map π)

Tactic:
infer_instance
-- 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.PreservesMonomorphisms
α : F ≅ G
⊢ G.PreservesMonomorphisms

Tactic:
of_natTrans α.inv

Premises used: CategoryTheory.Functor.preservesMonomorphisms.of_natTrans, CategoryTheory.Iso.inv
-- 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.PreservesMonomorphisms ↔ G.PreservesMonomorphisms

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

Premises used: CategoryTheory.Functor.preservesMonomorphisms.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.PreservesEpimorphisms
f : F ⟶ G
inst_3 : ∀ (X : C), Epi (f.app X)
X Y : C
π : X ⟶ Y
hπ : Epi π
suffices : Epi (f.app X ≫ G.map π)
⊢ Epi (G.map π)

Tactic:
suffices Epi (f.app X ≫ G.map π) from epi_of_epi (f.app X) (G.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.PreservesEpimorphisms
f : F ⟶ G
inst_3 : ∀ (X : C), Epi (f.app X)
X Y : C
π : X ⟶ Y
hπ : Epi π
rw : Epi (F.map π ≫ f.app Y)
⊢ Epi (f.app X ≫ G.map π)

Tactic:
rw [← f.naturality π]

Premises used: CategoryTheory.NatTrans.naturality
-- 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.PreservesEpimorphisms
f : F ⟶ G
inst_3 : ∀ (X : C), Epi (f.app X)
X Y : C
π : X ⟶ Y
hπ : Epi π
⊢ Epi (F.map π ≫ f.app Y)

Tactic:
infer_instance
-- 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.PreservesEpimorphisms
α : F ≅ G
⊢ G.PreservesEpimorphisms

Tactic:
of_natTrans α.hom

Premises used: CategoryTheory.Functor.preservesEpimorphisms.of_natTrans, CategoryTheory.Iso.hom
-- 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.PreservesEpimorphisms ↔ G.PreservesEpimorphisms

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

Premises used: CategoryTheory.Functor.preservesEpimorphisms.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.ReflectsMonomorphisms
α : F ≅ G
X Y : C
f : X ⟶ Y
h : Mono (G.map f)
apply : Mono (F.map f)
⊢ Mono f

Tactic:
apply 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 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)
suffices : F.map f = (α.app X).hom ≫ G.map f ≫ (α.app Y).inv
⊢ Mono (F.map f)

Tactic:
suffices F.map f = (α.app X).hom ≫ G.map f ≫ (α.app Y).inv from this ▸ mono_comp _ _