awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Convex.Function
Goal:
𝕜 : Type u_1
α : Type u_4
β : Type u_5
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid α
inst_3 : PartialOrder α
inst_4 : SMul 𝕜 α
inst_5 : AddCommMonoid β
inst_6 : PartialOrder β
inst_7 : SMul 𝕜 β
f : α ≃o β
hf : StrictConvexOn.{u_1, u_4, u_5} 𝕜 (E := α) (β := β) univ (⇑f : (a : α) → β)
refine :
  ∀ (x : β),
    Membership.mem (γ := Set β) univ x →
      ∀ (y : β),
        Membership.mem (γ := Set β) univ y →
          ∀ (hxy : x ≠ y) (a b : 𝕜) (ha : 0 < a) (hb : 0 < b) (hab : a + b = 1),
            HSMul.hSMul (β := α) a ((f.symm : (a : β) → α) x : α) +
                HSMul.hSMul (β := α) b ((f.symm : (a : β) → α) y : α) <
              (f.symm : (a : β) → α) (a • x + b • y)
⊢ StrictConcaveOn.{u_1, u_5, u_4} 𝕜 (E := β) (β := α) univ (⇑f.symm : (a : β) → α)

Tactic:
refine ⟨convex_univ, fun x _ y _ hxy a b ha hb hab => ?_⟩
-- Module: Mathlib.Analysis.Convex.Function
Goal:
𝕜 : Type u_1
α : Type u_4
β : Type u_5
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid α
inst_3 : PartialOrder α
inst_4 : SMul 𝕜 α
inst_5 : AddCommMonoid β
inst_6 : PartialOrder β
inst_7 : SMul 𝕜 β
f : α ≃o β
hf : StrictConvexOn.{u_1, u_4, u_5} 𝕜 (E := α) (β := β) univ (⇑f : (a : α) → β)
x : β
h : Membership.mem (γ := Set β) univ x
y : β
h_1 : Membership.mem (γ := Set β) univ y
hxy : x ≠ y
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
obtain :
  ∀ (x' : α) (hx'' : x = (f : (a : α) → β) x'),
    HSMul.hSMul (β := α) a ((f.symm : (a : β) → α) x : α) + HSMul.hSMul (β := α) b ((f.symm : (a : β) → α) y : α) <
      (f.symm : (a : β) → α) (a • x + b • y)
⊢ HSMul.hSMul (β := α) a ((f.symm : (a : β) → α) x : α) + HSMul.hSMul (β := α) b ((f.symm : (a : β) → α) y : α) <
    (f.symm : (a : β) → α) (a • x + b • y)

Tactic:
obtain ⟨x', hx''⟩ := f.surjective.exists.mp ⟨x, rfl⟩

Premises used: Function.Surjective.exists, OrderIso.surjective, Exists.intro, Iff.mp, rfl
-- Module: Mathlib.Analysis.Convex.Function
Goal:
𝕜 : Type u_1
α : Type u_4
β : Type u_5
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid α
inst_3 : PartialOrder α
inst_4 : SMul 𝕜 α
inst_5 : AddCommMonoid β
inst_6 : PartialOrder β
inst_7 : SMul 𝕜 β
f : α ≃o β
hf : StrictConvexOn.{u_1, u_4, u_5} 𝕜 (E := α) (β := β) univ (⇑f : (a : α) → β)
x : β
h : Membership.mem (γ := Set β) univ x
y : β
h_1 : Membership.mem (γ := Set β) univ y
hxy : x ≠ y
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
x' : α
hx'' : x = (f : (a : α) → β) x'
obtain :
  ∀ (y' : α) (hy'' : y = (f : (a : α) → β) y'),
    HSMul.hSMul (β := α) a ((f.symm : (a : β) → α) x : α) + HSMul.hSMul (β := α) b ((f.symm : (a : β) → α) y : α) <
      (f.symm : (a : β) → α) (a • x + b • y)
⊢ HSMul.hSMul (β := α) a ((f.symm : (a : β) → α) x : α) + HSMul.hSMul (β := α) b ((f.symm : (a : β) → α) y : α) <
    (f.symm : (a : β) → α) (a • x + b • y)

Tactic:
obtain ⟨y', hy''⟩ := f.surjective.exists.mp ⟨y, rfl⟩

