-- Mathlib/Analysis/Convex/Birkhoff.lean
/--
If M is a positive scalar multiple of a doubly stochastic matrix, then there is a permutation matrix
whose support is contained in the support of M.
-/
private lemma exists_perm_eq_zero_implies_eq_zero [Nonempty n] {s : R} (hs : 0 < s)
    (hM : ∃ M' ∈ doublyStochastic R n, M = s • M') :
    ∃ σ : Equiv.Perm n, ∀ i j, M i j = 0 → σ.permMatrix R i j = 0

Proof state:
R : Type u_1
n : Type u_2
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : LinearOrderedSemifield R
M : Matrix n n R
inst✝ : Nonempty n
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
f : n → Finset n := fun i => filter (fun j => M i j ≠ 0) univ
A : Finset n
this : ∀ (i : n), ∑ j ∈ f i, M i j = s
h₁ : ∑ i ∈ A, ∑ j ∈ f i, M i j = ↑(#A) * s
h₂ : ∑ i : n, ∑ j ∈ A.biUnion f, M i j = ↑(#(A.biUnion f)) * s
⊢ #A ≤ #(A.biUnion f)

Tactic:
suffices #A * s ≤ #(A.biUnion f) * s by exact_mod_cast le_of_mul_le_mul_right this hs

Result:
R : Type u_1
n : Type u_2
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : LinearOrderedSemifield R
M : Matrix n n R
inst✝ : Nonempty n
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
f : n → Finset n := fun i => filter (fun j => M i j ≠ 0) univ
A : Finset n
this : ∀ (i : n), ∑ j ∈ f i, M i j = s
h₁ : ∑ i ∈ A, ∑ j ∈ f i, M i j = ↑(#A) * s
h₂ : ∑ i : n, ∑ j ∈ A.biUnion f, M i j = ↑(#(A.biUnion f)) * s
⊢ ↑(#A) * s ≤ ↑(#(A.biUnion f)) * 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
inst✝ : Nonempty n
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
f : n → Finset n := fun i => filter (fun j => M i j ≠ 0) univ
A : Finset n
this : ∀ (i : n), ∑ j ∈ f i, M i j = s
h₁ : ∑ i ∈ A, ∑ j ∈ f i, M i j = ↑(#A) * s
h₂ : ∑ i : n, ∑ j ∈ A.biUnion f, M i j = ↑(#(A.biUnion f)) * s
⊢ ∑ i ∈ A, ∑ j ∈ A.biUnion f, M i j ≤ ∑ i : n, ∑ j ∈ A.biUnion f, M i j

Tactic:
exact sum_le_sum_of_subset_of_nonneg (by simp) fun _ _ _ => sum_nonneg fun j _ => hM.1 _ _

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
inst✝ : Nonempty n
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
⊢ ∃ σ, ∀ (i j : n), M i j = 0 → Equiv.Perm.permMatrix R σ i j = 0

Tactic:
let f (i : n) : Finset n := {j | M i j ≠ 0}

Result:
R : Type u_1
n : Type u_2
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : LinearOrderedSemifield R
M : Matrix n n R
inst✝ : Nonempty n
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
f : n → Finset n := fun i => filter (fun j => M i j ≠ 0) univ
⊢ ∃ σ, ∀ (i j : n), M i j = 0 → Equiv.Perm.permMatrix R σ i j = 0

Proof state:
R : Type u_1
n : Type u_2
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : LinearOrderedSemifield R
M : Matrix n n R
inst✝ : Nonempty n
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
f : n → Finset n := fun i => filter (fun j => M i j ≠ 0) univ
A : Finset n
this : ∀ (i : n), ∑ j ∈ f i, M i j = s
h₁ : ∑ i ∈ A, ∑ j ∈ f i, M i j = ↑(#A) * s
h₂ : ∑ i : n, ∑ j ∈ A.biUnion f, M i j = ↑(#(A.biUnion f)) * s
i : n
hi : i ∈ A
⊢ ∑ j ∈ f i, M i j ≤ ∑ j ∈ A.biUnion f, M i j

Tactic:
exact sum_le_sum_of_subset_of_nonneg (subset_biUnion_of_mem f hi) (by simp [*])

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
inst✝ : Nonempty n
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
f : n → Finset n := fun i => filter (fun j => M i j ≠ 0) univ
A : Finset n
this : ∀ (i : n), ∑ j ∈ f i, M i j = s
h₁ : ∑ i ∈ A, ∑ j ∈ f i, M i j = ↑(#A) * s
h₂ : ∑ i : n, ∑ j ∈ A.biUnion f, M i j = ↑(#(A.biUnion f)) * s
i : n
hi : i ∈ A
⊢ ∀ i_1 ∈ A.biUnion f, i_1 ∉ f i → 0 ≤ M i i_1

Tactic:
simp [*]

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
inst✝ : Nonempty n
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
f : n → Finset n := fun i => filter (fun j => M i j ≠ 0) univ
A : Finset n
this : ∀ (i : n), ∑ j ∈ f i, M i j = s
h₁ : ∑ i ∈ A, ∑ j ∈ f i, M i j = ↑(#A) * s
⊢ ∑ i : n, ∑ j ∈ A.biUnion f, M i j = ↑(#(A.biUnion f)) * s

Tactic:
simp [sum_comm (t := A.biUnion f), hM.2.2, mul_comm s]

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
inst✝ : Nonempty n
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
f : n → Finset n := fun i => filter (fun j => M i j ≠ 0) univ
A : Finset n
this : ∀ (i : n), ∑ j ∈ f i, M i j = s
h₁ : ∑ i ∈ A, ∑ j ∈ f i, M i j = ↑(#A) * s
h₂ : ∑ i : n, ∑ j ∈ A.biUnion f, M i j = ↑(#(A.biUnion f)) * s
⊢ ∑ i ∈ A, ∑ j ∈ f i, M i j ≤ ∑ i ∈ A, ∑ j ∈ A.biUnion f, M i j

Tactic:
refine sum_le_sum fun i hi => ?_

Result:
R : Type u_1
n : Type u_2
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : LinearOrderedSemifield R
M : Matrix n n R
inst✝ : Nonempty n
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
f : n → Finset n := fun i => filter (fun j => M i j ≠ 0) univ
A : Finset n
this : ∀ (i : n), ∑ j ∈ f i, M i j = s
h₁ : ∑ i ∈ A, ∑ j ∈ f i, M i j = ↑(#A) * s
h₂ : ∑ i : n, ∑ j ∈ A.biUnion f, M i j = ↑(#(A.biUnion f)) * s
i : n
hi : i ∈ A
⊢ ∑ j ∈ f i, M i j ≤ ∑ j ∈ A.biUnion f, M i j

Proof state:
R : Type u_1
n : Type u_2
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : LinearOrderedSemifield R
M : Matrix n n R
inst✝ : Nonempty n
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
f : n → Finset n := fun i => filter (fun j => M i j ≠ 0) univ
A : Finset n
this✝ : ∀ (i : n), ∑ j ∈ f i, M i j = s
h₁ : ∑ i ∈ A, ∑ j ∈ f i, M i j = ↑(#A) * s
h₂ : ∑ i : n, ∑ j ∈ A.biUnion f, M i j = ↑(#(A.biUnion f)) * s
this : ↑(#A) * s ≤ ↑(#(A.biUnion f)) * s
⊢ #A ≤ #(A.biUnion f)

Tactic:
exact_mod_cast le_of_mul_le_mul_right this hs

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
inst✝ : Nonempty n
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
f : n → Finset n := fun i => filter (fun j => M i j ≠ 0) univ
A : Finset n
this : ∀ (i : n), ∑ j ∈ f i, M i j = s
⊢ ∑ i ∈ A, ∑ j ∈ f i, M i j = ↑(#A) * s

Tactic:
simp [this]

Result:
no goals