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
β : Type u_5
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : AddCommMonoid β
inst_4 : PartialOrder β
inst_5 : Module 𝕜 E
inst_6 : Module 𝕜 β
inst_7 : LinearOrder E
s : Set E
f : E → β
hs : Convex 𝕜 s
hf :
  ∀ ⦃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 : a + b = 1
this :
  ∀ {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [inst : Semiring 𝕜] [inst_8 : PartialOrder 𝕜]
    [inst_9 : AddCommMonoid E] [inst_10 : AddCommMonoid β] [inst_11 : PartialOrder β] [inst_12 : Module 𝕜 E]
    [inst_13 : Module 𝕜 β] [inst_14 : LinearOrder E] {s : Set E} {f : E → β} (hs : Convex 𝕜 s)
    (hf :
      ∀ ⦃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 : a + b = 1)
    (h : x < y), f (a • x + b • y) ≤ a • f x + b • f y
h : ¬x < y
⊢ f (a • x + b • y) ≤ a • f x + b • f y
have inr : f (b • y + a • x) ≤ b • f y + a • f x
Tactic: rw [add_comm (a • x), add_comm (a • f x)]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Function (hypothesis)
Goal:
𝕜 : Type u_1
E : Type u_2
β : Type u_5
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : AddCommMonoid β
inst_4 : PartialOrder β
inst_5 : Module 𝕜 E
inst_6 : Module 𝕜 β
inst_7 : LinearOrder E
s : Set E
f : E → β
hs : Convex 𝕜 s
hf :
  ∀ ⦃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 : a + b = 1
this :
  ∀ {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [inst : Semiring 𝕜] [inst_8 : PartialOrder 𝕜]
    [inst_9 : AddCommMonoid E] [inst_10 : AddCommMonoid β] [inst_11 : PartialOrder β] [inst_12 : Module 𝕜 E]
    [inst_13 : Module 𝕜 β] [inst_14 : LinearOrder E] {s : Set E} {f : E → β} (hs : Convex 𝕜 s)
    (hf :
      ∀ ⦃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 : a + b = 1)
    (h : x < y), f (a • x + b • y) ≤ a • f x + b • f y
h : ¬x < y
⊢ f (b • y + a • x) ≤ b • f y + a • f x
have hab₁ : b + a = 1
Tactic: rw [add_comm] at hab
Cleared hypotheses: hab, this, h
-- Lean 4 proof step from Mathlib.Analysis.Convex.Function (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
β : Type u_5
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : AddCommMonoid β
inst_4 : PartialOrder β
inst_5 : Module 𝕜 E
inst_6 : Module 𝕜 β
inst_7 : LinearOrder E
s : Set E
f : E → β
hs : Convex 𝕜 s
hf :
  ∀ ⦃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
⊢ StrictConvexOn 𝕜 s f
have refine : ∀ (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: refine ⟨hs, fun x hx y hy hxy a b ha hb hab => ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Convex.Function (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
β : Type u_5
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : AddCommMonoid β
inst_4 : PartialOrder β
inst_5 : Module 𝕜 E
inst_6 : Module 𝕜 β
inst_7 : LinearOrder E
s : Set E
f : E → β
hs : Convex 𝕜 s
hf :
  ∀ ⦃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 : a + b = 1
⊢ f (a • x + b • y) < a • f x + b • f y
have inr : ∀
  (this :
    ∀ {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [inst : Semiring 𝕜] [inst_8 : PartialOrder 𝕜]
      [inst_9 : AddCommMonoid E] [inst_10 : AddCommMonoid β] [inst_11 : PartialOrder β] [inst_12 : Module 𝕜 E]
      [inst_13 : Module 𝕜 β] [inst_14 : LinearOrder E] {s : Set E} {f : E → β} (hs : Convex 𝕜 s)
      (hf :
        ∀ ⦃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 : a + b = 1)
      (h : x < y), f (a • x + b • y) < a • f x + b • f y)
  (h : ¬x < y), f (a • x + b • y) < a • f x + b • f y
Tactic: wlog h : x < y
-- Lean 4 proof step from Mathlib.Analysis.Convex.Function (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
β : Type u_5
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : AddCommMonoid β
inst_4 : PartialOrder β
inst_5 : Module 𝕜 E
inst_6 : Module 𝕜 β
inst_7 : LinearOrder E
s : Set E
f : E → β
hs : Convex 𝕜 s
hf :
  ∀ ⦃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 : a + b = 1
inr :
  ∀
    (this :
      ∀ {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [inst : Semiring 𝕜] [inst_8 : PartialOrder 𝕜]
        [inst_9 : AddCommMonoid E] [inst_10 : AddCommMonoid β] [inst_11 : PartialOrder β] [inst_12 : Module 𝕜 E]
        [inst_13 : Module 𝕜 β] [inst_14 : LinearOrder E] {s : Set E} {f : E → β} (hs : Convex 𝕜 s)
        (hf :
          ∀ ⦃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 : a + b = 1)
        (h : x < y), f (a • x + b • y) < a • f x + b • f y)
    (h : ¬x < y), f (a • x + b • y) < a • f x + b • f y
⊢ f (a • x + b • y) < a • f x + b • f y
have wlog : ∀ {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [inst : Semiring 𝕜] [inst_8 : PartialOrder 𝕜] [inst_9 : AddCommMonoid E]
  [inst_10 : AddCommMonoid β] [inst_11 : PartialOrder β] [inst_12 : Module 𝕜 E] [inst_13 : Module 𝕜 β]
  [inst_14 : LinearOrder E] {s : Set E} {f : E → β} (hs : Convex 𝕜 s)
  (hf :
    ∀ ⦃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 : a + b = 1)
  (h : x < y), f (a • x + b • y) < a • f x + b • f y
Tactic: wlog h : x < y
Cleared hypotheses: hs, hf, x, hx, y, hy, hxy, a, b, ha, hb, hab
-- Lean 4 proof step from Mathlib.Analysis.Convex.Function (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
β : Type u_5
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : AddCommMonoid β
inst_4 : PartialOrder β
inst_5 : Module 𝕜 E
inst_6 : Module 𝕜 β
inst_7 : LinearOrder E
s : Set E
f : E → β
hs : Convex 𝕜 s
hf :
  ∀ ⦃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 : a + b = 1
this :
  ∀ {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [inst : Semiring 𝕜] [inst_8 : PartialOrder 𝕜]
    [inst_9 : AddCommMonoid E] [inst_10 : AddCommMonoid β] [inst_11 : PartialOrder β] [inst_12 : Module 𝕜 E]
    [inst_13 : Module 𝕜 β] [inst_14 : LinearOrder E] {s : Set E} {f : E → β} (hs : Convex 𝕜 s)
    (hf :
      ∀ ⦃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 : a + b = 1)
    (h : x < y), f (a • x + b • y) < a • f x + b • f y
h : ¬x < y
⊢ f (a • x + b • y) < a • f x + b • f y
have inr : f (b • y + a • x) < b • f y + a • f x
Tactic: rw [add_comm (a • x), add_comm (a • f x)]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Function (hypothesis)
Goal:
𝕜 : Type u_1
E : Type u_2
β : Type u_5
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : AddCommMonoid β
inst_4 : PartialOrder β
inst_5 : Module 𝕜 E
inst_6 : Module 𝕜 β
inst_7 : LinearOrder E
s : Set E
f : E → β
hs : Convex 𝕜 s
hf :
  ∀ ⦃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 : a + b = 1
this :
  ∀ {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [inst : Semiring 𝕜] [inst_8 : PartialOrder 𝕜]
    [inst_9 : AddCommMonoid E] [inst_10 : AddCommMonoid β] [inst_11 : PartialOrder β] [inst_12 : Module 𝕜 E]
    [inst_13 : Module 𝕜 β] [inst_14 : LinearOrder E] {s : Set E} {f : E → β} (hs : Convex 𝕜 s)
    (hf :
      ∀ ⦃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 : a + b = 1)
    (h : x < y), f (a • x + b • y) < a • f x + b • f y
h : ¬x < y
⊢ f (b • y + a • x) < b • f y + a • f x
have hab₁ : b + a = 1
Tactic: rw [add_comm] at hab
Cleared hypotheses: hab, this, h
-- 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 : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : AddCommMonoid F
inst_4 : AddCommMonoid β
inst_5 : PartialOrder β
inst_6 : Module 𝕜 E
inst_7 : Module 𝕜 F
inst_8 : SMul 𝕜 β
f : F → β
s : Set F
hf : ConvexOn 𝕜 s f
g : E →ₗ[𝕜] 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 (HAdd.hAdd (α := F) (β := F) ((g : (a : E) → F) (a • x) : F) ((g : (a : E) → F) (b • 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 [g.map_add, g.map_smul, g.map_smul]
-- 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 : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : AddCommMonoid F
inst_4 : AddCommMonoid β
inst_5 : PartialOrder β
inst_6 : Module 𝕜 E
inst_7 : Module 𝕜 F
inst_8 : SMul 𝕜 β
f : F → β
s : Set F
hf : ConvexOn 𝕜 s f
g : E →ₗ[𝕜] 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
rw :
  f (HAdd.hAdd (α := F) (β := F) ((g : (a : E) → F) (a • x) : F) ((g : (a : E) → F) (b • y) : F)) =
    f (HSMul.hSMul (β := F) a ((g : (a : E) → F) x : F) + HSMul.hSMul (β := F) b ((g : (a : E) → F) y : F))
⊢ 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 (HAdd.hAdd (β := F) (HSMul.hSMul (β := F) a ((g : (a : E) → F) x : F)) ((g : (a : E) → F) (b • 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 [g.map_add, g.map_smul, g.map_smul]
-- 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 : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : AddCommMonoid F
inst_4 : AddCommMonoid β
inst_5 : PartialOrder β
inst_6 : Module 𝕜 E
inst_7 : Module 𝕜 F
inst_8 : SMul 𝕜 β
f : F → β
s : Set F
hf : ConvexOn 𝕜 s f
g : E →ₗ[𝕜] 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
rw :
  f (HAdd.hAdd (α := F) (β := F) ((g : (a : E) → F) (a • x) : F) ((g : (a : E) → F) (b • y) : F)) =
    f (HSMul.hSMul (β := F) a ((g : (a : E) → F) x : F) + HSMul.hSMul (β := F) b ((g : (a : E) → F) y : F))
rw₁ :
  f (HAdd.hAdd (β := F) (HSMul.hSMul (β := F) a ((g : (a : E) → F) x : F)) ((g : (a : E) → F) (b • y) : F)) =
    f (HSMul.hSMul (β := F) a ((g : (a : E) → F) x : F) + HSMul.hSMul (β := F) b ((g : (a : E) → F) y : F))
⊢ 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 [g.map_add, g.map_smul, g.map_smul]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Function (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
β : Type u_5
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : AddCommMonoid β
inst_4 : PartialOrder β
inst_5 : IsOrderedCancelAddMonoid β
inst_6 : SMul 𝕜 E
inst_7 : DistribMulAction 𝕜 β
s : Set E
f g : E → β
hf : StrictConvexOn 𝕜 s f
hg : ConvexOn 𝕜 s g
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
⊢ a • f x + b • f y + (a • g x + b • g y) = a • (f x + g x) + b • (f y + g y)
have rw : a • f x + b • f y + (a • g x + b • g y) = a • f x + a • g x + b • (f y + g y)
Tactic: rw [smul_add, smul_add, add_add_add_comm]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Function (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
β : Type u_5
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : AddCommMonoid β
inst_4 : PartialOrder β
inst_5 : IsOrderedCancelAddMonoid β
inst_6 : SMul 𝕜 E
inst_7 : DistribMulAction 𝕜 β
s : Set E
f g : E → β
hf : StrictConvexOn 𝕜 s f
hg : ConvexOn 𝕜 s g
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
rw : a • f x + b • f y + (a • g x + b • g y) = a • f x + a • g x + b • (f y + g y)
⊢ a • f x + b • f y + (a • g x + b • g y) = a • (f x + g x) + b • (f y + g y)
have rw₁ : a • f x + b • f y + (a • g x + b • g y) = a • f x + a • g x + (b • f y + b • g y)
Tactic: rw [smul_add, smul_add, add_add_add_comm]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Function (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
β : Type u_5
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : AddCommMonoid β
inst_4 : PartialOrder β
inst_5 : IsOrderedCancelAddMonoid β
inst_6 : SMul 𝕜 E
inst_7 : DistribMulAction 𝕜 β
s : Set E
f g : E → β
hf : StrictConvexOn 𝕜 s f
hg : ConvexOn 𝕜 s g
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
rw : a • f x + b • f y + (a • g x + b • g y) = a • f x + a • g x + b • (f y + g y)
rw₁ : a • f x + b • f y + (a • g x + b • g y) = a • f x + a • g x + (b • f y + b • g y)
⊢ a • f x + b • f y + (a • g x + b • g y) = a • (f x + g x) + b • (f y + g y)
have rw₂ : a • f x + a • g x + (b • f y + b • g y) = a • f x + a • g x + (b • f y + b • g y)
Tactic: rw [smul_add, smul_add, add_add_add_comm]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Function (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
β : Type u_5
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : AddCommMonoid β
inst_4 : PartialOrder β
inst_5 : IsOrderedCancelAddMonoid β
inst_6 : SMul 𝕜 E
inst_7 : DistribMulAction 𝕜 β
s : Set E
f g : E → β
hf : StrictConvexOn 𝕜 s f
hg : StrictConvexOn 𝕜 s g
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
⊢ a • f x + b • f y + (a • g x + b • g y) = a • (f x + g x) + b • (f y + g y)
have rw : a • f x + b • f y + (a • g x + b • g y) = a • f x + a • g x + b • (f y + g y)
Tactic: rw [smul_add, smul_add, add_add_add_comm]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Function (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
β : Type u_5
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : AddCommMonoid β
inst_4 : PartialOrder β
inst_5 : IsOrderedCancelAddMonoid β
inst_6 : SMul 𝕜 E
inst_7 : DistribMulAction 𝕜 β
s : Set E
f g : E → β
hf : StrictConvexOn 𝕜 s f
hg : StrictConvexOn 𝕜 s g
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
rw : a • f x + b • f y + (a • g x + b • g y) = a • f x + a • g x + b • (f y + g y)
⊢ a • f x + b • f y + (a • g x + b • g y) = a • (f x + g x) + b • (f y + g y)
have rw₁ : a • f x + b • f y + (a • g x + b • g y) = a • f x + a • g x + (b • f y + b • g y)
Tactic: rw [smul_add, smul_add, add_add_add_comm]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Function (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
β : Type u_5
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : AddCommMonoid β
inst_4 : PartialOrder β
inst_5 : IsOrderedCancelAddMonoid β
inst_6 : SMul 𝕜 E
inst_7 : DistribMulAction 𝕜 β
s : Set E
f g : E → β
hf : StrictConvexOn 𝕜 s f
hg : StrictConvexOn 𝕜 s g
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
rw : a • f x + b • f y + (a • g x + b • g y) = a • f x + a • g x + b • (f y + g y)
rw₁ : a • f x + b • f y + (a • g x + b • g y) = a • f x + a • g x + (b • f y + b • g y)
⊢ a • f x + b • f y + (a • g x + b • g y) = a • (f x + g x) + b • (f y + g y)
have rw₂ : a • f x + a • g x + (b • f y + b • g y) = a • f x + a • g x + (b • f y + b • g y)
Tactic: rw [smul_add, smul_add, add_add_add_comm]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Function (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
β : Type u_5
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : AddCommMonoid β
inst_4 : PartialOrder β
inst_5 : IsOrderedCancelAddMonoid β
inst_6 : Module 𝕜 E
inst_7 : Module 𝕜 β
inst_8 : PosSMulStrictMono 𝕜 β
s : Set E
f : E → β
hf : ConvexOn 𝕜 s f
p q : E × β
hp : p.1 ∈ s ∧ f p.1 < p.2
hq : q.1 ∈ s ∧ f q.1 ≤ q.2
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ Membership.mem (γ := Set (E × β)) {p : E × β | p.1 ∈ s ∧ f p.1 < p.2} (a • p + b • q)
have refine : f (a • p + b • q).1 < (a • p + b • q).2
Tactic: refine ⟨hf.1 hp.1 hq.1 ha.le hb.le hab, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Convex.Function (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
β : Type u_5
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : AddCommMonoid β
inst_4 : LinearOrder β
inst_5 : IsOrderedAddMonoid β
inst_6 : SMul 𝕜 E
inst_7 : Module 𝕜 β
inst_8 : PosSMulStrictMono 𝕜 β
s : Set E
f g : E → β
hf : ConvexOn 𝕜 s f
hg : ConvexOn 𝕜 s g
⊢ ConvexOn 𝕜 s (f ⊔ g)
have refine_1 : ∀ (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 ⊔ g) x + b • (f ⊔ g) y
Tactic: refine ⟨hf.left, fun x hx y hy a b ha hb hab => sup_le ?_ ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Convex.Function (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
β : Type u_5
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : AddCommMonoid β
inst_4 : LinearOrder β
inst_5 : IsOrderedAddMonoid β
inst_6 : SMul 𝕜 E
inst_7 : Module 𝕜 β
inst_8 : PosSMulStrictMono 𝕜 β
s : Set E
f g : E → β
hf : ConvexOn 𝕜 s f
hg : ConvexOn 𝕜 s g
refine_1 :
  ∀ (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 ⊔ g) x + b • (f ⊔ g) y
⊢ ConvexOn 𝕜 s (f ⊔ g)
have refine_2 : ∀ (x : E) (hx : x ∈ s) (y : E) (hy : y ∈ s) (a b : 𝕜) (ha : 0 ≤ a) (hb : 0 ≤ b) (hab : a + b = 1),
  g (a • x + b • y) ≤ a • (f ⊔ g) x + b • (f ⊔ g) y
Tactic: refine ⟨hf.left, fun x hx y hy a b ha hb hab => sup_le ?_ ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Convex.Function (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
β : Type u_5
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : AddCommMonoid β
inst_4 : LinearOrder β
inst_5 : IsOrderedAddMonoid β
inst_6 : SMul 𝕜 E
inst_7 : Module 𝕜 β
inst_8 : PosSMulStrictMono 𝕜 β
s : Set E
f g : E → β
hf : ConvexOn 𝕜 s f
hg : ConvexOn 𝕜 s g
x : E
hx : x ∈ s
y : E
hy : y ∈ s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ a • f x + b • f y ≤ a • max (f x) (g x) + b • max (f y) (g y)
have h₁ : f x ≤ max (f x) (g x)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.Convex.Function (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
β : Type u_5
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : AddCommMonoid β
inst_4 : LinearOrder β
inst_5 : IsOrderedAddMonoid β
inst_6 : SMul 𝕜 E
inst_7 : Module 𝕜 β
inst_8 : PosSMulStrictMono 𝕜 β
s : Set E
f g : E → β
hf : ConvexOn 𝕜 s f
hg : ConvexOn 𝕜 s g
x : E
hx : x ∈ s
y : E
hy : y ∈ s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
h₁ : f x ≤ max (f x) (g x)
⊢ a • f x + b • f y ≤ a • max (f x) (g x) + b • max (f y) (g y)
have h₂ : f y ≤ max (f y) (g y)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.Convex.Function (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
β : Type u_5
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : AddCommMonoid β
inst_4 : LinearOrder β
inst_5 : IsOrderedAddMonoid β
inst_6 : SMul 𝕜 E
inst_7 : Module 𝕜 β
inst_8 : PosSMulStrictMono 𝕜 β
s : Set E
f g : E → β
hf : ConvexOn 𝕜 s f
hg : ConvexOn 𝕜 s g
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 ⊔ g) x + b • (f ⊔ g) y
have f₁ : a • f x + b • f y ≤ a • max (f x) (g x) + b • max (f y) (g y)
Tactic: calc
      f (a • x + b • y) ≤ a • f x + b • f y := hf.right hx hy ha hb hab
      _ ≤ a • (f x ⊔ g x) + b • (f y ⊔ g y) := by gcongr <;> apply le_sup_left
-- Lean 4 proof step from Mathlib.Analysis.Convex.Function (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
β : Type u_5
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : AddCommMonoid β
inst_4 : LinearOrder β
inst_5 : IsOrderedAddMonoid β
inst_6 : SMul 𝕜 E
inst_7 : Module 𝕜 β
inst_8 : PosSMulStrictMono 𝕜 β
s : Set E
f g : E → β
hf : ConvexOn 𝕜 s f
hg : ConvexOn 𝕜 s g
x : E
hx : x ∈ s
y : E
hy : y ∈ s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ a • g x + b • g y ≤ a • max (f x) (g x) + b • max (f y) (g y)
have h₁ : g x ≤ max (f x) (g x)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.Convex.Function (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
β : Type u_5
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : AddCommMonoid β
inst_4 : LinearOrder β
inst_5 : IsOrderedAddMonoid β
inst_6 : SMul 𝕜 E
inst_7 : Module 𝕜 β
inst_8 : PosSMulStrictMono 𝕜 β
s : Set E
f g : E → β
hf : ConvexOn 𝕜 s f
hg : ConvexOn 𝕜 s g
x : E
hx : x ∈ s
y : E
hy : y ∈ s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
h₁ : g x ≤ max (f x) (g x)
⊢ a • g x + b • g y ≤ a • max (f x) (g x) + b • max (f y) (g y)
have h₂ : g y ≤ max (f y) (g y)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.Convex.Function (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
β : Type u_5
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : AddCommMonoid β
inst_4 : LinearOrder β
inst_5 : IsOrderedAddMonoid β
inst_6 : SMul 𝕜 E
inst_7 : Module 𝕜 β
inst_8 : PosSMulStrictMono 𝕜 β
s : Set E
f g : E → β
hf : ConvexOn 𝕜 s f
hg : ConvexOn 𝕜 s g
x : E
hx : x ∈ s
y : E
hy : y ∈ s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ g (a • x + b • y) ≤ a • (f ⊔ g) x + b • (f ⊔ g) y
have g₁ : a • g x + b • g y ≤ a • max (f x) (g x) + b • max (f y) (g y)
Tactic: calc
      g (a • x + b • y) ≤ a • g x + b • g y := hg.right hx hy ha hb hab
      _ ≤ a • (f x ⊔ g x) + b • (f y ⊔ g y) := by gcongr <;> apply le_sup_right
-- Lean 4 proof step from Mathlib.Analysis.Convex.Function (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
β : Type u_5
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : AddCommMonoid β
inst_4 : LinearOrder β
inst_5 : IsOrderedAddMonoid β
inst_6 : SMul 𝕜 E
inst_7 : Module 𝕜 β
inst_8 : PosSMulStrictMono 𝕜 β
s : Set E
f g : E → β
hf : StrictConvexOn 𝕜 s f
hg : StrictConvexOn 𝕜 s g
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
⊢ a • f x + b • f y ≤ a • max (f x) (g x) + b • max (f y) (g y)
have h₁ : f x ≤ max (f x) (g x)
Tactic: gcongr