case empty
m : Type ?u.1702450
n : Type u_1
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
R : Type v
inst✝ : CommRing R
A B : Matrix n n R
c : n → R
hs : ∀ (i : n), ¬i ∈ ∅ → c i = 0
k : n
A_eq : ∀ (i j : n), A i j = B i j + c i * B k j
⊢ det A = det B
case empty
m : Type ?u.1702450
n : Type u_1
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
R : Type v
inst✝ : CommRing R
A B : Matrix n n R
⊢ ∀ (c : n → R),
    (∀ (i : n), ¬i ∈ ∅ → c i = 0) → ∀ (k : n), ¬k ∈ ∅ → (∀ (i j : n), A i j = B i j + c i * B k j) → det A = det B
rintro c hs k - A_eq
case empty
m : Type ?u.1702450
n : Type u_1
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
R : Type v
inst✝ : CommRing R
A B : Matrix n n R
c : n → R
hs : ∀ (i : n), ¬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
⊢ det A = det B
case empty
m : Type ?u.1702450
n : Type u_1
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
R : Type v
inst✝ : CommRing R
A B : Matrix n n R
c : n → R
hs : ∀ (i : n), ¬i ∈ ∅ → c i = 0
k : n
A_eq : ∀ (i j : n), A i j = B i j + c i * B k j
⊢ det A = det B
have : ∀ i, c i = 0 := by
  intro i
  specialize hs i
  contrapose! hs
  simp [hs]
case empty.e_M
m : Type ?u.1702450
n : Type u_1
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
R : Type v
inst✝ : CommRing R
A B : Matrix n n R
c : n → R
hs : ∀ (i : n), ¬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
⊢ A = B
case empty
m : Type ?u.1702450
n : Type u_1
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
R : Type v
inst✝ : CommRing R
A B : Matrix n n R
c : n → R
hs : ∀ (i : n), ¬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
⊢ det A = det B
congr
case empty.e_M.a.h
m : Type ?u.1702450
n : Type u_1
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
R : Type v
inst✝ : CommRing R
A B : Matrix n n R
c : n → R
hs : ∀ (i : n), ¬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
⊢ A i j = B i j
case empty.e_M
m : Type ?u.1702450
n : Type u_1
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
R : Type v
inst✝ : CommRing R
A B : Matrix n n R
c : n → R
hs : ∀ (i : n), ¬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
⊢ A = B
ext (i j)
no goals
case empty.e_M.a.h
m : Type ?u.1702450
n : Type u_1
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
R : Type v
inst✝ : CommRing R
A B : Matrix n n R
c : n → R
hs : ∀ (i : n), ¬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
⊢ A i j = B i j
rw [A_eq, this, MulZeroClass.zero_mul, add_zero]
m : Type ?u.1702450
n : Type u_1
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
R : Type v
inst✝ : CommRing R
A B : Matrix n n R
c : n → R
hs : ∀ (i : n), ¬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
m : Type ?u.1702450
n : Type u_1
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
R : Type v
inst✝ : CommRing R
A B : Matrix n n R
c : n → R
hs : ∀ (i : n), ¬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
intro i
m : Type ?u.1702450
n : Type u_1
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
R : Type v
inst✝ : CommRing R
A B : Matrix n n R
c : n → R
k : n
A_eq : ∀ (i j : n), A i j = B i j + c i * B k j
i : n
hs : ¬i ∈ ∅ → c i = 0
⊢ c i = 0
m : Type ?u.1702450
n : Type u_1
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
R : Type v
inst✝ : CommRing R
A B : Matrix n n R
c : n → R
hs : ∀ (i : n), ¬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
specialize hs i
m : Type ?u.1702450
n : Type u_1
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
R : Type v
inst✝ : CommRing R
A B : Matrix n n R
c : n → R
k : n
A_eq : ∀ (i j : n), A i j = B i j + c i * B k j
i : n
hs : c i ≠ 0
⊢ ¬i ∈ ∅ ∧ c i ≠ 0
m : Type ?u.1702450
n : Type u_1
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
R : Type v
inst✝ : CommRing R
A B : Matrix n n R
c : n → R
k : n
A_eq : ∀ (i j : n), A i j = B i j + c i * B k j
i : n
hs : ¬i ∈ ∅ → c i = 0
⊢ c i = 0
contrapose! hs
no goals
m : Type ?u.1702450
n : Type u_1
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
R : Type v
inst✝ : CommRing R
A B : Matrix n n R
c : n → R
k : n
A_eq : ∀ (i j : n), A i j = B i j + c i * B k j
i : n
hs : c i ≠ 0
⊢ ¬i ∈ ∅ ∧ c i ≠ 0
simp [hs]
case insert
m : Type ?u.1702450
n : Type u_1
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
R : Type v
inst✝ : 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 : n), ¬i ∈ s → c i = 0) → ∀ (k : n), ¬k ∈ s → (∀ (i j : n), A i j = B i j + c i * B k j) → det A = det B
B : Matrix n n R
c : n → R
hs : ∀ (i_1 : n), ¬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
⊢ det A = det B
case insert
m : Type ?u.1702450
n : Type u_1
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
R : Type v
inst✝ : 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 : n), ¬i ∈ s → c i = 0) → ∀ (k : n), ¬k ∈ s → (∀ (i j : n), A i j = B i j + c i * B k j) → det A = det B
B : Matrix n n R
⊢ ∀ (c : n → R),
    (∀ (i_1 : n), ¬i_1 ∈ insert i s → c i_1 = 0) →
      ∀ (k : n), ¬k ∈ insert i s → (∀ (i j : n), A i j = B i j + c i * B k j) → det A = det B
intro c hs k hk A_eq
case insert
m : Type ?u.1702450
n : Type u_1
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
R : Type v
inst✝ : 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 : n), ¬i ∈ s → c i = 0) → ∀ (k : n), ¬k ∈ s → (∀ (i j : n), A i j = B i j + c i * B k j) → det A = det B
B : Matrix n n R
c : n → R
hs : ∀ (i_1 : n), ¬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
⊢ det A = det B
case insert
m : Type ?u.1702450
n : Type u_1
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
R : Type v
inst✝ : 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 : n), ¬i ∈ s → c i = 0) → ∀ (k : n), ¬k ∈ s → (∀ (i j : n), A i j = B i j + c i * B k j) → det A = det B
B : Matrix n n R
c : n → R
hs : ∀ (i_1 : n), ¬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
⊢ det A = det B
have hAi : A i = B i + c i • B k := funext (A_eq i)
case insert.hij
m : Type ?u.1702450
n : Type u_1
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
R : Type v
inst✝ : 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 : n), ¬i ∈ s → c i = 0) → ∀ (k : n), ¬k ∈ s → (∀ (i j : n), A i j = B i j + c i * B k j) → det A = det B
B : Matrix n n R
c : n → R
hs : ∀ (i_1 : n), ¬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

case insert.x
m : Type ?u.1702450
n : Type u_1
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
R : Type v
inst✝ : 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 : n), ¬i ∈ s → c i = 0) → ∀ (k : n), ¬k ∈ s → (∀ (i j : n), A i j = B i j + c i * B k j) → det A = det B
B : Matrix n n R
c : n → R
hs : ∀ (i_1 : n), ¬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_1 : n), ¬i_1 ∈ s → update c i 0 i_1 = 0

case insert.k
m : Type ?u.1702450
n : Type u_1
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
R : Type v
inst✝ : 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 : n), ¬i ∈ s → c i = 0) → ∀ (k : n), ¬k ∈ s → (∀ (i j : n), A i j = B i j + c i * B k j) → det A = det B
B : Matrix n n R
c : n → R
hs : ∀ (i_1 : n), ¬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

case insert.x
m : Type ?u.1702450
n : Type u_1
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
R : Type v
inst✝ : 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 : n), ¬i ∈ s → c i = 0) → ∀ (k : n), ¬k ∈ s → (∀ (i j : n), A i j = B i j + c i * B k j) → det A = det B
B : Matrix n n R
c : n → R
hs : ∀ (i_1 : n), ¬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
⊢ ¬?insert.k ∈ s

case insert.x
m : Type ?u.1702450
n : Type u_1
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
R : Type v
inst✝ : 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 : n), ¬i ∈ s → c i = 0) → ∀ (k : n), ¬k ∈ s → (∀ (i j : n), A i j = B i j + c i * B k j) → det A = det B
B : Matrix n n R
c : n → R
hs : ∀ (i_1 : n), ¬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_1 j : n), A i_1 j = updateRow B i (A i) i_1 j + update c i 0 i_1 * updateRow B i (A i) ?insert.k j
case insert
m : Type ?u.1702450
n : Type u_1
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
R : Type v
inst✝ : 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 : n), ¬i ∈ s → c i = 0) → ∀ (k : n), ¬k ∈ s → (∀ (i j : n), A i j = B i j + c i * B k j) → det A = det B
B : Matrix n n R
c : n → R
hs : ∀ (i_1 : n), ¬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
⊢ det A = det B
rw [@ih (updateRow  B i (A i)) (Function.update c i 0), hAi, det_updateRow_add_smul_self]
no goals
case insert.hij
m : Type ?u.1702450
n : Type u_1
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
R : Type v
inst✝ : 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 : n), ¬i ∈ s → c i = 0) → ∀ (k : n), ¬k ∈ s → (∀ (i j : n), A i j = B i j + c i * B k j) → det A = det B
B : Matrix n n R
c : n → R
hs : ∀ (i_1 : n), ¬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
exact mt (fun h => show k ∈ insert i s from h ▸ Finset.mem_insert_self _ _) hk
case insert.x
m : Type ?u.1702450
n : Type u_1
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
R : Type v
inst✝ : 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 : n), ¬i ∈ s → c i = 0) → ∀ (k : n), ¬k ∈ s → (∀ (i j : n), A i j = B i j + c i * B k j) → det A = det B
B : Matrix n n R
c : n → R
hs : ∀ (i_1 : n), ¬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 c i 0 i' = 0
case insert.x
m : Type ?u.1702450
n : Type u_1
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
R : Type v
inst✝ : 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 : n), ¬i ∈ s → c i = 0) → ∀ (k : n), ¬k ∈ s → (∀ (i j : n), A i j = B i j + c i * B k j) → det A = det B
B : Matrix n n R
c : n → R
hs : ∀ (i_1 : n), ¬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_1 : n), ¬i_1 ∈ s → update c i 0 i_1 = 0
intro i' hi'
case insert.x
m : Type ?u.1702450
n : Type u_1
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
R : Type v
inst✝ : 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 : n), ¬i ∈ s → c i = 0) → ∀ (k : n), ¬k ∈ s → (∀ (i j : n), A i j = B i j + c i * B k j) → det A = det B
B : Matrix n n R
c : n → R
hs : ∀ (i_1 : n), ¬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
case insert.x
m : Type ?u.1702450
n : Type u_1
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
R : Type v
inst✝ : 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 : n), ¬i ∈ s → c i = 0) → ∀ (k : n), ¬k ∈ s → (∀ (i j : n), A i j = B i j + c i * B k j) → det A = det B
B : Matrix n n R
c : n → R
hs : ∀ (i_1 : n), ¬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 c i 0 i' = 0
rw [Function.update_apply]
case insert.x.inl
m : Type ?u.1702450
n : Type u_1
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
R : Type v
inst✝ : 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 : n), ¬i ∈ s → c i = 0) → ∀ (k : n), ¬k ∈ s → (∀ (i j : n), A i j = B i j + c i * B k j) → det A = det B
B : Matrix n n R
c : n → R
hs : ∀ (i_1 : n), ¬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
⊢ 0 = 0

case insert.x.inr
m : Type ?u.1702450
n : Type u_1
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
R : Type v
inst✝ : 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 : n), ¬i ∈ s → c i = 0) → ∀ (k : n), ¬k ∈ s → (∀ (i j : n), A i j = B i j + c i * B k j) → det A = det B
B : Matrix n n R
c : n → R
hs : ∀ (i_1 : n), ¬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
case insert.x
m : Type ?u.1702450
n : Type u_1
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
R : Type v
inst✝ : 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 : n), ¬i ∈ s → c i = 0) → ∀ (k : n), ¬k ∈ s → (∀ (i j : n), A i j = B i j + c i * B k j) → det A = det B
B : Matrix n n R
c : n → R
hs : ∀ (i_1 : n), ¬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
split_ifs with hi'i
no goals
case insert.x.inl
m : Type ?u.1702450
n : Type u_1
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
R : Type v
inst✝ : 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 : n), ¬i ∈ s → c i = 0) → ∀ (k : n), ¬k ∈ s → (∀ (i j : n), A i j = B i j + c i * B k j) → det A = det B
B : Matrix n n R
c : n → R
hs : ∀ (i_1 : n), ¬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
⊢ 0 = 0
rfl
no goals
case insert.x.inr
m : Type ?u.1702450
n : Type u_1
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
R : Type v
inst✝ : 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 : n), ¬i ∈ s → c i = 0) → ∀ (k : n), ¬k ∈ s → (∀ (i j : n), A i j = B i j + c i * B k j) → det A = det B
B : Matrix n n R
c : n → R
hs : ∀ (i_1 : n), ¬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
exact hs i' fun h => hi' ((Finset.mem_insert.mp h).resolve_left hi'i)
no goals
case insert.k
m : Type ?u.1702450
n : Type u_1
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
R : Type v
inst✝ : 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 : n), ¬i ∈ s → c i = 0) → ∀ (k : n), ¬k ∈ s → (∀ (i j : n), A i j = B i j + c i * B k j) → det A = det B
B : Matrix n n R
c : n → R
hs : ∀ (i_1 : n), ¬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
exact k
no goals
case insert.x
m : Type ?u.1702450
n : Type u_1
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
R : Type v
inst✝ : 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 : n), ¬i ∈ s → c i = 0) → ∀ (k : n), ¬k ∈ s → (∀ (i j : n), A i j = B i j + c i * B k j) → det A = det B
B : Matrix n n R
c : n → R
hs : ∀ (i_1 : n), ¬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
exact fun h => hk (Finset.mem_insert_of_mem h)
case insert.x
m : Type ?u.1702450
n : Type u_1
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
R : Type v
inst✝ : 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 : n), ¬i ∈ s → c i = 0) → ∀ (k : n), ¬k ∈ s → (∀ (i j : n), A i j = B i j + c i * B k j) → det A = det B
B : Matrix n n R
c : n → R
hs : ∀ (i_1 : n), ¬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' = updateRow B i (A i) i' j' + update c i 0 i' * updateRow B i (A i) k j'
case insert.x
m : Type ?u.1702450
n : Type u_1
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
R : Type v
inst✝ : 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 : n), ¬i ∈ s → c i = 0) → ∀ (k : n), ¬k ∈ s → (∀ (i j : n), A i j = B i j + c i * B k j) → det A = det B
B : Matrix n n R
c : n → R
hs : ∀ (i_1 : n), ¬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_1 j : n), A i_1 j = updateRow B i (A i) i_1 j + update c i 0 i_1 * updateRow B i (A i) k j
intro i' j'
case insert.x
m : Type ?u.1702450
n : Type u_1
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
R : Type v
inst✝ : 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 : n), ¬i ∈ s → c i = 0) → ∀ (k : n), ¬k ∈ s → (∀ (i j : n), A i j = B i j + c i * B k j) → det A = det B
B : Matrix n n R
c : n → R
hs : ∀ (i_1 : n), ¬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') * updateRow B i (A i) k j'
case insert.x
m : Type ?u.1702450
n : Type u_1
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
R : Type v
inst✝ : 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 : n), ¬i ∈ s → c i = 0) → ∀ (k : n), ¬k ∈ s → (∀ (i j : n), A i j = B i j + c i * B k j) → det A = det B
B : Matrix n n R
c : n → R
hs : ∀ (i_1 : n), ¬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' = updateRow B i (A i) i' j' + update c i 0 i' * updateRow B i (A i) k j'
rw [updateRow_apply, Function.update_apply]
case insert.x.inl
m : Type ?u.1702450
n : Type u_1
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
R : Type v
inst✝ : 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 : n), ¬i ∈ s → c i = 0) → ∀ (k : n), ¬k ∈ s → (∀ (i j : n), A i j = B i j + c i * B k j) → det A = det B
B : Matrix n n R
c : n → R
hs : ∀ (i_1 : n), ¬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 * updateRow B i (A i) k j'

case insert.x.inr
m : Type ?u.1702450
n : Type u_1
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
R : Type v
inst✝ : 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 : n), ¬i ∈ s → c i = 0) → ∀ (k : n), ¬k ∈ s → (∀ (i j : n), A i j = B i j + c i * B k j) → det A = det B
B : Matrix n n R
c : n → R
hs : ∀ (i_1 : n), ¬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' * updateRow B i (A i) k j'
case insert.x
m : Type ?u.1702450
n : Type u_1
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
R : Type v
inst✝ : 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 : n), ¬i ∈ s → c i = 0) → ∀ (k : n), ¬k ∈ s → (∀ (i j : n), A i j = B i j + c i * B k j) → det A = det B
B : Matrix n n R
c : n → R
hs : ∀ (i_1 : n), ¬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') * updateRow B i (A i) k j'
split_ifs with hi'i
no goals
case insert.x.inr
m : Type ?u.1702450
n : Type u_1
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
R : Type v
inst✝ : 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 : n), ¬i ∈ s → c i = 0) → ∀ (k : n), ¬k ∈ s → (∀ (i j : n), A i j = B i j + c i * B k j) → det A = det B
B : Matrix n n R
c : n → R
hs : ∀ (i_1 : n), ¬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' * updateRow B i (A i) k j'
rw [A_eq, updateRow_ne fun h : k = i => hk <| h ▸ Finset.mem_insert_self k s]
no goals
case insert.x.inl
m : Type ?u.1702450
n : Type u_1
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
R : Type v
inst✝ : 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 : n), ¬i ∈ s → c i = 0) → ∀ (k : n), ¬k ∈ s → (∀ (i j : n), A i j = B i j + c i * B k j) → det A = det B
B : Matrix n n R
c : n → R
hs : ∀ (i_1 : n), ¬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 * updateRow B i (A i) k j'
simp [hi'i]