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
d : n → R
σ : Perm n
h2 : σ ≠ 1
x : n
h3 : ¬Eq (α := n) ((σ : (a : n) → n) x : n) ((1 : (a : n) → n) x : n)
h : diagonal d ((σ : (a : n) → n) x) x = 0
⊢ Eq.{v + 1} (α := R) (∏ i : n, diagonal d ((σ : (a : n) → n) i) i) 0

Tactic:
apply Finset.prod_eq_zero (mem_univ x)

Premises used: Finset.mem_univ, 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
d : n → R
σ : Perm n
h2 : σ ≠ 1
x : n
h3 : ¬Eq (α := n) ((σ : (a : n) → n) x : n) ((1 : (a : n) → n) x : n)
⊢ diagonal d ((σ : (a : n) → n) x) x = 0

Tactic:
if_neg h3

Premises used: if_neg, Matrix.diagonal, ite
-- 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
d : n → R
σ : Perm n
h2 : σ ≠ 1
x : n
h3 : ¬Eq (α := n) ((σ : (a : n) → n) x : n) ((1 : (a : n) → n) x : n)
⊢ diagonal d ((σ : (a : n) → n) x) x = 0

Tactic:
exact if_neg h3

Premises used: if_neg
-- 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
d : n → R
⊢ 1 ∉ univ →
    HMul.hMul (α := R) (↑(↑(((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) 1) : ℤ) : R)
        (∏ i : n, diagonal d ((1 : (a : n) → n) i) i) =
      0

Tactic:
simp
-- 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
d : n → R
⊢ HMul.hMul (α := R) (↑(↑(((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) 1) : ℤ) : R)
      (∏ i : n, diagonal d ((1 : (a : n) → n) i) i) =
    ∏ i : n, d i

Tactic:
simp
-- 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
h : Nonempty n
⊢ Eq.{v + 1} (α := R) (det.{v, u_2} (n := n) 0) 0

Tactic:
(detRowAlternating : (n → R) [⋀^n]→ₗ[R] R).map_zero

Premises used: Matrix.detRowAlternating, AlternatingMap.map_zero, Matrix.det
-- 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
⊢ Eq.{v + 1} (α := R) (det.{v, u_2} (n := n) (diagonal fun (x : n) ↦ 1)) 1

Tactic:
simp [-diagonal_one]

Premises used: Matrix.diagonal_one
-- 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
inst_3 : IsEmpty n
A : Matrix n n R
⊢ A.det = 1

Tactic:
simp [det_apply]

Premises used: Matrix.det_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
inst_3 : IsEmpty n
h : ∀ (x : Matrix n n R), x.det = const (Matrix n n R) 1 x
⊢ Eq (α := (M : Matrix n n R) → R) det (const (Matrix n n R) 1)

Tactic:
ext
-- 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
inst_3 : IsEmpty n
x : Matrix n n R
⊢ x.det = const (Matrix n n R) 1 x

Tactic:
det_isEmpty

Premises used: Matrix.det_isEmpty
-- 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
inst_3 : IsEmpty n
x : Matrix n n R
⊢ x.det = const (Matrix n n R) 1 x

Tactic:
exact det_isEmpty

Premises used: Matrix.det_isEmpty
-- 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
A : Matrix n n R
h : Fintype.card n = 0
⊢ A.det = 1

Tactic:
haveI : IsEmpty n := Fintype.card_eq_zero_iff.mp h
  det_isEmpty

Premises used: Matrix.det_isEmpty
-- Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic
Goal:
R : Type v
inst : CommRing R
n : Type u_3
inst_1 : Unique n
inst_2 : DecidableEq n
inst_3 : Fintype n
A : Matrix n n R
⊢ A.det = A default default

Tactic:
simp [det_apply, univ_unique]

Premises used: Matrix.det_apply, Finset.univ_unique
-- 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
inst_3 : Subsingleton n
A : Matrix n n R
k : n
have : ∀ (this : Unique n), A.det = A k k
⊢ A.det = A k k

Tactic:
have := uniqueOfSubsingleton k
-- 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
inst_3 : Subsingleton n
A : Matrix n n R
k : n
this : Unique n
⊢ A.det = A default default

Tactic:
det_unique A

Premises used: Matrix.det_unique
-- 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
inst_3 : Subsingleton n
A : Matrix n n R
k : n
this : Unique n
⊢ A.det = A k k

Tactic:
convert! det_unique A

Premises used: Matrix.det_unique
-- 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
A : Matrix n n R
h : Fintype.card n = 1
k : n
⊢ A.det = A k k

Tactic:
haveI : Subsingleton n := Fintype.card_le_one_iff_subsingleton.mp h.le
  det_eq_elem_of_subsingleton _ _

Premises used: Matrix.det_eq_elem_of_subsingleton
-- 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
M N : Matrix n n R
p : n → n
H : ¬Bijective p
⊢ ¬∀ ⦃a₁ a₂ : n⦄, p a₁ = p a₂ → a₁ = a₂

Tactic:
rw [← Finite.injective_iff_bijective, Injective] at H

Premises used: Finite.injective_iff_bijective, Function.Injective
-- 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
M N : Matrix n n R
p : n → n
H : ¬∀ ⦃a₁ a₂ : n⦄, p a₁ = p a₂ → a₁ = a₂
⊢ ∃ (a₁ : n) (a₂ : n), p a₁ = p a₂ ∧ a₁ ≠ a₂

Tactic:
push Not at H

Premises used: Not
-- 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
M N : Matrix n n R
p : n → n
H : ∃ (a₁ : n) (a₂ : n), p a₁ = p a₂ ∧ a₁ ≠ a₂
⊢ ∃ (i : n) (j : n), p i = p j ∧ i ≠ j

Tactic:
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
M N : Matrix n n R
p : n → n
H : ∃ (a₁ : n) (a₂ : n), p a₁ = p a₂ ∧ a₁ ≠ a₂
⊢ ∃ (i : n) (j : n), p i = p j ∧ i ≠ j

Tactic:
exact 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
M N : Matrix n n R
p : n → n
H : ¬Bijective p
obtain :
  ∀ (i j : n) (hpij : p i = p j) (hij : i ≠ j),
    Eq.{v + 1} (α := R)
      (∑ σ : Perm n,
        HMul.hMul (α := R) (↑(↑(((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) σ) : ℤ) : R)
          (∏ x : n, M ((σ : (a : n) → n) x) (p x) * N (p x) x))
      0
⊢ Eq.{v + 1} (α := R)
    (∑ σ : Perm n,
      HMul.hMul (α := R) (↑(↑(((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) σ) : ℤ) : R)
        (∏ x : n, M ((σ : (a : n) → n) x) (p x) * N (p x) x))
    0

Tactic:
obtain ⟨i, j, hpij, hij⟩ : ∃ i j, p i = p j ∧ i ≠ j := by
    rw [← Finite.injective_iff_bijective, Injective] at H
    push Not at H
    exact 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
M N : Matrix n n R
p : n → n
H : ¬Bijective p
i j : n
hpij : p i = p j
hij : i ≠ j
σ : Perm n
h : Membership.mem (γ := Finset (Perm n)) univ σ
⊢ ∀ (x : n),
    M ((σ : (a : n) → n) x) (p x) =
      M ((σ * Equiv.swap i j : (a : n) → n) ((Equiv.swap i j : (a : n) → n) x : n))
        (p ((Equiv.swap i j : (a : n) → n) x))

Tactic:
simp [apply_swap_eq_self hpij]

Premises used: Equiv.apply_swap_eq_self
-- 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
M N : Matrix n n R
p : n → n
H : ¬Bijective p
i j : n
hpij : p i = p j
hij : i ≠ j
σ : Perm n
h : Membership.mem (γ := Finset (Perm n)) univ σ
⊢ Eq.{v + 1} (α := R) (∏ x : n, M ((σ : (a : n) → n) x) (p x)) (∏ x : n, M ((σ * Equiv.swap i j : (a : n) → n) x) (p x))

Tactic:
have : (∏ x, M (σ x) (p x)) = ∏ x, M ((σ * Equiv.swap i j) x) (p x) :=
          Fintype.prod_equiv (swap i j) _ _ (by simp [apply_swap_eq_self hpij])
-- 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
M N : Matrix n n R
p : n → n
H : ¬Bijective p
i j : n
hpij : p i = p j
hij : i ≠ j
σ : Perm n
h : Membership.mem (γ := Finset (Perm n)) univ σ
this :
  Eq.{v + 1} (α := R) (∏ x : n, M ((σ : (a : n) → n) x) (p x)) (∏ x : n, M ((σ * Equiv.swap i j : (a : n) → n) x) (p x))
⊢ HMul.hMul (α := R) (↑(↑(((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) σ) : ℤ) : R)
        (∏ x : n, M ((σ : (a : n) → n) x) (p x) * N (p x) x) +
      HMul.hMul (α := R)
        (↑(↑(((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ)
                  ((fun (σ : Perm n) (x : Membership.mem (γ := Finset (Perm n)) univ σ) ↦ σ * Equiv.swap i j) σ h)) :
              ℤ) :
          R)
        (∏ x : n,
          M
              (((fun (σ : Perm n) (x : Membership.mem (γ := Finset (Perm n)) univ σ) ↦ σ * Equiv.swap i j) σ h :
                  (a : n) → n)
                x)
              (p x) *
            N (p x) x) =
    0

Tactic:
simp [this, sign_swap hij, -sign_swap', prod_mul_distrib]

Premises used: Finset.prod_mul_distrib, Equiv.Perm.sign_swap', Equiv.Perm.sign_swap
-- 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
M N : Matrix n n R
p : n → n
H : ¬Bijective p
i j : n
hpij : p i = p j
hij : i ≠ j
⊢ Eq.{v + 1} (α := R)
    (∑ σ : Perm n,
      HMul.hMul (α := R) (↑(↑(((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) σ) : ℤ) : R)
        (∏ x : n, M ((σ : (a : n) → n) x) (p x) * N (p x) x))
    0

Tactic:
exact
    sum_involution (fun σ _ => σ * Equiv.swap i j)
      (fun σ _ => by
        have : (∏ x, M (σ x) (p x)) = ∏ x, M ((σ * Equiv.swap i j) x) (p x) :=
          Fintype.prod_equiv (swap i j) _ _ (by simp [apply_swap_eq_self hpij])
        simp [this, sign_swap hij, -sign_swap', prod_mul_distrib])
      (fun σ _ _ => (not_congr mul_swap_eq_iff).mpr hij) (fun _ _ => mem_univ _) fun σ _ =>
      mul_swap_involutive i j σ

Premises used: Iff.mpr, Finset.mem_univ, HMul.hMul, Equiv.swap, Equiv.mul_swap_involutive, Equiv.mul_swap_eq_iff, Finset.sum_involution, not_congr
-- 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
M N : Matrix n n R
simp :
  Eq.{v + 1} (α := R)
    (∑ x : Perm n,
      ∑ i : (a : n) → n,
        HMul.hMul (α := R) (↑(↑(((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) x) : ℤ) : R)
          (∏ i_1 : n, M ((x : (a : n) → n) i_1) (i i_1) * N (i i_1) i_1))
    (∑ p : n → n,
      ∑ σ : Perm n,
        HMul.hMul (α := R) (↑(↑(((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) σ) : ℤ) : R)
          (∏ i : n, M ((σ : (a : n) → n) i) (p i) * N (p i) i))
⊢ (M * N).det =
    ∑ p : n → n,
      ∑ σ : Perm n,
        HMul.hMul (α := R) (↑(↑(((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) σ) : ℤ) : R)
          (∏ i : n, M ((σ : (a : n) → n) i) (p i) * N (p i) i)

Tactic:
simp only [det_apply', mul_apply, prod_univ_sum, mul_sum, Fintype.piFinset_univ]

Premises used: Finset.mul_sum, Fintype.piFinset_univ, Matrix.mul_apply, Matrix.det_apply', Finset.prod_univ_sum
-- 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
M N : Matrix n n R
rw rw₁ :
  Eq.{v + 1} (α := R)
    (∑ y : (a : n) → n,
      ∑ x : Perm n,
        HMul.hMul (α := R) (↑(↑(((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) x) : ℤ) : R)
          (∏ i : n, M ((x : (a : n) → n) i) (y i) * N (y i) i))
    (∑ p : n → n,
      ∑ σ : Perm n,
        HMul.hMul (α := R) (↑(↑(((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) σ) : ℤ) : R)
          (∏ i : n, M ((σ : (a : n) → n) i) (p i) * N (p i) i))
⊢ Eq.{v + 1} (α := R)
    (∑ x : Perm n,
      ∑ i : (a : n) → n,
        HMul.hMul (α := R) (↑(↑(((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) x) : ℤ) : R)
          (∏ i_1 : n, M ((x : (a : n) → n) i_1) (i i_1) * N (i i_1) i_1))
    (∑ p : n → n,
      ∑ σ : Perm n,
        HMul.hMul (α := R) (↑(↑(((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) σ) : ℤ) : R)
          (∏ i : n, M ((σ : (a : n) → n) i) (p i) * N (p i) i))

Tactic:
rw [Finset.sum_comm]

Premises used: Finset.sum_comm
-- 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
M N : Matrix n n R
⊢ Eq.{v + 1} (α := R)
    (∑ p : n → n,
      ∑ σ : Perm n,
        HMul.hMul (α := R) (↑(↑(((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) σ) : ℤ) : R)
          (∏ i : n, M ((σ : (a : n) → n) i) (p i) * N (p i) i))
    (∑ p : n → n with Bijective p,
      ∑ σ : Perm n,
        HMul.hMul (α := R) (↑(↑(((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) σ) : ℤ) : R)
          (∏ i : n, M ((σ : (a : n) → n) i) (p i) * N (p i) i))

Tactic:
(sum_subset (filter_subset _ _) fun f _ hbij ↦ det_mul_aux ?_).symm

Premises used: Finset.filter_subset, Finset.sum_subset, Matrix.det_mul_aux, Eq.symm
-- 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
M N : Matrix n n R
refine :
  ∀ (f : n → n), Membership.mem (γ := Finset (n → n)) univ f → ∀ (hbij : f ∉ {p : n → n | Bijective p}), ¬Bijective f
⊢ Eq.{v + 1} (α := R)
    (∑ p : n → n,
      ∑ σ : Perm n,
        HMul.hMul (α := R) (↑(↑(((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) σ) : ℤ) : R)
          (∏ i : n, M ((σ : (a : n) → n) i) (p i) * N (p i) i))
    (∑ p : n → n with Bijective p,
      ∑ σ : Perm n,
        HMul.hMul (α := R) (↑(↑(((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) σ) : ℤ) : R)
          (∏ i : n, M ((σ : (a : n) → n) i) (p i) * N (p i) i))

Tactic:
refine (sum_subset (filter_subset _ _) fun f _ hbij ↦ det_mul_aux ?_).symm

Premises used: Finset.filter_subset, Finset.sum_subset, Matrix.det_mul_aux, Eq.symm
-- 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
M N : Matrix n n R
f : n → n
h : Membership.mem (γ := Finset (n → n)) univ f
hbij : f ∉ {p : n → n | Bijective p}
⊢ ¬Bijective f

Tactic:
simpa only [mem_filter_univ] using hbij

Premises used: Finset.mem_filter_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
M N : Matrix n n R
x : n → n
h_1 : Membership.mem (γ := Finset (n → n)) {p : n → n | Bijective p} x
x_1 : n → n
h_2 : Membership.mem (γ := Finset (n → n)) {p : n → n | Bijective p} x_1
h :
  Eq.{u_2 + 1} (α := Perm n)
    ((fun (p : n → n) (h : Membership.mem (γ := Finset (n → n)) {p : n → n | Bijective p} p) ↦ ofBijective p ⋯) x h_1)
    ((fun (p : n → n) (h : Membership.mem (γ := Finset (n → n)) {p : n → n | Bijective p} p) ↦ ofBijective p ⋯) x_1 h_2)
⊢ x = x_1

Tactic:
injection 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
M N : Matrix n n R
⊢ Eq.{v + 1} (α := R)
    (∑ τ : Perm n,
      ∑ σ : Perm n,
        HMul.hMul (α := R) (↑(↑(((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) σ) : ℤ) : R)
          (∏ i : n, M ((σ : (a : n) → n) i) ((τ : (a : n) → n) i) * N ((τ : (a : n) → n) i) i))
    (∑ σ : Perm n,
      ∑ τ : Perm n,
        HMul.hMul (α := R) (∏ i : n, N ((σ : (a : n) → n) i) i)
            (↑(↑(((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) τ) : ℤ) : R) *
          ∏ j : n, M ((τ : (a : n) → n) j) ((σ : (a : n) → n) j))

Tactic:
simp only [mul_comm, mul_left_comm, prod_mul_distrib, mul_assoc]

Premises used: Finset.prod_mul_distrib, mul_assoc, mul_left_comm, mul_comm
-- 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
M N : Matrix n n R
σ : Perm n
h : Membership.mem (γ := Finset (Perm n)) univ σ
τ : Perm n
rw :
  Eq.{v + 1} (α := R)
    (∏ i : n, M ((τ : (a : n) → n) ((σ⁻¹ : (a : n) → n) i : n)) ((σ : (a : n) → n) ((σ⁻¹ : (a : n) → n) i : n)))
    (∏ j : n, M ((τ * σ⁻¹ : (a : n) → n) j) j)
⊢ Eq.{v + 1} (α := R) (∏ j : n, M ((τ : (a : n) → n) j) ((σ : (a : n) → n) j))
    (∏ j : n, M ((τ * σ⁻¹ : (a : n) → n) j) j)

Tactic:
rw [← (σ⁻¹ : _ ≃ _).prod_comp]

Premises used: Equiv.prod_comp, Inv.inv
-- 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
M N : Matrix n n R
σ : Perm n
h : Membership.mem (γ := Finset (Perm n)) univ σ
τ : Perm n
⊢ Eq.{v + 1} (α := R)
    (∏ i : n, M ((τ : (a : n) → n) ((σ⁻¹ : (a : n) → n) i : n)) ((σ : (a : n) → n) ((σ⁻¹ : (a : n) → n) i : n)))
    (∏ j : n, M ((τ * σ⁻¹ : (a : n) → n) j) j)

Tactic:
simp
-- 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
M N : Matrix n n R
σ : Perm n
h : Membership.mem (γ := Finset (Perm n)) univ σ
τ : Perm n
⊢ Eq.{v + 1} (α := R) (∏ j : n, M ((τ : (a : n) → n) j) ((σ : (a : n) → n) j))
    (∏ j : n, M ((τ * σ⁻¹ : (a : n) → n) j) j)

Tactic:
have : (∏ j, M (τ j) (σ j)) = ∏ j, M ((τ * σ⁻¹) j) j := by
            rw [← (σ⁻¹ : _ ≃ _).prod_comp]
            simp
-- 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
M N : Matrix n n R
σ : Perm n
h : Membership.mem (γ := Finset (Perm n)) univ σ
τ : Perm n
this :
  Eq.{v + 1} (α := R) (∏ j : n, M ((τ : (a : n) → n) j) ((σ : (a : n) → n) j))
    (∏ j : n, M ((τ * σ⁻¹ : (a : n) → n) j) j)
rw :
  HMul.hMul (α := R) (↑(↑(((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) (τ * σ⁻¹)) : ℤ) : R)
      (↑(↑(((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) σ) : ℤ) : R) =
    (↑(↑(HMul.hMul (α := ℤˣ) (β := ℤˣ) (((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) (τ * σ⁻¹) : ℤˣ)
              (((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) σ : ℤˣ)) :
          ℤ) :
      R)
⊢ HMul.hMul (α := R) (↑(↑(((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) σ) : ℤ) : R)
      (↑(↑(((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) (τ * σ⁻¹)) : ℤ) : R) =
    (↑(↑(((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) (τ * σ⁻¹ * σ)) : ℤ) : R)

Tactic:
rw [mul_comm, sign_mul (τ * σ⁻¹)]

Premises used: HMul.hMul, Equiv.Perm.sign_mul, Inv.inv, mul_comm
-- 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
M N : Matrix n n R
σ : Perm n
h : Membership.mem (γ := Finset (Perm n)) univ σ
τ : Perm n
this :
  Eq.{v + 1} (α := R) (∏ j : n, M ((τ : (a : n) → n) j) ((σ : (a : n) → n) j))
    (∏ j : n, M ((τ * σ⁻¹ : (a : n) → n) j) j)
⊢ HMul.hMul (α := R) (↑(↑(((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) (τ * σ⁻¹)) : ℤ) : R)
      (↑(↑(((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) σ) : ℤ) : R) =
    (↑(↑(HMul.hMul (α := ℤˣ) (β := ℤˣ) (((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) (τ * σ⁻¹) : ℤˣ)
              (((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) σ : ℤˣ)) :
          ℤ) :
      R)

Tactic:
simp only [Int.cast_mul, Units.val_mul]

Premises used: Int.cast_mul, Units.val_mul
-- 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
M N : Matrix n n R
σ : Perm n
h : Membership.mem (γ := Finset (Perm n)) univ σ
τ : Perm n
this :
  Eq.{v + 1} (α := R) (∏ j : n, M ((τ : (a : n) → n) j) ((σ : (a : n) → n) j))
    (∏ j : n, M ((τ * σ⁻¹ : (a : n) → n) j) j)
⊢ Eq.{v + 1} (α := R) (↑(↑(((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) (τ * σ⁻¹ * σ)) : ℤ) : R)
    (↑(↑(((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) τ) : ℤ) : R)

Tactic:
simp only [inv_mul_cancel_right]

Premises used: inv_mul_cancel_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
M N : Matrix n n R
σ : Perm n
h : Membership.mem (γ := Finset (Perm n)) univ σ
τ : Perm n
this :
  Eq.{v + 1} (α := R) (∏ j : n, M ((τ : (a : n) → n) j) ((σ : (a : n) → n) j))
    (∏ j : n, M ((τ * σ⁻¹ : (a : n) → n) j) j)
⊢ HMul.hMul (α := R) (↑(↑(((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) σ) : ℤ) : R)
      (↑(↑(((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) (τ * σ⁻¹)) : ℤ) : R) =
    (↑(↑(((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) τ) : ℤ) : R)

Tactic:
have h : ε σ * ε (τ * σ⁻¹) = ε τ :=
            calc
              ε σ * ε (τ * σ⁻¹) = ε (τ * σ⁻¹ * σ) := by
                rw [mul_comm, sign_mul (τ * σ⁻¹)]
                simp only [Int.cast_mul, Units.val_mul]
              _ = ε τ := by simp only [inv_mul_cancel_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
M N : Matrix n n R
σ : Perm n
h_1 : Membership.mem (γ := Finset (Perm n)) univ σ
τ : Perm n
this :
  Eq.{v + 1} (α := R) (∏ j : n, M ((τ : (a : n) → n) j) ((σ : (a : n) → n) j))
    (∏ j : n, M ((τ * σ⁻¹ : (a : n) → n) j) j)
h :
  HMul.hMul (α := R) (↑(↑(((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) σ) : ℤ) : R)
      (↑(↑(((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) (τ * σ⁻¹)) : ℤ) : R) =
    (↑(↑(((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) τ) : ℤ) : R)
simp_rw :
  HMul.hMul (α := R) (∏ i : n, N ((σ : (a : n) → n) i) i)
        (↑(↑(((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) τ) : ℤ) : R) *
      ∏ j : n, M ((τ : (a : n) → n) j) ((σ : (a : n) → n) j) =
    HMul.hMul (α := R) (∏ i : n, N ((σ : (a : n) → n) i) i)
        (↑(↑(((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) τ) : ℤ) : R) *
      ∏ x : n, M ((τ * σ⁻¹ : (a : n) → n) x) x
⊢ HMul.hMul (α := R) (∏ i : n, N ((σ : (a : n) → n) i) i)
        (↑(↑(((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) τ) : ℤ) : R) *
      ∏ j : n, M ((τ : (a : n) → n) j) ((σ : (a : n) → n) j) =
    (∏ i : n, N ((σ : (a : n) → n) i) i) *
        HMul.hMul (α := R) (↑(↑(((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) σ) : ℤ) : R)
          (↑(↑(((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) ((Equiv.mulRight σ⁻¹ : (a : Perm n) → Perm n) τ)) : ℤ) : R) *
      ∏ i : n, M ((((Equiv.mulRight σ⁻¹ : (a : Perm n) → Perm n) τ : Perm n) : (a : n) → n) i) i

Tactic:
simp_rw [Equiv.coe_mulRight, h]

Premises used: Equiv.coe_mulRight
-- 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
M N : Matrix n n R
σ : Perm n
h_1 : Membership.mem (γ := Finset (Perm n)) univ σ
τ : Perm n
this :
  Eq.{v + 1} (α := R) (∏ j : n, M ((τ : (a : n) → n) j) ((σ : (a : n) → n) j))
    (∏ j : n, M ((τ * σ⁻¹ : (a : n) → n) j) j)
h :
  HMul.hMul (α := R) (↑(↑(((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) σ) : ℤ) : R)
      (↑(↑(((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) (τ * σ⁻¹)) : ℤ) : R) =
    (↑(↑(((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) τ) : ℤ) : R)
⊢ HMul.hMul (α := R) (∏ i : n, N ((σ : (a : n) → n) i) i)
        (↑(↑(((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) τ) : ℤ) : R) *
      ∏ j : n, M ((τ : (a : n) → n) j) ((σ : (a : n) → n) j) =
    HMul.hMul (α := R) (∏ i : n, N ((σ : (a : n) → n) i) i)
        (↑(↑(((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) τ) : ℤ) : R) *
      ∏ x : n, M ((τ * σ⁻¹ : (a : n) → n) x) x

Tactic:
simp only [this]
-- 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
⊢ Eq (α := (a : Matrix n n R) → R) (⇑detMonoidHom : (a : Matrix n n R) → R) det

Tactic:
rfl

Premises used: Matrix.det, rfl