mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Polynomial.Lifts

Goal state before:
pp: case inl
R : Type u
inst✝¹ : Semiring R
S : Type v
inst✝ : Semiring S
f : R →+* S
n : ℕ
hl : (monomial n) 0 ∈ lifts f
⊢ ∃ q, map f q = (monomial n) 0 ∧ q.degree = ((monomial n) 0).degree

pp: case inr
R : Type u
inst✝¹ : Semiring R
S : Type v
inst✝ : Semiring S
f : R →+* S
s : S
n : ℕ
hl : (monomial n) s ∈ lifts f
h : s ≠ 0
⊢ ∃ q, map f q = (monomial n) s ∧ q.degree = ((monomial n) s).degree

Tactic:
·

Goal state after:
case inl
R : Type u
inst✝¹ : Semiring R
S : Type v
inst✝ : Semiring S
f : R →+* S
n : ℕ
hl : (monomial n) 0 ∈ lifts f
⊢ ∃ q, map f q = (monomial n) 0 ∧ q.degree = ((monomial n) 0).degree
Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff

Goal state before:
pp: case pos.«_@».Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff.4094078725._hygCtx._hyg.105.«2»
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
⊢ M.charpoly.coeff 2 = (X ^ 2 - C M.trace * X + C M.det).coeff 2

Tactic:
·

Goal state after:
case pos.«_@».Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff.4094078725._hygCtx._hyg.105.«2»
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
⊢ M.charpoly.coeff 2 = (X ^ 2 - C M.trace * X + C M.det).coeff 2
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
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:
·

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

Goal state before:
pp: case pos
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
hij : i = j
⊢ ((expand K k) ((M ^ k).charmatrix i j)).coeff m = ((if m = k then 1 else 0) - if m = 0 then M ^ k else 0) i j

pp: case neg
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
hij : ¬i = j
⊢ ((expand K k) ((M ^ k).charmatrix i j)).coeff m = ((if m = k then 1 else 0) - if m = 0 then M ^ k else 0) i j

Tactic:
·

Goal state after:
case pos
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
hij : i = j
⊢ ((expand K k) ((M ^ k).charmatrix i j)).coeff m = ((if m = k then 1 else 0) - if m = 0 then M ^ k else 0) i j
Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff

Goal state before:
pp: case neg
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
hij : ¬i = j
⊢ ((expand K k) ((M ^ k).charmatrix i j)).coeff m = ((if m = k then 1 else 0) - if m = 0 then M ^ k else 0) i j

Tactic:
·

Goal state after:
case neg
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
hij : ¬i = j
⊢ ((expand K k) ((M ^ k).charmatrix i j)).coeff m = ((if m = k then 1 else 0) - if m = 0 then M ^ k else 0) i j
Module: Mathlib.Algebra.Polynomial.Lifts

Goal state before:
pp: case inl
R : Type u
inst✝¹ : Semiring R
S : Type v
inst✝ : Semiring S
f : R →+* S
p : S[X]
hlifts : p ∈ lifts f
hp : p.Monic
hR : Subsingleton S
⊢ ∃ q, map f q = p ∧ q.natDegree = p.natDegree ∧ q.Monic

pp: case inr
R : Type u
inst✝¹ : Semiring R
S : Type v
inst✝ : Semiring S
f : R →+* S
p : S[X]
hlifts : p ∈ lifts f
hp : p.Monic
hR : Nontrivial S
⊢ ∃ q, map f q = p ∧ q.natDegree = p.natDegree ∧ q.Monic

Tactic:
·

Goal state after:
case inl
R : Type u
inst✝¹ : Semiring R
S : Type v
inst✝ : Semiring S
f : R →+* S
p : S[X]
hlifts : p ∈ lifts f
hp : p.Monic
hR : Subsingleton S
⊢ ∃ q, map f q = p ∧ q.natDegree = p.natDegree ∧ q.Monic
Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff

Goal state before:
pp: case zero
R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
I : Ideal R
h : ∀ (i j : n), M i j ∈ I
k : ℕ
c : Equiv.Perm n
this : ∑ x, 1 = Fintype.card n
i : n
⊢ (M.charmatrix (c i) i).coeff 0 ∈ I ^ (1 - 0)

