merge master

Author: kim-em

Mathlib.lean

@@ -2128,6 +2128,7 @@ import Mathlib.CategoryTheory.Iso
 import Mathlib.CategoryTheory.IsomorphismClasses
 import Mathlib.CategoryTheory.Join.Basic
 import Mathlib.CategoryTheory.Join.Final
+import Mathlib.CategoryTheory.Join.Opposites
 import Mathlib.CategoryTheory.Join.Sum
 import Mathlib.CategoryTheory.LiftingProperties.Adjunction
 import Mathlib.CategoryTheory.LiftingProperties.Basic
@@ -6093,6 +6094,7 @@ import Mathlib.Topology.CompactOpen
 import Mathlib.Topology.Compactification.OnePoint
 import Mathlib.Topology.Compactification.OnePoint.Basic
 import Mathlib.Topology.Compactification.OnePoint.ProjectiveLine
+import Mathlib.Topology.Compactification.OnePoint.Sphere
 import Mathlib.Topology.Compactification.OnePointEquiv
 import Mathlib.Topology.Compactness.Bases
 import Mathlib.Topology.Compactness.Compact

Mathlib/Algebra/BigOperators/Group/Finset/Basic.lean

@@ -72,7 +72,7 @@ theorem prod_pair [DecidableEq ι] {a b : ι} (h : a ≠ b) :
 
 @[to_additive (attr := simp)]
 theorem prod_image [DecidableEq ι] {s : Finset κ} {g : κ → ι} :
-    (∀ x ∈ s, ∀ y ∈ s, g x = g y → x = y) → ∏ x ∈ s.image g, f x = ∏ x ∈ s, f (g x) :=
+    Set.InjOn g s → ∏ x ∈ s.image g, f x = ∏ x ∈ s, f (g x) :=
   fold_image
 
 @[to_additive]

Mathlib/Algebra/BigOperators/Group/Finset/Preimage.lean

@@ -26,7 +26,7 @@ lemma prod_preimage' (f : ι → κ) [DecidablePred (· ∈ Set.range f)] (s : F
   classical
   calc
     ∏ x ∈ preimage s f hf, g (f x) = ∏ x ∈ image f (preimage s f hf), g x :=
-      Eq.symm <| prod_image <| by simpa only [mem_preimage, Set.InjOn] using hf
+      Eq.symm <| prod_image <| by simpa [mem_preimage, Set.InjOn] using hf
     _ = ∏ x ∈ s with x ∈ Set.range f, g x := by rw [image_preimage]
 
 @[to_additive]

Mathlib/Algebra/BigOperators/Intervals.lean

@@ -147,7 +147,7 @@ theorem prod_Ico_reflect (f : ℕ → M) (k : ℕ) {m n : ℕ} (h : m ≤ n + 1)
   rcases lt_or_le k m with hkm | hkm
   · rw [← Nat.Ico_image_const_sub_eq_Ico (this _ hkm)]
     refine (prod_image ?_).symm
-    simp only [mem_Ico]
+    simp only [mem_Ico, Set.InjOn, mem_coe]
     rintro i ⟨_, im⟩ j ⟨_, jm⟩ Hij
     rw [← tsub_tsub_cancel_of_le (this _ im), Hij, tsub_tsub_cancel_of_le (this _ jm)]
   · have : n + 1 - k ≤ n + 1 - m := by

Mathlib/Algebra/CharP/Invertible.lean

@@ -67,9 +67,8 @@ theorem CharP.isUnit_intCast_iff {z : ℤ} (hp : p.Prime) : IsUnit (z : R) ↔ 
 
 end Ring
 
-section Field
-
-variable [Field K]
+section Semifield
+variable [Semifield K]
 
 /-- A natural number `t` is invertible in a field `K` if the characteristic of `K` does not divide
 `t`. -/
