awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Comonadicity (goal)
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₁, u₂} D
F : Functor.{v₁, v₁, u₁, u₂} C D
G : Functor.{v₁, v₁, u₂, u₁} D C
adj : F ⊣ G
inst_2 : HasEqualizerOfIsCosplitPair F
inst_3 : PreservesLimitOfIsCosplitPair F
inst_4 : ReflectsLimitOfIsCosplitPair F
X : adj.toComonad.Coalgebra
⊢ IsIso (X := ((rightAdjointComparison adj ⋙ comparison adj).obj X).A)
    (Coalgebra.Hom.f (NatTrans.app (counit (comparisonAdjunction adj)) X))
have rw : IsIso (X := ((rightAdjointComparison adj ⋙ comparison adj).obj X).A)
  ((beckEqualizer X).lift (counitFork X) : (counitFork X).pt ⟶ (beckFork X).pt)
Tactic: rw [comparisonAdjunction_counit_f]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Comonadicity (goal)
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₁, u₂} D
F : Functor.{v₁, v₁, u₁, u₂} C D
G : Functor.{v₁, v₁, u₂, u₁} D C
adj : F ⊣ G
inst_2 : HasEqualizerOfIsCosplitPair F
inst_3 : PreservesLimitOfIsCosplitPair F
inst_4 : ReflectsLimitOfIsCosplitPair F
X : adj.toComonad.Coalgebra
⊢ IsIso (X := ((rightAdjointComparison adj ⋙ comparison adj).obj X).A)
    ((beckEqualizer X).lift (counitFork X) : (counitFork X).pt ⟶ (beckFork X).pt)
have this : IsIso (X := (counitFork X).pt) (Iso.inv ((beckEqualizer X).conePointUniqueUpToIso (counitLimitOfPreservesEqualizer X)))
Tactic: change
          IsIso
            (IsLimit.conePointUniqueUpToIso (beckEqualizer X)
                (counitLimitOfPreservesEqualizer X)).inv
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Comonadicity (hypothesis)
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₁, u₂} D
F : Functor.{v₁, v₁, u₁, u₂} C D
G : Functor.{v₁, v₁, u₂, u₁} D C
adj : F ⊣ G
inst_2 : HasEqualizerOfIsCosplitPair F
inst_3 : PreservesLimitOfIsCosplitPair F
inst_4 : ReflectsLimitOfIsCosplitPair F
⊢ (comparison adj).IsEquivalence
have this : ∀ (X : adj.toComonad.Coalgebra),
  IsIso (X := (rightAdjointComparison adj ⋙ comparison adj).obj X) (NatTrans.app (counit (comparisonAdjunction adj)) X)
Tactic: have : ∀ (X : Coalgebra adj.toComonad), IsIso ((comparisonAdjunction adj).counit.app X) := by
      intro X
      apply @isIso_of_reflects_iso _ _ _ _ _ _ _ (Comonad.forget adj.toComonad) ?_ _
      · change IsIso ((comparisonAdjunction adj).counit.app X).f
        rw [comparisonAdjunction_counit_f]
        change
          IsIso
            (IsLimit.conePointUniqueUpToIso (beckEqualizer X)
                (counitLimitOfPreservesEqualizer X)).inv
        exact (IsLimit.conePointUniqueUpToIso _ _).isIso_inv
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Comonadicity (goal)
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₁, u₂} D
F : Functor.{v₁, v₁, u₁, u₂} C D
G : Functor.{v₁, v₁, u₂, u₁} D C
adj : F ⊣ G
inst_2 : HasEqualizerOfIsCosplitPair F
inst_3 : PreservesLimitOfIsCosplitPair F
inst_4 : ReflectsLimitOfIsCosplitPair F
this :
  ∀ (X : adj.toComonad.Coalgebra),
    IsIso (X := (rightAdjointComparison adj ⋙ comparison adj).obj X)
      (NatTrans.app (counit (comparisonAdjunction adj)) X)
Y : C
⊢ IsIso (Y := (comparison adj ⋙ rightAdjointComparison adj).obj Y) (NatTrans.app (unit (comparisonAdjunction adj)) Y)
have rw : IsIso (X := Functor.obj.{v₁, v₁, u₁, u₁} (𝟭 C) Y) (Y := (comparison adj ⋙ rightAdjointComparison adj).obj Y)
  (limit.lift (parallelPair (G.map (F.map (adj.unit.app Y))) (adj.unit.app (G.obj (F.obj Y)))) (unitFork adj Y) :
    (unitFork adj Y).pt ⟶ limit (parallelPair (G.map (F.map (adj.unit.app Y))) (adj.unit.app (G.obj (F.obj Y)))))
Tactic: rw [comparisonAdjunction_unit_app]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Comonadicity (goal)
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₁, u₂} D
F : Functor.{v₁, v₁, u₁, u₂} C D
G : Functor.{v₁, v₁, u₂, u₁} D C
adj : F ⊣ G
inst_2 : HasEqualizerOfIsCosplitPair F
inst_3 : PreservesLimitOfIsCosplitPair F
inst_4 : ReflectsLimitOfIsCosplitPair F
this :
  ∀ (X : adj.toComonad.Coalgebra),
    IsIso (X := (rightAdjointComparison adj ⋙ comparison adj).obj X)
      (NatTrans.app (counit (comparisonAdjunction adj)) X)
Y : C
⊢ IsIso (X := Functor.obj.{v₁, v₁, u₁, u₁} (𝟭 C) Y) (Y := (comparison adj ⋙ rightAdjointComparison adj).obj Y)
    (limit.lift (parallelPair (G.map (F.map (adj.unit.app Y))) (adj.unit.app (G.obj (F.obj Y)))) (unitFork adj Y) :
      (unitFork adj Y).pt ⟶ limit (parallelPair (G.map (F.map (adj.unit.app Y))) (adj.unit.app (G.obj (F.obj Y)))))
have change : IsIso (Y := (limit.cone (parallelPair (G.map (F.map (adj.unit.app Y))) (adj.unit.app (G.obj (F.obj Y))))).pt)
  (Iso.inv
    (IsLimit.conePointUniqueUpToIso
      (limit.isLimit (parallelPair (G.map (F.map (adj.unit.app Y))) (adj.unit.app (G.obj (F.obj Y)))))
      (unitEqualizerOfCoreflectsEqualizer adj Y)))
Tactic: change IsIso (IsLimit.conePointUniqueUpToIso _ ?_).inv
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Comonadicity (goal)
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₁, u₂} D
F : Functor.{v₁, v₁, u₁, u₂} C D
G : Functor.{v₁, v₁, u₂, u₁} D C
adj : F ⊣ G
inst_2 : HasEqualizerOfIsCosplitPair F
inst_3 : PreservesLimitOfIsCosplitPair F
inst_4 : ReflectsLimitOfIsCosplitPair F
this :
  ∀ (X : adj.toComonad.Coalgebra),
    IsIso (X := (rightAdjointComparison adj ⋙ comparison adj).obj X)
      (NatTrans.app (counit (comparisonAdjunction adj)) X)
Y : C
change :
  IsIso (Y := (limit.cone (parallelPair (G.map (F.map (adj.unit.app Y))) (adj.unit.app (G.obj (F.obj Y))))).pt)
    (Iso.inv
      (IsLimit.conePointUniqueUpToIso
        (limit.isLimit (parallelPair (G.map (F.map (adj.unit.app Y))) (adj.unit.app (G.obj (F.obj Y)))))
        (unitEqualizerOfCoreflectsEqualizer adj Y)))
⊢ IsIso (X := Functor.obj.{v₁, v₁, u₁, u₁} (𝟭 C) Y) (Y := (comparison adj ⋙ rightAdjointComparison adj).obj Y)
    (limit.lift (parallelPair (G.map (F.map (adj.unit.app Y))) (adj.unit.app (G.obj (F.obj Y)))) (unitFork adj Y) :
      (unitFork adj Y).pt ⟶ limit (parallelPair (G.map (F.map (adj.unit.app Y))) (adj.unit.app (G.obj (F.obj Y)))))
have change₁ : IsLimit (unitFork adj Y)
Tactic: change IsIso (IsLimit.conePointUniqueUpToIso _ ?_).inv
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Comonadicity (goal)
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₁, u₂} D
F : Functor.{v₁, v₁, u₁, u₂} C D
G : Functor.{v₁, v₁, u₂, u₁} D C
adj : F ⊣ G
inst_2 : HasEqualizerOfIsCosplitPair F
inst_3 : PreservesLimitOfIsCosplitPair F
inst_4 : ReflectsLimitOfIsCosplitPair F
this :
  ∀ (X : adj.toComonad.Coalgebra),
    IsIso (X := (rightAdjointComparison adj ⋙ comparison adj).obj X)
      (NatTrans.app (counit (comparisonAdjunction adj)) X)
Y : C
⊢ IsLimit (unitFork adj Y)
have apply : ReflectsLimit (parallelPair (G.map (F.map (adj.unit.app Y))) (adj.unit.app (G.obj (F.obj Y)))) F
Tactic: apply @unitEqualizerOfCoreflectsEqualizer _ _ _ _ _ _ _ _ ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Comonadicity (hypothesis)
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₁, u₂} D
F : Functor.{v₁, v₁, u₁, u₂} C D
G : Functor.{v₁, v₁, u₂, u₁} D C
adj : F ⊣ G
inst_2 : HasEqualizerOfIsCosplitPair F
inst_3 : PreservesLimitOfIsCosplitPair F
inst_4 : ReflectsLimitOfIsCosplitPair F
this :
  ∀ (X : adj.toComonad.Coalgebra),
    IsIso (X := (rightAdjointComparison adj ⋙ comparison adj).obj X)
      (NatTrans.app (counit (comparisonAdjunction adj)) X)
⊢ (comparison adj).IsEquivalence
have this₁ : ∀ (Y : C),
  IsIso (Y := (comparison adj ⋙ rightAdjointComparison adj).obj Y) (NatTrans.app (unit (comparisonAdjunction adj)) Y)
Tactic: have : ∀ (Y : C), IsIso ((comparisonAdjunction adj).unit.app Y) := by
      intro Y
      rw [comparisonAdjunction_unit_app]
      change IsIso (IsLimit.conePointUniqueUpToIso _ ?_).inv
      · infer_instance
      apply @unitEqualizerOfCoreflectsEqualizer _ _ _ _ _ _ _ _ ?_
      letI _ :
        F.IsCosplitPair (G.map (F.map (adj.unit.app Y)))
          (adj.unit.app (G.obj (F.obj Y))) :=
        ComonadicityInternal.main_pair_F_cosplit _ ((comparison adj).obj Y)
      infer_instance
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Comonadicity (goal)
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₁, u₂} D
F : Functor.{v₁, v₁, u₁, u₂} C D
G : Functor.{v₁, v₁, u₂, u₁} D C
adj : F ⊣ G
inst_2 : CreatesLimitOfIsCosplitPair F
A B : C
f g : A ⟶ B
inst_3 : F.IsCosplitPair f g
⊢ HasLimit (parallelPair f g ⋙ F)
have rw : HasLimit
  (parallelPair ((parallelPair f g ⋙ F).map WalkingParallelPairHom.left)
    ((parallelPair f g ⋙ F).map WalkingParallelPairHom.right))
Tactic: rw [hasLimit_iff_of_iso (diagramIsoParallelPair _)]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Comonadicity (hypothesis)
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₁, u₂} D
F : Functor.{v₁, v₁, u₁, u₂} C D
G : Functor.{v₁, v₁, u₂, u₁} D C
adj : F ⊣ G
inst_2 : CreatesLimitOfIsCosplitPair F
⊢ ComonadicLeftAdjoint F
have I : ∀ {A B : C} (f g : A ⟶ B) [F.IsCosplitPair f g], HasLimit (parallelPair f g ⋙ F)
Tactic: have I {A B} (f g : A ⟶ B) [F.IsCosplitPair f g] : HasLimit (parallelPair f g ⋙ F) := by
    rw [hasLimit_iff_of_iso (diagramIsoParallelPair _)]
    exact inferInstanceAs <| HasEqualizer (F.map f) (F.map g)
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Comonadicity (hypothesis)
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₁, u₂} D
F : Functor.{v₁, v₁, u₁, u₂} C D
G : Functor.{v₁, v₁, u₂, u₁} D C
adj : F ⊣ G
inst_2 : CreatesLimitOfIsCosplitPair F
I : ∀ {A B : C} (f g : A ⟶ B) [F.IsCosplitPair f g], HasLimit (parallelPair f g ⋙ F)
⊢ ComonadicLeftAdjoint F
have this : HasEqualizerOfIsCosplitPair F
Tactic: have : HasEqualizerOfIsCosplitPair F := ⟨fun _ _ => hasLimit_of_created (parallelPair _ _) F⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Comonadicity (hypothesis)
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₁, u₂} D
F : Functor.{v₁, v₁, u₁, u₂} C D
G : Functor.{v₁, v₁, u₂, u₁} D C
adj : F ⊣ G
inst_2 : CreatesLimitOfIsCosplitPair F
I : ∀ {A B : C} (f g : A ⟶ B) [F.IsCosplitPair f g], HasLimit (parallelPair f g ⋙ F)
this : HasEqualizerOfIsCosplitPair F
⊢ ComonadicLeftAdjoint F
have this₁ : PreservesLimitOfIsCosplitPair F
Tactic: have : PreservesLimitOfIsCosplitPair F := ⟨by intros; infer_instance⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Comonadicity (hypothesis)
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₁, u₂} D
F : Functor.{v₁, v₁, u₁, u₂} C D
G : Functor.{v₁, v₁, u₂, u₁} D C
adj : F ⊣ G
inst_2 : CreatesLimitOfIsCosplitPair F
I : ∀ {A B : C} (f g : A ⟶ B) [F.IsCosplitPair f g], HasLimit (parallelPair f g ⋙ F)
this_1 : HasEqualizerOfIsCosplitPair F
this : PreservesLimitOfIsCosplitPair F
⊢ ComonadicLeftAdjoint F
have this₁ : ReflectsLimitOfIsCosplitPair F
Tactic: have : ReflectsLimitOfIsCosplitPair F := ⟨by intros; infer_instance⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Comonadicity (hypothesis)
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₁, u₂} D
F : Functor.{v₁, v₁, u₁, u₂} C D
G : Functor.{v₁, v₁, u₂, u₁} D C
adj : F ⊣ G
inst_2 : F.ReflectsIsomorphisms
inst_3 : HasEqualizerOfIsCosplitPair F
inst_4 : PreservesLimitOfIsCosplitPair F
A B : C
f g : A ⟶ B
h : F.IsCosplitPair f g
⊢ ReflectsLimit (parallelPair f g) F
have this : HasEqualizer f g
Tactic: have := HasEqualizerOfIsCosplitPair.out F f g
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Comonadicity (hypothesis)
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₁, u₂} D
F : Functor.{v₁, v₁, u₁, u₂} C D
G : Functor.{v₁, v₁, u₂, u₁} D C
adj : F ⊣ G
inst_2 : F.ReflectsIsomorphisms
inst_3 : HasEqualizerOfIsCosplitPair F
inst_4 : PreservesLimitOfIsCosplitPair F
⊢ ComonadicLeftAdjoint F
have this : ReflectsLimitOfIsCosplitPair F
Tactic: have : ReflectsLimitOfIsCosplitPair F := ⟨fun f g _ => by
    have := HasEqualizerOfIsCosplitPair.out F f g
    apply reflectsLimit_of_reflectsIsomorphisms⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Comonadicity (goal)
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₁, u₂} D
F : Functor.{v₁, v₁, u₁, u₂} C D
G : Functor.{v₁, v₁, u₂, u₁} D C
adj : F ⊣ G
inst_2 : HasCoreflexiveEqualizers.{v₁, u₁} C
inst_3 : F.ReflectsIsomorphisms
inst_4 : PreservesLimitOfIsCoreflexivePair F
X : adj.toComonad.Coalgebra
⊢ IsIso (X := (rightAdjointComparison adj ⋙ comparison adj).obj X) (NatTrans.app (counit (comparisonAdjunction adj)) X)
have _ : IsIso (X := adj.toComonad.forget.obj ((rightAdjointComparison adj ⋙ comparison adj).obj X))
  (adj.toComonad.forget.map (NatTrans.app (counit (comparisonAdjunction adj)) X))
Tactic: apply
        @isIso_of_reflects_iso _ _ _ _ _ _ _ (Comonad.forget adj.toComonad) ?_ _
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Comonadicity (goal)
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₁, u₂} D
F : Functor.{v₁, v₁, u₁, u₂} C D
G : Functor.{v₁, v₁, u₂, u₁} D C
adj : F ⊣ G
inst_2 : HasCoreflexiveEqualizers.{v₁, u₁} C
inst_3 : F.ReflectsIsomorphisms
inst_4 : PreservesLimitOfIsCoreflexivePair F
X : adj.toComonad.Coalgebra
⊢ IsIso (X := adj.toComonad.forget.obj ((rightAdjointComparison adj ⋙ comparison adj).obj X))
    (adj.toComonad.forget.map (NatTrans.app (counit (comparisonAdjunction adj)) X))
have change : IsIso (X := ((rightAdjointComparison adj ⋙ comparison adj).obj X).A)
  (Coalgebra.Hom.f (NatTrans.app (counit (comparisonAdjunction adj)) X))
Tactic: change IsIso ((comparisonAdjunction adj).counit.app X).f
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Comonadicity (goal)
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₁, u₂} D
F : Functor.{v₁, v₁, u₁, u₂} C D
G : Functor.{v₁, v₁, u₂, u₁} D C
adj : F ⊣ G
inst_2 : HasCoreflexiveEqualizers.{v₁, u₁} C
inst_3 : F.ReflectsIsomorphisms
inst_4 : PreservesLimitOfIsCoreflexivePair F
X : adj.toComonad.Coalgebra
⊢ IsIso (X := ((rightAdjointComparison adj ⋙ comparison adj).obj X).A)
    (Coalgebra.Hom.f (NatTrans.app (counit (comparisonAdjunction adj)) X))
have rw : IsIso (X := ((rightAdjointComparison adj ⋙ comparison adj).obj X).A)
  ((beckEqualizer X).lift (counitFork X) : (counitFork X).pt ⟶ (beckFork X).pt)
Tactic: rw [comparisonAdjunction_counit_f]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Comonadicity (hypothesis)
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₁, u₂} D
F : Functor.{v₁, v₁, u₁, u₂} C D
G : Functor.{v₁, v₁, u₂, u₁} D C
adj : F ⊣ G
inst_2 : HasCoreflexiveEqualizers.{v₁, u₁} C
inst_3 : F.ReflectsIsomorphisms
inst_4 : PreservesLimitOfIsCoreflexivePair F
⊢ (comparison adj).IsEquivalence
have this : ∀ (X : adj.toComonad.Coalgebra),
  IsIso (X := (rightAdjointComparison adj ⋙ comparison adj).obj X) (NatTrans.app (counit (comparisonAdjunction adj)) X)
Tactic: have : ∀ (X : adj.toComonad.Coalgebra), IsIso ((comparisonAdjunction adj).counit.app X) := by
      intro X
      apply
        @isIso_of_reflects_iso _ _ _ _ _ _ _ (Comonad.forget adj.toComonad) ?_ _
      · change IsIso ((comparisonAdjunction adj).counit.app X).f
        rw [comparisonAdjunction_counit_f]
        exact (IsLimit.conePointUniqueUpToIso (beckEqualizer X)
          (counitLimitOfPreservesEqualizer X)).isIso_inv
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Comonadicity (goal)
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₁, u₂} D
F : Functor.{v₁, v₁, u₁, u₂} C D
G : Functor.{v₁, v₁, u₂, u₁} D C
adj : F ⊣ G
inst_2 : HasCoreflexiveEqualizers.{v₁, u₁} C
inst_3 : F.ReflectsIsomorphisms
inst_4 : PreservesLimitOfIsCoreflexivePair F
this :
  ∀ (X : adj.toComonad.Coalgebra),
    IsIso (X := (rightAdjointComparison adj ⋙ comparison adj).obj X)
      (NatTrans.app (counit (comparisonAdjunction adj)) X)
Y : C
⊢ IsIso (Y := (comparison adj ⋙ rightAdjointComparison adj).obj Y) (NatTrans.app (unit (comparisonAdjunction adj)) Y)
have rw : IsIso (X := Functor.obj.{v₁, v₁, u₁, u₁} (𝟭 C) Y) (Y := (comparison adj ⋙ rightAdjointComparison adj).obj Y)
  (limit.lift (parallelPair (G.map (F.map (adj.unit.app Y))) (adj.unit.app (G.obj (F.obj Y)))) (unitFork adj Y) :
    (unitFork adj Y).pt ⟶ limit (parallelPair (G.map (F.map (adj.unit.app Y))) (adj.unit.app (G.obj (F.obj Y)))))
Tactic: rw [comparisonAdjunction_unit_app]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Comonadicity (goal)
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₁, u₂} D
F : Functor.{v₁, v₁, u₁, u₂} C D
G : Functor.{v₁, v₁, u₂, u₁} D C
adj : F ⊣ G
inst_2 : HasCoreflexiveEqualizers.{v₁, u₁} C
inst_3 : F.ReflectsIsomorphisms
inst_4 : PreservesLimitOfIsCoreflexivePair F
this :
  ∀ (X : adj.toComonad.Coalgebra),
    IsIso (X := (rightAdjointComparison adj ⋙ comparison adj).obj X)
      (NatTrans.app (counit (comparisonAdjunction adj)) X)
Y : C
⊢ IsIso (X := Functor.obj.{v₁, v₁, u₁, u₁} (𝟭 C) Y) (Y := (comparison adj ⋙ rightAdjointComparison adj).obj Y)
    (limit.lift (parallelPair (G.map (F.map (adj.unit.app Y))) (adj.unit.app (G.obj (F.obj Y)))) (unitFork adj Y) :
      (unitFork adj Y).pt ⟶ limit (parallelPair (G.map (F.map (adj.unit.app Y))) (adj.unit.app (G.obj (F.obj Y)))))
have change : IsIso (X := (unitFork adj Y).pt) (Y :=
  (limit.cone (parallelPair (G.map (F.map (adj.unit.app Y))) (adj.unit.app (G.obj (F.obj Y))))).pt)
  (Iso.inv
    (IsLimit.conePointUniqueUpToIso
      (limit.isLimit (parallelPair (G.map (F.map (adj.unit.app Y))) (adj.unit.app (G.obj (F.obj Y)))))
      (have this : IsCoreflexivePair (G.map (F.map (adj.unit.app Y))) (adj.unit.app (G.obj (F.obj Y))) := sorry;
      unitEqualizerOfCoreflectsEqualizer adj Y)))
Tactic: change IsIso (IsLimit.conePointUniqueUpToIso _ ?_).inv
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Comonadicity (goal)
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₁, u₂} D
F : Functor.{v₁, v₁, u₁, u₂} C D
G : Functor.{v₁, v₁, u₂, u₁} D C
adj : F ⊣ G
inst_2 : HasCoreflexiveEqualizers.{v₁, u₁} C
inst_3 : F.ReflectsIsomorphisms
inst_4 : PreservesLimitOfIsCoreflexivePair F
this :
  ∀ (X : adj.toComonad.Coalgebra),
    IsIso (X := (rightAdjointComparison adj ⋙ comparison adj).obj X)
      (NatTrans.app (counit (comparisonAdjunction adj)) X)
Y : C
change :
  IsIso (X := (unitFork adj Y).pt) (Y :=
    (limit.cone (parallelPair (G.map (F.map (adj.unit.app Y))) (adj.unit.app (G.obj (F.obj Y))))).pt)
    (Iso.inv
      (IsLimit.conePointUniqueUpToIso
        (limit.isLimit (parallelPair (G.map (F.map (adj.unit.app Y))) (adj.unit.app (G.obj (F.obj Y)))))
        (have this : IsCoreflexivePair (G.map (F.map (adj.unit.app Y))) (adj.unit.app (G.obj (F.obj Y))) := ⋯;
        unitEqualizerOfCoreflectsEqualizer adj Y)))
⊢ IsIso (X := Functor.obj.{v₁, v₁, u₁, u₁} (𝟭 C) Y) (Y := (comparison adj ⋙ rightAdjointComparison adj).obj Y)
    (limit.lift (parallelPair (G.map (F.map (adj.unit.app Y))) (adj.unit.app (G.obj (F.obj Y)))) (unitFork adj Y) :
      (unitFork adj Y).pt ⟶ limit (parallelPair (G.map (F.map (adj.unit.app Y))) (adj.unit.app (G.obj (F.obj Y)))))
have change₁ : IsLimit (unitFork adj Y)
Tactic: change IsIso (IsLimit.conePointUniqueUpToIso _ ?_).inv
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Comonadicity (goal)
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₁, u₂} D
F : Functor.{v₁, v₁, u₁, u₂} C D
G : Functor.{v₁, v₁, u₂, u₁} D C
adj : F ⊣ G
inst_2 : HasCoreflexiveEqualizers.{v₁, u₁} C
inst_3 : F.ReflectsIsomorphisms
inst_4 : PreservesLimitOfIsCoreflexivePair F
this :
  ∀ (X : adj.toComonad.Coalgebra),
    IsIso (X := (rightAdjointComparison adj ⋙ comparison adj).obj X)
      (NatTrans.app (counit (comparisonAdjunction adj)) X)
Y : C
⊢ IsCoreflexivePair (G.map (F.map (adj.unit.app Y))) (adj.unit.app (G.obj (F.obj Y)))
have apply : G.map (F.map (adj.unit.app Y)) ≫ G.map (adj.counit.app (F.1 (Functor.obj.{v₁, v₁, u₁, u₁} (𝟭 C) Y))) =
  𝟙 (G.obj (Functor.obj.{v₁, v₁, u₂, u₂} (𝟭 D) (F.1 (Functor.obj.{v₁, v₁, u₁, u₁} (𝟭 C) Y))))
Tactic: apply IsCoreflexivePair.mk' (G.map (adj.counit.app _)) _ _
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Comonadicity (goal)
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₁, u₂} D
F : Functor.{v₁, v₁, u₁, u₂} C D
G : Functor.{v₁, v₁, u₂, u₁} D C
adj : F ⊣ G
inst_2 : HasCoreflexiveEqualizers.{v₁, u₁} C
inst_3 : F.ReflectsIsomorphisms
inst_4 : PreservesLimitOfIsCoreflexivePair F
this :
  ∀ (X : adj.toComonad.Coalgebra),
    IsIso (X := (rightAdjointComparison adj ⋙ comparison adj).obj X)
      (NatTrans.app (counit (comparisonAdjunction adj)) X)
Y : C
apply :
  G.map (F.map (adj.unit.app Y)) ≫ G.map (adj.counit.app (F.1 (Functor.obj.{v₁, v₁, u₁, u₁} (𝟭 C) Y))) =
    𝟙 (G.obj (Functor.obj.{v₁, v₁, u₂, u₂} (𝟭 D) (F.1 (Functor.obj.{v₁, v₁, u₁, u₁} (𝟭 C) Y))))
⊢ IsCoreflexivePair (G.map (F.map (adj.unit.app Y))) (adj.unit.app (G.obj (F.obj Y)))
have apply₁ : adj.unit.app (G.obj (F.obj Y)) ≫ G.map (adj.counit.app (F.1 (Functor.obj.{v₁, v₁, u₁, u₁} (𝟭 C) Y))) =
  𝟙 (G.obj (Functor.obj.{v₁, v₁, u₂, u₂} (𝟭 D) (F.1 (Functor.obj.{v₁, v₁, u₁, u₁} (𝟭 C) Y))))
Tactic: apply IsCoreflexivePair.mk' (G.map (adj.counit.app _)) _ _
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Comonadicity (goal)
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₁, u₂} D
F : Functor.{v₁, v₁, u₁, u₂} C D
G : Functor.{v₁, v₁, u₂, u₁} D C
adj : F ⊣ G
inst_2 : HasCoreflexiveEqualizers.{v₁, u₁} C
inst_3 : F.ReflectsIsomorphisms
inst_4 : PreservesLimitOfIsCoreflexivePair F
this :
  ∀ (X : adj.toComonad.Coalgebra),
    IsIso (X := (rightAdjointComparison adj ⋙ comparison adj).obj X)
      (NatTrans.app (counit (comparisonAdjunction adj)) X)
Y : C
⊢ G.map (F.map (adj.unit.app Y)) ≫ G.map (adj.counit.app (F.1 (Functor.obj.{v₁, v₁, u₁, u₁} (𝟭 C) Y))) =
    𝟙 (G.obj (Functor.obj.{v₁, v₁, u₂, u₂} (𝟭 D) (F.1 (Functor.obj.{v₁, v₁, u₁, u₁} (𝟭 C) Y))))
have rw : G.map (F.map (adj.unit.app Y) ≫ adj.counit.app (F.1 (Functor.obj.{v₁, v₁, u₁, u₁} (𝟭 C) Y))) =
  G.map (𝟙 (Functor.obj.{v₁, v₁, u₂, u₂} (𝟭 D) (F.1 (Functor.obj.{v₁, v₁, u₁, u₁} (𝟭 C) Y))))
Tactic: rw [← G.map_comp, ← G.map_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Comonadicity (goal)
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₁, u₂} D
F : Functor.{v₁, v₁, u₁, u₂} C D
G : Functor.{v₁, v₁, u₂, u₁} D C
adj : F ⊣ G
inst_2 : HasCoreflexiveEqualizers.{v₁, u₁} C
inst_3 : F.ReflectsIsomorphisms
inst_4 : PreservesLimitOfIsCoreflexivePair F
this :
  ∀ (X : adj.toComonad.Coalgebra),
    IsIso (X := (rightAdjointComparison adj ⋙ comparison adj).obj X)
      (NatTrans.app (counit (comparisonAdjunction adj)) X)
Y : C
⊢ adj.unit.app (G.obj (F.obj Y)) ≫ G.map (adj.counit.app (F.1 (Functor.obj.{v₁, v₁, u₁, u₁} (𝟭 C) Y))) =
    𝟙 (G.obj (Functor.obj.{v₁, v₁, u₂, u₂} (𝟭 D) (F.1 (Functor.obj.{v₁, v₁, u₁, u₁} (𝟭 C) Y))))
have rw : adj.unit.app (G.obj (F.obj Y)) ≫ G.map (adj.counit.app (F.1 (Functor.obj.{v₁, v₁, u₁, u₁} (𝟭 C) Y))) =
  G.map (𝟙 (Functor.obj.{v₁, v₁, u₂, u₂} (𝟭 D) (F.1 (Functor.obj.{v₁, v₁, u₁, u₁} (𝟭 C) Y))))
Tactic: rw [← G.map_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Comonadicity (hypothesis)
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₁, u₂} D
F : Functor.{v₁, v₁, u₁, u₂} C D
G : Functor.{v₁, v₁, u₂, u₁} D C
adj : F ⊣ G
inst_2 : HasCoreflexiveEqualizers.{v₁, u₁} C
inst_3 : F.ReflectsIsomorphisms
inst_4 : PreservesLimitOfIsCoreflexivePair F
this :
  ∀ (X : adj.toComonad.Coalgebra),
    IsIso (X := (rightAdjointComparison adj ⋙ comparison adj).obj X)
      (NatTrans.app (counit (comparisonAdjunction adj)) X)
Y : C
⊢ IsLimit (unitFork adj Y)
have this₁ : IsCoreflexivePair (G.map (F.map (adj.unit.app Y))) (adj.unit.app (G.obj (F.obj Y)))
Tactic: have : IsCoreflexivePair (G.map (F.map (adj.unit.app Y)))
          (adj.unit.app (G.obj (F.obj Y))) := by
        apply IsCoreflexivePair.mk' (G.map (adj.counit.app _)) _ _
        · rw [← G.map_comp, ← G.map_id]
          exact congr_arg G.map (adj.left_triangle_components Y)
        · rw [← G.map_id]
          simp