pp: case succ
R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
I : Ideal R
h : ∀ (i j : n), M i j ∈ I
k✝ : ℕ
c : Equiv.Perm n
this : ∑ x, 1 = Fintype.card n
i : n
k : ℕ
⊢ (M.charmatrix (c i) i).coeff (k + 1) ∈ I ^ (1 - (k + 1))

Tactic:
·

Goal state after:
case zero
R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
I : Ideal R
h : ∀ (i j : n), M i j ∈ I
k : ℕ
c : Equiv.Perm n
this : ∑ x, 1 = Fintype.card n
i : n
⊢ (M.charmatrix (c i) i).coeff 0 ∈ I ^ (1 - 0)
Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff

Goal state before:
pp: case succ
R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
I : Ideal R
h : ∀ (i j : n), M i j ∈ I
k✝ : ℕ
c : Equiv.Perm n
this : ∑ x, 1 = Fintype.card n
i : n
k : ℕ
⊢ (M.charmatrix (c i) i).coeff (k + 1) ∈ I ^ (1 - (k + 1))

Tactic:
·

Goal state after:
case succ
R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
I : Ideal R
h : ∀ (i j : n), M i j ∈ I
k✝ : ℕ
c : Equiv.Perm n
this : ∑ x, 1 = Fintype.card n
i : n
k : ℕ
⊢ (M.charmatrix (c i) i).coeff (k + 1) ∈ I ^ (1 - (k + 1))
Module: Mathlib.Data.Nat.Choose.Vandermonde

Goal state before:

Tactic:
(m + n).choose k = ((X + 1) ^ (m + n)).coeff k := by rw [coeff_X_add_one_pow, cast_id]
    _ = ((X + 1) ^ m * (X + 1) ^ n).coeff k := by rw [pow_add]
    _ = ∑ ij ∈ antidiagonal k, m.choose ij.1 * n.choose ij.2 := by
      rw [coeff_mul, Finset.sum_congr rfl]
      simp only [coeff_X_add_one_pow, cast_id, imp_true_iff]

Goal state after:
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' := ⋯ }
f : ↥A' →ₐ[R] Module.End R ↥N :=
  AlgHom.ofLinearMap { toFun := fun x ↦ (DistribSMul.toLinearMap R M x).restrict ⋯, map_add' := ⋯, map_smul' := ⋯ } ⋯ ⋯
a : M
ha₁ : a ∈ N
ha₂ : a ≠ 0
s : ↥A'
hs : s ∈ f.toLinearMap.ker
this : ↑s • a = 0
⊢ s ∈ ⊥

Tactic:
exact Subtype.ext ((smul_eq_zero_iff_left ha₂).1 this)

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

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

pp: case inr
R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
a✝ : Nontrivial R
h✝ : Nonempty n
⊢ M.charpolyRev.coeff 1 = -M.trace

Tactic:
·

Goal state after:
case inl
R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
a✝ : Nontrivial R
h✝ : IsEmpty n
⊢ M.charpolyRev.coeff 1 = -M.trace
Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff

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

Tactic:
·

Goal state after:
case inr
R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
a✝ : Nontrivial R
h✝ : Nonempty n
⊢ M.charpolyRev.coeff 1 = -M.trace
Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff

Goal state before:
pp: case inl
R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
hM : IsNilpotent M
h✝ : IsEmpty n
⊢ IsNilpotent M.trace

pp: case inr
R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
hM : IsNilpotent M
h✝ : Nonempty n
⊢ IsNilpotent M.trace

Tactic:
·

Goal state after:
case inl
R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
hM : IsNilpotent M
h✝ : IsEmpty n
⊢ IsNilpotent M.trace
Module: Mathlib.Algebra.Polynomial.HasseDeriv

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
k : ℕ
f : R[X]
n : ℕ
⊢ (if n + k - k = n then ↑((n + k).choose k) * f.coeff (n + k) else 0) = ↑((n + k).choose k) * f.coeff (n + k)

pp: case h₀
R : Type u_1
inst✝ : Semiring R
k : ℕ
f : R[X]
n : ℕ
⊢ ∀ b ∈ f.support, b ≠ n + k → ((monomial (b - k)) (↑(b.choose k) * f.coeff b)).coeff n = 0

pp: case h₁
R : Type u_1
inst✝ : Semiring R
k : ℕ
f : R[X]
n : ℕ
⊢ n + k ∉ f.support → ((monomial (n + k - k)) (↑((n + k).choose k) * f.coeff (n + k))).coeff n = 0

Tactic:
·

Goal state after:
R : Type u_1
inst✝ : Semiring R
k : ℕ
f : R[X]
n : ℕ
⊢ (if n + k - k = n then ↑((n + k).choose k) * f.coeff (n + k) else 0) = ↑((n + k).choose k) * f.coeff (n + k)
Module: Mathlib.Algebra.Polynomial.HasseDeriv

Goal state before:
pp: case h₀
R : Type u_1
inst✝ : Semiring R
k : ℕ
f : R[X]
n : ℕ
⊢ ∀ b ∈ f.support, b ≠ n + k → ((monomial (b - k)) (↑(b.choose k) * f.coeff b)).coeff n = 0

pp: case h₁
R : Type u_1
inst✝ : Semiring R
k : ℕ
f : R[X]
n : ℕ
⊢ n + k ∉ f.support → ((monomial (n + k - k)) (↑((n + k).choose k) * f.coeff (n + k))).coeff n = 0

Tactic:
·

Goal state after:
case h₀
R : Type u_1
inst✝ : Semiring R
k : ℕ
f : R[X]
n : ℕ
⊢ ∀ b ∈ f.support, b ≠ n + k → ((monomial (b - k)) (↑(b.choose k) * f.coeff b)).coeff n = 0
Module: Mathlib.Algebra.Polynomial.HasseDeriv

Goal state before:
pp: case pos
R : Type u_1
inst✝ : Semiring R
k : ℕ
f : R[X]
n i : ℕ
_hi : i ∈ f.support
hink : i ≠ n + k
hik : i < k
⊢ (if i - k = n then ↑(i.choose k) * f.coeff i else 0) = 0

pp: case neg
R : Type u_1
inst✝ : Semiring R
k : ℕ
f : R[X]
n i : ℕ
_hi : i ∈ f.support
hink : i ≠ n + k
hik : ¬i < k
⊢ (if i - k = n then ↑(i.choose k) * f.coeff i else 0) = 0

Tactic:
·

Goal state after:
case pos
R : Type u_1
inst✝ : Semiring R
k : ℕ
f : R[X]
n i : ℕ
_hi : i ∈ f.support
hink : i ≠ n + k
hik : i < k
⊢ (if i - k = n then ↑(i.choose k) * f.coeff i else 0) = 0
Module: Mathlib.Algebra.Polynomial.HasseDeriv

Goal state before:
pp: case neg
R : Type u_1
inst✝ : Semiring R
k : ℕ
f : R[X]
n i : ℕ
_hi : i ∈ f.support
hink : i ≠ n + k
hik : ¬i < k
⊢ (if i - k = n then ↑(i.choose k) * f.coeff i else 0) = 0

Tactic:
·

Goal state after:
case neg
R : Type u_1
inst✝ : Semiring R
k : ℕ
f : R[X]
n i : ℕ
_hi : i ∈ f.support
hink : i ≠ n + k
hik : ¬i < k
⊢ (if i - k = n then ↑(i.choose k) * f.coeff i else 0) = 0
Module: Mathlib.Algebra.Polynomial.HasseDeriv

Goal state before:
pp: case h₁
R : Type u_1
inst✝ : Semiring R
k : ℕ
f : R[X]
n : ℕ
⊢ n + k ∉ f.support → ((monomial (n + k - k)) (↑((n + k).choose k) * f.coeff (n + k))).coeff n = 0

Tactic:
·

Goal state after:
case h₁
R : Type u_1
inst✝ : Semiring R
k : ℕ
f : R[X]
n : ℕ
⊢ n + k ∉ f.support → ((monomial (n + k - k)) (↑((n + k).choose k) * f.coeff (n + k))).coeff n = 0
Module: Mathlib.Algebra.Polynomial.HasseDeriv

Goal state before:
pp: case h₁
R : Type u_1
inst✝ : Semiring R
k : ℕ
f : R[X]
n : ℕ
h : n + k ∉ f.support
⊢ ((monomial (n + k - k)) (↑((n + k).choose k) * f.coeff (n + k))).coeff n = 0

Tactic:
simp only [notMem_support_iff.mp h, monomial_zero_right, mul_zero, coeff_zero]

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

Goal state before:
pp: case pos
R : Type u_1
inst✝ : Semiring R
k n : ℕ
r : R
i : ℕ
hnik : n = i + k
⊢ (↑((i + k).choose k) * if n = i + k then r else 0) = if n - k = i then ↑(n.choose k) * r else 0

pp: case neg
R : Type u_1
inst✝ : Semiring R
k n : ℕ
r : R
i : ℕ
hnik : ¬n = i + k
⊢ (↑((i + k).choose k) * if n = i + k then r else 0) = if n - k = i then ↑(n.choose k) * r else 0

Tactic:
·

Goal state after:
case pos
R : Type u_1
inst✝ : Semiring R
k n : ℕ
r : R
i : ℕ
hnik : n = i + k
⊢ (↑((i + k).choose k) * if n = i + k then r else 0) = if n - k = i then ↑(n.choose k) * r else 0
Module: Mathlib.Algebra.Polynomial.HasseDeriv

Goal state before:
pp: case neg
R : Type u_1
inst✝ : Semiring R
k n : ℕ
r : R
i : ℕ
hnik : ¬n = i + k
⊢ (↑((i + k).choose k) * if n = i + k then r else 0) = if n - k = i then ↑(n.choose k) * r else 0

Tactic:
·

Goal state after:
case neg
R : Type u_1
inst✝ : Semiring R
k n : ℕ
r : R
i : ℕ
hnik : ¬n = i + k
⊢ (↑((i + k).choose k) * if n = i + k then r else 0) = if n - k = i then ↑(n.choose k) * r else 0
Module: Mathlib.Algebra.Polynomial.HasseDeriv

Goal state before:
pp: case pos
R : Type u_1
inst✝ : Semiring R
k n : ℕ
r : R
i : ℕ
hnik : ¬n = i + k
hkn : k ≤ n
⊢ 0 = if n - k = i then ↑(n.choose k) * r else 0

pp: case neg
R : Type u_1
inst✝ : Semiring R
k n : ℕ
r : R
i : ℕ
hnik : ¬n = i + k
hkn : n < k
⊢ 0 = if n - k = i then ↑(n.choose k) * r else 0

Tactic:
·

Goal state after:
case pos
R : Type u_1
inst✝ : Semiring R
k n : ℕ
r : R
i : ℕ
hnik : ¬n = i + k
hkn : k ≤ n
⊢ 0 = if n - k = i then ↑(n.choose k) * r else 0
Module: Mathlib.Algebra.Polynomial.HasseDeriv

Goal state before:
pp: case pos
R : Type u_1
inst✝ : Semiring R
k n : ℕ
r : R
i : ℕ
hnik : ¬n = i + k
hkn : k ≤ n
⊢ 0 = if n - k = i then ↑(n.choose k) * r else 0

Tactic:
← tsub_eq_iff_eq_add_of_le hkn

Goal state after:
case pos
R : Type u_1
inst✝ : Semiring R
k n : ℕ
r : R
i : ℕ
hnik : ¬n - k = i
hkn : k ≤ n
⊢ 0 = if n - k = i then ↑(n.choose k) * r else 0
Module: Mathlib.Algebra.Polynomial.HasseDeriv

Goal state before:
pp: case neg
R : Type u_1
inst✝ : Semiring R
k n : ℕ
r : R
i : ℕ
hnik : ¬n = i + k
hkn : n < k
⊢ 0 = if n - k = i then ↑(n.choose k) * r else 0

Tactic:
·

Goal state after:
case neg
R : Type u_1
inst✝ : Semiring R
k n : ℕ
r : R
i : ℕ
hnik : ¬n = i + k
hkn : n < k
⊢ 0 = if n - k = i then ↑(n.choose k) * r else 0
Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff

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

pp: case inl.inr
R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
s : Finset n
e : ↥s ⊕ { a // a ∉ s } ≃ n := Equiv.sumCompl fun x ↦ x ∈ s
A : Matrix n n R := of (s.piecewise M 1)
i : ↥s
j : { a // a ∉ s }
⊢ s.piecewise M 1 ↑i ↑j = M ↑i ↑j

pp: case inr.inl
R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
s : Finset n
e : ↥s ⊕ { a // a ∉ s } ≃ n := Equiv.sumCompl fun x ↦ x ∈ s
A : Matrix n n R := of (s.piecewise M 1)
i : { a // a ∉ s }
j : ↥s
⊢ s.piecewise M 1 ↑i ↑j = 0

pp: case inr.inr
R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
s : Finset n
e : ↥s ⊕ { a // a ∉ s } ≃ n := Equiv.sumCompl fun x ↦ x ∈ s
A : Matrix n n R := of (s.piecewise M 1)
i j : { a // a ∉ s }
⊢ s.piecewise M 1 ↑i ↑j = 1 i j

Tactic:
·

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

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

pp: case inr.inl
R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
s : Finset n
e : ↥s ⊕ { a // a ∉ s } ≃ n := Equiv.sumCompl fun x ↦ x ∈ s
A : Matrix n n R := of (s.piecewise M 1)
i : { a // a ∉ s }
j : ↥s
⊢ s.piecewise M 1 ↑i ↑j = 0

pp: case inr.inr
R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
s : Finset n
e : ↥s ⊕ { a // a ∉ s } ≃ n := Equiv.sumCompl fun x ↦ x ∈ s
A : Matrix n n R := of (s.piecewise M 1)
i j : { a // a ∉ s }
⊢ s.piecewise M 1 ↑i ↑j = 1 i j

Tactic:
·

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

Goal state before:
pp: case inr.inl
R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
s : Finset n
e : ↥s ⊕ { a // a ∉ s } ≃ n := Equiv.sumCompl fun x ↦ x ∈ s
A : Matrix n n R := of (s.piecewise M 1)
i : { a // a ∉ s }
j : ↥s
⊢ s.piecewise M 1 ↑i ↑j = 0

pp: case inr.inr
R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
s : Finset n
e : ↥s ⊕ { a // a ∉ s } ≃ n := Equiv.sumCompl fun x ↦ x ∈ s
A : Matrix n n R := of (s.piecewise M 1)
i j : { a // a ∉ s }
⊢ s.piecewise M 1 ↑i ↑j = 1 i j

Tactic:
·

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

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

Tactic:
·

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

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

Tactic:
h_blocks,

Goal state after:
R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
s : Finset n
e : ↥s ⊕ { a // a ∉ s } ≃ n := Equiv.sumCompl fun x ↦ x ∈ s
A : Matrix n n R := of (s.piecewise M 1)
h_blocks :
  A.submatrix ⇑e ⇑e = fromBlocks (M.submatrix Subtype.val Subtype.val) (M.submatrix Subtype.val Subtype.val) 0 1
⊢ (fromBlocks (M.submatrix Subtype.val Subtype.val) (M.submatrix Subtype.val Subtype.val) 0 1).det =
    (M.submatrix Subtype.val Subtype.val).det
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:
·

Goal state after:
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)
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
hil : i < l
⊢ (i - l).choose k * i.choose l = 0

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

Tactic:
·

Goal state after:
case pos
R : Type u_1
inst✝ : Semiring R
k l i : ℕ
hikl : i < k + l
hil : i < l
⊢ (i - l).choose k * i.choose l = 0
Module: Mathlib.Algebra.Polynomial.HasseDeriv

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

Tactic:
·

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
p : R[X]
n : ℕ
⊢ max (if {x ∈ p.support | ↑(x.choose n) * p.coeff x = 0} = ∅ then 0 else max 0 0)
      (Finset.fold max 0 (fun x ↦ x - n) ({i ∈ p.support | ¬↑(i.choose n) * p.coeff i = 0})) ≤
    p.natDegree - n

pp: case h
R : Type u_1
inst✝ : Semiring R
p : R[X]
n : ℕ
⊢ max 0 (max 0 0) = max 0 0

Tactic:
·

Goal state after:
R : Type u_1
inst✝ : Semiring R
p : R[X]
n : ℕ
⊢ max (if {x ∈ p.support | ↑(x.choose n) * p.coeff x = 0} = ∅ then 0 else max 0 0)
      (Finset.fold max 0 (fun x ↦ x - n) ({i ∈ p.support | ¬↑(i.choose n) * p.coeff i = 0})) ≤
    p.natDegree - n
Module: Mathlib.Algebra.Polynomial.Taylor

Goal state before:
pp: case pos
R : Type u_1
inst✝ : Semiring R
r : R
n i : ℕ
h : n < i + 1
⊢ r ^ (i - n) * ↑(i.choose n) = r ^ (i - n) * ↑(i.choose n)

pp: case neg
R : Type u_1
inst✝ : Semiring R
r : R
n i : ℕ
h : ¬n < i + 1
⊢ 0 = r ^ (i - n) * ↑(i.choose n)

Tactic:
·

Goal state after:
case pos
R : Type u_1
inst✝ : Semiring R
r : R
n i : ℕ
h : n < i + 1
⊢ r ^ (i - n) * ↑(i.choose n) = r ^ (i - n) * ↑(i.choose n)
Module: Mathlib.Algebra.Polynomial.Taylor

Goal state before:
pp: case pos
R : Type u_1
inst✝ : Semiring R
r : R
f : R[X]
hf : f = 0
⊢ ((taylor r) f).coeff f.natDegree = f.leadingCoeff

pp: case neg
R : Type u_1
inst✝ : Semiring R
r : R
f : R[X]
hf : ¬f = 0
⊢ ((taylor r) f).coeff f.natDegree = f.leadingCoeff

Tactic:
·

Goal state after:
case pos
R : Type u_1
inst✝ : Semiring R
r : R
f : R[X]
hf : f = 0
⊢ ((taylor r) f).coeff f.natDegree = f.leadingCoeff
Module: Mathlib.Algebra.Polynomial.HasseDeriv

Goal state before:
pp: case h
R : Type u_1
inst✝ : Semiring R
p : R[X]
n : ℕ
⊢ max 0 (max 0 0) = max 0 0

Tactic:
·

Goal state after:
case h
R : Type u_1
inst✝ : Semiring R
p : R[X]
n : ℕ
⊢ max 0 (max 0 0) = max 0 0
Module: Mathlib.Algebra.Polynomial.Taylor

Goal state before:
pp: case neg
R : Type u_1
inst✝ : Semiring R
r : R
f : R[X]
hf : ¬f = 0
⊢ ((taylor r) f).coeff f.natDegree = f.leadingCoeff

Tactic:
·

Goal state after:
case neg
R : Type u_1
inst✝ : Semiring R
r : R
f : R[X]
hf : ¬f = 0
⊢ ((taylor r) f).coeff f.natDegree = f.leadingCoeff
Module: Mathlib.Algebra.Polynomial.Taylor

Goal state before:
pp: case pos
R : Type u_1
inst✝ : Semiring R
p : R[X]
r : R
hp : p = 0
⊢ ((taylor r) p).degree = p.degree

pp: case neg
R : Type u_1
inst✝ : Semiring R
p : R[X]
r : R
hp : ¬p = 0
⊢ ((taylor r) p).degree = p.degree

Tactic:
·

Goal state after:
case pos
R : Type u_1
inst✝ : Semiring R
p : R[X]
r : R
hp : p = 0
⊢ ((taylor r) p).degree = p.degree
Module: Mathlib.Algebra.Polynomial.Taylor

Goal state before:
pp: case neg
R : Type u_1
inst✝ : Semiring R
p : R[X]
r : R
hp : ¬p = 0
⊢ ((taylor r) p).degree = p.degree

Tactic:
·

Goal state after:
case neg
R : Type u_1
inst✝ : Semiring R
p : R[X]
r : R
hp : ¬p = 0
⊢ ((taylor r) p).degree = p.degree
Module: Mathlib.Algebra.Polynomial.Taylor

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
p : R[X]
x y t : R
⊢ ((taylor x) p).natDegree < ((taylor x) p).natDegree + 2

Tactic:
by lia

Goal state after: