-- 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
h₁ : Equiv.Perm.permMatrix R σ i j ∈ openSegment R (x₁ i j) (x₂ i j)
h : x₁ i j ≠ x₂ i j
h₂ : Equiv.Perm.permMatrix R σ i j ∈ Set.Ioo 0 1
⊢ False

Tactic:
aesop

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

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

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₂
⊢ x₁ = Equiv.Perm.permMatrix R σ ∧ x₂ = Equiv.Perm.permMatrix R σ

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
h₁ : Equiv.Perm.permMatrix R σ i j ∈ openSegment R (x₁ i j) (x₂ i j)
h : x₁ i j ≠ x₂ i j
⊢ False

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]

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)
h : x₁ i j ≠ x₂ i j
h₂ : openSegment R (x₁ i j) (x₂ i j) ⊆ Set.Ioo 0 1
⊢ False

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
⊢ Set.Ioo (x₁ i j ⊓ x₂ i j) (x₁ i j ⊔ x₂ i j) ⊆ Set.Ioo 0 1

Tactic:
apply Set.Ioo_subset_Ioo <;>
simp_all [nonneg_of_mem_doublyStochastic, le_one_of_mem_doublyStochastic]

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₂
⊢ ∀ (i j : n), x₁ i j = x₂ i j

Tactic:
intro i j

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

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
h₁ : Equiv.Perm.permMatrix R σ i j ∈ openSegment R (x₁ i j) (x₂ i j)
⊢ x₁ i j = x₂ i j

Tactic:
by_contra! h

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)
h : x₁ i j ≠ x₂ i j
⊢ False

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₁ = Equiv.Perm.permMatrix R σ ∧ x₂ = Equiv.Perm.permMatrix R σ

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

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₁ 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₁ = Equiv.Perm.permMatrix R σ ∧ x₁ = Equiv.Perm.permMatrix R σ

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
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
⊢ False

Tactic:
specialize h₂ h₁

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)
h : x₁ i j ≠ x₂ i j
h₂ : Equiv.Perm.permMatrix R σ i j ∈ Set.Ioo 0 1
⊢ False

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₁ 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₁ = Equiv.Perm.permMatrix R σ ∧ x₁ = Equiv.Perm.permMatrix R σ

Tactic:
simp_all

Result:
no goals

Proof state:
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)

Tactic:
rintro _ ⟨σ, 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
⊢ Equiv.Perm.permMatrix R σ ∈ Set.extremePoints R ↑(doublyStochastic R n)

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 ↑(doublyStochastic R n) ⊆ {x | ∃ σ, Equiv.Perm.permMatrix R σ = x}

Tactic:
rw [doublyStochastic_eq_convexHull_permMatrix]

Result:
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}