awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Adjunction.Triple
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
G : Functor.{v_2, v_1, u_2, u_1} D C
H : Functor.{v_1, v_2, u_1, u_2} C D
t : Triple F G H
inst_2 : F.Full
inst_3 : F.Faithful
X : C
rw : Mono (t.leftToRight.app X) ↔ Mono (t.leftToRight.app X ≫ H.map (t.adj₁.unit.app X))
rw₁ rw₂ : Mono (t.leftToRight.app X) ↔ Mono (t.leftToRight.app X)
⊢ Mono (t.leftToRight.app X) ↔ Mono (X := obj.{v_2, v_2, u_2, u_2} (𝟭 D) (F.obj X)) (t.adj₂.unit.app (F.obj X))

Tactic:
rw [← leftToRight_app_map_adj₁_unit_app, mono_comp_iff_of_mono]

Premises used: CategoryTheory.mono_comp_iff_of_mono, CategoryTheory.Adjunction.Triple.leftToRight_app_map_adj₁_unit_app
-- Module: Mathlib.CategoryTheory.Adjunction.Triple
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
G : Functor.{v_2, v_1, u_2, u_1} D C
H : Functor.{v_1, v_2, u_1, u_2} C D
t : Triple F G H
inst_2 : F.Full
inst_3 : F.Faithful
inst_4 : H.Full
inst_5 : H.Faithful
X : C
rw : Mono (t.leftToRight.app X) ↔ Mono (F.map (t.adj₂.counit.app X) ≫ t.leftToRight.app X)
rw₁ rw₂ : Mono (t.leftToRight.app X) ↔ Mono (t.leftToRight.app X)
⊢ Mono (t.leftToRight.app X) ↔ Mono (X := (G ⋙ F).obj (H.obj X)) (t.adj₁.counit.app (H.obj X))

Tactic:
rw [← map_adj₂_counit_app_leftToRight_app, mono_comp_iff_of_isIso]

Premises used: CategoryTheory.Adjunction.Triple.map_adj₂_counit_app_leftToRight_app, CategoryTheory.mono_comp_iff_of_isIso
-- Module: Mathlib.CategoryTheory.Adjunction.Triple
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
G : Functor.{v_2, v_1, u_2, u_1} D C
H : Functor.{v_1, v_2, u_1, u_2} C D
t : Triple F G H
inst_2 : F.Full
inst_3 : F.Faithful
h : ∀ (X : C), Mono (t.leftToRight.app X)
X : D
rw : Mono (X := F.obj (G.obj X)) (t.leftToRight.app (G.obj X))
⊢ Mono (t.adj₁.counit.app X ≫ t.adj₂.unit.app X)

Tactic:
rw [← leftToRight_app_obj]

Premises used: CategoryTheory.Adjunction.Triple.leftToRight_app_obj
-- Module: Mathlib.CategoryTheory.Adjunction.Triple
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
G : Functor.{v_2, v_1, u_2, u_1} D C
H : Functor.{v_1, v_2, u_1, u_2} C D
t : Triple F G H
inst_2 : F.Full
inst_3 : F.Faithful
h : ∀ (X : C), Mono (t.leftToRight.app X)
X : D
⊢ Mono (X := F.obj (G.obj X)) (t.leftToRight.app (G.obj X))

Tactic:
h _
-- Module: Mathlib.CategoryTheory.Adjunction.Triple
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
G : Functor.{v_2, v_1, u_2, u_1} D C
H : Functor.{v_1, v_2, u_1, u_2} C D
t : Triple F G H
inst_2 : F.Full
inst_3 : F.Faithful
h : ∀ (X : C), Mono (t.leftToRight.app X)
X : D
⊢ Mono (X := F.obj (G.obj X)) (t.leftToRight.app (G.obj X))

Tactic:
exact h _
-- Module: Mathlib.CategoryTheory.Adjunction.Triple
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
G : Functor.{v_2, v_1, u_2, u_1} D C
H : Functor.{v_1, v_2, u_1, u_2} C D
t : Triple F G H
inst_2 : F.Full
inst_3 : F.Faithful
refine : ∀ (h : ∀ (X : D), Mono (t.adj₁.counit.app X ≫ t.adj₂.unit.app X)) (X : C), Mono (t.leftToRight.app X)
⊢ (∀ (X : C), Mono (t.leftToRight.app X)) ↔ ∀ (X : D), Mono (t.adj₁.counit.app X ≫ t.adj₂.unit.app X)

Tactic:
refine ⟨fun h X ↦ by rw [← leftToRight_app_obj]; exact h _, fun h X ↦ ?_⟩
-- Module: Mathlib.CategoryTheory.Adjunction.Triple
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
G : Functor.{v_2, v_1, u_2, u_1} D C
H : Functor.{v_1, v_2, u_1, u_2} C D
t : Triple F G H
inst_2 : F.Full
inst_3 : F.Faithful
h : ∀ (X : D), Mono (t.adj₁.counit.app X ≫ t.adj₂.unit.app X)
X : C
rw : Mono (X := obj.{v_2, v_2, u_2, u_2} (𝟭 D) (F.obj X)) (t.adj₂.unit.app (F.obj X))
⊢ Mono (t.leftToRight.app X)

Tactic:
rw [mono_leftToRight_app_iff_mono_adj₂_unit_app]

Premises used: CategoryTheory.Adjunction.Triple.mono_leftToRight_app_iff_mono_adj₂_unit_app
-- Module: Mathlib.CategoryTheory.Adjunction.Triple
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
G : Functor.{v_2, v_1, u_2, u_1} D C
H : Functor.{v_1, v_2, u_1, u_2} C D
t : Triple F G H
inst_2 : F.Full
inst_3 : F.Faithful
h : ∀ (X : D), Mono (t.adj₁.counit.app X ≫ t.adj₂.unit.app X)
X : C
⊢ Mono (X := obj.{v_2, v_2, u_2, u_2} (𝟭 D) (F.obj X)) (t.adj₂.unit.app (F.obj X))

Tactic:
simpa using h (F.obj X)

Premises used: CategoryTheory.Functor.obj
-- Module: Mathlib.CategoryTheory.Adjunction.Unique
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
F F' : Functor.{v_1, v_2, u_1, u_2} C D
G : Functor.{v_2, v_1, u_2, u_1} D C
adj1 : F ⊣ G
adj2 : F' ⊣ G
x : C
⊢ ((adj1.homEquiv x (F'.obj x) : Equiv.{v_2 + 1, v_1 + 1} (F.obj x ⟶ F'.obj x) (x ⟶ G.obj (F'.obj x))) :
        (a : F.obj x ⟶ F'.obj x) → x ⟶ G.obj (F'.obj x))
      ((adj1.leftAdjointUniq adj2).hom.app x) =
    adj2.unit.app x

Tactic:
simp [leftAdjointUniq]

Premises used: CategoryTheory.Adjunction.leftAdjointUniq
-- Module: Mathlib.CategoryTheory.Adjunction.Unique
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
F F' : Functor.{v_1, v_2, u_1, u_2} C D
G : Functor.{v_2, v_1, u_2, u_1} D C
adj1 : F ⊣ G
adj2 : F' ⊣ G
w : ∀ (x : C), (adj1.unit ≫ whiskerRight (adj1.leftAdjointUniq adj2).hom G).app x = adj2.unit.app x
⊢ adj1.unit ≫ whiskerRight (adj1.leftAdjointUniq adj2).hom G = adj2.unit

Tactic:
ext x
-- Module: Mathlib.CategoryTheory.Adjunction.Unique
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
F F' : Functor.{v_1, v_2, u_1, u_2} C D
G : Functor.{v_2, v_1, u_2, u_1} D C
adj1 : F ⊣ G
adj2 : F' ⊣ G
x : C
w :
  adj1.unit.app x ≫ (whiskerRight (adj1.leftAdjointUniq adj2).hom G).app x =
    ((adj1.homEquiv x (F'.obj x) : Equiv.{v_2 + 1, v_1 + 1} (F.obj x ⟶ F'.obj x) (x ⟶ G.obj (F'.obj x))) :
        (a : F.obj x ⟶ F'.obj x) → x ⟶ G.obj (F'.obj x))
      ((adj1.leftAdjointUniq adj2).hom.app x)
⊢ (adj1.unit ≫ whiskerRight (adj1.leftAdjointUniq adj2).hom G).app x = adj2.unit.app x

Tactic:
rw [NatTrans.comp_app, ← homEquiv_leftAdjointUniq_hom_app adj1 adj2]

Premises used: CategoryTheory.NatTrans.comp_app, CategoryTheory.Adjunction.homEquiv_leftAdjointUniq_hom_app
-- Module: Mathlib.CategoryTheory.Adjunction.Unique
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
F F' : Functor.{v_1, v_2, u_1, u_2} C D
G : Functor.{v_2, v_1, u_2, u_1} D C
adj1 : F ⊣ G
adj2 : F' ⊣ G
x : C
⊢ adj1.unit.app x ≫ (whiskerRight (adj1.leftAdjointUniq adj2).hom G).app x =
    ((adj1.homEquiv x (F'.obj x) : Equiv.{v_2 + 1, v_1 + 1} (F.obj x ⟶ F'.obj x) (x ⟶ G.obj (F'.obj x))) :
        (a : F.obj x ⟶ F'.obj x) → x ⟶ G.obj (F'.obj x))
      ((adj1.leftAdjointUniq adj2).hom.app x)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Adjunction.Unique
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
F F' : Functor.{v_1, v_2, u_1, u_2} C D
G : Functor.{v_2, v_1, u_2, u_1} D C
adj1 : F ⊣ G
adj2 : F' ⊣ G
x : C
rw :
  adj1.unit.app x ≫ G.map ((adj1.leftAdjointUniq adj2).hom.app x) =
    (adj1.unit ≫ whiskerRight (adj1.leftAdjointUniq adj2).hom G).app x
⊢ adj1.unit.app x ≫ G.map ((adj1.leftAdjointUniq adj2).hom.app x) = adj2.unit.app x

Tactic:
rw [← unit_leftAdjointUniq_hom adj1 adj2]

Premises used: CategoryTheory.Adjunction.unit_leftAdjointUniq_hom
-- Module: Mathlib.CategoryTheory.Adjunction.Unique
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
F F' : Functor.{v_1, v_2, u_1, u_2} C D
G : Functor.{v_2, v_1, u_2, u_1} D C
adj1 : F ⊣ G
adj2 : F' ⊣ G
x : C
⊢ adj1.unit.app x ≫ G.map ((adj1.leftAdjointUniq adj2).hom.app x) =
    (adj1.unit ≫ whiskerRight (adj1.leftAdjointUniq adj2).hom G).app x

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Adjunction.Unique
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
F F' : Functor.{v_1, v_2, u_1, u_2} C D
G : Functor.{v_2, v_1, u_2, u_1} D C
adj1 : F ⊣ G
adj2 : F' ⊣ G
w : ∀ (x : D), (G.whiskerLeft (adj1.leftAdjointUniq adj2).hom ≫ adj2.counit).app x = adj1.counit.app x
⊢ G.whiskerLeft (adj1.leftAdjointUniq adj2).hom ≫ adj2.counit = adj1.counit

Tactic:
ext x
-- Module: Mathlib.CategoryTheory.Adjunction.Unique
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
F F' : Functor.{v_1, v_2, u_1, u_2} C D
G : Functor.{v_2, v_1, u_2, u_1} D C
adj1 : F ⊣ G
adj2 : F' ⊣ G
x : D
w : F.map (adj2.unit.app (G.obj x)) ≫ adj1.counit.app (F'.obj (G.obj x)) ≫ adj2.counit.app x = adj1.counit.app x
⊢ (G.whiskerLeft (adj1.leftAdjointUniq adj2).hom ≫ adj2.counit).app x = adj1.counit.app x

Tactic:
simp only [Functor.comp_obj, Functor.id_obj, leftAdjointUniq, Iso.symm_hom,
    conjugateIsoEquiv_symm_apply_inv, Iso.refl_inv, NatTrans.comp_app, whiskerLeft_app,
    conjugateEquiv_symm_apply_app, NatTrans.id_app, Functor.map_id, Category.id_comp,
    Category.assoc]

Premises used: CategoryTheory.Functor.comp_obj, CategoryTheory.Category.assoc, CategoryTheory.conjugateEquiv_symm_apply_app, CategoryTheory.Adjunction.leftAdjointUniq, CategoryTheory.Iso.symm_hom, CategoryTheory.Functor.whiskerLeft_app, CategoryTheory.Iso.refl_inv, CategoryTheory.Functor.map_id, CategoryTheory.Functor.id_obj, CategoryTheory.NatTrans.id_app, CategoryTheory.conjugateIsoEquiv_symm_apply_inv, CategoryTheory.NatTrans.comp_app, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Adjunction.Unique
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
F F' : Functor.{v_1, v_2, u_1, u_2} C D
G : Functor.{v_2, v_1, u_2, u_1} D C
adj1 : F ⊣ G
adj2 : F' ⊣ G
x : D
w : F.map (adj2.unit.app (G.obj x) ≫ G.map (adj2.counit.app x)) ≫ adj1.counit.app x = adj1.counit.app x
⊢ F.map (adj2.unit.app (G.obj x)) ≫ adj1.counit.app (F'.obj (G.obj x)) ≫ adj2.counit.app x = adj1.counit.app x

Tactic:
rw [← adj1.counit_naturality, ← Category.assoc, ← F.map_comp]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Adjunction.counit_naturality, CategoryTheory.Functor.map_comp
-- Module: Mathlib.CategoryTheory.Adjunction.Unique
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
F F' : Functor.{v_1, v_2, u_1, u_2} C D
G : Functor.{v_2, v_1, u_2, u_1} D C
adj1 : F ⊣ G
adj2 : F' ⊣ G
x : D
⊢ F.map (adj2.unit.app (G.obj x) ≫ G.map (adj2.counit.app x)) ≫ adj1.counit.app x = adj1.counit.app x

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Adjunction.Unique
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
F F' : Functor.{v_1, v_2, u_1, u_2} C D
G : Functor.{v_2, v_1, u_2, u_1} D C
adj1 : F ⊣ G
adj2 : F' ⊣ G
x : D
rw :
  (adj1.leftAdjointUniq adj2).hom.app (G.obj x) ≫ adj2.counit.app x =
    (G.whiskerLeft (adj1.leftAdjointUniq adj2).hom ≫ adj2.counit).app x
⊢ (adj1.leftAdjointUniq adj2).hom.app (G.obj x) ≫ adj2.counit.app x = adj1.counit.app x

Tactic:
rw [← leftAdjointUniq_hom_counit adj1 adj2]

Premises used: CategoryTheory.Adjunction.leftAdjointUniq_hom_counit
-- Module: Mathlib.CategoryTheory.Adjunction.Unique
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
F F' : Functor.{v_1, v_2, u_1, u_2} C D
G : Functor.{v_2, v_1, u_2, u_1} D C
adj1 : F ⊣ G
adj2 : F' ⊣ G
x : D
⊢ (adj1.leftAdjointUniq adj2).hom.app (G.obj x) ≫ adj2.counit.app x =
    (G.whiskerLeft (adj1.leftAdjointUniq adj2).hom ≫ adj2.counit).app x

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Adjunction.Unique
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
F F' : Functor.{v_1, v_2, u_1, u_2} C D
G : Functor.{v_2, v_1, u_2, u_1} D C
adj1 : F ⊣ G
adj2 : F' ⊣ G
x : C
⊢ (adj1.leftAdjointUniq adj2).inv.app x = (adj2.leftAdjointUniq adj1).hom.app x

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Adjunction.Unique
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
F F' F'' : Functor.{v_1, v_2, u_1, u_2} C D
G : Functor.{v_2, v_1, u_2, u_1} D C
adj1 : F ⊣ G
adj2 : F' ⊣ G
adj3 : F'' ⊣ G
⊢ (adj1.leftAdjointUniq adj2).hom ≫ (adj2.leftAdjointUniq adj3).hom = (adj1.leftAdjointUniq adj3).hom

Tactic:
simp [leftAdjointUniq]

Premises used: CategoryTheory.Adjunction.leftAdjointUniq
-- Module: Mathlib.CategoryTheory.Adjunction.Unique
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
F F' F'' : Functor.{v_1, v_2, u_1, u_2} C D
G : Functor.{v_2, v_1, u_2, u_1} D C
adj1 : F ⊣ G
adj2 : F' ⊣ G
adj3 : F'' ⊣ G
x : C
rw :
  (adj1.leftAdjointUniq adj2).hom.app x ≫ (adj2.leftAdjointUniq adj3).hom.app x =
    ((adj1.leftAdjointUniq adj2).hom ≫ (adj2.leftAdjointUniq adj3).hom).app x
⊢ (adj1.leftAdjointUniq adj2).hom.app x ≫ (adj2.leftAdjointUniq adj3).hom.app x = (adj1.leftAdjointUniq adj3).hom.app x

Tactic:
rw [← leftAdjointUniq_trans adj1 adj2 adj3]

Premises used: CategoryTheory.Adjunction.leftAdjointUniq_trans
-- Module: Mathlib.CategoryTheory.Adjunction.Unique
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
F F' F'' : Functor.{v_1, v_2, u_1, u_2} C D
G : Functor.{v_2, v_1, u_2, u_1} D C
adj1 : F ⊣ G
adj2 : F' ⊣ G
adj3 : F'' ⊣ G
x : C
⊢ (adj1.leftAdjointUniq adj2).hom.app x ≫ (adj2.leftAdjointUniq adj3).hom.app x =
    ((adj1.leftAdjointUniq adj2).hom ≫ (adj2.leftAdjointUniq adj3).hom).app x

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Adjunction.Unique
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
G : Functor.{v_2, v_1, u_2, u_1} D C
adj1 : F ⊣ G
⊢ (adj1.leftAdjointUniq adj1).hom = 𝟙 F

Tactic:
simp [leftAdjointUniq]

Premises used: CategoryTheory.Adjunction.leftAdjointUniq
-- Module: Mathlib.CategoryTheory.Adjunction.Unique
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
G G' : Functor.{v_2, v_1, u_2, u_1} D C
adj1 : F ⊣ G
adj2 : F ⊣ G'
x : D
⊢ ((Equiv.symm (adj2.homEquiv (G.obj x) x) : Equiv.{v_1 + 1, v_2 + 1} (G.obj x ⟶ G'.obj x) (F.obj (G.obj x) ⟶ x)) :
        (a : G.obj x ⟶ G'.obj x) → F.obj (G.obj x) ⟶ x)
      ((adj1.rightAdjointUniq adj2).hom.app x) =
    adj1.counit.app x

Tactic:
simp [rightAdjointUniq]

Premises used: CategoryTheory.Adjunction.rightAdjointUniq
-- Module: Mathlib.CategoryTheory.Adjunction.Unique
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
G G' : Functor.{v_2, v_1, u_2, u_1} D C
adj1 : F ⊣ G
adj2 : F ⊣ G'
x : C
simp : adj1.unit.app x ≫ adj2.unit.app (G.obj (F.obj x)) ≫ G'.map (adj1.counit.app (F.obj x)) = adj2.unit.app x
⊢ adj1.unit.app x ≫ (adj1.rightAdjointUniq adj2).hom.app (F.obj x) = adj2.unit.app x

Tactic:
simp only [Functor.id_obj, Functor.comp_obj, rightAdjointUniq, conjugateIsoEquiv_apply_hom,
    Iso.refl_hom, conjugateEquiv_apply_app, NatTrans.id_app, Functor.map_id, Category.id_comp]

Premises used: CategoryTheory.Functor.comp_obj, CategoryTheory.conjugateEquiv_apply_app, CategoryTheory.Functor.map_id, CategoryTheory.Functor.id_obj, CategoryTheory.NatTrans.id_app, CategoryTheory.Adjunction.rightAdjointUniq, CategoryTheory.conjugateIsoEquiv_apply_hom, CategoryTheory.Iso.refl_hom, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Adjunction.Unique
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
G G' : Functor.{v_2, v_1, u_2, u_1} D C
adj1 : F ⊣ G
adj2 : F ⊣ G'
x : C
rw : adj2.unit.app x ≫ G'.map (F.map (adj1.unit.app x) ≫ adj1.counit.app (F.obj x)) = adj2.unit.app x
⊢ adj1.unit.app x ≫ adj2.unit.app (G.obj (F.obj x)) ≫ G'.map (adj1.counit.app (F.obj x)) = adj2.unit.app x

Tactic:
rw [← adj2.unit_naturality_assoc, ← G'.map_comp]

Premises used: CategoryTheory.Functor.map_comp, CategoryTheory.Adjunction.unit_naturality_assoc
-- Module: Mathlib.CategoryTheory.Adjunction.Unique
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
G G' : Functor.{v_2, v_1, u_2, u_1} D C
adj1 : F ⊣ G
adj2 : F ⊣ G'
x : C
⊢ adj2.unit.app x ≫ G'.map (F.map (adj1.unit.app x) ≫ adj1.counit.app (F.obj x)) = adj2.unit.app x

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Adjunction.Unique
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
G G' : Functor.{v_2, v_1, u_2, u_1} D C
adj1 : F ⊣ G
adj2 : F ⊣ G'
w : ∀ (x : C), (adj1.unit ≫ F.whiskerLeft (adj1.rightAdjointUniq adj2).hom).app x = adj2.unit.app x
⊢ adj1.unit ≫ F.whiskerLeft (adj1.rightAdjointUniq adj2).hom = adj2.unit

Tactic:
ext x
-- Module: Mathlib.CategoryTheory.Adjunction.Unique
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
G G' : Functor.{v_2, v_1, u_2, u_1} D C
adj1 : F ⊣ G
adj2 : F ⊣ G'
x : C
⊢ (adj1.unit ≫ F.whiskerLeft (adj1.rightAdjointUniq adj2).hom).app x = adj2.unit.app x

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Adjunction.Unique
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
G G' : Functor.{v_2, v_1, u_2, u_1} D C
adj1 : F ⊣ G
adj2 : F ⊣ G'
x : D
⊢ F.map ((adj1.rightAdjointUniq adj2).hom.app x) ≫ adj2.counit.app x = adj1.counit.app x

Tactic:
simp [rightAdjointUniq]

Premises used: CategoryTheory.Adjunction.rightAdjointUniq
-- Module: Mathlib.CategoryTheory.Adjunction.Unique
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
G G' : Functor.{v_2, v_1, u_2, u_1} D C
adj1 : F ⊣ G
adj2 : F ⊣ G'
w : ∀ (x : D), (whiskerRight (adj1.rightAdjointUniq adj2).hom F ≫ adj2.counit).app x = adj1.counit.app x
⊢ whiskerRight (adj1.rightAdjointUniq adj2).hom F ≫ adj2.counit = adj1.counit

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Adjunction.Unique
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
G G' : Functor.{v_2, v_1, u_2, u_1} D C
adj1 : F ⊣ G
adj2 : F ⊣ G'
x : D
⊢ (whiskerRight (adj1.rightAdjointUniq adj2).hom F ≫ adj2.counit).app x = adj1.counit.app x

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Adjunction.Unique
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
G G' : Functor.{v_2, v_1, u_2, u_1} D C
adj1 : F ⊣ G
adj2 : F ⊣ G'
x : D
⊢ (adj1.rightAdjointUniq adj2).inv.app x = (adj2.rightAdjointUniq adj1).hom.app x

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Adjunction.Unique
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
G G' G'' : Functor.{v_2, v_1, u_2, u_1} D C
adj1 : F ⊣ G
adj2 : F ⊣ G'
adj3 : F ⊣ G''
⊢ (adj1.rightAdjointUniq adj2).hom ≫ (adj2.rightAdjointUniq adj3).hom = (adj1.rightAdjointUniq adj3).hom

Tactic:
simp [rightAdjointUniq]

Premises used: CategoryTheory.Adjunction.rightAdjointUniq
-- Module: Mathlib.CategoryTheory.Adjunction.Unique
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
G G' G'' : Functor.{v_2, v_1, u_2, u_1} D C
adj1 : F ⊣ G
adj2 : F ⊣ G'
adj3 : F ⊣ G''
x : D
rw :
  (adj1.rightAdjointUniq adj2).hom.app x ≫ (adj2.rightAdjointUniq adj3).hom.app x =
    ((adj1.rightAdjointUniq adj2).hom ≫ (adj2.rightAdjointUniq adj3).hom).app x
⊢ (adj1.rightAdjointUniq adj2).hom.app x ≫ (adj2.rightAdjointUniq adj3).hom.app x =
    (adj1.rightAdjointUniq adj3).hom.app x

Tactic:
rw [← rightAdjointUniq_trans adj1 adj2 adj3]

Premises used: CategoryTheory.Adjunction.rightAdjointUniq_trans
-- Module: Mathlib.CategoryTheory.Adjunction.Unique
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
G G' G'' : Functor.{v_2, v_1, u_2, u_1} D C
adj1 : F ⊣ G
adj2 : F ⊣ G'
adj3 : F ⊣ G''
x : D
⊢ (adj1.rightAdjointUniq adj2).hom.app x ≫ (adj2.rightAdjointUniq adj3).hom.app x =
    ((adj1.rightAdjointUniq adj2).hom ≫ (adj2.rightAdjointUniq adj3).hom).app x

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Adjunction.Unique
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
G : Functor.{v_2, v_1, u_2, u_1} D C
adj1 : F ⊣ G
⊢ Eq (α := G ⟶ G) (Iso.hom ((conjugateIsoEquiv adj1 adj1 : (a : F ≅ F) → G ≅ G) (Iso.refl F)) : G ⟶ G) (𝟙 G : G ⟶ G)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Adjunction.Whiskering
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} E
F : Functor.{v_2, v_3, u_2, u_3} D E
G : Functor.{v_3, v_2, u_3, u_2} E D
adj : F ⊣ G
X Y : Functor.{v_1, v_2, u_1, u_2} C D
f : X ⟶ Y
w :
  ∀ (x : C),
    (map (𝟭 (Functor.{v_1, v_2, u_1, u_2} C D)) f ≫
            (obj (𝟭 (Functor.{v_1, v_2, u_1, u_2} C D)) Y).rightUnitor.inv ≫
              Y.whiskerLeft adj.unit ≫ (Y.associator F G).inv).app
        x =
      NatTrans.app
        (((obj (𝟭 (Functor.{v_1, v_2, u_1, u_2} C D)) X).rightUnitor.inv ≫
            X.whiskerLeft adj.unit ≫ (X.associator F G).inv) ≫
          map (obj (whiskeringRight C D E) F ⋙ obj (whiskeringRight C E D) G) f)
        x
⊢ map (𝟭 (Functor.{v_1, v_2, u_1, u_2} C D)) f ≫
      (obj (𝟭 (Functor.{v_1, v_2, u_1, u_2} C D)) Y).rightUnitor.inv ≫ Y.whiskerLeft adj.unit ≫ (Y.associator F G).inv =
    ((obj (𝟭 (Functor.{v_1, v_2, u_1, u_2} C D)) X).rightUnitor.inv ≫ X.whiskerLeft adj.unit ≫ (X.associator F G).inv) ≫
      map (obj (whiskeringRight C D E) F ⋙ obj (whiskeringRight C E D) G) f

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Adjunction.Whiskering
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} E
F : Functor.{v_2, v_3, u_2, u_3} D E
G : Functor.{v_3, v_2, u_3, u_2} E D
adj : F ⊣ G
X Y : Functor.{v_1, v_2, u_1, u_2} C D
f : X ⟶ Y
x : C
⊢ (map (𝟭 (Functor.{v_1, v_2, u_1, u_2} C D)) f ≫
          (obj (𝟭 (Functor.{v_1, v_2, u_1, u_2} C D)) Y).rightUnitor.inv ≫
            Y.whiskerLeft adj.unit ≫ (Y.associator F G).inv).app
      x =
    NatTrans.app
      (((obj (𝟭 (Functor.{v_1, v_2, u_1, u_2} C D)) X).rightUnitor.inv ≫
          X.whiskerLeft adj.unit ≫ (X.associator F G).inv) ≫
        map (obj (whiskeringRight C D E) F ⋙ obj (whiskeringRight C E D) G) f)
      x

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Adjunction.Whiskering
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} E
F : Functor.{v_2, v_3, u_2, u_3} D E
G : Functor.{v_3, v_2, u_3, u_2} E D
adj : F ⊣ G
X Y : Functor.{v_1, v_3, u_1, u_3} C E
f : X ⟶ Y
w :
  ∀ (x : C),
    (map (obj (whiskeringRight C E D) G ⋙ obj (whiskeringRight C D E) F) f ≫
            (Y.associator G F).hom ≫ Y.whiskerLeft adj.counit ≫ Y.rightUnitor.hom).app
        x =
      NatTrans.app
        (((X.associator G F).hom ≫ X.whiskerLeft adj.counit ≫ X.rightUnitor.hom) ≫
          map (𝟭 (Functor.{v_1, v_3, u_1, u_3} C E)) f)
        x
⊢ map (obj (whiskeringRight C E D) G ⋙ obj (whiskeringRight C D E) F) f ≫
      (Y.associator G F).hom ≫ Y.whiskerLeft adj.counit ≫ Y.rightUnitor.hom =
    ((X.associator G F).hom ≫ X.whiskerLeft adj.counit ≫ X.rightUnitor.hom) ≫
      map (𝟭 (Functor.{v_1, v_3, u_1, u_3} C E)) f

Tactic:
ext