awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Convex.Birkhoff (goal)
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
⊢ ∃ (w : Equiv.Perm n → R), (∀ (σ : Equiv.Perm n), 0 ≤ w σ) ∧ ∑ σ : Equiv.Perm n, w σ • Equiv.Perm.permMatrix R σ = M
have 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
Tactic: clear_value d
Cleared hypotheses: d, hd
-- Lean 4 proof step from Mathlib.Analysis.Convex.Birkhoff (goal)
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
⊢ ∃ (w : Equiv.Perm n → R), (∀ (σ : Equiv.Perm n), 0 ≤ w σ) ∧ ∑ σ : Equiv.Perm n, w σ • Equiv.Perm.permMatrix R σ = M
have 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
Tactic: induction d using Nat.strongRecOn generalizing M s
Cleared hypotheses: M, s, hs, hM, d, hd
-- Lean 4 proof step from Mathlib.Analysis.Convex.Birkhoff (goal)
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
⊢ ∃ (w : Equiv.Perm n → R), (∀ (σ : Equiv.Perm n), 0 ≤ w σ) ∧ ∑ σ : Equiv.Perm n, w σ • Equiv.Perm.permMatrix R σ = M
have 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
Tactic: rcases eq_or_lt_of_le hs with rfl | hs'
Cleared hypotheses: s, hs, hM
-- Lean 4 proof step from Mathlib.Analysis.Convex.Birkhoff (goal)
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
⊢ ∃ (w : Equiv.Perm n → R), (∀ (σ : Equiv.Perm n), 0 ≤ w σ) ∧ ∑ σ : Equiv.Perm n, w σ • Equiv.Perm.permMatrix R σ = M
have inr : ∀ (hs' : 0 < s),
  ∃ (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'
-- Lean 4 proof step from Mathlib.Analysis.Convex.Birkhoff (goal)
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
have h : (∀ (σ : Equiv.Perm n), LE.le.{u_1} (α := R) 0 (0 σ)) ∧
  ∑ σ : Equiv.Perm n, HSMul.hSMul (α := R) (0 σ) (Equiv.Perm.permMatrix R σ) = M
Tactic: use 0
-- Lean 4 proof step from Mathlib.Analysis.Convex.Birkhoff (hypothesis)
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'
⊢ (∀ (σ : Equiv.Perm n), LE.le.{u_1} (α := R) 0 (0 σ)) ∧
    ∑ σ : Equiv.Perm n, HSMul.hSMul (α := R) (0 σ) (Equiv.Perm.permMatrix R σ) = M
have hM₁ : (∃ (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
Cleared hypotheses: hM
-- Lean 4 proof step from Mathlib.Analysis.Convex.Birkhoff (goal)
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
⊢ ∃ (w : Equiv.Perm n → R), (∀ (σ : Equiv.Perm n), 0 ≤ w σ) ∧ ∑ σ : Equiv.Perm n, w σ • Equiv.Perm.permMatrix R σ = M
have 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
Tactic: obtain ⟨σ, hσ⟩ := exists_perm_eq_zero_implies_eq_zero hs' hM
-- Lean 4 proof step from Mathlib.Analysis.Convex.Birkhoff (goal)
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
⊢ ∃ (w : Equiv.Perm n → R), (∀ (σ : Equiv.Perm n), 0 ≤ w σ) ∧ ∑ σ : Equiv.Perm n, w σ • Equiv.Perm.permMatrix R σ = M
have 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
Tactic: obtain ⟨i, hi, hi'⟩ := exists_min_image _ (fun i => M i (σ i)) univ_nonempty
-- Lean 4 proof step from Mathlib.Analysis.Convex.Birkhoff (goal)
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')
⊢ ∃ (w : Equiv.Perm n → R), (∀ (σ : Equiv.Perm n), 0 ≤ w σ) ∧ ∑ σ : Equiv.Perm n, w σ • Equiv.Perm.permMatrix R σ = M
have 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
Tactic: rw [exists_mem_doublyStochastic_eq_smul_iff hs] at hM
Cleared hypotheses: hM, hd, hs', σ, hσ, i, hi, hi'
-- Lean 4 proof step from Mathlib.Analysis.Convex.Birkhoff (hypothesis)
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' : 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 σ
⊢ ∃ (w : Equiv.Perm n → R), (∀ (σ : Equiv.Perm n), 0 ≤ w σ) ∧ ∑ σ : Equiv.Perm n, w σ • Equiv.Perm.permMatrix R σ = M
have hMi' : 0 < M i ((σ : (a : n) → n) i)
Tactic: have hMi' : 0 < M i (σ i) := (hM.1 _ _).lt_of_ne' fun h => by
    simpa [Equiv.toPEquiv_apply] using hσ _ _ h
-- Lean 4 proof step from Mathlib.Analysis.Convex.Birkhoff (goal)
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' : 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)
⊢ 0 ≤ s'
have simp : M i ((σ : (a : n) → n) i) ≤ ∑ j : n, M i j
Tactic: simp only [s', sub_nonneg, ← hM.2.1 i]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Birkhoff (hypothesis)
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' : 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)
⊢ ∃ (w : Equiv.Perm n → R), (∀ (σ : Equiv.Perm n), 0 ≤ w σ) ∧ ∑ σ : Equiv.Perm n, w σ • Equiv.Perm.permMatrix R σ = M
have hs'₁ : 0 ≤ s'
Tactic: have hs' : 0 ≤ s' := by
    simp only [s', sub_nonneg, ← hM.2.1 i]
    exact single_le_sum (fun j _ => hM.1 i j) (by simp)
-- Lean 4 proof step from Mathlib.Analysis.Convex.Birkhoff (goal)
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'
⊢ ∃ (M' : Matrix n n R), Membership.mem (γ := Submonoid (Matrix n n R)) (doublyStochastic R n) M' ∧ N = s' • M'
have rw : (∀ (i j : n), 0 ≤ N i j) ∧ (∀ (i : n), ∑ j : n, N i j = s') ∧ ∀ (j : n), ∑ i : n, N i j = s'
Tactic: rw [exists_mem_doublyStochastic_eq_smul_iff hs']
-- Lean 4 proof step from Mathlib.Analysis.Convex.Birkhoff (goal)
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'
⊢ (∀ (i j : n), 0 ≤ N i j) ∧ (∀ (i : n), ∑ j : n, N i j = s') ∧ ∀ (j : n), ∑ i : n, N i j = s'
have simp : (∀ (i_1 j : n), (if (σ : (a : n) → n) i_1 = j then M i ((σ : (a : n) → n) i) else 0) ≤ M i_1 j) ∧
  (∀ (i_1 : n), ∑ x : n, M i_1 x - M i ((σ : (a : n) → n) i) = s') ∧
    ∀ (j : n),
      HSub.hSub (α := R) (∑ x : n, M x j) (∑ x : n, if (σ : (a : n) → n) x = j then M i ((σ : (a : n) → n) i) else 0) =
        s'
Tactic: simp only [sub_apply, smul_apply, PEquiv.toMatrix_apply, Equiv.toPEquiv_apply, Option.mem_def,
      Option.some.injEq, smul_eq_mul, mul_ite, mul_one, mul_zero, sub_nonneg,
      sum_sub_distrib, sum_ite_eq, mem_univ, ↓reduceIte, N]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Birkhoff (goal)
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'
⊢ (∀ (i_1 j : n), (if (σ : (a : n) → n) i_1 = j then M i ((σ : (a : n) → n) i) else 0) ≤ M i_1 j) ∧
    (∀ (i_1 : n), ∑ x : n, M i_1 x - M i ((σ : (a : n) → n) i) = s') ∧
      ∀ (j : n),
        HSub.hSub (α := R) (∑ x : n, M x j)
            (∑ x : n, if (σ : (a : n) → n) x = j then M i ((σ : (a : n) → n) i) else 0) =
          s'
have refine : ∀ (i' j : n), (if (σ : (a : n) → n) i' = j then M i ((σ : (a : n) → n) i) else 0) ≤ M i' j
Tactic: refine ⟨fun i' j => ?_, by simp [s', hM.2.1], by simp [s', ← σ.eq_symm_apply, hM]⟩
-- Lean 4 proof step from Mathlib.Analysis.Convex.Birkhoff (goal)
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'
i' j : n
⊢ (if (σ : (a : n) → n) i' = j then M i ((σ : (a : n) → n) i) else 0) ≤ M i' j
have isTrue : (σ : (a : n) → n) i' = j → M i ((σ : (a : n) → n) i) ≤ M i' j
Tactic: split
-- Lean 4 proof step from Mathlib.Analysis.Convex.Birkhoff (goal)
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'
i' j : n
isTrue : (σ : (a : n) → n) i' = j → M i ((σ : (a : n) → n) i) ≤ M i' j
⊢ (if (σ : (a : n) → n) i' = j then M i ((σ : (a : n) → n) i) else 0) ≤ M i' j
have isFalse : ¬(σ : (a : n) → n) i' = j → 0 ≤ M i' j
Tactic: split