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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁷ : TopologicalSpace 𝕜
inst✝⁶ : Ring 𝕜
inst✝⁵ : PartialOrder 𝕜
inst✝⁴ : AddCommMonoid E
inst✝³ : TopologicalSpace E
inst✝² : Module 𝕜 E
inst✝¹ : IsOrderedRing 𝕜
inst✝ : ContinuousAdd 𝕜
A B C : Set E
hB : IsExposed 𝕜 A B
hC : IsExposed 𝕜 A C
⊢ IsExposed 𝕜 A (B ∩ C)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Convex.GaugeRescale

Goal state before:
pp: E : Type u_1
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s t : Set E
c : ℝ
hc : 0 ≤ c
x : E
⊢ gaugeRescale s t (c • x) = c • gaugeRescale s t x

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Convex.GaugeRescale

Goal state before:
pp: E : Type u_1
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s t : Set E
x : E
hx : gauge t x ≠ 0
⊢ gauge t (gaugeRescale s t x) = gauge s x

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Convex.GaugeRescale

Goal state before:
pp: E : Type u_1
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s t : Set E
x : E
⊢ gauge t (gaugeRescale s t x) ≤ gauge s x

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Convex.GaugeRescale

Goal state before:
pp: E : Type u_1
inst✝³ : AddCommGroup E
inst✝² : Module ℝ E
inst✝¹ : TopologicalSpace E
inst✝ : T1Space E
s : Set E
hsa : Absorbent ℝ s
hsb : IsVonNBounded ℝ s
x : E
⊢ gaugeRescale s s x = x

Tactic:
by

Goal state after:
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
hdnorm : range ⇑d ⊆ closedBall 0 (ε / 2)
⊢ ε / 2 < ε

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Convex.Exposed

Goal state before:
pp: 𝕜 : 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 𝕜
F : Finset (Set E)
hF : F.Nonempty
hAF : ∀ B ∈ F, IsExposed 𝕜 A B
⊢ IsExposed 𝕜 A (⋂₀ ↑F)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Convex.GaugeRescale

Goal state before:
pp: E : Type u_1
inst✝³ : AddCommGroup E
inst✝² : Module ℝ E
inst✝¹ : TopologicalSpace E
inst✝ : T1Space E
s t : Set E
hta : Absorbent ℝ t
htb : IsVonNBounded ℝ t
x : E
⊢ gauge t (gaugeRescale s t x) = gauge s x

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Convex.Exposed

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁵ : TopologicalSpace 𝕜
inst✝⁴ : Ring 𝕜
inst✝³ : PartialOrder 𝕜
inst✝² : AddCommMonoid E
inst✝¹ : TopologicalSpace E
inst✝ : Module 𝕜 E
A B C : Set E
hC : IsExposed 𝕜 A C
hCB : C ⊆ B
⊢ IsExposed 𝕜 (A ∩ B) C

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Convex.Exposed

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁵ : TopologicalSpace 𝕜
inst✝⁴ : Ring 𝕜
inst✝³ : PartialOrder 𝕜
inst✝² : AddCommMonoid E
inst✝¹ : TopologicalSpace E
inst✝ : Module 𝕜 E
A B C : Set E
hC : IsExposed 𝕜 B C
hCA : C ⊆ A
⊢ IsExposed 𝕜 (A ∩ B) C

Tactic:
by

Goal state after:
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 - ε)
hxy : x ≠ y
⊢ r - ε ≤ r

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Convex.Exposed

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁶ : TopologicalSpace 𝕜
inst✝⁵ : Ring 𝕜
inst✝⁴ : PartialOrder 𝕜
inst✝³ : AddCommMonoid E
inst✝² : TopologicalSpace E
inst✝¹ : Module 𝕜 E
inst✝ : OrderClosedTopology 𝕜
A B : Set E
hAB : IsExposed 𝕜 A B
hA : IsClosed A
⊢ IsClosed B

Tactic:
by

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 : Set E
x : E
hs : s ∈ 𝓝 x
⊢ ∃ b, x ∈ interior ((convexHull ℝ) (range ⇑b)) ∧ (convexHull ℝ) (range ⇑b) ⊆ s

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Convex.GaugeRescale

