-- Mathlib/LinearAlgebra/Matrix/Determinant/TotallyUnimodular.lean
/-- If `A` is totally unimodular and each row of `B` is all zeros except for at most a single `1` or
a single `-1` then `fromRows A B` is totally unimodular. -/
lemma IsTotallyUnimodular.fromRows_unitlike [DecidableEq n] {A : Matrix m n R} {B : Matrix m' n R}
    (hA : A.IsTotallyUnimodular)
    (hB : Nonempty n → ∀ i : m', ∃ j : n, ∃ s : SignType, B i = Pi.single j s.cast) :
    (fromRows A B).IsTotallyUnimodular

Proof state:
m : Type u_1
m' : Type u_2
n : Type u_3
R : Type u_5
inst✝¹ : CommRing R
inst✝ : DecidableEq n
A : Matrix m n R
B : Matrix m' n R
hA : A.IsTotallyUnimodular
k : ℕ
ih :
  ∀ (f : Fin k → m ⊕ m') (g : Fin k → n),
    Function.Injective f → Function.Injective g → ((A.fromRows B).submatrix f g).det ∈ Set.range SignType.cast
f : Fin (k + 1) → m ⊕ m'
g : Fin (k + 1) → n
hf : Function.Injective f
hg : Function.Injective g
hB : ∀ (i : m'), ∃ j s, B i = Pi.single j ↑s
i : Fin (k + 1)
j : m'
hfi : f i = Sum.inr j
s : SignType
x : Fin (k + 1)
hj' : B j = Pi.single (g x) ↑s
hAB :
  ((A.fromRows B).submatrix f g).det =
    (-1) ^ (↑i + ↑x) * ↑s * (((A.fromRows B).submatrix f g).submatrix i.succAbove x.succAbove).det
⊢ ↑SignType.castHom (-1) = -1

Tactic:
simp

Result:
no goals

Proof state:
m : Type u_1
m' : Type u_2
n : Type u_3
R : Type u_5
inst✝¹ : CommRing R
inst✝ : DecidableEq n
A : Matrix m n R
B : Matrix m' n R
hA : A.IsTotallyUnimodular
k : ℕ
ih :
  ∀ (f : Fin k → m ⊕ m') (g : Fin k → n),
    Function.Injective f → Function.Injective g → ((A.fromRows B).submatrix f g).det ∈ Set.range SignType.cast
f : Fin (k + 1) → m ⊕ m'
g : Fin (k + 1) → n
hf : Function.Injective f
hg : Function.Injective g
hB : ∀ (i : m'), ∃ j s, B i = Pi.single j ↑s
f' : Fin (k + 1) → m
hf' : ∀ (x : Fin (k + 1)), f x = Sum.inl (f' x)
⊢ ∃ f', f = Sum.inl ∘ f'

Tactic:
exact ⟨f', funext hf'⟩

Result:
no goals

Proof state:
case succ.inl.intro.intro
m : Type u_1
m' : Type u_2
n : Type u_3
R : Type u_5
inst✝¹ : CommRing R
inst✝ : DecidableEq n
A : Matrix m n R
B : Matrix m' n R
hA : A.IsTotallyUnimodular
k : ℕ
ih :
  ∀ (f : Fin k → m ⊕ m') (g : Fin k → n),
    Function.Injective f → Function.Injective g → ((A.fromRows B).submatrix f g).det ∈ Set.range SignType.cast
f : Fin (k + 1) → m ⊕ m'
g : Fin (k + 1) → n
hf : Function.Injective f
hg : Function.Injective g
hB : ∀ (i : m'), ∃ j s, B i = Pi.single j ↑s
i : Fin (k + 1)
j : m'
hfi : f i = Sum.inr j
hAB :
  ((A.fromRows B).submatrix f g).det =
    ∑ j : Fin k.succ,
      (-1) ^ (↑i + ↑j) * (A.fromRows B).submatrix f g i j *
        (((A.fromRows B).submatrix f g).submatrix i.succAbove j.succAbove).det
⊢ ((A.fromRows B).submatrix f g).det ∈ Set.range SignType.cast

Tactic:
simp only [submatrix_apply, hfi, fromRows_apply_inr] at hAB

Result:
case succ.inl.intro.intro
m : Type u_1
m' : Type u_2
n : Type u_3
R : Type u_5
inst✝¹ : CommRing R
inst✝ : DecidableEq n
A : Matrix m n R
B : Matrix m' n R
hA : A.IsTotallyUnimodular
k : ℕ
ih :
  ∀ (f : Fin k → m ⊕ m') (g : Fin k → n),
    Function.Injective f → Function.Injective g → ((A.fromRows B).submatrix f g).det ∈ Set.range SignType.cast
f : Fin (k + 1) → m ⊕ m'
g : Fin (k + 1) → n
hf : Function.Injective f
hg : Function.Injective g
hB : ∀ (i : m'), ∃ j s, B i = Pi.single j ↑s
i : Fin (k + 1)
j : m'
hfi : f i = Sum.inr j
hAB :
  ((A.fromRows B).submatrix f g).det =
    ∑ x : Fin k.succ,
      (-1) ^ (↑i + ↑x) * B j (g x) * (((A.fromRows B).submatrix f g).submatrix i.succAbove x.succAbove).det
⊢ ((A.fromRows B).submatrix f g).det ∈ Set.range SignType.cast

Proof state:
m : Type u_1
m' : Type u_2
n : Type u_3
R : Type u_5
inst✝¹ : CommRing R
inst✝ : DecidableEq n
A : Matrix m n R
B : Matrix m' n R
hA : A.IsTotallyUnimodular
k : ℕ
ih :
  ∀ (f : Fin k → m ⊕ m') (g : Fin k → n),
    Function.Injective f → Function.Injective g → ((A.fromRows B).submatrix f g).det ∈ Set.range SignType.cast
f : Fin (k + 1) → m ⊕ m'
g : Fin (k + 1) → n
hf : Function.Injective f
hg : Function.Injective g
hB : ∀ (i : m'), ∃ j s, B i = Pi.single j ↑s
i : Fin (k + 1)
j : m'
hfi : f i = Sum.inr j
s : SignType
x : Fin (k + 1)
hj' : B j = Pi.single (g x) ↑s
hAB :
  ((A.fromRows B).submatrix f g).det =
    ∑ x_1 : Fin k.succ,
      (-1) ^ (↑i + ↑x_1) * Pi.single (g x) (↑s) (g x_1) *
        (((A.fromRows B).submatrix f g).submatrix i.succAbove x_1.succAbove).det
y : Fin (k + 1)
hxy : y ≠ x
⊢ (-1) ^ (↑i + ↑y) * Pi.single (g x) (↑s) (g y) *
      (((A.fromRows B).submatrix f g).submatrix i.succAbove y.succAbove).det =
    0

Tactic:
simp [Pi.single_eq_of_ne, hg.ne_iff.mpr hxy]

Result:
no goals

Proof state:
case succ.inr.intro
m : Type u_1
m' : Type u_2
n : Type u_3
R : Type u_5
inst✝¹ : CommRing R
inst✝ : DecidableEq n
A : Matrix m n R
B : Matrix m' n R
hA : ∀ (k : ℕ) (f : Fin k → m) (g : Fin k → n), (A.submatrix f g).det ∈ Set.range SignType.cast
k : ℕ
ih :
  ∀ (f : Fin k → m ⊕ m') (g : Fin k → n),
    Function.Injective f → Function.Injective g → ((A.fromRows B).submatrix f g).det ∈ Set.range SignType.cast
g : Fin (k + 1) → n
hg : Function.Injective g
hB : ∀ (i : m'), ∃ j s, B i = Pi.single j ↑s
f' : Fin (k + 1) → m
hf : Function.Injective (Sum.inl ∘ f')
⊢ ((A.fromRows B).submatrix (Sum.inl ∘ f') g).det ∈ Set.range SignType.cast

Tactic:
apply hA

Result:
no goals

Proof state:
case succ.inl.intro.intro
m : Type u_1
m' : Type u_2
n : Type u_3
R : Type u_5
inst✝¹ : CommRing R
inst✝ : DecidableEq n
A : Matrix m n R
B : Matrix m' n R
hA : A.IsTotallyUnimodular
k : ℕ
ih :
  ∀ (f : Fin k → m ⊕ m') (g : Fin k → n),
    Function.Injective f → Function.Injective g → ((A.fromRows B).submatrix f g).det ∈ Set.range SignType.cast
f : Fin (k + 1) → m ⊕ m'
g : Fin (k + 1) → n
hf : Function.Injective f
hg : Function.Injective g
hB : ∀ (i : m'), ∃ j s, B i = Pi.single j ↑s
i : Fin (k + 1)
j : m'
hfi : f i = Sum.inr j
hAB :
  ((A.fromRows B).submatrix f g).det =
    ∑ x : Fin k.succ,
      (-1) ^ (↑i + ↑x) * B j (g x) * (((A.fromRows B).submatrix f g).submatrix i.succAbove x.succAbove).det
⊢ ((A.fromRows B).submatrix f g).det ∈ Set.range SignType.cast

Tactic:
obtain ⟨j', s, hj'⟩ := hB j

Result:
case succ.inl.intro.intro.intro.intro
m : Type u_1
m' : Type u_2
n : Type u_3
R : Type u_5
inst✝¹ : CommRing R
inst✝ : DecidableEq n
A : Matrix m n R
B : Matrix m' n R
hA : A.IsTotallyUnimodular
k : ℕ
ih :
  ∀ (f : Fin k → m ⊕ m') (g : Fin k → n),
    Function.Injective f → Function.Injective g → ((A.fromRows B).submatrix f g).det ∈ Set.range SignType.cast
f : Fin (k + 1) → m ⊕ m'
g : Fin (k + 1) → n
hf : Function.Injective f
hg : Function.Injective g
hB : ∀ (i : m'), ∃ j s, B i = Pi.single j ↑s
i : Fin (k + 1)
j : m'
hfi : f i = Sum.inr j
hAB :
  ((A.fromRows B).submatrix f g).det =
    ∑ x : Fin k.succ,
      (-1) ^ (↑i + ↑x) * B j (g x) * (((A.fromRows B).submatrix f g).submatrix i.succAbove x.succAbove).det
j' : n
s : SignType
hj' : B j = Pi.single j' ↑s
⊢ ((A.fromRows B).submatrix f g).det ∈ Set.range SignType.cast