mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.Dimension.Localization

Goal state before:
pp: R : Type uR
S : Type uS
N : Type uN
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
inst✝³ : Algebra R S
inst✝² : Module S N
inst✝¹ : IsScalarTower R S N
p : Submonoid R
inst✝ : IsLocalization p S
hp : p ≤ R⁰
⊢ Module.rank S N = Module.rank R N

Tactic:
cases subsingleton_or_nontrivial R

Goal state after:
case inl
R : Type uR
S : Type uS
N : Type uN
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
inst✝³ : Algebra R S
inst✝² : Module S N
inst✝¹ : IsScalarTower R S N
p : Submonoid R
inst✝ : IsLocalization p S
hp : p ≤ R⁰
h✝ : Subsingleton R
⊢ Module.rank S N = Module.rank R N

case inr
R : Type uR
S : Type uS
N : Type uN
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
inst✝³ : Algebra R S
inst✝² : Module S N
inst✝¹ : IsScalarTower R S N
p : Submonoid R
inst✝ : IsLocalization p S
hp : p ≤ R⁰
h✝ : Nontrivial R
⊢ Module.rank S N = Module.rank R N
Module: Mathlib.Algebra.Polynomial.Laurent

Goal state before:
pp: R : Type u_1
S✝ : Type u_2
inst✝¹ : CommSemiring R
S : Type u_3
inst✝ : CommSemiring S
f : R →+* S
x : Sˣ
x✝ : ↥(Submonoid.powers X)
n : ℕ
⊢ IsUnit (T ↑n)

Tactic:
exact isUnit_T ↑n

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

Goal state before:
pp: case mk
n : Type u_1
p : Type u_2
R : Type u₂
inst✝² : DecidableEq n
inst✝¹ : DecidableEq p
inst✝ : CommRing R
i✝ j✝ : n
hij✝ : i✝ ≠ j✝
c✝ : R
a b : n ⊕ p
⊢ (sumInl p { i := i✝, j := j✝, hij := hij✝, c := c✝ }).toMatrix a b =
    fromBlocks { i := i✝, j := j✝, hij := hij✝, c := c✝ }.toMatrix 0 0 1 a b

Tactic:
rcases a with a | a

Goal state after:
case mk.inl
n : Type u_1
p : Type u_2
R : Type u₂
inst✝² : DecidableEq n
inst✝¹ : DecidableEq p
inst✝ : CommRing R
i✝ j✝ : n
hij✝ : i✝ ≠ j✝
c✝ : R
b : n ⊕ p
a : n
⊢ (sumInl p { i := i✝, j := j✝, hij := hij✝, c := c✝ }).toMatrix (inl a) b =
    fromBlocks { i := i✝, j := j✝, hij := hij✝, c := c✝ }.toMatrix 0 0 1 (inl a) b

case mk.inr
n : Type u_1
p : Type u_2
R : Type u₂
inst✝² : DecidableEq n
inst✝¹ : DecidableEq p
inst✝ : CommRing R
i✝ j✝ : n
hij✝ : i✝ ≠ j✝
c✝ : R
b : n ⊕ p
a : p
⊢ (sumInl p { i := i✝, j := j✝, hij := hij✝, c := c✝ }).toMatrix (inr a) b =
    fromBlocks { i := i✝, j := j✝, hij := hij✝, c := c✝ }.toMatrix 0 0 1 (inr a) b
Module: Mathlib.LinearAlgebra.Dimension.Localization

Goal state before:
pp: R : Type uR
M : Type uM
inst✝¹⁰ : CommRing R
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module R M
T : Type uT
inst✝⁷ : CommRing T
inst✝⁶ : NoZeroDivisors T
inst✝⁵ : Algebra R T
inst✝⁴ : FaithfulSMul R T
P : Type uP
inst✝³ : AddCommGroup P
inst✝² : Module R P
inst✝¹ : Module T P
inst✝ : IsScalarTower R T P
g : M →ₗ[R] P
bc : IsBaseChange T g
inj : Function.Injective ⇑(algebraMap R T)
this : NoZeroDivisors R
⊢ Cardinal.lift.{uM, uP} (Module.rank T P) = Cardinal.lift.{uP, uM} (Module.rank R M)

Tactic:
cases subsingleton_or_nontrivial R

Goal state after:
case inl
R : Type uR
M : Type uM
inst✝¹⁰ : CommRing R
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module R M
T : Type uT
inst✝⁷ : CommRing T
inst✝⁶ : NoZeroDivisors T
inst✝⁵ : Algebra R T
inst✝⁴ : FaithfulSMul R T
P : Type uP
inst✝³ : AddCommGroup P
inst✝² : Module R P
inst✝¹ : Module T P
inst✝ : IsScalarTower R T P
g : M →ₗ[R] P
bc : IsBaseChange T g
inj : Function.Injective ⇑(algebraMap R T)
this : NoZeroDivisors R
h✝ : Subsingleton R
⊢ Cardinal.lift.{uM, uP} (Module.rank T P) = Cardinal.lift.{uP, uM} (Module.rank R M)

case inr
R : Type uR
M : Type uM
inst✝¹⁰ : CommRing R
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module R M
T : Type uT
inst✝⁷ : CommRing T
inst✝⁶ : NoZeroDivisors T
inst✝⁵ : Algebra R T
inst✝⁴ : FaithfulSMul R T
P : Type uP
inst✝³ : AddCommGroup P
inst✝² : Module R P
inst✝¹ : Module T P
inst✝ : IsScalarTower R T P
g : M →ₗ[R] P
bc : IsBaseChange T g
inj : Function.Injective ⇑(algebraMap R T)
this : NoZeroDivisors R
h✝ : Nontrivial R
⊢ Cardinal.lift.{uM, uP} (Module.rank T P) = Cardinal.lift.{uP, uM} (Module.rank R M)
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) = 1

Tactic:
calc
    (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 := by
      simp_rw [add_sub_assoc, add_mul, mul_sub, Matrix.mul_assoc]
    _ = (1 + U*C*V*⅟A) - (U*⅟(⅟C + V*⅟A*U)*V*⅟A + U*C*V*⅟A*U*⅟(⅟C + V*⅟A*U)*V*⅟A) := by
      rw [mul_invOf_self, Matrix.one_mul]
      abel
    _ = 1 + U*C*V*⅟A - (U + U*C*V*⅟A*U)*⅟(⅟C + V*⅟A*U)*V*⅟A := by
      rw [sub_right_inj, Matrix.add_mul, Matrix.add_mul, Matrix.add_mul]
    _ = 1 + U*C*V*⅟A - U*C*(⅟C + V*⅟A*U)*⅟(⅟C + V*⅟A*U)*V*⅟A := by
      congr
      simp only [Matrix.mul_add, Matrix.mul_invOf_cancel_right, ← Matrix.mul_assoc]
    _ = 1 := by
      rw [Matrix.mul_invOf_cancel_right]
      abel

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

Tactic:
by
  simp only [Matrix.mul_sub, Matrix.add_mul, mul_invOf_self']
  rw [add_sub_assoc, add_eq_left, sub_eq_zero]
  simp only [← Matrix.mul_assoc, mul_invOf_self', Matrix.one_mul]
  simp only [← Matrix.add_mul]
  congr
  rw [← Matrix.mul_right_eq_iff_eq_mul_invOf]
  simp only [Matrix.add_mul, Matrix.mul_add, Matrix.mul_assoc]

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 B C : Matrix n n α
h : A * B = 1
g : C * A = 1
⊢ B = C

Tactic:
rw [← inv_eq_right_inv h, ← inv_eq_left_inv g]

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

Goal state before:
pp: m : Type u
n : Type u'
α : Type v
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : CommRing α
inst✝¹ : Fintype m
inst✝ : DecidableEq m
A : Matrix n n α
U : Matrix n m α
C : Matrix m m α
V : Matrix m n α
hA : IsUnit A
hC : IsUnit C
hAC : IsUnit (C⁻¹ + V * A⁻¹ * U)
⊢ (A + U * C * V)⁻¹ = A⁻¹ - A⁻¹ * U * (C⁻¹ + V * A⁻¹ * U)⁻¹ * V * A⁻¹

Tactic:
obtain ⟨_⟩ := hA.nonempty_invertible

Goal state after:
m : Type u
n : Type u'
α : Type v
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : CommRing α
inst✝¹ : Fintype m
inst✝ : DecidableEq m
A : Matrix n n α
U : Matrix n m α
C : Matrix m m α
V : Matrix m n α
hA : IsUnit A
hC : IsUnit C
hAC : IsUnit (C⁻¹ + V * A⁻¹ * U)
val✝ : Invertible A
⊢ (A + U * C * V)⁻¹ = A⁻¹ - A⁻¹ * U * (C⁻¹ + V * A⁻¹ * U)⁻¹ * V * A⁻¹
Module: Mathlib.LinearAlgebra.Matrix.NonsingularInverse

Goal state before:
pp: m : Type u
n : Type u'
α : Type v
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : CommRing α
inst✝¹ : Fintype m
inst✝ : DecidableEq m
A : Matrix n n α
U : Matrix n m α
C : Matrix m m α
V : Matrix m n α
hA : IsUnit A
h : IsUnit (C + C * V * A⁻¹ * U * C)
⊢ (A + U * C * V)⁻¹ = A⁻¹ - A⁻¹ * U * C * (C + C * V * A⁻¹ * U * C)⁻¹ * C * V * A⁻¹

Tactic:
obtain ⟨_⟩ := hA.nonempty_invertible

Goal state after:
m : Type u
n : Type u'
α : Type v
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : CommRing α
inst✝¹ : Fintype m
inst✝ : DecidableEq m
A : Matrix n n α
U : Matrix n m α
C : Matrix m m α
V : Matrix m n α
hA : IsUnit A
h : IsUnit (C + C * V * A⁻¹ * U * C)
val✝ : Invertible A
⊢ (A + U * C * V)⁻¹ = A⁻¹ - A⁻¹ * U * C * (C + C * V * A⁻¹ * U * C)⁻¹ * C * V * A⁻¹
Module: Mathlib.LinearAlgebra.Matrix.NonsingularInverse

Goal state before:
pp: n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
⊢ [].prod⁻¹ = (List.map Inv.inv []).prod

Tactic:
List.map_nil,

Goal state after:
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
⊢ [].prod⁻¹ = [].prod
Module: Mathlib.LinearAlgebra.Matrix.Block

Goal state before:
pp: α : Type u_1
m : Type u_3
R : Type v
M : Matrix m m R
b : m → α
inst✝⁴ : CommRing R
inst✝³ : DecidableEq m
inst✝² : Fintype m
inst✝¹ : LinearOrder α
inst✝ : Invertible M
hM : M.BlockTriangular b
k : α
p : m → Prop := fun i ↦ b i < k
q : m → Prop := fun i ↦ ¬b i < k
h_sum : M⁻¹.toBlock q p * M.toBlock p p + M⁻¹.toBlock q q * M.toBlock q p = 0
h_zero : M.toBlock q p = 0
⊢ (M⁻¹.toBlock (fun i ↦ k ≤ b i) fun i ↦ b i < k) = 0

Tactic:
have h_mul_eq_zero : M⁻¹.toBlock q p * M.toBlock p p = 0 := by simpa [h_zero] using h_sum

Goal state after:
α : Type u_1
m : Type u_3
R : Type v
M : Matrix m m R
b : m → α
inst✝⁴ : CommRing R
inst✝³ : DecidableEq m
inst✝² : Fintype m
inst✝¹ : LinearOrder α
inst✝ : Invertible M
hM : M.BlockTriangular b
k : α
p : m → Prop := fun i ↦ b i < k
q : m → Prop := fun i ↦ ¬b i < k
h_sum : M⁻¹.toBlock q p * M.toBlock p p + M⁻¹.toBlock q q * M.toBlock q p = 0
h_zero : M.toBlock q p = 0
h_mul_eq_zero : M⁻¹.toBlock q p * M.toBlock p p = 0
⊢ (M⁻¹.toBlock (fun i ↦ k ≤ b i) fun i ↦ b i < k) = 0
Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Basic

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
m : Type u_3
inst✝¹ : DecidableEq m
inst✝ : Fintype m
M : Matrix m m R
t : R
⊢ eval t M.charpoly = ((scalar m) t - M).det

Tactic:
Matrix.charpoly,

Goal state after:
R : Type u_1
inst✝² : CommRing R
m : Type u_3
inst✝¹ : DecidableEq m
inst✝ : Fintype m
M : Matrix m m R
t : R
⊢ eval t M.charmatrix.det = ((scalar m) t - M).det
Module: Mathlib.LinearAlgebra.Matrix.Transvection

Goal state before:
pp: case nil
n : Type u_1
𝕜 : Type u_3
inst✝² : Field 𝕜
inst✝¹ : DecidableEq n
inst✝ : Fintype n
P : Matrix n n 𝕜 → Prop
M : Matrix n n 𝕜
hdiag : ∀ (D : n → 𝕜), (diagonal D).det = M.det → P (diagonal D)
htransvec : ∀ (t : TransvectionStruct n 𝕜), P t.toMatrix
hmul : ∀ (A B : Matrix n n 𝕜), P A → P B → P (A * B)
L L' : List (TransvectionStruct n 𝕜)
D : n → 𝕜
h : M = (List.map toMatrix L).prod * diagonal D * (List.map toMatrix L').prod
PD : P (diagonal D)
L₂ : List (TransvectionStruct n 𝕜)
E : Matrix n n 𝕜
PE : P E
⊢ P ((List.map toMatrix []).prod * E * (List.map toMatrix L₂).prod)

Tactic:
simp only [Matrix.one_mul, List.prod_nil, List.map]

Goal state after:
case nil
n : Type u_1
𝕜 : Type u_3
inst✝² : Field 𝕜
inst✝¹ : DecidableEq n
inst✝ : Fintype n
P : Matrix n n 𝕜 → Prop
M : Matrix n n 𝕜
hdiag : ∀ (D : n → 𝕜), (diagonal D).det = M.det → P (diagonal D)
htransvec : ∀ (t : TransvectionStruct n 𝕜), P t.toMatrix
hmul : ∀ (A B : Matrix n n 𝕜), P A → P B → P (A * B)
L L' : List (TransvectionStruct n 𝕜)
D : n → 𝕜
h : M = (List.map toMatrix L).prod * diagonal D * (List.map toMatrix L').prod
PD : P (diagonal D)
L₂ : List (TransvectionStruct n 𝕜)
E : Matrix n n 𝕜
PE : P E
⊢ P (E * (List.map toMatrix L₂).prod)
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 (fromBlocks A B 0 D)
⊢ (⅟(fromBlocks A B 0 D)).toBlocks₁₁ * A = 1

Tactic:
by
      have := invOf_mul_self (fromBlocks A B 0 D)
      rw [← fromBlocks_toBlocks (⅟(fromBlocks A B 0 D)), fromBlocks_multiply] at this
      simpa only [Matrix.toBlocks_fromBlocks₁₁, Matrix.mul_zero, add_zero, ← fromBlocks_one] using
        congr_arg Matrix.toBlocks₁₁ this

Goal state after:
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 m α
B : Matrix m n α
C : Matrix n m α
D : Matrix n n α
inst✝ : Invertible D
i j : m ⊕ n
⊢ fromBlocks A B C D i j = (fromBlocks D C B A).submatrix (⇑(Equiv.sumComm m n)) (⇑(Equiv.sumComm m n)) i j

Tactic:
cases i <;> cases j <;> rfl

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
P : R[X]
⊢ IsNilpotent (X * P) ↔ IsNilpotent P

Tactic:
exact isNilpotent_X_mul_iff

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

Goal state before:
pp: case pos
R : Type u_1
inst✝ : CommRing R
k : ℕ
hind :
  ∀ m < k, ∀ {P : R[X]}, IsUnit (P.coeff 0) → (∀ (i : ℕ), i ≠ 0 → IsNilpotent (P.coeff i)) → P.natDegree = m → IsUnit P
P : R[X]
hunit : IsUnit (P.coeff 0)
hnil : ∀ (i : ℕ), i ≠ 0 → IsNilpotent (P.coeff i)
h : P.natDegree = k
hdeg : P.natDegree = 0
⊢ IsUnit P

Tactic:
rw [eq_C_of_natDegree_eq_zero hdeg]
    exact hunit.map C

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
k : ℕ
hind :
  ∀ m < k, ∀ {P : R[X]}, IsUnit (P.coeff 0) → (∀ (i : ℕ), i ≠ 0 → IsNilpotent (P.coeff i)) → P.natDegree = m → IsUnit P
P : R[X]
hunit : IsUnit (P.coeff 0)
hnil : ∀ (i : ℕ), i ≠ 0 → IsNilpotent (P.coeff i)
h : P.natDegree = k
hdeg : ¬P.natDegree = 0
P₁ : R[X] := P.eraseLead
hP₁ : P₁ = P.eraseLead
this : IsUnit P₁
⊢ IsUnit P

Tactic:
← eraseLead_add_monomial_natDegree_leadingCoeff P,

Goal state after:
R : Type u_1
inst✝ : CommRing R
k : ℕ
hind :
  ∀ m < k, ∀ {P : R[X]}, IsUnit (P.coeff 0) → (∀ (i : ℕ), i ≠ 0 → IsNilpotent (P.coeff i)) → P.natDegree = m → IsUnit P
P : R[X]
hunit : IsUnit (P.coeff 0)
hnil : ∀ (i : ℕ), i ≠ 0 → IsNilpotent (P.coeff i)
h : P.natDegree = k
hdeg : ¬P.natDegree = 0
P₁ : R[X] := P.eraseLead
hP₁ : P₁ = P.eraseLead
this : IsUnit P₁
⊢ IsUnit (P.eraseLead + (monomial P.natDegree) P.leadingCoeff)
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
hb : Submodule.span R (Set.range b) = ⊤
⊢ Function.Injective ⇑(fromEnd R b)

Tactic:
by
  intro x y e
  ext m
  obtain ⟨m, rfl⟩ : m ∈ LinearMap.range (Fintype.linearCombination R b) := by
    rw [(Fintype.range_linearCombination R b).trans hb]
    exact Submodule.mem_top
  exact (LinearMap.congr_fun e m :)

Goal state after:
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
f : Module.End R M
I : Ideal R
hI : range f ≤ I • ⊤
⊢ ∃ p, p.Monic ∧ p.natDegree = ⊤.spanFinrank ∧ (∀ (k : ℕ), p.coeff k ∈ I ^ (p.natDegree - k)) ∧ (aeval f) p = 0

Tactic:
cases subsingleton_or_nontrivial R

Goal state after:
case inl
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✝ : Subsingleton R
⊢ ∃ p, p.Monic ∧ p.natDegree = ⊤.spanFinrank ∧ (∀ (k : ℕ), p.coeff k ∈ I ^ (p.natDegree - k)) ∧ (aeval f) p = 0

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
⊢ ∃ p, p.Monic ∧ p.natDegree = ⊤.spanFinrank ∧ (∀ (k : ℕ), p.coeff k ∈ I ^ (p.natDegree - k)) ∧ (aeval f) p = 0
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.FG
⊢ p.spanFinrank = 0 ↔ p = ⊥

Tactic:
by
  refine ⟨fun heq ↦ ?_, fun h ↦ by simp [h]⟩
  rw [← Submodule.FG.generators_ncard h, Set.ncard_eq_zero h.finite_generators] at heq
  rw [← p.span_generators, heq, span_empty]

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
⊢ ∃ s,
    Cardinal.lift.{u, v} (Cardinal.mk ↑s) ≤ Cardinal.lift.{v, u} (Cardinal.mk ↑(generators I)) ∧
      Submodule.span T s = map f I

Tactic:
refine ⟨f '' I.generators, Cardinal.mk_image_le_lift, le_antisymm (span_le.2 (fun s ⟨r, hr, hfr⟩ ↦
    hfr ▸ mem_map_of_mem _ <| span_generators I ▸ subset_span hr)) ?_⟩

Goal state after:
R : Type u
inst✝¹ : Semiring R
T : Type v
inst✝ : Semiring T
f : R →+* T
I : Ideal R
⊢ map f I ≤ Submodule.span T (⇑f '' generators I)
Module: Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic

Goal state before:
pp: case mp
R : Type u_1
B : Type u_3
inst✝² : CommRing R
inst✝¹ : Ring B
inst✝ : Algebra R B
r : B
p : R[X]
hmp : p.Monic
hpr : eval₂ (algebraMap R B) r p = 0
⊢ eval₂ (algebraMap R B) r p = 0

Tactic:
hpr

Goal state after:
case mp
R : Type u_1
B : Type u_3
inst✝² : CommRing R
inst✝¹ : Ring B
inst✝ : Algebra R B
r : B
p : R[X]
hmp : p.Monic
hpr : eval₂ (algebraMap R B) r p = 0
⊢ 0 = 0
Module: Mathlib.Algebra.Polynomial.Lifts

Goal state before:
pp: case mp
R : Type u
inst✝¹ : Semiring R
S : Type v
inst✝ : Semiring S
f : R →+* S
p : S[X]
h : ∀ (n : ℕ), p.coeff n ∈ Set.range ⇑f
a✝ : S
hc : a✝ ∈ ↑p.coeffs
n : ℕ
hn : a✝ = p.coeff n
⊢ a✝ ∈ Set.range ⇑f

Tactic:
exact hn ▸ h n

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

Goal state before:
pp: case pos
R : Type u_1
inst✝ : Semiring R
k l i : ℕ
hikl : i < k + l
⊢ (i - l).choose k * i.choose l = (k + l).choose k * i.choose (k + l)

pp: case neg
R : Type u_1
inst✝ : Semiring R
k l i : ℕ
hikl : k + l ≤ i
⊢ (i - l).choose k * i.choose l = (k + l).choose k * i.choose (k + l)

Tactic:
· rw [choose_eq_zero_of_lt hikl, mul_zero]
    by_cases! hil : i < l
    · rw [choose_eq_zero_of_lt hil, mul_zero]
    · rw [← tsub_lt_iff_right hil] at hikl
      rw [choose_eq_zero_of_lt hikl, zero_mul]

Goal state after:
case neg
R : Type u_1
inst✝ : Semiring R
k l i : ℕ
hikl : k + l ≤ i
⊢ (i - l).choose k * i.choose l = (k + l).choose k * i.choose (k + l)
Module: Mathlib.Algebra.Polynomial.Taylor

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
p : R[X]
x y : R
this :
  ∀ (t : R), eval t ((taylor x) p) = ∑ i ∈ Finset.range (((taylor x) p).natDegree + 2), ((taylor x) p).coeff i * t ^ i
⊢ ∃ c, c * y ^ 2 + eval x (derivative p) * y + eval x p = eval (x + y) p

Tactic:
rw [add_comm, ← p.taylor_eval x y, this, Finset.sum_range_succ', Finset.sum_range_succ']

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
p : R[X]
x y : R
this :
  ∀ (t : R), eval t ((taylor x) p) = ∑ i ∈ Finset.range (((taylor x) p).natDegree + 2), ((taylor x) p).coeff i * t ^ i
⊢ ∃ c,
    c * y ^ 2 + eval x (derivative p) * y + eval x p =
      ∑ k ∈ Finset.range ((taylor x) p).natDegree, ((taylor x) p).coeff (k + 1 + 1) * y ^ (k + 1 + 1) +
          ((taylor x) p).coeff (0 + 1) * y ^ (0 + 1) +
        ((taylor x) p).coeff 0 * y ^ 0
Module: Mathlib.RingTheory.Polynomial.ScaleRoots

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
p : R[X]
hp : p.Splits
r : R
⊢ (p.scaleRoots r).Splits

Tactic:
cases subsingleton_or_nontrivial R

Goal state after:
case inl
R : Type u_1
inst✝ : CommSemiring R
p : R[X]
hp : p.Splits
r : R
h✝ : Subsingleton R
⊢ (p.scaleRoots r).Splits

case inr
R : Type u_1
inst✝ : CommSemiring R
p : R[X]
hp : p.Splits
r : R
h✝ : Nontrivial R
⊢ (p.scaleRoots r).Splits
Module: Mathlib.RingTheory.Polynomial.ScaleRoots

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
p : R[X]
r a : R
hr : IsLeftRegular r
⊢ rootMultiplicity (r * a) (p.scaleRoots r) = rootMultiplicity a p

Tactic:
cases subsingleton_or_nontrivial R

Goal state after:
case inl
R : Type u_1
inst✝ : CommRing R
p : R[X]
r a : R
hr : IsLeftRegular r
h✝ : Subsingleton R
⊢ rootMultiplicity (r * a) (p.scaleRoots r) = rootMultiplicity a p

case inr
R : Type u_1
inst✝ : CommRing R
p : R[X]
r a : R
hr : IsLeftRegular r
h✝ : Nontrivial R
⊢ rootMultiplicity (r * a) (p.scaleRoots r) = rootMultiplicity a p
Module: Mathlib.Algebra.Polynomial.Splits

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
f : R[X]
⊢ f.Splits ↔ ∃ m, f = C f.leadingCoeff * (Multiset.map (fun x ↦ X - C x) m).prod

Tactic:
refine splits_iff_exists_multiset'.trans ⟨?_, ?_⟩ <;>
    rintro ⟨m, hm⟩

Goal state after:
case refine_1
R : Type u_1
inst✝ : CommRing R
f : R[X]
m : Multiset R
hm : f = C f.leadingCoeff * (Multiset.map (fun x ↦ X + C x) m).prod
⊢ ∃ m, f = C f.leadingCoeff * (Multiset.map (fun x ↦ X - C x) m).prod

case refine_2
R : Type u_1
inst✝ : CommRing R
f : R[X]
m : Multiset R
hm : f = C f.leadingCoeff * (Multiset.map (fun x ↦ X - C x) m).prod
⊢ ∃ m, f = C f.leadingCoeff * (Multiset.map (fun x ↦ X + C x) m).prod
Module: Mathlib.Algebra.Polynomial.Splits

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
f : R[X]
inst✝¹ : IsDomain R
hf : f.Splits
hm : f.Monic
S : Type u_4
inst✝ : Ring S
i : S →+* R
hr : ∀ a ∈ f.roots, a ∈ i.range
⊢ f ∈ lifts i

Tactic:
hf.eq_prod_roots_of_monic hm,

Goal state after:
R : Type u_1
inst✝² : CommRing R
f : R[X]
inst✝¹ : IsDomain R
hf : f.Splits
hm : f.Monic
S : Type u_4
inst✝ : Ring S
i : S →+* R
hr : ∀ a ∈ f.roots, a ∈ i.range
⊢ (Multiset.map (fun x ↦ X - C x) f.roots).prod ∈ lifts i
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
n : Type u_5
inst✝¹ : Fintype n
inst✝ : DecidableEq n
M : Matrix n n A
h : ∀ (i j : n), IsIntegral R (M i j)
⊢ IsIntegral R M.det

Tactic:
rw [Matrix.det_apply]

Goal state after:
R : Type u_1
A : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
n : Type u_5
inst✝¹ : Fintype n
inst✝ : DecidableEq n
M : Matrix n n A
h : ∀ (i j : n), IsIntegral R (M i j)
⊢ IsIntegral R (∑ σ, Equiv.Perm.sign σ • ∏ i, M (σ i) i)
Module: Mathlib.Algebra.Polynomial.Splits

Goal state before:
pp: case neg
R : Type u_1
inst✝¹ : CommRing R
f : R[X]
inst✝ : IsDomain R
a : R
hf : ((X - C a) * f).Splits
hf₀ : ¬f = 0
this : (X - C a) * f = C ((X - C a) * f).leadingCoeff * (Multiset.map (fun x ↦ X - C x) ((X - C a) * f).roots).prod
⊢ f.Splits

Tactic:
rw [leadingCoeff_mul, leadingCoeff_X_sub_C, one_mul,
    roots_mul (mul_ne_zero (X_sub_C_ne_zero _) hf₀), roots_X_sub_C,
    Multiset.singleton_add, Multiset.map_cons, Multiset.prod_cons, mul_left_comm] at this

Goal state after:
case neg
R : Type u_1
inst✝¹ : CommRing R
f : R[X]
inst✝ : IsDomain R
a : R
hf : ((X - C a) * f).Splits
hf₀ : ¬f = 0
this : (X - C a) * f = (X - C a) * (C f.leadingCoeff * (Multiset.map (fun x ↦ X - C x) f.roots).prod)
⊢ f.Splits
Module: Mathlib.Algebra.Polynomial.Splits

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
f : R[X]
inst✝ : IsDomain R
⊢ (X * f).Splits ↔ f.Splits

Tactic:
by simp [splits_mul']

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

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : Field A
inst✝³ : Algebra R A
inst✝² : CommRing B
inst✝¹ : IsDomain B
inst✝ : Algebra R B
f : R[X]
hf : (map (algebraMap R A) f).Splits
g : A →ₐ[R] B
⊢ ↑(Finset.image (⇑g) (f.aroots A).toFinset) = f.rootSet B

Tactic:
← Multiset.toFinset_map,

Goal state after:
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : Field A
inst✝³ : Algebra R A
inst✝² : CommRing B
inst✝¹ : IsDomain B
inst✝ : Algebra R B
f : R[X]
hf : (map (algebraMap R A) f).Splits
g : A →ₐ[R] B
⊢ ↑(Multiset.map (⇑g) (f.aroots A)).toFinset = f.rootSet B