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

Goal state before:
pp: R : Type u_1
M : Type u_3
I : Type u_6
inst✝³ : PartialOrder R
inst✝² : Semiring R
inst✝¹ : IsStrictOrderedRing R
inst✝ : ConvexSpace R M
i : I
f : I → M
⊢ iConvexComb (StdSimplex.single i) f = f i

Tactic:
by

Goal state after:
Module: Mathlib.Geometry.Convex.ConvexSpace.Defs

Goal state before:
pp: R : Type u_1
M : Type u_3
inst✝³ : PartialOrder R
inst✝² : Semiring R
inst✝¹ : IsStrictOrderedRing R
inst✝ : ConvexSpace R M
w : StdSimplex R M
⊢ iConvexComb w id = sConvexComb w

Tactic:
by

Goal state after:
Module: Mathlib.Geometry.Convex.ConvexSpace.Defs

Goal state before:
pp: R : Type u_1
M : Type u_3
I : Type u_6
J : Type u_7
inst✝³ : PartialOrder R
inst✝² : Semiring R
inst✝¹ : IsStrictOrderedRing R
inst✝ : ConvexSpace R M
s : StdSimplex R I
f : I → J
g : J → M
⊢ iConvexComb (map f s) g = iConvexComb s fun i ↦ g (f i)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
μ : Measure α
f : α → E
C : ℝ
inst✝ : StrictConvexSpace ℝ E
h_le : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ C
hC0 : 0 < C
hfi : Integrable f μ
hμt : μ univ < ∞
this : IsFiniteMeasure μ
⊢ ∀ᵐ (x : α) ∂μ, f x ∈ closedBall 0 C

Tactic:
by

Goal state after:
Module: Mathlib.Geometry.Convex.ConvexSpace.Defs

Goal state before:
pp: R : Type u_1
M : Type u_3
I : Type u_6
inst✝³ : PartialOrder R
inst✝² : Semiring R
inst✝¹ : IsStrictOrderedRing R
inst✝ : ConvexSpace R M
w : StdSimplex R I
f g : I → M
hfg : ∀ (i : I), w.weights i ≠ 0 → f i = g i
i✝ : M
i : I
hi : i ∈ w.weights.support
⊢ w.weights i ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.Geometry.Convex.ConvexSpace.Defs

Goal state before:
pp: R : Type u_1
M : Type u_3
I : Type u_6
inst✝³ : PartialOrder R
inst✝² : Semiring R
inst✝¹ : IsStrictOrderedRing R
inst✝ : ConvexSpace R M
w : StdSimplex R I
f g : I → M
hfg : ∀ (i : I), w.weights i ≠ 0 → f i = g i
⊢ iConvexComb w f = iConvexComb w g

Tactic:
by

Goal state after:
Module: Mathlib.Geometry.Convex.ConvexSpace.Defs

Goal state before:
pp: R : Type u_1
M : Type u_3
I : Type u_6
J : Type u_7
inst✝³ : PartialOrder R
inst✝² : Semiring R
inst✝¹ : IsStrictOrderedRing R
inst✝ : ConvexSpace R M
s : StdSimplex R I
f : I ≃ J
g : I → M
⊢ iConvexComb s g = iConvexComb (map (⇑f) s) (g ∘ ⇑f.symm)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
μ : Measure α
f : α → E
C : ℝ
inst✝ : StrictConvexSpace ℝ E
h_le : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ C
⊢ f =ᵐ[μ] const α (⨍ (x : α), f x ∂μ) ∨ ‖⨍ (x : α), f x ∂μ‖ < C

Tactic:
by

Goal state after:
Module: Mathlib.Geometry.Convex.ConvexSpace.Defs

Goal state before:
pp: R : Type u_1
M : Type u_3
I : Type u_6
inst✝³ : PartialOrder R
inst✝² : Semiring R
inst✝¹ : IsStrictOrderedRing R
inst✝ : ConvexSpace R M
J : I → Type u_9
s : StdSimplex R I
f : (i : I) → StdSimplex R (J i)
g : (i : I) → J i → M
⊢ (iConvexComb s fun i ↦ iConvexComb (f i) (g i)) =
    iConvexComb (iConvexComb s fun i ↦ map (fun x ↦ ⟨i, x⟩) (f i)) (Sigma.uncurry g)

