-- Mathlib/Analysis/Convex/Birkhoff.lean
theorem extremePoints_doublyStochastic :
    Set.extremePoints R (doublyStochastic R n) = {σ.permMatrix R | σ : Equiv.Perm n}

Proof state:
case refine_2.intro
R : Type u_1
n : Type u_2
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : LinearOrderedField R
σ : Equiv.Perm n
x₁ : Matrix n n R
hx₁ : x₁ ∈ ↑(doublyStochastic R n)
x₂ : Matrix n n R
hx₂ : x₂ ∈ ↑(doublyStochastic R n)
hσ : Equiv.Perm.permMatrix R σ ∈ openSegment R x₁ x₂
i j : n
⊢ 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⟩

Result:
case refine_2.intro
R : Type u_1
n : Type u_2
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : LinearOrderedField R
σ : Equiv.Perm n
x₁ : Matrix n n R
hx₁ : x₁ ∈ ↑(doublyStochastic R n)
x₂ : Matrix n n R
hx₂ : x₂ ∈ ↑(doublyStochastic R n)
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)
⊢ x₁ i j = x₂ i j

Proof state:
case refine_1
R : Type u_1
n : Type u_2
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : LinearOrderedField R
⊢ Set.extremePoints R ((convexHull R) {x | ∃ σ, Equiv.Perm.permMatrix R σ = x}) ⊆
    {x | ∃ σ, Equiv.Perm.permMatrix R σ = x}

Tactic:
exact extremePoints_convexHull_subset

Result:
no goals

Proof state:
R : Type u_1
n : Type u_2
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : LinearOrderedField R
⊢ Set.extremePoints R ↑(doublyStochastic R n) = {x | ∃ σ, Equiv.Perm.permMatrix R σ = x}

Tactic:
refine subset_antisymm ?_ ?_

Result:
case refine_1
R : Type u_1
n : Type u_2
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : LinearOrderedField R
⊢ Set.extremePoints R ↑(doublyStochastic R n) ⊆ {x | ∃ σ, Equiv.Perm.permMatrix R σ = x}

case refine_2
R : Type u_1
n : Type u_2
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : LinearOrderedField R
⊢ {x | ∃ σ, Equiv.Perm.permMatrix R σ = x} ⊆ Set.extremePoints R ↑(doublyStochastic R n)

Proof state:
R : Type u_1
n : Type u_2
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : LinearOrderedField R
σ : Equiv.Perm n
x₁ : Matrix n n R
hx₁ : x₁ ∈ ↑(doublyStochastic R n)
x₂ : Matrix n n R
hx₂ : x₂ ∈ ↑(doublyStochastic R n)
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:
rw [openSegment_eq_Ioo' h]

Result:
R : Type u_1
n : Type u_2
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : LinearOrderedField R
σ : Equiv.Perm n
x₁ : Matrix n n R
hx₁ : x₁ ∈ ↑(doublyStochastic R n)
x₂ : Matrix n n R
hx₂ : x₂ ∈ ↑(doublyStochastic R n)
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
⊢ Set.Ioo (x₁ i j ⊓ x₂ i j) (x₁ i j ⊔ x₂ i j) ⊆ Set.Ioo 0 1

Proof state:
R : Type u_1
n : Type u_2
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : LinearOrderedField R
σ : Equiv.Perm n
x₁ : Matrix n n R
hx₁ : x₁ ∈ ↑(doublyStochastic R n)
x₂ : Matrix n n R
hx₂ : x₂ ∈ ↑(doublyStochastic R n)
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]

Result:
no goals

Proof state:
case refine_2.intro
R : Type u_1
n : Type u_2
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : LinearOrderedField R
σ : Equiv.Perm n
x₁ : Matrix n n R
hx₁ : x₁ ∈ ↑(doublyStochastic R n)
x₂ : Matrix n n R
hx₂ : x₂ ∈ ↑(doublyStochastic R n)
hσ : Equiv.Perm.permMatrix R σ ∈ openSegment R x₁ x₂
⊢ x₁ = Equiv.Perm.permMatrix R σ ∧ 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

Result:
case refine_2.intro
R : Type u_1
n : Type u_2
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : LinearOrderedField R
σ : Equiv.Perm n
x₁ : Matrix n n R
hx₁ : x₁ ∈ ↑(doublyStochastic R n)
x₂ : Matrix n n R
hx₂ : x₂ ∈ ↑(doublyStochastic R n)
hσ : Equiv.Perm.permMatrix R σ ∈ openSegment R x₁ x₂
⊢ ∀ (i j : n), x₁ i j = x₂ i j