mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Convex.Cone.Dual

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
inst✝¹³ : CommRing R
inst✝¹² : PartialOrder R
inst✝¹¹ : IsOrderedRing R
inst✝¹⁰ : TopologicalSpace R
inst✝⁹ : ClosedIciTopology R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : TopologicalSpace M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
inst✝³ : TopologicalSpace N
p : M →ₗ[R] N →ₗ[R] R
inst✝² : p.IsContPerfPair
inst✝¹ : IsTopologicalRing R
inst✝ : T1Space N
y : N
hy : y ∈ dual p univ
x : M
⊢ (p x) y ≤ 0

Tactic:
simpa using

Goal state after:
R : Type u_1
M : Type u_2
N : Type u_3
inst✝¹³ : CommRing R
inst✝¹² : PartialOrder R
inst✝¹¹ : IsOrderedRing R
inst✝¹⁰ : TopologicalSpace R
inst✝⁹ : ClosedIciTopology R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : TopologicalSpace M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
inst✝³ : TopologicalSpace N
p : M →ₗ[R] N →ₗ[R] R
inst✝² : p.IsContPerfPair
inst✝¹ : IsTopologicalRing R
inst✝ : T1Space N
y : N
hy : y ∈ dual p univ
x : M
⊢ (p x) y ≤ 0
Module: Mathlib.Analysis.Convex.Cone.Dual

Goal state before:
pp: E : Type u_1
inst✝⁵ : TopologicalSpace E
inst✝⁴ : AddCommGroup E
inst✝³ : IsTopologicalAddGroup E
inst✝² : Module ℝ E
inst✝¹ : ContinuousSMul ℝ E
inst✝ : LocallyConvexSpace ℝ E
K : Set E
C : ProperCone ℝ E
hKconv : Convex ℝ K
hKcomp : IsCompact K
hKC : Disjoint K ↑C
x₀ : E
hx₀ : x₀ ∈ K
f : StrongDual ℝ E
u v : ℝ
hu : ∀ a ∈ K, f a < u
huv : u < v
hv : ∀ b ∈ ↑C, v < f b
⊢ v < 0

Tactic:
simpa using

Goal state after:
E : Type u_1
inst✝⁵ : TopologicalSpace E
inst✝⁴ : AddCommGroup E
inst✝³ : IsTopologicalAddGroup E
inst✝² : Module ℝ E
inst✝¹ : ContinuousSMul ℝ E
inst✝ : LocallyConvexSpace ℝ E
K : Set E
C : ProperCone ℝ E
hKconv : Convex ℝ K
hKcomp : IsCompact K
hKC : Disjoint K ↑C
x₀ : E
hx₀ : x₀ ∈ K
f : StrongDual ℝ E
u v : ℝ
hu : ∀ a ∈ K, f a < u
huv : u < v
hv : ∀ b ∈ ↑C, v < f b
⊢ v < 0
Module: Mathlib.Analysis.Convex.Cone.Dual

Goal state before:
pp: case inr
E : Type u_1
inst✝⁵ : TopologicalSpace E
inst✝⁴ : AddCommGroup E
inst✝³ : IsTopologicalAddGroup E
inst✝² : Module ℝ E
inst✝¹ : ContinuousSMul ℝ E
inst✝ : LocallyConvexSpace ℝ E
K : Set E
C : ProperCone ℝ E
hKconv : Convex ℝ K
hKcomp : IsCompact K
hKC : Disjoint K ↑C
x₀ : E
hx₀✝ : x₀ ∈ K
f : StrongDual ℝ E
u v : ℝ
hu : ∀ a ∈ K, f a < u
huv : u < v
hv : ∀ b ∈ ↑C, v < f b
hv₀ : v < 0
x : E
hx : x ∈ C
hx₀ : f x < 0
⊢ False

Tactic:
simpa using

Goal state after:
case inr
E : Type u_1
inst✝⁵ : TopologicalSpace E
inst✝⁴ : AddCommGroup E
inst✝³ : IsTopologicalAddGroup E
inst✝² : Module ℝ E
inst✝¹ : ContinuousSMul ℝ E
inst✝ : LocallyConvexSpace ℝ E
K : Set E
C : ProperCone ℝ E
hKconv : Convex ℝ K
hKcomp : IsCompact K
hKC : Disjoint K ↑C
x₀ : E
hx₀✝ : x₀ ∈ K
f : StrongDual ℝ E
u v : ℝ
hu : ∀ a ∈ K, f a < u
huv : u < v
hv : ∀ b ∈ ↑C, v < f b
hv₀ : v < 0
x : E
hx : x ∈ C
hx₀ : f x < 0
⊢ False
Module: Mathlib.Analysis.Convex.Cone.Dual

Goal state before:
pp: E : Type u_1
inst✝⁵ : TopologicalSpace E
inst✝⁴ : AddCommGroup E
inst✝³ : IsTopologicalAddGroup E
inst✝² : Module ℝ E
inst✝¹ : ContinuousSMul ℝ E
inst✝ : LocallyConvexSpace ℝ E
x₀ : E
C : ProperCone ℝ E
hx₀ : x₀ ∉ C
⊢ ∃ f, (∀ x ∈ C, 0 ≤ f x) ∧ f x₀ < 0

Tactic:
simpa using

Goal state after:
E : Type u_1
inst✝⁵ : TopologicalSpace E
inst✝⁴ : AddCommGroup E
inst✝³ : IsTopologicalAddGroup E
inst✝² : Module ℝ E
inst✝¹ : ContinuousSMul ℝ E
inst✝ : LocallyConvexSpace ℝ E
x₀ : E
C : ProperCone ℝ E
hx₀ : x₀ ∉ C
⊢ ∃ f, (∀ x ∈ C, 0 ≤ f x) ∧ f x₀ < 0
Module: Mathlib.Analysis.Convex.Cone.Dual

Goal state before:
pp: E : Type u_1
F : Type u_2
inst✝⁹ : TopologicalSpace E
inst✝⁸ : AddCommGroup E
inst✝⁷ : IsTopologicalAddGroup E
inst✝⁶ : TopologicalSpace F
inst✝⁵ : AddCommGroup F
inst✝⁴ : Module ℝ E
inst✝³ : ContinuousSMul ℝ E
inst✝² : LocallyConvexSpace ℝ E
inst✝¹ : Module ℝ F
p : E →ₗ[ℝ] F →ₗ[ℝ] ℝ
inst✝ : p.IsContPerfPair
C : ProperCone ℝ E
x : E
⊢ x ∉ C → ∃ x_1, (∀ ⦃x : E⦄, x ∈ C → 0 ≤ (p x) x_1) ∧ (p.flip x_1) x < 0

Tactic:
simpa using

Goal state after:
E : Type u_1
F : Type u_2
inst✝⁹ : TopologicalSpace E
inst✝⁸ : AddCommGroup E
inst✝⁷ : IsTopologicalAddGroup E
inst✝⁶ : TopologicalSpace F
inst✝⁵ : AddCommGroup F
inst✝⁴ : Module ℝ E
inst✝³ : ContinuousSMul ℝ E
inst✝² : LocallyConvexSpace ℝ E
inst✝¹ : Module ℝ F
p : E →ₗ[ℝ] F →ₗ[ℝ] ℝ
inst✝ : p.IsContPerfPair
C : ProperCone ℝ E
x : E
⊢ x ∉ C → ∃ x_1, (∀ ⦃x : E⦄, x ∈ C → 0 ≤ (p x) x_1) ∧ (p x) x_1 < 0
Module: Mathlib.Geometry.Convex.Cone.TensorProduct

Goal state before:
pp: case refine_1
R : Type u_1
inst✝⁶ : CommRing R
inst✝⁵ : LinearOrder R
inst✝⁴ : IsStrictOrderedRing R
G : Type u_2
inst✝³ : AddCommGroup G
inst✝² : Module R G
H : Type u_3
inst✝¹ : AddCommGroup H
inst✝ : Module R H
C₁ : PointedCone R G
C₂ : PointedCone R H
w : G ⊗[R] H
hw : ∀ φ ∈ dual (Dual.eval R G) ↑C₁, ∀ ψ ∈ dual (Dual.eval R H) ↑C₂, 0 ≤ ((dualDistrib R G H) (φ ⊗ₜ[R] ψ)) w
ψ : Dual R H
hψ : ψ ∈ dual (Dual.eval R H) ↑C₂
φ : Dual R G
hφ : φ ∈ dual (Dual.eval R G) ↑C₁
⊢ 0 ≤ ((dualDistrib R H G) (ψ ⊗ₜ[R] φ)) (↑(TensorProduct.comm R G H) w)

Tactic:
simpa using

Goal state after:
case refine_1
R : Type u_1
inst✝⁶ : CommRing R
inst✝⁵ : LinearOrder R
inst✝⁴ : IsStrictOrderedRing R
G : Type u_2
inst✝³ : AddCommGroup G
inst✝² : Module R G
H : Type u_3
inst✝¹ : AddCommGroup H
inst✝ : Module R H
C₁ : PointedCone R G
C₂ : PointedCone R H
w : G ⊗[R] H
hw : ∀ φ ∈ dual (Dual.eval R G) ↑C₁, ∀ ψ ∈ dual (Dual.eval R H) ↑C₂, 0 ≤ ((dualDistrib R G H) (φ ⊗ₜ[R] ψ)) w
ψ : Dual R H
hψ : ψ ∈ dual (Dual.eval R H) ↑C₂
φ : Dual R G
hφ : φ ∈ dual (Dual.eval R G) ↑C₁
⊢ 0 ≤ ((dualDistrib R G H) (φ ⊗ₜ[R] ψ)) w
Module: Mathlib.Geometry.Convex.Cone.TensorProduct

Goal state before:
pp: case refine_2
R : Type u_1
inst✝⁶ : CommRing R
inst✝⁵ : LinearOrder R
inst✝⁴ : IsStrictOrderedRing R
G : Type u_2
inst✝³ : AddCommGroup G
inst✝² : Module R G
H : Type u_3
inst✝¹ : AddCommGroup H
inst✝ : Module R H
C₁ : PointedCone R G
C₂ : PointedCone R H
z : H ⊗[R] G
hz : ∀ φ ∈ dual (Dual.eval R H) ↑C₂, ∀ ψ ∈ dual (Dual.eval R G) ↑C₁, 0 ≤ ((dualDistrib R H G) (φ ⊗ₜ[R] ψ)) z
φ : Dual R G
hφ : φ ∈ dual (Dual.eval R G) ↑C₁
ψ : Dual R H
hψ : ψ ∈ dual (Dual.eval R H) ↑C₂
⊢ 0 ≤ ((dualDistrib R G H) (φ ⊗ₜ[R] ψ)) ((TensorProduct.comm R H G) z)

Tactic:
simpa using

Goal state after:
case refine_2
R : Type u_1
inst✝⁶ : CommRing R
inst✝⁵ : LinearOrder R
inst✝⁴ : IsStrictOrderedRing R
G : Type u_2
inst✝³ : AddCommGroup G
inst✝² : Module R G
H : Type u_3
inst✝¹ : AddCommGroup H
inst✝ : Module R H
C₁ : PointedCone R G
C₂ : PointedCone R H
z : H ⊗[R] G
hz : ∀ φ ∈ dual (Dual.eval R H) ↑C₂, ∀ ψ ∈ dual (Dual.eval R G) ↑C₁, 0 ≤ ((dualDistrib R H G) (φ ⊗ₜ[R] ψ)) z
φ : Dual R G
hφ : φ ∈ dual (Dual.eval R G) ↑C₁
ψ : Dual R H
hψ : ψ ∈ dual (Dual.eval R H) ↑C₂
⊢ 0 ≤ ((dualDistrib R H G) (ψ ⊗ₜ[R] φ)) z
Module: Mathlib.Geometry.Convex.Cone.Dual

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommRing R
inst✝⁵ : PartialOrder R
inst✝⁴ : IsOrderedRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u_3
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
p : M →ₗ[R] N →ₗ[R] R
hp : Injective ⇑p.flip
y : N
hy : y ∈ dual p univ
x : M
⊢ (p x) y ≤ 0

Tactic:
simpa using

Goal state after:
R : Type u_1
inst✝⁶ : CommRing R
inst✝⁵ : PartialOrder R
inst✝⁴ : IsOrderedRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u_3
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
p : M →ₗ[R] N →ₗ[R] R
hp : Injective ⇑p.flip
y : N
hy : y ∈ dual p univ
x : M
⊢ (p x) y ≤ 0
Module: Mathlib.Analysis.Normed.Affine.Convex

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
s : Set E
x : E
hs : s ∈ 𝓝 x
this :
  ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [FiniteDimensional ℝ E] {s : Set E} {x : E},
    s ∈ 𝓝 x → x = 0 → ∃ b, x ∈ interior ((convexHull ℝ) (range ⇑b)) ∧ (convexHull ℝ) (range ⇑b) ⊆ s
hx : ¬x = 0
⊢ -x +ᵥ s ∈ 𝓝 0

Tactic:
simpa using

Goal state after:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
s : Set E
x : E
hs : s ∈ 𝓝 x
this :
  ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [FiniteDimensional ℝ E] {s : Set E} {x : E},
    s ∈ 𝓝 x → x = 0 → ∃ b, x ∈ interior ((convexHull ℝ) (range ⇑b)) ∧ (convexHull ℝ) (range ⇑b) ⊆ s
hx : ¬x = 0
⊢ -x +ᵥ s ∈ 𝓝 0
Module: Mathlib.Analysis.Normed.Affine.Convex

Goal state before:
pp: case h
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
s : Set E
x : E
hs : s ∈ 𝓝 x
this :
  ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [FiniteDimensional ℝ E] {s : Set E} {x : E},
    s ∈ 𝓝 x → x = 0 → ∃ b, x ∈ interior ((convexHull ℝ) (range ⇑b)) ∧ (convexHull ℝ) (range ⇑b) ⊆ s
hx : ¬x = 0
b : AffineBasis (Fin (finrank ℝ E + 1)) ℝ E
hb : 0 ∈ interior ((convexHull ℝ) (range ⇑b)) ∧ (convexHull ℝ) (range ⇑b) ⊆ -x +ᵥ s
⊢ x ∈ interior ((convexHull ℝ) (range ⇑(x +ᵥ b))) ∧ (convexHull ℝ) (range ⇑(x +ᵥ b)) ⊆ s

Tactic:
simpa using

Goal state after:
case h
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
s : Set E
x : E
hs : s ∈ 𝓝 x
this :
  ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [FiniteDimensional ℝ E] {s : Set E} {x : E},
    s ∈ 𝓝 x → x = 0 → ∃ b, x ∈ interior ((convexHull ℝ) (range ⇑b)) ∧ (convexHull ℝ) (range ⇑b) ⊆ s
hx : ¬x = 0
b : AffineBasis (Fin (finrank ℝ E + 1)) ℝ E
hb : 0 ∈ interior ((convexHull ℝ) (range ⇑b)) ∧ (convexHull ℝ) (range ⇑b) ⊆ -x +ᵥ s
⊢ 0 ∈ interior ((convexHull ℝ) (range ⇑b)) ∧ x +ᵥ (convexHull ℝ) (range ⇑b) ⊆ s
Module: Mathlib.Analysis.Normed.Affine.Convex

Goal state before:
pp: E✝ : Type u_1
inst✝⁴ : NormedAddCommGroup E✝
inst✝³ : NormedSpace ℝ E✝
s✝ : Set E✝
x : E✝
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
s : Set E
hs : s ∈ 𝓝 0
b : AffineBasis (Fin (finrank ℝ E + 1)) ℝ E
c : AffineBasis (Fin (finrank ℝ E + 1)) ℝ E := -Finset.centroid ℝ Finset.univ ⇑b +ᵥ b
⊢ 0 ∈ interior ((convexHull ℝ) (range ⇑c))

Tactic:
simpa using

Goal state after:
E✝ : Type u_1
inst✝⁴ : NormedAddCommGroup E✝
inst✝³ : NormedSpace ℝ E✝
s✝ : Set E✝
x : E✝
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
s : Set E
hs : s ∈ 𝓝 0
b : AffineBasis (Fin (finrank ℝ E + 1)) ℝ E
c : AffineBasis (Fin (finrank ℝ E + 1)) ℝ E := -Finset.centroid ℝ Finset.univ ⇑b +ᵥ b
⊢ Finset.univ.centerMass (Finset.centroidWeights ℝ Finset.univ) ⇑b ∈ interior ((convexHull ℝ) (range ⇑b))
Module: Mathlib.Analysis.Normed.Affine.Convex

Goal state before:
pp: E✝ : Type u_1
inst✝⁴ : NormedAddCommGroup E✝
inst✝³ : NormedSpace ℝ E✝
s✝ : Set E✝
x : E✝
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
s : Set E
hs : s ∈ 𝓝 0
b : AffineBasis (Fin (finrank ℝ E + 1)) ℝ E
c : AffineBasis (Fin (finrank ℝ E + 1)) ℝ E := -Finset.centroid ℝ Finset.univ ⇑b +ᵥ b
hc₀ : 0 ∈ interior ((convexHull ℝ) (range ⇑c))
cnorm : ℝ := Finset.univ.sup' ⋯ fun i ↦ ‖c i‖
⊢ range ⇑c ⊆ closedBall 0 (cnorm + 1)

Tactic:
simpa using

Goal state after:
E✝ : Type u_1
inst✝⁴ : NormedAddCommGroup E✝
inst✝³ : NormedSpace ℝ E✝
s✝ : Set E✝
x : E✝
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
s : Set E
hs : s ∈ 𝓝 0
b : AffineBasis (Fin (finrank ℝ E + 1)) ℝ E
c : AffineBasis (Fin (finrank ℝ E + 1)) ℝ E := -Finset.centroid ℝ Finset.univ ⇑b +ᵥ b
hc₀ : 0 ∈ interior ((convexHull ℝ) (range ⇑c))
cnorm : ℝ := Finset.univ.sup' ⋯ fun i ↦ ‖c i‖
⊢ ∀ (i : Fin (finrank ℝ E + 1)), ∃ b ∈ Finset.univ, ‖c i‖ - 1 ≤ ‖c b‖
Module: Mathlib.Analysis.Convex.Extrema

Goal state before:
pp: E : Type u_1
β : Type u_2
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : TopologicalSpace E
inst✝⁸ : Module ℝ E
inst✝⁷ : IsTopologicalAddGroup E
inst✝⁶ : ContinuousSMul ℝ E
inst✝⁵ : AddCommGroup β
inst✝⁴ : PartialOrder β
inst✝³ : IsOrderedAddMonoid β
inst✝² : Module ℝ β
inst✝¹ : IsOrderedModule ℝ β
inst✝ : PosSMulReflectLE ℝ β
s : Set E
f : E → β
a : E
a_in_s : a ∈ s
h_localmin : IsLocalMinOn f s a
h_conv : ConvexOn ℝ s f
x : E
x_in_s : x ∈ s
g : ℝ →ᵃ[ℝ] E := AffineMap.lineMap a x
hg0 : g 0 = a
hg1 : g 1 = x
hgc : Continuous[_, inst✝⁹] ⇑g
⊢ MapsTo (⇑g) (Icc 0 1) s

Tactic:
simpa using

Goal state after:
E : Type u_1
β : Type u_2
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : TopologicalSpace E
inst✝⁸ : Module ℝ E
inst✝⁷ : IsTopologicalAddGroup E
inst✝⁶ : ContinuousSMul ℝ E
inst✝⁵ : AddCommGroup β
inst✝⁴ : PartialOrder β
inst✝³ : IsOrderedAddMonoid β
inst✝² : Module ℝ β
inst✝¹ : IsOrderedModule ℝ β
inst✝ : PosSMulReflectLE ℝ β
s : Set E
f : E → β
a : E
a_in_s : a ∈ s
h_localmin : IsLocalMinOn f s a
h_conv : ConvexOn ℝ s f
x : E
x_in_s : x ∈ s
g : ℝ →ᵃ[ℝ] E := AffineMap.lineMap a x
hg0 : g 0 = a
hg1 : g 1 = x
hgc : Continuous[_, inst✝⁹] ⇑g
⊢ segment ℝ a x ⊆ s
Module: Mathlib.Analysis.Convex.Extrema

Goal state before:
pp: E : Type u_1
β : Type u_2
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : TopologicalSpace E
inst✝⁸ : Module ℝ E
inst✝⁷ : IsTopologicalAddGroup E
inst✝⁶ : ContinuousSMul ℝ E
inst✝⁵ : AddCommGroup β
inst✝⁴ : PartialOrder β
inst✝³ : IsOrderedAddMonoid β
inst✝² : Module ℝ β
inst✝¹ : IsOrderedModule ℝ β
inst✝ : PosSMulReflectLE ℝ β
s : Set E
f : E → β
a : E
a_in_s : a ∈ s
h_localmin : IsLocalMinOn f s a
h_conv : ConvexOn ℝ s f
x : E
x_in_s : x ∈ s
g : ℝ →ᵃ[ℝ] E := AffineMap.lineMap a x
hg0 : g 0 = a
hg1 : g 1 = x
hgc : Continuous[_, inst✝⁹] ⇑g
h_maps : MapsTo (⇑g) (Icc 0 1) s
fg_local_min_on : IsLocalMinOn (f ∘ ⇑g) (Icc 0 1) 0
fg_min_on : IsMinOn (f ∘ ⇑g) (Icc 0 1) 0
⊢ x ∈ {x | (fun x ↦ f a ≤ f x) x}

Tactic:
simpa using

Goal state after:
E : Type u_1
β : Type u_2
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : TopologicalSpace E
inst✝⁸ : Module ℝ E
inst✝⁷ : IsTopologicalAddGroup E
inst✝⁶ : ContinuousSMul ℝ E
inst✝⁵ : AddCommGroup β
inst✝⁴ : PartialOrder β
inst✝³ : IsOrderedAddMonoid β
inst✝² : Module ℝ β
inst✝¹ : IsOrderedModule ℝ β
inst✝ : PosSMulReflectLE ℝ β
s : Set E
f : E → β
a : E
a_in_s : a ∈ s
h_localmin : IsLocalMinOn f s a
h_conv : ConvexOn ℝ s f
x : E
x_in_s : x ∈ s
g : ℝ →ᵃ[ℝ] E := AffineMap.lineMap a x
hg0 : g 0 = a
hg1 : g 1 = x
hgc : Continuous[_, inst✝⁹] ⇑g
h_maps : MapsTo (⇑g) (Icc 0 1) s
fg_local_min_on : IsLocalMinOn (f ∘ ⇑g) (Icc 0 1) 0
fg_min_on : IsMinOn (f ∘ ⇑g) (Icc 0 1) 0
⊢ f a ≤ f x
Module: Mathlib.Analysis.Normed.Affine.Convex

Goal state before:
pp: E✝ : Type u_1
inst✝⁴ : NormedAddCommGroup E✝
inst✝³ : NormedSpace ℝ E✝
s✝ : Set E✝
x : E✝
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
s : Set E
hs : s ∈ 𝓝 0
b : AffineBasis (Fin (finrank ℝ E + 1)) ℝ E
c : AffineBasis (Fin (finrank ℝ E + 1)) ℝ E := -Finset.centroid ℝ Finset.univ ⇑b +ᵥ b
hc₀ : 0 ∈ interior ((convexHull ℝ) (range ⇑c))
cnorm : ℝ := Finset.univ.sup' ⋯ fun i ↦ ‖c i‖
hcnorm : range ⇑c ⊆ closedBall 0 (cnorm + 1)
ε : ℝ
hε : ε > 0
hεs : ball 0 ε ⊆ s
ε' : ℝ := ε / 2 / (cnorm + 1)
hc' : 0 < cnorm + 1
hε' : 0 < ε'
d : AffineBasis (Fin (finrank ℝ E + 1)) ℝ E := Units.mk0 ε' ⋯ • c
hε₀ : 0 < ε / 2
⊢ ∀ (y : Fin (finrank ℝ E + 1)), ε' * ‖c y‖ ≤ ε / 2

Tactic:
simpa using

Goal state after:
E✝ : Type u_1
inst✝⁴ : NormedAddCommGroup E✝
inst✝³ : NormedSpace ℝ E✝
s✝ : Set E✝
x : E✝
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
s : Set E
hs : s ∈ 𝓝 0
b : AffineBasis (Fin (finrank ℝ E + 1)) ℝ E
c : AffineBasis (Fin (finrank ℝ E + 1)) ℝ E := -Finset.centroid ℝ Finset.univ ⇑b +ᵥ b
hc₀ : 0 ∈ interior ((convexHull ℝ) (range ⇑c))
cnorm : ℝ := Finset.univ.sup' ⋯ fun i ↦ ‖c i‖
hcnorm : range ⇑c ⊆ closedBall 0 (cnorm + 1)
ε : ℝ
hε : ε > 0
hεs : ball 0 ε ⊆ s
ε' : ℝ := ε / 2 / (cnorm + 1)
hc' : 0 < cnorm + 1
hε' : 0 < ε'
d : AffineBasis (Fin (finrank ℝ E + 1)) ℝ E := Units.mk0 ε' ⋯ • c
hε₀ : 0 < ε / 2
⊢ ∀ (y : Fin (finrank ℝ E + 1)), ‖c y‖ ≤ cnorm + 1
Module: Mathlib.Analysis.Convex.Exposed

Goal state before:
pp: case insert.inr
𝕜 : Type u_1
E : Type u_2
inst✝⁷ : TopologicalSpace 𝕜
inst✝⁶ : Ring 𝕜
inst✝⁵ : PartialOrder 𝕜
inst✝⁴ : AddCommMonoid E
inst✝³ : TopologicalSpace E
inst✝² : Module 𝕜 E
A : Set E
inst✝¹ : IsOrderedRing 𝕜
inst✝ : ContinuousAdd 𝕜
C : Set E
F : Finset (Set E)
a✝ : C ∉ F
hF' : F.Nonempty → (∀ B ∈ F, IsExposed 𝕜 A B) → IsExposed 𝕜 A (⋂₀ ↑F)
hF : (insert C F).Nonempty
hAF : ∀ B ∈ insert C F, IsExposed 𝕜 A B
hFnemp : F.Nonempty
⊢ IsExposed 𝕜 A (C ∩ ⋂₀ ↑F)

Tactic:
· exact (hAF C (Finset.mem_insert_self C F)).inter
        (hF' hFnemp fun B hB => hAF B (Finset.mem_insert_of_mem hB))

Goal state after:
Module: Mathlib.Analysis.Normed.Affine.Convex

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
s t : Set E
hs₁ : Convex ℝ s
hs₂ : IsCompact s
ht : t ∈ 𝓝ˢ s
U : Set E
hU₁ : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U
hU₂ : s ⊆ U
hU₃ : U ⊆ t
V : Set E
hV₁ : V ∈ 𝓝 0
hV₂ : V + s ⊆ U
b : AffineBasis (Fin (finrank ℝ E + 1)) ℝ E
hb₁ : 0 ∈ interior ((convexHull ℝ) (range ⇑b))
hb₂ : (convexHull ℝ) (range ⇑b) ⊆ V
x : E
hx : x ∈ s
⊢ x ∈ interior ((convexHull ℝ) (range ⇑b)) + {x}

Tactic:
simpa using

Goal state after:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
s t : Set E
hs₁ : Convex ℝ s
hs₂ : IsCompact s
ht : t ∈ 𝓝ˢ s
U : Set E
hU₁ : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U
hU₂ : s ⊆ U
hU₃ : U ⊆ t
V : Set E
hV₁ : V ∈ 𝓝 0
hV₂ : V + s ⊆ U
b : AffineBasis (Fin (finrank ℝ E + 1)) ℝ E
hb₁ : 0 ∈ interior ((convexHull ℝ) (range ⇑b))
hb₂ : (convexHull ℝ) (range ⇑b) ⊆ V
x : E
hx : x ∈ s
⊢ 0 ∈ interior ((convexHull ℝ) (range ⇑b))
Module: Mathlib.Analysis.Convex.Continuous

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E → ℝ
x₀ : E
ε r M : ℝ
hf : ConvexOn ℝ (ball x₀ r) f
hε : 0 < ε
hM : ∀ (a : E), dist a x₀ < r → |f a| ≤ M
K : ℝ := 2 * M / ε
hK : K = 2 * M / ε
x y : E
hx : x ∈ ball x₀ (r - ε)
hy : y ∈ ball x₀ (r - ε)
hx₀r : ball x₀ (r - ε) ⊆ ball x₀ r
hx' : x ∈ ball x₀ r
hy' : y ∈ ball x₀ r
z : E := x + (ε / ‖x - y‖) • (x - y)
hxy : 0 < ‖x - y‖
hz : z ∈ ball x₀ r
a : ℝ := ε / (ε + ‖x - y‖)
b : ℝ := ‖x - y‖ / (ε + ‖x - y‖)
hab : a + b = 1
⊢ a • x + b • x = a • y + b • z

Tactic:
simp [z, a, b, smul_smul, hxy.ne', smul_sub]

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E → ℝ
x₀ : E
ε r M : ℝ
hf : ConvexOn ℝ (ball x₀ r) f
hε : 0 < ε
hM : ∀ (a : E), dist a x₀ < r → |f a| ≤ M
K : ℝ := 2 * M / ε
hK : K = 2 * M / ε
x y : E
hx : x ∈ ball x₀ (r - ε)
hy : y ∈ ball x₀ (r - ε)
hx₀r : ball x₀ (r - ε) ⊆ ball x₀ r
hx' : x ∈ ball x₀ r
hy' : y ∈ ball x₀ r
z : E := x + (ε / ‖x - y‖) • (x - y)
hxy : 0 < ‖x - y‖
hz : z ∈ ball x₀ r
a : ℝ := ε / (ε + ‖x - y‖)
b : ℝ := ‖x - y‖ / (ε + ‖x - y‖)
hab : a + b = 1
⊢ (ε / (ε + ‖x - y‖)) • x + (‖x - y‖ / (ε + ‖x - y‖)) • x =
    (ε / (ε + ‖x - y‖)) • y + ((‖x - y‖ / (ε + ‖x - y‖)) • x + ((ε / (ε + ‖x - y‖)) • x - (ε / (ε + ‖x - y‖)) • y))
Module: Mathlib.Analysis.Convex.Continuous

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E → ℝ
x₀ : E
ε r M : ℝ
hf : ConcaveOn ℝ (ball x₀ r) f
hε : 0 < ε
hM : ∀ (a : E), dist a x₀ < r → |f a| ≤ M
⊢ LipschitzOnWith (2 * M / ε).toNNReal f (ball x₀ (r - ε))

Tactic:
simpa using

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E → ℝ
x₀ : E
ε r M : ℝ
hf : ConcaveOn ℝ (ball x₀ r) f
hε : 0 < ε
hM : ∀ (a : E), dist a x₀ < r → |f a| ≤ M
⊢ LipschitzOnWith (2 * M / ε).toNNReal f (ball x₀ (r - ε))
Module: Mathlib.Analysis.Convex.Continuous

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E → ℝ
x₀ : E
ε r M : ℝ
hf : ConcaveOn ℝ (ball x₀ r) f
hε : 0 < ε
hM : ∀ (a : E), dist a x₀ < r → |f a| ≤ M
⊢ ∀ (a : E), dist a x₀ < r → |(-f) a| ≤ M

Tactic:
simpa using

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E → ℝ
x₀ : E
ε r M : ℝ
hf : ConcaveOn ℝ (ball x₀ r) f
hε : 0 < ε
hM : ∀ (a : E), dist a x₀ < r → |f a| ≤ M
⊢ ∀ (a : E), dist a x₀ < r → |f a| ≤ M
Module: Mathlib.Analysis.Convex.GaugeRescale

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s : Set E
hc : Convex ℝ s
hne : (interior s).Nonempty
hb : Bornology.IsBounded s
⊢ ∃ h,
    ⇑h '' interior s = ball 0 1 ∧
      ⇑h '' closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s = closedBall 0 1 ∧
        ⇑h '' frontier s = sphere 0 1

Tactic:
simpa using

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s : Set E
hc : Convex ℝ s
hne : (interior s).Nonempty
hb : Bornology.IsBounded s
⊢ ∃ h,
    ⇑h '' interior s = ball 0 1 ∧
      ⇑h '' closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s = closedBall 0 1 ∧
        ⇑h '' frontier s = sphere 0 1
Module: Mathlib.Analysis.Convex.Continuous

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E → ℝ
x₀ : E
r r' : ℝ
hf : ConvexOn ℝ (ball x₀ r) f
hr : r' < r
M : ℝ
hM : ∀ (a : E), dist a x₀ < r → |f a| < M
⊢ ∃ K, LipschitzOnWith K f (ball x₀ r')

Tactic:
← sub_sub_cancel r r'

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E → ℝ
x₀ : E
r r' : ℝ
hf : ConvexOn ℝ (ball x₀ r) f
hr : r' < r
M : ℝ
hM : ∀ (a : E), dist a x₀ < r → |f a| < M
⊢ ∃ K, LipschitzOnWith K f (ball x₀ (r - (r - r')))
Module: Mathlib.Analysis.Convex.Continuous

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E → ℝ
x₀ : E
r r' : ℝ
hf : ConcaveOn ℝ (ball x₀ r) f
hr : r' < r
hf' : IsBounded ((-f) '' ball x₀ r)
⊢ ∃ K, LipschitzOnWith K f (ball x₀ r')

Tactic:
simpa using

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E → ℝ
x₀ : E
r r' : ℝ
hf : ConcaveOn ℝ (ball x₀ r) f
hr : r' < r
hf' : IsBounded ((-f) '' ball x₀ r)
⊢ ∃ K, LipschitzOnWith K f (ball x₀ r')
Module: Mathlib.Analysis.Convex.Continuous

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
C : Set E
f : E → ℝ
hf : ConcaveOn ℝ C f
x₀ : E
hC : C ∈ 𝓝 x₀
⊢ Filter.IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) (𝓝 x₀) |f| ↔ Filter.IsBoundedUnder (fun x1 x2 ↦ x1 ≥ x2) (𝓝 x₀) f

Tactic:
simpa using

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
C : Set E
f : E → ℝ
hf : ConcaveOn ℝ C f
x₀ : E
hC : C ∈ 𝓝 x₀
⊢ (Filter.IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) (𝓝 x₀) fun i ↦ |f i|) ↔
    Filter.IsBoundedUnder (fun x1 x2 ↦ x2 ≤ x1) (𝓝 x₀) f
Module: Mathlib.Analysis.Convex.Integral

Goal state before:
pp: case refine_3
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
μ : Measure α
s : Set E
f : α → E
inst✝ : IsProbabilityMeasure μ
hs : Convex ℝ s
hsc : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hf : ∀ᵐ (x : α) ∂μ, f x ∈ s
this✝² : MeasurableSpace E := borel E
this✝¹ : BorelSpace E
g : α → E
hfi : Integrable g μ
hgm : StronglyMeasurable g
hfg : f =ᵐ[μ] g
this✝ : SeparableSpace ↑(range g ∩ s)
y₀ : E
h₀ : y₀ ∈ range g ∩ s
hg : ∀ᵐ (x : α) ∂μ, g x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (range g ∩ s)
G : ℕ → SimpleFunc α E := SimpleFunc.approxOn g ⋯ (range g ∩ s) y₀ h₀
this : Tendsto (fun n ↦ SimpleFunc.integral μ (G n)) atTop (𝓝 (∫ (x : α), g x ∂μ))
n : ℕ
⊢ ∀ i ∈ (G n).range, ↑(ContinuousLinearMap.id ℝ E) i ∈ s

Tactic:
simp only [SimpleFunc.mem_range, forall_mem_range]
    intro x
    apply (range g).inter_subset_right
    exact SimpleFunc.approxOn_mem hgm.measurable h₀ _ _

Goal state after: