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

Goal state before:
pp: case hsa
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
⊢ Absorbent ℝ t

pp: case hsb
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
⊢ IsVonNBounded ℝ t

pp: case hta
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
⊢ Absorbent ℝ s

pp: case htb
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
⊢ IsVonNBounded ℝ s

Tactic:
<;>

Goal state after:
case hsa
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
⊢ Absorbent ℝ t

case hsb
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
⊢ IsVonNBounded ℝ t

case hta
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
⊢ Absorbent ℝ s

case htb
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
⊢ IsVonNBounded ℝ s
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
⊢ gauge t (gaugeRescale s t x) < 1

pp: case hc
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
⊢ Convex ℝ t

pp: case hs₀
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
⊢ t ∈ 𝓝 0

Tactic:
<;>

Goal state after:
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
⊢ gauge t (gaugeRescale s t x) < 1

case hc
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
⊢ Convex ℝ t

case hs₀
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
⊢ t ∈ 𝓝 0
Module: Mathlib.Analysis.Convex.GaugeRescale

Goal state before:
pp: case inl
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
hta : Absorbent ℝ t
⊢ ContinuousAt (gaugeRescale s t) 0

Tactic:
ContinuousAt,

Goal state after:
case inl
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
hta : Absorbent ℝ t
⊢ Tendsto (gaugeRescale s t) (𝓝 0) (𝓝 (gaugeRescale s t 0))
Module: Mathlib.Analysis.Convex.Continuous

Goal state before:
pp: case inr
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‖)
⊢ f x - f y ≤ K * ‖x - y‖

Tactic:
let b := ‖x - y‖ / (ε + ‖x - y‖)

Goal state after:
case inr
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‖)
⊢ f x - f y ≤ K * ‖x - y‖
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
  refine ⟨fun hc i s h => ?_, fun h s i hi => ?_⟩
  · rw [hc.mem_convexHull_iff] at h
    exact h.2 (Set.mem_singleton _)
  · by_contra H
    refine h i s ?_
    rw [Set.sdiff_singleton_eq_self H]
    exact hi

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 / ε
oneside : ∀ {x y : E}, x ∈ ball x₀ (r - ε) → y ∈ ball x₀ (r - ε) → f x - f y ≤ K * ‖x - y‖
x : E
hx : x ∈ ball x₀ (r - ε)
y : E
hy : y ∈ ball x₀ (r - ε)
⊢ dist (f x) (f y) ≤ K * dist x y

Tactic:
dist_eq_norm_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 / ε
oneside : ∀ {x y : E}, x ∈ ball x₀ (r - ε) → y ∈ ball x₀ (r - ε) → f x - f y ≤ K * ‖x - y‖
x : E
hx : x ∈ ball x₀ (r - ε)
y : E
hy : y ∈ ball x₀ (r - ε)
⊢ ‖f x - f y‖ ≤ K * ‖x - y‖
Module: Mathlib.Analysis.Convex.Join

Goal state before:
pp: 𝕜 : Type u_2
E : Type u_3
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t u : Set E
x : E
hx : x ∈ s
y : E
hy : y ∈ t
a₁ b₁ : 𝕜
ha₁ : 0 ≤ a₁
hb₁ : 0 ≤ b₁
hab₁ : a₁ + b₁ = 1
z : E
hz : z ∈ u
a₂ b₂ : 𝕜
ha₂ : 0 ≤ a₂
hb₂✝ : 0 ≤ b₂
hab₂ : a₂ + b₂ = 1
hb₂ : 0 < b₂
⊢ a₂ * a₁ * 1 = a₂ * (a₁ * 1)

