-- Mathlib/LinearAlgebra/Matrix/Adjugate.lean
theorem cramer_eq_adjugate_mulVec (A : Matrix n n α) (b : n → α) :
    cramer A b = A.adjugate *ᵥ b

Proof state:
case e_f.h.h
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
b : n → α
j x✝ : n
⊢ (b j • fun j_1 => if j = j_1 then 1 else 0) x✝ = (b j • Pi.single j 1) x✝

Tactic:
simp [Pi.single_apply, eq_comm, Pi.smul_apply (b j)]

Result:
no goals

Proof state:
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
b : n → α
⊢ A.cramer b = Aᵀᵀ.adjugate *ᵥ b

Tactic:
rw [← adjugate_transpose, adjugate_def]

Result:
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
b : n → α
⊢ A.cramer b = (of fun i => Aᵀᵀ.cramer (Pi.single i 1))ᵀ *ᵥ b

Proof state:
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
b : n → α
this : b = ∑ i : n, b i • Pi.single i 1
⊢ A.cramer (∑ i : n, b i • Pi.single i 1) = (of fun i => Aᵀᵀ.cramer (Pi.single i 1))ᵀ *ᵥ b

Tactic:
ext k

Result:
case h
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
b : n → α
this : b = ∑ i : n, b i • Pi.single i 1
k : n
⊢ A.cramer (∑ i : n, b i • Pi.single i 1) k = ((of fun i => Aᵀᵀ.cramer (Pi.single i 1))ᵀ *ᵥ b) k

Proof state:
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
b : n → α
⊢ A.cramer b = A.adjugate *ᵥ b

Tactic:
nth_rw 2 [← A.transpose_transpose]

Result:
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
b : n → α
⊢ A.cramer b = Aᵀᵀ.adjugate *ᵥ b

Proof state:
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
b : n → α
this : b = ∑ i : n, b i • Pi.single i 1
⊢ A.cramer b = (of fun i => Aᵀᵀ.cramer (Pi.single i 1))ᵀ *ᵥ b

Tactic:
conv_lhs =>
  rw [this]

Result:
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
b : n → α
this : b = ∑ i : n, b i • Pi.single i 1
⊢ A.cramer (∑ i : n, b i • Pi.single i 1) = (of fun i => Aᵀᵀ.cramer (Pi.single i 1))ᵀ *ᵥ b

Proof state:
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
b : n → α
⊢ b = ∑ i : n, b i • Pi.single i 1

Tactic:
refine (pi_eq_sum_univ b).trans ?_

Result:
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
b : n → α
⊢ (∑ i : n, b i • fun j => if i = j then 1 else 0) = ∑ i : n, b i • Pi.single i 1

Proof state:
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
b : n → α
⊢ (∑ i : n, b i • fun j => if i = j then 1 else 0) = ∑ i : n, b i • Pi.single i 1

Tactic:
congr with j

Result:
case e_f.h.h
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
b : n → α
j x✝ : n
⊢ (b j • fun j_1 => if j = j_1 then 1 else 0) x✝ = (b j • Pi.single j 1) x✝

Proof state:
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
b : n → α
⊢ A.cramer b = (of fun i => Aᵀᵀ.cramer (Pi.single i 1))ᵀ *ᵥ b

Tactic:
have : b = ∑ i, b i • (Pi.single i 1 : n → α) := by
  refine (pi_eq_sum_univ b).trans ?_
  congr with j
  simp [Pi.single_apply, eq_comm, Pi.smul_apply (b j)]

Result:
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
b : n → α
this : b = ∑ i : n, b i • Pi.single i 1
⊢ A.cramer b = (of fun i => Aᵀᵀ.cramer (Pi.single i 1))ᵀ *ᵥ b

Proof state:
case h
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
b : n → α
this : b = ∑ i : n, b i • Pi.single i 1
k : n
⊢ A.cramer (∑ i : n, b i • Pi.single i 1) k = ((of fun i => Aᵀᵀ.cramer (Pi.single i 1))ᵀ *ᵥ b) k

Tactic:
simp [mulVec, dotProduct, mul_comm]

Result:
no goals