mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.FreeModule.Int

Goal state before:
pp: case e_a
ι : Type u_1
R : Type u_2
M : Type u_3
n : ℕ
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Fintype ι
inst✝ : Module R M
N : Submodule R M
bM : Basis ι R M
bN : Basis (Fin n) R ↥N
f : Fin n ↪ ι
a : Fin n → R
snf : ∀ (i : Fin n), ↑(bN i) = a i • bM (f i)
N' : Submodule R (ι → R) := Submodule.map (↑bM.equivFun) N
hN'✝ : N' = Submodule.map (↑bM.equivFun) N
bN' : Basis (Fin n) R ↥N' := bN.map (bM.equivFun.submoduleMap N)
snf' : ∀ (i : Fin n), ↑(bN' i) = Pi.single (f i) (a i)
hNN' : N.toAddSubgroup.index = N'.toAddSubgroup.index
hN' :
  N'.toAddSubgroup =
    AddSubgroup.pi Set.univ fun i ↦ Submodule.toAddSubgroup (Ideal.span {if h : ∃ j, f j = i then a h.choose else 0})
f' : Fin n → ↥{x | ∃ j, f j = x} := fun i ↦ ⟨f i, ⋯⟩
hf' : Function.Injective f'
f'' : Fin n ↪ ↥{x | ∃ j, f j = x} := { toFun := f', inj' := hf' }
hu : Finset.univ = Finset.map f'' Finset.univ
⊢ ∏ x, (Submodule.toAddSubgroup (Ideal.span {a ⋯.choose})).index =
    ∏ i, (Submodule.toAddSubgroup (Ideal.span {a i})).index

Tactic:
]

Goal state after:
case e_a
ι : Type u_1
R : Type u_2
M : Type u_3
n : ℕ
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Fintype ι
inst✝ : Module R M
N : Submodule R M
bM : Basis ι R M
bN : Basis (Fin n) R ↥N
f : Fin n ↪ ι
a : Fin n → R
snf : ∀ (i : Fin n), ↑(bN i) = a i • bM (f i)
N' : Submodule R (ι → R) := Submodule.map (↑bM.equivFun) N
hN'✝ : N' = Submodule.map (↑bM.equivFun) N
bN' : Basis (Fin n) R ↥N' := bN.map (bM.equivFun.submoduleMap N)
snf' : ∀ (i : Fin n), ↑(bN' i) = Pi.single (f i) (a i)
hNN' : N.toAddSubgroup.index = N'.toAddSubgroup.index
hN' :
  N'.toAddSubgroup =
    AddSubgroup.pi Set.univ fun i ↦ Submodule.toAddSubgroup (Ideal.span {if h : ∃ j, f j = i then a h.choose else 0})
f' : Fin n → ↥{x | ∃ j, f j = x} := fun i ↦ ⟨f i, ⋯⟩
hf' : Function.Injective f'
f'' : Fin n ↪ ↥{x | ∃ j, f j = x} := { toFun := f', inj' := hf' }
hu : Finset.univ = Finset.map f'' Finset.univ
⊢ ∏ x, (Submodule.toAddSubgroup (Ideal.span {a ⋯.choose})).index =
    ∏ i, (Submodule.toAddSubgroup (Ideal.span {a i})).index
Module: Mathlib.LinearAlgebra.Matrix.Determinant.TotallyUnimodular

Goal state before:
pp: case mp
m : Type u_1
n : Type u_3
R : Type u_5
inst✝² : CommRing R
A : Matrix m n R
ι : Type w
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
f : ι → m
g : ι → n
hA : (A.submatrix f g).det ∈ Set.range SignType.cast
⊢ (A.submatrix f g).det ∈ Set.range SignType.cast

Tactic:
]

Goal state after:
case mp
m : Type u_1
n : Type u_3
R : Type u_5
inst✝² : CommRing R
A : Matrix m n R
ι : Type w
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
f : ι → m
g : ι → n
hA : (A.submatrix f g).det ∈ Set.range SignType.cast
⊢ (A.submatrix f g).det ∈ Set.range SignType.cast
Module: Mathlib.LinearAlgebra.Matrix.Determinant.Misc

Goal state before:
pp: case succ
R : Type u_1
inst✝ : CommRing R
n : ℕ
M : Matrix (Fin (n + 1)) (Fin n) R
hv : ∑ j, M j = 0
j₁ j₂ : Fin (n + 1)
i : Fin n
h_ind : (M.submatrix i.castSucc.succAbove id).det = (↑↑i.castSucc).negOnePow • (M.submatrix (Fin.succAbove 0) id).det
⊢ ((M.submatrix i.succ.succAbove id).updateRow i (∑ k, -1 • M.submatrix i.succ.succAbove id k)).det =
    (M.submatrix i.castSucc.succAbove id).det

