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

Goal state before:
pp: R : Type u_1
X : Type u_2
Y : Type u_3
inst✝⁴ : Semiring R
inst✝³ : PartialOrder R
inst✝² : IsStrictOrderedRing R
inst✝¹ : ConvexSpace R X
inst✝ : ConvexSpace R Y
x : X
s : Set X
t : Set Y
y : Y
hs : IsStarConvexSet R x s
ht : IsStarConvexSet R y t
w : X
z : Y
hw : (w, z).1 ∈ s
hz : (w, z).2 ∈ t
a b : R
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ convexCombPair a b ha hb hab (x, y) (w, z) ∈ s ×ˢ t

Tactic:
;

Goal state after:
R : Type u_1
X : Type u_2
Y : Type u_3
inst✝⁴ : Semiring R
inst✝³ : PartialOrder R
inst✝² : IsStrictOrderedRing R
inst✝¹ : ConvexSpace R X
inst✝ : ConvexSpace R Y
x : X
s : Set X
t : Set Y
y : Y
hs : IsStarConvexSet R x s
ht : IsStarConvexSet R y t
w : X
z : Y
hw : (w, z).1 ∈ s
hz : (w, z).2 ∈ t
a b : R
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ convexCombPair a b ha hb hab (x, y) (w, z) ∈ s ×ˢ t
Module: Mathlib.Geometry.Convex.Set

Goal state before:
pp: R : Type u_3
X : Type u_5
Y : Type u_6
inst✝⁴ : Semiring R
inst✝³ : PartialOrder R
inst✝² : IsStrictOrderedRing R
inst✝¹ : ConvexSpace R X
inst✝ : ConvexSpace R Y
f : X → Y
s : Set X
hf : IsAffineMap R f
hs : IsConvexSet R s
w : StdSimplex R Y
hw : ↑w.weights.support ⊆ f '' s
u : Finset X
hus : ↑u ⊆ s
hfu : InjOn f ↑u
huw : Finset.image f u = w.weights.support
x : X
⊢ 0 ≤ if x ∈ u then w.weights (f x) else 0

Tactic:
;

Goal state after:
R : Type u_3
X : Type u_5
Y : Type u_6
inst✝⁴ : Semiring R
inst✝³ : PartialOrder R
inst✝² : IsStrictOrderedRing R
inst✝¹ : ConvexSpace R X
inst✝ : ConvexSpace R Y
f : X → Y
s : Set X
hf : IsAffineMap R f
hs : IsConvexSet R s
w : StdSimplex R Y
hw : ↑w.weights.support ⊆ f '' s
u : Finset X
hus : ↑u ⊆ s
hfu : InjOn f ↑u
huw : Finset.image f u = w.weights.support
x : X
⊢ 0 ≤ if x ∈ u then w.weights (f x) else 0
Module: Mathlib.Geometry.Convex.Set

Goal state before:
pp: R : Type u_3
X : Type u_5
Y : Type u_6
inst✝⁴ : Semiring R
inst✝³ : PartialOrder R
inst✝² : IsStrictOrderedRing R
inst✝¹ : ConvexSpace R X
inst✝ : ConvexSpace R Y
f : X → Y
s : Set X
hf : IsAffineMap R f
hs : IsConvexSet R s
w : StdSimplex R Y
hw : ↑w.weights.support ⊆ f '' s
u : Finset X
hus : ↑u ⊆ s
hfu : InjOn f ↑u
huw : Finset.image f u = w.weights.support
y : Y
hy : ∀ x ∈ u, ¬f x = y
⊢ ∀ x ∈ u, ¬w.weights (f x) = 0 → ¬f x = y

Tactic:
;

