feat(category_theory/nat_iso): dsimp lemma for natural isomorphisms (#…

…5973) a little simp lemma
leanprover-community · Feb 1, 2021 · 89c7963 · 89c7963
1 parent 8273588
commit 89c7963
Showing 1 changed file with 2 additions and 0 deletions.
diff --git a/src/category_theory/natural_isomorphism.lean b/src/category_theory/natural_isomorphism.lean
@@ -156,6 +156,8 @@ instance is_iso_app_of_is_iso (α : F ⟶ G) [is_iso α] (X) : is_iso (α.app X)
   hom_inv_id' := congr_fun (congr_arg nat_trans.app (is_iso.hom_inv_id α)) X,
   inv_hom_id' := congr_fun (congr_arg nat_trans.app (is_iso.inv_hom_id α)) X }
 
+@[simp] lemma is_iso_inv_app (α : F ⟶ G) [is_iso α] (X) : (inv α).app X = inv (α.app X) := rfl
+
 /--
 Construct a natural isomorphism between functors by giving object level isomorphisms,
 and checking naturality only in the forward direction.