awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Adjunction.Lifting.Right
Goal:
A : Type u₁
B : Type u₂
C : Type u₃
inst : Category.{v₁, u₁} A
inst_1 : Category.{v₂, u₂} B
inst_2 : Category.{v₃, u₃} C
U : Functor.{v₁, v₂, u₁, u₂} A B
F : Functor.{v₂, v₁, u₂, u₁} B A
L : Functor.{v₃, v₂, u₃, u₂} C B
U' : Functor.{v₁, v₃, u₁, u₃} A C
adj₁ : F ⊣ U
adj₂ : L ⋙ F ⊣ U'
inst_3 : HasCoreflexiveEqualizers.{v₃, u₃} C
h : (X : B) → RegularMono (adj₁.unit.app X)
Y : C
X : B
apply :
  ∀ (a : F.obj (L.obj Y) ⟶ F.obj X),
    F.map (adj₁.unit.app (L.obj Y) ≫ U.map a) = a ≫ F.map (adj₁.unit.app X) ↔
      Eq.{v₂ + 1} (α := L.obj Y ⟶ U.obj (F.obj ((F ⋙ U).obj X)))
        (((adj₁.homEquiv (L.obj Y) (F.obj X) :
                  Equiv.{v₁ + 1, v₂ + 1} (F.obj (L.obj Y) ⟶ F.obj X) (L.obj Y ⟶ U.obj (F.obj X))) :
                (a : F.obj (L.obj Y) ⟶ F.obj X) → L.obj Y ⟶ U.obj (F.obj X))
              a ≫
            U.map (F.map (adj₁.unit.app X)) :
          L.obj Y ⟶ U.obj (F.obj ((F ⋙ U).obj X)))
        (((adj₁.homEquiv (L.obj Y) (F.obj X) :
                  Equiv.{v₁ + 1, v₂ + 1} (F.obj (L.obj Y) ⟶ F.obj X) (L.obj Y ⟶ U.obj (F.obj X))) :
                (a : F.obj (L.obj Y) ⟶ F.obj X) → L.obj Y ⟶ U.obj (F.obj X))
              a ≫
            adj₁.unit.app (U.obj (F.obj X)) :
          L.obj Y ⟶ (F ⋙ U).obj (U.obj (F.obj X)))
⊢ Equiv.{v₁ + 1, max 1 (v₂ + 1)}
    { g : F.obj (L.obj Y) ⟶ F.obj X // F.map (adj₁.unit.app (L.obj Y) ≫ U.map g) = g ≫ F.map (adj₁.unit.app X) }
    { z : L.obj Y ⟶ U.obj (F.obj X) // z ≫ U.map (F.map (adj₁.unit.app X)) = z ≫ adj₁.unit.app (U.obj (F.obj X)) }

Tactic:
apply (adj₁.homEquiv _ _).subtypeEquiv

Premises used: Equiv.subtypeEquiv, CategoryTheory.Adjunction.homEquiv
-- Module: Mathlib.CategoryTheory.Adjunction.Lifting.Right
Goal:
A : Type u₁
B : Type u₂
C : Type u₃
inst : Category.{v₁, u₁} A
inst_1 : Category.{v₂, u₂} B
inst_2 : Category.{v₃, u₃} C
U : Functor.{v₁, v₂, u₁, u₂} A B
F : Functor.{v₂, v₁, u₂, u₁} B A
L : Functor.{v₃, v₂, u₃, u₂} C B
U' : Functor.{v₁, v₃, u₁, u₃} A C
adj₁ : F ⊣ U
adj₂ : L ⋙ F ⊣ U'
inst_3 : HasCoreflexiveEqualizers.{v₃, u₃} C
h : (X : B) → RegularMono (adj₁.unit.app X)
Y : C
X : B
g : F.obj (L.obj Y) ⟶ F.obj X
rw :
  adj₁.unit.app (Functor.obj.{v₂, v₂, u₂, u₂} (𝟭 B) (L.obj Y)) ≫ U.map (g ≫ F.map (adj₁.unit.app X)) =
      adj₁.unit.app (Functor.obj.{v₂, v₂, u₂, u₂} (𝟭 B) (L.obj Y)) ≫ U.map (F.map (adj₁.unit.app (L.obj Y) ≫ U.map g)) ↔
    (adj₁.unit.app (L.obj Y) ≫ U.map g) ≫ U.map (F.map (adj₁.unit.app X)) =
      (adj₁.unit.app (L.obj Y) ≫ U.map g) ≫ adj₁.unit.app (U.obj (F.obj X))
⊢ F.map (adj₁.unit.app (L.obj Y) ≫ U.map g) = g ≫ F.map (adj₁.unit.app X) ↔
    Eq.{v₂ + 1} (α := L.obj Y ⟶ U.obj (F.obj ((F ⋙ U).obj X)))
      (((adj₁.homEquiv (L.obj Y) (F.obj X) :
                Equiv.{v₁ + 1, v₂ + 1} (F.obj (L.obj Y) ⟶ F.obj X) (L.obj Y ⟶ U.obj (F.obj X))) :
              (a : F.obj (L.obj Y) ⟶ F.obj X) → L.obj Y ⟶ U.obj (F.obj X))
            g ≫
          U.map (F.map (adj₁.unit.app X)) :
        L.obj Y ⟶ U.obj (F.obj ((F ⋙ U).obj X)))
      (((adj₁.homEquiv (L.obj Y) (F.obj X) :
                Equiv.{v₁ + 1, v₂ + 1} (F.obj (L.obj Y) ⟶ F.obj X) (L.obj Y ⟶ U.obj (F.obj X))) :
              (a : F.obj (L.obj Y) ⟶ F.obj X) → L.obj Y ⟶ U.obj (F.obj X))
            g ≫
          adj₁.unit.app (U.obj (F.obj X)) :
        L.obj Y ⟶ (F ⋙ U).obj (U.obj (F.obj X)))

Tactic:
rw [← (adj₁.homEquiv _ _).injective.eq_iff, adj₁.homEquiv_unit,
        adj₁.homEquiv_unit, adj₁.homEquiv_unit, eq_comm]

Premises used: CategoryTheory.Adjunction.homEquiv_unit, Function.Injective.eq_iff, eq_comm, CategoryTheory.Adjunction.homEquiv, Equiv.injective
-- Module: Mathlib.CategoryTheory.Adjunction.Lifting.Right
Goal:
A : Type u₁
B : Type u₂
C : Type u₃
inst : Category.{v₁, u₁} A
inst_1 : Category.{v₂, u₂} B
inst_2 : Category.{v₃, u₃} C
U : Functor.{v₁, v₂, u₁, u₂} A B
F : Functor.{v₂, v₁, u₂, u₁} B A
L : Functor.{v₃, v₂, u₃, u₂} C B
U' : Functor.{v₁, v₃, u₁, u₃} A C
adj₁ : F ⊣ U
adj₂ : L ⋙ F ⊣ U'
inst_3 : HasCoreflexiveEqualizers.{v₃, u₃} C
h : (X : B) → RegularMono (adj₁.unit.app X)
Y : C
X : B
g : F.obj (L.obj Y) ⟶ F.obj X
⊢ adj₁.unit.app (Functor.obj.{v₂, v₂, u₂, u₂} (𝟭 B) (L.obj Y)) ≫ U.map (g ≫ F.map (adj₁.unit.app X)) =
      adj₁.unit.app (Functor.obj.{v₂, v₂, u₂, u₂} (𝟭 B) (L.obj Y)) ≫ U.map (F.map (adj₁.unit.app (L.obj Y) ≫ U.map g)) ↔
    (adj₁.unit.app (L.obj Y) ≫ U.map g) ≫ U.map (F.map (adj₁.unit.app X)) =
      (adj₁.unit.app (L.obj Y) ≫ U.map g) ≫ adj₁.unit.app (U.obj (F.obj X))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Adjunction.Lifting.Right
Goal:
A : Type u₁
B : Type u₂
C : Type u₃
inst : Category.{v₁, u₁} A
inst_1 : Category.{v₂, u₂} B
inst_2 : Category.{v₃, u₃} C
U : Functor.{v₁, v₂, u₁, u₂} A B
F : Functor.{v₂, v₁, u₂, u₁} B A
L : Functor.{v₃, v₂, u₃, u₂} C B
U' : Functor.{v₁, v₃, u₁, u₃} A C
adj₁ : F ⊣ U
adj₂ : L ⋙ F ⊣ U'
inst_3 : HasCoreflexiveEqualizers.{v₃, u₃} C
h : (X : B) → RegularMono (adj₁.unit.app X)
refine :
  ∀ (X' X : C) (Y : B) (f : X' ⟶ X) (g : L.obj X ⟶ Y),
    Eq.{v₃ + 1} (α := X' ⟶ constructRightAdjointObj L U' adj₁ adj₂ Y)
      ((((fun (X : C) (Y : B) ↦
                  (Equiv.symm (constructRightAdjointEquiv L U' adj₁ adj₂ h X Y) :
                    Equiv.{v₂ + 1, v₃ + 1} (L.obj X ⟶ Y) (X ⟶ constructRightAdjointObj L U' adj₁ adj₂ Y)))
                X' Y :
              Equiv.{v₂ + 1, v₃ + 1} (L.obj X' ⟶ Y) (X' ⟶ constructRightAdjointObj L U' adj₁ adj₂ Y)) :
            (a : L.obj X' ⟶ Y) → X' ⟶ constructRightAdjointObj L U' adj₁ adj₂ Y)
          (L.map f ≫ g) :
        X' ⟶ constructRightAdjointObj L U' adj₁ adj₂ Y)
      (f ≫
          (((fun (X : C) (Y : B) ↦
                    (Equiv.symm (constructRightAdjointEquiv L U' adj₁ adj₂ h X Y) :
                      Equiv.{v₂ + 1, v₃ + 1} (L.obj X ⟶ Y) (X ⟶ constructRightAdjointObj L U' adj₁ adj₂ Y)))
                  X Y :
                Equiv.{v₂ + 1, v₃ + 1} (L.obj X ⟶ Y) (X ⟶ constructRightAdjointObj L U' adj₁ adj₂ Y)) :
              (a : L.obj X ⟶ Y) → X ⟶ constructRightAdjointObj L U' adj₁ adj₂ Y)
            g :
        X' ⟶ constructRightAdjointObj L U' adj₁ adj₂ Y)
⊢ Functor.{v₂, v₃, u₂, u₃} B C

Tactic:
refine Adjunction.rightAdjointOfEquiv
    (fun X Y => (constructRightAdjointEquiv L _ adj₁ adj₂ h X Y).symm) ?_

Premises used: CategoryTheory.Adjunction.rightAdjointOfEquiv, CategoryTheory.LiftRightAdjoint.constructRightAdjointEquiv, Equiv.symm
-- Module: Mathlib.CategoryTheory.Adjunction.Lifting.Right
Goal:
A : Type u₁
B : Type u₂
C : Type u₃
inst : Category.{v₁, u₁} A
inst_1 : Category.{v₂, u₂} B
inst_2 : Category.{v₃, u₃} C
U : Functor.{v₁, v₂, u₁, u₂} A B
F : Functor.{v₂, v₁, u₂, u₁} B A
L : Functor.{v₃, v₂, u₃, u₂} C B
U' : Functor.{v₁, v₃, u₁, u₃} A C
adj₁ : F ⊣ U
adj₂ : L ⋙ F ⊣ U'
inst_3 : HasCoreflexiveEqualizers.{v₃, u₃} C
h_1 : (X : B) → RegularMono (adj₁.unit.app X)
X Y : C
Y' : B
g : X ⟶ Y
h : L.obj Y ⟶ Y'
⊢ Eq (α := X ⟶ U'.obj (F.obj Y'))
    (g ≫
      ((adj₂.homEquiv Y (F.obj Y') : Equiv.{v₁ + 1, v₃ + 1} ((L ⋙ F).obj Y ⟶ F.obj Y') (Y ⟶ U'.obj (F.obj Y'))) :
          (a : (L ⋙ F).obj Y ⟶ F.obj Y') → Y ⟶ U'.obj (F.obj Y'))
        (F.map
            (↑((Fork.IsLimit.homIso (unitEqualises adj₁ h_1 Y') (L.obj Y) :
                    (a : L.obj Y ⟶ Y') →
                      { h : L.obj Y ⟶ U.obj (F.obj Y') //
                        h ≫ U.map (F.map (adj₁.unit.app Y')) = h ≫ adj₁.unit.app (U.obj (F.obj Y')) })
                  h) :
              L.obj Y ⟶ U.obj (F.obj Y')) ≫
          adj₁.counit.app (F.obj Y')))
    (g ≫
      (↑(Subtype.mk (p := fun (b : Y ⟶ U'.obj (F.obj Y')) ↦
            b ≫ U'.map (F.map (adj₁.unit.app Y')) = b ≫ otherMap L U' adj₁ adj₂ Y')
            (((adj₂.homEquiv Y (F.obj Y') : Equiv.{v₁ + 1, v₃ + 1} ((L ⋙ F).obj Y ⟶ F.obj Y') (Y ⟶ U'.obj (F.obj Y'))) :
                (a : F.obj (L.obj Y) ⟶ F.obj Y') → Y ⟶ U'.obj (F.obj Y'))
              (F.map
                  (↑((Fork.IsLimit.homIso (unitEqualises adj₁ h_1 Y') (L.obj Y) :
                          (a : L.obj Y ⟶ Y') →
                            { z : L.obj Y ⟶ U.obj (F.obj Y') //
                              z ≫ U.map (F.map (adj₁.unit.app Y')) = z ≫ adj₁.unit.app (U.obj (F.obj Y')) })
                        h) :
                    L.obj Y ⟶ U.obj (F.obj Y')) ≫
                adj₁.counit.app (F.obj Y')))
            ⋯) :
        Y ⟶ U'.obj (F.obj Y')))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Adjunction.Lifting.Right
Goal:
A : Type u₁
B : Type u₂
C : Type u₃
inst : Category.{v₁, u₁} A
inst_1 : Category.{v₂, u₂} B
inst_2 : Category.{v₃, u₃} C
F : Functor.{v₂, v₁, u₂, u₁} B A
inst_3 : ComonadicLeftAdjoint F
L : Functor.{v₃, v₂, u₃, u₂} C B
inst_4 : HasCoreflexiveEqualizers.{v₃, u₃} C
inst_5 : (L ⋙ F).IsLeftAdjoint
L' : C ⥤ (Adjunction.toComonad (R := comonadicRightAdjoint F) (comonadicAdjunction F)).Coalgebra :=
  L ⋙ Comonad.comparison (comonadicAdjunction F)
rsuffices : L'.IsLeftAdjoint → L.IsLeftAdjoint
rsuffices₁ : L'.IsLeftAdjoint
⊢ L.IsLeftAdjoint

Tactic:
rsuffices : L'.IsLeftAdjoint

Premises used: CategoryTheory.Functor.IsLeftAdjoint
-- Module: Mathlib.CategoryTheory.Adjunction.Lifting.Right
Goal:
A : Type u₁
B : Type u₂
C : Type u₃
inst : Category.{v₁, u₁} A
inst_1 : Category.{v₂, u₂} B
inst_2 : Category.{v₃, u₃} C
F : Functor.{v₂, v₁, u₂, u₁} B A
inst_3 : ComonadicLeftAdjoint F
L : Functor.{v₃, v₂, u₃, u₂} C B
inst_4 : HasCoreflexiveEqualizers.{v₃, u₃} C
inst_5 : (L ⋙ F).IsLeftAdjoint
L' : C ⥤ (Adjunction.toComonad (R := comonadicRightAdjoint F) (comonadicAdjunction F)).Coalgebra :=
  L ⋙ Comonad.comparison (comonadicAdjunction F)
this : L'.IsLeftAdjoint
⊢ (L' ⋙ Functor.inv (Comonad.comparison (comonadicAdjunction F))).IsLeftAdjoint

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Adjunction.Lifting.Right
Goal:
A : Type u₁
B : Type u₂
C : Type u₃
inst : Category.{v₁, u₁} A
inst_1 : Category.{v₂, u₂} B
inst_2 : Category.{v₃, u₃} C
F : Functor.{v₂, v₁, u₂, u₁} B A
inst_3 : ComonadicLeftAdjoint F
L : Functor.{v₃, v₂, u₃, u₂} C B
inst_4 : HasCoreflexiveEqualizers.{v₃, u₃} C
inst_5 : (L ⋙ F).IsLeftAdjoint
L' : C ⥤ (Adjunction.toComonad (R := comonadicRightAdjoint F) (comonadicAdjunction F)).Coalgebra :=
  L ⋙ Comonad.comparison (comonadicAdjunction F)
this_1 : L'.IsLeftAdjoint
this : (L' ⋙ Functor.inv (Comonad.comparison (comonadicAdjunction F))).IsLeftAdjoint := ⋯
⊢ L.IsLeftAdjoint

Tactic:
((Adjunction.ofIsLeftAdjoint
      (L' ⋙ (Comonad.comparison (comonadicAdjunction F)).inv)).ofNatIsoLeft ?_).isLeftAdjoint

Premises used: CategoryTheory.Adjunction.ofIsLeftAdjoint, CategoryTheory.Functor.comp, CategoryTheory.Adjunction.isLeftAdjoint, CategoryTheory.Functor.inv, CategoryTheory.Comonad.comparison, CategoryTheory.comonadicAdjunction, CategoryTheory.Adjunction.ofNatIsoLeft
-- Module: Mathlib.CategoryTheory.Adjunction.Lifting.Right
Goal:
A : Type u₁
B : Type u₂
C : Type u₃
inst : Category.{v₁, u₁} A
inst_1 : Category.{v₂, u₂} B
inst_2 : Category.{v₃, u₃} C
F : Functor.{v₂, v₁, u₂, u₁} B A
inst_3 : ComonadicLeftAdjoint F
L : Functor.{v₃, v₂, u₃, u₂} C B
inst_4 : HasCoreflexiveEqualizers.{v₃, u₃} C
inst_5 : (L ⋙ F).IsLeftAdjoint
L' : C ⥤ (Adjunction.toComonad (R := comonadicRightAdjoint F) (comonadicAdjunction F)).Coalgebra :=
  L ⋙ Comonad.comparison (comonadicAdjunction F)
this_1 : L'.IsLeftAdjoint
this : (L' ⋙ Functor.inv (Comonad.comparison (comonadicAdjunction F))).IsLeftAdjoint := ⋯
refine : L' ⋙ Functor.inv (Comonad.comparison (comonadicAdjunction F)) ≅ L
⊢ L.IsLeftAdjoint

Tactic:
refine ((Adjunction.ofIsLeftAdjoint
      (L' ⋙ (Comonad.comparison (comonadicAdjunction F)).inv)).ofNatIsoLeft ?_).isLeftAdjoint

Premises used: CategoryTheory.Adjunction.ofIsLeftAdjoint, CategoryTheory.Functor.comp, CategoryTheory.Adjunction.isLeftAdjoint, CategoryTheory.Functor.inv, CategoryTheory.Comonad.comparison, CategoryTheory.comonadicAdjunction, CategoryTheory.Adjunction.ofNatIsoLeft
-- Module: Mathlib.CategoryTheory.Adjunction.Lifting.Right
Goal:
A : Type u₁
B : Type u₂
C : Type u₃
inst : Category.{v₁, u₁} A
inst_1 : Category.{v₂, u₂} B
inst_2 : Category.{v₃, u₃} C
F : Functor.{v₂, v₁, u₂, u₁} B A
inst_3 : ComonadicLeftAdjoint F
L : Functor.{v₃, v₂, u₃, u₂} C B
inst_4 : HasCoreflexiveEqualizers.{v₃, u₃} C
inst_5 : (L ⋙ F).IsLeftAdjoint
L' : C ⥤ (Adjunction.toComonad (R := comonadicRightAdjoint F) (comonadicAdjunction F)).Coalgebra :=
  L ⋙ Comonad.comparison (comonadicAdjunction F)
this_1 : L'.IsLeftAdjoint
this : (L' ⋙ Functor.inv (Comonad.comparison (comonadicAdjunction F))).IsLeftAdjoint := ⋯
⊢ L' ⋙ Functor.inv (Comonad.comparison (comonadicAdjunction F)) ≅ L

Tactic:
exact Functor.isoWhiskerLeft L (Comonad.comparison _).asEquivalence.unitIso.symm ≪≫ L.leftUnitor

Premises used: CategoryTheory.Equivalence.unitIso, CategoryTheory.Functor.asEquivalence, CategoryTheory.Functor.isoWhiskerLeft, CategoryTheory.Functor.leftUnitor, CategoryTheory.Iso.symm, CategoryTheory.Comonad.comparison
-- Module: Mathlib.CategoryTheory.Adjunction.Lifting.Right
Goal:
A : Type u₁
B : Type u₂
C : Type u₃
inst : Category.{v₁, u₁} A
inst_1 : Category.{v₂, u₂} B
inst_2 : Category.{v₃, u₃} C
F : Functor.{v₂, v₁, u₂, u₁} B A
inst_3 : ComonadicLeftAdjoint F
L : Functor.{v₃, v₂, u₃, u₂} C B
inst_4 : HasCoreflexiveEqualizers.{v₃, u₃} C
inst_5 : (L ⋙ F).IsLeftAdjoint
L' : C ⥤ (Adjunction.toComonad (R := comonadicRightAdjoint F) (comonadicAdjunction F)).Coalgebra :=
  L ⋙ Comonad.comparison (comonadicAdjunction F)
⊢ (L' ⋙ (Adjunction.toComonad (R := comonadicRightAdjoint F) (comonadicAdjunction F)).forget).IsLeftAdjoint

Tactic:
((Adjunction.ofIsLeftAdjoint (L ⋙ F)).ofNatIsoLeft ?_).isLeftAdjoint

Premises used: CategoryTheory.Adjunction.ofIsLeftAdjoint, CategoryTheory.Functor.comp, CategoryTheory.Adjunction.isLeftAdjoint, CategoryTheory.Adjunction.ofNatIsoLeft
-- Module: Mathlib.CategoryTheory.Adjunction.Lifting.Right
Goal:
A : Type u₁
B : Type u₂
C : Type u₃
inst : Category.{v₁, u₁} A
inst_1 : Category.{v₂, u₂} B
inst_2 : Category.{v₃, u₃} C
F : Functor.{v₂, v₁, u₂, u₁} B A
inst_3 : ComonadicLeftAdjoint F
L : Functor.{v₃, v₂, u₃, u₂} C B
inst_4 : HasCoreflexiveEqualizers.{v₃, u₃} C
inst_5 : (L ⋙ F).IsLeftAdjoint
L' : C ⥤ (Adjunction.toComonad (R := comonadicRightAdjoint F) (comonadicAdjunction F)).Coalgebra :=
  L ⋙ Comonad.comparison (comonadicAdjunction F)
refine : L ⋙ F ≅ L' ⋙ (Adjunction.toComonad (R := comonadicRightAdjoint F) (comonadicAdjunction F)).forget
⊢ (L' ⋙ (Adjunction.toComonad (R := comonadicRightAdjoint F) (comonadicAdjunction F)).forget).IsLeftAdjoint

Tactic:
refine ((Adjunction.ofIsLeftAdjoint (L ⋙ F)).ofNatIsoLeft ?_).isLeftAdjoint

Premises used: CategoryTheory.Adjunction.ofIsLeftAdjoint, CategoryTheory.Functor.comp, CategoryTheory.Adjunction.isLeftAdjoint, CategoryTheory.Adjunction.ofNatIsoLeft
-- Module: Mathlib.CategoryTheory.Adjunction.Lifting.Right
Goal:
A : Type u₁
B : Type u₂
C : Type u₃
inst : Category.{v₁, u₁} A
inst_1 : Category.{v₂, u₂} B
inst_2 : Category.{v₃, u₃} C
F : Functor.{v₂, v₁, u₂, u₁} B A
inst_3 : ComonadicLeftAdjoint F
L : Functor.{v₃, v₂, u₃, u₂} C B
inst_4 : HasCoreflexiveEqualizers.{v₃, u₃} C
inst_5 : (L ⋙ F).IsLeftAdjoint
L' : C ⥤ (Adjunction.toComonad (R := comonadicRightAdjoint F) (comonadicAdjunction F)).Coalgebra :=
  L ⋙ Comonad.comparison (comonadicAdjunction F)
⊢ L ⋙ F ≅ L' ⋙ (Adjunction.toComonad (R := comonadicRightAdjoint F) (comonadicAdjunction F)).forget

Tactic:
exact Functor.isoWhiskerLeft L (Comonad.comparisonForget (comonadicAdjunction F)).symm

Premises used: CategoryTheory.Functor.isoWhiskerLeft, CategoryTheory.Iso.symm, CategoryTheory.comonadicAdjunction, CategoryTheory.Comonad.comparisonForget
-- Module: Mathlib.CategoryTheory.Adjunction.Lifting.Right
Goal:
A : Type u₁
B : Type u₂
C : Type u₃
inst : Category.{v₁, u₁} A
inst_1 : Category.{v₂, u₂} B
inst_2 : Category.{v₃, u₃} C
F : Functor.{v₂, v₁, u₂, u₁} B A
inst_3 : ComonadicLeftAdjoint F
L : Functor.{v₃, v₂, u₃, u₂} C B
inst_4 : HasCoreflexiveEqualizers.{v₃, u₃} C
inst_5 : (L ⋙ F).IsLeftAdjoint
L' : C ⥤ (Adjunction.toComonad (R := comonadicRightAdjoint F) (comonadicAdjunction F)).Coalgebra :=
  L ⋙ Comonad.comparison (comonadicAdjunction F)
this : (L' ⋙ (Adjunction.toComonad (R := comonadicRightAdjoint F) (comonadicAdjunction F)).forget).IsLeftAdjoint := ⋯
X : (Adjunction.toComonad (R := comonadicRightAdjoint F) (comonadicAdjunction F)).Coalgebra
simp :
  RegularMono (C := (Adjunction.toComonad (R := comonadicRightAdjoint F) (comonadicAdjunction F)).Coalgebra) (X :=
    Functor.obj (𝟭 (Adjunction.toComonad (R := comonadicRightAdjoint F) (comonadicAdjunction F)).Coalgebra) X) (Y :=
    ((Adjunction.toComonad (R := comonadicRightAdjoint F) (comonadicAdjunction F)).forget ⋙
          (Adjunction.toComonad (R := comonadicRightAdjoint F) (comonadicAdjunction F)).cofree).obj
      X)
    { f := X.a, h := ⋯ :
      X.Hom ((Adjunction.toComonad (R := comonadicRightAdjoint F) (comonadicAdjunction F)).cofree.obj X.A) }
⊢ RegularMono ((Adjunction.toComonad (R := comonadicRightAdjoint F) (comonadicAdjunction F)).adj.unit.app X)

Tactic:
simp only [Comonad.adj_unit]

Premises used: CategoryTheory.Comonad.adj_unit
-- Module: Mathlib.CategoryTheory.Adjunction.Lifting.Right
Goal:
A : Type u₁
B : Type u₂
C : Type u₃
inst : Category.{v₁, u₁} A
inst_1 : Category.{v₂, u₂} B
inst_2 : Category.{v₃, u₃} C
F : Functor.{v₂, v₁, u₂, u₁} B A
inst_3 : ComonadicLeftAdjoint F
L : Functor.{v₃, v₂, u₃, u₂} C B
inst_4 : HasCoreflexiveEqualizers.{v₃, u₃} C
inst_5 : (L ⋙ F).IsLeftAdjoint
L' : C ⥤ (Adjunction.toComonad (R := comonadicRightAdjoint F) (comonadicAdjunction F)).Coalgebra :=
  L ⋙ Comonad.comparison (comonadicAdjunction F)
this : (L' ⋙ (Adjunction.toComonad (R := comonadicRightAdjoint F) (comonadicAdjunction F)).forget).IsLeftAdjoint := ⋯
X : (Adjunction.toComonad (R := comonadicRightAdjoint F) (comonadicAdjunction F)).Coalgebra
⊢ RegularMono (C := (Adjunction.toComonad (R := comonadicRightAdjoint F) (comonadicAdjunction F)).Coalgebra) (X :=
    Functor.obj (𝟭 (Adjunction.toComonad (R := comonadicRightAdjoint F) (comonadicAdjunction F)).Coalgebra) X) (Y :=
    ((Adjunction.toComonad (R := comonadicRightAdjoint F) (comonadicAdjunction F)).forget ⋙
          (Adjunction.toComonad (R := comonadicRightAdjoint F) (comonadicAdjunction F)).cofree).obj
      X)
    { f := X.a, h := ⋯ :
      X.Hom ((Adjunction.toComonad (R := comonadicRightAdjoint F) (comonadicAdjunction F)).cofree.obj X.A) }

Tactic:
exact ⟨_, _, _, _, Comonad.beckCoalgebraEqualizer X⟩
-- Module: Mathlib.CategoryTheory.Adjunction.Lifting.Right
Goal:
A : Type u₁
B : Type u₂
C : Type u₃
inst : Category.{v₁, u₁} A
inst_1 : Category.{v₂, u₂} B
inst_2 : Category.{v₃, u₃} C
F : Functor.{v₂, v₁, u₂, u₁} B A
inst_3 : ComonadicLeftAdjoint F
L : Functor.{v₃, v₂, u₃, u₂} C B
inst_4 : HasCoreflexiveEqualizers.{v₃, u₃} C
inst_5 : (L ⋙ F).IsLeftAdjoint
L' : C ⥤ (Adjunction.toComonad (R := comonadicRightAdjoint F) (comonadicAdjunction F)).Coalgebra :=
  L ⋙ Comonad.comparison (comonadicAdjunction F)
this_1 : (L' ⋙ (Adjunction.toComonad (R := comonadicRightAdjoint F) (comonadicAdjunction F)).forget).IsLeftAdjoint := ⋯
this : (X : (Adjunction.toComonad (R := comonadicRightAdjoint F) (comonadicAdjunction F)).Coalgebra) →
  RegularMono ((Adjunction.toComonad (R := comonadicRightAdjoint F) (comonadicAdjunction F)).adj.unit.app X) :=
  fun (X : (Adjunction.toComonad (R := comonadicRightAdjoint F) (comonadicAdjunction F)).Coalgebra) ↦
    Eq.mpr ⋯
      {
        Z :=
          (Adjunction.toComonad (R := comonadicRightAdjoint F) (comonadicAdjunction F)).cofree.obj
            ((Adjunction.toComonad (R := comonadicRightAdjoint F) (comonadicAdjunction F)).obj X.A),
        left := Comonad.CofreeEqualizer.topMap X, right := Comonad.CofreeEqualizer.bottomMap X, w := ⋯,
        isLimit := Comonad.beckCoalgebraEqualizer X :
        RegularMono (C := (Adjunction.toComonad (R := comonadicRightAdjoint F) (comonadicAdjunction F)).Coalgebra) (X :=
          Functor.obj (𝟭 (Adjunction.toComonad (R := comonadicRightAdjoint F) (comonadicAdjunction F)).Coalgebra) X)
          (Y :=
          ((Adjunction.toComonad (R := comonadicRightAdjoint F) (comonadicAdjunction F)).forget ⋙
                (Adjunction.toComonad (R := comonadicRightAdjoint F) (comonadicAdjunction F)).cofree).obj
            X)
          { f := X.a, h := ⋯ :
            X.Hom ((Adjunction.toComonad (R := comonadicRightAdjoint F) (comonadicAdjunction F)).cofree.obj X.A) } }
⊢ L'.IsLeftAdjoint

Tactic:
isLeftAdjoint_triangle_lift L' (Comonad.adj _) this

Premises used: CategoryTheory.Comonad.adj, CategoryTheory.isLeftAdjoint_triangle_lift
-- Module: Mathlib.CategoryTheory.Adjunction.Lifting.Right
Goal:
A : Type u₁
B : Type u₂
C : Type u₃
inst : Category.{v₁, u₁} A
inst_1 : Category.{v₂, u₂} B
inst_2 : Category.{v₃, u₃} C
F : Functor.{v₂, v₁, u₂, u₁} B A
inst_3 : ComonadicLeftAdjoint F
L : Functor.{v₃, v₂, u₃, u₂} C B
inst_4 : HasCoreflexiveEqualizers.{v₃, u₃} C
inst_5 : (L ⋙ F).IsLeftAdjoint
L' : C ⥤ (Adjunction.toComonad (R := comonadicRightAdjoint F) (comonadicAdjunction F)).Coalgebra :=
  L ⋙ Comonad.comparison (comonadicAdjunction F)
this_1 : (L' ⋙ (Adjunction.toComonad (R := comonadicRightAdjoint F) (comonadicAdjunction F)).forget).IsLeftAdjoint := ⋯
this : (X : (Adjunction.toComonad (R := comonadicRightAdjoint F) (comonadicAdjunction F)).Coalgebra) →
  RegularMono ((Adjunction.toComonad (R := comonadicRightAdjoint F) (comonadicAdjunction F)).adj.unit.app X) :=
  fun (X : (Adjunction.toComonad (R := comonadicRightAdjoint F) (comonadicAdjunction F)).Coalgebra) ↦
    Eq.mpr ⋯
      {
        Z :=
          (Adjunction.toComonad (R := comonadicRightAdjoint F) (comonadicAdjunction F)).cofree.obj
            ((Adjunction.toComonad (R := comonadicRightAdjoint F) (comonadicAdjunction F)).obj X.A),
        left := Comonad.CofreeEqualizer.topMap X, right := Comonad.CofreeEqualizer.bottomMap X, w := ⋯,
        isLimit := Comonad.beckCoalgebraEqualizer X :
        RegularMono (C := (Adjunction.toComonad (R := comonadicRightAdjoint F) (comonadicAdjunction F)).Coalgebra) (X :=
          Functor.obj (𝟭 (Adjunction.toComonad (R := comonadicRightAdjoint F) (comonadicAdjunction F)).Coalgebra) X)
          (Y :=
          ((Adjunction.toComonad (R := comonadicRightAdjoint F) (comonadicAdjunction F)).forget ⋙
                (Adjunction.toComonad (R := comonadicRightAdjoint F) (comonadicAdjunction F)).cofree).obj
            X)
          { f := X.a, h := ⋯ :
            X.Hom ((Adjunction.toComonad (R := comonadicRightAdjoint F) (comonadicAdjunction F)).cofree.obj X.A) } }
⊢ L'.IsLeftAdjoint

Tactic:
exact isLeftAdjoint_triangle_lift L' (Comonad.adj _) this

Premises used: CategoryTheory.Comonad.adj, CategoryTheory.isLeftAdjoint_triangle_lift
-- Module: Mathlib.CategoryTheory.Adjunction.Lifting.Right
Goal:
A : Type u₁
B : Type u₂
C : Type u₃
inst : Category.{v₁, u₁} A
inst_1 : Category.{v₂, u₂} B
inst_2 : Category.{v₃, u₃} C
D : Type u₄
inst_3 : Category.{v₄, u₄} D
Q : Functor.{v₁, v₂, u₁, u₂} A B
V : Functor.{v₂, v₄, u₂, u₄} B D
U : Functor.{v₁, v₃, u₁, u₃} A C
L : Functor.{v₃, v₄, u₃, u₄} C D
comm : U ⋙ L ≅ Q ⋙ V
inst_4 : U.IsLeftAdjoint
inst_5 : V.IsLeftAdjoint
inst_6 : L.IsLeftAdjoint
h :
  (X : B) →
    RegularMono (Y := (V ⋙ V.rightAdjoint).obj X) (NatTrans.app (Adjunction.unit (Adjunction.ofIsLeftAdjoint V)) X)
inst_7 : HasCoreflexiveEqualizers.{v₁, u₁} A
⊢ Q.IsLeftAdjoint

Tactic:
have := ((Adjunction.ofIsLeftAdjoint (U ⋙ L)).ofNatIsoLeft comm).isLeftAdjoint
  isLeftAdjoint_triangle_lift Q (Adjunction.ofIsLeftAdjoint V) h

Premises used: CategoryTheory.Adjunction.ofIsLeftAdjoint, CategoryTheory.Functor.comp, CategoryTheory.Adjunction.isLeftAdjoint, CategoryTheory.isLeftAdjoint_triangle_lift, CategoryTheory.Adjunction.ofNatIsoLeft