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
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), (∀ (σ : Equiv.Perm n), 0 ≤ w σ) ∧ ∑ σ : Equiv.Perm n, w σ • Equiv.Perm.permMatrix R σ = M
have 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
Tactic: obtain ⟨w, hw, hw'⟩ := ih _ hd' _ s' hs' this rfl
-- 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'
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
have 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
Tactic: refine ⟨w + fun σ' => if σ' = σ then M i (σ i) else 0, ?_⟩
-- 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'
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
⊢ (∀ (σ_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
have inr : ∀ (σ_1 : Equiv.Perm n), 0 ≤ w σ_1 + if σ_1 = σ then M i ((σ : (a : n) → n) i) else 0
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]
-- 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'
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
⊢ 0 ≤ w σ' + if σ' = σ then M i ((σ : (a : n) → n) i) else 0
have inr : σ' = σ → 0 ≤ w σ' + M i ((σ : (a : n) → n) i)
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'
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)
⊢ 0 ≤ w σ' + if σ' = σ then M i ((σ : (a : n) → n) i) else 0
have inr₁ : ¬σ' = σ → 0 ≤ w σ' + 0
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
M : Matrix n n R
hM : Membership.mem (γ := Submonoid (Matrix n n R)) (doublyStochastic R n) 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
have 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
Tactic: rcases isEmpty_or_nonempty 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
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
⊢ ∃ (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
have 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
Tactic: rcases isEmpty_or_nonempty 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
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),
    (∀ (σ : Equiv.Perm n), 0 ≤ w σ) ∧
      Eq.{u_1 + 1} (α := R) (∑ σ : Equiv.Perm n, w σ) 1 ∧ ∑ σ : Equiv.Perm n, w σ • Equiv.Perm.permMatrix R σ = M
have 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
Tactic: obtain ⟨w, hw1, hw3⟩ := doublyStochastic_sum_perm_aux M 1 (by simp) ⟨M, hM, 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
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
have inr : Eq.{u_1 + 1} (α := R) (∑ σ : Equiv.Perm n, w σ) 1
Tactic: refine ⟨w, hw1, ?_, hw3⟩
-- 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
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
⊢ Eq.{u_1 + 1} (α := R) (∑ σ : Equiv.Perm n, w σ) 1
have inr : ∀ (inhabited_h : Inhabited n), Eq.{u_1 + 1} (α := R) (∑ σ : Equiv.Perm n, w σ) 1
Tactic: inhabit 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
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
have simp : Eq.{u_1 + 1} (α := R) (∑ x : n, M default x) 1
Tactic: simp only [← smul_apply (m := n), ← Finset.sum_apply, hw3]
-- 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
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) (∑ x : n, M default x) 1
have rw : Eq.{u_1 + 1} (α := R) 1 1
Tactic: rw [sum_row_of_mem_doublyStochastic hM]
-- 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
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) (∑ σ : Equiv.Perm n, w σ) 1
have this : 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]
-- 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
⊢ (↑(doublyStochastic R n) : Set (Matrix n n R)) =
    (convexHull R : (a : Set (Matrix n n R)) → Set (Matrix n n R))
      {x : Matrix n n R | ∃ (σ : Equiv.Perm n), Equiv.Perm.permMatrix R σ = x}
have refine : {x : Matrix n n R | ∃ (σ : Equiv.Perm n), Equiv.Perm.permMatrix R σ = x} ⊆
  (↑(doublyStochastic R n) : Set (Matrix n n R))
Tactic: refine (convexHull_min ?g1 convex_doublyStochastic).antisymm' fun M hM => ?g2
-- 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
refine :
  {x : Matrix n n R | ∃ (σ : Equiv.Perm n), Equiv.Perm.permMatrix R σ = x} ⊆
    (↑(doublyStochastic R n) : Set (Matrix n n R))
⊢ (↑(doublyStochastic R n) : Set (Matrix n n R)) =
    (convexHull R : (a : Set (Matrix n n R)) → Set (Matrix n n R))
      {x : Matrix n n R | ∃ (σ : Equiv.Perm n), Equiv.Perm.permMatrix R σ = x}
have refine₁ : ∀ (M : Matrix n n R) (hM : M ∈ (↑(doublyStochastic R n) : Set (Matrix n n R))),
  Membership.mem (γ := Set (Matrix n n R))
    ((convexHull R : (a : Set (Matrix n n R)) → Set (Matrix n n R))
        {x : Matrix n n R | ∃ (σ : Equiv.Perm n), Equiv.Perm.permMatrix R σ = x} :
      Set (Matrix n n R))
    M
Tactic: refine (convexHull_min ?g1 convex_doublyStochastic).antisymm' fun M hM => ?g2
-- 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
hM : M ∈ (↑(doublyStochastic R n) : Set (Matrix n n R))
⊢ Membership.mem (γ := Set (Matrix n n R))
    ((convexHull R : (a : Set (Matrix n n R)) → Set (Matrix n n R))
        {x : Matrix n n R | ∃ (σ : Equiv.Perm n), Equiv.Perm.permMatrix R σ = x} :
      Set (Matrix n n R))
    M
have obtain : ∀ (w : Equiv.Perm n → R) (hw1 : ∀ (σ : Equiv.Perm n), 0 ≤ w σ) (hw2 : Eq.{u_1 + 1} (α := R) (∑ σ : Equiv.Perm n, w σ) 1)
  (hw3 : ∑ σ : Equiv.Perm n, w σ • Equiv.Perm.permMatrix R σ = M),
  Membership.mem (γ := Set (Matrix n n R))
    ((convexHull R : (a : Set (Matrix n n R)) → Set (Matrix n n R))
        {x : Matrix n n R | ∃ (σ : Equiv.Perm n), Equiv.Perm.permMatrix R σ = x} :
      Set (Matrix n n R))
    M
Tactic: obtain ⟨w, hw1, hw2, hw3⟩ := exists_eq_sum_perm_of_mem_doublyStochastic 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
M : Matrix n n R
hM : M ∈ (↑(doublyStochastic R n) : Set (Matrix n n R))
⊢ Membership.mem (γ := Set (Matrix n n R))
    ((convexHull R : (a : Set (Matrix n n R)) → Set (Matrix n n R))
        {x : Matrix n n R | ∃ (σ : Equiv.Perm n), Equiv.Perm.permMatrix R σ = x} :
      Set (Matrix n n R))
    M
have case : ∀ (w : Equiv.Perm n → R) (hw1 : ∀ (σ : Equiv.Perm n), 0 ≤ w σ) (hw2 : Eq.{u_1 + 1} (α := R) (∑ σ : Equiv.Perm n, w σ) 1)
  (hw3 : ∑ σ : Equiv.Perm n, w σ • Equiv.Perm.permMatrix R σ = M),
  Membership.mem (γ := Set (Matrix n n R))
    ((convexHull R : (a : Set (Matrix n n R)) → Set (Matrix n n R))
        {x : Matrix n n R | ∃ (σ : Equiv.Perm n), Equiv.Perm.permMatrix R σ = x} :
      Set (Matrix n n R))
    M
Tactic: case g2 =>
    obtain ⟨w, hw1, hw2, hw3⟩ := exists_eq_sum_perm_of_mem_doublyStochastic hM
    exact mem_convexHull_of_exists_fintype w (·.permMatrix R) hw1 hw2 (by simp) hw3
-- 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
⊢ Set.extremePoints R (↑(doublyStochastic R n) : Set (Matrix n n R)) =
    {x : Matrix n n R | ∃ (σ : Equiv.Perm n), Equiv.Perm.permMatrix R σ = x}
have refine_1 : Set.extremePoints R (↑(doublyStochastic R n) : Set (Matrix n n R)) ⊆
  {x : Matrix n n R | ∃ (σ : Equiv.Perm n), Equiv.Perm.permMatrix R σ = x}
Tactic: refine subset_antisymm ?_ ?_
-- 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
refine_1 :
  Set.extremePoints R (↑(doublyStochastic R n) : Set (Matrix n n R)) ⊆
    {x : Matrix n n R | ∃ (σ : Equiv.Perm n), Equiv.Perm.permMatrix R σ = x}
⊢ Set.extremePoints R (↑(doublyStochastic R n) : Set (Matrix n n R)) =
    {x : Matrix n n R | ∃ (σ : Equiv.Perm n), Equiv.Perm.permMatrix R σ = x}
have refine_2 : {x : Matrix n n R | ∃ (σ : Equiv.Perm n), Equiv.Perm.permMatrix R σ = x} ⊆
  Set.extremePoints R (↑(doublyStochastic R n) : Set (Matrix n n R))
Tactic: refine subset_antisymm ?_ ?_
-- 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
⊢ Set.extremePoints R (↑(doublyStochastic R n) : Set (Matrix n n R)) ⊆
    {x : Matrix n n R | ∃ (σ : Equiv.Perm n), Equiv.Perm.permMatrix R σ = x}
have refine_1 : Subset (α := Set (Matrix n n R))
  (Set.extremePoints R
    ((convexHull R : (a : Set (Matrix n n R)) → Set (Matrix n n R))
      {x : Matrix n n R | ∃ (σ : Equiv.Perm n), Equiv.Perm.permMatrix R σ = x}))
  {x : Matrix n n R | ∃ (σ : Equiv.Perm n), Equiv.Perm.permMatrix R σ = x}
Tactic: rw [doublyStochastic_eq_convexHull_permMatrix]
-- 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
σ : Equiv.Perm n
⊢ Equiv.Perm.permMatrix R σ ∈ Set.extremePoints R (↑(doublyStochastic R n) : Set (Matrix n n R))
have refine_2 : ∀ (x₁ : Matrix n n R) (hx₁ : x₁ ∈ (↑(doublyStochastic R n) : Set (Matrix n n R))) (x₂ : Matrix n n R)
  (hx₂ : x₂ ∈ (↑(doublyStochastic R n) : Set (Matrix n n R))) (hσ : Equiv.Perm.permMatrix R σ ∈ openSegment R x₁ x₂),
  x₁ = Equiv.Perm.permMatrix R σ
Tactic: refine ⟨permMatrix_mem_doublyStochastic, fun x₁ hx₁ x₂ hx₂ hσ ↦ ?_⟩
-- 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
σ : Equiv.Perm n
x₁ : Matrix n n R
hx₁ : x₁ ∈ (↑(doublyStochastic R n) : Set (Matrix n n R))
x₂ : Matrix n n R
hx₂ : x₂ ∈ (↑(doublyStochastic R n) : Set (Matrix n n R))
hσ : Equiv.Perm.permMatrix R σ ∈ openSegment R x₁ x₂
this : ∀ (i j : n), x₁ i j = x₂ i j
hx₃ : x₁ ∈ (↑(doublyStochastic R n) : Set (Matrix n n R))
⊢ x₁ = Equiv.Perm.permMatrix R σ
have hσ₁ : Equiv.Perm.permMatrix R σ ∈ openSegment R x₁ x₁
Tactic: obtain rfl : x₁ = x₂ := by simpa [← Matrix.ext_iff]
Cleared hypotheses: x₂, hx₂, hσ, this
-- 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
σ : Equiv.Perm n
x₁ : Matrix n n R
hx₁ : x₁ ∈ (↑(doublyStochastic R n) : Set (Matrix n n R))
x₂ : Matrix n n R
hx₂ : x₂ ∈ (↑(doublyStochastic R n) : Set (Matrix n n R))
hσ : Equiv.Perm.permMatrix R σ ∈ openSegment R x₁ x₂
this : ∀ (i j : n), x₁ i j = x₂ i j
hx₃ : x₁ ∈ (↑(doublyStochastic R n) : Set (Matrix n n R))
hσ₁ : Equiv.Perm.permMatrix R σ ∈ openSegment R x₁ x₁
⊢ x₁ = Equiv.Perm.permMatrix R σ
have this₁ : ∀ (i j : n), x₁ i j = x₁ i j
Tactic: obtain rfl : x₁ = x₂ := by simpa [← Matrix.ext_iff]
Cleared hypotheses: x₂, hx₂, hσ, this
-- 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
σ : Equiv.Perm n
x₁ : Matrix n n R
hx₁ : x₁ ∈ (↑(doublyStochastic R n) : Set (Matrix n n R))
x₂ : Matrix n n R
hx₂ : x₂ ∈ (↑(doublyStochastic R n) : Set (Matrix n n R))
hσ : Equiv.Perm.permMatrix R σ ∈ openSegment R x₁ x₂
⊢ x₁ = Equiv.Perm.permMatrix R σ
have refine_2 : ∀ (i j : n), x₁ i j = x₂ i j
Tactic: suffices ∀ i j : n, x₁ i j = x₂ i j by
    obtain rfl : x₁ = x₂ := by simpa [← Matrix.ext_iff]
    simp_all