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

Goal state before:
pp: R : Type u_1
n : Type u_2
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : Semifield R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
M : Matrix n n R
s : R
hs : 0 < s
hM : (∀ (i j : n), 0 ≤ M i j) ∧ (∀ (i : n), ∑ j, M i j = s) ∧ ∀ (j : n), ∑ i, M i j = s
f : n → Finset n := ⋯
A : Finset n
this : ∀ (i : n), ∑ j ∈ f i, M i j = s
h₁ : ∑ i ∈ A, ∑ j ∈ f i, M i j = ↑(#A) * s
h₂ : ∑ i, ∑ j ∈ A.biUnion f, M i j = ↑(#(A.biUnion f)) * s
⊢ ∑ i ∈ A, ∑ j ∈ A.biUnion f, M i j ≤ ∑ i, ∑ j ∈ A.biUnion f, M i j

Tactic:
exact sum_le_sum_of_subset_of_nonneg (by simp) fun _ _ _ => sum_nonneg fun j _ => hM.1 _ _

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u
inst✝⁵ : Field 𝕜
inst✝⁴ : LinearOrder 𝕜
inst✝³ : IsStrictOrderedRing 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : DecidableEq E
t : Finset E
f : E → 𝕜
fpos : ∀ y ∈ t, 0 ≤ f y
fsum : ∑ y ∈ t, f y = 1
g : E → 𝕜
gcombo : ∑ e ∈ t, g e • e = 0
gsum : ∑ e ∈ t, g e = 0
gpos : ∃ i ∈ t, 0 < g i
s : Finset E := {z ∈ t | 0 < g z}
i₀ : E
mem : i₀ ∈ s
w : ∀ i ∈ s, f i₀ / g i₀ ≤ f i / g i
hg : 0 < g i₀
hi₀ : i₀ ∈ t
k : E → 𝕜 := fun z ↦ f z - f i₀ / g i₀ * g z
hk : k i₀ = 0
ksum : ∑ e ∈ t.erase i₀, k e = 1
e : E
a✝ : ¬e = i₀
het : e ∈ t
hes : e ∈ t ∧ 0 < g e
⊢ 0 < g e

Tactic:
exact hes.2

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

Goal state before:
pp: R : Type u_1
inst✝² : Field R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
x y z : R
hxz✝ : x ≤ z
hxz : x < z
hxz' : 0 < z - x
r : R := (y - x) / (z - x)
⊢ y = r * (z - x) + x

Tactic:
simp [r, hxz'.ne']

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

Goal state before:
pp: case pos
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 : P
v : V
r₁ r₂ : R
hr₁ : 0 ≤ r₁
hr₂ : r₁ ≤ r₂
h : r₁ = 0
⊢ (lineMap x (r₂ • v +ᵥ x)) (r₁ / r₂) = r₁ • v +ᵥ x

Tactic:
simp [h]

Goal state after:
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 : P
h : x ≠ y
⊢ midpoint R x y ≠ x

Tactic:
simp [h]

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁶ : TopologicalSpace 𝕜
inst✝⁵ : Ring 𝕜
inst✝⁴ : LinearOrder 𝕜
inst✝³ : IsStrictOrderedRing 𝕜
inst✝² : AddCommMonoid E
inst✝¹ : TopologicalSpace E
inst✝ : Module 𝕜 E
A : Set E
x₁ : E
hx₁A : x₁ ∈ A
x₂ : E
hx₂A : x₂ ∈ A
x : E
hx : x ∈ openSegment 𝕜 x₁ x₂
l : StrongDual 𝕜 E
hAB : IsExposed 𝕜 A {x | x ∈ A ∧ ∀ y ∈ A, l y ≤ l x}
hxB : x ∈ {x | x ∈ A ∧ ∀ y ∈ A, l y ≤ l x}
⊢ x₁ ∈ {x | x ∈ A ∧ ∀ y ∈ A, l y ≤ l x}

Tactic:
have hl : ConvexOn 𝕜 univ l := l.toLinearMap.convexOn convex_univ

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝⁶ : TopologicalSpace 𝕜
inst✝⁵ : Ring 𝕜
inst✝⁴ : LinearOrder 𝕜
inst✝³ : IsStrictOrderedRing 𝕜
inst✝² : AddCommMonoid E
inst✝¹ : TopologicalSpace E
inst✝ : Module 𝕜 E
A : Set E
x₁ : E
hx₁A : x₁ ∈ A
x₂ : E
hx₂A : x₂ ∈ A
x : E
hx : x ∈ openSegment 𝕜 x₁ x₂
l : StrongDual 𝕜 E
hAB : IsExposed 𝕜 A {x | x ∈ A ∧ ∀ y ∈ A, l y ≤ l x}
hxB : x ∈ {x | x ∈ A ∧ ∀ y ∈ A, l y ≤ l x}
hl : ConvexOn 𝕜 univ ⇑l
⊢ x₁ ∈ {x | x ∈ A ∧ ∀ y ∈ A, l y ≤ l x}
Module: Mathlib.Analysis.Convex.GaugeRescale

Goal state before:
pp: case inl
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
hs : Convex ℝ s
hs₀ : s ∈ 𝓝 0
ht : Convex ℝ t
ht₀ : t ∈ 𝓝 0
htb : IsVonNBounded ℝ t
hta : Absorbent ℝ t
⊢ Tendsto (gaugeRescale s t) (𝓝 0) (𝓝 (gaugeRescale s t 0))

Tactic:
gaugeRescale_zero

Goal state after:
case inl
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
hs : Convex ℝ s
hs₀ : s ∈ 𝓝 0
ht : Convex ℝ t
ht₀ : t ∈ 𝓝 0
htb : IsVonNBounded ℝ t
hta : Absorbent ℝ t
⊢ Tendsto (gaugeRescale s t) (𝓝 0) (𝓝 0)
Module: Mathlib.Analysis.Convex.Continuous

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
C : Set E
f : E → ℝ
hf : ConvexOn ℝ C f
x₀ : E
hC : C ∈ 𝓝 x₀
r : ℝ
this : Filter.Tendsto (fun y ↦ 2 • x₀ - y) (𝓝 x₀) (𝓝 x₀)
hr : ∀ᶠ (a : E) in 𝓝 x₀, f a ≤ r
y : E
hx : 2 • x₀ - y ∈ C
hx' : y ∈ C
hfr : f y ≤ r
hfr' : f (2 • x₀ - y) ≤ r
⊢ -f y ≤ |r| + 2 * |f x₀|

Tactic:
← sub_le_iff_le_add,

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
C : Set E
f : E → ℝ
hf : ConvexOn ℝ C f
x₀ : E
hC : C ∈ 𝓝 x₀
r : ℝ
this : Filter.Tendsto (fun y ↦ 2 • x₀ - y) (𝓝 x₀) (𝓝 x₀)
hr : ∀ᶠ (a : E) in 𝓝 x₀, f a ≤ r
y : E
hx : 2 • x₀ - y ∈ C
hx' : y ∈ C
hfr : f y ≤ r
hfr' : f (2 • x₀ - y) ≤ r
⊢ -f y - 2 * |f x₀| ≤ |r|
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
⊢ intrinsicFrontier 𝕜 ∅ = ∅

Tactic:
by simp [intrinsicFrontier]

Goal state after:
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 t : Set P
h : s ⊆ t
x : ↥(affineSpan 𝕜 s)
hx : x ∈ closure[instTopologicalSpaceSubtype] (Subtype.val ⁻¹' s)
⊢ Subtype.val ⁻¹' s ⊆ Set.inclusion ⋯ ⁻¹' Subtype.val ⁻¹' t

Tactic:
exact fun y hy => h hy

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
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
⊢ intrinsicInterior 𝕜 (f '' s) = f '' intrinsicInterior 𝕜 s

Tactic:
rcases s.eq_empty_or_nonempty with rfl | hs

Goal state after:
case inl
𝕜 : 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
e : [Nonempty ↑∅] → ↥(affineSpan 𝕜 ∅) → ↥(affineSpan 𝕜 (f '' ∅))
he_homeo : ∀ [inst : Nonempty ↑∅], IsHomeomorph e
he : ∀ [inst : Nonempty ↑∅] (x : ↥(affineSpan 𝕜 ∅)), ↑(e x) = f ↑x
⊢ intrinsicInterior 𝕜 (f '' ∅) = f '' intrinsicInterior 𝕜 ∅

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
⊢ intrinsicInterior 𝕜 (f '' s) = f '' intrinsicInterior 𝕜 s
Module: Mathlib.Analysis.Convex.Intrinsic

Goal state before:
pp: 𝕜 : Type u_1
V : Type u_2
W : Type u_3
Q : Type u_4
P : Type u_5
inst✝⁸ : Ring 𝕜
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module 𝕜 V
inst✝⁵ : TopologicalSpace P
inst✝⁴ : AddTorsor V P
inst✝³ : AddCommGroup W
inst✝² : Module 𝕜 W
inst✝¹ : TopologicalSpace Q
inst✝ : AddTorsor W Q
f : P → Q
s : Set P
e : [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
⊢ intrinsicFrontier 𝕜 (f '' s) = f '' intrinsicFrontier 𝕜 s

Tactic:
rcases s.eq_empty_or_nonempty with rfl | hs

Goal state after:
case inl
𝕜 : 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
e : [Nonempty ↑∅] → ↥(affineSpan 𝕜 ∅) → ↥(affineSpan 𝕜 (f '' ∅))
he_homeo : ∀ [inst : Nonempty ↑∅], IsHomeomorph e
he : ∀ [inst : Nonempty ↑∅] (x : ↥(affineSpan 𝕜 ∅)), ↑(e x) = f ↑x
⊢ intrinsicFrontier 𝕜 (f '' ∅) = f '' intrinsicFrontier 𝕜 ∅

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
⊢ intrinsicFrontier 𝕜 (f '' s) = f '' intrinsicFrontier 𝕜 s
Module: Mathlib.Analysis.Convex.Intrinsic

Goal state before:
pp: 𝕜 : Type u_1
V : Type u_2
W : Type u_3
Q : Type u_4
P : Type u_5
inst✝⁸ : Ring 𝕜
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module 𝕜 V
inst✝⁵ : TopologicalSpace P
inst✝⁴ : AddTorsor V P
inst✝³ : AddCommGroup W
inst✝² : Module 𝕜 W
inst✝¹ : TopologicalSpace Q
inst✝ : AddTorsor W Q
f : P → Q
s : Set P
e : [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
⊢ intrinsicClosure 𝕜 (f '' s) = f '' intrinsicClosure 𝕜 s

Tactic:
rcases s.eq_empty_or_nonempty with rfl | hs

Goal state after:
case inl
𝕜 : 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
e : [Nonempty ↑∅] → ↥(affineSpan 𝕜 ∅) → ↥(affineSpan 𝕜 (f '' ∅))
he_homeo : ∀ [inst : Nonempty ↑∅], IsHomeomorph e
he : ∀ [inst : Nonempty ↑∅] (x : ↥(affineSpan 𝕜 ∅)), ↑(e x) = f ↑x
⊢ intrinsicClosure 𝕜 (f '' ∅) = f '' intrinsicClosure 𝕜 ∅

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
⊢ intrinsicClosure 𝕜 (f '' s) = f '' intrinsicClosure 𝕜 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 α
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:
swap

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

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
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
⊢ ((Finsupp.single x s + Finsupp.single y t).support.weightedVSubOfPoint id y)
        ⇑(Finsupp.single x s + Finsupp.single y t) +ᵥ
      y =
    s • (x -ᵥ y) +ᵥ y

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
⊢ ∑ i ∈ (Finsupp.single x s + Finsupp.single y t).support, (Finsupp.single x s + Finsupp.single y t) i = 1

Tactic:
swap

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

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
⊢ ((Finsupp.single x s + Finsupp.single y t).support.weightedVSubOfPoint id y)
        ⇑(Finsupp.single x s + Finsupp.single y t) +ᵥ
      y =
    s • (x -ᵥ y) +ᵥ y
Module: Mathlib.Analysis.Convex.MetricSpace

Goal state before:
pp: X : Type u_2
inst✝² : ConvexSpace ℝ X
inst✝¹ : MetricSpace X
inst✝ : IsConvexDist X
x y : X
s t s' t' : ℝ
hs : 0 ≤ s
ht : 0 ≤ t
h : s + t = 1
hs' : 0 ≤ s'
ht' : 0 ≤ t'
h' : s' + t' = 1
hss' : s' ≤ s
this : dist (convexCombPair s t hs ht h x y) (convexCombPair s' t' hs' ht' h' x y) ≤ |s - s'| * dist x y
⊢ |s - s'| * dist x y ≤ dist (convexCombPair s t hs ht h x y) (convexCombPair s' t' hs' ht' h' x y)

Tactic:
← abs_dist_sub_le (z := x)

Goal state after:
X : Type u_2
inst✝² : ConvexSpace ℝ X
inst✝¹ : MetricSpace X
inst✝ : IsConvexDist X
x y : X
s t s' t' : ℝ
hs : 0 ≤ s
ht : 0 ≤ t
h : s + t = 1
hs' : 0 ≤ s'
ht' : 0 ≤ t'
h' : s' + t' = 1
hss' : s' ≤ s
this : dist (convexCombPair s t hs ht h x y) (convexCombPair s' t' hs' ht' h' x y) ≤ |s - s'| * dist x y
⊢ |s - s'| * dist x y ≤ |dist (convexCombPair s t hs ht h x y) x - dist (convexCombPair s' t' hs' ht' h' x y) x|
Module: Mathlib.Analysis.Convex.MetricSpace

Goal state before:
pp: case e'_3
X : Type u_2
inst✝² : ConvexSpace ℝ X
inst✝¹ : MetricSpace X
inst✝ : IsConvexDist X
x y : X
s t s' t' : ℝ
hs : 0 ≤ s
ht : 0 ≤ t
h : s + t = 1
hs' : 0 ≤ s'
ht' : 0 ≤ t'
h' : s' + t' = 1
hss' : s' ≤ s
f : StdSimplex ℝ (Fin 3) := { weights := Finsupp.equivFunOnFinite.symm ![s', s - s', t], nonneg := ⋯, total := ⋯ }
⊢ dist (convexCombPair s t hs ht h x y) (convexCombPair s' t' hs' ht' h' x y) =
    dist (iConvexComb f ![x, x, y]) (iConvexComb f ![x, y, y])

pp: case e'_4
X : Type u_2
inst✝² : ConvexSpace ℝ X
inst✝¹ : MetricSpace X
inst✝ : IsConvexDist X
x y : X
s t s' t' : ℝ
hs : 0 ≤ s
ht : 0 ≤ t
h : s + t = 1
hs' : 0 ≤ s'
ht' : 0 ≤ t'
h' : s' + t' = 1
hss' : s' ≤ s
f : StdSimplex ℝ (Fin 3) := { weights := Finsupp.equivFunOnFinite.symm ![s', s - s', t], nonneg := ⋯, total := ⋯ }
⊢ |s - s'| * dist x y = iConvexComb f fun i ↦ dist (![x, x, y] i) (![x, y, y] i)

Tactic:
swap

Goal state after:
case e'_4
X : Type u_2
inst✝² : ConvexSpace ℝ X
inst✝¹ : MetricSpace X
inst✝ : IsConvexDist X
x y : X
s t s' t' : ℝ
hs : 0 ≤ s
ht : 0 ≤ t
h : s + t = 1
hs' : 0 ≤ s'
ht' : 0 ≤ t'
h' : s' + t' = 1
hss' : s' ≤ s
f : StdSimplex ℝ (Fin 3) := { weights := Finsupp.equivFunOnFinite.symm ![s', s - s', t], nonneg := ⋯, total := ⋯ }
⊢ |s - s'| * dist x y = iConvexComb f fun i ↦ dist (![x, x, y] i) (![x, y, y] i)

case e'_3
X : Type u_2
inst✝² : ConvexSpace ℝ X
inst✝¹ : MetricSpace X
inst✝ : IsConvexDist X
x y : X
s t s' t' : ℝ
hs : 0 ≤ s
ht : 0 ≤ t
h : s + t = 1
hs' : 0 ≤ s'
ht' : 0 ≤ t'
h' : s' + t' = 1
hss' : s' ≤ s
f : StdSimplex ℝ (Fin 3) := { weights := Finsupp.equivFunOnFinite.symm ![s', s - s', t], nonneg := ⋯, total := ⋯ }
⊢ dist (convexCombPair s t hs ht h x y) (convexCombPair s' t' hs' ht' h' x y) =
    dist (iConvexComb f ![x, x, y]) (iConvexComb f ![x, y, y])
Module: Mathlib.Analysis.Convex.MetricSpace

Goal state before:
pp: 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

Tactic:
intro i x y

Goal state after:
case ha
X : Type u_2
inst✝² : ConvexSpace ℝ X
inst✝¹ : MetricSpace X
inst✝ : IsConvexDist X
i : ↑(Set.Icc 0 1)
x y : X × X
⊢ edist ((fun y ↦ convexCombPair (↑(i, y).1) (1 - ↑(i, y).1) ⋯ ⋯ ⋯ (i, y).2.1 (i, y).2.2) x)
      ((fun y ↦ convexCombPair (↑(i, y).1) (1 - ↑(i, y).1) ⋯ ⋯ ⋯ (i, y).2.1 (i, y).2.2) y) ≤
    ↑1 * edist x y
Module: Mathlib.Analysis.Convex.MetricSpace

Goal state before:
pp: case ha
X : Type u_2
inst✝² : ConvexSpace ℝ X
inst✝¹ : MetricSpace X
inst✝ : IsConvexDist X
i : ↑(Set.Icc 0 1)
x y : X × X
⊢ ↑i * max (dist x.1 y.1) (dist x.2 y.2) + (1 - ↑i) * dist x.2 y.2 ≤ max (dist x.1 y.1) (dist x.2 y.2)

pp: case ha
X : Type u_2
inst✝² : ConvexSpace ℝ X
inst✝¹ : MetricSpace X
inst✝ : IsConvexDist X
i : ↑(Set.Icc 0 1)
x y : X × X
⊢ 0 ≤ ↑i

Tactic:
swap

Goal state after:
case ha
X : Type u_2
inst✝² : ConvexSpace ℝ X
inst✝¹ : MetricSpace X
inst✝ : IsConvexDist X
i : ↑(Set.Icc 0 1)
x y : X × X
⊢ 0 ≤ ↑i

case ha
X : Type u_2
inst✝² : ConvexSpace ℝ X
inst✝¹ : MetricSpace X
inst✝ : IsConvexDist X
i : ↑(Set.Icc 0 1)
x y : X × X
⊢ ↑i * max (dist x.1 y.1) (dist x.2 y.2) + (1 - ↑i) * dist x.2 y.2 ≤ max (dist x.1 y.1) (dist x.2 y.2)
Module: Mathlib.Analysis.Convex.MetricSpace

Goal state before:
pp: case ha
X : Type u_2
inst✝² : ConvexSpace ℝ X
inst✝¹ : MetricSpace X
inst✝ : IsConvexDist X
i : ↑(Set.Icc 0 1)
x y : X × X
⊢ ↑i * max (dist x.1 y.1) (dist x.2 y.2) + (1 - ↑i) * max (dist x.1 y.1) (dist x.2 y.2) ≤
    max (dist x.1 y.1) (dist x.2 y.2)

pp: case ha
X : Type u_2
inst✝² : ConvexSpace ℝ X
inst✝¹ : MetricSpace X
inst✝ : IsConvexDist X
i : ↑(Set.Icc 0 1)
x y : X × X
⊢ 0 ≤ 1 - ↑i

Tactic:
swap

Goal state after:
case ha
X : Type u_2
inst✝² : ConvexSpace ℝ X
inst✝¹ : MetricSpace X
inst✝ : IsConvexDist X
i : ↑(Set.Icc 0 1)
x y : X × X
⊢ 0 ≤ 1 - ↑i

case ha
X : Type u_2
inst✝² : ConvexSpace ℝ X
inst✝¹ : MetricSpace X
inst✝ : IsConvexDist X
i : ↑(Set.Icc 0 1)
x y : X × X
⊢ ↑i * max (dist x.1 y.1) (dist x.2 y.2) + (1 - ↑i) * max (dist x.1 y.1) (dist x.2 y.2) ≤
    max (dist x.1 y.1) (dist x.2 y.2)
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)
  · intro i x y
    simp only [← coe_nnreal_ennreal_nndist, ENNReal.coe_one, one_mul, ENNReal.coe_le_coe,
      NNReal.toReal_le, coe_nndist]
    grw [dist_convexCombPair_convexCombPair_le, Prod.dist_eq]
    nth_grw 1 [le_max_left (dist x.1 y.1) (dist x.2 y.2)]
    swap; · simpa using i.prop.left
    nth_grw 2 [le_max_right (dist x.1 y.1) (dist x.2 y.2)]
    swap; · simpa using i.prop.right
    rw [← add_mul, add_sub_cancel, one_mul]
  · intro b
    refine LipschitzWith.continuous (K := nndist b.1 b.2) fun x y ↦ ?_
    rw [mul_comm]
    simp [← coe_nnreal_ennreal_nndist, ← ENNReal.coe_mul, NNReal.toReal_le,
      dist_convexCombPair_convexCombPair, Subtype.dist_eq, dist_eq_norm]

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

Goal state before:
pp: case inl
R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁵ : CommRing R
inst✝⁴ : PartialOrder R
inst✝³ : IsStrictOrderedRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
s : AffineSubspace R P
x z : P
t : R
ht0 : 0 ≤ t
ht1 : t ≤ 1
hy : (lineMap x z) t ∈ s
ht1' : t < 1
⊢ SameRay R (x -ᵥ (lineMap x z) t) ((lineMap x z) t -ᵥ z)

pp: case inr
R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁵ : CommRing R
inst✝⁴ : PartialOrder R
inst✝³ : IsStrictOrderedRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
s : AffineSubspace R P
x z : P
ht0 : 0 ≤ 1
ht1 : 1 ≤ 1
hy : (lineMap x z) 1 ∈ s
⊢ SameRay R (x -ᵥ (lineMap x z) 1) ((lineMap x z) 1 -ᵥ z)

Tactic:
swap

Goal state after:
case inr
R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁵ : CommRing R
inst✝⁴ : PartialOrder R
inst✝³ : IsStrictOrderedRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
s : AffineSubspace R P
x z : P
ht0 : 0 ≤ 1
ht1 : 1 ≤ 1
hy : (lineMap x z) 1 ∈ s
⊢ SameRay R (x -ᵥ (lineMap x z) 1) ((lineMap x z) 1 -ᵥ z)

case inl
R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁵ : CommRing R
inst✝⁴ : PartialOrder R
inst✝³ : IsStrictOrderedRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
s : AffineSubspace R P
x z : P
t : R
ht0 : 0 ≤ t
ht1 : t ≤ 1
hy : (lineMap x z) t ∈ s
ht1' : t < 1
⊢ SameRay R (x -ᵥ (lineMap x z) t) ((lineMap x z) t -ᵥ z)
Module: Mathlib.Analysis.Convex.Side

Goal state before:
pp: case inl.inl
R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁵ : CommRing R
inst✝⁴ : PartialOrder R
inst✝³ : IsStrictOrderedRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
s : AffineSubspace R P
x z : P
t : R
ht0 : 0 ≤ t
ht1 : t ≤ 1
hy : (lineMap x z) t ∈ s
ht1' : t < 1
ht0' : 0 < t
⊢ SameRay R (x -ᵥ (lineMap x z) t) ((lineMap x z) t -ᵥ z)

pp: case inl.inr
R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁵ : CommRing R
inst✝⁴ : PartialOrder R
inst✝³ : IsStrictOrderedRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
s : AffineSubspace R P
x z : P
ht0 : 0 ≤ 0
ht1 : 0 ≤ 1
hy : (lineMap x z) 0 ∈ s
ht1' : 0 < 1
⊢ SameRay R (x -ᵥ (lineMap x z) 0) ((lineMap x z) 0 -ᵥ z)

Tactic:
swap

Goal state after:
case inl.inr
R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁵ : CommRing R
inst✝⁴ : PartialOrder R
inst✝³ : IsStrictOrderedRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
s : AffineSubspace R P
x z : P
ht0 : 0 ≤ 0
ht1 : 0 ≤ 1
hy : (lineMap x z) 0 ∈ s
ht1' : 0 < 1
⊢ SameRay R (x -ᵥ (lineMap x z) 0) ((lineMap x z) 0 -ᵥ z)

case inl.inl
R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁵ : CommRing R
inst✝⁴ : PartialOrder R
inst✝³ : IsStrictOrderedRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
s : AffineSubspace R P
x z : P
t : R
ht0 : 0 ≤ t
ht1 : t ≤ 1
hy : (lineMap x z) t ∈ s
ht1' : t < 1
ht0' : 0 < t
⊢ SameRay R (x -ᵥ (lineMap x z) t) ((lineMap x z) t -ᵥ z)
Module: Mathlib.Analysis.Convex.StrictCombination

Goal state before:
pp: V : Type u_2
P : Type u_3
ι : Type u_4
inst✝⁴ : NormedAddCommGroup V
inst✝³ : NormedSpace ℝ V
inst✝² : StrictConvexSpace ℝ V
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor V P
t : Finset ι
w : ι → ℝ
p₀ : P
r : ℝ
p : ι → P
h0 : ∀ i ∈ t, 0 ≤ w i
h1 : ∑ i ∈ t, w i = 1
i j : ι
hi : i ∈ t
hj : j ∈ t
hij : p i ≠ p j
hi0 : w i ≠ 0
hj0 : w j ≠ 0
hp : ∀ i ∈ t, dist (p i) p₀ ≤ r
⊢ dist ((affineCombination ℝ t p) w) p₀ < r

Tactic:
by
  rw [affineCombination_eq_weightedVSubOfPoint_vadd_of_sum_eq_one _ _ _ h1 p₀,
    weightedVSubOfPoint_apply, dist_vadd_left]
  simp_rw [dist_eq_norm_vsub] at hp
  exact norm_sum_lt_of_strictConvexSpace h0 h1 hi hj (by simpa using hij) hi0 hj0 hp

Goal state after: