-- Mathlib/CategoryTheory/Adjunction/Mates.lean
theorem unit_conjugateEquiv (α : L₂ ⟶ L₁) (c : C) :
    adj₁.unit.app _ ≫ (conjugateEquiv adj₁ adj₂ α).app _ =
      adj₂.unit.app c ≫ R₂.map (α.app _)

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₁
c : C
⊢ adj₁.unit.app c ≫
      adj₂.unit.app (R₁.obj (L₁.obj c)) ≫
        R₂.map (𝟙 (L₂.obj (R₁.obj (L₁.obj c))) ≫ α.app (R₁.obj (L₁.obj c)) ≫ 𝟙 (L₁.obj (R₁.obj (L₁.obj c)))) ≫
          R₂.map (adj₁.counit.app (L₁.obj c)) =
    adj₂.unit.app c ≫ R₂.map (α.app c)

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

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₁
c : C
this :
  (𝟭 C).map (adj₁.unit.app c) ≫ ((mateEquiv adj₁ adj₂) (L₂.leftUnitor.hom ≫ α ≫ L₁.rightUnitor.inv)).app (L₁.obj c) =
    adj₂.unit.app ((𝟭 C).obj ((𝟭 C).obj c)) ≫ R₂.map ((L₂.leftUnitor.hom ≫ α ≫ L₁.rightUnitor.inv).app ((𝟭 C).obj c))
⊢ adj₁.unit.app c ≫
      adj₂.unit.app (R₁.obj (L₁.obj c)) ≫
        R₂.map (𝟙 (L₂.obj (R₁.obj (L₁.obj c))) ≫ α.app (R₁.obj (L₁.obj c)) ≫ 𝟙 (L₁.obj (R₁.obj (L₁.obj c)))) ≫
          R₂.map (adj₁.counit.app (L₁.obj c)) =
    adj₂.unit.app c ≫ R₂.map (α.app c)

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₁
c : C
this :
  adj₁.unit.app c ≫
      adj₂.unit.app (R₁.obj (L₁.obj c)) ≫
        R₂.map (𝟙 (L₂.obj (R₁.obj (L₁.obj c))) ≫ α.app (R₁.obj (L₁.obj c)) ≫ 𝟙 (L₁.obj (R₁.obj (L₁.obj c)))) ≫
          R₂.map (adj₁.counit.app (L₁.obj c)) =
    adj₂.unit.app c ≫ R₂.map (𝟙 (L₂.obj c) ≫ α.app c ≫ 𝟙 (L₁.obj c))
⊢ adj₁.unit.app c ≫
      adj₂.unit.app (R₁.obj (L₁.obj c)) ≫
        R₂.map (𝟙 (L₂.obj (R₁.obj (L₁.obj c))) ≫ α.app (R₁.obj (L₁.obj c)) ≫ 𝟙 (L₁.obj (R₁.obj (L₁.obj c)))) ≫
          R₂.map (adj₁.counit.app (L₁.obj c)) =
    adj₂.unit.app c ≫ R₂.map (α.app c)

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₁
c : C
this :
  adj₁.unit.app c ≫
      adj₂.unit.app (R₁.obj (L₁.obj c)) ≫
        R₂.map (𝟙 (L₂.obj (R₁.obj (L₁.obj c))) ≫ α.app (R₁.obj (L₁.obj c)) ≫ 𝟙 (L₁.obj (R₁.obj (L₁.obj c)))) ≫
          R₂.map (adj₁.counit.app (L₁.obj c)) =
    adj₂.unit.app c ≫ R₂.map (𝟙 (L₂.obj c) ≫ α.app c ≫ 𝟙 (L₁.obj c))
⊢ adj₂.unit.app c ≫ R₂.map (𝟙 (L₂.obj c) ≫ α.app c ≫ 𝟙 (L₁.obj c)) = adj₂.unit.app c ≫ R₂.map (α.app c)

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₁
c : C
⊢ adj₁.unit.app c ≫ ((conjugateEquiv adj₁ adj₂) α).app (L₁.obj c) = adj₂.unit.app c ≫ R₂.map (α.app c)

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₁
c : C
⊢ adj₁.unit.app c ≫
      𝟙 (R₁.obj (L₁.obj c)) ≫
        (adj₂.unit.app (R₁.obj (L₁.obj c)) ≫
            R₂.map (𝟙 (L₂.obj (R₁.obj (L₁.obj c))) ≫ α.app (R₁.obj (L₁.obj c)) ≫ 𝟙 (L₁.obj (R₁.obj (L₁.obj c)))) ≫
              R₂.map (adj₁.counit.app (L₁.obj c))) ≫
          𝟙 (R₂.obj (L₁.obj c)) =
    adj₂.unit.app c ≫ R₂.map (α.app c)

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₁
c : C
⊢ adj₁.unit.app c ≫
      𝟙 (R₁.obj (L₁.obj c)) ≫
        (adj₂.unit.app (R₁.obj (L₁.obj c)) ≫
            R₂.map (𝟙 (L₂.obj (R₁.obj (L₁.obj c))) ≫ α.app (R₁.obj (L₁.obj c)) ≫ 𝟙 (L₁.obj (R₁.obj (L₁.obj c)))) ≫
              R₂.map (adj₁.counit.app (L₁.obj c))) ≫
          𝟙 (R₂.obj (L₁.obj c)) =
    adj₂.unit.app c ≫ R₂.map (α.app c)

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₁
c : C
⊢ adj₁.unit.app c ≫
      adj₂.unit.app (R₁.obj (L₁.obj c)) ≫
        R₂.map (𝟙 (L₂.obj (R₁.obj (L₁.obj c))) ≫ α.app (R₁.obj (L₁.obj c)) ≫ 𝟙 (L₁.obj (R₁.obj (L₁.obj c)))) ≫
          R₂.map (adj₁.counit.app (L₁.obj c)) =
    adj₂.unit.app c ≫ R₂.map (α.app c)

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₁
c : C
this :
  adj₁.unit.app c ≫
      adj₂.unit.app (R₁.obj (L₁.obj c)) ≫
        R₂.map (𝟙 (L₂.obj (R₁.obj (L₁.obj c))) ≫ α.app (R₁.obj (L₁.obj c)) ≫ 𝟙 (L₁.obj (R₁.obj (L₁.obj c)))) ≫
          R₂.map (adj₁.counit.app (L₁.obj c)) =
    adj₂.unit.app c ≫ R₂.map (𝟙 (L₂.obj c) ≫ α.app c ≫ 𝟙 (L₁.obj c))
⊢ adj₂.unit.app c ≫ R₂.map (𝟙 (L₂.obj c) ≫ α.app c ≫ 𝟙 (L₁.obj c)) = adj₂.unit.app c ≫ R₂.map (α.app c)

Tactic:
simp

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₁
c : C
this :
  (𝟭 C).map (adj₁.unit.app c) ≫ ((mateEquiv adj₁ adj₂) (L₂.leftUnitor.hom ≫ α ≫ L₁.rightUnitor.inv)).app (L₁.obj c) =
    adj₂.unit.app ((𝟭 C).obj ((𝟭 C).obj c)) ≫ R₂.map ((L₂.leftUnitor.hom ≫ α ≫ L₁.rightUnitor.inv).app ((𝟭 C).obj c))
⊢ adj₁.unit.app c ≫
      adj₂.unit.app (R₁.obj (L₁.obj c)) ≫
        R₂.map (𝟙 (L₂.obj (R₁.obj (L₁.obj c))) ≫ α.app (R₁.obj (L₁.obj c)) ≫ 𝟙 (L₁.obj (R₁.obj (L₁.obj c)))) ≫
          R₂.map (adj₁.counit.app (L₁.obj c)) =
    adj₂.unit.app c ≫ R₂.map (α.app c)

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₁
c : C
this :
  adj₁.unit.app c ≫
      adj₂.unit.app (R₁.obj (L₁.obj c)) ≫
        R₂.map (𝟙 (L₂.obj (R₁.obj (L₁.obj c))) ≫ α.app (R₁.obj (L₁.obj c)) ≫ 𝟙 (L₁.obj (R₁.obj (L₁.obj c)))) ≫
          R₂.map (adj₁.counit.app (L₁.obj c)) =
    adj₂.unit.app c ≫ R₂.map (𝟙 (L₂.obj c) ≫ α.app c ≫ 𝟙 (L₁.obj c))
⊢ adj₁.unit.app c ≫
      adj₂.unit.app (R₁.obj (L₁.obj c)) ≫
        R₂.map (𝟙 (L₂.obj (R₁.obj (L₁.obj c))) ≫ α.app (R₁.obj (L₁.obj c)) ≫ 𝟙 (L₁.obj (R₁.obj (L₁.obj c)))) ≫
          R₂.map (adj₁.counit.app (L₁.obj c)) =
    adj₂.unit.app c ≫ R₂.map (α.app c)