Goal state after:
R : Type u_3
X : Type u_5
Y : Type u_6
inst✝⁴ : Semiring R
inst✝³ : PartialOrder R
inst✝² : IsStrictOrderedRing R
inst✝¹ : ConvexSpace R X
inst✝ : ConvexSpace R Y
f : X → Y
s : Set X
hf : IsAffineMap R f
hs : IsConvexSet R s
w : StdSimplex R Y
hw : ↑w.weights.support ⊆ f '' s
u : Finset X
hus : ↑u ⊆ s
hfu : InjOn f ↑u
huw : Finset.image f u = w.weights.support
y : Y
hy : ∀ x ∈ u, ¬f x = y
⊢ ∀ x ∈ u, ¬w.weights (f x) = 0 → ¬f x = y
Module: Mathlib.Geometry.Convex.Set

Goal state before:
pp: ι : Type u_1
I : Type u_2
R : Type u_3
K : Type u_4
X : Type u_5
Y : Type u_6
inst✝⁴ : Semiring R
inst✝³ : PartialOrder R
inst✝² : IsStrictOrderedRing R
inst✝¹ : ConvexSpace R X
inst✝ : ConvexSpace R Y
f : X → Y
w✝ : StdSimplex R X
s✝ t : Set X
x y : X
s : Set X
hs : IsConvexSet R s
w : StdSimplex R (StdSimplex R ↑s)
⊢ ↑⟨iConvexComb (StdSimplex.map (fun w ↦ ⟨iConvexComb w Subtype.val, ⋯⟩) w) Subtype.val, ⋯⟩ =
    ↑⟨iConvexComb (sConvexComb w) Subtype.val, ⋯⟩

Tactic:
;

Goal state after:
ι : Type u_1
I : Type u_2
R : Type u_3
K : Type u_4
X : Type u_5
Y : Type u_6
inst✝⁴ : Semiring R
inst✝³ : PartialOrder R
inst✝² : IsStrictOrderedRing R
inst✝¹ : ConvexSpace R X
inst✝ : ConvexSpace R Y
f : X → Y
w✝ : StdSimplex R X
s✝ t : Set X
x y : X
s : Set X
hs : IsConvexSet R s
w : StdSimplex R (StdSimplex R ↑s)
⊢ ↑⟨iConvexComb (StdSimplex.map (fun w ↦ ⟨iConvexComb w Subtype.val, ⋯⟩) w) Subtype.val, ⋯⟩ =
    ↑⟨iConvexComb (sConvexComb w) Subtype.val, ⋯⟩
Module: Mathlib.Geometry.Convex.Set

Goal state before:
pp: K : Type u_4
X : Type u_5
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : ConvexSpace K X
s : Set X
hs : ∀ (a b : K) (ha : 0 ≤ a) (hb : 0 ≤ b) (hab : a + b = 1), ∀ x ∈ s, ∀ y ∈ s, convexCombPair a b ha hb hab x y ∈ s
t✝ : Finset X
x : X
t : Finset X
hx : x ∉ t
ht : t.Nonempty
ih : ∀ ⦃w : StdSimplex K X⦄, ↑t ⊆ s → t = w.weights.support → sConvexComb w ∈ s
w : StdSimplex K X
hw : ↑(Finset.cons x t hx) ⊆ s
hsw : Finset.cons x t hx = w.weights.support
hwx : w.weights x ≠ 0
hwx' : ∃ y, y ≠ x ∧ w.weights y ≠ 0
⊢ t = {x_1 ∈ insert x t | ¬x_1 = x}

Tactic:
;

Goal state after:
K : Type u_4
X : Type u_5
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : ConvexSpace K X
s : Set X
hs : ∀ (a b : K) (ha : 0 ≤ a) (hb : 0 ≤ b) (hab : a + b = 1), ∀ x ∈ s, ∀ y ∈ s, convexCombPair a b ha hb hab x y ∈ s
t✝ : Finset X
x : X
t : Finset X
hx : x ∉ t
ht : t.Nonempty
ih : ∀ ⦃w : StdSimplex K X⦄, ↑t ⊆ s → t = w.weights.support → sConvexComb w ∈ s
w : StdSimplex K X
hw : ↑(Finset.cons x t hx) ⊆ s
hsw : Finset.cons x t hx = w.weights.support
hwx : w.weights x ≠ 0
hwx' : ∃ y, y ≠ x ∧ w.weights y ≠ 0
⊢ t = {x_1 ∈ insert x t | ¬x_1 = x}
Module: Mathlib.Analysis.Convex.Quasiconvex

Goal state before:
pp: E : Type u_4
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module ℝ E
inst✝³ : TopologicalSpace E
inst✝² : IsTopologicalAddGroup E
inst✝¹ : ContinuousSMul ℝ E
β : Type u_5
inst✝ : Preorder β
f : E → β
s : Set E
t : β
hfc : QuasiconcaveOn ℝ s f
⊢ IsPreconnected (s ↓∩ f ⁻¹' Ici t)

Tactic:
rw [← Topology.IsInducing.subtypeVal.isPreconnected_image,
    image_preimage_eq_inter_range,
    Subtype.range_coe, inter_comm]

Goal state after:
E : Type u_4
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module ℝ E
inst✝³ : TopologicalSpace E
inst✝² : IsTopologicalAddGroup E
inst✝¹ : ContinuousSMul ℝ E
β : Type u_5
inst✝ : Preorder β
f : E → β
s : Set E
t : β
hfc : QuasiconcaveOn ℝ s f
⊢ IsPreconnected (s ∩ f ⁻¹' Ici t)
Module: Mathlib.Analysis.Convex.Quasiconvex

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
β : Type u_3
inst✝⁴ : Semiring 𝕜
inst✝³ : PartialOrder 𝕜
inst✝² : AddCommMonoid E
inst✝¹ : SMul 𝕜 E
s : Set E
f g : E → β
inst✝ : SemilatticeSup β
hf : QuasiconvexOn 𝕜 s f
hg : QuasiconvexOn 𝕜 s g
⊢ QuasiconvexOn 𝕜 s (f ⊔ g)

Tactic:
intro r

Goal state after:
𝕜 : Type u_1
E : Type u_2
β : Type u_3
inst✝⁴ : Semiring 𝕜
inst✝³ : PartialOrder 𝕜
inst✝² : AddCommMonoid E
inst✝¹ : SMul 𝕜 E
s : Set E
f g : E → β
inst✝ : SemilatticeSup β
hf : QuasiconvexOn 𝕜 s f
hg : QuasiconvexOn 𝕜 s g
r : β
⊢ Convex 𝕜 {x | x ∈ s ∧ (f ⊔ g) x ≤ r}
Module: Mathlib.Analysis.Convex.Piecewise

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
β : Type u_3
inst✝¹¹ : Semiring 𝕜
inst✝¹⁰ : PartialOrder 𝕜
inst✝⁹ : AddCommMonoid E
inst✝⁸ : LinearOrder E
inst✝⁷ : IsOrderedAddMonoid E
inst✝⁶ : Module 𝕜 E
inst✝⁵ : PosSMulMono 𝕜 E
inst✝⁴ : AddCommGroup β
inst✝³ : PartialOrder β
inst✝² : IsOrderedAddMonoid β
inst✝¹ : Module 𝕜 β
inst✝ : PosSMulMono 𝕜 β
e : E
f g : E → β
hf : ConvexOn 𝕜 (Set.Ici e) f
hg : ConvexOn 𝕜 (Set.Iic e) g
h_mono : MonotoneOn f (Set.Ici e)
h_anti : AntitoneOn g (Set.Iic e)
h_eq : f e = g e
x : E
⊢ (Set.Ici e).piecewise f g x = (Set.Iic e).piecewise g f x

Tactic:
;

Goal state after:
𝕜 : Type u_1
E : Type u_2
β : Type u_3
inst✝¹¹ : Semiring 𝕜
inst✝¹⁰ : PartialOrder 𝕜
inst✝⁹ : AddCommMonoid E
inst✝⁸ : LinearOrder E
inst✝⁷ : IsOrderedAddMonoid E
inst✝⁶ : Module 𝕜 E
inst✝⁵ : PosSMulMono 𝕜 E
inst✝⁴ : AddCommGroup β
inst✝³ : PartialOrder β
inst✝² : IsOrderedAddMonoid β
inst✝¹ : Module 𝕜 β
inst✝ : PosSMulMono 𝕜 β
e : E
f g : E → β
hf : ConvexOn 𝕜 (Set.Ici e) f
hg : ConvexOn 𝕜 (Set.Iic e) g
h_mono : MonotoneOn f (Set.Ici e)
h_anti : AntitoneOn g (Set.Iic e)
h_eq : f e = g e
x : E
⊢ (Set.Ici e).piecewise f g x = (Set.Iic e).piecewise g f x
Module: Mathlib.Analysis.Convex.MetricSpace

Goal state before:
pp: case inr.hss'
X : Type u_2
inst✝² : ConvexSpace ℝ X
inst✝¹ : MetricSpace X
inst✝ : IsConvexDist X
s t s' t' : ℝ
hs : 0 ≤ s
ht : 0 ≤ t
h : s + t = 1
hs' : 0 ≤ s'
ht' : 0 ≤ t'
h' : s' + t' = 1
x y : X
this :
  ∀ {s t s' t' : ℝ} (hs : 0 ≤ s) (ht : 0 ≤ t) (h : s + t = 1) (hs' : 0 ≤ s') (ht' : 0 ≤ t') (h' : s' + t' = 1),
    s' ≤ s → dist (convexCombPair s t hs ht h x y) (convexCombPair s' t' hs' ht' h' x y) = |s - s'| * dist x y
hss' : ¬s' ≤ s
⊢ s ≤ s'

Tactic:
;

Goal state after:
case inr.hss'
X : Type u_2
inst✝² : ConvexSpace ℝ X
inst✝¹ : MetricSpace X
inst✝ : IsConvexDist X
s t s' t' : ℝ
hs : 0 ≤ s
ht : 0 ≤ t
h : s + t = 1
hs' : 0 ≤ s'
ht' : 0 ≤ t'
h' : s' + t' = 1
x y : X
this :
  ∀ {s t s' t' : ℝ} (hs : 0 ≤ s) (ht : 0 ≤ t) (h : s + t = 1) (hs' : 0 ≤ s') (ht' : 0 ≤ t') (h' : s' + t' = 1),
    s' ≤ s → dist (convexCombPair s t hs ht h x y) (convexCombPair s' t' hs' ht' h' x y) = |s - s'| * dist x y
hss' : ¬s' ≤ s
⊢ s ≤ s'
Module: Mathlib.Analysis.Convex.MetricSpace

Goal state before:
pp: X : Type u_2
inst✝² : ConvexSpace ℝ X
inst✝¹ : MetricSpace X
inst✝ : IsConvexDist X
x y : X
s t s' t' : ℝ
hs : 0 ≤ s
ht : 0 ≤ t
h : s + t = 1
hs' : 0 ≤ s'
ht' : 0 ≤ t'
h' : s' + t' = 1
hss' : s' ≤ s
this : dist (convexCombPair s t hs ht h x y) (convexCombPair s' t' hs' ht' h' x y) ≤ |s - s'| * dist x y
⊢ |t - t'| = |1 - t - (1 - t')|

Tactic:
;

Goal state after:
X : Type u_2
inst✝² : ConvexSpace ℝ X
inst✝¹ : MetricSpace X
inst✝ : IsConvexDist X
x y : X
s t s' t' : ℝ
hs : 0 ≤ s
ht : 0 ≤ t
h : s + t = 1
hs' : 0 ≤ s'
ht' : 0 ≤ t'
h' : s' + t' = 1
hss' : s' ≤ s
this : dist (convexCombPair s t hs ht h x y) (convexCombPair s' t' hs' ht' h' x y) ≤ |s - s'| * dist x y
⊢ |t - t'| = |1 - t - (1 - t')|
Module: Mathlib.Analysis.Convex.MetricSpace

Goal state before:
pp: case e'_4
X : Type u_2
inst✝² : ConvexSpace ℝ X
inst✝¹ : MetricSpace X
inst✝ : IsConvexDist X
x y : X
s t s' t' : ℝ
hs : 0 ≤ s
ht : 0 ≤ t
h : s + t = 1
hs' : 0 ≤ s'
ht' : 0 ≤ t'
h' : s' + t' = 1
hss' : s' ≤ s
f : StdSimplex ℝ (Fin 3) := { weights := Finsupp.equivFunOnFinite.symm ![s', s - s', t], nonneg := ⋯, total := ⋯ }
⊢ |s - s'| * dist x y = iConvexComb f fun i ↦ dist (![x, x, y] i) (![x, y, y] i)

pp: case e'_3
X : Type u_2
inst✝² : ConvexSpace ℝ X
inst✝¹ : MetricSpace X
inst✝ : IsConvexDist X
x y : X
s t s' t' : ℝ
hs : 0 ≤ s
ht : 0 ≤ t
h : s + t = 1
hs' : 0 ≤ s'
ht' : 0 ≤ t'
h' : s' + t' = 1
hss' : s' ≤ s
f : StdSimplex ℝ (Fin 3) := { weights := Finsupp.equivFunOnFinite.symm ![s', s - s', t], nonneg := ⋯, total := ⋯ }
⊢ dist (convexCombPair s t hs ht h x y) (convexCombPair s' t' hs' ht' h' x y) =
    dist (iConvexComb f ![x, x, y]) (iConvexComb f ![x, y, y])

Tactic:
;

Goal state after:
case e'_4
X : Type u_2
inst✝² : ConvexSpace ℝ X
inst✝¹ : MetricSpace X
inst✝ : IsConvexDist X
x y : X
s t s' t' : ℝ
hs : 0 ≤ s
ht : 0 ≤ t
h : s + t = 1
hs' : 0 ≤ s'
ht' : 0 ≤ t'
h' : s' + t' = 1
hss' : s' ≤ s
f : StdSimplex ℝ (Fin 3) := { weights := Finsupp.equivFunOnFinite.symm ![s', s - s', t], nonneg := ⋯, total := ⋯ }
⊢ |s - s'| * dist x y = iConvexComb f fun i ↦ dist (![x, x, y] i) (![x, y, y] i)

case e'_3
X : Type u_2
inst✝² : ConvexSpace ℝ X
inst✝¹ : MetricSpace X
inst✝ : IsConvexDist X
x y : X
s t s' t' : ℝ
hs : 0 ≤ s
ht : 0 ≤ t
h : s + t = 1
hs' : 0 ≤ s'
ht' : 0 ≤ t'
h' : s' + t' = 1
hss' : s' ≤ s
f : StdSimplex ℝ (Fin 3) := { weights := Finsupp.equivFunOnFinite.symm ![s', s - s', t], nonneg := ⋯, total := ⋯ }
⊢ dist (convexCombPair s t hs ht h x y) (convexCombPair s' t' hs' ht' h' x y) =
    dist (iConvexComb f ![x, x, y]) (iConvexComb f ![x, y, y])
Module: Mathlib.Analysis.Convex.Radon

Goal state before:
pp: case hn
𝕜 : 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
i : ↥s
⊢ #s - 1 = k

Tactic:
;

Goal state after:
case hn
𝕜 : 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
i : ↥s
⊢ #s - 1 = k
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
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
⊢ #s = k - 1 + 2

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
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
⊢ #s = k - 1 + 2
Module: Mathlib.Analysis.Convex.MetricSpace

Goal state before:
pp: case ha
X : Type u_2
inst✝² : ConvexSpace ℝ X
inst✝¹ : MetricSpace X
inst✝ : IsConvexDist X
i : ↑(Set.Icc 0 1)
x y : X × X
⊢ 0 ≤ ↑i

pp: case ha
X : Type u_2
inst✝² : ConvexSpace ℝ X
inst✝¹ : MetricSpace X
inst✝ : IsConvexDist X
i : ↑(Set.Icc 0 1)
x y : X × X
⊢ ↑i * max (dist x.1 y.1) (dist x.2 y.2) + (1 - ↑i) * dist x.2 y.2 ≤ max (dist x.1 y.1) (dist x.2 y.2)

Tactic:
;

Goal state after:
case ha
X : Type u_2
inst✝² : ConvexSpace ℝ X
inst✝¹ : MetricSpace X
inst✝ : IsConvexDist X
i : ↑(Set.Icc 0 1)
x y : X × X
⊢ 0 ≤ ↑i

case ha
X : Type u_2
inst✝² : ConvexSpace ℝ X
inst✝¹ : MetricSpace X
inst✝ : IsConvexDist X
i : ↑(Set.Icc 0 1)
x y : X × X
⊢ ↑i * max (dist x.1 y.1) (dist x.2 y.2) + (1 - ↑i) * dist x.2 y.2 ≤ max (dist x.1 y.1) (dist x.2 y.2)
Module: Mathlib.Analysis.Convex.MetricSpace

Goal state before:
pp: case ha
X : Type u_2
inst✝² : ConvexSpace ℝ X
inst✝¹ : MetricSpace X
inst✝ : IsConvexDist X
i : ↑(Set.Icc 0 1)
x y : X × X
⊢ 0 ≤ 1 - ↑i

pp: case ha
X : Type u_2
inst✝² : ConvexSpace ℝ X
inst✝¹ : MetricSpace X
inst✝ : IsConvexDist X
i : ↑(Set.Icc 0 1)
x y : X × X
⊢ ↑i * max (dist x.1 y.1) (dist x.2 y.2) + (1 - ↑i) * max (dist x.1 y.1) (dist x.2 y.2) ≤
    max (dist x.1 y.1) (dist x.2 y.2)

Tactic:
;

Goal state after:
case ha
X : Type u_2
inst✝² : ConvexSpace ℝ X
inst✝¹ : MetricSpace X
inst✝ : IsConvexDist X
i : ↑(Set.Icc 0 1)
x y : X × X
⊢ 0 ≤ 1 - ↑i

case ha
X : Type u_2
inst✝² : ConvexSpace ℝ X
inst✝¹ : MetricSpace X
inst✝ : IsConvexDist X
i : ↑(Set.Icc 0 1)
x y : X × X
⊢ ↑i * max (dist x.1 y.1) (dist x.2 y.2) + (1 - ↑i) * max (dist x.1 y.1) (dist x.2 y.2) ≤
    max (dist x.1 y.1) (dist x.2 y.2)
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
D : ℝ
t : T
hx : ContinuousOn x (f ⁻¹' {0})ᶜ
hy : ContinuousOn y (f ⁻¹' {1})ᶜ
hx' : Bornology.IsBounded (Set.range x)
hy' : Bornology.IsBounded (Set.range y)
hD' : 0 < D
hD : ∀ (t₁ t₂ : T), dist (x t₁) (y t₂) ≤ D
ht : 0 < f t ∧ f t < 1
⊢ ∀ (a : T), 0 < f a → f a < 1 → ¬f a = 0

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
D : ℝ
t : T
hx : ContinuousOn x (f ⁻¹' {0})ᶜ
hy : ContinuousOn y (f ⁻¹' {1})ᶜ
hx' : Bornology.IsBounded (Set.range x)
hy' : Bornology.IsBounded (Set.range y)
hD' : 0 < D
hD : ∀ (t₁ t₂ : T), dist (x t₁) (y t₂) ≤ D
ht : 0 < f t ∧ f t < 1
⊢ ∀ (a : T), 0 < f a → f a < 1 → ¬f a = 0
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
D : ℝ
t : T
hx : ContinuousOn x (f ⁻¹' {0})ᶜ
hy : ContinuousOn y (f ⁻¹' {1})ᶜ
hx' : Bornology.IsBounded (Set.range x)
hy' : Bornology.IsBounded (Set.range y)
hD' : 0 < D
hD : ∀ (t₁ t₂ : T), dist (x t₁) (y t₂) ≤ D
ht : 0 < f t ∧ f t < 1
⊢ ∀ (a : T), 0 < f a → f a < 1 → ¬f a = 1

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
D : ℝ
t : T
hx : ContinuousOn x (f ⁻¹' {0})ᶜ
hy : ContinuousOn y (f ⁻¹' {1})ᶜ
hx' : Bornology.IsBounded (Set.range x)
hy' : Bornology.IsBounded (Set.range y)
hD' : 0 < D
hD : ∀ (t₁ t₂ : T), dist (x t₁) (y t₂) ≤ D
ht : 0 < f t ∧ f t < 1
⊢ ∀ (a : T), 0 < f a → f a < 1 → ¬f a = 1
Module: Mathlib.Analysis.Convex.MetricSpace

Goal state before:
pp: case neg.inl
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 = 0
⊢ ∀ (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 (y t) i

Tactic:
intro r

Goal state after:
case neg.inl
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 = 0
r : ℝ
⊢ 0 < r → ∀ᶠ (x_1 : T) in nhds t, convexCombPair (f x_1) (1 - f x_1) ⋯ ⋯ ⋯ (x x_1) (y x_1) ∈ Metric.ball (y t) r
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 := ⋯
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 := ⋯
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.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 = 0
r : ℝ
hr : 0 < r
j : T
hj : dist (y j) (y t) < r / 3
hj' : |f j| < r / D / 3
⊢ 1 + 1 ≤ 3

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 = 0
r : ℝ
hr : 0 < r
j : T
hj : dist (y j) (y t) < r / 3
hj' : |f j| < r / D / 3
⊢ 1 + 1 ≤ 3
Module: Mathlib.Geometry.Convex.ConvexSpace.Module

Goal state before:
pp: F : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
I : Type u_5
inst✝¹³ : Semiring R
inst✝¹² : PartialOrder R
inst✝¹¹ : IsStrictOrderedRing R
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : Module R M
inst✝⁸ : AddCommMonoid N
inst✝⁷ : Module R N
inst✝⁶ : SetLike F M
inst✝⁵ : AddSubmonoidClass F M
inst✝⁴ : SMulMemClass F R M
f g : M → N
inst✝³ : ConvexSpace R M
inst✝² : IsModuleConvexSpace R M
inst✝¹ : ConvexSpace R N
inst✝ : IsModuleConvexSpace R N
x y : M
s t : Set M
a b : R
S : F
w : StdSimplex R ↥S
⊢ ↑(sConvexComb w) = ↑(w.weights.sum fun m r ↦ r • m)

Tactic:
;

Goal state after:
F : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
I : Type u_5
inst✝¹³ : Semiring R
inst✝¹² : PartialOrder R
inst✝¹¹ : IsStrictOrderedRing R
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : Module R M
inst✝⁸ : AddCommMonoid N
inst✝⁷ : Module R N
inst✝⁶ : SetLike F M
inst✝⁵ : AddSubmonoidClass F M
inst✝⁴ : SMulMemClass F R M
f g : M → N
inst✝³ : ConvexSpace R M
inst✝² : IsModuleConvexSpace R M
inst✝¹ : ConvexSpace R N
inst✝ : IsModuleConvexSpace R N
x y : M
s t : Set M
a b : R
S : F
w : StdSimplex R ↥S
⊢ ↑(sConvexComb w) = ↑(w.weights.sum fun m r ↦ r • m)