awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Convex.Intrinsic
Goal:
𝕜 : Type u_1
V : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : AddCommGroup V
inst_3 : Module 𝕜 V
inst_4 : TopologicalSpace V
inst_5 : IsTopologicalAddGroup V
inst_6 : ContinuousConstSMul 𝕜 V
s : Set V
hs : Convex 𝕜 s
⊢ Convex 𝕜 (closure[inst_4] s ∩ (↑(affineSpan 𝕜 s) : Set V))

Tactic:
hs.closure.inter (affineSpan 𝕜 s).convex

Premises used: AffineSubspace.convex, Convex.closure, Convex.inter, affineSpan
-- Module: Mathlib.Analysis.Convex.Intrinsic
Goal:
𝕜 : Type u_1
V : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : AddCommGroup V
inst_3 : Module 𝕜 V
inst_4 : TopologicalSpace V
inst_5 : IsTopologicalAddGroup V
inst_6 : ContinuousConstSMul 𝕜 V
s : Set V
hs : Convex 𝕜 s
⊢ Convex 𝕜 (closure[inst_4] s ∩ (↑(affineSpan 𝕜 s) : Set V))

Tactic:
exact hs.closure.inter (affineSpan 𝕜 s).convex

Premises used: AffineSubspace.convex, Convex.closure, Convex.inter, affineSpan
-- Module: Mathlib.Analysis.Convex.Intrinsic
Goal:
α : Type u_6
β : Type u_7
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
φ : α ≃ₜ β
s : Set β
rw : (interior s).Nonempty ↔ Set.Nonempty.{u_6} (α := α) (interior ((⇑φ.symm : (a : β) → α) '' s))
rw₁ : (interior s).Nonempty ↔ Set.Nonempty.{u_6} (α := α) ((⇑φ.symm : (a : β) → α) '' interior s)
rw₂ rw₃ : (interior s).Nonempty ↔ (interior s).Nonempty
⊢ (interior s).Nonempty ↔ Set.Nonempty.{u_6} (α := α) (interior ((⇑φ : (a : α) → β) ⁻¹' s))

Tactic:
rw [← φ.image_symm, ← φ.symm.image_interior, image_nonempty]

Premises used: Set.image_nonempty, Homeomorph.image_interior, Homeomorph.image_symm, Homeomorph.symm
-- Module: Mathlib.Analysis.Convex.Intrinsic
Goal:
V : Type u_2
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : FiniteDimensional ℝ V
s : Set V
hscv : Convex ℝ s
hsne : s.Nonempty
⊢ Nonempty.{u_2 + 1} (↑s : Type u_2)

Tactic:
haveI := hsne.coe_sort
-- Module: Mathlib.Analysis.Convex.Intrinsic
Goal:
V : Type u_2
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : FiniteDimensional ℝ V
s : Set V
hscv : Convex ℝ s
hsne : s.Nonempty
this : Nonempty.{u_2 + 1} (↑s : Type u_2)
obtain : ∀ (p : V) (hp : p ∈ s), (intrinsicInterior ℝ s).Nonempty
⊢ (intrinsicInterior ℝ s).Nonempty

Tactic:
obtain ⟨p, hp⟩ := hsne
-- Module: Mathlib.Analysis.Convex.Intrinsic
Goal:
V : Type u_2
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : FiniteDimensional ℝ V
s : Set V
hscv : Convex ℝ s
this : Nonempty.{u_2 + 1} (↑s : Type u_2)
p : V
hp : p ∈ s
p' : ↥(_root_.affineSpan ℝ s) :=
  Subtype.mk (p := fun (x : V) ↦ Membership.mem (γ := AffineSubspace ℝ V) (_root_.affineSpan ℝ s) x) p ⋯
rw :
  Convex ℝ (E := ↥(direction (_root_.affineSpan ℝ s)))
    (Set.preimage (β := ↥(_root_.affineSpan ℝ s))
      (⇑(AffineIsometryEquiv.toHomeomorph (AffineIsometryEquiv.symm (AffineIsometryEquiv.constVSub ℝ p'))) :
        (a : ↥(_root_.affineSpan ℝ s).direction) → ↥(_root_.affineSpan ℝ s))
      (Subtype.val (p := fun (x : V) ↦ Membership.mem (γ := AffineSubspace ℝ V) (_root_.affineSpan ℝ s) x) ⁻¹' s))
⊢ (intrinsicInterior ℝ s).Nonempty

Tactic:
rw [intrinsicInterior, image_nonempty,
    aux (AffineIsometryEquiv.constVSub ℝ p').symm.toHomeomorph,
    Convex.interior_nonempty_iff_affineSpan_eq_top, AffineIsometryEquiv.coe_toHomeomorph, ←
    AffineIsometryEquiv.coe_toAffineEquiv, ← comap_span, affineSpan_coe_preimage_eq_top, comap_top]

Premises used: Set.image_nonempty, Real, intrinsicInterior, Convex.interior_nonempty_iff_affineSpan_eq_top, AffineIsometryEquiv.symm, AffineIsometryEquiv.constVSub, AffineSubspace.comap_span, affineSpan_coe_preimage_eq_top, AffineSubspace.comap_top, _private.0.aux, AffineIsometryEquiv.coe_toHomeomorph, AffineIsometryEquiv.toHomeomorph, AffineIsometryEquiv.coe_toAffineEquiv
-- Module: Mathlib.Analysis.Convex.Intrinsic
Goal:
V : Type u_2
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : FiniteDimensional ℝ V
s : Set V
hscv : Convex ℝ s
this : Nonempty.{u_2 + 1} (↑s : Type u_2)
p : V
hp : p ∈ s
p' : ↥(_root_.affineSpan ℝ s) :=
  Subtype.mk (p := fun (x : V) ↦ Membership.mem (γ := AffineSubspace ℝ V) (_root_.affineSpan ℝ s) x) p ⋯
⊢ Convex ℝ (E := ↥(direction (_root_.affineSpan ℝ s)))
    (Set.preimage (β := ↥(_root_.affineSpan ℝ s))
      (⇑(AffineIsometryEquiv.toHomeomorph (AffineIsometryEquiv.symm (AffineIsometryEquiv.constVSub ℝ p'))) :
        (a : ↥(_root_.affineSpan ℝ s).direction) → ↥(_root_.affineSpan ℝ s))
      (Subtype.val (p := fun (x : V) ↦ Membership.mem (γ := AffineSubspace ℝ V) (_root_.affineSpan ℝ s) x) ⁻¹' s))

Tactic:
hscv.affine_preimage
    ((_root_.affineSpan ℝ s).subtype.comp
      (AffineIsometryEquiv.constVSub ℝ p').symm.toAffineEquiv.toAffineMap)

Premises used: Real, Set.Mem, AffineIsometryEquiv.toAffineEquiv, setOf, AffineIsometryEquiv.symm, AffineIsometryEquiv.constVSub, affineSpan, Set.preimage, AffineSubspace.subtype, AffineEquiv.toAffineMap, AffineMap.comp, Convex.affine_preimage
-- Module: Mathlib.Analysis.Convex.Intrinsic
Goal:
V : Type u_2
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : FiniteDimensional ℝ V
s : Set V
hscv : Convex ℝ s
this : Nonempty.{u_2 + 1} (↑s : Type u_2)
p : V
hp : p ∈ s
p' : ↥(_root_.affineSpan ℝ s) :=
  Subtype.mk (p := fun (x : V) ↦ Membership.mem (γ := AffineSubspace ℝ V) (_root_.affineSpan ℝ s) x) p ⋯
⊢ Convex ℝ (E := ↥(direction (_root_.affineSpan ℝ s)))
    (Set.preimage (β := ↥(_root_.affineSpan ℝ s))
      (⇑(AffineIsometryEquiv.toHomeomorph (AffineIsometryEquiv.symm (AffineIsometryEquiv.constVSub ℝ p'))) :
        (a : ↥(_root_.affineSpan ℝ s).direction) → ↥(_root_.affineSpan ℝ s))
      (Subtype.val (p := fun (x : V) ↦ Membership.mem (γ := AffineSubspace ℝ V) (_root_.affineSpan ℝ s) x) ⁻¹' s))

Tactic:
exact hscv.affine_preimage
    ((_root_.affineSpan ℝ s).subtype.comp
      (AffineIsometryEquiv.constVSub ℝ p').symm.toAffineEquiv.toAffineMap)

Premises used: Real, AffineIsometryEquiv.toAffineEquiv, AffineIsometryEquiv.symm, AffineIsometryEquiv.constVSub, affineSpan, AffineSubspace.subtype, AffineEquiv.toAffineMap, AffineMap.comp, Convex.affine_preimage
-- Module: Mathlib.Analysis.Convex.Intrinsic
Goal:
V : Type u_2
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : FiniteDimensional ℝ V
s : Set V
hs : Convex ℝ s
simp_rw : intrinsicInterior ℝ s ≠ ∅ → s ≠ ∅
⊢ (intrinsicInterior ℝ s).Nonempty → s.Nonempty

Tactic:
simp_rw [nonempty_iff_ne_empty]

Premises used: Set.nonempty_iff_ne_empty
-- Module: Mathlib.Analysis.Convex.Intrinsic
Goal:
V : Type u_2
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : FiniteDimensional ℝ V
hs : Convex.{0, u_2} ℝ (E := V) ∅
h : Ne (α := Set V) (intrinsicInterior ℝ ∅) ∅
⊢ False

Tactic:
h intrinsicInterior_empty

Premises used: intrinsicInterior_empty
-- Module: Mathlib.Analysis.Convex.Intrinsic
Goal:
V : Type u_2
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : FiniteDimensional ℝ V
hs : Convex.{0, u_2} ℝ (E := V) ∅
h : Ne (α := Set V) (intrinsicInterior ℝ ∅) ∅
⊢ False

Tactic:
exact h intrinsicInterior_empty

Premises used: intrinsicInterior_empty
-- Module: Mathlib.Analysis.Convex.Jensen
Goal:
𝕜 : Type u_1
E : Type u_2
β : Type u_4
ι : Type u_5
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : AddCommGroup β
inst_5 : PartialOrder β
inst_6 : IsOrderedAddMonoid β
inst_7 : Module 𝕜 E
inst_8 : Module 𝕜 β
inst_9 : IsStrictOrderedModule 𝕜 β
s : Set E
f : E → β
t : Finset ι
w : ι → 𝕜
p : ι → E
hf : ConvexOn 𝕜 s f
h₀ : ∀ i ∈ t, 0 ≤ w i
h₁ : LT.lt.{u_1} (α := 𝕜) 0 (∑ i ∈ t, w i)
hmem : ∀ i ∈ t, p i ∈ s
⊢ ∀ i ∈ t, Membership.mem (γ := Set (E × β)) {p : E × β | p.1 ∈ s ∧ f p.1 ≤ p.2} (p i, (f ∘ p) i)

Tactic:
have hmem' : ∀ i ∈ t, (p i, (f ∘ p) i) ∈ { p : E × β | p.1 ∈ s ∧ f p.1 ≤ p.2 } := fun i hi =>
    ⟨hmem i hi, le_rfl⟩
-- Module: Mathlib.Analysis.Convex.Jensen
Goal:
𝕜 : Type u_1
E : Type u_2
β : Type u_4
ι : Type u_5
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : AddCommGroup β
inst_5 : PartialOrder β
inst_6 : IsOrderedAddMonoid β
inst_7 : Module 𝕜 E
inst_8 : Module 𝕜 β
inst_9 : IsStrictOrderedModule 𝕜 β
s : Set E
f : E → β
t : Finset ι
w : ι → 𝕜
p : ι → E
hf : ConvexOn 𝕜 s f
h₀ : ∀ i ∈ t, 0 ≤ w i
h₁ : LT.lt.{u_1} (α := 𝕜) 0 (∑ i ∈ t, w i)
hmem : ∀ i ∈ t, p i ∈ s
hmem' : ∀ i ∈ t, Membership.mem (γ := Set (E × β)) {p : E × β | p.1 ∈ s ∧ f p.1 ≤ p.2} (p i, (f ∘ p) i)
⊢ f (t.centerMass w fun (i : ι) ↦ (p i, (f ∘ p) i)).1 ≤ (t.centerMass w fun (i : ι) ↦ (p i, (f ∘ p) i)).2

Tactic:
(hf.convex_epigraph.centerMass_mem h₀ h₁ hmem').2

Premises used: Convex.centerMass_mem, ConvexOn.convex_epigraph, And.right
-- Module: Mathlib.Analysis.Convex.Jensen
Goal:
𝕜 : Type u_1
E : Type u_2
β : Type u_4
ι : Type u_5
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : AddCommGroup β
inst_5 : PartialOrder β
inst_6 : IsOrderedAddMonoid β
inst_7 : Module 𝕜 E
inst_8 : Module 𝕜 β
inst_9 : IsStrictOrderedModule 𝕜 β
s : Set E
f : E → β
t : Finset ι
w : ι → 𝕜
p : ι → E
hf : ConvexOn 𝕜 s f
h₀ : ∀ i ∈ t, 0 ≤ w i
h₁ : LT.lt.{u_1} (α := 𝕜) 0 (∑ i ∈ t, w i)
hmem : ∀ i ∈ t, p i ∈ s
hmem' : ∀ i ∈ t, Membership.mem (γ := Set (E × β)) {p : E × β | p.1 ∈ s ∧ f p.1 ≤ p.2} (p i, (f ∘ p) i)
h : t.centerMass w p = (t.centerMass w fun (i : ι) ↦ (p i, (f ∘ p) i)).1
h₂ : t.centerMass w (f ∘ p) = (t.centerMass w fun (i : ι) ↦ (p i, (f ∘ p) i)).2
⊢ f (t.centerMass w p) ≤ t.centerMass w (f ∘ p)

Tactic:
convert! (hf.convex_epigraph.centerMass_mem h₀ h₁ hmem').2

Premises used: Convex.centerMass_mem, ConvexOn.convex_epigraph, And.right
-- Module: Mathlib.Analysis.Convex.Jensen
Goal:
𝕜 : Type u_1
E : Type u_2
β : Type u_4
ι : Type u_5
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : AddCommGroup β
inst_5 : PartialOrder β
inst_6 : IsOrderedAddMonoid β
inst_7 : Module 𝕜 E
inst_8 : Module 𝕜 β
inst_9 : IsStrictOrderedModule 𝕜 β
s : Set E
f : E → β
t : Finset ι
w : ι → 𝕜
p : ι → E
hf : ConvexOn 𝕜 s f
h₀ : ∀ i ∈ t, 0 ≤ w i
h₁ : LT.lt.{u_1} (α := 𝕜) 0 (∑ i ∈ t, w i)
hmem : ∀ i ∈ t, p i ∈ s
hmem' : ∀ i ∈ t, Membership.mem (γ := Set (E × β)) {p : E × β | p.1 ∈ s ∧ f p.1 ≤ p.2} (p i, (f ∘ p) i)
⊢ t.centerMass w p = (t.centerMass w fun (i : ι) ↦ (p i, (f ∘ p) i)).1

Tactic:
simp only [centerMass, Function.comp, Prod.smul_fst, Prod.fst_sum, Prod.smul_snd, Prod.snd_sum]

Premises used: Function.comp, Prod.snd_sum, Prod.smul_snd, Finset.centerMass, Prod.fst_sum, Prod.smul_fst
-- Module: Mathlib.Analysis.Convex.Jensen
Goal:
𝕜 : Type u_1
E : Type u_2
β : Type u_4
ι : Type u_5
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : AddCommGroup β
inst_5 : PartialOrder β
inst_6 : IsOrderedAddMonoid β
inst_7 : Module 𝕜 E
inst_8 : Module 𝕜 β
inst_9 : IsStrictOrderedModule 𝕜 β
s : Set E
f : E → β
t : Finset ι
w : ι → 𝕜
p : ι → E
hf : ConvexOn 𝕜 s f
h₀ : ∀ i ∈ t, 0 ≤ w i
h₁ : LT.lt.{u_1} (α := 𝕜) 0 (∑ i ∈ t, w i)
hmem : ∀ i ∈ t, p i ∈ s
hmem' : ∀ i ∈ t, Membership.mem (γ := Set (E × β)) {p : E × β | p.1 ∈ s ∧ f p.1 ≤ p.2} (p i, (f ∘ p) i)
⊢ t.centerMass w (f ∘ p) = (t.centerMass w fun (i : ι) ↦ (p i, (f ∘ p) i)).2

Tactic:
simp only [centerMass, Function.comp, Prod.smul_fst, Prod.fst_sum, Prod.smul_snd, Prod.snd_sum]

Premises used: Function.comp, Prod.snd_sum, Prod.smul_snd, Finset.centerMass, Prod.fst_sum, Prod.smul_fst
-- Module: Mathlib.Analysis.Convex.Jensen
Goal:
𝕜 : Type u_1
E : Type u_2
β : Type u_4
ι : Type u_5
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : AddCommGroup β
inst_5 : PartialOrder β
inst_6 : IsOrderedAddMonoid β
inst_7 : Module 𝕜 E
inst_8 : Module 𝕜 β
inst_9 : IsStrictOrderedModule 𝕜 β
s : Set E
f : E → β
t : Finset ι
w : ι → 𝕜
p : ι → E
hf : ConcaveOn 𝕜 s f
h₀ : ∀ i ∈ t, 0 ≤ w i
h₁ : LT.lt.{u_1} (α := 𝕜) 0 (∑ i ∈ t, w i)
hmem : ∀ i ∈ t, p i ∈ s
⊢ t.centerMass w (f ∘ p) ≤ f (t.centerMass w p)

Tactic:
ConvexOn.map_centerMass_le (β := βᵒᵈ) hf h₀ h₁ hmem

Premises used: ConvexOn.map_centerMass_le, OrderDual
-- Module: Mathlib.Analysis.Convex.Jensen
Goal:
𝕜 : Type u_1
E : Type u_2
β : Type u_4
ι : Type u_5
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : AddCommGroup β
inst_5 : PartialOrder β
inst_6 : IsOrderedAddMonoid β
inst_7 : Module 𝕜 E
inst_8 : Module 𝕜 β
inst_9 : IsStrictOrderedModule 𝕜 β
s : Set E
f : E → β
t : Finset ι
w : ι → 𝕜
p : ι → E
hf : ConvexOn 𝕜 s f
h₀ : ∀ i ∈ t, 0 ≤ w i
h₁ : Eq.{u_1 + 1} (α := 𝕜) (∑ i ∈ t, w i) 1
hmem : ∀ i ∈ t, p i ∈ s
⊢ f (∑ i ∈ t, w i • p i) ≤ ∑ i ∈ t, w i • f (p i)

Tactic:
simpa only [centerMass, h₁, inv_one, one_smul] using
    hf.map_centerMass_le h₀ (h₁.symm ▸ zero_lt_one) hmem

Premises used: inv_one, Eq.rec, ConvexOn.map_centerMass_le, one_smul, zero_lt_one, Finset.centerMass, Eq.symm
-- Module: Mathlib.Analysis.Convex.Jensen
Goal:
𝕜 : Type u_1
E : Type u_2
β : Type u_4
ι : Type u_5
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : AddCommGroup β
inst_5 : PartialOrder β
inst_6 : IsOrderedAddMonoid β
inst_7 : Module 𝕜 E
inst_8 : Module 𝕜 β
inst_9 : IsStrictOrderedModule 𝕜 β
s : Set E
f : E → β
t : Finset ι
w : ι → 𝕜
p : ι → E
hf : ConcaveOn 𝕜 s f
h₀ : ∀ i ∈ t, 0 ≤ w i
h₁ : Eq.{u_1 + 1} (α := 𝕜) (∑ i ∈ t, w i) 1
hmem : ∀ i ∈ t, p i ∈ s
⊢ ∑ i ∈ t, w i • f (p i) ≤ f (∑ i ∈ t, w i • p i)

Tactic:
ConvexOn.map_sum_le (β := βᵒᵈ) hf h₀ h₁ hmem

Premises used: ConvexOn.map_sum_le, OrderDual
-- Module: Mathlib.Analysis.Convex.Jensen
Goal:
𝕜 : Type u_1
E : Type u_2
β : Type u_4
ι : Type u_5
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : AddCommGroup β
inst_5 : PartialOrder β
inst_6 : IsOrderedAddMonoid β
inst_7 : Module 𝕜 E
inst_8 : Module 𝕜 β
inst_9 : IsStrictOrderedModule 𝕜 β
s : Set E
f : E → β
t : Finset ι
w : ι → 𝕜
p : ι → E
v : 𝕜
q : E
hf : ConvexOn 𝕜 s f
h₀ : ∀ i ∈ t, 0 ≤ w i
h₁ : v + ∑ i ∈ t, w i = 1
hmem : ∀ i ∈ t, p i ∈ s
hv : 0 ≤ v
hq : q ∈ s
W : (j : Option ι) → 𝕜 := fun (j : Option ι) ↦ j.elim v w
P : (j : Option ι) → E := fun (j : Option ι) ↦ j.elim q p
⊢ Eq.{u_1 + 1} (α := 𝕜) (∑ i ∈ (insertNone : (a : Finset ι) → Finset (Option ι)) t, W i) 1

Tactic:
simpa using h₁
-- Module: Mathlib.Analysis.Convex.Jensen
Goal:
𝕜 : Type u_1
E : Type u_2
β : Type u_4
ι : Type u_5
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : AddCommGroup β
inst_5 : PartialOrder β
inst_6 : IsOrderedAddMonoid β
inst_7 : Module 𝕜 E
inst_8 : Module 𝕜 β
inst_9 : IsStrictOrderedModule 𝕜 β
s : Set E
f : E → β
t : Finset ι
w : ι → 𝕜
p : ι → E
v : 𝕜
q : E
hf : ConvexOn 𝕜 s f
h₀ : ∀ i ∈ t, 0 ≤ w i
h₁ : v + ∑ i ∈ t, w i = 1
hmem : ∀ i ∈ t, p i ∈ s
hv : 0 ≤ v
hq : q ∈ s
W : (j : Option ι) → 𝕜 := fun (j : Option ι) ↦ j.elim v w
P : (j : Option ι) → E := fun (j : Option ι) ↦ j.elim q p
⊢ f (∑ j ∈ (insertNone : (a : Finset ι) → Finset (Option ι)) t, W j • P j) ≤
    ∑ j ∈ (insertNone : (a : Finset ι) → Finset (Option ι)) t, W j • f (P j)

Tactic:
have : f (∑ j ∈ insertNone t, W j • P j) ≤ ∑ j ∈ insertNone t, W j • f (P j) :=
    hf.map_sum_le (forall_mem_insertNone.2 ⟨hv, h₀⟩) (by simpa using h₁)
      (forall_mem_insertNone.2 ⟨hq, hmem⟩)
-- Module: Mathlib.Analysis.Convex.Jensen
Goal:
𝕜 : Type u_1
E : Type u_2
β : Type u_4
ι : Type u_5
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : AddCommGroup β
inst_5 : PartialOrder β
inst_6 : IsOrderedAddMonoid β
inst_7 : Module 𝕜 E
inst_8 : Module 𝕜 β
inst_9 : IsStrictOrderedModule 𝕜 β
s : Set E
f : E → β
t : Finset ι
w : ι → 𝕜
p : ι → E
v : 𝕜
q : E
hf : ConvexOn 𝕜 s f
h₀ : ∀ i ∈ t, 0 ≤ w i
h₁ : v + ∑ i ∈ t, w i = 1
hmem : ∀ i ∈ t, p i ∈ s
hv : 0 ≤ v
hq : q ∈ s
W : (j : Option ι) → 𝕜 := fun (j : Option ι) ↦ j.elim v w
P : (j : Option ι) → E := fun (j : Option ι) ↦ j.elim q p
this :
  f (∑ j ∈ (insertNone : (a : Finset ι) → Finset (Option ι)) t, W j • P j) ≤
    ∑ j ∈ (insertNone : (a : Finset ι) → Finset (Option ι)) t, W j • f (P j)
⊢ f (v • q + ∑ i ∈ t, w i • p i) ≤ v • f q + ∑ i ∈ t, w i • f (p i)

Tactic:
simpa using this
-- Module: Mathlib.Analysis.Convex.Jensen
Goal:
𝕜 : Type u_1
E : Type u_2
β : Type u_4
ι : Type u_5
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : AddCommGroup β
inst_5 : PartialOrder β
inst_6 : IsOrderedAddMonoid β
inst_7 : Module 𝕜 E
inst_8 : Module 𝕜 β
inst_9 : IsStrictOrderedModule 𝕜 β
s : Set E
f : E → β
t : Finset ι
w : ι → 𝕜
p : ι → E
v : 𝕜
q : E
hf : ConcaveOn 𝕜 s f
h₀ : ∀ i ∈ t, 0 ≤ w i
h₁ : v + ∑ i ∈ t, w i = 1
hmem : ∀ i ∈ t, p i ∈ s
hv : 0 ≤ v
hq : q ∈ s
⊢ v • f q + ∑ i ∈ t, w i • f (p i) ≤ f (v • q + ∑ i ∈ t, w i • p i)

Tactic:
hf.dual.map_add_sum_le h₀ h₁ hmem hv hq

Premises used: OrderDual, ConcaveOn.dual, ConvexOn.map_add_sum_le
-- Module: Mathlib.Analysis.Convex.Jensen
Goal:
𝕜 : Type u_1
E : Type u_2
β : Type u_4
ι : Type u_5
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : AddCommGroup β
inst_5 : PartialOrder β
inst_6 : IsOrderedAddMonoid β
inst_7 : Module 𝕜 E
inst_8 : Module 𝕜 β
inst_9 : IsStrictOrderedModule 𝕜 β
s : Set E
f : E → β
t : Finset ι
w : ι → 𝕜
p : ι → E
hf : StrictConvexOn 𝕜 s f
h₀ : ∀ i ∈ t, 0 < w i
h₁ : Eq.{u_1 + 1} (α := 𝕜) (∑ i ∈ t, w i) 1
hmem : ∀ i ∈ t, p i ∈ s
hp : ∃ j ∈ t, ∃ k ∈ t, p j ≠ p k
obtain : ∀ (j : ι) (hj : j ∈ t) (k : ι) (hk : k ∈ t) (hjk : p j ≠ p k), f (∑ i ∈ t, w i • p i) < ∑ i ∈ t, w i • f (p i)
⊢ f (∑ i ∈ t, w i • p i) < ∑ i ∈ t, w i • f (p i)

Tactic:
obtain ⟨j, hj, k, hk, hjk⟩ := hp
-- Module: Mathlib.Analysis.Convex.Jensen
Goal:
𝕜 : Type u_1
E : Type u_2
β : Type u_4
ι : Type u_5
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : AddCommGroup β
inst_5 : PartialOrder β
inst_6 : IsOrderedAddMonoid β
inst_7 : Module 𝕜 E
inst_8 : Module 𝕜 β
inst_9 : IsStrictOrderedModule 𝕜 β
s : Set E
f : E → β
t : Finset ι
w : ι → 𝕜
p : ι → E
hf : StrictConvexOn 𝕜 s f
h₀ : ∀ i ∈ t, 0 < w i
h₁ : Eq.{u_1 + 1} (α := 𝕜) (∑ i ∈ t, w i) 1
hmem : ∀ i ∈ t, p i ∈ s
j : ι
hj : j ∈ t
k : ι
hk : k ∈ t
hjk : p j ≠ p k
⊢ k ∈ t.erase j

Tactic:
have : k ∈ t.erase j := mem_erase.2 ⟨ne_of_apply_ne _ hjk.symm, hk⟩
-- Module: Mathlib.Analysis.Convex.Jensen
Goal:
𝕜 : Type u_1
E : Type u_2
β : Type u_4
ι : Type u_5
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : AddCommGroup β
inst_5 : PartialOrder β
inst_6 : IsOrderedAddMonoid β
inst_7 : Module 𝕜 E
inst_8 : Module 𝕜 β
inst_9 : IsStrictOrderedModule 𝕜 β
s : Set E
f : E → β
t : Finset ι
w : ι → 𝕜
p : ι → E
hf : StrictConvexOn 𝕜 s f
h₀ : ∀ i ∈ t, 0 < w i
h₁ : Eq.{u_1 + 1} (α := 𝕜) (∑ i ∈ t, w i) 1
hmem : ∀ i ∈ t, p i ∈ s
j : ι
hj : j ∈ t
k : ι
hk : k ∈ t
hjk : p j ≠ p k
this : k ∈ t.erase j
u : Finset ι := (t.erase j).erase k
⊢ j ∉ u

Tactic:
simp [u]
-- Module: Mathlib.Analysis.Convex.Jensen
Goal:
𝕜 : Type u_1
E : Type u_2
β : Type u_4
ι : Type u_5
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : AddCommGroup β
inst_5 : PartialOrder β
inst_6 : IsOrderedAddMonoid β
inst_7 : Module 𝕜 E
inst_8 : Module 𝕜 β
inst_9 : IsStrictOrderedModule 𝕜 β
s : Set E
f : E → β
t : Finset ι
w : ι → 𝕜
p : ι → E
hf : StrictConvexOn 𝕜 s f
h₀ : ∀ i ∈ t, 0 < w i
h₁ : Eq.{u_1 + 1} (α := 𝕜) (∑ i ∈ t, w i) 1
hmem : ∀ i ∈ t, p i ∈ s
j : ι
hj : j ∈ t
k : ι
hk : k ∈ t
hjk : p j ≠ p k
this : k ∈ t.erase j
u : Finset ι := (t.erase j).erase k
⊢ j ∉ u

Tactic:
have hj : j ∉ u := by simp [u]
-- Module: Mathlib.Analysis.Convex.Jensen
Goal:
𝕜 : Type u_1
E : Type u_2
β : Type u_4
ι : Type u_5
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : AddCommGroup β
inst_5 : PartialOrder β
inst_6 : IsOrderedAddMonoid β
inst_7 : Module 𝕜 E
inst_8 : Module 𝕜 β
inst_9 : IsStrictOrderedModule 𝕜 β
s : Set E
f : E → β
t : Finset ι
w : ι → 𝕜
p : ι → E
hf : StrictConvexOn 𝕜 s f
h₀ : ∀ i ∈ t, 0 < w i
h₁ : Eq.{u_1 + 1} (α := 𝕜) (∑ i ∈ t, w i) 1
hmem : ∀ i ∈ t, p i ∈ s
j : ι
hj_1 : j ∈ t
k : ι
hk : k ∈ t
hjk : p j ≠ p k
this : k ∈ t.erase j
u : Finset ι := (t.erase j).erase k
hj : j ∉ u
⊢ k ∉ u

Tactic:
simp [u]
-- Module: Mathlib.Analysis.Convex.Jensen
Goal:
𝕜 : Type u_1
E : Type u_2
β : Type u_4
ι : Type u_5
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : AddCommGroup β
inst_5 : PartialOrder β
inst_6 : IsOrderedAddMonoid β
inst_7 : Module 𝕜 E
inst_8 : Module 𝕜 β
inst_9 : IsStrictOrderedModule 𝕜 β
s : Set E
f : E → β
t : Finset ι
w : ι → 𝕜
p : ι → E
hf : StrictConvexOn 𝕜 s f
h₀ : ∀ i ∈ t, 0 < w i
h₁ : Eq.{u_1 + 1} (α := 𝕜) (∑ i ∈ t, w i) 1
hmem : ∀ i ∈ t, p i ∈ s
j : ι
hj_1 : j ∈ t
k : ι
hk : k ∈ t
hjk : p j ≠ p k
this : k ∈ t.erase j
u : Finset ι := (t.erase j).erase k
hj : j ∉ u
⊢ k ∉ u

Tactic:
have hk : k ∉ u := by simp [u]
-- Module: Mathlib.Analysis.Convex.Jensen
Goal:
𝕜 : Type u_1
E : Type u_2
β : Type u_4
ι : Type u_5
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : AddCommGroup β
inst_5 : PartialOrder β
inst_6 : IsOrderedAddMonoid β
inst_7 : Module 𝕜 E
inst_8 : Module 𝕜 β
inst_9 : IsStrictOrderedModule 𝕜 β
s : Set E
f : E → β
t : Finset ι
w : ι → 𝕜
p : ι → E
hf : StrictConvexOn 𝕜 s f
h₀ : ∀ i ∈ t, 0 < w i
h₁ : Eq.{u_1 + 1} (α := 𝕜) (∑ i ∈ t, w i) 1
hmem : ∀ i ∈ t, p i ∈ s
j : ι
hj_1 : j ∈ t
k : ι
hk_1 : k ∈ t
hjk : p j ≠ p k
this : k ∈ t.erase j
u : Finset ι := (t.erase j).erase k
hj : j ∉ u
hk : k ∉ u
⊢ t = cons j (cons k u hk) ⋯

Tactic:
simp [u, insert_erase this, insert_erase ‹j ∈ t›, *]

Premises used: Finset.insert_erase
-- Module: Mathlib.Analysis.Convex.Jensen
Goal:
𝕜 : Type u_1
E : Type u_2
β : Type u_4
ι : Type u_5
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : AddCommGroup β
inst_5 : PartialOrder β
inst_6 : IsOrderedAddMonoid β
inst_7 : Module 𝕜 E
inst_8 : Module 𝕜 β
inst_9 : IsStrictOrderedModule 𝕜 β
s : Set E
f : E → β
t : Finset ι
w : ι → 𝕜
p : ι → E
hf : StrictConvexOn 𝕜 s f
h₀ : ∀ i ∈ t, 0 < w i
h₁ : Eq.{u_1 + 1} (α := 𝕜) (∑ i ∈ t, w i) 1
hmem : ∀ i ∈ t, p i ∈ s
j : ι
hj_1 : j ∈ t
k : ι
hk_1 : k ∈ t
hjk : p j ≠ p k
this : k ∈ t.erase j
u : Finset ι := (t.erase j).erase k
hj : j ∉ u
hk : k ∉ u
⊢ t = cons j (cons k u hk) ⋯

Tactic:
have ht :
      t = (u.cons k hk).cons j (mem_cons.not.2 <| not_or_intro (ne_of_apply_ne _ hjk) hj) := by
    simp [u, insert_erase this, insert_erase ‹j ∈ t›, *]
-- Module: Mathlib.Analysis.Convex.Jensen
Goal:
𝕜 : Type u_1
E : Type u_2
β : Type u_4
ι : Type u_5
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : AddCommGroup β
inst_5 : PartialOrder β
inst_6 : IsOrderedAddMonoid β
inst_7 : Module 𝕜 E
inst_8 : Module 𝕜 β
inst_9 : IsStrictOrderedModule 𝕜 β
s : Set E
f : E → β
t : Finset ι
w : ι → 𝕜
p : ι → E
hf : StrictConvexOn 𝕜 s f
h₀ : ∀ i ∈ t, 0 < w i
h₁ : Eq.{u_1 + 1} (α := 𝕜) (∑ i ∈ t, w i) 1
hmem : ∀ i ∈ t, p i ∈ s
j : ι
hj_1 : j ∈ t
k : ι
hk_1 : k ∈ t
hjk : p j ≠ p k
this : k ∈ t.erase j
u : Finset ι := (t.erase j).erase k
hj : j ∉ u
hk : k ∉ u
ht : t = cons j (cons k u hk) ⋯
clear_value :
  ∀ (u : Finset ι) (hj : j ∉ u) (hk : k ∉ u) (ht : t = cons j (cons k u hk) ⋯),
    f (∑ i ∈ t, w i • p i) < ∑ i ∈ t, w i • f (p i)
⊢ f (∑ i ∈ t, w i • p i) < ∑ i ∈ t, w i • f (p i)

Tactic:
clear_value u