awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Convex.BetweenList
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
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
⊢ (∃ (p₁ : P) (p₂ : P), p₁ ≠ p₂ ∧ ∃ (l' : List R), l'.SortedLT ∧ map (⇑(lineMap p₁ p₂) : (a : R) → P) l' = l) ↔
    List.Sbtw R l

Tactic:
refine ⟨fun ⟨p₁, p₂, hp₁p₂, l', hl's, hl'l⟩ ↦ ?_, fun h ↦ ?_⟩
-- Module: Mathlib.Analysis.Convex.BetweenList
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
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')
⊢ List.Sbtw R l

Tactic:
subst hl'l
-- Module: Mathlib.Analysis.Convex.BetweenList
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')
refine_1 : List.Sbtw R l'
⊢ List.Sbtw.{u_1, u_2, u_4} R (P := P) (map (⇑(lineMap p₁ p₂) : (a : R) → P) l')

Tactic:
rw [(lineMap_injective _ hp₁p₂).list_sbtw_map_iff]

Premises used: Function.Injective.list_sbtw_map_iff, AffineMap.lineMap_injective
-- Module: Mathlib.Analysis.Convex.BetweenList
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 R l'

Tactic:
hl's.sbtw

Premises used: List.SortedLT.sbtw
-- Module: Mathlib.Analysis.Convex.BetweenList
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 R l'

Tactic:
exact hl's.sbtw

Premises used: List.SortedLT.sbtw
-- Module: Mathlib.Analysis.Convex.BetweenList
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
neg :
  ∀ (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

Tactic:
by_cases hl : l = []
-- Module: Mathlib.Analysis.Convex.BetweenList
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 :
  ∀ (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
⊢ ∃ (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₂⟩

Premises used: exists_pair_ne
-- Module: Mathlib.Analysis.Convex.BetweenList
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
hp₁p₂ : p₁ ≠ p₂
⊢ ∃ (l' : List R), l'.SortedLT ∧ map (⇑(lineMap p₁ p₂) : (a : R) → P) l' = l

Tactic:
simp [hl, sortedLT_iff_pairwise]

Premises used: List.sortedLT_iff_pairwise
-- Module: Mathlib.Analysis.Convex.BetweenList
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
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:
exact ⟨p₁, p₂, hp₁p₂, by simp [hl, sortedLT_iff_pairwise]⟩
-- Module: Mathlib.Analysis.Convex.BetweenList
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
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
⊢ ∃ (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

Premises used: List.length
-- Module: Mathlib.Analysis.Convex.BetweenList
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
⊢ ∃ (a : P), l = [a]

Tactic:
rw [length_eq_one_iff] at hlen

Premises used: List.length_eq_one_iff
-- Module: Mathlib.Analysis.Convex.BetweenList
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]
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₁]
⊢ ∃ (p₁ : P) (p₂ : P), p₁ ≠ p₂ ∧ ∃ (l' : List R), l'.SortedLT ∧ map (⇑(lineMap p₁ p₂) : (a : R) → P) l' = l

Tactic:
rcases hlen with ⟨p₁, rfl⟩

Premises used: rfl
-- Module: Mathlib.Analysis.Convex.BetweenList
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₁] = []
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₁]
⊢ ∃ (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₁⟩

Premises used: exists_ne
-- Module: Mathlib.Analysis.Convex.BetweenList
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₂ : P
hp₂p₁ : p₂ ≠ p₁
⊢ SortedLT.{u_1} (α := R) [0] ∧ map.{u_1, u_4} (α := R) (⇑(lineMap p₁ p₂) : (a : R) → P) [0] = [p₁]

Tactic:
simp [sortedLT_iff_pairwise]

Premises used: List.sortedLT_iff_pairwise
-- Module: Mathlib.Analysis.Convex.BetweenList
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₂ : 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:
exact ⟨p₁, p₂, hp₂p₁.symm, [0], by simp [sortedLT_iff_pairwise]⟩
-- Module: Mathlib.Analysis.Convex.BetweenList
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

Tactic:
⟨l.head hl, l.getLast hl, ?_⟩

Premises used: List.head, List.getLast, Exists.intro
-- Module: Mathlib.Analysis.Convex.BetweenList
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
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
⊢ ∃ (p₁ : P) (p₂ : P), p₁ ≠ p₂ ∧ ∃ (l' : List R), l'.SortedLT ∧ map (⇑(lineMap p₁ p₂) : (a : R) → P) l' = l

Tactic:
refine ⟨l.head hl, l.getLast hl, ?_⟩
-- Module: Mathlib.Analysis.Convex.BetweenList
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' : 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

Premises used: List.exists_map_eq_of_sorted_nonempty_iff_sbtw
-- Module: Mathlib.Analysis.Convex.BetweenList
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
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)
⊢ ¬l.length = 1

Tactic:
rw [← exists_map_eq_of_sorted_nonempty_iff_sbtw hl] at h

Premises used: List.exists_map_eq_of_sorted_nonempty_iff_sbtw
-- Module: Mathlib.Analysis.Convex.BetweenList
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' : 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

Premises used: false_or
-- Module: Mathlib.Analysis.Convex.BetweenList
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
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
⊢ 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⟩
-- Module: Mathlib.Analysis.Convex.BetweenList
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_1 : ¬l = []
hlen : ¬l.length = 1
l' : List R
hl's : l'.SortedLT
hl'l : map (⇑(lineMap (l.head hl_1) (l.getLast hl_1)) : (a : R) → P) l' = l
hl : l.head hl_1 ≠ l.getLast hl_1
⊢ l.head hl_1 ≠ l.getLast hl_1 ∧
    ∃ (l' : List R), l'.SortedLT ∧ map (⇑(lineMap (l.head hl_1) (l.getLast hl_1)) : (a : R) → P) l' = l

Tactic:
⟨hl, l', hl's, hl'l⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.Analysis.Convex.BetweenList
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_1 : ¬l = []
hlen : ¬l.length = 1
l' : List R
hl's : l'.SortedLT
hl'l : map (⇑(lineMap (l.head hl_1) (l.getLast hl_1)) : (a : R) → P) l' = l
hl : l.head hl_1 ≠ l.getLast hl_1
⊢ l.head hl_1 ≠ l.getLast hl_1 ∧
    ∃ (l' : List R), l'.SortedLT ∧ map (⇑(lineMap (l.head hl_1) (l.getLast hl_1)) : (a : R) → P) l' = l

Tactic:
exact ⟨hl, l', hl's, hl'l⟩
-- Module: Mathlib.Analysis.Convex.Birkhoff
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'
⊢ (∀ (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

Premises used: LT.lt.le, 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 : 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
i : n
⊢ ∑ j ∈ f i, M i j = s

Tactic:
simp [f, sum_subset (filter_subset _ _), hM.2.1]

Premises used: Finset.filter_subset, And.right, And.left, Finset.sum_subset
-- Module: Mathlib.Analysis.Convex.Birkhoff
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
⊢ ∀ (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]
-- Module: Mathlib.Analysis.Convex.Birkhoff
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
⊢ ∑ i ∈ A, ∑ j ∈ f i, M i j = (↑(#A) : R) * s

Tactic:
simp [this]
-- Module: Mathlib.Analysis.Convex.Birkhoff
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
⊢ ∑ 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]
-- Module: Mathlib.Analysis.Convex.Birkhoff
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
⊢ ∑ i : n, ∑ j ∈ A.biUnion f, M i j = (↑(#(A.biUnion f)) : R) * s

Tactic:
simp [sum_comm (t := A.biUnion f), hM.2.2]

Premises used: And.right, Finset.sum_comm
-- Module: Mathlib.Analysis.Convex.Birkhoff
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
⊢ ∑ 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]
-- Module: Mathlib.Analysis.Convex.Birkhoff
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_1 : ∀ (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
this : (↑(#A) : R) * s ≤ (↑(#(A.biUnion f)) : R) * s
⊢ #A ≤ #(A.biUnion f)

Tactic:
exact_mod_cast le_of_mul_le_mul_right this hs

Premises used: le_of_mul_le_mul_right
-- Module: Mathlib.Analysis.Convex.Birkhoff
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
suffices : (↑(#A) : R) * s ≤ (↑(#(A.biUnion f)) : R) * s
⊢ #A ≤ #(A.biUnion f)

Tactic:
suffices #A * s ≤ #(A.biUnion f) * s by exact_mod_cast le_of_mul_le_mul_right this hs
-- Module: Mathlib.Analysis.Convex.Birkhoff
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
rw : LE.le.{u_1} (α := R) (∑ i ∈ A, ∑ j ∈ f i, M i j) (∑ i : n, ∑ j ∈ A.biUnion f, M i j)
⊢ (↑(#A) : R) * s ≤ (↑(#(A.biUnion f)) : R) * s

Tactic:
rw [← 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 : 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)
trans₁ : LE.le.{u_1} (α := R) (∑ i ∈ A, ∑ j ∈ A.biUnion f, M i j) (∑ i : n, ∑ 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)

Tactic:
trans ∑ i ∈ A, ∑ j ∈ A.biUnion f, M i j

Premises used: Finset.biUnion
-- Module: Mathlib.Analysis.Convex.Birkhoff
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)

Tactic:
sum_le_sum fun i hi => ?_

Premises used: Finset.sum_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 : 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
refine : ∀ (i : n) (hi : i ∈ A), LE.le.{u_1} (α := R) (∑ j ∈ f i, M i j) (∑ j ∈ A.biUnion f, M i j)
⊢ LE.le.{u_1} (α := R) (∑ i ∈ A, ∑ j ∈ f i, M i j) (∑ i ∈ A, ∑ j ∈ A.biUnion f, M i j)

Tactic:
refine sum_le_sum fun i hi => ?_

Premises used: Finset.sum_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 : 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
i : n
hi : i ∈ A
⊢ ∀ i_1 ∈ A.biUnion f, i_1 ∉ f i → 0 ≤ M i i_1

Tactic:
simp [*]