awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Adjugate (goal)
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 α
⊢ Eq (α := Matrix n n α) (adjugate (A.submatrix (⇑e : (a : n) → m) (⇑e : (a : n) → m)))
    (A.adjugate.submatrix (⇑e : (a : n) → m) (⇑e : (a : n) → m))
have a : ∀ (i j : n),
  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: ext i j
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Adjugate (hypothesis)
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
⊢ 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
have 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) → α)
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
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Adjugate (goal)
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) → α)
⊢ 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
have 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
Tactic: rw [adjugate_apply, submatrix_apply, adjugate_apply, ← det_submatrix_equiv_self e,
    updateRow_submatrix_equiv, this]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Adjugate (goal)
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
⊢ 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
have 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)
Tactic: rw [adjugate_apply, submatrix_apply, adjugate_apply, ← det_submatrix_equiv_self e,
    updateRow_submatrix_equiv, this]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Adjugate (goal)
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)
⊢ 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
have 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
Tactic: rw [adjugate_apply, submatrix_apply, adjugate_apply, ← det_submatrix_equiv_self e,
    updateRow_submatrix_equiv, this]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Adjugate (goal)
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
⊢ 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
have 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))
Tactic: rw [adjugate_apply, submatrix_apply, adjugate_apply, ← det_submatrix_equiv_self e,
    updateRow_submatrix_equiv, this]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Adjugate (goal)
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))
⊢ 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
have 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))
Tactic: rw [adjugate_apply, submatrix_apply, adjugate_apply, ← det_submatrix_equiv_self e,
    updateRow_submatrix_equiv, this]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Adjugate (goal)
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))
⊢ 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
have 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))
Tactic: rw [adjugate_apply, submatrix_apply, adjugate_apply, ← det_submatrix_equiv_self e,
    updateRow_submatrix_equiv, this]
-- 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.cramer : (a : n → α) → n → α) b = A.adjugate *ᵥ b
have nth_rw : (A.cramer : (a : n → α) → n → α) b = Aᵀᵀ.adjugate *ᵥ b
Tactic: nth_rw 2 [← A.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 α
b : n → α
⊢ (A.cramer : (a : n → α) → n → α) b = Aᵀᵀ.adjugate *ᵥ b
have 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 → α)
Tactic: rw [← adjugate_transpose, adjugate_def]
-- 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 → α
⊢ b = ∑ i : n, HSMul.hSMul (β := (j : n) → α) (b i) (Pi.single (M := fun (a : n) ↦ α) i 1)
have 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))
Tactic: refine (pi_eq_sum_univ b).trans ?_
-- 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 → α
⊢ 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))
have 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
Tactic: congr with j
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Adjugate (hypothesis)
Goal:
n : Type v
α : Type w
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : CommRing α
A : Matrix n n α
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 → α)
have this : 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]
-- 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 → α
this : b = ∑ i : n, HSMul.hSMul (β := (j : n) → α) (b i) (Pi.single (M := fun (a : n) ↦ α) i 1)
| ((A.cramer : (a : n → α) → n → α) b : n → α)
have rw : ((A.cramer : (a : n → α) → n → α)
    (∑ i : n, HSMul.hSMul (β := (j : n) → α) (b i) (Pi.single (M := fun (a : n) ↦ α) i 1)) :
  n → α)
Tactic: rw [this]
-- 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 → α
this : b = ∑ i : n, HSMul.hSMul (β := (j : n) → α) (b i) (Pi.single (M := fun (a : n) ↦ α) i 1)
⊢ 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 → α)
have 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 → α)
Tactic: conv_lhs =>
    rw [this]
-- 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 → α
this : b = ∑ i : n, HSMul.hSMul (β := (j : n) → α) (b i) (Pi.single (M := fun (a : n) ↦ α) i 1)
⊢ 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 → α)
have 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
Tactic: ext 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 α
A : Matrix n n α
i j k : n
⊢ 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 : 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]
-- 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
⊢ 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₁ : 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
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 α
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
⊢ 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₂ : 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
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 α
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
⊢ 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₃ : 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
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 α
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
⊢ 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) → α) (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 : α)
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 α
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 : α)
⊢ 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 (HSMul.hSMul (β := α) (A i k) 1)) 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 α
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 : α)
⊢ 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 * 1)) 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]