feat: add uppercase lean 3 linter (#1796)

* [ ] depends on: #1794

Implements a linter for lean 3 declarations containing capital letters (as [suggested on Zulip](https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/non-aligned.20definitions/near/323102645)).

Co-authored-by: Mario Carneiro <di.gama@gmail.com>

Mathlib/Algebra/EuclideanDomain/Basic.lean

@@ -222,6 +222,7 @@ theorem xgcdAux_P (a b : R) {r r' : R} {s t s' t'} (p : P a b (r, s, t))
     dsimp
     rw [mul_sub, mul_sub, add_sub, sub_add_eq_add_sub, ← p', sub_sub, mul_comm _ s, ← mul_assoc,
       mul_comm _ t, ← mul_assoc, ← add_mul, ← p, mod_eq_sub_mul_div]
+set_option linter.uppercaseLean3 false in
 #align euclidean_domain.xgcd_aux_P EuclideanDomain.xgcdAux_P
 
 /-- An explicit version of **Bézout's lemma** for Euclidean domains. -/

Mathlib/Algebra/GroupPower/Lemmas.lean

@@ -656,6 +656,7 @@ theorem sign_cases_of_C_mul_pow_nonneg {C r : R} (h : ∀ n : ℕ, 0 ≤ C * r ^
   refine' this.eq_or_lt.elim (fun h => Or.inl h.symm) fun hC => Or.inr ⟨hC, _⟩
   refine' nonneg_of_mul_nonneg_right _ hC
   simpa only [pow_one] using h 1
+set_option linter.uppercaseLean3 false in
 #align sign_cases_of_C_mul_pow_nonneg sign_cases_of_C_mul_pow_nonneg
 
 end LinearOrderedSemiring

Mathlib/Algebra/IndicatorFunction.lean

@@ -472,7 +472,7 @@ theorem mulIndicator_mul_compl_eq_piecewise [DecidablePred (· ∈ s)] (f g : α
   ·
     rw [piecewise_eq_of_not_mem _ _ _ h, Pi.mul_apply, Set.mulIndicator_of_not_mem h,
       Set.mulIndicator_of_mem (Set.mem_compl h), one_mul]
-#align set.mulIndicator_mul_compl_eq_piecewise Set.mulIndicator_mul_compl_eq_piecewise
+#align set.mul_indicator_mul_compl_eq_piecewise Set.mulIndicator_mul_compl_eq_piecewise
 #align set.indicator_add_compl_eq_piecewise Set.indicator_add_compl_eq_piecewise
 
 /-- `Set.mulIndicator` as a `monoidHom`. -/

Mathlib/Algebra/Order/LatticeGroup.lean

@@ -607,7 +607,9 @@ theorem mabs_inf_div_inf_le_mabs [CovariantClass α α (· * ·) (· ≤ ·)] (a
 theorem m_Birkhoff_inequalities [CovariantClass α α (· * ·) (· ≤ ·)] (a b c : α) :
     |(a ⊔ c) / (b ⊔ c)| ⊔ |(a ⊓ c) / (b ⊓ c)| ≤ |a / b| :=
   sup_le (mabs_sup_div_sup_le_mabs a b c) (mabs_inf_div_inf_le_mabs a b c)
+set_option linter.uppercaseLean3 false in
 #align lattice_ordered_comm_group.m_Birkhoff_inequalities LatticeOrderedCommGroup.m_Birkhoff_inequalities
+set_option linter.uppercaseLean3 false in
 #align lattice_ordered_comm_group.Birkhoff_inequalities LatticeOrderedCommGroup.Birkhoff_inequalities
 
 -- Banasiak Proposition 2.12, Zaanen 2nd lecture

Mathlib/Algebra/Ring/Basic.lean

@@ -135,6 +135,7 @@ theorem vieta_formula_quadratic {b c x : α} (h : x * x - b * x + c = 0) :
   have : c = x * (b - x) := (eq_neg_of_add_eq_zero_right h).trans (by simp [mul_sub, mul_comm])
   refine' ⟨b - x, _, by simp, by rw [this]⟩
   rw [this, sub_add, ← sub_mul, sub_self]
+set_option linter.uppercaseLean3 false in
 #align Vieta_formula_quadratic vieta_formula_quadratic
 
 end NonUnitalCommRing

Mathlib/CategoryTheory/Category/KleisliCat.lean

@@ -28,6 +28,9 @@ universe u v
 
 namespace CategoryTheory
 
+-- This file is about Lean 3 declaration "Kleisli".
+set_option linter.uppercaseLean3 false
+
 /-- The Kleisli category on the (type-)monad `m`. Note that the monad is not assumed to be lawful
 yet. -/
 @[nolint unusedArguments]

Mathlib/CategoryTheory/Category/RelCat.lean

@@ -19,6 +19,9 @@ namespace CategoryTheory
 
 universe u
 
+-- This file is about Lean 3 declaration "Rel".
+set_option linter.uppercaseLean3 false
+
 /-- A type synonym for `Type`, which carries the category instance for which
     morphisms are binary relations. -/
 def RelCat :=

Mathlib/Combinatorics/Hall/Finite.lean

@@ -123,6 +123,7 @@ theorem hall_hard_inductive_step_A {n : ℕ} (hn : Fintype.card ι = n + 1)
     · specialize hfr ⟨z, hz⟩
       rw [mem_erase] at hfr
       exact hfr.2
+set_option linter.uppercaseLean3 false in
 #align hall_marriage_theorem.hall_hard_inductive_step_A HallMarriageTheorem.hall_hard_inductive_step_A
 
 theorem hall_cond_of_restrict {ι : Type u} {t : ι → Finset α} {s : Finset ι}
@@ -221,8 +222,8 @@ theorem hall_hard_inductive_step_B {n : ℕ} (hn : Fintype.card ι = n + 1)
     split_ifs with h <;> simp
     · exact hsf' ⟨x, h⟩
     · exact sdiff_subset _ _ (hsf'' ⟨x, h⟩)
-#align
-    hall_marriage_theorem.hall_hard_inductive_step_B HallMarriageTheorem.hall_hard_inductive_step_B
+set_option linter.uppercaseLean3 false in
+#align hall_marriage_theorem.hall_hard_inductive_step_B HallMarriageTheorem.hall_hard_inductive_step_B
 
 end Fintype
 

Mathlib/Data/Int/GCD.lean

@@ -141,6 +141,7 @@ theorem xgcd_aux_P {r r'} :
     rw [Int.emod_def]; generalize (b / a : ℤ) = k
     rw [p, p', mul_sub, sub_add_eq_add_sub, mul_sub, add_mul, mul_comm k t, mul_comm k s,
       ← mul_assoc, ← mul_assoc, add_comm (x * s * k), ← add_sub_assoc, sub_sub]
+set_option linter.uppercaseLean3 false in
 #align nat.xgcd_aux_P Nat.xgcd_aux_P
 
 /-- **Bézout's lemma**: given `x y : ℕ`, `gcd x y = x * a + y * b`, where `a = gcd_a x y` and

Mathlib/Data/Nat/Factorial/Basic.lean

@@ -410,7 +410,7 @@ theorem add_descFactorial_eq_ascFactorial (n : ℕ) :
   | succ k => by
     rw [Nat.add_succ, Nat.succ_eq_add_one, Nat.succ_eq_add_one,
         succ_descFactorial_succ, ascFactorial_succ, add_descFactorial_eq_ascFactorial _ k]
-#align nat.add_descFactorial_eq_asc_factorial Nat.add_descFactorial_eq_ascFactorial
+#align nat.add_desc_factorial_eq_asc_factorial Nat.add_descFactorial_eq_ascFactorial
 
 /-- `n.descFactorial k = n! / (n - k)!` but without ℕ-division. See `Nat.descFactorial_eq_div`
 for the version using ℕ-division. -/

Mathlib/Data/PFunctor/Univariate/Basic.lean

@@ -18,6 +18,8 @@ polynomial functor.  (For the M-type construction, see
 pfunctor/M.lean.)
 -/
 
+-- "W", "Idx"
+set_option linter.uppercaseLean3 false
 
 universe u
 

Mathlib/Data/Real/Basic.lean

@@ -69,6 +69,7 @@ theorem ext_cauchy {x y : Real} : x.cauchy = y.cauchy → x = y :=
 /-- The real numbers are isomorphic to the quotient of Cauchy sequences on the rationals. -/
 def equivCauchy : ℝ ≃ CauSeq.Completion.Cauchy (abs : ℚ → ℚ) :=
   ⟨Real.cauchy, Real.ofCauchy, fun ⟨_⟩ => rfl, fun _ => rfl⟩
+set_option linter.uppercaseLean3 false in
 #align real.equiv_Cauchy Real.equivCauchy
 
 -- irreducible doesn't work for instances: https://github.com/leanprover-community/lean/issues/511
@@ -240,6 +241,7 @@ def ringEquivCauchy : ℝ ≃+* CauSeq.Completion.Cauchy (abs : ℚ → ℚ) :=
     invFun := ofCauchy
     map_add' := cauchy_add
     map_mul' := cauchy_mul }
+set_option linter.uppercaseLean3 false in
 #align real.ring_equiv_Cauchy Real.ringEquivCauchy
 
 /-! Extra instances to short-circuit type class resolution.

Mathlib/Data/Real/CauSeqCompletion.lean

@@ -32,6 +32,7 @@ variable {β : Type _} [Ring β] (abv : β → α) [IsAbsoluteValue abv]
 /-- The Cauchy completion of a ring with absolute value. -/
 def Cauchy :=
   @Quotient (CauSeq _ abv) CauSeq.equiv
+set_option linter.uppercaseLean3 false in
 #align cau_seq.completion.Cauchy CauSeq.Completion.Cauchy
 
 variable {abv}

Mathlib/Data/Seq/Computation.lean

@@ -67,6 +67,7 @@ def think (c : Computation α) : Computation α :=
 def thinkN (c : Computation α) : ℕ → Computation α
   | 0 => c
   | n + 1 => think (thinkN c n)
+set_option linter.uppercaseLean3 false in
 #align computation.thinkN Computation.thinkN
 
 -- check for immediate result
@@ -210,6 +211,7 @@ def Corec.f (f : β → Sum α β) : Sum α β → Option α × Sum α β
       | Sum.inl a => some a
       | Sum.inr _ => none,
       f b)
+set_option linter.uppercaseLean3 false in
 #align computation.corec.F Computation.Corec.f
 
 /-- `corec f b` is the corecursor for `Computation α` as a coinductive type.
@@ -412,14 +414,17 @@ theorem eq_empty_of_not_terminates {s} (H : ¬Terminates s) : s = empty α := by
 theorem thinkN_mem {s : Computation α} {a} : ∀ n, a ∈ thinkN s n ↔ a ∈ s
   | 0 => Iff.rfl
   | n + 1 => Iff.trans ⟨of_think_mem, think_mem⟩ (thinkN_mem n)
+set_option linter.uppercaseLean3 false in
 #align computation.thinkN_mem Computation.thinkN_mem
 
 instance thinkN_terminates (s : Computation α) : ∀ [Terminates s] (n), Terminates (thinkN s n)
   | ⟨⟨a, h⟩⟩, n => ⟨⟨a, (thinkN_mem n).2 h⟩⟩
+set_option linter.uppercaseLean3 false in
 #align computation.thinkN_terminates Computation.thinkN_terminates
 
 theorem of_thinkN_terminates (s : Computation α) (n) : Terminates (thinkN s n) → Terminates s
   | ⟨⟨a, h⟩⟩ => ⟨⟨a, (thinkN_mem _).1 h⟩⟩
+set_option linter.uppercaseLean3 false in
 #align computation.of_thinkN_terminates Computation.of_thinkN_terminates
 
 /-- `Promises s a`, or `s ~> a`, asserts that although the computation `s`
@@ -477,6 +482,7 @@ theorem get_think : get (think s) = get s :=
 @[simp]
 theorem get_thinkN (n) : get (thinkN s n) = get s :=
   get_eq_of_mem _ <| (thinkN_mem _).2 (get_mem _)
+set_option linter.uppercaseLean3 false in
 #align computation.get_thinkN Computation.get_thinkN
 
 theorem get_promises : s ~> get s := fun _ => get_eq_of_mem _
@@ -587,16 +593,19 @@ theorem results_thinkN {s : Computation α} {a m} :
     ∀ n, Results s a m → Results (thinkN s n) a (m + n)
   | 0, h => h
   | n + 1, h => results_think (results_thinkN n h)
+set_option linter.uppercaseLean3 false in
 #align computation.results_thinkN Computation.results_thinkN
 
 theorem results_thinkN_pure (a : α) (n) : Results (thinkN (pure a) n) a n := by
   have := results_thinkN n (results_pure a) ; rwa [Nat.zero_add] at this
+set_option linter.uppercaseLean3 false in
 #align computation.results_thinkN_ret Computation.results_thinkN_pure
 
 @[simp]
 theorem length_thinkN (s : Computation α) [_h : Terminates s] (n) :
     length (thinkN s n) = length s + n :=
   (results_thinkN n (results_of_terminates _)).length
+set_option linter.uppercaseLean3 false in
 #align computation.length_thinkN Computation.length_thinkN
 
 theorem eq_thinkN {s : Computation α} {a n} (h : Results s a n) : s = thinkN (pure a) n := by
@@ -611,11 +620,13 @@ theorem eq_thinkN {s : Computation α} {a n} (h : Results s a n) : s = thinkN (p
     contradiction
   · rw [IH (results_think_iff.1 h)]
     rfl
+set_option linter.uppercaseLean3 false in
 #align computation.eq_thinkN Computation.eq_thinkN
 
 theorem eq_thinkN' (s : Computation α) [_h : Terminates s] :
     s = thinkN (pure (get s)) (length s) :=
   eq_thinkN (results_of_terminates _)
+set_option linter.uppercaseLean3 false in
 #align computation.eq_thinkN' Computation.eq_thinkN'
 
 /-- Recursor based on memberhip-/
@@ -650,6 +661,7 @@ def map (f : α → β) : Computation α → Computation β
 def Bind.g : Sum β (Computation β) → Sum β (Sum (Computation α) (Computation β))
   | Sum.inl b => Sum.inl b
   | Sum.inr cb' => Sum.inr <| Sum.inr cb'
+set_option linter.uppercaseLean3 false in
 #align computation.bind.G Computation.Bind.g
 
 /-- bind over a function mapping `α` to a `Computation`-/
@@ -660,6 +672,7 @@ def Bind.f (f : α → Computation β) :
     | Sum.inl a => Bind.g <| destruct (f a)
     | Sum.inr ca' => Sum.inr <| Sum.inl ca'
   | Sum.inr cb => Bind.g <| destruct cb
+set_option linter.uppercaseLean3 false in
 #align computation.bind.F Computation.Bind.f
 
 /-- Compose two computations into a monadic `bind` operation. -/
@@ -1010,6 +1023,7 @@ theorem think_equiv (s : Computation α) : think s ~ s := fun _ => ⟨of_think_m
 #align computation.think_equiv Computation.think_equiv
 
 theorem thinkN_equiv (s : Computation α) (n) : thinkN s n ~ s := fun _ => thinkN_mem n
+set_option linter.uppercaseLean3 false in
 #align computation.thinkN_equiv Computation.thinkN_equiv
 
 theorem bind_congr {s1 s2 : Computation α} {f1 f2 : α → Computation β} (h1 : s1 ~ s2)

Mathlib/Data/Set/Intervals/OrdConnected.lean

@@ -148,7 +148,7 @@ theorem ordConnected_Ioi {a : α} : OrdConnected (Ioi a) :=
 @[instance]
 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.ord_connected_Iio Set.ordConnected_Iio
 
 @[instance]
 theorem ordConnected_Icc {a b : α} : OrdConnected (Icc a b) :=

Mathlib/Data/Set/Sigma.lean

@@ -40,7 +40,7 @@ theorem image_sigmaMk_preimage_sigmaMap_subset {β : ι' → Type _} (f : ι →
     (g : ∀ i, α i → β (f i)) (i : ι) (s : Set (β (f i))) :
     Sigma.mk i '' (g i ⁻¹' s) ⊆ Sigma.map f g ⁻¹' (Sigma.mk (f i) '' s) :=
   image_subset_iff.2 fun x hx ↦ ⟨g i x, hx, rfl⟩
-#align set.image_sigma_mk_preimage_sigmaMap_subset Set.image_sigmaMk_preimage_sigmaMap_subset
+#align set.image_sigma_mk_preimage_sigma_map_subset Set.image_sigmaMk_preimage_sigmaMap_subset
 
 theorem image_sigmaMk_preimage_sigmaMap {β : ι' → Type _} {f : ι → ι'} (hf : Function.Injective f)
     (g : ∀ i, α i → β (f i)) (i : ι) (s : Set (β (f i))) :

Mathlib/Data/TypeVec.lean

@@ -278,7 +278,7 @@ theorem appendFun_comp' {α₀ α₁ α₂ : TypeVec n} {β₀ β₁ β₂ : Typ
 
 theorem nilFun_comp {α₀ : TypeVec 0} (f₀ : α₀ ⟹ Fin2.elim0) : nilFun ⊚ f₀ = f₀ :=
   funext fun x => by apply Fin2.elim0 x -- porting note: `by apply` is necessary?
-#align typevec.nilFun_comp TypeVec.nilFun_comp
+#align typevec.nil_fun_comp TypeVec.nilFun_comp
 
 theorem appendFun_comp_id {α : TypeVec n} {β₀ β₁ β₂ : Type _} (g₀ : β₀ → β₁) (g₁ : β₁ → β₂) :
     (@id _ α ::: g₁ ∘ g₀) = (id ::: g₁) ⊚ (id ::: g₀) :=

Mathlib/Data/W/Basic.lean

@@ -30,6 +30,8 @@ While the name `WType` is somewhat verbose, it is preferable to putting a single
 identifier `W` in the root namespace.
 -/
 
+-- For "W_type"
+set_option linter.uppercaseLean3 false
 
 /--
 Given `β : α → Type*`, `WType β` is the type of finitely branching trees where nodes are labeled by

Mathlib/Init/Core.lean

@@ -15,12 +15,12 @@ import Mathlib.Tactic.Relation.Trans
 /-! ### alignments from lean 3 `init.core` -/
 
 #align id id -- align this first so idDelta doesn't take priority
-#align idDelta id
+#align id_delta id
 
 #align opt_param optParam
 #align out_param outParam
 
-#align idRhs id
+#align id_rhs id
 #align punit PUnit
 #align punit.star PUnit.unit
 #align unit.star Unit.unit
@@ -131,9 +131,6 @@ namespace Combinator
 def I (a : α) := a
 def K (a : α) (_b : β) := a
 def S (x : α → β → γ) (y : α → β) (z : α) := x z (y z)
-#align combinator.I Combinator.I
-#align combinator.K Combinator.K
-#align combinator.S Combinator.S
 
 end Combinator
 

Mathlib/Mathport/Rename.lean

@@ -86,6 +86,16 @@ def removeX : Name → Name
 
 open Lean.Elab Lean.Elab.Command
 
+/-- Because lean 3 uses a lowercase snake case convention, it is expected that all lean 3
+declaration names should use lowercase, with a few rare exceptions for categories and the set union
+operator. This linter warns if you use uppercase in the lean 3 part of an `#align` statement,
+because this is most likely a typo. But if the declaration actually uses capitals it is not unusual
+to disable this lint locally or at file scope. -/
+register_option linter.uppercaseLean3 : Bool := {
+  defValue := true
+  descr := "enable the lean 3 casing lint"
+}
+
 /-- Check that the referenced lean 4 definition exists in an `#align` directive. -/
 register_option align.precheck : Bool := {
   defValue := true
@@ -116,6 +126,20 @@ def ensureUnused [Monad m] [MonadEnv m] [MonadError m] (id : Name) : m Unit := d
     else
       throwError "{id} has already been aligned (to {n})"
 
+/--
+Purported Lean 3 names containing capital letters are suspicious.
+However, we disregard capital letters occurring in a few common names.
+-/
+def suspiciousLean3Name (s : String) : Bool := Id.run do
+  let allowed : List String :=
+    ["Prop", "Type", "Pi", "Exists", "End",
+     "Inf", "Sup", "Union", "Inter",
+     "Ioo", "Ico", "Iio", "Icc", "Iic", "Ioc", "Ici", "Ioi", "Ixx"]
+  let mut s := s
+  for a in allowed do
+    s := s.replace a ""
+  return s.any (·.isUpper)
+
 /-- Elaborate an `#align` command. -/
 @[command_elab align] def elabAlign : CommandElab
   | `(#align $id3:ident $id4:ident) => do
@@ -133,6 +157,12 @@ def ensureUnused [Monad m] [MonadEnv m] [MonadError m] (id : Name) : m Unit := d
           }\n\n#align inputs have to be fully qualified.{""
           } (Double check the lean 3 name too, we can't check that!)"
         throwErrorAt id4 "Declaration {c} not found.{inner}\n{note}"
+      if Linter.getLinterValue linter.uppercaseLean3 (← getOptions) then
+        if id3.getId.anyS suspiciousLean3Name then
+          Linter.logLint linter.uppercaseLean3 id3 $
+            "Lean 3 names are usually lowercase. This might be a typo.\n" ++
+            "If the Lean 3 name is correct, then above this line, add:\n" ++
+            "set_option linter.uppercaseLean3 false in\n"
     withRef id3 <| ensureUnused id3.getId
     liftCoreM <| addNameAlignment id3.getId id4.getId
   | _ => throwUnsupportedSyntax

Mathlib/Order/Bounds/Basic.lean

@@ -1410,7 +1410,7 @@ theorem image2_upperBounds_lowerBounds_subset_upperBounds_image2 :
     image2 f (upperBounds s) (lowerBounds t) ⊆ upperBounds (image2 f s t) := by
   rintro _ ⟨a, b, ha, hb, rfl⟩
   exact mem_upperBounds_image2_of_mem_upperBounds_of_mem_lowerBounds h₀ h₁ ha hb
-#align image2_upper_bounds_lower_bounds_subset_upperBounds_image2 image2_upperBounds_lowerBounds_subset_upperBounds_image2
+#align image2_upper_bounds_lower_bounds_subset_upper_bounds_image2 image2_upperBounds_lowerBounds_subset_upperBounds_image2
 
 theorem image2_lowerBounds_upperBounds_subset_lowerBounds_image2 :
     image2 f (lowerBounds s) (upperBounds t) ⊆ lowerBounds (image2 f s t) := by

Mathlib/Order/Filter/AtTopBot.lean

@@ -965,7 +965,7 @@ theorem not_tendsto_pow_atTop_atBot [LinearOrderedRing α] :
     ∀ {n : ℕ}, ¬Tendsto (fun x : α => x ^ n) atTop atBot
   | 0 => by simp [not_tendsto_const_atBot]
   | n + 1 => (tendsto_pow_atTop n.succ_ne_zero).not_tendsto disjoint_atTop_atBot
-#align filter.not_tendsto_pow_at_top_atBot Filter.not_tendsto_pow_atTop_atBot
+#align filter.not_tendsto_pow_at_top_at_bot Filter.not_tendsto_pow_atTop_atBot
 
 section LinearOrderedSemifield
 
@@ -1055,7 +1055,7 @@ and only if `f` tends to negative infinity along the same filter. -/
 theorem tendsto_const_mul_atBot_of_pos (hr : 0 < r) :
     Tendsto (fun x => r * f x) l atBot ↔ Tendsto f l atBot := by
   simpa only [← mul_neg, ← tendsto_neg_atTop_iff] using tendsto_const_mul_atTop_of_pos hr
-#align filter.tendsto_const_mul_atBot_of_pos Filter.tendsto_const_mul_atBot_of_pos
+#align filter.tendsto_const_mul_at_bot_of_pos Filter.tendsto_const_mul_atBot_of_pos
 
 /-- If `r` is a positive constant, then `λ x, f x * r` tends to negative infinity along a filter if
 and only if `f` tends to negative infinity along the same filter. -/
@@ -1579,7 +1579,7 @@ theorem tendsto_Ioi_atTop [SemilatticeSup α] {a : α} {f : β → Ioi a} {l : F
 theorem tendsto_Iio_atBot [SemilatticeInf α] {a : α} {f : β → Iio a} {l : Filter β} :
     Tendsto f l atBot ↔ Tendsto (fun x => (f x : α)) l atBot := by
   rw [atBot_Iio_eq, tendsto_comap_iff]; rfl
-#align filter.tendsto_Iio_atBot Filter.tendsto_Iio_atBot
+#align filter.tendsto_Iio_at_bot Filter.tendsto_Iio_atBot
 
 theorem tendsto_Ici_atTop [SemilatticeSup α] {a : α} {f : β → Ici a} {l : Filter β} :
     Tendsto f l atTop ↔ Tendsto (fun x => (f x : α)) l atTop := by

Mathlib/Order/Filter/Cofinite.lean

@@ -117,6 +117,7 @@ theorem coprodᵢ_cofinite {α : ι → Type _} [Finite ι] :
     (Filter.coprodᵢ fun i => (cofinite : Filter (α i))) = cofinite :=
   Filter.coext fun s => by
     simp only [compl_mem_coprodᵢ, mem_cofinite, compl_compl, forall_finite_image_eval_iff]
+set_option linter.uppercaseLean3 false in
 #align filter.Coprod_cofinite Filter.coprodᵢ_cofinite
 
 @[simp]

Mathlib/Order/Filter/Pi.lean

@@ -194,6 +194,9 @@ end Pi
 
 section CoprodCat
 
+-- for "Coprod"
+set_option linter.uppercaseLean3 false
+
 /-- Coproduct of filters. -/
 protected def coprodᵢ (f : ∀ i, Filter (α i)) : Filter (∀ i, α i) :=
   ⨆ i : ι, comap (eval i) (f i)