-- Mathlib/Analysis/Convex/Function.lean
theorem OrderIso.convexOn_symm (f : α ≃o β) (hf : ConcaveOn 𝕜 univ f) :
    ConvexOn 𝕜 univ f.symm

Proof state:
𝕜 : Type u_1
α : Type u_4
β : Type u_5
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : OrderedAddCommMonoid α
inst✝² : SMul 𝕜 α
inst✝¹ : OrderedAddCommMonoid β
inst✝ : SMul 𝕜 β
f : α ≃o β
hf : ConcaveOn 𝕜 univ ⇑f
x : β
x✝¹ : x ∈ univ
y : β
x✝ : y ∈ univ
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
x' : α
hx'' : x = f x'
y' : α
hy'' : y = f y'
⊢ x' ∈ univ

Tactic:
simp

Result:
no goals

Proof state:
𝕜 : Type u_1
α : Type u_4
β : Type u_5
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : OrderedAddCommMonoid α
inst✝² : SMul 𝕜 α
inst✝¹ : OrderedAddCommMonoid β
inst✝ : SMul 𝕜 β
f : α ≃o β
hf : ConcaveOn 𝕜 univ ⇑f
⊢ ConvexOn 𝕜 univ ⇑f.symm

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

Result:
𝕜 : Type u_1
α : Type u_4
β : Type u_5
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : OrderedAddCommMonoid α
inst✝² : SMul 𝕜 α
inst✝¹ : OrderedAddCommMonoid β
inst✝ : SMul 𝕜 β
f : α ≃o β
hf : ConcaveOn 𝕜 univ ⇑f
x : β
x✝¹ : x ∈ univ
y : β
x✝ : y ∈ univ
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ f.symm (a • x + b • y) ≤ a • f.symm x + b • f.symm y

Proof state:
case intro.intro
𝕜 : Type u_1
α : Type u_4
β : Type u_5
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : OrderedAddCommMonoid α
inst✝² : SMul 𝕜 α
inst✝¹ : OrderedAddCommMonoid β
inst✝ : SMul 𝕜 β
f : α ≃o β
hf : ConcaveOn 𝕜 univ ⇑f
x : β
x✝¹ : x ∈ univ
y : β
x✝ : y ∈ univ
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
x' : α
hx'' : x = f x'
y' : α
hy'' : y = f y'
⊢ a • f x' + b • f y' ≤ f (a • x' + b • y')

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

Result:
no goals

Proof state:
𝕜 : Type u_1
α : Type u_4
β : Type u_5
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : OrderedAddCommMonoid α
inst✝² : SMul 𝕜 α
inst✝¹ : OrderedAddCommMonoid β
inst✝ : SMul 𝕜 β
f : α ≃o β
hf : ConcaveOn 𝕜 univ ⇑f
x : β
x✝¹ : x ∈ univ
y : β
x✝ : y ∈ univ
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ f.symm (a • x + b • y) ≤ a • f.symm x + b • f.symm y

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

Result:
case intro
𝕜 : Type u_1
α : Type u_4
β : Type u_5
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : OrderedAddCommMonoid α
inst✝² : SMul 𝕜 α
inst✝¹ : OrderedAddCommMonoid β
inst✝ : SMul 𝕜 β
f : α ≃o β
hf : ConcaveOn 𝕜 univ ⇑f
x : β
x✝¹ : x ∈ univ
y : β
x✝ : y ∈ univ
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
x' : α
hx'' : x = f x'
⊢ f.symm (a • x + b • y) ≤ a • f.symm x + b • f.symm y

Proof state:
case intro
𝕜 : Type u_1
α : Type u_4
β : Type u_5
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : OrderedAddCommMonoid α
inst✝² : SMul 𝕜 α
inst✝¹ : OrderedAddCommMonoid β
inst✝ : SMul 𝕜 β
f : α ≃o β
hf : ConcaveOn 𝕜 univ ⇑f
x : β
x✝¹ : x ∈ univ
y : β
x✝ : y ∈ univ
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
x' : α
hx'' : x = f x'
⊢ f.symm (a • x + b • y) ≤ a • f.symm x + b • f.symm y

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

Result:
case intro.intro
𝕜 : Type u_1
α : Type u_4
β : Type u_5
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : OrderedAddCommMonoid α
inst✝² : SMul 𝕜 α
inst✝¹ : OrderedAddCommMonoid β
inst✝ : SMul 𝕜 β
f : α ≃o β
hf : ConcaveOn 𝕜 univ ⇑f
x : β
x✝¹ : x ∈ univ
y : β
x✝ : y ∈ univ
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
x' : α
hx'' : x = f x'
y' : α
hy'' : y = f y'
⊢ f.symm (a • x + b • y) ≤ a • f.symm x + b • f.symm y

Proof state:
case intro.intro
𝕜 : Type u_1
α : Type u_4
β : Type u_5
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : OrderedAddCommMonoid α
inst✝² : SMul 𝕜 α
inst✝¹ : OrderedAddCommMonoid β
inst✝ : SMul 𝕜 β
f : α ≃o β
hf : ConcaveOn 𝕜 univ ⇑f
x : β
x✝¹ : x ∈ univ
y : β
x✝ : y ∈ univ
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
x' : α
hx'' : x = f x'
y' : α
hy'' : y = f y'
⊢ f.symm (a • x + b • y) ≤ a • f.symm x + b • f.symm y

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

Result:
case intro.intro
𝕜 : Type u_1
α : Type u_4
β : Type u_5
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : OrderedAddCommMonoid α
inst✝² : SMul 𝕜 α
inst✝¹ : OrderedAddCommMonoid β
inst✝ : SMul 𝕜 β
f : α ≃o β
hf : ConcaveOn 𝕜 univ ⇑f
x : β
x✝¹ : x ∈ univ
y : β
x✝ : y ∈ univ
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
x' : α
hx'' : x = f x'
y' : α
hy'' : y = f y'
⊢ f.symm (a • f x' + b • f y') ≤ a • x' + b • y'

Proof state:
case intro.intro
𝕜 : Type u_1
α : Type u_4
β : Type u_5
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : OrderedAddCommMonoid α
inst✝² : SMul 𝕜 α
inst✝¹ : OrderedAddCommMonoid β
inst✝ : SMul 𝕜 β
f : α ≃o β
hf : ConcaveOn 𝕜 univ ⇑f
x : β
x✝¹ : x ∈ univ
y : β
x✝ : y ∈ univ
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
x' : α
hx'' : x = f x'
y' : α
hy'' : y = f y'
⊢ f.symm (a • f x' + b • f y') ≤ a • x' + b • y'

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

Result:
case intro.intro
𝕜 : Type u_1
α : Type u_4
β : Type u_5
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : OrderedAddCommMonoid α
inst✝² : SMul 𝕜 α
inst✝¹ : OrderedAddCommMonoid β
inst✝ : SMul 𝕜 β
f : α ≃o β
hf : ConcaveOn 𝕜 univ ⇑f
x : β
x✝¹ : x ∈ univ
y : β
x✝ : y ∈ univ
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
x' : α
hx'' : x = f x'
y' : α
hy'' : y = f y'
⊢ a • f x' + b • f y' ≤ f (a • x' + b • y')

Proof state:
𝕜 : Type u_1
α : Type u_4
β : Type u_5
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : OrderedAddCommMonoid α
inst✝² : SMul 𝕜 α
inst✝¹ : OrderedAddCommMonoid β
inst✝ : SMul 𝕜 β
f : α ≃o β
hf : ConcaveOn 𝕜 univ ⇑f
x : β
x✝¹ : x ∈ univ
y : β
x✝ : y ∈ univ
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
x' : α
hx'' : x = f x'
y' : α
hy'' : y = f y'
⊢ y' ∈ univ

Tactic:
simp

Result:
no goals