mathlib-initiative/mathlib-tactics huggingface dataset:
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 α
s : Set E
f : α → E
g : E → ℝ
inst✝¹ : IsFiniteMeasure μ
inst✝ : NeZero μ
hg : ConcaveOn ℝ s g
hgc : ContinuousOn g s
hsc : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hfs : ∀ᵐ (x : α) ∂μ, f x ∈ s
hfi : Integrable f μ
hgi : Integrable (g ∘ f) μ
⊢ (⨍ (x : α), f x ∂μ, ⨍ (x : α), g (f x) ∂μ) ∈ {p | p.1 ∈ s ∧ p.2 ≤ g p.1}

Tactic:
simpa using

Goal state after:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : CompleteSpace E
μ : Measure α
s : Set E
f : α → E
g : E → ℝ
inst✝¹ : IsFiniteMeasure μ
inst✝ : NeZero μ
hg : ConcaveOn ℝ s g
hgc : ContinuousOn g s
hsc : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hfs : ∀ᵐ (x : α) ∂μ, f x ∈ s
hfi : Integrable f μ
hgi : Integrable (g ∘ f) μ
⊢ ⨍ (x : α), f x ∂μ ∈ s ∧ ⨍ (x : α), g (f x) ∂μ ≤ g (⨍ (x : α), f x ∂μ)
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 α
s : Set E
t : Set α
f : α → E
g : E → ℝ
hg : ConcaveOn ℝ s g
hgc : ContinuousOn g s
hsc : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
h0 : μ t ≠ 0
ht : μ t ≠ ∞
hfs : ∀ᵐ (x : α) ∂μ.restrict t, f x ∈ s
hfi : IntegrableOn f t μ
hgi : IntegrableOn (g ∘ f) t μ
⊢ (⨍ (x : α) in t, f x ∂μ, ⨍ (x : α) in t, g (f x) ∂μ) ∈ {p | p.1 ∈ s ∧ p.2 ≤ g p.1}

Tactic:
simpa using

Goal state after:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
μ : Measure α
s : Set E
t : Set α
f : α → E
g : E → ℝ
hg : ConcaveOn ℝ s g
hgc : ContinuousOn g s
hsc : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
h0 : μ t ≠ 0
ht : μ t ≠ ∞
hfs : ∀ᵐ (x : α) ∂μ.restrict t, f x ∈ s
hfi : IntegrableOn f t μ
hgi : IntegrableOn (g ∘ f) t μ
⊢ ⨍ (x : α) in t, f x ∂μ ∈ s ∧ ⨍ (x : α) in t, g (f x) ∂μ ≤ g (⨍ (x : α) in t, f x ∂μ)
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 α
s : Set E
f : α → E
g : E → ℝ
inst✝ : IsProbabilityMeasure μ
hg : ConvexOn ℝ s g
hgc : ContinuousOn g s
hsc : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hfs : ∀ᵐ (x : α) ∂μ, f x ∈ s
hfi : Integrable f μ
hgi : Integrable (g ∘ f) μ
⊢ g (∫ (x : α), f x ∂μ) ≤ ∫ (x : α), g (f x) ∂μ

Tactic:
simpa using

Goal state after:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
μ : Measure α
s : Set E
f : α → E
g : E → ℝ
inst✝ : IsProbabilityMeasure μ
hg : ConvexOn ℝ s g
hgc : ContinuousOn g s
hsc : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hfs : ∀ᵐ (x : α) ∂μ, f x ∈ s
hfi : Integrable f μ
hgi : Integrable (g ∘ f) μ
⊢ g (∫ (x : α), f x ∂μ) ≤ ∫ (x : α), g (f x) ∂μ
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 α
s : Set E
f : α → E
g : E → ℝ
inst✝ : IsProbabilityMeasure μ
hg : ConcaveOn ℝ s g
hgc : ContinuousOn g s
hsc : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hfs : ∀ᵐ (x : α) ∂μ, f x ∈ s
hfi : Integrable f μ
hgi : Integrable (g ∘ f) μ
⊢ ∫ (x : α), g (f x) ∂μ ≤ g (∫ (x : α), f x ∂μ)

Tactic:
simpa using

Goal state after:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
μ : Measure α
s : Set E
f : α → E
g : E → ℝ
inst✝ : IsProbabilityMeasure μ
hg : ConcaveOn ℝ s g
hgc : ContinuousOn g s
hsc : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hfs : ∀ᵐ (x : α) ∂μ, f x ∈ s
hfi : Integrable f μ
hgi : Integrable (g ∘ f) μ
⊢ ∫ (x : α), g (f x) ∂μ ≤ g (∫ (x : α), f x ∂μ)
Module: Mathlib.Analysis.Convex.Intrinsic

Goal state before:
pp: 𝕜 : Type u_1
V : Type u_2
W : Type u_3
Q : Type u_4
P : Type u_5
inst✝⁸ : Ring 𝕜
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module 𝕜 V
inst✝⁵ : TopologicalSpace P
inst✝⁴ : AddTorsor V P
inst✝³ : AddCommGroup W
inst✝² : Module 𝕜 W
inst✝¹ : TopologicalSpace Q
inst✝ : AddTorsor W Q
f : P → Q
s : Set P
e : ↥(affineSpan 𝕜 s) → ↥(affineSpan 𝕜 (f '' s))
he_homeo : IsHomeomorph e
he : ∀ (x : ↥(affineSpan 𝕜 s)), ↑(e x) = f ↑x
x : ↥(affineSpan 𝕜 s)
x✝ : x ∈ f ∘ Subtype.val ⁻¹' f '' s
w✝ : P
hy : w✝ ∈ s
hfy : f w✝ = (f ∘ Subtype.val) x
⊢ ↑(e x) = ↑(e ⟨w✝, ⋯⟩)

Tactic:
simpa using

Goal state after:
𝕜 : Type u_1
V : Type u_2
W : Type u_3
Q : Type u_4
P : Type u_5
inst✝⁸ : Ring 𝕜
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module 𝕜 V
inst✝⁵ : TopologicalSpace P
inst✝⁴ : AddTorsor V P
inst✝³ : AddCommGroup W
inst✝² : Module 𝕜 W
inst✝¹ : TopologicalSpace Q
inst✝ : AddTorsor W Q
f : P → Q
s : Set P
e : ↥(affineSpan 𝕜 s) → ↥(affineSpan 𝕜 (f '' s))
he_homeo : IsHomeomorph e
he : ∀ (x : ↥(affineSpan 𝕜 s)), ↑(e x) = f ↑x
x : ↥(affineSpan 𝕜 s)
x✝ : x ∈ f ∘ Subtype.val ⁻¹' f '' s
w✝ : P
hy : w✝ ∈ s
hfy : f w✝ = (f ∘ Subtype.val) x
⊢ f ↑x = f w✝
Module: Mathlib.Analysis.Convex.Continuous

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
C : Set E
f : E → ℝ
hC : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] C
hf : ConcaveOn ℝ C f
⊢ LocallyLipschitzOn C f ↔ ContinuousOn f C

Tactic:
simpa using

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
C : Set E
f : E → ℝ
hC : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] C
hf : ConcaveOn ℝ C f
⊢ LocallyLipschitzOn C f ↔ ContinuousOn f C
Module: Mathlib.Analysis.Convex.Continuous

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
C : Set E
f : E → ℝ
inst✝ : FiniteDimensional ℝ E
hC : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] C
hf : ConcaveOn ℝ C f
⊢ LocallyLipschitzOn C f

Tactic:
simpa using

Goal state after:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
C : Set E
f : E → ℝ
inst✝ : FiniteDimensional ℝ E
hC : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] C
hf : ConcaveOn ℝ C f
⊢ LocallyLipschitzOn C f
Module: Mathlib.Analysis.Convex.Continuous

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
f : E → ℝ
inst✝ : FiniteDimensional ℝ E
hf : ConvexOn ℝ univ f
⊢ LocallyLipschitz f

Tactic:
simpa using

Goal state after:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
f : E → ℝ
inst✝ : FiniteDimensional ℝ E
hf : ConvexOn ℝ univ f
⊢ LocallyLipschitz f
Module: Mathlib.Analysis.Convex.Continuous

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
f : E → ℝ
inst✝ : FiniteDimensional ℝ E
hf : ConcaveOn ℝ univ f
⊢ LocallyLipschitz f

Tactic:
simpa using

Goal state after:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
f : E → ℝ
inst✝ : FiniteDimensional ℝ E
hf : ConcaveOn ℝ univ f
⊢ LocallyLipschitz f
Module: Mathlib.Analysis.Convex.Continuous

Goal state before:
pp: f : ℝ → ℝ
y : ℝ
hf_cnv : ConcaveOn ℝ (Ici y) f
hf_cont : ContinuousWithinAt f (Ici y) y
⊢ ContinuousOn f (Ici y)

Tactic:
simpa using

Goal state after:
f : ℝ → ℝ
y : ℝ
hf_cnv : ConcaveOn ℝ (Ici y) f
hf_cont : ContinuousWithinAt f (Ici y) y
⊢ ContinuousOn f (Ici y)
Module: Mathlib.Analysis.Convex.Continuous

Goal state before:
pp: f : ℝ → ℝ
y : ℝ
hf_cnv : ConcaveOn ℝ (Iic y) f
hf_cont : ContinuousWithinAt f (Iic y) y
⊢ ContinuousOn f (Iic y)

Tactic:
simpa using

Goal state after:
f : ℝ → ℝ
y : ℝ
hf_cnv : ConcaveOn ℝ (Iic y) f
hf_cont : ContinuousWithinAt f (Iic y) y
⊢ ContinuousOn f (Iic y)
Module: Mathlib.Analysis.Convex.Continuous

Goal state before:
pp: f : ℝ → ℝ
y : ℝ
hf_cnv : ConcaveOn ℝ (Iic y) f
hf_cont : ContinuousWithinAt f (Iic y) y
⊢ ContinuousOn f (Iic y)

Tactic:
by
  simpa using hf_cnv.neg.continuousOn_Iic hf_cont.neg

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

Goal state before:
pp: f : ℝ → ℝ
y z : ℝ
hf_cnv : ConcaveOn ℝ (Ioc y z) f
hf_cont : ContinuousWithinAt f (Iic z) z
⊢ ContinuousOn f (Ioc y z)

Tactic:
simpa using

Goal state after:
f : ℝ → ℝ
y z : ℝ
hf_cnv : ConcaveOn ℝ (Ioc y z) f
hf_cont : ContinuousWithinAt f (Iic z) z
⊢ ContinuousOn f (Ioc y z)
Module: Mathlib.Analysis.Convex.Continuous

Goal state before:
pp: f : ℝ → ℝ
y z : ℝ
hf_cnv : ConcaveOn ℝ (Ico y z) f
hf_cont : ContinuousWithinAt f (Ici y) y
⊢ ContinuousOn f (Ico y z)

Tactic:
simpa using

Goal state after:
f : ℝ → ℝ
y z : ℝ
hf_cnv : ConcaveOn ℝ (Ico y z) f
hf_cont : ContinuousWithinAt f (Ici y) y
⊢ ContinuousOn f (Ico y z)
Module: Mathlib.Analysis.Convex.Continuous

Goal state before:
pp: f : ℝ → ℝ
y z : ℝ
hf_cnv : ConcaveOn ℝ (Icc y z) f
hyz : y < z
hfy : ContinuousWithinAt f (Ici y) y
hfz : ContinuousWithinAt f (Iic z) z
⊢ ContinuousOn f (Icc y z)

Tactic:
simpa using

Goal state after:
f : ℝ → ℝ
y z : ℝ
hf_cnv : ConcaveOn ℝ (Icc y z) f
hyz : y < z
hfy : ContinuousWithinAt f (Ici y) y
hfz : ContinuousWithinAt f (Iic z) z
⊢ ContinuousOn f (Icc y z)
Module: Mathlib.Geometry.Convex.ConvexSpace.Defs

Goal state before:
pp: case e_b
R : Type u
inst✝² : PartialOrder R
inst✝¹ : Semiring R
M : Type u_9
w : StdSimplex R M
x : M
inst✝ : IsStrictOrderedRing R
a : R
ha : a ≠ 0
hwa : w.weights = Finsupp.single x a
⊢ a = 1

Tactic:
simpa using

Goal state after:
case e_b
R : Type u
inst✝² : PartialOrder R
inst✝¹ : Semiring R
M : Type u_9
w : StdSimplex R M
x : M
inst✝ : IsStrictOrderedRing R
a : R
ha : a ≠ 0
hwa : w.weights = Finsupp.single x a
⊢ a = 1
Module: Mathlib.Geometry.Convex.ConvexSpace.Defs

Goal state before:
pp: R : Type u
inst✝² : PartialOrder R
inst✝¹ : Semiring R
M : Type u_9
N : Type u_10
inst✝ : IsStrictOrderedRing R
f : StdSimplex R M
x : N
⊢ map (fun x_1 ↦ x) f = single x

Tactic:
ext a; by_cases x = a <;> simp [*, mapDomain]

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 α
s : Set E
f : α → E
g : E → ℝ
inst✝ : IsFiniteMeasure μ
hg : StrictConvexOn ℝ s g
hgc : ContinuousOn g s
hsc : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hfs : ∀ᵐ (x : α) ∂μ, f x ∈ s
hfi : Integrable f μ
hgi : Integrable (g ∘ f) μ
⊢ f =ᵐ[μ] const α (⨍ (x : α), f x ∂μ) ∨ g (⨍ (x : α), f x ∂μ) < ⨍ (x : α), g (f x) ∂μ

Tactic:
have : ∀ {t}, μ t ≠ 0 → (⨍ x in t, f x ∂μ) ∈ s ∧ g (⨍ x in t, f x ∂μ) ≤ ⨍ x in t, g (f x) ∂μ :=
    fun ht =>
    hg.convexOn.set_average_mem_epigraph hgc hsc ht (by finiteness) (ae_restrict_of_ae hfs)
      hfi.integrableOn hgi.integrableOn
  refine (ae_eq_const_or_exists_average_ne_compl hfi).imp_right ?_
  rintro ⟨t, hm, h₀, h₀', hne⟩
  rcases average_mem_openSegment_compl_self hm.nullMeasurableSet h₀ h₀' (hfi.prodMk hgi) with
    ⟨a, b, ha, hb, hab, h_avg⟩
  rw [average_pair hfi hgi, average_pair hfi.integrableOn hgi.integrableOn,
    average_pair hfi.integrableOn hgi.integrableOn, Prod.smul_mk,
    Prod.smul_mk, Prod.mk_add_mk, Prod.mk_inj] at h_avg
  simp only [Function.comp] at h_avg
  rw [← h_avg.1, ← h_avg.2]
  calc
    g ((a • ⨍ x in t, f x ∂μ) + b • ⨍ x in tᶜ, f x ∂μ) <
        a * g (⨍ x in t, f x ∂μ) + b * g (⨍ x in tᶜ, f x ∂μ) :=
      hg.2 (this h₀).1 (this h₀').1 hne ha hb hab
    _ ≤ (a * ⨍ x in t, g (f x) ∂μ) + b * ⨍ x in tᶜ, g (f x) ∂μ := by
      gcongr
      exacts [(this h₀).2, (this h₀').2]

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 α
s : Set E
f : α → E
g : E → ℝ
inst✝ : IsFiniteMeasure μ
hg : StrictConcaveOn ℝ s g
hgc : ContinuousOn g s
hsc : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hfs : ∀ᵐ (x : α) ∂μ, f x ∈ s
hfi : Integrable f μ
hgi : Integrable (g ∘ f) μ
⊢ f =ᵐ[μ] const α (⨍ (x : α), f x ∂μ) ∨ ⨍ (x : α), g (f x) ∂μ < g (⨍ (x : α), f x ∂μ)

Tactic:
simpa using

Goal state after:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
μ : Measure α
s : Set E
f : α → E
g : E → ℝ
inst✝ : IsFiniteMeasure μ
hg : StrictConcaveOn ℝ s g
hgc : ContinuousOn g s
hsc : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hfs : ∀ᵐ (x : α) ∂μ, f x ∈ s
hfi : Integrable f μ
hgi : Integrable (g ∘ f) μ
⊢ f =ᵐ[μ] const α (⨍ (x : α), f x ∂μ) ∨ ⨍ (x : α), g (f x) ∂μ < g (⨍ (x : α), f x ∂μ)
Module: Mathlib.Geometry.Convex.ConvexSpace.Defs

Goal state before:
pp: X : Type u_2
K : Type u_8
inst✝³ : Semifield K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : IsDomain K
w : StdSimplex K X
a✝ : X
hx : ∃ x ∈ {a✝}, w.weights x ≠ 0
⊢ ¬w.weights a✝ = 0

Tactic:
simpa using

Goal state after:
X : Type u_2
K : Type u_8
inst✝³ : Semifield K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : IsDomain K
w : StdSimplex K X
a✝ : X
hx : ∃ x ∈ {a✝}, w.weights x ≠ 0
⊢ ¬w.weights a✝ = 0
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:
simpa using

Goal state after:
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
Module: Mathlib.Analysis.Convex.Integral

Goal state before:
pp: case pos.inr
α : 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
hC0 : 0 < C
hfi : Integrable f μ
hμt : μ univ < ∞
this : IsFiniteMeasure μ
h_le : ∀ᵐ (x : α) ∂μ, f x ∈ closedBall 0 C
⊢ f =ᵐ[μ] const α (⨍ (x : α), f x ∂μ) ∨ ‖⨍ (x : α), f x ∂μ‖ < C

Tactic:
simpa using

Goal state after:
case pos.inr
α : 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
hC0 : 0 < C
hfi : Integrable f μ
hμt : μ univ < ∞
this : IsFiniteMeasure μ
h_le : ∀ᵐ (x : α) ∂μ, f x ∈ closedBall 0 C
⊢ f =ᵐ[μ] const α (⨍ (x : α), f x ∂μ) ∨ ‖⨍ (x : α), f x ∂μ‖ < C
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:
rintro y ⟨s, hs, hy⟩ a ha b hb hab; exact ⟨s, hs, hS _ hs hy _ ..⟩

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
y : X
hy : y ∈ s
⊢ x ∈ s

Tactic:
simpa using

Goal state after:
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
y : X
hy : y ∈ s
⊢ x ∈ s
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:
simpa using

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
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 (f x) (f y) ∈ s
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:
simpa using

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 w ∈ s
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:
simpa using

Goal state after:
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))
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:
simpa using

Goal state after:
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))
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:
simpa using

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 y z ∈ t
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:
simpa using

Goal state after:
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 i) (y i) ∈ t i
Module: Mathlib.Geometry.Convex.ConvexSpace.Defs

Goal state before:
pp: R : Type u_9
M : Type u_10
I : Type u_11
inst✝³ : PartialOrder R
inst✝² : CommSemiring R
inst✝¹ : IsStrictOrderedRing R
inst✝ : ConvexSpace R M
s t : R
hs : 0 ≤ s
ht : 0 ≤ t
h : s + t = 1
f : StdSimplex R I
m : M
e : I → M
⊢ (iConvexComb f fun x ↦ convexCombPair s t hs ht h (e x) m) = convexCombPair s t hs ht h (iConvexComb f e) m

Tactic:
simpa using

Goal state after:
R : Type u_9
M : Type u_10
I : Type u_11
inst✝³ : PartialOrder R
inst✝² : CommSemiring R
inst✝¹ : IsStrictOrderedRing R
inst✝ : ConvexSpace R M
s t : R
hs : 0 ≤ s
ht : 0 ≤ t
h : s + t = 1
f : StdSimplex R I
m : M
e : I → M
⊢ (iConvexComb f fun x ↦ convexCombPair s t hs ht h (e x) m) = convexCombPair s t hs ht h (iConvexComb f e) m
Module: Mathlib.Geometry.Convex.ConvexSpace.Defs

Goal state before:
pp: R : Type u_9
M : Type u_10
I : Type u_11
inst✝³ : PartialOrder R
inst✝² : CommSemiring R
inst✝¹ : IsStrictOrderedRing R
inst✝ : ConvexSpace R M
s t : R
hs : 0 ≤ s
ht : 0 ≤ t
h : s + t = 1
f : StdSimplex R I
m : M
e : I → M
⊢ (iConvexComb f fun x ↦ convexCombPair s t hs ht h m (e x)) = convexCombPair s t hs ht h m (iConvexComb f e)

Tactic:
simpa using

Goal state after:
R : Type u_9
M : Type u_10
I : Type u_11
inst✝³ : PartialOrder R
inst✝² : CommSemiring R
inst✝¹ : IsStrictOrderedRing R
inst✝ : ConvexSpace R M
s t : R
hs : 0 ≤ s
ht : 0 ≤ t
h : s + t = 1
f : StdSimplex R I
m : M
e : I → M
⊢ (iConvexComb f fun x ↦ convexCombPair s t hs ht h m (e x)) = convexCombPair s t hs ht h m (iConvexComb f e)
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
⊢ w.weights x ≠ 0

Tactic:
simpa using

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
⊢ ¬w.weights x = 0