awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Elements (goal)
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
rw :
  Eq (α := Functor.obj uliftYoneda.{w, v, u} (unop (unop X).1) ⟶ F)
    ((Equiv.symm uliftYonedaEquiv :
          (a : F.obj (op (unop (unop X).fst))) → uliftYoneda.{w, v, u}.obj (unop (unop X).fst) ⟶ F)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (↑(unop f) : (unop Y).fst ⟶ (unop X).fst)) :
            (a : (fun (X : Type (max v w)) ↦ X) (F.obj (unop Y).fst)) →
              (fun (X : Type (max v w)) ↦ X) (F.obj (unop X).fst))
          ((unop Y).snd (β := fun (c : Cᵒᵖ) ↦ F.obj c))) :
      Functor.obj uliftYoneda.{w, v, u} (unop ((unop X).fst (β := fun (c : Cᵒᵖ) ↦ F.obj c))) ⟶ F)
    ((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)) :
      Functor.obj uliftYoneda.{w, v, u} (unop (unop X).1) ⟶ F)
⊢ Eq (α := Functor.obj uliftYoneda.{w, v, u} (unop (unop X).1) ⟶ F)
    (Functor.map uliftYoneda.{w, v, u} (↑(unop f) : (unop Y).fst ⟶ (unop X).fst).unop ≫
      (Equiv.symm uliftYonedaEquiv : (a : F.obj (unop Y).1) → uliftYoneda.{w, v, u}.obj (unop (unop Y).1) ⟶ F)
        ((unop Y).snd (β := fun (c : Cᵒᵖ) ↦ F.obj c)))
    ((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)))
have rw₁ : Eq (α := Functor.obj uliftYoneda.{w, v, u} (unop (unop X).1) ⟶ F)
  ((Equiv.symm uliftYonedaEquiv :
        (a : F.obj (op (unop (unop X).fst))) → uliftYoneda.{w, v, u}.obj (unop (unop X).fst) ⟶ F)
      ((unop X).snd (β := fun (c : Cᵒᵖ) ↦ F.obj c)) :
    Functor.obj uliftYoneda.{w, v, u} (unop ((unop X).fst (β := fun (c : Cᵒᵖ) ↦ F.obj c))) ⟶ F)
  ((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)) :
    Functor.obj uliftYoneda.{w, v, u} (unop (unop X).1) ⟶ F)
Tactic: rw [← uliftYonedaEquiv_symm_map, map_snd]
-- Lean 4 proof step from Mathlib.CategoryTheory.Elements (goal)
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 : CostructuredArrow uliftYoneda.{w, v, u} F
f : X ⟶ Y
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f.left.op) :
        (a :
            (fun (X : Type (max v w)) ↦ X)
              (F.obj
                (F.elementsMk (op Y.left)
                    ((uliftYonedaEquiv : (a : uliftYoneda.{w, v, u}.obj Y.left ⟶ F) → F.obj (op Y.left)) Y.hom)).fst)) →
          (fun (X : Type (max v w)) ↦ X)
            (F.obj
              (F.elementsMk (op X.left)
                  ((uliftYonedaEquiv : (a : uliftYoneda.{w, v, u}.obj X.left ⟶ F) → F.obj (op X.left)) X.hom)).fst))
      ((F.elementsMk (op Y.left)
            ((uliftYonedaEquiv : (a : uliftYoneda.{w, v, u}.obj Y.left ⟶ F) → F.obj (op Y.left)) Y.hom)).snd
        (β := fun (c : Cᵒᵖ) ↦ F.obj c)) =
    (F.elementsMk (op X.left)
          ((uliftYonedaEquiv : (a : uliftYoneda.{w, v, u}.obj X.left ⟶ F) → F.obj (op X.left)) X.hom)).snd
      (β := fun (c : Cᵒᵖ) ↦ F.obj c)
have dsimp : Eq (α := F.obj (op X.left))
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f.left.op) : (a : F.obj (op Y.left)) → F.obj (op X.left))
      ((uliftYonedaEquiv : (a : uliftYoneda.{w, v, u}.obj Y.left ⟶ F) → F.obj (op Y.left)) Y.hom) :
    F.obj (op X.left))
  ((uliftYonedaEquiv : (a : uliftYoneda.{w, v, u}.obj X.left ⟶ F) → F.obj (op X.left)) X.hom : F.obj (op X.left))
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Elements (goal)
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 : CostructuredArrow uliftYoneda.{w, v, u} F
f : X ⟶ Y
⊢ Eq (α := F.obj (op X.left))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f.left.op) : (a : F.obj (op Y.left)) → F.obj (op X.left))
        ((uliftYonedaEquiv : (a : uliftYoneda.{w, v, u}.obj Y.left ⟶ F) → F.obj (op Y.left)) Y.hom) :
      F.obj (op X.left))
    ((uliftYonedaEquiv : (a : uliftYoneda.{w, v, u}.obj X.left ⟶ F) → F.obj (op X.left)) X.hom : F.obj (op X.left))
have rw : Eq (α := F.obj (op X.left))
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f.left.op) : (a : F.obj (op Y.left)) → F.obj (op X.left))
      ((uliftYonedaEquiv : (a : uliftYoneda.{w, v, u}.obj Y.left ⟶ F) → F.obj (op Y.left)) Y.hom) :
    F.obj (op X.left))
  ((uliftYonedaEquiv : (a : uliftYoneda.{w, v, u}.obj X.left ⟶ F) → F.obj (op X.left))
      (Functor.map uliftYoneda.{w, v, u} f.left ≫ Y.hom) :
    F.obj (op X.left))
Tactic: rw [← CostructuredArrow.w f, uliftYonedaEquiv_naturality, Quiver.Hom.unop_op]
-- Lean 4 proof step from Mathlib.CategoryTheory.Elements (goal)
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 : CostructuredArrow uliftYoneda.{w, v, u} F
f : X ⟶ Y
rw :
  Eq (α := F.obj (op X.left))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f.left.op) : (a : F.obj (op Y.left)) → F.obj (op X.left))
        ((uliftYonedaEquiv : (a : uliftYoneda.{w, v, u}.obj Y.left ⟶ F) → F.obj (op Y.left)) Y.hom) :
      F.obj (op X.left))
    ((uliftYonedaEquiv : (a : uliftYoneda.{w, v, u}.obj X.left ⟶ F) → F.obj (op X.left))
        (Functor.map uliftYoneda.{w, v, u} f.left ≫ Y.hom) :
      F.obj (op X.left))
⊢ Eq (α := F.obj (op X.left))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f.left.op) : (a : F.obj (op Y.left)) → F.obj (op X.left))
        ((uliftYonedaEquiv : (a : uliftYoneda.{w, v, u}.obj Y.left ⟶ F) → F.obj (op Y.left)) Y.hom) :
      F.obj (op X.left))
    ((uliftYonedaEquiv : (a : uliftYoneda.{w, v, u}.obj X.left ⟶ F) → F.obj (op X.left)) X.hom : F.obj (op X.left))
have rw₁ : Eq (α := F.obj (op X.left))
  ((uliftYonedaEquiv : (a : uliftYoneda.{w, v, u}.obj (unop (op X.left)) ⟶ F) → F.obj (op (unop (op X.left))))
      (Functor.map uliftYoneda.{w, v, u} f.left.op.unop ≫ Y.hom) :
    F.obj (op (unop (op X.left))))
  ((uliftYonedaEquiv : (a : uliftYoneda.{w, v, u}.obj X.left ⟶ F) → F.obj (op X.left))
      (Functor.map uliftYoneda.{w, v, u} f.left ≫ Y.hom) :
    F.obj (op X.left))