@@ -90,11 +89,10 @@ def invertibleOfCharPNotDvd {p : ℕ} [CharP K p] {t : ℕ} (not_dvd : ¬p ∣ t
 instance invertibleOfPos [CharZero K] (n : ℕ) [NeZero n] : Invertible (n : K) :=
   invertibleOfNonzero <| NeZero.out
 
-end Field
-
-section DivisionRing
+end Semifield
 
-variable [DivisionRing K] [CharZero K]
+section DivisionSemiring
+variable [DivisionSemiring K] [CharZero K]
 
 instance invertibleSucc (n : ℕ) : Invertible (n.succ : K) :=
   invertibleOfNonzero (Nat.cast_ne_zero.mpr (Nat.succ_ne_zero _))
@@ -111,4 +109,4 @@ instance invertibleTwo : Invertible (2 : K) :=
 instance invertibleThree : Invertible (3 : K) :=
   invertibleOfNonzero (mod_cast (by decide : 3 ≠ 0))
 
-end DivisionRing
+end DivisionSemiring

Mathlib/Algebra/Group/Submonoid/Basic.lean

@@ -302,7 +302,7 @@ theorem disjoint_def' {p₁ p₂ : Submonoid M} :
 
 variable {t : Set M}
 
-@[to_additive (attr := simp)]
+@[to_additive] -- this must not be a simp-lemma as the conclusion applies to `hts`, causing loops
 lemma closure_sdiff_eq_closure (hts : t ⊆ closure (s \ t)) : closure (s \ t) = closure s := by
   refine (closure_mono Set.diff_subset).antisymm <| closure_le.mpr <| fun x hxs ↦ ?_
   by_cases hxt : x ∈ t

Mathlib/Algebra/GroupWithZero/Basic.lean

@@ -262,14 +262,14 @@ theorem GroupWithZero.mul_left_injective (h : x ≠ 0) :
     Function.Injective fun y => y * x := fun y y' w => by
   simpa only [mul_assoc, mul_inv_cancel₀ h, mul_one] using congr_arg (fun y => y * x⁻¹) w
 
-@[simp]
+@[simp high] -- should take priority over `IsUnit.mul_inv_cancel_right`
 theorem inv_mul_cancel_right₀ (h : b ≠ 0) (a : G₀) : a * b⁻¹ * b = a :=
   calc
     a * b⁻¹ * b = a * (b⁻¹ * b) := mul_assoc _ _ _
     _ = a := by simp [h]
 
 
-@[simp]
+@[simp high] -- should take priority over `IsUnit.mul_inv_cancel_left`
 theorem inv_mul_cancel_left₀ (h : a ≠ 0) (b : G₀) : a⁻¹ * (a * b) = b :=
   calc
     a⁻¹ * (a * b) = a⁻¹ * a * b := (mul_assoc _ _ _).symm

Mathlib/Algebra/GroupWithZero/Defs.lean

@@ -205,7 +205,7 @@ variable [GroupWithZero G₀] {a : G₀}
 
 @[simp] lemma inv_zero : (0 : G₀)⁻¹ = 0 := GroupWithZero.inv_zero
 
-@[simp]
+@[simp high] -- should take priority over `IsUnit.mul_inv_cancel`
 lemma mul_inv_cancel₀ (h : a ≠ 0) : a * a⁻¹ = 1 := GroupWithZero.mul_inv_cancel a h
 
 -- See note [lower instance priority]
@@ -232,13 +232,13 @@ section GroupWithZero
 
 variable [GroupWithZero G₀] {a b : G₀}
 
-@[simp]
+@[simp high] -- should take priority over `IsUnit.mul_inv_cancel_right`
 theorem mul_inv_cancel_right₀ (h : b ≠ 0) (a : G₀) : a * b * b⁻¹ = a :=
   calc
     a * b * b⁻¹ = a * (b * b⁻¹) := mul_assoc _ _ _
     _ = a := by simp [h]
 
-@[simp]
+@[simp high] -- should take priority over `IsUnit.mul_inv_cancel_left`
 theorem mul_inv_cancel_left₀ (h : a ≠ 0) (b : G₀) : a * (a⁻¹ * b) = b :=
   calc
     a * (a⁻¹ * b) = a * a⁻¹ * b := (mul_assoc _ _ _).symm

Mathlib/Algebra/GroupWithZero/NeZero.lean

@@ -48,7 +48,7 @@ theorem inv_ne_zero (h : a ≠ 0) : a⁻¹ ≠ 0 := fun a_eq_0 => by
   have := mul_inv_cancel₀ h
   simp only [a_eq_0, mul_zero, zero_ne_one] at this
 
-@[simp]
+@[simp high] -- should take priority over `IsUnit.inv_mul_cancel`
 theorem inv_mul_cancel₀ (h : a ≠ 0) : a⁻¹ * a = 1 :=
   calc
     a⁻¹ * a = a⁻¹ * a * a⁻¹ * a⁻¹⁻¹ := by simp [inv_ne_zero h]

Mathlib/Algebra/Homology/DifferentialObject.lean

@@ -41,14 +41,18 @@ abbrev objEqToHom {i j : β} (h : i = j) :
 theorem objEqToHom_refl (i : β) : X.objEqToHom (refl i) = 𝟙 _ :=
   rfl
 
-@[reassoc (attr := simp)]
+-- Removing `@[simp]`, because it is in the opposite direction of `eqToHom_naturality`.
+-- Having both causes an infinite loop in the simpNF linter.
+@[reassoc]
 theorem objEqToHom_d {x y : β} (h : x = y) :
     X.objEqToHom h ≫ X.d y = X.d x ≫ X.objEqToHom (by cases h; rfl) := by cases h; simp
 
 @[reassoc (attr := simp)]
 theorem d_squared_apply {x : β} : X.d x ≫ X.d _ = 0 := congr_fun X.d_squared _
 
-@[reassoc (attr := simp)]
+-- Removing `@[simp]`, because it is in the opposite direction of `eqToHom_naturality`.
+-- Having both causes an infinite loop in the simpNF linter.
+@[reassoc]
 theorem eqToHom_f' {X Y : DifferentialObject ℤ (GradedObjectWithShift b V)} (f : X ⟶ Y) {x y : β}
     (h : x = y) : X.objEqToHom h ≫ f.f y = f.f x ≫ Y.objEqToHom h := by cases h; simp
 
@@ -79,7 +83,7 @@ def dgoToHomologicalComplex :
       shape := fun i j w => by dsimp at w; convert dif_neg w
       d_comp_d' := fun i j k hij hjk => by
         dsimp at hij hjk; substs hij hjk
-        simp }
+        simp [objEqToHom_d_assoc] }
   map {X Y} f :=
     { f := f.f
       comm' := fun i j h => by