awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.Lifting.Right (goal)
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
⊢ 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)))
have 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)))
Tactic: simp only [otherMap, assoc, ← Functor.map_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.Lifting.Right (goal)
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
⊢ 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) }
have 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))
Tactic: apply (adj₂.homEquiv _ _).symm.subtypeEquiv _
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.Lifting.Right (goal)
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)
⊢ 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))
have 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))))
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]
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.Lifting.Right (goal)
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
⊢ 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)) }
have 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)))
Tactic: apply (adj₁.homEquiv _ _).subtypeEquiv
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.Lifting.Right (goal)
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
⊢ 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)))
have 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))
Tactic: rw [← (adj₁.homEquiv _ _).injective.eq_iff, adj₁.homEquiv_unit,
        adj₁.homEquiv_unit, adj₁.homEquiv_unit, eq_comm]
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.Lifting.Right (goal)
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)
⊢ Functor.{v₂, v₃, u₂, u₃} B C
have 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)
Tactic: refine Adjunction.rightAdjointOfEquiv
    (fun X Y => (constructRightAdjointEquiv L _ adj₁ adj₂ h X Y).symm) ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.Lifting.Right (goal)
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.IsLeftAdjoint
have rsuffices : L'.IsLeftAdjoint → L.IsLeftAdjoint
Tactic: rsuffices : L'.IsLeftAdjoint
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.Lifting.Right (goal)
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
⊢ L.IsLeftAdjoint
have rsuffices₁ : L'.IsLeftAdjoint
Tactic: rsuffices : L'.IsLeftAdjoint
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.Lifting.Right (goal)
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
have refine : L' ⋙ Functor.inv (Comonad.comparison (comonadicAdjunction F)) ≅ L
Tactic: refine ((Adjunction.ofIsLeftAdjoint
      (L' ⋙ (Comonad.comparison (comonadicAdjunction F)).inv)).ofNatIsoLeft ?_).isLeftAdjoint
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.Lifting.Right (goal)
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
have refine : L ⋙ F ≅ L' ⋙ (Adjunction.toComonad (R := comonadicRightAdjoint F) (comonadicAdjunction F)).forget
Tactic: refine ((Adjunction.ofIsLeftAdjoint (L ⋙ F)).ofNatIsoLeft ?_).isLeftAdjoint
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.Lifting.Right (goal)
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 ((Adjunction.toComonad (R := comonadicRightAdjoint F) (comonadicAdjunction F)).adj.unit.app X)
have 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 := sorry :
    X.Hom ((Adjunction.toComonad (R := comonadicRightAdjoint F) (comonadicAdjunction F)).cofree.obj X.A) }
Tactic: simp only [Comonad.adj_unit]
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.Limits (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
J : Type u
inst_2 : Category.{v, u} J
K : Functor.{v, v₁, u, u₁} J C
E : Functor.{v₁, v₂, u₁, u₂} C D
inst_3 : E.IsEquivalence
inst_4 : HasColimit (K ⋙ E)
⊢ HasColimit K
have rw : HasColimit (K ⋙ E.asEquivalence.functor ⋙ E.asEquivalence.inverse)
Tactic: rw [hasColimit_iff_of_iso
    ((Functor.rightUnitor _).symm ≪≫ isoWhiskerLeft K E.asEquivalence.unitIso)]
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.Limits (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
J : Type u
inst_2 : Category.{v, u} J
K : Functor.{v, v₂, u, u₂} J D
E : Functor.{v₂, v₁, u₂, u₁} D C
inst_3 : E.IsEquivalence
inst_4 : HasLimit (K ⋙ E)
⊢ HasLimit K
have rw : HasLimit (K ⋙ E.asEquivalence.functor ⋙ E.asEquivalence.inverse)
Tactic: rw [← hasLimit_iff_of_iso
    (isoWhiskerLeft K E.asEquivalence.unitIso.symm ≪≫ Functor.rightUnitor _)]
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.Limits (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
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
J : Type u
inst_2 : Category.{v, u} J
K : Functor.{v, v₁, u, u₁} J C
Y : D
t : (obj (cocones J D) (op (K ⋙ F))).obj Y
j j' : J
f : j ⟶ j'
⊢ Eq (α := (unop (op (unop (op K)))).obj j ⟶ obj.{v, v₁, u, u₁} (obj (const J) (G.obj Y)) j')
    ((unop (op (unop (op K)))).map f ≫
      ((adj.homEquiv (K.obj j') Y : Equiv.{v₂ + 1, v₁ + 1} (F.obj (K.obj j') ⟶ Y) (K.obj j' ⟶ G.obj Y)) :
          (a : F.obj (K.obj j') ⟶ Y) → K.obj j' ⟶ G.obj Y)
        (t.app j'))
    (((adj.homEquiv (K.obj j) Y : Equiv.{v₂ + 1, v₁ + 1} (F.obj (K.obj j) ⟶ Y) (K.obj j ⟶ G.obj Y)) :
          (a : F.obj (K.obj j) ⟶ Y) → K.obj j ⟶ G.obj Y)
        (t.app j) ≫
      map (obj (const J) (G.obj Y)) f)
have rw : Eq.{v₁ + 1} (α := (unop (op (unop (op K)))).obj j ⟶ obj.{v, v₁, u, u₁} (obj (const J) (G.obj Y)) j')
  (((adj.homEquiv ((unop (op (unop (op K)))).obj j) Y :
          Equiv.{v₂ + 1, v₁ + 1} (F.obj ((unop (op (unop (op K)))).obj j) ⟶ Y)
            ((unop (op (unop (op K)))).obj j ⟶ G.obj Y)) :
        (a : F.obj ((unop (op (unop (op K)))).obj j) ⟶ Y) → (unop (op (unop (op K)))).obj j ⟶ G.obj Y)
      (t.app j ≫ map (obj (const J) Y) f) :
    (unop (op (unop (op K)))).obj j ⟶ G.obj Y)
  (((adj.homEquiv (K.obj j) Y : Equiv.{v₂ + 1, v₁ + 1} (F.obj (K.obj j) ⟶ Y) (K.obj j ⟶ G.obj Y)) :
          (a : F.obj (K.obj j) ⟶ Y) → K.obj j ⟶ G.obj Y)
        (t.app j) ≫
      map (obj (const J) (G.obj Y)) f :
    (unop (op (unop (op K)))).obj j ⟶ obj.{v, v₁, u, u₁} (obj (const J) (G.obj Y)) j')
Tactic: rw [← adj.homEquiv_naturality_left, ← Functor.comp_map, t.naturality]
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.Limits (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
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
J : Type u
inst_2 : Category.{v, u} J
K : Functor.{v, v₂, u, u₂} J D
X : Cᵒᵖ
t : (F.op ⋙ obj (cones J D) K).obj X
j j' : J
f : j ⟶ j'
⊢ Eq.{v₁ + 1} (α := obj.{v, v₁, u, u₁} (unop (obj (Functor.op (const J)) X)) j ⟶ (K ⋙ G).obj j')
    (map (unop (obj (Functor.op (const J)) X)) f ≫
      ((adj.homEquiv (unop X) (K.obj j') :
            Equiv.{v₂ + 1, v₁ + 1} (F.obj (unop X) ⟶ K.obj j') (unop X ⟶ G.obj (K.obj j'))) :
          (a : F.obj (unop X) ⟶ K.obj j') → unop X ⟶ G.obj (K.obj j'))
        (t.app j'))
    (((adj.homEquiv (unop X) (K.obj j) : Equiv.{v₂ + 1, v₁ + 1} (F.obj (unop X) ⟶ K.obj j) (unop X ⟶ G.obj (K.obj j))) :
          (a : F.obj (unop X) ⟶ K.obj j) → unop X ⟶ G.obj (K.obj j))
        (t.app j) ≫
      (K ⋙ G).map f)
have erw : Eq.{v₁ + 1} (α := obj.{v, v₁, u, u₁} (unop (obj (Functor.op (const J)) X)) j ⟶ (K ⋙ G).obj j')
  (((adj.homEquiv (unop X) (K.obj j') :
          Equiv.{v₂ + 1, v₁ + 1} (F.obj (unop X) ⟶ K.obj j') (unop X ⟶ G.obj (K.obj j'))) :
        (a : F.obj (unop X) ⟶ K.obj j') → unop X ⟶ G.obj (K.obj j'))
      (t.app j') :
    unop X ⟶ G.obj (K.obj j'))
  (((adj.homEquiv (obj.{v, v₁, u, u₁} (unop (obj (Functor.op (const J)) X)) j) (K.obj j') :
          Equiv.{v₂ + 1, v₁ + 1} (F.obj (obj.{v, v₁, u, u₁} (unop (obj (Functor.op (const J)) X)) j) ⟶ K.obj j')
            (obj.{v, v₁, u, u₁} (unop (obj (Functor.op (const J)) X)) j ⟶ G.obj (K.obj j'))) :
        (a : F.obj ((unop ((const J).op.obj X)).obj j) ⟶ K.obj j') →
          (unop ((const J).op.obj X)).obj j ⟶ G.obj (K.obj j'))
      (t.app j') :
    obj.{v, v₁, u, u₁} (unop (obj (Functor.op (const J)) X)) j ⟶ G.obj (K.obj j'))
Tactic: erw [← adj.homEquiv_naturality_right, ← t.naturality, Category.id_comp, Category.id_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.Limits (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
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
J : Type u
inst_2 : Category.{v, u} J
K : Functor.{v, v₂, u, u₂} J D
X : Cᵒᵖ
t : (obj (cones J C) (K ⋙ G)).obj X
j j' : J
f : j ⟶ j'
⊢ Eq.{v₂ + 1} (α := obj.{v, v₂, u, u₂} (unop (obj (Functor.op (const J)) (F.op.obj X))) j ⟶ K.obj j')
    (map (unop (obj (Functor.op (const J)) (F.op.obj X))) f ≫
      ((Equiv.symm (adj.homEquiv (unop X) (K.obj j')) :
            Equiv.{v₁ + 1, v₂ + 1} (unop X ⟶ G.obj (K.obj j')) (F.obj (unop X) ⟶ K.obj j')) :
          (a : unop X ⟶ G.obj (K.obj j')) → F.obj (unop X) ⟶ K.obj j')
        (t.app j'))
    (((Equiv.symm (adj.homEquiv (unop X) (K.obj j)) :
            Equiv.{v₁ + 1, v₂ + 1} (unop X ⟶ G.obj (K.obj j)) (F.obj (unop X) ⟶ K.obj j)) :
          (a : unop X ⟶ G.obj (K.obj j)) → F.obj (unop X) ⟶ K.obj j)
        (t.app j) ≫
      K.map f)
have erw : Eq.{v₂ + 1} (α := obj.{v, v₂, u, u₂} (unop (obj (Functor.op (const J)) (F.op.obj X))) j ⟶ K.obj j')
  (map (unop (obj (Functor.op (const J)) (F.op.obj X))) f ≫
    ((Equiv.symm (adj.homEquiv (unop X) (K.obj j')) :
          Equiv.{v₁ + 1, v₂ + 1} (unop X ⟶ G.obj (K.obj j')) (F.obj (unop X) ⟶ K.obj j')) :
        (a : unop X ⟶ G.obj (K.obj j')) → F.obj (unop X) ⟶ K.obj j')
      (t.app j'))
  (((Equiv.symm (adj.homEquiv (unop X) (K.obj j')) :
        Equiv.{v₁ + 1, v₂ + 1} (unop X ⟶ G.obj (K.obj j')) (F.obj (unop X) ⟶ K.obj j')) :
      (a : unop X ⟶ G.obj (K.obj j')) → F.obj (unop X) ⟶ K.obj j')
    (t.app j ≫ G.map (K.map f)))
Tactic: erw [← adj.homEquiv_naturality_right_symm, ← t.naturality, Category.id_comp, Category.id_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.Limits (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
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
J : Type u
inst_2 : Category.{v, u} J
K : Functor.{v, v₂, u, u₂} J D
X : Cᵒᵖ
t : (obj (cones J C) (K ⋙ G)).obj X
j j' : J
f : j ⟶ j'
erw :
  Eq.{v₂ + 1} (α := obj.{v, v₂, u, u₂} (unop (obj (Functor.op (const J)) (F.op.obj X))) j ⟶ K.obj j')
    (map (unop (obj (Functor.op (const J)) (F.op.obj X))) f ≫
      ((Equiv.symm (adj.homEquiv (unop X) (K.obj j')) :
            Equiv.{v₁ + 1, v₂ + 1} (unop X ⟶ G.obj (K.obj j')) (F.obj (unop X) ⟶ K.obj j')) :
          (a : unop X ⟶ G.obj (K.obj j')) → F.obj (unop X) ⟶ K.obj j')
        (t.app j'))
    (((Equiv.symm (adj.homEquiv (unop X) (K.obj j')) :
          Equiv.{v₁ + 1, v₂ + 1} (unop X ⟶ G.obj (K.obj j')) (F.obj (unop X) ⟶ K.obj j')) :
        (a : unop X ⟶ G.obj (K.obj j')) → F.obj (unop X) ⟶ K.obj j')
      (t.app j ≫ G.map (K.map f)))
⊢ Eq.{v₂ + 1} (α := obj.{v, v₂, u, u₂} (unop (obj (Functor.op (const J)) (F.op.obj X))) j ⟶ K.obj j')
    (map (unop (obj (Functor.op (const J)) (F.op.obj X))) f ≫
      ((Equiv.symm (adj.homEquiv (unop X) (K.obj j')) :
            Equiv.{v₁ + 1, v₂ + 1} (unop X ⟶ G.obj (K.obj j')) (F.obj (unop X) ⟶ K.obj j')) :
          (a : unop X ⟶ G.obj (K.obj j')) → F.obj (unop X) ⟶ K.obj j')
        (t.app j'))
    (((Equiv.symm (adj.homEquiv (unop X) (K.obj j)) :
            Equiv.{v₁ + 1, v₂ + 1} (unop X ⟶ G.obj (K.obj j)) (F.obj (unop X) ⟶ K.obj j)) :
          (a : unop X ⟶ G.obj (K.obj j)) → F.obj (unop X) ⟶ K.obj j)
        (t.app j) ≫
      K.map f)
have erw₁ : Eq.{v₂ + 1} (α := obj.{v, v₂, u, u₂} (unop (obj (Functor.op (const J)) (F.op.obj X))) j ⟶ K.obj j')
  (map (unop (obj (Functor.op (const J)) (F.op.obj X))) f ≫
    ((Equiv.symm (adj.homEquiv (unop X) (K.obj j')) :
          Equiv.{v₁ + 1, v₂ + 1} (unop X ⟶ G.obj (K.obj j')) (F.obj (unop X) ⟶ K.obj j')) :
        (a : unop X ⟶ G.obj (K.obj j')) → F.obj (unop X) ⟶ K.obj j')
      (t.app j'))
  (((Equiv.symm (adj.homEquiv (unop X) (K.obj j')) :
        Equiv.{v₁ + 1, v₂ + 1} (unop X ⟶ G.obj (K.obj j')) (F.obj (unop X) ⟶ K.obj j')) :
      (a : unop X ⟶ G.obj (K.obj j')) → F.obj (unop X) ⟶ K.obj j')
    (map (unop (obj (Functor.op (const J)) X)) f ≫ t.app j'))
Tactic: erw [← adj.homEquiv_naturality_right_symm, ← t.naturality, Category.id_comp, Category.id_comp]