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 : 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 : (∀ (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'_1 : 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')
N : Matrix n n R := M - M i ((σ : (a : n) → n) i) • Equiv.Perm.permMatrix R σ
hMi' : 0 < M i ((σ : (a : n) → n) i)
s' : R := s - M i ((σ : (a : n) → n) i)
hs' : 0 ≤ s'
this : ∃ (M' : Matrix n n R), Membership.mem (γ := Submonoid (Matrix n n R)) (doublyStochastic R n) M' ∧ N = s' • M'
⊢ card.{u_2} (α := n × n) {i : n × n | N i.1 i.2 ≠ 0} < d

Tactic:
have hd' : #{i : n × n | N i.1 i.2 ≠ 0} < d := by
    rw [← hd]
    gcongr
    rw [ssubset_iff_of_subset (monotone_filter_right _ _)]
    · simp_rw [mem_filter_univ, not_not, Prod.exists]
      refine ⟨i, σ i, hMi'.ne', ?_⟩
      simp [N, Equiv.toPEquiv_apply]
    · rintro ⟨i', j'⟩ _ hN' hM'
      dsimp at hN' hM'
      simp only [sub_apply, hM', smul_apply, PEquiv.toMatrix_apply, Equiv.toPEquiv_apply,
        Option.mem_def, Option.some.injEq, smul_eq_mul, mul_ite, mul_one, mul_zero, zero_sub,
        neg_eq_zero, ite_eq_right_iff, Classical.not_imp, N] at hN'
      obtain ⟨rfl, _⟩ := hN'
      linarith [hi' i' (by 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
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 : (∀ (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'_1 : 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')
N : Matrix n n R := M - M i ((σ : (a : n) → n) i) • Equiv.Perm.permMatrix R σ
hMi' : 0 < M i ((σ : (a : n) → n) i)
s' : R := s - M i ((σ : (a : n) → n) i)
hs' : 0 ≤ s'
this : ∃ (M' : Matrix n n R), Membership.mem (γ := Submonoid (Matrix n n R)) (doublyStochastic R n) M' ∧ N = s' • M'
hd' : card.{u_2} (α := n × n) {i : n × n | N i.1 i.2 ≠ 0} < d
inr :
  ∀ (w : Equiv.Perm n → R) (hw : ∀ (σ : Equiv.Perm n), 0 ≤ w σ)
    (hw' : ∑ σ : Equiv.Perm n, w σ • Equiv.Perm.permMatrix R σ = 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:
obtain ⟨w, hw, hw'⟩ := ih _ hd' _ s' hs' this rfl

Premises used: 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 : 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 : (∀ (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'_1 : 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')
N : Matrix n n R := M - M i ((σ : (a : n) → n) i) • Equiv.Perm.permMatrix R σ
hMi' : 0 < M i ((σ : (a : n) → n) i)
s' : R := s - M i ((σ : (a : n) → n) i)
hs' : 0 ≤ s'
this : ∃ (M' : Matrix n n R), Membership.mem (γ := Submonoid (Matrix n n R)) (doublyStochastic R n) M' ∧ N = s' • M'
hd' : card.{u_2} (α := n × n) {i : n × n | N i.1 i.2 ≠ 0} < d
w : Equiv.Perm n → R
hw : ∀ (σ : Equiv.Perm n), 0 ≤ w σ
hw' : ∑ σ : Equiv.Perm n, w σ • Equiv.Perm.permMatrix R σ = N
⊢ ∃ (w : Equiv.Perm n → R), (∀ (σ : Equiv.Perm n), 0 ≤ w σ) ∧ ∑ σ : Equiv.Perm n, w σ • Equiv.Perm.permMatrix R σ = M

Tactic:
⟨w + fun σ' => if σ' = σ then M i (σ i) else 0, ?_⟩

Premises used: HAdd.hAdd, Exists.intro, OfNat.ofNat, Eq, DFunLike.coe, ite
-- 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 : (∀ (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'_1 : 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')
N : Matrix n n R := M - M i ((σ : (a : n) → n) i) • Equiv.Perm.permMatrix R σ
hMi' : 0 < M i ((σ : (a : n) → n) i)
s' : R := s - M i ((σ : (a : n) → n) i)
hs' : 0 ≤ s'
this : ∃ (M' : Matrix n n R), Membership.mem (γ := Submonoid (Matrix n n R)) (doublyStochastic R n) M' ∧ N = s' • M'
hd' : card.{u_2} (α := n × n) {i : n × n | N i.1 i.2 ≠ 0} < d
w : Equiv.Perm n → R
hw : ∀ (σ : Equiv.Perm n), 0 ≤ w σ
hw' : ∑ σ : Equiv.Perm n, w σ • Equiv.Perm.permMatrix R σ = N
inr :
  (∀ (σ_1 : Equiv.Perm n),
      0 ≤
        HAdd.hAdd (β := (σ' : Equiv.Perm n) → R) w
          (fun (σ' : Equiv.Perm n) ↦ if σ' = σ then M i ((σ : (a : n) → n) i) else 0) σ_1) ∧
    ∑ σ_1 : Equiv.Perm n,
        HAdd.hAdd (β := (σ' : Equiv.Perm n) → R) w
            (fun (σ' : Equiv.Perm n) ↦ if σ' = σ then M i ((σ : (a : n) → n) i) else 0) σ_1 •
          Equiv.Perm.permMatrix R σ_1 =
      M
⊢ ∃ (w : Equiv.Perm n → R), (∀ (σ : Equiv.Perm n), 0 ≤ w σ) ∧ ∑ σ : Equiv.Perm n, w σ • Equiv.Perm.permMatrix R σ = M

Tactic:
refine ⟨w + fun σ' => if σ' = σ then M i (σ i) else 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
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
hd : card.{u_2} (α := n × n) {i : n × n | M i.1 i.2 ≠ 0} = d
hs'_1 : 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')
N : Matrix n n R := M - M i ((σ : (a : n) → n) i) • Equiv.Perm.permMatrix R σ
hMi' : 0 < M i ((σ : (a : n) → n) i)
s' : R := s - M i ((σ : (a : n) → n) i)
hs' : 0 ≤ s'
this : ∃ (M' : Matrix n n R), Membership.mem (γ := Submonoid (Matrix n n R)) (doublyStochastic R n) M' ∧ N = s' • M'
hd' : card.{u_2} (α := n × n) {i : n × n | N i.1 i.2 ≠ 0} < d
w : Equiv.Perm n → R
hw : ∀ (σ : Equiv.Perm n), 0 ≤ w σ
hw' : ∑ σ : Equiv.Perm n, w σ • Equiv.Perm.permMatrix R σ = N
inr : ∀ (σ_1 : Equiv.Perm n), 0 ≤ w σ_1 + if σ_1 = σ then M i ((σ : (a : n) → n) i) else 0
⊢ (∀ (σ_1 : Equiv.Perm n),
      0 ≤
        HAdd.hAdd (β := (σ' : Equiv.Perm n) → R) w
          (fun (σ' : Equiv.Perm n) ↦ if σ' = σ then M i ((σ : (a : n) → n) i) else 0) σ_1) ∧
    ∑ σ_1 : Equiv.Perm n,
        HAdd.hAdd (β := (σ' : Equiv.Perm n) → R) w
            (fun (σ' : Equiv.Perm n) ↦ if σ' = σ then M i ((σ : (a : n) → n) i) else 0) σ_1 •
          Equiv.Perm.permMatrix R σ_1 =
      M

Tactic:
simp only [Pi.add_apply, add_smul, sum_add_distrib, hw', ite_smul, zero_smul,
    sum_ite_eq', mem_univ, ↓reduceIte, N, sub_add_cancel, and_true]

Premises used: Finset.mem_univ, and_true, Finset.sum_ite_eq', Finset.sum_add_distrib, Pi.add_apply, zero_smul, add_smul, reduceIte, ite_smul, sub_add_cancel
-- 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 : (∀ (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'_1 : 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')
N : Matrix n n R := M - M i ((σ : (a : n) → n) i) • Equiv.Perm.permMatrix R σ
hMi' : 0 < M i ((σ : (a : n) → n) i)
s' : R := s - M i ((σ : (a : n) → n) i)
hs' : 0 ≤ s'
this : ∃ (M' : Matrix n n R), Membership.mem (γ := Submonoid (Matrix n n R)) (doublyStochastic R n) M' ∧ N = s' • M'
hd' : card.{u_2} (α := n × n) {i : n × n | N i.1 i.2 ≠ 0} < d
w : Equiv.Perm n → R
hw : ∀ (σ : Equiv.Perm n), 0 ≤ w σ
hw' : ∑ σ : Equiv.Perm n, w σ • Equiv.Perm.permMatrix R σ = N
σ' : Equiv.Perm n
inr : σ' = σ → 0 ≤ w σ' + M i ((σ : (a : n) → n) i)
inr₁ : ¬σ' = σ → 0 ≤ w σ' + 0
⊢ 0 ≤ w σ' + if σ' = σ then M i ((σ : (a : n) → n) i) else 0

Tactic:
split
-- 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 : (∀ (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'_1 : 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')
N : Matrix n n R := M - M i ((σ : (a : n) → n) i) • Equiv.Perm.permMatrix R σ
hMi' : 0 < M i ((σ : (a : n) → n) i)
s' : R := s - M i ((σ : (a : n) → n) i)
hs' : 0 ≤ s'
this : ∃ (M' : Matrix n n R), Membership.mem (γ := Submonoid (Matrix n n R)) (doublyStochastic R n) M' ∧ N = s' • M'
hd' : card.{u_2} (α := n × n) {i : n × n | N i.1 i.2 ≠ 0} < d
w : Equiv.Perm n → R
hw : ∀ (σ : Equiv.Perm n), 0 ≤ w σ
hw' : ∑ σ : Equiv.Perm n, w σ • Equiv.Perm.permMatrix R σ = N
σ' : Equiv.Perm n
h_1 : σ' = σ
⊢ 0 ≤ w σ' + M i ((σ : (a : n) → n) i)

Tactic:
simp [add_nonneg, hw, hM.1]

Premises used: add_nonneg, And.left
-- 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 : (∀ (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'_1 : 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')
N : Matrix n n R := M - M i ((σ : (a : n) → n) i) • Equiv.Perm.permMatrix R σ
hMi' : 0 < M i ((σ : (a : n) → n) i)
s' : R := s - M i ((σ : (a : n) → n) i)
hs' : 0 ≤ s'
this : ∃ (M' : Matrix n n R), Membership.mem (γ := Submonoid (Matrix n n R)) (doublyStochastic R n) M' ∧ N = s' • M'
hd' : card.{u_2} (α := n × n) {i : n × n | N i.1 i.2 ≠ 0} < d
w : Equiv.Perm n → R
hw : ∀ (σ : Equiv.Perm n), 0 ≤ w σ
hw' : ∑ σ : Equiv.Perm n, w σ • Equiv.Perm.permMatrix R σ = N
σ' : Equiv.Perm n
h_1 : ¬σ' = σ
⊢ 0 ≤ w σ' + 0

Tactic:
simp [add_nonneg, hw, hM.1]

Premises used: add_nonneg, And.left
-- 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
hM : Membership.mem (γ := Submonoid (Matrix n n R)) (doublyStochastic R n) M
rcases :
  IsEmpty n →
    ∃ (w : Equiv.Perm n → R),
      (∀ (σ : Equiv.Perm n), 0 ≤ w σ) ∧
        Eq.{u_1 + 1} (α := R) (∑ σ : Equiv.Perm n, w σ) 1 ∧ ∑ σ : Equiv.Perm n, w σ • Equiv.Perm.permMatrix R σ = M
inr :
  Nonempty n →
    ∃ (w : Equiv.Perm n → R),
      (∀ (σ : Equiv.Perm n), 0 ≤ w σ) ∧
        Eq.{u_1 + 1} (α := R) (∑ σ : Equiv.Perm n, w σ) 1 ∧ ∑ σ : Equiv.Perm n, w σ • Equiv.Perm.permMatrix R σ = M
⊢ ∃ (w : Equiv.Perm n → R),
    (∀ (σ : Equiv.Perm n), 0 ≤ w σ) ∧
      Eq.{u_1 + 1} (α := R) (∑ σ : Equiv.Perm n, w σ) 1 ∧ ∑ σ : 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
hM : Membership.mem (γ := Submonoid (Matrix n n R)) (doublyStochastic R n) M
h : IsEmpty n
⊢ ∀ (σ : Equiv.Perm n), LE.le.{u_1} (α := R) 0 ((fun (x : Equiv.Perm n) ↦ (1 : R)) σ)

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
hM : Membership.mem (γ := Submonoid (Matrix n n R)) (doublyStochastic R n) M
h : IsEmpty n
⊢ Eq.{u_1 + 1} (α := R) (∑ σ : Equiv.Perm n, (fun (x : Equiv.Perm n) ↦ (1 : R)) σ) 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
hM : Membership.mem (γ := Submonoid (Matrix n n R)) (doublyStochastic R n) M
h : IsEmpty n
⊢ ∃ (w : Equiv.Perm n → R),
    (∀ (σ : Equiv.Perm n), 0 ≤ w σ) ∧
      Eq.{u_1 + 1} (α := R) (∑ σ : Equiv.Perm n, w σ) 1 ∧ ∑ σ : Equiv.Perm n, w σ • Equiv.Perm.permMatrix R σ = M

Tactic:
exact ⟨fun _ => 1, by simp, 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
hM : Membership.mem (γ := Submonoid (Matrix n n R)) (doublyStochastic R n) M
h : IsEmpty n
⊢ ∃ (w : Equiv.Perm n → R),
    (∀ (σ : Equiv.Perm n), 0 ≤ w σ) ∧
      Eq.{u_1 + 1} (α := R) (∑ σ : Equiv.Perm n, w σ) 1 ∧ ∑ σ : Equiv.Perm n, w σ • Equiv.Perm.permMatrix R σ = M

Tactic:
case inl => exact ⟨fun _ => 1, by simp, 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
hM : Membership.mem (γ := Submonoid (Matrix n n R)) (doublyStochastic R n) M
h : Nonempty 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
hM : Membership.mem (γ := Submonoid (Matrix n n R)) (doublyStochastic R n) M
h : Nonempty n
⊢ M = HSMul.hSMul (α := R) 1 M

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
hM : Membership.mem (γ := Submonoid (Matrix n n R)) (doublyStochastic R n) M
h : Nonempty n
inr :
  ∀ (w : Equiv.Perm n → R) (hw1 : ∀ (σ : Equiv.Perm n), 0 ≤ w σ)
    (hw3 : ∑ σ : Equiv.Perm n, w σ • Equiv.Perm.permMatrix R σ = M),
    ∃ (w : Equiv.Perm n → R),
      (∀ (σ : Equiv.Perm n), 0 ≤ w σ) ∧
        Eq.{u_1 + 1} (α := R) (∑ σ : Equiv.Perm n, w σ) 1 ∧ ∑ σ : Equiv.Perm n, w σ • Equiv.Perm.permMatrix R σ = M
⊢ ∃ (w : Equiv.Perm n → R),
    (∀ (σ : Equiv.Perm n), 0 ≤ w σ) ∧
      Eq.{u_1 + 1} (α := R) (∑ σ : Equiv.Perm n, w σ) 1 ∧ ∑ σ : Equiv.Perm n, w σ • Equiv.Perm.permMatrix R σ = M

Tactic:
obtain ⟨w, hw1, hw3⟩ := doublyStochastic_sum_perm_aux M 1 (by simp) ⟨M, hM, by simp⟩

Premises used: _private.0.doublyStochastic_sum_perm_aux, And.intro, Exists.intro, OfNat.ofNat
-- 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
hM : Membership.mem (γ := Submonoid (Matrix n n R)) (doublyStochastic R n) M
h : Nonempty n
w : Equiv.Perm n → R
hw1 : ∀ (σ : Equiv.Perm n), 0 ≤ w σ
hw3 : ∑ σ : Equiv.Perm n, w σ • Equiv.Perm.permMatrix R σ = M
⊢ ∃ (w : Equiv.Perm n → R),
    (∀ (σ : Equiv.Perm n), 0 ≤ w σ) ∧
      Eq.{u_1 + 1} (α := R) (∑ σ : Equiv.Perm n, w σ) 1 ∧ ∑ σ : Equiv.Perm n, w σ • Equiv.Perm.permMatrix R σ = M

Tactic:
⟨w, hw1, ?_, hw3⟩

Premises used: And.intro, 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 : Field R
inst_3 : LinearOrder R
inst_4 : IsStrictOrderedRing R
M : Matrix n n R
hM : Membership.mem (γ := Submonoid (Matrix n n R)) (doublyStochastic R n) M
h : Nonempty n
w : Equiv.Perm n → R
hw1 : ∀ (σ : Equiv.Perm n), 0 ≤ w σ
hw3 : ∑ σ : Equiv.Perm n, w σ • Equiv.Perm.permMatrix R σ = M
inr : Eq.{u_1 + 1} (α := R) (∑ σ : Equiv.Perm n, w σ) 1
⊢ ∃ (w : Equiv.Perm n → R),
    (∀ (σ : Equiv.Perm n), 0 ≤ w σ) ∧
      Eq.{u_1 + 1} (α := R) (∑ σ : Equiv.Perm n, w σ) 1 ∧ ∑ σ : Equiv.Perm n, w σ • Equiv.Perm.permMatrix R σ = M

Tactic:
refine ⟨w, hw1, ?_, hw3⟩
-- 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
hM : Membership.mem (γ := Submonoid (Matrix n n R)) (doublyStochastic R n) M
h : Nonempty n
w : Equiv.Perm n → R
hw1 : ∀ (σ : Equiv.Perm n), 0 ≤ w σ
hw3 : ∑ σ : Equiv.Perm n, w σ • Equiv.Perm.permMatrix R σ = M
inr : ∀ (inhabited_h : Inhabited n), Eq.{u_1 + 1} (α := R) (∑ σ : Equiv.Perm n, w σ) 1
⊢ Eq.{u_1 + 1} (α := R) (∑ σ : Equiv.Perm n, w σ) 1

Tactic:
inhabit n
-- 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
hM : Membership.mem (γ := Submonoid (Matrix n n R)) (doublyStochastic R n) M
h : Nonempty n
w : Equiv.Perm n → R
hw1 : ∀ (σ : Equiv.Perm n), 0 ≤ w σ
hw3 : ∑ σ : Equiv.Perm n, w σ • Equiv.Perm.permMatrix R σ = M
inhabited_h : Inhabited n
simp : Eq.{u_1 + 1} (α := R) (∑ x : n, M default x) 1
⊢ Eq.{u_1 + 1} (α := R) (∑ j : n, ∑ σ : Equiv.Perm n, w σ • Equiv.Perm.permMatrix R σ default j) 1

Tactic:
simp only [← smul_apply (m := n), ← Finset.sum_apply, hw3]

Premises used: Finset.sum_apply, Matrix.smul_apply
-- 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
hM : Membership.mem (γ := Submonoid (Matrix n n R)) (doublyStochastic R n) M
h : Nonempty n
w : Equiv.Perm n → R
hw1 : ∀ (σ : Equiv.Perm n), 0 ≤ w σ
hw3 : ∑ σ : Equiv.Perm n, w σ • Equiv.Perm.permMatrix R σ = M
inhabited_h : Inhabited n
rw rw₁ : Eq.{u_1 + 1} (α := R) 1 1
⊢ Eq.{u_1 + 1} (α := R) (∑ x : n, M default x) 1

Tactic:
rw [sum_row_of_mem_doublyStochastic hM]

Premises used: sum_row_of_mem_doublyStochastic
-- 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
hM : Membership.mem (γ := Submonoid (Matrix n n R)) (doublyStochastic R n) M
h : Nonempty n
w : Equiv.Perm n → R
hw1 : ∀ (σ : Equiv.Perm n), 0 ≤ w σ
hw3 : ∑ σ : Equiv.Perm n, w σ • Equiv.Perm.permMatrix R σ = M
inhabited_h : Inhabited n
⊢ Eq.{u_1 + 1} (α := R) (∑ j : n, ∑ σ : Equiv.Perm n, w σ • Equiv.Perm.permMatrix R σ default j) 1

Tactic:
have : ∑ j, ∑ σ : Equiv.Perm n, w σ • σ.permMatrix R default j = 1 := by
    simp only [← smul_apply (m := n), ← Finset.sum_apply, hw3]
    rw [sum_row_of_mem_doublyStochastic 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
M : Matrix n n R
hM : Membership.mem (γ := Submonoid (Matrix n n R)) (doublyStochastic R n) M
h : Nonempty n
w : Equiv.Perm n → R
hw1 : ∀ (σ : Equiv.Perm n), 0 ≤ w σ
hw3 : ∑ σ : Equiv.Perm n, w σ • Equiv.Perm.permMatrix R σ = M
inhabited_h : Inhabited n
this : Eq.{u_1 + 1} (α := R) (∑ j : n, ∑ σ : Equiv.Perm n, w σ • Equiv.Perm.permMatrix R σ default j) 1
⊢ Eq.{u_1 + 1} (α := R) (∑ σ : Equiv.Perm n, w σ) 1

Tactic:
simpa [sum_comm (γ := n), Equiv.toPEquiv_apply] using this

Premises used: Equiv.toPEquiv_apply, Finset.sum_comm