-- Mathlib/LinearAlgebra/Matrix/Determinant/Basic.lean
theorem abs_det_submatrix_equiv_equiv {R : Type*} [LinearOrderedCommRing R]
    (e₁ e₂ : n ≃ m) (A : Matrix m m R) :
    |(A.submatrix e₁ e₂).det| = |A.det|

Proof state:
m : Type u_1
n : Type u_2
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
R : Type u_3
inst✝ : LinearOrderedCommRing R
e₁ e₂ : n ≃ m
A : Matrix m m R
hee : e₂ = e₁.trans (e₁.symm.trans e₂)
⊢ |((A.submatrix id ⇑(e₁.symm.trans e₂)).submatrix ⇑e₁ ⇑e₁).det| = |A.det|

Tactic:
rw [Matrix.det_submatrix_equiv_self, Matrix.det_permute', abs_mul, abs_unit_intCast, one_mul]

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 u_3
inst✝ : LinearOrderedCommRing R
e₁ e₂ : n ≃ m
A : Matrix m m R
hee : e₂ = e₁.trans (e₁.symm.trans e₂)
⊢ |(A.submatrix ⇑e₁ ⇑(e₁.trans (e₁.symm.trans e₂))).det| = |A.det|

Tactic:
show |((A.submatrix id (e₁.symm.trans e₂)).submatrix e₁ e₁).det| = |A.det|

Result:
m : Type u_1
n : Type u_2
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
R : Type u_3
inst✝ : LinearOrderedCommRing R
e₁ e₂ : n ≃ m
A : Matrix m m R
hee : e₂ = e₁.trans (e₁.symm.trans e₂)
⊢ |((A.submatrix id ⇑(e₁.symm.trans e₂)).submatrix ⇑e₁ ⇑e₁).det| = |A.det|

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

Tactic:
have hee : e₂ = e₁.trans (e₁.symm.trans e₂) := by ext; simp

Result:
m : Type u_1
n : Type u_2
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
R : Type u_3
inst✝ : LinearOrderedCommRing R
e₁ e₂ : n ≃ m
A : Matrix m m R
hee : e₂ = e₁.trans (e₁.symm.trans e₂)
⊢ |(A.submatrix ⇑e₁ ⇑e₂).det| = |A.det|

Proof state:
m : Type u_1
n : Type u_2
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
R : Type u_3
inst✝ : LinearOrderedCommRing R
e₁ e₂ : n ≃ m
A : Matrix m m R
hee : e₂ = e₁.trans (e₁.symm.trans e₂)
⊢ |(A.submatrix ⇑e₁ ⇑e₂).det| = |A.det|

Tactic:
rw [hee]

Result:
m : Type u_1
n : Type u_2
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
R : Type u_3
inst✝ : LinearOrderedCommRing R
e₁ e₂ : n ≃ m
A : Matrix m m R
hee : e₂ = e₁.trans (e₁.symm.trans e₂)
⊢ |(A.submatrix ⇑e₁ ⇑(e₁.trans (e₁.symm.trans e₂))).det| = |A.det|

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 u_3
inst✝ : LinearOrderedCommRing R
e₁ e₂ : n ≃ m
A : Matrix m m R
x✝ : n
⊢ e₂ x✝ = (e₁.trans (e₁.symm.trans e₂)) x✝

Tactic:
simp

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 u_3
inst✝ : LinearOrderedCommRing R
e₁ e₂ : n ≃ m
A : Matrix m m R
⊢ e₂ = e₁.trans (e₁.symm.trans e₂)

Tactic:
ext

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 u_3
inst✝ : LinearOrderedCommRing R
e₁ e₂ : n ≃ m
A : Matrix m m R
x✝ : n
⊢ e₂ x✝ = (e₁.trans (e₁.symm.trans e₂)) x✝