awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Adjunction.CompositionIso
Goal:
C₀ : Type u_1
C₁ : Type u_2
C₂ : Type u_3
C₃ : Type u_4
inst : Category.{v_1, u_1} C₀
inst_1 : Category.{v_2, u_2} C₁
inst_2 : Category.{v_3, u_3} C₂
inst_3 : Category.{v_4, u_4} C₃
F₀₁ : Functor.{v_1, v_2, u_1, u_2} C₀ C₁
F₁₂ : Functor.{v_2, v_3, u_2, u_3} C₁ C₂
F₂₃ : Functor.{v_3, v_4, u_3, u_4} C₂ C₃
F₀₂ : Functor.{v_1, v_3, u_1, u_3} C₀ C₂
F₁₃ : Functor.{v_2, v_4, u_2, u_4} C₁ C₃
F₀₃ : Functor.{v_1, v_4, u_1, u_4} C₀ C₃
G₁₀ : Functor.{v_2, v_1, u_2, u_1} C₁ C₀
G₂₁ : Functor.{v_3, v_2, u_3, u_2} C₂ C₁
G₃₂ : Functor.{v_4, v_3, u_4, u_3} C₃ C₂
G₂₀ : Functor.{v_3, v_1, u_3, u_1} C₂ C₀
G₃₁ : Functor.{v_4, v_2, u_4, u_2} C₃ C₁
G₃₀ : Functor.{v_4, v_1, u_4, u_1} C₃ C₀
adj₀₁ : F₀₁ ⊣ G₁₀
adj₁₂ : F₁₂ ⊣ G₂₁
adj₂₃ : F₂₃ ⊣ G₃₂
adj₀₂ : F₀₂ ⊣ G₂₀
adj₁₃ : F₁₃ ⊣ G₃₁
adj₀₃ : F₀₃ ⊣ G₃₀
e₀₁₂ : G₂₁ ⋙ G₁₀ ≅ G₂₀
e₁₂₃ : G₃₂ ⋙ G₂₁ ≅ G₃₁
e₀₁₃ : G₃₁ ⋙ G₁₀ ≅ G₃₀
e₀₂₃ : G₃₂ ⋙ G₂₀ ≅ G₃₀
h : G₃₂.isoWhiskerLeft e₀₁₂ ≪≫ e₀₂₃ = (G₃₂.associator G₂₁ G₁₀).symm ≪≫ isoWhiskerRight e₁₂₃ G₁₀ ≪≫ e₀₁₃
⊢ e₀₂₃.inv ≫ G₃₂.whiskerLeft e₀₁₂.inv = e₀₁₃.inv ≫ whiskerRight e₁₂₃.inv G₁₀ ≫ (G₃₂.associator G₂₁ G₁₀).hom

Tactic:
simpa using congr_arg Iso.inv h

Premises used: congr_arg, CategoryTheory.Iso.inv
-- Module: Mathlib.CategoryTheory.Adjunction.CompositionIso
Goal:
C₀ : Type u_1
C₁ : Type u_2
C₂ : Type u_3
C₃ : Type u_4
inst : Category.{v_1, u_1} C₀
inst_1 : Category.{v_2, u_2} C₁
inst_2 : Category.{v_3, u_3} C₂
inst_3 : Category.{v_4, u_4} C₃
F₀₁ : Functor.{v_1, v_2, u_1, u_2} C₀ C₁
F₁₂ : Functor.{v_2, v_3, u_2, u_3} C₁ C₂
F₂₃ : Functor.{v_3, v_4, u_3, u_4} C₂ C₃
F₀₂ : Functor.{v_1, v_3, u_1, u_3} C₀ C₂
F₁₃ : Functor.{v_2, v_4, u_2, u_4} C₁ C₃
F₀₃ : Functor.{v_1, v_4, u_1, u_4} C₀ C₃
G₁₀ : Functor.{v_2, v_1, u_2, u_1} C₁ C₀
G₂₁ : Functor.{v_3, v_2, u_3, u_2} C₂ C₁
G₃₂ : Functor.{v_4, v_3, u_4, u_3} C₃ C₂
G₂₀ : Functor.{v_3, v_1, u_3, u_1} C₂ C₀
G₃₁ : Functor.{v_4, v_2, u_4, u_2} C₃ C₁
G₃₀ : Functor.{v_4, v_1, u_4, u_1} C₃ C₀
adj₀₁ : F₀₁ ⊣ G₁₀
adj₁₂ : F₁₂ ⊣ G₂₁
adj₂₃ : F₂₃ ⊣ G₃₂
adj₀₂ : F₀₂ ⊣ G₂₀
adj₁₃ : F₁₃ ⊣ G₃₁
adj₀₃ : F₀₃ ⊣ G₃₀
e₀₁₂ : G₂₁ ⋙ G₁₀ ≅ G₂₀
e₁₂₃ : G₃₂ ⋙ G₂₁ ≅ G₃₁
e₀₁₃ : G₃₁ ⋙ G₁₀ ≅ G₃₀
e₀₂₃ : G₃₂ ⋙ G₂₀ ≅ G₃₀
h : G₃₂.isoWhiskerLeft e₀₁₂ ≪≫ e₀₂₃ = (G₃₂.associator G₂₁ G₁₀).symm ≪≫ isoWhiskerRight e₁₂₃ G₁₀ ≪≫ e₀₁₃
⊢ F₀₁.whiskerLeft (adj₁₂.leftAdjointCompNatTrans adj₂₃ adj₁₃ e₁₂₃.inv) ≫
      adj₀₁.leftAdjointCompNatTrans adj₁₃ adj₀₃ e₀₁₃.inv =
    (F₀₁.associator F₁₂ F₂₃).inv ≫
      whiskerRight (adj₀₁.leftAdjointCompNatTrans adj₁₂ adj₀₂ e₀₁₂.inv) F₂₃ ≫
        adj₀₂.leftAdjointCompNatTrans adj₂₃ adj₀₃ e₀₂₃.inv

