mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.Alternating.DomCoprod

Goal state before:
pp: ιa : Type u_1
ιb : Type u_2
inst✝¹⁰ : Fintype ιa
inst✝⁹ : Fintype ιb
R' : Type u_3
Mᵢ : Type u_4
N₁ : Type u_5
N₂ : Type u_6
inst✝⁸ : CommSemiring R'
inst✝⁷ : AddCommGroup N₁
inst✝⁶ : Module R' N₁
inst✝⁵ : AddCommGroup N₂
inst✝⁴ : Module R' N₂
inst✝³ : AddCommMonoid Mᵢ
inst✝² : Module R' Mᵢ
inst✝¹ : DecidableEq ιa
inst✝ : DecidableEq ιb
a : MultilinearMap R' (fun x ↦ Mᵢ) N₁
b : MultilinearMap R' (fun x ↦ Mᵢ) N₂
⊢ domCoprod' ((∑ σ, Perm.sign σ • domDomCongr σ a) ⊗ₜ[R'] ∑ σ, Perm.sign σ • domDomCongr σ b) =
    ∑ σa, ∑ σb, Perm.sign σa • Perm.sign σb • domCoprod' (domDomCongr σa a ⊗ₜ[R'] domDomCongr σb b)

Tactic:
TensorProduct.sum_tmul,

Goal state after:
ιa : Type u_1
ιb : Type u_2
inst✝¹⁰ : Fintype ιa
inst✝⁹ : Fintype ιb
R' : Type u_3
Mᵢ : Type u_4
N₁ : Type u_5
N₂ : Type u_6
inst✝⁸ : CommSemiring R'
inst✝⁷ : AddCommGroup N₁
inst✝⁶ : Module R' N₁
inst✝⁵ : AddCommGroup N₂
inst✝⁴ : Module R' N₂
inst✝³ : AddCommMonoid Mᵢ
inst✝² : Module R' Mᵢ
inst✝¹ : DecidableEq ιa
inst✝ : DecidableEq ιb
a : MultilinearMap R' (fun x ↦ Mᵢ) N₁
b : MultilinearMap R' (fun x ↦ Mᵢ) N₂
⊢ domCoprod' (∑ a_1, (Perm.sign a_1 • domDomCongr a_1 a) ⊗ₜ[R'] ∑ σ, Perm.sign σ • domDomCongr σ b) =
    ∑ σa, ∑ σb, Perm.sign σa • Perm.sign σb • domCoprod' (domDomCongr σa a ⊗ₜ[R'] domDomCongr σb b)
Module: Mathlib.LinearAlgebra.FixedSubmodule

Goal state before:
pp: R✝ : Type u_1
inst✝⁷ : Semiring R✝
U : Type u_2
V✝ : Type u_3
inst✝⁶ : AddCommMonoid U
inst✝⁵ : AddCommMonoid V✝
inst✝⁴ : Module R✝ U
inst✝³ : Module R✝ V✝
e : V✝ ≃ₗ[R✝] V✝
P : Submodule R✝ U
Q : Submodule R✝ V✝
R : Type u_4
V : Type u_5
inst✝² : Ring R
inst✝¹ : AddCommGroup V
inst✝ : Module R V
W : Submodule R V
u v : ↥(stabilizer (V ≃ₗ[R] V) W)
⊢ Quotient.equiv W W ↑(u * v) ⋯ = Quotient.equiv W W ↑u ⋯ * Quotient.equiv W W ↑v ⋯

Tactic:
ext x

Goal state after:
R✝ : Type u_1
inst✝⁷ : Semiring R✝
U : Type u_2
V✝ : Type u_3
inst✝⁶ : AddCommMonoid U
inst✝⁵ : AddCommMonoid V✝
inst✝⁴ : Module R✝ U
inst✝³ : Module R✝ V✝
e : V✝ ≃ₗ[R✝] V✝
P : Submodule R✝ U
Q : Submodule R✝ V✝
R : Type u_4
V : Type u_5
inst✝² : Ring R
inst✝¹ : AddCommGroup V
inst✝ : Module R V
W : Submodule R V
u v : ↥(stabilizer (V ≃ₗ[R] V) W)
x : V ⧸ W
⊢ (Quotient.equiv W W ↑(u * v) ⋯) x = (Quotient.equiv W W ↑u ⋯ * Quotient.equiv W W ↑v ⋯) x
Module: Mathlib.LinearAlgebra.Center

Goal state before:
pp: case inl
R : Type u_1
V : Type u_2
inst✝³ : Ring R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
ι : Type u_3
inst✝ : Nontrivial ι
b : Basis ι R V
f : V →ₗ[R] V
hcomm : ∀ (i j : ι) (r : R), i ≠ j → Commute f ((b.coord i).transvection (r • b j))
hV : Subsingleton V
⊢ f = ⟨1, ⋯⟩ • 1

Tactic:
ext x

Goal state after:
case inl
R : Type u_1
V : Type u_2
inst✝³ : Ring R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
ι : Type u_3
inst✝ : Nontrivial ι
b : Basis ι R V
f : V →ₗ[R] V
hcomm : ∀ (i j : ι) (r : R), i ≠ j → Commute f ((b.coord i).transvection (r • b j))
hV : Subsingleton V
x : V
⊢ f x = (⟨1, ⋯⟩ • 1) x
Module: Mathlib.LinearAlgebra.Center

Goal state before:
pp: case inr
R : Type u_1
V : Type u_2
inst✝³ : Ring R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
ι : Type u_3
inst✝ : Nontrivial ι
b : Basis ι R V
f : V →ₗ[R] V
hV : Nontrivial V
h_allEq : ∀ (i j : ι), (b.coord i) (f (b i)) = (b.coord j) (f (b j))
hcomm : ∀ (i : ι) (r : R), r • f (b i) = (b.coord i) (f (b i)) • r • b i
i : ι := Classical.ofNonempty
⊢ f = ⟨(b.coord i) (f (b i)), ⋯⟩ • 1

Tactic:
ext x

Goal state after:
case inr
R : Type u_1
V : Type u_2
inst✝³ : Ring R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
ι : Type u_3
inst✝ : Nontrivial ι
b : Basis ι R V
f : V →ₗ[R] V
hV : Nontrivial V
h_allEq : ∀ (i j : ι), (b.coord i) (f (b i)) = (b.coord j) (f (b j))
hcomm : ∀ (i : ι) (r : R), r • f (b i) = (b.coord i) (f (b i)) • r • b i
i : ι := Classical.ofNonempty
x : V
⊢ f x = (⟨(b.coord i) (f (b i)), ⋯⟩ • 1) x
Module: Mathlib.LinearAlgebra.Transvection.Basic

Goal state before:
pp: R : Type u_1
V : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid V
inst✝ : Module R V
f : Dual R V
v : V
r s : R
⊢ transvection f (r • v) ∘ₗ transvection f (s • v) = transvection f ((r + s + s * f v * r) • v)

Tactic:
ext x

Goal state after:
R : Type u_1
V : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid V
inst✝ : Module R V
f : Dual R V
v : V
r s : R
x : V
⊢ (transvection f (r • v) ∘ₗ transvection f (s • v)) x = (transvection f ((r + s + s * f v * r) • v)) x
Module: Mathlib.LinearAlgebra.Transvection.Basic

Goal state before:
pp: case «1»
R : Type u_3
V : Type u_4
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid V
inst✝³ : Module R V
inst✝² : Free R V
inst✝¹ : Module.Finite R V
inst✝ : StrongRankCondition R
f : Dual R V
v : V
hfv : f v = 0
h : finrank R V = 1
h1 : 1 ≤ 1
b : Basis (Fin (finrank R V)) R V := finBasis R V
⊢ transvection f v = id

Tactic:
ext x

Goal state after:
case «1»
R : Type u_3
V : Type u_4
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid V
inst✝³ : Module R V
inst✝² : Free R V
inst✝¹ : Module.Finite R V
inst✝ : StrongRankCondition R
f : Dual R V
v : V
hfv : f v = 0
h : finrank R V = 1
h1 : 1 ≤ 1
b : Basis (Fin (finrank R V)) R V := finBasis R V
x : V
⊢ (transvection f v) x = id x
Module: Mathlib.LinearAlgebra.Transvection.Basic

Goal state before:
pp: case h
R : Type u_1
V : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup V
inst✝ : Module R V
e✝ e : V ≃ₗ[R] V
f : Dual R V
v : V
he : ↑e = LinearMap.transvection f v
⊢ ↑e.symm = LinearMap.transvection f (-e.symm v)

Tactic:
ext x

Goal state after:
case h
R : Type u_1
V : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup V
inst✝ : Module R V
e✝ e : V ≃ₗ[R] V
f : Dual R V
v : V
he : ↑e = LinearMap.transvection f v
x : V
⊢ ↑e.symm x = (LinearMap.transvection f (-e.symm v)) x
Module: Mathlib.LinearAlgebra.Transvection.Basic

Goal state before:
pp: case h
V : Type u_2
inst✝² : AddCommGroup V
K : Type u_3
inst✝¹ : DivisionRing K
inst✝ : Module K V
e : V ≃ₗ[K] V
u : V →ₗ[K] V := ⋯
he : Module.rank K ↥u.range ≤ 1
hu : u + LinearMap.id = ↑e
hr : Module.rank K ↥u.range = 0
⊢ ↑e = LinearMap.transvection 0 0

Tactic:
ext x

Goal state after:
case h
V : Type u_2
inst✝² : AddCommGroup V
K : Type u_3
inst✝¹ : DivisionRing K
inst✝ : Module K V
e : V ≃ₗ[K] V
u : V →ₗ[K] V := ↑e - LinearMap.id
he : Module.rank K ↥u.range ≤ 1
hu : u + LinearMap.id = ↑e
hr : Module.rank K ↥u.range = 0
x : V
⊢ ↑e x = (LinearMap.transvection 0 0) x
Module: Mathlib.LinearAlgebra.Center

Goal state before:
pp: case h
R : Type u_1
V : Type u_2
inst✝⁵ : Ring R
inst✝⁴ : IsDomain R
inst✝³ : StrongRankCondition R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : Free R V
f : V →ₗ[R] V
hV1 : finrank R V ≠ 1
h : ∀ (v : V), ¬LinearIndependent R ![v, f v]
hV : Subsingleton V
⊢ f = 1 • 1

Tactic:
ext x

Goal state after:
case h
R : Type u_1
V : Type u_2
inst✝⁵ : Ring R
inst✝⁴ : IsDomain R
inst✝³ : StrongRankCondition R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : Free R V
f : V →ₗ[R] V
hV1 : finrank R V ≠ 1
h : ∀ (v : V), ¬LinearIndependent R ![v, f v]
hV : Subsingleton V
x : V
⊢ f x = (1 • 1) x
Module: Mathlib.LinearAlgebra.Transvection.Basic

Goal state before:
pp: case h
V : Type u_2
inst✝² : AddCommGroup V
K : Type u_3
inst✝¹ : DivisionRing K
inst✝ : Module K V
e : V ≃ₗ[K] V
u : V →ₗ[K] V := ⋯
hu : u + LinearMap.id = ↑e
hr : 1 ≤ Module.rank K ↥u.range
b : Basis Unit K ↥u.range
⊢ ↑e = (b.coord default ∘ₗ u.rangeRestrict).transvection ↑(b default)

Tactic:
ext x

Goal state after:
case h
V : Type u_2
inst✝² : AddCommGroup V
K : Type u_3
inst✝¹ : DivisionRing K
inst✝ : Module K V
e : V ≃ₗ[K] V
u : V →ₗ[K] V := ↑e - LinearMap.id
hu : u + LinearMap.id = ↑e
hr : 1 ≤ Module.rank K ↥u.range
b : Basis Unit K ↥u.range
x : V
⊢ ↑e x = ((b.coord default ∘ₗ u.rangeRestrict).transvection ↑(b default)) x
Module: Mathlib.LinearAlgebra.QuadraticForm.TensorProduct

