awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Convex.Exposed (hypothesis)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : TopologicalSpace 𝕜
inst_1 : Ring 𝕜
inst_2 : LinearOrder 𝕜
inst_3 : IsStrictOrderedRing 𝕜
inst_4 : AddCommMonoid E
inst_5 : TopologicalSpace E
inst_6 : Module 𝕜 E
A : Set E
x₁ : E
hx₁A : x₁ ∈ A
x₂ : E
hx₂A : x₂ ∈ A
x : E
hx : x ∈ openSegment 𝕜 x₁ x₂
l : StrongDual 𝕜 E
hAB : IsExposed 𝕜 A {x : E | x ∈ A ∧ ∀ y ∈ A, LE.le.{u_1} (α := 𝕜) ((l : (a : E) → 𝕜) y : 𝕜) ((l : (a : E) → 𝕜) x : 𝕜)}
hxB :
  Membership.mem (γ := Set E)
    {x : E | x ∈ A ∧ ∀ y ∈ A, LE.le.{u_1} (α := 𝕜) ((l : (a : E) → 𝕜) y : 𝕜) ((l : (a : E) → 𝕜) x : 𝕜)} x
hl : ConvexOn.{u_1, u_2, u_1} 𝕜 (E := E) (β := 𝕜) univ (⇑l : (a : E) → 𝕜)
hlx₁ : LE.le.{u_1} (α := 𝕜) ((l : (a : E) → 𝕜) x₁ : 𝕜) ((l : (a : E) → 𝕜) x : 𝕜)
⊢ Membership.mem (γ := Set E)
    {x : E | x ∈ A ∧ ∀ y ∈ A, LE.le.{u_1} (α := 𝕜) ((l : (a : E) → 𝕜) y : 𝕜) ((l : (a : E) → 𝕜) x : 𝕜)} x₁
