fixes after bump to v4.22.0 (google-deepmind#1141)

Author: mo271

FormalConjectures/ErdosProblems/730.lean

@@ -58,17 +58,16 @@ There are examples where $(n, m) ∈ S$ with $m ≠ n + 1$.
 (Found by AlphaProof, although it was implicit already in [A129515])
 -/
 @[category research solved, AMS 11]
-theorem erdos_730.variants.delta_ne_one : ∃ (n m : ℕ) (h : (n, m) ∈ S), m ≠ n + 1 := by
+theorem erdos_730.variants.delta_ne_one : ∃ (n m : ℕ), (n, m) ∈ S ∧ m ≠ n + 1 := by
   dsimp [S]
   use 10003
   use 10005
-  simp_all
-  norm_num [ Finset.ext_iff,Nat.choose_eq_zero_iff]
-  simp_rw[Nat.choose_eq_descFactorial_div_factorial]
+  norm_num [Finset.ext_iff, Nat.choose_eq_zero_iff]
+  simp_rw [Nat.choose_eq_descFactorial_div_factorial]
   intro p hp
   constructor
   all_goals exact fun h' => or_self_iff.1 (hp.dvd_mul.1 (
-    h'.trans (by refine' of_decide_eq_true (by constructor:_ = ↑_))))
+    h'.trans (by refine' of_decide_eq_true (by constructor : _ = ↑_))))
 
 
 end Erdos730

FormalConjectures/ErdosProblems/74.lean

@@ -85,7 +85,7 @@ theorem SimpleGraph.subgraphEdgeDistsToBipartite_bddAbove (G : SimpleGraph V) (n
     have := h_fin.fintype
     have := Fintype.ofFinite ↑A.coe.edgeSet
     convert (A.coe).card_edgeFinset_le_card_choose_two
-    · rw [← Set.ncard_coe_Finset A.coe.edgeFinset, coe_edgeFinset A.coe, ← Subgraph.image_coe_edgeSet_coe A]
+    · rw [← Set.ncard_coe_finset A.coe.edgeFinset, coe_edgeFinset A.coe, ← Subgraph.image_coe_edgeSet_coe A]
       exact (Set.ncard_image_iff (Set.toFinite A.coe.edgeSet)).mpr <|
         Function.Injective.injOn <| Sym2.map.injective Subtype.coe_injective
     · rw [Set.ncard_eq_toFinset_card _ h_fin, Set.Finite.card_toFinset]

FormalConjectures/ForMathlib/Computability/TuringMachine/BusyBeavers.lean

@@ -169,7 +169,7 @@ def HaltsAfter (s : Cfg Γ Λ) (n : ℕ) : Prop :=
 
 lemma haltsAfter_zero_iff (s : Cfg Γ Λ) :
     HaltsAfter M s 0 ↔ step M s = none := by
-  rw [HaltsAfter, multiStep, Function.iterate_one, Option.some_bind]
+  rw [HaltsAfter, multiStep, Function.iterate_one, Option.bind_some]
 
 lemma isHalting_iff_exists_haltsAt : IsHalting M ↔ ∃ n, M.HaltsAfter (init []) n :=
   ⟨fun _ ↦ eval_dom_iff.mpr IsHalting.halts, fun H ↦ ⟨eval_dom_iff.mp H⟩⟩

FormalConjectures/ForMathlib/Computability/TuringMachine/PostTuringMachine.lean

@@ -66,13 +66,13 @@ theorem eval_dom_iff {σ : Type*} {f : σ → Option σ} {s : σ} :
   refine ⟨fun ⟨n, hn⟩ ↦ ?_, fun H ↦ ?_⟩
   · induction n generalizing s with
     | zero =>
-      rw [zero_add, Function.iterate_one, Option.some_bind] at hn
+      rw [zero_add, Function.iterate_one, Option.bind_some] at hn
       simpa [Part.dom_iff_mem] using ⟨s, dom_of_apply_eq_none hn⟩
     | succ n ih =>
       obtain ha | ⟨a', ha'⟩ := (f s).eq_none_or_eq_some
       · simpa [Part.dom_iff_mem] using ⟨s, dom_of_apply_eq_none ha⟩
-      · simp_rw [Function.iterate_succ, Function.comp_apply, Option.some_bind] at hn ih
-        simp_rw [ha', Option.some_bind] at hn
+      · simp_rw [Function.iterate_succ, Function.comp_apply, Option.bind_some] at hn ih
+        simp_rw [ha', Option.bind_some] at hn
         have ih := @ih a' ⟨n, hn⟩ hn
         rwa [Turing.eval_eq_eval ha']
   · let C (s) : Prop := (Turing.eval f s).Dom → ∃ n, (Option.bind · f)^[n+1] s = none
@@ -83,7 +83,7 @@ theorem eval_dom_iff {σ : Type*} {f : σ → Option σ} {s : σ} :
       simp [ha]
     · obtain ⟨n, hn⟩ := h a' ha' (by rwa [←Turing.eval_eq_eval ha'])
       use n + 1
-      simp only [Function.iterate_succ, Function.comp_apply, Option.some_bind] at hn
+      simp only [Function.iterate_succ, Function.comp_apply, Option.bind_some] at hn
       simp [ha', hn]
 
 end Turing

FormalConjectures/ForMathlib/Data/Finset/Empty.lean

@@ -0,0 +1,25 @@
+/-
+Copyright 2025 The Formal Conjectures Authors.
+
+Licensed under the Apache License, Version 2.0 (the "License");
+you may not use this file except in compliance with the License.
+You may obtain a copy of the License at
+
+    https://www.apache.org/licenses/LICENSE-2.0
+
+Unless required by applicable law or agreed to in writing, software
+distributed under the License is distributed on an "AS IS" BASIS,
+WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+See the License for the specific language governing permissions and
+limitations under the License.
+-/
+
+import Mathlib.Data.Finset.Empty
+
+@[simp]
+theorem Finset.univ_finset_of_isEmpty {α : Type*} [h : IsEmpty α] :
+    (Set.univ : Set (Finset α)) = {∅} := by
+  ext S
+  rw [Set.mem_singleton_iff, eq_true (Set.mem_univ S), true_iff]
+  ext a
+  exact IsEmpty.elim h a

FormalConjectures/ForMathlib/Data/Nat/Factorization/Basic.lean

@@ -24,7 +24,7 @@ theorem prod_primeFactors_factorization_apply (n : ℕ) {p : ℕ} (hp : p.Prime)
   rw [factorization_prod fun _ _ _ ↦ by simp_all, Finset.sum_congr rfl fun x hx ↦ by
       rw [factorization_pow, (mem_primeFactors.1 hx).1.factorization]]
   by_cases hpn : p ∣ n <;> simp [Finsupp.single_apply, hp, hpn]
-  · exact fun _ ↦ by simp_all [hf₀]
+  · exact fun _ ↦ by simp_all
   · simp [hf _ _ hpn]
 
 end Nat

FormalConjectures/ForMathlib/Data/Real/Constants.lean

@@ -14,7 +14,7 @@ See the License for the specific language governing permissions and
 limitations under the License.
 -/
 
-import Mathlib.MeasureTheory.Integral.Bochner
+import Mathlib.MeasureTheory.Integral.Bochner.Basic
 import Mathlib.MeasureTheory.Measure.Haar.OfBasis
 
 /-! # Standard real valued constants

FormalConjectures/ForMathlib/Data/Set/Triplewise.lean

@@ -54,13 +54,13 @@ theorem triplewise_of_encard_lt (r : α → α → α → Prop)
   contrapose! h
   obtain ⟨x, hx, y, hy, z, hz, hxy, hyz, hxz, _⟩ := h
   trans encard {x, y, z}
-  · norm_num [encard_insert_of_not_mem, *]
+  · norm_num [encard_insert_of_notMem, *]
   · exact encard_le_encard_of_injOn (by simp [MapsTo, hx, hy, hz]) (injOn_id _)
 
 @[simp]
 theorem triplewise_empty (r : α → α → α → Prop) :
     Set.Triplewise ∅ r :=
-  (not_mem_empty · · |>.elim)
+  (notMem_empty · · |>.elim)
 
 @[simp]
 theorem triplewise_singleton (r : α → α → α → Prop) :

FormalConjectures/Util/ForMathlib.lean

@@ -34,6 +34,7 @@ import FormalConjectures.ForMathlib.Combinatorics.SimpleGraph.GraphConjectures.I
 import FormalConjectures.ForMathlib.Combinatorics.SimpleGraph.Balanced
 import FormalConjectures.ForMathlib.Computability.TuringMachine.BusyBeavers
 import FormalConjectures.ForMathlib.Computability.TuringMachine.PostTuringMachine
+import FormalConjectures.ForMathlib.Data.Finset.Empty
 import FormalConjectures.ForMathlib.Data.Finset.OrdConnected
 import FormalConjectures.ForMathlib.Data.Nat.Factorization.Basic
 import FormalConjectures.ForMathlib.Data.Nat.Full

FormalConjectures/Wikipedia/Conway99Graph.lean

@@ -30,7 +30,6 @@ open SimpleGraph
 
 variable {V : Type} {G : SimpleGraph V}
 
-
 @[category undergraduate, AMS 5]
 lemma completeGraphIsClique (s : Finset V) : (⊤ : SimpleGraph V).IsClique s :=
   Pairwise.set_pairwise (fun _ _ a ↦ a) _
@@ -40,7 +39,7 @@ variable [Fintype V]
 @[category undergraduate, AMS 5]
 lemma completeGraph_cliqueSet :
     (⊤ : SimpleGraph V).cliqueSet (Fintype.card V) = {Set.univ.toFinset} := by
-  simp only [SimpleGraph.cliqueSet, SimpleGraph.isNClique_iff ⊤, completeGraphIsClique, true_and,
+  simp only [cliqueSet, isNClique_iff ⊤, completeGraphIsClique, true_and,
     Set.toFinset_univ]
   exact (Set.Sized.univ_mem_iff fun ⦃x⦄ a ↦ a).mp rfl
 
@@ -71,9 +70,9 @@ The triangle is an example with 3 vertices satisfying the condition.
 theorem triangle_locallyLinear_and_nonEdgesAreDiagonals : (completeGraph (Fin 3)).LocallyLinear ∧
     NonEdgesAreDiagonals (completeGraph (Fin 3)) := by
   constructor
-  · simp [SimpleGraph.LocallyLinear]
+  · simp [LocallyLinear]
     constructor
-    · simp only [SimpleGraph.EdgeDisjointTriangles, Set.Pairwise]
+    · simp only [EdgeDisjointTriangles, Set.Pairwise]
       intro x hx y hy hxy
       have := @completeGraph_cliqueSet (Fin 3) _
       rw [Fintype.card_fin] at this
@@ -101,15 +100,14 @@ theorem conway9_nonEdgesAreDiagonals : NonEdgesAreDiagonals Conway9 := by
     exact Fintype.ofFinite ↑(Conway9.neighborSet i)
   have : ∀ i j, ((Conway9.neighborFinset i) ∩ Conway9.neighborFinset j).card =
     (Conway9.neighborSet i ∩ Conway9.neighborSet j).ncard := by
-    simp only [SimpleGraph.neighborFinset]
+    simp only [neighborFinset]
     intros
     rw [← Set.toFinset_inter, Set.ncard_eq_toFinset_card']
   simp only [← this]
   intro x y
   have ⟨x1, x2⟩ := x
   have ⟨y1, y2⟩ := y
-  simp only [Conway9, SimpleGraph.completeGraph_eq_top,
-    SimpleGraph.boxProd_adj, SimpleGraph.top_adj, SimpleGraph.neighborFinset_boxProd]
+  simp only [Conway9, completeGraph_eq_top, boxProd_adj, top_adj, neighborFinset_boxProd]
   fin_cases x1 <;> fin_cases x2 <;> fin_cases y1 <;> fin_cases y2 <;> decide
 
 @[category API, AMS 5]
@@ -121,9 +119,9 @@ lemma completeGraph_boxProd_completeGraph_cliqueSet :
 
 @[category test, AMS 5]
 theorem conway9_locallyLinear : Conway9.LocallyLinear := by
-  dsimp [SimpleGraph.LocallyLinear]
+  dsimp [LocallyLinear]
   constructor
-  · simp only [SimpleGraph.EdgeDisjointTriangles, Set.Pairwise]
+  · simp only [EdgeDisjointTriangles, Set.Pairwise]
     intro x hx y hy hxy
     simp only [Conway9, completeGraph_boxProd_completeGraph_cliqueSet] at hx hy
     rcases hx with hx | hx <;>
@@ -142,15 +140,15 @@ theorem conway9_locallyLinear : Conway9.LocallyLinear := by
     intro h
     use {(x1, x2), (y1, y2), (x1 + x1 + y1 + y1, x2 + x2 + y2 + y2)}
     simp only [Finset.mem_insert, Prod.mk.injEq, true_or, or_true, and_true]
-    simp only [Conway9, SimpleGraph.completeGraph_eq_top, SimpleGraph.boxProd_adj,
-      SimpleGraph.top_adj, ne_eq] at h ⊢
+    simp only [Conway9, completeGraph_eq_top, boxProd_adj, top_adj, ne_eq] at h ⊢
     constructor
-    · dsimp [SimpleGraph.IsClique, ]
+    · dsimp [IsClique]
       fin_cases x1 <;> fin_cases x2 <;> fin_cases y1 <;> fin_cases y2 <;>
       simp only [Fin.reduceFinMk,  not_true_eq_false, Fin.reduceEq, or_true, Fin.reduceAdd,
-        Finset.coe_insert, Finset.coe_singleton, SimpleGraph.isClique_insert,
-        Set.pairwise_singleton, Set.mem_singleton_iff, ne_eq, SimpleGraph.boxProd_adj,
-        SimpleGraph.top_adj, forall_eq, Prod.mk.injEq, and_false, imp_self, Set.mem_insert_iff,forall_eq_or_imp, or_false, and_true, not_false_eq_true] at h ⊢
+        Finset.coe_insert, Finset.coe_singleton, isClique_insert,
+        Set.pairwise_singleton, Set.mem_singleton_iff, ne_eq, boxProd_adj,
+        top_adj, forall_eq, Prod.mk.injEq, and_false, imp_self, Set.mem_insert_iff,
+        forall_eq_or_imp, or_false, and_true, not_false_eq_true] at h ⊢
     · fin_cases x1 <;> fin_cases x2 <;> fin_cases y1 <;> fin_cases y2 <;>
       simp only [not_true_eq_false, or_self, and_true] at h <;>
       decide