Goal state before:
pp: R : Type uR
A : Type uA
M₂ : Type uM₂
N₁ : Type uN₁
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : AddCommGroup M₂
inst✝⁵ : AddCommGroup N₁
inst✝⁴ : Algebra R A
inst✝³ : Module R N₁
inst✝² : Module A N₁
inst✝¹ : IsScalarTower R A N₁
inst✝ : Module R M₂
Q₁ Q₂ : QuadraticMap A (A ⊗[R] M₂) N₁
h : ∀ (a : A) (m : M₂), Q₁ (a ⊗ₜ[R] m) = Q₂ (a ⊗ₜ[R] m)
⊢ Q₁ = Q₂

Tactic:
ext x

Goal state after:
R : Type uR
A : Type uA
M₂ : Type uM₂
N₁ : Type uN₁
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : AddCommGroup M₂
inst✝⁵ : AddCommGroup N₁
inst✝⁴ : Algebra R A
inst✝³ : Module R N₁
inst✝² : Module A N₁
inst✝¹ : IsScalarTower R A N₁
inst✝ : Module R M₂
Q₁ Q₂ : QuadraticMap A (A ⊗[R] M₂) N₁
h : ∀ (a : A) (m : M₂), Q₁ (a ⊗ₜ[R] m) = Q₂ (a ⊗ₜ[R] m)
x : A ⊗[R] M₂
⊢ Q₁ x = Q₂ x
Module: Mathlib.LinearAlgebra.CliffordAlgebra.BaseChange

Goal state before:
pp: R : Type u_1
A : Type u_2
V : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : AddCommGroup V
inst✝² : Algebra R A
inst✝¹ : Module R V
inst✝ : Invertible 2
Q : QuadraticForm R V
⊢ (ofBaseChange A Q).comp (toBaseChange A Q) = AlgHom.id A (CliffordAlgebra (QuadraticForm.baseChange A Q))

Tactic:
ext x

Goal state after:
R : Type u_1
A : Type u_2
V : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : AddCommGroup V
inst✝² : Algebra R A
inst✝¹ : Module R V
inst✝ : Invertible 2
Q : QuadraticForm R V
x : V
⊢ ((TensorProduct.AlgebraTensorModule.curry
          (((ofBaseChange A Q).comp (toBaseChange A Q)).toLinearMap ∘ₗ ι (QuadraticForm.baseChange A Q)))
        1)
      x =
    ((TensorProduct.AlgebraTensorModule.curry
          ((AlgHom.id A (CliffordAlgebra (QuadraticForm.baseChange A Q))).toLinearMap ∘ₗ
            ι (QuadraticForm.baseChange A Q)))
        1)
      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 : QuadraticForm R M
d : Module.Dual R M
x : CliffordAlgebra Q
⊢ (contractRight ((contractRight x) d)) d = 0

Tactic:
by
  rw [contractRight_eq, contractRight_eq, reverse_reverse, contractLeft_contractLeft, map_zero]

Goal state after:
Module: Mathlib.LinearAlgebra.Transvection.Basic

Goal state before:
pp: case neg
K : Type u_3
V : Type u_4
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : Dual K V
v : V
hfv : ¬f v = 0
ι : Set V
b : Basis (↑ι) K V
i : ↑ι
hv : v = b i
hf : f = f v • b.coord i
this : Fintype ↑ι
x y : ↑ι
hxy : ¬x = y
hxi : ¬x = i
⊢ (Finsupp.single y 1) i * (Finsupp.single i 1) x = 0

Tactic:
simp [Finsupp.single_eq_of_ne hxi]

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
m₁✝ m₂✝ : M × R
m₁ : M
r₁ : R
m₂ : M
r₂ : R
h1 : e0 Q * (v Q) m₁ * (e0 Q * (v Q) m₂) = (v Q) m₁ * (v Q) m₂
h2 : -(r₂ • e0 Q * (v Q) m₁) = (v Q) m₁ * r₂ • e0 Q
h3 : -(algebraMap R (CliffordAlgebra (Q' Q))) (r₁ * r₂) = r₁ • e0 Q * r₂ • e0 Q
⊢ e0 Q * (v Q) m₁ * (e0 Q * (v Q) m₂) + r₁ • e0 Q * (v Q) m₂ - r₂ • e0 Q * (v Q) m₁ -
      (algebraMap R (CliffordAlgebra (Q' Q))) (r₁ * r₂) =
    (v Q) m₁ * (v Q) m₂ + r₁ • e0 Q * (v Q) m₂ + (v Q) m₁ * r₂ • e0 Q + r₁ • e0 Q * r₂ • e0 Q

Tactic:
rw [sub_eq_add_neg, sub_eq_add_neg, h1, h2, h3]

Goal state after:
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
f : ModN G n →+ M
⊢ (fun φ ↦ QuotientAddGroup.lift ((LinearMap.lsmul ℤ G) ↑n).range.toAddSubgroup ↑φ ⋯)
      ((fun f ↦ ⟨f.comp (QuotientAddGroup.mk' ((LinearMap.lsmul ℤ G) ↑n).range.toAddSubgroup), ⋯⟩) f) =
    f

Tactic:
ext x

Goal state after:
G : Type u_1
H : Type u_2
M : Type u_3
inst✝¹ : AddCommGroup G
n : ℕ
inst✝ : AddMonoid M
f : ModN G n →+ M
x : G ⧸ ((LinearMap.lsmul ℤ G) ↑n).range.toAddSubgroup
⊢ ((fun φ ↦ QuotientAddGroup.lift ((LinearMap.lsmul ℤ G) ↑n).range.toAddSubgroup ↑φ ⋯)
        ((fun f ↦ ⟨f.comp (QuotientAddGroup.mk' ((LinearMap.lsmul ℤ G) ↑n).range.toAddSubgroup), ⋯⟩) f))
      x =
    f x
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)
⊢ L.goursatFst.toAddSubgroup = L.toAddSubgroup.goursatFst

Tactic:
ext x

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)
x : M
⊢ x ∈ L.goursatFst.toAddSubgroup ↔ x ∈ L.toAddSubgroup.goursatFst
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)
⊢ L.goursatSnd.toAddSubgroup = L.toAddSubgroup.goursatSnd

Tactic:
ext x

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)
x : N
⊢ x ∈ L.goursatSnd.toAddSubgroup ↔ x ∈ L.toAddSubgroup.goursatSnd
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
i x : FreeTensorAlgebra R A
⊢ rel R A i x ↔ (rel R A on ⇑ofDirectSum on ⇑(powerAlgebraEquivFreeTensorAlgebra R A).toRingEquiv.symm) i x

Tactic:
simp [Function.onFun]

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Charpoly.FiniteField

Goal state before:
pp: case inl.h
n : Type u_1
inst✝³ : DecidableEq n
inst✝² : Fintype n
K : Type u_2
inst✝¹ : Field K
inst✝ : Fintype K
M : Matrix n n K
h✝ : Nonempty n
p : ℕ
hp✝ : CharP K p
k : ℕ
kpos : 0 < k
hp : Nat.Prime p
hk : Fintype.card K = p ^ k
this : Fact (Nat.Prime p)
⊢ Commute X (C M)

Tactic:
exact (C M).commute_X

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Circulant

Goal state before:
pp: α : Type u_1
n : Type u_3
inst✝³ : CommMagma α
inst✝² : AddCommMonoid α
inst✝¹ : Fintype n
inst✝ : AddCommGroup n
v w : n → α
i j : n
⊢ (circulant v * circulant w) i j = (circulant w * circulant v) i j

Tactic:
simp only [mul_apply, circulant_apply]

Goal state after:
α : Type u_1
n : Type u_3
inst✝³ : CommMagma α
inst✝² : AddCommMonoid α
inst✝¹ : Fintype n
inst✝ : AddCommGroup n
v w : n → α
i j : n
⊢ ∑ j_1, v (i - j_1) * w (j_1 - j) = ∑ j_1, w (i - j_1) * v (j_1 - j)
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
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' }
⊢ Finset.univ = Finset.map f'' Finset.univ

Tactic:
ext x

Goal state after:
ι : 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' }
x : ↥{x | ∃ j, f j = x}
⊢ x ∈ Finset.univ ↔ x ∈ Finset.map f'' Finset.univ
Module: Mathlib.LinearAlgebra.Matrix.Determinant.TotallyUnimodular

Goal state before:
pp: case h.inl
m : Type u_1
n : Type u_3
R : Type u_5
inst✝ : CommRing R
A : Matrix m n R
hA : A.IsTotallyUnimodular
k : ℕ
f : Fin k → m
g : Fin k → n
i j : Fin k
hfij : f i = f j
hij : i ≠ j
⊢ (A.submatrix f g)ᵀ.det = 0

Tactic:
transpose_submatrix

Goal state after:
case h.inl
m : Type u_1
n : Type u_3
R : Type u_5
inst✝ : CommRing R
A : Matrix m n R
hA : A.IsTotallyUnimodular
k : ℕ
f : Fin k → m
g : Fin k → n
i j : Fin k
hfij : f i = f j
hij : i ≠ j
⊢ (Aᵀ.submatrix g f).det = 0
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
inst✝ : IsEmpty m
A : Matrix m n R
⊢ A.IsTotallyUnimodular

Tactic:
intro k f _ _ _

Goal state after:
m : Type u_1
n : Type u_3
R : Type u_5
inst✝¹ : CommRing R
inst✝ : IsEmpty m
A : Matrix m n R
k : ℕ
f : Fin k → m
g✝ : Fin k → n
a✝¹ : Function.Injective f
a✝ : Function.Injective g✝
⊢ (A.submatrix f g✝).det ∈ Set.range SignType.cast
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 : l i = ⊤
⊢ ⊤ = ↑c'

Tactic:
rw [hl.eq_top_iff] at hc

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.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:
refine and_congr_right' <| and_congr_right' <| forall_congr' fun i => ?_

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
i : m
⊢ ((∀ (j : n), ↑j < l i → A i j = 0) ∧ ∀ (c : n), l i = ↑c → A i c ≠ 0) ↔
    l i = ⊤ ∧ A i = 0 ∨ ∃ c, l i = ↑c ∧ A.IsLeadingEntry i c
Module: Mathlib.LinearAlgebra.Matrix.Determinant.TotallyUnimodular

Goal state before:
pp: m : Type u_1
m' : Type u_2
n : Type u_3
R : Type u_5
inst✝ : CommRing R
A : Matrix m n R
x✝¹ : Nonempty n
x✝ : m'
inhabited_h : Inhabited n
⊢ replicateRow m' 0 x✝ = Pi.single default ↑0

Tactic:
ext x

Goal state after:
m : Type u_1
m' : Type u_2
n : Type u_3
R : Type u_5
inst✝ : CommRing R
A : Matrix m n R
x✝¹ : Nonempty n
x✝ : m'
inhabited_h : Inhabited n
x : n
⊢ replicateRow m' 0 x✝ x = Pi.single default (↑0) x
Module: Mathlib.LinearAlgebra.Matrix.FixedDetMatrices

Goal state before:
pp: case neg.refine_2
m : ℤ
hm : m ≠ 0
A : FixedDetMatrix (Fin 2) ℤ m
h : ↑A 1 0 = 0
hd : ↑A 1 1 ≠ 0
h1 : ¬0 < ↑A 0 0
⊢ -↑A 0 1 % ↑A 1 1 < |↑A 1 1|

Tactic:
exact Int.emod_lt_abs _ hd

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.HadamardMatrix

Goal state before:
pp: n : Type u_2
R : Type u_3
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : CommSemiring R
inst✝ : StarRing R
A : Matrix n n R
hA : A.IsHadamard
⊢ ↑(Fintype.card n) • 1ᵀ = ↑(Fintype.card n) • 1

Tactic:
transpose_one

Goal state after:
n : Type u_2
R : Type u_3
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : CommSemiring R
inst✝ : StarRing R
A : Matrix n n R
hA : A.IsHadamard
⊢ ↑(Fintype.card n) • 1 = ↑(Fintype.card n) • 1
Module: Mathlib.LinearAlgebra.Matrix.Gershgorin

Goal state before:
pp: K : Type u_1
n : Type u_2
inst✝² : NormedField K
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n K
h : ∀ (k : n), ∑ i ∈ Finset.univ.erase k, ‖A i k‖ < ‖A k k‖
⊢ A.det ≠ 0

Tactic:
rw [← Matrix.det_transpose]
  exact det_ne_zero_of_sum_row_lt_diag (by simp_rw [Matrix.transpose_apply]; exact h)

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Swap

Goal state before:
pp: R : Type u_1
n : Type u_2
m : Type u_3
inst✝² : Semiring R
inst✝¹ : DecidableEq n
inst✝ : Fintype n
i j b : n
a : m
hbi : b ≠ i
hbj : b ≠ j
g : Matrix m n R
⊢ (g * swap R i j) a b = g a b

Tactic:
simp [swap, PEquiv.mul_toMatrix_toPEquiv, Equiv.swap_apply_of_ne_of_ne hbi hbj]

Goal state after:
Module: Mathlib.LinearAlgebra.Multilinear.Pi

Goal state before:
pp: ι : Type uι
κ : ι → Type uκ
R : Type uR
M : (i : ι) → κ i → Type uM
N : Type uN
inst✝⁷ : Semiring R
inst✝⁶ : (i : ι) → (k : κ i) → AddCommMonoid (M i k)
inst✝⁵ : AddCommMonoid N
inst✝⁴ : (i : ι) → (k : κ i) → Module R (M i k)
inst✝³ : Module R N
inst✝² : Finite ι
inst✝¹ : ∀ (i : ι), Finite (κ i)
inst✝ : (i : ι) → DecidableEq (κ i)
f g : MultilinearMap R (fun i ↦ (j : κ i) → M i j) N
h :
  ∀ (p : (i : ι) → κ i),
    (f.compLinearMap fun i ↦ LinearMap.single R (M i) (p i)) = g.compLinearMap fun i ↦ LinearMap.single R (M i) (p i)
⊢ f = g

Tactic:
ext x

Goal state after:
ι : Type uι
κ : ι → Type uκ
R : Type uR
M : (i : ι) → κ i → Type uM
N : Type uN
inst✝⁷ : Semiring R
inst✝⁶ : (i : ι) → (k : κ i) → AddCommMonoid (M i k)
inst✝⁵ : AddCommMonoid N
inst✝⁴ : (i : ι) → (k : κ i) → Module R (M i k)
inst✝³ : Module R N
inst✝² : Finite ι
inst✝¹ : ∀ (i : ι), Finite (κ i)
inst✝ : (i : ι) → DecidableEq (κ i)
f g : MultilinearMap R (fun i ↦ (j : κ i) → M i j) N
h :
  ∀ (p : (i : ι) → κ i),
    (f.compLinearMap fun i ↦ LinearMap.single R (M i) (p i)) = g.compLinearMap fun i ↦ LinearMap.single R (M i) (p i)
x : (i : ι) → (j : κ i) → M i j
⊢ f x = g x
Module: Mathlib.LinearAlgebra.Multilinear.Pi

Goal state before:
pp: case inr
ι : Type uι
κ : ι → Type uκ
R : Type uR
M : (i : ι) → κ i → Type uM
N : ((i : ι) → κ i) → Type uN
inst✝⁶ : Semiring R
inst✝⁵ : (i : ι) → (k : κ i) → AddCommMonoid (M i k)
inst✝⁴ : (p : (i : ι) → κ i) → AddCommMonoid (N p)
inst✝³ : (i : ι) → (k : κ i) → Module R (M i k)
inst✝² : (p : (i : ι) → κ i) → Module R (N p)
inst✝¹ : Fintype ι
inst✝ : (i : ι) → DecidableEq (κ i)
p : (i : ι) → κ i
f : MultilinearMap R (fun i ↦ M i (p i)) (N p)
x : (i : ι) → (j : κ i) → M i j
p' : (i : ι) → κ i
hp : p ≠ p'
⊢ (piFamily (Pi.single p f)) x p' = Pi.single p (f fun i ↦ x i (p i)) p'

Tactic:
simp [hp]

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Nonsingular

Goal state before:
pp: R : Type u_1
n : Type u_3
inst✝² : CommSemiring R
inst✝¹ : Fintype n
A : Matrix n n R
inst✝ : IsCancelAdd R
⊢ IsLeftRegular A ↔ IsRightRegular A

Tactic:
by
  classical rw [isLeftRegular_iff_nonsingular, isRightRegular_iff_nonsingular]

Goal state after: