awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Convex.StoneSeparation
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
s t : Set E
hs : Convex 𝕜 s
ht : Convex 𝕜 t
hst : Disjoint s t
S : Set (Set E) := {C : Set E | Convex 𝕜 C ∧ Disjoint C t}
C : Set E
hsC : s ⊆ C
hmax : Maximal (fun (x : Set E) ↦ x ∈ S) C
hC : Convex 𝕜 C ∧ Disjoint C t
x : E
hx : x ∈ Cᶜ
y : E
hy : y ∈ Cᶜ
z : E
hz : z ∈ segment 𝕜 x y
hzC : z ∈ C
c : E
hc : c ∈ Cᶜ
h : ∀ (a : E) (_ : a ∈ C), segment 𝕜 c a ∩ t = ∅
suffices : Disjoint ((convexHull 𝕜 : (a : Set E) → Set E) (insert c C)) t
⊢ False

Tactic:
suffices h : Disjoint (convexHull 𝕜 (insert c C)) t by
    rw [hmax.eq_of_subset ⟨convex_convexHull _ _, h⟩ <|
      (subset_insert ..).trans <| subset_convexHull ..] at hc
    exact hc (subset_convexHull _ _ <| mem_insert _ _)
-- Module: Mathlib.Analysis.Convex.StoneSeparation
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
s t : Set E
hs : Convex 𝕜 s
ht : Convex 𝕜 t
hst : Disjoint s t
S : Set (Set E) := {C : Set E | Convex 𝕜 C ∧ Disjoint C t}
C : Set E
hsC : s ⊆ C
hmax : Maximal (fun (x : Set E) ↦ x ∈ S) C
hC : Convex 𝕜 C ∧ Disjoint C t
x : E
hx : x ∈ Cᶜ
y : E
hy : y ∈ Cᶜ
z : E
hz : z ∈ segment 𝕜 x y
hzC : z ∈ C
c : E
hc : c ∈ Cᶜ
h : ∀ (a : E) (_ : a ∈ C), segment 𝕜 c a ∩ t = ∅
rw :
  Disjoint
    (⋃ (y : E), ⋃ (_ : Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) C : Set E) y), segment 𝕜 c y) t
⊢ Disjoint ((convexHull 𝕜 : (a : Set E) → Set E) (insert c C)) t

Tactic:
rw [convexHull_insert ⟨z, hzC⟩, convexJoin_singleton_left]

Premises used: convexHull_insert, convexJoin_singleton_left, Exists.intro
-- Module: Mathlib.Analysis.Convex.StoneSeparation
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
s t : Set E
hs : Convex 𝕜 s
ht : Convex 𝕜 t
hst : Disjoint s t
S : Set (Set E) := {C : Set E | Convex 𝕜 C ∧ Disjoint C t}
C : Set E
hsC : s ⊆ C
hmax : Maximal (fun (x : Set E) ↦ x ∈ S) C
hC : Convex 𝕜 C ∧ Disjoint C t
x : E
hx : x ∈ Cᶜ
y : E
hy : y ∈ Cᶜ
z : E
hz : z ∈ segment 𝕜 x y
hzC : z ∈ C
c : E
hc : c ∈ Cᶜ
h : ∀ (a : E) (_ : a ∈ C), segment 𝕜 c a ∩ t = ∅
⊢ Disjoint
    (⋃ (y : E), ⋃ (_ : Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) C : Set E) y), segment 𝕜 c y) t

Tactic:
disjoint_iUnion₂_left.2 fun a ha => disjoint_iff_inter_eq_empty.2 (h a ?_)

Premises used: Iff.mpr, Set.disjoint_iff_inter_eq_empty, Set.disjoint_iUnion₂_left
-- Module: Mathlib.Analysis.Convex.StoneSeparation
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
s t : Set E
hs : Convex 𝕜 s
ht : Convex 𝕜 t
hst : Disjoint s t
S : Set (Set E) := {C : Set E | Convex 𝕜 C ∧ Disjoint C t}
C : Set E
hsC : s ⊆ C
hmax : Maximal (fun (x : Set E) ↦ x ∈ S) C
hC : Convex 𝕜 C ∧ Disjoint C t
x : E
hx : x ∈ Cᶜ
y : E
hy : y ∈ Cᶜ
z : E
hz : z ∈ segment 𝕜 x y
hzC : z ∈ C
c : E
hc : c ∈ Cᶜ
h : ∀ (a : E) (_ : a ∈ C), segment 𝕜 c a ∩ t = ∅
refine : ∀ (a : E) (ha : Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) C : Set E) a), a ∈ C
⊢ Disjoint
    (⋃ (y : E), ⋃ (_ : Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) C : Set E) y), segment 𝕜 c y) t

Tactic:
refine disjoint_iUnion₂_left.2 fun a ha => disjoint_iff_inter_eq_empty.2 (h a ?_)

Premises used: Iff.mpr, Set.disjoint_iff_inter_eq_empty, Set.disjoint_iUnion₂_left
-- Module: Mathlib.Analysis.Convex.StoneSeparation
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
s t : Set E
hs : Convex 𝕜 s
ht : Convex 𝕜 t
hst : Disjoint s t
S : Set (Set E) := {C : Set E | Convex 𝕜 C ∧ Disjoint C t}
C : Set E
hsC : s ⊆ C
hmax : Maximal (fun (x : Set E) ↦ x ∈ S) C
hC : Convex 𝕜 C ∧ Disjoint C t
x : E
hx : x ∈ Cᶜ
y : E
hy : y ∈ Cᶜ
z : E
hz : z ∈ segment 𝕜 x y
hzC : z ∈ C
c : E
hc : c ∈ Cᶜ
h : ∀ (a : E) (_ : a ∈ C), segment 𝕜 c a ∩ t = ∅
a : E
ha rwa rwa₁ rwa₂ rwa₃ : Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) C : Set E) a
⊢ a ∈ C

Tactic:
rwa [← hC.1.convexHull_eq]

Premises used: And.left, Convex.convexHull_eq
-- Module: Mathlib.Analysis.Convex.Strict.Extreme
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : TopologicalSpace E
inst_3 : IsTopologicalAddGroup E
inst_4 : ContinuousSMul ℝ E
inst_5 : Nontrivial E
S : Set E
⊢ Disjoint (interior S) (extremePoints ℝ S)

Tactic:
Set.disjoint_iff.mpr fun x ⟨x_int, x_ext⟩ ↦ ?_

Premises used: Iff.mpr, Membership.mem, _private.0.disjoint_interior_extremePoints.match_1, EmptyCollection.emptyCollection, Set.disjoint_iff
-- Module: Mathlib.Analysis.Convex.Strict.Extreme
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : TopologicalSpace E
inst_3 : IsTopologicalAddGroup E
inst_4 : ContinuousSMul ℝ E
inst_5 : Nontrivial E
S : Set E
refine :
  ∀ x ∈ interior S ∩ extremePoints ℝ S,
    ∀ (x_int : x ∈ interior S) (x_ext : x ∈ extremePoints ℝ S), Membership.mem (γ := Set E) ∅ x
⊢ Disjoint (interior S) (extremePoints ℝ S)

Tactic:
refine Set.disjoint_iff.mpr fun x ⟨x_int, x_ext⟩ ↦ ?_

Premises used: Iff.mpr, Set.disjoint_iff
-- Module: Mathlib.Analysis.Convex.Strict.Extreme
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : TopologicalSpace E
inst_3 : IsTopologicalAddGroup E
inst_4 : ContinuousSMul ℝ E
inst_5 : Nontrivial E
S : Set E
x : E
h : x ∈ interior S ∩ extremePoints ℝ S
x_int : x ∈ interior S
x_ext : x ∈ extremePoints ℝ S
⊢ S ∈ 𝓝 x

Tactic:
rw [mem_interior_iff_mem_nhds] at x_int

Premises used: mem_interior_iff_mem_nhds
-- Module: Mathlib.Analysis.Convex.Strict.Extreme
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : TopologicalSpace E
inst_3 : IsTopologicalAddGroup E
inst_4 : ContinuousSMul ℝ E
inst_5 : Nontrivial E
S : Set E
x : E
h : x ∈ interior S ∩ extremePoints ℝ S
x_int : x ∈ interior S
x_ext : x ∈ extremePoints ℝ S
x_int₁ : S ∈ 𝓝 x
⊢ x ∈ extremePoints ℝ S

Tactic:
rw [mem_interior_iff_mem_nhds] at x_int

Premises used: mem_interior_iff_mem_nhds
-- Module: Mathlib.Analysis.Convex.Strict.Extreme
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : TopologicalSpace E
inst_3 : IsTopologicalAddGroup E
inst_4 : ContinuousSMul ℝ E
inst_5 : Nontrivial E
S : Set E
x : E
h : x ∈ interior S ∩ extremePoints ℝ S
x_int : S ∈ 𝓝 x
x_ext : x ∈ extremePoints ℝ S
⊢ ∀ᶠ (v : E) in 𝓝[≠] 0, x - v ∈ S

Tactic:
have h₁ : ∀ᶠ v in 𝓝[≠] 0, x - v ∈ S :=
    (tendsto_inf_left <| (continuous_sub_left _).tendsto' _ _ (sub_zero _)).eventually x_int
-- Module: Mathlib.Analysis.Convex.Strict.Extreme
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : TopologicalSpace E
inst_3 : IsTopologicalAddGroup E
inst_4 : ContinuousSMul ℝ E
inst_5 : Nontrivial E
S : Set E
x : E
h : x ∈ interior S ∩ extremePoints ℝ S
x_int : S ∈ 𝓝 x
x_ext : x ∈ extremePoints ℝ S
h₁ : ∀ᶠ (v : E) in 𝓝[≠] 0, x - v ∈ S
⊢ ∀ᶠ (v : E) in 𝓝[≠] 0, x + v ∈ S

Tactic:
have h₂ : ∀ᶠ v in 𝓝[≠] 0, x + v ∈ S :=
    (tendsto_inf_left <| (continuous_const_add _).tendsto' _ _ (add_zero _)).eventually x_int
-- Module: Mathlib.Analysis.Convex.Strict.Extreme
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : TopologicalSpace E
inst_3 : IsTopologicalAddGroup E
inst_4 : ContinuousSMul ℝ E
inst_5 : Nontrivial E
S : Set E
x : E
h : x ∈ interior S ∩ extremePoints ℝ S
x_int : S ∈ 𝓝 x
x_ext : x ∈ extremePoints ℝ S
h₁ : ∀ᶠ (v : E) in 𝓝[≠] 0, x - v ∈ S
h₂ : ∀ᶠ (v : E) in 𝓝[≠] 0, x + v ∈ S
obtain : ∀ (v : E) (v_ne : v ≠ 0) (hv₁ : x - v ∈ S) (hv₂ : x + v ∈ S), Membership.mem (γ := Set E) ∅ x
⊢ Membership.mem (γ := Set E) ∅ x

Tactic:
obtain ⟨v, ⟨hv₁, hv₂⟩, (v_ne : v ≠ 0)⟩ := h₁.and h₂ |>.and eventually_mem_nhdsWithin |>.exists

Premises used: eventually_mem_nhdsWithin, Filter.Eventually.and, Filter.Eventually.exists
-- Module: Mathlib.Analysis.Convex.Strict.Extreme
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : TopologicalSpace E
inst_3 : IsTopologicalAddGroup E
inst_4 : ContinuousSMul ℝ E
inst_5 : Nontrivial E
S : Set E
x : E
h : x ∈ interior S ∩ extremePoints ℝ S
x_int : S ∈ 𝓝 x
x_ext : x ∈ extremePoints ℝ S
h₁ : ∀ᶠ (v : E) in 𝓝[≠] 0, x - v ∈ S
h₂ : ∀ᶠ (v : E) in 𝓝[≠] 0, x + v ∈ S
v : E
v_ne : v ≠ 0
hv₁ : x - v ∈ S
hv₂ : x + v ∈ S
⊢ x ∈ openSegment ℝ (x - v) (x + v)

Tactic:
have key : x ∈ openSegment ℝ (x - v) (x + v) := mem_openSegment_sub_add _ _
-- Module: Mathlib.Analysis.Convex.Strict.Extreme
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : TopologicalSpace E
inst_3 : IsTopologicalAddGroup E
inst_4 : ContinuousSMul ℝ E
inst_5 : Nontrivial E
S : Set E
x : E
h : x ∈ interior S ∩ extremePoints ℝ S
x_int : S ∈ 𝓝 x
x_ext : x ∈ extremePoints ℝ S
h₁ : ∀ᶠ (v : E) in 𝓝[≠] 0, x - v ∈ S
h₂ : ∀ᶠ (v : E) in 𝓝[≠] 0, x + v ∈ S
v : E
v_ne : v ≠ 0
hv₁ : x - v ∈ S
hv₂ : x + v ∈ S
key : x ∈ openSegment ℝ (x - v) (x + v)
⊢ Membership.mem (γ := Set E) ∅ x

Tactic:
grind only [x_ext.2 hv₁ hv₂ key]

Premises used: And.right
-- Module: Mathlib.Analysis.Convex.Strict.Extreme
Goal:
𝕜 : Type u_1
A : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid A
inst_3 : Module 𝕜 A
inst_4 : TopologicalSpace A
C : Set A
hc : StrictConvex 𝕜 C
⊢ C \ interior C ⊆ extremePoints 𝕜 C

Tactic:
fun x hx ↦ ⟨hx.1, fun y hy z hz ⟨a, b, ha, hb, hab, hxab⟩ ↦ ?_⟩

Premises used: Set.extremePoints, Set.Mem, setOf, Set.Subset, _private.0.StrictConvex.diff_interior_subset_extremePoints.match_1, And.left, And.intro, Eq
-- Module: Mathlib.Analysis.Convex.Strict.Extreme
Goal:
𝕜 : Type u_1
A : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid A
inst_3 : Module 𝕜 A
inst_4 : TopologicalSpace A
C : Set A
hc : StrictConvex 𝕜 C
refine :
  ∀ (x : A) (hx : x ∈ C \ interior C) (y : A) (hy : y ∈ C) (z : A) (hz : z ∈ C),
    x ∈ openSegment 𝕜 y z → ∀ (a b : 𝕜) (ha : 0 < a) (hb : 0 < b) (hab : a + b = 1) (hxab : a • y + b • z = x), y = x
⊢ C \ interior C ⊆ extremePoints 𝕜 C

Tactic:
refine fun x hx ↦ ⟨hx.1, fun y hy z hz ⟨a, b, ha, hb, hab, hxab⟩ ↦ ?_⟩
-- Module: Mathlib.Analysis.Convex.Strict.Extreme
Goal:
𝕜 : Type u_1
A : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid A
inst_3 : Module 𝕜 A
inst_4 : TopologicalSpace A
C : Set A
hc : StrictConvex 𝕜 C
x : A
hx : x ∈ C \ interior C
y : A
hy : y ∈ C
z : A
hz : z ∈ C
h : x ∈ openSegment 𝕜 y z
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
hxab : a • y + b • z = x
by_contra : ∀ (this : ¬y = z), False
⊢ y = z

Tactic:
by_contra
-- Module: Mathlib.Analysis.Convex.Strict.Extreme
Goal:
𝕜 : Type u_1
A : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid A
inst_3 : Module 𝕜 A
inst_4 : TopologicalSpace A
C : Set A
hc : StrictConvex 𝕜 C
x : A
hx : x ∈ C \ interior C
y : A
hy : y ∈ C
z : A
hz : z ∈ C
h : x ∈ openSegment 𝕜 y z
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
hxab : a • y + b • z = x
this : ¬y = z
⊢ False

Tactic:
hx.2 <| hxab ▸ hc hy hz this ha hb hab

Premises used: Eq.rec, And.right
-- Module: Mathlib.Analysis.Convex.Strict.Extreme
Goal:
𝕜 : Type u_1
A : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid A
inst_3 : Module 𝕜 A
inst_4 : TopologicalSpace A
C : Set A
hc : StrictConvex 𝕜 C
x : A
hx : x ∈ C \ interior C
y : A
hy : y ∈ C
z : A
hz : z ∈ C
h : x ∈ openSegment 𝕜 y z
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
hxab : a • y + b • z = x
this : ¬y = z
⊢ False

Tactic:
exact hx.2 <| hxab ▸ hc hy hz this ha hb hab

Premises used: And.right
-- Module: Mathlib.Analysis.Convex.Strict.Extreme
Goal:
𝕜 : Type u_1
A : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid A
inst_3 : Module 𝕜 A
inst_4 : TopologicalSpace A
C : Set A
hc : StrictConvex 𝕜 C
x : A
hx : x ∈ C \ interior C
y : A
hy : y ∈ C
z : A
hz : z ∈ C
h : x ∈ openSegment 𝕜 y z
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
hxab : a • y + b • z = x
⊢ y = z

Tactic:
have hyz : y = z := by
    by_contra
    exact hx.2 <| hxab ▸ hc hy hz this ha hb hab
-- Module: Mathlib.Analysis.Convex.Strict.Extreme
Goal:
𝕜 : Type u_1
A : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid A
inst_3 : Module 𝕜 A
inst_4 : TopologicalSpace A
C : Set A
hc : StrictConvex 𝕜 C
x : A
hx : x ∈ C \ interior C
y : A
hy : y ∈ C
z : A
hz : z ∈ C
h : x ∈ openSegment 𝕜 y z
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
hxab : a • y + b • z = x
hyz : y = z
rwa : ∀ (hxab : a • y + b • y = x) (hyz : y = z), y = x
rwa₁ : ∀ (hxab : (a + b) • y = x) (hyz : y = z), y = x
rwa₂ : ∀ (hxab : HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 1 y = x) (hyz : y = z), y = x
rwa₃ rwa₄ rwa₅ rwa₆ : ∀ (hxab : y = x) (hyz : y = z), y = x
⊢ y = x

Tactic:
rwa [← hyz, ← add_smul, hab, one_smul] at hxab

Premises used: one_smul, add_smul
-- Module: Mathlib.Analysis.Convex.Strict.Extreme
Goal:
A : Type u_1
inst : NormedAddCommGroup A
inst_1 : NormedSpace ℝ A
inst_2 : Nontrivial A
x : A
r : ℝ
rw :
  extremePoints ℝ (closedBall x r) ⊆ closedBall x r ∧
    Disjoint (extremePoints ℝ (closedBall x r)) (interior (closedBall x r))
⊢ extremePoints ℝ (closedBall x r) ⊆ sphere x r

Tactic:
rw [← closedBall_diff_ball, subset_diff, ← interior_closedBall' _]

Premises used: Set.subset_diff, Metric.closedBall_diff_ball, interior_closedBall'
-- Module: Mathlib.Analysis.Convex.Strict.Extreme
Goal:
A : Type u_1
inst : NormedAddCommGroup A
inst_1 : NormedSpace ℝ A
inst_2 : Nontrivial A
x : A
r : ℝ
⊢ extremePoints ℝ (closedBall x r) ⊆ closedBall x r ∧
    Disjoint (extremePoints ℝ (closedBall x r)) (interior (closedBall x r))

Tactic:
⟨extremePoints_subset, disjoint_interior_extremePoints _ |>.symm⟩

Premises used: Disjoint.symm, And.intro, extremePoints_subset, disjoint_interior_extremePoints
-- Module: Mathlib.Analysis.Convex.Strict.Extreme
Goal:
A : Type u_1
inst : NormedAddCommGroup A
inst_1 : NormedSpace ℝ A
inst_2 : Nontrivial A
x : A
r : ℝ
⊢ extremePoints ℝ (closedBall x r) ⊆ closedBall x r ∧
    Disjoint (extremePoints ℝ (closedBall x r)) (interior (closedBall x r))

Tactic:
exact ⟨extremePoints_subset, disjoint_interior_extremePoints _ |>.symm⟩
-- Module: Mathlib.Analysis.Convex.Strict.Extreme
Goal:
A : Type u_1
inst : NormedAddCommGroup A
inst_1 : NormedSpace ℝ A
inst_2 : Nontrivial A
S : Set A
hS : StrictConvex ℝ S
⊢ extremePoints ℝ S = S \ interior S

Tactic:
antisymm (subset_diff.mpr ⟨extremePoints_subset, disjoint_interior_extremePoints _ |>.symm⟩)
    hS.diff_interior_subset_extremePoints

Premises used: Iff.mpr, StrictConvex.diff_interior_subset_extremePoints, Set.subset_diff, Disjoint.symm, And.intro, antisymm, extremePoints_subset, disjoint_interior_extremePoints
-- Module: Mathlib.Analysis.Convex.Strict.Extreme
Goal:
A : Type u_1
inst : NormedAddCommGroup A
inst_1 : NormedSpace ℝ A
inst_2 : StrictConvexSpace ℝ A
a : A
r : ℝ
hr : r ≠ 0
x : A
hx : x ∈ sphere a r
⊢ x ∈ closedBall a r \ interior (closedBall a r)

Tactic:
rw [← frontier_closedBall _ hr, frontier, closure_closedBall] at hx

Premises used: frontier, Metric.closure_closedBall, frontier_closedBall
-- Module: Mathlib.Analysis.Convex.Strict.Extreme
Goal:
A : Type u_1
inst : NormedAddCommGroup A
inst_1 : NormedSpace ℝ A
inst_2 : StrictConvexSpace ℝ A
a : A
r : ℝ
hr : r ≠ 0
x : A
hx : x ∈ closedBall a r \ interior (closedBall a r)
⊢ x ∈ extremePoints ℝ (closedBall a r)

Tactic:
(_root_.strictConvex_closedBall ℝ _ _).diff_interior_subset_extremePoints hx

Premises used: StrictConvex.diff_interior_subset_extremePoints, Real, Set.Mem, strictConvex_closedBall
-- Module: Mathlib.Analysis.Convex.Strict.Extreme
Goal:
A : Type u_1
inst : NormedAddCommGroup A
inst_1 : NormedSpace ℝ A
inst_2 : StrictConvexSpace ℝ A
a : A
r : ℝ
hr : r ≠ 0
x : A
hx : x ∈ closedBall a r \ interior (closedBall a r)
⊢ x ∈ extremePoints ℝ (closedBall a r)

Tactic:
exact (_root_.strictConvex_closedBall ℝ _ _).diff_interior_subset_extremePoints hx

Premises used: StrictConvex.diff_interior_subset_extremePoints, Real, strictConvex_closedBall
-- Module: Mathlib.Analysis.Convex.Strict.Extreme
Goal:
A : Type u_1
inst : NormedAddCommGroup A
inst_1 : NormedSpace ℝ A
inst_2 : Nontrivial A
x : A
r : ℝ
inst_3 : StrictConvexSpace ℝ A
rw : closedBall x r \ interior (closedBall x r) = sphere x r
rw₁ : closedBall x r \ ball x r = sphere x r
rw₂ rw₃ : sphere x r = sphere x r
⊢ extremePoints ℝ (closedBall x r) = sphere x r

Tactic:
rw [(_root_.strictConvex_closedBall ℝ x r).extremePoints_eq_diff_interior, interior_closedBall',
    closedBall_diff_ball]

Premises used: Real, StrictConvex.extremePoints_eq_diff_interior, strictConvex_closedBall, Metric.closedBall_diff_ball, interior_closedBall'
-- Module: Mathlib.Analysis.Convex.Strict.Extreme
Goal:
a b : ℝ
hab : a ≤ b
rw : sphere ((a + b) / 2) ((b - a) / 2) = {a, b}
⊢ extremePoints ℝ (Icc a b) = {a, b}

Tactic:
rw [Real.Icc_eq_closedBall, StrictConvexSpace.extremePoints_closedBall_eq_sphere]

Premises used: StrictConvexSpace.extremePoints_closedBall_eq_sphere, Real.Icc_eq_closedBall
-- Module: Mathlib.Analysis.Convex.Strict.Extreme
Goal:
a b : ℝ
hab : a ≤ b
⊢ sphere ((a + b) / 2) ((b - a) / 2) = {a, b}

Tactic:
grind [Real.sphere_eq_pair]

Premises used: Real.sphere_eq_pair
-- Module: Mathlib.Analysis.Convex.Strict
Goal:
𝕜 : Type u_1
E : Type u_3
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : TopologicalSpace E
inst_3 : AddCommMonoid E
inst_4 : SMul 𝕜 E
s : Set E
⊢ StrictConvex 𝕜 s ↔ s.Pairwise fun (x y : E) ↦ openSegment 𝕜 x y ⊆ interior s

Tactic:
forall₅_congr fun _ _ _ _ _ => (openSegment_subset_iff 𝕜).symm

Premises used: forall₅_congr, StrictConvex, openSegment_subset_iff, Set.Pairwise, Iff.symm
-- Module: Mathlib.Analysis.Convex.Strict
Goal:
𝕜 : Type u_1
E : Type u_3
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : TopologicalSpace E
inst_3 : AddCommMonoid E
inst_4 : SMul 𝕜 E
s : Set E
x y : E
hs : StrictConvex 𝕜 s
hx : x ∈ s
hy : y ∈ s
h : x ≠ y
⊢ openSegment 𝕜 x y ⊆ interior s

Tactic:
strictConvex_iff_openSegment_subset.1 hs hx hy h

Premises used: strictConvex_iff_openSegment_subset, Iff.mp
-- Module: Mathlib.Analysis.Convex.Strict
Goal:
𝕜 : Type u_1
E : Type u_3
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : TopologicalSpace E
inst_3 : AddCommMonoid E
inst_4 : SMul 𝕜 E
⊢ StrictConvex.{u_1, u_3} 𝕜 (E := E) ∅

Tactic:
pairwise_empty _

Premises used: StrictConvex, Set.pairwise_empty
-- Module: Mathlib.Analysis.Convex.Strict
Goal:
𝕜 : Type u_1
E : Type u_3
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : TopologicalSpace E
inst_3 : AddCommMonoid E
inst_4 : SMul 𝕜 E
x : E
_ :
  Membership.mem (γ := Set E) univ x →
    ∀ ⦃y : E⦄,
      Membership.mem (γ := Set E) univ y →
        x ≠ y →
          (fun (x y : E) ↦
              ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → Membership.mem (γ := Set E) (interior univ) (a • x + b • y))
            x y
⊢ Membership.mem (γ := Set E) univ x →
    ∀ ⦃y : E⦄,
      Membership.mem (γ := Set E) univ y →
        x ≠ y →
          (fun (x y : E) ↦
              ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → Membership.mem (γ := Set E) (interior univ) (a • x + b • y))
            x y

Tactic:
_
-- Module: Mathlib.Analysis.Convex.Strict
Goal:
𝕜 : Type u_1
E : Type u_3
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : TopologicalSpace E
inst_3 : AddCommMonoid E
inst_4 : SMul 𝕜 E
x : E
h : Membership.mem (γ := Set E) univ x
y : E
_ :
  Membership.mem (γ := Set E) univ y →
    x ≠ y →
      (fun (x y : E) ↦
          ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → Membership.mem (γ := Set E) (interior univ) (a • x + b • y))
        x y
⊢ Membership.mem (γ := Set E) univ y →
    x ≠ y →
      (fun (x y : E) ↦
          ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → Membership.mem (γ := Set E) (interior univ) (a • x + b • y))
        x y

Tactic:
_
-- Module: Mathlib.Analysis.Convex.Strict
Goal:
𝕜 : Type u_1
E : Type u_3
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : TopologicalSpace E
inst_3 : AddCommMonoid E
inst_4 : SMul 𝕜 E
x : E
h : Membership.mem (γ := Set E) univ x
y : E
h_1 : Membership.mem (γ := Set E) univ y
_ : x ≠ y → ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → Membership.mem (γ := Set E) (interior univ) (a • x + b • y)
⊢ x ≠ y →
    (fun (x y : E) ↦
        ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → Membership.mem (γ := Set E) (interior univ) (a • x + b • y))
      x y

Tactic:
_
-- Module: Mathlib.Analysis.Convex.Strict
Goal:
𝕜 : Type u_1
E : Type u_3
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : TopologicalSpace E
inst_3 : AddCommMonoid E
inst_4 : SMul 𝕜 E
x : E
h : Membership.mem (γ := Set E) univ x
y : E
h_1 : Membership.mem (γ := Set E) univ y
h_2 : x ≠ y
a b : 𝕜
_ : 0 < a → 0 < b → a + b = 1 → Membership.mem (γ := Set E) (interior univ) (a • x + b • y)
⊢ 0 < a → 0 < b → a + b = 1 → Membership.mem (γ := Set E) (interior univ) (a • x + b • y)

Tactic:
_
-- Module: Mathlib.Analysis.Convex.Strict
Goal:
𝕜 : Type u_1
E : Type u_3
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : TopologicalSpace E
inst_3 : AddCommMonoid E
inst_4 : SMul 𝕜 E
x : E
h : Membership.mem (γ := Set E) univ x
y : E
h_1 : Membership.mem (γ := Set E) univ y
h_2 : x ≠ y
a b : 𝕜
h_3 : 0 < a
_ : 0 < b → a + b = 1 → Membership.mem (γ := Set E) (interior univ) (a • x + b • y)
⊢ 0 < b → a + b = 1 → Membership.mem (γ := Set E) (interior univ) (a • x + b • y)

Tactic:
_
-- Module: Mathlib.Analysis.Convex.Strict
Goal:
𝕜 : Type u_1
E : Type u_3
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : TopologicalSpace E
inst_3 : AddCommMonoid E
inst_4 : SMul 𝕜 E
x : E
h : Membership.mem (γ := Set E) univ x
y : E
h_1 : Membership.mem (γ := Set E) univ y
h_2 : x ≠ y
a b : 𝕜
h_3 : 0 < a
h_4 : 0 < b
_ : a + b = 1 → Membership.mem (γ := Set E) (interior univ) (a • x + b • y)
⊢ a + b = 1 → Membership.mem (γ := Set E) (interior univ) (a • x + b • y)

Tactic:
_
-- Module: Mathlib.Analysis.Convex.Strict
Goal:
𝕜 : Type u_1
E : Type u_3
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : TopologicalSpace E
inst_3 : AddCommMonoid E
inst_4 : SMul 𝕜 E
x : E
h : Membership.mem (γ := Set E) univ x
y : E
h_1 : Membership.mem (γ := Set E) univ y
h_2 : x ≠ y
a b : 𝕜
h_3 : 0 < a
h_4 : 0 < b
h_5 : a + b = 1
rw : Membership.mem (γ := Set E) univ (a • x + b • y)
⊢ Membership.mem (γ := Set E) (interior univ) (a • x + b • y)

Tactic:
rw [interior_univ]

Premises used: interior_univ
-- Module: Mathlib.Analysis.Convex.Strict
Goal:
𝕜 : Type u_1
E : Type u_3
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : TopologicalSpace E
inst_3 : AddCommMonoid E
inst_4 : SMul 𝕜 E
x : E
h : Membership.mem (γ := Set E) univ x
y : E
h_1 : Membership.mem (γ := Set E) univ y
h_2 : x ≠ y
a b : 𝕜
h_3 : 0 < a
h_4 : 0 < b
h_5 : a + b = 1
⊢ Membership.mem (γ := Set E) univ (a • x + b • y)

Tactic:
mem_univ _

Premises used: Set.mem_univ
-- Module: Mathlib.Analysis.Convex.Strict
Goal:
𝕜 : Type u_1
E : Type u_3
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : TopologicalSpace E
inst_3 : AddCommMonoid E
inst_4 : SMul 𝕜 E
x : E
h : Membership.mem (γ := Set E) univ x
y : E
h_1 : Membership.mem (γ := Set E) univ y
h_2 : x ≠ y
a b : 𝕜
h_3 : 0 < a
h_4 : 0 < b
h_5 : a + b = 1
⊢ Membership.mem (γ := Set E) univ (a • x + b • y)

Tactic:
exact mem_univ _

Premises used: Set.mem_univ
-- Module: Mathlib.Analysis.Convex.Strict
Goal:
𝕜 : Type u_1
E : Type u_3
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : TopologicalSpace E
inst_3 : AddCommMonoid E
inst_4 : SMul 𝕜 E
s : Set E
x y : E
a b : 𝕜
hs : StrictConvex 𝕜 s
hx : x ∈ s
hy : y ∈ s
ha : 0 < a
hb : 0 < b
hab : a + b = 1
h : a • x + b • y ∉ interior s
⊢ x = y

Tactic:
hs.eq hx hy fun H => h <| H ha hb hab

Premises used: Set.Pairwise.eq
-- Module: Mathlib.Analysis.Convex.Strict
Goal:
𝕜 : Type u_1
E : Type u_3
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : TopologicalSpace E
inst_3 : AddCommMonoid E
inst_4 : SMul 𝕜 E
s t : Set E
hs : StrictConvex 𝕜 s
ht : StrictConvex 𝕜 t
x : E
hx : x ∈ s ∩ t
y : E
hy : y ∈ s ∩ t
hxy : x ≠ y
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
rw : a • x + b • y ∈ interior s ∩ interior t
⊢ a • x + b • y ∈ interior (s ∩ t)

Tactic:
rw [interior_inter]

Premises used: interior_inter