chore(Covby): rename Covby to CovBy (#9578)

Rename

- `Covby` → `CovBy`, `Wcovby` → `WCovBy`
- `*covby*` → `*covBy*`
- `wcovby.finset_val` → `WCovBy.finset_val`, `wcovby.finset_coe` → `WCovBy.finset_coe`
- `Covby.is_coatom` → `CovBy.isCoatom`

Mathlib/Algebra/Function/Support.lean

@@ -138,7 +138,7 @@ theorem range_subset_insert_image_mulSupport (f : α → M) :
 @[to_additive]
 lemma range_eq_image_or_of_mulSupport_subset {f : α → M} {k : Set α} (h : mulSupport f ⊆ k) :
     range f = f '' k ∨ range f = insert 1 (f '' k) := by
-  apply (wcovby_insert _ _).eq_or_eq (image_subset_range _ _)
+  apply (wcovBy_insert _ _).eq_or_eq (image_subset_range _ _)
   exact (range_subset_insert_image_mulSupport f).trans (insert_subset_insert (image_subset f h))
 
 @[to_additive (attr := simp)]

Mathlib/Algebra/Order/ToIntervalMod.lean

@@ -690,23 +690,23 @@ theorem Ico_eq_locus_Ioc_eq_iUnion_Ioo :
     Classical.not_not]
 #align Ico_eq_locus_Ioc_eq_Union_Ioo Ico_eq_locus_Ioc_eq_iUnion_Ioo
 
-theorem toIocDiv_wcovby_toIcoDiv (a b : α) : toIocDiv hp a b ⩿ toIcoDiv hp a b := by
+theorem toIocDiv_wcovBy_toIcoDiv (a b : α) : toIocDiv hp a b ⩿ toIcoDiv hp a b := by
   suffices toIocDiv hp a b = toIcoDiv hp a b ∨ toIocDiv hp a b + 1 = toIcoDiv hp a b by
-    rwa [wcovby_iff_eq_or_covby, ← Order.succ_eq_iff_covby]
+    rwa [wcovBy_iff_eq_or_covBy, ← Order.succ_eq_iff_covBy]
   rw [eq_comm, ← not_modEq_iff_toIcoDiv_eq_toIocDiv, eq_comm, ←
     modEq_iff_toIcoDiv_eq_toIocDiv_add_one]
   exact em' _
-#align to_Ioc_div_wcovby_to_Ico_div toIocDiv_wcovby_toIcoDiv
+#align to_Ioc_div_wcovby_to_Ico_div toIocDiv_wcovBy_toIcoDiv
 
 theorem toIcoMod_le_toIocMod (a b : α) : toIcoMod hp a b ≤ toIocMod hp a b := by
   rw [toIcoMod, toIocMod, sub_le_sub_iff_left]
-  exact zsmul_mono_left hp.le (toIocDiv_wcovby_toIcoDiv _ _ _).le
+  exact zsmul_mono_left hp.le (toIocDiv_wcovBy_toIcoDiv _ _ _).le
 #align to_Ico_mod_le_to_Ioc_mod toIcoMod_le_toIocMod
 
 theorem toIocMod_le_toIcoMod_add (a b : α) : toIocMod hp a b ≤ toIcoMod hp a b + p := by
   rw [toIcoMod, toIocMod, sub_add, sub_le_sub_iff_left, sub_le_iff_le_add, ← add_one_zsmul,
     (zsmul_strictMono_left hp).le_iff_le]
-  apply (toIocDiv_wcovby_toIcoDiv _ _ _).le_succ
+  apply (toIocDiv_wcovBy_toIcoDiv _ _ _).le_succ
 #align to_Ioc_mod_le_to_Ico_mod_add toIocMod_le_toIcoMod_add
 
 end IcoIoc

Mathlib/Combinatorics/SetFamily/Shadow.lean

@@ -101,12 +101,12 @@ theorem erase_mem_shadow (hs : s ∈ 𝒜) (ha : a ∈ s) : erase s a ∈ ∂ 
 
 See also `Finset.mem_shadow_iff_exists_mem_card_add_one`. -/
 lemma mem_shadow_iff_exists_sdiff : t ∈ ∂ 𝒜 ↔ ∃ s ∈ 𝒜, t ⊆ s ∧ (s \ t).card = 1 := by
-  simp_rw [mem_shadow_iff, ← covby_iff_card_sdiff_eq_one, covby_iff_exists_erase]
+  simp_rw [mem_shadow_iff, ← covBy_iff_card_sdiff_eq_one, covBy_iff_exists_erase]
 
 /-- `t` is in the shadow of `𝒜` iff we can add an element to it so that the resulting finset is in
 `𝒜`. -/
 lemma mem_shadow_iff_insert_mem : t ∈ ∂ 𝒜 ↔ ∃ a, a ∉ t ∧ insert a t ∈ 𝒜 := by
-  simp_rw [mem_shadow_iff_exists_sdiff, ← covby_iff_card_sdiff_eq_one, covby_iff_exists_insert]
+  simp_rw [mem_shadow_iff_exists_sdiff, ← covBy_iff_card_sdiff_eq_one, covBy_iff_exists_insert]
   aesop
 #align finset.mem_shadow_iff_insert_mem Finset.mem_shadow_iff_insert_mem
 
@@ -223,12 +223,12 @@ theorem insert_mem_upShadow (hs : s ∈ 𝒜) (ha : a ∉ s) : insert a s ∈ 
 
 See also `Finset.mem_upShadow_iff_exists_mem_card_add_one`. -/
 lemma mem_upShadow_iff_exists_sdiff : t ∈ ∂⁺ 𝒜 ↔ ∃ s ∈ 𝒜, s ⊆ t ∧ (t \ s).card = 1 := by
-  simp_rw [mem_upShadow_iff, ← covby_iff_card_sdiff_eq_one, covby_iff_exists_insert]
+  simp_rw [mem_upShadow_iff, ← covBy_iff_card_sdiff_eq_one, covBy_iff_exists_insert]
 
 /-- `t` is in the upper shadow of `𝒜` iff we can remove an element from it so that the resulting
 finset is in `𝒜`. -/
 lemma mem_upShadow_iff_erase_mem : t ∈ ∂⁺ 𝒜 ↔ ∃ a, a ∈ t ∧ erase t a ∈ 𝒜 := by
-  simp_rw [mem_upShadow_iff_exists_sdiff, ← covby_iff_card_sdiff_eq_one, covby_iff_exists_erase]
+  simp_rw [mem_upShadow_iff_exists_sdiff, ← covBy_iff_card_sdiff_eq_one, covBy_iff_exists_erase]
   aesop
 #align finset.mem_up_shadow_iff_erase_mem Finset.mem_upShadow_iff_erase_mem
 

Mathlib/Combinatorics/SimpleGraph/ConcreteColorings.lean

@@ -38,7 +38,7 @@ def pathGraph_two_embedding (n : ℕ) (h : 2 ≤ n) : pathGraph 2 ↪g pathGraph
     exact Fin.ext
   map_rel_iff' := by
     intro v w
-    fin_cases v <;> fin_cases w <;> simp [pathGraph, ← Fin.coe_covby_iff]
+    fin_cases v <;> fin_cases w <;> simp [pathGraph, ← Fin.coe_covBy_iff]
 
 theorem chromaticNumber_pathGraph (n : ℕ) (h : 2 ≤ n) :
     (pathGraph n).chromaticNumber = 2 := by

Mathlib/Combinatorics/SimpleGraph/Hasse.lean

@@ -13,7 +13,7 @@ import Mathlib.Order.SuccPred.Relation
 /-!
 # The Hasse diagram as a graph
 
-This file defines the Hasse diagram of an order (graph of `Covby`, the covering relation) and the
+This file defines the Hasse diagram of an order (graph of `CovBy`, the covering relation) and the
 path graph on `n` vertices.
 
 ## Main declarations
@@ -71,7 +71,7 @@ variable [PartialOrder α] [PartialOrder β]
 @[simp]
 theorem hasse_prod : hasse (α × β) = hasse α □ hasse β := by
   ext x y
-  simp_rw [boxProd_adj, hasse_adj, Prod.covby_iff, or_and_right, @eq_comm _ y.1, @eq_comm _ y.2,
+  simp_rw [boxProd_adj, hasse_adj, Prod.covBy_iff, or_and_right, @eq_comm _ y.1, @eq_comm _ y.2,
     or_or_or_comm]
 #align simple_graph.hasse_prod SimpleGraph.hasse_prod
 
@@ -85,16 +85,16 @@ theorem hasse_preconnected_of_succ [SuccOrder α] [IsSuccArchimedean α] : (hass
   fun a b => by
   rw [reachable_iff_reflTransGen]
   exact
-    reflTransGen_of_succ _ (fun c hc => Or.inl <| covby_succ_of_not_isMax hc.2.not_isMax)
-      fun c hc => Or.inr <| covby_succ_of_not_isMax hc.2.not_isMax
+    reflTransGen_of_succ _ (fun c hc => Or.inl <| covBy_succ_of_not_isMax hc.2.not_isMax)
+      fun c hc => Or.inr <| covBy_succ_of_not_isMax hc.2.not_isMax
 #align simple_graph.hasse_preconnected_of_succ SimpleGraph.hasse_preconnected_of_succ
 
 theorem hasse_preconnected_of_pred [PredOrder α] [IsPredArchimedean α] : (hasse α).Preconnected :=
   fun a b => by
   rw [reachable_iff_reflTransGen, ← reflTransGen_swap]
   exact
-    reflTransGen_of_pred _ (fun c hc => Or.inl <| pred_covby_of_not_isMin hc.1.not_isMin)
-      fun c hc => Or.inr <| pred_covby_of_not_isMin hc.1.not_isMin
+    reflTransGen_of_pred _ (fun c hc => Or.inl <| pred_covBy_of_not_isMin hc.1.not_isMin)
+      fun c hc => Or.inr <| pred_covBy_of_not_isMin hc.1.not_isMin
 #align simple_graph.hasse_preconnected_of_pred SimpleGraph.hasse_preconnected_of_pred
 
 end LinearOrder
@@ -107,7 +107,7 @@ def pathGraph (n : ℕ) : SimpleGraph (Fin n) :=
 theorem pathGraph_adj {n : ℕ} {u v : Fin n} :
     (pathGraph n).Adj u v ↔ u.val + 1 = v.val ∨ v.val + 1 = u.val := by
   simp only [pathGraph, hasse]
-  simp_rw [← Fin.coe_covby_iff, Nat.covby_iff_succ_eq]
+  simp_rw [← Fin.coe_covBy_iff, Nat.covBy_iff_succ_eq]
 
 theorem pathGraph_preconnected (n : ℕ) : (pathGraph n).Preconnected :=
   hasse_preconnected_of_succ _
@@ -119,6 +119,6 @@ theorem pathGraph_connected (n : ℕ) : (pathGraph (n + 1)).Connected :=
 
 theorem pathGraph_two_eq_top : pathGraph 2 = ⊤ := by
   ext u v
-  fin_cases u <;> fin_cases v <;> simp [pathGraph, ← Fin.coe_covby_iff, Nat.covby_iff_succ_eq]
+  fin_cases u <;> fin_cases v <;> simp [pathGraph, ← Fin.coe_covBy_iff, Nat.covBy_iff_succ_eq]
 
 end SimpleGraph

Mathlib/Data/Fin/FlagRange.lean

@@ -28,10 +28,10 @@ variable {α : Type*} [PartialOrder α] [BoundedOrder α] {n : ℕ} {f : Fin (n
 - `fₖ₊₁` weakly covers `fₖ` for all `0 ≤ k < n`;
   this means that `fₖ ≤ fₖ₊₁` and there is no `c` such that `fₖ<c<fₖ₊₁`.
 Then the range of `f` is a maximal chain. -/
-theorem IsMaxChain.range_fin_of_covby (h0 : f 0 = ⊥) (hlast : f (.last n) = ⊤)
-    (hcovby : ∀ k : Fin n, f k.castSucc ⩿ f k.succ) :
+theorem IsMaxChain.range_fin_of_covBy (h0 : f 0 = ⊥) (hlast : f (.last n) = ⊤)
+    (hcovBy : ∀ k : Fin n, f k.castSucc ⩿ f k.succ) :
     IsMaxChain (· ≤ ·) (range f) := by
-  have hmono : Monotone f := Fin.monotone_iff_le_succ.2 fun k ↦ (hcovby k).1
+  have hmono : Monotone f := Fin.monotone_iff_le_succ.2 fun k ↦ (hcovBy k).1
   refine ⟨hmono.isChain_range, fun t htc hbt ↦ hbt.antisymm fun x hx ↦ ?_⟩
   rw [mem_range]; by_contra! h
   suffices ∀ k, f k < x by simpa [hlast] using this (.last _)
@@ -40,7 +40,7 @@ theorem IsMaxChain.range_fin_of_covby (h0 : f 0 = ⊥) (hlast : f (.last n) = 
   | zero => simpa [h0, bot_lt_iff_ne_bot] using (h 0).symm
   | succ k ihk =>
     rw [range_subset_iff] at hbt
-    exact (htc.lt_of_le (hbt k.succ) hx (h _)).resolve_right ((hcovby k).2 ihk)
+    exact (htc.lt_of_le (hbt k.succ) hx (h _)).resolve_right ((hcovBy k).2 ihk)
 
 /-- Let `f : Fin (n + 1) → α` be an `(n + 1)`-tuple `(f₀, …, fₙ)` such that
 - `f₀ = ⊥` and `fₙ = ⊤`;
@@ -49,11 +49,11 @@ theorem IsMaxChain.range_fin_of_covby (h0 : f 0 = ⊥) (hlast : f (.last n) = 
 Then the range of `f` is a `Flag α`. -/
 @[simps]
 def Flag.rangeFin (f : Fin (n + 1) → α) (h0 : f 0 = ⊥) (hlast : f (.last n) = ⊤)
-    (hcovby : ∀ k : Fin n, f k.castSucc ⩿ f k.succ) : Flag α where
+    (hcovBy : ∀ k : Fin n, f k.castSucc ⩿ f k.succ) : Flag α where
   carrier := range f
-  Chain' := (IsMaxChain.range_fin_of_covby h0 hlast hcovby).1
-  max_chain' := (IsMaxChain.range_fin_of_covby h0 hlast hcovby).2
+  Chain' := (IsMaxChain.range_fin_of_covBy h0 hlast hcovBy).1
+  max_chain' := (IsMaxChain.range_fin_of_covBy h0 hlast hcovBy).2
 
-@[simp] theorem Flag.mem_rangeFin {x h0 hlast hcovby} :
-    x ∈ rangeFin f h0 hlast hcovby ↔ ∃ k, f k = x :=
+@[simp] theorem Flag.mem_rangeFin {x h0 hlast hcovBy} :
+    x ∈ rangeFin f h0 hlast hcovBy ↔ ∃ k, f k = x :=
   Iff.rfl

Mathlib/Data/Finset/Grade.lean

@@ -27,27 +27,27 @@ variable {α : Type*}
 namespace Multiset
 variable {s t : Multiset α} {a : α}
 
-@[simp] lemma covby_cons (s : Multiset α) (a : α) : s ⋖ a ::ₘ s :=
-  ⟨lt_cons_self _ _, fun t hst hts ↦ (covby_succ _).2 (card_lt_card hst) <| by
+@[simp] lemma covBy_cons (s : Multiset α) (a : α) : s ⋖ a ::ₘ s :=
+  ⟨lt_cons_self _ _, fun t hst hts ↦ (covBy_succ _).2 (card_lt_card hst) <| by
     simpa using card_lt_card hts⟩
 
-lemma _root_.Covby.exists_multiset_cons (h : s ⋖ t) : ∃ a, a ::ₘ s = t :=
+lemma _root_.CovBy.exists_multiset_cons (h : s ⋖ t) : ∃ a, a ::ₘ s = t :=
   (lt_iff_cons_le.1 h.lt).imp fun _a ha ↦ ha.eq_of_not_lt <| h.2 <| lt_cons_self _ _
 
-lemma covby_iff : s ⋖ t ↔ ∃ a, a ::ₘ s = t :=
-  ⟨Covby.exists_multiset_cons, by rintro ⟨a, rfl⟩; exact covby_cons _ _⟩
+lemma covBy_iff : s ⋖ t ↔ ∃ a, a ::ₘ s = t :=
+  ⟨CovBy.exists_multiset_cons, by rintro ⟨a, rfl⟩; exact covBy_cons _ _⟩
 
-lemma _root_.Covby.card_multiset (h : s ⋖ t) : card s ⋖ card t := by
-  obtain ⟨a, rfl⟩ := h.exists_multiset_cons; rw [card_cons]; exact covby_succ _
+lemma _root_.CovBy.card_multiset (h : s ⋖ t) : card s ⋖ card t := by
+  obtain ⟨a, rfl⟩ := h.exists_multiset_cons; rw [card_cons]; exact covBy_succ _
 
-lemma isAtom_iff : IsAtom s ↔ ∃ a, s = {a} := by simp [← bot_covby_iff, covby_iff, eq_comm]
+lemma isAtom_iff : IsAtom s ↔ ∃ a, s = {a} := by simp [← bot_covBy_iff, covBy_iff, eq_comm]
 
 @[simp] lemma isAtom_singleton (a : α) : IsAtom ({a} : Multiset α) := isAtom_iff.2 ⟨_, rfl⟩
 
 instance instGradeMinOrder : GradeMinOrder ℕ (Multiset α) where
   grade := card
   grade_strictMono := card_strictMono
-  covby_grade s t := Covby.card_multiset
+  covBy_grade s t := CovBy.card_multiset
   isMin_grade s hs := by rw [isMin_iff_eq_bot.1 hs]; exact isMin_bot
 
 @[simp] lemma grade_eq (m : Multiset α) : grade ℕ m = card m := rfl
@@ -65,56 +65,56 @@ lemma ordConnected_range_val : Set.OrdConnected (Set.range val : Set <| Multiset
 lemma ordConnected_range_coe : Set.OrdConnected (Set.range ((↑) : Finset α → Set α)) :=
   ⟨by rintro _ _ _ ⟨s, rfl⟩ t ht; exact ⟨_, (s.finite_toSet.subset ht.2).coe_toFinset⟩⟩
 
-@[simp] lemma val_wcovby_val : s.1 ⩿ t.1 ↔ s ⩿ t :=
-  ordConnected_range_val.apply_wcovby_apply_iff ⟨⟨_, val_injective⟩, val_le_iff⟩
+@[simp] lemma val_wcovBy_val : s.1 ⩿ t.1 ↔ s ⩿ t :=
+  ordConnected_range_val.apply_wcovBy_apply_iff ⟨⟨_, val_injective⟩, val_le_iff⟩
 
-@[simp] lemma val_covby_val : s.1 ⋖ t.1 ↔ s ⋖ t :=
-  ordConnected_range_val.apply_covby_apply_iff ⟨⟨_, val_injective⟩, val_le_iff⟩
+@[simp] lemma val_covBy_val : s.1 ⋖ t.1 ↔ s ⋖ t :=
+  ordConnected_range_val.apply_covBy_apply_iff ⟨⟨_, val_injective⟩, val_le_iff⟩
 
-@[simp] lemma coe_wcovby_coe : (s : Set α) ⩿ t ↔ s ⩿ t :=
-  ordConnected_range_coe.apply_wcovby_apply_iff ⟨⟨_, coe_injective⟩, coe_subset⟩
+@[simp] lemma coe_wcovBy_coe : (s : Set α) ⩿ t ↔ s ⩿ t :=
+  ordConnected_range_coe.apply_wcovBy_apply_iff ⟨⟨_, coe_injective⟩, coe_subset⟩
 
-@[simp] lemma coe_covby_coe : (s : Set α) ⋖ t ↔ s ⋖ t :=
-  ordConnected_range_coe.apply_covby_apply_iff ⟨⟨_, coe_injective⟩, coe_subset⟩
+@[simp] lemma coe_covBy_coe : (s : Set α) ⋖ t ↔ s ⋖ t :=
+  ordConnected_range_coe.apply_covBy_apply_iff ⟨⟨_, coe_injective⟩, coe_subset⟩
 
-alias ⟨_, _root_.wcovby.finset_val⟩ := val_wcovby_val
-alias ⟨_, _root_.Covby.finset_val⟩ := val_covby_val
-alias ⟨_, _root_.wcovby.finset_coe⟩ := coe_wcovby_coe
-alias ⟨_, _root_.Covby.finset_coe⟩ := coe_covby_coe
+alias ⟨_, _root_.WCovBy.finset_val⟩ := val_wcovBy_val
+alias ⟨_, _root_.CovBy.finset_val⟩ := val_covBy_val
+alias ⟨_, _root_.WCovBy.finset_coe⟩ := coe_wcovBy_coe
+alias ⟨_, _root_.CovBy.finset_coe⟩ := coe_covBy_coe
 
-@[simp] lemma covby_cons (ha : a ∉ s) : s ⋖ s.cons a ha := by simp [← val_covby_val]
+@[simp] lemma covBy_cons (ha : a ∉ s) : s ⋖ s.cons a ha := by simp [← val_covBy_val]
 
-lemma _root_.Covby.exists_finset_cons (h : s ⋖ t) : ∃ a, ∃ ha : a ∉ s, s.cons a ha = t :=
+lemma _root_.CovBy.exists_finset_cons (h : s ⋖ t) : ∃ a, ∃ ha : a ∉ s, s.cons a ha = t :=
   let ⟨a, ha, hst⟩ := ssubset_iff_exists_cons_subset.1 h.lt
   ⟨a, ha, (hst.eq_of_not_ssuperset <| h.2 <| ssubset_cons _).symm⟩
 
-lemma covby_iff_exists_cons : s ⋖ t ↔ ∃ a, ∃ ha : a ∉ s, s.cons a ha = t :=
-  ⟨Covby.exists_finset_cons, by rintro ⟨a, ha, rfl⟩; exact covby_cons _⟩
+lemma covBy_iff_exists_cons : s ⋖ t ↔ ∃ a, ∃ ha : a ∉ s, s.cons a ha = t :=
+  ⟨CovBy.exists_finset_cons, by rintro ⟨a, ha, rfl⟩; exact covBy_cons _⟩
 
-lemma _root_.Covby.card_finset (h : s ⋖ t) : s.card ⋖ t.card := (val_covby_val.2 h).card_multiset
+lemma _root_.CovBy.card_finset (h : s ⋖ t) : s.card ⋖ t.card := (val_covBy_val.2 h).card_multiset
 
 section DecidableEq
 variable [DecidableEq α]
 
-@[simp] lemma wcovby_insert (s : Finset α) (a : α) : s ⩿ insert a s := by simp [← coe_wcovby_coe]
-@[simp] lemma erase_wcovby (s : Finset α) (a : α) : s.erase a ⩿ s := by simp [← coe_wcovby_coe]
+@[simp] lemma wcovBy_insert (s : Finset α) (a : α) : s ⩿ insert a s := by simp [← coe_wcovBy_coe]
+@[simp] lemma erase_wcovBy (s : Finset α) (a : α) : s.erase a ⩿ s := by simp [← coe_wcovBy_coe]
 
-lemma covby_insert (ha : a ∉ s) : s ⋖ insert a s :=
-  (wcovby_insert _ _).covby_of_lt <| ssubset_insert ha
+lemma covBy_insert (ha : a ∉ s) : s ⋖ insert a s :=
+  (wcovBy_insert _ _).covBy_of_lt <| ssubset_insert ha
 
-@[simp] lemma erase_covby (ha : a ∈ s) : s.erase a ⋖ s := ⟨erase_ssubset ha, (erase_wcovby _ _).2⟩
+@[simp] lemma erase_covBy (ha : a ∈ s) : s.erase a ⋖ s := ⟨erase_ssubset ha, (erase_wcovBy _ _).2⟩
 
-lemma _root_.Covby.exists_finset_insert (h : s ⋖ t) : ∃ a ∉ s, insert a s = t := by
+lemma _root_.CovBy.exists_finset_insert (h : s ⋖ t) : ∃ a ∉ s, insert a s = t := by
   simpa using h.exists_finset_cons
 
-lemma _root_.Covby.exists_finset_erase (h : s ⋖ t) : ∃ a ∈ t, t.erase a = s := by
+lemma _root_.CovBy.exists_finset_erase (h : s ⋖ t) : ∃ a ∈ t, t.erase a = s := by
   simpa only [← coe_inj, coe_erase] using h.finset_coe.exists_set_sdiff_singleton
 
-lemma covby_iff_exists_insert : s ⋖ t ↔ ∃ a ∉ s, insert a s = t := by
-  simp only [← coe_covby_coe, Set.covby_iff_exists_insert, ← coe_inj, coe_insert, mem_coe]
+lemma covBy_iff_exists_insert : s ⋖ t ↔ ∃ a ∉ s, insert a s = t := by
+  simp only [← coe_covBy_coe, Set.covBy_iff_exists_insert, ← coe_inj, coe_insert, mem_coe]
 
-lemma covby_iff_card_sdiff_eq_one : t ⋖ s ↔ t ⊆ s ∧ (s \ t).card = 1 := by
-  rw [covby_iff_exists_insert]
+lemma covBy_iff_card_sdiff_eq_one : t ⋖ s ↔ t ⊆ s ∧ (s \ t).card = 1 := by
+  rw [covBy_iff_exists_insert]
   constructor
   · rintro ⟨a, ha, rfl⟩
     simp [*]
@@ -123,16 +123,16 @@ lemma covby_iff_card_sdiff_eq_one : t ⋖ s ↔ t ⊆ s ∧ (s \ t).card = 1 :=
     refine ⟨a, (mem_sdiff.1 <| superset_of_eq ha <| mem_singleton_self _).2, ?_⟩
     rw [insert_eq, ← ha, sdiff_union_of_subset hts]
 
-lemma covby_iff_exists_erase : s ⋖ t ↔ ∃ a ∈ t, t.erase a = s := by
-  simp only [← coe_covby_coe, Set.covby_iff_exists_sdiff_singleton, ← coe_inj, coe_erase, mem_coe]
+lemma covBy_iff_exists_erase : s ⋖ t ↔ ∃ a ∈ t, t.erase a = s := by
+  simp only [← coe_covBy_coe, Set.covBy_iff_exists_sdiff_singleton, ← coe_inj, coe_erase, mem_coe]
 
 end DecidableEq
 
 @[simp] lemma isAtom_singleton (a : α) : IsAtom ({a} : Finset α) :=
   ⟨singleton_ne_empty a, fun _ ↦ eq_empty_of_ssubset_singleton⟩
 
 protected lemma isAtom_iff : IsAtom s ↔ ∃ a, s = {a} := by
-  simp [← bot_covby_iff, covby_iff_exists_cons, eq_comm]
+  simp [← bot_covBy_iff, covBy_iff_exists_cons, eq_comm]
 
 section Fintype
 variable [Fintype α] [DecidableEq α]
@@ -149,15 +149,15 @@ to record that the inclusion `Finset α ↪ Multiset α` preserves the covering
 instance instGradeMinOrder_multiset : GradeMinOrder (Multiset α) (Finset α) where
   grade := val
   grade_strictMono := val_strictMono
-  covby_grade _ _ := Covby.finset_val
+  covBy_grade _ _ := CovBy.finset_val
   isMin_grade s hs := by rw [isMin_iff_eq_bot.1 hs]; exact isMin_bot
 
 @[simp] lemma grade_multiset_eq (s : Finset α) : grade (Multiset α) s = s.1 := rfl
 
 instance instGradeMinOrder_nat : GradeMinOrder ℕ (Finset α) where
   grade := card
   grade_strictMono := card_strictMono
-  covby_grade _ _ := Covby.card_finset
+  covBy_grade _ _ := CovBy.card_finset
   isMin_grade s hs := by rw [isMin_iff_eq_bot.1 hs]; exact isMin_bot
 
 @[simp] lemma grade_eq (s : Finset α) : grade ℕ s = s.card := rfl

Mathlib/Data/Finset/Interval.lean

@@ -140,7 +140,7 @@ section Cons
 /-- A function `f` from `Finset α` is monotone if and only if `f s ≤ f (cons a s ha)` for all `s`
 and `a ∉ s`. -/
 lemma monotone_iff_forall_le_cons : Monotone f ↔ ∀ s, ∀ ⦃a⦄ (ha), f s ≤ f (cons a s ha) := by
-  classical simp [monotone_iff_forall_covby, covby_iff_exists_cons]
+  classical simp [monotone_iff_forall_covBy, covBy_iff_exists_cons]
 
 /-- A function `f` from `Finset α` is antitone if and only if `f (cons a s ha) ≤ f s` for all
 `s` and `a ∉ s`. -/
@@ -150,7 +150,7 @@ lemma antitone_iff_forall_cons_le : Antitone f ↔ ∀ s ⦃a⦄ ha, f (cons a s
 /-- A function `f` from `Finset α` is strictly monotone if and only if `f s < f (cons a s ha)` for
 all `s` and `a ∉ s`. -/
 lemma strictMono_iff_forall_lt_cons : StrictMono f ↔ ∀ s ⦃a⦄ ha, f s < f (cons a s ha) := by
-  classical simp [strictMono_iff_forall_covby, covby_iff_exists_cons]
+  classical simp [strictMono_iff_forall_covBy, covBy_iff_exists_cons]
 
 /-- A function `f` from `Finset α` is strictly antitone if and only if `f (cons a s ha) < f s` for
 all `s` and `a ∉ s`. -/