awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.Basic (goal)
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
⊢ A i j = B i j
have empty₂ : B i j + 0 = B i j
Tactic: rw [A_eq, this, zero_mul, add_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.Basic (goal)
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
⊢ A i j = B i j
have empty₃ : B i j = B i j
Tactic: rw [A_eq, this, zero_mul, add_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.Basic (hypothesis)
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.det = B.det
have hAi : A i = B i + c i • B k
Tactic: have hAi : A i = B i + c i • B k := funext (A_eq i)
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.Basic (goal)
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
⊢ A.det = B.det
have insert : i ≠ k
Tactic: rw [@ih (updateRow B i (A i)) (Function.update c i 0), hAi, det_updateRow_add_smul_self]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.Basic (goal)
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
⊢ A.det = B.det
have insert₁ : ∀ i_1 ∉ s, update (β := fun (a : n) ↦ R) c i 0 i_1 = 0
Tactic: rw [@ih (updateRow B i (A i)) (Function.update c i 0), hAi, det_updateRow_add_smul_self]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.Basic (goal)
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
⊢ A.det = B.det
have insert₃ : k ∉ s
Tactic: rw [@ih (updateRow B i (A i)) (Function.update c i 0), hAi, det_updateRow_add_smul_self]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.Basic (goal)
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
⊢ A.det = B.det
have 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
Tactic: rw [@ih (updateRow B i (A i)) (Function.update c i 0), hAi, det_updateRow_add_smul_self]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.Basic (goal)
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
⊢ update (β := fun (a : n) ↦ R) c i 0 i' = 0
have insert : (if i' = i then 0 else c i') = 0
Tactic: rw [Function.update_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.Basic (goal)
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
⊢ (if i' = i then 0 else c i') = 0
have pos : ∀ (hi'i : i' = i), Eq.{v + 1} (α := R) 0 0
Tactic: split_ifs with hi'i
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.Basic (goal)
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
⊢ (if i' = i then 0 else c i') = 0
have neg : ∀ (hi'i : ¬i' = i), c i' = 0
Tactic: split_ifs with hi'i
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.Basic (goal)
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
⊢ 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'
have 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'
Tactic: rw [updateRow_apply, Function.update_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.Basic (goal)
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
⊢ 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'
have pos : ∀ (hi'i : i' = i), A i' j' = A i j' + 0 * B.updateRow i (A i) k j'
Tactic: split_ifs with hi'i
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.Basic (goal)
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'
⊢ 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'
have neg : ∀ (hi'i : ¬i' = i), A i' j' = B i' j' + c i' * B.updateRow i (A i) k j'
Tactic: split_ifs with hi'i
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.Basic (goal)
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' = B i' j' + c i' * B.updateRow i (A i) k j'
have neg : B i' j' + c i' * B k 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]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.Basic (goal)
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'
⊢ A i' j' = B i' j' + c i' * B.updateRow i (A i) k j'
have neg₁ : B i' j' + c i' * B k j' = B i' j' + c i' * B k j'
Tactic: rw [A_eq, updateRow_ne fun h : k = i => hk <| h ▸ Finset.mem_insert_self k s]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.Basic (goal)
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
⊢ ∀ (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
have 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
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]
Cleared hypotheses: B, s
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.Basic (goal)
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
⊢ ∀ (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
have 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 i s, c i_1 = 0) → ∀ k ∉ insert i 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]
Cleared hypotheses: B, s
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.Basic (goal)
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
have 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
Tactic: refine Fin.induction ?_ (fun k ih => ?_) k
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.Basic (goal)
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
⊢ ∀ (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
have 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
Tactic: refine Fin.induction ?_ (fun k ih => ?_) k
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.Basic (goal)
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
⊢ M.det = N.det
have refine_1 : M = N
Tactic: congr
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.Basic (goal)
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
⊢ M = N
have refine_1 : ∀ (i j : Fin n.succ), M i j = N i j
Tactic: ext i j
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.Basic (goal)
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
have refine_1 : ∀ (i : Fin n), M i.succ j = N i.succ j
Tactic: refine Fin.cases (h0 j) (fun i => ?_) i
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.Basic (goal)
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
⊢ M i.succ j = N i.succ j
have refine_1 : N i.succ j + c i * M i.castSucc j = N i.succ j
Tactic: rw [hsucc, hc i (Fin.succ_pos _), zero_mul, add_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.Basic (goal)
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
⊢ M i.succ j = N i.succ j
have refine_1₁ : N i.succ j + 0 * M i.castSucc j = N i.succ j
Tactic: rw [hsucc, hc i (Fin.succ_pos _), zero_mul, add_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.Basic (goal)
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
⊢ M i.succ j = N i.succ j
have refine_1₂ : N i.succ j + 0 = N i.succ j
Tactic: rw [hsucc, hc i (Fin.succ_pos _), zero_mul, add_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.Basic (goal)
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
⊢ M i.succ j = N i.succ j
have refine_1₃ : N i.succ j = N i.succ j
Tactic: rw [hsucc, hc i (Fin.succ_pos _), zero_mul, add_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.Basic (hypothesis)
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.det = N.det
have hM' : 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'
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.Basic (goal)
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)
have a : ∀ (i j : Fin n.succ), M i j = M'.updateRow k.succ (M' k.succ + c k • M k.castSucc) i j
Tactic: ext i j
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.Basic (goal)
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
⊢ M i j = M'.updateRow k.succ (M' k.succ + c k • M k.castSucc) i j
have pos : ∀ (hi : i = k.succ), M i j = M'.updateRow k.succ (M' k.succ + c k • M k.castSucc) i j
Tactic: by_cases hi : i = k.succ
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.Basic (goal)
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
⊢ M i j = M'.updateRow k.succ (M' k.succ + c k • M k.castSucc) i j
have neg : ∀ (hi : ¬i = k.succ), M i j = M'.updateRow k.succ (M' k.succ + c k • M k.castSucc) i j
Tactic: by_cases hi : i = k.succ
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.Basic (goal)
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
have neg : M i j = M' i j
Tactic: rw [updateRow_ne hi, hM', updateRow_ne hi]