awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Limits (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D_1 : Type u₂
inst_1 : Category.{v₂, u₂} D_1
J : Type u
inst_2 : Category.{v, u} J
T : Comonad.{v₁, u₁} C
D : J ⥤ T.Coalgebra
c : Cone (D ⋙ T.forget)
t : IsLimit c
inst_3 : PreservesLimit (D ⋙ T.forget) T.toFunctor
inst_4 : PreservesLimit ((D ⋙ T.forget) ⋙ T.toFunctor) T.toFunctor
inst_5 : PreservesColimit ((D ⋙ T.forget) ⋙ T.toFunctor) T.toFunctor
⊢ lambda c t ≫ T.δ.app c.pt = lambda c t ≫ T.map (lambda c t)
have refine : ∀ (j : J),
  (lambda c t ≫ T.δ.app c.pt) ≫ (T.mapCone (T.mapCone c)).π.app j =
    (lambda c t ≫ T.map (lambda c t)) ≫ (T.mapCone (T.mapCone c)).π.app j
Tactic: refine (isLimitOfPreserves _ (isLimitOfPreserves _ t)).hom_ext fun j => ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Limits (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D_1 : Type u₂
inst_1 : Category.{v₂, u₂} D_1
J : Type u
inst_2 : Category.{v, u} J
T : Comonad.{v₁, u₁} C
D : J ⥤ T.Coalgebra
c : Cone (D ⋙ T.forget)
t : IsLimit c
inst_3 : PreservesLimit (D ⋙ T.forget) T.toFunctor
inst_4 : PreservesLimit ((D ⋙ T.forget) ⋙ T.toFunctor) T.toFunctor
inst_5 : PreservesColimit ((D ⋙ T.forget) ⋙ T.toFunctor) T.toFunctor
j : J
⊢ (lambda c t ≫ T.δ.app c.pt) ≫ (T.mapCone (T.mapCone c)).π.app j =
    (lambda c t ≫ T.map (lambda c t)) ≫ (T.mapCone (T.mapCone c)).π.app j
have rw : (c.π.app j ≫ (D.obj j).a) ≫ T.δ.app ((D ⋙ T.forget).obj j) = lambda c t ≫ T.map (c.π.app j) ≫ T.map (D.obj j).a
Tactic: rw [Functor.mapCone_π_app, Functor.mapCone_π_app, assoc,
      ← show _ = _ ≫ T.map (T.map _) from T.δ.naturality _, assoc, ← Functor.map_comp, commuting,
      Functor.map_comp, ← assoc, commuting]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Limits (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D_1 : Type u₂
inst_1 : Category.{v₂, u₂} D_1
J : Type u
inst_2 : Category.{v, u} J
T : Comonad.{v₁, u₁} C
D : J ⥤ T.Coalgebra
c : Cone (D ⋙ T.forget)
t : IsLimit c
inst_3 : PreservesLimit (D ⋙ T.forget) T.toFunctor
inst_4 : PreservesLimit ((D ⋙ T.forget) ⋙ T.toFunctor) T.toFunctor
inst_5 : PreservesColimit ((D ⋙ T.forget) ⋙ T.toFunctor) T.toFunctor
j : J
⊢ (c.π.app j ≫ (D.obj j).a) ≫ T.δ.app ((D ⋙ T.forget).obj j) = lambda c t ≫ T.map (c.π.app j) ≫ T.map (D.obj j).a
have simp : c.π.app j ≫ (D.obj j).a ≫ T.δ.app (D.obj j).A = lambda c t ≫ T.map (c.π.app j) ≫ T.map (D.obj j).a
Tactic: simp only [Functor.comp_obj, forget_obj, Functor.const_obj_obj, assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Limits (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D_1 : Type u₂
inst_1 : Category.{v₂, u₂} D_1
J : Type u
inst_2 : Category.{v, u} J
T : Comonad.{v₁, u₁} C
D : J ⥤ T.Coalgebra
c : Cone (D ⋙ T.forget)
t : IsLimit c
inst_3 : PreservesLimit (D ⋙ T.forget) T.toFunctor
inst_4 : PreservesLimit ((D ⋙ T.forget) ⋙ T.toFunctor) T.toFunctor
inst_5 : PreservesColimit ((D ⋙ T.forget) ⋙ T.toFunctor) T.toFunctor
j : J
⊢ c.π.app j ≫ (D.obj j).a ≫ T.δ.app (D.obj j).A = lambda c t ≫ T.map (c.π.app j) ≫ T.map (D.obj j).a
have rw : c.π.app j ≫ (D.obj j).a ≫ T.map (D.obj j).a = lambda c t ≫ T.map (c.π.app j) ≫ T.map (D.obj j).a
Tactic: rw [(D.obj j).coassoc, ← assoc, ← assoc, commuting]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Limits (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D_1 : Type u₂
inst_1 : Category.{v₂, u₂} D_1
J : Type u
inst_2 : Category.{v, u} J
T : Comonad.{v₁, u₁} C
D : J ⥤ T.Coalgebra
c : Cone (D ⋙ T.forget)
t : IsLimit c
inst_3 : PreservesLimit (D ⋙ T.forget) T.toFunctor
inst_4 : PreservesLimit ((D ⋙ T.forget) ⋙ T.toFunctor) T.toFunctor
inst_5 : PreservesColimit ((D ⋙ T.forget) ⋙ T.toFunctor) T.toFunctor
j : J
rw : c.π.app j ≫ (D.obj j).a ≫ T.map (D.obj j).a = lambda c t ≫ T.map (c.π.app j) ≫ T.map (D.obj j).a
⊢ c.π.app j ≫ (D.obj j).a ≫ T.δ.app (D.obj j).A = lambda c t ≫ T.map (c.π.app j) ≫ T.map (D.obj j).a
have rw₁ : (c.π.app j ≫ (D.obj j).a) ≫ T.map (D.obj j).a = lambda c t ≫ T.map (c.π.app j) ≫ T.map (D.obj j).a
Tactic: rw [(D.obj j).coassoc, ← assoc, ← assoc, commuting]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Limits (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D_1 : Type u₂
inst_1 : Category.{v₂, u₂} D_1
J : Type u
inst_2 : Category.{v, u} J
T : Comonad.{v₁, u₁} C
D : J ⥤ T.Coalgebra
c : Cone (D ⋙ T.forget)
t : IsLimit c
inst_3 : PreservesLimit (D ⋙ T.forget) T.toFunctor
inst_4 : PreservesLimit ((D ⋙ T.forget) ⋙ T.toFunctor) T.toFunctor
inst_5 : PreservesColimit ((D ⋙ T.forget) ⋙ T.toFunctor) T.toFunctor
j : J
rw : c.π.app j ≫ (D.obj j).a ≫ T.map (D.obj j).a = lambda c t ≫ T.map (c.π.app j) ≫ T.map (D.obj j).a
rw₁ : (c.π.app j ≫ (D.obj j).a) ≫ T.map (D.obj j).a = lambda c t ≫ T.map (c.π.app j) ≫ T.map (D.obj j).a
⊢ c.π.app j ≫ (D.obj j).a ≫ T.δ.app (D.obj j).A = lambda c t ≫ T.map (c.π.app j) ≫ T.map (D.obj j).a
have rw₂ : (c.π.app j ≫ (D.obj j).a) ≫ T.map (D.obj j).a = (lambda c t ≫ T.map (c.π.app j)) ≫ T.map (D.obj j).a
Tactic: rw [(D.obj j).coassoc, ← assoc, ← assoc, commuting]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Limits (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D_1 : Type u₂
inst_1 : Category.{v₂, u₂} D_1
J : Type u
inst_2 : Category.{v, u} J
T : Comonad.{v₁, u₁} C
D : J ⥤ T.Coalgebra
c : Cone (D ⋙ T.forget)
t : IsLimit c
inst_3 : PreservesLimit (D ⋙ T.forget) T.toFunctor
inst_4 : PreservesLimit ((D ⋙ T.forget) ⋙ T.toFunctor) T.toFunctor
inst_5 : PreservesColimit ((D ⋙ T.forget) ⋙ T.toFunctor) T.toFunctor
j : J
rw : c.π.app j ≫ (D.obj j).a ≫ T.map (D.obj j).a = lambda c t ≫ T.map (c.π.app j) ≫ T.map (D.obj j).a
rw₁ : (c.π.app j ≫ (D.obj j).a) ≫ T.map (D.obj j).a = lambda c t ≫ T.map (c.π.app j) ≫ T.map (D.obj j).a
rw₂ : (c.π.app j ≫ (D.obj j).a) ≫ T.map (D.obj j).a = (lambda c t ≫ T.map (c.π.app j)) ≫ T.map (D.obj j).a
⊢ c.π.app j ≫ (D.obj j).a ≫ T.δ.app (D.obj j).A = lambda c t ≫ T.map (c.π.app j) ≫ T.map (D.obj j).a
have rw₃ : (c.π.app j ≫ (D.obj j).a) ≫ T.map (D.obj j).a = (c.π.app j ≫ (D.obj j).a) ≫ T.map (D.obj j).a
Tactic: rw [(D.obj j).coassoc, ← assoc, ← assoc, commuting]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Limits (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D_1 : Type u₂
inst_1 : Category.{v₂, u₂} D_1
J : Type u
inst_2 : Category.{v, u} J
T : Comonad.{v₁, u₁} C
D : J ⥤ T.Coalgebra
c : Cone (D ⋙ T.forget)
t : IsLimit c
inst_3 : PreservesLimit (D ⋙ T.forget) T.toFunctor
inst_4 : PreservesLimit ((D ⋙ T.forget) ⋙ T.toFunctor) T.toFunctor
inst_5 : PreservesColimit ((D ⋙ T.forget) ⋙ T.toFunctor) T.toFunctor
A B : J
f : A ⟶ B
⊢ Eq (α := obj (obj (const J) (conePoint c t)) A ⟶ D.obj B)
    (map (obj (const J) (conePoint c t)) f ≫ { f := c.π.app B, h := ⋯ }) ({ f := c.π.app A, h := ⋯ } ≫ D.map f)
have h : Eq (α := (obj (obj (const J) (conePoint c t)) A).A ⟶ (D.obj B).A)
  (Coalgebra.Hom.f (map (obj (const J) (conePoint c t)) f ≫ { f := c.π.app B, h := sorry }))
  (Coalgebra.Hom.f ({ f := c.π.app A, h := sorry } ≫ D.map f))
Tactic: ext1
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Limits (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D_1 : Type u₂
inst_1 : Category.{v₂, u₂} D_1
J : Type u
inst_2 : Category.{v, u} J
T : Comonad.{v₁, u₁} C
D : J ⥤ T.Coalgebra
c : Cone (D ⋙ T.forget)
t : IsLimit c
inst_3 : PreservesLimit (D ⋙ T.forget) T.toFunctor
inst_4 : PreservesLimit ((D ⋙ T.forget) ⋙ T.toFunctor) T.toFunctor
inst_5 : PreservesColimit ((D ⋙ T.forget) ⋙ T.toFunctor) T.toFunctor
A B : J
f : A ⟶ B
⊢ Eq (α := (obj (obj (const J) (conePoint c t)) A).A ⟶ (D.obj B).A)
    (Coalgebra.Hom.f (map (obj (const J) (conePoint c t)) f ≫ { f := c.π.app B, h := ⋯ }))
    (Coalgebra.Hom.f ({ f := c.π.app A, h := ⋯ } ≫ D.map f))
have h : 𝟙 c.pt ≫ c.π.app B = c.π.app A ≫ (D.map f).f
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Limits (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D_1 : Type u₂
inst_1 : Category.{v₂, u₂} D_1
J : Type u
inst_2 : Category.{v, u} J
T : Comonad.{v₁, u₁} C
D : J ⥤ T.Coalgebra
c : Cone (D ⋙ T.forget)
t : IsLimit c
inst_3 : PreservesLimit (D ⋙ T.forget) T.toFunctor
inst_4 : PreservesLimit ((D ⋙ T.forget) ⋙ T.toFunctor) T.toFunctor
inst_5 : PreservesColimit ((D ⋙ T.forget) ⋙ T.toFunctor) T.toFunctor
A B : J
f : A ⟶ B
⊢ 𝟙 c.pt ≫ c.π.app B = c.π.app A ≫ (D.map f).f
have h : c.π.app A ≫ (D ⋙ T.forget).map f = c.π.app A ≫ (D.map f).f
Tactic: rw [id_comp, ← c.w]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Limits (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D_1 : Type u₂
inst_1 : Category.{v₂, u₂} D_1
J : Type u
inst_2 : Category.{v, u} J
T : Comonad.{v₁, u₁} C
D : J ⥤ T.Coalgebra
c : Cone (D ⋙ T.forget)
t : IsLimit c
inst_3 : PreservesLimit (D ⋙ T.forget) T.toFunctor
inst_4 : PreservesLimit ((D ⋙ T.forget) ⋙ T.toFunctor) T.toFunctor
inst_5 : PreservesColimit ((D ⋙ T.forget) ⋙ T.toFunctor) T.toFunctor
s : Cone D
j : J
⊢ (s.pt.a ≫ T.map (t.lift (T.forget.mapCone s))) ≫ (T.mapCone c).π.app j =
    (t.lift (T.forget.mapCone s) ≫ (liftedCone c t).pt.a) ≫ (T.mapCone c).π.app j
have dsimp : (s.pt.a ≫ T.map (t.lift (T.forget.mapCone s))) ≫ T.map (c.π.app j) =
  (t.lift (T.forget.mapCone s) ≫ lambda c t) ≫ T.map (c.π.app j)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Limits (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D_1 : Type u₂
inst_1 : Category.{v₂, u₂} D_1
J : Type u
inst_2 : Category.{v, u} J
T : Comonad.{v₁, u₁} C
D : J ⥤ T.Coalgebra
c : Cone (D ⋙ T.forget)
t : IsLimit c
inst_3 : PreservesLimit (D ⋙ T.forget) T.toFunctor
inst_4 : PreservesLimit ((D ⋙ T.forget) ⋙ T.toFunctor) T.toFunctor
inst_5 : PreservesColimit ((D ⋙ T.forget) ⋙ T.toFunctor) T.toFunctor
s : Cone D
j : J
⊢ (s.pt.a ≫ T.map (t.lift (T.forget.mapCone s))) ≫ T.map (c.π.app j) =
    (t.lift (T.forget.mapCone s) ≫ lambda c t) ≫ T.map (c.π.app j)
have rw : s.pt.a ≫ T.map ((T.forget.mapCone s).π.app j) = (T.forget.mapCone s).π.app j ≫ (D.obj j).a
Tactic: rw [Category.assoc, ← t.fac, Category.assoc, t.fac, commuting, ← assoc, ← assoc, t.fac,
            assoc, ← Functor.map_comp, t.fac]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Limits (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D_1 : Type u₂
inst_1 : Category.{v₂, u₂} D_1
J_1 : Type u
inst_2 : Category.{v, u} J_1
T : Comonad.{v₁, u₁} C
D : J_1 ⥤ T.Coalgebra
c : Cone (D ⋙ T.forget)
t : IsLimit c
inst_3 : PreservesLimit (D ⋙ T.forget) T.toFunctor
inst_4 : PreservesLimit ((D ⋙ T.forget) ⋙ T.toFunctor) T.toFunctor
inst_5 : PreservesColimit ((D ⋙ T.forget) ⋙ T.toFunctor) T.toFunctor
s : Cone D
m : s.pt ⟶ (liftedCone c t).pt
J : ∀ (j : J_1), m ≫ (liftedCone c t).π.app j = s.π.app j
⊢ m = { f := t.lift (T.forget.mapCone s), h := ⋯ }
have h : m.f = Coalgebra.Hom.f { f := t.lift (T.forget.mapCone s), h := sorry }
Tactic: ext1
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Limits (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D_1 : Type u₂
inst_1 : Category.{v₂, u₂} D_1
J_1 : Type u
inst_2 : Category.{v, u} J_1
T : Comonad.{v₁, u₁} C
D : J_1 ⥤ T.Coalgebra
c : Cone (D ⋙ T.forget)
t : IsLimit c
inst_3 : PreservesLimit (D ⋙ T.forget) T.toFunctor
inst_4 : PreservesLimit ((D ⋙ T.forget) ⋙ T.toFunctor) T.toFunctor
inst_5 : PreservesColimit ((D ⋙ T.forget) ⋙ T.toFunctor) T.toFunctor
s : Cone D
m : s.pt ⟶ (liftedCone c t).pt
J : ∀ (j : J_1), m ≫ (liftedCone c t).π.app j = s.π.app j
⊢ m.f = Coalgebra.Hom.f { f := t.lift (T.forget.mapCone s), h := ⋯ }
have h : ∀ (j : J_1), m.f ≫ c.π.app j = Coalgebra.Hom.f { f := t.lift (T.forget.mapCone s), h := sorry } ≫ c.π.app j
Tactic: apply t.hom_ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Limits (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D_1 : Type u₂
inst_1 : Category.{v₂, u₂} D_1
J : Type u
inst_2 : Category.{v, u} J
T : Comonad.{v₁, u₁} C
D : J ⥤ T.Coalgebra
inst_3 : PreservesLimit (D ⋙ T.forget) T.toFunctor
inst_4 : PreservesLimit ((D ⋙ T.forget) ⋙ T.toFunctor) T.toFunctor
c : Cone (D ⋙ T.forget)
t : IsLimit c
A B : J
f : A ⟶ B
⊢ Eq (α := obj (obj (const J) (conePoint c t)) A ⟶ D.obj B)
    (map (obj (const J) (conePoint c t)) f ≫ { f := c.π.app B, h := ⋯ }) ({ f := c.π.app A, h := ⋯ } ≫ D.map f)
have h : Eq (α := (obj (obj (const J) (conePoint c t)) A).A ⟶ (D.obj B).A)
  (Coalgebra.Hom.f (map (obj (const J) (conePoint c t)) f ≫ { f := c.π.app B, h := sorry }))
  (Coalgebra.Hom.f ({ f := c.π.app A, h := sorry } ≫ D.map f))
Tactic: ext1
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Limits (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
J : Type u
inst_2 : Category.{v, u} J
R : Functor.{v₂, v₁, u₂, u₁} D C
inst_3 : Coreflective R
inst_4 : HasLimitsOfShape.{v, u, v₁, u₁} J C
F : Functor.{v, v₂, u, u₂} J D
c : Cone ((F ⋙ R) ⋙ comonadicRightAdjoint R) := (comonadicRightAdjoint R).mapCone (limit.cone (F ⋙ R))
this : PreservesLimitsOfShape.{v, u, v₁, v₂, u₁, u₂} J (comonadicRightAdjoint R) := ⋯
t : IsLimit c := isLimitOfPreserves (comonadicRightAdjoint R) (limit.isLimit (F ⋙ R))
⊢ HasLimit F
have apply : (F ⋙ R) ⋙ comonadicRightAdjoint R ≅ F
Tactic: apply HasLimit.mk ⟨_, (IsLimit.postcomposeHomEquiv _ _).symm t⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Limits (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
R : Functor.{v₂, v₁, u₂, u₁} D C
inst_2 : Coreflective R
K : Functor.{v, v₁, v, u₁} (Discrete PEmpty.{v + 1}) C
F : Functor.{v, v₂, v, u₂} (Discrete PEmpty.{v + 1}) D := empty D
⊢ PreservesColimit (F ⋙ R) (comonadicRightAdjoint R)
have preserves : ∀ {c : Cocone (F ⋙ R)} (hc : IsColimit c), Nonempty (IsColimit ((comonadicRightAdjoint R).mapCocone c))
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Limits (hypothesis)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
R : Functor.{v₂, v₁, u₂, u₁} D C
inst_2 : Coreflective R
K : Functor.{v, v₁, v, u₁} (Discrete PEmpty.{v + 1}) C
F : Functor.{v, v₂, v, u₂} (Discrete PEmpty.{v + 1}) D := empty D
c : Cocone (F ⋙ R)
h : IsColimit c
⊢ Nonempty (IsColimit ((comonadicRightAdjoint R).mapCocone c))
have this : HasColimit (F ⋙ R)
Tactic: haveI : HasColimit (F ⋙ R) := ⟨⟨⟨c, h⟩⟩⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Limits (hypothesis)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
R : Functor.{v₂, v₁, u₂, u₁} D C
inst_2 : Coreflective R
K : Functor.{v, v₁, v, u₁} (Discrete PEmpty.{v + 1}) C
F : Functor.{v, v₂, v, u₂} (Discrete PEmpty.{v + 1}) D := empty D
c : Cocone (F ⋙ R)
h : IsColimit c
this : HasColimit (F ⋙ R)
⊢ Nonempty (IsColimit ((comonadicRightAdjoint R).mapCocone c))
have this₁ : HasColimit F
Tactic: haveI : HasColimit F := hasColimit_of_coreflective F R
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Limits (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
R : Functor.{v₂, v₁, u₂, u₁} D C
inst_2 : Coreflective R
K : Functor.{v, v₁, v, u₁} (Discrete PEmpty.{v + 1}) C
F : Functor.{v, v₂, v, u₂} (Discrete PEmpty.{v + 1}) D := empty D
c : Cocone (F ⋙ R)
h : IsColimit c
this_1 : HasColimit (F ⋙ R)
this : HasColimit F
⊢ Nonempty (IsColimit ((comonadicRightAdjoint R).mapCocone c))
have preserves : IsColimit ((comonadicRightAdjoint R).mapCocone c)
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Limits (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
R : Functor.{v₂, v₁, u₂, u₁} D C
inst_2 : Coreflective R
K : Functor.{v, v₁, v, u₁} (Discrete PEmpty.{v + 1}) C
F : Functor.{v, v₂, v, u₂} (Discrete PEmpty.{v + 1}) D := empty D
c : Cocone (F ⋙ R)
h : IsColimit c
this_1 : HasColimit (F ⋙ R)
this : HasColimit F
⊢ IsColimit ((comonadicRightAdjoint R).mapCocone c)
have preserves : (colimit.cocone F).pt ≅ ((comonadicRightAdjoint R).mapCocone c).pt
Tactic: apply isColimitChangeEmptyCocone D (colimit.isColimit F)
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Limits (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
R : Functor.{v₂, v₁, u₂, u₁} D C
inst_2 : Coreflective R
K : Functor.{v, v₁, v, u₁} (Discrete PEmpty.{v + 1}) C
F : Functor.{v, v₂, v, u₂} (Discrete PEmpty.{v + 1}) D := empty D
c : Cocone (F ⋙ R)
h : IsColimit c
this_1 : HasColimit (F ⋙ R)
this : HasColimit F
⊢ (colimit.cocone F).pt ≅ ((comonadicRightAdjoint R).mapCocone c).pt
have preserves : (R ⋙ comonadicRightAdjoint R).obj (colimit.cocone F).1 ≅ ((comonadicRightAdjoint R).mapCocone c).pt
Tactic: apply (asIso ((comonadicAdjunction R).unit.app _)).trans
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Limits (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
R : Functor.{v₂, v₁, u₂, u₁} D C
inst_2 : Coreflective R
K : Functor.{v, v₁, v, u₁} (Discrete PEmpty.{v + 1}) C
F : Functor.{v, v₂, v, u₂} (Discrete PEmpty.{v + 1}) D := empty D
c : Cocone (F ⋙ R)
h : IsColimit c
this_1 : HasColimit (F ⋙ R)
this : HasColimit F
⊢ (R ⋙ comonadicRightAdjoint R).obj (colimit.cocone F).1 ≅ ((comonadicRightAdjoint R).mapCocone c).pt
have preserves : R.obj (colimit.cocone F).1 ≅ c.pt
Tactic: apply (comonadicRightAdjoint R).mapIso
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Monadicity (goal)
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₁, u₂} D
G : Functor.{v₁, v₁, u₂, u₁} D C
F : Functor.{v₁, v₁, u₁, u₂} C D
adj : F ⊣ G
A : adj.toMonad.Algebra
⊢ IsReflexivePair (F.map A.a) (adj.counit.app (F.obj A.A))
have apply : F.map (adj.unit.app A.A) ≫ F.map A.a = 𝟙 (F.obj (Functor.obj.{v₁, v₁, u₁, u₁} (𝟭 C) A.A))
Tactic: apply IsReflexivePair.mk' (F.map (adj.unit.app _)) _ _
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Monadicity (goal)
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₁, u₂} D
G : Functor.{v₁, v₁, u₂, u₁} D C
F : Functor.{v₁, v₁, u₁, u₂} C D
adj : F ⊣ G
A : adj.toMonad.Algebra
apply : F.map (adj.unit.app A.A) ≫ F.map A.a = 𝟙 (F.obj (Functor.obj.{v₁, v₁, u₁, u₁} (𝟭 C) A.A))
⊢ IsReflexivePair (F.map A.a) (adj.counit.app (F.obj A.A))
have apply₁ : F.map (adj.unit.app A.A) ≫ adj.counit.app (F.obj A.A) = 𝟙 (F.obj (Functor.obj.{v₁, v₁, u₁, u₁} (𝟭 C) A.A))
Tactic: apply IsReflexivePair.mk' (F.map (adj.unit.app _)) _ _
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Monadicity (goal)
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₁, u₂} D
G : Functor.{v₁, v₁, u₂, u₁} D C
F : Functor.{v₁, v₁, u₁, u₂} C D
adj : F ⊣ G
A : adj.toMonad.Algebra
⊢ F.map (adj.unit.app A.A) ≫ F.map A.a = 𝟙 (F.obj (Functor.obj.{v₁, v₁, u₁, u₁} (𝟭 C) A.A))
have rw : F.map (adj.unit.app A.A ≫ A.a) = F.map (𝟙 (Functor.obj.{v₁, v₁, u₁, u₁} (𝟭 C) A.A))
Tactic: rw [← F.map_comp, ← F.map_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Monadicity (goal)
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₁, u₂} D
G : Functor.{v₁, v₁, u₂, u₁} D C
F : Functor.{v₁, v₁, u₁, u₂} C D
adj : F ⊣ G
A : adj.toMonad.Algebra
⊢ F.map (adj.unit.app A.A) ≫ adj.counit.app (F.obj A.A) = 𝟙 (F.obj (Functor.obj.{v₁, v₁, u₁, u₁} (𝟭 C) A.A))
have dsimp : F.map (adj.unit.app A.A) ≫ adj.counit.app (F.obj A.A) = 𝟙 (F.obj A.A)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Monadicity (goal)
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₁, u₂} D
G : Functor.{v₁, v₁, u₂, u₁} D C
F : Functor.{v₁, v₁, u₁, u₂} C D
adj : F ⊣ G
A : adj.toMonad.Algebra
⊢ F.map (adj.unit.app A.A) ≫ adj.counit.app (F.obj A.A) = 𝟙 (F.obj A.A)
have rw : Eq.{v₁ + 1} (α := F.obj A.A ⟶ F.obj A.A) (𝟙 (F.obj A.A)) (𝟙 (F.obj A.A))
Tactic: rw [adj.left_triangle_components]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Monadicity (goal)
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₁, u₂} D
G : Functor.{v₁, v₁, u₂, u₁} D C
F : Functor.{v₁, v₁, u₁, u₂} C D
adj : F ⊣ G
A : adj.toMonad.Algebra
B : D
inst_2 : HasCoequalizer (F.map A.a) (adj.counit.app (F.obj A.A))
⊢ { f : F.obj A.A ⟶ B // F.map A.a ≫ f = adj.counit.app (F.obj A.A) ≫ f } ≃
    { g : A.A ⟶ G.obj B // G.map (F.map g) ≫ G.map (adj.counit.app B) = A.a ≫ g }
have refine : ∀ (a : F.obj A.A ⟶ B),
  F.map A.a ≫ a = adj.counit.app (F.obj A.A) ≫ a ↔
    G.map (F.map ((adj.homEquiv A.A B : (a : F.obj A.A ⟶ B) → A.A ⟶ G.obj B) a)) ≫ G.map (adj.counit.app B) =
      A.a ≫ (adj.homEquiv A.A B : (a : F.obj A.A ⟶ B) → A.A ⟶ G.obj B) a
Tactic: refine (adj.homEquiv _ _).subtypeEquiv ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Monadicity (goal)
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₁, u₂} D
G : Functor.{v₁, v₁, u₂, u₁} D C
F : Functor.{v₁, v₁, u₁, u₂} C D
adj : F ⊣ G
A : adj.toMonad.Algebra
B : D
inst_2 : HasCoequalizer (F.map A.a) (adj.counit.app (F.obj A.A))
f : F.obj A.A ⟶ B
⊢ F.map A.a ≫ f = adj.counit.app (F.obj A.A) ≫ f ↔
    G.map (F.map ((adj.homEquiv A.A B : (a : F.obj A.A ⟶ B) → A.A ⟶ G.obj B) f)) ≫ G.map (adj.counit.app B) =
      A.a ≫ (adj.homEquiv A.A B : (a : F.obj A.A ⟶ B) → A.A ⟶ G.obj B) f
have rw : A.a ≫ adj.unit.app A.A ≫ G.map f = adj.unit.app (adj.toMonad.obj A.A) ≫ G.map (adj.counit.app (F.obj A.A)) ≫ G.map f ↔
  G.map (F.map (adj.unit.app A.A ≫ G.map f)) ≫ G.map (adj.counit.app B) = A.a ≫ adj.unit.app A.A ≫ G.map f
Tactic: rw [← (adj.homEquiv _ _).injective.eq_iff, Adjunction.homEquiv_naturality_left,
        adj.homEquiv_unit, adj.homEquiv_unit, G.map_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Monadicity (goal)
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₁, u₂} D
G : Functor.{v₁, v₁, u₂, u₁} D C
F : Functor.{v₁, v₁, u₁, u₂} C D
adj : F ⊣ G
A : adj.toMonad.Algebra
B : D
inst_2 : HasCoequalizer (F.map A.a) (adj.counit.app (F.obj A.A))
f : F.obj A.A ⟶ B
⊢ A.a ≫ adj.unit.app A.A ≫ G.map f = adj.unit.app (adj.toMonad.obj A.A) ≫ G.map (adj.counit.app (F.obj A.A)) ≫ G.map f ↔
    G.map (F.map (adj.unit.app A.A ≫ G.map f)) ≫ G.map (adj.counit.app B) = A.a ≫ adj.unit.app A.A ≫ G.map f
have dsimp : A.a ≫ adj.unit.app A.A ≫ G.map f = adj.unit.app (G.obj (F.obj A.A)) ≫ G.map (adj.counit.app (F.obj A.A)) ≫ G.map f ↔
  G.map (F.map (adj.unit.app A.A ≫ G.map f)) ≫ G.map (adj.counit.app B) = A.a ≫ adj.unit.app A.A ≫ G.map f
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Monadicity (goal)
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₁, u₂} D
G : Functor.{v₁, v₁, u₂, u₁} D C
F : Functor.{v₁, v₁, u₁, u₂} C D
adj : F ⊣ G
A : adj.toMonad.Algebra
B : D
inst_2 : HasCoequalizer (F.map A.a) (adj.counit.app (F.obj A.A))
f : F.obj A.A ⟶ B
⊢ A.a ≫ adj.unit.app A.A ≫ G.map f = adj.unit.app (G.obj (F.obj A.A)) ≫ G.map (adj.counit.app (F.obj A.A)) ≫ G.map f ↔
    G.map (F.map (adj.unit.app A.A ≫ G.map f)) ≫ G.map (adj.counit.app B) = A.a ≫ adj.unit.app A.A ≫ G.map f
have rw : A.a ≫ adj.unit.app A.A ≫ G.map f = G.map f ↔ G.map f = A.a ≫ adj.unit.app A.A ≫ G.map f
Tactic: rw [adj.right_triangle_components_assoc, ← G.map_comp, F.map_comp, Category.assoc,
        adj.counit_naturality, adj.left_triangle_components_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Monadicity (goal)
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₁, u₂} D
G : Functor.{v₁, v₁, u₂, u₁} D C
F : Functor.{v₁, v₁, u₁, u₂} C D
adj : F ⊣ G
inst_2 : ∀ (A : adj.toMonad.Algebra), HasCoequalizer (F.map A.a) (adj.counit.app (F.obj A.A))
⊢ adj.toMonad.Algebra ⥤ D
have refine_1 : (A : adj.toMonad.Algebra) →
  (B : D) → ((fun (A : adj.toMonad.Algebra) ↦ comparisonLeftAdjointObj adj A) A ⟶ B) ≃ (A ⟶ (comparison adj).obj B)
Tactic: refine
    Adjunction.leftAdjointOfEquiv (G := comparison adj)
      (F_obj := fun A => comparisonLeftAdjointObj adj A) (fun A B => ?_) ?_