Tactic: rw [← CostructuredArrow.w f, uliftYonedaEquiv_naturality, Quiver.Hom.unop_op]
-- Lean 4 proof step from Mathlib.CategoryTheory.Elements (goal)
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 : CostructuredArrow uliftYoneda.{w, v, u} F
f : X ⟶ Y
rw :
  Eq (α := F.obj (op X.left))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f.left.op) : (a : F.obj (op Y.left)) → F.obj (op X.left))
        ((uliftYonedaEquiv : (a : uliftYoneda.{w, v, u}.obj Y.left ⟶ F) → F.obj (op Y.left)) Y.hom) :
      F.obj (op X.left))
    ((uliftYonedaEquiv : (a : uliftYoneda.{w, v, u}.obj X.left ⟶ F) → F.obj (op X.left))
        (Functor.map uliftYoneda.{w, v, u} f.left ≫ Y.hom) :
      F.obj (op X.left))
rw₁ :
  Eq (α := F.obj (op X.left))
    ((uliftYonedaEquiv : (a : uliftYoneda.{w, v, u}.obj (unop (op X.left)) ⟶ F) → F.obj (op (unop (op X.left))))
        (Functor.map uliftYoneda.{w, v, u} f.left.op.unop ≫ Y.hom) :
      F.obj (op (unop (op X.left))))
    ((uliftYonedaEquiv : (a : uliftYoneda.{w, v, u}.obj X.left ⟶ F) → F.obj (op X.left))
        (Functor.map uliftYoneda.{w, v, u} f.left ≫ Y.hom) :
      F.obj (op X.left))
⊢ Eq (α := F.obj (op X.left))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f.left.op) : (a : F.obj (op Y.left)) → F.obj (op X.left))
        ((uliftYonedaEquiv : (a : uliftYoneda.{w, v, u}.obj Y.left ⟶ F) → F.obj (op Y.left)) Y.hom) :
      F.obj (op X.left))
    ((uliftYonedaEquiv : (a : uliftYoneda.{w, v, u}.obj X.left ⟶ F) → F.obj (op X.left)) X.hom : F.obj (op X.left))
have rw₂ : Eq (α := F.obj (op X.left))
  ((uliftYonedaEquiv : (a : uliftYoneda.{w, v, u}.obj (unop (op X.left)) ⟶ F) → F.obj (op (unop (op X.left))))
      (Functor.map uliftYoneda.{w, v, u} f.left ≫ Y.hom) :
    F.obj (op (unop (op X.left))))
  ((uliftYonedaEquiv : (a : uliftYoneda.{w, v, u}.obj X.left ⟶ F) → F.obj (op X.left))
      (Functor.map uliftYoneda.{w, v, u} f.left ≫ Y.hom) :
    F.obj (op X.left))
Tactic: rw [← CostructuredArrow.w f, uliftYonedaEquiv_naturality, Quiver.Hom.unop_op]
-- Lean 4 proof step from Mathlib.CategoryTheory.Elements (goal)
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ᵒᵖ
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
have dsimp : (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: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Endofunctor.Algebra (goal)
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 ≫ A₀.str = A₁.str ≫ h.inv
have rw : F.map (h.inv ≫ h.hom) ≫ A₁.str = A₁.str
Tactic: rw [h.eq_comp_inv, Category.assoc, ← w, ← Functor.map_comp_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Endofunctor.Algebra (goal)
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
⊢ F.map (strInv h ≫ A.str) ≫ A.str = A.str ≫ strInv h ≫ A.str
have rw : F.map (strInv h ≫ A.str) ≫ A.str = (A.str ≫ strInv h) ≫ A.str
Tactic: rw [← Category.assoc, F.map_comp, strInv, ← Hom.h]
-- Lean 4 proof step from Mathlib.CategoryTheory.Endofunctor.Algebra (goal)
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
⊢ F.map (strInv h ≫ A.str) ≫ A.str = A.str ≫ strInv h ≫ A.str
have rw₁ : (F.map (strInv h) ≫ F.map A.str) ≫ A.str = (A.str ≫ strInv h) ≫ A.str
Tactic: rw [← Category.assoc, F.map_comp, strInv, ← Hom.h]
-- Lean 4 proof step from Mathlib.CategoryTheory.Endofunctor.Algebra (goal)
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
⊢ F.map (strInv h ≫ A.str) ≫ A.str = A.str ≫ strInv h ≫ A.str
have 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
Tactic: rw [← Category.assoc, F.map_comp, strInv, ← Hom.h]
-- Lean 4 proof step from Mathlib.CategoryTheory.Endofunctor.Algebra (goal)
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
⊢ F.map (strInv h ≫ A.str) ≫ A.str = A.str ≫ strInv h ≫ A.str
have 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
Tactic: rw [← Category.assoc, F.map_comp, strInv, ← Hom.h]
-- Lean 4 proof step from Mathlib.CategoryTheory.Endofunctor.Algebra (goal)
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{v, v, u, u} C C
A : Algebra F
h : Limits.IsInitial A
⊢ A.str ≫ strInv h = 𝟙 (F.obj A.a)
have rw : F.map (Hom.f (h.to { a := F.obj A.a, str := F.map A.str }) ≫ A.str) = F.map (𝟙 A.a)
Tactic: rw [strInv, ← (h.to ⟨F.obj A.1, F.map A.str⟩).h, ← F.map_id, ← F.map_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Endofunctor.Algebra (goal)
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.map (Hom.f (h.to { a := F.obj A.a, str := F.map A.str }) ≫ A.str) = F.map (𝟙 A.a)
have e_a : Hom.f (h.to { a := F.obj A.a, str := F.map A.str }) ≫ A.str = 𝟙 A.a
Tactic: congr
-- Lean 4 proof step from Mathlib.CategoryTheory.Endofunctor.Algebra (goal)
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.inv = h.inv ≫ V₀.str
have rw : V₀.str ≫ F.map (h.hom ≫ h.inv) = V₀.str
Tactic: rw [h.eq_inv_comp, ← Category.assoc, ← w, Category.assoc, ← F.map_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Endofunctor.Algebra (goal)
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 (inv f.f) = inv f.f ≫ V₀.str
have rw : V₀.str ≫ F.map f.f ≫ F.map (inv f.f) = V₀.str
Tactic: rw [IsIso.eq_inv_comp f.1, ← Category.assoc, ← f.h, Category.assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Endofunctor.Algebra (goal)
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
⊢ { 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
have rw : X.str ≫ α.app X.V ≫ 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]
-- Lean 4 proof step from Mathlib.CategoryTheory.Endofunctor.Algebra (goal)
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
⊢ { 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
have 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
Tactic: rw [Category.assoc, ← α.naturality, ← Category.assoc, f.h, Category.assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Endofunctor.Algebra (goal)
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
⊢ { 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
have 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
Tactic: rw [Category.assoc, ← α.naturality, ← Category.assoc, f.h, Category.assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Endofunctor.Algebra (goal)
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
⊢ { 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
have 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
Tactic: rw [Category.assoc, ← α.naturality, ← Category.assoc, f.h, Category.assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Endofunctor.Algebra (goal)
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
⊢ { 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
have 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
Tactic: rw [Category.assoc, ← α.naturality, ← Category.assoc, f.h, Category.assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Endofunctor.Algebra (goal)
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
⊢ A.str ≫ F.map (A.str ≫ strInv h) = (A.str ≫ strInv h) ≫ A.str
have rw : A.str ≫ F.map (A.str ≫ strInv h) = A.str ≫ strInv h ≫ A.str
Tactic: rw [Category.assoc, F.map_comp, strInv, ← Hom.h]
-- Lean 4 proof step from Mathlib.CategoryTheory.Endofunctor.Algebra (goal)
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
⊢ A.str ≫ F.map (A.str ≫ strInv h) = (A.str ≫ strInv h) ≫ A.str
have rw₁ : A.str ≫ F.map A.str ≫ F.map (strInv h) = A.str ≫ strInv h ≫ A.str
Tactic: rw [Category.assoc, F.map_comp, strInv, ← Hom.h]
-- Lean 4 proof step from Mathlib.CategoryTheory.Endofunctor.Algebra (goal)
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
⊢ A.str ≫ F.map (A.str ≫ strInv h) = (A.str ≫ strInv h) ≫ A.str
have 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)
Tactic: rw [Category.assoc, F.map_comp, strInv, ← Hom.h]
-- Lean 4 proof step from Mathlib.CategoryTheory.Endofunctor.Algebra (goal)
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)
⊢ A.str ≫ F.map (A.str ≫ strInv h) = (A.str ≫ strInv h) ≫ A.str
have 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 }))
Tactic: rw [Category.assoc, F.map_comp, strInv, ← Hom.h]
-- Lean 4 proof step from Mathlib.CategoryTheory.Endofunctor.Algebra (goal)
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{v, v, u, u} C C
A : Coalgebra F
h : Limits.IsTerminal A
⊢ strInv h ≫ A.str = 𝟙 (F.obj A.V)
have rw : F.map (A.str ≫ Hom.f (h.from { V := F.obj A.V, str := F.map A.str })) = F.map (𝟙 A.V)
Tactic: rw [strInv, ← (h.from ⟨F.obj A.V, F.map A.str⟩).h, ← F.map_id, ← F.map_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Endofunctor.Algebra (goal)
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.map (A.str ≫ Hom.f (h.from { V := F.obj A.V, str := F.map A.str })) = F.map (𝟙 A.V)
have e_a : A.str ≫ Hom.f (h.from { V := F.obj A.V, str := F.map A.str }) = 𝟙 A.V
Tactic: congr
-- Lean 4 proof step from Mathlib.CategoryTheory.Endofunctor.Algebra (goal)
Goal:
C : Type u
inst : Category.{v, u} C
F G : Functor.{v, v, u, u} C C
adj : F ⊣ G
A₁ A₂ : Algebra F
f : A₁ ⟶ A₂
⊢ Eq (α := A₁.a ⟶ G.obj A₂.a)
    ((adj.homEquiv A₁.a A₁.a : (a : F.obj A₁.a ⟶ A₁.a) → A₁.a ⟶ G.obj A₁.a) A₁.str ≫ G.map f.f : A₁.a ⟶ G.obj A₂.a)
    (f.f ≫ (adj.homEquiv A₂.a A₂.a : (a : F.obj A₂.a ⟶ A₂.a) → A₂.a ⟶ G.obj A₂.a) A₂.str : A₁.a ⟶ G.obj A₂.a)
have rw : Eq (α := A₁.a ⟶ G.obj A₂.a)
  ((adj.homEquiv A₁.a A₂.a : (a : F.obj A₁.a ⟶ A₂.a) → A₁.a ⟶ G.obj A₂.a) (A₁.str ≫ f.f) : A₁.a ⟶ G.obj A₂.a)
  (f.f ≫ (adj.homEquiv A₂.a A₂.a : (a : F.obj A₂.a ⟶ A₂.a) → A₂.a ⟶ G.obj A₂.a) A₂.str : A₁.a ⟶ G.obj A₂.a)
Tactic: rw [← Adjunction.homEquiv_naturality_right, ← Adjunction.homEquiv_naturality_left, f.h]
-- Lean 4 proof step from Mathlib.CategoryTheory.Endofunctor.Algebra (goal)
Goal:
C : Type u
inst : Category.{v, u} C
F G : Functor.{v, v, u, u} C C
adj : F ⊣ G
A₁ A₂ : Algebra F
f : A₁ ⟶ A₂
rw :
  Eq (α := A₁.a ⟶ G.obj A₂.a)
    ((adj.homEquiv A₁.a A₂.a : (a : F.obj A₁.a ⟶ A₂.a) → A₁.a ⟶ G.obj A₂.a) (A₁.str ≫ f.f) : A₁.a ⟶ G.obj A₂.a)
    (f.f ≫ (adj.homEquiv A₂.a A₂.a : (a : F.obj A₂.a ⟶ A₂.a) → A₂.a ⟶ G.obj A₂.a) A₂.str : A₁.a ⟶ G.obj A₂.a)
⊢ Eq (α := A₁.a ⟶ G.obj A₂.a)
    ((adj.homEquiv A₁.a A₁.a : (a : F.obj A₁.a ⟶ A₁.a) → A₁.a ⟶ G.obj A₁.a) A₁.str ≫ G.map f.f : A₁.a ⟶ G.obj A₂.a)
    (f.f ≫ (adj.homEquiv A₂.a A₂.a : (a : F.obj A₂.a ⟶ A₂.a) → A₂.a ⟶ G.obj A₂.a) A₂.str : A₁.a ⟶ G.obj A₂.a)
have rw₁ : Eq (α := A₁.a ⟶ G.obj A₂.a)
  ((adj.homEquiv A₁.a A₂.a : (a : F.obj A₁.a ⟶ A₂.a) → A₁.a ⟶ G.obj A₂.a) (A₁.str ≫ f.f) : A₁.a ⟶ G.obj A₂.a)
  ((adj.homEquiv A₁.a A₂.a : (a : F.obj A₁.a ⟶ A₂.a) → A₁.a ⟶ G.obj A₂.a) (F.map f.f ≫ A₂.str) : A₁.a ⟶ G.obj A₂.a)
Tactic: rw [← Adjunction.homEquiv_naturality_right, ← Adjunction.homEquiv_naturality_left, f.h]
-- Lean 4 proof step from Mathlib.CategoryTheory.Endofunctor.Algebra (goal)
Goal:
C : Type u
inst : Category.{v, u} C
F G : Functor.{v, v, u, u} C C
adj : F ⊣ G
A₁ A₂ : Algebra F
f : A₁ ⟶ A₂
rw :
  Eq (α := A₁.a ⟶ G.obj A₂.a)
    ((adj.homEquiv A₁.a A₂.a : (a : F.obj A₁.a ⟶ A₂.a) → A₁.a ⟶ G.obj A₂.a) (A₁.str ≫ f.f) : A₁.a ⟶ G.obj A₂.a)
    (f.f ≫ (adj.homEquiv A₂.a A₂.a : (a : F.obj A₂.a ⟶ A₂.a) → A₂.a ⟶ G.obj A₂.a) A₂.str : A₁.a ⟶ G.obj A₂.a)
rw₁ :
  Eq (α := A₁.a ⟶ G.obj A₂.a)
    ((adj.homEquiv A₁.a A₂.a : (a : F.obj A₁.a ⟶ A₂.a) → A₁.a ⟶ G.obj A₂.a) (A₁.str ≫ f.f) : A₁.a ⟶ G.obj A₂.a)
    ((adj.homEquiv A₁.a A₂.a : (a : F.obj A₁.a ⟶ A₂.a) → A₁.a ⟶ G.obj A₂.a) (F.map f.f ≫ A₂.str) : A₁.a ⟶ G.obj A₂.a)
⊢ Eq (α := A₁.a ⟶ G.obj A₂.a)
    ((adj.homEquiv A₁.a A₁.a : (a : F.obj A₁.a ⟶ A₁.a) → A₁.a ⟶ G.obj A₁.a) A₁.str ≫ G.map f.f : A₁.a ⟶ G.obj A₂.a)
    (f.f ≫ (adj.homEquiv A₂.a A₂.a : (a : F.obj A₂.a ⟶ A₂.a) → A₂.a ⟶ G.obj A₂.a) A₂.str : A₁.a ⟶ G.obj A₂.a)
have rw₂ : Eq (α := A₁.a ⟶ G.obj A₂.a)
  ((adj.homEquiv A₁.a A₂.a : (a : F.obj A₁.a ⟶ A₂.a) → A₁.a ⟶ G.obj A₂.a) (A₁.str ≫ f.f) : A₁.a ⟶ G.obj A₂.a)
  ((adj.homEquiv A₁.a A₂.a : (a : F.obj A₁.a ⟶ A₂.a) → A₁.a ⟶ G.obj A₂.a) (A₁.str ≫ f.f) : A₁.a ⟶ G.obj A₂.a)
Tactic: rw [← Adjunction.homEquiv_naturality_right, ← Adjunction.homEquiv_naturality_left, f.h]