-- Mathlib/LinearAlgebra/Matrix/Determinant/TotallyUnimodular.lean
lemma isTotallyUnimodular_iff_fintype.{w} (A : Matrix m n R) : A.IsTotallyUnimodular ↔
    ∀ (ι : Type w) [Fintype ι] [DecidableEq ι], ∀ f : ι → m, ∀ g : ι → n,
      (A.submatrix f g).det ∈ Set.range SignType.cast

Proof state:
m : Type u_1
n : Type u_3
R : Type u_5
inst✝ : CommRing R
A : Matrix m n R
⊢ (∀ (k : ℕ) (f : Fin k → m) (g : Fin k → n), (A.submatrix f g).det ∈ Set.range SignType.cast) ↔
    ∀ (ι : Type w) [inst : Fintype ι] [inst_1 : DecidableEq ι] (f : ι → m) (g : ι → n),
      (A.submatrix f g).det ∈ Set.range SignType.cast

Tactic:
constructor

Result:
case mp
m : Type u_1
n : Type u_3
R : Type u_5
inst✝ : CommRing R
A : Matrix m n R
⊢ (∀ (k : ℕ) (f : Fin k → m) (g : Fin k → n), (A.submatrix f g).det ∈ Set.range SignType.cast) →
    ∀ (ι : Type w) [inst : Fintype ι] [inst_1 : DecidableEq ι] (f : ι → m) (g : ι → n),
      (A.submatrix f g).det ∈ Set.range SignType.cast

case mpr
m : Type u_1
n : Type u_3
R : Type u_5
inst✝ : CommRing R
A : Matrix m n R
⊢ (∀ (ι : Type w) [inst : Fintype ι] [inst_1 : DecidableEq ι] (f : ι → m) (g : ι → n),
      (A.submatrix f g).det ∈ Set.range SignType.cast) →
    ∀ (k : ℕ) (f : Fin k → m) (g : Fin k → n), (A.submatrix f g).det ∈ Set.range SignType.cast

Proof state:
m : Type u_1
n : Type u_3
R : Type u_5
inst✝ : CommRing R
A : Matrix m n R
⊢ A.IsTotallyUnimodular ↔
    ∀ (ι : Type w) [inst : Fintype ι] [inst_1 : DecidableEq ι] (f : ι → m) (g : ι → n),
      (A.submatrix f g).det ∈ Set.range SignType.cast

Tactic:
rw [isTotallyUnimodular_iff]

Result:
m : Type u_1
n : Type u_3
R : Type u_5
inst✝ : CommRing R
A : Matrix m n R
⊢ (∀ (k : ℕ) (f : Fin k → m) (g : Fin k → n), (A.submatrix f g).det ∈ Set.range SignType.cast) ↔
    ∀ (ι : Type w) [inst : Fintype ι] [inst_1 : DecidableEq ι] (f : ι → m) (g : ι → n),
      (A.submatrix f g).det ∈ Set.range SignType.cast

Proof state:
case mp
m : Type u_1
n : Type u_3
R : Type u_5
inst✝ : CommRing R
A : Matrix m n R
⊢ (∀ (k : ℕ) (f : Fin k → m) (g : Fin k → n), (A.submatrix f g).det ∈ Set.range SignType.cast) →
    ∀ (ι : Type w) [inst : Fintype ι] [inst_1 : DecidableEq ι] (f : ι → m) (g : ι → n),
      (A.submatrix f g).det ∈ Set.range SignType.cast

Tactic:
intro hA ι _ _ f g

Result:
case mp
m : Type u_1
n : Type u_3
R : Type u_5
inst✝² : CommRing R
A : Matrix m n R
hA : ∀ (k : ℕ) (f : Fin k → m) (g : Fin k → n), (A.submatrix f g).det ∈ Set.range SignType.cast
ι : Type w
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
f : ι → m
g : ι → n
⊢ (A.submatrix f g).det ∈ Set.range SignType.cast

Proof state:
case mp
m : Type u_1
n : Type u_3
R : Type u_5
inst✝² : CommRing R
A : Matrix m n R
hA : ∀ (k : ℕ) (f : Fin k → m) (g : Fin k → n), (A.submatrix f g).det ∈ Set.range SignType.cast
ι : Type w
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
f : ι → m
g : ι → n
⊢ (A.submatrix f g).det ∈ Set.range SignType.cast

Tactic:
specialize hA (Fintype.card ι) (f ∘ (Fintype.equivFin ι).symm) (g ∘ (Fintype.equivFin ι).symm)

Result:
case mp
m : Type u_1
n : Type u_3
R : Type u_5
inst✝² : CommRing R
A : Matrix m n R
ι : Type w
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
f : ι → m
g : ι → n
hA : (A.submatrix (f ∘ ⇑(Fintype.equivFin ι).symm) (g ∘ ⇑(Fintype.equivFin ι).symm)).det ∈ Set.range SignType.cast
⊢ (A.submatrix f g).det ∈ Set.range SignType.cast

Proof state:
case mpr
m : Type u_1
n : Type u_3
R : Type u_5
inst✝ : CommRing R
A : Matrix m n R
hA :
  ∀ (ι : Type w) [inst : Fintype ι] [inst_1 : DecidableEq ι] (f : ι → m) (g : ι → n),
    (A.submatrix f g).det ∈ Set.range SignType.cast
k : ℕ
f : Fin k → m
g : Fin k → n
⊢ (A.submatrix f g).det ∈ Set.range SignType.cast

Tactic:
specialize hA (ULift (Fin k)) (f ∘ Equiv.ulift) (g ∘ Equiv.ulift)

Result:
case mpr
m : Type u_1
n : Type u_3
R : Type u_5
inst✝ : CommRing R
A : Matrix m n R
k : ℕ
f : Fin k → m
g : Fin k → n
hA : (A.submatrix (f ∘ ⇑Equiv.ulift) (g ∘ ⇑Equiv.ulift)).det ∈ Set.range SignType.cast
⊢ (A.submatrix f g).det ∈ Set.range SignType.cast

Proof state:
case mp
m : Type u_1
n : Type u_3
R : Type u_5
inst✝² : CommRing R
A : Matrix m n R
ι : Type w
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
f : ι → m
g : ι → n
hA : (A.submatrix (f ∘ ⇑(Fintype.equivFin ι).symm) (g ∘ ⇑(Fintype.equivFin ι).symm)).det ∈ Set.range SignType.cast
⊢ (A.submatrix f g).det ∈ Set.range SignType.cast

Tactic:
rwa [←submatrix_submatrix, det_submatrix_equiv_self] at hA

Result:
no goals

Proof state:
case mpr
m : Type u_1
n : Type u_3
R : Type u_5
inst✝ : CommRing R
A : Matrix m n R
k : ℕ
f : Fin k → m
g : Fin k → n
hA : (A.submatrix (f ∘ ⇑Equiv.ulift) (g ∘ ⇑Equiv.ulift)).det ∈ Set.range SignType.cast
⊢ (A.submatrix f g).det ∈ Set.range SignType.cast

Tactic:
rwa [←submatrix_submatrix, det_submatrix_equiv_self] at hA

Result:
no goals

Proof state:
case mpr
m : Type u_1
n : Type u_3
R : Type u_5
inst✝ : CommRing R
A : Matrix m n R
⊢ (∀ (ι : Type w) [inst : Fintype ι] [inst_1 : DecidableEq ι] (f : ι → m) (g : ι → n),
      (A.submatrix f g).det ∈ Set.range SignType.cast) →
    ∀ (k : ℕ) (f : Fin k → m) (g : Fin k → n), (A.submatrix f g).det ∈ Set.range SignType.cast

Tactic:
intro hA k f g

Result:
case mpr
m : Type u_1
n : Type u_3
R : Type u_5
inst✝ : CommRing R
A : Matrix m n R
hA :
  ∀ (ι : Type w) [inst : Fintype ι] [inst_1 : DecidableEq ι] (f : ι → m) (g : ι → n),
    (A.submatrix f g).det ∈ Set.range SignType.cast
k : ℕ
f : Fin k → m
g : Fin k → n
⊢ (A.submatrix f g).det ∈ Set.range SignType.cast