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

Goal state after:
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:
simp

Goal state after:
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:
simp

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) ∂μ
⊢ a * g (⨍ (x : α) in t, f x ∂μ) + b * g (⨍ (x : α) in tᶜ, f x ∂μ) ≤
    a * ⨍ (x : α) in t, g (f x) ∂μ + b * ⨍ (x : α) in tᶜ, g (f x) ∂μ

Tactic:
by
      gcongr
      exacts [(this h₀).2, (this h₀').2]

Goal state after:
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:
simp

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
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
x✝ : P
⊢ 0 • (x✝ -ᵥ b) = 0

Tactic:
simp

Goal state after:
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
X : Type u_3
Y : Type u_4
inst✝¹ : ConvexSpace R X
inst✝ : ConvexSpace R Y
⊢ ∀ (x : X × Y), (iConvexComb (StdSimplex.single x) fst, iConvexComb (StdSimplex.single x) snd) = x

Tactic:
simp

Goal state after:
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✝ : (i : ι) → ConvexSpace R (X i)
i : ι
⊢ ∀ (x : (i : ι) → X i), (fun i ↦ iConvexComb (StdSimplex.single x) fun x ↦ x i) = x

Tactic:
simp

Goal state after:
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 : ι
⊢ ∀ (x : ι →₀ X),
    onFinset ((StdSimplex.single x).weights.support.biUnion support)
        (fun i ↦ iConvexComb (StdSimplex.single x) fun x ↦ x i) ⋯ =
      x

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
X : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
I : Type u_6
J : Type u_7
K : Type u_8
inst✝⁹ : PartialOrder R
inst✝⁸ : Semiring R
inst✝⁷ : IsStrictOrderedRing R
inst✝⁶ : ConvexSpace R M
inst✝⁵ : ConvexSpace R N
inst✝⁴ : ConvexSpace R P
inst✝³ : Semifield K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
w : StdSimplex K I
s : Set I
hs : ∃ x ∈ s, w.weights x ≠ 0
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).sum fun _x k ↦ k) = 1

Tactic:
simp

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

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

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
M : Type u_3
N : Type u_4
inst✝⁴ : PartialOrder R
inst✝³ : Semiring R
inst✝² : IsStrictOrderedRing R
inst✝¹ : ConvexSpace R M
inst✝ : ConvexSpace R N
x : N
x✝ : StdSimplex R M
⊢ x = sConvexComb (map (fun x_1 ↦ x) x✝)

Tactic:
simp

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

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

Tactic:
simp

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

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

Tactic:
simp

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

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

Tactic:
simp

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

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

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
X : Type u_2
Y : Type u_3
inst✝⁴ : Semiring R
inst✝³ : PartialOrder R
inst✝² : IsStrictOrderedRing R
inst✝¹ : ConvexSpace R X
inst✝ : ConvexSpace R Y
x : X
s : Set X
t : Set Y
y : Y
hs : IsStarConvexSet R x s
ht : IsStarConvexSet R y t
w : X
z : Y
hw : (w, z).1 ∈ s
hz : (w, z).2 ∈ t
a b : R
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ (convexCombPair a b ha hb hab (x, y) (w, z)).1 ∈ s

Tactic:
by simpa using hs hw _ ..

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

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

Tactic:
simp

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

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

Tactic:
simp

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

Goal state before:
pp: case inl
R : Type u_3
X : Type u_5
inst✝³ : Semiring R
inst✝² : PartialOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : ConvexSpace R X
hS : DirectedOn (fun x1 x2 ↦ x1 ⊆ x2) ∅
hS' : ∀ s ∈ ∅, IsConvexSet R s
⊢ IsConvexSet R (⋃₀ ∅)

Tactic:
simp

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

Goal state before:
pp: R : Type u_3
X : Type u_5
Y : Type u_6
inst✝⁴ : Semiring R
inst✝³ : PartialOrder R
inst✝² : IsStrictOrderedRing R
inst✝¹ : ConvexSpace R X
inst✝ : ConvexSpace R Y
f : X → Y
s : Set X
hf : IsAffineMap R f
hs : IsConvexSet R s
w : StdSimplex R Y
hw : ↑w.weights.support ⊆ f '' s
u : Finset X
hus : ↑u ⊆ s
hfu : InjOn f ↑u
huw : Finset.image f u = w.weights.support
x : X
⊢ 0 x ≤ (onFinset u (fun x ↦ if x ∈ u then w.weights (f x) else 0) ⋯) x

Tactic:
simp

Goal state after:
R : Type u_3
X : Type u_5
Y : Type u_6
inst✝⁴ : Semiring R
inst✝³ : PartialOrder R
inst✝² : IsStrictOrderedRing R
inst✝¹ : ConvexSpace R X
inst✝ : ConvexSpace R Y
f : X → Y
s : Set X
hf : IsAffineMap R f
hs : IsConvexSet R s
w : StdSimplex R Y
hw : ↑w.weights.support ⊆ f '' s
u : Finset X
hus : ↑u ⊆ s
hfu : InjOn f ↑u
huw : Finset.image f u = w.weights.support
x : X
⊢ 0 ≤ if x ∈ u then w.weights (f x) else 0
Module: Mathlib.Geometry.Convex.Set

Goal state before:
pp: case isTrue
R : Type u_3
X : Type u_5
Y : Type u_6
inst✝⁴ : Semiring R
inst✝³ : PartialOrder R
inst✝² : IsStrictOrderedRing R
inst✝¹ : ConvexSpace R X
inst✝ : ConvexSpace R Y
f : X → Y
s : Set X
hf : IsAffineMap R f
hs : IsConvexSet R s
w : StdSimplex R Y
hw : ↑w.weights.support ⊆ f '' s
u : Finset X
hus : ↑u ⊆ s
hfu : InjOn f ↑u
huw : Finset.image f u = w.weights.support
x : X
h✝ : x ∈ u
⊢ 0 ≤ w.weights (f x)

Tactic:
simp

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

Goal state before:
pp: case isFalse
R : Type u_3
X : Type u_5
Y : Type u_6
inst✝⁴ : Semiring R
inst✝³ : PartialOrder R
inst✝² : IsStrictOrderedRing R
inst✝¹ : ConvexSpace R X
inst✝ : ConvexSpace R Y
f : X → Y
s : Set X
hf : IsAffineMap R f
hs : IsConvexSet R s
w : StdSimplex R Y
hw : ↑w.weights.support ⊆ f '' s
u : Finset X
hus : ↑u ⊆ s
hfu : InjOn f ↑u
huw : Finset.image f u = w.weights.support
x : X
h✝ : x ∉ u
⊢ 0 ≤ 0

Tactic:
simp

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

Goal state before:
pp: case e'_2.«0»
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
e₁ e₂ : I → M
i : I
a✝¹ : f.weights i ≠ 0
a✝ : (duple 0 1 hs ht h).weights ((fun i ↦ i) ⟨0, ⋯⟩) ≠ 0
⊢ ![e₁ i, e₂ i] ((fun i ↦ i) ⟨0, ⋯⟩) = ![e₁, e₂] ((fun i ↦ i) ⟨0, ⋯⟩) i

Tactic:
simp

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

Goal state before:
pp: case e'_2.«1»
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
e₁ e₂ : I → M
i : I
a✝¹ : f.weights i ≠ 0
a✝ : (duple 0 1 hs ht h).weights ((fun i ↦ i) ⟨1, ⋯⟩) ≠ 0
⊢ ![e₁ i, e₂ i] ((fun i ↦ i) ⟨1, ⋯⟩) = ![e₁, e₂] ((fun i ↦ i) ⟨1, ⋯⟩) i

Tactic:
simp

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

Goal state before:
pp: case e'_3.«0»
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
e₁ e₂ : I → M
a✝ : (duple 0 1 hs ht h).weights ((fun i ↦ i) ⟨0, ⋯⟩) ≠ 0
⊢ ![iConvexComb f e₁, iConvexComb f e₂] ((fun i ↦ i) ⟨0, ⋯⟩) = iConvexComb f (![e₁, e₂] ((fun i ↦ i) ⟨0, ⋯⟩))

Tactic:
simp

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

Goal state before:
pp: case e'_3.«1»
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
e₁ e₂ : I → M
a✝ : (duple 0 1 hs ht h).weights ((fun i ↦ i) ⟨1, ⋯⟩) ≠ 0
⊢ ![iConvexComb f e₁, iConvexComb f e₂] ((fun i ↦ i) ⟨1, ⋯⟩) = iConvexComb f (![e₁, e₂] ((fun i ↦ i) ⟨1, ⋯⟩))

Tactic:
simp

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

Goal state before:
pp: R : Type u_9
M : Type u_10
I : Type u_11
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:
by
  simpa using iConvexComb_convexCombPair_comm hs ht h f e (fun _ ↦ m)

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
s t : R
hs : 0 ≤ s
ht : 0 ≤ t
h : s + t = 1
x y : P
⊢ ∀ a ∈ (Finsupp.single x s).support ∪ (Finsupp.single y t).support, 0 = 0

Tactic:
simp

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
s t : R
hs : 0 ≤ s
ht : 0 ≤ t
h : s + t = 1
x y : P
⊢ ∀ a ∈ (Finsupp.single x s).support ∪ (Finsupp.single y t).support, ∀ (b₁ b₂ : R), b₁ + b₂ = b₁ + b₂

Tactic:
simp

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
s t : R
hs : 0 ≤ s
ht : 0 ≤ t
h : s + t = 1
x y : P
⊢ 0 = 0

Tactic:
simp

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

Goal state before:
pp: case pos
R : Type u_3
X : Type u_5
Y : Type u_6
inst✝⁴ : Semiring R
inst✝³ : PartialOrder R
inst✝² : IsStrictOrderedRing R
inst✝¹ : ConvexSpace R X
inst✝ : ConvexSpace R Y
f : X → Y
s : Set X
hf : IsAffineMap R f
hs : IsConvexSet R s
w : StdSimplex R Y
hw : ↑w.weights.support ⊆ f '' s
u : Finset X
hus : ↑u ⊆ s
hfu : InjOn f ↑u
huw : Finset.image f u = w.weights.support
y : Y
hy : y ∈ w.weights.support
⊢ (mapDomain f
        { weights := onFinset u (fun x ↦ if x ∈ u then w.weights (f x) else 0) ⋯, nonneg := ⋯, total := ⋯ }.weights)
      y =
    w.weights y

Tactic:
rw [← huw, Finset.mem_image] at hy

Goal state after:
case pos
R : Type u_3
X : Type u_5
Y : Type u_6
inst✝⁴ : Semiring R
inst✝³ : PartialOrder R
inst✝² : IsStrictOrderedRing R
inst✝¹ : ConvexSpace R X
inst✝ : ConvexSpace R Y
f : X → Y
s : Set X
hf : IsAffineMap R f
hs : IsConvexSet R s
w : StdSimplex R Y
hw : ↑w.weights.support ⊆ f '' s
u : Finset X
hus : ↑u ⊆ s
hfu : InjOn f ↑u
huw : Finset.image f u = w.weights.support
y : Y
hy : ∃ a ∈ u, f a = y
⊢ (mapDomain f
        { weights := onFinset u (fun x ↦ if x ∈ u then w.weights (f x) else 0) ⋯, nonneg := ⋯, total := ⋯ }.weights)
      y =
    w.weights y
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
s t : R
hs : 0 ≤ s
ht : 0 ≤ t
h : s + t = 1
x y : P
⊢ ∀ a ∈ (Finsupp.single x s).support ∪ (Finsupp.single y t).support, 0 • (a -ᵥ y) = 0

Tactic:
simp

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
s t : R
hs : 0 ≤ s
ht : 0 ≤ t
h : s + t = 1
x y : P
⊢ 0 • (x -ᵥ y) = 0

Tactic:
simp

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
s t : R
hs : 0 ≤ s
ht : 0 ≤ t
h : s + t = 1
x y : P
⊢ 0 • (y -ᵥ y) = 0

Tactic:
simp

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

Goal state before:
pp: ι : Type u_1
I : Type u_2
R : Type u_3
K : Type u_4
X : Type u_5
Y : Type u_6
inst✝⁴ : Semiring R
inst✝³ : PartialOrder R
inst✝² : IsStrictOrderedRing R
inst✝¹ : ConvexSpace R X
inst✝ : ConvexSpace R Y
f : X → Y
w✝ : StdSimplex R X
s✝ t : Set X
x y : X
s : Set X
hs : IsConvexSet R s
w : StdSimplex R ↑s
⊢ ∀ (i : ↑s), w.weights i ≠ 0 → ↑i ∈ s

Tactic:
simp

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

Goal state before:
pp: ι : Type u_1
I : Type u_2
R : Type u_3
K : Type u_4
X : Type u_5
Y : Type u_6
inst✝⁴ : Semiring R
inst✝³ : PartialOrder R
inst✝² : IsStrictOrderedRing R
inst✝¹ : ConvexSpace R X
inst✝ : ConvexSpace R Y
f : X → Y
w : StdSimplex R X
s✝ t : Set X
x✝ y : X
s : Set X
hs : IsConvexSet R s
x : ↑s
⊢ ⟨iConvexComb (StdSimplex.single x) Subtype.val, ⋯⟩ = x

Tactic:
simp

Goal state after:
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
hwx : w.weights x ≠ 0
hwx' : ∃ y, y ≠ x ∧ w.weights y ≠ 0
⊢ x ∈ ↑(Finset.cons x t hx)

Tactic:
simp

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

Goal state before:
pp: 𝕜 : Type u_1
β : Type u_3
inst✝³ : Field 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
s : Set 𝕜
f : 𝕜 → β
inst✝ : LinearOrder β
hf : QuasilinearOn 𝕜 s f
⊢ MonotoneOn f s ∨ AntitoneOn f s

Tactic:
monotoneOn_or_antitoneOn_iff_uIcc,

Goal state after:
𝕜 : Type u_1
β : Type u_3
inst✝³ : Field 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
s : Set 𝕜
f : 𝕜 → β
inst✝ : LinearOrder β
hf : QuasilinearOn 𝕜 s f
⊢ ∀ a ∈ s, ∀ b ∈ s, ∀ c ∈ s, c ∈ uIcc a b → f c ∈ uIcc (f a) (f b)
Module: Mathlib.Analysis.Convex.Radon

Goal state before:
pp: ι : Type u_1
𝕜 : Type u_2
E : Type u_3
inst✝² : Field 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
F : ι → Set E
s : Finset ι
h_card_small : #s ≤ finrank 𝕜 E + 1
h_inter : ∀ I ⊆ s, #I ≤ finrank 𝕜 E + 1 → (⋂ i ∈ I, F i).Nonempty
⊢ s ⊆ s

Tactic:
simp

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

Goal state before:
pp: X : Type u_2
inst✝² : ConvexSpace ℝ X
inst✝¹ : MetricSpace X
inst✝ : IsConvexDist X
⊢ Continuous fun x ↦ convexCombPair (↑x.1) (1 - ↑x.1) ⋯ ⋯ ⋯ x.2.1 x.2.2

Tactic:
apply continuous_prod_of_continuous_lipschitzWith' (K := 1)

Goal state after:
case ha
X : Type u_2
inst✝² : ConvexSpace ℝ X
inst✝¹ : MetricSpace X
inst✝ : IsConvexDist X
⊢ ∀ (a : ↑(Set.Icc 0 1)), LipschitzWith 1 fun y ↦ convexCombPair (↑(a, y).1) (1 - ↑(a, y).1) ⋯ ⋯ ⋯ (a, y).2.1 (a, y).2.2

case hb
X : Type u_2
inst✝² : ConvexSpace ℝ X
inst✝¹ : MetricSpace X
inst✝ : IsConvexDist X
⊢ ∀ (b : X × X), Continuous fun x ↦ convexCombPair (↑(x, b).1) (1 - ↑(x, b).1) ⋯ ⋯ ⋯ (x, b).2.1 (x, b).2.2
Module: Mathlib.Geometry.Convex.ConvexSpace.Module

Goal state before:
pp: F : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
I : Type u_5
inst✝⁹ : Semiring R
inst✝⁸ : PartialOrder R
inst✝⁷ : IsStrictOrderedRing R
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module R M
inst✝⁴ : AddCommMonoid N
inst✝³ : Module R N
inst✝² : SetLike F M
inst✝¹ : AddSubmonoidClass F M
inst✝ : SMulMemClass F R M
f g : M → N
⊢ ∀ (x : M), ((StdSimplex.single x).weights.sum fun m r ↦ r • m) = x

Tactic:
simp

Goal state after:
Module: Mathlib.Analysis.Convex.SimplicialComplex.Basic

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝³ : Ring 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
K : SimplicialComplex 𝕜 E
s : Finset E
x : E
hx : x ∈ K.vertices
hs : s ∈ K.faces
h : x ∈ (convexHull 𝕜) ↑s
⊢ x ∈ (convexHull 𝕜) ↑{x}

Tactic:
simp

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

Goal state before:
pp: 𝕜 : Type u_2
E : Type u_3
inst✝⁵ : Field 𝕜
inst✝⁴ : LinearOrder 𝕜
inst✝³ : IsStrictOrderedRing 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
F : Finset (Set E)
h_convex : ∀ X ∈ F, Convex 𝕜 X
h_inter : ∀ G ⊆ F, #G ≤ finrank 𝕜 E + 1 → (⋂₀ ↑G).Nonempty
x✝ : E
⊢ x✝ ∈ ⋂₀ ↑F ↔ x✝ ∈ ⋂ X ∈ F, X

Tactic:
simp

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

Goal state before:
pp: 𝕜 : Type u_2
E : Type u_3
inst✝⁵ : Field 𝕜
inst✝⁴ : LinearOrder 𝕜
inst✝³ : IsStrictOrderedRing 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
F : Finset (Set E)
h_convex : ∀ X ∈ F, Convex 𝕜 X
h_inter : ∀ G ⊆ F, #G ≤ finrank 𝕜 E + 1 → (⋂₀ ↑G).Nonempty
G : Finset (Set E)
hG_ss : G ⊆ F
hG_card : #G ≤ finrank 𝕜 E + 1
x✝ : E
⊢ x✝ ∈ ⋂ X ∈ G, X ↔ x✝ ∈ ⋂₀ ↑G

Tactic:
simp

Goal state after:
Module: Mathlib.Analysis.Convex.SimplicialComplex.AffineIndependentUnion

Goal state before:
pp: case inl
ι : Type u_1
inst✝ : DecidableEq ι
G : SimpleGraph ι
v : ι
⊢ {v}.Nonempty ∧ ∀ ⦃b : Finset ι⦄, b ⊆ {v} → b.Nonempty → b ∈ {s | ∃ v, s = {v}} ∪ Sym2.toFinset '' G.edgeSet

Tactic:
simp

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Basic

Goal state before:
pp: case refine_3
V : Type u
inst✝¹ : Fintype V
inst✝ : DecidableEq V
Adj : V → V → Prop
hs : Std.Symm Adj
hi : Std.Irrefl Adj
x✝¹ x✝ : V
⊢ (SimpleGraph.mk' ⟨fun v w ↦ decide (Adj v w), ⋯⟩).Adj x✝¹ x✝ ↔ { Adj := Adj, symm := hs, loopless := hi }.Adj x✝¹ x✝

Tactic:
simp

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Basic

Goal state before:
pp: V : Type u
G₁ G₂ : SimpleGraph V
⊢ G₁.edgeSet ⊆ G₂.edgeSet ↔ G₁ ≤ G₂

Tactic:
simp

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Basic

Goal state before:
pp: V : Type u
G₁ G₂ : SimpleGraph V
⊢ G₁.edgeSet ⊂ G₂.edgeSet ↔ G₁ < G₂

Tactic:
simp

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Basic

Goal state before:
pp: case mk
V : Type u
s : Set (SimpleGraph V)
x✝ : Sym2 V
x y : V
⊢ Quot.mk (Sym2.Rel V) (x, y) ∈ (sSup s).edgeSet ↔ Quot.mk (Sym2.Rel V) (x, y) ∈ ⋃₀ (edgeSet '' s)

Tactic:
simp

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

Goal state before:
pp: 𝕜 : Type u_2
E : Type u_3
inst✝⁷ : Field 𝕜
inst✝⁶ : LinearOrder 𝕜
inst✝⁵ : IsStrictOrderedRing 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : FiniteDimensional 𝕜 E
inst✝¹ : TopologicalSpace E
inst✝ : T2Space E
F : Set (Set E)
h_convex : ∀ X ∈ F, Convex 𝕜 X
h_compact : ∀ X ∈ F, IsCompact X
h_inter : ∀ (G : Finset (Set E)), ↑G ⊆ F → #G ≤ finrank 𝕜 E + 1 → (⋂₀ ↑G).Nonempty
x✝ : E
⊢ x✝ ∈ ⋂₀ F ↔ x✝ ∈ ⋂ X, ↑X

Tactic:
simp

Goal state after: