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_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
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
h : (σ : (a : n) → n) i' = j
⊢ M i' ((σ : (a : n) → n) i') = M i' j
have rw : M i' j = M i' j
Tactic: rw [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
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'
⊢ ∃ (w : Equiv.Perm n → R), (∀ (σ : Equiv.Perm n), 0 ≤ w σ) ∧ ∑ σ : Equiv.Perm n, w σ • Equiv.Perm.permMatrix R σ = M
have this : ∃ (M' : Matrix n n R), Membership.mem (γ := Submonoid (Matrix n n R)) (doublyStochastic R n) M' ∧ N = s' • M'
Tactic: have : ∃ M' ∈ doublyStochastic R n, N = s' • M' := by
    rw [exists_mem_doublyStochastic_eq_smul_iff hs']
    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]
    refine ⟨fun i' j => ?_, by simp [s', hM.2.1], by simp [s', ← σ.eq_symm_apply, hM]⟩
    split
    case isTrue h => exact (hi' i' (by simp)).trans_eq (by rw [h])
    case isFalse h => exact hM.1 _ _
-- 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'
⊢ card.{u_2} (α := n × n) {i : n × n | N i.1 i.2 ≠ 0} < d
have rw : card.{u_2} (α := n × n) {i : n × n | N i.1 i.2 ≠ 0} < card.{u_2} (α := n × n) {i : n × n | M i.1 i.2 ≠ 0}
Tactic: rw [← 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 : (∀ (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} < card.{u_2} (α := n × n) {i : n × n | M i.1 i.2 ≠ 0}
have h : SSubset.{u_2} (α := Finset (n × n)) {i : n × n | N i.1 i.2 ≠ 0} {i : n × n | M i.1 i.2 ≠ 0}
Tactic: gcongr
-- 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'
⊢ SSubset.{u_2} (α := Finset (n × n)) {i : n × n | N i.1 i.2 ≠ 0} {i : n × n | M i.1 i.2 ≠ 0}
have h : ∃ (x : n × n), Membership.mem (γ := Finset (n × n)) {i : n × n | M i.1 i.2 ≠ 0} x ∧ x ∉ {i : n × n | N i.1 i.2 ≠ 0}
Tactic: rw [ssubset_iff_of_subset (monotone_filter_right _ _)]
-- 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_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
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'
h : ∃ (x : n × n), Membership.mem (γ := Finset (n × n)) {i : n × n | M i.1 i.2 ≠ 0} x ∧ x ∉ {i : n × n | N i.1 i.2 ≠ 0}
⊢ SSubset.{u_2} (α := Finset (n × n)) {i : n × n | N i.1 i.2 ≠ 0} {i : n × n | M i.1 i.2 ≠ 0}
have rw : ∀ (a : n × n), Membership.mem (γ := Finset (n × n)) univ a → N a.1 a.2 ≠ 0 → M a.1 a.2 ≠ 0
Tactic: rw [ssubset_iff_of_subset (monotone_filter_right _ _)]
-- 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'
⊢ ∃ (x : n × n), Membership.mem (γ := Finset (n × n)) {i : n × n | M i.1 i.2 ≠ 0} x ∧ x ∉ {i : n × n | N i.1 i.2 ≠ 0}
have h : ∃ (a : n) (b : n), M a b ≠ 0 ∧ N a b = 0
Tactic: simp_rw [mem_filter_univ, not_not, Prod.exists]
-- 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'
⊢ ∃ (a : n) (b : n), M a b ≠ 0 ∧ N a b = 0
have h : N i ((σ : (a : n) → n) i) = 0
Tactic: refine ⟨i, σ i, hMi'.ne', ?_⟩
-- 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'_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'
i' j' : n
h_1 : Membership.mem (γ := Finset (n × n)) univ (i', j')
hN' : ¬N i' j' = 0
hM' : M i' j' = 0
⊢ False
have hN'₁ : (σ : (a : n) → n) i' = j' ∧ ¬M i ((σ : (a : n) → n) i) = 0
Tactic: 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'
Cleared hypotheses: hN'
-- 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'_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'
i' j' : n
h_1 : Membership.mem (γ := Finset (n × n)) univ (i', j')
hM' : M i' j' = 0
hN' : (σ : (a : n) → n) i' = j' ∧ ¬M i ((σ : (a : n) → n) i) = 0
⊢ False
have right : ¬M i ((σ : (a : n) → n) i) = 0
Tactic: obtain ⟨rfl, _⟩ := hN'
Cleared hypotheses: j', h_1, hM', hN'
-- 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'_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'
i' j' : n
h_1 : Membership.mem (γ := Finset (n × n)) univ (i', j')
hM' : M i' j' = 0
hN' : (σ : (a : n) → n) i' = j' ∧ ¬M i ((σ : (a : n) → n) i) = 0
right : ¬M i ((σ : (a : n) → n) i) = 0
⊢ False
have a : Membership.mem (α := n × n) (γ := Finset (n × n)) univ ((i', (σ : (a : n) → n) i') : n × n)
Tactic: obtain ⟨rfl, _⟩ := hN'
Cleared hypotheses: j', h_1, hM', hN'
-- 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'_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'
i' j' : n
h_1 : Membership.mem (γ := Finset (n × n)) univ (i', j')
hM' : M i' j' = 0
hN' : (σ : (a : n) → n) i' = j' ∧ ¬M i ((σ : (a : n) → n) i) = 0
right : ¬M i ((σ : (a : n) → n) i) = 0
a : Membership.mem (α := n × n) (γ := Finset (n × n)) univ ((i', (σ : (a : n) → n) i') : n × n)
⊢ False
have hM'₁ : M i' ((σ : (a : n) → n) i') = 0
Tactic: obtain ⟨rfl, _⟩ := hN'
Cleared hypotheses: j', h_1, hM', hN'
-- 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'
i' : n
right : ¬M i ((σ : (a : n) → n) i) = 0
h_1 : Membership.mem (α := n × n) (γ := Finset (n × n)) univ ((i', (σ : (a : n) → n) i') : n × n)
hM' : M i' ((σ : (a : n) → n) i') = 0
⊢ False
have linarith : 0 - M i ((σ : (a : n) → n) i) + (M i' ((σ : (a : n) → n) i') - 0) +
    (M i ((σ : (a : n) → n) i) - M i' ((σ : (a : n) → n) i')) =
  0
Tactic: linarith [hi' i' (by simp)]
-- 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'_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'
⊢ ∃ (w : Equiv.Perm n → R), (∀ (σ : Equiv.Perm n), 0 ≤ w σ) ∧ ∑ σ : Equiv.Perm n, w σ • Equiv.Perm.permMatrix R σ = M
have hd' : 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)]