case a.h
m : Type u
n : Type v
α : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing α
v : n → α
i j : n
⊢ adjugate (diagonal v) i j = diagonal (fun i => ∏ j in Finset.erase univ i, v j) i j
m : Type u
n : Type v
α : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing α
v : n → α
⊢ adjugate (diagonal v) = diagonal fun i => ∏ j in Finset.erase univ i, v j
ext i j
case a.h
m : Type u
n : Type v
α : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing α
v : n → α
i j : n
⊢ det (updateColumn (diagonal v) j (Pi.single i 1)) = diagonal (fun i => ∏ j in Finset.erase univ i, v j) i j
case a.h
m : Type u
n : Type v
α : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing α
v : n → α
i j : n
⊢ adjugate (diagonal v) i j = diagonal (fun i => ∏ j in Finset.erase univ i, v j) i j
simp only [adjugate_def, cramer_apply, diagonal_transpose, of_apply]
case a.h.inl
m : Type u
n : Type v
α : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing α
v : n → α
i : n
⊢ det (updateColumn (diagonal v) i (Pi.single i 1)) = diagonal (fun i => ∏ j in Finset.erase univ i, v j) i i

case a.h.inr
m : Type u
n : Type v
α : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing α
v : n → α
i j : n
hij : i ≠ j
⊢ det (updateColumn (diagonal v) j (Pi.single i 1)) = diagonal (fun i => ∏ j in Finset.erase univ i, v j) i j
case a.h
m : Type u
n : Type v
α : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing α
v : n → α
i j : n
⊢ det (updateColumn (diagonal v) j (Pi.single i 1)) = diagonal (fun i => ∏ j in Finset.erase univ i, v j) i j
obtain rfl | hij := eq_or_ne i j
no goals
case a.h.inl
m : Type u
n : Type v
α : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing α
v : n → α
i : n
⊢ det (updateColumn (diagonal v) i (Pi.single i 1)) = diagonal (fun i => ∏ j in Finset.erase univ i, v j) i i
rw [diagonal_apply_eq, diagonal_updateColumn_single, det_diagonal,
  prod_update_of_mem (Finset.mem_univ _), sdiff_singleton_eq_erase, one_mul]
case a.h.inr
m : Type u
n : Type v
α : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing α
v : n → α
i j : n
hij : i ≠ j
⊢ det (updateColumn (diagonal v) j (Pi.single i 1)) = 0
case a.h.inr
m : Type u
n : Type v
α : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing α
v : n → α
i j : n
hij : i ≠ j
⊢ det (updateColumn (diagonal v) j (Pi.single i 1)) = diagonal (fun i => ∏ j in Finset.erase univ i, v j) i j
rw [diagonal_apply_ne _ hij]
case a.h.inr
m : Type u
n : Type v
α : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing α
v : n → α
i j : n
hij : i ≠ j
k : n
⊢ updateColumn (diagonal v) j (Pi.single i 1) j k = 0
case a.h.inr
m : Type u
n : Type v
α : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing α
v : n → α
i j : n
hij : i ≠ j
⊢ det (updateColumn (diagonal v) j (Pi.single i 1)) = 0
refine' det_eq_zero_of_row_eq_zero j fun k => _
case a.h.inr.inl
m : Type u
n : Type v
α : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing α
v : n → α
i k : n
hij : i ≠ k
⊢ updateColumn (diagonal v) k (Pi.single i 1) k k = 0

case a.h.inr.inr
m : Type u
n : Type v
α : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing α
v : n → α
i j : n
hij : i ≠ j
k : n
hjk : k ≠ j
⊢ updateColumn (diagonal v) j (Pi.single i 1) j k = 0
case a.h.inr
m : Type u
n : Type v
α : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing α
v : n → α
i j : n
hij : i ≠ j
k : n
⊢ updateColumn (diagonal v) j (Pi.single i 1) j k = 0
obtain rfl | hjk := eq_or_ne k j
no goals
case a.h.inr.inl
m : Type u
n : Type v
α : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing α
v : n → α
i k : n
hij : i ≠ k
⊢ updateColumn (diagonal v) k (Pi.single i 1) k k = 0
rw [updateColumn_self, Pi.single_eq_of_ne' hij]
no goals
case a.h.inr.inr
m : Type u
n : Type v
α : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing α
v : n → α
i j : n
hij : i ≠ j
k : n
hjk : k ≠ j
⊢ updateColumn (diagonal v) j (Pi.single i 1) j k = 0
rw [updateColumn_ne hjk, diagonal_apply_ne' _ hjk]