chore: make _root_.toContinuousMap reducible (leanprover-community#40477)

ocfnash · ocfnash · commit d18bb636bbd4 · 2026-06-16T13:17:59.000Z
If a structure extends `ContinuousMap` and also carries an instance of `ContinuousMapClass` then it will have two `toContinuousMap` functions available to it. Without this change, at non-reducible transparency Lean is unable to see that these two are defeq (assuming we have written a sane API and they are!). The motivating example is the `Path` structure where the lack of this reducibility was responsible for some `backward.isDefEq.respectTransparency false` in leanprover-community#33108.
diff --git a/Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Basic.lean b/Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Basic.lean
@@ -212,7 +212,7 @@ instance IsStarNormal.instNonUnitalIsometricContinuousFunctionalCalculus :
     rw [← norm_inr (𝕜 := ℂ), ← inrNonUnitalStarAlgHom_apply, ← NonUnitalStarAlgHom.comp_apply,
       inr_comp_cfcₙHom_eq_cfcₙAux a, cfcₙAux]
     simp only [NonUnitalStarAlgHom.comp_assoc, NonUnitalStarAlgHom.comp_apply,
-      toContinuousMapHom_apply, NonUnitalStarAlgHom.coe_coe]
+      NonUnitalStarAlgHom.coe_coe]
     rw [norm_cfcHom (a : Unitization ℂ A), StarAlgEquiv.norm_map]
     rfl
 
diff --git a/Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Isometric.lean b/Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Isometric.lean
@@ -387,7 +387,7 @@ protected theorem isometric_cfc (f : C(S, R)) (halg : Isometry (algebraMap R S))
     · simpa [halg.dist_eq] using! ContinuousMap.dist_apply_le_dist _
     · let x' : σₙ S a := Subtype.map (algebraMap R S) (fun _ ↦ quasispectrum.algebraMap_mem S) x
       apply le_of_eq_of_le ?_ <| ContinuousMap.dist_apply_le_dist x'
-      simp only [ContinuousMap.coe_coe, ContinuousMapZero.comp_apply, ContinuousMapZero.coe_mk,
+      simp only [ContinuousMapZero.comp_apply, ContinuousMapZero.coe_mk,
         ContinuousMap.coe_mk, StarAlgHom.ofId_apply, halg.dist_eq, x']
       congr! 2
       all_goals ext; exact haf.left_inv _ |>.symm
diff --git a/Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/NonUnital.lean b/Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/NonUnital.lean
@@ -873,7 +873,7 @@ lemma cfcₙ_eq_cfc [ContinuousFunctionalCalculus R A p] [ContinuousMapZero.Uniq
   by_cases ha : p a
   · have hf' := hf.mono <| spectrum_subset_quasispectrum R a
     rw [cfc_apply f a ha hf', cfcₙ_apply f a hf, cfcₙHom_eq_cfcₙHom_of_cfcHom, cfcₙHom_of_cfcHom]
-    dsimp only [NonUnitalStarAlgHom.comp_apply, toContinuousMapHom_apply,
+    dsimp only [NonUnitalStarAlgHom.comp_apply,
       NonUnitalStarAlgHom.coe_coe, compStarAlgHom'_apply]
     congr
   · simp [cfc_apply_of_not_predicate a ha, cfcₙ_apply_of_not_predicate (R := R) a ha]
diff --git a/Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Unique.lean b/Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Unique.lean
@@ -262,14 +262,14 @@ lemma toNNReal_mul_add_neg_mul_add_mul_neg_eq (f g : C(X, ℝ)₀) :
     ((f * g).toNNReal + (-f).toNNReal * g.toNNReal + f.toNNReal * (-g).toNNReal) =
     ((-(f * g)).toNNReal + f.toNNReal * g.toNNReal + (-f).toNNReal * (-g).toNNReal) := by
   apply toContinuousMap_injective
-  simpa only [← toContinuousMapHom_apply, map_add, map_mul, map_neg, toContinuousMapHom_toNNReal]
+  simpa only [map_add, map_mul, map_neg, toContinuousMapHom_toNNReal]
     using! (f : C(X, ℝ)).toNNReal_mul_add_neg_mul_add_mul_neg_eq g
 
 lemma toNNReal_add_add_neg_add_neg_eq (f g : C(X, ℝ)₀) :
     ((f + g).toNNReal + (-f).toNNReal + (-g).toNNReal) =
       ((-(f + g)).toNNReal + f.toNNReal + g.toNNReal) := by
   apply toContinuousMap_injective
-  simpa only [← toContinuousMapHom_apply, map_add, map_mul, map_neg, toContinuousMapHom_toNNReal]
+  simpa only [map_add, map_mul, map_neg, toContinuousMapHom_toNNReal]
     using! (f : C(X, ℝ)).toNNReal_add_add_neg_add_neg_eq g
 
 end ContinuousMapZero
diff --git a/Mathlib/Analysis/RCLike/BoundedContinuous.lean b/Mathlib/Analysis/RCLike/BoundedContinuous.lean
@@ -32,7 +32,7 @@ theorem restrict_toContinuousMap_eq_toContinuousMapStar_restrict
     (ofRealAm.compLeftContinuous ℝ continuous_ofReal) := by
   ext g
   simp only [Subalgebra.mem_map, Subalgebra.mem_comap, Subalgebra.mem_restrictScalars,
-    StarSubalgebra.mem_toSubalgebra, toContinuousMapₐ_apply, StarSubalgebra.mem_map]
+    StarSubalgebra.mem_toSubalgebra, StarSubalgebra.mem_map]
   constructor
   · intro ⟨x, hxA, hxg⟩
     use (@ofRealAm 𝕜 _).compLeftContinuousBounded ℝ lipschitzWith_ofReal x, hxA
diff --git a/Mathlib/Topology/ContinuousMap/ContinuousMapZero.lean b/Mathlib/Topology/ContinuousMap/ContinuousMapZero.lean
@@ -329,7 +329,7 @@ def toContinuousMapHom [StarRing R] [ContinuousStar R] : C(X, R)₀ →⋆ₙₐ
   map_mul' _ _ := rfl
   map_star' _ := rfl
 
-lemma coe_toContinuousMapHom [StarRing R] [ContinuousStar R] :
+@[simp] lemma coe_toContinuousMapHom [StarRing R] [ContinuousStar R] :
     ⇑(toContinuousMapHom (X := X) (R := R)) = (↑) :=
   rfl
 
diff --git a/Mathlib/Topology/ContinuousMap/Defs.lean b/Mathlib/Topology/ContinuousMap/Defs.lean
@@ -61,7 +61,7 @@ variable {F X Y : Type*} [TopologicalSpace X] [TopologicalSpace Y] [FunLike F X
 variable [ContinuousMapClass F X Y]
 
 /-- Coerce a bundled morphism with a `ContinuousMapClass` instance to a `ContinuousMap`. -/
-@[coe] def toContinuousMap (f : F) : C(X, Y) := ⟨f, map_continuous f⟩
+@[coe, reducible] def toContinuousMap (f : F) : C(X, Y) := ⟨f, map_continuous f⟩
 
 instance : CoeTC F C(X, Y) := ⟨toContinuousMap⟩
 
diff --git a/Mathlib/Topology/ContinuousMap/Ideals.lean b/Mathlib/Topology/ContinuousMap/Ideals.lean
@@ -268,7 +268,7 @@ theorem idealOfSet_ofIdeal_eq_closure (I : Ideal C(X, 𝕜)) :
             pow_pos (norm_pos_iff.mpr hx.1) 2⟩⟩
       convert! I.mul_mem_left (star g) hI
       ext
-      simp only [comp_apply, ContinuousMap.coe_coe, coe_mk, algebraMapCLM_apply, map_pow,
+      simp only [comp_apply, coe_mk, algebraMapCLM_apply, map_pow,
         mul_apply, star_apply, star_def]
       simp only [RCLike.conj_mul]
       rfl
diff --git a/Mathlib/Topology/ContinuousMap/StoneWeierstrass.lean b/Mathlib/Topology/ContinuousMap/StoneWeierstrass.lean
@@ -632,10 +632,10 @@ lemma ContinuousMapZero.adjoin_id_dense (s : Set 𝕜) [Fact (0 ∈ s)]
     ← isClosedEmbedding_toContinuousMap.injective.preimage_image (closure _),
     ← isClosedEmbedding_toContinuousMap.closure_image_eq, ← coe_toContinuousMapHom,
     ← NonUnitalStarSubalgebra.coe_map, NonUnitalStarAlgHom.map_adjoin_singleton,
-    toContinuousMapHom_apply, toContinuousMap_id,
+    coe_toContinuousMapHom, toContinuousMap_id,
     ← ContinuousMap.ker_evalStarAlgHom_eq_closure_adjoin_id s h0']
   apply Set.eq_univ_of_forall fun f ↦ ?_
-  simp only [Set.mem_preimage, toContinuousMapHom_apply, SetLike.mem_coe, RingHom.mem_ker,
+  simp only [Set.mem_preimage, SetLike.mem_coe, RingHom.mem_ker,
     ContinuousMap.evalStarAlgHom_apply, ContinuousMap.coe_coe]
   exact map_zero f
 
diff --git a/Mathlib/Topology/Homotopy/HomotopyGroup.lean b/Mathlib/Topology/Homotopy/HomotopyGroup.lean
@@ -285,7 +285,7 @@ def fromLoop (i : N) (p : Ω (Ω^ { j // j ≠ i } X x) const) : Ω^ N X x :=
     (Cube.splitAt i),
     by
     rintro y ⟨j, Hj⟩
-    simp only [ContinuousMap.comp_apply, ContinuousMap.coe_coe,
+    simp only [ContinuousMap.comp_apply,
       funSplitAt_apply, ContinuousMap.uncurry_apply, ContinuousMap.coe_mk,
       Function.uncurry_apply_pair]
     obtain rfl | Hne := eq_or_ne j i
diff --git a/Mathlib/Topology/Homotopy/TopCat/ZerothHomotopy.lean b/Mathlib/Topology/Homotopy/TopCat/ZerothHomotopy.lean
@@ -43,14 +43,14 @@ set_option backward.isDefEq.respectTransparency false in
 @[simp]
 lemma toSSetObj₁Equiv_apply_zero (s : toSSet.obj X _⦋1⦌) :
     X.toSSetObj₁Equiv s 0 = toSSetObj₀Equiv ((toSSet.obj X).δ 1 s) := by
-  simp [toSSetObj₀Equiv, toSSetObj₁Equiv,
+  simp [toSSetObj₀Equiv, toSSetObj₁Equiv, -ContinuousMap.coe_mk,
     Subsingleton.elim (default : stdSimplex ℝ (Fin 1)) (stdSimplex.vertex 0)]
 
 set_option backward.isDefEq.respectTransparency false in
 @[simp]
 lemma toSSetObj₁Equiv_apply_one (s : toSSet.obj X _⦋1⦌) :
     X.toSSetObj₁Equiv s 1 = toSSetObj₀Equiv ((toSSet.obj X).δ 0 s) := by
-  simp [toSSetObj₀Equiv, toSSetObj₁Equiv,
+  simp [toSSetObj₀Equiv, toSSetObj₁Equiv, -ContinuousMap.coe_mk,
     Subsingleton.elim (default : stdSimplex ℝ (Fin 1)) (stdSimplex.vertex 0)]
 
 @[simp]
