case intro.intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
F : Type ?u.344708
α : Type ?u.344711
β : Type u_3
ι : Type ?u.344717
inst✝⁶ : OrderedSemiring 𝕜
inst✝⁵ : AddCommMonoid E
inst✝⁴ : AddCommMonoid F
inst✝³ : OrderedCancelAddCommMonoid β
inst✝² : Module 𝕜 E
inst✝¹ : Module 𝕜 β
inst✝ : OrderedSMul 𝕜 β
s : Set E
f : E → β
hf : ConvexOn 𝕜 s f
p q : E × β
hp : p.fst ∈ s ∧ f p.fst < p.snd
hq : q.fst ∈ s ∧ f q.fst ≤ q.snd
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ a • p + b • q ∈ {p | p.fst ∈ s ∧ f p.fst < p.snd}
𝕜 : Type u_1
E : Type u_2
F : Type ?u.344708
α : Type ?u.344711
β : Type u_3
ι : Type ?u.344717
inst✝⁶ : OrderedSemiring 𝕜
inst✝⁵ : AddCommMonoid E
inst✝⁴ : AddCommMonoid F
inst✝³ : OrderedCancelAddCommMonoid β
inst✝² : Module 𝕜 E
inst✝¹ : Module 𝕜 β
inst✝ : OrderedSMul 𝕜 β
s : Set E
f : E → β
hf : ConvexOn 𝕜 s f
p q : E × β
hp : p.fst ∈ s ∧ f p.fst < p.snd
hq : q.fst ∈ s ∧ f q.fst ≤ q.snd
⊢ openSegment 𝕜 p q ⊆ {p | p.fst ∈ s ∧ f p.fst < p.snd}
rintro _ ⟨a, b, ha, hb, hab, rfl⟩
case intro.intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
F : Type ?u.344708
α : Type ?u.344711
β : Type u_3
ι : Type ?u.344717
inst✝⁶ : OrderedSemiring 𝕜
inst✝⁵ : AddCommMonoid E
inst✝⁴ : AddCommMonoid F
inst✝³ : OrderedCancelAddCommMonoid β
inst✝² : Module 𝕜 E
inst✝¹ : Module 𝕜 β
inst✝ : OrderedSMul 𝕜 β
s : Set E
f : E → β
hf : ConvexOn 𝕜 s f
p q : E × β
hp : p.fst ∈ s ∧ f p.fst < p.snd
hq : q.fst ∈ s ∧ f q.fst ≤ q.snd
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ f (a • p + b • q).fst < (a • p + b • q).snd
case intro.intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
F : Type ?u.344708
α : Type ?u.344711
β : Type u_3
ι : Type ?u.344717
inst✝⁶ : OrderedSemiring 𝕜
inst✝⁵ : AddCommMonoid E
inst✝⁴ : AddCommMonoid F
inst✝³ : OrderedCancelAddCommMonoid β
inst✝² : Module 𝕜 E
inst✝¹ : Module 𝕜 β
inst✝ : OrderedSMul 𝕜 β
s : Set E
f : E → β
hf : ConvexOn 𝕜 s f
p q : E × β
hp : p.fst ∈ s ∧ f p.fst < p.snd
hq : q.fst ∈ s ∧ f q.fst ≤ q.snd
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ a • p + b • q ∈ {p | p.fst ∈ s ∧ f p.fst < p.snd}
refine' ⟨hf.1 hp.1 hq.1 ha.le hb.le hab, _⟩
no goals
case intro.intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
F : Type ?u.344708
α : Type ?u.344711
β : Type u_3
ι : Type ?u.344717
inst✝⁶ : OrderedSemiring 𝕜
inst✝⁵ : AddCommMonoid E
inst✝⁴ : AddCommMonoid F
inst✝³ : OrderedCancelAddCommMonoid β
inst✝² : Module 𝕜 E
inst✝¹ : Module 𝕜 β
inst✝ : OrderedSMul 𝕜 β
s : Set E
f : E → β
hf : ConvexOn 𝕜 s f
p q : E × β
hp : p.fst ∈ s ∧ f p.fst < p.snd
hq : q.fst ∈ s ∧ f q.fst ≤ q.snd
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ f (a • p + b • q).fst < (a • p + b • q).snd
calc
  f (a • p.1 + b • q.1) ≤ a • f p.1 + b • f q.1 := hf.2 hp.1 hq.1 ha.le hb.le hab
  _ < a • p.2 + b • q.2 :=
    add_lt_add_of_lt_of_le (smul_lt_smul_of_pos hp.2 ha) (smul_le_smul_of_nonneg hq.2 hb.le)