bump to nightly-2023-05-16-22

mathlib commit leanprover-community/mathlib@0b9eaaa

Mathbin/Analysis/Convex/Hull.lean

@@ -290,7 +290,7 @@ variable [AddCommGroup E] [AddCommGroup F] [Module 𝕜 E] [Module 𝕜 F] (s :
 lean 3 declaration is
   forall {𝕜 : Type.{u1}} {E : Type.{u2}} {F : Type.{u3}} [_inst_1 : OrderedRing.{u1} 𝕜] [_inst_2 : AddCommGroup.{u2} E] [_inst_3 : AddCommGroup.{u3} F] [_inst_4 : Module.{u1, u2} 𝕜 E (Ring.toSemiring.{u1} 𝕜 (OrderedRing.toRing.{u1} 𝕜 _inst_1)) (AddCommGroup.toAddCommMonoid.{u2} E _inst_2)] [_inst_5 : Module.{u1, u3} 𝕜 F (Ring.toSemiring.{u1} 𝕜 (OrderedRing.toRing.{u1} 𝕜 _inst_1)) (AddCommGroup.toAddCommMonoid.{u3} F _inst_3)] (s : Set.{u2} E) (f : AffineMap.{u1, u2, u2, u3, u3} 𝕜 E E F F (OrderedRing.toRing.{u1} 𝕜 _inst_1) _inst_2 _inst_4 (addGroupIsAddTorsor.{u2} E (AddCommGroup.toAddGroup.{u2} E _inst_2)) _inst_3 _inst_5 (addGroupIsAddTorsor.{u3} F (AddCommGroup.toAddGroup.{u3} F _inst_3))), Eq.{succ u3} (Set.{u3} F) (Set.image.{u2, u3} E F (coeFn.{max (succ u2) (succ u3), max (succ u2) (succ u3)} (AffineMap.{u1, u2, u2, u3, u3} 𝕜 E E F F (OrderedRing.toRing.{u1} 𝕜 _inst_1) _inst_2 _inst_4 (addGroupIsAddTorsor.{u2} E (AddCommGroup.toAddGroup.{u2} E _inst_2)) _inst_3 _inst_5 (addGroupIsAddTorsor.{u3} F (AddCommGroup.toAddGroup.{u3} F _inst_3))) (fun (_x : AffineMap.{u1, u2, u2, u3, u3} 𝕜 E E F F (OrderedRing.toRing.{u1} 𝕜 _inst_1) _inst_2 _inst_4 (addGroupIsAddTorsor.{u2} E (AddCommGroup.toAddGroup.{u2} E _inst_2)) _inst_3 _inst_5 (addGroupIsAddTorsor.{u3} F (AddCommGroup.toAddGroup.{u3} F _inst_3))) => E -> F) (AffineMap.hasCoeToFun.{u1, u2, u2, u3, u3} 𝕜 E E F F (OrderedRing.toRing.{u1} 𝕜 _inst_1) _inst_2 _inst_4 (addGroupIsAddTorsor.{u2} E (AddCommGroup.toAddGroup.{u2} E _inst_2)) _inst_3 _inst_5 (addGroupIsAddTorsor.{u3} F (AddCommGroup.toAddGroup.{u3} F _inst_3))) f) (coeFn.{succ u2, succ u2} (ClosureOperator.{u2} (Set.{u2} E) (PartialOrder.toPreorder.{u2} (Set.{u2} E) (CompleteSemilatticeInf.toPartialOrder.{u2} (Set.{u2} E) (CompleteLattice.toCompleteSemilatticeInf.{u2} (Set.{u2} E) (Order.Coframe.toCompleteLattice.{u2} (Set.{u2} E) (CompleteDistribLattice.toCoframe.{u2} (Set.{u2} E) (CompleteBooleanAlgebra.toCompleteDistribLattice.{u2} (Set.{u2} E) (Set.completeBooleanAlgebra.{u2} E)))))))) (fun (_x : ClosureOperator.{u2} (Set.{u2} E) (PartialOrder.toPreorder.{u2} (Set.{u2} E) (CompleteSemilatticeInf.toPartialOrder.{u2} (Set.{u2} E) (CompleteLattice.toCompleteSemilatticeInf.{u2} (Set.{u2} E) (Order.Coframe.toCompleteLattice.{u2} (Set.{u2} E) (CompleteDistribLattice.toCoframe.{u2} (Set.{u2} E) (CompleteBooleanAlgebra.toCompleteDistribLattice.{u2} (Set.{u2} E) (Set.completeBooleanAlgebra.{u2} E)))))))) => (Set.{u2} E) -> (Set.{u2} E)) (ClosureOperator.hasCoeToFun.{u2} (Set.{u2} E) (PartialOrder.toPreorder.{u2} (Set.{u2} E) (CompleteSemilatticeInf.toPartialOrder.{u2} (Set.{u2} E) (CompleteLattice.toCompleteSemilatticeInf.{u2} (Set.{u2} E) (Order.Coframe.toCompleteLattice.{u2} (Set.{u2} E) (CompleteDistribLattice.toCoframe.{u2} (Set.{u2} E) (CompleteBooleanAlgebra.toCompleteDistribLattice.{u2} (Set.{u2} E) (Set.completeBooleanAlgebra.{u2} E)))))))) (convexHull.{u1, u2} 𝕜 E (OrderedRing.toOrderedSemiring.{u1} 𝕜 _inst_1) (AddCommGroup.toAddCommMonoid.{u2} E _inst_2) _inst_4) s)) (coeFn.{succ u3, succ u3} (ClosureOperator.{u3} (Set.{u3} F) (PartialOrder.toPreorder.{u3} (Set.{u3} F) (CompleteSemilatticeInf.toPartialOrder.{u3} (Set.{u3} F) (CompleteLattice.toCompleteSemilatticeInf.{u3} (Set.{u3} F) (Order.Coframe.toCompleteLattice.{u3} (Set.{u3} F) (CompleteDistribLattice.toCoframe.{u3} (Set.{u3} F) (CompleteBooleanAlgebra.toCompleteDistribLattice.{u3} (Set.{u3} F) (Set.completeBooleanAlgebra.{u3} F)))))))) (fun (_x : ClosureOperator.{u3} (Set.{u3} F) (PartialOrder.toPreorder.{u3} (Set.{u3} F) (CompleteSemilatticeInf.toPartialOrder.{u3} (Set.{u3} F) (CompleteLattice.toCompleteSemilatticeInf.{u3} (Set.{u3} F) (Order.Coframe.toCompleteLattice.{u3} (Set.{u3} F) (CompleteDistribLattice.toCoframe.{u3} (Set.{u3} F) (CompleteBooleanAlgebra.toCompleteDistribLattice.{u3} (Set.{u3} F) (Set.completeBooleanAlgebra.{u3} F)))))))) => (Set.{u3} F) -> (Set.{u3} F)) (ClosureOperator.hasCoeToFun.{u3} (Set.{u3} F) (PartialOrder.toPreorder.{u3} (Set.{u3} F) (CompleteSemilatticeInf.toPartialOrder.{u3} (Set.{u3} F) (CompleteLattice.toCompleteSemilatticeInf.{u3} (Set.{u3} F) (Order.Coframe.toCompleteLattice.{u3} (Set.{u3} F) (CompleteDistribLattice.toCoframe.{u3} (Set.{u3} F) (CompleteBooleanAlgebra.toCompleteDistribLattice.{u3} (Set.{u3} F) (Set.completeBooleanAlgebra.{u3} F)))))))) (convexHull.{u1, u3} 𝕜 F (OrderedRing.toOrderedSemiring.{u1} 𝕜 _inst_1) (AddCommGroup.toAddCommMonoid.{u3} F _inst_3) _inst_5) (Set.image.{u2, u3} E F (coeFn.{max (succ u2) (succ u3), max (succ u2) (succ u3)} (AffineMap.{u1, u2, u2, u3, u3} 𝕜 E E F F (OrderedRing.toRing.{u1} 𝕜 _inst_1) _inst_2 _inst_4 (addGroupIsAddTorsor.{u2} E (AddCommGroup.toAddGroup.{u2} E _inst_2)) _inst_3 _inst_5 (addGroupIsAddTorsor.{u3} F (AddCommGroup.toAddGroup.{u3} F _inst_3))) (fun (_x : AffineMap.{u1, u2, u2, u3, u3} 𝕜 E E F F (OrderedRing.toRing.{u1} 𝕜 _inst_1) _inst_2 _inst_4 (addGroupIsAddTorsor.{u2} E (AddCommGroup.toAddGroup.{u2} E _inst_2)) _inst_3 _inst_5 (addGroupIsAddTorsor.{u3} F (AddCommGroup.toAddGroup.{u3} F _inst_3))) => E -> F) (AffineMap.hasCoeToFun.{u1, u2, u2, u3, u3} 𝕜 E E F F (OrderedRing.toRing.{u1} 𝕜 _inst_1) _inst_2 _inst_4 (addGroupIsAddTorsor.{u2} E (AddCommGroup.toAddGroup.{u2} E _inst_2)) _inst_3 _inst_5 (addGroupIsAddTorsor.{u3} F (AddCommGroup.toAddGroup.{u3} F _inst_3))) f) s))
 but is expected to have type
-  forall {𝕜 : Type.{u3}} {E : Type.{u2}} {F : Type.{u1}} [_inst_1 : OrderedRing.{u3} 𝕜] [_inst_2 : AddCommGroup.{u2} E] [_inst_3 : AddCommGroup.{u1} F] [_inst_4 : Module.{u3, u2} 𝕜 E (OrderedSemiring.toSemiring.{u3} 𝕜 (OrderedRing.toOrderedSemiring.{u3} 𝕜 _inst_1)) (AddCommGroup.toAddCommMonoid.{u2} E _inst_2)] [_inst_5 : Module.{u3, u1} 𝕜 F (OrderedSemiring.toSemiring.{u3} 𝕜 (OrderedRing.toOrderedSemiring.{u3} 𝕜 _inst_1)) (AddCommGroup.toAddCommMonoid.{u1} F _inst_3)] (s : Set.{u2} E) (f : AffineMap.{u3, u2, u2, u1, u1} 𝕜 E E F F (OrderedRing.toRing.{u3} 𝕜 _inst_1) _inst_2 _inst_4 (addGroupIsAddTorsor.{u2} E (AddCommGroup.toAddGroup.{u2} E _inst_2)) _inst_3 _inst_5 (addGroupIsAddTorsor.{u1} F (AddCommGroup.toAddGroup.{u1} F _inst_3))), Eq.{succ u1} (Set.{u1} F) (Set.image.{u2, u1} E F (FunLike.coe.{max (succ u2) (succ u1), succ u2, succ u1} (AffineMap.{u3, u2, u2, u1, u1} 𝕜 E E F F (OrderedRing.toRing.{u3} 𝕜 _inst_1) _inst_2 _inst_4 (addGroupIsAddTorsor.{u2} E (AddCommGroup.toAddGroup.{u2} E _inst_2)) _inst_3 _inst_5 (addGroupIsAddTorsor.{u1} F (AddCommGroup.toAddGroup.{u1} F _inst_3))) E (fun (_x : E) => (fun (a._@.Mathlib.LinearAlgebra.AffineSpace.AffineMap._hyg.1004 : E) => F) _x) (AffineMap.funLike.{u3, u2, u2, u1, u1} 𝕜 E E F F (OrderedRing.toRing.{u3} 𝕜 _inst_1) _inst_2 _inst_4 (addGroupIsAddTorsor.{u2} E (AddCommGroup.toAddGroup.{u2} E _inst_2)) _inst_3 _inst_5 (addGroupIsAddTorsor.{u1} F (AddCommGroup.toAddGroup.{u1} F _inst_3))) f) (OrderHom.toFun.{u2, u2} (Set.{u2} E) (Set.{u2} E) (PartialOrder.toPreorder.{u2} (Set.{u2} E) (OmegaCompletePartialOrder.toPartialOrder.{u2} (Set.{u2} E) (CompleteLattice.instOmegaCompletePartialOrder.{u2} (Set.{u2} E) (Order.Coframe.toCompleteLattice.{u2} (Set.{u2} E) (CompleteDistribLattice.toCoframe.{u2} (Set.{u2} E) (CompleteBooleanAlgebra.toCompleteDistribLattice.{u2} (Set.{u2} E) (Set.instCompleteBooleanAlgebraSet.{u2} E))))))) (PartialOrder.toPreorder.{u2} (Set.{u2} E) (OmegaCompletePartialOrder.toPartialOrder.{u2} (Set.{u2} E) (CompleteLattice.instOmegaCompletePartialOrder.{u2} (Set.{u2} E) (Order.Coframe.toCompleteLattice.{u2} (Set.{u2} E) (CompleteDistribLattice.toCoframe.{u2} (Set.{u2} E) (CompleteBooleanAlgebra.toCompleteDistribLattice.{u2} (Set.{u2} E) (Set.instCompleteBooleanAlgebraSet.{u2} E))))))) (ClosureOperator.toOrderHom.{u2} (Set.{u2} E) (PartialOrder.toPreorder.{u2} (Set.{u2} E) (OmegaCompletePartialOrder.toPartialOrder.{u2} (Set.{u2} E) (CompleteLattice.instOmegaCompletePartialOrder.{u2} (Set.{u2} E) (Order.Coframe.toCompleteLattice.{u2} (Set.{u2} E) (CompleteDistribLattice.toCoframe.{u2} (Set.{u2} E) (CompleteBooleanAlgebra.toCompleteDistribLattice.{u2} (Set.{u2} E) (Set.instCompleteBooleanAlgebraSet.{u2} E))))))) (convexHull.{u3, u2} 𝕜 E (OrderedRing.toOrderedSemiring.{u3} 𝕜 _inst_1) (AddCommGroup.toAddCommMonoid.{u2} E _inst_2) _inst_4)) s)) (OrderHom.toFun.{u1, u1} (Set.{u1} F) (Set.{u1} F) (PartialOrder.toPreorder.{u1} (Set.{u1} F) (OmegaCompletePartialOrder.toPartialOrder.{u1} (Set.{u1} F) (CompleteLattice.instOmegaCompletePartialOrder.{u1} (Set.{u1} F) (Order.Coframe.toCompleteLattice.{u1} (Set.{u1} F) (CompleteDistribLattice.toCoframe.{u1} (Set.{u1} F) (CompleteBooleanAlgebra.toCompleteDistribLattice.{u1} (Set.{u1} F) (Set.instCompleteBooleanAlgebraSet.{u1} F))))))) (PartialOrder.toPreorder.{u1} (Set.{u1} F) (OmegaCompletePartialOrder.toPartialOrder.{u1} (Set.{u1} F) (CompleteLattice.instOmegaCompletePartialOrder.{u1} (Set.{u1} F) (Order.Coframe.toCompleteLattice.{u1} (Set.{u1} F) (CompleteDistribLattice.toCoframe.{u1} (Set.{u1} F) (CompleteBooleanAlgebra.toCompleteDistribLattice.{u1} (Set.{u1} F) (Set.instCompleteBooleanAlgebraSet.{u1} F))))))) (ClosureOperator.toOrderHom.{u1} (Set.{u1} F) (PartialOrder.toPreorder.{u1} (Set.{u1} F) (OmegaCompletePartialOrder.toPartialOrder.{u1} (Set.{u1} F) (CompleteLattice.instOmegaCompletePartialOrder.{u1} (Set.{u1} F) (Order.Coframe.toCompleteLattice.{u1} (Set.{u1} F) (CompleteDistribLattice.toCoframe.{u1} (Set.{u1} F) (CompleteBooleanAlgebra.toCompleteDistribLattice.{u1} (Set.{u1} F) (Set.instCompleteBooleanAlgebraSet.{u1} F))))))) (convexHull.{u3, u1} 𝕜 F (OrderedRing.toOrderedSemiring.{u3} 𝕜 _inst_1) (AddCommGroup.toAddCommMonoid.{u1} F _inst_3) _inst_5)) (Set.image.{u2, u1} E F (FunLike.coe.{max (succ u2) (succ u1), succ u2, succ u1} (AffineMap.{u3, u2, u2, u1, u1} 𝕜 E E F F (OrderedRing.toRing.{u3} 𝕜 _inst_1) _inst_2 _inst_4 (addGroupIsAddTorsor.{u2} E (AddCommGroup.toAddGroup.{u2} E _inst_2)) _inst_3 _inst_5 (addGroupIsAddTorsor.{u1} F (AddCommGroup.toAddGroup.{u1} F _inst_3))) E (fun (_x : E) => (fun (a._@.Mathlib.LinearAlgebra.AffineSpace.AffineMap._hyg.1004 : E) => F) _x) (AffineMap.funLike.{u3, u2, u2, u1, u1} 𝕜 E E F F (OrderedRing.toRing.{u3} 𝕜 _inst_1) _inst_2 _inst_4 (addGroupIsAddTorsor.{u2} E (AddCommGroup.toAddGroup.{u2} E _inst_2)) _inst_3 _inst_5 (addGroupIsAddTorsor.{u1} F (AddCommGroup.toAddGroup.{u1} F _inst_3))) f) s))
+  forall {𝕜 : Type.{u3}} {E : Type.{u2}} {F : Type.{u1}} [_inst_1 : OrderedRing.{u3} 𝕜] [_inst_2 : AddCommGroup.{u2} E] [_inst_3 : AddCommGroup.{u1} F] [_inst_4 : Module.{u3, u2} 𝕜 E (OrderedSemiring.toSemiring.{u3} 𝕜 (OrderedRing.toOrderedSemiring.{u3} 𝕜 _inst_1)) (AddCommGroup.toAddCommMonoid.{u2} E _inst_2)] [_inst_5 : Module.{u3, u1} 𝕜 F (OrderedSemiring.toSemiring.{u3} 𝕜 (OrderedRing.toOrderedSemiring.{u3} 𝕜 _inst_1)) (AddCommGroup.toAddCommMonoid.{u1} F _inst_3)] (s : Set.{u2} E) (f : AffineMap.{u3, u2, u2, u1, u1} 𝕜 E E F F (OrderedRing.toRing.{u3} 𝕜 _inst_1) _inst_2 _inst_4 (addGroupIsAddTorsor.{u2} E (AddCommGroup.toAddGroup.{u2} E _inst_2)) _inst_3 _inst_5 (addGroupIsAddTorsor.{u1} F (AddCommGroup.toAddGroup.{u1} F _inst_3))), Eq.{succ u1} (Set.{u1} F) (Set.image.{u2, u1} E F (FunLike.coe.{max (succ u2) (succ u1), succ u2, succ u1} (AffineMap.{u3, u2, u2, u1, u1} 𝕜 E E F F (OrderedRing.toRing.{u3} 𝕜 _inst_1) _inst_2 _inst_4 (addGroupIsAddTorsor.{u2} E (AddCommGroup.toAddGroup.{u2} E _inst_2)) _inst_3 _inst_5 (addGroupIsAddTorsor.{u1} F (AddCommGroup.toAddGroup.{u1} F _inst_3))) E (fun (_x : E) => (fun (a._@.Mathlib.LinearAlgebra.AffineSpace.AffineMap._hyg.1003 : E) => F) _x) (AffineMap.funLike.{u3, u2, u2, u1, u1} 𝕜 E E F F (OrderedRing.toRing.{u3} 𝕜 _inst_1) _inst_2 _inst_4 (addGroupIsAddTorsor.{u2} E (AddCommGroup.toAddGroup.{u2} E _inst_2)) _inst_3 _inst_5 (addGroupIsAddTorsor.{u1} F (AddCommGroup.toAddGroup.{u1} F _inst_3))) f) (OrderHom.toFun.{u2, u2} (Set.{u2} E) (Set.{u2} E) (PartialOrder.toPreorder.{u2} (Set.{u2} E) (OmegaCompletePartialOrder.toPartialOrder.{u2} (Set.{u2} E) (CompleteLattice.instOmegaCompletePartialOrder.{u2} (Set.{u2} E) (Order.Coframe.toCompleteLattice.{u2} (Set.{u2} E) (CompleteDistribLattice.toCoframe.{u2} (Set.{u2} E) (CompleteBooleanAlgebra.toCompleteDistribLattice.{u2} (Set.{u2} E) (Set.instCompleteBooleanAlgebraSet.{u2} E))))))) (PartialOrder.toPreorder.{u2} (Set.{u2} E) (OmegaCompletePartialOrder.toPartialOrder.{u2} (Set.{u2} E) (CompleteLattice.instOmegaCompletePartialOrder.{u2} (Set.{u2} E) (Order.Coframe.toCompleteLattice.{u2} (Set.{u2} E) (CompleteDistribLattice.toCoframe.{u2} (Set.{u2} E) (CompleteBooleanAlgebra.toCompleteDistribLattice.{u2} (Set.{u2} E) (Set.instCompleteBooleanAlgebraSet.{u2} E))))))) (ClosureOperator.toOrderHom.{u2} (Set.{u2} E) (PartialOrder.toPreorder.{u2} (Set.{u2} E) (OmegaCompletePartialOrder.toPartialOrder.{u2} (Set.{u2} E) (CompleteLattice.instOmegaCompletePartialOrder.{u2} (Set.{u2} E) (Order.Coframe.toCompleteLattice.{u2} (Set.{u2} E) (CompleteDistribLattice.toCoframe.{u2} (Set.{u2} E) (CompleteBooleanAlgebra.toCompleteDistribLattice.{u2} (Set.{u2} E) (Set.instCompleteBooleanAlgebraSet.{u2} E))))))) (convexHull.{u3, u2} 𝕜 E (OrderedRing.toOrderedSemiring.{u3} 𝕜 _inst_1) (AddCommGroup.toAddCommMonoid.{u2} E _inst_2) _inst_4)) s)) (OrderHom.toFun.{u1, u1} (Set.{u1} F) (Set.{u1} F) (PartialOrder.toPreorder.{u1} (Set.{u1} F) (OmegaCompletePartialOrder.toPartialOrder.{u1} (Set.{u1} F) (CompleteLattice.instOmegaCompletePartialOrder.{u1} (Set.{u1} F) (Order.Coframe.toCompleteLattice.{u1} (Set.{u1} F) (CompleteDistribLattice.toCoframe.{u1} (Set.{u1} F) (CompleteBooleanAlgebra.toCompleteDistribLattice.{u1} (Set.{u1} F) (Set.instCompleteBooleanAlgebraSet.{u1} F))))))) (PartialOrder.toPreorder.{u1} (Set.{u1} F) (OmegaCompletePartialOrder.toPartialOrder.{u1} (Set.{u1} F) (CompleteLattice.instOmegaCompletePartialOrder.{u1} (Set.{u1} F) (Order.Coframe.toCompleteLattice.{u1} (Set.{u1} F) (CompleteDistribLattice.toCoframe.{u1} (Set.{u1} F) (CompleteBooleanAlgebra.toCompleteDistribLattice.{u1} (Set.{u1} F) (Set.instCompleteBooleanAlgebraSet.{u1} F))))))) (ClosureOperator.toOrderHom.{u1} (Set.{u1} F) (PartialOrder.toPreorder.{u1} (Set.{u1} F) (OmegaCompletePartialOrder.toPartialOrder.{u1} (Set.{u1} F) (CompleteLattice.instOmegaCompletePartialOrder.{u1} (Set.{u1} F) (Order.Coframe.toCompleteLattice.{u1} (Set.{u1} F) (CompleteDistribLattice.toCoframe.{u1} (Set.{u1} F) (CompleteBooleanAlgebra.toCompleteDistribLattice.{u1} (Set.{u1} F) (Set.instCompleteBooleanAlgebraSet.{u1} F))))))) (convexHull.{u3, u1} 𝕜 F (OrderedRing.toOrderedSemiring.{u3} 𝕜 _inst_1) (AddCommGroup.toAddCommMonoid.{u1} F _inst_3) _inst_5)) (Set.image.{u2, u1} E F (FunLike.coe.{max (succ u2) (succ u1), succ u2, succ u1} (AffineMap.{u3, u2, u2, u1, u1} 𝕜 E E F F (OrderedRing.toRing.{u3} 𝕜 _inst_1) _inst_2 _inst_4 (addGroupIsAddTorsor.{u2} E (AddCommGroup.toAddGroup.{u2} E _inst_2)) _inst_3 _inst_5 (addGroupIsAddTorsor.{u1} F (AddCommGroup.toAddGroup.{u1} F _inst_3))) E (fun (_x : E) => (fun (a._@.Mathlib.LinearAlgebra.AffineSpace.AffineMap._hyg.1003 : E) => F) _x) (AffineMap.funLike.{u3, u2, u2, u1, u1} 𝕜 E E F F (OrderedRing.toRing.{u3} 𝕜 _inst_1) _inst_2 _inst_4 (addGroupIsAddTorsor.{u2} E (AddCommGroup.toAddGroup.{u2} E _inst_2)) _inst_3 _inst_5 (addGroupIsAddTorsor.{u1} F (AddCommGroup.toAddGroup.{u1} F _inst_3))) f) s))
 Case conversion may be inaccurate. Consider using '#align affine_map.image_convex_hull AffineMap.image_convexHullₓ'. -/
 theorem AffineMap.image_convexHull (f : E →ᵃ[𝕜] F) : f '' convexHull 𝕜 s = convexHull 𝕜 (f '' s) :=
   by