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
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
⊢ 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 }

Tactic:
exact ⟨_, _, _, _, Monad.beckAlgebraCoequalizer X⟩
-- 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' ⋙ (Adjunction.toMonad (L := monadicLeftAdjoint U) (monadicAdjunction U)).forget).IsRightAdjoint := ⋯
this : (X : (Adjunction.toMonad (L := monadicLeftAdjoint U) (monadicAdjunction U)).Algebra) →
  RegularEpi ((Adjunction.toMonad (L := monadicLeftAdjoint U) (monadicAdjunction U)).adj.counit.app X) :=
  fun (X : (Adjunction.toMonad (L := monadicLeftAdjoint U) (monadicAdjunction U)).Algebra) ↦
    Eq.mpr ⋯
      {
        W :=
          (Adjunction.toMonad (L := monadicLeftAdjoint U) (monadicAdjunction U)).free.obj
            ((Adjunction.toMonad (L := monadicLeftAdjoint U) (monadicAdjunction U)).obj X.A),
        left := Monad.FreeCoequalizer.topMap X, right := Monad.FreeCoequalizer.bottomMap X, w := ⋯,
        isColimit := Monad.beckAlgebraCoequalizer X :
        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 } }
⊢ R'.IsRightAdjoint

Tactic:
isRightAdjoint_triangle_lift R' (Monad.adj _) this

Premises used: CategoryTheory.Monad.adj, CategoryTheory.isRightAdjoint_triangle_lift
-- 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' ⋙ (Adjunction.toMonad (L := monadicLeftAdjoint U) (monadicAdjunction U)).forget).IsRightAdjoint := ⋯
this : (X : (Adjunction.toMonad (L := monadicLeftAdjoint U) (monadicAdjunction U)).Algebra) →
  RegularEpi ((Adjunction.toMonad (L := monadicLeftAdjoint U) (monadicAdjunction U)).adj.counit.app X) :=
  fun (X : (Adjunction.toMonad (L := monadicLeftAdjoint U) (monadicAdjunction U)).Algebra) ↦
    Eq.mpr ⋯
      {
        W :=
          (Adjunction.toMonad (L := monadicLeftAdjoint U) (monadicAdjunction U)).free.obj
            ((Adjunction.toMonad (L := monadicLeftAdjoint U) (monadicAdjunction U)).obj X.A),
        left := Monad.FreeCoequalizer.topMap X, right := Monad.FreeCoequalizer.bottomMap X, w := ⋯,
        isColimit := Monad.beckAlgebraCoequalizer X :
        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 } }
⊢ R'.IsRightAdjoint

Tactic:
exact isRightAdjoint_triangle_lift R' (Monad.adj _) this

Premises used: CategoryTheory.Monad.adj, CategoryTheory.isRightAdjoint_triangle_lift
-- 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
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
R : Functor.{v₃, v₄, u₃, u₄} C D
comm : U ⋙ R ≅ Q ⋙ V
inst_4 : U.IsRightAdjoint
inst_5 : V.IsRightAdjoint
inst_6 : R.IsRightAdjoint
h :
  (X : B) →
    RegularEpi (X := (V ⋙ V.leftAdjoint).obj X) (NatTrans.app (Adjunction.counit (Adjunction.ofIsRightAdjoint V)) X)
inst_7 : HasReflexiveCoequalizers.{v₁, u₁} A
⊢ Q.IsRightAdjoint

Tactic:
have := ((Adjunction.ofIsRightAdjoint (U ⋙ R)).ofNatIsoRight comm).isRightAdjoint
  isRightAdjoint_triangle_lift Q (Adjunction.ofIsRightAdjoint V) h

Premises used: CategoryTheory.Functor.comp, CategoryTheory.Adjunction.isRightAdjoint, CategoryTheory.isRightAdjoint_triangle_lift, 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
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
R : Functor.{v₃, v₄, u₃, u₄} C D
comm : U ⋙ R ≅ Q ⋙ V
inst_4 : U.IsRightAdjoint
inst_5 : MonadicRightAdjoint V
inst_6 : R.IsRightAdjoint
inst_7 : HasReflexiveCoequalizers.{v₁, u₁} A
⊢ Q.IsRightAdjoint

Tactic:
have := ((Adjunction.ofIsRightAdjoint (U ⋙ R)).ofNatIsoRight comm).isRightAdjoint
  isRightAdjoint_triangle_lift_monadic V

Premises used: CategoryTheory.isRightAdjoint_triangle_lift_monadic, CategoryTheory.Functor.comp, CategoryTheory.Adjunction.isRightAdjoint, CategoryTheory.Adjunction.ofIsRightAdjoint, CategoryTheory.Adjunction.ofNatIsoRight
-- 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'
h : (X : B) → RegularMono (adj₁.unit.app X)
X : B
s : Fork (U.map (F.map (adj₁.unit.app X))) (adj₁.unit.app ((F ⋙ U).obj X))
⊢ ∀ (Y : B), Mono (adj₁.unit.app Y)

Tactic:
have := fun Y ↦ h Y |>.mono
-- 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'
h : (X : B) → RegularMono (adj₁.unit.app X)
X : B
s : Fork (U.map (F.map (adj₁.unit.app X))) (adj₁.unit.app ((F ⋙ U).obj X))
this : ∀ (Y : B), Mono (adj₁.unit.app Y)
refine_1 : s.ι ≫ (h X).left = s.ι ≫ (h X).right
refine_2 : (↑((h X).lift' s.ι ⋯) : s.pt ⟶ (𝟭 B).obj X) ≫ (Fork.ofι (adj₁.unit.app X) ⋯).ι = s.ι
refine_3 :
  ∀ {m : s.pt ⟶ (Fork.ofι (adj₁.unit.app X) ⋯).pt},
    m ≫ (Fork.ofι (adj₁.unit.app X) ⋯).ι = s.ι → m = (↑((h X).lift' s.ι ⋯) : s.pt ⟶ (𝟭 B).obj X)
⊢ { l : s.pt ⟶ (Fork.ofι (adj₁.unit.app X) ⋯).pt //
    l ≫ (Fork.ofι (adj₁.unit.app X) ⋯).ι = s.ι ∧
      ∀ {m : s.pt ⟶ (Fork.ofι (adj₁.unit.app X) ⋯).pt}, m ≫ (Fork.ofι (adj₁.unit.app X) ⋯).ι = s.ι → m = l }

Tactic:
refine ⟨((h X).lift' s.ι ?_).1, ?_, ?_⟩
-- 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'
h : (X : B) → RegularMono (adj₁.unit.app X)
X : B
s : Fork (U.map (F.map (adj₁.unit.app X))) (adj₁.unit.app ((F ⋙ U).obj X))
this : ∀ (Y : B), Mono (adj₁.unit.app Y)
refine_1 : s.ι ≫ adj₁.unit.app ((F ⋙ U).obj X) ≫ U.map (F.map (h X).left) = (s.ι ≫ (h X).right) ≫ adj₁.unit.app (h X).Z
⊢ s.ι ≫ (h X).left = s.ι ≫ (h X).right

Tactic:
rw [← cancel_mono (adj₁.unit.app ((h X).Z)), assoc, ← adj₁.unit_naturality (h _).left]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Adjunction.unit, CategoryTheory.cancel_mono, CategoryTheory.RegularMono.left, CategoryTheory.RegularMono.Z, CategoryTheory.Adjunction.unit_naturality, CategoryTheory.NatTrans.app
-- 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'
h : (X : B) → RegularMono (adj₁.unit.app X)
X : B
s : Fork (U.map (F.map (adj₁.unit.app X))) (adj₁.unit.app ((F ⋙ U).obj X))
this : ∀ (Y : B), Mono (adj₁.unit.app Y)
refine_1 :
  s.ι ≫ adj₁.unit.app (U.obj (F.obj X)) ≫ U.map (F.map (h X).left) = (s.ι ≫ (h X).right) ≫ adj₁.unit.app (h X).Z
⊢ s.ι ≫ adj₁.unit.app ((F ⋙ U).obj X) ≫ U.map (F.map (h X).left) = (s.ι ≫ (h X).right) ≫ adj₁.unit.app (h X).Z

Tactic:
dsimp only [Functor.comp_obj]

Premises used: CategoryTheory.Functor.comp_obj
-- 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'
h : (X : B) → RegularMono (adj₁.unit.app X)
X : B
s : Fork (U.map (F.map (adj₁.unit.app X))) (adj₁.unit.app ((F ⋙ U).obj X))
this : ∀ (Y : B), Mono (adj₁.unit.app Y)
⊢ s.ι ≫ U.map (F.map (adj₁.unit.app X)) = s.ι ≫ adj₁.unit.app ((F ⋙ U).obj X)

Tactic:
have := s.condition
-- 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'
h : (X : B) → RegularMono (adj₁.unit.app X)
X : B
s : Fork (U.map (F.map (adj₁.unit.app X))) (adj₁.unit.app ((F ⋙ U).obj X))
this_1 : ∀ (Y : B), Mono (adj₁.unit.app Y)
this : s.ι ≫ U.map (F.map (adj₁.unit.app X)) = s.ι ≫ adj₁.unit.app (U.obj (F.obj X))
refine_1 :
  (s.ι ≫ adj₁.unit.app (U.obj (F.obj X))) ≫ U.map (F.map (h X).left) = (s.ι ≫ (h X).right) ≫ adj₁.unit.app (h X).Z
refine_1₁ :
  (s.ι ≫ U.map (F.map (adj₁.unit.app X))) ≫ U.map (F.map (h X).left) = (s.ι ≫ (h X).right) ≫ adj₁.unit.app (h X).Z
refine_1₂ :
  s.ι ≫ U.map (F.map (adj₁.unit.app X)) ≫ U.map (F.map (h X).left) = (s.ι ≫ (h X).right) ≫ adj₁.unit.app (h X).Z
refine_1₃ : s.ι ≫ U.map (F.map (adj₁.unit.app X) ≫ F.map (h X).left) = (s.ι ≫ (h X).right) ≫ adj₁.unit.app (h X).Z
refine_1₄ : s.ι ≫ U.map (F.map (adj₁.unit.app X ≫ (h X).left)) = (s.ι ≫ (h X).right) ≫ adj₁.unit.app (h X).Z
refine_1₅ : s.ι ≫ U.map (F.map (adj₁.unit.app X ≫ (h X).right)) = (s.ι ≫ (h X).right) ≫ adj₁.unit.app (h X).Z
refine_1₆ : s.ι ≫ U.map (F.map (adj₁.unit.app X) ≫ F.map (h X).right) = (s.ι ≫ (h X).right) ≫ adj₁.unit.app (h X).Z
refine_1₇ :
  s.ι ≫ U.map (F.map (adj₁.unit.app X)) ≫ U.map (F.map (h X).right) = (s.ι ≫ (h X).right) ≫ adj₁.unit.app (h X).Z
refine_1₈ :
  s.ι ≫ adj₁.unit.app ((F ⋙ U).obj X) ≫ U.map (F.map (h X).right) = (s.ι ≫ (h X).right) ≫ adj₁.unit.app (h X).Z
refine_1₉ : s.ι ≫ adj₁.unit.app ((F ⋙ U).obj X) ≫ U.map (F.map (h X).right) = s.ι ≫ (h X).right ≫ adj₁.unit.app (h X).Z
refine_1₁₀ refine_1₁₁ :
  s.ι ≫ adj₁.unit.app ((F ⋙ U).obj X) ≫ U.map (F.map (h X).right) =
    s.ι ≫ adj₁.unit.app ((F ⋙ U).obj X) ≫ U.map (F.map (h X).right)
⊢ s.ι ≫ adj₁.unit.app (U.obj (F.obj X)) ≫ U.map (F.map (h X).left) = (s.ι ≫ (h X).right) ≫ adj₁.unit.app (h X).Z

Tactic:
rw [← assoc, ← this, assoc, ← U.map_comp, ← F.map_comp, RegularMono.w, F.map_comp,
        U.map_comp, s.condition_assoc, assoc, ← adj₁.unit_naturality (h _).right]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.RegularMono.w, CategoryTheory.Adjunction.unit_naturality, CategoryTheory.Functor.map_comp, CategoryTheory.RegularMono.right, CategoryTheory.Limits.Fork.condition_assoc
-- 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'
h : (X : B) → RegularMono (adj₁.unit.app X)
X : B
s : Fork (U.map (F.map (adj₁.unit.app X))) (adj₁.unit.app ((F ⋙ U).obj X))
this : ∀ (Y : B), Mono (adj₁.unit.app Y)
⊢ (↑((h X).lift' s.ι ⋯) : s.pt ⟶ (𝟭 B).obj X) ≫ (Fork.ofι (adj₁.unit.app X) ⋯).ι = s.ι

Tactic:
apply ((h X).lift' s.ι _).2

Premises used: CategoryTheory.Limits.Fork.ι, CategoryTheory.RegularMono.lift', Subtype.property
-- 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'
h : (X : B) → RegularMono (adj₁.unit.app X)
X : B
s : Fork (U.map (F.map (adj₁.unit.app X))) (adj₁.unit.app ((F ⋙ U).obj X))
this : ∀ (Y : B), Mono (adj₁.unit.app Y)
m : s.pt ⟶ (Fork.ofι (adj₁.unit.app X) ⋯).pt
hm : m ≫ (Fork.ofι (adj₁.unit.app X) ⋯).ι = s.ι
refine_3 : m ≫ adj₁.unit.app X = (↑((h X).lift' s.ι ⋯) : s.pt ⟶ (𝟭 B).obj X) ≫ adj₁.unit.app X
⊢ m = (↑((h X).lift' s.ι ⋯) : s.pt ⟶ (𝟭 B).obj X)

Tactic:
rw [← cancel_mono (adj₁.unit.app X)]

Premises used: CategoryTheory.Adjunction.unit, CategoryTheory.cancel_mono, CategoryTheory.NatTrans.app
-- 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'
h : (X : B) → RegularMono (adj₁.unit.app X)
X : B
s : Fork (U.map (F.map (adj₁.unit.app X))) (adj₁.unit.app ((F ⋙ U).obj X))
this : ∀ (Y : B), Mono (adj₁.unit.app Y)
m : s.pt ⟶ (Fork.ofι (adj₁.unit.app X) ⋯).pt
hm : m ≫ (Fork.ofι (adj₁.unit.app X) ⋯).ι = s.ι
⊢ m ≫ adj₁.unit.app X = (↑((h X).lift' s.ι ⋯) : s.pt ⟶ (𝟭 B).obj X) ≫ adj₁.unit.app X

Tactic:
apply hm.trans ((h X).lift' s.ι _).2.symm

Premises used: CategoryTheory.Limits.Fork.ι, Eq.symm, CategoryTheory.RegularMono.lift', Eq.trans, Subtype.property
-- 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'
X : B
⊢ U'.map (F.map (adj₁.unit.app X)) ≫ U'.map (adj₁.counit.app (F.obj X)) =
    𝟙 (U'.obj (F.obj (Functor.obj.{v₂, v₂, u₂, u₂} (𝟭 B) X)))

Tactic:
simp [← Functor.map_comp]

Premises used: CategoryTheory.Functor.map_comp
-- 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'
X : B
simp :
  adj₂.unit.app (U'.1 (F.obj X)) ≫
      U'.map
        (F.map (adj₁.unit.app (L.1 (U'.1 (F.obj X))) ≫ U.map (adj₂.counit.app (F.obj X))) ≫ adj₁.counit.app (F.obj X)) =
    𝟙 (U'.obj (F.obj (Functor.obj.{v₂, v₂, u₂, u₂} (𝟭 B) X)))
⊢ otherMap L U' adj₁ adj₂ X ≫ U'.map (adj₁.counit.app (F.obj X)) =
    𝟙 (U'.obj (F.obj (Functor.obj.{v₂, v₂, u₂, u₂} (𝟭 B) X)))

Tactic:
simp only [otherMap, assoc, ← Functor.map_comp]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.LiftRightAdjoint.otherMap, CategoryTheory.Functor.map_comp
-- 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'
X : B
⊢ adj₂.unit.app (U'.1 (F.obj X)) ≫
      U'.map
        (F.map (adj₁.unit.app (L.1 (U'.1 (F.obj X))) ≫ U.map (adj₂.counit.app (F.obj X))) ≫ adj₁.counit.app (F.obj X)) =
    𝟙 (U'.obj (F.obj (Functor.obj.{v₂, v₂, u₂, u₂} (𝟭 B) 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)
Y : C
X : B
apply :
  ∀ (a : Y ⟶ U'.obj (F.obj X)),
    a ≫ U'.map (F.map (adj₁.unit.app X)) = a ≫ otherMap L U' adj₁ adj₂ X ↔
      Eq (α := F.obj (Functor.obj.{v₂, v₂, u₂, u₂} (𝟭 B) (L.obj Y)) ⟶ F.obj (U.obj (F.obj X)))
        (F.map
          (adj₁.unit.app (L.obj Y) ≫
            U.map
              (((Equiv.symm (adj₂.homEquiv Y (F.obj X)) :
                    Equiv.{v₃ + 1, v₁ + 1} (Y ⟶ U'.obj (F.obj X)) ((L ⋙ F).obj Y ⟶ F.obj X)) :
                  (a : Y ⟶ U'.obj (F.obj X)) → (L ⋙ F).obj Y ⟶ F.obj X)
                a)))
        (((Equiv.symm (adj₂.homEquiv Y (F.obj X)) :
                Equiv.{v₃ + 1, v₁ + 1} (Y ⟶ U'.obj (F.obj X)) ((L ⋙ F).obj Y ⟶ F.obj X)) :
              (a : Y ⟶ U'.obj (F.obj X)) → (L ⋙ F).obj Y ⟶ F.obj X)
            a ≫
          F.map (adj₁.unit.app X))
⊢ Equiv.{v₃ + 1, max 1 (v₁ + 1)}
    { f : Y ⟶ U'.obj (F.obj X) // f ≫ U'.map (F.map (adj₁.unit.app X)) = f ≫ otherMap L U' adj₁ adj₂ X }
    { 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) }

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

Premises used: Equiv.subtypeEquiv, CategoryTheory.Adjunction.homEquiv, 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 : (X : B) → RegularMono (adj₁.unit.app X)
Y : C
X : B
f : Y ⟶ U'.obj (F.obj X)
rw :
  adj₂.unit.app Y ≫
        U'.map ((L ⋙ F).map f) ≫
          U'.map (F.map (adj₁.unit.app (L.1 (U'.1 (F.obj X))) ≫ U.map (adj₂.counit.app (F.obj X)))) =
      f ≫ U'.map (F.map (adj₁.unit.app X)) ↔
    adj₂.unit.app Y ≫ U'.map (F.map (adj₁.unit.app (L.obj Y) ≫ U.map ((L ⋙ F).map f ≫ adj₂.counit.app (F.obj X)))) =
      ((adj₂.homEquiv Y (F.obj (U.obj (F.obj X))) :
            Equiv.{v₁ + 1, v₃ + 1} ((L ⋙ F).obj Y ⟶ F.obj (U.obj (F.obj X))) (Y ⟶ U'.obj (F.obj (U.obj (F.obj X))))) :
          (a : (L ⋙ F).obj Y ⟶ F.obj (U.obj (F.obj X))) → Y ⟶ U'.obj (F.obj (U.obj (F.obj X))))
        (((Equiv.symm (adj₂.homEquiv Y (F.obj ((F ⋙ U).obj X))) :
              Equiv.{v₃ + 1, v₁ + 1} (Y ⟶ U'.obj (F.obj ((F ⋙ U).obj X))) ((L ⋙ F).obj Y ⟶ F.obj ((F ⋙ U).obj X))) :
            (a : Y ⟶ U'.obj (F.obj ((F ⋙ U).obj X))) → (L ⋙ F).obj Y ⟶ F.obj ((F ⋙ U).obj X))
          (f ≫ U'.map (F.map (adj₁.unit.app X))))
⊢ f ≫ U'.map (F.map (adj₁.unit.app X)) = f ≫ otherMap L U' adj₁ adj₂ X ↔
    Eq (α := F.obj (Functor.obj.{v₂, v₂, u₂, u₂} (𝟭 B) (L.obj Y)) ⟶ F.obj (U.obj (F.obj X)))
      (F.map
        (adj₁.unit.app (L.obj Y) ≫
          U.map
            (((Equiv.symm (adj₂.homEquiv Y (F.obj X)) :
                  Equiv.{v₃ + 1, v₁ + 1} (Y ⟶ U'.obj (F.obj X)) ((L ⋙ F).obj Y ⟶ F.obj X)) :
                (a : Y ⟶ U'.obj (F.obj X)) → (L ⋙ F).obj Y ⟶ F.obj X)
              f)))
      (((Equiv.symm (adj₂.homEquiv Y (F.obj X)) :
              Equiv.{v₃ + 1, v₁ + 1} (Y ⟶ U'.obj (F.obj X)) ((L ⋙ F).obj Y ⟶ F.obj X)) :
            (a : Y ⟶ U'.obj (F.obj X)) → (L ⋙ F).obj Y ⟶ F.obj X)
          f ≫
        F.map (adj₁.unit.app X))

Tactic:
rw [← (adj₂.homEquiv _ _).injective.eq_iff, eq_comm, otherMap,
        ← adj₂.homEquiv_naturality_right_symm, adj₂.homEquiv_unit, ← adj₂.unit_naturality_assoc,
        adj₂.homEquiv_counit]

Premises used: CategoryTheory.Adjunction.homEquiv_unit, Function.Injective.eq_iff, eq_comm, CategoryTheory.LiftRightAdjoint.otherMap, CategoryTheory.Adjunction.homEquiv_naturality_right_symm, CategoryTheory.Adjunction.homEquiv_counit, CategoryTheory.Adjunction.homEquiv, Equiv.injective, CategoryTheory.Adjunction.unit_naturality_assoc
-- 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
f : Y ⟶ U'.obj (F.obj X)
⊢ adj₂.unit.app Y ≫
        U'.map ((L ⋙ F).map f) ≫
          U'.map (F.map (adj₁.unit.app (L.1 (U'.1 (F.obj X))) ≫ U.map (adj₂.counit.app (F.obj X)))) =
      f ≫ U'.map (F.map (adj₁.unit.app X)) ↔
    adj₂.unit.app Y ≫ U'.map (F.map (adj₁.unit.app (L.obj Y) ≫ U.map ((L ⋙ F).map f ≫ adj₂.counit.app (F.obj X)))) =
      ((adj₂.homEquiv Y (F.obj (U.obj (F.obj X))) :
            Equiv.{v₁ + 1, v₃ + 1} ((L ⋙ F).obj Y ⟶ F.obj (U.obj (F.obj X))) (Y ⟶ U'.obj (F.obj (U.obj (F.obj X))))) :
          (a : (L ⋙ F).obj Y ⟶ F.obj (U.obj (F.obj X))) → Y ⟶ U'.obj (F.obj (U.obj (F.obj X))))
        (((Equiv.symm (adj₂.homEquiv Y (F.obj ((F ⋙ U).obj X))) :
              Equiv.{v₃ + 1, v₁ + 1} (Y ⟶ U'.obj (F.obj ((F ⋙ U).obj X))) ((L ⋙ F).obj Y ⟶ F.obj ((F ⋙ U).obj X))) :
            (a : Y ⟶ U'.obj (F.obj ((F ⋙ U).obj X))) → (L ⋙ F).obj Y ⟶ F.obj ((F ⋙ U).obj X))
          (f ≫ U'.map (F.map (adj₁.unit.app X))))

Tactic:
simp