pp: 𝕜 : Type u_2
E : Type u_3
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t u : Set E
x : E
hx : x ∈ s
y : E
hy : y ∈ t
a₁ b₁ : 𝕜
ha₁ : 0 ≤ a₁
hb₁ : 0 ≤ b₁
hab₁ : a₁ + b₁ = 1
z : E
hz : z ∈ u
a₂ b₂ : 𝕜
ha₂ : 0 ≤ a₂
hb₂✝ : 0 ≤ b₂
hab₂ : a₂ + b₂ = 1
hb₂ : 0 < b₂
⊢ (a₂ * b₁ + b₂) * (a₂ * b₁ / (a₂ * b₁ + b₂) * 1) = a₂ * (b₁ * 1)

pp: 𝕜 : Type u_2
E : Type u_3
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t u : Set E
x : E
hx : x ∈ s
y : E
hy : y ∈ t
a₁ b₁ : 𝕜
ha₁ : 0 ≤ a₁
hb₁ : 0 ≤ b₁
hab₁ : a₁ + b₁ = 1
z : E
hz : z ∈ u
a₂ b₂ : 𝕜
ha₂ : 0 ≤ a₂
hb₂✝ : 0 ≤ b₂
hab₂ : a₂ + b₂ = 1
hb₂ : 0 < b₂
⊢ (a₂ * b₁ + b₂) * (b₂ / (a₂ * b₁ + b₂) * 1) = b₂ * 1

Tactic:
<;>

Goal state after:
𝕜 : Type u_2
E : Type u_3
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t u : Set E
x : E
hx : x ∈ s
y : E
hy : y ∈ t
a₁ b₁ : 𝕜
ha₁ : 0 ≤ a₁
hb₁ : 0 ≤ b₁
hab₁ : a₁ + b₁ = 1
z : E
hz : z ∈ u
a₂ b₂ : 𝕜
ha₂ : 0 ≤ a₂
hb₂✝ : 0 ≤ b₂
hab₂ : a₂ + b₂ = 1
hb₂ : 0 < b₂
⊢ a₂ * a₁ * 1 = a₂ * (a₁ * 1)

𝕜 : Type u_2
E : Type u_3
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t u : Set E
x : E
hx : x ∈ s
y : E
hy : y ∈ t
a₁ b₁ : 𝕜
ha₁ : 0 ≤ a₁
hb₁ : 0 ≤ b₁
hab₁ : a₁ + b₁ = 1
z : E
hz : z ∈ u
a₂ b₂ : 𝕜
ha₂ : 0 ≤ a₂
hb₂✝ : 0 ≤ b₂
hab₂ : a₂ + b₂ = 1
hb₂ : 0 < b₂
⊢ (a₂ * b₁ + b₂) * (a₂ * b₁ / (a₂ * b₁ + b₂) * 1) = a₂ * (b₁ * 1)

𝕜 : Type u_2
E : Type u_3
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t u : Set E
x : E
hx : x ∈ s
y : E
hy : y ∈ t
a₁ b₁ : 𝕜
ha₁ : 0 ≤ a₁
hb₁ : 0 ≤ b₁
hab₁ : a₁ + b₁ = 1
z : E
hz : z ∈ u
a₂ b₂ : 𝕜
ha₂ : 0 ≤ a₂
hb₂✝ : 0 ≤ b₂
hab₂ : a₂ + b₂ = 1
hb₂ : 0 < b₂
⊢ (a₂ * b₁ + b₂) * (b₂ / (a₂ * b₁ + b₂) * 1) = b₂ * 1
Module: Mathlib.Analysis.Convex.Intrinsic

Goal state before:
pp: 𝕜 : Type u_1
V : Type u_2
P : Type u_5
inst✝⁴ : Ring 𝕜
inst✝³ : AddCommGroup V
inst✝² : Module 𝕜 V
inst✝¹ : TopologicalSpace P
inst✝ : AddTorsor V P
s : Set P
hs : IsClosed[instTopologicalSpaceSubtype] (Subtype.val ⁻¹' s)
⊢ intrinsicClosure 𝕜 s = s

Tactic:
intrinsicClosure,

Goal state after:
𝕜 : Type u_1
V : Type u_2
P : Type u_5
inst✝⁴ : Ring 𝕜
inst✝³ : AddCommGroup V
inst✝² : Module 𝕜 V
inst✝¹ : TopologicalSpace P
inst✝ : AddTorsor V P
s : Set P
hs : IsClosed[instTopologicalSpaceSubtype] (Subtype.val ⁻¹' s)
⊢ Subtype.val '' closure[instTopologicalSpaceSubtype] (Subtype.val ⁻¹' s) = s
Module: Mathlib.Analysis.Convex.Intrinsic

Goal state before:
pp: 𝕜 : Type u_1
V : Type u_2
P : Type u_5
inst✝⁴ : Ring 𝕜
inst✝³ : AddCommGroup V
inst✝² : Module 𝕜 V
inst✝¹ : TopologicalSpace P
inst✝ : AddTorsor V P
s : Set P
ht : affineSpan 𝕜 s = affineSpan 𝕜 (intrinsicClosure 𝕜 s)
⊢ IsClosed[instTopologicalSpaceSubtype] (Subtype.val ⁻¹' intrinsicClosure 𝕜 s)

Tactic:
intrinsicClosure,

Goal state after:
𝕜 : Type u_1
V : Type u_2
P : Type u_5
inst✝⁴ : Ring 𝕜
inst✝³ : AddCommGroup V
inst✝² : Module 𝕜 V
inst✝¹ : TopologicalSpace P
inst✝ : AddTorsor V P
s : Set P
ht : affineSpan 𝕜 s = affineSpan 𝕜 (intrinsicClosure 𝕜 s)
⊢ IsClosed[instTopologicalSpaceSubtype]
    (Subtype.val ⁻¹' Subtype.val '' closure[instTopologicalSpaceSubtype] (Subtype.val ⁻¹' s))
Module: Mathlib.Analysis.Convex.Intrinsic

Goal state before:
pp: 𝕜 : Type u_1
V : Type u_2
P : Type u_5
inst✝⁴ : Ring 𝕜
inst✝³ : AddCommGroup V
inst✝² : Module 𝕜 V
inst✝¹ : TopologicalSpace P
inst✝ : AddTorsor V P
s : Set P
h : IsInducing Subtype.val
⊢ intrinsicClosure 𝕜 s = closure[inst✝¹] s ∩ ↑(affineSpan 𝕜 s)

Tactic:
intrinsicClosure,

Goal state after:
𝕜 : Type u_1
V : Type u_2
P : Type u_5
inst✝⁴ : Ring 𝕜
inst✝³ : AddCommGroup V
inst✝² : Module 𝕜 V
inst✝¹ : TopologicalSpace P
inst✝ : AddTorsor V P
s : Set P
h : IsInducing Subtype.val
⊢ Subtype.val '' closure[instTopologicalSpaceSubtype] (Subtype.val ⁻¹' s) = closure[inst✝¹] s ∩ ↑(affineSpan 𝕜 s)
Module: Mathlib.Analysis.Convex.Continuous

Goal state before:
pp: case e'_2
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
C : Set E
f : E → ℝ
hC : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] C
hC' : C.Nonempty
hf : ConcaveOn ℝ C f
this :
  [LocallyLipschitzOn C f, ContinuousOn f C, ∃ x₀ ∈ C, ContinuousAt f x₀,
      ∃ x₀ ∈ C, Filter.IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) (𝓝 x₀) (-f),
      ∀ ⦃x₀ : E⦄, x₀ ∈ C → Filter.IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) (𝓝 x₀) (-f),
      ∀ ⦃x₀ : E⦄, x₀ ∈ C → Filter.IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) (𝓝 x₀) |f|].TFAE
x✝ : E
⊢ Filter.IsBoundedUnder (fun x1 x2 ↦ x1 ≥ x2) (𝓝 x✝) f ↔ Filter.IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) (𝓝 x✝) (-f)

pp: case e'_3
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
C : Set E
f : E → ℝ
hC : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] C
hC' : C.Nonempty
hf : ConcaveOn ℝ C f
this :
  [LocallyLipschitzOn C f, ContinuousOn f C, ∃ x₀ ∈ C, ContinuousAt f x₀,
      ∃ x₀ ∈ C, Filter.IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) (𝓝 x₀) (-f),
      ∀ ⦃x₀ : E⦄, x₀ ∈ C → Filter.IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) (𝓝 x₀) (-f),
      ∀ ⦃x₀ : E⦄, x₀ ∈ C → Filter.IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) (𝓝 x₀) |f|].TFAE
a✝¹ : E
a✝ : a✝¹ ∈ C
⊢ Filter.IsBoundedUnder (fun x1 x2 ↦ x1 ≥ x2) (𝓝 a✝¹) f ↔ Filter.IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) (𝓝 a✝¹) (-f)

Tactic:
<;>

Goal state after:
case e'_2
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
C : Set E
f : E → ℝ
hC : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] C
hC' : C.Nonempty
hf : ConcaveOn ℝ C f
this :
  [LocallyLipschitzOn C f, ContinuousOn f C, ∃ x₀ ∈ C, ContinuousAt f x₀,
      ∃ x₀ ∈ C, Filter.IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) (𝓝 x₀) (-f),
      ∀ ⦃x₀ : E⦄, x₀ ∈ C → Filter.IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) (𝓝 x₀) (-f),
      ∀ ⦃x₀ : E⦄, x₀ ∈ C → Filter.IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) (𝓝 x₀) |f|].TFAE
x✝ : E
⊢ Filter.IsBoundedUnder (fun x1 x2 ↦ x1 ≥ x2) (𝓝 x✝) f ↔ Filter.IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) (𝓝 x✝) (-f)

case e'_3
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
C : Set E
f : E → ℝ
hC : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] C
hC' : C.Nonempty
hf : ConcaveOn ℝ C f
this :
  [LocallyLipschitzOn C f, ContinuousOn f C, ∃ x₀ ∈ C, ContinuousAt f x₀,
      ∃ x₀ ∈ C, Filter.IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) (𝓝 x₀) (-f),
      ∀ ⦃x₀ : E⦄, x₀ ∈ C → Filter.IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) (𝓝 x₀) (-f),
      ∀ ⦃x₀ : E⦄, x₀ ∈ C → Filter.IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) (𝓝 x₀) |f|].TFAE
a✝¹ : E
a✝ : a✝¹ ∈ C
⊢ Filter.IsBoundedUnder (fun x1 x2 ↦ x1 ≥ x2) (𝓝 a✝¹) f ↔ Filter.IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) (𝓝 a✝¹) (-f)
Module: Mathlib.Analysis.Convex.Intrinsic

Goal state before:
pp: case inr
𝕜 : Type u_1
V : Type u_2
W : Type u_3
Q : Type u_4
P : Type u_5
inst✝⁸ : Ring 𝕜
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module 𝕜 V
inst✝⁵ : TopologicalSpace P
inst✝⁴ : AddTorsor V P
inst✝³ : AddCommGroup W
inst✝² : Module 𝕜 W
inst✝¹ : TopologicalSpace Q
inst✝ : AddTorsor W Q
f : P → Q
s : Set P
e : [Nonempty ↑s] → ↥(affineSpan 𝕜 s) → ↥(affineSpan 𝕜 (f '' s))
he_homeo : ∀ [inst : Nonempty ↑s], IsHomeomorph e
he : ∀ [inst : Nonempty ↑s] (x : ↥(affineSpan 𝕜 s)), ↑(e x) = f ↑x
hs : s.Nonempty
this : Nonempty ↑s
⊢ intrinsicClosure 𝕜 (f '' s) = f '' intrinsicClosure 𝕜 s

Tactic:
intrinsicClosure,

