awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Matrix.Determinant.TotallyUnimodular
Goal:
m : Type u_1
m' : Type u_2
n : Type u_3
R : Type u_5
inst : CommRing R
inst_1 : 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) (hf : Function.Injective f) (hg : Function.Injective g),
    Membership.mem (γ := Set R) (Set.range SignType.cast) ((A.fromRows B).submatrix f g).det
f : Fin (k + 1) → m ⊕ m'
g : Fin (k + 1) → n
hf : Function.Injective f
hg : Function.Injective g
hB : ∀ (i : m'), ∃ (j : n) (s : SignType), B i = Pi.single (M := fun (j : n) ↦ R) j (↑s : R)
i : Fin (k + 1)
j : m'
hfi : f i = Sum.inr j
⊢ ((A.fromRows B).submatrix f g).det =
    ∑ j : Fin k.succ,
      HPow.hPow (α := R) (-1) ((↑i : ℕ) + (↑j : ℕ)) * (A.fromRows B).submatrix f g i j *
        (((A.fromRows B).submatrix f g).submatrix i.succAbove j.succAbove).det

Tactic:
have hAB := det_succ_row ((fromRows A B).submatrix f g) i
-- Module: Mathlib.LinearAlgebra.Matrix.Determinant.TotallyUnimodular
Goal:
m : Type u_1
m' : Type u_2
n : Type u_3
R : Type u_5
inst : CommRing R
inst_1 : 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) (hf : Function.Injective f) (hg : Function.Injective g),
    Membership.mem (γ := Set R) (Set.range SignType.cast) ((A.fromRows B).submatrix f g).det
f : Fin (k + 1) → m ⊕ m'
g : Fin (k + 1) → n
hf : Function.Injective f
hg : Function.Injective g
hB : ∀ (i : m'), ∃ (j : n) (s : SignType), B i = Pi.single (M := fun (j : n) ↦ R) j (↑s : R)
i : Fin (k + 1)
j : m'
hfi : f i = Sum.inr j
hAB :
  ((A.fromRows B).submatrix f g).det =
    ∑ j : Fin k.succ,
      HPow.hPow (α := R) (-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 =
    ∑ x : Fin k.succ,
      HPow.hPow (α := R) (-1) ((↑i : ℕ) + (↑x : ℕ)) * B j (g x) *
        (((A.fromRows B).submatrix f g).submatrix i.succAbove x.succAbove).det

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

Premises used: Matrix.fromRows_apply_inr, Matrix.submatrix_apply
-- Module: Mathlib.LinearAlgebra.Matrix.Determinant.TotallyUnimodular
Goal:
m : Type u_1
m' : Type u_2
n : Type u_3
R : Type u_5
inst : CommRing R
inst_1 : 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) (hf : Function.Injective f) (hg : Function.Injective g),
    Membership.mem (γ := Set R) (Set.range SignType.cast) ((A.fromRows B).submatrix f g).det
f : Fin (k + 1) → m ⊕ m'
g : Fin (k + 1) → n
hf : Function.Injective f
hg : Function.Injective g
hB : ∀ (i : m'), ∃ (j : n) (s : SignType), B i = Pi.single (M := fun (j : n) ↦ R) j (↑s : R)
i : Fin (k + 1)
j : m'
hfi : f i = Sum.inr j
hAB :
  ((A.fromRows B).submatrix f g).det =
    ∑ x : Fin k.succ,
      HPow.hPow (α := R) (-1) ((↑i : ℕ) + (↑x : ℕ)) * B j (g x) *
        (((A.fromRows B).submatrix f g).submatrix i.succAbove x.succAbove).det
succ :
  ∀ (j' : n) (s : SignType) (hj' : B j = Pi.single (M := fun (j : n) ↦ R) j' (↑s : R)),
    Membership.mem (γ := Set R) (Set.range SignType.cast) ((A.fromRows B).submatrix f g).det
⊢ Membership.mem (γ := Set R) (Set.range SignType.cast) ((A.fromRows B).submatrix f g).det

Tactic:
obtain ⟨j', s, hj'⟩ := hB j
-- Module: Mathlib.LinearAlgebra.Matrix.Determinant.TotallyUnimodular
Goal:
m : Type u_1
m' : Type u_2
n : Type u_3
R : Type u_5
inst : CommRing R
inst_1 : 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) (hf : Function.Injective f) (hg : Function.Injective g),
    Membership.mem (γ := Set R) (Set.range SignType.cast) ((A.fromRows B).submatrix f g).det
f : Fin (k + 1) → m ⊕ m'
g : Fin (k + 1) → n
hf : Function.Injective f
hg : Function.Injective g
hB : ∀ (i : m'), ∃ (j : n) (s : SignType), B i = Pi.single (M := fun (j : n) ↦ R) j (↑s : R)
i : Fin (k + 1)
j : m'
hfi : f i = Sum.inr j
hAB :
  ((A.fromRows B).submatrix f g).det =
    ∑ x : Fin k.succ,
      HPow.hPow (α := R) (-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 (M := fun (j : n) ↦ R) j' (↑s : R)
⊢ ((A.fromRows B).submatrix f g).det =
    ∑ x : Fin k.succ,
      HMul.hMul (β := R) (HPow.hPow (α := R) (-1) ((↑i : ℕ) + (↑x : ℕ)))
          (Pi.single (M := fun (j : n) ↦ R) j' (↑s : R) (g x) : R) *
        (((A.fromRows B).submatrix f g).submatrix i.succAbove x.succAbove).det

Tactic:
simp only [hj'] at hAB
-- Module: Mathlib.LinearAlgebra.Matrix.Determinant.TotallyUnimodular
Goal:
m : Type u_1
m' : Type u_2
n : Type u_3
R : Type u_5
inst : CommRing R
inst_1 : 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) (hf : Function.Injective f) (hg : Function.Injective g),
    Membership.mem (γ := Set R) (Set.range SignType.cast) ((A.fromRows B).submatrix f g).det
f : Fin (k + 1) → m ⊕ m'
g : Fin (k + 1) → n
hf : Function.Injective f
hg : Function.Injective g
hB : ∀ (i : m'), ∃ (j : n) (s : SignType), B i = Pi.single (M := fun (j : n) ↦ R) j (↑s : R)
i : Fin (k + 1)
j : m'
hfi : f i = Sum.inr j
j' : n
s : SignType
hj' : B j = Pi.single (M := fun (j : n) ↦ R) j' (↑s : R)
hAB :
  ((A.fromRows B).submatrix f g).det =
    ∑ x : Fin k.succ,
      HMul.hMul (β := R) (HPow.hPow (α := R) (-1) ((↑i : ℕ) + (↑x : ℕ)))
          (Pi.single (M := fun (j : n) ↦ R) j' (↑s : R) (g x) : R) *
        (((A.fromRows B).submatrix f g).submatrix i.succAbove x.succAbove).det
pos :
  ∀ (hj'' : ∃ (x : Fin (k + 1)), g x = j'),
    Membership.mem (γ := Set R) (Set.range SignType.cast) ((A.fromRows B).submatrix f g).det
neg :
  ∀ (hj'' : ¬∃ (x : Fin (k + 1)), g x = j'),
    Membership.mem (γ := Set R) (Set.range SignType.cast) ((A.fromRows B).submatrix f g).det
⊢ Membership.mem (γ := Set R) (Set.range SignType.cast) ((A.fromRows B).submatrix f g).det

Tactic:
by_cases hj'' : ∃ x, g x = j'
-- Module: Mathlib.LinearAlgebra.Matrix.Determinant.TotallyUnimodular
Goal:
m : Type u_1
m' : Type u_2
n : Type u_3
R : Type u_5
inst : CommRing R
inst_1 : 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) (hf : Function.Injective f) (hg : Function.Injective g),
    Membership.mem (γ := Set R) (Set.range SignType.cast) ((A.fromRows B).submatrix f g).det
f : Fin (k + 1) → m ⊕ m'
g : Fin (k + 1) → n
hf : Function.Injective f
hg : Function.Injective g
hB : ∀ (i : m'), ∃ (j : n) (s : SignType), B i = Pi.single (M := fun (j : n) ↦ R) j (↑s : R)
i : Fin (k + 1)
j : m'
hfi : f i = Sum.inr j
j' : n
s : SignType
hj' : B j = Pi.single (M := fun (j : n) ↦ R) j' (↑s : R)
hAB :
  ((A.fromRows B).submatrix f g).det =
    ∑ x : Fin k.succ,
      HMul.hMul (β := R) (HPow.hPow (α := R) (-1) ((↑i : ℕ) + (↑x : ℕ)))
          (Pi.single (M := fun (j : n) ↦ R) j' (↑s : R) (g x) : R) *
        (((A.fromRows B).submatrix f g).submatrix i.succAbove x.succAbove).det
hj'' : ∃ (x : Fin (k + 1)), g x = j'
pos :
  ∀ (x : Fin (k + 1)) (hj' : B j = Pi.single (M := fun (j : n) ↦ R) (g x) (↑s : R))
    (hAB :
      ((A.fromRows B).submatrix f g).det =
        ∑ x_1 : Fin k.succ,
          HMul.hMul (β := R) (HPow.hPow (α := R) (-1) ((↑i : ℕ) + (↑x_1 : ℕ)))
              (Pi.single (M := fun (j : n) ↦ R) (g x) (↑s : R) (g x_1) : R) *
            (((A.fromRows B).submatrix f g).submatrix i.succAbove x_1.succAbove).det),
    Membership.mem (γ := Set R) (Set.range SignType.cast) ((A.fromRows B).submatrix f g).det
⊢ Membership.mem (γ := Set R) (Set.range SignType.cast) ((A.fromRows B).submatrix f g).det

Tactic:
obtain ⟨x, rfl⟩ := hj''

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.Matrix.Determinant.TotallyUnimodular
Goal:
m : Type u_1
m' : Type u_2
n : Type u_3
R : Type u_5
inst : CommRing R
inst_1 : 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) (hf : Function.Injective f) (hg : Function.Injective g),
    Membership.mem (γ := Set R) (Set.range SignType.cast) ((A.fromRows B).submatrix f g).det
f : Fin (k + 1) → m ⊕ m'
g : Fin (k + 1) → n
hf : Function.Injective f
hg : Function.Injective g
hB : ∀ (i : m'), ∃ (j : n) (s : SignType), B i = Pi.single (M := fun (j : n) ↦ R) j (↑s : R)
i : Fin (k + 1)
j : m'
hfi : f i = Sum.inr j
s : SignType
x : Fin (k + 1)
hj' : B j = Pi.single (M := fun (j : n) ↦ R) (g x) (↑s : R)
hAB :
  ((A.fromRows B).submatrix f g).det =
    ∑ x_1 : Fin k.succ,
      HMul.hMul (β := R) (HPow.hPow (α := R) (-1) ((↑i : ℕ) + (↑x_1 : ℕ)))
          (Pi.single (M := fun (j : n) ↦ R) (g x) (↑s : R) (g x_1) : R) *
        (((A.fromRows B).submatrix f g).submatrix i.succAbove x_1.succAbove).det
pos :
  ∀
    (hAB :
      ((A.fromRows B).submatrix f g).det =
        HPow.hPow (α := R) (-1) ((↑i : ℕ) + (↑x : ℕ)) * (↑s : R) *
          (((A.fromRows B).submatrix f g).submatrix i.succAbove x.succAbove).det),
    Membership.mem (γ := Set R) (Set.range SignType.cast) ((A.fromRows B).submatrix f g).det
rw :
  ∀ (y : Fin (k + 1)) (hxy : y ≠ x),
    HMul.hMul (β := R) (HPow.hPow (α := R) (-1) ((↑i : ℕ) + (↑y : ℕ)))
          (Pi.single (M := fun (j : n) ↦ R) (g x) (↑s : R) (g y) : R) *
        (((A.fromRows B).submatrix f g).submatrix i.succAbove y.succAbove).det =
      0
⊢ Membership.mem (γ := Set R) (Set.range SignType.cast) ((A.fromRows B).submatrix f g).det

Tactic:
rw [Fintype.sum_eq_single x fun y hxy => ?_, Pi.single_eq_same] at hAB

Premises used: Pi.single_eq_same, Fintype.sum_eq_single
-- Module: Mathlib.LinearAlgebra.Matrix.Determinant.TotallyUnimodular
Goal:
m : Type u_1
m' : Type u_2
n : Type u_3
R : Type u_5
inst : CommRing R
inst_1 : 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) (hf : Function.Injective f) (hg : Function.Injective g),
    Membership.mem (γ := Set R) (Set.range SignType.cast) ((A.fromRows B).submatrix f g).det
f : Fin (k + 1) → m ⊕ m'
g : Fin (k + 1) → n
hf : Function.Injective f
hg : Function.Injective g
hB : ∀ (i : m'), ∃ (j : n) (s : SignType), B i = Pi.single (M := fun (j : n) ↦ R) j (↑s : R)
i : Fin (k + 1)
j : m'
hfi : f i = Sum.inr j
s : SignType
x : Fin (k + 1)
hj' : B j = Pi.single (M := fun (j : n) ↦ R) (g x) (↑s : R)
hAB :
  ((A.fromRows B).submatrix f g).det =
    HPow.hPow (α := R) (-1) ((↑i : ℕ) + (↑x : ℕ)) * (↑s : R) *
      (((A.fromRows B).submatrix f g).submatrix i.succAbove x.succAbove).det
pos :
  Membership.mem (γ := Set R) (Set.range SignType.cast)
    (HPow.hPow (α := R) (-1) ((↑i : ℕ) + (↑x : ℕ)) * (↑s : R) *
      (((A.fromRows B).submatrix f g).submatrix i.succAbove x.succAbove).det)
⊢ Membership.mem (γ := Set R) (Set.range SignType.cast) ((A.fromRows B).submatrix f g).det

Tactic:
rw [hAB]
-- Module: Mathlib.LinearAlgebra.Matrix.Determinant.TotallyUnimodular
Goal:
m : Type u_1
m' : Type u_2
n : Type u_3
R : Type u_5
inst : CommRing R
inst_1 : 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) (hf : Function.Injective f) (hg : Function.Injective g),
    Membership.mem (γ := Set R) (Set.range SignType.cast) ((A.fromRows B).submatrix f g).det
f : Fin (k + 1) → m ⊕ m'
g : Fin (k + 1) → n
hf : Function.Injective f
hg : Function.Injective g
hB : ∀ (i : m'), ∃ (j : n) (s : SignType), B i = Pi.single (M := fun (j : n) ↦ R) j (↑s : R)
i : Fin (k + 1)
j : m'
hfi : f i = Sum.inr j
s : SignType
x : Fin (k + 1)
hj' : B j = Pi.single (M := fun (j : n) ↦ R) (g x) (↑s : R)
hAB :
  ((A.fromRows B).submatrix f g).det =
    HPow.hPow (α := R) (-1) ((↑i : ℕ) + (↑x : ℕ)) * (↑s : R) *
      (((A.fromRows B).submatrix f g).submatrix i.succAbove x.succAbove).det
pos :
  Membership.mem (γ := Submonoid R) (MonoidHom.mrange (F := SignType →* R) (↑SignType.castHom : SignType →* R))
    (HPow.hPow (α := R) (-1) ((↑i : ℕ) + (↑x : ℕ)) * (↑s : R) *
      (((A.fromRows B).submatrix f g).submatrix i.succAbove x.succAbove).det)
⊢ Membership.mem (γ := Set R) (Set.range SignType.cast)
    (HPow.hPow (α := R) (-1) ((↑i : ℕ) + (↑x : ℕ)) * (↑s : R) *
      (((A.fromRows B).submatrix f g).submatrix i.succAbove x.succAbove).det)

Tactic:
change _ ∈ MonoidHom.mrange SignType.castHom.toMonoidHom

Premises used: SignType.castHom, MonoidWithZeroHom.toMonoidHom, MonoidHom.mrange
-- Module: Mathlib.LinearAlgebra.Matrix.Determinant.TotallyUnimodular
Goal:
m : Type u_1
m' : Type u_2
n : Type u_3
R : Type u_5
inst : CommRing R
inst_1 : 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) (hf : Function.Injective f) (hg : Function.Injective g),
    Membership.mem (γ := Set R) (Set.range SignType.cast) ((A.fromRows B).submatrix f g).det
f : Fin (k + 1) → m ⊕ m'
g : Fin (k + 1) → n
hf : Function.Injective f
hg : Function.Injective g
hB : ∀ (i : m'), ∃ (j : n) (s : SignType), B i = Pi.single (M := fun (j : n) ↦ R) j (↑s : R)
i : Fin (k + 1)
j : m'
hfi : f i = Sum.inr j
s : SignType
x : Fin (k + 1)
hj' : B j = Pi.single (M := fun (j : n) ↦ R) (g x) (↑s : R)
hAB :
  ((A.fromRows B).submatrix f g).det =
    HPow.hPow (α := R) (-1) ((↑i : ℕ) + (↑x : ℕ)) * (↑s : R) *
      (((A.fromRows B).submatrix f g).submatrix i.succAbove x.succAbove).det
⊢ Membership.mem (γ := Submonoid R) (MonoidHom.mrange (F := SignType →* R) (↑SignType.castHom : SignType →* R))
    (HPow.hPow (α := R) (-1) ((↑i : ℕ) + (↑x : ℕ)) * (↑s : R) *
      (((A.fromRows B).submatrix f g).submatrix i.succAbove x.succAbove).det)

Tactic:
mul_mem (mul_mem ?_ (Set.mem_range_self s)) ?_

Premises used: Set.mem_range_self, MulMemClass.mul_mem
-- Module: Mathlib.LinearAlgebra.Matrix.Determinant.TotallyUnimodular
Goal:
m : Type u_1
m' : Type u_2
n : Type u_3
R : Type u_5
inst : CommRing R
inst_1 : 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) (hf : Function.Injective f) (hg : Function.Injective g),
    Membership.mem (γ := Set R) (Set.range SignType.cast) ((A.fromRows B).submatrix f g).det
f : Fin (k + 1) → m ⊕ m'
g : Fin (k + 1) → n
hf : Function.Injective f
hg : Function.Injective g
hB : ∀ (i : m'), ∃ (j : n) (s : SignType), B i = Pi.single (M := fun (j : n) ↦ R) j (↑s : R)
i : Fin (k + 1)
j : m'
hfi : f i = Sum.inr j
s : SignType
x : Fin (k + 1)
hj' : B j = Pi.single (M := fun (j : n) ↦ R) (g x) (↑s : R)
hAB :
  ((A.fromRows B).submatrix f g).det =
    HPow.hPow (α := R) (-1) ((↑i : ℕ) + (↑x : ℕ)) * (↑s : R) *
      (((A.fromRows B).submatrix f g).submatrix i.succAbove x.succAbove).det
pos :
  Membership.mem (γ := Submonoid R) (MonoidHom.mrange (F := SignType →* R) (↑SignType.castHom : SignType →* R))
    (HPow.hPow (α := R) (-1) ((↑i : ℕ) + (↑x : ℕ)))
pos₁ :
  Membership.mem (γ := Submonoid R) (MonoidHom.mrange (F := SignType →* R) (↑SignType.castHom : SignType →* R))
    (((A.fromRows B).submatrix f g).submatrix i.succAbove x.succAbove).det
⊢ Membership.mem (γ := Submonoid R) (MonoidHom.mrange (F := SignType →* R) (↑SignType.castHom : SignType →* R))
    (HPow.hPow (α := R) (-1) ((↑i : ℕ) + (↑x : ℕ)) * (↑s : R) *
      (((A.fromRows B).submatrix f g).submatrix i.succAbove x.succAbove).det)

Tactic:
refine mul_mem (mul_mem ?_ (Set.mem_range_self s)) ?_

Premises used: MulMemClass.mul_mem
-- Module: Mathlib.LinearAlgebra.Matrix.Determinant.TotallyUnimodular
Goal:
m : Type u_1
m' : Type u_2
n : Type u_3
R : Type u_5
inst : CommRing R
inst_1 : 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) (hf : Function.Injective f) (hg : Function.Injective g),
    Membership.mem (γ := Set R) (Set.range SignType.cast) ((A.fromRows B).submatrix f g).det
f : Fin (k + 1) → m ⊕ m'
g : Fin (k + 1) → n
hf : Function.Injective f
hg : Function.Injective g
hB : ∀ (i : m'), ∃ (j : n) (s : SignType), B i = Pi.single (M := fun (j : n) ↦ R) j (↑s : R)
i : Fin (k + 1)
j : m'
hfi : f i = Sum.inr j
s : SignType
x : Fin (k + 1)
hj' : B j = Pi.single (M := fun (j : n) ↦ R) (g x) (↑s : R)
hAB :
  ((A.fromRows B).submatrix f g).det =
    HPow.hPow (α := R) (-1) ((↑i : ℕ) + (↑x : ℕ)) * (↑s : R) *
      (((A.fromRows B).submatrix f g).submatrix i.succAbove x.succAbove).det
pos : Membership.mem (γ := Submonoid R) (MonoidHom.mrange (F := SignType →* R) (↑SignType.castHom : SignType →* R)) (-1)
⊢ Membership.mem (γ := Submonoid R) (MonoidHom.mrange (F := SignType →* R) (↑SignType.castHom : SignType →* R))
    (HPow.hPow (α := R) (-1) ((↑i : ℕ) + (↑x : ℕ)))

Tactic:
apply pow_mem

Premises used: pow_mem
-- Module: Mathlib.LinearAlgebra.Matrix.Determinant.TotallyUnimodular
Goal:
m : Type u_1
m' : Type u_2
n : Type u_3
R : Type u_5
inst : CommRing R
inst_1 : 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) (hf : Function.Injective f) (hg : Function.Injective g),
    Membership.mem (γ := Set R) (Set.range SignType.cast) ((A.fromRows B).submatrix f g).det
f : Fin (k + 1) → m ⊕ m'
g : Fin (k + 1) → n
hf : Function.Injective f
hg : Function.Injective g
hB : ∀ (i : m'), ∃ (j : n) (s : SignType), B i = Pi.single (M := fun (j : n) ↦ R) j (↑s : R)
i : Fin (k + 1)
j : m'
hfi : f i = Sum.inr j
s : SignType
x : Fin (k + 1)
hj' : B j = Pi.single (M := fun (j : n) ↦ R) (g x) (↑s : R)
hAB :
  ((A.fromRows B).submatrix f g).det =
    HPow.hPow (α := R) (-1) ((↑i : ℕ) + (↑x : ℕ)) * (↑s : R) *
      (((A.fromRows B).submatrix f g).submatrix i.succAbove x.succAbove).det
⊢ Eq.{u_5 + 1} (α := R) (((↑SignType.castHom : SignType →* R) : (a : SignType) → R) (-1) : R) (-1 : R)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Matrix.Determinant.TotallyUnimodular
Goal:
m : Type u_1
m' : Type u_2
n : Type u_3
R : Type u_5
inst : CommRing R
inst_1 : 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) (hf : Function.Injective f) (hg : Function.Injective g),
    Membership.mem (γ := Set R) (Set.range SignType.cast) ((A.fromRows B).submatrix f g).det
f : Fin (k + 1) → m ⊕ m'
g : Fin (k + 1) → n
hf : Function.Injective f
hg : Function.Injective g
hB : ∀ (i : m'), ∃ (j : n) (s : SignType), B i = Pi.single (M := fun (j : n) ↦ R) j (↑s : R)
i : Fin (k + 1)
j : m'
hfi : f i = Sum.inr j
s : SignType
x : Fin (k + 1)
hj' : B j = Pi.single (M := fun (j : n) ↦ R) (g x) (↑s : R)
hAB :
  ((A.fromRows B).submatrix f g).det =
    HPow.hPow (α := R) (-1) ((↑i : ℕ) + (↑x : ℕ)) * (↑s : R) *
      (((A.fromRows B).submatrix f g).submatrix i.succAbove x.succAbove).det
⊢ Membership.mem (γ := Submonoid R) (MonoidHom.mrange (F := SignType →* R) (↑SignType.castHom : SignType →* R)) (-1)

Tactic:
exact ⟨-1, by simp⟩
-- Module: Mathlib.LinearAlgebra.Matrix.Determinant.TotallyUnimodular
Goal:
m : Type u_1
m' : Type u_2
n : Type u_3
R : Type u_5
inst : CommRing R
inst_1 : 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) (hf : Function.Injective f) (hg : Function.Injective g),
    Membership.mem (γ := Set R) (Set.range SignType.cast) ((A.fromRows B).submatrix f g).det
f : Fin (k + 1) → m ⊕ m'
g : Fin (k + 1) → n
hf : Function.Injective f
hg : Function.Injective g
hB : ∀ (i : m'), ∃ (j : n) (s : SignType), B i = Pi.single (M := fun (j : n) ↦ R) j (↑s : R)
i : Fin (k + 1)
j : m'
hfi : f i = Sum.inr j
s : SignType
x : Fin (k + 1)
hj' : B j = Pi.single (M := fun (j : n) ↦ R) (g x) (↑s : R)
hAB :
  ((A.fromRows B).submatrix f g).det =
    HPow.hPow (α := R) (-1) ((↑i : ℕ) + (↑x : ℕ)) * (↑s : R) *
      (((A.fromRows B).submatrix f g).submatrix i.succAbove x.succAbove).det
⊢ Membership.mem (γ := Submonoid R) (MonoidHom.mrange (F := SignType →* R) (↑SignType.castHom : SignType →* R))
    (((A.fromRows B).submatrix f g).submatrix i.succAbove x.succAbove).det

Tactic:
ih _ _
                (hf.comp Fin.succAbove_right_injective)
                (hg.comp Fin.succAbove_right_injective)

Premises used: SignType.cast, Matrix.submatrix, Set.Mem, setOf, Fin.succAbove_right_injective, Function.Injective.comp, Matrix.fromRows, Set.range, Sum.elim
-- Module: Mathlib.LinearAlgebra.Matrix.Determinant.TotallyUnimodular
Goal:
m : Type u_1
m' : Type u_2
n : Type u_3
R : Type u_5
inst : CommRing R
inst_1 : 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) (hf : Function.Injective f) (hg : Function.Injective g),
    Membership.mem (γ := Set R) (Set.range SignType.cast) ((A.fromRows B).submatrix f g).det
f : Fin (k + 1) → m ⊕ m'
g : Fin (k + 1) → n
hf : Function.Injective f
hg : Function.Injective g
hB : ∀ (i : m'), ∃ (j : n) (s : SignType), B i = Pi.single (M := fun (j : n) ↦ R) j (↑s : R)
i : Fin (k + 1)
j : m'
hfi : f i = Sum.inr j
s : SignType
x : Fin (k + 1)
hj' : B j = Pi.single (M := fun (j : n) ↦ R) (g x) (↑s : R)
hAB :
  ((A.fromRows B).submatrix f g).det =
    HPow.hPow (α := R) (-1) ((↑i : ℕ) + (↑x : ℕ)) * (↑s : R) *
      (((A.fromRows B).submatrix f g).submatrix i.succAbove x.succAbove).det
⊢ Membership.mem (γ := Submonoid R) (MonoidHom.mrange (F := SignType →* R) (↑SignType.castHom : SignType →* R))
    (((A.fromRows B).submatrix f g).submatrix i.succAbove x.succAbove).det

Tactic:
exact ih _ _
                (hf.comp Fin.succAbove_right_injective)
                (hg.comp Fin.succAbove_right_injective)

Premises used: Fin.succAbove_right_injective, Function.Injective.comp
-- Module: Mathlib.LinearAlgebra.Matrix.Determinant.TotallyUnimodular
Goal:
m : Type u_1
m' : Type u_2
n : Type u_3
R : Type u_5
inst : CommRing R
inst_1 : 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) (hf : Function.Injective f) (hg : Function.Injective g),
    Membership.mem (γ := Set R) (Set.range SignType.cast) ((A.fromRows B).submatrix f g).det
f : Fin (k + 1) → m ⊕ m'
g : Fin (k + 1) → n
hf : Function.Injective f
hg : Function.Injective g
hB : ∀ (i : m'), ∃ (j : n) (s : SignType), B i = Pi.single (M := fun (j : n) ↦ R) j (↑s : R)
i : Fin (k + 1)
j : m'
hfi : f i = Sum.inr j
s : SignType
x : Fin (k + 1)
hj' : B j = Pi.single (M := fun (j : n) ↦ R) (g x) (↑s : R)
hAB :
  ((A.fromRows B).submatrix f g).det =
    ∑ x_1 : Fin k.succ,
      HMul.hMul (β := R) (HPow.hPow (α := R) (-1) ((↑i : ℕ) + (↑x_1 : ℕ)))
          (Pi.single (M := fun (j : n) ↦ R) (g x) (↑s : R) (g x_1) : R) *
        (((A.fromRows B).submatrix f g).submatrix i.succAbove x_1.succAbove).det
y : Fin (k + 1)
hxy : y ≠ x
⊢ HMul.hMul (β := R) (HPow.hPow (α := R) (-1) ((↑i : ℕ) + (↑y : ℕ)))
        (Pi.single (M := fun (j : n) ↦ R) (g x) (↑s : R) (g y) : R) *
      (((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]

Premises used: Iff.mpr, Pi.single_eq_of_ne, Function.Injective.ne_iff
-- Module: Mathlib.LinearAlgebra.Matrix.Determinant.TotallyUnimodular
Goal:
m : Type u_1
m' : Type u_2
n : Type u_3
R : Type u_5
inst : CommRing R
inst_1 : 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) (hf : Function.Injective f) (hg : Function.Injective g),
    Membership.mem (γ := Set R) (Set.range SignType.cast) ((A.fromRows B).submatrix f g).det
f : Fin (k + 1) → m ⊕ m'
g : Fin (k + 1) → n
hf : Function.Injective f
hg : Function.Injective g
hB : ∀ (i : m'), ∃ (j : n) (s : SignType), B i = Pi.single (M := fun (j : n) ↦ R) j (↑s : R)
i : Fin (k + 1)
j : m'
hfi : f i = Sum.inr j
j' : n
s : SignType
hj' : B j = Pi.single (M := fun (j : n) ↦ R) j' (↑s : R)
hAB :
  ((A.fromRows B).submatrix f g).det =
    ∑ x : Fin k.succ,
      HMul.hMul (β := R) (HPow.hPow (α := R) (-1) ((↑i : ℕ) + (↑x : ℕ)))
          (Pi.single (M := fun (j : n) ↦ R) j' (↑s : R) (g x) : R) *
        (((A.fromRows B).submatrix f g).submatrix i.succAbove x.succAbove).det
hj'' : ¬∃ (x : Fin (k + 1)), g x = j'
⊢ ∀ (x : Fin (k + 1)), ¬g x = j'

Tactic:
rw [not_exists] at hj''

Premises used: not_exists