Goal state before:
pp: E : Type u_1
inst✝³ : AddCommGroup E
inst✝² : Module ℝ E
inst✝¹ : TopologicalSpace E
inst✝ : T1Space E
s t u : Set E
hta : Absorbent ℝ t
htb : IsVonNBounded ℝ t
x : E
⊢ gaugeRescale t u (gaugeRescale s t x) = gaugeRescale s u x

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Convex.Exposed

Goal state before:
pp: 𝕜 : 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
x : E
⊢ x ∈ exposedPoints 𝕜 A ↔ IsExposed 𝕜 A {x}

Tactic:
by

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:
by

Goal state after:
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 - ε)
hxy : x ≠ y
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)
⊢ 0 < ‖x - y‖

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Convex.Exposed

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁶ : TopologicalSpace 𝕜
inst✝⁵ : Ring 𝕜
inst✝⁴ : LinearOrder 𝕜
inst✝³ : IsStrictOrderedRing 𝕜
inst✝² : AddCommMonoid E
inst✝¹ : TopologicalSpace E
inst✝ : Module 𝕜 E
A B : Set E
hAB : IsExposed 𝕜 A B
hA : Convex 𝕜 A
⊢ Convex 𝕜 B

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Convex.GaugeRescale

Goal state before:
pp: E : Type u_1
inst✝³ : AddCommGroup E
inst✝² : Module ℝ E
inst✝¹ : TopologicalSpace E
inst✝ : T1Space E
s t : Set E
hsa : Absorbent ℝ s
hsb : IsVonNBounded ℝ s
hta : Absorbent ℝ t
htb : IsVonNBounded ℝ t
x : E
⊢ gaugeRescale t s (gaugeRescale s t x) = x

Tactic:
by

Goal state after:
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‖
⊢ ‖z - x₀‖ = ‖x - x₀ + (ε / ‖x - y‖) • (x - y)‖

Tactic:
by

Goal state after:
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‖
⊢ ‖(ε / ‖x - y‖) • (x - y)‖ ≤ ε

Tactic:
by

Goal state after:
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‖
⊢ r - ε + ε = r

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Convex.Exposed

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁶ : TopologicalSpace 𝕜
inst✝⁵ : Ring 𝕜
inst✝⁴ : LinearOrder 𝕜
inst✝³ : IsStrictOrderedRing 𝕜
inst✝² : AddCommMonoid E
inst✝¹ : TopologicalSpace E
inst✝ : Module 𝕜 E
A B : Set E
hAB : IsExposed 𝕜 A B
⊢ IsExtreme 𝕜 A B

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Convex.GaugeRescale

Goal state before:
pp: E : Type u_1
inst✝³ : AddCommGroup E
inst✝² : Module ℝ E
inst✝¹ : TopologicalSpace E
inst✝ : T1Space E
s t : Set E
hsa : Absorbent ℝ s
hsb : IsVonNBounded ℝ s
hta : Absorbent ℝ t
htb : IsVonNBounded ℝ t
x : E
⊢ gaugeRescale s t (gaugeRescale t s x) = x

Tactic:
by

Goal state after:
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‖
⊢ ‖z - x₀‖ < r

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Convex.Independent

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝⁴ : Semiring 𝕜
inst✝³ : PartialOrder 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : Subsingleton ι
p : ι → E
⊢ ConvexIndependent 𝕜 p

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Convex.Independent

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝³ : Semiring 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : ι → E
hc : ConvexIndependent 𝕜 p
⊢ Injective p

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Convex.Independent

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝³ : Semiring 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
ι' : Type u_4
f : ι' ↪ ι
p : ι → E
hc : ConvexIndependent 𝕜 p
s : Set ι'
x : ι'
hx : (p ∘ ⇑f) x ∈ (convexHull 𝕜) (p ∘ ⇑f '' s)
⊢ p (f x) ∈ (convexHull 𝕜) (p '' ⇑f '' s)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Convex.Independent

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝³ : Semiring 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
ι' : Type u_4
f : ι' ↪ ι
p : ι → E
hc : ConvexIndependent 𝕜 p
⊢ ConvexIndependent 𝕜 (p ∘ ⇑f)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Convex.GaugeRescale

Goal state before:
pp: E : Type u_1
inst✝⁴ : AddCommGroup E
inst✝³ : Module ℝ E
inst✝² : TopologicalSpace E
inst✝¹ : IsTopologicalAddGroup E
inst✝ : ContinuousSMul ℝ E
s t : Set E
h₀ : t ∈ 𝓝 0
hc : Convex ℝ t
x : E
hx : x ∈ interior s
⊢ gaugeRescale s t x ∈ interior t

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Convex.Independent

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝³ : Semiring 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : ι → E
hc : ConvexIndependent 𝕜 p
⊢ ConvexIndependent 𝕜 Subtype.val

Tactic:
by

Goal state after:
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‖)
⊢ a + b = 1

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Convex.GaugeRescale

Goal state before:
pp: E : Type u_1
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module ℝ E
inst✝³ : TopologicalSpace E
inst✝² : IsTopologicalAddGroup E
inst✝¹ : ContinuousSMul ℝ E
inst✝ : T1Space E
s t : Set E
hs : Convex ℝ s
hs₀ : s ∈ 𝓝 0
ht : Convex ℝ t
ht₀ : t ∈ 𝓝 0
htb : IsVonNBounded ℝ t
⊢ Continuous[inst✝³, inst✝³] (gaugeRescale s t)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Convex.Independent

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝³ : Semiring 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : ι → E
⊢ ConvexIndependent 𝕜 p ↔ ∀ (i : ι) (s : Set ι), p i ∉ (convexHull 𝕜) (p '' (s \ {i}))

Tactic:
by

Goal state after:
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
⊢ x = a • x + b • x

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Convex.GaugeRescale

Goal state before:
pp: E : Type u_1
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module ℝ E
inst✝³ : TopologicalSpace E
inst✝² : IsTopologicalAddGroup E
inst✝¹ : ContinuousSMul ℝ E
s✝ t✝ : Set E
inst✝ : T1Space E
s t : Set E
hsc : Convex ℝ s
hs₀ : s ∈ 𝓝 0
hsb : IsVonNBounded ℝ s
htc : Convex ℝ t
ht₀ : t ∈ 𝓝 0
htb : IsVonNBounded ℝ t
⊢ Continuous[inst✝³, inst✝³] (gaugeRescaleEquiv s t ⋯ hsb ⋯ htb).toFun

Tactic:
by

Goal state after:
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:
by

Goal state after:
Module: Mathlib.Analysis.Convex.Independent

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝³ : Semiring 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
⊢ ConvexIndependent 𝕜 Subtype.val ↔ ∀ t ⊆ s, s ∩ (convexHull 𝕜) t ⊆ t

Tactic:
by

Goal state after:
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
⊢ x = a • y + b • z

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Convex.GaugeRescale

Goal state before:
pp: E : Type u_1
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module ℝ E
inst✝³ : TopologicalSpace E
inst✝² : IsTopologicalAddGroup E
inst✝¹ : ContinuousSMul ℝ E
s✝ t✝ : Set E
inst✝ : T1Space E
s t : Set E
hsc : Convex ℝ s
hs₀ : s ∈ 𝓝 0
hsb : IsVonNBounded ℝ s
htc : Convex ℝ t
ht₀ : t ∈ 𝓝 0
htb : IsVonNBounded ℝ t
⊢ Continuous[inst✝³, inst✝³] (gaugeRescaleEquiv s t ⋯ hsb ⋯ htb).invFun

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Convex.GaugeRescale

Goal state before:
pp: E : Type u_1
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module ℝ E
inst✝³ : TopologicalSpace E
inst✝² : IsTopologicalAddGroup E
inst✝¹ : ContinuousSMul ℝ E
inst✝ : T1Space E
s t : Set E
hsc : Convex ℝ s
hs₀ : s ∈ 𝓝 0
hsb : IsVonNBounded ℝ s
htc : Convex ℝ t
ht₀ : t ∈ 𝓝 0
htb : IsVonNBounded ℝ t
⊢ interior t ⊆ ⇑(gaugeRescaleHomeomorph s t hsc hs₀ hsb htc ht₀ htb) '' interior s

Tactic:
by

Goal state after:
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
hxyz : x = a • y + b • z
⊢ 0 ≤ a

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Convex.Independent

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝³ : Semiring 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
⊢ ConvexIndependent 𝕜 Subtype.val ↔ ∀ x ∈ s, x ∉ (convexHull 𝕜) (s \ {x})

Tactic:
by

