awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Convex.Extrema
Goal:
β : Type u_2
inst : AddCommGroup β
inst_1 : PartialOrder β
inst_2 : IsOrderedAddMonoid β
inst_3 : Module ℝ β
inst_4 : IsOrderedModule ℝ β
inst_5 : PosSMulReflectLE ℝ β
f : ℝ → β
a b : ℝ
a_lt_b : a < b
h_local_min : IsLocalMinOn f (Icc a b) a
h_conv : ConvexOn ℝ (Icc a b) f
c : ℝ
hc : c ∈ Icc a b
rw : ∀ (h_local_min : IsMinFilter f (𝓝[≥] a) a) (h_conv : ConvexOn ℝ (Icc a b) f) ⦃c : ℝ⦄ (hc : c ∈ Icc a b), f a ≤ f c
⊢ f a ≤ f c

Tactic:
rw [IsLocalMinOn, nhdsWithin_Icc_eq_nhdsGE a_lt_b] at h_local_min

Premises used: IsLocalMinOn, nhdsWithin_Icc_eq_nhdsGE
-- Module: Mathlib.Analysis.Convex.Extrema
Goal:
β : Type u_2
inst : AddCommGroup β
inst_1 : PartialOrder β
inst_2 : IsOrderedAddMonoid β
inst_3 : Module ℝ β
inst_4 : IsOrderedModule ℝ β
inst_5 : PosSMulReflectLE ℝ β
f : ℝ → β
a b : ℝ
a_lt_b : a < b
h_local_min : IsMinFilter f (𝓝[≥] a) a
h_conv : ConvexOn ℝ (Icc a b) f
c : ℝ
hc : c ∈ Icc a b
inl : ∀ (hc : a ∈ Icc a b), f a ≤ f a
inr : ∀ (a_lt_c : a < c), f a ≤ f c
⊢ f a ≤ f c

Tactic:
rcases hc.1.eq_or_lt with (rfl | a_lt_c)

Premises used: LE.le.eq_or_lt, And.left, rfl
-- Module: Mathlib.Analysis.Convex.Extrema
Goal:
β : Type u_2
inst : AddCommGroup β
inst_1 : PartialOrder β
inst_2 : IsOrderedAddMonoid β
inst_3 : Module ℝ β
inst_4 : IsOrderedModule ℝ β
inst_5 : PosSMulReflectLE ℝ β
f : ℝ → β
a b : ℝ
a_lt_b : a < b
h_local_min : IsMinFilter f (𝓝[≥] a) a
h_conv : ConvexOn ℝ (Icc a b) f
hc : a ∈ Icc a b
⊢ f a ≤ f a

Tactic:
le_rfl

Premises used: le_rfl
-- Module: Mathlib.Analysis.Convex.Extrema
Goal:
β : Type u_2
inst : AddCommGroup β
inst_1 : PartialOrder β
inst_2 : IsOrderedAddMonoid β
inst_3 : Module ℝ β
inst_4 : IsOrderedModule ℝ β
inst_5 : PosSMulReflectLE ℝ β
f : ℝ → β
a b : ℝ
a_lt_b : a < b
h_local_min : IsMinFilter f (𝓝[≥] a) a
h_conv : ConvexOn ℝ (Icc a b) f
hc : a ∈ Icc a b
⊢ f a ≤ f a

Tactic:
exact le_rfl

Premises used: le_rfl
-- Module: Mathlib.Analysis.Convex.Extrema
Goal:
β : Type u_2
inst : AddCommGroup β
inst_1 : PartialOrder β
inst_2 : IsOrderedAddMonoid β
inst_3 : Module ℝ β
inst_4 : IsOrderedModule ℝ β
inst_5 : PosSMulReflectLE ℝ β
f : ℝ → β
a b : ℝ
a_lt_b : a < b
h_local_min : IsMinFilter f (𝓝[≥] a) a
h_conv : ConvexOn ℝ (Icc a b) f
c : ℝ
hc : c ∈ Icc a b
a_lt_c : a < c
⊢ ∀ᶠ (y : ℝ) in 𝓝[>] a, f a ≤ f y

Tactic:
have H₁ : ∀ᶠ y in 𝓝[>] a, f a ≤ f y :=
    h_local_min.filter_mono (nhdsWithin_mono _ Ioi_subset_Ici_self)
