remove #align from remaining files

Mathlib/GroupTheory/Schreier.lean

@@ -56,7 +56,6 @@ theorem closure_mul_image_mul_eq_top
       (mul_inv_toFun_mem hR (f (r * s⁻¹) * s))
     rw [mul_assoc, ← inv_inv s, ← mul_inv_rev, inv_inv]
     exact toFun_mul_inv_mem hR (r * s⁻¹)
-#align subgroup.closure_mul_image_mul_eq_top Subgroup.closure_mul_image_mul_eq_top
 
 /-- **Schreier's Lemma**: If `R : Set G` is a `rightTransversal of` `H : Subgroup G`
   with `1 ∈ R`, and if `G` is generated by `S : Set G`, then `H` is generated by the `Set`
@@ -77,7 +76,6 @@ theorem closure_mul_image_eq (hR : R ∈ rightTransversals (H : Set G)) (hR1 : (
     exact H.one_mem
   · rw [Subtype.coe_mk, inv_one, mul_one]
     exact (H.mul_mem_cancel_left (hU hg)).mp hh
-#align subgroup.closure_mul_image_eq Subgroup.closure_mul_image_eq
 
 /-- **Schreier's Lemma**: If `R : Set G` is a `rightTransversal` of `H : Subgroup G`
   with `1 ∈ R`, and if `G` is generated by `S : Set G`, then `H` is generated by the `Set`
@@ -87,7 +85,6 @@ theorem closure_mul_image_eq_top (hR : R ∈ rightTransversals (H : Set G)) (hR1
       ⟨g * (toFun hR g : G)⁻¹, mul_inv_toFun_mem hR g⟩ : Set H) = ⊤ := by
   rw [eq_top_iff, ← map_subtype_le_map_subtype, MonoidHom.map_closure, Set.image_image]
   exact (map_subtype_le ⊤).trans (ge_of_eq (closure_mul_image_eq hR hR1 hS))
-#align subgroup.closure_mul_image_eq_top Subgroup.closure_mul_image_eq_top
 
 /-- **Schreier's Lemma**: If `R : Finset G` is a `rightTransversal` of `H : Subgroup G`
   with `1 ∈ R`, and if `G` is generated by `S : Finset G`, then `H` is generated by the `Finset`
@@ -98,7 +95,6 @@ theorem closure_mul_image_eq_top' [DecidableEq G] {R S : Finset G}
     closure (((R * S).image fun g => ⟨_, mul_inv_toFun_mem hR g⟩ : Finset H) : Set H) = ⊤ := by
   rw [Finset.coe_image, Finset.coe_mul]
   exact closure_mul_image_eq_top hR hR1 hS
-#align subgroup.closure_mul_image_eq_top' Subgroup.closure_mul_image_eq_top'
 
 variable (H)
 
@@ -122,15 +118,13 @@ theorem exists_finset_card_le_mul [FiniteIndex H] {S : Finset G} (hS : closure (
     _ = _ := (Fintype.card_congr (toEquiv hR)).symm
     _ = Fintype.card (G ⧸ H) := (QuotientGroup.card_quotient_rightRel H)
     _ = H.index := H.index_eq_card.symm
-#align subgroup.exists_finset_card_le_mul Subgroup.exists_finset_card_le_mul
 
 /-- **Schreier's Lemma**: A finite index subgroup of a finitely generated
   group is finitely generated. -/
 instance fg_of_index_ne_zero [hG : Group.FG G] [FiniteIndex H] : Group.FG H := by
   obtain ⟨S, hS⟩ := hG.1
   obtain ⟨T, -, hT⟩ := exists_finset_card_le_mul H hS
   exact ⟨⟨T, hT⟩⟩
-#align subgroup.fg_of_index_ne_zero Subgroup.fg_of_index_ne_zero
 
 theorem rank_le_index_mul_rank [hG : Group.FG G] [FiniteIndex H] :
     Group.rank H ≤ H.index * Group.rank G := by
@@ -141,7 +135,6 @@ theorem rank_le_index_mul_rank [hG : Group.FG G] [FiniteIndex H] :
     Group.rank H ≤ T.card := Group.rank_le H hT
     _ ≤ H.index * S.card := hT₀
     _ = H.index * Group.rank G := congr_arg ((· * ·) H.index) hS₀
-#align subgroup.rank_le_index_mul_rank Subgroup.rank_le_index_mul_rank
 
 variable (G)
 
@@ -176,12 +169,10 @@ theorem card_commutator_dvd_index_center_pow [Finite (commutatorSet G)] :
   have := Abelianization.commutator_subset_ker (MonoidHom.transferCenterPow G) g.1.2
   -- `transfer g` is defeq to `g ^ [G : Z(G)]`, so we are done
   simpa only [MonoidHom.mem_ker, Subtype.ext_iff] using this
-#align subgroup.card_commutator_dvd_index_center_pow Subgroup.card_commutator_dvd_index_center_pow
 
 /-- A bound for the size of the commutator subgroup in terms of the number of commutators. -/
 def cardCommutatorBound (n : ℕ) :=
   (n ^ (2 * n)) ^ (n ^ (2 * n + 1) + 1)
-#align subgroup.card_commutator_bound Subgroup.cardCommutatorBound
 
 /-- A theorem of Schur: The size of the commutator subgroup is bounded in terms of the number of
   commutators. -/
@@ -198,7 +189,6 @@ theorem card_commutator_le_of_finite_commutatorSet [Finite (commutatorSet G)] :
   rw [← pow_succ'] at h2
   refine' (Nat.le_of_dvd _ h2).trans (Nat.pow_le_pow_of_le_left h1 _)
   exact pow_pos (Nat.pos_of_ne_zero FiniteIndex.finiteIndex) _
-#align subgroup.card_commutator_le_of_finite_commutator_set Subgroup.card_commutator_le_of_finite_commutatorSet
 
 /-- A theorem of Schur: A group with finitely many commutators has finite commutator subgroup. -/
 instance [Finite (commutatorSet G)] : Finite (_root_.commutator G) := by

Mathlib/Topology/Connected/LocallyConnected.lean

@@ -30,13 +30,11 @@ equivalence later in `locallyConnectedSpace_iff_connected_basis`. -/
 class LocallyConnectedSpace (α : Type*) [TopologicalSpace α] : Prop where
   /-- Open connected neighborhoods form a basis of the neighborhoods filter. -/
   open_connected_basis : ∀ x, (𝓝 x).HasBasis (fun s : Set α => IsOpen s ∧ x ∈ s ∧ IsConnected s) id
-#align locally_connected_space LocallyConnectedSpace
 
 theorem locallyConnectedSpace_iff_open_connected_basis :
     LocallyConnectedSpace α ↔
       ∀ x, (𝓝 x).HasBasis (fun s : Set α => IsOpen s ∧ x ∈ s ∧ IsConnected s) id :=
   ⟨@LocallyConnectedSpace.open_connected_basis _ _, LocallyConnectedSpace.mk⟩
-#align locally_connected_space_iff_open_connected_basis locallyConnectedSpace_iff_open_connected_basis
 
 theorem locallyConnectedSpace_iff_open_connected_subsets :
     LocallyConnectedSpace α ↔
@@ -50,41 +48,35 @@ theorem locallyConnectedSpace_iff_open_connected_subsets :
   · exact fun h => ⟨fun U => ⟨fun hU =>
       let ⟨V, hVU, hV⟩ := h U hU
       ⟨V, hV, hVU⟩, fun ⟨V, ⟨hV, hxV, _⟩, hVU⟩ => mem_nhds_iff.mpr ⟨V, hVU, hV, hxV⟩⟩⟩
-#align locally_connected_space_iff_open_connected_subsets locallyConnectedSpace_iff_open_connected_subsets
 
 /-- A space with discrete topology is a locally connected space. -/
 instance (priority := 100) DiscreteTopology.toLocallyConnectedSpace (α) [TopologicalSpace α]
     [DiscreteTopology α] : LocallyConnectedSpace α :=
   locallyConnectedSpace_iff_open_connected_subsets.2 fun x _U hU =>
     ⟨{x}, singleton_subset_iff.2 <| mem_of_mem_nhds hU, isOpen_discrete _, rfl,
       isConnected_singleton⟩
-#align discrete_topology.to_locally_connected_space DiscreteTopology.toLocallyConnectedSpace
 
 theorem connectedComponentIn_mem_nhds [LocallyConnectedSpace α] {F : Set α} {x : α} (h : F ∈ 𝓝 x) :
     connectedComponentIn F x ∈ 𝓝 x := by
   rw [(LocallyConnectedSpace.open_connected_basis x).mem_iff] at h
   rcases h with ⟨s, ⟨h1s, hxs, h2s⟩, hsF⟩
   exact mem_nhds_iff.mpr ⟨s, h2s.isPreconnected.subset_connectedComponentIn hxs hsF, h1s, hxs⟩
-#align connected_component_in_mem_nhds connectedComponentIn_mem_nhds
 
 protected theorem IsOpen.connectedComponentIn [LocallyConnectedSpace α] {F : Set α} {x : α}
     (hF : IsOpen F) : IsOpen (connectedComponentIn F x) := by
   rw [isOpen_iff_mem_nhds]
   intro y hy
   rw [connectedComponentIn_eq hy]
   exact connectedComponentIn_mem_nhds (hF.mem_nhds <| connectedComponentIn_subset F x hy)
-#align is_open.connected_component_in IsOpen.connectedComponentIn
 
 theorem isOpen_connectedComponent [LocallyConnectedSpace α] {x : α} :
     IsOpen (connectedComponent x) := by
   rw [← connectedComponentIn_univ]
   exact isOpen_univ.connectedComponentIn
-#align is_open_connected_component isOpen_connectedComponent
 
 theorem isClopen_connectedComponent [LocallyConnectedSpace α] {x : α} :
     IsClopen (connectedComponent x) :=
   ⟨isOpen_connectedComponent, isClosed_connectedComponent⟩
-#align is_clopen_connected_component isClopen_connectedComponent
 
 theorem locallyConnectedSpace_iff_connectedComponentIn_open :
     LocallyConnectedSpace α ↔
@@ -99,7 +91,6 @@ theorem locallyConnectedSpace_iff_connectedComponentIn_open :
           (connectedComponentIn_subset _ _).trans interior_subset, h _ isOpen_interior x _,
           mem_connectedComponentIn _, isConnected_connectedComponentIn_iff.mpr _⟩ <;>
       exact mem_interior_iff_mem_nhds.mpr hU
-#align locally_connected_space_iff_connected_component_in_open locallyConnectedSpace_iff_connectedComponentIn_open
 
 theorem locallyConnectedSpace_iff_connected_subsets :
     LocallyConnectedSpace α ↔ ∀ (x : α), ∀ U ∈ 𝓝 x, ∃ V ∈ 𝓝 x, IsPreconnected V ∧ V ⊆ U := by
@@ -113,14 +104,12 @@ theorem locallyConnectedSpace_iff_connected_subsets :
     rw [connectedComponentIn_eq hy]
     rcases h y U (hU.mem_nhds <| (connectedComponentIn_subset _ _) hy) with ⟨V, hVy, hV, hVU⟩
     exact Filter.mem_of_superset hVy (hV.subset_connectedComponentIn (mem_of_mem_nhds hVy) hVU)
-#align locally_connected_space_iff_connected_subsets locallyConnectedSpace_iff_connected_subsets
 
 theorem locallyConnectedSpace_iff_connected_basis :
     LocallyConnectedSpace α ↔
       ∀ x, (𝓝 x).HasBasis (fun s : Set α => s ∈ 𝓝 x ∧ IsPreconnected s) id := by
   rw [locallyConnectedSpace_iff_connected_subsets]
   exact forall_congr' <| fun x => Filter.hasBasis_self.symm
-#align locally_connected_space_iff_connected_basis locallyConnectedSpace_iff_connected_basis
 
 theorem locallyConnectedSpace_of_connected_bases {ι : Type*} (b : α → ι → Set α) (p : α → ι → Prop)
     (hbasis : ∀ x, (𝓝 x).HasBasis (p x) (b x))
@@ -130,7 +119,6 @@ theorem locallyConnectedSpace_of_connected_bases {ι : Type*} (b : α → ι →
     (hbasis x).to_hasBasis
       (fun i hi => ⟨b x i, ⟨(hbasis x).mem_of_mem hi, hconnected x i hi⟩, subset_rfl⟩) fun s hs =>
       ⟨(hbasis x).index s hs.1, ⟨(hbasis x).property_index hs.1, (hbasis x).set_index_subset hs.1⟩⟩
-#align locally_connected_space_of_connected_bases locallyConnectedSpace_of_connected_bases
 
 theorem OpenEmbedding.locallyConnectedSpace [LocallyConnectedSpace α] [TopologicalSpace β]
     {f : β → α} (h : OpenEmbedding f) : LocallyConnectedSpace β := by