Tactic:
by

Goal state after:
Module: Mathlib.Geometry.Convex.ConvexSpace.Defs

Goal state before:
pp: R : Type u_1
M : Type u_3
I : Type u_6
inst✝³ : PartialOrder R
inst✝² : Semiring R
inst✝¹ : IsStrictOrderedRing R
inst✝ : ConvexSpace R M
J : Type u_9
s : StdSimplex R I
f : I → StdSimplex R J
g : I → J → M
⊢ (iConvexComb s fun i ↦ iConvexComb (f i) (g i)) =
    iConvexComb (iConvexComb s fun i ↦ map (fun x ↦ (i, x)) (f i)) (Function.uncurry g)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : CompleteSpace E
μ : Measure α
f : α → E
C : ℝ
inst✝¹ : StrictConvexSpace ℝ E
inst✝ : IsFiniteMeasure μ
h_le : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ C
h₀ : μ ≠ 0
⊢ 0 < μ.real univ

Tactic:
by

Goal state after:
Module: Mathlib.Geometry.Convex.ConvexSpace.Defs

Goal state before:
pp: R : Type u_1
M : Type u_3
I : Type u_6
inst✝³ : PartialOrder R
inst✝² : Semiring R
inst✝¹ : IsStrictOrderedRing R
inst✝ : ConvexSpace R M
J : Type u_9
s : StdSimplex R I
f : I → StdSimplex R J
g : J → M
⊢ (iConvexComb s fun i ↦ iConvexComb (f i) g) = iConvexComb (iConvexComb s f) g

Tactic:
by

Goal state after:
Module: Mathlib.Geometry.Convex.ConvexSpace.Defs

Goal state before:
pp: R : Type u_9
M : Type u_10
I : Type u_11
J : Type u_12
inst✝³ : PartialOrder R
inst✝² : CommSemiring R
inst✝¹ : IsStrictOrderedRing R
inst✝ : ConvexSpace R M
f : StdSimplex R I
g : StdSimplex R J
e : I → J → M
this : sConvexComb (map (fun x ↦ map (fun x_1 ↦ (x_1, x)) g) f) = sConvexComb (map ((fun g ↦ map g f) ∘ Prod.mk) g)
⊢ map (⇑(Equiv.prodComm I J)) (iConvexComb f fun i ↦ map (fun x ↦ (i, x)) g) =
    iConvexComb g fun i ↦ map (fun x ↦ (i, x)) f

Tactic:
by

Goal state after:
Module: Mathlib.Geometry.Convex.ConvexSpace.Defs

Goal state before:
pp: R : Type u_9
M : Type u_10
I : Type u_11
J : Type u_12
inst✝³ : PartialOrder R
inst✝² : CommSemiring R
inst✝¹ : IsStrictOrderedRing R
inst✝ : ConvexSpace R M
f : StdSimplex R I
g : StdSimplex R J
e : I → J → M
⊢ (iConvexComb f fun i ↦ iConvexComb g (e i)) = iConvexComb g fun j ↦ iConvexComb f fun i ↦ e i j

Tactic:
by

Goal state after:
Module: Mathlib.Geometry.Convex.ConvexSpace.Defs

Goal state before:
pp: R : Type u_1
M : Type u_3
N : Type u_4
I : Type u_6
inst✝⁴ : PartialOrder R
inst✝³ : Semiring R
inst✝² : IsStrictOrderedRing R
inst✝¹ : ConvexSpace R M
inst✝ : ConvexSpace R N
f : M → N
hf : IsAffineMap R f
s : StdSimplex R I
g : I → M
⊢ f (iConvexComb s g) = iConvexComb s (f ∘ g)

Tactic:
by

Goal state after:
Module: Mathlib.Geometry.Convex.ConvexSpace.Defs

Goal state before:
pp: R : Type u_1
M : Type u_3
inst✝³ : PartialOrder R
inst✝² : Semiring R
inst✝¹ : IsStrictOrderedRing R
inst✝ : ConvexSpace R M
s t : R
hs : 0 ≤ s
ht : 0 ≤ t
h : s + t = 1
p q : M
⊢ convexCombPair s t hs ht h p q = iConvexComb (duple 0 1 hs ht h) ![p, q]

Tactic:
by

Goal state after:
Module: Mathlib.Geometry.Convex.ConvexSpace.Defs

Goal state before:
pp: R : Type u_1
X : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
I : Type u_6
J : Type u_7
K : Type u_8
inst✝⁵ : PartialOrder R
inst✝⁴ : Semiring R
inst✝³ : IsStrictOrderedRing R
inst✝² : ConvexSpace R M
inst✝¹ : ConvexSpace R N
inst✝ : ConvexSpace R P
s t : R
hs : 0 ≤ s
ht : 0 ≤ t
h : s + t = 1
s' t' : R
hs' : 0 ≤ s'
ht' : 0 ≤ t'
h' : s' + t' = 1
s'' t'' : R
hs'' : 0 ≤ s''
ht'' : 0 ≤ t''
h'' : s'' + t'' = 1
x y : M
⊢ 0 ≤ 0

Tactic:
by

Goal state after:
Module: Mathlib.Geometry.Convex.ConvexSpace.Defs

Goal state before:
pp: R : Type u_1
X : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
I : Type u_6
J : Type u_7
K : Type u_8
inst✝⁵ : PartialOrder R
inst✝⁴ : Semiring R
inst✝³ : IsStrictOrderedRing R
inst✝² : ConvexSpace R M
inst✝¹ : ConvexSpace R N
inst✝ : ConvexSpace R P
s t : R
hs : 0 ≤ s
ht : 0 ≤ t
h : s + t = 1
s' t' : R
hs' : 0 ≤ s'
ht' : 0 ≤ t'
h' : s' + t' = 1
s'' t'' : R
hs'' : 0 ≤ s''
ht'' : 0 ≤ t''
h'' : s'' + t'' = 1
x y : M
⊢ 0 ≤ 1

Tactic:
by

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

Goal state before:
pp: α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : CompleteSpace E
μ : Measure α
f : α → E
C : ℝ
inst✝¹ : StrictConvexSpace ℝ E
inst✝ : IsFiniteMeasure μ
h_le : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ C
⊢ f =ᵐ[μ] const α (⨍ (x : α), f x ∂μ) ∨ ‖∫ (x : α), f x ∂μ‖ < μ.real univ * C

Tactic:
by

Goal state after:
Module: Mathlib.Geometry.Convex.ConvexSpace.Defs

Goal state before:
pp: R : Type u_1
X : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
I : Type u_6
J : Type u_7
K : Type u_8
inst✝⁵ : PartialOrder R
inst✝⁴ : Semiring R
inst✝³ : IsStrictOrderedRing R
inst✝² : ConvexSpace R M
inst✝¹ : ConvexSpace R N
inst✝ : ConvexSpace R P
s t : R
hs : 0 ≤ s
ht : 0 ≤ t
h : s + t = 1
s' t' : R
hs' : 0 ≤ s'
ht' : 0 ≤ t'
h' : s' + t' = 1
s'' t'' : R
hs'' : 0 ≤ s''
ht'' : 0 ≤ t''
h'' : s'' + t'' = 1
x y : M
⊢ 0 + 1 = 1

Tactic:
by

Goal state after:
Module: Mathlib.Geometry.Convex.ConvexSpace.Defs

Goal state before:
pp: R : Type u_1
M : Type u_3
inst✝³ : PartialOrder R
inst✝² : Semiring R
inst✝¹ : IsStrictOrderedRing R
inst✝ : ConvexSpace R M
x y : M
⊢ convexCombPair 0 1 ⋯ ⋯ ⋯ x y = y

Tactic:
by

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

