awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Convex.BetweenList (goal)
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : AddTorsor V P
inst_6 : Nontrivial P
l : List P
refine_1 :
  (∃ (p₁ : P) (p₂ : P), p₁ ≠ p₂ ∧ ∃ (l' : List R), l'.SortedLT ∧ map (⇑(lineMap p₁ p₂) : (a : R) → P) l' = l) →
    ∀ (p₁ p₂ : P) (hp₁p₂ : p₁ ≠ p₂) (l' : List R) (hl's : l'.SortedLT)
      (hl'l : map (⇑(lineMap p₁ p₂) : (a : R) → P) l' = l), List.Sbtw R l
⊢ (∃ (p₁ : P) (p₂ : P), p₁ ≠ p₂ ∧ ∃ (l' : List R), l'.SortedLT ∧ map (⇑(lineMap p₁ p₂) : (a : R) → P) l' = l) ↔
    List.Sbtw R l
have refine_2 : ∀ (h : List.Sbtw R l),
  ∃ (p₁ : P) (p₂ : P), p₁ ≠ p₂ ∧ ∃ (l' : List R), l'.SortedLT ∧ map (⇑(lineMap p₁ p₂) : (a : R) → P) l' = l
Tactic: refine ⟨fun ⟨p₁, p₂, hp₁p₂, l', hl's, hl'l⟩ ↦ ?_, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Convex.BetweenList (goal)
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : AddTorsor V P
inst_6 : Nontrivial P
l : List P
h : ∃ (p₁ : P) (p₂ : P), p₁ ≠ p₂ ∧ ∃ (l' : List R), l'.SortedLT ∧ map (⇑(lineMap p₁ p₂) : (a : R) → P) l' = l
p₁ p₂ : P
hp₁p₂ : p₁ ≠ p₂
l' : List R
hl's : l'.SortedLT
hl'l : map (⇑(lineMap p₁ p₂) : (a : R) → P) l' = l
⊢ List.Sbtw R l
have refine_1 : (∃ (p₁_1 : P) (p₂_1 : P),
    p₁_1 ≠ p₂_1 ∧
      ∃ (l'_1 : List R),
        l'_1.SortedLT ∧
          Eq.{u_4 + 1} (α := List P) (map (⇑(lineMap p₁_1 p₂_1) : (a : R) → P) l'_1)
            (map (⇑(lineMap p₁ p₂) : (a : R) → P) l')) →
  List.Sbtw.{u_1, u_2, u_4} R (P := P) (map (⇑(lineMap p₁ p₂) : (a : R) → P) l')
Tactic: subst hl'l
Cleared hypotheses: l, h, hl'l
-- Lean 4 proof step from Mathlib.Analysis.Convex.BetweenList (goal)
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : AddTorsor V P
inst_6 : Nontrivial P
p₁ p₂ : P
hp₁p₂ : p₁ ≠ p₂
l' : List R
hl's : l'.SortedLT
h :
  ∃ (p₁_1 : P) (p₂_1 : P),
    p₁_1 ≠ p₂_1 ∧
      ∃ (l'_1 : List R),
        l'_1.SortedLT ∧
          Eq.{u_4 + 1} (α := List P) (map (⇑(lineMap p₁_1 p₂_1) : (a : R) → P) l'_1)
            (map (⇑(lineMap p₁ p₂) : (a : R) → P) l')
⊢ List.Sbtw.{u_1, u_2, u_4} R (P := P) (map (⇑(lineMap p₁ p₂) : (a : R) → P) l')
have refine_1 : List.Sbtw R l'
Tactic: rw [(lineMap_injective _ hp₁p₂).list_sbtw_map_iff]
-- Lean 4 proof step from Mathlib.Analysis.Convex.BetweenList (goal)
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : AddTorsor V P
inst_6 : Nontrivial P
l : List P
h : List.Sbtw R l
⊢ ∃ (p₁ : P) (p₂ : P), p₁ ≠ p₂ ∧ ∃ (l' : List R), l'.SortedLT ∧ map (⇑(lineMap p₁ p₂) : (a : R) → P) l' = l
have pos : ∀ (hl : l = []),
  ∃ (p₁ : P) (p₂ : P), p₁ ≠ p₂ ∧ ∃ (l' : List R), l'.SortedLT ∧ map (⇑(lineMap p₁ p₂) : (a : R) → P) l' = l
Tactic: by_cases hl : l = []
-- Lean 4 proof step from Mathlib.Analysis.Convex.BetweenList (goal)
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : AddTorsor V P
inst_6 : Nontrivial P
l : List P
h : List.Sbtw R l
pos :
  ∀ (hl : l = []),
    ∃ (p₁ : P) (p₂ : P), p₁ ≠ p₂ ∧ ∃ (l' : List R), l'.SortedLT ∧ map (⇑(lineMap p₁ p₂) : (a : R) → P) l' = l
⊢ ∃ (p₁ : P) (p₂ : P), p₁ ≠ p₂ ∧ ∃ (l' : List R), l'.SortedLT ∧ map (⇑(lineMap p₁ p₂) : (a : R) → P) l' = l
have neg : ∀ (hl : ¬l = []),
  ∃ (p₁ : P) (p₂ : P), p₁ ≠ p₂ ∧ ∃ (l' : List R), l'.SortedLT ∧ map (⇑(lineMap p₁ p₂) : (a : R) → P) l' = l
Tactic: by_cases hl : l = []
-- Lean 4 proof step from Mathlib.Analysis.Convex.BetweenList (goal)
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : AddTorsor V P
inst_6 : Nontrivial P
l : List P
h : List.Sbtw R l
hl : l = []
⊢ ∃ (p₁ : P) (p₂ : P), p₁ ≠ p₂ ∧ ∃ (l' : List R), l'.SortedLT ∧ map (⇑(lineMap p₁ p₂) : (a : R) → P) l' = l
have pos : ∀ (p₁ p₂ : P) (hp₁p₂ : p₁ ≠ p₂),
  ∃ (p₁ : P) (p₂ : P), p₁ ≠ p₂ ∧ ∃ (l' : List R), l'.SortedLT ∧ map (⇑(lineMap p₁ p₂) : (a : R) → P) l' = l
Tactic: rcases exists_pair_ne P with ⟨p₁, p₂, hp₁p₂⟩
-- Lean 4 proof step from Mathlib.Analysis.Convex.BetweenList (goal)
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : AddTorsor V P
inst_6 : Nontrivial P
l : List P
h : List.Sbtw R l
hl : ¬l = []
⊢ ∃ (p₁ : P) (p₂ : P), p₁ ≠ p₂ ∧ ∃ (l' : List R), l'.SortedLT ∧ map (⇑(lineMap p₁ p₂) : (a : R) → P) l' = l
have pos : ∀ (hlen : l.length = 1),
  ∃ (p₁ : P) (p₂ : P), p₁ ≠ p₂ ∧ ∃ (l' : List R), l'.SortedLT ∧ map (⇑(lineMap p₁ p₂) : (a : R) → P) l' = l
Tactic: by_cases hlen : l.length = 1
-- Lean 4 proof step from Mathlib.Analysis.Convex.BetweenList (goal)
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : AddTorsor V P
inst_6 : Nontrivial P
l : List P
h : List.Sbtw R l
hl : ¬l = []
pos :
  ∀ (hlen : l.length = 1),
    ∃ (p₁ : P) (p₂ : P), p₁ ≠ p₂ ∧ ∃ (l' : List R), l'.SortedLT ∧ map (⇑(lineMap p₁ p₂) : (a : R) → P) l' = l
⊢ ∃ (p₁ : P) (p₂ : P), p₁ ≠ p₂ ∧ ∃ (l' : List R), l'.SortedLT ∧ map (⇑(lineMap p₁ p₂) : (a : R) → P) l' = l
have neg : ∀ (hlen : ¬l.length = 1),
  ∃ (p₁ : P) (p₂ : P), p₁ ≠ p₂ ∧ ∃ (l' : List R), l'.SortedLT ∧ map (⇑(lineMap p₁ p₂) : (a : R) → P) l' = l
Tactic: by_cases hlen : l.length = 1
-- Lean 4 proof step from Mathlib.Analysis.Convex.BetweenList (hypothesis)
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : AddTorsor V P
inst_6 : Nontrivial P
l : List P
h : List.Sbtw R l
hl : ¬l = []
hlen : l.length = 1
⊢ ∃ (p₁ : P) (p₂ : P), p₁ ≠ p₂ ∧ ∃ (l' : List R), l'.SortedLT ∧ map (⇑(lineMap p₁ p₂) : (a : R) → P) l' = l
have hlen₁ : ∃ (a : P), l = [a]
Tactic: rw [length_eq_one_iff] at hlen
Cleared hypotheses: hlen
-- Lean 4 proof step from Mathlib.Analysis.Convex.BetweenList (goal)
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : AddTorsor V P
inst_6 : Nontrivial P
l : List P
h : List.Sbtw R l
hl : ¬l = []
hlen : ∃ (a : P), l = [a]
⊢ ∃ (p₁ : P) (p₂ : P), p₁ ≠ p₂ ∧ ∃ (l' : List R), l'.SortedLT ∧ map (⇑(lineMap p₁ p₂) : (a : R) → P) l' = l
have pos : ∀ (p₁ : P) (h : List.Sbtw R [p₁]) (hl : ¬[p₁] = []),
  ∃ (p₁_1 : P) (p₂ : P), p₁_1 ≠ p₂ ∧ ∃ (l' : List R), l'.SortedLT ∧ map (⇑(lineMap p₁_1 p₂) : (a : R) → P) l' = [p₁]
Tactic: rcases hlen with ⟨p₁, rfl⟩
Cleared hypotheses: l, h, hl, hlen
-- Lean 4 proof step from Mathlib.Analysis.Convex.BetweenList (goal)
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : AddTorsor V P
inst_6 : Nontrivial P
p₁ : P
h : List.Sbtw R [p₁]
hl : ¬[p₁] = []
⊢ ∃ (p₁_1 : P) (p₂ : P), p₁_1 ≠ p₂ ∧ ∃ (l' : List R), l'.SortedLT ∧ map (⇑(lineMap p₁_1 p₂) : (a : R) → P) l' = [p₁]
have pos : ∀ (p₂ : P) (hp₂p₁ : p₂ ≠ p₁),
  ∃ (p₁_1 : P) (p₂ : P), p₁_1 ≠ p₂ ∧ ∃ (l' : List R), l'.SortedLT ∧ map (⇑(lineMap p₁_1 p₂) : (a : R) → P) l' = [p₁]
Tactic: rcases exists_ne p₁ with ⟨p₂, hp₂p₁⟩
-- Lean 4 proof step from Mathlib.Analysis.Convex.BetweenList (goal)
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : AddTorsor V P
inst_6 : Nontrivial P
l : List P
h : List.Sbtw R l
hl : ¬l = []
hlen : ¬l.length = 1
⊢ ∃ (p₁ : P) (p₂ : P), p₁ ≠ p₂ ∧ ∃ (l' : List R), l'.SortedLT ∧ map (⇑(lineMap p₁ p₂) : (a : R) → P) l' = l
have neg : l.head hl ≠ l.getLast hl ∧
  ∃ (l' : List R), l'.SortedLT ∧ map (⇑(lineMap (l.head hl) (l.getLast hl)) : (a : R) → P) l' = l
Tactic: refine ⟨l.head hl, l.getLast hl, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Convex.BetweenList (hypothesis)
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : AddTorsor V P
inst_6 : Nontrivial P
l : List P
h : List.Sbtw R l
hl : ¬l = []
hlen : ¬l.length = 1
⊢ l.head hl ≠ l.getLast hl ∧
    ∃ (l' : List R), l'.SortedLT ∧ map (⇑(lineMap (l.head hl) (l.getLast hl)) : (a : R) → P) l' = l
have h₁ : ∃ (l' : List R),
  l'.SortedLT ∧
    map (⇑(lineMap (l.head hl) (l.getLast hl)) : (a : R) → P) l' = l ∧ (l.length = 1 ∨ l.head hl ≠ l.getLast hl)
Tactic: rw [← exists_map_eq_of_sorted_nonempty_iff_sbtw hl] at h
Cleared hypotheses: h, hlen
-- Lean 4 proof step from Mathlib.Analysis.Convex.BetweenList (hypothesis)
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : AddTorsor V P
inst_6 : Nontrivial P
l : List P
hl : ¬l = []
h :
  ∃ (l' : List R),
    l'.SortedLT ∧
      map (⇑(lineMap (l.head hl) (l.getLast hl)) : (a : R) → P) l' = l ∧ (l.length = 1 ∨ l.head hl ≠ l.getLast hl)
hlen : ¬l.length = 1
⊢ l.head hl ≠ l.getLast hl ∧
    ∃ (l' : List R), l'.SortedLT ∧ map (⇑(lineMap (l.head hl) (l.getLast hl)) : (a : R) → P) l' = l
have h₁ : ∃ (l' : List R),
  l'.SortedLT ∧ map (⇑(lineMap (l.head hl) (l.getLast hl)) : (a : R) → P) l' = l ∧ l.head hl ≠ l.getLast hl
Tactic: simp only [hlen, false_or] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.Convex.BetweenList (goal)
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : AddTorsor V P
inst_6 : Nontrivial P
l : List P
hl : ¬l = []
hlen : ¬l.length = 1
h :
  ∃ (l' : List R),
    l'.SortedLT ∧ map (⇑(lineMap (l.head hl) (l.getLast hl)) : (a : R) → P) l' = l ∧ l.head hl ≠ l.getLast hl
⊢ l.head hl ≠ l.getLast hl ∧
    ∃ (l' : List R), l'.SortedLT ∧ map (⇑(lineMap (l.head hl) (l.getLast hl)) : (a : R) → P) l' = l
have neg : ∀ (l' : List R) (hl's : l'.SortedLT) (hl'l : map (⇑(lineMap (l.head hl) (l.getLast hl)) : (a : R) → P) l' = l)
  (hl_1 : l.head hl ≠ l.getLast hl),
  l.head hl ≠ l.getLast hl ∧
    ∃ (l' : List R), l'.SortedLT ∧ map (⇑(lineMap (l.head hl) (l.getLast hl)) : (a : R) → P) l' = l
Tactic: rcases h with ⟨l', hl's, hl'l, hl⟩
Cleared hypotheses: 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 : Semifield R
inst_3 : LinearOrder R
inst_4 : IsStrictOrderedRing R
M : Matrix n n R
inst_5 : Nonempty n
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'
⊢ ∃ (σ : Equiv.Perm n), ∀ (i j : n), M i j = 0 → Equiv.Perm.permMatrix R σ i j = 0
have hM₁ : (∀ (i j : n), 0 ≤ M i j) ∧ (∀ (i : n), ∑ j : n, M i j = s) ∧ ∀ (j : n), ∑ i : n, M i j = s
Tactic: rw [exists_mem_doublyStochastic_eq_smul_iff hs.le] at hM
Cleared hypotheses: 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 : Semifield R
inst_3 : LinearOrder R
inst_4 : IsStrictOrderedRing R
M : Matrix n n R
inst_5 : Nonempty n
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
f : (i : n) → Finset n := fun (i : n) ↦ {j : n | M i j ≠ 0}
A : Finset n
⊢ #A ≤ #(A.biUnion f)
have this : ∀ (i : n), ∑ j ∈ f i, M i j = s
Tactic: have (i : _) : ∑ j ∈ f i, M i j = s := by simp [f, sum_subset (filter_subset _ _), hM.2.1]
-- 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 : Semifield R
inst_3 : LinearOrder R
inst_4 : IsStrictOrderedRing R
M : Matrix n n R
inst_5 : Nonempty n
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
f : (i : n) → Finset n := fun (i : n) ↦ {j : n | M i j ≠ 0}
A : Finset n
this : ∀ (i : n), ∑ j ∈ f i, M i j = s
⊢ #A ≤ #(A.biUnion f)
have h₁ : ∑ i ∈ A, ∑ j ∈ f i, M i j = (↑(#A) : R) * s
Tactic: have h₁ : ∑ i ∈ A, ∑ j ∈ f i, M i j = #A * s := by simp [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 : Semifield R
inst_3 : LinearOrder R
inst_4 : IsStrictOrderedRing R
M : Matrix n n R
inst_5 : Nonempty n
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
f : (i : n) → Finset n := fun (i : n) ↦ {j : n | M i j ≠ 0}
A : Finset n
this : ∀ (i : n), ∑ j ∈ f i, M i j = s
h₁ : ∑ i ∈ A, ∑ j ∈ f i, M i j = (↑(#A) : R) * s
⊢ #A ≤ #(A.biUnion f)
have h₂ : ∑ i : n, ∑ j ∈ A.biUnion f, M i j = (↑(#(A.biUnion f)) : R) * s
Tactic: have h₂ : ∑ i, ∑ j ∈ A.biUnion f, M i j = #(A.biUnion f) * s := by
      simp [sum_comm (t := A.biUnion f), hM.2.2]
-- 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 : Semifield R
inst_3 : LinearOrder R
inst_4 : IsStrictOrderedRing R
M : Matrix n n R
inst_5 : Nonempty n
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
f : (i : n) → Finset n := fun (i : n) ↦ {j : n | M i j ≠ 0}
A : Finset n
this : ∀ (i : n), ∑ j ∈ f i, M i j = s
h₁ : ∑ i ∈ A, ∑ j ∈ f i, M i j = (↑(#A) : R) * s
h₂ : ∑ i : n, ∑ j ∈ A.biUnion f, M i j = (↑(#(A.biUnion f)) : R) * s
⊢ #A ≤ #(A.biUnion f)
have suffices : (↑(#A) : R) * s ≤ (↑(#(A.biUnion f)) : R) * s
Tactic: suffices #A * s ≤ #(A.biUnion f) * s by exact_mod_cast le_of_mul_le_mul_right this 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 : Semifield R
inst_3 : LinearOrder R
inst_4 : IsStrictOrderedRing R
M : Matrix n n R
inst_5 : Nonempty n
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
f : (i : n) → Finset n := fun (i : n) ↦ {j : n | M i j ≠ 0}
A : Finset n
this : ∀ (i : n), ∑ j ∈ f i, M i j = s
h₁ : ∑ i ∈ A, ∑ j ∈ f i, M i j = (↑(#A) : R) * s
h₂ : ∑ i : n, ∑ j ∈ A.biUnion f, M i j = (↑(#(A.biUnion f)) : R) * s
⊢ (↑(#A) : R) * s ≤ (↑(#(A.biUnion f)) : R) * s
have rw : LE.le.{u_1} (α := R) (∑ i ∈ A, ∑ j ∈ f i, M i j) (∑ i : n, ∑ j ∈ A.biUnion f, M i j)
Tactic: rw [← 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 : Semifield R
inst_3 : LinearOrder R
inst_4 : IsStrictOrderedRing R
M : Matrix n n R
inst_5 : Nonempty n
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
f : (i : n) → Finset n := fun (i : n) ↦ {j : n | M i j ≠ 0}
A : Finset n
this : ∀ (i : n), ∑ j ∈ f i, M i j = s
h₁ : ∑ i ∈ A, ∑ j ∈ f i, M i j = (↑(#A) : R) * s
h₂ : ∑ i : n, ∑ j ∈ A.biUnion f, M i j = (↑(#(A.biUnion f)) : R) * s
⊢ LE.le.{u_1} (α := R) (∑ i ∈ A, ∑ j ∈ f i, M i j) (∑ i : n, ∑ j ∈ A.biUnion f, M i j)
have trans : LE.le.{u_1} (α := R) (∑ i ∈ A, ∑ j ∈ f i, M i j) (∑ i ∈ A, ∑ j ∈ A.biUnion f, M i j)
Tactic: trans ∑ i ∈ A, ∑ j ∈ A.biUnion f, M i j
-- 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 : Semifield R
inst_3 : LinearOrder R
inst_4 : IsStrictOrderedRing R
M : Matrix n n R
inst_5 : Nonempty n
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
f : (i : n) → Finset n := fun (i : n) ↦ {j : n | M i j ≠ 0}
A : Finset n
this : ∀ (i : n), ∑ j ∈ f i, M i j = s
h₁ : ∑ i ∈ A, ∑ j ∈ f i, M i j = (↑(#A) : R) * s
h₂ : ∑ i : n, ∑ j ∈ A.biUnion f, M i j = (↑(#(A.biUnion f)) : R) * s
trans : LE.le.{u_1} (α := R) (∑ i ∈ A, ∑ j ∈ f i, M i j) (∑ i ∈ A, ∑ j ∈ A.biUnion f, M i j)
⊢ LE.le.{u_1} (α := R) (∑ i ∈ A, ∑ j ∈ f i, M i j) (∑ i : n, ∑ j ∈ A.biUnion f, M i j)
have trans₁ : LE.le.{u_1} (α := R) (∑ i ∈ A, ∑ j ∈ A.biUnion f, M i j) (∑ i : n, ∑ j ∈ A.biUnion f, M i j)
Tactic: trans ∑ i ∈ A, ∑ j ∈ A.biUnion f, M i j
-- 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 : Semifield R
inst_3 : LinearOrder R
inst_4 : IsStrictOrderedRing R
M : Matrix n n R
inst_5 : Nonempty n
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
f : (i : n) → Finset n := fun (i : n) ↦ {j : n | M i j ≠ 0}
A : Finset n
this : ∀ (i : n), ∑ j ∈ f i, M i j = s
h₁ : ∑ i ∈ A, ∑ j ∈ f i, M i j = (↑(#A) : R) * s
h₂ : ∑ i : n, ∑ j ∈ A.biUnion f, M i j = (↑(#(A.biUnion f)) : R) * s
⊢ LE.le.{u_1} (α := R) (∑ i ∈ A, ∑ j ∈ f i, M i j) (∑ i ∈ A, ∑ j ∈ A.biUnion f, M i j)
have refine : ∀ (i : n) (hi : i ∈ A), LE.le.{u_1} (α := R) (∑ j ∈ f i, M i j) (∑ j ∈ A.biUnion f, M i j)
Tactic: refine sum_le_sum fun i 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 : Semifield R
inst_3 : LinearOrder R
inst_4 : IsStrictOrderedRing R
M : Matrix n n R
inst_5 : Nonempty n
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
f : (i : n) → Finset n := fun (i : n) ↦ {j : n | M i j ≠ 0}
⊢ ∃ (σ : Equiv.Perm n), ∀ (i j : n), M i j = 0 → Equiv.Perm.permMatrix R σ i j = 0
have hf : ∀ (A : Finset n), #A ≤ #(A.biUnion f)
Tactic: have hf (A : Finset n) : #A ≤ #(A.biUnion f) := by
    have (i : _) : ∑ j ∈ f i, M i j = s := by simp [f, sum_subset (filter_subset _ _), hM.2.1]
    have h₁ : ∑ i ∈ A, ∑ j ∈ f i, M i j = #A * s := by simp [this]
    have h₂ : ∑ i, ∑ j ∈ A.biUnion f, M i j = #(A.biUnion f) * s := by
      simp [sum_comm (t := A.biUnion f), hM.2.2]
    suffices #A * s ≤ #(A.biUnion f) * s by exact_mod_cast le_of_mul_le_mul_right this hs
    rw [← h₁, ← h₂]
    trans ∑ i ∈ A, ∑ j ∈ A.biUnion f, M i j
    · refine sum_le_sum fun i hi => ?_
      exact sum_le_sum_of_subset_of_nonneg (subset_biUnion_of_mem f hi) (by simp [*])
    · exact sum_le_sum_of_subset_of_nonneg (by simp) fun _ _ _ => sum_nonneg fun j _ => 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 : Semifield R
inst_3 : LinearOrder R
inst_4 : IsStrictOrderedRing R
M : Matrix n n R
inst_5 : Nonempty n
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
f : (i : n) → Finset n := fun (i : n) ↦ {j : n | M i j ≠ 0}
hf : ∀ (A : Finset n), #A ≤ #(A.biUnion f)
⊢ ∃ (σ : Equiv.Perm n), ∀ (i j : n), M i j = 0 → Equiv.Perm.permMatrix R σ i j = 0
have obtain : ∀ (g : n → n) (hg : Injective g) (hg' : ∀ (x : n), g x ∈ f x),
  ∃ (σ : Equiv.Perm n), ∀ (i j : n), M i j = 0 → Equiv.Perm.permMatrix R σ i j = 0
Tactic: obtain ⟨g, hg, hg'⟩ := (all_card_le_biUnion_card_iff_exists_injective f).1 hf
-- 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 : Semifield R
inst_3 : LinearOrder R
inst_4 : IsStrictOrderedRing R
M : Matrix n n R
inst_5 : Nonempty n
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
f : (i : n) → Finset n := fun (i : n) ↦ {j : n | M i j ≠ 0}
hf : ∀ (A : Finset n), #A ≤ #(A.biUnion f)
g : n → n
hg : Injective g
hg' : ∀ (x : n), g x ∈ f x
⊢ ∃ (σ : Equiv.Perm n), ∀ (i j : n), M i j = 0 → Equiv.Perm.permMatrix R σ i j = 0
have hg₁ : Bijective g
Tactic: rw [Finite.injective_iff_bijective] at hg
Cleared hypotheses: hg, hg'
-- 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 : Semifield R
inst_3 : LinearOrder R
inst_4 : IsStrictOrderedRing R
M : Matrix n n R
inst_5 : Nonempty n
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
f : (i : n) → Finset n := fun (i : n) ↦ {j : n | M i j ≠ 0}
hf : ∀ (A : Finset n), #A ≤ #(A.biUnion f)
g : n → n
hg : Bijective g
hg' : ∀ (x : n), g x ∈ f x
⊢ ∃ (σ : Equiv.Perm n), ∀ (i j : n), M i j = 0 → Equiv.Perm.permMatrix R σ i j = 0
have refine : ∀ (i j : n) (hij : M i j = 0), Equiv.Perm.permMatrix R (Equiv.ofBijective g hg) i j = 0
Tactic: refine ⟨Equiv.ofBijective g hg, fun i j hij => ?_⟩
-- 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 : Semifield R
inst_3 : LinearOrder R
inst_4 : IsStrictOrderedRing R
M : Matrix n n R
inst_5 : Nonempty n
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
f : (i : n) → Finset n := fun (i : n) ↦ {j : n | M i j ≠ 0}
hf : ∀ (A : Finset n), #A ≤ #(A.biUnion f)
g : n → n
hg : Bijective g
hg' : ∀ (x : n), g x ∈ f x
i j : n
hij : M i j = 0
⊢ Equiv.Perm.permMatrix R (Equiv.ofBijective g hg) i j = 0
have simp : ¬g i = j
Tactic: simp only [PEquiv.toMatrix_apply, Option.mem_def, ite_eq_right_iff, one_ne_zero, imp_false,
    Equiv.toPEquiv_apply, Equiv.ofBijective_apply, Option.some.injEq]
-- 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'
⊢ ∃ (w : Equiv.Perm n → R), (∀ (σ : Equiv.Perm n), 0 ≤ w σ) ∧ ∑ σ : Equiv.Perm n, w σ • Equiv.Perm.permMatrix R σ = M
have rcases : IsEmpty n →
  ∃ (w : Equiv.Perm n → R), (∀ (σ : Equiv.Perm n), 0 ≤ w σ) ∧ ∑ σ : 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
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'
rcases :
  IsEmpty n →
    ∃ (w : Equiv.Perm n → R), (∀ (σ : Equiv.Perm n), 0 ≤ w σ) ∧ ∑ σ : Equiv.Perm n, w σ • Equiv.Perm.permMatrix R σ = M
⊢ ∃ (w : Equiv.Perm n → R), (∀ (σ : Equiv.Perm n), 0 ≤ w σ) ∧ ∑ σ : Equiv.Perm n, w σ • Equiv.Perm.permMatrix R σ = M
have inr : Nonempty n →
  ∃ (w : Equiv.Perm n → R), (∀ (σ : Equiv.Perm n), 0 ≤ w σ) ∧ ∑ σ : Equiv.Perm n, w σ • Equiv.Perm.permMatrix R σ = M
Tactic: rcases isEmpty_or_nonempty n
-- 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
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
⊢ ∃ (w : Equiv.Perm n → R), (∀ (σ : Equiv.Perm n), 0 ≤ w σ) ∧ ∑ σ : Equiv.Perm n, w σ • Equiv.Perm.permMatrix R σ = M
have hd : let d := card.{u_2} (α := n × n) {i : n × n | M i.1 i.2 ≠ 0};
card.{u_2} (α := n × n) {i : n × n | M i.1 i.2 ≠ 0} = d
Tactic: set d : ℕ := #{i : n × n | M i.1 i.2 ≠ 0} with ← hd