awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
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))
⊢ 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 a : Eq.{u_2 + 1} (α := S) ((f.mapMatrix : (a : Matrix n n R) → Matrix n n S) M.adjugate i k : S)
  (det (updateRow ((f.mapMatrix : (a : Matrix n n R) → Matrix n n S) M) k (Pi.single (M := fun (a : n) ↦ S) i 1)) : S)
Tactic: rw [adjugate_apply, RingHom.mapMatrix_apply, map_apply, RingHom.mapMatrix_apply, this, ←
    map_updateRow, ← RingHom.mapMatrix_apply, ← RingHom.map_det, ← adjugate_apply]
-- 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
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))
a :
  Eq.{u_2 + 1} (α := S) ((f.mapMatrix : (a : Matrix n n R) → Matrix n n S) M.adjugate i k : S)
    (det (updateRow ((f.mapMatrix : (a : Matrix n n R) → Matrix n n S) M) k (Pi.single (M := fun (a : n) ↦ S) i 1)) : S)
⊢ 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 a₁ : Eq.{u_2 + 1} (α := S) (M.adjugate.map (⇑f : (a : R) → S) i k)
  (det (updateRow ((f.mapMatrix : (a : Matrix n n R) → Matrix n n S) M) k (Pi.single (M := fun (a : n) ↦ S) i 1)))
Tactic: rw [adjugate_apply, RingHom.mapMatrix_apply, map_apply, RingHom.mapMatrix_apply, this, ←
    map_updateRow, ← RingHom.mapMatrix_apply, ← RingHom.map_det, ← adjugate_apply]
-- 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
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))
a :
  Eq.{u_2 + 1} (α := S) ((f.mapMatrix : (a : Matrix n n R) → Matrix n n S) M.adjugate i k : S)
    (det (updateRow ((f.mapMatrix : (a : Matrix n n R) → Matrix n n S) M) k (Pi.single (M := fun (a : n) ↦ S) i 1)) : S)
a₁ :
  Eq.{u_2 + 1} (α := S) (M.adjugate.map (⇑f : (a : R) → S) i k)
    (det (updateRow ((f.mapMatrix : (a : Matrix n n R) → Matrix n n S) M) k (Pi.single (M := fun (a : n) ↦ S) i 1)))
⊢ 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 a₂ : Eq.{u_2 + 1} (α := S) ((f : (a : R) → S) (M.adjugate i k) : S)
  (det (updateRow ((f.mapMatrix : (a : Matrix n n R) → Matrix n n S) M) k (Pi.single (M := fun (a : n) ↦ S) i 1)) : S)
Tactic: rw [adjugate_apply, RingHom.mapMatrix_apply, map_apply, RingHom.mapMatrix_apply, this, ←
    map_updateRow, ← RingHom.mapMatrix_apply, ← RingHom.map_det, ← adjugate_apply]
-- 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
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))
a :
  Eq.{u_2 + 1} (α := S) ((f.mapMatrix : (a : Matrix n n R) → Matrix n n S) M.adjugate i k : S)
    (det (updateRow ((f.mapMatrix : (a : Matrix n n R) → Matrix n n S) M) k (Pi.single (M := fun (a : n) ↦ S) i 1)) : S)
a₁ :
  Eq.{u_2 + 1} (α := S) (M.adjugate.map (⇑f : (a : R) → S) i k)
    (det (updateRow ((f.mapMatrix : (a : Matrix n n R) → Matrix n n S) M) k (Pi.single (M := fun (a : n) ↦ S) i 1)))
a₂ :
  Eq.{u_2 + 1} (α := S) ((f : (a : R) → S) (M.adjugate i k) : S)
    (det (updateRow ((f.mapMatrix : (a : Matrix n n R) → Matrix n n S) M) k (Pi.single (M := fun (a : n) ↦ S) i 1)) : S)
⊢ 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 a₃ : Eq.{u_2 + 1} (α := S) ((f : (a : R) → S) (M.adjugate i k) : S)
  (det (updateRow (M.map (⇑f : (a : R) → S)) k (Pi.single (M := fun (a : n) ↦ S) i 1)) : S)
Tactic: rw [adjugate_apply, RingHom.mapMatrix_apply, map_apply, RingHom.mapMatrix_apply, this, ←
    map_updateRow, ← RingHom.mapMatrix_apply, ← RingHom.map_det, ← adjugate_apply]
-- 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
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))
a :
  Eq.{u_2 + 1} (α := S) ((f.mapMatrix : (a : Matrix n n R) → Matrix n n S) M.adjugate i k : S)
    (det (updateRow ((f.mapMatrix : (a : Matrix n n R) → Matrix n n S) M) k (Pi.single (M := fun (a : n) ↦ S) i 1)) : S)
a₁ :
  Eq.{u_2 + 1} (α := S) (M.adjugate.map (⇑f : (a : R) → S) i k)
    (det (updateRow ((f.mapMatrix : (a : Matrix n n R) → Matrix n n S) M) k (Pi.single (M := fun (a : n) ↦ S) i 1)))
a₂ :
  Eq.{u_2 + 1} (α := S) ((f : (a : R) → S) (M.adjugate i k) : S)
    (det (updateRow ((f.mapMatrix : (a : Matrix n n R) → Matrix n n S) M) k (Pi.single (M := fun (a : n) ↦ S) i 1)) : S)
a₃ :
  Eq.{u_2 + 1} (α := S) ((f : (a : R) → S) (M.adjugate i k) : S)
    (det (updateRow (M.map (⇑f : (a : R) → S)) k (Pi.single (M := fun (a : n) ↦ S) i 1)) : S)
⊢ 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 a₄ : Eq.{u_2 + 1} (α := S) ((f : (a : R) → S) (M.adjugate i k) : S)
  (det
      (updateRow (M.map (⇑f : (a : R) → S)) k
        (Function.comp.{v + 1, u_1 + 1, u_2 + 1} (β := R) (⇑f : (a : R) → S) (Pi.single (M := fun (a : n) ↦ R) i 1))) :
    S)
Tactic: rw [adjugate_apply, RingHom.mapMatrix_apply, map_apply, RingHom.mapMatrix_apply, this, ←
    map_updateRow, ← RingHom.mapMatrix_apply, ← RingHom.map_det, ← adjugate_apply]
-- 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
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))
a :
  Eq.{u_2 + 1} (α := S) ((f.mapMatrix : (a : Matrix n n R) → Matrix n n S) M.adjugate i k : S)
    (det (updateRow ((f.mapMatrix : (a : Matrix n n R) → Matrix n n S) M) k (Pi.single (M := fun (a : n) ↦ S) i 1)) : S)
a₁ :
  Eq.{u_2 + 1} (α := S) (M.adjugate.map (⇑f : (a : R) → S) i k)
    (det (updateRow ((f.mapMatrix : (a : Matrix n n R) → Matrix n n S) M) k (Pi.single (M := fun (a : n) ↦ S) i 1)))
a₂ :
  Eq.{u_2 + 1} (α := S) ((f : (a : R) → S) (M.adjugate i k) : S)
    (det (updateRow ((f.mapMatrix : (a : Matrix n n R) → Matrix n n S) M) k (Pi.single (M := fun (a : n) ↦ S) i 1)) : S)
a₃ :
  Eq.{u_2 + 1} (α := S) ((f : (a : R) → S) (M.adjugate i k) : S)
    (det (updateRow (M.map (⇑f : (a : R) → S)) k (Pi.single (M := fun (a : n) ↦ S) i 1)) : S)
a₄ :
  Eq.{u_2 + 1} (α := S) ((f : (a : R) → S) (M.adjugate i k) : S)
    (det
        (updateRow (M.map (⇑f : (a : R) → S)) k
          (Function.comp.{v + 1, u_1 + 1, u_2 + 1} (β := R) (⇑f : (a : R) → S)
            (Pi.single (M := fun (a : n) ↦ R) i 1))) :
      S)
⊢ 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 a₅ : Eq.{u_2 + 1} (α := S) ((f : (a : R) → S) (M.adjugate i k) : S)
  (det ((M.updateRow k (Pi.single (M := fun (a : n) ↦ R) i 1)).map (⇑f : (a : R) → S)) : S)
Tactic: rw [adjugate_apply, RingHom.mapMatrix_apply, map_apply, RingHom.mapMatrix_apply, this, ←
    map_updateRow, ← RingHom.mapMatrix_apply, ← RingHom.map_det, ← adjugate_apply]
-- 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
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))
a :
  Eq.{u_2 + 1} (α := S) ((f.mapMatrix : (a : Matrix n n R) → Matrix n n S) M.adjugate i k : S)
    (det (updateRow ((f.mapMatrix : (a : Matrix n n R) → Matrix n n S) M) k (Pi.single (M := fun (a : n) ↦ S) i 1)) : S)
a₁ :
  Eq.{u_2 + 1} (α := S) (M.adjugate.map (⇑f : (a : R) → S) i k)
    (det (updateRow ((f.mapMatrix : (a : Matrix n n R) → Matrix n n S) M) k (Pi.single (M := fun (a : n) ↦ S) i 1)))
a₂ :
  Eq.{u_2 + 1} (α := S) ((f : (a : R) → S) (M.adjugate i k) : S)
    (det (updateRow ((f.mapMatrix : (a : Matrix n n R) → Matrix n n S) M) k (Pi.single (M := fun (a : n) ↦ S) i 1)) : S)
a₃ :
  Eq.{u_2 + 1} (α := S) ((f : (a : R) → S) (M.adjugate i k) : S)
    (det (updateRow (M.map (⇑f : (a : R) → S)) k (Pi.single (M := fun (a : n) ↦ S) i 1)) : S)
a₄ :
  Eq.{u_2 + 1} (α := S) ((f : (a : R) → S) (M.adjugate i k) : S)
    (det
        (updateRow (M.map (⇑f : (a : R) → S)) k
          (Function.comp.{v + 1, u_1 + 1, u_2 + 1} (β := R) (⇑f : (a : R) → S)
            (Pi.single (M := fun (a : n) ↦ R) i 1))) :
      S)
a₅ :
  Eq.{u_2 + 1} (α := S) ((f : (a : R) → S) (M.adjugate i k) : S)
    (det ((M.updateRow k (Pi.single (M := fun (a : n) ↦ R) i 1)).map (⇑f : (a : R) → S)) : S)
⊢ 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 a₆ : Eq.{u_2 + 1} (α := S) ((f : (a : R) → S) (M.adjugate i k) : S)
  (det.{u_2, v} (n := n)
      ((f.mapMatrix : (a : Matrix n n R) → Matrix n n S) (M.updateRow k (Pi.single (M := fun (a : n) ↦ R) i 1))) :
    S)
Tactic: rw [adjugate_apply, RingHom.mapMatrix_apply, map_apply, RingHom.mapMatrix_apply, this, ←
    map_updateRow, ← RingHom.mapMatrix_apply, ← RingHom.map_det, ← adjugate_apply]
-- 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
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))
a :
  Eq.{u_2 + 1} (α := S) ((f.mapMatrix : (a : Matrix n n R) → Matrix n n S) M.adjugate i k : S)
    (det (updateRow ((f.mapMatrix : (a : Matrix n n R) → Matrix n n S) M) k (Pi.single (M := fun (a : n) ↦ S) i 1)) : S)
a₁ :
  Eq.{u_2 + 1} (α := S) (M.adjugate.map (⇑f : (a : R) → S) i k)
    (det (updateRow ((f.mapMatrix : (a : Matrix n n R) → Matrix n n S) M) k (Pi.single (M := fun (a : n) ↦ S) i 1)))
a₂ :
  Eq.{u_2 + 1} (α := S) ((f : (a : R) → S) (M.adjugate i k) : S)
    (det (updateRow ((f.mapMatrix : (a : Matrix n n R) → Matrix n n S) M) k (Pi.single (M := fun (a : n) ↦ S) i 1)) : S)
a₃ :
  Eq.{u_2 + 1} (α := S) ((f : (a : R) → S) (M.adjugate i k) : S)
    (det (updateRow (M.map (⇑f : (a : R) → S)) k (Pi.single (M := fun (a : n) ↦ S) i 1)) : S)
a₄ :
  Eq.{u_2 + 1} (α := S) ((f : (a : R) → S) (M.adjugate i k) : S)
    (det
        (updateRow (M.map (⇑f : (a : R) → S)) k
          (Function.comp.{v + 1, u_1 + 1, u_2 + 1} (β := R) (⇑f : (a : R) → S)
            (Pi.single (M := fun (a : n) ↦ R) i 1))) :
      S)
a₅ :
  Eq.{u_2 + 1} (α := S) ((f : (a : R) → S) (M.adjugate i k) : S)
    (det ((M.updateRow k (Pi.single (M := fun (a : n) ↦ R) i 1)).map (⇑f : (a : R) → S)) : S)
a₆ :
  Eq.{u_2 + 1} (α := S) ((f : (a : R) → S) (M.adjugate i k) : S)
    (det.{u_2, v} (n := n)
        ((f.mapMatrix : (a : Matrix n n R) → Matrix n n S) (M.updateRow k (Pi.single (M := fun (a : n) ↦ R) i 1))) :
      S)
⊢ 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 a₇ : Eq.{u_2 + 1} (α := S) ((f : (a : R) → S) (M.adjugate i k) : S)
  ((f : (a : R) → S) (M.updateRow k (Pi.single (M := fun (a : n) ↦ R) i 1)).det : S)
Tactic: rw [adjugate_apply, RingHom.mapMatrix_apply, map_apply, RingHom.mapMatrix_apply, this, ←
    map_updateRow, ← RingHom.mapMatrix_apply, ← RingHom.map_det, ← adjugate_apply]
-- 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
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))
a :
  Eq.{u_2 + 1} (α := S) ((f.mapMatrix : (a : Matrix n n R) → Matrix n n S) M.adjugate i k : S)
    (det (updateRow ((f.mapMatrix : (a : Matrix n n R) → Matrix n n S) M) k (Pi.single (M := fun (a : n) ↦ S) i 1)) : S)
a₁ :
  Eq.{u_2 + 1} (α := S) (M.adjugate.map (⇑f : (a : R) → S) i k)
    (det (updateRow ((f.mapMatrix : (a : Matrix n n R) → Matrix n n S) M) k (Pi.single (M := fun (a : n) ↦ S) i 1)))
a₂ :
  Eq.{u_2 + 1} (α := S) ((f : (a : R) → S) (M.adjugate i k) : S)
    (det (updateRow ((f.mapMatrix : (a : Matrix n n R) → Matrix n n S) M) k (Pi.single (M := fun (a : n) ↦ S) i 1)) : S)
a₃ :
  Eq.{u_2 + 1} (α := S) ((f : (a : R) → S) (M.adjugate i k) : S)
    (det (updateRow (M.map (⇑f : (a : R) → S)) k (Pi.single (M := fun (a : n) ↦ S) i 1)) : S)
a₄ :
  Eq.{u_2 + 1} (α := S) ((f : (a : R) → S) (M.adjugate i k) : S)
    (det
        (updateRow (M.map (⇑f : (a : R) → S)) k
          (Function.comp.{v + 1, u_1 + 1, u_2 + 1} (β := R) (⇑f : (a : R) → S)
            (Pi.single (M := fun (a : n) ↦ R) i 1))) :
      S)
a₅ :
  Eq.{u_2 + 1} (α := S) ((f : (a : R) → S) (M.adjugate i k) : S)
    (det ((M.updateRow k (Pi.single (M := fun (a : n) ↦ R) i 1)).map (⇑f : (a : R) → S)) : S)
a₆ :
  Eq.{u_2 + 1} (α := S) ((f : (a : R) → S) (M.adjugate i k) : S)
    (det.{u_2, v} (n := n)
        ((f.mapMatrix : (a : Matrix n n R) → Matrix n n S) (M.updateRow k (Pi.single (M := fun (a : n) ↦ R) i 1))) :
      S)
a₇ :
  Eq.{u_2 + 1} (α := S) ((f : (a : R) → S) (M.adjugate i k) : S)
    ((f : (a : R) → S) (M.updateRow k (Pi.single (M := fun (a : n) ↦ R) i 1)).det : S)
⊢ 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 a₈ : Eq.{u_2 + 1} (α := S) ((f : (a : R) → S) (M.adjugate i k) : S) ((f : (a : R) → S) (M.adjugate i k) : S)
Tactic: rw [adjugate_apply, RingHom.mapMatrix_apply, map_apply, RingHom.mapMatrix_apply, this, ←
    map_updateRow, ← RingHom.mapMatrix_apply, ← RingHom.map_det, ← adjugate_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 α
A : Matrix n n α
⊢ A.adjugate.det = A.det ^ (Fintype.card n - 1)
have inl : ∀ (h_card : Fintype.card n = 0), A.adjugate.det = A.det ^ (Fintype.card n - 1)
Tactic: rcases (Fintype.card n).eq_zero_or_pos with h_card | h_card
-- 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 α
inl : ∀ (h_card : Fintype.card n = 0), A.adjugate.det = A.det ^ (Fintype.card n - 1)
⊢ A.adjugate.det = A.det ^ (Fintype.card n - 1)
have inr : ∀ (h_card : Fintype.card n > 0), A.adjugate.det = A.det ^ (Fintype.card n - 1)
Tactic: rcases (Fintype.card n).eq_zero_or_pos with h_card | h_card
-- 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 α
h_card : Fintype.card n = 0
⊢ A.adjugate.det = A.det ^ (Fintype.card n - 1)
have this : IsEmpty n
Tactic: haveI : IsEmpty n := Fintype.card_eq_zero_iff.mp h_card
-- 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 α
h_card : Fintype.card n = 0
this : IsEmpty n
⊢ A.adjugate.det = A.det ^ (Fintype.card n - 1)
have inl : A.adjugate.det = A.det ^ HSub.hSub (α := ℕ) 0 1
Tactic: rw [h_card, Nat.zero_sub, pow_zero, adjugate_subsingleton, det_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 α
h_card : Fintype.card n = 0
this : IsEmpty n
inl : A.adjugate.det = A.det ^ HSub.hSub (α := ℕ) 0 1
inl₁ : A.adjugate.det = HPow.hPow (β := ℕ) A.det 0
⊢ A.adjugate.det = A.det ^ (Fintype.card n - 1)
have inl₂ : A.adjugate.det = 1
Tactic: rw [h_card, Nat.zero_sub, pow_zero, adjugate_subsingleton, det_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 α
h_card : Fintype.card n = 0
this : IsEmpty n
inl : A.adjugate.det = A.det ^ HSub.hSub (α := ℕ) 0 1
inl₁ : A.adjugate.det = HPow.hPow (β := ℕ) A.det 0
inl₂ : A.adjugate.det = 1
⊢ A.adjugate.det = A.det ^ (Fintype.card n - 1)
have inl₃ : Eq.{w + 1} (α := α) (det.{w, v} (n := n) 1) 1
Tactic: rw [h_card, Nat.zero_sub, pow_zero, adjugate_subsingleton, det_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 α
h_card : Fintype.card n = 0
this : IsEmpty n
inl : A.adjugate.det = A.det ^ HSub.hSub (α := ℕ) 0 1
inl₁ : A.adjugate.det = HPow.hPow (β := ℕ) A.det 0
inl₂ : A.adjugate.det = 1
inl₃ : Eq.{w + 1} (α := α) (det.{w, v} (n := n) 1) 1
⊢ A.adjugate.det = A.det ^ (Fintype.card n - 1)
have inl₄ : Eq.{w + 1} (α := α) 1 1
Tactic: rw [h_card, Nat.zero_sub, pow_zero, adjugate_subsingleton, det_one]
-- 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 α
h_card : Fintype.card n > 0
⊢ A.adjugate.det = A.det ^ (Fintype.card n - 1)
have h_card₁ : Fintype.card n - Nat.succ 0 + Nat.succ 0 = Fintype.card n
Tactic: replace h_card := tsub_add_cancel_of_le h_card.nat_succ_le
Cleared hypotheses: h_card
-- 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 α
h_card : Fintype.card n - Nat.succ 0 + Nat.succ 0 = Fintype.card n
A' : Matrix n n (MvPolynomial (n × n) ℤ) := mvPolynomialX n n ℤ
this : A'.adjugate.det = A'.det ^ (Fintype.card n - 1)
⊢ A.adjugate.det = A.det ^ (Fintype.card n - 1)
have rw : det.{w, v} (n := n)
    (adjugate
      ((AlgHom.mapMatrix (MvPolynomial.aeval.{0, w, v} (R := ℤ) (S₁ := α) fun (p : n × n) ↦ A p.1 p.2) :
          (a : Matrix n n (MvPolynomial (n × n) ℤ)) → Matrix n n α)
        (mvPolynomialX n n ℤ))) =
  HPow.hPow (α := α)
    (det.{w, v} (n := n)
      ((AlgHom.mapMatrix (MvPolynomial.aeval.{0, w, v} (R := ℤ) (S₁ := α) fun (p : n × n) ↦ A p.1 p.2) :
          (a : Matrix n n (MvPolynomial (n × n) ℤ)) → Matrix n n α)
        (mvPolynomialX n n ℤ)))
    (Fintype.card n - 1)
Tactic: rw [← mvPolynomialX_mapMatrix_aeval ℤ A, ← AlgHom.map_adjugate, ← AlgHom.map_det, ←
      AlgHom.map_det, ← map_pow, 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 α
h_card : Fintype.card n - Nat.succ 0 + Nat.succ 0 = Fintype.card n
A' : Matrix n n (MvPolynomial (n × n) ℤ) := mvPolynomialX n n ℤ
this : A'.adjugate.det = A'.det ^ (Fintype.card n - 1)
rw :
  det.{w, v} (n := n)
      (adjugate
        ((AlgHom.mapMatrix (MvPolynomial.aeval.{0, w, v} (R := ℤ) (S₁ := α) fun (p : n × n) ↦ A p.1 p.2) :
            (a : Matrix n n (MvPolynomial (n × n) ℤ)) → Matrix n n α)
          (mvPolynomialX n n ℤ))) =
    HPow.hPow (α := α)
      (det.{w, v} (n := n)
        ((AlgHom.mapMatrix (MvPolynomial.aeval.{0, w, v} (R := ℤ) (S₁ := α) fun (p : n × n) ↦ A p.1 p.2) :
            (a : Matrix n n (MvPolynomial (n × n) ℤ)) → Matrix n n α)
          (mvPolynomialX n n ℤ)))
      (Fintype.card n - 1)
⊢ A.adjugate.det = A.det ^ (Fintype.card n - 1)
have rw₁ : det.{w, v} (n := n)
    ((AlgHom.mapMatrix (MvPolynomial.aeval.{0, w, v} (R := ℤ) (S₁ := α) fun (p : n × n) ↦ A p.1 p.2) :
        (a : Matrix n n (MvPolynomial (n × n) ℤ)) → Matrix n n α)
      (adjugate (mvPolynomialX n n ℤ))) =
  HPow.hPow (α := α)
    (det.{w, v} (n := n)
      ((AlgHom.mapMatrix (MvPolynomial.aeval.{0, w, v} (R := ℤ) (S₁ := α) fun (p : n × n) ↦ A p.1 p.2) :
          (a : Matrix n n (MvPolynomial (n × n) ℤ)) → Matrix n n α)
        (mvPolynomialX n n ℤ)))
    (Fintype.card n - 1)
Tactic: rw [← mvPolynomialX_mapMatrix_aeval ℤ A, ← AlgHom.map_adjugate, ← AlgHom.map_det, ←
      AlgHom.map_det, ← map_pow, 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 α
h_card : Fintype.card n - Nat.succ 0 + Nat.succ 0 = Fintype.card n
A' : Matrix n n (MvPolynomial (n × n) ℤ) := mvPolynomialX n n ℤ
this : A'.adjugate.det = A'.det ^ (Fintype.card n - 1)
rw :
  det.{w, v} (n := n)
      (adjugate
        ((AlgHom.mapMatrix (MvPolynomial.aeval.{0, w, v} (R := ℤ) (S₁ := α) fun (p : n × n) ↦ A p.1 p.2) :
            (a : Matrix n n (MvPolynomial (n × n) ℤ)) → Matrix n n α)
          (mvPolynomialX n n ℤ))) =
    HPow.hPow (α := α)
      (det.{w, v} (n := n)
        ((AlgHom.mapMatrix (MvPolynomial.aeval.{0, w, v} (R := ℤ) (S₁ := α) fun (p : n × n) ↦ A p.1 p.2) :
            (a : Matrix n n (MvPolynomial (n × n) ℤ)) → Matrix n n α)
          (mvPolynomialX n n ℤ)))
      (Fintype.card n - 1)
rw₁ :
  det.{w, v} (n := n)
      ((AlgHom.mapMatrix (MvPolynomial.aeval.{0, w, v} (R := ℤ) (S₁ := α) fun (p : n × n) ↦ A p.1 p.2) :
          (a : Matrix n n (MvPolynomial (n × n) ℤ)) → Matrix n n α)
        (adjugate (mvPolynomialX n n ℤ))) =
    HPow.hPow (α := α)
      (det.{w, v} (n := n)
        ((AlgHom.mapMatrix (MvPolynomial.aeval.{0, w, v} (R := ℤ) (S₁ := α) fun (p : n × n) ↦ A p.1 p.2) :
            (a : Matrix n n (MvPolynomial (n × n) ℤ)) → Matrix n n α)
          (mvPolynomialX n n ℤ)))
      (Fintype.card n - 1)
⊢ A.adjugate.det = A.det ^ (Fintype.card n - 1)
have rw₂ : ((MvPolynomial.aeval.{0, w, v} (R := ℤ) (S₁ := α) fun (p : n × n) ↦ A p.1 p.2 :
        AlgHom.{0, v, w} ℤ (MvPolynomial (n × n) ℤ) α) :
      (a : MvPolynomial (n × n) ℤ) → α)
    (det (adjugate (mvPolynomialX n n ℤ))) =
  HPow.hPow (α := α)
    (det.{w, v} (n := n)
      ((AlgHom.mapMatrix (MvPolynomial.aeval.{0, w, v} (R := ℤ) (S₁ := α) fun (p : n × n) ↦ A p.1 p.2) :
          (a : Matrix n n (MvPolynomial (n × n) ℤ)) → Matrix n n α)
        (mvPolynomialX n n ℤ)))
    (Fintype.card n - 1)
Tactic: rw [← mvPolynomialX_mapMatrix_aeval ℤ A, ← AlgHom.map_adjugate, ← AlgHom.map_det, ←
      AlgHom.map_det, ← map_pow, this]