Premises used: Function.Surjective.exists, OrderIso.surjective, Exists.intro, Iff.mp, rfl
-- Module: Mathlib.Analysis.Convex.Function
Goal:
𝕜 : Type u_1
α : Type u_4
β : Type u_5
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid α
inst_3 : PartialOrder α
inst_4 : SMul 𝕜 α
inst_5 : AddCommMonoid β
inst_6 : PartialOrder β
inst_7 : SMul 𝕜 β
f : α ≃o β
hf : StrictConvexOn.{u_1, u_4, u_5} 𝕜 (E := α) (β := β) univ (⇑f : (a : α) → β)
x : β
h : Membership.mem (γ := Set β) univ x
y : β
h_1 : Membership.mem (γ := Set β) univ y
hxy : x ≠ y
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
x' : α
hx'' : x = (f : (a : α) → β) x'
y' : α
hy'' : y = (f : (a : α) → β) y'
rw : x ≠ y
⊢ x' ≠ y'

Tactic:
rw [← f.injective.ne_iff, ← hx'', ← hy'']

Premises used: Function.Injective.ne_iff, OrderIso.injective
-- Module: Mathlib.Analysis.Convex.Function
Goal:
𝕜 : Type u_1
α : Type u_4
β : Type u_5
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid α
inst_3 : PartialOrder α
inst_4 : SMul 𝕜 α
inst_5 : AddCommMonoid β
inst_6 : PartialOrder β
inst_7 : SMul 𝕜 β
f : α ≃o β
hf : StrictConvexOn.{u_1, u_4, u_5} 𝕜 (E := α) (β := β) univ (⇑f : (a : α) → β)
x : β
h : Membership.mem (γ := Set β) univ x
y : β
h_1 : Membership.mem (γ := Set β) univ y
hxy : x ≠ y
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
x' : α
hx'' : x = (f : (a : α) → β) x'
y' : α
hy'' : y = (f : (a : α) → β) y'
⊢ x ≠ y

Tactic:
hxy
-- Module: Mathlib.Analysis.Convex.Function
Goal:
𝕜 : Type u_1
α : Type u_4
β : Type u_5
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid α
inst_3 : PartialOrder α
inst_4 : SMul 𝕜 α
inst_5 : AddCommMonoid β
inst_6 : PartialOrder β
inst_7 : SMul 𝕜 β
f : α ≃o β
hf : StrictConvexOn.{u_1, u_4, u_5} 𝕜 (E := α) (β := β) univ (⇑f : (a : α) → β)
x : β
h : Membership.mem (γ := Set β) univ x
y : β
h_1 : Membership.mem (γ := Set β) univ y
hxy : x ≠ y
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
x' : α
hx'' : x = (f : (a : α) → β) x'
y' : α
hy'' : y = (f : (a : α) → β) y'
⊢ x ≠ y

Tactic:
exact hxy
-- Module: Mathlib.Analysis.Convex.Function
Goal:
𝕜 : Type u_1
α : Type u_4
β : Type u_5
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid α
inst_3 : PartialOrder α
inst_4 : SMul 𝕜 α
inst_5 : AddCommMonoid β
inst_6 : PartialOrder β
inst_7 : SMul 𝕜 β
f : α ≃o β
hf : StrictConvexOn.{u_1, u_4, u_5} 𝕜 (E := α) (β := β) univ (⇑f : (a : α) → β)
x : β
h : Membership.mem (γ := Set β) univ x
y : β
h_1 : Membership.mem (γ := Set β) univ y
hxy : x ≠ y
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
x' : α
hx'' : x = (f : (a : α) → β) x'
y' : α
hy'' : y = (f : (a : α) → β) y'
⊢ x' ≠ y'

Tactic:
have hxy' : x' ≠ y' := by rw [← f.injective.ne_iff, ← hx'', ← hy'']; exact hxy
-- Module: Mathlib.Analysis.Convex.Function
Goal:
𝕜 : Type u_1
α : Type u_4
β : Type u_5
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid α
inst_3 : PartialOrder α
inst_4 : SMul 𝕜 α
inst_5 : AddCommMonoid β
inst_6 : PartialOrder β
inst_7 : SMul 𝕜 β
f : α ≃o β
hf : StrictConvexOn.{u_1, u_4, u_5} 𝕜 (E := α) (β := β) univ (⇑f : (a : α) → β)
x : β
h : Membership.mem (γ := Set β) univ x
y : β
h_1 : Membership.mem (γ := Set β) univ y
hxy : x ≠ y
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
x' : α
hx'' : x = (f : (a : α) → β) x'
y' : α
hy'' : y = (f : (a : α) → β) y'
hxy' : x' ≠ y'
simp :
  a • x' + b • y' <
    (f.symm : (a : β) → α)
      (HSMul.hSMul (β := β) a ((f : (a : α) → β) x' : β) + HSMul.hSMul (β := β) b ((f : (a : α) → β) y' : β))
⊢ HSMul.hSMul (β := α) a ((f.symm : (a : β) → α) x : α) + HSMul.hSMul (β := α) b ((f.symm : (a : β) → α) y : α) <
    (f.symm : (a : β) → α) (a • x + b • y)

Tactic:
simp only [hx'', hy'', OrderIso.symm_apply_apply, gt_iff_lt]

Premises used: gt_iff_lt, OrderIso.symm_apply_apply
-- Module: Mathlib.Analysis.Convex.Function
Goal:
𝕜 : Type u_1
α : Type u_4
β : Type u_5
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid α
inst_3 : PartialOrder α
inst_4 : SMul 𝕜 α
inst_5 : AddCommMonoid β
inst_6 : PartialOrder β
inst_7 : SMul 𝕜 β
f : α ≃o β
hf : StrictConvexOn.{u_1, u_4, u_5} 𝕜 (E := α) (β := β) univ (⇑f : (a : α) → β)
x : β
h : Membership.mem (γ := Set β) univ x
y : β
h_1 : Membership.mem (γ := Set β) univ y
hxy : x ≠ y
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
x' : α
hx'' : x = (f : (a : α) → β) x'
y' : α
hy'' : y = (f : (a : α) → β) y'
hxy' : x' ≠ y'
rw :
  (f : (a : α) → β) (a • x' + b • y') <
    HSMul.hSMul (β := β) a ((f : (a : α) → β) x' : β) + HSMul.hSMul (β := β) b ((f : (a : α) → β) y' : β)
⊢ a • x' + b • y' <
    (f.symm : (a : β) → α)
      (HSMul.hSMul (β := β) a ((f : (a : α) → β) x' : β) + HSMul.hSMul (β := β) b ((f : (a : α) → β) y' : β))

Tactic:
rw [← f.lt_iff_lt, OrderIso.apply_symm_apply]

Premises used: OrderIso.lt_iff_lt, OrderIso.apply_symm_apply
-- Module: Mathlib.Analysis.Convex.Function
Goal:
𝕜 : Type u_1
α : Type u_4
β : Type u_5
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid α
inst_3 : PartialOrder α
inst_4 : SMul 𝕜 α
inst_5 : AddCommMonoid β
inst_6 : PartialOrder β
inst_7 : SMul 𝕜 β
f : α ≃o β
hf : StrictConvexOn.{u_1, u_4, u_5} 𝕜 (E := α) (β := β) univ (⇑f : (a : α) → β)
x : β
h : Membership.mem (γ := Set β) univ x
y : β
h_1 : Membership.mem (γ := Set β) univ y
hxy : x ≠ y
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
x' : α
hx'' : x = (f : (a : α) → β) x'
y' : α
hy'' : y = (f : (a : α) → β) y'
hxy' : x' ≠ y'
⊢ Membership.mem (γ := Set α) univ x'

Tactic:
simp
-- Module: Mathlib.Analysis.Convex.Function
Goal:
𝕜 : Type u_1
α : Type u_4
β : Type u_5
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid α
inst_3 : PartialOrder α
inst_4 : SMul 𝕜 α
inst_5 : AddCommMonoid β
inst_6 : PartialOrder β
inst_7 : SMul 𝕜 β
f : α ≃o β
hf : StrictConvexOn.{u_1, u_4, u_5} 𝕜 (E := α) (β := β) univ (⇑f : (a : α) → β)
x : β
h : Membership.mem (γ := Set β) univ x
y : β
h_1 : Membership.mem (γ := Set β) univ y
hxy : x ≠ y
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
x' : α
hx'' : x = (f : (a : α) → β) x'
y' : α
hy'' : y = (f : (a : α) → β) y'
hxy' : x' ≠ y'
⊢ Membership.mem (γ := Set α) univ y'

Tactic:
simp
-- Module: Mathlib.Analysis.Convex.Function
Goal:
𝕜 : Type u_1
α : Type u_4
β : Type u_5
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid α
inst_3 : PartialOrder α
inst_4 : SMul 𝕜 α
inst_5 : AddCommMonoid β
inst_6 : PartialOrder β
inst_7 : SMul 𝕜 β
f : α ≃o β
hf : StrictConvexOn.{u_1, u_4, u_5} 𝕜 (E := α) (β := β) univ (⇑f : (a : α) → β)
x : β
h : Membership.mem (γ := Set β) univ x
y : β
h_1 : Membership.mem (γ := Set β) univ y
hxy : x ≠ y
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
x' : α
hx'' : x = (f : (a : α) → β) x'
y' : α
hy'' : y = (f : (a : α) → β) y'
hxy' : x' ≠ y'
⊢ (f : (a : α) → β) (a • x' + b • y') <
    HSMul.hSMul (β := β) a ((f : (a : α) → β) x' : β) + HSMul.hSMul (β := β) b ((f : (a : α) → β) y' : β)

Tactic:
exact hf.2 (by simp : x' ∈ univ) (by simp : y' ∈ univ) hxy' ha hb hab

Premises used: And.right
-- Module: Mathlib.Analysis.Convex.Function
Goal:
𝕜 : Type u_1
α : Type u_4
β : Type u_5
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid α
inst_3 : PartialOrder α
inst_4 : SMul 𝕜 α
inst_5 : AddCommMonoid β
inst_6 : PartialOrder β
inst_7 : SMul 𝕜 β
f : α ≃o β
hf : ConvexOn.{u_1, u_4, u_5} 𝕜 (E := α) (β := β) univ (⇑f : (a : α) → β)
⊢ ConcaveOn.{u_1, u_5, u_4} 𝕜 (E := β) (β := α) univ (⇑f.symm : (a : β) → α)

Tactic:
⟨convex_univ, fun x _ y _ a b ha hb hab => ?_⟩

Premises used: convex_univ, And.intro, ConcaveOn
-- Module: Mathlib.Analysis.Convex.Function
Goal:
𝕜 : Type u_1
α : Type u_4
β : Type u_5
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid α
inst_3 : PartialOrder α
inst_4 : SMul 𝕜 α
inst_5 : AddCommMonoid β
inst_6 : PartialOrder β
inst_7 : SMul 𝕜 β
f : α ≃o β
hf : ConvexOn.{u_1, u_4, u_5} 𝕜 (E := α) (β := β) univ (⇑f : (a : α) → β)
refine :
  ∀ (x : β),
    Membership.mem (γ := Set β) univ x →
      ∀ (y : β),
        Membership.mem (γ := Set β) univ y →
          ∀ (a b : 𝕜) (ha : 0 ≤ a) (hb : 0 ≤ b) (hab : a + b = 1),
            HSMul.hSMul (β := α) a ((f.symm : (a : β) → α) x : α) +
                HSMul.hSMul (β := α) b ((f.symm : (a : β) → α) y : α) ≤
              (f.symm : (a : β) → α) (a • x + b • y)
⊢ ConcaveOn.{u_1, u_5, u_4} 𝕜 (E := β) (β := α) univ (⇑f.symm : (a : β) → α)

Tactic:
refine ⟨convex_univ, fun x _ y _ a b ha hb hab => ?_⟩
-- Module: Mathlib.Analysis.Convex.Function
Goal:
𝕜 : Type u_1
α : Type u_4
β : Type u_5
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid α
inst_3 : PartialOrder α
inst_4 : SMul 𝕜 α
inst_5 : AddCommMonoid β
inst_6 : PartialOrder β
inst_7 : SMul 𝕜 β
f : α ≃o β
hf : ConvexOn.{u_1, u_4, u_5} 𝕜 (E := α) (β := β) univ (⇑f : (a : α) → β)
x : β
h : Membership.mem (γ := Set β) univ x
y : β
h_1 : Membership.mem (γ := Set β) univ y
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
obtain :
  ∀ (x' : α) (hx'' : x = (f : (a : α) → β) x'),
    HSMul.hSMul (β := α) a ((f.symm : (a : β) → α) x : α) + HSMul.hSMul (β := α) b ((f.symm : (a : β) → α) y : α) ≤
      (f.symm : (a : β) → α) (a • x + b • y)
⊢ HSMul.hSMul (β := α) a ((f.symm : (a : β) → α) x : α) + HSMul.hSMul (β := α) b ((f.symm : (a : β) → α) y : α) ≤
    (f.symm : (a : β) → α) (a • x + b • y)

Tactic:
obtain ⟨x', hx''⟩ := f.surjective.exists.mp ⟨x, rfl⟩

Premises used: Function.Surjective.exists, OrderIso.surjective, Exists.intro, Iff.mp, rfl
-- Module: Mathlib.Analysis.Convex.Function
Goal:
𝕜 : Type u_1
α : Type u_4
β : Type u_5
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid α
inst_3 : PartialOrder α
inst_4 : SMul 𝕜 α
inst_5 : AddCommMonoid β
inst_6 : PartialOrder β
inst_7 : SMul 𝕜 β
f : α ≃o β
hf : ConvexOn.{u_1, u_4, u_5} 𝕜 (E := α) (β := β) univ (⇑f : (a : α) → β)
x : β
h : Membership.mem (γ := Set β) univ x
y : β
h_1 : Membership.mem (γ := Set β) univ y
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
x' : α
hx'' : x = (f : (a : α) → β) x'
obtain :
  ∀ (y' : α) (hy'' : y = (f : (a : α) → β) y'),
    HSMul.hSMul (β := α) a ((f.symm : (a : β) → α) x : α) + HSMul.hSMul (β := α) b ((f.symm : (a : β) → α) y : α) ≤
      (f.symm : (a : β) → α) (a • x + b • y)
⊢ HSMul.hSMul (β := α) a ((f.symm : (a : β) → α) x : α) + HSMul.hSMul (β := α) b ((f.symm : (a : β) → α) y : α) ≤
    (f.symm : (a : β) → α) (a • x + b • y)

Tactic:
obtain ⟨y', hy''⟩ := f.surjective.exists.mp ⟨y, rfl⟩

Premises used: Function.Surjective.exists, OrderIso.surjective, Exists.intro, Iff.mp, rfl
-- Module: Mathlib.Analysis.Convex.Function
Goal:
𝕜 : Type u_1
α : Type u_4
β : Type u_5
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid α
inst_3 : PartialOrder α
inst_4 : SMul 𝕜 α
inst_5 : AddCommMonoid β
inst_6 : PartialOrder β
inst_7 : SMul 𝕜 β
f : α ≃o β
hf : ConvexOn.{u_1, u_4, u_5} 𝕜 (E := α) (β := β) univ (⇑f : (a : α) → β)
x : β
h : Membership.mem (γ := Set β) univ x
y : β
h_1 : Membership.mem (γ := Set β) univ y
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
x' : α
hx'' : x = (f : (a : α) → β) x'
y' : α
hy'' : y = (f : (a : α) → β) y'
simp :
  a • x' + b • y' ≤
    (f.symm : (a : β) → α)
      (HSMul.hSMul (β := β) a ((f : (a : α) → β) x' : β) + HSMul.hSMul (β := β) b ((f : (a : α) → β) y' : β))
⊢ HSMul.hSMul (β := α) a ((f.symm : (a : β) → α) x : α) + HSMul.hSMul (β := α) b ((f.symm : (a : β) → α) y : α) ≤
    (f.symm : (a : β) → α) (a • x + b • y)

Tactic:
simp only [hx'', hy'', OrderIso.symm_apply_apply]

Premises used: OrderIso.symm_apply_apply
-- Module: Mathlib.Analysis.Convex.Function
Goal:
𝕜 : Type u_1
α : Type u_4
β : Type u_5
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid α
inst_3 : PartialOrder α
inst_4 : SMul 𝕜 α
inst_5 : AddCommMonoid β
inst_6 : PartialOrder β
inst_7 : SMul 𝕜 β
f : α ≃o β
hf : ConvexOn.{u_1, u_4, u_5} 𝕜 (E := α) (β := β) univ (⇑f : (a : α) → β)
x : β
h : Membership.mem (γ := Set β) univ x
y : β
h_1 : Membership.mem (γ := Set β) univ y
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
x' : α
hx'' : x = (f : (a : α) → β) x'
y' : α
hy'' : y = (f : (a : α) → β) y'
rw :
  (f : (a : α) → β) (a • x' + b • y') ≤
    HSMul.hSMul (β := β) a ((f : (a : α) → β) x' : β) + HSMul.hSMul (β := β) b ((f : (a : α) → β) y' : β)
⊢ a • x' + b • y' ≤
    (f.symm : (a : β) → α)
      (HSMul.hSMul (β := β) a ((f : (a : α) → β) x' : β) + HSMul.hSMul (β := β) b ((f : (a : α) → β) y' : β))

Tactic:
rw [← f.le_iff_le, OrderIso.apply_symm_apply]

Premises used: OrderIso.apply_symm_apply, OrderIso.le_iff_le
-- Module: Mathlib.Analysis.Convex.Function
Goal:
𝕜 : Type u_1
α : Type u_4
β : Type u_5
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid α
inst_3 : PartialOrder α
inst_4 : SMul 𝕜 α
inst_5 : AddCommMonoid β
inst_6 : PartialOrder β
inst_7 : SMul 𝕜 β
f : α ≃o β
hf : ConvexOn.{u_1, u_4, u_5} 𝕜 (E := α) (β := β) univ (⇑f : (a : α) → β)
x : β
h : Membership.mem (γ := Set β) univ x
y : β
h_1 : Membership.mem (γ := Set β) univ y
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
x' : α
hx'' : x = (f : (a : α) → β) x'
y' : α
hy'' : y = (f : (a : α) → β) y'
⊢ Membership.mem (γ := Set α) univ x'

Tactic:
simp
-- Module: Mathlib.Analysis.Convex.Function
Goal:
𝕜 : Type u_1
α : Type u_4
β : Type u_5
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid α
inst_3 : PartialOrder α
inst_4 : SMul 𝕜 α
inst_5 : AddCommMonoid β
inst_6 : PartialOrder β
inst_7 : SMul 𝕜 β
f : α ≃o β
hf : ConvexOn.{u_1, u_4, u_5} 𝕜 (E := α) (β := β) univ (⇑f : (a : α) → β)
x : β
h : Membership.mem (γ := Set β) univ x
y : β
h_1 : Membership.mem (γ := Set β) univ y
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
x' : α
hx'' : x = (f : (a : α) → β) x'
y' : α
hy'' : y = (f : (a : α) → β) y'
⊢ Membership.mem (γ := Set α) univ y'

Tactic:
simp
-- Module: Mathlib.Analysis.Convex.Function
Goal:
𝕜 : Type u_1
α : Type u_4
β : Type u_5
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid α
inst_3 : PartialOrder α
inst_4 : SMul 𝕜 α
inst_5 : AddCommMonoid β
inst_6 : PartialOrder β
inst_7 : SMul 𝕜 β
f : α ≃o β
hf : ConvexOn.{u_1, u_4, u_5} 𝕜 (E := α) (β := β) univ (⇑f : (a : α) → β)
x : β
h : Membership.mem (γ := Set β) univ x
y : β
h_1 : Membership.mem (γ := Set β) univ y
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
x' : α
hx'' : x = (f : (a : α) → β) x'
y' : α
hy'' : y = (f : (a : α) → β) y'
⊢ (f : (a : α) → β) (a • x' + b • y') ≤
    HSMul.hSMul (β := β) a ((f : (a : α) → β) x' : β) + HSMul.hSMul (β := β) b ((f : (a : α) → β) y' : β)

Tactic:
exact hf.2 (by simp : x' ∈ univ) (by simp : y' ∈ univ) ha hb hab

Premises used: And.right
-- Module: Mathlib.Analysis.Convex.Function
Goal:
𝕜 : Type u_1
E : Type u_2
β : Type u_5
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommMonoid β
inst_4 : PartialOrder β
inst_5 : IsOrderedAddMonoid β
inst_6 : AddCommMonoid E
inst_7 : SMul 𝕜 E
inst_8 : Module 𝕜 β
inst_9 : PosSMulMono 𝕜 β
f : E → β
s : Set E
x y : E
hf : StrictConvexOn 𝕜 s f
hfx : IsMinOn f s x
hfy : IsMinOn f s y
hx : x ∈ s
hy : y ∈ s
by_contra : ∀ (hxy : ¬x = y), False
⊢ x = y

Tactic:
by_contra hxy
-- Module: Mathlib.Analysis.Convex.Function
Goal:
𝕜 : Type u_1
E : Type u_2
β : Type u_5
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommMonoid β
inst_4 : PartialOrder β
inst_5 : IsOrderedAddMonoid β
inst_6 : AddCommMonoid E
inst_7 : SMul 𝕜 E
inst_8 : Module 𝕜 β
inst_9 : PosSMulMono 𝕜 β
f : E → β
s : Set E
x y : E
hf : StrictConvexOn 𝕜 s f
hfx : IsMinOn f s x
hfy : IsMinOn f s y
hx : x ∈ s
hy : y ∈ s
hxy : ¬x = y
z : E := HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 2⁻¹ x + HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 2⁻¹ y
⊢ LE.le.{u_1} (α := 𝕜) 0 2⁻¹

Tactic:
simp
-- Module: Mathlib.Analysis.Convex.Function
Goal:
𝕜 : Type u_1
E : Type u_2
β : Type u_5
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommMonoid β
inst_4 : PartialOrder β
inst_5 : IsOrderedAddMonoid β
inst_6 : AddCommMonoid E
inst_7 : SMul 𝕜 E
inst_8 : Module 𝕜 β
inst_9 : PosSMulMono 𝕜 β
f : E → β
s : Set E
x y : E
hf : StrictConvexOn 𝕜 s f
hfx : IsMinOn f s x
hfy : IsMinOn f s y
hx : x ∈ s
hy : y ∈ s
hxy : ¬x = y
z : E := HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 2⁻¹ x + HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 2⁻¹ y
⊢ HAdd.hAdd (α := 𝕜) 2⁻¹ 2⁻¹ = 1

Tactic:
norm_num
-- Module: Mathlib.Analysis.Convex.Function
Goal:
𝕜 : Type u_1
E : Type u_2
β : Type u_5
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommMonoid β
inst_4 : PartialOrder β
inst_5 : IsOrderedAddMonoid β
inst_6 : AddCommMonoid E
inst_7 : SMul 𝕜 E
inst_8 : Module 𝕜 β
inst_9 : PosSMulMono 𝕜 β
f : E → β
s : Set E
x y : E
hf : StrictConvexOn 𝕜 s f
hfx : IsMinOn f s x
hfy : IsMinOn f s y
hx : x ∈ s
hy : y ∈ s
hxy : ¬x = y
z : E := HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 2⁻¹ x + HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 2⁻¹ y
⊢ z ∈ s

Tactic:
have hz : z ∈ s := hf.1 hx hy (by simp) (by simp) <| by norm_num
-- Module: Mathlib.Analysis.Convex.Function
Goal:
𝕜 : Type u_1
E : Type u_2
β : Type u_5
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommMonoid β
inst_4 : PartialOrder β
inst_5 : IsOrderedAddMonoid β
inst_6 : AddCommMonoid E
inst_7 : SMul 𝕜 E
inst_8 : Module 𝕜 β
inst_9 : PosSMulMono 𝕜 β
f : E → β
s : Set E
x y : E
hf : StrictConvexOn 𝕜 s f
hfx : IsMinOn f s x
hfy : IsMinOn f s y
hx : x ∈ s
hy : y ∈ s
hxy : ¬x = y
z : E := HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 2⁻¹ x + HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 2⁻¹ y
hz : z ∈ s
⊢ False

Tactic:
lt_irrefl (f z) ?_

Premises used: lt_irrefl
-- Module: Mathlib.Analysis.Convex.Function
Goal:
𝕜 : Type u_1
E : Type u_2
β : Type u_5
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommMonoid β
inst_4 : PartialOrder β
inst_5 : IsOrderedAddMonoid β
inst_6 : AddCommMonoid E
inst_7 : SMul 𝕜 E
inst_8 : Module 𝕜 β
inst_9 : PosSMulMono 𝕜 β
f : E → β
s : Set E
x y : E
hf : StrictConvexOn 𝕜 s f
hfx : IsMinOn f s x
hfy : IsMinOn f s y
hx : x ∈ s
hy : y ∈ s
hxy : ¬x = y
z : E := HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 2⁻¹ x + HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 2⁻¹ y
hz : z ∈ s
refine : f z < f z
⊢ False

Tactic:
refine lt_irrefl (f z) ?_

Premises used: lt_irrefl
-- Module: Mathlib.Analysis.Convex.Function
Goal:
𝕜 : Type u_1
E : Type u_2
β : Type u_5
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommMonoid β
inst_4 : PartialOrder β
inst_5 : IsOrderedAddMonoid β
inst_6 : AddCommMonoid E
inst_7 : SMul 𝕜 E
inst_8 : Module 𝕜 β
inst_9 : PosSMulMono 𝕜 β
f : E → β
s : Set E
x y : E
hf : StrictConvexOn 𝕜 s f
hfx : IsMinOn f s x
hfy : IsMinOn f s y
hx : x ∈ s
hy : y ∈ s
hxy : ¬x = y
z : E := HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 2⁻¹ x + HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 2⁻¹ y
hz : z ∈ s
⊢ LT.lt.{u_1} (α := 𝕜) 0 2⁻¹

Tactic:
simp
-- Module: Mathlib.Analysis.Convex.Function
Goal:
𝕜 : Type u_1
E : Type u_2
β : Type u_5
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommMonoid β
inst_4 : PartialOrder β
inst_5 : IsOrderedAddMonoid β
inst_6 : AddCommMonoid E
inst_7 : SMul 𝕜 E
inst_8 : Module 𝕜 β
inst_9 : PosSMulMono 𝕜 β
f : E → β
s : Set E
x y : E
hf : StrictConvexOn 𝕜 s f
hfx : IsMinOn f s x
hfy : IsMinOn f s y
hx : x ∈ s
hy : y ∈ s
hxy : ¬x = y
z : E := HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 2⁻¹ x + HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 2⁻¹ y
hz : z ∈ s
⊢ HAdd.hAdd (α := 𝕜) 2⁻¹ 2⁻¹ = 1

Tactic:
norm_num
-- Module: Mathlib.Analysis.Convex.Function
Goal:
𝕜 : Type u_1
E : Type u_2
β : Type u_5
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommMonoid β
inst_4 : PartialOrder β
inst_5 : IsOrderedAddMonoid β
inst_6 : AddCommMonoid E
inst_7 : SMul 𝕜 E
inst_8 : Module 𝕜 β
inst_9 : PosSMulMono 𝕜 β
f : E → β
s : Set E
x y : E
hf : StrictConvexOn 𝕜 s f
hfx : IsMinOn f s x
hfy : IsMinOn f s y
hx : x ∈ s
hy : y ∈ s
hxy : ¬x = y
z : E := HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 2⁻¹ x + HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 2⁻¹ y
hz : z ∈ s
h₁ : f x ≤ f z
h₂ : f y ≤ f z
⊢ HSMul.hSMul.{u_1, u_5, u_5} (α := 𝕜) 2⁻¹ (f x) + HSMul.hSMul.{u_1, u_5, u_5} (α := 𝕜) 2⁻¹ (f y) ≤
    HSMul.hSMul.{u_1, u_5, u_5} (α := 𝕜) 2⁻¹ (f z) + HSMul.hSMul.{u_1, u_5, u_5} (α := 𝕜) 2⁻¹ (f z)

Tactic:
gcongr
-- Module: Mathlib.Analysis.Convex.Function
Goal:
𝕜 : Type u_1
E : Type u_2
β : Type u_5
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommMonoid β
inst_4 : PartialOrder β
inst_5 : IsOrderedAddMonoid β
inst_6 : AddCommMonoid E
inst_7 : SMul 𝕜 E
inst_8 : Module 𝕜 β
inst_9 : PosSMulMono 𝕜 β
f : E → β
s : Set E
x y : E
hf : StrictConvexOn 𝕜 s f
hfx : IsMinOn f s x
hfy : IsMinOn f s y
hx : x ∈ s
hy : y ∈ s
hxy : ¬x = y
z : E := HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 2⁻¹ x + HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 2⁻¹ y
hz : z ∈ s
⊢ f x ≤ f z

Tactic:
hfx hz

Premises used: Set.Mem, setOf
-- Module: Mathlib.Analysis.Convex.Function
Goal:
𝕜 : Type u_1
E : Type u_2
β : Type u_5
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommMonoid β
inst_4 : PartialOrder β
inst_5 : IsOrderedAddMonoid β
inst_6 : AddCommMonoid E
inst_7 : SMul 𝕜 E
inst_8 : Module 𝕜 β
inst_9 : PosSMulMono 𝕜 β
f : E → β
s : Set E
x y : E
hf : StrictConvexOn 𝕜 s f
hfx : IsMinOn f s x
hfy : IsMinOn f s y
hx : x ∈ s
hy : y ∈ s
hxy : ¬x = y
z : E := HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 2⁻¹ x + HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 2⁻¹ y
hz : z ∈ s
⊢ f y ≤ f z

Tactic:
hfy hz

Premises used: Set.Mem, setOf