awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Adjugate (goal)
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 : α)
⊢ A i k * A.adjugate k j = (Aᵀ.cramer : (a : n → α) → n → α) (Pi.single (M := fun (a : n) ↦ α) k (A i k)) j
have 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 : α)
Tactic: rw [← smul_eq_mul, adjugate, of_apply, ← Pi.smul_apply, ← map_smul, ← Pi.single_smul',
    smul_eq_mul, mul_one]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Adjugate (goal)
Goal:
n : Type v
α : Type w
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : CommRing α
A : Matrix n n α
⊢ A * A.adjugate = HSMul.hSMul (β := Matrix n n α) A.det 1
have a : ∀ (i j : n), (A * A.adjugate) i j = HSMul.hSMul (β := Matrix n n α) A.det 1 i j
Tactic: ext i j
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Adjugate (goal)
Goal:
n : Type v
α : Type w
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : CommRing α
A : Matrix n n α
i j : n
⊢ (A * A.adjugate) i j = HSMul.hSMul (β := Matrix n n α) A.det 1 i j
have a : ∑ j_1 : n, A i j_1 * A.adjugate j_1 j = if i = j then A.det else 0
Tactic: rw [mul_apply, Pi.smul_apply, Pi.smul_apply, one_apply, smul_eq_mul, mul_boole]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Adjugate (goal)
Goal:
n : Type v
α : Type w
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : CommRing α
A : Matrix n n α
⊢ A.adjugate * A = (Aᵀ * Aᵀ.adjugate)ᵀ
have rw : A.adjugate * A = (Aᵀ * A.adjugateᵀ)ᵀ
Tactic: rw [← adjugate_transpose, ← transpose_mul, transpose_transpose]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Adjugate (goal)
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ᵀ)ᵀ
⊢ A.adjugate * A = (Aᵀ * Aᵀ.adjugate)ᵀ
have rw₁ : A.adjugate * A = (A.adjugate * A)ᵀᵀ
Tactic: rw [← adjugate_transpose, ← transpose_mul, transpose_transpose]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Adjugate (goal)
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)ᵀᵀ
⊢ A.adjugate * A = (Aᵀ * Aᵀ.adjugate)ᵀ
have rw₂ : A.adjugate * A = A.adjugate * A
Tactic: rw [← adjugate_transpose, ← transpose_mul, transpose_transpose]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Adjugate (goal)
Goal:
n : Type v
α : Type w
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : CommRing α
A : Matrix n n α
⊢ (Aᵀ * Aᵀ.adjugate)ᵀ = HSMul.hSMul (β := Matrix n n α) A.det 1
have rw : (HSMul.hSMul (β := Matrix n n α) Aᵀ.det 1)ᵀ = HSMul.hSMul (β := Matrix n n α) A.det 1
Tactic: rw [mul_adjugate Aᵀ, det_transpose, transpose_smul, transpose_one]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Adjugate (goal)
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
⊢ (Aᵀ * Aᵀ.adjugate)ᵀ = HSMul.hSMul (β := Matrix n n α) A.det 1
have rw₁ : (HSMul.hSMul (β := Matrix n n α) A.det 1)ᵀ = HSMul.hSMul (β := Matrix n n α) A.det 1
Tactic: rw [mul_adjugate Aᵀ, det_transpose, transpose_smul, transpose_one]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Adjugate (goal)
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
⊢ (Aᵀ * Aᵀ.adjugate)ᵀ = HSMul.hSMul (β := Matrix n n α) A.det 1
have rw₂ : HSMul.hSMul (β := Matrix n n α) A.det 1ᵀ = HSMul.hSMul (β := Matrix n n α) A.det 1
Tactic: rw [mul_adjugate Aᵀ, det_transpose, transpose_smul, transpose_one]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Adjugate (goal)
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
⊢ (Aᵀ * Aᵀ.adjugate)ᵀ = HSMul.hSMul (β := Matrix n n α) A.det 1
have rw₃ : HSMul.hSMul (β := Matrix n n α) A.det 1 = HSMul.hSMul (β := Matrix n n α) A.det 1
Tactic: rw [mul_adjugate Aᵀ, det_transpose, transpose_smul, transpose_one]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Adjugate (goal)
Goal:
n : Type v
α : Type w
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : CommRing α
r : α
A : Matrix n n α
⊢ (r • A).adjugate = r ^ (Fintype.card n - 1) • A.adjugate
have 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))
Tactic: rw [adjugate, adjugate, transpose_smul, cramer_smul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Adjugate (goal)
Goal:
n : Type v
α : Type w
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : CommRing α
A : Matrix n n α
b : n → α
⊢ A *ᵥ (A.cramer : (a : n → α) → n → α) b = A.det • b
have rw : A *ᵥ A.adjugate *ᵥ b = A.det • b
Tactic: rw [cramer_eq_adjugate_mulVec, mulVec_mulVec, mul_adjugate, smul_mulVec, one_mulVec]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Adjugate (goal)
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
⊢ A *ᵥ (A.cramer : (a : n → α) → n → α) b = A.det • b
have rw₁ : (A * A.adjugate) *ᵥ b = A.det • b
Tactic: rw [cramer_eq_adjugate_mulVec, mulVec_mulVec, mul_adjugate, smul_mulVec, one_mulVec]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Adjugate (goal)
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
⊢ A *ᵥ (A.cramer : (a : n → α) → n → α) b = A.det • b
have rw₂ : HSMul.hSMul (β := Matrix n n α) A.det 1 *ᵥ b = A.det • b
Tactic: rw [cramer_eq_adjugate_mulVec, mulVec_mulVec, mul_adjugate, smul_mulVec, one_mulVec]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Adjugate (goal)
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
⊢ A *ᵥ (A.cramer : (a : n → α) → n → α) b = A.det • b
have rw₃ : HSMul.hSMul (β := n → α) A.det (1 *ᵥ b) = A.det • b
Tactic: rw [cramer_eq_adjugate_mulVec, mulVec_mulVec, mul_adjugate, smul_mulVec, one_mulVec]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Adjugate (goal)
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
⊢ A *ᵥ (A.cramer : (a : n → α) → n → α) b = A.det • b
have rw₄ : A.det • b = A.det • b
Tactic: rw [cramer_eq_adjugate_mulVec, mulVec_mulVec, mul_adjugate, smul_mulVec, one_mulVec]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Adjugate (goal)
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 = 0
have apply : M.det * v i = 0
Tactic: apply mul_right_mem_nonZeroDivisors_eq_zero_iff hi |>.mp
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Adjugate (goal)
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.adjugate = 1
have a : ∀ (i j : n), A.adjugate i j = 1 i j
Tactic: ext i j
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Adjugate (goal)
Goal:
n : Type v
α : Type w
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : CommRing α
inst_3 : Nontrivial n
⊢ Eq (α := Matrix n n α) (adjugate 0) 0
have a : ∀ (i j : n), Eq.{w + 1} (α := α) (adjugate 0 i j) (0 i j)
Tactic: ext i j
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Adjugate (goal)
Goal:
n : Type v
α : Type w
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : CommRing α
inst_3 : Nontrivial n
i j : n
⊢ Eq.{w + 1} (α := α) (adjugate 0 i j) (0 i j)
have a : ∀ (j' : n) (hj' : j' ≠ j), Eq.{w + 1} (α := α) (adjugate 0 i j) (0 i j)
Tactic: obtain ⟨j', hj'⟩ : ∃ j', j' ≠ j := exists_ne j
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Adjugate (goal)
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
⊢ Eq.{w + 1} (α := α) (adjugate 0 i j) (0 i j)
have a : ∀ (i_1 : n), Eq.{w + 1} (α := α) (updateCol 0ᵀ j (Pi.single (M := fun (a : n) ↦ α) i 1) i_1 j') 0
Tactic: apply det_eq_zero_of_column_eq_zero j'
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Adjugate (goal)
Goal:
n : Type v
α : Type w
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : CommRing α
⊢ Eq (α := Matrix n n α) (adjugate 1) 1
have a : ∀ (i j : n), Eq.{w + 1} (α := α) (adjugate 1 i j) (1 i j)
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Adjugate (goal)
Goal:
n : Type v
α : Type w
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : CommRing α
v : n → α
⊢ (diagonal v).adjugate = diagonal fun (i : n) ↦ ∏ j ∈ Finset.erase univ i, v j
have a : ∀ (i j : n), (diagonal v).adjugate i j = diagonal (fun (i : n) ↦ ∏ j ∈ Finset.erase univ i, v j) i j
Tactic: ext i j
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Adjugate (goal)
Goal:
n : Type v
α : Type w
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : CommRing α
v : n → α
i j : n
⊢ (diagonal v).adjugate i j = diagonal (fun (i : n) ↦ ∏ j ∈ Finset.erase univ i, v j) i j
have 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
Tactic: simp only [adjugate_def, cramer_apply, diagonal_transpose, of_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Adjugate (goal)
Goal:
n : Type v
α : Type w
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : CommRing α
v : n → α
i j : n
⊢ ((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
have 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
Tactic: obtain rfl | hij := eq_or_ne i j
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Adjugate (goal)
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
⊢ ((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
have 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
Tactic: obtain rfl | hij := eq_or_ne i j
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Adjugate (goal)
Goal:
n : Type v
α : Type w
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : CommRing α
v : n → α
i : n
⊢ ((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
have a : ((diagonal v).updateCol i (Pi.single (M := fun (a : n) ↦ α) i 1)).det = ∏ j ∈ Finset.erase univ i, v j
Tactic: rw [diagonal_apply_eq, diagonal_updateCol_single, det_diagonal,
      prod_update_of_mem (Finset.mem_univ _), sdiff_singleton_eq_erase, one_mul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Adjugate (goal)
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
⊢ ((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
have a₁ : (diagonal (Function.update (β := fun (a : n) ↦ α) v i 1)).det = ∏ j ∈ Finset.erase univ i, v j
Tactic: rw [diagonal_apply_eq, diagonal_updateCol_single, det_diagonal,
      prod_update_of_mem (Finset.mem_univ _), sdiff_singleton_eq_erase, one_mul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Adjugate (goal)
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
⊢ ((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
have a₂ : Eq.{w + 1} (α := α) (∏ i_1 : n, Function.update (β := fun (a : n) ↦ α) v i 1 i_1) (∏ j ∈ Finset.erase univ i, v j)
Tactic: rw [diagonal_apply_eq, diagonal_updateCol_single, det_diagonal,
      prod_update_of_mem (Finset.mem_univ _), sdiff_singleton_eq_erase, one_mul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Adjugate (goal)
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)
⊢ ((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
have a₃ : HMul.hMul (α := α) 1 (∏ x ∈ univ \ {i}, v x) = ∏ j ∈ Finset.erase univ i, v j
Tactic: rw [diagonal_apply_eq, diagonal_updateCol_single, det_diagonal,
      prod_update_of_mem (Finset.mem_univ _), sdiff_singleton_eq_erase, one_mul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Adjugate (goal)
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
⊢ ((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
have a₄ : HMul.hMul (α := α) 1 (∏ x ∈ Finset.erase univ i, v x) = ∏ j ∈ Finset.erase univ i, v j
Tactic: rw [diagonal_apply_eq, diagonal_updateCol_single, det_diagonal,
      prod_update_of_mem (Finset.mem_univ _), sdiff_singleton_eq_erase, one_mul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Adjugate (goal)
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
⊢ ((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
have a₅ : Eq.{w + 1} (α := α) (∏ x ∈ Finset.erase univ i, v x) (∏ j ∈ Finset.erase univ i, v j)
Tactic: rw [diagonal_apply_eq, diagonal_updateCol_single, det_diagonal,
      prod_update_of_mem (Finset.mem_univ _), sdiff_singleton_eq_erase, one_mul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Adjugate (goal)
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 =
    diagonal (fun (i : n) ↦ ∏ j ∈ Finset.erase univ i, v j) i j
have a : ((diagonal v).updateCol j (Pi.single (M := fun (a : n) ↦ α) i 1)).det = 0
Tactic: rw [diagonal_apply_ne _ hij]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Adjugate (goal)
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
have a : ∀ (k : n), (diagonal v).updateCol j (Pi.single (M := fun (a : n) ↦ α) i 1) j k = 0
Tactic: refine det_eq_zero_of_row_eq_zero j fun k => ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Adjugate (goal)
Goal:
n : Type v
α : Type w
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : CommRing α
v : n → α
i j : n
hij : i ≠ j
k : n
⊢ (diagonal v).updateCol j (Pi.single (M := fun (a : n) ↦ α) i 1) j k = 0
have a : ∀ (hij : i ≠ k), (diagonal v).updateCol k (Pi.single (M := fun (a : n) ↦ α) i 1) k k = 0
Tactic: obtain rfl | hjk := eq_or_ne k j
Cleared hypotheses: j, hij
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Adjugate (goal)
Goal:
n : Type v
α : Type w
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : CommRing α
v : n → α
i j : n
hij : i ≠ j
k : n
a : ∀ (hij : i ≠ k), (diagonal v).updateCol k (Pi.single (M := fun (a : n) ↦ α) i 1) k k = 0
⊢ (diagonal v).updateCol j (Pi.single (M := fun (a : n) ↦ α) i 1) j k = 0
have a₁ : ∀ (hjk : k ≠ j), (diagonal v).updateCol j (Pi.single (M := fun (a : n) ↦ α) i 1) j k = 0
Tactic: obtain rfl | hjk := eq_or_ne k j
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Adjugate (goal)
Goal:
n : Type v
α : Type w
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : CommRing α
v : n → α
i k : n
hij : i ≠ k
⊢ (diagonal v).updateCol k (Pi.single (M := fun (a : n) ↦ α) i 1) k k = 0
have a : Eq.{w + 1} (α := α) (Pi.single (M := fun (a : n) ↦ α) i 1 k : α) (0 : α)
Tactic: rw [updateCol_self, Pi.single_eq_of_ne' hij]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Adjugate (goal)
Goal:
n : Type v
α : Type w
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : CommRing α
v : n → α
i k : n
hij : i ≠ k
a : Eq.{w + 1} (α := α) (Pi.single (M := fun (a : n) ↦ α) i 1 k : α) (0 : α)
⊢ (diagonal v).updateCol k (Pi.single (M := fun (a : n) ↦ α) i 1) k k = 0
have a₁ : Eq.{w + 1} (α := α) 0 0
Tactic: rw [updateCol_self, Pi.single_eq_of_ne' hij]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Adjugate (goal)
Goal:
n : Type v
α : Type w
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : CommRing α
v : n → α
i j : n
hij : i ≠ j
k : n
hjk : k ≠ j
⊢ (diagonal v).updateCol j (Pi.single (M := fun (a : n) ↦ α) i 1) j k = 0
have a : diagonal v j k = 0
Tactic: rw [updateCol_ne hjk, diagonal_apply_ne' _ hjk]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Adjugate (goal)
Goal:
n : Type v
α : Type w
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : CommRing α
v : n → α
i j : n
hij : i ≠ j
k : n
hjk : k ≠ j
a : diagonal v j k = 0
⊢ (diagonal v).updateCol j (Pi.single (M := fun (a : n) ↦ α) i 1) j k = 0
have a₁ : Eq.{w + 1} (α := α) 0 0
Tactic: rw [updateCol_ne hjk, diagonal_apply_ne' _ hjk]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Adjugate (goal)
Goal:
n : Type v
inst : DecidableEq n
inst_1 : Fintype n
R : Type u_1
S : Type u_2
inst_2 : CommRing R
inst_3 : CommRing S
f : R →+* S
M : Matrix n n R
⊢ Eq (α := Matrix n n S) ((f.mapMatrix : (a : Matrix n n R) → Matrix n n S) M.adjugate : Matrix n n S)
    (adjugate ((f.mapMatrix : (a : Matrix n n R) → Matrix n n S) M) : Matrix n n S)
have a : ∀ (i k : n),
  Eq.{u_2 + 1} (α := S) ((f.mapMatrix : (a : Matrix n n R) → Matrix n n S) M.adjugate i k : S)
    (adjugate ((f.mapMatrix : (a : Matrix n n R) → Matrix n n S) M) i k : S)
Tactic: ext i k
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Adjugate (goal)
Goal:
n : Type v
inst : DecidableEq n
inst_1 : Fintype n
R : Type u_1
S : Type u_2
inst_2 : CommRing R
inst_3 : CommRing S
f : R →+* S
M : Matrix n n R
i k : n
⊢ Eq (α := (j : n) → S) (Pi.single (M := fun (a : n) ↦ S) i 1)
    (Function.comp.{v + 1, u_1 + 1, u_2 + 1} (β := R) (⇑f : (a : R) → S) (Pi.single (M := fun (a : n) ↦ R) i 1))
have rw : Eq (α := (j : n) → S) (Pi.single (M := fun (a : n) ↦ S) i ((f : (a : R) → S) 1))
  (Function.comp.{v + 1, u_1 + 1, u_2 + 1} (β := R) (⇑f : (a : R) → S) (Pi.single (M := fun (a : n) ↦ R) i 1))
Tactic: rw [← f.map_one]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Adjugate (hypothesis)
Goal:
n : Type v
inst : DecidableEq n
inst_1 : Fintype n
R : Type u_1
S : Type u_2
inst_2 : CommRing R
inst_3 : CommRing S
f : R →+* S
M : Matrix n n R
i k : n
⊢ Eq.{u_2 + 1} (α := S) ((f.mapMatrix : (a : Matrix n n R) → Matrix n n S) M.adjugate i k : S)
    (adjugate ((f.mapMatrix : (a : Matrix n n R) → Matrix n n S) M) i k : S)
have this : Eq (α := (j : n) → S) (Pi.single (M := fun (a : n) ↦ S) i 1)
  (Function.comp.{v + 1, u_1 + 1, u_2 + 1} (β := R) (⇑f : (a : R) → S) (Pi.single (M := fun (a : n) ↦ R) i 1))
Tactic: have : Pi.single i (1 : S) = f ∘ Pi.single i 1 := by
    rw [← f.map_one]
    exact Pi.single_op (fun _ => f) (fun _ => f.map_zero) i (1 : R)