Bump mathlib

Polyhedral.lean

@@ -68,10 +68,8 @@ public import Polyhedral.Mathlib.GroupTheory.GroupAction.SubMulActionWithZero
 public import Polyhedral.Mathlib.GroupTheory.GroupAction.SubMulActionWithZero.Closure
 public import Polyhedral.Mathlib.GroupTheory.GroupAction.SubMulActionWithZero.Nonneg
 public import Polyhedral.Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
-public import Polyhedral.Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
 public import Polyhedral.Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Range
 public import Polyhedral.Mathlib.LinearAlgebra.AffineSpace.Defs
-public import Polyhedral.Mathlib.LinearAlgebra.AffineSpace.Dimension
 public import Polyhedral.Mathlib.LinearAlgebra.AffineSpace.Homogenization.IsHomogenization
 public import Polyhedral.Mathlib.LinearAlgebra.AffineSpace.Homogenization.Set
 public import Polyhedral.Mathlib.LinearAlgebra.AffineSpace.Lattice

Polyhedral/Mathlib/Algebra/Group/Pointwise/SetLike/Basic.lean

@@ -12,7 +12,7 @@ import Mathlib.Algebra.Group.Equiv.Basic
 import Mathlib.Algebra.Group.Prod
 import Mathlib.Algebra.Order.Monoid.Unbundled.Pow
 import Mathlib.Data.Set.NAry
-import Mathlib.Data.SetLike.Basic
+import Mathlib.Basic.SetLike.Basic
 import Mathlib.Algebra.Group.Defs
 
 /-! This files defines the pointwise operations on `SetLike` that are inherited from `Set`-/

Polyhedral/Mathlib/Data/SetLike/IsConcrete.lean

@@ -5,7 +5,7 @@ Authors: Martin Winter
 -/
 module
 
-public import Mathlib.Data.SetLike.Basic
+public import Mathlib.Basic.SetLike.Basic
 public import Mathlib.Order.CompleteLattice.Defs
 
 import Mathlib.Data.Set.Basic

Polyhedral/Mathlib/Geometry/Convex/AffineMap/Module.lean

@@ -8,29 +8,9 @@ public section
 open Convexity
 open scoped Pointwise
 
-namespace LinearMap
-variable {R M N : Type*} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] [AddCommMonoid M]
-  [Module R M] [AddCommMonoid N] [Module R N] [ConvexSpace R M] [IsModuleConvexSpace R M]
-  [ConvexSpace R N] [IsModuleConvexSpace R N] (f : M →ₗ[R] N)
-
-alias isAffineMap := IsAffineMap.linearMap
-
-@[simp] lemma map_sConvexComb (w : StdSimplex R M) :
-    f (sConvexComb w) = sConvexComb (w.map f) := f.isAffineMap.map_sConvexComb w
-
-lemma isConvexSet_image {s : Set M} (hs : IsConvexSet R s) : IsConvexSet R (f '' s) :=
-  hs.image f.isAffineMap
-
-lemma isConvexSet_range : IsConvexSet R (Set.range f) := by
-  rw [← Set.image_univ]
-  exact isConvexSet_image f .univ
-
-end LinearMap
-
 namespace Convexity
 variable {R S M : Type*}
 
-
 section Semiring
 variable [Ring R] [PartialOrder R] [IsStrictOrderedRing R] [AddCommGroup M]
   [Module R M] [ConvexSpace R M] [IsModuleConvexSpace R M] {K K₁ K₂ : Set M}
