awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Convex.KreinMilman
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : TopologicalSpace E
inst_3 : T2Space E
inst_4 : IsTopologicalAddGroup E
inst_5 : ContinuousSMul ℝ E
inst_6 : LocallyConvexSpace ℝ E
s : Set E
hscomp : IsCompact s
hAconv : Convex ℝ s
hs : ¬s ⊆ closure ((convexHull ℝ : (a : Set E) → Set E) (extremePoints ℝ s))
x : E
hxA : x ∈ s
hxt : x ∉ closure ((convexHull ℝ : (a : Set E) → Set E) (extremePoints ℝ s))
l : StrongDual ℝ E
r : ℝ
hlr :
  ∀ (a : E),
    Membership.mem (γ := Set E) (closure ((convexHull ℝ : (a : Set E) → Set E) (extremePoints ℝ s))) a →
      (l : (a : E) → ℝ) a < r
hrx : r < (l : (a : E) → ℝ) x
h : IsExposed ℝ s {y : E | y ∈ s ∧ ∀ z ∈ s, LE.le (α := ℝ) ((l : (a : E) → ℝ) z : ℝ) ((l : (a : E) → ℝ) y : ℝ)}
obtain : ∀ (z : E) (hzA : z ∈ s) (hz : IsMaxOn (β := ℝ) (⇑l : (a : E) → ℝ) s z), False
⊢ False

Tactic:
obtain ⟨z, hzA, hz⟩ := hscomp.exists_isMaxOn ⟨x, hxA⟩ l.continuous.continuousOn

Premises used: Continuous.continuousOn, ContinuousLinearMap.continuous, Exists.intro, IsCompact.exists_isMaxOn
-- Module: Mathlib.Analysis.Convex.KreinMilman
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : TopologicalSpace E
inst_3 : T2Space E
inst_4 : IsTopologicalAddGroup E
inst_5 : ContinuousSMul ℝ E
inst_6 : LocallyConvexSpace ℝ E
s : Set E
hscomp : IsCompact s
hAconv : Convex ℝ s
hs : ¬s ⊆ closure ((convexHull ℝ : (a : Set E) → Set E) (extremePoints ℝ s))
x : E
hxA : x ∈ s
hxt : x ∉ closure ((convexHull ℝ : (a : Set E) → Set E) (extremePoints ℝ s))
l : StrongDual ℝ E
r : ℝ
hlr :
  ∀ (a : E),
    Membership.mem (γ := Set E) (closure ((convexHull ℝ : (a : Set E) → Set E) (extremePoints ℝ s))) a →
      (l : (a : E) → ℝ) a < r
hrx : r < (l : (a : E) → ℝ) x
h : IsExposed ℝ s {y : E | y ∈ s ∧ ∀ z ∈ s, LE.le (α := ℝ) ((l : (a : E) → ℝ) z : ℝ) ((l : (a : E) → ℝ) y : ℝ)}
z : E
hzA : z ∈ s
hz : IsMaxOn (β := ℝ) (⇑l : (a : E) → ℝ) s z
obtain :
  ∀ (y : E)
    (hy :
      Membership.mem (γ := Set E)
        (extremePoints ℝ {y : E | y ∈ s ∧ ∀ z ∈ s, LE.le (α := ℝ) ((l : (a : E) → ℝ) z : ℝ) ((l : (a : E) → ℝ) y : ℝ)})
        y),
    False
⊢ False

Tactic:
obtain ⟨y, hy⟩ := (h.isCompact hscomp).extremePoints_nonempty ⟨z, hzA, hz⟩

Premises used: IsCompact.extremePoints_nonempty, And.intro, IsExposed.isCompact, Exists.intro
-- Module: Mathlib.Analysis.Convex.KreinMilman
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : TopologicalSpace E
inst_3 : T2Space E
inst_4 : IsTopologicalAddGroup E
inst_5 : ContinuousSMul ℝ E
inst_6 : LocallyConvexSpace ℝ E
s : Set E
hscomp : IsCompact s
hAconv : Convex ℝ s
hs : ¬s ⊆ closure ((convexHull ℝ : (a : Set E) → Set E) (extremePoints ℝ s))
x : E
hxA : x ∈ s
hxt : x ∉ closure ((convexHull ℝ : (a : Set E) → Set E) (extremePoints ℝ s))
l : StrongDual ℝ E
r : ℝ
hlr :
  ∀ (a : E),
    Membership.mem (γ := Set E) (closure ((convexHull ℝ : (a : Set E) → Set E) (extremePoints ℝ s))) a →
      (l : (a : E) → ℝ) a < r
hrx : r < (l : (a : E) → ℝ) x
h : IsExposed ℝ s {y : E | y ∈ s ∧ ∀ z ∈ s, LE.le (α := ℝ) ((l : (a : E) → ℝ) z : ℝ) ((l : (a : E) → ℝ) y : ℝ)}
z : E
hzA : z ∈ s
hz : IsMaxOn (β := ℝ) (⇑l : (a : E) → ℝ) s z
y : E
hy :
  Membership.mem (γ := Set E)
    (extremePoints ℝ {y : E | y ∈ s ∧ ∀ z ∈ s, LE.le (α := ℝ) ((l : (a : E) → ℝ) z : ℝ) ((l : (a : E) → ℝ) y : ℝ)}) y
linarith :
  HSub.hSub (β := ℝ) r ((l : (a : E) → ℝ) x : ℝ) + HSub.hSub (α := ℝ) ((l : (a : E) → ℝ) y : ℝ) r +
      HSub.hSub (α := ℝ) (β := ℝ) ((l : (a : E) → ℝ) x : ℝ) ((l : (a : E) → ℝ) y : ℝ) =
    0
⊢ False

Tactic:
linarith [hlr _ (subset_closure <| subset_convexHull _ _ <|
    h.isExtreme.extremePoints_subset_extremePoints hy), hy.1.2 x hxA]

Premises used: IsExposed.isExtreme, subset_closure, subset_convexHull, IsExtreme.extremePoints_subset_extremePoints, And.right, And.left
-- Module: Mathlib.Analysis.Convex.KreinMilman
Goal:
E : Type u_1
F : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : TopologicalSpace E
inst_3 : T2Space E
inst_4 : IsTopologicalAddGroup E
inst_5 : ContinuousSMul ℝ E
inst_6 : LocallyConvexSpace ℝ E
s : Set E
inst_7 : AddCommGroup F
inst_8 : Module ℝ F
inst_9 : TopologicalSpace F
inst_10 : T1Space F
f : E →ᴬ[ℝ] F
hs : IsCompact s
w : F
hw : Membership.mem (γ := Set F) (extremePoints ℝ ((⇑f : (a : E) → F) '' s)) w
⊢ IsCompact.{u_1} (X := E) {x : E | x ∈ s ∧ (f : (a : E) → F) x = w}

Tactic:
have ht : IsCompact {x ∈ s | f x = w} :=
    hs.inter_right <| isClosed_singleton.preimage f.continuous
-- Module: Mathlib.Analysis.Convex.KreinMilman
Goal:
E : Type u_1
F : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : TopologicalSpace E
inst_3 : T2Space E
inst_4 : IsTopologicalAddGroup E
inst_5 : ContinuousSMul ℝ E
inst_6 : LocallyConvexSpace ℝ E
s : Set E
inst_7 : AddCommGroup F
inst_8 : Module ℝ F
inst_9 : TopologicalSpace F
inst_10 : T1Space F
f : E →ᴬ[ℝ] F
hs : IsCompact s
w : F
hw : Membership.mem (γ := Set F) (extremePoints ℝ ((⇑f : (a : E) → F) '' s)) w
ht : IsCompact.{u_1} (X := E) {x : E | x ∈ s ∧ (f : (a : E) → F) x = w}
⊢ Set.Nonempty.{u_1} (α := E) {x : E | x ∈ s ∧ (f : (a : E) → F) x = w}

Tactic:
simpa using extremePoints_subset hw

Premises used: extremePoints_subset
-- Module: Mathlib.Analysis.Convex.KreinMilman
Goal:
E : Type u_1
F : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : TopologicalSpace E
inst_3 : T2Space E
inst_4 : IsTopologicalAddGroup E
inst_5 : ContinuousSMul ℝ E
inst_6 : LocallyConvexSpace ℝ E
s : Set E
inst_7 : AddCommGroup F
inst_8 : Module ℝ F
inst_9 : TopologicalSpace F
inst_10 : T1Space F
f : E →ᴬ[ℝ] F
hs : IsCompact s
w : F
hw : Membership.mem (γ := Set F) (extremePoints ℝ ((⇑f : (a : E) → F) '' s)) w
ht : IsCompact.{u_1} (X := E) {x : E | x ∈ s ∧ (f : (a : E) → F) x = w}
⊢ Set.Nonempty.{u_1} (α := E) {x : E | x ∈ s ∧ (f : (a : E) → F) x = w}

Tactic:
have ht₀ : {x ∈ s | f x = w}.Nonempty := by simpa using extremePoints_subset hw
-- Module: Mathlib.Analysis.Convex.KreinMilman
Goal:
E : Type u_1
F : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : TopologicalSpace E
inst_3 : T2Space E
inst_4 : IsTopologicalAddGroup E
inst_5 : ContinuousSMul ℝ E
inst_6 : LocallyConvexSpace ℝ E
s : Set E
inst_7 : AddCommGroup F
inst_8 : Module ℝ F
inst_9 : TopologicalSpace F
inst_10 : T1Space F
f : E →ᴬ[ℝ] F
hs : IsCompact s
w : F
hw : Membership.mem (γ := Set F) (extremePoints ℝ ((⇑f : (a : E) → F) '' s)) w
ht : IsCompact.{u_1} (X := E) {x : E | x ∈ s ∧ (f : (a : E) → F) x = w}
ht₀ : Set.Nonempty.{u_1} (α := E) {x : E | x ∈ s ∧ (f : (a : E) → F) x = w}
obtain :
  ∀ (x : E) (hx : x ∈ s)
    (hw :
      Membership.mem.{u_2, u_2} (α := F) (γ := Set F) (extremePoints ℝ ((⇑f : (a : E) → F) '' s))
        ((f : (a : E) → F) x : F))
    (ht :
      IsCompact.{u_1} (X := E)
        {x_1 : E | x_1 ∈ s ∧ Eq.{u_2 + 1} (α := F) ((f : (a : E) → F) x_1 : F) ((f : (a : E) → F) x : F)})
    (ht₀ :
      Set.Nonempty.{u_1} (α := E)
        {x_1 : E | x_1 ∈ s ∧ Eq.{u_2 + 1} (α := F) ((f : (a : E) → F) x_1 : F) ((f : (a : E) → F) x : F)})
    (hyt :
      ∀ ⦃x₁ : E⦄,
        Membership.mem (γ := Set E)
            {x_1 : E | x_1 ∈ s ∧ Eq.{u_2 + 1} (α := F) ((f : (a : E) → F) x_1 : F) ((f : (a : E) → F) x : F)} x₁ →
          ∀ ⦃x₂ : E⦄,
            Membership.mem (γ := Set E)
                {x_1 : E | x_1 ∈ s ∧ Eq.{u_2 + 1} (α := F) ((f : (a : E) → F) x_1 : F) ((f : (a : E) → F) x : F)} x₂ →
              x ∈ openSegment ℝ x₁ x₂ → x₁ = x),
    Membership.mem.{u_2, u_2} (α := F) (γ := Set F) ((⇑f : (a : E) → F) '' extremePoints ℝ s) ((f : (a : E) → F) x : F)
⊢ Membership.mem (γ := Set F) ((⇑f : (a : E) → F) '' extremePoints ℝ s) w

Tactic:
obtain ⟨x, ⟨hx, rfl⟩, hyt⟩ := ht.extremePoints_nonempty ht₀

Premises used: IsCompact.extremePoints_nonempty, rfl
-- Module: Mathlib.Analysis.Convex.KreinMilman
Goal:
E : Type u_1
F : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : TopologicalSpace E
inst_3 : T2Space E
inst_4 : IsTopologicalAddGroup E
inst_5 : ContinuousSMul ℝ E
inst_6 : LocallyConvexSpace ℝ E
s : Set E
inst_7 : AddCommGroup F
inst_8 : Module ℝ F
inst_9 : TopologicalSpace F
inst_10 : T1Space F
f : E →ᴬ[ℝ] F
hs : IsCompact s
x : E
hx : x ∈ s
hw :
  Membership.mem.{u_2, u_2} (α := F) (γ := Set F) (extremePoints ℝ ((⇑f : (a : E) → F) '' s)) ((f : (a : E) → F) x : F)
ht :
  IsCompact.{u_1} (X := E)
    {x_1 : E | x_1 ∈ s ∧ Eq.{u_2 + 1} (α := F) ((f : (a : E) → F) x_1 : F) ((f : (a : E) → F) x : F)}
ht₀ :
  Set.Nonempty.{u_1} (α := E)
    {x_1 : E | x_1 ∈ s ∧ Eq.{u_2 + 1} (α := F) ((f : (a : E) → F) x_1 : F) ((f : (a : E) → F) x : F)}
hyt :
  ∀ ⦃x₁ : E⦄,
    Membership.mem (γ := Set E)
        {x_1 : E | x_1 ∈ s ∧ Eq.{u_2 + 1} (α := F) ((f : (a : E) → F) x_1 : F) ((f : (a : E) → F) x : F)} x₁ →
      ∀ ⦃x₂ : E⦄,
        Membership.mem (γ := Set E)
            {x_1 : E | x_1 ∈ s ∧ Eq.{u_2 + 1} (α := F) ((f : (a : E) → F) x_1 : F) ((f : (a : E) → F) x : F)} x₂ →
          x ∈ openSegment ℝ x₁ x₂ → x₁ = x
⊢ Membership.mem.{u_2, u_2} (α := F) (γ := Set F) ((⇑f : (a : E) → F) '' extremePoints ℝ s) ((f : (a : E) → F) x : F)

Tactic:
mem_image_of_mem _ ⟨hx, fun y hy z hz hxyz ↦ ?_⟩

Premises used: Set.mem_image_of_mem, And.intro
-- Module: Mathlib.Analysis.Convex.KreinMilman
Goal:
E : Type u_1
F : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : TopologicalSpace E
inst_3 : T2Space E
inst_4 : IsTopologicalAddGroup E
inst_5 : ContinuousSMul ℝ E
inst_6 : LocallyConvexSpace ℝ E
s : Set E
inst_7 : AddCommGroup F
inst_8 : Module ℝ F
inst_9 : TopologicalSpace F
inst_10 : T1Space F
f : E →ᴬ[ℝ] F
hs : IsCompact s
x : E
hx : x ∈ s
hw :
  Membership.mem.{u_2, u_2} (α := F) (γ := Set F) (extremePoints ℝ ((⇑f : (a : E) → F) '' s)) ((f : (a : E) → F) x : F)
ht :
  IsCompact.{u_1} (X := E)
    {x_1 : E | x_1 ∈ s ∧ Eq.{u_2 + 1} (α := F) ((f : (a : E) → F) x_1 : F) ((f : (a : E) → F) x : F)}
ht₀ :
  Set.Nonempty.{u_1} (α := E)
    {x_1 : E | x_1 ∈ s ∧ Eq.{u_2 + 1} (α := F) ((f : (a : E) → F) x_1 : F) ((f : (a : E) → F) x : F)}
hyt :
  ∀ ⦃x₁ : E⦄,
    Membership.mem (γ := Set E)
        {x_1 : E | x_1 ∈ s ∧ Eq.{u_2 + 1} (α := F) ((f : (a : E) → F) x_1 : F) ((f : (a : E) → F) x : F)} x₁ →
      ∀ ⦃x₂ : E⦄,
        Membership.mem (γ := Set E)
            {x_1 : E | x_1 ∈ s ∧ Eq.{u_2 + 1} (α := F) ((f : (a : E) → F) x_1 : F) ((f : (a : E) → F) x : F)} x₂ →
          x ∈ openSegment ℝ x₁ x₂ → x₁ = x
refine : ∀ (y : E) (hy : y ∈ s) (z : E) (hz : z ∈ s) (hxyz : x ∈ openSegment ℝ y z), y = x
⊢ Membership.mem.{u_2, u_2} (α := F) (γ := Set F) ((⇑f : (a : E) → F) '' extremePoints ℝ s) ((f : (a : E) → F) x : F)

Tactic:
refine mem_image_of_mem _ ⟨hx, fun y hy z hz hxyz ↦ ?_⟩
-- Module: Mathlib.Analysis.Convex.KreinMilman
Goal:
E : Type u_1
F : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : TopologicalSpace E
inst_3 : T2Space E
inst_4 : IsTopologicalAddGroup E
inst_5 : ContinuousSMul ℝ E
inst_6 : LocallyConvexSpace ℝ E
s : Set E
inst_7 : AddCommGroup F
inst_8 : Module ℝ F
inst_9 : TopologicalSpace F
inst_10 : T1Space F
f : E →ᴬ[ℝ] F
hs : IsCompact s
x : E
hx : x ∈ s
hw :
  Membership.mem.{u_2, u_2} (α := F) (γ := Set F) (extremePoints ℝ ((⇑f : (a : E) → F) '' s)) ((f : (a : E) → F) x : F)
ht :
  IsCompact.{u_1} (X := E)
    {x_1 : E | x_1 ∈ s ∧ Eq.{u_2 + 1} (α := F) ((f : (a : E) → F) x_1 : F) ((f : (a : E) → F) x : F)}
ht₀ :
  Set.Nonempty.{u_1} (α := E)
    {x_1 : E | x_1 ∈ s ∧ Eq.{u_2 + 1} (α := F) ((f : (a : E) → F) x_1 : F) ((f : (a : E) → F) x : F)}
hyt :
  ∀ ⦃x₁ : E⦄,
    Membership.mem (γ := Set E)
        {x_1 : E | x_1 ∈ s ∧ Eq.{u_2 + 1} (α := F) ((f : (a : E) → F) x_1 : F) ((f : (a : E) → F) x : F)} x₁ →
      ∀ ⦃x₂ : E⦄,
        Membership.mem (γ := Set E)
            {x_1 : E | x_1 ∈ s ∧ Eq.{u_2 + 1} (α := F) ((f : (a : E) → F) x_1 : F) ((f : (a : E) → F) x : F)} x₂ →
          x ∈ openSegment ℝ x₁ x₂ → x₁ = x
y : E
hy : y ∈ s
z : E
hz : z ∈ s
hxyz : x ∈ openSegment ℝ y z
⊢ Eq.{u_2 + 1} (α := Set F) ((fun (a : E) ↦ (f : (a : E) → F) a) '' openSegment ℝ y z : Set F)
    (openSegment ℝ ((f : (a : E) → F) y) ((f : (a : E) → F) z) : Set F)

Tactic:
simpa using image_openSegment _ f.toAffineMap y z

Premises used: image_openSegment, ContinuousAffineMap.toAffineMap
-- Module: Mathlib.Analysis.Convex.KreinMilman
Goal:
E : Type u_1
F : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : TopologicalSpace E
inst_3 : T2Space E
inst_4 : IsTopologicalAddGroup E
inst_5 : ContinuousSMul ℝ E
inst_6 : LocallyConvexSpace ℝ E
s : Set E
inst_7 : AddCommGroup F
inst_8 : Module ℝ F
inst_9 : TopologicalSpace F
inst_10 : T1Space F
f : E →ᴬ[ℝ] F
hs : IsCompact s
x : E
hx : x ∈ s
hw :
  Membership.mem.{u_2, u_2} (α := F) (γ := Set F) (extremePoints ℝ ((⇑f : (a : E) → F) '' s)) ((f : (a : E) → F) x : F)
ht :
  IsCompact.{u_1} (X := E)
    {x_1 : E | x_1 ∈ s ∧ Eq.{u_2 + 1} (α := F) ((f : (a : E) → F) x_1 : F) ((f : (a : E) → F) x : F)}
ht₀ :
  Set.Nonempty.{u_1} (α := E)
    {x_1 : E | x_1 ∈ s ∧ Eq.{u_2 + 1} (α := F) ((f : (a : E) → F) x_1 : F) ((f : (a : E) → F) x : F)}
hyt :
  ∀ ⦃x₁ : E⦄,
    Membership.mem (γ := Set E)
        {x_1 : E | x_1 ∈ s ∧ Eq.{u_2 + 1} (α := F) ((f : (a : E) → F) x_1 : F) ((f : (a : E) → F) x : F)} x₁ →
      ∀ ⦃x₂ : E⦄,
        Membership.mem (γ := Set E)
            {x_1 : E | x_1 ∈ s ∧ Eq.{u_2 + 1} (α := F) ((f : (a : E) → F) x_1 : F) ((f : (a : E) → F) x : F)} x₂ →
          x ∈ openSegment ℝ x₁ x₂ → x₁ = x
y : E
hy : y ∈ s
z : E
hz : z ∈ s
hxyz : x ∈ openSegment ℝ y z
⊢ Eq.{u_2 + 1} (α := Set F) ((fun (a : E) ↦ (f : (a : E) → F) a) '' openSegment ℝ y z : Set F)
    (openSegment ℝ ((f : (a : E) → F) y) ((f : (a : E) → F) z) : Set F)

Tactic:
have := by simpa using image_openSegment _ f.toAffineMap y z
-- Module: Mathlib.Analysis.Convex.KreinMilman
Goal:
E : Type u_1
F : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : TopologicalSpace E
inst_3 : T2Space E
inst_4 : IsTopologicalAddGroup E
inst_5 : ContinuousSMul ℝ E
inst_6 : LocallyConvexSpace ℝ E
s : Set E
inst_7 : AddCommGroup F
inst_8 : Module ℝ F
inst_9 : TopologicalSpace F
inst_10 : T1Space F
f : E →ᴬ[ℝ] F
hs : IsCompact s
x : E
hx : x ∈ s
hw :
  Membership.mem.{u_2, u_2} (α := F) (γ := Set F) (extremePoints ℝ ((⇑f : (a : E) → F) '' s)) ((f : (a : E) → F) x : F)
ht :
  IsCompact.{u_1} (X := E)
    {x_1 : E | x_1 ∈ s ∧ Eq.{u_2 + 1} (α := F) ((f : (a : E) → F) x_1 : F) ((f : (a : E) → F) x : F)}
ht₀ :
  Set.Nonempty.{u_1} (α := E)
    {x_1 : E | x_1 ∈ s ∧ Eq.{u_2 + 1} (α := F) ((f : (a : E) → F) x_1 : F) ((f : (a : E) → F) x : F)}
hyt :
  ∀ ⦃x₁ : E⦄,
    Membership.mem (γ := Set E)
        {x_1 : E | x_1 ∈ s ∧ Eq.{u_2 + 1} (α := F) ((f : (a : E) → F) x_1 : F) ((f : (a : E) → F) x : F)} x₁ →
      ∀ ⦃x₂ : E⦄,
        Membership.mem (γ := Set E)
            {x_1 : E | x_1 ∈ s ∧ Eq.{u_2 + 1} (α := F) ((f : (a : E) → F) x_1 : F) ((f : (a : E) → F) x : F)} x₂ →
          x ∈ openSegment ℝ x₁ x₂ → x₁ = x
y : E
hy : y ∈ s
z : E
hz : z ∈ s
hxyz : x ∈ openSegment ℝ y z
this :
  Eq.{u_2 + 1} (α := Set F) ((fun (a : E) ↦ (f : (a : E) → F) a) '' openSegment ℝ y z : Set F)
    (openSegment ℝ ((f : (a : E) → F) y) ((f : (a : E) → F) z) : Set F)
rw :
  ∀
    (hw :
      Membership.mem.{u_2, u_2} (α := F) (γ := Set F) ((⇑f : (a : E) → F) '' s) ((f : (a : E) → F) x : F) ∧
        ∀ (x₁ : F),
          Membership.mem (γ := Set F) ((⇑f : (a : E) → F) '' s) x₁ →
            ∀ (x₂ : F),
              Membership.mem (γ := Set F) ((⇑f : (a : E) → F) '' s) x₂ →
                Membership.mem (α := F) (openSegment ℝ x₁ x₂) ((f : (a : E) → F) x : F) →
                  x₁ = (f : (a : E) → F) x ∧ x₂ = (f : (a : E) → F) x)
    (ht :
      IsCompact.{u_1} (X := E)
        {x_1 : E | x_1 ∈ s ∧ Eq.{u_2 + 1} (α := F) ((f : (a : E) → F) x_1 : F) ((f : (a : E) → F) x : F)})
    (ht₀ :
      Set.Nonempty.{u_1} (α := E)
        {x_1 : E | x_1 ∈ s ∧ Eq.{u_2 + 1} (α := F) ((f : (a : E) → F) x_1 : F) ((f : (a : E) → F) x : F)})
    (hyt :
      ∀ ⦃x₁ : E⦄,
        Membership.mem (γ := Set E)
            {x_1 : E | x_1 ∈ s ∧ Eq.{u_2 + 1} (α := F) ((f : (a : E) → F) x_1 : F) ((f : (a : E) → F) x : F)} x₁ →
          ∀ ⦃x₂ : E⦄,
            Membership.mem (γ := Set E)
                {x_1 : E | x_1 ∈ s ∧ Eq.{u_2 + 1} (α := F) ((f : (a : E) → F) x_1 : F) ((f : (a : E) → F) x : F)} x₂ →
              x ∈ openSegment ℝ x₁ x₂ → x₁ = x)
    (y : E) (hy : y ∈ s) (z : E) (hz : z ∈ s) (hxyz : x ∈ openSegment ℝ y z)
    (this :
      Eq.{u_2 + 1} (α := Set F) ((fun (a : E) ↦ (f : (a : E) → F) a) '' openSegment ℝ y z : Set F)
        (openSegment ℝ ((f : (a : E) → F) y) ((f : (a : E) → F) z) : Set F)),
    y = x
⊢ y = x

Tactic:
rw [mem_extremePoints] at hw

Premises used: mem_extremePoints
-- Module: Mathlib.Analysis.Convex.KreinMilman
Goal:
E : Type u_1
F : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : TopologicalSpace E
inst_3 : T2Space E
inst_4 : IsTopologicalAddGroup E
inst_5 : ContinuousSMul ℝ E
inst_6 : LocallyConvexSpace ℝ E
s : Set E
inst_7 : AddCommGroup F
inst_8 : Module ℝ F
inst_9 : TopologicalSpace F
inst_10 : T1Space F
f : E →ᴬ[ℝ] F
hs : IsCompact s
x : E
hx : x ∈ s
hw :
  Membership.mem.{u_2, u_2} (α := F) (γ := Set F) ((⇑f : (a : E) → F) '' s) ((f : (a : E) → F) x : F) ∧
    ∀ (x₁ : F),
      Membership.mem (γ := Set F) ((⇑f : (a : E) → F) '' s) x₁ →
        ∀ (x₂ : F),
          Membership.mem (γ := Set F) ((⇑f : (a : E) → F) '' s) x₂ →
            Membership.mem (α := F) (openSegment ℝ x₁ x₂) ((f : (a : E) → F) x : F) →
              x₁ = (f : (a : E) → F) x ∧ x₂ = (f : (a : E) → F) x
ht :
  IsCompact.{u_1} (X := E)
    {x_1 : E | x_1 ∈ s ∧ Eq.{u_2 + 1} (α := F) ((f : (a : E) → F) x_1 : F) ((f : (a : E) → F) x : F)}
ht₀ :
  Set.Nonempty.{u_1} (α := E)
    {x_1 : E | x_1 ∈ s ∧ Eq.{u_2 + 1} (α := F) ((f : (a : E) → F) x_1 : F) ((f : (a : E) → F) x : F)}
hyt :
  ∀ ⦃x₁ : E⦄,
    Membership.mem (γ := Set E)
        {x_1 : E | x_1 ∈ s ∧ Eq.{u_2 + 1} (α := F) ((f : (a : E) → F) x_1 : F) ((f : (a : E) → F) x : F)} x₁ →
      ∀ ⦃x₂ : E⦄,
        Membership.mem (γ := Set E)
            {x_1 : E | x_1 ∈ s ∧ Eq.{u_2 + 1} (α := F) ((f : (a : E) → F) x_1 : F) ((f : (a : E) → F) x : F)} x₂ →
          x ∈ openSegment ℝ x₁ x₂ → x₁ = x
y : E
hy : y ∈ s
z : E
hz : z ∈ s
hxyz : x ∈ openSegment ℝ y z
this :
  Eq.{u_2 + 1} (α := Set F) ((fun (a : E) ↦ (f : (a : E) → F) a) '' openSegment ℝ y z : Set F)
    (openSegment ℝ ((f : (a : E) → F) y) ((f : (a : E) → F) z) : Set F)
rw :
  Membership.mem.{u_2, u_2} (α := F) (γ := Set F) ((fun (a : E) ↦ (f : (a : E) → F) a) '' openSegment ℝ y z)
    ((f : (a : E) → F) x : F)
⊢ Membership.mem.{u_2, u_2} (α := F) (γ := Set F) (openSegment ℝ ((f : (a : E) → F) y) ((f : (a : E) → F) z) : Set F)
    ((f : (a : E) → F) x : F)

Tactic:
rw [← this]
-- Module: Mathlib.Analysis.Convex.KreinMilman
Goal:
E : Type u_1
F : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : TopologicalSpace E
inst_3 : T2Space E
inst_4 : IsTopologicalAddGroup E
inst_5 : ContinuousSMul ℝ E
inst_6 : LocallyConvexSpace ℝ E
s : Set E
inst_7 : AddCommGroup F
inst_8 : Module ℝ F
inst_9 : TopologicalSpace F
inst_10 : T1Space F
f : E →ᴬ[ℝ] F
hs : IsCompact s
x : E
hx : x ∈ s
hw :
  Membership.mem.{u_2, u_2} (α := F) (γ := Set F) ((⇑f : (a : E) → F) '' s) ((f : (a : E) → F) x : F) ∧
    ∀ (x₁ : F),
      Membership.mem (γ := Set F) ((⇑f : (a : E) → F) '' s) x₁ →
        ∀ (x₂ : F),
          Membership.mem (γ := Set F) ((⇑f : (a : E) → F) '' s) x₂ →
            Membership.mem (α := F) (openSegment ℝ x₁ x₂) ((f : (a : E) → F) x : F) →
              x₁ = (f : (a : E) → F) x ∧ x₂ = (f : (a : E) → F) x
ht :
  IsCompact.{u_1} (X := E)
    {x_1 : E | x_1 ∈ s ∧ Eq.{u_2 + 1} (α := F) ((f : (a : E) → F) x_1 : F) ((f : (a : E) → F) x : F)}
ht₀ :
  Set.Nonempty.{u_1} (α := E)
    {x_1 : E | x_1 ∈ s ∧ Eq.{u_2 + 1} (α := F) ((f : (a : E) → F) x_1 : F) ((f : (a : E) → F) x : F)}
hyt :
  ∀ ⦃x₁ : E⦄,
    Membership.mem (γ := Set E)
        {x_1 : E | x_1 ∈ s ∧ Eq.{u_2 + 1} (α := F) ((f : (a : E) → F) x_1 : F) ((f : (a : E) → F) x : F)} x₁ →
      ∀ ⦃x₂ : E⦄,
        Membership.mem (γ := Set E)
            {x_1 : E | x_1 ∈ s ∧ Eq.{u_2 + 1} (α := F) ((f : (a : E) → F) x_1 : F) ((f : (a : E) → F) x : F)} x₂ →
          x ∈ openSegment ℝ x₁ x₂ → x₁ = x
y : E
hy : y ∈ s
z : E
hz : z ∈ s
hxyz : x ∈ openSegment ℝ y z
this :
  Eq.{u_2 + 1} (α := Set F) ((fun (a : E) ↦ (f : (a : E) → F) a) '' openSegment ℝ y z : Set F)
    (openSegment ℝ ((f : (a : E) → F) y) ((f : (a : E) → F) z) : Set F)
⊢ Membership.mem.{u_2, u_2} (α := F) (γ := Set F) ((fun (a : E) ↦ (f : (a : E) → F) a) '' openSegment ℝ y z)
    ((f : (a : E) → F) x : F)

Tactic:
mem_image_of_mem _ hxyz

Premises used: Set.mem_image_of_mem
-- Module: Mathlib.Analysis.Convex.KreinMilman
Goal:
E : Type u_1
F : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : TopologicalSpace E
inst_3 : T2Space E
inst_4 : IsTopologicalAddGroup E
inst_5 : ContinuousSMul ℝ E
inst_6 : LocallyConvexSpace ℝ E
s : Set E
inst_7 : AddCommGroup F
inst_8 : Module ℝ F
inst_9 : TopologicalSpace F
inst_10 : T1Space F
f : E →ᴬ[ℝ] F
hs : IsCompact s
x : E
hx : x ∈ s
hw :
  Membership.mem.{u_2, u_2} (α := F) (γ := Set F) ((⇑f : (a : E) → F) '' s) ((f : (a : E) → F) x : F) ∧
    ∀ (x₁ : F),
      Membership.mem (γ := Set F) ((⇑f : (a : E) → F) '' s) x₁ →
        ∀ (x₂ : F),
          Membership.mem (γ := Set F) ((⇑f : (a : E) → F) '' s) x₂ →
            Membership.mem (α := F) (openSegment ℝ x₁ x₂) ((f : (a : E) → F) x : F) →
              x₁ = (f : (a : E) → F) x ∧ x₂ = (f : (a : E) → F) x
ht :
  IsCompact.{u_1} (X := E)
    {x_1 : E | x_1 ∈ s ∧ Eq.{u_2 + 1} (α := F) ((f : (a : E) → F) x_1 : F) ((f : (a : E) → F) x : F)}
ht₀ :
  Set.Nonempty.{u_1} (α := E)
    {x_1 : E | x_1 ∈ s ∧ Eq.{u_2 + 1} (α := F) ((f : (a : E) → F) x_1 : F) ((f : (a : E) → F) x : F)}
hyt :
  ∀ ⦃x₁ : E⦄,
    Membership.mem (γ := Set E)
        {x_1 : E | x_1 ∈ s ∧ Eq.{u_2 + 1} (α := F) ((f : (a : E) → F) x_1 : F) ((f : (a : E) → F) x : F)} x₁ →
      ∀ ⦃x₂ : E⦄,
        Membership.mem (γ := Set E)
            {x_1 : E | x_1 ∈ s ∧ Eq.{u_2 + 1} (α := F) ((f : (a : E) → F) x_1 : F) ((f : (a : E) → F) x : F)} x₂ →
          x ∈ openSegment ℝ x₁ x₂ → x₁ = x
y : E
hy : y ∈ s
z : E
hz : z ∈ s
hxyz : x ∈ openSegment ℝ y z
this :
  Eq.{u_2 + 1} (α := Set F) ((fun (a : E) ↦ (f : (a : E) → F) a) '' openSegment ℝ y z : Set F)
    (openSegment ℝ ((f : (a : E) → F) y) ((f : (a : E) → F) z) : Set F)
⊢ Membership.mem.{u_2, u_2} (α := F) (γ := Set F) ((fun (a : E) ↦ (f : (a : E) → F) a) '' openSegment ℝ y z)
    ((f : (a : E) → F) x : F)

Tactic:
exact mem_image_of_mem _ hxyz

Premises used: Set.mem_image_of_mem