mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.LinearIndependent.Algebra

Goal state before:
pp: R : Type u_1
S : Type u_2
A : Type u_3
inst✝⁷ : CommSemiring R
inst✝⁶ : CommSemiring S
inst✝⁵ : Semiring A
inst✝⁴ : Algebra R S
inst✝³ : Algebra S A
inst✝² : Algebra R A
inst✝¹ : IsScalarTower R S A
inst✝ : FaithfulSMul S A
ι : Type u_4
v : ι → S
⊢ Set.InjOn ⇑(IsScalarTower.toAlgHom R S A).toLinearMap ↑(Submodule.span R (Set.range v))

Tactic:
simp

Goal state after:
Module: Mathlib.LinearAlgebra.LinearIndependent.Algebra

Goal state before:
pp: R : Type u_1
S : Type u_2
A : Type u_3
inst✝⁷ : CommSemiring R
inst✝⁶ : CommSemiring S
inst✝⁵ : Semiring A
inst✝⁴ : Algebra R S
inst✝³ : Algebra S A
inst✝² : Algebra R A
inst✝¹ : IsScalarTower R S A
inst✝ : FaithfulSMul S A
s : Set S
⊢ Set.InjOn (⇑(algebraMap S A)) s

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.LocalProperties.Basic

Goal state before:
pp: R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
H : HoldsForLocalizationAway fun {R S} [CommRing R] [CommRing S] ↦ P
hf : Function.Bijective ⇑f
this : Algebra R S := f.toAlgebra
⊢ Submonoid.powers 1 ≤ IsUnit.submonoid R

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.LocalProperties.Basic

Goal state before:
pp: P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : LocalizationAwayPreserves fun {R S} [CommRing R] [CommRing S] ↦ P
R S T : Type u
x✝² : CommRing R
x✝¹ : CommRing S
x✝ : CommRing T
f : R →+* S
e : S ≃+* T
hf : P f
this✝ : Algebra S T := e.toRingHom.toAlgebra
this : IsLocalization.Away 1 R
⊢ IsUnit (f 1)

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.LocalProperties.Basic

Goal state before:
pp: P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : LocalizationAwayPreserves fun {R S} [CommRing R] [CommRing S] ↦ P
R S T : Type u
x✝² : CommRing R
x✝¹ : CommRing S
x✝ : CommRing T
f : S →+* T
e : R ≃+* S
hf : P f
this✝ : Algebra S R := e.symm.toRingHom.toAlgebra
this : IsLocalization.Away 1 R
⊢ IsUnit (f 1)

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.LocalProperties.Basic

Goal state before:
pp: P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : StableUnderCompositionWithLocalizationAway fun {R S} [CommRing R] [CommRing S] ↦ P
R S T : Type u
x✝² : CommRing R
x✝¹ : CommRing S
x✝ : CommRing T
f : R →+* S
e : S ≃+* T
hf : P f
this✝ : Algebra S T := e.toRingHom.toAlgebra
this : IsLocalization.Away 1 T
⊢ (fun {R S} [CommRing R] [CommRing S] ↦ P) (e.toRingHom.comp f)

Tactic:
exact hP.right T (1 : S) f hf

Goal state after:
Module: Mathlib.RingTheory.LocalProperties.Basic

Goal state before:
pp: P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
H : LocalizationPreserves P
R S : Type u
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
f : R →+* S
r : R
R' S' : Type u
inst✝⁵ : CommRing R'
inst✝⁴ : CommRing S'
inst✝³ : Algebra R R'
inst✝² : Algebra S S'
inst✝¹ : IsLocalization.Away r R'
inst✝ : IsLocalization.Away (f r) S'
⊢ (fun {R S} [CommRing R] [CommRing S] ↦ P) f →
    (fun {R S} [CommRing R] [CommRing S] ↦ P) (IsLocalization.Away.map R' S' f r)

Tactic:
hf

Goal state after:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
H : LocalizationPreserves P
R S : Type u
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
f : R →+* S
r : R
R' S' : Type u
inst✝⁵ : CommRing R'
inst✝⁴ : CommRing S'
inst✝³ : Algebra R R'
inst✝² : Algebra S S'
inst✝¹ : IsLocalization.Away r R'
inst✝ : IsLocalization.Away (f r) S'
hf : P f
⊢ P (IsLocalization.Away.map R' S' f r)
Module: Mathlib.RingTheory.LocalProperties.Basic

Goal state before:
pp: P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : PropertyIsLocal P
hPi : ContainsIdentities fun {R S} [CommRing R] [CommRing S] ↦ P
R S : Type u
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
r : R
inst✝ : IsLocalization.Away r S
⊢ algebraMap R S = (algebraMap R S).comp (id R)

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.LocalProperties.Basic

Goal state before:
pp: P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : OfLocalizationSpan fun {R S} [CommRing R] [CommRing S] ↦ P
hPi : RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ P
R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Set R
hs : Ideal.span s = ⊤
hT :
  ∀ (r : ↑s),
    ∃ Rᵣ Sᵣ x x_1 x_2 x_3,
      ∃ (x_4 : IsLocalization.Away (↑r) Rᵣ) (x_5 : IsLocalization.Away (f ↑r) Sᵣ),
        P (IsLocalization.Away.map Rᵣ Sᵣ f ↑r)
r : ↑s
Rᵣ Sᵣ : Type u
w✝⁵ : CommRing Rᵣ
w✝⁴ : CommRing Sᵣ
w✝³ : Algebra R Rᵣ
w✝² : Algebra S Sᵣ
w✝¹ : IsLocalization.Away (↑r) Rᵣ
w✝ : IsLocalization.Away (f ↑r) Sᵣ
hf : P (IsLocalization.Away.map Rᵣ Sᵣ f ↑r)
⊢ ∃ Rᵣ Sᵣ x x_1 x_2 x_3,
    ∃ (_ : IsLocalization.Away (↑r) Rᵣ) (_ : IsLocalization.Away (f ↑r) Sᵣ),
      ∃ fᵣ, ∃ (_ : fᵣ.comp (algebraMap R Rᵣ) = (algebraMap S Sᵣ).comp f), P fᵣ

Tactic:
exact ⟨Rᵣ, Sᵣ, inferInstance, inferInstance, inferInstance, inferInstance,
    inferInstance, inferInstance, IsLocalization.Away.map Rᵣ Sᵣ f r, IsLocalization.map_comp _, hf⟩

Goal state after:
Module: Mathlib.RingTheory.Localization.AtPrime.Basic

Goal state before:
pp: case refine_1
R✝ : Type u_1
inst✝²⁷ : CommSemiring R✝
S✝ : Type u_2
inst✝²⁶ : CommSemiring S✝
inst✝²⁵ : Algebra R✝ S✝
P✝ : Type u_3
inst✝²⁴ : CommSemiring P✝
p✝ : Ideal R✝
inst✝²³ : p✝.IsPrime
Rₚ✝ : Type u_4
inst✝²² : CommSemiring Rₚ✝
inst✝²¹ : Algebra R✝ Rₚ✝
inst✝²⁰ : IsLocalization.AtPrime Rₚ✝ p✝
inst✝¹⁹ : IsLocalRing Rₚ✝
Sₚ✝ : Type u_5
inst✝¹⁸ : CommSemiring Sₚ✝
inst✝¹⁷ : Algebra S✝ Sₚ✝
inst✝¹⁶ : IsLocalization (algebraMapSubmonoid S✝ p✝.primeCompl) Sₚ✝
inst✝¹⁵ : Algebra Rₚ✝ Sₚ✝
P : Ideal S✝
S : Type u_6
R : Type u_7
inst✝¹⁴ : CommRing R
p : Ideal R
inst✝¹³ : p.IsMaximal
Rₚ : Type u_8
inst✝¹² : CommRing Rₚ
inst✝¹¹ : Algebra R Rₚ
inst✝¹⁰ : IsLocalization.AtPrime Rₚ p
inst✝⁹ : IsLocalRing Rₚ
Sₚ : Type u_9
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
inst✝⁶ : CommRing Sₚ
inst✝⁵ : Algebra S Sₚ
inst✝⁴ : Algebra R Sₚ
inst✝³ : Algebra Rₚ Sₚ
inst✝² : IsLocalization (algebraMapSubmonoid S p.primeCompl) Sₚ
inst✝¹ : IsScalarTower R S Sₚ
inst✝ : IsScalarTower R Rₚ Sₚ
h : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
rw [IsScalarTower.algebraMap_eq S Sₚ, Ideal.Quotient.algebraMap_eq, ← RingHom.comap_ker,
      Ideal.mk_ker, h, Ideal.map_map, ← IsScalarTower.algebraMap_eq, ← under_def, under_map_eq_map]

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

