case refine'_1
m : Type ?u.1709668
n✝ : Type ?u.1709671
inst✝⁴ : DecidableEq n✝
inst✝³ : Fintype n✝
inst✝² : DecidableEq m
inst✝¹ : Fintype m
R : Type v
inst✝ : CommRing R
n : ℕ
k : Fin (n + 1)
c : Fin n → R
hc : ∀ (i : Fin n), 0 < Fin.succ i → c i = 0
M N : Matrix (Fin (Nat.succ n)) (Fin (Nat.succ n)) R
h0 : ∀ (j : Fin (Nat.succ n)), M 0 j = N 0 j
hsucc : ∀ (i : Fin n) (j : Fin (Nat.succ n)), M (Fin.succ i) j = N (Fin.succ i) j + c i * M (↑Fin.castSucc i) j
⊢ det M = det N

case refine'_2
m : Type ?u.1709668
n✝ : Type ?u.1709671
inst✝⁴ : DecidableEq n✝
inst✝³ : Fintype n✝
inst✝² : DecidableEq m
inst✝¹ : Fintype m
R : Type v
inst✝ : CommRing R
n : ℕ
k✝ : Fin (n + 1)
k : Fin n
ih :
  ∀ (c : Fin n → R),
    (∀ (i : Fin n), ↑Fin.castSucc k < Fin.succ i → c i = 0) →
      ∀ {M N : Matrix (Fin (Nat.succ n)) (Fin (Nat.succ n)) R},
        (∀ (j : Fin (Nat.succ n)), M 0 j = N 0 j) →
          (∀ (i : Fin n) (j : Fin (Nat.succ n)), M (Fin.succ i) j = N (Fin.succ i) j + c i * M (↑Fin.castSucc i) j) →
            det M = det N
c : Fin n → R
hc : ∀ (i : Fin n), Fin.succ k < Fin.succ i → c i = 0
M N : Matrix (Fin (Nat.succ n)) (Fin (Nat.succ n)) R
h0 : ∀ (j : Fin (Nat.succ n)), M 0 j = N 0 j
hsucc : ∀ (i : Fin n) (j : Fin (Nat.succ n)), M (Fin.succ i) j = N (Fin.succ i) j + c i * M (↑Fin.castSucc i) j
⊢ det M = det N
m : Type ?u.1709668
n✝ : Type ?u.1709671
inst✝⁴ : DecidableEq n✝
inst✝³ : Fintype n✝
inst✝² : DecidableEq m
inst✝¹ : Fintype m
R : Type v
inst✝ : CommRing R
n : ℕ
k : Fin (n + 1)
⊢ ∀ (c : Fin n → R),
    (∀ (i : Fin n), k < Fin.succ i → c i = 0) →
      ∀ {M N : Matrix (Fin (Nat.succ n)) (Fin (Nat.succ n)) R},
        (∀ (j : Fin (Nat.succ n)), M 0 j = N 0 j) →
          (∀ (i : Fin n) (j : Fin (Nat.succ n)), M (Fin.succ i) j = N (Fin.succ i) j + c i * M (↑Fin.castSucc i) j) →
            det M = det N
refine' Fin.induction _ (fun k ih => _) k <;> intro c hc M N h0 hsucc
case refine'_2
m : Type ?u.1709668
n✝ : Type ?u.1709671
inst✝⁴ : DecidableEq n✝
inst✝³ : Fintype n✝
inst✝² : DecidableEq m
inst✝¹ : Fintype m
R : Type v
inst✝ : CommRing R
n : ℕ
k✝ : Fin (n + 1)
k : Fin n
ih :
  ∀ (c : Fin n → R),
    (∀ (i : Fin n), ↑Fin.castSucc k < Fin.succ i → c i = 0) →
      ∀ {M N : Matrix (Fin (Nat.succ n)) (Fin (Nat.succ n)) R},
        (∀ (j : Fin (Nat.succ n)), M 0 j = N 0 j) →
          (∀ (i : Fin n) (j : Fin (Nat.succ n)), M (Fin.succ i) j = N (Fin.succ i) j + c i * M (↑Fin.castSucc i) j) →
            det M = det N
c : Fin n → R
hc : ∀ (i : Fin n), Fin.succ k < Fin.succ i → c i = 0
M N : Matrix (Fin (Nat.succ n)) (Fin (Nat.succ n)) R
h0 : ∀ (j : Fin (Nat.succ n)), M 0 j = N 0 j
hsucc : ∀ (i : Fin n) (j : Fin (Nat.succ n)), M (Fin.succ i) j = N (Fin.succ i) j + c i * M (↑Fin.castSucc i) j
M' : Matrix (Fin (Nat.succ n)) (Fin (Nat.succ n)) R := updateRow M (Fin.succ k) (N (Fin.succ k))
hM' : M' = updateRow M (Fin.succ k) (N (Fin.succ k))
⊢ det M = det N
case refine'_2
m : Type ?u.1709668
n✝ : Type ?u.1709671
inst✝⁴ : DecidableEq n✝
inst✝³ : Fintype n✝
inst✝² : DecidableEq m
inst✝¹ : Fintype m
R : Type v
inst✝ : CommRing R
n : ℕ
k✝ : Fin (n + 1)
k : Fin n
ih :
  ∀ (c : Fin n → R),
    (∀ (i : Fin n), ↑Fin.castSucc k < Fin.succ i → c i = 0) →
      ∀ {M N : Matrix (Fin (Nat.succ n)) (Fin (Nat.succ n)) R},
        (∀ (j : Fin (Nat.succ n)), M 0 j = N 0 j) →
          (∀ (i : Fin n) (j : Fin (Nat.succ n)), M (Fin.succ i) j = N (Fin.succ i) j + c i * M (↑Fin.castSucc i) j) →
            det M = det N
c : Fin n → R
hc : ∀ (i : Fin n), Fin.succ k < Fin.succ i → c i = 0
M N : Matrix (Fin (Nat.succ n)) (Fin (Nat.succ n)) R
h0 : ∀ (j : Fin (Nat.succ n)), M 0 j = N 0 j
hsucc : ∀ (i : Fin n) (j : Fin (Nat.succ n)), M (Fin.succ i) j = N (Fin.succ i) j + c i * M (↑Fin.castSucc i) j
⊢ det M = det N
set M' := updateRow M k.succ (N k.succ) with hM'
case refine'_2
m : Type ?u.1709668
n✝ : Type ?u.1709671
inst✝⁴ : DecidableEq n✝
inst✝³ : Fintype n✝
inst✝² : DecidableEq m
inst✝¹ : Fintype m
R : Type v
inst✝ : CommRing R
n : ℕ
k✝ : Fin (n + 1)
k : Fin n
ih :
  ∀ (c : Fin n → R),
    (∀ (i : Fin n), ↑Fin.castSucc k < Fin.succ i → c i = 0) →
      ∀ {M N : Matrix (Fin (Nat.succ n)) (Fin (Nat.succ n)) R},
        (∀ (j : Fin (Nat.succ n)), M 0 j = N 0 j) →
          (∀ (i : Fin n) (j : Fin (Nat.succ n)), M (Fin.succ i) j = N (Fin.succ i) j + c i * M (↑Fin.castSucc i) j) →
            det M = det N
c : Fin n → R
hc : ∀ (i : Fin n), Fin.succ k < Fin.succ i → c i = 0
M N : Matrix (Fin (Nat.succ n)) (Fin (Nat.succ n)) R
h0 : ∀ (j : Fin (Nat.succ n)), M 0 j = N 0 j
hsucc : ∀ (i : Fin n) (j : Fin (Nat.succ n)), M (Fin.succ i) j = N (Fin.succ i) j + c i * M (↑Fin.castSucc i) j
M' : Matrix (Fin (Nat.succ n)) (Fin (Nat.succ n)) R := updateRow M (Fin.succ k) (N (Fin.succ k))
hM' : M' = updateRow M (Fin.succ k) (N (Fin.succ k))
hM : M = updateRow M' (Fin.succ k) (M' (Fin.succ k) + c k • M (↑Fin.castSucc k))
k_ne_succ : ↑Fin.castSucc k ≠ Fin.succ k
⊢ det M = det N
case refine'_2
m : Type ?u.1709668
n✝ : Type ?u.1709671
inst✝⁴ : DecidableEq n✝
inst✝³ : Fintype n✝
inst✝² : DecidableEq m
inst✝¹ : Fintype m
R : Type v
inst✝ : CommRing R
n : ℕ
k✝ : Fin (n + 1)
k : Fin n
ih :
  ∀ (c : Fin n → R),
    (∀ (i : Fin n), ↑Fin.castSucc k < Fin.succ i → c i = 0) →
      ∀ {M N : Matrix (Fin (Nat.succ n)) (Fin (Nat.succ n)) R},
        (∀ (j : Fin (Nat.succ n)), M 0 j = N 0 j) →
          (∀ (i : Fin n) (j : Fin (Nat.succ n)), M (Fin.succ i) j = N (Fin.succ i) j + c i * M (↑Fin.castSucc i) j) →
            det M = det N
c : Fin n → R
hc : ∀ (i : Fin n), Fin.succ k < Fin.succ i → c i = 0
M N : Matrix (Fin (Nat.succ n)) (Fin (Nat.succ n)) R
h0 : ∀ (j : Fin (Nat.succ n)), M 0 j = N 0 j
hsucc : ∀ (i : Fin n) (j : Fin (Nat.succ n)), M (Fin.succ i) j = N (Fin.succ i) j + c i * M (↑Fin.castSucc i) j
M' : Matrix (Fin (Nat.succ n)) (Fin (Nat.succ n)) R := updateRow M (Fin.succ k) (N (Fin.succ k))
hM' : M' = updateRow M (Fin.succ k) (N (Fin.succ k))
hM : M = updateRow M' (Fin.succ k) (M' (Fin.succ k) + c k • M (↑Fin.castSucc k))
⊢ det M = det N
have k_ne_succ : (Fin.castSucc k) ≠ k.succ := (Fin.castSucc_lt_succ k).ne
case refine'_2
m : Type ?u.1709668
n✝ : Type ?u.1709671
inst✝⁴ : DecidableEq n✝
inst✝³ : Fintype n✝
inst✝² : DecidableEq m
inst✝¹ : Fintype m
R : Type v
inst✝ : CommRing R
n : ℕ
k✝ : Fin (n + 1)
k : Fin n
ih :
  ∀ (c : Fin n → R),
    (∀ (i : Fin n), ↑Fin.castSucc k < Fin.succ i → c i = 0) →
      ∀ {M N : Matrix (Fin (Nat.succ n)) (Fin (Nat.succ n)) R},
        (∀ (j : Fin (Nat.succ n)), M 0 j = N 0 j) →
          (∀ (i : Fin n) (j : Fin (Nat.succ n)), M (Fin.succ i) j = N (Fin.succ i) j + c i * M (↑Fin.castSucc i) j) →
            det M = det N
c : Fin n → R
hc : ∀ (i : Fin n), Fin.succ k < Fin.succ i → c i = 0
M N : Matrix (Fin (Nat.succ n)) (Fin (Nat.succ n)) R
h0 : ∀ (j : Fin (Nat.succ n)), M 0 j = N 0 j
hsucc : ∀ (i : Fin n) (j : Fin (Nat.succ n)), M (Fin.succ i) j = N (Fin.succ i) j + c i * M (↑Fin.castSucc i) j
M' : Matrix (Fin (Nat.succ n)) (Fin (Nat.succ n)) R := updateRow M (Fin.succ k) (N (Fin.succ k))
hM' : M' = updateRow M (Fin.succ k) (N (Fin.succ k))
hM : M = updateRow M' (Fin.succ k) (M' (Fin.succ k) + c k • M (↑Fin.castSucc k))
k_ne_succ : ↑Fin.castSucc k ≠ Fin.succ k
M_k : M (↑Fin.castSucc k) = M' (↑Fin.castSucc k)
⊢ det M = det N
case refine'_2
m : Type ?u.1709668
n✝ : Type ?u.1709671
inst✝⁴ : DecidableEq n✝
inst✝³ : Fintype n✝
inst✝² : DecidableEq m
inst✝¹ : Fintype m
R : Type v
inst✝ : CommRing R
n : ℕ
k✝ : Fin (n + 1)
k : Fin n
ih :
  ∀ (c : Fin n → R),
    (∀ (i : Fin n), ↑Fin.castSucc k < Fin.succ i → c i = 0) →
      ∀ {M N : Matrix (Fin (Nat.succ n)) (Fin (Nat.succ n)) R},
        (∀ (j : Fin (Nat.succ n)), M 0 j = N 0 j) →
          (∀ (i : Fin n) (j : Fin (Nat.succ n)), M (Fin.succ i) j = N (Fin.succ i) j + c i * M (↑Fin.castSucc i) j) →
            det M = det N
c : Fin n → R
hc : ∀ (i : Fin n), Fin.succ k < Fin.succ i → c i = 0
M N : Matrix (Fin (Nat.succ n)) (Fin (Nat.succ n)) R
h0 : ∀ (j : Fin (Nat.succ n)), M 0 j = N 0 j
hsucc : ∀ (i : Fin n) (j : Fin (Nat.succ n)), M (Fin.succ i) j = N (Fin.succ i) j + c i * M (↑Fin.castSucc i) j
M' : Matrix (Fin (Nat.succ n)) (Fin (Nat.succ n)) R := updateRow M (Fin.succ k) (N (Fin.succ k))
hM' : M' = updateRow M (Fin.succ k) (N (Fin.succ k))
hM : M = updateRow M' (Fin.succ k) (M' (Fin.succ k) + c k • M (↑Fin.castSucc k))
k_ne_succ : ↑Fin.castSucc k ≠ Fin.succ k
⊢ det M = det N
have M_k : M (Fin.castSucc k) = M' (Fin.castSucc k) := (updateRow_ne k_ne_succ).symm
case refine'_2._hc
m : Type ?u.1709668
n✝ : Type ?u.1709671
inst✝⁴ : DecidableEq n✝
inst✝³ : Fintype n✝
inst✝² : DecidableEq m
inst✝¹ : Fintype m
R : Type v
inst✝ : CommRing R
n : ℕ
k✝ : Fin (n + 1)
k : Fin n
ih :
  ∀ (c : Fin n → R),
    (∀ (i : Fin n), ↑Fin.castSucc k < Fin.succ i → c i = 0) →
      ∀ {M N : Matrix (Fin (Nat.succ n)) (Fin (Nat.succ n)) R},
        (∀ (j : Fin (Nat.succ n)), M 0 j = N 0 j) →
          (∀ (i : Fin n) (j : Fin (Nat.succ n)), M (Fin.succ i) j = N (Fin.succ i) j + c i * M (↑Fin.castSucc i) j) →
            det M = det N
c : Fin n → R
hc : ∀ (i : Fin n), Fin.succ k < Fin.succ i → c i = 0
M N : Matrix (Fin (Nat.succ n)) (Fin (Nat.succ n)) R
h0 : ∀ (j : Fin (Nat.succ n)), M 0 j = N 0 j
hsucc : ∀ (i : Fin n) (j : Fin (Nat.succ n)), M (Fin.succ i) j = N (Fin.succ i) j + c i * M (↑Fin.castSucc i) j
M' : Matrix (Fin (Nat.succ n)) (Fin (Nat.succ n)) R := updateRow M (Fin.succ k) (N (Fin.succ k))
hM' : M' = updateRow M (Fin.succ k) (N (Fin.succ k))
hM : M = updateRow M' (Fin.succ k) (M' (Fin.succ k) + c k • M (↑Fin.castSucc k))
k_ne_succ : ↑Fin.castSucc k ≠ Fin.succ k
M_k : M (↑Fin.castSucc k) = M' (↑Fin.castSucc k)
⊢ ∀ (i : Fin n), ↑Fin.castSucc k < Fin.succ i → update c k 0 i = 0

case refine'_2._h0
m : Type ?u.1709668
n✝ : Type ?u.1709671
inst✝⁴ : DecidableEq n✝
inst✝³ : Fintype n✝
inst✝² : DecidableEq m
inst✝¹ : Fintype m
R : Type v
inst✝ : CommRing R
n : ℕ
k✝ : Fin (n + 1)
k : Fin n
ih :
  ∀ (c : Fin n → R),
    (∀ (i : Fin n), ↑Fin.castSucc k < Fin.succ i → c i = 0) →
      ∀ {M N : Matrix (Fin (Nat.succ n)) (Fin (Nat.succ n)) R},
        (∀ (j : Fin (Nat.succ n)), M 0 j = N 0 j) →
          (∀ (i : Fin n) (j : Fin (Nat.succ n)), M (Fin.succ i) j = N (Fin.succ i) j + c i * M (↑Fin.castSucc i) j) →
            det M = det N
c : Fin n → R
hc : ∀ (i : Fin n), Fin.succ k < Fin.succ i → c i = 0
M N : Matrix (Fin (Nat.succ n)) (Fin (Nat.succ n)) R
h0 : ∀ (j : Fin (Nat.succ n)), M 0 j = N 0 j
hsucc : ∀ (i : Fin n) (j : Fin (Nat.succ n)), M (Fin.succ i) j = N (Fin.succ i) j + c i * M (↑Fin.castSucc i) j
M' : Matrix (Fin (Nat.succ n)) (Fin (Nat.succ n)) R := updateRow M (Fin.succ k) (N (Fin.succ k))
hM' : M' = updateRow M (Fin.succ k) (N (Fin.succ k))
hM : M = updateRow M' (Fin.succ k) (M' (Fin.succ k) + c k • M (↑Fin.castSucc k))
k_ne_succ : ↑Fin.castSucc k ≠ Fin.succ k
M_k : M (↑Fin.castSucc k) = M' (↑Fin.castSucc k)
⊢ ∀ (j : Fin (Nat.succ n)), M' 0 j = N 0 j

case refine'_2._hsucc
m : Type ?u.1709668
n✝ : Type ?u.1709671
inst✝⁴ : DecidableEq n✝
inst✝³ : Fintype n✝
inst✝² : DecidableEq m
inst✝¹ : Fintype m
R : Type v
inst✝ : CommRing R
n : ℕ
k✝ : Fin (n + 1)
k : Fin n
ih :
  ∀ (c : Fin n → R),
    (∀ (i : Fin n), ↑Fin.castSucc k < Fin.succ i → c i = 0) →
      ∀ {M N : Matrix (Fin (Nat.succ n)) (Fin (Nat.succ n)) R},
        (∀ (j : Fin (Nat.succ n)), M 0 j = N 0 j) →
          (∀ (i : Fin n) (j : Fin (Nat.succ n)), M (Fin.succ i) j = N (Fin.succ i) j + c i * M (↑Fin.castSucc i) j) →
            det M = det N
c : Fin n → R
hc : ∀ (i : Fin n), Fin.succ k < Fin.succ i → c i = 0
M N : Matrix (Fin (Nat.succ n)) (Fin (Nat.succ n)) R
h0 : ∀ (j : Fin (Nat.succ n)), M 0 j = N 0 j
hsucc : ∀ (i : Fin n) (j : Fin (Nat.succ n)), M (Fin.succ i) j = N (Fin.succ i) j + c i * M (↑Fin.castSucc i) j
M' : Matrix (Fin (Nat.succ n)) (Fin (Nat.succ n)) R := updateRow M (Fin.succ k) (N (Fin.succ k))
hM' : M' = updateRow M (Fin.succ k) (N (Fin.succ k))
hM : M = updateRow M' (Fin.succ k) (M' (Fin.succ k) + c k • M (↑Fin.castSucc k))
k_ne_succ : ↑Fin.castSucc k ≠ Fin.succ k
M_k : M (↑Fin.castSucc k) = M' (↑Fin.castSucc k)
⊢ ∀ (i : Fin n) (j : Fin (Nat.succ n)), M' (Fin.succ i) j = N (Fin.succ i) j + update c k 0 i * M' (↑Fin.castSucc i) j
case refine'_2
m : Type ?u.1709668
n✝ : Type ?u.1709671
inst✝⁴ : DecidableEq n✝
inst✝³ : Fintype n✝
inst✝² : DecidableEq m
inst✝¹ : Fintype m
R : Type v
inst✝ : CommRing R
n : ℕ
k✝ : Fin (n + 1)
k : Fin n
ih :
  ∀ (c : Fin n → R),
    (∀ (i : Fin n), ↑Fin.castSucc k < Fin.succ i → c i = 0) →
      ∀ {M N : Matrix (Fin (Nat.succ n)) (Fin (Nat.succ n)) R},
        (∀ (j : Fin (Nat.succ n)), M 0 j = N 0 j) →
          (∀ (i : Fin n) (j : Fin (Nat.succ n)), M (Fin.succ i) j = N (Fin.succ i) j + c i * M (↑Fin.castSucc i) j) →
            det M = det N
c : Fin n → R
hc : ∀ (i : Fin n), Fin.succ k < Fin.succ i → c i = 0
M N : Matrix (Fin (Nat.succ n)) (Fin (Nat.succ n)) R
h0 : ∀ (j : Fin (Nat.succ n)), M 0 j = N 0 j
hsucc : ∀ (i : Fin n) (j : Fin (Nat.succ n)), M (Fin.succ i) j = N (Fin.succ i) j + c i * M (↑Fin.castSucc i) j
M' : Matrix (Fin (Nat.succ n)) (Fin (Nat.succ n)) R := updateRow M (Fin.succ k) (N (Fin.succ k))
hM' : M' = updateRow M (Fin.succ k) (N (Fin.succ k))
hM : M = updateRow M' (Fin.succ k) (M' (Fin.succ k) + c k • M (↑Fin.castSucc k))
k_ne_succ : ↑Fin.castSucc k ≠ Fin.succ k
M_k : M (↑Fin.castSucc k) = M' (↑Fin.castSucc k)
⊢ det M = det N
rw [hM, M_k, det_updateRow_add_smul_self M' k_ne_succ.symm, ih (Function.update c k 0)]
case refine'_2._hsucc
m : Type ?u.1709668
n✝ : Type ?u.1709671
inst✝⁴ : DecidableEq n✝
inst✝³ : Fintype n✝
inst✝² : DecidableEq m
inst✝¹ : Fintype m
R : Type v
inst✝ : CommRing R
n : ℕ
k✝ : Fin (n + 1)
k : Fin n
ih :
  ∀ (c : Fin n → R),
    (∀ (i : Fin n), ↑Fin.castSucc k < Fin.succ i → c i = 0) →
      ∀ {M N : Matrix (Fin (Nat.succ n)) (Fin (Nat.succ n)) R},
        (∀ (j : Fin (Nat.succ n)), M 0 j = N 0 j) →
          (∀ (i : Fin n) (j : Fin (Nat.succ n)), M (Fin.succ i) j = N (Fin.succ i) j + c i * M (↑Fin.castSucc i) j) →
            det M = det N
c : Fin n → R
hc : ∀ (i : Fin n), Fin.succ k < Fin.succ i → c i = 0
M N : Matrix (Fin (Nat.succ n)) (Fin (Nat.succ n)) R
h0 : ∀ (j : Fin (Nat.succ n)), M 0 j = N 0 j
hsucc : ∀ (i : Fin n) (j : Fin (Nat.succ n)), M (Fin.succ i) j = N (Fin.succ i) j + c i * M (↑Fin.castSucc i) j
M' : Matrix (Fin (Nat.succ n)) (Fin (Nat.succ n)) R := updateRow M (Fin.succ k) (N (Fin.succ k))
hM' : M' = updateRow M (Fin.succ k) (N (Fin.succ k))
hM : M = updateRow M' (Fin.succ k) (M' (Fin.succ k) + c k • M (↑Fin.castSucc k))
k_ne_succ : ↑Fin.castSucc k ≠ Fin.succ k
M_k : M (↑Fin.castSucc k) = M' (↑Fin.castSucc k)
i : Fin n
j : Fin (Nat.succ n)
⊢ M' (Fin.succ i) j = N (Fin.succ i) j + update c k 0 i * M' (↑Fin.castSucc i) j
case refine'_2._hsucc
m : Type ?u.1709668
n✝ : Type ?u.1709671
inst✝⁴ : DecidableEq n✝
inst✝³ : Fintype n✝
inst✝² : DecidableEq m
inst✝¹ : Fintype m
R : Type v
inst✝ : CommRing R
n : ℕ
k✝ : Fin (n + 1)
k : Fin n
ih :
  ∀ (c : Fin n → R),
    (∀ (i : Fin n), ↑Fin.castSucc k < Fin.succ i → c i = 0) →
      ∀ {M N : Matrix (Fin (Nat.succ n)) (Fin (Nat.succ n)) R},
        (∀ (j : Fin (Nat.succ n)), M 0 j = N 0 j) →
          (∀ (i : Fin n) (j : Fin (Nat.succ n)), M (Fin.succ i) j = N (Fin.succ i) j + c i * M (↑Fin.castSucc i) j) →
            det M = det N
c : Fin n → R
hc : ∀ (i : Fin n), Fin.succ k < Fin.succ i → c i = 0
M N : Matrix (Fin (Nat.succ n)) (Fin (Nat.succ n)) R
h0 : ∀ (j : Fin (Nat.succ n)), M 0 j = N 0 j
hsucc : ∀ (i : Fin n) (j : Fin (Nat.succ n)), M (Fin.succ i) j = N (Fin.succ i) j + c i * M (↑Fin.castSucc i) j
M' : Matrix (Fin (Nat.succ n)) (Fin (Nat.succ n)) R := updateRow M (Fin.succ k) (N (Fin.succ k))
hM' : M' = updateRow M (Fin.succ k) (N (Fin.succ k))
hM : M = updateRow M' (Fin.succ k) (M' (Fin.succ k) + c k • M (↑Fin.castSucc k))
k_ne_succ : ↑Fin.castSucc k ≠ Fin.succ k
M_k : M (↑Fin.castSucc k) = M' (↑Fin.castSucc k)
⊢ ∀ (i : Fin n) (j : Fin (Nat.succ n)), M' (Fin.succ i) j = N (Fin.succ i) j + update c k 0 i * M' (↑Fin.castSucc i) j
intro i j
case refine'_2._hsucc
m : Type ?u.1709668
n✝ : Type ?u.1709671
inst✝⁴ : DecidableEq n✝
inst✝³ : Fintype n✝
inst✝² : DecidableEq m
inst✝¹ : Fintype m
R : Type v
inst✝ : CommRing R
n : ℕ
k✝ : Fin (n + 1)
k : Fin n
ih :
  ∀ (c : Fin n → R),
    (∀ (i : Fin n), ↑Fin.castSucc k < Fin.succ i → c i = 0) →
      ∀ {M N : Matrix (Fin (Nat.succ n)) (Fin (Nat.succ n)) R},
        (∀ (j : Fin (Nat.succ n)), M 0 j = N 0 j) →
          (∀ (i : Fin n) (j : Fin (Nat.succ n)), M (Fin.succ i) j = N (Fin.succ i) j + c i * M (↑Fin.castSucc i) j) →
            det M = det N
c : Fin n → R
hc : ∀ (i : Fin n), Fin.succ k < Fin.succ i → c i = 0
M N : Matrix (Fin (Nat.succ n)) (Fin (Nat.succ n)) R
h0 : ∀ (j : Fin (Nat.succ n)), M 0 j = N 0 j
hsucc : ∀ (i : Fin n) (j : Fin (Nat.succ n)), M (Fin.succ i) j = N (Fin.succ i) j + c i * M (↑Fin.castSucc i) j
M' : Matrix (Fin (Nat.succ n)) (Fin (Nat.succ n)) R := updateRow M (Fin.succ k) (N (Fin.succ k))
hM' : M' = updateRow M (Fin.succ k) (N (Fin.succ k))
hM : M = updateRow M' (Fin.succ k) (M' (Fin.succ k) + c k • M (↑Fin.castSucc k))
k_ne_succ : ↑Fin.castSucc k ≠ Fin.succ k
M_k : M (↑Fin.castSucc k) = M' (↑Fin.castSucc k)
i : Fin n
j : Fin (Nat.succ n)
⊢ M' (Fin.succ i) j = N (Fin.succ i) j + (if i = k then 0 else c i) * M' (↑Fin.castSucc i) j
case refine'_2._hsucc
m : Type ?u.1709668
n✝ : Type ?u.1709671
inst✝⁴ : DecidableEq n✝
inst✝³ : Fintype n✝
inst✝² : DecidableEq m
inst✝¹ : Fintype m
R : Type v
inst✝ : CommRing R
n : ℕ
k✝ : Fin (n + 1)
k : Fin n
ih :
  ∀ (c : Fin n → R),
    (∀ (i : Fin n), ↑Fin.castSucc k < Fin.succ i → c i = 0) →
      ∀ {M N : Matrix (Fin (Nat.succ n)) (Fin (Nat.succ n)) R},
        (∀ (j : Fin (Nat.succ n)), M 0 j = N 0 j) →
          (∀ (i : Fin n) (j : Fin (Nat.succ n)), M (Fin.succ i) j = N (Fin.succ i) j + c i * M (↑Fin.castSucc i) j) →
            det M = det N
c : Fin n → R
hc : ∀ (i : Fin n), Fin.succ k < Fin.succ i → c i = 0
M N : Matrix (Fin (Nat.succ n)) (Fin (Nat.succ n)) R
h0 : ∀ (j : Fin (Nat.succ n)), M 0 j = N 0 j
hsucc : ∀ (i : Fin n) (j : Fin (Nat.succ n)), M (Fin.succ i) j = N (Fin.succ i) j + c i * M (↑Fin.castSucc i) j
M' : Matrix (Fin (Nat.succ n)) (Fin (Nat.succ n)) R := updateRow M (Fin.succ k) (N (Fin.succ k))
hM' : M' = updateRow M (Fin.succ k) (N (Fin.succ k))
hM : M = updateRow M' (Fin.succ k) (M' (Fin.succ k) + c k • M (↑Fin.castSucc k))
k_ne_succ : ↑Fin.castSucc k ≠ Fin.succ k
M_k : M (↑Fin.castSucc k) = M' (↑Fin.castSucc k)
i : Fin n
j : Fin (Nat.succ n)
⊢ M' (Fin.succ i) j = N (Fin.succ i) j + update c k 0 i * M' (↑Fin.castSucc i) j
rw [Function.update_apply]
case refine'_2._hsucc.inl
m : Type ?u.1709668
n✝ : Type ?u.1709671
inst✝⁴ : DecidableEq n✝
inst✝³ : Fintype n✝
inst✝² : DecidableEq m
inst✝¹ : Fintype m
R : Type v
inst✝ : CommRing R
n : ℕ
k✝ : Fin (n + 1)
k : Fin n
ih :
  ∀ (c : Fin n → R),
    (∀ (i : Fin n), ↑Fin.castSucc k < Fin.succ i → c i = 0) →
      ∀ {M N : Matrix (Fin (Nat.succ n)) (Fin (Nat.succ n)) R},
        (∀ (j : Fin (Nat.succ n)), M 0 j = N 0 j) →
          (∀ (i : Fin n) (j : Fin (Nat.succ n)), M (Fin.succ i) j = N (Fin.succ i) j + c i * M (↑Fin.castSucc i) j) →
            det M = det N
c : Fin n → R
hc : ∀ (i : Fin n), Fin.succ k < Fin.succ i → c i = 0
M N : Matrix (Fin (Nat.succ n)) (Fin (Nat.succ n)) R
h0 : ∀ (j : Fin (Nat.succ n)), M 0 j = N 0 j
hsucc : ∀ (i : Fin n) (j : Fin (Nat.succ n)), M (Fin.succ i) j = N (Fin.succ i) j + c i * M (↑Fin.castSucc i) j
M' : Matrix (Fin (Nat.succ n)) (Fin (Nat.succ n)) R := updateRow M (Fin.succ k) (N (Fin.succ k))
hM' : M' = updateRow M (Fin.succ k) (N (Fin.succ k))
hM : M = updateRow M' (Fin.succ k) (M' (Fin.succ k) + c k • M (↑Fin.castSucc k))
k_ne_succ : ↑Fin.castSucc k ≠ Fin.succ k
M_k : M (↑Fin.castSucc k) = M' (↑Fin.castSucc k)
i : Fin n
j : Fin (Nat.succ n)
hik : i = k
⊢ M' (Fin.succ i) j = N (Fin.succ i) j + 0 * M' (↑Fin.castSucc i) j

case refine'_2._hsucc.inr
m : Type ?u.1709668
n✝ : Type ?u.1709671
inst✝⁴ : DecidableEq n✝
inst✝³ : Fintype n✝
inst✝² : DecidableEq m
inst✝¹ : Fintype m
R : Type v
inst✝ : CommRing R
n : ℕ
k✝ : Fin (n + 1)
k : Fin n
ih :
  ∀ (c : Fin n → R),
    (∀ (i : Fin n), ↑Fin.castSucc k < Fin.succ i → c i = 0) →
      ∀ {M N : Matrix (Fin (Nat.succ n)) (Fin (Nat.succ n)) R},
        (∀ (j : Fin (Nat.succ n)), M 0 j = N 0 j) →
          (∀ (i : Fin n) (j : Fin (Nat.succ n)), M (Fin.succ i) j = N (Fin.succ i) j + c i * M (↑Fin.castSucc i) j) →
            det M = det N
c : Fin n → R
hc : ∀ (i : Fin n), Fin.succ k < Fin.succ i → c i = 0
M N : Matrix (Fin (Nat.succ n)) (Fin (Nat.succ n)) R
h0 : ∀ (j : Fin (Nat.succ n)), M 0 j = N 0 j
hsucc : ∀ (i : Fin n) (j : Fin (Nat.succ n)), M (Fin.succ i) j = N (Fin.succ i) j + c i * M (↑Fin.castSucc i) j
M' : Matrix (Fin (Nat.succ n)) (Fin (Nat.succ n)) R := updateRow M (Fin.succ k) (N (Fin.succ k))
hM' : M' = updateRow M (Fin.succ k) (N (Fin.succ k))
hM : M = updateRow M' (Fin.succ k) (M' (Fin.succ k) + c k • M (↑Fin.castSucc k))
k_ne_succ : ↑Fin.castSucc k ≠ Fin.succ k
M_k : M (↑Fin.castSucc k) = M' (↑Fin.castSucc k)
i : Fin n
j : Fin (Nat.succ n)
hik : ¬i = k
⊢ M' (Fin.succ i) j = N (Fin.succ i) j + c i * M' (↑Fin.castSucc i) j
case refine'_2._hsucc
m : Type ?u.1709668
n✝ : Type ?u.1709671
inst✝⁴ : DecidableEq n✝
inst✝³ : Fintype n✝
inst✝² : DecidableEq m
inst✝¹ : Fintype m
R : Type v
inst✝ : CommRing R
n : ℕ
k✝ : Fin (n + 1)
k : Fin n
ih :
  ∀ (c : Fin n → R),
    (∀ (i : Fin n), ↑Fin.castSucc k < Fin.succ i → c i = 0) →
      ∀ {M N : Matrix (Fin (Nat.succ n)) (Fin (Nat.succ n)) R},
        (∀ (j : Fin (Nat.succ n)), M 0 j = N 0 j) →
          (∀ (i : Fin n) (j : Fin (Nat.succ n)), M (Fin.succ i) j = N (Fin.succ i) j + c i * M (↑Fin.castSucc i) j) →
            det M = det N
c : Fin n → R
hc : ∀ (i : Fin n), Fin.succ k < Fin.succ i → c i = 0
M N : Matrix (Fin (Nat.succ n)) (Fin (Nat.succ n)) R
h0 : ∀ (j : Fin (Nat.succ n)), M 0 j = N 0 j
hsucc : ∀ (i : Fin n) (j : Fin (Nat.succ n)), M (Fin.succ i) j = N (Fin.succ i) j + c i * M (↑Fin.castSucc i) j
M' : Matrix (Fin (Nat.succ n)) (Fin (Nat.succ n)) R := updateRow M (Fin.succ k) (N (Fin.succ k))
hM' : M' = updateRow M (Fin.succ k) (N (Fin.succ k))
hM : M = updateRow M' (Fin.succ k) (M' (Fin.succ k) + c k • M (↑Fin.castSucc k))
k_ne_succ : ↑Fin.castSucc k ≠ Fin.succ k
M_k : M (↑Fin.castSucc k) = M' (↑Fin.castSucc k)
i : Fin n
j : Fin (Nat.succ n)
⊢ M' (Fin.succ i) j = N (Fin.succ i) j + (if i = k then 0 else c i) * M' (↑Fin.castSucc i) j
split_ifs with hik
case refine'_2._hsucc.inr
m : Type ?u.1709668
n✝ : Type ?u.1709671
inst✝⁴ : DecidableEq n✝
inst✝³ : Fintype n✝
inst✝² : DecidableEq m
inst✝¹ : Fintype m
R : Type v
inst✝ : CommRing R
n : ℕ
k✝ : Fin (n + 1)
k : Fin n
ih :
  ∀ (c : Fin n → R),
    (∀ (i : Fin n), ↑Fin.castSucc k < Fin.succ i → c i = 0) →
      ∀ {M N : Matrix (Fin (Nat.succ n)) (Fin (Nat.succ n)) R},
        (∀ (j : Fin (Nat.succ n)), M 0 j = N 0 j) →
          (∀ (i : Fin n) (j : Fin (Nat.succ n)), M (Fin.succ i) j = N (Fin.succ i) j + c i * M (↑Fin.castSucc i) j) →
            det M = det N
c : Fin n → R
hc : ∀ (i : Fin n), Fin.succ k < Fin.succ i → c i = 0
M N : Matrix (Fin (Nat.succ n)) (Fin (Nat.succ n)) R
h0 : ∀ (j : Fin (Nat.succ n)), M 0 j = N 0 j
hsucc : ∀ (i : Fin n) (j : Fin (Nat.succ n)), M (Fin.succ i) j = N (Fin.succ i) j + c i * M (↑Fin.castSucc i) j
M' : Matrix (Fin (Nat.succ n)) (Fin (Nat.succ n)) R := updateRow M (Fin.succ k) (N (Fin.succ k))
hM' : M' = updateRow M (Fin.succ k) (N (Fin.succ k))
hM : M = updateRow M' (Fin.succ k) (M' (Fin.succ k) + c k • M (↑Fin.castSucc k))
k_ne_succ : ↑Fin.castSucc k ≠ Fin.succ k
M_k : M (↑Fin.castSucc k) = M' (↑Fin.castSucc k)
i : Fin n
j : Fin (Nat.succ n)
hik : ¬i = k
⊢ N (Fin.succ i) j + c i * M (↑Fin.castSucc i) j =
    N (Fin.succ i) j + c i * updateRow M (Fin.succ k) (N (Fin.succ k)) (↑Fin.castSucc i) j
case refine'_2._hsucc.inr
m : Type ?u.1709668
n✝ : Type ?u.1709671
inst✝⁴ : DecidableEq n✝
inst✝³ : Fintype n✝
inst✝² : DecidableEq m
inst✝¹ : Fintype m
R : Type v
inst✝ : CommRing R
n : ℕ
k✝ : Fin (n + 1)
k : Fin n
ih :
  ∀ (c : Fin n → R),
    (∀ (i : Fin n), ↑Fin.castSucc k < Fin.succ i → c i = 0) →
      ∀ {M N : Matrix (Fin (Nat.succ n)) (Fin (Nat.succ n)) R},
        (∀ (j : Fin (Nat.succ n)), M 0 j = N 0 j) →
          (∀ (i : Fin n) (j : Fin (Nat.succ n)), M (Fin.succ i) j = N (Fin.succ i) j + c i * M (↑Fin.castSucc i) j) →
            det M = det N
c : Fin n → R
hc : ∀ (i : Fin n), Fin.succ k < Fin.succ i → c i = 0
M N : Matrix (Fin (Nat.succ n)) (Fin (Nat.succ n)) R
h0 : ∀ (j : Fin (Nat.succ n)), M 0 j = N 0 j
hsucc : ∀ (i : Fin n) (j : Fin (Nat.succ n)), M (Fin.succ i) j = N (Fin.succ i) j + c i * M (↑Fin.castSucc i) j
M' : Matrix (Fin (Nat.succ n)) (Fin (Nat.succ n)) R := updateRow M (Fin.succ k) (N (Fin.succ k))
hM' : M' = updateRow M (Fin.succ k) (N (Fin.succ k))
hM : M = updateRow M' (Fin.succ k) (M' (Fin.succ k) + c k • M (↑Fin.castSucc k))
k_ne_succ : ↑Fin.castSucc k ≠ Fin.succ k
M_k : M (↑Fin.castSucc k) = M' (↑Fin.castSucc k)
i : Fin n
j : Fin (Nat.succ n)
hik : ¬i = k
⊢ M' (Fin.succ i) j = N (Fin.succ i) j + c i * M' (↑Fin.castSucc i) j
rw [hM', updateRow_ne ((Fin.succ_injective _).ne hik), hsucc]
case pos
m : Type ?u.1709668
n✝ : Type ?u.1709671
inst✝⁴ : DecidableEq n✝
inst✝³ : Fintype n✝
inst✝² : DecidableEq m
inst✝¹ : Fintype m
R : Type v
inst✝ : CommRing R
n : ℕ
k✝ : Fin (n + 1)
k : Fin n
ih :
  ∀ (c : Fin n → R),
    (∀ (i : Fin n), ↑Fin.castSucc k < Fin.succ i → c i = 0) →
      ∀ {M N : Matrix (Fin (Nat.succ n)) (Fin (Nat.succ n)) R},
        (∀ (j : Fin (Nat.succ n)), M 0 j = N 0 j) →
          (∀ (i : Fin n) (j : Fin (Nat.succ n)), M (Fin.succ i) j = N (Fin.succ i) j + c i * M (↑Fin.castSucc i) j) →
            det M = det N
c : Fin n → R
hc : ∀ (i : Fin n), Fin.succ k < Fin.succ i → c i = 0
M N : Matrix (Fin (Nat.succ n)) (Fin (Nat.succ n)) R
h0 : ∀ (j : Fin (Nat.succ n)), M 0 j = N 0 j
hsucc : ∀ (i : Fin n) (j : Fin (Nat.succ n)), M (Fin.succ i) j = N (Fin.succ i) j + c i * M (↑Fin.castSucc i) j
M' : Matrix (Fin (Nat.succ n)) (Fin (Nat.succ n)) R := updateRow M (Fin.succ k) (N (Fin.succ k))
hM' : M' = updateRow M (Fin.succ k) (N (Fin.succ k))
hM : M = updateRow M' (Fin.succ k) (M' (Fin.succ k) + c k • M (↑Fin.castSucc k))
k_ne_succ : ↑Fin.castSucc k ≠ Fin.succ k
M_k : M (↑Fin.castSucc k) = M' (↑Fin.castSucc k)
i : Fin n
j : Fin (Nat.succ n)
hik : ¬i = k
hik2 : k < i
⊢ N (Fin.succ i) j + c i * M (↑Fin.castSucc i) j =
    N (Fin.succ i) j + c i * updateRow M (Fin.succ k) (N (Fin.succ k)) (↑Fin.castSucc i) j

case neg
m : Type ?u.1709668
n✝ : Type ?u.1709671
inst✝⁴ : DecidableEq n✝
inst✝³ : Fintype n✝
inst✝² : DecidableEq m
inst✝¹ : Fintype m
R : Type v
inst✝ : CommRing R
n : ℕ
k✝ : Fin (n + 1)
k : Fin n
ih :
  ∀ (c : Fin n → R),
    (∀ (i : Fin n), ↑Fin.castSucc k < Fin.succ i → c i = 0) →
      ∀ {M N : Matrix (Fin (Nat.succ n)) (Fin (Nat.succ n)) R},
        (∀ (j : Fin (Nat.succ n)), M 0 j = N 0 j) →
          (∀ (i : Fin n) (j : Fin (Nat.succ n)), M (Fin.succ i) j = N (Fin.succ i) j + c i * M (↑Fin.castSucc i) j) →
            det M = det N
c : Fin n → R
hc : ∀ (i : Fin n), Fin.succ k < Fin.succ i → c i = 0
M N : Matrix (Fin (Nat.succ n)) (Fin (Nat.succ n)) R
h0 : ∀ (j : Fin (Nat.succ n)), M 0 j = N 0 j
hsucc : ∀ (i : Fin n) (j : Fin (Nat.succ n)), M (Fin.succ i) j = N (Fin.succ i) j + c i * M (↑Fin.castSucc i) j
M' : Matrix (Fin (Nat.succ n)) (Fin (Nat.succ n)) R := updateRow M (Fin.succ k) (N (Fin.succ k))
hM' : M' = updateRow M (Fin.succ k) (N (Fin.succ k))
hM : M = updateRow M' (Fin.succ k) (M' (Fin.succ k) + c k • M (↑Fin.castSucc k))
k_ne_succ : ↑Fin.castSucc k ≠ Fin.succ k
M_k : M (↑Fin.castSucc k) = M' (↑Fin.castSucc k)
i : Fin n
j : Fin (Nat.succ n)
hik : ¬i = k
hik2 : ¬k < i
⊢ N (Fin.succ i) j + c i * M (↑Fin.castSucc i) j =
    N (Fin.succ i) j + c i * updateRow M (Fin.succ k) (N (Fin.succ k)) (↑Fin.castSucc i) j
case refine'_2._hsucc.inr
m : Type ?u.1709668
n✝ : Type ?u.1709671
inst✝⁴ : DecidableEq n✝
inst✝³ : Fintype n✝
inst✝² : DecidableEq m
inst✝¹ : Fintype m
R : Type v
inst✝ : CommRing R
n : ℕ
k✝ : Fin (n + 1)
k : Fin n
ih :
  ∀ (c : Fin n → R),
    (∀ (i : Fin n), ↑Fin.castSucc k < Fin.succ i → c i = 0) →
      ∀ {M N : Matrix (Fin (Nat.succ n)) (Fin (Nat.succ n)) R},
        (∀ (j : Fin (Nat.succ n)), M 0 j = N 0 j) →
          (∀ (i : Fin n) (j : Fin (Nat.succ n)), M (Fin.succ i) j = N (Fin.succ i) j + c i * M (↑Fin.castSucc i) j) →
            det M = det N
c : Fin n → R
hc : ∀ (i : Fin n), Fin.succ k < Fin.succ i → c i = 0
M N : Matrix (Fin (Nat.succ n)) (Fin (Nat.succ n)) R
h0 : ∀ (j : Fin (Nat.succ n)), M 0 j = N 0 j
hsucc : ∀ (i : Fin n) (j : Fin (Nat.succ n)), M (Fin.succ i) j = N (Fin.succ i) j + c i * M (↑Fin.castSucc i) j
M' : Matrix (Fin (Nat.succ n)) (Fin (Nat.succ n)) R := updateRow M (Fin.succ k) (N (Fin.succ k))
hM' : M' = updateRow M (Fin.succ k) (N (Fin.succ k))
hM : M = updateRow M' (Fin.succ k) (M' (Fin.succ k) + c k • M (↑Fin.castSucc k))
k_ne_succ : ↑Fin.castSucc k ≠ Fin.succ k
M_k : M (↑Fin.castSucc k) = M' (↑Fin.castSucc k)
i : Fin n
j : Fin (Nat.succ n)
hik : ¬i = k
⊢ N (Fin.succ i) j + c i * M (↑Fin.castSucc i) j =
    N (Fin.succ i) j + c i * updateRow M (Fin.succ k) (N (Fin.succ k)) (↑Fin.castSucc i) j
by_cases hik2 : k < i
case neg
m : Type ?u.1709668
n✝ : Type ?u.1709671
inst✝⁴ : DecidableEq n✝
inst✝³ : Fintype n✝
inst✝² : DecidableEq m
inst✝¹ : Fintype m
R : Type v
inst✝ : CommRing R
n : ℕ
k✝ : Fin (n + 1)
k : Fin n
ih :
  ∀ (c : Fin n → R),
    (∀ (i : Fin n), ↑Fin.castSucc k < Fin.succ i → c i = 0) →
      ∀ {M N : Matrix (Fin (Nat.succ n)) (Fin (Nat.succ n)) R},
        (∀ (j : Fin (Nat.succ n)), M 0 j = N 0 j) →
          (∀ (i : Fin n) (j : Fin (Nat.succ n)), M (Fin.succ i) j = N (Fin.succ i) j + c i * M (↑Fin.castSucc i) j) →
            det M = det N
c : Fin n → R
hc : ∀ (i : Fin n), Fin.succ k < Fin.succ i → c i = 0
M N : Matrix (Fin (Nat.succ n)) (Fin (Nat.succ n)) R
h0 : ∀ (j : Fin (Nat.succ n)), M 0 j = N 0 j
hsucc : ∀ (i : Fin n) (j : Fin (Nat.succ n)), M (Fin.succ i) j = N (Fin.succ i) j + c i * M (↑Fin.castSucc i) j
M' : Matrix (Fin (Nat.succ n)) (Fin (Nat.succ n)) R := updateRow M (Fin.succ k) (N (Fin.succ k))
hM' : M' = updateRow M (Fin.succ k) (N (Fin.succ k))
hM : M = updateRow M' (Fin.succ k) (M' (Fin.succ k) + c k • M (↑Fin.castSucc k))
k_ne_succ : ↑Fin.castSucc k ≠ Fin.succ k
M_k : M (↑Fin.castSucc k) = M' (↑Fin.castSucc k)
i : Fin n
j : Fin (Nat.succ n)
hik : ¬i = k
hik2 : ¬k < i
⊢ ↑Fin.castSucc i ≠ Fin.succ k
case neg
m : Type ?u.1709668
n✝ : Type ?u.1709671
inst✝⁴ : DecidableEq n✝
inst✝³ : Fintype n✝
inst✝² : DecidableEq m
inst✝¹ : Fintype m
R : Type v
inst✝ : CommRing R
n : ℕ
k✝ : Fin (n + 1)
k : Fin n
ih :
  ∀ (c : Fin n → R),
    (∀ (i : Fin n), ↑Fin.castSucc k < Fin.succ i → c i = 0) →
      ∀ {M N : Matrix (Fin (Nat.succ n)) (Fin (Nat.succ n)) R},
        (∀ (j : Fin (Nat.succ n)), M 0 j = N 0 j) →
          (∀ (i : Fin n) (j : Fin (Nat.succ n)), M (Fin.succ i) j = N (Fin.succ i) j + c i * M (↑Fin.castSucc i) j) →
            det M = det N
c : Fin n → R
hc : ∀ (i : Fin n), Fin.succ k < Fin.succ i → c i = 0
M N : Matrix (Fin (Nat.succ n)) (Fin (Nat.succ n)) R
h0 : ∀ (j : Fin (Nat.succ n)), M 0 j = N 0 j
hsucc : ∀ (i : Fin n) (j : Fin (Nat.succ n)), M (Fin.succ i) j = N (Fin.succ i) j + c i * M (↑Fin.castSucc i) j
M' : Matrix (Fin (Nat.succ n)) (Fin (Nat.succ n)) R := updateRow M (Fin.succ k) (N (Fin.succ k))
hM' : M' = updateRow M (Fin.succ k) (N (Fin.succ k))
hM : M = updateRow M' (Fin.succ k) (M' (Fin.succ k) + c k • M (↑Fin.castSucc k))
k_ne_succ : ↑Fin.castSucc k ≠ Fin.succ k
M_k : M (↑Fin.castSucc k) = M' (↑Fin.castSucc k)
i : Fin n
j : Fin (Nat.succ n)
hik : ¬i = k
hik2 : ¬k < i
⊢ N (Fin.succ i) j + c i * M (↑Fin.castSucc i) j =
    N (Fin.succ i) j + c i * updateRow M (Fin.succ k) (N (Fin.succ k)) (↑Fin.castSucc i) j
rw [updateRow_ne]
case neg.h
m : Type ?u.1709668
n✝ : Type ?u.1709671
inst✝⁴ : DecidableEq n✝
inst✝³ : Fintype n✝
inst✝² : DecidableEq m
inst✝¹ : Fintype m
R : Type v
inst✝ : CommRing R
n : ℕ
k✝ : Fin (n + 1)
k : Fin n
ih :
  ∀ (c : Fin n → R),
    (∀ (i : Fin n), ↑Fin.castSucc k < Fin.succ i → c i = 0) →
      ∀ {M N : Matrix (Fin (Nat.succ n)) (Fin (Nat.succ n)) R},
        (∀ (j : Fin (Nat.succ n)), M 0 j = N 0 j) →
          (∀ (i : Fin n) (j : Fin (Nat.succ n)), M (Fin.succ i) j = N (Fin.succ i) j + c i * M (↑Fin.castSucc i) j) →
            det M = det N
c : Fin n → R
hc : ∀ (i : Fin n), Fin.succ k < Fin.succ i → c i = 0
M N : Matrix (Fin (Nat.succ n)) (Fin (Nat.succ n)) R
h0 : ∀ (j : Fin (Nat.succ n)), M 0 j = N 0 j
hsucc : ∀ (i : Fin n) (j : Fin (Nat.succ n)), M (Fin.succ i) j = N (Fin.succ i) j + c i * M (↑Fin.castSucc i) j
M' : Matrix (Fin (Nat.succ n)) (Fin (Nat.succ n)) R := updateRow M (Fin.succ k) (N (Fin.succ k))
hM' : M' = updateRow M (Fin.succ k) (N (Fin.succ k))
hM : M = updateRow M' (Fin.succ k) (M' (Fin.succ k) + c k • M (↑Fin.castSucc k))
k_ne_succ : ↑Fin.castSucc k ≠ Fin.succ k
M_k : M (↑Fin.castSucc k) = M' (↑Fin.castSucc k)
i : Fin n
j : Fin (Nat.succ n)
hik : ¬i = k
hik2 : ¬k < i
⊢ ↑Fin.castSucc i < Fin.succ k
case neg
m : Type ?u.1709668
n✝ : Type ?u.1709671
inst✝⁴ : DecidableEq n✝
inst✝³ : Fintype n✝
inst✝² : DecidableEq m
inst✝¹ : Fintype m
R : Type v
inst✝ : CommRing R
n : ℕ
k✝ : Fin (n + 1)
k : Fin n
ih :
  ∀ (c : Fin n → R),
    (∀ (i : Fin n), ↑Fin.castSucc k < Fin.succ i → c i = 0) →
      ∀ {M N : Matrix (Fin (Nat.succ n)) (Fin (Nat.succ n)) R},
        (∀ (j : Fin (Nat.succ n)), M 0 j = N 0 j) →
          (∀ (i : Fin n) (j : Fin (Nat.succ n)), M (Fin.succ i) j = N (Fin.succ i) j + c i * M (↑Fin.castSucc i) j) →
            det M = det N
c : Fin n → R
hc : ∀ (i : Fin n), Fin.succ k < Fin.succ i → c i = 0
M N : Matrix (Fin (Nat.succ n)) (Fin (Nat.succ n)) R
h0 : ∀ (j : Fin (Nat.succ n)), M 0 j = N 0 j
hsucc : ∀ (i : Fin n) (j : Fin (Nat.succ n)), M (Fin.succ i) j = N (Fin.succ i) j + c i * M (↑Fin.castSucc i) j
M' : Matrix (Fin (Nat.succ n)) (Fin (Nat.succ n)) R := updateRow M (Fin.succ k) (N (Fin.succ k))
hM' : M' = updateRow M (Fin.succ k) (N (Fin.succ k))
hM : M = updateRow M' (Fin.succ k) (M' (Fin.succ k) + c k • M (↑Fin.castSucc k))
k_ne_succ : ↑Fin.castSucc k ≠ Fin.succ k
M_k : M (↑Fin.castSucc k) = M' (↑Fin.castSucc k)
i : Fin n
j : Fin (Nat.succ n)
hik : ¬i = k
hik2 : ¬k < i
⊢ ↑Fin.castSucc i ≠ Fin.succ k
apply ne_of_lt
no goals
case neg.h
m : Type ?u.1709668
n✝ : Type ?u.1709671
inst✝⁴ : DecidableEq n✝
inst✝³ : Fintype n✝
inst✝² : DecidableEq m
inst✝¹ : Fintype m
R : Type v
inst✝ : CommRing R
n : ℕ
k✝ : Fin (n + 1)
k : Fin n
ih :
  ∀ (c : Fin n → R),
    (∀ (i : Fin n), ↑Fin.castSucc k < Fin.succ i → c i = 0) →
      ∀ {M N : Matrix (Fin (Nat.succ n)) (Fin (Nat.succ n)) R},
        (∀ (j : Fin (Nat.succ n)), M 0 j = N 0 j) →
          (∀ (i : Fin n) (j : Fin (Nat.succ n)), M (Fin.succ i) j = N (Fin.succ i) j + c i * M (↑Fin.castSucc i) j) →
            det M = det N
c : Fin n → R
hc : ∀ (i : Fin n), Fin.succ k < Fin.succ i → c i = 0
M N : Matrix (Fin (Nat.succ n)) (Fin (Nat.succ n)) R
h0 : ∀ (j : Fin (Nat.succ n)), M 0 j = N 0 j
hsucc : ∀ (i : Fin n) (j : Fin (Nat.succ n)), M (Fin.succ i) j = N (Fin.succ i) j + c i * M (↑Fin.castSucc i) j
M' : Matrix (Fin (Nat.succ n)) (Fin (Nat.succ n)) R := updateRow M (Fin.succ k) (N (Fin.succ k))
hM' : M' = updateRow M (Fin.succ k) (N (Fin.succ k))
hM : M = updateRow M' (Fin.succ k) (M' (Fin.succ k) + c k • M (↑Fin.castSucc k))
k_ne_succ : ↑Fin.castSucc k ≠ Fin.succ k
M_k : M (↑Fin.castSucc k) = M' (↑Fin.castSucc k)
i : Fin n
j : Fin (Nat.succ n)
hik : ¬i = k
hik2 : ¬k < i
⊢ ↑Fin.castSucc i < Fin.succ k
rwa [Fin.lt_iff_val_lt_val, Fin.coe_castSucc, Fin.val_succ, Nat.lt_succ_iff, ← not_lt]
case refine'_1.e_M
m : Type ?u.1709668
n✝ : Type ?u.1709671
inst✝⁴ : DecidableEq n✝
inst✝³ : Fintype n✝
inst✝² : DecidableEq m
inst✝¹ : Fintype m
R : Type v
inst✝ : CommRing R
n : ℕ
k : Fin (n + 1)
c : Fin n → R
hc : ∀ (i : Fin n), 0 < Fin.succ i → c i = 0
M N : Matrix (Fin (Nat.succ n)) (Fin (Nat.succ n)) R
h0 : ∀ (j : Fin (Nat.succ n)), M 0 j = N 0 j
hsucc : ∀ (i : Fin n) (j : Fin (Nat.succ n)), M (Fin.succ i) j = N (Fin.succ i) j + c i * M (↑Fin.castSucc i) j
⊢ M = N
case refine'_1
m : Type ?u.1709668
n✝ : Type ?u.1709671
inst✝⁴ : DecidableEq n✝
inst✝³ : Fintype n✝
inst✝² : DecidableEq m
inst✝¹ : Fintype m
R : Type v
inst✝ : CommRing R
n : ℕ
k : Fin (n + 1)
c : Fin n → R
hc : ∀ (i : Fin n), 0 < Fin.succ i → c i = 0
M N : Matrix (Fin (Nat.succ n)) (Fin (Nat.succ n)) R
h0 : ∀ (j : Fin (Nat.succ n)), M 0 j = N 0 j
hsucc : ∀ (i : Fin n) (j : Fin (Nat.succ n)), M (Fin.succ i) j = N (Fin.succ i) j + c i * M (↑Fin.castSucc i) j
⊢ det M = det N
congr
case refine'_1.e_M.a.h
m : Type ?u.1709668
n✝ : Type ?u.1709671
inst✝⁴ : DecidableEq n✝
inst✝³ : Fintype n✝
inst✝² : DecidableEq m
inst✝¹ : Fintype m
R : Type v
inst✝ : CommRing R
n : ℕ
k : Fin (n + 1)
c : Fin n → R
hc : ∀ (i : Fin n), 0 < Fin.succ i → c i = 0
M N : Matrix (Fin (Nat.succ n)) (Fin (Nat.succ n)) R
h0 : ∀ (j : Fin (Nat.succ n)), M 0 j = N 0 j
hsucc : ∀ (i : Fin n) (j : Fin (Nat.succ n)), M (Fin.succ i) j = N (Fin.succ i) j + c i * M (↑Fin.castSucc i) j
i j : Fin (Nat.succ n)
⊢ M i j = N i j
case refine'_1.e_M
m : Type ?u.1709668
n✝ : Type ?u.1709671
inst✝⁴ : DecidableEq n✝
inst✝³ : Fintype n✝
inst✝² : DecidableEq m
inst✝¹ : Fintype m
R : Type v
inst✝ : CommRing R
n : ℕ
k : Fin (n + 1)
c : Fin n → R
hc : ∀ (i : Fin n), 0 < Fin.succ i → c i = 0
M N : Matrix (Fin (Nat.succ n)) (Fin (Nat.succ n)) R
h0 : ∀ (j : Fin (Nat.succ n)), M 0 j = N 0 j
hsucc : ∀ (i : Fin n) (j : Fin (Nat.succ n)), M (Fin.succ i) j = N (Fin.succ i) j + c i * M (↑Fin.castSucc i) j
⊢ M = N
ext (i j)
case refine'_1.e_M.a.h
m : Type ?u.1709668
n✝ : Type ?u.1709671
inst✝⁴ : DecidableEq n✝
inst✝³ : Fintype n✝
inst✝² : DecidableEq m
inst✝¹ : Fintype m
R : Type v
inst✝ : CommRing R
n : ℕ
k : Fin (n + 1)
c : Fin n → R
hc : ∀ (i : Fin n), 0 < Fin.succ i → c i = 0
M N : Matrix (Fin (Nat.succ n)) (Fin (Nat.succ n)) R
h0 : ∀ (j : Fin (Nat.succ n)), M 0 j = N 0 j
hsucc : ∀ (i : Fin n) (j : Fin (Nat.succ n)), M (Fin.succ i) j = N (Fin.succ i) j + c i * M (↑Fin.castSucc i) j
i✝ j : Fin (Nat.succ n)
i : Fin n
⊢ M (Fin.succ i) j = N (Fin.succ i) j
case refine'_1.e_M.a.h
m : Type ?u.1709668
n✝ : Type ?u.1709671
inst✝⁴ : DecidableEq n✝
inst✝³ : Fintype n✝
inst✝² : DecidableEq m
inst✝¹ : Fintype m
R : Type v
inst✝ : CommRing R
n : ℕ
k : Fin (n + 1)
c : Fin n → R
hc : ∀ (i : Fin n), 0 < Fin.succ i → c i = 0
M N : Matrix (Fin (Nat.succ n)) (Fin (Nat.succ n)) R
h0 : ∀ (j : Fin (Nat.succ n)), M 0 j = N 0 j
hsucc : ∀ (i : Fin n) (j : Fin (Nat.succ n)), M (Fin.succ i) j = N (Fin.succ i) j + c i * M (↑Fin.castSucc i) j
i j : Fin (Nat.succ n)
⊢ M i j = N i j
refine' Fin.cases (h0 j) (fun i => _) i
no goals
case refine'_1.e_M.a.h
m : Type ?u.1709668
n✝ : Type ?u.1709671
inst✝⁴ : DecidableEq n✝
inst✝³ : Fintype n✝
inst✝² : DecidableEq m
inst✝¹ : Fintype m
R : Type v
inst✝ : CommRing R
n : ℕ
k : Fin (n + 1)
c : Fin n → R
hc : ∀ (i : Fin n), 0 < Fin.succ i → c i = 0
M N : Matrix (Fin (Nat.succ n)) (Fin (Nat.succ n)) R
h0 : ∀ (j : Fin (Nat.succ n)), M 0 j = N 0 j
hsucc : ∀ (i : Fin n) (j : Fin (Nat.succ n)), M (Fin.succ i) j = N (Fin.succ i) j + c i * M (↑Fin.castSucc i) j
i✝ j : Fin (Nat.succ n)
i : Fin n
⊢ M (Fin.succ i) j = N (Fin.succ i) j
rw [hsucc, hc i (Fin.succ_pos _), MulZeroClass.zero_mul, add_zero]
case a.h
m : Type ?u.1709668
n✝ : Type ?u.1709671
inst✝⁴ : DecidableEq n✝
inst✝³ : Fintype n✝
inst✝² : DecidableEq m
inst✝¹ : Fintype m
R : Type v
inst✝ : CommRing R
n : ℕ
k✝ : Fin (n + 1)
k : Fin n
ih :
  ∀ (c : Fin n → R),
    (∀ (i : Fin n), ↑Fin.castSucc k < Fin.succ i → c i = 0) →
      ∀ {M N : Matrix (Fin (Nat.succ n)) (Fin (Nat.succ n)) R},
        (∀ (j : Fin (Nat.succ n)), M 0 j = N 0 j) →
          (∀ (i : Fin n) (j : Fin (Nat.succ n)), M (Fin.succ i) j = N (Fin.succ i) j + c i * M (↑Fin.castSucc i) j) →
            det M = det N
c : Fin n → R
hc : ∀ (i : Fin n), Fin.succ k < Fin.succ i → c i = 0
M N : Matrix (Fin (Nat.succ n)) (Fin (Nat.succ n)) R
h0 : ∀ (j : Fin (Nat.succ n)), M 0 j = N 0 j
hsucc : ∀ (i : Fin n) (j : Fin (Nat.succ n)), M (Fin.succ i) j = N (Fin.succ i) j + c i * M (↑Fin.castSucc i) j
M' : Matrix (Fin (Nat.succ n)) (Fin (Nat.succ n)) R := updateRow M (Fin.succ k) (N (Fin.succ k))
hM' : M' = updateRow M (Fin.succ k) (N (Fin.succ k))
i j : Fin (Nat.succ n)
⊢ M i j = updateRow M' (Fin.succ k) (M' (Fin.succ k) + c k • M (↑Fin.castSucc k)) i j
m : Type ?u.1709668
n✝ : Type ?u.1709671
inst✝⁴ : DecidableEq n✝
inst✝³ : Fintype n✝
inst✝² : DecidableEq m
inst✝¹ : Fintype m
R : Type v
inst✝ : CommRing R
n : ℕ
k✝ : Fin (n + 1)
k : Fin n
ih :
  ∀ (c : Fin n → R),
    (∀ (i : Fin n), ↑Fin.castSucc k < Fin.succ i → c i = 0) →
      ∀ {M N : Matrix (Fin (Nat.succ n)) (Fin (Nat.succ n)) R},
        (∀ (j : Fin (Nat.succ n)), M 0 j = N 0 j) →
          (∀ (i : Fin n) (j : Fin (Nat.succ n)), M (Fin.succ i) j = N (Fin.succ i) j + c i * M (↑Fin.castSucc i) j) →
            det M = det N
c : Fin n → R
hc : ∀ (i : Fin n), Fin.succ k < Fin.succ i → c i = 0
M N : Matrix (Fin (Nat.succ n)) (Fin (Nat.succ n)) R
h0 : ∀ (j : Fin (Nat.succ n)), M 0 j = N 0 j
hsucc : ∀ (i : Fin n) (j : Fin (Nat.succ n)), M (Fin.succ i) j = N (Fin.succ i) j + c i * M (↑Fin.castSucc i) j
M' : Matrix (Fin (Nat.succ n)) (Fin (Nat.succ n)) R := updateRow M (Fin.succ k) (N (Fin.succ k))
hM' : M' = updateRow M (Fin.succ k) (N (Fin.succ k))
⊢ M = updateRow M' (Fin.succ k) (M' (Fin.succ k) + c k • M (↑Fin.castSucc k))
ext (i j)
case pos
m : Type ?u.1709668
n✝ : Type ?u.1709671
inst✝⁴ : DecidableEq n✝
inst✝³ : Fintype n✝
inst✝² : DecidableEq m
inst✝¹ : Fintype m
R : Type v
inst✝ : CommRing R
n : ℕ
k✝ : Fin (n + 1)
k : Fin n
ih :
  ∀ (c : Fin n → R),
    (∀ (i : Fin n), ↑Fin.castSucc k < Fin.succ i → c i = 0) →
      ∀ {M N : Matrix (Fin (Nat.succ n)) (Fin (Nat.succ n)) R},
        (∀ (j : Fin (Nat.succ n)), M 0 j = N 0 j) →
          (∀ (i : Fin n) (j : Fin (Nat.succ n)), M (Fin.succ i) j = N (Fin.succ i) j + c i * M (↑Fin.castSucc i) j) →
            det M = det N
c : Fin n → R
hc : ∀ (i : Fin n), Fin.succ k < Fin.succ i → c i = 0
M N : Matrix (Fin (Nat.succ n)) (Fin (Nat.succ n)) R
h0 : ∀ (j : Fin (Nat.succ n)), M 0 j = N 0 j
hsucc : ∀ (i : Fin n) (j : Fin (Nat.succ n)), M (Fin.succ i) j = N (Fin.succ i) j + c i * M (↑Fin.castSucc i) j
M' : Matrix (Fin (Nat.succ n)) (Fin (Nat.succ n)) R := updateRow M (Fin.succ k) (N (Fin.succ k))
hM' : M' = updateRow M (Fin.succ k) (N (Fin.succ k))
i j : Fin (Nat.succ n)
hi : i = Fin.succ k
⊢ M i j = updateRow M' (Fin.succ k) (M' (Fin.succ k) + c k • M (↑Fin.castSucc k)) i j

case neg
m : Type ?u.1709668
n✝ : Type ?u.1709671
inst✝⁴ : DecidableEq n✝
inst✝³ : Fintype n✝
inst✝² : DecidableEq m
inst✝¹ : Fintype m
R : Type v
inst✝ : CommRing R
n : ℕ
k✝ : Fin (n + 1)
k : Fin n
ih :
  ∀ (c : Fin n → R),
    (∀ (i : Fin n), ↑Fin.castSucc k < Fin.succ i → c i = 0) →
      ∀ {M N : Matrix (Fin (Nat.succ n)) (Fin (Nat.succ n)) R},
        (∀ (j : Fin (Nat.succ n)), M 0 j = N 0 j) →
          (∀ (i : Fin n) (j : Fin (Nat.succ n)), M (Fin.succ i) j = N (Fin.succ i) j + c i * M (↑Fin.castSucc i) j) →
            det M = det N
c : Fin n → R
hc : ∀ (i : Fin n), Fin.succ k < Fin.succ i → c i = 0
M N : Matrix (Fin (Nat.succ n)) (Fin (Nat.succ n)) R
h0 : ∀ (j : Fin (Nat.succ n)), M 0 j = N 0 j
hsucc : ∀ (i : Fin n) (j : Fin (Nat.succ n)), M (Fin.succ i) j = N (Fin.succ i) j + c i * M (↑Fin.castSucc i) j
M' : Matrix (Fin (Nat.succ n)) (Fin (Nat.succ n)) R := updateRow M (Fin.succ k) (N (Fin.succ k))
hM' : M' = updateRow M (Fin.succ k) (N (Fin.succ k))
i j : Fin (Nat.succ n)
hi : ¬i = Fin.succ k
⊢ M i j = updateRow M' (Fin.succ k) (M' (Fin.succ k) + c k • M (↑Fin.castSucc k)) i j
case a.h
m : Type ?u.1709668
n✝ : Type ?u.1709671
inst✝⁴ : DecidableEq n✝
inst✝³ : Fintype n✝
inst✝² : DecidableEq m
inst✝¹ : Fintype m
R : Type v
inst✝ : CommRing R
n : ℕ
k✝ : Fin (n + 1)
k : Fin n
ih :
  ∀ (c : Fin n → R),
    (∀ (i : Fin n), ↑Fin.castSucc k < Fin.succ i → c i = 0) →
      ∀ {M N : Matrix (Fin (Nat.succ n)) (Fin (Nat.succ n)) R},
        (∀ (j : Fin (Nat.succ n)), M 0 j = N 0 j) →
          (∀ (i : Fin n) (j : Fin (Nat.succ n)), M (Fin.succ i) j = N (Fin.succ i) j + c i * M (↑Fin.castSucc i) j) →
            det M = det N
c : Fin n → R
hc : ∀ (i : Fin n), Fin.succ k < Fin.succ i → c i = 0
M N : Matrix (Fin (Nat.succ n)) (Fin (Nat.succ n)) R
h0 : ∀ (j : Fin (Nat.succ n)), M 0 j = N 0 j
hsucc : ∀ (i : Fin n) (j : Fin (Nat.succ n)), M (Fin.succ i) j = N (Fin.succ i) j + c i * M (↑Fin.castSucc i) j
M' : Matrix (Fin (Nat.succ n)) (Fin (Nat.succ n)) R := updateRow M (Fin.succ k) (N (Fin.succ k))
hM' : M' = updateRow M (Fin.succ k) (N (Fin.succ k))
i j : Fin (Nat.succ n)
⊢ M i j = updateRow M' (Fin.succ k) (M' (Fin.succ k) + c k • M (↑Fin.castSucc k)) i j
by_cases hi : i = k.succ
no goals
case neg
m : Type ?u.1709668
n✝ : Type ?u.1709671
inst✝⁴ : DecidableEq n✝
inst✝³ : Fintype n✝
inst✝² : DecidableEq m
inst✝¹ : Fintype m
R : Type v
inst✝ : CommRing R
n : ℕ
k✝ : Fin (n + 1)
k : Fin n
ih :
  ∀ (c : Fin n → R),
    (∀ (i : Fin n), ↑Fin.castSucc k < Fin.succ i → c i = 0) →
      ∀ {M N : Matrix (Fin (Nat.succ n)) (Fin (Nat.succ n)) R},
        (∀ (j : Fin (Nat.succ n)), M 0 j = N 0 j) →
          (∀ (i : Fin n) (j : Fin (Nat.succ n)), M (Fin.succ i) j = N (Fin.succ i) j + c i * M (↑Fin.castSucc i) j) →
            det M = det N
c : Fin n → R
hc : ∀ (i : Fin n), Fin.succ k < Fin.succ i → c i = 0
M N : Matrix (Fin (Nat.succ n)) (Fin (Nat.succ n)) R
h0 : ∀ (j : Fin (Nat.succ n)), M 0 j = N 0 j
hsucc : ∀ (i : Fin n) (j : Fin (Nat.succ n)), M (Fin.succ i) j = N (Fin.succ i) j + c i * M (↑Fin.castSucc i) j
M' : Matrix (Fin (Nat.succ n)) (Fin (Nat.succ n)) R := updateRow M (Fin.succ k) (N (Fin.succ k))
hM' : M' = updateRow M (Fin.succ k) (N (Fin.succ k))
i j : Fin (Nat.succ n)
hi : ¬i = Fin.succ k
⊢ M i j = updateRow M' (Fin.succ k) (M' (Fin.succ k) + c k • M (↑Fin.castSucc k)) i j
rw [updateRow_ne hi, hM', updateRow_ne hi]
no goals
case pos
m : Type ?u.1709668
n✝ : Type ?u.1709671
inst✝⁴ : DecidableEq n✝
inst✝³ : Fintype n✝
inst✝² : DecidableEq m
inst✝¹ : Fintype m
R : Type v
inst✝ : CommRing R
n : ℕ
k✝ : Fin (n + 1)
k : Fin n
ih :
  ∀ (c : Fin n → R),
    (∀ (i : Fin n), ↑Fin.castSucc k < Fin.succ i → c i = 0) →
      ∀ {M N : Matrix (Fin (Nat.succ n)) (Fin (Nat.succ n)) R},
        (∀ (j : Fin (Nat.succ n)), M 0 j = N 0 j) →
          (∀ (i : Fin n) (j : Fin (Nat.succ n)), M (Fin.succ i) j = N (Fin.succ i) j + c i * M (↑Fin.castSucc i) j) →
            det M = det N
c : Fin n → R
hc : ∀ (i : Fin n), Fin.succ k < Fin.succ i → c i = 0
M N : Matrix (Fin (Nat.succ n)) (Fin (Nat.succ n)) R
h0 : ∀ (j : Fin (Nat.succ n)), M 0 j = N 0 j
hsucc : ∀ (i : Fin n) (j : Fin (Nat.succ n)), M (Fin.succ i) j = N (Fin.succ i) j + c i * M (↑Fin.castSucc i) j
M' : Matrix (Fin (Nat.succ n)) (Fin (Nat.succ n)) R := updateRow M (Fin.succ k) (N (Fin.succ k))
hM' : M' = updateRow M (Fin.succ k) (N (Fin.succ k))
i j : Fin (Nat.succ n)
hi : i = Fin.succ k
⊢ M i j = updateRow M' (Fin.succ k) (M' (Fin.succ k) + c k • M (↑Fin.castSucc k)) i j
simp [hi, hM', hsucc, updateRow_self]
case refine'_2._hc
m : Type ?u.1709668
n✝ : Type ?u.1709671
inst✝⁴ : DecidableEq n✝
inst✝³ : Fintype n✝
inst✝² : DecidableEq m
inst✝¹ : Fintype m
R : Type v
inst✝ : CommRing R
n : ℕ
k✝ : Fin (n + 1)
k : Fin n
ih :
  ∀ (c : Fin n → R),
    (∀ (i : Fin n), ↑Fin.castSucc k < Fin.succ i → c i = 0) →
      ∀ {M N : Matrix (Fin (Nat.succ n)) (Fin (Nat.succ n)) R},
        (∀ (j : Fin (Nat.succ n)), M 0 j = N 0 j) →
          (∀ (i : Fin n) (j : Fin (Nat.succ n)), M (Fin.succ i) j = N (Fin.succ i) j + c i * M (↑Fin.castSucc i) j) →
            det M = det N
c : Fin n → R
hc : ∀ (i : Fin n), Fin.succ k < Fin.succ i → c i = 0
M N : Matrix (Fin (Nat.succ n)) (Fin (Nat.succ n)) R
h0 : ∀ (j : Fin (Nat.succ n)), M 0 j = N 0 j
hsucc : ∀ (i : Fin n) (j : Fin (Nat.succ n)), M (Fin.succ i) j = N (Fin.succ i) j + c i * M (↑Fin.castSucc i) j
M' : Matrix (Fin (Nat.succ n)) (Fin (Nat.succ n)) R := updateRow M (Fin.succ k) (N (Fin.succ k))
hM' : M' = updateRow M (Fin.succ k) (N (Fin.succ k))
hM : M = updateRow M' (Fin.succ k) (M' (Fin.succ k) + c k • M (↑Fin.castSucc k))
k_ne_succ : ↑Fin.castSucc k ≠ Fin.succ k
M_k : M (↑Fin.castSucc k) = M' (↑Fin.castSucc k)
i : Fin n
hi : ↑Fin.castSucc k < Fin.succ i
⊢ update c k 0 i = 0
case refine'_2._hc
m : Type ?u.1709668
n✝ : Type ?u.1709671
inst✝⁴ : DecidableEq n✝
inst✝³ : Fintype n✝
inst✝² : DecidableEq m
inst✝¹ : Fintype m
R : Type v
inst✝ : CommRing R
n : ℕ
k✝ : Fin (n + 1)
k : Fin n
ih :
  ∀ (c : Fin n → R),
    (∀ (i : Fin n), ↑Fin.castSucc k < Fin.succ i → c i = 0) →
      ∀ {M N : Matrix (Fin (Nat.succ n)) (Fin (Nat.succ n)) R},
        (∀ (j : Fin (Nat.succ n)), M 0 j = N 0 j) →
          (∀ (i : Fin n) (j : Fin (Nat.succ n)), M (Fin.succ i) j = N (Fin.succ i) j + c i * M (↑Fin.castSucc i) j) →
            det M = det N
c : Fin n → R
hc : ∀ (i : Fin n), Fin.succ k < Fin.succ i → c i = 0
M N : Matrix (Fin (Nat.succ n)) (Fin (Nat.succ n)) R
h0 : ∀ (j : Fin (Nat.succ n)), M 0 j = N 0 j
hsucc : ∀ (i : Fin n) (j : Fin (Nat.succ n)), M (Fin.succ i) j = N (Fin.succ i) j + c i * M (↑Fin.castSucc i) j
M' : Matrix (Fin (Nat.succ n)) (Fin (Nat.succ n)) R := updateRow M (Fin.succ k) (N (Fin.succ k))
hM' : M' = updateRow M (Fin.succ k) (N (Fin.succ k))
hM : M = updateRow M' (Fin.succ k) (M' (Fin.succ k) + c k • M (↑Fin.castSucc k))
k_ne_succ : ↑Fin.castSucc k ≠ Fin.succ k
M_k : M (↑Fin.castSucc k) = M' (↑Fin.castSucc k)
⊢ ∀ (i : Fin n), ↑Fin.castSucc k < Fin.succ i → update c k 0 i = 0
intro i hi
case refine'_2._hc
m : Type ?u.1709668
n✝ : Type ?u.1709671
inst✝⁴ : DecidableEq n✝
inst✝³ : Fintype n✝
inst✝² : DecidableEq m
inst✝¹ : Fintype m
R : Type v
inst✝ : CommRing R
n : ℕ
k✝ : Fin (n + 1)
k : Fin n
ih :
  ∀ (c : Fin n → R),
    (∀ (i : Fin n), ↑Fin.castSucc k < Fin.succ i → c i = 0) →
      ∀ {M N : Matrix (Fin (Nat.succ n)) (Fin (Nat.succ n)) R},
        (∀ (j : Fin (Nat.succ n)), M 0 j = N 0 j) →
          (∀ (i : Fin n) (j : Fin (Nat.succ n)), M (Fin.succ i) j = N (Fin.succ i) j + c i * M (↑Fin.castSucc i) j) →
            det M = det N
c : Fin n → R
hc : ∀ (i : Fin n), Fin.succ k < Fin.succ i → c i = 0
M N : Matrix (Fin (Nat.succ n)) (Fin (Nat.succ n)) R
h0 : ∀ (j : Fin (Nat.succ n)), M 0 j = N 0 j
hsucc : ∀ (i : Fin n) (j : Fin (Nat.succ n)), M (Fin.succ i) j = N (Fin.succ i) j + c i * M (↑Fin.castSucc i) j
M' : Matrix (Fin (Nat.succ n)) (Fin (Nat.succ n)) R := updateRow M (Fin.succ k) (N (Fin.succ k))
hM' : M' = updateRow M (Fin.succ k) (N (Fin.succ k))
hM : M = updateRow M' (Fin.succ k) (M' (Fin.succ k) + c k • M (↑Fin.castSucc k))
k_ne_succ : ↑Fin.castSucc k ≠ Fin.succ k
M_k : M (↑Fin.castSucc k) = M' (↑Fin.castSucc k)
i : Fin n
hi : ↑k ≤ ↑i
⊢ update c k 0 i = 0
case refine'_2._hc
m : Type ?u.1709668
n✝ : Type ?u.1709671
inst✝⁴ : DecidableEq n✝
inst✝³ : Fintype n✝
inst✝² : DecidableEq m
inst✝¹ : Fintype m
R : Type v
inst✝ : CommRing R
n : ℕ
k✝ : Fin (n + 1)
k : Fin n
ih :
  ∀ (c : Fin n → R),
    (∀ (i : Fin n), ↑Fin.castSucc k < Fin.succ i → c i = 0) →
      ∀ {M N : Matrix (Fin (Nat.succ n)) (Fin (Nat.succ n)) R},
        (∀ (j : Fin (Nat.succ n)), M 0 j = N 0 j) →
          (∀ (i : Fin n) (j : Fin (Nat.succ n)), M (Fin.succ i) j = N (Fin.succ i) j + c i * M (↑Fin.castSucc i) j) →
            det M = det N
c : Fin n → R
hc : ∀ (i : Fin n), Fin.succ k < Fin.succ i → c i = 0
M N : Matrix (Fin (Nat.succ n)) (Fin (Nat.succ n)) R
h0 : ∀ (j : Fin (Nat.succ n)), M 0 j = N 0 j
hsucc : ∀ (i : Fin n) (j : Fin (Nat.succ n)), M (Fin.succ i) j = N (Fin.succ i) j + c i * M (↑Fin.castSucc i) j
M' : Matrix (Fin (Nat.succ n)) (Fin (Nat.succ n)) R := updateRow M (Fin.succ k) (N (Fin.succ k))
hM' : M' = updateRow M (Fin.succ k) (N (Fin.succ k))
hM : M = updateRow M' (Fin.succ k) (M' (Fin.succ k) + c k • M (↑Fin.castSucc k))
k_ne_succ : ↑Fin.castSucc k ≠ Fin.succ k
M_k : M (↑Fin.castSucc k) = M' (↑Fin.castSucc k)
i : Fin n
hi : ↑Fin.castSucc k < Fin.succ i
⊢ update c k 0 i = 0
rw [Fin.lt_iff_val_lt_val, Fin.coe_castSucc, Fin.val_succ, Nat.lt_succ_iff] at hi
case refine'_2._hc
m : Type ?u.1709668
n✝ : Type ?u.1709671
inst✝⁴ : DecidableEq n✝
inst✝³ : Fintype n✝
inst✝² : DecidableEq m
inst✝¹ : Fintype m
R : Type v
inst✝ : CommRing R
n : ℕ
k✝ : Fin (n + 1)
k : Fin n
ih :
  ∀ (c : Fin n → R),
    (∀ (i : Fin n), ↑Fin.castSucc k < Fin.succ i → c i = 0) →
      ∀ {M N : Matrix (Fin (Nat.succ n)) (Fin (Nat.succ n)) R},
        (∀ (j : Fin (Nat.succ n)), M 0 j = N 0 j) →
          (∀ (i : Fin n) (j : Fin (Nat.succ n)), M (Fin.succ i) j = N (Fin.succ i) j + c i * M (↑Fin.castSucc i) j) →
            det M = det N
c : Fin n → R
hc : ∀ (i : Fin n), Fin.succ k < Fin.succ i → c i = 0
M N : Matrix (Fin (Nat.succ n)) (Fin (Nat.succ n)) R
h0 : ∀ (j : Fin (Nat.succ n)), M 0 j = N 0 j
hsucc : ∀ (i : Fin n) (j : Fin (Nat.succ n)), M (Fin.succ i) j = N (Fin.succ i) j + c i * M (↑Fin.castSucc i) j
M' : Matrix (Fin (Nat.succ n)) (Fin (Nat.succ n)) R := updateRow M (Fin.succ k) (N (Fin.succ k))
hM' : M' = updateRow M (Fin.succ k) (N (Fin.succ k))
hM : M = updateRow M' (Fin.succ k) (M' (Fin.succ k) + c k • M (↑Fin.castSucc k))
k_ne_succ : ↑Fin.castSucc k ≠ Fin.succ k
M_k : M (↑Fin.castSucc k) = M' (↑Fin.castSucc k)
i : Fin n
hi : ↑k ≤ ↑i
⊢ (if i = k then 0 else c i) = 0
case refine'_2._hc
m : Type ?u.1709668
n✝ : Type ?u.1709671
inst✝⁴ : DecidableEq n✝
inst✝³ : Fintype n✝
inst✝² : DecidableEq m
inst✝¹ : Fintype m
R : Type v
inst✝ : CommRing R
n : ℕ
k✝ : Fin (n + 1)
k : Fin n
ih :
  ∀ (c : Fin n → R),
    (∀ (i : Fin n), ↑Fin.castSucc k < Fin.succ i → c i = 0) →
      ∀ {M N : Matrix (Fin (Nat.succ n)) (Fin (Nat.succ n)) R},
        (∀ (j : Fin (Nat.succ n)), M 0 j = N 0 j) →
          (∀ (i : Fin n) (j : Fin (Nat.succ n)), M (Fin.succ i) j = N (Fin.succ i) j + c i * M (↑Fin.castSucc i) j) →
            det M = det N
c : Fin n → R
hc : ∀ (i : Fin n), Fin.succ k < Fin.succ i → c i = 0
M N : Matrix (Fin (Nat.succ n)) (Fin (Nat.succ n)) R
h0 : ∀ (j : Fin (Nat.succ n)), M 0 j = N 0 j
hsucc : ∀ (i : Fin n) (j : Fin (Nat.succ n)), M (Fin.succ i) j = N (Fin.succ i) j + c i * M (↑Fin.castSucc i) j
M' : Matrix (Fin (Nat.succ n)) (Fin (Nat.succ n)) R := updateRow M (Fin.succ k) (N (Fin.succ k))
hM' : M' = updateRow M (Fin.succ k) (N (Fin.succ k))
hM : M = updateRow M' (Fin.succ k) (M' (Fin.succ k) + c k • M (↑Fin.castSucc k))
k_ne_succ : ↑Fin.castSucc k ≠ Fin.succ k
M_k : M (↑Fin.castSucc k) = M' (↑Fin.castSucc k)
i : Fin n
hi : ↑k ≤ ↑i
⊢ update c k 0 i = 0
rw [Function.update_apply]
case refine'_2._hc.inl
m : Type ?u.1709668
n✝ : Type ?u.1709671
inst✝⁴ : DecidableEq n✝
inst✝³ : Fintype n✝
inst✝² : DecidableEq m
inst✝¹ : Fintype m
R : Type v
inst✝ : CommRing R
n : ℕ
k✝ : Fin (n + 1)
k : Fin n
ih :
  ∀ (c : Fin n → R),
    (∀ (i : Fin n), ↑Fin.castSucc k < Fin.succ i → c i = 0) →
      ∀ {M N : Matrix (Fin (Nat.succ n)) (Fin (Nat.succ n)) R},
        (∀ (j : Fin (Nat.succ n)), M 0 j = N 0 j) →
          (∀ (i : Fin n) (j : Fin (Nat.succ n)), M (Fin.succ i) j = N (Fin.succ i) j + c i * M (↑Fin.castSucc i) j) →
            det M = det N
c : Fin n → R
hc : ∀ (i : Fin n), Fin.succ k < Fin.succ i → c i = 0
M N : Matrix (Fin (Nat.succ n)) (Fin (Nat.succ n)) R
h0 : ∀ (j : Fin (Nat.succ n)), M 0 j = N 0 j
hsucc : ∀ (i : Fin n) (j : Fin (Nat.succ n)), M (Fin.succ i) j = N (Fin.succ i) j + c i * M (↑Fin.castSucc i) j
M' : Matrix (Fin (Nat.succ n)) (Fin (Nat.succ n)) R := updateRow M (Fin.succ k) (N (Fin.succ k))
hM' : M' = updateRow M (Fin.succ k) (N (Fin.succ k))
hM : M = updateRow M' (Fin.succ k) (M' (Fin.succ k) + c k • M (↑Fin.castSucc k))
k_ne_succ : ↑Fin.castSucc k ≠ Fin.succ k
M_k : M (↑Fin.castSucc k) = M' (↑Fin.castSucc k)
i : Fin n
hi : ↑k ≤ ↑i
hik : i = k
⊢ 0 = 0

case refine'_2._hc.inr
m : Type ?u.1709668
n✝ : Type ?u.1709671
inst✝⁴ : DecidableEq n✝
inst✝³ : Fintype n✝
inst✝² : DecidableEq m
inst✝¹ : Fintype m
R : Type v
inst✝ : CommRing R
n : ℕ
k✝ : Fin (n + 1)
k : Fin n
ih :
  ∀ (c : Fin n → R),
    (∀ (i : Fin n), ↑Fin.castSucc k < Fin.succ i → c i = 0) →
      ∀ {M N : Matrix (Fin (Nat.succ n)) (Fin (Nat.succ n)) R},
        (∀ (j : Fin (Nat.succ n)), M 0 j = N 0 j) →
          (∀ (i : Fin n) (j : Fin (Nat.succ n)), M (Fin.succ i) j = N (Fin.succ i) j + c i * M (↑Fin.castSucc i) j) →
            det M = det N
c : Fin n → R
hc : ∀ (i : Fin n), Fin.succ k < Fin.succ i → c i = 0
M N : Matrix (Fin (Nat.succ n)) (Fin (Nat.succ n)) R
h0 : ∀ (j : Fin (Nat.succ n)), M 0 j = N 0 j
hsucc : ∀ (i : Fin n) (j : Fin (Nat.succ n)), M (Fin.succ i) j = N (Fin.succ i) j + c i * M (↑Fin.castSucc i) j
M' : Matrix (Fin (Nat.succ n)) (Fin (Nat.succ n)) R := updateRow M (Fin.succ k) (N (Fin.succ k))
hM' : M' = updateRow M (Fin.succ k) (N (Fin.succ k))
hM : M = updateRow M' (Fin.succ k) (M' (Fin.succ k) + c k • M (↑Fin.castSucc k))
k_ne_succ : ↑Fin.castSucc k ≠ Fin.succ k
M_k : M (↑Fin.castSucc k) = M' (↑Fin.castSucc k)
i : Fin n
hi : ↑k ≤ ↑i
hik : ¬i = k
⊢ c i = 0
case refine'_2._hc
m : Type ?u.1709668
n✝ : Type ?u.1709671
inst✝⁴ : DecidableEq n✝
inst✝³ : Fintype n✝
inst✝² : DecidableEq m
inst✝¹ : Fintype m
R : Type v
inst✝ : CommRing R
n : ℕ
k✝ : Fin (n + 1)
k : Fin n
ih :
  ∀ (c : Fin n → R),
    (∀ (i : Fin n), ↑Fin.castSucc k < Fin.succ i → c i = 0) →
      ∀ {M N : Matrix (Fin (Nat.succ n)) (Fin (Nat.succ n)) R},
        (∀ (j : Fin (Nat.succ n)), M 0 j = N 0 j) →
          (∀ (i : Fin n) (j : Fin (Nat.succ n)), M (Fin.succ i) j = N (Fin.succ i) j + c i * M (↑Fin.castSucc i) j) →
            det M = det N
c : Fin n → R
hc : ∀ (i : Fin n), Fin.succ k < Fin.succ i → c i = 0
M N : Matrix (Fin (Nat.succ n)) (Fin (Nat.succ n)) R
h0 : ∀ (j : Fin (Nat.succ n)), M 0 j = N 0 j
hsucc : ∀ (i : Fin n) (j : Fin (Nat.succ n)), M (Fin.succ i) j = N (Fin.succ i) j + c i * M (↑Fin.castSucc i) j
M' : Matrix (Fin (Nat.succ n)) (Fin (Nat.succ n)) R := updateRow M (Fin.succ k) (N (Fin.succ k))
hM' : M' = updateRow M (Fin.succ k) (N (Fin.succ k))
hM : M = updateRow M' (Fin.succ k) (M' (Fin.succ k) + c k • M (↑Fin.castSucc k))
k_ne_succ : ↑Fin.castSucc k ≠ Fin.succ k
M_k : M (↑Fin.castSucc k) = M' (↑Fin.castSucc k)
i : Fin n
hi : ↑k ≤ ↑i
⊢ (if i = k then 0 else c i) = 0
split_ifs with hik
no goals
case refine'_2._hc.inr
m : Type ?u.1709668
n✝ : Type ?u.1709671
inst✝⁴ : DecidableEq n✝
inst✝³ : Fintype n✝
inst✝² : DecidableEq m
inst✝¹ : Fintype m
R : Type v
inst✝ : CommRing R
n : ℕ
k✝ : Fin (n + 1)
k : Fin n
ih :
  ∀ (c : Fin n → R),
    (∀ (i : Fin n), ↑Fin.castSucc k < Fin.succ i → c i = 0) →
      ∀ {M N : Matrix (Fin (Nat.succ n)) (Fin (Nat.succ n)) R},
        (∀ (j : Fin (Nat.succ n)), M 0 j = N 0 j) →
          (∀ (i : Fin n) (j : Fin (Nat.succ n)), M (Fin.succ i) j = N (Fin.succ i) j + c i * M (↑Fin.castSucc i) j) →
            det M = det N
c : Fin n → R
hc : ∀ (i : Fin n), Fin.succ k < Fin.succ i → c i = 0
M N : Matrix (Fin (Nat.succ n)) (Fin (Nat.succ n)) R
h0 : ∀ (j : Fin (Nat.succ n)), M 0 j = N 0 j
hsucc : ∀ (i : Fin n) (j : Fin (Nat.succ n)), M (Fin.succ i) j = N (Fin.succ i) j + c i * M (↑Fin.castSucc i) j
M' : Matrix (Fin (Nat.succ n)) (Fin (Nat.succ n)) R := updateRow M (Fin.succ k) (N (Fin.succ k))
hM' : M' = updateRow M (Fin.succ k) (N (Fin.succ k))
hM : M = updateRow M' (Fin.succ k) (M' (Fin.succ k) + c k • M (↑Fin.castSucc k))
k_ne_succ : ↑Fin.castSucc k ≠ Fin.succ k
M_k : M (↑Fin.castSucc k) = M' (↑Fin.castSucc k)
i : Fin n
hi : ↑k ≤ ↑i
hik : ¬i = k
⊢ c i = 0
exact hc _ (Fin.succ_lt_succ_iff.mpr (lt_of_le_of_ne hi (Ne.symm hik)))
no goals
case refine'_2._hc.inl
m : Type ?u.1709668
n✝ : Type ?u.1709671
inst✝⁴ : DecidableEq n✝
inst✝³ : Fintype n✝
inst✝² : DecidableEq m
inst✝¹ : Fintype m
R : Type v
inst✝ : CommRing R
n : ℕ
k✝ : Fin (n + 1)
k : Fin n
ih :
  ∀ (c : Fin n → R),
    (∀ (i : Fin n), ↑Fin.castSucc k < Fin.succ i → c i = 0) →
      ∀ {M N : Matrix (Fin (Nat.succ n)) (Fin (Nat.succ n)) R},
        (∀ (j : Fin (Nat.succ n)), M 0 j = N 0 j) →
          (∀ (i : Fin n) (j : Fin (Nat.succ n)), M (Fin.succ i) j = N (Fin.succ i) j + c i * M (↑Fin.castSucc i) j) →
            det M = det N
c : Fin n → R
hc : ∀ (i : Fin n), Fin.succ k < Fin.succ i → c i = 0
M N : Matrix (Fin (Nat.succ n)) (Fin (Nat.succ n)) R
h0 : ∀ (j : Fin (Nat.succ n)), M 0 j = N 0 j
hsucc : ∀ (i : Fin n) (j : Fin (Nat.succ n)), M (Fin.succ i) j = N (Fin.succ i) j + c i * M (↑Fin.castSucc i) j
M' : Matrix (Fin (Nat.succ n)) (Fin (Nat.succ n)) R := updateRow M (Fin.succ k) (N (Fin.succ k))
hM' : M' = updateRow M (Fin.succ k) (N (Fin.succ k))
hM : M = updateRow M' (Fin.succ k) (M' (Fin.succ k) + c k • M (↑Fin.castSucc k))
k_ne_succ : ↑Fin.castSucc k ≠ Fin.succ k
M_k : M (↑Fin.castSucc k) = M' (↑Fin.castSucc k)
i : Fin n
hi : ↑k ≤ ↑i
hik : i = k
⊢ 0 = 0
rfl
no goals
case refine'_2._h0
m : Type ?u.1709668
n✝ : Type ?u.1709671
inst✝⁴ : DecidableEq n✝
inst✝³ : Fintype n✝
inst✝² : DecidableEq m
inst✝¹ : Fintype m
R : Type v
inst✝ : CommRing R
n : ℕ
k✝ : Fin (n + 1)
k : Fin n
ih :
  ∀ (c : Fin n → R),
    (∀ (i : Fin n), ↑Fin.castSucc k < Fin.succ i → c i = 0) →
      ∀ {M N : Matrix (Fin (Nat.succ n)) (Fin (Nat.succ n)) R},
        (∀ (j : Fin (Nat.succ n)), M 0 j = N 0 j) →
          (∀ (i : Fin n) (j : Fin (Nat.succ n)), M (Fin.succ i) j = N (Fin.succ i) j + c i * M (↑Fin.castSucc i) j) →
            det M = det N
c : Fin n → R
hc : ∀ (i : Fin n), Fin.succ k < Fin.succ i → c i = 0
M N : Matrix (Fin (Nat.succ n)) (Fin (Nat.succ n)) R
h0 : ∀ (j : Fin (Nat.succ n)), M 0 j = N 0 j
hsucc : ∀ (i : Fin n) (j : Fin (Nat.succ n)), M (Fin.succ i) j = N (Fin.succ i) j + c i * M (↑Fin.castSucc i) j
M' : Matrix (Fin (Nat.succ n)) (Fin (Nat.succ n)) R := updateRow M (Fin.succ k) (N (Fin.succ k))
hM' : M' = updateRow M (Fin.succ k) (N (Fin.succ k))
hM : M = updateRow M' (Fin.succ k) (M' (Fin.succ k) + c k • M (↑Fin.castSucc k))
k_ne_succ : ↑Fin.castSucc k ≠ Fin.succ k
M_k : M (↑Fin.castSucc k) = M' (↑Fin.castSucc k)
⊢ ∀ (j : Fin (Nat.succ n)), M' 0 j = N 0 j
rwa [hM', updateRow_ne (Fin.succ_ne_zero _).symm]
no goals
case refine'_2._hsucc.inl
m : Type ?u.1709668
n✝ : Type ?u.1709671
inst✝⁴ : DecidableEq n✝
inst✝³ : Fintype n✝
inst✝² : DecidableEq m
inst✝¹ : Fintype m
R : Type v
inst✝ : CommRing R
n : ℕ
k✝ : Fin (n + 1)
k : Fin n
ih :
  ∀ (c : Fin n → R),
    (∀ (i : Fin n), ↑Fin.castSucc k < Fin.succ i → c i = 0) →
      ∀ {M N : Matrix (Fin (Nat.succ n)) (Fin (Nat.succ n)) R},
        (∀ (j : Fin (Nat.succ n)), M 0 j = N 0 j) →
          (∀ (i : Fin n) (j : Fin (Nat.succ n)), M (Fin.succ i) j = N (Fin.succ i) j + c i * M (↑Fin.castSucc i) j) →
            det M = det N
c : Fin n → R
hc : ∀ (i : Fin n), Fin.succ k < Fin.succ i → c i = 0
M N : Matrix (Fin (Nat.succ n)) (Fin (Nat.succ n)) R
h0 : ∀ (j : Fin (Nat.succ n)), M 0 j = N 0 j
hsucc : ∀ (i : Fin n) (j : Fin (Nat.succ n)), M (Fin.succ i) j = N (Fin.succ i) j + c i * M (↑Fin.castSucc i) j
M' : Matrix (Fin (Nat.succ n)) (Fin (Nat.succ n)) R := updateRow M (Fin.succ k) (N (Fin.succ k))
hM' : M' = updateRow M (Fin.succ k) (N (Fin.succ k))
hM : M = updateRow M' (Fin.succ k) (M' (Fin.succ k) + c k • M (↑Fin.castSucc k))
k_ne_succ : ↑Fin.castSucc k ≠ Fin.succ k
M_k : M (↑Fin.castSucc k) = M' (↑Fin.castSucc k)
i : Fin n
j : Fin (Nat.succ n)
hik : i = k
⊢ M' (Fin.succ i) j = N (Fin.succ i) j + 0 * M' (↑Fin.castSucc i) j
rw [MulZeroClass.zero_mul, add_zero, hM', hik, updateRow_self]
no goals
case pos
m : Type ?u.1709668
n✝ : Type ?u.1709671
inst✝⁴ : DecidableEq n✝
inst✝³ : Fintype n✝
inst✝² : DecidableEq m
inst✝¹ : Fintype m
R : Type v
inst✝ : CommRing R
n : ℕ
k✝ : Fin (n + 1)
k : Fin n
ih :
  ∀ (c : Fin n → R),
    (∀ (i : Fin n), ↑Fin.castSucc k < Fin.succ i → c i = 0) →
      ∀ {M N : Matrix (Fin (Nat.succ n)) (Fin (Nat.succ n)) R},
        (∀ (j : Fin (Nat.succ n)), M 0 j = N 0 j) →
          (∀ (i : Fin n) (j : Fin (Nat.succ n)), M (Fin.succ i) j = N (Fin.succ i) j + c i * M (↑Fin.castSucc i) j) →
            det M = det N
c : Fin n → R
hc : ∀ (i : Fin n), Fin.succ k < Fin.succ i → c i = 0
M N : Matrix (Fin (Nat.succ n)) (Fin (Nat.succ n)) R
h0 : ∀ (j : Fin (Nat.succ n)), M 0 j = N 0 j
hsucc : ∀ (i : Fin n) (j : Fin (Nat.succ n)), M (Fin.succ i) j = N (Fin.succ i) j + c i * M (↑Fin.castSucc i) j
M' : Matrix (Fin (Nat.succ n)) (Fin (Nat.succ n)) R := updateRow M (Fin.succ k) (N (Fin.succ k))
hM' : M' = updateRow M (Fin.succ k) (N (Fin.succ k))
hM : M = updateRow M' (Fin.succ k) (M' (Fin.succ k) + c k • M (↑Fin.castSucc k))
k_ne_succ : ↑Fin.castSucc k ≠ Fin.succ k
M_k : M (↑Fin.castSucc k) = M' (↑Fin.castSucc k)
i : Fin n
j : Fin (Nat.succ n)
hik : ¬i = k
hik2 : k < i
⊢ N (Fin.succ i) j + c i * M (↑Fin.castSucc i) j =
    N (Fin.succ i) j + c i * updateRow M (Fin.succ k) (N (Fin.succ k)) (↑Fin.castSucc i) j
simp [hc i (Fin.succ_lt_succ_iff.mpr hik2)]