awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Convex.Function (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
β : Type u_5
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : AddCommGroup E
inst_3 : AddCommGroup F
inst_4 : AddCommMonoid β
inst_5 : PartialOrder β
inst_6 : Module 𝕜 E
inst_7 : Module 𝕜 F
inst_8 : SMul 𝕜 β
f : F → β
g : E →ᵃ[𝕜] F
s : Set F
hf : ConvexOn 𝕜 s f
x : E
hx : Membership.mem (γ := Set E) ((⇑g : (a : E) → F) ⁻¹' s) x
y : E
hy : Membership.mem (γ := Set E) ((⇑g : (a : E) → F) ⁻¹' s) y
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ f ((g : (a : E) → F) (a • x + b • y)) =
    f (HSMul.hSMul (β := F) a ((g : (a : E) → F) x : F) + HSMul.hSMul (β := F) b ((g : (a : E) → F) y : F))
have rw : f (HSMul.hSMul (β := F) a ((g : (a : E) → F) x : F) + HSMul.hSMul (β := F) b ((g : (a : E) → F) y : F)) =
  f (HSMul.hSMul (β := F) a ((g : (a : E) → F) x : F) + HSMul.hSMul (β := F) b ((g : (a : E) → F) y : F))
Tactic: rw [Convex.combo_affine_apply hab]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Function (goal)
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
⊢ f ((a / (a + b)) • x + (b / (a + b)) • y) ≤ (a / (a + b)) • f x + (b / (a + b)) • f y
have apply : a / (a + b) + b / (a + b) = 1
Tactic: apply h hx hy (div_nonneg ha hab.le) (div_nonneg hb hab.le)
-- Lean 4 proof step from Mathlib.Analysis.Convex.Function (goal)
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
⊢ a / (a + b) + b / (a + b) = 1
have rw : (a + b) / (a + b) = 1
Tactic: rw [← add_div, div_self hab.ne']
-- Lean 4 proof step from Mathlib.Analysis.Convex.Function (goal)
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
⊢ a / (a + b) + b / (a + b) = 1
have rw₁ : Eq.{u_1 + 1} (α := 𝕜) 1 1
Tactic: rw [← add_div, div_self hab.ne']
-- Lean 4 proof step from Mathlib.Analysis.Convex.Function (hypothesis)
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
⊢ f ((a / (a + b)) • x + (b / (a + b)) • y) < (a / (a + b)) • f x + (b / (a + b)) • f y
have hab : 0 < a + b
Tactic: have hab := add_pos ha hb
-- Lean 4 proof step from Mathlib.Analysis.Convex.Function (goal)
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
⊢ f ((a / (a + b)) • x + (b / (a + b)) • y) < (a / (a + b)) • f x + (b / (a + b)) • f y
have apply : a / (a + b) + b / (a + b) = 1
Tactic: apply h hx hy hxy (div_pos ha hab) (div_pos hb hab)
-- Lean 4 proof step from Mathlib.Analysis.Convex.Function (goal)
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
⊢ a / (a + b) + b / (a + b) = 1
have rw : (a + b) / (a + b) = 1
Tactic: rw [← add_div, div_self hab.ne']
-- Lean 4 proof step from Mathlib.Analysis.Convex.Function (goal)
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
⊢ a / (a + b) + b / (a + b) = 1
have rw₁ : Eq.{u_1 + 1} (α := 𝕜) 1 1
Tactic: rw [← add_div, div_self hab.ne']
-- Lean 4 proof step from Mathlib.Analysis.Convex.Function (goal)
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 : β) → α)
have 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 : α)
Tactic: refine ⟨convex_univ, fun x _ y _ hxy a b ha hb hab => ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Convex.Function (goal)
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
⊢ (f.symm : (a : β) → α) (a • x + b • y) <
    HSMul.hSMul (β := α) a ((f.symm : (a : β) → α) x : α) + HSMul.hSMul (β := α) b ((f.symm : (a : β) → α) y : α)
have 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 : α)
Tactic: obtain ⟨x', hx''⟩ := f.surjective.exists.mp ⟨x, rfl⟩
-- Lean 4 proof step from Mathlib.Analysis.Convex.Function (goal)
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'
⊢ (f.symm : (a : β) → α) (a • x + b • y) <
    HSMul.hSMul (β := α) a ((f.symm : (a : β) → α) x : α) + HSMul.hSMul (β := α) b ((f.symm : (a : β) → α) y : α)
have 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 : α)
Tactic: obtain ⟨y', hy''⟩ := f.surjective.exists.mp ⟨y, rfl⟩
-- Lean 4 proof step from Mathlib.Analysis.Convex.Function (hypothesis)
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'
⊢ (f.symm : (a : β) → α) (a • x + b • y) <
    HSMul.hSMul (β := α) a ((f.symm : (a : β) → α) x : α) + HSMul.hSMul (β := α) b ((f.symm : (a : β) → α) y : α)
have hxy' : x' ≠ y'
Tactic: have hxy' : x' ≠ y' := by rw [← f.injective.ne_iff, ← hx'', ← hy'']; exact hxy
-- Lean 4 proof step from Mathlib.Analysis.Convex.Function (goal)
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'
⊢ (f.symm : (a : β) → α) (a • x + b • y) <
    HSMul.hSMul (β := α) a ((f.symm : (a : β) → α) x : α) + HSMul.hSMul (β := α) b ((f.symm : (a : β) → α) y : α)
have simp : (f.symm : (a : β) → α)
    (HSMul.hSMul (β := β) a ((f : (a : α) → β) x' : β) + HSMul.hSMul (β := β) b ((f : (a : α) → β) y' : β)) <
  a • x' + b • y'
Tactic: simp only [hx'', hy'', OrderIso.symm_apply_apply, gt_iff_lt]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Function (goal)
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'
⊢ (f.symm : (a : β) → α)
      (HSMul.hSMul (β := β) a ((f : (a : α) → β) x' : β) + HSMul.hSMul (β := β) b ((f : (a : α) → β) y' : β)) <
    a • x' + b • y'
have rw : HSMul.hSMul (β := β) a ((f : (a : α) → β) x' : β) + HSMul.hSMul (β := β) b ((f : (a : α) → β) y' : β) <
  (f : (a : α) → β) (a • x' + b • y')
Tactic: rw [← f.lt_iff_lt, OrderIso.apply_symm_apply]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Function (goal)
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 : β) → α)
have 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 : α)
Tactic: refine ⟨convex_univ, fun x _ y _ a b ha hb hab => ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Convex.Function (goal)
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
⊢ (f.symm : (a : β) → α) (a • x + b • y) ≤
    HSMul.hSMul (β := α) a ((f.symm : (a : β) → α) x : α) + HSMul.hSMul (β := α) b ((f.symm : (a : β) → α) y : α)
have 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 : α)
Tactic: obtain ⟨x', hx''⟩ := f.surjective.exists.mp ⟨x, rfl⟩
-- Lean 4 proof step from Mathlib.Analysis.Convex.Function (goal)
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'
⊢ (f.symm : (a : β) → α) (a • x + b • y) ≤
    HSMul.hSMul (β := α) a ((f.symm : (a : β) → α) x : α) + HSMul.hSMul (β := α) b ((f.symm : (a : β) → α) y : α)
have 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 : α)
Tactic: obtain ⟨y', hy''⟩ := f.surjective.exists.mp ⟨y, rfl⟩
-- Lean 4 proof step from Mathlib.Analysis.Convex.Function (goal)
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'
⊢ (f.symm : (a : β) → α) (a • x + b • y) ≤
    HSMul.hSMul (β := α) a ((f.symm : (a : β) → α) x : α) + HSMul.hSMul (β := α) b ((f.symm : (a : β) → α) y : α)
have simp : (f.symm : (a : β) → α)
    (HSMul.hSMul (β := β) a ((f : (a : α) → β) x' : β) + HSMul.hSMul (β := β) b ((f : (a : α) → β) y' : β)) ≤
  a • x' + b • y'
Tactic: simp only [hx'', hy'', OrderIso.symm_apply_apply]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Function (goal)
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'
⊢ (f.symm : (a : β) → α)
      (HSMul.hSMul (β := β) a ((f : (a : α) → β) x' : β) + HSMul.hSMul (β := β) b ((f : (a : α) → β) y' : β)) ≤
    a • x' + b • y'