Goal state before:
pp: α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
μ : Measure α
t : Set α
f : α → E
C : ℝ
inst✝ : StrictConvexSpace ℝ E
ht : μ t ≠ ∞
h_le : ∀ᵐ (x : α) ∂μ.restrict t, ‖f x‖ ≤ C
⊢ f =ᵐ[μ.restrict t] const α (⨍ (x : α) in t, f x ∂μ) ∨ ‖∫ (x : α) in t, f x ∂μ‖ < μ.real t * C

Tactic:
by

Goal state after:
Module: Mathlib.Geometry.Convex.ConvexSpace.Defs

Goal state before:
pp: R : Type u_1
X : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
I : Type u_6
J : Type u_7
K : Type u_8
inst✝⁵ : PartialOrder R
inst✝⁴ : Semiring R
inst✝³ : IsStrictOrderedRing R
inst✝² : ConvexSpace R M
inst✝¹ : ConvexSpace R N
inst✝ : ConvexSpace R P
s t : R
hs : 0 ≤ s
ht : 0 ≤ t
h : s + t = 1
s' t' : R
hs' : 0 ≤ s'
ht' : 0 ≤ t'
h' : s' + t' = 1
s'' t'' : R
hs'' : 0 ≤ s''
ht'' : 0 ≤ t''
h'' : s'' + t'' = 1
x y : M
⊢ 1 + 0 = 1

Tactic:
by

Goal state after:
Module: Mathlib.Geometry.Convex.ConvexSpace.Defs

Goal state before:
pp: R : Type u_1
M : Type u_3
inst✝³ : PartialOrder R
inst✝² : Semiring R
inst✝¹ : IsStrictOrderedRing R
inst✝ : ConvexSpace R M
x y : M
⊢ convexCombPair 1 0 ⋯ ⋯ ⋯ x y = x

Tactic:
by

Goal state after:
Module: Mathlib.Geometry.Convex.ConvexSpace.Defs

Goal state before:
pp: R : Type u_1
M : Type u_3
inst✝³ : PartialOrder R
inst✝² : Semiring R
inst✝¹ : IsStrictOrderedRing R
inst✝ : ConvexSpace R M
s t : R
hs : 0 ≤ s
ht : 0 ≤ t
h : s + t = 1
x : M
⊢ convexCombPair s t hs ht h x x = x

Tactic:
by

Goal state after:
Module: Mathlib.Geometry.Convex.Star

Goal state before:
pp: R : Type u_1
X : Type u_2
inst✝³ : Semiring R
inst✝² : PartialOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : ConvexSpace R X
x : X
⊢ IsStarConvexSet R x ∅

Tactic:
by

Goal state after:
Module: Mathlib.Geometry.Convex.Star

Goal state before:
pp: R : Type u_1
X : Type u_2
inst✝³ : Semiring R
inst✝² : PartialOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : ConvexSpace R X
x : X
⊢ IsStarConvexSet R x univ

Tactic:
by

Goal state after:
Module: Mathlib.Geometry.Convex.Star

Goal state before:
pp: R : Type u_1
X : Type u_2
inst✝³ : Semiring R
inst✝² : PartialOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : ConvexSpace R X
x : X
⊢ IsStarConvexSet R x {x}

Tactic:
by

Goal state after:
Module: Mathlib.Geometry.Convex.Star

Goal state before:
pp: R : Type u_1
X : Type u_2
inst✝³ : Semiring R
inst✝² : PartialOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : ConvexSpace R X
x : X
s t : Set X
hs : IsStarConvexSet R x s
ht : IsStarConvexSet R x t
⊢ IsStarConvexSet R x (s ∩ t)

Tactic:
by

Goal state after:
Module: Mathlib.Geometry.Convex.Star

Goal state before:
pp: R : Type u_1
X : Type u_2
inst✝³ : Semiring R
inst✝² : PartialOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : ConvexSpace R X
x : X
s t : Set X
hs : IsStarConvexSet R x s
ht : IsStarConvexSet R x t
⊢ IsStarConvexSet R x (s ∪ t)

Tactic:
by

Goal state after:
Module: Mathlib.Geometry.Convex.Star

Goal state before:
pp: R : Type u_1
X : Type u_2
inst✝³ : Semiring R
inst✝² : PartialOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : ConvexSpace R X
x : X
S : Set (Set X)
hS : ∀ s ∈ S, IsStarConvexSet R x s
⊢ IsStarConvexSet R x (⋂₀ S)

Tactic:
by

Goal state after:
Module: Mathlib.Geometry.Convex.Star

Goal state before:
pp: R : Type u_1
X : Type u_2
ι : Sort u_4
inst✝³ : Semiring R
inst✝² : PartialOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : ConvexSpace R X
x : X
s : ι → Set X
hs : ∀ (i : ι), IsStarConvexSet R x (s i)
⊢ IsStarConvexSet R x (⋂ i, s i)

Tactic:
by

Goal state after:
Module: Mathlib.Geometry.Convex.Star

Goal state before:
pp: R : Type u_1
X : Type u_2
inst✝³ : Semiring R
inst✝² : PartialOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : ConvexSpace R X
x : X
S : Set (Set X)
hS : ∀ s ∈ S, IsStarConvexSet R x s
⊢ IsStarConvexSet R x (⋃₀ S)

Tactic:
by

Goal state after:
Module: Mathlib.Geometry.Convex.Star

Goal state before:
pp: R : Type u_1
X : Type u_2
ι : Sort u_4
inst✝³ : Semiring R
inst✝² : PartialOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : ConvexSpace R X
x : X
s : ι → Set X
hs : ∀ (i : ι), IsStarConvexSet R x (s i)
⊢ ∀ s_1 ∈ range fun i ↦ s i, IsStarConvexSet R x s_1

Tactic:
by

Goal state after:
Module: Mathlib.Geometry.Convex.Star

Goal state before:
pp: R : Type u_1
X : Type u_2
inst✝³ : Semiring R
inst✝² : PartialOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : ConvexSpace R X
x : X
s : Set X
hs : IsStarConvexSet R x s
hs₀ : s.Nonempty
⊢ x ∈ s

Tactic:
by

Goal state after:
Module: Mathlib.Geometry.Convex.ConvexSpace.Defs

Goal state before:
pp: R : Type u_1
M : Type u_3
inst✝³ : PartialOrder R
inst✝² : Semiring R
inst✝¹ : IsStrictOrderedRing R
inst✝ : ConvexSpace R M
s t : R
hs : 0 ≤ s
ht : 0 ≤ t
h : s + t = 1
x y : M
⊢ convexCombPair s t hs ht h x y = convexCombPair t s ht hs ⋯ y x

Tactic:
by

Goal state after:
Module: Mathlib.Geometry.Convex.ConvexSpace.Defs

Goal state before:
pp: R : Type u_1
M : Type u_3
N : Type u_4
inst✝⁴ : PartialOrder R
inst✝³ : Semiring R
inst✝² : IsStrictOrderedRing R
inst✝¹ : ConvexSpace R M
inst✝ : ConvexSpace R N
f : M → N
hf : IsAffineMap R f
s t : R
hs : 0 ≤ s
ht : 0 ≤ t
h : s + t = 1
x y : M
⊢ f (convexCombPair s t hs ht h x y) = convexCombPair s t hs ht h (f x) (f y)

Tactic:
by

Goal state after:
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
f : X → Y
x : X
s : Set Y
hf : IsAffineMap R f
hs : IsStarConvexSet R (f x) s
y : X
hy : y ∈ f ⁻¹' s
a b : R
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ convexCombPair a b ha hb hab x y ∈ f ⁻¹' s

Tactic:
by

Goal state after:
Module: Mathlib.Geometry.Convex.ConvexSpace.Defs

Goal state before:
pp: R : Type u_1
M : Type u_3
inst✝³ : PartialOrder R
inst✝² : Semiring R
inst✝¹ : IsStrictOrderedRing R
inst✝ : ConvexSpace R M
s t : R
hs : 0 ≤ s
ht : 0 ≤ t
h : s + t = 1
J₁ : Type u₁
J₂ : Type u₂
g₁ : StdSimplex R J₁
g₂ : StdSimplex R J₂
m₁ : J₁ → M
m₂ : J₂ → M
⊢ convexCombPair s t hs ht h (iConvexComb g₁ m₁) (iConvexComb g₂ m₂) =
    sConvexComb (convexCombPair s t hs ht h (map m₁ g₁) (map m₂ g₂))

