awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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)
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'
h : (↑0 : 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 0
-- 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)
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'
⊢ (↑0 : R) = ((A.fromRows B).submatrix f g).det

Tactic:
simpa [hj''] using hAB.symm

Premises used: Eq.symm
-- 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
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')
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
⊢ Membership.mem (γ := Set R) (Set.range SignType.cast) ((A.fromRows B).submatrix (Sum.inl ∘ f') g).det

Tactic:
rw [isTotallyUnimodular_iff] at hA

Premises used: Matrix.isTotallyUnimodular_iff
-- 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 :
  ∀ (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:
apply hA
-- 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 : ℕ
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
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
⊢ 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

Premises used: Matrix.isTotallyUnimodular_iff, SignType.castHom, Function.comp, Exists, not_exists, Pi.single_eq_of_ne, Sum.inl, Matrix.fromRows_apply_inr, MonoidWithZeroHom.toMonoidHom, Sum.inr, pow_mem, MonoidHom.mrange, Matrix.submatrix_apply, Pi.single_eq_same, Eq, Matrix.zero, rfl
-- 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
hB : Nonempty n → ∀ (i : m'), ∃ (j : n) (s : SignType), B i = Pi.single (M := fun (j : n) ↦ R) j (↑s : R)
⊢ (A.fromRows B).IsTotallyUnimodular ↔ A.IsTotallyUnimodular

Tactic:
⟨.submatrix Sum.inl id, fun hA => hA.fromRows_unitlike hB⟩

Premises used: Matrix.IsTotallyUnimodular.fromRows_unitlike, id, Sum.inl, Iff.intro, Matrix.IsTotallyUnimodular.submatrix
-- Module: Mathlib.LinearAlgebra.Matrix.Determinant.TotallyUnimodular
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
h : Nonempty n
i j : n
⊢ Eq.{u_5 + 1} (α := R) (1 i j : R) (Pi.single (M := fun (j : n) ↦ R) i (↑1 : R) j : R)

Tactic:
simp [one_apply, Pi.single_apply, eq_comm]

Premises used: Matrix.one_apply, Pi.single_apply, eq_comm
-- Module: Mathlib.LinearAlgebra.Matrix.Determinant.TotallyUnimodular
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
⊢ 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:
aesop
-- Module: Mathlib.LinearAlgebra.Matrix.Determinant.TotallyUnimodular
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
⊢ 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
-- Module: Mathlib.LinearAlgebra.Matrix.Determinant.TotallyUnimodular
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
rw₂ rw₃ : A.IsTotallyUnimodular ↔ A.IsTotallyUnimodular
⊢ IsTotallyUnimodular (m := n ⊕ m) (fromRows 1 A) ↔ A.IsTotallyUnimodular

Tactic:
rw [hA, reindex_isTotallyUnimodular, fromRows_one_isTotallyUnimodular_iff]

Premises used: Matrix.reindex_isTotallyUnimodular, Matrix.fromRows_one_isTotallyUnimodular_iff
-- Module: Mathlib.LinearAlgebra.Matrix.Determinant.TotallyUnimodular
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
rw₂ : IsTotallyUnimodular (m := n ⊕ m) (Aᵀ.fromRows 1) ↔ A.IsTotallyUnimodular
rw₃ : Aᵀ.IsTotallyUnimodular ↔ A.IsTotallyUnimodular
rw₄ rw₅ : A.IsTotallyUnimodular ↔ A.IsTotallyUnimodular
⊢ IsTotallyUnimodular (n := n ⊕ m) (A.fromCols 1) ↔ A.IsTotallyUnimodular

Tactic:
rw [← transpose_isTotallyUnimodular_iff, transpose_fromCols, transpose_one,
    fromRows_one_isTotallyUnimodular_iff, transpose_isTotallyUnimodular_iff]

Premises used: Matrix.transpose_isTotallyUnimodular_iff, Matrix.fromRows_one_isTotallyUnimodular_iff, Matrix.transpose_one, Matrix.transpose_fromCols
-- Module: Mathlib.LinearAlgebra.Matrix.Determinant.TotallyUnimodular
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 := m ⊕ n) (fromCols 1 A)ᵀ ↔ A.IsTotallyUnimodular
rw₁ : IsTotallyUnimodular (m := m ⊕ n) (fromRows 1ᵀ Aᵀ) ↔ A.IsTotallyUnimodular
rw₂ : IsTotallyUnimodular (m := m ⊕ n) (fromRows 1 Aᵀ) ↔ A.IsTotallyUnimodular
rw₃ : Aᵀ.IsTotallyUnimodular ↔ A.IsTotallyUnimodular
rw₄ rw₅ : A.IsTotallyUnimodular ↔ A.IsTotallyUnimodular
⊢ IsTotallyUnimodular (n := m ⊕ n) (fromCols 1 A) ↔ A.IsTotallyUnimodular

Tactic:
rw [← transpose_isTotallyUnimodular_iff, transpose_fromCols, transpose_one,
    one_fromRows_isTotallyUnimodular_iff, transpose_isTotallyUnimodular_iff]

Premises used: Matrix.one_fromRows_isTotallyUnimodular_iff, Matrix.transpose_isTotallyUnimodular_iff, Matrix.transpose_one, Matrix.transpose_fromCols
-- 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
A : Matrix m n R
⊢ (A.fromRows (replicateRow m' 0)).IsTotallyUnimodular ↔ A.IsTotallyUnimodular

Tactic:
fromRows_isTotallyUnimodular_iff_rows <| fun _ _ => ?_

Premises used: Matrix.fromRows_isTotallyUnimodular_iff_rows
-- 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
A : Matrix m n R
refine :
  Nonempty n →
    ∀ (x : m'),
      ∃ (j : n) (s : SignType), Eq (α := n → R) (replicateRow m' 0 x) (Pi.single (M := fun (j : n) ↦ R) j (↑s : R))
⊢ (A.fromRows (replicateRow m' 0)).IsTotallyUnimodular ↔ A.IsTotallyUnimodular

Tactic:
refine fromRows_isTotallyUnimodular_iff_rows <| fun _ _ => ?_

Premises used: Matrix.fromRows_isTotallyUnimodular_iff_rows
-- 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
A : Matrix m n R
h : Nonempty n
x : m'
inhabit :
  ∀ (inhabited_h : Inhabited n),
    ∃ (j : n) (s : SignType), Eq (α := n → R) (replicateRow m' 0 x) (Pi.single (M := fun (j : n) ↦ R) j (↑s : R))
⊢ ∃ (j : n) (s : SignType), Eq (α := n → R) (replicateRow m' 0 x) (Pi.single (M := fun (j : n) ↦ R) j (↑s : R))

Tactic:
inhabit n
-- 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
A : Matrix m n R
h : Nonempty n
x : m'
inhabited_h : Inhabited n
⊢ ∃ (j : n) (s : SignType), Eq (α := n → R) (replicateRow m' 0 x) (Pi.single (M := fun (j : n) ↦ R) j (↑s : R))

Tactic:
⟨default, 0, ?_⟩

Premises used: Inhabited.default, Exists.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
A : Matrix m n R
h : Nonempty n
x : m'
inhabited_h : Inhabited n
refine : Eq (α := n → R) (replicateRow m' 0 x) (Pi.single (M := fun (j : n) ↦ R) default (↑0 : R))
⊢ ∃ (j : n) (s : SignType), Eq (α := n → R) (replicateRow m' 0 x) (Pi.single (M := fun (j : n) ↦ R) j (↑s : R))

Tactic:
refine ⟨default, 0, ?_⟩
-- 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
A : Matrix m n R
h_1 : Nonempty n
x : m'
inhabited_h : Inhabited n
h :
  ∀ (x_1 : n),
    Eq.{u_5 + 1} (α := R) (replicateRow m' 0 x x_1 : R) (Pi.single (M := fun (j : n) ↦ R) default (↑0 : R) x_1 : R)
⊢ Eq (α := n → R) (replicateRow m' 0 x) (Pi.single (M := fun (j : n) ↦ R) default (↑0 : R))

Tactic:
ext x
-- 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
A : Matrix m n R
h : Nonempty n
x_1 : m'
inhabited_h : Inhabited n
x : n
⊢ Eq.{u_5 + 1} (α := R) (replicateRow m' 0 x_1 x : R) (Pi.single (M := fun (j : n) ↦ R) default (↑0 : R) x : R)

Tactic:
simp [Pi.single_apply]

Premises used: Pi.single_apply
-- 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
A : Matrix m n R
refine :
  Nonempty n →
    ∀ (x : m'),
      ∃ (j : n) (s : SignType), Eq (α := n → R) (replicateRow m' 0 x) (Pi.single (M := fun (j : n) ↦ R) j (↑s : R))
refine₁ :
  Nonempty n →
    ∀ (x : m') (inhabited_h : Inhabited n),
      ∃ (j : n) (s : SignType), Eq (α := n → R) (replicateRow m' 0 x) (Pi.single (M := fun (j : n) ↦ R) j (↑s : R))
refine₂ :
  Nonempty n →
    ∀ (x : m') (inhabited_h : Inhabited n),
      Eq (α := n → R) (replicateRow m' 0 x) (Pi.single (M := fun (j : n) ↦ R) default (↑0 : R))
h :
  Nonempty n →
    ∀ (x : m') (inhabited_h : Inhabited n) (x_1 : n),
      Eq.{u_5 + 1} (α := R) (replicateRow m' 0 x x_1 : R) (Pi.single (M := fun (j : n) ↦ R) default (↑0 : R) x_1 : R)
⊢ (A.fromRows (replicateRow m' 0)).IsTotallyUnimodular ↔ A.IsTotallyUnimodular

Tactic:
classical
  refine fromRows_isTotallyUnimodular_iff_rows <| fun _ _ => ?_
  inhabit n
  refine ⟨default, 0, ?_⟩
  ext x
  simp [Pi.single_apply]

Premises used: Pi.single_apply, Matrix.fromRows_isTotallyUnimodular_iff_rows
-- Module: Mathlib.LinearAlgebra.Matrix.Determinant.TotallyUnimodular
Goal:
m : Type u_1
n : Type u_3
n' : Type u_4
R : Type u_5
inst : CommRing R
A : Matrix m n R
rw : (A.fromCols (replicateCol n' 0))ᵀ.IsTotallyUnimodular ↔ A.IsTotallyUnimodular
rw₁ : (Aᵀ.fromRows (replicateCol n' 0)ᵀ).IsTotallyUnimodular ↔ A.IsTotallyUnimodular
rw₂ : (Aᵀ.fromRows (replicateRow n' 0)).IsTotallyUnimodular ↔ A.IsTotallyUnimodular
rw₃ : Aᵀ.IsTotallyUnimodular ↔ A.IsTotallyUnimodular
rw₄ rw₅ : A.IsTotallyUnimodular ↔ A.IsTotallyUnimodular
⊢ (A.fromCols (replicateCol n' 0)).IsTotallyUnimodular ↔ A.IsTotallyUnimodular

Tactic:
rw [← transpose_isTotallyUnimodular_iff, transpose_fromCols, transpose_replicateCol,
    fromRows_replicateRow0_isTotallyUnimodular_iff, transpose_isTotallyUnimodular_iff]

Premises used: Matrix.transpose_replicateCol, Matrix.transpose_isTotallyUnimodular_iff, Matrix.fromRows_replicateRow0_isTotallyUnimodular_iff, Matrix.transpose_fromCols
-- Module: Mathlib.LinearAlgebra.Matrix.Diagonal
Goal:
n : Type u_1
inst : Fintype n
inst_1 : DecidableEq n
R : Type v
inst_2 : CommSemiring R
i : n
w : n → R
⊢ proj (φ := fun (a : n) ↦ R) i ∘ₗ (toLin' : (a : Matrix n n R) → (n → R) →ₗ[R] n → R) (diagonal w) =
    HSMul.hSMul (β := ((i : n) → R) →ₗ[R] R) (w i) (proj (φ := fun (a : n) ↦ R) i)

Tactic:
LinearMap.ext fun _ => mulVec_diagonal _ _ _

Premises used: LinearMap.ext, Matrix.mulVec_diagonal
-- Module: Mathlib.LinearAlgebra.Matrix.Diagonal
Goal:
n : Type u_1
inst : Fintype n
inst_1 : DecidableEq n
R : Type v
inst_2 : CommSemiring R
w : n → R
i : n
⊢ (toLin' : (a : Matrix n n R) → (n → R) →ₗ[R] n → R) (diagonal w) ∘ₗ LinearMap.single R (fun (x : n) ↦ R) i =
    HSMul.hSMul (β := R →ₗ[R] (i : n) → R) (w i) (LinearMap.single R (fun (x : n) ↦ R) i : R →ₗ[R] (i : n) → R)

Tactic:
LinearMap.ext fun x => (diagonal_mulVec_single w _ _).trans (Pi.single_smul' i (w i) x)

Premises used: LinearMap.ext, Matrix.diagonal_mulVec_single, Pi.single_smul', Eq.trans
-- Module: Mathlib.LinearAlgebra.Matrix.Diagonal
Goal:
n : Type u_1
inst : Fintype n
inst_1 : DecidableEq n
R : Type v
inst_2 : CommSemiring R
w : n → R
⊢ Eq (α := (n → R) →ₗ[R] n → R) ((toLin' : (a : Matrix n n R) → (n → R) →ₗ[R] n → R) (diagonal w) : (n → R) →ₗ[R] n → R)
    (LinearMap.pi (φ := fun (i : n) ↦ R) fun (i : n) ↦
        HSMul.hSMul (β := ((i : n) → R) →ₗ[R] R) (w i) (proj (φ := fun (a : n) ↦ R) i) :
      (n → R) →ₗ[R] (i : n) → R)

Tactic:
LinearMap.ext fun _ => funext fun _ => mulVec_diagonal _ _ _

Premises used: LinearMap.ext, funext, Matrix.mulVec_diagonal
-- Module: Mathlib.LinearAlgebra.Matrix.Diagonal
Goal:
m : Type u_1
inst : Fintype m
K : Type u
inst_1 : Semifield K
inst_2 : DecidableEq m
w : m → K
rw :
  Eq (α := Submodule K (m → K))
    (⨅ (i : m),
      comap (R₂ := K) (M₂ := m → K) (σ₁₂ := RingHom.id K)
        ((toLin' : (a : Matrix m m K) → (m → K) →ₗ[K] m → K) (diagonal w)) (ker (proj (φ := fun (a : m) ↦ K) i)))
    (⨆ (i : m),
      ⨆ (_ : Membership.mem (γ := Set m) {i : m | w i = 0} i), LinearMap.range (LinearMap.single K (fun (x : m) ↦ K) i))
⊢ Eq (α := Submodule K (m → K))
    (ker (R₂ := K) (M₂ := m → K) (τ₁₂ := RingHom.id K)
      ((toLin' : (a : Matrix m m K) → (m → K) →ₗ[K] m → K) (diagonal w)))
    (⨆ (i : m),
      ⨆ (_ : Membership.mem (γ := Set m) {i : m | w i = 0} i), LinearMap.range (LinearMap.single K (fun (x : m) ↦ K) i))

Tactic:
rw [← comap_bot, ← iInf_ker_proj, comap_iInf]

Premises used: LinearMap.iInf_ker_proj, Submodule.comap_iInf, Submodule.comap_bot
-- Module: Mathlib.LinearAlgebra.Matrix.Diagonal
Goal:
m : Type u_1
inst : Fintype m
K : Type u
inst_1 : Semifield K
inst_2 : DecidableEq m
w : m → K
⊢ ∀ (i : m),
    Eq (α := Submodule K (m → K))
      (ker (M₂ := K)
        (proj (φ := fun (a : m) ↦ K) i ∘ₗ (toLin' : (a : Matrix m m K) → (m → K) →ₗ[K] m → K) (diagonal w) :
          (m → K) →ₗ[K] K))
      (comap (R₂ := K) (M₂ := m → K) (σ₁₂ := RingHom.id K)
        ((toLin' : (a : Matrix m m K) → (m → K) →ₗ[K] m → K) (diagonal w)) (ker (proj (φ := fun (a : m) ↦ K) i)))

Tactic:
have := fun i : m => ker_comp (toLin' (diagonal w)) (proj i)
-- Module: Mathlib.LinearAlgebra.Matrix.Diagonal
Goal:
m : Type u_1
inst : Fintype m
K : Type u
inst_1 : Semifield K
inst_2 : DecidableEq m
w : m → K
this :
  ∀ (i : m),
    Eq (α := Submodule K (m → K))
      (ker (M₂ := K)
        (proj (φ := fun (a : m) ↦ K) i ∘ₗ (toLin' : (a : Matrix m m K) → (m → K) →ₗ[K] m → K) (diagonal w) :
          (m → K) →ₗ[K] K))
      (comap (R₂ := K) (M₂ := m → K) (σ₁₂ := RingHom.id K)
        ((toLin' : (a : Matrix m m K) → (m → K) →ₗ[K] m → K) (diagonal w)) (ker (proj (φ := fun (a : m) ↦ K) i)))
simp :
  Eq (α := Submodule K (m → K)) (⨅ (i : m), ⨅ (_ : w i ≠ 0), ker (proj (φ := fun (a : m) ↦ K) i))
    (⨆ (i : m),
      ⨆ (_ : Membership.mem (γ := Set m) {i : m | w i = 0} i), LinearMap.range (LinearMap.single K (fun (x : m) ↦ K) i))
⊢ Eq (α := Submodule K (m → K))
    (⨅ (i : m),
      comap (R₂ := K) (M₂ := m → K) (σ₁₂ := RingHom.id K)
        ((toLin' : (a : Matrix m m K) → (m → K) →ₗ[K] m → K) (diagonal w)) (ker (proj (φ := fun (a : m) ↦ K) i)))
    (⨆ (i : m),
      ⨆ (_ : Membership.mem (γ := Set m) {i : m | w i = 0} i), LinearMap.range (LinearMap.single K (fun (x : m) ↦ K) i))

Tactic:
simp only [← this, proj_diagonal, ker_smul']

Premises used: LinearMap.ker_smul', Matrix.proj_diagonal
-- Module: Mathlib.LinearAlgebra.Matrix.Diagonal
Goal:
m : Type u_1
inst : Fintype m
K : Type u
inst_1 : Semifield K
inst_2 : DecidableEq m
w : m → K
this :
  ∀ (i : m),
    Eq (α := Submodule K (m → K))
      (ker (M₂ := K)
        (proj (φ := fun (a : m) ↦ K) i ∘ₗ (toLin' : (a : Matrix m m K) → (m → K) →ₗ[K] m → K) (diagonal w) :
          (m → K) →ₗ[K] K))
      (comap (R₂ := K) (M₂ := m → K) (σ₁₂ := RingHom.id K)
        ((toLin' : (a : Matrix m m K) → (m → K) →ₗ[K] m → K) (diagonal w)) (ker (proj (φ := fun (a : m) ↦ K) i)))
rw rw₁ : Subset.{u_1} (α := Set m) univ univ
⊢ Subset.{u_1} (α := Set m) univ ({i : m | w i = 0} ∪ {i : m | w i = 0}ᶜ)

Tactic:
rw [Set.union_compl_self]

Premises used: Set.union_compl_self
-- Module: Mathlib.LinearAlgebra.Matrix.Diagonal
Goal:
m : Type u_1
inst : Fintype m
K : Type u
inst_1 : Semifield K
inst_2 : DecidableEq m
w : m → K
this :
  ∀ (i : m),
    Eq (α := Submodule K (m → K))
      (ker (M₂ := K)
        (proj (φ := fun (a : m) ↦ K) i ∘ₗ (toLin' : (a : Matrix m m K) → (m → K) →ₗ[K] m → K) (diagonal w) :
          (m → K) →ₗ[K] K))
      (comap (R₂ := K) (M₂ := m → K) (σ₁₂ := RingHom.id K)
        ((toLin' : (a : Matrix m m K) → (m → K) →ₗ[K] m → K) (diagonal w)) (ker (proj (φ := fun (a : m) ↦ K) i)))
⊢ Subset.{u_1} (α := Set m) univ ({i : m | w i = 0} ∪ {i : m | w i = 0}ᶜ)

Tactic:
have : univ ⊆ { i : m | w i = 0 } ∪ { i : m | w i = 0 }ᶜ := by rw [Set.union_compl_self]
-- Module: Mathlib.LinearAlgebra.Matrix.Diagonal
Goal:
m : Type u_1
inst : Fintype m
K : Type u
inst_1 : Semifield K
inst_2 : DecidableEq m
w : m → K
this_1 :
  ∀ (i : m),
    Eq (α := Submodule K (m → K))
      (ker (M₂ := K)
        (proj (φ := fun (a : m) ↦ K) i ∘ₗ (toLin' : (a : Matrix m m K) → (m → K) →ₗ[K] m → K) (diagonal w) :
          (m → K) →ₗ[K] K))
      (comap (R₂ := K) (M₂ := m → K) (σ₁₂ := RingHom.id K)
        ((toLin' : (a : Matrix m m K) → (m → K) →ₗ[K] m → K) (diagonal w)) (ker (proj (φ := fun (a : m) ↦ K) i)))
this : Subset.{u_1} (α := Set m) univ ({i : m | w i = 0} ∪ {i : m | w i = 0}ᶜ)
⊢ Eq (α := Submodule K (m → K)) (⨅ (i : m), ⨅ (_ : w i ≠ 0), ker (proj (φ := fun (a : m) ↦ K) i))
    (⨆ (i : m),
      ⨆ (_ : Membership.mem (γ := Set m) {i : m | w i = 0} i), LinearMap.range (LinearMap.single K (fun (x : m) ↦ K) i))

Tactic:
(iSup_range_single_eq_iInf_ker_proj K (fun _ : m => K) disjoint_compl_right this
    (Set.toFinite _)).symm

Premises used: Set.Mem, setOf, LinearMap.iSup_range_single_eq_iInf_ker_proj, Set.toFinite, disjoint_compl_right, Eq.symm, Not