Reduce diff to nightly-testing-2024-08-09

Mathlib/Algebra/Quaternion.lean

@@ -198,9 +198,6 @@ instance : Add ℍ[R,c₁,c₂] :=
 
 @[simp] theorem add_imK : (a + b).imK = a.imK + b.imK := rfl
 
-@[simp] theorem add_im : (a + b).im = a.im + b.im :=
-  QuaternionAlgebra.ext (zero_add _).symm rfl rfl rfl
-
 @[simp]
 theorem mk_add_mk (a₁ a₂ a₃ a₄ b₁ b₂ b₃ b₄ : R) :
     (mk a₁ a₂ a₃ a₄ : ℍ[R,c₁,c₂]) + mk b₁ b₂ b₃ b₄ = mk (a₁ + b₁) (a₂ + b₂) (a₃ + b₃) (a₄ + b₄) :=
@@ -233,9 +230,6 @@ instance : Neg ℍ[R,c₁,c₂] := ⟨fun a => ⟨-a.1, -a.2, -a.3, -a.4⟩⟩
 
 @[simp] theorem neg_imK : (-a).imK = -a.imK := rfl
 
-@[simp] theorem neg_im : (-a).im = -a.im :=
-  QuaternionAlgebra.ext neg_zero.symm rfl rfl rfl
-
 @[simp]
 theorem neg_mk (a₁ a₂ a₃ a₄ : R) : -(mk a₁ a₂ a₃ a₄ : ℍ[R,c₁,c₂]) = ⟨-a₁, -a₂, -a₃, -a₄⟩ :=
   rfl
@@ -286,6 +280,11 @@ theorem sub_self_im : a - a.im = a.re :=
 theorem sub_self_re : a - a.re = a.im :=
   QuaternionAlgebra.ext (sub_self _) (sub_zero _) (sub_zero _) (sub_zero _)
 
+end AddGroup
+
+section Ring
+variable [Ring R]
+
 /-- Multiplication is given by
 
 * `1 * x = x * 1 = x`;
@@ -343,7 +342,7 @@ instance [SMulCommClass S T R] : SMulCommClass S T ℍ[R,c₁,c₂] where
 
 @[simp] theorem smul_imK : (s • a).imK = s • a.imK := rfl
 
-@[simp] theorem smul_im {S} [SMulZeroClass S R] (s : S) : (s • a).im = s • a.im :=
+@[simp] theorem smul_im {S} [CommRing R] [SMulZeroClass S R] (s : S) : (s • a).im = s • a.im :=
   QuaternionAlgebra.ext (smul_zero s).symm rfl rfl rfl
 
 @[simp]

Mathlib/AlgebraicGeometry/Properties.lean

@@ -230,7 +230,7 @@ instance irreducibleSpace_of_isIntegral [IsIntegral X] : IrreducibleSpace X := b
     · rintro ⟨hS, hT⟩
       cases' h₁ (show x ∈ ⊤ by trivial) with h h
       exacts [hS h, hT h]
-    · exact False.elim
+    · simp
 
 theorem isIntegral_of_irreducibleSpace_of_isReduced [IsReduced X] [H : IrreducibleSpace X] :
     IsIntegral X := by

Mathlib/Combinatorics/SimpleGraph/Hamiltonian.lean

@@ -84,8 +84,8 @@ lemma IsHamiltonianCycle.map {H : SimpleGraph β} (f : G →g H) (hf : Bijective
     intro x
     rcases p with (_ | ⟨y, p⟩)
     · cases hp.ne_nil rfl
-    simp only [support_cons, List.count_cons, List.map_cons, List.head_cons, beq_iff_eq,
-      hf.injective.eq_iff, add_tsub_cancel_right]
+    simp only [support_cons, List.count_cons, beq_iff_eq, List.head_cons, hf.injective.eq_iff,
+      add_tsub_cancel_right]
     exact hp.isHamiltonian_tail _
 
 lemma isHamiltonianCycle_isCycle_and_isHamiltonian_tail  :

Mathlib/Combinatorics/SimpleGraph/Walk.lean

@@ -901,7 +901,7 @@ theorem count_edges_takeUntil_le_one {u v w : V} (p : G.Walk v w) (h : u ∈ p.s
         simp
       · rw [edges_cons, List.count_cons]
         split_ifs with h''
-        · simp only [beq_iff_eq, Sym2.eq, Sym2.rel_iff'] at h''
+        · simp only [beq_iff_eq, Sym2.eq, Sym2.rel_iff', Prod.mk.injEq, Prod.swap_prod_mk] at h''
           obtain ⟨rfl, rfl⟩ | ⟨rfl, rfl⟩ := h''
           · exact (h' rfl).elim
           · cases p' <;> simp!

Mathlib/Data/List/Perm.lean

@@ -250,9 +250,9 @@ theorem perm_replicate_append_replicate {l : List α} {a b : α} {m n : ℕ} (h
 theorem Perm.dedup {l₁ l₂ : List α} (p : l₁ ~ l₂) : dedup l₁ ~ dedup l₂ :=
   perm_iff_count.2 fun a =>
     if h : a ∈ l₁ then by
-      simp [nodup_dedup, h, p.subset h]
+      simp [h, nodup_dedup, p.subset h]
     else by
-      simp [mem_dedup, h, not_false_eq_true, count_eq_zero_of_not_mem, mt p.mem_iff.2 h]
+      simp [h, count_eq_zero_of_not_mem, mt p.mem_iff.2]
 
 theorem Perm.inter_append {l t₁ t₂ : List α} (h : Disjoint t₁ t₂) :
     l ∩ (t₁ ++ t₂) ~ l ∩ t₁ ++ l ∩ t₂ := by

lake-manifest.json

@@ -5,10 +5,10 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "8a09d5093af15b69775e17993d00406d0416243f",
+   "rev": "9cf9bd609587e4b56ec6fc05b36e82065fada39e",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "nightly-testing-2024-07-09",
+   "inputRev": "nightly-testing",
    "inherited": false,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/quote4",
@@ -45,20 +45,20 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "a11566029bd9ec4f68a65394e8c3ff1af74c1a29",
+   "rev": "2cf1030dc2ae6b3632c84a09350b675ef3e347d0",
    "name": "Cli",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
    "inherited": true,
-   "configFile": "lakefile.lean"},
+   "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/import-graph",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "033082103b7b53f35ccee18702a995382503d6ef",
+   "rev": "57bd2065f1dbea5e9235646fb836c7cea9ab03b6",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "nightly-testing",
+   "inputRev": "main",
    "inherited": false,
    "configFile": "lakefile.toml"}],
  "name": "mathlib",

lakefile.lean

@@ -17,11 +17,11 @@ package mathlib where
 ## Mathlib dependencies on upstream projects.
 -/
 
-require "leanprover-community" / "batteries" @ "git#nightly-testing-2024-07-09"
-require "leanprover-community" / "Qq" @ "git#master"
-require "leanprover-community" / "aesop" @ "git#master"
-require "leanprover-community" / "proofwidgets" @ "git#v0.0.40"
-require "leanprover-community" / "importGraph" @ "git#nightly-testing"
+require "leanprover-community" / "batteries" @ git "nightly-testing"
+require "leanprover-community" / "Qq" @ git "nightly-testing"
+require "leanprover-community" / "aesop" @ git "nightly-testing"
+require "leanprover-community" / "proofwidgets" @ git "v0.0.42-pre2"
+require "leanprover-community" / "importGraph" @ git "main"
 
 /-!
 ## Mathlib libraries