awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Matrix.Notation
Goal:
α : Type u
R : Type u_1
inst : SMul R α
x : R
a₀ a₁ : α
⊢ x • ![a₀, a₁] = ![x • a₀, x • a₁]

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Matrix.Notation
Goal:
α : Type u
R : Type u_1
inst : SMul R α
x : R
a₀ a₁ a₂ : α
⊢ x • ![a₀, a₁, a₂] = ![x • a₀, x • a₁, x • a₂]

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Matrix.Notation
Goal:
α : Type u
inst : AddCommMonoid α
inst_1 : Mul α
a₀ a₁ b₀ b₁ : α
⊢ ![a₀, a₁] ⬝ᵥ ![b₀, b₁] = a₀ * b₀ + a₁ * b₁

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Matrix.Notation
Goal:
α : Type u
inst : AddCommMonoid α
inst_1 : Mul α
v w : Fin 2 → α
⊢ v ⬝ᵥ w = v 0 * w 0 + v 1 * w 1

Tactic:
vec2_dotProduct'

Premises used: Eq.mpr, Multiset.map, dotProduct, List.map, Fin.cons, Fin.induction.go, Fin.ofNat, Fin.induction, Matrix.vec2_dotProduct', Fin.cases, Matrix.vecCons, Finset.sum
-- Module: Mathlib.LinearAlgebra.Matrix.Notation
Goal:
α : Type u
inst : AddCommMonoid α
inst_1 : Mul α
a₀ a₁ a₂ b₀ b₁ b₂ : α
⊢ ![a₀, a₁, a₂] ⬝ᵥ ![b₀, b₁, b₂] = a₀ * b₀ + a₁ * b₁ + a₂ * b₂

Tactic:
simp [add_assoc]

Premises used: add_assoc
-- Module: Mathlib.LinearAlgebra.Matrix.Notation
Goal:
α : Type u
inst : AddCommMonoid α
inst_1 : Mul α
v w : Fin 3 → α
⊢ v ⬝ᵥ w = v 0 * w 0 + v 1 * w 1 + v 2 * w 2

Tactic:
vec3_dotProduct'

Premises used: Eq.mpr, Multiset.map, dotProduct, List.map, Fin.cons, Fin.induction.go, Fin.ofNat, Matrix.vec3_dotProduct', Fin.induction, Fin.cases, Matrix.vecCons, Finset.sum
-- Module: Mathlib.LinearAlgebra.Matrix.Notation
Goal:
α : Type u_1
x y : α
⊢ Function.Injective ![x, y] ↔ x ≠ y

Tactic:
⟨fun h ↦ ?_, fun h a b h' ↦ ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.LinearAlgebra.Matrix.Notation
Goal:
α : Type u_1
x y : α
refine_1 : ∀ (h : Function.Injective ![x, y]), x ≠ y
refine_2 : ∀ (h : x ≠ y) (a b : Fin (Nat.succ 0).succ) (h' : ![x, y] a = ![x, y] b), a = b
⊢ Function.Injective ![x, y] ↔ x ≠ y

Tactic:
refine ⟨fun h ↦ ?_, fun h a b h' ↦ ?_⟩
-- Module: Mathlib.LinearAlgebra.Matrix.Notation
Goal:
α : Type u_1
x y : α
h : Function.Injective ![x, y]
⊢ x ≠ y

Tactic:
simpa using h.ne Fin.zero_ne_one

Premises used: Function.Injective.ne, Fin.zero_ne_one
-- Module: Mathlib.LinearAlgebra.Matrix.Notation
Goal:
α : Type u_1
x y : α
h : x ≠ y
a b : Fin (Nat.succ 0).succ
h' : ![x, y] a = ![x, y] b
refine_2 :
  ∀ (h' : ![x, y] ((fun (i : Fin (Nat.succ 0).succ) ↦ i) (⟨0, ⋯⟩ : Fin (Nat.succ 0).succ)) = ![x, y] b),
    (fun (i : Fin (Nat.succ 0).succ) ↦ i) ⟨0, ⋯⟩ = b
refine_2₁ :
  ∀ (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
⊢ a = b

Tactic:
fin_cases a
-- Module: Mathlib.LinearAlgebra.Matrix.Notation
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, ⋯⟩)
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) ⟨1, ⋯⟩)),
    Eq (α := Fin (Nat.succ 0).succ) ((fun (i : Fin (Nat.succ 0).succ) ↦ i) ⟨0, ⋯⟩)
      ((fun (i : Fin (Nat.succ 0).succ) ↦ i) ⟨1, ⋯⟩)