have rw : HSMul.hSMul (β := β) a ((f : (a : α) → β) x' : β) + HSMul.hSMul (β := β) b ((f : (a : α) → β) y' : β) ≤
  (f : (a : α) → β) (a • x' + b • y')
Tactic: rw [← f.le_iff_le, OrderIso.apply_symm_apply]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Function (goal)
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 : β) → α)
have 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)
Tactic: refine ⟨convex_univ, fun x _ y _ hxy a b ha hb hab => ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Convex.Function (goal)
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
⊢ HSMul.hSMul (β := α) a ((f.symm : (a : β) → α) x : α) + HSMul.hSMul (β := α) b ((f.symm : (a : β) → α) y : α) <
    (f.symm : (a : β) → α) (a • x + b • y)
have 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)
Tactic: obtain ⟨x', hx''⟩ := f.surjective.exists.mp ⟨x, rfl⟩
-- Lean 4 proof step from Mathlib.Analysis.Convex.Function (goal)
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'
⊢ HSMul.hSMul (β := α) a ((f.symm : (a : β) → α) x : α) + HSMul.hSMul (β := α) b ((f.symm : (a : β) → α) y : α) <
    (f.symm : (a : β) → α) (a • x + b • y)
have 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)
Tactic: obtain ⟨y', hy''⟩ := f.surjective.exists.mp ⟨y, rfl⟩
-- Lean 4 proof step from Mathlib.Analysis.Convex.Function (hypothesis)
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'
⊢ HSMul.hSMul (β := α) a ((f.symm : (a : β) → α) x : α) + HSMul.hSMul (β := α) b ((f.symm : (a : β) → α) y : α) <
    (f.symm : (a : β) → α) (a • x + b • y)
have hxy' : x' ≠ y'
Tactic: have hxy' : x' ≠ y' := by rw [← f.injective.ne_iff, ← hx'', ← hy'']; exact hxy
-- Lean 4 proof step from Mathlib.Analysis.Convex.Function (goal)
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'
⊢ HSMul.hSMul (β := α) a ((f.symm : (a : β) → α) x : α) + HSMul.hSMul (β := α) b ((f.symm : (a : β) → α) y : α) <
    (f.symm : (a : β) → α) (a • x + b • y)
have simp : a • x' + b • y' <
  (f.symm : (a : β) → α)
    (HSMul.hSMul (β := β) a ((f : (a : α) → β) x' : β) + HSMul.hSMul (β := β) b ((f : (a : α) → β) y' : β))
Tactic: simp only [hx'', hy'', OrderIso.symm_apply_apply, gt_iff_lt]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Function (goal)
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'
⊢ a • x' + b • y' <
    (f.symm : (a : β) → α)
      (HSMul.hSMul (β := β) a ((f : (a : α) → β) x' : β) + HSMul.hSMul (β := β) b ((f : (a : α) → β) y' : β))
have rw : (f : (a : α) → β) (a • x' + b • y') <
  HSMul.hSMul (β := β) a ((f : (a : α) → β) x' : β) + HSMul.hSMul (β := β) b ((f : (a : α) → β) y' : β)
Tactic: rw [← f.lt_iff_lt, OrderIso.apply_symm_apply]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Function (goal)
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 : β) → α)
have 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)
Tactic: refine ⟨convex_univ, fun x _ y _ a b ha hb hab => ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Convex.Function (goal)
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
⊢ HSMul.hSMul (β := α) a ((f.symm : (a : β) → α) x : α) + HSMul.hSMul (β := α) b ((f.symm : (a : β) → α) y : α) ≤
    (f.symm : (a : β) → α) (a • x + b • y)
have 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)
Tactic: obtain ⟨x', hx''⟩ := f.surjective.exists.mp ⟨x, rfl⟩