mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Localization.LocalizationLocalization

Goal state before:
pp: case mpr
R : Type u_1
inst✝² : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
N : Submonoid S
x : R
⊢ (∃ y z, (algebraMap R S) x = ↑y * (algebraMap R S) ↑z) →
    ∃ y ∈ N, ∃ z ∈ Submonoid.map (algebraMap R S) M, y * z = (algebraMap R S) x

Tactic:
· rintro ⟨y, z, e⟩
    exact ⟨y, y.prop, _, ⟨z, z.prop, rfl⟩, e.symm⟩

Goal state after:
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✝ : EssFiniteType R S
⊢ FiniteType R ↥(EssFiniteType.subalgebra R S)

Tactic:
constructor
  rw [Subalgebra.fg_top, EssFiniteType.subalgebra]
  exact ⟨_, rfl⟩

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

Goal state before:
pp: R : Type u_1
inst✝³ : CommSemiring R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
P : Ideal R
hp : P.IsPrime
inst✝ : IsLocalization.AtPrime S P
this✝ : Nontrivial S := nontrivial S P
x y : S
hx : x ∈ nonunits S
hy : y ∈ nonunits S
hu : IsUnit (x + y)
z : S
this : ∀ {r : R} {s : ↥P.primeCompl}, mk' S r s ∈ nonunits S → r ∈ P
rx : R
sx : ↥P.primeCompl
hrx : mk' S rx sx = x
ry : R
sy : ↥P.primeCompl
hry : mk' S ry sy = y
rz : R
sz : ↥P.primeCompl
hxyz : mk' S ((rx * ↑sy + ry * ↑sx) * rz) (sx * sy * sz) = mk' S 1 ⟨1, ⋯⟩
hrz : mk' S rz sz = z
⊢ False

Tactic:
rw [← hrx] at hx

Goal state after:
R : Type u_1
inst✝³ : CommSemiring R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
P : Ideal R
hp : P.IsPrime
inst✝ : IsLocalization.AtPrime S P
this✝ : Nontrivial S := nontrivial S P
x y : S
hy : y ∈ nonunits S
hu : IsUnit (x + y)
z : S
this : ∀ {r : R} {s : ↥P.primeCompl}, mk' S r s ∈ nonunits S → r ∈ P
rx : R
sx : ↥P.primeCompl
hx : mk' S rx sx ∈ nonunits S
hrx : mk' S rx sx = x
ry : R
sy : ↥P.primeCompl
hry : mk' S ry sy = y
rz : R
sz : ↥P.primeCompl
hxyz : mk' S ((rx * ↑sy + ry * ↑sx) * rz) (sx * sy * sz) = mk' S 1 ⟨1, ⋯⟩
hrz : mk' S rz sz = z
⊢ False
Module: Mathlib.RingTheory.EssentialFiniteness

Goal state before:
pp: case h.add
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 y tx : T ⊗[R] S
hx₁ : tx ∈ adjoin T ↑(Finset.image (⇑TensorProduct.includeRight) σ)
hx₂ : IsUnit tx
hx₃ : x * tx ∈ adjoin T ↑(Finset.image (⇑TensorProduct.includeRight) σ)
ty : T ⊗[R] S
hy₁ : ty ∈ adjoin T ↑(Finset.image (⇑TensorProduct.includeRight) σ)
hy₂ : IsUnit ty
hy₃ : y * ty ∈ adjoin T ↑(Finset.image (⇑TensorProduct.includeRight) σ)
⊢ (x + y) * (tx * ty) ∈ adjoin T ↑(Finset.image (⇑TensorProduct.includeRight) σ)

Tactic:
add_mul,

Goal state after:
case h.add
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 y tx : T ⊗[R] S
hx₁ : tx ∈ adjoin T ↑(Finset.image (⇑TensorProduct.includeRight) σ)
hx₂ : IsUnit tx
hx₃ : x * tx ∈ adjoin T ↑(Finset.image (⇑TensorProduct.includeRight) σ)
ty : T ⊗[R] S
hy₁ : ty ∈ adjoin T ↑(Finset.image (⇑TensorProduct.includeRight) σ)
hy₂ : IsUnit ty
hy₃ : y * ty ∈ adjoin T ↑(Finset.image (⇑TensorProduct.includeRight) σ)
⊢ x * (tx * ty) + y * (tx * ty) ∈ adjoin T ↑(Finset.image (⇑TensorProduct.includeRight) σ)
Module: Mathlib.Algebra.Ring.Regular

Goal state before:
pp: α : Type u_1
inst✝ : Ring α
h : ∀ (x y z : α), x * z = 1 → y * z = 1 → x = y
x y : α
eq : x * y = 1
⊢ (1 - y * x + x) * y = 1

Tactic:
add_mul,

Goal state after:
α : Type u_1
inst✝ : Ring α
h : ∀ (x y z : α), x * z = 1 → y * z = 1 → x = y
x y : α
eq : x * y = 1
⊢ (1 - y * x) * y + x * y = 1
Module: Mathlib.LinearAlgebra.Matrix.Symmetric

Goal state before:
pp: α : Type u_1
β : Type u_2
n : Type u_3
A : Matrix n n α
f : α → β
hf : Function.Injective f
⊢ Aᵀ.map f = A.map f ↔ Aᵀ = A

Tactic:
map_injective hf |>.eq_iff

Goal state after:
α : Type u_1
β : Type u_2
n : Type u_3
A : Matrix n n α
f : α → β
hf : Function.Injective f
⊢ Aᵀ = A ↔ Aᵀ = A
Module: Mathlib.Algebra.Polynomial.Laurent

Goal state before:
pp: case e'_3
R : Type u_1
inst✝ : Semiring R
r : R
⊢ C r = C r * T ↑0

Tactic:
simp only [Int.ofNat_zero, T_zero, mul_one]

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

Goal state before:
pp: n : Type u_1
p : Type u_2
R : Type u₂
inst✝² : DecidableEq n
inst✝¹ : DecidableEq p
inst✝ : CommRing R
t : TransvectionStruct n R
⊢ (sumInl p t).toMatrix = fromBlocks t.toMatrix 0 0 1

Tactic:
cases t
  ext a b
  rcases a with a | a <;> rcases b with b | b
  · by_cases h : a = b <;> simp [TransvectionStruct.sumInl, transvection, h, single]
  · simp [TransvectionStruct.sumInl, transvection]
  · simp [TransvectionStruct.sumInl, transvection]
  · by_cases h : a = b <;> simp [TransvectionStruct.sumInl, transvection, h]

Goal state after:
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 n n α
B : Matrix n m α
inst✝ : Invertible A
⊢ ⅟A * A * B = B

Tactic:
invOf_mul_self,

Goal state after:
m : Type u_1
n : Type u_2
α : Type u_3
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : Semiring α
A : Matrix n n α
B : Matrix n m α
inst✝ : Invertible A
⊢ 1 * B = B
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:
invOf_mul_self,

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 * 1 = 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✝¹ : CommSemiring α
A : Matrix n n α
inst✝ : Invertible A
⊢ (⅟A * A)ᵀ = 1

Tactic:
invOf_mul_self,

Goal state after:
m : Type u_1
n : Type u_2
α : Type u_3
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : CommSemiring α
A : Matrix n n α
inst✝ : Invertible A
⊢ 1ᵀ = 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✝⁵ : Fintype m
inst✝⁴ : DecidableEq m
inst✝³ : Ring α
A : Matrix n n α
U : Matrix n m α
C : Matrix m m α
V : Matrix m n α
inst✝² : Invertible A
inst✝¹ : Invertible C
inst✝ : Invertible (⅟C + V * ⅟A * U)
⊢ (A + U * C * V) * (⅟A - ⅟A * U * ⅟(⅟C + V * ⅟A * U) * V * ⅟A) =
    A * ⅟A - A * ⅟A * U * ⅟(⅟C + V * ⅟A * U) * V * ⅟A +
      (U * C * V * ⅟A - U * C * V * ⅟A * U * ⅟(⅟C + V * ⅟A * U) * V * ⅟A)

Tactic:
add_mul,

Goal state after:
m : Type u_1
n : Type u_2
α : Type u_3
inst✝⁷ : Fintype n
inst✝⁶ : DecidableEq n
inst✝⁵ : Fintype m
inst✝⁴ : DecidableEq m
inst✝³ : Ring α
A : Matrix n n α
U : Matrix n m α
C : Matrix m m α
V : Matrix m n α
inst✝² : Invertible A
inst✝¹ : Invertible C
inst✝ : Invertible (⅟C + V * ⅟A * U)
⊢ A * (⅟A - ⅟A * U * ⅟(⅟C + V * ⅟A * U) * V * ⅟A) + U * C * V * (⅟A - ⅟A * U * ⅟(⅟C + V * ⅟A * U) * V * ⅟A) =
    A * ⅟A - A * ⅟A * U * ⅟(⅟C + V * ⅟A * U) * V * ⅟A +
      (U * C * V * ⅟A - U * C * V * ⅟A * U * ⅟(⅟C + V * ⅟A * U) * V * ⅟A)
Module: Mathlib.LinearAlgebra.Dimension.Localization

Goal state before:
pp: R : Type u_1
inst✝¹ : Ring R
inst✝ : IsDomain R
r : R
s : ↥R⁰
h : ∀ (r' : R) (s' : ↥R⁰), ↑s' * r ≠ r' * ↑s
n : ℕ
g : ℕ → R
x : ℕ
hg : ∑ i ∈ Finset.range n, g i • (r * ↑s ^ (i + x)) = 0
i : ℕ
hin : i < n
⊢ g i = 0

Tactic:
induction n generalizing g x i with
  | zero => contradiction
  | succ n IH =>
    rw [Finset.sum_range_succ'] at hg
    by_cases hg0 : g 0 = 0
    · simp only [hg0, zero_smul, add_zero, add_assoc] at hg
      cases i; exacts [hg0, IH _ _ hg _ (Nat.succ_lt_succ_iff.mp hin)]
    simp only [zero_add, pow_add _ _ x,
      ← mul_assoc, pow_succ, ← Finset.sum_mul, smul_eq_mul] at hg
    rw [← neg_eq_iff_add_eq_zero, ← neg_mul, ← neg_mul] at hg
    have := mul_right_cancel₀ (mem_nonZeroDivisors_iff_ne_zero.mp (s ^ x).prop) hg
    exact (h _ ⟨(g 0), mem_nonZeroDivisors_iff_ne_zero.mpr (by simpa)⟩ this.symm).elim

Goal state after:
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✝⁵ : Fintype m
inst✝⁴ : DecidableEq m
inst✝³ : Ring α
A : Matrix n n α
U : Matrix n m α
C : Matrix m m α
V : Matrix m n α
inst✝² : Invertible A
inst✝¹ : Invertible C
inst✝ : Invertible (⅟C + V * ⅟A * U)
⊢ ⅟A * A - ⅟A * U * ⅟(⅟C + V * ⅟A * U) * V * ⅟A * A + ⅟A * U * C * V -
      ⅟A * U * ⅟(⅟C + V * ⅟A * U) * V * ⅟A * U * C * V =
    1 + ⅟A * U * C * V - (⅟A * U * ⅟(⅟C + V * ⅟A * U) * V + ⅟A * U * ⅟(⅟C + V * ⅟A * U) * V * ⅟A * U * C * V)

Tactic:
invOf_mul_self,

Goal state after:
m : Type u_1
n : Type u_2
α : Type u_3
inst✝⁷ : Fintype n
inst✝⁶ : DecidableEq n
inst✝⁵ : Fintype m
inst✝⁴ : DecidableEq m
inst✝³ : Ring α
A : Matrix n n α
U : Matrix n m α
C : Matrix m m α
V : Matrix m n α
inst✝² : Invertible A
inst✝¹ : Invertible C
inst✝ : Invertible (⅟C + V * ⅟A * U)
⊢ 1 - ⅟A * U * ⅟(⅟C + V * ⅟A * U) * V * ⅟A * A + ⅟A * U * C * V - ⅟A * U * ⅟(⅟C + V * ⅟A * U) * V * ⅟A * U * C * V =
    1 + ⅟A * U * C * V - (⅟A * U * ⅟(⅟C + V * ⅟A * U) * V + ⅟A * U * ⅟(⅟C + V * ⅟A * U) * V * ⅟A * U * C * V)
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.det • (1 * B) = A.det • (1 * C)

Tactic:
← Matrix.smul_mul,

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.det • 1 * B = A.det • (1 * 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.det • 1 * B = A.det • (1 * C)

Tactic:
← Matrix.smul_mul,

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.det • 1 * B = A.det • 1 * C
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✝ : Invertible A.det
⊢ (⅟A.det * A.det) • 1 = 1

Tactic:
invOf_mul_self,

Goal state after:
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✝ : Invertible A.det
⊢ 1 • 1 = 1
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
⊢ (M * (listTransvecRow M).prod) (inr ()) (inl i) = 0

Tactic:
by
    have A : (listTransvecRow M).length = r := by simp [listTransvecRow]
    rw [← List.take_length (l := listTransvecRow M), A]
    have : ¬r ≤ i := by simp
    simpa only [this, ite_eq_right_iff] using! H r le_rfl

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

Goal state before:
pp: m : Type u
n : Type u'
R : Type u_2
inst✝³ : Semiring R
inst✝² : DecidableEq n
inst✝¹ : Fintype m
inst✝ : Finite n
A : Matrix m n R
⊢ (Function.Surjective fun v ↦ v ᵥ* A) ↔ ∃ B, B * A = 1

Tactic:
cases nonempty_fintype n
  refine ⟨fun h ↦ ?_, fun ⟨B, hBA⟩ y ↦ ⟨y ᵥ* B, by simp [hBA]⟩⟩
  choose rows hrows using (h <| Pi.single · 1)
  refine ⟨Matrix.of rows, Matrix.ext fun i j => ?_⟩
  rw [mul_apply_eq_vecMul, one_eq_pi_single, ← hrows]
  rfl

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

Goal state before:
pp: case neg
α : Type u_1
m : Type u_3
R : Type v
b : m → α
inst✝² : LinearOrder α
inst✝¹ : Fintype m
inst✝ : NonUnitalNonAssocSemiring R
M N : Matrix m m R
hM : M.BlockTriangular b
hN : N.BlockTriangular b
i j : m
hij : b j < b i
k : m
a✝ : k ∈ univ
hki : b i ≤ b k
⊢ (fun j ↦ M i j) k * (fun j_1 ↦ N j_1 j) k = 0

Tactic:
· simp_rw [hN (lt_of_lt_of_le hij hki), mul_zero]

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

Goal state before:
pp: α : Type u_1
m : Type u_3
n : Type u_4
R : Type v
inst✝¹ : Zero R
inst✝ : Preorder α
A : Matrix m m R
B : Matrix m n R
D : Matrix n n R
a b : α
hab : a < b
⊢ (fromBlocks A B 0 D).BlockTriangular (Sum.elim (fun x ↦ a) fun x ↦ b)

Tactic:
rintro (c | c) (d | d) hcd

Goal state after:
case inl.inl
α : Type u_1
m : Type u_3
n : Type u_4
R : Type v
inst✝¹ : Zero R
inst✝ : Preorder α
A : Matrix m m R
B : Matrix m n R
D : Matrix n n R
a b : α
hab : a < b
c d : m
hcd : Sum.elim (fun x ↦ a) (fun x ↦ b) (Sum.inl d) < Sum.elim (fun x ↦ a) (fun x ↦ b) (Sum.inl c)
⊢ fromBlocks A B 0 D (Sum.inl c) (Sum.inl d) = 0

case inl.inr
α : Type u_1
m : Type u_3
n : Type u_4
R : Type v
inst✝¹ : Zero R
inst✝ : Preorder α
A : Matrix m m R
B : Matrix m n R
D : Matrix n n R
a b : α
hab : a < b
c : m
d : n
hcd : Sum.elim (fun x ↦ a) (fun x ↦ b) (Sum.inr d) < Sum.elim (fun x ↦ a) (fun x ↦ b) (Sum.inl c)
⊢ fromBlocks A B 0 D (Sum.inl c) (Sum.inr d) = 0

case inr.inl
α : Type u_1
m : Type u_3
n : Type u_4
R : Type v
inst✝¹ : Zero R
inst✝ : Preorder α
A : Matrix m m R
B : Matrix m n R
D : Matrix n n R
a b : α
hab : a < b
c : n
d : m
hcd : Sum.elim (fun x ↦ a) (fun x ↦ b) (Sum.inl d) < Sum.elim (fun x ↦ a) (fun x ↦ b) (Sum.inr c)
⊢ fromBlocks A B 0 D (Sum.inr c) (Sum.inl d) = 0

case inr.inr
α : Type u_1
m : Type u_3
n : Type u_4
R : Type v
inst✝¹ : Zero R
inst✝ : Preorder α
A : Matrix m m R
B : Matrix m n R
D : Matrix n n R
a b : α
hab : a < b
c d : n
hcd : Sum.elim (fun x ↦ a) (fun x ↦ b) (Sum.inr d) < Sum.elim (fun x ↦ a) (fun x ↦ b) (Sum.inr c)
⊢ fromBlocks A B 0 D (Sum.inr c) (Sum.inr d) = 0
Module: Mathlib.LinearAlgebra.Matrix.Block

Goal state before:
pp: m : Type u_3
R : Type v
inst✝³ : CommRing R
inst✝² : DecidableEq m
inst✝¹ : Fintype m
M : Matrix m m R
p : m → Prop
inst✝ : DecidablePred p
h : ∀ (i : m), ¬p i → ∀ (j : m), p j → M i j = 0
⊢ M.det = (M.toSquareBlockProp p).det * (M.toSquareBlockProp fun i ↦ ¬p i).det

Tactic:
det_toBlock M p

Goal state after:
m : Type u_3
R : Type v
inst✝³ : CommRing R
inst✝² : DecidableEq m
inst✝¹ : Fintype m
M : Matrix m m R
p : m → Prop
inst✝ : DecidablePred p
h : ∀ (i : m), ¬p i → ∀ (j : m), p j → M i j = 0
⊢ (fromBlocks (M.toBlock p p) (M.toBlock p fun j ↦ ¬p j) (M.toBlock (fun j ↦ ¬p j) p)
        (M.toBlock (fun j ↦ ¬p j) fun j ↦ ¬p j)).det =
    (M.toSquareBlockProp p).det * (M.toSquareBlockProp fun i ↦ ¬p i).det
Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Basic

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
n : Type u_4
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
f : R →+* S
⊢ (M.charmatrix.map ⇑(mapRingHom f)).det = ((mapRingHom f).mapMatrix M.charmatrix).det

Tactic:
RingHom.mapMatrix_apply

Goal state after:
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
n : Type u_4
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
f : R →+* S
⊢ (M.charmatrix.map ⇑(mapRingHom f)).det = (M.charmatrix.map ⇑(mapRingHom f)).det
Module: Mathlib.LinearAlgebra.Matrix.SchurComplement

Goal state before:
pp: l : Type u_1
m : Type u_2
n : Type u_3
α : Type u_4
inst✝⁸ : Fintype l
inst✝⁷ : Fintype m
inst✝⁶ : Fintype n
inst✝⁵ : DecidableEq l
inst✝⁴ : DecidableEq m
inst✝³ : DecidableEq n
inst✝² : CommRing α
A : Matrix m m α
B : Matrix m n α
D : Matrix n n α
inst✝¹ : Invertible A
inst✝ : Invertible D
⊢ fromBlocks (⅟A * A) (⅟A * B + -(⅟A * B * ⅟D * D)) 0 (⅟D * D) = 1

Tactic:
invOf_mul_self,

Goal state after:
l : Type u_1
m : Type u_2
n : Type u_3
α : Type u_4
inst✝⁸ : Fintype l
inst✝⁷ : Fintype m
inst✝⁶ : Fintype n
inst✝⁵ : DecidableEq l
inst✝⁴ : DecidableEq m
inst✝³ : DecidableEq n
inst✝² : CommRing α
A : Matrix m m α
B : Matrix m n α
D : Matrix n n α
inst✝¹ : Invertible A
inst✝ : Invertible D
⊢ fromBlocks 1 (⅟A * B + -(⅟A * B * ⅟D * D)) 0 1 = 1
Module: Mathlib.LinearAlgebra.Matrix.SchurComplement

Goal state before:
pp: l : Type u_1
m : Type u_2
n : Type u_3
α : Type u_4
inst✝⁸ : Fintype l
inst✝⁷ : Fintype m
inst✝⁶ : Fintype n
inst✝⁵ : DecidableEq l
inst✝⁴ : DecidableEq m
inst✝³ : DecidableEq n
inst✝² : CommRing α
A : Matrix m m α
C : Matrix n m α
D : Matrix n n α
inst✝¹ : Invertible A
inst✝ : Invertible D
⊢ fromBlocks (⅟A * A) 0 (-(⅟D * C * ⅟A * A) + ⅟D * C) (⅟D * D) = 1

Tactic:
invOf_mul_self,

Goal state after:
l : Type u_1
m : Type u_2
n : Type u_3
α : Type u_4
inst✝⁸ : Fintype l
inst✝⁷ : Fintype m
inst✝⁶ : Fintype n
inst✝⁵ : DecidableEq l
inst✝⁴ : DecidableEq m
inst✝³ : DecidableEq n
inst✝² : CommRing α
A : Matrix m m α
C : Matrix n m α
D : Matrix n n α
inst✝¹ : Invertible A
inst✝ : Invertible D
⊢ fromBlocks 1 0 (-(⅟D * C * ⅟A * A) + ⅟D * C) 1 = 1
Module: Mathlib.RingTheory.Nilpotent.Basic

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
r : R
hnil : IsNilpotent r
⊢ IsUnit (-r - 1)

Tactic:
exact isUnit_sub_one hnil.neg

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

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
r u : R
hnil : IsNilpotent r
hu : IsUnit u
h_comm : Commute r u
⊢ IsUnit ((u + r) * ↑hu.unit⁻¹)

Tactic:
add_mul,

Goal state after:
R : Type u_1
inst✝ : Ring R
r u : R
hnil : IsNilpotent r
hu : IsUnit u
h_comm : Commute r u
⊢ IsUnit (u * ↑hu.unit⁻¹ + r * ↑hu.unit⁻¹)
Module: Mathlib.RingTheory.Nilpotent.Basic

Goal state before:
pp: R : Type u_1
inst✝ : MonoidWithZero R
k : ℕ
hk : 1 < k
⊢ IsReduced R ↔ ∀ (x : R), x ^ k = 0 → x = 0

Tactic:
simp_rw [← zero_isRadical_iff, isRadical_iff_pow_one_lt k hk, zero_dvd_iff]

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 : ∀ (i : Set M), span R i = p → i.encard = ⊤
⊢ ∀ (i : { s // span R ↑s = p }), ↑(↑i).card = ⊤

Tactic:
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.LinearAlgebra.Matrix.Charpoly.LinearMap

Goal state before:
pp: case inr
M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_3
inst✝² : CommRing R
inst✝¹ : Module R M
inst✝ : Module.Finite R M
f : Module.End R M
I : Ideal R
hI : range f ≤ I • ⊤
h✝ : Nontrivial R
s : Finset M
hs_card : s.card = ⊤.spanFinrank
hs_span : Submodule.span R ↑s = ⊤
⊢ ∃ p, p.Monic ∧ p.natDegree = ⊤.spanFinrank ∧ (∀ (k : ℕ), p.coeff k ∈ I ^ (p.natDegree - k)) ∧ (aeval f) p = 0

Tactic:
have : Submodule.span R (Set.range ((↑) : s → M)) = ⊤ := by simp [hs_span]

Goal state after:
case inr
M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_3
inst✝² : CommRing R
inst✝¹ : Module R M
inst✝ : Module.Finite R M
f : Module.End R M
I : Ideal R
hI : range f ≤ I • ⊤
h✝ : Nontrivial R
s : Finset M
hs_card : s.card = ⊤.spanFinrank
hs_span : Submodule.span R ↑s = ⊤
this : Submodule.span R (Set.range Subtype.val) = ⊤
⊢ ∃ p, p.Monic ∧ p.natDegree = ⊤.spanFinrank ∧ (∀ (k : ℕ), p.coeff k ∈ I ^ (p.natDegree - k)) ∧ (aeval f) p = 0
Module: Mathlib.LinearAlgebra.Matrix.Charpoly.LinearMap

Goal state before:
pp: M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_3
inst✝² : CommRing R
inst✝¹ : Module R M
inst✝ : Module.Finite R M
I : Ideal R
h✝ : Nontrivial R
s : Finset M
hs_card : s.card = ⊤.spanFinrank
hs_span : Submodule.span R ↑s = ⊤
this : Submodule.span R (Set.range Subtype.val) = ⊤
A : ↥(isRepresentation R Subtype.val)
h : ∀ (i j : ↥s), ↑A i j ∈ I
hI : range ((isRepresentation.toEnd R Subtype.val this) A) ≤ I • ⊤
⊢ (↑A).charpoly.natDegree = ⊤.spanFinrank

Tactic:
simp [hs_card]

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
⊢ p.spanRank = ↑p.spanFinrank ↔ p.FG

Tactic:
rw [spanFinrank, ← spanRank_finite_iff_fg, eq_comm]

Goal state after:
R : Type u_1
M : Type u
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p : Submodule R M
⊢ ↑(toNat p.spanRank) = p.spanRank ↔ p.spanRank < ℵ₀
Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff

Goal state before:
pp: case neg
R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
a✝ : Nontrivial R
h : ¬Fintype.card n = 0
⊢ M.charpoly.Monic

Tactic:
have mon : (∏ i : n, (X - C (M i i))).Monic := by
    apply monic_prod_of_monic univ fun i : n => X - C (M i i)
    simp [monic_X_sub_C]

Goal state after:
case neg
R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
a✝ : Nontrivial R
h : ¬Fintype.card n = 0
mon : (∏ i, (X - C (M i i))).Monic
⊢ M.charpoly.Monic
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.det = (-1) ^ Fintype.card n * M.charpoly.coeff 0

Tactic:
by
  rw [coeff_zero_eq_eval_zero, charpoly, eval_det, matPolyEquiv_charmatrix, ← det_smul]
  simp

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Free R M
inst✝ : StrongRankCondition R
⊢ Module.rank R M = ⊤.spanRank

Tactic:
by
  have := nontrivial_of_invariantBasisNumber R
  obtain ⟨I, B⟩ := ‹Module.Free R M›
  rw [← Basis.mk_eq_rank'' B, ← Basis.mk_eq_spanRank B, ← Cardinal.lift_id #(Set.range B),
    Cardinal.mk_range_eq_of_injective B.injective, Cardinal.lift_id _]

Goal state after:
Module: Mathlib.RingTheory.IntegralClosure.Algebra.Basic

Goal state before:
pp: R : Type u_1
S : Type u_4
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
x y z : S
hx : f.IsIntegralElem x
hy : f.IsIntegralElem y
hz : z ∈ Subring.closure {x, y}
⊢ f.IsIntegralElem z

Tactic:
let : Algebra R S := f.toAlgebra

Goal state after:
R : Type u_1
S : Type u_4
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
x y z : S
hx : f.IsIntegralElem x
hy : f.IsIntegralElem y
hz : z ∈ Subring.closure {x, y}
this : Algebra R S := f.toAlgebra
⊢ f.IsIntegralElem z
Module: Mathlib.Algebra.Polynomial.Taylor

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
f : R[X]
r : R
⊢ (((taylor r) f).sum fun i a ↦ C a * (X - C r) ^ i) = f

Tactic:
← comp_eq_sum_left,

Goal state after:
R : Type u_1
inst✝ : CommRing R
f : R[X]
r : R
⊢ ((taylor r) f).comp (X - C r) = f
Module: Mathlib.RingTheory.Polynomial.IntegralNormalization

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
i : ℕ
hi : p.degree ≠ ↑i
⊢ p.integralNormalization.coeff i = p.coeff i * p.leadingCoeff ^ (p.natDegree - 1 - i)

Tactic:
rw [integralNormalization_coeff, if_neg hi]

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

Goal state before:
pp: case succ
R : Type u_1
inst✝ : CommSemiring R
p : R[X]
r : R
n : ℕ
IH : p.leadingCoeff ^ n ≠ 0 → (p ^ n).scaleRoots r = p.scaleRoots r ^ n
hp : p.leadingCoeff ^ (n + 1) ≠ 0
⊢ (p ^ (n + 1)).scaleRoots r = p.scaleRoots r ^ (n + 1)

Tactic:
rw [pow_succ, mul_scaleRoots', IH, pow_succ]

Goal state after:
case succ
R : Type u_1
inst✝ : CommSemiring R
p : R[X]
r : R
n : ℕ
IH : p.leadingCoeff ^ n ≠ 0 → (p ^ n).scaleRoots r = p.scaleRoots r ^ n
hp : p.leadingCoeff ^ (n + 1) ≠ 0
⊢ p.leadingCoeff ^ n ≠ 0

case succ.h
R : Type u_1
inst✝ : CommSemiring R
p : R[X]
r : R
n : ℕ
IH : p.leadingCoeff ^ n ≠ 0 → (p ^ n).scaleRoots r = p.scaleRoots r ^ n
hp : p.leadingCoeff ^ (n + 1) ≠ 0
⊢ (p ^ n).leadingCoeff * p.leadingCoeff ≠ 0