awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Elements
Goal:
C : Type u
inst : Category.{v, u} C
F_1 : Functor.{v, w, u, w + 1} C (Type w)
F : Cᵒᵖ ⥤ Type (max w v)
x : F.Elementsᵒᵖ
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (𝟙 (unop x).1)) : (a : F.obj (unop x).1) → F.obj (unop x).fst)
      ((uliftYonedaEquiv : (a : uliftYoneda.{w, v, u}.obj (unop (unop x).1) ⟶ F) → F.obj (unop x).1)
        ((Equiv.symm uliftYonedaEquiv : (a : F.obj (unop x).1) → uliftYoneda.{w, v, u}.obj (unop (unop x).1) ⟶ F)
          ((unop x).snd (β := fun (c : Cᵒᵖ) ↦ F.obj c)))) =
    (unop x).snd (β := fun (c : Cᵒᵖ) ↦ F.obj c)

Tactic:
simpa only [Functor.map_id_apply] using
      uliftYonedaEquiv.apply_symm_apply (unop x).snd

Premises used: Equiv.apply_symm_apply, CategoryTheory.Functor.map_id_apply, Sigma.snd, Opposite.unop, CategoryTheory.uliftYonedaEquiv
-- Module: Mathlib.CategoryTheory.Elements
Goal:
C : Type u
inst : Category.{v, u} C
F_1 : Functor.{v, w, u, w + 1} C (Type w)
F : Cᵒᵖ ⥤ Type (max w v)
X Y : F.Elementsᵒᵖ
f : X ⟶ Y
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
aesop
-- Module: Mathlib.CategoryTheory.Elements
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{v, u_1, u, u_1 + 1} Cᵒᵖ (Type u_1)
X : C
h : F.RepresentableBy X
Y : F.Elements
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun)
          (F.map
            (Quiver.Hom.op
              (((Equiv.symm h.homEquiv :
                    Equiv.{u_1 + 1, v + 1} (F.obj (Opposite.op (Opposite.unop Y.1))) (Opposite.unop Y.1 ⟶ X)) :
                  (a : F.obj (Opposite.op (Opposite.unop Y.1))) → Opposite.unop Y.1 ⟶ X)
                (Y.snd (β := fun (c : Cᵒᵖ) ↦ F.obj c))))) :
        (a : (fun (X : Type u_1) ↦ X) (F.obj (initialOfRepresentableBy h).fst)) →
          (fun (X : Type u_1) ↦ X) (F.obj Y.fst))
      ((initialOfRepresentableBy h).snd (β := fun (c : Cᵒᵖ) ↦ F.obj c)) =
    Y.snd (β := fun (c : Cᵒᵖ) ↦ F.obj c)

Tactic:
simp [← h.homEquiv_comp]

Premises used: CategoryTheory.Functor.RepresentableBy.homEquiv_comp
-- Module: Mathlib.CategoryTheory.Elements
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{v, u_1, u, u_1 + 1} Cᵒᵖ (Type u_1)
X : C
h : F.RepresentableBy X
Y : F.Elements
m : initialOfRepresentableBy h ⟶ Y
⊢ m =
    (fun (Y : F.Elements) ↦
        (Subtype.mk (p :=
            fun
              (f :
                (initialOfRepresentableBy h).fst (β := fun (c : Cᵒᵖ) ↦ F.obj c) ⟶
                  Y.fst (β := fun (c : Cᵒᵖ) ↦ F.obj c)) ↦
            (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f) :
                  (a : (fun (X : Type u_1) ↦ X) (F.obj (initialOfRepresentableBy h).fst)) →
                    (fun (X : Type u_1) ↦ X) (F.obj Y.fst))
                ((initialOfRepresentableBy h).snd (β := fun (c : Cᵒᵖ) ↦ F.obj c)) =
              Y.snd (β := fun (c : Cᵒᵖ) ↦ F.obj c))
            (Quiver.Hom.op
              (((Equiv.symm h.homEquiv :
                    Equiv.{u_1 + 1, v + 1} (F.obj (Opposite.op (Opposite.unop Y.1))) (Opposite.unop Y.1 ⟶ X)) :
                  (a : F.obj (Opposite.op (Opposite.unop Y.1))) → Opposite.unop Y.1 ⟶ X)
                (Y.snd (β := fun (c : Cᵒᵖ) ↦ F.obj c))))
            ⋯ :
          { f :
            (initialOfRepresentableBy h).fst (β := fun (c : Cᵒᵖ) ↦ F.obj c) ⟶ Y.fst (β := fun (c : Cᵒᵖ) ↦ F.obj c) //
            (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f) :
                  (a : (fun (X : Type u_1) ↦ X) (F.obj (initialOfRepresentableBy h).fst)) →
                    (fun (X : Type u_1) ↦ X) (F.obj Y.fst))
                ((initialOfRepresentableBy h).snd (β := fun (c : Cᵒᵖ) ↦ F.obj c)) =
              Y.snd (β := fun (c : Cᵒᵖ) ↦ F.obj c) }))
      Y

Tactic:
simp [← m.2, ← h.homEquiv_unop_comp]

Premises used: CategoryTheory.Functor.RepresentableBy.homEquiv_unop_comp, Subtype.property
-- Module: Mathlib.CategoryTheory.Elements
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{v, u_1, u, u_1 + 1} C (Type u_1)
X : C
h : F.CorepresentableBy X
Y : F.Elements
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun)
          (F.map
            (((Equiv.symm h.homEquiv :
                  Equiv.{u_1 + 1, v + 1} (F.obj (Y.fst (β := fun (c : C) ↦ F.obj c)))
                    (X ⟶ Y.fst (β := fun (c : C) ↦ F.obj c))) :
                (a : F.obj Y.fst) → X ⟶ Y.fst)
              (Y.snd (β := fun (c : C) ↦ F.obj c)))) :
        (a : (fun (X : Type u_1) ↦ X) (F.obj (initialOfCorepresentableBy h).fst)) →
          (fun (X : Type u_1) ↦ X) (F.obj Y.fst))
      ((initialOfCorepresentableBy h).snd (β := fun (c : C) ↦ F.obj c)) =
    Y.snd (β := fun (c : C) ↦ F.obj c)

Tactic:
simp [← h.homEquiv_comp]

Premises used: CategoryTheory.Functor.CorepresentableBy.homEquiv_comp
-- Module: Mathlib.CategoryTheory.Elements
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{v, u_1, u, u_1 + 1} C (Type u_1)
X : C
h : F.CorepresentableBy X
Y : F.Elements
m : initialOfCorepresentableBy h ⟶ Y
⊢ m =
    (fun (Y : F.Elements) ↦
        (Subtype.mk (p :=
            fun
              (f :
                (initialOfCorepresentableBy h).fst (β := fun (c : C) ↦ F.obj c) ⟶ Y.fst (β := fun (c : C) ↦ F.obj c)) ↦
            (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f) :
                  (a : (fun (X : Type u_1) ↦ X) (F.obj (initialOfCorepresentableBy h).fst)) →
                    (fun (X : Type u_1) ↦ X) (F.obj Y.fst))
                ((initialOfCorepresentableBy h).snd (β := fun (c : C) ↦ F.obj c)) =
              Y.snd (β := fun (c : C) ↦ F.obj c))
            (((Equiv.symm h.homEquiv :
                  Equiv.{u_1 + 1, v + 1} (F.obj (Y.fst (β := fun (c : C) ↦ F.obj c)))
                    (X ⟶ Y.fst (β := fun (c : C) ↦ F.obj c))) :
                (a : F.obj Y.fst) → X ⟶ Y.fst)
              (Y.snd (β := fun (c : C) ↦ F.obj c)))
            ⋯ :
          { f : (initialOfCorepresentableBy h).fst (β := fun (c : C) ↦ F.obj c) ⟶ Y.fst (β := fun (c : C) ↦ F.obj c) //
            (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f) :
                  (a : (fun (X : Type u_1) ↦ X) (F.obj (initialOfCorepresentableBy h).fst)) →
                    (fun (X : Type u_1) ↦ X) (F.obj Y.fst))
                ((initialOfCorepresentableBy h).snd (β := fun (c : C) ↦ F.obj c)) =
              Y.snd (β := fun (c : C) ↦ F.obj c) }))
      Y

Tactic:
simp [← m.2, ← h.homEquiv_comp]

Premises used: CategoryTheory.Functor.CorepresentableBy.homEquiv_comp, Subtype.property
-- Module: Mathlib.CategoryTheory.Endofunctor.Algebra
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{v, v, u, u} C C
A B : Algebra F
f g : A ⟶ B
w : f.f = g.f
⊢ f = g

Tactic:
Hom.ext w

Premises used: CategoryTheory.Endofunctor.Algebra.Hom.ext
-- Module: Mathlib.CategoryTheory.Endofunctor.Algebra
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{v, v, u, u} C C
A : Algebra F
⊢ Hom.id A = 𝟙 A

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Endofunctor.Algebra
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{v, v, u, u} C C
A : Algebra F
⊢ Hom.f (𝟙 A) = 𝟙 A.a

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Endofunctor.Algebra
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{v, v, u, u} C C
A₀ A₁ A₂ : Algebra F
f : A₀ ⟶ A₁
g : A₁ ⟶ A₂
⊢ Hom.comp f g = f ≫ g

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Endofunctor.Algebra
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{v, v, u, u} C C
A₀ A₁ A₂ : Algebra F
f : A₀ ⟶ A₁
g : A₁ ⟶ A₂
⊢ (f ≫ g).f = f.f ≫ g.f

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Endofunctor.Algebra
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{v, v, u, u} C C
A A₀ A₁ A₂ : Algebra F
f : A₀ ⟶ A₁
g : A₁ ⟶ A₂
h : A₀.a ≅ A₁.a
w : F.map h.hom ≫ A₁.str = A₀.str ≫ h.hom
rw : F.map (h.inv ≫ h.hom) ≫ A₁.str = A₁.str
⊢ F.map h.inv ≫ A₀.str = A₁.str ≫ h.inv

Tactic:
rw [h.eq_comp_inv, Category.assoc, ← w, ← Functor.map_comp_assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Iso.eq_comp_inv, CategoryTheory.Functor.map_comp_assoc
-- Module: Mathlib.CategoryTheory.Endofunctor.Algebra
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{v, v, u, u} C C
A A₀ A₁ A₂ : Algebra F
f : A₀ ⟶ A₁
g : A₁ ⟶ A₂
h : A₀.a ≅ A₁.a
w : F.map h.hom ≫ A₁.str = A₀.str ≫ h.hom
⊢ F.map (h.inv ≫ h.hom) ≫ A₁.str = A₁.str

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Endofunctor.Algebra
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{v, v, u, u} C C
A₀ A₁ : Algebra F
f : A₀ ⟶ A₁
inst_1 : IsIso f.f
⊢ F.map (inv f.f) ≫ A₀.str = A₁.str ≫ inv f.f

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Endofunctor.Algebra
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{v, v, u, u} C C
A A₀ A₁ A₂ : Algebra F
f : A₀ ⟶ A₁
g : A₁ ⟶ A₂
⊢ (forget F).Faithful

Tactic:

Premises used: CategoryTheory.Functor.Faithful.mk
-- Module: Mathlib.CategoryTheory.Endofunctor.Algebra
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{v, v, u, u} C C
X Y : Algebra F
f : X ⟶ Y
h : Epi f.f
⊢ Epi f

Tactic:
(forget F).epi_of_epi_map h

Premises used: CategoryTheory.Endofunctor.Algebra.forget, CategoryTheory.Functor.epi_of_epi_map
-- Module: Mathlib.CategoryTheory.Endofunctor.Algebra
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{v, v, u, u} C C
X Y : Algebra F
f : X ⟶ Y
h : Mono f.f
⊢ Mono f

Tactic:
(forget F).mono_of_mono_map h

Premises used: CategoryTheory.Endofunctor.Algebra.forget, CategoryTheory.Functor.mono_of_mono_map
-- Module: Mathlib.CategoryTheory.Endofunctor.Algebra
Goal:
C : Type u
inst : Category.{v, u} C
F_1 : Functor.{v, v, u, u} C C
A A₀ A₁ A₂ : Algebra F_1
f : A₀ ⟶ A₁
g : A₁ ⟶ A₂
F G : Functor.{v, v, u, u} C C
α : F ≅ G
⊢ 𝟙 F = α.hom ≫ α.inv

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Endofunctor.Algebra
Goal:
C : Type u
inst : Category.{v, u} C
F_1 : Functor.{v, v, u, u} C C
A A₀ A₁ A₂ : Algebra F_1
f : A₀ ⟶ A₁
g : A₁ ⟶ A₂
F G : Functor.{v, v, u, u} C C
α : F ≅ G
⊢ α.inv ≫ α.hom = 𝟙 G

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Endofunctor.Algebra
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{v, v, u, u} C C
A_1 A₀ A₁ A₂ : Algebra F
f : A₀ ⟶ A₁
g : A₁ ⟶ A₂
A : Algebra F
h : Limits.IsInitial A
rw : F.map (strInv h ≫ A.str) ≫ A.str = (A.str ≫ strInv h) ≫ A.str
rw₁ : (F.map (strInv h) ≫ F.map A.str) ≫ A.str = (A.str ≫ strInv h) ≫ A.str
rw₂ :
  (F.map (Hom.f (h.to { a := F.obj A.a, str := F.map A.str : Algebra F })) ≫ F.map A.str) ≫ A.str =
    (A.str ≫ Hom.f (h.to { a := F.obj A.a, str := F.map A.str })) ≫ A.str
rw₃ rw₄ :
  (F.map (Hom.f (h.to { a := F.obj A.a, str := F.map A.str : Algebra F })) ≫ F.map A.str) ≫ A.str =
    (F.map (Hom.f (h.to { a := F.obj A.a, str := F.map A.str : Algebra F })) ≫
        { a := F.obj A.a, str := F.map A.str : Algebra F }.str) ≫
      A.str
⊢ F.map (strInv h ≫ A.str) ≫ A.str = A.str ≫ strInv h ≫ A.str

Tactic:
rw [← Category.assoc, F.map_comp, strInv, ← Hom.h]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Endofunctor.Algebra.Hom.h, CategoryTheory.Functor.map_comp, CategoryTheory.Endofunctor.Algebra.Initial.strInv
-- Module: Mathlib.CategoryTheory.Endofunctor.Algebra
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{v, v, u, u} C C
A : Algebra F
h : Limits.IsInitial A
⊢ { f := strInv h ≫ A.str, h := ⋯ : A.Hom A } = 𝟙 A

Tactic:
Limits.IsInitial.hom_ext h _ (𝟙 A)

Premises used: CategoryTheory.Limits.IsInitial.hom_ext, CategoryTheory.CategoryStruct.id
-- Module: Mathlib.CategoryTheory.Endofunctor.Algebra
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{v, v, u, u} C C
A : Algebra F
h : Limits.IsInitial A
⊢ strInv h ≫ A.str = 𝟙 A.a

Tactic:
congr_arg Hom.f (left_inv' h)

Premises used: congr_arg, CategoryTheory.Endofunctor.Algebra.Hom.f, CategoryTheory.Endofunctor.Algebra.Initial.left_inv'
-- Module: Mathlib.CategoryTheory.Endofunctor.Algebra
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{v, v, u, u} C C
A : Algebra F
h : Limits.IsInitial A
rw : F.map (Hom.f (h.to { a := F.obj A.a, str := F.map A.str }) ≫ A.str) = F.map (𝟙 A.a)
⊢ A.str ≫ strInv h = 𝟙 (F.obj A.a)

Tactic:
rw [strInv, ← (h.to ⟨F.obj A.1, F.map A.str⟩).h, ← F.map_id, ← F.map_comp]

Premises used: CategoryTheory.Endofunctor.Algebra.str, CategoryTheory.Endofunctor.Algebra.a, CategoryTheory.Functor.map, CategoryTheory.Endofunctor.Algebra.mk, CategoryTheory.Limits.IsInitial.to, CategoryTheory.Functor.map_id, CategoryTheory.Endofunctor.Algebra.Hom.h, CategoryTheory.Functor.map_comp, CategoryTheory.Endofunctor.Algebra.Initial.strInv, CategoryTheory.Functor.obj
-- Module: Mathlib.CategoryTheory.Endofunctor.Algebra
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{v, v, u, u} C C
A : Algebra F
h : Limits.IsInitial A
e_a : Hom.f (h.to { a := F.obj A.a, str := F.map A.str }) ≫ A.str = 𝟙 A.a
⊢ F.map (Hom.f (h.to { a := F.obj A.a, str := F.map A.str }) ≫ A.str) = F.map (𝟙 A.a)

Tactic:
congr
-- Module: Mathlib.CategoryTheory.Endofunctor.Algebra
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{v, v, u, u} C C
A : Algebra F
h : Limits.IsInitial A
⊢ Hom.f (h.to { a := F.obj A.a, str := F.map A.str }) ≫ A.str = 𝟙 A.a

Tactic:
left_inv h

Premises used: CategoryTheory.Endofunctor.Algebra.Initial.strInv, CategoryTheory.Endofunctor.Algebra.Initial.left_inv
-- Module: Mathlib.CategoryTheory.Endofunctor.Algebra
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{v, v, u, u} C C
A : Algebra F
h : Limits.IsInitial A
⊢ Hom.f (h.to { a := F.obj A.a, str := F.map A.str }) ≫ A.str = 𝟙 A.a

Tactic:
exact left_inv h

Premises used: CategoryTheory.Endofunctor.Algebra.Initial.left_inv
-- Module: Mathlib.CategoryTheory.Endofunctor.Algebra
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{v, v, u, u} C C
A : Algebra F
h : Limits.IsInitial A
⊢ IsIso A.str

Tactic:
{ out := ⟨strInv h, right_inv _, left_inv _⟩ }

Premises used: CategoryTheory.Endofunctor.Algebra.Initial.right_inv, And.intro, Exists.intro, CategoryTheory.Endofunctor.Algebra.Initial.strInv, CategoryTheory.IsIso.mk, CategoryTheory.Endofunctor.Algebra.Initial.left_inv
-- Module: Mathlib.CategoryTheory.Endofunctor.Algebra
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{v, v, u, u} C C
A B : Coalgebra F
f g : A ⟶ B
w : f.f = g.f
⊢ f = g

Tactic:
Hom.ext w

Premises used: CategoryTheory.Endofunctor.Coalgebra.Hom.ext
-- Module: Mathlib.CategoryTheory.Endofunctor.Algebra
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{v, v, u, u} C C
V : Coalgebra F
⊢ Hom.id V = 𝟙 V

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Endofunctor.Algebra
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{v, v, u, u} C C
V : Coalgebra F
⊢ Hom.f (𝟙 V) = 𝟙 V.V

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Endofunctor.Algebra
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{v, v, u, u} C C
V₀ V₁ V₂ : Coalgebra F
f : V₀ ⟶ V₁
g : V₁ ⟶ V₂
⊢ Hom.comp f g = f ≫ g

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Endofunctor.Algebra
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{v, v, u, u} C C
V₀ V₁ V₂ : Coalgebra F
f : V₀ ⟶ V₁
g : V₁ ⟶ V₂
⊢ (f ≫ g).f = f.f ≫ g.f

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Endofunctor.Algebra
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{v, v, u, u} C C
V V₀ V₁ V₂ : Coalgebra F
f : V₀ ⟶ V₁
g : V₁ ⟶ V₂
h : V₀.V ≅ V₁.V
w : V₀.str ≫ F.map h.hom = h.hom ≫ V₁.str
rw : V₀.str ≫ F.map (h.hom ≫ h.inv) = V₀.str
⊢ V₁.str ≫ F.map h.inv = h.inv ≫ V₀.str

Tactic:
rw [h.eq_inv_comp, ← Category.assoc, ← w, Category.assoc, ← F.map_comp]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Functor.map_comp, CategoryTheory.Iso.eq_inv_comp
-- Module: Mathlib.CategoryTheory.Endofunctor.Algebra
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{v, v, u, u} C C
V V₀ V₁ V₂ : Coalgebra F
f : V₀ ⟶ V₁
g : V₁ ⟶ V₂
h : V₀.V ≅ V₁.V
w : V₀.str ≫ F.map h.hom = h.hom ≫ V₁.str
⊢ V₀.str ≫ F.map (h.hom ≫ h.inv) = V₀.str

Tactic:
simp only [Iso.hom_inv_id, Functor.map_id, Category.comp_id]

Premises used: CategoryTheory.Iso.hom_inv_id, CategoryTheory.Category.comp_id, CategoryTheory.Functor.map_id
-- Module: Mathlib.CategoryTheory.Endofunctor.Algebra
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{v, v, u, u} C C
V₀ V₁ : Coalgebra F
f : V₀ ⟶ V₁
inst_1 : IsIso f.f
rw : V₀.str ≫ F.map f.f ≫ F.map (inv f.f) = V₀.str
⊢ V₁.str ≫ F.map (inv f.f) = inv f.f ≫ V₀.str

Tactic:
rw [IsIso.eq_inv_comp f.1, ← Category.assoc, ← f.h, Category.assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.IsIso.eq_inv_comp, CategoryTheory.Endofunctor.Coalgebra.Hom.f, CategoryTheory.Endofunctor.Coalgebra.Hom.h
-- Module: Mathlib.CategoryTheory.Endofunctor.Algebra
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{v, v, u, u} C C
V₀ V₁ : Coalgebra F
f : V₀ ⟶ V₁
inst_1 : IsIso f.f
⊢ V₀.str ≫ F.map f.f ≫ F.map (inv f.f) = V₀.str

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Endofunctor.Algebra
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{v, v, u, u} C C
V V₀ V₁ V₂ : Coalgebra F
f : V₀ ⟶ V₁
g : V₁ ⟶ V₂
⊢ (forget F).Faithful

Tactic:

Premises used: CategoryTheory.Functor.Faithful.mk
-- Module: Mathlib.CategoryTheory.Endofunctor.Algebra
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{v, v, u, u} C C
X Y : Coalgebra F
f : X ⟶ Y
h : Epi f.f
⊢ Epi f

Tactic:
(forget F).epi_of_epi_map h

Premises used: CategoryTheory.Endofunctor.Coalgebra.forget, CategoryTheory.Functor.epi_of_epi_map
-- Module: Mathlib.CategoryTheory.Endofunctor.Algebra
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{v, v, u, u} C C
X Y : Coalgebra F
f : X ⟶ Y
h : Mono f.f
⊢ Mono f

Tactic:
(forget F).mono_of_mono_map h

Premises used: CategoryTheory.Endofunctor.Coalgebra.forget, CategoryTheory.Functor.mono_of_mono_map
-- Module: Mathlib.CategoryTheory.Endofunctor.Algebra
Goal:
C : Type u
inst : Category.{v, u} C
F_1 : Functor.{v, v, u, u} C C
V V₀ V₁ V₂ : Coalgebra F_1
f_1 : V₀ ⟶ V₁
g : V₁ ⟶ V₂
F G : Functor.{v, v, u, u} C C
α : F ⟶ G
X Y : Coalgebra F
f : X ⟶ Y
rw : X.str ≫ α.app X.V ≫ G.map f.f = f.f ≫ { V := Y.V, str := Y.str ≫ α.app Y.V }.str
rw₁ :
  X.str ≫ F.map f.f ≫ α.app { V := Y.V, str := Y.str ≫ α.app Y.V : Coalgebra G }.V =
    f.f ≫ { V := Y.V, str := Y.str ≫ α.app Y.V }.str
rw₂ :
  (X.str ≫ F.map f.f) ≫ α.app { V := Y.V, str := Y.str ≫ α.app Y.V : Coalgebra G }.V =
    f.f ≫ { V := Y.V, str := Y.str ≫ α.app Y.V }.str
rw₃ :
  (f.f ≫ Y.str) ≫ α.app { V := Y.V, str := Y.str ≫ α.app Y.V : Coalgebra G }.V =
    f.f ≫ { V := Y.V, str := Y.str ≫ α.app Y.V }.str
rw₄ rw₅ :
  f.f ≫ Y.str ≫ α.app { V := Y.V, str := Y.str ≫ α.app Y.V : Coalgebra G }.V =
    f.f ≫ { V := Y.V, str := Y.str ≫ α.app Y.V }.str
⊢ { V := X.V, str := X.str ≫ α.app X.V : Coalgebra G }.str ≫ G.map f.f =
    f.f ≫ { V := Y.V, str := Y.str ≫ α.app Y.V }.str

Tactic:
rw [Category.assoc, ← α.naturality, ← Category.assoc, f.h, Category.assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Endofunctor.Coalgebra.Hom.h, CategoryTheory.NatTrans.naturality
-- Module: Mathlib.CategoryTheory.Endofunctor.Algebra
Goal:
C : Type u
inst : Category.{v, u} C
F_1 : Functor.{v, v, u, u} C C
V V₀ V₁ V₂ : Coalgebra F_1
f : V₀ ⟶ V₁
g : V₁ ⟶ V₂
F G : Functor.{v, v, u, u} C C
α : F ≅ G
⊢ 𝟙 F = α.hom ≫ α.inv

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Endofunctor.Algebra
Goal:
C : Type u
inst : Category.{v, u} C
F_1 : Functor.{v, v, u, u} C C
V V₀ V₁ V₂ : Coalgebra F_1
f : V₀ ⟶ V₁
g : V₁ ⟶ V₂
F G : Functor.{v, v, u, u} C C
α : F ≅ G
⊢ α.inv ≫ α.hom = 𝟙 G

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Endofunctor.Algebra
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{v, v, u, u} C C
V V₀ V₁ V₂ : Coalgebra F
f : V₀ ⟶ V₁
g : V₁ ⟶ V₂
A : Coalgebra F
h : Limits.IsTerminal A
rw : A.str ≫ F.map (A.str ≫ strInv h) = A.str ≫ strInv h ≫ A.str
rw₁ : A.str ≫ F.map A.str ≫ F.map (strInv h) = A.str ≫ strInv h ≫ A.str
rw₂ :
  Eq (α := A.V ⟶ F.obj A.V) (A.str ≫ F.map A.str ≫ F.map (Hom.f (h.from { V := F.obj A.V, str := F.map A.str })))
    (A.str ≫ Hom.f (h.from { V := F.obj A.V, str := F.map A.str }) ≫ A.str)
rw₃ rw₄ :
  A.str ≫ F.map A.str ≫ F.map (Hom.f (h.from { V := F.obj A.V, str := F.map A.str })) =
    A.str ≫
      { V := F.obj A.V, str := F.map A.str : Coalgebra F }.str ≫
        F.map (Hom.f (h.from { V := F.obj A.V, str := F.map A.str : Coalgebra F }))
⊢ A.str ≫ F.map (A.str ≫ strInv h) = (A.str ≫ strInv h) ≫ A.str

Tactic:
rw [Category.assoc, F.map_comp, strInv, ← Hom.h]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Endofunctor.Coalgebra.Hom.h, CategoryTheory.Functor.map_comp, CategoryTheory.Endofunctor.Coalgebra.Terminal.strInv
-- Module: Mathlib.CategoryTheory.Endofunctor.Algebra
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{v, v, u, u} C C
A : Coalgebra F
h : Limits.IsTerminal A
⊢ { f := A.str ≫ strInv h, h := ⋯ : A.Hom A } = 𝟙 A

Tactic:
Limits.IsTerminal.hom_ext h _ (𝟙 A)

Premises used: CategoryTheory.CategoryStruct.id, CategoryTheory.Limits.IsTerminal.hom_ext
-- Module: Mathlib.CategoryTheory.Endofunctor.Algebra
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{v, v, u, u} C C
A : Coalgebra F
h : Limits.IsTerminal A
⊢ A.str ≫ strInv h = 𝟙 A.V

Tactic:
congr_arg Hom.f (right_inv' h)

Premises used: CategoryTheory.Endofunctor.Coalgebra.Hom.f, congr_arg, CategoryTheory.Endofunctor.Coalgebra.Terminal.right_inv'
-- Module: Mathlib.CategoryTheory.Endofunctor.Algebra
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{v, v, u, u} C C
A : Coalgebra F
h : Limits.IsTerminal A
rw : F.map (A.str ≫ Hom.f (h.from { V := F.obj A.V, str := F.map A.str })) = F.map (𝟙 A.V)
⊢ strInv h ≫ A.str = 𝟙 (F.obj A.V)

Tactic:
rw [strInv, ← (h.from ⟨F.obj A.V, F.map A.str⟩).h, ← F.map_id, ← F.map_comp]

Premises used: CategoryTheory.Limits.IsTerminal.from, CategoryTheory.Endofunctor.Coalgebra.mk, CategoryTheory.Endofunctor.Coalgebra.str, CategoryTheory.Endofunctor.Coalgebra.V, CategoryTheory.Functor.map, CategoryTheory.Endofunctor.Coalgebra.Hom.h, CategoryTheory.Functor.map_id, CategoryTheory.Functor.map_comp, CategoryTheory.Functor.obj, CategoryTheory.Endofunctor.Coalgebra.Terminal.strInv
-- Module: Mathlib.CategoryTheory.Endofunctor.Algebra
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{v, v, u, u} C C
A : Coalgebra F
h : Limits.IsTerminal A
e_a : A.str ≫ Hom.f (h.from { V := F.obj A.V, str := F.map A.str }) = 𝟙 A.V
⊢ F.map (A.str ≫ Hom.f (h.from { V := F.obj A.V, str := F.map A.str })) = F.map (𝟙 A.V)

Tactic:
congr
-- Module: Mathlib.CategoryTheory.Endofunctor.Algebra
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{v, v, u, u} C C
A : Coalgebra F
h : Limits.IsTerminal A
⊢ A.str ≫ Hom.f (h.from { V := F.obj A.V, str := F.map A.str }) = 𝟙 A.V

Tactic:
right_inv h

Premises used: CategoryTheory.Endofunctor.Coalgebra.Terminal.right_inv, CategoryTheory.Endofunctor.Coalgebra.Terminal.strInv
-- Module: Mathlib.CategoryTheory.Endofunctor.Algebra
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{v, v, u, u} C C
A : Coalgebra F
h : Limits.IsTerminal A
⊢ A.str ≫ Hom.f (h.from { V := F.obj A.V, str := F.map A.str }) = 𝟙 A.V

Tactic:
exact right_inv h

Premises used: CategoryTheory.Endofunctor.Coalgebra.Terminal.right_inv
-- Module: Mathlib.CategoryTheory.Endofunctor.Algebra
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{v, v, u, u} C C
A : Coalgebra F
h : Limits.IsTerminal A
⊢ IsIso A.str

Tactic:
{ out := ⟨strInv h, right_inv _, left_inv _⟩  }

Premises used: CategoryTheory.Endofunctor.Coalgebra.Terminal.left_inv, CategoryTheory.Endofunctor.Coalgebra.Terminal.right_inv, And.intro, Exists.intro, CategoryTheory.IsIso.mk, CategoryTheory.Endofunctor.Coalgebra.Terminal.strInv