awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Stochastic (goal)
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
have refine : ∀ (i j : n), 0 ≤ Equiv.Perm.permMatrix R σ i j
Tactic: refine ⟨fun i j => ?g1, ?g2⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Stochastic (goal)
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
⊢ (∀ (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
have refine₁ : ∀ (i : n), Eq.{u_1 + 1} (α := R) (∑ j : n, Equiv.Perm.permMatrix R σ i j) 1
Tactic: refine ⟨fun i j => ?g1, ?g2⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Stochastic (goal)
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)
have refine_1 : Membership.mem (γ := Set (Matrix n n R)) (fun (M : Matrix n n R) ↦ ∀ (i j : n), 0 ≤ M i j) (M * N)
Tactic: refine Set.mem_sep ?_ ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Stochastic (goal)
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)
⊢ Membership.mem (γ := Set (Matrix n n R)) {M : Matrix n n R | (∀ (i j : n), 0 ≤ M i j) ∧ 1 ᵥ* M = 1} (M * N)
have refine_2 : 1 ᵥ* (M * N) = 1
Tactic: refine Set.mem_sep ?_ ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Stochastic (goal)
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
⊢ 0 ≤ (M * N) i j
have 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)
Tactic: apply Finset.sum_nonneg
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Stochastic (goal)
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
⊢ 1 ᵥ* (M * N) = 1
have refine_2 : 1 ᵥ* M ᵥ* N = 1
Tactic: rw [← vecMul_vecMul, hM.2, hN.2]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Stochastic (goal)
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
⊢ 1 ᵥ* (M * N) = 1
have refine_2₁ : 1 ᵥ* N = 1
Tactic: rw [← vecMul_vecMul, hM.2, hN.2]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Stochastic (goal)
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
⊢ 1 ᵥ* (M * N) = 1
have refine_2₂ : Eq (α := n → R) 1 1
Tactic: rw [← vecMul_vecMul, hM.2, hN.2]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Stochastic (goal)
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 ≤ 1
have rw : M j i ≤ ∑ j : n, M j i
Tactic: rw [← sum_col_of_mem_colStochastic hM i]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Stochastic (goal)
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
⊢ 0 ≤ (M *ᵥ x) j
have simp : LE.le.{u_1} (α := R) 0 (∑ x_1 : n, M j x_1 * x x_1)
Tactic: simp only [Matrix.mulVec, dotProduct]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Stochastic (goal)
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
⊢ LE.le.{u_1} (α := R) 0 (∑ x_1 : n, M j x_1 * x x_1)
have h : ∀ (i : n), Membership.mem (γ := Finset n) univ i → 0 ≤ M j i * x i
Tactic: apply Finset.sum_nonneg
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Stochastic (goal)
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
have h : 0 ≤ M j k
Tactic: refine Left.mul_nonneg ?_ (hx k)
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Stochastic (goal)
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
⊢ 0 ≤ (x ᵥ* M) j
have simp : LE.le.{u_1} (α := R) 0 (∑ x_1 : n, x x_1 * M x_1 j)
Tactic: simp only [Matrix.vecMul, dotProduct]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Stochastic (goal)
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
⊢ LE.le.{u_1} (α := R) 0 (∑ x_1 : n, x x_1 * M x_1 j)
have h : ∀ (i : n), Membership.mem (γ := Finset n) univ i → 0 ≤ x i * M i j
Tactic: apply Finset.sum_nonneg
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Stochastic (goal)
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
have h : 0 ≤ M k j
Tactic: refine Left.mul_nonneg (hx k) ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Stochastic (goal)
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
⊢ 1 ⬝ᵥ M *ᵥ x = 1
have rw : 1 ᵥ* M ⬝ᵥ x = 1
Tactic: rw [dotProduct_mulVec, hM.2, hx]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Stochastic (goal)
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
⊢ 1 ⬝ᵥ M *ᵥ x = 1
have rw₂ : Eq.{u_1 + 1} (α := R) 1 1
Tactic: rw [dotProduct_mulVec, hM.2, hx]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Stochastic (goal)
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) (∑ i : n, (M *ᵥ x) i) (∑ i : n, x i)
have simp : Eq.{u_1 + 1} (α := R) (∑ x_1 : n, ∑ x_2 : n, M x_1 x_2 * x x_2) (∑ i : n, x i)
Tactic: simp only [Matrix.mulVec, dotProduct]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Stochastic (goal)
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) (∑ x_1 : n, ∑ x_2 : n, M x_1 x_2 * x x_2) (∑ i : n, x i)
have rw : Eq.{u_1 + 1} (α := R) (∑ y : n, ∑ x_1 : n, M x_1 y * x y) (∑ i : n, x i)
Tactic: rw [Finset.sum_comm]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Stochastic (goal)
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
⊢ a • x + b • y ∈ (↑(colStochastic R n) : Set (Matrix n n R))
have 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
Tactic: simp only [SetLike.mem_coe, mem_colStochastic_iff_sum] at hx hy ⊢
Cleared hypotheses: hx, hy
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Stochastic (goal)
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
⊢ Membership.mem (γ := Submonoid (Matrix n n R)) (colStochastic R n) (Equiv.Perm.permMatrix R σ)
have 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
Tactic: rw [mem_colStochastic_iff_sum]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Stochastic (goal)
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
have refine : ∀ (i j : n), 0 ≤ Equiv.Perm.permMatrix R σ i j
Tactic: refine ⟨fun i j => ?g1, ?g2⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Stochastic (goal)
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
⊢ (∀ (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
have refine₁ : ∀ (j : n), Eq.{u_1 + 1} (α := R) (∑ i : n, Equiv.Perm.permMatrix R σ i j) 1
Tactic: refine ⟨fun i j => ?g1, ?g2⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Stochastic (goal)
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ᵀ ↔
    Membership.mem (γ := Submonoid (Matrix n n R)) (colStochastic R n) M
have 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)
Tactic: simp only [mem_colStochastic_iff_sum, mem_rowStochastic_iff_sum, transpose_apply,
    and_congr_left_iff]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Stochastic (goal)
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ᵀ ↔
    Membership.mem (γ := Submonoid (Matrix n n R)) (rowStochastic R n) M
have 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)
Tactic: simp only [mem_colStochastic_iff_sum, mem_rowStochastic_iff_sum, transpose_apply,
    and_congr_left_iff]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Stochastic (goal)
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
have 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
Tactic: refine ⟨fun h => ?_, reindex_mem_rowStochastic⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Stochastic (hypothesis)
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)
⊢ Membership.mem (γ := Submonoid (Matrix n n R)) (rowStochastic R n) M
have 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)
Tactic: have : M = (M.reindex e₁ e₂).reindex e₁.symm e₂.symm := by simp
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Stochastic (goal)
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 (γ := Submonoid (Matrix n n R)) (rowStochastic R n) M
have 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)
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Stochastic (goal)
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)) (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
have 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
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]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Stochastic (goal)
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
⊢ 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
have 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
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]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Stochastic (goal)
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
⊢ 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
have 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
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]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Stochastic (goal)
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
⊢ 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
have rw₃ : Membership.mem (γ := Submonoid (Matrix n n R)) (rowStochastic R n) Mᵀ ↔
  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]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Stochastic (goal)
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
⊢ 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
have rw₄ : Membership.mem (γ := Submonoid (Matrix n n R)) (colStochastic R n) Mᵀᵀ ↔
  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]