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_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' : 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 σ
h : M i ((σ : (a : n) → n) i) = 0
⊢ False

Tactic:
simpa [Equiv.toPEquiv_apply] using hσ _ _ h

Premises used: Equiv.toPEquiv_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
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 σ
⊢ 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
-- 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' : 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)
simp : M i ((σ : (a : n) → n) i) ≤ ∑ j : n, M i j
⊢ 0 ≤ s'

Tactic:
simp only [s', sub_nonneg, ← hM.2.1 i]

Premises used: And.right, And.left, sub_nonneg
-- 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' : 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)
⊢ Membership.mem (α := n) (γ := Finset n) univ ((σ : (a : n) → n) i : n)

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
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)
⊢ M i ((σ : (a : n) → n) i) ≤ ∑ j : n, M i j

Tactic:
exact single_le_sum (fun j _ => hM.1 i j) (by simp)

Premises used: And.left, Finset.single_le_sum
-- 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' : 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'

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)
-- 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'
rw : (∀ (i j : n), 0 ≤ N i j) ∧ (∀ (i : n), ∑ j : n, N i j = s') ∧ ∀ (j : n), ∑ i : n, N i j = s'
⊢ ∃ (M' : Matrix n n R), Membership.mem (γ := Submonoid (Matrix n n R)) (doublyStochastic R n) M' ∧ N = s' • M'

Tactic:
rw [exists_mem_doublyStochastic_eq_smul_iff hs']

Premises used: exists_mem_doublyStochastic_eq_smul_iff
-- 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'
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'
⊢ (∀ (i j : n), 0 ≤ N i j) ∧ (∀ (i : n), ∑ j : n, N i j = s') ∧ ∀ (j : n), ∑ i : n, N i j = 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]

Premises used: Finset.mem_univ, Equiv.toPEquiv_apply, Option.some.injEq, Matrix.sub_apply, mul_ite, Matrix.smul_apply, MulZeroClass.mul_zero, Finset.sum_sub_distrib, reduceIte, PEquiv.toMatrix_apply, smul_eq_mul, mul_one, sub_nonneg, Finset.sum_ite_eq, Option.mem_def
-- Module: Mathlib.Analysis.Convex.Birkhoff
Goal:
R : Type u_1
n : Type u_2
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : 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 : n), ∑ x : n, M i_1 x - M i ((σ : (a : n) → n) i) = s'

Tactic:
simp [s', hM.2.1]

Premises used: And.right, 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'
⊢ ∀ (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 [s', ← σ.eq_symm_apply, hM]

Premises used: Equiv.eq_symm_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
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'
refine : ∀ (i' j : n), (if (σ : (a : n) → n) i' = j then M i ((σ : (a : n) → n) i) else 0) ≤ M i' j
⊢ (∀ (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:
refine ⟨fun i' j => ?_, by simp [s', hM.2.1], by simp [s', ← σ.eq_symm_apply, hM]⟩
-- Module: Mathlib.Analysis.Convex.Birkhoff
Goal:
R : Type u_1
n : Type u_2
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : Field R
inst_3 : LinearOrder R
inst_4 : IsStrictOrderedRing R
h : Nonempty n
d : ℕ
ih :
  ∀ m < d,
    ∀ (M : Matrix n n R) (s : R) (hs : 0 ≤ s)
      (hM :
        ∃ (M' : Matrix n n R), Membership.mem (γ := Submonoid (Matrix n n R)) (doublyStochastic R n) M' ∧ M = s • M')
      (hd : card.{u_2} (α := n × n) {i : n × n | M i.1 i.2 ≠ 0} = m),
      ∃ (w : Equiv.Perm n → R),
        (∀ (σ : Equiv.Perm n), 0 ≤ w σ) ∧ ∑ σ : Equiv.Perm n, w σ • Equiv.Perm.permMatrix R σ = M
M : Matrix n n R
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
isFalse : ¬(σ : (a : n) → n) i' = j → 0 ≤ M i' j
⊢ (if (σ : (a : n) → n) i' = j then M i ((σ : (a : n) → n) i) else 0) ≤ M i' j

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_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
⊢ Membership.mem (γ := Finset n) univ i'

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
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
rw rw₁ : M i' j = M i' j
⊢ M i' ((σ : (a : n) → n) i') = M i' j

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

Tactic:
exact (hi' i' (by simp)).trans_eq (by rw [h])

Premises used: LE.le.trans_eq
-- 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'
i' j : n
h_1 : (σ : (a : n) → n) i' = j
⊢ M i ((σ : (a : n) → n) i) ≤ M i' j

Tactic:
case isTrue h => exact (hi' i' (by simp)).trans_eq (by rw [h])

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

Tactic:
hM.1 _ _

Premises used: And.left