-- 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:
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'
this : ∃ M' ∈ doublyStochastic R n, N = s' • M'
⊢ #(filter (fun i => N i.1 i.2 ≠ 0) univ) < #(filter (fun i => M i.1 i.2 ≠ 0) univ)

Tactic:
refine card_lt_card ?_

Result:
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'
this : ∃ M' ∈ doublyStochastic R n, N = s' • M'
⊢ filter (fun i => N i.1 i.2 ≠ 0) univ ⊂ filter (fun i => M i.1 i.2 ≠ 0) univ

Proof state:
case h
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
hd : #(filter (fun i => M i.1 i.2 ≠ 0) univ) = d
hs : 0 ≤ 0
hM : (∃ x, x ∈ doublyStochastic R n) ∧ M = 0
⊢ (∀ (σ : Equiv.Perm n), 0 ≤ 0 σ) ∧ ∑ σ : Equiv.Perm n, 0 σ • Equiv.Perm.permMatrix R σ = M

Tactic:
simp [hM]

Result:
no goals

Proof state:
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

Tactic:
rw [h]

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
s : R
hs : 0 ≤ s
hM : ∃ M' ∈ doublyStochastic R n, M = s • M'
h✝ : Nonempty n
d : ℕ := #(filter (fun i => M i.1 i.2 ≠ 0) univ)
hd : #(filter (fun i => M i.1 i.2 ≠ 0) univ) = d
⊢ ∃ w, (∀ (σ : Equiv.Perm n), 0 ≤ w σ) ∧ ∑ σ : Equiv.Perm n, w σ • Equiv.Perm.permMatrix R σ = M

Tactic:
clear_value d

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
d : ℕ
hd : #(filter (fun i => M i.1 i.2 ≠ 0) univ) = d
⊢ ∃ w, (∀ (σ : Equiv.Perm n), 0 ≤ w σ) ∧ ∑ σ : Equiv.Perm n, w σ • Equiv.Perm.permMatrix R σ = M

Proof state:
case inr
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 : ∃ M' ∈ doublyStochastic R n, M = s • M'
hd : #(filter (fun i => M i.1 i.2 ≠ 0) univ) = d
hs' : 0 < s
⊢ ∃ w, (∀ (σ : Equiv.Perm n), 0 ≤ w σ) ∧ ∑ σ : Equiv.Perm n, w σ • Equiv.Perm.permMatrix R σ = M

Tactic:
obtain ⟨σ, hσ⟩ := exists_perm_eq_zero_implies_eq_zero hs' hM

Result:
case inr.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 : ∃ M' ∈ doublyStochastic R n, M = s • M'
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
⊢ ∃ w, (∀ (σ : Equiv.Perm n), 0 ≤ w σ) ∧ ∑ σ : 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
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'
this : ∃ M' ∈ doublyStochastic R n, N = s' • M'
i' : n
right✝ : ¬M i (σ i) = 0
hM' : M i' (σ i') = 0
⊢ i' ∈ univ

Tactic:
simp

Result:
no goals