Goal state after:
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
hxyz : x = a • y + b • z
⊢ 0 ≤ b

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Convex.Independent

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : ι → E
h : ∀ (s : Finset ι) (x : ι), p x ∈ (convexHull 𝕜) ↑(image p s) → x ∈ s
s : Set ι
x : ι
hx : p x ∈ (convexHull 𝕜) (p '' s)
⊢ Injective p

Tactic:
rintro a b hab

Goal state after:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : ι → E
h : ∀ (s : Finset ι) (x : ι), p x ∈ (convexHull 𝕜) ↑(image p s) → x ∈ s
s : Set ι
x : ι
hx : p x ∈ (convexHull 𝕜) (p '' s)
a b : ι
hab : p a = p b
⊢ a = b
Module: Mathlib.Analysis.Convex.GaugeRescale

Goal state before:
pp: E : Type u_1
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module ℝ E
inst✝³ : TopologicalSpace E
inst✝² : IsTopologicalAddGroup E
inst✝¹ : ContinuousSMul ℝ E
inst✝ : T1Space E
s t : Set E
hsc : Convex ℝ s
hs₀ : s ∈ 𝓝 0
hsb : IsVonNBounded ℝ s
htc : Convex ℝ t
ht₀ : t ∈ 𝓝 0
htb : IsVonNBounded ℝ t
⊢ ⇑(gaugeRescaleHomeomorph s t hsc hs₀ hsb htc ht₀ htb) '' closure[inst✝³] s = closure[inst✝³] t

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Convex.Independent

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : ι → E
h : ∀ (s : Finset ι) (x : ι), p x ∈ (convexHull 𝕜) ↑(image p s) → x ∈ s
s : Set ι
x : ι
hx : p x ∈ (convexHull 𝕜) (p '' s)
⊢ Injective p

Tactic:
by

Goal state after:
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
hxyz : x = a • y + b • z
⊢ ε * (f x - f y) ≤ ‖x - y‖ * (f z - f x)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Convex.Independent

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : ι → E
h : ∀ (s : Finset ι) (x : ι), p x ∈ (convexHull 𝕜) ↑(image p s) → x ∈ s
s : Set ι
x : ι
hp : Injective p
t : Finset E
ht : ↑t ⊆ p '' s
hx : p x ∈ (convexHull 𝕜) ↑t
this : x ∈ t.preimage p ⋯
⊢ p x ∈ ↑t

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Convex.Independent

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : ι → E
⊢ ConvexIndependent 𝕜 p ↔ ∀ (s : Finset ι) (x : ι), p x ∈ (convexHull 𝕜) ↑(image p s) → x ∈ s

Tactic:
by

Goal state after:
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
hxyz : x = a • y + b • z
⊢ ‖x - y‖ * (f z - f x) ≤ ‖x - y‖ * (2 * M)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Convex.GaugeRescale

Goal state before:
pp: E : Type u_1
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module ℝ E
inst✝³ : TopologicalSpace E
inst✝² : IsTopologicalAddGroup E
inst✝¹ : ContinuousSMul ℝ E
inst✝ : T1Space E
s t : Set E
hsc : Convex ℝ s
hsne : (interior s).Nonempty
hsb : IsVonNBounded ℝ s
hst : Convex ℝ t
htne : (interior t).Nonempty
htb : IsVonNBounded ℝ t
⊢ ∃ e, ⇑e '' interior s = interior t ∧ ⇑e '' closure[inst✝³] s = closure[inst✝³] t

Tactic:
rcases hsne with ⟨x, hx⟩

Goal state after:
E : Type u_1
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module ℝ E
inst✝³ : TopologicalSpace E
inst✝² : IsTopologicalAddGroup E
inst✝¹ : ContinuousSMul ℝ E
inst✝ : T1Space E
s t : Set E
hsc : Convex ℝ s
hsb : IsVonNBounded ℝ s
hst : Convex ℝ t
htne : (interior t).Nonempty
htb : IsVonNBounded ℝ t
x : E
hx : x ∈ interior s
⊢ ∃ e, ⇑e '' interior s = interior t ∧ ⇑e '' closure[inst✝³] s = closure[inst✝³] t
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 - ε)
⊢ f x - f y ≤ K * ‖x - y‖

Tactic:
by

Goal state after: