awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Matrix.Determinant.Misc
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
M : Matrix (Fin (n + 1)) (Fin n) R
hv : Eq.{u_1 + 1} (α := Fin n → R) (∑ j : Fin (n + 1), M j) 0
j₁ j₂ j : Fin (n + 1)
zero : (M.submatrix (Fin.succAbove 0) id).det = Int.negOnePow (↑(↑0 : ℕ) : ℤ) • (M.submatrix (Fin.succAbove 0) id).det
succ :
  ∀ (i : Fin n)
    (h_ind :
      (M.submatrix i.castSucc.succAbove id).det =
        Int.negOnePow (↑(↑i.castSucc : ℕ) : ℤ) • (M.submatrix (Fin.succAbove 0) id).det),
    (M.submatrix i.succ.succAbove id).det = Int.negOnePow (↑(↑i.succ : ℕ) : ℤ) • (M.submatrix (Fin.succAbove 0) id).det
⊢ (M.submatrix j.succAbove id).det = Int.negOnePow (↑(↑j : ℕ) : ℤ) • (M.submatrix (Fin.succAbove 0) id).det

Tactic:
induction j using Fin.induction with
  | zero => rw [Fin.val_zero, Nat.cast_zero, Int.negOnePow_zero, one_smul]
  | succ i h_ind =>
      rw [Fin.val_succ, Nat.cast_add, Nat.cast_one, Int.negOnePow_succ, Units.neg_smul,
        ← neg_eq_iff_eq_neg, ← neg_one_smul R,
        ← det_updateRow_sum (M.submatrix i.succ.succAbove id) i (fun _ ↦ -1),
        ← Fin.val_castSucc i, ← h_ind]
      congr
      ext a b
      simp_rw [neg_one_smul, updateRow_apply, Finset.sum_neg_distrib, Pi.neg_apply,
        Finset.sum_apply, submatrix_apply, id_eq]
      split_ifs with h
      · replace hv := congr_fun hv b
        rw [Fin.sum_univ_succAbove _ i.succ, Pi.add_apply, Finset.sum_apply] at hv
        rwa [h, Fin.succAbove_castSucc_self, neg_eq_iff_add_eq_zero, add_comm]
      · obtain h | h := ne_iff_lt_or_gt.mp h
        · rw [Fin.succAbove_castSucc_of_lt _ _ h,
            Fin.succAbove_of_succ_le _ _ (Fin.succ_lt_succ_iff.mpr h).le]
        · rw [Fin.succAbove_succ_of_lt _ _ h, Fin.succAbove_castSucc_of_le _ _ h.le]

Premises used: neg_eq_iff_add_eq_zero, neg_one_smul, Fin.succAbove_castSucc_self, Finset.sum_apply, neg_eq_iff_eq_neg, Fin.val_succ, add_comm, one_smul, Pi.add_apply, Nat.cast_add, Units.neg_smul, Int.negOnePow_zero, Matrix.submatrix_apply, Nat.cast_zero, Finset.sum_neg_distrib, Pi.neg_apply, Matrix.zero, Fin.val_zero, Nat.cast_one, Int.negOnePow_succ, Matrix.updateRow_apply, id_eq
-- Module: Mathlib.LinearAlgebra.Matrix.Determinant.Misc
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
M : Matrix (Fin n) (Fin (n + 1)) R
hv : ∀ (i : Fin n), Eq.{u_1 + 1} (α := R) (∑ j : Fin (n + 1), M i j) 0
j₁ j₂ : Fin (n + 1)
rw : Eq.{u_1 + 1} (α := Fin n → R) (∑ j : Fin (n + 1), Mᵀ j) 0
⊢ (M.submatrix id j₁.succAbove).det =
    (HSub.hSub (α := ℤ) (↑(↑j₁ : ℕ) : ℤ) (↑(↑j₂ : ℕ) : ℤ)).negOnePow • (M.submatrix id j₂.succAbove).det

Tactic:
rw [← det_transpose, transpose_submatrix,
    submatrix_succAbove_det_eq_negOnePow_submatrix_succAbove_det M.transpose ?_ j₁ j₂,
    ← det_transpose, transpose_submatrix, transpose_transpose]

Premises used: Matrix.det_transpose, Matrix.transpose_submatrix, Matrix.transpose_transpose, Matrix.transpose, Matrix.submatrix_succAbove_det_eq_negOnePow_submatrix_succAbove_det
-- Module: Mathlib.LinearAlgebra.Matrix.Determinant.Misc
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
M : Matrix (Fin n) (Fin (n + 1)) R
hv : ∀ (i : Fin n), Eq.{u_1 + 1} (α := R) (∑ j : Fin (n + 1), M i j) 0
j₁ j₂ : Fin (n + 1)
h : ∀ (x : Fin n), Eq.{u_1 + 1} (α := R) ((∑ j : Fin (n + 1), Mᵀ j) x) (0 x)
⊢ Eq.{u_1 + 1} (α := Fin n → R) (∑ j : Fin (n + 1), Mᵀ j) 0

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.Matrix.Determinant.Misc
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
M : Matrix (Fin n) (Fin (n + 1)) R
hv : ∀ (i : Fin n), Eq.{u_1 + 1} (α := R) (∑ j : Fin (n + 1), M i j) 0
j₁ j₂ : Fin (n + 1)
x : Fin n
h : Eq.{u_1 + 1} (α := R) (∑ c : Fin (n + 1), Mᵀ c x) (0 x)
h₁ : Eq.{u_1 + 1} (α := R) (∑ x_1 : Fin (n + 1), M x x_1) (0 x)
h₂ : Eq.{u_1 + 1} (α := R) 0 (0 x)
⊢ Eq.{u_1 + 1} (α := R) ((∑ j : Fin (n + 1), Mᵀ j) x) (0 x)

Tactic:
simp_rw [Finset.sum_apply, transpose_apply, hv, Pi.zero_apply]

Premises used: Finset.sum_apply, Pi.zero_apply, Matrix.transpose_apply
-- Module: Mathlib.LinearAlgebra.Matrix.Determinant.Misc
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
M : Matrix (Fin (n + 1)) (Fin (n + 1)) R
i₀ j₀ : Fin (n + 1)
hv : ∀ (j : Fin (n + 1)), j ≠ j₀ → Eq.{u_1 + 1} (α := R) (∑ i : Fin (n + 1), M i j) 0
rw :
  ∑ j : Fin n.succ,
      HPow.hPow (α := R) (-1) ((↑i₀ : ℕ) + (↑j : ℕ)) *
          M.updateRow i₀ (∑ k : Fin (n + 1), HSMul.hSMul (α := R) 1 (M k)) i₀ j *
        ((M.updateRow i₀ (∑ k : Fin (n + 1), HSMul.hSMul (α := R) 1 (M k))).submatrix i₀.succAbove j.succAbove).det =
    (HPow.hPow (α := R) (-1) ((↑i₀ : ℕ) + (↑j₀ : ℕ)) * ∑ i : Fin (n + 1), M i j₀) *
      (M.submatrix i₀.succAbove j₀.succAbove).det
⊢ M.det =
    (HPow.hPow (α := R) (-1) ((↑i₀ : ℕ) + (↑j₀ : ℕ)) * ∑ i : Fin (n + 1), M i j₀) *
      (M.submatrix i₀.succAbove j₀.succAbove).det

Tactic:
rw [← one_smul R M.det, ← Matrix.det_updateRow_sum _ i₀ (fun _ ↦ 1), Matrix.det_succ_row _ i₀]

Premises used: Matrix.det_succ_row, Matrix.det_updateRow_sum, one_smul, OfNat.ofNat, Matrix.det
-- Module: Mathlib.LinearAlgebra.Matrix.Determinant.Misc
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
M : Matrix (Fin (n + 1)) (Fin (n + 1)) R
i₀ j₀ : Fin (n + 1)
hv : ∀ (j : Fin (n + 1)), j ≠ j₀ → Eq.{u_1 + 1} (α := R) (∑ i : Fin (n + 1), M i j) 0
simp :
  ∑ x : Fin n.succ,
      (HPow.hPow (α := R) (-1) ((↑i₀ : ℕ) + (↑x : ℕ)) * ∑ c : Fin (n + 1), M c x) *
        (M.submatrix i₀.succAbove x.succAbove).det =
    (HPow.hPow (α := R) (-1) ((↑i₀ : ℕ) + (↑j₀ : ℕ)) * ∑ i : Fin (n + 1), M i j₀) *
      (M.submatrix i₀.succAbove j₀.succAbove).det
⊢ ∑ j : Fin n.succ,
      HPow.hPow (α := R) (-1) ((↑i₀ : ℕ) + (↑j : ℕ)) *
          M.updateRow i₀ (∑ k : Fin (n + 1), HSMul.hSMul (α := R) 1 (M k)) i₀ j *
        ((M.updateRow i₀ (∑ k : Fin (n + 1), HSMul.hSMul (α := R) 1 (M k))).submatrix i₀.succAbove j.succAbove).det =
    (HPow.hPow (α := R) (-1) ((↑i₀ : ℕ) + (↑j₀ : ℕ)) * ∑ i : Fin (n + 1), M i j₀) *
      (M.submatrix i₀.succAbove j₀.succAbove).det

Tactic:
simp only [updateRow_apply, if_true, one_smul, submatrix_updateRow_succAbove, Finset.sum_apply]

Premises used: if_true, Finset.sum_apply, Matrix.submatrix_updateRow_succAbove, one_smul, Matrix.updateRow_apply
-- Module: Mathlib.LinearAlgebra.Matrix.Determinant.Misc
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
M : Matrix (Fin (n + 1)) (Fin (n + 1)) R
i₀ j₀ : Fin (n + 1)
hv : ∀ (j : Fin (n + 1)), j ≠ j₀ → Eq.{u_1 + 1} (α := R) (∑ i : Fin (n + 1), M i j) 0
rw :
  (HPow.hPow (α := R) (-1) ((↑i₀ : ℕ) + (↑j₀ : ℕ)) * ∑ c : Fin (n + 1), M c j₀) *
        (M.submatrix i₀.succAbove j₀.succAbove).det +
      ∑ i : { i : Fin (n + 1) // i ≠ j₀ },
        (HPow.hPow (α := R) (-1) ((↑i₀ : ℕ) + (↑(↑i : Fin (n + 1)) : ℕ)) * ∑ c : Fin (n + 1), M c (↑i : Fin (n + 1))) *
          (M.submatrix i₀.succAbove (↑i : Fin (n + 1)).succAbove).det =
    (HPow.hPow (α := R) (-1) ((↑i₀ : ℕ) + (↑j₀ : ℕ)) * ∑ i : Fin (n + 1), M i j₀) *
      (M.submatrix i₀.succAbove j₀.succAbove).det
⊢ ∑ x : Fin n.succ,
      (HPow.hPow (α := R) (-1) ((↑i₀ : ℕ) + (↑x : ℕ)) * ∑ c : Fin (n + 1), M c x) *
        (M.submatrix i₀.succAbove x.succAbove).det =
    (HPow.hPow (α := R) (-1) ((↑i₀ : ℕ) + (↑j₀ : ℕ)) * ∑ i : Fin (n + 1), M i j₀) *
      (M.submatrix i₀.succAbove j₀.succAbove).det

Tactic:
rw [Fintype.sum_eq_add_sum_subtype_ne _ j₀]

Premises used: Fintype.sum_eq_add_sum_subtype_ne
-- Module: Mathlib.LinearAlgebra.Matrix.Determinant.Misc
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
M : Matrix (Fin (n + 1)) (Fin (n + 1)) R
i₀ j₀ : Fin (n + 1)
hv : ∀ (j : Fin (n + 1)), j ≠ j₀ → Eq.{u_1 + 1} (α := R) (∑ i : Fin (n + 1), M i j) 0
h :
  ∀ (i : { i : Fin (n + 1) // i ≠ j₀ }),
    (HPow.hPow (α := R) (-1) ((↑i₀ : ℕ) + (↑(↑i : Fin (n + 1)) : ℕ)) * ∑ c : Fin (n + 1), M c (↑i : Fin (n + 1))) *
      (M.submatrix i₀.succAbove (↑i : Fin (n + 1)).succAbove).det
| (HPow.hPow (α := R) (-1) ((↑i₀ : ℕ) + (↑j₀ : ℕ)) * ∑ c : Fin (n + 1), M c j₀) *
      (M.submatrix i₀.succAbove j₀.succAbove).det +
    ∑ i : { i : Fin (n + 1) // i ≠ j₀ },
      (HPow.hPow (α := R) (-1) ((↑i₀ : ℕ) + (↑(↑i : Fin (n + 1)) : ℕ)) * ∑ c : Fin (n + 1), M c (↑i : Fin (n + 1))) *
        (M.submatrix i₀.succAbove (↑i : Fin (n + 1)).succAbove).det

Tactic:
enter [2, 2, i]
-- Module: Mathlib.LinearAlgebra.Matrix.Determinant.Misc
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
M : Matrix (Fin (n + 1)) (Fin (n + 1)) R
i₀ j₀ : Fin (n + 1)
hv : ∀ (j : Fin (n + 1)), j ≠ j₀ → Eq.{u_1 + 1} (α := R) (∑ i : Fin (n + 1), M i j) 0
i : { i : Fin (n + 1) // i ≠ j₀ }
h : 0
| (HPow.hPow (α := R) (-1) ((↑i₀ : ℕ) + (↑(↑i : Fin (n + 1)) : ℕ)) * ∑ c : Fin (n + 1), M c (↑i : Fin (n + 1))) *
    (M.submatrix i₀.succAbove (↑i : Fin (n + 1)).succAbove).det

Tactic:
rw [hv _ i.prop, mul_zero, zero_mul]

Premises used: MulZeroClass.zero_mul, MulZeroClass.mul_zero, Subtype.prop
-- Module: Mathlib.LinearAlgebra.Matrix.Determinant.Misc
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
M : Matrix (Fin (n + 1)) (Fin (n + 1)) R
i₀ j₀ : Fin (n + 1)
hv : ∀ (j : Fin (n + 1)), j ≠ j₀ → Eq.{u_1 + 1} (α := R) (∑ i : Fin (n + 1), M i j) 0
h : ∀ (i : { i : Fin (n + 1) // i ≠ j₀ }), 0
| (HPow.hPow (α := R) (-1) ((↑i₀ : ℕ) + (↑j₀ : ℕ)) * ∑ c : Fin (n + 1), M c j₀) *
      (M.submatrix i₀.succAbove j₀.succAbove).det +
    ∑ i : { i : Fin (n + 1) // i ≠ j₀ },
      (HPow.hPow (α := R) (-1) ((↑i₀ : ℕ) + (↑(↑i : Fin (n + 1)) : ℕ)) * ∑ c : Fin (n + 1), M c (↑i : Fin (n + 1))) *
        (M.submatrix i₀.succAbove (↑i : Fin (n + 1)).succAbove).det

Tactic:
enter [2, 2, i]
    rw [hv _ i.prop, mul_zero, zero_mul]

Premises used: MulZeroClass.zero_mul, MulZeroClass.mul_zero
-- Module: Mathlib.LinearAlgebra.Matrix.Determinant.Misc
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
M : Matrix (Fin (n + 1)) (Fin (n + 1)) R
i₀ j₀ : Fin (n + 1)
hv : ∀ (j : Fin (n + 1)), j ≠ j₀ → Eq.{u_1 + 1} (α := R) (∑ i : Fin (n + 1), M i j) 0
conv_lhs :
  (HPow.hPow (α := R) (-1) ((↑i₀ : ℕ) + (↑j₀ : ℕ)) * ∑ c : Fin (n + 1), M c j₀) *
        (M.submatrix i₀.succAbove j₀.succAbove).det +
      ∑ i : { i : Fin (n + 1) // i ≠ j₀ }, 0 =
    (HPow.hPow (α := R) (-1) ((↑i₀ : ℕ) + (↑j₀ : ℕ)) * ∑ i : Fin (n + 1), M i j₀) *
      (M.submatrix i₀.succAbove j₀.succAbove).det
⊢ (HPow.hPow (α := R) (-1) ((↑i₀ : ℕ) + (↑j₀ : ℕ)) * ∑ c : Fin (n + 1), M c j₀) *
        (M.submatrix i₀.succAbove j₀.succAbove).det +
      ∑ i : { i : Fin (n + 1) // i ≠ j₀ },
        (HPow.hPow (α := R) (-1) ((↑i₀ : ℕ) + (↑(↑i : Fin (n + 1)) : ℕ)) * ∑ c : Fin (n + 1), M c (↑i : Fin (n + 1))) *
          (M.submatrix i₀.succAbove (↑i : Fin (n + 1)).succAbove).det =
    (HPow.hPow (α := R) (-1) ((↑i₀ : ℕ) + (↑j₀ : ℕ)) * ∑ i : Fin (n + 1), M i j₀) *
      (M.submatrix i₀.succAbove j₀.succAbove).det

Tactic:
conv_lhs =>
    enter [2, 2, i]
    rw [hv _ i.prop, mul_zero, zero_mul]

Premises used: MulZeroClass.zero_mul, MulZeroClass.mul_zero
-- Module: Mathlib.LinearAlgebra.Matrix.Determinant.Misc
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
M : Matrix (Fin (n + 1)) (Fin (n + 1)) R
i₀ j₀ : Fin (n + 1)
hv : ∀ (j : Fin (n + 1)), j ≠ j₀ → Eq.{u_1 + 1} (α := R) (∑ i : Fin (n + 1), M i j) 0
⊢ (HPow.hPow (α := R) (-1) ((↑i₀ : ℕ) + (↑j₀ : ℕ)) * ∑ c : Fin (n + 1), M c j₀) *
        (M.submatrix i₀.succAbove j₀.succAbove).det +
      ∑ i : { i : Fin (n + 1) // i ≠ j₀ }, 0 =
    (HPow.hPow (α := R) (-1) ((↑i₀ : ℕ) + (↑j₀ : ℕ)) * ∑ i : Fin (n + 1), M i j₀) *
      (M.submatrix i₀.succAbove j₀.succAbove).det

Tactic:
simp [Finset.sum_const_zero, add_zero]

Premises used: Finset.sum_const_zero, add_zero
-- Module: Mathlib.LinearAlgebra.Matrix.Determinant.Misc
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
M : Matrix (Fin (n + 1)) (Fin (n + 1)) R
i₀ j₀ : Fin (n + 1)
hv : ∀ (i : Fin (n + 1)), i ≠ i₀ → Eq.{u_1 + 1} (α := R) (∑ j : Fin (n + 1), M i j) 0
⊢ ∀ (j : Fin (n + 1)), j ≠ i₀ → Eq.{u_1 + 1} (α := R) (∑ i : Fin (n + 1), Mᵀ i j) 0

Tactic:
simpa using hv
-- Module: Mathlib.LinearAlgebra.Matrix.Determinant.Misc
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
M : Matrix (Fin (n + 1)) (Fin (n + 1)) R
i₀ j₀ : Fin (n + 1)
hv : ∀ (i : Fin (n + 1)), i ≠ i₀ → Eq.{u_1 + 1} (α := R) (∑ j : Fin (n + 1), M i j) 0
rw :
  (HPow.hPow (α := R) (-1) ((↑i₀ : ℕ) + (↑j₀ : ℕ)) * ∑ i : Fin (n + 1), Mᵀ i i₀) *
      (M.submatrix i₀.succAbove j₀.succAbove).det =
    (HPow.hPow (α := R) (-1) ((↑i₀ : ℕ) + (↑j₀ : ℕ)) * ∑ j : Fin (n + 1), M i₀ j) *
      (M.submatrix i₀.succAbove j₀.succAbove).det
⊢ M.det =
    (HPow.hPow (α := R) (-1) ((↑i₀ : ℕ) + (↑j₀ : ℕ)) * ∑ j : Fin (n + 1), M i₀ j) *
      (M.submatrix i₀.succAbove j₀.succAbove).det

Tactic:
rw [← det_transpose, det_eq_sum_column_mul_submatrix_succAbove_succAbove_det _ j₀ i₀
    (by simpa using hv), ← det_transpose, transpose_submatrix, transpose_transpose, add_comm]

Premises used: Matrix.det_transpose, Matrix.transpose_submatrix, Matrix.transpose_transpose, Matrix.det_eq_sum_column_mul_submatrix_succAbove_succAbove_det, add_comm
-- Module: Mathlib.LinearAlgebra.Matrix.Determinant.Misc
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
M : Matrix (Fin (n + 1)) (Fin (n + 1)) R
i₀ j₀ : Fin (n + 1)
hv : ∀ (i : Fin (n + 1)), i ≠ i₀ → Eq.{u_1 + 1} (α := R) (∑ j : Fin (n + 1), M i j) 0
⊢ (HPow.hPow (α := R) (-1) ((↑i₀ : ℕ) + (↑j₀ : ℕ)) * ∑ i : Fin (n + 1), Mᵀ i i₀) *
      (M.submatrix i₀.succAbove j₀.succAbove).det =
    (HPow.hPow (α := R) (-1) ((↑i₀ : ℕ) + (↑j₀ : ℕ)) * ∑ j : Fin (n + 1), M i₀ j) *
      (M.submatrix i₀.succAbove j₀.succAbove).det

Tactic:
simp_rw [transpose_apply]

Premises used: Matrix.transpose_apply
-- Module: Mathlib.LinearAlgebra.Matrix.Determinant.TotallyUnimodular
Goal:
m : Type u_1
n : Type u_3
R : Type u_5
inst : CommRing R
A : Matrix m n R
mp :
  A.IsTotallyUnimodular →
    ∀ (k : ℕ) (f : Fin k → m) (g : Fin k → n),
      Membership.mem (γ := Set R) (Set.range SignType.cast) (A.submatrix f g).det
mpr :
  (∀ (k : ℕ) (f : Fin k → m) (g : Fin k → n),
      Membership.mem (γ := Set R) (Set.range SignType.cast) (A.submatrix f g).det) →
    A.IsTotallyUnimodular
⊢ A.IsTotallyUnimodular ↔
    ∀ (k : ℕ) (f : Fin k → m) (g : Fin k → n),
      Membership.mem (γ := Set R) (Set.range SignType.cast) (A.submatrix f g).det

Tactic:
constructor
-- Module: Mathlib.LinearAlgebra.Matrix.Determinant.TotallyUnimodular
Goal:
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
pos :
  ∀ (hfg : Function.Injective f ∧ Function.Injective g),
    Membership.mem (γ := Set R) (Set.range SignType.cast) (A.submatrix f g).det
neg :
  ∀ (hfg : ¬(Function.Injective f ∧ Function.Injective g)),
    Membership.mem (γ := Set R) (Set.range SignType.cast) (A.submatrix f g).det
⊢ Membership.mem (γ := Set R) (Set.range SignType.cast) (A.submatrix f g).det

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

Premises used: Function.Injective
-- Module: Mathlib.LinearAlgebra.Matrix.Determinant.TotallyUnimodular
Goal:
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
⊢ Membership.mem (γ := Set R) (Set.range SignType.cast) (A.submatrix f g).det

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

Premises used: And.right, And.left
-- Module: Mathlib.LinearAlgebra.Matrix.Determinant.TotallyUnimodular
Goal:
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
⊢ Membership.mem (γ := Set R) (Set.range SignType.cast) (A.submatrix f g).det

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

Premises used: And.right, And.left
-- Module: Mathlib.LinearAlgebra.Matrix.Determinant.TotallyUnimodular
Goal:
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)
h : (↑0 : R) = (A.submatrix f g).det
⊢ Membership.mem (γ := Set R) (Set.range SignType.cast) (A.submatrix f g).det

Tactic:
use 0
-- Module: Mathlib.LinearAlgebra.Matrix.Determinant.TotallyUnimodular
Goal:
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)
h : (A.submatrix f g).det = 0
⊢ (↑0 : R) = (A.submatrix f g).det

Tactic:
rw [SignType.coe_zero, eq_comm]

Premises used: SignType.coe_zero, eq_comm
-- Module: Mathlib.LinearAlgebra.Matrix.Determinant.TotallyUnimodular
Goal:
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 : Fin k) (b : Fin k), f a = f b ∧ a ≠ b) ∨ ∃ (a : Fin k) (b : Fin k), g a = g b ∧ a ≠ b

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

Premises used: not_and_or, Function.not_injective_iff
-- Module: Mathlib.LinearAlgebra.Matrix.Determinant.TotallyUnimodular
Goal:
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 : Fin k) (b : Fin k), f a = f b ∧ a ≠ b) ∨ ∃ (a : Fin k) (b : Fin k), g a = g b ∧ a ≠ b
h : ∀ (i j : Fin k) (hfij : f i = f j) (hij : i ≠ j), (A.submatrix f g).det = 0
h₁ : ∀ (i j : Fin k) (hgij : g i = g j) (hij : i ≠ j), (A.submatrix f g).det = 0
⊢ (A.submatrix f g).det = 0

Tactic:
obtain ⟨i, j, hfij, hij⟩ | ⟨i, j, hgij, hij⟩ := hfg
-- Module: Mathlib.LinearAlgebra.Matrix.Determinant.TotallyUnimodular
Goal:
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
h : (Aᵀ.submatrix g f).det = 0
⊢ (A.submatrix f g).det = 0

Tactic:
rw [← det_transpose, transpose_submatrix]

Premises used: Matrix.det_transpose, Matrix.transpose_submatrix
-- Module: Mathlib.LinearAlgebra.Matrix.Determinant.TotallyUnimodular
Goal:
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
h : ∀ (k_1 : Fin k), Aᵀ.submatrix g f k_1 j = Aᵀ.submatrix g f k_1 i
⊢ (Aᵀ.submatrix g f).det = 0

Tactic:
apply det_zero_of_column_eq hij.symm

Premises used: Matrix.det_zero_of_column_eq, Ne.symm
-- Module: Mathlib.LinearAlgebra.Matrix.Determinant.TotallyUnimodular
Goal:
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]
-- Module: Mathlib.LinearAlgebra.Matrix.Determinant.TotallyUnimodular
Goal:
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
h : ∀ (k_1 : Fin k), A.submatrix f g k_1 i = A.submatrix f g k_1 j
⊢ (A.submatrix f g).det = 0

Tactic:
apply det_zero_of_column_eq hij

Premises used: Matrix.det_zero_of_column_eq
-- Module: Mathlib.LinearAlgebra.Matrix.Determinant.TotallyUnimodular
Goal:
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]
-- Module: Mathlib.LinearAlgebra.Matrix.Determinant.TotallyUnimodular
Goal:
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), Membership.mem (γ := Set R) (Set.range SignType.cast) (A.submatrix f g).det
k : ℕ
mpr :
  ∀ (f : Fin k → m) (g : Fin k → n),
    Function.Injective f →
      Function.Injective g → Membership.mem (γ := Set R) (Set.range SignType.cast) (A.submatrix f g).det
⊢ ∀ (f : Fin k → m) (g : Fin k → n),
    Function.Injective f →
      Function.Injective g → Membership.mem (γ := Set R) (Set.range SignType.cast) (A.submatrix f g).det

Tactic:
_
-- Module: Mathlib.LinearAlgebra.Matrix.Determinant.TotallyUnimodular
Goal:
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), Membership.mem (γ := Set R) (Set.range SignType.cast) (A.submatrix f g).det
k : ℕ
f : Fin k → m
mpr :
  ∀ (g : Fin k → n),
    Function.Injective f →
      Function.Injective g → Membership.mem (γ := Set R) (Set.range SignType.cast) (A.submatrix f g).det
⊢ ∀ (g : Fin k → n),
    Function.Injective f →
      Function.Injective g → Membership.mem (γ := Set R) (Set.range SignType.cast) (A.submatrix f g).det

Tactic:
_
-- Module: Mathlib.LinearAlgebra.Matrix.Determinant.TotallyUnimodular
Goal:
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), Membership.mem (γ := Set R) (Set.range SignType.cast) (A.submatrix f g).det
k : ℕ
f : Fin k → m
g : Fin k → n
mpr :
  Function.Injective f →
    Function.Injective g → Membership.mem (γ := Set R) (Set.range SignType.cast) (A.submatrix f g).det
⊢ Function.Injective f →
    Function.Injective g → Membership.mem (γ := Set R) (Set.range SignType.cast) (A.submatrix f g).det

Tactic:
_
-- Module: Mathlib.LinearAlgebra.Matrix.Determinant.TotallyUnimodular
Goal:
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), Membership.mem (γ := Set R) (Set.range SignType.cast) (A.submatrix f g).det
k : ℕ
f : Fin k → m
g : Fin k → n
h : Function.Injective f
mpr : Function.Injective g → Membership.mem (γ := Set R) (Set.range SignType.cast) (A.submatrix f g).det
⊢ Function.Injective g → Membership.mem (γ := Set R) (Set.range SignType.cast) (A.submatrix f g).det

Tactic:
_
-- Module: Mathlib.LinearAlgebra.Matrix.Determinant.TotallyUnimodular
Goal:
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), Membership.mem (γ := Set R) (Set.range SignType.cast) (A.submatrix f g).det
k : ℕ
f : Fin k → m
g : Fin k → n
h : Function.Injective f
h_1 : Function.Injective g
⊢ Membership.mem (γ := Set R) (Set.range SignType.cast) (A.submatrix f g).det

Tactic:
apply hA
-- Module: Mathlib.LinearAlgebra.Matrix.Determinant.TotallyUnimodular
Goal:
m : Type u_1
n : Type u_3
R : Type u_5
inst : CommRing R
A : Matrix m n R
rw :
  (∀ (k : ℕ) (f : Fin k → m) (g : Fin k → n),
      Membership.mem (γ := Set R) (Set.range SignType.cast) (A.submatrix f g).det) ↔
    ∀ (ι : Type w) [inst_1 : Fintype ι] [inst_2 : DecidableEq ι] (f : ι → m) (g : ι → n),
      Membership.mem (γ := Set R) (Set.range SignType.cast) (A.submatrix f g).det
⊢ A.IsTotallyUnimodular ↔
    ∀ (ι : Type w) [inst_1 : Fintype ι] [inst_2 : DecidableEq ι] (f : ι → m) (g : ι → n),
      Membership.mem (γ := Set R) (Set.range SignType.cast) (A.submatrix f g).det

Tactic:
rw [isTotallyUnimodular_iff]

Premises used: Matrix.isTotallyUnimodular_iff
-- Module: Mathlib.LinearAlgebra.Matrix.Determinant.TotallyUnimodular
Goal:
m : Type u_1
n : Type u_3
R : Type u_5
inst : CommRing R
A : Matrix m n R
mp :
  (∀ (k : ℕ) (f : Fin k → m) (g : Fin k → n),
      Membership.mem (γ := Set R) (Set.range SignType.cast) (A.submatrix f g).det) →
    ∀ (ι : Type w) [inst_1 : Fintype ι] [inst_2 : DecidableEq ι] (f : ι → m) (g : ι → n),
      Membership.mem (γ := Set R) (Set.range SignType.cast) (A.submatrix f g).det
mpr :
  (∀ (ι : Type w) [inst_1 : Fintype ι] [inst_2 : DecidableEq ι] (f : ι → m) (g : ι → n),
      Membership.mem (γ := Set R) (Set.range SignType.cast) (A.submatrix f g).det) →
    ∀ (k : ℕ) (f : Fin k → m) (g : Fin k → n),
      Membership.mem (γ := Set R) (Set.range SignType.cast) (A.submatrix f g).det
⊢ (∀ (k : ℕ) (f : Fin k → m) (g : Fin k → n),
      Membership.mem (γ := Set R) (Set.range SignType.cast) (A.submatrix f g).det) ↔
    ∀ (ι : Type w) [inst_1 : Fintype ι] [inst_2 : DecidableEq ι] (f : ι → m) (g : ι → n),
      Membership.mem (γ := Set R) (Set.range SignType.cast) (A.submatrix f g).det

Tactic:
constructor