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

Tactic:
det_updateRow_add_smul_self Aᵀ hij c

Premises used: Matrix.det_updateRow_add_smul_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 fun (k : n) ↦ A k i + c • A k j).det = Aᵀ.det

Tactic:
exact det_updateRow_add_smul_self Aᵀ hij c

Premises used: Matrix.det_updateRow_add_smul_self, Matrix.transpose
-- 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 : IsDomain R
A : Matrix m m R
hA : ¬LinearIndependent R (M := m → R) fun (i : m) ↦ A i
⊢ A.det = 0

Tactic:
detRowAlternating.map_linearDependent A hA

Premises used: AlternatingMap.map_linearDependent, 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
inst_3 : IsDomain R
A : Matrix m m R
hA : A.det ≠ 0
contrapose : ∀ (hA : ¬LinearIndependent R (M := m → R) fun (i : m) ↦ A i), A.det = 0
⊢ LinearIndependent R (M := m → R) fun (i : m) ↦ A i

Tactic:
contrapose hA
-- 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 : IsDomain R
A : Matrix m m R
hA : ¬LinearIndependent R (M := m → R) fun (i : m) ↦ A i
⊢ A.det = 0

Tactic:
det_eq_zero_of_not_linearIndependent_rows hA

Premises used: Matrix.det_eq_zero_of_not_linearIndependent_rows
-- 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 : IsDomain R
A : Matrix m m R
hA : ¬LinearIndependent R (M := m → R) fun (i : m) ↦ A i
⊢ A.det = 0

Tactic:
exact det_eq_zero_of_not_linearIndependent_rows hA

Premises used: Matrix.det_eq_zero_of_not_linearIndependent_rows
-- 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 : IsDomain R
A : Matrix m m R
hA : A.det ≠ 0
⊢ det A.col ≠ 0

Tactic:
simpa [Matrix.col]

Premises used: Matrix.col
-- 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 : IsDomain R
A : Matrix m m R
hA : ¬LinearIndependent R (M := m → R) fun (i : m) ↦ Aᵀ i
contrapose! : ∀ (hA : A.det ≠ 0), LinearIndependent R (M := m → R) fun (i : m) ↦ Aᵀ i
⊢ A.det = 0

Tactic:
contrapose! hA
-- 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 : IsDomain R
A : Matrix m m R
hA : A.det ≠ 0
⊢ LinearIndependent R (M := m → R) fun (i : m) ↦ Aᵀ i

Tactic:
linearIndependent_cols_of_det_ne_zero hA

Premises used: Matrix.linearIndependent_cols_of_det_ne_zero, Matrix.col
-- 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 : IsDomain R
A : Matrix m m R
hA : A.det ≠ 0
⊢ LinearIndependent R (M := m → R) fun (i : m) ↦ Aᵀ i

Tactic:
exact linearIndependent_cols_of_det_ne_zero hA

Premises used: Matrix.linearIndependent_cols_of_det_ne_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
inst_3 : Nontrivial n
u v : n → R
obtain : ∀ (i j : n) (hij : i ≠ j), (vecMulVec u v).det = 0
⊢ (vecMulVec u v).det = 0

Tactic:
obtain ⟨i, j, hij⟩ := exists_pair_ne n

Premises used: exists_pair_ne
-- 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
inst_3 : Nontrivial n
u v : n → R
i j : n
hij : i ≠ j
uv' : Matrix n n R := ((vecMulVec u v).updateRow i v).updateRow j v
⊢ uv'.det = 0

Tactic:
detRowAlternating.map_eq_zero_of_eq _ ?_ hij

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
inst_3 : Nontrivial n
u v : n → R
i j : n
hij : i ≠ j
uv' : Matrix n n R := ((vecMulVec u v).updateRow i v).updateRow j v
refine : uv' i = uv' j
⊢ uv'.det = 0

Tactic:
refine detRowAlternating.map_eq_zero_of_eq _ ?_ hij

Premises used: Matrix.detRowAlternating, AlternatingMap.map_eq_zero_of_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
inst_3 : Nontrivial n
u v : n → R
i j : n
hij : i ≠ j
uv' : Matrix n n R := ((vecMulVec u v).updateRow i v).updateRow j v
⊢ uv' i = uv' j

Tactic:
simp [uv', hij]
-- 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
inst_3 : Nontrivial n
u v : n → R
i j : n
hij : i ≠ j
uv' : Matrix n n R := ((vecMulVec u v).updateRow i v).updateRow j v
⊢ uv'.det = 0

Tactic:
have huv' : uv'.det = 0 := by
    refine detRowAlternating.map_eq_zero_of_eq _ ?_ hij
    simp [uv', hij]
-- 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
inst_3 : Nontrivial n
u v : n → R
i j : n
hij : i ≠ j
uv' : Matrix n n R := ((vecMulVec u v).updateRow i v).updateRow j v
huv' : uv'.det = 0
unfold :
  vecMulVec u v =
    ((((vecMulVec u v).updateRow i v).updateRow j v).updateRow i
          (u i • ((vecMulVec u v).updateRow i v).updateRow j v i)).updateRow
      j
      (u j •
        (((vecMulVec u v).updateRow i v).updateRow j v).updateRow i
          (u i • ((vecMulVec u v).updateRow i v).updateRow j v i) j)
⊢ vecMulVec u v = (uv'.updateRow i (u i • uv' i)).updateRow j (u j • uv'.updateRow i (u i • uv' i) j)

Tactic:
unfold uv'
-- 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
inst_3 : Nontrivial n
u v : n → R
i j : n
hij : i ≠ j
uv' : Matrix n n R := ((vecMulVec u v).updateRow i v).updateRow j v
huv' : uv'.det = 0
rw :
  vecMulVec u v =
    ((((vecMulVec u v).updateRow i v).updateRow j v).updateRow j
          (u j •
            (((vecMulVec u v).updateRow i v).updateRow j v).updateRow i
              (u i • ((vecMulVec u v).updateRow i v).updateRow j v i) j)).updateRow
      i (u i • ((vecMulVec u v).updateRow i v).updateRow j v i)
rw₁ :
  vecMulVec u v =
    (((vecMulVec u v).updateRow i v).updateRow j
          (u j •
            (((vecMulVec u v).updateRow i v).updateRow j v).updateRow i
              (u i • ((vecMulVec u v).updateRow i v).updateRow j v i) j)).updateRow
      i (u i • ((vecMulVec u v).updateRow i v).updateRow j v i)
rw₂ :
  vecMulVec u v =
    (((vecMulVec u v).updateRow i v).updateRow j (u j • ((vecMulVec u v).updateRow i v).updateRow j v j)).updateRow i
      (u i • ((vecMulVec u v).updateRow i v).updateRow j v i)
rw₃ :
  vecMulVec u v =
    (((vecMulVec u v).updateRow i v).updateRow j (u j • ((vecMulVec u v).updateRow i v).updateRow j v j)).updateRow i
      (u i • (vecMulVec u v).updateRow i v i)
rw₄ :
  vecMulVec u v =
    (((vecMulVec u v).updateRow i v).updateRow j (u j • v)).updateRow i (u i • (vecMulVec u v).updateRow i v i)
rw₅ : vecMulVec u v = (((vecMulVec u v).updateRow i v).updateRow j (u j • v)).updateRow i (u i • v)
rw₆ : vecMulVec u v = (((vecMulVec u v).updateRow j (u j • v)).updateRow i v).updateRow i (u i • v)
rw₇ : vecMulVec u v = ((vecMulVec u v).updateRow j (u j • v)).updateRow i (u i • v)
rw₈ : vecMulVec u v = (vecMulVec (update (β := fun (a : n) ↦ R) u j (u j)) v).updateRow i (u i • v)
rw₉ : vecMulVec u v = (vecMulVec u v).updateRow i (u i • v)
rw₁₀ : vecMulVec u v = vecMulVec (update (β := fun (a : n) ↦ R) u i (u i)) v
rw₁₁ rw₁₂ : vecMulVec u v = vecMulVec u v
⊢ vecMulVec u v =
    ((((vecMulVec u v).updateRow i v).updateRow j v).updateRow i
          (u i • ((vecMulVec u v).updateRow i v).updateRow j v i)).updateRow
      j
      (u j •
        (((vecMulVec u v).updateRow i v).updateRow j v).updateRow i
          (u i • ((vecMulVec u v).updateRow i v).updateRow j v i) j)

Tactic:
rw [updateRow_comm _ hij, updateRow_idem, updateRow_ne hij.symm, updateRow_ne hij,
      updateRow_self, updateRow_self, updateRow_comm _ hij, updateRow_idem,
      ← update_vecMulVec u v j, update_eq_self, ← update_vecMulVec u v i, update_eq_self]

Premises used: Function.update_eq_self, Matrix.updateRow_idem, Ne.symm, Matrix.updateRow_ne, Matrix.updateRow_comm, Matrix.update_vecMulVec, Matrix.updateRow_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
inst_3 : Nontrivial n
u v : n → R
i j : n
hij : i ≠ j
uv' : Matrix n n R := ((vecMulVec u v).updateRow i v).updateRow j v
huv' : uv'.det = 0
⊢ vecMulVec u v = (uv'.updateRow i (u i • uv' i)).updateRow j (u j • uv'.updateRow i (u i • uv' i) j)

Tactic:
have : vecMulVec u v =
      (uv'.updateRow i (u i • uv' i)).updateRow j (u j • uv'.updateRow i (u i • uv' i) j) := by
    unfold uv'
    rw [updateRow_comm _ hij, updateRow_idem, updateRow_ne hij.symm, updateRow_ne hij,
      updateRow_self, updateRow_self, updateRow_comm _ hij, updateRow_idem,
      ← update_vecMulVec u v j, update_eq_self, ← update_vecMulVec u v i, update_eq_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
inst_3 : Nontrivial n
u v : n → R
i j : n
hij : i ≠ j
uv' : Matrix n n R := ((vecMulVec u v).updateRow i v).updateRow j v
huv' : uv'.det = 0
this : vecMulVec u v = (uv'.updateRow i (u i • uv' i)).updateRow j (u j • uv'.updateRow i (u i • uv' i) j)
rw : ((uv'.updateRow i (u i • uv' i)).updateRow j (u j • uv'.updateRow i (u i • uv' i) j)).det = 0
rw₁ : u j * ((uv'.updateRow i (u i • uv' i)).updateRow j (uv'.updateRow i (u i • uv' i) j)).det = 0
rw₂ : u j * (uv'.updateRow i (u i • uv' i)).det = 0
rw₃ : u j * (u i * (uv'.updateRow i (uv' i)).det) = 0
rw₄ : u j * (u i * uv'.det) = 0
rw₅ : u j * (u i * 0) = 0
rw₆ : u j * 0 = 0
rw₇ rw₈ : Eq.{v + 1} (α := R) 0 0
⊢ (vecMulVec u v).det = 0

Tactic:
rw [this, det_updateRow_smul, updateRow_eq_self, det_updateRow_smul, updateRow_eq_self, huv',
    mul_zero, mul_zero]

Premises used: MulZeroClass.mul_zero, Matrix.updateRow_eq_self, 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
A B : Matrix n n R
c : n → R
hs : ∀ i ∉ ∅, c i = 0
k : n
A_eq : ∀ (i j : n), A i j = B i j + c i * B k j
⊢ ∀ (i : n), c i = 0

Tactic:
grind
-- 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 : Matrix n n R
c : n → R
hs : ∀ i ∉ ∅, c i = 0
k : n
A_eq : ∀ (i j : n), A i j = B i j + c i * B k j
⊢ ∀ (i : n), c i = 0

Tactic:
have : ∀ i, c i = 0 := by grind
-- 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 : Matrix n n R
c : n → R
hs : ∀ i ∉ ∅, c i = 0
k : n
A_eq : ∀ (i j : n), A i j = B i j + c i * B k j
this : ∀ (i : n), c i = 0
empty : A = B
⊢ A.det = B.det

Tactic:
congr
-- 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 : Matrix n n R
c : n → R
hs : ∀ i ∉ ∅, c i = 0
k : n
A_eq : ∀ (i j : n), A i j = B i j + c i * B k j
this : ∀ (i : n), c i = 0
empty : ∀ (i j : n), A i j = B i j
⊢ A = B

Tactic:
ext i j
-- 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 : Matrix n n R
c : n → R
hs : ∀ i ∉ ∅, c i = 0
k : n
A_eq : ∀ (i j : n), A i j = B i j + c i * B k j
this : ∀ (i : n), c i = 0
i j : n
empty : B i j + c i * B k j = B i j
empty₁ : B i j + 0 * B k j = B i j
empty₂ : B i j + 0 = B i j
empty₃ empty₄ : B i j = B i j
⊢ A i j = B i j

Tactic:
rw [A_eq, this, zero_mul, add_zero]

Premises used: MulZeroClass.zero_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
A : Matrix n n R
i : n
s : Finset n
_hi : i ∉ s
ih :
  ∀ {B : Matrix n n R} (c : n → R),
    (∀ i ∉ s, c i = 0) → ∀ k ∉ s, (∀ (i j : n), A i j = B i j + c i * B k j) → A.det = B.det
B : Matrix n n R
c : n → R
hs : ∀ i_1 ∉ insert i s, c i_1 = 0
k : n
hk : k ∉ insert i s
A_eq : ∀ (i j : n), A i j = B i j + c i * B k j
⊢ A i = B i + c i • B k

Tactic:
have hAi : A i = B i + c i • B k := funext (A_eq i)
-- 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
s : Finset n
_hi : i ∉ s
ih :
  ∀ {B : Matrix n n R} (c : n → R),
    (∀ i ∉ s, c i = 0) → ∀ k ∉ s, (∀ (i j : n), A i j = B i j + c i * B k j) → A.det = B.det
B : Matrix n n R
c : n → R
hs : ∀ i_1 ∉ Insert.insert i s, c i_1 = 0
k : n
hk : k ∉ Insert.insert i s
A_eq : ∀ (i j : n), A i j = B i j + c i * B k j
hAi : A i = B i + c i • B k
insert : i ≠ k
insert₁ : ∀ i_1 ∉ s, update (β := fun (a : n) ↦ R) c i 0 i_1 = 0
insert₂ : n
insert₃ : k ∉ s
insert₄ :
  ∀ (i_1 j : n), A i_1 j = B.updateRow i (A i) i_1 j + update (β := fun (a : n) ↦ R) c i 0 i_1 * B.updateRow i (A i) k j
⊢ A.det = B.det

Tactic:
rw [@ih (updateRow B i (A i)) (Function.update c i 0), hAi, det_updateRow_add_smul_self]

Premises used: Function.update, Matrix.det_updateRow_add_smul_self, OfNat.ofNat
-- 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
s : Finset n
_hi : i ∉ s
ih :
  ∀ {B : Matrix n n R} (c : n → R),
    (∀ i ∉ s, c i = 0) → ∀ k ∉ s, (∀ (i j : n), A i j = B i j + c i * B k j) → A.det = B.det
B : Matrix n n R
c : n → R
hs : ∀ i_1 ∉ insert i s, c i_1 = 0
k : n
hk : k ∉ insert i s
A_eq : ∀ (i j : n), A i j = B i j + c i * B k j
hAi : A i = B i + c i • B k
⊢ i ≠ k

Tactic:
mt (fun h => show k ∈ insert i s from h ▸ Finset.mem_insert_self _ _) hk

Premises used: Finset.mem_insert_self, mt, Eq.rec
-- 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
s : Finset n
_hi : i ∉ s
ih :
  ∀ {B : Matrix n n R} (c : n → R),
    (∀ i ∉ s, c i = 0) → ∀ k ∉ s, (∀ (i j : n), A i j = B i j + c i * B k j) → A.det = B.det
B : Matrix n n R
c : n → R
hs : ∀ i_1 ∉ insert i s, c i_1 = 0
k : n
hk : k ∉ insert i s
A_eq : ∀ (i j : n), A i j = B i j + c i * B k j
hAi : A i = B i + c i • B k
⊢ i ≠ k

Tactic:
exact mt (fun h => show k ∈ insert i s from h ▸ Finset.mem_insert_self _ _) hk
-- 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
s : Finset n
_hi : i ∉ s
ih :
  ∀ {B : Matrix n n R} (c : n → R),
    (∀ i ∉ s, c i = 0) → ∀ k ∉ s, (∀ (i j : n), A i j = B i j + c i * B k j) → A.det = B.det
B : Matrix n n R
c : n → R
hs : ∀ i_1 ∉ Insert.insert i s, c i_1 = 0
k : n
hk : k ∉ Insert.insert i s
A_eq : ∀ (i j : n), A i j = B i j + c i * B k j
hAi : A i = B i + c i • B k
i' : n
hi' : i' ∉ s
insert : (if i' = i then 0 else c i') = 0
⊢ update (β := fun (a : n) ↦ R) c i 0 i' = 0

Tactic:
rw [Function.update_apply]

Premises used: Function.update_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 : Matrix n n R
i : n
s : Finset n
_hi : i ∉ s
ih :
  ∀ {B : Matrix n n R} (c : n → R),
    (∀ i ∉ s, c i = 0) → ∀ k ∉ s, (∀ (i j : n), A i j = B i j + c i * B k j) → A.det = B.det
B : Matrix n n R
c : n → R
hs : ∀ i_1 ∉ insert i s, c i_1 = 0
k : n
hk : k ∉ insert i s
A_eq : ∀ (i j : n), A i j = B i j + c i * B k j
hAi : A i = B i + c i • B k
i' : n
hi' : i' ∉ s
pos : ∀ (hi'i : i' = i), Eq.{v + 1} (α := R) 0 0
neg : ∀ (hi'i : ¬i' = i), c i' = 0
⊢ (if i' = i then 0 else c i') = 0

Tactic:
split_ifs with hi'i
-- 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
s : Finset n
_hi : i ∉ s
ih :
  ∀ {B : Matrix n n R} (c : n → R),
    (∀ i ∉ s, c i = 0) → ∀ k ∉ s, (∀ (i j : n), A i j = B i j + c i * B k j) → A.det = B.det
B : Matrix n n R
c : n → R
hs : ∀ i_1 ∉ insert i s, c i_1 = 0
k : n
hk : k ∉ insert i s
A_eq : ∀ (i j : n), A i j = B i j + c i * B k j
hAi : A i = B i + c i • B k
i' : n
hi' : i' ∉ s
hi'i : i' = i
⊢ Eq.{v + 1} (α := R) 0 0

Tactic:
rfl
-- 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
s : Finset n
_hi : i ∉ s
ih :
  ∀ {B : Matrix n n R} (c : n → R),
    (∀ i ∉ s, c i = 0) → ∀ k ∉ s, (∀ (i j : n), A i j = B i j + c i * B k j) → A.det = B.det
B : Matrix n n R
c : n → R
hs : ∀ i_1 ∉ insert i s, c i_1 = 0
k : n
hk : k ∉ insert i s
A_eq : ∀ (i j : n), A i j = B i j + c i * B k j
hAi : A i = B i + c i • B k
i' : n
hi' : i' ∉ s
hi'i : ¬i' = i
⊢ c i' = 0

Tactic:
hs i' fun h => hi' ((Finset.mem_insert.mp h).resolve_left hi'i)

Premises used: Or.resolve_left, Finset.mem_insert, 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
A : Matrix n n R
i : n
s : Finset n
_hi : i ∉ s
ih :
  ∀ {B : Matrix n n R} (c : n → R),
    (∀ i ∉ s, c i = 0) → ∀ k ∉ s, (∀ (i j : n), A i j = B i j + c i * B k j) → A.det = B.det
B : Matrix n n R
c : n → R
hs : ∀ i_1 ∉ insert i s, c i_1 = 0
k : n
hk : k ∉ insert i s
A_eq : ∀ (i j : n), A i j = B i j + c i * B k j
hAi : A i = B i + c i • B k
i' : n
hi' : i' ∉ s
hi'i : ¬i' = i
⊢ c i' = 0

Tactic:
exact hs i' fun h => hi' ((Finset.mem_insert.mp h).resolve_left hi'i)

Premises used: Or.resolve_left, Finset.mem_insert, 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
A : Matrix n n R
i : n
s : Finset n
_hi : i ∉ s
ih :
  ∀ {B : Matrix n n R} (c : n → R),
    (∀ i ∉ s, c i = 0) → ∀ k ∉ s, (∀ (i j : n), A i j = B i j + c i * B k j) → A.det = B.det
B : Matrix n n R
c : n → R
hs : ∀ i_1 ∉ insert i s, c i_1 = 0
k : n
hk : k ∉ insert i s
A_eq : ∀ (i j : n), A i j = B i j + c i * B k j
hAi : A i = B i + c i • B k
⊢ n

Tactic:
exact k
-- 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
s : Finset n
_hi : i ∉ s
ih :
  ∀ {B : Matrix n n R} (c : n → R),
    (∀ i ∉ s, c i = 0) → ∀ k ∉ s, (∀ (i j : n), A i j = B i j + c i * B k j) → A.det = B.det
B : Matrix n n R
c : n → R
hs : ∀ i_1 ∉ insert i s, c i_1 = 0
k : n
hk : k ∉ insert i s
A_eq : ∀ (i j : n), A i j = B i j + c i * B k j
hAi : A i = B i + c i • B k
⊢ k ∉ s

Tactic:
fun h => hk (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
A : Matrix n n R
i : n
s : Finset n
_hi : i ∉ s
ih :
  ∀ {B : Matrix n n R} (c : n → R),
    (∀ i ∉ s, c i = 0) → ∀ k ∉ s, (∀ (i j : n), A i j = B i j + c i * B k j) → A.det = B.det
B : Matrix n n R
c : n → R
hs : ∀ i_1 ∉ insert i s, c i_1 = 0
k : n
hk : k ∉ insert i s
A_eq : ∀ (i j : n), A i j = B i j + c i * B k j
hAi : A i = B i + c i • B k
⊢ k ∉ s

Tactic:
exact fun h => hk (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
A : Matrix n n R
i : n
s : Finset n
_hi : i ∉ s
ih :
  ∀ {B : Matrix n n R} (c : n → R),
    (∀ i ∉ s, c i = 0) → ∀ k ∉ s, (∀ (i j : n), A i j = B i j + c i * B k j) → A.det = B.det
B : Matrix n n R
c : n → R
hs : ∀ i_1 ∉ Insert.insert i s, c i_1 = 0
k : n
hk : k ∉ Insert.insert i s
A_eq : ∀ (i j : n), A i j = B i j + c i * B k j
hAi : A i = B i + c i • B k
i' j' : n
insert : A i' j' = (if i' = i then A i j' else B i' j') + (if i' = i then 0 else c i') * B.updateRow i (A i) k j'
⊢ A i' j' = B.updateRow i (A i) i' j' + update (β := fun (a : n) ↦ R) c i 0 i' * B.updateRow i (A i) k j'

Tactic:
rw [updateRow_apply, Function.update_apply]

Premises used: Function.update_apply, Matrix.updateRow_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 : Matrix n n R
i : n
s : Finset n
_hi : i ∉ s
ih :
  ∀ {B : Matrix n n R} (c : n → R),
    (∀ i ∉ s, c i = 0) → ∀ k ∉ s, (∀ (i j : n), A i j = B i j + c i * B k j) → A.det = B.det
B : Matrix n n R
c : n → R
hs : ∀ i_1 ∉ insert i s, c i_1 = 0
k : n
hk : k ∉ insert i s
A_eq : ∀ (i j : n), A i j = B i j + c i * B k j
hAi : A i = B i + c i • B k
i' j' : n
pos : ∀ (hi'i : i' = i), A i' j' = A i j' + 0 * B.updateRow i (A i) k j'
neg : ∀ (hi'i : ¬i' = i), A i' j' = B i' j' + c i' * B.updateRow i (A i) k j'
⊢ A i' j' = (if i' = i then A i j' else B i' j') + (if i' = i then 0 else c i') * B.updateRow i (A i) k j'

Tactic:
split_ifs with hi'i
-- 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
s : Finset n
_hi : i ∉ s
ih :
  ∀ {B : Matrix n n R} (c : n → R),
    (∀ i ∉ s, c i = 0) → ∀ k ∉ s, (∀ (i j : n), A i j = B i j + c i * B k j) → A.det = B.det
B : Matrix n n R
c : n → R
hs : ∀ i_1 ∉ insert i s, c i_1 = 0
k : n
hk : k ∉ insert i s
A_eq : ∀ (i j : n), A i j = B i j + c i * B k j
hAi : A i = B i + c i • B k
i' j' : n
hi'i : i' = i
⊢ A i' j' = A i j' + 0 * B.updateRow i (A i) k j'

Tactic:
simp [hi'i]
-- 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
s : Finset n
_hi : i ∉ s
ih :
  ∀ {B : Matrix n n R} (c : n → R),
    (∀ i ∉ s, c i = 0) → ∀ k ∉ s, (∀ (i j : n), A i j = B i j + c i * B k j) → A.det = B.det
B : Matrix n n R
c : n → R
hs : ∀ i_1 ∉ insert i s, c i_1 = 0
k : n
hk : k ∉ insert i s
A_eq : ∀ (i j : n), A i j = B i j + c i * B k j
hAi : A i = B i + c i • B k
i' j' : n
hi'i : ¬i' = i
neg : B i' j' + c i' * B k j' = B i' j' + c i' * B.updateRow i (A i) k j'
neg₁ neg₂ : B i' j' + c i' * B k j' = B i' j' + c i' * B k j'
⊢ A i' j' = B i' j' + c i' * B.updateRow i (A i) k j'

Tactic:
rw [A_eq, updateRow_ne fun h : k = i => hk <| h ▸ Finset.mem_insert_self k s]

Premises used: Finset.mem_insert_self, Eq.rec, Matrix.updateRow_ne