awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Enriched.Ordinary.Basic
Goal:
V : Type u'
inst : Category.{v', u'} V
inst_1 : MonoidalCategory.{v', u'} V
C : Type u
inst_2 : Category.{v, u} C
inst_3 : EnrichedOrdinaryCategory.{v', v, u, u'} V C
W_1 : Type u''
inst_4 : Category.{v'', u''} W_1
inst_5 : MonoidalCategory.{v'', u''} W_1
F_1 : Functor.{v', v'', u', u''} V W_1
inst_6 : F_1.LaxMonoidal
W : Type u''
inst_7 : Category.{v'', u''} W
inst_8 : MonoidalCategory.{v'', u''} W
F : Functor.{v', v'', u', u''} V W
inst_9 : F.LaxMonoidal
D : Type u
inst_10 : EnrichedCategory.{v', u', u} V D
e :
  (v : V) →
    Equiv.{v' + 1, v'' + 1} (tensorUnit.{v', u'} V (𝒞 := inst) ⟶ v) (tensorUnit.{v'', u''} W (𝒞 := inst_7) ⟶ F.obj v)
h :
  ∀ (v : V) (f : tensorUnit.{v', u'} V (𝒞 := inst) ⟶ v),
    Eq.{v'' + 1} (α := tensorUnit.{v'', u''} W (𝒞 := inst_7) ⟶ F.obj v)
      ((e v : (a : 𝟙_ V ⟶ v) → 𝟙_ W ⟶ F.obj v) f : tensorUnit.{v'', u''} W (𝒞 := inst_7) ⟶ F.obj v)
      (Functor.LaxMonoidal.ε F ≫ F.map f : tensorUnit.{v'', u''} W (𝒞 := inst_7) ⟶ F.obj v)
⊢ ∀ {X Y : TransportEnrichment F (ForgetEnrichment.{v', u', u} V D)} (f : X ⟶ Y),
    Eq (α :=
      Functor.obj.{v', v', u, u} (𝟭 (TransportEnrichment F (ForgetEnrichment.{v', u', u} V D))) X ⟶
        Functor.obj (forgetEnrichmentEquivFunctor F D e h ⋙ forgetEnrichmentEquivInverse F D e h) Y)
      (Functor.map (𝟭 (TransportEnrichment F (ForgetEnrichment.{v', u', u} V D))) f ≫
        Iso.hom
          ((fun (x : TransportEnrichment F (ForgetEnrichment.{v', u', u} V D)) ↦
              (Iso.refl (Functor.obj.{v', v', u, u} (𝟭 (TransportEnrichment F (ForgetEnrichment.{v', u', u} V D))) x) :
                Functor.obj.{v', v', u, u} (𝟭 (TransportEnrichment F (ForgetEnrichment.{v', u', u} V D))) x ≅
                  Functor.obj.{v', v', u, u} (𝟭 (TransportEnrichment F (ForgetEnrichment.{v', u', u} V D))) x))
            Y))
      (Iso.hom
          ((fun (x : TransportEnrichment F (ForgetEnrichment.{v', u', u} V D)) ↦
              (Iso.refl (Functor.obj.{v', v', u, u} (𝟭 (TransportEnrichment F (ForgetEnrichment.{v', u', u} V D))) x) :
                Functor.obj.{v', v', u, u} (𝟭 (TransportEnrichment F (ForgetEnrichment.{v', u', u} V D))) x ≅
                  Functor.obj.{v', v', u, u} (𝟭 (TransportEnrichment F (ForgetEnrichment.{v', u', u} V D))) x))
            X) ≫
        Functor.map (forgetEnrichmentEquivFunctor F D e h ⋙ forgetEnrichmentEquivInverse F D e h) f)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Enriched.Ordinary.Basic
Goal:
V : Type u'
inst : Category.{v', u'} V
inst_1 : MonoidalCategory.{v', u'} V
C : Type u
inst_2 : Category.{v, u} C
inst_3 : EnrichedOrdinaryCategory.{v', v, u, u'} V C
W_1 : Type u''
inst_4 : Category.{v'', u''} W_1
inst_5 : MonoidalCategory.{v'', u''} W_1
F_1 : Functor.{v', v'', u', u''} V W_1
inst_6 : F_1.LaxMonoidal
W : Type u''
inst_7 : Category.{v'', u''} W
inst_8 : MonoidalCategory.{v'', u''} W
F : Functor.{v', v'', u', u''} V W
inst_9 : F.LaxMonoidal
D : Type u
inst_10 : EnrichedCategory.{v', u', u} V D
e :
  (v : V) →
    Equiv.{v' + 1, v'' + 1} (tensorUnit.{v', u'} V (𝒞 := inst) ⟶ v) (tensorUnit.{v'', u''} W (𝒞 := inst_7) ⟶ F.obj v)
h :
  ∀ (v : V) (f : tensorUnit.{v', u'} V (𝒞 := inst) ⟶ v),
    Eq.{v'' + 1} (α := tensorUnit.{v'', u''} W (𝒞 := inst_7) ⟶ F.obj v)
      ((e v : (a : 𝟙_ V ⟶ v) → 𝟙_ W ⟶ F.obj v) f : tensorUnit.{v'', u''} W (𝒞 := inst_7) ⟶ F.obj v)
      (Functor.LaxMonoidal.ε F ≫ F.map f : tensorUnit.{v'', u''} W (𝒞 := inst_7) ⟶ F.obj v)
X Y : ForgetEnrichment.{v'', u'', u} W (TransportEnrichment F D)
f : X ⟶ Y
⊢ Eq (α :=
    Functor.obj (forgetEnrichmentEquivInverse F D e h ⋙ forgetEnrichmentEquivFunctor F D e h) X ⟶
      Functor.obj.{v'', v'', u, u} (𝟭 (ForgetEnrichment.{v'', u'', u} W (TransportEnrichment F D))) Y)
    (Functor.map (forgetEnrichmentEquivInverse F D e h ⋙ forgetEnrichmentEquivFunctor F D e h) f ≫
      Iso.hom
        ((fun (x : ForgetEnrichment.{v'', u'', u} W (TransportEnrichment F D)) ↦
            (Iso.refl (Functor.obj (forgetEnrichmentEquivInverse F D e h ⋙ forgetEnrichmentEquivFunctor F D e h) x) :
              Functor.obj (forgetEnrichmentEquivInverse F D e h ⋙ forgetEnrichmentEquivFunctor F D e h) x ≅
                Functor.obj (forgetEnrichmentEquivInverse F D e h ⋙ forgetEnrichmentEquivFunctor F D e h) x))
          Y))
    (Iso.hom
        ((fun (x : ForgetEnrichment.{v'', u'', u} W (TransportEnrichment F D)) ↦
            (Iso.refl (Functor.obj (forgetEnrichmentEquivInverse F D e h ⋙ forgetEnrichmentEquivFunctor F D e h) x) :
              Functor.obj (forgetEnrichmentEquivInverse F D e h ⋙ forgetEnrichmentEquivFunctor F D e h) x ≅
                Functor.obj (forgetEnrichmentEquivInverse F D e h ⋙ forgetEnrichmentEquivFunctor F D e h) x))
          X) ≫
      Functor.map (𝟭 (ForgetEnrichment.{v'', u'', u} W (TransportEnrichment F D))) f)

Tactic:
simp [ForgetEnrichment.to, ForgetEnrichment.of]

Premises used: CategoryTheory.ForgetEnrichment.of, CategoryTheory.ForgetEnrichment.to
-- Module: Mathlib.CategoryTheory.Enriched.Ordinary.Basic
Goal:
V : Type u'
inst : Category.{v', u'} V
inst_1 : MonoidalCategory.{v', u'} V
C : Type u
inst_2 : Category.{v, u} C
inst_3 : EnrichedOrdinaryCategory.{v', v, u, u'} V C
W_1 : Type u''
inst_4 : Category.{v'', u''} W_1
inst_5 : MonoidalCategory.{v'', u''} W_1
F_1 : Functor.{v', v'', u', u''} V W_1
inst_6 : F_1.LaxMonoidal
W : Type u''
inst_7 : Category.{v'', u''} W
inst_8 : MonoidalCategory.{v'', u''} W
F : Functor.{v', v'', u', u''} V W
inst_9 : F.LaxMonoidal
D : Type u
inst_10 : EnrichedCategory.{v', u', u} V D
e :
  (v : V) →
    Equiv.{v' + 1, v'' + 1} (tensorUnit.{v', u'} V (𝒞 := inst) ⟶ v) (tensorUnit.{v'', u''} W (𝒞 := inst_7) ⟶ F.obj v)
h :
  ∀ (v : V) (f : tensorUnit.{v', u'} V (𝒞 := inst) ⟶ v),
    Eq.{v'' + 1} (α := tensorUnit.{v'', u''} W (𝒞 := inst_7) ⟶ F.obj v)
      ((e v : (a : 𝟙_ V ⟶ v) → 𝟙_ W ⟶ F.obj v) f : tensorUnit.{v'', u''} W (𝒞 := inst_7) ⟶ F.obj v)
      (Functor.LaxMonoidal.ε F ≫ F.map f : tensorUnit.{v'', u''} W (𝒞 := inst_7) ⟶ F.obj v)
X : TransportEnrichment F (ForgetEnrichment.{v', u', u} V D)
rw :
  Eq.{v'' + 1} (α :=
    Quiver.Hom (V := ForgetEnrichment.{v'', u'', u} W (TransportEnrichment F D)) (ForgetEnrichment.of W X)
      (ForgetEnrichment.of W X))
    (ForgetEnrichment.homOf W (Functor.LaxMonoidal.ε F ≫ F.map (eId V (ForgetEnrichment.to V X))))
    (ForgetEnrichment.homOf W (Functor.LaxMonoidal.ε F ≫ F.map (eId V X)))
⊢ Eq.{v'' + 1} (α :=
    Quiver.Hom (V := ForgetEnrichment.{v'', u'', u} W (TransportEnrichment F D)) (ForgetEnrichment.of W X)
      (ForgetEnrichment.of W X))
    (ForgetEnrichment.homOf W (Functor.LaxMonoidal.ε F ≫ F.map (ForgetEnrichment.homTo V (𝟙 X))))
    (𝟙 (ForgetEnrichment.of W X))

Tactic:
rw [← ForgetEnrichment.homOf_eId, TransportEnrichment.eId_eq, ForgetEnrichment.homTo_id]

Premises used: CategoryTheory.TransportEnrichment.eId_eq, CategoryTheory.ForgetEnrichment.homOf_eId, CategoryTheory.ForgetEnrichment.homTo_id
-- Module: Mathlib.CategoryTheory.Enriched.Ordinary.Basic
Goal:
V : Type u'
inst : Category.{v', u'} V
inst_1 : MonoidalCategory.{v', u'} V
C : Type u
inst_2 : Category.{v, u} C
inst_3 : EnrichedOrdinaryCategory.{v', v, u, u'} V C
W_1 : Type u''
inst_4 : Category.{v'', u''} W_1
inst_5 : MonoidalCategory.{v'', u''} W_1
F_1 : Functor.{v', v'', u', u''} V W_1
inst_6 : F_1.LaxMonoidal
W : Type u''
inst_7 : Category.{v'', u''} W
inst_8 : MonoidalCategory.{v'', u''} W
F : Functor.{v', v'', u', u''} V W
inst_9 : F.LaxMonoidal
D : Type u
inst_10 : EnrichedCategory.{v', u', u} V D
e :
  (v : V) →
    Equiv.{v' + 1, v'' + 1} (tensorUnit.{v', u'} V (𝒞 := inst) ⟶ v) (tensorUnit.{v'', u''} W (𝒞 := inst_7) ⟶ F.obj v)
h :
  ∀ (v : V) (f : tensorUnit.{v', u'} V (𝒞 := inst) ⟶ v),
    Eq.{v'' + 1} (α := tensorUnit.{v'', u''} W (𝒞 := inst_7) ⟶ F.obj v)
      ((e v : (a : 𝟙_ V ⟶ v) → 𝟙_ W ⟶ F.obj v) f : tensorUnit.{v'', u''} W (𝒞 := inst_7) ⟶ F.obj v)
      (Functor.LaxMonoidal.ε F ≫ F.map f : tensorUnit.{v'', u''} W (𝒞 := inst_7) ⟶ F.obj v)
X : TransportEnrichment F (ForgetEnrichment.{v', u', u} V D)
⊢ Eq.{v'' + 1} (α :=
    Quiver.Hom (V := ForgetEnrichment.{v'', u'', u} W (TransportEnrichment F D)) (ForgetEnrichment.of W X)
      (ForgetEnrichment.of W X))
    (ForgetEnrichment.homOf W (Functor.LaxMonoidal.ε F ≫ F.map (eId V (ForgetEnrichment.to V X))))
    (ForgetEnrichment.homOf W (Functor.LaxMonoidal.ε F ≫ F.map (eId V X)))

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Enriched.Ordinary.Basic
Goal:
V_1 : Type u'
inst : Category.{v', u'} V_1
inst_1 : MonoidalCategory.{v', u'} V_1
C_1 : Type u
inst_2 : Category.{v, u} C_1
inst_3 : EnrichedOrdinaryCategory.{v', v, u, u'} V_1 C_1
V : Type u'
inst_4 : Category.{v', u'} V
inst_5 : MonoidalCategory.{v', u'} V
C : Type u
inst_6 : Category.{v, u} C
inst_7 : EnrichedOrdinaryCategory.{v', v, u, u'} V C
P : ObjectProperty.{v, u} C
X : P.FullSubcategory
change :
  Eq.{v' + 1} (α :=
    tensorUnit.{v', u'} V (𝒞 := inst_4) ⟶
      @EnrichedCategory.Hom.{v', u', u} _ inst_4 inst_5 _ _ (X.obj (P := P)) (X.obj (P := P)))
    ((Equiv.trans P.fullyFaithfulι.homEquiv (eHomEquiv V) : (a : X ⟶ X) → 𝟙_ V ⟶ X.obj ⟶[V] X.obj) (𝟙 X) :
      tensorUnit.{v', u'} V (𝒞 := inst_4) ⟶
        @EnrichedCategory.Hom.{v', u', u} _ inst_4 inst_5 _ _ (X.obj (P := P)) (X.obj (P := P)))
    (eId V (X.obj (P := P)) :
      tensorUnit.{v', u'} V (𝒞 := inst_4) ⟶
        @EnrichedCategory.Hom.{v', u', u} _ inst_4 inst_5 _ _ (X.obj (P := P)) (X.obj (P := P)))
⊢ Eq.{v' + 1} (α :=
    tensorUnit.{v', u'} V (𝒞 := inst_4) ⟶
      @EnrichedCategory.Hom.{v', u', u} _ inst_4 inst_5 _ _ (X.obj (P := P)) (X.obj (P := P)))
    ((Equiv.trans P.fullyFaithfulι.homEquiv (eHomEquiv V) : (a : X ⟶ X) → 𝟙_ V ⟶ X.obj ⟶[V] X.obj) (𝟙 X) :
      tensorUnit.{v', u'} V (𝒞 := inst_4) ⟶
        @EnrichedCategory.Hom.{v', u', u} _ inst_4 inst_5 _ _ (X.obj (P := P)) (X.obj (P := P)))
    (eId V X : tensorUnit.{v', u'} V (𝒞 := inst_4) ⟶ @EnrichedCategory.Hom.{v', u', u} _ inst_4 inst_5 _ _ X X)

Tactic:
change _ = eId V X.obj

Premises used: CategoryTheory.ObjectProperty.FullSubcategory.obj, CategoryTheory.eId
-- Module: Mathlib.CategoryTheory.Enriched.Ordinary.Basic
Goal:
V_1 : Type u'
inst : Category.{v', u'} V_1
inst_1 : MonoidalCategory.{v', u'} V_1
C_1 : Type u
inst_2 : Category.{v, u} C_1
inst_3 : EnrichedOrdinaryCategory.{v', v, u, u'} V_1 C_1
V : Type u'
inst_4 : Category.{v', u'} V
inst_5 : MonoidalCategory.{v', u'} V
C : Type u
inst_6 : Category.{v, u} C
inst_7 : EnrichedOrdinaryCategory.{v', v, u, u'} V C
P : ObjectProperty.{v, u} C
X : P.FullSubcategory
rw :
  Eq.{v' + 1} (α :=
    tensorUnit.{v', u'} V (𝒞 := inst_4) ⟶
      @EnrichedCategory.Hom.{v', u', u} _ inst_4 inst_5 _ _ (X.obj (P := P)) (X.obj (P := P)))
    ((Equiv.trans P.fullyFaithfulι.homEquiv (eHomEquiv V) : (a : X ⟶ X) → 𝟙_ V ⟶ X.obj ⟶[V] X.obj) (𝟙 X) :
      tensorUnit.{v', u'} V (𝒞 := inst_4) ⟶
        @EnrichedCategory.Hom.{v', u', u} _ inst_4 inst_5 _ _ (X.obj (P := P)) (X.obj (P := P)))
    ((eHomEquiv V : (a : X.obj ⟶ X.obj) → 𝟙_ V ⟶ X.obj ⟶[V] X.obj) (𝟙 (X.obj (P := P))) :
      tensorUnit.{v', u'} V (𝒞 := inst_4) ⟶
        @EnrichedCategory.Hom.{v', u', u} _ inst_4 inst_5 _ _ (X.obj (P := P)) (X.obj (P := P)))
⊢ Eq.{v' + 1} (α :=
    tensorUnit.{v', u'} V (𝒞 := inst_4) ⟶
      @EnrichedCategory.Hom.{v', u', u} _ inst_4 inst_5 _ _ (X.obj (P := P)) (X.obj (P := P)))
    ((Equiv.trans P.fullyFaithfulι.homEquiv (eHomEquiv V) : (a : X ⟶ X) → 𝟙_ V ⟶ X.obj ⟶[V] X.obj) (𝟙 X) :
      tensorUnit.{v', u'} V (𝒞 := inst_4) ⟶
        @EnrichedCategory.Hom.{v', u', u} _ inst_4 inst_5 _ _ (X.obj (P := P)) (X.obj (P := P)))
    (eId V (X.obj (P := P)) :
      tensorUnit.{v', u'} V (𝒞 := inst_4) ⟶
        @EnrichedCategory.Hom.{v', u', u} _ inst_4 inst_5 _ _ (X.obj (P := P)) (X.obj (P := P)))

Tactic:
rw [← eHomEquiv_id]

Premises used: CategoryTheory.eHomEquiv_id
-- Module: Mathlib.CategoryTheory.Enriched.Ordinary.Basic
Goal:
V_1 : Type u'
inst : Category.{v', u'} V_1
inst_1 : MonoidalCategory.{v', u'} V_1
C_1 : Type u
inst_2 : Category.{v, u} C_1
inst_3 : EnrichedOrdinaryCategory.{v', v, u, u'} V_1 C_1
V : Type u'
inst_4 : Category.{v', u'} V
inst_5 : MonoidalCategory.{v', u'} V
C : Type u
inst_6 : Category.{v, u} C
inst_7 : EnrichedOrdinaryCategory.{v', v, u, u'} V C
P : ObjectProperty.{v, u} C
X : P.FullSubcategory
⊢ Eq.{v' + 1} (α :=
    tensorUnit.{v', u'} V (𝒞 := inst_4) ⟶
      @EnrichedCategory.Hom.{v', u', u} _ inst_4 inst_5 _ _ (X.obj (P := P)) (X.obj (P := P)))
    ((Equiv.trans P.fullyFaithfulι.homEquiv (eHomEquiv V) : (a : X ⟶ X) → 𝟙_ V ⟶ X.obj ⟶[V] X.obj) (𝟙 X) :
      tensorUnit.{v', u'} V (𝒞 := inst_4) ⟶
        @EnrichedCategory.Hom.{v', u', u} _ inst_4 inst_5 _ _ (X.obj (P := P)) (X.obj (P := P)))
    ((eHomEquiv V : (a : X.obj ⟶ X.obj) → 𝟙_ V ⟶ X.obj ⟶[V] X.obj) (𝟙 (X.obj (P := P))) :
      tensorUnit.{v', u'} V (𝒞 := inst_4) ⟶
        @EnrichedCategory.Hom.{v', u', u} _ inst_4 inst_5 _ _ (X.obj (P := P)) (X.obj (P := P)))

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Enriched.Ordinary.Basic
Goal:
V_1 : Type u'
inst : Category.{v', u'} V_1
inst_1 : MonoidalCategory.{v', u'} V_1
C_1 : Type u
inst_2 : Category.{v, u} C_1
inst_3 : EnrichedOrdinaryCategory.{v', v, u, u'} V_1 C_1
V : Type u'
inst_4 : Category.{v', u'} V
inst_5 : MonoidalCategory.{v', u'} V
C : Type u
inst_6 : Category.{v, u} C
inst_7 : EnrichedOrdinaryCategory.{v', v, u, u'} V C
P : ObjectProperty.{v, u} C
X Y Z : P.FullSubcategory
f : X ⟶ Y
g : Y ⟶ Z
⊢ Eq.{v' + 1} (α :=
    tensorUnit.{v', u'} V (𝒞 := inst_4) ⟶ @EnrichedCategory.Hom.{v', u', u} _ inst_4 inst_5 _ _ (P.ι.obj X) (P.ι.obj Z))
    (CategoryStruct.comp (Y :=
      tensorObj.{v', u'} (𝒞 := inst_4) (tensorUnit.{v', u'} V (𝒞 := inst_4)) (tensorUnit.{v', u'} V (𝒞 := inst_4)))
      (Iso.inv (λ_ (tensorUnit.{v', u'} V (𝒞 := inst_4))))
      (CategoryStruct.comp (Y :=
        tensorObj.{v', u'} (𝒞 := inst_4) (@EnrichedCategory.Hom.{v', u', u} _ inst_4 inst_5 _ _ (P.ι.obj X) (P.ι.obj Y))
          (@EnrichedCategory.Hom.{v', u', u} _ inst_4 inst_5 _ _ (P.ι.obj Y) (P.ι.obj Z)))
        ((eHomEquiv V : (a : P.ι.obj X ⟶ P.ι.obj Y) → 𝟙_ V ⟶ P.ι.obj X ⟶[V] P.ι.obj Y) (P.ι.map f) ⊗ₘ
          (eHomEquiv V : (a : P.ι.obj Y ⟶ P.ι.obj Z) → 𝟙_ V ⟶ P.ι.obj Y ⟶[V] P.ι.obj Z) (P.ι.map g))
        (eComp V (P.ι.obj X) (P.ι.obj Y) (P.ι.obj Z))))
    (CategoryStruct.comp (Y :=
      tensorObj.{v', u'} (𝒞 := inst_4) (tensorUnit.{v', u'} V (𝒞 := inst_4)) (tensorUnit.{v', u'} V (𝒞 := inst_4)))
      (Iso.inv (λ_ (tensorUnit.{v', u'} V (𝒞 := inst_4))))
      (CategoryStruct.comp (Y :=
        tensorObj.{v', u'} (𝒞 := inst_4)
          (@EnrichedCategory.Hom.{v', u', u} _ inst_4 inst_5 _ _ (X.obj (P := P)) (Y.obj (P := P)))
          (@EnrichedCategory.Hom.{v', u', u} _ inst_4 inst_5 _ _ (Y.obj (P := P)) (Z.obj (P := P))))
        ((eHomEquiv V : (a : X.obj ⟶ Y.obj) → 𝟙_ V ⟶ X.obj ⟶[V] Y.obj)
            ((P.fullyFaithfulι.homEquiv : (a : X ⟶ Y) → X.obj ⟶ Y.obj) f) ⊗ₘ
          (eHomEquiv V : (a : Y.obj ⟶ Z.obj) → 𝟙_ V ⟶ Y.obj ⟶[V] Z.obj)
            ((P.fullyFaithfulι.homEquiv : (a : Y ⟶ Z) → Y.obj ⟶ Z.obj) g))
        (eComp V X Y Z)))

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.EpiMono
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
A B : Cᵒᵖ
f : A ⟶ B
inst_1 : Mono.{v₁, u₁} (C := Cᵒᵖ) (X := A) (Y := B) f
⊢ Epi f.unop

Tactic:
⟨fun _ _ eq => Quiver.Hom.op_inj ((cancel_mono f).1 (Quiver.Hom.unop_inj eq))⟩

Premises used: Quiver.Hom.op_inj, CategoryTheory.Epi.mk, CategoryTheory.cancel_mono, Quiver.Hom.unop_inj, Iff.mp
-- Module: Mathlib.CategoryTheory.EpiMono
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
A B : C
f : A ⟶ B
inst_1 : Mono f
⊢ Epi.{v₁, u₁} (C := Cᵒᵖ) (X := Opposite.op B) (Y := Opposite.op A) f.op

Tactic:
⟨fun _ _ eq => Quiver.Hom.unop_inj ((cancel_mono f).1 (Quiver.Hom.op_inj eq))⟩

Premises used: Quiver.Hom.op_inj, CategoryTheory.Epi.mk, CategoryTheory.cancel_mono, Quiver.Hom.unop_inj, Iff.mp
-- Module: Mathlib.CategoryTheory.EpiMono
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
⊢ Epi.{v₁, u₁} (C := Cᵒᵖ) (X := Opposite.op Y) (Y := Opposite.op X) f.op ↔ Mono f

Tactic:
⟨fun _ ↦ unop_mono_of_epi f.op, fun _ ↦ inferInstance⟩

Premises used: Quiver.Hom.op, inferInstance, CategoryTheory.unop_mono_of_epi, Iff.intro
-- Module: Mathlib.CategoryTheory.EpiMono
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : Cᵒᵖ
f : X ⟶ Y
⊢ Epi f.unop ↔ Mono.{v₁, u₁} (C := Cᵒᵖ) (X := X) (Y := Y) f

Tactic:
⟨fun _ ↦ op_mono_of_epi f.unop, fun _ ↦ inferInstance⟩

Premises used: CategoryTheory.op_mono_of_epi, Quiver.Hom.unop, inferInstance, Iff.intro
-- Module: Mathlib.CategoryTheory.EpiMono
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
se : SplitEpi f
⊢ IsSplitEpi f

Tactic:
⟨Nonempty.intro se⟩

Premises used: Nonempty.intro, CategoryTheory.IsSplitEpi.mk
-- Module: Mathlib.CategoryTheory.EpiMono
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
hf : IsSplitEpi f
⊢ section_ f ≫ f = 𝟙 Y

Tactic:
hf.exists_splitEpi.some.id

Premises used: CategoryTheory.SplitEpi.id, Nonempty.some, CategoryTheory.section_, CategoryTheory.IsSplitEpi.exists_splitEpi
-- Module: Mathlib.CategoryTheory.EpiMono
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
inst_1 : IsSplitEpi f
⊢ IsSplitMono (section_ f)

Tactic:
IsSplitMono.mk' (SplitEpi.splitMono _)

Premises used: CategoryTheory.SplitEpi.splitMono, CategoryTheory.IsSplitMono.mk'
-- Module: Mathlib.CategoryTheory.EpiMono
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
inst_1 : Mono f
inst_2 : IsSplitEpi f
⊢ f ≫ section_ f = 𝟙 X

Tactic:
simp [← cancel_mono f]

Premises used: CategoryTheory.cancel_mono
-- Module: Mathlib.CategoryTheory.EpiMono
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
inst_1 : Mono f
inst_2 : IsSplitEpi f
⊢ section_ f ≫ f = 𝟙 Y

Tactic:
simp
-- Module: Mathlib.CategoryTheory.EpiMono
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
inst_1 : IsIso f
⊢ IsSplitEpi f

Tactic:
IsSplitEpi.mk' { section_ := inv f }

Premises used: CategoryTheory.SplitEpi.mk, CategoryTheory.inv, CategoryTheory.IsSplitEpi.mk'
-- Module: Mathlib.CategoryTheory.EpiMono
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
se : SplitEpi f
Z : C
g h : Y ⟶ Z
w : f ≫ g = f ≫ h
⊢ se.section_ ≫ f ≫ g = se.section_ ≫ f ≫ h

Tactic:
replace w := se.section_ ≫= w
-- Module: Mathlib.CategoryTheory.EpiMono
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
se : SplitEpi f
Z : C
g h : Y ⟶ Z
w : se.section_ ≫ f ≫ g = se.section_ ≫ f ≫ h
⊢ g = h

Tactic:
simpa using w
-- Module: Mathlib.CategoryTheory.EpiMono
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
hf : IsSplitEpi f
⊢ Epi f

Tactic:
hf.exists_splitEpi.some.epi

Premises used: Nonempty.some, CategoryTheory.IsSplitEpi.exists_splitEpi, CategoryTheory.SplitEpi.epi
-- Module: Mathlib.CategoryTheory.EpiMono
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
hf : IsSplitEpi f
hg : IsSplitEpi g
⊢ IsSplitEpi (f ≫ g)

Tactic:
IsSplitEpi.mk' <| hf.exists_splitEpi.some.comp hg.exists_splitEpi.some

Premises used: CategoryTheory.SplitEpi.comp, Nonempty.some, CategoryTheory.IsSplitEpi.exists_splitEpi, CategoryTheory.IsSplitEpi.mk'
-- Module: Mathlib.CategoryTheory.EpiMono
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
hf : SplitEpi f
inst_1 : Epi hf.section_
⊢ hf.section_ ≫ f ≫ hf.section_ = hf.section_

Tactic:
simp
-- Module: Mathlib.CategoryTheory.EpiMono
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
hf : SplitEpi f
inst_1 : Epi hf.section_
⊢ hf.section_ ≫ f = 𝟙 Y

Tactic:
simp
-- Module: Mathlib.CategoryTheory.EpiMono
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
hf : IsSplitEpi f
hf' : Epi (section_ f)
⊢ IsIso f

Tactic:
@IsIso.of_epi_section' _ _ _ _ _ hf.exists_splitEpi.some hf'

Premises used: Nonempty.some, CategoryTheory.IsIso.of_epi_section', CategoryTheory.IsSplitEpi.exists_splitEpi
-- Module: Mathlib.CategoryTheory.EpiMono
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
all_split_mono : ∀ {X Y : C} (f : X ⟶ Y), Trunc (IsSplitMono f)
all_is_iso : ∀ {X Y : C} (f : X ⟶ Y), IsIso f
⊢ Groupoid.{v₁, u₁} C

Tactic:
apply Groupoid.ofIsIso

Premises used: CategoryTheory.Groupoid.ofIsIso
-- Module: Mathlib.CategoryTheory.EpiMono
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
all_split_mono : ∀ {X Y : C} (f : X ⟶ Y), Trunc (IsSplitMono f)
X Y : C
f : X ⟶ Y
⊢ IsSplitMono f

Tactic:
have ⟨a,_⟩ := Trunc.exists_rep <| all_split_mono f
-- Module: Mathlib.CategoryTheory.EpiMono
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
all_split_mono : ∀ {X Y : C} (f : X ⟶ Y), Trunc (IsSplitMono f)
X Y : C
f : X ⟶ Y
a : IsSplitMono f
⊢ ⋯ = ⋯

Tactic:
have ⟨a,_⟩ := Trunc.exists_rep <| all_split_mono f
-- Module: Mathlib.CategoryTheory.EpiMono
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
all_split_mono : ∀ {X Y : C} (f : X ⟶ Y), Trunc (IsSplitMono f)
X Y : C
f : X ⟶ Y
a : IsSplitMono f
h : ⋯ = ⋯
⊢ IsSplitMono (retraction f)

Tactic:
have ⟨b,_⟩ := Trunc.exists_rep <| all_split_mono <| retraction f
-- Module: Mathlib.CategoryTheory.EpiMono
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
all_split_mono : ∀ {X Y : C} (f : X ⟶ Y), Trunc (IsSplitMono f)
X Y : C
f : X ⟶ Y
a : IsSplitMono f
h : ⋯ = ⋯
b : IsSplitMono (retraction f)
⊢ ⋯ = ⋯

Tactic:
have ⟨b,_⟩ := Trunc.exists_rep <| all_split_mono <| retraction f
-- Module: Mathlib.CategoryTheory.EpiMono
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
all_split_mono : ∀ {X Y : C} (f : X ⟶ Y), Trunc (IsSplitMono f)
X Y : C
f : X ⟶ Y
a : IsSplitMono f
h : ⋯ = ⋯
b : IsSplitMono (retraction f)
h_1 : ⋯ = ⋯
⊢ IsIso f

Tactic:
apply IsIso.of_mono_retraction

Premises used: CategoryTheory.IsIso.of_mono_retraction
-- Module: Mathlib.CategoryTheory.EpiMono
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : SplitEpiCategory.{v₁, u₁} C
X Y : C
f : X ⟶ Y
inst_2 : Epi f
⊢ IsSplitEpi f

Tactic:
SplitEpiCategory.isSplitEpi_of_epi _

Premises used: CategoryTheory.SplitEpiCategory.isSplitEpi_of_epi
-- Module: Mathlib.CategoryTheory.EpiMono
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
X Y : C
f : X ⟶ Y
se : SplitEpi f
F : Functor.{v₁, v₂, u₁, u₂} C D
rw : F.map (se.section_ ≫ f) = 𝟙 (F.obj Y)
rw₁ : F.map (𝟙 Y) = 𝟙 (F.obj Y)
rw₂ rw₃ : Eq.{v₂ + 1} (α := F.obj Y ⟶ F.obj Y) (𝟙 (F.obj Y)) (𝟙 (F.obj Y))
⊢ F.map se.section_ ≫ F.map f = 𝟙 (F.obj Y)

Tactic:
rw [← Functor.map_comp, SplitEpi.id, Functor.map_id]

Premises used: CategoryTheory.SplitEpi.id, CategoryTheory.Functor.map_id, CategoryTheory.Functor.map_comp
-- Module: Mathlib.CategoryTheory.EpiMono
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
X Y : C
f : X ⟶ Y
hf : IsSplitEpi f
F : Functor.{v₁, v₂, u₁, u₂} C D
⊢ IsSplitEpi (F.map f)

Tactic:
IsSplitEpi.mk' (hf.exists_splitEpi.some.map F)

Premises used: Nonempty.some, CategoryTheory.SplitEpi.map, CategoryTheory.IsSplitEpi.exists_splitEpi, CategoryTheory.IsSplitEpi.mk'
-- Module: Mathlib.CategoryTheory.EpiMono
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y Z : C
f : X ⟶ Y
inst_1 : Epi f
g : Y ⟶ Z
⊢ Epi (f ≫ g) ↔ Epi g

Tactic:
⟨fun _ ↦ epi_of_epi f _, fun _ ↦ inferInstance⟩

Premises used: CategoryTheory.epi_of_epi, inferInstance, Iff.intro
-- Module: Mathlib.CategoryTheory.EpiMono
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
inst_1 : IsIso g
⊢ Epi (f ≫ g) ↔ Epi f

Tactic:
⟨fun h ↦ ?_, fun h ↦ inferInstance⟩

Premises used: inferInstance, Iff.intro
-- Module: Mathlib.CategoryTheory.EpiMono
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
inst_1 : IsIso g
refine : ∀ (h : Epi (f ≫ g)), Epi f
⊢ Epi (f ≫ g) ↔ Epi f

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ inferInstance⟩
-- Module: Mathlib.CategoryTheory.EpiMono
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
inst_1 : IsIso g
h : Epi (f ≫ g)
⊢ Epi f

Tactic:
simpa using (inferInstance : Epi ((f ≫ g) ≫ inv g))

Premises used: inferInstance
-- Module: Mathlib.CategoryTheory.EpiMono
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
h : SplitEpi f
⊢ Eq.{v₁ + 1} (α := Opposite.unop (Opposite.op Y) ⟶ Opposite.unop (Opposite.op Y))
    (Quiver.Hom.unop (f.op ≫ h.section_.op)) (Quiver.Hom.unop (𝟙 (Opposite.op Y)))

Tactic:
simp