awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
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))))
⊢ Membership.mem (γ := Set R) (Set.range SignType.cast) (A.submatrix f g).det
have mpr : ∀
  (hA :
    Membership.mem (γ := Set R) (Set.range SignType.cast)
      (det.{u_5, w} (n := ULift.{w, 0} (Fin k))
        ((A.submatrix f g).submatrix (⇑Equiv.ulift : (a : ULift.{w, 0} (Fin k)) → Fin k)
          (⇑Equiv.ulift : (a : ULift.{w, 0} (Fin k)) → Fin k)))),
  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
k : ℕ
f : Fin k → m
g : Fin k → n
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))))
mpr :
  ∀
    (hA :
      Membership.mem (γ := Set R) (Set.range SignType.cast)
        (det.{u_5, w} (n := ULift.{w, 0} (Fin k))
          ((A.submatrix f g).submatrix (⇑Equiv.ulift : (a : ULift.{w, 0} (Fin k)) → Fin k)
            (⇑Equiv.ulift : (a : ULift.{w, 0} (Fin k)) → Fin k)))),
    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 mpr₁ : ∀ (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 (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
i : m
j : n
⊢ Membership.mem (γ := Set R) (Set.range SignType.cast) (A i j)
have rw : ∀
  (hA :
    ∀ (k : ℕ) (f : Fin k → m) (g : Fin k → n),
      Membership.mem (γ := Set R) (Set.range SignType.cast) (A.submatrix f g).det)
  (i : m) (j : n), Membership.mem (γ := Set R) (Set.range SignType.cast) (A i j)
Tactic: rw [isTotallyUnimodular_iff] at hA
Cleared hypotheses: hA, i, j
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.TotallyUnimodular (goal)
Goal:
m : Type u_1
m' : Type u_2
n : Type u_3
n' : Type u_4
R : Type u_5
inst : CommRing R
A : Matrix m n R
f : m' → m
g : n' → n
hA : A.IsTotallyUnimodular
⊢ (A.submatrix f g).IsTotallyUnimodular
have simp : ∀
  (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_1 : Fin k → m') (g_1 : Fin k → n'),
  Membership.mem (γ := Set R) (Set.range SignType.cast) (A.submatrix (f ∘ f_1) (g ∘ g_1)).det
Tactic: simp only [isTotallyUnimodular_iff, submatrix_submatrix] 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
hA : A.IsTotallyUnimodular
⊢ Aᵀ.IsTotallyUnimodular
have simp : ∀
  (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 → n) (g : Fin k → m), Membership.mem (γ := Set R) (Set.range SignType.cast) (A.submatrix g f).det
Tactic: simp only [isTotallyUnimodular_iff, ← transpose_submatrix, det_transpose] 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
⊢ Aᵀ.IsTotallyUnimodular ↔ A.IsTotallyUnimodular
have mp : Aᵀ.IsTotallyUnimodular → 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
mp : Aᵀ.IsTotallyUnimodular → A.IsTotallyUnimodular
⊢ Aᵀ.IsTotallyUnimodular ↔ A.IsTotallyUnimodular
have mpr : A.IsTotallyUnimodular → 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
inst_1 : IsEmpty m
A : Matrix m n R
f : Fin 0 → m
g : Fin 0 → n
h : Function.Injective f
h_1 : Function.Injective g
⊢ Membership.mem (γ := Set R) (Set.range SignType.cast) (A.submatrix f g).det
have h : (↑1 : R) = (A.submatrix f g).det
Tactic: use 1
-- 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
inst_1 : IsEmpty m
A : Matrix m n R
f : Fin 0 → m
g : Fin 0 → n
h : Function.Injective f
h_1 : Function.Injective g
⊢ (↑1 : R) = (A.submatrix f g).det
have h : Eq.{u_5 + 1} (α := R) (↑1 : R) (det ![])
Tactic: rw [submatrix_empty, det_fin_zero, SignType.coe_one]
-- 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
inst_1 : IsEmpty m
A : Matrix m n R
f : Fin 0 → m
g : Fin 0 → n
h_1 : Function.Injective f
h_2 : Function.Injective g
h : Eq.{u_5 + 1} (α := R) (↑1 : R) (det ![])
⊢ (↑1 : R) = (A.submatrix f g).det
have h₁ : Eq.{u_5 + 1} (α := R) (↑1 : R) 1
Tactic: rw [submatrix_empty, det_fin_zero, SignType.coe_one]
-- 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
inst_1 : IsEmpty m
A : Matrix m n R
f : Fin 0 → m
g : Fin 0 → n
h_1 : Function.Injective f
h_2 : Function.Injective g
h : Eq.{u_5 + 1} (α := R) (↑1 : R) (det ![])
h₁ : Eq.{u_5 + 1} (α := R) (↑1 : R) 1
⊢ (↑1 : R) = (A.submatrix f g).det
have h₂ : Eq.{u_5 + 1} (α := R) 1 1
Tactic: rw [submatrix_empty, det_fin_zero, SignType.coe_one]
-- 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
inst_1 : IsEmpty m
A : Matrix m n R
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
have zero : ∀ (f : Fin 0 → m) (g : Fin 0 → n),
  Function.Injective f →
    Function.Injective g → Membership.mem (γ := Set R) (Set.range SignType.cast) (A.submatrix f g).det
Tactic: cases k with
  | zero => use 1; rw [submatrix_empty, det_fin_zero, SignType.coe_one]
  | succ => exact (IsEmpty.false (f 0)).elim
Cleared hypotheses: k, f, g, h, h_1
-- 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
inst_1 : IsEmpty m
A : Matrix m n R
k : ℕ
f : Fin k → m
g : Fin k → n
h : Function.Injective f
h_1 : Function.Injective g
zero :
  ∀ (f : Fin 0 → m) (g : Fin 0 → n),
    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 succ : ∀ (n_1 : ℕ) (f : Fin (n_1 + 1) → m) (g : Fin (n_1 + 1) → n),
  Function.Injective f →
    Function.Injective g → Membership.mem (γ := Set R) (Set.range SignType.cast) (A.submatrix f g).det
Tactic: cases k with
  | zero => use 1; rw [submatrix_empty, det_fin_zero, SignType.coe_one]
  | succ => exact (IsEmpty.false (f 0)).elim
Cleared hypotheses: k, f, g, h, h_1
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.TotallyUnimodular (goal)
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
hB : Nonempty n → ∀ (i : m'), ∃ (j : n) (s : SignType), B i = Pi.single (M := fun (j : n) ↦ R) j (↑s : R)
f : Fin 0 → m ⊕ m'
g : Fin 0 → n
hf : Function.Injective f
hg : Function.Injective g
⊢ Membership.mem (γ := Set R) (Set.range SignType.cast) ((A.fromRows B).submatrix f g).det
have h : (↑1 : R) = ((A.fromRows B).submatrix f g).det
Tactic: use 1
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.TotallyUnimodular (hypothesis)
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
hB : Nonempty n → ∀ (i : m'), ∃ (j : n) (s : SignType), B i = Pi.single (M := fun (j : n) ↦ R) j (↑s : R)
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
⊢ Membership.mem (γ := Set R) (Set.range SignType.cast) ((A.fromRows B).submatrix f g).det
have hB₁ : ∀ (i : m'), ∃ (j : n) (s : SignType), B i = Pi.single (M := fun (j : n) ↦ R) j (↑s : R)
Tactic: specialize hB ⟨g 0⟩
Cleared hypotheses: hB
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.TotallyUnimodular (goal)
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'), f i = Sum.inr j) ∨ ∃ (f' : Fin (k + 1) → m), f = Sum.inl ∘ f'
have simp_rw : (∀ (x : Fin (k + 1)), ∃ (y : m), f x = Sum.inl y) → ∃ (f' : Fin (k + 1) → m), f = Sum.inl ∘ f'
Tactic: simp_rw [← Sum.isRight_iff, or_iff_not_imp_left, not_exists, Bool.not_eq_true,
        Sum.isRight_eq_false, Sum.isLeft_iff]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.TotallyUnimodular (goal)
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)
hfr : ∀ (x : Fin (k + 1)), ∃ (y : m), f x = Sum.inl y
⊢ ∃ (f' : Fin (k + 1) → m), f = Sum.inl ∘ f'
have choose : ∀ (f' : (x : Fin (k + 1)) → m) (hf' : ∀ (x : Fin (k + 1)), f x = Sum.inl (f' x)),
  ∃ (f' : Fin (k + 1) → m), f = Sum.inl ∘ f'
Tactic: choose f' hf' using hfr
Cleared hypotheses: hfr
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.TotallyUnimodular (goal)
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)
⊢ Membership.mem (γ := Set R) (Set.range SignType.cast) ((A.fromRows B).submatrix f g).det
have succ : ∀ (i : Fin (k + 1)) (j : m') (hfi : f i = Sum.inr j),
  Membership.mem (γ := Set R) (Set.range SignType.cast) ((A.fromRows B).submatrix f g).det
Tactic: obtain ⟨i, j, hfi⟩ | ⟨f', rfl⟩ : (∃ i j, f i = .inr j) ∨ (∃ f', f = .inl ∘ f') := by
      simp_rw [← Sum.isRight_iff, or_iff_not_imp_left, not_exists, Bool.not_eq_true,
        Sum.isRight_eq_false, Sum.isLeft_iff]
      intro hfr
      choose f' hf' using hfr
      exact ⟨f', funext hf'⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.TotallyUnimodular (goal)
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)
succ :
  ∀ (i : Fin (k + 1)) (j : m') (hfi : f i = Sum.inr 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
have succ₁ : ∀ (f' : Fin (k + 1) → m) (hf : Function.Injective (β := m ⊕ m') (Sum.inl ∘ f')),
  Membership.mem (γ := Set R) (Set.range SignType.cast) ((A.fromRows B).submatrix (Sum.inl ∘ f') g).det
Tactic: obtain ⟨i, j, hfi⟩ | ⟨f', rfl⟩ : (∃ i j, f i = .inr j) ∨ (∃ f', f = .inl ∘ f') := by
      simp_rw [← Sum.isRight_iff, or_iff_not_imp_left, not_exists, Bool.not_eq_true,
        Sum.isRight_eq_false, Sum.isLeft_iff]
      intro hfr
      choose f' hf' using hfr
      exact ⟨f', funext hf'⟩
Cleared hypotheses: f, hf
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.TotallyUnimodular (hypothesis)
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
⊢ Membership.mem (γ := Set R) (Set.range SignType.cast) ((A.fromRows B).submatrix f g).det
have 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
Tactic: have hAB := det_succ_row ((fromRows A B).submatrix f g) i
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.TotallyUnimodular (hypothesis)
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
⊢ Membership.mem (γ := Set R) (Set.range SignType.cast) ((A.fromRows B).submatrix f g).det
have 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
Tactic: simp only [submatrix_apply, hfi, fromRows_apply_inr] at hAB
Cleared hypotheses: hAB
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.TotallyUnimodular (goal)
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
⊢ Membership.mem (γ := Set R) (Set.range SignType.cast) ((A.fromRows B).submatrix f g).det
have 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
Tactic: obtain ⟨j', s, hj'⟩ := hB j
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.TotallyUnimodular (hypothesis)
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)
⊢ Membership.mem (γ := Set R) (Set.range SignType.cast) ((A.fromRows B).submatrix f g).det
have 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
Tactic: simp only [hj'] at hAB
Cleared hypotheses: hAB
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.TotallyUnimodular (goal)
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
⊢ Membership.mem (γ := Set R) (Set.range SignType.cast) ((A.fromRows B).submatrix f g).det
have pos : ∀ (hj'' : ∃ (x : Fin (k + 1)), g x = j'),
  Membership.mem (γ := Set R) (Set.range SignType.cast) ((A.fromRows B).submatrix f g).det
Tactic: by_cases hj'' : ∃ x, g x = j'
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.TotallyUnimodular (goal)
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
⊢ Membership.mem (γ := Set R) (Set.range SignType.cast) ((A.fromRows B).submatrix f g).det
have neg : ∀ (hj'' : ¬∃ (x : Fin (k + 1)), g x = j'),
  Membership.mem (γ := Set R) (Set.range SignType.cast) ((A.fromRows B).submatrix f g).det
Tactic: by_cases hj'' : ∃ x, g x = j'
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.TotallyUnimodular (goal)
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'
⊢ Membership.mem (γ := Set R) (Set.range SignType.cast) ((A.fromRows B).submatrix f g).det
have 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
Tactic: obtain ⟨x, rfl⟩ := hj''
Cleared hypotheses: j', hj', hAB, hj''