mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.Matrix.Transvection

Goal state before:
pp: 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 ())

Tactic:
rw [if_neg, if_neg]

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

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
Module: Mathlib.LinearAlgebra.Matrix.Kronecker

Goal state before:
pp: R : Type u_1
S : Type u_2
α : Type u_3
β : Type u_5
γ : Type u_7
m : Type u_10
n : Type u_11
inst✝¹³ : Semiring S
inst✝¹² : Semiring R
inst✝¹¹ : Fintype m
inst✝¹⁰ : Fintype n
inst✝⁹ : DecidableEq m
inst✝⁸ : DecidableEq n
inst✝⁷ : NonAssocSemiring α
inst✝⁶ : NonAssocSemiring β
inst✝⁵ : CommRing γ
inst✝⁴ : Module R α
inst✝³ : Module S β
inst✝² : Module R γ
inst✝¹ : Module S γ
inst✝ : SMulCommClass S R γ
f : α →ₗ[R] β →ₗ[S] γ
h_comm : ∀ (a b : α) (a' b' : β), (f (a * b)) (a' * b') = (f a) a' * (f b) b'
A : Matrix m m α
B : Matrix n n β
⊢ ∀ (x : α), (f x) 0 = 0

Tactic:
intro; exact map_zero _

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 fun v ↦ v ᵥ* A) ↔ IsUnit A

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
  · rw [← vecMul_surjective_iff_isUnit]
    exact LinearMap.surjective_of_injective (f := A.vecMulLinear) h
  exact vecMul_injective_of_isUnit h

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

Goal state before:
pp: 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

Tactic:
rw [if_neg, if_neg]

Goal state after:
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
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
⊢ ¬n + 1 ≤ ↑i

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
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
⊢ ¬n ≤ ↑i
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:
M.twoBlockTriangular_det fun i => ¬p i,

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
⊢ (M.toSquareBlockProp fun i ↦ ¬p i).det * (M.toSquareBlockProp fun i ↦ ¬¬p i).det =
    (M.toSquareBlockProp p).det * (M.toSquareBlockProp fun i ↦ ¬p i).det

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
⊢ ∀ (i : m), ¬¬p i → ∀ (j : m), ¬p j → M i j = 0
Module: Mathlib.LinearAlgebra.Matrix.Block

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

Tactic:
cases isEmpty_or_nonempty m

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

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

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

Tactic:
nonsing_inv_nonsing_inv _ h

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

Goal state before:
pp: case neg
m : Type u
n : Type u'
α : Type v
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : CommRing α
inst✝¹ : Fintype m
inst✝ : DecidableEq m
A : Matrix m m α
B : Matrix n n α
hA : IsUnit A.det
hB : ¬IsUnit B.det
⊢ (kroneckerMap (fun x1 x2 ↦ x1 * x2) A B)⁻¹ = kroneckerMap (fun x1 x2 ↦ x1 * x2) A⁻¹ B⁻¹

Tactic:
cases isEmpty_or_nonempty m

Goal state after:
case neg.inl
m : Type u
n : Type u'
α : Type v
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : CommRing α
inst✝¹ : Fintype m
inst✝ : DecidableEq m
A : Matrix m m α
B : Matrix n n α
hA : IsUnit A.det
hB : ¬IsUnit B.det
h✝ : IsEmpty m
⊢ (kroneckerMap (fun x1 x2 ↦ x1 * x2) A B)⁻¹ = kroneckerMap (fun x1 x2 ↦ x1 * x2) A⁻¹ B⁻¹

case neg.inr
m : Type u
n : Type u'
α : Type v
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : CommRing α
inst✝¹ : Fintype m
inst✝ : DecidableEq m
A : Matrix m m α
B : Matrix n n α
hA : IsUnit A.det
hB : ¬IsUnit B.det
h✝ : Nonempty m
⊢ (kroneckerMap (fun x1 x2 ↦ x1 * x2) A B)⁻¹ = kroneckerMap (fun x1 x2 ↦ x1 * x2) A⁻¹ B⁻¹
Module: Mathlib.LinearAlgebra.Matrix.Transvection

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

Tactic:
refine
    ⟨L₀.map (sumInl Unit) ++ L₁, L₁' ++ L₀'.map (sumInl Unit),
      Sum.elim D₀ fun _ => M' (inr unit) (inr unit), ?_⟩

Goal state after:
𝕜 : Type u_3
inst✝ : Field 𝕜
r : ℕ
IH :
  ∀ (M : Matrix (Fin r) (Fin r) 𝕜),
    ∃ L₀ L₀' D₀, (List.map toMatrix L₀).prod * M * (List.map toMatrix L₀').prod = diagonal D₀
M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
L₁ L₁' : List (TransvectionStruct (Fin r ⊕ Unit) 𝕜)
hM : ((List.map toMatrix L₁).prod * M * (List.map toMatrix L₁').prod).IsTwoBlockDiagonal
M' : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜 := (List.map toMatrix L₁).prod * M * (List.map toMatrix L₁').prod
M'' : Matrix (Fin r) (Fin r) 𝕜 := M'.toBlocks₁₁
L₀ L₀' : List (TransvectionStruct (Fin r) 𝕜)
D₀ : Fin r → 𝕜
h₀ : (List.map toMatrix L₀).prod * M'' * (List.map toMatrix L₀').prod = diagonal D₀
c : 𝕜 := M' (inr ()) (inr ())
⊢ (List.map toMatrix (List.map (sumInl Unit) L₀ ++ L₁)).prod * M *
      (List.map toMatrix (L₁' ++ List.map (sumInl Unit) L₀')).prod =
    diagonal (Sum.elim D₀ fun x ↦ M' (inr ()) (inr ()))
Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Basic

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

Tactic:
coeff_C,

Goal state after:
case neg
R : Type u_1
inst✝² : CommRing R
n : Type u_4
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
k : ℕ
i j : n
h : ¬i = j
⊢ (-if k = 0 then M i j else 0) = ((if 1 = k then 1 else 0) - (C M).coeff k) i j
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 + A * B).det = (B * A + 1).det

Tactic:
det_one_add_mul_comm,

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

Tactic:
det_one_add_mul_comm,

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
α : Type u_4
inst✝³ : Fintype m
inst✝² : DecidableEq m
inst✝¹ : CommRing α
ι : Type u_5
inst✝ : Unique ι
u v : m → α
⊢ (1 + replicateCol ι u * replicateRow ι v).det = 1 + v ⬝ᵥ u

Tactic:
det_one_add_mul_comm,

Goal state after:
m : Type u_2
α : Type u_4
inst✝³ : Fintype m
inst✝² : DecidableEq m
inst✝¹ : CommRing α
ι : Type u_5
inst✝ : Unique ι
u v : m → α
⊢ (1 + replicateRow ι v * replicateCol ι u).det = 1 + v ⬝ᵥ u
Module: Mathlib.LinearAlgebra.Matrix.SchurComplement

Goal state before:
pp: m : Type u_2
α : Type u_4
inst✝³ : Fintype m
inst✝² : DecidableEq m
inst✝¹ : CommRing α
ι : Type u_5
inst✝ : Unique ι
A : Matrix m m α
hA : IsUnit A.det
u v : m → α
⊢ A.det * (1 + A⁻¹ * replicateCol ι u * replicateRow ι v).det =
    A.det * (1 + replicateRow ι v * A⁻¹ * replicateCol ι u).det

pp: m : Type u_2
α : Type u_4
inst✝³ : Fintype m
inst✝² : DecidableEq m
inst✝¹ : CommRing α
ι : Type u_5
inst✝ : Unique ι
A : Matrix m m α
hA : IsUnit A.det
u v : m → α
⊢ IsUnit A.det

Tactic:
det_one_add_mul_comm,

Goal state after:
m : Type u_2
α : Type u_4
inst✝³ : Fintype m
inst✝² : DecidableEq m
inst✝¹ : CommRing α
ι : Type u_5
inst✝ : Unique ι
A : Matrix m m α
hA : IsUnit A.det
u v : m → α
⊢ A.det * (1 + replicateRow ι v * (A⁻¹ * replicateCol ι u)).det =
    A.det * (1 + replicateRow ι v * A⁻¹ * replicateCol ι u).det

m : Type u_2
α : Type u_4
inst✝³ : Fintype m
inst✝² : DecidableEq m
inst✝¹ : CommRing α
ι : Type u_5
inst✝ : Unique ι
A : Matrix m m α
hA : IsUnit A.det
u v : m → α
⊢ IsUnit 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 m α
U : Matrix m n α
V : Matrix n m α
hA : IsUnit A.det
⊢ A.det * (1 + A⁻¹ * U * V).det = A.det * (1 + V * A⁻¹ * U).det

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 α
U : Matrix m n α
V : Matrix n m α
hA : IsUnit A.det
⊢ IsUnit A.det

Tactic:
det_one_add_mul_comm,

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 m α
U : Matrix m n α
V : Matrix n m α
hA : IsUnit A.det
⊢ A.det * (1 + V * (A⁻¹ * U)).det = A.det * (1 + V * A⁻¹ * U).det

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 α
U : Matrix m n α
V : Matrix n m α
hA : IsUnit A.det
⊢ IsUnit A.det
Module: Mathlib.RingTheory.Nilpotent.Basic

Goal state before:
pp: case succ
R : Type u_1
inst✝ : MonoidWithZero R
e : R
idem : IsIdempotentElem e
n : ℕ
hn : e ^ (n + 1) = 0
⊢ e = 0

Tactic:
· rw [← hn, idem.pow_succ_eq]

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommMonoidWithZero R
inst✝ : IsCancelMulZero R
x y : R
hy : IsRadical y
h0 : y ≠ 0
hxy : x ∣ y
⊢ ∀ (x_1 : R), x ∣ x_1 ^ 2 → x ∣ x_1

Tactic:
obtain ⟨z, rfl⟩ := hxy
  refine fun w dvd ↦ ((mul_dvd_mul_iff_right <| right_ne_zero_of_mul h0).mp <| hy 2 _ ?_)
  rw [mul_pow]
  gcongr
  exact dvd_pow_self _ two_ne_zero

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
P : R[X]
N : ℕ
hN : P.natDegree ≤ N
⊢ (∀ (i : ℕ), IsNilpotent ((reflect N P).coeff i)) ↔ ∀ (i : ℕ), IsNilpotent (P.coeff i)

Tactic:
refine ⟨fun h i ↦ ?_, fun h i ↦ ?_⟩ <;> rcases le_or_gt i N with hi | hi

Goal state after:
case refine_1.inl
R : Type u_1
inst✝ : CommRing R
P : R[X]
N : ℕ
hN : P.natDegree ≤ N
h : ∀ (i : ℕ), IsNilpotent ((reflect N P).coeff i)
i : ℕ
hi : i ≤ N
⊢ IsNilpotent (P.coeff i)

case refine_1.inr
R : Type u_1
inst✝ : CommRing R
P : R[X]
N : ℕ
hN : P.natDegree ≤ N
h : ∀ (i : ℕ), IsNilpotent ((reflect N P).coeff i)
i : ℕ
hi : N < i
⊢ IsNilpotent (P.coeff i)

case refine_2.inl
R : Type u_1
inst✝ : CommRing R
P : R[X]
N : ℕ
hN : P.natDegree ≤ N
h : ∀ (i : ℕ), IsNilpotent (P.coeff i)
i : ℕ
hi : i ≤ N
⊢ IsNilpotent ((reflect N P).coeff i)

case refine_2.inr
R : Type u_1
inst✝ : CommRing R
P : R[X]
N : ℕ
hN : P.natDegree ≤ N
h : ∀ (i : ℕ), IsNilpotent (P.coeff i)
i : ℕ
hi : N < i
⊢ IsNilpotent ((reflect N P).coeff i)
Module: Mathlib.RingTheory.Polynomial.Nilpotent

Goal state before:
pp: case refine_2.inl
R : Type u_1
inst✝ : CommRing R
P : R[X]
N : ℕ
hN : P.natDegree ≤ N
h : ∀ (i : ℕ), IsNilpotent (P.coeff i)
i : ℕ
hi : i ≤ N
⊢ IsNilpotent ((reflect N P).coeff i)

Tactic:
simpa [hi, revAt_le] using h (N - i)

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
inst✝ : RankCondition R
ι : Type u
v : ι → M
hv : Function.Injective v
hs : LinearIndependent R v
⊢ (span R (Set.range v)).spanRank = #ι

Tactic:
refine le_antisymm (le_trans (spanRank_span_le_card _) mk_range_le) (le_ciInf fun x ↦ ?_)
  have : #x.1 = #((Subtype.val : span R (.range v) → _) ⁻¹' x.1) :=
    (mk_preimage_of_injective_of_subset_range _ _ Subtype.val_injective (by simp [← x.2])).symm
  rw [this]
  refine le_trans ?_ ((Module.Basis.span hs).le_span (R := R) (J := Subtype.val ⁻¹' x.1) ?_)
  · rw [mk_range_eq]
    exact .of_comp (f := Subtype.val) (by convert! hv; ext; simp [Module.Basis.span_apply])
  · apply map_injective_of_injective (f := (span R _).subtype) (injective_subtype _)
    simp [map_span, Set.image_preimage_eq_inter_range, Set.inter_eq_self_of_subset_left, ← x.2]

Goal state after:
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
inst✝ : Nontrivial R
M : Matrix n n R
h : ¬Fintype.card n = 0
h1 : (∏ i, (X - C (M i i))).degree = ↑(Fintype.card n)
⊢ (∏ i, (X - C (M i i))).degree = ↑(Fintype.card n)

pp: case neg
R : Type u
inst✝³ : CommRing R
n : Type v
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : Nontrivial R
M : Matrix n n R
h : ¬Fintype.card n = 0
h1 : (∏ i, (X - C (M i i))).degree = ↑(Fintype.card n)
⊢ (M.charpoly - ∏ i, (X - C (M i i))).degree < (∏ i, (X - C (M i i))).degree

Tactic:
· exact h1

Goal state after:
case neg
R : Type u
inst✝³ : CommRing R
n : Type v
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : Nontrivial R
M : Matrix n n R
h : ¬Fintype.card n = 0
h1 : (∏ i, (X - C (M i i))).degree = ↑(Fintype.card n)
⊢ (M.charpoly - ∏ i, (X - C (M i i))).degree < (∏ i, (X - C (M i i))).degree
Module: Mathlib.Algebra.Module.SpanRank

Goal state before:
pp: R : Type u_1
S : Type u_2
M : Type u
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring S
inst✝⁴ : AddCommMonoid M
inst✝³ : Algebra R S
inst✝² : Module R M
inst✝¹ : Module S M
inst✝ : IsScalarTower R S M
H : Function.Surjective ⇑(algebraMap R S)
N : Submodule S M
⊢ (restrictScalars R N).spanRank = N.spanRank

Tactic:
refine N.le_spanRank_restrictScalars.antisymm' ?_

Goal state after:
R : Type u_1
S : Type u_2
M : Type u
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring S
inst✝⁴ : AddCommMonoid M
inst✝³ : Algebra R S
inst✝² : Module R M
inst✝¹ : Module S M
inst✝ : IsScalarTower R S M
H : Function.Surjective ⇑(algebraMap R S)
N : Submodule S M
⊢ (restrictScalars R N).spanRank ≤ N.spanRank
Module: Mathlib.Algebra.Polynomial.Eval.Subring

Goal state before:
pp: case mpr
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
p : S[X]
⊢ (∀ (n : ℕ), p.coeff n ∈ f.rangeS) → p ∈ (mapRingHom f).rangeS

Tactic:
intro h
    rw [p.as_sum_range_C_mul_X_pow]
    refine (mapRingHom f).rangeS.sum_mem ?_
    intro i _hi
    rcases h i with ⟨c, hc⟩
    use C c * X ^ i
    rw [coe_mapRingHom, Polynomial.map_mul, map_C, hc, Polynomial.map_pow, map_X]

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

Goal state before:
pp: case pos
R : Type u
inst✝³ : CommRing R
n : Type v
inst✝² : DecidableEq n
inst✝¹ : Fintype n
M : Matrix n n R
inst✝ : Nontrivial R
hn : Fintype.card n = 2
this : Nonempty n
i : ℕ
hi : i ∈ range 3
⊢ M.charpoly.coeff i = (X ^ 2 - C M.trace * X + C M.det).coeff i

Tactic:
fin_cases hi
    · simp [det_eq_sign_charpoly_coeff, hn]
    · simp [trace_eq_neg_charpoly_coeff, hn]
    · simpa [leadingCoeff, charpoly_natDegree_eq_dim, hn, coeff_X] using
        M.charpoly_monic.leadingCoeff

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

Goal state before:
pp: n : Type v
inst✝² : DecidableEq n
inst✝¹ : Fintype n
K : Type u_1
k : ℕ
inst✝ : CommRing K
M : Matrix n n K
m : ℕ
i j : n
⊢ (matPolyEquiv ((↑(expand K k)).mapMatrix (M ^ k).charmatrix)).coeff m i j =
    ((X ^ k).coeff m - (C (M ^ k)).coeff m) i j

Tactic:
coeff_C,

Goal state after:
n : Type v
inst✝² : DecidableEq n
inst✝¹ : Fintype n
K : Type u_1
k : ℕ
inst✝ : CommRing K
M : Matrix n n K
m : ℕ
i j : n
⊢ (matPolyEquiv ((↑(expand K k)).mapMatrix (M ^ k).charmatrix)).coeff m i j =
    ((X ^ k).coeff m - if m = 0 then M ^ k else 0) i j
Module: Mathlib.RingTheory.IntegralClosure.Algebra.Basic

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
inst✝⁵ : IsDomain A
M : Type u_5
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : Module A M
inst✝¹ : IsScalarTower R A M
inst✝ : Module.IsTorsionFree A M
N : Submodule R M
hN : N ≠ ⊥
hN' : N.FG
x : A
hx : ∀ n ∈ N, x • n ∈ N
A' : Subalgebra R A :=
  { carrier := {x | ∀ n ∈ N, x • n ∈ N}, mul_mem' := ⋯, one_mem' := ⋯, add_mem' := ⋯, zero_mem' := ⋯,
    algebraMap_mem' := ⋯ }
⊢ ∀ (m : R) (x : ↥A'),
    (DistribSMul.toLinearMap R M (m • x)).restrict ⋯ = (RingHom.id R) m • (DistribSMul.toLinearMap R M x).restrict ⋯

Tactic:
by intro r s; ext; apply smul_assoc

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 ↑M.charpoly.natDegree) = invert q

Tactic:
charpoly_natDegree_eq_dim,

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)) = invert q
Module: Mathlib.RingTheory.Polynomial.Subring

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
p : R[X]
T : Subring R
hp : ↑p.coeffs ⊆ ↑T
⊢ (p.toSubring T hp).degree = p.degree

Tactic:
by simp [degree]

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

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

Tactic:
refine ⟨fun hf ↦ ?_, ?_⟩

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

case refine_2
R : Type u_1
inst✝ : CommSemiring R
f : R[X]
⊢ (∃ m, f = C f.leadingCoeff * (Multiset.map (fun x ↦ X + C x) m).prod) → f.Splits