awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 E
inst_4 : AddCommMonoid β
inst_5 : PartialOrder β
inst_6 : SMul 𝕜 E
inst_7 : SMul 𝕜 β
s : Set E
f : E → β
h : ∀ ⦃x : E⦄, x ∈ s → ∀ ⦃y : E⦄, y ∈ s → ∀ ⦃a b : 𝕜⦄, 0 ≤ a → 0 ≤ b → a + b = 1 → f (a • x + b • y) ≤ a • f x + b • f y
x : E
hx : x ∈ s
y : E
hy : y ∈ s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : 0 < a + b
rw : (a + b) / (a + b) = 1
rw₁ rw₂ : Eq.{u_1 + 1} (α := 𝕜) 1 1
⊢ a / (a + b) + b / (a + b) = 1

Tactic:
rw [← add_div, div_self hab.ne']

Premises used: LT.lt.ne', div_self, add_div
-- 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 E
inst_4 : AddCommMonoid β
inst_5 : PartialOrder β
inst_6 : SMul 𝕜 E
inst_7 : SMul 𝕜 β
s : Set E
f : E → β
h :
  ∀ ⦃x : E⦄,
    x ∈ s →
      ∀ ⦃y : E⦄,
        y ∈ s →
          ∀ ⦃a b : 𝕜⦄,
            0 ≤ a →
              0 ≤ b → 0 < a + b → f ((a / (a + b)) • x + (b / (a + b)) • y) ≤ (a / (a + b)) • f x + (b / (a + b)) • f y
x : E
hx : x ∈ s
y : E
hy : y ∈ s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ f (a • x + b • y) ≤ a • f x + b • f y

Tactic:
simpa [hab, zero_lt_one] using h hx hy ha hb

Premises used: zero_lt_one
-- 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 E
inst_4 : AddCommMonoid β
inst_5 : PartialOrder β
inst_6 : SMul 𝕜 E
inst_7 : SMul 𝕜 β
s : Set E
f : E → β
⊢ ConcaveOn 𝕜 s f ↔
    Convex 𝕜 s ∧
      ∀ ⦃x : E⦄,
        x ∈ s →
          ∀ ⦃y : E⦄,
            y ∈ s →
              ∀ ⦃a b : 𝕜⦄,
                0 ≤ a →
                  0 ≤ b →
                    0 < a + b → (a / (a + b)) • f x + (b / (a + b)) • f y ≤ f ((a / (a + b)) • x + (b / (a + b)) • y)

Tactic:
convexOn_iff_div (β := βᵒᵈ)

Premises used: convexOn_iff_div, ConcaveOn
-- 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 E
inst_4 : AddCommMonoid β
inst_5 : PartialOrder β
inst_6 : SMul 𝕜 E
inst_7 : SMul 𝕜 β
s : Set E
f : E → β
h :
  ∀ ⦃x : E⦄,
    x ∈ s → ∀ ⦃y : E⦄, y ∈ s → x ≠ y → ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → f (a • x + b • y) < a • f x + b • f y
x : E
hx : x ∈ s
y : E
hy : y ∈ s
hxy : x ≠ y
a b : 𝕜
ha : 0 < a
hb : 0 < b
⊢ 0 < a + b

Tactic:
have hab := add_pos ha hb
-- 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 E
inst_4 : AddCommMonoid β
inst_5 : PartialOrder β
inst_6 : SMul 𝕜 E
inst_7 : SMul 𝕜 β
s : Set E
f : E → β
h :
  ∀ ⦃x : E⦄,
    x ∈ s → ∀ ⦃y : E⦄, y ∈ s → x ≠ y → ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → f (a • x + b • y) < a • f x + b • f y
x : E
hx : x ∈ s
y : E
hy : y ∈ s
hxy : x ≠ y
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : 0 < a + b
apply : a / (a + b) + b / (a + b) = 1
⊢ f ((a / (a + b)) • x + (b / (a + b)) • y) < (a / (a + b)) • f x + (b / (a + b)) • f y

Tactic:
apply h hx hy hxy (div_pos ha hab) (div_pos hb hab)

Premises used: div_pos
-- 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 E
inst_4 : AddCommMonoid β
inst_5 : PartialOrder β
inst_6 : SMul 𝕜 E
inst_7 : SMul 𝕜 β
s : Set E
f : E → β
h :
  ∀ ⦃x : E⦄,
    x ∈ s → ∀ ⦃y : E⦄, y ∈ s → x ≠ y → ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → f (a • x + b • y) < a • f x + b • f y
x : E
hx : x ∈ s
y : E
hy : y ∈ s
hxy : x ≠ y
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : 0 < a + b
rw : (a + b) / (a + b) = 1
rw₁ rw₂ : Eq.{u_1 + 1} (α := 𝕜) 1 1
⊢ a / (a + b) + b / (a + b) = 1

Tactic:
rw [← add_div, div_self hab.ne']

Premises used: LT.lt.ne', div_self, add_div
-- 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 E
inst_4 : AddCommMonoid β
inst_5 : PartialOrder β
inst_6 : SMul 𝕜 E
inst_7 : SMul 𝕜 β
s : Set E
f : E → β
h :
  ∀ ⦃x : E⦄,
    x ∈ s →
      ∀ ⦃y : E⦄,
        y ∈ s →
          x ≠ y →
            ∀ ⦃a b : 𝕜⦄,
              0 < a → 0 < b → f ((a / (a + b)) • x + (b / (a + b)) • y) < (a / (a + b)) • f x + (b / (a + b)) • f y
x : E
hx : x ∈ s
y : E
hy : y ∈ s
hxy : x ≠ y
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ f (a • x + b • y) < a • f x + b • f y

Tactic:
simpa [hab, zero_lt_one] using h hx hy hxy ha hb

Premises used: zero_lt_one
-- 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 E
inst_4 : AddCommMonoid β
inst_5 : PartialOrder β
inst_6 : SMul 𝕜 E
inst_7 : SMul 𝕜 β
s : Set E
f : E → β
⊢ StrictConcaveOn 𝕜 s f ↔
    Convex 𝕜 s ∧
      ∀ ⦃x : E⦄,
        x ∈ s →
          ∀ ⦃y : E⦄,
            y ∈ s →
              x ≠ y →
                ∀ ⦃a b : 𝕜⦄,
                  0 < a → 0 < b → (a / (a + b)) • f x + (b / (a + b)) • f y < f ((a / (a + b)) • x + (b / (a + b)) • y)

Tactic:
strictConvexOn_iff_div (β := βᵒᵈ)

Premises used: StrictConcaveOn, strictConvexOn_iff_div
-- 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 : StrictConcaveOn.{u_1, u_4, u_5} 𝕜 (E := α) (β := β) univ (⇑f : (a : α) → β)
⊢ StrictConvexOn.{u_1, u_5, u_4} 𝕜 (E := β) (β := α) univ (⇑f.symm : (a : β) → α)

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

Premises used: StrictConvexOn, convex_univ, And.intro
-- 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 : StrictConcaveOn.{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),
            (f.symm : (a : β) → α) (a • x + b • y) <
              HSMul.hSMul (β := α) a ((f.symm : (a : β) → α) x : α) +
                HSMul.hSMul (β := α) b ((f.symm : (a : β) → α) y : α)
⊢ StrictConvexOn.{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 : StrictConcaveOn.{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'),
    (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) <
    HSMul.hSMul (β := α) a ((f.symm : (a : β) → α) x : α) + HSMul.hSMul (β := α) b ((f.symm : (a : β) → α) 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 : StrictConcaveOn.{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'),
    (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) <
    HSMul.hSMul (β := α) a ((f.symm : (a : β) → α) x : α) + HSMul.hSMul (β := α) b ((f.symm : (a : β) → α) 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 : StrictConcaveOn.{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 : StrictConcaveOn.{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 : StrictConcaveOn.{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 : StrictConcaveOn.{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 : StrictConcaveOn.{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 :
  (f.symm : (a : β) → α)
      (HSMul.hSMul (β := β) a ((f : (a : α) → β) x' : β) + HSMul.hSMul (β := β) b ((f : (a : α) → β) y' : β)) <
    a • x' + b • y'
⊢ (f.symm : (a : β) → α) (a • x + b • y) <
    HSMul.hSMul (β := α) a ((f.symm : (a : β) → α) x : α) + HSMul.hSMul (β := α) b ((f.symm : (a : β) → α) 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 : StrictConcaveOn.{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 :
  HSMul.hSMul (β := β) a ((f : (a : α) → β) x' : β) + HSMul.hSMul (β := β) b ((f : (a : α) → β) y' : β) <
    (f : (a : α) → β) (a • x' + b • y')
⊢ (f.symm : (a : β) → α)
      (HSMul.hSMul (β := β) a ((f : (a : α) → β) x' : β) + HSMul.hSMul (β := β) b ((f : (a : α) → β) y' : β)) <
    a • x' + b • 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 : StrictConcaveOn.{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 : StrictConcaveOn.{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 : StrictConcaveOn.{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'
⊢ HSMul.hSMul (β := β) a ((f : (a : α) → β) x' : β) + HSMul.hSMul (β := β) b ((f : (a : α) → β) y' : β) <
    (f : (a : α) → β) (a • x' + b • 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 : ConcaveOn.{u_1, u_4, u_5} 𝕜 (E := α) (β := β) univ (⇑f : (a : α) → β)
⊢ ConvexOn.{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, ConvexOn
-- 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 : ConcaveOn.{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),
            (f.symm : (a : β) → α) (a • x + b • y) ≤
              HSMul.hSMul (β := α) a ((f.symm : (a : β) → α) x : α) +
                HSMul.hSMul (β := α) b ((f.symm : (a : β) → α) y : α)
⊢ ConvexOn.{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 : ConcaveOn.{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'),
    (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) ≤
    HSMul.hSMul (β := α) a ((f.symm : (a : β) → α) x : α) + HSMul.hSMul (β := α) b ((f.symm : (a : β) → α) 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 : ConcaveOn.{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'),
    (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) ≤
    HSMul.hSMul (β := α) a ((f.symm : (a : β) → α) x : α) + HSMul.hSMul (β := α) b ((f.symm : (a : β) → α) 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 : ConcaveOn.{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 :
  (f.symm : (a : β) → α)
      (HSMul.hSMul (β := β) a ((f : (a : α) → β) x' : β) + HSMul.hSMul (β := β) b ((f : (a : α) → β) y' : β)) ≤
    a • x' + b • y'
⊢ (f.symm : (a : β) → α) (a • x + b • y) ≤
    HSMul.hSMul (β := α) a ((f.symm : (a : β) → α) x : α) + HSMul.hSMul (β := α) b ((f.symm : (a : β) → α) 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 : ConcaveOn.{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 :
  HSMul.hSMul (β := β) a ((f : (a : α) → β) x' : β) + HSMul.hSMul (β := β) b ((f : (a : α) → β) y' : β) ≤
    (f : (a : α) → β) (a • x' + b • y')
⊢ (f.symm : (a : β) → α)
      (HSMul.hSMul (β := β) a ((f : (a : α) → β) x' : β) + HSMul.hSMul (β := β) b ((f : (a : α) → β) y' : β)) ≤
    a • x' + b • 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 : ConcaveOn.{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 : ConcaveOn.{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 : ConcaveOn.{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'
⊢ HSMul.hSMul (β := β) a ((f : (a : α) → β) x' : β) + HSMul.hSMul (β := β) b ((f : (a : α) → β) y' : β) ≤
    (f : (a : α) → β) (a • x' + b • 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
α : 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 : α) → β)
⊢ StrictConcaveOn.{u_1, u_5, u_4} 𝕜 (E := β) (β := α) univ (⇑f.symm : (a : β) → α)

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

Premises used: StrictConcaveOn, convex_univ, And.intro