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
t : Set α
f : α → E
inst✝ : IsFiniteMeasure μ
hs : Convex ℝ s
h0 : μ (toMeasurable μ t) ≠ 0
hfs : ∀ᵐ (x : α) ∂μ, f x ∈ s
hfi : Integrable f μ
ht : ⨍ (x : α) in t, f x ∂μ ∈ interior s
⊢ ⨍ (x : α), f x ∂μ ∈ interior s

Tactic:
]

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
inst✝ : IsFiniteMeasure μ
hs : Convex ℝ s
h0 : μ (toMeasurable μ t) ≠ 0
hfs : ∀ᵐ (x : α) ∂μ, f x ∈ s
hfi : Integrable f μ
ht : ⨍ (x : α) in t, f x ∂μ ∈ interior s
⊢ ⨍ (x : α), f x ∂μ ∈ interior s
Module: Mathlib.Analysis.Convex.Measure

Goal state before:
pp: E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
s : Set E
hs : Convex ℝ s
x : E
hx : x ∈ interior s
H : ∀ (t : Set E), Convex ℝ t → x ∈ interior t → Bornology.IsBounded t → μ (frontier t) = 0
B : ℕ → Set E := fun n ↦ ball x (↑n + 1)
y : E
hy : y ∈ frontier s
N : ℕ := ⌊dist y x⌋₊
hN : y ∈ B N
⊢ y ∈ frontier s ∩ ball x (↑N + 1)

Tactic:
]

Goal state after:
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
s : Set E
hs : Convex ℝ s
x : E
hx : x ∈ interior s
H : ∀ (t : Set E), Convex ℝ t → x ∈ interior t → Bornology.IsBounded t → μ (frontier t) = 0
B : ℕ → Set E := fun n ↦ ball x (↑n + 1)
y : E
hy : y ∈ frontier s
N : ℕ := ⌊dist y x⌋₊
hN : y ∈ B N
⊢ y ∈ frontier s ∩ ball x (↑N + 1)
Module: Mathlib.Analysis.Convex.Intrinsic

Goal state before:
pp: case inr
𝕜 : 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 : [Nonempty ↑s] → ↥(affineSpan 𝕜 s) → ↥(affineSpan 𝕜 (f '' s))
he_homeo : ∀ [inst : Nonempty ↑s], IsHomeomorph e
he : ∀ [inst : Nonempty ↑s] (x : ↥(affineSpan 𝕜 s)), ↑(e x) = f ↑x
hs : s.Nonempty
this : Nonempty ↑s
⊢ f '' Subtype.val '' interior (Subtype.val ⁻¹' s) = f '' intrinsicInterior 𝕜 s

Tactic:
]

Goal state after:
case inr
𝕜 : 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 : [Nonempty ↑s] → ↥(affineSpan 𝕜 s) → ↥(affineSpan 𝕜 (f '' s))
he_homeo : ∀ [inst : Nonempty ↑s], IsHomeomorph e
he : ∀ [inst : Nonempty ↑s] (x : ↥(affineSpan 𝕜 s)), ↑(e x) = f ↑x
hs : s.Nonempty
this : Nonempty ↑s
⊢ f '' Subtype.val '' interior (Subtype.val ⁻¹' s) = f '' intrinsicInterior 𝕜 s
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
inst✝ : IsFiniteMeasure μ
hs : Convex ℝ s
h0 : μ (toMeasurable μ t) ≠ 0
hfs : ∀ᵐ (x : α) ∂μ, f x ∈ s
hfi : Integrable f μ
ht : ⨍ (x : α) in toMeasurable μ t, f x ∂μ ∈ interior s
⊢ ⨍ (x : α), f x ∂μ ∈ interior s

Tactic:
]

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
inst✝ : IsFiniteMeasure μ
hs : Convex ℝ s
h0 : μ (toMeasurable μ t) ≠ 0
hfs : ∀ᵐ (x : α) ∂μ, f x ∈ s
hfi : Integrable f μ
ht : ⨍ (x : α) in toMeasurable μ t, f x ∂μ ∈ interior s
⊢ ⨍ (x : α), f x ∂μ ∈ interior s
Module: Mathlib.Analysis.Convex.Integral

Goal state before:
pp: case pos
α : 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
inst✝ : IsFiniteMeasure μ
hs : Convex ℝ s
h0 : μ (toMeasurable μ t) ≠ 0
hfs : ∀ᵐ (x : α) ∂μ, f x ∈ s
hfi : Integrable f μ
ht : ⨍ (x : α) in toMeasurable μ t, f x ∂μ ∈ interior s
h0' : toMeasurable μ t =ᵐ[μ] univ
⊢ ⨍ (x : α), f x ∂μ ∈ interior s

Tactic:
]

Goal state after:
case pos
α : 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
inst✝ : IsFiniteMeasure μ
hs : Convex ℝ s
h0 : μ (toMeasurable μ t) ≠ 0
hfs : ∀ᵐ (x : α) ∂μ, f x ∈ s
hfi : Integrable f μ
ht : ⨍ (x : α) in toMeasurable μ t, f x ∂μ ∈ interior s
h0' : toMeasurable μ t =ᵐ[μ] univ
⊢ ⨍ (x : α), f x ∂μ ∈ interior s
Module: Mathlib.Analysis.Convex.Integral

Goal state before:
pp: case pos
α : 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
inst✝ : IsFiniteMeasure μ
hs : Convex ℝ s
h0 : μ (toMeasurable μ t) ≠ 0
hfs : ∀ᵐ (x : α) ∂μ, f x ∈ s
hfi : Integrable f μ
ht : ⨍ (x : α), f x ∂μ ∈ interior s
h0' : toMeasurable μ t =ᵐ[μ] univ
⊢ ⨍ (x : α), f x ∂μ ∈ interior s

Tactic:
]

Goal state after:
case pos
α : 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
inst✝ : IsFiniteMeasure μ
hs : Convex ℝ s
h0 : μ (toMeasurable μ t) ≠ 0
hfs : ∀ᵐ (x : α) ∂μ, f x ∈ s
hfi : Integrable f μ
ht : ⨍ (x : α), f x ∂μ ∈ interior s
h0' : toMeasurable μ t =ᵐ[μ] univ
⊢ ⨍ (x : α), f x ∂μ ∈ interior s
Module: Mathlib.Analysis.Convex.Measure

Goal state before:
pp: E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
s✝ : Set E
hs✝ : Convex ℝ s✝
x : E
hx✝ : x ∈ interior s✝
s : Set E
hs : Convex ℝ s
hx : x ∈ interior s
hb : μ (interior s) ≠ ∞
this : μ (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s) ≤ μ (interior s)
⊢ μ (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s) ≤ μ (interior s)

Tactic:
]

Goal state after:
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
s✝ : Set E
hs✝ : Convex ℝ s✝
x : E
hx✝ : x ∈ interior s✝
s : Set E
hs : Convex ℝ s
hx : x ∈ interior s
hb : μ (interior s) ≠ ∞
this : μ (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s) ≤ μ (interior s)
⊢ μ (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s) ≤ μ (interior s)
Module: Mathlib.Analysis.Convex.Intrinsic

Goal state before:
pp: case inr
𝕜 : 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 : [Nonempty ↑s] → ↥(affineSpan 𝕜 s) → ↥(affineSpan 𝕜 (f '' s))
he_homeo : ∀ [inst : Nonempty ↑s], IsHomeomorph e
he : ∀ [inst : Nonempty ↑s] (x : ↥(affineSpan 𝕜 s)), ↑(e x) = f ↑x
hs : s.Nonempty
this : Nonempty ↑s
⊢ f '' Subtype.val '' frontier (Subtype.val ⁻¹' s) = f '' intrinsicFrontier 𝕜 s

Tactic:
]

Goal state after:
case inr
𝕜 : 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 : [Nonempty ↑s] → ↥(affineSpan 𝕜 s) → ↥(affineSpan 𝕜 (f '' s))
he_homeo : ∀ [inst : Nonempty ↑s], IsHomeomorph e
he : ∀ [inst : Nonempty ↑s] (x : ↥(affineSpan 𝕜 s)), ↑(e x) = f ↑x
hs : s.Nonempty
this : Nonempty ↑s
⊢ f '' Subtype.val '' frontier (Subtype.val ⁻¹' s) = f '' intrinsicFrontier 𝕜 s
Module: Mathlib.Analysis.Convex.Measure

Goal state before:
pp: E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
s✝ : Set E
hs✝ : Convex ℝ s✝
x : E
hx✝ : x ∈ interior s✝
s : Set E
hs : Convex ℝ s
hx : x ∈ interior s
hb : μ (interior s) ≠ ∞
d : ℕ := finrank ℝ E
r : ℝ≥0
hr : 1 < r
⊢ ↑(r ^ finrank ℝ E) * μ (interior s) = ↑(r ^ d) * μ (interior s)

Tactic:
]

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

Goal state before:
pp: case inr
f : ℝ → ℝ
y : ℝ
hf_cvx : ConvexOn ℝ (Ici y) f
hf_cont : ContinuousWithinAt f (Ici y) y
x : ℝ
hx : x ∈ Ici y
hxy : y < x
h : y < x → ContinuousAt f x
⊢ ContinuousWithinAt f (Ici y) x

Tactic:
]

Goal state after:
case inr
f : ℝ → ℝ
y : ℝ
hf_cvx : ConvexOn ℝ (Ici y) f
hf_cont : ContinuousWithinAt f (Ici y) y
x : ℝ
hx : x ∈ Ici y
hxy : y < x
h : y < x → ContinuousAt f x
⊢ ContinuousWithinAt f (Ici y) x
Module: Mathlib.Analysis.Convex.Intrinsic

Goal state before:
pp: case inr
𝕜 : 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 : [Nonempty ↑s] → ↥(affineSpan 𝕜 s) → ↥(affineSpan 𝕜 (f '' s))
he_homeo : ∀ [inst : Nonempty ↑s], IsHomeomorph e
he : ∀ [inst : Nonempty ↑s] (x : ↥(affineSpan 𝕜 s)), ↑(e x) = f ↑x
hs : s.Nonempty
this : Nonempty ↑s
⊢ f '' Subtype.val '' closure[instTopologicalSpaceSubtype] (Subtype.val ⁻¹' s) = f '' intrinsicClosure 𝕜 s

Tactic:
]

Goal state after:
case inr
𝕜 : 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 : [Nonempty ↑s] → ↥(affineSpan 𝕜 s) → ↥(affineSpan 𝕜 (f '' s))
he_homeo : ∀ [inst : Nonempty ↑s], IsHomeomorph e
he : ∀ [inst : Nonempty ↑s] (x : ↥(affineSpan 𝕜 s)), ↑(e x) = f ↑x
hs : s.Nonempty
this : Nonempty ↑s
⊢ f '' Subtype.val '' closure[instTopologicalSpaceSubtype] (Subtype.val ⁻¹' s) = f '' intrinsicClosure 𝕜 s
Module: Mathlib.Analysis.Convex.Continuous

Goal state before:
pp: case inr
f : ℝ → ℝ
y : ℝ
hf_cvx : ConvexOn ℝ (Iic y) f
hf_cont : ContinuousWithinAt f (Iic y) y
x : ℝ
hx : x ∈ Iic y
hxy : x < y
h : x < y → ContinuousAt f x
⊢ ContinuousWithinAt f (Iic y) x

Tactic:
]

Goal state after:
case inr
f : ℝ → ℝ
y : ℝ
hf_cvx : ConvexOn ℝ (Iic y) f
hf_cont : ContinuousWithinAt f (Iic y) y
x : ℝ
hx : x ∈ Iic y
hxy : x < y
h : x < y → ContinuousAt f x
⊢ ContinuousWithinAt f (Iic y) x
Module: Mathlib.Analysis.Convex.Continuous

Goal state before:
pp: case inl
f : ℝ → ℝ
y x : ℝ
hf_cvx : ConvexOn ℝ (Ioc y x) f
hf_cont : ContinuousWithinAt f (Iic x) x
hx : x ∈ Ioc y x
⊢ ContinuousWithinAt f (Iic x) x

Tactic:
]

Goal state after:
case inl
f : ℝ → ℝ
y x : ℝ
hf_cvx : ConvexOn ℝ (Ioc y x) f
hf_cont : ContinuousWithinAt f (Iic x) x
hx : x ∈ Ioc y x
⊢ ContinuousWithinAt f (Iic x) x
Module: Mathlib.Analysis.Convex.Continuous

Goal state before:
pp: case inr
f : ℝ → ℝ
y z : ℝ
hf_cvx : ConvexOn ℝ (Ioc y z) f
hf_cont : ContinuousWithinAt f (Iic z) z
x : ℝ
hx : x ∈ Ioc y z
hxz : x < z
h : ContinuousAt f x
⊢ ContinuousWithinAt f (Ioc y z) x

Tactic:
]

Goal state after:
case inr
f : ℝ → ℝ
y z : ℝ
hf_cvx : ConvexOn ℝ (Ioc y z) f
hf_cont : ContinuousWithinAt f (Iic z) z
x : ℝ
hx : x ∈ Ioc y z
hxz : x < z
h : ContinuousAt f x
⊢ ContinuousWithinAt f (Ioc y z) x
Module: Mathlib.Analysis.Convex.Continuous

Goal state before:
pp: case inl
f : ℝ → ℝ
y z : ℝ
hf_cvx : ConvexOn ℝ (Ico y z) f
hf_cont : ContinuousWithinAt f (Ici y) y
hx : y ∈ Ico y z
⊢ ContinuousWithinAt f (Ici y) y

Tactic:
]

Goal state after:
case inl
f : ℝ → ℝ
y z : ℝ
hf_cvx : ConvexOn ℝ (Ico y z) f
hf_cont : ContinuousWithinAt f (Ici y) y
hx : y ∈ Ico y z
⊢ ContinuousWithinAt f (Ici y) y
Module: Mathlib.Analysis.Convex.Continuous

Goal state before:
pp: case inr
f : ℝ → ℝ
y z : ℝ
hf_cvx : ConvexOn ℝ (Ico y z) f
hf_cont : ContinuousWithinAt f (Ici y) y
x : ℝ
hx : x ∈ Ico y z
hyx : y < x
h : ContinuousAt f x
⊢ ContinuousWithinAt f (Ico y z) x

Tactic:
]

Goal state after:
case inr
f : ℝ → ℝ
y z : ℝ
hf_cvx : ConvexOn ℝ (Ico y z) f
hf_cont : ContinuousWithinAt f (Ici y) y
x : ℝ
hx : x ∈ Ico y z
hyx : y < x
h : ContinuousAt f x
⊢ ContinuousWithinAt f (Ico y z) x
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:
by
  simpa using hf_cnv.neg.continuousOn_Ico hf_cont.neg

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) μ
this : ∀ {t : Set α}, μ t ≠ 0 → ⨍ (x : α) in t, f x ∂μ ∈ s ∧ g (⨍ (x : α) in t, f x ∂μ) ≤ ⨍ (x : α) in t, g (f x) ∂μ
t : Set α
hm : MeasurableSet t
h₀ : μ t ≠ 0
h₀' : μ tᶜ ≠ 0
hne : ⨍ (x : α) in t, f x ∂μ ≠ ⨍ (x : α) in tᶜ, f x ∂μ
a b : ℝ
ha : 0 < a
hb : 0 < b
hab : a + b = 1
h_avg :
  a • ⨍ (x : α) in t, f x ∂μ + b • ⨍ (x : α) in tᶜ, f x ∂μ = ⨍ (x : α), f x ∂μ ∧
    a • ⨍ (x : α) in t, (g ∘ f) x ∂μ + b • ⨍ (x : α) in tᶜ, (g ∘ f) x ∂μ = ⨍ (x : α), (g ∘ f) x ∂μ
⊢ g (⨍ (x : α), f x ∂μ) < ⨍ (x : α), g (f x) ∂μ

Tactic:
]

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 : 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) μ
this : ∀ {t : Set α}, μ t ≠ 0 → ⨍ (x : α) in t, f x ∂μ ∈ s ∧ g (⨍ (x : α) in t, f x ∂μ) ≤ ⨍ (x : α) in t, g (f x) ∂μ
t : Set α
hm : MeasurableSet t
h₀ : μ t ≠ 0
h₀' : μ tᶜ ≠ 0
hne : ⨍ (x : α) in t, f x ∂μ ≠ ⨍ (x : α) in tᶜ, f x ∂μ
a b : ℝ
ha : 0 < a
hb : 0 < b
hab : a + b = 1
h_avg :
  a • ⨍ (x : α) in t, f x ∂μ + b • ⨍ (x : α) in tᶜ, f x ∂μ = ⨍ (x : α), f x ∂μ ∧
    a • ⨍ (x : α) in t, (g ∘ f) x ∂μ + b • ⨍ (x : α) in tᶜ, (g ∘ f) x ∂μ = ⨍ (x : α), (g ∘ f) x ∂μ
⊢ g (⨍ (x : α), f x ∂μ) < ⨍ (x : α), g (f x) ∂μ
Module: Mathlib.Analysis.Convex.Continuous

Goal state before:
pp: case inr.inr
f : ℝ → ℝ
y z : ℝ
hf_cvx : ConvexOn ℝ (Icc y z) f
hyz : y < z
hfy : ContinuousWithinAt f (Ici y) y
hfz : ContinuousWithinAt f (Iic z) z
this : ContinuousOn f (Ico y z) ∧ ContinuousOn f (Ioc y z)
x : ℝ
hx✝ : x ∈ Icc y z
hyx : y < x
hxz : x < z
hx : ContinuousAt f x
⊢ ContinuousWithinAt f (Icc y z) x

Tactic:
]

Goal state after:
case inr.inr
f : ℝ → ℝ
y z : ℝ
hf_cvx : ConvexOn ℝ (Icc y z) f
hyz : y < z
hfy : ContinuousWithinAt f (Ici y) y
hfz : ContinuousWithinAt f (Iic z) z
this : ContinuousOn f (Ico y z) ∧ ContinuousOn f (Ioc y z)
x : ℝ
hx✝ : x ∈ Icc y z
hyx : y < x
hxz : x < z
hx : ContinuousAt f x
⊢ ContinuousWithinAt f (Icc y z) x
Module: Mathlib.Geometry.Convex.ConvexSpace.Defs

Goal state before:
pp: R : Type u
inst✝² : PartialOrder R
inst✝¹ : Semiring R
M : Type u_9
w : StdSimplex R M
x : M
inst✝ : IsStrictOrderedRing R
⊢ (∃ b, b ≠ 0 ∧ w.weights = Finsupp.single x b) → w = single x

Tactic:
]

Goal state after:
R : Type u
inst✝² : PartialOrder R
inst✝¹ : Semiring R
M : Type u_9
w : StdSimplex R M
x : M
inst✝ : IsStrictOrderedRing R
⊢ (∃ b, b ≠ 0 ∧ w.weights = Finsupp.single x b) → w = single x
Module: Mathlib.Analysis.Convex.Intrinsic

Goal state before:
pp: 𝕜 : Type u_1
V : Type u_2
inst✝⁶ : Field 𝕜
inst✝⁵ : LinearOrder 𝕜
inst✝⁴ : AddCommGroup V
inst✝³ : Module 𝕜 V
inst✝² : TopologicalSpace V
inst✝¹ : IsTopologicalAddGroup V
inst✝ : ContinuousConstSMul 𝕜 V
s : Set V
hs : Convex 𝕜 s
⊢ Convex 𝕜 (closure[inst✝²] s ∩ ↑(affineSpan 𝕜 s))

Tactic:
]

Goal state after:
𝕜 : Type u_1
V : Type u_2
inst✝⁶ : Field 𝕜
inst✝⁵ : LinearOrder 𝕜
inst✝⁴ : AddCommGroup V
inst✝³ : Module 𝕜 V
inst✝² : TopologicalSpace V
inst✝¹ : IsTopologicalAddGroup V
inst✝ : ContinuousConstSMul 𝕜 V
s : Set V
hs : Convex 𝕜 s
⊢ Convex 𝕜 (closure[inst✝²] s ∩ ↑(affineSpan 𝕜 s))
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) μ
this : ∀ {t : Set α}, μ t ≠ 0 → ⨍ (x : α) in t, f x ∂μ ∈ s ∧ g (⨍ (x : α) in t, f x ∂μ) ≤ ⨍ (x : α) in t, g (f x) ∂μ
t : Set α
hm : MeasurableSet t
h₀ : μ t ≠ 0
h₀' : μ tᶜ ≠ 0
hne : ⨍ (x : α) in t, f x ∂μ ≠ ⨍ (x : α) in tᶜ, f x ∂μ
a b : ℝ
ha : 0 < a
hb : 0 < b
hab : a + b = 1
h_avg :
  a • ⨍ (x : α) in t, f x ∂μ + b • ⨍ (x : α) in tᶜ, f x ∂μ = ⨍ (x : α), f x ∂μ ∧
    a • ⨍ (x : α) in t, g (f x) ∂μ + b • ⨍ (x : α) in tᶜ, g (f x) ∂μ = ⨍ (x : α), g (f x) ∂μ
⊢ g (a • ⨍ (x : α) in t, f x ∂μ + b • ⨍ (x : α) in tᶜ, f x ∂μ) <
    a • ⨍ (x : α) in t, g (f x) ∂μ + b • ⨍ (x : α) in tᶜ, g (f x) ∂μ

Tactic:
]

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 : 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) μ
this : ∀ {t : Set α}, μ t ≠ 0 → ⨍ (x : α) in t, f x ∂μ ∈ s ∧ g (⨍ (x : α) in t, f x ∂μ) ≤ ⨍ (x : α) in t, g (f x) ∂μ
t : Set α
hm : MeasurableSet t
h₀ : μ t ≠ 0
h₀' : μ tᶜ ≠ 0
hne : ⨍ (x : α) in t, f x ∂μ ≠ ⨍ (x : α) in tᶜ, f x ∂μ
a b : ℝ
ha : 0 < a
hb : 0 < b
hab : a + b = 1
h_avg :
  a • ⨍ (x : α) in t, f x ∂μ + b • ⨍ (x : α) in tᶜ, f x ∂μ = ⨍ (x : α), f x ∂μ ∧
    a • ⨍ (x : α) in t, g (f x) ∂μ + b • ⨍ (x : α) in tᶜ, g (f x) ∂μ = ⨍ (x : α), g (f x) ∂μ
⊢ g (a • ⨍ (x : α) in t, f x ∂μ + b • ⨍ (x : α) in tᶜ, f x ∂μ) <
    a • ⨍ (x : α) in t, g (f x) ∂μ + b • ⨍ (x : α) in tᶜ, g (f x) ∂μ
Module: Mathlib.Analysis.Convex.Intrinsic

Goal state before:
pp: α : Type u_6
β : Type u_7
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
φ : α ≃ₜ β
s : Set β
⊢ (interior s).Nonempty ↔ (⇑φ.symm '' interior s).Nonempty

Tactic:
image_nonempty

Goal state after:
α : Type u_6
β : Type u_7
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
φ : α ≃ₜ β
s : Set β
⊢ (interior s).Nonempty ↔ (interior s).Nonempty
Module: Mathlib.Analysis.Convex.Intrinsic

Goal state before:
pp: α : Type u_6
β : Type u_7
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
φ : α ≃ₜ β
s : Set β
⊢ (interior s).Nonempty ↔ (interior s).Nonempty

Tactic:
]

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

Goal state before:
pp: R : Type u_1
V : Type u_2
P : Type u_3
inst✝⁵ : Ring R
inst✝⁴ : PartialOrder R
inst✝³ : IsStrictOrderedRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AffineSpace V P
x : P
⊢ (Finset.affineCombination R {x} id) ⇑(Finsupp.single x 1) = x

Tactic:
]

Goal state after:
R : Type u_1
V : Type u_2
P : Type u_3
inst✝⁵ : Ring R
inst✝⁴ : PartialOrder R
inst✝³ : IsStrictOrderedRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AffineSpace V P
x : P
⊢ (Finset.affineCombination R {x} id) ⇑(Finsupp.single x 1) = x
Module: Mathlib.Analysis.Convex.Intrinsic

Goal state before:
pp: V : Type u_2
inst✝² : NormedAddCommGroup V
inst✝¹ : NormedSpace ℝ V
inst✝ : FiniteDimensional ℝ V
s : Set V
hscv : Convex ℝ s
this : Nonempty ↑s
p : V
hp : p ∈ s
p' : ↥(_root_.affineSpan ℝ s) := ⟨p, ⋯⟩
⊢ ⊤ = ⊤

pp: V : Type u_2
inst✝² : NormedAddCommGroup V
inst✝¹ : NormedSpace ℝ V
inst✝ : FiniteDimensional ℝ V
s : Set V
hscv : Convex ℝ s
this : Nonempty ↑s
p : V
hp : p ∈ s
p' : ↥(_root_.affineSpan ℝ s) := ⟨p, ⋯⟩
⊢ Convex ℝ (⇑(AffineIsometryEquiv.constVSub ℝ p').symm.toHomeomorph ⁻¹' Subtype.val ⁻¹' s)

Tactic:
]

Goal state after:
V : Type u_2
inst✝² : NormedAddCommGroup V
inst✝¹ : NormedSpace ℝ V
inst✝ : FiniteDimensional ℝ V
s : Set V
hscv : Convex ℝ s
this : Nonempty ↑s
p : V
hp : p ∈ s
p' : ↥(_root_.affineSpan ℝ s) := ⟨p, ⋯⟩
⊢ Convex ℝ (⇑(AffineIsometryEquiv.constVSub ℝ p').symm.toHomeomorph ⁻¹' Subtype.val ⁻¹' s)
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
s : Set X
hs : ∃ x ∈ s, w.weights x ≠ 0
inst✝ : DecidablePred fun x ↦ x ∈ s
this : ((filter (fun x ↦ x ∈ s) w.weights).sum fun x k ↦ k) ≠ 0
⊢ (filter (fun x ↦ x ∈ s) w.weights).support = {x ∈ w.weights.support | x ∈ s}

Tactic:
]

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
s : Set X
hs : ∃ x ∈ s, w.weights x ≠ 0
inst✝ : DecidablePred fun x ↦ x ∈ s
this : ((filter (fun x ↦ x ∈ s) w.weights).sum fun x k ↦ k) ≠ 0
⊢ (filter (fun x ↦ x ∈ s) w.weights).support = {x ∈ w.weights.support | x ∈ s}
Module: Mathlib.Geometry.Convex.ConvexSpace.AffineSpace

Goal state before:
pp: case e_a
R : Type u_1
V : Type u_2
P : Type u_3
inst✝⁵ : Ring R
inst✝⁴ : PartialOrder R
inst✝³ : IsStrictOrderedRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AffineSpace V P
f : StdSimplex R (StdSimplex R P)
b : P
hL :
  (Finset.affineCombination R (StdSimplex.map convexCombination f).weights.support id)
      ⇑(StdSimplex.map convexCombination f).weights =
    ((StdSimplex.map convexCombination f).weights.support.weightedVSubOfPoint id b)
        ⇑(StdSimplex.map convexCombination f).weights +ᵥ
      b
hR :
  (Finset.affineCombination R f.join.weights.support id) ⇑f.join.weights =
    (f.join.weights.support.weightedVSubOfPoint id b) ⇑f.join.weights +ᵥ b
⊢ (f.weights.sum fun a m ↦ m • (convexCombination a -ᵥ b)) =
    ∑ x ∈ (f.weights.sum fun d r ↦ r • d.weights).support, (f.weights.sum fun d r ↦ r • d.weights) x • (x -ᵥ b)

Tactic:
]

Goal state after:
case e_a
R : Type u_1
V : Type u_2
P : Type u_3
inst✝⁵ : Ring R
inst✝⁴ : PartialOrder R
inst✝³ : IsStrictOrderedRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AffineSpace V P
f : StdSimplex R (StdSimplex R P)
b : P
hL :
  (Finset.affineCombination R (StdSimplex.map convexCombination f).weights.support id)
      ⇑(StdSimplex.map convexCombination f).weights =
    ((StdSimplex.map convexCombination f).weights.support.weightedVSubOfPoint id b)
        ⇑(StdSimplex.map convexCombination f).weights +ᵥ
      b
hR :
  (Finset.affineCombination R f.join.weights.support id) ⇑f.join.weights =
    (f.join.weights.support.weightedVSubOfPoint id b) ⇑f.join.weights +ᵥ b
⊢ (f.weights.sum fun a m ↦ m • (convexCombination a -ᵥ b)) =
    ∑ x ∈ (f.weights.sum fun d r ↦ r • d.weights).support, (f.weights.sum fun d r ↦ r • d.weights) x • (x -ᵥ b)