-- Mathlib/LinearAlgebra/Matrix/Adjugate.lean
theorem adjugate_diagonal (v : n → α) :
    adjugate (diagonal v) = diagonal fun i => ∏ j ∈ Finset.univ.erase i, v j

Proof state:
case a.inr
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
v : n → α
i j : n
hij : i ≠ j
⊢ ((diagonal v).updateCol j (Pi.single i 1)).det = diagonal (fun i => ∏ j ∈ univ.erase i, v j) i j

Tactic:
rw [diagonal_apply_ne _ hij]

Result:
case a.inr
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
v : n → α
i j : n
hij : i ≠ j
⊢ ((diagonal v).updateCol j (Pi.single i 1)).det = 0

Proof state:
case a.inr
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
v : n → α
i j : n
hij : i ≠ j
k : n
⊢ (diagonal v).updateCol j (Pi.single i 1) j k = 0

Tactic:
obtain rfl | hjk := eq_or_ne k j

Result:
case a.inr.inl
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
v : n → α
i k : n
hij : i ≠ k
⊢ (diagonal v).updateCol k (Pi.single i 1) k k = 0

case a.inr.inr
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
v : n → α
i j : n
hij : i ≠ j
k : n
hjk : k ≠ j
⊢ (diagonal v).updateCol j (Pi.single i 1) j k = 0

Proof state:
case a.inr
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
v : n → α
i j : n
hij : i ≠ j
⊢ ((diagonal v).updateCol j (Pi.single i 1)).det = 0

Tactic:
refine det_eq_zero_of_row_eq_zero j fun k => ?_

Result:
case a.inr
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
v : n → α
i j : n
hij : i ≠ j
k : n
⊢ (diagonal v).updateCol j (Pi.single i 1) j k = 0

Proof state:
case a
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
v : n → α
i j : n
⊢ ((diagonal v).updateCol j (Pi.single i 1)).det = diagonal (fun i => ∏ j ∈ univ.erase i, v j) i j

Tactic:
obtain rfl | hij := eq_or_ne i j

Result:
case a.inl
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
v : n → α
i : n
⊢ ((diagonal v).updateCol i (Pi.single i 1)).det = diagonal (fun i => ∏ j ∈ univ.erase i, v j) i i

case a.inr
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
v : n → α
i j : n
hij : i ≠ j
⊢ ((diagonal v).updateCol j (Pi.single i 1)).det = diagonal (fun i => ∏ j ∈ univ.erase i, v j) i j

Proof state:
case a
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
v : n → α
i j : n
⊢ (diagonal v).adjugate i j = diagonal (fun i => ∏ j ∈ univ.erase i, v j) i j

Tactic:
simp only [adjugate_def, cramer_apply, diagonal_transpose, of_apply]

Result:
case a
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
v : n → α
i j : n
⊢ ((diagonal v).updateCol j (Pi.single i 1)).det = diagonal (fun i => ∏ j ∈ univ.erase i, v j) i j

Proof state:
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
v : n → α
⊢ (diagonal v).adjugate = diagonal fun i => ∏ j ∈ univ.erase i, v j

Tactic:
ext i j

Result:
case a
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
v : n → α
i j : n
⊢ (diagonal v).adjugate i j = diagonal (fun i => ∏ j ∈ univ.erase i, v j) i j

Proof state:
case a.inl
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
v : n → α
i : n
⊢ ((diagonal v).updateCol i (Pi.single i 1)).det = diagonal (fun i => ∏ j ∈ univ.erase i, v j) i i

Tactic:
rw [diagonal_apply_eq, diagonal_updateCol_single, det_diagonal,
  prod_update_of_mem (Finset.mem_univ _), sdiff_singleton_eq_erase, one_mul]

Result:
no goals

Proof state:
case a.inr.inr
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
v : n → α
i j : n
hij : i ≠ j
k : n
hjk : k ≠ j
⊢ (diagonal v).updateCol j (Pi.single i 1) j k = 0

Tactic:
rw [updateCol_ne hjk, diagonal_apply_ne' _ hjk]

Result:
no goals

Proof state:
case a.inr.inl
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
v : n → α
i k : n
hij : i ≠ k
⊢ (diagonal v).updateCol k (Pi.single i 1) k k = 0

Tactic:
rw [updateCol_self, Pi.single_eq_of_ne' hij]

Result:
no goals