refactor(category_theory/shift): remove opaque_eq_to_iso (#14262)

It seems `opaque_eq_to_iso` was only needed because we had over-eager simp lemmas. After #14260, it is easy to remove.



Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

Author: kim-em

src/category_theory/differential_object.lean

@@ -234,10 +234,12 @@ local attribute [reducible] discrete.add_monoidal shift_comm
 begin
   refine nat_iso.of_components (λ X, mk_iso (shift_add X.X _ _) _) _,
   { dsimp,
+    -- This is just `simp, simp [eq_to_hom_map]`.
     simp_rw [category.assoc, obj_μ_inv_app, μ_inv_hom_app_assoc, functor.map_comp, obj_μ_app,
       category.assoc, μ_naturality_assoc, μ_inv_hom_app_assoc, obj_μ_inv_app, category.assoc,
       μ_naturalityₗ_assoc, μ_inv_hom_app_assoc, μ_inv_naturalityᵣ_assoc],
-    simp [opaque_eq_to_iso] },
+    simp only [eq_to_hom_map, eq_to_hom_app, eq_to_iso.hom, eq_to_hom_trans_assoc,
+      eq_to_iso.inv], },
   { intros X Y f, ext, dsimp, exact nat_trans.naturality _ _ }
 end
 
@@ -257,6 +259,8 @@ end
 
 end
 
+local attribute [simp] eq_to_hom_map
+
 instance : has_shift (differential_object C) ℤ :=
 has_shift_mk _ _
 { F := shift_functor C,

src/category_theory/shift.lean

@@ -193,31 +193,6 @@ by { symmetry, apply nat_iso.naturality_2 }
 
 end add_monoid
 
-section opaque_eq_to_iso
-
-variables {ι : Type*} {i j k : ι}
-
-/-- This definition is used instead of `eq_to_iso` so that the proof of `i = j` is visible
-to the simplifier -/
-def opaque_eq_to_iso (h : i = j) : @iso (discrete ι) _ ⟨i⟩ ⟨j⟩ := discrete.eq_to_iso h
-
-@[simp]
-lemma opaque_eq_to_iso_symm (h : i = j) :
-  (opaque_eq_to_iso h).symm = opaque_eq_to_iso h.symm := rfl
-
-@[simp]
-lemma opaque_eq_to_iso_inv (h : i = j) :
-  (opaque_eq_to_iso h).inv = (opaque_eq_to_iso h.symm).hom := rfl
-
-local attribute [simp] eq_to_hom_map
-
-@[simp, reassoc]
-lemma map_opaque_eq_to_iso_comp_app (F : discrete ι ⥤ C ⥤ C) (h : i = j) (h' : j = k) (X : C) :
-  (F.map (opaque_eq_to_iso h).hom).app X ≫ (F.map (opaque_eq_to_iso h').hom).app X =
-    (F.map (opaque_eq_to_iso $ h.trans h').hom).app X := by { delta opaque_eq_to_iso, simp }
-
-end opaque_eq_to_iso
-
 section add_group
 
 variables (C) {A} [add_group A] [has_shift C A]
@@ -228,13 +203,13 @@ variables (X Y : C) (f : X ⟶ Y)
 abbreviation shift_functor_comp_shift_functor_neg (i : A) :
   shift_functor C i ⋙ shift_functor C (-i) ≅ 𝟭 C :=
 unit_of_tensor_iso_unit (shift_monoidal_functor C A) ⟨i⟩ ⟨(-i : A)⟩
-  (opaque_eq_to_iso (add_neg_self i))
+  (discrete.eq_to_iso (add_neg_self i))
 
 /-- Shifting by `-i` and then shifting by `i` is the identity. -/
 abbreviation shift_functor_neg_comp_shift_functor (i : A) :
   shift_functor C (-i) ⋙ shift_functor C i ≅ 𝟭 C :=
 unit_of_tensor_iso_unit (shift_monoidal_functor C A) ⟨(-i : A)⟩ ⟨i⟩
-  (opaque_eq_to_iso (neg_add_self i))
+  (discrete.eq_to_iso (neg_add_self i))
 
 section
 
@@ -287,12 +262,17 @@ lemma shift_equiv_triangle (n : A) (X : C) :
 (add_neg_equiv (shift_monoidal_functor C A) n).functor_unit_iso_comp X
 
 section
-local attribute [simp] eq_to_hom_map
 local attribute [reducible] discrete.add_monoidal
 
 lemma shift_shift_neg_hom_shift (n : A) (X : C) :
   (shift_shift_neg X n).hom ⟦n⟧' = (shift_neg_shift (X⟦n⟧) n).hom :=
-by simp
+begin
+  -- This is just `simp, simp [eq_to_hom_map]`.
+  simp only [iso.app_hom, unit_of_tensor_iso_unit_hom_app, eq_to_iso.hom, functor.map_comp,
+    obj_μ_app, eq_to_iso.inv, obj_ε_inv_app, μ_naturalityₗ_assoc, category.assoc,
+    μ_inv_hom_app_assoc, ε_inv_app_obj, μ_naturalityᵣ_assoc],
+  simp only [eq_to_hom_map, eq_to_hom_app, eq_to_hom_trans],
+end
 
 end
 
@@ -333,19 +313,27 @@ variables (X Y : C) (f : X ⟶ Y)
 /-- When shifts are indexed by an additive commutative monoid, then shifts commute. -/
 def shift_comm (i j : A) : X⟦i⟧⟦j⟧ ≅ X⟦j⟧⟦i⟧ :=
 (shift_add X i j).symm ≪≫ ((shift_monoidal_functor C A).to_functor.map_iso
-  (opaque_eq_to_iso $ add_comm i j : _)).app X ≪≫ shift_add X j i
+  (discrete.eq_to_iso $ add_comm i j : (⟨i+j⟩ : discrete A) ≅ ⟨j+i⟩)).app X ≪≫ shift_add X j i
 
 @[simp] lemma shift_comm_symm (i j : A) : (shift_comm X i j).symm = shift_comm X j i :=
 begin
-  ext, dsimp [shift_comm], simpa
+  ext, dsimp [shift_comm], simpa [eq_to_hom_map],
 end
 
 variables {X Y}
 
 /-- When shifts are indexed by an additive commutative monoid, then shifts commute. -/
 lemma shift_comm' (i j : A) :
   f⟦i⟧'⟦j⟧' = (shift_comm _ _ _).hom ≫ f⟦j⟧'⟦i⟧' ≫ (shift_comm _ _ _).hom :=
-by simp [shift_comm]
+begin
+  -- This is just `simp, simp [eq_to_hom_map]`.
+  simp only [shift_comm, iso.trans_hom, iso.symm_hom, iso.app_inv, iso.symm_inv,
+    monoidal_functor.μ_iso_hom, iso.app_hom, functor.map_iso_hom, eq_to_iso.hom, μ_naturality_assoc,
+    nat_trans.naturality_assoc, nat_trans.naturality, functor.comp_map, category.assoc,
+    μ_inv_hom_app_assoc],
+  simp only [eq_to_hom_map, eq_to_hom_app, eq_to_hom_trans_assoc, eq_to_hom_refl, category.id_comp,
+    μ_hom_inv_app_assoc],
+end
 
 @[reassoc] lemma shift_comm_hom_comp (i j : A) :
   (shift_comm X i j).hom ≫ f⟦j⟧'⟦i⟧' = f⟦i⟧'⟦j⟧' ≫ (shift_comm Y i j).hom :=

src/category_theory/triangulated/rotate.lean

@@ -151,7 +151,7 @@ def inv_rotate (f : triangle_morphism T₁ T₂) :
   end,
   comm₃' := begin
     dsimp,
-    simp only [discrete.functor_map_id, id_comp, opaque_eq_to_iso_inv, μ_inv_naturality,
+    simp only [discrete.functor_map_id, id_comp, μ_inv_naturality,
       category.assoc, nat_trans.id_app, unit_of_tensor_iso_unit_inv_app],
     erw ε_naturality_assoc,
     rw comm₂_assoc
@@ -190,8 +190,8 @@ def to_inv_rotate_rotate (T : triangle C) : T ⟶ (inv_rotate C).obj ((rotate C)
     comm₃' := begin
       dsimp,
       simp only [ε_app_obj, eq_to_iso.hom, discrete.functor_map_id, id_comp, eq_to_iso.inv,
-        opaque_eq_to_iso_inv, category.assoc, obj_μ_inv_app, functor.map_comp, nat_trans.id_app,
-        obj_ε_app, unit_of_tensor_iso_unit_inv_app],
+        category.assoc, obj_μ_inv_app, functor.map_comp, nat_trans.id_app, obj_ε_app,
+        unit_of_tensor_iso_unit_inv_app],
       erw μ_inv_hom_app_assoc,
       refl
     end }
@@ -207,8 +207,7 @@ def rot_comp_inv_rot_hom : 𝟭 (triangle C) ⟶ rotate C ⋙ inv_rotate C :=
     introv, ext,
     { dsimp,
       simp only [nat_iso.cancel_nat_iso_inv_right_assoc, discrete.functor_map_id, id_comp,
-        opaque_eq_to_iso_inv, μ_inv_naturality, assoc, nat_trans.id_app,
-        unit_of_tensor_iso_unit_inv_app],
+        μ_inv_naturality, assoc, nat_trans.id_app, unit_of_tensor_iso_unit_inv_app],
       erw ε_naturality },
     { dsimp, rw [comp_id, id_comp] },
     { dsimp, rw [comp_id, id_comp] },