awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
ι : Type w
mp :
  ∀ [inst_1 : Fintype ι] [inst_2 : DecidableEq ι] (f : ι → m) (g : ι → n),
    Membership.mem (γ := Set R) (Set.range SignType.cast) (A.submatrix f g).det
⊢ ∀ [inst_1 : Fintype ι] [inst_2 : DecidableEq ι] (f : ι → m) (g : ι → n),
    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
ι : Type w
inst_1 : Fintype ι
mp :
  ∀ [inst_2 : DecidableEq ι] (f : ι → m) (g : ι → n),
    Membership.mem (γ := Set R) (Set.range SignType.cast) (A.submatrix f g).det
⊢ ∀ [inst_2 : DecidableEq ι] (f : ι → m) (g : ι → n),
    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
ι : Type w
inst_1 : Fintype ι
inst_2 : DecidableEq ι
f : ι → m
g : ι → n
⊢ 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)

Premises used: Function.comp, Fintype.card, Fintype.equivFin, Equiv.symm, DFunLike.coe
-- 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
ι : 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
mp₁ mp₂ mp₃ 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
⊢ Membership.mem (γ := Set R) (Set.range SignType.cast) (A.submatrix f g).det

Tactic:
rwa [← submatrix_submatrix, det_submatrix_equiv_self] at hA

Premises used: Matrix.submatrix_submatrix, Matrix.det_submatrix_equiv_self
-- 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 :
  ∀ (ι : 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)
    (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)

Premises used: ULift, Function.comp, Equiv.ulift, Fin, DFunLike.coe
-- 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
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
mpr₁ mpr₂ mpr₃ 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
⊢ Membership.mem (γ := Set R) (Set.range SignType.cast) (A.submatrix f g).det

Tactic:
rwa [← submatrix_submatrix, det_submatrix_equiv_self] at hA

Premises used: Matrix.submatrix_submatrix, Matrix.det_submatrix_equiv_self
-- 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
i : m
j : n
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)
⊢ Membership.mem (γ := Set R) (Set.range SignType.cast) (A i j)

Tactic:
rw [isTotallyUnimodular_iff] at hA

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
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:
simpa using hA 1 (fun _ => i) (fun _ => j)

Premises used: OfNat.ofNat
-- Module: Mathlib.LinearAlgebra.Matrix.Determinant.TotallyUnimodular
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
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
⊢ (A.submatrix f g).IsTotallyUnimodular

Tactic:
simp only [isTotallyUnimodular_iff, submatrix_submatrix] at hA ⊢

Premises used: Matrix.isTotallyUnimodular_iff, Matrix.submatrix_submatrix
-- Module: Mathlib.LinearAlgebra.Matrix.Determinant.TotallyUnimodular
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 :
  ∀ (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
⊢ ∀ (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:
_
-- Module: Mathlib.LinearAlgebra.Matrix.Determinant.TotallyUnimodular
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 :
  ∀ (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
⊢ ∀ (g_1 : Fin k → n'), Membership.mem (γ := Set R) (Set.range SignType.cast) (A.submatrix (f ∘ f_1) (g ∘ g_1)).det

Tactic:
_
-- Module: Mathlib.LinearAlgebra.Matrix.Determinant.TotallyUnimodular
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 :
  ∀ (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:
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
hA : A.IsTotallyUnimodular
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
⊢ Aᵀ.IsTotallyUnimodular

Tactic:
simp only [isTotallyUnimodular_iff, ← transpose_submatrix, det_transpose] at hA ⊢

Premises used: Matrix.isTotallyUnimodular_iff, 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 :
  ∀ (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
⊢ ∀ (f : Fin k → n) (g : Fin k → m), Membership.mem (γ := Set R) (Set.range SignType.cast) (A.submatrix g f).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 → n
_ : ∀ (g : Fin k → m), Membership.mem (γ := Set R) (Set.range SignType.cast) (A.submatrix g f).det
⊢ ∀ (g : Fin k → m), Membership.mem (γ := Set R) (Set.range SignType.cast) (A.submatrix g f).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 → n
g : Fin k → m
⊢ Membership.mem (γ := Set R) (Set.range SignType.cast) (A.submatrix g f).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
mp : Aᵀ.IsTotallyUnimodular → A.IsTotallyUnimodular
mpr : A.IsTotallyUnimodular → Aᵀ.IsTotallyUnimodular
⊢ Aᵀ.IsTotallyUnimodular ↔ A.IsTotallyUnimodular

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
⊢ Aᵀ.IsTotallyUnimodular → A.IsTotallyUnimodular

Tactic:
apply IsTotallyUnimodular.transpose

Premises used: Matrix.IsTotallyUnimodular.transpose
-- 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
⊢ A.IsTotallyUnimodular → Aᵀ.IsTotallyUnimodular

Tactic:
apply IsTotallyUnimodular.transpose

Premises used: Matrix.IsTotallyUnimodular.transpose
-- Module: Mathlib.LinearAlgebra.Matrix.Determinant.TotallyUnimodular
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
em : m ≃ m'
en : n ≃ n'
hA : A.IsTotallyUnimodular
⊢ IsTotallyUnimodular.{u_2, u_4, u_5} (m := m') (n := n') (R := R)
    ((Matrix.reindex em en : (a : Matrix m n R) → Matrix m' n' R) A)

Tactic:
hA.submatrix _ _

Premises used: Matrix.submatrix, Matrix.IsTotallyUnimodular.submatrix
-- Module: Mathlib.LinearAlgebra.Matrix.Determinant.TotallyUnimodular
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
em : m ≃ m'
en : n ≃ n'
hA :
  IsTotallyUnimodular.{u_2, u_4, u_5} (m := m') (n := n') (R := R)
    ((reindex em en : (a : Matrix m n R) → Matrix m' n' R) A)
⊢ A.IsTotallyUnimodular

Tactic:
simpa [Equiv.symm_apply_eq] using hA.reindex em.symm en.symm

Premises used: Equiv.symm_apply_eq, Matrix.IsTotallyUnimodular.reindex, Equiv.symm
-- Module: Mathlib.LinearAlgebra.Matrix.Determinant.TotallyUnimodular
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),
    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
inst_1 : IsEmpty m
A : Matrix m n R
k : ℕ
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
⊢ 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
inst_1 : IsEmpty m
A : Matrix m n R
k : ℕ
f : Fin k → m
g : Fin k → n
h : Function.Injective f
_ : 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
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 : (↑1 : R) = (A.submatrix f g).det
⊢ Membership.mem (γ := Set R) (Set.range SignType.cast) (A.submatrix f g).det

Tactic:
use 1
-- Module: Mathlib.LinearAlgebra.Matrix.Determinant.TotallyUnimodular
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
h₂ h₃ : Eq.{u_5 + 1} (α := R) 1 1
⊢ (↑1 : R) = (A.submatrix f g).det

Tactic:
rw [submatrix_empty, det_fin_zero, SignType.coe_one]

Premises used: SignType.coe_one, Matrix.submatrix_empty, Matrix.det_fin_zero
-- Module: Mathlib.LinearAlgebra.Matrix.Determinant.TotallyUnimodular
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
n_1 : ℕ
f : Fin (n_1 + 1) → m
g : Fin (n_1 + 1) → n
h : Function.Injective f
h_1 : Function.Injective g
⊢ Membership.mem (γ := Set R) (Set.range SignType.cast) (A.submatrix f g).det

Tactic:
(IsEmpty.false (f 0)).elim

Premises used: False.elim, IsEmpty.false, OfNat.ofNat
-- Module: Mathlib.LinearAlgebra.Matrix.Determinant.TotallyUnimodular
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
n_1 : ℕ
f : Fin (n_1 + 1) → m
g : Fin (n_1 + 1) → n
h : Function.Injective f
h_1 : Function.Injective g
⊢ Membership.mem (γ := Set R) (Set.range SignType.cast) (A.submatrix f g).det

Tactic:
exact (IsEmpty.false (f 0)).elim

Premises used: False.elim, IsEmpty.false, OfNat.ofNat
-- Module: Mathlib.LinearAlgebra.Matrix.Determinant.TotallyUnimodular
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
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
⊢ 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

Premises used: SignType.coe_one, Matrix.submatrix_empty, Matrix.det_fin_zero, Matrix.zero
-- Module: Mathlib.LinearAlgebra.Matrix.Determinant.TotallyUnimodular
Goal:
m : Type u_1
n : Type u_3
R : Type u_5
inst : CommRing R
inst_1 : IsEmpty n
A : Matrix m n R
⊢ A.IsTotallyUnimodular

Tactic:
A.transpose.emptyRows_isTotallyUnimodular.transpose

Premises used: Matrix.transpose, Matrix.emptyRows_isTotallyUnimodular, Matrix.IsTotallyUnimodular.transpose
-- Module: Mathlib.LinearAlgebra.Matrix.Determinant.TotallyUnimodular
Goal:
m : Type u_1
m' : Type u_2
n : Type u_3
R : Type u_5
inst : CommRing R
inst_1 : DecidableEq n
A : Matrix m n R
B : Matrix m' n R
hA : A.IsTotallyUnimodular
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
h : (↑1 : R) = ((A.fromRows B).submatrix f g).det
⊢ Membership.mem (γ := Set R) (Set.range SignType.cast) ((A.fromRows B).submatrix f g).det

Tactic:
use 1
-- Module: Mathlib.LinearAlgebra.Matrix.Determinant.TotallyUnimodular
Goal:
m : Type u_1
m' : Type u_2
n : Type u_3
R : Type u_5
inst : CommRing R
inst_1 : DecidableEq n
A : Matrix m n R
B : Matrix m' n R
hA : A.IsTotallyUnimodular
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
⊢ (↑1 : R) = ((A.fromRows B).submatrix f g).det

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Matrix.Determinant.TotallyUnimodular
Goal:
m : Type u_1
m' : Type u_2
n : Type u_3
R : Type u_5
inst : CommRing R
inst_1 : DecidableEq n
A : Matrix m n R
B : Matrix m' n R
hA : A.IsTotallyUnimodular
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
⊢ ∀ (i : m'), ∃ (j : n) (s : SignType), B i = Pi.single (M := fun (j : n) ↦ R) j (↑s : R)

Tactic:
specialize hB ⟨g 0⟩

Premises used: Nonempty.intro, OfNat.ofNat
-- Module: Mathlib.LinearAlgebra.Matrix.Determinant.TotallyUnimodular
Goal:
m : Type u_1
m' : Type u_2
n : Type u_3
R : Type u_5
inst : CommRing R
inst_1 : DecidableEq n
A : Matrix m n R
B : Matrix m' n R
hA : A.IsTotallyUnimodular
k : ℕ
ih :
  ∀ (f : Fin k → m ⊕ m') (g : Fin k → n) (hf : Function.Injective f) (hg : Function.Injective g),
    Membership.mem (γ := Set R) (Set.range SignType.cast) ((A.fromRows B).submatrix f g).det
f : Fin (k + 1) → m ⊕ m'
g : Fin (k + 1) → n
hf : Function.Injective f
hg : Function.Injective g
hB : ∀ (i : m'), ∃ (j : n) (s : SignType), B i = Pi.single (M := fun (j : n) ↦ R) j (↑s : R)
simp_rw : (∀ (x : Fin (k + 1)), ∃ (y : m), f x = Sum.inl y) → ∃ (f' : Fin (k + 1) → m), f = Sum.inl ∘ f'
⊢ (∃ (i : Fin (k + 1)) (j : m'), f i = Sum.inr j) ∨ ∃ (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]

Premises used: Sum.isRight_eq_false, not_exists, Sum.isLeft_iff, Sum.isRight_iff, Classical.or_iff_not_imp_left, Bool.not_eq_true
-- Module: Mathlib.LinearAlgebra.Matrix.Determinant.TotallyUnimodular
Goal:
m : Type u_1
m' : Type u_2
n : Type u_3
R : Type u_5
inst : CommRing R
inst_1 : DecidableEq n
A : Matrix m n R
B : Matrix m' n R
hA : A.IsTotallyUnimodular
k : ℕ
ih :
  ∀ (f : Fin k → m ⊕ m') (g : Fin k → n) (hf : Function.Injective f) (hg : Function.Injective g),
    Membership.mem (γ := Set R) (Set.range SignType.cast) ((A.fromRows B).submatrix f g).det
f : Fin (k + 1) → m ⊕ m'
g : Fin (k + 1) → n
hf : Function.Injective f
hg : Function.Injective g
hB : ∀ (i : m'), ∃ (j : n) (s : SignType), B i = Pi.single (M := fun (j : n) ↦ R) j (↑s : R)
hfr : ∀ (x : Fin (k + 1)), ∃ (y : m), f x = Sum.inl y
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'
⊢ ∃ (f' : Fin (k + 1) → m), f = Sum.inl ∘ f'

Tactic:
choose f' hf' using hfr
-- Module: Mathlib.LinearAlgebra.Matrix.Determinant.TotallyUnimodular
Goal:
m : Type u_1
m' : Type u_2
n : Type u_3
R : Type u_5
inst : CommRing R
inst_1 : DecidableEq n
A : Matrix m n R
B : Matrix m' n R
hA : A.IsTotallyUnimodular
k : ℕ
ih :
  ∀ (f : Fin k → m ⊕ m') (g : Fin k → n) (hf : Function.Injective f) (hg : Function.Injective g),
    Membership.mem (γ := Set R) (Set.range SignType.cast) ((A.fromRows B).submatrix f g).det
f : Fin (k + 1) → m ⊕ m'
g : Fin (k + 1) → n
hf : Function.Injective f
hg : Function.Injective g
hB : ∀ (i : m'), ∃ (j : n) (s : SignType), B i = Pi.single (M := fun (j : n) ↦ R) j (↑s : R)
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:
⟨f', funext hf'⟩

Premises used: funext, Exists.intro
-- Module: Mathlib.LinearAlgebra.Matrix.Determinant.TotallyUnimodular
Goal:
m : Type u_1
m' : Type u_2
n : Type u_3
R : Type u_5
inst : CommRing R
inst_1 : DecidableEq n
A : Matrix m n R
B : Matrix m' n R
hA : A.IsTotallyUnimodular
k : ℕ
ih :
  ∀ (f : Fin k → m ⊕ m') (g : Fin k → n) (hf : Function.Injective f) (hg : Function.Injective g),
    Membership.mem (γ := Set R) (Set.range SignType.cast) ((A.fromRows B).submatrix f g).det
f : Fin (k + 1) → m ⊕ m'
g : Fin (k + 1) → n
hf : Function.Injective f
hg : Function.Injective g
hB : ∀ (i : m'), ∃ (j : n) (s : SignType), B i = Pi.single (M := fun (j : n) ↦ R) j (↑s : R)
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:
exact ⟨f', funext hf'⟩
-- Module: Mathlib.LinearAlgebra.Matrix.Determinant.TotallyUnimodular
Goal:
m : Type u_1
m' : Type u_2
n : Type u_3
R : Type u_5
inst : CommRing R
inst_1 : DecidableEq n
A : Matrix m n R
B : Matrix m' n R
hA : A.IsTotallyUnimodular
k : ℕ
ih :
  ∀ (f : Fin k → m ⊕ m') (g : Fin k → n) (hf : Function.Injective f) (hg : Function.Injective g),
    Membership.mem (γ := Set R) (Set.range SignType.cast) ((A.fromRows B).submatrix f g).det
f : Fin (k + 1) → m ⊕ m'
g : Fin (k + 1) → n
hf : Function.Injective f
hg : Function.Injective g
hB : ∀ (i : m'), ∃ (j : n) (s : SignType), B i = Pi.single (M := fun (j : n) ↦ R) j (↑s : R)
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
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
⊢ 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'⟩

Premises used: Function.comp, Exists, Sum.inl, Sum.inr, Eq, rfl