feat(gcongr): support @[gcongr] for Monotone and friends (#28339)

JovanGerb · JovanGerb · commit ef9ae2a4015f · 2025-10-27T16:35:57.000Z
This PR adds the feature to `gcongr` that you can now tag lemmas whose conclusion is `Monotone f`, `Antitone f`, etc.
diff --git a/Mathlib/Algebra/Order/Floor/Ring.lean b/Mathlib/Algebra/Order/Floor/Ring.lean
@@ -128,11 +128,11 @@ theorem lt_succ_floor (a : R) : a < ⌊a⌋.succ :=
 theorem lt_floor_add_one (a : R) : a < ⌊a⌋ + 1 := by
   simpa only [Int.succ, Int.cast_add, Int.cast_one] using lt_succ_floor a
 
-@[mono]
+@[gcongr, mono]
 theorem floor_mono : Monotone (floor : R → ℤ) :=
   gc_coe_floor.monotone_u
 
-@[gcongr, bound] lemma floor_le_floor (hab : a ≤ b) : ⌊a⌋ ≤ ⌊b⌋ := floor_mono hab
+@[bound] lemma floor_le_floor (hab : a ≤ b) : ⌊a⌋ ≤ ⌊b⌋ := floor_mono hab
 
 theorem floor_pos : 0 < ⌊a⌋ ↔ 1 ≤ a := by
   rw [Int.lt_iff_add_one_le, zero_add, le_floor, cast_one]
diff --git a/Mathlib/Algebra/Order/Floor/Semiring.lean b/Mathlib/Algebra/Order/Floor/Semiring.lean
@@ -81,13 +81,14 @@ theorem floor_of_nonpos (ha : a ≤ 0) : ⌊a⌋₊ = 0 :=
     rintro rfl
     exact floor_zero
 
+@[gcongr]
 theorem floor_mono : Monotone (floor : R → ℕ) := fun a b h => by
   obtain ha | ha := le_total a 0
   · rw [floor_of_nonpos ha]
     exact Nat.zero_le _
   · exact le_floor ((floor_le ha).trans h)
 
-@[gcongr, bound] lemma floor_le_floor (hab : a ≤ b) : ⌊a⌋₊ ≤ ⌊b⌋₊ := floor_mono hab
+@[bound] lemma floor_le_floor (hab : a ≤ b) : ⌊a⌋₊ ≤ ⌊b⌋₊ := floor_mono hab
 
 theorem le_floor_iff' (hn : n ≠ 0) : n ≤ ⌊a⌋₊ ↔ (n : R) ≤ a := by
   obtain ha | ha := le_total a 0
diff --git a/Mathlib/Algebra/Order/Module/Algebra.lean b/Mathlib/Algebra/Order/Module/Algebra.lean
@@ -23,15 +23,10 @@ section OrderedSemiring
 variable (β)
 variable [Semiring β] [PartialOrder β] [IsOrderedRing β] [Algebra α β] [SMulPosMono α β] {a : α}
 
-@[mono] lemma algebraMap_mono : Monotone (algebraMap α β) :=
+@[gcongr, mono] lemma algebraMap_mono : Monotone (algebraMap α β) :=
   fun a₁ a₂ ha ↦ by
     simpa only [Algebra.algebraMap_eq_smul_one] using smul_le_smul_of_nonneg_right ha zero_le_one
 
-/-- A version of `algebraMap_mono` for use by `gcongr` since it currently does not preprocess
-`Monotone` conclusions. -/
-@[gcongr] protected lemma GCongr.algebraMap_le_algebraMap {a₁ a₂ : α} (ha : a₁ ≤ a₂) :
-    algebraMap α β a₁ ≤ algebraMap α β a₂ := algebraMap_mono _ ha
-
 lemma algebraMap_nonneg (ha : 0 ≤ a) : 0 ≤ algebraMap α β a := by simpa using algebraMap_mono β ha
 
 end OrderedSemiring
@@ -51,15 +46,10 @@ section SMulPosStrictMono
 variable [SMulPosStrictMono α β] {a a₁ a₂ : α}
 variable (β)
 
-@[mono] lemma algebraMap_strictMono : StrictMono (algebraMap α β) :=
+@[gcongr, mono] lemma algebraMap_strictMono : StrictMono (algebraMap α β) :=
   fun a₁ a₂ ha ↦ by
     simpa only [Algebra.algebraMap_eq_smul_one] using smul_lt_smul_of_pos_right ha zero_lt_one
 
-/-- A version of `algebraMap_strictMono` for use by `gcongr` since it currently does not preprocess
-`Monotone` conclusions. -/
-@[gcongr] protected lemma GCongr.algebraMap_lt_algebraMap {a₁ a₂ : α} (ha : a₁ < a₂) :
-    algebraMap α β a₁ < algebraMap α β a₂ := algebraMap_strictMono _ ha
-
 lemma algebraMap_pos (ha : 0 < a) : 0 < algebraMap α β a := by
   simpa using algebraMap_strictMono β ha
 
diff --git a/Mathlib/Algebra/Order/Ring/Cast.lean b/Mathlib/Algebra/Order/Ring/Cast.lean
@@ -30,15 +30,14 @@ section OrderedAddCommGroupWithOne
 variable [AddCommGroupWithOne R] [PartialOrder R] [AddLeftMono R]
 variable [ZeroLEOneClass R]
 
+@[gcongr]
 lemma cast_mono : Monotone (Int.cast : ℤ → R) := by
   intro m n h
   rw [← sub_nonneg] at h
   lift n - m to ℕ using h with k hk
   rw [← sub_nonneg, ← cast_sub, ← hk, cast_natCast]
   exact k.cast_nonneg'
 
-@[gcongr] protected lemma GCongr.intCast_mono {m n : ℤ} (hmn : m ≤ n) : (m : R) ≤ n := cast_mono hmn
-
 variable [NeZero (1 : R)] {m n : ℤ}
 
 @[simp] lemma cast_nonneg : ∀ {n : ℤ}, (0 : R) ≤ n ↔ 0 ≤ n
diff --git a/Mathlib/Algebra/Ring/Subring/Basic.lean b/Mathlib/Algebra/Ring/Subring/Basic.lean
@@ -69,32 +69,32 @@ variable [Ring S] [Ring T]
 namespace Subring
 variable {s t : Subring R}
 
-@[mono]
+@[gcongr, mono]
 theorem toSubsemiring_strictMono : StrictMono (toSubsemiring : Subring R → Subsemiring R) :=
   fun _ _ => id
 
-@[mono]
+@[gcongr, mono]
 theorem toSubsemiring_mono : Monotone (toSubsemiring : Subring R → Subsemiring R) :=
   toSubsemiring_strictMono.monotone
 
-@[gcongr]
+@[deprecated toSubsemiring_strictMono (since := "2025-10-20")]
 lemma toSubsemiring_lt_toSubsemiring (hst : s < t) : s.toSubsemiring < t.toSubsemiring := hst
 
-@[gcongr]
+@[deprecated toSubsemiring_mono (since := "2025-10-20")]
 lemma toSubsemiring_le_toSubsemiring (hst : s ≤ t) : s.toSubsemiring ≤ t.toSubsemiring := hst
 
-@[mono]
+@[gcongr, mono]
 theorem toAddSubgroup_strictMono : StrictMono (toAddSubgroup : Subring R → AddSubgroup R) :=
   fun _ _ => id
 
-@[mono]
+@[gcongr, mono]
 theorem toAddSubgroup_mono : Monotone (toAddSubgroup : Subring R → AddSubgroup R) :=
   toAddSubgroup_strictMono.monotone
 
-@[gcongr]
+@[deprecated toAddSubgroup_strictMono (since := "2025-10-20")]
 lemma toAddSubgroup_lt_toAddSubgroup (hst : s < t) : s.toAddSubgroup < t.toAddSubgroup := hst
 
-@[gcongr]
+@[deprecated toAddSubgroup_mono (since := "2025-10-20")]
 lemma toAddSubgroup_le_toAddSubgroup (hst : s ≤ t) : s.toAddSubgroup ≤ t.toAddSubgroup := hst
 
 @[mono]
diff --git a/Mathlib/Analysis/Complex/Exponential.lean b/Mathlib/Analysis/Complex/Exponential.lean
@@ -288,20 +288,20 @@ theorem abs_exp (x : ℝ) : |exp x| = exp x :=
 lemma exp_abs_le (x : ℝ) : exp |x| ≤ exp x + exp (-x) := by
   cases le_total x 0 <;> simp [abs_of_nonpos, abs_of_nonneg, exp_nonneg, *]
 
-@[mono]
+@[mono, gcongr]
 theorem exp_strictMono : StrictMono exp := fun x y h => by
   rw [← sub_add_cancel y x, Real.exp_add]
   exact (lt_mul_iff_one_lt_left (exp_pos _)).2
       (lt_of_lt_of_le (by linarith) (add_one_le_exp_of_nonneg (by linarith)))
 
-@[gcongr]
+@[deprecated exp_strictMono (since := "2025-10-20")]
 theorem exp_lt_exp_of_lt {x y : ℝ} (h : x < y) : exp x < exp y := exp_strictMono h
 
-@[mono]
+@[gcongr, mono]
 theorem exp_monotone : Monotone exp :=
   exp_strictMono.monotone
 
-@[gcongr, bound]
+@[bound] -- temporary lemma for the `bound` tactic
 theorem exp_le_exp_of_le {x y : ℝ} (h : x ≤ y) : exp x ≤ exp y := exp_monotone h
 
 @[simp]
diff --git a/Mathlib/Analysis/SpecialFunctions/Log/ERealExp.lean b/Mathlib/Analysis/SpecialFunctions/Log/ERealExp.lean
@@ -54,6 +54,7 @@ end Definition
 /-! ### Monotonicity -/
 section Monotonicity
 
+@[gcongr]
 lemma exp_strictMono : StrictMono exp := by
   intro x y h
   induction x
@@ -62,10 +63,11 @@ lemma exp_strictMono : StrictMono exp := by
   · induction y
     · simp at h
     · simp_rw [exp_coe]
-      exact ENNReal.ofReal_lt_ofReal_iff'.mpr ⟨Real.exp_lt_exp_of_lt (mod_cast h), Real.exp_pos _⟩
+      exact ENNReal.ofReal_lt_ofReal_iff'.mpr ⟨Real.exp_strictMono (mod_cast h), Real.exp_pos _⟩
     · simp
   · exact (not_top_lt h).elim
 
+@[gcongr]
 lemma exp_monotone : Monotone exp := exp_strictMono.monotone
 
 @[simp] lemma exp_lt_exp_iff {a b : EReal} : exp a < exp b ↔ a < b := exp_strictMono.lt_iff_lt
@@ -84,9 +86,11 @@ lemma exp_monotone : Monotone exp := exp_strictMono.monotone
 
 @[simp] lemma one_le_exp_iff {a : EReal} : 1 ≤ exp a ↔ 0 ≤ a := exp_zero ▸ @exp_le_exp_iff 0 a
 
-@[gcongr] lemma exp_le_exp {a b : EReal} (h : a ≤ b) : exp a ≤ exp b := by simpa
+@[deprecated exp_monotone (since := "2025-10-20")]
+lemma exp_le_exp {a b : EReal} (h : a ≤ b) : exp a ≤ exp b := by simpa
 
-@[gcongr] lemma exp_lt_exp {a b : EReal} (h : a < b) : exp a < exp b := by simpa
+@[deprecated exp_strictMono (since := "2025-10-20")]
+lemma exp_lt_exp {a b : EReal} (h : a < b) : exp a < exp b := by simpa
 
 end Monotonicity
 
diff --git a/Mathlib/Analysis/SpecialFunctions/Trigonometric/Arctan.lean b/Mathlib/Analysis/SpecialFunctions/Trigonometric/Arctan.lean
@@ -156,18 +156,19 @@ theorem arcsin_eq_arctan (h : x ∈ Ioo (-(1 : ℝ)) 1) :
 @[simp]
 theorem arctan_zero : arctan 0 = 0 := by simp [arctan_eq_arcsin]
 
-@[mono]
+@[gcongr, mono]
 theorem arctan_strictMono : StrictMono arctan := tanOrderIso.symm.strictMono
 
+@[gcongr]
 theorem arctan_mono : Monotone arctan := arctan_strictMono.monotone
 
-@[gcongr]
+@[deprecated arctan_strictMono (since := "2025-10-20")]
 lemma arctan_lt_arctan (hxy : x < y) : arctan x < arctan y := arctan_strictMono hxy
 
 @[simp]
 theorem arctan_lt_arctan_iff : arctan x < arctan y ↔ x < y := arctan_strictMono.lt_iff_lt
 
-@[gcongr]
+@[deprecated arctan_mono (since := "2025-10-20")]
 lemma arctan_le_arctan (hxy : x ≤ y) : arctan x ≤ arctan y :=
   arctan_strictMono.monotone hxy
 
diff --git a/Mathlib/Combinatorics/Extremal/RuzsaSzemeredi.lean b/Mathlib/Combinatorics/Extremal/RuzsaSzemeredi.lean
@@ -88,13 +88,9 @@ noncomputable def ruzsaSzemerediNumberNat (n : ℕ) : ℕ := ruzsaSzemerediNumbe
 lemma ruzsaSzemerediNumberNat_card : ruzsaSzemerediNumberNat (card α) = ruzsaSzemerediNumber α :=
   ruzsaSzemerediNumber_congr (Fintype.equivFin _).symm
 
--- TODO: Remove once #28339 lands?
-@[gcongr] lemma ruzsaSzemerediNumberNat_le_ruzsaSzemerediNumberNat (hmn : m ≤ n) :
-    ruzsaSzemerediNumberNat m ≤ ruzsaSzemerediNumberNat n :=
-  ruzsaSzemerediNumber_mono (Fin.castLEEmb hmn)
-
-lemma ruzsaSzemerediNumberNat_mono : Monotone ruzsaSzemerediNumberNat :=
-  fun _m _n => ruzsaSzemerediNumberNat_le_ruzsaSzemerediNumberNat
+@[gcongr]
+lemma ruzsaSzemerediNumberNat_mono : Monotone ruzsaSzemerediNumberNat := fun _m _n h =>
+  ruzsaSzemerediNumber_mono (Fin.castLEEmb h)
 
 lemma ruzsaSzemerediNumberNat_le : ruzsaSzemerediNumberNat n ≤ n.choose 3 :=
   ruzsaSzemerediNumber_le.trans_eq <| by rw [Fintype.card_fin]
diff --git a/Mathlib/Data/Finsupp/Order.lean b/Mathlib/Data/Finsupp/Order.lean
@@ -81,12 +81,10 @@ variable [AddCommMonoid α] [PartialOrder α] [IsOrderedAddMonoid α]
 instance isOrderedAddMonoid : IsOrderedAddMonoid (ι →₀ α) :=
   { add_le_add_left := fun _a _b h c s => add_le_add_left (h s) (c s) }
 
+@[gcongr]
 lemma mapDomain_mono : Monotone (mapDomain f : (ι →₀ α) → (κ →₀ α)) := by
   classical exact fun g₁ g₂ h ↦ sum_le_sum_index h (fun _ _ ↦ single_mono) (by simp)
 
-@[gcongr] protected lemma GCongr.mapDomain_mono (hg : g₁ ≤ g₂) : g₁.mapDomain f ≤ g₂.mapDomain f :=
-  mapDomain_mono hg
-
 lemma mapDomain_nonneg (hg : 0 ≤ g) : 0 ≤ g.mapDomain f := by simpa using mapDomain_mono hg
 lemma mapDomain_nonpos (hg : g ≤ 0) : g.mapDomain f ≤ 0 := by simpa using mapDomain_mono hg
 
diff --git a/Mathlib/Data/Multiset/Defs.lean b/Mathlib/Data/Multiset/Defs.lean
@@ -224,21 +224,20 @@ def card : Multiset α → ℕ := Quot.lift length fun _l₁ _l₂ => Perm.lengt
 theorem coe_card (l : List α) : card (l : Multiset α) = length l :=
   rfl
 
-@[gcongr]
 theorem card_le_card {s t : Multiset α} (h : s ≤ t) : card s ≤ card t :=
   leInductionOn h Sublist.length_le
 
 theorem eq_of_le_of_card_le {s t : Multiset α} (h : s ≤ t) : card t ≤ card s → s = t :=
   leInductionOn h fun s h₂ => congr_arg _ <| s.eq_of_length_le h₂
 
-@[gcongr]
 theorem card_lt_card {s t : Multiset α} (h : s < t) : card s < card t :=
   lt_of_not_ge fun h₂ => _root_.ne_of_lt h <| eq_of_le_of_card_le (le_of_lt h) h₂
 
-@[mono]
+@[gcongr, mono]
 theorem card_mono : Monotone (@card α) := fun _a _b => card_le_card
 
-lemma card_strictMono : StrictMono (card : Multiset α → ℕ) := fun _ _ ↦ card_lt_card
+@[gcongr]
+lemma card_strictMono : StrictMono (@card α) := fun _ _ ↦ card_lt_card
 
 /-- Another way of expressing `strongInductionOn`: the `(<)` relation is well-founded. -/
 instance instWellFoundedLT : WellFoundedLT (Multiset α) :=
diff --git a/Mathlib/Data/Nat/Cast/Order/Basic.lean b/Mathlib/Data/Nat/Cast/Order/Basic.lean
@@ -28,14 +28,11 @@ we use a generic collection of instances so that it applies in other settings (e
 variable [AddMonoidWithOne α] [PartialOrder α]
 variable [AddLeftMono α] [ZeroLEOneClass α]
 
-@[mono]
+@[gcongr, mono]
 theorem mono_cast : Monotone (Nat.cast : ℕ → α) :=
   monotone_nat_of_le_succ fun n ↦ by
     rw [Nat.cast_succ]; exact le_add_of_nonneg_right zero_le_one
 
-@[gcongr]
-theorem _root_.GCongr.natCast_le_natCast {a b : ℕ} (h : a ≤ b) : (a : α) ≤ b := mono_cast h
-
 /-- See also `Nat.cast_nonneg`, specialised for an `OrderedSemiring`. -/
 @[simp low]
 theorem cast_nonneg' (n : ℕ) : 0 ≤ (n : α) :=
@@ -62,12 +59,10 @@ end Nontrivial
 
 variable [CharZero α] {m n : ℕ}
 
+@[gcongr]
 theorem strictMono_cast : StrictMono (Nat.cast : ℕ → α) :=
   mono_cast.strictMono_of_injective cast_injective
 
-@[gcongr]
-lemma _root_.GCongr.natCast_lt_natCast {a b : ℕ} (h : a < b) : (a : α) < b := strictMono_cast h
-
 /-- `Nat.cast : ℕ → α` as an `OrderEmbedding` -/
 @[simps! -fullyApplied]
 def castOrderEmbedding : ℕ ↪o α :=
diff --git a/Mathlib/Data/Rat/Cast/Order.lean b/Mathlib/Data/Rat/Cast/Order.lean
@@ -28,11 +28,11 @@ theorem cast_pos_of_pos (hq : 0 < q) : (0 : K) < q := by
   rw [Rat.cast_def]
   exact div_pos (Int.cast_pos.2 <| num_pos.2 hq) (Nat.cast_pos.2 q.pos)
 
-@[mono]
+@[gcongr, mono]
 theorem cast_strictMono : StrictMono ((↑) : ℚ → K) := fun p q => by
   simpa only [sub_pos, cast_sub] using cast_pos_of_pos (K := K) (q := q - p)
 
-@[mono]
+@[gcongr, mono]
 theorem cast_mono : Monotone ((↑) : ℚ → K) :=
   cast_strictMono.monotone
 
@@ -45,9 +45,6 @@ def castOrderEmbedding : ℚ ↪o K :=
 
 @[simp, norm_cast] lemma cast_lt : (p : K) < q ↔ p < q := cast_strictMono.lt_iff_lt
 
-@[gcongr] alias ⟨_, _root_.GCongr.ratCast_le_ratCast⟩ := cast_le
-@[gcongr] alias ⟨_, _root_.GCongr.ratCast_lt_ratCast⟩ := cast_lt
-
 @[simp] lemma cast_nonneg : 0 ≤ (q : K) ↔ 0 ≤ q := by norm_cast
 
 @[simp] lemma cast_nonpos : (q : K) ≤ 0 ↔ q ≤ 0 := by norm_cast
diff --git a/Mathlib/Data/Real/Sqrt.lean b/Mathlib/Data/Real/Sqrt.lean
@@ -184,11 +184,12 @@ theorem sqrt_lt_sqrt_iff (hx : 0 ≤ x) : √x < √y ↔ x < y :=
 theorem sqrt_lt_sqrt_iff_of_pos (hy : 0 < y) : √x < √y ↔ x < y := by
   rw [Real.sqrt, Real.sqrt, NNReal.coe_lt_coe, NNReal.sqrt_lt_sqrt, toNNReal_lt_toNNReal_iff hy]
 
-@[gcongr, bound]
+@[bound]
 theorem sqrt_le_sqrt (h : x ≤ y) : √x ≤ √y := by
   rw [Real.sqrt, Real.sqrt, NNReal.coe_le_coe, NNReal.sqrt_le_sqrt]
   exact toNNReal_le_toNNReal h
 
+@[gcongr]
 theorem sqrt_monotone : Monotone Real.sqrt :=
   fun _ _ ↦ sqrt_le_sqrt
 
diff --git a/Mathlib/LinearAlgebra/Basis/Flag.lean b/Mathlib/LinearAlgebra/Basis/Flag.lean
@@ -55,20 +55,21 @@ theorem self_mem_flag_iff [Nontrivial R] (b : Basis (Fin n) R M) {i : Fin n} {k
     b i ∈ b.flag k ↔ i.castSucc < k :=
   b.self_mem_span_image
 
-@[mono]
+@[gcongr, mono]
 theorem flag_mono (b : Basis (Fin n) R M) : Monotone b.flag :=
   Fin.monotone_iff_le_succ.2 fun k ↦ by rw [flag_succ]; exact le_sup_right
 
 theorem isChain_range_flag (b : Basis (Fin n) R M) : IsChain (· ≤ ·) (range b.flag) :=
   b.flag_mono.isChain_range
 
-@[mono]
+@[gcongr, mono]
 theorem flag_strictMono [Nontrivial R] (b : Basis (Fin n) R M) : StrictMono b.flag :=
   Fin.strictMono_iff_lt_succ.2 fun _ ↦ by simp [flag_succ]
 
-@[gcongr] lemma flag_le_flag (hij : i ≤ j) : b.flag i ≤ b.flag j := flag_mono _ hij
+@[deprecated flag_mono (since := "2025-10-20")]
+lemma flag_le_flag (hij : i ≤ j) : b.flag i ≤ b.flag j := flag_mono _ hij
 
-@[gcongr]
+@[deprecated flag_strictMono (since := "2025-10-20")]
 lemma flag_lt_flag [Nontrivial R] (hij : i < j) : b.flag i < b.flag j := flag_strictMono _ hij
 
 end Semiring
diff --git a/Mathlib/MeasureTheory/Function/SimpleFunc.lean b/Mathlib/MeasureTheory/Function/SimpleFunc.lean
@@ -885,11 +885,11 @@ theorem eapprox_lt_top (f : α → ℝ≥0∞) (n : ℕ) (a : α) : eapprox f n
       _ < ⊤ := ENNReal.coe_lt_top
   · exact WithTop.top_pos
 
-@[mono]
+@[gcongr, mono]
 theorem monotone_eapprox (f : α → ℝ≥0∞) : Monotone (eapprox f) :=
   monotone_approx _ f
 
-@[gcongr]
+@[deprecated monotone_eapprox (since := "2025-08-13")]
 lemma eapprox_mono {m n : ℕ} (hmn : m ≤ n) : eapprox f m ≤ eapprox f n := monotone_eapprox _ hmn
 
 lemma iSup_eapprox_apply (hf : Measurable f) (a : α) : ⨆ n, (eapprox f n : α →ₛ ℝ≥0∞) a = f a := by
diff --git a/Mathlib/MeasureTheory/Integral/Lebesgue/Add.lean b/Mathlib/MeasureTheory/Integral/Lebesgue/Add.lean
@@ -363,7 +363,7 @@ theorem lintegral_const_mul (r : ℝ≥0∞) {f : α → ℝ≥0∞} (hf : Measu
       · intro i j h a
         dsimp
         gcongr
-        exact eapprox_mono h _
+        exact monotone_eapprox _ h _
     _ = r * ∫⁻ a, f a ∂μ := by rw [← ENNReal.mul_iSup, lintegral_eq_iSup_eapprox_lintegral hf]
 
 theorem lintegral_const_mul'' (r : ℝ≥0∞) {f : α → ℝ≥0∞} (hf : AEMeasurable f μ) :
diff --git a/Mathlib/Order/Filter/Map.lean b/Mathlib/Order/Filter/Map.lean
diff --git a/Mathlib/Order/Hom/Basic.lean b/Mathlib/Order/Hom/Basic.lean
diff --git a/Mathlib/Order/KrullDimension.lean b/Mathlib/Order/KrullDimension.lean
diff --git a/Mathlib/Tactic/GCongr/Core.lean b/Mathlib/Tactic/GCongr/Core.lean
diff --git a/MathlibTest/GCongr/inequalities.lean b/MathlibTest/GCongr/inequalities.lean