Goal state after:
case inr
𝕜 : Type u_1
V : Type u_2
W : Type u_3
Q : Type u_4
P : Type u_5
inst✝⁸ : Ring 𝕜
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module 𝕜 V
inst✝⁵ : TopologicalSpace P
inst✝⁴ : AddTorsor V P
inst✝³ : AddCommGroup W
inst✝² : Module 𝕜 W
inst✝¹ : TopologicalSpace Q
inst✝ : AddTorsor W Q
f : P → Q
s : Set P
e : [Nonempty ↑s] → ↥(affineSpan 𝕜 s) → ↥(affineSpan 𝕜 (f '' s))
he_homeo : ∀ [inst : Nonempty ↑s], IsHomeomorph e
he : ∀ [inst : Nonempty ↑s] (x : ↥(affineSpan 𝕜 s)), ↑(e x) = f ↑x
hs : s.Nonempty
this : Nonempty ↑s
⊢ Subtype.val '' closure[instTopologicalSpaceSubtype] (Subtype.val ⁻¹' f '' s) = f '' intrinsicClosure 𝕜 s
Module: Mathlib.Analysis.Convex.Intrinsic

Goal state before:
pp: 𝕜 : Type u_1
V : Type u_2
P : Type u_5
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : CompleteSpace 𝕜
inst✝⁴ : NormedAddCommGroup V
inst✝³ : NormedSpace 𝕜 V
inst✝² : FiniteDimensional 𝕜 V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s : Set P
⊢ intrinsicClosure 𝕜 s = closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s

Tactic:
ext x
  simp only [mem_closure_iff, mem_intrinsicClosure]
  refine ⟨?_, fun h => ⟨⟨x, _⟩, ?_, Subtype.coe_mk _ ?_⟩⟩
  · rintro ⟨x, h, rfl⟩ t ht hx
    obtain ⟨z, hz₁, hz₂⟩ := h _ (continuous_induced_dom.isOpen_preimage t ht) hx
    exact ⟨z, hz₁, hz₂⟩
  · rintro _ ⟨t, ht, rfl⟩ hx
    obtain ⟨y, hyt, hys⟩ := h _ ht hx
    exact ⟨⟨_, subset_affineSpan 𝕜 s hys⟩, hyt, hys⟩
  · by_contra hc
    obtain ⟨z, hz₁, hz₂⟩ := h _ (affineSpan 𝕜 s).closed_of_finiteDimensional.isOpen_compl hc
    exact hz₁ (subset_affineSpan 𝕜 s hz₂)

Goal state after:
Module: Mathlib.Geometry.Convex.ConvexSpace.Defs

Goal state before:
pp: case pos
R : Type u
inst✝² : PartialOrder R
inst✝¹ : Semiring R
M : Type u_9
N : Type u_10
inst✝ : IsStrictOrderedRing R
f : StdSimplex R M
x a : N
h✝ : x = a
⊢ (map (fun x_1 ↦ x) f).weights a = (single x).weights a

pp: case neg
R : Type u
inst✝² : PartialOrder R
inst✝¹ : Semiring R
M : Type u_9
N : Type u_10
inst✝ : IsStrictOrderedRing R
f : StdSimplex R M
x a : N
h✝ : ¬x = a
⊢ (map (fun x_1 ↦ x) f).weights a = (single x).weights a

Tactic:
<;>

Goal state after:
case pos
R : Type u
inst✝² : PartialOrder R
inst✝¹ : Semiring R
M : Type u_9
N : Type u_10
inst✝ : IsStrictOrderedRing R
f : StdSimplex R M
x a : N
h✝ : x = a
⊢ (map (fun x_1 ↦ x) f).weights a = (single x).weights a

case neg
R : Type u
inst✝² : PartialOrder R
inst✝¹ : Semiring R
M : Type u_9
N : Type u_10
inst✝ : IsStrictOrderedRing R
f : StdSimplex R M
x a : N
h✝ : ¬x = a
⊢ (map (fun x_1 ↦ x) f).weights a = (single x).weights a
Module: Mathlib.Geometry.Convex.ConvexSpace.Defs

Goal state before:
pp: R : Type u_1
M : Type u_3
inst✝³ : PartialOrder R
inst✝² : Semiring R
inst✝¹ : IsStrictOrderedRing R
inst✝ : ConvexSpace R M
s t : R
hs : 0 ≤ s
ht : 0 ≤ t
h : s + t = 1
J₁ : Type u₁
J₂ : Type u₂
g₁ : StdSimplex R J₁
g₂ : StdSimplex R J₂
m₁ : J₁ → M
m₂ : J₂ → M
⊢ convexCombPair s t hs ht h (iConvexComb g₁ m₁) (iConvexComb g₂ m₂) =
    sConvexComb (convexCombPair s t hs ht h (map m₁ g₁) (map m₂ g₂))

Tactic:
have := iConvexComb_assoc'' (I := Fin 2) (.duple 0 1 hs ht h)
    (J := ![ULift.{max u₁ u₂} J₁, ULift.{max u₁ u₂} J₂])
    (M := M) (Fin.cons (g₁.map ULift.up) (Fin.cons (g₂.map ULift.up) nofun))
    (Fin.cons (m₁ ∘ ULift.down) (Fin.cons (m₂ ∘ ULift.down) nofun))

Goal state after:
R : Type u_1
M : Type u_3
inst✝³ : PartialOrder R
inst✝² : Semiring R
inst✝¹ : IsStrictOrderedRing R
inst✝ : ConvexSpace R M
s t : R
hs : 0 ≤ s
ht : 0 ≤ t
h : s + t = 1
J₁ : Type u₁
J₂ : Type u₂
g₁ : StdSimplex R J₁
g₂ : StdSimplex R J₂
m₁ : J₁ → M
m₂ : J₂ → M
this :
  (iConvexComb (duple 0 1 hs ht h) fun i ↦
      iConvexComb (Fin.cons (map ULift.up g₁) (Fin.cons (map ULift.up g₂) fun a ↦ nomatch a) i)
        (Fin.cons (m₁ ∘ ULift.down) (Fin.cons (m₂ ∘ ULift.down) fun a a_1 ↦ nomatch a, a_1) i)) =
    iConvexComb
      (iConvexComb (duple 0 1 hs ht h) fun i ↦
        map (fun x ↦ ⟨i, x⟩) (Fin.cons (map ULift.up g₁) (Fin.cons (map ULift.up g₂) fun a ↦ nomatch a) i))
      (Sigma.uncurry (Fin.cons (m₁ ∘ ULift.down) (Fin.cons (m₂ ∘ ULift.down) fun a a_1 ↦ nomatch a, a_1)))
⊢ convexCombPair s t hs ht h (iConvexComb g₁ m₁) (iConvexComb g₂ m₂) =
    sConvexComb (convexCombPair s t hs ht h (map m₁ g₁) (map m₂ g₂))
Module: Mathlib.Geometry.Convex.ConvexSpace.Defs

Goal state before:
pp: R : Type u_1
M : Type u_3
I : Type u_6
inst✝³ : PartialOrder R
inst✝² : Semiring R
inst✝¹ : IsStrictOrderedRing R
inst✝ : ConvexSpace R M
s t : I → R
hs : ∀ (i : I), 0 ≤ s i
ht : ∀ (i : I), 0 ≤ t i
h : ∀ (i : I), s i + t i = 1
f : StdSimplex R I
m₁ m₂ : I → M
⊢ (iConvexComb f fun i ↦ convexCombPair (s i) (t i) ⋯ ⋯ ⋯ (m₁ i) (m₂ i)) =
    sConvexComb (iConvexComb f fun i ↦ duple (m₁ i) (m₂ i) ⋯ ⋯ ⋯)

Tactic:
have := iConvexComb_assoc' (I := I) (J := Fin 2) (R := R) (M := M) f
    (fun i ↦ .duple 0 1 (hs i) (ht i) (h i)) (fun i ↦ ![m₁ i, m₂ i])
  simp [iConvexComb, map_sConvexComb, map_map] at this
  simp only [← convexCombPair.eq_def] at this
  simp only [← iConvexComb.eq_def] at this
  simpa [convexCombPair, ← convexCombPair_def]

Goal state after:
Module: Mathlib.Geometry.Convex.Set

Goal state before:
pp: case inl
R : Type u_3
X : Type u_5
inst✝³ : Semiring R
inst✝² : PartialOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : ConvexSpace R X
hs : ∅.Subsingleton
⊢ IsConvexSet R ∅

pp: case inr
R : Type u_3
X : Type u_5
inst✝³ : Semiring R
inst✝² : PartialOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : ConvexSpace R X
x : X
hs : {x}.Subsingleton
⊢ IsConvexSet R {x}

Tactic:
<;>

Goal state after:
case inl
R : Type u_3
X : Type u_5
inst✝³ : Semiring R
inst✝² : PartialOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : ConvexSpace R X
hs : ∅.Subsingleton
⊢ IsConvexSet R ∅

case inr
R : Type u_3
X : Type u_5
inst✝³ : Semiring R
inst✝² : PartialOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : ConvexSpace R X
x : X
hs : {x}.Subsingleton
⊢ IsConvexSet R {x}
Module: Mathlib.Geometry.Convex.Set

Goal state before:
pp: case isTrue
R : Type u_3
X : Type u_5
Y : Type u_6
inst✝⁴ : Semiring R
inst✝³ : PartialOrder R
inst✝² : IsStrictOrderedRing R
inst✝¹ : ConvexSpace R X
inst✝ : ConvexSpace R Y
f : X → Y
s : Set X
hf : IsAffineMap R f
hs : IsConvexSet R s
w : StdSimplex R Y
hw : ↑w.weights.support ⊆ f '' s
u : Finset X
hus : ↑u ⊆ s
hfu : InjOn f ↑u
huw : Finset.image f u = w.weights.support
x : X
h✝ : x ∈ u
⊢ 0 ≤ w.weights (f x)

pp: case isFalse
R : Type u_3
X : Type u_5
Y : Type u_6
inst✝⁴ : Semiring R
inst✝³ : PartialOrder R
inst✝² : IsStrictOrderedRing R
inst✝¹ : ConvexSpace R X
inst✝ : ConvexSpace R Y
f : X → Y
s : Set X
hf : IsAffineMap R f
hs : IsConvexSet R s
w : StdSimplex R Y
hw : ↑w.weights.support ⊆ f '' s
u : Finset X
hus : ↑u ⊆ s
hfu : InjOn f ↑u
huw : Finset.image f u = w.weights.support
x : X
h✝ : x ∉ u
⊢ 0 ≤ 0

Tactic:
<;>

Goal state after:
case isTrue
R : Type u_3
X : Type u_5
Y : Type u_6
inst✝⁴ : Semiring R
inst✝³ : PartialOrder R
inst✝² : IsStrictOrderedRing R
inst✝¹ : ConvexSpace R X
inst✝ : ConvexSpace R Y
f : X → Y
s : Set X
hf : IsAffineMap R f
hs : IsConvexSet R s
w : StdSimplex R Y
hw : ↑w.weights.support ⊆ f '' s
u : Finset X
hus : ↑u ⊆ s
hfu : InjOn f ↑u
huw : Finset.image f u = w.weights.support
x : X
h✝ : x ∈ u
⊢ 0 ≤ w.weights (f x)

case isFalse
R : Type u_3
X : Type u_5
Y : Type u_6
inst✝⁴ : Semiring R
inst✝³ : PartialOrder R
inst✝² : IsStrictOrderedRing R
inst✝¹ : ConvexSpace R X
inst✝ : ConvexSpace R Y
f : X → Y
s : Set X
hf : IsAffineMap R f
hs : IsConvexSet R s
w : StdSimplex R Y
hw : ↑w.weights.support ⊆ f '' s
u : Finset X
hus : ↑u ⊆ s
hfu : InjOn f ↑u
huw : Finset.image f u = w.weights.support
x : X
h✝ : x ∉ u
⊢ 0 ≤ 0
Module: Mathlib.Geometry.Convex.ConvexSpace.Defs

Goal state before:
pp: case e'_2.«0»
R : Type u_9
M : Type u_10
I : Type u_11
inst✝³ : PartialOrder R
inst✝² : CommSemiring R
inst✝¹ : IsStrictOrderedRing R
inst✝ : ConvexSpace R M
s t : R
hs : 0 ≤ s
ht : 0 ≤ t
h : s + t = 1
f : StdSimplex R I
e₁ e₂ : I → M
i : I
a✝¹ : f.weights i ≠ 0
a✝ : (duple 0 1 hs ht h).weights ((fun i ↦ i) ⟨0, ⋯⟩) ≠ 0
⊢ ![e₁ i, e₂ i] ((fun i ↦ i) ⟨0, ⋯⟩) = ![e₁, e₂] ((fun i ↦ i) ⟨0, ⋯⟩) i

pp: case e'_2.«1»
R : Type u_9
M : Type u_10
I : Type u_11
inst✝³ : PartialOrder R
inst✝² : CommSemiring R
inst✝¹ : IsStrictOrderedRing R
inst✝ : ConvexSpace R M
s t : R
hs : 0 ≤ s
ht : 0 ≤ t
h : s + t = 1
f : StdSimplex R I
e₁ e₂ : I → M
i : I
a✝¹ : f.weights i ≠ 0
a✝ : (duple 0 1 hs ht h).weights ((fun i ↦ i) ⟨1, ⋯⟩) ≠ 0
⊢ ![e₁ i, e₂ i] ((fun i ↦ i) ⟨1, ⋯⟩) = ![e₁, e₂] ((fun i ↦ i) ⟨1, ⋯⟩) i

Tactic:
<;>

Goal state after:
case e'_2.«0»
R : Type u_9
M : Type u_10
I : Type u_11
inst✝³ : PartialOrder R
inst✝² : CommSemiring R
inst✝¹ : IsStrictOrderedRing R
inst✝ : ConvexSpace R M
s t : R
hs : 0 ≤ s
ht : 0 ≤ t
h : s + t = 1
f : StdSimplex R I
e₁ e₂ : I → M
i : I
a✝¹ : f.weights i ≠ 0
a✝ : (duple 0 1 hs ht h).weights ((fun i ↦ i) ⟨0, ⋯⟩) ≠ 0
⊢ ![e₁ i, e₂ i] ((fun i ↦ i) ⟨0, ⋯⟩) = ![e₁, e₂] ((fun i ↦ i) ⟨0, ⋯⟩) i

case e'_2.«1»
R : Type u_9
M : Type u_10
I : Type u_11
inst✝³ : PartialOrder R
inst✝² : CommSemiring R
inst✝¹ : IsStrictOrderedRing R
inst✝ : ConvexSpace R M
s t : R
hs : 0 ≤ s
ht : 0 ≤ t
h : s + t = 1
f : StdSimplex R I
e₁ e₂ : I → M
i : I
a✝¹ : f.weights i ≠ 0
a✝ : (duple 0 1 hs ht h).weights ((fun i ↦ i) ⟨1, ⋯⟩) ≠ 0
⊢ ![e₁ i, e₂ i] ((fun i ↦ i) ⟨1, ⋯⟩) = ![e₁, e₂] ((fun i ↦ i) ⟨1, ⋯⟩) i