-- Mathlib/Data/Matrix/DoublyStochastic.lean
/--
A matrix is `s` times a doubly stochastic matrix iff all entries are nonnegative, and all row and
column sums are equal to `s`.

This lemma is useful for the proof of Birkhoff's theorem - in particular because it allows scaling
by nonnegative factors rather than positive ones only.
-/
lemma exists_mem_doublyStochastic_eq_smul_iff {M : Matrix n n R} {s : R} (hs : 0 ≤ s) :
    (∃ M' ∈ doublyStochastic R n, M = s • M') ↔
      (∀ i j, 0 ≤ M i j) ∧ (∀ i, ∑ j, M i j = s) ∧ (∀ j, ∑ i, M i j = s)

Proof state:
case mpr
R : Type u_1
n : Type u_2
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : LinearOrderedSemifield R
M : Matrix n n R
s : R
hs : 0 ≤ s
⊢ ((∀ (i j : n), 0 ≤ M i j) ∧ (∀ (i : n), ∑ j : n, M i j = s) ∧ ∀ (j : n), ∑ i : n, M i j = s) →
    ∃ M' ∈ doublyStochastic R n, M = s • M'

Tactic:
rcases eq_or_lt_of_le hs with rfl | hs

Result:
case mpr.inl
R : Type u_1
n : Type u_2
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : LinearOrderedSemifield R
M : Matrix n n R
hs : 0 ≤ 0
⊢ ((∀ (i j : n), 0 ≤ M i j) ∧ (∀ (i : n), ∑ j : n, M i j = 0) ∧ ∀ (j : n), ∑ i : n, M i j = 0) →
    ∃ M' ∈ doublyStochastic R n, M = 0 • M'

case mpr.inr
R : Type u_1
n : Type u_2
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : LinearOrderedSemifield R
M : Matrix n n R
s : R
hs✝ : 0 ≤ s
hs : 0 < s
⊢ ((∀ (i j : n), 0 ≤ M i j) ∧ (∀ (i : n), ∑ j : n, M i j = s) ∧ ∀ (j : n), ∑ i : n, M i j = s) →
    ∃ M' ∈ doublyStochastic R n, M = s • M'

Proof state:
case mpr.inr
R : Type u_1
n : Type u_2
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : LinearOrderedSemifield R
M : Matrix n n R
s : R
hs✝ : 0 ≤ s
hs : 0 < s
⊢ ((∀ (i j : n), 0 ≤ M i j) ∧ (∀ (i : n), ∑ j : n, M i j = s) ∧ ∀ (j : n), ∑ i : n, M i j = s) →
    ∃ M' ∈ doublyStochastic R n, M = s • M'

Tactic:
rintro ⟨hM₁, hM₂, hM₃⟩

Result:
case mpr.inr.intro.intro
R : Type u_1
n : Type u_2
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : LinearOrderedSemifield R
M : Matrix n n R
s : R
hs✝ : 0 ≤ s
hs : 0 < s
hM₁ : ∀ (i j : n), 0 ≤ M i j
hM₂ : ∀ (i : n), ∑ j : n, M i j = s
hM₃ : ∀ (j : n), ∑ i : n, M i j = s
⊢ ∃ M' ∈ doublyStochastic R n, M = s • M'

Proof state:
case mpr.inr.intro.intro
R : Type u_1
n : Type u_2
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : LinearOrderedSemifield R
M : Matrix n n R
s : R
hs✝ : 0 ≤ s
hs : 0 < s
hM₁ : ∀ (i j : n), 0 ≤ M i j
hM₂ : ∀ (i : n), ∑ j : n, M i j = s
hM₃ : ∀ (j : n), ∑ i : n, M i j = s
⊢ ∃ M' ∈ doublyStochastic R n, M = s • M'

Tactic:
exact ⟨s⁻¹ • M, by simp [mem_doublyStochastic_iff_sum, ← mul_sum, hs.ne', inv_mul_cancel₀, *]⟩

Result:
no goals

Proof state:
R : Type u_1
n : Type u_2
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : LinearOrderedSemifield R
M : Matrix n n R
hs : 0 ≤ 0
⊢ ((∀ (i j : n), 0 ≤ M i j) ∧ (∀ (i : n), ∑ j : n, M i j = 0) ∧ ∀ (j : n), ∑ i : n, M i j = 0) →
    ∃ M' ∈ doublyStochastic R n, M = 0 • M'

Tactic:
simp only [zero_smul, exists_and_right, and_imp]

Result:
R : Type u_1
n : Type u_2
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : LinearOrderedSemifield R
M : Matrix n n R
hs : 0 ≤ 0
⊢ (∀ (i j : n), 0 ≤ M i j) →
    (∀ (i : n), ∑ j : n, M i j = 0) → (∀ (j : n), ∑ i : n, M i j = 0) → (∃ x, x ∈ doublyStochastic R n) ∧ M = 0

Proof state:
case a
R : Type u_1
n : Type u_2
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : LinearOrderedSemifield R
M : Matrix n n R
hs : 0 ≤ 0
h₁ : ∀ (i j : n), 0 ≤ M i j
a✝ : ∀ (j : n), ∑ i : n, M i j = 0
i j : n
h₂ : ∑ j : n, M i j = 0
⊢ M i j = 0 i j

Tactic:
rw [sum_eq_zero_iff_of_nonneg (by simp [h₁ i])] at h₂

Result:
case a
R : Type u_1
n : Type u_2
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : LinearOrderedSemifield R
M : Matrix n n R
hs : 0 ≤ 0
h₁ : ∀ (i j : n), 0 ≤ M i j
a✝ : ∀ (j : n), ∑ i : n, M i j = 0
i j : n
h₂ : ∀ i_1 ∈ univ, M i i_1 = 0
⊢ M i j = 0 i j

Proof state:
case intro.intro
R : Type u_1
n : Type u_2
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : LinearOrderedSemifield R
s : R
hs : 0 ≤ s
M' : Matrix n n R
hM' : (∀ (i j : n), 0 ≤ M' i j) ∧ (∀ (i : n), ∑ j : n, M' i j = 1) ∧ ∀ (j : n), ∑ i : n, M' i j = 1
⊢ (∀ (i j : n), 0 ≤ (s • M') i j) ∧ (∀ (i : n), ∑ j : n, (s • M') i j = s) ∧ ∀ (j : n), ∑ i : n, (s • M') i j = s

Tactic:
simp only [smul_apply, smul_eq_mul, ← mul_sum]

Result:
case intro.intro
R : Type u_1
n : Type u_2
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : LinearOrderedSemifield R
s : R
hs : 0 ≤ s
M' : Matrix n n R
hM' : (∀ (i j : n), 0 ≤ M' i j) ∧ (∀ (i : n), ∑ j : n, M' i j = 1) ∧ ∀ (j : n), ∑ i : n, M' i j = 1
⊢ (∀ (i j : n), 0 ≤ s * M' i j) ∧ (∀ (i : n), s * ∑ i_1 : n, M' i i_1 = s) ∧ ∀ (j : n), s * ∑ i : n, M' i j = s

Proof state:
case mpr.inl
R : Type u_1
n : Type u_2
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : LinearOrderedSemifield R
M : Matrix n n R
hs : 0 ≤ 0
⊢ ((∀ (i j : n), 0 ≤ M i j) ∧ (∀ (i : n), ∑ j : n, M i j = 0) ∧ ∀ (j : n), ∑ i : n, M i j = 0) →
    ∃ M' ∈ doublyStochastic R n, M = 0 • M'

case mpr.inr
R : Type u_1
n : Type u_2
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : LinearOrderedSemifield R
M : Matrix n n R
s : R
hs✝ : 0 ≤ s
hs : 0 < s
⊢ ((∀ (i j : n), 0 ≤ M i j) ∧ (∀ (i : n), ∑ j : n, M i j = s) ∧ ∀ (j : n), ∑ i : n, M i j = s) →
    ∃ M' ∈ doublyStochastic R n, M = s • M'

Tactic:
case inl =>
  simp only [zero_smul, exists_and_right, and_imp]
  intro h₁ h₂ _
  refine ⟨⟨1, Submonoid.one_mem _⟩, ?_⟩
  ext i j
  specialize h₂ i
  rw [sum_eq_zero_iff_of_nonneg (by simp [h₁ i])] at h₂
  exact h₂ _ (by simp)

Result:
case mpr.inr
R : Type u_1
n : Type u_2
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : LinearOrderedSemifield R
M : Matrix n n R
s : R
hs✝ : 0 ≤ s
hs : 0 < s
⊢ ((∀ (i j : n), 0 ≤ M i j) ∧ (∀ (i : n), ∑ j : n, M i j = s) ∧ ∀ (j : n), ∑ i : n, M i j = s) →
    ∃ M' ∈ doublyStochastic R n, M = s • M'

Proof state:
case intro.intro
R : Type u_1
n : Type u_2
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : LinearOrderedSemifield R
s : R
hs : 0 ≤ s
M' : Matrix n n R
hM' : (∀ (i j : n), 0 ≤ M' i j) ∧ (∀ (i : n), ∑ j : n, M' i j = 1) ∧ ∀ (j : n), ∑ i : n, M' i j = 1
⊢ (∀ (i j : n), 0 ≤ s * M' i j) ∧ (∀ (i : n), s * ∑ i_1 : n, M' i i_1 = s) ∧ ∀ (j : n), s * ∑ i : n, M' i j = s

Tactic:
exact ⟨fun i j => mul_nonneg hs (hM'.1 _ _), by simp [hM']⟩

Result:
no goals

Proof state:
case intro.intro
R : Type u_1
n : Type u_2
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : LinearOrderedSemifield R
s : R
hs : 0 ≤ s
M' : Matrix n n R
hM' : M' ∈ doublyStochastic R n
⊢ (∀ (i j : n), 0 ≤ (s • M') i j) ∧ (∀ (i : n), ∑ j : n, (s • M') i j = s) ∧ ∀ (j : n), ∑ i : n, (s • M') i j = s

Tactic:
rw [mem_doublyStochastic_iff_sum] at hM'

Result:
case intro.intro
R : Type u_1
n : Type u_2
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : LinearOrderedSemifield R
s : R
hs : 0 ≤ s
M' : Matrix n n R
hM' : (∀ (i j : n), 0 ≤ M' i j) ∧ (∀ (i : n), ∑ j : n, M' i j = 1) ∧ ∀ (j : n), ∑ i : n, M' i j = 1
⊢ (∀ (i j : n), 0 ≤ (s • M') i j) ∧ (∀ (i : n), ∑ j : n, (s • M') i j = s) ∧ ∀ (j : n), ∑ i : n, (s • M') i j = s

Proof state:
R : Type u_1
n : Type u_2
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : LinearOrderedSemifield R
M : Matrix n n R
hs : 0 ≤ 0
h₁ : ∀ (i j : n), 0 ≤ M i j
h₂ : ∀ (i : n), ∑ j : n, M i j = 0
a✝ : ∀ (j : n), ∑ i : n, M i j = 0
⊢ M = 0

Tactic:
ext i j

Result:
case a
R : Type u_1
n : Type u_2
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : LinearOrderedSemifield R
M : Matrix n n R
hs : 0 ≤ 0
h₁ : ∀ (i j : n), 0 ≤ M i j
h₂ : ∀ (i : n), ∑ j : n, M i j = 0
a✝ : ∀ (j : n), ∑ i : n, M i j = 0
i j : n
⊢ M i j = 0 i j