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 B : Matrix n n R
s : Finset n
empty :
  ∀ {B : Matrix n n R} (c : n → R),
    (∀ i ∉ ∅, c i = 0) → ∀ k ∉ ∅, (∀ (i j : n), A i j = B i j + c i * B k j) → A.det = B.det
insert :
  ∀ (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),
    (∀ i_1 ∉ Insert.insert i s, c i_1 = 0) →
      ∀ k ∉ Insert.insert i s, (∀ (i j : n), A i j = B i j + c i * B k j) → A.det = B.det
⊢ ∀ (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

Tactic:
induction s using Finset.induction_on generalizing B with
  | empty =>
    rintro c hs k - A_eq
    have : ∀ i, c i = 0 := by grind
    congr
    ext i j
    rw [A_eq, this, zero_mul, add_zero]
  | insert i s _hi ih =>
    intro c hs k hk A_eq
    have hAi : A i = B i + c i • B k := funext (A_eq i)
    rw [@ih (updateRow B i (A i)) (Function.update c i 0), hAi, det_updateRow_add_smul_self]
    · exact mt (fun h => show k ∈ insert i s from h ▸ Finset.mem_insert_self _ _) hk
    · intro i' hi'
      rw [Function.update_apply]
      split_ifs with hi'i
      · rfl
      · exact hs i' fun h => hi' ((Finset.mem_insert.mp h).resolve_left hi'i)
    · exact k
    · exact fun h => hk (Finset.mem_insert_of_mem h)
    · intro i' j'
      rw [updateRow_apply, Function.update_apply]
      split_ifs with hi'i
      · simp [hi'i]
      rw [A_eq, updateRow_ne fun h : k = i => hk <| h ▸ Finset.mem_insert_self k s]

Premises used: Matrix.det_updateRow_add_smul_self, MulZeroClass.zero_mul, Insert.insert, Function.update_apply, add_zero, 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 B : Matrix n n R
c : n → R
k : n
hk : c k = 0
A_eq : ∀ (i j : n), A i j = B i j + c i * B k j
⊢ A.det = B.det

Tactic:
det_eq_of_forall_row_eq_smul_add_const_aux c
    (fun i =>
      not_imp_comm.mp fun hi =>
        Finset.mem_erase.mpr
          ⟨mt (fun h : i = k => show c i = 0 from h.symm ▸ hk) hi, Finset.mem_univ i⟩)
    k (Finset.notMem_erase k Finset.univ) A_eq

Premises used: Iff.mpr, Finset.mem_univ, Finset.univ, not_imp_comm, mt, Eq.rec, Matrix.det_eq_of_forall_row_eq_smul_add_const_aux, Finset.mem_erase, And.intro, Iff.mp, Finset.notMem_erase, Eq.symm
-- Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic
Goal:
R : Type v
inst : CommRing R
n : ℕ
k : Fin (n + 1)
⊢ ∀ (c : Fin n → R) (_hc : ∀ (i : Fin n), k < i.succ → c i = 0) {M N : Matrix (Fin n.succ) (Fin n.succ) R}
    (_h0 : ∀ (j : Fin n.succ), M 0 j = N 0 j)
    (_hsucc : ∀ (i : Fin n) (j : Fin n.succ), M i.succ j = N i.succ j + c i * M i.castSucc j), M.det = N.det

Tactic:
Fin.induction ?_ (fun k ih => ?_) k

Premises used: Fin.induction
-- Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic
Goal:
R : Type v
inst : CommRing R
n : ℕ
k : Fin (n + 1)
refine_1 :
  ∀ (c : Fin n → R) (_hc : ∀ (i : Fin n), 0 < i.succ → c i = 0) {M N : Matrix (Fin n.succ) (Fin n.succ) R}
    (_h0 : ∀ (j : Fin n.succ), M 0 j = N 0 j)
    (_hsucc : ∀ (i : Fin n) (j : Fin n.succ), M i.succ j = N i.succ j + c i * M i.castSucc j), M.det = N.det
refine_2 :
  ∀ (k : Fin n)
    (ih :
      ∀ (c : Fin n → R) (_hc : ∀ (i : Fin n), k.castSucc < i.succ → c i = 0) {M N : Matrix (Fin n.succ) (Fin n.succ) R}
        (_h0 : ∀ (j : Fin n.succ), M 0 j = N 0 j)
        (_hsucc : ∀ (i : Fin n) (j : Fin n.succ), M i.succ j = N i.succ j + c i * M i.castSucc j), M.det = N.det)
    (c : Fin n → R) (_hc : ∀ (i : Fin n), k.succ < i.succ → c i = 0) {M N : Matrix (Fin n.succ) (Fin n.succ) R}
    (_h0 : ∀ (j : Fin n.succ), M 0 j = N 0 j)
    (_hsucc : ∀ (i : Fin n) (j : Fin n.succ), M i.succ j = N i.succ j + c i * M i.castSucc j), M.det = N.det
⊢ ∀ (c : Fin n → R) (_hc : ∀ (i : Fin n), k < i.succ → c i = 0) {M N : Matrix (Fin n.succ) (Fin n.succ) R}
    (_h0 : ∀ (j : Fin n.succ), M 0 j = N 0 j)
    (_hsucc : ∀ (i : Fin n) (j : Fin n.succ), M i.succ j = N i.succ j + c i * M i.castSucc j), M.det = N.det

Tactic:
refine Fin.induction ?_ (fun k ih => ?_) k
-- Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic
Goal:
R : Type v
inst : CommRing R
n : ℕ
k : Fin (n + 1)
c : Fin n → R
hc : ∀ (i : Fin n), 0 < i.succ → c i = 0
M N : Matrix (Fin n.succ) (Fin n.succ) R
h0 : ∀ (j : Fin n.succ), M 0 j = N 0 j
hsucc : ∀ (i : Fin n) (j : Fin n.succ), M i.succ j = N i.succ j + c i * M i.castSucc j
refine_1 : M = N
⊢ M.det = N.det

Tactic:
congr
-- Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic
Goal:
R : Type v
inst : CommRing R
n : ℕ
k : Fin (n + 1)
c : Fin n → R
hc : ∀ (i : Fin n), 0 < i.succ → c i = 0
M N : Matrix (Fin n.succ) (Fin n.succ) R
h0 : ∀ (j : Fin n.succ), M 0 j = N 0 j
hsucc : ∀ (i : Fin n) (j : Fin n.succ), M i.succ j = N i.succ j + c i * M i.castSucc j
refine_1 : ∀ (i j : Fin n.succ), M i j = N i j
⊢ M = N

Tactic:
ext i j
-- Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic
Goal:
R : Type v
inst : CommRing R
n : ℕ
k : Fin (n + 1)
c : Fin n → R
hc : ∀ (i : Fin n), 0 < i.succ → c i = 0
M N : Matrix (Fin n.succ) (Fin n.succ) R
h0 : ∀ (j : Fin n.succ), M 0 j = N 0 j
hsucc : ∀ (i : Fin n) (j : Fin n.succ), M i.succ j = N i.succ j + c i * M i.castSucc j
i j : Fin n.succ
⊢ M i j = N i j

Tactic:
Fin.cases (h0 j) (fun i => ?_) i

Premises used: Fin.cases
-- Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic
Goal:
R : Type v
inst : CommRing R
n : ℕ
k : Fin (n + 1)
c : Fin n → R
hc : ∀ (i : Fin n), 0 < i.succ → c i = 0
M N : Matrix (Fin n.succ) (Fin n.succ) R
h0 : ∀ (j : Fin n.succ), M 0 j = N 0 j
hsucc : ∀ (i : Fin n) (j : Fin n.succ), M i.succ j = N i.succ j + c i * M i.castSucc j
i j : Fin n.succ
refine_1 : ∀ (i : Fin n), M i.succ j = N i.succ j
⊢ M i j = N i j

Tactic:
refine Fin.cases (h0 j) (fun i => ?_) i
-- Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic
Goal:
R : Type v
inst : CommRing R
n : ℕ
k : Fin (n + 1)
c : Fin n → R
hc : ∀ (i : Fin n), 0 < i.succ → c i = 0
M N : Matrix (Fin n.succ) (Fin n.succ) R
h0 : ∀ (j : Fin n.succ), M 0 j = N 0 j
hsucc : ∀ (i : Fin n) (j : Fin n.succ), M i.succ j = N i.succ j + c i * M i.castSucc j
i_1 j : Fin n.succ
i : Fin n
refine_1 : N i.succ j + c i * M i.castSucc j = N i.succ j
refine_1₁ : N i.succ j + 0 * M i.castSucc j = N i.succ j
refine_1₂ : N i.succ j + 0 = N i.succ j
refine_1₃ refine_1₄ : N i.succ j = N i.succ j
⊢ M i.succ j = N i.succ j

Tactic:
rw [hsucc, hc i (Fin.succ_pos _), zero_mul, add_zero]

Premises used: MulZeroClass.zero_mul, Fin.succ_pos, add_zero
-- Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic
Goal:
R : Type v
inst : CommRing R
n : ℕ
k_1 : Fin (n + 1)
k : Fin n
ih :
  ∀ (c : Fin n → R) (_hc : ∀ (i : Fin n), k.castSucc < i.succ → c i = 0) {M N : Matrix (Fin n.succ) (Fin n.succ) R}
    (_h0 : ∀ (j : Fin n.succ), M 0 j = N 0 j)
    (_hsucc : ∀ (i : Fin n) (j : Fin n.succ), M i.succ j = N i.succ j + c i * M i.castSucc j), M.det = N.det
c : Fin n → R
hc : ∀ (i : Fin n), k.succ < i.succ → c i = 0
M N : Matrix (Fin n.succ) (Fin n.succ) R
h0 : ∀ (j : Fin n.succ), M 0 j = N 0 j
hsucc : ∀ (i : Fin n) (j : Fin n.succ), M i.succ j = N i.succ j + c i * M i.castSucc j
⊢ let M' := M.updateRow k.succ (N k.succ);
  M' = M.updateRow k.succ (N k.succ)

Tactic:
set M' := updateRow M k.succ (N k.succ) with hM'

Premises used: Fin.succ, Matrix.updateRow
-- Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic
Goal:
R : Type v
inst : CommRing R
n : ℕ
k_1 : Fin (n + 1)
k : Fin n
ih :
  ∀ (c : Fin n → R) (_hc : ∀ (i : Fin n), k.castSucc < i.succ → c i = 0) {M N : Matrix (Fin n.succ) (Fin n.succ) R}
    (_h0 : ∀ (j : Fin n.succ), M 0 j = N 0 j)
    (_hsucc : ∀ (i : Fin n) (j : Fin n.succ), M i.succ j = N i.succ j + c i * M i.castSucc j), M.det = N.det
c : Fin n → R
hc : ∀ (i : Fin n), k.succ < i.succ → c i = 0
M N : Matrix (Fin n.succ) (Fin n.succ) R
h0 : ∀ (j : Fin n.succ), M 0 j = N 0 j
hsucc : ∀ (i : Fin n) (j : Fin n.succ), M i.succ j = N i.succ j + c i * M i.castSucc j
M' : Matrix (Fin n.succ) (Fin n.succ) R := M.updateRow k.succ (N k.succ)
hM' : M' = M.updateRow k.succ (N k.succ)
a : ∀ (i j : Fin n.succ), M i j = M'.updateRow k.succ (M' k.succ + c k • M k.castSucc) i j
⊢ M = M'.updateRow k.succ (M' k.succ + c k • M k.castSucc)

Tactic:
ext i j
-- Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic
Goal:
R : Type v
inst : CommRing R
n : ℕ
k_1 : Fin (n + 1)
k : Fin n
ih :
  ∀ (c : Fin n → R) (_hc : ∀ (i : Fin n), k.castSucc < i.succ → c i = 0) {M N : Matrix (Fin n.succ) (Fin n.succ) R}
    (_h0 : ∀ (j : Fin n.succ), M 0 j = N 0 j)
    (_hsucc : ∀ (i : Fin n) (j : Fin n.succ), M i.succ j = N i.succ j + c i * M i.castSucc j), M.det = N.det
c : Fin n → R
hc : ∀ (i : Fin n), k.succ < i.succ → c i = 0
M N : Matrix (Fin n.succ) (Fin n.succ) R
h0 : ∀ (j : Fin n.succ), M 0 j = N 0 j
hsucc : ∀ (i : Fin n) (j : Fin n.succ), M i.succ j = N i.succ j + c i * M i.castSucc j
M' : Matrix (Fin n.succ) (Fin n.succ) R := M.updateRow k.succ (N k.succ)
hM' : M' = M.updateRow k.succ (N k.succ)
i j : Fin n.succ
pos : ∀ (hi : i = k.succ), M i j = M'.updateRow k.succ (M' k.succ + c k • M k.castSucc) i j
neg : ∀ (hi : ¬i = k.succ), M i j = M'.updateRow k.succ (M' k.succ + c k • M k.castSucc) i j
⊢ M i j = M'.updateRow k.succ (M' k.succ + c k • M k.castSucc) i j

Tactic:
by_cases hi : i = k.succ

Premises used: Fin.succ
-- Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic
Goal:
R : Type v
inst : CommRing R
n : ℕ
k_1 : Fin (n + 1)
k : Fin n
ih :
  ∀ (c : Fin n → R) (_hc : ∀ (i : Fin n), k.castSucc < i.succ → c i = 0) {M N : Matrix (Fin n.succ) (Fin n.succ) R}
    (_h0 : ∀ (j : Fin n.succ), M 0 j = N 0 j)
    (_hsucc : ∀ (i : Fin n) (j : Fin n.succ), M i.succ j = N i.succ j + c i * M i.castSucc j), M.det = N.det
c : Fin n → R
hc : ∀ (i : Fin n), k.succ < i.succ → c i = 0
M N : Matrix (Fin n.succ) (Fin n.succ) R
h0 : ∀ (j : Fin n.succ), M 0 j = N 0 j
hsucc : ∀ (i : Fin n) (j : Fin n.succ), M i.succ j = N i.succ j + c i * M i.castSucc j
M' : Matrix (Fin n.succ) (Fin n.succ) R := M.updateRow k.succ (N k.succ)
hM' : M' = M.updateRow k.succ (N k.succ)
i j : Fin n.succ
hi : i = k.succ
⊢ M i j = M'.updateRow k.succ (M' k.succ + c k • M k.castSucc) i j

Tactic:
simp [hi, hM', hsucc, updateRow_self]

Premises used: Matrix.updateRow_self
-- Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic
Goal:
R : Type v
inst : CommRing R
n : ℕ
k_1 : Fin (n + 1)
k : Fin n
ih :
  ∀ (c : Fin n → R) (_hc : ∀ (i : Fin n), k.castSucc < i.succ → c i = 0) {M N : Matrix (Fin n.succ) (Fin n.succ) R}
    (_h0 : ∀ (j : Fin n.succ), M 0 j = N 0 j)
    (_hsucc : ∀ (i : Fin n) (j : Fin n.succ), M i.succ j = N i.succ j + c i * M i.castSucc j), M.det = N.det
c : Fin n → R
hc : ∀ (i : Fin n), k.succ < i.succ → c i = 0
M N : Matrix (Fin n.succ) (Fin n.succ) R
h0 : ∀ (j : Fin n.succ), M 0 j = N 0 j
hsucc : ∀ (i : Fin n) (j : Fin n.succ), M i.succ j = N i.succ j + c i * M i.castSucc j
M' : Matrix (Fin n.succ) (Fin n.succ) R := M.updateRow k.succ (N k.succ)
hM' : M' = M.updateRow k.succ (N k.succ)
i j : Fin n.succ
hi : ¬i = k.succ
neg : M i j = M' i j
neg₁ : M i j = M.updateRow k.succ (N k.succ) i j
neg₂ neg₃ : M i j = M i j
⊢ M i j = M'.updateRow k.succ (M' k.succ + c k • M k.castSucc) i j

Tactic:
rw [updateRow_ne hi, hM', updateRow_ne hi]

Premises used: Matrix.updateRow_ne
-- Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic
Goal:
R : Type v
inst : CommRing R
n : ℕ
k_1 : Fin (n + 1)
k : Fin n
ih :
  ∀ (c : Fin n → R) (_hc : ∀ (i : Fin n), k.castSucc < i.succ → c i = 0) {M N : Matrix (Fin n.succ) (Fin n.succ) R}
    (_h0 : ∀ (j : Fin n.succ), M 0 j = N 0 j)
    (_hsucc : ∀ (i : Fin n) (j : Fin n.succ), M i.succ j = N i.succ j + c i * M i.castSucc j), M.det = N.det
c : Fin n → R
hc : ∀ (i : Fin n), k.succ < i.succ → c i = 0
M N : Matrix (Fin n.succ) (Fin n.succ) R
h0 : ∀ (j : Fin n.succ), M 0 j = N 0 j
hsucc : ∀ (i : Fin n) (j : Fin n.succ), M i.succ j = N i.succ j + c i * M i.castSucc j
M' : Matrix (Fin n.succ) (Fin n.succ) R := M.updateRow k.succ (N k.succ)
hM' : M' = M.updateRow k.succ (N k.succ)
⊢ M = M'.updateRow k.succ (M' k.succ + c k • M k.castSucc)

Tactic:
have hM : M = updateRow M' k.succ (M' k.succ + c k • M (Fin.castSucc k)) := by
    ext i j
    by_cases hi : i = k.succ
    · simp [hi, hM', hsucc, updateRow_self]
    rw [updateRow_ne hi, hM', updateRow_ne hi]
-- Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic
Goal:
R : Type v
inst : CommRing R
n : ℕ
k_1 : Fin (n + 1)
k : Fin n
ih :
  ∀ (c : Fin n → R) (_hc : ∀ (i : Fin n), k.castSucc < i.succ → c i = 0) {M N : Matrix (Fin n.succ) (Fin n.succ) R}
    (_h0 : ∀ (j : Fin n.succ), M 0 j = N 0 j)
    (_hsucc : ∀ (i : Fin n) (j : Fin n.succ), M i.succ j = N i.succ j + c i * M i.castSucc j), M.det = N.det
c : Fin n → R
hc : ∀ (i : Fin n), k.succ < i.succ → c i = 0
M N : Matrix (Fin n.succ) (Fin n.succ) R
h0 : ∀ (j : Fin n.succ), M 0 j = N 0 j
hsucc : ∀ (i : Fin n) (j : Fin n.succ), M i.succ j = N i.succ j + c i * M i.castSucc j
M' : Matrix (Fin n.succ) (Fin n.succ) R := M.updateRow k.succ (N k.succ)
hM' : M' = M.updateRow k.succ (N k.succ)
hM : M = M'.updateRow k.succ (M' k.succ + c k • M k.castSucc)
⊢ k.castSucc ≠ k.succ

Tactic:
have k_ne_succ : (Fin.castSucc k) ≠ k.succ := Fin.castSucc_lt_succ.ne
-- Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic
Goal:
R : Type v
inst : CommRing R
n : ℕ
k_1 : Fin (n + 1)
k : Fin n
ih :
  ∀ (c : Fin n → R) (_hc : ∀ (i : Fin n), k.castSucc < i.succ → c i = 0) {M N : Matrix (Fin n.succ) (Fin n.succ) R}
    (_h0 : ∀ (j : Fin n.succ), M 0 j = N 0 j)
    (_hsucc : ∀ (i : Fin n) (j : Fin n.succ), M i.succ j = N i.succ j + c i * M i.castSucc j), M.det = N.det
c : Fin n → R
hc : ∀ (i : Fin n), k.succ < i.succ → c i = 0
M N : Matrix (Fin n.succ) (Fin n.succ) R
h0 : ∀ (j : Fin n.succ), M 0 j = N 0 j
hsucc : ∀ (i : Fin n) (j : Fin n.succ), M i.succ j = N i.succ j + c i * M i.castSucc j
M' : Matrix (Fin n.succ) (Fin n.succ) R := M.updateRow k.succ (N k.succ)
hM' : M' = M.updateRow k.succ (N k.succ)
hM : M = M'.updateRow k.succ (M' k.succ + c k • M k.castSucc)
k_ne_succ : k.castSucc ≠ k.succ
⊢ M k.castSucc = M' k.castSucc

Tactic:
have M_k : M (Fin.castSucc k) = M' (Fin.castSucc k) := (updateRow_ne k_ne_succ).symm
-- Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic
Goal:
R : Type v
inst : CommRing R
n : ℕ
k_1 : Fin (n + 1)
k : Fin n
ih :
  ∀ (c : Fin n → R) (_hc : ∀ (i : Fin n), k.castSucc < i.succ → c i = 0) {M N : Matrix (Fin n.succ) (Fin n.succ) R}
    (_h0 : ∀ (j : Fin n.succ), M 0 j = N 0 j)
    (_hsucc : ∀ (i : Fin n) (j : Fin n.succ), M i.succ j = N i.succ j + c i * M i.castSucc j), M.det = N.det
c : Fin n → R
hc : ∀ (i : Fin n), k.succ < i.succ → c i = 0
M N : Matrix (Fin n.succ) (Fin n.succ) R
h0 : ∀ (j : Fin n.succ), M 0 j = N 0 j
hsucc : ∀ (i : Fin n) (j : Fin n.succ), M i.succ j = N i.succ j + c i * M i.castSucc j
M' : Matrix (Fin n.succ) (Fin n.succ) R := M.updateRow k.succ (N k.succ)
hM' : M' = M.updateRow k.succ (N k.succ)
hM : M = M'.updateRow k.succ (M' k.succ + c k • M k.castSucc)
k_ne_succ : k.castSucc ≠ k.succ
M_k : M k.castSucc = M' k.castSucc
refine_2 : ∀ (i : Fin n), k.castSucc < i.succ → update (β := fun (a : Fin n) ↦ R) c k 0 i = 0
refine_2₁ : ∀ (j : Fin n.succ), M' 0 j = N 0 j
refine_2₂ :
  ∀ (i : Fin n) (j : Fin n.succ), M' i.succ j = N i.succ j + update (β := fun (a : Fin n) ↦ R) c k 0 i * M' i.castSucc j
⊢ M.det = N.det

Tactic:
rw [hM, M_k, det_updateRow_add_smul_self M' k_ne_succ.symm, ih (Function.update c k 0)]

Premises used: Function.update, Matrix.det_updateRow_add_smul_self, Ne.symm, OfNat.ofNat
-- Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic
Goal:
R : Type v
inst : CommRing R
n : ℕ
k_1 : Fin (n + 1)
k : Fin n
ih :
  ∀ (c : Fin n → R) (_hc : ∀ (i : Fin n), k.castSucc < i.succ → c i = 0) {M N : Matrix (Fin n.succ) (Fin n.succ) R}
    (_h0 : ∀ (j : Fin n.succ), M 0 j = N 0 j)
    (_hsucc : ∀ (i : Fin n) (j : Fin n.succ), M i.succ j = N i.succ j + c i * M i.castSucc j), M.det = N.det
c : Fin n → R
hc : ∀ (i : Fin n), k.succ < i.succ → c i = 0
M N : Matrix (Fin n.succ) (Fin n.succ) R
h0 : ∀ (j : Fin n.succ), M 0 j = N 0 j
hsucc : ∀ (i : Fin n) (j : Fin n.succ), M i.succ j = N i.succ j + c i * M i.castSucc j
M' : Matrix (Fin n.succ) (Fin n.succ) R := M.updateRow k.succ (N k.succ)
hM' : M' = M.updateRow k.succ (N k.succ)
hM : M = M'.updateRow k.succ (M' k.succ + c k • M k.castSucc)
k_ne_succ : k.castSucc ≠ k.succ
M_k : M k.castSucc = M' k.castSucc
i : Fin n
hi : k.castSucc < i.succ
⊢ (↑k : ℕ) ≤ (↑i : ℕ)

Tactic:
rw [Fin.lt_def, Fin.val_castSucc, Fin.val_succ, Nat.lt_succ_iff] at hi

Premises used: Fin.val_succ, Fin.lt_def, Nat.lt_succ_iff, Fin.val_castSucc
-- Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic
Goal:
R : Type v
inst : CommRing R
n : ℕ
k_1 : Fin (n + 1)
k : Fin n
ih :
  ∀ (c : Fin n → R) (_hc : ∀ (i : Fin n), k.castSucc < i.succ → c i = 0) {M N : Matrix (Fin n.succ) (Fin n.succ) R}
    (_h0 : ∀ (j : Fin n.succ), M 0 j = N 0 j)
    (_hsucc : ∀ (i : Fin n) (j : Fin n.succ), M i.succ j = N i.succ j + c i * M i.castSucc j), M.det = N.det
c : Fin n → R
hc : ∀ (i : Fin n), k.succ < i.succ → c i = 0
M N : Matrix (Fin n.succ) (Fin n.succ) R
h0 : ∀ (j : Fin n.succ), M 0 j = N 0 j
hsucc : ∀ (i : Fin n) (j : Fin n.succ), M i.succ j = N i.succ j + c i * M i.castSucc j
M' : Matrix (Fin n.succ) (Fin n.succ) R := M.updateRow k.succ (N k.succ)
hM' : M' = M.updateRow k.succ (N k.succ)
hM : M = M'.updateRow k.succ (M' k.succ + c k • M k.castSucc)
k_ne_succ : k.castSucc ≠ k.succ
M_k : M k.castSucc = M' k.castSucc
i : Fin n
hi : (↑k : ℕ) ≤ (↑i : ℕ)
refine_2 : (if i = k then 0 else c i) = 0
⊢ update (β := fun (a : Fin n) ↦ R) c k 0 i = 0

Tactic:
rw [Function.update_apply]

Premises used: Function.update_apply
-- Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic
Goal:
R : Type v
inst : CommRing R
n : ℕ
k_1 : Fin (n + 1)
k : Fin n
ih :
  ∀ (c : Fin n → R) (_hc : ∀ (i : Fin n), k.castSucc < i.succ → c i = 0) {M N : Matrix (Fin n.succ) (Fin n.succ) R}
    (_h0 : ∀ (j : Fin n.succ), M 0 j = N 0 j)
    (_hsucc : ∀ (i : Fin n) (j : Fin n.succ), M i.succ j = N i.succ j + c i * M i.castSucc j), M.det = N.det
c : Fin n → R
hc : ∀ (i : Fin n), k.succ < i.succ → c i = 0
M N : Matrix (Fin n.succ) (Fin n.succ) R
h0 : ∀ (j : Fin n.succ), M 0 j = N 0 j
hsucc : ∀ (i : Fin n) (j : Fin n.succ), M i.succ j = N i.succ j + c i * M i.castSucc j
M' : Matrix (Fin n.succ) (Fin n.succ) R := M.updateRow k.succ (N k.succ)
hM' : M' = M.updateRow k.succ (N k.succ)
hM : M = M'.updateRow k.succ (M' k.succ + c k • M k.castSucc)
k_ne_succ : k.castSucc ≠ k.succ
M_k : M k.castSucc = M' k.castSucc
i : Fin n
hi : (↑k : ℕ) ≤ (↑i : ℕ)
pos : ∀ (hik : i = k), Eq.{v + 1} (α := R) 0 0
neg : ∀ (hik : ¬i = k), c i = 0
⊢ (if i = k then 0 else c i) = 0

Tactic:
split_ifs with hik
-- Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic
Goal:
R : Type v
inst : CommRing R
n : ℕ
k_1 : Fin (n + 1)
k : Fin n
ih :
  ∀ (c : Fin n → R) (_hc : ∀ (i : Fin n), k.castSucc < i.succ → c i = 0) {M N : Matrix (Fin n.succ) (Fin n.succ) R}
    (_h0 : ∀ (j : Fin n.succ), M 0 j = N 0 j)
    (_hsucc : ∀ (i : Fin n) (j : Fin n.succ), M i.succ j = N i.succ j + c i * M i.castSucc j), M.det = N.det
c : Fin n → R
hc : ∀ (i : Fin n), k.succ < i.succ → c i = 0
M N : Matrix (Fin n.succ) (Fin n.succ) R
h0 : ∀ (j : Fin n.succ), M 0 j = N 0 j
hsucc : ∀ (i : Fin n) (j : Fin n.succ), M i.succ j = N i.succ j + c i * M i.castSucc j
M' : Matrix (Fin n.succ) (Fin n.succ) R := M.updateRow k.succ (N k.succ)
hM' : M' = M.updateRow k.succ (N k.succ)
hM : M = M'.updateRow k.succ (M' k.succ + c k • M k.castSucc)
k_ne_succ : k.castSucc ≠ k.succ
M_k : M k.castSucc = M' k.castSucc
i : Fin n
hi : (↑k : ℕ) ≤ (↑i : ℕ)
hik : i = k
⊢ Eq.{v + 1} (α := R) 0 0

Tactic:
rfl
-- Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic
Goal:
R : Type v
inst : CommRing R
n : ℕ
k_1 : Fin (n + 1)
k : Fin n
ih :
  ∀ (c : Fin n → R) (_hc : ∀ (i : Fin n), k.castSucc < i.succ → c i = 0) {M N : Matrix (Fin n.succ) (Fin n.succ) R}
    (_h0 : ∀ (j : Fin n.succ), M 0 j = N 0 j)
    (_hsucc : ∀ (i : Fin n) (j : Fin n.succ), M i.succ j = N i.succ j + c i * M i.castSucc j), M.det = N.det
c : Fin n → R
hc : ∀ (i : Fin n), k.succ < i.succ → c i = 0
M N : Matrix (Fin n.succ) (Fin n.succ) R
h0 : ∀ (j : Fin n.succ), M 0 j = N 0 j
hsucc : ∀ (i : Fin n) (j : Fin n.succ), M i.succ j = N i.succ j + c i * M i.castSucc j
M' : Matrix (Fin n.succ) (Fin n.succ) R := M.updateRow k.succ (N k.succ)
hM' : M' = M.updateRow k.succ (N k.succ)
hM : M = M'.updateRow k.succ (M' k.succ + c k • M k.castSucc)
k_ne_succ : k.castSucc ≠ k.succ
M_k : M k.castSucc = M' k.castSucc
i : Fin n
hi : (↑k : ℕ) ≤ (↑i : ℕ)
hik : ¬i = k
⊢ c i = 0

Tactic:
hc _ (Fin.succ_lt_succ_iff.mpr (lt_of_le_of_ne hi (Ne.symm hik)))

Premises used: Iff.mpr, Fin.succ_lt_succ_iff, Ne.symm, lt_of_le_of_ne
-- Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic
Goal:
R : Type v
inst : CommRing R
n : ℕ
k_1 : Fin (n + 1)
k : Fin n
ih :
  ∀ (c : Fin n → R) (_hc : ∀ (i : Fin n), k.castSucc < i.succ → c i = 0) {M N : Matrix (Fin n.succ) (Fin n.succ) R}
    (_h0 : ∀ (j : Fin n.succ), M 0 j = N 0 j)
    (_hsucc : ∀ (i : Fin n) (j : Fin n.succ), M i.succ j = N i.succ j + c i * M i.castSucc j), M.det = N.det
c : Fin n → R
hc : ∀ (i : Fin n), k.succ < i.succ → c i = 0
M N : Matrix (Fin n.succ) (Fin n.succ) R
h0 : ∀ (j : Fin n.succ), M 0 j = N 0 j
hsucc : ∀ (i : Fin n) (j : Fin n.succ), M i.succ j = N i.succ j + c i * M i.castSucc j
M' : Matrix (Fin n.succ) (Fin n.succ) R := M.updateRow k.succ (N k.succ)
hM' : M' = M.updateRow k.succ (N k.succ)
hM : M = M'.updateRow k.succ (M' k.succ + c k • M k.castSucc)
k_ne_succ : k.castSucc ≠ k.succ
M_k : M k.castSucc = M' k.castSucc
i : Fin n
hi : (↑k : ℕ) ≤ (↑i : ℕ)
hik : ¬i = k
⊢ c i = 0

Tactic:
exact hc _ (Fin.succ_lt_succ_iff.mpr (lt_of_le_of_ne hi (Ne.symm hik)))

Premises used: Iff.mpr, Fin.succ_lt_succ_iff, Ne.symm, lt_of_le_of_ne
-- Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic
Goal:
R : Type v
inst : CommRing R
n : ℕ
k_1 : Fin (n + 1)
k : Fin n
ih :
  ∀ (c : Fin n → R) (_hc : ∀ (i : Fin n), k.castSucc < i.succ → c i = 0) {M N : Matrix (Fin n.succ) (Fin n.succ) R}
    (_h0 : ∀ (j : Fin n.succ), M 0 j = N 0 j)
    (_hsucc : ∀ (i : Fin n) (j : Fin n.succ), M i.succ j = N i.succ j + c i * M i.castSucc j), M.det = N.det
c : Fin n → R
hc : ∀ (i : Fin n), k.succ < i.succ → c i = 0
M N : Matrix (Fin n.succ) (Fin n.succ) R
h0 : ∀ (j : Fin n.succ), M 0 j = N 0 j
hsucc : ∀ (i : Fin n) (j : Fin n.succ), M i.succ j = N i.succ j + c i * M i.castSucc j
M' : Matrix (Fin n.succ) (Fin n.succ) R := M.updateRow k.succ (N k.succ)
hM' : M' = M.updateRow k.succ (N k.succ)
hM : M = M'.updateRow k.succ (M' k.succ + c k • M k.castSucc)
k_ne_succ : k.castSucc ≠ k.succ
M_k : M k.castSucc = M' k.castSucc
refine_2 : ∀ (j : Fin n.succ), M.updateRow k.succ (N k.succ) 0 j = N 0 j
refine_2₁ refine_2₂ refine_2₃ refine_2₄ : ∀ (j : Fin n.succ), M 0 j = N 0 j
⊢ ∀ (j : Fin n.succ), M' 0 j = N 0 j

Tactic:
rwa [hM', updateRow_ne (Fin.succ_ne_zero _).symm]

Premises used: Ne.symm, Matrix.updateRow_ne, Fin.succ_ne_zero
-- Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic
Goal:
R : Type v
inst : CommRing R
n : ℕ
k_1 : Fin (n + 1)
k : Fin n
ih :
  ∀ (c : Fin n → R) (_hc : ∀ (i : Fin n), k.castSucc < i.succ → c i = 0) {M N : Matrix (Fin n.succ) (Fin n.succ) R}
    (_h0 : ∀ (j : Fin n.succ), M 0 j = N 0 j)
    (_hsucc : ∀ (i : Fin n) (j : Fin n.succ), M i.succ j = N i.succ j + c i * M i.castSucc j), M.det = N.det
c : Fin n → R
hc : ∀ (i : Fin n), k.succ < i.succ → c i = 0
M N : Matrix (Fin n.succ) (Fin n.succ) R
h0 : ∀ (j : Fin n.succ), M 0 j = N 0 j
hsucc : ∀ (i : Fin n) (j : Fin n.succ), M i.succ j = N i.succ j + c i * M i.castSucc j
M' : Matrix (Fin n.succ) (Fin n.succ) R := M.updateRow k.succ (N k.succ)
hM' : M' = M.updateRow k.succ (N k.succ)
hM : M = M'.updateRow k.succ (M' k.succ + c k • M k.castSucc)
k_ne_succ : k.castSucc ≠ k.succ
M_k : M k.castSucc = M' k.castSucc
i : Fin n
j : Fin n.succ
refine_2 : M' i.succ j = N i.succ j + (if i = k then 0 else c i) * M' i.castSucc j
⊢ M' i.succ j = N i.succ j + update (β := fun (a : Fin n) ↦ R) c k 0 i * M' i.castSucc j

Tactic:
rw [Function.update_apply]

Premises used: Function.update_apply