-- 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
i : n
⊢ ∑ j ∈ f i, M i j = s

Tactic:
simp [f, sum_subset (filter_subset _ _), hM.2.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
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
⊢ #A ≤ #(A.biUnion f)

Tactic:
have h₂ : ∑ i, ∑ j ∈ A.biUnion f, M i j = #(A.biUnion f) * s := by
  simp [sum_comm (t := A.biUnion f), hM.2.2, mul_comm s]

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

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

Tactic:
have (i) : ∑ j ∈ f i, M i j = s := by simp [f, sum_subset (filter_subset _ _), hM.2.1]

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

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 : n
hij : M i (g i) = 0
⊢ False

Tactic:
simpa [f, hij] using hg' i

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

Tactic:
have h₁ : ∑ i ∈ A, ∑ j ∈ f i, M i j = #A * s := by simp [this]

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

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
⊢ ¬g i = j

Tactic:
rintro rfl

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 : n
hij : M i (g i) = 0
⊢ False

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 : ∃ M' ∈ doublyStochastic R n, M = s • M'
⊢ ∃ σ, ∀ (i j : n), M i j = 0 → Equiv.Perm.permMatrix R σ i j = 0

Tactic:
rw [exists_mem_doublyStochastic_eq_smul_iff hs.le] at hM

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
⊢ ∃ σ, ∀ (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
hf : ∀ (A : Finset n), #A ≤ #(A.biUnion f)
⊢ ∃ σ, ∀ (i j : n), M i j = 0 → Equiv.Perm.permMatrix R σ i j = 0

Tactic:
obtain ⟨g, hg, hg'⟩ := (all_card_le_biUnion_card_iff_exists_injective f).1 hf

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 : Injective g
hg' : ∀ (x : n), g x ∈ f x
⊢ ∃ σ, ∀ (i j : n), M i j = 0 → Equiv.Perm.permMatrix R σ i j = 0

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), M i j = 0 → Equiv.Perm.permMatrix R σ i j = 0

Tactic:
refine ⟨Equiv.ofBijective g hg, fun i j hij => ?_⟩

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
⊢ Equiv.Perm.permMatrix R (Equiv.ofBijective g hg) i j = 0