awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Matrix.Adjugate
Goal:
m : Type u
n : Type v
α : Type w
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : DecidableEq m
inst_3 : Fintype m
inst_4 : CommRing α
e : n ≃ m
A : Matrix m m α
i j : n
⊢ Eq (α := (j : m) → α) (fun (j : m) ↦ (Pi.single (M := fun (a : n) ↦ α) i 1 ((e.symm : (a : m) → n) j) : α))
    (Pi.single (M := fun (j : m) ↦ α) ((e : (a : n) → m) i) 1 : (j : m) → α)

Tactic:
have : (fun j ↦ Pi.single i 1 <| e.symm j) = Pi.single (e i) 1 :=
    Function.update_comp_equiv (0 : n → α) e.symm i 1
-- Module: Mathlib.LinearAlgebra.Matrix.Adjugate
Goal:
m : Type u
n : Type v
α : Type w
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : DecidableEq m
inst_3 : Fintype m
inst_4 : CommRing α
e : n ≃ m
A : Matrix m m α
i j : n
this :
  Eq (α := (j : m) → α) (fun (j : m) ↦ (Pi.single (M := fun (a : n) ↦ α) i 1 ((e.symm : (a : m) → n) j) : α))
    (Pi.single (M := fun (j : m) ↦ α) ((e : (a : n) → m) i) 1 : (j : m) → α)
a :
  (updateRow (A.submatrix (⇑e : (a : n) → m) (⇑e : (a : n) → m)) j (Pi.single (M := fun (a : n) ↦ α) i 1)).det =
    A.adjugate.submatrix (⇑e : (a : n) → m) (⇑e : (a : n) → m) i j
a₁ :
  (updateRow (A.submatrix (⇑e : (a : n) → m) (⇑e : (a : n) → m)) j (Pi.single (M := fun (a : n) ↦ α) i 1)).det =
    A.adjugate ((e : (a : n) → m) i) ((e : (a : n) → m) j)
a₂ :
  (updateRow (A.submatrix (⇑e : (a : n) → m) (⇑e : (a : n) → m)) j (Pi.single (M := fun (a : n) ↦ α) i 1)).det =
    (A.updateRow ((e : (a : n) → m) j) (Pi.single (M := fun (a : m) ↦ α) ((e : (a : n) → m) i) 1)).det
a₃ :
  (updateRow (A.submatrix (⇑e : (a : n) → m) (⇑e : (a : n) → m)) j (Pi.single (M := fun (a : n) ↦ α) i 1)).det =
    det.{w, v} (n := n)
      ((A.updateRow ((e : (a : n) → m) j) (Pi.single (M := fun (a : m) ↦ α) ((e : (a : n) → m) i) 1)).submatrix
        (⇑e : (a : n) → m) (⇑e : (a : n) → m))
a₄ :
  det.{w, v} (n := n)
      ((A.updateRow ((e : (a : n) → m) j) fun (j : m) ↦
            Pi.single (M := fun (a : n) ↦ α) i 1 ((e.symm : (a : m) → n) j)).submatrix
        (⇑e : (a : n) → m) (⇑e : (a : n) → m)) =
    det.{w, v} (n := n)
      ((A.updateRow ((e : (a : n) → m) j) (Pi.single (M := fun (a : m) ↦ α) ((e : (a : n) → m) i) 1)).submatrix
        (⇑e : (a : n) → m) (⇑e : (a : n) → m))
a₅ a₆ :
  det.{w, v} (n := n)
      ((A.updateRow ((e : (a : n) → m) j) (Pi.single (M := fun (j : m) ↦ α) ((e : (a : n) → m) i) 1)).submatrix
        (⇑e : (a : n) → m) (⇑e : (a : n) → m)) =
    det.{w, v} (n := n)
      ((A.updateRow ((e : (a : n) → m) j) (Pi.single (M := fun (a : m) ↦ α) ((e : (a : n) → m) i) 1)).submatrix
        (⇑e : (a : n) → m) (⇑e : (a : n) → m))
⊢ adjugate (A.submatrix (⇑e : (a : n) → m) (⇑e : (a : n) → m)) i j =
    A.adjugate.submatrix (⇑e : (a : n) → m) (⇑e : (a : n) → m) i j

Tactic:
rw [adjugate_apply, submatrix_apply, adjugate_apply, ← det_submatrix_equiv_self e,
    updateRow_submatrix_equiv, this]

Premises used: Matrix.updateRow_submatrix_equiv, Matrix.adjugate_apply, Matrix.submatrix_apply, Matrix.det_submatrix_equiv_self
-- Module: Mathlib.LinearAlgebra.Matrix.Adjugate
Goal:
m : Type u
n : Type v
α : Type w
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : DecidableEq m
inst_3 : Fintype m
inst_4 : CommRing α
e : m ≃ n
A : Matrix m m α
⊢ Eq (α := Matrix n n α) (adjugate ((reindex e e : (a : Matrix m m α) → Matrix n n α) A))
    ((reindex e e : (a : Matrix m m α) → Matrix n n α) A.adjugate)

Tactic:
adjugate_submatrix_equiv_self _ _

Premises used: Matrix.submatrix, Matrix.cramerMap, Matrix.adjugate_submatrix_equiv_self, Matrix.adjugate, Matrix.det
-- Module: Mathlib.LinearAlgebra.Matrix.Adjugate
Goal:
n : Type v
α : Type w
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : CommRing α
A : Matrix n n α
b : n → α
nth_rw : (A.cramer : (a : n → α) → n → α) b = Aᵀᵀ.adjugate *ᵥ b
⊢ (A.cramer : (a : n → α) → n → α) b = A.adjugate *ᵥ b

Tactic:
nth_rw 2 [← A.transpose_transpose]

Premises used: Matrix.transpose_transpose
-- Module: Mathlib.LinearAlgebra.Matrix.Adjugate
Goal:
n : Type v
α : Type w
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : CommRing α
A : Matrix n n α
b : n → α
rw :
  Eq (α := n → α) ((A.cramer : (a : n → α) → n → α) b : n → α)
    (((of : (a : n → n → α) → Matrix n n α) fun (i : n) ↦
            (Aᵀᵀ.cramer : (a : n → α) → n → α) (Pi.single (M := fun (a : n) ↦ α) i 1))ᵀ *ᵥ
        b :
      n → α)
⊢ (A.cramer : (a : n → α) → n → α) b = Aᵀᵀ.adjugate *ᵥ b

Tactic:
rw [← adjugate_transpose, adjugate_def]

Premises used: Matrix.adjugate_def, Matrix.adjugate_transpose
-- Module: Mathlib.LinearAlgebra.Matrix.Adjugate
Goal:
n : Type v
α : Type w
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : CommRing α
A : Matrix n n α
b : n → α
⊢ b = ∑ i : n, HSMul.hSMul (β := (j : n) → α) (b i) (Pi.single (M := fun (a : n) ↦ α) i 1)

Tactic:
(pi_eq_sum_univ b).trans ?_

Premises used: pi_eq_sum_univ, Eq.trans
-- Module: Mathlib.LinearAlgebra.Matrix.Adjugate
Goal:
n : Type v
α : Type w
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : CommRing α
A : Matrix n n α
b : n → α
refine :
  Eq (α := n → α) (∑ i : n, HSMul.hSMul (β := (j : n) → α) (b i) fun (j : n) ↦ if i = j then 1 else 0)
    (∑ i : n, HSMul.hSMul (β := (j : n) → α) (b i) (Pi.single (M := fun (a : n) ↦ α) i 1))
⊢ b = ∑ i : n, HSMul.hSMul (β := (j : n) → α) (b i) (Pi.single (M := fun (a : n) ↦ α) i 1)

Tactic:
refine (pi_eq_sum_univ b).trans ?_

Premises used: pi_eq_sum_univ, Eq.trans
-- Module: Mathlib.LinearAlgebra.Matrix.Adjugate
Goal:
n : Type v
α : Type w
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : CommRing α
A : Matrix n n α
b : n → α
e_f :
  ∀ (j x : n),
    HSMul.hSMul (β := (j : n) → α) (b j) (fun (j_1 : n) ↦ if j = j_1 then 1 else 0) x =
      HSMul.hSMul (β := (j : n) → α) (b j) (Pi.single (M := fun (a : n) ↦ α) j 1) x
⊢ Eq (α := n → α) (∑ i : n, HSMul.hSMul (β := (j : n) → α) (b i) fun (j : n) ↦ if i = j then 1 else 0)
    (∑ i : n, HSMul.hSMul (β := (j : n) → α) (b i) (Pi.single (M := fun (a : n) ↦ α) i 1))

Tactic:
congr with j
-- Module: Mathlib.LinearAlgebra.Matrix.Adjugate
Goal:
n : Type v
α : Type w
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : CommRing α
A : Matrix n n α
b : n → α
j x : n
⊢ HSMul.hSMul (β := (j : n) → α) (b j) (fun (j_1 : n) ↦ if j = j_1 then 1 else 0) x =
    HSMul.hSMul (β := (j : n) → α) (b j) (Pi.single (M := fun (a : n) ↦ α) j 1) x

Tactic:
simp [Pi.single_apply, eq_comm]

Premises used: Pi.single_apply, eq_comm
-- Module: Mathlib.LinearAlgebra.Matrix.Adjugate
Goal:
n : Type v
α : Type w
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : CommRing α
A : Matrix n n α
b : n → α
⊢ b = ∑ i : n, HSMul.hSMul (β := (j : n) → α) (b i) (Pi.single (M := fun (a : n) ↦ α) i 1)

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]
-- Module: Mathlib.LinearAlgebra.Matrix.Adjugate
Goal:
n : Type v
α : Type w
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : CommRing α
A : Matrix n n α
b : n → α
this : b = ∑ i : n, HSMul.hSMul (β := (j : n) → α) (b i) (Pi.single (M := fun (a : n) ↦ α) i 1)
rw :
  ((A.cramer : (a : n → α) → n → α)
      (∑ i : n, HSMul.hSMul (β := (j : n) → α) (b i) (Pi.single (M := fun (a : n) ↦ α) i 1)) :
    n → α)
| ((A.cramer : (a : n → α) → n → α) b : n → α)

Tactic:
rw [this]
-- Module: Mathlib.LinearAlgebra.Matrix.Adjugate
Goal:
n : Type v
α : Type w
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : CommRing α
A : Matrix n n α
b : n → α
this : b = ∑ i : n, HSMul.hSMul (β := (j : n) → α) (b i) (Pi.single (M := fun (a : n) ↦ α) i 1)
conv_lhs :
  Eq (α := n → α)
    ((A.cramer : (a : n → α) → n → α)
        (∑ i : n, HSMul.hSMul (β := (j : n) → α) (b i) (Pi.single (M := fun (a : n) ↦ α) i 1)) :
      n → α)
    (((of : (a : n → n → α) → Matrix n n α) fun (i : n) ↦
            (Aᵀᵀ.cramer : (a : n → α) → n → α) (Pi.single (M := fun (a : n) ↦ α) i 1))ᵀ *ᵥ
        b :
      n → α)
⊢ Eq (α := n → α) ((A.cramer : (a : n → α) → n → α) b : n → α)
    (((of : (a : n → n → α) → Matrix n n α) fun (i : n) ↦
            (Aᵀᵀ.cramer : (a : n → α) → n → α) (Pi.single (M := fun (a : n) ↦ α) i 1))ᵀ *ᵥ
        b :
      n → α)

Tactic:
conv_lhs =>
    rw [this]
-- Module: Mathlib.LinearAlgebra.Matrix.Adjugate
Goal:
n : Type v
α : Type w
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : CommRing α
A : Matrix n n α
b : n → α
this : b = ∑ i : n, HSMul.hSMul (β := (j : n) → α) (b i) (Pi.single (M := fun (a : n) ↦ α) i 1)
h :
  ∀ (k : n),
    (A.cramer : (a : n → α) → n → α)
        (∑ i : n, HSMul.hSMul (β := (j : n) → α) (b i) (Pi.single (M := fun (a : n) ↦ α) i 1)) k =
      (((of : (a : n → n → α) → Matrix n n α) fun (i : n) ↦
              (Aᵀᵀ.cramer : (a : n → α) → n → α) (Pi.single (M := fun (a : n) ↦ α) i 1))ᵀ *ᵥ
          b)
        k
⊢ Eq (α := n → α)
    ((A.cramer : (a : n → α) → n → α)
        (∑ i : n, HSMul.hSMul (β := (j : n) → α) (b i) (Pi.single (M := fun (a : n) ↦ α) i 1)) :
      n → α)
    (((of : (a : n → n → α) → Matrix n n α) fun (i : n) ↦
            (Aᵀᵀ.cramer : (a : n → α) → n → α) (Pi.single (M := fun (a : n) ↦ α) i 1))ᵀ *ᵥ
        b :
      n → α)

Tactic:
ext k
-- Module: Mathlib.LinearAlgebra.Matrix.Adjugate
Goal:
n : Type v
α : Type w
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : CommRing α
A : Matrix n n α
b : n → α
this : b = ∑ i : n, HSMul.hSMul (β := (j : n) → α) (b i) (Pi.single (M := fun (a : n) ↦ α) i 1)
k : n
⊢ (A.cramer : (a : n → α) → n → α)
      (∑ i : n, HSMul.hSMul (β := (j : n) → α) (b i) (Pi.single (M := fun (a : n) ↦ α) i 1)) k =
    (((of : (a : n → n → α) → Matrix n n α) fun (i : n) ↦
            (Aᵀᵀ.cramer : (a : n → α) → n → α) (Pi.single (M := fun (a : n) ↦ α) i 1))ᵀ *ᵥ
        b)
      k

Tactic:
simp [mulVec, dotProduct, mul_comm]

Premises used: dotProduct, mul_comm, Matrix.mulVec
-- Module: Mathlib.LinearAlgebra.Matrix.Adjugate
Goal:
n : Type v
α : Type w
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : CommRing α
A : Matrix n n α
i j k : n
rw : A i k • A.adjugate k j = (Aᵀ.cramer : (a : n → α) → n → α) (Pi.single (M := fun (a : n) ↦ α) k (A i k)) j
rw₁ :
  HSMul.hSMul (β := α) (A i k)
      ((of : (a : n → n → α) → Matrix n n α)
          (fun (i : n) ↦ (Aᵀ.cramer : (a : n → α) → n → α) (Pi.single (M := fun (a : n) ↦ α) i 1)) k j :
        α) =
    (Aᵀ.cramer : (a : n → α) → n → α) (Pi.single (M := fun (a : n) ↦ α) k (A i k)) j
rw₂ :
  HSMul.hSMul (β := α) (A i k) ((Aᵀ.cramer : (a : n → α) → n → α) (Pi.single (M := fun (a : n) ↦ α) k 1) j : α) =
    (Aᵀ.cramer : (a : n → α) → n → α) (Pi.single (M := fun (a : n) ↦ α) k (A i k)) j
rw₃ :
  HSMul.hSMul (β := (i : n) → α) (A i k)
      ((Aᵀ.cramer : (a : n → α) → n → α) (Pi.single (M := fun (a : n) ↦ α) k 1) : n → α) j =
    (Aᵀ.cramer : (a : n → α) → n → α) (Pi.single (M := fun (a : n) ↦ α) k (A i k)) j
rw₄ :
  Eq.{w + 1} (α := α)
    ((Aᵀ.cramer : (a : n → α) → (i : n) → α) (HSMul.hSMul (β := n → α) (A i k) (Pi.single (M := fun (a : n) ↦ α) k 1))
        j :
      α)
    ((Aᵀ.cramer : (a : n → α) → n → α) (Pi.single (M := fun (a : n) ↦ α) k (A i k)) j : α)
rw₅ :
  Eq.{w + 1} (α := α)
    ((Aᵀ.cramer : (a : n → α) → (i : n) → α) (Pi.single (M := fun (x : n) ↦ α) k (HSMul.hSMul (β := α) (A i k) 1)) j :
      α)
    ((Aᵀ.cramer : (a : n → α) → n → α) (Pi.single (M := fun (a : n) ↦ α) k (A i k)) j : α)
rw₆ :
  Eq.{w + 1} (α := α) ((Aᵀ.cramer : (a : n → α) → (i : n) → α) (Pi.single (M := fun (x : n) ↦ α) k (A i k * 1)) j : α)
    ((Aᵀ.cramer : (a : n → α) → n → α) (Pi.single (M := fun (a : n) ↦ α) k (A i k)) j : α)
rw₇ rw₈ :
  Eq.{w + 1} (α := α) ((Aᵀ.cramer : (a : n → α) → (i : n) → α) (Pi.single (M := fun (x : n) ↦ α) k (A i k)) j : α)
    ((Aᵀ.cramer : (a : n → α) → n → α) (Pi.single (M := fun (a : n) ↦ α) k (A i k)) j : α)
⊢ A i k * A.adjugate k j = (Aᵀ.cramer : (a : n → α) → n → α) (Pi.single (M := fun (a : n) ↦ α) k (A i k)) j

Tactic:
rw [← smul_eq_mul, adjugate, of_apply, ← Pi.smul_apply, ← map_smul, ← Pi.single_smul',
    smul_eq_mul, mul_one]

Premises used: Matrix.of_apply, Matrix.adjugate, Pi.single_smul', smul_eq_mul, mul_one, map_smul, Pi.smul_apply
-- Module: Mathlib.LinearAlgebra.Matrix.Adjugate
Goal:
n : Type v
α : Type w
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : CommRing α
A : Matrix n n α
a : ∀ (i j : n), (A * A.adjugate) i j = HSMul.hSMul (β := Matrix n n α) A.det 1 i j
⊢ A * A.adjugate = HSMul.hSMul (β := Matrix n n α) A.det 1

Tactic:
ext i j
-- Module: Mathlib.LinearAlgebra.Matrix.Adjugate
Goal:
n : Type v
α : Type w
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : CommRing α
A : Matrix n n α
i j : n
a : ∑ j_1 : n, A i j_1 * A.adjugate j_1 j = if i = j then A.det else 0
⊢ (A * A.adjugate) i j = HSMul.hSMul (β := Matrix n n α) A.det 1 i j

Tactic:
rw [mul_apply, Pi.smul_apply, Pi.smul_apply, one_apply, smul_eq_mul, mul_boole]

Premises used: Matrix.one_apply, mul_boole, Matrix.mul_apply, smul_eq_mul, Pi.smul_apply
-- Module: Mathlib.LinearAlgebra.Matrix.Adjugate
Goal:
n : Type v
α : Type w
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : CommRing α
A : Matrix n n α
i j : n
⊢ ∑ j_1 : n, A i j_1 * A.adjugate j_1 j = if i = j then A.det else 0

Tactic:
simp [mul_adjugate_apply, sum_cramer_apply, cramer_transpose_row_self, Pi.single_apply, eq_comm]

Premises used: Matrix.cramer_transpose_row_self, Pi.single_apply, Matrix.mul_adjugate_apply, eq_comm, Matrix.sum_cramer_apply
-- Module: Mathlib.LinearAlgebra.Matrix.Adjugate
Goal:
n : Type v
α : Type w
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : CommRing α
A : Matrix n n α
rw : A.adjugate * A = (Aᵀ * A.adjugateᵀ)ᵀ
rw₁ : A.adjugate * A = (A.adjugate * A)ᵀᵀ
rw₂ rw₃ : A.adjugate * A = A.adjugate * A
⊢ A.adjugate * A = (Aᵀ * Aᵀ.adjugate)ᵀ

Tactic:
rw [← adjugate_transpose, ← transpose_mul, transpose_transpose]

Premises used: Matrix.transpose_transpose, Matrix.transpose_mul, Matrix.adjugate_transpose
-- Module: Mathlib.LinearAlgebra.Matrix.Adjugate
Goal:
n : Type v
α : Type w
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : CommRing α
A : Matrix n n α
rw : (HSMul.hSMul (β := Matrix n n α) Aᵀ.det 1)ᵀ = HSMul.hSMul (β := Matrix n n α) A.det 1
rw₁ : (HSMul.hSMul (β := Matrix n n α) A.det 1)ᵀ = HSMul.hSMul (β := Matrix n n α) A.det 1
rw₂ : HSMul.hSMul (β := Matrix n n α) A.det 1ᵀ = HSMul.hSMul (β := Matrix n n α) A.det 1
rw₃ rw₄ : HSMul.hSMul (β := Matrix n n α) A.det 1 = HSMul.hSMul (β := Matrix n n α) A.det 1
⊢ (Aᵀ * Aᵀ.adjugate)ᵀ = HSMul.hSMul (β := Matrix n n α) A.det 1

Tactic:
rw [mul_adjugate Aᵀ, det_transpose, transpose_smul, transpose_one]

Premises used: Matrix.det_transpose, Matrix.transpose_one, Matrix.transpose, Matrix.transpose_smul, Matrix.mul_adjugate
-- Module: Mathlib.LinearAlgebra.Matrix.Adjugate
Goal:
n : Type v
α : Type w
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : CommRing α
r : α
A : Matrix n n α
rw :
  ((of : (a : n → n → α) → Matrix n n α) fun (i : n) ↦
      (HSMul.hSMul (β := (n → α) →ₗ[α] n → α) (r ^ (Fintype.card n - 1)) Aᵀ.cramer : (a : n → α) → n → α)
        (Pi.single (M := fun (a : n) ↦ α) i 1)) =
    HSMul.hSMul (β := Matrix n n α) (r ^ (Fintype.card n - 1))
      ((of : (a : n → n → α) → Matrix n n α) fun (i : n) ↦
        (Aᵀ.cramer : (a : n → α) → n → α) (Pi.single (M := fun (a : n) ↦ α) i 1))
⊢ (r • A).adjugate = r ^ (Fintype.card n - 1) • A.adjugate

Tactic:
rw [adjugate, adjugate, transpose_smul, cramer_smul]

Premises used: Matrix.adjugate, Matrix.transpose_smul, Matrix.cramer_smul
-- Module: Mathlib.LinearAlgebra.Matrix.Adjugate
Goal:
n : Type v
α : Type w
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : CommRing α
r : α
A : Matrix n n α
⊢ ((of : (a : n → n → α) → Matrix n n α) fun (i : n) ↦
      (HSMul.hSMul (β := (n → α) →ₗ[α] n → α) (r ^ (Fintype.card n - 1)) Aᵀ.cramer : (a : n → α) → n → α)
        (Pi.single (M := fun (a : n) ↦ α) i 1)) =
    HSMul.hSMul (β := Matrix n n α) (r ^ (Fintype.card n - 1))
      ((of : (a : n → n → α) → Matrix n n α) fun (i : n) ↦
        (Aᵀ.cramer : (a : n → α) → n → α) (Pi.single (M := fun (a : n) ↦ α) i 1))

Tactic:
rfl
-- Module: Mathlib.LinearAlgebra.Matrix.Adjugate
Goal:
n : Type v
α : Type w
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : CommRing α
A : Matrix n n α
b : n → α
rw : A *ᵥ A.adjugate *ᵥ b = A.det • b
rw₁ : (A * A.adjugate) *ᵥ b = A.det • b
rw₂ : HSMul.hSMul (β := Matrix n n α) A.det 1 *ᵥ b = A.det • b
rw₃ : HSMul.hSMul (β := n → α) A.det (1 *ᵥ b) = A.det • b
rw₄ rw₅ : A.det • b = A.det • b
⊢ A *ᵥ (A.cramer : (a : n → α) → n → α) b = A.det • b

Tactic:
rw [cramer_eq_adjugate_mulVec, mulVec_mulVec, mul_adjugate, smul_mulVec, one_mulVec]

Premises used: Matrix.one_mulVec, Matrix.smul_mulVec, Matrix.cramer_eq_adjugate_mulVec, Matrix.mul_adjugate, Matrix.mulVec_mulVec
-- Module: Mathlib.LinearAlgebra.Matrix.Adjugate
Goal:
n : Type v
α : Type w
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : CommRing α
M : Matrix n n α
v : n → α
h : M *ᵥ v = 0
i : n
hi : Membership.mem (γ := Submonoid α) (nonZeroDivisors α) (v i)
apply : M.det * v i = 0
⊢ M.det = 0

Tactic:
apply mul_right_mem_nonZeroDivisors_eq_zero_iff hi |>.mp

Premises used: mul_right_mem_nonZeroDivisors_eq_zero_iff, Iff.mp
-- Module: Mathlib.LinearAlgebra.Matrix.Adjugate
Goal:
n : Type v
α : Type w
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : CommRing α
M : Matrix n n α
v : n → α
h : M *ᵥ v = 0
i : n
hi : Membership.mem (γ := Submonoid α) (nonZeroDivisors α) (v i)
⊢ M.det * v i = 0

Tactic:
simpa [adjugate_mul, smul_mulVec] using congr((M.adjugate *ᵥ $h) i)

Premises used: Matrix.adjugate_mul, Matrix.smul_mulVec
-- Module: Mathlib.LinearAlgebra.Matrix.Adjugate
Goal:
n : Type v
α : Type w
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : CommRing α
inst_3 : Subsingleton n
A : Matrix n n α
a : ∀ (i j : n), A.adjugate i j = 1 i j
⊢ A.adjugate = 1

Tactic:
ext i j
-- Module: Mathlib.LinearAlgebra.Matrix.Adjugate
Goal:
n : Type v
α : Type w
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : CommRing α
inst_3 : Subsingleton n
A : Matrix n n α
i j : n
⊢ A.adjugate i j = 1 i j

Tactic:
simp [Subsingleton.elim i j, adjugate_apply, det_eq_elem_of_subsingleton _ i, one_apply]

Premises used: Matrix.one_apply, Matrix.det_eq_elem_of_subsingleton, Matrix.adjugate_apply, Subsingleton.elim
-- Module: Mathlib.LinearAlgebra.Matrix.Adjugate
Goal:
n : Type v
α : Type w
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : CommRing α
A : Matrix n n α
h : Fintype.card n = 1
⊢ A.adjugate = 1

Tactic:
haveI : Subsingleton n := Fintype.card_le_one_iff_subsingleton.mp h.le
  adjugate_subsingleton _

Premises used: Matrix.adjugate_subsingleton
-- Module: Mathlib.LinearAlgebra.Matrix.Adjugate
Goal:
n : Type v
α : Type w
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : CommRing α
inst_3 : Nontrivial n
a : ∀ (i j : n), Eq.{w + 1} (α := α) (adjugate 0 i j) (0 i j)
⊢ Eq (α := Matrix n n α) (adjugate 0) 0

Tactic:
ext i j
-- Module: Mathlib.LinearAlgebra.Matrix.Adjugate
Goal:
n : Type v
α : Type w
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : CommRing α
inst_3 : Nontrivial n
i j : n
a : ∀ (j' : n) (hj' : j' ≠ j), Eq.{w + 1} (α := α) (adjugate 0 i j) (0 i j)
⊢ Eq.{w + 1} (α := α) (adjugate 0 i j) (0 i j)

Tactic:
obtain ⟨j', hj'⟩ : ∃ j', j' ≠ j := exists_ne j

Premises used: exists_ne
-- Module: Mathlib.LinearAlgebra.Matrix.Adjugate
Goal:
n : Type v
α : Type w
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : CommRing α
inst_3 : Nontrivial n
i j j' : n
hj' : j' ≠ j
a : ∀ (i_1 : n), Eq.{w + 1} (α := α) (updateCol 0ᵀ j (Pi.single (M := fun (a : n) ↦ α) i 1) i_1 j') 0
⊢ Eq.{w + 1} (α := α) (adjugate 0 i j) (0 i j)

Tactic:
apply det_eq_zero_of_column_eq_zero j'

Premises used: Matrix.det_eq_zero_of_column_eq_zero
-- Module: Mathlib.LinearAlgebra.Matrix.Adjugate
Goal:
n : Type v
α : Type w
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : CommRing α
inst_3 : Nontrivial n
i j j' : n
hj' : j' ≠ j
⊢ ∀ (i_1 : n), Eq.{w + 1} (α := α) (updateCol 0ᵀ j (Pi.single (M := fun (a : n) ↦ α) i 1) i_1 j') 0

Tactic:
simp [updateCol_ne hj']

Premises used: Matrix.updateCol_ne
-- Module: Mathlib.LinearAlgebra.Matrix.Adjugate
Goal:
n : Type v
α : Type w
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : CommRing α
a : ∀ (i j : n), Eq.{w + 1} (α := α) (adjugate 1 i j) (1 i j)
⊢ Eq (α := Matrix n n α) (adjugate 1) 1

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.Matrix.Adjugate
Goal:
n : Type v
α : Type w
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : CommRing α
i j : n
⊢ Eq.{w + 1} (α := α) (adjugate 1 i j) (1 i j)

Tactic:
simp [adjugate_def, Matrix.one_apply, Pi.single_apply, eq_comm]

Premises used: Matrix.one_apply, Pi.single_apply, eq_comm, Matrix.adjugate_def
-- Module: Mathlib.LinearAlgebra.Matrix.Adjugate
Goal:
n : Type v
α : Type w
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : CommRing α
v : n → α
a : ∀ (i j : n), (diagonal v).adjugate i j = diagonal (fun (i : n) ↦ ∏ j ∈ Finset.erase univ i, v j) i j
⊢ (diagonal v).adjugate = diagonal fun (i : n) ↦ ∏ j ∈ Finset.erase univ i, v j

Tactic:
ext i j
-- Module: Mathlib.LinearAlgebra.Matrix.Adjugate
Goal:
n : Type v
α : Type w
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : CommRing α
v : n → α
i j : n
a :
  ((diagonal v).updateCol j (Pi.single (M := fun (a : n) ↦ α) i 1)).det =
    diagonal (fun (i : n) ↦ ∏ j ∈ Finset.erase univ i, v j) i j
⊢ (diagonal v).adjugate i j = diagonal (fun (i : n) ↦ ∏ j ∈ Finset.erase univ i, v j) i j

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

Premises used: Matrix.cramer_apply, Matrix.of_apply, Matrix.adjugate_def, Matrix.diagonal_transpose
-- Module: Mathlib.LinearAlgebra.Matrix.Adjugate
Goal:
n : Type v
α : Type w
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : CommRing α
v : n → α
i j : n
a :
  ((diagonal v).updateCol i (Pi.single (M := fun (a : n) ↦ α) i 1)).det =
    diagonal (fun (i : n) ↦ ∏ j ∈ Finset.erase univ i, v j) i i
a₁ :
  ∀ (hij : i ≠ j),
    ((diagonal v).updateCol j (Pi.single (M := fun (a : n) ↦ α) i 1)).det =
      diagonal (fun (i : n) ↦ ∏ j ∈ Finset.erase univ i, v j) i j
⊢ ((diagonal v).updateCol j (Pi.single (M := fun (a : n) ↦ α) i 1)).det =
    diagonal (fun (i : n) ↦ ∏ j ∈ Finset.erase univ i, v j) i j

Tactic:
obtain rfl | hij := eq_or_ne i j

Premises used: eq_or_ne, rfl
-- Module: Mathlib.LinearAlgebra.Matrix.Adjugate
Goal:
n : Type v
α : Type w
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : CommRing α
v : n → α
i : n
a : ((diagonal v).updateCol i (Pi.single (M := fun (a : n) ↦ α) i 1)).det = ∏ j ∈ Finset.erase univ i, v j
a₁ : (diagonal (Function.update (β := fun (a : n) ↦ α) v i 1)).det = ∏ j ∈ Finset.erase univ i, v j
a₂ : Eq.{w + 1} (α := α) (∏ i_1 : n, Function.update (β := fun (a : n) ↦ α) v i 1 i_1) (∏ j ∈ Finset.erase univ i, v j)
a₃ : HMul.hMul (α := α) 1 (∏ x ∈ univ \ {i}, v x) = ∏ j ∈ Finset.erase univ i, v j
a₄ : HMul.hMul (α := α) 1 (∏ x ∈ Finset.erase univ i, v x) = ∏ j ∈ Finset.erase univ i, v j
a₅ a₆ : Eq.{w + 1} (α := α) (∏ x ∈ Finset.erase univ i, v x) (∏ j ∈ Finset.erase univ i, v j)
⊢ ((diagonal v).updateCol i (Pi.single (M := fun (a : n) ↦ α) i 1)).det =
    diagonal (fun (i : n) ↦ ∏ j ∈ Finset.erase univ 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]

Premises used: Finset.mem_univ, Finset.sdiff_singleton_eq_erase, Matrix.diagonal_apply_eq, Matrix.diagonal_updateCol_single, Matrix.det_diagonal, Finset.prod_update_of_mem, one_mul
-- Module: Mathlib.LinearAlgebra.Matrix.Adjugate
Goal:
n : Type v
α : Type w
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : CommRing α
v : n → α
i j : n
hij : i ≠ j
a : ((diagonal v).updateCol j (Pi.single (M := fun (a : n) ↦ α) i 1)).det = 0
⊢ ((diagonal v).updateCol j (Pi.single (M := fun (a : n) ↦ α) i 1)).det =
    diagonal (fun (i : n) ↦ ∏ j ∈ Finset.erase univ i, v j) i j

Tactic:
rw [diagonal_apply_ne _ hij]

Premises used: Matrix.diagonal_apply_ne
-- Module: Mathlib.LinearAlgebra.Matrix.Adjugate
Goal:
n : Type v
α : Type w
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : CommRing α
v : n → α
i j : n
hij : i ≠ j
⊢ ((diagonal v).updateCol j (Pi.single (M := fun (a : n) ↦ α) i 1)).det = 0

Tactic:
det_eq_zero_of_row_eq_zero j fun k => ?_

Premises used: Matrix.det_eq_zero_of_row_eq_zero