awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Adjunction.Lifting.Left
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₃} B C
F : Functor.{v₃, v₂, u₃, u₂} C B
R : Functor.{v₁, v₂, u₁, u₂} A B
F' : Functor.{v₃, v₁, u₃, u₁} C A
adj₁ : F ⊣ U
adj₂ : F' ⊣ R ⋙ U
inst_3 : HasReflexiveCoequalizers.{v₁, u₁} A
h : (X : B) → RegularEpi (adj₁.counit.app X)
Y : A
X : B
f : F'.obj (U.obj X) ⟶ Y
rw :
  U.map (F.map (adj₂.unit.app (U.1 X)) ≫ adj₁.counit.app (R.obj (F'.obj (U.1 X))) ≫ R.map f) =
      U.map (adj₁.counit.app X) ≫
        ((adj₂.homEquiv (U.obj (Functor.obj.{v₂, v₂, u₂, u₂} (𝟭 B) X)) Y :
              Equiv.{v₁ + 1, v₃ + 1} (F'.obj (U.obj (Functor.obj.{v₂, v₂, u₂, u₂} (𝟭 B) X)) ⟶ Y)
                (U.obj (Functor.obj.{v₂, v₂, u₂, u₂} (𝟭 B) X) ⟶ (R ⋙ U).obj Y)) :
            (a : F'.obj (U.obj ((𝟭 B).obj X)) ⟶ Y) → U.obj ((𝟭 B).obj X) ⟶ (R ⋙ U).obj Y)
          f ↔
    Eq (α := U.obj (F.obj (U.obj X)) ⟶ U.obj (Functor.obj.{v₂, v₂, u₂, u₂} (𝟭 B) (R.obj Y)))
      (U.map
        (F.map
            (((adj₂.homEquiv (U.obj X) Y : Equiv.{v₁ + 1, v₃ + 1} (F'.obj (U.obj X) ⟶ Y) (U.obj X ⟶ (R ⋙ U).obj Y)) :
                (a : F'.obj (U.obj X) ⟶ Y) → U.obj X ⟶ (R ⋙ U).obj Y)
              f) ≫
          adj₁.counit.app (R.obj Y)))
      (U.map (adj₁.counit.app X) ≫
        ((adj₂.homEquiv (U.obj X) Y : Equiv.{v₁ + 1, v₃ + 1} (F'.obj (U.obj X) ⟶ Y) (U.obj X ⟶ (R ⋙ U).obj Y)) :
            (a : F'.obj (U.obj X) ⟶ Y) → U.obj X ⟶ (R ⋙ U).obj Y)
          f)
⊢ F'.map (U.map (adj₁.counit.app X)) ≫ f = otherMap R F' adj₁ adj₂ X ≫ f ↔
    Eq (α := U.obj (F.obj (U.obj X)) ⟶ U.obj (Functor.obj.{v₂, v₂, u₂, u₂} (𝟭 B) (R.obj Y)))
      (U.map
        (F.map
            (((adj₂.homEquiv (U.obj X) Y : Equiv.{v₁ + 1, v₃ + 1} (F'.obj (U.obj X) ⟶ Y) (U.obj X ⟶ (R ⋙ U).obj Y)) :
                (a : F'.obj (U.obj X) ⟶ Y) → U.obj X ⟶ (R ⋙ U).obj Y)
              f) ≫
          adj₁.counit.app (R.obj Y)))
      (U.map (adj₁.counit.app X) ≫
        ((adj₂.homEquiv (U.obj X) Y : Equiv.{v₁ + 1, v₃ + 1} (F'.obj (U.obj X) ⟶ Y) (U.obj X ⟶ (R ⋙ U).obj Y)) :
            (a : F'.obj (U.obj X) ⟶ Y) → U.obj X ⟶ (R ⋙ U).obj Y)
          f)

Tactic:
rw [← (adj₂.homEquiv _ _).injective.eq_iff, eq_comm, adj₂.homEquiv_naturality_left,
        otherMap, assoc, adj₂.homEquiv_naturality_left, ← adj₂.counit_naturality,
        adj₂.homEquiv_naturality_left, adj₂.homEquiv_unit, adj₂.right_triangle_components,
        comp_id, Functor.comp_map, ← U.map_comp, assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Adjunction.homEquiv_unit, Function.Injective.eq_iff, CategoryTheory.Adjunction.counit_naturality, CategoryTheory.Category.comp_id, eq_comm, CategoryTheory.LiftLeftAdjoint.otherMap, CategoryTheory.Functor.map_comp, CategoryTheory.Adjunction.right_triangle_components, CategoryTheory.Adjunction.homEquiv, Equiv.injective, CategoryTheory.Functor.comp_map, CategoryTheory.Adjunction.homEquiv_naturality_left
-- Module: Mathlib.CategoryTheory.Adjunction.Lifting.Left
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₃} B C
F : Functor.{v₃, v₂, u₃, u₂} C B
R : Functor.{v₁, v₂, u₁, u₂} A B
F' : Functor.{v₃, v₁, u₃, u₁} C A
adj₁ : F ⊣ U
adj₂ : F' ⊣ R ⋙ U
inst_3 : HasReflexiveCoequalizers.{v₁, u₁} A
h : (X : B) → RegularEpi (adj₁.counit.app X)
Y : A
X : B
f : F'.obj (U.obj X) ⟶ Y
dsimp :
  U.map (F.map (adj₂.unit.app (U.1 X)) ≫ adj₁.counit.app (R.obj (F'.obj (U.1 X))) ≫ R.map f) =
      U.map (adj₁.counit.app X) ≫
        ((adj₂.homEquiv (U.obj X) Y : Equiv.{v₁ + 1, v₃ + 1} (F'.obj (U.obj X) ⟶ Y) (U.obj X ⟶ (R ⋙ U).obj Y)) :
            (a : F'.obj (U.obj X) ⟶ Y) → U.obj X ⟶ U.obj (R.obj Y))
          f ↔
    Eq (α := U.obj (F.obj (U.obj X)) ⟶ U.obj (R.obj Y))
      (U.map
        (F.map
            (((adj₂.homEquiv (U.obj X) Y : Equiv.{v₁ + 1, v₃ + 1} (F'.obj (U.obj X) ⟶ Y) (U.obj X ⟶ (R ⋙ U).obj Y)) :
                (a : F'.obj (U.obj X) ⟶ Y) → U.obj X ⟶ U.obj (R.obj Y))
              f) ≫
          adj₁.counit.app (R.obj Y)))
      (U.map (adj₁.counit.app X) ≫
        ((adj₂.homEquiv (U.obj X) Y : Equiv.{v₁ + 1, v₃ + 1} (F'.obj (U.obj X) ⟶ Y) (U.obj X ⟶ (R ⋙ U).obj Y)) :
            (a : F'.obj (U.obj X) ⟶ Y) → U.obj X ⟶ U.obj (R.obj Y))
          f)
⊢ U.map (F.map (adj₂.unit.app (U.1 X)) ≫ adj₁.counit.app (R.obj (F'.obj (U.1 X))) ≫ R.map f) =
      U.map (adj₁.counit.app X) ≫
        ((adj₂.homEquiv (U.obj (Functor.obj.{v₂, v₂, u₂, u₂} (𝟭 B) X)) Y :
              Equiv.{v₁ + 1, v₃ + 1} (F'.obj (U.obj (Functor.obj.{v₂, v₂, u₂, u₂} (𝟭 B) X)) ⟶ Y)
                (U.obj (Functor.obj.{v₂, v₂, u₂, u₂} (𝟭 B) X) ⟶ (R ⋙ U).obj Y)) :
            (a : F'.obj (U.obj ((𝟭 B).obj X)) ⟶ Y) → U.obj ((𝟭 B).obj X) ⟶ (R ⋙ U).obj Y)
          f ↔
    Eq (α := U.obj (F.obj (U.obj X)) ⟶ U.obj (Functor.obj.{v₂, v₂, u₂, u₂} (𝟭 B) (R.obj Y)))
      (U.map
        (F.map
            (((adj₂.homEquiv (U.obj X) Y : Equiv.{v₁ + 1, v₃ + 1} (F'.obj (U.obj X) ⟶ Y) (U.obj X ⟶ (R ⋙ U).obj Y)) :
                (a : F'.obj (U.obj X) ⟶ Y) → U.obj X ⟶ (R ⋙ U).obj Y)
              f) ≫
          adj₁.counit.app (R.obj Y)))
      (U.map (adj₁.counit.app X) ≫
        ((adj₂.homEquiv (U.obj X) Y : Equiv.{v₁ + 1, v₃ + 1} (F'.obj (U.obj X) ⟶ Y) (U.obj X ⟶ (R ⋙ U).obj Y)) :
            (a : F'.obj (U.obj X) ⟶ Y) → U.obj X ⟶ (R ⋙ U).obj Y)
          f)

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Adjunction.Lifting.Left
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₃} B C
F : Functor.{v₃, v₂, u₃, u₂} C B
R : Functor.{v₁, v₂, u₁, u₂} A B
F' : Functor.{v₃, v₁, u₃, u₁} C A
adj₁ : F ⊣ U
adj₂ : F' ⊣ R ⋙ U
inst_3 : HasReflexiveCoequalizers.{v₁, u₁} A
h : (X : B) → RegularEpi (adj₁.counit.app X)
Y : A
X : B
f : F'.obj (U.obj X) ⟶ Y
rw :
  U.map (F.map (adj₂.unit.app (U.1 X)) ≫ F.map (U.map (R.map f)) ≫ adj₁.counit.app (R.obj Y)) =
      U.map (adj₁.counit.app X) ≫
        ((adj₂.homEquiv (U.obj X) Y : Equiv.{v₁ + 1, v₃ + 1} (F'.obj (U.obj X) ⟶ Y) (U.obj X ⟶ (R ⋙ U).obj Y)) :
            (a : F'.obj (U.obj X) ⟶ Y) → U.obj X ⟶ U.obj (R.obj Y))
          f ↔
    Eq (α := U.obj (F.obj (U.obj X)) ⟶ U.obj (R.obj Y))
      (U.map
        (F.map
            (((adj₂.homEquiv (U.obj X) Y : Equiv.{v₁ + 1, v₃ + 1} (F'.obj (U.obj X) ⟶ Y) (U.obj X ⟶ (R ⋙ U).obj Y)) :
                (a : F'.obj (U.obj X) ⟶ Y) → U.obj X ⟶ U.obj (R.obj Y))
              f) ≫
          adj₁.counit.app (R.obj Y)))
      (U.map (adj₁.counit.app X) ≫
        ((adj₂.homEquiv (U.obj X) Y : Equiv.{v₁ + 1, v₃ + 1} (F'.obj (U.obj X) ⟶ Y) (U.obj X ⟶ (R ⋙ U).obj Y)) :
            (a : F'.obj (U.obj X) ⟶ Y) → U.obj X ⟶ U.obj (R.obj Y))
          f)
⊢ U.map (F.map (adj₂.unit.app (U.1 X)) ≫ adj₁.counit.app (R.obj (F'.obj (U.1 X))) ≫ R.map f) =
      U.map (adj₁.counit.app X) ≫
        ((adj₂.homEquiv (U.obj X) Y : Equiv.{v₁ + 1, v₃ + 1} (F'.obj (U.obj X) ⟶ Y) (U.obj X ⟶ (R ⋙ U).obj Y)) :
            (a : F'.obj (U.obj X) ⟶ Y) → U.obj X ⟶ U.obj (R.obj Y))
          f ↔
    Eq (α := U.obj (F.obj (U.obj X)) ⟶ U.obj (R.obj Y))
      (U.map
        (F.map
            (((adj₂.homEquiv (U.obj X) Y : Equiv.{v₁ + 1, v₃ + 1} (F'.obj (U.obj X) ⟶ Y) (U.obj X ⟶ (R ⋙ U).obj Y)) :
                (a : F'.obj (U.obj X) ⟶ Y) → U.obj X ⟶ U.obj (R.obj Y))
              f) ≫
          adj₁.counit.app (R.obj Y)))
      (U.map (adj₁.counit.app X) ≫
        ((adj₂.homEquiv (U.obj X) Y : Equiv.{v₁ + 1, v₃ + 1} (F'.obj (U.obj X) ⟶ Y) (U.obj X ⟶ (R ⋙ U).obj Y)) :
            (a : F'.obj (U.obj X) ⟶ Y) → U.obj X ⟶ U.obj (R.obj Y))
          f)

Tactic:
rw [← adj₁.counit_naturality]

Premises used: CategoryTheory.Adjunction.counit_naturality
-- Module: Mathlib.CategoryTheory.Adjunction.Lifting.Left
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₃} B C
F : Functor.{v₃, v₂, u₃, u₂} C B
R : Functor.{v₁, v₂, u₁, u₂} A B
F' : Functor.{v₃, v₁, u₃, u₁} C A
adj₁ : F ⊣ U
adj₂ : F' ⊣ R ⋙ U
inst_3 : HasReflexiveCoequalizers.{v₁, u₁} A
h : (X : B) → RegularEpi (adj₁.counit.app X)
Y : A
X : B
f : F'.obj (U.obj X) ⟶ Y
⊢ U.map (F.map (adj₂.unit.app (U.1 X)) ≫ F.map (U.map (R.map f)) ≫ adj₁.counit.app (R.obj Y)) =
      U.map (adj₁.counit.app X) ≫
        ((adj₂.homEquiv (U.obj X) Y : Equiv.{v₁ + 1, v₃ + 1} (F'.obj (U.obj X) ⟶ Y) (U.obj X ⟶ (R ⋙ U).obj Y)) :
            (a : F'.obj (U.obj X) ⟶ Y) → U.obj X ⟶ U.obj (R.obj Y))
          f ↔
    Eq (α := U.obj (F.obj (U.obj X)) ⟶ U.obj (R.obj Y))
      (U.map
        (F.map
            (((adj₂.homEquiv (U.obj X) Y : Equiv.{v₁ + 1, v₃ + 1} (F'.obj (U.obj X) ⟶ Y) (U.obj X ⟶ (R ⋙ U).obj Y)) :
                (a : F'.obj (U.obj X) ⟶ Y) → U.obj X ⟶ U.obj (R.obj Y))
              f) ≫
          adj₁.counit.app (R.obj Y)))
      (U.map (adj₁.counit.app X) ≫
        ((adj₂.homEquiv (U.obj X) Y : Equiv.{v₁ + 1, v₃ + 1} (F'.obj (U.obj X) ⟶ Y) (U.obj X ⟶ (R ⋙ U).obj Y)) :
            (a : F'.obj (U.obj X) ⟶ Y) → U.obj X ⟶ U.obj (R.obj Y))
          f)

Tactic:
simp [dsimp% adj₂.homEquiv_unit _ _ f ]

Premises used: CategoryTheory.Adjunction.homEquiv_unit
-- Module: Mathlib.CategoryTheory.Adjunction.Lifting.Left
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₃} B C
F : Functor.{v₃, v₂, u₃, u₂} C B
R : Functor.{v₁, v₂, u₁, u₂} A B
F' : Functor.{v₃, v₁, u₃, u₁} C A
adj₁ : F ⊣ U
adj₂ : F' ⊣ R ⋙ U
inst_3 : HasReflexiveCoequalizers.{v₁, u₁} A
h : (X : B) → RegularEpi (adj₁.counit.app X)
Y : A
X : B
apply :
  ∀ (a : U.obj X ⟶ U.obj (R.obj Y)),
    U.map (F.map a ≫ adj₁.counit.app (R.obj Y)) = U.map (adj₁.counit.app X) ≫ a ↔
      Eq (α := F.obj (U.obj ((U ⋙ F).obj X)) ⟶ R.obj Y)
        (F.map (U.map (adj₁.counit.app X)) ≫
          ((Equiv.symm (adj₁.homEquiv (U.obj X) (R.obj Y)) :
                Equiv.{v₃ + 1, v₂ + 1} (U.obj X ⟶ U.obj (R.obj Y)) (F.obj (U.obj X) ⟶ R.obj Y)) :
              (a : U.obj X ⟶ U.obj (R.obj Y)) → F.obj (U.obj X) ⟶ R.obj Y)
            a)
        (adj₁.counit.app ((U ⋙ F).obj X) ≫
          ((Equiv.symm (adj₁.homEquiv (U.obj X) (R.obj Y)) :
                Equiv.{v₃ + 1, v₂ + 1} (U.obj X ⟶ U.obj (R.obj Y)) (F.obj (U.obj X) ⟶ R.obj Y)) :
              (a : U.obj X ⟶ U.obj (R.obj Y)) → F.obj (U.obj X) ⟶ R.obj Y)
            a)
⊢ Equiv.{v₃ + 1, max 1 (v₂ + 1)}
    { g : U.obj X ⟶ U.obj (R.obj Y) // U.map (F.map g ≫ adj₁.counit.app (R.obj Y)) = U.map (adj₁.counit.app X) ≫ g }
    { z : F.obj (U.obj X) ⟶ R.obj Y // F.map (U.map (adj₁.counit.app X)) ≫ z = adj₁.counit.app ((U ⋙ F).obj X) ≫ z }

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

Premises used: Equiv.subtypeEquiv, CategoryTheory.Adjunction.homEquiv, Equiv.symm
-- Module: Mathlib.CategoryTheory.Adjunction.Lifting.Left
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₃} B C
F : Functor.{v₃, v₂, u₃, u₂} C B
R : Functor.{v₁, v₂, u₁, u₂} A B
F' : Functor.{v₃, v₁, u₃, u₁} C A
adj₁ : F ⊣ U
adj₂ : F' ⊣ R ⋙ U
inst_3 : HasReflexiveCoequalizers.{v₁, u₁} A
h : (X : B) → RegularEpi (adj₁.counit.app X)
Y : A
X : B
g : U.obj X ⟶ U.obj (R.obj Y)
rw :
  adj₁.counit.app (F.obj (U.obj X)) ≫ F.map g ≫ adj₁.counit.app (R.obj Y) =
      F.map (U.map (adj₁.counit.app X)) ≫ F.map g ≫ adj₁.counit.app (Functor.obj.{v₂, v₂, u₂, u₂} (𝟭 B) (R.obj Y)) ↔
    F.map (U.map (adj₁.counit.app X)) ≫ F.map g ≫ adj₁.counit.app (R.obj Y) =
      adj₁.counit.app ((U ⋙ F).obj X) ≫ F.map g ≫ adj₁.counit.app (R.obj Y)
⊢ U.map (F.map g ≫ adj₁.counit.app (R.obj Y)) = U.map (adj₁.counit.app X) ≫ g ↔
    Eq (α := F.obj (U.obj ((U ⋙ F).obj X)) ⟶ R.obj Y)
      (F.map (U.map (adj₁.counit.app X)) ≫
        ((Equiv.symm (adj₁.homEquiv (U.obj X) (R.obj Y)) :
              Equiv.{v₃ + 1, v₂ + 1} (U.obj X ⟶ U.obj (R.obj Y)) (F.obj (U.obj X) ⟶ R.obj Y)) :
            (a : U.obj X ⟶ U.obj (R.obj Y)) → F.obj (U.obj X) ⟶ R.obj Y)
          g)
      (adj₁.counit.app ((U ⋙ F).obj X) ≫
        ((Equiv.symm (adj₁.homEquiv (U.obj X) (R.obj Y)) :
              Equiv.{v₃ + 1, v₂ + 1} (U.obj X ⟶ U.obj (R.obj Y)) (F.obj (U.obj X) ⟶ R.obj Y)) :
            (a : U.obj X ⟶ U.obj (R.obj Y)) → F.obj (U.obj X) ⟶ R.obj Y)
          g)

Tactic:
rw [← (adj₁.homEquiv _ _).symm.injective.eq_iff, adj₁.homEquiv_counit,
        adj₁.homEquiv_counit, adj₁.homEquiv_counit, F.map_comp, assoc, U.map_comp, F.map_comp,
        assoc, adj₁.counit_naturality, adj₁.counit_naturality_assoc]

Premises used: CategoryTheory.Category.assoc, Function.Injective.eq_iff, CategoryTheory.Adjunction.counit_naturality, CategoryTheory.Functor.map_comp, CategoryTheory.Adjunction.homEquiv_counit, CategoryTheory.Adjunction.counit_naturality_assoc, CategoryTheory.Adjunction.homEquiv, Equiv.injective, Equiv.symm
-- Module: Mathlib.CategoryTheory.Adjunction.Lifting.Left
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₃} B C
F : Functor.{v₃, v₂, u₃, u₂} C B
R : Functor.{v₁, v₂, u₁, u₂} A B
F' : Functor.{v₃, v₁, u₃, u₁} C A
adj₁ : F ⊣ U
adj₂ : F' ⊣ R ⋙ U
inst_3 : HasReflexiveCoequalizers.{v₁, u₁} A
h : (X : B) → RegularEpi (adj₁.counit.app X)
Y : A
X : B
g : U.obj X ⟶ U.obj (R.obj Y)
⊢ adj₁.counit.app (F.obj (U.obj X)) ≫ F.map g ≫ adj₁.counit.app (R.obj Y) =
      F.map (U.map (adj₁.counit.app X)) ≫ F.map g ≫ adj₁.counit.app (Functor.obj.{v₂, v₂, u₂, u₂} (𝟭 B) (R.obj Y)) ↔
    F.map (U.map (adj₁.counit.app X)) ≫ F.map g ≫ adj₁.counit.app (R.obj Y) =
      adj₁.counit.app ((U ⋙ F).obj X) ≫ F.map g ≫ adj₁.counit.app (R.obj Y)

Tactic:
apply eq_comm

Premises used: eq_comm
-- Module: Mathlib.CategoryTheory.Adjunction.Lifting.Left
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₃} B C
F : Functor.{v₃, v₂, u₃, u₂} C B
R : Functor.{v₁, v₂, u₁, u₂} A B
F' : Functor.{v₃, v₁, u₃, u₁} C A
adj₁ : F ⊣ U
adj₂ : F' ⊣ R ⋙ U
inst_3 : HasReflexiveCoequalizers.{v₁, u₁} A
h : (X : B) → RegularEpi (adj₁.counit.app X)
refine :
  ∀ (X : B) (Y Y' : A) (g : Y ⟶ Y') (h_1 : constructLeftAdjointObj R F' adj₁ adj₂ X ⟶ Y),
    Eq.{v₂ + 1} (α := X ⟶ R.obj Y')
      ((((fun (X : B) (Y : A) ↦
                  (constructLeftAdjointEquiv R F' adj₁ adj₂ h Y X :
                    Equiv.{v₁ + 1, v₂ + 1} (constructLeftAdjointObj R F' adj₁ adj₂ X ⟶ Y) (X ⟶ R.obj Y)))
                X Y' :
              Equiv.{v₁ + 1, v₂ + 1} (constructLeftAdjointObj R F' adj₁ adj₂ X ⟶ Y') (X ⟶ R.obj Y')) :
            (a : constructLeftAdjointObj R F' adj₁ adj₂ X ⟶ Y') → X ⟶ R.obj Y')
          (h_1 ≫ g) :
        X ⟶ R.obj Y')
      ((((fun (X : B) (Y : A) ↦
                    (constructLeftAdjointEquiv R F' adj₁ adj₂ h Y X :
                      Equiv.{v₁ + 1, v₂ + 1} (constructLeftAdjointObj R F' adj₁ adj₂ X ⟶ Y) (X ⟶ R.obj Y)))
                  X Y :
                Equiv.{v₁ + 1, v₂ + 1} (constructLeftAdjointObj R F' adj₁ adj₂ X ⟶ Y) (X ⟶ R.obj Y)) :
              (a : constructLeftAdjointObj R F' adj₁ adj₂ X ⟶ Y) → X ⟶ R.obj Y)
            h_1 ≫
          R.map g :
        X ⟶ R.obj Y')
⊢ Functor.{v₂, v₁, u₂, u₁} B A

Tactic:
refine Adjunction.leftAdjointOfEquiv (fun X Y => constructLeftAdjointEquiv R _ adj₁ adj₂ h Y X) ?_

Premises used: CategoryTheory.LiftLeftAdjoint.constructLeftAdjointEquiv, CategoryTheory.Adjunction.leftAdjointOfEquiv
-- Module: Mathlib.CategoryTheory.Adjunction.Lifting.Left
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₃} B C
inst_3 : MonadicRightAdjoint U
R : Functor.{v₁, v₂, u₁, u₂} A B
inst_4 : HasReflexiveCoequalizers.{v₁, u₁} A
inst_5 : (R ⋙ U).IsRightAdjoint
R' : A ⥤ (Adjunction.toMonad (L := monadicLeftAdjoint U) (monadicAdjunction U)).Algebra :=
  R ⋙ Monad.comparison (monadicAdjunction U)
rsuffices : R'.IsRightAdjoint → R.IsRightAdjoint
rsuffices₁ : R'.IsRightAdjoint
⊢ R.IsRightAdjoint

Tactic:
rsuffices : R'.IsRightAdjoint

Premises used: CategoryTheory.Functor.IsRightAdjoint
-- Module: Mathlib.CategoryTheory.Adjunction.Lifting.Left
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₃} B C
inst_3 : MonadicRightAdjoint U
R : Functor.{v₁, v₂, u₁, u₂} A B
inst_4 : HasReflexiveCoequalizers.{v₁, u₁} A
inst_5 : (R ⋙ U).IsRightAdjoint
R' : A ⥤ (Adjunction.toMonad (L := monadicLeftAdjoint U) (monadicAdjunction U)).Algebra :=
  R ⋙ Monad.comparison (monadicAdjunction U)
this : R'.IsRightAdjoint
⊢ (R' ⋙ Functor.inv (Monad.comparison (monadicAdjunction U))).IsRightAdjoint

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Adjunction.Lifting.Left
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₃} B C
inst_3 : MonadicRightAdjoint U
R : Functor.{v₁, v₂, u₁, u₂} A B
inst_4 : HasReflexiveCoequalizers.{v₁, u₁} A
inst_5 : (R ⋙ U).IsRightAdjoint
R' : A ⥤ (Adjunction.toMonad (L := monadicLeftAdjoint U) (monadicAdjunction U)).Algebra :=
  R ⋙ Monad.comparison (monadicAdjunction U)
this_1 : R'.IsRightAdjoint
this : (R' ⋙ Functor.inv (Monad.comparison (monadicAdjunction U))).IsRightAdjoint := ⋯
⊢ R.IsRightAdjoint

Tactic:
((Adjunction.ofIsRightAdjoint
      (R' ⋙ (Monad.comparison (monadicAdjunction U)).inv)).ofNatIsoRight ?_).isRightAdjoint

Premises used: CategoryTheory.Functor.comp, CategoryTheory.Monad.comparison, CategoryTheory.Adjunction.isRightAdjoint, CategoryTheory.Functor.inv, CategoryTheory.Adjunction.ofIsRightAdjoint, CategoryTheory.monadicAdjunction, CategoryTheory.Adjunction.ofNatIsoRight
-- Module: Mathlib.CategoryTheory.Adjunction.Lifting.Left
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₃} B C
inst_3 : MonadicRightAdjoint U
R : Functor.{v₁, v₂, u₁, u₂} A B
inst_4 : HasReflexiveCoequalizers.{v₁, u₁} A
inst_5 : (R ⋙ U).IsRightAdjoint
R' : A ⥤ (Adjunction.toMonad (L := monadicLeftAdjoint U) (monadicAdjunction U)).Algebra :=
  R ⋙ Monad.comparison (monadicAdjunction U)
this_1 : R'.IsRightAdjoint
this : (R' ⋙ Functor.inv (Monad.comparison (monadicAdjunction U))).IsRightAdjoint := ⋯
refine : R' ⋙ Functor.inv (Monad.comparison (monadicAdjunction U)) ≅ R
⊢ R.IsRightAdjoint

Tactic:
refine ((Adjunction.ofIsRightAdjoint
      (R' ⋙ (Monad.comparison (monadicAdjunction U)).inv)).ofNatIsoRight ?_).isRightAdjoint

Premises used: CategoryTheory.Functor.comp, CategoryTheory.Monad.comparison, CategoryTheory.Adjunction.isRightAdjoint, CategoryTheory.Functor.inv, CategoryTheory.Adjunction.ofIsRightAdjoint, CategoryTheory.monadicAdjunction, CategoryTheory.Adjunction.ofNatIsoRight
-- Module: Mathlib.CategoryTheory.Adjunction.Lifting.Left
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₃} B C
inst_3 : MonadicRightAdjoint U
R : Functor.{v₁, v₂, u₁, u₂} A B
inst_4 : HasReflexiveCoequalizers.{v₁, u₁} A
inst_5 : (R ⋙ U).IsRightAdjoint
R' : A ⥤ (Adjunction.toMonad (L := monadicLeftAdjoint U) (monadicAdjunction U)).Algebra :=
  R ⋙ Monad.comparison (monadicAdjunction U)
this_1 : R'.IsRightAdjoint
this : (R' ⋙ Functor.inv (Monad.comparison (monadicAdjunction U))).IsRightAdjoint := ⋯
⊢ R' ⋙ Functor.inv (Monad.comparison (monadicAdjunction U)) ≅ R

Tactic:
exact Functor.isoWhiskerLeft R (Monad.comparison _).asEquivalence.unitIso.symm ≪≫ R.rightUnitor

Premises used: CategoryTheory.Equivalence.unitIso, CategoryTheory.Functor.rightUnitor, CategoryTheory.Monad.comparison, CategoryTheory.Functor.asEquivalence, CategoryTheory.Functor.isoWhiskerLeft, CategoryTheory.Iso.symm
-- Module: Mathlib.CategoryTheory.Adjunction.Lifting.Left
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₃} B C
inst_3 : MonadicRightAdjoint U
R : Functor.{v₁, v₂, u₁, u₂} A B
inst_4 : HasReflexiveCoequalizers.{v₁, u₁} A
inst_5 : (R ⋙ U).IsRightAdjoint
R' : A ⥤ (Adjunction.toMonad (L := monadicLeftAdjoint U) (monadicAdjunction U)).Algebra :=
  R ⋙ Monad.comparison (monadicAdjunction U)
⊢ (R' ⋙ (Adjunction.toMonad (L := monadicLeftAdjoint U) (monadicAdjunction U)).forget).IsRightAdjoint

Tactic:
((Adjunction.ofIsRightAdjoint (R ⋙ U)).ofNatIsoRight ?_).isRightAdjoint

Premises used: CategoryTheory.Functor.comp, CategoryTheory.Adjunction.isRightAdjoint, CategoryTheory.Adjunction.ofIsRightAdjoint, CategoryTheory.Adjunction.ofNatIsoRight
-- Module: Mathlib.CategoryTheory.Adjunction.Lifting.Left
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₃} B C
inst_3 : MonadicRightAdjoint U
R : Functor.{v₁, v₂, u₁, u₂} A B
inst_4 : HasReflexiveCoequalizers.{v₁, u₁} A
inst_5 : (R ⋙ U).IsRightAdjoint
R' : A ⥤ (Adjunction.toMonad (L := monadicLeftAdjoint U) (monadicAdjunction U)).Algebra :=
  R ⋙ Monad.comparison (monadicAdjunction U)
refine : R ⋙ U ≅ R' ⋙ (Adjunction.toMonad (L := monadicLeftAdjoint U) (monadicAdjunction U)).forget
⊢ (R' ⋙ (Adjunction.toMonad (L := monadicLeftAdjoint U) (monadicAdjunction U)).forget).IsRightAdjoint

Tactic:
refine ((Adjunction.ofIsRightAdjoint (R ⋙ U)).ofNatIsoRight ?_).isRightAdjoint

Premises used: CategoryTheory.Functor.comp, CategoryTheory.Adjunction.isRightAdjoint, CategoryTheory.Adjunction.ofIsRightAdjoint, CategoryTheory.Adjunction.ofNatIsoRight
-- Module: Mathlib.CategoryTheory.Adjunction.Lifting.Left
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₃} B C
inst_3 : MonadicRightAdjoint U
R : Functor.{v₁, v₂, u₁, u₂} A B
inst_4 : HasReflexiveCoequalizers.{v₁, u₁} A
inst_5 : (R ⋙ U).IsRightAdjoint
R' : A ⥤ (Adjunction.toMonad (L := monadicLeftAdjoint U) (monadicAdjunction U)).Algebra :=
  R ⋙ Monad.comparison (monadicAdjunction U)
⊢ R ⋙ U ≅ R' ⋙ (Adjunction.toMonad (L := monadicLeftAdjoint U) (monadicAdjunction U)).forget

Tactic:
exact Functor.isoWhiskerLeft R (Monad.comparisonForget (monadicAdjunction U)).symm

Premises used: CategoryTheory.Functor.isoWhiskerLeft, CategoryTheory.Monad.comparisonForget, CategoryTheory.Iso.symm, CategoryTheory.monadicAdjunction
-- Module: Mathlib.CategoryTheory.Adjunction.Lifting.Left
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₃} B C
inst_3 : MonadicRightAdjoint U
R : Functor.{v₁, v₂, u₁, u₂} A B
inst_4 : HasReflexiveCoequalizers.{v₁, u₁} A
inst_5 : (R ⋙ U).IsRightAdjoint
R' : A ⥤ (Adjunction.toMonad (L := monadicLeftAdjoint U) (monadicAdjunction U)).Algebra :=
  R ⋙ Monad.comparison (monadicAdjunction U)
this : (R' ⋙ (Adjunction.toMonad (L := monadicLeftAdjoint U) (monadicAdjunction U)).forget).IsRightAdjoint := ⋯
X : (Adjunction.toMonad (L := monadicLeftAdjoint U) (monadicAdjunction U)).Algebra
simp :
  RegularEpi (C := (Adjunction.toMonad (L := monadicLeftAdjoint U) (monadicAdjunction U)).Algebra) (X :=
    ((Adjunction.toMonad (L := monadicLeftAdjoint U) (monadicAdjunction U)).forget ⋙
          (Adjunction.toMonad (L := monadicLeftAdjoint U) (monadicAdjunction U)).free).obj
      X)
    (Y := Functor.obj (𝟭 (Adjunction.toMonad (L := monadicLeftAdjoint U) (monadicAdjunction U)).Algebra) X)
    { f := X.a, h := ⋯ : ((Adjunction.toMonad (L := monadicLeftAdjoint U) (monadicAdjunction U)).free.obj X.A).Hom X }
⊢ RegularEpi ((Adjunction.toMonad (L := monadicLeftAdjoint U) (monadicAdjunction U)).adj.counit.app X)

Tactic:
simp only [Monad.adj_counit]

Premises used: CategoryTheory.Monad.adj_counit