awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.Misc (goal)
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
⊢ (M.submatrix j.succAbove id).det = Int.negOnePow (↑(↑j : ℕ) : ℤ) • (M.submatrix (Fin.succAbove 0) id).det
have 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
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]
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.Misc (goal)
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)
⊢ (M.submatrix id j₁.succAbove).det =
    (HSub.hSub (α := ℤ) (↑(↑j₁ : ℕ) : ℤ) (↑(↑j₂ : ℕ) : ℤ)).negOnePow • (M.submatrix id j₂.succAbove).det
have rw : Eq.{u_1 + 1} (α := Fin n → R) (∑ j : Fin (n + 1), Mᵀ j) 0
Tactic: rw [← det_transpose, transpose_submatrix,
    submatrix_succAbove_det_eq_negOnePow_submatrix_succAbove_det M.transpose ?_ j₁ j₂,
    ← det_transpose, transpose_submatrix, transpose_transpose]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.Misc (goal)
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)
⊢ Eq.{u_1 + 1} (α := Fin n → R) (∑ j : Fin (n + 1), Mᵀ j) 0
have h : ∀ (x : Fin n), Eq.{u_1 + 1} (α := R) ((∑ j : Fin (n + 1), Mᵀ j) x) (0 x)
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.Misc (goal)
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
⊢ Eq.{u_1 + 1} (α := R) ((∑ j : Fin (n + 1), Mᵀ j) x) (0 x)
have h : Eq.{u_1 + 1} (α := R) (∑ c : Fin (n + 1), Mᵀ c x) (0 x)
Tactic: simp_rw [Finset.sum_apply, transpose_apply, hv, Pi.zero_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.Misc (goal)
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)
⊢ Eq.{u_1 + 1} (α := R) ((∑ j : Fin (n + 1), Mᵀ j) x) (0 x)
have h₁ : Eq.{u_1 + 1} (α := R) (∑ x_1 : Fin (n + 1), M x x_1) (0 x)
Tactic: simp_rw [Finset.sum_apply, transpose_apply, hv, Pi.zero_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.Misc (goal)
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)
⊢ Eq.{u_1 + 1} (α := R) ((∑ j : Fin (n + 1), Mᵀ j) x) (0 x)
have h₂ : Eq.{u_1 + 1} (α := R) 0 (0 x)
Tactic: simp_rw [Finset.sum_apply, transpose_apply, hv, Pi.zero_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.Misc (goal)
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
⊢ M.det =
    (HPow.hPow (α := R) (-1) ((↑i₀ : ℕ) + (↑j₀ : ℕ)) * ∑ i : Fin (n + 1), M i j₀) *
      (M.submatrix i₀.succAbove j₀.succAbove).det
have 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
Tactic: rw [← one_smul R M.det, ← Matrix.det_updateRow_sum _ i₀ (fun _ ↦ 1), Matrix.det_succ_row _ i₀]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.Misc (goal)
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
⊢ ∑ 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
have 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
Tactic: simp only [updateRow_apply, if_true, one_smul, submatrix_updateRow_succAbove, Finset.sum_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.Misc (goal)
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
⊢ ∑ 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
have 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
Tactic: rw [Fintype.sum_eq_add_sum_subtype_ne _ j₀]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.Misc (goal)
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₀ },
      (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
have 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
Tactic: enter [2, 2, i]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.Misc (goal)
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₀ }
| (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
have h : 0
Tactic: rw [hv _ i.prop, mul_zero, zero_mul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.Misc (goal)
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₀ },
      (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
have h : ∀ (i : { i : Fin (n + 1) // i ≠ j₀ }), 0
Tactic: enter [2, 2, i]
    rw [hv _ i.prop, mul_zero, zero_mul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.Misc (goal)
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₀ },
        (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
have 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
Tactic: conv_lhs =>
    enter [2, 2, i]
    rw [hv _ i.prop, mul_zero, zero_mul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.Misc (goal)
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
⊢ M.det =
    (HPow.hPow (α := R) (-1) ((↑i₀ : ℕ) + (↑j₀ : ℕ)) * ∑ j : Fin (n + 1), M i₀ j) *
      (M.submatrix i₀.succAbove j₀.succAbove).det
have 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
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]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.TotallyUnimodular (goal)
Goal:
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),
      Membership.mem (γ := Set R) (Set.range SignType.cast) (A.submatrix f g).det
have 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
Tactic: constructor
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.TotallyUnimodular (goal)
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
⊢ A.IsTotallyUnimodular ↔
    ∀ (k : ℕ) (f : Fin k → m) (g : Fin k → n),
      Membership.mem (γ := Set R) (Set.range SignType.cast) (A.submatrix f g).det
have 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
Tactic: constructor
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.TotallyUnimodular (goal)
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
⊢ Membership.mem (γ := Set R) (Set.range SignType.cast) (A.submatrix f g).det
have pos : ∀ (hfg : Function.Injective f ∧ Function.Injective g),
  Membership.mem (γ := Set R) (Set.range SignType.cast) (A.submatrix f g).det
Tactic: by_cases hfg : f.Injective ∧ g.Injective
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.TotallyUnimodular (goal)
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
⊢ Membership.mem (γ := Set R) (Set.range SignType.cast) (A.submatrix f g).det
have neg : ∀ (hfg : ¬(Function.Injective f ∧ Function.Injective g)),
  Membership.mem (γ := Set R) (Set.range SignType.cast) (A.submatrix f g).det
Tactic: by_cases hfg : f.Injective ∧ g.Injective
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.TotallyUnimodular (goal)
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
have h : (↑0 : R) = (A.submatrix f g).det
Tactic: use 0
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.TotallyUnimodular (goal)
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)
⊢ (↑0 : R) = (A.submatrix f g).det
have h : (A.submatrix f g).det = 0
Tactic: rw [SignType.coe_zero, eq_comm]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.TotallyUnimodular (hypothesis)
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.submatrix f g).det = 0
have 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
Tactic: simp_rw [not_and_or, Function.not_injective_iff] at hfg
Cleared hypotheses: hfg
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.TotallyUnimodular (goal)
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
⊢ (A.submatrix f g).det = 0
have h : ∀ (i j : Fin k) (hfij : f i = f j) (hij : i ≠ j), (A.submatrix f g).det = 0
Tactic: obtain ⟨i, j, hfij, hij⟩ | ⟨i, j, hgij, hij⟩ := hfg
Cleared hypotheses: hfg
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.TotallyUnimodular (goal)
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
⊢ (A.submatrix f g).det = 0
have h₁ : ∀ (i j : Fin k) (hgij : g i = g j) (hij : i ≠ j), (A.submatrix f g).det = 0
Tactic: obtain ⟨i, j, hfij, hij⟩ | ⟨i, j, hgij, hij⟩ := hfg
Cleared hypotheses: hfg
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.TotallyUnimodular (goal)
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
⊢ (A.submatrix f g).det = 0
have h : (Aᵀ.submatrix g f).det = 0
Tactic: rw [← det_transpose, transpose_submatrix]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.TotallyUnimodular (goal)
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
⊢ (Aᵀ.submatrix g f).det = 0
have h : ∀ (k_1 : Fin k), Aᵀ.submatrix g f k_1 j = Aᵀ.submatrix g f k_1 i
Tactic: apply det_zero_of_column_eq hij.symm
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.TotallyUnimodular (goal)
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
⊢ (A.submatrix f g).det = 0
have h : ∀ (k_1 : Fin k), A.submatrix f g k_1 i = A.submatrix f g k_1 j
Tactic: apply det_zero_of_column_eq hij
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.TotallyUnimodular (goal)
Goal:
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_1 : Fintype ι] [inst_2 : DecidableEq ι] (f : ι → m) (g : ι → n),
      Membership.mem (γ := Set R) (Set.range SignType.cast) (A.submatrix f g).det
have 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
Tactic: rw [isTotallyUnimodular_iff]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.TotallyUnimodular (goal)
Goal:
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),
      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
have 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
Tactic: constructor
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.TotallyUnimodular (goal)
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
⊢ (∀ (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
have 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
Tactic: constructor
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.TotallyUnimodular (hypothesis)
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
ι : 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
have hA₁ : Membership.mem (γ := Set R) (Set.range SignType.cast)
  (det (n := Fin (Fintype.card ι))
    (A.submatrix (f ∘ (⇑(Equiv.symm (Fintype.equivFin ι)) : (a : Fin (Fintype.card ι)) → ι))
      (g ∘ (⇑(Equiv.symm (Fintype.equivFin ι)) : (a : Fin (Fintype.card ι)) → ι))))
Tactic: specialize hA (Fintype.card ι) (f ∘ (Fintype.equivFin ι).symm) (g ∘ (Fintype.equivFin ι).symm)
Cleared hypotheses: hA
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.TotallyUnimodular (goal)
Goal:
m : Type u_1
n : Type u_3
R : Type u_5
inst : CommRing R
A : Matrix m n R
ι : Type w
inst_1 : Fintype ι
inst_2 : DecidableEq ι
f : ι → m
g : ι → n
hA :
  Membership.mem (γ := Set R) (Set.range SignType.cast)
    (det (n := Fin (Fintype.card ι))
      (A.submatrix (f ∘ (⇑(Equiv.symm (Fintype.equivFin ι)) : (a : Fin (Fintype.card ι)) → ι))
        (g ∘ (⇑(Equiv.symm (Fintype.equivFin ι)) : (a : Fin (Fintype.card ι)) → ι))))
⊢ Membership.mem (γ := Set R) (Set.range SignType.cast) (A.submatrix f g).det
have mp : ∀
  (hA :
    Membership.mem (γ := Set R) (Set.range SignType.cast)
      (det (n := Fin (Fintype.card ι))
        ((A.submatrix f g).submatrix (⇑(Equiv.symm (Fintype.equivFin ι)) : (a : Fin (Fintype.card ι)) → ι)
          (⇑(Equiv.symm (Fintype.equivFin ι)) : (a : Fin (Fintype.card ι)) → ι)))),
  Membership.mem (γ := Set R) (Set.range SignType.cast) (A.submatrix f g).det
Tactic: rwa [← submatrix_submatrix, det_submatrix_equiv_self] at hA
Cleared hypotheses: hA
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.TotallyUnimodular (goal)
Goal:
m : Type u_1
n : Type u_3
R : Type u_5
inst : CommRing R
A : Matrix m n R
ι : Type w
inst_1 : Fintype ι
inst_2 : DecidableEq ι
f : ι → m
g : ι → n
hA :
  Membership.mem (γ := Set R) (Set.range SignType.cast)
    (det (n := Fin (Fintype.card ι))
      (A.submatrix (f ∘ (⇑(Equiv.symm (Fintype.equivFin ι)) : (a : Fin (Fintype.card ι)) → ι))
        (g ∘ (⇑(Equiv.symm (Fintype.equivFin ι)) : (a : Fin (Fintype.card ι)) → ι))))
mp :
  ∀
    (hA :
      Membership.mem (γ := Set R) (Set.range SignType.cast)
        (det (n := Fin (Fintype.card ι))
          ((A.submatrix f g).submatrix (⇑(Equiv.symm (Fintype.equivFin ι)) : (a : Fin (Fintype.card ι)) → ι)
            (⇑(Equiv.symm (Fintype.equivFin ι)) : (a : Fin (Fintype.card ι)) → ι)))),
    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
have mp₁ : ∀ (hA : 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: rwa [← submatrix_submatrix, det_submatrix_equiv_self] at hA
Cleared hypotheses: hA
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.TotallyUnimodular (hypothesis)
Goal:
m : Type u_1
n : Type u_3
R : Type u_5
inst : CommRing R
A : Matrix m n R
hA :
  ∀ (ι : 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
have hA₁ : Membership.mem (γ := Set R) (Set.range SignType.cast)
  (det.{u_5, w} (n := ULift.{w, 0} (Fin k))
    (A.submatrix (f ∘ (⇑Equiv.ulift : (a : ULift.{w, 0} (Fin k)) → Fin k))
      (g ∘ (⇑Equiv.ulift : (a : ULift.{w, 0} (Fin k)) → Fin k))))
Tactic: specialize hA (ULift (Fin k)) (f ∘ Equiv.ulift) (g ∘ Equiv.ulift)
Cleared hypotheses: hA