awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
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
⊢ Membership.mem (γ := Set R) (Set.range SignType.cast) ((A.fromRows B).submatrix f g).det
have 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
Tactic: rw [Fintype.sum_eq_single x fun y hxy => ?_, Pi.single_eq_same] 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
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
⊢ Membership.mem (γ := Set R) (Set.range SignType.cast) ((A.fromRows B).submatrix f g).det
have 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
Tactic: rw [Fintype.sum_eq_single x fun y hxy => ?_, Pi.single_eq_same] at 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
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 (γ := Set R) (Set.range SignType.cast) ((A.fromRows B).submatrix f g).det
have 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)
Tactic: rw [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
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 (γ := 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)
have 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)
Tactic: change _ ∈ MonoidHom.mrange SignType.castHom.toMonoidHom
-- 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
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)
have pos : Membership.mem (γ := Submonoid R) (MonoidHom.mrange (F := SignType →* R) (↑SignType.castHom : SignType →* R))
  (HPow.hPow (α := R) (-1) ((↑i : ℕ) + (↑x : ℕ)))
Tactic: refine mul_mem (mul_mem ?_ (Set.mem_range_self s)) ?_
-- 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
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 : ℕ)))
⊢ 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)
have 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
Tactic: refine mul_mem (mul_mem ?_ (Set.mem_range_self s)) ?_
-- 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
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 : ℕ)))
have pos : Membership.mem (γ := Submonoid R) (MonoidHom.mrange (F := SignType →* R) (↑SignType.castHom : SignType →* R)) (-1)
Tactic: apply pow_mem
-- 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
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 hj''₁ : ∀ (x : Fin (k + 1)), ¬g x = j'
Tactic: rw [not_exists] at hj''
Cleared hypotheses: hj''
-- 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 h : (↑0 : R) = ((A.fromRows B).submatrix f g).det
Tactic: use 0
-- 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
g : Fin (k + 1) → n
hg : Function.Injective g
hB : ∀ (i : m'), ∃ (j : n) (s : SignType), B i = Pi.single (M := fun (j : n) ↦ R) j (↑s : R)
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
have succ : ∀
  (hA :
    ∀ (k : ℕ) (f : Fin k → m) (g : Fin k → n),
      Membership.mem (γ := Set R) (Set.range SignType.cast) (A.submatrix f g).det)
  (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)
  (g : Fin (k + 1) → n) (hg : Function.Injective g)
  (hB : ∀ (i : m'), ∃ (j : n) (s : SignType), B i = Pi.single (M := fun (j : n) ↦ R) j (↑s : R)) (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: rw [isTotallyUnimodular_iff] at hA
Cleared hypotheses: hA, k, ih, g, hg, hB, f', 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
hB : Nonempty n → ∀ (i : m'), ∃ (j : n) (s : SignType), B i = Pi.single (M := fun (j : n) ↦ R) j (↑s : R)
k : ℕ
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
have zero : ∀ (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
Tactic: induction k with
  | zero => use 1; simp
  | succ k ih =>
    specialize hB ⟨g 0⟩
    -- Either `f` is `inr` somewhere or `inl` everywhere
    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'⟩
    · have hAB := det_succ_row ((fromRows A B).submatrix f g) i
      simp only [submatrix_apply, hfi, fromRows_apply_inr] at hAB
      obtain ⟨j', s, hj'⟩ := hB j
      · simp only [hj'] at hAB
        by_cases hj'' : ∃ x, g x = j'
        · obtain ⟨x, rfl⟩ := hj''
          rw [Fintype.sum_eq_single x fun y hxy => ?_, Pi.single_eq_same] at hAB
          · rw [hAB]
            change _ ∈ MonoidHom.mrange SignType.castHom.toMonoidHom
            refine mul_mem (mul_mem ?_ (Set.mem_range_self s)) ?_
            · apply pow_mem
              exact ⟨-1, by simp⟩
            · exact ih _ _
                (hf.comp Fin.succAbove_right_injective)
                (hg.comp Fin.succAbove_right_injective)
          · simp [Pi.single_eq_of_ne, hg.ne_iff.mpr hxy]
        · rw [not_exists] at hj''
          use 0
          simpa [hj''] using hAB.symm
    · rw [isTotallyUnimodular_iff] at hA
      apply hA
Cleared hypotheses: k, f, g, hf, hg
-- 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)
k : ℕ
f : Fin k → m ⊕ m'
g : Fin k → n
hf : Function.Injective f
hg : Function.Injective g
zero :
  ∀ (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
⊢ Membership.mem (γ := Set R) (Set.range SignType.cast) ((A.fromRows B).submatrix f g).det
have succ : ∀ (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
Tactic: induction k with
  | zero => use 1; simp
  | succ k ih =>
    specialize hB ⟨g 0⟩
    -- Either `f` is `inr` somewhere or `inl` everywhere
    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'⟩
    · have hAB := det_succ_row ((fromRows A B).submatrix f g) i
      simp only [submatrix_apply, hfi, fromRows_apply_inr] at hAB
      obtain ⟨j', s, hj'⟩ := hB j
      · simp only [hj'] at hAB
        by_cases hj'' : ∃ x, g x = j'
        · obtain ⟨x, rfl⟩ := hj''
          rw [Fintype.sum_eq_single x fun y hxy => ?_, Pi.single_eq_same] at hAB
          · rw [hAB]
            change _ ∈ MonoidHom.mrange SignType.castHom.toMonoidHom
            refine mul_mem (mul_mem ?_ (Set.mem_range_self s)) ?_
            · apply pow_mem
              exact ⟨-1, by simp⟩
            · exact ih _ _
                (hf.comp Fin.succAbove_right_injective)
                (hg.comp Fin.succAbove_right_injective)
          · simp [Pi.single_eq_of_ne, hg.ne_iff.mpr hxy]
        · rw [not_exists] at hj''
          use 0
          simpa [hj''] using hAB.symm
    · rw [isTotallyUnimodular_iff] at hA
      apply hA
Cleared hypotheses: k, f, g, hf, hg
-- 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
inst_1 : DecidableEq n
A : Matrix m n R
⊢ IsTotallyUnimodular (m := n ⊕ m) (fromRows 1 A) ↔ A.IsTotallyUnimodular
have hA : Eq (α := Matrix (n ⊕ m) n R) (fromRows 1 A)
  ((reindex (Equiv.sumComm m n) (Equiv.refl n) : (a : Matrix (m ⊕ n) n R) → Matrix (n ⊕ m) n R) (A.fromRows 1))
Tactic: have hA :
    fromRows (1 : Matrix n n R) A =
      (fromRows A (1 : Matrix n n R)).reindex (Equiv.sumComm m n) (Equiv.refl n) := by
    aesop
-- 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 : DecidableEq n
A : Matrix m n R
hA :
  Eq (α := Matrix (n ⊕ m) n R) (fromRows 1 A)
    ((reindex (Equiv.sumComm m n) (Equiv.refl n) : (a : Matrix (m ⊕ n) n R) → Matrix (n ⊕ m) n R) (A.fromRows 1))
⊢ IsTotallyUnimodular (m := n ⊕ m) (fromRows 1 A) ↔ A.IsTotallyUnimodular
have rw : IsTotallyUnimodular (m := n ⊕ m) (n := n) (R := R)
    ((reindex (Equiv.sumComm m n) (Equiv.refl n) : (a : Matrix (m ⊕ n) n R) → Matrix (n ⊕ m) n R) (A.fromRows 1)) ↔
  A.IsTotallyUnimodular
Tactic: rw [hA, reindex_isTotallyUnimodular, fromRows_one_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
inst_1 : DecidableEq n
A : Matrix m n R
hA :
  Eq (α := Matrix (n ⊕ m) n R) (fromRows 1 A)
    ((reindex (Equiv.sumComm m n) (Equiv.refl n) : (a : Matrix (m ⊕ n) n R) → Matrix (n ⊕ m) n R) (A.fromRows 1))
rw :
  IsTotallyUnimodular (m := n ⊕ m) (n := n) (R := R)
      ((reindex (Equiv.sumComm m n) (Equiv.refl n) : (a : Matrix (m ⊕ n) n R) → Matrix (n ⊕ m) n R) (A.fromRows 1)) ↔
    A.IsTotallyUnimodular
⊢ IsTotallyUnimodular (m := n ⊕ m) (fromRows 1 A) ↔ A.IsTotallyUnimodular
have rw₁ : IsTotallyUnimodular (m := m ⊕ n) (A.fromRows 1) ↔ A.IsTotallyUnimodular
Tactic: rw [hA, reindex_isTotallyUnimodular, fromRows_one_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
inst_1 : DecidableEq n
A : Matrix m n R
hA :
  Eq (α := Matrix (n ⊕ m) n R) (fromRows 1 A)
    ((reindex (Equiv.sumComm m n) (Equiv.refl n) : (a : Matrix (m ⊕ n) n R) → Matrix (n ⊕ m) n R) (A.fromRows 1))
rw :
  IsTotallyUnimodular (m := n ⊕ m) (n := n) (R := R)
      ((reindex (Equiv.sumComm m n) (Equiv.refl n) : (a : Matrix (m ⊕ n) n R) → Matrix (n ⊕ m) n R) (A.fromRows 1)) ↔
    A.IsTotallyUnimodular
rw₁ : IsTotallyUnimodular (m := m ⊕ n) (A.fromRows 1) ↔ A.IsTotallyUnimodular
⊢ IsTotallyUnimodular (m := n ⊕ m) (fromRows 1 A) ↔ A.IsTotallyUnimodular
have rw₂ : A.IsTotallyUnimodular ↔ A.IsTotallyUnimodular
Tactic: rw [hA, reindex_isTotallyUnimodular, fromRows_one_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
inst_1 : DecidableEq m
A : Matrix m n R
⊢ IsTotallyUnimodular (n := n ⊕ m) (A.fromCols 1) ↔ A.IsTotallyUnimodular
have rw : IsTotallyUnimodular (m := n ⊕ m) (A.fromCols 1)ᵀ ↔ A.IsTotallyUnimodular
Tactic: rw [← transpose_isTotallyUnimodular_iff, transpose_fromCols, transpose_one,
    fromRows_one_isTotallyUnimodular_iff, transpose_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
inst_1 : DecidableEq m
A : Matrix m n R
rw : IsTotallyUnimodular (m := n ⊕ m) (A.fromCols 1)ᵀ ↔ A.IsTotallyUnimodular
⊢ IsTotallyUnimodular (n := n ⊕ m) (A.fromCols 1) ↔ A.IsTotallyUnimodular
have rw₁ : IsTotallyUnimodular (m := n ⊕ m) (Aᵀ.fromRows 1ᵀ) ↔ A.IsTotallyUnimodular
Tactic: rw [← transpose_isTotallyUnimodular_iff, transpose_fromCols, transpose_one,
    fromRows_one_isTotallyUnimodular_iff, transpose_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
inst_1 : DecidableEq m
A : Matrix m n R
rw : IsTotallyUnimodular (m := n ⊕ m) (A.fromCols 1)ᵀ ↔ A.IsTotallyUnimodular
rw₁ : IsTotallyUnimodular (m := n ⊕ m) (Aᵀ.fromRows 1ᵀ) ↔ A.IsTotallyUnimodular
⊢ IsTotallyUnimodular (n := n ⊕ m) (A.fromCols 1) ↔ A.IsTotallyUnimodular
have rw₂ : IsTotallyUnimodular (m := n ⊕ m) (Aᵀ.fromRows 1) ↔ A.IsTotallyUnimodular
Tactic: rw [← transpose_isTotallyUnimodular_iff, transpose_fromCols, transpose_one,
    fromRows_one_isTotallyUnimodular_iff, transpose_isTotallyUnimodular_iff]