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 α
A : Matrix n n α
β : Type u_1
s : Finset β
f : n → β → α
i : n
rw :
  (A.updateCol i (∑ x ∈ s, fun (j : n) ↦ f j x)).det = (A.cramer : (a : n → α) → n → α) (fun (j : n) ↦ ∑ x ∈ s, f j x) i
⊢ Eq.{w + 1} (α := α) ((∑ x ∈ s, (A.cramer : (a : n → α) → n → α) fun (j : n) ↦ f j x) i : α)
    ((A.cramer : (a : n → α) → n → α) (fun (j : n) ↦ ∑ x ∈ s, f j x) i : α)

Tactic:
rw [sum_cramer, cramer_apply]

Premises used: Matrix.sum_cramer, Matrix.cramer_apply
-- Module: Mathlib.LinearAlgebra.Matrix.Adjugate
Goal:
n : Type v
α : Type w
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : CommRing α
A : Matrix n n α
β : Type u_1
s : Finset β
f : n → β → α
i : n
e_M : ∀ (j : n), Eq.{w + 1} (α := α) ((∑ x ∈ s, fun (j : n) ↦ f j x) j) (∑ x ∈ s, f j x)
⊢ (A.updateCol i (∑ x ∈ s, fun (j : n) ↦ f j x)).det = (A.cramer : (a : n → α) → n → α) (fun (j : n) ↦ ∑ x ∈ s, f j x) i

Tactic:
congr with j
-- Module: Mathlib.LinearAlgebra.Matrix.Adjugate
Goal:
n : Type v
α : Type w
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : CommRing α
A : Matrix n n α
β : Type u_1
s : Finset β
f : n → β → α
i j : n
⊢ Eq.{w + 1} (α := α) ((∑ x ∈ s, fun (j : n) ↦ f j x) j) (∑ x ∈ s, f j x)

Tactic:
apply Finset.sum_apply

Premises used: Finset.sum_apply
-- Module: Mathlib.LinearAlgebra.Matrix.Adjugate
Goal:
m : Type u
n : Type v
α : Type w
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : DecidableEq m
inst_3 : Fintype m
inst_4 : CommRing α
A : Matrix m m α
e : n ≃ m
b : n → α
h :
  ∀ (i : n),
    Eq.{w + 1} (α := α) ((cramer (A.submatrix (⇑e : (a : n) → m) (⇑e : (a : n) → m)) : (a : n → α) → n → α) b i : α)
      (Function.comp.{v + 1, u + 1, w + 1} (β := m) ((A.cramer : (a : m → α) → m → α) (b ∘ (⇑e.symm : (a : m) → n)))
          (⇑e : (a : n) → m) i :
        α)
⊢ Eq (α := n → α) ((cramer (A.submatrix (⇑e : (a : n) → m) (⇑e : (a : n) → m)) : (a : n → α) → n → α) b : n → α)
    (Function.comp.{v + 1, u + 1, w + 1} (β := m) ((A.cramer : (a : m → α) → m → α) (b ∘ (⇑e.symm : (a : m) → n)))
        (⇑e : (a : n) → m) :
      n → α)

Tactic:
ext i
-- Module: Mathlib.LinearAlgebra.Matrix.Adjugate
Goal:
m : Type u
n : Type v
α : Type w
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : DecidableEq m
inst_3 : Fintype m
inst_4 : CommRing α
A : Matrix m m α
e : n ≃ m
b : n → α
i : n
h :
  Eq.{w + 1} (α := α) ((cramer (A.submatrix (⇑e : (a : n) → m) (⇑e : (a : n) → m)) : (a : n → α) → n → α) b i : α)
    ((A.cramer : (a : m → α) → m → α) (b ∘ (⇑e.symm : (a : m) → n)) ((e : (a : n) → m) i) : α)
h₁ :
  (updateCol (A.submatrix (⇑e : (a : n) → m) (⇑e : (a : n) → m)) i b).det =
    (A.updateCol ((e : (a : n) → m) i) (b ∘ (⇑e.symm : (a : m) → n))).det
h₂ :
  det.{w, v} (n := n)
      ((A.updateCol ((e : (a : n) → m) i) fun (i : m) ↦ b ((e.symm : (a : m) → n) i)).submatrix (⇑e : (a : n) → m)
        (⇑e : (a : n) → m)) =
    (A.updateCol ((e : (a : n) → m) i) (b ∘ (⇑e.symm : (a : m) → n))).det
h₃ :
  (A.updateCol ((e : (a : n) → m) i) fun (i : m) ↦ b ((e.symm : (a : m) → n) i)).det =
    (A.updateCol ((e : (a : n) → m) i) (b ∘ (⇑e.symm : (a : m) → n))).det
⊢ Eq.{w + 1} (α := α) ((cramer (A.submatrix (⇑e : (a : n) → m) (⇑e : (a : n) → m)) : (a : n → α) → n → α) b i : α)
    (Function.comp.{v + 1, u + 1, w + 1} (β := m) ((A.cramer : (a : m → α) → m → α) (b ∘ (⇑e.symm : (a : m) → n)))
        (⇑e : (a : n) → m) i :
      α)

Tactic:
simp_rw [Function.comp_apply, cramer_apply, updateCol_submatrix_equiv,
    det_submatrix_equiv_self e, Function.comp_def]

Premises used: Matrix.cramer_apply, Function.comp_def, Matrix.updateCol_submatrix_equiv, Function.comp_apply, Matrix.det_submatrix_equiv_self
-- Module: Mathlib.LinearAlgebra.Matrix.Adjugate
Goal:
m : Type u
n : Type v
α : Type w
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : DecidableEq m
inst_3 : Fintype m
inst_4 : CommRing α
e : m ≃ n
A : Matrix m m α
b : n → α
⊢ Eq (α := n → α) ((cramer ((reindex e e : (a : Matrix m m α) → Matrix n n α) A) : (a : n → α) → n → α) b : n → α)
    (Function.comp.{v + 1, u + 1, w + 1} (β := m) ((A.cramer : (a : m → α) → m → α) (b ∘ (⇑e : (a : m) → n)))
        (⇑e.symm : (a : n) → m) :
      n → α)

Tactic:
cramer_submatrix_equiv _ _ _

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

Tactic:
rfl

Premises used: Matrix.adjugate, rfl
-- Module: Mathlib.LinearAlgebra.Matrix.Adjugate
Goal:
n : Type v
α : Type w
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : CommRing α
A : Matrix n n α
i j : n
rw :
  (of : (a : n → n → α) → Matrix n n α)
      (fun (i : n) ↦ (Aᵀ.cramer : (a : n → α) → n → α) (Pi.single (M := fun (a : n) ↦ α) i 1)) i j =
    (A.updateRow j (Pi.single (M := fun (a : n) ↦ α) i 1)).det
rw₁ :
  (Aᵀ.cramer : (a : n → α) → n → α) (Pi.single (M := fun (a : n) ↦ α) i 1) j =
    (A.updateRow j (Pi.single (M := fun (a : n) ↦ α) i 1)).det
rw₂ :
  (Aᵀ.updateCol j (Pi.single (M := fun (a : n) ↦ α) i 1)).det =
    (A.updateRow j (Pi.single (M := fun (a : n) ↦ α) i 1)).det
rw₃ :
  (A.updateRow j (Pi.single (M := fun (a : n) ↦ α) i 1))ᵀ.det =
    (A.updateRow j (Pi.single (M := fun (a : n) ↦ α) i 1)).det
rw₄ rw₅ :
  (A.updateRow j (Pi.single (M := fun (a : n) ↦ α) i 1)).det =
    (A.updateRow j (Pi.single (M := fun (a : n) ↦ α) i 1)).det
⊢ A.adjugate i j = (A.updateRow j (Pi.single (M := fun (a : n) ↦ α) i 1)).det

Tactic:
rw [adjugate_def, of_apply, cramer_apply, updateCol_transpose, det_transpose]

Premises used: Matrix.det_transpose, Matrix.cramer_apply, Matrix.of_apply, Matrix.adjugate_def, Matrix.updateCol_transpose
-- Module: Mathlib.LinearAlgebra.Matrix.Adjugate
Goal:
n : Type v
α : Type w
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : CommRing α
A : Matrix n n α
a : ∀ (i j : n), A.adjugateᵀ i j = Aᵀ.adjugate i j
⊢ A.adjugateᵀ = Aᵀ.adjugate

Tactic:
ext i j
-- Module: Mathlib.LinearAlgebra.Matrix.Adjugate
Goal:
n : Type v
α : Type w
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : CommRing α
A : Matrix n n α
i j : n
a :
  (A.updateRow i (Pi.single (M := fun (a : n) ↦ α) j 1)).det =
    (A.updateCol j (Pi.single (M := fun (a : n) ↦ α) i 1)).det
⊢ A.adjugateᵀ i j = Aᵀ.adjugate i j

Tactic:
rw [transpose_apply, adjugate_apply, adjugate_apply, updateRow_transpose, det_transpose]

Premises used: Matrix.det_transpose, Matrix.updateRow_transpose, Matrix.adjugate_apply, Matrix.transpose_apply
-- Module: Mathlib.LinearAlgebra.Matrix.Adjugate
Goal:
n : Type v
α : Type w
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : CommRing α
A : Matrix n n α
i j : n
a :
  Eq.{w + 1} (α := α)
    (∑ σ : Perm n,
      HMul.hMul (α := α) (↑(↑(((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) σ) : ℤ) : α)
        (∏ i_1 : n, A.updateRow i (Pi.single (M := fun (a : n) ↦ α) j 1) ((σ : (a : n) → n) i_1) i_1))
    (∑ σ : Perm n,
      HMul.hMul (α := α) (↑(↑(((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) σ) : ℤ) : α)
        (∏ i_1 : n, A.updateCol j (Pi.single (M := fun (a : n) ↦ α) i 1) ((σ : (a : n) → n) i_1) i_1))
⊢ (A.updateRow i (Pi.single (M := fun (a : n) ↦ α) j 1)).det =
    (A.updateCol j (Pi.single (M := fun (a : n) ↦ α) i 1)).det

Tactic:
rw [det_apply', det_apply']

Premises used: Matrix.det_apply'
-- Module: Mathlib.LinearAlgebra.Matrix.Adjugate
Goal:
n : Type v
α : Type w
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : CommRing α
A : Matrix n n α
i j : n
a :
  ∀ (x : Perm n),
    Membership.mem (γ := Finset (Perm n)) univ x →
      HMul.hMul (α := α) (↑(↑(((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) x) : ℤ) : α)
          (∏ i_1 : n, A.updateRow i (Pi.single (M := fun (a : n) ↦ α) j 1) ((x : (a : n) → n) i_1) i_1) =
        HMul.hMul (α := α) (↑(↑(((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) x) : ℤ) : α)
          (∏ i_1 : n, A.updateCol j (Pi.single (M := fun (a : n) ↦ α) i 1) ((x : (a : n) → n) i_1) i_1)
⊢ Eq.{w + 1} (α := α)
    (∑ σ : Perm n,
      HMul.hMul (α := α) (↑(↑(((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) σ) : ℤ) : α)
        (∏ i_1 : n, A.updateRow i (Pi.single (M := fun (a : n) ↦ α) j 1) ((σ : (a : n) → n) i_1) i_1))
    (∑ σ : Perm n,
      HMul.hMul (α := α) (↑(↑(((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) σ) : ℤ) : α)
        (∏ i_1 : n, A.updateCol j (Pi.single (M := fun (a : n) ↦ α) i 1) ((σ : (a : n) → n) i_1) i_1))

Tactic:
apply Finset.sum_congr rfl

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.LinearAlgebra.Matrix.Adjugate
Goal:
n : Type v
α : Type w
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : CommRing α
A : Matrix n n α
i j : n
σ : Perm n
a :
  Membership.mem (γ := Finset (Perm n)) univ σ →
    HMul.hMul (α := α) (↑(↑(((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) σ) : ℤ) : α)
        (∏ i_1 : n, A.updateRow i (Pi.single (M := fun (a : n) ↦ α) j 1) ((σ : (a : n) → n) i_1) i_1) =
      HMul.hMul (α := α) (↑(↑(((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) σ) : ℤ) : α)
        (∏ i_1 : n, A.updateCol j (Pi.single (M := fun (a : n) ↦ α) i 1) ((σ : (a : n) → n) i_1) i_1)
⊢ Membership.mem (γ := Finset (Perm n)) univ σ →
    HMul.hMul (α := α) (↑(↑(((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) σ) : ℤ) : α)
        (∏ i_1 : n, A.updateRow i (Pi.single (M := fun (a : n) ↦ α) j 1) ((σ : (a : n) → n) i_1) i_1) =
      HMul.hMul (α := α) (↑(↑(((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) σ) : ℤ) : α)
        (∏ i_1 : n, A.updateCol j (Pi.single (M := fun (a : n) ↦ α) i 1) ((σ : (a : n) → n) i_1) i_1)

Tactic:
_
-- Module: Mathlib.LinearAlgebra.Matrix.Adjugate
Goal:
n : Type v
α : Type w
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : CommRing α
A : Matrix n n α
i j : n
σ : Perm n
h : Membership.mem (γ := Finset (Perm n)) univ σ
a :
  Eq.{w + 1} (α := α) (∏ i_1 : n, A.updateRow i (Pi.single (M := fun (a : n) ↦ α) j 1) ((σ : (a : n) → n) i_1) i_1)
    (∏ i_1 : n, A.updateCol j (Pi.single (M := fun (a : n) ↦ α) i 1) ((σ : (a : n) → n) i_1) i_1)
⊢ HMul.hMul (α := α) (↑(↑(((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) σ) : ℤ) : α)
      (∏ i_1 : n, A.updateRow i (Pi.single (M := fun (a : n) ↦ α) j 1) ((σ : (a : n) → n) i_1) i_1) =
    HMul.hMul (α := α) (↑(↑(((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) σ) : ℤ) : α)
      (∏ i_1 : n, A.updateCol j (Pi.single (M := fun (a : n) ↦ α) i 1) ((σ : (a : n) → n) i_1) i_1)

Tactic:
congr 1
-- Module: Mathlib.LinearAlgebra.Matrix.Adjugate
Goal:
n : Type v
α : Type w
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : CommRing α
A : Matrix n n α
i j : n
σ : Perm n
h : Membership.mem (γ := Finset (Perm n)) univ σ
pos :
  ∀ (h : i = (σ : (a : n) → n) j),
    Eq.{w + 1} (α := α) (∏ i_1 : n, A.updateRow i (Pi.single (M := fun (a : n) ↦ α) j 1) ((σ : (a : n) → n) i_1) i_1)
      (∏ i_1 : n, A.updateCol j (Pi.single (M := fun (a : n) ↦ α) i 1) ((σ : (a : n) → n) i_1) i_1)
neg :
  ∀ (h : ¬i = (σ : (a : n) → n) j),
    Eq.{w + 1} (α := α) (∏ i_1 : n, A.updateRow i (Pi.single (M := fun (a : n) ↦ α) j 1) ((σ : (a : n) → n) i_1) i_1)
      (∏ i_1 : n, A.updateCol j (Pi.single (M := fun (a : n) ↦ α) i 1) ((σ : (a : n) → n) i_1) i_1)
⊢ Eq.{w + 1} (α := α) (∏ i_1 : n, A.updateRow i (Pi.single (M := fun (a : n) ↦ α) j 1) ((σ : (a : n) → n) i_1) i_1)
    (∏ i_1 : n, A.updateCol j (Pi.single (M := fun (a : n) ↦ α) i 1) ((σ : (a : n) → n) i_1) i_1)

Tactic:
by_cases h : i = σ j

Premises used: DFunLike.coe
-- Module: Mathlib.LinearAlgebra.Matrix.Adjugate
Goal:
n : Type v
α : Type w
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : CommRing α
A : Matrix n n α
i j : n
σ : Perm n
h_1 : Membership.mem (γ := Finset (Perm n)) univ σ
h : i = (σ : (a : n) → n) j
pos :
  Eq (α := n → α) (fun (i_1 : n) ↦ A.updateRow i (Pi.single (M := fun (a : n) ↦ α) j 1) ((σ : (a : n) → n) i_1) i_1)
    fun (i_1 : n) ↦ A.updateCol j (Pi.single (M := fun (a : n) ↦ α) i 1) ((σ : (a : n) → n) i_1) i_1
⊢ Eq.{w + 1} (α := α) (∏ i_1 : n, A.updateRow i (Pi.single (M := fun (a : n) ↦ α) j 1) ((σ : (a : n) → n) i_1) i_1)
    (∏ i_1 : n, A.updateCol j (Pi.single (M := fun (a : n) ↦ α) i 1) ((σ : (a : n) → n) i_1) i_1)

Tactic:
congr
-- Module: Mathlib.LinearAlgebra.Matrix.Adjugate
Goal:
n : Type v
α : Type w
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : CommRing α
A : Matrix n n α
i j : n
σ : Perm n
h_1 : Membership.mem (γ := Finset (Perm n)) univ σ
h : i = (σ : (a : n) → n) j
pos :
  ∀ (j' : n),
    A.updateRow i (Pi.single (M := fun (a : n) ↦ α) j 1) ((σ : (a : n) → n) j') j' =
      A.updateCol j (Pi.single (M := fun (a : n) ↦ α) i 1) ((σ : (a : n) → n) j') j'
⊢ Eq (α := n → α) (fun (i_1 : n) ↦ A.updateRow i (Pi.single (M := fun (a : n) ↦ α) j 1) ((σ : (a : n) → n) i_1) i_1)
    fun (i_1 : n) ↦ A.updateCol j (Pi.single (M := fun (a : n) ↦ α) i 1) ((σ : (a : n) → n) i_1) i_1

Tactic:
ext j'
-- Module: Mathlib.LinearAlgebra.Matrix.Adjugate
Goal:
n : Type v
α : Type w
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : CommRing α
A : Matrix n n α
i j : n
σ : Perm n
h_1 : Membership.mem (γ := Finset (Perm n)) univ σ
h : i = (σ : (a : n) → n) j
j' : n
pos :
  A.updateRow ((σ : (a : n) → n) j) (Pi.single (M := fun (a : n) ↦ α) j 1) ((σ : (a : n) → n) j') j' =
    A.updateCol j (Pi.single (M := fun (a : n) ↦ α) ((σ : (a : n) → n) j) 1) ((σ : (a : n) → n) j') j'
⊢ A.updateRow i (Pi.single (M := fun (a : n) ↦ α) j 1) ((σ : (a : n) → n) j') j' =
    A.updateCol j (Pi.single (M := fun (a : n) ↦ α) i 1) ((σ : (a : n) → n) j') j'

Tactic:
subst h
-- 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 α
j : n
σ : Perm n
h : Membership.mem (γ := Finset (Perm n)) univ σ
j' : n
⊢ Eq (α := n) ((σ : (a : n) → n) j' : n) ((σ : (a : n) → n) j : n) ↔ j' = j

Tactic:
have : σ j' = σ j ↔ j' = j := σ.injective.eq_iff
-- 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 α
j : n
σ : Perm n
h : Membership.mem (γ := Finset (Perm n)) univ σ
j' : n
this : Eq (α := n) ((σ : (a : n) → n) j' : n) ((σ : (a : n) → n) j : n) ↔ j' = j
pos :
  Eq.{w + 1} (α := α)
    (if Eq (α := n) ((σ : (a : n) → n) j' : n) ((σ : (a : n) → n) j : n) then Pi.single (M := fun (a : n) ↦ α) j 1 j'
      else A ((σ : (a : n) → n) j') j' :
      α)
    (if j' = j then
        Pi.single.{v, w} (ι := n) (M := fun (a : n) ↦ α) ((σ : (a : n) → n) j : n) (1 : α) ((σ : (a : n) → n) j' : n)
      else A ((σ : (a : n) → n) j') j' :
      α)
⊢ A.updateRow ((σ : (a : n) → n) j) (Pi.single (M := fun (a : n) ↦ α) j 1) ((σ : (a : n) → n) j') j' =
    A.updateCol j (Pi.single (M := fun (a : n) ↦ α) ((σ : (a : n) → n) j) 1) ((σ : (a : n) → n) j') j'

Tactic:
rw [updateRow_apply, updateCol_apply]

Premises used: Matrix.updateCol_apply, Matrix.updateRow_apply
-- Module: Mathlib.LinearAlgebra.Matrix.Adjugate
Goal:
n : Type v
α : Type w
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : CommRing α
A : Matrix n n α
j : n
σ : Perm n
h : Membership.mem (γ := Finset (Perm n)) univ σ
j' : n
this : Eq (α := n) ((σ : (a : n) → n) j' : n) ((σ : (a : n) → n) j : n) ↔ j' = j
pos :
  Eq.{w + 1} (α := α) (if j' = j then Pi.single (M := fun (a : n) ↦ α) j 1 j' else A ((σ : (a : n) → n) j') j' : α)
    (if j' = j then
        Pi.single.{v, w} (ι := n) (M := fun (a : n) ↦ α) ((σ : (a : n) → n) j : n) (1 : α) ((σ : (a : n) → n) j' : n)
      else A ((σ : (a : n) → n) j') j' :
      α)
⊢ Eq.{w + 1} (α := α)
    (if Eq (α := n) ((σ : (a : n) → n) j' : n) ((σ : (a : n) → n) j : n) then Pi.single (M := fun (a : n) ↦ α) j 1 j'
      else A ((σ : (a : n) → n) j') j' :
      α)
    (if j' = j then
        Pi.single.{v, w} (ι := n) (M := fun (a : n) ↦ α) ((σ : (a : n) → n) j : n) (1 : α) ((σ : (a : n) → n) j' : n)
      else A ((σ : (a : n) → n) j') j' :
      α)

Tactic:
simp_rw [this]
-- Module: Mathlib.LinearAlgebra.Matrix.Adjugate
Goal:
n : Type v
α : Type w
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : CommRing α
A : Matrix n n α
j : n
σ : Perm n
h : Membership.mem (γ := Finset (Perm n)) univ σ
j' : n
this : Eq (α := n) ((σ : (a : n) → n) j' : n) ((σ : (a : n) → n) j : n) ↔ j' = j
pos :
  ∀ (this : Eq (α := n) ((σ : (a : n) → n) j' : n) ((σ : (a : n) → n) j' : n) ↔ j' = j'),
    Eq.{w + 1} (α := α) (Pi.single (M := fun (a : n) ↦ α) j' 1 j' : α)
      (Pi.single.{v, w} (ι := n) (M := fun (a : n) ↦ α) ((σ : (a : n) → n) j' : n) (1 : α) ((σ : (a : n) → n) j' : n) :
        α)
⊢ Eq.{w + 1} (α := α) (if x : j' = j then Pi.single (M := fun (a : n) ↦ α) j 1 j' else A ((σ : (a : n) → n) j') j')
    (if x : j' = j then
      Pi.single.{v, w} (ι := n) (M := fun (a : n) ↦ α) ((σ : (a : n) → n) j : n) (1 : α) ((σ : (a : n) → n) j' : n)
    else A ((σ : (a : n) → n) j') j')

Tactic:
congr 1 with rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.Matrix.Adjugate
Goal:
n : Type v
α : Type w
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : CommRing α
A : Matrix n n α
σ : Perm n
h : Membership.mem (γ := Finset (Perm n)) univ σ
j' : n
this : Eq (α := n) ((σ : (a : n) → n) j' : n) ((σ : (a : n) → n) j' : n) ↔ j' = j'
pos :
  Eq.{w + 1} (α := α) (1 : α)
    (Pi.single.{v, w} (ι := n) (M := fun (a : n) ↦ α) ((σ : (a : n) → n) j' : n) (1 : α) ((σ : (a : n) → n) j' : n) : α)
pos₁ pos₂ : Eq.{w + 1} (α := α) 1 1
⊢ Eq.{w + 1} (α := α) (Pi.single (M := fun (a : n) ↦ α) j' 1 j' : α)
    (Pi.single.{v, w} (ι := n) (M := fun (a : n) ↦ α) ((σ : (a : n) → n) j' : n) (1 : α) ((σ : (a : n) → n) j' : n) : α)

Tactic:
rw [Pi.single_eq_same, Pi.single_eq_same]

Premises used: Pi.single_eq_same
-- Module: Mathlib.LinearAlgebra.Matrix.Adjugate
Goal:
n : Type v
α : Type w
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : CommRing α
A : Matrix n n α
i j : n
σ : Perm n
h_1 : Membership.mem (γ := Finset (Perm n)) univ σ
h : ¬i = (σ : (a : n) → n) j
apply : A.updateCol j (Pi.single (M := fun (a : n) ↦ α) i 1) ((σ : (a : n) → n) j) j = 0
⊢ Eq.{w + 1} (α := α) (∏ j' : n, A.updateCol j (Pi.single (M := fun (a : n) ↦ α) i 1) ((σ : (a : n) → n) j') j') 0

Tactic:
apply prod_eq_zero (mem_univ j)

Premises used: Finset.mem_univ, Finset.prod_eq_zero
-- Module: Mathlib.LinearAlgebra.Matrix.Adjugate
Goal:
n : Type v
α : Type w
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : CommRing α
A : Matrix n n α
i j : n
σ : Perm n
h_1 : Membership.mem (γ := Finset (Perm n)) univ σ
h : ¬i = (σ : (a : n) → n) j
rw : Eq.{w + 1} (α := α) (Pi.single (M := fun (a : n) ↦ α) i 1 ((σ : (a : n) → n) j) : α) (0 : α)
rw₁ rw₂ : Eq.{w + 1} (α := α) 0 0
⊢ A.updateCol j (Pi.single (M := fun (a : n) ↦ α) i 1) ((σ : (a : n) → n) j) j = 0

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

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 α
A : Matrix n n α
i j : n
σ : Perm n
h_1 : Membership.mem (γ := Finset (Perm n)) univ σ
h : ¬i = (σ : (a : n) → n) j
⊢ Eq.{w + 1} (α := α) (∏ j' : n, A.updateCol j (Pi.single (M := fun (a : n) ↦ α) i 1) ((σ : (a : n) → n) j') j') 0

Tactic:
have : (∏ j' : n, updateCol A j (Pi.single i 1) (σ j') j') = 0 := by
      apply prod_eq_zero (mem_univ j)
      rw [updateCol_self, Pi.single_eq_of_ne' h]
-- Module: Mathlib.LinearAlgebra.Matrix.Adjugate
Goal:
n : Type v
α : Type w
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : CommRing α
A : Matrix n n α
i j : n
σ : Perm n
h_1 : Membership.mem (γ := Finset (Perm n)) univ σ
h : ¬i = (σ : (a : n) → n) j
this : Eq.{w + 1} (α := α) (∏ j' : n, A.updateCol j (Pi.single (M := fun (a : n) ↦ α) i 1) ((σ : (a : n) → n) j') j') 0
neg :
  Eq.{w + 1} (α := α) (∏ i_1 : n, A.updateRow i (Pi.single (M := fun (a : n) ↦ α) j 1) ((σ : (a : n) → n) i_1) i_1) 0
⊢ Eq.{w + 1} (α := α) (∏ i_1 : n, A.updateRow i (Pi.single (M := fun (a : n) ↦ α) j 1) ((σ : (a : n) → n) i_1) i_1)
    (∏ i_1 : n, A.updateCol j (Pi.single (M := fun (a : n) ↦ α) i 1) ((σ : (a : n) → n) i_1) i_1)

Tactic:
rw [this]
-- Module: Mathlib.LinearAlgebra.Matrix.Adjugate
Goal:
n : Type v
α : Type w
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : CommRing α
A : Matrix n n α
i j : n
σ : Perm n
h_1 : Membership.mem (γ := Finset (Perm n)) univ σ
h : ¬i = (σ : (a : n) → n) j
this : Eq.{w + 1} (α := α) (∏ j' : n, A.updateCol j (Pi.single (M := fun (a : n) ↦ α) i 1) ((σ : (a : n) → n) j') j') 0
neg :
  A.updateRow i (Pi.single (M := fun (a : n) ↦ α) j 1) ((σ : (a : n) → n) ((σ⁻¹ : (a : n) → n) i : n))
      ((σ⁻¹ : (a : n) → n) i) =
    0
⊢ Eq.{w + 1} (α := α) (∏ i_1 : n, A.updateRow i (Pi.single (M := fun (a : n) ↦ α) j 1) ((σ : (a : n) → n) i_1) i_1) 0

Tactic:
apply prod_eq_zero (mem_univ (σ⁻¹ i))

Premises used: Finset.mem_univ, Inv.inv, Finset.prod_eq_zero, DFunLike.coe
-- Module: Mathlib.LinearAlgebra.Matrix.Adjugate
Goal:
n : Type v
α : Type w
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : CommRing α
A : Matrix n n α
i j : n
σ : Perm n
h_1 : Membership.mem (γ := Finset (Perm n)) univ σ
h : ¬i = (σ : (a : n) → n) j
this : Eq.{w + 1} (α := α) (∏ j' : n, A.updateCol j (Pi.single (M := fun (a : n) ↦ α) i 1) ((σ : (a : n) → n) j') j') 0
neg : Eq.{w + 1} (α := α) (Pi.single (M := fun (a : n) ↦ α) j 1 ((Equiv.symm σ : (a : n) → n) i) : α) (0 : α)
⊢ A.updateRow i (Pi.single (M := fun (a : n) ↦ α) j 1) ((σ : (a : n) → n) ((σ⁻¹ : (a : n) → n) i : n))
      ((σ⁻¹ : (a : n) → n) i) =
    0

Tactic:
simp only [Perm.coe_inv, apply_symm_apply, updateRow_self]

Premises used: Equiv.apply_symm_apply, Equiv.Perm.coe_inv, Matrix.updateRow_self
-- Module: Mathlib.LinearAlgebra.Matrix.Adjugate
Goal:
n : Type v
α : Type w
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : CommRing α
A : Matrix n n α
i j : n
σ : Perm n
h_1 : Membership.mem (γ := Finset (Perm n)) univ σ
h : ¬i = (σ : (a : n) → n) j
this : Eq.{w + 1} (α := α) (∏ j' : n, A.updateCol j (Pi.single (M := fun (a : n) ↦ α) i 1) ((σ : (a : n) → n) j') j') 0
neg : (Equiv.symm σ : (a : n) → n) i ≠ j
⊢ Eq.{w + 1} (α := α) (Pi.single (M := fun (a : n) ↦ α) j 1 ((Equiv.symm σ : (a : n) → n) i) : α) (0 : α)

Tactic:
apply Pi.single_eq_of_ne

Premises used: 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 α
A : Matrix n n α
i j : n
σ : Perm n
h_1 : Membership.mem (γ := Finset (Perm n)) univ σ
h : ¬i = (σ : (a : n) → n) j
this : Eq.{w + 1} (α := α) (∏ j' : n, A.updateCol j (Pi.single (M := fun (a : n) ↦ α) i 1) ((σ : (a : n) → n) j') j') 0
h' : (Equiv.symm σ : (a : n) → n) i = j
⊢ False

Tactic:
h ((symm_apply_eq σ).mp h')

Premises used: Equiv.symm_apply_eq, Iff.mp
-- Module: Mathlib.LinearAlgebra.Matrix.Adjugate
Goal:
n : Type v
α : Type w
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : CommRing α
A : Matrix n n α
i j : n
σ : Perm n
h_1 : Membership.mem (γ := Finset (Perm n)) univ σ
h : ¬i = (σ : (a : n) → n) j
this : Eq.{w + 1} (α := α) (∏ j' : n, A.updateCol j (Pi.single (M := fun (a : n) ↦ α) i 1) ((σ : (a : n) → n) j') j') 0
h' : (Equiv.symm σ : (a : n) → n) i = j
⊢ False

Tactic:
exact h ((symm_apply_eq σ).mp h')

Premises used: Equiv.symm_apply_eq, Iff.mp
-- 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 α
hA : A.IsSymm
rw : A.adjugateᵀ = A.adjugate
rw₁ : Aᵀ.adjugate = A.adjugate
rw₂ rw₃ : A.adjugate = A.adjugate
⊢ A.adjugate.IsSymm

Tactic:
rw [IsSymm, Matrix.adjugate_transpose, hA.eq]

Premises used: Matrix.IsSymm.eq, Matrix.IsSymm, Matrix.adjugate_transpose
-- Module: Mathlib.LinearAlgebra.Matrix.Adjugate
Goal:
m : Type u
n : Type v
α : Type w
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : DecidableEq m
inst_3 : Fintype m
inst_4 : CommRing α
e : n ≃ m
A : Matrix m m α
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
⊢ 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))

Tactic:
ext i j