-- Mathlib/Analysis/Convex/Birkhoff.lean
theorem doublyStochastic_eq_convexHull_permMatrix :
    doublyStochastic R n = convexHull R {σ.permMatrix R | σ : Equiv.Perm n}

Proof state:
case intro
R : Type u_1
n : Type u_2
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : LinearOrderedField R
h : Equiv.Perm n
⊢ Equiv.Perm.permMatrix R h ∈ ↑(doublyStochastic R n)

Tactic:
exact permMatrix_mem_doublyStochastic

Result:
no goals

Proof state:
R : Type u_1
n : Type u_2
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : LinearOrderedField R
⊢ ↑(doublyStochastic R n) = (convexHull R) {x | ∃ σ, Equiv.Perm.permMatrix R σ = x}

Tactic:
refine (convexHull_min ?g1 convex_doublyStochastic).antisymm' fun M hM => ?g2

Result:
case g1
R : Type u_1
n : Type u_2
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : LinearOrderedField R
⊢ {x | ∃ σ, Equiv.Perm.permMatrix R σ = x} ⊆ ↑(doublyStochastic R n)

case g2
R : Type u_1
n : Type u_2
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : LinearOrderedField R
M : Matrix n n R
hM : M ∈ ↑(doublyStochastic R n)
⊢ M ∈ (convexHull R) {x | ∃ σ, Equiv.Perm.permMatrix R σ = x}

Proof state:
R : Type u_1
n : Type u_2
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : LinearOrderedField R
M : Matrix n n R
hM : M ∈ ↑(doublyStochastic R n)
w : Equiv.Perm n → R
hw1 : ∀ (σ : Equiv.Perm n), 0 ≤ w σ
hw2 : ∑ σ : Equiv.Perm n, w σ = 1
hw3 : ∑ σ : Equiv.Perm n, w σ • Equiv.Perm.permMatrix R σ = M
⊢ ∀ (i : Equiv.Perm n), (fun x => Equiv.Perm.permMatrix R x) i ∈ {x | ∃ σ, Equiv.Perm.permMatrix R σ = x}

Tactic:
simp

Result:
no goals

Proof state:
R : Type u_1
n : Type u_2
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : LinearOrderedField R
M : Matrix n n R
hM : M ∈ ↑(doublyStochastic R n)
⊢ M ∈ (convexHull R) {x | ∃ σ, Equiv.Perm.permMatrix R σ = x}

Tactic:
obtain ⟨w, hw1, hw2, hw3⟩ := exists_eq_sum_perm_of_mem_doublyStochastic hM

Result:
case intro.intro.intro
R : Type u_1
n : Type u_2
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : LinearOrderedField R
M : Matrix n n R
hM : M ∈ ↑(doublyStochastic R n)
w : Equiv.Perm n → R
hw1 : ∀ (σ : Equiv.Perm n), 0 ≤ w σ
hw2 : ∑ σ : Equiv.Perm n, w σ = 1
hw3 : ∑ σ : Equiv.Perm n, w σ • Equiv.Perm.permMatrix R σ = M
⊢ M ∈ (convexHull R) {x | ∃ σ, Equiv.Perm.permMatrix R σ = x}

Proof state:
R : Type u_1
n : Type u_2
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : LinearOrderedField R
⊢ {x | ∃ σ, Equiv.Perm.permMatrix R σ = x} ⊆ ↑(doublyStochastic R n)

Tactic:
rintro x ⟨h, rfl⟩

Result:
case intro
R : Type u_1
n : Type u_2
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : LinearOrderedField R
h : Equiv.Perm n
⊢ Equiv.Perm.permMatrix R h ∈ ↑(doublyStochastic R n)

Proof state:
case g1
R : Type u_1
n : Type u_2
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : LinearOrderedField R
⊢ {x | ∃ σ, Equiv.Perm.permMatrix R σ = x} ⊆ ↑(doublyStochastic R n)

case g2
R : Type u_1
n : Type u_2
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : LinearOrderedField R
M : Matrix n n R
hM : M ∈ ↑(doublyStochastic R n)
⊢ M ∈ (convexHull R) {x | ∃ σ, Equiv.Perm.permMatrix R σ = x}

Tactic:
case g1 =>
  rintro x ⟨h, rfl⟩
  exact permMatrix_mem_doublyStochastic

Result:
case g2
R : Type u_1
n : Type u_2
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : LinearOrderedField R
M : Matrix n n R
hM : M ∈ ↑(doublyStochastic R n)
⊢ M ∈ (convexHull R) {x | ∃ σ, Equiv.Perm.permMatrix R σ = x}