awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Matrix.Stochastic
Goal:
R_1 : Type u_1
n_1 : Type u_2
inst : Fintype n_1
inst_1 : DecidableEq n_1
inst_2 : Semiring R_1
inst_3 : PartialOrder R_1
inst_4 : IsOrderedRing R_1
M_1 : Matrix n_1 n_1 R_1
x : n_1 → R_1
R : Type u_3
n : Type u_4
inst_5 : Fintype n
inst_6 : DecidableEq n
inst_7 : Semiring R
inst_8 : PartialOrder R
inst_9 : IsOrderedRing R
M N : Matrix n n R
hM : Membership.mem (γ := Set (Matrix n n R)) {M : Matrix n n R | (∀ (i j : n), 0 ≤ M i j) ∧ M *ᵥ 1 = 1} M
hN : Membership.mem (γ := Set (Matrix n n R)) {M : Matrix n n R | (∀ (i j : n), 0 ≤ M i j) ∧ M *ᵥ 1 = 1} N
rw : M *ᵥ N *ᵥ 1 = 1
rw₁ : M *ᵥ 1 = 1
rw₂ rw₃ : Eq (α := n → R) 1 1
⊢ (M * N) *ᵥ 1 = 1

Tactic:
rw [← mulVec_mulVec, hN.2, hM.2]

Premises used: And.right, Matrix.mulVec_mulVec
-- Module: Mathlib.LinearAlgebra.Matrix.Stochastic
Goal:
R_1 : Type u_1
n_1 : Type u_2
inst : Fintype n_1
inst_1 : DecidableEq n_1
inst_2 : Semiring R_1
inst_3 : PartialOrder R_1
inst_4 : IsOrderedRing R_1
M : Matrix n_1 n_1 R_1
x : n_1 → R_1
R : Type u_3
n : Type u_4
inst_5 : Fintype n
inst_6 : DecidableEq n
inst_7 : Semiring R
inst_8 : PartialOrder R
inst_9 : IsOrderedRing R
⊢ Membership.mem (γ := Set (Matrix n n R)) {M : Matrix n n R | (∀ (i j : n), 0 ≤ M i j) ∧ M *ᵥ 1 = 1} 1

Tactic:
simp [zero_le_one_elem]

Premises used: Matrix.zero_le_one_elem
-- Module: Mathlib.LinearAlgebra.Matrix.Stochastic
Goal:
R : Type u_1
n : Type u_2
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : Semiring R
inst_3 : PartialOrder R
inst_4 : IsOrderedRing R
M : Matrix n n R
⊢ Membership.mem (γ := Submonoid (Matrix n n R)) (rowStochastic R n) M ↔ (∀ (i j : n), 0 ≤ M i j) ∧ M *ᵥ 1 = 1

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf
-- Module: Mathlib.LinearAlgebra.Matrix.Stochastic
Goal:
R : Type u_1
n : Type u_2
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : Semiring R
inst_3 : PartialOrder R
inst_4 : IsOrderedRing R
M : Matrix n n R
⊢ Membership.mem (γ := Submonoid (Matrix n n R)) (rowStochastic R n) M ↔
    (∀ (i j : n), 0 ≤ M i j) ∧ ∀ (i : n), Eq.{u_1 + 1} (α := R) (∑ j : n, M i j) 1

Tactic:
simp [funext_iff, rowStochastic, mulVec, dotProduct]

Premises used: dotProduct, funext_iff, Matrix.rowStochastic, Matrix.mulVec
-- Module: Mathlib.LinearAlgebra.Matrix.Stochastic
Goal:
R : Type u_1
n : Type u_2
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : Semiring R
inst_3 : PartialOrder R
inst_4 : IsOrderedRing R
M : Matrix n n R
hM : Membership.mem (γ := Submonoid (Matrix n n R)) (rowStochastic R n) M
i j : n
⊢ 0 ≤ M i j

Tactic:
hM.1 _ _

Premises used: And.left
-- Module: Mathlib.LinearAlgebra.Matrix.Stochastic
Goal:
R : Type u_1
n : Type u_2
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : Semiring R
inst_3 : PartialOrder R
inst_4 : IsOrderedRing R
M : Matrix n n R
hM : Membership.mem (γ := Submonoid (Matrix n n R)) (rowStochastic R n) M
i : n
⊢ Eq.{u_1 + 1} (α := R) (∑ j : n, M i j) 1

Tactic:
(mem_rowStochastic_iff_sum.1 hM).2 _

Premises used: Matrix.mem_rowStochastic_iff_sum, And.right, Iff.mp
-- Module: Mathlib.LinearAlgebra.Matrix.Stochastic
Goal:
R : Type u_1
n : Type u_2
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : Semiring R
inst_3 : PartialOrder R
inst_4 : IsOrderedRing R
M : Matrix n n R
hM : Membership.mem (γ := Submonoid (Matrix n n R)) (rowStochastic R n) M
⊢ M *ᵥ 1 = 1

Tactic:
(mem_rowStochastic.1 hM).2

Premises used: And.right, Iff.mp, Matrix.mem_rowStochastic
-- Module: Mathlib.LinearAlgebra.Matrix.Stochastic
Goal:
R : Type u_1
n : Type u_2
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : Semiring R
inst_3 : PartialOrder R
inst_4 : IsOrderedRing R
M : Matrix n n R
hM : Membership.mem (γ := Submonoid (Matrix n n R)) (rowStochastic R n) M
i j : n
rw : M i j ≤ ∑ j : n, M i j
⊢ M i j ≤ 1

Tactic:
rw [← sum_row_of_mem_rowStochastic hM i]

Premises used: Matrix.sum_row_of_mem_rowStochastic
-- Module: Mathlib.LinearAlgebra.Matrix.Stochastic
Goal:
R : Type u_1
n : Type u_2
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : Semiring R
inst_3 : PartialOrder R
inst_4 : IsOrderedRing R
M : Matrix n n R
hM : Membership.mem (γ := Submonoid (Matrix n n R)) (rowStochastic R n) M
i j : n
⊢ M i j ≤ ∑ j : n, M i j

Tactic:
single_le_sum (fun k _ => hM.1 _ k) (mem_univ j)

Premises used: Finset.mem_univ, And.left, Finset.single_le_sum
-- Module: Mathlib.LinearAlgebra.Matrix.Stochastic
Goal:
R : Type u_1
n : Type u_2
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : Semiring R
inst_3 : PartialOrder R
inst_4 : IsOrderedRing R
M : Matrix n n R
hM : Membership.mem (γ := Submonoid (Matrix n n R)) (rowStochastic R n) M
i j : n
⊢ M i j ≤ ∑ j : n, M i j

Tactic:
exact single_le_sum (fun k _ => hM.1 _ k) (mem_univ j)

Premises used: Finset.mem_univ, And.left, Finset.single_le_sum
-- Module: Mathlib.LinearAlgebra.Matrix.Stochastic
Goal:
R : Type u_1
n : Type u_2
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : Semiring R
inst_3 : PartialOrder R
inst_4 : IsOrderedRing R
M : Matrix n n R
x : n → R
hM : Membership.mem (γ := Submonoid (Matrix n n R)) (rowStochastic R n) M
hx : ∀ (i : n), 0 ≤ x i
j : n
simp : LE.le.{u_1} (α := R) 0 (∑ x_1 : n, x x_1 * M x_1 j)
⊢ 0 ≤ (x ᵥ* M) j

Tactic:
simp only [Matrix.vecMul, dotProduct]

Premises used: dotProduct, Matrix.vecMul
-- Module: Mathlib.LinearAlgebra.Matrix.Stochastic
Goal:
R : Type u_1
n : Type u_2
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : Semiring R
inst_3 : PartialOrder R
inst_4 : IsOrderedRing R
M : Matrix n n R
x : n → R
hM : Membership.mem (γ := Submonoid (Matrix n n R)) (rowStochastic R n) M
hx : ∀ (i : n), 0 ≤ x i
j : n
h : ∀ (i : n), Membership.mem (γ := Finset n) univ i → 0 ≤ x i * M i j
⊢ LE.le.{u_1} (α := R) 0 (∑ x_1 : n, x x_1 * M x_1 j)

Tactic:
apply Finset.sum_nonneg

Premises used: Finset.sum_nonneg
-- Module: Mathlib.LinearAlgebra.Matrix.Stochastic
Goal:
R : Type u_1
n : Type u_2
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : Semiring R
inst_3 : PartialOrder R
inst_4 : IsOrderedRing R
M : Matrix n n R
x : n → R
hM : Membership.mem (γ := Submonoid (Matrix n n R)) (rowStochastic R n) M
hx : ∀ (i : n), 0 ≤ x i
j k : n
h : Membership.mem (γ := Finset n) univ k → 0 ≤ x k * M k j
⊢ Membership.mem (γ := Finset n) univ k → 0 ≤ x k * M k j

Tactic:
_
-- Module: Mathlib.LinearAlgebra.Matrix.Stochastic
Goal:
R : Type u_1
n : Type u_2
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : Semiring R
inst_3 : PartialOrder R
inst_4 : IsOrderedRing R
M : Matrix n n R
x : n → R
hM : Membership.mem (γ := Submonoid (Matrix n n R)) (rowStochastic R n) M
hx : ∀ (i : n), 0 ≤ x i
j k : n
h_1 : Membership.mem (γ := Finset n) univ k
h : 0 ≤ M k j
⊢ 0 ≤ x k * M k j

Tactic:
apply mul_nonneg (hx k)

Premises used: mul_nonneg
-- Module: Mathlib.LinearAlgebra.Matrix.Stochastic
Goal:
R : Type u_1
n : Type u_2
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : Semiring R
inst_3 : PartialOrder R
inst_4 : IsOrderedRing R
M : Matrix n n R
x : n → R
hM : Membership.mem (γ := Submonoid (Matrix n n R)) (rowStochastic R n) M
hx : ∀ (i : n), 0 ≤ x i
j k : n
h : Membership.mem (γ := Finset n) univ k
⊢ 0 ≤ M k j

Tactic:
nonneg_of_mem_rowStochastic hM

Premises used: Matrix.nonneg_of_mem_rowStochastic
-- Module: Mathlib.LinearAlgebra.Matrix.Stochastic
Goal:
R : Type u_1
n : Type u_2
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : Semiring R
inst_3 : PartialOrder R
inst_4 : IsOrderedRing R
M : Matrix n n R
x : n → R
hM : Membership.mem (γ := Submonoid (Matrix n n R)) (rowStochastic R n) M
hx : ∀ (i : n), 0 ≤ x i
j k : n
h : Membership.mem (γ := Finset n) univ k
⊢ 0 ≤ M k j

Tactic:
exact nonneg_of_mem_rowStochastic hM

Premises used: Matrix.nonneg_of_mem_rowStochastic
-- Module: Mathlib.LinearAlgebra.Matrix.Stochastic
Goal:
R : Type u_1
n : Type u_2
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : Semiring R
inst_3 : PartialOrder R
inst_4 : IsOrderedRing R
M : Matrix n n R
x : n → R
hM : Membership.mem (γ := Submonoid (Matrix n n R)) (rowStochastic R n) M
hx : ∀ (i : n), 0 ≤ x i
j : n
simp : LE.le.{u_1} (α := R) 0 (∑ x_1 : n, M j x_1 * x x_1)
⊢ 0 ≤ (M *ᵥ x) j

Tactic:
simp only [Matrix.mulVec, dotProduct]

Premises used: dotProduct, Matrix.mulVec
-- Module: Mathlib.LinearAlgebra.Matrix.Stochastic
Goal:
R : Type u_1
n : Type u_2
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : Semiring R
inst_3 : PartialOrder R
inst_4 : IsOrderedRing R
M : Matrix n n R
x : n → R
hM : Membership.mem (γ := Submonoid (Matrix n n R)) (rowStochastic R n) M
hx : ∀ (i : n), 0 ≤ x i
j : n
h : ∀ (i : n), Membership.mem (γ := Finset n) univ i → 0 ≤ M j i * x i
⊢ LE.le.{u_1} (α := R) 0 (∑ x_1 : n, M j x_1 * x x_1)

Tactic:
apply Finset.sum_nonneg

Premises used: Finset.sum_nonneg
-- Module: Mathlib.LinearAlgebra.Matrix.Stochastic
Goal:
R : Type u_1
n : Type u_2
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : Semiring R
inst_3 : PartialOrder R
inst_4 : IsOrderedRing R
M : Matrix n n R
x : n → R
hM : Membership.mem (γ := Submonoid (Matrix n n R)) (rowStochastic R n) M
hx : ∀ (i : n), 0 ≤ x i
j k : n
h : Membership.mem (γ := Finset n) univ k → 0 ≤ M j k * x k
⊢ Membership.mem (γ := Finset n) univ k → 0 ≤ M j k * x k

Tactic:
_
-- Module: Mathlib.LinearAlgebra.Matrix.Stochastic
Goal:
R : Type u_1
n : Type u_2
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : Semiring R
inst_3 : PartialOrder R
inst_4 : IsOrderedRing R
M : Matrix n n R
x : n → R
hM : Membership.mem (γ := Submonoid (Matrix n n R)) (rowStochastic R n) M
hx : ∀ (i : n), 0 ≤ x i
j k : n
h : Membership.mem (γ := Finset n) univ k
⊢ 0 ≤ M j k * x k

Tactic:
Left.mul_nonneg ?_ (hx k)

Premises used: Left.mul_nonneg
-- Module: Mathlib.LinearAlgebra.Matrix.Stochastic
Goal:
R : Type u_1
n : Type u_2
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : Semiring R
inst_3 : PartialOrder R
inst_4 : IsOrderedRing R
M : Matrix n n R
x : n → R
hM : Membership.mem (γ := Submonoid (Matrix n n R)) (rowStochastic R n) M
hx : ∀ (i : n), 0 ≤ x i
j k : n
h_1 : Membership.mem (γ := Finset n) univ k
h : 0 ≤ M j k
⊢ 0 ≤ M j k * x k

Tactic:
refine Left.mul_nonneg ?_ (hx k)

Premises used: Left.mul_nonneg
-- Module: Mathlib.LinearAlgebra.Matrix.Stochastic
Goal:
R : Type u_1
n : Type u_2
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : Semiring R
inst_3 : PartialOrder R
inst_4 : IsOrderedRing R
M : Matrix n n R
x : n → R
hM : Membership.mem (γ := Submonoid (Matrix n n R)) (rowStochastic R n) M
hx : ∀ (i : n), 0 ≤ x i
j k : n
h : Membership.mem (γ := Finset n) univ k
⊢ 0 ≤ M j k

Tactic:
nonneg_of_mem_rowStochastic hM

Premises used: Matrix.nonneg_of_mem_rowStochastic
-- Module: Mathlib.LinearAlgebra.Matrix.Stochastic
Goal:
R : Type u_1
n : Type u_2
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : Semiring R
inst_3 : PartialOrder R
inst_4 : IsOrderedRing R
M : Matrix n n R
x : n → R
hM : Membership.mem (γ := Submonoid (Matrix n n R)) (rowStochastic R n) M
hx : ∀ (i : n), 0 ≤ x i
j k : n
h : Membership.mem (γ := Finset n) univ k
⊢ 0 ≤ M j k

Tactic:
exact nonneg_of_mem_rowStochastic hM

Premises used: Matrix.nonneg_of_mem_rowStochastic
-- Module: Mathlib.LinearAlgebra.Matrix.Stochastic
Goal:
R : Type u_1
n : Type u_2
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : Semiring R
inst_3 : PartialOrder R
inst_4 : IsOrderedRing R
M : Matrix n n R
x : n → R
hM : Membership.mem (γ := Submonoid (Matrix n n R)) (rowStochastic R n) M
hx : x ⬝ᵥ 1 = 1
rw : x ⬝ᵥ M *ᵥ 1 = 1
rw₁ : x ⬝ᵥ 1 = 1
rw₂ rw₃ : Eq.{u_1 + 1} (α := R) 1 1
⊢ x ᵥ* M ⬝ᵥ 1 = 1

Tactic:
rw [← dotProduct_mulVec, hM.2, hx]

Premises used: And.right, Matrix.dotProduct_mulVec
-- Module: Mathlib.LinearAlgebra.Matrix.Stochastic
Goal:
R : Type u_1
n : Type u_2
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : Semiring R
inst_3 : PartialOrder R
inst_4 : IsOrderedRing R
x : Matrix n n R
hx : x ∈ (↑(rowStochastic R n) : Set (Matrix n n R))
y : Matrix n n R
hy : y ∈ (↑(rowStochastic R n) : Set (Matrix n n R))
a b : R
ha : 0 ≤ a
hb : 0 ≤ b
h : a + b = 1
simp :
  ∀ (hx : (∀ (i j : n), 0 ≤ x i j) ∧ ∀ (i : n), Eq.{u_1 + 1} (α := R) (∑ j : n, x i j) 1)
    (hy : (∀ (i j : n), 0 ≤ y i j) ∧ ∀ (i : n), Eq.{u_1 + 1} (α := R) (∑ j : n, y i j) 1),
    (∀ (i j : n), 0 ≤ (a • x + b • y) i j) ∧ ∀ (i : n), Eq.{u_1 + 1} (α := R) (∑ j : n, (a • x + b • y) i j) 1
⊢ a • x + b • y ∈ (↑(rowStochastic R n) : Set (Matrix n n R))

Tactic:
simp only [SetLike.mem_coe, mem_rowStochastic_iff_sum] at hx hy ⊢

Premises used: Matrix.mem_rowStochastic_iff_sum, SetLike.mem_coe
-- Module: Mathlib.LinearAlgebra.Matrix.Stochastic
Goal:
R : Type u_1
n : Type u_2
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : Semiring R
inst_3 : PartialOrder R
inst_4 : IsOrderedRing R
x y : Matrix n n R
a b : R
ha : 0 ≤ a
hb : 0 ≤ b
h : a + b = 1
hx : (∀ (i j : n), 0 ≤ x i j) ∧ ∀ (i : n), Eq.{u_1 + 1} (α := R) (∑ j : n, x i j) 1
hy : (∀ (i j : n), 0 ≤ y i j) ∧ ∀ (i : n), Eq.{u_1 + 1} (α := R) (∑ j : n, y i j) 1
⊢ (∀ (i j : n), 0 ≤ (a • x + b • y) i j) ∧ ∀ (i : n), Eq.{u_1 + 1} (α := R) (∑ j : n, (a • x + b • y) i j) 1

Tactic:
simp [add_nonneg, ha, hb, mul_nonneg, hx, hy, sum_add_distrib, ← mul_sum, h]

Premises used: Finset.mul_sum, mul_nonneg, Finset.sum_add_distrib, add_nonneg
-- Module: Mathlib.LinearAlgebra.Matrix.Stochastic
Goal:
R : Type u_1
n : Type u_2
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : Semiring R
inst_3 : PartialOrder R
inst_4 : IsOrderedRing R
σ : Equiv.Perm n
rw :
  (∀ (i j : n), 0 ≤ Equiv.Perm.permMatrix R σ i j) ∧
    ∀ (i : n), Eq.{u_1 + 1} (α := R) (∑ j : n, Equiv.Perm.permMatrix R σ i j) 1
⊢ Membership.mem (γ := Submonoid (Matrix n n R)) (rowStochastic R n) (Equiv.Perm.permMatrix R σ)

Tactic:
rw [mem_rowStochastic_iff_sum]

Premises used: Matrix.mem_rowStochastic_iff_sum
-- Module: Mathlib.LinearAlgebra.Matrix.Stochastic
Goal:
R : Type u_1
n : Type u_2
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : Semiring R
inst_3 : PartialOrder R
inst_4 : IsOrderedRing R
σ : Equiv.Perm n
⊢ (∀ (i j : n), 0 ≤ Equiv.Perm.permMatrix R σ i j) ∧
    ∀ (i : n), Eq.{u_1 + 1} (α := R) (∑ j : n, Equiv.Perm.permMatrix R σ i j) 1

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

Premises used: And.intro
-- Module: Mathlib.LinearAlgebra.Matrix.Stochastic
Goal:
R : Type u_1
n : Type u_2
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : Semiring R
inst_3 : PartialOrder R
inst_4 : IsOrderedRing R
σ : Equiv.Perm n
refine : ∀ (i j : n), 0 ≤ Equiv.Perm.permMatrix R σ i j
refine₁ : ∀ (i : n), Eq.{u_1 + 1} (α := R) (∑ j : n, Equiv.Perm.permMatrix R σ i j) 1
⊢ (∀ (i j : n), 0 ≤ Equiv.Perm.permMatrix R σ i j) ∧
    ∀ (i : n), Eq.{u_1 + 1} (α := R) (∑ j : n, Equiv.Perm.permMatrix R σ i j) 1

Tactic:
refine ⟨fun i j => ?g1, ?g2⟩
-- Module: Mathlib.LinearAlgebra.Matrix.Stochastic
Goal:
R : Type u_1
n : Type u_2
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : Semiring R
inst_3 : PartialOrder R
inst_4 : IsOrderedRing R
σ : Equiv.Perm n
i j : n
⊢ 0 ≤ Equiv.Perm.permMatrix R σ i j

Tactic:
aesop
-- Module: Mathlib.LinearAlgebra.Matrix.Stochastic
Goal:
R : Type u_1
n : Type u_2
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : Semiring R
inst_3 : PartialOrder R
inst_4 : IsOrderedRing R
σ : Equiv.Perm n
i j : n
⊢ 0 ≤ Equiv.Perm.permMatrix R σ i j

Tactic:
case g1 => aesop
-- Module: Mathlib.LinearAlgebra.Matrix.Stochastic
Goal:
R : Type u_1
n : Type u_2
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : Semiring R
inst_3 : PartialOrder R
inst_4 : IsOrderedRing R
σ : Equiv.Perm n
⊢ ∀ (i : n), Eq.{u_1 + 1} (α := R) (∑ j : n, Equiv.Perm.permMatrix R σ i j) 1

Tactic:
simp [Equiv.toPEquiv_apply]

Premises used: Equiv.toPEquiv_apply
-- Module: Mathlib.LinearAlgebra.Matrix.Stochastic
Goal:
R : Type u_1
n : Type u_2
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : Semiring R
inst_3 : PartialOrder R
inst_4 : IsOrderedRing R
σ : Equiv.Perm n
⊢ ∀ (i : n), Eq.{u_1 + 1} (α := R) (∑ j : n, Equiv.Perm.permMatrix R σ i j) 1

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

Premises used: Equiv.toPEquiv_apply
-- Module: Mathlib.LinearAlgebra.Matrix.Stochastic
Goal:
R_1 : Type u_1
n_1 : Type u_2
inst : Fintype n_1
inst_1 : DecidableEq n_1
inst_2 : Semiring R_1
inst_3 : PartialOrder R_1
inst_4 : IsOrderedRing R_1
M_1 : Matrix n_1 n_1 R_1
x : n_1 → R_1
R : Type u_3
n : Type u_4
inst_5 : Fintype n
inst_6 : DecidableEq n
inst_7 : Semiring R
inst_8 : PartialOrder R
inst_9 : IsOrderedRing R
M N : Matrix n n R
hM : Membership.mem (γ := Set (Matrix n n R)) {M : Matrix n n R | (∀ (i j : n), 0 ≤ M i j) ∧ 1 ᵥ* M = 1} M
hN : Membership.mem (γ := Set (Matrix n n R)) {M : Matrix n n R | (∀ (i j : n), 0 ≤ M i j) ∧ 1 ᵥ* M = 1} N
⊢ Membership.mem (γ := Set (Matrix n n R)) {M : Matrix n n R | (∀ (i j : n), 0 ≤ M i j) ∧ 1 ᵥ* M = 1} (M * N)

Tactic:
Set.mem_sep ?_ ?_

Premises used: Set.Mem, setOf, Set.mem_sep
-- Module: Mathlib.LinearAlgebra.Matrix.Stochastic
Goal:
R_1 : Type u_1
n_1 : Type u_2
inst : Fintype n_1
inst_1 : DecidableEq n_1
inst_2 : Semiring R_1
inst_3 : PartialOrder R_1
inst_4 : IsOrderedRing R_1
M_1 : Matrix n_1 n_1 R_1
x : n_1 → R_1
R : Type u_3
n : Type u_4
inst_5 : Fintype n
inst_6 : DecidableEq n
inst_7 : Semiring R
inst_8 : PartialOrder R
inst_9 : IsOrderedRing R
M N : Matrix n n R
hM : Membership.mem (γ := Set (Matrix n n R)) {M : Matrix n n R | (∀ (i j : n), 0 ≤ M i j) ∧ 1 ᵥ* M = 1} M
hN : Membership.mem (γ := Set (Matrix n n R)) {M : Matrix n n R | (∀ (i j : n), 0 ≤ M i j) ∧ 1 ᵥ* M = 1} N
refine_1 : Membership.mem (γ := Set (Matrix n n R)) (fun (M : Matrix n n R) ↦ ∀ (i j : n), 0 ≤ M i j) (M * N)
refine_2 : 1 ᵥ* (M * N) = 1
⊢ Membership.mem (γ := Set (Matrix n n R)) {M : Matrix n n R | (∀ (i j : n), 0 ≤ M i j) ∧ 1 ᵥ* M = 1} (M * N)

Tactic:
refine Set.mem_sep ?_ ?_

Premises used: Set.mem_sep
-- Module: Mathlib.LinearAlgebra.Matrix.Stochastic
Goal:
R_1 : Type u_1
n_1 : Type u_2
inst : Fintype n_1
inst_1 : DecidableEq n_1
inst_2 : Semiring R_1
inst_3 : PartialOrder R_1
inst_4 : IsOrderedRing R_1
M_1 : Matrix n_1 n_1 R_1
x : n_1 → R_1
R : Type u_3
n : Type u_4
inst_5 : Fintype n
inst_6 : DecidableEq n
inst_7 : Semiring R
inst_8 : PartialOrder R
inst_9 : IsOrderedRing R
M N : Matrix n n R
hM : Membership.mem (γ := Set (Matrix n n R)) {M : Matrix n n R | (∀ (i j : n), 0 ≤ M i j) ∧ 1 ᵥ* M = 1} M
hN : Membership.mem (γ := Set (Matrix n n R)) {M : Matrix n n R | (∀ (i j : n), 0 ≤ M i j) ∧ 1 ᵥ* M = 1} N
i j : n
refine_1 :
  ∀ (i_1 : n),
    Membership.mem (γ := Finset n) univ i_1 →
      0 ≤ HMul.hMul (α := R) ((fun (j : n) ↦ M i j) i_1) ((fun (j_1 : n) ↦ N j_1 j) i_1)
⊢ 0 ≤ (M * N) i j

Tactic:
apply Finset.sum_nonneg

Premises used: Finset.sum_nonneg
-- Module: Mathlib.LinearAlgebra.Matrix.Stochastic
Goal:
R_1 : Type u_1
n_1 : Type u_2
inst : Fintype n_1
inst_1 : DecidableEq n_1
inst_2 : Semiring R_1
inst_3 : PartialOrder R_1
inst_4 : IsOrderedRing R_1
M_1 : Matrix n_1 n_1 R_1
x : n_1 → R_1
R : Type u_3
n : Type u_4
inst_5 : Fintype n
inst_6 : DecidableEq n
inst_7 : Semiring R
inst_8 : PartialOrder R
inst_9 : IsOrderedRing R
M N : Matrix n n R
hM : Membership.mem (γ := Set (Matrix n n R)) {M : Matrix n n R | (∀ (i j : n), 0 ≤ M i j) ∧ 1 ᵥ* M = 1} M
hN : Membership.mem (γ := Set (Matrix n n R)) {M : Matrix n n R | (∀ (i j : n), 0 ≤ M i j) ∧ 1 ᵥ* M = 1} N
i j : n
⊢ ∀ (i_1 : n),
    Membership.mem (γ := Finset n) univ i_1 →
      0 ≤ HMul.hMul (α := R) ((fun (j : n) ↦ M i j) i_1) ((fun (j_1 : n) ↦ N j_1 j) i_1)

Tactic:
grind [mul_nonneg]

Premises used: mul_nonneg
-- Module: Mathlib.LinearAlgebra.Matrix.Stochastic
Goal:
R_1 : Type u_1
n_1 : Type u_2
inst : Fintype n_1
inst_1 : DecidableEq n_1
inst_2 : Semiring R_1
inst_3 : PartialOrder R_1
inst_4 : IsOrderedRing R_1
M_1 : Matrix n_1 n_1 R_1
x : n_1 → R_1
R : Type u_3
n : Type u_4
inst_5 : Fintype n
inst_6 : DecidableEq n
inst_7 : Semiring R
inst_8 : PartialOrder R
inst_9 : IsOrderedRing R
M N : Matrix n n R
hM : Membership.mem (γ := Set (Matrix n n R)) {M : Matrix n n R | (∀ (i j : n), 0 ≤ M i j) ∧ 1 ᵥ* M = 1} M
hN : Membership.mem (γ := Set (Matrix n n R)) {M : Matrix n n R | (∀ (i j : n), 0 ≤ M i j) ∧ 1 ᵥ* M = 1} N
refine_2 : 1 ᵥ* M ᵥ* N = 1
refine_2₁ : 1 ᵥ* N = 1
refine_2₂ refine_2₃ : Eq (α := n → R) 1 1
⊢ 1 ᵥ* (M * N) = 1

Tactic:
rw [← vecMul_vecMul, hM.2, hN.2]

Premises used: And.right, Matrix.vecMul_vecMul
-- Module: Mathlib.LinearAlgebra.Matrix.Stochastic
Goal:
R_1 : Type u_1
n_1 : Type u_2
inst : Fintype n_1
inst_1 : DecidableEq n_1
inst_2 : Semiring R_1
inst_3 : PartialOrder R_1
inst_4 : IsOrderedRing R_1
M : Matrix n_1 n_1 R_1
x : n_1 → R_1
R : Type u_3
n : Type u_4
inst_5 : Fintype n
inst_6 : DecidableEq n
inst_7 : Semiring R
inst_8 : PartialOrder R
inst_9 : IsOrderedRing R
⊢ Membership.mem (γ := Set (Matrix n n R)) {M : Matrix n n R | (∀ (i j : n), 0 ≤ M i j) ∧ 1 ᵥ* M = 1} 1

Tactic:
simp [zero_le_one_elem]

Premises used: Matrix.zero_le_one_elem
-- Module: Mathlib.LinearAlgebra.Matrix.Stochastic
Goal:
R : Type u_1
n : Type u_2
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : Semiring R
inst_3 : PartialOrder R
inst_4 : IsOrderedRing R
M : Matrix n n R
⊢ Membership.mem (γ := Submonoid (Matrix n n R)) (colStochastic R n) M ↔ (∀ (i j : n), 0 ≤ M i j) ∧ 1 ᵥ* M = 1

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf
-- Module: Mathlib.LinearAlgebra.Matrix.Stochastic
Goal:
R : Type u_1
n : Type u_2
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : Semiring R
inst_3 : PartialOrder R
inst_4 : IsOrderedRing R
M : Matrix n n R
⊢ Membership.mem (γ := Submonoid (Matrix n n R)) (colStochastic R n) M ↔
    (∀ (i j : n), 0 ≤ M i j) ∧ ∀ (j : n), Eq.{u_1 + 1} (α := R) (∑ i : n, M i j) 1