-- Module: Mathlib.Analysis.Convex.Extrema
Goal:
β : Type u_2
inst : AddCommGroup β
inst_1 : PartialOrder β
inst_2 : IsOrderedAddMonoid β
inst_3 : Module ℝ β
inst_4 : IsOrderedModule ℝ β
inst_5 : PosSMulReflectLE ℝ β
f : ℝ → β
a b : ℝ
a_lt_b : a < b
h_local_min : IsMinFilter f (𝓝[≥] a) a
h_conv : ConvexOn ℝ (Icc a b) f
c : ℝ
hc : c ∈ Icc a b
a_lt_c : a < c
H₁ : ∀ᶠ (y : ℝ) in 𝓝[>] a, f a ≤ f y
⊢ ∀ᶠ (y : ℝ) in 𝓝[>] a, y ∈ Ioc a c

Tactic:
have H₂ : ∀ᶠ y in 𝓝[>] a, y ∈ Ioc a c := Ioc_mem_nhdsGT a_lt_c
-- Module: Mathlib.Analysis.Convex.Extrema
Goal:
β : Type u_2
inst : AddCommGroup β
inst_1 : PartialOrder β
inst_2 : IsOrderedAddMonoid β
inst_3 : Module ℝ β
inst_4 : IsOrderedModule ℝ β
inst_5 : PosSMulReflectLE ℝ β
f : ℝ → β
a b : ℝ
a_lt_b : a < b
h_local_min : IsMinFilter f (𝓝[≥] a) a
h_conv : ConvexOn ℝ (Icc a b) f
c : ℝ
hc : c ∈ Icc a b
a_lt_c : a < c
H₁ : ∀ᶠ (y : ℝ) in 𝓝[>] a, f a ≤ f y
H₂ : ∀ᶠ (y : ℝ) in 𝓝[>] a, y ∈ Ioc a c
inr : ∀ (y : ℝ) (hfy : f a ≤ f y) (hy_ac : y ∈ Ioc a c), f a ≤ f c
⊢ f a ≤ f c

Tactic:
rcases (H₁.and H₂).exists with ⟨y, hfy, hy_ac⟩

Premises used: Filter.Eventually.and, Filter.Eventually.exists
-- Module: Mathlib.Analysis.Convex.Extrema
Goal:
β : Type u_2
inst : AddCommGroup β
inst_1 : PartialOrder β
inst_2 : IsOrderedAddMonoid β
inst_3 : Module ℝ β
inst_4 : IsOrderedModule ℝ β
inst_5 : PosSMulReflectLE ℝ β
f : ℝ → β
a b : ℝ
a_lt_b : a < b
h_local_min : IsMinFilter f (𝓝[≥] a) a
h_conv : ConvexOn ℝ (Icc a b) f
c : ℝ
hc : c ∈ Icc a b
a_lt_c : a < c
H₁ : ∀ᶠ (y : ℝ) in 𝓝[>] a, f a ≤ f y
H₂ : ∀ᶠ (y : ℝ) in 𝓝[>] a, y ∈ Ioc a c
y : ℝ
hfy : f a ≤ f y
hy_ac : y ∈ Ioc a c
inr :
  ∀ (ya yc : ℝ) (ya₀ : 0 ≤ ya) (yc₀ : 0 < yc) (yac : ya + yc = 1) (hfy : f a ≤ f (ya * a + yc * c))
    (hy_ac : ya * a + yc * c ∈ Ioc a c), f a ≤ f c
⊢ f a ≤ f c

Tactic:
rcases (Convex.mem_Ioc a_lt_c).mp hy_ac with ⟨ya, yc, ya₀, yc₀, yac, rfl⟩

Premises used: Iff.mp, rfl, Convex.mem_Ioc
-- Module: Mathlib.Analysis.Convex.Extrema
Goal:
β : Type u_2
inst : AddCommGroup β
inst_1 : PartialOrder β
inst_2 : IsOrderedAddMonoid β
inst_3 : Module ℝ β
inst_4 : IsOrderedModule ℝ β
inst_5 : PosSMulReflectLE ℝ β
f : ℝ → β
a b : ℝ
a_lt_b : a < b
h_local_min : IsMinFilter f (𝓝[≥] a) a
h_conv : ConvexOn ℝ (Icc a b) f
c : ℝ
hc : c ∈ Icc a b
a_lt_c : a < c
H₁ : ∀ᶠ (y : ℝ) in 𝓝[>] a, f a ≤ f y
H₂ : ∀ᶠ (y : ℝ) in 𝓝[>] a, y ∈ Ioc a c
ya yc : ℝ
ya₀ : 0 ≤ ya
yc₀ : 0 < yc
yac : ya + yc = 1
hfy : f a ≤ f (ya * a + yc * c)
hy_ac : ya * a + yc * c ∈ Ioc a c
inr : ya • f a + yc • f a ≤ ya • f a + yc • f c
⊢ f a ≤ f c

