-- Mathlib/Analysis/Convex/Extrema.lean
theorem IsMinOn.of_isLocalMinOn_of_convexOn_Icc {f : ℝ → β} {a b : ℝ} (a_lt_b : a < b)
    (h_local_min : IsLocalMinOn f (Icc a b) a) (h_conv : ConvexOn ℝ (Icc a b) f) :
    IsMinOn f (Icc a b) a

Proof state:
β : Type u_2
inst✝² : OrderedAddCommGroup β
inst✝¹ : Module ℝ β
inst✝ : OrderedSMul ℝ β
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
⊢ f a ≤ f c

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

Result:
case inl
β : Type u_2
inst✝² : OrderedAddCommGroup β
inst✝¹ : Module ℝ β
inst✝ : OrderedSMul ℝ β
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

case inr
β : Type u_2
inst✝² : OrderedAddCommGroup β
inst✝¹ : Module ℝ β
inst✝ : OrderedSMul ℝ β
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
⊢ f a ≤ f c

Proof state:
case inr.intro.intro
β : Type u_2
inst✝² : OrderedAddCommGroup β
inst✝¹ : Module ℝ β
inst✝ : OrderedSMul ℝ β
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
⊢ f a ≤ f c

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

Result:
case inr.intro.intro.intro.intro.intro.intro.intro
β : Type u_2
inst✝² : OrderedAddCommGroup β
inst✝¹ : Module ℝ β
inst✝ : OrderedSMul ℝ β
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 c

Proof state:
case inr.intro.intro.intro.intro.intro.intro.intro
β : Type u_2
inst✝² : OrderedAddCommGroup β
inst✝¹ : Module ℝ β
inst✝ : OrderedSMul ℝ β
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 • 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

Result:
no goals

Proof state:
case inr.intro.intro.intro.intro.intro.intro.intro
β : Type u_2
inst✝² : OrderedAddCommGroup β
inst✝¹ : Module ℝ β
inst✝ : OrderedSMul ℝ β
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 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)

Result:
case inr.intro.intro.intro.intro.intro.intro.intro
β : Type u_2
inst✝² : OrderedAddCommGroup β
inst✝¹ : Module ℝ β
inst✝ : OrderedSMul ℝ β
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 • f a + yc • f a ≤ ya • f a + yc • f c

Proof state:
case inr
β : Type u_2
inst✝² : OrderedAddCommGroup β
inst✝¹ : Module ℝ β
inst✝ : OrderedSMul ℝ β
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
⊢ f a ≤ f c

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

Result:
case inr.intro.intro
β : Type u_2
inst✝² : OrderedAddCommGroup β
inst✝¹ : Module ℝ β
inst✝ : OrderedSMul ℝ β
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
⊢ f a ≤ f c

Proof state:
β : Type u_2
inst✝² : OrderedAddCommGroup β
inst✝¹ : Module ℝ β
inst✝ : OrderedSMul ℝ β
f : ℝ → β
a b : ℝ
a_lt_b : a < b
h_local_min : IsLocalMinOn f (Icc a b) a
h_conv : ConvexOn ℝ (Icc a b) f
⊢ IsMinOn f (Icc a b) a

Tactic:
rintro c hc

Result:
β : Type u_2
inst✝² : OrderedAddCommGroup β
inst✝¹ : Module ℝ β
inst✝ : OrderedSMul ℝ β
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
⊢ c ∈ {x | (fun x => f a ≤ f x) x}

Proof state:
case inl
β : Type u_2
inst✝² : OrderedAddCommGroup β
inst✝¹ : Module ℝ β
inst✝ : OrderedSMul ℝ β
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

Result:
no goals

Proof state:
case inr
β : Type u_2
inst✝² : OrderedAddCommGroup β
inst✝¹ : Module ℝ β
inst✝ : OrderedSMul ℝ β
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
⊢ f a ≤ f c

Tactic:
have H₁ : ∀ᶠ y in 𝓝[>] a, f a ≤ f y :=
  h_local_min.filter_mono (nhdsWithin_mono _ Ioi_subset_Ici_self)

Result:
case inr
β : Type u_2
inst✝² : OrderedAddCommGroup β
inst✝¹ : Module ℝ β
inst✝ : OrderedSMul ℝ β
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
⊢ f a ≤ f c

Proof state:
case inr
β : Type u_2
inst✝² : OrderedAddCommGroup β
inst✝¹ : Module ℝ β
inst✝ : OrderedSMul ℝ β
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
⊢ f a ≤ f c

Tactic:
have H₂ : ∀ᶠ y in 𝓝[>] a, y ∈ Ioc a c := Ioc_mem_nhdsGT a_lt_c

Result:
case inr
β : Type u_2
inst✝² : OrderedAddCommGroup β
inst✝¹ : Module ℝ β
inst✝ : OrderedSMul ℝ β
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
⊢ f a ≤ f c

Proof state:
β : Type u_2
inst✝² : OrderedAddCommGroup β
inst✝¹ : Module ℝ β
inst✝ : OrderedSMul ℝ β
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
⊢ f a ≤ f c

Tactic:
rw [IsLocalMinOn, nhdsWithin_Icc_eq_nhdsGE a_lt_b] at h_local_min

Result:
β : Type u_2
inst✝² : OrderedAddCommGroup β
inst✝¹ : Module ℝ β
inst✝ : OrderedSMul ℝ β
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
⊢ f a ≤ f c

Proof state:
β : Type u_2
inst✝² : OrderedAddCommGroup β
inst✝¹ : Module ℝ β
inst✝ : OrderedSMul ℝ β
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 • f a + yc • f a = f a

Tactic:
rw [← add_smul, yac, one_smul]

Result:
no goals