awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Adjunction (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
L : Functor.{v₁, v₂, u₁, u₂} C D
R : Functor.{v₂, v₁, u₂, u₁} D C
inst_2 : Reflective R
X : (Adjunction.toMonad (L := reflector R) (reflectorAdjunction R)).Algebra
refine_1 :
  X.A ≅
    Monad.Algebra.A (T := Adjunction.toMonad (L := reflector R) (reflectorAdjunction R))
      (obj (Monad.comparison (reflectorAdjunction R)) ((reflector R).obj X.A))
⊢ X ≅ obj (Monad.comparison (reflectorAdjunction R)) ((reflector R).obj X.A)
have refine_2 : Eq (α :=
  (Adjunction.toMonad (L := reflector R) (reflectorAdjunction R)).obj X.A ⟶
    Monad.Algebra.A (T := Adjunction.toMonad (L := reflector R) (reflectorAdjunction R))
      (obj (Monad.comparison (reflectorAdjunction R)) ((reflector R).obj X.A)))
  (CategoryStruct.comp (Y :=
    (Adjunction.toMonad (L := reflector R) (reflectorAdjunction R)).obj
      (Monad.Algebra.A (T := Adjunction.toMonad (L := reflector R) (reflectorAdjunction R))
        (obj (Monad.comparison (reflectorAdjunction R)) ((reflector R).obj X.A))))
    ((Adjunction.toMonad (L := reflector R) (reflectorAdjunction R)).map
      (Iso.hom (asIso (NatTrans.app (Adjunction.unit (reflectorAdjunction R)) X.A))))
    (Monad.Algebra.a (obj (Monad.comparison (reflectorAdjunction R)) ((reflector R).obj X.A))))
  (X.a ≫ Iso.hom (asIso (NatTrans.app (Adjunction.unit (reflectorAdjunction R)) X.A)))
Tactic: refine Monad.Algebra.isoMk ?_ ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Adjunction (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
L : Functor.{v₁, v₂, u₁, u₂} C D
R : Functor.{v₂, v₁, u₂, u₁} D C
inst_2 : Reflective R
X : (Adjunction.toMonad (L := reflector R) (reflectorAdjunction R)).Algebra
⊢ Eq (α :=
    (Adjunction.toMonad (L := reflector R) (reflectorAdjunction R)).obj X.A ⟶
      Monad.Algebra.A (T := Adjunction.toMonad (L := reflector R) (reflectorAdjunction R))
        (obj (Monad.comparison (reflectorAdjunction R)) ((reflector R).obj X.A)))
    (CategoryStruct.comp (Y :=
      (Adjunction.toMonad (L := reflector R) (reflectorAdjunction R)).obj
        (Monad.Algebra.A (T := Adjunction.toMonad (L := reflector R) (reflectorAdjunction R))
          (obj (Monad.comparison (reflectorAdjunction R)) ((reflector R).obj X.A))))
      ((Adjunction.toMonad (L := reflector R) (reflectorAdjunction R)).map
        (Iso.hom (asIso (NatTrans.app (Adjunction.unit (reflectorAdjunction R)) X.A))))
      (Monad.Algebra.a (obj (Monad.comparison (reflectorAdjunction R)) ((reflector R).obj X.A))))
    (X.a ≫ Iso.hom (asIso (NatTrans.app (Adjunction.unit (reflectorAdjunction R)) X.A)))
have refine_2 : Eq (α := R.obj ((reflector R).obj X.A) ⟶ R.obj ((reflector R).obj X.A))
  (R.map ((reflector R).map (NatTrans.app (Adjunction.unit (reflectorAdjunction R)) X.A)) ≫
    R.map (NatTrans.app (Adjunction.counit (reflectorAdjunction R)) ((reflector R).obj X.A)))
  (X.a ≫ NatTrans.app (Adjunction.unit (reflectorAdjunction R)) X.A)
Tactic: dsimp only [Functor.comp_map, Monad.comparison_obj_a, asIso_hom, Functor.comp_obj,
    Monad.comparison_obj_A, Adjunction.toMonad_coe]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Adjunction (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
L : Functor.{v₁, v₂, u₁, u₂} C D
R : Functor.{v₂, v₁, u₂, u₁} D C
inst_2 : Reflective R
X : (Adjunction.toMonad (L := reflector R) (reflectorAdjunction R)).Algebra
⊢ Eq (α := R.obj ((reflector R).obj X.A) ⟶ R.obj ((reflector R).obj X.A))
    (R.map ((reflector R).map (NatTrans.app (Adjunction.unit (reflectorAdjunction R)) X.A)) ≫
      R.map (NatTrans.app (Adjunction.counit (reflectorAdjunction R)) ((reflector R).obj X.A)))
    (X.a ≫ NatTrans.app (Adjunction.unit (reflectorAdjunction R)) X.A)
have refine_2 : Eq (α := obj.{v₁, v₁, u₁, u₁} (𝟭 C) X.A ⟶ R.obj ((reflector R).obj X.A))
  (NatTrans.app (Adjunction.unit (reflectorAdjunction R)) X.A ≫
    R.map ((reflector R).map (NatTrans.app (Adjunction.unit (reflectorAdjunction R)) X.A)) ≫
      R.map (NatTrans.app (Adjunction.counit (reflectorAdjunction R)) ((reflector R).obj X.A)))
  (NatTrans.app (Adjunction.unit (reflectorAdjunction R)) X.A ≫
    X.a ≫ NatTrans.app (Adjunction.unit (reflectorAdjunction R)) X.A)
Tactic: rw [← cancel_epi ((reflectorAdjunction R).unit.app X.A)]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Adjunction (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
L : Functor.{v₁, v₂, u₁, u₂} C D
R : Functor.{v₂, v₁, u₂, u₁} D C
inst_2 : Reflective R
X : (Adjunction.toMonad (L := reflector R) (reflectorAdjunction R)).Algebra
⊢ Eq (α := X.A ⟶ R.obj ((reflector R).obj X.A))
    (NatTrans.app (Adjunction.unit (reflectorAdjunction R)) X.A ≫
      R.map ((reflector R).map (NatTrans.app (Adjunction.unit (reflectorAdjunction R)) X.A)) ≫
        R.map (NatTrans.app (Adjunction.counit (reflectorAdjunction R)) ((reflector R).obj X.A)))
    (NatTrans.app (Adjunction.unit (reflectorAdjunction R)) X.A ≫
      X.a ≫ NatTrans.app (Adjunction.unit (reflectorAdjunction R)) X.A)
have refine_2 : Eq (α := X.A ⟶ R.obj ((reflector R).obj X.A)) (NatTrans.app (Adjunction.unit (reflectorAdjunction R)) X.A)
  (NatTrans.app (Adjunction.unit (reflectorAdjunction R)) X.A ≫
    X.a ≫ NatTrans.app (Adjunction.unit (reflectorAdjunction R)) X.A)
Tactic: rw [Adjunction.unit_naturality_assoc,
    Adjunction.right_triangle_components, comp_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Adjunction (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
L : Functor.{v₁, v₂, u₁, u₂} C D
R : Functor.{v₂, v₁, u₂, u₁} D C
inst_2 : Coreflective R
X : (Adjunction.toComonad (R := coreflector R) (coreflectorAdjunction R)).Coalgebra
⊢ NatTrans.app (Adjunction.counit (coreflectorAdjunction R)) X.A ≫ X.a = 𝟙 ((coreflector R ⋙ R).obj X.A)
have rw : R.map ((coreflector R).map X.a) ≫
    NatTrans.app (Adjunction.counit (coreflectorAdjunction R)) ((coreflector R ⋙ R).obj X.A) =
  𝟙 ((coreflector R ⋙ R).obj X.A)
Tactic: rw [← (coreflectorAdjunction R).counit_naturality]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Adjunction (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
L : Functor.{v₁, v₂, u₁, u₂} C D
R : Functor.{v₂, v₁, u₂, u₁} D C
inst_2 : Coreflective R
X : (Adjunction.toComonad (R := coreflector R) (coreflectorAdjunction R)).Coalgebra
⊢ R.map ((coreflector R).map X.a) ≫
      NatTrans.app (Adjunction.counit (coreflectorAdjunction R)) ((coreflector R ⋙ R).obj X.A) =
    𝟙 ((coreflector R ⋙ R).obj X.A)
have dsimp : R.map ((coreflector R).map X.a) ≫
    NatTrans.app (Adjunction.counit (coreflectorAdjunction R)) (R.obj ((coreflector R).obj X.A)) =
  𝟙 (R.obj ((coreflector R).obj X.A))
Tactic: dsimp only [Functor.comp_obj, Adjunction.toMonad_coe]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Adjunction (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
L : Functor.{v₁, v₂, u₁, u₂} C D
R : Functor.{v₂, v₁, u₂, u₁} D C
inst_2 : Coreflective R
X : (Adjunction.toComonad (R := coreflector R) (coreflectorAdjunction R)).Coalgebra
⊢ R.map ((coreflector R).map X.a) ≫
      NatTrans.app (Adjunction.counit (coreflectorAdjunction R)) (R.obj ((coreflector R).obj X.A)) =
    𝟙 (R.obj ((coreflector R).obj X.A))
have rw : R.map ((coreflector R).map (X.a ≫ NatTrans.app (Adjunction.counit (coreflectorAdjunction R)) X.A)) =
  𝟙 (R.obj ((coreflector R).obj X.A))
Tactic: rw [counit_obj_eq_map_counit, ← Functor.map_comp, ← Functor.map_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Adjunction (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
L : Functor.{v₁, v₂, u₁, u₂} C D
R : Functor.{v₂, v₁, u₂, u₁} D C
inst_2 : Coreflective R
⊢ EssSurj (D := (Adjunction.toComonad (R := coreflector R) (coreflectorAdjunction R)).Coalgebra)
    (Comonad.comparison (coreflectorAdjunction R))
have refine : (X : (Adjunction.toComonad (R := coreflector R) (coreflectorAdjunction R)).Coalgebra) →
  obj (Comonad.comparison (coreflectorAdjunction R)) ((coreflector R).obj X.A) ≅ X
Tactic: refine ⟨fun X => ⟨(coreflector R).obj X.A, ⟨?_⟩⟩⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Adjunction (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
L : Functor.{v₁, v₂, u₁, u₂} C D
R : Functor.{v₂, v₁, u₂, u₁} D C
inst_2 : Coreflective R
X : (Adjunction.toComonad (R := coreflector R) (coreflectorAdjunction R)).Coalgebra
⊢ obj (Comonad.comparison (coreflectorAdjunction R)) ((coreflector R).obj X.A) ≅ X
have refine_1 : Comonad.Coalgebra.A (G := Adjunction.toComonad (R := coreflector R) (coreflectorAdjunction R))
    (obj (Comonad.comparison (coreflectorAdjunction R)) ((coreflector R).obj X.A)) ≅
  X.A
Tactic: refine Comonad.Coalgebra.isoMk ?_ ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Adjunction (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
L : Functor.{v₁, v₂, u₁, u₂} C D
R : Functor.{v₂, v₁, u₂, u₁} D C
inst_2 : Coreflective R
X : (Adjunction.toComonad (R := coreflector R) (coreflectorAdjunction R)).Coalgebra
refine_1 :
  Comonad.Coalgebra.A (G := Adjunction.toComonad (R := coreflector R) (coreflectorAdjunction R))
      (obj (Comonad.comparison (coreflectorAdjunction R)) ((coreflector R).obj X.A)) ≅
    X.A
⊢ obj (Comonad.comparison (coreflectorAdjunction R)) ((coreflector R).obj X.A) ≅ X
have refine_2 : Eq (α :=
  Comonad.Coalgebra.A (G := Adjunction.toComonad (R := coreflector R) (coreflectorAdjunction R))
      (obj (Comonad.comparison (coreflectorAdjunction R)) ((coreflector R).obj X.A)) ⟶
    (Adjunction.toComonad (R := coreflector R) (coreflectorAdjunction R)).obj X.A)
  (Comonad.Coalgebra.a (obj (Comonad.comparison (coreflectorAdjunction R)) ((coreflector R).obj X.A)) ≫
    (Adjunction.toComonad (R := coreflector R) (coreflectorAdjunction R)).map
      (Iso.hom (asIso (NatTrans.app (Adjunction.counit (coreflectorAdjunction R)) X.A))))
  (Iso.hom (asIso (NatTrans.app (Adjunction.counit (coreflectorAdjunction R)) X.A)) ≫ X.a)
Tactic: refine Comonad.Coalgebra.isoMk ?_ ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Adjunction (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
L : Functor.{v₁, v₂, u₁, u₂} C D
R : Functor.{v₂, v₁, u₂, u₁} D C
inst_2 : Coreflective R
X : (Adjunction.toComonad (R := coreflector R) (coreflectorAdjunction R)).Coalgebra
⊢ Eq (α :=
    Comonad.Coalgebra.A (G := Adjunction.toComonad (R := coreflector R) (coreflectorAdjunction R))
        (obj (Comonad.comparison (coreflectorAdjunction R)) ((coreflector R).obj X.A)) ⟶
      (Adjunction.toComonad (R := coreflector R) (coreflectorAdjunction R)).obj X.A)
    (Comonad.Coalgebra.a (obj (Comonad.comparison (coreflectorAdjunction R)) ((coreflector R).obj X.A)) ≫
      (Adjunction.toComonad (R := coreflector R) (coreflectorAdjunction R)).map
        (Iso.hom (asIso (NatTrans.app (Adjunction.counit (coreflectorAdjunction R)) X.A))))
    (Iso.hom (asIso (NatTrans.app (Adjunction.counit (coreflectorAdjunction R)) X.A)) ≫ X.a)
have refine_2 : Eq (α :=
  Comonad.Coalgebra.A (G := Adjunction.toComonad (R := coreflector R) (coreflectorAdjunction R))
      (obj (Comonad.comparison (coreflectorAdjunction R)) ((coreflector R).obj X.A)) ⟶
    obj.{v₁, v₁, u₁, u₁} (𝟭 C) X.A)
  (CategoryStruct.comp (Y := (coreflector R ⋙ R).obj X.A)
    (Comonad.Coalgebra.a (obj (Comonad.comparison (coreflectorAdjunction R)) ((coreflector R).obj X.A)) ≫
      (Adjunction.toComonad (R := coreflector R) (coreflectorAdjunction R)).map
        (Iso.hom (asIso (NatTrans.app (Adjunction.counit (coreflectorAdjunction R)) X.A))))
    (NatTrans.app (Adjunction.counit (coreflectorAdjunction R)) X.A))
  ((Iso.hom (asIso (NatTrans.app (Adjunction.counit (coreflectorAdjunction R)) X.A)) ≫ X.a) ≫
    NatTrans.app (Adjunction.counit (coreflectorAdjunction R)) X.A)
Tactic: rw [← cancel_mono ((coreflectorAdjunction R).counit.app X.A)]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Adjunction (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
L : Functor.{v₁, v₂, u₁, u₂} C D
R : Functor.{v₂, v₁, u₂, u₁} D C
inst_2 : Coreflective R
X : (Adjunction.toComonad (R := coreflector R) (coreflectorAdjunction R)).Coalgebra
⊢ Eq (α :=
    Comonad.Coalgebra.A (G := Adjunction.toComonad (R := coreflector R) (coreflectorAdjunction R))
        (obj (Comonad.comparison (coreflectorAdjunction R)) ((coreflector R).obj X.A)) ⟶
      obj.{v₁, v₁, u₁, u₁} (𝟭 C) X.A)
    (CategoryStruct.comp (Y := (coreflector R ⋙ R).obj X.A)
      (Comonad.Coalgebra.a (obj (Comonad.comparison (coreflectorAdjunction R)) ((coreflector R).obj X.A)) ≫
        (Adjunction.toComonad (R := coreflector R) (coreflectorAdjunction R)).map
          (Iso.hom (asIso (NatTrans.app (Adjunction.counit (coreflectorAdjunction R)) X.A))))
      (NatTrans.app (Adjunction.counit (coreflectorAdjunction R)) X.A))
    ((Iso.hom (asIso (NatTrans.app (Adjunction.counit (coreflectorAdjunction R)) X.A)) ≫ X.a) ≫
      NatTrans.app (Adjunction.counit (coreflectorAdjunction R)) X.A)
have refine_2 : Eq (α :=
  Comonad.Coalgebra.A (G := Adjunction.toComonad (R := coreflector R) (coreflectorAdjunction R))
      (obj (Comonad.comparison (coreflectorAdjunction R)) ((coreflector R).obj X.A)) ⟶
    X.A)
  (Comonad.Coalgebra.a (obj (Comonad.comparison (coreflectorAdjunction R)) ((coreflector R).obj X.A)) ≫
    (Adjunction.toComonad (R := coreflector R) (coreflectorAdjunction R)).map
        (Iso.hom (asIso (NatTrans.app (Adjunction.counit (coreflectorAdjunction R)) X.A))) ≫
      NatTrans.app (Adjunction.counit (coreflectorAdjunction R)) X.A)
  (Iso.hom (asIso (NatTrans.app (Adjunction.counit (coreflectorAdjunction R)) X.A)) ≫
    X.a ≫ NatTrans.app (Adjunction.counit (coreflectorAdjunction R)) X.A)
Tactic: simp only [Functor.comp_obj, Functor.id_obj,
    assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Algebra (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
T : Monad.{v₁, u₁} C
A B : T.Algebra
h : A.A ≅ B.A
w : T.map h.hom ≫ B.a = A.a ≫ h.hom
⊢ T.map h.inv ≫ A.a = B.a ≫ h.inv
have rw : T.map (h.inv ≫ h.hom) ≫ B.a = B.a
Tactic: rw [h.eq_comp_inv, Category.assoc, ← w, ← Functor.map_comp_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Algebra (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
T : Monad.{v₁, u₁} C
X : C
Y : T.Algebra
f : T.free.obj X ⟶ Y
⊢ (fun (f : X ⟶ T.forget.obj Y) ↦ { f := T.map f ≫ Y.a, h := ⋯ : (T.free.obj X).Hom Y })
      ((fun (f : T.free.obj X ⟶ Y) ↦ T.η.app X ≫ f.f) f) =
    f
have h : Algebra.Hom.f
    ((fun (f : X ⟶ T.forget.obj Y) ↦ { f := T.map f ≫ Y.a, h := sorry : (T.free.obj X).Hom Y })
      ((fun (f : T.free.obj X ⟶ Y) ↦ T.η.app X ≫ f.f) f)) =
  f.f
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Algebra (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
T : Monad.{v₁, u₁} C
X : C
Y : T.Algebra
f : X ⟶ T.forget.obj Y
⊢ (fun (f : T.free.obj X ⟶ Y) ↦ T.η.app X ≫ f.f)
      ((fun (f : X ⟶ T.forget.obj Y) ↦ { f := T.map f ≫ Y.a, h := ⋯ : (T.free.obj X).Hom Y }) f) =
    f
have dsimp : T.η.app X ≫ T.map f ≫ Y.a = f
Tactic: dsimp only [forget_obj]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Algebra (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
T : Monad.{v₁, u₁} C
X : C
Y : T.Algebra
f : X ⟶ T.forget.obj Y
⊢ T.η.app X ≫ T.map f ≫ Y.a = f
have rw : Functor.map (𝟭 C) f ≫ 𝟙 Y.A = f
Tactic: rw [← T.η.naturality_assoc, Y.unit]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Algebra (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
G : Comonad.{v₁, u₁} C
A B : G.Coalgebra
h : A.A ≅ B.A
w : A.a ≫ G.map h.hom = h.hom ≫ B.a
⊢ B.a ≫ G.map h.inv = h.inv ≫ A.a
have rw : A.a ≫ G.map (h.hom ≫ h.inv) = A.a
Tactic: rw [h.eq_inv_comp, ← reassoc_of% w, ← Functor.map_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Algebra (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
G : Comonad.{v₁, u₁} C
X : G.Coalgebra
Y : C
f : G.forget.obj X ⟶ Y
⊢ (fun (g : X ⟶ G.cofree.obj Y) ↦ g.f ≫ G.ε.app Y)
      ((fun (f : G.forget.obj X ⟶ Y) ↦ { f := X.a ≫ G.map f, h := ⋯ : X.Hom (G.cofree.obj Y) }) f) =
    f
have dsimp : (X.a ≫ G.map f) ≫ G.ε.app Y = f
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Algebra (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
G : Comonad.{v₁, u₁} C
X : G.Coalgebra
Y : C
f : G.forget.obj X ⟶ Y
⊢ (X.a ≫ G.map f) ≫ G.ε.app Y = f
have rw : X.a ≫ G.map f ≫ G.ε.app Y = f
Tactic: rw [Category.assoc, G.ε.naturality, Functor.id_map, X.counit_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Algebra (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
G : Comonad.{v₁, u₁} C
X : G.Coalgebra
Y : C
f : G.forget.obj X ⟶ Y
rw : X.a ≫ G.map f ≫ G.ε.app Y = f
⊢ (X.a ≫ G.map f) ≫ G.ε.app Y = f
have rw₁ : X.a ≫ G.ε.app X.A ≫ Functor.map (𝟭 C) f = f
Tactic: rw [Category.assoc, G.ε.naturality, Functor.id_map, X.counit_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Algebra (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
G : Comonad.{v₁, u₁} C
X : G.Coalgebra
Y : C
f : G.forget.obj X ⟶ Y
rw : X.a ≫ G.map f ≫ G.ε.app Y = f
rw₁ : X.a ≫ G.ε.app X.A ≫ Functor.map (𝟭 C) f = f
⊢ (X.a ≫ G.map f) ≫ G.ε.app Y = f
have rw₂ : X.a ≫ G.ε.app X.A ≫ f = f
Tactic: rw [Category.assoc, G.ε.naturality, Functor.id_map, X.counit_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Algebra (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
G : Comonad.{v₁, u₁} C
X : G.Coalgebra
Y : C
f : G.forget.obj X ⟶ Y
rw : X.a ≫ G.map f ≫ G.ε.app Y = f
rw₁ : X.a ≫ G.ε.app X.A ≫ Functor.map (𝟭 C) f = f
rw₂ : X.a ≫ G.ε.app X.A ≫ f = f
⊢ (X.a ≫ G.map f) ≫ G.ε.app Y = f
have rw₃ : f = f
Tactic: rw [Category.assoc, G.ε.naturality, Functor.id_map, X.counit_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Algebra (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
G : Comonad.{v₁, u₁} C
X : G.Coalgebra
Y : C
g : X ⟶ G.cofree.obj Y
⊢ (fun (f : G.forget.obj X ⟶ Y) ↦ { f := X.a ≫ G.map f, h := ⋯ : X.Hom (G.cofree.obj Y) })
      ((fun (g : X ⟶ G.cofree.obj Y) ↦ g.f ≫ G.ε.app Y) g) =
    g
have h : Coalgebra.Hom.f
    ((fun (f : G.forget.obj X ⟶ Y) ↦ { f := X.a ≫ G.map f, h := sorry : X.Hom (G.cofree.obj Y) })
      ((fun (g : X ⟶ G.cofree.obj Y) ↦ g.f ≫ G.ε.app Y) g)) =
  g.f
Tactic: ext1
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Algebra (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
G : Comonad.{v₁, u₁} C
X : G.Coalgebra
Y : C
g : X ⟶ G.cofree.obj Y
⊢ Coalgebra.Hom.f
      ((fun (f : G.forget.obj X ⟶ Y) ↦ { f := X.a ≫ G.map f, h := ⋯ : X.Hom (G.cofree.obj Y) })
        ((fun (g : X ⟶ G.cofree.obj Y) ↦ g.f ≫ G.ε.app Y) g)) =
    g.f
have h : X.a ≫ G.map (g.f ≫ G.ε.app Y) = g.f
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Algebra (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
G : Comonad.{v₁, u₁} C
X : G.Coalgebra
Y : C
g : X ⟶ G.cofree.obj Y
⊢ X.a ≫ G.map (g.f ≫ G.ε.app Y) = g.f
have h : g.f ≫ 𝟙 (G.obj Y) = g.f
Tactic: rw [Functor.map_comp, g.h_assoc, cofree_obj_a, Comonad.right_counit]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Algebra (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
G : Comonad.{v₁, u₁} C
A B : G.Coalgebra
f : A ⟶ B
inst_1 : IsIso f.f
⊢ B.a ≫ G.map (inv f.f) = inv f.f ≫ A.a
have rw : A.a ≫ G.map f.f ≫ G.map (inv f.f) = A.a
Tactic: rw [IsIso.eq_inv_comp f.f, ← f.h_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
T : Monad.{v₁, u₁} C
G : Comonad.{v₁, u₁} C
X_1 Y_1 Z : Monad.{v₁, u₁} C
f : X_1 ⟶ Y_1
g : Y_1 ⟶ Z
X Y : C
h : X ⟶ Y
⊢ X_1.map h ≫ f.app Y ≫ g.app Y = (f.app X ≫ g.app X) ≫ Z.map h
have rw : X_1.map h ≫ f.app Y ≫ g.app Y = f.app X ≫ g.app X ≫ Z.map h
Tactic: rw [assoc, f.1.naturality_assoc, g.1.naturality]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
T : Monad.{v₁, u₁} C
G : Comonad.{v₁, u₁} C
X_1 Y_1 Z : Monad.{v₁, u₁} C
f : X_1 ⟶ Y_1
g : Y_1 ⟶ Z
X Y : C
h : X ⟶ Y
rw : X_1.map h ≫ f.app Y ≫ g.app Y = f.app X ≫ g.app X ≫ Z.map h
⊢ X_1.map h ≫ f.app Y ≫ g.app Y = (f.app X ≫ g.app X) ≫ Z.map h
have rw₁ : f.app X ≫ Y_1.map h ≫ g.app Y = f.app X ≫ g.app X ≫ Z.map h
Tactic: rw [assoc, f.1.naturality_assoc, g.1.naturality]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
T : Monad.{v₁, u₁} C
G : Comonad.{v₁, u₁} C
X_1 Y_1 Z : Monad.{v₁, u₁} C
f : X_1 ⟶ Y_1
g : Y_1 ⟶ Z
X Y : C
h : X ⟶ Y
rw : X_1.map h ≫ f.app Y ≫ g.app Y = f.app X ≫ g.app X ≫ Z.map h
rw₁ : f.app X ≫ Y_1.map h ≫ g.app Y = f.app X ≫ g.app X ≫ Z.map h
⊢ X_1.map h ≫ f.app Y ≫ g.app Y = (f.app X ≫ g.app X) ≫ Z.map h
have rw₂ : f.app X ≫ g.app X ≫ Z.map h = f.app X ≫ g.app X ≫ Z.map h
Tactic: rw [assoc, f.1.naturality_assoc, g.1.naturality]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
T : Monad.{v₁, u₁} C
G X_1 Y_1 Z : Comonad.{v₁, u₁} C
f : X_1 ⟶ Y_1
g : Y_1 ⟶ Z
X Y : C
h : X ⟶ Y
⊢ X_1.map h ≫ f.app Y ≫ g.app Y = (f.app X ≫ g.app X) ≫ Z.map h
have rw : X_1.map h ≫ f.app Y ≫ g.app Y = f.app X ≫ g.app X ≫ Z.map h
Tactic: rw [assoc, f.1.naturality_assoc, g.1.naturality]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
T : Monad.{v₁, u₁} C
G X_1 Y_1 Z : Comonad.{v₁, u₁} C
f : X_1 ⟶ Y_1
g : Y_1 ⟶ Z
X Y : C
h : X ⟶ Y
rw : X_1.map h ≫ f.app Y ≫ g.app Y = f.app X ≫ g.app X ≫ Z.map h
⊢ X_1.map h ≫ f.app Y ≫ g.app Y = (f.app X ≫ g.app X) ≫ Z.map h
have rw₁ : f.app X ≫ Y_1.map h ≫ g.app Y = f.app X ≫ g.app X ≫ Z.map h
Tactic: rw [assoc, f.1.naturality_assoc, g.1.naturality]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
T : Monad.{v₁, u₁} C
G X_1 Y_1 Z : Comonad.{v₁, u₁} C
f : X_1 ⟶ Y_1
g : Y_1 ⟶ Z
X Y : C
h : X ⟶ Y
rw : X_1.map h ≫ f.app Y ≫ g.app Y = f.app X ≫ g.app X ≫ Z.map h
rw₁ : f.app X ≫ Y_1.map h ≫ g.app Y = f.app X ≫ g.app X ≫ Z.map h
⊢ X_1.map h ≫ f.app Y ≫ g.app Y = (f.app X ≫ g.app X) ≫ Z.map h
have rw₂ : f.app X ≫ g.app X ≫ Z.map h = f.app X ≫ g.app X ≫ Z.map h
Tactic: rw [assoc, f.1.naturality_assoc, g.1.naturality]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
T : Monad.{v₁, u₁} C
G : Comonad.{v₁, u₁} C
M N : Monad.{v₁, u₁} C
f : M.toFunctor ≅ N.toFunctor
f_η : ∀ (X : C), M.η.app X ≫ f.hom.app X = N.η.app X
f_μ : ∀ (X : C), M.μ.app X ≫ f.hom.app X = (M.map (f.hom.app X) ≫ f.hom.app (N.obj X)) ≫ N.μ.app X
X : C
⊢ N.μ.app X ≫ f.inv.app X = (N.map (f.inv.app X) ≫ f.inv.app (M.obj X)) ≫ M.μ.app X
have rw : (N.μ.app X ≫ f.inv.app X) ≫ f.hom.app X = ((N.map (f.inv.app X) ≫ f.inv.app (M.obj X)) ≫ M.μ.app X) ≫ f.hom.app X
Tactic: rw [← NatIso.cancel_natIso_hom_right f]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
T : Monad.{v₁, u₁} C
G : Comonad.{v₁, u₁} C
M N : Monad.{v₁, u₁} C
f : M.toFunctor ≅ N.toFunctor
f_η : ∀ (X : C), M.η.app X ≫ f.hom.app X = N.η.app X
f_μ : ∀ (X : C), M.μ.app X ≫ f.hom.app X = (M.map (f.hom.app X) ≫ f.hom.app (N.obj X)) ≫ N.μ.app X
X : C
⊢ (N.μ.app X ≫ f.inv.app X) ≫ f.hom.app X = ((N.map (f.inv.app X) ≫ f.inv.app (M.obj X)) ≫ M.μ.app X) ≫ f.hom.app X
have simp : N.μ.app X = N.map (𝟙 (N.obj X)) ≫ N.μ.app X
Tactic: simp only [NatTrans.naturality, Iso.inv_hom_id_app, assoc, comp_id, f_μ,
          NatTrans.naturality_assoc, Iso.inv_hom_id_app_assoc, ← Functor.map_comp_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
T : Monad.{v₁, u₁} C
G M N : Comonad.{v₁, u₁} C
f : M.toFunctor ≅ N.toFunctor
f_ε : ∀ (X : C), f.hom.app X ≫ N.ε.app X = M.ε.app X
f_δ : ∀ (X : C), f.hom.app X ≫ N.δ.app X = M.δ.app X ≫ f.hom.app (M.obj X) ≫ N.map (f.hom.app X)
X : C
⊢ f.inv.app X ≫ M.δ.app X = N.δ.app X ≫ f.inv.app (N.obj X) ≫ M.map (f.inv.app X)
have rw : f.hom.app X ≫ f.inv.app X ≫ M.δ.app X = f.hom.app X ≫ N.δ.app X ≫ f.inv.app (N.obj X) ≫ M.map (f.inv.app X)
Tactic: rw [← NatIso.cancel_natIso_hom_left f]