awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Convex.Birkhoff
Goal:
R : Type u_1
n : Type u_2
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : Semifield R
inst_3 : LinearOrder R
inst_4 : IsStrictOrderedRing R
M : Matrix n n R
inst_5 : 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 : (i : n) → Finset n := fun (i : n) ↦ {j : n | M i j ≠ 0}
A : Finset n
this : ∀ (i : n), ∑ j ∈ f i, M i j = s
h₁ : ∑ i ∈ A, ∑ j ∈ f i, M i j = (↑(#A) : R) * s
h₂ : ∑ i : n, ∑ j ∈ A.biUnion f, M i j = (↑(#(A.biUnion f)) : R) * s
i : n
hi : i ∈ A
⊢ LE.le.{u_1} (α := R) (∑ 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 [*])

Premises used: Finset.subset_biUnion_of_mem, Finset.sum_le_sum_of_subset_of_nonneg
-- Module: Mathlib.Analysis.Convex.Birkhoff
Goal:
R : Type u_1
n : Type u_2
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : Semifield R
inst_3 : LinearOrder R
inst_4 : IsStrictOrderedRing R
M : Matrix n n R
inst_5 : 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 : (i : n) → Finset n := fun (i : n) ↦ {j : n | M i j ≠ 0}
A : Finset n
this : ∀ (i : n), ∑ j ∈ f i, M i j = s
h₁ : ∑ i ∈ A, ∑ j ∈ f i, M i j = (↑(#A) : R) * s
h₂ : ∑ i : n, ∑ j ∈ A.biUnion f, M i j = (↑(#(A.biUnion f)) : R) * s
⊢ A ⊆ univ

Tactic:
simp
-- Module: Mathlib.Analysis.Convex.Birkhoff
Goal:
R : Type u_1
n : Type u_2
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : Semifield R
inst_3 : LinearOrder R
inst_4 : IsStrictOrderedRing R
M : Matrix n n R
inst_5 : 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 : (i : n) → Finset n := fun (i : n) ↦ {j : n | M i j ≠ 0}
A : Finset n
this : ∀ (i : n), ∑ j ∈ f i, M i j = s
h₁ : ∑ i ∈ A, ∑ j ∈ f i, M i j = (↑(#A) : R) * s
h₂ : ∑ i : n, ∑ j ∈ A.biUnion f, M i j = (↑(#(A.biUnion f)) : R) * s
⊢ LE.le.{u_1} (α := R) (∑ 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 _ _

Premises used: Finset.sum_nonneg, And.left, Finset.sum_le_sum_of_subset_of_nonneg
-- Module: Mathlib.Analysis.Convex.Birkhoff
Goal:
R : Type u_1
n : Type u_2
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : Semifield R
inst_3 : LinearOrder R
inst_4 : IsStrictOrderedRing R
M : Matrix n n R
inst_5 : 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 : (i : n) → Finset n := fun (i : n) ↦ {j : n | M i j ≠ 0}
⊢ ∀ (A : Finset n), #A ≤ #(A.biUnion f)

Tactic:
have hf (A : Finset n) : #A ≤ #(A.biUnion f) := by
    have (i : _) : ∑ j ∈ f i, M i j = s := by simp [f, sum_subset (filter_subset _ _), hM.2.1]
    have h₁ : ∑ i ∈ A, ∑ j ∈ f i, M i j = #A * s := by simp [this]
    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]
    suffices #A * s ≤ #(A.biUnion f) * s by exact_mod_cast le_of_mul_le_mul_right this hs
    rw [← h₁, ← h₂]
    trans ∑ i ∈ A, ∑ j ∈ A.biUnion f, M i j
    · refine sum_le_sum fun i hi => ?_
      exact sum_le_sum_of_subset_of_nonneg (subset_biUnion_of_mem f hi) (by simp [*])
    · exact sum_le_sum_of_subset_of_nonneg (by simp) fun _ _ _ => sum_nonneg fun j _ => hM.1 _ _
-- Module: Mathlib.Analysis.Convex.Birkhoff
Goal:
R : Type u_1
n : Type u_2
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : Semifield R
inst_3 : LinearOrder R
inst_4 : IsStrictOrderedRing R
M : Matrix n n R
inst_5 : 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 : (i : n) → Finset n := fun (i : n) ↦ {j : n | M i j ≠ 0}
hf : ∀ (A : Finset n), #A ≤ #(A.biUnion f)
obtain :
  ∀ (g : n → n) (hg : Injective g) (hg' : ∀ (x : n), g x ∈ f x),
    ∃ (σ : Equiv.Perm n), ∀ (i j : n), M i j = 0 → Equiv.Perm.permMatrix R σ i j = 0
⊢ ∃ (σ : Equiv.Perm n), ∀ (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

Premises used: Finset.all_card_le_biUnion_card_iff_exists_injective, Iff.mp
-- Module: Mathlib.Analysis.Convex.Birkhoff
Goal:
R : Type u_1
n : Type u_2
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : Semifield R
inst_3 : LinearOrder R
inst_4 : IsStrictOrderedRing R
M : Matrix n n R
inst_5 : 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 : (i : n) → Finset n := fun (i : n) ↦ {j : n | M i j ≠ 0}
hf : ∀ (A : Finset n), #A ≤ #(A.biUnion f)
g : n → n
hg : Injective g
hg' : ∀ (x : n), g x ∈ f x
⊢ Bijective g

Tactic:
rw [Finite.injective_iff_bijective] at hg

Premises used: Finite.injective_iff_bijective
-- Module: Mathlib.Analysis.Convex.Birkhoff
Goal:
R : Type u_1
n : Type u_2
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : Semifield R
inst_3 : LinearOrder R
inst_4 : IsStrictOrderedRing R
M : Matrix n n R
inst_5 : 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 : (i : n) → Finset n := fun (i : n) ↦ {j : n | M i j ≠ 0}
hf : ∀ (A : Finset n), #A ≤ #(A.biUnion f)
g : n → n
hg : Injective g
hg' : ∀ (x : n), g x ∈ f x
hg₁ : Bijective g
⊢ ∀ (x : n), g x ∈ f x

Tactic:
rw [Finite.injective_iff_bijective] at hg

Premises used: Finite.injective_iff_bijective
-- Module: Mathlib.Analysis.Convex.Birkhoff
Goal:
R : Type u_1
n : Type u_2
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : Semifield R
inst_3 : LinearOrder R
inst_4 : IsStrictOrderedRing R
M : Matrix n n R
inst_5 : 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 : (i : n) → Finset n := fun (i : n) ↦ {j : n | M i j ≠ 0}
hf : ∀ (A : Finset n), #A ≤ #(A.biUnion f)
g : n → n
hg : Bijective g
hg' : ∀ (x : n), g x ∈ f x
⊢ ∃ (σ : Equiv.Perm n), ∀ (i j : n), M i j = 0 → Equiv.Perm.permMatrix R σ i j = 0

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

Premises used: Equiv.ofBijective, Exists.intro
-- Module: Mathlib.Analysis.Convex.Birkhoff
Goal:
R : Type u_1
n : Type u_2
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : Semifield R
inst_3 : LinearOrder R
inst_4 : IsStrictOrderedRing R
M : Matrix n n R
inst_5 : 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 : (i : n) → Finset n := fun (i : n) ↦ {j : n | M i j ≠ 0}
hf : ∀ (A : Finset n), #A ≤ #(A.biUnion f)
g : n → n
hg : Bijective g
hg' : ∀ (x : n), g x ∈ f x
refine : ∀ (i j : n) (hij : M i j = 0), Equiv.Perm.permMatrix R (Equiv.ofBijective g hg) i j = 0
⊢ ∃ (σ : Equiv.Perm n), ∀ (i j : n), M i j = 0 → Equiv.Perm.permMatrix R σ i j = 0

Tactic:
refine ⟨Equiv.ofBijective g hg, fun i j hij => ?_⟩
-- Module: Mathlib.Analysis.Convex.Birkhoff
Goal:
R : Type u_1
n : Type u_2
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : Semifield R
inst_3 : LinearOrder R
inst_4 : IsStrictOrderedRing R
M : Matrix n n R
inst_5 : 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 : (i : n) → Finset n := fun (i : n) ↦ {j : n | M i j ≠ 0}
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
simp : ¬g i = j
⊢ 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]

Premises used: Equiv.toPEquiv_apply, imp_false, Option.some.injEq, Equiv.ofBijective_apply, ite_eq_right_iff, PEquiv.toMatrix_apply, one_ne_zero, Option.mem_def
-- Module: Mathlib.Analysis.Convex.Birkhoff
Goal:
R : Type u_1
n : Type u_2
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : Semifield R
inst_3 : LinearOrder R
inst_4 : IsStrictOrderedRing R
M : Matrix n n R
inst_5 : 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 : (i : n) → Finset n := fun (i : n) ↦ {j : n | M i j ≠ 0}
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
-- Module: Mathlib.Analysis.Convex.Birkhoff
Goal:
R : Type u_1
n : Type u_2
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : Field R
inst_3 : LinearOrder R
inst_4 : IsStrictOrderedRing R
M : Matrix n n R
s : R
hs : 0 ≤ s
hM : ∃ (M' : Matrix n n R), Membership.mem (γ := Submonoid (Matrix n n R)) (doublyStochastic R n) M' ∧ M = s • M'
rcases :
  IsEmpty n →
    ∃ (w : Equiv.Perm n → R), (∀ (σ : Equiv.Perm n), 0 ≤ w σ) ∧ ∑ σ : Equiv.Perm n, w σ • Equiv.Perm.permMatrix R σ = M
inr :
  Nonempty n →
    ∃ (w : Equiv.Perm n → R), (∀ (σ : Equiv.Perm n), 0 ≤ w σ) ∧ ∑ σ : Equiv.Perm n, w σ • Equiv.Perm.permMatrix R σ = M
⊢ ∃ (w : Equiv.Perm n → R), (∀ (σ : Equiv.Perm n), 0 ≤ w σ) ∧ ∑ σ : Equiv.Perm n, w σ • Equiv.Perm.permMatrix R σ = M

Tactic:
rcases isEmpty_or_nonempty n

Premises used: isEmpty_or_nonempty
-- Module: Mathlib.Analysis.Convex.Birkhoff
Goal:
R : Type u_1
n : Type u_2
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : Field R
inst_3 : LinearOrder R
inst_4 : IsStrictOrderedRing R
M : Matrix n n R
s : R
hs : 0 ≤ s
hM : ∃ (M' : Matrix n n R), Membership.mem (γ := Submonoid (Matrix n n R)) (doublyStochastic R n) M' ∧ M = s • M'
h : IsEmpty n
⊢ ∀ (σ : Equiv.Perm n), LE.le.{u_1} (α := R) 0 (1 σ)

Tactic:
simp
-- Module: Mathlib.Analysis.Convex.Birkhoff
Goal:
R : Type u_1
n : Type u_2
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : Field R
inst_3 : LinearOrder R
inst_4 : IsStrictOrderedRing R
M : Matrix n n R
s : R
hs : 0 ≤ s
hM : ∃ (M' : Matrix n n R), Membership.mem (γ := Submonoid (Matrix n n R)) (doublyStochastic R n) M' ∧ M = s • M'
h : IsEmpty n
⊢ ∃ (w : Equiv.Perm n → R), (∀ (σ : Equiv.Perm n), 0 ≤ w σ) ∧ ∑ σ : Equiv.Perm n, w σ • Equiv.Perm.permMatrix R σ = M

Tactic:
exact ⟨1, by simp, Subsingleton.elim _ _⟩
-- Module: Mathlib.Analysis.Convex.Birkhoff
Goal:
R : Type u_1
n : Type u_2
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : Field R
inst_3 : LinearOrder R
inst_4 : IsStrictOrderedRing R
M : Matrix n n R
s : R
hs : 0 ≤ s
hM : ∃ (M' : Matrix n n R), Membership.mem (γ := Submonoid (Matrix n n R)) (doublyStochastic R n) M' ∧ M = s • M'
h : IsEmpty n
⊢ ∃ (w : Equiv.Perm n → R), (∀ (σ : Equiv.Perm n), 0 ≤ w σ) ∧ ∑ σ : Equiv.Perm n, w σ • Equiv.Perm.permMatrix R σ = M

Tactic:
case inl => exact ⟨1, by simp, Subsingleton.elim _ _⟩
-- Module: Mathlib.Analysis.Convex.Birkhoff
Goal:
R : Type u_1
n : Type u_2
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : Field R
inst_3 : LinearOrder R
inst_4 : IsStrictOrderedRing R
M : Matrix n n R
s : R
hs : 0 ≤ s
hM : ∃ (M' : Matrix n n R), Membership.mem (γ := Submonoid (Matrix n n R)) (doublyStochastic R n) M' ∧ M = s • M'
h : Nonempty n
⊢ let d := card.{u_2} (α := n × n) {i : n × n | M i.1 i.2 ≠ 0};
  card.{u_2} (α := n × n) {i : n × n | M i.1 i.2 ≠ 0} = d

Tactic:
set d : ℕ := #{i : n × n | M i.1 i.2 ≠ 0} with ← hd
-- Module: Mathlib.Analysis.Convex.Birkhoff
Goal:
R : Type u_1
n : Type u_2
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : Field R
inst_3 : LinearOrder R
inst_4 : IsStrictOrderedRing R
M : Matrix n n R
s : R
hs : 0 ≤ s
hM : ∃ (M' : Matrix n n R), Membership.mem (γ := Submonoid (Matrix n n R)) (doublyStochastic R n) M' ∧ M = s • M'
h : Nonempty n
d : ℕ := card.{u_2} (α := n × n) {i : n × n | M i.1 i.2 ≠ 0}
hd : card.{u_2} (α := n × n) {i : n × n | M i.1 i.2 ≠ 0} = d
inr :
  ∀ (d : ℕ) (hd : card.{u_2} (α := n × n) {i : n × n | M i.1 i.2 ≠ 0} = d),
    ∃ (w : Equiv.Perm n → R), (∀ (σ : Equiv.Perm n), 0 ≤ w σ) ∧ ∑ σ : Equiv.Perm n, w σ • Equiv.Perm.permMatrix R σ = M
⊢ ∃ (w : Equiv.Perm n → R), (∀ (σ : Equiv.Perm n), 0 ≤ w σ) ∧ ∑ σ : Equiv.Perm n, w σ • Equiv.Perm.permMatrix R σ = M

Tactic:
clear_value d
-- Module: Mathlib.Analysis.Convex.Birkhoff
Goal:
R : Type u_1
n : Type u_2
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : Field R
inst_3 : LinearOrder R
inst_4 : IsStrictOrderedRing R
M : Matrix n n R
s : R
hs : 0 ≤ s
hM : ∃ (M' : Matrix n n R), Membership.mem (γ := Submonoid (Matrix n n R)) (doublyStochastic R n) M' ∧ M = s • M'
h : Nonempty n
d : ℕ
hd : card.{u_2} (α := n × n) {i : n × n | M i.1 i.2 ≠ 0} = d
inr :
  ∀ (n_1 : ℕ),
    (∀ m < n_1,
        ∀ (M : Matrix n n R) (s : R) (hs : 0 ≤ s)
          (hM :
            ∃ (M' : Matrix n n R),
              Membership.mem (γ := Submonoid (Matrix n n R)) (doublyStochastic R n) M' ∧ M = s • M')
          (hd : card.{u_2} (α := n × n) {i : n × n | M i.1 i.2 ≠ 0} = m),
          ∃ (w : Equiv.Perm n → R),
            (∀ (σ : 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' : Matrix n n R), Membership.mem (γ := Submonoid (Matrix n n R)) (doublyStochastic R n) M' ∧ M = s • M')
        (hd : card.{u_2} (α := n × n) {i : n × n | M i.1 i.2 ≠ 0} = n_1),
        ∃ (w : Equiv.Perm n → R),
          (∀ (σ : Equiv.Perm n), 0 ≤ w σ) ∧ ∑ σ : Equiv.Perm n, w σ • Equiv.Perm.permMatrix R σ = M
⊢ ∃ (w : Equiv.Perm n → R), (∀ (σ : Equiv.Perm n), 0 ≤ w σ) ∧ ∑ σ : Equiv.Perm n, w σ • Equiv.Perm.permMatrix R σ = M

Tactic:
induction d using Nat.strongRecOn generalizing M s
-- Module: Mathlib.Analysis.Convex.Birkhoff
Goal:
R : Type u_1
n : Type u_2
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : Field R
inst_3 : LinearOrder R
inst_4 : IsStrictOrderedRing R
h : Nonempty n
d : ℕ
ih :
  ∀ m < d,
    ∀ (M : Matrix n n R) (s : R) (hs : 0 ≤ s)
      (hM :
        ∃ (M' : Matrix n n R), Membership.mem (γ := Submonoid (Matrix n n R)) (doublyStochastic R n) M' ∧ M = s • M')
      (hd : card.{u_2} (α := n × n) {i : n × n | M i.1 i.2 ≠ 0} = m),
      ∃ (w : Equiv.Perm n → R),
        (∀ (σ : 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' : Matrix n n R), Membership.mem (γ := Submonoid (Matrix n n R)) (doublyStochastic R n) M' ∧ M = s • M'
hd : card.{u_2} (α := n × n) {i : n × n | M i.1 i.2 ≠ 0} = d
rcases :
  ∀ (hs : LE.le.{u_1} (α := R) 0 0)
    (hM :
      ∃ (M' : Matrix n n R),
        Membership.mem (γ := Submonoid (Matrix n n R)) (doublyStochastic R n) M' ∧ M = HSMul.hSMul (α := R) 0 M'),
    ∃ (w : Equiv.Perm n → R), (∀ (σ : Equiv.Perm n), 0 ≤ w σ) ∧ ∑ σ : Equiv.Perm n, w σ • Equiv.Perm.permMatrix R σ = M
inr :
  ∀ (hs' : 0 < s),
    ∃ (w : Equiv.Perm n → R), (∀ (σ : Equiv.Perm n), 0 ≤ w σ) ∧ ∑ σ : Equiv.Perm n, w σ • Equiv.Perm.permMatrix R σ = M
⊢ ∃ (w : Equiv.Perm n → R), (∀ (σ : Equiv.Perm n), 0 ≤ w σ) ∧ ∑ σ : Equiv.Perm n, w σ • Equiv.Perm.permMatrix R σ = M

Tactic:
rcases eq_or_lt_of_le hs with rfl | hs'

Premises used: eq_or_lt_of_le, rfl
-- Module: Mathlib.Analysis.Convex.Birkhoff
Goal:
R : Type u_1
n : Type u_2
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : Field R
inst_3 : LinearOrder R
inst_4 : IsStrictOrderedRing R
h_1 : Nonempty n
d : ℕ
ih :
  ∀ m < d,
    ∀ (M : Matrix n n R) (s : R) (hs : 0 ≤ s)
      (hM :
        ∃ (M' : Matrix n n R), Membership.mem (γ := Submonoid (Matrix n n R)) (doublyStochastic R n) M' ∧ M = s • M')
      (hd : card.{u_2} (α := n × n) {i : n × n | M i.1 i.2 ≠ 0} = m),
      ∃ (w : Equiv.Perm n → R),
        (∀ (σ : Equiv.Perm n), 0 ≤ w σ) ∧ ∑ σ : Equiv.Perm n, w σ • Equiv.Perm.permMatrix R σ = M
M : Matrix n n R
hd : card.{u_2} (α := n × n) {i : n × n | M i.1 i.2 ≠ 0} = d
hs : LE.le.{u_1} (α := R) 0 0
hM :
  ∃ (M' : Matrix n n R),
    Membership.mem (γ := Submonoid (Matrix n n R)) (doublyStochastic R n) M' ∧ M = HSMul.hSMul (α := R) 0 M'
h :
  (∀ (σ : Equiv.Perm n), LE.le.{u_1} (α := R) 0 (0 σ)) ∧
    ∑ σ : Equiv.Perm n, HSMul.hSMul (α := R) (0 σ) (Equiv.Perm.permMatrix R σ) = M
⊢ ∃ (w : Equiv.Perm n → R), (∀ (σ : Equiv.Perm n), 0 ≤ w σ) ∧ ∑ σ : Equiv.Perm n, w σ • Equiv.Perm.permMatrix R σ = M

Tactic:
use 0
-- Module: Mathlib.Analysis.Convex.Birkhoff
Goal:
R : Type u_1
n : Type u_2
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : Field R
inst_3 : LinearOrder R
inst_4 : IsStrictOrderedRing R
h : Nonempty n
d : ℕ
ih :
  ∀ m < d,
    ∀ (M : Matrix n n R) (s : R) (hs : 0 ≤ s)
      (hM :
        ∃ (M' : Matrix n n R), Membership.mem (γ := Submonoid (Matrix n n R)) (doublyStochastic R n) M' ∧ M = s • M')
      (hd : card.{u_2} (α := n × n) {i : n × n | M i.1 i.2 ≠ 0} = m),
      ∃ (w : Equiv.Perm n → R),
        (∀ (σ : Equiv.Perm n), 0 ≤ w σ) ∧ ∑ σ : Equiv.Perm n, w σ • Equiv.Perm.permMatrix R σ = M
M : Matrix n n R
hd : card.{u_2} (α := n × n) {i : n × n | M i.1 i.2 ≠ 0} = d
hs : LE.le.{u_1} (α := R) 0 0
hM :
  ∃ (M' : Matrix n n R),
    Membership.mem (γ := Submonoid (Matrix n n R)) (doublyStochastic R n) M' ∧ M = HSMul.hSMul (α := R) 0 M'
⊢ (∃ (x : Matrix n n R), Membership.mem (γ := Submonoid (Matrix n n R)) (doublyStochastic R n) x) ∧ M = 0

Tactic:
simp only [zero_smul, exists_and_right] at hM

Premises used: exists_and_right, zero_smul
-- Module: Mathlib.Analysis.Convex.Birkhoff
Goal:
R : Type u_1
n : Type u_2
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : Field R
inst_3 : LinearOrder R
inst_4 : IsStrictOrderedRing R
h : Nonempty n
d : ℕ
ih :
  ∀ m < d,
    ∀ (M : Matrix n n R) (s : R) (hs : 0 ≤ s)
      (hM :
        ∃ (M' : Matrix n n R), Membership.mem (γ := Submonoid (Matrix n n R)) (doublyStochastic R n) M' ∧ M = s • M')
      (hd : card.{u_2} (α := n × n) {i : n × n | M i.1 i.2 ≠ 0} = m),
      ∃ (w : Equiv.Perm n → R),
        (∀ (σ : Equiv.Perm n), 0 ≤ w σ) ∧ ∑ σ : Equiv.Perm n, w σ • Equiv.Perm.permMatrix R σ = M
M : Matrix n n R
hd : card.{u_2} (α := n × n) {i : n × n | M i.1 i.2 ≠ 0} = d
hs : LE.le.{u_1} (α := R) 0 0
hM : (∃ (x : Matrix n n R), Membership.mem (γ := Submonoid (Matrix n n R)) (doublyStochastic R n) x) ∧ M = 0
⊢ (∀ (σ : Equiv.Perm n), LE.le.{u_1} (α := R) 0 (0 σ)) ∧
    ∑ σ : Equiv.Perm n, HSMul.hSMul (α := R) (0 σ) (Equiv.Perm.permMatrix R σ) = M

Tactic:
simp [hM]
-- Module: Mathlib.Analysis.Convex.Birkhoff
Goal:
R : Type u_1
n : Type u_2
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : Field R
inst_3 : LinearOrder R
inst_4 : IsStrictOrderedRing R
h : Nonempty n
d : ℕ
ih :
  ∀ m < d,
    ∀ (M : Matrix n n R) (s : R) (hs : 0 ≤ s)
      (hM :
        ∃ (M' : Matrix n n R), Membership.mem (γ := Submonoid (Matrix n n R)) (doublyStochastic R n) M' ∧ M = s • M')
      (hd : card.{u_2} (α := n × n) {i : n × n | M i.1 i.2 ≠ 0} = m),
      ∃ (w : Equiv.Perm n → R),
        (∀ (σ : Equiv.Perm n), 0 ≤ w σ) ∧ ∑ σ : Equiv.Perm n, w σ • Equiv.Perm.permMatrix R σ = M
M : Matrix n n R
hd : card.{u_2} (α := n × n) {i : n × n | M i.1 i.2 ≠ 0} = d
hs : LE.le.{u_1} (α := R) 0 0
hM :
  ∃ (M' : Matrix n n R),
    Membership.mem (γ := Submonoid (Matrix n n R)) (doublyStochastic R n) M' ∧ M = HSMul.hSMul (α := R) 0 M'
⊢ ∃ (w : Equiv.Perm n → R), (∀ (σ : Equiv.Perm n), 0 ≤ w σ) ∧ ∑ σ : Equiv.Perm n, w σ • Equiv.Perm.permMatrix R σ = M

Tactic:
case inl =>
    use 0
    simp only [zero_smul, exists_and_right] at hM
    simp [hM]

Premises used: exists_and_right, zero_smul
-- Module: Mathlib.Analysis.Convex.Birkhoff
Goal:
R : Type u_1
n : Type u_2
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : Field R
inst_3 : LinearOrder R
inst_4 : IsStrictOrderedRing R
h : Nonempty n
d : ℕ
ih :
  ∀ m < d,
    ∀ (M : Matrix n n R) (s : R) (hs : 0 ≤ s)
      (hM :
        ∃ (M' : Matrix n n R), Membership.mem (γ := Submonoid (Matrix n n R)) (doublyStochastic R n) M' ∧ M = s • M')
      (hd : card.{u_2} (α := n × n) {i : n × n | M i.1 i.2 ≠ 0} = m),
      ∃ (w : Equiv.Perm n → R),
        (∀ (σ : 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' : Matrix n n R), Membership.mem (γ := Submonoid (Matrix n n R)) (doublyStochastic R n) M' ∧ M = s • M'
hd : card.{u_2} (α := n × n) {i : n × n | M i.1 i.2 ≠ 0} = d
hs' : 0 < s
inr :
  ∀ (σ : Equiv.Perm n) (hσ : ∀ (i j : n), M i j = 0 → Equiv.Perm.permMatrix R σ i j = 0),
    ∃ (w : Equiv.Perm n → R), (∀ (σ : Equiv.Perm n), 0 ≤ w σ) ∧ ∑ σ : Equiv.Perm n, w σ • Equiv.Perm.permMatrix R σ = M
⊢ ∃ (w : Equiv.Perm n → R), (∀ (σ : 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

Premises used: _private.0.exists_perm_eq_zero_implies_eq_zero
-- Module: Mathlib.Analysis.Convex.Birkhoff
Goal:
R : Type u_1
n : Type u_2
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : Field R
inst_3 : LinearOrder R
inst_4 : IsStrictOrderedRing R
h : Nonempty n
d : ℕ
ih :
  ∀ m < d,
    ∀ (M : Matrix n n R) (s : R) (hs : 0 ≤ s)
      (hM :
        ∃ (M' : Matrix n n R), Membership.mem (γ := Submonoid (Matrix n n R)) (doublyStochastic R n) M' ∧ M = s • M')
      (hd : card.{u_2} (α := n × n) {i : n × n | M i.1 i.2 ≠ 0} = m),
      ∃ (w : Equiv.Perm n → R),
        (∀ (σ : 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' : Matrix n n R), Membership.mem (γ := Submonoid (Matrix n n R)) (doublyStochastic R n) M' ∧ M = s • M'
hd : card.{u_2} (α := n × n) {i : n × n | M i.1 i.2 ≠ 0} = d
hs' : 0 < s
σ : Equiv.Perm n
hσ : ∀ (i j : n), M i j = 0 → Equiv.Perm.permMatrix R σ i j = 0
inr :
  ∀ (i : n) (hi : Membership.mem (γ := Finset n) univ i)
    (hi' :
      ∀ (x' : n), Membership.mem (γ := Finset n) univ x' → M i ((σ : (a : n) → n) i) ≤ M x' ((σ : (a : n) → n) x')),
    ∃ (w : Equiv.Perm n → R), (∀ (σ : Equiv.Perm n), 0 ≤ w σ) ∧ ∑ σ : Equiv.Perm n, w σ • Equiv.Perm.permMatrix R σ = M
⊢ ∃ (w : Equiv.Perm n → R), (∀ (σ : Equiv.Perm n), 0 ≤ w σ) ∧ ∑ σ : Equiv.Perm n, w σ • Equiv.Perm.permMatrix R σ = M

Tactic:
obtain ⟨i, hi, hi'⟩ := exists_min_image _ (fun i => M i (σ i)) univ_nonempty

Premises used: Finset.univ_nonempty, Finset.exists_min_image, DFunLike.coe
-- Module: Mathlib.Analysis.Convex.Birkhoff
Goal:
R : Type u_1
n : Type u_2
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : Field R
inst_3 : LinearOrder R
inst_4 : IsStrictOrderedRing R
h : Nonempty n
d : ℕ
ih :
  ∀ m < d,
    ∀ (M : Matrix n n R) (s : R) (hs : 0 ≤ s)
      (hM :
        ∃ (M' : Matrix n n R), Membership.mem (γ := Submonoid (Matrix n n R)) (doublyStochastic R n) M' ∧ M = s • M')
      (hd : card.{u_2} (α := n × n) {i : n × n | M i.1 i.2 ≠ 0} = m),
      ∃ (w : Equiv.Perm n → R),
        (∀ (σ : 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' : Matrix n n R), Membership.mem (γ := Submonoid (Matrix n n R)) (doublyStochastic R n) M' ∧ M = s • M'
hd : card.{u_2} (α := n × n) {i : n × n | M i.1 i.2 ≠ 0} = 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 : Membership.mem (γ := Finset n) univ i
hi' : ∀ (x' : n), Membership.mem (γ := Finset n) univ x' → M i ((σ : (a : n) → n) i) ≤ M x' ((σ : (a : n) → n) x')
inr :
  ∀ (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 : card.{u_2} (α := n × n) {i : n × n | M i.1 i.2 ≠ 0} = 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 : Membership.mem (γ := Finset n) univ i)
    (hi' :
      ∀ (x' : n), Membership.mem (γ := Finset n) univ x' → M i ((σ : (a : n) → n) i) ≤ M x' ((σ : (a : n) → n) x')),
    ∃ (w : Equiv.Perm n → R), (∀ (σ : Equiv.Perm n), 0 ≤ w σ) ∧ ∑ σ : Equiv.Perm n, w σ • Equiv.Perm.permMatrix R σ = M
⊢ ∃ (w : Equiv.Perm n → R), (∀ (σ : Equiv.Perm n), 0 ≤ w σ) ∧ ∑ σ : Equiv.Perm n, w σ • Equiv.Perm.permMatrix R σ = M

Tactic:
rw [exists_mem_doublyStochastic_eq_smul_iff hs] at hM

Premises used: exists_mem_doublyStochastic_eq_smul_iff