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 α
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
⊢ 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 :
      α)
have 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
Tactic: simp_rw [Function.comp_apply, cramer_apply, updateCol_submatrix_equiv,
    det_submatrix_equiv_self e, Function.comp_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 α
i j : n
⊢ A.adjugate i j = (A.updateRow j (Pi.single (M := fun (a : n) ↦ α) i 1)).det
have 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
Tactic: rw [adjugate_def, of_apply, cramer_apply, updateCol_transpose, det_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 α
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
⊢ A.adjugate i j = (A.updateRow j (Pi.single (M := fun (a : n) ↦ α) i 1)).det
have 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
Tactic: rw [adjugate_def, of_apply, cramer_apply, updateCol_transpose, det_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 α
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
⊢ A.adjugate i j = (A.updateRow j (Pi.single (M := fun (a : n) ↦ α) i 1)).det
have 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
Tactic: rw [adjugate_def, of_apply, cramer_apply, updateCol_transpose, det_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 α
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
⊢ A.adjugate i j = (A.updateRow j (Pi.single (M := fun (a : n) ↦ α) i 1)).det
have 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
Tactic: rw [adjugate_def, of_apply, cramer_apply, updateCol_transpose, det_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 α
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
⊢ A.adjugate i j = (A.updateRow j (Pi.single (M := fun (a : n) ↦ α) i 1)).det
have 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
Tactic: rw [adjugate_def, of_apply, cramer_apply, updateCol_transpose, det_transpose]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Adjugate (goal)
Goal:
n : Type v
α : Type w
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : CommRing α
A : Matrix n n α
⊢ A.adjugateᵀ = Aᵀ.adjugate
have a : ∀ (i j : n), A.adjugateᵀ i j = Aᵀ.adjugate i j
Tactic: ext i j
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Adjugate (goal)
Goal:
n : Type v
α : Type w
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : CommRing α
A : Matrix n n α
i j : n
⊢ A.adjugateᵀ i j = Aᵀ.adjugate i j
have 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
Tactic: rw [transpose_apply, adjugate_apply, adjugate_apply, updateRow_transpose, det_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 α
i j : n
⊢ (A.updateRow i (Pi.single (M := fun (a : n) ↦ α) j 1)).det =
    (A.updateCol j (Pi.single (M := fun (a : n) ↦ α) i 1)).det
have 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))
Tactic: rw [det_apply', det_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 α
i j : n
⊢ 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))
have 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)
Tactic: apply Finset.sum_congr rfl
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Adjugate (goal)
Goal:
n : Type v
α : Type w
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : CommRing α
A : Matrix n n α
i j : n
σ : Perm n
h : 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)
have 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)
Tactic: congr 1
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Adjugate (goal)
Goal:
n : Type v
α : Type w
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : CommRing α
A : Matrix n n α
i j : n
σ : Perm n
h : Membership.mem (γ := Finset (Perm n)) univ σ
⊢ 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)
have 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)
Tactic: by_cases h : i = σ j
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Adjugate (goal)
Goal:
n : Type v
α : Type w
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : CommRing α
A : Matrix n n α
i j : n
σ : 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)
⊢ 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)
have 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)
Tactic: by_cases h : i = σ j
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Adjugate (goal)
Goal:
n : Type v
α : Type w
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : CommRing α
A : Matrix n n α
i j : n
σ : Perm n
h_1 : Membership.mem (γ := Finset (Perm n)) univ σ
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)
have 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
Tactic: congr
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Adjugate (goal)
Goal:
n : Type v
α : Type w
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : CommRing α
A : Matrix n n α
i j : n
σ : Perm n
h_1 : Membership.mem (γ := Finset (Perm n)) univ σ
h : i = (σ : (a : n) → n) 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
have 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'
Tactic: ext j'
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Adjugate (goal)
Goal:
n : Type v
α : Type w
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : CommRing α
A : Matrix n n α
i j : n
σ : Perm n
h_1 : Membership.mem (γ := Finset (Perm n)) univ σ
h : i = (σ : (a : n) → n) j
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'
have 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'
Tactic: subst h
Cleared hypotheses: i, h
-- 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 α
j : n
σ : Perm n
h : Membership.mem (γ := Finset (Perm n)) univ σ
j' : n
⊢ 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'
have this : Eq (α := n) ((σ : (a : n) → n) j' : n) ((σ : (a : n) → n) j : n) ↔ j' = j
Tactic: have : σ j' = σ j ↔ j' = j := σ.injective.eq_iff
-- 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 α
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
⊢ 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'
have 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' :
    α)
Tactic: rw [updateRow_apply, updateCol_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 α
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
⊢ 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' :
      α)
have 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' :
    α)
Tactic: simp_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 α
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
⊢ 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')
have 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) : α)
Tactic: congr 1 with rfl
Cleared hypotheses: j, 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 α
σ : 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'
⊢ 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) : α)
have 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) : α)
Tactic: rw [Pi.single_eq_same, Pi.single_eq_same]
-- 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 α
σ : 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) : α)
⊢ 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) : α)
have pos₁ : Eq.{w + 1} (α := α) 1 1
Tactic: rw [Pi.single_eq_same, Pi.single_eq_same]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Adjugate (goal)
Goal:
n : Type v
α : Type w
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : CommRing α
A : Matrix n n α
i j : n
σ : 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
have apply : 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)
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Adjugate (goal)
Goal:
n : Type v
α : Type w
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : CommRing α
A : Matrix n n α
i j : n
σ : Perm n
h_1 : Membership.mem (γ := Finset (Perm n)) univ σ
h : ¬i = (σ : (a : n) → n) j
⊢ A.updateCol j (Pi.single (M := fun (a : n) ↦ α) i 1) ((σ : (a : n) → n) j) j = 0
have rw : Eq.{w + 1} (α := α) (Pi.single (M := fun (a : n) ↦ α) i 1 ((σ : (a : n) → n) j) : α) (0 : α)
Tactic: rw [updateCol_self, Pi.single_eq_of_ne' h]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Adjugate (goal)
Goal:
n : Type v
α : Type w
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : CommRing α
A : Matrix n n α
i j : n
σ : 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 : α)
⊢ A.updateCol j (Pi.single (M := fun (a : n) ↦ α) i 1) ((σ : (a : n) → n) j) j = 0
have rw₁ : Eq.{w + 1} (α := α) 0 0
Tactic: rw [updateCol_self, Pi.single_eq_of_ne' h]
-- 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 α
i j : n
σ : Perm n
h_1 : Membership.mem (γ := Finset (Perm n)) univ σ
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)
have this : 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]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Adjugate (goal)
Goal:
n : Type v
α : Type w
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : CommRing α
A : Matrix n n α
i j : n
σ : 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
⊢ 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)
have 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
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 α
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
⊢ 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
have 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
Tactic: apply prod_eq_zero (mem_univ (σ⁻¹ i))
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Adjugate (goal)
Goal:
n : Type v
α : Type w
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : CommRing α
A : Matrix n n α
i j : n
σ : 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
⊢ A.updateRow i (Pi.single (M := fun (a : n) ↦ α) j 1) ((σ : (a : n) → n) ((σ⁻¹ : (a : n) → n) i : n))
      ((σ⁻¹ : (a : n) → n) i) =
    0
have neg : Eq.{w + 1} (α := α) (Pi.single (M := fun (a : n) ↦ α) j 1 ((Equiv.symm σ : (a : n) → n) i) : α) (0 : α)
Tactic: simp only [Perm.coe_inv, apply_symm_apply, updateRow_self]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Adjugate (goal)
Goal:
n : Type v
α : Type w
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : CommRing α
A : Matrix n n α
i j : n
σ : 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
⊢ Eq.{w + 1} (α := α) (Pi.single (M := fun (a : n) ↦ α) j 1 ((Equiv.symm σ : (a : n) → n) i) : α) (0 : α)
have neg : (Equiv.symm σ : (a : n) → n) i ≠ j
Tactic: apply Pi.single_eq_of_ne
-- 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 α
hA : A.IsSymm
⊢ A.adjugate.IsSymm
have rw : A.adjugateᵀ = A.adjugate
Tactic: rw [IsSymm, Matrix.adjugate_transpose, hA.eq]
-- 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 α
hA : A.IsSymm
rw : A.adjugateᵀ = A.adjugate
⊢ A.adjugate.IsSymm
have rw₁ : Aᵀ.adjugate = A.adjugate
Tactic: rw [IsSymm, Matrix.adjugate_transpose, hA.eq]
-- 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 α
hA : A.IsSymm
rw : A.adjugateᵀ = A.adjugate
rw₁ : Aᵀ.adjugate = A.adjugate
⊢ A.adjugate.IsSymm
have rw₂ : A.adjugate = A.adjugate
Tactic: rw [IsSymm, Matrix.adjugate_transpose, hA.eq]