-- Mathlib/Data/Matrix/DoublyStochastic.lean
/-- Any permutation matrix is doubly stochastic. -/
lemma permMatrix_mem_doublyStochastic {σ : Equiv.Perm n} :
    σ.permMatrix R ∈ doublyStochastic R n

Proof state:
R : Type u_1
n : Type u_2
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : OrderedSemiring R
σ : Equiv.Perm n
i j : n
⊢ 0 ≤ Equiv.Perm.permMatrix R σ i j

Tactic:
aesop

Result:
no goals

Proof state:
case g3
R : Type u_1
n : Type u_2
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : OrderedSemiring R
σ : Equiv.Perm n
⊢ ∀ (j : n), ∑ i : n, Equiv.Perm.permMatrix R σ i j = 1

Tactic:
case g3 => simp [Equiv.toPEquiv_apply, ← Equiv.eq_symm_apply]

Result:
no goals

Proof state:
R : Type u_1
n : Type u_2
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : OrderedSemiring R
σ : Equiv.Perm n
⊢ ∀ (i : n), ∑ j : n, Equiv.Perm.permMatrix R σ i j = 1

Tactic:
simp [Equiv.toPEquiv_apply]

Result:
no goals

Proof state:
case g1
R : Type u_1
n : Type u_2
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : OrderedSemiring R
σ : Equiv.Perm n
i j : n
⊢ 0 ≤ Equiv.Perm.permMatrix R σ i j

case g2
R : Type u_1
n : Type u_2
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : OrderedSemiring R
σ : Equiv.Perm n
⊢ ∀ (i : n), ∑ j : n, Equiv.Perm.permMatrix R σ i j = 1

case g3
R : Type u_1
n : Type u_2
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : OrderedSemiring R
σ : Equiv.Perm n
⊢ ∀ (j : n), ∑ i : n, Equiv.Perm.permMatrix R σ i j = 1

Tactic:
case g1 => aesop

Result:
case g2
R : Type u_1
n : Type u_2
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : OrderedSemiring R
σ : Equiv.Perm n
⊢ ∀ (i : n), ∑ j : n, Equiv.Perm.permMatrix R σ i j = 1

case g3
R : Type u_1
n : Type u_2
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : OrderedSemiring R
σ : Equiv.Perm n
⊢ ∀ (j : n), ∑ i : n, Equiv.Perm.permMatrix R σ i j = 1

Proof state:
case g2
R : Type u_1
n : Type u_2
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : OrderedSemiring R
σ : Equiv.Perm n
⊢ ∀ (i : n), ∑ j : n, Equiv.Perm.permMatrix R σ i j = 1

case g3
R : Type u_1
n : Type u_2
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : OrderedSemiring R
σ : Equiv.Perm n
⊢ ∀ (j : n), ∑ i : n, Equiv.Perm.permMatrix R σ i j = 1

Tactic:
case g2 => simp [Equiv.toPEquiv_apply]

Result:
case g3
R : Type u_1
n : Type u_2
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : OrderedSemiring R
σ : Equiv.Perm n
⊢ ∀ (j : n), ∑ i : n, Equiv.Perm.permMatrix R σ i j = 1

Proof state:
R : Type u_1
n : Type u_2
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : OrderedSemiring R
σ : Equiv.Perm n
⊢ Equiv.Perm.permMatrix R σ ∈ doublyStochastic R n

Tactic:
rw [mem_doublyStochastic_iff_sum]

Result:
R : Type u_1
n : Type u_2
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : OrderedSemiring R
σ : Equiv.Perm n
⊢ (∀ (i j : n), 0 ≤ Equiv.Perm.permMatrix R σ i j) ∧
    (∀ (i : n), ∑ j : n, Equiv.Perm.permMatrix R σ i j = 1) ∧ ∀ (j : n), ∑ i : n, Equiv.Perm.permMatrix R σ i j = 1

Proof state:
R : Type u_1
n : Type u_2
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : OrderedSemiring R
σ : Equiv.Perm n
⊢ (∀ (i j : n), 0 ≤ Equiv.Perm.permMatrix R σ i j) ∧
    (∀ (i : n), ∑ j : n, Equiv.Perm.permMatrix R σ i j = 1) ∧ ∀ (j : n), ∑ i : n, Equiv.Perm.permMatrix R σ i j = 1

Tactic:
refine ⟨fun i j => ?g1, ?g2, ?g3⟩

Result:
case g1
R : Type u_1
n : Type u_2
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : OrderedSemiring R
σ : Equiv.Perm n
i j : n
⊢ 0 ≤ Equiv.Perm.permMatrix R σ i j

case g2
R : Type u_1
n : Type u_2
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : OrderedSemiring R
σ : Equiv.Perm n
⊢ ∀ (i : n), ∑ j : n, Equiv.Perm.permMatrix R σ i j = 1

case g3
R : Type u_1
n : Type u_2
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : OrderedSemiring R
σ : Equiv.Perm n
⊢ ∀ (j : n), ∑ i : n, Equiv.Perm.permMatrix R σ i j = 1

Proof state:
R : Type u_1
n : Type u_2
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : OrderedSemiring R
σ : Equiv.Perm n
⊢ ∀ (j : n), ∑ i : n, Equiv.Perm.permMatrix R σ i j = 1

Tactic:
simp [Equiv.toPEquiv_apply, ← Equiv.eq_symm_apply]

Result:
no goals