mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Geometry.Convex.ConvexSpace.Module

Goal state before:
pp: F : Type u_1
R : Type u_2
M : Type u_3
inst✝⁹ : Semiring R
inst✝⁸ : PartialOrder R
inst✝⁷ : IsStrictOrderedRing R
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module R M
inst✝⁴ : SetLike F M
inst✝³ : AddSubmonoidClass F M
inst✝² : SMulMemClass F R M
inst✝¹ : ConvexSpace R M
inst✝ : IsModuleConvexSpace R M
S : F
w : StdSimplex R M
hw : ↑w.weights.support ⊆ ↑S
⊢ (w.weights.sum fun m r ↦ r • m) ∈ ↑S

Tactic:
]

Goal state after:
F : Type u_1
R : Type u_2
M : Type u_3
inst✝⁹ : Semiring R
inst✝⁸ : PartialOrder R
inst✝⁷ : IsStrictOrderedRing R
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module R M
inst✝⁴ : SetLike F M
inst✝³ : AddSubmonoidClass F M
inst✝² : SMulMemClass F R M
inst✝¹ : ConvexSpace R M
inst✝ : IsModuleConvexSpace R M
S : F
w : StdSimplex R M
hw : ↑w.weights.support ⊆ ↑S
⊢ (w.weights.sum fun m r ↦ r • m) ∈ ↑S
Module: Mathlib.Analysis.Convex.MetricSpace

Goal state before:
pp: case neg.inr
X : Type u_2
inst✝³ : ConvexSpace ℝ X
inst✝² : MetricSpace X
inst✝¹ : IsConvexDist X
T : Type u_3
inst✝ : TopologicalSpace T
f : T → ℝ
hf : Continuous f
hf0 : ∀ (t : T), 0 ≤ f t
hf1 : ∀ (t : T), f t ≤ 1
x y : T → X
hx : ContinuousOn x (f ⁻¹' {0}ᶜ)
hy : ContinuousOn y (f ⁻¹' {1}ᶜ)
hx' : Bornology.IsBounded (Set.range x)
hy' : Bornology.IsBounded (Set.range y)
D : ℝ
hD' : 0 < D
hD : ∀ (t₁ t₂ : T), dist (x t₁) (y t₂) ≤ D
t : T
ht✝ : f t ∉ Set.Ioo 0 1
ht : f t = 1
⊢ ∀ (i : ℝ),
    0 < i → ∀ᶠ (x_1 : T) in nhds t, convexCombPair (f x_1) (1 - f x_1) ⋯ ⋯ ⋯ (x x_1) (y x_1) ∈ Metric.ball (x t) i

Tactic:
]

Goal state after:
case neg.inr
X : Type u_2
inst✝³ : ConvexSpace ℝ X
inst✝² : MetricSpace X
inst✝¹ : IsConvexDist X
T : Type u_3
inst✝ : TopologicalSpace T
f : T → ℝ
hf : Continuous f
hf0 : ∀ (t : T), 0 ≤ f t
hf1 : ∀ (t : T), f t ≤ 1
x y : T → X
hx : ContinuousOn x (f ⁻¹' {0}ᶜ)
hy : ContinuousOn y (f ⁻¹' {1}ᶜ)
hx' : Bornology.IsBounded (Set.range x)
hy' : Bornology.IsBounded (Set.range y)
D : ℝ
hD' : 0 < D
hD : ∀ (t₁ t₂ : T), dist (x t₁) (y t₂) ≤ D
t : T
ht✝ : f t ∉ Set.Ioo 0 1
ht : f t = 1
⊢ ∀ (i : ℝ),
    0 < i → ∀ᶠ (x_1 : T) in nhds t, convexCombPair (f x_1) (1 - f x_1) ⋯ ⋯ ⋯ (x x_1) (y x_1) ∈ Metric.ball (x t) i
Module: Mathlib.Analysis.Convex.Radon

Goal state before:
pp: case neg
𝕜 : Type u_2
E : Type u_3
inst✝⁵ : Field 𝕜
inst✝⁴ : LinearOrder 𝕜
inst✝³ : IsStrictOrderedRing 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
n k : ℕ
h_card : finrank 𝕜 E + 1 ≤ k
hk :
  ∀ {ι : Type u_1} {F : ι → Set E} {s : Finset ι},
    (∀ i ∈ s, Convex 𝕜 (F i)) →
      (∀ I ⊆ s, #I ≤ finrank 𝕜 E + 1 → (⋂ i ∈ I, F i).Nonempty) → #s = k → (⋂ i ∈ s, F i).Nonempty
ι : Type u_1
F : ι → Set E
s : Finset ι
h_convex : ∀ i ∈ s, Convex 𝕜 (F i)
h_inter : ∀ I ⊆ s, #I ≤ finrank 𝕜 E + 1 → (⋂ i ∈ I, F i).Nonempty
hn : #s = k + 1
a : ↥s → E := fun i ↦ ⋯.some
h_ind : ¬AffineIndependent 𝕜 a
I : Set ↥s
p : E
hp_I : p ∈ (convexHull 𝕜) (a '' I)
hp_Ic : p ∈ (convexHull 𝕜) (a '' Iᶜ)
i : ↥s
this : ∀ (J : Set ↥s), i ∈ J → (convexHull 𝕜) (a '' Jᶜ) ⊆ F ↑i
h : i ∉ I
⊢ p ∈ (convexHull 𝕜) (a '' I)

Tactic:
]

Goal state after:
case neg
𝕜 : Type u_2
E : Type u_3
inst✝⁵ : Field 𝕜
inst✝⁴ : LinearOrder 𝕜
inst✝³ : IsStrictOrderedRing 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
n k : ℕ
h_card : finrank 𝕜 E + 1 ≤ k
hk :
  ∀ {ι : Type u_1} {F : ι → Set E} {s : Finset ι},
    (∀ i ∈ s, Convex 𝕜 (F i)) →
      (∀ I ⊆ s, #I ≤ finrank 𝕜 E + 1 → (⋂ i ∈ I, F i).Nonempty) → #s = k → (⋂ i ∈ s, F i).Nonempty
ι : Type u_1
F : ι → Set E
s : Finset ι
h_convex : ∀ i ∈ s, Convex 𝕜 (F i)
h_inter : ∀ I ⊆ s, #I ≤ finrank 𝕜 E + 1 → (⋂ i ∈ I, F i).Nonempty
hn : #s = k + 1
a : ↥s → E := fun i ↦ ⋯.some
h_ind : ¬AffineIndependent 𝕜 a
I : Set ↥s
p : E
hp_I : p ∈ (convexHull 𝕜) (a '' I)
hp_Ic : p ∈ (convexHull 𝕜) (a '' Iᶜ)
i : ↥s
this : ∀ (J : Set ↥s), i ∈ J → (convexHull 𝕜) (a '' Jᶜ) ⊆ F ↑i
h : i ∉ I
⊢ p ∈ (convexHull 𝕜) (a '' I)
Module: Mathlib.Geometry.Convex.ConvexSpace.Module

Goal state before:
pp: R : Type u_2
M : Type u_3
inst✝⁶ : Semiring R
inst✝⁵ : PartialOrder R
inst✝⁴ : IsStrictOrderedRing R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : ConvexSpace R M
inst✝ : IsModuleConvexSpace R M
x y : M
s t : Set M
hs : IsStarConvexSet R x s
ht : IsStarConvexSet R y t
⊢ IsStarConvexSet R (x + y) ((fun x ↦ x.1 + x.2) '' s ×ˢ t)

Tactic:
]

Goal state after:
R : Type u_2
M : Type u_3
inst✝⁶ : Semiring R
inst✝⁵ : PartialOrder R
inst✝⁴ : IsStrictOrderedRing R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : ConvexSpace R M
inst✝ : IsModuleConvexSpace R M
x y : M
s t : Set M
hs : IsStarConvexSet R x s
ht : IsStarConvexSet R y t
⊢ IsStarConvexSet R (x + y) ((fun x ↦ x.1 + x.2) '' s ×ˢ t)
Module: Mathlib.Geometry.Convex.ConvexSpace.Module

Goal state before:
pp: R : Type u_2
M : Type u_3
inst✝⁶ : Semiring R
inst✝⁵ : PartialOrder R
inst✝⁴ : IsStrictOrderedRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : ConvexSpace R M
inst✝ : IsModuleConvexSpace R M
x : M
s : Set M
hs : IsStarConvexSet R x s
⊢ IsStarConvexSet R (-x) ((fun x ↦ -x) '' s)

Tactic:
]

Goal state after:
R : Type u_2
M : Type u_3
inst✝⁶ : Semiring R
inst✝⁵ : PartialOrder R
inst✝⁴ : IsStrictOrderedRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : ConvexSpace R M
inst✝ : IsModuleConvexSpace R M
x : M
s : Set M
hs : IsStarConvexSet R x s
⊢ IsStarConvexSet R (-x) ((fun x ↦ -x) '' s)
Module: Mathlib.Geometry.Convex.ConvexSpace.Module

Goal state before:
pp: R : Type u_2
M : Type u_3
inst✝⁶ : Semiring R
inst✝⁵ : PartialOrder R
inst✝⁴ : IsStrictOrderedRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : ConvexSpace R M
inst✝ : IsModuleConvexSpace R M
x y : M
s t : Set M
hs : IsStarConvexSet R x s
ht : IsStarConvexSet R y t
⊢ IsStarConvexSet R (x - y) ((fun x ↦ x.1 - x.2) '' s ×ˢ t)

Tactic:
]

Goal state after:
R : Type u_2
M : Type u_3
inst✝⁶ : Semiring R
inst✝⁵ : PartialOrder R
inst✝⁴ : IsStrictOrderedRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : ConvexSpace R M
inst✝ : IsModuleConvexSpace R M
x y : M
s t : Set M
hs : IsStarConvexSet R x s
ht : IsStarConvexSet R y t
⊢ IsStarConvexSet R (x - y) ((fun x ↦ x.1 - x.2) '' s ×ˢ t)
Module: Mathlib.Analysis.Convex.MetricSpace

Goal state before:
pp: X : Type u_2
inst✝³ : ConvexSpace ℝ X
inst✝² : MetricSpace X
inst✝¹ : IsConvexDist X
T : Type u_3
inst✝ : TopologicalSpace T
f : T → ℝ
hf : Continuous f
hf0 : ∀ (t : T), 0 ≤ f t
hf1 : ∀ (t : T), f t ≤ 1
x y : T → X
hx : ContinuousOn x (f ⁻¹' {0}ᶜ)
hy : ContinuousOn y (f ⁻¹' {1}ᶜ)
hx' : Bornology.IsBounded (Set.range x)
hy' : Bornology.IsBounded (Set.range y)
D : ℝ
hD' : 0 < D
hD : ∀ (t₁ t₂ : T), dist (x t₁) (y t₂) ≤ D
t : T
ht✝ : f t ∉ Set.Ioo 0 1
ht : f t = 1
r : ℝ
hr : 0 < r
j : T
hj : dist (x j) (x t) < r / 3
hj' : |f j - 1| < r / D / 3
⊢ f j * dist (x j) (x t) + (1 - f j) * dist (y j) (y j) +
      dist (convexCombPair (f j) (1 - f j) ⋯ ⋯ ⋯ (x t) (y j)) (x t) <
    r

Tactic:
]

Goal state after:
X : Type u_2
inst✝³ : ConvexSpace ℝ X
inst✝² : MetricSpace X
inst✝¹ : IsConvexDist X
T : Type u_3
inst✝ : TopologicalSpace T
f : T → ℝ
hf : Continuous f
hf0 : ∀ (t : T), 0 ≤ f t
hf1 : ∀ (t : T), f t ≤ 1
x y : T → X
hx : ContinuousOn x (f ⁻¹' {0}ᶜ)
hy : ContinuousOn y (f ⁻¹' {1}ᶜ)
hx' : Bornology.IsBounded (Set.range x)
hy' : Bornology.IsBounded (Set.range y)
D : ℝ
hD' : 0 < D
hD : ∀ (t₁ t₂ : T), dist (x t₁) (y t₂) ≤ D
t : T
ht✝ : f t ∉ Set.Ioo 0 1
ht : f t = 1
r : ℝ
hr : 0 < r
j : T
hj : dist (x j) (x t) < r / 3
hj' : |f j - 1| < r / D / 3
⊢ f j * dist (x j) (x t) + (1 - f j) * dist (y j) (y j) +
      dist (convexCombPair (f j) (1 - f j) ⋯ ⋯ ⋯ (x t) (y j)) (x t) <
    r
Module: Mathlib.Analysis.Convex.SimplicialComplex.Basic

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝³ : Ring 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
K : SimplicialComplex 𝕜 E
s t : Finset E
hs : s ∈ K.faces
ht : t ∈ K.faces
h :
  ((convexHull 𝕜) ↑s ∩ (convexHull 𝕜) ↑t).Nonempty ∧
    ∀ u ∈ K.faces, (convexHull 𝕜) ↑s ∩ (convexHull 𝕜) ↑t ≠ (convexHull 𝕜) ↑u
⊢ False

Tactic:
]

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝³ : Ring 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
K : SimplicialComplex 𝕜 E
s t : Finset E
hs : s ∈ K.faces
ht : t ∈ K.faces
h :
  ((convexHull 𝕜) ↑s ∩ (convexHull 𝕜) ↑t).Nonempty ∧
    ∀ u ∈ K.faces, (convexHull 𝕜) ↑s ∩ (convexHull 𝕜) ↑t ≠ (convexHull 𝕜) ↑u
⊢ False
Module: Mathlib.Analysis.Convex.SimplicialComplex.Basic

Goal state before:
pp: case refine_2
𝕜 : Type u_1
E : Type u_2
inst✝³ : Ring 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
K : SimplicialComplex 𝕜 E
s t : Finset E
hs : s ∈ K.faces
ht : t ∈ K.faces
h :
  ((convexHull 𝕜) ↑s ∩ (convexHull 𝕜) ↑t).Nonempty ∧
    ∀ u ∈ K.faces, (convexHull 𝕜) ↑s ∩ (convexHull 𝕜) ↑t ≠ (convexHull 𝕜) ↑u
⊢ (convexHull 𝕜) (↑s ∩ ↑t) = (convexHull 𝕜) (↑s ∩ ↑t)

Tactic:
]

Goal state after:
Module: Mathlib.Analysis.Convex.MetricSpace

Goal state before:
pp: X : Type u_2
inst✝³ : ConvexSpace ℝ X
inst✝² : MetricSpace X
inst✝¹ : IsConvexDist X
T : Type u_3
inst✝ : TopologicalSpace T
f : T → ℝ
hf : Continuous f
hf0 : ∀ (t : T), 0 ≤ f t
hf1 : ∀ (t : T), f t ≤ 1
x y : T → X
hx : ContinuousOn x (f ⁻¹' {0}ᶜ)
hy : ContinuousOn y (f ⁻¹' {1}ᶜ)
hx' : Bornology.IsBounded (Set.range x)
hy' : Bornology.IsBounded (Set.range y)
D : ℝ
hD' : 0 < D
hD : ∀ (t₁ t₂ : T), dist (x t₁) (y t₂) ≤ D
t : T
ht✝ : f t ∉ Set.Ioo 0 1
ht : f t = 1
r : ℝ
hr : 0 < r
j : T
hj : dist (x j) (x t) < r / 3
hj' : 1 - f j < r / D / 3
⊢ f j * dist (x j) (x t) + (1 - f j) * dist (x t) (y j) < r

Tactic:
]

Goal state after:
X : Type u_2
inst✝³ : ConvexSpace ℝ X
inst✝² : MetricSpace X
inst✝¹ : IsConvexDist X
T : Type u_3
inst✝ : TopologicalSpace T
f : T → ℝ
hf : Continuous f
hf0 : ∀ (t : T), 0 ≤ f t
hf1 : ∀ (t : T), f t ≤ 1
x y : T → X
hx : ContinuousOn x (f ⁻¹' {0}ᶜ)
hy : ContinuousOn y (f ⁻¹' {1}ᶜ)
hx' : Bornology.IsBounded (Set.range x)
hy' : Bornology.IsBounded (Set.range y)
D : ℝ
hD' : 0 < D
hD : ∀ (t₁ t₂ : T), dist (x t₁) (y t₂) ≤ D
t : T
ht✝ : f t ∉ Set.Ioo 0 1
ht : f t = 1
r : ℝ
hr : 0 < r
j : T
hj : dist (x j) (x t) < r / 3
hj' : 1 - f j < r / D / 3
⊢ f j * dist (x j) (x t) + (1 - f j) * dist (x t) (y j) < r
Module: Mathlib.Analysis.Convex.Radon

Goal state before:
pp: case h
𝕜 : Type u_2
E : Type u_3
inst✝⁵ : Field 𝕜
inst✝⁴ : LinearOrder 𝕜
inst✝³ : IsStrictOrderedRing 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
n k : ℕ
h_card : finrank 𝕜 E + 1 ≤ k
hk :
  ∀ {ι : Type u_1} {F : ι → Set E} {s : Finset ι},
    (∀ i ∈ s, Convex 𝕜 (F i)) →
      (∀ I ⊆ s, #I ≤ finrank 𝕜 E + 1 → (⋂ i ∈ I, F i).Nonempty) → #s = k → (⋂ i ∈ s, F i).Nonempty
ι : Type u_1
F : ι → Set E
s : Finset ι
h_convex : ∀ i ∈ s, Convex 𝕜 (F i)
h_inter : ∀ I ⊆ s, #I ≤ finrank 𝕜 E + 1 → (⋂ i ∈ I, F i).Nonempty
hn : #s = k + 1
a : ↥s → E := fun i ↦ ⋯.some
h_ind : ¬AffineIndependent 𝕜 a
I : Set ↥s
p : E
hp_I : p ∈ (convexHull 𝕜) (a '' I)
hp_Ic : p ∈ (convexHull 𝕜) (a '' Iᶜ)
i : ↥s
J : Set ↥s
hi : i ∈ J
⊢ a '' Jᶜ ⊆ F ↑i

Tactic:
]

Goal state after:
case h
𝕜 : Type u_2
E : Type u_3
inst✝⁵ : Field 𝕜
inst✝⁴ : LinearOrder 𝕜
inst✝³ : IsStrictOrderedRing 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
n k : ℕ
h_card : finrank 𝕜 E + 1 ≤ k
hk :
  ∀ {ι : Type u_1} {F : ι → Set E} {s : Finset ι},
    (∀ i ∈ s, Convex 𝕜 (F i)) →
      (∀ I ⊆ s, #I ≤ finrank 𝕜 E + 1 → (⋂ i ∈ I, F i).Nonempty) → #s = k → (⋂ i ∈ s, F i).Nonempty
ι : Type u_1
F : ι → Set E
s : Finset ι
h_convex : ∀ i ∈ s, Convex 𝕜 (F i)
h_inter : ∀ I ⊆ s, #I ≤ finrank 𝕜 E + 1 → (⋂ i ∈ I, F i).Nonempty
hn : #s = k + 1
a : ↥s → E := fun i ↦ ⋯.some
h_ind : ¬AffineIndependent 𝕜 a
I : Set ↥s
p : E
hp_I : p ∈ (convexHull 𝕜) (a '' I)
hp_Ic : p ∈ (convexHull 𝕜) (a '' Iᶜ)
i : ↥s
J : Set ↥s
hi : i ∈ J
⊢ a '' Jᶜ ⊆ F ↑i
Module: Mathlib.Analysis.Convex.Radon

Goal state before:
pp: case h
𝕜 : Type u_2
E : Type u_3
inst✝⁵ : Field 𝕜
inst✝⁴ : LinearOrder 𝕜
inst✝³ : IsStrictOrderedRing 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
n k : ℕ
h_card : finrank 𝕜 E + 1 ≤ k
hk :
  ∀ {ι : Type u_1} {F : ι → Set E} {s : Finset ι},
    (∀ i ∈ s, Convex 𝕜 (F i)) →
      (∀ I ⊆ s, #I ≤ finrank 𝕜 E + 1 → (⋂ i ∈ I, F i).Nonempty) → #s = k → (⋂ i ∈ s, F i).Nonempty
ι : Type u_1
F : ι → Set E
s : Finset ι
h_convex : ∀ i ∈ s, Convex 𝕜 (F i)
h_inter : ∀ I ⊆ s, #I ≤ finrank 𝕜 E + 1 → (⋂ i ∈ I, F i).Nonempty
hn : #s = k + 1
a : ↥s → E := fun i ↦ ⋯.some
h_ind : ¬AffineIndependent 𝕜 a
I : Set ↥s
p : E
hp_I : p ∈ (convexHull 𝕜) (a '' I)
hp_Ic : p ∈ (convexHull 𝕜) (a '' Iᶜ)
i : ↥s
J : Set ↥s
hi : i ∈ J
v : E
j : ↥s
hj : j ∈ Jᶜ
hj_v : a j = v
⊢ a j ∈ F ↑i

Tactic:
]

Goal state after:
case h
𝕜 : Type u_2
E : Type u_3
inst✝⁵ : Field 𝕜
inst✝⁴ : LinearOrder 𝕜
inst✝³ : IsStrictOrderedRing 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
n k : ℕ
h_card : finrank 𝕜 E + 1 ≤ k
hk :
  ∀ {ι : Type u_1} {F : ι → Set E} {s : Finset ι},
    (∀ i ∈ s, Convex 𝕜 (F i)) →
      (∀ I ⊆ s, #I ≤ finrank 𝕜 E + 1 → (⋂ i ∈ I, F i).Nonempty) → #s = k → (⋂ i ∈ s, F i).Nonempty
ι : Type u_1
F : ι → Set E
s : Finset ι
h_convex : ∀ i ∈ s, Convex 𝕜 (F i)
h_inter : ∀ I ⊆ s, #I ≤ finrank 𝕜 E + 1 → (⋂ i ∈ I, F i).Nonempty
hn : #s = k + 1
a : ↥s → E := fun i ↦ ⋯.some
h_ind : ¬AffineIndependent 𝕜 a
I : Set ↥s
p : E
hp_I : p ∈ (convexHull 𝕜) (a '' I)
hp_Ic : p ∈ (convexHull 𝕜) (a '' Iᶜ)
i : ↥s
J : Set ↥s
hi : i ∈ J
v : E
j : ↥s
hj : j ∈ Jᶜ
hj_v : a j = v
⊢ a j ∈ F ↑i
Module: Mathlib.Analysis.Convex.MetricSpace

Goal state before:
pp: X : Type u_2
inst✝³ : ConvexSpace ℝ X
inst✝² : MetricSpace X
inst✝¹ : IsConvexDist X
T : Type u_3
inst✝ : TopologicalSpace T
f : T → ℝ
hf : Continuous f
hf0 : ∀ (t : T), 0 ≤ f t
hf1 : ∀ (t : T), f t ≤ 1
x y : T → X
hx : ContinuousOn x (f ⁻¹' {0}ᶜ)
hy : ContinuousOn y (f ⁻¹' {1}ᶜ)
hx' : Bornology.IsBounded (Set.range x)
hy' : Bornology.IsBounded (Set.range y)
D : ℝ
hD' : 0 < D
hD : ∀ (t₁ t₂ : T), dist (x t₁) (y t₂) ≤ D
t : T
ht✝ : f t ∉ Set.Ioo 0 1
ht : f t = 1
r : ℝ
hr : 0 < r
j : T
hj : dist (x j) (x t) < r / 3
hj' : 1 - f j < r / D / 3
⊢ 1 * (r / 3) + r / D / 3 * D < r

pp: case ha
X : Type u_2
inst✝³ : ConvexSpace ℝ X
inst✝² : MetricSpace X
inst✝¹ : IsConvexDist X
T : Type u_3
inst✝ : TopologicalSpace T
f : T → ℝ
hf : Continuous f
hf0 : ∀ (t : T), 0 ≤ f t
hf1 : ∀ (t : T), f t ≤ 1
x y : T → X
hx : ContinuousOn x (f ⁻¹' {0}ᶜ)
hy : ContinuousOn y (f ⁻¹' {1}ᶜ)
hx' : Bornology.IsBounded (Set.range x)
hy' : Bornology.IsBounded (Set.range y)
D : ℝ
hD' : 0 < D
hD : ∀ (t₁ t₂ : T), dist (x t₁) (y t₂) ≤ D
t : T
ht✝ : f t ∉ Set.Ioo 0 1
ht : f t = 1
r : ℝ
hr : 0 < r
j : T
hj : dist (x j) (x t) < r / 3
hj' : 1 - f j < r / D / 3
⊢ 0 ≤ f j

Tactic:
]

Goal state after:
X : Type u_2
inst✝³ : ConvexSpace ℝ X
inst✝² : MetricSpace X
inst✝¹ : IsConvexDist X
T : Type u_3
inst✝ : TopologicalSpace T
f : T → ℝ
hf : Continuous f
hf0 : ∀ (t : T), 0 ≤ f t
hf1 : ∀ (t : T), f t ≤ 1
x y : T → X
hx : ContinuousOn x (f ⁻¹' {0}ᶜ)
hy : ContinuousOn y (f ⁻¹' {1}ᶜ)
hx' : Bornology.IsBounded (Set.range x)
hy' : Bornology.IsBounded (Set.range y)
D : ℝ
hD' : 0 < D
hD : ∀ (t₁ t₂ : T), dist (x t₁) (y t₂) ≤ D
t : T
ht✝ : f t ∉ Set.Ioo 0 1
ht : f t = 1
r : ℝ
hr : 0 < r
j : T
hj : dist (x j) (x t) < r / 3
hj' : 1 - f j < r / D / 3
⊢ 1 * (r / 3) + r / D / 3 * D < r

case ha
X : Type u_2
inst✝³ : ConvexSpace ℝ X
inst✝² : MetricSpace X
inst✝¹ : IsConvexDist X
T : Type u_3
inst✝ : TopologicalSpace T
f : T → ℝ
hf : Continuous f
hf0 : ∀ (t : T), 0 ≤ f t
hf1 : ∀ (t : T), f t ≤ 1
x y : T → X
hx : ContinuousOn x (f ⁻¹' {0}ᶜ)
hy : ContinuousOn y (f ⁻¹' {1}ᶜ)
hx' : Bornology.IsBounded (Set.range x)
hy' : Bornology.IsBounded (Set.range y)
D : ℝ
hD' : 0 < D
hD : ∀ (t₁ t₂ : T), dist (x t₁) (y t₂) ≤ D
t : T
ht✝ : f t ∉ Set.Ioo 0 1
ht : f t = 1
r : ℝ
hr : 0 < r
j : T
hj : dist (x j) (x t) < r / 3
hj' : 1 - f j < r / D / 3
⊢ 0 ≤ f j
Module: Mathlib.Analysis.Convex.SimplicialComplex.Basic

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝³ : Ring 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
K : SimplicialComplex 𝕜 E
s : Finset E
x : E
hx : x ∈ K.vertices
hs : s ∈ K.faces
h✝ : x ∈ (convexHull 𝕜) ↑s
h : x ∈ ∅
H : ¬x ∈ s
⊢ False

Tactic:
]

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝³ : Ring 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
K : SimplicialComplex 𝕜 E
s : Finset E
x : E
hx : x ∈ K.vertices
hs : s ∈ K.faces
h✝ : x ∈ (convexHull 𝕜) ↑s
h : x ∈ ∅
H : ¬x ∈ s
⊢ False
Module: Mathlib.Analysis.Convex.SimplicialComplex.Basic

Goal state before:
pp: case refine_2
𝕜 : Type u_1
E : Type u_2
inst✝³ : Ring 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
K : SimplicialComplex 𝕜 E
s : Finset E
hs✝ : s ∈ K.faces
t : Finset E
ht : t ∈ K.faces ∧ t ⊂ t
hs : s ∈ K.faces
hs' : ∀ ⦃t : Finset E⦄, t ∈ K.faces → s ⊆ t → s = t
this : s = t
⊢ False

Tactic:
]

Goal state after:
case refine_2
𝕜 : Type u_1
E : Type u_2
inst✝³ : Ring 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
K : SimplicialComplex 𝕜 E
s : Finset E
hs✝ : s ∈ K.faces
t : Finset E
ht : t ∈ K.faces ∧ t ⊂ t
hs : s ∈ K.faces
hs' : ∀ ⦃t : Finset E⦄, t ∈ K.faces → s ⊆ t → s = t
this : s = t
⊢ False
Module: Mathlib.Analysis.Convex.Radon

Goal state before:
pp: 𝕜 : Type u_2
E : Type u_3
inst✝⁵ : Field 𝕜
inst✝⁴ : LinearOrder 𝕜
inst✝³ : IsStrictOrderedRing 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
F : Finset (Set E)
h_convex : ∀ X ∈ F, Convex 𝕜 X
h_inter : ∀ G ⊆ F, #G ≤ finrank 𝕜 E + 1 → (⋂₀ ↑G).Nonempty
⊢ (⋂ X ∈ F, X).Nonempty

Tactic:
]

Goal state after:
𝕜 : Type u_2
E : Type u_3
inst✝⁵ : Field 𝕜
inst✝⁴ : LinearOrder 𝕜
inst✝³ : IsStrictOrderedRing 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
F : Finset (Set E)
h_convex : ∀ X ∈ F, Convex 𝕜 X
h_inter : ∀ G ⊆ F, #G ≤ finrank 𝕜 E + 1 → (⋂₀ ↑G).Nonempty
⊢ (⋂ X ∈ F, X).Nonempty
Module: Mathlib.Analysis.Convex.MetricSpace

Goal state before:
pp: I : Type u_1
X : Type u_2
inst✝⁶ : ConvexSpace ℝ X
inst✝⁵ : MetricSpace X
inst✝⁴ : IsConvexDist X
V : Type u_3
P : Type u_4
inst✝³ : NormedAddCommGroup V
inst✝² : NormedSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
f : StdSimplex ℝ (P × P)
p : P := ⋯.some
⊢ dist (((f.weights.support.weightedVSubOfPoint Prod.fst p) fun i ↦ (fun x r ↦ r) i (f.weights i)) +ᵥ p)
      (((f.weights.support.weightedVSubOfPoint Prod.snd p) fun i ↦ (fun x r ↦ r) i (f.weights i)) +ᵥ p) ≤
    iConvexComb f fun x ↦ dist x.1 x.2

Tactic:
]

Goal state after:
I : Type u_1
X : Type u_2
inst✝⁶ : ConvexSpace ℝ X
inst✝⁵ : MetricSpace X
inst✝⁴ : IsConvexDist X
V : Type u_3
P : Type u_4
inst✝³ : NormedAddCommGroup V
inst✝² : NormedSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
f : StdSimplex ℝ (P × P)
p : P := ⋯.some
⊢ dist (((f.weights.support.weightedVSubOfPoint Prod.fst p) fun i ↦ (fun x r ↦ r) i (f.weights i)) +ᵥ p)
      (((f.weights.support.weightedVSubOfPoint Prod.snd p) fun i ↦ (fun x r ↦ r) i (f.weights i)) +ᵥ p) ≤
    iConvexComb f fun x ↦ dist x.1 x.2
Module: Mathlib.Analysis.Convex.MetricSpace

Goal state before:
pp: I : Type u_1
X : Type u_2
inst✝⁶ : ConvexSpace ℝ X
inst✝⁵ : MetricSpace X
inst✝⁴ : IsConvexDist X
V : Type u_3
P : Type u_4
inst✝³ : NormedAddCommGroup V
inst✝² : NormedSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
f : StdSimplex ℝ (P × P)
p : P := ⋯.some
⊢ ∑ i ∈ f.weights.support, ‖f.weights i • (i.1 -ᵥ i.2)‖ ≤ ∑ a ∈ f.weights.support, f.weights a * ‖a.1 -ᵥ a.2‖

Tactic:
]

Goal state after:
I : Type u_1
X : Type u_2
inst✝⁶ : ConvexSpace ℝ X
inst✝⁵ : MetricSpace X
inst✝⁴ : IsConvexDist X
V : Type u_3
P : Type u_4
inst✝³ : NormedAddCommGroup V
inst✝² : NormedSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
f : StdSimplex ℝ (P × P)
p : P := ⋯.some
⊢ ∑ i ∈ f.weights.support, ‖f.weights i • (i.1 -ᵥ i.2)‖ ≤ ∑ a ∈ f.weights.support, f.weights a * ‖a.1 -ᵥ a.2‖
Module: Mathlib.Analysis.Convex.Radon

Goal state before:
pp: 𝕜 : Type u_2
E : Type u_3
inst✝⁵ : Field 𝕜
inst✝⁴ : LinearOrder 𝕜
inst✝³ : IsStrictOrderedRing 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
F : Finset (Set E)
h_convex : ∀ X ∈ F, Convex 𝕜 X
h_inter : ∀ G ⊆ F, #G ≤ finrank 𝕜 E + 1 → (⋂₀ ↑G).Nonempty
G : Finset (Set E)
hG_ss : G ⊆ F
hG_card : #G ≤ finrank 𝕜 E + 1
⊢ (⋂₀ ↑G).Nonempty

Tactic:
]

Goal state after:
𝕜 : Type u_2
E : Type u_3
inst✝⁵ : Field 𝕜
inst✝⁴ : LinearOrder 𝕜
inst✝³ : IsStrictOrderedRing 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
F : Finset (Set E)
h_convex : ∀ X ∈ F, Convex 𝕜 X
h_inter : ∀ G ⊆ F, #G ≤ finrank 𝕜 E + 1 → (⋂₀ ↑G).Nonempty
G : Finset (Set E)
hG_ss : G ⊆ F
hG_card : #G ≤ finrank 𝕜 E + 1
⊢ (⋂₀ ↑G).Nonempty
Module: Mathlib.Analysis.Convex.SimplicialComplex.AffineIndependentUnion

Goal state before:
pp: 𝕜 : Type ?u.4
E : Type ?u.12
inst✝⁵ : Field 𝕜
inst✝⁴ : LinearOrder 𝕜
inst✝³ : IsStrictOrderedRing 𝕜
inst✝² : DecidableEq E
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
abstract : PreAbstractSimplicialComplex E
indep : AffineIndependent 𝕜 Subtype.val
s t : Finset E
hs : s ∈ abstract.faces
ht : t ∈ abstract.faces
⊢ (convexHull 𝕜) ↑s ∩ (convexHull 𝕜) ↑t = (convexHull 𝕜) ↑s ∩ (convexHull 𝕜) ↑t

pp: case hs
𝕜 : Type ?u.4
E : Type ?u.12
inst✝⁵ : Field 𝕜
inst✝⁴ : LinearOrder 𝕜
inst✝³ : IsStrictOrderedRing 𝕜
inst✝² : DecidableEq E
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
abstract : PreAbstractSimplicialComplex E
indep : AffineIndependent 𝕜 Subtype.val
s t : Finset E
hs : s ∈ abstract.faces
ht : t ∈ abstract.faces
⊢ AffineIndependent 𝕜 Subtype.val

pp: case ht₁
𝕜 : Type ?u.4
E : Type ?u.12
inst✝⁵ : Field 𝕜
inst✝⁴ : LinearOrder 𝕜
inst✝³ : IsStrictOrderedRing 𝕜
inst✝² : DecidableEq E
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
abstract : PreAbstractSimplicialComplex E
indep : AffineIndependent 𝕜 Subtype.val
s t : Finset E
hs : s ∈ abstract.faces
ht : t ∈ abstract.faces
⊢ s ⊆ s ∪ t

pp: case ht₂
𝕜 : Type ?u.4
E : Type ?u.12
inst✝⁵ : Field 𝕜
inst✝⁴ : LinearOrder 𝕜
inst✝³ : IsStrictOrderedRing 𝕜
inst✝² : DecidableEq E
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
abstract : PreAbstractSimplicialComplex E
indep : AffineIndependent 𝕜 Subtype.val
s t : Finset E
hs : s ∈ abstract.faces
ht : t ∈ abstract.faces
⊢ t ⊆ s ∪ t

Tactic:
]

Goal state after:
case hs
𝕜 : Type ?u.4
E : Type ?u.12
inst✝⁵ : Field 𝕜
inst✝⁴ : LinearOrder 𝕜
inst✝³ : IsStrictOrderedRing 𝕜
inst✝² : DecidableEq E
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
abstract : PreAbstractSimplicialComplex E
indep : AffineIndependent 𝕜 Subtype.val
s t : Finset E
hs : s ∈ abstract.faces
ht : t ∈ abstract.faces
⊢ AffineIndependent 𝕜 Subtype.val

case ht₁
𝕜 : Type ?u.4
E : Type ?u.12
inst✝⁵ : Field 𝕜
inst✝⁴ : LinearOrder 𝕜
inst✝³ : IsStrictOrderedRing 𝕜
inst✝² : DecidableEq E
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
abstract : PreAbstractSimplicialComplex E
indep : AffineIndependent 𝕜 Subtype.val
s t : Finset E
hs : s ∈ abstract.faces
ht : t ∈ abstract.faces
⊢ s ⊆ s ∪ t

case ht₂
𝕜 : Type ?u.4
E : Type ?u.12
inst✝⁵ : Field 𝕜
inst✝⁴ : LinearOrder 𝕜
inst✝³ : IsStrictOrderedRing 𝕜
inst✝² : DecidableEq E
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
abstract : PreAbstractSimplicialComplex E
indep : AffineIndependent 𝕜 Subtype.val
s t : Finset E
hs : s ∈ abstract.faces
ht : t ∈ abstract.faces
⊢ t ⊆ s ∪ t
Module: Mathlib.Analysis.Convex.Radon

Goal state before:
pp: ι : Type u_1
𝕜 : Type u_2
E : Type u_3
inst✝⁷ : Field 𝕜
inst✝⁶ : LinearOrder 𝕜
inst✝⁵ : IsStrictOrderedRing 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : FiniteDimensional 𝕜 E
inst✝¹ : TopologicalSpace E
inst✝ : T2Space E
F : ι → Set E
h_convex : ∀ (i : ι), Convex 𝕜 (F i)
h_compact : ∀ (i : ι), IsCompact (F i)
h_inter : ∀ (I : Finset ι), #I ≤ finrank 𝕜 E + 1 → (⋂ i ∈ I, F i).Nonempty
h_nonempty : Nonempty ι
h_fin : ∀ (I : Finset ι), (⋂ i ∈ I, F i).Nonempty
i0 : ι
⊢ ⋂ i, F i = F i0 ∩ ⋂ i, F i

Tactic:
simp [iInter_subset]

Goal state after: