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

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁶ : Semiring 𝕜
inst✝⁵ : PartialOrder 𝕜
E : Type u_2
inst✝⁴ : AddCommMonoid E
inst✝³ : TopologicalSpace E
inst✝² : ContinuousAdd E
inst✝¹ : SMul 𝕜 E
inst✝ : ContinuousConstSMul 𝕜 E
K : ConvexCone 𝕜 E
c : 𝕜
hc : 0 < c
x✝ : E
h₁ : x✝ ∈ closure ↑K
⊢ Continuous (HSMul.hSMul c)

Tactic:
by

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
⊢ k i₀ • i₀ = 0

Tactic:
by

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_3
inst✝⁹ : AddCommMonoid E
inst✝⁸ : TopologicalSpace E
inst✝⁷ : Semifield 𝕜
inst✝⁶ : LinearOrder 𝕜
inst✝⁵ : Module 𝕜 E
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : OrderTopology 𝕜
inst✝² : DenselyOrdered 𝕜
inst✝¹ : NoMaxOrder 𝕜
inst✝ : ContinuousSMul 𝕜 E
C : ConvexCone 𝕜 E
hSclos : IsClosed ↑C
x : E
hx : x ∈ ↑C
f : 𝕜 → E := fun x_1 ↦ x_1 • x
⊢ f '' Ioi 0 ⊆ ↑C

Tactic:
by

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_3
inst✝⁹ : AddCommMonoid E
inst✝⁸ : TopologicalSpace E
inst✝⁷ : Semifield 𝕜
inst✝⁶ : LinearOrder 𝕜
inst✝⁵ : Module 𝕜 E
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : OrderTopology 𝕜
inst✝² : DenselyOrdered 𝕜
inst✝¹ : NoMaxOrder 𝕜
inst✝ : ContinuousSMul 𝕜 E
C : ConvexCone 𝕜 E
hSclos : IsClosed ↑C
x : E
hx : x ∈ ↑C
f : 𝕜 → E := fun x_1 ↦ x_1 • x
hfS : closure (f '' Ioi 0) ⊆ ↑C
⊢ ContinuousWithinAt f (Ioi 0) 0

Tactic:
by

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_3
inst✝⁹ : AddCommMonoid E
inst✝⁸ : TopologicalSpace E
inst✝⁷ : Semifield 𝕜
inst✝⁶ : LinearOrder 𝕜
inst✝⁵ : Module 𝕜 E
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : OrderTopology 𝕜
inst✝² : DenselyOrdered 𝕜
inst✝¹ : NoMaxOrder 𝕜
inst✝ : ContinuousSMul 𝕜 E
C : ConvexCone 𝕜 E
hSclos : IsClosed ↑C
x : E
hx : x ∈ ↑C
f : 𝕜 → E := fun x_1 ↦ x_1 • x
hfS : closure (f '' Ioi 0) ⊆ ↑C
fc : ContinuousWithinAt f (Ioi 0) 0
⊢ 0 ∈ closure (Ioi 0)

Tactic:
by

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_3
inst✝⁹ : AddCommMonoid E
inst✝⁸ : TopologicalSpace E
inst✝⁷ : Semifield 𝕜
inst✝⁶ : LinearOrder 𝕜
inst✝⁵ : Module 𝕜 E
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : OrderTopology 𝕜
inst✝² : DenselyOrdered 𝕜
inst✝¹ : NoMaxOrder 𝕜
inst✝ : ContinuousSMul 𝕜 E
C : ConvexCone 𝕜 E
hC : (↑C).Nonempty
hSclos : IsClosed ↑C
⊢ C.Pointed

Tactic:
by

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 ∈ t, (f e - f i₀ / g i₀ * g e) • e = t.centerMass f id

Tactic:
by

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
h : ¬AffineIndependent 𝕜 Subtype.val
x : E
m : x ∈ (convexHull 𝕜) ↑t
⊢ ∃ y, x ∈ (convexHull 𝕜) ↑(t.erase ↑y)

Tactic:
by

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
s : Set E
x : E
hx : x ∈ (convexHull 𝕜) s
⊢ {t | ↑t ⊆ s ∧ x ∈ (convexHull 𝕜) ↑t}.Nonempty

Tactic:
by

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
s : Set E
x : E
hx : x ∈ (convexHull 𝕜) s
⊢ (minCardFinsetOfMemConvexHull hx).Nonempty

Tactic:
by

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
s : Set E
x : E
hx : x ∈ (convexHull 𝕜) s
t : Finset E
ht₁ : ↑t ⊆ s
ht₂ : x ∈ (convexHull 𝕜) ↑t
⊢ t ∈ {t | ↑t ⊆ s ∧ x ∈ (convexHull 𝕜) ↑t}

Tactic:
by

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✝⁶ : Ring R
inst✝⁵ : LinearOrder R
inst✝⁴ : IsStrictOrderedRing R
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : AddTorsor V P
inst✝ : IsTorsionFree R V
t : Affine.Triangle R P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
p₁ p₂ p : P
h₁ : Sbtw R (t.points i₂) p₁ (t.points i₃)
h₂ : Sbtw R (t.points i₁) p₂ (t.points i₃)
h₁' : p ∈ line[R, t.points i₁, p₁]
h₂' : p ∈ line[R, t.points i₂, p₂]
⊢ Sbtw R (t.points i₁) p p₁

Tactic:
by

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:
by

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
⊢ Wbtw R x y z ↔ x ≤ y ∧ y ≤ z

Tactic:
by

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
s : Set E
x : E
hx : x ∈ (convexHull 𝕜) s
⊢ AffineIndependent 𝕜 Subtype.val

Tactic:
by

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 z : P
⊢ Wbtw R x y z ↔ x = y ∨ z ∈ ⇑(lineMap x y) '' Set.Ici 1

Tactic:
by

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 z : P
h : Wbtw R x y z
hne : x ≠ y
⊢ z ∈ line[R, x, y]

Tactic:
by

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
s : Set E
⊢ (convexHull 𝕜) s = ⋃ t, ⋃ (_ : ↑t ⊆ s), ⋃ (_ : AffineIndependent 𝕜 Subtype.val), (convexHull 𝕜) ↑t

Tactic:
by

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

Goal state before:
pp: R : Type u_1
n : Type u_2
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : Field R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
h✝ : Nonempty n
d : ℕ
ih :
  ∀ m < d,
    ∀ (M : Matrix n n R) (s : R),
      0 ≤ s →
        (∃ M' ∈ doublyStochastic R n, M = s • M') →
          #{i | M i.1 i.2 ≠ 0} = m → ∃ w, (∀ (σ : Equiv.Perm n), 0 ≤ w σ) ∧ ∑ σ, w σ • Equiv.Perm.permMatrix R σ = M
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
hd : #{i | M i.1 i.2 ≠ 0} = d
hs'✝ : 0 < s
σ : Equiv.Perm n
hσ : ∀ (i j : n), M i j = 0 → Equiv.Perm.permMatrix R σ i j = 0
i : n
hi : i ∈ univ
hi' : ∀ x' ∈ univ, M i (σ i) ≤ M x' (σ x')
N : Matrix n n R := M - M i (σ i) • Equiv.Perm.permMatrix R σ
hMi' : 0 < M i (σ i)
s' : R := s - M i (σ i)
hs' : 0 ≤ s'
this : ∃ M' ∈ doublyStochastic R n, N = s' • M'
⊢ N i (σ i) = 0

Tactic:
by

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 z : P
⊢ Sbtw R x y z ↔ x ≠ y ∧ z ∈ ⇑(lineMap x y) '' Set.Ioi 1

Tactic:
by

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 z : P
⊢ Wbtw R x y z ↔ z = y ∨ x ∈ ⇑(lineMap z y) '' Set.Ici 1

Tactic:
by

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

Goal state before:
pp: R : Type u_1
n : Type u_2
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : Field R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
h✝ : Nonempty n
d : ℕ
ih :
  ∀ m < d,
    ∀ (M : Matrix n n R) (s : R),
      0 ≤ s →
        (∃ M' ∈ doublyStochastic R n, M = s • M') →
          #{i | M i.1 i.2 ≠ 0} = m → ∃ w, (∀ (σ : Equiv.Perm n), 0 ≤ w σ) ∧ ∑ σ, w σ • Equiv.Perm.permMatrix R σ = M
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
hd : #{i | M i.1 i.2 ≠ 0} = d
hs'✝ : 0 < s
σ : Equiv.Perm n
hσ : ∀ (i j : n), M i j = 0 → Equiv.Perm.permMatrix R σ i j = 0
i : n
hi : i ∈ univ
hi' : ∀ x' ∈ univ, M i (σ i) ≤ M x' (σ x')
N : Matrix n n R := M - M i (σ i) • Equiv.Perm.permMatrix R σ
hMi' : 0 < M i (σ i)
s' : R := s - M i (σ i)
hs' : 0 ≤ s'
this : ∃ M' ∈ doublyStochastic R n, N = s' • M'
i' j' : n
a✝ : (i', j') ∈ univ
hN' : N (i', j').1 (i', j').2 ≠ 0
hM' : M (i', j').1 (i', j').2 = 0
⊢ σ i' ≠ j'

Tactic:
by

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 z : P
⊢ Sbtw R x y z ↔ z ≠ y ∧ x ∈ ⇑(lineMap z y) '' Set.Ioi 1

Tactic:
by

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✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x z : P
s : AffineSubspace R P
hx : x ∈ s
ε : R
hy : (lineMap x z) ε ∈ s
hxy : x ≠ (lineMap x z) ε
⊢ ε ≠ 0

Tactic:
by

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✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x y z : P
s : AffineSubspace R P
hxyz : Wbtw R x y z
hx : x ∈ s
hy : y ∈ s
hxy : x ≠ y
⊢ z ∈ s

Tactic:
by

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 : P
v : V
r₁ r₂ : R
hr₁ : 0 ≤ r₁
hr₂ : r₁ ≤ r₂
⊢ Wbtw R x (r₁ • v +ᵥ x) (r₂ • v +ᵥ x)

Tactic:
by

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 : P
v : V
r₁ r₂ : R
hr₁ : 0 ≤ r₁
hr₂ : 0 ≤ r₂
⊢ Wbtw R x (r₁ • v +ᵥ x) (r₂ • v +ᵥ x) ∨ Wbtw R x (r₂ • v +ᵥ x) (r₁ • v +ᵥ x)

Tactic:
by

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 : P
v : V
r₁ r₂ : R
hr₁ : r₁ ≤ 0
hr₂ : r₂ ≤ r₁
⊢ Wbtw R x (r₁ • v +ᵥ x) (r₂ • v +ᵥ x)

Tactic:
by

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 : P
v : V
r₁ r₂ : R
hr₁ : r₁ ≤ 0
hr₂ : r₂ ≤ 0
⊢ Wbtw R x (r₁ • v +ᵥ x) (r₂ • v +ᵥ x) ∨ Wbtw R x (r₂ • v +ᵥ x) (r₁ • v +ᵥ x)

Tactic:
by

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

Goal state before:
pp: R : Type u_1
n : Type u_2
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : Field R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
h✝ : Nonempty n
d : ℕ
ih :
  ∀ m < d,
    ∀ (M : Matrix n n R) (s : R),
      0 ≤ s →
        (∃ M' ∈ doublyStochastic R n, M = s • M') →
          #{i | M i.1 i.2 ≠ 0} = m → ∃ w, (∀ (σ : Equiv.Perm n), 0 ≤ w σ) ∧ ∑ σ, w σ • Equiv.Perm.permMatrix R σ = M
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
hd : #{i | M i.1 i.2 ≠ 0} = d
hs'✝ : 0 < s
σ : Equiv.Perm n
hσ : ∀ (i j : n), M i j = 0 → Equiv.Perm.permMatrix R σ i j = 0
i : n
hi : i ∈ univ
hi' : ∀ x' ∈ univ, M i (σ i) ≤ M x' (σ x')
N : Matrix n n R := M - M i (σ i) • Equiv.Perm.permMatrix R σ
hMi' : 0 < M i (σ i)
s' : R := s - M i (σ i)
hs' : 0 ≤ s'
this : ∃ M' ∈ doublyStochastic R n, N = s' • M'
i' j' : n
a✝ : (i', j') ∈ univ
hN' : N (i', j').1 (i', j').2 ≠ 0
hM' : M (i', j').1 (i', j').2 = 0
hσ' : σ i' ≠ j'
⊢ N (i', j').1 (i', j').2 = 0

Tactic:
by

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 : P
v : V
r₁ r₂ : R
hr₁ : r₁ ≤ 0
hr₂ : 0 ≤ r₂
⊢ Wbtw R (r₁ • v +ᵥ x) x (r₂ • v +ᵥ x)

Tactic:
by

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 : P
v : V
r₁ r₂ : R
hr₁ : 0 ≤ r₁
hr₂ : r₂ ≤ 0
⊢ Wbtw R (r₁ • v +ᵥ x) x (r₂ • v +ᵥ x)

Tactic:
by

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

Goal state before:
pp: R : Type u_1
n : Type u_2
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : Field R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
h✝ : Nonempty n
d : ℕ
ih :
  ∀ m < d,
    ∀ (M : Matrix n n R) (s : R),
      0 ≤ s →
        (∃ M' ∈ doublyStochastic R n, M = s • M') →
          #{i | M i.1 i.2 ≠ 0} = m → ∃ w, (∀ (σ : Equiv.Perm n), 0 ≤ w σ) ∧ ∑ σ, w σ • Equiv.Perm.permMatrix R σ = M
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
hd : #{i | M i.1 i.2 ≠ 0} = d
hs'✝ : 0 < s
σ : Equiv.Perm n
hσ : ∀ (i j : n), M i j = 0 → Equiv.Perm.permMatrix R σ i j = 0
i : n
hi : i ∈ univ
hi' : ∀ x' ∈ univ, M i (σ i) ≤ M x' (σ x')
N : Matrix n n R := M - M i (σ i) • Equiv.Perm.permMatrix R σ
hMi' : 0 < M i (σ i)
s' : R := s - M i (σ i)
hs' : 0 ≤ s'
this : ∃ M' ∈ doublyStochastic R n, N = s' • M'
⊢ #{i | N i.1 i.2 ≠ 0} < d

Tactic:
by

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
w z : P
t₁ : R
ht₁ : t₁ ∈ Set.Icc 0 1
t₂ : R
ht₂ : t₂ ∈ Set.Icc 0 1
h : t₂ * t₁ = 1
this : t₁ = 1
⊢ ((t₁ - 1) * ((1 - 1) / (1 - 1)) + 1) • (z -ᵥ w) = t₁ • (z -ᵥ w)

Tactic:
by

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
s : Set E
x : E
hx : x ∈ (convexHull 𝕜) s
⊢ ∃ ι x_1 z w, Set.range z ⊆ s ∧ AffineIndependent 𝕜 z ∧ (∀ (i : ι), 0 < w i) ∧ ∑ i, w i = 1 ∧ ∑ i, w i • z i = x

Tactic:
by

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
w x y z : P
h₁ : Wbtw R w y z
h₂ : Wbtw R w x y
⊢ Wbtw R x y z

Tactic:
by

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
w x y z : P
h₁ : Wbtw R w x z
h₂ : Wbtw R x y z
⊢ Wbtw R w x y

Tactic:
by

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
w x y z : P
t₁ : R
ht₁ : t₁ ∈ Set.Icc 0 1
hx : (lineMap w y) t₁ = x
t₂ : R
ht₂ : t₂ ∈ Set.Icc 0 1
hy : (lineMap x z) t₂ = y
h_ne : 1 - t₁ + t₁ * t₂ = 0
⊢ t₁ = 1

Tactic:
by

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
w x y z : P
h_ne : x ≠ y
t₁ : R
ht₁ : t₁ ∈ Set.Icc 0 1
hx : (lineMap w y) t₁ = x
t₂ : R
ht₂ : t₂ ∈ Set.Icc 0 1
hy : (lineMap x z) t₂ = y
⊢ 1 - t₁ + t₁ * t₂ ≠ 0

Tactic:
by

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

Goal state before:
pp: R : Type u_1
n : Type u_2
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : Field R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
M : Matrix n n R
s : R
hs : 0 ≤ s
hM : ∃ M' ∈ doublyStochastic R n, M = s • M'
⊢ ∃ w, (∀ (σ : Equiv.Perm n), 0 ≤ w σ) ∧ ∑ σ, w σ • Equiv.Perm.permMatrix R σ = M

Tactic:
by

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

Goal state before:
pp: R : Type u_1
n : Type u_2
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : Field R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
M : Matrix n n R
hM : M ∈ doublyStochastic R n
h✝ : IsEmpty n
⊢ ∀ (σ : Equiv.Perm n), 0 ≤ (fun x ↦ 1) σ

Tactic:
by

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

Goal state before:
pp: R : Type u_1
n : Type u_2
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : Field R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
M : Matrix n n R
hM : M ∈ doublyStochastic R n
h✝ : IsEmpty n
⊢ ∑ σ, (fun x ↦ 1) σ = 1

Tactic:
by

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

Goal state before:
pp: R : Type u_1
n : Type u_2
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : Field R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
M : Matrix n n R
hM : M ∈ doublyStochastic R n
h✝ : Nonempty n
⊢ 0 ≤ 1

Tactic:
by

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

Goal state before:
pp: R : Type u_1
n : Type u_2
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : Field R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
M : Matrix n n R
hM : M ∈ doublyStochastic R n
h✝ : Nonempty n
⊢ M = 1 • M

Tactic:
by

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

Goal state before:
pp: R : Type u_1
n : Type u_2
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : Field R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
M : Matrix n n R
hM : M ∈ doublyStochastic R n
h✝ : Nonempty n
w : Equiv.Perm n → R
hw1 : ∀ (σ : Equiv.Perm n), 0 ≤ w σ
hw3 : ∑ σ, w σ • Equiv.Perm.permMatrix R σ = M
inhabited_h : Inhabited n
⊢ ∑ j, ∑ σ, w σ • Equiv.Perm.permMatrix R σ default j = 1

Tactic:
by

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

Goal state before:
pp: R : Type u_1
n : Type u_2
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : Field R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
M : Matrix n n R
hM : M ∈ doublyStochastic R n
⊢ ∃ w, (∀ (σ : Equiv.Perm n), 0 ≤ w σ) ∧ ∑ σ, w σ = 1 ∧ ∑ σ, w σ • Equiv.Perm.permMatrix R σ = M

Tactic:
by

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

Goal state before:
pp: R : Type u_1
n : Type u_2
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : Field R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
M : Matrix n n R
hM : M ∈ ↑(doublyStochastic R n)
w : Equiv.Perm n → R
hw1 : ∀ (σ : Equiv.Perm n), 0 ≤ w σ
hw2 : ∑ σ, w σ = 1
hw3 : ∑ σ, w σ • Equiv.Perm.permMatrix R σ = M
⊢ ∀ (i : Equiv.Perm n), Equiv.Perm.permMatrix R i ∈ {x | ∃ σ, Equiv.Perm.permMatrix R σ = x}

Tactic:
by

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

Goal state before:
pp: R : Type u_1
n : Type u_2
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : Field R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
⊢ ↑(doublyStochastic R n) = (convexHull R) {x | ∃ σ, Equiv.Perm.permMatrix R σ = x}

Tactic:
by

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
w x y z : P
h₁ : Wbtw R w x y
h₂ : Wbtw R x y z
h_ne : x ≠ y
⊢ Wbtw R w x z

Tactic:
by

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

Goal state before:
pp: R : Type u_1
n : Type u_2
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : Field R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
σ : Equiv.Perm n
x₁ : Matrix n n R
hx₁ : x₁ ∈ ↑(doublyStochastic R n)
x₂ : Matrix n n R
hx₂ : x₂ ∈ ↑(doublyStochastic R n)
hσ : Equiv.Perm.permMatrix R σ ∈ openSegment R x₁ x₂
this : ∀ (i j : n), x₁ i j = x₂ i j
⊢ x₁ = x₂

Tactic:
by

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✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x y z : P
h : Wbtw R x y z
⊢ Collinear R {x, y, z}

Tactic:
by

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

Goal state before:
pp: R : Type u_1
n : Type u_2
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : Field R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
σ : Equiv.Perm n
x₁ : Matrix n n R
hx₁ : x₁ ∈ ↑(doublyStochastic R n)
x₂ : Matrix n n R
hx₂ : x₂ ∈ ↑(doublyStochastic R n)
hσ : Equiv.Perm.permMatrix R σ ∈ openSegment R x₁ x₂
this : ∀ (i j : n), x₁ i j = x₂ i j
⊢ x₁ = Equiv.Perm.permMatrix R σ

Tactic:
by

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

Goal state before:
pp: R : Type u_1
n : Type u_2
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : Field R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
σ : Equiv.Perm n
x₁ : Matrix n n R
hx₁ : x₁ ∈ ↑(doublyStochastic R n)
x₂ : Matrix n n R
hx₂ : x₂ ∈ ↑(doublyStochastic R n)
hσ : Equiv.Perm.permMatrix R σ ∈ openSegment R x₁ x₂
i j : n
h₁ : Equiv.Perm.permMatrix R σ i j ∈ openSegment R (x₁ i j) (x₂ i j)
h : x₁ i j ≠ x₂ i j
⊢ openSegment R (x₁ i j) (x₂ i j) ⊆ Set.Ioo 0 1

Tactic:
by

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

Goal state before:
pp: R : Type u_1
n : Type u_2
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : Field R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
⊢ Set.extremePoints R ↑(doublyStochastic R n) = {x | ∃ σ, Equiv.Perm.permMatrix R σ = x}

Tactic:
by

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

Goal state before:
pp: n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
M : Matrix n n ℝ
hM : M ∈ (convexHull ℝ) {x | ∃ σ, Equiv.Perm.permMatrix ℝ σ = x}
⊢ {x | ∃ σ, Equiv.Perm.permMatrix ℝ σ = x} ⊆ Set.univ

Tactic:
by

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

Goal state before:
pp: n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
M : Matrix n n ℝ
hM : M ∈ doublyStochastic ℝ n
⊢ ‖M‖ ≤ 1

Tactic:
by

Goal state after: