-- Mathlib/Analysis/Convex/Birkhoff.lean
/--
If M is a doubly stochastic matrix, then it is an convex combination of permutation matrices. Note
`doublyStochastic_eq_convexHull_permMatrix` shows `doublyStochastic n` is exactly the convex hull of
the permutation matrices, and this lemma is instead most useful for accessing the coefficients of
each permutation matrices directly.
-/
lemma exists_eq_sum_perm_of_mem_doublyStochastic (hM : M ∈ doublyStochastic R n) :
    ∃ w : Equiv.Perm n → R, (∀ σ, 0 ≤ w σ) ∧ ∑ σ, w σ = 1 ∧ ∑ σ, w σ • σ.permMatrix R = M

Proof state:
case inl
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
h✝ : IsEmpty n
⊢ ∃ w,
    (∀ (σ : Equiv.Perm n), 0 ≤ w σ) ∧
      ∑ σ : Equiv.Perm n, w σ = 1 ∧ ∑ σ : Equiv.Perm n, w σ • Equiv.Perm.permMatrix R σ = M

case inr
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
h✝ : Nonempty n
⊢ ∃ w,
    (∀ (σ : Equiv.Perm n), 0 ≤ w σ) ∧
      ∑ σ : Equiv.Perm n, w σ = 1 ∧ ∑ σ : Equiv.Perm n, w σ • Equiv.Perm.permMatrix R σ = M

Tactic:
case inl => exact ⟨fun _ => 1, by simp, by simp, Subsingleton.elim _ _⟩

Result:
case inr
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
h✝ : Nonempty n
⊢ ∃ w,
    (∀ (σ : Equiv.Perm n), 0 ≤ w σ) ∧
      ∑ σ : Equiv.Perm n, w σ = 1 ∧ ∑ σ : Equiv.Perm n, w σ • Equiv.Perm.permMatrix R σ = M

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), 0 ≤ w σ) ∧
      ∑ σ : Equiv.Perm n, w σ = 1 ∧ ∑ σ : Equiv.Perm n, w σ • Equiv.Perm.permMatrix R σ = M

Tactic:
rcases isEmpty_or_nonempty n

Result:
case inl
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
h✝ : IsEmpty n
⊢ ∃ w,
    (∀ (σ : Equiv.Perm n), 0 ≤ w σ) ∧
      ∑ σ : Equiv.Perm n, w σ = 1 ∧ ∑ σ : Equiv.Perm n, w σ • Equiv.Perm.permMatrix R σ = M

case inr
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
h✝ : Nonempty n
⊢ ∃ w,
    (∀ (σ : Equiv.Perm n), 0 ≤ w σ) ∧
      ∑ σ : Equiv.Perm n, w σ = 1 ∧ ∑ σ : Equiv.Perm n, w σ • Equiv.Perm.permMatrix R σ = M

Proof state:
case inr.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
h✝ : Nonempty n
w : Equiv.Perm n → R
hw1 : ∀ (σ : Equiv.Perm n), 0 ≤ w σ
hw3 : ∑ σ : Equiv.Perm n, w σ • Equiv.Perm.permMatrix R σ = M
inhabited_h : Inhabited n
this : ∑ j : n, ∑ σ : Equiv.Perm n, w σ • Equiv.Perm.permMatrix R σ default j = 1
⊢ ∑ σ : Equiv.Perm n, w σ = 1

Tactic:
simpa [sum_comm (γ := n), Equiv.toPEquiv_apply] using this

Result:
no goals

Proof state:
case inr.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
h✝ : Nonempty n
w : Equiv.Perm n → R
hw1 : ∀ (σ : Equiv.Perm n), 0 ≤ w σ
hw3 : ∑ σ : Equiv.Perm n, w σ • Equiv.Perm.permMatrix R σ = M
⊢ ∃ w,
    (∀ (σ : Equiv.Perm n), 0 ≤ w σ) ∧
      ∑ σ : Equiv.Perm n, w σ = 1 ∧ ∑ σ : Equiv.Perm n, w σ • Equiv.Perm.permMatrix R σ = M

Tactic:
refine ⟨w, hw1, ?_, hw3⟩

Result:
case inr.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
h✝ : Nonempty n
w : Equiv.Perm n → R
hw1 : ∀ (σ : Equiv.Perm n), 0 ≤ w σ
hw3 : ∑ σ : Equiv.Perm n, w σ • Equiv.Perm.permMatrix R σ = M
⊢ ∑ σ : Equiv.Perm n, w σ = 1

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
h✝ : Nonempty n
w : Equiv.Perm n → R
hw1 : ∀ (σ : Equiv.Perm n), 0 ≤ w σ
hw3 : ∑ σ : Equiv.Perm n, w σ • Equiv.Perm.permMatrix R σ = M
inhabited_h : Inhabited n
⊢ ∑ j : n, ∑ σ : Equiv.Perm n, w σ • Equiv.Perm.permMatrix R σ default j = 1

Tactic:
simp only [← smul_apply (m := n), ← Finset.sum_apply, hw3]

Result:
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
h✝ : Nonempty n
w : Equiv.Perm n → R
hw1 : ∀ (σ : Equiv.Perm n), 0 ≤ w σ
hw3 : ∑ σ : Equiv.Perm n, w σ • Equiv.Perm.permMatrix R σ = M
inhabited_h : Inhabited n
⊢ ∑ x : n, M default x = 1

Proof state:
case inr.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
h✝ : Nonempty n
w : Equiv.Perm n → R
hw1 : ∀ (σ : Equiv.Perm n), 0 ≤ w σ
hw3 : ∑ σ : Equiv.Perm n, w σ • Equiv.Perm.permMatrix R σ = M
inhabited_h : Inhabited n
⊢ ∑ σ : Equiv.Perm n, w σ = 1

Tactic:
have : ∑ j, ∑ σ : Equiv.Perm n, w σ • σ.permMatrix R default j = 1 := by
  simp only [← smul_apply (m := n), ← Finset.sum_apply, hw3]
  rw [sum_row_of_mem_doublyStochastic hM]

Result:
case inr.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
h✝ : Nonempty n
w : Equiv.Perm n → R
hw1 : ∀ (σ : Equiv.Perm n), 0 ≤ w σ
hw3 : ∑ σ : Equiv.Perm n, w σ • Equiv.Perm.permMatrix R σ = M
inhabited_h : Inhabited n
this : ∑ j : n, ∑ σ : Equiv.Perm n, w σ • Equiv.Perm.permMatrix R σ default j = 1
⊢ ∑ σ : Equiv.Perm n, w σ = 1

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
h✝ : Nonempty n
⊢ M = 1 • M

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
h✝ : IsEmpty n
⊢ ∃ w,
    (∀ (σ : Equiv.Perm n), 0 ≤ w σ) ∧
      ∑ σ : Equiv.Perm n, w σ = 1 ∧ ∑ σ : Equiv.Perm n, w σ • Equiv.Perm.permMatrix R σ = M

Tactic:
exact ⟨fun _ => 1, by simp, by simp, Subsingleton.elim _ _⟩

Result:
no goals

Proof state:
case inr
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
h✝ : Nonempty n
⊢ ∃ w,
    (∀ (σ : Equiv.Perm n), 0 ≤ w σ) ∧
      ∑ σ : Equiv.Perm n, w σ = 1 ∧ ∑ σ : Equiv.Perm n, w σ • Equiv.Perm.permMatrix R σ = M

Tactic:
obtain ⟨w, hw1, hw3⟩ := doublyStochastic_sum_perm_aux M 1 (by simp) ⟨M, hM, by simp⟩

Result:
case inr.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
h✝ : Nonempty n
w : Equiv.Perm n → R
hw1 : ∀ (σ : Equiv.Perm n), 0 ≤ w σ
hw3 : ∑ σ : Equiv.Perm n, w σ • Equiv.Perm.permMatrix R σ = M
⊢ ∃ w,
    (∀ (σ : Equiv.Perm n), 0 ≤ w σ) ∧
      ∑ σ : Equiv.Perm n, w σ = 1 ∧ ∑ σ : Equiv.Perm n, w σ • Equiv.Perm.permMatrix R σ = M

Proof state:
case inr.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
h✝ : Nonempty n
w : Equiv.Perm n → R
hw1 : ∀ (σ : Equiv.Perm n), 0 ≤ w σ
hw3 : ∑ σ : Equiv.Perm n, w σ • Equiv.Perm.permMatrix R σ = M
⊢ ∑ σ : Equiv.Perm n, w σ = 1

Tactic:
inhabit n

Result:
case inr.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
h✝ : Nonempty n
w : Equiv.Perm n → R
hw1 : ∀ (σ : Equiv.Perm n), 0 ≤ w σ
hw3 : ∑ σ : Equiv.Perm n, w σ • Equiv.Perm.permMatrix R σ = M
inhabited_h : Inhabited n
⊢ ∑ σ : Equiv.Perm n, w σ = 1