mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Convex.Between

Goal state before:
pp: R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁵ : Field R
inst✝⁴ : LinearOrder R
inst✝³ : IsStrictOrderedRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x y z : P
v : V
h : ∀ p ∈ {x, y, z}, ∃ r, p = r • v +ᵥ x
⊢ Wbtw R x y z ∨ Wbtw R y z x ∨ Wbtw R z x y

Tactic:
[

Goal state after:
R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁵ : Field R
inst✝⁴ : LinearOrder R
inst✝³ : IsStrictOrderedRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x y z : P
v : V
h : ∀ p ∈ {x, y, z}, ∃ r, p = r • v +ᵥ x
⊢ Wbtw R x y z ∨ Wbtw R y z x ∨ Wbtw R z x y
Module: Mathlib.Analysis.Convex.Cone.Dual

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁹ : CommRing R
inst✝⁸ : PartialOrder R
inst✝⁷ : TopologicalSpace R
inst✝⁶ : ClosedIciTopology R
inst✝⁵ : IsOrderedRing R
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : TopologicalSpace N
p : M →ₗ[R] N →ₗ[R] R
s : Set M
hp : ∀ (x : M), Continuous ⇑(p x)
⊢ IsClosed ↑(dual p (⋃ x ∈ s, {x}))

Tactic:
[

Goal state after:
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁹ : CommRing R
inst✝⁸ : PartialOrder R
inst✝⁷ : TopologicalSpace R
inst✝⁶ : ClosedIciTopology R
inst✝⁵ : IsOrderedRing R
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : TopologicalSpace N
p : M →ₗ[R] N →ₗ[R] R
s : Set M
hp : ∀ (x : M), Continuous ⇑(p x)
⊢ IsClosed ↑(dual p (⋃ x ∈ s, {x}))
Module: Mathlib.Analysis.Convex.Exposed

Goal state before:
pp: case mpr
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : TopologicalSpace 𝕜
inst✝⁴ : Ring 𝕜
inst✝³ : PartialOrder 𝕜
inst✝² : AddCommMonoid E
inst✝¹ : TopologicalSpace E
inst✝ : Module 𝕜 E
A : Set E
x : E
h : IsExposed 𝕜 A {x}
l : StrongDual 𝕜 E
hl : x ∈ {x | x ∈ A ∧ ∀ y ∈ A, l y ≤ l x} ∧ ∀ x_1 ∈ {x | x ∈ A ∧ ∀ y ∈ A, l y ≤ l x}, x_1 = x
⊢ x ∈ exposedPoints 𝕜 A

Tactic:
exact
    ⟨hl.1.1, l, fun y hy =>
      ⟨hl.1.2 y hy, fun hxy => hl.2 y ⟨hy, fun z hz => (hl.1.2 z hz).trans hxy⟩⟩⟩

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

Goal state before:
pp: case refine_2
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : ι → E
h : ∀ (s : Finset ι) (x : ι), p x ∈ (convexHull 𝕜) ↑(image p s) → x ∈ s
s : Set ι
x : ι
hx : p x ∈ ⋃ t, ⋃ (_ : ↑t ⊆ p '' s), (convexHull 𝕜) ↑t
hp : Injective p
⊢ x ∈ s

Tactic:
[

Goal state after:
case refine_2
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : ι → E
h : ∀ (s : Finset ι) (x : ι), p x ∈ (convexHull 𝕜) ↑(image p s) → x ∈ s
s : Set ι
x : ι
hx : p x ∈ ⋃ t, ⋃ (_ : ↑t ⊆ p '' s), (convexHull 𝕜) ↑t
hp : Injective p
⊢ x ∈ s
Module: Mathlib.Analysis.Convex.GaugeRescale

Goal state before:
pp: E : Type u_1
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module ℝ E
inst✝³ : TopologicalSpace E
inst✝² : IsTopologicalAddGroup E
inst✝¹ : ContinuousSMul ℝ E
inst✝ : T1Space E
s t : Set E
hsc : Convex ℝ s
hsne : (interior s).Nonempty
hsb : IsVonNBounded ℝ s
hst : Convex ℝ t
htne : (interior t).Nonempty
htb : IsVonNBounded ℝ t
e : E ≃ₜ E
h₁ : ⇑e '' interior s = interior t
h₂ : ⇑e '' closure[inst✝³] s = closure[inst✝³] t
⊢ ⇑e '' frontier s = frontier t

Tactic:
[

Goal state after:
E : Type u_1
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module ℝ E
inst✝³ : TopologicalSpace E
inst✝² : IsTopologicalAddGroup E
inst✝¹ : ContinuousSMul ℝ E
inst✝ : T1Space E
s t : Set E
hsc : Convex ℝ s
hsne : (interior s).Nonempty
hsb : IsVonNBounded ℝ s
hst : Convex ℝ t
htne : (interior t).Nonempty
htb : IsVonNBounded ℝ t
e : E ≃ₜ E
h₁ : ⇑e '' interior s = interior t
h₂ : ⇑e '' closure[inst✝³] s = closure[inst✝³] t
⊢ ⇑e '' frontier s = frontier t
Module: Mathlib.Analysis.Convex.Continuous

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E → ℝ
x₀ : E
ε r M : ℝ
hf : ConvexOn ℝ (ball x₀ r) f
hε : 0 < ε
hM : ∀ (a : E), dist a x₀ < r → |f a| ≤ M
K : ℝ := 2 * M / ε
hK : K = 2 * M / ε
oneside : ∀ {x y : E}, x ∈ ball x₀ (r - ε) → y ∈ ball x₀ (r - ε) → f x - f y ≤ K * ‖x - y‖
x : E
hx : x ∈ ball x₀ (r - ε)
y : E
hy : y ∈ ball x₀ (r - ε)
⊢ dist (f x) (f y) ≤ K * dist x y

Tactic:
[

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E → ℝ
x₀ : E
ε r M : ℝ
hf : ConvexOn ℝ (ball x₀ r) f
hε : 0 < ε
hM : ∀ (a : E), dist a x₀ < r → |f a| ≤ M
K : ℝ := 2 * M / ε
hK : K = 2 * M / ε
oneside : ∀ {x y : E}, x ∈ ball x₀ (r - ε) → y ∈ ball x₀ (r - ε) → f x - f y ≤ K * ‖x - y‖
x : E
hx : x ∈ ball x₀ (r - ε)
y : E
hy : y ∈ ball x₀ (r - ε)
⊢ dist (f x) (f y) ≤ K * dist x y
Module: Mathlib.Analysis.Convex.GaugeRescale

Goal state before:
pp: E : Type u_1
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module ℝ E
inst✝³ : TopologicalSpace E
inst✝² : IsTopologicalAddGroup E
inst✝¹ : ContinuousSMul ℝ E
inst✝ : T1Space E
s t : Set E
hsc : Convex ℝ s
hsb : IsVonNBounded ℝ s
hst : Convex ℝ t
htb : IsVonNBounded ℝ t
x : E
hx : x ∈ interior s
y : E
hy : y ∈ interior t
h : E ≃ₜ E := gaugeRescaleHomeomorph (-x +ᵥ s) (-y +ᵥ t) ⋯ ⋯ ⋯ ⋯ ⋯ ⋯
⊢ (fun a ↦ y + h (-x + a)) '' interior s = y +ᵥ ⇑h '' interior (-x +ᵥ s)

Tactic:
[

Goal state after:
E : Type u_1
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module ℝ E
inst✝³ : TopologicalSpace E
inst✝² : IsTopologicalAddGroup E
inst✝¹ : ContinuousSMul ℝ E
inst✝ : T1Space E
s t : Set E
hsc : Convex ℝ s
hsb : IsVonNBounded ℝ s
hst : Convex ℝ t
htb : IsVonNBounded ℝ t
x : E
hx : x ∈ interior s
y : E
hy : y ∈ interior t
h : E ≃ₜ E := gaugeRescaleHomeomorph (-x +ᵥ s) (-y +ᵥ t) ⋯ ⋯ ⋯ ⋯ ⋯ ⋯
⊢ (fun a ↦ y + h (-x + a)) '' interior s = y +ᵥ ⇑h '' interior (-x +ᵥ s)
Module: Mathlib.Analysis.Convex.GaugeRescale

Goal state before:
pp: E : Type u_1
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module ℝ E
inst✝³ : TopologicalSpace E
inst✝² : IsTopologicalAddGroup E
inst✝¹ : ContinuousSMul ℝ E
inst✝ : T1Space E
s t : Set E
hsc : Convex ℝ s
hsb : IsVonNBounded ℝ s
hst : Convex ℝ t
htb : IsVonNBounded ℝ t
x : E
hx : x ∈ interior s
y : E
hy : y ∈ interior t
h : E ≃ₜ E := gaugeRescaleHomeomorph (-x +ᵥ s) (-y +ᵥ t) ⋯ ⋯ ⋯ ⋯ ⋯ ⋯
⊢ (fun a ↦ y + h (-x + a)) '' closure[inst✝³] s = y +ᵥ ⇑h '' closure[inst✝³] (-x +ᵥ s)

Tactic:
[

Goal state after:
E : Type u_1
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module ℝ E
inst✝³ : TopologicalSpace E
inst✝² : IsTopologicalAddGroup E
inst✝¹ : ContinuousSMul ℝ E
inst✝ : T1Space E
s t : Set E
hsc : Convex ℝ s
hsb : IsVonNBounded ℝ s
hst : Convex ℝ t
htb : IsVonNBounded ℝ t
x : E
hx : x ∈ interior s
y : E
hy : y ∈ interior t
h : E ≃ₜ E := gaugeRescaleHomeomorph (-x +ᵥ s) (-y +ᵥ t) ⋯ ⋯ ⋯ ⋯ ⋯ ⋯
⊢ (fun a ↦ y + h (-x + a)) '' closure[inst✝³] s = y +ᵥ ⇑h '' closure[inst✝³] (-x +ᵥ s)
Module: Mathlib.Analysis.Convex.Join

Goal state before:
pp: 𝕜 : Type u_2
E : Type u_3
inst✝³ : Semiring 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
s t : Set E
⊢ ⋃ i' ∈ t, ⋃ i ∈ s, segment 𝕜 i i' = convexJoin 𝕜 t s

Tactic:
[

Goal state after:
𝕜 : Type u_2
E : Type u_3
inst✝³ : Semiring 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
s t : Set E
⊢ ⋃ i' ∈ t, ⋃ i ∈ s, segment 𝕜 i i' = convexJoin 𝕜 t s
Module: Mathlib.Analysis.Convex.Join

Goal state before:
pp: 𝕜 : Type u_2
E : Type u_3
inst✝³ : Semiring 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
s₁ s₂ t : Set E
⊢ convexJoin 𝕜 (s₁ ∪ s₂) t = convexJoin 𝕜 s₁ t ∪ convexJoin 𝕜 s₂ t

Tactic:
[

Goal state after:
𝕜 : Type u_2
E : Type u_3
inst✝³ : Semiring 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
s₁ s₂ t : Set E
⊢ convexJoin 𝕜 (s₁ ∪ s₂) t = convexJoin 𝕜 s₁ t ∪ convexJoin 𝕜 s₂ t
Module: Mathlib.Analysis.Convex.Join

Goal state before:
pp: 𝕜 : Type u_2
E : Type u_3
inst✝³ : Semiring 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
s t₁ t₂ : Set E
⊢ convexJoin 𝕜 s (t₁ ∪ t₂) = convexJoin 𝕜 s t₁ ∪ convexJoin 𝕜 s t₂

Tactic:
[

Goal state after:
𝕜 : Type u_2
E : Type u_3
inst✝³ : Semiring 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
s t₁ t₂ : Set E
⊢ convexJoin 𝕜 s (t₁ ∪ t₂) = convexJoin 𝕜 s t₁ ∪ convexJoin 𝕜 s t₂
Module: Mathlib.Analysis.Convex.Join

Goal state before:
pp: ι : Sort u_1
𝕜 : Type u_2
E : Type u_3
inst✝³ : Semiring 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
s : ι → Set E
t : Set E
⊢ convexJoin 𝕜 (⋃ i, s i) t = ⋃ i, convexJoin 𝕜 (s i) t

Tactic:
[

Goal state after:
ι : Sort u_1
𝕜 : Type u_2
E : Type u_3
inst✝³ : Semiring 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
s : ι → Set E
t : Set E
⊢ convexJoin 𝕜 (⋃ i, s i) t = ⋃ i, convexJoin 𝕜 (s i) t
Module: Mathlib.Analysis.Convex.Join

Goal state before:
pp: ι : Sort u_1
𝕜 : Type u_2
E : Type u_3
inst✝³ : Semiring 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
s : Set E
t : ι → Set E
⊢ convexJoin 𝕜 s (⋃ i, t i) = ⋃ i, convexJoin 𝕜 s (t i)

Tactic:
[

Goal state after:
ι : Sort u_1
𝕜 : Type u_2
E : Type u_3
inst✝³ : Semiring 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
s : Set E
t : ι → Set E
⊢ convexJoin 𝕜 s (⋃ i, t i) = ⋃ i, convexJoin 𝕜 s (t i)
Module: Mathlib.Analysis.Convex.Join

Goal state before:
pp: 𝕜 : Type u_2
E : Type u_3
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t u : Set E
⊢ convexJoin 𝕜 (convexJoin 𝕜 s t) u ⊆ convexJoin 𝕜 s (convexJoin 𝕜 t u)

Tactic:
[

Goal state after:
𝕜 : Type u_2
E : Type u_3
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t u : Set E
⊢ convexJoin 𝕜 (convexJoin 𝕜 s t) u ⊆ convexJoin 𝕜 s (convexJoin 𝕜 t u)
Module: Mathlib.Analysis.Convex.Join

Goal state before:
pp: 𝕜 : Type u_2
E : Type u_3
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t u : Set E
⊢ convexJoin 𝕜 s (convexJoin 𝕜 t u) ⊆ convexJoin 𝕜 (convexJoin 𝕜 s t) u

Tactic:
[

Goal state after:
𝕜 : Type u_2
E : Type u_3
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t u : Set E
⊢ convexJoin 𝕜 s (convexJoin 𝕜 t u) ⊆ convexJoin 𝕜 (convexJoin 𝕜 s t) u
Module: Mathlib.Analysis.Convex.Join

Goal state before:
pp: 𝕜 : Type u_2
E : Type u_3
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t u : Set E
⊢ convexJoin 𝕜 s (convexJoin 𝕜 t u) = convexJoin 𝕜 t (convexJoin 𝕜 s u)

Tactic:
[

Goal state after:
𝕜 : Type u_2
E : Type u_3
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t u : Set E
⊢ convexJoin 𝕜 s (convexJoin 𝕜 t u) = convexJoin 𝕜 t (convexJoin 𝕜 s u)
Module: Mathlib.Analysis.Convex.Join

Goal state before:
pp: 𝕜 : Type u_2
E : Type u_3
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t u : Set E
⊢ convexJoin 𝕜 (convexJoin 𝕜 s t) u = convexJoin 𝕜 (convexJoin 𝕜 s u) t

Tactic:
[

Goal state after:
𝕜 : Type u_2
E : Type u_3
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t u : Set E
⊢ convexJoin 𝕜 (convexJoin 𝕜 s t) u = convexJoin 𝕜 (convexJoin 𝕜 s u) t
Module: Mathlib.Analysis.Convex.Join

Goal state before:
pp: 𝕜 : Type u_2
E : Type u_3
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t u v : Set E
⊢ convexJoin 𝕜 (convexJoin 𝕜 s t) (convexJoin 𝕜 u v) = convexJoin 𝕜 (convexJoin 𝕜 s u) (convexJoin 𝕜 t v)

Tactic:
[

Goal state after:
𝕜 : Type u_2
E : Type u_3
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t u v : Set E
⊢ convexJoin 𝕜 (convexJoin 𝕜 s t) (convexJoin 𝕜 u v) = convexJoin 𝕜 (convexJoin 𝕜 s u) (convexJoin 𝕜 t v)
Module: Mathlib.Analysis.Convex.Integral

Goal state before:
pp: case refine_2
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
μ : Measure α
s : Set E
f : α → E
inst✝ : IsProbabilityMeasure μ
hs : Convex ℝ s
hsc : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hf : ∀ᵐ (x : α) ∂μ, f x ∈ s
this✝² : MeasurableSpace E := borel E
this✝¹ : BorelSpace E
g : α → E
hfi : Integrable g μ
hgm : StronglyMeasurable g
hfg : f =ᵐ[μ] g
this✝ : SeparableSpace ↑(range g ∩ s)
y₀ : E
h₀ : y₀ ∈ range g ∩ s
hg : ∀ᵐ (x : α) ∂μ, g x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (range g ∩ s)
G : ℕ → SimpleFunc α E := SimpleFunc.approxOn g ⋯ (range g ∩ s) y₀ h₀
this : Tendsto (fun n ↦ SimpleFunc.integral μ (G n)) atTop (𝓝 (∫ (x : α), g x ∂μ))
n : ℕ
⊢ ∑ i ∈ (G n).range, μ.real (⇑(G n) ⁻¹' {i}) = 1

Tactic:
[

Goal state after:
case refine_2
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
μ : Measure α
s : Set E
f : α → E
inst✝ : IsProbabilityMeasure μ
hs : Convex ℝ s
hsc : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hf : ∀ᵐ (x : α) ∂μ, f x ∈ s
this✝² : MeasurableSpace E := borel E
this✝¹ : BorelSpace E
g : α → E
hfi : Integrable g μ
hgm : StronglyMeasurable g
hfg : f =ᵐ[μ] g
this✝ : SeparableSpace ↑(range g ∩ s)
y₀ : E
h₀ : y₀ ∈ range g ∩ s
hg : ∀ᵐ (x : α) ∂μ, g x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (range g ∩ s)
G : ℕ → SimpleFunc α E := SimpleFunc.approxOn g ⋯ (range g ∩ s) y₀ h₀
this : Tendsto (fun n ↦ SimpleFunc.integral μ (G n)) atTop (𝓝 (∫ (x : α), g x ∂μ))
n : ℕ
⊢ ∑ i ∈ (G n).range, μ.real (⇑(G n) ⁻¹' {i}) = 1
Module: Mathlib.Analysis.Convex.Intrinsic

Goal state before:
pp: 𝕜 : Type u_1
V : Type u_2
P : Type u_5
inst✝⁴ : Ring 𝕜
inst✝³ : AddCommGroup V
inst✝² : Module 𝕜 V
inst✝¹ : TopologicalSpace P
inst✝ : AddTorsor V P
s : Set P
⊢ (intrinsicClosure 𝕜 s).Nonempty → s.Nonempty

Tactic:
[

Goal state after:
𝕜 : Type u_1
V : Type u_2
P : Type u_5
inst✝⁴ : Ring 𝕜
inst✝³ : AddCommGroup V
inst✝² : Module 𝕜 V
inst✝¹ : TopologicalSpace P
inst✝ : AddTorsor V P
s : Set P
⊢ (intrinsicClosure 𝕜 s).Nonempty → s.Nonempty
Module: Mathlib.Analysis.Convex.Join

Goal state before:
pp: 𝕜 : Type u_2
E : Type u_3
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
a b c d : E
⊢ convexJoin 𝕜 (segment 𝕜 a b) (segment 𝕜 c d) = (convexHull 𝕜) {a, b, c, d}

Tactic:
[

Goal state after:
𝕜 : Type u_2
E : Type u_3
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
a b c d : E
⊢ convexJoin 𝕜 (segment 𝕜 a b) (segment 𝕜 c d) = (convexHull 𝕜) {a, b, c, d}
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
inst✝ : IsProbabilityMeasure μ
hs : Convex ℝ s
hsc : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hf : ∀ᵐ (x : α) ∂μ, f x ∈ s
hfi : Integrable f μ
⊢ ∫ (x : α), f x ∂μ ∈ s

Tactic:
by
  borelize E
  rcases hfi.aestronglyMeasurable with ⟨g, hgm, hfg⟩
  have : SeparableSpace (range g ∩ s : Set E) :=
    (hgm.isSeparable_range.mono inter_subset_left).separableSpace
  obtain ⟨y₀, h₀⟩ : (range g ∩ s).Nonempty := by
    rcases (hf.and hfg).exists with ⟨x₀, h₀⟩
    exact ⟨f x₀, by simp only [h₀.2, mem_range_self], h₀.1⟩
  rw [integral_congr_ae hfg]; rw [integrable_congr hfg] at hfi
  have hg : ∀ᵐ x ∂μ, g x ∈ closure (range g ∩ s) := by
    filter_upwards [hfg.rw (fun _ y => y ∈ s) hf] with x hx
    apply subset_closure
    exact ⟨mem_range_self _, hx⟩
  set G : ℕ → SimpleFunc α E := SimpleFunc.approxOn _ hgm.measurable (range g ∩ s) y₀ h₀
  have : Tendsto (fun n => (G n).integral μ) atTop (𝓝 <| ∫ x, g x ∂μ) :=
    tendsto_integral_approxOn_of_measurable hfi _ hg _ (integrable_const _)
  refine hsc.mem_of_tendsto this (Eventually.of_forall fun n => hs.sum_mem ?_ ?_ ?_)
  · exact fun _ _ => ENNReal.toReal_nonneg
  · simp_rw [measureReal_def]
    rw [← ENNReal.toReal_sum, (G n).sum_range_measure_preimage_singleton, measure_univ,
      ENNReal.toReal_one]
    finiteness
  · simp only [SimpleFunc.mem_range, forall_mem_range]
    intro x
    apply (range g).inter_subset_right
    exact SimpleFunc.approxOn_mem hgm.measurable h₀ _ _

Goal state after:
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
s : Set P
t : Set Q
e : ↥(affineSpan 𝕜 (s ×ˢ t)) ≃ₜ ↥(affineSpan 𝕜 s) × ↥(affineSpan 𝕜 t) :=
  (Homeomorph.setCongr ⋯).trans (Homeomorph.Set.prod ↑(affineSpan 𝕜 s) ↑(affineSpan 𝕜 t))
this : Subtype.val ∘ ⇑e.symm = fun p ↦ (↑p.1, ↑p.2)
⊢ intrinsicInterior 𝕜 (s ×ˢ t) = intrinsicInterior 𝕜 s ×ˢ intrinsicInterior 𝕜 t

Tactic:
have h : ((↑) ⁻¹' (s ×ˢ t) : Set _) = e ⁻¹' (((↑) ⁻¹' s) ×ˢ ((↑) ⁻¹' t)) := rfl

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
s : Set P
t : Set Q
e : ↥(affineSpan 𝕜 (s ×ˢ t)) ≃ₜ ↥(affineSpan 𝕜 s) × ↥(affineSpan 𝕜 t) :=
  (Homeomorph.setCongr ⋯).trans (Homeomorph.Set.prod ↑(affineSpan 𝕜 s) ↑(affineSpan 𝕜 t))
this : Subtype.val ∘ ⇑e.symm = fun p ↦ (↑p.1, ↑p.2)
h : Subtype.val ⁻¹' s ×ˢ t = ⇑e ⁻¹' (Subtype.val ⁻¹' s) ×ˢ (Subtype.val ⁻¹' t)
⊢ intrinsicInterior 𝕜 (s ×ˢ t) = intrinsicInterior 𝕜 s ×ˢ intrinsicInterior 𝕜 t
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
s : Set P
t : Set Q
e : ↥(affineSpan 𝕜 (s ×ˢ t)) ≃ₜ ↥(affineSpan 𝕜 s) × ↥(affineSpan 𝕜 t) :=
  (Homeomorph.setCongr ⋯).trans (Homeomorph.Set.prod ↑(affineSpan 𝕜 s) ↑(affineSpan 𝕜 t))
this : Subtype.val ∘ ⇑e.symm = fun p ↦ (↑p.1, ↑p.2)
h : Subtype.val ⁻¹' s ×ˢ t = ⇑e ⁻¹' (Subtype.val ⁻¹' s) ×ˢ (Subtype.val ⁻¹' t)
⊢ intrinsicInterior 𝕜 (s ×ˢ t) = intrinsicInterior 𝕜 s ×ˢ intrinsicInterior 𝕜 t

Tactic:
[

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
s : Set P
t : Set Q
e : ↥(affineSpan 𝕜 (s ×ˢ t)) ≃ₜ ↥(affineSpan 𝕜 s) × ↥(affineSpan 𝕜 t) :=
  (Homeomorph.setCongr ⋯).trans (Homeomorph.Set.prod ↑(affineSpan 𝕜 s) ↑(affineSpan 𝕜 t))
this : Subtype.val ∘ ⇑e.symm = fun p ↦ (↑p.1, ↑p.2)
h : Subtype.val ⁻¹' s ×ˢ t = ⇑e ⁻¹' (Subtype.val ⁻¹' s) ×ˢ (Subtype.val ⁻¹' t)
⊢ intrinsicInterior 𝕜 (s ×ˢ t) = intrinsicInterior 𝕜 s ×ˢ intrinsicInterior 𝕜 t
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
s : Set P
t : Set Q
e : ↥(affineSpan 𝕜 (s ×ˢ t)) ≃ₜ ↥(affineSpan 𝕜 s) × ↥(affineSpan 𝕜 t) :=
  (Homeomorph.setCongr ⋯).trans (Homeomorph.Set.prod ↑(affineSpan 𝕜 s) ↑(affineSpan 𝕜 t))
this : Subtype.val ∘ ⇑e.symm = fun p ↦ (↑p.1, ↑p.2)
h : Subtype.val ⁻¹' s ×ˢ t = ⇑e ⁻¹' (Subtype.val ⁻¹' s) ×ˢ (Subtype.val ⁻¹' t)
⊢ Subtype.val ∘ ⇑e.symm '' interior (Subtype.val ⁻¹' s) ×ˢ interior (Subtype.val ⁻¹' t) =
    (fun p ↦ (↑p.1, ↑p.2)) '' interior (Subtype.val ⁻¹' s) ×ˢ interior (Subtype.val ⁻¹' t)

Tactic:
this

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

Goal state before:
pp: case inl
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
hspan : affineSpan ℝ s ≠ ⊤
⊢ μ (frontier s) = 0

Tactic:
refine measure_mono_null ?_ (addHaar_affineSubspace _ _ hspan)

Goal state after:
case inl
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
hspan : affineSpan ℝ s ≠ ⊤
⊢ frontier s ⊆ ↑(affineSpan ℝ s)
Module: Mathlib.Analysis.Convex.Measure

Goal state before:
pp: case inr
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
⊢ μ (frontier s) = 0

Tactic:
suffices H : ∀ t : Set E, Convex ℝ t → x ∈ interior t → IsBounded t → μ (frontier t) = 0 by
    let B : ℕ → Set E := fun n => ball x (n + 1)
    have : μ (⋃ n : ℕ, frontier (s ∩ B n)) = 0 := by
      refine measure_iUnion_null fun n =>
        H _ (hs.inter (convex_ball _ _)) ?_ (isBounded_ball.subset inter_subset_right)
      rw [interior_inter, isOpen_ball.interior_eq]
      exact ⟨hx, mem_ball_self (add_pos_of_nonneg_of_pos n.cast_nonneg zero_lt_one)⟩
    refine measure_mono_null (fun y hy => ?_) this; clear this
    set N : ℕ := ⌊dist y x⌋₊
    refine mem_iUnion.2 ⟨N, ?_⟩
    have hN : y ∈ B N := by simp [B, N, Nat.lt_floor_add_one]
    suffices y ∈ frontier (s ∩ B N) ∩ B N from this.1
    rw [frontier_inter_open_inter isOpen_ball]
    exact ⟨hy, hN⟩

Goal state after:
case inr
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
⊢ ∀ (t : Set E), Convex ℝ t → x ∈ interior t → Bornology.IsBounded t → μ (frontier t) = 0
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
a : R
ha : a ≠ 0
hwa : w.weights = Finsupp.single x a
⊢ w.weights = (single x).weights

Tactic:
simp only [hwa, weights_single]

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
a : R
ha : a ≠ 0
hwa : w.weights = Finsupp.single x a
⊢ Finsupp.single x a = Finsupp.single x 1
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
hs : Convex ℝ s
⊢ (intrinsicInterior ℝ s).Nonempty → s.Nonempty

Tactic:
[

Goal state after:
V : Type u_2
inst✝² : NormedAddCommGroup V
inst✝¹ : NormedSpace ℝ V
inst✝ : FiniteDimensional ℝ V
s : Set V
hs : Convex ℝ s
⊢ (intrinsicInterior ℝ s).Nonempty → s.Nonempty
Module: Mathlib.Geometry.Convex.ConvexSpace.Prod

Goal state before:
pp: I : Type u_1
R : Type u_2
inst✝⁴ : Semiring R
inst✝³ : PartialOrder R
inst✝² : IsStrictOrderedRing R
ι : Type u_3
X : Type u_4
inst✝¹ : Zero X
inst✝ : ConvexSpace R X
i : ι
w : StdSimplex R (StdSimplex R (ι →₀ X))
⊢ onFinset
      ((StdSimplex.map (fun w ↦ onFinset (w.weights.support.biUnion support) (fun i ↦ iConvexComb w fun x ↦ x i) ⋯)
                w).weights.support.biUnion
        support)
      (fun i ↦
        iConvexComb
          (StdSimplex.map (fun w ↦ onFinset (w.weights.support.biUnion support) (fun i ↦ iConvexComb w fun x ↦ x i) ⋯)
            w)
          fun x ↦ x i)
      ⋯ =
    onFinset ((sConvexComb w).weights.support.biUnion support) (fun i ↦ iConvexComb (sConvexComb w) fun x ↦ x i) ⋯

Tactic:
by ext; simp [iConvexComb_assoc]

Goal state after: