mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Contraction

Goal state before:
pp: R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
d d' : Module.Dual R M
x : CliffordAlgebra Q
⊢ reverse ((contractLeft d') (reverse (reverse ((contractLeft d) (reverse x))))) =
    -(contractRight ((contractRight x) d')) d

Tactic:
contractRight_eq,

Goal state after:
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
d d' : Module.Dual R M
x : CliffordAlgebra Q
⊢ reverse ((contractLeft d') (reverse (reverse ((contractLeft d) (reverse x))))) =
    -reverse ((contractLeft d) (reverse ((contractRight x) d')))
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Contraction

Goal state before:
pp: R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
d d' : Module.Dual R M
x : CliffordAlgebra Q
⊢ reverse ((contractLeft d') (reverse (reverse ((contractLeft d) (reverse x))))) =
    -reverse ((contractLeft d) (reverse ((contractRight x) d')))

Tactic:
contractRight_eq,

Goal state after:
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
d d' : Module.Dual R M
x : CliffordAlgebra Q
⊢ reverse ((contractLeft d') (reverse (reverse ((contractLeft d) (reverse x))))) =
    -reverse ((contractLeft d) (reverse (reverse ((contractLeft d') (reverse x)))))
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Contraction

Goal state before:
pp: R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q Q' : QuadraticForm R M
B : BilinForm R M
h : BilinMap.toQuadraticMap B = Q' - Q
⊢ (changeForm h) 1 = 1

Tactic:
simpa using

Goal state after:
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q Q' : QuadraticForm R M
B : BilinForm R M
h : BilinMap.toQuadraticMap B = Q' - Q
⊢ (changeForm h) 1 = 1
Module: Mathlib.LinearAlgebra.Transvection.Basic

Goal state before:
pp: R : Type u_3
V : Type u_4
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup V
inst✝³ : Module R V
inst✝² : Free R V
inst✝¹ : Module.Finite R V
inst✝ : IsDomain R
f : Dual R V
v : V
K : Type u_3 := FractionRing R
this✝ : Field K := inferInstance
this : (algebraMap R K) (LinearMap.det (transvection f v)) = ↑1 + ((Dual.baseChange K) f) (↑1 ⊗ₜ[R] v)
⊢ (algebraMap R K) (LinearMap.det (transvection f v)) = (algebraMap R K) (1 + f v)

Tactic:
simpa using

Goal state after:
R : Type u_3
V : Type u_4
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup V
inst✝³ : Module R V
inst✝² : Free R V
inst✝¹ : Module.Finite R V
inst✝ : IsDomain R
f : Dual R V
v : V
K : Type u_3 := FractionRing R
this✝ : Field K := inferInstance
this : (algebraMap R K) (LinearMap.det (transvection f v)) = ↑1 + ((Dual.baseChange K) f) (↑1 ⊗ₜ[R] v)
⊢ LinearMap.det (transvection f v) • 1 = 1 + f v • 1
Module: Mathlib.LinearAlgebra.TensorProduct.Graded.Internal

Goal state before:
pp: R : Type u_1
ι : Type u_2
A : Type u_3
B : Type u_4
inst✝⁸ : CommSemiring ι
inst✝⁷ : DecidableEq ι
inst✝⁶ : CommRing R
inst✝⁵ : Ring A
inst✝⁴ : Ring B
inst✝³ : Algebra R A
inst✝² : Algebra R B
𝒜 : ι → Submodule R A
ℬ : ι → Submodule R B
inst✝¹ : GradedAlgebra 𝒜
inst✝ : GradedAlgebra ℬ
⊢ (auxEquiv R 𝒜 ℬ) 1 = 1

Tactic:
by
  rw [← of_one, Algebra.TensorProduct.one_def, auxEquiv_tmul 𝒜 ℬ, DirectSum.decompose_one,
    DirectSum.decompose_one, Algebra.TensorProduct.one_def]

Goal state after:
Module: Mathlib.LinearAlgebra.CliffordAlgebra.SpinGroup

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
Q : QuadraticForm R M
x : (CliffordAlgebra Q)ˣ
inst✝ : Invertible 2
y z : (CliffordAlgebra Q)ˣ
hx✝ : y ∈ Subgroup.closure (Units.val ⁻¹' Set.range ⇑(ι Q))
hy✝ : z ∈ Subgroup.closure (Units.val ⁻¹' Set.range ⇑(ι Q))
hy : ∀ (m : M), ↑y * (ι Q) m * ↑y⁻¹ ∈ (ι Q).range
hz : ∀ (m : M), ↑z * (ι Q) m * ↑z⁻¹ ∈ (ι Q).range
m : M
this : ↑y * (↑z * (ι Q) m * ↑z⁻¹) * ↑y⁻¹ ∈ ?m.199
⊢ ↑y * ↑z * (ι Q) m * (↑z⁻¹ * ↑y⁻¹) ∈ (ι Q).range

Tactic:
simpa using

Goal state after:
R : Type u_1
inst✝³ : CommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
Q : QuadraticForm R M
x : (CliffordAlgebra Q)ˣ
inst✝ : Invertible 2
y z : (CliffordAlgebra Q)ˣ
hx✝ : y ∈ Subgroup.closure (Units.val ⁻¹' Set.range ⇑(ι Q))
hy✝ : z ∈ Subgroup.closure (Units.val ⁻¹' Set.range ⇑(ι Q))
hy : ∀ (m : M), ↑y * (ι Q) m * ↑y⁻¹ ∈ (ι Q).range
hz : ∀ (m : M), ↑z * (ι Q) m * ↑z⁻¹ ∈ (ι Q).range
m : M
this : ↑y * (↑z * (ι Q) m * ↑z⁻¹) * ↑y⁻¹ ∈ ?m.199
⊢ ↑y * (↑z * ((ι Q) m * (↑z⁻¹ * ↑y⁻¹))) ∈ (ι Q).range
Module: Mathlib.LinearAlgebra.CliffordAlgebra.SpinGroup

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
Q : QuadraticForm R M
inst✝ : Invertible 2
x y z : (CliffordAlgebra Q)ˣ
hx✝ : y ∈ Subgroup.closure (Units.val ⁻¹' Set.range ⇑(ι Q))
hy✝ : z ∈ Subgroup.closure (Units.val ⁻¹' Set.range ⇑(ι Q))
hy : ∀ (b : M), involute ↑y * (ι Q) b * ↑y⁻¹ ∈ (ι Q).range
hz : ∀ (b : M), involute ↑z * (ι Q) b * ↑z⁻¹ ∈ (ι Q).range
b : M
this : involute ↑y * (involute ↑z * (ι Q) b * ↑z⁻¹) * ↑y⁻¹ ∈ ?m.248
⊢ involute ↑y * involute ↑z * (ι Q) b * (↑z⁻¹ * ↑y⁻¹) ∈ (ι Q).range

Tactic:
simpa using

Goal state after:
R : Type u_1
inst✝³ : CommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
Q : QuadraticForm R M
inst✝ : Invertible 2
x y z : (CliffordAlgebra Q)ˣ
hx✝ : y ∈ Subgroup.closure (Units.val ⁻¹' Set.range ⇑(ι Q))
hy✝ : z ∈ Subgroup.closure (Units.val ⁻¹' Set.range ⇑(ι Q))
hy : ∀ (b : M), involute ↑y * (ι Q) b * ↑y⁻¹ ∈ (ι Q).range
hz : ∀ (b : M), involute ↑z * (ι Q) b * ↑z⁻¹ ∈ (ι Q).range
b : M
this : involute ↑y * (involute ↑z * (ι Q) b * ↑z⁻¹) * ↑y⁻¹ ∈ ?m.248
⊢ involute ↑y * (involute ↑z * ((ι Q) b * (↑z⁻¹ * ↑y⁻¹))) ∈ (ι Q).range
Module: Mathlib.LinearAlgebra.Dimension.Torsion.Finite

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Nontrivial R
h : IsTorsion R M
h' : Module.rank R M ≠ 0
⊢ ?m.22

Tactic:
← Cardinal.one_le_iff_ne_zero,

Goal state after:
R : Type u_1
M : Type u_2
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Nontrivial R
h : IsTorsion R M
h'✝ : Module.rank R M ≠ 0
h' : 1 ≤ Module.rank R M
⊢ ?m.22
Module: Mathlib.LinearAlgebra.Dimension.Torsion.Finite

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Nontrivial R
h : IsTorsion R M
h' : Module.rank R M ≠ 0
f : R →ₗ[R] M
hf : Function.Injective ⇑f
⊢ False

Tactic:
simpa using

Goal state after:
R : Type u_1
M : Type u_2
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Nontrivial R
h : IsTorsion R M
h' : Module.rank R M ≠ 0
f : R →ₗ[R] M
hf : Function.Injective ⇑f
⊢ False
Module: Mathlib.LinearAlgebra.ExteriorAlgebra.Basis

Goal state before:
pp: R : Type u_1
M : Type u_2
m n : ℕ
I : Type u_3
inst✝³ : LinearOrder I
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
b : Basis I R M
s : ↑(powersetCard I m)
t : ↑(powersetCard I n)
h : ¬Disjoint ↑s ↑t
⊢ b.ExteriorAlgebra ↑s * b.ExteriorAlgebra ↑t = 0

Tactic:
simpa using

Goal state after:
R : Type u_1
M : Type u_2
m n : ℕ
I : Type u_3
inst✝³ : LinearOrder I
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
b : Basis I R M
s : ↑(powersetCard I m)
t : ↑(powersetCard I n)
h : ¬Disjoint ↑s ↑t
⊢ ιMulti_family R m (⇑b) s * ιMulti_family R n (⇑b) t = 0
Module: Mathlib.LinearAlgebra.ExteriorAlgebra.Basis

Goal state before:
pp: R : Type u_1
M : Type u_2
m n : ℕ
I : Type u_3
inst✝³ : LinearOrder I
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
b : Basis I R M
s : ↑(powersetCard I m)
t : ↑(powersetCard I n)
h : Disjoint ↑s ↑t
⊢ b.ExteriorAlgebra ↑s * b.ExteriorAlgebra ↑t = Equiv.Perm.sign (permOfDisjoint h) • b.ExteriorAlgebra ↑(disjUnion h)

Tactic:
simpa using

Goal state after:
R : Type u_1
M : Type u_2
m n : ℕ
I : Type u_3
inst✝³ : LinearOrder I
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
b : Basis I R M
s : ↑(powersetCard I m)
t : ↑(powersetCard I n)
h : Disjoint ↑s ↑t
⊢ ιMulti_family R m (⇑b) s * ιMulti_family R n (⇑b) t =
    Equiv.Perm.sign (permOfDisjoint h) • ιMulti_family R (m + n) (⇑b) (disjUnion h)
Module: Mathlib.LinearAlgebra.ExteriorAlgebra.Grading

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
m : M
⊢ (ι R) m ∈ ⋀[R]^1 M

Tactic:
simpa using

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
m : M
⊢ (ι R) m ∈ (ι R).range
Module: Mathlib.LinearAlgebra.FreeModule.ModN

Goal state before:
pp: G : Type u_1
H : Type u_2
M : Type u_3
inst✝¹ : AddCommGroup G
n : ℕ
inst✝ : AddMonoid M
φ : { φ // ∀ (g : G), n • φ g = 0 }
g : G
⊢ ((LinearMap.lsmul ℤ G) ↑n) g ∈ (↑φ).ker

Tactic:
simpa using

Goal state after:
G : Type u_1
H : Type u_2
M : Type u_3
inst✝¹ : AddCommGroup G
n : ℕ
inst✝ : AddMonoid M
φ : { φ // ∀ (g : G), n • φ g = 0 }
g : G
⊢ n • ↑φ g = 0
Module: Mathlib.LinearAlgebra.FreeProduct.Basic

Goal state before:
pp: I : Type u
inst✝⁵ : DecidableEq I
i : I
R : Type v
inst✝⁴ : CommSemiring R
A : I → Type w
inst✝³ : (i : I) → Semiring (A i)
inst✝² : (i : I) → Algebra R (A i)
B : Type w'
inst✝¹ : Semiring B
inst✝ : Algebra R B
maps : {i : I} → A i →ₐ[R] B
⊢ ((lift R A) fun {i} ↦ maps) ∘ₐ ι R A i = maps

Tactic:
ext a
  simp [lift_apply, ι, ← ι_apply]

Goal state after:
Module: Mathlib.LinearAlgebra.Goursat

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
L : Submodule R (M × N)
M' : Submodule R M := map (LinearMap.fst R M N) L
N' : Submodule R N := map (LinearMap.snd R M N) L
P : ↥L →ₗ[R] ↥M' := (LinearMap.fst R M N).submoduleMap L
Q : ↥L →ₗ[R] ↥N' := (LinearMap.snd R M N).submoduleMap L
L' : Submodule R (↥M' × ↥N') := (P.prod Q).range
⊢ map (LinearMap.fst R ↥M' ↥N') L' = ⊤

Tactic:
simpa using

Goal state after:
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
L : Submodule R (M × N)
M' : Submodule R M := map (LinearMap.fst R M N) L
N' : Submodule R N := map (LinearMap.snd R M N) L
P : ↥L →ₗ[R] ↥M' := (LinearMap.fst R M N).submoduleMap L
Q : ↥L →ₗ[R] ↥N' := (LinearMap.snd R M N).submoduleMap L
L' : Submodule R (↥M' × ↥N') := (P.prod Q).range
⊢ Surjective ⇑P
Module: Mathlib.LinearAlgebra.Goursat

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
L : Submodule R (M × N)
M' : Submodule R M := map (LinearMap.fst R M N) L
N' : Submodule R N := map (LinearMap.snd R M N) L
P : ↥L →ₗ[R] ↥M' := (LinearMap.fst R M N).submoduleMap L
Q : ↥L →ₗ[R] ↥N' := (LinearMap.snd R M N).submoduleMap L
L' : Submodule R (↥M' × ↥N') := (P.prod Q).range
hL₁' : Surjective (Prod.fst ∘ ⇑L'.subtype)
⊢ map (LinearMap.snd R ↥M' ↥N') L' = ⊤

Tactic:
simpa using

Goal state after:
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
L : Submodule R (M × N)
M' : Submodule R M := map (LinearMap.fst R M N) L
N' : Submodule R N := map (LinearMap.snd R M N) L
P : ↥L →ₗ[R] ↥M' := (LinearMap.fst R M N).submoduleMap L
Q : ↥L →ₗ[R] ↥N' := (LinearMap.snd R M N).submoduleMap L
L' : Submodule R (↥M' × ↥N') := (P.prod Q).range
hL₁' : Surjective (Prod.fst ∘ ⇑L'.subtype)
⊢ Surjective ⇑Q
Module: Mathlib.LinearAlgebra.Matrix.CharP

Goal state before:
pp: n : Type u_1
R : Type u_2
inst✝³ : AddMonoidWithOne R
inst✝² : DecidableEq n
inst✝¹ : Nonempty n
p : ℕ
inst✝ : CharP R p
k : ℕ
⊢ ((diagonal fun x ↦ ↑k) = diagonal fun x ↦ 0) ↔ p ∣ k

Tactic:
diagonal_eq_diagonal_iff,

Goal state after:
n : Type u_1
R : Type u_2
inst✝³ : AddMonoidWithOne R
inst✝² : DecidableEq n
inst✝¹ : Nonempty n
p : ℕ
inst✝ : CharP R p
k : ℕ
⊢ (∀ (i : n), ↑k = 0) ↔ p ∣ k
Module: Mathlib.LinearAlgebra.LinearIndependent.BaseChange

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
inst✝⁵ : Finite ι'
R : Type u_3
S : Type u_4
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : FaithfulSMul R S
inst✝ : IsDomain S
v✝ : ι → ι' → R
h : LinearIndependent R v✝
this : IsDomain R
K : Type u_3 := FractionRing R
L : Type u_4 := FractionRing S
v : ι' → R
hv : v ∈ (Pi.algebraMap ι' R K).ker
i : ι'
⊢ v i = 0 i

Tactic:
simpa using

Goal state after:
ι : Type u_1
ι' : Type u_2
inst✝⁵ : Finite ι'
R : Type u_3
S : Type u_4
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : FaithfulSMul R S
inst✝ : IsDomain S
v✝ : ι → ι' → R
h : LinearIndependent R v✝
this : IsDomain R
K : Type u_3 := FractionRing R
L : Type u_4 := FractionRing S
v : ι' → R
hv : v ∈ (Pi.algebraMap ι' R K).ker
i : ι'
⊢ v i = 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✝ : 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
g : ι → R
h : ∀ (i : ι), (if h : ∃ j, f j = i then a h.choose else 0) ∣ g i
i : ι
hj : ∃ j, f j = i
⊢ (if i = f hj.choose then Exists.choose ⋯ * a hj.choose else 0) = g i

Tactic:
by
              simp only [hj.choose_spec, ↓reduceIte]
              rw [mul_comm]
              conv_rhs =>
                rw [← hj.choose_spec, (h (f hj.choose)).choose_spec]
              simp only [EmbeddingLike.apply_eq_iff_eq, exists_eq, ↓reduceDIte, Classical.choose_eq]
              congr!
              · exact hj.choose_spec.symm
              · simp [hj]

Goal state after:
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 ∘ ⇑(Fintype.equivFin ι).symm) (g ∘ ⇑(Fintype.equivFin ι).symm)).det ∈ Set.range SignType.cast
⊢ (A.submatrix f g).det ∈ Set.range SignType.cast

Tactic:
rwa [← submatrix_submatrix, det_submatrix_equiv_self] at hA

Goal state after:
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 ∘ ⇑Equiv.ulift) (g ∘ ⇑Equiv.ulift)).det ∈ Set.range SignType.cast
⊢ (A.submatrix f g).det ∈ Set.range SignType.cast

Tactic:
rwa [← submatrix_submatrix, det_submatrix_equiv_self] at hA

Goal state after:
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:
simpa using

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
⊢ ∃ y, ↑y = A i j
Module: Mathlib.LinearAlgebra.Matrix.Determinant.TotallyUnimodular

Goal state before:
pp: 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 : ((reindex em en) A).IsTotallyUnimodular
⊢ A.IsTotallyUnimodular

Tactic:
simpa using

Goal state after:
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 : ((reindex em en) A).IsTotallyUnimodular
⊢ A.IsTotallyUnimodular
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:
simpa using

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
⊢ ∀ (x : n), A i x = 0
Module: Mathlib.LinearAlgebra.Matrix.Echelon.Pivot

Goal state before:
pp: case coe
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
c : n
hc : l i = ↑c
⊢ ↑c = ⊤ ↔ A i = 0

Tactic:
simpa using

Goal state after:
case coe
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
c : n
hc : l i = ↑c
⊢ ¬A i = 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
h : ¬n = Fintype.card ι
⊢ n ≤ Fintype.card ι

Tactic:
simpa using

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
h : ¬n = Fintype.card ι
⊢ n ≤ Fintype.card ι
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
bM : Basis ι ℤ M
bN : Basis (Fin n) ℤ ↥N
f : Fin n ↪ ι
a : Fin n → ℤ
i : Fin n
snf : ↑(bN i) = a i • bM (f i)
hi : a i = 0
⊢ bN i = 0

Tactic:
simpa using

Goal state after:
ι : Type u_1
M : Type u_3
n : ℕ
inst✝¹ : AddCommGroup M
inst✝ : Fintype ι
N : Submodule ℤ M
bM : Basis ι ℤ M
bN : Basis (Fin n) ℤ ↥N
f : Fin n ↪ ι
a : Fin n → ℤ
i : Fin n
snf : ↑(bN i) = a i • bM (f i)
hi : a i = 0
⊢ bN i = 0
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
bM : Basis ι ℤ M
bN : Basis (Fin n) ℤ ↥N
f : Fin n ↪ ι
a : Fin n → ℤ
snf : ∀ (i : Fin n), ↑(bN i) = a i • bM (f i)
ha : ∀ (i : Fin n), a i ≠ 0
h : n = Fintype.card ι
⊢ ¬∏ x, (Submodule.toAddSubgroup (Ideal.span {a x})).index = 0

Tactic:
simpa using

Goal state after:
ι : Type u_1
M : Type u_3
n : ℕ
inst✝¹ : AddCommGroup M
inst✝ : Fintype ι
N : Submodule ℤ M
bM : Basis ι ℤ M
bN : Basis (Fin n) ℤ ↥N
f : Fin n ↪ ι
a : Fin n → ℤ
snf : ∀ (i : Fin n), ↑(bN i) = a i • bM (f i)
ha : ∀ (i : Fin n), a i ≠ 0
h : n = Fintype.card ι
⊢ ∀ (x : Fin n), ¬a x = 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 : ∀ (i : Fin (n + 1)), i ≠ i₀ → ∑ j, M i j = 0
⊢ ∀ (j : Fin (n + 1)), j ≠ i₀ → ∑ i, Mᵀ i j = 0

Tactic:
simpa using

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
⊢ ∀ (j : Fin (n + 1)), ¬j = i₀ → ∑ i, M j i = 0
Module: Mathlib.LinearAlgebra.FreeModule.Int

Goal state before:
pp: case refine_2
ι : Type u_1
inst✝ : Finite ι
N : Submodule ℤ (ι → ℤ)
n : ℕ
this : Fintype ι
bN : Module.Basis (Fin n) ℤ ↥N
x✝ : Nonempty (↥N ≃ₗ[ℤ] ι → ℤ)
e : ↥N ≃ₗ[ℤ] ι → ℤ
hc : Fintype.card (Fin n) = Fintype.card ι
⊢ n = Fintype.card ι

Tactic:
simpa using

Goal state after:
case refine_2
ι : Type u_1
inst✝ : Finite ι
N : Submodule ℤ (ι → ℤ)
n : ℕ
this : Fintype ι
bN : Module.Basis (Fin n) ℤ ↥N
x✝ : Nonempty (↥N ≃ₗ[ℤ] ι → ℤ)
e : ↥N ≃ₗ[ℤ] ι → ℤ
hc : Fintype.card (Fin n) = Fintype.card ι
⊢ n = Fintype.card ι
Module: Mathlib.LinearAlgebra.Matrix.Determinant.TotallyUnimodular

Goal state before:
pp: case h
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
j' : n
s : SignType
hj' : B j = Pi.single j' ↑s
hAB :
  ((A.fromRows B).submatrix f g).det =
    ∑ x,
      (-1) ^ (↑i + ↑x) * Pi.single j' (↑s) (g x) *
        (((A.fromRows B).submatrix f g).submatrix i.succAbove x.succAbove).det
hj'' : ∀ (x : Fin (k + 1)), ¬g x = j'
⊢ ↑0 = ((A.fromRows B).submatrix f g).det

Tactic:
simpa using

Goal state after:
case h
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
j' : n
s : SignType
hj' : B j = Pi.single j' ↑s
hAB :
  ((A.fromRows B).submatrix f g).det =
    ∑ x,
      (-1) ^ (↑i + ↑x) * Pi.single j' (↑s) (g x) *
        (((A.fromRows B).submatrix f g).submatrix i.succAbove x.succAbove).det
hj'' : ∀ (x : Fin (k + 1)), ¬g x = j'
⊢ 0 = ((A.fromRows B).submatrix f g).det
Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Card

Goal state before:
pp: case zero
K : Type u_1
V : Type u_2
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : Module K V
inst✝¹ : Fintype K
inst✝ : Finite V
hk : 0 ≤ n
this : Unique { s // ⊤ = ⊥ }
⊢ card { s // (Finsupp.linearCombination K s).ker = ⊥ } = ∏ i, (q ^ n - q ^ ↑i)

Tactic:
Finsupp.linearCombination_fin_zero,

Goal state after:
case zero
K : Type u_1
V : Type u_2
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : Module K V
inst✝¹ : Fintype K
inst✝ : Finite V
hk : 0 ≤ n
this : Unique { s // ⊤ = ⊥ }
⊢ card { s // ker 0 = ⊥ } = ∏ i, (q ^ n - q ^ ↑i)
Module: Mathlib.LinearAlgebra.Matrix.FixedDetMatrices

Goal state before:
pp: m : ℤ
A : FixedDetMatrix (Fin 2) ℤ m
ha : ↑A 1 0 = 0
⊢ ↑A 0 0 * ↑A 1 1 = m

Tactic:
simpa using

Goal state after:
m : ℤ
A : FixedDetMatrix (Fin 2) ℤ m
ha : ↑A 1 0 = 0
⊢ ↑A 0 0 * ↑A 1 1 = m
Module: Mathlib.LinearAlgebra.Matrix.Integer

Goal state before:
pp: m : Type u_1
n : Type u_2
inst✝¹ : Fintype m
inst✝ : Fintype n
A : Matrix m n ℚ
x✝ : ℕ
⊢ Aᵀ.den ∣ x✝ ↔ A.den ∣ x✝

Tactic:
simpa using

Goal state after:
m : Type u_1
n : Type u_2
inst✝¹ : Fintype m
inst✝ : Fintype n
A : Matrix m n ℚ
x✝ : ℕ
⊢ (∀ (i : n) (j : m), (A j i).den ∣ x✝) ↔ ∀ (i : m) (j : n), (A i j).den ∣ x✝
Module: Mathlib.LinearAlgebra.Matrix.Integer

Goal state before:
pp: m : Type u_1
inst✝¹ : Fintype m
inst✝ : DecidableEq m
a : ℕ
⊢ (↑a).den = 1

Tactic:
simpa using

Goal state after:
m : Type u_1
inst✝¹ : Fintype m
inst✝ : DecidableEq m
a : ℕ
⊢ (diagonal fun x ↦ ↑a).den = 1
Module: Mathlib.LinearAlgebra.Matrix.Integer

Goal state before:
pp: m : Type u_1
inst✝¹ : Fintype m
inst✝ : DecidableEq m
a : ℕ
⊢ (↑a).num = ↑a

Tactic:
simpa using

Goal state after:
m : Type u_1
inst✝¹ : Fintype m
inst✝ : DecidableEq m
a : ℕ
⊢ (diagonal fun x ↦ ↑a).num = diagonal fun x ↦ ↑a
Module: Mathlib.LinearAlgebra.Matrix.Integer

Goal state before:
pp: m : Type u_1
inst✝¹ : Fintype m
inst✝ : DecidableEq m
a : ℤ
⊢ (↑a).den = 1

Tactic:
simpa using

Goal state after:
m : Type u_1
inst✝¹ : Fintype m
inst✝ : DecidableEq m
a : ℤ
⊢ (diagonal fun x ↦ ↑a).den = 1
Module: Mathlib.LinearAlgebra.Matrix.Integer

Goal state before:
pp: m : Type u_1
inst✝¹ : Fintype m
inst✝ : DecidableEq m
a : ℤ
⊢ (↑a).num = ↑a

Tactic:
simpa using

Goal state after:
m : Type u_1
inst✝¹ : Fintype m
inst✝ : DecidableEq m
a : ℤ
⊢ (diagonal fun x ↦ ↑a).num = diagonal fun x ↦ a