awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.Basic (goal)
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
⊢ (fromBlocks A B 0 D).det = A.det * D.det
have simp_rw : ∑ σ : Perm (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) =
  HMul.hMul (α := R)
    (∑ σ : Perm m,
      HMul.hMul (α := R) (↑(↑(((sign : Perm m →* ℤˣ) : (a : Perm m) → ℤˣ) σ) : ℤ) : R)
        (∏ i : m, A ((σ : (a : m) → m) i) i))
    (∑ σ : Perm n,
      HMul.hMul (α := R) (↑(↑(((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) σ) : ℤ) : R)
        (∏ i : n, D ((σ : (a : n) → n) i) i))
Tactic: classical
    simp_rw [det_apply']
    convert!
      Eq.symm <|
        sum_subset (M := R) (subset_univ ((sumCongrHom m n).range : Set (Perm (m ⊕ n))).toFinset) ?_
    · simp_rw [sum_mul_sum, ← sum_product', univ_product_univ]
      refine sum_nbij (fun σ ↦ σ.fst.sumCongr σ.snd) ?_ ?_ ?_ ?_
      · intro σ₁₂ _
        simp
      · intro σ₁ _ σ₂ _
        dsimp only
        intro h
        have h2 : ∀ x, Perm.sumCongr σ₁.fst σ₁.snd x = Perm.sumCongr σ₂.fst σ₂.snd x :=
          DFunLike.congr_fun h
        simp only [Sum.map_inr, Sum.map_inl, Perm.sumCongr_apply, Sum.forall, Sum.inl.injEq,
          Sum.inr.injEq] at h2
        ext x
        · exact h2.left x
        · exact h2.right x
      · intro σ hσ
        rw [mem_coe, Set.mem_toFinset] at hσ
        obtain ⟨σ₁₂, hσ₁₂⟩ := hσ
        use σ₁₂
        rw [← hσ₁₂]
        simp
      · simp only [forall_prop_of_true, Prod.forall, mem_univ]
        intro σ₁ σ₂
        rw [Fintype.prod_sum_type]
        simp_rw [Equiv.sumCongr_apply, Sum.map_inr, Sum.map_inl, fromBlocks_apply₁₁,
          fromBlocks_apply₂₂]
        rw [mul_mul_mul_comm]
        congr
        rw [sign_sumCongr, Units.val_mul, Int.cast_mul]
    · rintro σ - hσn
      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
      obtain ⟨a, ha⟩ := not_forall.mp h1
      rcases hx : σ (Sum.inl a) with a2 | b
      · have hn := (not_exists.mp ha) a2
        exact absurd hx.symm hn
      · rw [Finset.prod_eq_zero (Finset.mem_univ (Sum.inl a)), mul_zero]
        rw [hx, fromBlocks_apply₂₁, zero_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.Basic (goal)
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
simp_rw :
  ∑ σ : Perm (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) =
    HMul.hMul (α := R)
      (∑ σ : Perm m,
        HMul.hMul (α := R) (↑(↑(((sign : Perm m →* ℤˣ) : (a : Perm m) → ℤˣ) σ) : ℤ) : R)
          (∏ i : m, A ((σ : (a : m) → m) i) i))
      (∑ σ : Perm n,
        HMul.hMul (α := R) (↑(↑(((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) σ) : ℤ) : R)
          (∏ i : n, D ((σ : (a : n) → n) i) i))
⊢ (fromBlocks A B 0 D).det = A.det * D.det
have h : HMul.hMul (α := R)
    (∑ σ : Perm m,
      HMul.hMul (α := R) (↑(↑(((sign : Perm m →* ℤˣ) : (a : Perm m) → ℤˣ) σ) : ℤ) : R)
        (∏ i : m, A ((σ : (a : m) → m) i) i))
    (∑ σ : Perm n,
      HMul.hMul (α := R) (↑(↑(((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) σ) : ℤ) : R)
        (∏ i : n, D ((σ : (a : n) → n) i) i)) =
  ∑ x ∈ (↑(sumCongrHom m n).range : Set (Perm (m ⊕ n))).toFinset,
    HMul.hMul (α := R) (↑(↑(((sign : Perm (m ⊕ n) →* ℤˣ) : (a : Perm (m ⊕ n)) → ℤˣ) x) : ℤ) : R)
      (∏ i : m ⊕ n, fromBlocks A B 0 D ((x : (a : m ⊕ n) → m ⊕ n) i) i)
Tactic: classical
    simp_rw [det_apply']
    convert!
      Eq.symm <|
        sum_subset (M := R) (subset_univ ((sumCongrHom m n).range : Set (Perm (m ⊕ n))).toFinset) ?_
    · simp_rw [sum_mul_sum, ← sum_product', univ_product_univ]
      refine sum_nbij (fun σ ↦ σ.fst.sumCongr σ.snd) ?_ ?_ ?_ ?_
      · intro σ₁₂ _
        simp
      · intro σ₁ _ σ₂ _
        dsimp only
        intro h
        have h2 : ∀ x, Perm.sumCongr σ₁.fst σ₁.snd x = Perm.sumCongr σ₂.fst σ₂.snd x :=
          DFunLike.congr_fun h
        simp only [Sum.map_inr, Sum.map_inl, Perm.sumCongr_apply, Sum.forall, Sum.inl.injEq,
          Sum.inr.injEq] at h2
        ext x
        · exact h2.left x
        · exact h2.right x
      · intro σ hσ
        rw [mem_coe, Set.mem_toFinset] at hσ
        obtain ⟨σ₁₂, hσ₁₂⟩ := hσ
        use σ₁₂
        rw [← hσ₁₂]
        simp
      · simp only [forall_prop_of_true, Prod.forall, mem_univ]
        intro σ₁ σ₂
        rw [Fintype.prod_sum_type]
        simp_rw [Equiv.sumCongr_apply, Sum.map_inr, Sum.map_inl, fromBlocks_apply₁₁,
          fromBlocks_apply₂₂]
        rw [mul_mul_mul_comm]
        congr
        rw [sign_sumCongr, Units.val_mul, Int.cast_mul]
    · rintro σ - hσn
      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
      obtain ⟨a, ha⟩ := not_forall.mp h1
      rcases hx : σ (Sum.inl a) with a2 | b
      · have hn := (not_exists.mp ha) a2
        exact absurd hx.symm hn
      · rw [Finset.prod_eq_zero (Finset.mem_univ (Sum.inl a)), mul_zero]
        rw [hx, fromBlocks_apply₂₁, zero_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.Basic (goal)
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
⊢ (fromBlocks A 0 C D).det = A.det * D.det
have rw : (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]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.Basic (goal)
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
⊢ (fromBlocks A 0 C D).det = A.det * D.det
have rw₁ : (fromBlocks Aᵀ Cᵀ 0ᵀ Dᵀ).det = A.det * D.det
Tactic: rw [← det_transpose, fromBlocks_transpose, transpose_zero, det_fromBlocks_zero₂₁, det_transpose,
    det_transpose]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.Basic (goal)
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
⊢ (fromBlocks A 0 C D).det = A.det * D.det
have rw₂ : (fromBlocks Aᵀ Cᵀ 0 Dᵀ).det = A.det * D.det
Tactic: rw [← det_transpose, fromBlocks_transpose, transpose_zero, det_fromBlocks_zero₂₁, det_transpose,
    det_transpose]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.Basic (goal)
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
⊢ (fromBlocks A 0 C D).det = A.det * D.det
have rw₃ : Aᵀ.det * Dᵀ.det = A.det * D.det
Tactic: rw [← det_transpose, fromBlocks_transpose, transpose_zero, det_fromBlocks_zero₂₁, det_transpose,
    det_transpose]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.Basic (goal)
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
⊢ (fromBlocks A 0 C D).det = A.det * D.det
have rw₄ : A.det * Dᵀ.det = A.det * D.det
Tactic: rw [← det_transpose, fromBlocks_transpose, transpose_zero, det_fromBlocks_zero₂₁, det_transpose,
    det_transpose]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.Basic (goal)
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
⊢ (fromBlocks A 0 C D).det = A.det * D.det
have rw₅ : A.det * D.det = A.det * D.det
Tactic: rw [← det_transpose, fromBlocks_transpose, transpose_zero, det_fromBlocks_zero₂₁, det_transpose,
    det_transpose]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.Basic (goal)
Goal:
R : Type v
inst : CommRing R
n : ℕ
A : Matrix (Fin n.succ) (Fin n.succ) R
⊢ A.det = ∑ i : Fin n.succ, HPow.hPow (α := R) (-1) (↑i : ℕ) * A i 0 * (A.submatrix i.succAbove Fin.succ).det
have 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)
Tactic: rw [Matrix.det_apply, Finset.univ_perm_fin_succ, ← Finset.univ_product_univ]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.Basic (goal)
Goal:
R : Type v
inst : CommRing R
n : ℕ
A : Matrix (Fin n.succ) (Fin n.succ) R
⊢ 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)
have 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))
Tactic: simp only [Finset.sum_map, Equiv.toEmbedding_apply, Finset.sum_product, Matrix.submatrix]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.Basic (goal)
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))
have 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)
Tactic: refine Finset.sum_congr rfl fun i _ => Fin.cases ?_ (fun i => ?_) i
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.Basic (goal)
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)
⊢ 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))
have 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)
Tactic: refine Finset.sum_congr rfl fun i _ => Fin.cases ?_ (fun i => ?_) i
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.Basic (hypothesis)
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
⊢ ∑ 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_2 j : Fin n) ↦
          A (i.succ.succAbove i_2) j.succ)
have this : 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]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.Basic (goal)
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
this : HPow.hPow (α := R) (-1) (↑i : ℕ) = (↑(↑((sign : (a : Perm (Fin n)) → ℤˣ) i.cycleRange) : ℤ) : R)
⊢ ∑ 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_2 j : Fin n) ↦
          A (i.succ.succAbove i_2) j.succ)
have refine_2 : Eq.{v + 1} (α := R)
  (∑ 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))
  (∑ i_2 : Perm (Fin n),
    -1 *
      (A i.succ 0 *
        HSMul.hSMul (α := ℤˣ) (β := R) ((sign : (a : Perm (Fin n)) → ℤˣ) i_2 : ℤˣ)
          (∏ i_3 : Fin n,
            submatrix (l := Fin n) (m := Fin n)
              ((of : (a : Fin n → Fin n → R) → Matrix (Fin n) (Fin n) R) fun (i_4 j : Fin n) ↦
                A (i.succ.succAbove i_4) j.succ)
              ((⇑i.cycleRange : (a : Fin n) → Fin n) : (a : Fin n) → Fin n) id ((i_2 : (a : Fin n) → Fin n) i_3 : Fin n)
              i_3)))
Tactic: rw [Fin.val_succ, pow_succ', this, mul_assoc, mul_assoc, mul_left_comm (ε _),
    ← det_permute, Matrix.det_apply, Finset.mul_sum, Finset.mul_sum]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.Basic (goal)
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
this : HPow.hPow (α := R) (-1) (↑i : ℕ) = (↑(↑((sign : (a : Perm (Fin n)) → ℤˣ) i.cycleRange) : ℤ) : R)
⊢ Eq.{v + 1} (α := R)
    (∑ 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))
    (∑ i_2 : Perm (Fin n),
      -1 *
        (A i.succ 0 *
          HSMul.hSMul (α := ℤˣ) (β := R) ((sign : (a : Perm (Fin n)) → ℤˣ) i_2 : ℤˣ)
            (∏ i_3 : Fin n,
              submatrix (l := Fin n) (m := Fin n)
                ((of : (a : Fin n → Fin n → R) → Matrix (Fin n) (Fin n) R) fun (i_4 j : Fin n) ↦
                  A (i.succ.succAbove i_4) j.succ)
                ((⇑i.cycleRange : (a : Fin n) → Fin n) : (a : Fin n) → Fin n) id
                ((i_2 : (a : Fin n) → Fin n) i_3 : Fin n) i_3)))
have refine_2 : ∀ (σ : Perm (Fin n)),
  Membership.mem (γ := Finset (Perm (Fin n))) univ σ →
    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, σ)) :
          ℤˣ)
        (∏ x : Fin n.succ,
          A
            ((((Equiv.symm decomposeFin : (a : Fin n.succ × Perm (Fin n)) → Perm (Fin n.succ)) (i.succ, σ) :
                  Perm (Fin n.succ)) :
                (a : Fin n.succ) → Fin n.succ)
              x)
            x) =
      -1 *
        (A i.succ 0 *
          HSMul.hSMul (α := ℤˣ) (β := R) ((sign : (a : Perm (Fin n)) → ℤˣ) σ : ℤˣ)
            (∏ i_2 : Fin n,
              submatrix (l := Fin n) (m := Fin n)
                ((of : (a : Fin n → Fin n → R) → Matrix (Fin n) (Fin n) R) fun (i_3 j : Fin n) ↦
                  A (i.succ.succAbove i_3) j.succ)
                ((⇑i.cycleRange : (a : Fin n) → Fin n) : (a : Fin n) → Fin n) id ((σ : (a : Fin n) → Fin n) i_2 : Fin n)
                i_2))
Tactic: refine Finset.sum_congr rfl fun σ _ => ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.Basic (goal)
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
this : HPow.hPow (α := R) (-1) (↑i : ℕ) = (↑(↑((sign : (a : Perm (Fin n)) → ℤˣ) i.cycleRange) : ℤ) : R)
σ : Perm (Fin n)
h_1 : Membership.mem (γ := Finset (Perm (Fin n))) univ σ
⊢ 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, σ)) :
        ℤˣ)
      (∏ x : Fin n.succ,
        A
          ((((Equiv.symm decomposeFin : (a : Fin n.succ × Perm (Fin n)) → Perm (Fin n.succ)) (i.succ, σ) :
                Perm (Fin n.succ)) :
              (a : Fin n.succ) → Fin n.succ)
            x)
          x) =
    -1 *
      (A i.succ 0 *
        HSMul.hSMul (α := ℤˣ) (β := R) ((sign : (a : Perm (Fin n)) → ℤˣ) σ : ℤˣ)
          (∏ i_2 : Fin n,
            submatrix (l := Fin n) (m := Fin n)
              ((of : (a : Fin n → Fin n → R) → Matrix (Fin n) (Fin n) R) fun (i_3 j : Fin n) ↦
                A (i.succ.succAbove i_3) j.succ)
              ((⇑i.cycleRange : (a : Fin n) → Fin n) : (a : Fin n) → Fin n) id ((σ : (a : Fin n) → Fin n) i_2 : Fin n)
              i_2))
have refine_2 : HSMul.hSMul (β := R) (HMul.hMul (α := ℤˣ) (β := ℤˣ) (-1 : ℤˣ) ((sign : (a : Perm (Fin n)) → ℤˣ) σ : ℤˣ))
    (∏ x : Fin n.succ,
      A
        ((((Equiv.symm decomposeFin : (a : Fin n.succ × Perm (Fin n)) → Perm (Fin n.succ)) (i.succ, σ) :
              Perm (Fin n.succ)) :
            (a : Fin n.succ) → Fin n.succ)
          x)
        x) =
  -1 *
    (A i.succ 0 *
      HSMul.hSMul (α := ℤˣ) (β := R) ((sign : (a : Perm (Fin n)) → ℤˣ) σ : ℤˣ)
        (∏ i_2 : Fin n,
          submatrix (l := Fin n) (m := Fin n)
            ((of : (a : Fin n → Fin n → R) → Matrix (Fin n) (Fin n) R) fun (i_3 j : Fin n) ↦
              A (i.succ.succAbove i_3) j.succ)
            ((⇑i.cycleRange : (a : Fin n) → Fin n) : (a : Fin n) → Fin n) id ((σ : (a : Fin n) → Fin n) i_2 : Fin n)
            i_2))
Tactic: rw [Equiv.Perm.decomposeFin.symm_sign, if_neg (Fin.succ_ne_zero i)]