-- Mathlib/Analysis/Convex/KreinMilman.lean
/-- A continuous affine map is surjective from the extreme points of a compact set to the extreme
points of the image of that set. This inclusion is in general strict. -/
lemma surjOn_extremePoints_image (f : E →ᴬ[ℝ] F) (hs : IsCompact s) :
    SurjOn f (extremePoints ℝ s) (extremePoints ℝ (f '' s))

Proof state:
E : Type u_1
F : Type u_2
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : Module ℝ E
inst✝⁸ : TopologicalSpace E
inst✝⁷ : T2Space E
inst✝⁶ : IsTopologicalAddGroup E
inst✝⁵ : ContinuousSMul ℝ E
inst✝⁴ : LocallyConvexSpace ℝ E
s : Set E
inst✝³ : AddCommGroup F
inst✝² : Module ℝ F
inst✝¹ : TopologicalSpace F
inst✝ : T1Space F
f : E →ᴬ[ℝ] F
hs : IsCompact s
x : E
hx : x ∈ s
hw : f x ∈ extremePoints ℝ (⇑f '' s)
ht : IsCompact {x_1 | x_1 ∈ s ∧ f x_1 = f x}
ht₀ : {x_1 | x_1 ∈ s ∧ f x_1 = f x}.Nonempty
hyt :
  ∀ ⦃x₁ : E⦄,
    x₁ ∈ {x_1 | x_1 ∈ s ∧ f x_1 = f x} →
      ∀ ⦃x₂ : E⦄, x₂ ∈ {x_1 | x_1 ∈ s ∧ f x_1 = f x} → x ∈ openSegment ℝ x₁ x₂ → x₁ = x ∧ x₂ = x
y : E
hy : y ∈ s
z : E
hz : z ∈ s
hxyz : x ∈ openSegment ℝ y z
this : (fun a => f a) '' openSegment ℝ y z = openSegment ℝ (f y) (f z)
⊢ f x ∈ (fun a => f a) '' openSegment ℝ y z

Tactic:
exact mem_image_of_mem _ hxyz

Result:
no goals

Proof state:
case intro.intro.intro
E : Type u_1
F : Type u_2
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : Module ℝ E
inst✝⁸ : TopologicalSpace E
inst✝⁷ : T2Space E
inst✝⁶ : IsTopologicalAddGroup E
inst✝⁵ : ContinuousSMul ℝ E
inst✝⁴ : LocallyConvexSpace ℝ E
s : Set E
inst✝³ : AddCommGroup F
inst✝² : Module ℝ F
inst✝¹ : TopologicalSpace F
inst✝ : T1Space F
f : E →ᴬ[ℝ] F
hs : IsCompact s
x : E
hx : x ∈ s
hw : f x ∈ extremePoints ℝ (⇑f '' s)
ht : IsCompact {x_1 | x_1 ∈ s ∧ f x_1 = f x}
ht₀ : {x_1 | x_1 ∈ s ∧ f x_1 = f x}.Nonempty
hyt :
  ∀ ⦃x₁ : E⦄,
    x₁ ∈ {x_1 | x_1 ∈ s ∧ f x_1 = f x} →
      ∀ ⦃x₂ : E⦄, x₂ ∈ {x_1 | x_1 ∈ s ∧ f x_1 = f x} → x ∈ openSegment ℝ x₁ x₂ → x₁ = x ∧ x₂ = x
y : E
hy : y ∈ s
z : E
hz : z ∈ s
hxyz : x ∈ openSegment ℝ y z
⊢ y = x ∧ z = x

Tactic:
have := by simpa using image_openSegment _ f.toAffineMap y z

Result:
case intro.intro.intro
E : Type u_1
F : Type u_2
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : Module ℝ E
inst✝⁸ : TopologicalSpace E
inst✝⁷ : T2Space E
inst✝⁶ : IsTopologicalAddGroup E
inst✝⁵ : ContinuousSMul ℝ E
inst✝⁴ : LocallyConvexSpace ℝ E
s : Set E
inst✝³ : AddCommGroup F
inst✝² : Module ℝ F
inst✝¹ : TopologicalSpace F
inst✝ : T1Space F
f : E →ᴬ[ℝ] F
hs : IsCompact s
x : E
hx : x ∈ s
hw : f x ∈ extremePoints ℝ (⇑f '' s)
ht : IsCompact {x_1 | x_1 ∈ s ∧ f x_1 = f x}
ht₀ : {x_1 | x_1 ∈ s ∧ f x_1 = f x}.Nonempty
hyt :
  ∀ ⦃x₁ : E⦄,
    x₁ ∈ {x_1 | x_1 ∈ s ∧ f x_1 = f x} →
      ∀ ⦃x₂ : E⦄, x₂ ∈ {x_1 | x_1 ∈ s ∧ f x_1 = f x} → x ∈ openSegment ℝ x₁ x₂ → x₁ = x ∧ x₂ = x
y : E
hy : y ∈ s
z : E
hz : z ∈ s
hxyz : x ∈ openSegment ℝ y z
this : (fun a => f a) '' openSegment ℝ y z = openSegment ℝ (f y) (f z)
⊢ y = x ∧ z = x

Proof state:
E : Type u_1
F : Type u_2
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : Module ℝ E
inst✝⁸ : TopologicalSpace E
inst✝⁷ : T2Space E
inst✝⁶ : IsTopologicalAddGroup E
inst✝⁵ : ContinuousSMul ℝ E
inst✝⁴ : LocallyConvexSpace ℝ E
s : Set E
inst✝³ : AddCommGroup F
inst✝² : Module ℝ F
inst✝¹ : TopologicalSpace F
inst✝ : T1Space F
f : E →ᴬ[ℝ] F
hs : IsCompact s
x : E
hx : x ∈ s
hw : f x ∈ extremePoints ℝ (⇑f '' s)
ht : IsCompact {x_1 | x_1 ∈ s ∧ f x_1 = f x}
ht₀ : {x_1 | x_1 ∈ s ∧ f x_1 = f x}.Nonempty
hyt :
  ∀ ⦃x₁ : E⦄,
    x₁ ∈ {x_1 | x_1 ∈ s ∧ f x_1 = f x} →
      ∀ ⦃x₂ : E⦄, x₂ ∈ {x_1 | x_1 ∈ s ∧ f x_1 = f x} → x ∈ openSegment ℝ x₁ x₂ → x₁ = x ∧ x₂ = x
y : E
hy : y ∈ s
z : E
hz : z ∈ s
hxyz : x ∈ openSegment ℝ y z
this : (fun a => f a) '' openSegment ℝ y z = openSegment ℝ (f y) (f z)
⊢ f x ∈ openSegment ℝ (f y) (f z)

Tactic:
rw [← this]

Result:
E : Type u_1
F : Type u_2
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : Module ℝ E
inst✝⁸ : TopologicalSpace E
inst✝⁷ : T2Space E
inst✝⁶ : IsTopologicalAddGroup E
inst✝⁵ : ContinuousSMul ℝ E
inst✝⁴ : LocallyConvexSpace ℝ E
s : Set E
inst✝³ : AddCommGroup F
inst✝² : Module ℝ F
inst✝¹ : TopologicalSpace F
inst✝ : T1Space F
f : E →ᴬ[ℝ] F
hs : IsCompact s
x : E
hx : x ∈ s
hw : f x ∈ extremePoints ℝ (⇑f '' s)
ht : IsCompact {x_1 | x_1 ∈ s ∧ f x_1 = f x}
ht₀ : {x_1 | x_1 ∈ s ∧ f x_1 = f x}.Nonempty
hyt :
  ∀ ⦃x₁ : E⦄,
    x₁ ∈ {x_1 | x_1 ∈ s ∧ f x_1 = f x} →
      ∀ ⦃x₂ : E⦄, x₂ ∈ {x_1 | x_1 ∈ s ∧ f x_1 = f x} → x ∈ openSegment ℝ x₁ x₂ → x₁ = x ∧ x₂ = x
y : E
hy : y ∈ s
z : E
hz : z ∈ s
hxyz : x ∈ openSegment ℝ y z
this : (fun a => f a) '' openSegment ℝ y z = openSegment ℝ (f y) (f z)
⊢ f x ∈ (fun a => f a) '' openSegment ℝ y z

Proof state:
E : Type u_1
F : Type u_2
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : Module ℝ E
inst✝⁸ : TopologicalSpace E
inst✝⁷ : T2Space E
inst✝⁶ : IsTopologicalAddGroup E
inst✝⁵ : ContinuousSMul ℝ E
inst✝⁴ : LocallyConvexSpace ℝ E
s : Set E
inst✝³ : AddCommGroup F
inst✝² : Module ℝ F
inst✝¹ : TopologicalSpace F
inst✝ : T1Space F
f : E →ᴬ[ℝ] F
hs : IsCompact s
w : F
hw : w ∈ extremePoints ℝ (⇑f '' s)
⊢ w ∈ ⇑f '' extremePoints ℝ s

Tactic:
have ht : IsCompact {x ∈ s | f x = w} :=
  hs.inter_right <| isClosed_singleton.preimage f.continuous

Result:
E : Type u_1
F : Type u_2
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : Module ℝ E
inst✝⁸ : TopologicalSpace E
inst✝⁷ : T2Space E
inst✝⁶ : IsTopologicalAddGroup E
inst✝⁵ : ContinuousSMul ℝ E
inst✝⁴ : LocallyConvexSpace ℝ E
s : Set E
inst✝³ : AddCommGroup F
inst✝² : Module ℝ F
inst✝¹ : TopologicalSpace F
inst✝ : T1Space F
f : E →ᴬ[ℝ] F
hs : IsCompact s
w : F
hw : w ∈ extremePoints ℝ (⇑f '' s)
ht : IsCompact {x | x ∈ s ∧ f x = w}
⊢ w ∈ ⇑f '' extremePoints ℝ s

Proof state:
E : Type u_1
F : Type u_2
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : Module ℝ E
inst✝⁸ : TopologicalSpace E
inst✝⁷ : T2Space E
inst✝⁶ : IsTopologicalAddGroup E
inst✝⁵ : ContinuousSMul ℝ E
inst✝⁴ : LocallyConvexSpace ℝ E
s : Set E
inst✝³ : AddCommGroup F
inst✝² : Module ℝ F
inst✝¹ : TopologicalSpace F
inst✝ : T1Space F
f : E →ᴬ[ℝ] F
hs : IsCompact s
w : F
hw : w ∈ extremePoints ℝ (⇑f '' s)
ht : IsCompact {x | x ∈ s ∧ f x = w}
⊢ w ∈ ⇑f '' extremePoints ℝ s

Tactic:
have ht₀ : {x ∈ s | f x = w}.Nonempty := by simpa using extremePoints_subset hw

Result:
E : Type u_1
F : Type u_2
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : Module ℝ E
inst✝⁸ : TopologicalSpace E
inst✝⁷ : T2Space E
inst✝⁶ : IsTopologicalAddGroup E
inst✝⁵ : ContinuousSMul ℝ E
inst✝⁴ : LocallyConvexSpace ℝ E
s : Set E
inst✝³ : AddCommGroup F
inst✝² : Module ℝ F
inst✝¹ : TopologicalSpace F
inst✝ : T1Space F
f : E →ᴬ[ℝ] F
hs : IsCompact s
w : F
hw : w ∈ extremePoints ℝ (⇑f '' s)
ht : IsCompact {x | x ∈ s ∧ f x = w}
ht₀ : {x | x ∈ s ∧ f x = w}.Nonempty
⊢ w ∈ ⇑f '' extremePoints ℝ s

Proof state:
E : Type u_1
F : Type u_2
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : Module ℝ E
inst✝⁸ : TopologicalSpace E
inst✝⁷ : T2Space E
inst✝⁶ : IsTopologicalAddGroup E
inst✝⁵ : ContinuousSMul ℝ E
inst✝⁴ : LocallyConvexSpace ℝ E
s : Set E
inst✝³ : AddCommGroup F
inst✝² : Module ℝ F
inst✝¹ : TopologicalSpace F
inst✝ : T1Space F
f : E →ᴬ[ℝ] F
hs : IsCompact s
w : F
hw : w ∈ extremePoints ℝ (⇑f '' s)
ht : IsCompact {x | x ∈ s ∧ f x = w}
⊢ {x | x ∈ s ∧ f x = w}.Nonempty

Tactic:
simpa using extremePoints_subset hw

Result:
no goals