awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Notation (goal)
Goal:
α : Type u_1
x y : α
h : x ≠ y
b : Fin (Nat.succ 0).succ
h' : ![x, y] ((fun (i : Fin (Nat.succ 0).succ) ↦ i) (⟨0, ⋯⟩ : Fin (Nat.succ 0).succ)) = ![x, y] b
refine_2 :
  ∀
    (h' :
      ![x, y] ((fun (i : Fin (Nat.succ 0).succ) ↦ i) (⟨0, ⋯⟩ : Fin (Nat.succ 0).succ)) =
        ![x, y] ((fun (i : Fin (Nat.succ 0).succ) ↦ i) ⟨0, ⋯⟩)),
    Eq (α := Fin (Nat.succ 0).succ) ((fun (i : Fin (Nat.succ 0).succ) ↦ i) ⟨0, ⋯⟩)
      ((fun (i : Fin (Nat.succ 0).succ) ↦ i) ⟨0, ⋯⟩)
⊢ (fun (i : Fin (Nat.succ 0).succ) ↦ i) ⟨0, ⋯⟩ = b
have refine_2₁ : ∀
  (h' :
    ![x, y] ((fun (i : Fin (Nat.succ 0).succ) ↦ i) (⟨0, sorry⟩ : Fin (Nat.succ 0).succ)) =
      ![x, y] ((fun (i : Fin (Nat.succ 0).succ) ↦ i) ⟨1, sorry⟩)),
  Eq (α := Fin (Nat.succ 0).succ) ((fun (i : Fin (Nat.succ 0).succ) ↦ i) ⟨0, sorry⟩)
    ((fun (i : Fin (Nat.succ 0).succ) ↦ i) ⟨1, sorry⟩)
Tactic: fin_cases b
Cleared hypotheses: b, h'
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Notation (goal)
Goal:
α : Type u_1
x y : α
h : x ≠ y
b : Fin (Nat.succ 0).succ
h' : ![x, y] ((fun (i : Fin (Nat.succ 0).succ) ↦ i) (⟨1, ⋯⟩ : Fin (Nat.succ 0).succ)) = ![x, y] b
⊢ (fun (i : Fin (Nat.succ 0).succ) ↦ i) ⟨1, ⋯⟩ = b
have refine_2 : ∀
  (h' :
    ![x, y] ((fun (i : Fin (Nat.succ 0).succ) ↦ i) (⟨1, sorry⟩ : Fin (Nat.succ 0).succ)) =
      ![x, y] ((fun (i : Fin (Nat.succ 0).succ) ↦ i) ⟨0, sorry⟩)),
  Eq (α := Fin (Nat.succ 0).succ) ((fun (i : Fin (Nat.succ 0).succ) ↦ i) ⟨1, sorry⟩)
    ((fun (i : Fin (Nat.succ 0).succ) ↦ i) ⟨0, sorry⟩)
Tactic: fin_cases b
Cleared hypotheses: b, h'
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Notation (goal)
Goal:
α : Type u_1
x y : α
h : x ≠ y
b : Fin (Nat.succ 0).succ
h' : ![x, y] ((fun (i : Fin (Nat.succ 0).succ) ↦ i) (⟨1, ⋯⟩ : Fin (Nat.succ 0).succ)) = ![x, y] b
refine_2 :
  ∀
    (h' :
      ![x, y] ((fun (i : Fin (Nat.succ 0).succ) ↦ i) (⟨1, ⋯⟩ : Fin (Nat.succ 0).succ)) =
        ![x, y] ((fun (i : Fin (Nat.succ 0).succ) ↦ i) ⟨0, ⋯⟩)),
    Eq (α := Fin (Nat.succ 0).succ) ((fun (i : Fin (Nat.succ 0).succ) ↦ i) ⟨1, ⋯⟩)
      ((fun (i : Fin (Nat.succ 0).succ) ↦ i) ⟨0, ⋯⟩)
⊢ (fun (i : Fin (Nat.succ 0).succ) ↦ i) ⟨1, ⋯⟩ = b
have refine_2₁ : ∀
  (h' :
    ![x, y] ((fun (i : Fin (Nat.succ 0).succ) ↦ i) (⟨1, sorry⟩ : Fin (Nat.succ 0).succ)) =
      ![x, y] ((fun (i : Fin (Nat.succ 0).succ) ↦ i) ⟨1, sorry⟩)),
  Eq (α := Fin (Nat.succ 0).succ) ((fun (i : Fin (Nat.succ 0).succ) ↦ i) ⟨1, sorry⟩)
    ((fun (i : Fin (Nat.succ 0).succ) ↦ i) ⟨1, sorry⟩)
Tactic: fin_cases b
Cleared hypotheses: b, h'
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Permanent (goal)
Goal:
n : Type u_1
inst : DecidableEq n
inst_1 : Fintype n
R : Type u_2
inst_2 : CommSemiring R
d : n → R
⊢ (diagonal d).permanent = ∏ i : n, d i
have refine_1 : ∀ (σ : Perm n),
  Membership.mem (γ := Finset (Perm n)) univ σ →
    ∀ (hσ : σ ≠ 1), Eq.{u_2 + 1} (α := R) (∏ i : n, diagonal d ((σ : (a : n) → n) i) i) 0
Tactic: refine (sum_eq_single 1 (fun σ _ hσ ↦ ?_) (fun h ↦ (h <| mem_univ _).elim)).trans ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Permanent (goal)
Goal:
n : Type u_1
inst : DecidableEq n
inst_1 : Fintype n
R : Type u_2
inst_2 : CommSemiring R
d : n → R
refine_1 :
  ∀ (σ : Perm n),
    Membership.mem (γ := Finset (Perm n)) univ σ →
      ∀ (hσ : σ ≠ 1), Eq.{u_2 + 1} (α := R) (∏ i : n, diagonal d ((σ : (a : n) → n) i) i) 0
⊢ (diagonal d).permanent = ∏ i : n, d i
have refine_2 : Eq.{u_2 + 1} (α := R) (∏ i : n, diagonal d ((1 : (a : n) → n) i) i) (∏ i : n, d i)
Tactic: refine (sum_eq_single 1 (fun σ _ hσ ↦ ?_) (fun h ↦ (h <| mem_univ _).elim)).trans ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Permanent (goal)
Goal:
n : Type u_1
inst : DecidableEq n
inst_1 : Fintype n
R : Type u_2
inst_2 : CommSemiring R
inst_3 : Subsingleton n
A : Matrix n n R
k : n
⊢ A.permanent = A k k
have have : ∀ (this : Unique n), A.permanent = A k k
Tactic: have := uniqueOfSubsingleton k
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Permanent (goal)
Goal:
n : Type u_1
inst : DecidableEq n
inst_1 : Fintype n
R : Type u_2
inst_2 : CommSemiring R
M : Matrix n n R
⊢ Mᵀ.permanent = M.permanent
have refine : ∀ (x : Perm n), Eq.{u_2 + 1} (α := R) (∏ i : n, Mᵀ ((x : (a : n) → n) i) i) (∏ i : n, M ((x⁻¹ : (a : n) → n) i) i)
Tactic: refine sum_bijective _ inv_involutive.bijective _ _ ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Permanent (goal)
Goal:
n : Type u_1
inst : DecidableEq n
inst_1 : Fintype n
R : Type u_2
inst_2 : CommSemiring R
M : Matrix n n R
σ : Perm n
⊢ Eq.{u_2 + 1} (α := R) (∏ i : n, Mᵀ ((σ : (a : n) → n) i) i) (∏ i : n, M ((σ⁻¹ : (a : n) → n) i) i)
have h : ∀ (x : n), Mᵀ ((σ : (a : n) → n) x) x = M ((σ⁻¹ : (a : n) → n) ((σ : (a : n) → n) x : n)) ((σ : (a : n) → n) x)
Tactic: apply Fintype.prod_equiv σ
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Permanent (goal)
Goal:
n : Type u_1
inst : DecidableEq n
inst_1 : Fintype n
R : Type u_2
inst_2 : CommSemiring R
σ : Perm n
M : Matrix n n R
⊢ permanent (M.submatrix id (⇑σ : (a : n) → n)) = M.permanent
have rw : permanent (M.submatrix id (⇑σ : (a : n) → n))ᵀ = M.permanent
Tactic: rw [← permanent_transpose, transpose_submatrix, permanent_permute_cols, permanent_transpose]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Permanent (goal)
Goal:
n : Type u_1
inst : DecidableEq n
inst_1 : Fintype n
R : Type u_2
inst_2 : CommSemiring R
σ : Perm n
M : Matrix n n R
rw : permanent (M.submatrix id (⇑σ : (a : n) → n))ᵀ = M.permanent
⊢ permanent (M.submatrix id (⇑σ : (a : n) → n)) = M.permanent
have rw₁ : permanent (Mᵀ.submatrix (⇑σ : (a : n) → n) id) = M.permanent
Tactic: rw [← permanent_transpose, transpose_submatrix, permanent_permute_cols, permanent_transpose]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Permanent (goal)
Goal:
n : Type u_1
inst : DecidableEq n
inst_1 : Fintype n
R : Type u_2
inst_2 : CommSemiring R
σ : Perm n
M : Matrix n n R
rw : permanent (M.submatrix id (⇑σ : (a : n) → n))ᵀ = M.permanent
rw₁ : permanent (Mᵀ.submatrix (⇑σ : (a : n) → n) id) = M.permanent
⊢ permanent (M.submatrix id (⇑σ : (a : n) → n)) = M.permanent
have rw₂ : Mᵀ.permanent = M.permanent
Tactic: rw [← permanent_transpose, transpose_submatrix, permanent_permute_cols, permanent_transpose]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Permanent (goal)
Goal:
n : Type u_1
inst : DecidableEq n
inst_1 : Fintype n
R : Type u_2
inst_2 : CommSemiring R
σ : Perm n
M : Matrix n n R
rw : permanent (M.submatrix id (⇑σ : (a : n) → n))ᵀ = M.permanent
rw₁ : permanent (Mᵀ.submatrix (⇑σ : (a : n) → n) id) = M.permanent
rw₂ : Mᵀ.permanent = M.permanent
⊢ permanent (M.submatrix id (⇑σ : (a : n) → n)) = M.permanent
have rw₃ : M.permanent = M.permanent
Tactic: rw [← permanent_transpose, transpose_submatrix, permanent_permute_cols, permanent_transpose]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Permanent (goal)
Goal:
n : Type u_1
inst : DecidableEq n
inst_1 : Fintype n
R : Type u_2
inst_2 : CommSemiring R
M : Matrix n n R
c : R
⊢ (c • M).permanent = c ^ Fintype.card n * M.permanent
have simp : Eq.{u_2 + 1} (α := R) (∑ x : Perm n, ∏ x_1 : n, c * M ((x : (a : n) → n) x_1) x_1)
  (∑ i : Perm n, c ^ Fintype.card n * ∏ i_1 : n, M ((i : (a : n) → n) i_1) i_1)
Tactic: simp only [permanent, smul_apply, smul_eq_mul, Finset.mul_sum]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Permanent (goal)
Goal:
n : Type u_1
inst : DecidableEq n
inst_1 : Fintype n
R : Type u_2
inst_2 : CommSemiring R
M : Matrix n n R
c : R
⊢ Eq.{u_2 + 1} (α := R) (∑ x : Perm n, ∏ x_1 : n, c * M ((x : (a : n) → n) x_1) x_1)
    (∑ i : Perm n, c ^ Fintype.card n * ∏ i_1 : n, M ((i : (a : n) → n) i_1) i_1)
have e_f : Eq (α := Perm n → R) (fun (x : Perm n) ↦ ∏ x_1 : n, c * M ((x : (a : n) → n) x_1) x_1) fun (i : Perm n) ↦
  c ^ Fintype.card n * ∏ i_1 : n, M ((i : (a : n) → n) i_1) i_1
Tactic: congr
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Permanent (goal)
Goal:
n : Type u_1
inst : DecidableEq n
inst_1 : Fintype n
R : Type u_2
inst_2 : CommSemiring R
M : Matrix n n R
c : R
⊢ Eq (α := Perm n → R) (fun (x : Perm n) ↦ ∏ x_1 : n, c * M ((x : (a : n) → n) x_1) x_1) fun (i : Perm n) ↦
    c ^ Fintype.card n * ∏ i_1 : n, M ((i : (a : n) → n) i_1) i_1
have e_f : ∀ (x : Perm n), ∏ x_1 : n, c * M ((x : (a : n) → n) x_1) x_1 = c ^ Fintype.card n * ∏ i : n, M ((x : (a : n) → n) i) i
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Permanent (goal)
Goal:
n : Type u_1
inst : DecidableEq n
inst_1 : Fintype n
R : Type u_2
inst_2 : CommSemiring R
M : Matrix n n R
c : R
x : Perm n
⊢ ∏ x_1 : n, c * M ((x : (a : n) → n) x_1) x_1 = c ^ Fintype.card n * ∏ i : n, M ((x : (a : n) → n) i) i
have e_f : ∏ x_1 : n, c * M ((x : (a : n) → n) x_1) x_1 = (∏ i : n, M ((x : (a : n) → n) i) i) * c ^ Fintype.card n
Tactic: rw [mul_comm]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Permanent (goal)
Goal:
n : Type u_1
inst : DecidableEq n
inst_1 : Fintype n
R : Type u_2
inst_2 : CommSemiring R
M : Matrix n n R
c : R
x : Perm n
| ∏ x_1 : n, c * M ((x : (a : n) → n) x_1) x_1
have simp : ∏ x_1 : n, M ((x : (a : n) → n) x_1) x_1 * c
Tactic: simp [mul_comm c]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Permanent (goal)
Goal:
n : Type u_1
inst : DecidableEq n
inst_1 : Fintype n
R : Type u_2
inst_2 : CommSemiring R
M : Matrix n n R
c : R
x : Perm n
| ∏ x_1 : n, c * M ((x : (a : n) → n) x_1) x_1
have simp : ∏ x_1 : n, M ((x : (a : n) → n) x_1) x_1 * c
Tactic: simp [mul_comm c];
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Permanent (goal)
Goal:
n : Type u_1
inst : DecidableEq n
inst_1 : Fintype n
R : Type u_2
inst_2 : CommSemiring R
M : Matrix n n R
c : R
x : Perm n
⊢ ∏ x_1 : n, c * M ((x : (a : n) → n) x_1) x_1 = (∏ i : n, M ((x : (a : n) → n) i) i) * c ^ Fintype.card n
have e_f : ∏ x_1 : n, M ((x : (a : n) → n) x_1) x_1 * c = (∏ i : n, M ((x : (a : n) → n) i) i) * c ^ Fintype.card n
Tactic: conv in ∏ _, c * _ => simp [mul_comm c];
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Permanent (goal)
Goal:
n : Type u_1
inst : DecidableEq n
inst_1 : Fintype n
R : Type u_2
inst_2 : CommSemiring R
M : Matrix n n R
j : n
c : R
u : n → R
⊢ (M.updateCol j (c • u)).permanent = c * (M.updateCol j u).permanent
have simp : Eq.{u_2 + 1} (α := R)
  (∑ x : Perm n, c * u ((x : (a : n) → n) j) * ∏ i ∈ erase univ j, M.updateCol j (c • u) ((x : (a : n) → n) i) i)
  (∑ x : Perm n, c * u ((x : (a : n) → n) j) * ∏ i ∈ erase univ j, M.updateCol j u ((x : (a : n) → n) i) i)
Tactic: simp only [permanent, ← mul_prod_erase _ _ (mem_univ j), updateCol_self, Pi.smul_apply,
    smul_eq_mul, mul_sum, ← mul_assoc]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Permanent (goal)
Goal:
n : Type u_1
inst : DecidableEq n
inst_1 : Fintype n
R : Type u_2
inst_2 : CommSemiring R
M : Matrix n n R
j : n
c : R
u : n → R
⊢ Eq.{u_2 + 1} (α := R)
    (∑ x : Perm n, c * u ((x : (a : n) → n) j) * ∏ i ∈ erase univ j, M.updateCol j (c • u) ((x : (a : n) → n) i) i)
    (∑ x : Perm n, c * u ((x : (a : n) → n) j) * ∏ i ∈ erase univ j, M.updateCol j u ((x : (a : n) → n) i) i)
have e_f : ∀ (p : Perm n),
  c * u ((p : (a : n) → n) j) * ∏ i ∈ erase univ j, M.updateCol j (c • u) ((p : (a : n) → n) i) i =
    c * u ((p : (a : n) → n) j) * ∏ i ∈ erase univ j, M.updateCol j u ((p : (a : n) → n) i) i
Tactic: congr 1 with p
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Permanent (goal)
Goal:
n : Type u_1
inst : DecidableEq n
inst_1 : Fintype n
R : Type u_2
inst_2 : CommSemiring R
M : Matrix n n R
j : n
c : R
u : n → R
p : Perm n
⊢ c * u ((p : (a : n) → n) j) * ∏ i ∈ erase univ j, M.updateCol j (c • u) ((p : (a : n) → n) i) i =
    c * u ((p : (a : n) → n) j) * ∏ i ∈ erase univ j, M.updateCol j u ((p : (a : n) → n) i) i
have rw : ∀ (i : n) (hi : i ∈ erase univ j),
  M.updateCol j (c • u) ((p : (a : n) → n) i) i = M.updateCol j u ((p : (a : n) → n) i) i
Tactic: rw [Finset.prod_congr rfl (fun i hi ↦ ?_)]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Permanent (goal)
Goal:
n : Type u_1
inst : DecidableEq n
inst_1 : Fintype n
R : Type u_2
inst_2 : CommSemiring R
M : Matrix n n R
j : n
c : R
u : n → R
⊢ (M.updateRow j (c • u)).permanent = c * (M.updateRow j u).permanent
have rw : (M.updateRow j (c • u))ᵀ.permanent = c * (M.updateRow j u).permanent
Tactic: rw [← permanent_transpose, ← updateCol_transpose, permanent_updateCol_smul,
    updateCol_transpose, permanent_transpose]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Permanent (goal)
Goal:
n : Type u_1
inst : DecidableEq n
inst_1 : Fintype n
R : Type u_2
inst_2 : CommSemiring R
M : Matrix n n R
j : n
c : R
u : n → R
rw : (M.updateRow j (c • u))ᵀ.permanent = c * (M.updateRow j u).permanent
⊢ (M.updateRow j (c • u)).permanent = c * (M.updateRow j u).permanent
have rw₁ : (Mᵀ.updateCol j (c • u)).permanent = c * (M.updateRow j u).permanent
Tactic: rw [← permanent_transpose, ← updateCol_transpose, permanent_updateCol_smul,
    updateCol_transpose, permanent_transpose]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Permanent (goal)
Goal:
n : Type u_1
inst : DecidableEq n
inst_1 : Fintype n
R : Type u_2
inst_2 : CommSemiring R
M : Matrix n n R
j : n
c : R
u : n → R
rw : (M.updateRow j (c • u))ᵀ.permanent = c * (M.updateRow j u).permanent
rw₁ : (Mᵀ.updateCol j (c • u)).permanent = c * (M.updateRow j u).permanent
⊢ (M.updateRow j (c • u)).permanent = c * (M.updateRow j u).permanent
have rw₂ : c * (Mᵀ.updateCol j u).permanent = c * (M.updateRow j u).permanent
Tactic: rw [← permanent_transpose, ← updateCol_transpose, permanent_updateCol_smul,
    updateCol_transpose, permanent_transpose]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Permanent (goal)
Goal:
n : Type u_1
inst : DecidableEq n
inst_1 : Fintype n
R : Type u_2
inst_2 : CommSemiring R
M : Matrix n n R
j : n
c : R
u : n → R
rw : (M.updateRow j (c • u))ᵀ.permanent = c * (M.updateRow j u).permanent
rw₁ : (Mᵀ.updateCol j (c • u)).permanent = c * (M.updateRow j u).permanent
rw₂ : c * (Mᵀ.updateCol j u).permanent = c * (M.updateRow j u).permanent
⊢ (M.updateRow j (c • u)).permanent = c * (M.updateRow j u).permanent
have rw₃ : c * (M.updateRow j u)ᵀ.permanent = c * (M.updateRow j u).permanent
Tactic: rw [← permanent_transpose, ← updateCol_transpose, permanent_updateCol_smul,
    updateCol_transpose, permanent_transpose]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Permanent (goal)
Goal:
n : Type u_1
inst : DecidableEq n
inst_1 : Fintype n
R : Type u_2
inst_2 : CommSemiring R
M : Matrix n n R
j : n
c : R
u : n → R
rw : (M.updateRow j (c • u))ᵀ.permanent = c * (M.updateRow j u).permanent
rw₁ : (Mᵀ.updateCol j (c • u)).permanent = c * (M.updateRow j u).permanent
rw₂ : c * (Mᵀ.updateCol j u).permanent = c * (M.updateRow j u).permanent
rw₃ : c * (M.updateRow j u)ᵀ.permanent = c * (M.updateRow j u).permanent
⊢ (M.updateRow j (c • u)).permanent = c * (M.updateRow j u).permanent
have rw₄ : c * (M.updateRow j u).permanent = c * (M.updateRow j u).permanent
Tactic: rw [← permanent_transpose, ← updateCol_transpose, permanent_updateCol_smul,
    updateCol_transpose, permanent_transpose]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Permutation (goal)
Goal:
n : Type u_1
R : Type u_2
inst : DecidableEq n
σ : Perm n
inst_1 : Zero R
inst_2 : One R
⊢ (Perm.permMatrix R σ)ᵀ = Perm.permMatrix R σ⁻¹
have rw : (toPEquiv σ).symm.toMatrix = Perm.permMatrix R σ⁻¹
Tactic: rw [← PEquiv.toMatrix_symm, ← Equiv.toPEquiv_symm, ← Equiv.Perm.inv_def]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Permutation (goal)
Goal:
n : Type u_1
R : Type u_2
inst : DecidableEq n
σ : Perm n
inst_1 : Zero R
inst_2 : One R
rw : (toPEquiv σ).symm.toMatrix = Perm.permMatrix R σ⁻¹
⊢ (Perm.permMatrix R σ)ᵀ = Perm.permMatrix R σ⁻¹
have rw₁ : (Equiv.symm σ).toPEquiv.toMatrix = Perm.permMatrix R σ⁻¹
Tactic: rw [← PEquiv.toMatrix_symm, ← Equiv.toPEquiv_symm, ← Equiv.Perm.inv_def]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Permutation (goal)
Goal:
n : Type u_1
R : Type u_2
inst : DecidableEq n
σ : Perm n
inst_1 : Zero R
inst_2 : One R
rw : (toPEquiv σ).symm.toMatrix = Perm.permMatrix R σ⁻¹
rw₁ : (Equiv.symm σ).toPEquiv.toMatrix = Perm.permMatrix R σ⁻¹
⊢ (Perm.permMatrix R σ)ᵀ = Perm.permMatrix R σ⁻¹
have rw₂ : (toPEquiv σ⁻¹).toMatrix = Perm.permMatrix R σ⁻¹
Tactic: rw [← PEquiv.toMatrix_symm, ← Equiv.toPEquiv_symm, ← Equiv.Perm.inv_def]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Permutation (goal)
Goal:
n : Type u_1
R : Type u_2
inst : DecidableEq n
σ : Perm n
inst_1 : NonAssocSemiring R
inst_2 : StarRing R
⊢ (Perm.permMatrix R σ)ᴴ = Perm.permMatrix R σ⁻¹
have simp : ((of : (a : n → n → R) → Matrix n n R) fun (i j : n) ↦ star (Perm.permMatrix R σ⁻¹ i j)) = Perm.permMatrix R σ⁻¹
Tactic: simp only [conjTranspose, transpose_permMatrix, map]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Permutation (goal)
Goal:
n : Type u_1
R : Type u_2
inst : DecidableEq n
σ : Perm n
inst_1 : Fintype n
inst_2 : CommRing R
⊢ (Perm.permMatrix R σ).det = (↑(↑(((Perm.sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) σ) : ℤ) : R)
have rw : (Perm.permMatrix R σ * 1).det = (↑(↑(((Perm.sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) σ) : ℤ) : R)
Tactic: rw [← Matrix.mul_one (σ.permMatrix R), PEquiv.toMatrix_toPEquiv_mul,
    det_permute, det_one, mul_one]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Permutation (goal)
Goal:
n : Type u_1
R : Type u_2
inst : DecidableEq n
σ : Perm n
inst_1 : Fintype n
inst_2 : CommRing R
rw : (Perm.permMatrix R σ * 1).det = (↑(↑(((Perm.sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) σ) : ℤ) : R)
⊢ (Perm.permMatrix R σ).det = (↑(↑(((Perm.sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) σ) : ℤ) : R)
have rw₁ : Eq.{u_2 + 1} (α := R) (det (n := n) (submatrix (m := n) 1 (⇑σ : (a : n) → n) id))
  (↑(↑(((Perm.sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) σ) : ℤ) : R)
Tactic: rw [← Matrix.mul_one (σ.permMatrix R), PEquiv.toMatrix_toPEquiv_mul,
    det_permute, det_one, mul_one]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Permutation (goal)
Goal:
n : Type u_1
R : Type u_2
inst : DecidableEq n
σ : Perm n
inst_1 : Fintype n
inst_2 : CommRing R
rw : (Perm.permMatrix R σ * 1).det = (↑(↑(((Perm.sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) σ) : ℤ) : R)
rw₁ :
  Eq.{u_2 + 1} (α := R) (det (n := n) (submatrix (m := n) 1 (⇑σ : (a : n) → n) id))
    (↑(↑(((Perm.sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) σ) : ℤ) : R)
⊢ (Perm.permMatrix R σ).det = (↑(↑(((Perm.sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) σ) : ℤ) : R)
have rw₂ : HMul.hMul (α := R) (↑(↑(((Perm.sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) σ) : ℤ) : R) (det.{u_2, u_1} (n := n) 1) =
  (↑(↑(((Perm.sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) σ) : ℤ) : R)
Tactic: rw [← Matrix.mul_one (σ.permMatrix R), PEquiv.toMatrix_toPEquiv_mul,
    det_permute, det_one, mul_one]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Permutation (goal)
Goal:
n : Type u_1
R : Type u_2
inst : DecidableEq n
σ : Perm n
inst_1 : Fintype n
inst_2 : CommRing R
rw : (Perm.permMatrix R σ * 1).det = (↑(↑(((Perm.sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) σ) : ℤ) : R)
rw₁ :
  Eq.{u_2 + 1} (α := R) (det (n := n) (submatrix (m := n) 1 (⇑σ : (a : n) → n) id))
    (↑(↑(((Perm.sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) σ) : ℤ) : R)
rw₂ :
  HMul.hMul (α := R) (↑(↑(((Perm.sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) σ) : ℤ) : R) (det.{u_2, u_1} (n := n) 1) =
    (↑(↑(((Perm.sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) σ) : ℤ) : R)
⊢ (Perm.permMatrix R σ).det = (↑(↑(((Perm.sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) σ) : ℤ) : R)
have rw₃ : HMul.hMul (α := R) (↑(↑(((Perm.sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) σ) : ℤ) : R) 1 =
  (↑(↑(((Perm.sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) σ) : ℤ) : R)
Tactic: rw [← Matrix.mul_one (σ.permMatrix R), PEquiv.toMatrix_toPEquiv_mul,
    det_permute, det_one, mul_one]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Permutation (goal)
Goal:
n : Type u_1
R : Type u_2
inst : DecidableEq n
σ : Perm n
inst_1 : Fintype n
inst_2 : CommRing R
rw : (Perm.permMatrix R σ * 1).det = (↑(↑(((Perm.sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) σ) : ℤ) : R)
rw₁ :
  Eq.{u_2 + 1} (α := R) (det (n := n) (submatrix (m := n) 1 (⇑σ : (a : n) → n) id))
    (↑(↑(((Perm.sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) σ) : ℤ) : R)
rw₂ :
  HMul.hMul (α := R) (↑(↑(((Perm.sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) σ) : ℤ) : R) (det.{u_2, u_1} (n := n) 1) =
    (↑(↑(((Perm.sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) σ) : ℤ) : R)
rw₃ :
  HMul.hMul (α := R) (↑(↑(((Perm.sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) σ) : ℤ) : R) 1 =
    (↑(↑(((Perm.sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) σ) : ℤ) : R)
⊢ (Perm.permMatrix R σ).det = (↑(↑(((Perm.sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) σ) : ℤ) : R)
have rw₄ : Eq.{u_2 + 1} (α := R) (↑(↑(((Perm.sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) σ) : ℤ) : R)
  (↑(↑(((Perm.sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) σ) : ℤ) : R)
Tactic: rw [← Matrix.mul_one (σ.permMatrix R), PEquiv.toMatrix_toPEquiv_mul,
    det_permute, det_one, mul_one]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Permutation (goal)
Goal:
n : Type u_1
R : Type u_2
inst : DecidableEq n
σ : Perm n
inst_1 : Fintype n
v : n → R
inst_2 : CommRing R
⊢ Perm.permMatrix R σ *ᵥ v = v ∘ (⇑σ : (a : n) → n)
have h : ∀ (j : n), (Perm.permMatrix R σ *ᵥ v) j = (v ∘ (⇑σ : (a : n) → n)) j
Tactic: ext j
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Permutation (goal)
Goal:
n : Type u_1
R : Type u_2
inst : DecidableEq n
σ : Perm n
inst_1 : Fintype n
v : n → R
inst_2 : CommRing R
⊢ v ᵥ* Perm.permMatrix R σ = v ∘ (⇑(Equiv.symm σ) : (a : n) → n)
have h : ∀ (j : n), (v ᵥ* Perm.permMatrix R σ) j = (v ∘ (⇑(Equiv.symm σ) : (a : n) → n)) j
Tactic: ext j
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Permutation (goal)
Goal:
n : Type u_1
R : Type u_2
inst : DecidableEq n
σ τ : Perm n
inst_1 : Fintype n
inst_2 : NonAssocSemiring R
⊢ Perm.permMatrix R (σ * τ) = Perm.permMatrix R τ * Perm.permMatrix R σ
have rw : (toPEquiv (σ * τ)).toMatrix = Perm.permMatrix R τ * Perm.permMatrix R σ
Tactic: rw [Perm.permMatrix, Perm.mul_def, toPEquiv_trans, PEquiv.toMatrix_trans]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Permutation (goal)
Goal:
n : Type u_1
R : Type u_2
inst : DecidableEq n
σ τ : Perm n
inst_1 : Fintype n
inst_2 : NonAssocSemiring R
rw : (toPEquiv (σ * τ)).toMatrix = Perm.permMatrix R τ * Perm.permMatrix R σ
⊢ Perm.permMatrix R (σ * τ) = Perm.permMatrix R τ * Perm.permMatrix R σ
have rw₁ : (Equiv.trans τ σ).toPEquiv.toMatrix = Perm.permMatrix R τ * Perm.permMatrix R σ
Tactic: rw [Perm.permMatrix, Perm.mul_def, toPEquiv_trans, PEquiv.toMatrix_trans]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Permutation (goal)
Goal:
n : Type u_1
R : Type u_2
inst : DecidableEq n
σ τ : Perm n
inst_1 : Fintype n
inst_2 : NonAssocSemiring R
rw : (toPEquiv (σ * τ)).toMatrix = Perm.permMatrix R τ * Perm.permMatrix R σ
rw₁ : (Equiv.trans τ σ).toPEquiv.toMatrix = Perm.permMatrix R τ * Perm.permMatrix R σ
⊢ Perm.permMatrix R (σ * τ) = Perm.permMatrix R τ * Perm.permMatrix R σ
have rw₂ : ((toPEquiv τ).trans (toPEquiv σ)).toMatrix = Perm.permMatrix R τ * Perm.permMatrix R σ
Tactic: rw [Perm.permMatrix, Perm.mul_def, toPEquiv_trans, PEquiv.toMatrix_trans]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Permutation (goal)
Goal:
n : Type u_1
R : Type u_2
inst : DecidableEq n
σ τ : Perm n
inst_1 : Fintype n
inst_2 : NonAssocSemiring R
rw : (toPEquiv (σ * τ)).toMatrix = Perm.permMatrix R τ * Perm.permMatrix R σ
rw₁ : (Equiv.trans τ σ).toPEquiv.toMatrix = Perm.permMatrix R τ * Perm.permMatrix R σ
rw₂ : ((toPEquiv τ).trans (toPEquiv σ)).toMatrix = Perm.permMatrix R τ * Perm.permMatrix R σ
⊢ Perm.permMatrix R (σ * τ) = Perm.permMatrix R τ * Perm.permMatrix R σ
have rw₃ : HMul.hMul (α := Matrix n n R) (toPEquiv τ).toMatrix (toPEquiv σ).toMatrix = Perm.permMatrix R τ * Perm.permMatrix R σ
Tactic: rw [Perm.permMatrix, Perm.mul_def, toPEquiv_trans, PEquiv.toMatrix_trans]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Permutation (goal)
Goal:
n : Type u_1
R : Type u_2
inst : DecidableEq n
σ_1 τ_1 : Perm n
inst_1 : Fintype n
inst_2 : NonAssocSemiring R
σ τ : Perm n
⊢ Perm.permMatrix R (σ * τ)⁻¹ = Perm.permMatrix R σ⁻¹ * Perm.permMatrix R τ⁻¹
have rw : Perm.permMatrix R (τ⁻¹ * σ⁻¹) = Perm.permMatrix R σ⁻¹ * Perm.permMatrix R τ⁻¹
Tactic: rw [_root_.mul_inv_rev, permMatrix_mul]