chore: various naming fixes (#1258)

Mathlib/Data/Set/Basic.lean

@@ -1664,7 +1664,7 @@ alias disjoint_compl_left_iff_subset ↔ _ _root_.HasSubset.Subset.disjoint_comp
 alias disjoint_compl_right_iff_subset ↔ _ _root_.HasSubset.Subset.disjoint_compl_right
 
 theorem subset_union_compl_iff_inter_subset {s t u : Set α} : s ⊆ t ∪ uᶜ ↔ s ∩ u ⊆ t :=
-  (@is_compl_compl _ u _).le_sup_right_iff_inf_left_le
+  (@isCompl_compl _ u _).le_sup_right_iff_inf_left_le
 #align set.subset_union_compl_iff_inter_subset Set.subset_union_compl_iff_inter_subset
 
 theorem compl_subset_iff_union {s t : Set α} : sᶜ ⊆ t ↔ s ∪ t = univ :=

Mathlib/Data/Set/Intervals/OrdConnected.lean

@@ -47,24 +47,24 @@ theorem OrdConnected.out (h : OrdConnected s) : ∀ ⦃x⦄ (_ : x ∈ s) ⦃y
   h.1
 #align set.ord_connected.out Set.OrdConnected.out
 
-theorem OrdConnected_def : OrdConnected s ↔ ∀ ⦃x⦄ (_ : x ∈ s) ⦃y⦄ (_ : y ∈ s), Icc x y ⊆ s :=
+theorem ordConnected_def : OrdConnected s ↔ ∀ ⦃x⦄ (_ : x ∈ s) ⦃y⦄ (_ : y ∈ s), Icc x y ⊆ s :=
   ⟨fun h => h.1, fun h => ⟨h⟩⟩
-#align set.ord_connected_def Set.OrdConnected_def
+#align set.ord_connected_def Set.ordConnected_def
 
 /-- It suffices to prove `[[x, y]] ⊆ s` for `x y ∈ s`, `x ≤ y`. -/
-theorem OrdConnected_iff : OrdConnected s ↔ ∀ x ∈ s, ∀ y ∈ s, x ≤ y → Icc x y ⊆ s :=
-  OrdConnected_def.trans
+theorem ordConnected_iff : OrdConnected s ↔ ∀ x ∈ s, ∀ y ∈ s, x ≤ y → Icc x y ⊆ s :=
+  ordConnected_def.trans
     ⟨fun hs _ hx _ hy _ => hs hx hy, fun H x hx y hy _ hz => H x hx y hy (le_trans hz.1 hz.2) hz⟩
-#align set.ord_connected_iff Set.OrdConnected_iff
+#align set.ord_connected_iff Set.ordConnected_iff
 
-theorem OrdConnected_of_Ioo {α : Type _} [PartialOrder α] {s : Set α}
+theorem ordConnected_of_Ioo {α : Type _} [PartialOrder α] {s : Set α}
     (hs : ∀ x ∈ s, ∀ y ∈ s, x < y → Ioo x y ⊆ s) : OrdConnected s := by
-  rw [OrdConnected_iff]
+  rw [ordConnected_iff]
   intro x hx y hy hxy
   rcases eq_or_lt_of_le hxy with (rfl | hxy'); · simpa
   rw [← Ioc_insert_left hxy, ← Ioo_insert_right hxy']
   exact insert_subset.2 ⟨hx, insert_subset.2 ⟨hy, hs x hx y hy hxy'⟩⟩
-#align set.ord_connected_of_Ioo Set.OrdConnected_of_Ioo
+#align set.ord_connected_of_Ioo Set.ordConnected_of_Ioo
 
 theorem OrdConnected.preimage_mono {f : β → α} (hs : OrdConnected s) (hf : Monotone f) :
     OrdConnected (f ⁻¹' s) :=
@@ -96,97 +96,97 @@ theorem OrdConnected.dual {s : Set α} (hs : OrdConnected s) :
   ⟨fun _ hx _ hy _ hz => hs.out hy hx ⟨hz.2, hz.1⟩⟩
 #align set.ord_connected.dual Set.OrdConnected.dual
 
-theorem OrdConnected_dual {s : Set α} : OrdConnected (OrderDual.ofDual ⁻¹' s) ↔ OrdConnected s :=
-  ⟨fun h => by simpa only [OrdConnected_def] using h.dual, fun h => h.dual⟩
-#align set.ord_connected_dual Set.OrdConnected_dual
+theorem ordConnected_dual {s : Set α} : OrdConnected (OrderDual.ofDual ⁻¹' s) ↔ OrdConnected s :=
+  ⟨fun h => by simpa only [ordConnected_def] using h.dual, fun h => h.dual⟩
+#align set.ord_connected_dual Set.ordConnected_dual
 
-theorem OrdConnected_interₛ {S : Set (Set α)} (hS : ∀ s ∈ S, OrdConnected s) :
+theorem ordConnected_interₛ {S : Set (Set α)} (hS : ∀ s ∈ S, OrdConnected s) :
     OrdConnected (⋂₀ S) :=
   ⟨fun _ hx _ hy => subset_interₛ fun s hs => (hS s hs).out (hx s hs) (hy s hs)⟩
-#align set.ord_connected_sInter Set.OrdConnected_interₛ
+#align set.ord_connected_sInter Set.ordConnected_interₛ
 
-theorem OrdConnected_interᵢ {ι : Sort _} {s : ι → Set α} (hs : ∀ i, OrdConnected (s i)) :
+theorem ordConnected_interᵢ {ι : Sort _} {s : ι → Set α} (hs : ∀ i, OrdConnected (s i)) :
     OrdConnected (⋂ i, s i) :=
-  OrdConnected_interₛ <| forall_range_iff.2 hs
-#align set.ord_connected_Inter Set.OrdConnected_interᵢ
+  ordConnected_interₛ <| forall_range_iff.2 hs
+#align set.ord_connected_Inter Set.ordConnected_interᵢ
 
-instance OrdConnected_interᵢ' {ι : Sort _} {s : ι → Set α} [∀ i, OrdConnected (s i)] :
+instance ordConnected_interᵢ' {ι : Sort _} {s : ι → Set α} [∀ i, OrdConnected (s i)] :
     OrdConnected (⋂ i, s i) :=
-  OrdConnected_interᵢ ‹_›
-#align set.ord_connected_Inter' Set.OrdConnected_interᵢ'
+  ordConnected_interᵢ ‹_›
+#align set.ord_connected_Inter' Set.ordConnected_interᵢ'
 
 /- ./././Mathport/Syntax/Translate/Expr.lean:107:6: warning: expanding binder group (i hi) -/
-theorem OrdConnected_binterᵢ  {ι : Sort _} {p : ι → Prop} {s : ∀ (i : ι) (_ : p i), Set α}
+theorem ordConnected_binterᵢ  {ι : Sort _} {p : ι → Prop} {s : ∀ (i : ι) (_ : p i), Set α}
     (hs : ∀ i hi, OrdConnected (s i hi)) : OrdConnected (⋂ (i) (hi), s i hi) :=
-  OrdConnected_interᵢ fun i => OrdConnected_interᵢ <| hs i
-#align set.ord_connected_bInter Set.OrdConnected_binterᵢ
+  ordConnected_interᵢ fun i => ordConnected_interᵢ <| hs i
+#align set.ord_connected_bInter Set.ordConnected_binterᵢ
 
-theorem OrdConnected_pi {ι : Type _} {α : ι → Type _} [∀ i, Preorder (α i)] {s : Set ι}
+theorem ordConnected_pi {ι : Type _} {α : ι → Type _} [∀ i, Preorder (α i)] {s : Set ι}
     {t : ∀ i, Set (α i)} (h : ∀ i ∈ s, OrdConnected (t i)) : OrdConnected (s.pi t) :=
   ⟨fun _ hx _ hy _ hz i hi => (h i hi).out (hx i hi) (hy i hi) ⟨hz.1 i, hz.2 i⟩⟩
-#align set.ord_connected_pi Set.OrdConnected_pi
+#align set.ord_connected_pi Set.ordConnected_pi
 
-instance OrdConnected_pi' {ι : Type _} {α : ι → Type _} [∀ i, Preorder (α i)] {s : Set ι}
+instance ordConnected_pi' {ι : Type _} {α : ι → Type _} [∀ i, Preorder (α i)] {s : Set ι}
     {t : ∀ i, Set (α i)} [h : ∀ i, OrdConnected (t i)] : OrdConnected (s.pi t) :=
-  OrdConnected_pi fun i _ => h i
-#align set.ord_connected_pi' Set.OrdConnected_pi'
+  ordConnected_pi fun i _ => h i
+#align set.ord_connected_pi' Set.ordConnected_pi'
 
 @[instance]
-theorem OrdConnected_Ici {a : α} : OrdConnected (Ici a) :=
+theorem ordConnected_Ici {a : α} : OrdConnected (Ici a) :=
   ⟨fun _ hx _ _ _ hz => le_trans hx hz.1⟩
-#align set.ord_connected_Ici Set.OrdConnected_Ici
+#align set.ord_connected_Ici Set.ordConnected_Ici
 
 @[instance]
-theorem OrdConnected_Iic {a : α} : OrdConnected (Iic a) :=
+theorem ordConnected_Iic {a : α} : OrdConnected (Iic a) :=
   ⟨fun _ _ _ hy _ hz => le_trans hz.2 hy⟩
-#align set.ord_connected_Iic Set.OrdConnected_Iic
+#align set.ord_connected_Iic Set.ordConnected_Iic
 
 @[instance]
-theorem OrdConnected_Ioi {a : α} : OrdConnected (Ioi a) :=
+theorem ordConnected_Ioi {a : α} : OrdConnected (Ioi a) :=
   ⟨fun _ hx _ _ _ hz => lt_of_lt_of_le hx hz.1⟩
-#align set.ord_connected_Ioi Set.OrdConnected_Ioi
+#align set.ord_connected_Ioi Set.ordConnected_Ioi
 
 @[instance]
-theorem OrdConnected_Iio {a : α} : OrdConnected (Iio a) :=
+theorem ordConnected_Iio {a : α} : OrdConnected (Iio a) :=
   ⟨fun _ _ _ hy _ hz => lt_of_le_of_lt hz.2 hy⟩
-#align set.OrdConnected_Iio Set.OrdConnected_Iio
+#align set.OrdConnected_Iio Set.ordConnected_Iio
 
 @[instance]
-theorem OrdConnected_Icc {a b : α} : OrdConnected (Icc a b) :=
-  OrdConnected_Ici.inter OrdConnected_Iic
-#align set.ord_connected_Icc Set.OrdConnected_Icc
+theorem ordConnected_Icc {a b : α} : OrdConnected (Icc a b) :=
+  ordConnected_Ici.inter ordConnected_Iic
+#align set.ord_connected_Icc Set.ordConnected_Icc
 
 @[instance]
-theorem OrdConnected_Ico {a b : α} : OrdConnected (Ico a b) :=
-  OrdConnected_Ici.inter OrdConnected_Iio
-#align set.ord_connected_Ico Set.OrdConnected_Ico
+theorem ordConnected_Ico {a b : α} : OrdConnected (Ico a b) :=
+  ordConnected_Ici.inter ordConnected_Iio
+#align set.ord_connected_Ico Set.ordConnected_Ico
 
 @[instance]
-theorem OrdConnected_Ioc {a b : α} : OrdConnected (Ioc a b) :=
-  OrdConnected_Ioi.inter OrdConnected_Iic
-#align set.ord_connected_Ioc Set.OrdConnected_Ioc
+theorem ordConnected_Ioc {a b : α} : OrdConnected (Ioc a b) :=
+  ordConnected_Ioi.inter ordConnected_Iic
+#align set.ord_connected_Ioc Set.ordConnected_Ioc
 
 @[instance]
-theorem OrdConnected_Ioo {a b : α} : OrdConnected (Ioo a b) :=
-  OrdConnected_Ioi.inter OrdConnected_Iio
-#align set.ord_connected_Ioo Set.OrdConnected_Ioo
+theorem ordConnected_Ioo {a b : α} : OrdConnected (Ioo a b) :=
+  ordConnected_Ioi.inter ordConnected_Iio
+#align set.ord_connected_Ioo Set.ordConnected_Ioo
 
 @[instance]
-theorem OrdConnected_singleton {α : Type _} [PartialOrder α] {a : α} :
+theorem ordConnected_singleton {α : Type _} [PartialOrder α] {a : α} :
     OrdConnected ({a} : Set α) := by
   rw [← Icc_self]
-  exact OrdConnected_Icc
-#align set.ord_connected_singleton Set.OrdConnected_singleton
+  exact ordConnected_Icc
+#align set.ord_connected_singleton Set.ordConnected_singleton
 
 @[instance]
-theorem OrdConnected_empty : OrdConnected (∅ : Set α) :=
+theorem ordConnected_empty : OrdConnected (∅ : Set α) :=
   ⟨fun _ => False.elim⟩
-#align set.ord_connected_empty Set.OrdConnected_empty
+#align set.ord_connected_empty Set.ordConnected_empty
 
 @[instance]
-theorem OrdConnected_univ : OrdConnected (univ : Set α) :=
+theorem ordConnected_univ : OrdConnected (univ : Set α) :=
   ⟨fun _ _ _ _ => subset_univ _⟩
-#align set.ord_connected_univ Set.OrdConnected_univ
+#align set.ord_connected_univ Set.ordConnected_univ
 
 /-- In a dense order `α`, the subtype from an `OrdConnected` set is also densely ordered. -/
 instance [DenselyOrdered α] {s : Set α} [hs : OrdConnected s] : DenselyOrdered s :=
@@ -195,35 +195,35 @@ instance [DenselyOrdered α] {s : Set α} [hs : OrdConnected s] : DenselyOrdered
     ⟨⟨x, (hs.out a.2 b.2) (Ioo_subset_Icc_self H)⟩, H⟩⟩
 
 @[instance]
-theorem OrdConnected_preimage {F : Type _} [OrderHomClass F α β] (f : F) {s : Set β}
+theorem ordConnected_preimage {F : Type _} [OrderHomClass F α β] (f : F) {s : Set β}
     [hs : OrdConnected s] : OrdConnected (f ⁻¹' s) :=
   ⟨fun _ hx _ hy _ hz => hs.out hx hy ⟨OrderHomClass.mono _ hz.1, OrderHomClass.mono _ hz.2⟩⟩
-#align set.ord_connected_preimage Set.OrdConnected_preimage
+#align set.ord_connected_preimage Set.ordConnected_preimage
 
 @[instance]
-theorem OrdConnected_image {E : Type _} [OrderIsoClass E α β] (e : E) {s : Set α}
+theorem ordConnected_image {E : Type _} [OrderIsoClass E α β] (e : E) {s : Set α}
     [hs : OrdConnected s] : OrdConnected (e '' s) := by
   erw [(e : α ≃o β).image_eq_preimage]
-  apply OrdConnected_preimage (e : α ≃o β).symm
-#align set.ord_connected_image Set.OrdConnected_image
+  apply ordConnected_preimage (e : α ≃o β).symm
+#align set.ord_connected_image Set.ordConnected_image
 
 -- porting note: split up `simp_rw [← image_univ, OrdConnected_image e]`, would not work otherwise
 @[instance]
-theorem OrdConnected_range {E : Type _} [OrderIsoClass E α β] (e : E) : OrdConnected (range e) := by
+theorem ordConnected_range {E : Type _} [OrderIsoClass E α β] (e : E) : OrdConnected (range e) := by
   simp_rw [← image_univ]
-  exact OrdConnected_image (e : α ≃o β)
-#align set.ord_connected_range Set.OrdConnected_range
+  exact ordConnected_image (e : α ≃o β)
+#align set.ord_connected_range Set.ordConnected_range
 
 @[simp]
-theorem dual_OrdConnected_iff {s : Set α} : OrdConnected (ofDual ⁻¹' s) ↔ OrdConnected s := by
-  simp_rw [OrdConnected_def, toDual.surjective.forall, dual_Icc, Subtype.forall']
+theorem dual_ordConnected_iff {s : Set α} : OrdConnected (ofDual ⁻¹' s) ↔ OrdConnected s := by
+  simp_rw [ordConnected_def, toDual.surjective.forall, dual_Icc, Subtype.forall']
   exact forall_swap
-#align set.dual_ord_connected_iff Set.dual_OrdConnected_iff
+#align set.dual_ord_connected_iff Set.dual_ordConnected_iff
 
 @[instance]
-theorem dual_OrdConnected {s : Set α} [OrdConnected s] : OrdConnected (ofDual ⁻¹' s) :=
-  dual_OrdConnected_iff.2 ‹_›
-#align set.dual_ord_connected Set.dual_OrdConnected
+theorem dual_ordConnected {s : Set α} [OrdConnected s] : OrdConnected (ofDual ⁻¹' s) :=
+  dual_ordConnected_iff.2 ‹_›
+#align set.dual_ord_connected Set.dual_ordConnected
 
 end Preorder
 
@@ -232,14 +232,14 @@ section LinearOrder
 variable {α : Type _} [LinearOrder α] {s : Set α} {x : α}
 
 @[instance]
-theorem OrdConnected_interval {a b : α} : OrdConnected [[a, b]] :=
-  OrdConnected_Icc
-#align set.ord_connected_interval Set.OrdConnected_interval
+theorem ordConnected_interval {a b : α} : OrdConnected [[a, b]] :=
+  ordConnected_Icc
+#align set.ord_connected_interval Set.ordConnected_interval
 
 @[instance]
-theorem OrdConnected_interval_oc {a b : α} : OrdConnected (Ι a b) :=
-  OrdConnected_Ioc
-#align set.ord_connected_interval_oc Set.OrdConnected_interval_oc
+theorem ordConnected_interval_oc {a b : α} : OrdConnected (Ι a b) :=
+  ordConnected_Ioc
+#align set.ord_connected_interval_oc Set.ordConnected_interval_oc
 
 theorem OrdConnected.interval_subset (hs : OrdConnected s) ⦃x⦄ (hx : x ∈ s) ⦃y⦄ (hy : y ∈ s) :
     [[x, y]] ⊆ s :=
@@ -251,25 +251,25 @@ theorem OrdConnected.interval_oc_subset (hs : OrdConnected s) ⦃x⦄ (hx : x 
   Ioc_subset_Icc_self.trans <| hs.interval_subset hx hy
 #align set.ord_connected.interval_oc_subset Set.OrdConnected.interval_oc_subset
 
-theorem OrdConnected_iff_interval_subset :
+theorem ordConnected_iff_interval_subset :
     OrdConnected s ↔ ∀ ⦃x⦄ (_ : x ∈ s) ⦃y⦄ (_ : y ∈ s), [[x, y]] ⊆ s :=
   ⟨fun h => h.interval_subset, fun H => ⟨fun _ hx _ hy => Icc_subset_interval.trans <| H hx hy⟩⟩
-#align set.ord_connected_iff_interval_subset Set.OrdConnected_iff_interval_subset
+#align set.ord_connected_iff_interval_subset Set.ordConnected_iff_interval_subset
 
-theorem OrdConnected_of_interval_subset_left (h : ∀ y ∈ s, [[x, y]] ⊆ s) : OrdConnected s :=
-  OrdConnected_iff_interval_subset.2 fun y hy z hz =>
+theorem ordConnected_of_interval_subset_left (h : ∀ y ∈ s, [[x, y]] ⊆ s) : OrdConnected s :=
+  ordConnected_iff_interval_subset.2 fun y hy z hz =>
     calc
       [[y, z]] ⊆ [[y, x]] ∪ [[x, z]] := interval_subset_interval_union_interval
       _ = [[x, y]] ∪ [[x, z]] := by rw [interval_swap]
       _ ⊆ s := union_subset (h y hy) (h z hz)
-#align set.ord_connected_of_interval_subset_left Set.OrdConnected_of_interval_subset_left
+#align set.ord_connected_of_interval_subset_left Set.ordConnected_of_interval_subset_left
 
-theorem OrdConnected_iff_interval_subset_left (hx : x ∈ s) :
+theorem ordConnected_iff_interval_subset_left (hx : x ∈ s) :
     OrdConnected s ↔ ∀ ⦃y⦄, y ∈ s → [[x, y]] ⊆ s :=
-  ⟨fun hs => hs.interval_subset hx, OrdConnected_of_interval_subset_left⟩
-#align set.ord_connected_iff_interval_subset_left Set.OrdConnected_iff_interval_subset_left
+  ⟨fun hs => hs.interval_subset hx, ordConnected_of_interval_subset_left⟩
+#align set.ord_connected_iff_interval_subset_left Set.ordConnected_iff_interval_subset_left
 
-theorem OrdConnected_iff_interval_subset_right (hx : x ∈ s) :
+theorem ordConnected_iff_interval_subset_right (hx : x ∈ s) :
     OrdConnected s ↔ ∀ ⦃y⦄, y ∈ s → [[y, x]] ⊆ s := by
-  simp_rw [OrdConnected_iff_interval_subset_left hx, interval_swap]
-#align set.ord_connected_iff_interval_subset_right Set.OrdConnected_iff_interval_subset_right
+  simp_rw [ordConnected_iff_interval_subset_left hx, interval_swap]
+#align set.ord_connected_iff_interval_subset_right Set.ordConnected_iff_interval_subset_right

Mathlib/Order/BooleanAlgebra.lean

@@ -568,9 +568,9 @@ theorem compl_sup_eq_top : xᶜ ⊔ x = ⊤ :=
   sup_comm.trans sup_compl_eq_top
 #align compl_sup_eq_top compl_sup_eq_top
 
-theorem is_compl_compl : IsCompl x (xᶜ) :=
+theorem isCompl_compl : IsCompl x (xᶜ) :=
   IsCompl.of_eq inf_compl_eq_bot' sup_compl_eq_top
-#align is_compl_compl is_compl_compl
+#align is_compl_compl isCompl_compl
 
 theorem sdiff_eq : x \ y = x ⊓ yᶜ :=
   BooleanAlgebra.sdiff_eq x y
@@ -581,7 +581,7 @@ theorem himp_eq : x ⇨ y = y ⊔ xᶜ :=
 #align himp_eq himp_eq
 
 instance (priority := 100) BooleanAlgebra.toComplementedLattice : ComplementedLattice α :=
-  ⟨fun x => ⟨xᶜ, is_compl_compl⟩⟩
+  ⟨fun x => ⟨xᶜ, isCompl_compl⟩⟩
 #align boolean_algebra.to_complemented_lattice BooleanAlgebra.toComplementedLattice
 
 -- see Note [lower instance priority]
@@ -597,7 +597,7 @@ instance (priority := 100) BooleanAlgebra.toGeneralizedBooleanAlgebra :
 instance (priority := 100) BooleanAlgebra.toBiheytingAlgebra : BiheytingAlgebra α :=
   { ‹BooleanAlgebra α›, GeneralizedBooleanAlgebra.toGeneralizedCoheytingAlgebra with
     hnot := compl,
-    le_himp_iff := fun a b c => by rw [himp_eq, is_compl_compl.le_sup_right_iff_inf_left_le],
+    le_himp_iff := fun a b c => by rw [himp_eq, isCompl_compl.le_sup_right_iff_inf_left_le],
     himp_bot := fun _ => _root_.himp_eq.trans bot_sup_eq,
     top_sdiff := fun a => by rw [sdiff_eq, top_inf_eq]; rfl }
 #align boolean_algebra.to_biheyting_algebra BooleanAlgebra.toBiheytingAlgebra
@@ -615,13 +615,13 @@ theorem top_sdiff : ⊤ \ x = xᶜ :=
 theorem eq_compl_iff_is_compl : x = yᶜ ↔ IsCompl x y :=
   ⟨fun h => by
     rw [h]
-    exact is_compl_compl.symm, IsCompl.eq_compl⟩
+    exact isCompl_compl.symm, IsCompl.eq_compl⟩
 #align eq_compl_iff_is_compl eq_compl_iff_is_compl
 
 theorem compl_eq_iff_is_compl : xᶜ = y ↔ IsCompl x y :=
   ⟨fun h => by
     rw [← h]
-    exact is_compl_compl, IsCompl.compl_eq⟩
+    exact isCompl_compl, IsCompl.compl_eq⟩
 #align compl_eq_iff_is_compl compl_eq_iff_is_compl
 
 theorem compl_eq_comm : xᶜ = y ↔ yᶜ = x := by
@@ -634,7 +634,7 @@ theorem eq_compl_comm : x = yᶜ ↔ y = xᶜ := by
 
 @[simp]
 theorem compl_compl (x : α) : xᶜᶜ = x :=
-  (@is_compl_compl _ x _).symm.compl_eq
+  (@isCompl_compl _ x _).symm.compl_eq
 #align compl_compl compl_compl
 
 theorem compl_comp_compl : compl ∘ compl = @id α :=

Mathlib/Order/Cover.lean

@@ -131,7 +131,7 @@ theorem Set.OrdConnected.apply_wcovby_apply_iff (f : α ↪o β) (h : (range f).
 
 @[simp]
 theorem apply_wcovby_apply_iff {E : Type _} [OrderIsoClass E α β] (e : E) : e a ⩿ e b ↔ a ⩿ b :=
-  (OrdConnected_range (e : α ≃o β)).apply_wcovby_apply_iff ((e : α ≃o β) : α ↪o β)
+  (ordConnected_range (e : α ≃o β)).apply_wcovby_apply_iff ((e : α ≃o β) : α ↪o β)
 #align apply_wcovby_apply_iff apply_wcovby_apply_iff
 
 @[simp]
@@ -352,7 +352,7 @@ theorem Set.OrdConnected.apply_covby_apply_iff (f : α ↪o β) (h : (range f).O
 
 @[simp]
 theorem apply_covby_apply_iff {E : Type _} [OrderIsoClass E α β] (e : E) : e a ⋖ e b ↔ a ⋖ b :=
-  (OrdConnected_range (e : α ≃o β)).apply_covby_apply_iff ((e : α ≃o β) : α ↪o β)
+  (ordConnected_range (e : α ≃o β)).apply_covby_apply_iff ((e : α ≃o β) : α ↪o β)
 #align apply_covby_apply_iff apply_covby_apply_iff
 
 theorem covby_of_eq_or_eq (hab : a < b) (h : ∀ c, a ≤ c → c ≤ b → c = a ∨ c = b) : a ⋖ b :=

Mathlib/Order/ModularLattice.lean

@@ -371,12 +371,12 @@ namespace IsCompl
 variable [Lattice α] [BoundedOrder α] [IsModularLattice α]
 
 /-- The diamond isomorphism between the intervals `set.Iic a` and `set.Ici b`. -/
-def iicOrderIsoIci {a b : α} (h : IsCompl a b) : Set.Iic a ≃o Set.Ici b :=
+def IicOrderIsoIci {a b : α} (h : IsCompl a b) : Set.Iic a ≃o Set.Ici b :=
   (OrderIso.setCongr (Set.Iic a) (Set.Icc (a ⊓ b) a)
         (h.inf_eq_bot.symm ▸ Set.Icc_bot.symm)).trans <|
     (infIccOrderIsoIccSup a b).trans
       (OrderIso.setCongr (Set.Icc b (a ⊔ b)) (Set.Ici b) (h.sup_eq_top.symm ▸ Set.Icc_top))
-#align is_compl.Iic_order_iso_Ici IsCompl.iicOrderIsoIci
+#align is_compl.Iic_order_iso_Ici IsCompl.IicOrderIsoIci
 
 end IsCompl