chore: tidy various files (#3606)

Mathlib/Algebra/Homology/Exact.lean

@@ -45,9 +45,7 @@ these results are found in `CategoryTheory/Abelian/Exact.lean`.
 
 universe v v₂ u u₂
 
-open CategoryTheory
-
-open CategoryTheory.Limits
+open CategoryTheory CategoryTheory.Limits
 
 variable {V : Type u} [Category.{v} V]
 
@@ -56,8 +54,8 @@ variable [HasImages V]
 namespace CategoryTheory
 
 -- One nice feature of this definition is that we have
--- `epi f → exact g h → exact (f ≫ g) h` and `exact f g → mono h → exact f (g ≫ h)`,
--- which do not necessarily hold in a non-abelian category with the usual definition of `exact`.
+-- `Epi f → Exact g h → Exact (f ≫ g) h` and `Exact f g → Mono h → Exact f (g ≫ h)`,
+-- which do not necessarily hold in a non-abelian category with the usual definition of `Exact`.
 /-- Two morphisms `f : A ⟶ B`, `g : B ⟶ C` are called exact if `w : f ≫ g = 0` and the natural map
 `imageToKernel f g w : imageSubobject f ⟶ kernelSubobject g` is an epimorphism.
 
@@ -93,7 +91,8 @@ theorem Preadditive.exact_iff_homology_zero {A B C : V} (f : A ⟶ B) (g : B ⟶
     Exact f g ↔ ∃ w : f ≫ g = 0, Nonempty (homology f g w ≅ 0) :=
   ⟨fun h => ⟨h.w, ⟨by
     haveI := h.epi
-    exact cokernel.ofEpi _⟩⟩, fun h => by
+    exact cokernel.ofEpi _⟩⟩,
+   fun h => by
     obtain ⟨w, ⟨i⟩⟩ := h
     exact ⟨w, Preadditive.epi_of_cokernel_zero ((cancel_mono i.hom).mp (by ext))⟩⟩
 #align category_theory.preadditive.exact_iff_homology_zero CategoryTheory.Preadditive.exact_iff_homology_zero

Mathlib/Algebra/Order/ToIntervalMod.lean

@@ -515,7 +515,7 @@ def MemIooMod (b x : α) : Prop :=
 #align mem_Ioo_mod MemIooMod
 
 open List in
-theorem tFAE_memIooMod :
+theorem tfae_memIooMod :
     TFAE
       [MemIooMod a b x,
       toIcoMod a hb x = toIocMod a hb x,
@@ -538,21 +538,21 @@ theorem tFAE_memIooMod :
     conv_lhs => rw [← toIcoMod_add_toIcoDiv_zsmul a hb x, h]
   · have h' := toIcoMod_mem_Ico a hb x
     exact fun h => ⟨_, h'.1.lt_of_ne' h, h'.2⟩
-#align tfae_mem_Ioo_mod tFAE_memIooMod
+#align tfae_mem_Ioo_mod tfae_memIooMod
 
 variable {a x}
 
 theorem memIooMod_iff_toIcoMod_eq_toIocMod : MemIooMod a b x ↔ toIcoMod a hb x = toIocMod a hb x :=
-  (tFAE_memIooMod a hb x).out 0 1
+  (tfae_memIooMod a hb x).out 0 1
 #align mem_Ioo_mod_iff_to_Ico_mod_eq_to_Ioc_mod memIooMod_iff_toIcoMod_eq_toIocMod
 
 theorem memIooMod_iff_toIcoMod_add_period_ne_toIocMod :
     MemIooMod a b x ↔ toIcoMod a hb x + b ≠ toIocMod a hb x :=
-  (tFAE_memIooMod a hb x).out 0 2
+  (tfae_memIooMod a hb x).out 0 2
 #align mem_Ioo_mod_iff_to_Ico_mod_add_period_ne_to_Ioc_mod memIooMod_iff_toIcoMod_add_period_ne_toIocMod
 
 theorem memIooMod_iff_toIcoMod_ne_left : MemIooMod a b x ↔ toIcoMod a hb x ≠ a :=
-  (tFAE_memIooMod a hb x).out 0 3
+  (tfae_memIooMod a hb x).out 0 3
 #align mem_Ioo_mod_iff_to_Ico_mod_ne_left memIooMod_iff_toIcoMod_ne_left
 
 theorem not_memIooMod_iff_toIcoMod_add_period_eq_toIocMod :

Mathlib/Analysis/Normed/Group/AddTorsor.lean

@@ -58,7 +58,7 @@ instance (priority := 100) SeminormedAddCommGroup.toNormedAddTorsor : NormedAddT
     where dist_eq_norm' := dist_eq_norm
 #align seminormed_add_comm_group.to_normed_add_torsor SeminormedAddCommGroup.toNormedAddTorsor
 
--- Because of the add_torsor.nonempty instance.
+-- Because of the AddTorsor.nonempty instance.
 /-- A nonempty affine subspace of a `NormedAddTorsor` is itself a `NormedAddTorsor`. -/
 instance AffineSubspace.toNormedAddTorsor {R : Type _} [Ring R] [Module R V]
     (s : AffineSubspace R P) [Nonempty s] : NormedAddTorsor s.direction s :=
@@ -176,11 +176,10 @@ def pseudoMetricSpaceOfNormedAddCommGroupOfAddTorsor (V P : Type _) [SeminormedA
     [AddTorsor V P] : PseudoMetricSpace P where
   dist x y := ‖(x -ᵥ y : V)‖
   -- porting note: `edist_dist` is no longer an `autoParam`
-  edist_dist := fun p p' => by simp only [←ENNReal.ofReal_eq_coe_nnreal]
+  edist_dist _ _ := by simp only [←ENNReal.ofReal_eq_coe_nnreal]
   dist_self x := by simp
   dist_comm x y := by simp only [← neg_vsub_eq_vsub_rev y x, norm_neg]
-  dist_triangle := by
-    intro x y z
+  dist_triangle x y z := by
     change ‖x -ᵥ z‖ ≤ ‖x -ᵥ y‖ + ‖y -ᵥ z‖
     rw [← vsub_add_vsub_cancel]
     apply norm_add_le
@@ -192,12 +191,11 @@ P`. -/
 def metricSpaceOfNormedAddCommGroupOfAddTorsor (V P : Type _) [NormedAddCommGroup V]
     [AddTorsor V P] : MetricSpace P where
   dist x y := ‖(x -ᵥ y : V)‖
-  edist_dist := fun p p' => by simp only; rw [ENNReal.ofReal_eq_coe_nnreal]
+  edist_dist _ _ := by simp only; rw [ENNReal.ofReal_eq_coe_nnreal]
   dist_self x := by simp
   eq_of_dist_eq_zero h := by simpa using h
   dist_comm x y := by simp only [← neg_vsub_eq_vsub_rev y x, norm_neg]
-  dist_triangle := by
-    intro x y z
+  dist_triangle x y z := by
     change ‖x -ᵥ z‖ ≤ ‖x -ᵥ y‖ + ‖y -ᵥ z‖
     rw [← vsub_add_vsub_cancel]
     apply norm_add_le
@@ -231,8 +229,8 @@ theorem uniformContinuous_vsub : UniformContinuous fun x : P × P => x.1 -ᵥ x.
   (LipschitzWith.prod_fst.vsub LipschitzWith.prod_snd).uniformContinuous
 #align uniform_continuous_vsub uniformContinuous_vsub
 
-instance (priority := 100) NormedAddTorsor.to_continuousVAdd : ContinuousVAdd V P
-    where continuous_vadd := uniformContinuous_vadd.continuous
+instance (priority := 100) NormedAddTorsor.to_continuousVAdd : ContinuousVAdd V P where
+  continuous_vadd := uniformContinuous_vadd.continuous
 #align normed_add_torsor.to_has_continuous_vadd NormedAddTorsor.to_continuousVAdd
 
 theorem continuous_vsub : Continuous fun x : P × P => x.1 -ᵥ x.2 :=

Mathlib/CategoryTheory/Sites/Sheafification.lean

@@ -403,7 +403,6 @@ theorem exists_of_sep (P : Cᵒᵖ ⥤ D)
           exact hf)
   use e0, 𝟙 _
   ext IV
-  --dsimp only [Meq.refine_apply, Meq.pullback_apply, w]
   let IA : B.Arrow := ⟨_, (IV.f ≫ II.f) ≫ I.f,
     ⟨I.Y, _, _, I.hf, Sieve.downward_closed _ II.hf _, rfl⟩⟩
   let IB : S.Arrow := IA.fromMiddle

Mathlib/Dynamics/Circle/RotationNumber/TranslationNumber.lean

@@ -25,8 +25,8 @@ $$
 exists and does not depend on `x`. This number is called the *translation number* of `f`.
 Different authors use different notation for this number: `τ`, `ρ`, `rot`, etc
 
-In this file we define a structure `circle_deg1_lift` for bundled maps with these properties, define
-translation number of `f : circle_deg1_lift`, prove some estimates relating `f^n(x)-x` to `τ(f)`. In
+In this file we define a structure `CircleDeg1Lift` for bundled maps with these properties, define
+translation number of `f : CircleDeg1Lift`, prove some estimates relating `f^n(x)-x` to `τ(f)`. In
 case of a continuous map `f` we also prove that `f` admits a point `x` such that `f^n(x)=x+m` if and
 only if `τ(f)=m/n`.
 
@@ -41,50 +41,50 @@ It does not depend on the choice of `a`.
 
 ## Main definitions
 
-* `circle_deg1_lift`: a monotone map `f : ℝ → ℝ` such that `f (x + 1) = f x + 1` for all `x`;
-  the type `circle_deg1_lift` is equipped with `lattice` and `monoid` structures; the
+* `CircleDeg1Lift`: a monotone map `f : ℝ → ℝ` such that `f (x + 1) = f x + 1` for all `x`;
+  the type `CircleDeg1Lift` is equipped with `Lattice` and `Monoid` structures; the
   multiplication is given by composition: `(f * g) x = f (g x)`.
-* `circle_deg1_lift.translation_number`: translation number of `f : circle_deg1_lift`.
+* `CircleDeg1Lift.translationNumber`: translation number of `f : CircleDeg1Lift`.
 
 ## Main statements
 
-We prove the following properties of `circle_deg1_lift.translation_number`.
+We prove the following properties of `CircleDeg1Lift.translationNumber`.
 
-* `circle_deg1_lift.translation_number_eq_of_dist_bounded`: if the distance between `(f^n) 0`
+* `CircleDeg1Lift.translationNumber_eq_of_dist_bounded`: if the distance between `(f^n) 0`
   and `(g^n) 0` is bounded from above uniformly in `n : ℕ`, then `f` and `g` have equal
   translation numbers.
 
-* `circle_deg1_lift.translation_number_eq_of_semiconj_by`: if two `circle_deg1_lift` maps `f`, `g`
-  are semiconjugate by a `circle_deg1_lift` map, then `τ f = τ g`.
+* `CircleDeg1Lift.translationNumber_eq_of_semiconjBy`: if two `CircleDeg1Lift` maps `f`, `g`
+  are semiconjugate by a `CircleDeg1Lift` map, then `τ f = τ g`.
 
-* `circle_deg1_lift.translation_number_units_inv`: if `f` is an invertible `circle_deg1_lift` map
+* `CircleDeg1Lift.translationNumber_units_inv`: if `f` is an invertible `CircleDeg1Lift` map
   (equivalently, `f` is a lift of an orientation-preserving circle homeomorphism), then
   the translation number of `f⁻¹` is the negative of the translation number of `f`.
 
-* `circle_deg1_lift.translation_number_mul_of_commute`: if `f` and `g` commute, then
+* `CircleDeg1Lift.translationNumber_mul_of_commute`: if `f` and `g` commute, then
   `τ (f * g) = τ f + τ g`.
 
-* `circle_deg1_lift.translation_number_eq_rat_iff`: the translation number of `f` is equal to
+* `CircleDeg1Lift.translationNumber_eq_rat_iff`: the translation number of `f` is equal to
   a rational number `m / n` if and only if `(f^n) x = x + m` for some `x`.
 
-* `circle_deg1_lift.semiconj_of_bijective_of_translation_number_eq`: if `f` and `g` are two
-  bijective `circle_deg1_lift` maps and their translation numbers are equal, then these
+* `CircleDeg1Lift.semiconj_of_bijective_of_translationNumber_eq`: if `f` and `g` are two
+  bijective `CircleDeg1Lift` maps and their translation numbers are equal, then these
   maps are semiconjugate to each other.
 
-* `circle_deg1_lift.semiconj_of_group_action_of_forall_translation_number_eq`: let `f₁` and `f₂` be
+* `CircleDeg1Lift.semiconj_of_group_action_of_forall_translationNumber_eq`: let `f₁` and `f₂` be
   two actions of a group `G` on the circle by degree 1 maps (formally, `f₁` and `f₂` are two
-  homomorphisms from `G →* circle_deg1_lift`). If the translation numbers of `f₁ g` and `f₂ g` are
+  homomorphisms from `G →* CircleDeg1Lift`). If the translation numbers of `f₁ g` and `f₂ g` are
   equal to each other for all `g : G`, then these two actions are semiconjugate by some `F :
-  circle_deg1_lift`. This is a version of Proposition 5.4 from [Étienne Ghys, Groupes
+  CircleDeg1Lift`. This is a version of Proposition 5.4 from [Étienne Ghys, Groupes
   d'homeomorphismes du cercle et cohomologie bornee][ghys87:groupes].
 
 ## Notation
 
-We use a local notation `τ` for the translation number of `f : circle_deg1_lift`.
+We use a local notation `τ` for the translation number of `f : CircleDeg1Lift`.
 
 ## Implementation notes
 
-We define the translation number of `f : circle_deg1_lift` to be the limit of the sequence
+We define the translation number of `f : CircleDeg1Lift` to be the limit of the sequence
 `(f ^ (2 ^ n)) 0 / (2 ^ n)`, then prove that `((f ^ n) x - x) / n` tends to this number for any `x`.
 This way it is much easier to prove that the limit exists and basic properties of the limit.
 
@@ -104,17 +104,17 @@ preserving circle homeomorphisms for two reasons:
 
 Here are some short-term goals.
 
-* Introduce a structure or a typeclass for lifts of circle homeomorphisms. We use `units
-  circle_deg1_lift` for now, but it's better to have a dedicated type (or a typeclass?).
+* Introduce a structure or a typeclass for lifts of circle homeomorphisms. We use `Units
+  CircleDeg1Lift` for now, but it's better to have a dedicated type (or a typeclass?).
 
-* Prove that the `semiconj_by` relation on circle homeomorphisms is an equivalence relation.
+* Prove that the `SemiconjBy` relation on circle homeomorphisms is an equivalence relation.
 
-* Introduce `conditionally_complete_lattice` structure, use it in the proof of
-  `circle_deg1_lift.semiconj_of_group_action_of_forall_translation_number_eq`.
+* Introduce `ConditionallyCompleteLattice` structure, use it in the proof of
+  `CircleDeg1Lift.semiconj_of_group_action_of_forall_translationNumber_eq`.
 
 * Prove that the orbits of the irrational rotation are dense in the circle. Deduce that a
   homeomorphism with an irrational rotation is semiconjugate to the corresponding irrational
-  translation by a continuous `circle_deg1_lift`.
+  translation by a continuous `CircleDeg1Lift`.
 
 ## Tags
 
@@ -283,9 +283,9 @@ theorem commute_iff_commute {f g : CircleDeg1Lift} : Commute f g ↔ Function.Co
 -/
 
 
-/-- The map `y ↦ x + y` as a `circle_deg1_lift`. More precisely, we define a homomorphism from
-`multiplicative ℝ` to `circle_deg1_liftˣ`, so the translation by `x` is
-`translation (multiplicative.of_add x)`. -/
+/-- The map `y ↦ x + y` as a `CircleDeg1Lift`. More precisely, we define a homomorphism from
+`Multiplicative ℝ` to `CircleDeg1Liftˣ`, so the translation by `x` is
+`translation (Multiplicative.ofAdd x)`. -/
 def translate : Multiplicative ℝ →* CircleDeg1Liftˣ := MonoidHom.toHomUnits <|
   { toFun := fun x =>
       ⟨⟨fun y => Multiplicative.toAdd x + y, fun _ _ h => add_le_add_left h _⟩, fun _ =>
@@ -327,7 +327,7 @@ theorem translate_iterate (x : ℝ) (n : ℕ) :
 
 In this section we prove that `f` commutes with translations by an integer number.
 First we formulate these statements (for a natural or an integer number,
-addition on the left or on the right, addition or subtraction) using `function.commute`,
+addition on the left or on the right, addition or subtraction) using `Function.Commute`,
 then reformulate as `simp` lemmas `map_int_add` etc.
 -/
 
@@ -406,7 +406,7 @@ noncomputable instance : Lattice CircleDeg1Lift where
   sup f g :=
     { toFun := fun x => max (f x) (g x)
       monotone' := fun x y h => max_le_max (f.mono h) (g.mono h)
-      -- TODO: generalize to `monotone.max`
+      -- TODO: generalize to `Monotone.max`
       map_add_one' := fun x => by simp [max_add_add_right] }
   le f g := ∀ x, f x ≤ g x
   le_refl f x := le_refl (f x)
@@ -630,7 +630,7 @@ def transnumAuxSeq (n : ℕ) : ℝ :=
   (f ^ (2 ^ n : ℕ)) 0 / 2 ^ n
 #align circle_deg1_lift.transnum_aux_seq CircleDeg1Lift.transnumAuxSeq
 
-/-- The translation number of a `circle_deg1_lift`, $τ(f)=\lim_{n→∞}\frac{f^n(x)-x}{n}$. We use
+/-- The translation number of a `CircleDeg1Lift`, $τ(f)=\lim_{n→∞}\frac{f^n(x)-x}{n}$. We use
 an auxiliary sequence `\frac{f^{2^n}(0)}{2^n}` to define `τ(f)` because some proofs are simpler
 this way. -/
 def translationNumber : ℝ :=
@@ -640,7 +640,7 @@ def translationNumber : ℝ :=
 end
 
 -- mathport name: exprτ
--- TODO: choose two different symbols for `circle_deg1_lift.translation_number` and the future
+-- TODO: choose two different symbols for `CircleDeg1Lift.translationNumber` and the future
 -- `circle_mono_homeo.rotation_number`, then make them `localized notation`s
 local notation "τ" => translationNumber
 
@@ -960,9 +960,9 @@ theorem translationNumber_eq_rat_iff (hf : Continuous f) {m : ℤ} {n : ℕ} (hn
   exact (f ^ n).translationNumber_eq_int_iff (f.continuous_pow hf n)
 #align circle_deg1_lift.translation_number_eq_rat_iff CircleDeg1Lift.translationNumber_eq_rat_iff
 
-/-- Consider two actions `f₁ f₂ : G →* circle_deg1_lift` of a group on the real line by lifts of
+/-- Consider two actions `f₁ f₂ : G →* CircleDeg1Lift` of a group on the real line by lifts of
 orientation preserving circle homeomorphisms. Suppose that for each `g : G` the homeomorphisms
-`f₁ g` and `f₂ g` have equal rotation numbers. Then there exists `F : circle_deg1_lift`  such that
+`f₁ g` and `f₂ g` have equal rotation numbers. Then there exists `F : CircleDeg1Lift`  such that
 `F * f₁ g = f₂ g * F` for all `g : G`.
 
 This is a version of Proposition 5.4 from [Étienne Ghys, Groupes d'homeomorphismes du cercle et
@@ -985,7 +985,7 @@ theorem semiconj_of_group_action_of_forall_translationNumber_eq {G : Type _} [Gr
       _ ≤ x + τ (f₂ g) + τ (f₂ g⁻¹) + 1 + 1 :=
         add_le_add_right (map_lt_add_translationNumber_add_one _ _).le _
       _ = x + 2 := by simp [this, add_assoc, one_add_one_eq_two]
-  -- We have a theorem about actions by `order_iso`, so we introduce auxiliary maps
+  -- We have a theorem about actions by `OrderIso`, so we introduce auxiliary maps
   -- to `ℝ ≃o ℝ`.
   set F₁ := toOrderIso.comp f₁.toHomUnits
   set F₂ := toOrderIso.comp f₂.toHomUnits
@@ -1002,7 +1002,7 @@ theorem semiconj_of_group_action_of_forall_translationNumber_eq {G : Type _} [Gr
 #align circle_deg1_lift.semiconj_of_group_action_of_forall_translation_number_eq CircleDeg1Lift.semiconj_of_group_action_of_forall_translationNumber_eq
 
 /-- If two lifts of circle homeomorphisms have the same translation number, then they are
-semiconjugate by a `circle_deg1_lift`. This version uses arguments `f₁ f₂ : circle_deg1_liftˣ`
+semiconjugate by a `CircleDeg1Lift`. This version uses arguments `f₁ f₂ : CircleDeg1Liftˣ`
 to assume that `f₁` and `f₂` are homeomorphisms. -/
 theorem units_semiconj_of_translationNumber_eq {f₁ f₂ : CircleDeg1Liftˣ} (h : τ f₁ = τ f₂) :
     ∃ F : CircleDeg1Lift, Semiconj F f₁ f₂ :=
@@ -1015,7 +1015,7 @@ theorem units_semiconj_of_translationNumber_eq {f₁ f₂ : CircleDeg1Liftˣ} (h
 #align circle_deg1_lift.units_semiconj_of_translation_number_eq CircleDeg1Lift.units_semiconj_of_translationNumber_eq
 
 /-- If two lifts of circle homeomorphisms have the same translation number, then they are
-semiconjugate by a `circle_deg1_lift`. This version uses assumptions `is_unit f₁` and `is_unit f₂`
+semiconjugate by a `CircleDeg1Lift`. This version uses assumptions `IsUnit f₁` and `IsUnit f₂`
 to assume that `f₁` and `f₂` are homeomorphisms. -/
 theorem semiconj_of_isUnit_of_translationNumber_eq {f₁ f₂ : CircleDeg1Lift} (h₁ : IsUnit f₁)
     (h₂ : IsUnit f₂) (h : τ f₁ = τ f₂) : ∃ F : CircleDeg1Lift, Semiconj F f₁ f₂ := by
@@ -1024,7 +1024,7 @@ theorem semiconj_of_isUnit_of_translationNumber_eq {f₁ f₂ : CircleDeg1Lift}
 #align circle_deg1_lift.semiconj_of_is_unit_of_translation_number_eq CircleDeg1Lift.semiconj_of_isUnit_of_translationNumber_eq
 
 /-- If two lifts of circle homeomorphisms have the same translation number, then they are
-semiconjugate by a `circle_deg1_lift`. This version uses assumptions `bijective f₁` and
+semiconjugate by a `CircleDeg1Lift`. This version uses assumptions `bijective f₁` and
 `bijective f₂` to assume that `f₁` and `f₂` are homeomorphisms. -/
 theorem semiconj_of_bijective_of_translationNumber_eq {f₁ f₂ : CircleDeg1Lift} (h₁ : Bijective f₁)
     (h₂ : Bijective f₂) (h : τ f₁ = τ f₂) : ∃ F : CircleDeg1Lift, Semiconj F f₁ f₂ :=

Mathlib/Geometry/Manifold/ChartedSpace.lean

@@ -115,9 +115,7 @@ composition of local equivs with `≫`.
 
 noncomputable section
 
-open Classical Topology
-
-open Filter
+open Classical Topology Filter
 
 universe u
 
@@ -402,10 +400,10 @@ class ClosedUnderRestriction (G : StructureGroupoid H) : Prop where
     ∀ {e : LocalHomeomorph H H}, e ∈ G → ∀ s : Set H, IsOpen s → e.restr s ∈ G
 #align closed_under_restriction ClosedUnderRestriction
 
-theorem closed_under_restriction' {G : StructureGroupoid H} [ClosedUnderRestriction G]
+theorem closedUnderRestriction' {G : StructureGroupoid H} [ClosedUnderRestriction G]
     {e : LocalHomeomorph H H} (he : e ∈ G) {s : Set H} (hs : IsOpen s) : e.restr s ∈ G :=
   ClosedUnderRestriction.closedUnderRestriction he s hs
-#align closed_under_restriction' closed_under_restriction'
+#align closed_under_restriction' closedUnderRestriction'
 
 /-- The trivial restriction-closed groupoid, containing only local homeomorphisms equivalent to the
 restriction of the identity to the various open subsets. -/
@@ -460,7 +458,7 @@ theorem closedUnderRestriction_iff_id_le (G : StructureGroupoid H) :
     apply StructureGroupoid.le_iff.mpr
     rintro e ⟨s, hs, hes⟩
     refine' G.eq_on_source _ hes
-    convert closed_under_restriction' G.id_mem hs
+    convert closedUnderRestriction' G.id_mem hs
     -- Porting note: was
     -- change s = _ ∩ _
     -- rw [hs.interior_eq]
@@ -1073,7 +1071,7 @@ instance [ClosedUnderRestriction G] : HasGroupoid s G where
     rw [hc'.symm, mem_singleton_iff] at he'
     rw [he, he']
     refine' G.eq_on_source _ (subtypeRestr_symm_trans_subtypeRestr s (chartAt x) (chartAt x'))
-    apply closed_under_restriction'
+    apply closedUnderRestriction'
     · exact G.compatible (chart_mem_atlas _) (chart_mem_atlas _)
     · exact preimage_open_of_open_symm (chartAt _) s.2