awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : ∀ (k : n), (diagonal v).updateCol j (Pi.single (M := fun (a : n) ↦ α) i 1) j k = 0
⊢ ((diagonal v).updateCol j (Pi.single (M := fun (a : n) ↦ α) i 1)).det = 0

Tactic:
refine det_eq_zero_of_row_eq_zero j fun k => ?_

Premises used: Matrix.det_eq_zero_of_row_eq_zero
-- 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
k : n
a : ∀ (hij : i ≠ k), (diagonal v).updateCol k (Pi.single (M := fun (a : n) ↦ α) i 1) k k = 0
a₁ : ∀ (hjk : k ≠ j), (diagonal v).updateCol j (Pi.single (M := fun (a : n) ↦ α) i 1) j k = 0
⊢ (diagonal v).updateCol j (Pi.single (M := fun (a : n) ↦ α) i 1) j k = 0

Tactic:
obtain rfl | hjk := eq_or_ne k 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 k : n
hij : i ≠ k
a : Eq.{w + 1} (α := α) (Pi.single (M := fun (a : n) ↦ α) i 1 k : α) (0 : α)
a₁ a₂ : Eq.{w + 1} (α := α) 0 0
⊢ (diagonal v).updateCol k (Pi.single (M := fun (a : n) ↦ α) i 1) k k = 0

Tactic:
rw [updateCol_self, Pi.single_eq_of_ne' hij]

Premises used: Matrix.updateCol_self, Pi.single_eq_of_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
k : n
hjk : k ≠ j
a : diagonal v j k = 0
a₁ a₂ : Eq.{w + 1} (α := α) 0 0
⊢ (diagonal v).updateCol j (Pi.single (M := fun (a : n) ↦ α) i 1) j k = 0

Tactic:
rw [updateCol_ne hjk, diagonal_apply_ne' _ hjk]

Premises used: Matrix.diagonal_apply_ne', Matrix.updateCol_ne
-- Module: Mathlib.LinearAlgebra.Matrix.Adjugate
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
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)
⊢ 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)

Tactic:
ext i k
-- Module: Mathlib.LinearAlgebra.Matrix.Adjugate
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
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))
⊢ 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:
rw [← f.map_one]

Premises used: RingHom.map_one
-- Module: Mathlib.LinearAlgebra.Matrix.Adjugate
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 ((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:
Pi.single_op (fun _ => f) (fun _ => f.map_zero) i (1 : R)

Premises used: RingHom.map_zero, Pi.single_op, OfNat.ofNat, DFunLike.coe
-- Module: Mathlib.LinearAlgebra.Matrix.Adjugate
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 ((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:
exact Pi.single_op (fun _ => f) (fun _ => f.map_zero) i (1 : R)

Premises used: RingHom.map_zero, Pi.single_op, OfNat.ofNat, DFunLike.coe
-- Module: Mathlib.LinearAlgebra.Matrix.Adjugate
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))

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)
-- Module: Mathlib.LinearAlgebra.Matrix.Adjugate
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)
a₈ a₉ : Eq.{u_2 + 1} (α := S) ((f : (a : R) → S) (M.adjugate i k) : S) ((f : (a : R) → S) (M.adjugate i k) : 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)

Tactic:
rw [adjugate_apply, RingHom.mapMatrix_apply, map_apply, RingHom.mapMatrix_apply, this, ←
    map_updateRow, ← RingHom.mapMatrix_apply, ← RingHom.map_det, ← adjugate_apply]

Premises used: RingHom.mapMatrix_apply, Matrix.map_updateRow, Matrix.map_apply, Matrix.adjugate_apply, RingHom.map_det
-- Module: Mathlib.LinearAlgebra.Matrix.Adjugate
Goal:
n : Type v
inst : DecidableEq n
inst_1 : Fintype n
R : Type u_1
A : Type u_2
B : Type u_3
inst_2 : CommSemiring R
inst_3 : CommRing A
inst_4 : CommRing B
inst_5 : Algebra R A
inst_6 : Algebra R B
f : A →ₐ[R] B
M : Matrix n n A
⊢ Eq (α := Matrix n n B) ((f.mapMatrix : (a : Matrix n n A) → Matrix n n B) M.adjugate : Matrix n n B)
    (adjugate ((f.mapMatrix : (a : Matrix n n A) → Matrix n n B) M) : Matrix n n B)

Tactic:
f.toRingHom.map_adjugate _

Premises used: RingHom.map_adjugate, AlgHom.toRingHom
-- 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 α
inl : ∀ (h_card : Fintype.card n = 0), A.adjugate.det = A.det ^ (Fintype.card n - 1)
inr : ∀ (h_card : Fintype.card n > 0), A.adjugate.det = A.det ^ (Fintype.card n - 1)
⊢ A.adjugate.det = A.det ^ (Fintype.card n - 1)

Tactic:
rcases (Fintype.card n).eq_zero_or_pos with h_card | h_card

Premises used: Fintype.card, Nat.eq_zero_or_pos
-- 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_card : Fintype.card n = 0
⊢ IsEmpty n

Tactic:
haveI : IsEmpty n := Fintype.card_eq_zero_iff.mp h_card
-- 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_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
inl₄ inl₅ : Eq.{w + 1} (α := α) 1 1
⊢ A.adjugate.det = A.det ^ (Fintype.card n - 1)

Tactic:
rw [h_card, Nat.zero_sub, pow_zero, adjugate_subsingleton, det_one]

Premises used: Nat.zero_sub, pow_zero, Matrix.adjugate_subsingleton, Matrix.det_one
-- 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_card : Fintype.card n > 0
⊢ 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
-- 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_card : Fintype.card n - Nat.succ 0 + Nat.succ 0 = Fintype.card n
A' : Matrix n n (MvPolynomial (n × n) ℤ) := mvPolynomialX n n ℤ
inr : A'.adjugate.det = A'.det ^ (Fintype.card n - 1)
⊢ A.adjugate.det = A.det ^ (Fintype.card n - 1)

Tactic:
suffices A'.adjugate.det = A'.det ^ (Fintype.card n - 1) by
    rw [← mvPolynomialX_mapMatrix_aeval ℤ A, ← AlgHom.map_adjugate, ← AlgHom.map_det, ←
      AlgHom.map_det, ← map_pow, 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 α
h_card : Fintype.card n - Nat.succ 0 + Nat.succ 0 = Fintype.card n
A' : Matrix n n (MvPolynomial (n × n) ℤ) := mvPolynomialX n n ℤ
inr : A'.det * A'.adjugate.det = A'.det * A'.det ^ (Fintype.card n - 1)
⊢ A'.adjugate.det = A'.det ^ (Fintype.card n - 1)

Tactic:
apply mul_left_cancel₀ (show A'.det ≠ 0 from det_mvPolynomialX_ne_zero n ℤ)

Premises used: Matrix.det_mvPolynomialX_ne_zero, Int, mul_left_cancel₀
-- 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_card : Fintype.card n - Nat.succ 0 + Nat.succ 0 = Fintype.card n
A' : Matrix n n (MvPolynomial (n × n) ℤ) := mvPolynomialX n n ℤ
⊢ A'.det * A'.adjugate.det = (A' * A'.adjugate).det

Tactic:
(det_mul _ _).symm

Premises used: Matrix.det_mul, Eq.symm
-- 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_card : Fintype.card n - Nat.succ 0 + Nat.succ 0 = Fintype.card n
A' : Matrix n n (MvPolynomial (n × n) ℤ) := mvPolynomialX n n ℤ
rw : (HSMul.hSMul (β := Matrix n n (MvPolynomial (n × n) ℤ)) A'.det 1).det = A'.det ^ Fintype.card n
rw₁ : A'.det ^ Fintype.card n * det (n := n) 1 = A'.det ^ Fintype.card n
rw₂ : A'.det ^ Fintype.card n * 1 = A'.det ^ Fintype.card n
rw₃ rw₄ : A'.det ^ Fintype.card n = A'.det ^ Fintype.card n
⊢ (A' * A'.adjugate).det = A'.det ^ Fintype.card n

Tactic:
rw [mul_adjugate A', det_smul, det_one, mul_one]

Premises used: Matrix.det_smul, Matrix.det_one, mul_one, Matrix.mul_adjugate
-- 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_card : Fintype.card n - Nat.succ 0 + Nat.succ 0 = Fintype.card n
A' : Matrix n n (MvPolynomial (n × n) ℤ) := mvPolynomialX n n ℤ
rw : A'.det ^ Fintype.card n = A'.det ^ (Fintype.card n - 1 + 1)
rw₁ rw₂ : A'.det ^ Fintype.card n = A'.det ^ Fintype.card n
⊢ A'.det ^ Fintype.card n = A'.det * A'.det ^ (Fintype.card n - 1)

Tactic:
rw [← pow_succ', h_card]

Premises used: pow_succ'
-- 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_card : Fintype.card n - Nat.succ 0 + Nat.succ 0 = Fintype.card n
A' : Matrix n n (MvPolynomial (n × n) ℤ) := mvPolynomialX n n ℤ
adjugate : (A' * A'.adjugate).det = A'.det ^ Fintype.card n
adjugate₁ : A'.det ^ Fintype.card n = A'.det * A'.det ^ (Fintype.card n - 1)
⊢ A'.det * A'.adjugate.det = A'.det * A'.det ^ (Fintype.card n - 1)

Tactic:
calc
    A'.det * A'.adjugate.det = (A' * adjugate A').det := (det_mul _ _).symm
    _ = A'.det ^ Fintype.card n := by rw [mul_adjugate A', det_smul, det_one, mul_one]
    _ = A'.det * A'.det ^ (Fintype.card n - 1) := by rw [← pow_succ', h_card]

Premises used: HMul.hMul, HSub.hSub, Fintype.card, Matrix.det_mul, Matrix.adjugate, OfNat.ofNat, Eq.symm, Matrix.det
-- Module: Mathlib.LinearAlgebra.Matrix.Adjugate
Goal:
α : Type w
inst : CommRing α
A : Matrix (Fin 0) (Fin 0) α
⊢ A.adjugate = 0

Tactic:
Subsingleton.elim _ _

Premises used: Subsingleton.elim
-- Module: Mathlib.LinearAlgebra.Matrix.Adjugate
Goal:
α : Type w
inst : CommRing α
A : Matrix (Fin 1) (Fin 1) α
⊢ A.adjugate = 1

Tactic:
adjugate_subsingleton A

Premises used: Matrix.adjugate_subsingleton
-- Module: Mathlib.LinearAlgebra.Matrix.Adjugate
Goal:
α : Type w
inst : CommRing α
n : ℕ
A : Matrix (Fin n.succ) (Fin n.succ) α
i j : Fin n.succ
simp_rw :
  ∑ x : Fin n.succ,
      HMul.hMul (β := α) (HPow.hPow (α := α) (-1) ((↑j : ℕ) + (↑x : ℕ)))
          (Pi.single (M := fun (a : Fin n.succ) ↦ α) i 1 x : α) *
        (A.submatrix j.succAbove x.succAbove).det =
    HPow.hPow (α := α) (-1) ((↑j : ℕ) + (↑i : ℕ)) * (A.submatrix j.succAbove i.succAbove).det
⊢ A.adjugate i j = HPow.hPow (α := α) (-1) ((↑j : ℕ) + (↑i : ℕ)) * (A.submatrix j.succAbove i.succAbove).det

Tactic:
simp_rw [adjugate_apply, det_succ_row _ j, updateRow_self, submatrix_updateRow_succAbove]

Premises used: Matrix.det_succ_row, Matrix.submatrix_updateRow_succAbove, Matrix.adjugate_apply, Matrix.updateRow_self
-- Module: Mathlib.LinearAlgebra.Matrix.Adjugate
Goal:
α : Type w
inst : CommRing α
n : ℕ
A : Matrix (Fin n.succ) (Fin n.succ) α
i j : Fin n.succ
rw :
  ∀ (h : Fin n.succ) (hjk : h ≠ i),
    HMul.hMul (β := α) (HPow.hPow (α := α) (-1) ((↑j : ℕ) + (↑h : ℕ)))
          (Pi.single (M := fun (a : Fin n.succ) ↦ α) i 1 h : α) *
        (A.submatrix j.succAbove h.succAbove).det =
      0
⊢ ∑ x : Fin n.succ,
      HMul.hMul (β := α) (HPow.hPow (α := α) (-1) ((↑j : ℕ) + (↑x : ℕ)))
          (Pi.single (M := fun (a : Fin n.succ) ↦ α) i 1 x : α) *
        (A.submatrix j.succAbove x.succAbove).det =
    HPow.hPow (α := α) (-1) ((↑j : ℕ) + (↑i : ℕ)) * (A.submatrix j.succAbove i.succAbove).det

Tactic:
rw [Fintype.sum_eq_single i fun h hjk => ?_, Pi.single_eq_same, mul_one]

Premises used: mul_one, Pi.single_eq_same, Fintype.sum_eq_single
-- Module: Mathlib.LinearAlgebra.Matrix.Adjugate
Goal:
α : Type w
inst : CommRing α
n : ℕ
A : Matrix (Fin n.succ) (Fin n.succ) α
i j h : Fin n.succ
hjk : h ≠ i
rw : HPow.hPow (α := α) (-1) ((↑j : ℕ) + (↑h : ℕ)) * 0 * (A.submatrix j.succAbove h.succAbove).det = 0
rw₁ : 0 * (A.submatrix j.succAbove h.succAbove).det = 0
rw₂ rw₃ : Eq.{w + 1} (α := α) 0 0
⊢ HMul.hMul (β := α) (HPow.hPow (α := α) (-1) ((↑j : ℕ) + (↑h : ℕ)))
        (Pi.single (M := fun (a : Fin n.succ) ↦ α) i 1 h : α) *
      (A.submatrix j.succAbove h.succAbove).det =
    0

Tactic:
rw [Pi.single_eq_of_ne hjk, mul_zero, zero_mul]

Premises used: MulZeroClass.zero_mul, Pi.single_eq_of_ne, MulZeroClass.mul_zero
-- Module: Mathlib.LinearAlgebra.Matrix.Adjugate
Goal:
α : Type w
inst : CommRing α
A : Matrix (Fin 2) (Fin 2) α
a : ∀ (i j : Fin 2), A.adjugate i j = !![A 1 1, -A 0 1; -A 1 0, A 0 0] i j
⊢ A.adjugate = !![A 1 1, -A 0 1; -A 1 0, A 0 0]

Tactic:
ext i j
-- Module: Mathlib.LinearAlgebra.Matrix.Adjugate
Goal:
α : Type w
inst : CommRing α
A : Matrix (Fin 2) (Fin 2) α
i j : Fin 2
a :
  HPow.hPow (α := α) (-1) ((↑j : ℕ) + (↑i : ℕ)) * (A.submatrix j.succAbove i.succAbove).det =
    !![A 1 1, -A 0 1; -A 1 0, A 0 0] i j
⊢ A.adjugate i j = !![A 1 1, -A 0 1; -A 1 0, A 0 0] i j

Tactic:
rw [adjugate_fin_succ_eq_det_submatrix]

Premises used: Matrix.adjugate_fin_succ_eq_det_submatrix
-- Module: Mathlib.LinearAlgebra.Matrix.Adjugate
Goal:
α : Type w
inst : CommRing α
A : Matrix (Fin 2) (Fin 2) α
i j : Fin 2
a :
  HPow.hPow (α := α) (-1) ((↑j : ℕ) + (↑((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2)) : ℕ)) *
      (A.submatrix j.succAbove (Fin.succAbove ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2)))).det =
    !![A 1 1, -A 0 1; -A 1 0, A 0 0] ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) j
a₁ :
  HPow.hPow (α := α) (-1) ((↑j : ℕ) + (↑((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2)) : ℕ)) *
      (A.submatrix j.succAbove (Fin.succAbove ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2)))).det =
    !![A 1 1, -A 0 1; -A 1 0, A 0 0] ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) j
⊢ HPow.hPow (α := α) (-1) ((↑j : ℕ) + (↑i : ℕ)) * (A.submatrix j.succAbove i.succAbove).det =
    !![A 1 1, -A 0 1; -A 1 0, A 0 0] i j

Tactic:
fin_cases i
-- Module: Mathlib.LinearAlgebra.Matrix.Adjugate
Goal:
α : Type w
inst : CommRing α
A : Matrix (Fin 2) (Fin 2) α
j : Fin 2
a :
  HPow.hPow (α := α) (-1)
        ((↑((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2)) : ℕ) + (↑((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2)) : ℕ)) *
      (A.submatrix (Fin.succAbove ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2)))
          (Fin.succAbove ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2)))).det =
    !![A 1 1, -A 0 1; -A 1 0, A 0 0] ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩)
a₁ :
  HPow.hPow (α := α) (-1)
        ((↑((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2)) : ℕ) + (↑((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2)) : ℕ)) *
      (A.submatrix (Fin.succAbove ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2)))
          (Fin.succAbove ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2)))).det =
    !![A 1 1, -A 0 1; -A 1 0, A 0 0] ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩)
⊢ HPow.hPow (α := α) (-1) ((↑j : ℕ) + (↑((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2)) : ℕ)) *
      (A.submatrix j.succAbove (Fin.succAbove ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2)))).det =
    !![A 1 1, -A 0 1; -A 1 0, A 0 0] ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) j

Tactic:
fin_cases j
-- Module: Mathlib.LinearAlgebra.Matrix.Adjugate
Goal:
α : Type w
inst : CommRing α
A : Matrix (Fin 2) (Fin 2) α
j : Fin 2
a :
  HPow.hPow (α := α) (-1)
        ((↑((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2)) : ℕ) + (↑((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2)) : ℕ)) *
      (A.submatrix (Fin.succAbove ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2)))
          (Fin.succAbove ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2)))).det =
    !![A 1 1, -A 0 1; -A 1 0, A 0 0] ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩)
a₁ :
  HPow.hPow (α := α) (-1)
        ((↑((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2)) : ℕ) + (↑((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2)) : ℕ)) *
      (A.submatrix (Fin.succAbove ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2)))
          (Fin.succAbove ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2)))).det =
    !![A 1 1, -A 0 1; -A 1 0, A 0 0] ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩)
⊢ HPow.hPow (α := α) (-1) ((↑j : ℕ) + (↑((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2)) : ℕ)) *
      (A.submatrix j.succAbove (Fin.succAbove ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2)))).det =
    !![A 1 1, -A 0 1; -A 1 0, A 0 0] ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) j

Tactic:
fin_cases j
-- Module: Mathlib.LinearAlgebra.Matrix.Adjugate
Goal:
α : Type w
inst : CommRing α
A : Matrix (Fin 2) (Fin 2) α
⊢ HPow.hPow (α := α) (-1)
        ((↑((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2)) : ℕ) + (↑((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2)) : ℕ)) *
      (A.submatrix (Fin.succAbove ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2)))
          (Fin.succAbove ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2)))).det =
    !![A 1 1, -A 0 1; -A 1 0, A 0 0] ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Matrix.Adjugate
Goal:
α : Type w
inst : CommRing α
A : Matrix (Fin 2) (Fin 2) α
⊢ HPow.hPow (α := α) (-1)
        ((↑((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2)) : ℕ) + (↑((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2)) : ℕ)) *
      (A.submatrix (Fin.succAbove ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2)))
          (Fin.succAbove ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2)))).det =
    !![A 1 1, -A 0 1; -A 1 0, A 0 0] ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Matrix.Adjugate
Goal:
α : Type w
inst : CommRing α
A : Matrix (Fin 2) (Fin 2) α
⊢ HPow.hPow (α := α) (-1)
        ((↑((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2)) : ℕ) + (↑((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2)) : ℕ)) *
      (A.submatrix (Fin.succAbove ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2)))
          (Fin.succAbove ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2)))).det =
    !![A 1 1, -A 0 1; -A 1 0, A 0 0] ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Matrix.Adjugate
Goal:
α : Type w
inst : CommRing α
A : Matrix (Fin 2) (Fin 2) α
⊢ HPow.hPow (α := α) (-1)
        ((↑((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2)) : ℕ) + (↑((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2)) : ℕ)) *
      (A.submatrix (Fin.succAbove ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2)))
          (Fin.succAbove ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2)))).det =
    !![A 1 1, -A 0 1; -A 1 0, A 0 0] ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Matrix.Adjugate
Goal:
α : Type w
inst : CommRing α
a b c d : α
⊢ Eq.{w + 1} (α := Matrix (Fin 2) (Fin 2) α) (adjugate !![a, b; c, d]) !![d, -b; -c, a]

Tactic:
adjugate_fin_two _

Premises used: Eq.mpr, Matrix.adjugate_fin_two, Fin.cons, Fin.induction.go, Fin.induction, Fin.cases, Matrix.vecCons
-- Module: Mathlib.LinearAlgebra.Matrix.Adjugate
Goal:
α : Type w
inst : CommRing α
A : Matrix (Fin 3) (Fin 3) α
a :
  ∀ (i j : Fin 3),
    A.adjugate i j =
      !![A 1 1 * A 2 2 - A 1 2 * A 2 1, -(A 0 1 * A 2 2) + A 0 2 * A 2 1, A 0 1 * A 1 2 - A 0 2 * A 1 1;
          -(A 1 0 * A 2 2) + A 1 2 * A 2 0, A 0 0 * A 2 2 - A 0 2 * A 2 0, -(A 0 0 * A 1 2) + A 0 2 * A 1 0;
          A 1 0 * A 2 1 - A 1 1 * A 2 0, -(A 0 0 * A 2 1) + A 0 1 * A 2 0, A 0 0 * A 1 1 - A 0 1 * A 1 0]
        i j
⊢ A.adjugate =
    !![A 1 1 * A 2 2 - A 1 2 * A 2 1, -(A 0 1 * A 2 2) + A 0 2 * A 2 1, A 0 1 * A 1 2 - A 0 2 * A 1 1;
      -(A 1 0 * A 2 2) + A 1 2 * A 2 0, A 0 0 * A 2 2 - A 0 2 * A 2 0, -(A 0 0 * A 1 2) + A 0 2 * A 1 0;
      A 1 0 * A 2 1 - A 1 1 * A 2 0, -(A 0 0 * A 2 1) + A 0 1 * A 2 0, A 0 0 * A 1 1 - A 0 1 * A 1 0]

Tactic:
ext i j
-- Module: Mathlib.LinearAlgebra.Matrix.Adjugate
Goal:
α : Type w
inst : CommRing α
A : Matrix (Fin 3) (Fin 3) α
i j : Fin 3
a :
  HPow.hPow (α := α) (-1) ((↑j : ℕ) + (↑i : ℕ)) *
      (A.submatrix j.succAbove i.succAbove 0 0 * A.submatrix j.succAbove i.succAbove 1 1 -
        A.submatrix j.succAbove i.succAbove 0 1 * A.submatrix j.succAbove i.succAbove 1 0) =
    !![A 1 1 * A 2 2 - A 1 2 * A 2 1, -(A 0 1 * A 2 2) + A 0 2 * A 2 1, A 0 1 * A 1 2 - A 0 2 * A 1 1;
        -(A 1 0 * A 2 2) + A 1 2 * A 2 0, A 0 0 * A 2 2 - A 0 2 * A 2 0, -(A 0 0 * A 1 2) + A 0 2 * A 1 0;
        A 1 0 * A 2 1 - A 1 1 * A 2 0, -(A 0 0 * A 2 1) + A 0 1 * A 2 0, A 0 0 * A 1 1 - A 0 1 * A 1 0]
      i j
⊢ A.adjugate i j =
    !![A 1 1 * A 2 2 - A 1 2 * A 2 1, -(A 0 1 * A 2 2) + A 0 2 * A 2 1, A 0 1 * A 1 2 - A 0 2 * A 1 1;
        -(A 1 0 * A 2 2) + A 1 2 * A 2 0, A 0 0 * A 2 2 - A 0 2 * A 2 0, -(A 0 0 * A 1 2) + A 0 2 * A 1 0;
        A 1 0 * A 2 1 - A 1 1 * A 2 0, -(A 0 0 * A 2 1) + A 0 1 * A 2 0, A 0 0 * A 1 1 - A 0 1 * A 1 0]
      i j

Tactic:
rw [adjugate_fin_succ_eq_det_submatrix, det_fin_two]

Premises used: Matrix.adjugate_fin_succ_eq_det_submatrix, Matrix.det_fin_two