-- Mathlib/LinearAlgebra/Matrix/Determinant/TotallyUnimodular.lean
lemma isTotallyUnimodular_iff (A : Matrix m n R) : A.IsTotallyUnimodular ↔
    ∀ k : ℕ, ∀ f : Fin k → m, ∀ g : Fin k → n,
      (A.submatrix f g).det ∈ Set.range SignType.cast

Proof state:
case h.inl.intro.intro.intro
m : Type u_1
n : Type u_3
R : Type u_5
inst✝ : CommRing R
A : Matrix m n R
hA : A.IsTotallyUnimodular
k : ℕ
f : Fin k → m
g : Fin k → n
i j : Fin k
hfij : f i = f j
hij : i ≠ j
⊢ ∀ (k_1 : Fin k), Aᵀ.submatrix g f k_1 j = Aᵀ.submatrix g f k_1 i

Tactic:
simp [hfij]

Result:
no goals

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 : A.IsTotallyUnimodular
k : ℕ
f : Fin k → m
g : Fin k → n
⊢ (A.submatrix f g).det ∈ Set.range SignType.cast

Tactic:
by_cases hfg : f.Injective ∧ g.Injective

Result:
case pos
m : Type u_1
n : Type u_3
R : Type u_5
inst✝ : CommRing R
A : Matrix m n R
hA : A.IsTotallyUnimodular
k : ℕ
f : Fin k → m
g : Fin k → n
hfg : Function.Injective f ∧ Function.Injective g
⊢ (A.submatrix f g).det ∈ Set.range SignType.cast

case neg
m : Type u_1
n : Type u_3
R : Type u_5
inst✝ : CommRing R
A : Matrix m n R
hA : A.IsTotallyUnimodular
k : ℕ
f : Fin k → m
g : Fin k → n
hfg : ¬(Function.Injective f ∧ Function.Injective g)
⊢ (A.submatrix f g).det ∈ Set.range SignType.cast

Proof state:
case h
m : Type u_1
n : Type u_3
R : Type u_5
inst✝ : CommRing R
A : Matrix m n R
hA : A.IsTotallyUnimodular
k : ℕ
f : Fin k → m
g : Fin k → n
hfg : ¬(Function.Injective f ∧ Function.Injective g)
⊢ ↑0 = (A.submatrix f g).det

Tactic:
rw [SignType.coe_zero, eq_comm]

Result:
case h
m : Type u_1
n : Type u_3
R : Type u_5
inst✝ : CommRing R
A : Matrix m n R
hA : A.IsTotallyUnimodular
k : ℕ
f : Fin k → m
g : Fin k → n
hfg : ¬(Function.Injective f ∧ Function.Injective g)
⊢ (A.submatrix f g).det = 0

Proof state:
case pos
m : Type u_1
n : Type u_3
R : Type u_5
inst✝ : CommRing R
A : Matrix m n R
hA : A.IsTotallyUnimodular
k : ℕ
f : Fin k → m
g : Fin k → n
hfg : Function.Injective f ∧ Function.Injective g
⊢ (A.submatrix f g).det ∈ Set.range SignType.cast

Tactic:
exact hA k f g hfg.1 hfg.2

Result:
no goals

Proof state:
case h.inr.intro.intro.intro
m : Type u_1
n : Type u_3
R : Type u_5
inst✝ : CommRing R
A : Matrix m n R
hA : A.IsTotallyUnimodular
k : ℕ
f : Fin k → m
g : Fin k → n
i j : Fin k
hgij : g i = g j
hij : i ≠ j
⊢ ∀ (k_1 : Fin k), A.submatrix f g k_1 i = A.submatrix f g k_1 j

Tactic:
simp [hgij]

Result:
no goals

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 : A.IsTotallyUnimodular
⊢ ∀ (k : ℕ) (f : Fin k → m) (g : Fin k → n), (A.submatrix f g).det ∈ Set.range SignType.cast

Tactic:
intro k 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 : A.IsTotallyUnimodular
k : ℕ
f : Fin k → m
g : Fin k → n
⊢ (A.submatrix f g).det ∈ Set.range SignType.cast

Proof state:
case h.inl.intro.intro.intro
m : Type u_1
n : Type u_3
R : Type u_5
inst✝ : CommRing R
A : Matrix m n R
hA : A.IsTotallyUnimodular
k : ℕ
f : Fin k → m
g : Fin k → n
i j : Fin k
hfij : f i = f j
hij : i ≠ j
⊢ (A.submatrix f g).det = 0

Tactic:
rw [← det_transpose, transpose_submatrix]

Result:
case h.inl.intro.intro.intro
m : Type u_1
n : Type u_3
R : Type u_5
inst✝ : CommRing R
A : Matrix m n R
hA : A.IsTotallyUnimodular
k : ℕ
f : Fin k → m
g : Fin k → n
i j : Fin k
hfij : f i = f j
hij : i ≠ j
⊢ (Aᵀ.submatrix g f).det = 0

Proof state:
case h
m : Type u_1
n : Type u_3
R : Type u_5
inst✝ : CommRing R
A : Matrix m n R
hA : A.IsTotallyUnimodular
k : ℕ
f : Fin k → m
g : Fin k → n
hfg : (∃ a b, f a = f b ∧ a ≠ b) ∨ ∃ a b, g a = g b ∧ a ≠ b
⊢ (A.submatrix f g).det = 0

Tactic:
obtain ⟨i, j, hfij, hij⟩ | ⟨i, j, hgij, hij⟩ := hfg

Result:
case h.inl.intro.intro.intro
m : Type u_1
n : Type u_3
R : Type u_5
inst✝ : CommRing R
A : Matrix m n R
hA : A.IsTotallyUnimodular
k : ℕ
f : Fin k → m
g : Fin k → n
i j : Fin k
hfij : f i = f j
hij : i ≠ j
⊢ (A.submatrix f g).det = 0

case h.inr.intro.intro.intro
m : Type u_1
n : Type u_3
R : Type u_5
inst✝ : CommRing R
A : Matrix m n R
hA : A.IsTotallyUnimodular
k : ℕ
f : Fin k → m
g : Fin k → n
i j : Fin k
hgij : g i = g j
hij : i ≠ j
⊢ (A.submatrix f g).det = 0

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 : ∀ (k : ℕ) (f : Fin k → m) (g : Fin k → n), (A.submatrix f g).det ∈ Set.range SignType.cast
⊢ A.IsTotallyUnimodular

Tactic:
intro _ _ _ _ _

Result:
case mpr
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
k✝ : ℕ
f✝ : Fin k✝ → m
g✝ : Fin k✝ → n
a✝¹ : Function.Injective f✝
a✝ : Function.Injective g✝
⊢ (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 : ∀ (k : ℕ) (f : Fin k → m) (g : Fin k → n), (A.submatrix f g).det ∈ Set.range SignType.cast
k✝ : ℕ
f✝ : Fin k✝ → m
g✝ : Fin k✝ → n
a✝¹ : Function.Injective f✝
a✝ : Function.Injective g✝
⊢ (A.submatrix f✝ g✝).det ∈ Set.range SignType.cast

Tactic:
apply hA

Result:
no goals

Proof state:
case h
m : Type u_1
n : Type u_3
R : Type u_5
inst✝ : CommRing R
A : Matrix m n R
hA : A.IsTotallyUnimodular
k : ℕ
f : Fin k → m
g : Fin k → n
hfg : ¬(Function.Injective f ∧ Function.Injective g)
⊢ (A.submatrix f g).det = 0

Tactic:
simp_rw [not_and_or, Function.not_injective_iff] at hfg

Result:
case h
m : Type u_1
n : Type u_3
R : Type u_5
inst✝ : CommRing R
A : Matrix m n R
hA : A.IsTotallyUnimodular
k : ℕ
f : Fin k → m
g : Fin k → n
hfg : (∃ a b, f a = f b ∧ a ≠ b) ∨ ∃ a b, g a = g b ∧ a ≠ b
⊢ (A.submatrix f g).det = 0

Proof state:
case h.inl.intro.intro.intro
m : Type u_1
n : Type u_3
R : Type u_5
inst✝ : CommRing R
A : Matrix m n R
hA : A.IsTotallyUnimodular
k : ℕ
f : Fin k → m
g : Fin k → n
i j : Fin k
hfij : f i = f j
hij : i ≠ j
⊢ (Aᵀ.submatrix g f).det = 0

Tactic:
apply det_zero_of_column_eq hij.symm

Result:
case h.inl.intro.intro.intro
m : Type u_1
n : Type u_3
R : Type u_5
inst✝ : CommRing R
A : Matrix m n R
hA : A.IsTotallyUnimodular
k : ℕ
f : Fin k → m
g : Fin k → n
i j : Fin k
hfij : f i = f j
hij : i ≠ j
⊢ ∀ (k_1 : Fin k), Aᵀ.submatrix g f k_1 j = Aᵀ.submatrix g f k_1 i

Proof state:
case neg
m : Type u_1
n : Type u_3
R : Type u_5
inst✝ : CommRing R
A : Matrix m n R
hA : A.IsTotallyUnimodular
k : ℕ
f : Fin k → m
g : Fin k → n
hfg : ¬(Function.Injective f ∧ Function.Injective g)
⊢ (A.submatrix f g).det ∈ Set.range SignType.cast

Tactic:
use 0

Result:
case h
m : Type u_1
n : Type u_3
R : Type u_5
inst✝ : CommRing R
A : Matrix m n R
hA : A.IsTotallyUnimodular
k : ℕ
f : Fin k → m
g : Fin k → n
hfg : ¬(Function.Injective f ∧ Function.Injective g)
⊢ ↑0 = (A.submatrix f g).det

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

Tactic:
constructor <;> intro hA

Result:
case mp
m : Type u_1
n : Type u_3
R : Type u_5
inst✝ : CommRing R
A : Matrix m n R
hA : A.IsTotallyUnimodular
⊢ ∀ (k : ℕ) (f : Fin k → m) (g : Fin k → 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
hA : ∀ (k : ℕ) (f : Fin k → m) (g : Fin k → n), (A.submatrix f g).det ∈ Set.range SignType.cast
⊢ A.IsTotallyUnimodular