-- Mathlib/LinearAlgebra/Matrix/Determinant/Basic.lean
theorem det_submatrix_equiv_self (e : n ≃ m) (A : Matrix m m R) :
    det (A.submatrix e e) = det A

Proof state:
case h
m : Type u_1
n : Type u_2
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
R : Type v
inst✝ : CommRing R
e : n ≃ m
A : Matrix m m R
σ : Perm n
⊢ ↑↑(sign σ) * ∏ i : n, A.submatrix (⇑e) (⇑e) (σ i) i = ↑↑(sign (e.permCongr σ)) * ∏ i : m, A ((e.permCongr σ) i) i

Tactic:
rw [Equiv.Perm.sign_permCongr e σ]

Result:
case h
m : Type u_1
n : Type u_2
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
R : Type v
inst✝ : CommRing R
e : n ≃ m
A : Matrix m m R
σ : Perm n
⊢ ↑↑(sign σ) * ∏ i : n, A.submatrix (⇑e) (⇑e) (σ i) i = ↑↑(sign σ) * ∏ i : m, A ((e.permCongr σ) i) i

Proof state:
case h.e_a.h
m : Type u_1
n : Type u_2
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
R : Type v
inst✝ : CommRing R
e : n ≃ m
A : Matrix m m R
σ : Perm n
i : n
⊢ A.submatrix (⇑e) (⇑e) (σ i) i = A ((e.permCongr σ) (e i)) (e i)

Tactic:
rw [Equiv.permCongr_apply, Equiv.symm_apply_apply, submatrix_apply]

Result:
no goals

Proof state:
m : Type u_1
n : Type u_2
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
R : Type v
inst✝ : CommRing R
e : n ≃ m
A : Matrix m m R
⊢ (A.submatrix ⇑e ⇑e).det = A.det

Tactic:
rw [det_apply', det_apply']

Result:
m : Type u_1
n : Type u_2
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
R : Type v
inst✝ : CommRing R
e : n ≃ m
A : Matrix m m R
⊢ ∑ σ : Perm n, ↑↑(sign σ) * ∏ i : n, A.submatrix (⇑e) (⇑e) (σ i) i = ∑ σ : Perm m, ↑↑(sign σ) * ∏ i : m, A (σ i) i

Proof state:
case h.e_a
m : Type u_1
n : Type u_2
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
R : Type v
inst✝ : CommRing R
e : n ≃ m
A : Matrix m m R
σ : Perm n
⊢ ∏ i : n, A.submatrix (⇑e) (⇑e) (σ i) i = ∏ i : m, A ((e.permCongr σ) i) i

Tactic:
apply Fintype.prod_equiv e

Result:
case h.e_a.h
m : Type u_1
n : Type u_2
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
R : Type v
inst✝ : CommRing R
e : n ≃ m
A : Matrix m m R
σ : Perm n
⊢ ∀ (x : n), A.submatrix (⇑e) (⇑e) (σ x) x = A ((e.permCongr σ) (e x)) (e x)

Proof state:
m : Type u_1
n : Type u_2
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
R : Type v
inst✝ : CommRing R
e : n ≃ m
A : Matrix m m R
⊢ ∑ σ : Perm n, ↑↑(sign σ) * ∏ i : n, A.submatrix (⇑e) (⇑e) (σ i) i = ∑ σ : Perm m, ↑↑(sign σ) * ∏ i : m, A (σ i) i

Tactic:
apply Fintype.sum_equiv (Equiv.permCongr e)

Result:
case h
m : Type u_1
n : Type u_2
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
R : Type v
inst✝ : CommRing R
e : n ≃ m
A : Matrix m m R
⊢ ∀ (x : Perm n),
    ↑↑(sign x) * ∏ i : n, A.submatrix (⇑e) (⇑e) (x i) i = ↑↑(sign (e.permCongr x)) * ∏ i : m, A ((e.permCongr x) i) i

Proof state:
case h
m : Type u_1
n : Type u_2
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
R : Type v
inst✝ : CommRing R
e : n ≃ m
A : Matrix m m R
σ : Perm n
⊢ ↑↑(sign σ) * ∏ i : n, A.submatrix (⇑e) (⇑e) (σ i) i = ↑↑(sign σ) * ∏ i : m, A ((e.permCongr σ) i) i

Tactic:
congr 1

Result:
case h.e_a
m : Type u_1
n : Type u_2
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
R : Type v
inst✝ : CommRing R
e : n ≃ m
A : Matrix m m R
σ : Perm n
⊢ ∏ i : n, A.submatrix (⇑e) (⇑e) (σ i) i = ∏ i : m, A ((e.permCongr σ) i) i

Proof state:
case h
m : Type u_1
n : Type u_2
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
R : Type v
inst✝ : CommRing R
e : n ≃ m
A : Matrix m m R
⊢ ∀ (x : Perm n),
    ↑↑(sign x) * ∏ i : n, A.submatrix (⇑e) (⇑e) (x i) i = ↑↑(sign (e.permCongr x)) * ∏ i : m, A ((e.permCongr x) i) i

Tactic:
intro σ

Result:
case h
m : Type u_1
n : Type u_2
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
R : Type v
inst✝ : CommRing R
e : n ≃ m
A : Matrix m m R
σ : Perm n
⊢ ↑↑(sign σ) * ∏ i : n, A.submatrix (⇑e) (⇑e) (σ i) i = ↑↑(sign (e.permCongr σ)) * ∏ i : m, A ((e.permCongr σ) i) i

Proof state:
case h.e_a.h
m : Type u_1
n : Type u_2
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
R : Type v
inst✝ : CommRing R
e : n ≃ m
A : Matrix m m R
σ : Perm n
⊢ ∀ (x : n), A.submatrix (⇑e) (⇑e) (σ x) x = A ((e.permCongr σ) (e x)) (e x)

Tactic:
intro i

Result:
case h.e_a.h
m : Type u_1
n : Type u_2
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
R : Type v
inst✝ : CommRing R
e : n ≃ m
A : Matrix m m R
σ : Perm n
i : n
⊢ A.submatrix (⇑e) (⇑e) (σ i) i = A ((e.permCongr σ) (e i)) (e i)