awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Convex.Extreme (hypothesis)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
L : Type u_6
inst : Ring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : IsOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
inst_5 : AddCommGroup F
inst_6 : Module 𝕜 F
inst_7 : EquivLike L E F
inst_8 : LinearEquivClass L 𝕜 E F
f : L
s : Set E
a : E
⊢ Membership.mem.{u_3, u_3} (α := F) (γ := Set F) ((⇑f : (a : E) → F) '' extremePoints 𝕜 s) ((f : (a : E) → F) a : F) ↔
    Membership.mem.{u_3, u_3} (α := F) (γ := Set F) (extremePoints 𝕜 ((⇑f : (a : E) → F) '' s))
      ((f : (a : E) → F) a : F)
have this : ∀ (x y : E),
  Eq.{u_3 + 1} (α := Set F) ((⇑f : (a : E) → F) '' openSegment 𝕜 x y : Set F)
    (openSegment 𝕜 ((f : (a : E) → F) x) ((f : (a : E) → F) y) : Set F)
Tactic: have : ∀ x y, f '' openSegment 𝕜 x y = openSegment 𝕜 (f x) (f y) :=
    image_openSegment _ (LinearMapClass.linearMap f).toAffineMap
-- Lean 4 proof step from Mathlib.Analysis.Convex.Extreme (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Ring 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
inst_5 : DenselyOrdered 𝕜
inst_6 : IsTorsionFree 𝕜 E
A : Set E
x : E
⊢ x ∈ extremePoints 𝕜 A ↔ x ∈ A ∧ ∀ x₁ ∈ A, ∀ x₂ ∈ A, x ∈ segment 𝕜 x₁ x₂ → x₁ = x ∨ x₂ = x
have rw : (x ∈ A ∧ ∀ x₁ ∈ A, ∀ x₂ ∈ A, x ∈ openSegment 𝕜 x₁ x₂ → x₁ = x ∧ x₂ = x) ↔
  x ∈ A ∧ ∀ x₁ ∈ A, ∀ x₂ ∈ A, x ∈ segment 𝕜 x₁ x₂ → x₁ = x ∨ x₂ = x
Tactic: rw [mem_extremePoints]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Extreme (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Ring 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
inst_5 : DenselyOrdered 𝕜
inst_6 : IsTorsionFree 𝕜 E
A : Set E
x : E
⊢ (x ∈ A ∧ ∀ x₁ ∈ A, ∀ x₂ ∈ A, x ∈ openSegment 𝕜 x₁ x₂ → x₁ = x ∧ x₂ = x) ↔
    x ∈ A ∧ ∀ x₁ ∈ A, ∀ x₂ ∈ A, x ∈ segment 𝕜 x₁ x₂ → x₁ = x ∨ x₂ = x
have refine : ∀ (hxA : x ∈ A) (x₁ : E) (h₁ : x₁ ∈ A) (x₂ : E) (h₂ : x₂ ∈ A),
  x ∈ openSegment 𝕜 x₁ x₂ → x₁ = x ∧ x₂ = x ↔ x ∈ segment 𝕜 x₁ x₂ → x₁ = x ∨ x₂ = x
Tactic: refine and_congr_right fun hxA ↦ forall₄_congr fun x₁ h₁ x₂ h₂ ↦ ?_
-- Lean 4 proof step from Mathlib.Analysis.Convex.Extreme (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Ring 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
inst_5 : DenselyOrdered 𝕜
inst_6 : IsTorsionFree 𝕜 E
A : Set E
x : E
hxA : x ∈ A
x₁ : E
h₁ : x₁ ∈ A
x₂ : E
h₂ : x₂ ∈ A
⊢ x ∈ openSegment 𝕜 x₁ x₂ → x₁ = x ∧ x₂ = x ↔ x ∈ segment 𝕜 x₁ x₂ → x₁ = x ∨ x₂ = x
have mp : (x ∈ openSegment 𝕜 x₁ x₂ → x₁ = x ∧ x₂ = x) → x ∈ segment 𝕜 x₁ x₂ → x₁ = x ∨ x₂ = x
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.Convex.Extreme (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Ring 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
inst_5 : DenselyOrdered 𝕜
inst_6 : IsTorsionFree 𝕜 E
A : Set E
x : E
hxA : x ∈ A
x₁ : E
h₁ : x₁ ∈ A
x₂ : E
h₂ : x₂ ∈ A
mp : (x ∈ openSegment 𝕜 x₁ x₂ → x₁ = x ∧ x₂ = x) → x ∈ segment 𝕜 x₁ x₂ → x₁ = x ∨ x₂ = x
⊢ x ∈ openSegment 𝕜 x₁ x₂ → x₁ = x ∧ x₂ = x ↔ x ∈ segment 𝕜 x₁ x₂ → x₁ = x ∨ x₂ = x
have mpr : (x ∈ segment 𝕜 x₁ x₂ → x₁ = x ∨ x₂ = x) → x ∈ openSegment 𝕜 x₁ x₂ → x₁ = x ∧ x₂ = x
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.Convex.Extreme (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Ring 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
inst_5 : DenselyOrdered 𝕜
inst_6 : IsTorsionFree 𝕜 E
A : Set E
x : E
hxA : x ∈ A
x₁ : E
h₁ : x₁ ∈ A
x₂ : E
h₂ : x₂ ∈ A
⊢ (x ∈ openSegment 𝕜 x₁ x₂ → x₁ = x ∧ x₂ = x) → x ∈ segment 𝕜 x₁ x₂ → x₁ = x ∨ x₂ = x
have mp : (x ∈ openSegment 𝕜 x₁ x₂ → x₁ = x ∧ x₂ = x) → x ∈ insert x₁ (insert x₂ (openSegment 𝕜 x₁ x₂)) → x₁ = x ∨ x₂ = x
Tactic: rw [← insert_endpoints_openSegment]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Extreme (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Ring 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
inst_5 : DenselyOrdered 𝕜
inst_6 : IsTorsionFree 𝕜 E
A : Set E
x : E
hxA : x ∈ A
x₁ : E
h₁ : x₁ ∈ A
x₂ : E
h₂ : x₂ ∈ A
H : x ∈ segment 𝕜 x₁ x₂ → x₁ = x ∨ x₂ = x
hx : x ∈ openSegment 𝕜 x₁ x₂
⊢ x₁ = x ∧ x₂ = x
have mpr : ∀ (hxA : x₁ ∈ A) (H : x₁ ∈ segment 𝕜 x₁ x₂ → x₁ = x₁ ∨ x₂ = x₁) (hx : x₁ ∈ openSegment 𝕜 x₁ x₂), x₁ = x₁ ∧ x₂ = x₁
Tactic: rcases H (openSegment_subset_segment _ _ _ hx) with (rfl | rfl)
Cleared hypotheses: x, hxA, H, hx
-- Lean 4 proof step from Mathlib.Analysis.Convex.Extreme (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Ring 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
inst_5 : DenselyOrdered 𝕜
inst_6 : IsTorsionFree 𝕜 E
A : Set E
x : E
hxA : x ∈ A
x₁ : E
h₁ : x₁ ∈ A
x₂ : E
h₂ : x₂ ∈ A
H : x ∈ segment 𝕜 x₁ x₂ → x₁ = x ∨ x₂ = x
hx : x ∈ openSegment 𝕜 x₁ x₂
mpr : ∀ (hxA : x₁ ∈ A) (H : x₁ ∈ segment 𝕜 x₁ x₂ → x₁ = x₁ ∨ x₂ = x₁) (hx : x₁ ∈ openSegment 𝕜 x₁ x₂), x₁ = x₁ ∧ x₂ = x₁
⊢ x₁ = x ∧ x₂ = x
have mpr₁ : ∀ (hxA : x₂ ∈ A) (H : x₂ ∈ segment 𝕜 x₁ x₂ → x₁ = x₂ ∨ x₂ = x₂) (hx : x₂ ∈ openSegment 𝕜 x₁ x₂), x₁ = x₂ ∧ x₂ = x₂
Tactic: rcases H (openSegment_subset_segment _ _ _ hx) with (rfl | rfl)
Cleared hypotheses: x, hxA, H, hx
-- Lean 4 proof step from Mathlib.Analysis.Convex.Extreme (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Ring 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
inst_5 : DenselyOrdered 𝕜
inst_6 : IsTorsionFree 𝕜 E
A : Set E
x : E
hA : Convex 𝕜 A
⊢ x ∈ extremePoints 𝕜 A ↔ x ∈ A ∧ Convex 𝕜 (A \ {x})
have mpr : x ∈ A ∧ Convex 𝕜 (A \ {x}) → x ∈ extremePoints 𝕜 A
Tactic: use fun hx ↦ ⟨hx.1, (isExtreme_singleton.2 hx).convex_diff hA⟩
-- Lean 4 proof step from Mathlib.Analysis.Convex.Extreme (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Ring 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
inst_5 : DenselyOrdered 𝕜
inst_6 : IsTorsionFree 𝕜 E
A : Set E
x : E
hA : Convex 𝕜 A
hxA : x ∈ A
hAx : Convex 𝕜 (A \ {x})
⊢ x ∈ extremePoints 𝕜 A
have mpr : ∀ (x₁ : E) (hx₁ : x₁ ∈ A) (x₂ : E) (hx₂ : x₂ ∈ A) (hx : x ∈ [x₁ -[𝕜] x₂]), x₁ = x ∨ x₂ = x
Tactic: refine mem_extremePoints_iff_forall_segment.2 ⟨hxA, fun x₁ hx₁ x₂ hx₂ hx ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Convex.Extreme (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Ring 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
inst_5 : DenselyOrdered 𝕜
inst_6 : IsTorsionFree 𝕜 E
A : Set E
x : E
hA : Convex 𝕜 A
hxA : x ∈ A
hAx : Convex 𝕜 (A \ {x})
x₁ : E
hx₁ : x₁ ∈ A
x₂ : E
hx₂ : x₂ ∈ A
hx : x ∈ [x₁ -[𝕜] x₂]
⊢ x₁ = x ∨ x₂ = x
have mpr : ∀ (hAx : ∀ ⦃x_1 : E⦄, x_1 ∈ A \ {x} → ∀ ⦃y : E⦄, y ∈ A \ {x} → [x_1 -[𝕜] y] ⊆ A \ {x}) (x₁ : E) (hx₁ : x₁ ∈ A) (x₂ : E)
  (hx₂ : x₂ ∈ A) (hx : x ∈ [x₁ -[𝕜] x₂]), x₁ = x ∨ x₂ = x
Tactic: rw [convex_iff_segment_subset] at hAx
Cleared hypotheses: hAx, x₁, hx₁, x₂, hx₂, hx
-- Lean 4 proof step from Mathlib.Analysis.Convex.Extreme (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Ring 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
inst_5 : DenselyOrdered 𝕜
inst_6 : IsTorsionFree 𝕜 E
A : Set E
x : E
hA : Convex 𝕜 A
hxA : x ∈ A
hAx : ∀ ⦃x_1 : E⦄, x_1 ∈ A \ {x} → ∀ ⦃y : E⦄, y ∈ A \ {x} → [x_1 -[𝕜] y] ⊆ A \ {x}
x₁ : E
hx₁ : x₁ ∈ A
x₂ : E
hx₂ : x₂ ∈ A
hx : x ∈ [x₁ -[𝕜] x₂]
⊢ x₁ = x ∨ x₂ = x
have mpr : ∀ (h : x₁ ≠ x ∧ x₂ ≠ x), False
Tactic: by_contra! h
-- Lean 4 proof step from Mathlib.Analysis.Convex.Extreme (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Ring 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
inst_5 : DenselyOrdered 𝕜
inst_6 : IsTorsionFree 𝕜 E
A : Set E
x : E
hA : Convex 𝕜 A
⊢ x ∈ extremePoints 𝕜 A ↔ x ∈ A \ (convexHull 𝕜 : (a : Set E) → Set E) (A \ {x})
have rw : x ∈ A ∧ Convex 𝕜 (A \ {x}) ↔ x ∈ A \ (convexHull 𝕜 : (a : Set E) → Set E) (A \ {x})
Tactic: rw [hA.mem_extremePoints_iff_convex_diff, hA.convex_remove_iff_notMem_convexHull_remove,
    mem_diff]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Extreme (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Ring 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
inst_5 : DenselyOrdered 𝕜
inst_6 : IsTorsionFree 𝕜 E
A : Set E
x : E
hA : Convex 𝕜 A
rw : x ∈ A ∧ Convex 𝕜 (A \ {x}) ↔ x ∈ A \ (convexHull 𝕜 : (a : Set E) → Set E) (A \ {x})
⊢ x ∈ extremePoints 𝕜 A ↔ x ∈ A \ (convexHull 𝕜 : (a : Set E) → Set E) (A \ {x})
have rw₁ : x ∈ A ∧ x ∉ ((convexHull 𝕜 : (a : Set E) → Set E) (A \ {x}) : Set E) ↔
  x ∈ A \ (convexHull 𝕜 : (a : Set E) → Set E) (A \ {x})
Tactic: rw [hA.mem_extremePoints_iff_convex_diff, hA.convex_remove_iff_notMem_convexHull_remove,
    mem_diff]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Extreme (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Ring 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
inst_5 : DenselyOrdered 𝕜
inst_6 : IsTorsionFree 𝕜 E
A : Set E
x : E
hA : Convex 𝕜 A
rw : x ∈ A ∧ Convex 𝕜 (A \ {x}) ↔ x ∈ A \ (convexHull 𝕜 : (a : Set E) → Set E) (A \ {x})
rw₁ :
  x ∈ A ∧ x ∉ ((convexHull 𝕜 : (a : Set E) → Set E) (A \ {x}) : Set E) ↔
    x ∈ A \ (convexHull 𝕜 : (a : Set E) → Set E) (A \ {x})
⊢ x ∈ extremePoints 𝕜 A ↔ x ∈ A \ (convexHull 𝕜 : (a : Set E) → Set E) (A \ {x})
have rw₂ : x ∈ A ∧ x ∉ ((convexHull 𝕜 : (a : Set E) → Set E) (A \ {x}) : Set E) ↔
  x ∈ A ∧ x ∉ ((convexHull 𝕜 : (a : Set E) → Set E) (A \ {x}) : Set E)
Tactic: rw [hA.mem_extremePoints_iff_convex_diff, hA.convex_remove_iff_notMem_convexHull_remove,
    mem_diff]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Extreme (hypothesis)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Ring 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
inst_5 : DenselyOrdered 𝕜
inst_6 : IsTorsionFree 𝕜 E
A : Set E
x : E
hx : Membership.mem (γ := Set E) (extremePoints 𝕜 ((convexHull 𝕜 : (a : Set E) → Set E) A)) x
⊢ x ∈ A
have hx₁ : Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) A : Set E) x ∧
  Convex.{u_1, u_2} 𝕜 (E := E) ((convexHull 𝕜 : (a : Set E) → Set E) A \ {x})
Tactic: rw [(convex_convexHull 𝕜 _).mem_extremePoints_iff_convex_diff] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Analysis.Convex.Extreme (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Ring 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
inst_5 : DenselyOrdered 𝕜
inst_6 : IsTorsionFree 𝕜 E
A : Set E
x : E
hx :
  Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) A : Set E) x ∧
    Convex.{u_1, u_2} 𝕜 (E := E) ((convexHull 𝕜 : (a : Set E) → Set E) A \ {x})
⊢ x ∈ A
have by_contra : ∀ (h : x ∉ A), False
Tactic: by_contra 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 : IsOrderedAddMonoid β
inst_6 : SMul 𝕜 E
inst_7 : DistribMulAction 𝕜 β
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 • 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 : IsOrderedAddMonoid β
inst_6 : SMul 𝕜 E
inst_7 : DistribMulAction 𝕜 β
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
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 : IsOrderedAddMonoid β
inst_6 : SMul 𝕜 E
inst_7 : DistribMulAction 𝕜 β
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
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 : IsOrderedAddMonoid β
inst_6 : SMul 𝕜 E
inst_7 : Module 𝕜 β
inst_8 : PosSMulMono 𝕜 β
s : Set E
f : E → β
hf : ConvexOn 𝕜 s f
r : β
x : E
hx : Membership.mem (γ := Set E) {x : E | x ∈ s ∧ f x ≤ r} x
y : E
hy : Membership.mem (γ := Set E) {x : E | x ∈ s ∧ f x ≤ r} y
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ a • f x + b • f y ≤ a • r + b • r
have h₁ : f x ≤ r
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 : PartialOrder β
inst_5 : IsOrderedAddMonoid β
inst_6 : SMul 𝕜 E
inst_7 : Module 𝕜 β
inst_8 : PosSMulMono 𝕜 β
s : Set E
f : E → β
hf : ConvexOn 𝕜 s f
r : β
x : E
hx : Membership.mem (γ := Set E) {x : E | x ∈ s ∧ f x ≤ r} x
y : E
hy : Membership.mem (γ := Set E) {x : E | x ∈ s ∧ f x ≤ r} y
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
h₁ : f x ≤ r
⊢ a • f x + b • f y ≤ a • r + b • r
have h₂ : f y ≤ r
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 : PartialOrder β
inst_5 : IsOrderedAddMonoid β
inst_6 : SMul 𝕜 E
inst_7 : Module 𝕜 β
inst_8 : PosSMulMono 𝕜 β
s : Set E
f : E → β
hf : ConvexOn 𝕜 s f
x : E
r : β
hx : (x, r).1 ∈ s
hr : f (x, r).1 ≤ (x, r).2
y : E
t : β
hy : (y, t).1 ∈ s
ht : f (y, t).1 ≤ (y, t).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 • (x, r) + b • (y, t))
have refine : f (a • (x, r) + b • (y, t)).1 ≤ (a • (x, r) + b • (y, t)).2
Tactic: refine ⟨hf.1 hx hy 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 : IsOrderedAddMonoid β
inst_6 : SMul 𝕜 E
inst_7 : Module 𝕜 β
inst_8 : PosSMulMono 𝕜 β
s : Set E
f : E → β
hf : ConvexOn 𝕜 s f
x : E
r : β
hx : (x, r).1 ∈ s
hr : f (x, r).1 ≤ (x, r).2
y : E
t : β
hy : (y, t).1 ∈ s
ht : f (y, t).1 ≤ (y, t).2
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ f (a • (x, r) + b • (y, t)).1 ≤ (a • (x, r) + b • (y, t)).2
have f₁ : a • f x + b • f y ≤ a • r + b • t
Tactic: calc
    f (a • x + b • y) ≤ a • f x + b • f y := hf.2 hx hy ha hb hab
    _ ≤ a • r + b • t := by 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 : PartialOrder β
inst_5 : Module 𝕜 E
inst_6 : SMul 𝕜 β
s : Set E
f : E → β
hf : ConvexOn 𝕜 s f
c x : E
hx : Membership.mem (γ := Set E) ((fun (z : E) ↦ c + z) ⁻¹' s) x
y : E
hy : Membership.mem (γ := Set E) ((fun (z : E) ↦ c + z) ⁻¹' s) y
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ f (c + (a • x + b • y)) = f (a • (c + x) + b • (c + y))
have rw : f (c + (a • x + b • y)) = f (a • c + a • x + b • (c + y))
Tactic: rw [smul_add, smul_add, add_add_add_comm, Convex.combo_self 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 : SMul 𝕜 β
s : Set E
f : E → β
hf : ConvexOn 𝕜 s f
c x : E
hx : Membership.mem (γ := Set E) ((fun (z : E) ↦ c + z) ⁻¹' s) x
y : E
hy : Membership.mem (γ := Set E) ((fun (z : E) ↦ c + z) ⁻¹' s) y
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
rw : f (c + (a • x + b • y)) = f (a • c + a • x + b • (c + y))
⊢ f (c + (a • x + b • y)) = f (a • (c + x) + b • (c + y))
have rw₁ : f (c + (a • x + b • y)) = f (a • c + a • x + (b • c + b • y))
Tactic: rw [smul_add, smul_add, add_add_add_comm, Convex.combo_self 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 : SMul 𝕜 β
s : Set E
f : E → β
hf : ConvexOn 𝕜 s f
c x : E
hx : Membership.mem (γ := Set E) ((fun (z : E) ↦ c + z) ⁻¹' s) x
y : E
hy : Membership.mem (γ := Set E) ((fun (z : E) ↦ c + z) ⁻¹' s) y
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
rw : f (c + (a • x + b • y)) = f (a • c + a • x + b • (c + y))
rw₁ : f (c + (a • x + b • y)) = f (a • c + a • x + (b • c + b • y))
⊢ f (c + (a • x + b • y)) = f (a • (c + x) + b • (c + y))
have rw₂ : f (c + (a • x + b • y)) = f (a • c + b • c + (a • x + b • y))
Tactic: rw [smul_add, smul_add, add_add_add_comm, Convex.combo_self 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 : SMul 𝕜 β
s : Set E
f : E → β
hf : ConvexOn 𝕜 s f
c x : E
hx : Membership.mem (γ := Set E) ((fun (z : E) ↦ c + z) ⁻¹' s) x
y : E
hy : Membership.mem (γ := Set E) ((fun (z : E) ↦ c + z) ⁻¹' s) y
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
rw : f (c + (a • x + b • y)) = f (a • c + a • x + b • (c + y))
rw₁ : f (c + (a • x + b • y)) = f (a • c + a • x + (b • c + b • y))
rw₂ : f (c + (a • x + b • y)) = f (a • c + b • c + (a • x + b • y))
⊢ f (c + (a • x + b • y)) = f (a • (c + x) + b • (c + y))
have rw₃ : f (c + (a • x + b • y)) = f (c + (a • x + b • y))
Tactic: rw [smul_add, smul_add, add_add_add_comm, Convex.combo_self 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 𝕜 β
s : Set E
f : E → β
⊢ ConvexOn 𝕜 s f ↔
    Convex 𝕜 s ∧
      ∀ ⦃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
have refine : ∀
  (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 : a + b = 1),
  f (a • x + b • y) ≤ a • f x + b • f y
Tactic: refine and_congr_right'
    ⟨fun h x hx y hy a b ha hb hab => h hx hy ha.le hb.le hab, fun h x hx y hy 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 𝕜 β
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 : a + b = 1
⊢ f (a • x + b • y) ≤ a • f x + b • f y
have inl : ∀ (ha : LE.le.{u_1} (α := 𝕜) 0 0) (hab : 0 + b = 1),
  f (HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 0 x + b • y) ≤ HSMul.hSMul.{u_1, u_5, u_5} (α := 𝕜) 0 (f x) + b • f y
Tactic: obtain rfl | ha' := ha.eq_or_lt
Cleared hypotheses: a, ha, 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 𝕜 β
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 : a + b = 1
inl :
  ∀ (ha : LE.le.{u_1} (α := 𝕜) 0 0) (hab : 0 + b = 1),
    f (HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 0 x + b • y) ≤ HSMul.hSMul.{u_1, u_5, u_5} (α := 𝕜) 0 (f x) + b • f y
⊢ f (a • x + b • y) ≤ a • f x + b • f y
have inr : ∀ (ha' : 0 < a), f (a • x + b • y) ≤ a • f x + b • f y
Tactic: obtain rfl | ha' := ha.eq_or_lt
-- 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 𝕜 β
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
b : 𝕜
hb : 0 ≤ b
ha : LE.le.{u_1} (α := 𝕜) 0 0
hab : 0 + b = 1
⊢ f (HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 0 x + b • y) ≤ HSMul.hSMul.{u_1, u_5, u_5} (α := 𝕜) 0 (f x) + b • f y
have hab₁ : b = 1
Tactic: rw [zero_add] at hab
Cleared hypotheses: 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 𝕜 β
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
b : 𝕜
hb : 0 ≤ b
ha : LE.le.{u_1} (α := 𝕜) 0 0
hab : b = 1
⊢ f (HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 0 x + b • y) ≤ HSMul.hSMul.{u_1, u_5, u_5} (α := 𝕜) 0 (f x) + b • f y
have inl : ∀ (hb : LE.le.{u_1} (α := 𝕜) 0 1),
  f (HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 0 x + HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 1 y) ≤
    HSMul.hSMul.{u_1, u_5, u_5} (α := 𝕜) 0 (f x) + HSMul.hSMul.{u_1, u_5, u_5} (α := 𝕜) 1 (f y)
Tactic: subst b
Cleared hypotheses: b, 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 𝕜 β
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
ha : LE.le.{u_1} (α := 𝕜) 0 0
hb : LE.le.{u_1} (α := 𝕜) 0 1
⊢ f (HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 0 x + HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 1 y) ≤
    HSMul.hSMul.{u_1, u_5, u_5} (α := 𝕜) 0 (f x) + HSMul.hSMul.{u_1, u_5, u_5} (α := 𝕜) 1 (f y)
have inl : f (0 + HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 1 y) ≤ 0 + HSMul.hSMul.{u_1, u_5, u_5} (α := 𝕜) 1 (f y)
Tactic: simp_rw [zero_smul, zero_add, one_smul, le_rfl]