awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Convex.Exposed
Goal:
𝕜 : Type u_1
E : Type u_2
inst : TopologicalSpace 𝕜
inst_1 : Ring 𝕜
inst_2 : PartialOrder 𝕜
inst_3 : AddCommMonoid E
inst_4 : TopologicalSpace E
inst_5 : Module 𝕜 E
A B C : Set E
hC : IsExposed 𝕜 B C
hCA : C ⊆ A
rw : IsExposed 𝕜 (B ∩ A) C
⊢ IsExposed 𝕜 (A ∩ B) C

Tactic:
rw [inter_comm]

Premises used: Set.inter_comm
-- Module: Mathlib.Analysis.Convex.Exposed
Goal:
𝕜 : Type u_1
E : Type u_2
inst : TopologicalSpace 𝕜
inst_1 : Ring 𝕜
inst_2 : PartialOrder 𝕜
inst_3 : AddCommMonoid E
inst_4 : TopologicalSpace E
inst_5 : Module 𝕜 E
A B C : Set E
hC : IsExposed 𝕜 B C
hCA : C ⊆ A
⊢ IsExposed 𝕜 (B ∩ A) C

Tactic:
hC.inter_left hCA

Premises used: IsExposed.inter_left
-- Module: Mathlib.Analysis.Convex.Exposed
Goal:
𝕜 : Type u_1
E : Type u_2
inst : TopologicalSpace 𝕜
inst_1 : Ring 𝕜
inst_2 : PartialOrder 𝕜
inst_3 : AddCommMonoid E
inst_4 : TopologicalSpace E
inst_5 : Module 𝕜 E
A B C : Set E
hC : IsExposed 𝕜 B C
hCA : C ⊆ A
⊢ IsExposed 𝕜 (B ∩ A) C

Tactic:
exact hC.inter_left hCA

Premises used: IsExposed.inter_left
-- Module: Mathlib.Analysis.Convex.Exposed
Goal:
𝕜 : Type u_1
E : Type u_2
inst : TopologicalSpace 𝕜
inst_1 : Ring 𝕜
inst_2 : PartialOrder 𝕜
inst_3 : AddCommMonoid E
inst_4 : TopologicalSpace E
inst_5 : Module 𝕜 E
inst_6 : OrderClosedTopology 𝕜
A B : Set E
hAB : IsExposed 𝕜 A B
hA : IsClosed A
inl : ∀ (hAB : IsExposed 𝕜 A ∅), IsClosed.{u_2} (X := E) ∅
inr : ∀ (hB : B.Nonempty), IsClosed B
⊢ IsClosed B

Tactic:
obtain rfl | hB := B.eq_empty_or_nonempty

Premises used: Set.eq_empty_or_nonempty, rfl
-- Module: Mathlib.Analysis.Convex.Exposed
Goal:
𝕜 : Type u_1
E : Type u_2
inst : TopologicalSpace 𝕜
inst_1 : Ring 𝕜
inst_2 : PartialOrder 𝕜
inst_3 : AddCommMonoid E
inst_4 : TopologicalSpace E
inst_5 : Module 𝕜 E
inst_6 : OrderClosedTopology 𝕜
A : Set E
hA : IsClosed A
hAB : IsExposed 𝕜 A ∅
⊢ IsClosed.{u_2} (X := E) ∅

Tactic:
simp
-- Module: Mathlib.Analysis.Convex.Exposed
Goal:
𝕜 : Type u_1
E : Type u_2
inst : TopologicalSpace 𝕜
inst_1 : Ring 𝕜
inst_2 : PartialOrder 𝕜
inst_3 : AddCommMonoid E
inst_4 : TopologicalSpace E
inst_5 : Module 𝕜 E
inst_6 : OrderClosedTopology 𝕜
A B : Set E
hAB : IsExposed 𝕜 A B
hA : IsClosed A
hB : B.Nonempty
inr :
  ∀ (l : StrongDual 𝕜 E) (a : 𝕜) (hAB : IsExposed 𝕜 A {x : E | x ∈ A ∧ a ≤ (l : (a : E) → 𝕜) x})
    (hB : Set.Nonempty.{u_2} (α := E) {x : E | x ∈ A ∧ a ≤ (l : (a : E) → 𝕜) x}),
    IsClosed.{u_2} (X := E) {x : E | x ∈ A ∧ a ≤ (l : (a : E) → 𝕜) x}
⊢ IsClosed B

Tactic:
obtain ⟨l, a, rfl⟩ := hAB.eq_inter_halfSpace' hB

Premises used: IsExposed.eq_inter_halfSpace', rfl
-- Module: Mathlib.Analysis.Convex.Exposed
Goal:
𝕜 : Type u_1
E : Type u_2
inst : TopologicalSpace 𝕜
inst_1 : Ring 𝕜
inst_2 : PartialOrder 𝕜
inst_3 : AddCommMonoid E
inst_4 : TopologicalSpace E
inst_5 : Module 𝕜 E
inst_6 : OrderClosedTopology 𝕜
A : Set E
hA : IsClosed A
l : StrongDual 𝕜 E
a : 𝕜
hAB : IsExposed 𝕜 A {x : E | x ∈ A ∧ a ≤ (l : (a : E) → 𝕜) x}
hB : Set.Nonempty.{u_2} (α := E) {x : E | x ∈ A ∧ a ≤ (l : (a : E) → 𝕜) x}
⊢ IsClosed.{u_2} (X := E) {x : E | x ∈ A ∧ a ≤ (l : (a : E) → 𝕜) x}

Tactic:
hA.isClosed_le continuousOn_const l.continuous.continuousOn

Premises used: Continuous.continuousOn, continuousOn_const, ContinuousLinearMap.continuous, IsClosed.isClosed_le
-- Module: Mathlib.Analysis.Convex.Exposed
Goal:
𝕜 : Type u_1
E : Type u_2
inst : TopologicalSpace 𝕜
inst_1 : Ring 𝕜
inst_2 : PartialOrder 𝕜
inst_3 : AddCommMonoid E
inst_4 : TopologicalSpace E
inst_5 : Module 𝕜 E
inst_6 : OrderClosedTopology 𝕜
A : Set E
hA : IsClosed A
l : StrongDual 𝕜 E
a : 𝕜
hAB : IsExposed 𝕜 A {x : E | x ∈ A ∧ a ≤ (l : (a : E) → 𝕜) x}
hB : Set.Nonempty.{u_2} (α := E) {x : E | x ∈ A ∧ a ≤ (l : (a : E) → 𝕜) x}
⊢ IsClosed.{u_2} (X := E) {x : E | x ∈ A ∧ a ≤ (l : (a : E) → 𝕜) x}

Tactic:
exact hA.isClosed_le continuousOn_const l.continuous.continuousOn

Premises used: Continuous.continuousOn, continuousOn_const, ContinuousLinearMap.continuous, IsClosed.isClosed_le
-- Module: Mathlib.Analysis.Convex.Exposed
Goal:
𝕜 : Type u_1
E : Type u_2
inst : TopologicalSpace 𝕜
inst_1 : Ring 𝕜
inst_2 : PartialOrder 𝕜
inst_3 : AddCommMonoid E
inst_4 : TopologicalSpace E
inst_5 : Module 𝕜 E
inst_6 : OrderClosedTopology 𝕜
inst_7 : T2Space E
A B : Set E
hAB : IsExposed 𝕜 A B
hA : IsCompact A
⊢ IsCompact B

Tactic:
hA.of_isClosed_subset (hAB.isClosed hA.isClosed) hAB.subset

Premises used: IsExposed.isClosed, IsExposed.subset, IsCompact.of_isClosed_subset, IsCompact.isClosed
-- Module: Mathlib.Analysis.Convex.Exposed
Goal:
𝕜 : Type u_1
E : Type u_2
inst : TopologicalSpace 𝕜
inst_1 : Ring 𝕜
inst_2 : PartialOrder 𝕜
inst_3 : AddCommMonoid E
inst_4 : TopologicalSpace E
inst_5 : Module 𝕜 E
A : Set E
x : E
⊢ x ∈ exposedPoints 𝕜 A ↔
    x ∈ A ∧
      ∃ (l : StrongDual 𝕜 E),
        ∀ y ∈ A,
          LE.le.{u_1} (α := 𝕜) ((l : (a : E) → 𝕜) y : 𝕜) ((l : (a : E) → 𝕜) x : 𝕜) ∧
            (LE.le.{u_1} (α := 𝕜) ((l : (a : E) → 𝕜) x : 𝕜) ((l : (a : E) → 𝕜) y : 𝕜) → y = x)

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Set.exposedPoints
-- Module: Mathlib.Analysis.Convex.Exposed
Goal:
𝕜 : Type u_1
E : Type u_2
inst : TopologicalSpace 𝕜
inst_1 : Ring 𝕜
inst_2 : PartialOrder 𝕜
inst_3 : AddCommMonoid E
inst_4 : TopologicalSpace E
inst_5 : Module 𝕜 E
A : Set E
⊢ exposedPoints 𝕜 A ⊆ A

Tactic:
fun _ hx => hx.1

Premises used: Set.Subset, And.left
-- Module: Mathlib.Analysis.Convex.Exposed
Goal:
𝕜 : Type u_1
E : Type u_2
inst : TopologicalSpace 𝕜
inst_1 : Ring 𝕜
inst_2 : PartialOrder 𝕜
inst_3 : AddCommMonoid E
inst_4 : TopologicalSpace E
inst_5 : Module 𝕜 E
⊢ Eq.{u_2 + 1} (α := Set E) (exposedPoints 𝕜 ∅) ∅

Tactic:
subset_empty_iff.1 exposedPoints_subset

Premises used: exposedPoints_subset, Iff.mp, Set.subset_empty_iff
-- Module: Mathlib.Analysis.Convex.Exposed
Goal:
𝕜 : Type u_1
E : Type u_2
inst : TopologicalSpace 𝕜
inst_1 : Ring 𝕜
inst_2 : PartialOrder 𝕜
inst_3 : AddCommMonoid E
inst_4 : TopologicalSpace E
inst_5 : Module 𝕜 E
A : Set E
x : E
mpr : IsExposed 𝕜 A {x} → x ∈ exposedPoints 𝕜 A
⊢ x ∈ exposedPoints 𝕜 A ↔ IsExposed 𝕜 A {x}

Tactic:
use fun ⟨hxA, l, hl⟩ _ =>
    ⟨l,
      Eq.symm <|
        eq_singleton_iff_unique_mem.2
          ⟨⟨hxA, fun y hy => (hl y hy).1⟩, fun z hz => (hl z hz.1).2 (hz.2 x hxA)⟩⟩
-- Module: Mathlib.Analysis.Convex.Exposed
Goal:
𝕜 : Type u_1
E : Type u_2
inst : TopologicalSpace 𝕜
inst_1 : Ring 𝕜
inst_2 : PartialOrder 𝕜
inst_3 : AddCommMonoid E
inst_4 : TopologicalSpace E
inst_5 : Module 𝕜 E
A : Set E
x : E
h : IsExposed 𝕜 A {x}
mpr :
  ∀ (l : StrongDual 𝕜 E)
    (hl :
      Eq (α := Set E) {x}
        {x : E | x ∈ A ∧ ∀ y ∈ A, LE.le.{u_1} (α := 𝕜) ((l : (a : E) → 𝕜) y : 𝕜) ((l : (a : E) → 𝕜) x : 𝕜)}),
    x ∈ exposedPoints 𝕜 A
⊢ x ∈ exposedPoints 𝕜 A

Tactic:
obtain ⟨l, hl⟩ := h ⟨x, mem_singleton _⟩

Premises used: Set.mem_singleton, Exists.intro
-- Module: Mathlib.Analysis.Convex.Exposed
Goal:
𝕜 : Type u_1
E : Type u_2
inst : TopologicalSpace 𝕜
inst_1 : Ring 𝕜
inst_2 : PartialOrder 𝕜
inst_3 : AddCommMonoid E
inst_4 : TopologicalSpace E
inst_5 : Module 𝕜 E
A : Set E
x : E
h : IsExposed 𝕜 A {x}
l : StrongDual 𝕜 E
hl :
  Eq (α := Set E) {x}
    {x : E | x ∈ A ∧ ∀ y ∈ A, LE.le.{u_1} (α := 𝕜) ((l : (a : E) → 𝕜) y : 𝕜) ((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 ∧
    ∀ (x_1 : E),
      Membership.mem (γ := Set E)
          {x : E | x ∈ A ∧ ∀ y ∈ A, LE.le.{u_1} (α := 𝕜) ((l : (a : E) → 𝕜) y : 𝕜) ((l : (a : E) → 𝕜) x : 𝕜)} x_1 →
        x_1 = x

Tactic:
rw [eq_comm, eq_singleton_iff_unique_mem] at hl

Premises used: eq_comm, Set.eq_singleton_iff_unique_mem
-- Module: Mathlib.Analysis.Convex.Exposed
Goal:
𝕜 : Type u_1
E : Type u_2
inst : TopologicalSpace 𝕜
inst_1 : Ring 𝕜
inst_2 : PartialOrder 𝕜
inst_3 : AddCommMonoid E
inst_4 : TopologicalSpace E
inst_5 : Module 𝕜 E
A : Set E
x : E
h : IsExposed 𝕜 A {x}
l : StrongDual 𝕜 E
hl :
  Membership.mem (γ := Set E)
      {x : E | x ∈ A ∧ ∀ y ∈ A, LE.le.{u_1} (α := 𝕜) ((l : (a : E) → 𝕜) y : 𝕜) ((l : (a : E) → 𝕜) x : 𝕜)} x ∧
    ∀ (x_1 : E),
      Membership.mem (γ := Set E)
          {x : E | x ∈ A ∧ ∀ y ∈ A, LE.le.{u_1} (α := 𝕜) ((l : (a : E) → 𝕜) y : 𝕜) ((l : (a : E) → 𝕜) x : 𝕜)} x_1 →
        x_1 = x
⊢ x ∈ exposedPoints 𝕜 A

Tactic:
⟨hl.1.1, l, fun y hy =>
      ⟨hl.1.2 y hy, fun hxy => hl.2 y ⟨hy, fun z hz => (hl.1.2 z hz).trans hxy⟩⟩⟩

Premises used: Set.Mem, setOf, Set.exposedPoints, And.right, And.left, And.intro, Exists.intro, LE.le.trans
-- Module: Mathlib.Analysis.Convex.Exposed
Goal:
𝕜 : Type u_1
E : Type u_2
inst : TopologicalSpace 𝕜
inst_1 : Ring 𝕜
inst_2 : PartialOrder 𝕜
inst_3 : AddCommMonoid E
inst_4 : TopologicalSpace E
inst_5 : Module 𝕜 E
A : Set E
x : E
h : IsExposed 𝕜 A {x}
l : StrongDual 𝕜 E
hl :
  Membership.mem (γ := Set E)
      {x : E | x ∈ A ∧ ∀ y ∈ A, LE.le.{u_1} (α := 𝕜) ((l : (a : E) → 𝕜) y : 𝕜) ((l : (a : E) → 𝕜) x : 𝕜)} x ∧
    ∀ (x_1 : E),
      Membership.mem (γ := Set E)
          {x : E | x ∈ A ∧ ∀ y ∈ A, LE.le.{u_1} (α := 𝕜) ((l : (a : E) → 𝕜) y : 𝕜) ((l : (a : E) → 𝕜) x : 𝕜)} x_1 →
        x_1 = x
⊢ x ∈ exposedPoints 𝕜 A

Tactic:
exact
    ⟨hl.1.1, l, fun y hy =>
      ⟨hl.1.2 y hy, fun hxy => hl.2 y ⟨hy, fun z hz => (hl.1.2 z hz).trans hxy⟩⟩⟩
-- Module: Mathlib.Analysis.Convex.Exposed
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 B : Set E
hAB : IsExposed 𝕜 A B
hA : Convex 𝕜 A
inl : ∀ (hAB : IsExposed 𝕜 A ∅), Convex.{u_1, u_2} 𝕜 (E := E) ∅
inr : ∀ (hB : B.Nonempty), Convex 𝕜 B
⊢ Convex 𝕜 B

Tactic:
obtain rfl | hB := B.eq_empty_or_nonempty

Premises used: Set.eq_empty_or_nonempty, rfl
-- Module: Mathlib.Analysis.Convex.Exposed
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
hA : Convex 𝕜 A
hAB : IsExposed 𝕜 A ∅
⊢ Convex.{u_1, u_2} 𝕜 (E := E) ∅

Tactic:
convex_empty

Premises used: convex_empty
-- Module: Mathlib.Analysis.Convex.Exposed
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
hA : Convex 𝕜 A
hAB : IsExposed 𝕜 A ∅
⊢ Convex.{u_1, u_2} 𝕜 (E := E) ∅

Tactic:
exact convex_empty

Premises used: convex_empty
-- Module: Mathlib.Analysis.Convex.Exposed
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 B : Set E
hAB : IsExposed 𝕜 A B
hA : Convex 𝕜 A
hB : B.Nonempty
inr :
  ∀ (l : StrongDual 𝕜 E)
    (hAB :
      IsExposed 𝕜 A {x : E | x ∈ A ∧ ∀ y ∈ A, LE.le.{u_1} (α := 𝕜) ((l : (a : E) → 𝕜) y : 𝕜) ((l : (a : E) → 𝕜) x : 𝕜)})
    (hB :
      Set.Nonempty.{u_2} (α := E)
        {x : E | x ∈ A ∧ ∀ y ∈ A, LE.le.{u_1} (α := 𝕜) ((l : (a : E) → 𝕜) y : 𝕜) ((l : (a : E) → 𝕜) x : 𝕜)}),
    Convex.{u_1, u_2} 𝕜 (E := E)
      {x : E | x ∈ A ∧ ∀ y ∈ A, LE.le.{u_1} (α := 𝕜) ((l : (a : E) → 𝕜) y : 𝕜) ((l : (a : E) → 𝕜) x : 𝕜)}
⊢ Convex 𝕜 B

Tactic:
obtain ⟨l, rfl⟩ := hAB hB

Premises used: rfl
-- Module: Mathlib.Analysis.Convex.Exposed
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
hA : Convex 𝕜 A
l : StrongDual 𝕜 E
hAB : IsExposed 𝕜 A {x : E | x ∈ A ∧ ∀ y ∈ A, LE.le.{u_1} (α := 𝕜) ((l : (a : E) → 𝕜) y : 𝕜) ((l : (a : E) → 𝕜) x : 𝕜)}
hB :
  Set.Nonempty.{u_2} (α := E)
    {x : E | x ∈ A ∧ ∀ y ∈ A, LE.le.{u_1} (α := 𝕜) ((l : (a : E) → 𝕜) y : 𝕜) ((l : (a : E) → 𝕜) x : 𝕜)}
⊢ Convex.{u_1, u_2} 𝕜 (E := E)
    {x : E | x ∈ A ∧ ∀ y ∈ A, LE.le.{u_1} (α := 𝕜) ((l : (a : E) → 𝕜) y : 𝕜) ((l : (a : E) → 𝕜) x : 𝕜)}

Tactic:
fun x₁ hx₁ x₂ hx₂ a b ha hb hab =>
    ⟨hA hx₁.1 hx₂.1 ha hb hab, fun y hy =>
      ((l.toLinearMap.concaveOn convex_univ).convex_ge _ ⟨mem_univ _, hx₁.2 y hy⟩
          ⟨mem_univ _, hx₂.2 y hy⟩ ha hb hab).2⟩

Premises used: ConcaveOn.convex_ge, Set.Mem, setOf, ContinuousLinearMap.toLinearMap, LinearMap.concaveOn, convex_univ, And.right, And.left, Convex, And.intro, Set.mem_univ, DFunLike.coe, StarConvex
-- Module: Mathlib.Analysis.Convex.Exposed
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
hA : Convex 𝕜 A
l : StrongDual 𝕜 E
hAB : IsExposed 𝕜 A {x : E | x ∈ A ∧ ∀ y ∈ A, LE.le.{u_1} (α := 𝕜) ((l : (a : E) → 𝕜) y : 𝕜) ((l : (a : E) → 𝕜) x : 𝕜)}
hB :
  Set.Nonempty.{u_2} (α := E)
    {x : E | x ∈ A ∧ ∀ y ∈ A, LE.le.{u_1} (α := 𝕜) ((l : (a : E) → 𝕜) y : 𝕜) ((l : (a : E) → 𝕜) x : 𝕜)}
⊢ Convex.{u_1, u_2} 𝕜 (E := E)
    {x : E | x ∈ A ∧ ∀ y ∈ A, LE.le.{u_1} (α := 𝕜) ((l : (a : E) → 𝕜) y : 𝕜) ((l : (a : E) → 𝕜) x : 𝕜)}

Tactic:
exact fun x₁ hx₁ x₂ hx₂ a b ha hb hab =>
    ⟨hA hx₁.1 hx₂.1 ha hb hab, fun y hy =>
      ((l.toLinearMap.concaveOn convex_univ).convex_ge _ ⟨mem_univ _, hx₁.2 y hy⟩
          ⟨mem_univ _, hx₂.2 y hy⟩ ha hb hab).2⟩
-- Module: Mathlib.Analysis.Convex.Exposed
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 B : Set E
hAB : IsExposed 𝕜 A B
⊢ IsExtreme 𝕜 A B

Tactic:
⟨hAB.subset, fun x₁ hx₁A x₂ hx₂A x hxB hx => ?_⟩

Premises used: IsExposed.subset, IsExtreme.mk
-- Module: Mathlib.Analysis.Convex.Exposed
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 B : Set E
hAB : IsExposed 𝕜 A B
refine :
  ∀ (x₁ : E) (hx₁A : x₁ ∈ A) (x₂ : E) (hx₂A : x₂ ∈ A) (x : E) (hxB : x ∈ B) (hx : x ∈ openSegment 𝕜 x₁ x₂), x₁ ∈ B
⊢ IsExtreme 𝕜 A B

Tactic:
refine ⟨hAB.subset, fun x₁ hx₁A x₂ hx₂A x hxB hx => ?_⟩
-- Module: Mathlib.Analysis.Convex.Exposed
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 B : Set E
hAB : IsExposed 𝕜 A B
x₁ : E
hx₁A : x₁ ∈ A
x₂ : E
hx₂A : x₂ ∈ A
x : E
hxB : x ∈ B
hx : x ∈ openSegment 𝕜 x₁ x₂
obtain :
  ∀ (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),
    Membership.mem (γ := Set E)
      {x : E | x ∈ A ∧ ∀ y ∈ A, LE.le.{u_1} (α := 𝕜) ((l : (a : E) → 𝕜) y : 𝕜) ((l : (a : E) → 𝕜) x : 𝕜)} x₁
⊢ x₁ ∈ B

Tactic:
obtain ⟨l, rfl⟩ := hAB ⟨x, hxB⟩

Premises used: Exists.intro, rfl
-- Module: Mathlib.Analysis.Convex.Exposed
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
⊢ ConvexOn.{u_1, u_2, u_1} 𝕜 (E := E) (β := 𝕜) univ (⇑l : (a : E) → 𝕜)

Tactic:
have hl : ConvexOn 𝕜 univ l := l.toLinearMap.convexOn convex_univ
-- Module: Mathlib.Analysis.Convex.Exposed
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) → 𝕜)
⊢ LE.le.{u_1} (α := 𝕜) ((l : (a : E) → 𝕜) x₁ : 𝕜) ((l : (a : E) → 𝕜) x : 𝕜)

Tactic:
have hlx₁ := hxB.2 x₁ hx₁A
-- Module: Mathlib.Analysis.Convex.Exposed
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 : 𝕜)
⊢ LE.le.{u_1} (α := 𝕜) ((l : (a : E) → 𝕜) x₂ : 𝕜) ((l : (a : E) → 𝕜) x : 𝕜)

Tactic:
have hlx₂ := hxB.2 x₂ hx₂A
-- Module: Mathlib.Analysis.Convex.Exposed
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₁

Tactic:
⟨hx₁A, fun y hy => ?_⟩

Premises used: Set.Mem, setOf, And.intro
-- Module: Mathlib.Analysis.Convex.Exposed
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 : 𝕜)
refine : ∀ (y : E) (hy : y ∈ A), LE.le.{u_1} (α := 𝕜) ((l : (a : E) → 𝕜) y : 𝕜) ((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₁

Tactic:
refine ⟨hx₁A, fun y hy => ?_⟩
-- Module: Mathlib.Analysis.Convex.Exposed
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
rw : LE.le.{u_1} (α := 𝕜) ((l : (a : E) → 𝕜) y : 𝕜) ((l : (a : E) → 𝕜) x : 𝕜)
⊢ 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₂)]

Premises used: LE.le.antisymm, Set.mem_univ, ConvexOn.le_left_of_right_le
-- Module: Mathlib.Analysis.Convex.Exposed
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 : 𝕜)

Tactic:
hxB.2 y hy

Premises used: And.right
-- Module: Mathlib.Analysis.Convex.Exposed
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 : 𝕜)

Tactic:
exact hxB.2 y hy

Premises used: And.right
-- Module: Mathlib.Analysis.Convex.Exposed
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
⊢ exposedPoints 𝕜 A ⊆ extremePoints 𝕜 A

Tactic:
fun _ hx =>
  (mem_exposedPoints_iff_exposed_singleton.1 hx).isExtreme.mem_extremePoints

Premises used: IsExposed.isExtreme, IsExtreme.mem_extremePoints, Set.Subset, Iff.mp, mem_exposedPoints_iff_exposed_singleton
-- Module: Mathlib.Analysis.Convex.Extrema
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
dsimp : f a ≤ f c
⊢ Membership.mem (γ := Set ℝ) {x : ℝ | (fun (x : ℝ) ↦ f a ≤ f x) x} c

Tactic:
dsimp only [mem_setOf_eq]

Premises used: Set.mem_setOf_eq