-- Mathlib/CategoryTheory/Adjunction/Mates.lean
theorem unit_mateEquiv (α : TwoSquare G L₁ L₂ H) (c : C) :
    G.map (adj₁.unit.app c) ≫ (mateEquiv adj₁ adj₂ α).app _ =
      adj₂.unit.app _ ≫ R₂.map (α.app _)

Proof state:
C : Type u₁
D : Type u₂
E : Type u₃
F : Type u₄
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₂, u₂} D
inst✝¹ : Category.{v₃, u₃} E
inst✝ : Category.{v₄, u₄} F
G : C ⥤ E
H : D ⥤ F
L₁ : C ⥤ D
R₁ : D ⥤ C
L₂ : E ⥤ F
R₂ : F ⥤ E
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
α : TwoSquare G L₁ L₂ H
c : C
⊢ adj₂.unit.app (G.obj c) ≫
      R₂.map (α.app c ≫ (L₁ ⋙ H).map (adj₁.unit.app c)) ≫ R₂.map (H.map (adj₁.counit.app (L₁.obj c))) =
    adj₂.unit.app (G.obj c) ≫ R₂.map (α.app c)

Tactic:
rw [R₂.map_comp]

Result:
C : Type u₁
D : Type u₂
E : Type u₃
F : Type u₄
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₂, u₂} D
inst✝¹ : Category.{v₃, u₃} E
inst✝ : Category.{v₄, u₄} F
G : C ⥤ E
H : D ⥤ F
L₁ : C ⥤ D
R₁ : D ⥤ C
L₂ : E ⥤ F
R₂ : F ⥤ E
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
α : TwoSquare G L₁ L₂ H
c : C
⊢ adj₂.unit.app (G.obj c) ≫
      (R₂.map (α.app c) ≫ R₂.map ((L₁ ⋙ H).map (adj₁.unit.app c))) ≫ R₂.map (H.map (adj₁.counit.app (L₁.obj c))) =
    adj₂.unit.app (G.obj c) ≫ R₂.map (α.app c)

Proof state:
C : Type u₁
D : Type u₂
E : Type u₃
F : Type u₄
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₂, u₂} D
inst✝¹ : Category.{v₃, u₃} E
inst✝ : Category.{v₄, u₄} F
G : C ⥤ E
H : D ⥤ F
L₁ : C ⥤ D
R₁ : D ⥤ C
L₂ : E ⥤ F
R₂ : F ⥤ E
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
α : TwoSquare G L₁ L₂ H
c : C
⊢ G.map (adj₁.unit.app c) ≫ ((mateEquiv adj₁ adj₂) α).app (L₁.obj c) =
    adj₂.unit.app (G.obj ((𝟭 C).obj c)) ≫ R₂.map (α.app ((𝟭 C).obj c))

Tactic:
dsimp [mateEquiv]

Result:
C : Type u₁
D : Type u₂
E : Type u₃
F : Type u₄
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₂, u₂} D
inst✝¹ : Category.{v₃, u₃} E
inst✝ : Category.{v₄, u₄} F
G : C ⥤ E
H : D ⥤ F
L₁ : C ⥤ D
R₁ : D ⥤ C
L₂ : E ⥤ F
R₂ : F ⥤ E
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
α : TwoSquare G L₁ L₂ H
c : C
⊢ G.map (adj₁.unit.app c) ≫
      adj₂.unit.app (G.obj (R₁.obj (L₁.obj c))) ≫
        R₂.map (α.natTrans.app (R₁.obj (L₁.obj c))) ≫ R₂.map (H.map (adj₁.counit.app (L₁.obj c))) =
    adj₂.unit.app (G.obj c) ≫ R₂.map (α.app c)

Proof state:
C : Type u₁
D : Type u₂
E : Type u₃
F : Type u₄
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₂, u₂} D
inst✝¹ : Category.{v₃, u₃} E
inst✝ : Category.{v₄, u₄} F
G : C ⥤ E
H : D ⥤ F
L₁ : C ⥤ D
R₁ : D ⥤ C
L₂ : E ⥤ F
R₂ : F ⥤ E
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
α : TwoSquare G L₁ L₂ H
c : C
⊢ adj₂.unit.app (G.obj c) ≫ R₂.map (α.app c) ≫ R₂.map (H.map (𝟙 (L₁.obj c))) =
    adj₂.unit.app (G.obj c) ≫ R₂.map (α.app c)

Tactic:
simp only [comp_obj, map_id, comp_id]

Result:
no goals

Proof state:
C : Type u₁
D : Type u₂
E : Type u₃
F : Type u₄
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₂, u₂} D
inst✝¹ : Category.{v₃, u₃} E
inst✝ : Category.{v₄, u₄} F
G : C ⥤ E
H : D ⥤ F
L₁ : C ⥤ D
R₁ : D ⥤ C
L₂ : E ⥤ F
R₂ : F ⥤ E
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
α : TwoSquare G L₁ L₂ H
c : C
⊢ adj₂.unit.app (G.obj c) ≫
      (R₂.map (α.app c) ≫ R₂.map ((L₁ ⋙ H).map (adj₁.unit.app c))) ≫ R₂.map (H.map (adj₁.counit.app (L₁.obj c))) =
    adj₂.unit.app (G.obj c) ≫ R₂.map (α.app c)

Tactic:
slice_lhs 3 4 =>
  rw [← R₂.map_comp, Functor.comp_map L₁ H, ← H.map_comp, left_triangle_components]

Result:
C : Type u₁
D : Type u₂
E : Type u₃
F : Type u₄
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₂, u₂} D
inst✝¹ : Category.{v₃, u₃} E
inst✝ : Category.{v₄, u₄} F
G : C ⥤ E
H : D ⥤ F
L₁ : C ⥤ D
R₁ : D ⥤ C
L₂ : E ⥤ F
R₂ : F ⥤ E
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
α : TwoSquare G L₁ L₂ H
c : C
⊢ adj₂.unit.app (G.obj c) ≫ R₂.map (α.app c) ≫ R₂.map (H.map (𝟙 (L₁.obj c))) =
    adj₂.unit.app (G.obj c) ≫ R₂.map (α.app c)

Proof state:
C : Type u₁
D : Type u₂
E : Type u₃
F : Type u₄
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₂, u₂} D
inst✝¹ : Category.{v₃, u₃} E
inst✝ : Category.{v₄, u₄} F
G : C ⥤ E
H : D ⥤ F
L₁ : C ⥤ D
R₁ : D ⥤ C
L₂ : E ⥤ F
R₂ : F ⥤ E
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
α : TwoSquare G L₁ L₂ H
c : C
⊢ adj₂.unit.app (G.obj c) ≫
      R₂.map (L₂.map (G.map (adj₁.unit.app c))) ≫
        R₂.map (α.natTrans.app (R₁.obj (L₁.obj c))) ≫ R₂.map (H.map (adj₁.counit.app (L₁.obj c))) =
    adj₂.unit.app (G.obj c) ≫ R₂.map (α.app c)

Tactic:
slice_lhs 2 3 =>
  rw [← R₂.map_comp, ← Functor.comp_map G L₂, α.naturality]

Result:
C : Type u₁
D : Type u₂
E : Type u₃
F : Type u₄
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₂, u₂} D
inst✝¹ : Category.{v₃, u₃} E
inst✝ : Category.{v₄, u₄} F
G : C ⥤ E
H : D ⥤ F
L₁ : C ⥤ D
R₁ : D ⥤ C
L₂ : E ⥤ F
R₂ : F ⥤ E
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
α : TwoSquare G L₁ L₂ H
c : C
⊢ adj₂.unit.app (G.obj c) ≫
      R₂.map (α.app c ≫ (L₁ ⋙ H).map (adj₁.unit.app c)) ≫ R₂.map (H.map (adj₁.counit.app (L₁.obj c))) =
    adj₂.unit.app (G.obj c) ≫ R₂.map (α.app c)

Proof state:
C : Type u₁
D : Type u₂
E : Type u₃
F : Type u₄
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₂, u₂} D
inst✝¹ : Category.{v₃, u₃} E
inst✝ : Category.{v₄, u₄} F
G : C ⥤ E
H : D ⥤ F
L₁ : C ⥤ D
R₁ : D ⥤ C
L₂ : E ⥤ F
R₂ : F ⥤ E
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
α : TwoSquare G L₁ L₂ H
c : C
⊢ G.map (adj₁.unit.app c) ≫
      adj₂.unit.app (G.obj (R₁.obj (L₁.obj c))) ≫
        R₂.map (α.natTrans.app (R₁.obj (L₁.obj c))) ≫ R₂.map (H.map (adj₁.counit.app (L₁.obj c))) =
    adj₂.unit.app (G.obj c) ≫ R₂.map (α.app c)

Tactic:
rw [← adj₂.unit_naturality_assoc]

Result:
C : Type u₁
D : Type u₂
E : Type u₃
F : Type u₄
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₂, u₂} D
inst✝¹ : Category.{v₃, u₃} E
inst✝ : Category.{v₄, u₄} F
G : C ⥤ E
H : D ⥤ F
L₁ : C ⥤ D
R₁ : D ⥤ C
L₂ : E ⥤ F
R₂ : F ⥤ E
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
α : TwoSquare G L₁ L₂ H
c : C
⊢ adj₂.unit.app (G.obj c) ≫
      R₂.map (L₂.map (G.map (adj₁.unit.app c))) ≫
        R₂.map (α.natTrans.app (R₁.obj (L₁.obj c))) ≫ R₂.map (H.map (adj₁.counit.app (L₁.obj c))) =
    adj₂.unit.app (G.obj c) ≫ R₂.map (α.app c)