Tactic:
exact leftAdjointCompNatTrans_assoc _ _ _ _ _ _ _ _ _ _
    (by simpa using congr_arg Iso.inv h)

Premises used: CategoryTheory.Adjunction.leftAdjointCompNatTrans_assoc
-- Module: Mathlib.CategoryTheory.Adjunction.Evaluation
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : ∀ (a b : C), HasCoproductsOfShape.{v₁, u₂, v₂} (a ⟶ b) D
c : C
x d₂ : D
f : x ⟶ d₂
X Y : C
f_1 : X ⟶ Y
dsimp :
  Eq.{v₂ + 1} (α :=
    Quiver.Hom.{v₂, u₂} (V := D) (sigmaObj.{v₁, v₂, u₂} fun (x_1 : c ⟶ X) ↦ x)
      (sigmaObj.{v₁, v₂, u₂} fun (x : c ⟶ Y) ↦ d₂))
    (CategoryStruct.comp (Y := sigmaObj.{v₁, v₂, u₂} fun (x_1 : c ⟶ Y) ↦ x)
      (Sigma.desc fun (g : c ⟶ X) ↦ Sigma.ι.{v₁, v₂, u₂} (C := D) (fun (x_1 : c ⟶ Y) ↦ x) (g ≫ f_1))
      (Sigma.desc fun (h : c ⟶ Y) ↦ f ≫ Sigma.ι.{v₁, v₂, u₂} (C := D) (fun (x : c ⟶ Y) ↦ d₂) h))
    (CategoryStruct.comp (Y := sigmaObj.{v₁, v₂, u₂} fun (x : c ⟶ X) ↦ d₂)
      (Sigma.desc fun (h : c ⟶ X) ↦ f ≫ Sigma.ι.{v₁, v₂, u₂} (C := D) (fun (x : c ⟶ X) ↦ d₂) h)
      (Sigma.desc fun (g : c ⟶ X) ↦ Sigma.ι.{v₁, v₂, u₂} (C := D) (fun (x : c ⟶ Y) ↦ d₂) (g ≫ f_1)))
⊢ Eq.{v₂ + 1} (α :=
    Quiver.Hom.{v₂, u₂} (V := D)
      (Functor.obj.{v₁, v₂, u₁, u₂}
        { obj := fun (t : C) ↦ sigmaObj.{v₁, v₂, u₂} fun (x_1 : c ⟶ t) ↦ x,
          map := fun {X Y : C} (f : X ⟶ Y) ↦
            Sigma.desc fun (g : c ⟶ X) ↦ Sigma.ι.{v₁, v₂, u₂} (C := D) (fun (x_1 : c ⟶ Y) ↦ x) (g ≫ f),
          map_id := ⋯, map_comp := ⋯ }
        X)
      (Functor.obj.{v₁, v₂, u₁, u₂}
        { obj := fun (t : C) ↦ sigmaObj.{v₁, v₂, u₂} fun (x : c ⟶ t) ↦ d₂,
          map := fun {X Y : C} (f : X ⟶ Y) ↦
            Sigma.desc fun (g : c ⟶ X) ↦ Sigma.ι.{v₁, v₂, u₂} (C := D) (fun (x : c ⟶ Y) ↦ d₂) (g ≫ f),
          map_id := ⋯, map_comp := ⋯ }
        Y))
    (Functor.map
        { obj := fun (t : C) ↦ sigmaObj.{v₁, v₂, u₂} fun (x_1 : c ⟶ t) ↦ x,
          map := fun {X Y : C} (f : X ⟶ Y) ↦
            Sigma.desc fun (g : c ⟶ X) ↦ Sigma.ι.{v₁, v₂, u₂} (C := D) (fun (x_1 : c ⟶ Y) ↦ x) (g ≫ f),
          map_id := ⋯, map_comp := ⋯ : Functor.{v₁, v₂, u₁, u₂} C D }
        f_1 ≫
      Sigma.desc fun (h : c ⟶ Y) ↦ f ≫ Sigma.ι.{v₁, v₂, u₂} (C := D) (fun (x : c ⟶ Y) ↦ d₂) h)
    ((Sigma.desc fun (h : c ⟶ X) ↦ f ≫ Sigma.ι.{v₁, v₂, u₂} (C := D) (fun (x : c ⟶ X) ↦ d₂) h) ≫
      Functor.map
        { obj := fun (t : C) ↦ sigmaObj.{v₁, v₂, u₂} fun (x : c ⟶ t) ↦ d₂,
          map := fun {X Y : C} (f : X ⟶ Y) ↦
            Sigma.desc fun (g : c ⟶ X) ↦ Sigma.ι.{v₁, v₂, u₂} (C := D) (fun (x : c ⟶ Y) ↦ d₂) (g ≫ f),
          map_id := ⋯, map_comp := ⋯ : Functor.{v₁, v₂, u₁, u₂} C D }
        f_1)

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Adjunction.Evaluation
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : ∀ (a b : C), HasCoproductsOfShape.{v₁, u₂, v₂} (a ⟶ b) D
c : C
x d₂ : D
f : x ⟶ d₂
X Y : C
f_1 : X ⟶ Y
h :
  ∀ (b : c ⟶ X),
    Eq.{v₂ + 1} (α := x ⟶ sigmaObj.{v₁, v₂, u₂} fun (x : c ⟶ Y) ↦ d₂)
      (CategoryStruct.comp (Y := sigmaObj.{v₁, v₂, u₂} fun (x_1 : c ⟶ X) ↦ x)
          (Sigma.ι.{v₁, v₂, u₂} (C := D) (fun (x_1 : c ⟶ X) ↦ x) b)
          (CategoryStruct.comp (Y := sigmaObj.{v₁, v₂, u₂} fun (x_1 : c ⟶ Y) ↦ x)
            (Sigma.desc fun (g : c ⟶ X) ↦ Sigma.ι.{v₁, v₂, u₂} (C := D) (fun (x_1 : c ⟶ Y) ↦ x) (g ≫ f_1))
            (Sigma.desc fun (h : c ⟶ Y) ↦ f ≫ Sigma.ι.{v₁, v₂, u₂} (C := D) (fun (x : c ⟶ Y) ↦ d₂) h)) :
        x ⟶ sigmaObj.{v₁, v₂, u₂} fun (x : c ⟶ Y) ↦ d₂)
      (CategoryStruct.comp (Y := sigmaObj.{v₁, v₂, u₂} fun (x_1 : c ⟶ X) ↦ x)
          (Sigma.ι.{v₁, v₂, u₂} (C := D) (fun (x_1 : c ⟶ X) ↦ x) b)
          (CategoryStruct.comp (Y := sigmaObj.{v₁, v₂, u₂} fun (x : c ⟶ X) ↦ d₂)
            (Sigma.desc fun (h : c ⟶ X) ↦ f ≫ Sigma.ι.{v₁, v₂, u₂} (C := D) (fun (x : c ⟶ X) ↦ d₂) h)
            (Sigma.desc fun (g : c ⟶ X) ↦ Sigma.ι.{v₁, v₂, u₂} (C := D) (fun (x : c ⟶ Y) ↦ d₂) (g ≫ f_1))) :
        x ⟶ sigmaObj.{v₁, v₂, u₂} fun (x : c ⟶ Y) ↦ d₂)
⊢ Eq.{v₂ + 1} (α :=
    Quiver.Hom.{v₂, u₂} (V := D) (sigmaObj.{v₁, v₂, u₂} fun (x_1 : c ⟶ X) ↦ x)
      (sigmaObj.{v₁, v₂, u₂} fun (x : c ⟶ Y) ↦ d₂))
    (CategoryStruct.comp (Y := sigmaObj.{v₁, v₂, u₂} fun (x_1 : c ⟶ Y) ↦ x)
      (Sigma.desc fun (g : c ⟶ X) ↦ Sigma.ι.{v₁, v₂, u₂} (C := D) (fun (x_1 : c ⟶ Y) ↦ x) (g ≫ f_1))
      (Sigma.desc fun (h : c ⟶ Y) ↦ f ≫ Sigma.ι.{v₁, v₂, u₂} (C := D) (fun (x : c ⟶ Y) ↦ d₂) h))
    (CategoryStruct.comp (Y := sigmaObj.{v₁, v₂, u₂} fun (x : c ⟶ X) ↦ d₂)
      (Sigma.desc fun (h : c ⟶ X) ↦ f ≫ Sigma.ι.{v₁, v₂, u₂} (C := D) (fun (x : c ⟶ X) ↦ d₂) h)
      (Sigma.desc fun (g : c ⟶ X) ↦ Sigma.ι.{v₁, v₂, u₂} (C := D) (fun (x : c ⟶ Y) ↦ d₂) (g ≫ f_1)))

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Adjunction.Evaluation
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : ∀ (a b : C), HasCoproductsOfShape.{v₁, u₂, v₂} (a ⟶ b) D
c : C
x d₂ : D
f : x ⟶ d₂
X Y : C
f_1 : X ⟶ Y
b : c ⟶ X
⊢ Eq.{v₂ + 1} (α := x ⟶ sigmaObj.{v₁, v₂, u₂} fun (x : c ⟶ Y) ↦ d₂)
    (CategoryStruct.comp (Y := sigmaObj.{v₁, v₂, u₂} fun (x_1 : c ⟶ X) ↦ x)
        (Sigma.ι.{v₁, v₂, u₂} (C := D) (fun (x_1 : c ⟶ X) ↦ x) b)
        (CategoryStruct.comp (Y := sigmaObj.{v₁, v₂, u₂} fun (x_1 : c ⟶ Y) ↦ x)
          (Sigma.desc fun (g : c ⟶ X) ↦ Sigma.ι.{v₁, v₂, u₂} (C := D) (fun (x_1 : c ⟶ Y) ↦ x) (g ≫ f_1))
          (Sigma.desc fun (h : c ⟶ Y) ↦ f ≫ Sigma.ι.{v₁, v₂, u₂} (C := D) (fun (x : c ⟶ Y) ↦ d₂) h)) :
      x ⟶ sigmaObj.{v₁, v₂, u₂} fun (x : c ⟶ Y) ↦ d₂)
    (CategoryStruct.comp (Y := sigmaObj.{v₁, v₂, u₂} fun (x_1 : c ⟶ X) ↦ x)
        (Sigma.ι.{v₁, v₂, u₂} (C := D) (fun (x_1 : c ⟶ X) ↦ x) b)
        (CategoryStruct.comp (Y := sigmaObj.{v₁, v₂, u₂} fun (x : c ⟶ X) ↦ d₂)
          (Sigma.desc fun (h : c ⟶ X) ↦ f ≫ Sigma.ι.{v₁, v₂, u₂} (C := D) (fun (x : c ⟶ X) ↦ d₂) h)
          (Sigma.desc fun (g : c ⟶ X) ↦ Sigma.ι.{v₁, v₂, u₂} (C := D) (fun (x : c ⟶ Y) ↦ d₂) (g ≫ f_1))) :
      x ⟶ sigmaObj.{v₁, v₂, u₂} fun (x : c ⟶ Y) ↦ d₂)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Adjunction.Evaluation
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : ∀ (a b : C), HasCoproductsOfShape.{v₁, u₂, v₂} (a ⟶ b) D
c : C
d : D
F : Functor.{v₁, v₂, u₁, u₂} C D
f : Functor.obj (evaluationLeftAdjoint D c) d ⟶ F
w :
  ∀ (x : C),
    NatTrans.app
        ((fun (f : d ⟶ Functor.obj (Functor.obj (evaluation C D) c) F) ↦
            ({ app := fun (x : C) ↦ Sigma.desc fun (h : c ⟶ x) ↦ f ≫ F.map h, naturality := ⋯ } :
              NatTrans (Functor.obj (evaluationLeftAdjoint D c) d) F))
          ((fun (f : Functor.obj (evaluationLeftAdjoint D c) d ⟶ F) ↦
              Sigma.ι.{v₁, v₂, u₂} (C := D) (fun (x : c ⟶ c) ↦ d) (𝟙 c) ≫ f.app c)
            f))
        x =
      f.app x
⊢ (fun (f : d ⟶ Functor.obj (Functor.obj (evaluation C D) c) F) ↦
        ({ app := fun (x : C) ↦ Sigma.desc fun (h : c ⟶ x) ↦ f ≫ F.map h, naturality := ⋯ } :
          NatTrans (Functor.obj (evaluationLeftAdjoint D c) d) F))
      ((fun (f : Functor.obj (evaluationLeftAdjoint D c) d ⟶ F) ↦
          Sigma.ι.{v₁, v₂, u₂} (C := D) (fun (x : c ⟶ c) ↦ d) (𝟙 c) ≫ f.app c)
        f) =
    f

Tactic:
ext x
-- Module: Mathlib.CategoryTheory.Adjunction.Evaluation
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : ∀ (a b : C), HasCoproductsOfShape.{v₁, u₂, v₂} (a ⟶ b) D
c : C
d : D
F : Functor.{v₁, v₂, u₁, u₂} C D
f : Functor.obj (evaluationLeftAdjoint D c) d ⟶ F
x : C
w :
  (Sigma.desc fun (h : c ⟶ x) ↦ (Sigma.ι.{v₁, v₂, u₂} (C := D) (fun (x : c ⟶ c) ↦ d) (𝟙 c) ≫ f.app c) ≫ F.map h) =
    f.app x
⊢ NatTrans.app
      ((fun (f : d ⟶ Functor.obj (Functor.obj (evaluation C D) c) F) ↦
          ({ app := fun (x : C) ↦ Sigma.desc fun (h : c ⟶ x) ↦ f ≫ F.map h, naturality := ⋯ } :
            NatTrans (Functor.obj (evaluationLeftAdjoint D c) d) F))
        ((fun (f : Functor.obj (evaluationLeftAdjoint D c) d ⟶ F) ↦
            Sigma.ι.{v₁, v₂, u₂} (C := D) (fun (x : c ⟶ c) ↦ d) (𝟙 c) ≫ f.app c)
          f))
      x =
    f.app x

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Adjunction.Evaluation
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : ∀ (a b : C), HasCoproductsOfShape.{v₁, u₂, v₂} (a ⟶ b) D
c : C
d : D
F : Functor.{v₁, v₂, u₁, u₂} C D
f : Functor.obj (evaluationLeftAdjoint D c) d ⟶ F
x : C
w :
  ∀ (g : c ⟶ x),
    CategoryStruct.comp (Y := sigmaObj.{v₁, v₂, u₂} fun (x : c ⟶ x) ↦ d)
        (Sigma.ι.{v₁, v₂, u₂} (C := D) (fun (x : c ⟶ x) ↦ d) g)
        (Sigma.desc fun (h : c ⟶ x) ↦ (Sigma.ι.{v₁, v₂, u₂} (C := D) (fun (x : c ⟶ c) ↦ d) (𝟙 c) ≫ f.app c) ≫ F.map h) =
      Sigma.ι.{v₁, v₂, u₂} (C := D) (fun (x : c ⟶ x) ↦ d) g ≫ f.app x
⊢ (Sigma.desc fun (h : c ⟶ x) ↦ (Sigma.ι.{v₁, v₂, u₂} (C := D) (fun (x : c ⟶ c) ↦ d) (𝟙 c) ≫ f.app c) ≫ F.map h) =
    f.app x

Tactic:
ext g
-- Module: Mathlib.CategoryTheory.Adjunction.Evaluation
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : ∀ (a b : C), HasCoproductsOfShape.{v₁, u₂, v₂} (a ⟶ b) D
c : C
d : D
F : Functor.{v₁, v₂, u₁, u₂} C D
f : Functor.obj (evaluationLeftAdjoint D c) d ⟶ F
x : C
g : c ⟶ x
⊢ CategoryStruct.comp (Y := sigmaObj.{v₁, v₂, u₂} fun (x : c ⟶ x) ↦ d)
      (Sigma.ι.{v₁, v₂, u₂} (C := D) (fun (x : c ⟶ x) ↦ d) g)
      (Sigma.desc fun (h : c ⟶ x) ↦ (Sigma.ι.{v₁, v₂, u₂} (C := D) (fun (x : c ⟶ c) ↦ d) (𝟙 c) ≫ f.app c) ≫ F.map h) =
    Sigma.ι.{v₁, v₂, u₂} (C := D) (fun (x : c ⟶ x) ↦ d) g ≫ f.app x

Tactic:
simp only [colimit.ι_desc, Cofan.mk_ι_app, Category.assoc, ← f.naturality,
              evaluationLeftAdjoint_obj_map, colimit.ι_desc_assoc,
              Discrete.functor_obj, Cofan.mk_pt, Category.id_comp]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Discrete.functor_obj, CategoryTheory.Limits.Cofan.mk_ι_app, CategoryTheory.Limits.Cofan.mk_pt, CategoryTheory.Limits.colimit.ι_desc, CategoryTheory.NatTrans.naturality, CategoryTheory.Limits.colimit.ι_desc_assoc, CategoryTheory.Category.id_comp, CategoryTheory.evaluationLeftAdjoint_obj_map
-- Module: Mathlib.CategoryTheory.Adjunction.Evaluation
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : ∀ (a b : C), HasCoproductsOfShape.{v₁, u₂, v₂} (a ⟶ b) D
c : C
d : D
F : Functor.{v₁, v₂, u₁, u₂} C D
f : d ⟶ Functor.obj (Functor.obj (evaluation C D) c) F
⊢ (fun (f : Functor.obj (evaluationLeftAdjoint D c) d ⟶ F) ↦
        Sigma.ι.{v₁, v₂, u₂} (C := D) (fun (x : c ⟶ c) ↦ d) (𝟙 c) ≫ f.app c)
      ((fun (f : d ⟶ Functor.obj (Functor.obj (evaluation C D) c) F) ↦
          ({ app := fun (x : C) ↦ Sigma.desc fun (h : c ⟶ x) ↦ f ≫ F.map h, naturality := ⋯ } :
            NatTrans (Functor.obj (evaluationLeftAdjoint D c) d) F))
        f) =
    f

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Adjunction.Evaluation
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : ∀ (a b : C), HasCoproductsOfShape.{v₁, u₂, v₂} (a ⟶ b) D
c : C
⊢ Functor.IsRightAdjoint (D := Functor.{v₁, v₂, u₁, u₂} C D) (Functor.obj (evaluation C D) c)

Tactic:
⟨_, ⟨evaluationAdjunctionRight _ _⟩⟩

Premises used: Nonempty.intro, CategoryTheory.evaluationAdjunctionRight, Exists.intro, CategoryTheory.Functor.IsRightAdjoint.mk
-- Module: Mathlib.CategoryTheory.Adjunction.Evaluation
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : ∀ (a b : C), HasCoproductsOfShape.{v₁, u₂, v₂} (a ⟶ b) D
F G : Functor.{v₁, v₂, u₁, u₂} C D
η : F ⟶ G
mp : Mono η → ∀ (c : C), Mono (η.app c)
mpr : (∀ (c : C), Mono (η.app c)) → Mono η
⊢ Mono η ↔ ∀ (c : C), Mono (η.app c)

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.Adjunction.Evaluation
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : ∀ (a b : C), HasCoproductsOfShape.{v₁, u₂, v₂} (a ⟶ b) D
F G : Functor.{v₁, v₂, u₁, u₂} C D
η : F ⟶ G
h : Mono η
c : C
⊢ Mono (η.app c)

Tactic:
(inferInstance : Mono (((evaluation _ _).obj c).map η))

Premises used: inferInstance
-- Module: Mathlib.CategoryTheory.Adjunction.Evaluation
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : ∀ (a b : C), HasCoproductsOfShape.{v₁, u₂, v₂} (a ⟶ b) D
F G : Functor.{v₁, v₂, u₁, u₂} C D
η : F ⟶ G
h : Mono η
c : C
⊢ Mono (η.app c)

Tactic:
exact (inferInstance : Mono (((evaluation _ _).obj c).map η))

Premises used: inferInstance
-- Module: Mathlib.CategoryTheory.Adjunction.Evaluation
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : ∀ (a b : C), HasCoproductsOfShape.{v₁, u₂, v₂} (a ⟶ b) D
F G : Functor.{v₁, v₂, u₁, u₂} C D
η : F ⟶ G
h : ∀ (c : C), Mono (η.app c)
⊢ Mono η

Tactic:
apply NatTrans.mono_of_mono_app

Premises used: CategoryTheory.NatTrans.mono_of_mono_app
-- Module: Mathlib.CategoryTheory.Adjunction.Evaluation
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : ∀ (a b : C), HasProductsOfShape.{v₁, u₂, v₂} (a ⟶ b) D
c : C
F : Functor.{v₁, v₂, u₁, u₂} C D
d : D
f : Functor.obj (Functor.obj (evaluation C D) c) F ⟶ d
⊢ (fun (f : F ⟶ Functor.obj (evaluationRightAdjoint D c) d) ↦ f.app c ≫ Pi.π (fun (x : c ⟶ c) ↦ d) (𝟙 c))
      ((fun (f : Functor.obj (Functor.obj (evaluation C D) c) F ⟶ d) ↦
          ({ app := fun (x : C) ↦ Pi.lift fun (g : x ⟶ c) ↦ F.map g ≫ f, naturality := ⋯ } :
            NatTrans F (Functor.obj (evaluationRightAdjoint D c) d)))
        f) =
    f

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Adjunction.Evaluation
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : ∀ (a b : C), HasProductsOfShape.{v₁, u₂, v₂} (a ⟶ b) D
c : C
F : Functor.{v₁, v₂, u₁, u₂} C D
d : D
f : F ⟶ Functor.obj (evaluationRightAdjoint D c) d
w :
  ∀ (x : C),
    NatTrans.app
        ((fun (f : Functor.obj (Functor.obj (evaluation C D) c) F ⟶ d) ↦
            ({ app := fun (x : C) ↦ Pi.lift fun (g : x ⟶ c) ↦ F.map g ≫ f, naturality := ⋯ } :
              NatTrans F (Functor.obj (evaluationRightAdjoint D c) d)))
          ((fun (f : F ⟶ Functor.obj (evaluationRightAdjoint D c) d) ↦ f.app c ≫ Pi.π (fun (x : c ⟶ c) ↦ d) (𝟙 c)) f))
        x =
      f.app x
⊢ (fun (f : Functor.obj (Functor.obj (evaluation C D) c) F ⟶ d) ↦
        ({ app := fun (x : C) ↦ Pi.lift fun (g : x ⟶ c) ↦ F.map g ≫ f, naturality := ⋯ } :
          NatTrans F (Functor.obj (evaluationRightAdjoint D c) d)))
      ((fun (f : F ⟶ Functor.obj (evaluationRightAdjoint D c) d) ↦ f.app c ≫ Pi.π (fun (x : c ⟶ c) ↦ d) (𝟙 c)) f) =
    f

Tactic:
ext x
-- Module: Mathlib.CategoryTheory.Adjunction.Evaluation
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : ∀ (a b : C), HasProductsOfShape.{v₁, u₂, v₂} (a ⟶ b) D
c : C
F : Functor.{v₁, v₂, u₁, u₂} C D
d : D
f : F ⟶ Functor.obj (evaluationRightAdjoint D c) d
x : C
w : (Pi.lift fun (g : x ⟶ c) ↦ F.map g ≫ f.app c ≫ Pi.π (fun (x : c ⟶ c) ↦ d) (𝟙 c)) = f.app x
⊢ NatTrans.app
      ((fun (f : Functor.obj (Functor.obj (evaluation C D) c) F ⟶ d) ↦
          ({ app := fun (x : C) ↦ Pi.lift fun (g : x ⟶ c) ↦ F.map g ≫ f, naturality := ⋯ } :
            NatTrans F (Functor.obj (evaluationRightAdjoint D c) d)))
        ((fun (f : F ⟶ Functor.obj (evaluationRightAdjoint D c) d) ↦ f.app c ≫ Pi.π (fun (x : c ⟶ c) ↦ d) (𝟙 c)) f))
      x =
    f.app x

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Adjunction.Evaluation
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : ∀ (a b : C), HasProductsOfShape.{v₁, u₂, v₂} (a ⟶ b) D
c : C
F : Functor.{v₁, v₂, u₁, u₂} C D
d : D
f : F ⟶ Functor.obj (evaluationRightAdjoint D c) d
x : C
w :
  ∀ (g : x ⟶ c),
    CategoryStruct.comp (Y := piObj.{v₁, v₂, u₂} fun (x : x ⟶ c) ↦ d)
        (Pi.lift fun (g : x ⟶ c) ↦ F.map g ≫ f.app c ≫ Pi.π (fun (x : c ⟶ c) ↦ d) (𝟙 c))
        (Pi.π (fun (x : x ⟶ c) ↦ d) g) =
      f.app x ≫ Pi.π (fun (x : x ⟶ c) ↦ d) g
⊢ (Pi.lift fun (g : x ⟶ c) ↦ F.map g ≫ f.app c ≫ Pi.π (fun (x : c ⟶ c) ↦ d) (𝟙 c)) = f.app x

Tactic:
ext g
-- Module: Mathlib.CategoryTheory.Adjunction.Evaluation
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : ∀ (a b : C), HasProductsOfShape.{v₁, u₂, v₂} (a ⟶ b) D
c : C
F : Functor.{v₁, v₂, u₁, u₂} C D
d : D
f : F ⟶ Functor.obj (evaluationRightAdjoint D c) d
x : C
g : x ⟶ c
⊢ CategoryStruct.comp (Y := piObj.{v₁, v₂, u₂} fun (x : x ⟶ c) ↦ d)
      (Pi.lift fun (g : x ⟶ c) ↦ F.map g ≫ f.app c ≫ Pi.π (fun (x : c ⟶ c) ↦ d) (𝟙 c)) (Pi.π (fun (x : x ⟶ c) ↦ d) g) =
    f.app x ≫ Pi.π (fun (x : x ⟶ c) ↦ d) g

Tactic:
simp only [NatTrans.naturality_assoc,
              evaluationRightAdjoint_obj_obj, evaluationRightAdjoint_obj_map, limit.lift_π,
              Fan.mk_pt, Fan.mk_π_app, Category.comp_id]

Premises used: CategoryTheory.evaluationRightAdjoint_obj_map, CategoryTheory.Category.comp_id, CategoryTheory.Limits.Fan.mk_pt, CategoryTheory.evaluationRightAdjoint_obj_obj, CategoryTheory.Limits.limit.lift_π, CategoryTheory.Limits.Fan.mk_π_app, CategoryTheory.NatTrans.naturality_assoc
-- Module: Mathlib.CategoryTheory.Adjunction.Evaluation
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : ∀ (a b : C), HasProductsOfShape.{v₁, u₂, v₂} (a ⟶ b) D
c : C
⊢ Functor.IsLeftAdjoint (C := Functor.{v₁, v₂, u₁, u₂} C D) (Functor.obj (evaluation C D) c)

Tactic:
⟨_, ⟨evaluationAdjunctionLeft _ _⟩⟩

Premises used: Nonempty.intro, Exists.intro, CategoryTheory.Functor.IsLeftAdjoint.mk, CategoryTheory.evaluationAdjunctionLeft
-- Module: Mathlib.CategoryTheory.Adjunction.Evaluation
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : ∀ (a b : C), HasProductsOfShape.{v₁, u₂, v₂} (a ⟶ b) D
F G : Functor.{v₁, v₂, u₁, u₂} C D
η : F ⟶ G
mp : Epi η → ∀ (c : C), Epi (η.app c)
mpr : (∀ (c : C), Epi (η.app c)) → Epi η
⊢ Epi η ↔ ∀ (c : C), Epi (η.app c)

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.Adjunction.Evaluation
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : ∀ (a b : C), HasProductsOfShape.{v₁, u₂, v₂} (a ⟶ b) D
F G : Functor.{v₁, v₂, u₁, u₂} C D
η : F ⟶ G
h : Epi η
c : C
⊢ Epi (η.app c)

Tactic:
(inferInstance : Epi (((evaluation _ _).obj c).map η))

Premises used: inferInstance
-- Module: Mathlib.CategoryTheory.Adjunction.Evaluation
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : ∀ (a b : C), HasProductsOfShape.{v₁, u₂, v₂} (a ⟶ b) D
F G : Functor.{v₁, v₂, u₁, u₂} C D
η : F ⟶ G
h : Epi η
c : C
⊢ Epi (η.app c)

Tactic:
exact (inferInstance : Epi (((evaluation _ _).obj c).map η))

Premises used: inferInstance
-- Module: Mathlib.CategoryTheory.Adjunction.Evaluation
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : ∀ (a b : C), HasProductsOfShape.{v₁, u₂, v₂} (a ⟶ b) D
F G : Functor.{v₁, v₂, u₁, u₂} C D
η : F ⟶ G
h : ∀ (c : C), Epi (η.app c)
⊢ Epi η

Tactic:
apply NatTrans.epi_of_epi_app

Premises used: CategoryTheory.NatTrans.epi_of_epi_app
-- Module: Mathlib.CategoryTheory.Adjunction.FullyFaithful
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
L : Functor.{v₁, v₂, u₁, u₂} C D
R : Functor.{v₂, v₁, u₂, u₁} D C
h : L ⊣ R
inst_2 : L.Faithful
X Y : C
f g : Y ⟶ obj.{v₁, v₁, u₁, u₁} (𝟭 C) X
hfg : f ≫ h.unit.app X = g ≫ h.unit.app X
⊢ Eq.{v₁ + 1} (α := Y ⟶ R.obj (L.obj X))
    (((h.homEquiv Y (L.obj X) : Equiv.{v₂ + 1, v₁ + 1} (L.obj Y ⟶ L.obj X) (Y ⟶ R.obj (L.obj X))) :
          (a : L.obj Y ⟶ L.obj X) → Y ⟶ R.obj (L.obj X))
        (L.map f) :
      Y ⟶ R.obj (L.obj X))
    (((h.homEquiv Y (L.obj X) : Equiv.{v₂ + 1, v₁ + 1} (L.obj Y ⟶ L.obj X) (Y ⟶ R.obj (L.obj X))) :
          (a : L.obj Y ⟶ L.obj X) → Y ⟶ R.obj (L.obj X))
        (L.map g) :
      Y ⟶ R.obj (L.obj X))

Tactic:
simpa using hfg
-- Module: Mathlib.CategoryTheory.Adjunction.FullyFaithful
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
L : Functor.{v₁, v₂, u₁, u₂} C D
R : Functor.{v₂, v₁, u₂, u₁} D C
h : L ⊣ R
inst_2 : L.Full
X : C
⊢ L.preimage (h.counit.app (L.obj X)) ≫ h.unit.app X = 𝟙 ((L ⋙ R).obj X)

Tactic:
simp [← h.unit_naturality (L.preimage (h.counit.app (L.obj X)))]

Premises used: CategoryTheory.Functor.preimage, CategoryTheory.Adjunction.counit, CategoryTheory.Adjunction.unit_naturality, CategoryTheory.Functor.obj, CategoryTheory.NatTrans.app
-- Module: Mathlib.CategoryTheory.Adjunction.FullyFaithful
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
L : Functor.{v₁, v₂, u₁, u₂} C D
R : Functor.{v₂, v₁, u₂, u₁} D C
h : L ⊣ R
inst_2 : L.Full
X : C
⊢ IsSplitEpi (h.unit.app X)

Tactic:
⟨⟨h.unitSplitEpiOfLFull X⟩⟩

Premises used: Nonempty.intro, CategoryTheory.IsSplitEpi.mk, CategoryTheory.Adjunction.unitSplitEpiOfLFull
-- Module: Mathlib.CategoryTheory.Adjunction.FullyFaithful
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
L : Functor.{v₁, v₂, u₁, u₂} C D
R : Functor.{v₂, v₁, u₂, u₁} D C
h : L ⊣ R
inst_2 : L.Full
inst_3 : L.Faithful
X : C
⊢ IsIso (h.unit.app X)

Tactic:
isIso_of_mono_of_isSplitEpi _

Premises used: CategoryTheory.isIso_of_mono_of_isSplitEpi
-- Module: Mathlib.CategoryTheory.Adjunction.FullyFaithful
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
L : Functor.{v₁, v₂, u₁, u₂} C D
R : Functor.{v₂, v₁, u₂, u₁} D C
h : L ⊣ R
inst_2 : L.Full
inst_3 : L.Faithful
⊢ IsIso h.unit

Tactic:
NatIso.isIso_of_isIso_app _

Premises used: CategoryTheory.NatIso.isIso_of_isIso_app