-- 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) * s ≤ ↑(#(A.biUnion f)) * s

Tactic:
rw [← h₁, ← h₂]

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 ∈ A, ∑ j ∈ f i, M i j ≤ ∑ i : n, ∑ 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
⊢ ∑ i ∈ A, ∑ j ∈ f i, M i j ≤ ∑ i : n, ∑ j ∈ A.biUnion f, M i j

Tactic:
trans ∑ i ∈ A, ∑ j ∈ A.biUnion f, M i j

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 ∈ A, ∑ j ∈ f i, M i j ≤ ∑ i ∈ A, ∑ j ∈ A.biUnion f, M i j

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

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 ⊆ univ

Tactic:
simp

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
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
hf : ∀ (A : Finset n), #A ≤ #(A.biUnion f)
g : n → n
hg : Bijective g
hg' : ∀ (x : n), g x ∈ f x
i j : n
hij : M i j = 0
⊢ Equiv.Perm.permMatrix R (Equiv.ofBijective g hg) i j = 0

Tactic:
simp only [PEquiv.toMatrix_apply, Option.mem_def, ite_eq_right_iff, one_ne_zero, imp_false,
  Equiv.toPEquiv_apply, Equiv.ofBijective_apply, Option.some.injEq]

Result:
case intro.intro
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
hf : ∀ (A : Finset n), #A ≤ #(A.biUnion f)
g : n → n
hg : Bijective g
hg' : ∀ (x : n), g x ∈ f x
i j : n
hij : M i j = 0
⊢ ¬g i = j

Proof state:
case intro.intro
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
hf : ∀ (A : Finset n), #A ≤ #(A.biUnion f)
g : n → n
hg : Injective g
hg' : ∀ (x : n), g x ∈ f x
⊢ ∃ σ, ∀ (i j : n), M i j = 0 → Equiv.Perm.permMatrix R σ i j = 0

Tactic:
rw [Finite.injective_iff_bijective] at hg

Result:
case intro.intro
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
hf : ∀ (A : Finset n), #A ≤ #(A.biUnion f)
g : n → n
hg : Bijective g
hg' : ∀ (x : n), g x ∈ f x
⊢ ∃ σ, ∀ (i j : n), M i j = 0 → Equiv.Perm.permMatrix R σ i j = 0