mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Ideal.Over

Goal state before:
pp: A : Type u_2
inst✝⁴ : CommSemiring A
B : Type u_3
inst✝³ : Semiring B
inst✝² : Algebra A B
P : Ideal B
p : Ideal A
inst✝¹ : P.LiesOver p
inst✝ : P.IsPrime
⊢ p.IsPrime

Tactic:
over_def P p

Goal state after:
A : Type u_2
inst✝⁴ : CommSemiring A
B : Type u_3
inst✝³ : Semiring B
inst✝² : Algebra A B
P : Ideal B
p : Ideal A
inst✝¹ : P.LiesOver p
inst✝ : P.IsPrime
⊢ (under A P).IsPrime
Module: Mathlib.RingTheory.Ideal.Over

Goal state before:
pp: A : Type u_2
inst✝⁷ : CommSemiring A
B : Type u_3
C : Type u_4
inst✝⁶ : Semiring B
inst✝⁵ : Semiring C
inst✝⁴ : Algebra A B
inst✝³ : Algebra A C
P : Ideal B
Q : Ideal C
p : Ideal A
inst✝² : Q.LiesOver p
F : Type u_6
inst✝¹ : FunLike F B C
inst✝ : AlgHomClass F A B C
f : F
h : P = comap f Q
⊢ p = under A (comap f Q)

Tactic:
exact (over_def Q p).trans <|
      congrFun (congrFun (congrArg
        comap ((AlgHomClass.toAlgHom f : B →ₐ[A] C).comp_algebraMap.symm)) _) Q

Goal state after:
Module: Mathlib.RingTheory.Ideal.Over

Goal state before:
pp: A : Type u_2
inst✝¹⁰ : CommSemiring A
B : Type u_3
inst✝⁹ : CommSemiring B
inst✝⁸ : Algebra A B
P : Ideal B
C : Type u_5
D : Type u_6
inst✝⁷ : CommSemiring C
inst✝⁶ : Semiring D
inst✝⁵ : Algebra A C
inst✝⁴ : Algebra C D
inst✝³ : Algebra A D
inst✝² : Algebra B D
inst✝¹ : IsScalarTower A C D
inst✝ : IsScalarTower A B D
⊢ under A P ≤ comap (algebraMap A B) (comap (algebraMap B D) (map (algebraMap B D) P))

Tactic:
exact comap_mono <| le_comap_map

Goal state after:
Module: Mathlib.RingTheory.IsPrimary

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
S : Submodule R M
x✝ : S ≠ ⊤
⊢ (∀ {r : R} {x : M}, r • x ∈ S → x ∈ S ∨ ∃ n, r ^ n • ⊤ ≤ S) ↔
    ∀ (r : R) (x : M), S.mkQ x ≠ 0 → S.mkQ (r • x) = 0 → ∃ n, r ^ n • ⊤ = ⊥

Tactic:
ne_eq,

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
S : Submodule R M
x✝ : S ≠ ⊤
⊢ (∀ {r : R} {x : M}, r • x ∈ S → x ∈ S ∨ ∃ n, r ^ n • ⊤ ≤ S) ↔
    ∀ (r : R) (x : M), ¬S.mkQ x = 0 → S.mkQ (r • x) = 0 → ∃ n, r ^ n • ⊤ = ⊥
Module: Mathlib.Algebra.Module.LocalizedModule.Submodule

Goal state before:
pp: R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
inst✝¹⁰ : CommSemiring R
inst✝⁹ : CommSemiring S
inst✝⁸ : AddCommMonoid M
inst✝⁷ : AddCommMonoid N
inst✝⁶ : Module R M
inst✝⁵ : Module R N
inst✝⁴ : Algebra R S
inst✝³ : Module S N
inst✝² : IsScalarTower R S N
p : Submonoid R
inst✝¹ : IsLocalization p S
f : M →ₗ[R] N
inst✝ : IsLocalizedModule p f
M' M'' : Submodule R M
r : R
x : N
m : M
hm : m ∈ M'
s : ↥p
hx : IsLocalizedModule.mk' f m s = x
⊢ r • x ∈ {x | ∃ m ∈ M', ∃ s, IsLocalizedModule.mk' f m s = x}

Tactic:
exact ⟨r • m, smul_mem M' _ hm, s, by rw [IsLocalizedModule.mk'_smul, hx]⟩

Goal state after:
Module: Mathlib.RingTheory.Nilpotent.Lemmas

Goal state before:
pp: case mp
R : Type u_1
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
a : A
⊢ IsNilpotent (mulLeft R a) → IsNilpotent a

Tactic:
rintro ⟨n, hn⟩

Goal state after:
case mp
R : Type u_1
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
a : A
n : ℕ
hn : mulLeft R a ^ n = 0
⊢ IsNilpotent a
Module: Mathlib.RingTheory.Nilpotent.Lemmas

Goal state before:
pp: case mpr
R : Type u_1
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
a : A
⊢ IsNilpotent a → IsNilpotent (mulLeft R a)

Tactic:
rintro ⟨n, hn⟩

Goal state after:
case mpr
R : Type u_1
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
a : A
n : ℕ
hn : a ^ n = 0
⊢ IsNilpotent (mulLeft R a)
Module: Mathlib.RingTheory.Nilpotent.Lemmas

Goal state before:
pp: case mp
R : Type u_1
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
a : A
⊢ IsNilpotent (mulRight R a) → IsNilpotent a

Tactic:
rintro ⟨n, hn⟩

Goal state after:
case mp
R : Type u_1
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
a : A
n : ℕ
hn : mulRight R a ^ n = 0
⊢ IsNilpotent a
Module: Mathlib.RingTheory.Nilpotent.Lemmas

Goal state before:
pp: case mpr
R : Type u_1
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
a : A
⊢ IsNilpotent a → IsNilpotent (mulRight R a)

Tactic:
rintro ⟨n, hn⟩

Goal state after:
case mpr
R : Type u_1
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
a : A
n : ℕ
hn : a ^ n = 0
⊢ IsNilpotent (mulRight R a)
Module: Mathlib.RingTheory.Localization.Ideal

Goal state before:
pp: case a
R : Type u_1
inst✝ : CommSemiring R
S : Finset R
hS : Ideal.span ↑S = ⊤
I : Ideal R
x s : R
hs : s ∈ ↑S
hx : ∀ i ∈ S, (algebraMap R (Localization.Away i)) x ∈ Ideal.map (algebraMap R (Localization.Away i)) I
y : ↥I
n m : ℕ
e : ↑⟨(fun x ↦ s ^ x) m, ⋯⟩ * (x * s ^ n) = ↑⟨(fun x ↦ s ^ x) m, ⋯⟩ * ↑y
⊢ ∃ n, ↑⟨s, hs⟩ ^ n • x ∈ I

Tactic:
use m + n

Goal state after:
case h
R : Type u_1
inst✝ : CommSemiring R
S : Finset R
hS : Ideal.span ↑S = ⊤
I : Ideal R
x s : R
hs : s ∈ ↑S
hx : ∀ i ∈ S, (algebraMap R (Localization.Away i)) x ∈ Ideal.map (algebraMap R (Localization.Away i)) I
y : ↥I
n m : ℕ
e : ↑⟨(fun x ↦ s ^ x) m, ⋯⟩ * (x * s ^ n) = ↑⟨(fun x ↦ s ^ x) m, ⋯⟩ * ↑y
⊢ ↑⟨s, hs⟩ ^ (m + n) • x ∈ I
Module: Mathlib.RingTheory.Localization.Ideal

Goal state before:
pp: R : Type u_1
inst✝¹⁶ : CommRing R
S : Type u_2
inst✝¹⁵ : CommRing S
inst✝¹⁴ : Algebra R S
inst✝¹³ : IsDomain R
inst✝¹² : IsDomain S
Rₚ : Type u_3
Sₚ : Type u_4
inst✝¹¹ : CommRing Rₚ
inst✝¹⁰ : IsDomain Rₚ
inst✝⁹ : CommRing Sₚ
inst✝⁸ : Algebra R Rₚ
inst✝⁷ : Algebra R Sₚ
inst✝⁶ : Algebra S Sₚ
inst✝⁵ : Algebra Rₚ Sₚ
inst✝⁴ : IsScalarTower R S Sₚ
inst✝³ : IsScalarTower R Rₚ Sₚ
M : Submonoid R
hM : M ≤ R⁰
inst✝² : IsLocalization M Rₚ
inst✝¹ : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₚ
inst✝ : Module.IsTorsionFree R S
e : Algebra.algebraMapSubmonoid S M ≤ S⁰
this✝ : IsDomain Sₚ
this : algebraMap Rₚ Sₚ = map Sₚ (algebraMap R S) ⋯
⊢ Module.IsTorsionFree Rₚ Sₚ

Tactic:
rw [Module.isTorsionFree_iff_algebraMap_injective, RingHom.injective_iff_ker_eq_bot,
    RingHom.ker_eq_bot_iff_eq_zero]

Goal state after:
R : Type u_1
inst✝¹⁶ : CommRing R
S : Type u_2
inst✝¹⁵ : CommRing S
inst✝¹⁴ : Algebra R S
inst✝¹³ : IsDomain R
inst✝¹² : IsDomain S
Rₚ : Type u_3
Sₚ : Type u_4
inst✝¹¹ : CommRing Rₚ
inst✝¹⁰ : IsDomain Rₚ
inst✝⁹ : CommRing Sₚ
inst✝⁸ : Algebra R Rₚ
inst✝⁷ : Algebra R Sₚ
inst✝⁶ : Algebra S Sₚ
inst✝⁵ : Algebra Rₚ Sₚ
inst✝⁴ : IsScalarTower R S Sₚ
inst✝³ : IsScalarTower R Rₚ Sₚ
M : Submonoid R
hM : M ≤ R⁰
inst✝² : IsLocalization M Rₚ
inst✝¹ : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₚ
inst✝ : Module.IsTorsionFree R S
e : Algebra.algebraMapSubmonoid S M ≤ S⁰
this✝ : IsDomain Sₚ
this : algebraMap Rₚ Sₚ = map Sₚ (algebraMap R S) ⋯
⊢ ∀ (x : Rₚ), (algebraMap Rₚ Sₚ) x = 0 → x = 0
Module: Mathlib.RingTheory.EssentialFiniteness

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : CommRing T
inst✝² : Algebra R S
inst✝¹ : Algebra R T
inst✝ : FiniteType R S
⊢ EssFiniteType R S

Tactic:
obtain ⟨s, hs⟩ := ‹FiniteType R S›
  rw [essFiniteType_iff]
  exact ⟨s, fun _ ↦ by simpa only [hs, mem_top, and_true, true_and] using ⟨1, isUnit_one⟩⟩

Goal state after:
Module: Mathlib.LinearAlgebra.TensorProduct.Quotient

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
m : Submodule R M
n : Submodule R N
x : N
hx : x ∈ n
y : M
⊢ (((mk R M N).flip.compr₂ ((map m.subtype LinearMap.id).range ⊔ (map LinearMap.id n.subtype).range).mkQ) x) y = 0 y

Tactic:
simp only [LinearMap.compr₂_apply, LinearMap.flip_apply, mk_apply, Submodule.mkQ_apply,
        LinearMap.zero_apply, Submodule.Quotient.mk_eq_zero]

Goal state after:
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
m : Submodule R M
n : Submodule R N
x : N
hx : x ∈ n
y : M
⊢ y ⊗ₜ[R] x ∈ (map m.subtype LinearMap.id).range ⊔ (map LinearMap.id n.subtype).range
Module: Mathlib.RingTheory.EssentialFiniteness

Goal state before:
pp: case h.tmul
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : CommRing T
inst✝³ : Algebra R S
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
σ : Finset S
hσ : ∀ (s : S), ∃ t ∈ adjoin R ↑σ, IsUnit t ∧ s * t ∈ adjoin R ↑σ
x : T
y t : S
h₁ : t ∈ adjoin R ↑σ
h₂ : IsUnit t
h₃ : y * t ∈ adjoin R ↑σ
H : ∀ x ∈ adjoin R ↑σ, 1 ⊗ₜ[R] x ∈ adjoin T ↑(Finset.image (⇑TensorProduct.includeRight) σ)
⊢ x ⊗ₜ[R] y * TensorProduct.includeRight t ∈ adjoin T ↑(Finset.image (⇑TensorProduct.includeRight) σ)

Tactic:
simp only [Algebra.TensorProduct.includeRight_apply, Algebra.TensorProduct.tmul_mul_tmul,
      mul_one]