Tactic:
by

Goal state after:
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
f : X → Y
x : X
s : Set X
hf : IsAffineMap R f
hs : IsStarConvexSet R x s
⊢ IsStarConvexSet R (f x) (f '' s)

Tactic:
by

Goal state after:
Module: Mathlib.Geometry.Convex.ConvexSpace.Defs

Goal state before:
pp: R : Type u_1
M : Type u_3
I : Type u_6
inst✝³ : PartialOrder R
inst✝² : Semiring R
inst✝¹ : IsStrictOrderedRing R
inst✝ : ConvexSpace R M
s t : I → R
hs : ∀ (i : I), 0 ≤ s i
ht : ∀ (i : I), 0 ≤ t i
h : ∀ (i : I), s i + t i = 1
f : StdSimplex R I
m₁ m₂ : I → M
⊢ (iConvexComb f fun i ↦ convexCombPair (s i) (t i) ⋯ ⋯ ⋯ (m₁ i) (m₂ i)) =
    sConvexComb (iConvexComb f fun i ↦ duple (m₁ i) (m₂ i) ⋯ ⋯ ⋯)

Tactic:
by

Goal state after:
Module: Mathlib.Geometry.Convex.ConvexSpace.Defs

Goal state before:
pp: R : Type u_1
M : Type u_3
J : Type u_7
inst✝³ : PartialOrder R
inst✝² : Semiring R
inst✝¹ : IsStrictOrderedRing R
inst✝ : ConvexSpace R M
s t : R
hs : 0 ≤ s
ht : 0 ≤ t
h : s + t = 1
g : StdSimplex R J
e : J → M
m : M
⊢ convexCombPair s t hs ht h (iConvexComb g e) m =
    sConvexComb (convexCombPair s t hs ht h (map e g) (StdSimplex.single m))

Tactic:
by

Goal state after:
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)).1 ∈ s

Tactic:
by

Goal state after:
Module: Mathlib.Geometry.Convex.ConvexSpace.Defs

Goal state before:
pp: R : Type u_1
M : Type u_3
J : Type u_7
inst✝³ : PartialOrder R
inst✝² : Semiring R
inst✝¹ : IsStrictOrderedRing R
inst✝ : ConvexSpace R M
s t : R
hs : 0 ≤ s
ht : 0 ≤ t
h : s + t = 1
m : M
g : StdSimplex R J
e : J → M
⊢ convexCombPair s t hs ht h m (iConvexComb g e) =
    sConvexComb (convexCombPair s t hs ht h (StdSimplex.single m) (map e g))

Tactic:
by

Goal state after:
Module: Mathlib.Geometry.Convex.ConvexSpace.Defs

Goal state before:
pp: R : Type u_1
M : Type u_3
J : Type u_7
inst✝³ : PartialOrder R
inst✝² : Semiring R
inst✝¹ : IsStrictOrderedRing R
inst✝ : ConvexSpace R M
s t : R
hs : 0 ≤ s
ht : 0 ≤ t
h : s + t = 1
m : M
g : StdSimplex R J
e : J → M
⊢ convexCombPair s t hs ht h m (iConvexComb g e) =
    sConvexComb (convexCombPair s t hs ht h (StdSimplex.single m) (map e g))

Tactic:
by
  simpa using convexCombPair_iConvexComb_iConvexComb hs ht h g g (fun _ ↦ m) e

Goal state after:
Module: Mathlib.Geometry.Convex.ConvexSpace.Defs

Goal state before:
pp: R : Type u_1
M : Type u_3
inst✝³ : PartialOrder R
inst✝² : Semiring R
inst✝¹ : IsStrictOrderedRing R
inst✝ : ConvexSpace R M
s t : R
hs : 0 ≤ s
ht : 0 ≤ t
h : s + t = 1
s' t' : R
hs' : 0 ≤ s'
ht' : 0 ≤ t'
h' : s' + t' = 1
m₁ m₂ m₃ : M
⊢ convexCombPair s t hs ht h (convexCombPair s' t' hs' ht' h' m₁ m₂) m₃ =
    sConvexComb (convexCombPair s t hs ht h (duple m₁ m₂ hs' ht' h') (StdSimplex.single m₃))

Tactic:
by

Goal state after:
Module: Mathlib.Geometry.Convex.ConvexSpace.Defs

Goal state before:
pp: R : Type u_1
M : Type u_3
inst✝³ : PartialOrder R
inst✝² : Semiring R
inst✝¹ : IsStrictOrderedRing R
inst✝ : ConvexSpace R M
s t : R
hs : 0 ≤ s
ht : 0 ≤ t
h : s + t = 1
s' t' : R
hs' : 0 ≤ s'
ht' : 0 ≤ t'
h' : s' + t' = 1
m₁ m₂ m₃ : M
⊢ convexCombPair s t hs ht h m₁ (convexCombPair s' t' hs' ht' h' m₂ m₃) =
    sConvexComb (convexCombPair s t hs ht h (StdSimplex.single m₁) (duple m₂ m₃ hs' ht' h'))

Tactic:
by

Goal state after:
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)).2 ∈ t

Tactic:
by

Goal state after:
Module: Mathlib.Geometry.Convex.ConvexSpace.Defs

Goal state before:
pp: R : Type u_1
X : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
I : Type u_6
J : Type u_7
K : Type u_8
inst✝⁵ : PartialOrder R
inst✝⁴ : Semiring R
inst✝³ : IsStrictOrderedRing R
inst✝² : ConvexSpace R M
inst✝¹ : ConvexSpace R N
inst✝ : ConvexSpace R P
s t : R
hs : 0 ≤ s
ht : 0 ≤ t
h : s + t = 1
s' t' : R
hs' : 0 ≤ s'
ht' : 0 ≤ t'
h' : s' + t' = 1
s'' t'' : R
hs'' : 0 ≤ s''
ht'' : 0 ≤ t''
h'' : s'' + t'' = 1
H : t * s'' = s * t' * t''
m₁ m₂ m₃ : M
⊢ 0 ≤ s * s'

Tactic:
by

Goal state after:
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
⊢ IsStarConvexSet R (x, y) (s ×ˢ t)

Tactic:
by

Goal state after:
Module: Mathlib.Geometry.Convex.ConvexSpace.Defs

Goal state before:
pp: R : Type u_1
X : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
I : Type u_6
J : Type u_7
K : Type u_8
inst✝⁵ : PartialOrder R
inst✝⁴ : Semiring R
inst✝³ : IsStrictOrderedRing R
inst✝² : ConvexSpace R M
inst✝¹ : ConvexSpace R N
inst✝ : ConvexSpace R P
s t : R
hs : 0 ≤ s
ht : 0 ≤ t
h : s + t = 1
s' t' : R
hs' : 0 ≤ s'
ht' : 0 ≤ t'
h' : s' + t' = 1
s'' t'' : R
hs'' : 0 ≤ s''
ht'' : 0 ≤ t''
h'' : s'' + t'' = 1
H : t * s'' = s * t' * t''
m₁ m₂ m₃ : M
⊢ 0 ≤ s * t' + t

Tactic:
by

Goal state after:
Module: Mathlib.Geometry.Convex.Set

Goal state before:
pp: ι : Type u_1
R : Type u_3
X : Type u_5
inst✝³ : Semiring R
inst✝² : PartialOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : ConvexSpace R X
s : Set X
hs : IsConvexSet R s
w : StdSimplex R ι
f : ι → X
hf : ∀ (i : ι), w.weights i ≠ 0 → f i ∈ s
⊢ iConvexComb w f ∈ s

Tactic:
by

Goal state after:
Module: Mathlib.Geometry.Convex.Star

Goal state before:
pp: R : Type u_1
inst✝³ : Semiring R
inst✝² : PartialOrder R
inst✝¹ : IsStrictOrderedRing R
ι : Type u_6
X : ι → Type u_7
inst✝ : (i : ι) → ConvexSpace R (X i)
s : Set ι
x : (i : ι) → X i
t : (i : ι) → Set (X i)
ht : ∀ i ∈ s, IsStarConvexSet R (x i) (t i)
y : (i : ι) → X i
hy : y ∈ s.pi t
a b : R
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
i : ι
hi : i ∈ s
⊢ convexCombPair a b ha hb hab x y i ∈ t i

Tactic:
by

Goal state after:
Module: Mathlib.Geometry.Convex.ConvexSpace.Defs

Goal state before:
pp: R : Type u_1
X : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
I : Type u_6
J : Type u_7
K : Type u_8
inst✝⁵ : PartialOrder R
inst✝⁴ : Semiring R
inst✝³ : IsStrictOrderedRing R
inst✝² : ConvexSpace R M
inst✝¹ : ConvexSpace R N
inst✝ : ConvexSpace R P
s t : R
hs : 0 ≤ s
ht : 0 ≤ t
h : s + t = 1
s' t' : R
hs' : 0 ≤ s'
ht' : 0 ≤ t'
h' : s' + t' = 1
s'' t'' : R
hs'' : 0 ≤ s''
ht'' : 0 ≤ t''
h'' : s'' + t'' = 1
H : t * s'' = s * t' * t''
m₁ m₂ m₃ : M
⊢ s * s' + (s * t' + t) = 1

Tactic:
by

Goal state after:
Module: Mathlib.Geometry.Convex.Set

Goal state before:
pp: R : Type u_3
X : Type u_5
inst✝³ : Semiring R
inst✝² : PartialOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : ConvexSpace R X
s : Set X
x y : X
hs : IsConvexSet R s
hx : x ∈ s
hy : y ∈ s
a b : R
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ convexCombPair a b ha hb hab x y ∈ s

Tactic:
by

Goal state after:
Module: Mathlib.Geometry.Convex.Set

Goal state before:
pp: R : Type u_3
X : Type u_5
inst✝³ : Semiring R
inst✝² : PartialOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : ConvexSpace R X
⊢ IsConvexSet R ∅

Tactic:
by

Goal state after:
Module: Mathlib.Geometry.Convex.Set

Goal state before:
pp: R : Type u_3
X : Type u_5
inst✝³ : Semiring R
inst✝² : PartialOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : ConvexSpace R X
⊢ IsConvexSet R univ

Tactic:
by

Goal state after:
Module: Mathlib.Geometry.Convex.Set

Goal state before:
pp: R : Type u_3
X : Type u_5
inst✝³ : Semiring R
inst✝² : PartialOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : ConvexSpace R X
x : X
⊢ IsConvexSet R {x}

Tactic:
by

Goal state after:
Module: Mathlib.Geometry.Convex.Set

Goal state before:
pp: R : Type u_3
X : Type u_5
inst✝³ : Semiring R
inst✝² : PartialOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : ConvexSpace R X
s : Set X
hs : s.Subsingleton
⊢ IsConvexSet R s

Tactic:
by

Goal state after:
Module: Mathlib.Geometry.Convex.Set

Goal state before:
pp: R : Type u_3
X : Type u_5
inst✝³ : Semiring R
inst✝² : PartialOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : ConvexSpace R X
s t : Set X
hs : IsConvexSet R s
ht : IsConvexSet R t
⊢ IsConvexSet R (s ∩ t)

Tactic:
by

Goal state after:
Module: Mathlib.Geometry.Convex.Set

Goal state before:
pp: R : Type u_3
X : Type u_5
inst✝³ : Semiring R
inst✝² : PartialOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : ConvexSpace R X
S : Set (Set X)
hS : ∀ s ∈ S, IsConvexSet R s
⊢ IsConvexSet R (⋂₀ S)

Tactic:
by

Goal state after:
Module: Mathlib.Geometry.Convex.Set

Goal state before:
pp: R : Type u_3
X : Type u_5
inst✝³ : Semiring R
inst✝² : PartialOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : ConvexSpace R X
ι : Sort u_7
s : ι → Set X
hs : ∀ (i : ι), IsConvexSet R (s i)
⊢ IsConvexSet R (⋂ i, s i)

Tactic:
by

Goal state after: