mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Monad.Limits

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
T : Monad C
J : Type u
inst✝ : Category.{v, u} J
D : J ⥤ T.Algebra
c : Cone (D ⋙ T.forget)
t : IsLimit c
j : J
⊢ (T.η.app c.pt ≫ t.lift (newCone D c)) ≫ c.π.app j = 𝟙 c.pt ≫ c.π.app j

Tactic:
by
      rw [Category.assoc, t.fac, newCone_π_app, ← T.η.naturality_assoc, Functor.id_map,
        (D.obj j).unit]
      simp

Goal state after:
Module: Mathlib.RingTheory.Ideal.MinimalPrime.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : CommSemiring R
I J : Ideal R
inst✝ : J.IsPrime
e : I ≤ J
S : Set (Ideal R)ᵒᵈ := {p | IsPrime p ∧ I ≤ OrderDual.ofDual p}
h : ∃ m, OrderDual.toDual J ≤ m ∧ Maximal (fun x ↦ x ∈ S) m
⊢ ∃ p ∈ I.minimalPrimes, p ≤ J

Tactic:
by
    obtain ⟨p, hJp, hp⟩ := h
    exact ⟨p, ⟨hp.prop, fun q hq hle ↦ hp.le_of_ge hq hle⟩, hJp⟩

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

Goal state before:
pp: case mp.refine_1
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
J : Ideal S
h : J.IsPrime
hJ : Ideal.under R J = ⊤
⊢ J = ⊤

Tactic:
eq_top_iff,

Goal state after:
case mp.refine_1
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
J : Ideal S
h : J.IsPrime
hJ : Ideal.under R J = ⊤
⊢ ⊤ ≤ J
Module: Mathlib.RingTheory.Localization.Ideal

Goal state before:
pp: case mpr.refine_1
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
J : Ideal S
h : (Ideal.under R J).IsPrime ∧ Disjoint ↑M ↑(Ideal.under R J)
hJ : J = ⊤
⊢ ⊤ ≤ Ideal.under R J

Tactic:
eq_top_iff,

Goal state after:
case mpr.refine_1
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
J : Ideal S
h : (Ideal.under R J).IsPrime ∧ Disjoint ↑M ↑(Ideal.under R J)
hJ : ⊤ ≤ J
⊢ ⊤ ≤ Ideal.under R J
Module: Mathlib.RingTheory.Localization.Algebra

Goal state before:
pp: R : Type u_1
S : Type u_2
P : Type u_3
Q : Type u_4
inst✝⁷ : CommSemiring R
inst✝⁶ : CommSemiring S
inst✝⁵ : CommSemiring P
inst✝⁴ : CommSemiring Q
M : Submonoid R
T : Submonoid P
inst✝³ : Algebra R S
inst✝² : Algebra P Q
inst✝¹ : IsLocalization M S
inst✝ : IsLocalization T Q
g : R →+* P
hy : M ≤ Submonoid.comap g T
x : ↥(ker g)
⊢ (algebraMap R S) ↑x ∈ ker (IsLocalization.map Q g hy)

Tactic:
by simp [RingHom.mem_ker, RingHom.mem_ker.mp x.property]

Goal state after:
Module: Mathlib.RingTheory.Localization.LocalizationLocalization

Goal state before:
pp: case refine_2
R : Type u_1
inst✝⁸ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
N : Submonoid S
T : Type u_3
inst✝⁵ : CommSemiring T
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
inst✝¹ : IsLocalization M S
inst✝ : IsLocalization N T
x : T
y : S
s : ↥N
eq₁ : x * (algebraMap S T) ↑s = (algebraMap S T) y
z : R
t : ↥M
eq₂ : y * (algebraMap R S) ↑t = (algebraMap R S) z
z' : R
t' : ↥M
eq₃ : ↑s * (algebraMap R S) ↑t' = (algebraMap R S) z'
⊢ x * (algebraMap R T) ↑(z * ↑t', ⟨z' * ↑t, ⋯⟩).2 = (algebraMap R T) (z * ↑t', ⟨z' * ↑t, ⋯⟩).1

Tactic:
· simp only [map_mul, IsScalarTower.algebraMap_apply R S T, ← eq₃, ← eq₂, ← eq₁]
    ring

Goal state after:
Module: Mathlib.RingTheory.Localization.LocalizationLocalization

Goal state before:
pp: case e_S
R : Type u_1
inst✝⁸ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
N : Submonoid S
T : Type u_3
inst✝⁵ : CommSemiring T
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
inst✝¹ : IsLocalization M S
inst✝ : IsLocalization N T
H : ∀ (x : S), IsUnit x → x ∈ N
⊢ N = N ⊔ Submonoid.map (algebraMap R S) M

Tactic:
symm

Goal state after:
case e_S
R : Type u_1
inst✝⁸ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
N : Submonoid S
T : Type u_3
inst✝⁵ : CommSemiring T
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
inst✝¹ : IsLocalization M S
inst✝ : IsLocalization N T
H : ∀ (x : S), IsUnit x → x ∈ N
⊢ N ⊔ Submonoid.map (algebraMap R S) M = N
Module: Mathlib.RingTheory.Localization.LocalizationLocalization

Goal state before:
pp: R : Type u_1
inst✝⁸ : CommSemiring R
S : Type u_2
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
T : Type u_3
inst✝⁵ : CommSemiring T
inst✝⁴ : Algebra R T
M N : Submonoid R
h : M ≤ N
inst✝³ : IsLocalization M S
inst✝² : IsLocalization N T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
x₁ x₂ : S
y₁ : R
s₁ : ↥M
e₁ : x₁ * (algebraMap R S) ↑s₁ = (algebraMap R S) y₁
y₂ : R
s₂ : ↥M
e₂ : x₂ * (algebraMap R S) ↑s₂ = (algebraMap R S) y₂
a : ↥N
e : ↑a * (y₁ * ↑s₂) = ↑a * (y₂ * ↑s₁)
⊢ ↑1 * (↑a * (y₁ * ↑s₂)) = ↑1 * (↑a * (y₂ * ↑s₁))

Tactic:
by convert! e using 1 <;> simp

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

Goal state before:
pp: case hr
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
a : ↥m ⊗[R] N
b : M ⊗[R] ↥n
f : ↥m ⊗[R] N →ₗ[R] (M ⧸ m) ⊗[R] (N ⧸ n) := map m.mkQ n.mkQ ∘ₗ map m.subtype LinearMap.id
g : M ⊗[R] ↥n →ₗ[R] (M ⧸ m) ⊗[R] (N ⧸ n) := map m.mkQ n.mkQ ∘ₗ map LinearMap.id n.subtype
x : M
y : ↥n
⊢ ((AlgebraTensorModule.curry (f.coprod g ∘ₗ LinearMap.inr R (↥m ⊗[R] N) (M ⊗[R] ↥n))) x) y =
    ((AlgebraTensorModule.curry (0 ∘ₗ LinearMap.inr R (↥m ⊗[R] N) (M ⊗[R] ↥n))) x) y

Tactic:
· simp [g, Submodule.Quotient.mk_eq_zero _ |>.2 y.2]

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 : Type u_3
inst✝³ : CommSemiring P
A : Type u_4
inst✝² : CommRing A
inst✝¹ : IsDomain A
I : Ideal R
hI : I.IsPrime
inst✝ : IsLocalization.AtPrime S I
⊢ {p | p.IsPrime ∧ Disjoint ↑I.primeCompl ↑p} = {p | p.IsPrime ∧ p ≤ I}

Tactic:
ext; simp [Ideal.primeCompl, ← le_compl_iff_disjoint_left]

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommSemiring R
P : Type u_3
inst✝ : CommSemiring P
I : Ideal R
hI : I.IsPrime
J : Ideal P
hJ : J.IsPrime
f : R →+* P
hIJ : I = Ideal.comap f J
r : R
s : ↥I.primeCompl
hx : IsUnit (mk' (Localization.AtPrime J) (f r) ⟨f ↑s, ⋯⟩)
⊢ IsUnit (mk' (Localization.AtPrime I) r s)

Tactic:
AtPrime.isUnit_mk'_iff

Goal state after:
R : Type u_1
inst✝¹ : CommSemiring R
P : Type u_3
inst✝ : CommSemiring P
I : Ideal R
hI : I.IsPrime
J : Ideal P
hJ : J.IsPrime
f : R →+* P
hIJ : I = Ideal.comap f J
r : R
s : ↥I.primeCompl
hx : f r ∈ J.primeCompl
⊢ r ∈ I.primeCompl
Module: Mathlib.RingTheory.Localization.Submodule

Goal state before:
pp: case mp.refine_4
R : Type u_1
inst✝⁷ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝⁶ : CommSemiring S
inst✝⁵ : Algebra R S
inst✝⁴ : IsLocalization M S
N : Type u_3
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : Module S N
inst✝ : IsScalarTower R S N
x : N
a : Set N
h : x ∈ Submodule.span S a
y : N
hy : y ∈ Submodule.span R a
z : ↥M
hx✝ : mk' S 1 z • y ∈ Submodule.span S a
y' : R
z' : ↥M
⊢ mk' S (y' * 1) (z' * z) • y = (mk' S 1 (z' * z) * (algebraMap R S) y') • y

Tactic:
mul_comm (mk' S _ _),

Goal state after:
case mp.refine_4
R : Type u_1
inst✝⁷ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝⁶ : CommSemiring S
inst✝⁵ : Algebra R S
inst✝⁴ : IsLocalization M S
N : Type u_3
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : Module S N
inst✝ : IsScalarTower R S N
x : N
a : Set N
h : x ∈ Submodule.span S a
y : N
hy : y ∈ Submodule.span R a
z : ↥M
hx✝ : mk' S 1 z • y ∈ Submodule.span S a
y' : R
z' : ↥M
⊢ mk' S (y' * 1) (z' * z) • y = ((algebraMap R S) y' * mk' S 1 (z' * z)) • y
Module: Mathlib.RingTheory.OreLocalization.OreSet

Goal state before:
pp: case mpr
R : Type u_1
inst✝ : Monoid R
S : Submonoid R
H : ∀ (r₁ r₂ : R) (s : ↥S), r₁ * ↑s = r₂ * ↑s → ∃ s', ↑s' * r₁ = ↑s' * r₂
r' : R → ↥S → R
s' : R → ↥S → ↥S
h : ∀ (r : R) (s : ↥S), ↑(s' r s) * r = r' r s * ↑s
⊢ Nonempty (OreSet S)

Tactic:
exact ⟨H, r', s', h⟩

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

Goal state before:
pp: case mul_T
R : Type u_1
inst✝ : Semiring R
Q : R[T;T⁻¹] → Prop
Qf : ∀ (f : R[X]), Q (toLaurent f)
QT : ∀ (f : R[T;T⁻¹]), Q (f * T 1) → Q f
f : R[X]
n : ℕ
⊢ Q (toLaurent f * T (-↑n))

Tactic:
| _ f n
   => 

Goal state after:
case mul_T
R : Type u_1
inst✝ : Semiring R
Q : R[T;T⁻¹] → Prop
Qf : ∀ (f : R[X]), Q (toLaurent f)
QT : ∀ (f : R[T;T⁻¹]), Q (f * T 1) → Q f
f : R[X]
n : ℕ
⊢ Q (toLaurent f * T (-↑n))
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:
nth_rw 2 [← A.transpose_transpose]

Goal state after:
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
Module: Mathlib.LinearAlgebra.Matrix.Transvection

Goal state before:
pp: n : Type u_1
R : Type u₂
inst✝² : DecidableEq n
inst✝¹ : CommRing R
inst✝ : Fintype n
M : Matrix n n R
hM : ∀ (t : TransvectionStruct n R), Commute t.toMatrix M
⊢ M ∈ Set.range ⇑(scalar n)

Tactic:
by
  refine mem_range_scalar_of_commute_single ?_
  intro i j hij
  simpa [transvection, mul_add, add_mul] using! (hM ⟨i, j, hij, 1⟩).eq

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

Goal state before:
pp: m : Type u_2
n : Type u_3
p : Type u_4
R : Type u_6
inst✝³ : Fintype m
inst✝² : Fintype n
inst✝¹ : Fintype p
inst✝ : NonUnitalCommSemiring R
A : Matrix m n R
B : Matrix n p R
C : Matrix p m R
⊢ (A * (B * C)).trace = (C * (A * B)).trace

Tactic:
by
  rw [← Matrix.mul_assoc, trace_mul_comm]

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)
⊢ 1 + U * C * V * ⅟A - (U * ⅟(⅟C + V * ⅟A * U) * V * ⅟A + U * C * V * ⅟A * U * ⅟(⅟C + V * ⅟A * U) * V * ⅟A) =
    1 + U * C * V * ⅟A - (U + U * C * V * ⅟A * U) * ⅟(⅟C + V * ⅟A * U) * V * ⅟A

Tactic:
rw [sub_right_inj, Matrix.add_mul, Matrix.add_mul, Matrix.add_mul]

Goal state after:
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) 𝕜
hM : M (inr ()) (inr ()) ≠ 0
i : Fin r
k n : ℕ
hn : n < r
IH : ((List.drop (n + 1) (listTransvecCol M)).prod * M) (inl i) (inr ()) = if n + 1 ≤ ↑i then 0 else M (inl i) (inr ())
hn' : n < (listTransvecCol M).length
n' : Fin r := ⟨n, hn⟩
A : (listTransvecCol M)[n] = transvection (inl n') (inr ()) (-M (inl n') (inr ()) / M (inr ()) (inr ()))
h : ¬n' = i
hni : n ≠ ↑i
⊢ (if n + 1 ≤ ↑i then 0 else M (inl i) (inr ())) = if n ≤ ↑i then 0 else M (inl i) (inr ())

Tactic:
rcases le_or_gt (n + 1) i with (hi | hi)

Goal state after:
case neg.inl
𝕜 : Type u_3
inst✝ : Field 𝕜
r : ℕ
M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
hM : M (inr ()) (inr ()) ≠ 0
i : Fin r
k n : ℕ
hn : n < r
IH : ((List.drop (n + 1) (listTransvecCol M)).prod * M) (inl i) (inr ()) = if n + 1 ≤ ↑i then 0 else M (inl i) (inr ())
hn' : n < (listTransvecCol M).length
n' : Fin r := ⟨n, hn⟩
A : (listTransvecCol M)[n] = transvection (inl n') (inr ()) (-M (inl n') (inr ()) / M (inr ()) (inr ()))
h : ¬n' = i
hni : n ≠ ↑i
hi : n + 1 ≤ ↑i
⊢ (if n + 1 ≤ ↑i then 0 else M (inl i) (inr ())) = if n ≤ ↑i then 0 else M (inl i) (inr ())

case neg.inr
𝕜 : Type u_3
inst✝ : Field 𝕜
r : ℕ
M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
hM : M (inr ()) (inr ()) ≠ 0
i : Fin r
k n : ℕ
hn : n < r
IH : ((List.drop (n + 1) (listTransvecCol M)).prod * M) (inl i) (inr ()) = if n + 1 ≤ ↑i then 0 else M (inl i) (inr ())
hn' : n < (listTransvecCol M).length
n' : Fin r := ⟨n, hn⟩
A : (listTransvecCol M)[n] = transvection (inl n') (inr ()) (-M (inl n') (inr ()) / M (inr ()) (inr ()))
h : ¬n' = i
hni : n ≠ ↑i
hi : ↑i < n + 1
⊢ (if n + 1 ≤ ↑i then 0 else M (inl i) (inr ())) = if n ≤ ↑i then 0 else M (inl i) (inr ())
Module: Mathlib.LinearAlgebra.Matrix.Transvection

Goal state before:
pp: case neg.inr.hnc
𝕜 : Type u_3
inst✝ : Field 𝕜
r : ℕ
M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
hM : M (inr ()) (inr ()) ≠ 0
i : Fin r
k n : ℕ
hn : n < r
IH : ((List.drop (n + 1) (listTransvecCol M)).prod * M) (inl i) (inr ()) = if n + 1 ≤ ↑i then 0 else M (inl i) (inr ())
hn' : n < (listTransvecCol M).length
n' : Fin r := ⟨n, hn⟩
A : (listTransvecCol M)[n] = transvection (inl n') (inr ()) (-M (inl n') (inr ()) / M (inr ()) (inr ()))
h : ¬n' = i
hni : n ≠ ↑i
hi : ↑i < n + 1
⊢ ¬n + 1 ≤ ↑i

Tactic:
· simpa only [not_le] using hi

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

Goal state before:
pp: m : Type u
inst✝² : DecidableEq m
K : Type u_3
inst✝¹ : Field K
inst✝ : Fintype m
A : Matrix m m K
⊢ Function.Injective A.mulVec ↔ Function.Injective fun v ↦ v ᵥ* Aᵀ

Tactic:
simp_rw [vecMul_transpose]

Goal state after:
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) 𝕜
hM : M (inr ()) (inr ()) ≠ 0
i : Fin r
n : ℕ
IH : n ≤ r → (M * (List.take n (listTransvecRow M)).prod) (inr ()) (inl i) = if n ≤ ↑i then M (inr ()) (inl i) else 0
hk : n + 1 ≤ r
hnr : n < r
n' : Fin r := ⟨n, hnr⟩
A : (listTransvecRow M)[n]? = some (transvection (inr ()) (inl n') (-M (inr ()) (inl n') / M (inr ()) (inr ())))
h : ¬n' = i
hni : n ≠ ↑i
⊢ (if n ≤ ↑i then M (inr ()) (inl i) else 0) = if n + 1 ≤ ↑i then M (inr ()) (inl i) else 0

Tactic:
rcases le_or_gt (n + 1) i with (hi | hi)

Goal state after:
case neg.inl
𝕜 : Type u_3
inst✝ : Field 𝕜
r : ℕ
M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
hM : M (inr ()) (inr ()) ≠ 0
i : Fin r
n : ℕ
IH : n ≤ r → (M * (List.take n (listTransvecRow M)).prod) (inr ()) (inl i) = if n ≤ ↑i then M (inr ()) (inl i) else 0
hk : n + 1 ≤ r
hnr : n < r
n' : Fin r := ⟨n, hnr⟩
A : (listTransvecRow M)[n]? = some (transvection (inr ()) (inl n') (-M (inr ()) (inl n') / M (inr ()) (inr ())))
h : ¬n' = i
hni : n ≠ ↑i
hi : n + 1 ≤ ↑i
⊢ (if n ≤ ↑i then M (inr ()) (inl i) else 0) = if n + 1 ≤ ↑i then M (inr ()) (inl i) else 0

case neg.inr
𝕜 : Type u_3
inst✝ : Field 𝕜
r : ℕ
M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
hM : M (inr ()) (inr ()) ≠ 0
i : Fin r
n : ℕ
IH : n ≤ r → (M * (List.take n (listTransvecRow M)).prod) (inr ()) (inl i) = if n ≤ ↑i then M (inr ()) (inl i) else 0
hk : n + 1 ≤ r
hnr : n < r
n' : Fin r := ⟨n, hnr⟩
A : (listTransvecRow M)[n]? = some (transvection (inr ()) (inl n') (-M (inr ()) (inl n') / M (inr ()) (inr ())))
h : ¬n' = i
hni : n ≠ ↑i
hi : ↑i < n + 1
⊢ (if n ≤ ↑i then M (inr ()) (inl i) else 0) = if n + 1 ≤ ↑i then M (inr ()) (inl i) else 0
Module: Mathlib.RingTheory.MatrixPolynomialAlgebra

Goal state before:
pp: 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 m).coeff k i j = (m i j).coeff k

Tactic:
refine Matrix.induction_on' m ?_ ?_ ?_

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

case refine_2
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
⊢ ∀ (p q : Matrix n n R[X]),
    (matPolyEquiv p).coeff k i j = (p i j).coeff k →
      (matPolyEquiv q).coeff k i j = (q i j).coeff k → (matPolyEquiv (p + q)).coeff k i j = ((p + q) i j).coeff k

case refine_3
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
⊢ ∀ (i_1 j_1 : n) (x : R[X]), (matPolyEquiv (single i_1 j_1 x)).coeff k i j = (single i_1 j_1 x i j).coeff k
Module: Mathlib.Algebra.Polynomial.Identities

Goal state before:
pp: R : Type u
S : Type v
T : Type w
ι : Type x
k✝ : Type y
A : Type z
a b : R
m n : ℕ
inst✝ : CommRing R
x y : R
k : ℕ
z : R
hz : x ^ (k + 1) - y ^ (k + 1) = z * (x - y)
⊢ x ^ (k + 2) - y ^ (k + 2) = (z * x + y ^ (k + 1)) * (x - y)

Tactic:
linear_combination (norm := ring) x * hz

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
⊢ (∑ x ∈ univ.erase (Equiv.refl n), ↑↑(Equiv.Perm.sign x) * ∏ i, M.charmatrix (x i) i +
          ↑↑(Equiv.Perm.sign (Equiv.refl n)) * ∏ i, M.charmatrix ((Equiv.refl n) i) i -
        ∏ i, (X - C (M i i))).degree <
    ↑(Fintype.card n - 1)

Tactic:
simp only [charmatrix_apply_eq, one_mul, Equiv.Perm.sign_refl, id, Int.cast_one,
    Units.val_one, add_sub_cancel_right, Equiv.coe_refl]

Goal state after:
R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
⊢ (∑ x ∈ univ.erase (Equiv.refl n), ↑↑(Equiv.Perm.sign x) * ∏ i, M.charmatrix (x i) i).degree < ↑(Fintype.card n - 1)
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
hp : p.FG
⊢ p.spanRank < ℵ₀

Tactic:
exact spanRank_finite_iff_fg.mpr hp

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

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
T : Type v
inst✝ : Semiring T
f : R ≃+* T
I : Ideal R
⊢ Submodule.spanFinrank (map f I) = Submodule.spanFinrank I

Tactic:
rw [Submodule.spanFinrank, Submodule.spanFinrank, ← Cardinal.toNat_lift.{u, v},
    ← Cardinal.toNat_lift.{v, u}, I.lift_spanRank_map_eq_of_ringEquiv f]

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
a✝ : Nontrivial R
t : R[T;T⁻¹] := T 1
t_inv : R[T;T⁻¹] := T (-1)
p : R[T;T⁻¹] := ((scalar n) t - M.map ⇑LaurentPolynomial.C).det
q : R[T;T⁻¹] := (1 - (scalar n) t * M.map ⇑LaurentPolynomial.C).det
ht : t_inv * t = 1
hp : toLaurentAlg M.charpoly = p
hq : toLaurentAlg M.charpolyRev = q
this : t_inv ^ Fintype.card n * p = invert q
⊢ p * invert (T ↑(Fintype.card n)) = invert q

Tactic:
← mul_one (Fintype.card n : ℤ),

Goal state after:
R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
a✝ : Nontrivial R
t : R[T;T⁻¹] := T 1
t_inv : R[T;T⁻¹] := T (-1)
p : R[T;T⁻¹] := ((scalar n) t - M.map ⇑LaurentPolynomial.C).det
q : R[T;T⁻¹] := (1 - (scalar n) t * M.map ⇑LaurentPolynomial.C).det
ht : t_inv * t = 1
hp : toLaurentAlg M.charpoly = p
hq : toLaurentAlg M.charpolyRev = q
this : t_inv ^ Fintype.card n * p = invert q
⊢ p * invert (T (↑(Fintype.card n) * 1)) = invert q
Module: Mathlib.RingTheory.IntegralClosure.Algebra.Basic

Goal state before:
pp: G : Type u_1
R : Type u_2
K : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing K
inst✝³ : Algebra R K
inst✝² : Group G
inst✝¹ : MulSemiringAction G K
inst✝ : SMulCommClass G R K
g : G
⊢ g • 0 = 0

Tactic:
by ext; exact smul_zero g

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

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
A : Type u_1
inst✝ : Semiring A
f : R →+* A
p : R[X]
H : f p.leadingCoeff ≠ 0
⊢ (map f p).integralNormalization = map f p.integralNormalization

Tactic:
ext i
  simp [integralNormalization_coeff, degree_map_eq_of_leadingCoeff_ne_zero _ H, apply_ite f,
    leadingCoeff_map_of_leadingCoeff_ne_zero _ H, natDegree_map_eq_iff.mpr (.inl H)]

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

Goal state before:
pp: case refine_1
R : Type u_1
inst✝ : CommSemiring R
S : Submonoid R[X] := MonoidHom.mrange C
hS : ↑S = {x | ∃ a, C a = x}
a : R
mg : Multiset R[X]
hg : mg.prod ∈ Submonoid.closure {x | ∃ a, X + C a = x}
j : R[X] → R
hj : ∀ y ∈ mg, X + C (j y) = y
hmg : mg = Multiset.map (fun x ↦ X + C x) (Multiset.map j mg)
⊢ ∃ m,
    C a * (Multiset.map (fun x ↦ X + C x) (Multiset.map j mg)).prod =
      C (C a).leadingCoeff * (Multiset.map (fun x ↦ X + C x) m).prod

pp: case refine_1
R : Type u_1
inst✝ : CommSemiring R
S : Submonoid R[X] := MonoidHom.mrange C
hS : ↑S = {x | ∃ a, C a = x}
a : R
mg : Multiset R[X]
hg : mg.prod ∈ Submonoid.closure {x | ∃ a, X + C a = x}
j : R[X] → R
hj : ∀ y ∈ mg, X + C (j y) = y
hmg : mg = Multiset.map (fun x ↦ X + C x) (Multiset.map j mg)
⊢ (Multiset.map (fun x ↦ X + C x) (Multiset.map j mg)).prod.Monic

Tactic:
leadingCoeff_C

Goal state after:
case refine_1
R : Type u_1
inst✝ : CommSemiring R
S : Submonoid R[X] := MonoidHom.mrange C
hS : ↑S = {x | ∃ a, C a = x}
a : R
mg : Multiset R[X]
hg : mg.prod ∈ Submonoid.closure {x | ∃ a, X + C a = x}
j : R[X] → R
hj : ∀ y ∈ mg, X + C (j y) = y
hmg : mg = Multiset.map (fun x ↦ X + C x) (Multiset.map j mg)
⊢ ∃ m, C a * (Multiset.map (fun x ↦ X + C x) (Multiset.map j mg)).prod = C a * (Multiset.map (fun x ↦ X + C x) m).prod

case refine_1
R : Type u_1
inst✝ : CommSemiring R
S : Submonoid R[X] := MonoidHom.mrange C
hS : ↑S = {x | ∃ a, C a = x}
a : R
mg : Multiset R[X]
hg : mg.prod ∈ Submonoid.closure {x | ∃ a, X + C a = x}
j : R[X] → R
hj : ∀ y ∈ mg, X + C (j y) = y
hmg : mg = Multiset.map (fun x ↦ X + C x) (Multiset.map j mg)
⊢ (Multiset.map (fun x ↦ X + C x) (Multiset.map j mg)).prod.Monic
Module: Mathlib.Algebra.Polynomial.Splits

Goal state before:
pp: case inr
R : Type u_1
inst✝ : CommSemiring R
f : R[X]
hf : f.Splits
h : Irreducible f
a✝ : Nontrivial R
a : R
m : Multiset R
hm : f = C f.leadingCoeff * ((X + C a) ::ₘ Multiset.map (fun x ↦ X + C x) m).prod
ha : a ∈ a ::ₘ m
⊢ f.natDegree ≤ 1

Tactic:
Multiset.prod_cons

Goal state after:
case inr
R : Type u_1
inst✝ : CommSemiring R
f : R[X]
hf : f.Splits
h : Irreducible f
a✝ : Nontrivial R
a : R
m : Multiset R
hm : f = C f.leadingCoeff * ((X + C a) * (Multiset.map (fun x ↦ X + C x) m).prod)
ha : a ∈ a ::ₘ m
⊢ f.natDegree ≤ 1
Module: Mathlib.Algebra.Polynomial.Splits

Goal state before:
pp: case inr
R : Type u_1
inst✝ : CommSemiring R
f g : R[X]
hf : f.Splits
hg✝ : g.natDegree ≤ 1
h : Invertible g.leadingCoeff
hg : g.natDegree = 1
m : Multiset R
hm : f = C f.leadingCoeff * (Multiset.map (fun x ↦ X + C x) m).prod
⊢ ∀ f ∈ Multiset.map (fun p ↦ p.comp g) (Multiset.map (fun x ↦ X + C x) m), f.Splits

Tactic:
simp only [Multiset.mem_map]

Goal state after:
case inr
R : Type u_1
inst✝ : CommSemiring R
f g : R[X]
hf : f.Splits
hg✝ : g.natDegree ≤ 1
h : Invertible g.leadingCoeff
hg : g.natDegree = 1
m : Multiset R
hm : f = C f.leadingCoeff * (Multiset.map (fun x ↦ X + C x) m).prod
⊢ ∀ (f : R[X]), (∃ a, (∃ a_1 ∈ m, X + C a_1 = a) ∧ a.comp g = f) → f.Splits
Module: Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
S T : Subalgebra R A
⊢ Algebra.IsIntegral R ↥(S ⊔ T) ↔ Algebra.IsIntegral R ↥S ∧ Algebra.IsIntegral R ↥T

Tactic:
simp_rw [← le_integralClosure_iff_isIntegral, sup_le_iff]

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
n : ℕ
ih : ∀ {f g : R[X]}, f ≠ 0 → g ≠ 0 → ∀ (p : R[X]), f * g = p → p.Splits → p.natDegree = n → f.Splits ∧ g.Splits
g : R[X]
hg₀ : g ≠ 0
p : R[X]
h : p.Splits
hn : p.natDegree = n + 1
a : R
ha : eval a p = 0
f : R[X]
hf₀ : (X - C a) * f ≠ 0
hp : (X - C a) * f * g = p
this : X - C a ∣ (X - C a) * f ∨ X - C a ∣ g
⊢ ((X - C a) * f).Splits ∧ g.Splits

Tactic:
rw [mul_assoc] at hp

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
n : ℕ
ih : ∀ {f g : R[X]}, f ≠ 0 → g ≠ 0 → ∀ (p : R[X]), f * g = p → p.Splits → p.natDegree = n → f.Splits ∧ g.Splits
g : R[X]
hg₀ : g ≠ 0
p : R[X]
h : p.Splits
hn : p.natDegree = n + 1
a : R
ha : eval a p = 0
f : R[X]
hf₀ : (X - C a) * f ≠ 0
hp : (X - C a) * (f * g) = p
this : X - C a ∣ (X - C a) * f ∨ X - C a ∣ g
⊢ ((X - C a) * f).Splits ∧ g.Splits