-- Mathlib/CategoryTheory/Adjunction/Triple.lean
lemma isIso_unit_iff_isIso_counit : IsIso adj₁.unit ↔ IsIso adj₂.counit

Proof state:
case mpr
C : Type u_1
D : Type u_2
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Category.{u_4, u_2} D
F H : C ⥤ D
G : D ⥤ C
adj₁ : F ⊣ G
adj₂ : G ⊣ H
adj : F ⋙ G ⊣ H ⋙ G := adj₁.comp adj₂
h : IsIso adj₂.counit
⊢ IsIso adj₁.unit

Tactic:
let adjId : F ⋙ G ⊣ 𝟭 C := adj.ofNatIsoRight (asIso adj₂.counit)

Result:
case mpr
C : Type u_1
D : Type u_2
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Category.{u_4, u_2} D
F H : C ⥤ D
G : D ⥤ C
adj₁ : F ⊣ G
adj₂ : G ⊣ H
adj : F ⋙ G ⊣ H ⋙ G := adj₁.comp adj₂
h : IsIso adj₂.counit
adjId : F ⋙ G ⊣ 𝟭 C := adj.ofNatIsoRight (asIso adj₂.counit)
⊢ IsIso adj₁.unit

Proof state:
case mp
C : Type u_1
D : Type u_2
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Category.{u_4, u_2} D
F H : C ⥤ D
G : D ⥤ C
adj₁ : F ⊣ G
adj₂ : G ⊣ H
adj : F ⋙ G ⊣ H ⋙ G := adj₁.comp adj₂
h : IsIso adj₁.unit
idAdj : 𝟭 C ⊣ H ⋙ G := adj.ofNatIsoLeft (asIso adj₁.unit).symm
⊢ IsIso adj₂.counit

Tactic:
exact adj₂.isIso_counit_of_iso (idAdj.rightAdjointUniq id)

Result:
no goals

Proof state:
case mp
C : Type u_1
D : Type u_2
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Category.{u_4, u_2} D
F H : C ⥤ D
G : D ⥤ C
adj₁ : F ⊣ G
adj₂ : G ⊣ H
adj : F ⋙ G ⊣ H ⋙ G := adj₁.comp adj₂
h : IsIso adj₁.unit
⊢ IsIso adj₂.counit

Tactic:
let idAdj : 𝟭 C ⊣ H ⋙ G := adj.ofNatIsoLeft (asIso adj₁.unit).symm

Result:
case mp
C : Type u_1
D : Type u_2
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Category.{u_4, u_2} D
F H : C ⥤ D
G : D ⥤ C
adj₁ : F ⊣ G
adj₂ : G ⊣ H
adj : F ⋙ G ⊣ H ⋙ G := adj₁.comp adj₂
h : IsIso adj₁.unit
idAdj : 𝟭 C ⊣ H ⋙ G := adj.ofNatIsoLeft (asIso adj₁.unit).symm
⊢ IsIso adj₂.counit

Proof state:
case mp
C : Type u_1
D : Type u_2
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Category.{u_4, u_2} D
F H : C ⥤ D
G : D ⥤ C
adj₁ : F ⊣ G
adj₂ : G ⊣ H
adj : F ⋙ G ⊣ H ⋙ G := adj₁.comp adj₂
⊢ IsIso adj₁.unit → IsIso adj₂.counit

Tactic:
intro h

Result:
case mp
C : Type u_1
D : Type u_2
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Category.{u_4, u_2} D
F H : C ⥤ D
G : D ⥤ C
adj₁ : F ⊣ G
adj₂ : G ⊣ H
adj : F ⋙ G ⊣ H ⋙ G := adj₁.comp adj₂
h : IsIso adj₁.unit
⊢ IsIso adj₂.counit

Proof state:
C : Type u_1
D : Type u_2
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Category.{u_4, u_2} D
F H : C ⥤ D
G : D ⥤ C
adj₁ : F ⊣ G
adj₂ : G ⊣ H
⊢ IsIso adj₁.unit ↔ IsIso adj₂.counit

Tactic:
let adj : F ⋙ G ⊣ H ⋙ G := adj₁.comp adj₂

Result:
C : Type u_1
D : Type u_2
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Category.{u_4, u_2} D
F H : C ⥤ D
G : D ⥤ C
adj₁ : F ⊣ G
adj₂ : G ⊣ H
adj : F ⋙ G ⊣ H ⋙ G := adj₁.comp adj₂
⊢ IsIso adj₁.unit ↔ IsIso adj₂.counit

Proof state:
C : Type u_1
D : Type u_2
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Category.{u_4, u_2} D
F H : C ⥤ D
G : D ⥤ C
adj₁ : F ⊣ G
adj₂ : G ⊣ H
adj : F ⋙ G ⊣ H ⋙ G := adj₁.comp adj₂
⊢ IsIso adj₁.unit ↔ IsIso adj₂.counit

Tactic:
constructor

Result:
case mp
C : Type u_1
D : Type u_2
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Category.{u_4, u_2} D
F H : C ⥤ D
G : D ⥤ C
adj₁ : F ⊣ G
adj₂ : G ⊣ H
adj : F ⋙ G ⊣ H ⋙ G := adj₁.comp adj₂
⊢ IsIso adj₁.unit → IsIso adj₂.counit

case mpr
C : Type u_1
D : Type u_2
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Category.{u_4, u_2} D
F H : C ⥤ D
G : D ⥤ C
adj₁ : F ⊣ G
adj₂ : G ⊣ H
adj : F ⋙ G ⊣ H ⋙ G := adj₁.comp adj₂
⊢ IsIso adj₂.counit → IsIso adj₁.unit

Proof state:
case mpr
C : Type u_1
D : Type u_2
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Category.{u_4, u_2} D
F H : C ⥤ D
G : D ⥤ C
adj₁ : F ⊣ G
adj₂ : G ⊣ H
adj : F ⋙ G ⊣ H ⋙ G := adj₁.comp adj₂
h : IsIso adj₂.counit
adjId : F ⋙ G ⊣ 𝟭 C := adj.ofNatIsoRight (asIso adj₂.counit)
⊢ IsIso adj₁.unit

Tactic:
exact adj₁.isIso_unit_of_iso (adjId.leftAdjointUniq id)

Result:
no goals

Proof state:
case mpr
C : Type u_1
D : Type u_2
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Category.{u_4, u_2} D
F H : C ⥤ D
G : D ⥤ C
adj₁ : F ⊣ G
adj₂ : G ⊣ H
adj : F ⋙ G ⊣ H ⋙ G := adj₁.comp adj₂
⊢ IsIso adj₂.counit → IsIso adj₁.unit

Tactic:
intro h

Result:
case mpr
C : Type u_1
D : Type u_2
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Category.{u_4, u_2} D
F H : C ⥤ D
G : D ⥤ C
adj₁ : F ⊣ G
adj₂ : G ⊣ H
adj : F ⋙ G ⊣ H ⋙ G := adj₁.comp adj₂
h : IsIso adj₂.counit
⊢ IsIso adj₁.unit