Tactic:
suffices ya • f a + yc • f a ≤ ya • f a + yc • f c from
    (smul_le_smul_iff_of_pos_left yc₀).1 (le_of_add_le_add_left this)
-- Module: Mathlib.Analysis.Convex.Extrema
Goal:
β : Type u_2
inst : AddCommGroup β
inst_1 : PartialOrder β
inst_2 : IsOrderedAddMonoid β
inst_3 : Module ℝ β
inst_4 : IsOrderedModule ℝ β
inst_5 : PosSMulReflectLE ℝ β
f : ℝ → β
a b : ℝ
a_lt_b : a < b
h_local_min : IsMinFilter f (𝓝[≥] a) a
h_conv : ConvexOn ℝ (Icc a b) f
c : ℝ
hc : c ∈ Icc a b
a_lt_c : a < c
H₁ : ∀ᶠ (y : ℝ) in 𝓝[>] a, f a ≤ f y
H₂ : ∀ᶠ (y : ℝ) in 𝓝[>] a, y ∈ Ioc a c
ya yc : ℝ
ya₀ : 0 ≤ ya
yc₀ : 0 < yc
yac : ya + yc = 1
hfy : f a ≤ f (ya * a + yc * c)
hy_ac : ya * a + yc * c ∈ Ioc a c
rw : (ya + yc) • f a = f a
rw₁ : HSMul.hSMul (α := ℝ) 1 (f a) = f a
rw₂ rw₃ : f a = f a
⊢ ya • f a + yc • f a = f a

Tactic:
rw [← add_smul, yac, one_smul]

Premises used: one_smul, add_smul
-- Module: Mathlib.Analysis.Convex.Extrema
Goal:
β : Type u_2
inst : AddCommGroup β
inst_1 : PartialOrder β
inst_2 : IsOrderedAddMonoid β
inst_3 : Module ℝ β
inst_4 : IsOrderedModule ℝ β
inst_5 : PosSMulReflectLE ℝ β
f : ℝ → β
a b : ℝ
a_lt_b : a < b
h_local_min : IsMinFilter f (𝓝[≥] a) a
h_conv : ConvexOn ℝ (Icc a b) f
c : ℝ
hc : c ∈ Icc a b
a_lt_c : a < c
H₁ : ∀ᶠ (y : ℝ) in 𝓝[>] a, f a ≤ f y
H₂ : ∀ᶠ (y : ℝ) in 𝓝[>] a, y ∈ Ioc a c
ya yc : ℝ
ya₀ : 0 ≤ ya
yc₀ : 0 < yc
yac : ya + yc = 1
hfy : f a ≤ f (ya * a + yc * c)
hy_ac : ya * a + yc * c ∈ Ioc a c
⊢ f a ≤ f (ya * a + yc * c)

Tactic:
hfy
-- Module: Mathlib.Analysis.Convex.Extrema
Goal:
β : Type u_2
inst : AddCommGroup β
inst_1 : PartialOrder β
inst_2 : IsOrderedAddMonoid β
inst_3 : Module ℝ β
inst_4 : IsOrderedModule ℝ β
inst_5 : PosSMulReflectLE ℝ β
f : ℝ → β
a b : ℝ
a_lt_b : a < b
h_local_min : IsMinFilter f (𝓝[≥] a) a
h_conv : ConvexOn ℝ (Icc a b) f
c : ℝ
hc : c ∈ Icc a b
a_lt_c : a < c
H₁ : ∀ᶠ (y : ℝ) in 𝓝[>] a, f a ≤ f y
H₂ : ∀ᶠ (y : ℝ) in 𝓝[>] a, y ∈ Ioc a c
ya yc : ℝ
ya₀ : 0 ≤ ya
yc₀ : 0 < yc
yac : ya + yc = 1
hfy : f a ≤ f (ya * a + yc * c)
hy_ac : ya * a + yc * c ∈ Ioc a c
⊢ f (ya * a + yc * c) ≤ ya • f a + yc • f c

Tactic:
h_conv.2 (left_mem_Icc.2 a_lt_b.le) hc ya₀ yc₀.le yac

Premises used: Iff.mpr, LT.lt.le, And.right, Set.left_mem_Icc
-- Module: Mathlib.Analysis.Convex.Extrema
Goal:
β : Type u_2
inst : AddCommGroup β
inst_1 : PartialOrder β
inst_2 : IsOrderedAddMonoid β
inst_3 : Module ℝ β
inst_4 : IsOrderedModule ℝ β
inst_5 : PosSMulReflectLE ℝ β
f : ℝ → β
a b : ℝ
a_lt_b : a < b
h_local_min : IsMinFilter f (𝓝[≥] a) a
h_conv : ConvexOn ℝ (Icc a b) f
c : ℝ
hc : c ∈ Icc a b
a_lt_c : a < c
H₁ : ∀ᶠ (y : ℝ) in 𝓝[>] a, f a ≤ f y
H₂ : ∀ᶠ (y : ℝ) in 𝓝[>] a, y ∈ Ioc a c
ya yc : ℝ
ya₀ : 0 ≤ ya
yc₀ : 0 < yc
yac : ya + yc = 1
hfy : f a ≤ f (ya * a + yc * c)
hy_ac : ya * a + yc * c ∈ Ioc a c
ya₁ : ya • f a + yc • f a = f a
⊢ ya • f a + yc • f a ≤ ya • f a + yc • f c

Tactic:
calc
    ya • f a + yc • f a = f a := by rw [← add_smul, yac, one_smul]
    _ ≤ f (ya * a + yc * c) := hfy
    _ ≤ ya • f a + yc • f c := h_conv.2 (left_mem_Icc.2 a_lt_b.le) hc ya₀ yc₀.le yac

Premises used: Iff.mpr, HMul.hMul, LT.lt.le, And.right, HAdd.hAdd, Set.left_mem_Icc
-- Module: Mathlib.Analysis.Convex.Extrema
Goal:
E : Type u_1
β : Type u_2
inst : AddCommGroup E
inst_1 : TopologicalSpace E
inst_2 : Module ℝ E
inst_3 : IsTopologicalAddGroup E
inst_4 : ContinuousSMul ℝ E
inst_5 : AddCommGroup β
inst_6 : PartialOrder β
inst_7 : IsOrderedAddMonoid β
inst_8 : Module ℝ β
inst_9 : IsOrderedModule ℝ β
inst_10 : 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
⊢ (g : (a : ℝ) → E) 0 = a

Tactic:
have hg0 : g 0 = a := AffineMap.lineMap_apply_zero a x
-- Module: Mathlib.Analysis.Convex.Extrema
Goal:
E : Type u_1
β : Type u_2
inst : AddCommGroup E
inst_1 : TopologicalSpace E
inst_2 : Module ℝ E
inst_3 : IsTopologicalAddGroup E
inst_4 : ContinuousSMul ℝ E
inst_5 : AddCommGroup β
inst_6 : PartialOrder β
inst_7 : IsOrderedAddMonoid β
inst_8 : Module ℝ β
inst_9 : IsOrderedModule ℝ β
inst_10 : 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 : (a : ℝ) → E) 0 = a
⊢ (g : (a : ℝ) → E) 1 = x

Tactic:
have hg1 : g 1 = x := AffineMap.lineMap_apply_one a x
-- Module: Mathlib.Analysis.Convex.Extrema
Goal:
E : Type u_1
β : Type u_2
inst : AddCommGroup E
inst_1 : TopologicalSpace E
inst_2 : Module ℝ E
inst_3 : IsTopologicalAddGroup E
inst_4 : ContinuousSMul ℝ E
inst_5 : AddCommGroup β
inst_6 : PartialOrder β
inst_7 : IsOrderedAddMonoid β
inst_8 : Module ℝ β
inst_9 : IsOrderedModule ℝ β
inst_10 : 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 : (a : ℝ) → E) 0 = a
hg1 : (g : (a : ℝ) → E) 1 = x
⊢ Continuous[_, inst_1] (⇑g : (a : ℝ) → E)

Tactic:
have hgc : Continuous g := AffineMap.lineMap_continuous
-- Module: Mathlib.Analysis.Convex.Extrema
Goal:
E : Type u_1
β : Type u_2
inst : AddCommGroup E
inst_1 : TopologicalSpace E
inst_2 : Module ℝ E
inst_3 : IsTopologicalAddGroup E
inst_4 : ContinuousSMul ℝ E
inst_5 : AddCommGroup β
inst_6 : PartialOrder β
inst_7 : IsOrderedAddMonoid β
inst_8 : Module ℝ β
inst_9 : IsOrderedModule ℝ β
inst_10 : 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 : (a : ℝ) → E) 0 = a
hg1 : (g : (a : ℝ) → E) 1 = x
hgc : Continuous[_, inst_1] (⇑g : (a : ℝ) → E)
⊢ MapsTo (α := ℝ) (⇑g : (a : ℝ) → E) (Icc 0 1) s

Tactic:
simpa only [g, mapsTo_iff_image_subset, ← segment_eq_image_lineMap]
      using h_conv.1.segment_subset a_in_s x_in_s

Premises used: Set.mapsTo_iff_image_subset, And.left, segment_eq_image_lineMap, Convex.segment_subset
-- Module: Mathlib.Analysis.Convex.Extrema
Goal:
E : Type u_1
β : Type u_2
inst : AddCommGroup E
inst_1 : TopologicalSpace E
inst_2 : Module ℝ E
inst_3 : IsTopologicalAddGroup E
inst_4 : ContinuousSMul ℝ E
inst_5 : AddCommGroup β
inst_6 : PartialOrder β
inst_7 : IsOrderedAddMonoid β
inst_8 : Module ℝ β
inst_9 : IsOrderedModule ℝ β
inst_10 : 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 : (a : ℝ) → E) 0 = a
hg1 : (g : (a : ℝ) → E) 1 = x
hgc : Continuous[_, inst_1] (⇑g : (a : ℝ) → E)
⊢ MapsTo (α := ℝ) (⇑g : (a : ℝ) → E) (Icc 0 1) s

Tactic:
have h_maps : MapsTo g (Icc 0 1) s := by
    simpa only [g, mapsTo_iff_image_subset, ← segment_eq_image_lineMap]
      using h_conv.1.segment_subset a_in_s x_in_s
-- Module: Mathlib.Analysis.Convex.Extrema
Goal:
E : Type u_1
β : Type u_2
inst : AddCommGroup E
inst_1 : TopologicalSpace E
inst_2 : Module ℝ E
inst_3 : IsTopologicalAddGroup E
inst_4 : ContinuousSMul ℝ E
inst_5 : AddCommGroup β
inst_6 : PartialOrder β
inst_7 : IsOrderedAddMonoid β
inst_8 : Module ℝ β
inst_9 : IsOrderedModule ℝ β
inst_10 : 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 : (a : ℝ) → E) 0 = a
hg1 : (g : (a : ℝ) → E) 1 = x
hgc : Continuous[_, inst_1] (⇑g : (a : ℝ) → E)
h_maps : MapsTo (α := ℝ) (⇑g : (a : ℝ) → E) (Icc 0 1) s
⊢ IsLocalMinOn f s ((g : (a : ℝ) → E) 0)

Tactic:
rw [← hg0] at h_localmin
-- Module: Mathlib.Analysis.Convex.Extrema
Goal:
E : Type u_1
β : Type u_2
inst : AddCommGroup E
inst_1 : TopologicalSpace E
inst_2 : Module ℝ E
inst_3 : IsTopologicalAddGroup E
inst_4 : ContinuousSMul ℝ E
inst_5 : AddCommGroup β
inst_6 : PartialOrder β
inst_7 : IsOrderedAddMonoid β
inst_8 : Module ℝ β
inst_9 : IsOrderedModule ℝ β
inst_10 : 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 : (a : ℝ) → E) 0 = a
hg1 : (g : (a : ℝ) → E) 1 = x
hgc : Continuous[_, inst_1] (⇑g : (a : ℝ) → E)
h_maps : MapsTo (α := ℝ) (⇑g : (a : ℝ) → E) (Icc 0 1) s
h_localmin₁ : IsLocalMinOn f s ((g : (a : ℝ) → E) 0)
⊢ (g : (a : ℝ) → E) 0 = a

Tactic:
rw [← hg0] at h_localmin
-- Module: Mathlib.Analysis.Convex.Extrema
Goal:
E : Type u_1
β : Type u_2
inst : AddCommGroup E
inst_1 : TopologicalSpace E
inst_2 : Module ℝ E
inst_3 : IsTopologicalAddGroup E
inst_4 : ContinuousSMul ℝ E
inst_5 : AddCommGroup β
inst_6 : PartialOrder β
inst_7 : IsOrderedAddMonoid β
inst_8 : Module ℝ β
inst_9 : IsOrderedModule ℝ β
inst_10 : 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 : (a : ℝ) → E) 0 = a
hg1 : (g : (a : ℝ) → E) 1 = x
hgc : Continuous[_, inst_1] (⇑g : (a : ℝ) → E)
h_maps : MapsTo (α := ℝ) (⇑g : (a : ℝ) → E) (Icc 0 1) s
h_localmin₁ : IsLocalMinOn f s ((g : (a : ℝ) → E) 0)
hg0₁ : (g : (a : ℝ) → E) 0 = a
⊢ (g : (a : ℝ) → E) 1 = x

Tactic:
rw [← hg0] at h_localmin
-- Module: Mathlib.Analysis.Convex.Extrema
Goal:
E : Type u_1
β : Type u_2
inst : AddCommGroup E
inst_1 : TopologicalSpace E
inst_2 : Module ℝ E
inst_3 : IsTopologicalAddGroup E
inst_4 : ContinuousSMul ℝ E
inst_5 : AddCommGroup β
inst_6 : PartialOrder β
inst_7 : IsOrderedAddMonoid β
inst_8 : Module ℝ β
inst_9 : IsOrderedModule ℝ β
inst_10 : 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 : (a : ℝ) → E) 0 = a
hg1 : (g : (a : ℝ) → E) 1 = x
hgc : Continuous[_, inst_1] (⇑g : (a : ℝ) → E)
h_maps : MapsTo (α := ℝ) (⇑g : (a : ℝ) → E) (Icc 0 1) s
h_localmin₁ : IsLocalMinOn f s ((g : (a : ℝ) → E) 0)
hg0₁ : (g : (a : ℝ) → E) 0 = a
hg1₁ : (g : (a : ℝ) → E) 1 = x
⊢ Continuous[_, inst_1] (⇑g : (a : ℝ) → E)

Tactic:
rw [← hg0] at h_localmin
-- Module: Mathlib.Analysis.Convex.Extrema
Goal:
E : Type u_1
β : Type u_2
inst : AddCommGroup E
inst_1 : TopologicalSpace E
inst_2 : Module ℝ E
inst_3 : IsTopologicalAddGroup E
inst_4 : ContinuousSMul ℝ E
inst_5 : AddCommGroup β
inst_6 : PartialOrder β
inst_7 : IsOrderedAddMonoid β
inst_8 : Module ℝ β
inst_9 : IsOrderedModule ℝ β
inst_10 : 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 : (a : ℝ) → E) 0 = a
hg1 : (g : (a : ℝ) → E) 1 = x
hgc : Continuous[_, inst_1] (⇑g : (a : ℝ) → E)
h_maps : MapsTo (α := ℝ) (⇑g : (a : ℝ) → E) (Icc 0 1) s
h_localmin₁ : IsLocalMinOn f s ((g : (a : ℝ) → E) 0)
hg0₁ : (g : (a : ℝ) → E) 0 = a
hg1₁ : (g : (a : ℝ) → E) 1 = x
hgc₁ : Continuous[_, inst_1] (⇑g : (a : ℝ) → E)
⊢ MapsTo (α := ℝ) (⇑g : (a : ℝ) → E) (Icc 0 1) s

Tactic:
rw [← hg0] at h_localmin
-- Module: Mathlib.Analysis.Convex.Extrema
Goal:
E : Type u_1
β : Type u_2
inst : AddCommGroup E
inst_1 : TopologicalSpace E
inst_2 : Module ℝ E
inst_3 : IsTopologicalAddGroup E
inst_4 : ContinuousSMul ℝ E
inst_5 : AddCommGroup β
inst_6 : PartialOrder β
inst_7 : IsOrderedAddMonoid β
inst_8 : Module ℝ β
inst_9 : IsOrderedModule ℝ β
inst_10 : PosSMulReflectLE ℝ β
s : Set E
f : E → β
a : E
a_in_s : a ∈ s
h_conv : ConvexOn ℝ s f
x : E
x_in_s : x ∈ s
g : ℝ →ᵃ[ℝ] E := AffineMap.lineMap a x
h_localmin : IsLocalMinOn f s ((g : (a : ℝ) → E) 0)
hg0 : (g : (a : ℝ) → E) 0 = a
hg1 : (g : (a : ℝ) → E) 1 = x
hgc : Continuous[_, inst_1] (⇑g : (a : ℝ) → E)
h_maps : MapsTo (α := ℝ) (⇑g : (a : ℝ) → E) (Icc 0 1) s
⊢ IsLocalMinOn (α := ℝ) (f ∘ (⇑g : (a : ℝ) → E)) (Icc 0 1) 0

Tactic:
h_localmin.comp_continuousOn h_maps hgc.continuousOn (left_mem_Icc.2 zero_le_one)

Premises used: Iff.mpr, Continuous.continuousOn, IsLocalMinOn.comp_continuousOn, zero_le_one, Set.left_mem_Icc
-- Module: Mathlib.Analysis.Convex.Extrema
Goal:
E : Type u_1
β : Type u_2
inst : AddCommGroup E
inst_1 : TopologicalSpace E
inst_2 : Module ℝ E
inst_3 : IsTopologicalAddGroup E
inst_4 : ContinuousSMul ℝ E
inst_5 : AddCommGroup β
inst_6 : PartialOrder β
inst_7 : IsOrderedAddMonoid β
inst_8 : Module ℝ β
inst_9 : IsOrderedModule ℝ β
inst_10 : PosSMulReflectLE ℝ β
s : Set E
f : E → β
a : E
a_in_s : a ∈ s
h_conv : ConvexOn ℝ s f
x : E
x_in_s : x ∈ s
g : ℝ →ᵃ[ℝ] E := AffineMap.lineMap a x
h_localmin : IsLocalMinOn f s ((g : (a : ℝ) → E) 0)
hg0 : (g : (a : ℝ) → E) 0 = a
hg1 : (g : (a : ℝ) → E) 1 = x
hgc : Continuous[_, inst_1] (⇑g : (a : ℝ) → E)
h_maps : MapsTo (α := ℝ) (⇑g : (a : ℝ) → E) (Icc 0 1) s
⊢ IsLocalMinOn (α := ℝ) (f ∘ (⇑g : (a : ℝ) → E)) (Icc 0 1) 0

Tactic:
exact h_localmin.comp_continuousOn h_maps hgc.continuousOn (left_mem_Icc.2 zero_le_one)

Premises used: Iff.mpr, Continuous.continuousOn, IsLocalMinOn.comp_continuousOn, zero_le_one, Set.left_mem_Icc
-- Module: Mathlib.Analysis.Convex.Extrema
Goal:
E : Type u_1
β : Type u_2
inst : AddCommGroup E
inst_1 : TopologicalSpace E
inst_2 : Module ℝ E
inst_3 : IsTopologicalAddGroup E
inst_4 : ContinuousSMul ℝ E
inst_5 : AddCommGroup β
inst_6 : PartialOrder β
inst_7 : IsOrderedAddMonoid β
inst_8 : Module ℝ β
inst_9 : IsOrderedModule ℝ β
inst_10 : 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 : (a : ℝ) → E) 0 = a
hg1 : (g : (a : ℝ) → E) 1 = x
hgc : Continuous[_, inst_1] (⇑g : (a : ℝ) → E)
h_maps : MapsTo (α := ℝ) (⇑g : (a : ℝ) → E) (Icc 0 1) s
⊢ IsLocalMinOn (α := ℝ) (f ∘ (⇑g : (a : ℝ) → E)) (Icc 0 1) 0

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)
-- Module: Mathlib.Analysis.Convex.Extrema
Goal:
E : Type u_1
β : Type u_2
inst : AddCommGroup E
inst_1 : TopologicalSpace E
inst_2 : Module ℝ E
inst_3 : IsTopologicalAddGroup E
inst_4 : ContinuousSMul ℝ E
inst_5 : AddCommGroup β
inst_6 : PartialOrder β
inst_7 : IsOrderedAddMonoid β
inst_8 : Module ℝ β
inst_9 : IsOrderedModule ℝ β
inst_10 : 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 : (a : ℝ) → E) 0 = a
hg1 : (g : (a : ℝ) → E) 1 = x
hgc : Continuous[_, inst_1] (⇑g : (a : ℝ) → E)
h_maps : MapsTo (α := ℝ) (⇑g : (a : ℝ) → E) (Icc 0 1) s
fg_local_min_on : IsLocalMinOn (α := ℝ) (f ∘ (⇑g : (a : ℝ) → E)) (Icc 0 1) 0
⊢ IsMinOn (α := ℝ) (f ∘ (⇑g : (a : ℝ) → E)) (Icc 0 1) 0

Tactic:
IsMinOn.of_isLocalMinOn_of_convexOn_Icc one_pos fg_local_min_on ?_

Premises used: IsMinOn.of_isLocalMinOn_of_convexOn_Icc, one_pos
-- Module: Mathlib.Analysis.Convex.Extrema
Goal:
E : Type u_1
β : Type u_2
inst : AddCommGroup E
inst_1 : TopologicalSpace E
inst_2 : Module ℝ E
inst_3 : IsTopologicalAddGroup E
inst_4 : ContinuousSMul ℝ E
inst_5 : AddCommGroup β
inst_6 : PartialOrder β
inst_7 : IsOrderedAddMonoid β
inst_8 : Module ℝ β
inst_9 : IsOrderedModule ℝ β
inst_10 : 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 : (a : ℝ) → E) 0 = a
hg1 : (g : (a : ℝ) → E) 1 = x
hgc : Continuous[_, inst_1] (⇑g : (a : ℝ) → E)
h_maps : MapsTo (α := ℝ) (⇑g : (a : ℝ) → E) (Icc 0 1) s
fg_local_min_on : IsLocalMinOn (α := ℝ) (f ∘ (⇑g : (a : ℝ) → E)) (Icc 0 1) 0
refine : ConvexOn ℝ (E := ℝ) (Icc 0 1) (f ∘ (⇑g : (a : ℝ) → E))
⊢ IsMinOn (α := ℝ) (f ∘ (⇑g : (a : ℝ) → E)) (Icc 0 1) 0

Tactic:
refine IsMinOn.of_isLocalMinOn_of_convexOn_Icc one_pos fg_local_min_on ?_

Premises used: IsMinOn.of_isLocalMinOn_of_convexOn_Icc, one_pos
-- Module: Mathlib.Analysis.Convex.Extrema
Goal:
E : Type u_1
β : Type u_2
inst : AddCommGroup E
inst_1 : TopologicalSpace E
inst_2 : Module ℝ E
inst_3 : IsTopologicalAddGroup E
inst_4 : ContinuousSMul ℝ E
inst_5 : AddCommGroup β
inst_6 : PartialOrder β
inst_7 : IsOrderedAddMonoid β
inst_8 : Module ℝ β
inst_9 : IsOrderedModule ℝ β
inst_10 : 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 : (a : ℝ) → E) 0 = a
hg1 : (g : (a : ℝ) → E) 1 = x
hgc : Continuous[_, inst_1] (⇑g : (a : ℝ) → E)
h_maps : MapsTo (α := ℝ) (⇑g : (a : ℝ) → E) (Icc 0 1) s
fg_local_min_on : IsLocalMinOn (α := ℝ) (f ∘ (⇑g : (a : ℝ) → E)) (Icc 0 1) 0
⊢ ConvexOn ℝ (E := ℝ) (Icc 0 1) (f ∘ (⇑g : (a : ℝ) → E))

Tactic:
(h_conv.comp_affineMap g).subset h_maps (convex_Icc 0 1)

Premises used: convex_Icc, ConvexOn.comp_affineMap, OfNat.ofNat, ConvexOn.subset
-- Module: Mathlib.Analysis.Convex.Extrema
Goal:
E : Type u_1
β : Type u_2
inst : AddCommGroup E
inst_1 : TopologicalSpace E
inst_2 : Module ℝ E
inst_3 : IsTopologicalAddGroup E
inst_4 : ContinuousSMul ℝ E
inst_5 : AddCommGroup β
inst_6 : PartialOrder β
inst_7 : IsOrderedAddMonoid β
inst_8 : Module ℝ β
inst_9 : IsOrderedModule ℝ β
inst_10 : 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 : (a : ℝ) → E) 0 = a
hg1 : (g : (a : ℝ) → E) 1 = x
hgc : Continuous[_, inst_1] (⇑g : (a : ℝ) → E)
h_maps : MapsTo (α := ℝ) (⇑g : (a : ℝ) → E) (Icc 0 1) s
fg_local_min_on : IsLocalMinOn (α := ℝ) (f ∘ (⇑g : (a : ℝ) → E)) (Icc 0 1) 0
⊢ ConvexOn ℝ (E := ℝ) (Icc 0 1) (f ∘ (⇑g : (a : ℝ) → E))

Tactic:
exact (h_conv.comp_affineMap g).subset h_maps (convex_Icc 0 1)

Premises used: convex_Icc, ConvexOn.comp_affineMap, OfNat.ofNat, ConvexOn.subset
-- Module: Mathlib.Analysis.Convex.Extrema
Goal:
E : Type u_1
β : Type u_2
inst : AddCommGroup E
inst_1 : TopologicalSpace E
inst_2 : Module ℝ E
inst_3 : IsTopologicalAddGroup E
inst_4 : ContinuousSMul ℝ E
inst_5 : AddCommGroup β
inst_6 : PartialOrder β
inst_7 : IsOrderedAddMonoid β
inst_8 : Module ℝ β
inst_9 : IsOrderedModule ℝ β
inst_10 : 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 : (a : ℝ) → E) 0 = a
hg1 : (g : (a : ℝ) → E) 1 = x
hgc : Continuous[_, inst_1] (⇑g : (a : ℝ) → E)
h_maps : MapsTo (α := ℝ) (⇑g : (a : ℝ) → E) (Icc 0 1) s
fg_local_min_on : IsLocalMinOn (α := ℝ) (f ∘ (⇑g : (a : ℝ) → E)) (Icc 0 1) 0
⊢ IsMinOn (α := ℝ) (f ∘ (⇑g : (a : ℝ) → E)) (Icc 0 1) 0

Tactic:
have fg_min_on : IsMinOn (f ∘ g) (Icc 0 1 : Set ℝ) 0 := by
    refine IsMinOn.of_isLocalMinOn_of_convexOn_Icc one_pos fg_local_min_on ?_
    exact (h_conv.comp_affineMap g).subset h_maps (convex_Icc 0 1)