have hlx₂ : LE.le.{u_1} (α := 𝕜) ((l : (a : E) → 𝕜) x₂ : 𝕜) ((l : (a : E) → 𝕜) x : 𝕜)
Tactic: have hlx₂ := hxB.2 x₂ hx₂A
-- Lean 4 proof step from Mathlib.Analysis.Convex.Exposed (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : TopologicalSpace 𝕜
inst_1 : Ring 𝕜
inst_2 : LinearOrder 𝕜
inst_3 : IsStrictOrderedRing 𝕜
inst_4 : AddCommMonoid E
inst_5 : TopologicalSpace E
inst_6 : Module 𝕜 E
A : Set E
x₁ : E
hx₁A : x₁ ∈ A
x₂ : E
hx₂A : x₂ ∈ A
x : E
hx : x ∈ openSegment 𝕜 x₁ x₂
l : StrongDual 𝕜 E
hAB : IsExposed 𝕜 A {x : E | x ∈ A ∧ ∀ y ∈ A, LE.le.{u_1} (α := 𝕜) ((l : (a : E) → 𝕜) y : 𝕜) ((l : (a : E) → 𝕜) x : 𝕜)}
hxB :
  Membership.mem (γ := Set E)
    {x : E | x ∈ A ∧ ∀ y ∈ A, LE.le.{u_1} (α := 𝕜) ((l : (a : E) → 𝕜) y : 𝕜) ((l : (a : E) → 𝕜) x : 𝕜)} x
hl : ConvexOn.{u_1, u_2, u_1} 𝕜 (E := E) (β := 𝕜) univ (⇑l : (a : E) → 𝕜)
hlx₁ : LE.le.{u_1} (α := 𝕜) ((l : (a : E) → 𝕜) x₁ : 𝕜) ((l : (a : E) → 𝕜) x : 𝕜)
hlx₂ : LE.le.{u_1} (α := 𝕜) ((l : (a : E) → 𝕜) x₂ : 𝕜) ((l : (a : E) → 𝕜) x : 𝕜)
⊢ Membership.mem (γ := Set E)
    {x : E | x ∈ A ∧ ∀ y ∈ A, LE.le.{u_1} (α := 𝕜) ((l : (a : E) → 𝕜) y : 𝕜) ((l : (a : E) → 𝕜) x : 𝕜)} x₁
have refine : ∀ (y : E) (hy : y ∈ A), LE.le.{u_1} (α := 𝕜) ((l : (a : E) → 𝕜) y : 𝕜) ((l : (a : E) → 𝕜) x₁ : 𝕜)
Tactic: refine ⟨hx₁A, fun y hy => ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Convex.Exposed (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : TopologicalSpace 𝕜
inst_1 : Ring 𝕜
inst_2 : LinearOrder 𝕜
inst_3 : IsStrictOrderedRing 𝕜
inst_4 : AddCommMonoid E
inst_5 : TopologicalSpace E
inst_6 : Module 𝕜 E
A : Set E
x₁ : E
hx₁A : x₁ ∈ A
x₂ : E
hx₂A : x₂ ∈ A
x : E
hx : x ∈ openSegment 𝕜 x₁ x₂
l : StrongDual 𝕜 E
hAB : IsExposed 𝕜 A {x : E | x ∈ A ∧ ∀ y ∈ A, LE.le.{u_1} (α := 𝕜) ((l : (a : E) → 𝕜) y : 𝕜) ((l : (a : E) → 𝕜) x : 𝕜)}
hxB :
  Membership.mem (γ := Set E)
    {x : E | x ∈ A ∧ ∀ y ∈ A, LE.le.{u_1} (α := 𝕜) ((l : (a : E) → 𝕜) y : 𝕜) ((l : (a : E) → 𝕜) x : 𝕜)} x
hl : ConvexOn.{u_1, u_2, u_1} 𝕜 (E := E) (β := 𝕜) univ (⇑l : (a : E) → 𝕜)
hlx₁ : LE.le.{u_1} (α := 𝕜) ((l : (a : E) → 𝕜) x₁ : 𝕜) ((l : (a : E) → 𝕜) x : 𝕜)
hlx₂ : LE.le.{u_1} (α := 𝕜) ((l : (a : E) → 𝕜) x₂ : 𝕜) ((l : (a : E) → 𝕜) x : 𝕜)
y : E
hy : y ∈ A
⊢ LE.le.{u_1} (α := 𝕜) ((l : (a : E) → 𝕜) y : 𝕜) ((l : (a : E) → 𝕜) x₁ : 𝕜)
have rw : LE.le.{u_1} (α := 𝕜) ((l : (a : E) → 𝕜) y : 𝕜) ((l : (a : E) → 𝕜) x : 𝕜)
Tactic: rw [hlx₁.antisymm (hl.le_left_of_right_le (mem_univ _) (mem_univ _) hx hlx₂)]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Extrema (goal)
Goal:
β : Type u_2
inst : AddCommGroup β
inst_1 : PartialOrder β
inst_2 : IsOrderedAddMonoid β
inst_3 : Module ℝ β
inst_4 : IsOrderedModule ℝ β
inst_5 : PosSMulReflectLE ℝ β
f : ℝ → β
a b : ℝ
a_lt_b : a < b
h_local_min : IsLocalMinOn f (Icc a b) a
h_conv : ConvexOn ℝ (Icc a b) f
c : ℝ
hc : c ∈ Icc a b
⊢ Membership.mem (γ := Set ℝ) {x : ℝ | (fun (x : ℝ) ↦ f a ≤ f x) x} c
have dsimp : f a ≤ f c
Tactic: dsimp only [mem_setOf_eq]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Extrema (goal)
Goal:
β : Type u_2
inst : AddCommGroup β
inst_1 : PartialOrder β
inst_2 : IsOrderedAddMonoid β
inst_3 : Module ℝ β
inst_4 : IsOrderedModule ℝ β
inst_5 : PosSMulReflectLE ℝ β
f : ℝ → β
a b : ℝ
a_lt_b : a < b
h_local_min : IsLocalMinOn f (Icc a b) a
h_conv : ConvexOn ℝ (Icc a b) f
c : ℝ
hc : c ∈ Icc a b
⊢ f a ≤ f c
have rw : ∀ (h_local_min : IsMinFilter f (𝓝[≥] a) a) (h_conv : ConvexOn ℝ (Icc a b) f) ⦃c : ℝ⦄ (hc : c ∈ Icc a b), f a ≤ f c
Tactic: rw [IsLocalMinOn, nhdsWithin_Icc_eq_nhdsGE a_lt_b] at h_local_min
Cleared hypotheses: h_local_min, h_conv, c, hc
-- Lean 4 proof step from Mathlib.Analysis.Convex.Extrema (goal)
Goal:
β : Type u_2
inst : AddCommGroup β
inst_1 : PartialOrder β
inst_2 : IsOrderedAddMonoid β
inst_3 : Module ℝ β
inst_4 : IsOrderedModule ℝ β
inst_5 : PosSMulReflectLE ℝ β
f : ℝ → β
a b : ℝ
a_lt_b : a < b
h_local_min : IsMinFilter f (𝓝[≥] a) a
h_conv : ConvexOn ℝ (Icc a b) f
c : ℝ
hc : c ∈ Icc a b
⊢ f a ≤ f c
have inl : ∀ (hc : a ∈ Icc a b), f a ≤ f a
Tactic: rcases hc.1.eq_or_lt with (rfl | a_lt_c)
Cleared hypotheses: c, hc
-- Lean 4 proof step from Mathlib.Analysis.Convex.Extrema (goal)
Goal:
β : Type u_2
inst : AddCommGroup β
inst_1 : PartialOrder β
inst_2 : IsOrderedAddMonoid β
inst_3 : Module ℝ β
inst_4 : IsOrderedModule ℝ β
inst_5 : PosSMulReflectLE ℝ β
f : ℝ → β
a b : ℝ
a_lt_b : a < b
h_local_min : IsMinFilter f (𝓝[≥] a) a
h_conv : ConvexOn ℝ (Icc a b) f
c : ℝ
hc : c ∈ Icc a b
inl : ∀ (hc : a ∈ Icc a b), f a ≤ f a
⊢ f a ≤ f c
have inr : ∀ (a_lt_c : a < c), f a ≤ f c
Tactic: rcases hc.1.eq_or_lt with (rfl | a_lt_c)
-- Lean 4 proof step from Mathlib.Analysis.Convex.Extrema (hypothesis)
Goal:
β : Type u_2
inst : AddCommGroup β
inst_1 : PartialOrder β
inst_2 : IsOrderedAddMonoid β
inst_3 : Module ℝ β
inst_4 : IsOrderedModule ℝ β
inst_5 : PosSMulReflectLE ℝ β
f : ℝ → β
a b : ℝ
a_lt_b : a < b
h_local_min : IsMinFilter f (𝓝[≥] a) a
h_conv : ConvexOn ℝ (Icc a b) f
c : ℝ
hc : c ∈ Icc a b
a_lt_c : a < c
⊢ f a ≤ f c
have H₁ : ∀ᶠ (y : ℝ) in 𝓝[>] a, f a ≤ f y
Tactic: have H₁ : ∀ᶠ y in 𝓝[>] a, f a ≤ f y :=
    h_local_min.filter_mono (nhdsWithin_mono _ Ioi_subset_Ici_self)
-- Lean 4 proof step from Mathlib.Analysis.Convex.Extrema (hypothesis)
Goal:
β : Type u_2
inst : AddCommGroup β
inst_1 : PartialOrder β
inst_2 : IsOrderedAddMonoid β
inst_3 : Module ℝ β
inst_4 : IsOrderedModule ℝ β
inst_5 : PosSMulReflectLE ℝ β
f : ℝ → β
a b : ℝ
a_lt_b : a < b
h_local_min : IsMinFilter f (𝓝[≥] a) a
h_conv : ConvexOn ℝ (Icc a b) f
c : ℝ
hc : c ∈ Icc a b
a_lt_c : a < c
H₁ : ∀ᶠ (y : ℝ) in 𝓝[>] a, f a ≤ f y
⊢ f a ≤ f c
have H₂ : ∀ᶠ (y : ℝ) in 𝓝[>] a, y ∈ Ioc a c
Tactic: have H₂ : ∀ᶠ y in 𝓝[>] a, y ∈ Ioc a c := Ioc_mem_nhdsGT a_lt_c
-- Lean 4 proof step from Mathlib.Analysis.Convex.Extrema (goal)
Goal:
β : Type u_2
inst : AddCommGroup β
inst_1 : PartialOrder β
inst_2 : IsOrderedAddMonoid β
inst_3 : Module ℝ β
inst_4 : IsOrderedModule ℝ β
inst_5 : PosSMulReflectLE ℝ β
f : ℝ → β
a b : ℝ
a_lt_b : a < b
h_local_min : IsMinFilter f (𝓝[≥] a) a
h_conv : ConvexOn ℝ (Icc a b) f
c : ℝ
hc : c ∈ Icc a b
a_lt_c : a < c
H₁ : ∀ᶠ (y : ℝ) in 𝓝[>] a, f a ≤ f y
H₂ : ∀ᶠ (y : ℝ) in 𝓝[>] a, y ∈ Ioc a c
⊢ f a ≤ f c
have inr : ∀ (y : ℝ) (hfy : f a ≤ f y) (hy_ac : y ∈ Ioc a c), f a ≤ f c
Tactic: rcases (H₁.and H₂).exists with ⟨y, hfy, hy_ac⟩
-- Lean 4 proof step from Mathlib.Analysis.Convex.Extrema (goal)
Goal:
β : Type u_2
inst : AddCommGroup β
inst_1 : PartialOrder β
inst_2 : IsOrderedAddMonoid β
inst_3 : Module ℝ β
inst_4 : IsOrderedModule ℝ β
inst_5 : PosSMulReflectLE ℝ β
f : ℝ → β
a b : ℝ
a_lt_b : a < b
h_local_min : IsMinFilter f (𝓝[≥] a) a
h_conv : ConvexOn ℝ (Icc a b) f
c : ℝ
hc : c ∈ Icc a b
a_lt_c : a < c
H₁ : ∀ᶠ (y : ℝ) in 𝓝[>] a, f a ≤ f y
H₂ : ∀ᶠ (y : ℝ) in 𝓝[>] a, y ∈ Ioc a c
y : ℝ
hfy : f a ≤ f y
hy_ac : y ∈ Ioc a c
⊢ f a ≤ f c
have inr : ∀ (ya yc : ℝ) (ya₀ : 0 ≤ ya) (yc₀ : 0 < yc) (yac : ya + yc = 1) (hfy : f a ≤ f (ya * a + yc * c))
  (hy_ac : ya * a + yc * c ∈ Ioc a c), f a ≤ f c
Tactic: rcases (Convex.mem_Ioc a_lt_c).mp hy_ac with ⟨ya, yc, ya₀, yc₀, yac, rfl⟩
Cleared hypotheses: y, hfy, hy_ac
-- Lean 4 proof step from Mathlib.Analysis.Convex.Extrema (goal)
Goal:
β : Type u_2
inst : AddCommGroup β
inst_1 : PartialOrder β
inst_2 : IsOrderedAddMonoid β
inst_3 : Module ℝ β
inst_4 : IsOrderedModule ℝ β
inst_5 : PosSMulReflectLE ℝ β
f : ℝ → β
a b : ℝ
a_lt_b : a < b
h_local_min : IsMinFilter f (𝓝[≥] a) a
h_conv : ConvexOn ℝ (Icc a b) f
c : ℝ
hc : c ∈ Icc a b
a_lt_c : a < c
H₁ : ∀ᶠ (y : ℝ) in 𝓝[>] a, f a ≤ f y
H₂ : ∀ᶠ (y : ℝ) in 𝓝[>] a, y ∈ Ioc a c
ya yc : ℝ
ya₀ : 0 ≤ ya
yc₀ : 0 < yc
yac : ya + yc = 1
hfy : f a ≤ f (ya * a + yc * c)
hy_ac : ya * a + yc * c ∈ Ioc a c
⊢ f a ≤ f c
have inr : ya • f a + yc • f a ≤ ya • f a + yc • f c
Tactic: suffices ya • f a + yc • f a ≤ ya • f a + yc • f c from
    (smul_le_smul_iff_of_pos_left yc₀).1 (le_of_add_le_add_left this)
-- Lean 4 proof step from Mathlib.Analysis.Convex.Extrema (goal)
Goal:
β : Type u_2
inst : AddCommGroup β
inst_1 : PartialOrder β
inst_2 : IsOrderedAddMonoid β
inst_3 : Module ℝ β
inst_4 : IsOrderedModule ℝ β
inst_5 : PosSMulReflectLE ℝ β
f : ℝ → β
a b : ℝ
a_lt_b : a < b
h_local_min : IsMinFilter f (𝓝[≥] a) a
h_conv : ConvexOn ℝ (Icc a b) f
c : ℝ
hc : c ∈ Icc a b
a_lt_c : a < c
H₁ : ∀ᶠ (y : ℝ) in 𝓝[>] a, f a ≤ f y
H₂ : ∀ᶠ (y : ℝ) in 𝓝[>] a, y ∈ Ioc a c
ya yc : ℝ
ya₀ : 0 ≤ ya
yc₀ : 0 < yc
yac : ya + yc = 1
hfy : f a ≤ f (ya * a + yc * c)
hy_ac : ya * a + yc * c ∈ Ioc a c
⊢ ya • f a + yc • f a = f a
have rw : (ya + yc) • f a = f a
Tactic: rw [← add_smul, yac, one_smul]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Extrema (goal)
Goal:
β : Type u_2
inst : AddCommGroup β
inst_1 : PartialOrder β
inst_2 : IsOrderedAddMonoid β
inst_3 : Module ℝ β
inst_4 : IsOrderedModule ℝ β
inst_5 : PosSMulReflectLE ℝ β
f : ℝ → β
a b : ℝ
a_lt_b : a < b
h_local_min : IsMinFilter f (𝓝[≥] a) a
h_conv : ConvexOn ℝ (Icc a b) f
c : ℝ
hc : c ∈ Icc a b
a_lt_c : a < c
H₁ : ∀ᶠ (y : ℝ) in 𝓝[>] a, f a ≤ f y
H₂ : ∀ᶠ (y : ℝ) in 𝓝[>] a, y ∈ Ioc a c
ya yc : ℝ
ya₀ : 0 ≤ ya
yc₀ : 0 < yc
yac : ya + yc = 1
hfy : f a ≤ f (ya * a + yc * c)
hy_ac : ya * a + yc * c ∈ Ioc a c
rw : (ya + yc) • f a = f a
⊢ ya • f a + yc • f a = f a
have rw₁ : HSMul.hSMul (α := ℝ) 1 (f a) = f a
Tactic: rw [← add_smul, yac, one_smul]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Extrema (goal)
Goal:
β : Type u_2
inst : AddCommGroup β
inst_1 : PartialOrder β
inst_2 : IsOrderedAddMonoid β
inst_3 : Module ℝ β
inst_4 : IsOrderedModule ℝ β
inst_5 : PosSMulReflectLE ℝ β
f : ℝ → β
a b : ℝ
a_lt_b : a < b
h_local_min : IsMinFilter f (𝓝[≥] a) a
h_conv : ConvexOn ℝ (Icc a b) f
c : ℝ
hc : c ∈ Icc a b
a_lt_c : a < c
H₁ : ∀ᶠ (y : ℝ) in 𝓝[>] a, f a ≤ f y
H₂ : ∀ᶠ (y : ℝ) in 𝓝[>] a, y ∈ Ioc a c
ya yc : ℝ
ya₀ : 0 ≤ ya
yc₀ : 0 < yc
yac : ya + yc = 1
hfy : f a ≤ f (ya * a + yc * c)
hy_ac : ya * a + yc * c ∈ Ioc a c
rw : (ya + yc) • f a = f a
rw₁ : HSMul.hSMul (α := ℝ) 1 (f a) = f a
⊢ ya • f a + yc • f a = f a
have rw₂ : f a = f a
Tactic: rw [← add_smul, yac, one_smul]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Extrema (goal)
Goal:
β : Type u_2
inst : AddCommGroup β
inst_1 : PartialOrder β
inst_2 : IsOrderedAddMonoid β
inst_3 : Module ℝ β
inst_4 : IsOrderedModule ℝ β
inst_5 : PosSMulReflectLE ℝ β
f : ℝ → β
a b : ℝ
a_lt_b : a < b
h_local_min : IsMinFilter f (𝓝[≥] a) a
h_conv : ConvexOn ℝ (Icc a b) f
c : ℝ
hc : c ∈ Icc a b
a_lt_c : a < c
H₁ : ∀ᶠ (y : ℝ) in 𝓝[>] a, f a ≤ f y
H₂ : ∀ᶠ (y : ℝ) in 𝓝[>] a, y ∈ Ioc a c
ya yc : ℝ
ya₀ : 0 ≤ ya
yc₀ : 0 < yc
yac : ya + yc = 1
hfy : f a ≤ f (ya * a + yc * c)
hy_ac : ya * a + yc * c ∈ Ioc a c
⊢ ya • f a + yc • f a ≤ ya • f a + yc • f c
have ya₁ : ya • f a + yc • f a = f a
Tactic: calc
    ya • f a + yc • f a = f a := by rw [← add_smul, yac, one_smul]
    _ ≤ f (ya * a + yc * c) := hfy
    _ ≤ ya • f a + yc • f c := h_conv.2 (left_mem_Icc.2 a_lt_b.le) hc ya₀ yc₀.le yac
-- Lean 4 proof step from Mathlib.Analysis.Convex.Extrema (hypothesis)
Goal:
E : Type u_1
β : Type u_2
inst : AddCommGroup E
inst_1 : TopologicalSpace E
inst_2 : Module ℝ E
inst_3 : IsTopologicalAddGroup E
inst_4 : ContinuousSMul ℝ E
inst_5 : AddCommGroup β
inst_6 : PartialOrder β
inst_7 : IsOrderedAddMonoid β
inst_8 : Module ℝ β
inst_9 : IsOrderedModule ℝ β
inst_10 : PosSMulReflectLE ℝ β
s : Set E
f : E → β
a : E
a_in_s : a ∈ s
h_localmin : IsLocalMinOn f s a
h_conv : ConvexOn ℝ s f
x : E
x_in_s : x ∈ s
g : ℝ →ᵃ[ℝ] E := AffineMap.lineMap a x
⊢ Membership.mem (γ := Set E) {x : E | (fun (x : E) ↦ f a ≤ f x) x} x
have hg0 : (g : (a : ℝ) → E) 0 = a
Tactic: have hg0 : g 0 = a := AffineMap.lineMap_apply_zero a x
-- Lean 4 proof step from Mathlib.Analysis.Convex.Extrema (hypothesis)
Goal:
E : Type u_1
β : Type u_2
inst : AddCommGroup E
inst_1 : TopologicalSpace E
inst_2 : Module ℝ E
inst_3 : IsTopologicalAddGroup E
inst_4 : ContinuousSMul ℝ E
inst_5 : AddCommGroup β
inst_6 : PartialOrder β
inst_7 : IsOrderedAddMonoid β
inst_8 : Module ℝ β
inst_9 : IsOrderedModule ℝ β
inst_10 : PosSMulReflectLE ℝ β
s : Set E
f : E → β
a : E
a_in_s : a ∈ s
h_localmin : IsLocalMinOn f s a
h_conv : ConvexOn ℝ s f
x : E
x_in_s : x ∈ s
g : ℝ →ᵃ[ℝ] E := AffineMap.lineMap a x
hg0 : (g : (a : ℝ) → E) 0 = a
⊢ Membership.mem (γ := Set E) {x : E | (fun (x : E) ↦ f a ≤ f x) x} x
have hg1 : (g : (a : ℝ) → E) 1 = x
Tactic: have hg1 : g 1 = x := AffineMap.lineMap_apply_one a x
-- Lean 4 proof step from Mathlib.Analysis.Convex.Extrema (hypothesis)
Goal:
E : Type u_1
β : Type u_2
inst : AddCommGroup E
inst_1 : TopologicalSpace E
inst_2 : Module ℝ E
inst_3 : IsTopologicalAddGroup E
inst_4 : ContinuousSMul ℝ E
inst_5 : AddCommGroup β
inst_6 : PartialOrder β
inst_7 : IsOrderedAddMonoid β
inst_8 : Module ℝ β
inst_9 : IsOrderedModule ℝ β
inst_10 : PosSMulReflectLE ℝ β
s : Set E
f : E → β
a : E
a_in_s : a ∈ s
h_localmin : IsLocalMinOn f s a
h_conv : ConvexOn ℝ s f
x : E
x_in_s : x ∈ s
g : ℝ →ᵃ[ℝ] E := AffineMap.lineMap a x
hg0 : (g : (a : ℝ) → E) 0 = a
hg1 : (g : (a : ℝ) → E) 1 = x
⊢ Membership.mem (γ := Set E) {x : E | (fun (x : E) ↦ f a ≤ f x) x} x
have hgc : Continuous[_, inst_1] (⇑g : (a : ℝ) → E)
Tactic: have hgc : Continuous g := AffineMap.lineMap_continuous
-- Lean 4 proof step from Mathlib.Analysis.Convex.Extrema (hypothesis)
Goal:
E : Type u_1
β : Type u_2
inst : AddCommGroup E
inst_1 : TopologicalSpace E
inst_2 : Module ℝ E
inst_3 : IsTopologicalAddGroup E
inst_4 : ContinuousSMul ℝ E
inst_5 : AddCommGroup β
inst_6 : PartialOrder β
inst_7 : IsOrderedAddMonoid β
inst_8 : Module ℝ β
inst_9 : IsOrderedModule ℝ β
inst_10 : PosSMulReflectLE ℝ β
s : Set E
f : E → β
a : E
a_in_s : a ∈ s
h_localmin : IsLocalMinOn f s a
h_conv : ConvexOn ℝ s f
x : E
x_in_s : x ∈ s
g : ℝ →ᵃ[ℝ] E := AffineMap.lineMap a x
hg0 : (g : (a : ℝ) → E) 0 = a
hg1 : (g : (a : ℝ) → E) 1 = x
hgc : Continuous[_, inst_1] (⇑g : (a : ℝ) → E)
⊢ Membership.mem (γ := Set E) {x : E | (fun (x : E) ↦ f a ≤ f x) x} x
have h_maps : MapsTo (α := ℝ) (⇑g : (a : ℝ) → E) (Icc 0 1) s
Tactic: have h_maps : MapsTo g (Icc 0 1) s := by
    simpa only [g, mapsTo_iff_image_subset, ← segment_eq_image_lineMap]
      using h_conv.1.segment_subset a_in_s x_in_s
-- Lean 4 proof step from Mathlib.Analysis.Convex.Extrema (hypothesis)
Goal:
E : Type u_1
β : Type u_2
inst : AddCommGroup E
inst_1 : TopologicalSpace E
inst_2 : Module ℝ E
inst_3 : IsTopologicalAddGroup E
inst_4 : ContinuousSMul ℝ E
inst_5 : AddCommGroup β
inst_6 : PartialOrder β
inst_7 : IsOrderedAddMonoid β
inst_8 : Module ℝ β
inst_9 : IsOrderedModule ℝ β
inst_10 : PosSMulReflectLE ℝ β
s : Set E
f : E → β
a : E
a_in_s : a ∈ s
h_localmin : IsLocalMinOn f s a
h_conv : ConvexOn ℝ s f
x : E
x_in_s : x ∈ s
g : ℝ →ᵃ[ℝ] E := AffineMap.lineMap a x
hg0 : (g : (a : ℝ) → E) 0 = a
hg1 : (g : (a : ℝ) → E) 1 = x
hgc : Continuous[_, inst_1] (⇑g : (a : ℝ) → E)
h_maps : MapsTo (α := ℝ) (⇑g : (a : ℝ) → E) (Icc 0 1) s
⊢ IsLocalMinOn (α := ℝ) (f ∘ (⇑g : (a : ℝ) → E)) (Icc 0 1) 0
have h_localmin₁ : IsLocalMinOn f s ((g : (a : ℝ) → E) 0)
Tactic: rw [← hg0] at h_localmin
Cleared hypotheses: h_localmin, hg0, hg1, hgc, h_maps
-- Lean 4 proof step from Mathlib.Analysis.Convex.Extrema (hypothesis)
Goal:
E : Type u_1
β : Type u_2
inst : AddCommGroup E
inst_1 : TopologicalSpace E
inst_2 : Module ℝ E
inst_3 : IsTopologicalAddGroup E
inst_4 : ContinuousSMul ℝ E
inst_5 : AddCommGroup β
inst_6 : PartialOrder β
inst_7 : IsOrderedAddMonoid β
inst_8 : Module ℝ β
inst_9 : IsOrderedModule ℝ β
inst_10 : PosSMulReflectLE ℝ β
s : Set E
f : E → β
a : E
a_in_s : a ∈ s
h_localmin : IsLocalMinOn f s a
h_conv : ConvexOn ℝ s f
x : E
x_in_s : x ∈ s
g : ℝ →ᵃ[ℝ] E := AffineMap.lineMap a x
hg0 : (g : (a : ℝ) → E) 0 = a
hg1 : (g : (a : ℝ) → E) 1 = x
hgc : Continuous[_, inst_1] (⇑g : (a : ℝ) → E)
h_maps : MapsTo (α := ℝ) (⇑g : (a : ℝ) → E) (Icc 0 1) s
⊢ Membership.mem (γ := Set E) {x : E | (fun (x : E) ↦ f a ≤ f x) x} x
have fg_local_min_on : IsLocalMinOn (α := ℝ) (f ∘ (⇑g : (a : ℝ) → E)) (Icc 0 1) 0
Tactic: have fg_local_min_on : IsLocalMinOn (f ∘ g) (Icc 0 1) 0 := by
    rw [← hg0] at h_localmin
    exact h_localmin.comp_continuousOn h_maps hgc.continuousOn (left_mem_Icc.2 zero_le_one)
-- Lean 4 proof step from Mathlib.Analysis.Convex.Extrema (goal)
Goal:
E : Type u_1
β : Type u_2
inst : AddCommGroup E
inst_1 : TopologicalSpace E
inst_2 : Module ℝ E
inst_3 : IsTopologicalAddGroup E
inst_4 : ContinuousSMul ℝ E
inst_5 : AddCommGroup β
inst_6 : PartialOrder β
inst_7 : IsOrderedAddMonoid β
inst_8 : Module ℝ β
inst_9 : IsOrderedModule ℝ β
inst_10 : PosSMulReflectLE ℝ β
s : Set E
f : E → β
a : E
a_in_s : a ∈ s
h_localmin : IsLocalMinOn f s a
h_conv : ConvexOn ℝ s f
x : E
x_in_s : x ∈ s
g : ℝ →ᵃ[ℝ] E := AffineMap.lineMap a x
hg0 : (g : (a : ℝ) → E) 0 = a
hg1 : (g : (a : ℝ) → E) 1 = x
hgc : Continuous[_, inst_1] (⇑g : (a : ℝ) → E)
h_maps : MapsTo (α := ℝ) (⇑g : (a : ℝ) → E) (Icc 0 1) s
fg_local_min_on : IsLocalMinOn (α := ℝ) (f ∘ (⇑g : (a : ℝ) → E)) (Icc 0 1) 0
⊢ IsMinOn (α := ℝ) (f ∘ (⇑g : (a : ℝ) → E)) (Icc 0 1) 0
have refine : ConvexOn ℝ (E := ℝ) (Icc 0 1) (f ∘ (⇑g : (a : ℝ) → E))
Tactic: refine IsMinOn.of_isLocalMinOn_of_convexOn_Icc one_pos fg_local_min_on ?_
-- Lean 4 proof step from Mathlib.Analysis.Convex.Extrema (hypothesis)
Goal:
E : Type u_1
β : Type u_2
inst : AddCommGroup E
inst_1 : TopologicalSpace E
inst_2 : Module ℝ E
inst_3 : IsTopologicalAddGroup E
inst_4 : ContinuousSMul ℝ E
inst_5 : AddCommGroup β
inst_6 : PartialOrder β
inst_7 : IsOrderedAddMonoid β
inst_8 : Module ℝ β
inst_9 : IsOrderedModule ℝ β
inst_10 : PosSMulReflectLE ℝ β
s : Set E
f : E → β
a : E
a_in_s : a ∈ s
h_localmin : IsLocalMinOn f s a
h_conv : ConvexOn ℝ s f
x : E
x_in_s : x ∈ s
g : ℝ →ᵃ[ℝ] E := AffineMap.lineMap a x
hg0 : (g : (a : ℝ) → E) 0 = a
hg1 : (g : (a : ℝ) → E) 1 = x
hgc : Continuous[_, inst_1] (⇑g : (a : ℝ) → E)
h_maps : MapsTo (α := ℝ) (⇑g : (a : ℝ) → E) (Icc 0 1) s
fg_local_min_on : IsLocalMinOn (α := ℝ) (f ∘ (⇑g : (a : ℝ) → E)) (Icc 0 1) 0
⊢ Membership.mem (γ := Set E) {x : E | (fun (x : E) ↦ f a ≤ f x) x} x
have fg_min_on : IsMinOn (α := ℝ) (f ∘ (⇑g : (a : ℝ) → E)) (Icc 0 1) 0
Tactic: have fg_min_on : IsMinOn (f ∘ g) (Icc 0 1 : Set ℝ) 0 := by
    refine IsMinOn.of_isLocalMinOn_of_convexOn_Icc one_pos fg_local_min_on ?_
    exact (h_conv.comp_affineMap g).subset h_maps (convex_Icc 0 1)
-- Lean 4 proof step from Mathlib.Analysis.Convex.Extreme (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : SMul 𝕜 E
A B C : Set E
hAB : IsExtreme 𝕜 A B
hBC : IsExtreme 𝕜 B C
⊢ IsExtreme 𝕜 A C
have refine : ∀ (x₁ : E) (hx₁A : x₁ ∈ A) (x₂ : E) (hx₂A : x₂ ∈ A) (x : E) (hxC : x ∈ C) (hx : x ∈ openSegment 𝕜 x₁ x₂), x₁ ∈ C
Tactic: refine ⟨hBC.subset.trans hAB.subset, fun x₁ hx₁A x₂ hx₂A x hxC hx ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Convex.Extreme (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : SMul 𝕜 E
A B C : Set E
hAB : IsExtreme 𝕜 A B
hAC : IsExtreme 𝕜 A C
⊢ IsExtreme 𝕜 A (B ∩ C)
have left_mem_of_mem_openSegment : ∀ ⦃x : E⦄, x ∈ A → ∀ ⦃y : E⦄, y ∈ A → ∀ ⦃z : E⦄, z ∈ B ∩ C → z ∈ openSegment 𝕜 x y → x ∈ B ∩ C
Tactic: use Subset.trans inter_subset_left hAB.1
-- Lean 4 proof step from Mathlib.Analysis.Convex.Extreme (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : SMul 𝕜 E
A : Set E
ι : Sort u_6
inst_4 : Nonempty ι
F : ι → Set E
hAF : ∀ (i : ι), IsExtreme 𝕜 A (F i)
⊢ IsExtreme 𝕜 A (⋂ (i : ι), F i)
have inhabit : ∀ (inhabited_h : Inhabited ι), IsExtreme 𝕜 A (⋂ (i : ι), F i)
Tactic: inhabit ι
-- Lean 4 proof step from Mathlib.Analysis.Convex.Extreme (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : SMul 𝕜 E
A : Set E
ι : Sort u_6
inst_4 : Nonempty ι
F : ι → Set E
hAF : ∀ (i : ι), IsExtreme 𝕜 A (F i)
inhabited_h : Inhabited ι
⊢ IsExtreme 𝕜 A (⋂ (i : ι), F i)
have refine : ∀ (x₁ : E) (hx₁A : x₁ ∈ A) (x₂ : E) (hx₂A : x₂ ∈ A) (x : E) (hxF : Membership.mem (γ := Set E) (⋂ (i : ι), F i) x)
  (hx : x ∈ openSegment 𝕜 x₁ x₂), Membership.mem (γ := Set E) (⋂ (i : ι), F i) x₁
Tactic: refine ⟨iInter_subset_of_subset default (hAF default).1, fun x₁ hx₁A x₂ hx₂A x hxF hx ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Convex.Extreme (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : SMul 𝕜 E
A : Set E
ι : Sort u_6
inst_4 : Nonempty ι
F : ι → Set E
hAF : ∀ (i : ι), IsExtreme 𝕜 A (F i)
inhabited_h : Inhabited ι
x₁ : E
hx₁A : x₁ ∈ A
x₂ : E
hx₂A : x₂ ∈ A
x : E
hxF : Membership.mem (γ := Set E) (⋂ (i : ι), F i) x
hx : x ∈ openSegment 𝕜 x₁ x₂
⊢ Membership.mem (γ := Set E) (⋂ (i : ι), F i) x₁
have rw : ∀ (hxF : ∀ (i : ι), x ∈ F i) (hx : x ∈ openSegment 𝕜 x₁ x₂) (i : ι), x₁ ∈ F i
Tactic: rw [mem_iInter] at hxF ⊢
Cleared hypotheses: hxF, hx
-- Lean 4 proof step from Mathlib.Analysis.Convex.Extreme (hypothesis)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : SMul 𝕜 E
A : Set E
F : Set (Set E)
hF : F.Nonempty
hA : ∀ B ∈ F, IsExtreme 𝕜 A B
⊢ IsExtreme 𝕜 A (⋂ B ∈ F, B)
have this : Nonempty.{u_2 + 1} (↑F : Type u_2)
Tactic: haveI := hF.to_subtype
-- Lean 4 proof step from Mathlib.Analysis.Convex.Extreme (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : SMul 𝕜 E
A : Set E
x : E
⊢ x ∈ extremePoints 𝕜 A ↔ x ∈ A ∧ ∀ x₁ ∈ A, ∀ x₂ ∈ A, x ∈ openSegment 𝕜 x₁ x₂ → x₁ = x ∧ x₂ = x
have refine : ∀ (h : x ∈ extremePoints 𝕜 A) (x₁ : E) (hx₁ : x₁ ∈ A) (x₂ : E) (hx₂ : x₂ ∈ A) (hx : x ∈ openSegment 𝕜 x₁ x₂), x₂ = x
Tactic: refine ⟨fun h ↦ ⟨h.1, fun x₁ hx₁ x₂ hx₂ hx ↦ ⟨h.2 hx₁ hx₂ hx, ?_⟩⟩,
    fun h ↦ ⟨h.1, fun x₁ hx₁ x₂ hx₂ hx ↦ (h.2 x₁ hx₁ x₂ hx₂ hx).1⟩⟩
-- Lean 4 proof step from Mathlib.Analysis.Convex.Extreme (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : SMul 𝕜 E
A : Set E
x : E
h : x ∈ extremePoints 𝕜 A
x₁ : E
hx₁ : x₁ ∈ A
x₂ : E
hx₂ : x₂ ∈ A
hx : x ∈ openSegment 𝕜 x₁ x₂
⊢ x₂ = x
have apply : x ∈ openSegment 𝕜 x₂ x₁
Tactic: apply h.2 hx₂ hx₁
-- Lean 4 proof step from Mathlib.Analysis.Convex.Extreme (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommGroup E
inst_3 : AddCommGroup F
inst_4 : Module 𝕜 E
inst_5 : Module 𝕜 F
s : Set E
t : Set F
⊢ extremePoints 𝕜 (s ×ˢ t) = extremePoints 𝕜 s ×ˢ extremePoints 𝕜 t
have h : ∀ (x : E) (y : F), (x, y) ∈ extremePoints 𝕜 (s ×ˢ t) ↔ (x, y) ∈ extremePoints 𝕜 s ×ˢ extremePoints 𝕜 t
Tactic: ext ⟨x, y⟩
-- Lean 4 proof step from Mathlib.Analysis.Convex.Extreme (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommGroup E
inst_3 : AddCommGroup F
inst_4 : Module 𝕜 E
inst_5 : Module 𝕜 F
s : Set E
t : Set F
x : E
y : F
⊢ (x, y) ∈ extremePoints 𝕜 (s ×ˢ t) ↔ (x, y) ∈ extremePoints 𝕜 s ×ˢ extremePoints 𝕜 t
have h : ∀ (hx : (x, y) ∈ s ×ˢ t)
  (h :
    (∀ ⦃x₁ : E⦄, x₁ ∈ s → ∀ ⦃x₂ : E⦄, x₂ ∈ s → (x, y).1 ∈ openSegment 𝕜 x₁ x₂ → x₁ = (x, y).1) ∧
      ∀ ⦃x₁ : F⦄, x₁ ∈ t → ∀ ⦃x₂ : F⦄, x₂ ∈ t → (x, y).2 ∈ openSegment 𝕜 x₁ x₂ → x₁ = (x, y).2)
  ⦃x₁ : E × F⦄, x₁ ∈ s ×ˢ t → ∀ ⦃x₂ : E × F⦄, x₂ ∈ s ×ˢ t → (x, y) ∈ openSegment 𝕜 x₁ x₂ → x₁ = (x, y)
Tactic: refine (and_congr_right fun hx ↦ ⟨fun h ↦ ⟨?_, ?_⟩, fun h ↦ ?_⟩).trans and_and_and_comm