mathlib-initiative/mathlib-tactics huggingface dataset:
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.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.Continuous

Goal state before:
pp: case h
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 : ConvexOn ℝ C f
x₀ : E
hx₀ : x₀ ∈ C
b : AffineBasis (Fin (Module.finrank ℝ E + 1)) ℝ E
hx₀b : x₀ ∈ interior ((convexHull ℝ) (Set.range ⇑b))
hbC : (convexHull ℝ) (Set.range ⇑b) ⊆ C
⊢ interior ((convexHull ℝ) (Set.range ⇑b)) ⊆ (convexHull ℝ) (Set.range ⇑b)

Tactic:
;

Goal state after:
case h
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 : ConvexOn ℝ C f
x₀ : E
hx₀ : x₀ ∈ C
b : AffineBasis (Fin (Module.finrank ℝ E + 1)) ℝ E
hx₀b : x₀ ∈ interior ((convexHull ℝ) (Set.range ⇑b))
hbC : (convexHull ℝ) (Set.range ⇑b) ⊆ C
⊢ interior ((convexHull ℝ) (Set.range ⇑b)) ⊆ (convexHull ℝ) (Set.range ⇑b)
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.Intrinsic

Goal state before:
pp: case refine_2
𝕜 : Type u_1
V : Type u_2
P : Type u_5
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : CompleteSpace 𝕜
inst✝⁴ : NormedAddCommGroup V
inst✝³ : NormedSpace 𝕜 V
inst✝² : FiniteDimensional 𝕜 V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s : Set P
x : P
h : ∀ (o : Set P), IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] o → x ∈ o → (o ∩ s).Nonempty
t : Set P
ht : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t
hx : ⟨x, ?refine_3⟩ ∈ Subtype.val ⁻¹' t
⊢ (Subtype.val ⁻¹' t ∩ Subtype.val ⁻¹' s).Nonempty

Tactic:
obtain ⟨y, hyt, hys⟩ := h _ ht hx

Goal state after:
case refine_2
𝕜 : Type u_1
V : Type u_2
P : Type u_5
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : CompleteSpace 𝕜
inst✝⁴ : NormedAddCommGroup V
inst✝³ : NormedSpace 𝕜 V
inst✝² : FiniteDimensional 𝕜 V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s : Set P
x : P
h : ∀ (o : Set P), IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] o → x ∈ o → (o ∩ s).Nonempty
t : Set P
ht : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t
hx : ⟨x, ?refine_3⟩ ∈ Subtype.val ⁻¹' t
y : P
hyt : y ∈ t
hys : y ∈ s
⊢ (Subtype.val ⁻¹' t ∩ Subtype.val ⁻¹' s).Nonempty
Module: Mathlib.Geometry.Convex.ConvexSpace.Defs

Goal state before:
pp: R : Type u
inst✝² : PartialOrder R
inst✝¹ : Semiring R
M : Type u_9
inst✝ : Nontrivial R
total : (sum 0 fun x r ↦ r) = 1
⊢ False

Tactic:
;

Goal state after:
R : Type u
inst✝² : PartialOrder R
inst✝¹ : Semiring R
M : Type u_9
inst✝ : Nontrivial R
total : (sum 0 fun x r ↦ r) = 1
⊢ False
Module: Mathlib.Geometry.Convex.ConvexSpace.Defs

Goal state before:
pp: case mk
R : Type u
inst✝¹ : PartialOrder R
inst✝ : Semiring R
M : Type u_9
g : StdSimplex R M
weights✝ : M →₀ R
nonneg✝ : 0 ≤ weights✝
total✝ : (weights✝.sum fun x r ↦ r) = 1
⊢ { weights := weights✝, nonneg := nonneg✝, total := total✝ }.weights = g.weights ↔
    { weights := weights✝, nonneg := nonneg✝, total := total✝ } = g

Tactic:
;

Goal state after:
case mk
R : Type u
inst✝¹ : PartialOrder R
inst✝ : Semiring R
M : Type u_9
g : StdSimplex R M
weights✝ : M →₀ R
nonneg✝ : 0 ≤ weights✝
total✝ : (weights✝.sum fun x r ↦ r) = 1
⊢ { weights := weights✝, nonneg := nonneg✝, total := total✝ }.weights = g.weights ↔
    { weights := weights✝, nonneg := nonneg✝, total := total✝ } = g
Module: Mathlib.Geometry.Convex.ConvexSpace.Defs

Goal state before:
pp: case mk.mk
R : Type u
inst✝¹ : PartialOrder R
inst✝ : Semiring R
M : Type u_9
weights✝¹ : M →₀ R
nonneg✝¹ : 0 ≤ weights✝¹
total✝¹ : (weights✝¹.sum fun x r ↦ r) = 1
weights✝ : M →₀ R
nonneg✝ : 0 ≤ weights✝
total✝ : (weights✝.sum fun x r ↦ r) = 1
⊢ { weights := weights✝¹, nonneg := nonneg✝¹, total := total✝¹ }.weights =
      { weights := weights✝, nonneg := nonneg✝, total := total✝ }.weights ↔
    { weights := weights✝¹, nonneg := nonneg✝¹, total := total✝¹ } =
      { weights := weights✝, nonneg := nonneg✝, total := total✝ }

Tactic:
;

Goal state after:
case mk.mk
R : Type u
inst✝¹ : PartialOrder R
inst✝ : Semiring R
M : Type u_9
weights✝¹ : M →₀ R
nonneg✝¹ : 0 ≤ weights✝¹
total✝¹ : (weights✝¹.sum fun x r ↦ r) = 1
weights✝ : M →₀ R
nonneg✝ : 0 ≤ weights✝
total✝ : (weights✝.sum fun x r ↦ r) = 1
⊢ { weights := weights✝¹, nonneg := nonneg✝¹, total := total✝¹ }.weights =
      { weights := weights✝, nonneg := nonneg✝, total := total✝ }.weights ↔
    { weights := weights✝¹, nonneg := nonneg✝¹, total := total✝¹ } =
      { weights := weights✝, nonneg := nonneg✝, total := total✝ }
Module: Mathlib.Geometry.Convex.ConvexSpace.Defs

Goal state before:
pp: R : Type u
inst✝² : PartialOrder R
inst✝¹ : Semiring R
M : Type u_9
x : M
inst✝ : IsStrictOrderedRing R
⊢ (single x).weights.support = {x}

Tactic:
;

Goal state after:
R : Type u
inst✝² : PartialOrder R
inst✝¹ : Semiring R
M : Type u_9
x : M
inst✝ : IsStrictOrderedRing R
⊢ (single x).weights.support = {x}
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 a : N
⊢ (map (fun x_1 ↦ x) f).weights a = (single x).weights a

Tactic:
;

Goal state after:
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 a : N
⊢ (map (fun x_1 ↦ x) f).weights a = (single x).weights a
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
x : M
f : M → N
a✝ : N
⊢ (map f (single x)).weights a✝ = (single (f x)).weights a✝

Tactic:
;

Goal state after:
R : Type u
inst✝² : PartialOrder R
inst✝¹ : Semiring R
M : Type u_9
N : Type u_10
inst✝ : IsStrictOrderedRing R
x : M
f : M → N
a✝ : N
⊢ (map f (single x)).weights a✝ = (single (f x)).weights a✝
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
s t : R
hs : 0 ≤ s
ht : 0 ≤ t
h : s + t = 1
x y : M
f : M → N
a✝ : N
⊢ (map f (duple x y hs ht h)).weights a✝ = (duple (f x) (f y) hs ht h).weights a✝

Tactic:
;

Goal state after:
R : Type u
inst✝² : PartialOrder R
inst✝¹ : Semiring R
M : Type u_9
N : Type u_10
inst✝ : IsStrictOrderedRing R
s t : R
hs : 0 ≤ s
ht : 0 ≤ t
h : s + t = 1
x y : M
f : M → N
a✝ : N
⊢ (map f (duple x y hs ht h)).weights a✝ = (duple (f x) (f y) hs ht h).weights a✝
Module: Mathlib.Geometry.Convex.ConvexSpace.Defs

Goal state before:
pp: R : Type u
inst✝² : PartialOrder R
inst✝¹ : Semiring R
M : Type u_9
inst✝ : IsStrictOrderedRing R
f : StdSimplex R M
a✝ : M
⊢ (map id f).weights a✝ = f.weights a✝

Tactic:
;

Goal state after:
R : Type u
inst✝² : PartialOrder R
inst✝¹ : Semiring R
M : Type u_9
inst✝ : IsStrictOrderedRing R
f : StdSimplex R M
a✝ : M
⊢ (map id f).weights a✝ = f.weights a✝
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
P : Type u_11
inst✝ : IsStrictOrderedRing R
f : StdSimplex R M
g₁ : M → N
g₂ : N → P
a✝ : P
⊢ (map (g₂ ∘ g₁) f).weights a✝ = (map g₂ (map g₁ f)).weights a✝

Tactic:
;

Goal state after:
R : Type u
inst✝² : PartialOrder R
inst✝¹ : Semiring R
M : Type u_9
N : Type u_10
P : Type u_11
inst✝ : IsStrictOrderedRing R
f : StdSimplex R M
g₁ : M → N
g₂ : N → P
a✝ : P
⊢ (map (g₂ ∘ g₁) f).weights a✝ = (map g₂ (map g₁ f)).weights a✝
Module: Mathlib.Geometry.Convex.ConvexSpace.Defs

Goal state before:
pp: R : Type u
inst✝² : PartialOrder R
inst✝¹ : Semiring R
M : Type u_9
inst✝ : IsStrictOrderedRing R
f : StdSimplex R (StdSimplex R (StdSimplex R M))
⊢ f.join.join.weights = (map (fun x ↦ x.join) f).join.weights

Tactic:
;

Goal state after:
R : Type u
inst✝² : PartialOrder R
inst✝¹ : Semiring R
M : Type u_9
inst✝ : IsStrictOrderedRing R
f : StdSimplex R (StdSimplex R (StdSimplex R M))
⊢ f.join.join.weights = (map (fun x ↦ x.join) f).join.weights
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 (StdSimplex R M)
g : M → N
⊢ (map g f.join).weights = (map (fun x ↦ map g x) f).join.weights

Tactic:
;

Goal state after:
R : Type u
inst✝² : PartialOrder R
inst✝¹ : Semiring R
M : Type u_9
N : Type u_10
inst✝ : IsStrictOrderedRing R
f : StdSimplex R (StdSimplex R M)
g : M → N
⊢ (map g f.join).weights = (map (fun x ↦ map g x) f).join.weights
Module: Mathlib.Geometry.Convex.ConvexSpace.Defs

Goal state before:
pp: R : Type u
inst✝² : PartialOrder R
inst✝¹ : Semiring R
M : Type u_9
inst✝ : IsStrictOrderedRing R
x : StdSimplex R M
a✝ : M
⊢ (single x).join.weights a✝ = x.weights a✝

Tactic:
;

Goal state after:
R : Type u
inst✝² : PartialOrder R
inst✝¹ : Semiring R
M : Type u_9
inst✝ : IsStrictOrderedRing R
x : StdSimplex R M
a✝ : M
⊢ (single x).join.weights a✝ = x.weights a✝
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
w : StdSimplex K X
s : Set X
hs : ∃ x ∈ s, w.weights x ≠ 0
inst✝ : DecidablePred fun x ↦ x ∈ s
⊢ ((filter (fun x ↦ x ∈ s) w.weights).sum fun x k ↦ k)⁻¹ • filter (fun x ↦ x ∈ s) w.weights =
    ((filter (fun x ↦ x ∈ s) w.weights).sum fun x k ↦ k)⁻¹ • filter (fun x ↦ x ∈ s) w.weights

Tactic:
;

Goal state after:
X : Type u_2
K : Type u_8
inst✝³ : Semifield K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
w : StdSimplex K X
s : Set X
hs : ∃ x ∈ s, w.weights x ≠ 0
inst✝ : DecidablePred fun x ↦ x ∈ s
⊢ ((filter (fun x ↦ x ∈ s) w.weights).sum fun x k ↦ k)⁻¹ • filter (fun x ↦ x ∈ s) w.weights =
    ((filter (fun x ↦ x ∈ s) w.weights).sum fun x k ↦ k)⁻¹ • filter (fun x ↦ x ∈ s) w.weights
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 ≠ ∅ → s ≠ ∅

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 ≠ ∅ → s ≠ ∅
Module: Mathlib.Analysis.Convex.Intrinsic

Goal state before:
pp: V : Type u_2
inst✝² : NormedAddCommGroup V
inst✝¹ : NormedSpace ℝ V
inst✝ : FiniteDimensional ℝ V
hs : Convex ℝ ∅
h : intrinsicInterior ℝ ∅ ≠ ∅
⊢ False

Tactic:
;

Goal state after:
V : Type u_2
inst✝² : NormedAddCommGroup V
inst✝¹ : NormedSpace ℝ V
inst✝ : FiniteDimensional ℝ V
hs : Convex ℝ ∅
h : intrinsicInterior ℝ ∅ ≠ ∅
⊢ False
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))
a✝ : ι
⊢ (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)
        ⋯)
      a✝ =
    (onFinset ((sConvexComb w).weights.support.biUnion support) (fun i ↦ iConvexComb (sConvexComb w) fun x ↦ x i) ⋯) a✝

Tactic:
;

Goal state after:
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))
a✝ : ι
⊢ (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)
        ⋯)
      a✝ =
    (onFinset ((sConvexComb w).weights.support.biUnion support) (fun i ↦ iConvexComb (sConvexComb w) fun x ↦ x i) ⋯) a✝
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 α
f : α → E
C : ℝ
inst✝ : StrictConvexSpace ℝ E
h_le : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ C
hC0 : 0 < C
hfi : Integrable f μ
⊢ f =ᵐ[μ] const α (⨍ (x : α), f x ∂μ) ∨ ‖⨍ (x : α), f x ∂μ‖ < C

pp: case neg
α : 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 μ
⊢ f =ᵐ[μ] const α (⨍ (x : α), f x ∂μ) ∨ ‖⨍ (x : α), f x ∂μ‖ < C

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 α
f : α → E
C : ℝ
inst✝ : StrictConvexSpace ℝ E
h_le : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ C
hC0 : 0 < C
hfi : Integrable f μ
⊢ f =ᵐ[μ] const α (⨍ (x : α), f x ∂μ) ∨ ‖⨍ (x : α), f x ∂μ‖ < C

case neg
α : 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 μ
⊢ f =ᵐ[μ] const α (⨍ (x : α), f x ∂μ) ∨ ‖⨍ (x : α), f x ∂μ‖ < C
Module: Mathlib.Geometry.Convex.ConvexSpace.AffineSpace

Goal state before:
pp: case s
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.support

pp: case f
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
| fun a ↦ f.weights a • ((Finset.affineCombination R a.weights.support id) ⇑a.weights -ᵥ b)

Tactic:
;

Goal state after:
case s
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.support

case f
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
| fun a ↦ f.weights a • ((Finset.affineCombination R a.weights.support id) ⇑a.weights -ᵥ b)
Module: Mathlib.Analysis.Convex.Integral

Goal state before:
pp: case inl
α : 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
⊢ f =ᵐ[μ] const α (⨍ (x : α), f x ∂μ) ∨ ‖∫ (x : α), f x ∂μ‖ < μ.real univ * C

pp: case 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
inst✝ : IsFiniteMeasure μ
h_le : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ C
h₀ : μ ≠ 0
⊢ f =ᵐ[μ] const α (⨍ (x : α), f x ∂μ) ∨ ‖∫ (x : α), f x ∂μ‖ < μ.real univ * C

Tactic:
;

Goal state after:
case inl
α : 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
⊢ f =ᵐ[μ] const α (⨍ (x : α), f x ∂μ) ∨ ‖∫ (x : α), f x ∂μ‖ < μ.real univ * C

case 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
inst✝ : IsFiniteMeasure μ
h_le : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ C
h₀ : μ ≠ 0
⊢ f =ᵐ[μ] const α (⨍ (x : α), f x ∂μ) ∨ ‖∫ (x : α), f x ∂μ‖ < μ.real univ * 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
y : X
s : Set X
hs : s ∈ S
hy : y ∈ s
a ha : R
b : 0 ≤ a
hb : 0 ≤ ha
hab : a + ha = 1
⊢ convexCombPair a ha b hb hab x y ∈ ⋃₀ S

Tactic:
;

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 (Set X)
hS : ∀ s ∈ S, IsStarConvexSet R x s
y : X
s : Set X
hs : s ∈ S
hy : y ∈ s
a ha : R
b : 0 ≤ a
hb : 0 ≤ ha
hab : a + ha = 1
⊢ convexCombPair a ha b hb hab x y ∈ ⋃₀ S
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:
;

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

Tactic:
;

Goal state after:
R : Type u_1
X : Type u_2
Y : Type u_3
inst✝⁴ : Semiring R
inst✝³ : PartialOrder R
inst✝² : IsStrictOrderedRing R
inst✝¹ : ConvexSpace R X
inst✝ : ConvexSpace R Y
f : X → Y
x : X
s : Set X
hf : IsAffineMap R f
hs : IsStarConvexSet R x s
y : X
hy : y ∈ s
a b : R
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ convexCombPair a b ha hb hab (f x) (f y) ∈ f '' s