⊢ (fun (i : Fin (Nat.succ 0).succ) ↦ i) ⟨0, ⋯⟩ = b

Tactic:
fin_cases b
-- Module: Mathlib.LinearAlgebra.Matrix.Notation
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, ⋯⟩)
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) ⟨1, ⋯⟩)),
    Eq (α := Fin (Nat.succ 0).succ) ((fun (i : Fin (Nat.succ 0).succ) ↦ i) ⟨1, ⋯⟩)
      ((fun (i : Fin (Nat.succ 0).succ) ↦ i) ⟨1, ⋯⟩)
⊢ (fun (i : Fin (Nat.succ 0).succ) ↦ i) ⟨1, ⋯⟩ = b

Tactic:
fin_cases b
-- Module: Mathlib.LinearAlgebra.Matrix.Notation
Goal:
α : Type u_1
x y : α
h : x ≠ y
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, ⋯⟩)

Tactic:
aesop
-- Module: Mathlib.LinearAlgebra.Matrix.Notation
Goal:
α : Type u_1
x y : α
h : x ≠ y
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) ⟨1, ⋯⟩)
⊢ Eq (α := Fin (Nat.succ 0).succ) ((fun (i : Fin (Nat.succ 0).succ) ↦ i) ⟨0, ⋯⟩)
    ((fun (i : Fin (Nat.succ 0).succ) ↦ i) ⟨1, ⋯⟩)

Tactic:
aesop
-- Module: Mathlib.LinearAlgebra.Matrix.Notation
Goal:
α : Type u_1
x y : α
h : x ≠ y
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, ⋯⟩)

Tactic:
aesop
-- Module: Mathlib.LinearAlgebra.Matrix.Notation
Goal:
α : Type u_1
x y : α
h : x ≠ y
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) ⟨1, ⋯⟩)
⊢ Eq (α := Fin (Nat.succ 0).succ) ((fun (i : Fin (Nat.succ 0).succ) ↦ i) ⟨1, ⋯⟩)
    ((fun (i : Fin (Nat.succ 0).succ) ↦ i) ⟨1, ⋯⟩)

Tactic:
aesop
-- Module: Mathlib.LinearAlgebra.Matrix.Orthogonal
Goal:
α : Type u_1
n : Type u_2
m : Type u_3
inst : Mul α
inst_1 : AddCommMonoid α
A : Matrix m n α
inst_2 : Fintype m
⊢ Aᵀ.HasOrthogonalRows ↔ A.HasOrthogonalCols

Tactic:
Iff.rfl

Premises used: Iff.rfl, Matrix.HasOrthogonalCols
-- Module: Mathlib.LinearAlgebra.Matrix.Orthogonal
Goal:
α : Type u_1
n : Type u_2
m : Type u_3
inst : Mul α
inst_1 : AddCommMonoid α
A : Matrix m n α
inst_2 : Fintype n
⊢ Aᵀ.HasOrthogonalCols ↔ A.HasOrthogonalRows

Tactic:
Iff.rfl

Premises used: Iff.rfl, Matrix.HasOrthogonalCols, Matrix.transpose
-- Module: Mathlib.LinearAlgebra.Matrix.Orthogonal
Goal:
α : Type u_1
n : Type u_2
m : Type u_3
inst : Mul α
inst_1 : AddCommMonoid α
A : Matrix m n α
inst_2 : Fintype m
h : Aᵀ.HasOrthogonalRows
⊢ A.HasOrthogonalCols

Tactic:
h

Premises used: Matrix.HasOrthogonalCols
-- Module: Mathlib.LinearAlgebra.Matrix.Orthogonal
Goal:
α : Type u_1
n : Type u_2
m : Type u_3
inst : Mul α
inst_1 : AddCommMonoid α
A : Matrix m n α
inst_2 : Fintype m
h : A.HasOrthogonalCols
⊢ Aᵀ.HasOrthogonalRows

Tactic:
h

Premises used: Matrix.HasOrthogonalCols
-- Module: Mathlib.LinearAlgebra.Matrix.Orthogonal
Goal:
α : Type u_1
n : Type u_2
m : Type u_3
inst : Mul α
inst_1 : AddCommMonoid α
A : Matrix m n α
inst_2 : Fintype n
h : Aᵀ.HasOrthogonalCols
⊢ A.HasOrthogonalRows

Tactic:
h

Premises used: Matrix.HasOrthogonalCols, Matrix.transpose
-- Module: Mathlib.LinearAlgebra.Matrix.Orthogonal
Goal:
α : Type u_1
n : Type u_2
m : Type u_3
inst : Mul α
inst_1 : AddCommMonoid α
A : Matrix m n α
inst_2 : Fintype n
h : A.HasOrthogonalRows
⊢ Aᵀ.HasOrthogonalCols

Tactic:
h

Premises used: Matrix.HasOrthogonalCols, Matrix.transpose
-- Module: Mathlib.LinearAlgebra.Matrix.Permanent
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

Tactic:
(sum_eq_single 1 (fun σ _ hσ ↦ ?_) (fun h ↦ (h <| mem_univ _).elim)).trans ?_

Premises used: Finset.mem_univ, False.elim, Finset.sum_eq_single, Matrix.permanent, OfNat.ofNat, Eq.trans
-- Module: Mathlib.LinearAlgebra.Matrix.Permanent
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
refine_2 : Eq.{u_2 + 1} (α := R) (∏ i : n, diagonal d ((1 : (a : n) → n) i) i) (∏ i : n, d i)
⊢ (diagonal d).permanent = ∏ i : n, d i

Tactic:
refine (sum_eq_single 1 (fun σ _ hσ ↦ ?_) (fun h ↦ (h <| mem_univ _).elim)).trans ?_

Premises used: Finset.mem_univ, False.elim, Finset.sum_eq_single, OfNat.ofNat, Eq.trans
-- Module: Mathlib.LinearAlgebra.Matrix.Permanent
Goal:
n : Type u_1
inst : DecidableEq n
inst_1 : Fintype n
R : Type u_2
inst_2 : CommSemiring R
d : n → R
σ : Perm n
h : Membership.mem (γ := Finset (Perm n)) univ σ
hσ : σ ≠ 1
x : n
hx : ¬Eq (α := n) ((σ : (a : n) → n) x : n) ((1 : (a : n) → n) x : n)
⊢ Eq.{u_2 + 1} (α := R) (∏ i : n, diagonal d ((σ : (a : n) → n) i) i) 0

Tactic:
Finset.prod_eq_zero (mem_univ x) (if_neg hx)

Premises used: Finset.mem_univ, Finset.prod_eq_zero, if_neg
-- Module: Mathlib.LinearAlgebra.Matrix.Permanent
Goal:
n : Type u_1
inst : DecidableEq n
inst_1 : Fintype n
R : Type u_2
inst_2 : CommSemiring R
d : n → R
σ : Perm n
h : Membership.mem (γ := Finset (Perm n)) univ σ
hσ : σ ≠ 1
x : n
hx : ¬Eq (α := n) ((σ : (a : n) → n) x : n) ((1 : (a : n) → n) x : n)
⊢ Eq.{u_2 + 1} (α := R) (∏ i : n, diagonal d ((σ : (a : n) → n) i) i) 0

Tactic:
exact Finset.prod_eq_zero (mem_univ x) (if_neg hx)

Premises used: Finset.mem_univ, Finset.prod_eq_zero
-- Module: Mathlib.LinearAlgebra.Matrix.Permanent
Goal:
n : Type u_1
inst : DecidableEq n
inst_1 : Fintype n
R : Type u_2
inst_2 : CommSemiring R
d : n → R
σ : Perm n
h : Membership.mem (γ := Finset (Perm n)) univ σ
hσ : σ ≠ 1
⊢ Eq.{u_2 + 1} (α := R) (∏ i : n, diagonal d ((σ : (a : n) → n) i) i) 0

Tactic:
match not_forall.mp (mt Equiv.ext hσ) with
    | ⟨x, hx⟩ => exact Finset.prod_eq_zero (mem_univ x) (if_neg hx)
-- Module: Mathlib.LinearAlgebra.Matrix.Permanent
Goal:
n : Type u_1
inst : DecidableEq n
inst_1 : Fintype n
R : Type u_2
inst_2 : CommSemiring R
d : n → R
⊢ Eq.{u_2 + 1} (α := R) (∏ i : n, diagonal d ((1 : (a : n) → n) i) i) (∏ i : n, d i)

Tactic:
simp only [Perm.one_apply, diagonal_apply_eq]

Premises used: Matrix.diagonal_apply_eq, Equiv.Perm.one_apply
-- Module: Mathlib.LinearAlgebra.Matrix.Permanent
Goal:
n : Type u_1
inst : DecidableEq n
inst_1 : Fintype n
R : Type u_2
inst_2 : CommSemiring R
inst_3 : Nonempty n
⊢ Eq.{u_2 + 1} (α := R) (permanent.{u_1, u_2} (n := n) 0) 0

Tactic:
simp [permanent]

Premises used: Matrix.permanent
-- Module: Mathlib.LinearAlgebra.Matrix.Permanent
Goal:
n : Type u_1
inst : DecidableEq n
inst_1 : Fintype n
R : Type u_2
inst_2 : CommSemiring R
⊢ Eq.{u_2 + 1} (α := R) (permanent.{u_1, u_2} (n := n) (diagonal fun (x : n) ↦ 1)) 1

Tactic:
simp [-diagonal_one]

Premises used: Matrix.diagonal_one
-- Module: Mathlib.LinearAlgebra.Matrix.Permanent
Goal:
n : Type u_1
inst : DecidableEq n
inst_1 : Fintype n
R : Type u_2
inst_2 : CommSemiring R
inst_3 : IsEmpty n
A : Matrix n n R
⊢ A.permanent = 1

Tactic:
simp [permanent]

Premises used: Matrix.permanent
-- Module: Mathlib.LinearAlgebra.Matrix.Permanent
Goal:
n : Type u_1
inst : DecidableEq n
inst_1 : Fintype n
R : Type u_2
inst_2 : CommSemiring R
A : Matrix n n R
h : Fintype.card n = 0
⊢ A.permanent = 1

Tactic:
haveI : IsEmpty n := card_eq_zero_iff.mp h
  permanent_isEmpty

Premises used: Matrix.permanent_isEmpty
-- Module: Mathlib.LinearAlgebra.Matrix.Permanent
Goal:
R : Type u_2
inst : CommSemiring R
n : Type u_3
inst_1 : Unique n
inst_2 : DecidableEq n
inst_3 : Fintype n
A : Matrix n n R
⊢ A.permanent = A default default

Tactic:
simp [permanent, univ_unique]

Premises used: Finset.univ_unique, Matrix.permanent
-- Module: Mathlib.LinearAlgebra.Matrix.Permanent
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
have : ∀ (this : Unique n), A.permanent = A k k
⊢ A.permanent = A k k

Tactic:
have := uniqueOfSubsingleton k
-- Module: Mathlib.LinearAlgebra.Matrix.Permanent
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
this : Unique n
⊢ A.permanent = A default default

Tactic:
permanent_unique A

Premises used: Matrix.permanent_unique
-- Module: Mathlib.LinearAlgebra.Matrix.Permanent
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
this : Unique n
⊢ A.permanent = A k k

Tactic:
convert! permanent_unique A

Premises used: Matrix.permanent_unique
-- Module: Mathlib.LinearAlgebra.Matrix.Permanent
Goal:
n : Type u_1
inst : DecidableEq n
inst_1 : Fintype n
R : Type u_2
inst_2 : CommSemiring R
A : Matrix n n R
h : Fintype.card n = 1
k : n
⊢ A.permanent = A k k

Tactic:
haveI : Subsingleton n := card_le_one_iff_subsingleton.mp h.le
  permanent_eq_elem_of_subsingleton _ _

Premises used: Matrix.permanent_eq_elem_of_subsingleton
-- Module: Mathlib.LinearAlgebra.Matrix.Permanent
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

Tactic:
sum_bijective _ inv_involutive.bijective _ _ ?_

Premises used: Fintype.sum_bijective, inv_involutive, Function.Involutive.bijective, Matrix.permanent
-- Module: Mathlib.LinearAlgebra.Matrix.Permanent
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
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)
⊢ Mᵀ.permanent = M.permanent

Tactic:
refine sum_bijective _ inv_involutive.bijective _ _ ?_

Premises used: Fintype.sum_bijective, inv_involutive, Function.Involutive.bijective
-- Module: Mathlib.LinearAlgebra.Matrix.Permanent
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
h : ∀ (x : n), Mᵀ ((σ : (a : n) → n) x) x = M ((σ⁻¹ : (a : n) → n) ((σ : (a : n) → n) x : n)) ((σ : (a : n) → n) x)
⊢ Eq.{u_2 + 1} (α := R) (∏ i : n, Mᵀ ((σ : (a : n) → n) i) i) (∏ i : n, M ((σ⁻¹ : (a : n) → n) i) i)

Tactic:
apply Fintype.prod_equiv σ

Premises used: Fintype.prod_equiv
-- Module: Mathlib.LinearAlgebra.Matrix.Permanent
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
⊢ ∀ (x : n), Mᵀ ((σ : (a : n) → n) x) x = M ((σ⁻¹ : (a : n) → n) ((σ : (a : n) → n) x : n)) ((σ : (a : n) → n) x)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Matrix.Permanent
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 (⇑σ : (a : n) → n) id) = M.permanent

Tactic:
(Group.mulLeft_bijective σ).sum_comp fun τ ↦ ∏ i : n, M (τ i) i

Premises used: Matrix.submatrix, Finset.univ, Function.Bijective.sum_comp, Group.mulLeft_bijective, Finset.prod, Matrix.permanent, DFunLike.coe
-- Module: Mathlib.LinearAlgebra.Matrix.Permanent
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
rw₃ rw₄ : M.permanent = M.permanent
⊢ permanent (M.submatrix id (⇑σ : (a : n) → n)) = M.permanent

Tactic:
rw [← permanent_transpose, transpose_submatrix, permanent_permute_cols, permanent_transpose]

Premises used: Matrix.transpose_submatrix, Matrix.permanent_permute_cols, Matrix.permanent_transpose
-- Module: Mathlib.LinearAlgebra.Matrix.Permanent
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
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)
⊢ (c • M).permanent = c ^ Fintype.card n * M.permanent

Tactic:
simp only [permanent, smul_apply, smul_eq_mul, Finset.mul_sum]

Premises used: Finset.mul_sum, Matrix.smul_apply, smul_eq_mul, Matrix.permanent
-- Module: Mathlib.LinearAlgebra.Matrix.Permanent
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
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
⊢ 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:
congr
-- Module: Mathlib.LinearAlgebra.Matrix.Permanent
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
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
⊢ 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:
ext
-- Module: Mathlib.LinearAlgebra.Matrix.Permanent
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
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
⊢ ∏ 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:
rw [mul_comm]

Premises used: mul_comm
-- Module: Mathlib.LinearAlgebra.Matrix.Permanent
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
simp : ∏ x_1 : n, M ((x : (a : n) → n) x_1) x_1 * c
| ∏ x_1 : n, c * M ((x : (a : n) → n) x_1) x_1

Tactic:
simp [mul_comm c]

Premises used: mul_comm
-- Module: Mathlib.LinearAlgebra.Matrix.Permanent
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
simp : ∏ x_1 : n, M ((x : (a : n) → n) x_1) x_1 * c
| ∏ x_1 : n, c * M ((x : (a : n) → n) x_1) x_1

Tactic:
simp [mul_comm c];

Premises used: mul_comm
-- Module: Mathlib.LinearAlgebra.Matrix.Permanent
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
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
⊢ ∏ 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:
conv in ∏ _, c * _ => simp [mul_comm c];

Premises used: mul_comm
-- Module: Mathlib.LinearAlgebra.Matrix.Permanent
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, M ((x : (a : n) → n) x_1) x_1 * c = (∏ i : n, M ((x : (a : n) → n) i) i) * c ^ Fintype.card n

Tactic:
prod_mul_pow_card.symm

Premises used: Finset.prod_mul_pow_card, Fintype.card, Eq.symm
-- Module: Mathlib.LinearAlgebra.Matrix.Permanent
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, M ((x : (a : n) → n) x_1) x_1 * c = (∏ i : n, M ((x : (a : n) → n) i) i) * c ^ Fintype.card n

Tactic:
exact prod_mul_pow_card.symm

Premises used: Finset.prod_mul_pow_card, Eq.symm
-- Module: Mathlib.LinearAlgebra.Matrix.Permanent
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
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)
⊢ (M.updateCol j (c • u)).permanent = c * (M.updateCol j u).permanent

Tactic:
simp only [permanent, ← mul_prod_erase _ _ (mem_univ j), updateCol_self, Pi.smul_apply,
    smul_eq_mul, mul_sum, ← mul_assoc]

Premises used: Finset.mem_univ, Finset.mul_sum, Matrix.updateCol_self, mul_assoc, Finset.mul_prod_erase, smul_eq_mul, Matrix.permanent, Pi.smul_apply
-- Module: Mathlib.LinearAlgebra.Matrix.Permanent
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
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
⊢ 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:
congr 1 with p
-- Module: Mathlib.LinearAlgebra.Matrix.Permanent
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
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
⊢ 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:
rw [Finset.prod_congr rfl (fun i hi ↦ ?_)]

Premises used: Finset.prod_congr, rfl
-- Module: Mathlib.LinearAlgebra.Matrix.Permanent
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
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:
simp only [ne_eq, ne_of_mem_erase hi, not_false_eq_true, updateCol_ne]

Premises used: Finset.ne_of_mem_erase, Matrix.updateCol_ne, ne_eq, not_false_eq_true
-- Module: Mathlib.LinearAlgebra.Matrix.Permanent
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
rw₄ 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

Tactic:
rw [← permanent_transpose, ← updateCol_transpose, permanent_updateCol_smul,
    updateCol_transpose, permanent_transpose]

Premises used: Matrix.permanent_updateCol_smul, Matrix.updateCol_transpose, Matrix.permanent_transpose
-- Module: Mathlib.LinearAlgebra.Matrix.Permutation
Goal:
n : Type u_1
R : Type u_2
inst : DecidableEq n
inst_1 : Zero R
inst_2 : One R
⊢ Perm.permMatrix R (Equiv.refl n) = 1

Tactic:
simp [← Matrix.ext_iff, Matrix.one_apply]

Premises used: Matrix.one_apply, Matrix.ext_iff
-- Module: Mathlib.LinearAlgebra.Matrix.Permutation
Goal:
n : Type u_1
R : Type u_2
inst : DecidableEq n
inst_1 : Zero R
inst_2 : One R
⊢ Eq (α := Matrix n n R) (Perm.permMatrix R 1) 1

Tactic:
permMatrix_refl

Premises used: Matrix.permMatrix_refl
-- Module: Mathlib.LinearAlgebra.Matrix.Permutation
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 σ⁻¹
rw₂ rw₃ : (toPEquiv σ⁻¹).toMatrix = Perm.permMatrix R σ⁻¹
⊢ (Perm.permMatrix R σ)ᵀ = Perm.permMatrix R σ⁻¹

Tactic:
rw [← PEquiv.toMatrix_symm, ← Equiv.toPEquiv_symm, ← Equiv.Perm.inv_def]

Premises used: PEquiv.toMatrix_symm, Equiv.toPEquiv_symm, Equiv.Perm.inv_def