-- Mathlib/Analysis/Convex/Extrema.lean
theorem IsMinOn.of_isLocalMinOn_of_convexOn {f : E → β} {a : E} (a_in_s : a ∈ s)
    (h_localmin : IsLocalMinOn f s a) (h_conv : ConvexOn ℝ s f) : IsMinOn f s a

Proof state:
E : Type u_1
β : Type u_2
inst✝⁷ : AddCommGroup E
inst✝⁶ : TopologicalSpace E
inst✝⁵ : Module ℝ E
inst✝⁴ : IsTopologicalAddGroup E
inst✝³ : ContinuousSMul ℝ E
inst✝² : OrderedAddCommGroup β
inst✝¹ : Module ℝ β
inst✝ : OrderedSMul ℝ β
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 ⇑g
⊢ x ∈ {x | (fun x => f a ≤ f x) x}

Tactic:
have h_maps : MapsTo g (Icc 0 1) s := by
  simpa only [g, mapsTo', ← segment_eq_image_lineMap] using h_conv.1.segment_subset a_in_s x_in_s

Result:
E : Type u_1
β : Type u_2
inst✝⁷ : AddCommGroup E
inst✝⁶ : TopologicalSpace E
inst✝⁵ : Module ℝ E
inst✝⁴ : IsTopologicalAddGroup E
inst✝³ : ContinuousSMul ℝ E
inst✝² : OrderedAddCommGroup β
inst✝¹ : Module ℝ β
inst✝ : OrderedSMul ℝ β
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 ⇑g
h_maps : MapsTo (⇑g) (Icc 0 1) s
⊢ x ∈ {x | (fun x => f a ≤ f x) x}

Proof state:
E : Type u_1
β : Type u_2
inst✝⁷ : AddCommGroup E
inst✝⁶ : TopologicalSpace E
inst✝⁵ : Module ℝ E
inst✝⁴ : IsTopologicalAddGroup E
inst✝³ : ContinuousSMul ℝ E
inst✝² : OrderedAddCommGroup β
inst✝¹ : Module ℝ β
inst✝ : OrderedSMul ℝ β
s : Set E
f : E → β
a : E
a_in_s : a ∈ s
h_localmin : IsLocalMinOn f s a
h_conv : ConvexOn ℝ s f
⊢ IsMinOn f s a

Tactic:
intro x x_in_s

Result:
E : Type u_1
β : Type u_2
inst✝⁷ : AddCommGroup E
inst✝⁶ : TopologicalSpace E
inst✝⁵ : Module ℝ E
inst✝⁴ : IsTopologicalAddGroup E
inst✝³ : ContinuousSMul ℝ E
inst✝² : OrderedAddCommGroup β
inst✝¹ : Module ℝ β
inst✝ : OrderedSMul ℝ β
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
⊢ x ∈ {x | (fun x => f a ≤ f x) x}

Proof state:
E : Type u_1
β : Type u_2
inst✝⁷ : AddCommGroup E
inst✝⁶ : TopologicalSpace E
inst✝⁵ : Module ℝ E
inst✝⁴ : IsTopologicalAddGroup E
inst✝³ : ContinuousSMul ℝ E
inst✝² : OrderedAddCommGroup β
inst✝¹ : Module ℝ β
inst✝ : OrderedSMul ℝ β
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 ⇑g
h_maps : MapsTo (⇑g) (Icc 0 1) s
⊢ x ∈ {x | (fun x => f a ≤ f x) x}

Tactic:
have fg_local_min_on : IsLocalMinOn (f ∘ g) (Icc 0 1) 0 := by
  rw [← hg0] at h_localmin
  exact h_localmin.comp_continuousOn h_maps hgc.continuousOn (left_mem_Icc.2 zero_le_one)

Result:
E : Type u_1
β : Type u_2
inst✝⁷ : AddCommGroup E
inst✝⁶ : TopologicalSpace E
inst✝⁵ : Module ℝ E
inst✝⁴ : IsTopologicalAddGroup E
inst✝³ : ContinuousSMul ℝ E
inst✝² : OrderedAddCommGroup β
inst✝¹ : Module ℝ β
inst✝ : OrderedSMul ℝ β
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 ⇑g
h_maps : MapsTo (⇑g) (Icc 0 1) s
fg_local_min_on : IsLocalMinOn (f ∘ ⇑g) (Icc 0 1) 0
⊢ x ∈ {x | (fun x => f a ≤ f x) x}

Proof state:
E : Type u_1
β : Type u_2
inst✝⁷ : AddCommGroup E
inst✝⁶ : TopologicalSpace E
inst✝⁵ : Module ℝ E
inst✝⁴ : IsTopologicalAddGroup E
inst✝³ : ContinuousSMul ℝ E
inst✝² : OrderedAddCommGroup β
inst✝¹ : Module ℝ β
inst✝ : OrderedSMul ℝ β
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 ⇑g
h_maps : MapsTo (⇑g) (Icc 0 1) s
fg_local_min_on : IsLocalMinOn (f ∘ ⇑g) (Icc 0 1) 0
⊢ IsMinOn (f ∘ ⇑g) (Icc 0 1) 0

Tactic:
refine IsMinOn.of_isLocalMinOn_of_convexOn_Icc one_pos fg_local_min_on ?_

Result:
E : Type u_1
β : Type u_2
inst✝⁷ : AddCommGroup E
inst✝⁶ : TopologicalSpace E
inst✝⁵ : Module ℝ E
inst✝⁴ : IsTopologicalAddGroup E
inst✝³ : ContinuousSMul ℝ E
inst✝² : OrderedAddCommGroup β
inst✝¹ : Module ℝ β
inst✝ : OrderedSMul ℝ β
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 ⇑g
h_maps : MapsTo (⇑g) (Icc 0 1) s
fg_local_min_on : IsLocalMinOn (f ∘ ⇑g) (Icc 0 1) 0
⊢ ConvexOn ℝ (Icc 0 1) (f ∘ ⇑g)

Proof state:
E : Type u_1
β : Type u_2
inst✝⁷ : AddCommGroup E
inst✝⁶ : TopologicalSpace E
inst✝⁵ : Module ℝ E
inst✝⁴ : IsTopologicalAddGroup E
inst✝³ : ContinuousSMul ℝ E
inst✝² : OrderedAddCommGroup β
inst✝¹ : Module ℝ β
inst✝ : OrderedSMul ℝ β
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 ⇑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 only [hg0, hg1, comp_apply, mem_setOf_eq] using fg_min_on (right_mem_Icc.2 zero_le_one)

Result:
no goals

Proof state:
E : Type u_1
β : Type u_2
inst✝⁷ : AddCommGroup E
inst✝⁶ : TopologicalSpace E
inst✝⁵ : Module ℝ E
inst✝⁴ : IsTopologicalAddGroup E
inst✝³ : ContinuousSMul ℝ E
inst✝² : OrderedAddCommGroup β
inst✝¹ : Module ℝ β
inst✝ : OrderedSMul ℝ β
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
⊢ x ∈ {x | (fun x => f a ≤ f x) x}

Tactic:
have hgc : Continuous g := AffineMap.lineMap_continuous

Result:
E : Type u_1
β : Type u_2
inst✝⁷ : AddCommGroup E
inst✝⁶ : TopologicalSpace E
inst✝⁵ : Module ℝ E
inst✝⁴ : IsTopologicalAddGroup E
inst✝³ : ContinuousSMul ℝ E
inst✝² : OrderedAddCommGroup β
inst✝¹ : Module ℝ β
inst✝ : OrderedSMul ℝ β
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 ⇑g
⊢ x ∈ {x | (fun x => f a ≤ f x) x}