awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Matrix.Defs
Goal:
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type v
A : Matrix m n α
r : l → m
c : o → n
i : l
j : o
⊢ A.submatrix r c i j = A (r i) (c j)

Tactic:
rfl

Premises used: Matrix.submatrix, rfl
-- Module: Mathlib.LinearAlgebra.Matrix.Defs
Goal:
m : Type u_2
n : Type u_3
α : Type v
A : Matrix m n α
⊢ A.submatrix id id = A

Tactic:
ext fun _ _ => rfl

Premises used: Matrix.ext, rfl
-- Module: Mathlib.LinearAlgebra.Matrix.Defs
Goal:
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type v
l₂ : Type u_10
o₂ : Type u_11
A : Matrix m n α
r₁ : l → m
c₁ : o → n
r₂ : l₂ → l
c₂ : o₂ → o
⊢ (A.submatrix r₁ c₁).submatrix r₂ c₂ = A.submatrix (r₁ ∘ r₂) (c₁ ∘ c₂)

Tactic:
ext fun _ _ => rfl

Premises used: Matrix.ext, rfl
-- Module: Mathlib.LinearAlgebra.Matrix.Defs
Goal:
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type v
A : Matrix m n α
r : l → m
c : o → n
⊢ (A.submatrix r c)ᵀ = Aᵀ.submatrix c r

Tactic:
ext fun _ _ => rfl

Premises used: Matrix.ext, rfl
-- Module: Mathlib.LinearAlgebra.Matrix.Defs
Goal:
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type v
inst : Add α
A B : Matrix m n α
⊢ (A + B).submatrix = HAdd.hAdd (α := (r : l → m) → (c : o → n) → Matrix l o α) A.submatrix B.submatrix

Tactic:
rfl

Premises used: Matrix.submatrix, rfl
-- Module: Mathlib.LinearAlgebra.Matrix.Defs
Goal:
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type v
inst : Neg α
A : Matrix m n α
⊢ Eq (α := (r : l → m) → (c : o → n) → Matrix l o α) (-A).submatrix (-A.submatrix)

Tactic:
rfl

Premises used: Matrix.submatrix, rfl
-- Module: Mathlib.LinearAlgebra.Matrix.Defs
Goal:
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type v
inst : Sub α
A B : Matrix m n α
⊢ (A - B).submatrix = HSub.hSub (α := (r : l → m) → (c : o → n) → Matrix l o α) A.submatrix B.submatrix

Tactic:
rfl

Premises used: Matrix.submatrix, rfl
-- Module: Mathlib.LinearAlgebra.Matrix.Defs
Goal:
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type v
inst : Zero α
⊢ Eq (α := (r : l → m) → (c : o → n) → Matrix l o α) (submatrix 0) 0

Tactic:
rfl

Premises used: Matrix.submatrix, rfl
-- Module: Mathlib.LinearAlgebra.Matrix.Defs
Goal:
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type v
R : Type u_10
inst : SMul R α
r : R
A : Matrix m n α
⊢ (r • A).submatrix = HSMul.hSMul (β := (r : l → m) → (c : o → n) → Matrix l o α) r A.submatrix

Tactic:
rfl

Premises used: Matrix.submatrix, rfl
-- Module: Mathlib.LinearAlgebra.Matrix.Defs
Goal:
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type v
β : Type w
f : α → β
e₁ : l → m
e₂ : o → n
A : Matrix m n α
⊢ (A.map f).submatrix e₁ e₂ = (A.submatrix e₁ e₂).map f

Tactic:
rfl

Premises used: Matrix.submatrix, Matrix.map, rfl
-- Module: Mathlib.LinearAlgebra.Matrix.Defs
Goal:
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
eₘ : m ≃ l
eₙ : n ≃ o
M : Matrix m n α
⊢ (fun (M : Matrix l o α) ↦ (M.submatrix (⇑eₘ : (a : m) → l) (⇑eₙ : (a : n) → o) : Matrix m n α))
      ((fun (M : Matrix m n α) ↦ (M.submatrix (⇑eₘ.symm : (a : l) → m) (⇑eₙ.symm : (a : o) → n) : Matrix l o α)) M) =
    M

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Matrix.Defs
Goal:
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
eₘ : m ≃ l
eₙ : n ≃ o
M : Matrix l o α
⊢ (fun (M : Matrix m n α) ↦ (M.submatrix (⇑eₘ.symm : (a : l) → m) (⇑eₙ.symm : (a : o) → n) : Matrix l o α))
      ((fun (M : Matrix l o α) ↦ (M.submatrix (⇑eₘ : (a : m) → l) (⇑eₙ : (a : n) → o) : Matrix m n α)) M) =
    M

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Matrix.Defs
Goal:
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type v
eₘ : m ≃ l
eₙ : n ≃ o
M : Matrix m n α
⊢ Eq (α := Matrix l o α) ((reindex eₘ eₙ : (a : Matrix m n α) → Matrix l o α) M : Matrix l o α)
    (M.submatrix (⇑eₘ.symm : (a : l) → m) (⇑eₙ.symm : (a : o) → n) : Matrix l o α)

Tactic:
rfl

Premises used: Matrix.submatrix, rfl
-- Module: Mathlib.LinearAlgebra.Matrix.Defs
Goal:
m : Type u_2
n : Type u_3
α : Type v
A : Matrix m n α
⊢ (reindex (Equiv.refl m) (Equiv.refl n) : (a : Matrix m n α) → Matrix m n α) A = A

Tactic:
A.submatrix_id_id

Premises used: Matrix.submatrix, Matrix.submatrix_id_id
-- Module: Mathlib.LinearAlgebra.Matrix.Defs
Goal:
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type v
eₘ : m ≃ l
eₙ : n ≃ o
⊢ Eq (α := Matrix l o α ≃ Matrix m n α) (Equiv.symm (reindex eₘ eₙ)) (reindex eₘ.symm eₙ.symm)

Tactic:
rfl

Premises used: Matrix.submatrix, Matrix.reindex, Equiv.symm, rfl
-- Module: Mathlib.LinearAlgebra.Matrix.Defs
Goal:
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type v
l₂ : Type u_10
o₂ : Type u_11
eₘ : m ≃ l
eₙ : n ≃ o
eₘ₂ : l ≃ l₂
eₙ₂ : o ≃ o₂
⊢ Eq (α := Matrix m n α ≃ Matrix l₂ o₂ α) (Equiv.trans (reindex eₘ eₙ) (reindex eₘ₂ eₙ₂))
    (reindex (eₘ.trans eₘ₂) (eₙ.trans eₙ₂))

Tactic:
Equiv.ext fun A => (A.submatrix_submatrix eₘ.symm eₙ.symm eₘ₂.symm eₙ₂.symm :)

Premises used: Equiv.ext, Matrix.submatrix_submatrix, Equiv.symm, DFunLike.coe
-- Module: Mathlib.LinearAlgebra.Matrix.Defs
Goal:
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type v
eₘ : m ≃ l
eₙ : n ≃ o
M : Matrix m n α
⊢ Eq (α := Matrix o l α) ((reindex eₘ eₙ : (a : Matrix m n α) → Matrix l o α) M)ᵀ
    ((reindex eₙ eₘ : (a : Matrix n m α) → Matrix o l α) Mᵀ)

Tactic:
rfl

Premises used: Matrix.submatrix, Matrix.transpose, rfl
-- Module: Mathlib.LinearAlgebra.Matrix.Defs
Goal:
m : Type u_2
n : Type u_3
α : Type v
A : Matrix m n α
⊢ A.row = (Equiv.symm of : (a : Matrix m n α) → m → n → α) A

Tactic:
rfl

Premises used: Matrix.row, rfl
-- Module: Mathlib.LinearAlgebra.Matrix.Defs
Goal:
m : Type u_2
n : Type u_3
α : Type v
A : Matrix m n α
⊢ A.col = (Equiv.symm of : (a : Matrix n m α) → n → m → α) Aᵀ

Tactic:
rfl

Premises used: Matrix.transpose, Matrix.col, rfl
-- Module: Mathlib.LinearAlgebra.Matrix.Defs
Goal:
m : Type u_2
n : Type u_3
α : Type v
f : m → n → α
⊢ row ((of : (a : m → n → α) → Matrix m n α) f) = f

Tactic:
rfl

Premises used: Matrix.row, rfl
-- Module: Mathlib.LinearAlgebra.Matrix.Defs
Goal:
m : Type u_2
n : Type u_3
α : Type v
f : m → n → α
⊢ col ((of : (a : m → n → α) → Matrix m n α) f)ᵀ = f

Tactic:
rfl

Premises used: Matrix.transpose, Matrix.col, rfl
-- Module: Mathlib.LinearAlgebra.Matrix.Defs
Goal:
m : Type u_2
n : Type u_3
α : Type v
A : Matrix m n α
⊢ A.row = fun (i : m) ↦ A i

Tactic:
rfl

Premises used: Matrix.row, rfl
-- Module: Mathlib.LinearAlgebra.Matrix.Defs
Goal:
m : Type u_2
n : Type u_3
α : Type v
A : Matrix m n α
⊢ A.col = fun (j : n) ↦ Aᵀ j

Tactic:
rfl

Premises used: Matrix.col, rfl
-- Module: Mathlib.LinearAlgebra.Matrix.Defs
Goal:
m : Type u_2
n : Type u_3
α : Type v
A : Matrix m n α
i : m
j : n
⊢ A.row i j = A i j

Tactic:
rfl

Premises used: Matrix.row, rfl
-- Module: Mathlib.LinearAlgebra.Matrix.Defs
Goal:
m : Type u_2
n : Type u_3
α : Type v
A : Matrix m n α
i : m
⊢ A.row i = A i

Tactic:
rfl

Premises used: Matrix.row, rfl
-- Module: Mathlib.LinearAlgebra.Matrix.Defs
Goal:
m : Type u_2
n : Type u_3
α : Type v
A : Matrix m n α
i : n
j : m
⊢ A.col i j = A j i

Tactic:
rfl

Premises used: Matrix.transpose, Matrix.col, rfl
-- Module: Mathlib.LinearAlgebra.Matrix.Defs
Goal:
m : Type u_2
n : Type u_3
α : Type v
A : Matrix m n α
i : n
⊢ A.col i = fun (j : m) ↦ A j i

Tactic:
rfl

Premises used: Matrix.transpose, Matrix.col, rfl
-- Module: Mathlib.LinearAlgebra.Matrix.Defs
Goal:
m : Type u_2
n : Type u_3
α : Type v
A B : Matrix m n α
h : ∀ (i : m), A.row i = B.row i
⊢ A = B

Tactic:
ext fun i j => congr_fun (h i) j

Premises used: congr_fun, Matrix.ext
-- Module: Mathlib.LinearAlgebra.Matrix.Defs
Goal:
m : Type u_2
n : Type u_3
α : Type v
A B : Matrix m n α
h : ∀ (j : n), A.col j = B.col j
⊢ A = B

Tactic:
ext fun i j => congr_fun (h j) i

Premises used: congr_fun, Matrix.ext
-- Module: Mathlib.LinearAlgebra.Matrix.Defs
Goal:
m : Type u_2
n : Type u_3
α : Type v
m₀ : Type u_10
n₀ : Type u_11
A : Matrix m n α
r : m₀ → m
c : n₀ → n
i : m₀
⊢ (A.submatrix r c).row i = (A.submatrix id c).row (r i)

Tactic:
rfl

Premises used: Matrix.submatrix, Matrix.row, rfl
-- Module: Mathlib.LinearAlgebra.Matrix.Defs
Goal:
m : Type u_2
n : Type u_3
α : Type v
m₀ : Type u_10
n₀ : Type u_11
A : Matrix m n α
r : m₀ → m
c : n₀ → n
i : m₀
⊢ (A.submatrix r c).row i = A.row (r i) ∘ c

Tactic:
rfl

Premises used: Matrix.submatrix, Matrix.row, rfl
-- Module: Mathlib.LinearAlgebra.Matrix.Defs
Goal:
m : Type u_2
n : Type u_3
α : Type v
m₀ : Type u_10
n₀ : Type u_11
A : Matrix m n α
r : m₀ → m
c : n₀ → n
j : n₀
⊢ (A.submatrix r c).col j = (A.submatrix r id).col (c j)

Tactic:
rfl

Premises used: Matrix.submatrix, Matrix.transpose, Matrix.col, rfl
-- Module: Mathlib.LinearAlgebra.Matrix.Defs
Goal:
m : Type u_2
n : Type u_3
α : Type v
m₀ : Type u_10
n₀ : Type u_11
A : Matrix m n α
r : m₀ → m
c : n₀ → n
j : n₀
⊢ (A.submatrix r c).col j = A.col (c j) ∘ r

Tactic:
rfl

Premises used: Matrix.submatrix, Matrix.transpose, Matrix.col, rfl
-- Module: Mathlib.LinearAlgebra.Matrix.Defs
Goal:
m : Type u_2
n : Type u_3
α : Type v
β : Type w
A : Matrix m n α
f : α → β
i : m
⊢ (A.map f).row i = f ∘ A.row i

Tactic:
rfl

Premises used: Matrix.map, Matrix.row, rfl
-- Module: Mathlib.LinearAlgebra.Matrix.Defs
Goal:
m : Type u_2
n : Type u_3
α : Type v
β : Type w
A : Matrix m n α
f : α → β
j : n
⊢ (A.map f).col j = f ∘ A.col j

Tactic:
rfl

Premises used: Matrix.transpose, Matrix.map, Matrix.col, rfl
-- Module: Mathlib.LinearAlgebra.Matrix.Defs
Goal:
m : Type u_2
n : Type u_3
α : Type v
A : Matrix m n α
⊢ Aᵀ.row = A.col

Tactic:
rfl

Premises used: Matrix.transpose, Matrix.row, Matrix.col, rfl
-- Module: Mathlib.LinearAlgebra.Matrix.Defs
Goal:
m : Type u_2
n : Type u_3
α : Type v
A : Matrix m n α
⊢ Aᵀ.col = A.row

Tactic:
rfl

Premises used: Matrix.transpose, Matrix.row, Matrix.col, rfl
-- Module: Mathlib.LinearAlgebra.Matrix.Defs
Goal:
m : Type u_2
n : Type u_3
α : Type v
S : Set α
M : Matrix m n α
⊢ Membership.mem (γ := Set (Matrix m n α)) S.matrix M ↔ ∀ (i : m) (j : n), M i j ∈ S

Tactic:
.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Set.matrix
-- Module: Mathlib.LinearAlgebra.Matrix.Defs
Goal:
m : Type u_2
n : Type u_3
α : Type v
S : Set α
h :
  ∀ (x : Matrix m n α),
    Membership.mem (γ := Set (Matrix m n α)) S.matrix x ↔
      Membership.mem (γ := Set (Matrix m n α))
        (preimage (β := m → n → α) (⇑(Equiv.symm of) : (a : Matrix m n α) → m → n → α)
          (pi (α := fun (a : m) ↦ n → α) univ fun (x : m) ↦ pi (α := fun (a : n) ↦ α) univ fun (x : n) ↦ S))
        x
⊢ Eq (α := Set (Matrix m n α)) S.matrix
    (preimage (β := m → n → α) (⇑(Equiv.symm of) : (a : Matrix m n α) → m → n → α)
      (pi (α := fun (a : m) ↦ n → α) univ fun (x : m) ↦ pi (α := fun (a : n) ↦ α) univ fun (x : n) ↦ S))

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.Matrix.Defs
Goal:
m : Type u_2
n : Type u_3
α : Type v
S : Set α
x : Matrix m n α
⊢ Membership.mem (γ := Set (Matrix m n α)) S.matrix x ↔
    Membership.mem (γ := Set (Matrix m n α))
      (preimage (β := m → n → α) (⇑(Equiv.symm of) : (a : Matrix m n α) → m → n → α)
        (pi (α := fun (a : m) ↦ n → α) univ fun (x : m) ↦ pi (α := fun (a : n) ↦ α) univ fun (x : n) ↦ S))
      x

Tactic:
simp [Set.mem_matrix]

Premises used: Set.mem_matrix
-- Module: Mathlib.LinearAlgebra.Matrix.Defs
Goal:
m : Type u_2
n : Type u_3
α : Type v
S : Set α
M : Matrix m n α
⊢ Membership.mem (γ := Set (Matrix n m α)) S.matrix Mᵀ ↔ Membership.mem (γ := Set (Matrix m n α)) S.matrix M

Tactic:
forall_comm

Premises used: Set.Mem, setOf, forall_comm, Matrix.transpose, Set.matrix
-- Module: Mathlib.LinearAlgebra.Matrix.Defs
Goal:
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type v
S : Set α
M : Matrix m n α
r : l → m
c : o → n
hM : Membership.mem (γ := Set (Matrix m n α)) S.matrix M
⊢ Membership.mem (γ := Set (Matrix l o α)) S.matrix (M.submatrix r c)

Tactic:
simp_all [Set.mem_matrix]

Premises used: Set.mem_matrix
-- Module: Mathlib.LinearAlgebra.Matrix.Defs
Goal:
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type v
S : Set α
M : Matrix m n α
r : l → m
c : o → n
hr : Function.Surjective r
hc : Function.Surjective c
⊢ Membership.mem (γ := Set (Matrix l o α)) S.matrix (M.submatrix r c) ↔
    Membership.mem (γ := Set (Matrix m n α)) S.matrix M

Tactic:
⟨(hr.forall.mpr fun _ => hc.forall.mpr fun _ => · _ _), submatrix_mem_matrix⟩

Premises used: Iff.mpr, Function.Surjective.forall, Iff.intro, Matrix.submatrix_mem_matrix
-- Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic
Goal:
n : Type u_2
inst : DecidableEq n
inst_1 : Fintype n
R : Type v
inst_2 : CommRing R
M : Matrix n n R
⊢ M.det =
    ∑ σ : Perm n,
      HSMul.hSMul (α := ℤˣ) (β := R) (((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) σ : ℤˣ)
        (∏ i : n, M ((σ : (a : n) → n) i) i)

Tactic:
MultilinearMap.alternatization_apply _ M

Premises used: Multiset.foldr, Multiset.prod, Finset.prod, MultilinearMap.alternatization_apply, Matrix.det
-- Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic
Goal:
n : Type u_2
inst : DecidableEq n
inst_1 : Fintype n
R : Type v
inst_2 : CommRing R
M : Matrix n n R
⊢ M.det =
    ∑ σ : Perm n,
      HMul.hMul (α := R) (↑(↑(((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) σ) : ℤ) : R)
        (∏ i : n, M ((σ : (a : n) → n) i) i)

Tactic:
simp [det_apply, Units.smul_def]

Premises used: Matrix.det_apply, Units.smul_def
-- Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic
Goal:
n : Type u_2
inst : DecidableEq n
inst_1 : Fintype n
R : Type v
inst_2 : CommRing R
M : Matrix n n R
rw :
  HAdd.hAdd (α := R)
      (∑ x ∈ ofSign 1,
        HSMul.hSMul (α := ℤˣ) (β := R)
          (((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) ((Equiv.inv (Perm n) : (a : Perm n) → Perm n) x) : ℤˣ)
          (∏ i : n, M ((((Equiv.inv (Perm n) : (a : Perm n) → Perm n) x : Perm n) : (a : n) → n) i) i))
      (∑ x ∈ ofSign (-1),
        HSMul.hSMul (α := ℤˣ) (β := R)
          (((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) ((Equiv.inv (Perm n) : (a : Perm n) → Perm n) x) : ℤˣ)
          (∏ i : n, M ((((Equiv.inv (Perm n) : (a : Perm n) → Perm n) x : Perm n) : (a : n) → n) i) i)) =
    detp 1 M - detp (-1) M
⊢ M.det = detp 1 M - detp (-1) M

Tactic:
rw [det_apply, ← Equiv.sum_comp (Equiv.inv (Perm n)), ← ofSign_disjUnion, sum_disjUnion]

Premises used: Matrix.det_apply, Equiv.inv, Equiv.sum_comp, Finset.sum_disjUnion, Equiv.Perm, Equiv.Perm.ofSign_disjUnion
-- Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic
Goal:
n : Type u_2
inst : DecidableEq n
inst_1 : Fintype n
R : Type v
inst_2 : CommRing R
M : Matrix n n R
simp_rw :
  HAdd.hAdd (α := R)
      (∑ x ∈ ofSign 1,
        HSMul.hSMul (α := ℤˣ) (β := R) (((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) x : ℤˣ)
          (∏ x_1 : n, M ((x⁻¹ : (a : n) → n) x_1) x_1))
      (∑ x ∈ ofSign (-1),
        HSMul.hSMul (α := ℤˣ) (β := R) (((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) x : ℤˣ)
          (∏ x_1 : n, M ((x⁻¹ : (a : n) → n) x_1) x_1)) =
    HAdd.hAdd (α := R) (∑ σ ∈ ofSign 1, ∏ k : n, M k ((σ : (a : n) → n) k))
      (∑ x ∈ ofSign (-1), -∏ k : n, M k ((x : (a : n) → n) k))
⊢ HAdd.hAdd (α := R)
      (∑ x ∈ ofSign 1,
        HSMul.hSMul (α := ℤˣ) (β := R)
          (((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) ((Equiv.inv (Perm n) : (a : Perm n) → Perm n) x) : ℤˣ)
          (∏ i : n, M ((((Equiv.inv (Perm n) : (a : Perm n) → Perm n) x : Perm n) : (a : n) → n) i) i))
      (∑ x ∈ ofSign (-1),
        HSMul.hSMul (α := ℤˣ) (β := R)
          (((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) ((Equiv.inv (Perm n) : (a : Perm n) → Perm n) x) : ℤˣ)
          (∏ i : n, M ((((Equiv.inv (Perm n) : (a : Perm n) → Perm n) x : Perm n) : (a : n) → n) i) i)) =
    detp 1 M - detp (-1) M

Tactic:
simp_rw [inv_apply, sign_inv, sub_eq_add_neg, detp, ← sum_neg_distrib]

Premises used: sub_eq_add_neg, Matrix.detp, Equiv.inv_apply, Equiv.Perm.sign_inv, Finset.sum_neg_distrib
-- Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic
Goal:
n : Type u_2
inst : DecidableEq n
inst_1 : Fintype n
R : Type v
inst_2 : CommRing R
M : Matrix n n R
⊢ HAdd.hAdd (α := R)
      (∑ x ∈ ofSign 1,
        HSMul.hSMul (α := ℤˣ) (β := R) (((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) x : ℤˣ)
          (∏ x_1 : n, M ((x⁻¹ : (a : n) → n) x_1) x_1))
      (∑ x ∈ ofSign (-1),
        HSMul.hSMul (α := ℤˣ) (β := R) (((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) x : ℤˣ)
          (∏ x_1 : n, M ((x⁻¹ : (a : n) → n) x_1) x_1)) =
    HAdd.hAdd (α := R) (∑ σ ∈ ofSign 1, ∏ k : n, M k ((σ : (a : n) → n) k))
      (∑ x ∈ ofSign (-1), -∏ k : n, M k ((x : (a : n) → n) k))

Tactic:
congr_arg₂ (· + ·) (sum_congr rfl fun σ hσ ↦ ?_) (sum_congr rfl fun σ hσ ↦ ?_)

Premises used: HAdd.hAdd, Finset.sum_congr, rfl, congr_arg₂
-- Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic
Goal:
n : Type u_2
inst : DecidableEq n
inst_1 : Fintype n
R : Type v
inst_2 : CommRing R
M : Matrix n n R
refine_1 :
  ∀ (σ : Perm n) (hσ : Membership.mem (γ := Finset (Perm n)) (ofSign 1) σ),
    HSMul.hSMul (α := ℤˣ) (β := R) (((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) σ : ℤˣ)
        (∏ x : n, M ((σ⁻¹ : (a : n) → n) x) x) =
      ∏ k : n, M k ((σ : (a : n) → n) k)
refine_2 :
  ∀ (σ : Perm n) (hσ : Membership.mem (γ := Finset (Perm n)) (ofSign (-1)) σ),
    HSMul.hSMul (α := ℤˣ) (β := R) (((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) σ : ℤˣ)
        (∏ x : n, M ((σ⁻¹ : (a : n) → n) x) x) =
      -∏ k : n, M k ((σ : (a : n) → n) k)
⊢ HAdd.hAdd (α := R)
      (∑ x ∈ ofSign 1,
        HSMul.hSMul (α := ℤˣ) (β := R) (((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) x : ℤˣ)
          (∏ x_1 : n, M ((x⁻¹ : (a : n) → n) x_1) x_1))
      (∑ x ∈ ofSign (-1),
        HSMul.hSMul (α := ℤˣ) (β := R) (((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) x : ℤˣ)
          (∏ x_1 : n, M ((x⁻¹ : (a : n) → n) x_1) x_1)) =
    HAdd.hAdd (α := R) (∑ σ ∈ ofSign 1, ∏ k : n, M k ((σ : (a : n) → n) k))
      (∑ x ∈ ofSign (-1), -∏ k : n, M k ((x : (a : n) → n) k))

Tactic:
refine congr_arg₂ (· + ·) (sum_congr rfl fun σ hσ ↦ ?_) (sum_congr rfl fun σ hσ ↦ ?_)

Premises used: HAdd.hAdd, Finset.sum_congr, rfl, congr_arg₂
-- Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic
Goal:
n : Type u_2
inst : DecidableEq n
inst_1 : Fintype n
R : Type v
inst_2 : CommRing R
M : Matrix n n R
σ : Perm n
hσ : Membership.mem (γ := Finset (Perm n)) (ofSign 1) σ
refine_1 :
  HSMul.hSMul (α := ℤˣ) (β := R) 1 (∏ i : n, M ((σ⁻¹ : (a : n) → n) ((σ : (a : n) → n) i : n)) ((σ : (a : n) → n) i)) =
    ∏ k : n, M k ((σ : (a : n) → n) k)
⊢ HSMul.hSMul (α := ℤˣ) (β := R) (((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) σ : ℤˣ)
      (∏ x : n, M ((σ⁻¹ : (a : n) → n) x) x) =
    ∏ k : n, M k ((σ : (a : n) → n) k)

Tactic:
rw [mem_ofSign.mp hσ, ← Equiv.prod_comp σ]

Premises used: Equiv.Perm.mem_ofSign, Equiv.prod_comp, Iff.mp
-- Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic
Goal:
n : Type u_2
inst : DecidableEq n
inst_1 : Fintype n
R : Type v
inst_2 : CommRing R
M : Matrix n n R
σ : Perm n
hσ : Membership.mem (γ := Finset (Perm n)) (ofSign (-1)) σ
refine_2 :
  HSMul.hSMul (α := ℤˣ) (β := R) (-1)
      (∏ i : n, M ((σ⁻¹ : (a : n) → n) ((σ : (a : n) → n) i : n)) ((σ : (a : n) → n) i)) =
    -∏ k : n, M k ((σ : (a : n) → n) k)
⊢ HSMul.hSMul (α := ℤˣ) (β := R) (((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) σ : ℤˣ)
      (∏ x : n, M ((σ⁻¹ : (a : n) → n) x) x) =
    -∏ k : n, M k ((σ : (a : n) → n) k)

Tactic:
rw [mem_ofSign.mp hσ, ← Equiv.prod_comp σ]

Premises used: Equiv.Perm.mem_ofSign, Equiv.prod_comp, Iff.mp
-- Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic
Goal:
n : Type u_2
inst : DecidableEq n
inst_1 : Fintype n
R : Type v
inst_2 : CommRing R
M : Matrix n n R
σ : Perm n
hσ : Membership.mem (γ := Finset (Perm n)) (ofSign 1) σ
⊢ HSMul.hSMul (α := ℤˣ) (β := R) 1 (∏ i : n, M ((σ⁻¹ : (a : n) → n) ((σ : (a : n) → n) i : n)) ((σ : (a : n) → n) i)) =
    ∏ k : n, M k ((σ : (a : n) → n) k)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic
Goal:
n : Type u_2
inst : DecidableEq n
inst_1 : Fintype n
R : Type v
inst_2 : CommRing R
M : Matrix n n R
σ : Perm n
hσ : Membership.mem (γ := Finset (Perm n)) (ofSign (-1)) σ
⊢ HSMul.hSMul (α := ℤˣ) (β := R) (-1)
      (∏ i : n, M ((σ⁻¹ : (a : n) → n) ((σ : (a : n) → n) i : n)) ((σ : (a : n) → n) i)) =
    -∏ k : n, M k ((σ : (a : n) → n) k)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic
Goal:
n : Type u_2
inst : DecidableEq n
inst_1 : Fintype n
R : Type v
inst_2 : CommRing R
d : n → R
rw :
  Eq.{v + 1} (α := R)
    (∑ σ : Perm n,
      HMul.hMul (α := R) (↑(↑(((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) σ) : ℤ) : R)
        (∏ i : n, diagonal d ((σ : (a : n) → n) i) i))
    (∏ i : n, d i)
⊢ (diagonal d).det = ∏ i : n, d i

Tactic:
rw [det_apply']

Premises used: Matrix.det_apply'
-- Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic
Goal:
n : Type u_2
inst : DecidableEq n
inst_1 : Fintype n
R : Type v
inst_2 : CommRing R
d : n → R
⊢ Eq.{v + 1} (α := R)
    (∑ σ : Perm n,
      HMul.hMul (α := R) (↑(↑(((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) σ) : ℤ) : R)
        (∏ i : n, diagonal d ((σ : (a : n) → n) i) i))
    (∏ i : n, d i)

Tactic:
(Finset.sum_eq_single 1 ?_ ?_).trans ?_

Premises used: Finset.sum_eq_single, OfNat.ofNat, Eq.trans
-- Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic
Goal:
n : Type u_2
inst : DecidableEq n
inst_1 : Fintype n
R : Type v
inst_2 : CommRing R
d : n → R
refine_1 :
  ∀ (b : Perm n),
    Membership.mem (γ := Finset (Perm n)) univ b →
      b ≠ 1 →
        HMul.hMul (α := R) (↑(↑(((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) b) : ℤ) : R)
            (∏ i : n, diagonal d ((b : (a : n) → n) i) i) =
          0
refine_2 :
  1 ∉ univ →
    HMul.hMul (α := R) (↑(↑(((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) 1) : ℤ) : R)
        (∏ i : n, diagonal d ((1 : (a : n) → n) i) i) =
      0
refine_3 :
  HMul.hMul (α := R) (↑(↑(((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) 1) : ℤ) : R)
      (∏ i : n, diagonal d ((1 : (a : n) → n) i) i) =
    ∏ i : n, d i
⊢ Eq.{v + 1} (α := R)
    (∑ σ : Perm n,
      HMul.hMul (α := R) (↑(↑(((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) σ) : ℤ) : R)
        (∏ i : n, diagonal d ((σ : (a : n) → n) i) i))
    (∏ i : n, d i)

Tactic:
refine (Finset.sum_eq_single 1 ?_ ?_).trans ?_

Premises used: Finset.sum_eq_single, OfNat.ofNat, Eq.trans
-- Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic
Goal:
n : Type u_2
inst : DecidableEq n
inst_1 : Fintype n
R : Type v
inst_2 : CommRing R
d : n → R
σ : Perm n
h2 : σ ≠ 1
refine_1 :
  ∀ (x : n) (h3 : ¬Eq (α := n) ((σ : (a : n) → n) x : n) ((1 : (a : n) → n) x : n)),
    HMul.hMul (α := R) (↑(↑(((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) σ) : ℤ) : R)
        (∏ i : n, diagonal d ((σ : (a : n) → n) i) i) =
      0
⊢ HMul.hMul (α := R) (↑(↑(((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) σ) : ℤ) : R)
      (∏ i : n, diagonal d ((σ : (a : n) → n) i) i) =
    0

Tactic:
obtain ⟨x, h3⟩ := not_forall.1 (mt Equiv.ext h2)

Premises used: mt, Equiv.ext, Iff.mp, Classical.not_forall
-- Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic
Goal:
n : Type u_2
inst : DecidableEq n
inst_1 : Fintype n
R : Type v
inst_2 : CommRing R
d : n → R
σ : Perm n
h2 : σ ≠ 1
x : n
h3 : ¬Eq (α := n) ((σ : (a : n) → n) x : n) ((1 : (a : n) → n) x : n)
⊢ HMul.hMul (α := R) (↑(↑(((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) σ) : ℤ) : R) 0 = 0

Tactic:
mul_zero (ε σ)

Premises used: Int.cast, Units.val, Equiv.Perm.sign, MulZeroClass.mul_zero, DFunLike.coe
-- Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic
Goal:
n : Type u_2
inst : DecidableEq n
inst_1 : Fintype n
R : Type v
inst_2 : CommRing R
d : n → R
σ : Perm n
h2 : σ ≠ 1
x : n
h3 : ¬Eq (α := n) ((σ : (a : n) → n) x : n) ((1 : (a : n) → n) x : n)
h : Eq.{v + 1} (α := R) (∏ i : n, diagonal d ((σ : (a : n) → n) i) i) 0
⊢ HMul.hMul (α := R) (↑(↑(((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) σ) : ℤ) : R)
      (∏ i : n, diagonal d ((σ : (a : n) → n) i) i) =
    0

Tactic:
convert! mul_zero (ε σ)