mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.RootSystem.Base

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
P : RootPairing ι R M N
b : P.Base
inst✝³ : CharZero R
inst✝² : Finite ι
inst✝¹ : IsDomain R
inst✝ : P.IsCrystallographic
i : ι
hi : b.IsPos i
j k l : ι
⊢ P.root l = P.root j + P.root k →
    (∃ n f,
        range f ⊆ ↑b.support ∧ P.root j = ∑ m, P.root (f m) ∧ ∀ (m : Fin n), ∑ m' ≤ m, P.root (f m') ∈ range ⇑P.root) →
      k ∈ b.support →
        ∃ n f,
          range f ⊆ ↑b.support ∧ P.root l = ∑ m, P.root (f m) ∧ ∀ (m : Fin n), ∑ m' ≤ m, P.root (f m') ∈ range ⇑P.root

Tactic:
h₁

Goal state after:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
P : RootPairing ι R M N
b : P.Base
inst✝³ : CharZero R
inst✝² : Finite ι
inst✝¹ : IsDomain R
inst✝ : P.IsCrystallographic
i : ι
hi : b.IsPos i
j k l : ι
h₁ : P.root l = P.root j + P.root k
⊢ (∃ n f,
      range f ⊆ ↑b.support ∧ P.root j = ∑ m, P.root (f m) ∧ ∀ (m : Fin n), ∑ m' ≤ m, P.root (f m') ∈ range ⇑P.root) →
    k ∈ b.support →
      ∃ n f,
        range f ⊆ ↑b.support ∧ P.root l = ∑ m, P.root (f m) ∧ ∀ (m : Fin n), ∑ m' ≤ m, P.root (f m') ∈ range ⇑P.root
Module: Mathlib.Algebra.Order.CauSeq.Completion

Goal state before:
pp: α : Type u_1
inst✝⁵ : Field α
inst✝⁴ : LinearOrder α
inst✝³ : IsStrictOrderedRing α
β : Type u_2
inst✝² : Ring β
abv : β → α
inst✝¹ : IsAbsoluteValue abv
inst✝ : IsComplete β abv
f : CauSeq β abv
h : f.LimZero
h₁ : f = f - const abv 0
⊢ f.lim = 0

Tactic:
h₁

Goal state after:
α : Type u_1
inst✝⁵ : Field α
inst✝⁴ : LinearOrder α
inst✝³ : IsStrictOrderedRing α
β : Type u_2
inst✝² : Ring β
abv : β → α
inst✝¹ : IsAbsoluteValue abv
inst✝ : IsComplete β abv
f : CauSeq β abv
h : (f - const abv 0).LimZero
h₁ : f = f - const abv 0
⊢ f.lim = 0
Module: Mathlib.Data.Real.Basic

Goal state before:
pp: case h
x : ℝ
f y✝ : CauSeq ℚ abs
h : ∃ i, ∀ j ≥ i, mk y✝ ≤ ↑(↑f j)
K : ℚ
K0 : K > 0
hK : ∃ i, ∀ j ≥ i, K ≤ ↑(y✝ - f) j
i : ℕ
H : ∀ j ≥ i, mk y✝ ≤ ↑(↑f j) ∧ K ≤ ↑(y✝ - f) j ∧ ∀ k ≥ j, |↑f k - ↑f j| < K / 2
⊢ ↑(↑f i) < mk y✝

Tactic:
rw [← mk_const, mk_lt]

Goal state after:
case h
x : ℝ
f y✝ : CauSeq ℚ abs
h : ∃ i, ∀ j ≥ i, mk y✝ ≤ ↑(↑f j)
K : ℚ
K0 : K > 0
hK : ∃ i, ∀ j ≥ i, K ≤ ↑(y✝ - f) j
i : ℕ
H : ∀ j ≥ i, mk y✝ ≤ ↑(↑f j) ∧ K ≤ ↑(y✝ - f) j ∧ ∀ k ≥ j, |↑f k - ↑f j| < K / 2
⊢ const abs (↑f i) < y✝
Module: Mathlib.LinearAlgebra.Matrix.Hermitian

Goal state before:
pp: α : Type u_1
m : Type u_3
n : Type u_4
inst✝² : AddMonoid α
inst✝¹ : StarAddMonoid α
inst✝ : DecidableEq n
M : n → Matrix m m α
⊢ (blockDiagonal M).IsHermitian ↔ ∀ (i : n), (M i).IsHermitian

Tactic:
simpa [IsHermitian] using isHermitian_blockDiagonal'_iff

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

Goal state before:
pp: case succ.succ.inr
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
n : ℕ
IH : ∀ (m : ℕ), A⁻¹ ^ m * A ^ n = A ^ n * A⁻¹ ^ m
m : ℕ
h : A⁻¹ = 0
⊢ A⁻¹ ^ (m + 1) * A ^ (n + 1) = A ^ (n + 1) * A⁻¹ ^ (m + 1)

Tactic:
· simp [h]

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

Goal state before:
pp: n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
h : IsUnit A.det
n : ℕ
⊢ A ^ (n + 1) = (A ^ (n + 1))⁻¹⁻¹

Tactic:
nonsing_inv_nonsing_inv

Goal state after:
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
h : IsUnit A.det
n : ℕ
⊢ A ^ (n + 1) = A ^ (n + 1)

case h
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
h : IsUnit A.det
n : ℕ
⊢ IsUnit (A ^ (n + 1)).det
Module: Mathlib.LinearAlgebra.Eigenspace.Matrix

Goal state before:
pp: R : Type u_1
n : Type u_2
M : Type u_3
inst✝⁵ : DecidableEq n
inst✝⁴ : Fintype n
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
d : n → R
μ : R
b : Basis n R M
inst✝ : IsDomain R
x : M
hx : x ∈ maxGenEigenspace ((toLin b b) (diagonal d)) μ
k : ℕ
hk : ∀ (j : n), (b.repr x) j = 0 ∨ d j = μ ∧ k ≠ 0
⊢ x ∈ eigenspace ((toLin b b) (diagonal d)) μ

Tactic:
have aux (j : n) : (b.repr x j * d j) • b j = μ • (b.repr x j • b j) := by
    rcases hk j with hj | hj
    · simp [hj]
    · rw [← hj.1, mul_comm, mul_smul]

Goal state after:
R : Type u_1
n : Type u_2
M : Type u_3
inst✝⁵ : DecidableEq n
inst✝⁴ : Fintype n
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
d : n → R
μ : R
b : Basis n R M
inst✝ : IsDomain R
x : M
hx : x ∈ maxGenEigenspace ((toLin b b) (diagonal d)) μ
k : ℕ
hk : ∀ (j : n), (b.repr x) j = 0 ∨ d j = μ ∧ k ≠ 0
aux : ∀ (j : n), ((b.repr x) j * d j) • b j = μ • (b.repr x) j • b j
⊢ x ∈ eigenspace ((toLin b b) (diagonal d)) μ
Module: Mathlib.LinearAlgebra.Matrix.ZPow

Goal state before:
pp: n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
h : IsUnit A.det
m n : ℕ
⊢ A ^ (m.succ * n.succ) = (A ^ ((m + 1) * (n + 1)))⁻¹⁻¹

Tactic:
nonsing_inv_nonsing_inv

Goal state after:
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
h : IsUnit A.det
m n : ℕ
⊢ A ^ (m.succ * n.succ) = A ^ ((m + 1) * (n + 1))

case h
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
h : IsUnit A.det
m n : ℕ
⊢ IsUnit (A ^ ((m + 1) * (n + 1))).det
Module: Mathlib.LinearAlgebra.Matrix.PosDef

Goal state before:
pp: n : Type u_2
R : Type u_3
inst✝² : Ring R
inst✝¹ : PartialOrder R
inst✝ : StarRing R
A : Matrix n n R
hA : A.PosSemidef
i : n
⊢ 0 ≤ A i i

Tactic:
simpa using hA.2 <| .single i 1

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

Goal state before:
pp: case mp
m : Type u_1
n : Type u_2
R' : Type u_4
inst✝⁷ : CommRing R'
inst✝⁶ : PartialOrder R'
inst✝⁵ : StarRing R'
inst✝⁴ : Fintype m
inst✝³ : StarOrderedRing R'
inst✝² : Finite n
inst✝¹ : DecidableEq m
A : Matrix m m R'
B : Matrix m n R'
D : Matrix n n R'
hA : A.PosDef
inst✝ : Invertible A
this✝ : Fintype n
h : (D - Bᴴ * A⁻¹ * B).IsHermitian ∧ ∀ (x : m ⊕ n → R'), 0 ≤ star x ⬝ᵥ fromBlocks A B Bᴴ D *ᵥ x
x : n → R'
this : 0 ≤ star (-((A⁻¹ * B) *ᵥ x) ⊕ᵥ x) ᵥ* fromBlocks A B Bᴴ D ⬝ᵥ (-((A⁻¹ * B) *ᵥ x) ⊕ᵥ x)
⊢ 0 ≤ star x ⬝ᵥ (D - Bᴴ * A⁻¹ * B) *ᵥ x

Tactic:
schur_complement_eq₁₁ B D _ _ hA.1,

Goal state after:
case mp
m : Type u_1
n : Type u_2
R' : Type u_4
inst✝⁷ : CommRing R'
inst✝⁶ : PartialOrder R'
inst✝⁵ : StarRing R'
inst✝⁴ : Fintype m
inst✝³ : StarOrderedRing R'
inst✝² : Finite n
inst✝¹ : DecidableEq m
A : Matrix m m R'
B : Matrix m n R'
D : Matrix n n R'
hA : A.PosDef
inst✝ : Invertible A
this✝ : Fintype n
h : (D - Bᴴ * A⁻¹ * B).IsHermitian ∧ ∀ (x : m ⊕ n → R'), 0 ≤ star x ⬝ᵥ fromBlocks A B Bᴴ D *ᵥ x
x : n → R'
this :
  0 ≤
    star (-((A⁻¹ * B) *ᵥ x) + (A⁻¹ * B) *ᵥ x) ᵥ* A ⬝ᵥ (-((A⁻¹ * B) *ᵥ x) + (A⁻¹ * B) *ᵥ x) +
      star x ᵥ* (D - Bᴴ * A⁻¹ * B) ⬝ᵥ x
⊢ 0 ≤ star x ⬝ᵥ (D - Bᴴ * A⁻¹ * B) *ᵥ x
Module: Mathlib.LinearAlgebra.RootSystem.CartanMatrix

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝¹⁰ : CommRing R
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module R M
inst✝⁷ : AddCommGroup N
inst✝⁶ : Module R N
P : RootPairing ι R M N
b : P.Base
inst✝⁵ : P.IsCrystallographic
inst✝⁴ : CharZero R
inst✝³ : IsDomain R
inst✝² : Finite ι
inst✝¹ : P.IsReduced
inst✝ : P.IsIrreducible
p : ↥b.support → Prop
i j : ↥b.support
hi : p i
hp : ∀ (i j : ↥b.support), p i → b.cartanMatrix j i ≠ 0 → p j
⊢ p j

Tactic:
let q : Submodule R M := span R (P.root ∘ (↑) '' {i | p i})

Goal state after:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝¹⁰ : CommRing R
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module R M
inst✝⁷ : AddCommGroup N
inst✝⁶ : Module R N
P : RootPairing ι R M N
b : P.Base
inst✝⁵ : P.IsCrystallographic
inst✝⁴ : CharZero R
inst✝³ : IsDomain R
inst✝² : Finite ι
inst✝¹ : P.IsReduced
inst✝ : P.IsIrreducible
p : ↥b.support → Prop
i j : ↥b.support
hi : p i
hp : ∀ (i j : ↥b.support), p i → b.cartanMatrix j i ≠ 0 → p j
q : Submodule R M := span R (⇑P.root ∘ Subtype.val '' {i | p i})
⊢ p j
Module: Mathlib.LinearAlgebra.Eigenspace.Minpoly

Goal state before:
pp: case refine_2
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ : R
x : M
p✝ : R[X]
h : f.HasEigenvector μ x
p q : R[X]
⊢ ((aeval f) p) x = eval μ p • x → ((aeval f) q) x = eval μ q • x → ((aeval f) (p + q)) x = eval μ (p + q) • x

Tactic:
hp

Goal state after:
case refine_2
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ : R
x : M
p✝ : R[X]
h : f.HasEigenvector μ x
p q : R[X]
hp : ((aeval f) p) x = eval μ p • x
⊢ ((aeval f) q) x = eval μ q • x → ((aeval f) (p + q)) x = eval μ (p + q) • x
Module: Mathlib.LinearAlgebra.Vandermonde

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
n : ℕ
v0 : R
v : Fin n → R
i✝ j : Fin (n + 1)
i : Fin n
⊢ vandermonde (Fin.cons v0 v) i.succ j =
    Fin.cons (fun j ↦ v0 ^ ↑j) (fun i ↦ Fin.cons 1 fun j ↦ v i * vandermonde v i j) i.succ j

Tactic:
refine Fin.cases (by simp) (fun j => ?_) j

Goal state after:
R : Type u_1
inst✝ : CommRing R
n : ℕ
v0 : R
v : Fin n → R
i✝ j✝ : Fin (n + 1)
i j : Fin n
⊢ vandermonde (Fin.cons v0 v) i.succ j.succ =
    Fin.cons (fun j ↦ v0 ^ ↑j) (fun i ↦ Fin.cons 1 fun j ↦ v i * vandermonde v i j) i.succ j.succ
Module: Mathlib.Algebra.Lie.Basis.Prod

Goal state before:
pp: ι₁ : Type u_1
ι₂ : Type u_2
L₁ : Type u_3
L₂ : Type u_4
inst✝⁶ : Finite ι₁
inst✝⁵ : Finite ι₂
eι : ι₁ ≃ ι₂
inst✝⁴ : LieRing L₁
inst✝³ : LieRing L₂
R : Type u_5
inst✝² : CommRing R
inst✝¹ : LieAlgebra R L₁
H₁ : LieSubalgebra R L₁
b₁ : Basis ι₁ H₁
inst✝ : LieAlgebra R L₂
H₂ : LieSubalgebra R L₂
b₂ : Basis ι₂ H₂
this : ∀ (y : L₂), (∃ l, (linearCombination R fun i ↦ (b₁.h i, b₂.h (eι i))) l = (0, y)) → y = 0
aux : {x | ∃ i, (b₁.h i, b₂.h (eι i)) = x} = (fun i ↦ (b₁.h i, b₂.h (eι i))) '' univ
⊢ InjOn ⇑(LinearMap.fst R L₁ L₂) ↑(span R {x | ∃ i, (b₁.h i, b₂.h (eι i)) = x})

Tactic:
simp_rw [← LinearMap.disjoint_ker_iff_injOn, LinearMap.disjoint_ker, aux,
      mem_span_image_iff_linearCombination]

Goal state after:
ι₁ : Type u_1
ι₂ : Type u_2
L₁ : Type u_3
L₂ : Type u_4
inst✝⁶ : Finite ι₁
inst✝⁵ : Finite ι₂
eι : ι₁ ≃ ι₂
inst✝⁴ : LieRing L₁
inst✝³ : LieRing L₂
R : Type u_5
inst✝² : CommRing R
inst✝¹ : LieAlgebra R L₁
H₁ : LieSubalgebra R L₁
b₁ : Basis ι₁ H₁
inst✝ : LieAlgebra R L₂
H₂ : LieSubalgebra R L₂
b₂ : Basis ι₂ H₂
this : ∀ (y : L₂), (∃ l, (linearCombination R fun i ↦ (b₁.h i, b₂.h (eι i))) l = (0, y)) → y = 0
aux : {x | ∃ i, (b₁.h i, b₂.h (eι i)) = x} = (fun i ↦ (b₁.h i, b₂.h (eι i))) '' univ
⊢ ∀ (x : L₁ × L₂),
    (∃ l ∈ supported R R univ, (linearCombination R fun i ↦ (b₁.h i, b₂.h (eι i))) l = x) →
      (LinearMap.fst R L₁ L₂) x = 0 → x = 0
Module: Mathlib.LinearAlgebra.Vandermonde

Goal state before:
pp: case mpr
R : Type u_1
inst✝¹ : CommRing R
n : ℕ
inst✝ : IsDomain R
v : Fin n → R
i j : Fin n
h₁ : v i = v j
h₂ : ¬i = j
k : Fin n
⊢ v i ^ ↑k = v j ^ ↑k

Tactic:
h₁

Goal state after:
case mpr
R : Type u_1
inst✝¹ : CommRing R
n : ℕ
inst✝ : IsDomain R
v : Fin n → R
i j : Fin n
h₁ : v i = v j
h₂ : ¬i = j
k : Fin n
⊢ v j ^ ↑k = v j ^ ↑k
Module: Mathlib.LinearAlgebra.Lagrange

Goal state before:
pp: case pos
F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s t : Finset ι
v r : ι → F
hvt : Set.InjOn v ↑t
hs : s.Nonempty
hst : s ⊆ t
i : ι
hi : i ∈ t
hi' : i ∈ s
⊢ eval (v i) ((interpolate (insert i (t \ s)) v) r) * 1 +
      ∑ x ∈ s.erase i, eval (v i) ((interpolate (insert x (t \ s)) v) r) * eval (v i) (Lagrange.basis s v x) =
    r i

Tactic:
eval_interpolate_at_node _
          (hvt.mono (coe_subset.mpr (insert_subset_iff.mpr ⟨hi, sdiff_subset⟩)))
          (mem_insert_self _ _),

Goal state after:
case pos
F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s t : Finset ι
v r : ι → F
hvt : Set.InjOn v ↑t
hs : s.Nonempty
hst : s ⊆ t
i : ι
hi : i ∈ t
hi' : i ∈ s
⊢ r i * 1 + ∑ x ∈ s.erase i, eval (v i) ((interpolate (insert x (t \ s)) v) r) * eval (v i) (Lagrange.basis s v x) = r i
Module: Mathlib.LinearAlgebra.Lagrange

Goal state before:
pp: F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s : Finset ι
v : ι → F
hvs : Set.InjOn v ↑s
P : F[X]
hP : P.degree < ↑(#s)
k : ℕ
hk : k < #s
x : F
⊢ eval x ((⇑derivative)^[k] P) =
    ↑k.factorial *
      ∑ i ∈ s,
        (eval (v i) P / ∏ j ∈ s.erase i, (v i - v j)) *
          ∑ t ∈ powersetCard (#s - (k + 1)) (s.erase i), ∏ a ∈ t, (x - v a)

Tactic:
eq_interpolate hvs hP,

Goal state after:
F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s : Finset ι
v : ι → F
hvs : Set.InjOn v ↑s
P : F[X]
hP : P.degree < ↑(#s)
k : ℕ
hk : k < #s
x : F
⊢ eval x ((⇑derivative)^[k] ((interpolate s v) fun i ↦ eval (v i) P)) =
    ↑k.factorial *
      ∑ i ∈ s,
        (eval (v i) P / ∏ j ∈ s.erase i, (v i - v j)) *
          ∑ t ∈ powersetCard (#s - (k + 1)) (s.erase i), ∏ a ∈ t, (x - v a)
Module: Mathlib.LinearAlgebra.Lagrange

Goal state before:
pp: F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s : Finset ι
v : ι → F
hvs : Set.InjOn v ↑s
P : F[X]
hP : P.degree < ↑(#s)
⊢ P.coeff (#s - 1) = ∑ i ∈ s, eval (v i) P / ∏ j ∈ s.erase i, (v i - v j)

Tactic:
eq_interpolate hvs hP,

Goal state after:
F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s : Finset ι
v : ι → F
hvs : Set.InjOn v ↑s
P : F[X]
hP : P.degree < ↑(#s)
⊢ ((interpolate s v) fun i ↦ eval (v i) P).coeff (#s - 1) = ∑ i ∈ s, eval (v i) P / ∏ j ∈ s.erase i, (v i - v j)
Module: Mathlib.LinearAlgebra.Lagrange

Goal state before:
pp: F : Type u_1
inst✝¹ : Field F
ι : Type u_3
inst✝ : Finite ι
x y : ι → F
⊢ (∃ q, ∀ (i : ι), eval (x i) q = y i) ↔ ∀ (i j : ι), x i = x j → y i = y j

Tactic:
refine ⟨fun ⟨q, hq⟩ i j hij ↦ by rw [← hq, ← hq, hij], fun hwd ↦ ?_⟩
  classical
  have : Fintype ι := Fintype.ofFinite ι
  have hinj : Set.InjOn (fun d : F ↦ d) (Finset.univ.image x) := Function.injective_id.injOn
  set v : F → F := fun z ↦ if h : ∃ i, x i = z then y h.choose else 0 with v_def
  refine ⟨Lagrange.interpolate (Finset.univ.image x) (fun d : F ↦ d) v, fun i ↦ ?_⟩
  rw [Lagrange.eval_interpolate_at_node _ hinj (by simp), v_def]
  simp only
  split_ifs with h
  · exact hwd _ _ h.choose_spec
  · aesop

Goal state after:
Module: Mathlib.LinearAlgebra.Charpoly.Basic

Goal state before:
pp: R : Type u
M : Type v
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : Free R M
inst✝¹ : Module.Finite R M
f : M →ₗ[R] M
inst✝ : StrongRankCondition R
⊢ f.charpoly.natDegree = finrank R M

Tactic:
by
  have := nontrivial_of_invariantBasisNumber
  rw [charpoly, Matrix.charpoly_natDegree_eq_dim, finrank_eq_card_chooseBasisIndex]

Goal state after:
Module: Mathlib.LinearAlgebra.Charpoly.ToMatrix

Goal state before:
pp: R : Type u_1
M₁ : Type u_3
M₂ : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M₁
inst✝⁶ : Module R M₁
inst✝⁵ : Module.Finite R M₁
inst✝⁴ : Free R M₁
inst✝³ : AddCommGroup M₂
inst✝² : Module R M₂
inst✝¹ : Module.Finite R M₂
inst✝ : Free R M₂
e : M₁ ≃ₗ[R] M₂
φ : End R M₁
b : Basis (ChooseBasisIndex R M₁) R M₁ := chooseBasis R M₁
⊢ LinearMap.charpoly (e.conj φ) = LinearMap.charpoly φ

Tactic:
rw [← LinearMap.charpoly_toMatrix φ b, ← LinearMap.charpoly_toMatrix (e.conj φ) (b.map e)]

Goal state after:
R : Type u_1
M₁ : Type u_3
M₂ : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M₁
inst✝⁶ : Module R M₁
inst✝⁵ : Module.Finite R M₁
inst✝⁴ : Free R M₁
inst✝³ : AddCommGroup M₂
inst✝² : Module R M₂
inst✝¹ : Module.Finite R M₂
inst✝ : Free R M₂
e : M₁ ≃ₗ[R] M₂
φ : End R M₁
b : Basis (ChooseBasisIndex R M₁) R M₁ := chooseBasis R M₁
⊢ ((LinearMap.toMatrix (b.map e) (b.map e)) (e.conj φ)).charpoly = ((LinearMap.toMatrix b b) φ).charpoly
Module: Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal

Goal state before:
pp: ι : Type u_1
σ : Type u_2
A : Type u_3
inst✝⁵ : Semiring A
inst✝⁴ : DecidableEq ι
inst✝³ : AddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
I J : Ideal A
HI : IsHomogeneous 𝒜 I
HJ : IsHomogeneous 𝒜 J
⊢ IsHomogeneous 𝒜 (I ⊔ J)

Tactic:
rw [iff_exists] at HI HJ ⊢

Goal state after:
ι : Type u_1
σ : Type u_2
A : Type u_3
inst✝⁵ : Semiring A
inst✝⁴ : DecidableEq ι
inst✝³ : AddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
I J : Ideal A
HI : ∃ S, I = span (Subtype.val '' S)
HJ : ∃ S, J = span (Subtype.val '' S)
⊢ ∃ S, I ⊔ J = span (Subtype.val '' S)
Module: Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal

Goal state before:
pp: case pos
ι : Type u_1
σ : Type u_2
A : Type u_3
inst✝⁷ : Semiring A
inst✝⁶ : DecidableEq ι
inst✝⁵ : AddCommMonoid ι
inst✝⁴ : PartialOrder ι
inst✝³ : CanonicallyOrderedAdd ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
i : ι
r : A
hr : ↑(((decompose 𝒜) r) 0) = 0
h : i = 0
⊢ ↑(0 0) = 0

Tactic:
zero_apply,

Goal state after:
case pos
ι : Type u_1
σ : Type u_2
A : Type u_3
inst✝⁷ : Semiring A
inst✝⁶ : DecidableEq ι
inst✝⁵ : AddCommMonoid ι
inst✝⁴ : PartialOrder ι
inst✝³ : CanonicallyOrderedAdd ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
i : ι
r : A
hr : ↑(((decompose 𝒜) r) 0) = 0
h : i = 0
⊢ ↑0 = 0
Module: Mathlib.LinearAlgebra.Eigenspace.Zero

Goal state before:
pp: case h
R : Type u_1
M : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : IsDomain R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : Module.Finite R M
inst✝¹ : Free R M
inst✝ : IsNoetherian R M
φ : End R M
tfae_1_to_2 : IsNilpotent φ → charpoly φ = X ^ finrank R M
tfae_2_to_3 : charpoly φ = X ^ finrank R M → ∀ (m : M), ∃ n, (φ ^ n) m = 0
x✝ : ∀ (m : M), ∃ n, (φ ^ n) m = 0
h : ∀ (m : M), ∃ n, (φ ^ n) m = 0 := x✝
n : ℕ
hn : ∀ (b : ℕ), n ≤ b → ⨆ m, (φ ^ m).ker = (φ ^ b).ker
x : M
⊢ (φ ^ n) x = 0 x

Tactic:
zero_apply,

Goal state after:
case h
R : Type u_1
M : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : IsDomain R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : Module.Finite R M
inst✝¹ : Free R M
inst✝ : IsNoetherian R M
φ : End R M
tfae_1_to_2 : IsNilpotent φ → charpoly φ = X ^ finrank R M
tfae_2_to_3 : charpoly φ = X ^ finrank R M → ∀ (m : M), ∃ n, (φ ^ n) m = 0
x✝ : ∀ (m : M), ∃ n, (φ ^ n) m = 0
h : ∀ (m : M), ∃ n, (φ ^ n) m = 0 := x✝
n : ℕ
hn : ∀ (b : ℕ), n ≤ b → ⨆ m, (φ ^ m).ker = (φ ^ b).ker
x : M
⊢ (φ ^ n) x = 0
Module: Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous

Goal state before:
pp: case neg
R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
σ : Type u_3
inst✝ : AddCommMonoid M
w : σ → M
m n : M
p : MvPolynomial σ R
hp : IsWeightedHomogeneous w p m
hn : n ≠ m
x : σ →₀ ℕ
zero_coeff : ¬coeff x p = 0
⊢ 0 = coeff x 0

Tactic:
rw [coeff_zero]

Goal state after:
Module: Mathlib.RingTheory.MvPolynomial.Homogeneous

Goal state before:
pp: case h
R : Type u_3
inst✝ : CommSemiring R
N : ℕ
F : MvPolynomial (Fin N.succ) R
n : ℕ
hF : F.IsHomogeneous n
hF₀ : F ≠ 0
hdeg : ((finSuccEquiv R N) F).natDegree < n + 1
aux : ∀ i ∈ Finset.range n, constantCoeff (((finSuccEquiv R N) F).coeff i) = 0
hFn : constantCoeff (((finSuccEquiv R N) F).coeff n) = 0
d : Fin N →₀ ℕ
⊢ coeff d (((finSuccEquiv R N) F).coeff n) = coeff d 0

Tactic:
rw [coeff_zero]

Goal state after:
case h
R : Type u_3
inst✝ : CommSemiring R
N : ℕ
F : MvPolynomial (Fin N.succ) R
n : ℕ
hF : F.IsHomogeneous n
hF₀ : F ≠ 0
hdeg : ((finSuccEquiv R N) F).natDegree < n + 1
aux : ∀ i ∈ Finset.range n, constantCoeff (((finSuccEquiv R N) F).coeff i) = 0
hFn : constantCoeff (((finSuccEquiv R N) F).coeff n) = 0
d : Fin N →₀ ℕ
⊢ coeff d (((finSuccEquiv R N) F).coeff n) = 0
Module: Mathlib.LinearAlgebra.Eigenspace.Zero

Goal state before:
pp: K : Type u_2
M : Type u_3
inst✝³ : Field K
inst✝² : AddCommGroup M
inst✝¹ : Module K M
inst✝ : Module.Finite K M
φ : End K M
this :
  [¬φ.HasEigenvalue 0, ¬(minpoly K φ).IsRoot 0, constantCoeff (charpoly φ) ≠ 0, LinearMap.det φ ≠ 0, ¬⊥ < ker φ,
      ∀ (m : M), m ≠ 0 → φ m ≠ 0].TFAE
aux₁ : ∀ (m : M), m ≠ 0 → φ m ≠ 0 ↔ φ m = 0 → m = 0
⊢ ker φ = ⊥ ↔ ¬ker φ ≠ ⊥

Tactic:
not_not

Goal state after:
K : Type u_2
M : Type u_3
inst✝³ : Field K
inst✝² : AddCommGroup M
inst✝¹ : Module K M
inst✝ : Module.Finite K M
φ : End K M
this :
  [¬φ.HasEigenvalue 0, ¬(minpoly K φ).IsRoot 0, constantCoeff (charpoly φ) ≠ 0, LinearMap.det φ ≠ 0, ¬⊥ < ker φ,
      ∀ (m : M), m ≠ 0 → φ m ≠ 0].TFAE
aux₁ : ∀ (m : M), m ≠ 0 → φ m ≠ 0 ↔ φ m = 0 → m = 0
⊢ ker φ = ⊥ ↔ ker φ = ⊥
Module: Mathlib.Algebra.Module.LinearMap.Polynomial

Goal state before:
pp: R : Type u_1
L : Type u_2
M : Type u_3
ι : Type u_5
ιM : Type u_7
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup L
inst✝⁶ : Module R L
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
φ : L →ₗ[R] End R M
inst✝³ : Fintype ι
inst✝² : Fintype ιM
inst✝¹ : DecidableEq ι
inst✝ : DecidableEq ιM
b : Basis ι R L
bₘ : Basis ιM R M
x : L
⊢ Polynomial.map (eval₂Hom ((eval ⇑(b.repr x)).comp C) fun i ↦ (eval ⇑(b.repr x)) (toMvPolynomial b bₘ.end φ i))
      (charpoly.univ R ιM) =
    ((toMatrix bₘ bₘ) (φ x)).charpoly

Tactic:
charpoly.univ_map_eval₂Hom

Goal state after:
R : Type u_1
L : Type u_2
M : Type u_3
ι : Type u_5
ιM : Type u_7
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup L
inst✝⁶ : Module R L
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
φ : L →ₗ[R] End R M
inst✝³ : Fintype ι
inst✝² : Fintype ιM
inst✝¹ : DecidableEq ι
inst✝ : DecidableEq ιM
b : Basis ι R L
bₘ : Basis ιM R M
x : L
⊢ (of (Function.curry fun i ↦ (eval ⇑(b.repr x)) (toMvPolynomial b bₘ.end φ i))).charpoly =
    ((toMatrix bₘ bₘ) (φ x)).charpoly
Module: Mathlib.Algebra.Lie.Character

Goal state before:
pp: case add
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
χ : LieCharacter R L
x y z : L
hx✝ : y ∈ Submodule.span R {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x}
hy✝ : z ∈ Submodule.span R {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x}
hy : χ y = 0
hz : χ z = 0
⊢ χ (y + z) = 0

Tactic:
rw [map_add, hy, hz, add_zero]

Goal state after:
Module: Mathlib.Algebra.Lie.SkewAdjoint

Goal state before:
pp: case mpr
R : Type u
n : Type w
inst✝² : CommRing R
inst✝¹ : Fintype n
inst✝ : DecidableEq n
u : Rˣ
J A : Matrix n n R
h : Aᵀ * J = J * -A
⊢ Aᵀ * u • J = u • J * -A

Tactic:
· simp [h]

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

Goal state before:
pp: m : Type u_1
inst✝³ : Fintype m
K : Type u
inst✝² : Field K
inst✝¹ : DecidableEq m
inst✝ : DecidableEq K
w : m → K
hIJ : IsCompl {i | w i ≠ 0} {i | w i = 0}
B₁ : ⨆ i ∈ {i | w i ≠ 0}, (single K (fun x ↦ K) i).range = ⨅ i ∈ {i | w i = 0}, (proj i).ker
⊢ Module.rank K ↥(toLin' (Matrix.diagonal w)).range = ↑(Fintype.card { i // w i ≠ 0 })

Tactic:
range_diagonal,

Goal state after:
m : Type u_1
inst✝³ : Fintype m
K : Type u
inst✝² : Field K
inst✝¹ : DecidableEq m
inst✝ : DecidableEq K
w : m → K
hIJ : IsCompl {i | w i ≠ 0} {i | w i = 0}
B₁ : ⨆ i ∈ {i | w i ≠ 0}, (single K (fun x ↦ K) i).range = ⨅ i ∈ {i | w i = 0}, (proj i).ker
⊢ Module.rank K ↥(⨆ i ∈ {i | w i ≠ 0}, (single K (fun x ↦ K) i).range) = ↑(Fintype.card { i // w i ≠ 0 })
Module: Mathlib.Algebra.Lie.Classical

Goal state before:
pp: case inr.inr
p : Type u_2
q : Type u_3
R : Type u₂
inst✝⁴ : DecidableEq p
inst✝³ : DecidableEq q
inst✝² : CommRing R
inst✝¹ : Fintype p
inst✝ : Fintype q
i : R
hi : i * i = -1
x y : q
⊢ (Pso p q R i * Pso p q R (-i)) (Sum.inr x) (Sum.inr y) = 1 (Sum.inr x) (Sum.inr y)

Tactic:
· -- x y : q
    by_cases h : x = y <;>
    simp [Pso, h, hi, one_apply]

Goal state after:
Module: Mathlib.RingTheory.Derivation.Lie

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
A : Type u_2
inst✝¹ : CommRing A
inst✝ : Algebra R A
D1 D2 : Derivation R A A
a : A
d e f : Derivation R A A
⊢ ⁅d, ⁅e, f⁆⁆ = ⁅⁅d, e⁆, f⁆ + ⁅e, ⁅d, f⁆⁆

Tactic:
ext a; simp only [commutator_apply, add_apply, map_sub]; ring

Goal state after: