awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic
Goal:
m : Type u_1
n : Type u_2
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : DecidableEq m
inst_3 : Fintype m
R : Type v
inst_4 : CommRing R
A : Matrix m m R
B : Matrix m n R
D : Matrix n n R
σ₁ : Perm m
σ₂ : Perm n
h :
  HMul.hMul (α := R) (↑(↑(((sign : Perm m →* ℤˣ) : (a : Perm m) → ℤˣ) σ₁) : ℤ) : R)
        (↑(↑(((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) σ₂) : ℤ) : R) *
      HMul.hMul (α := R) (∏ x : m, A ((σ₁ : (a : m) → m) x) x) (∏ x : n, D ((σ₂ : (a : n) → n) x) x) =
    (↑(↑(((sign : Perm (m ⊕ n) →* ℤˣ) : (a : Perm (m ⊕ n)) → ℤˣ) (σ₁.sumCongr σ₂)) : ℤ) : R) *
      HMul.hMul (α := R) (∏ x : m, A ((σ₁ : (a : m) → m) x) x) (∏ x : n, D ((σ₂ : (a : n) → n) x) x)
⊢ HMul.hMul (α := R) (↑(↑(((sign : Perm m →* ℤˣ) : (a : Perm m) → ℤˣ) σ₁) : ℤ) : R)
        (∏ x : m, A ((σ₁ : (a : m) → m) x) x) *
      HMul.hMul (α := R) (↑(↑(((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) σ₂) : ℤ) : R)
        (∏ x : n, D ((σ₂ : (a : n) → n) x) x) =
    (↑(↑(((sign : Perm (m ⊕ n) →* ℤˣ) : (a : Perm (m ⊕ n)) → ℤˣ) (σ₁.sumCongr σ₂)) : ℤ) : R) *
      HMul.hMul (α := R) (∏ x : m, A ((σ₁ : (a : m) → m) x) x) (∏ x : n, D ((σ₂ : (a : n) → n) x) x)

Tactic:
rw [mul_mul_mul_comm]

Premises used: mul_mul_mul_comm
-- Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic
Goal:
m : Type u_1
n : Type u_2
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : DecidableEq m
inst_3 : Fintype m
R : Type v
inst_4 : CommRing R
A : Matrix m m R
B : Matrix m n R
D : Matrix n n R
σ₁ : Perm m
σ₂ : Perm n
h :
  HMul.hMul (α := R) (↑(↑(((sign : Perm m →* ℤˣ) : (a : Perm m) → ℤˣ) σ₁) : ℤ) : R)
      (↑(↑(((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) σ₂) : ℤ) : R) =
    (↑(↑(((sign : Perm (m ⊕ n) →* ℤˣ) : (a : Perm (m ⊕ n)) → ℤˣ) (σ₁.sumCongr σ₂)) : ℤ) : R)
⊢ HMul.hMul (α := R) (↑(↑(((sign : Perm m →* ℤˣ) : (a : Perm m) → ℤˣ) σ₁) : ℤ) : R)
        (↑(↑(((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) σ₂) : ℤ) : R) *
      HMul.hMul (α := R) (∏ x : m, A ((σ₁ : (a : m) → m) x) x) (∏ x : n, D ((σ₂ : (a : n) → n) x) x) =
    (↑(↑(((sign : Perm (m ⊕ n) →* ℤˣ) : (a : Perm (m ⊕ n)) → ℤˣ) (σ₁.sumCongr σ₂)) : ℤ) : R) *
      HMul.hMul (α := R) (∏ x : m, A ((σ₁ : (a : m) → m) x) x) (∏ x : n, D ((σ₂ : (a : n) → n) x) x)

Tactic:
congr
-- Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic
Goal:
m : Type u_1
n : Type u_2
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : DecidableEq m
inst_3 : Fintype m
R : Type v
inst_4 : CommRing R
A : Matrix m m R
B : Matrix m n R
D : Matrix n n R
σ₁ : Perm m
σ₂ : Perm n
h :
  HMul.hMul (α := R) (↑(↑(((sign : Perm m →* ℤˣ) : (a : Perm m) → ℤˣ) σ₁) : ℤ) : R)
      (↑(↑(((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) σ₂) : ℤ) : R) =
    (↑(↑(HMul.hMul (α := ℤˣ) (β := ℤˣ) (((sign : Perm m →* ℤˣ) : (a : Perm m) → ℤˣ) σ₁ : ℤˣ)
              (((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) σ₂ : ℤˣ)) :
          ℤ) :
      R)
h₁ :
  HMul.hMul (α := R) (↑(↑(((sign : Perm m →* ℤˣ) : (a : Perm m) → ℤˣ) σ₁) : ℤ) : R)
      (↑(↑(((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) σ₂) : ℤ) : R) =
    (↑(HMul.hMul (α := ℤ) (↑(((sign : Perm m →* ℤˣ) : (a : Perm m) → ℤˣ) σ₁) : ℤ)
          (↑(((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) σ₂) : ℤ)) :
      R)
h₂ h₃ :
  HMul.hMul (α := R) (↑(↑(((sign : Perm m →* ℤˣ) : (a : Perm m) → ℤˣ) σ₁) : ℤ) : R)
      (↑(↑(((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) σ₂) : ℤ) : R) =
    HMul.hMul (α := R) (↑(↑(((sign : Perm m →* ℤˣ) : (a : Perm m) → ℤˣ) σ₁) : ℤ) : R)
      (↑(↑(((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) σ₂) : ℤ) : R)
⊢ HMul.hMul (α := R) (↑(↑(((sign : Perm m →* ℤˣ) : (a : Perm m) → ℤˣ) σ₁) : ℤ) : R)
      (↑(↑(((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) σ₂) : ℤ) : R) =
    (↑(↑(((sign : Perm (m ⊕ n) →* ℤˣ) : (a : Perm (m ⊕ n)) → ℤˣ) (σ₁.sumCongr σ₂)) : ℤ) : R)

Tactic:
rw [sign_sumCongr, Units.val_mul, Int.cast_mul]

Premises used: Equiv.Perm.sign_sumCongr, Int.cast_mul, Units.val_mul
-- Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic
Goal:
m : Type u_1
n : Type u_2
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : DecidableEq m
inst_3 : Fintype m
R : Type v
inst_4 : CommRing R
A : Matrix m m R
B : Matrix m n R
D : Matrix n n R
σ : Perm (m ⊕ n)
hσn : σ ∉ (↑(sumCongrHom m n).range : Set (Perm (m ⊕ n))).toFinset
⊢ σ ∉ (↑(sumCongrHom m n).range : Set (Perm (m ⊕ n)))

Tactic:
rw [Set.mem_toFinset] at hσn

Premises used: Set.mem_toFinset
-- Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic
Goal:
m : Type u_1
n : Type u_2
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : DecidableEq m
inst_3 : Fintype m
R : Type v
inst_4 : CommRing R
A : Matrix m m R
B : Matrix m n R
D : Matrix n n R
σ : Perm (m ⊕ n)
hσn : σ ∉ (↑(sumCongrHom m n).range : Set (Perm (m ⊕ n)))
⊢ ¬∀ (x : m), ∃ (y : m), Eq (α := m ⊕ n) (Sum.inl y) ((σ : (a : m ⊕ n) → m ⊕ n) (Sum.inl x))

Tactic:
simpa only [Set.MapsTo, Set.mem_range, forall_exists_index, forall_apply_eq_imp_iff] using
          mt mem_sumCongrHom_range_of_perm_mapsTo_inl hσn

Premises used: Set.mem_range, forall_exists_index, mt, Equiv.Perm.mem_sumCongrHom_range_of_perm_mapsTo_inl, Set.MapsTo, forall_apply_eq_imp_iff
-- Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic
Goal:
m : Type u_1
n : Type u_2
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : DecidableEq m
inst_3 : Fintype m
R : Type v
inst_4 : CommRing R
A : Matrix m m R
B : Matrix m n R
D : Matrix n n R
σ : Perm (m ⊕ n)
hσn : σ ∉ (↑(sumCongrHom m n).range : Set (Perm (m ⊕ n))).toFinset
⊢ ¬∀ (x : m), ∃ (y : m), Eq (α := m ⊕ n) (Sum.inl y) ((σ : (a : m ⊕ n) → m ⊕ n) (Sum.inl x))

Tactic:
have h1 : ¬∀ x, ∃ y, Sum.inl y = σ (Sum.inl x) := by
        rw [Set.mem_toFinset] at hσn
        simpa only [Set.MapsTo, Set.mem_range, forall_exists_index, forall_apply_eq_imp_iff] using
          mt mem_sumCongrHom_range_of_perm_mapsTo_inl hσn
-- Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic
Goal:
m : Type u_1
n : Type u_2
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : DecidableEq m
inst_3 : Fintype m
R : Type v
inst_4 : CommRing R
A : Matrix m m R
B : Matrix m n R
D : Matrix n n R
σ : Perm (m ⊕ n)
hσn : σ ∉ (↑(sumCongrHom m n).range : Set (Perm (m ⊕ n))).toFinset
h1 : ¬∀ (x : m), ∃ (y : m), Eq (α := m ⊕ n) (Sum.inl y) ((σ : (a : m ⊕ n) → m ⊕ n) (Sum.inl x))
convert_2 :
  ∀ (a : m) (ha : ¬∃ (y : m), Eq (α := m ⊕ n) (Sum.inl y) ((σ : (a : m ⊕ n) → m ⊕ n) (Sum.inl a))),
    HMul.hMul (α := R) (↑(↑(((sign : Perm (m ⊕ n) →* ℤˣ) : (a : Perm (m ⊕ n)) → ℤˣ) σ) : ℤ) : R)
        (∏ i : m ⊕ n, fromBlocks A B 0 D ((σ : (a : m ⊕ n) → m ⊕ n) i) i) =
      0
⊢ HMul.hMul (α := R) (↑(↑(((sign : Perm (m ⊕ n) →* ℤˣ) : (a : Perm (m ⊕ n)) → ℤˣ) σ) : ℤ) : R)
      (∏ i : m ⊕ n, fromBlocks A B 0 D ((σ : (a : m ⊕ n) → m ⊕ n) i) i) =
    0

Tactic:
obtain ⟨a, ha⟩ := not_forall.mp h1

Premises used: Iff.mp, Classical.not_forall
-- Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic
Goal:
m : Type u_1
n : Type u_2
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : DecidableEq m
inst_3 : Fintype m
R : Type v
inst_4 : CommRing R
A : Matrix m m R
B : Matrix m n R
D : Matrix n n R
σ : Perm (m ⊕ n)
hσn : σ ∉ (↑(sumCongrHom m n).range : Set (Perm (m ⊕ n))).toFinset
h1 : ¬∀ (x : m), ∃ (y : m), Eq (α := m ⊕ n) (Sum.inl y) ((σ : (a : m ⊕ n) → m ⊕ n) (Sum.inl x))
a : m
ha : ¬∃ (y : m), Eq (α := m ⊕ n) (Sum.inl y) ((σ : (a : m ⊕ n) → m ⊕ n) (Sum.inl a))
convert_2 :
  ∀ (a2 : m) (hx : Eq (α := m ⊕ n) ((σ : (a : m ⊕ n) → m ⊕ n) (Sum.inl a) : m ⊕ n) (Sum.inl a2 : m ⊕ n)),
    HMul.hMul (α := R) (↑(↑(((sign : Perm (m ⊕ n) →* ℤˣ) : (a : Perm (m ⊕ n)) → ℤˣ) σ) : ℤ) : R)
        (∏ i : m ⊕ n, fromBlocks A B 0 D ((σ : (a : m ⊕ n) → m ⊕ n) i) i) =
      0
convert_2₁ :
  ∀ (b : n) (hx : Eq (α := m ⊕ n) ((σ : (a : m ⊕ n) → m ⊕ n) (Sum.inl a) : m ⊕ n) (Sum.inr b : m ⊕ n)),
    HMul.hMul (α := R) (↑(↑(((sign : Perm (m ⊕ n) →* ℤˣ) : (a : Perm (m ⊕ n)) → ℤˣ) σ) : ℤ) : R)
        (∏ i : m ⊕ n, fromBlocks A B 0 D ((σ : (a : m ⊕ n) → m ⊕ n) i) i) =
      0
⊢ HMul.hMul (α := R) (↑(↑(((sign : Perm (m ⊕ n) →* ℤˣ) : (a : Perm (m ⊕ n)) → ℤˣ) σ) : ℤ) : R)
      (∏ i : m ⊕ n, fromBlocks A B 0 D ((σ : (a : m ⊕ n) → m ⊕ n) i) i) =
    0

Tactic:
rcases hx : σ (Sum.inl a) with a2 | b

Premises used: Sum.inl, DFunLike.coe
-- Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic
Goal:
m : Type u_1
n : Type u_2
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : DecidableEq m
inst_3 : Fintype m
R : Type v
inst_4 : CommRing R
A : Matrix m m R
B : Matrix m n R
D : Matrix n n R
σ : Perm (m ⊕ n)
hσn : σ ∉ (↑(sumCongrHom m n).range : Set (Perm (m ⊕ n))).toFinset
h1 : ¬∀ (x : m), ∃ (y : m), Eq (α := m ⊕ n) (Sum.inl y) ((σ : (a : m ⊕ n) → m ⊕ n) (Sum.inl x))
a : m
ha : ¬∃ (y : m), Eq (α := m ⊕ n) (Sum.inl y) ((σ : (a : m ⊕ n) → m ⊕ n) (Sum.inl a))
a2 : m
hx : Eq (α := m ⊕ n) ((σ : (a : m ⊕ n) → m ⊕ n) (Sum.inl a) : m ⊕ n) (Sum.inl a2 : m ⊕ n)
⊢ ¬Eq (α := m ⊕ n) (Sum.inl a2) ((σ : (a : m ⊕ n) → m ⊕ n) (Sum.inl a))

Tactic:
have hn := (not_exists.mp ha) a2
-- Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic
Goal:
m : Type u_1
n : Type u_2
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : DecidableEq m
inst_3 : Fintype m
R : Type v
inst_4 : CommRing R
A : Matrix m m R
B : Matrix m n R
D : Matrix n n R
σ : Perm (m ⊕ n)
hσn : σ ∉ (↑(sumCongrHom m n).range : Set (Perm (m ⊕ n))).toFinset
h1 : ¬∀ (x : m), ∃ (y : m), Eq (α := m ⊕ n) (Sum.inl y) ((σ : (a : m ⊕ n) → m ⊕ n) (Sum.inl x))
a : m
ha : ¬∃ (y : m), Eq (α := m ⊕ n) (Sum.inl y) ((σ : (a : m ⊕ n) → m ⊕ n) (Sum.inl a))
a2 : m
hx : Eq (α := m ⊕ n) ((σ : (a : m ⊕ n) → m ⊕ n) (Sum.inl a) : m ⊕ n) (Sum.inl a2 : m ⊕ n)
hn : ¬Eq (α := m ⊕ n) (Sum.inl a2) ((σ : (a : m ⊕ n) → m ⊕ n) (Sum.inl a))
⊢ HMul.hMul (α := R) (↑(↑(((sign : Perm (m ⊕ n) →* ℤˣ) : (a : Perm (m ⊕ n)) → ℤˣ) σ) : ℤ) : R)
      (∏ i : m ⊕ n, fromBlocks A B 0 D ((σ : (a : m ⊕ n) → m ⊕ n) i) i) =
    0

Tactic:
absurd hx.symm hn

Premises used: absurd, Eq.symm
-- Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic
Goal:
m : Type u_1
n : Type u_2
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : DecidableEq m
inst_3 : Fintype m
R : Type v
inst_4 : CommRing R
A : Matrix m m R
B : Matrix m n R
D : Matrix n n R
σ : Perm (m ⊕ n)
hσn : σ ∉ (↑(sumCongrHom m n).range : Set (Perm (m ⊕ n))).toFinset
h1 : ¬∀ (x : m), ∃ (y : m), Eq (α := m ⊕ n) (Sum.inl y) ((σ : (a : m ⊕ n) → m ⊕ n) (Sum.inl x))
a : m
ha : ¬∃ (y : m), Eq (α := m ⊕ n) (Sum.inl y) ((σ : (a : m ⊕ n) → m ⊕ n) (Sum.inl a))
a2 : m
hx : Eq (α := m ⊕ n) ((σ : (a : m ⊕ n) → m ⊕ n) (Sum.inl a) : m ⊕ n) (Sum.inl a2 : m ⊕ n)
hn : ¬Eq (α := m ⊕ n) (Sum.inl a2) ((σ : (a : m ⊕ n) → m ⊕ n) (Sum.inl a))
⊢ HMul.hMul (α := R) (↑(↑(((sign : Perm (m ⊕ n) →* ℤˣ) : (a : Perm (m ⊕ n)) → ℤˣ) σ) : ℤ) : R)
      (∏ i : m ⊕ n, fromBlocks A B 0 D ((σ : (a : m ⊕ n) → m ⊕ n) i) i) =
    0

Tactic:
exact absurd hx.symm hn

Premises used: absurd, Eq.symm
-- Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic
Goal:
m : Type u_1
n : Type u_2
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : DecidableEq m
inst_3 : Fintype m
R : Type v
inst_4 : CommRing R
A : Matrix m m R
B : Matrix m n R
D : Matrix n n R
σ : Perm (m ⊕ n)
hσn : σ ∉ (↑(sumCongrHom m n).range : Set (Perm (m ⊕ n))).toFinset
h1 : ¬∀ (x : m), ∃ (y : m), Eq (α := m ⊕ n) (Sum.inl y) ((σ : (a : m ⊕ n) → m ⊕ n) (Sum.inl x))
a : m
ha : ¬∃ (y : m), Eq (α := m ⊕ n) (Sum.inl y) ((σ : (a : m ⊕ n) → m ⊕ n) (Sum.inl a))
b : n
hx : Eq (α := m ⊕ n) ((σ : (a : m ⊕ n) → m ⊕ n) (Sum.inl a) : m ⊕ n) (Sum.inr b : m ⊕ n)
convert_2 : fromBlocks A B 0 D ((σ : (a : m ⊕ n) → m ⊕ n) (Sum.inl a)) (Sum.inl a) = 0
⊢ HMul.hMul (α := R) (↑(↑(((sign : Perm (m ⊕ n) →* ℤˣ) : (a : Perm (m ⊕ n)) → ℤˣ) σ) : ℤ) : R)
      (∏ i : m ⊕ n, fromBlocks A B 0 D ((σ : (a : m ⊕ n) → m ⊕ n) i) i) =
    0

Tactic:
rw [Finset.prod_eq_zero (Finset.mem_univ (Sum.inl a)), mul_zero]

Premises used: Finset.mem_univ, Sum.inl, MulZeroClass.mul_zero, Finset.prod_eq_zero
-- Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic
Goal:
m : Type u_1
n : Type u_2
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : DecidableEq m
inst_3 : Fintype m
R : Type v
inst_4 : CommRing R
A : Matrix m m R
B : Matrix m n R
D : Matrix n n R
σ : Perm (m ⊕ n)
hσn : σ ∉ (↑(sumCongrHom m n).range : Set (Perm (m ⊕ n))).toFinset
h1 : ¬∀ (x : m), ∃ (y : m), Eq (α := m ⊕ n) (Sum.inl y) ((σ : (a : m ⊕ n) → m ⊕ n) (Sum.inl x))
a : m
ha : ¬∃ (y : m), Eq (α := m ⊕ n) (Sum.inl y) ((σ : (a : m ⊕ n) → m ⊕ n) (Sum.inl a))
b : n
hx : Eq (α := m ⊕ n) ((σ : (a : m ⊕ n) → m ⊕ n) (Sum.inl a) : m ⊕ n) (Sum.inr b : m ⊕ n)
convert_2 : fromBlocks A B 0 D (Sum.inr b) (Sum.inl a) = 0
convert_2₁ : Eq.{v + 1} (α := R) (0 b a) 0
convert_2₂ convert_2₃ : Eq.{v + 1} (α := R) 0 0
⊢ fromBlocks A B 0 D ((σ : (a : m ⊕ n) → m ⊕ n) (Sum.inl a)) (Sum.inl a) = 0

Tactic:
rw [hx, fromBlocks_apply₂₁, zero_apply]

Premises used: Matrix.zero_apply, Matrix.fromBlocks_apply₂₁
-- Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic
Goal:
m : Type u_1
n : Type u_2
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : DecidableEq m
inst_3 : Fintype m
R : Type v
inst_4 : CommRing R
A : Matrix m m R
C : Matrix n m R
D : Matrix n n R
rw : (fromBlocks A 0 C D)ᵀ.det = A.det * D.det
rw₁ : (fromBlocks Aᵀ Cᵀ 0ᵀ Dᵀ).det = A.det * D.det
rw₂ : (fromBlocks Aᵀ Cᵀ 0 Dᵀ).det = A.det * D.det
rw₃ : Aᵀ.det * Dᵀ.det = A.det * D.det
rw₄ : A.det * Dᵀ.det = A.det * D.det
rw₅ rw₆ : A.det * D.det = A.det * D.det
⊢ (fromBlocks A 0 C D).det = A.det * D.det

Tactic:
rw [← det_transpose, fromBlocks_transpose, transpose_zero, det_fromBlocks_zero₂₁, det_transpose,
    det_transpose]

Premises used: Matrix.det_transpose, Matrix.transpose_zero, Matrix.fromBlocks_transpose, Matrix.det_fromBlocks_zero₂₁
-- Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic
Goal:
R : Type v
inst : CommRing R
n : ℕ
A : Matrix (Fin n.succ) (Fin n.succ) R
rw :
  Eq.{v + 1} (α := R)
    (∑
      σ ∈
        Finset.map (Equiv.toEmbedding (Equiv.symm decomposeFin))
          (SProd.sprod (α := Finset (Fin n.succ)) (β := Finset (Perm (Fin n))) univ univ),
      HSMul.hSMul (α := ℤˣ) (β := R) ((sign : (a : Perm (Fin n.succ)) → ℤˣ) σ : ℤˣ)
        (∏ i : Fin n.succ, A ((σ : (a : Fin n.succ) → Fin n.succ) i) i))
    (∑ i : Fin n.succ, HPow.hPow (α := R) (-1) (↑i : ℕ) * A i 0 * (A.submatrix i.succAbove Fin.succ).det)
⊢ A.det = ∑ i : Fin n.succ, HPow.hPow (α := R) (-1) (↑i : ℕ) * A i 0 * (A.submatrix i.succAbove Fin.succ).det

Tactic:
rw [Matrix.det_apply, Finset.univ_perm_fin_succ, ← Finset.univ_product_univ]

Premises used: Matrix.det_apply, Finset.univ_product_univ, Finset.univ_perm_fin_succ
-- Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic
Goal:
R : Type v
inst : CommRing R
n : ℕ
A : Matrix (Fin n.succ) (Fin n.succ) R
simp :
  Eq.{v + 1} (α := R)
    (∑ x : Fin n.succ,
      ∑ y : Perm (Fin n),
        HSMul.hSMul (α := ℤˣ) (β := R)
          ((sign : (a : Perm (Fin n.succ)) → ℤˣ)
              ((Equiv.symm decomposeFin : (a : Fin n.succ × Perm (Fin n)) → Perm (Fin n.succ)) (x, y)) :
            ℤˣ)
          (∏ x_1 : Fin n.succ,
            A
              ((((Equiv.symm decomposeFin : (a : Fin n.succ × Perm (Fin n)) → Perm (Fin n.succ)) (x, y) :
                    Perm (Fin n.succ)) :
                  (a : Fin n.succ) → Fin n.succ)
                x_1)
              x_1))
    (∑ x : Fin n.succ,
      HPow.hPow (α := R) (-1) (↑x : ℕ) * A x 0 *
        det (n := Fin n)
          ((of : (a : Fin n → Fin n → R) → Matrix (Fin n) (Fin n) R) fun (i j : Fin n) ↦ A (x.succAbove i) j.succ))
⊢ Eq.{v + 1} (α := R)
    (∑
      σ ∈
        Finset.map (Equiv.toEmbedding (Equiv.symm decomposeFin))
          (SProd.sprod (α := Finset (Fin n.succ)) (β := Finset (Perm (Fin n))) univ univ),
      HSMul.hSMul (α := ℤˣ) (β := R) ((sign : (a : Perm (Fin n.succ)) → ℤˣ) σ : ℤˣ)
        (∏ i : Fin n.succ, A ((σ : (a : Fin n.succ) → Fin n.succ) i) i))
    (∑ i : Fin n.succ, HPow.hPow (α := R) (-1) (↑i : ℕ) * A i 0 * (A.submatrix i.succAbove Fin.succ).det)

Tactic:
simp only [Finset.sum_map, Equiv.toEmbedding_apply, Finset.sum_product, Matrix.submatrix]

Premises used: Matrix.submatrix, Finset.sum_map, Equiv.toEmbedding_apply, Finset.sum_product
-- Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic
Goal:
R : Type v
inst : CommRing R
n : ℕ
A : Matrix (Fin n.succ) (Fin n.succ) R
⊢ Eq.{v + 1} (α := R)
    (∑ x : Fin n.succ,
      ∑ y : Perm (Fin n),
        HSMul.hSMul (α := ℤˣ) (β := R)
          ((sign : (a : Perm (Fin n.succ)) → ℤˣ)
              ((Equiv.symm decomposeFin : (a : Fin n.succ × Perm (Fin n)) → Perm (Fin n.succ)) (x, y)) :
            ℤˣ)
          (∏ x_1 : Fin n.succ,
            A
              ((((Equiv.symm decomposeFin : (a : Fin n.succ × Perm (Fin n)) → Perm (Fin n.succ)) (x, y) :
                    Perm (Fin n.succ)) :
                  (a : Fin n.succ) → Fin n.succ)
                x_1)
              x_1))
    (∑ x : Fin n.succ,
      HPow.hPow (α := R) (-1) (↑x : ℕ) * A x 0 *
        det (n := Fin n)
          ((of : (a : Fin n → Fin n → R) → Matrix (Fin n) (Fin n) R) fun (i j : Fin n) ↦ A (x.succAbove i) j.succ))

Tactic:
Finset.sum_congr rfl fun i _ => Fin.cases ?_ (fun i => ?_) i

Premises used: Fin.cases, Finset.sum_congr, rfl
-- Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic
Goal:
R : Type v
inst : CommRing R
n : ℕ
A : Matrix (Fin n.succ) (Fin n.succ) R
refine_1 :
  ∀ (i : Fin n.succ),
    Membership.mem (γ := Finset (Fin n.succ)) univ i →
      ∑ y : Perm (Fin n),
          HSMul.hSMul (α := ℤˣ) (β := R)
            ((sign : (a : Perm (Fin n.succ)) → ℤˣ)
                ((Equiv.symm decomposeFin : (a : Fin n.succ × Perm (Fin n)) → Perm (Fin n.succ)) (0, y)) :
              ℤˣ)
            (∏ x : Fin n.succ,
              A
                ((((Equiv.symm decomposeFin : (a : Fin n.succ × Perm (Fin n)) → Perm (Fin n.succ)) (0, y) :
                      Perm (Fin n.succ)) :
                    (a : Fin n.succ) → Fin n.succ)
                  x)
                x) =
        HPow.hPow (α := R) (-1) (↑0 : ℕ) * A 0 0 *
          det (n := Fin n)
            ((of : (a : Fin n → Fin n → R) → Matrix (Fin n) (Fin n) R) fun (i j : Fin n) ↦ A (Fin.succAbove 0 i) j.succ)
refine_2 :
  ∀ (i : Fin n.succ),
    Membership.mem (γ := Finset (Fin n.succ)) univ i →
      ∀ (i : Fin n),
        ∑ y : Perm (Fin n),
            HSMul.hSMul (α := ℤˣ) (β := R)
              ((sign : (a : Perm (Fin n.succ)) → ℤˣ)
                  ((Equiv.symm decomposeFin : (a : Fin n.succ × Perm (Fin n)) → Perm (Fin n.succ)) (i.succ, y)) :
                ℤˣ)
              (∏ x : Fin n.succ,
                A
                  ((((Equiv.symm decomposeFin : (a : Fin n.succ × Perm (Fin n)) → Perm (Fin n.succ)) (i.succ, y) :
                        Perm (Fin n.succ)) :
                      (a : Fin n.succ) → Fin n.succ)
                    x)
                  x) =
          HPow.hPow (α := R) (-1) (↑i.succ : ℕ) * A i.succ 0 *
            det (n := Fin n)
              ((of : (a : Fin n → Fin n → R) → Matrix (Fin n) (Fin n) R) fun (i_1 j : Fin n) ↦
                A (i.succ.succAbove i_1) j.succ)
⊢ Eq.{v + 1} (α := R)
    (∑ x : Fin n.succ,
      ∑ y : Perm (Fin n),
        HSMul.hSMul (α := ℤˣ) (β := R)
          ((sign : (a : Perm (Fin n.succ)) → ℤˣ)
              ((Equiv.symm decomposeFin : (a : Fin n.succ × Perm (Fin n)) → Perm (Fin n.succ)) (x, y)) :
            ℤˣ)
          (∏ x_1 : Fin n.succ,
            A
              ((((Equiv.symm decomposeFin : (a : Fin n.succ × Perm (Fin n)) → Perm (Fin n.succ)) (x, y) :
                    Perm (Fin n.succ)) :
                  (a : Fin n.succ) → Fin n.succ)
                x_1)
              x_1))
    (∑ x : Fin n.succ,
      HPow.hPow (α := R) (-1) (↑x : ℕ) * A x 0 *
        det (n := Fin n)
          ((of : (a : Fin n → Fin n → R) → Matrix (Fin n) (Fin n) R) fun (i j : Fin n) ↦ A (x.succAbove i) j.succ))

Tactic:
refine Finset.sum_congr rfl fun i _ => Fin.cases ?_ (fun i => ?_) i

Premises used: Fin.cases, Finset.sum_congr, rfl
-- Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic
Goal:
R : Type v
inst : CommRing R
n : ℕ
A : Matrix (Fin n.succ) (Fin n.succ) R
i : Fin n.succ
h : Membership.mem (γ := Finset (Fin n.succ)) univ i
⊢ ∑ y : Perm (Fin n),
      HSMul.hSMul (α := ℤˣ) (β := R)
        ((sign : (a : Perm (Fin n.succ)) → ℤˣ)
            ((Equiv.symm decomposeFin : (a : Fin n.succ × Perm (Fin n)) → Perm (Fin n.succ)) (0, y)) :
          ℤˣ)
        (∏ x : Fin n.succ,
          A
            ((((Equiv.symm decomposeFin : (a : Fin n.succ × Perm (Fin n)) → Perm (Fin n.succ)) (0, y) :
                  Perm (Fin n.succ)) :
                (a : Fin n.succ) → Fin n.succ)
              x)
            x) =
    HPow.hPow (α := R) (-1) (↑0 : ℕ) * A 0 0 *
      det (n := Fin n)
        ((of : (a : Fin n → Fin n → R) → Matrix (Fin n) (Fin n) R) fun (i j : Fin n) ↦ A (Fin.succAbove 0 i) j.succ)

Tactic:
simp only [Fin.prod_univ_succ, Matrix.det_apply, Finset.mul_sum,
      Equiv.Perm.decomposeFin_symm_apply_zero, Fin.val_zero, one_mul,
      Equiv.Perm.decomposeFin.symm_sign, Equiv.swap_self, if_true, id,
      Equiv.Perm.decomposeFin_symm_apply_succ, Fin.succAbove_zero, Equiv.coe_refl, pow_zero,
      mul_smul_comm, of_apply]

Premises used: Matrix.det_apply, Finset.mul_sum, if_true, Equiv.Perm.decomposeFin.symm_sign, id, Matrix.of_apply, pow_zero, Equiv.Perm.decomposeFin_symm_apply_succ, Fin.prod_univ_succ, Equiv.coe_refl, Equiv.swap_self, mul_smul_comm, Fin.succAbove_zero, Fin.val_zero, one_mul, Equiv.Perm.decomposeFin_symm_apply_zero
-- Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic
Goal:
R : Type v
inst : CommRing R
n : ℕ
A : Matrix (Fin n.succ) (Fin n.succ) R
i_1 : Fin n.succ
h : Membership.mem (γ := Finset (Fin n.succ)) univ i_1
i : Fin n
⊢ HPow.hPow (α := R) (-1) (↑i : ℕ) = (↑(↑((sign : (a : Perm (Fin n)) → ℤˣ) i.cycleRange) : ℤ) : R)

Tactic:
simp [Fin.sign_cycleRange]

Premises used: Fin.sign_cycleRange
-- Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic
Goal:
R : Type v
inst : CommRing R
n : ℕ
A : Matrix (Fin n.succ) (Fin n.succ) R
i_1 : Fin n.succ
h : Membership.mem (γ := Finset (Fin n.succ)) univ i_1
i : Fin n
⊢ HPow.hPow (α := R) (-1) (↑i : ℕ) = (↑(↑((sign : (a : Perm (Fin n)) → ℤˣ) i.cycleRange) : ℤ) : R)

Tactic:
have : (-1 : R) ^ (i : ℕ) = (Perm.sign i.cycleRange) := by simp [Fin.sign_cycleRange]