-- Mathlib/CategoryTheory/Adjunction/Mates.lean
theorem conjugateEquiv_counit (α : L₂ ⟶ L₁) (d : D) :
    L₂.map ((conjugateEquiv adj₁ adj₂ α).app _) ≫ adj₂.counit.app d =
      α.app _ ≫ adj₁.counit.app d

Proof state:
C : Type u₁
D : Type u₂
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Category.{v₂, u₂} D
L₁ L₂ : C ⥤ D
R₁ R₂ : D ⥤ C
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
α : L₂ ⟶ L₁
d : D
this :
  L₂.map
        (adj₂.unit.app (R₁.obj d) ≫
          R₂.map (𝟙 (L₂.obj (R₁.obj d)) ≫ α.app (R₁.obj d) ≫ 𝟙 (L₁.obj (R₁.obj d))) ≫ R₂.map (adj₁.counit.app d)) ≫
      adj₂.counit.app d =
    (𝟙 (L₂.obj (R₁.obj d)) ≫ α.app (R₁.obj d) ≫ 𝟙 (L₁.obj (R₁.obj d))) ≫ adj₁.counit.app d
⊢ (𝟙 (L₂.obj (R₁.obj d)) ≫ α.app (R₁.obj d) ≫ 𝟙 (L₁.obj (R₁.obj d))) ≫ adj₁.counit.app d =
    α.app (R₁.obj d) ≫ adj₁.counit.app d

Tactic:
simp only [comp_id, id_comp]

Result:
no goals

Proof state:
C : Type u₁
D : Type u₂
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Category.{v₂, u₂} D
L₁ L₂ : C ⥤ D
R₁ R₂ : D ⥤ C
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
α : L₂ ⟶ L₁
d : D
this :
  L₂.map
        (adj₂.unit.app (R₁.obj d) ≫
          R₂.map (𝟙 (L₂.obj (R₁.obj d)) ≫ α.app (R₁.obj d) ≫ 𝟙 (L₁.obj (R₁.obj d))) ≫ R₂.map (adj₁.counit.app d)) ≫
      adj₂.counit.app d =
    (𝟙 (L₂.obj (R₁.obj d)) ≫ α.app (R₁.obj d) ≫ 𝟙 (L₁.obj (R₁.obj d))) ≫ adj₁.counit.app d
⊢ L₂.map
        (adj₂.unit.app (R₁.obj d) ≫
          R₂.map (𝟙 (L₂.obj (R₁.obj d)) ≫ α.app (R₁.obj d) ≫ 𝟙 (L₁.obj (R₁.obj d))) ≫ R₂.map (adj₁.counit.app d)) ≫
      adj₂.counit.app d =
    α.app (R₁.obj d) ≫ adj₁.counit.app d

Tactic:
rw [this]

Result:
C : Type u₁
D : Type u₂
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Category.{v₂, u₂} D
L₁ L₂ : C ⥤ D
R₁ R₂ : D ⥤ C
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
α : L₂ ⟶ L₁
d : D
this :
  L₂.map
        (adj₂.unit.app (R₁.obj d) ≫
          R₂.map (𝟙 (L₂.obj (R₁.obj d)) ≫ α.app (R₁.obj d) ≫ 𝟙 (L₁.obj (R₁.obj d))) ≫ R₂.map (adj₁.counit.app d)) ≫
      adj₂.counit.app d =
    (𝟙 (L₂.obj (R₁.obj d)) ≫ α.app (R₁.obj d) ≫ 𝟙 (L₁.obj (R₁.obj d))) ≫ adj₁.counit.app d
⊢ (𝟙 (L₂.obj (R₁.obj d)) ≫ α.app (R₁.obj d) ≫ 𝟙 (L₁.obj (R₁.obj d))) ≫ adj₁.counit.app d =
    α.app (R₁.obj d) ≫ adj₁.counit.app d

Proof state:
C : Type u₁
D : Type u₂
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Category.{v₂, u₂} D
L₁ L₂ : C ⥤ D
R₁ R₂ : D ⥤ C
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
α : L₂ ⟶ L₁
d : D
this :
  L₂.map (((mateEquiv adj₁ adj₂) (L₂.leftUnitor.hom ≫ α ≫ L₁.rightUnitor.inv)).app d) ≫ adj₂.counit.app ((𝟭 D).obj d) =
    (L₂.leftUnitor.hom ≫ α ≫ L₁.rightUnitor.inv).app (R₁.obj d) ≫ (𝟭 D).map (adj₁.counit.app d)
⊢ L₂.map
        (adj₂.unit.app (R₁.obj d) ≫
          R₂.map (𝟙 (L₂.obj (R₁.obj d)) ≫ α.app (R₁.obj d) ≫ 𝟙 (L₁.obj (R₁.obj d))) ≫ R₂.map (adj₁.counit.app d)) ≫
      adj₂.counit.app d =
    α.app (R₁.obj d) ≫ adj₁.counit.app d

Tactic:
dsimp at this

Result:
C : Type u₁
D : Type u₂
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Category.{v₂, u₂} D
L₁ L₂ : C ⥤ D
R₁ R₂ : D ⥤ C
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
α : L₂ ⟶ L₁
d : D
this :
  L₂.map
        (adj₂.unit.app (R₁.obj d) ≫
          R₂.map (𝟙 (L₂.obj (R₁.obj d)) ≫ α.app (R₁.obj d) ≫ 𝟙 (L₁.obj (R₁.obj d))) ≫ R₂.map (adj₁.counit.app d)) ≫
      adj₂.counit.app d =
    (𝟙 (L₂.obj (R₁.obj d)) ≫ α.app (R₁.obj d) ≫ 𝟙 (L₁.obj (R₁.obj d))) ≫ adj₁.counit.app d
⊢ L₂.map
        (adj₂.unit.app (R₁.obj d) ≫
          R₂.map (𝟙 (L₂.obj (R₁.obj d)) ≫ α.app (R₁.obj d) ≫ 𝟙 (L₁.obj (R₁.obj d))) ≫ R₂.map (adj₁.counit.app d)) ≫
      adj₂.counit.app d =
    α.app (R₁.obj d) ≫ adj₁.counit.app d

Proof state:
C : Type u₁
D : Type u₂
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Category.{v₂, u₂} D
L₁ L₂ : C ⥤ D
R₁ R₂ : D ⥤ C
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
α : L₂ ⟶ L₁
d : D
⊢ L₂.map
        (𝟙 (R₁.obj d) ≫
          (adj₂.unit.app (R₁.obj d) ≫
              R₂.map (𝟙 (L₂.obj (R₁.obj d)) ≫ α.app (R₁.obj d) ≫ 𝟙 (L₁.obj (R₁.obj d))) ≫ R₂.map (adj₁.counit.app d)) ≫
            𝟙 (R₂.obj d)) ≫
      adj₂.counit.app d =
    α.app (R₁.obj d) ≫ adj₁.counit.app d

Tactic:
rw [id_comp, comp_id]

Result:
C : Type u₁
D : Type u₂
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Category.{v₂, u₂} D
L₁ L₂ : C ⥤ D
R₁ R₂ : D ⥤ C
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
α : L₂ ⟶ L₁
d : D
⊢ L₂.map
        (adj₂.unit.app (R₁.obj d) ≫
          R₂.map (𝟙 (L₂.obj (R₁.obj d)) ≫ α.app (R₁.obj d) ≫ 𝟙 (L₁.obj (R₁.obj d))) ≫ R₂.map (adj₁.counit.app d)) ≫
      adj₂.counit.app d =
    α.app (R₁.obj d) ≫ adj₁.counit.app d

Proof state:
C : Type u₁
D : Type u₂
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Category.{v₂, u₂} D
L₁ L₂ : C ⥤ D
R₁ R₂ : D ⥤ C
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
α : L₂ ⟶ L₁
d : D
⊢ L₂.map (((conjugateEquiv adj₁ adj₂) α).app d) ≫ adj₂.counit.app d = α.app (R₁.obj d) ≫ adj₁.counit.app d

Tactic:
dsimp [conjugateEquiv]

Result:
C : Type u₁
D : Type u₂
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Category.{v₂, u₂} D
L₁ L₂ : C ⥤ D
R₁ R₂ : D ⥤ C
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
α : L₂ ⟶ L₁
d : D
⊢ L₂.map
        (𝟙 (R₁.obj d) ≫
          (adj₂.unit.app (R₁.obj d) ≫
              R₂.map (𝟙 (L₂.obj (R₁.obj d)) ≫ α.app (R₁.obj d) ≫ 𝟙 (L₁.obj (R₁.obj d))) ≫ R₂.map (adj₁.counit.app d)) ≫
            𝟙 (R₂.obj d)) ≫
      adj₂.counit.app d =
    α.app (R₁.obj d) ≫ adj₁.counit.app d

Proof state:
C : Type u₁
D : Type u₂
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Category.{v₂, u₂} D
L₁ L₂ : C ⥤ D
R₁ R₂ : D ⥤ C
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
α : L₂ ⟶ L₁
d : D
⊢ L₂.map
        (adj₂.unit.app (R₁.obj d) ≫
          R₂.map (𝟙 (L₂.obj (R₁.obj d)) ≫ α.app (R₁.obj d) ≫ 𝟙 (L₁.obj (R₁.obj d))) ≫ R₂.map (adj₁.counit.app d)) ≫
      adj₂.counit.app d =
    α.app (R₁.obj d) ≫ adj₁.counit.app d

Tactic:
have := mateEquiv_counit adj₁ adj₂ (L₂.leftUnitor.hom ≫ α ≫ L₁.rightUnitor.inv) d

Result:
C : Type u₁
D : Type u₂
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Category.{v₂, u₂} D
L₁ L₂ : C ⥤ D
R₁ R₂ : D ⥤ C
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
α : L₂ ⟶ L₁
d : D
this :
  L₂.map (((mateEquiv adj₁ adj₂) (L₂.leftUnitor.hom ≫ α ≫ L₁.rightUnitor.inv)).app d) ≫ adj₂.counit.app ((𝟭 D).obj d) =
    (L₂.leftUnitor.hom ≫ α ≫ L₁.rightUnitor.inv).app (R₁.obj d) ≫ (𝟭 D).map (adj₁.counit.app d)
⊢ L₂.map
        (adj₂.unit.app (R₁.obj d) ≫
          R₂.map (𝟙 (L₂.obj (R₁.obj d)) ≫ α.app (R₁.obj d) ≫ 𝟙 (L₁.obj (R₁.obj d))) ≫ R₂.map (adj₁.counit.app d)) ≫
      adj₂.counit.app d =
    α.app (R₁.obj d) ≫ adj₁.counit.app d