-- Mathlib/Analysis/Convex/Birkhoff.lean
/--
If M is a scalar multiple of a doubly stochastic matrix, then it is a conical combination of
permutation matrices. This is most useful when M is a doubly stochastic matrix, in which case
the combination is convex.

This particular formulation is chosen to make the inductive step easier: we no longer need to
rescale each time a permutation matrix is subtracted.
-/
private lemma doublyStochastic_sum_perm_aux (M : Matrix n n R)
    (s : R) (hs : 0 ≤ s)
    (hM : ∃ M' ∈ doublyStochastic R n, M = s • M') :
    ∃ w : Equiv.Perm n → R, (∀ σ, 0 ≤ w σ) ∧ ∑ σ, w σ • σ.permMatrix R = M

Proof state:
case isTrue
R : Type u_1
n : Type u_2
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : LinearOrderedField R
h✝¹ : Nonempty n
d : ℕ
ih :
  ∀ m < d,
    ∀ (M : Matrix n n R) (s : R),
      0 ≤ s →
        (∃ M' ∈ doublyStochastic R n, M = s • M') →
          #(filter (fun i => M i.1 i.2 ≠ 0) univ) = m →
            ∃ w, (∀ (σ : Equiv.Perm n), 0 ≤ w σ) ∧ ∑ σ : Equiv.Perm n, 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 : n, M i j = s) ∧ ∀ (j : n), ∑ i : n, M i j = s
hd : #(filter (fun i => M i.1 i.2 ≠ 0) univ) = 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'
i' j : n
h✝ : σ i' = j
⊢ M i (σ i) ≤ M i' j

case isFalse
R : Type u_1
n : Type u_2
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : LinearOrderedField R
h✝¹ : Nonempty n
d : ℕ
ih :
  ∀ m < d,
    ∀ (M : Matrix n n R) (s : R),
      0 ≤ s →
        (∃ M' ∈ doublyStochastic R n, M = s • M') →
          #(filter (fun i => M i.1 i.2 ≠ 0) univ) = m →
            ∃ w, (∀ (σ : Equiv.Perm n), 0 ≤ w σ) ∧ ∑ σ : Equiv.Perm n, 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 : n, M i j = s) ∧ ∀ (j : n), ∑ i : n, M i j = s
hd : #(filter (fun i => M i.1 i.2 ≠ 0) univ) = 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'
i' j : n
h✝ : ¬σ i' = j
⊢ 0 ≤ M i' j

Tactic:
case isTrue h => exact (hi' i' (by simp)).trans_eq (by rw [h])

Result:
case isFalse
R : Type u_1
n : Type u_2
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : LinearOrderedField R
h✝¹ : Nonempty n
d : ℕ
ih :
  ∀ m < d,
    ∀ (M : Matrix n n R) (s : R),
      0 ≤ s →
        (∃ M' ∈ doublyStochastic R n, M = s • M') →
          #(filter (fun i => M i.1 i.2 ≠ 0) univ) = m →
            ∃ w, (∀ (σ : Equiv.Perm n), 0 ≤ w σ) ∧ ∑ σ : Equiv.Perm n, 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 : n, M i j = s) ∧ ∀ (j : n), ∑ i : n, M i j = s
hd : #(filter (fun i => M i.1 i.2 ≠ 0) univ) = 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'
i' j : n
h✝ : ¬σ i' = j
⊢ 0 ≤ M i' j

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

Tactic:
case inl => exact ⟨1, 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
s : R
hs : 0 ≤ s
hM : ∃ M' ∈ doublyStochastic R n, M = s • M'
h✝ : Nonempty n
⊢ ∃ w, (∀ (σ : Equiv.Perm n), 0 ≤ w σ) ∧ ∑ σ : Equiv.Perm n, w σ • Equiv.Perm.permMatrix R σ = M

Proof state:
case inr.intro.intro.intro
R : Type u_1
n : Type u_2
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : LinearOrderedField R
h✝ : Nonempty n
d : ℕ
ih :
  ∀ m < d,
    ∀ (M : Matrix n n R) (s : R),
      0 ≤ s →
        (∃ M' ∈ doublyStochastic R n, M = s • M') →
          #(filter (fun i => M i.1 i.2 ≠ 0) univ) = m →
            ∃ w, (∀ (σ : Equiv.Perm n), 0 ≤ w σ) ∧ ∑ σ : Equiv.Perm n, 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 : n, M i j = s) ∧ ∀ (j : n), ∑ i : n, M i j = s
hd : #(filter (fun i => M i.1 i.2 ≠ 0) univ) = 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')
⊢ ∃ w, (∀ (σ : Equiv.Perm n), 0 ≤ w σ) ∧ ∑ σ : Equiv.Perm n, w σ • Equiv.Perm.permMatrix R σ = M

Tactic:
let N : Matrix n n R := M - M i (σ i) • σ.permMatrix R

Result:
case inr.intro.intro.intro
R : Type u_1
n : Type u_2
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : LinearOrderedField R
h✝ : Nonempty n
d : ℕ
ih :
  ∀ m < d,
    ∀ (M : Matrix n n R) (s : R),
      0 ≤ s →
        (∃ M' ∈ doublyStochastic R n, M = s • M') →
          #(filter (fun i => M i.1 i.2 ≠ 0) univ) = m →
            ∃ w, (∀ (σ : Equiv.Perm n), 0 ≤ w σ) ∧ ∑ σ : Equiv.Perm n, 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 : n, M i j = s) ∧ ∀ (j : n), ∑ i : n, M i j = s
hd : #(filter (fun i => M i.1 i.2 ≠ 0) univ) = 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 σ
⊢ ∃ w, (∀ (σ : Equiv.Perm n), 0 ≤ w σ) ∧ ∑ σ : Equiv.Perm n, w σ • Equiv.Perm.permMatrix R σ = M