Goal state before:
pp: α : Type u_1
n : Type u_3
m : Type u_4
A : Matrix m m α
B : Matrix m n α
C : Matrix n m α
D : Matrix n n α
hA : A.IsSymm
hBC : Bᵀ = C
hD : D.IsSymm
⊢ Bᵀᵀ = B

Tactic:
simp

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

Goal state before:
pp: case e'_3
n : Type u_1
α : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A B : Matrix n n α
g : Equiv.Perm n
⊢ ∀ x ∈ Finset.univ, B (g x) x = ((X • A.map ⇑C + B.map ⇑C) (g x) x).coeff 0

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Polynomial.Laurent

Goal state before:
pp: case refine_1
R : Type u_1
inst✝ : Semiring R
f✝ f g : R[X]
⊢ trunc (toLaurent f) = f → trunc (toLaurent g) = g → trunc (toLaurent (f + g)) = f + g

Tactic:
hf

Goal state after:
case refine_1
R : Type u_1
inst✝ : Semiring R
f✝ f g : R[X]
hf : trunc (toLaurent f) = f
⊢ trunc (toLaurent g) = g → trunc (toLaurent (f + g)) = f + g
Module: Mathlib.Algebra.Polynomial.Laurent

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
a : R
n : ℕ
⊢ toLaurent (Polynomial.C a * X ^ n) = C a * T (Int.ofNat n) * T ↑0

Tactic:
simp

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

Goal state before:
pp: case e'_3.e'_1
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
i j : n
⊢ 1 = det 1

Tactic:
simp

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

Goal state before:
pp: n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
i j : n
⊢ ∀ (j : n), Pi.single i 1 j = 1 j i

Tactic:
intro j

Goal state after:
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
i j✝ j : n
⊢ Pi.single i 1 j = 1 j i
Module: Mathlib.LinearAlgebra.Matrix.Transvection

Goal state before:
pp: case nil
n : Type u_1
R : Type u₂
inst✝² : DecidableEq n
inst✝¹ : CommRing R
inst✝ : Fintype n
⊢ (List.map toMatrix []).prod.det = 1

Tactic:
simp

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

Goal state before:
pp: case nil
n : Type u_1
R : Type u₂
inst✝² : DecidableEq n
inst✝¹ : CommRing R
inst✝ : Fintype n
⊢ (List.map (toMatrix ∘ TransvectionStruct.inv) [].reverse).prod * (List.map toMatrix []).prod = 1

Tactic:
simp

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

Goal state before:
pp: case nil
n : Type u_1
R : Type u₂
inst✝² : DecidableEq n
inst✝¹ : CommRing R
inst✝ : Fintype n
⊢ (List.map toMatrix []).prod * (List.map (toMatrix ∘ TransvectionStruct.inv) [].reverse).prod = 1

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Polynomial.Laurent

Goal state before:
pp: R : Type u_1
inst✝¹ : CommSemiring R
S : Type u_3
inst✝ : CommSemiring S
f : R →+* S
x : Sˣ
r : R
n : ℤ
⊢ (eval₂ f x) (C r * T n) = f r * ↑(x ^ n)

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Polynomial.Laurent

Goal state before:
pp: R : Type u_3
inst✝ : CommSemiring R
x✝ : R
a✝ : ℤ
⊢ ((⇑invert ∘ ⇑C) x✝).coeff a✝ = (C x✝).coeff a✝

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Polynomial.Laurent

Goal state before:
pp: R : Type u_3
inst✝ : CommSemiring R
t : R
a✝ : ℤ
⊢ (invert (C t)).coeff a✝ = (C t).coeff a✝

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Polynomial.Laurent

Goal state before:
pp: R : Type u_3
inst✝ : CommSemiring R
x✝ : R[T;T⁻¹]
a✝ : ℤ
⊢ (invert (invert x✝)).coeff a✝ = x✝.coeff a✝

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Polynomial.Laurent

Goal state before:
pp: case M0
R : Type u_3
inst✝ : CommSemiring R
a✝ : Nontrivial R
⊢ toLaurent (reverse 0) = invert (toLaurent 0) * T ↑(natDegree 0)

Tactic:
simp

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

Goal state before:
pp: case nil
n : Type u_1
p : Type u_2
R : Type u₂
inst✝⁴ : DecidableEq n
inst✝³ : DecidableEq p
inst✝² : CommRing R
inst✝¹ : Fintype n
inst✝ : Fintype p
M : Matrix n n R
N : Matrix p p R
⊢ (List.map (toMatrix ∘ sumInl p) []).prod * fromBlocks M 0 0 N = fromBlocks ((List.map toMatrix []).prod * M) 0 0 N

Tactic:
simp

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

Goal state before:
pp: case nil
n : Type u_1
p : Type u_2
R : Type u₂
inst✝⁴ : DecidableEq n
inst✝³ : DecidableEq p
inst✝² : CommRing R
inst✝¹ : Fintype n
inst✝ : Fintype p
M : Matrix n n R
N : Matrix p p R
⊢ fromBlocks M 0 0 N * (List.map (toMatrix ∘ sumInl p) []).prod = fromBlocks (M * (List.map toMatrix []).prod) 0 0 N

Tactic:
simp

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

Goal state before:
pp: case nil
n : Type u_1
p : Type u_2
R : Type u₂
inst✝⁴ : DecidableEq n
inst✝³ : DecidableEq p
inst✝² : CommRing R
inst✝¹ : Fintype n
inst✝ : Fintype p
e : n ≃ p
⊢ (List.map (toMatrix ∘ reindexEquiv e) []).prod = (reindexAlgEquiv R R e) (List.map toMatrix []).prod

Tactic:
simp

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

Goal state before:
pp: case «0».«0»
α : Type w
inst✝ : CommRing α
A : Matrix (Fin 2) (Fin 2) α
⊢ (-1) ^ (↑((fun i ↦ i) ⟨0, ⋯⟩) + ↑((fun i ↦ i) ⟨0, ⋯⟩)) *
      (A.submatrix ((fun i ↦ i) ⟨0, ⋯⟩).succAbove ((fun i ↦ i) ⟨0, ⋯⟩).succAbove).det =
    !![A 1 1, -A 0 1; -A 1 0, A 0 0] ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩)

Tactic:
simp

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

Goal state before:
pp: case «0».«1»
α : Type w
inst✝ : CommRing α
A : Matrix (Fin 2) (Fin 2) α
⊢ (-1) ^ (↑((fun i ↦ i) ⟨1, ⋯⟩) + ↑((fun i ↦ i) ⟨0, ⋯⟩)) *
      (A.submatrix ((fun i ↦ i) ⟨1, ⋯⟩).succAbove ((fun i ↦ i) ⟨0, ⋯⟩).succAbove).det =
    !![A 1 1, -A 0 1; -A 1 0, A 0 0] ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩)

Tactic:
simp

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

Goal state before:
pp: case «1».«0»
α : Type w
inst✝ : CommRing α
A : Matrix (Fin 2) (Fin 2) α
⊢ (-1) ^ (↑((fun i ↦ i) ⟨0, ⋯⟩) + ↑((fun i ↦ i) ⟨1, ⋯⟩)) *
      (A.submatrix ((fun i ↦ i) ⟨0, ⋯⟩).succAbove ((fun i ↦ i) ⟨1, ⋯⟩).succAbove).det =
    !![A 1 1, -A 0 1; -A 1 0, A 0 0] ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩)

Tactic:
simp

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

Goal state before:
pp: case «1».«1»
α : Type w
inst✝ : CommRing α
A : Matrix (Fin 2) (Fin 2) α
⊢ (-1) ^ (↑((fun i ↦ i) ⟨1, ⋯⟩) + ↑((fun i ↦ i) ⟨1, ⋯⟩)) *
      (A.submatrix ((fun i ↦ i) ⟨1, ⋯⟩).succAbove ((fun i ↦ i) ⟨1, ⋯⟩).succAbove).det =
    !![A 1 1, -A 0 1; -A 1 0, A 0 0] ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩)

Tactic:
simp

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

Goal state before:
pp: R : Type u_6
n : ℕ
inst✝ : AddCommMonoid R
M : Matrix (Fin n.succ) (Fin n.succ) R
⊢ M 0 0 + ∑ i, (M.submatrix Fin.succ Fin.succ).diag i = ∑ i, M.diag ((finSuccEquiv n).symm i)

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
m : Type u_10
n : Type u_11
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : CommRing R
A : Matrix m m R
B : Matrix n n R
⊢ (A.map fun a ↦ ((Algebra.lmul ℕ R).toLinearMap a) 1).det ^ Fintype.card n *
      (B.map fun b ↦ ((Algebra.lmul ℕ R).toLinearMap 1) b).det ^ Fintype.card m =
    A.det ^ Fintype.card n * B.det ^ Fintype.card m

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
l : Type u_9
m : Type u_10
n : Type u_11
p : Type u_12
inst✝¹ : CommMagma R
inst✝ : StarMul R
x : Matrix l m R
y : Matrix n p R
i✝ : m × p
j✝ : l × n
⊢ (kroneckerMap (fun x1 x2 ↦ x1 * x2) x y)ᴴ i✝ j✝ = kroneckerMap (fun x1 x2 ↦ x1 * x2) xᴴ yᴴ i✝ j✝

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
l : Type u_9
m : Type u_10
n : Type u_11
p : Type u_12
inst✝¹ : Mul R
inst✝ : StarMul R
x : Matrix l m R
y : Matrix n p R
i✝ : m × p
j✝ : l × n
⊢ (kroneckerMap (fun x1 x2 ↦ x1 * x2) x y)ᴴ i✝ j✝ =
    (kroneckerMap (fun x1 x2 ↦ x1 * x2) yᴴ xᴴ).submatrix Prod.swap Prod.swap i✝ j✝

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
α : Type u_3
β : Type u_5
l : Type u_9
m : Type u_10
n : Type u_11
p : Type u_12
inst✝⁹ : CommSemiring R
inst✝⁸ : AddCommMonoid α
inst✝⁷ : AddCommMonoid β
inst✝⁶ : Module R α
inst✝⁵ : Module R β
inst✝⁴ : StarRing R
inst✝³ : StarAddMonoid α
inst✝² : StarAddMonoid β
inst✝¹ : StarModule R α
inst✝ : StarModule R β
x : Matrix l m α
y : Matrix n p β
i✝ : m × p
j✝ : l × n
⊢ (kroneckerMap (tmul R) x y)ᴴ i✝ j✝ = kroneckerMap (tmul R) xᴴ yᴴ i✝ j✝

Tactic:
simp

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

Goal state before:
pp: 𝕜 : Type u_3
inst✝ : Field 𝕜
r : ℕ
M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
hM : M (inr ()) (inr ()) ≠ 0
i : Fin r
H : ∀ k ≤ r, (M * (List.take k (listTransvecRow M)).prod) (inr ()) (inl i) = if k ≤ ↑i then M (inr ()) (inl i) else 0
A : (listTransvecRow M).length = r
⊢ ¬r ≤ ↑i

Tactic:
simp

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

Goal state before:
pp: case zero
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
⊢ (A ^ 0).adjugate = A.adjugate ^ 0

Tactic:
simp

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

Goal state before:
pp: case zero
𝕜 : Type u_3
inst✝ : Field 𝕜
r : ℕ
M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
hM : M (inr ()) (inr ()) ≠ 0
i : Fin r
hk : 0 ≤ r
⊢ (M * (List.take 0 (listTransvecRow M)).prod) (inr ()) (inl i) = if 0 ≤ ↑i then M (inr ()) (inl i) else 0

Tactic:
simp

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

Goal state before:
pp: l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A B : Matrix n n α
⊢ 1 * 1 = 1

Tactic:
simp

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

Goal state before:
pp: case H.inl
α : Type u_1
R : Type v
inst✝⁴ : CommRing R
inst✝³ : DecidableEq α
inst✝² : LinearOrder α
m : Type u_3
M : Matrix m m R
b : m → α
inst✝¹ : DecidableEq m
inst✝ : Fintype m
hM : M.BlockTriangular b
ih :
  ∀ s ∈ image b univ,
    ∀ {m_1 : Type u_3} {M : Matrix m_1 m_1 R} {b_1 : m_1 → α} [inst : DecidableEq m_1] [inst_1 : Fintype m_1],
      M.BlockTriangular b_1 →
        image b_1 univ = (image b univ).erase s → M.det = ∏ a ∈ (image b univ).erase s, (M.toSquareBlock b_1 a).det
h✝ : IsEmpty m
⊢ M.det = ∏ a ∈ image b univ, (M.toSquareBlock b a).det

Tactic:
simp

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

Goal state before:
pp: 𝕜 : Type u_3
inst✝ : Field 𝕜
r : ℕ
M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
hM : M (inr ()) (inr ()) ≠ 0
i : Fin r
⊢ inl i ≠ inr ()

Tactic:
simp

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

Goal state before:
pp: 𝕜 : Type u_3
inst✝ : Field 𝕜
r : ℕ
M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
hM : M (inr ()) (inr ()) ≠ 0
L : List (TransvectionStruct (Fin r ⊕ Unit) 𝕜) :=
  List.ofFn fun i ↦ { i := inl i, j := inr (), hij := ⋯, c := -M (inl i) (inr ()) / M (inr ()) (inr ()) }
i : Fin r
⊢ inr () ≠ inl i

Tactic:
simp

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

Goal state before:
pp: l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝⁵ : Fintype n
inst✝⁴ : DecidableEq n
inst✝³ : CommRing α
A✝ B : Matrix n n α
inst✝² : Fintype m
inst✝¹ : DecidableEq m
A : Matrix m m α
e₁ e₂ : n ≃ m
inst✝ : Invertible (A.submatrix ⇑e₁ ⇑e₂)
⊢ A = (A.submatrix ⇑e₁ ⇑e₂).submatrix ⇑e₁.symm ⇑e₂.symm

Tactic:
simp

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

Goal state before:
pp: 𝕜 : Type u_3
inst✝ : Field 𝕜
r : ℕ
M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
hM : M (inr ()) (inr ()) = 0
H :
  (¬∀ (i : Fin r) (j : Unit), of (fun i j ↦ M (inl i) (inr j)) i j = 0 i j) ∨
    ¬∀ (i : Unit) (j : Fin r), of (fun i j ↦ M (inr i) (inl j)) i j = 0 i j
i : Fin r
h : M (inl i) (inr ()) ≠ 0
M' : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜 := transvection (inr ()) (inl i) 1 * M
hM' : M' (inr ()) (inr ()) ≠ 0
L L' : List (TransvectionStruct (Fin r ⊕ Unit) 𝕜)
hLL' : ((List.map toMatrix L).prod * (M' * (List.map toMatrix L').prod)).IsTwoBlockDiagonal
⊢ inr () ≠ inl i

Tactic:
simp

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

Goal state before:
pp: 𝕜 : Type u_3
inst✝ : Field 𝕜
r : ℕ
M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
hM : M (inr ()) (inr ()) = 0
H :
  (¬∀ (i : Fin r) (j : Unit), of (fun i j ↦ M (inl i) (inr j)) i j = 0 i j) ∨
    ¬∀ (i : Unit) (j : Fin r), of (fun i j ↦ M (inr i) (inl j)) i j = 0 i j
i : Fin r
h : M (inr ()) (inl i) ≠ 0
M' : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜 := M * transvection (inl i) (inr ()) 1
hM' : M' (inr ()) (inr ()) ≠ 0
L L' : List (TransvectionStruct (Fin r ⊕ Unit) 𝕜)
hLL' : ((List.map toMatrix L).prod * M' * (List.map toMatrix L').prod).IsTwoBlockDiagonal
⊢ inl i ≠ inr ()

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.MatrixPolynomialAlgebra

Goal state before:
pp: case pos
R : Type u_1
inst✝² : CommSemiring R
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
i j : n
p : R[X]
k✝ k : ℕ
x : R
h✝ : k = k✝
x✝¹ x✝ : n
⊢ single i j x x✝¹ x✝ = single i j x x✝¹ x✝

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.MatrixPolynomialAlgebra

Goal state before:
pp: case neg
R : Type u_1
inst✝² : CommSemiring R
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
i j : n
p : R[X]
k✝ k : ℕ
x : R
h✝ : ¬k = k✝
x✝¹ x✝ : n
⊢ 0 x✝¹ x✝ = single i j 0 x✝¹ x✝

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.MatrixPolynomialAlgebra

Goal state before:
pp: case refine_1
R : Type u_1
inst✝² : CommSemiring R
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
m : Matrix n n R[X]
k : ℕ
i j : n
⊢ (matPolyEquiv 0).coeff k i j = (0 i j).coeff k

Tactic:
simp

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

Goal state before:
pp: case pos
R : Type u_1
inst✝² : CommRing R
n : Type u_4
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
k : ℕ
i : n
h✝¹ : 1 = k
h✝ : k = 0
⊢ 1 - M i i = (1 - M) i i

Tactic:
simp

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

Goal state before:
pp: case neg
R : Type u_1
inst✝² : CommRing R
n : Type u_4
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
k : ℕ
i : n
h✝¹ : 1 = k
h✝ : ¬k = 0
⊢ 1 - 0 = (1 - 0) i i

Tactic:
simp

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

Goal state before:
pp: case pos
R : Type u_1
inst✝² : CommRing R
n : Type u_4
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
k : ℕ
i : n
h✝¹ : ¬1 = k
h✝ : k = 0
⊢ 0 - M i i = (0 - M) i i

Tactic:
simp

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

Goal state before:
pp: case neg
R : Type u_1
inst✝² : CommRing R
n : Type u_4
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
k : ℕ
i : n
h✝¹ : ¬1 = k
h✝ : ¬k = 0
⊢ 0 - 0 = (0 - 0) i i

Tactic:
simp

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

Goal state before:
pp: 𝕜 : Type u_3
inst✝ : Field 𝕜
r : ℕ
IH :
  ∀ (M : Matrix (Fin r) (Fin r) 𝕜),
    ∃ L₀ L₀' D₀, (List.map toMatrix L₀).prod * M * (List.map toMatrix L₀').prod = diagonal D₀
M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
⊢ ∃ L L' D, (List.map toMatrix L).prod * M * (List.map toMatrix L').prod = diagonal D

Tactic:
by
  rcases exists_isTwoBlockDiagonal_list_transvec_mul_mul_list_transvec M with ⟨L₁, L₁', hM⟩
  let M' := (L₁.map toMatrix).prod * M * (L₁'.map toMatrix).prod
  let M'' := toBlocks₁₁ M'
  rcases IH M'' with ⟨L₀, L₀', D₀, h₀⟩
  set c := M' (inr unit) (inr unit)
  refine
    ⟨L₀.map (sumInl Unit) ++ L₁, L₁' ++ L₀'.map (sumInl Unit),
      Sum.elim D₀ fun _ => M' (inr unit) (inr unit), ?_⟩
  suffices (L₀.map (toMatrix ∘ sumInl Unit)).prod * M' * (L₀'.map (toMatrix ∘ sumInl Unit)).prod =
      diagonal (Sum.elim D₀ fun _ => c) by
    simpa [M', c, Matrix.mul_assoc]
  have : M' = fromBlocks M'' 0 0 (diagonal fun _ => c) := by
    rw [← fromBlocks_toBlocks M', hM.1, hM.2]
    rfl
  rw [this]
  simp [h₀]

Goal state after:
Module: Mathlib.RingTheory.MatrixPolynomialAlgebra

Goal state before:
pp: case neg
R : Type u_1
inst✝² : CommSemiring R
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
m : Matrix n n R[X]
k : ℕ
i j i' j' : n
x : R[X]
h : ¬(i' = i ∧ j' = j)
⊢ 0 = coeff 0 k

Tactic:
simp

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

Goal state before:
pp: n : Type u_1
p : Type u_2
𝕜 : Type u_3
inst✝⁴ : Field 𝕜
inst✝³ : DecidableEq n
inst✝² : DecidableEq p
inst✝¹ : Fintype n
inst✝ : Fintype p
M : Matrix p p 𝕜
e : p ≃ n
L₀ L₀' : List (TransvectionStruct n 𝕜)
D₀ : n → 𝕜
h₀ : (List.map toMatrix L₀).prod * (reindexAlgEquiv 𝕜 𝕜 e) M * (List.map toMatrix L₀').prod = diagonal D₀
⊢ M = (reindexAlgEquiv 𝕜 𝕜 e.symm) ((reindexAlgEquiv 𝕜 𝕜 e) M)

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.MatrixPolynomialAlgebra

Goal state before:
pp: R : Type u_1
inst✝² : CommSemiring R
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
p : (Matrix n n R)[X]
i j : n
k : ℕ
⊢ p = matPolyEquiv (matPolyEquiv.symm p)

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.MatrixPolynomialAlgebra

Goal state before:
pp: case pos
R : Type u_1
inst✝² : CommSemiring R
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
p : R[X]
m : ℕ
i j : n
h✝ : i = j
⊢ p.coeff m = p.coeff m

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.MatrixPolynomialAlgebra

Goal state before:
pp: case neg
R : Type u_1
inst✝² : CommSemiring R
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
p : R[X]
m : ℕ
i j : n
h✝ : ¬i = j
⊢ coeff 0 m = 0

Tactic:
simp

Goal state after: