Trigger CI for leanprover/lean4#2643

Mathlib/Data/Nat/Cast/Defs.lean

@@ -55,6 +55,14 @@ because they are recognized as terms of `R` (at least when `R` is an `AddMonoidW
 instance instOfNat [NatCast R] [Nat.AtLeastTwo n] : OfNat R n where
   ofNat := n.cast
 
+library_note "no_index around OfNat.ofNat"
+/--
+When writing lemmas about `OfNat.ofNat` that assume `Nat.AtLeastTwo`, the term need to be wrapped in
+`no_index` so as not to confuse `simp`, as `no_index (OfNat.ofNat n)`.
+
+Some discussion is [on Zulip here](https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/.E2.9C.94.20Polynomial.2Ecoeff.20example/near/395438147).
+-/
+
 @[simp, norm_cast] theorem Nat.cast_ofNat [NatCast R] [Nat.AtLeastTwo n] :
   (Nat.cast (no_index (OfNat.ofNat n)) : R) = OfNat.ofNat n := rfl
 

Mathlib/Data/Polynomial/Basic.lean

@@ -757,6 +757,19 @@ lemma coeff_C_succ {r : R} {n : ℕ} : coeff (C r) (n + 1) = 0 := by simp [coeff
 theorem coeff_nat_cast_ite : (Nat.cast m : R[X]).coeff n = ite (n = 0) m 0 := by
   simp only [← C_eq_nat_cast, coeff_C, Nat.cast_ite, Nat.cast_zero]
 
+-- See note [no_index around OfNat.ofNat]
+@[simp]
+theorem coeff_ofNat_zero (a : ℕ) [a.AtLeastTwo] :
+    coeff (no_index (OfNat.ofNat a : R[X])) 0 = OfNat.ofNat a :=
+  coeff_monomial
+
+-- See note [no_index around OfNat.ofNat]
+@[simp]
+theorem coeff_ofNat_succ (a n : ℕ) [h : a.AtLeastTwo] :
+    coeff (no_index (OfNat.ofNat a : R[X])) (n + 1) = 0 := by
+  rw [← Nat.cast_eq_ofNat]
+  simp
+
 theorem C_mul_X_pow_eq_monomial : ∀ {n : ℕ}, C a * X ^ n = monomial n a
   | 0 => mul_one _
   | n + 1 => by

Mathlib/Topology/Homeomorph.lean

@@ -258,10 +258,12 @@ protected theorem secondCountableTopology [TopologicalSpace.SecondCountableTopol
   h.inducing.secondCountableTopology
 #align homeomorph.second_countable_topology Homeomorph.secondCountableTopology
 
+@[simp]
 theorem isCompact_image {s : Set α} (h : α ≃ₜ β) : IsCompact (h '' s) ↔ IsCompact s :=
   h.embedding.isCompact_iff_isCompact_image.symm
 #align homeomorph.is_compact_image Homeomorph.isCompact_image
 
+@[simp]
 theorem isCompact_preimage {s : Set β} (h : α ≃ₜ β) : IsCompact (h ⁻¹' s) ↔ IsCompact s := by
   rw [← image_symm]; exact h.symm.isCompact_image
 #align homeomorph.is_compact_preimage Homeomorph.isCompact_preimage

Mathlib/Topology/SubsetProperties.lean

@@ -2041,3 +2041,35 @@ theorem IsPreirreducible.preimage {Z : Set α} (hZ : IsPreirreducible Z) {f : β
 #align is_preirreducible.preimage IsPreirreducible.preimage
 
 end Preirreducible
+
+section codiscrete_filter
+
+/-- Criterion for a subset `S ⊆ α` to be closed and discrete in terms of the punctured
+neighbourhood filter at an arbitrary point of `α`. (Compare `discreteTopology_subtype_iff`.) -/
+theorem isClosed_and_discrete_iff {S : Set α} : IsClosed S ∧ DiscreteTopology S ↔
+    ∀ x, Disjoint (𝓝[≠] x) (𝓟 S) := by
+  rw [discreteTopology_subtype_iff, isClosed_iff_clusterPt, ← forall_and]
+  congrm (∀ x, ?_)
+  rw [← not_imp_not, clusterPt_iff_not_disjoint, not_not, ←disjoint_iff]
+  constructor <;> intro H
+  · by_cases hx : x ∈ S
+    exacts [H.2 hx, (H.1 hx).mono_left nhdsWithin_le_nhds]
+  · refine ⟨fun hx ↦ ?_, fun _ ↦ H⟩
+    simpa [disjoint_iff, nhdsWithin, inf_assoc, hx] using H
+
+variable (α)
+
+/-- In any topological space, the open sets with with discrete complement form a filter. -/
+def Filter.codiscrete : Filter α where
+  sets := {U | IsOpen U ∧ DiscreteTopology ↑Uᶜ}
+  univ_sets := ⟨isOpen_univ, compl_univ.symm ▸ Subsingleton.discreteTopology⟩
+  sets_of_superset := by
+    intro U V hU hV
+    simp_rw [←isClosed_compl_iff, isClosed_and_discrete_iff] at hU ⊢
+    exact fun x ↦ (hU x).mono_right (principal_mono.mpr <| compl_subset_compl.mpr hV)
+  inter_sets := by
+    intro U V hU hV
+    simp_rw [←isClosed_compl_iff, isClosed_and_discrete_iff] at hU hV ⊢
+    exact fun x ↦ compl_inter U V ▸ sup_principal ▸ disjoint_sup_right.mpr ⟨hU x, hV x⟩
+
+end codiscrete_filter