m : Type u
n : Type v
α : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing α
A : Matrix n n α
b : n → α
β : Type u_1
s : Finset β
f : n → β → α
i : n
⊢ det (updateColumn A i (∑ x in s, fun j => f j x)) = det (updateColumn A i fun j => ∑ x in s, f j x)
m : Type u
n : Type v
α : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing α
A : Matrix n n α
b : n → α
β : Type u_1
s : Finset β
f : n → β → α
i : n
⊢ Finset.sum s (fun x => ↑(cramer A) fun j => f j x) i = ↑(cramer A) (fun j => ∑ x in s, f j x) i
rw [sum_cramer, cramer_apply, cramer_apply]
m : Type u
n : Type v
α : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing α
A : Matrix n n α
b : n → α
β : Type u_1
s : Finset β
f : n → β → α
i : n
⊢ det (↑of fun i_1 => Function.update (A i_1) i (Finset.sum s (fun x j => f j x) i_1)) =
    det (↑of fun i_1 => Function.update (A i_1) i (∑ x in s, f i_1 x))
m : Type u
n : Type v
α : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing α
A : Matrix n n α
b : n → α
β : Type u_1
s : Finset β
f : n → β → α
i : n
⊢ det (updateColumn A i (∑ x in s, fun j => f j x)) = det (updateColumn A i fun j => ∑ x in s, f j x)
simp only [updateColumn]
case e_M.h.e_6.h.h.h
m : Type u
n : Type v
α : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing α
A : Matrix n n α
b : n → α
β : Type u_1
s : Finset β
f : n → β → α
i j x✝ : n
⊢ Function.update (A j) i (Finset.sum s (fun x j => f j x) j) x✝ = Function.update (A j) i (∑ x in s, f j x) x✝
m : Type u
n : Type v
α : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing α
A : Matrix n n α
b : n → α
β : Type u_1
s : Finset β
f : n → β → α
i : n
⊢ det (↑of fun i_1 => Function.update (A i_1) i (Finset.sum s (fun x j => f j x) i_1)) =
    det (↑of fun i_1 => Function.update (A i_1) i (∑ x in s, f i_1 x))
congr with j
case e_M.h.e_6.h.h.h.e_v
m : Type u
n : Type v
α : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing α
A : Matrix n n α
b : n → α
β : Type u_1
s : Finset β
f : n → β → α
i j x✝ : n
⊢ Finset.sum s (fun x j => f j x) j = ∑ x in s, f j x
case e_M.h.e_6.h.h.h
m : Type u
n : Type v
α : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing α
A : Matrix n n α
b : n → α
β : Type u_1
s : Finset β
f : n → β → α
i j x✝ : n
⊢ Function.update (A j) i (Finset.sum s (fun x j => f j x) j) x✝ = Function.update (A j) i (∑ x in s, f j x) x✝
congr
no goals
case e_M.h.e_6.h.h.h.e_v
m : Type u
n : Type v
α : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing α
A : Matrix n n α
b : n → α
β : Type u_1
s : Finset β
f : n → β → α
i j x✝ : n
⊢ Finset.sum s (fun x j => f j x) j = ∑ x in s, f j x
apply Finset.sum_apply