Goal state after:
case h.tmul
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : CommRing T
inst✝³ : Algebra R S
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
σ : Finset S
hσ : ∀ (s : S), ∃ t ∈ adjoin R ↑σ, IsUnit t ∧ s * t ∈ adjoin R ↑σ
x : T
y t : S
h₁ : t ∈ adjoin R ↑σ
h₂ : IsUnit t
h₃ : y * t ∈ adjoin R ↑σ
H : ∀ x ∈ adjoin R ↑σ, 1 ⊗ₜ[R] x ∈ adjoin T ↑(Finset.image (⇑TensorProduct.includeRight) σ)
⊢ x ⊗ₜ[R] (y * t) ∈ adjoin T ↑(Finset.image (⇑TensorProduct.includeRight) σ)
Module: Mathlib.LinearAlgebra.Matrix.Adjugate

Goal state before:
pp: n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
i j : n
⊢ ∀ x ∈ univ,
    ↑↑(sign x) * ∏ i_1, A.updateRow i (Pi.single j 1) (x i_1) i_1 =
      ↑↑(sign x) * ∏ i_1, A.updateCol j (Pi.single i 1) (x i_1) i_1

Tactic:
intro σ

Goal state after:
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
i j : n
σ : Perm n
⊢ σ ∈ univ →
    ↑↑(sign σ) * ∏ i_1, A.updateRow i (Pi.single j 1) (σ i_1) i_1 =
      ↑↑(sign σ) * ∏ i_1, A.updateCol j (Pi.single i 1) (σ i_1) i_1
Module: Mathlib.LinearAlgebra.Matrix.Adjugate

Goal state before:
pp: n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
b : n → α
⊢ A.cramer b = A.adjugate *ᵥ b

Tactic:
by
  nth_rw 2 [← A.transpose_transpose]
  rw [← adjugate_transpose, adjugate_def]
  have : b = ∑ i, b i • (Pi.single i 1 : n → α) := by
    refine (pi_eq_sum_univ b).trans ?_
    congr with j
    simp [Pi.single_apply, eq_comm]
  conv_lhs =>
    rw [this]
  ext k
  simp [mulVec, dotProduct, mul_comm]

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

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

Tactic:
fin_cases i <;> fin_cases j

Goal state after:
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, ⋯⟩)

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, ⋯⟩)

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, ⋯⟩)

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, ⋯⟩)
Module: Mathlib.LinearAlgebra.Matrix.Invertible

Goal state before:
pp: m : Type u_1
n : Type u_2
α : Type u_3
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : Semiring α
A : Matrix m n α
B : Matrix n n α
inst✝ : Invertible B
⊢ A * ⅟B * B = A

Tactic:
Matrix.mul_assoc,

Goal state after:
m : Type u_1
n : Type u_2
α : Type u_3
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : Semiring α
A : Matrix m n α
B : Matrix n n α
inst✝ : Invertible B
⊢ A * (⅟B * B) = A
Module: Mathlib.LinearAlgebra.Matrix.Invertible

Goal state before:
pp: m : Type u_1
n : Type u_2
α : Type u_3
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : Semiring α
A : Matrix m n α
B : Matrix n n α
inst✝ : Invertible B
⊢ A * B * ⅟B = A

Tactic:
Matrix.mul_assoc,

Goal state after:
m : Type u_1
n : Type u_2
α : Type u_3
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : Semiring α
A : Matrix m n α
B : Matrix n n α
inst✝ : Invertible B
⊢ A * (B * ⅟B) = A
Module: Mathlib.LinearAlgebra.Matrix.Adjugate

Goal state before:
pp: case left
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
hA : IsLeftRegular A.det
B C : Matrix n n α
h : A * B = A * C
⊢ A.adjugate * A * B = A.adjugate * A * C

Tactic:
Matrix.mul_assoc,

Goal state after:
case left
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
hA : IsLeftRegular A.det
B C : Matrix n n α
h : A * B = A * C
⊢ A.adjugate * (A * B) = A.adjugate * A * C
Module: Mathlib.LinearAlgebra.Matrix.Adjugate

Goal state before:
pp: case left
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
hA : IsLeftRegular A.det
B C : Matrix n n α
h : A * B = A * C
⊢ A.adjugate * (A * B) = A.adjugate * A * C

Tactic:
Matrix.mul_assoc,

Goal state after:
case left
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
hA : IsLeftRegular A.det
B C : Matrix n n α
h : A * B = A * C
⊢ A.adjugate * (A * B) = A.adjugate * (A * C)
Module: Mathlib.LinearAlgebra.Matrix.Adjugate

Goal state before:
pp: n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A B : Matrix n n α
hA : IsLeftRegular A.det
hB : IsLeftRegular B.det
hAB : IsLeftRegular (A * B).det
⊢ (A * B).det • 1 = A * B * (B.adjugate * A.adjugate)

Tactic:
Matrix.mul_assoc,

Goal state after:
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A B : Matrix n n α
hA : IsLeftRegular A.det
hB : IsLeftRegular B.det
hAB : IsLeftRegular (A * B).det
⊢ (A * B).det • 1 = A * (B * (B.adjugate * A.adjugate))
Module: Mathlib.LinearAlgebra.Matrix.NonsingularInverse

Goal state before:
pp: m : Type u
inst✝² : DecidableEq m
R : Type u_2
inst✝¹ : CommRing R
inst✝ : Fintype m
A : Matrix m m R
⊢ (Function.Surjective fun v ↦ v ᵥ* A) ↔ IsUnit A

Tactic:
by
  rw [vecMul_surjective_iff_exists_left_inverse, isUnit_iff_exists_inv']

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

Goal state before:
pp: n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A : Matrix n n α
h : IsUnit A.det
⊢ A * A⁻¹ * A⁻¹⁻¹ = A

Tactic:
Matrix.mul_assoc,

Goal state after:
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A : Matrix n n α
h : IsUnit A.det
⊢ A * (A⁻¹ * A⁻¹⁻¹) = A
Module: Mathlib.LinearAlgebra.Matrix.NonsingularInverse

Goal state before:
pp: n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
v : n → α
⊢ (diagonal v)⁻¹ = diagonal v⁻¹ʳ

Tactic:
rw [nonsing_inv_eq_ringInverse]

Goal state after:
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
v : n → α
⊢ (diagonal v)⁻¹ʳ = diagonal v⁻¹ʳ
Module: Mathlib.LinearAlgebra.Matrix.Transvection

Goal state before:
pp: case neg
𝕜 : Type u_3
inst✝ : Field 𝕜
r : ℕ
M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
H : ¬M.IsTwoBlockDiagonal
⊢ ∃ L L', ((List.map toMatrix L).prod * M * (List.map toMatrix L').prod).IsTwoBlockDiagonal

Tactic:
by_cases hM : M (inr unit) (inr unit) = 0

Goal state after:
case pos
𝕜 : Type u_3
inst✝ : Field 𝕜
r : ℕ
M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
H : ¬M.IsTwoBlockDiagonal
hM : M (inr ()) (inr ()) = 0
⊢ ∃ L L', ((List.map toMatrix L).prod * M * (List.map toMatrix L').prod).IsTwoBlockDiagonal

case neg
𝕜 : Type u_3
inst✝ : Field 𝕜
r : ℕ
M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
H : ¬M.IsTwoBlockDiagonal
hM : ¬M (inr ()) (inr ()) = 0
⊢ ∃ L L', ((List.map toMatrix L).prod * M * (List.map toMatrix L').prod).IsTwoBlockDiagonal
Module: Mathlib.LinearAlgebra.Matrix.SchurComplement

Goal state before:
pp: m : Type u_2
n : Type u_3
α : Type u_4
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A : Matrix m n α
B : Matrix n m α
⊢ (1 - B * -A).det = (1 + B * A).det

Tactic:
Matrix.mul_neg,

Goal state after:
m : Type u_2
n : Type u_3
α : Type u_4
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A : Matrix m n α
B : Matrix n m α
⊢ (1 - -(B * A)).det = (1 + B * A).det
Module: Mathlib.LinearAlgebra.Matrix.SchurComplement

Goal state before:
pp: m : Type u_2
n : Type u_3
α : Type u_4
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A : Matrix m n α
B : Matrix n m α
⊢ (1 + B * -A).det = (1 - B * A).det

Tactic:
Matrix.mul_neg,

Goal state after:
m : Type u_2
n : Type u_3
α : Type u_4
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A : Matrix m n α
B : Matrix n m α
⊢ (1 + -(B * A)).det = (1 - B * A).det
Module: Mathlib.RingTheory.Nilpotent.Basic

Goal state before:
pp: R : Type u_1
x : R
inst✝ : Ring R
h : IsNilpotent x
⊢ IsNilpotent (-x)

Tactic:
obtain ⟨n, hn⟩ := h
  use n
  rw [neg_pow, hn, mul_zero]

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

Goal state before:
pp: ι : Type u_1
inst✝⁴ : Fintype ι
M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_3
inst✝² : CommRing R
inst✝¹ : Module R M
b : ι → M
inst✝ : DecidableEq ι
f : Module.End R M
i : ι
⊢ ((fromEnd R b) f) (Pi.single i 1) = f (b i)

Tactic:
by
  rw [PiToModule.fromEnd_apply, Fintype.linearCombination_apply_single, one_smul]

Goal state after:
Module: Mathlib.Algebra.Module.SpanRank

Goal state before:
pp: case inl
R : Type u_1
M : Type u
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p : Submodule R M
h1 : ⨅ s, ⨅ (_ : span R s = p), s.encard = ⊤
⊢ ⨅ s, ⨅ (_ : span R s = p), s.encard = ⨅ s, ↑(↑s).card

Tactic:
rw [h1, eq_comm]; simp_rw [iInf_eq_top] at h1 ⊢
    exact fun s ↦ False.elim (Set.encard_ne_top_iff.mpr s.1.finite_toSet (h1 s.1 s.2))

Goal state after:
Module: Mathlib.RingTheory.Finiteness.Subalgebra

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
M : Submodule R A
h : M.FG
n✝ n : ℕ
ih : (M ^ n).FG
⊢ (M ^ n.succ).FG

Tactic:
by simpa [pow_succ] using ih.mul h

Goal state after:
Module: Mathlib.Algebra.Module.SpanRank

Goal state before:
pp: case mpr
R : Type u_1
M : Type u
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p : Submodule R M
a : Cardinal.{max u v}
⊢ (∃ s, lift.{v, u} #↑s ≤ a ∧ span R s = p) → lift.{v, u} p.spanRank ≤ a

Tactic:
exact fun ⟨s, ⟨h₁, h₂⟩⟩ ↦ h₂.symm ▸ (Cardinal.lift_le.mpr (spanRank_span_le_card s)).trans h₁

Goal state after:
Module: Mathlib.Algebra.Module.SpanRank

Goal state before:
pp: R : Type u_1
M : Type u
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p : Submodule R M
h : p.spanFinrank = 1
fg : p.FG
⊢ p.IsPrincipal

Tactic:
obtain ⟨a, ha⟩ : ∃ a, p.generators = {a} := by simpa [← fg.generators_ncard] using h

Goal state after:
R : Type u_1
M : Type u
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p : Submodule R M
h : p.spanFinrank = 1
fg : p.FG
a : M
ha : p.generators = {a}
⊢ p.IsPrincipal
Module: Mathlib.Data.Nat.Choose.Vandermonde

Goal state before:
pp: m n k : ℕ
⊢ ((X + 1) ^ (m + n)).coeff k = ((X + 1) ^ m * (X + 1) ^ n).coeff k

Tactic:
pow_add

Goal state after:
m n k : ℕ
⊢ ((X + 1) ^ m * (X + 1) ^ n).coeff k = ((X + 1) ^ m * (X + 1) ^ n).coeff k
Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff

Goal state before:
pp: R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
⊢ M.charpolyRev.coeff 1 = -M.trace

Tactic:
by
  nontriviality R
  cases isEmpty_or_nonempty n
  · simp [charpolyRev, coeff_one]
  · simp [trace_eq_neg_charpoly_coeff M, ← M.reverse_charpoly, nextCoeff]

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

Goal state before:
pp: R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
s : Finset n
e : ↥s ⊕ { a // a ∉ s } ≃ n := Equiv.sumCompl fun x ↦ x ∈ s
⊢ (of (s.piecewise M.row (row 1))).det = (M.submatrix Subtype.val Subtype.val).det

Tactic:
let +generalize A : Matrix n n R := Matrix.of (s.piecewise M (1 : Matrix n n R))

Goal state after:
R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
s : Finset n
e : ↥s ⊕ { a // a ∉ s } ≃ n := Equiv.sumCompl fun x ↦ x ∈ s
A : Matrix n n R := of (s.piecewise M 1)
⊢ A.det = (M.submatrix Subtype.val Subtype.val).det
Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff

Goal state before:
pp: R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
s : Finset n
e : ↥s ⊕ { a // a ∉ s } ≃ n := Equiv.sumCompl fun x ↦ x ∈ s
A : Matrix n n R := of (s.piecewise M 1)
⊢ (A.submatrix ⇑e ⇑e).det = (M.submatrix Subtype.val Subtype.val).det

Tactic:
have h_blocks : A.submatrix e e =
      Matrix.fromBlocks
        (M.submatrix Subtype.val Subtype.val)
        (M.submatrix Subtype.val Subtype.val) 0 1 := by
    ext (i | i) (j | j) <;> dsimp [A, e]
    · simp only [Finset.piecewise, if_pos i.prop]
    · simp only [Finset.piecewise, if_pos i.prop]
    · simp only [Finset.piecewise, if_neg i.prop]
      exact Matrix.one_apply_ne (fun h => i.prop (h ▸ j.prop))
    · simp only [Finset.piecewise, if_neg i.prop, Matrix.one_apply, Subtype.ext_iff]

Goal state after:
R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
s : Finset n
e : ↥s ⊕ { a // a ∉ s } ≃ n := Equiv.sumCompl fun x ↦ x ∈ s
A : Matrix n n R := of (s.piecewise M 1)
h_blocks :
  A.submatrix ⇑e ⇑e = fromBlocks (M.submatrix Subtype.val Subtype.val) (M.submatrix Subtype.val Subtype.val) 0 1
⊢ (A.submatrix ⇑e ⇑e).det = (M.submatrix Subtype.val Subtype.val).det
Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff

Goal state before:
pp: R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
k : ℕ
D : (n → R[X]) [⋀^n]→ₗ[R[X]] R[X] := detRowAlternating
s : Finset n
i j : n
n✝ : ℕ
⊢ ((if i ∈ s then M.map (⇑C) i else 1 i) j).coeff n✝ = (C ((if i ∈ s then M i else 1 i) j)).coeff n✝

Tactic:
split_ifs with h <;> simp [Matrix.one_apply]

Goal state after:
Module: Mathlib.RingTheory.Polynomial.ScaleRoots

Goal state before:
pp: case inr.inr.h
R : Type u_1
inst✝ : CommRing R
p : R[X]
r a : R
hr : IsLeftRegular r
h✝ : Nontrivial R
hp : p ≠ 0
q : R[X]
e : p = (X - C a) ^ rootMultiplicity a p * q
hq : ¬X - C a ∣ q
hq0 : q ≠ 0
⊢ q.leadingCoeff ≠ 0

Tactic:
ne_eq,

Goal state after:
case inr.inr.h
R : Type u_1
inst✝ : CommRing R
p : R[X]
r a : R
hr : IsLeftRegular r
h✝ : Nontrivial R
hp : p ≠ 0
q : R[X]
e : p = (X - C a) ^ rootMultiplicity a p * q
hq : ¬X - C a ∣ q
hq0 : q ≠ 0
⊢ ¬q.leadingCoeff = 0
Module: Mathlib.Algebra.Polynomial.Splits

Goal state before:
pp: R : Type u_1
inst✝ : Field R
f : R[X]
hf : f.Splits
x : R
hx : eval x f ≠ 0
z : R
hz : z ∈ f.roots
⊢ f.leadingCoeff * (Multiset.map (fun x_1 ↦ x - x_1) (f.roots.erase z)).prod =
    f.leadingCoeff * ((x - z) * (Multiset.map (fun x_1 ↦ x - x_1) (f.roots.erase z)).prod * (1 / (x - z)))

Tactic:
mul_one_div,

Goal state after:
R : Type u_1
inst✝ : Field R
f : R[X]
hf : f.Splits
x : R
hx : eval x f ≠ 0
z : R
hz : z ∈ f.roots
⊢ f.leadingCoeff * (Multiset.map (fun x_1 ↦ x - x_1) (f.roots.erase z)).prod =
    f.leadingCoeff * ((x - z) * (Multiset.map (fun x_1 ↦ x - x_1) (f.roots.erase z)).prod / (x - z))