diff --git a/Mathlib/Algebra/Category/ModuleCat/Free.lean b/Mathlib/Algebra/Category/ModuleCat/Free.lean index ce028e860756f..0cf3303dd9713 100644 --- a/Mathlib/Algebra/Category/ModuleCat/Free.lean +++ b/Mathlib/Algebra/Category/ModuleCat/Free.lean @@ -144,7 +144,7 @@ theorem span_rightExact {w : ι' → S.X₃} (hv : ⊤ ≤ span R (range v)) · convert hw simp only [AddHom.toFun_eq_coe, LinearMap.coe_toAddHom, Sum.elim_comp_inr] rw [ModuleCat.epi_iff_surjective] at hE - rw [← Function.comp.assoc, Function.RightInverse.comp_eq_id (Function.rightInverse_invFun hE), + rw [← Function.comp_assoc, Function.RightInverse.comp_eq_id (Function.rightInverse_invFun hE), Function.id_comp] end Span diff --git a/Mathlib/Algebra/Module/PID.lean b/Mathlib/Algebra/Module/PID.lean index 65924b9cdde6d..a00bd3ef0ee93 100644 --- a/Mathlib/Algebra/Module/PID.lean +++ b/Mathlib/Algebra/Module/PID.lean @@ -225,7 +225,7 @@ theorem torsion_by_prime_power_decomposition (hN : Module.IsTorsion' N (Submonoi ⟨(@hN x).choose, by rw [← Quotient.mk_smul, (@hN x).choose_spec, Quotient.mk_zero]⟩ · have hs' := congr_arg (Submodule.map <| mkQ <| R ∙ s j) hs rw [Submodule.map_span, Submodule.map_top, range_mkQ] at hs'; simp only [mkQ_apply] at hs' - simp only [s']; rw [← Function.comp.assoc, Set.range_comp (_ ∘ s), Fin.range_succAbove] + simp only [s']; rw [← Function.comp_assoc, Set.range_comp (_ ∘ s), Fin.range_succAbove] rw [← Set.range_comp, ← Set.insert_image_compl_eq_range _ j, Function.comp_apply, (Quotient.mk_eq_zero _).mpr (Submodule.mem_span_singleton_self _), span_insert_zero] at hs' exact hs' diff --git a/Mathlib/Algebra/Order/Rearrangement.lean b/Mathlib/Algebra/Order/Rearrangement.lean index 6643fbdac7eec..f032d3104e240 100644 --- a/Mathlib/Algebra/Order/Rearrangement.lean +++ b/Mathlib/Algebra/Order/Rearrangement.lean @@ -164,10 +164,10 @@ theorem MonovaryOn.sum_comp_perm_smul_eq_sum_smul_iff (hfg : MonovaryOn f g s) rw [σ.sum_comp' s (fun i j ↦ f i • g j) hσ] congr · convert h.comp_right σ - · rw [comp.assoc, inv_def, symm_comp_self, comp_id] + · rw [comp_assoc, inv_def, symm_comp_self, comp_id] · rw [σ.eq_preimage_iff_image_eq, Set.image_perm hσ] · convert h.comp_right σ.symm - · rw [comp.assoc, self_comp_symm, comp_id] + · rw [comp_assoc, self_comp_symm, comp_id] · rw [σ.symm.eq_preimage_iff_image_eq] exact Set.image_perm hσinv diff --git a/Mathlib/AlgebraicGeometry/AffineScheme.lean b/Mathlib/AlgebraicGeometry/AffineScheme.lean index 8945030d7edd1..56989b5600798 100644 --- a/Mathlib/AlgebraicGeometry/AffineScheme.lean +++ b/Mathlib/AlgebraicGeometry/AffineScheme.lean @@ -265,7 +265,7 @@ instance isOpenImmersion_fromSpec : theorem range_fromSpec : Set.range hU.fromSpec.1.base = (U : Set X) := by delta IsAffineOpen.fromSpec; dsimp - rw [Function.comp.assoc, Set.range_comp, Set.range_iff_surjective.mpr, Set.image_univ] + rw [Function.comp_assoc, Set.range_comp, Set.range_iff_surjective.mpr, Set.image_univ] · exact Subtype.range_coe erw [← coe_comp, ← TopCat.epi_iff_surjective] -- now `erw` after #13170 infer_instance diff --git a/Mathlib/Analysis/Calculus/ContDiff/Bounds.lean b/Mathlib/Analysis/Calculus/ContDiff/Bounds.lean index d5cce4ded4d53..75f2e43860603 100644 --- a/Mathlib/Analysis/Calculus/ContDiff/Bounds.lean +++ b/Mathlib/Analysis/Calculus/ContDiff/Bounds.lean @@ -304,7 +304,7 @@ theorem norm_iteratedFDerivWithin_prod_le [DecidableEq ι] [NormOneClass A'] {u (g := (fun v ↦ v.multinomial * ∏ j ∈ insert i u, ‖iteratedFDerivWithin 𝕜 (v.count j) (f j) s x‖) ∘ Sym.toMultiset ∘ Subtype.val ∘ (Finset.symInsertEquiv hi).symm) - (by simp) (by simp only [← comp_apply (g := Finset.symInsertEquiv hi), comp.assoc]; simp)] + (by simp) (by simp only [← comp_apply (g := Finset.symInsertEquiv hi), comp_assoc]; simp)] rw [← Finset.univ_sigma_univ, Finset.sum_sigma, Finset.sum_range] simp only [comp_apply, Finset.symInsertEquiv_symm_apply_coe] refine Finset.sum_le_sum ?_ diff --git a/Mathlib/Analysis/Calculus/FDeriv/Equiv.lean b/Mathlib/Analysis/Calculus/FDeriv/Equiv.lean index e2f34a6adc71a..1c6738f520fcc 100644 --- a/Mathlib/Analysis/Calculus/FDeriv/Equiv.lean +++ b/Mathlib/Analysis/Calculus/FDeriv/Equiv.lean @@ -87,7 +87,7 @@ theorem comp_differentiableWithinAt_iff {f : G → E} {s : Set G} {x : G} : ⟨fun H => ?_, fun H => iso.differentiable.differentiableAt.comp_differentiableWithinAt x H⟩ have : DifferentiableWithinAt 𝕜 (iso.symm ∘ iso ∘ f) s x := iso.symm.differentiable.differentiableAt.comp_differentiableWithinAt x H - rwa [← Function.comp.assoc iso.symm iso f, iso.symm_comp_self] at this + rwa [← Function.comp_assoc iso.symm iso f, iso.symm_comp_self] at this theorem comp_differentiableAt_iff {f : G → E} {x : G} : DifferentiableAt 𝕜 (iso ∘ f) x ↔ DifferentiableAt 𝕜 f x := by @@ -107,7 +107,7 @@ theorem comp_hasFDerivWithinAt_iff {f : G → E} {s : Set G} {x : G} {f' : G → HasFDerivWithinAt (iso ∘ f) ((iso : E →L[𝕜] F).comp f') s x ↔ HasFDerivWithinAt f f' s x := by refine ⟨fun H => ?_, fun H => iso.hasFDerivAt.comp_hasFDerivWithinAt x H⟩ have A : f = iso.symm ∘ iso ∘ f := by - rw [← Function.comp.assoc, iso.symm_comp_self] + rw [← Function.comp_assoc, iso.symm_comp_self] rfl have B : f' = (iso.symm : F →L[𝕜] E).comp ((iso : E →L[𝕜] F).comp f') := by rw [← ContinuousLinearMap.comp_assoc, iso.coe_symm_comp_coe, ContinuousLinearMap.id_comp] @@ -174,7 +174,7 @@ theorem comp_right_differentiableWithinAt_iff {f : F → G} {s : Set F} {x : E} apply H.comp (iso x) iso.symm.differentiableWithinAt intro y hy simpa only [mem_preimage, apply_symm_apply] using hy - rwa [Function.comp.assoc, iso.self_comp_symm] at this + rwa [Function.comp_assoc, iso.self_comp_symm] at this theorem comp_right_differentiableAt_iff {f : F → G} {x : E} : DifferentiableAt 𝕜 (f ∘ iso) x ↔ DifferentiableAt 𝕜 f (iso x) := by @@ -198,7 +198,7 @@ theorem comp_right_hasFDerivWithinAt_iff {f : F → G} {s : Set F} {x : E} {f' : refine ⟨fun H => ?_, fun H => H.comp x iso.hasFDerivWithinAt (mapsTo_preimage _ s)⟩ rw [← iso.symm_apply_apply x] at H have A : f = (f ∘ iso) ∘ iso.symm := by - rw [Function.comp.assoc, iso.self_comp_symm] + rw [Function.comp_assoc, iso.self_comp_symm] rfl have B : f' = (f'.comp (iso : E →L[𝕜] F)).comp (iso.symm : F →L[𝕜] E) := by rw [ContinuousLinearMap.comp_assoc, iso.coe_comp_coe_symm, ContinuousLinearMap.comp_id] diff --git a/Mathlib/Analysis/Calculus/IteratedDeriv/Defs.lean b/Mathlib/Analysis/Calculus/IteratedDeriv/Defs.lean index b662ec13e36fc..f5790c73a631f 100644 --- a/Mathlib/Analysis/Calculus/IteratedDeriv/Defs.lean +++ b/Mathlib/Analysis/Calculus/IteratedDeriv/Defs.lean @@ -82,7 +82,7 @@ iterated derivative. -/ theorem iteratedFDerivWithin_eq_equiv_comp : iteratedFDerivWithin 𝕜 n f s = ContinuousMultilinearMap.piFieldEquiv 𝕜 (Fin n) F ∘ iteratedDerivWithin n f s := by - rw [iteratedDerivWithin_eq_equiv_comp, ← Function.comp.assoc, LinearIsometryEquiv.self_comp_symm, + rw [iteratedDerivWithin_eq_equiv_comp, ← Function.comp_assoc, LinearIsometryEquiv.self_comp_symm, Function.id_comp] /-- The `n`-th Fréchet derivative applied to a vector `(m 0, ..., m (n-1))` is the derivative @@ -203,7 +203,7 @@ theorem iteratedDeriv_eq_equiv_comp : iteratedDeriv n f = iterated derivative. -/ theorem iteratedFDeriv_eq_equiv_comp : iteratedFDeriv 𝕜 n f = ContinuousMultilinearMap.piFieldEquiv 𝕜 (Fin n) F ∘ iteratedDeriv n f := by - rw [iteratedDeriv_eq_equiv_comp, ← Function.comp.assoc, LinearIsometryEquiv.self_comp_symm, + rw [iteratedDeriv_eq_equiv_comp, ← Function.comp_assoc, LinearIsometryEquiv.self_comp_symm, Function.id_comp] /-- The `n`-th Fréchet derivative applied to a vector `(m 0, ..., m (n-1))` is the derivative diff --git a/Mathlib/Analysis/Convex/Intrinsic.lean b/Mathlib/Analysis/Convex/Intrinsic.lean index d05235e251337..b244bd60d24fb 100644 --- a/Mathlib/Analysis/Convex/Intrinsic.lean +++ b/Mathlib/Analysis/Convex/Intrinsic.lean @@ -250,8 +250,8 @@ theorem image_intrinsicInterior (φ : P →ᵃⁱ[𝕜] Q) (s : Set P) : let f := ((affineSpan 𝕜 s).isometryEquivMap φ).toHomeomorph have : φ.toAffineMap ∘ (↑) ∘ f.symm = (↑) := funext isometryEquivMap.apply_symm_apply rw [intrinsicInterior, intrinsicInterior, ← φ.coe_toAffineMap, ← map_span φ.toAffineMap s, ← this, - ← Function.comp.assoc, image_comp, image_comp, f.symm.image_interior, f.image_symm, - ← preimage_comp, Function.comp.assoc, f.symm_comp_self, AffineIsometry.coe_toAffineMap, + ← Function.comp_assoc, image_comp, image_comp, f.symm.image_interior, f.image_symm, + ← preimage_comp, Function.comp_assoc, f.symm_comp_self, AffineIsometry.coe_toAffineMap, Function.comp_id, preimage_comp, φ.injective.preimage_image] @[simp] @@ -263,8 +263,8 @@ theorem image_intrinsicFrontier (φ : P →ᵃⁱ[𝕜] Q) (s : Set P) : let f := ((affineSpan 𝕜 s).isometryEquivMap φ).toHomeomorph have : φ.toAffineMap ∘ (↑) ∘ f.symm = (↑) := funext isometryEquivMap.apply_symm_apply rw [intrinsicFrontier, intrinsicFrontier, ← φ.coe_toAffineMap, ← map_span φ.toAffineMap s, ← this, - ← Function.comp.assoc, image_comp, image_comp, f.symm.image_frontier, f.image_symm, - ← preimage_comp, Function.comp.assoc, f.symm_comp_self, AffineIsometry.coe_toAffineMap, + ← Function.comp_assoc, image_comp, image_comp, f.symm.image_frontier, f.image_symm, + ← preimage_comp, Function.comp_assoc, f.symm_comp_self, AffineIsometry.coe_toAffineMap, Function.comp_id, preimage_comp, φ.injective.preimage_image] @[simp] @@ -276,8 +276,8 @@ theorem image_intrinsicClosure (φ : P →ᵃⁱ[𝕜] Q) (s : Set P) : let f := ((affineSpan 𝕜 s).isometryEquivMap φ).toHomeomorph have : φ.toAffineMap ∘ (↑) ∘ f.symm = (↑) := funext isometryEquivMap.apply_symm_apply rw [intrinsicClosure, intrinsicClosure, ← φ.coe_toAffineMap, ← map_span φ.toAffineMap s, ← this, - ← Function.comp.assoc, image_comp, image_comp, f.symm.image_closure, f.image_symm, - ← preimage_comp, Function.comp.assoc, f.symm_comp_self, AffineIsometry.coe_toAffineMap, + ← Function.comp_assoc, image_comp, image_comp, f.symm.image_closure, f.image_symm, + ← preimage_comp, Function.comp_assoc, f.symm_comp_self, AffineIsometry.coe_toAffineMap, Function.comp_id, preimage_comp, φ.injective.preimage_image] end AffineIsometry diff --git a/Mathlib/Analysis/SpecialFunctions/Complex/Arg.lean b/Mathlib/Analysis/SpecialFunctions/Complex/Arg.lean index f34699a4c7f97..b7b5fa601494d 100644 --- a/Mathlib/Analysis/SpecialFunctions/Complex/Arg.lean +++ b/Mathlib/Analysis/SpecialFunctions/Complex/Arg.lean @@ -598,7 +598,7 @@ theorem continuousAt_arg_coe_angle (h : x ≠ 0) : ContinuousAt ((↑) ∘ arg : · exact Real.Angle.continuous_coe.continuousAt.comp (continuousAt_arg hs) · rw [← Function.comp_id (((↑) : ℝ → Real.Angle) ∘ arg), (Function.funext_iff.2 fun _ => (neg_neg _).symm : (id : ℂ → ℂ) = Neg.neg ∘ Neg.neg), ← - Function.comp.assoc] + Function.comp_assoc] refine ContinuousAt.comp ?_ continuous_neg.continuousAt suffices ContinuousAt (Function.update (((↑) ∘ arg) ∘ Neg.neg : ℂ → Real.Angle) 0 π) (-x) by rwa [continuousAt_update_of_ne (neg_ne_zero.2 h)] at this diff --git a/Mathlib/Combinatorics/HalesJewett.lean b/Mathlib/Combinatorics/HalesJewett.lean index b97bcd5a4cdf7..f02b849012141 100644 --- a/Mathlib/Combinatorics/HalesJewett.lean +++ b/Mathlib/Combinatorics/HalesJewett.lean @@ -150,7 +150,7 @@ def reindex (l : Subspace η α ι) (eη : η ≃ η') (eα : α ≃ α') (eι : protected lemma IsMono.reindex {eη : η ≃ η'} {eα : α ≃ α'} {eι : ι ≃ ι'} {C : (ι → α) → κ} (hl : l.IsMono C) : (l.reindex eη eα eι).IsMono fun x ↦ C <| eα.symm ∘ x ∘ eι := by - simp [reindex_isMono, Function.comp.assoc]; simpa [← Function.comp.assoc] + simp [reindex_isMono, Function.comp_assoc]; simpa [← Function.comp_assoc] end Subspace diff --git a/Mathlib/Data/Fin/Tuple/Sort.lean b/Mathlib/Data/Fin/Tuple/Sort.lean index d53751d03f1f5..6dfe8a11de7e8 100644 --- a/Mathlib/Data/Fin/Tuple/Sort.lean +++ b/Mathlib/Data/Fin/Tuple/Sort.lean @@ -178,7 +178,7 @@ theorem comp_sort_eq_comp_iff_monotone : f ∘ σ = f ∘ sort f ↔ Monotone (f /-- The sorted versions of a tuple `f` and of any permutation of `f` agree. -/ theorem comp_perm_comp_sort_eq_comp_sort : (f ∘ σ) ∘ sort (f ∘ σ) = f ∘ sort f := by - rw [Function.comp.assoc, ← Equiv.Perm.coe_mul] + rw [Function.comp_assoc, ← Equiv.Perm.coe_mul] exact unique_monotone (monotone_sort (f ∘ σ)) (monotone_sort f) /-- If a permutation `f ∘ σ` of the tuple `f` is not the same as `f ∘ sort f`, then `f ∘ σ` diff --git a/Mathlib/Dynamics/Ergodic/MeasurePreserving.lean b/Mathlib/Dynamics/Ergodic/MeasurePreserving.lean index f3cf7b84dd1bf..aeb910c97b9ae 100644 --- a/Mathlib/Dynamics/Ergodic/MeasurePreserving.lean +++ b/Mathlib/Dynamics/Ergodic/MeasurePreserving.lean @@ -102,13 +102,13 @@ protected theorem comp_left_iff {g : α → β} {e : β ≃ᵐ γ} (h : MeasureP MeasurePreserving (e ∘ g) μa μc ↔ MeasurePreserving g μa μb := by refine ⟨fun hg => ?_, fun hg => h.comp hg⟩ convert (MeasurePreserving.symm e h).comp hg - simp [← Function.comp.assoc e.symm e g] + simp [← Function.comp_assoc e.symm e g] protected theorem comp_right_iff {g : α → β} {e : γ ≃ᵐ α} (h : MeasurePreserving e μc μa) : MeasurePreserving (g ∘ e) μc μb ↔ MeasurePreserving g μa μb := by refine ⟨fun hg => ?_, fun hg => hg.comp h⟩ convert hg.comp (MeasurePreserving.symm e h) - simp [Function.comp.assoc g e e.symm] + simp [Function.comp_assoc g e e.symm] protected theorem sigmaFinite {f : α → β} (hf : MeasurePreserving f μa μb) [SigmaFinite μb] : SigmaFinite μa := diff --git a/Mathlib/Geometry/Manifold/LocalInvariantProperties.lean b/Mathlib/Geometry/Manifold/LocalInvariantProperties.lean index f1f298984aaa0..9feae63ffc666 100644 --- a/Mathlib/Geometry/Manifold/LocalInvariantProperties.lean +++ b/Mathlib/Geometry/Manifold/LocalInvariantProperties.lean @@ -272,8 +272,8 @@ theorem liftPropWithinAt_indep_chart_aux (he : e ∈ G.maximalAtlas M) (xe : x (xf : g x ∈ f.source) (hf' : f' ∈ G'.maximalAtlas M') (xf' : g x ∈ f'.source) (hgs : ContinuousWithinAt g s x) : P (f ∘ g ∘ e.symm) (e.symm ⁻¹' s) (e x) ↔ P (f' ∘ g ∘ e'.symm) (e'.symm ⁻¹' s) (e' x) := by - rw [← Function.comp.assoc, hG.liftPropWithinAt_indep_chart_source_aux (f ∘ g) he xe he' xe', - Function.comp.assoc, hG.liftPropWithinAt_indep_chart_target_aux xe' hf xf hf' xf' hgs] + rw [← Function.comp_assoc, hG.liftPropWithinAt_indep_chart_source_aux (f ∘ g) he xe he' xe', + Function.comp_assoc, hG.liftPropWithinAt_indep_chart_target_aux xe' hf xf hf' xf' hgs] theorem liftPropWithinAt_indep_chart [HasGroupoid M G] [HasGroupoid M' G'] (he : e ∈ G.maximalAtlas M) (xe : x ∈ e.source) (hf : f ∈ G'.maximalAtlas M') @@ -292,9 +292,9 @@ theorem liftPropWithinAt_indep_chart_source [HasGroupoid M G] (he : e ∈ G.maxi rw [liftPropWithinAt_self_source, liftPropWithinAt_iff', e.symm.continuousWithinAt_iff_continuousWithinAt_comp_right xe, e.symm_symm] refine and_congr Iff.rfl ?_ - rw [Function.comp_apply, e.left_inv xe, ← Function.comp.assoc, + rw [Function.comp_apply, e.left_inv xe, ← Function.comp_assoc, hG.liftPropWithinAt_indep_chart_source_aux (chartAt _ (g x) ∘ g) (chart_mem_maximalAtlas G x) - (mem_chart_source _ x) he xe, Function.comp.assoc] + (mem_chart_source _ x) he xe, Function.comp_assoc] /-- A version of `liftPropWithinAt_indep_chart`, only for the target. -/ theorem liftPropWithinAt_indep_chart_target [HasGroupoid M' G'] (hf : f ∈ G'.maximalAtlas M') diff --git a/Mathlib/Geometry/Manifold/MFDeriv/Atlas.lean b/Mathlib/Geometry/Manifold/MFDeriv/Atlas.lean index 5161781aac7d7..908659feaf54a 100644 --- a/Mathlib/Geometry/Manifold/MFDeriv/Atlas.lean +++ b/Mathlib/Geometry/Manifold/MFDeriv/Atlas.lean @@ -156,7 +156,7 @@ theorem tangentMap_chart_symm {p : TangentBundle I M} {q : TangentBundle I H} lemma mfderiv_chartAt_eq_tangentCoordChange {x y : M} (hsrc : x ∈ (chartAt H y).source) : mfderiv I I (chartAt H y) x = tangentCoordChange I x y x := by have := mdifferentiableAt_atlas I (ChartedSpace.chart_mem_atlas _) hsrc - simp [mfderiv, if_pos this, Function.comp.assoc] + simp [mfderiv, if_pos this, Function.comp_assoc] end Charts diff --git a/Mathlib/Geometry/Manifold/SmoothManifoldWithCorners.lean b/Mathlib/Geometry/Manifold/SmoothManifoldWithCorners.lean index b252d909311ac..5ed443618c56c 100644 --- a/Mathlib/Geometry/Manifold/SmoothManifoldWithCorners.lean +++ b/Mathlib/Geometry/Manifold/SmoothManifoldWithCorners.lean @@ -309,7 +309,7 @@ theorem symm_continuousWithinAt_comp_right_iff {X} [TopologicalSpace X] {f : H · have := h.comp I.continuousWithinAt (mapsTo_preimage _ _) simp_rw [preimage_inter, preimage_preimage, I.left_inv, preimage_id', preimage_range, inter_univ] at this - rwa [Function.comp.assoc, I.symm_comp_self] at this + rwa [Function.comp_assoc, I.symm_comp_self] at this · rw [← I.left_inv x] at h; exact h.comp I.continuousWithinAt_symm inter_subset_left protected theorem locallyCompactSpace [LocallyCompactSpace E] (I : ModelWithCorners 𝕜 E H) : diff --git a/Mathlib/LinearAlgebra/Alternating/Basic.lean b/Mathlib/LinearAlgebra/Alternating/Basic.lean index 3c306db16e0ea..1c884e7f3cd86 100644 --- a/Mathlib/LinearAlgebra/Alternating/Basic.lean +++ b/Mathlib/LinearAlgebra/Alternating/Basic.lean @@ -603,8 +603,8 @@ theorem map_perm [DecidableEq ι] [Fintype ι] (v : ι → M) (σ : Equiv.Perm -- Porting note: `apply` → `induction'` induction' σ using Equiv.Perm.swap_induction_on' with s x y hxy hI · simp - · -- Porting note: `← Function.comp.assoc` & `-Equiv.Perm.sign_swap'` are required. - simpa [← Function.comp.assoc, g.map_swap (v ∘ s) hxy, + · -- Porting note: `← Function.comp_assoc` & `-Equiv.Perm.sign_swap'` are required. + simpa [← Function.comp_assoc, g.map_swap (v ∘ s) hxy, Equiv.Perm.sign_swap hxy, -Equiv.Perm.sign_swap'] using hI theorem map_congr_perm [DecidableEq ι] [Fintype ι] (σ : Equiv.Perm ι) : diff --git a/Mathlib/LinearAlgebra/Determinant.lean b/Mathlib/LinearAlgebra/Determinant.lean index 984b62e9b92a4..ce891c2dddd94 100644 --- a/Mathlib/LinearAlgebra/Determinant.lean +++ b/Mathlib/LinearAlgebra/Determinant.lean @@ -558,7 +558,7 @@ theorem Basis.det_reindex' {ι' : Type*} [Fintype ι'] [DecidableEq ι'] (b : Ba theorem Basis.det_reindex_symm {ι' : Type*} [Fintype ι'] [DecidableEq ι'] (b : Basis ι R M) (v : ι → M) (e : ι' ≃ ι) : (b.reindex e.symm).det (v ∘ e) = b.det v := by - rw [Basis.det_reindex, Function.comp.assoc, e.self_comp_symm, Function.comp_id] + rw [Basis.det_reindex, Function.comp_assoc, e.self_comp_symm, Function.comp_id] @[simp] theorem Basis.det_map (b : Basis ι R M) (f : M ≃ₗ[R] M') (v : ι → M') : diff --git a/Mathlib/LinearAlgebra/LinearDisjoint.lean b/Mathlib/LinearAlgebra/LinearDisjoint.lean index 20c9c3b4316e4..3eb097c1e65c0 100644 --- a/Mathlib/LinearAlgebra/LinearDisjoint.lean +++ b/Mathlib/LinearAlgebra/LinearDisjoint.lean @@ -311,7 +311,7 @@ theorem linearIndependent_left_of_flat (H : M.LinearDisjoint N) [Module.Flat R N {ι : Type*} {m : ι → M} (hm : LinearIndependent R m) : LinearMap.ker (mulLeftMap N m) = ⊥ := by refine LinearMap.ker_eq_bot_of_injective ?_ classical simp_rw [mulLeftMap_eq_mulMap_comp, LinearMap.coe_comp, LinearEquiv.coe_coe, - ← Function.comp.assoc, EquivLike.injective_comp] + ← Function.comp_assoc, EquivLike.injective_comp] rw [LinearIndependent, LinearMap.ker_eq_bot] at hm exact H.injective.comp (Module.Flat.rTensor_preserves_injective_linearMap (M := N) _ hm) @@ -332,7 +332,7 @@ theorem linearIndependent_right_of_flat (H : M.LinearDisjoint N) [Module.Flat R {ι : Type*} {n : ι → N} (hn : LinearIndependent R n) : LinearMap.ker (mulRightMap M n) = ⊥ := by refine LinearMap.ker_eq_bot_of_injective ?_ classical simp_rw [mulRightMap_eq_mulMap_comp, LinearMap.coe_comp, LinearEquiv.coe_coe, - ← Function.comp.assoc, EquivLike.injective_comp] + ← Function.comp_assoc, EquivLike.injective_comp] rw [LinearIndependent, LinearMap.ker_eq_bot] at hn exact H.injective.comp (Module.Flat.lTensor_preserves_injective_linearMap (M := M) _ hn) diff --git a/Mathlib/LinearAlgebra/Matrix/Block.lean b/Mathlib/LinearAlgebra/Matrix/Block.lean index c998bad25a879..8432d56b10b42 100644 --- a/Mathlib/LinearAlgebra/Matrix/Block.lean +++ b/Mathlib/LinearAlgebra/Matrix/Block.lean @@ -62,7 +62,7 @@ theorem blockTriangular_reindex_iff {b : n → α} {e : m ≃ n} : · convert h.submatrix simp only [reindex_apply, submatrix_submatrix, submatrix_id_id, Equiv.symm_comp_self] · convert h.submatrix - simp only [comp.assoc b e e.symm, Equiv.self_comp_symm, comp_id] + simp only [comp_assoc b e e.symm, Equiv.self_comp_symm, comp_id] protected theorem BlockTriangular.transpose : M.BlockTriangular b → Mᵀ.BlockTriangular (toDual ∘ b) := diff --git a/Mathlib/LinearAlgebra/RootSystem/Hom.lean b/Mathlib/LinearAlgebra/RootSystem/Hom.lean index 2602934fad93e..f70d0830fdaee 100644 --- a/Mathlib/LinearAlgebra/RootSystem/Hom.lean +++ b/Mathlib/LinearAlgebra/RootSystem/Hom.lean @@ -74,11 +74,11 @@ def Hom.comp {ι₁ M₁ N₁ ι₂ M₂ N₂ : Type*} [AddCommGroup M₁] [Modu root_weightMap := by ext i simp only [LinearMap.coe_comp, Equiv.coe_trans] - rw [comp.assoc, f.root_weightMap, ← comp.assoc, g.root_weightMap, comp.assoc] + rw [comp_assoc, f.root_weightMap, ← comp_assoc, g.root_weightMap, comp_assoc] coroot_coweightMap := by ext i simp only [LinearMap.coe_comp, Equiv.symm_trans_apply] - rw [comp.assoc, g.coroot_coweightMap, ← comp.assoc, f.coroot_coweightMap, comp.assoc] + rw [comp_assoc, g.coroot_coweightMap, ← comp_assoc, f.coroot_coweightMap, comp_assoc] simp @[simp] diff --git a/Mathlib/Logic/Function/Basic.lean b/Mathlib/Logic/Function/Basic.lean index a7dcb29d9f608..21435518020b1 100644 --- a/Mathlib/Logic/Function/Basic.lean +++ b/Mathlib/Logic/Function/Basic.lean @@ -329,7 +329,7 @@ theorem LeftInverse.eq_rightInverse {f : α → β} {g₁ g₂ : β → α} (h (h₂ : RightInverse g₂ f) : g₁ = g₂ := calc g₁ = g₁ ∘ f ∘ g₂ := by rw [h₂.comp_eq_id, comp_id] - _ = g₂ := by rw [← comp.assoc, h₁.comp_eq_id, id_comp] + _ = g₂ := by rw [← comp_assoc, h₁.comp_eq_id, id_comp] attribute [local instance] Classical.propDecidable @@ -672,7 +672,7 @@ theorem Injective.surjective_comp_right [Nonempty γ] (hf : Injective f) : theorem Bijective.comp_right (hf : Bijective f) : Bijective fun g : β → γ ↦ g ∘ f := ⟨hf.surjective.injective_comp_right, fun g ↦ ⟨g ∘ surjInv hf.surjective, - by simp only [comp.assoc g _ f, (leftInverse_surjInv hf).comp_eq_id, comp_id]⟩⟩ + by simp only [comp_assoc g _ f, (leftInverse_surjInv hf).comp_eq_id, comp_id]⟩⟩ end Extend diff --git a/Mathlib/Logic/Function/Defs.lean b/Mathlib/Logic/Function/Defs.lean index 72aa534f806b9..78f83b38c66c0 100644 --- a/Mathlib/Logic/Function/Defs.lean +++ b/Mathlib/Logic/Function/Defs.lean @@ -88,8 +88,9 @@ theorem comp_id (f : α → β) : f ∘ id = f := rfl @[deprecated (since := "2024-01-14")] alias right_id := comp_id @[deprecated (since := "2024-01-14")] alias comp.right_id := comp_id -theorem comp.assoc (f : φ → δ) (g : β → φ) (h : α → β) : (f ∘ g) ∘ h = f ∘ g ∘ h := +theorem comp_assoc (f : φ → δ) (g : β → φ) (h : α → β) : (f ∘ g) ∘ h = f ∘ g ∘ h := rfl +@[deprecated (since := "2024-09-24")] alias comp.assoc := comp_assoc @[deprecated (since := "2024-01-14")] alias comp_const_right := comp_const diff --git a/Mathlib/MeasureTheory/Function/Jacobian.lean b/Mathlib/MeasureTheory/Function/Jacobian.lean index 2aa9266c5528d..3b9bc2e1d765d 100644 --- a/Mathlib/MeasureTheory/Function/Jacobian.lean +++ b/Mathlib/MeasureTheory/Function/Jacobian.lean @@ -1155,7 +1155,7 @@ theorem integrableOn_image_iff_integrableOn_abs_det_fderiv_smul (hs : Measurable IntegrableOn g (f '' s) μ ↔ IntegrableOn (fun x => |(f' x).det| • g (f x)) s μ := by rw [IntegrableOn, ← restrict_map_withDensity_abs_det_fderiv_eq_addHaar μ hs hf' hf, (measurableEmbedding_of_fderivWithin hs hf' hf).integrable_map_iff] - simp only [Set.restrict_eq, ← Function.comp.assoc, ENNReal.ofReal] + simp only [Set.restrict_eq, ← Function.comp_assoc, ENNReal.ofReal] rw [← (MeasurableEmbedding.subtype_coe hs).integrable_map_iff, map_comap_subtype_coe hs, restrict_withDensity hs, integrable_withDensity_iff_integrable_coe_smul₀] · simp_rw [IntegrableOn, Real.coe_toNNReal _ (abs_nonneg _), Function.comp_apply] diff --git a/Mathlib/ModelTheory/Basic.lean b/Mathlib/ModelTheory/Basic.lean index 0643bc17fdebe..e19707451b558 100644 --- a/Mathlib/ModelTheory/Basic.lean +++ b/Mathlib/ModelTheory/Basic.lean @@ -474,7 +474,7 @@ def comp (hnp : N ↪[L] P) (hmn : M ↪[L] N) : M ↪[L] P where -- Porting note: should be done by autoparam? map_fun' := by intros; simp only [Function.comp_apply, map_fun]; trivial -- Porting note: should be done by autoparam? - map_rel' := by intros; rw [Function.comp.assoc, map_rel, map_rel] + map_rel' := by intros; rw [Function.comp_assoc, map_rel, map_rel] @[simp] theorem comp_apply (g : N ↪[L] P) (f : M ↪[L] N) (x : M) : g.comp f x = g (f x) := @@ -551,11 +551,11 @@ def symm (f : M ≃[L] N) : N ≃[L] M := simp only [Equiv.toFun_as_coe] rw [Equiv.symm_apply_eq] refine Eq.trans ?_ (f.map_fun' f' (f.toEquiv.symm ∘ x)).symm - rw [← Function.comp.assoc, Equiv.toFun_as_coe, Equiv.self_comp_symm, Function.id_comp] + rw [← Function.comp_assoc, Equiv.toFun_as_coe, Equiv.self_comp_symm, Function.id_comp] map_rel' := fun n r {x} => by simp only [Equiv.toFun_as_coe] refine (f.map_rel' r (f.toEquiv.symm ∘ x)).symm.trans ?_ - rw [← Function.comp.assoc, Equiv.toFun_as_coe, Equiv.self_comp_symm, Function.id_comp] } + rw [← Function.comp_assoc, Equiv.toFun_as_coe, Equiv.self_comp_symm, Function.id_comp] } instance hasCoeToFun : CoeFun (M ≃[L] N) fun _ => M → N := DFunLike.hasCoeToFun @@ -648,7 +648,7 @@ def comp (hnp : N ≃[L] P) (hmn : M ≃[L] N) : M ≃[L] P := -- Porting note: should be done by autoparam? map_fun' := by intros; simp only [Function.comp_apply, map_fun]; trivial -- Porting note: should be done by autoparam? - map_rel' := by intros; rw [Function.comp.assoc, map_rel, map_rel] } + map_rel' := by intros; rw [Function.comp_assoc, map_rel, map_rel] } @[simp] theorem comp_apply (g : N ≃[L] P) (f : M ≃[L] N) (x : M) : g.comp f x = g (f x) := @@ -830,8 +830,8 @@ def inducedStructureEquiv (e : M ≃ N) : @Language.Equiv L M N _ (inducedStruct letI : L.Structure N := inducedStructure e exact { e with - map_fun' := @fun n f x => by simp [← Function.comp.assoc e.symm e x] - map_rel' := @fun n r x => by simp [← Function.comp.assoc e.symm e x] } + map_fun' := @fun n f x => by simp [← Function.comp_assoc e.symm e x] + map_rel' := @fun n r x => by simp [← Function.comp_assoc e.symm e x] } @[simp] theorem toEquiv_inducedStructureEquiv (e : M ≃ N) : diff --git a/Mathlib/ModelTheory/DirectLimit.lean b/Mathlib/ModelTheory/DirectLimit.lean index a9c1fe39191e1..3a74358878660 100644 --- a/Mathlib/ModelTheory/DirectLimit.lean +++ b/Mathlib/ModelTheory/DirectLimit.lean @@ -353,13 +353,13 @@ def lift (g : ∀ i, G i ↪[L] P) (Hg : ∀ i j hij x, g j (f i j hij x) = g i map_fun' F x := by obtain ⟨i, y, rfl⟩ := exists_quotient_mk'_sigma_mk'_eq G f x change _ = funMap F (Quotient.lift _ _ ∘ Quotient.mk _ ∘ Structure.Sigma.mk f i ∘ y) - rw [funMap_quotient_mk'_sigma_mk', ← Function.comp.assoc, Quotient.lift_comp_mk] + rw [funMap_quotient_mk'_sigma_mk', ← Function.comp_assoc, Quotient.lift_comp_mk] simp only [Quotient.lift_mk, Embedding.map_fun] rfl map_rel' R x := by obtain ⟨i, y, rfl⟩ := exists_quotient_mk'_sigma_mk'_eq G f x change RelMap R (Quotient.lift _ _ ∘ Quotient.mk _ ∘ Structure.Sigma.mk f i ∘ y) ↔ _ - rw [relMap_quotient_mk'_sigma_mk' G f, ← (g i).map_rel R y, ← Function.comp.assoc, + rw [relMap_quotient_mk'_sigma_mk' G f, ← (g i).map_rel R y, ← Function.comp_assoc, Quotient.lift_comp_mk] rfl diff --git a/Mathlib/ModelTheory/ElementaryMaps.lean b/Mathlib/ModelTheory/ElementaryMaps.lean index ea469044e0dc8..54428842a22a5 100644 --- a/Mathlib/ModelTheory/ElementaryMaps.lean +++ b/Mathlib/ModelTheory/ElementaryMaps.lean @@ -79,12 +79,12 @@ theorem map_boundedFormula (f : M ↪ₑ[L] N) {α : Type*} {n : ℕ} (φ : L.Bo f.map_formula' ((φ.restrictFreeVar id).toFormula.relabel (Fintype.equivFin _)) (Sum.elim (v ∘ (↑)) xs ∘ (Fintype.equivFin _).symm) simp only [Formula.realize_relabel, BoundedFormula.realize_toFormula, iff_eq_eq] at h - rw [← Function.comp.assoc _ _ (Fintype.equivFin _).symm, - Function.comp.assoc _ (Fintype.equivFin _).symm (Fintype.equivFin _), - _root_.Equiv.symm_comp_self, Function.comp_id, Function.comp.assoc, Sum.elim_comp_inl, - Function.comp.assoc _ _ Sum.inr, Sum.elim_comp_inr, ← Function.comp.assoc] at h + rw [← Function.comp_assoc _ _ (Fintype.equivFin _).symm, + Function.comp_assoc _ (Fintype.equivFin _).symm (Fintype.equivFin _), + _root_.Equiv.symm_comp_self, Function.comp_id, Function.comp_assoc, Sum.elim_comp_inl, + Function.comp_assoc _ _ Sum.inr, Sum.elim_comp_inr, ← Function.comp_assoc] at h refine h.trans ?_ - erw [Function.comp.assoc _ _ (Fintype.equivFin _), _root_.Equiv.symm_comp_self, + erw [Function.comp_assoc _ _ (Fintype.equivFin _), _root_.Equiv.symm_comp_self, Function.comp_id, Sum.elim_comp_inl, Sum.elim_comp_inr (v ∘ Subtype.val) xs, ← Set.inclusion_eq_id (s := (BoundedFormula.freeVarFinset φ : Set α)) Set.Subset.rfl, BoundedFormula.realize_restrictFreeVar Set.Subset.rfl] diff --git a/Mathlib/ModelTheory/Syntax.lean b/Mathlib/ModelTheory/Syntax.lean index c302df830a56f..fb5f3691aab1a 100644 --- a/Mathlib/ModelTheory/Syntax.lean +++ b/Mathlib/ModelTheory/Syntax.lean @@ -418,7 +418,7 @@ theorem castLE_castLE {k m n} (km : k ≤ m) (mn : m ≤ n) (φ : L.BoundedFormu | rel => intros simp only [castLE, eq_self_iff_true, heq_iff_eq] - rw [← Function.comp.assoc, Term.relabel_comp_relabel] + rw [← Function.comp_assoc, Term.relabel_comp_relabel] simp | imp _ _ ih1 ih2 => simp [ih1, ih2] | all _ ih3 => intros; simp only [castLE, ih3] diff --git a/Mathlib/Topology/Algebra/InfiniteSum/Basic.lean b/Mathlib/Topology/Algebra/InfiniteSum/Basic.lean index 9642c81b12ef4..bc17c8afdc322 100644 --- a/Mathlib/Topology/Algebra/InfiniteSum/Basic.lean +++ b/Mathlib/Topology/Algebra/InfiniteSum/Basic.lean @@ -204,7 +204,7 @@ protected theorem Multipliable.map_iff_of_leftInverse [CommMonoid γ] [Topologic Multipliable (g ∘ f) ↔ Multipliable f := ⟨fun h ↦ by have := h.map _ hg' - rwa [← Function.comp.assoc, hinv.id] at this, fun h ↦ h.map _ hg⟩ + rwa [← Function.comp_assoc, hinv.id] at this, fun h ↦ h.map _ hg⟩ @[to_additive] theorem Multipliable.map_tprod [CommMonoid γ] [TopologicalSpace γ] [T2Space γ] (hf : Multipliable f) diff --git a/Mathlib/Topology/Category/CompHaus/Projective.lean b/Mathlib/Topology/Category/CompHaus/Projective.lean index 17bdb7ef5c926..97532c9b45d96 100644 --- a/Mathlib/Topology/Category/CompHaus/Projective.lean +++ b/Mathlib/Topology/Category/CompHaus/Projective.lean @@ -52,7 +52,7 @@ instance projective_ultrafilter (X : Type*) : Projective (of <| Ultrafilter X) w let g'' : ContinuousMap Y Z := g have : g'' ∘ g' = id := hg'.comp_eq_id -- This used to be `rw`, but we need `erw` after leanprover/lean4#2644 - erw [comp.assoc, ultrafilter_extend_extends, ← comp.assoc, this, id_comp] + erw [comp_assoc, ultrafilter_extend_extends, ← comp_assoc, this, id_comp] /-- For any compact Hausdorff space `X`, the natural map `Ultrafilter X → X` is a projective presentation. -/ diff --git a/Mathlib/Topology/Category/Profinite/Nobeling.lean b/Mathlib/Topology/Category/Profinite/Nobeling.lean index b666e7f0d9593..d9f4b3c3fea60 100644 --- a/Mathlib/Topology/Category/Profinite/Nobeling.lean +++ b/Mathlib/Topology/Category/Profinite/Nobeling.lean @@ -412,7 +412,7 @@ theorem evalFacProps {l : Products I} (J K : I → Prop) have : l.eval (π C J) ∘ Homeomorph.setCongr (proj_eq_of_subset C J K hJK) = l.eval (π (π C K) J) := by ext; simp [Homeomorph.setCongr, Products.eval_eq] - rw [ProjRestricts, ← Function.comp.assoc, this, ← evalFacProp (π C K) J h] + rw [ProjRestricts, ← Function.comp_assoc, this, ← evalFacProp (π C K) J h] theorem prop_of_isGood {l : Products I} (J : I → Prop) [∀ j, Decidable (J j)] (h : l.isGood (π C J)) : ∀ a, a ∈ l.val → J a := by @@ -1043,7 +1043,7 @@ theorem smaller_mono {o₁ o₂ : Ordinal} (h : o₁ ≤ o₂) : smaller C o₁ ext x rw [eval, ← Products.eval_πs' _ h (Products.prop_of_isGood C _ gl), eval] · rw [← LocallyConstant.coe_inj, coe_πs C o₂, ← LocallyConstant.toFun_eq_coe, coe_πs', - Function.comp.assoc, projRestricts_comp_projRestrict C _, coe_πs] + Function.comp_assoc, projRestricts_comp_projRestrict C _, coe_πs] rfl end GoodProducts diff --git a/Mathlib/Topology/Category/Profinite/Projective.lean b/Mathlib/Topology/Category/Profinite/Projective.lean index becda45ececde..98eb2deeef7fc 100644 --- a/Mathlib/Topology/Category/Profinite/Projective.lean +++ b/Mathlib/Topology/Category/Profinite/Projective.lean @@ -51,7 +51,7 @@ instance projective_ultrafilter (X : Type u) : Projective (of <| Ultrafilter X) let g'' : ContinuousMap Y Z := g have : g'' ∘ g' = id := hg'.comp_eq_id -- This used to be `rw`, but we need `erw` after leanprover/lean4#2644 - erw [comp.assoc, ultrafilter_extend_extends, ← comp.assoc, this, id_comp] + erw [comp_assoc, ultrafilter_extend_extends, ← comp_assoc, this, id_comp] /-- For any profinite `X`, the natural map `Ultrafilter X → X` is a projective presentation. -/ def projectivePresentation (X : Profinite.{u}) : ProjectivePresentation X where diff --git a/Mathlib/Topology/Category/TopCat/EffectiveEpi.lean b/Mathlib/Topology/Category/TopCat/EffectiveEpi.lean index 75ee84190369c..35693a3a1dedc 100644 --- a/Mathlib/Topology/Category/TopCat/EffectiveEpi.lean +++ b/Mathlib/Topology/Category/TopCat/EffectiveEpi.lean @@ -60,7 +60,7 @@ theorem effectiveEpi_iff_quotientMap {B X : TopCat.{u}} (π : X ⟶ B) : let F := parallelPair hπ.left hπ.right let i : B ≅ colimit F := hπ.isColimit.coconePointUniqueUpToIso (colimit.isColimit _) suffices QuotientMap (homeoOfIso i ∘ π) by - simpa [← Function.comp.assoc] using (homeoOfIso i).symm.quotientMap.comp this + simpa [← Function.comp_assoc] using (homeoOfIso i).symm.quotientMap.comp this constructor /- Effective epimorphisms are epimorphisms and epimorphisms in `TopCat` are surjective. -/ · change Function.Surjective (π ≫ i.hom) diff --git a/Mathlib/Topology/ExtremallyDisconnected.lean b/Mathlib/Topology/ExtremallyDisconnected.lean index a5d3b08560a46..f81a6b4448fd2 100644 --- a/Mathlib/Topology/ExtremallyDisconnected.lean +++ b/Mathlib/Topology/ExtremallyDisconnected.lean @@ -88,7 +88,7 @@ theorem StoneCech.projective [DiscreteTopology X] : CompactT2.Projective (StoneC let h : StoneCech X → Y := stoneCechExtend ht have hh : Continuous h := continuous_stoneCechExtend ht refine ⟨h, hh, denseRange_stoneCechUnit.equalizer (hg.comp hh) hf ?_⟩ - rw [comp.assoc, stoneCechExtend_extends ht, ← comp.assoc, hs, id_comp] + rw [comp_assoc, stoneCechExtend_extends ht, ← comp_assoc, hs, id_comp] protected theorem CompactT2.Projective.extremallyDisconnected [CompactSpace X] [T2Space X] (h : CompactT2.Projective X) : ExtremallyDisconnected X := by @@ -271,7 +271,7 @@ protected theorem CompactT2.ExtremallyDisconnected.projective [ExtremallyDisconn have π₂_cont : Continuous π₂ := continuous_snd.comp continuous_subtype_val refine ⟨E.restrict π₂ ∘ ρ'.symm, ⟨π₂_cont.continuousOn.restrict.comp ρ'.symm.continuous, ?_⟩⟩ suffices f ∘ E.restrict π₂ = φ ∘ ρ' by - rw [← comp.assoc, this, comp.assoc, Homeomorph.self_comp_symm, comp_id] + rw [← comp_assoc, this, comp_assoc, Homeomorph.self_comp_symm, comp_id] ext x exact x.val.mem.symm diff --git a/Mathlib/Topology/Homeomorph.lean b/Mathlib/Topology/Homeomorph.lean index 3a5abc02d2bd4..bc14d3525fda0 100644 --- a/Mathlib/Topology/Homeomorph.lean +++ b/Mathlib/Topology/Homeomorph.lean @@ -451,14 +451,14 @@ theorem comp_continuousWithinAt_iff (h : X ≃ₜ Y) (f : Z → X) (s : Set Z) ( theorem comp_isOpenMap_iff (h : X ≃ₜ Y) {f : Z → X} : IsOpenMap (h ∘ f) ↔ IsOpenMap f := by refine ⟨?_, fun hf => h.isOpenMap.comp hf⟩ intro hf - rw [← Function.id_comp f, ← h.symm_comp_self, Function.comp.assoc] + rw [← Function.id_comp f, ← h.symm_comp_self, Function.comp_assoc] exact h.symm.isOpenMap.comp hf @[simp] theorem comp_isOpenMap_iff' (h : X ≃ₜ Y) {f : Y → Z} : IsOpenMap (f ∘ h) ↔ IsOpenMap f := by refine ⟨?_, fun hf => hf.comp h.isOpenMap⟩ intro hf - rw [← Function.comp_id f, ← h.self_comp_symm, ← Function.comp.assoc] + rw [← Function.comp_id f, ← h.self_comp_symm, ← Function.comp_assoc] exact hf.comp h.symm.isOpenMap /-- A homeomorphism `h : X ≃ₜ Y` lifts to a homeomorphism between subtypes corresponding to