awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
α : Type u_3
inst_3 : Monoid α
inst_4 : MulAction α R
inst_5 : IsScalarTower α R R
inst_6 : SMulCommClass α R R
c : α
A : Matrix n n R
rw : (HSMul.hSMul (β := R) c 1 • A).det = c ^ Fintype.card n • A.det
rw₁ : HSMul.hSMul (β := R) c 1 ^ Fintype.card n * A.det = c ^ Fintype.card n • A.det
rw₂ : c ^ Fintype.card n • HPow.hPow (α := R) 1 (Fintype.card n) * A.det = c ^ Fintype.card n • A.det
rw₃ : HSMul.hSMul (β := R) (c ^ Fintype.card n) 1 * A.det = c ^ Fintype.card n • A.det
rw₄ : c ^ Fintype.card n • (1 * A.det) = c ^ Fintype.card n • A.det
rw₅ rw₆ : c ^ Fintype.card n • A.det = c ^ Fintype.card n • A.det
⊢ (c • A).det = c ^ Fintype.card n • A.det

Tactic:
rw [← smul_one_smul R c A, det_smul, smul_pow, one_pow, smul_mul_assoc, one_mul]

Premises used: one_pow, Matrix.det_smul, smul_mul_assoc, smul_one_smul, smul_pow, one_mul
-- 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
A : Matrix n n R
rw : (-A).det = (HSMul.hSMul (α := R) (-1) A).det
rw₁ rw₂ : (-A).det = (-A).det
⊢ (-A).det = HPow.hPow (α := R) (-1) (Fintype.card n) * A.det

Tactic:
rw [← det_smul, neg_one_smul]

Premises used: neg_one_smul, Matrix.det_smul
-- 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
A : Matrix n n R
rw : (-A).det = (HSMul.hSMul (α := ℤˣ) (-1) A).det
rw₁ : (-A).det = (-HSMul.hSMul (α := ℤˣ) 1 A).det
rw₂ rw₃ : (-A).det = (-A).det
⊢ (-A).det = HPow.hPow (α := ℤˣ) (-1) (Fintype.card n) • A.det

Tactic:
rw [← det_smul_of_tower, Units.neg_smul, one_smul]

Premises used: Matrix.det_smul_of_tower, one_smul, Units.neg_smul
-- 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
v : n → R
A : Matrix n n R
a : ∀ (i j : n), (of : (a : n → n → R) → Matrix n n R) (fun (i j : n) ↦ v j * A i j) i j = (A * diagonal v) i j
⊢ ((of : (a : n → n → R) → Matrix n n R) fun (i j : n) ↦ v j * A i j) = A * diagonal v

Tactic:
ext
-- 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
v : n → R
A : Matrix n n R
i j : n
⊢ (of : (a : n → n → R) → Matrix n n R) (fun (i j : n) ↦ v j * A i j) i j = (A * diagonal v) i j

Tactic:
simp [mul_comm]

Premises used: mul_comm
-- 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
v : n → R
A : Matrix n n R
rw : A.det * (diagonal v).det = (∏ i : n, v i) * A.det
rw₁ : A.det * ∏ i : n, v i = (∏ i : n, v i) * A.det
rw₂ rw₃ : (∏ i : n, v i) * A.det = (∏ i : n, v i) * A.det
⊢ (A * diagonal v).det = (∏ i : n, v i) * A.det

Tactic:
rw [det_mul, det_diagonal, mul_comm]

Premises used: Matrix.det_diagonal, Matrix.det_mul, mul_comm
-- 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
v : n → R
A : Matrix n n R
⊢ det.{v, u_2} (n := n) ((of : (a : n → n → R) → Matrix n n R) fun (i j : n) ↦ v i * A i j) = (∏ i : n, v i) * A.det

Tactic:
MultilinearMap.map_smul_univ _ v A

Premises used: MultilinearMap.map_smul_univ, Matrix.det
-- Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic
Goal:
m : Type u_1
inst : DecidableEq m
inst_1 : Fintype m
R : Type v
inst_2 : CommRing R
M : Matrix m m R
n : ℕ
⊢ (M ^ n).det = M.det ^ n

Tactic:
(detMonoidHom : Matrix m m R →* R).map_pow M n

Premises used: Matrix.detMonoidHom, Matrix.det, MonoidHom.map_pow
-- 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
S : Type w
inst_3 : CommRing S
f : R →+* S
M : Matrix n n R
⊢ Eq.{w + 1} (α := S) ((f : (a : R) → S) M.det : S)
    (det.{w, u_2} (n := n) ((f.mapMatrix : (a : Matrix n n R) → Matrix n n S) M) : S)

Tactic:
simp [Matrix.det_apply', map_sum f, map_prod f]

Premises used: map_sum, map_prod, 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
S : Type w
inst_3 : CommRing S
f : R ≃+* S
M : Matrix n n R
⊢ Eq.{w + 1} (α := S) ((f : (a : R) → S) M.det : S)
    (det.{w, u_2} (n := n) ((f.mapMatrix : (a : Matrix n n R) → Matrix n n S) M) : S)

Tactic:
f.toRingHom.map_det _

Premises used: RingHom.map_det, RingEquiv.toRingHom, Matrix.map
-- 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
S : Type w
inst_3 : CommRing S
inst_4 : Algebra R S
T : Type z
inst_5 : CommRing T
inst_6 : Algebra R T
f : S →ₐ[R] T
M : Matrix n n S
⊢ Eq.{z + 1} (α := T) ((f : (a : S) → T) M.det : T)
    (det.{z, u_2} (n := n) ((f.mapMatrix : (a : Matrix n n S) → Matrix n n T) M) : T)

Tactic:
f.toRingHom.map_det _

Premises used: RingHom.map_det, AlgHom.toRingHom
-- 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
S : Type w
inst_3 : CommRing S
inst_4 : Algebra R S
T : Type z
inst_5 : CommRing T
inst_6 : Algebra R T
f : S ≃ₐ[R] T
M : Matrix n n S
⊢ Eq.{z + 1} (α := T) ((f : (a : S) → T) M.det : T)
    (det.{z, u_2} (n := n) ((f.mapMatrix : (a : Matrix n n S) → Matrix n n T) M) : T)

Tactic:
f.toAlgHom.map_det _

Premises used: AlgEquiv.toAlgHom, AlgHom.map_det, Matrix.map
-- 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 ℤ
⊢ Eq.{v + 1} (α := R) (↑M.det : R) (det (M.map fun (x : ℤ) ↦ (↑x : R)))

Tactic:
Int.castRingHom R |>.map_det M

Premises used: RingHom.map_det, Int.castRingHom, Matrix.map
-- Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic
Goal:
n : Type u_2
inst : DecidableEq n
inst_1 : Fintype n
F : Type u_3
inst_2 : Field F
inst_3 : CharZero F
M : Matrix n n ℚ
⊢ Eq.{u_3 + 1} (α := F) (↑M.det : F) (det (M.map fun (x : ℚ) ↦ (↑x : F)))

Tactic:
Rat.castHom F |>.map_det M

Premises used: RingHom.map_det, Matrix.map, Rat.castHom
-- Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic
Goal:
m : Type u_1
inst : DecidableEq m
inst_1 : Fintype m
R : Type v
inst_2 : CommRing R
inst_3 : StarRing R
M : Matrix m m R
⊢ Mᴴ.det = star M.det

Tactic:
((starRingEnd R).map_det _).symm.trans <| congr_arg star M.det_transpose

Premises used: Matrix.det_transpose, congr_arg, RingHom.map_det, Matrix.map, starRingEnd, Eq.symm, Matrix.conjTranspose, Eq.trans, Star.star
-- 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
A : Matrix n n R
i : n
h : ∀ (j : n), A i j = 0
⊢ A.det = 0

Tactic:
(detRowAlternating : (n → R) [⋀^n]→ₗ[R] R).map_coord_zero i (funext h)

Premises used: Matrix.detRowAlternating, funext, AlternatingMap.map_coord_zero, 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
A : Matrix n n R
j : n
h : ∀ (i : n), A i j = 0
rw : Aᵀ.det = 0
⊢ A.det = 0

Tactic:
rw [← det_transpose]

Premises used: Matrix.det_transpose
-- 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
A : Matrix n n R
j : n
h : ∀ (i : n), A i j = 0
⊢ Aᵀ.det = 0

Tactic:
det_eq_zero_of_row_eq_zero j h

Premises used: Matrix.det_eq_zero_of_row_eq_zero
-- 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
A : Matrix n n R
j : n
h : ∀ (i : n), A i j = 0
⊢ Aᵀ.det = 0

Tactic:
exact det_eq_zero_of_row_eq_zero j h

Premises used: Matrix.det_eq_zero_of_row_eq_zero
-- 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
i j : n
i_ne_j : i ≠ j
hij : M i = M j
⊢ M.det = 0

Tactic:
(detRowAlternating : (n → R) [⋀^n]→ₗ[R] R).map_eq_zero_of_eq M hij i_ne_j

Premises used: Matrix.detRowAlternating, AlternatingMap.map_eq_zero_of_eq, 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
i j : n
i_ne_j : i ≠ j
hij : ∀ (k : n), M k i = M k j
rw : Mᵀ i = Mᵀ j
⊢ M.det = 0

Tactic:
rw [← det_transpose, det_zero_of_row_eq i_ne_j]

Premises used: Matrix.det_transpose, Matrix.det_zero_of_row_eq
-- 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
i j : n
i_ne_j : i ≠ j
hij : ∀ (k : n), M k i = M k j
⊢ Mᵀ i = Mᵀ j

Tactic:
funext hij

Premises used: funext
-- 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
i j : n
i_ne_j : i ≠ j
hij : ∀ (k : n), M k i = M k j
⊢ Mᵀ i = Mᵀ j

Tactic:
exact funext hij

Premises used: funext
-- 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
i j : n
h : i ≠ j
⊢ M.updateRow j (M i) i = M.updateRow j (M i) j

Tactic:
simp [h]
-- 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
i j : n
h : i ≠ j
⊢ ∀ (k : n), M.updateCol j (fun (k : n) ↦ M k i) k i = M.updateCol j (fun (k : n) ↦ M k i) k j

Tactic:
simp [h]
-- 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
j : n
u v : n → R
⊢ (M.updateRow j (u + v)).det = (M.updateRow j u).det + (M.updateRow j v).det

Tactic:
(detRowAlternating : (n → R) [⋀^n]→ₗ[R] R).map_update_add M j u v

Premises used: Function.update, AlternatingMap.map_update_add, Matrix.detRowAlternating, dite, Matrix.det, Matrix.updateRow
-- 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
j : n
u v : n → R
rw : (Mᵀ.updateRow j u).det + (Mᵀ.updateRow j v).det = (M.updateCol j u).det + (M.updateCol j v).det
⊢ (M.updateCol j (u + v)).det = (M.updateCol j u).det + (M.updateCol j v).det

Tactic:
rw [← det_transpose, ← updateRow_transpose, det_updateRow_add]

Premises used: Matrix.det_transpose, Matrix.updateRow_transpose, Matrix.det_updateRow_add
-- 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
j : n
u v : n → R
⊢ (Mᵀ.updateRow j u).det + (Mᵀ.updateRow j v).det = (M.updateCol j u).det + (M.updateCol j v).det

Tactic:
simp [updateRow_transpose, det_transpose]

Premises used: Matrix.det_transpose, Matrix.updateRow_transpose
-- 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
j : n
s : R
u : n → R
⊢ (M.updateRow j (s • u)).det = s * (M.updateRow j u).det

Tactic:
(detRowAlternating : (n → R) [⋀^n]→ₗ[R] R).map_update_smul M j s u

Premises used: Function.update, AlternatingMap.map_update_smul, Matrix.detRowAlternating, dite, Matrix.det, Matrix.updateRow
-- 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
j : n
s : R
u : n → R
rw : s * (Mᵀ.updateRow j u).det = s * (M.updateCol j u).det
⊢ (M.updateCol j (s • u)).det = s * (M.updateCol j u).det

Tactic:
rw [← det_transpose, ← updateRow_transpose, det_updateRow_smul]

Premises used: Matrix.det_transpose, Matrix.updateRow_transpose, Matrix.det_updateRow_smul
-- 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
j : n
s : R
u : n → R
⊢ s * (Mᵀ.updateRow j u).det = s * (M.updateCol j u).det

Tactic:
simp [updateRow_transpose, det_transpose]

Premises used: Matrix.det_transpose, Matrix.updateRow_transpose
-- 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
j : n
s : R
u : n → R
⊢ ((s • M).updateRow j u).det = s ^ (Fintype.card n - 1) * (M.updateRow j u).det

Tactic:
MultilinearMap.map_update_smul_left _ M j s u

Premises used: Function.update, MultilinearMap.map_update_smul_left, dite, Matrix.det, Matrix.updateRow
-- 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
j : n
s : R
u : n → R
rw : s ^ (Fintype.card n - 1) * (Mᵀ.updateRow j u).det = s ^ (Fintype.card n - 1) * (M.updateCol j u).det
⊢ ((s • M).updateCol j u).det = s ^ (Fintype.card n - 1) * (M.updateCol j u).det

Tactic:
rw [← det_transpose, ← updateRow_transpose, transpose_smul, det_updateRow_smul_left]

Premises used: Matrix.det_transpose, Matrix.det_updateRow_smul_left, Matrix.updateRow_transpose, Matrix.transpose_smul
-- 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
j : n
s : R
u : n → R
⊢ s ^ (Fintype.card n - 1) * (Mᵀ.updateRow j u).det = s ^ (Fintype.card n - 1) * (M.updateCol j u).det

Tactic:
simp [updateRow_transpose, det_transpose]

Premises used: Matrix.det_transpose, Matrix.updateRow_transpose
-- 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
j : n
c : n → R
a : R
hj : j ∉ ∅
empty : (M.updateRow j (a • M j + 0)).det = a • M.det
empty₁ : (M.updateRow j (a • M j)).det = a • M.det
empty₂ : (M.updateRow j (a • M j)).det = a * M.det
empty₃ : a * (M.updateRow j (M j)).det = a * M.det
empty₄ empty₅ : a * M.det = a * M.det
⊢ (M.updateRow j (a • M j + ∑ k ∈ ∅, c k • M k)).det = a • M.det

Tactic:
rw [Finset.sum_empty, add_zero, smul_eq_mul, det_updateRow_smul, updateRow_eq_self]

Premises used: Matrix.updateRow_eq_self, Matrix.det_updateRow_smul, Finset.sum_empty, smul_eq_mul, add_zero
-- 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
j : n
c : n → R
a : R
k : n
s : Finset n
hk : k ∉ s
h_ind : ∀ (hj : j ∉ s), (M.updateRow j (a • M j + ∑ k ∈ s, c k • M k)).det = a • M.det
hj : j ∉ insert k s
⊢ k ≠ j

Tactic:
have h : k ≠ j := fun h ↦ (h ▸ hj) (Finset.mem_insert_self _ _)
-- 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
j : n
c : n → R
a : R
k : n
s : Finset n
hk : k ∉ s
h_ind : ∀ (hj : j ∉ s), (M.updateRow j (a • M j + ∑ k ∈ s, c k • M k)).det = a • M.det
hj : j ∉ Insert.insert k s
h : k ≠ j
insert : j ∉ s
⊢ (M.updateRow j (a • M j + ∑ k ∈ Insert.insert k s, c k • M k)).det = a • M.det

Tactic:
rw [Finset.sum_insert hk, add_comm ((c k) • M k), ← add_assoc, det_updateRow_add,
        det_updateRow_smul, det_updateRow_eq_zero h, mul_zero, add_zero, h_ind]

Premises used: add_assoc, add_comm, MulZeroClass.mul_zero, Matrix.det_updateRow_eq_zero, HSMul.hSMul, Matrix.det_updateRow_smul, Finset.sum_insert, add_zero, Matrix.det_updateRow_add
-- 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
j : n
c : n → R
a : R
k : n
s : Finset n
hk : k ∉ s
h_ind : ∀ (hj : j ∉ s), (M.updateRow j (a • M j + ∑ k ∈ s, c k • M k)).det = a • M.det
hj : j ∉ insert k s
h : k ≠ j
⊢ j ∉ s

Tactic:
fun h ↦ hj (Finset.mem_insert_of_mem h)

Premises used: Finset.mem_insert_of_mem, Not
-- 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
j : n
c : n → R
a : R
k : n
s : Finset n
hk : k ∉ s
h_ind : ∀ (hj : j ∉ s), (M.updateRow j (a • M j + ∑ k ∈ s, c k • M k)).det = a • M.det
hj : j ∉ insert k s
h : k ≠ j
⊢ j ∉ s

Tactic:
exact fun h ↦ hj (Finset.mem_insert_of_mem h)

Premises used: Finset.mem_insert_of_mem
-- 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
j : n
s : Finset n
hj : j ∉ s
c : n → R
a : R
empty : ∀ (hj : j ∉ ∅), (M.updateRow j (a • M j + ∑ k ∈ ∅, c k • M k)).det = a • M.det
insert :
  ∀ (k : n) (s : Finset n) (hk : k ∉ s)
    (h_ind : ∀ (hj : j ∉ s), (M.updateRow j (a • M j + ∑ k ∈ s, c k • M k)).det = a • M.det)
    (hj : j ∉ Insert.insert k s), (M.updateRow j (a • M j + ∑ k ∈ Insert.insert k s, c k • M k)).det = a • M.det
⊢ (M.updateRow j (a • M j + ∑ k ∈ s, c k • M k)).det = a • M.det

Tactic:
induction s using Finset.induction_on with
  | empty => rw [Finset.sum_empty, add_zero, smul_eq_mul, det_updateRow_smul, updateRow_eq_self]
  | insert k _ hk h_ind =>
      have h : k ≠ j := fun h ↦ (h ▸ hj) (Finset.mem_insert_self _ _)
      rw [Finset.sum_insert hk, add_comm ((c k) • M k), ← add_assoc, det_updateRow_add,
        det_updateRow_smul, det_updateRow_eq_zero h, mul_zero, add_zero, h_ind]
      exact fun h ↦ hj (Finset.mem_insert_of_mem h)

Premises used: add_assoc, Insert.insert, MulZeroClass.mul_zero, Matrix.updateRow_eq_self, Matrix.det_updateRow_smul, Finset.sum_empty, smul_eq_mul, add_zero, Matrix.det_updateRow_add
-- 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
A : Matrix n n R
j : n
c : n → R
⊢ (A.updateRow j (c j • A j + ∑ k ∈ erase univ j, c k • A k)).det = c j • A.det

Tactic:
det_updateRow_sum_aux A (Finset.univ.erase j) (Finset.univ.notMem_erase j) c (c j)

Premises used: Finset.univ, Matrix.det_updateRow_sum_aux, Finset.notMem_erase, Finset.erase
-- 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
A : Matrix n n R
j : n
c : n → R
h : ∑ k : n, c k • A k = c j • A j + ∑ k ∈ erase univ j, c k • A k
⊢ (A.updateRow j (∑ k : n, c k • A k)).det = c j • A.det

Tactic:
convert! det_updateRow_sum_aux A (Finset.univ.erase j) (Finset.univ.notMem_erase j) c (c j)

Premises used: Finset.univ, Matrix.det_updateRow_sum_aux, Finset.notMem_erase, Finset.erase
-- 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
A : Matrix n n R
j : n
c : n → R
h h₁ : c j • A j + ∑ x ∈ erase univ j, c x • A x = c j • A j + ∑ k ∈ erase univ j, c k • A k
⊢ ∑ k : n, c k • A k = c j • A j + ∑ k ∈ erase univ j, c k • A k

Tactic:
rw [← Finset.univ.add_sum_erase _ (Finset.mem_univ j)]

Premises used: Finset.mem_univ, Finset.univ, Finset.add_sum_erase
-- 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
A : Matrix n n R
j : n
c : n → R
rw : (Aᵀ.updateRow j fun (k : n) ↦ ∑ i : n, c i • A k i).det = c j • Aᵀ.det
⊢ (A.updateCol j fun (k : n) ↦ ∑ i : n, c i • A k i).det = c j • A.det

Tactic:
rw [← det_transpose, ← updateRow_transpose, ← det_transpose A]

Premises used: Matrix.det_transpose, Matrix.updateRow_transpose
-- 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
A : Matrix n n R
j : n
c : n → R
⊢ (Aᵀ.updateRow j (∑ k : n, c k • Aᵀ k)).det = c j • Aᵀ.det

Tactic:
det_updateRow_sum A.transpose j c

Premises used: Matrix.det_updateRow_sum, Matrix.transpose
-- 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
A : Matrix n n R
j : n
c : n → R
h : ∀ (x : n), Eq.{v + 1} (α := R) (∑ i : n, c i • A x i) ((∑ k : n, c k • Aᵀ k) x)
⊢ (Aᵀ.updateRow j fun (k : n) ↦ ∑ i : n, c i • A k i).det = c j • Aᵀ.det

Tactic:
convert! det_updateRow_sum A.transpose j c

Premises used: Matrix.det_updateRow_sum, Matrix.transpose
-- 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
A : Matrix n n R
j : n
c : n → R
x : n
⊢ Eq.{v + 1} (α := R) (∑ i : n, c i • A x i) ((∑ k : n, c k • Aᵀ k) x)

Tactic:
simp only [smul_eq_mul, Finset.sum_apply, Pi.smul_apply, transpose_apply]

Premises used: Finset.sum_apply, smul_eq_mul, Matrix.transpose_apply, Pi.smul_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
A B C : Matrix n n R
hC : C.det = 1
hA : A = B * C
rw : B.det * 1 = B.det
rw₁ rw₂ : B.det = B.det
⊢ B.det * C.det = B.det

Tactic:
rw [hC, mul_one]

Premises used: mul_one
-- 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
A B C : Matrix n n R
hC : C.det = 1
hA : A = C * B
rw : 1 * B.det = B.det
rw₁ rw₂ : B.det = B.det
⊢ C.det * B.det = B.det

Tactic:
rw [hC, one_mul]

Premises used: one_mul
-- 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
A : Matrix n n R
i j : n
hij : i ≠ j
⊢ (A.updateRow i (A i + A j)).det = A.det

Tactic:
simp [det_updateRow_add,
    det_zero_of_row_eq hij (updateRow_self.trans (updateRow_ne hij.symm).symm)]

Premises used: Matrix.det_zero_of_row_eq, Ne.symm, Matrix.updateRow_ne, Matrix.updateRow_self, Eq.symm, Matrix.det_updateRow_add, 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
A : Matrix n n R
i j : n
hij : i ≠ j
rw : (Aᵀ.updateRow i fun (k : n) ↦ A k i + A k j).det = Aᵀ.det
⊢ (A.updateCol i fun (k : n) ↦ A k i + A k j).det = A.det

Tactic:
rw [← det_transpose, ← updateRow_transpose, ← det_transpose A]

Premises used: Matrix.det_transpose, Matrix.updateRow_transpose
-- 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
A : Matrix n n R
i j : n
hij : i ≠ j
⊢ (Aᵀ.updateRow i fun (k : n) ↦ A k i + A k j).det = Aᵀ.det

Tactic:
det_updateRow_add_self Aᵀ hij

Premises used: Matrix.det_updateRow_add_self, Matrix.transpose
-- 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
A : Matrix n n R
i j : n
hij : i ≠ j
⊢ (Aᵀ.updateRow i fun (k : n) ↦ A k i + A k j).det = Aᵀ.det

Tactic:
exact det_updateRow_add_self Aᵀ hij

Premises used: Matrix.det_updateRow_add_self, Matrix.transpose
-- 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
A : Matrix n n R
i j : n
hij : i ≠ j
c : R
⊢ (A.updateRow i (A i + c • A j)).det = A.det

Tactic:
simp [det_updateRow_add, det_updateRow_smul,
    det_zero_of_row_eq hij (updateRow_self.trans (updateRow_ne hij.symm).symm)]

Premises used: Matrix.det_zero_of_row_eq, Ne.symm, Matrix.updateRow_ne, Matrix.det_updateRow_smul, Matrix.updateRow_self, Eq.symm, Matrix.det_updateRow_add, 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
A : Matrix n n R
i j : n
hij : i ≠ j
c : R
rw : (Aᵀ.updateRow i fun (k : n) ↦ A k i + c • A k j).det = Aᵀ.det
⊢ (A.updateCol i fun (k : n) ↦ A k i + c • A k j).det = A.det

Tactic:
rw [← det_transpose, ← updateRow_transpose, ← det_transpose A]

Premises used: Matrix.det_transpose, Matrix.updateRow_transpose