Tactic:
simp [funext_iff, colStochastic, vecMul, dotProduct]

Premises used: Matrix.colStochastic, dotProduct, Matrix.vecMul, funext_iff
-- Module: Mathlib.LinearAlgebra.Matrix.Stochastic
Goal:
R : Type u_1
n : Type u_2
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : Semiring R
inst_3 : PartialOrder R
inst_4 : IsOrderedRing R
M : Matrix n n R
hM : Membership.mem (γ := Submonoid (Matrix n n R)) (colStochastic R n) M
i j : n
⊢ 0 ≤ M i j

Tactic:
hM.1 _ _

Premises used: And.left
-- Module: Mathlib.LinearAlgebra.Matrix.Stochastic
Goal:
R : Type u_1
n : Type u_2
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : Semiring R
inst_3 : PartialOrder R
inst_4 : IsOrderedRing R
M : Matrix n n R
hM : Membership.mem (γ := Submonoid (Matrix n n R)) (colStochastic R n) M
i : n
⊢ Eq.{u_1 + 1} (α := R) (∑ j : n, M j i) 1

Tactic:
(mem_colStochastic_iff_sum.1 hM).2 _

Premises used: And.right, Matrix.mem_colStochastic_iff_sum, Iff.mp
-- Module: Mathlib.LinearAlgebra.Matrix.Stochastic
Goal:
R : Type u_1
n : Type u_2
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : Semiring R
inst_3 : PartialOrder R
inst_4 : IsOrderedRing R
M : Matrix n n R
hM : Membership.mem (γ := Submonoid (Matrix n n R)) (colStochastic R n) M
⊢ 1 ᵥ* M = 1

Tactic:
(mem_colStochastic.1 hM).2

Premises used: And.right, Matrix.mem_colStochastic, Iff.mp
-- Module: Mathlib.LinearAlgebra.Matrix.Stochastic
Goal:
R : Type u_1
n : Type u_2
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : Semiring R
inst_3 : PartialOrder R
inst_4 : IsOrderedRing R
M : Matrix n n R
hM : Membership.mem (γ := Submonoid (Matrix n n R)) (colStochastic R n) M
i j : n
rw : M j i ≤ ∑ j : n, M j i
⊢ M j i ≤ 1

Tactic:
rw [← sum_col_of_mem_colStochastic hM i]

Premises used: Matrix.sum_col_of_mem_colStochastic
-- Module: Mathlib.LinearAlgebra.Matrix.Stochastic
Goal:
R : Type u_1
n : Type u_2
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : Semiring R
inst_3 : PartialOrder R
inst_4 : IsOrderedRing R
M : Matrix n n R
hM : Membership.mem (γ := Submonoid (Matrix n n R)) (colStochastic R n) M
i j : n
⊢ M j i ≤ ∑ j : n, M j i

Tactic:
single_le_sum (fun k _ => hM.1 k _) (mem_univ j)

Premises used: Finset.mem_univ, And.left, Finset.single_le_sum
-- Module: Mathlib.LinearAlgebra.Matrix.Stochastic
Goal:
R : Type u_1
n : Type u_2
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : Semiring R
inst_3 : PartialOrder R
inst_4 : IsOrderedRing R
M : Matrix n n R
hM : Membership.mem (γ := Submonoid (Matrix n n R)) (colStochastic R n) M
i j : n
⊢ M j i ≤ ∑ j : n, M j i

Tactic:
exact single_le_sum (fun k _ => hM.1 k _) (mem_univ j)

Premises used: Finset.mem_univ, And.left, Finset.single_le_sum
-- Module: Mathlib.LinearAlgebra.Matrix.Stochastic
Goal:
R : Type u_1
n : Type u_2
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : Semiring R
inst_3 : PartialOrder R
inst_4 : IsOrderedRing R
M : Matrix n n R
x : n → R
hM : Membership.mem (γ := Submonoid (Matrix n n R)) (colStochastic R n) M
hx : ∀ (i : n), 0 ≤ x i
j : n
simp : LE.le.{u_1} (α := R) 0 (∑ x_1 : n, M j x_1 * x x_1)
⊢ 0 ≤ (M *ᵥ x) j

Tactic:
simp only [Matrix.mulVec, dotProduct]

Premises used: dotProduct, Matrix.mulVec