C : Type u₁
D : Type u₂
inst✝² : Category C
inst✝¹ : Category D
L₁ L₂ L₃ : C ⥤ D
R₁ R₂ R₃ : D ⥤ C
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
adj₃ : L₃ ⊣ R₃
f : R₁ ⟶ R₂
inst✝ : IsIso (↑(transferNatTransSelf adj₁ adj₂).symm f)
⊢ IsIso (↑(transferNatTransSelf adj₁ adj₂) (↑(transferNatTransSelf adj₁ adj₂).symm f))
C : Type u₁
D : Type u₂
inst✝² : Category C
inst✝¹ : Category D
L₁ L₂ L₃ : C ⥤ D
R₁ R₂ R₃ : D ⥤ C
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
adj₃ : L₃ ⊣ R₃
f : R₁ ⟶ R₂
inst✝ : IsIso (↑(transferNatTransSelf adj₁ adj₂).symm f)
⊢ IsIso f
suffices IsIso ((transferNatTransSelf adj₁ adj₂) ((transferNatTransSelf adj₁ adj₂).symm f))
  by simpa using this
no goals
C : Type u₁
D : Type u₂
inst✝² : Category C
inst✝¹ : Category D
L₁ L₂ L₃ : C ⥤ D
R₁ R₂ R₃ : D ⥤ C
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
adj₃ : L₃ ⊣ R₃
f : R₁ ⟶ R₂
inst✝ : IsIso (↑(transferNatTransSelf adj₁ adj₂).symm f)
⊢ IsIso (↑(transferNatTransSelf adj₁ adj₂) (↑(transferNatTransSelf adj₁ adj₂).symm f))
infer_instance
no goals
C : Type u₁
D : Type u₂
inst✝² : Category C
inst✝¹ : Category D
L₁ L₂ L₃ : C ⥤ D
R₁ R₂ R₃ : D ⥤ C
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
adj₃ : L₃ ⊣ R₃
f : R₁ ⟶ R₂
inst✝ : IsIso (↑(transferNatTransSelf adj₁ adj₂).symm f)
this : IsIso (↑(transferNatTransSelf adj₁ adj₂) (↑(transferNatTransSelf adj₁ adj₂).symm f))
⊢ IsIso f
simpa using this