-- Mathlib/LinearAlgebra/Matrix/Determinant/Basic.lean
theorem det_mul_aux {M N : Matrix n n R} {p : n → n} (H : ¬Bijective p) :
    (∑ σ : Perm n, ε σ * ∏ x, M (σ x) (p x) * N (p x) x) = 0

Proof state:
n : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type v
inst✝ : 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
x✝ : σ ∈ univ
⊢ ∀ (x : n), M (σ x) (p x) = M ((σ * Equiv.swap i j) ((Equiv.swap i j) x)) (p ((Equiv.swap i j) x))

Tactic:
simp [apply_swap_eq_self hpij]

Result:
no goals

Proof state:
n : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type v
inst✝ : CommRing R
M N : Matrix n n R
p : n → n
H : ∃ a₁ a₂, p a₁ = p a₂ ∧ a₁ ≠ a₂
⊢ ∃ i j, p i = p j ∧ i ≠ j

Tactic:
exact H

Result:
no goals

Proof state:
n : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type v
inst✝ : 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
x✝ : σ ∈ univ
this : ∏ x : n, M (σ x) (p x) = ∏ x : n, M ((σ * Equiv.swap i j) x) (p x)
⊢ ↑↑(sign σ) * ∏ x : n, M (σ x) (p x) * N (p x) x +
      ↑↑(sign ((fun σ x => σ * Equiv.swap i j) σ x✝)) *
        ∏ x : n, M (((fun σ x => σ * Equiv.swap i j) σ x✝) x) (p x) * N (p x) x =
    0

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

Result:
no goals

Proof state:
n : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type v
inst✝ : CommRing R
M N : Matrix n n R
p : n → n
H : ¬Bijective p
⊢ ∑ σ : Perm n, ↑↑(sign σ) * ∏ x : n, M (σ 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_neg at H
  exact H

Result:
case intro.intro.intro
n : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type v
inst✝ : 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, ↑↑(sign σ) * ∏ x : n, M (σ x) (p x) * N (p x) x = 0

Proof state:
case intro.intro.intro
n : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type v
inst✝ : 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, ↑↑(sign σ) * ∏ x : n, M (σ 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 σ

Result:
no goals

Proof state:
n : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type v
inst✝ : CommRing R
M N : Matrix n n R
p : n → n
H : ¬∀ ⦃a₁ a₂ : n⦄, p a₁ = p a₂ → a₁ = a₂
⊢ ∃ i j, p i = p j ∧ i ≠ j

Tactic:
push_neg at H

Result:
n : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type v
inst✝ : CommRing R
M N : Matrix n n R
p : n → n
H : ∃ a₁ a₂, p a₁ = p a₂ ∧ a₁ ≠ a₂
⊢ ∃ i j, p i = p j ∧ i ≠ j

Proof state:
n : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type v
inst✝ : 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
x✝ : σ ∈ univ
⊢ ↑↑(sign σ) * ∏ x : n, M (σ x) (p x) * N (p x) x +
      ↑↑(sign ((fun σ x => σ * Equiv.swap i j) σ x✝)) *
        ∏ x : n, M (((fun σ x => σ * Equiv.swap i j) σ x✝) x) (p x) * N (p x) x =
    0

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])

Result:
n : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type v
inst✝ : 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
x✝ : σ ∈ univ
this : ∏ x : n, M (σ x) (p x) = ∏ x : n, M ((σ * Equiv.swap i j) x) (p x)
⊢ ↑↑(sign σ) * ∏ x : n, M (σ x) (p x) * N (p x) x +
      ↑↑(sign ((fun σ x => σ * Equiv.swap i j) σ x✝)) *
        ∏ x : n, M (((fun σ x => σ * Equiv.swap i j) σ x✝) x) (p x) * N (p x) x =
    0

Proof state:
n : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type v
inst✝ : CommRing R
M N : Matrix n n R
p : n → n
H : ¬Bijective p
⊢ ∃ i j, p i = p j ∧ i ≠ j

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

Result:
n : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type v
inst✝ : CommRing R
M N : Matrix n n R
p : n → n
H : ¬∀ ⦃a₁ a₂ : n⦄, p a₁ = p a₂ → a₁ = a₂
⊢ ∃ i j, p i = p j ∧ i ≠ j