Tactic:
]

Goal state after:
case succ
R : Type u_1
inst✝ : CommRing R
n : ℕ
M : Matrix (Fin (n + 1)) (Fin n) R
hv : ∑ j, M j = 0
j₁ j₂ : Fin (n + 1)
i : Fin n
h_ind : (M.submatrix i.castSucc.succAbove id).det = (↑↑i.castSucc).negOnePow • (M.submatrix (Fin.succAbove 0) id).det
⊢ ((M.submatrix i.succ.succAbove id).updateRow i (∑ k, -1 • M.submatrix i.succ.succAbove id k)).det =
    (M.submatrix i.castSucc.succAbove id).det
Module: Mathlib.LinearAlgebra.Matrix.Determinant.TotallyUnimodular

Goal state before:
pp: case mpr
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 : (A.submatrix f g).det ∈ Set.range SignType.cast
⊢ (A.submatrix f g).det ∈ Set.range SignType.cast

Tactic:
]

Goal state after:
case mpr
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 : (A.submatrix f g).det ∈ Set.range SignType.cast
⊢ (A.submatrix f g).det ∈ Set.range SignType.cast
Module: Mathlib.LinearAlgebra.Matrix.Determinant.TotallyUnimodular

Goal state before:
pp: 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), (A.submatrix f g).det ∈ Set.range SignType.cast
i : m
j : n
⊢ A i j ∈ Set.range SignType.cast

Tactic:
]

Goal state after:
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), (A.submatrix f g).det ∈ Set.range SignType.cast
i : m
j : n
⊢ A i j ∈ Set.range SignType.cast
Module: Mathlib.LinearAlgebra.Matrix.Determinant.TotallyUnimodular

Goal state before:
pp: case h
m : Type u_1
n : Type u_3
R : Type u_5
inst✝¹ : CommRing R
inst✝ : IsEmpty m
A : Matrix m n R
f : Fin 0 → m
g✝ : Fin 0 → n
a✝¹ : Function.Injective f
a✝ : Function.Injective g✝
⊢ 1 = 1

Tactic:
]

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Echelon.Pivot

Goal state before:
pp: m : Type u_1
n : Type u_2
R : Type u_3
inst✝² : Zero R
A : Matrix m n R
l : m → WithTop n
inst✝¹ : LT m
inst✝ : LT n
i : m
c : n
hA : A.IsPivotedBy l
hc : l i = ↑c
j : n
hj : j < c
⊢ ↑j < ↑c

Tactic:
]

Goal state after:
m : Type u_1
n : Type u_2
R : Type u_3
inst✝² : Zero R
A : Matrix m n R
l : m → WithTop n
inst✝¹ : LT m
inst✝ : LT n
i : m
c : n
hA : A.IsPivotedBy l
hc : l i = ↑c
j : n
hj : j < c
⊢ ↑j < ↑c
Module: Mathlib.LinearAlgebra.FreeModule.Int

Goal state before:
pp: case e_a.a
ι : Type u_1
R : Type u_2
M : Type u_3
n : ℕ
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Fintype ι
inst✝ : Module R M
N : Submodule R M
bM : Basis ι R M
bN : Basis (Fin n) R ↥N
f : Fin n ↪ ι
a : Fin n → R
snf : ∀ (i : Fin n), ↑(bN i) = a i • bM (f i)
N' : Submodule R (ι → R) := Submodule.map (↑bM.equivFun) N
hN'✝ : N' = Submodule.map (↑bM.equivFun) N
bN' : Basis (Fin n) R ↥N' := bN.map (bM.equivFun.submoduleMap N)
snf' : ∀ (i : Fin n), ↑(bN' i) = Pi.single (f i) (a i)
hNN' : N.toAddSubgroup.index = N'.toAddSubgroup.index
hN' :
  N'.toAddSubgroup =
    AddSubgroup.pi Set.univ fun i ↦ Submodule.toAddSubgroup (Ideal.span {if h : ∃ j, f j = i then a h.choose else 0})
f' : Fin n → ↥{x | ∃ j, f j = x} := fun i ↦ ⟨f i, ⋯⟩
hf' : Function.Injective f'
f'' : Fin n ↪ ↥{x | ∃ j, f j = x} := { toFun := f', inj' := hf' }
hu : Finset.univ = Finset.map f'' Finset.univ
i : Fin n
a✝ : i ∈ Finset.univ
⊢ f ⋯.choose = f i

Tactic:
]

Goal state after:
case e_a.a
ι : Type u_1
R : Type u_2
M : Type u_3
n : ℕ
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Fintype ι
inst✝ : Module R M
N : Submodule R M
bM : Basis ι R M
bN : Basis (Fin n) R ↥N
f : Fin n ↪ ι
a : Fin n → R
snf : ∀ (i : Fin n), ↑(bN i) = a i • bM (f i)
N' : Submodule R (ι → R) := Submodule.map (↑bM.equivFun) N
hN'✝ : N' = Submodule.map (↑bM.equivFun) N
bN' : Basis (Fin n) R ↥N' := bN.map (bM.equivFun.submoduleMap N)
snf' : ∀ (i : Fin n), ↑(bN' i) = Pi.single (f i) (a i)
hNN' : N.toAddSubgroup.index = N'.toAddSubgroup.index
hN' :
  N'.toAddSubgroup =
    AddSubgroup.pi Set.univ fun i ↦ Submodule.toAddSubgroup (Ideal.span {if h : ∃ j, f j = i then a h.choose else 0})
f' : Fin n → ↥{x | ∃ j, f j = x} := fun i ↦ ⟨f i, ⋯⟩
hf' : Function.Injective f'
f'' : Fin n ↪ ↥{x | ∃ j, f j = x} := { toFun := f', inj' := hf' }
hu : Finset.univ = Finset.map f'' Finset.univ
i : Fin n
a✝ : i ∈ Finset.univ
⊢ f ⋯.choose = f i
Module: Mathlib.LinearAlgebra.Matrix.Determinant.Misc

Goal state before:
pp: case pos
R : Type u_1
inst✝ : CommRing R
n : ℕ
M : Matrix (Fin (n + 1)) (Fin n) R
j₁ j₂ : Fin (n + 1)
i : Fin n
h_ind : (M.submatrix i.castSucc.succAbove id).det = (↑↑i.castSucc).negOnePow • (M.submatrix (Fin.succAbove 0) id).det
a b : Fin n
h : a = i
hv : M i.succ b + ∑ c, M (i.succ.succAbove c) b = 0 b
⊢ -∑ x, M (i.succ.succAbove x) b = M (i.castSucc.succAbove a) b

Tactic:
]

Goal state after:
case pos
R : Type u_1
inst✝ : CommRing R
n : ℕ
M : Matrix (Fin (n + 1)) (Fin n) R
j₁ j₂ : Fin (n + 1)
i : Fin n
h_ind : (M.submatrix i.castSucc.succAbove id).det = (↑↑i.castSucc).negOnePow • (M.submatrix (Fin.succAbove 0) id).det
a b : Fin n
h : a = i
hv : M i.succ b + ∑ c, M (i.succ.succAbove c) b = 0 b
⊢ -∑ x, M (i.succ.succAbove x) b = M (i.castSucc.succAbove a) b
Module: Mathlib.LinearAlgebra.Matrix.Echelon.Pivot

Goal state before:
pp: case top
m : Type u_1
n : Type u_2
R : Type u_3
inst✝² : Zero R
A : Matrix m n R
l : m → WithTop n
inst✝¹ : LT m
inst✝ : LT n
i : m
hA : A.IsPivotedBy l
hc : l i = ⊤
h : ∀ (j : n), ↑j < ⊤ → A i j = 0
⊢ ⊤ = ⊤ ↔ A i = 0

Tactic:
]

Goal state after:
case top
m : Type u_1
n : Type u_2
R : Type u_3
inst✝² : Zero R
A : Matrix m n R
l : m → WithTop n
inst✝¹ : LT m
inst✝ : LT n
i : m
hA : A.IsPivotedBy l
hc : l i = ⊤
h : ∀ (j : n), ↑j < ⊤ → A i j = 0
⊢ ⊤ = ⊤ ↔ A i = 0
Module: Mathlib.LinearAlgebra.Matrix.Determinant.Misc

Goal state before:
pp: case pos
R : Type u_1
inst✝ : CommRing R
n : ℕ
M : Matrix (Fin (n + 1)) (Fin n) R
j₁ j₂ : Fin (n + 1)
i : Fin n
h_ind : (M.submatrix i.castSucc.succAbove id).det = (↑↑i.castSucc).negOnePow • (M.submatrix (Fin.succAbove 0) id).det
a b : Fin n
h : a = i
hv : M i.succ b + ∑ c, M (i.succ.succAbove c) b = 0 b
⊢ M i.succ b + ∑ x, M (i.succ.succAbove x) b = 0

Tactic:
]

Goal state after:
case pos
R : Type u_1
inst✝ : CommRing R
n : ℕ
M : Matrix (Fin (n + 1)) (Fin n) R
j₁ j₂ : Fin (n + 1)
i : Fin n
h_ind : (M.submatrix i.castSucc.succAbove id).det = (↑↑i.castSucc).negOnePow • (M.submatrix (Fin.succAbove 0) id).det
a b : Fin n
h : a = i
hv : M i.succ b + ∑ c, M (i.succ.succAbove c) b = 0 b
⊢ M i.succ b + ∑ x, M (i.succ.succAbove x) b = 0
Module: Mathlib.LinearAlgebra.Matrix.Echelon.Pivot

Goal state before:
pp: case top
m : Type u_1
n : Type u_2
R : Type u_3
inst✝² : Zero R
A : Matrix m n R
l : m → WithTop n
inst✝¹ : LinearOrder n
inst✝ : LT m
l' : m → WithTop n
hl : A.IsPivotedBy l
hl' : A.IsPivotedBy l'
i : m
hc' : l' i = ⊤
⊢ l' i = ⊤

Tactic:
]

Goal state after:
case top
m : Type u_1
n : Type u_2
R : Type u_3
inst✝² : Zero R
A : Matrix m n R
l : m → WithTop n
inst✝¹ : LinearOrder n
inst✝ : LT m
l' : m → WithTop n
hl : A.IsPivotedBy l
hl' : A.IsPivotedBy l'
i : m
hc' : l' i = ⊤
⊢ l' i = ⊤
Module: Mathlib.LinearAlgebra.FreeModule.Int

Goal state before:
pp: case e_a.a
ι : Type u_1
R : Type u_2
M : Type u_3
n : ℕ
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Fintype ι
inst✝ : Module R M
N : Submodule R M
bM : Basis ι R M
bN : Basis (Fin n) R ↥N
f : Fin n ↪ ι
a : Fin n → R
snf : ∀ (i : Fin n), ↑(bN i) = a i • bM (f i)
N' : Submodule R (ι → R) := Submodule.map (↑bM.equivFun) N
hN'✝ : N' = Submodule.map (↑bM.equivFun) N
bN' : Basis (Fin n) R ↥N' := bN.map (bM.equivFun.submoduleMap N)
snf' : ∀ (i : Fin n), ↑(bN' i) = Pi.single (f i) (a i)
hNN' : N.toAddSubgroup.index = N'.toAddSubgroup.index
hN' :
  N'.toAddSubgroup =
    AddSubgroup.pi Set.univ fun i ↦ Submodule.toAddSubgroup (Ideal.span {if h : ∃ j, f j = i then a h.choose else 0})
f' : Fin n → ↥{x | ∃ j, f j = x} := fun i ↦ ⟨f i, ⋯⟩
hf' : Function.Injective f'
f'' : Fin n ↪ ↥{x | ∃ j, f j = x} := { toFun := f', inj' := hf' }
hu : Finset.univ = Finset.map f'' Finset.univ
i : Fin n
a✝ : i ∈ Finset.univ
h : ∃ j, f j = ↑(f'' i)
⊢ ↑(f'' i) = f i

Tactic:
]

Goal state after:
case e_a.a
ι : Type u_1
R : Type u_2
M : Type u_3
n : ℕ
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Fintype ι
inst✝ : Module R M
N : Submodule R M
bM : Basis ι R M
bN : Basis (Fin n) R ↥N
f : Fin n ↪ ι
a : Fin n → R
snf : ∀ (i : Fin n), ↑(bN i) = a i • bM (f i)
N' : Submodule R (ι → R) := Submodule.map (↑bM.equivFun) N
hN'✝ : N' = Submodule.map (↑bM.equivFun) N
bN' : Basis (Fin n) R ↥N' := bN.map (bM.equivFun.submoduleMap N)
snf' : ∀ (i : Fin n), ↑(bN' i) = Pi.single (f i) (a i)
hNN' : N.toAddSubgroup.index = N'.toAddSubgroup.index
hN' :
  N'.toAddSubgroup =
    AddSubgroup.pi Set.univ fun i ↦ Submodule.toAddSubgroup (Ideal.span {if h : ∃ j, f j = i then a h.choose else 0})
f' : Fin n → ↥{x | ∃ j, f j = x} := fun i ↦ ⟨f i, ⋯⟩
hf' : Function.Injective f'
f'' : Fin n ↪ ↥{x | ∃ j, f j = x} := { toFun := f', inj' := hf' }
hu : Finset.univ = Finset.map f'' Finset.univ
i : Fin n
a✝ : i ∈ Finset.univ
h : ∃ j, f j = ↑(f'' i)
⊢ ↑(f'' i) = f i
Module: Mathlib.LinearAlgebra.Matrix.Echelon.Pivot

Goal state before:
pp: case coe.top
m : Type u_1
n : Type u_2
R : Type u_3
inst✝² : Zero R
A : Matrix m n R
l : m → WithTop n
inst✝¹ : LinearOrder n
inst✝ : LT m
l' : m → WithTop n
hl : A.IsPivotedBy l
hl' : A.IsPivotedBy l'
i : m
c' : n
hc' : l' i = ↑c'
hc : A i = 0
⊢ ⊤ = ↑c'

Tactic:
]

Goal state after:
case coe.top
m : Type u_1
n : Type u_2
R : Type u_3
inst✝² : Zero R
A : Matrix m n R
l : m → WithTop n
inst✝¹ : LinearOrder n
inst✝ : LT m
l' : m → WithTop n
hl : A.IsPivotedBy l
hl' : A.IsPivotedBy l'
i : m
c' : n
hc' : l' i = ↑c'
hc : A i = 0
⊢ ⊤ = ↑c'
Module: Mathlib.LinearAlgebra.Matrix.Determinant.Misc

Goal state before:
pp: case neg.inl
R : Type u_1
inst✝ : CommRing R
n : ℕ
M : Matrix (Fin (n + 1)) (Fin n) R
hv : ∑ j, M j = 0
j₁ j₂ : Fin (n + 1)
i : Fin n
h_ind : (M.submatrix i.castSucc.succAbove id).det = (↑↑i.castSucc).negOnePow • (M.submatrix (Fin.succAbove 0) id).det
a b : Fin n
h✝ : ¬a = i
h : a < i
⊢ M a.castSucc b = M a.castSucc b

Tactic:
]

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Determinant.Misc

Goal state before:
pp: case neg.inr
R : Type u_1
inst✝ : CommRing R
n : ℕ
M : Matrix (Fin (n + 1)) (Fin n) R
hv : ∑ j, M j = 0
j₁ j₂ : Fin (n + 1)
i : Fin n
h_ind : (M.submatrix i.castSucc.succAbove id).det = (↑↑i.castSucc).negOnePow • (M.submatrix (Fin.succAbove 0) id).det
a b : Fin n
h✝ : ¬a = i
h : i < a
⊢ M a.succ b = M a.succ b

Tactic:
]

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Determinant.Misc

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
n : ℕ
M : Matrix (Fin n) (Fin (n + 1)) R
hv : ∀ (i : Fin n), ∑ j, M i j = 0
j₁ j₂ : Fin (n + 1)
⊢ (↑↑j₁ - ↑↑j₂).negOnePow • (M.submatrix id j₂.succAbove).det =
    (↑↑j₁ - ↑↑j₂).negOnePow • (M.submatrix id j₂.succAbove).det

pp: R : Type u_1
inst✝ : CommRing R
n : ℕ
M : Matrix (Fin n) (Fin (n + 1)) R
hv : ∀ (i : Fin n), ∑ j, M i j = 0
j₁ j₂ : Fin (n + 1)
⊢ ∑ j, Mᵀ j = 0

Tactic:
]

Goal state after:
R : Type u_1
inst✝ : CommRing R
n : ℕ
M : Matrix (Fin n) (Fin (n + 1)) R
hv : ∀ (i : Fin n), ∑ j, M i j = 0
j₁ j₂ : Fin (n + 1)
⊢ ∑ j, Mᵀ j = 0
Module: Mathlib.LinearAlgebra.FreeModule.Int

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
n : ℕ
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Fintype ι
inst✝¹ : Infinite R
inst✝ : Module R M
N : Submodule R M
snf : SmithNormalForm N ι n
⊢ Nat.card R ^ (Fintype.card ι - n) * ∏ i, (Submodule.toAddSubgroup (Ideal.span {snf.a i})).index =
    if n = Fintype.card ι then ∏ i, (Submodule.toAddSubgroup (Ideal.span {snf.a i})).index else 0

Tactic:
]

Goal state after:
ι : Type u_1
R : Type u_2
M : Type u_3
n : ℕ
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Fintype ι
inst✝¹ : Infinite R
inst✝ : Module R M
N : Submodule R M
snf : SmithNormalForm N ι n
⊢ Nat.card R ^ (Fintype.card ι - n) * ∏ i, (Submodule.toAddSubgroup (Ideal.span {snf.a i})).index =
    if n = Fintype.card ι then ∏ i, (Submodule.toAddSubgroup (Ideal.span {snf.a i})).index else 0
Module: Mathlib.LinearAlgebra.Matrix.Determinant.Misc

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
n : ℕ
M : Matrix (Fin (n + 1)) (Fin (n + 1)) R
i₀ j₀ : Fin (n + 1)
hv : ∀ (j : Fin (n + 1)), j ≠ j₀ → ∑ i, M i j = 0
⊢ ∑ j,
      (-1) ^ (↑i₀ + ↑j) * M.updateRow i₀ (∑ k, 1 • M k) i₀ j *
        ((M.updateRow i₀ (∑ k, 1 • M k)).submatrix i₀.succAbove j.succAbove).det =
    ((-1) ^ (↑i₀ + ↑j₀) * ∑ i, M i j₀) * (M.submatrix i₀.succAbove j₀.succAbove).det

Tactic:
]

Goal state after:
R : Type u_1
inst✝ : CommRing R
n : ℕ
M : Matrix (Fin (n + 1)) (Fin (n + 1)) R
i₀ j₀ : Fin (n + 1)
hv : ∀ (j : Fin (n + 1)), j ≠ j₀ → ∑ i, M i j = 0
⊢ ∑ j,
      (-1) ^ (↑i₀ + ↑j) * M.updateRow i₀ (∑ k, 1 • M k) i₀ j *
        ((M.updateRow i₀ (∑ k, 1 • M k)).submatrix i₀.succAbove j.succAbove).det =
    ((-1) ^ (↑i₀ + ↑j₀) * ∑ i, M i j₀) * (M.submatrix i₀.succAbove j₀.succAbove).det
Module: Mathlib.LinearAlgebra.Matrix.Echelon.Pivot

Goal state before:
pp: case inl
m : Type u_1
n : Type u_2
R : Type u_3
inst✝² : Zero R
A : Matrix m n R
l : m → WithTop n
inst✝¹ : PartialOrder m
inst✝ : LinearOrder n
x✝ :
  Monotone l ∧
    StrictMonoOn l {i | l i ≠ ⊤} ∧ ∀ (i : m), (∀ (j : n), ↑j < l i → A i j = 0) ∧ ∀ (c : n), l i = ↑c → A i c ≠ 0
hmono : Monotone l
hstrict : StrictMonoOn l {i | l i ≠ ⊤}
hlead : ∀ (i : m), (∀ (j : n), ↑j < l i → A i j = 0) ∧ ∀ (c : n), l i = ↑c → A i c ≠ 0
i₁ i₂ : m
hlt : i₁ < i₂
j₂ : n
hz : ∀ j₁ < j₂, A i₁ j₁ = 0
h₂ : l i₂ = ⊤
⊢ ↑j₂ < ⊤

Tactic:
]

Goal state after:
case inl
m : Type u_1
n : Type u_2
R : Type u_3
inst✝² : Zero R
A : Matrix m n R
l : m → WithTop n
inst✝¹ : PartialOrder m
inst✝ : LinearOrder n
x✝ :
  Monotone l ∧
    StrictMonoOn l {i | l i ≠ ⊤} ∧ ∀ (i : m), (∀ (j : n), ↑j < l i → A i j = 0) ∧ ∀ (c : n), l i = ↑c → A i c ≠ 0
hmono : Monotone l
hstrict : StrictMonoOn l {i | l i ≠ ⊤}
hlead : ∀ (i : m), (∀ (j : n), ↑j < l i → A i j = 0) ∧ ∀ (c : n), l i = ↑c → A i c ≠ 0
i₁ i₂ : m
hlt : i₁ < i₂
j₂ : n
hz : ∀ j₁ < j₂, A i₁ j₁ = 0
h₂ : l i₂ = ⊤
⊢ ↑j₂ < ⊤
Module: Mathlib.LinearAlgebra.FreeModule.Int

Goal state before:
pp: ι : Type u_1
M : Type u_3
n : ℕ
inst✝¹ : AddCommGroup M
inst✝ : Fintype ι
N : Submodule ℤ M
snf : SmithNormalForm N ι n
⊢ (if n = Fintype.card ι then ∏ i, (Submodule.toAddSubgroup (Ideal.span {snf.a i})).index else 0) ≠ 0 ↔
    n = Fintype.card ι

Tactic:
]

Goal state after:
ι : Type u_1
M : Type u_3
n : ℕ
inst✝¹ : AddCommGroup M
inst✝ : Fintype ι
N : Submodule ℤ M
snf : SmithNormalForm N ι n
⊢ (if n = Fintype.card ι then ∏ i, (Submodule.toAddSubgroup (Ideal.span {snf.a i})).index else 0) ≠ 0 ↔
    n = Fintype.card ι
Module: Mathlib.LinearAlgebra.Matrix.Determinant.Misc

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
n : ℕ
M : Matrix (Fin (n + 1)) (Fin (n + 1)) R
i₀ j₀ : Fin (n + 1)
hv : ∀ (j : Fin (n + 1)), j ≠ j₀ → ∑ i, M i j = 0
⊢ ((-1) ^ (↑i₀ + ↑j₀) * ∑ c, M c j₀) * (M.submatrix i₀.succAbove j₀.succAbove).det +
      ∑ i, ((-1) ^ (↑i₀ + ↑↑i) * ∑ c, M c ↑i) * (M.submatrix i₀.succAbove (↑i).succAbove).det =
    ((-1) ^ (↑i₀ + ↑j₀) * ∑ i, M i j₀) * (M.submatrix i₀.succAbove j₀.succAbove).det

Tactic:
]

Goal state after:
R : Type u_1
inst✝ : CommRing R
n : ℕ
M : Matrix (Fin (n + 1)) (Fin (n + 1)) R
i₀ j₀ : Fin (n + 1)
hv : ∀ (j : Fin (n + 1)), j ≠ j₀ → ∑ i, M i j = 0
⊢ ((-1) ^ (↑i₀ + ↑j₀) * ∑ c, M c j₀) * (M.submatrix i₀.succAbove j₀.succAbove).det +
      ∑ i, ((-1) ^ (↑i₀ + ↑↑i) * ∑ c, M c ↑i) * (M.submatrix i₀.succAbove (↑i).succAbove).det =
    ((-1) ^ (↑i₀ + ↑j₀) * ∑ i, M i j₀) * (M.submatrix i₀.succAbove j₀.succAbove).det
Module: Mathlib.LinearAlgebra.Matrix.Determinant.TotallyUnimodular

Goal state before:
pp: case pos
m : Type u_1
m' : Type u_2
n : Type u_3
R : Type u_5
inst✝¹ : CommRing R
inst✝ : DecidableEq n
A : Matrix m n R
B : Matrix m' n R
hA : A.IsTotallyUnimodular
hB : ∀ (i : m'), ∃ j s, B i = Pi.single j ↑s
k : ℕ
ih :
  ∀ (f : Fin k → m ⊕ m') (g : Fin k → n),
    Function.Injective f → Function.Injective g → ((A.fromRows B).submatrix f g).det ∈ Set.range SignType.cast
f : Fin (k + 1) → m ⊕ m'
g : Fin (k + 1) → n
hf : Function.Injective f
hg : Function.Injective g
i : Fin (k + 1)
j : m'
hfi : f i = Sum.inr j
s : SignType
x : Fin (k + 1)
hj' : B j = Pi.single (g x) ↑s
hAB :
  ((A.fromRows B).submatrix f g).det =
    (-1) ^ (↑i + ↑x) * ↑s * (((A.fromRows B).submatrix f g).submatrix i.succAbove x.succAbove).det
⊢ (-1) ^ (↑i + ↑x) * ↑s * (((A.fromRows B).submatrix f g).submatrix i.succAbove x.succAbove).det ∈
    Set.range SignType.cast

Tactic:
]

Goal state after:
case pos
m : Type u_1
m' : Type u_2
n : Type u_3
R : Type u_5
inst✝¹ : CommRing R
inst✝ : DecidableEq n
A : Matrix m n R
B : Matrix m' n R
hA : A.IsTotallyUnimodular
hB : ∀ (i : m'), ∃ j s, B i = Pi.single j ↑s
k : ℕ
ih :
  ∀ (f : Fin k → m ⊕ m') (g : Fin k → n),
    Function.Injective f → Function.Injective g → ((A.fromRows B).submatrix f g).det ∈ Set.range SignType.cast
f : Fin (k + 1) → m ⊕ m'
g : Fin (k + 1) → n
hf : Function.Injective f
hg : Function.Injective g
i : Fin (k + 1)
j : m'
hfi : f i = Sum.inr j
s : SignType
x : Fin (k + 1)
hj' : B j = Pi.single (g x) ↑s
hAB :
  ((A.fromRows B).submatrix f g).det =
    (-1) ^ (↑i + ↑x) * ↑s * (((A.fromRows B).submatrix f g).submatrix i.succAbove x.succAbove).det
⊢ (-1) ^ (↑i + ↑x) * ↑s * (((A.fromRows B).submatrix f g).submatrix i.succAbove x.succAbove).det ∈
    Set.range SignType.cast
Module: Mathlib.LinearAlgebra.Matrix.Echelon.Pivot

Goal state before:
pp: m : Type u_1
n : Type u_2
R : Type u_3
inst✝² : Zero R
A : Matrix m n R
l : m → WithTop n
inst✝¹ : PartialOrder m
inst✝ : LinearOrder n
⊢ (Monotone l ∧
      StrictMonoOn l {i | l i ≠ ⊤} ∧ ∀ (i : m), (∀ (j : n), ↑j < l i → A i j = 0) ∧ ∀ (c : n), l i = ↑c → A i c ≠ 0) ↔
    Monotone l ∧ StrictMonoOn l {i | l i ≠ ⊤} ∧ ∀ (i : m), l i = ⊤ ∧ A i = 0 ∨ ∃ c, l i = ↑c ∧ A.IsLeadingEntry i c

Tactic:
]

Goal state after:
m : Type u_1
n : Type u_2
R : Type u_3
inst✝² : Zero R
A : Matrix m n R
l : m → WithTop n
inst✝¹ : PartialOrder m
inst✝ : LinearOrder n
⊢ (Monotone l ∧
      StrictMonoOn l {i | l i ≠ ⊤} ∧ ∀ (i : m), (∀ (j : n), ↑j < l i → A i j = 0) ∧ ∀ (c : n), l i = ↑c → A i c ≠ 0) ↔
    Monotone l ∧ StrictMonoOn l {i | l i ≠ ⊤} ∧ ∀ (i : m), l i = ⊤ ∧ A i = 0 ∨ ∃ c, l i = ↑c ∧ A.IsLeadingEntry i c
Module: Mathlib.LinearAlgebra.FreeModule.Int

Goal state before:
pp: ι : Type u_1
inst✝ : Finite ι
N : Submodule ℤ (ι → ℤ)
n : ℕ
snf : Module.Basis.SmithNormalForm N ι n
this : Fintype ι
⊢ n = Fintype.card ι ↔ Nonempty (↥N ≃ₗ[ℤ] ι → ℤ)

Tactic:
]

Goal state after:
ι : Type u_1
inst✝ : Finite ι
N : Submodule ℤ (ι → ℤ)
n : ℕ
snf : Module.Basis.SmithNormalForm N ι n
this : Fintype ι
⊢ n = Fintype.card ι ↔ Nonempty (↥N ≃ₗ[ℤ] ι → ℤ)
Module: Mathlib.LinearAlgebra.Matrix.Determinant.Misc

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
n : ℕ
M : Matrix (Fin (n + 1)) (Fin (n + 1)) R
i₀ j₀ : Fin (n + 1)
hv : ∀ (i : Fin (n + 1)), i ≠ i₀ → ∑ j, M i j = 0
⊢ ((-1) ^ (↑i₀ + ↑j₀) * ∑ i, Mᵀ i i₀) * (M.submatrix i₀.succAbove j₀.succAbove).det =
    ((-1) ^ (↑i₀ + ↑j₀) * ∑ j, M i₀ j) * (M.submatrix i₀.succAbove j₀.succAbove).det

Tactic:
]

Goal state after:
R : Type u_1
inst✝ : CommRing R
n : ℕ
M : Matrix (Fin (n + 1)) (Fin (n + 1)) R
i₀ j₀ : Fin (n + 1)
hv : ∀ (i : Fin (n + 1)), i ≠ i₀ → ∑ j, M i j = 0
⊢ ((-1) ^ (↑i₀ + ↑j₀) * ∑ i, Mᵀ i i₀) * (M.submatrix i₀.succAbove j₀.succAbove).det =
    ((-1) ^ (↑i₀ + ↑j₀) * ∑ j, M i₀ j) * (M.submatrix i₀.succAbove j₀.succAbove).det
Module: Mathlib.LinearAlgebra.Matrix.Echelon.Decomposition

Goal state before:
pp: m : Type u_1
inst✝⁵ : Fintype m
inst✝⁴ : LinearOrder m
n : Type u_2
inst✝³ : Fintype n
inst✝² : LinearOrder n
R : Type u_3
inst✝¹ : CommRing R
inst✝ : IsDomain R
A : Matrix m n R
cert : Decomposition A
⊢ A.rank = (A.submatrix (⇑cert.σ) id).rank

Tactic:
]

Goal state after:
m : Type u_1
inst✝⁵ : Fintype m
inst✝⁴ : LinearOrder m
n : Type u_2
inst✝³ : Fintype n
inst✝² : LinearOrder n
R : Type u_3
inst✝¹ : CommRing R
inst✝ : IsDomain R
A : Matrix m n R
cert : Decomposition A
⊢ A.rank = (A.submatrix (⇑cert.σ) id).rank