awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
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)) (colStochastic 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)) (colStochastic 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)) (colStochastic 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)) (colStochastic 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_colStochastic hM

Premises used: Matrix.nonneg_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
x : n → R
hM : Membership.mem (γ := Submonoid (Matrix n n R)) (colStochastic 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_colStochastic hM

Premises used: Matrix.nonneg_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
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, 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)) (colStochastic 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)) (colStochastic 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)) (colStochastic 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

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)) (colStochastic 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:
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)) (colStochastic 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_colStochastic hM

Premises used: Matrix.nonneg_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
x : n → R
hM : Membership.mem (γ := Submonoid (Matrix n n R)) (colStochastic 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_colStochastic hM

Premises used: Matrix.nonneg_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
x : n → R
hM : Membership.mem (γ := Submonoid (Matrix n n R)) (colStochastic R n) M
hx : 1 ⬝ᵥ x = 1
rw : 1 ᵥ* M ⬝ᵥ x = 1
rw₁ : 1 ⬝ᵥ x = 1
rw₂ rw₃ : Eq.{u_1 + 1} (α := R) 1 1
⊢ 1 ⬝ᵥ M *ᵥ x = 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
M : Matrix n n R
x : n → R
hA : Membership.mem (γ := Submonoid (Matrix n n R)) (colStochastic R n) M
simp : Eq.{u_1 + 1} (α := R) (∑ x_1 : n, ∑ x_2 : n, M x_1 x_2 * x x_2) (∑ i : n, x i)
⊢ Eq.{u_1 + 1} (α := R) (∑ i : n, (M *ᵥ x) i) (∑ i : n, x i)

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
hA : Membership.mem (γ := Submonoid (Matrix n n R)) (colStochastic R n) M
rw : Eq.{u_1 + 1} (α := R) (∑ y : n, ∑ x_1 : n, M x_1 y * x y) (∑ i : n, x i)
⊢ Eq.{u_1 + 1} (α := R) (∑ x_1 : n, ∑ x_2 : n, M x_1 x_2 * x x_2) (∑ i : n, x i)

Tactic:
rw [Finset.sum_comm]

Premises used: Finset.sum_comm
-- 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
hA : Membership.mem (γ := Submonoid (Matrix n n R)) (colStochastic R n) M
⊢ Eq.{u_1 + 1} (α := R) (∑ y : n, ∑ x_1 : n, M x_1 y * x y) (∑ i : n, x i)

Tactic:
simp [sum_col_of_mem_colStochastic hA, ← Finset.sum_mul]

Premises used: Matrix.sum_col_of_mem_colStochastic, Finset.sum_mul
-- 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 ∈ (↑(colStochastic R n) : Set (Matrix n n R))
y : Matrix n n R
hy : y ∈ (↑(colStochastic 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) ∧ ∀ (j : n), Eq.{u_1 + 1} (α := R) (∑ i : n, x i j) 1)
    (hy : (∀ (i j : n), 0 ≤ y i j) ∧ ∀ (j : n), Eq.{u_1 + 1} (α := R) (∑ i : n, y i j) 1),
    (∀ (i j : n), 0 ≤ (a • x + b • y) i j) ∧ ∀ (j : n), Eq.{u_1 + 1} (α := R) (∑ i : n, (a • x + b • y) i j) 1
⊢ a • x + b • y ∈ (↑(colStochastic R n) : Set (Matrix n n R))

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

Premises used: SetLike.mem_coe, Matrix.mem_colStochastic_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
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) ∧ ∀ (j : n), Eq.{u_1 + 1} (α := R) (∑ i : n, x i j) 1
hy : (∀ (i j : n), 0 ≤ y i j) ∧ ∀ (j : n), Eq.{u_1 + 1} (α := R) (∑ i : n, y i j) 1
⊢ (∀ (i j : n), 0 ≤ (a • x + b • y) i j) ∧ ∀ (j : n), Eq.{u_1 + 1} (α := R) (∑ i : 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) ∧
    ∀ (j : n), Eq.{u_1 + 1} (α := R) (∑ i : n, Equiv.Perm.permMatrix R σ i j) 1
⊢ Membership.mem (γ := Submonoid (Matrix n n R)) (colStochastic R n) (Equiv.Perm.permMatrix R σ)

Tactic:
rw [mem_colStochastic_iff_sum]

Premises used: Matrix.mem_colStochastic_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) ∧
    ∀ (j : n), Eq.{u_1 + 1} (α := R) (∑ i : 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₁ : ∀ (j : n), Eq.{u_1 + 1} (α := R) (∑ i : n, Equiv.Perm.permMatrix R σ i j) 1
⊢ (∀ (i j : n), 0 ≤ Equiv.Perm.permMatrix R σ i j) ∧
    ∀ (j : n), Eq.{u_1 + 1} (α := R) (∑ i : 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
⊢ ∀ (j : n), Eq.{u_1 + 1} (α := R) (∑ i : n, Equiv.Perm.permMatrix R σ i j) 1

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

Premises used: Equiv.toPEquiv_apply, Equiv.eq_symm_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
⊢ ∀ (j : n), Eq.{u_1 + 1} (α := R) (∑ i : n, Equiv.Perm.permMatrix R σ i j) 1

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

Premises used: Equiv.toPEquiv_apply, Equiv.eq_symm_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
M : Matrix n n R
simp : (∀ (i : n), Eq.{u_1 + 1} (α := R) (∑ x : n, M x i) 1) → ((∀ (i j : n), 0 ≤ M j i) ↔ ∀ (i j : n), 0 ≤ M i j)
⊢ Membership.mem (γ := Submonoid (Matrix n n R)) (rowStochastic R n) Mᵀ ↔
    Membership.mem (γ := Submonoid (Matrix n n R)) (colStochastic R n) M

Tactic:
simp only [mem_colStochastic_iff_sum, mem_rowStochastic_iff_sum, transpose_apply,
    and_congr_left_iff]

Premises used: Matrix.mem_rowStochastic_iff_sum, Matrix.mem_colStochastic_iff_sum, and_congr_left_iff, Matrix.transpose_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
M : Matrix n n R
⊢ (∀ (i : n), Eq.{u_1 + 1} (α := R) (∑ x : n, M x i) 1) → ((∀ (i j : n), 0 ≤ M j i) ↔ ∀ (i j : n), 0 ≤ M i j)

Tactic:
fun _ ↦ forall_comm

Premises used: forall_comm
-- 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
⊢ (∀ (i : n), Eq.{u_1 + 1} (α := R) (∑ x : n, M x i) 1) → ((∀ (i j : n), 0 ≤ M j i) ↔ ∀ (i j : n), 0 ≤ M i j)

Tactic:
exact fun _ ↦ forall_comm

Premises used: forall_comm
-- 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
simp : (∀ (j : n), Eq.{u_1 + 1} (α := R) (∑ x : n, M j x) 1) → ((∀ (i j : n), 0 ≤ M j i) ↔ ∀ (i j : n), 0 ≤ M i j)
⊢ Membership.mem (γ := Submonoid (Matrix n n R)) (colStochastic R n) Mᵀ ↔
    Membership.mem (γ := Submonoid (Matrix n n R)) (rowStochastic R n) M

Tactic:
simp only [mem_colStochastic_iff_sum, mem_rowStochastic_iff_sum, transpose_apply,
    and_congr_left_iff]

Premises used: Matrix.mem_rowStochastic_iff_sum, Matrix.mem_colStochastic_iff_sum, and_congr_left_iff, Matrix.transpose_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
M : Matrix n n R
⊢ (∀ (j : n), Eq.{u_1 + 1} (α := R) (∑ x : n, M j x) 1) → ((∀ (i j : n), 0 ≤ M j i) ↔ ∀ (i j : n), 0 ≤ M i j)

Tactic:
fun _ ↦ forall_comm

Premises used: forall_comm
-- 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
⊢ (∀ (j : n), Eq.{u_1 + 1} (α := R) (∑ x : n, M j x) 1) → ((∀ (i j : n), 0 ≤ M j i) ↔ ∀ (i j : n), 0 ≤ M i j)

Tactic:
exact fun _ ↦ forall_comm

Premises used: forall_comm
-- 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 : Type u_3
inst_5 : Fintype m
inst_6 : DecidableEq m
M : Matrix n n R
e₁ e₂ : n ≃ m
hM : Membership.mem (γ := Submonoid (Matrix n n R)) (rowStochastic R n) M
x x_1 : m
⊢ LE.le.{u_1} (α := R) (0 : R) ((reindex e₁ e₂ : (a : Matrix n n R) → Matrix m m R) M x x_1 : R)

Tactic:
simpa using 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 : Type u_3
inst_5 : Fintype m
inst_6 : DecidableEq m
M : Matrix n n R
e₁ e₂ : n ≃ m
hM : Membership.mem (γ := Submonoid (Matrix n n R)) (rowStochastic R n) M
⊢ Eq (α := m → R) (mulVec (n := m) ((reindex e₁ e₂ : (a : Matrix n n R) → Matrix m m R) M) 1) 1

Tactic:
simp [submatrix_mulVec_equiv, hM.2]

Premises used: Matrix.submatrix_mulVec_equiv, And.right
-- 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 : Type u_3
inst_5 : Fintype m
inst_6 : DecidableEq m
M : Matrix n n R
e₁ e₂ : n ≃ m
⊢ Membership.mem (α := Matrix m m R) (γ := Submonoid (Matrix m m R)) (rowStochastic R m)
      ((reindex e₁ e₂ : (a : Matrix n n R) → Matrix m m R) M : Matrix m m R) ↔
    Membership.mem (γ := Submonoid (Matrix n n R)) (rowStochastic R n) M

Tactic:
⟨fun h => ?_, reindex_mem_rowStochastic⟩

Premises used: Iff.intro, Matrix.reindex_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 : Type u_3
inst_5 : Fintype m
inst_6 : DecidableEq m
M : Matrix n n R
e₁ e₂ : n ≃ m
refine :
  ∀
    (h :
      Membership.mem (α := Matrix m m R) (γ := Submonoid (Matrix m m R)) (rowStochastic R m)
        ((reindex e₁ e₂ : (a : Matrix n n R) → Matrix m m R) M : Matrix m m R)),
    Membership.mem (γ := Submonoid (Matrix n n R)) (rowStochastic R n) M
⊢ Membership.mem (α := Matrix m m R) (γ := Submonoid (Matrix m m R)) (rowStochastic R m)
      ((reindex e₁ e₂ : (a : Matrix n n R) → Matrix m m R) M : Matrix m m R) ↔
    Membership.mem (γ := Submonoid (Matrix n n R)) (rowStochastic R n) M

Tactic:
refine ⟨fun h => ?_, reindex_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 : Type u_3
inst_5 : Fintype m
inst_6 : DecidableEq m
M : Matrix n n R
e₁ e₂ : n ≃ m
h :
  Membership.mem (α := Matrix m m R) (γ := Submonoid (Matrix m m R)) (rowStochastic R m)
    ((reindex e₁ e₂ : (a : Matrix n n R) → Matrix m m R) M : Matrix m m R)
⊢ M =
    (reindex e₁.symm e₂.symm : (a : Matrix m m R) → Matrix n n R)
      ((reindex e₁ e₂ : (a : Matrix n n R) → Matrix m m R) M)

Tactic:
simp
-- 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 : Type u_3
inst_5 : Fintype m
inst_6 : DecidableEq m
M : Matrix n n R
e₁ e₂ : n ≃ m
h :
  Membership.mem (α := Matrix m m R) (γ := Submonoid (Matrix m m R)) (rowStochastic R m)
    ((reindex e₁ e₂ : (a : Matrix n n R) → Matrix m m R) M : Matrix m m R)
⊢ M =
    (reindex e₁.symm e₂.symm : (a : Matrix m m R) → Matrix n n R)
      ((reindex e₁ e₂ : (a : Matrix n n R) → Matrix m m R) M)

Tactic:
have : M = (M.reindex e₁ e₂).reindex e₁.symm e₂.symm := by simp
-- 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 : Type u_3
inst_5 : Fintype m
inst_6 : DecidableEq m
M : Matrix n n R
e₁ e₂ : n ≃ m
h :
  Membership.mem (α := Matrix m m R) (γ := Submonoid (Matrix m m R)) (rowStochastic R m)
    ((reindex e₁ e₂ : (a : Matrix n n R) → Matrix m m R) M : Matrix m m R)
this :
  M =
    (reindex e₁.symm e₂.symm : (a : Matrix m m R) → Matrix n n R)
      ((reindex e₁ e₂ : (a : Matrix n n R) → Matrix m m R) M)
rw :
  Membership.mem (α := Matrix n n R) (γ := Submonoid (Matrix n n R)) (rowStochastic R n)
    ((reindex e₁.symm e₂.symm : (a : Matrix m m R) → Matrix n n R)
        ((reindex e₁ e₂ : (a : Matrix n n R) → Matrix m m R) M) :
      Matrix n n R)
⊢ Membership.mem (γ := Submonoid (Matrix n n R)) (rowStochastic R n) M

Tactic:
rw [this]
-- 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 : Type u_3
inst_5 : Fintype m
inst_6 : DecidableEq m
M : Matrix n n R
e₁ e₂ : n ≃ m
h :
  Membership.mem (α := Matrix m m R) (γ := Submonoid (Matrix m m R)) (rowStochastic R m)
    ((reindex e₁ e₂ : (a : Matrix n n R) → Matrix m m R) M : Matrix m m R)
this :
  M =
    (reindex e₁.symm e₂.symm : (a : Matrix m m R) → Matrix n n R)
      ((reindex e₁ e₂ : (a : Matrix n n R) → Matrix m m R) M)
⊢ Membership.mem (α := Matrix n n R) (γ := Submonoid (Matrix n n R)) (rowStochastic R n)
    ((reindex e₁.symm e₂.symm : (a : Matrix m m R) → Matrix n n R)
        ((reindex e₁ e₂ : (a : Matrix n n R) → Matrix m m R) M) :
      Matrix n n R)

Tactic:
reindex_mem_rowStochastic h

Premises used: Set.Mem, setOf, Matrix.reindex_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 : Type u_3
inst_5 : Fintype m
inst_6 : DecidableEq m
M : Matrix n n R
e₁ e₂ : n ≃ m
h :
  Membership.mem (α := Matrix m m R) (γ := Submonoid (Matrix m m R)) (rowStochastic R m)
    ((reindex e₁ e₂ : (a : Matrix n n R) → Matrix m m R) M : Matrix m m R)
this :
  M =
    (reindex e₁.symm e₂.symm : (a : Matrix m m R) → Matrix n n R)
      ((reindex e₁ e₂ : (a : Matrix n n R) → Matrix m m R) M)
⊢ Membership.mem (α := Matrix n n R) (γ := Submonoid (Matrix n n R)) (rowStochastic R n)
    ((reindex e₁.symm e₂.symm : (a : Matrix m m R) → Matrix n n R)
        ((reindex e₁ e₂ : (a : Matrix n n R) → Matrix m m R) M) :
      Matrix n n R)

Tactic:
exact reindex_mem_rowStochastic h

Premises used: Matrix.reindex_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 : Type u_3
inst_5 : Fintype m
inst_6 : DecidableEq m
M : Matrix n n R
e₁ e₂ : n ≃ m
rw :
  Membership.mem (γ := Submonoid (Matrix m m R)) (colStochastic R m)
      ((reindex e₁ e₂ : (a : Matrix n n R) → Matrix m m R) M)ᵀᵀ ↔
    Membership.mem (γ := Submonoid (Matrix n n R)) (colStochastic R n) M
rw₁ :
  Membership.mem (γ := Submonoid (Matrix m m R)) (colStochastic R m)
      ((reindex e₂ e₁ : (a : Matrix n n R) → Matrix m m R) Mᵀ)ᵀ ↔
    Membership.mem (γ := Submonoid (Matrix n n R)) (colStochastic R n) M
rw₂ :
  Membership.mem (α := Matrix m m R) (γ := Submonoid (Matrix m m R)) (rowStochastic R m)
      ((reindex e₂ e₁ : (a : Matrix n n R) → Matrix m m R) Mᵀ : Matrix m m R) ↔
    Membership.mem (γ := Submonoid (Matrix n n R)) (colStochastic R n) M
rw₃ :
  Membership.mem (γ := Submonoid (Matrix n n R)) (rowStochastic R n) Mᵀ ↔
    Membership.mem (γ := Submonoid (Matrix n n R)) (colStochastic R n) M
rw₄ :
  Membership.mem (γ := Submonoid (Matrix n n R)) (colStochastic R n) Mᵀᵀ ↔
    Membership.mem (γ := Submonoid (Matrix n n R)) (colStochastic R n) M
rw₅ rw₆ :
  Membership.mem (γ := Submonoid (Matrix n n R)) (colStochastic R n) M ↔
    Membership.mem (γ := Submonoid (Matrix n n R)) (colStochastic R n) M
⊢ Membership.mem (α := Matrix m m R) (γ := Submonoid (Matrix m m R)) (colStochastic R m)
      ((reindex e₁ e₂ : (a : Matrix n n R) → Matrix m m R) M : Matrix m m R) ↔
    Membership.mem (γ := Submonoid (Matrix n n R)) (colStochastic R n) M

Tactic:
rw [← transpose_transpose (reindex e₁ e₂ M), transpose_reindex,
    transpose_mem_colStochastic_iff_mem_rowStochastic, reindex_mem_rowStochastic_iff,
    ← transpose_mem_colStochastic_iff_mem_rowStochastic, transpose_transpose]

Premises used: Matrix.transpose_transpose, Matrix.reindex_mem_rowStochastic_iff, Matrix.reindex, Matrix.transpose_mem_colStochastic_iff_mem_rowStochastic, DFunLike.coe, Matrix.transpose_reindex
-- Module: Mathlib.LinearAlgebra.Matrix.Swap
Goal:
R : Type u_1
n : Type u_2
inst : Zero R
inst_1 : One R
inst_2 : DecidableEq n
i j : n
⊢ swap R i j = swap R j i

Tactic:
simp only [swap, Equiv.swap_comm]

Premises used: Equiv.swap_comm, Matrix.swap
-- Module: Mathlib.LinearAlgebra.Matrix.Swap
Goal:
R : Type u_1
n : Type u_2
inst : Zero R
inst_1 : One R
inst_2 : DecidableEq n
i j : n
⊢ (swap R i j)ᵀ = swap R i j

Tactic:
simp [swap]

Premises used: Matrix.swap
-- Module: Mathlib.LinearAlgebra.Matrix.Swap
Goal:
R : Type u_1
n : Type u_2
inst : Zero R
inst_1 : One R
inst_2 : DecidableEq n
i j : n
⊢ (swap R i j).IsSymm

Tactic:
transpose_swap i j

Premises used: Matrix.transpose_swap, Matrix.IsSymm