@@ -40,7 +20,8 @@ protected lemma IsConvexSet.add (hK₁ : IsConvexSet R K₁) (hK₂ : IsConvexSe
 
 variable [DistribSMul S M] [SMulCommClass R S M]
 
-lemma isAffineMap_smul (s : S) : IsAffineMap R fun x : M ↦ s • x := (s • LinearMap.id).isAffineMap
+lemma isAffineMap_smul (s : S) : IsAffineMap R fun x : M ↦ s • x :=
+  IsAffineMap.linearMap (s • LinearMap.id : M →ₗ[R] M)
 
 protected lemma IsConvexSet.smul (s : S) {K : Set M} (hK : IsConvexSet R K) :
     IsConvexSet R (s • K) := by rw [← Set.image_smul]; exact hK.image (isAffineMap_smul s)
@@ -53,7 +34,7 @@ variable [Ring R] [PartialOrder R] [IsStrictOrderedRing R] [AddCommGroup M]
 
 protected lemma IsConvexSet.neg (hK : IsConvexSet R K) : IsConvexSet R (-K) := by
   rw [← Set.image_neg_eq_neg]
-  exact hK.image (LinearEquiv.neg R).toLinearMap.isAffineMap
+  exact hK.image (.linearMap (LinearEquiv.neg R).toLinearMap)
 
 @[simp] lemma isConvexSet_neg : IsConvexSet R (-K) ↔ IsConvexSet R K where
   mp h := by simpa using h.neg

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

@@ -10,7 +10,7 @@ public import Polyhedral.Mathlib.Algebra.Module.Submodule.Basic
 public import Mathlib.Algebra.Order.Nonneg.Basic
 
 import Mathlib.RingTheory.LocalRing.Basic
-import Polyhedral.Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
+import Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
 
 /-! This file proves basic facts about cones that are intended to go into Pointed/Basic. -/
 

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

@@ -215,7 +215,7 @@ lemma dual_eq_bot_iff_forall_eq_zero_or_exists_neg :
 lemma dual_dual_eq_top_iff_exists_ne_zero_forall_nonneg :
     dual p.flip (dual p C) ≠ ⊤ ↔ ∃ φ : N, p.flip φ ≠ 0 ∧ ∀ x ∈ C, 0 ≤ p x φ := by
   constructor <;> intro h
-  · obtain ⟨x, hx⟩ := SetLike.exists_not_mem_of_ne_top _ h
+  · obtain ⟨x, hx⟩ := SetLike.exists_notMem_of_ne_top _ h
     obtain ⟨φ, hxφ, hφ⟩ := farkas (dual_dualClosed _ _) hx
     use φ
     constructor

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

@@ -148,7 +148,7 @@ lemma span_inf_of_codisjoint_lineal {S : Submodule R M} (hS : Codisjoint C.linea
     span R (C ⊓ S : PointedCone R M) = span R C ⊓ S := by
   nth_rw 2 [← C.inf_sup_lineal hS]
   rw [← coe_sup_submodule_span, Submodule.span_union, coe_ofSubmodule, Submodule.span_eq C.lineal]
-  rw [sup_inf_assoc_of_le C.lineal (Submodule.span_le.mpr fun _ hx ↦ hx.2)]
+  rw [sup_inf_assoc_of_le C.lineal (Submodule.span_le.mpr (by simp))]
   rw [Eq.comm, sup_eq_left]
   intro x hx
   apply Submodule.subset_span

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

@@ -1,13 +1,13 @@
 /-
-Copyright (c) 2025 Olivia Röhig, Kilian Rueß, Mrtin Winter. All rights reserved.
+Copyright (c) 2025 Olivia Röhig, Kilian Rueß, Martin Winter. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Olivia Röhig, Kilian Rueß, Mrtin Winter
+Authors: Olivia Röhig, Kilian Rueß, Martin Winter
 -/
 module
 
+public import Mathlib.LinearAlgebra.AffineSpace.Dimension
 public import Polyhedral.Mathlib.Geometry.Convex.Cone.Pointed.Lineal
 public import Polyhedral.Mathlib.Algebra.Module.Submodule.Dual.Field
-public import Polyhedral.Mathlib.LinearAlgebra.AffineSpace.Dimension
 
 /-!
 ## Rank of Pointed Cones

Polyhedral/Mathlib/Geometry/Convex/ConvexSpace/AffineSpace.lean

@@ -26,33 +26,6 @@ public section
 open Convexity Finset AddTorsor
 open scoped Pointwise
 
-namespace AffineMap
-variable {R V₁ V₂ P₁ P₂ : Type*}
-variable [Ring R] [PartialOrder R] [IsStrictOrderedRing R]
-variable [AddCommGroup V₁] [Module R V₁] [AddTorsor V₁ P₁]
-variable [AddCommGroup V₂] [Module R V₂] [AddTorsor V₂ P₂]
-variable [ConvexSpace R P₁] [IsAffineConvexSpace R V₁ P₁]
-variable [ConvexSpace R P₂] [IsAffineConvexSpace R V₂ P₂]
-variable (f : P₁ →ᵃ[R] P₂)
-
--- PR #39437
-lemma isAffineMap : IsAffineMap R f where
-  map_sConvexComb s := by
-    rw [sConvexComb_eq_affineCombination, sConvexComb_map, iConvexComb_eq_affineCombination]
-    simpa only [Function.comp_id] using
-      map_affineCombination (s := s.weights.support) _root_.id s.weights s.total f
-
-@[simp] lemma map_sConvexComb (w : StdSimplex R P₁) :
-    f (sConvexComb w) = sConvexComb (w.map f) := f.isAffineMap.map_sConvexComb w
-
-lemma isConvexSet_image {s : Set P₁} (hs : IsConvexSet R s) : IsConvexSet R (f '' s) :=
-  hs.image f.isAffineMap
-
-lemma isConvexSet_range : IsConvexSet R (Set.range f) := by
-  simpa using f.isConvexSet_image .univ
-
-end AffineMap
-
 namespace Convexity
 variable {R V P I : Type*}
 variable [Ring R] [PartialOrder R] [IsStrictOrderedRing R]

Polyhedral/Mathlib/Geometry/Convex/ConvexSpace/Homogenization.lean

@@ -79,7 +79,6 @@ variable (hom) in
 embedding of the set. -/
 theorem image_hull_eq_convexHull_image {s : Set A} :
     ℋ.ofPoint '' Convexity.convexHull R s ⊆ hull R (ℋ.ofPoint '' s) := by
-  apply Set.image_subset_iff.mp
   rw [ℋ.ofPoint.isAffineMap.image_convexHull]
   simpa using (hull R _).isConvexSet.convexHull_subset_iff.mpr subset_hull
 

Polyhedral/Mathlib/Geometry/Convex/ConvexSpace/Set/Face/Basic.lean

@@ -170,9 +170,7 @@ theorem isFaceOf_map_iff {f : M₁ → M₂} {F C : ConvexSet R M₁} (hhf : IsA
         rw [hf hzy] at hy
         use hy
       · intro hz
-        have hhz : f z ∈ (A.map hhf) := by
-          use z, hz
-        apply Set.mem_preimage.mp hhz
+        exact ⟨z, hz, rfl⟩
     rw [h F, h C] at hh
     exact hh
   · intro h

Polyhedral/Mathlib/Geometry/Convex/ConvexSpace/Set/Face/Homogenization.lean

@@ -11,7 +11,7 @@ public import Polyhedral.Mathlib.Geometry.Convex.ConvexSpace.Set.Homogenization
 
 /-! This files proves results about faces of convex sets / cones and homogenization. -/
 
-@[expose] public section
+@[expose] public noncomputable section
 
 namespace Affine.IsHomogenization
 

Polyhedral/Mathlib/Geometry/Convex/ConvexSpace/Set/Homogenization.lean

@@ -11,7 +11,7 @@ public import Polyhedral.Mathlib.LinearAlgebra.AffineSpace.Homogenization.IsHomo
 
 /-! This file defines homogenization of convex sets in affine spaces. -/
 
-@[expose] public section
+@[expose] public noncomputable section
 
 open Convexity Pointwise Set PointedCone Submodule
 
@@ -228,7 +228,7 @@ theorem homogenize_dehomogenize_of_le_positive {C : PointedCone R W}
         simpa [y', ℋ.ofPoint_range_eq_comap_weight_one]
           using inv_mul_cancel₀ (@hC y hyC hy0).ne.symm
       exact ⟨y', hy'C, hy'⟩
-    · exact C.isConvexSet.inter ℋ.ofPoint.isConvexSet_range
+    · exact C.isConvexSet.inter (.range ℋ.ofPoint.isAffineMap)
 
 lemma homogenize_mono_iff {K₁ K₂ : ConvexSet R A} :
     K₁.homogenize ℋ ≤ K₂.homogenize ℋ ↔ K₁ ≤ K₂ where

Polyhedral/Mathlib/Geometry/Convex/Fun/Defs.lean

@@ -53,7 +53,7 @@ See `IsConvexFunOn.of_map_convexCombPair_le`.
 
 Under mild assumptions, convexity of the function `f` implies convexity of the set `s`.
 See `IsConvexFunOn.isConvexSet`. -/
-@[to_dual IsConcaveFunOn
+@[to_dual (dont_translate := R) IsConcaveFunOn
 /-- A function `f : X → Y` from a convex space to an ordered convex space is concave on a set `s`
 if its hypograph `{(x, y) : X × Y | x ∈ s ∧ y ≤ f x}` is a convex set.
 
@@ -64,7 +64,7 @@ Under mild assumptions, concavity of the function `f` implies convexity of the s
 See `IsConcaveFunOn.isConvexSet`. -/]
 def IsConvexFunOn : Prop := IsConvexSet R {(x, y) : X × Y | x ∈ s ∧ f x ≤ y}
 
-@[to_dual]
+@[to_dual (dont_translate := R)]
 lemma IsConvexFunOn.isConvexSet_epigraph (hf : IsConvexFunOn R s f) :
     IsConvexSet R {(x, y) : X × Y | x ∈ s ∧ f x ≤ y} := hf
 
@@ -80,7 +80,7 @@ lemma IsConvexFunOn.isConvexSet (hf : IsConvexFunOn R s f) : IsConvexSet R s :=
     grw [StdSimplex.weights_map, mapDomain_support]; simpa
   simpa [Function.comp_def] using (hf.isConvexSet_epigraph.sConvexComb_mem this).1
 
-@[to_dual le_map_sConvexComb]
+@[to_dual (dont_translate := R) le_map_sConvexComb]
 lemma IsConvexFunOn.map_sConvexComb_le (hf : IsConvexFunOn R s f) {w : StdSimplex R X}
     (hw : ↑w.weights.support ⊆ s) :
     f w.sConvexComb ≤ w.iConvexComb f := by

Polyhedral/Mathlib/Geometry/Convex/Hull.lean

@@ -31,7 +31,7 @@ For finite `ι`, this can be interpreted as saying that a polytope is the image
 simplex under some affine map. -/
 lemma convexHull_range (f : ι → X) :
     convexHull R (.range f) = .range (fun w : StdSimplex R ι ↦ iConvexComb w f) := by
-  refine (convexHull_min ?_ isAffineMap_iConvexComb.isConvexSet_range).antisymm ?_
+  refine (convexHull_min ?_ (.range isAffineMap_iConvexComb)).antisymm ?_
   · rintro _ ⟨i, rfl⟩
     exact ⟨.single i, by simp⟩
   · rintro _ ⟨w, rfl⟩

Polyhedral/Mathlib/Geometry/Convex/Set.lean

@@ -10,7 +10,7 @@ variable {R X Y Z : Type*} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R]
   [ConvexSpace R X] [ConvexSpace R Y] [ConvexSpace R Z] {f : X → Y} {s : Set X} {t : Set Y}
 
 /-- The range of an affine map between convex spaces is convex. -/
-lemma IsAffineMap.isConvexSet_range (hf : IsAffineMap R f) :
+lemma IsConvexSet.range (hf : IsAffineMap R f) :
     IsConvexSet R (.range f) := by simpa using IsConvexSet.univ.image hf
 
 protected lemma IsConvexSet.image2 {f : X → Y → Z} (hf : IsAffineMap R ↿f)

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

@@ -17,7 +17,7 @@ import Mathlib.Algebra.Order.Nonneg.Field
 In particular, the homogenization is never empty. This enables to prove suitable order
 isomorphisms. -/
 
-@[expose] public section
+@[expose] public noncomputable section
 
 namespace Affine.Set