awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic
Goal:
n : Type u_2
inst : DecidableEq n
inst_1 : Fintype n
R : Type v
inst_2 : CommRing R
o : Type u_3
inst_3 : Fintype o
inst_4 : DecidableEq o
M : o → Matrix n n R
preserving_snd : Finset (Perm (n × o)) := {σ : Perm (n × o) | ∀ (x : n × o), ((σ : (a : n × o) → n × o) x).2 = x.2}
mem_preserving_snd : ∀ {σ : Perm (n × o)}, σ ∈ preserving_snd ↔ ∀ (x : n × o), ((σ : (a : n × o) → n × o) x).2 = x.2
σ : n × o ≃ n × o
hσ : ∀ (x : n × o), ((σ : (a : n × o) → n × o) x).2 = x.2
hσ' : ∀ (x : n × o), ((σ.symm : (a : n × o) → n × o) x).2 = x.2
mk_apply_eq :
  ∀ (k : o) (x : n), Eq (α := n × o) (((σ : (a : n × o) → n × o) (x, k)).1, k) ((σ : (a : n × o) → n × o) (x, k))
mk_inv_apply_eq :
  ∀ (k : o) (x : n),
    Eq (α := n × o) (((σ.symm : (a : n × o) → n × o) (x, k)).1, k) ((σ.symm : (a : n × o) → n × o) (x, k))
⊢ Membership.mem (γ := Finset ((a : o) → Membership.mem (γ := Finset o) univ a → Perm n)) univ
    fun (k : o) (x : Membership.mem (γ := Finset o) univ k) ↦
    { toFun := fun (x : n) ↦ ((σ : (a : n × o) → n × o) (x, k)).1,
      invFun := fun (x : n) ↦ ((σ.symm : (a : n × o) → n × o) (x, k)).1, left_inv := ⋯, right_inv := ⋯ }

Tactic:
apply Finset.mem_univ

Premises used: Finset.mem_univ
-- Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic
Goal:
n : Type u_2
inst : DecidableEq n
inst_1 : Fintype n
R : Type v
inst_2 : CommRing R
o : Type u_3
inst_3 : Fintype o
inst_4 : DecidableEq o
M : o → Matrix n n R
preserving_snd : Finset (Perm (n × o)) := {σ : Perm (n × o) | ∀ (x : n × o), ((σ : (a : n × o) → n × o) x).2 = x.2}
mem_preserving_snd : ∀ {σ : Perm (n × o)}, σ ∈ preserving_snd ↔ ∀ (x : n × o), ((σ : (a : n × o) → n × o) x).2 = x.2
σ : n × o ≃ n × o
hσ : ∀ (x : n × o), ((σ : (a : n × o) → n × o) x).2 = x.2
hσ' : ∀ (x : n × o), ((σ.symm : (a : n × o) → n × o) x).2 = x.2
mk_apply_eq :
  ∀ (k : o) (x : n), Eq (α := n × o) (((σ : (a : n × o) → n × o) (x, k)).1, k) ((σ : (a : n × o) → n × o) (x, k))
mk_inv_apply_eq :
  ∀ (k : o) (x : n),
    Eq (α := n × o) (((σ.symm : (a : n × o) → n × o) (x, k)).1, k) ((σ.symm : (a : n × o) → n × o) (x, k))
refine_3 :
  ∀ (k : n) (x : o),
    Eq.{u_2 + 1} (α := n)
      (((fun (σ : (a : o) → Membership.mem (γ := Finset o) univ a → Perm n)
                  (x : Membership.mem (γ := Finset ((a : o) → Membership.mem (γ := Finset o) univ a → Perm n)) univ σ) ↦
                (prodCongrLeft fun (k : o) ↦ σ k ⋯ : n × o ≃ n × o))
              (fun (k : o) (x : Membership.mem (γ := Finset o) univ k) ↦
                { toFun := fun (x : n) ↦ ((σ : (a : n × o) → n × o) (x, k)).1,
                  invFun := fun (x : n) ↦ ((σ.symm : (a : n × o) → n × o) (x, k)).1, left_inv := ⋯, right_inv := ⋯ })
              ⋯ :
            (a : n × o) → n × o)
          (k, x)).1
      ((σ : (a : n × o) → n × o) (k, x)).1
refine_3₁ :
  ∀ (k : n) (x : o),
    Eq.{u_3 + 1} (α := o)
      (((fun (σ : (a : o) → Membership.mem (γ := Finset o) univ a → Perm n)
                  (x : Membership.mem (γ := Finset ((a : o) → Membership.mem (γ := Finset o) univ a → Perm n)) univ σ) ↦
                (prodCongrLeft fun (k : o) ↦ σ k ⋯ : n × o ≃ n × o))
              (fun (k : o) (x : Membership.mem (γ := Finset o) univ k) ↦
                { toFun := fun (x : n) ↦ ((σ : (a : n × o) → n × o) (x, k)).1,
                  invFun := fun (x : n) ↦ ((σ.symm : (a : n × o) → n × o) (x, k)).1, left_inv := ⋯, right_inv := ⋯ })
              ⋯ :
            (a : n × o) → n × o)
          (k, x)).2
      ((σ : (a : n × o) → n × o) (k, x)).2
⊢ (fun (σ : (a : o) → Membership.mem (γ := Finset o) univ a → Perm n)
          (x : Membership.mem (γ := Finset ((a : o) → Membership.mem (γ := Finset o) univ a → Perm n)) univ σ) ↦
        (prodCongrLeft fun (k : o) ↦ σ k ⋯ : n × o ≃ n × o))
      (fun (k : o) (x : Membership.mem (γ := Finset o) univ k) ↦
        { toFun := fun (x : n) ↦ ((σ : (a : n × o) → n × o) (x, k)).1,
          invFun := fun (x : n) ↦ ((σ.symm : (a : n × o) → n × o) (x, k)).1, left_inv := ⋯, right_inv := ⋯ })
      ⋯ =
    σ

Tactic:
ext ⟨k, x⟩
-- Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic
Goal:
n : Type u_2
inst : DecidableEq n
inst_1 : Fintype n
R : Type v
inst_2 : CommRing R
o : Type u_3
inst_3 : Fintype o
inst_4 : DecidableEq o
M : o → Matrix n n R
preserving_snd : Finset (Perm (n × o)) := {σ : Perm (n × o) | ∀ (x : n × o), ((σ : (a : n × o) → n × o) x).2 = x.2}
mem_preserving_snd : ∀ {σ : Perm (n × o)}, σ ∈ preserving_snd ↔ ∀ (x : n × o), ((σ : (a : n × o) → n × o) x).2 = x.2
σ : n × o ≃ n × o
hσ : ∀ (x : n × o), ((σ : (a : n × o) → n × o) x).2 = x.2
hσ' : ∀ (x : n × o), ((σ.symm : (a : n × o) → n × o) x).2 = x.2
mk_apply_eq :
  ∀ (k : o) (x : n), Eq (α := n × o) (((σ : (a : n × o) → n × o) (x, k)).1, k) ((σ : (a : n × o) → n × o) (x, k))
mk_inv_apply_eq :
  ∀ (k : o) (x : n),
    Eq (α := n × o) (((σ.symm : (a : n × o) → n × o) (x, k)).1, k) ((σ.symm : (a : n × o) → n × o) (x, k))
k : n
x : o
⊢ Eq.{u_2 + 1} (α := n)
    (((fun (σ : (a : o) → Membership.mem (γ := Finset o) univ a → Perm n)
                (x : Membership.mem (γ := Finset ((a : o) → Membership.mem (γ := Finset o) univ a → Perm n)) univ σ) ↦
              (prodCongrLeft fun (k : o) ↦ σ k ⋯ : n × o ≃ n × o))
            (fun (k : o) (x : Membership.mem (γ := Finset o) univ k) ↦
              { toFun := fun (x : n) ↦ ((σ : (a : n × o) → n × o) (x, k)).1,
                invFun := fun (x : n) ↦ ((σ.symm : (a : n × o) → n × o) (x, k)).1, left_inv := ⋯, right_inv := ⋯ })
            ⋯ :
          (a : n × o) → n × o)
        (k, x)).1
    ((σ : (a : n × o) → n × o) (k, x)).1

Tactic:
simp only [coe_fn_mk, prodCongrLeft_apply]

Premises used: Equiv.prodCongrLeft_apply, Equiv.coe_fn_mk
-- Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic
Goal:
n : Type u_2
inst : DecidableEq n
inst_1 : Fintype n
R : Type v
inst_2 : CommRing R
o : Type u_3
inst_3 : Fintype o
inst_4 : DecidableEq o
M : o → Matrix n n R
preserving_snd : Finset (Perm (n × o)) := {σ : Perm (n × o) | ∀ (x : n × o), ((σ : (a : n × o) → n × o) x).2 = x.2}
mem_preserving_snd : ∀ {σ : Perm (n × o)}, σ ∈ preserving_snd ↔ ∀ (x : n × o), ((σ : (a : n × o) → n × o) x).2 = x.2
σ : n × o ≃ n × o
hσ : ∀ (x : n × o), ((σ : (a : n × o) → n × o) x).2 = x.2
hσ' : ∀ (x : n × o), ((σ.symm : (a : n × o) → n × o) x).2 = x.2
mk_apply_eq :
  ∀ (k : o) (x : n), Eq (α := n × o) (((σ : (a : n × o) → n × o) (x, k)).1, k) ((σ : (a : n × o) → n × o) (x, k))
mk_inv_apply_eq :
  ∀ (k : o) (x : n),
    Eq (α := n × o) (((σ.symm : (a : n × o) → n × o) (x, k)).1, k) ((σ.symm : (a : n × o) → n × o) (x, k))
k : n
x : o
⊢ Eq.{u_3 + 1} (α := o)
    (((fun (σ : (a : o) → Membership.mem (γ := Finset o) univ a → Perm n)
                (x : Membership.mem (γ := Finset ((a : o) → Membership.mem (γ := Finset o) univ a → Perm n)) univ σ) ↦
              (prodCongrLeft fun (k : o) ↦ σ k ⋯ : n × o ≃ n × o))
            (fun (k : o) (x : Membership.mem (γ := Finset o) univ k) ↦
              { toFun := fun (x : n) ↦ ((σ : (a : n × o) → n × o) (x, k)).1,
                invFun := fun (x : n) ↦ ((σ.symm : (a : n × o) → n × o) (x, k)).1, left_inv := ⋯, right_inv := ⋯ })
            ⋯ :
          (a : n × o) → n × o)
        (k, x)).2
    ((σ : (a : n × o) → n × o) (k, x)).2

Tactic:
simp only [prodCongrLeft_apply, hσ]

Premises used: Equiv.prodCongrLeft_apply
-- Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic
Goal:
n : Type u_2
inst : DecidableEq n
inst_1 : Fintype n
R : Type v
inst_2 : CommRing R
o : Type u_3
inst_3 : Fintype o
inst_4 : DecidableEq o
M : o → Matrix n n R
preserving_snd : Finset (Perm (n × o)) := {σ : Perm (n × o) | ∀ (x : n × o), ((σ : (a : n × o) → n × o) x).2 = x.2}
mem_preserving_snd : ∀ {σ : Perm (n × o)}, σ ∈ preserving_snd ↔ ∀ (x : n × o), ((σ : (a : n × o) → n × o) x).2 = x.2
σ : (a : o) → Membership.mem (γ := Finset o) univ a → Perm n
refine_4 :
  ∀ (ha : Membership.mem (γ := Finset ((a : o) → Membership.mem (γ := Finset o) univ a → Perm n)) univ σ),
    ∏ x : o,
        HMul.hMul (α := R) (↑(↑(((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) (σ x ⋯)) : ℤ) : R)
          (∏ x_1 : n, M x ((σ x ⋯ : (a : n) → n) x_1) x_1) =
      HMul.hMul (α := R)
        (↑(↑(((sign : Perm (n × o) →* ℤˣ) : (a : Perm (n × o)) → ℤˣ)
                  ((fun (σ : (a : o) → Membership.mem (γ := Finset o) univ a → Perm n)
                        (x :
                          Membership.mem (γ := Finset ((a : o) → Membership.mem (γ := Finset o) univ a → Perm n)) univ
                            σ) ↦
                      (prodCongrLeft fun (k : o) ↦ σ k ⋯ : n × o ≃ n × o))
                    σ ha)) :
              ℤ) :
          R)
        (∏ i : n × o,
          blockDiagonal M
            (((fun (σ : (a : o) → Membership.mem (γ := Finset o) univ a → Perm n)
                      (x :
                        Membership.mem (γ := Finset ((a : o) → Membership.mem (γ := Finset o) univ a → Perm n)) univ
                          σ) ↦
                    (prodCongrLeft fun (k : o) ↦ σ k ⋯ : n × o ≃ n × o))
                  σ ha :
                (a : n × o) → n × o)
              i)
            i)
⊢ ∀ (ha : Membership.mem (γ := Finset ((a : o) → Membership.mem (γ := Finset o) univ a → Perm n)) univ σ),
    ∏ x : o,
        HMul.hMul (α := R) (↑(↑(((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) (σ x ⋯)) : ℤ) : R)
          (∏ x_1 : n, M x ((σ x ⋯ : (a : n) → n) x_1) x_1) =
      HMul.hMul (α := R)
        (↑(↑(((sign : Perm (n × o) →* ℤˣ) : (a : Perm (n × o)) → ℤˣ)
                  ((fun (σ : (a : o) → Membership.mem (γ := Finset o) univ a → Perm n)
                        (x :
                          Membership.mem (γ := Finset ((a : o) → Membership.mem (γ := Finset o) univ a → Perm n)) univ
                            σ) ↦
                      (prodCongrLeft fun (k : o) ↦ σ k ⋯ : n × o ≃ n × o))
                    σ ha)) :
              ℤ) :
          R)
        (∏ i : n × o,
          blockDiagonal M
            (((fun (σ : (a : o) → Membership.mem (γ := Finset o) univ a → Perm n)
                      (x :
                        Membership.mem (γ := Finset ((a : o) → Membership.mem (γ := Finset o) univ a → Perm n)) univ
                          σ) ↦
                    (prodCongrLeft fun (k : o) ↦ σ k ⋯ : n × o ≃ n × o))
                  σ ha :
                (a : n × o) → n × o)
              i)
            i)

Tactic:
_
-- Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic
Goal:
n : Type u_2
inst : DecidableEq n
inst_1 : Fintype n
R : Type v
inst_2 : CommRing R
o : Type u_3
inst_3 : Fintype o
inst_4 : DecidableEq o
M : o → Matrix n n R
preserving_snd : Finset (Perm (n × o)) := {σ : Perm (n × o) | ∀ (x : n × o), ((σ : (a : n × o) → n × o) x).2 = x.2}
mem_preserving_snd : ∀ {σ : Perm (n × o)}, σ ∈ preserving_snd ↔ ∀ (x : n × o), ((σ : (a : n × o) → n × o) x).2 = x.2
σ : (a : o) → Membership.mem (γ := Finset o) univ a → Perm n
ha : Membership.mem (γ := Finset ((a : o) → Membership.mem (γ := Finset o) univ a → Perm n)) univ σ
refine_4 :
  HMul.hMul (α := R) (∏ x : o, (↑(↑(((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) (σ x ⋯)) : ℤ) : R))
      (∏ x : o, ∏ x_1 : n, M x ((σ x ⋯ : (a : n) → n) x_1) x_1) =
    HMul.hMul (α := R)
      (↑(↑(((sign : Perm (n × o) →* ℤˣ) : (a : Perm (n × o)) → ℤˣ)
                ((fun (σ : (a : o) → Membership.mem (γ := Finset o) univ a → Perm n)
                      (x :
                        Membership.mem (γ := Finset ((a : o) → Membership.mem (γ := Finset o) univ a → Perm n)) univ
                          σ) ↦
                    (prodCongrLeft fun (k : o) ↦ σ k ⋯ : n × o ≃ n × o))
                  σ ha)) :
            ℤ) :
        R)
      (∏ y : o,
        ∏ x : n,
          blockDiagonal M
            (((fun (σ : (a : o) → Membership.mem (γ := Finset o) univ a → Perm n)
                      (x :
                        Membership.mem (γ := Finset ((a : o) → Membership.mem (γ := Finset o) univ a → Perm n)) univ
                          σ) ↦
                    (prodCongrLeft fun (k : o) ↦ σ k ⋯ : n × o ≃ n × o))
                  σ ha :
                (a : n × o) → n × o)
              (x, y))
            (x, y))
⊢ ∏ x : o,
      HMul.hMul (α := R) (↑(↑(((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) (σ x ⋯)) : ℤ) : R)
        (∏ x_1 : n, M x ((σ x ⋯ : (a : n) → n) x_1) x_1) =
    HMul.hMul (α := R)
      (↑(↑(((sign : Perm (n × o) →* ℤˣ) : (a : Perm (n × o)) → ℤˣ)
                ((fun (σ : (a : o) → Membership.mem (γ := Finset o) univ a → Perm n)
                      (x :
                        Membership.mem (γ := Finset ((a : o) → Membership.mem (γ := Finset o) univ a → Perm n)) univ
                          σ) ↦
                    (prodCongrLeft fun (k : o) ↦ σ k ⋯ : n × o ≃ n × o))
                  σ ha)) :
            ℤ) :
        R)
      (∏ i : n × o,
        blockDiagonal M
          (((fun (σ : (a : o) → Membership.mem (γ := Finset o) univ a → Perm n)
                    (x :
                      Membership.mem (γ := Finset ((a : o) → Membership.mem (γ := Finset o) univ a → Perm n)) univ σ) ↦
                  (prodCongrLeft fun (k : o) ↦ σ k ⋯ : n × o ≃ n × o))
                σ ha :
              (a : n × o) → n × o)
            i)
          i)

Tactic:
rw [Finset.prod_mul_distrib, ← Finset.univ_product_univ, Finset.prod_product_right]

Premises used: Finset.prod_mul_distrib, Finset.univ_product_univ, Finset.prod_product_right
-- Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic
Goal:
n : Type u_2
inst : DecidableEq n
inst_1 : Fintype n
R : Type v
inst_2 : CommRing R
o : Type u_3
inst_3 : Fintype o
inst_4 : DecidableEq o
M : o → Matrix n n R
preserving_snd : Finset (Perm (n × o)) := {σ : Perm (n × o) | ∀ (x : n × o), ((σ : (a : n × o) → n × o) x).2 = x.2}
mem_preserving_snd : ∀ {σ : Perm (n × o)}, σ ∈ preserving_snd ↔ ∀ (x : n × o), ((σ : (a : n × o) → n × o) x).2 = x.2
σ : (a : o) → Membership.mem (γ := Finset o) univ a → Perm n
ha : Membership.mem (γ := Finset ((a : o) → Membership.mem (γ := Finset o) univ a → Perm n)) univ σ
⊢ HMul.hMul (α := R) (∏ x : o, (↑(↑(((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) (σ x ⋯)) : ℤ) : R))
      (∏ x : o, ∏ x_1 : n, M x ((σ x ⋯ : (a : n) → n) x_1) x_1) =
    HMul.hMul (α := R)
      (↑(↑(((sign : Perm (n × o) →* ℤˣ) : (a : Perm (n × o)) → ℤˣ)
                ((fun (σ : (a : o) → Membership.mem (γ := Finset o) univ a → Perm n)
                      (x :
                        Membership.mem (γ := Finset ((a : o) → Membership.mem (γ := Finset o) univ a → Perm n)) univ
                          σ) ↦
                    (prodCongrLeft fun (k : o) ↦ σ k ⋯ : n × o ≃ n × o))
                  σ ha)) :
            ℤ) :
        R)
      (∏ y : o,
        ∏ x : n,
          blockDiagonal M
            (((fun (σ : (a : o) → Membership.mem (γ := Finset o) univ a → Perm n)
                      (x :
                        Membership.mem (γ := Finset ((a : o) → Membership.mem (γ := Finset o) univ a → Perm n)) univ
                          σ) ↦
                    (prodCongrLeft fun (k : o) ↦ σ k ⋯ : n × o ≃ n × o))
                  σ ha :
                (a : n × o) → n × o)
              (x, y))
            (x, y))

Tactic:
simp only [sign_prodCongrLeft, Units.coe_prod, Int.cast_prod, blockDiagonal_apply_eq,
        prodCongrLeft_apply]

Premises used: Units.coe_prod, Matrix.blockDiagonal_apply_eq, Equiv.prodCongrLeft_apply, Equiv.Perm.sign_prodCongrLeft, Int.cast_prod
-- Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic
Goal:
n : Type u_2
inst : DecidableEq n
inst_1 : Fintype n
R : Type v
inst_2 : CommRing R
o : Type u_3
inst_3 : Fintype o
inst_4 : DecidableEq o
M : o → Matrix n n R
preserving_snd : Finset (Perm (n × o)) := {σ : Perm (n × o) | ∀ (x : n × o), ((σ : (a : n × o) → n × o) x).2 = x.2}
mem_preserving_snd : ∀ {σ : Perm (n × o)}, σ ∈ preserving_snd ↔ ∀ (x : n × o), ((σ : (a : n × o) → n × o) x).2 = x.2
σ : Perm (n × o)
_ :
  Membership.mem (γ := Finset (Perm (n × o))) univ σ →
    σ ∉ preserving_snd →
      HMul.hMul (α := R) (↑(↑(((sign : Perm (n × o) →* ℤˣ) : (a : Perm (n × o)) → ℤˣ) σ) : ℤ) : R)
          (∏ i : n × o, blockDiagonal M ((σ : (a : n × o) → n × o) i) i) =
        0
⊢ Membership.mem (γ := Finset (Perm (n × o))) univ σ →
    σ ∉ preserving_snd →
      HMul.hMul (α := R) (↑(↑(((sign : Perm (n × o) →* ℤˣ) : (a : Perm (n × o)) → ℤˣ) σ) : ℤ) : R)
          (∏ i : n × o, blockDiagonal M ((σ : (a : n × o) → n × o) i) i) =
        0

Tactic:
_
-- Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic
Goal:
n : Type u_2
inst : DecidableEq n
inst_1 : Fintype n
R : Type v
inst_2 : CommRing R
o : Type u_3
inst_3 : Fintype o
inst_4 : DecidableEq o
M : o → Matrix n n R
preserving_snd : Finset (Perm (n × o)) := {σ : Perm (n × o) | ∀ (x : n × o), ((σ : (a : n × o) → n × o) x).2 = x.2}
mem_preserving_snd : ∀ {σ : Perm (n × o)}, σ ∈ preserving_snd ↔ ∀ (x : n × o), ((σ : (a : n × o) → n × o) x).2 = x.2
σ : Perm (n × o)
h : Membership.mem (γ := Finset (Perm (n × o))) univ σ
hσ : σ ∉ preserving_snd
⊢ ¬∀ (x : n × o), ((σ : (a : n × o) → n × o) x).2 = x.2

Tactic:
rw [mem_preserving_snd] at hσ
-- Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic
Goal:
n : Type u_2
inst : DecidableEq n
inst_1 : Fintype n
R : Type v
inst_2 : CommRing R
o : Type u_3
inst_3 : Fintype o
inst_4 : DecidableEq o
M : o → Matrix n n R
preserving_snd : Finset (Perm (n × o)) := {σ : Perm (n × o) | ∀ (x : n × o), ((σ : (a : n × o) → n × o) x).2 = x.2}
mem_preserving_snd : ∀ {σ : Perm (n × o)}, σ ∈ preserving_snd ↔ ∀ (x : n × o), ((σ : (a : n × o) → n × o) x).2 = x.2
σ : Perm (n × o)
h : Membership.mem (γ := Finset (Perm (n × o))) univ σ
hσ : ¬∀ (x : n × o), ((σ : (a : n × o) → n × o) x).2 = x.2
obtain :
  ∀ (k : n) (x : o) (hkx : ¬((σ : (a : n × o) → n × o) (k, x)).2 = (k, x).2),
    HMul.hMul (α := R) (↑(↑(((sign : Perm (n × o) →* ℤˣ) : (a : Perm (n × o)) → ℤˣ) σ) : ℤ) : R)
        (∏ i : n × o, blockDiagonal M ((σ : (a : n × o) → n × o) i) i) =
      0
⊢ HMul.hMul (α := R) (↑(↑(((sign : Perm (n × o) →* ℤˣ) : (a : Perm (n × o)) → ℤˣ) σ) : ℤ) : R)
      (∏ i : n × o, blockDiagonal M ((σ : (a : n × o) → n × o) i) i) =
    0

Tactic:
obtain ⟨⟨k, x⟩, hkx⟩ := not_forall.mp hσ

Premises used: Iff.mp, Classical.not_forall
-- Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic
Goal:
n : Type u_2
inst : DecidableEq n
inst_1 : Fintype n
R : Type v
inst_2 : CommRing R
o : Type u_3
inst_3 : Fintype o
inst_4 : DecidableEq o
M : o → Matrix n n R
preserving_snd : Finset (Perm (n × o)) := {σ : Perm (n × o) | ∀ (x : n × o), ((σ : (a : n × o) → n × o) x).2 = x.2}
mem_preserving_snd : ∀ {σ : Perm (n × o)}, σ ∈ preserving_snd ↔ ∀ (x : n × o), ((σ : (a : n × o) → n × o) x).2 = x.2
σ : Perm (n × o)
h : Membership.mem (γ := Finset (Perm (n × o))) univ σ
hσ : ¬∀ (x : n × o), ((σ : (a : n × o) → n × o) x).2 = x.2
k : n
x : o
hkx : ¬((σ : (a : n × o) → n × o) (k, x)).2 = (k, x).2
rw : blockDiagonal M ((σ : (a : n × o) → n × o) (k, x)) (k, x) = 0
⊢ HMul.hMul (α := R) (↑(↑(((sign : Perm (n × o) →* ℤˣ) : (a : Perm (n × o)) → ℤˣ) σ) : ℤ) : R)
      (∏ i : n × o, blockDiagonal M ((σ : (a : n × o) → n × o) i) i) =
    0

Tactic:
rw [Finset.prod_eq_zero (Finset.mem_univ (k, x)), mul_zero]

Premises used: Finset.mem_univ, Prod.mk, MulZeroClass.mul_zero, Finset.prod_eq_zero
-- Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic
Goal:
n : Type u_2
inst : DecidableEq n
inst_1 : Fintype n
R : Type v
inst_2 : CommRing R
o : Type u_3
inst_3 : Fintype o
inst_4 : DecidableEq o
M : o → Matrix n n R
preserving_snd : Finset (Perm (n × o)) := {σ : Perm (n × o) | ∀ (x : n × o), ((σ : (a : n × o) → n × o) x).2 = x.2}
mem_preserving_snd : ∀ {σ : Perm (n × o)}, σ ∈ preserving_snd ↔ ∀ (x : n × o), ((σ : (a : n × o) → n × o) x).2 = x.2
σ : Perm (n × o)
h_1 : Membership.mem (γ := Finset (Perm (n × o))) univ σ
hσ : ¬∀ (x : n × o), ((σ : (a : n × o) → n × o) x).2 = x.2
k : n
x : o
hkx : ¬((σ : (a : n × o) → n × o) (k, x)).2 = (k, x).2
h : ((σ : (a : n × o) → n × o) (k, x)).2 ≠ x
⊢ blockDiagonal M ((σ : (a : n × o) → n × o) (k, x)) (k, x) = 0

Tactic:
rw [blockDiagonal_apply_ne]

Premises used: Matrix.blockDiagonal_apply_ne
-- Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic
Goal:
n : Type u_2
inst : DecidableEq n
inst_1 : Fintype n
R : Type v
inst_2 : CommRing R
o : Type u_3
inst_3 : Fintype o
inst_4 : DecidableEq o
M : o → Matrix n n R
preserving_snd : Finset (Perm (n × o)) := {σ : Perm (n × o) | ∀ (x : n × o), ((σ : (a : n × o) → n × o) x).2 = x.2}
mem_preserving_snd : ∀ {σ : Perm (n × o)}, σ ∈ preserving_snd ↔ ∀ (x : n × o), ((σ : (a : n × o) → n × o) x).2 = x.2
σ : Perm (n × o)
h : Membership.mem (γ := Finset (Perm (n × o))) univ σ
hσ : ¬∀ (x : n × o), ((σ : (a : n × o) → n × o) x).2 = x.2
k : n
x : o
hkx : ¬((σ : (a : n × o) → n × o) (k, x)).2 = (k, x).2
⊢ ((σ : (a : n × o) → n × o) (k, x)).2 ≠ x

Tactic:
hkx
-- Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic
Goal:
n : Type u_2
inst : DecidableEq n
inst_1 : Fintype n
R : Type v
inst_2 : CommRing R
o : Type u_3
inst_3 : Fintype o
inst_4 : DecidableEq o
M : o → Matrix n n R
preserving_snd : Finset (Perm (n × o)) := {σ : Perm (n × o) | ∀ (x : n × o), ((σ : (a : n × o) → n × o) x).2 = x.2}
mem_preserving_snd : ∀ {σ : Perm (n × o)}, σ ∈ preserving_snd ↔ ∀ (x : n × o), ((σ : (a : n × o) → n × o) x).2 = x.2
σ : Perm (n × o)
h : Membership.mem (γ := Finset (Perm (n × o))) univ σ
hσ : ¬∀ (x : n × o), ((σ : (a : n × o) → n × o) x).2 = x.2
k : n
x : o
hkx : ¬((σ : (a : n × o) → n × o) (k, x)).2 = (k, x).2
⊢ ((σ : (a : n × o) → n × o) (k, x)).2 ≠ x

Tactic:
exact hkx
-- 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
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

Tactic:
simp_rw [det_apply']

Premises used: Matrix.det_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
B : Matrix m n R
D : Matrix n n R
⊢ Eq.{v + 1} (α := R)
    (∑ x : Perm (m ⊕ n),
      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))
    (∑ 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:
Eq.symm <|
        sum_subset (M := R) (subset_univ ((sumCongrHom m n).range : Set (Perm (m ⊕ n))).toFinset) ?_

Premises used: MonoidHom.range, Equiv.Perm.sumCongrHom, Set.toFinset, SetLike.coe, Finset.sum_subset, Eq.symm, Finset.subset_univ