Bump mathlib

Polyhedral.lean

@@ -13,8 +13,6 @@ public import Polyhedral.Mathlib.Algebra.Module.Submodule.Hyperplane
 public import Polyhedral.Mathlib.Algebra.Module.Submodule.Map
 public import Polyhedral.Mathlib.Algebra.Module.Submodule.Restrict
 public import Polyhedral.Mathlib.Algebra.Module.Submodule.SubMulActionWithZero
-public import Polyhedral.Mathlib.Algebra.Order.Nonneg.Basic
-public import Polyhedral.Mathlib.Algebra.Order.Nonneg.DivisionRing
 public import Polyhedral.Mathlib.Algebra.Order.Nonneg.Ring
 public import Polyhedral.Mathlib.Data.Finsupp.Basic
 public import Polyhedral.Mathlib.Data.Finsupp.Option

Polyhedral/Mathlib/Algebra/Order/Nonneg/Ring.lean

@@ -5,7 +5,7 @@ Authors: Martin Winter
 -/
 module
 
-public import Polyhedral.Mathlib.Algebra.Order.Nonneg.Basic
+public import Mathlib.Algebra.Order.Nonneg.Basic
 public import Mathlib.Algebra.Order.Ring.Defs
 
 /-!

Polyhedral/Mathlib/Geometry/Convex/Cone/Pointed/Basic.lean

@@ -7,7 +7,7 @@ module
 
 public import Mathlib.Geometry.Convex.Cone.Pointed
 public import Polyhedral.Mathlib.Algebra.Module.Submodule.Basic
-public import Polyhedral.Mathlib.Algebra.Order.Nonneg.Basic
+public import Mathlib.Algebra.Order.Nonneg.Basic
 
 import Mathlib.RingTheory.LocalRing.Basic
 
@@ -207,76 +207,6 @@ lemma comap_neg_apply (C : PointedCone R M) (f : N →ₗ[R] M) : -comap f C = c
 
 end PartialOrder
 
-section DirectedOrderRing
-
-/- NOTE: This section is mathlib PR #36605. Delete it after PR is merged. -/
-
-open Submodule
-
-variable {R : Type*} [Ring R] [PartialOrder R] [IsDirectedOrder R] [IsOrderedRing R]
-variable {E : Type*} [AddCommGroup E] [Module R E]
-
-variable {C : PointedCone R E} {x : E}
-
-/-- A cone that is closed under negation forms a submodule. -/
-abbrev toSubmodule (hC : -C = C) : Submodule R E where
-  __ := C
-  smul_mem' a x hx := by
-    obtain ⟨b, hab, hb⟩ := exists_ge_ge a 0
-    suffices b • x + -(b - a) • x ∈ C by
-      rw [← add_smul] at this
-      abel_nf at this
-      exact this
-    have : -(b - a) • x ∈ C := by
-      rw [← hC]
-      simpa [← neg_smul] using smul_mem _ (sub_nonneg.mpr hab) hx
-    aesop
-
-@[simp] lemma ofSubmodule_toSubmodule (hC : -C = C) : C.toSubmodule hC = C := rfl
-
-lemma coe_toSubmodule (hC : -C = C) : (C.toSubmodule hC : Set E) = C := by simp
-
-lemma mem_toSubmodule {hC : -C = C} : x ∈ C.toSubmodule hC ↔ x ∈ C := by simp
-
-instance : CanLift (PointedCone R E) (Submodule R E) ofSubmodule (fun C => -C = C) where
-  prf _ h := ⟨toSubmodule h, ofSubmodule_toSubmodule h⟩
-
-variable (R)
-
-lemma span_eq_hull_neg_sup_hull (s : Set E) : span R s = hull R (-s) ⊔ hull R s := by
-  suffices span R s = (hull R (-s) ⊔ hull R s).toSubmodule
-    (by simp [← span_neg_eq_neg, sup_comm]) by simp [this]
-  refine span_eq_of_le _ (fun x hx ↦ ?_) ?_
-  · simpa using mem_sup_right (Submodule.subset_span hx)
-  · rw [← ofSubmodule_le_ofSubmodule]
-    simpa [hull_le_span] using hull_le_span R (-s)
-
-variable (x) in
-@[simp] lemma hull_neg_pair_eq_span_singleton : hull R {-x, x} = R ∙ x := by
-  change hull R ({-x} ∪ {x}) = (R ∙ x)
-  simp only [span_union, span_eq_hull_neg_sup_hull, Set.neg_singleton]
-
-lemma hull_eq_span_of_neg_eq {s : Set E} (hs : -s = s) :
-    hull R s = span R s := by
-  simp [span_eq_hull_neg_sup_hull, hs]
-
-variable {R}
-
-variable (C) in
-lemma span_eq_neg_sup : span R (C : Set E) = -C ⊔ C := by
-  simp [span_eq_hull_neg_sup_hull, span_neg_eq_neg]
-
-lemma mem_span_iff_mem_neg_sup : x ∈ span R C ↔ x ∈ -C ⊔ C := by
-  rw [← span_eq_neg_sup, mem_ofSubmodule_iff]
-
-lemma mem_span : x ∈ span R C ↔ ∃ p ∈ C, ∃ n ∈ C, x = p - n := by
-  simp_rw [mem_span_iff_mem_neg_sup, mem_sup, mem_neg]
-  refine ⟨fun ⟨y, hy', z, hz, h⟩ ↦ ?_, fun ⟨p, hp, n, hn, h⟩ ↦ ?_⟩
-  · exact ⟨z, hz, -y, hy', by grind⟩
-  · exact ⟨-n, by simp [hn], x + n, by simp [h, hp], by simp⟩
-
-end DirectedOrderRing
-
 section PartialOrder
 
 variable {R M : Type*} [Ring R] [PartialOrder R] [IsOrderedRing R] [AddCommGroup M] [Module R M]

Polyhedral/Mathlib/LinearAlgebra/AffineSpace/AffineSubspace/Basic.lean

@@ -40,17 +40,8 @@ instance : IsConcreteEmpty (AffineSubspace R A) A := ⟨rfl⟩
 
 lemma AffineSubspace.affineSpan_empty : affineSpan R (∅ : Set A) = ∅ := by simp
 
-instance : Singleton A (AffineSubspace R A) where
-  singleton x := {
-    carrier := {x}
-    smul_vsub_vadd_mem' _ _ _ _ := by simp +contextual }
-
 instance : IsConcreteSingleton (AffineSubspace R A) A := ⟨fun _ => rfl⟩
 
-@[simp]
-lemma AffineSubspace.affineSpan_singleton (x : A) : affineSpan R ({x} : Set A) = {x} := by
-  ext; simp
-
 instance : IsConcreteTop (AffineSubspace R A) A := ⟨rfl⟩
 
 end AddTorsor

Polyhedral/Mathlib/LinearAlgebra/AffineSpace/Homogenization/Set.lean

@@ -10,7 +10,7 @@ public import Polyhedral.Mathlib.LinearAlgebra.AffineSpace.Homogenization.Basic
 
 import Polyhedral.Mathlib.Data.Set.Lattice.Image
 import Polyhedral.Mathlib.Algebra.Order.Nonneg.Ring
-import Polyhedral.Mathlib.Algebra.Order.Nonneg.DivisionRing
+import Mathlib.Algebra.Order.Nonneg.Field
 
 /-! This file defines homogenization of general sets. The homogenization is of type
 `SubMulAction₀ R≥0 W`, which is closed under multiplication and always contains zero.

lake-manifest.json

@@ -5,7 +5,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "738f2ab17ae4e57b2b668d2f913280b67582712c",
+   "rev": "38f65a093a9e4a3436fcae95c625c40931d80a85",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -55,7 +55,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "d8823026ac7ef130c253089d95685f9877b95323",
+   "rev": "1681d78dd6e65e38b143f9740d829c826673807c",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -95,7 +95,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "7e23602c91bc04586b2b06de2708a041853e4681",
+   "rev": "4cac2177c37f5530c4da76aa8e4307f3fc9e4dcb",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",