chore(Function): rename some lemmas (#9738)

- Merge `Function.left_id` and `Function.comp.left_id` into `Function.id_comp`. - Merge `Function.right_id` and `Function.comp.right_id` into `Function.comp_id`. - Merge `Function.comp_const_right` and `Function.comp_const` into `Function.comp_const`, use explicit arguments. - Move `Function.const_comp` to `Mathlib.Init.Function`, use explicit arguments.
leanprover-community · Jan 16, 2024 · 00364d4 · 00364d4
1 parent 1abaf8f
commit 00364d4
Show file tree

Hide file tree

Showing 44 changed files with 99 additions and 111 deletions.
diff --git a/Mathlib/Algebra/Category/ModuleCat/Free.lean b/Mathlib/Algebra/Category/ModuleCat/Free.lean
@@ -138,7 +138,7 @@ theorem span_rightExact {w : ι' → S.X₃} (hv : ⊤ ≤ span R (range v))
     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),
-      Function.comp.left_id]
+      Function.id_comp]
 
 end Span
 

diff --git a/Mathlib/Algebra/Order/Rearrangement.lean b/Mathlib/Algebra/Order/Rearrangement.lean
@@ -167,10 +167,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.right_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.right_id]
+    · rw [comp.assoc, self_comp_symm, comp_id]
     · rw [σ.symm.eq_preimage_iff_image_eq]
       exact Set.image_perm hσinv
 #align monovary_on.sum_comp_perm_smul_eq_sum_smul_iff MonovaryOn.sum_comp_perm_smul_eq_sum_smul_iff

diff --git a/Mathlib/Analysis/BoundedVariation.lean b/Mathlib/Analysis/BoundedVariation.lean
@@ -888,7 +888,7 @@ theorem ae_differentiableWithinAt_of_mem {f : ℝ → V} {s : Set ℝ}
   suffices H : ∀ᵐ x, x ∈ s → DifferentiableWithinAt ℝ (A ∘ f) s x
   · filter_upwards [H] with x hx xs
     have : f = (A.symm ∘ A) ∘ f := by
-      simp only [ContinuousLinearEquiv.symm_comp_self, Function.comp.left_id]
+      simp only [ContinuousLinearEquiv.symm_comp_self, Function.id_comp]
     rw [this]
     exact A.symm.differentiableAt.comp_differentiableWithinAt x (hx xs)
   apply ae_differentiableWithinAt_of_mem_pi

diff --git a/Mathlib/Analysis/Calculus/ContDiff/FiniteDimension.lean b/Mathlib/Analysis/Calculus/ContDiff/FiniteDimension.lean
@@ -39,7 +39,7 @@ theorem contDiffOn_clm_apply {n : ℕ∞} {f : E → F →L[𝕜] G} {s : Set E}
   have hd : d = finrank 𝕜 (Fin d → 𝕜) := (finrank_fin_fun 𝕜).symm
   let e₁ := ContinuousLinearEquiv.ofFinrankEq hd
   let e₂ := (e₁.arrowCongr (1 : G ≃L[𝕜] G)).trans (ContinuousLinearEquiv.piRing (Fin d))
-  rw [← comp.left_id f, ← e₂.symm_comp_self]
+  rw [← id_comp f, ← e₂.symm_comp_self]
   exact e₂.symm.contDiff.comp_contDiffOn (contDiffOn_pi.mpr fun i => h _)
 #align cont_diff_on_clm_apply contDiffOn_clm_apply
 

diff --git a/Mathlib/Analysis/Calculus/IteratedDeriv.lean b/Mathlib/Analysis/Calculus/IteratedDeriv.lean
@@ -94,7 +94,7 @@ 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,
-    Function.left_id]
+    Function.id_comp]
 #align iterated_fderiv_within_eq_equiv_comp iteratedFDerivWithin_eq_equiv_comp
 
 /-- The `n`-th Fréchet derivative applied to a vector `(m 0, ..., m (n-1))` is the derivative
@@ -230,7 +230,7 @@ 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,
-    Function.left_id]
+    Function.id_comp]
 #align iterated_fderiv_eq_equiv_comp iteratedFDeriv_eq_equiv_comp
 
 /-- The `n`-th Fréchet derivative applied to a vector `(m 0, ..., m (n-1))` is the derivative

diff --git a/Mathlib/Analysis/Calculus/Rademacher.lean b/Mathlib/Analysis/Calculus/Rademacher.lean
@@ -357,7 +357,7 @@ theorem ae_differentiableWithinAt_of_mem {f : E → F} (hf : LipschitzOnWith C f
   suffices H : ∀ᵐ x ∂μ, x ∈ s → DifferentiableWithinAt ℝ (A ∘ f) s x by
     filter_upwards [H] with x hx xs
     have : f = (A.symm ∘ A) ∘ f := by
-      simp only [ContinuousLinearEquiv.symm_comp_self, Function.comp.left_id]
+      simp only [ContinuousLinearEquiv.symm_comp_self, Function.id_comp]
     rw [this]
     exact A.symm.differentiableAt.comp_differentiableWithinAt x (hx xs)
   apply ae_differentiableWithinAt_of_mem_pi

diff --git a/Mathlib/Analysis/Convex/Intrinsic.lean b/Mathlib/Analysis/Convex/Intrinsic.lean
@@ -260,7 +260,7 @@ theorem image_intrinsicInterior (φ : P →ᵃⁱ[𝕜] Q) (s : Set P) :
   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.right_id, preimage_comp, φ.injective.preimage_image]
+    Function.comp_id, preimage_comp, φ.injective.preimage_image]
 #align affine_isometry.image_intrinsic_interior AffineIsometry.image_intrinsicInterior
 
 @[simp]
@@ -274,7 +274,7 @@ theorem image_intrinsicFrontier (φ : P →ᵃⁱ[𝕜] Q) (s : Set P) :
   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.right_id, preimage_comp, φ.injective.preimage_image]
+    Function.comp_id, preimage_comp, φ.injective.preimage_image]
 #align affine_isometry.image_intrinsic_frontier AffineIsometry.image_intrinsicFrontier
 
 @[simp]
@@ -288,7 +288,7 @@ theorem image_intrinsicClosure (φ : P →ᵃⁱ[𝕜] Q) (s : Set P) :
   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.right_id, preimage_comp, φ.injective.preimage_image]
+    Function.comp_id, preimage_comp, φ.injective.preimage_image]
 #align affine_isometry.image_intrinsic_closure AffineIsometry.image_intrinsicClosure
 
 end AffineIsometry

diff --git a/Mathlib/Analysis/NormedSpace/FiniteDimension.lean b/Mathlib/Analysis/NormedSpace/FiniteDimension.lean
@@ -568,7 +568,7 @@ theorem continuousOn_clm_apply {X : Type*} [TopologicalSpace X] [FiniteDimension
   let e₁ : E ≃L[𝕜] Fin d → 𝕜 := ContinuousLinearEquiv.ofFinrankEq hd
   let e₂ : (E →L[𝕜] F) ≃L[𝕜] Fin d → F :=
     (e₁.arrowCongr (1 : F ≃L[𝕜] F)).trans (ContinuousLinearEquiv.piRing (Fin d))
-  rw [← Function.comp.left_id f, ← e₂.symm_comp_self]
+  rw [← f.id_comp, ← e₂.symm_comp_self]
   exact e₂.symm.continuous.comp_continuousOn (continuousOn_pi.mpr fun i => h _)
 #align continuous_on_clm_apply continuousOn_clm_apply
 

diff --git a/Mathlib/Analysis/NormedSpace/Multilinear/Curry.lean b/Mathlib/Analysis/NormedSpace/Multilinear/Curry.lean
@@ -534,7 +534,7 @@ theorem norm_domDomCongr (σ : ι ≃ ι') (f : ContinuousMultilinearMap 𝕜 (f
     ‖domDomCongr σ f‖ = ‖f‖ := by
   simp only [norm_def, LinearEquiv.coe_mk, ← σ.prod_comp,
     (σ.arrowCongr (Equiv.refl G)).surjective.forall, domDomCongr_apply, Equiv.arrowCongr_apply,
-    Equiv.coe_refl, comp.left_id, comp_apply, Equiv.symm_apply_apply, id]
+    Equiv.coe_refl, id_comp, comp_apply, Equiv.symm_apply_apply, id]
 #align continuous_multilinear_map.norm_dom_dom_congr ContinuousMultilinearMap.norm_domDomCongr
 
 /-- An equivalence of the index set defines a linear isometric equivalence between the spaces

diff --git a/Mathlib/Analysis/SpecialFunctions/Complex/Arg.lean b/Mathlib/Analysis/SpecialFunctions/Complex/Arg.lean
@@ -640,7 +640,7 @@ theorem tendsto_arg_nhdsWithin_im_nonneg_of_re_neg_of_im_zero {z : ℂ} (hre : z
 theorem continuousAt_arg_coe_angle (h : x ≠ 0) : ContinuousAt ((↑) ∘ arg : ℂ → Real.Angle) x := by
   by_cases hs : x ∈ slitPlane
   · exact Real.Angle.continuous_coe.continuousAt.comp (continuousAt_arg hs)
-  · rw [← Function.comp.right_id (((↑) : ℝ → Real.Angle) ∘ arg),
+  · rw [← Function.comp_id (((↑) : ℝ → Real.Angle) ∘ arg),
       (Function.funext_iff.2 fun _ => (neg_neg _).symm : (id : ℂ → ℂ) = Neg.neg ∘ Neg.neg), ←
       Function.comp.assoc]
     refine' ContinuousAt.comp _ continuous_neg.continuousAt

diff --git a/Mathlib/Analysis/SpecialFunctions/Log/NegMulLog.lean b/Mathlib/Analysis/SpecialFunctions/Log/NegMulLog.lean
@@ -52,8 +52,7 @@ lemma hasDerivAt_mul_log {x : ℝ} (hx : x ≠ 0) : HasDerivAt (fun x ↦ x * lo
   simp [hx]
 
 lemma deriv2_mul_log {x : ℝ} (hx : x ≠ 0) : deriv^[2] (fun x ↦ x * log x) x = x⁻¹ := by
-  simp only [Function.iterate_succ, Function.iterate_zero, Function.comp.left_id,
-    Function.comp_apply]
+  simp only [Function.iterate_succ, Function.iterate_zero, Function.id_comp, Function.comp_apply]
   suffices ∀ᶠ y in (𝓝 x), deriv (fun x ↦ x * log x) y = log y + 1 by
     refine (Filter.EventuallyEq.deriv_eq this).trans ?_
     rw [deriv_add_const, deriv_log x]
@@ -118,7 +117,7 @@ lemma hasDerivAt_negMulLog {x : ℝ} (hx : x ≠ 0) : HasDerivAt negMulLog (- lo
 lemma deriv2_negMulLog {x : ℝ} (hx : x ≠ 0) : deriv^[2] negMulLog x = - x⁻¹ := by
   rw [negMulLog_eq_neg]
   have h := deriv2_mul_log hx
-  simp only [Function.iterate_succ, Function.iterate_zero, Function.comp.left_id,
+  simp only [Function.iterate_succ, Function.iterate_zero, Function.id_comp,
     Function.comp_apply, deriv.neg', differentiableAt_id', differentiableAt_log_iff, ne_eq] at h ⊢
   rw [h]
 

diff --git a/Mathlib/CategoryTheory/Monad/Types.lean b/Mathlib/CategoryTheory/Monad/Types.lean
@@ -57,7 +57,7 @@ def eq : KleisliCat m ≌ Kleisli (ofTypeMonad m) where
         funext t
         -- Porting note: missing tactic `unfold_projs`, using `change` instead.
         change _ = joinM (g <$> (f t))
-        simp only [joinM, seq_bind_eq, Function.comp.left_id]
+        simp only [joinM, seq_bind_eq, Function.id_comp]
         rfl }
   inverse :=
     { obj := fun X => X
@@ -75,7 +75,7 @@ def eq : KleisliCat m ≌ Kleisli (ofTypeMonad m) where
         dsimp
         -- Porting note: missing tactic `unfold_projs`, using `change` instead.
         change joinM (g <$> (f t)) = _
-        simp only [joinM, seq_bind_eq, Function.comp.left_id]
+        simp only [joinM, seq_bind_eq, Function.id_comp]
         rfl }
   unitIso := by
     refine' NatIso.ofComponents (fun X => Iso.refl X) fun f => _

diff --git a/Mathlib/Data/Fin/Tuple/Sort.lean b/Mathlib/Data/Fin/Tuple/Sort.lean
@@ -185,7 +185,7 @@ theorem eq_sort_iff :
 
 /-- The permutation that sorts `f` is the identity if and only if `f` is monotone. -/
 theorem sort_eq_refl_iff_monotone : sort f = Equiv.refl _ ↔ Monotone f := by
-  rw [eq_comm, eq_sort_iff, Equiv.coe_refl, Function.comp.right_id]
+  rw [eq_comm, eq_sort_iff, Equiv.coe_refl, Function.comp_id]
   simp only [id.def, and_iff_left_iff_imp]
   exact fun _ _ _ hij _ => hij
 #align tuple.sort_eq_refl_iff_monotone Tuple.sort_eq_refl_iff_monotone

diff --git a/Mathlib/Data/Finset/Lattice.lean b/Mathlib/Data/Finset/Lattice.lean
@@ -305,7 +305,7 @@ theorem sup_set_eq_biUnion (s : Finset α) (f : α → Set β) : s.sup f = ⋃ x
 
 theorem sup_eq_sSup_image [CompleteLattice β] (s : Finset α) (f : α → β) :
     s.sup f = sSup (f '' s) :=
-  by classical rw [← Finset.coe_image, ← sup_id_eq_sSup, sup_image, Function.comp.left_id]
+  by classical rw [← Finset.coe_image, ← sup_id_eq_sSup, sup_image, Function.id_comp]
 #align finset.sup_eq_Sup_image Finset.sup_eq_sSup_image
 
 /-! ### inf -/

diff --git a/Mathlib/Data/List/FinRange.lean b/Mathlib/Data/List/FinRange.lean
@@ -52,7 +52,7 @@ theorem ofFn_id (n) : ofFn id = finRange n :=
 #align list.of_fn_id List.ofFn_id
 
 theorem ofFn_eq_map {α n} {f : Fin n → α} : ofFn f = (finRange n).map f := by
-  rw [← ofFn_id, map_ofFn, Function.right_id]
+  rw [← ofFn_id, map_ofFn, Function.comp_id]
 #align list.of_fn_eq_map List.ofFn_eq_map
 
 theorem nodup_ofFn_ofInjective {α n} {f : Fin n → α} (hf : Function.Injective f) :

diff --git a/Mathlib/Data/Matrix/Basic.lean b/Mathlib/Data/Matrix/Basic.lean
@@ -2567,9 +2567,9 @@ theorem mul_submatrix_one [Fintype n] [Finite o] [NonAssocSemiring α] [Decidabl
   cases nonempty_fintype o
   let A := M.submatrix id e₁.symm
   have : M = A.submatrix id e₁ := by
-    simp only [submatrix_submatrix, Function.comp.right_id, submatrix_id_id, Equiv.symm_comp_self]
+    simp only [submatrix_submatrix, Function.comp_id, submatrix_id_id, Equiv.symm_comp_self]
   rw [this, submatrix_mul_equiv]
-  simp only [Matrix.mul_one, submatrix_submatrix, Function.comp.right_id, submatrix_id_id,
+  simp only [Matrix.mul_one, submatrix_submatrix, Function.comp_id, submatrix_id_id,
     Equiv.symm_comp_self]
 #align matrix.mul_submatrix_one Matrix.mul_submatrix_one
 
@@ -2579,9 +2579,9 @@ theorem one_submatrix_mul [Fintype m] [Finite o] [NonAssocSemiring α] [Decidabl
   cases nonempty_fintype o
   let A := M.submatrix e₂.symm id
   have : M = A.submatrix e₂ id := by
-    simp only [submatrix_submatrix, Function.comp.right_id, submatrix_id_id, Equiv.symm_comp_self]
+    simp only [submatrix_submatrix, Function.comp_id, submatrix_id_id, Equiv.symm_comp_self]
   rw [this, submatrix_mul_equiv]
-  simp only [Matrix.one_mul, submatrix_submatrix, Function.comp.right_id, submatrix_id_id,
+  simp only [Matrix.one_mul, submatrix_submatrix, Function.comp_id, submatrix_id_id,
     Equiv.symm_comp_self]
 #align matrix.one_submatrix_mul Matrix.one_submatrix_mul
 

diff --git a/Mathlib/Data/Multiset/Basic.lean b/Mathlib/Data/Multiset/Basic.lean
@@ -2728,7 +2728,7 @@ for more discussion.
 @[simp]
 theorem map_count_True_eq_filter_card (s : Multiset α) (p : α → Prop) [DecidablePred p] :
     (s.map p).count True = card (s.filter p) := by
-  simp only [count_eq_card_filter_eq, map_filter, card_map, Function.comp.left_id,
+  simp only [count_eq_card_filter_eq, map_filter, card_map, Function.id_comp,
     eq_true_eq_id, Function.comp_apply]
 #align multiset.map_count_true_eq_filter_card Multiset.map_count_True_eq_filter_card
 

diff --git a/Mathlib/Data/MvPolynomial/Monad.lean b/Mathlib/Data/MvPolynomial/Monad.lean
@@ -202,7 +202,7 @@ theorem join₂_comp_map (f : R →+* MvPolynomial σ S) : join₂.comp (map f)
 #align mv_polynomial.join₂_comp_map MvPolynomial.join₂_comp_map
 
 theorem aeval_id_rename (f : σ → MvPolynomial τ R) (p : MvPolynomial σ R) :
-    aeval id (rename f p) = aeval f p := by rw [aeval_rename, Function.comp.left_id]
+    aeval id (rename f p) = aeval f p := by rw [aeval_rename, Function.id_comp]
 #align mv_polynomial.aeval_id_rename MvPolynomial.aeval_id_rename
 
 @[simp]

diff --git a/Mathlib/Data/Nat/Parity.lean b/Mathlib/Data/Nat/Parity.lean
@@ -305,7 +305,7 @@ theorem iterate_bit0 (hf : Involutive f) (n : ℕ) : f^[bit0 n] = id := by
 #align function.involutive.iterate_bit0 Function.Involutive.iterate_bit0
 
 theorem iterate_bit1 (hf : Involutive f) (n : ℕ) : f^[bit1 n] = f := by
-  rw [bit1, ← succ_eq_add_one, iterate_succ, hf.iterate_bit0, comp.left_id]
+  rw [bit1, ← succ_eq_add_one, iterate_succ, hf.iterate_bit0, id_comp]
 #align function.involutive.iterate_bit1 Function.Involutive.iterate_bit1
 
 end
@@ -320,7 +320,7 @@ theorem iterate_even (hf : Involutive f) (hn : Even n) : f^[n] = id := by
 
 theorem iterate_odd (hf : Involutive f) (hn : Odd n) : f^[n] = f := by
   rcases hn with ⟨m, rfl⟩
-  rw [iterate_add, hf.iterate_two_mul, comp.left_id, iterate_one]
+  rw [iterate_add, hf.iterate_two_mul, id_comp, iterate_one]
 #align function.involutive.iterate_odd Function.Involutive.iterate_odd
 
 theorem iterate_eq_self (hf : Involutive f) (hne : f ≠ id) : f^[n] = f ↔ Odd n :=

diff --git a/Mathlib/Data/QPF/Multivariate/Constructions/Cofix.lean b/Mathlib/Data/QPF/Multivariate/Constructions/Cofix.lean
@@ -403,17 +403,17 @@ theorem liftR_map_last [lawful : LawfulMvFunctor F]
     dsimp
     apply eq_of_drop_last_eq
     · dsimp
-      simp only [prod_map_id, dropFun_prod, dropFun_appendFun, dropFun_diag, id_comp,
+      simp only [prod_map_id, dropFun_prod, dropFun_appendFun, dropFun_diag, TypeVec.id_comp,
         dropFun_toSubtype]
-      erw [toSubtype_of_subtype_assoc, id_comp]
+      erw [toSubtype_of_subtype_assoc, TypeVec.id_comp]
       clear liftR_map_last q mvf lawful F x R f g hh h b c
       ext (i x) : 2
       induction i with
       | fz => rfl
       | fs _ ih =>
         apply ih
     simp only [lastFun_from_append1_drop_last, lastFun_toSubtype, lastFun_appendFun,
-      lastFun_subtypeVal, comp.left_id, lastFun_comp, lastFun_prod]
+      lastFun_subtypeVal, Function.id_comp, lastFun_comp, lastFun_prod]
     ext1
     rfl
   liftR_map _ _ _ _ (toSubtype _ ⊚ fromAppend1DropLast ⊚ c ⊚ b) hh

diff --git a/Mathlib/Dynamics/Ergodic/Ergodic.lean b/Mathlib/Dynamics/Ergodic/Ergodic.lean
@@ -101,9 +101,9 @@ theorem preErgodic_conjugate_iff {e : α ≃ᵐ β} (h : MeasurePreserving e μ
   refine' ⟨fun hf => preErgodic_of_preErgodic_conjugate (h.symm e) hf _,
       fun hf => preErgodic_of_preErgodic_conjugate h hf _⟩
   · change (e.symm ∘ e) ∘ f ∘ e.symm = f ∘ e.symm
-    rw [MeasurableEquiv.symm_comp_self, comp.left_id]
+    rw [MeasurableEquiv.symm_comp_self, id_comp]
   · change e ∘ f = e ∘ f ∘ e.symm ∘ e
-    rw [MeasurableEquiv.symm_comp_self, comp.right_id]
+    rw [MeasurableEquiv.symm_comp_self, comp_id]
 #align measure_theory.measure_preserving.pre_ergodic_conjugate_iff MeasureTheory.MeasurePreserving.preErgodic_conjugate_iff
 
 theorem ergodic_conjugate_iff {e : α ≃ᵐ β} (h : MeasurePreserving e μ μ') :

diff --git a/Mathlib/Geometry/Manifold/ContMDiff/Defs.lean b/Mathlib/Geometry/Manifold/ContMDiff/Defs.lean
@@ -166,7 +166,7 @@ theorem contDiffWithinAtProp_mono_of_mem (n : ℕ∞) ⦃s x t⦄ ⦃f : H → H
 #align cont_diff_within_at_prop_mono_of_mem contDiffWithinAtProp_mono_of_mem
 
 theorem contDiffWithinAtProp_id (x : H) : ContDiffWithinAtProp I I n id univ x := by
-  simp only [ContDiffWithinAtProp._eq_1, comp.left_id, preimage_univ, univ_inter]
+  simp only [ContDiffWithinAtProp, id_comp, preimage_univ, univ_inter]
   have : ContDiffWithinAt 𝕜 n id (range I) (I x) := contDiff_id.contDiffAt.contDiffWithinAt
   refine this.congr (fun y hy => ?_) ?_
   · simp only [ModelWithCorners.right_inv I hy, mfld_simps]
@@ -362,7 +362,7 @@ theorem contMDiffWithinAt_iff_target :
       and_iff_left_of_imp <| (continuousAt_extChartAt _ _).comp_continuousWithinAt
   simp_rw [cont, ContDiffWithinAtProp, extChartAt, PartialHomeomorph.extend, PartialEquiv.coe_trans,
     ModelWithCorners.toPartialEquiv_coe, PartialHomeomorph.coe_coe, modelWithCornersSelf_coe,
-    chartAt_self_eq, PartialHomeomorph.refl_apply, comp.left_id]
+    chartAt_self_eq, PartialHomeomorph.refl_apply, id_comp]
   rfl
 #align cont_mdiff_within_at_iff_target contMDiffWithinAt_iff_target
 

diff --git a/Mathlib/Geometry/Manifold/SmoothManifoldWithCorners.lean b/Mathlib/Geometry/Manifold/SmoothManifoldWithCorners.lean
@@ -711,7 +711,7 @@ def analyticGroupoid : StructureGroupoid H :=
             (f := (1 : E →L[𝕜] E)) (fun x _ => (1 : E →L[𝕜] E).analyticAt x)
             (fun z hz => (I.right_inv (interior_subset hz)).symm)
         · intro x hx
-          simp only [left_id, comp_apply, preimage_univ, univ_inter, mem_image] at hx
+          simp only [id_comp, comp_apply, preimage_univ, univ_inter, mem_image] at hx
           rcases hx with ⟨y, hy⟩
           rw [← hy.right, I.right_inv (interior_subset hy.left)]
           exact hy.left
@@ -755,7 +755,7 @@ theorem ofSet_mem_analyticGroupoid {s : Set H} (hs : IsOpen s) :
   apply mem_groupoid_of_pregroupoid.mpr
   suffices h : AnalyticOn 𝕜 (I ∘ I.symm) (I.symm ⁻¹' s ∩ interior (range I)) ∧
       (I.symm ⁻¹' s ∩ interior (range I)).image (I ∘ I.symm) ⊆ interior (range I)
-  · simp only [PartialHomeomorph.ofSet_apply, left_id, PartialHomeomorph.ofSet_toPartialEquiv,
+  · simp only [PartialHomeomorph.ofSet_apply, id_comp, PartialHomeomorph.ofSet_toPartialEquiv,
       PartialEquiv.ofSet_source, h, comp_apply, mem_range, image_subset_iff, true_and,
       PartialHomeomorph.ofSet_symm, PartialEquiv.ofSet_target, and_self]
     intro x hx