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
⊢ (↑(doublyStochastic R n) : Set (Matrix n n R)) =
    (convexHull R : (a : Set (Matrix n n R)) → Set (Matrix n n R))
      {x : Matrix n n R | ∃ (σ : Equiv.Perm n), Equiv.Perm.permMatrix R σ = x}

Tactic:
(convexHull_min ?g1 convex_doublyStochastic).antisymm' fun M hM => ?g2

Premises used: convexHull_min, HasSubset.Subset.antisymm'
-- 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
refine :
  {x : Matrix n n R | ∃ (σ : Equiv.Perm n), Equiv.Perm.permMatrix R σ = x} ⊆
    (↑(doublyStochastic R n) : Set (Matrix n n R))
refine₁ :
  ∀ (M : Matrix n n R) (hM : M ∈ (↑(doublyStochastic R n) : Set (Matrix n n R))),
    Membership.mem (γ := Set (Matrix n n R))
      ((convexHull R : (a : Set (Matrix n n R)) → Set (Matrix n n R))
          {x : Matrix n n R | ∃ (σ : Equiv.Perm n), Equiv.Perm.permMatrix R σ = x} :
        Set (Matrix n n R))
      M
⊢ (↑(doublyStochastic R n) : Set (Matrix n n R)) =
    (convexHull R : (a : Set (Matrix n n R)) → Set (Matrix n n R))
      {x : Matrix n n R | ∃ (σ : Equiv.Perm n), Equiv.Perm.permMatrix R σ = x}

Tactic:
refine (convexHull_min ?g1 convex_doublyStochastic).antisymm' fun M hM => ?g2

Premises used: convexHull_min, HasSubset.Subset.antisymm'
-- 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 : Equiv.Perm n
⊢ Equiv.Perm.permMatrix R h ∈ (↑(doublyStochastic R n) : Set (Matrix n n R))

Tactic:
permMatrix_mem_doublyStochastic

Premises used: Set.Mem, setOf, permMatrix_mem_doublyStochastic
-- 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 : Equiv.Perm n
⊢ Equiv.Perm.permMatrix R h ∈ (↑(doublyStochastic R n) : Set (Matrix n n R))

Tactic:
exact permMatrix_mem_doublyStochastic

Premises used: permMatrix_mem_doublyStochastic
-- 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
⊢ {x : Matrix n n R | ∃ (σ : Equiv.Perm n), Equiv.Perm.permMatrix R σ = x} ⊆
    (↑(doublyStochastic R n) : Set (Matrix n n R))

Tactic:
case g1 =>
    rintro x ⟨h, rfl⟩
    exact permMatrix_mem_doublyStochastic

Premises used: permMatrix_mem_doublyStochastic, rfl
-- 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
M : Matrix n n R
hM : M ∈ (↑(doublyStochastic R n) : Set (Matrix n n R))
obtain :
  ∀ (w : Equiv.Perm n → R) (hw1 : ∀ (σ : Equiv.Perm n), 0 ≤ w σ)
    (hw2 : Eq.{u_1 + 1} (α := R) (∑ σ : Equiv.Perm n, w σ) 1)
    (hw3 : ∑ σ : Equiv.Perm n, w σ • Equiv.Perm.permMatrix R σ = M),
    Membership.mem (γ := Set (Matrix n n R))
      ((convexHull R : (a : Set (Matrix n n R)) → Set (Matrix n n R))
          {x : Matrix n n R | ∃ (σ : Equiv.Perm n), Equiv.Perm.permMatrix R σ = x} :
        Set (Matrix n n R))
      M
⊢ Membership.mem (γ := Set (Matrix n n R))
    ((convexHull R : (a : Set (Matrix n n R)) → Set (Matrix n n R))
        {x : Matrix n n R | ∃ (σ : Equiv.Perm n), Equiv.Perm.permMatrix R σ = x} :
      Set (Matrix n n R))
    M

Tactic:
obtain ⟨w, hw1, hw2, hw3⟩ := exists_eq_sum_perm_of_mem_doublyStochastic hM

Premises used: exists_eq_sum_perm_of_mem_doublyStochastic
-- 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
M : Matrix n n R
hM : M ∈ (↑(doublyStochastic R n) : Set (Matrix n n R))
w : Equiv.Perm n → R
hw1 : ∀ (σ : Equiv.Perm n), 0 ≤ w σ
hw2 : Eq.{u_1 + 1} (α := R) (∑ σ : Equiv.Perm n, w σ) 1
hw3 : ∑ σ : Equiv.Perm n, w σ • Equiv.Perm.permMatrix R σ = M
⊢ ∀ (i : Equiv.Perm n),
    Membership.mem (γ := Set (Matrix n n R)) {x : Matrix n n R | ∃ (σ : Equiv.Perm n), Equiv.Perm.permMatrix R σ = x}
      ((fun (x : Equiv.Perm n) ↦ Equiv.Perm.permMatrix R x) 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
M : Matrix n n R
hM : M ∈ (↑(doublyStochastic R n) : Set (Matrix n n R))
w : Equiv.Perm n → R
hw1 : ∀ (σ : Equiv.Perm n), 0 ≤ w σ
hw2 : Eq.{u_1 + 1} (α := R) (∑ σ : Equiv.Perm n, w σ) 1
hw3 : ∑ σ : Equiv.Perm n, w σ • Equiv.Perm.permMatrix R σ = M
⊢ Membership.mem (γ := Set (Matrix n n R))
    ((convexHull R : (a : Set (Matrix n n R)) → Set (Matrix n n R))
        {x : Matrix n n R | ∃ (σ : Equiv.Perm n), Equiv.Perm.permMatrix R σ = x} :
      Set (Matrix n n R))
    M

Tactic:
exact mem_convexHull_of_exists_fintype w (·.permMatrix R) hw1 hw2 (by simp) hw3

Premises used: Equiv.Perm.permMatrix, mem_convexHull_of_exists_fintype
-- 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
M : Matrix n n R
hM : M ∈ (↑(doublyStochastic R n) : Set (Matrix n n R))
case :
  ∀ (w : Equiv.Perm n → R) (hw1 : ∀ (σ : Equiv.Perm n), 0 ≤ w σ)
    (hw2 : Eq.{u_1 + 1} (α := R) (∑ σ : Equiv.Perm n, w σ) 1)
    (hw3 : ∑ σ : Equiv.Perm n, w σ • Equiv.Perm.permMatrix R σ = M),
    Membership.mem (γ := Set (Matrix n n R))
      ((convexHull R : (a : Set (Matrix n n R)) → Set (Matrix n n R))
          {x : Matrix n n R | ∃ (σ : Equiv.Perm n), Equiv.Perm.permMatrix R σ = x} :
        Set (Matrix n n R))
      M
⊢ Membership.mem (γ := Set (Matrix n n R))
    ((convexHull R : (a : Set (Matrix n n R)) → Set (Matrix n n R))
        {x : Matrix n n R | ∃ (σ : Equiv.Perm n), Equiv.Perm.permMatrix R σ = x} :
      Set (Matrix n n R))
    M

Tactic:
case g2 =>
    obtain ⟨w, hw1, hw2, hw3⟩ := exists_eq_sum_perm_of_mem_doublyStochastic hM
    exact mem_convexHull_of_exists_fintype w (·.permMatrix R) hw1 hw2 (by simp) hw3

Premises used: exists_eq_sum_perm_of_mem_doublyStochastic
-- 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
⊢ Set.extremePoints R (↑(doublyStochastic R n) : Set (Matrix n n R)) =
    {x : Matrix n n R | ∃ (σ : Equiv.Perm n), Equiv.Perm.permMatrix R σ = x}

Tactic:
subset_antisymm ?_ ?_

Premises used: subset_antisymm
-- 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
refine_1 :
  Set.extremePoints R (↑(doublyStochastic R n) : Set (Matrix n n R)) ⊆
    {x : Matrix n n R | ∃ (σ : Equiv.Perm n), Equiv.Perm.permMatrix R σ = x}
refine_2 :
  {x : Matrix n n R | ∃ (σ : Equiv.Perm n), Equiv.Perm.permMatrix R σ = x} ⊆
    Set.extremePoints R (↑(doublyStochastic R n) : Set (Matrix n n R))
⊢ Set.extremePoints R (↑(doublyStochastic R n) : Set (Matrix n n R)) =
    {x : Matrix n n R | ∃ (σ : Equiv.Perm n), Equiv.Perm.permMatrix R σ = x}

Tactic:
refine subset_antisymm ?_ ?_

Premises used: subset_antisymm
-- 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
refine_1 :
  Subset (α := Set (Matrix n n R))
    (Set.extremePoints R
      ((convexHull R : (a : Set (Matrix n n R)) → Set (Matrix n n R))
        {x : Matrix n n R | ∃ (σ : Equiv.Perm n), Equiv.Perm.permMatrix R σ = x}))
    {x : Matrix n n R | ∃ (σ : Equiv.Perm n), Equiv.Perm.permMatrix R σ = x}
⊢ Set.extremePoints R (↑(doublyStochastic R n) : Set (Matrix n n R)) ⊆
    {x : Matrix n n R | ∃ (σ : Equiv.Perm n), Equiv.Perm.permMatrix R σ = x}

Tactic:
rw [doublyStochastic_eq_convexHull_permMatrix]

Premises used: doublyStochastic_eq_convexHull_permMatrix
-- 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
⊢ Subset (α := Set (Matrix n n R))
    (Set.extremePoints R
      ((convexHull R : (a : Set (Matrix n n R)) → Set (Matrix n n R))
        {x : Matrix n n R | ∃ (σ : Equiv.Perm n), Equiv.Perm.permMatrix R σ = x}))
    {x : Matrix n n R | ∃ (σ : Equiv.Perm n), Equiv.Perm.permMatrix R σ = x}

Tactic:
extremePoints_convexHull_subset

Premises used: extremePoints_convexHull_subset
-- 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
⊢ Subset (α := Set (Matrix n n R))
    (Set.extremePoints R
      ((convexHull R : (a : Set (Matrix n n R)) → Set (Matrix n n R))
        {x : Matrix n n R | ∃ (σ : Equiv.Perm n), Equiv.Perm.permMatrix R σ = x}))
    {x : Matrix n n R | ∃ (σ : Equiv.Perm n), Equiv.Perm.permMatrix R σ = x}

Tactic:
exact extremePoints_convexHull_subset

Premises used: extremePoints_convexHull_subset
-- 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
σ : Equiv.Perm n
⊢ Equiv.Perm.permMatrix R σ ∈ Set.extremePoints R (↑(doublyStochastic R n) : Set (Matrix n n R))

Tactic:
⟨permMatrix_mem_doublyStochastic, fun x₁ hx₁ x₂ hx₂ hσ ↦ ?_⟩

Premises used: Set.extremePoints, Set.Mem, setOf, And.intro, permMatrix_mem_doublyStochastic
-- 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
σ : Equiv.Perm n
refine_2 :
  ∀ (x₁ : Matrix n n R) (hx₁ : x₁ ∈ (↑(doublyStochastic R n) : Set (Matrix n n R))) (x₂ : Matrix n n R)
    (hx₂ : x₂ ∈ (↑(doublyStochastic R n) : Set (Matrix n n R))) (hσ : Equiv.Perm.permMatrix R σ ∈ openSegment R x₁ x₂),
    x₁ = Equiv.Perm.permMatrix R σ
⊢ Equiv.Perm.permMatrix R σ ∈ Set.extremePoints R (↑(doublyStochastic R n) : Set (Matrix n n R))

Tactic:
refine ⟨permMatrix_mem_doublyStochastic, fun x₁ hx₁ x₂ hx₂ 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
σ : Equiv.Perm n
x₁ : Matrix n n R
hx₁ : x₁ ∈ (↑(doublyStochastic R n) : Set (Matrix n n R))
x₂ : Matrix n n R
hx₂ : x₂ ∈ (↑(doublyStochastic R n) : Set (Matrix n n R))
hσ : Equiv.Perm.permMatrix R σ ∈ openSegment R x₁ x₂
this : ∀ (i j : n), x₁ i j = x₂ i j
⊢ x₁ = x₂

Tactic:
simpa [← Matrix.ext_iff]

Premises used: Matrix.ext_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
σ : Equiv.Perm n
x₁ : Matrix n n R
hx₁ : x₁ ∈ (↑(doublyStochastic R n) : Set (Matrix n n R))
x₂ : Matrix n n R
hx₂ : x₂ ∈ (↑(doublyStochastic R n) : Set (Matrix n n R))
hσ : Equiv.Perm.permMatrix R σ ∈ openSegment R x₁ x₂
this : ∀ (i j : n), x₁ i j = x₂ i j
⊢ x₁ ∈ (↑(doublyStochastic R n) : Set (Matrix n n R))

Tactic:
obtain rfl : x₁ = x₂ := by simpa [← Matrix.ext_iff]

Premises used: rfl
-- 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
σ : Equiv.Perm n
x₁ : Matrix n n R
hx₁ : x₁ ∈ (↑(doublyStochastic R n) : Set (Matrix n n R))
x₂ : Matrix n n R
hx₂ : x₂ ∈ (↑(doublyStochastic R n) : Set (Matrix n n R))
hσ : Equiv.Perm.permMatrix R σ ∈ openSegment R x₁ x₂
this : ∀ (i j : n), x₁ i j = x₂ i j
hx₃ : x₁ ∈ (↑(doublyStochastic R n) : Set (Matrix n n R))
⊢ Equiv.Perm.permMatrix R σ ∈ openSegment R x₁ x₁

Tactic:
obtain rfl : x₁ = x₂ := by simpa [← Matrix.ext_iff]

Premises used: rfl
-- 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
σ : Equiv.Perm n
x₁ : Matrix n n R
hx₁ : x₁ ∈ (↑(doublyStochastic R n) : Set (Matrix n n R))
x₂ : Matrix n n R
hx₂ : x₂ ∈ (↑(doublyStochastic R n) : Set (Matrix n n R))
hσ : Equiv.Perm.permMatrix R σ ∈ openSegment R x₁ x₂
this : ∀ (i j : n), x₁ i j = x₂ i j
hx₃ : x₁ ∈ (↑(doublyStochastic R n) : Set (Matrix n n R))
hσ₁ : Equiv.Perm.permMatrix R σ ∈ openSegment R x₁ x₁
⊢ ∀ (i j : n), x₁ i j = x₁ i j

Tactic:
obtain rfl : x₁ = x₂ := by simpa [← Matrix.ext_iff]

Premises used: rfl
-- 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
σ : Equiv.Perm n
x₁ : Matrix n n R
hx₁ hx₂ : x₁ ∈ (↑(doublyStochastic R n) : Set (Matrix n n R))
hσ : Equiv.Perm.permMatrix R σ ∈ openSegment R x₁ x₁
this : ∀ (i j : n), x₁ i j = x₁ i j
⊢ x₁ = Equiv.Perm.permMatrix R σ

Tactic:
simp_all
-- 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
σ : Equiv.Perm n
x₁ : Matrix n n R
hx₁ : x₁ ∈ (↑(doublyStochastic R n) : Set (Matrix n n R))
x₂ : Matrix n n R
hx₂ : x₂ ∈ (↑(doublyStochastic R n) : Set (Matrix n n R))
hσ : Equiv.Perm.permMatrix R σ ∈ openSegment R x₁ x₂
refine_2 : ∀ (i j : n), x₁ i j = x₂ i j
⊢ x₁ = Equiv.Perm.permMatrix R σ

Tactic:
suffices ∀ i j : n, x₁ i j = x₂ i j by
    obtain rfl : x₁ = x₂ := by simpa [← Matrix.ext_iff]
    simp_all
-- 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
σ : Equiv.Perm n
x₁ : Matrix n n R
hx₁ : x₁ ∈ (↑(doublyStochastic R n) : Set (Matrix n n R))
x₂ : Matrix n n R
hx₂ : x₂ ∈ (↑(doublyStochastic R n) : Set (Matrix n n R))
hσ : Equiv.Perm.permMatrix R σ ∈ openSegment R x₁ x₂
i j : n
⊢ Equiv.Perm.permMatrix R σ i j ∈ openSegment R (x₁ i j) (x₂ i j)

Tactic:
have h₁ : σ.permMatrix R i j ∈ openSegment R (x₁ i j) (x₂ i j) :=
    image_openSegment _ (entryLinearMap R R i j).toAffineMap x₁ x₂ ▸ ⟨_, hσ, rfl⟩
-- 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
σ : Equiv.Perm n
x₁ : Matrix n n R
hx₁ : x₁ ∈ (↑(doublyStochastic R n) : Set (Matrix n n R))
x₂ : Matrix n n R
hx₂ : x₂ ∈ (↑(doublyStochastic R n) : Set (Matrix n n R))
hσ : Equiv.Perm.permMatrix R σ ∈ openSegment R x₁ x₂
i j : n
h₁ : Equiv.Perm.permMatrix R σ i j ∈ openSegment R (x₁ i j) (x₂ i j)
refine_2 : ∀ (h : x₁ i j ≠ x₂ i j), False
⊢ x₁ i j = x₂ i j

Tactic:
by_contra! 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
σ : Equiv.Perm n
x₁ : Matrix n n R
hx₁ : x₁ ∈ (↑(doublyStochastic R n) : Set (Matrix n n R))
x₂ : Matrix n n R
hx₂ : x₂ ∈ (↑(doublyStochastic R n) : Set (Matrix n n R))
hσ : Equiv.Perm.permMatrix R σ ∈ openSegment R x₁ x₂
i j : n
h₁ : Equiv.Perm.permMatrix R σ i j ∈ openSegment R (x₁ i j) (x₂ i j)
h : x₁ i j ≠ x₂ i j
rw : Set.Ioo (min (x₁ i j) (x₂ i j)) (max (x₁ i j) (x₂ i j)) ⊆ Set.Ioo 0 1
⊢ openSegment R (x₁ i j) (x₂ i j) ⊆ Set.Ioo 0 1

Tactic:
rw [openSegment_eq_Ioo' h]

Premises used: openSegment_eq_Ioo'
-- 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
σ : Equiv.Perm n
x₁ : Matrix n n R
hx₁ : x₁ ∈ (↑(doublyStochastic R n) : Set (Matrix n n R))
x₂ : Matrix n n R
hx₂ : x₂ ∈ (↑(doublyStochastic R n) : Set (Matrix n n R))
hσ : Equiv.Perm.permMatrix R σ ∈ openSegment R x₁ x₂
i j : n
h₁ : Equiv.Perm.permMatrix R σ i j ∈ openSegment R (x₁ i j) (x₂ i j)
h : x₁ i j ≠ x₂ i j
ha : 0 ≤ min (x₁ i j) (x₂ i j)
hb : max (x₁ i j) (x₂ i j) ≤ 1
⊢ Set.Ioo (min (x₁ i j) (x₂ i j)) (max (x₁ i j) (x₂ i j)) ⊆ Set.Ioo 0 1

Tactic:
apply Set.Ioo_subset_Ioo

Premises used: Set.Ioo_subset_Ioo
-- 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
σ : Equiv.Perm n
x₁ : Matrix n n R
hx₁ : x₁ ∈ (↑(doublyStochastic R n) : Set (Matrix n n R))
x₂ : Matrix n n R
hx₂ : x₂ ∈ (↑(doublyStochastic R n) : Set (Matrix n n R))
hσ : Equiv.Perm.permMatrix R σ ∈ openSegment R x₁ x₂
i j : n
h₁ : Equiv.Perm.permMatrix R σ i j ∈ openSegment R (x₁ i j) (x₂ i j)
h : x₁ i j ≠ x₂ i j
⊢ 0 ≤ min (x₁ i j) (x₂ i j)

Tactic:
simp_all [nonneg_of_mem_doublyStochastic, le_one_of_mem_doublyStochastic]

Premises used: nonneg_of_mem_doublyStochastic, le_one_of_mem_doublyStochastic
-- 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
σ : Equiv.Perm n
x₁ : Matrix n n R
hx₁ : x₁ ∈ (↑(doublyStochastic R n) : Set (Matrix n n R))
x₂ : Matrix n n R
hx₂ : x₂ ∈ (↑(doublyStochastic R n) : Set (Matrix n n R))
hσ : Equiv.Perm.permMatrix R σ ∈ openSegment R x₁ x₂
i j : n
h₁ : Equiv.Perm.permMatrix R σ i j ∈ openSegment R (x₁ i j) (x₂ i j)
h : x₁ i j ≠ x₂ i j
⊢ max (x₁ i j) (x₂ i j) ≤ 1

Tactic:
simp_all [nonneg_of_mem_doublyStochastic, le_one_of_mem_doublyStochastic]

Premises used: nonneg_of_mem_doublyStochastic, le_one_of_mem_doublyStochastic
-- 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
σ : Equiv.Perm n
x₁ : Matrix n n R
hx₁ : x₁ ∈ (↑(doublyStochastic R n) : Set (Matrix n n R))
x₂ : Matrix n n R
hx₂ : x₂ ∈ (↑(doublyStochastic R n) : Set (Matrix n n R))
hσ : Equiv.Perm.permMatrix R σ ∈ openSegment R x₁ x₂
i j : n
h₁ : Equiv.Perm.permMatrix R σ i j ∈ openSegment R (x₁ i j) (x₂ i j)
h : x₁ i j ≠ x₂ i j
⊢ openSegment R (x₁ i j) (x₂ i j) ⊆ Set.Ioo 0 1

Tactic:
have h₂ : openSegment R (x₁ i j) (x₂ i j) ⊆ Set.Ioo 0 1 := by
    rw [openSegment_eq_Ioo' h]
    apply Set.Ioo_subset_Ioo <;>
    simp_all [nonneg_of_mem_doublyStochastic, le_one_of_mem_doublyStochastic]
-- 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
σ : Equiv.Perm n
x₁ : Matrix n n R
hx₁ : x₁ ∈ (↑(doublyStochastic R n) : Set (Matrix n n R))
x₂ : Matrix n n R
hx₂ : x₂ ∈ (↑(doublyStochastic R n) : Set (Matrix n n R))
hσ : Equiv.Perm.permMatrix R σ ∈ openSegment R x₁ x₂
i j : n
h₁ : Equiv.Perm.permMatrix R σ i j ∈ openSegment R (x₁ i j) (x₂ i j)
h : x₁ i j ≠ x₂ i j
h₂ : openSegment R (x₁ i j) (x₂ i j) ⊆ Set.Ioo 0 1
⊢ Membership.mem (γ := Set R) (Set.Ioo 0 1) (Equiv.Perm.permMatrix R σ i j)

Tactic:
specialize 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
σ : Equiv.Perm n
x₁ : Matrix n n R
hx₁ : x₁ ∈ (↑(doublyStochastic R n) : Set (Matrix n n R))
x₂ : Matrix n n R
hx₂ : x₂ ∈ (↑(doublyStochastic R n) : Set (Matrix n n R))
hσ : Equiv.Perm.permMatrix R σ ∈ openSegment R x₁ x₂
i j : n
h₁ : Equiv.Perm.permMatrix R σ i j ∈ openSegment R (x₁ i j) (x₂ i j)
h : x₁ i j ≠ x₂ i j
h₂ : Membership.mem (γ := Set R) (Set.Ioo 0 1) (Equiv.Perm.permMatrix R σ i j)
⊢ False

Tactic:
aesop
-- Module: Mathlib.Analysis.Convex.Birkhoff
Goal:
n : Type u_2
inst : Fintype n
inst_1 : DecidableEq n
M : Matrix n n ℝ
hM : Membership.mem (γ := Submonoid (Matrix n n ℝ)) (doublyStochastic ℝ n) M
⊢ Membership.mem (γ := Set (Matrix n n ℝ))
    ((convexHull ℝ : (a : Set (Matrix n n ℝ)) → Set (Matrix n n ℝ))
        {x : Matrix n n ℝ | ∃ (σ : Equiv.Perm n), Equiv.Perm.permMatrix ℝ σ = x} :
      Set (Matrix n n ℝ))
    M

Tactic:
rw [← SetLike.mem_coe, doublyStochastic_eq_convexHull_permMatrix] at hM

Premises used: doublyStochastic_eq_convexHull_permMatrix, SetLike.mem_coe
-- Module: Mathlib.Analysis.Convex.Birkhoff
Goal:
n : Type u_2
inst : Fintype n
inst_1 : DecidableEq n
M : Matrix n n ℝ
hM :
  Membership.mem (γ := Set (Matrix n n ℝ))
    ((convexHull ℝ : (a : Set (Matrix n n ℝ)) → Set (Matrix n n ℝ))
        {x : Matrix n n ℝ | ∃ (σ : Equiv.Perm n), Equiv.Perm.permMatrix ℝ σ = x} :
      Set (Matrix n n ℝ))
    M
⊢ Subset.{u_2} (α := Set (Matrix n n ℝ)) {x : Matrix n n ℝ | ∃ (σ : Equiv.Perm n), Equiv.Perm.permMatrix ℝ σ = x}
    Set.univ

Tactic:
simp
-- Module: Mathlib.Analysis.Convex.Birkhoff
Goal:
n : Type u_2
inst : Fintype n
inst_1 : DecidableEq n
M : Matrix n n ℝ
hM :
  Membership.mem (γ := Set (Matrix n n ℝ))
    ((convexHull ℝ : (a : Set (Matrix n n ℝ)) → Set (Matrix n n ℝ))
        {x : Matrix n n ℝ | ∃ (σ : Equiv.Perm n), Equiv.Perm.permMatrix ℝ σ = x} :
      Set (Matrix n n ℝ))
    M
have : ∀ (σ : Equiv.Perm n) (hσ : ‖M‖ ≤ ‖Equiv.Perm.permMatrix ℝ σ‖), ‖M‖ ≤ 1
⊢ ‖M‖ ≤ 1

Tactic:
have ⟨_, ⟨σ, rfl⟩, hσ⟩ := convexOn_univ_norm.exists_ge_of_mem_convexHull (by simp) hM
-- Module: Mathlib.Analysis.Convex.Birkhoff
Goal:
n : Type u_2
inst : Fintype n
inst_1 : DecidableEq n
M : Matrix n n ℝ
hM :
  Membership.mem (γ := Set (Matrix n n ℝ))
    ((convexHull ℝ : (a : Set (Matrix n n ℝ)) → Set (Matrix n n ℝ))
        {x : Matrix n n ℝ | ∃ (σ : Equiv.Perm n), Equiv.Perm.permMatrix ℝ σ = x} :
      Set (Matrix n n ℝ))
    M
σ : Equiv.Perm n
hσ : ‖M‖ ≤ ‖Equiv.Perm.permMatrix ℝ σ‖
⊢ ‖M‖ ≤ 1

Tactic:
hσ.trans (permMatrix_l2_opNorm_le _)

Premises used: Matrix.permMatrix_l2_opNorm_le, LE.le.trans
-- Module: Mathlib.Analysis.Convex.Birkhoff
Goal:
n : Type u_2
inst : Fintype n
inst_1 : DecidableEq n
M : Matrix n n ℝ
hM :
  Membership.mem (γ := Set (Matrix n n ℝ))
    ((convexHull ℝ : (a : Set (Matrix n n ℝ)) → Set (Matrix n n ℝ))
        {x : Matrix n n ℝ | ∃ (σ : Equiv.Perm n), Equiv.Perm.permMatrix ℝ σ = x} :
      Set (Matrix n n ℝ))
    M
σ : Equiv.Perm n
hσ : ‖M‖ ≤ ‖Equiv.Perm.permMatrix ℝ σ‖
⊢ ‖M‖ ≤ 1

Tactic:
exact hσ.trans (permMatrix_l2_opNorm_le _)

Premises used: Matrix.permMatrix_l2_opNorm_le, LE.le.trans
-- Module: Mathlib.Analysis.Convex.Body
Goal:
V : Type u_1
inst : TopologicalSpace V
inst_1 : AddCommGroup V
inst_2 : Module ℝ V
K L : ConvexBody V
h : K.carrier = L.carrier
mk :
  ∀ (carrier : Set V) (convex' : Convex ℝ carrier) (isCompact' : IsCompact carrier) (nonempty' : carrier.Nonempty)
    (h :
      { carrier := carrier, convex' := convex', isCompact' := isCompact', nonempty' := nonempty' :
            ConvexBody V }.carrier =
        L.carrier),
    { carrier := carrier, convex' := convex', isCompact' := isCompact', nonempty' := nonempty' : ConvexBody V } = L
⊢ K = L

Tactic:
cases K
-- Module: Mathlib.Analysis.Convex.Body
Goal:
V : Type u_1
inst : TopologicalSpace V
inst_1 : AddCommGroup V
inst_2 : Module ℝ V
L : ConvexBody V
carrier : Set V
convex' : Convex ℝ carrier
isCompact' : IsCompact carrier
nonempty' : carrier.Nonempty
h :
  { carrier := carrier, convex' := convex', isCompact' := isCompact', nonempty' := nonempty' : ConvexBody V }.carrier =
    L.carrier
mk :
  ∀ (carrier_1 : Set V) (convex'_1 : Convex ℝ carrier_1) (isCompact'_1 : IsCompact carrier_1)
    (nonempty'_1 : carrier_1.Nonempty)
    (h :
      { carrier := carrier, convex' := convex', isCompact' := isCompact', nonempty' := nonempty' :
            ConvexBody V }.carrier =
        { carrier := carrier_1, convex' := convex'_1, isCompact' := isCompact'_1, nonempty' := nonempty'_1 :
            ConvexBody V }.carrier),
    { carrier := carrier, convex' := convex', isCompact' := isCompact', nonempty' := nonempty' : ConvexBody V } =
      { carrier := carrier_1, convex' := convex'_1, isCompact' := isCompact'_1, nonempty' := nonempty'_1 }
⊢ { carrier := carrier, convex' := convex', isCompact' := isCompact', nonempty' := nonempty' : ConvexBody V } = L

Tactic:
cases L