mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Matrix.Spectrum

Goal state before:
pp: case mp
𝕜 : Type u_1
inst✝² : RCLike 𝕜
n : Type u_2
inst✝¹ : Fintype n
A B : Matrix n n 𝕜
inst✝ : DecidableEq n
hA : A.IsHermitian
hB : B.IsHermitian
h : hA.eigenvalues = hB.eigenvalues
⊢ ∏ i, (Polynomial.X - Polynomial.C ↑(hB.eigenvalues i)) = ∏ i, (Polynomial.X - Polynomial.C ↑(hB.eigenvalues i))

Tactic:
]

Goal state after:
Module: Mathlib.Analysis.Matrix.Spectrum

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : RCLike 𝕜
n : Type u_2
inst✝¹ : Fintype n
A B : Matrix n n 𝕜
inst✝ : DecidableEq n
hA : A.IsHermitian
hB : B.IsHermitian
h : A.charpoly = B.charpoly
this : hA.eigenvalues₀ = hB.eigenvalues₀
⊢ (fun i ↦ hB.eigenvalues₀ ((Fintype.equivOfCardEq ⋯).symm i)) = fun i ↦
    hB.eigenvalues₀ ((Fintype.equivOfCardEq ⋯).symm i)

Tactic:
]

Goal state after:
Module: Mathlib.Analysis.Normed.Operator.Compact.FredholmAlternative

Goal state before:
pp: case mp
𝕜 : Type u_1
X : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedAddCommGroup X
inst✝¹ : NormedSpace 𝕜 X
T : X →L[𝕜] X
μ : 𝕜
inst✝ : CompleteSpace X
hT : IsCompactOperator ⇑T
hμ : μ ≠ 0
hμ' : HasEigenvalue (↑T) μ
⊢ μ ∈ spectrum 𝕜 ↑T

Tactic:
]

Goal state after:
case mp
𝕜 : Type u_1
X : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedAddCommGroup X
inst✝¹ : NormedSpace 𝕜 X
T : X →L[𝕜] X
μ : 𝕜
inst✝ : CompleteSpace X
hT : IsCompactOperator ⇑T
hμ : μ ≠ 0
hμ' : HasEigenvalue (↑T) μ
⊢ μ ∈ spectrum 𝕜 ↑T
Module: Mathlib.Analysis.Matrix.Spectrum

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : RCLike 𝕜
n : Type u_2
inst✝¹ : Fintype n
A : Matrix n n 𝕜
inst✝ : DecidableEq n
hA : A.IsHermitian
⊢ Fintype.card { i // hA.eigenvalues i ≠ 0 } = Fintype.card { i // hA.eigenvalues i ≠ 0 }

Tactic:
]

Goal state after:
Module: Mathlib.Analysis.Matrix.HermitianFunctionalCalculus

Goal state before:
pp: n : Type u_1
𝕜 : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n 𝕜
hA : A.IsHermitian
r : ℝ
⊢ (↑hA.eigenvectorUnitary * diagonal fun x ↦ ↑r) * star ↑hA.eigenvectorUnitary =
    ↑hA.eigenvectorUnitary * (algebraMap ℝ (Matrix n n 𝕜)) r * star ↑hA.eigenvectorUnitary

Tactic:
]

Goal state after:
n : Type u_1
𝕜 : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n 𝕜
hA : A.IsHermitian
r : ℝ
⊢ (↑hA.eigenvectorUnitary * diagonal fun x ↦ ↑r) * star ↑hA.eigenvectorUnitary =
    ↑hA.eigenvectorUnitary * (algebraMap ℝ (Matrix n n 𝕜)) r * star ↑hA.eigenvectorUnitary
Module: Mathlib.Analysis.Matrix.Spectrum

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : RCLike 𝕜
n : Type u_2
inst✝¹ : Fintype n
A : Matrix n n 𝕜
inst✝ : DecidableEq n
hA : A.IsHermitian
h : hA.eigenvalues = 0
⊢ 0 = 0

Tactic:
]

Goal state after:
Module: Mathlib.Analysis.Matrix.Spectrum

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹ : RCLike 𝕜
n : Type u_2
inst✝ : Fintype n
A : Matrix n n 𝕜
hA : A.IsHermitian
h_ne : hA.eigenvalues = 0
this : A = 0
⊢ A = 0

Tactic:
]

Goal state after:
𝕜 : Type u_1
inst✝¹ : RCLike 𝕜
n : Type u_2
inst✝ : Fintype n
A : Matrix n n 𝕜
hA : A.IsHermitian
h_ne : hA.eigenvalues = 0
this : A = 0
⊢ A = 0
Module: Mathlib.Analysis.InnerProductSpace.Spectrum

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : RCLike 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
hT : T.IsSymmetric
μ : 𝕜
v : E
hv : v ∈ (eigenspace T μ)ᗮ
w : E
hw : T w = μ • w
⊢ T w = μ • w

Tactic:
]

Goal state after:
𝕜 : Type u_1
inst✝² : RCLike 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
hT : T.IsSymmetric
μ : 𝕜
v : E
hv : v ∈ (eigenspace T μ)ᗮ
w : E
hw : T w = μ • w
⊢ T w = μ • w
Module: Mathlib.Analysis.Matrix.HermitianFunctionalCalculus

Goal state before:
pp: n : Type u_1
𝕜 : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n 𝕜
hA : A.IsHermitian
h0 : FiniteDimensional ℝ C(↑(spectrum ℝ A), ℝ)
f : C(↑(spectrum ℝ A), ℝ)
hf : ↑hA.cfcAux f = 0
h2 : diagonal (RCLike.ofReal ∘ ⇑f ∘ fun i ↦ ⟨hA.eigenvalues i, ⋯⟩) = diagonal fun x ↦ 0
i : n
hx : hA.eigenvalues i ∈ spectrum ℝ A
⊢ f ⟨hA.eigenvalues i, hx⟩ = 0

Tactic:
]

Goal state after:
n : Type u_1
𝕜 : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n 𝕜
hA : A.IsHermitian
h0 : FiniteDimensional ℝ C(↑(spectrum ℝ A), ℝ)
f : C(↑(spectrum ℝ A), ℝ)
hf : ↑hA.cfcAux f = 0
h2 : diagonal (RCLike.ofReal ∘ ⇑f ∘ fun i ↦ ⟨hA.eigenvalues i, ⋯⟩) = diagonal fun x ↦ 0
i : n
hx : hA.eigenvalues i ∈ spectrum ℝ A
⊢ f ⟨hA.eigenvalues i, hx⟩ = 0
Module: Mathlib.Analysis.InnerProductSpace.Spectrum

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : RCLike 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
hT : T.IsSymmetric
μ : 𝕜
hμ : HasEigenvalue T μ
v : E
hv₁ : T v = μ • v
hv₂ : v ≠ 0
⊢ (starRingEnd 𝕜) μ = μ

Tactic:
]

Goal state after:
𝕜 : Type u_1
inst✝² : RCLike 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
hT : T.IsSymmetric
μ : 𝕜
hμ : HasEigenvalue T μ
v : E
hv₁ : T v = μ • v
hv₂ : v ≠ 0
⊢ (starRingEnd 𝕜) μ = μ
Module: Mathlib.Analysis.InnerProductSpace.Spectrum

Goal state before:
pp: case neg
𝕜 : Type u_1
inst✝² : RCLike 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
hT : T.IsSymmetric
μ ν : 𝕜
hμν : μ ≠ ν
v : E
hv✝ : v ∈ eigenspace T μ
hv : T v = μ • v
w : E
hw✝ : w ∈ eigenspace T ν
hw : T w = ν • w
hv' : ¬v = 0
H : (starRingEnd 𝕜) μ = μ
⊢ ⟪((fun μ ↦ (eigenspace T μ).subtypeₗᵢ) μ) ⟨v, hv✝⟩, ((fun μ ↦ (eigenspace T μ).subtypeₗᵢ) ν) ⟨w, hw✝⟩⟫ = 0

Tactic:
]

Goal state after:
case neg
𝕜 : Type u_1
inst✝² : RCLike 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
hT : T.IsSymmetric
μ ν : 𝕜
hμν : μ ≠ ν
v : E
hv✝ : v ∈ eigenspace T μ
hv : T v = μ • v
w : E
hw✝ : w ∈ eigenspace T ν
hw : T w = ν • w
hv' : ¬v = 0
H : (starRingEnd 𝕜) μ = μ
⊢ ⟪((fun μ ↦ (eigenspace T μ).subtypeₗᵢ) μ) ⟨v, hv✝⟩, ((fun μ ↦ (eigenspace T μ).subtypeₗᵢ) ν) ⟨w, hw✝⟩⟫ = 0
Module: Mathlib.Analysis.Matrix.PosDef

Goal state before:
pp: n : Type u_2
𝕜 : Type u_3
inst✝² : Fintype n
inst✝¹ : RCLike 𝕜
A : Matrix n n 𝕜
inst✝ : DecidableEq n
hA : A.PosSemidef
⊢ 0 ≤ ∏ i, ↑(⋯.eigenvalues i)

Tactic:
]

Goal state after:
n : Type u_2
𝕜 : Type u_3
inst✝² : Fintype n
inst✝¹ : RCLike 𝕜
A : Matrix n n 𝕜
inst✝ : DecidableEq n
hA : A.PosSemidef
⊢ 0 ≤ ∏ i, ↑(⋯.eigenvalues i)
Module: Mathlib.Analysis.InnerProductSpace.Spectrum

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : RCLike 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
hT : T.IsSymmetric
v : E
hv : v ∈ ⨅ i, (eigenspace T i)ᗮ
⊢ T v ∈ ⨅ i, (eigenspace T i)ᗮ

Tactic:
]

Goal state after:
𝕜 : Type u_1
inst✝² : RCLike 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
hT : T.IsSymmetric
v : E
hv : v ∈ ⨅ i, (eigenspace T i)ᗮ
⊢ T v ∈ ⨅ i, (eigenspace T i)ᗮ
Module: Mathlib.Analysis.Matrix.HermitianFunctionalCalculus

Goal state before:
pp: case a
n : Type u_1
𝕜 : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n 𝕜
hA : A.IsHermitian
a : Matrix n n 𝕜
ha : a.IsHermitian
f : C(↑(spectrum ℝ a), ℝ)
⊢ spectrum ℝ (ha.cfcAux f) ⊆ spectrum ℝ f

Tactic:
]

Goal state after:
case a
n : Type u_1
𝕜 : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n 𝕜
hA : A.IsHermitian
a : Matrix n n 𝕜
ha : a.IsHermitian
f : C(↑(spectrum ℝ a), ℝ)
⊢ spectrum ℝ (ha.cfcAux f) ⊆ spectrum ℝ f
Module: Mathlib.Analysis.Matrix.PosDef

Goal state before:
pp: n : Type u_2
𝕜 : Type u_3
inst✝² : Fintype n
inst✝¹ : RCLike 𝕜
A : Matrix n n 𝕜
inst✝ : DecidableEq n
hA : A.PosDef
⊢ 0 < ∏ i, ↑(⋯.eigenvalues i)

Tactic:
]

Goal state after:
n : Type u_2
𝕜 : Type u_3
inst✝² : Fintype n
inst✝¹ : RCLike 𝕜
A : Matrix n n 𝕜
inst✝ : DecidableEq n
hA : A.PosDef
⊢ 0 < ∏ i, ↑(⋯.eigenvalues i)
Module: Mathlib.Analysis.Distribution.ContDiffMapSupportedIn

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
F' : Type u_4
inst✝¹⁰ : NontriviallyNormedField 𝕜
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace ℝ E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℝ F
inst✝⁵ : NormedSpace 𝕜 F
inst✝⁴ : SMulCommClass ℝ 𝕜 F
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace ℝ F'
inst✝¹ : NormedSpace 𝕜 F'
inst✝ : SMulCommClass ℝ 𝕜 F'
n n₁ n₂ k : ℕ∞
K K₁ K₂ : Compacts E
f g : 𝓓^{n}_{K}(E, F)
⊢ EqOn (⇑f + ⇑g) (0 + 0) (↑K)ᶜ

Tactic:
]

Goal state after:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
F' : Type u_4
inst✝¹⁰ : NontriviallyNormedField 𝕜
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace ℝ E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℝ F
inst✝⁵ : NormedSpace 𝕜 F
inst✝⁴ : SMulCommClass ℝ 𝕜 F
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace ℝ F'
inst✝¹ : NormedSpace 𝕜 F'
inst✝ : SMulCommClass ℝ 𝕜 F'
n n₁ n₂ k : ℕ∞
K K₁ K₂ : Compacts E
f g : 𝓓^{n}_{K}(E, F)
⊢ EqOn (⇑f + ⇑g) (0 + 0) (↑K)ᶜ
Module: Mathlib.Analysis.Matrix.HermitianFunctionalCalculus

Goal state before:
pp: case a
n : Type u_1
𝕜 : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n 𝕜
hA : A.IsHermitian
a : Matrix n n 𝕜
ha : a.IsHermitian
f : C(↑(spectrum ℝ a), ℝ)
⊢ Set.range ⇑f ⊆ spectrum ℝ (diagonal (RCLike.ofReal ∘ ⇑f ∘ fun i ↦ ⟨ha.eigenvalues i, ⋯⟩))

Tactic:
]

Goal state after:
case a
n : Type u_1
𝕜 : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n 𝕜
hA : A.IsHermitian
a : Matrix n n 𝕜
ha : a.IsHermitian
f : C(↑(spectrum ℝ a), ℝ)
⊢ Set.range ⇑f ⊆ spectrum ℝ (diagonal (RCLike.ofReal ∘ ⇑f ∘ fun i ↦ ⟨ha.eigenvalues i, ⋯⟩))
Module: Mathlib.Analysis.Distribution.ContDiffMapSupportedIn

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
F' : Type u_4
inst✝¹⁰ : NontriviallyNormedField 𝕜
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace ℝ E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℝ F
inst✝⁵ : NormedSpace 𝕜 F
inst✝⁴ : SMulCommClass ℝ 𝕜 F
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace ℝ F'
inst✝¹ : NormedSpace 𝕜 F'
inst✝ : SMulCommClass ℝ 𝕜 F'
n n₁ n₂ k : ℕ∞
K K₁ K₂ : Compacts E
f : 𝓓^{n}_{K}(E, F)
⊢ EqOn (-⇑f) (-0) (↑K)ᶜ

Tactic:
]

Goal state after:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
F' : Type u_4
inst✝¹⁰ : NontriviallyNormedField 𝕜
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace ℝ E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℝ F
inst✝⁵ : NormedSpace 𝕜 F
inst✝⁴ : SMulCommClass ℝ 𝕜 F
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace ℝ F'
inst✝¹ : NormedSpace 𝕜 F'
inst✝ : SMulCommClass ℝ 𝕜 F'
n n₁ n₂ k : ℕ∞
K K₁ K₂ : Compacts E
f : 𝓓^{n}_{K}(E, F)
⊢ EqOn (-⇑f) (-0) (↑K)ᶜ
Module: Mathlib.Analysis.Matrix.PosDef

Goal state before:
pp: m : Type u_1
n : Type u_2
𝕜 : Type u_3
inst✝² : Fintype m
inst✝¹ : Fintype n
inst✝ : RCLike 𝕜
A M : Matrix n n 𝕜
hM : M.PosSemidef
x y : n → 𝕜
⊢ star x ᵥ* M ⬝ᵥ y = star x ᵥ* M ⬝ᵥ y

Tactic:
]

Goal state after:
Module: Mathlib.Analysis.InnerProductSpace.Spectrum

Goal state before:
pp: 𝕜 : Type u_1
inst✝³ : RCLike 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
inst✝ : FiniteDimensional 𝕜 E
hT : T.IsSymmetric
⊢ ⊥ = ⊥

Tactic:
]

Goal state after:
Module: Mathlib.Analysis.Distribution.ContDiffMapSupportedIn

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
F' : Type u_4
inst✝¹⁰ : NontriviallyNormedField 𝕜
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace ℝ E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℝ F
inst✝⁵ : NormedSpace 𝕜 F
inst✝⁴ : SMulCommClass ℝ 𝕜 F
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace ℝ F'
inst✝¹ : NormedSpace 𝕜 F'
inst✝ : SMulCommClass ℝ 𝕜 F'
n n₁ n₂ k : ℕ∞
K K₁ K₂ : Compacts E
f g : 𝓓^{n}_{K}(E, F)
⊢ EqOn (⇑f - ⇑g) (0 - 0) (↑K)ᶜ

Tactic:
]

Goal state after:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
F' : Type u_4
inst✝¹⁰ : NontriviallyNormedField 𝕜
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace ℝ E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℝ F
inst✝⁵ : NormedSpace 𝕜 F
inst✝⁴ : SMulCommClass ℝ 𝕜 F
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace ℝ F'
inst✝¹ : NormedSpace 𝕜 F'
inst✝ : SMulCommClass ℝ 𝕜 F'
n n₁ n₂ k : ℕ∞
K K₁ K₂ : Compacts E
f g : 𝓓^{n}_{K}(E, F)
⊢ EqOn (⇑f - ⇑g) (0 - 0) (↑K)ᶜ
Module: Mathlib.Analysis.Matrix.PosDef

Goal state before:
pp: m : Type u_1
n : Type u_2
𝕜 : Type u_3
inst✝² : Fintype m
inst✝¹ : Fintype n
inst✝ : RCLike 𝕜
A M : Matrix n n 𝕜
hM : M.PosSemidef
x✝² x✝¹ : n → 𝕜
x✝ : 𝕜
⊢ M *ᵥ x✝¹ ⬝ᵥ star (x✝ • x✝²) = M *ᵥ x✝¹ ⬝ᵥ star (x✝ • x✝²)

Tactic:
]

Goal state after:
Module: Mathlib.Analysis.Matrix.HermitianFunctionalCalculus

Goal state before:
pp: n : Type u_1
𝕜 : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n 𝕜
hA : A.IsHermitian
a : Matrix n n 𝕜
ha : a.IsHermitian
f : C(↑(spectrum ℝ a), ℝ)
⊢ ((conjStarAlgAut 𝕜 (Matrix n n 𝕜)) ha.eigenvectorUnitary)
      (diagonal (star (RCLike.ofReal ∘ ⇑f ∘ fun i ↦ ⟨ha.eigenvalues i, ⋯⟩))) =
    ((conjStarAlgAut 𝕜 (Matrix n n 𝕜)) ha.eigenvectorUnitary)
      (diagonal (RCLike.ofReal ∘ ⇑f ∘ fun i ↦ ⟨ha.eigenvalues i, ⋯⟩))

Tactic:
]

Goal state after:
n : Type u_1
𝕜 : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n 𝕜
hA : A.IsHermitian
a : Matrix n n 𝕜
ha : a.IsHermitian
f : C(↑(spectrum ℝ a), ℝ)
⊢ ((conjStarAlgAut 𝕜 (Matrix n n 𝕜)) ha.eigenvectorUnitary)
      (diagonal (star (RCLike.ofReal ∘ ⇑f ∘ fun i ↦ ⟨ha.eigenvalues i, ⋯⟩))) =
    ((conjStarAlgAut 𝕜 (Matrix n n 𝕜)) ha.eigenvectorUnitary)
      (diagonal (RCLike.ofReal ∘ ⇑f ∘ fun i ↦ ⟨ha.eigenvalues i, ⋯⟩))
Module: Mathlib.Analysis.Distribution.ContDiffMapSupportedIn

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
F' : Type u_4
inst✝¹⁴ : NontriviallyNormedField 𝕜
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : NormedAddCommGroup F
inst✝¹⁰ : NormedSpace ℝ F
inst✝⁹ : NormedSpace 𝕜 F
inst✝⁸ : SMulCommClass ℝ 𝕜 F
inst✝⁷ : NormedAddCommGroup F'
inst✝⁶ : NormedSpace ℝ F'
inst✝⁵ : NormedSpace 𝕜 F'
inst✝⁴ : SMulCommClass ℝ 𝕜 F'
n n₁ n₂ k : ℕ∞
K K₁ K₂ : Compacts E
R : Type ?u.48
inst✝³ : Semiring R
inst✝² : Module R F
inst✝¹ : SMulCommClass ℝ R F
inst✝ : ContinuousConstSMul R F
c : R
f : 𝓓^{n}_{K}(E, F)
⊢ EqOn (c • ⇑f) (c • 0) (↑K)ᶜ

Tactic:
]

Goal state after:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
F' : Type u_4
inst✝¹⁴ : NontriviallyNormedField 𝕜
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : NormedAddCommGroup F
inst✝¹⁰ : NormedSpace ℝ F
inst✝⁹ : NormedSpace 𝕜 F
inst✝⁸ : SMulCommClass ℝ 𝕜 F
inst✝⁷ : NormedAddCommGroup F'
inst✝⁶ : NormedSpace ℝ F'
inst✝⁵ : NormedSpace 𝕜 F'
inst✝⁴ : SMulCommClass ℝ 𝕜 F'
n n₁ n₂ k : ℕ∞
K K₁ K₂ : Compacts E
R : Type ?u.48
inst✝³ : Semiring R
inst✝² : Module R F
inst✝¹ : SMulCommClass ℝ R F
inst✝ : ContinuousConstSMul R F
c : R
f : 𝓓^{n}_{K}(E, F)
⊢ EqOn (c • ⇑f) (c • 0) (↑K)ᶜ
Module: Mathlib.Analysis.InnerProductSpace.Spectrum

Goal state before:
pp: 𝕜 : Type u_1
inst✝³ : RCLike 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
inst✝ : FiniteDimensional 𝕜 E
n : ℕ
hT : T.IsSymmetric
hn : finrank 𝕜 E = n
i : Fin n
x : 𝕜
hx : HasUnifEigenvalue T x 1
⊢ HasEigenvalue T x

Tactic:
]

Goal state after:
𝕜 : Type u_1
inst✝³ : RCLike 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
inst✝ : FiniteDimensional 𝕜 E
n : ℕ
hT : T.IsSymmetric
hn : finrank 𝕜 E = n
i : Fin n
x : 𝕜
hx : HasUnifEigenvalue T x 1
⊢ HasEigenvalue T x
Module: Mathlib.Analysis.Matrix.HermitianFunctionalCalculus

Goal state before:
pp: n : Type u_1
𝕜 : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n 𝕜
hA : A.IsHermitian
f : ℝ → ℝ
hA' : IsSelfAdjoint A
this : cfcHom hA' = hA.cfcAux
⊢ Continuous ((spectrum ℝ A).domRestrict f)

Tactic:
]

Goal state after:
n : Type u_1
𝕜 : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n 𝕜
hA : A.IsHermitian
f : ℝ → ℝ
hA' : IsSelfAdjoint A
this : cfcHom hA' = hA.cfcAux
⊢ Continuous ((spectrum ℝ A).domRestrict f)
Module: Mathlib.Analysis.Distribution.ContDiffMapSupportedIn

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
F' : Type u_4
inst✝¹¹ : NontriviallyNormedField 𝕜
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace ℝ F
inst✝⁶ : NormedSpace 𝕜 F
inst✝⁵ : SMulCommClass ℝ 𝕜 F
inst✝⁴ : NormedAddCommGroup F'
inst✝³ : NormedSpace ℝ F'
inst✝² : NormedSpace 𝕜 F'
inst✝¹ : SMulCommClass ℝ 𝕜 F'
n n₁ n₂ k : ℕ∞
K K₁ K₂ : Compacts E
inst✝ : LinearMap.CompatibleSMul F F' ℝ 𝕜
T : F →L[𝕜] F'
f g : 𝓓^{n}_{K}(E, F)
⊢ { toFun := ⇑T ∘ ⇑(f + g), contDiff' := ⋯, zero_on_compl' := ⋯ } =
    { toFun := ⇑T ∘ ⇑f, contDiff' := ⋯, zero_on_compl' := ⋯ } +
      { toFun := ⇑T ∘ ⇑g, contDiff' := ⋯, zero_on_compl' := ⋯ }

Tactic:
by ext x; exact map_add T (f x) (g x)

Goal state after:
Module: Mathlib.Analysis.Matrix.HermitianFunctionalCalculus

Goal state before:
pp: n : Type u_1
𝕜 : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n 𝕜
hA : A.IsHermitian
f : ℝ → ℝ
hA' : IsSelfAdjoint A
this : cfcHom hA' = hA.cfcAux
⊢ hA.cfcAux { toFun := (spectrum ℝ A).domRestrict f, continuous_toFun := ⋯ } = hA.cfc f

Tactic:
]

Goal state after:
n : Type u_1
𝕜 : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n 𝕜
hA : A.IsHermitian
f : ℝ → ℝ
hA' : IsSelfAdjoint A
this : cfcHom hA' = hA.cfcAux
⊢ hA.cfcAux { toFun := (spectrum ℝ A).domRestrict f, continuous_toFun := ⋯ } = hA.cfc f
Module: Mathlib.Analysis.InnerProductSpace.Spectrum

Goal state before:
pp: case h
𝕜 : Type u_1
inst✝³ : RCLike 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
inst✝ : FiniteDimensional 𝕜 E
n : ℕ
hT : T.IsSymmetric
hn : finrank 𝕜 E = n
μ : 𝕜
hμ : HasEigenvalue T μ
x : Eigenvalues T := ⟨μ, hμ⟩
hx : x = ⟨μ, hμ⟩
i : Fin n
hi : DirectSum.IsInternal.subordinateOrthonormalBasisIndex hn ⋯ i ⋯ = x
⊢ μ = μ

Tactic:
]

Goal state after:
Module: Mathlib.Analysis.Matrix.HermitianFunctionalCalculus

Goal state before:
pp: n : Type u_1
𝕜 : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n 𝕜
hA : A.IsHermitian
f : ℝ → ℝ
⊢ (star ↑hA.eigenvectorUnitary * ↑hA.eigenvectorUnitary * diagonal (RCLike.ofReal ∘ f ∘ hA.eigenvalues)).charpoly =
    ∏ i, (X - C ↑(f (hA.eigenvalues i)))

Tactic:
]

Goal state after:
n : Type u_1
𝕜 : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n 𝕜
hA : A.IsHermitian
f : ℝ → ℝ
⊢ (star ↑hA.eigenvectorUnitary * ↑hA.eigenvectorUnitary * diagonal (RCLike.ofReal ∘ f ∘ hA.eigenvalues)).charpoly =
    ∏ i, (X - C ↑(f (hA.eigenvalues i)))
Module: Mathlib.Analysis.InnerProductSpace.Spectrum

Goal state before:
pp: case e'_2
𝕜 : Type u_1
inst✝³ : RCLike 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
inst✝ : FiniteDimensional 𝕜 E
n : ℕ
hT : T.IsSymmetric
hn : finrank 𝕜 E = n
μ : 𝕜
hμ : HasEigenvalue T μ
i : Fin n
a✝ : i ∈ Finset.univ
x : 𝕜
hx : HasUnifEigenvalue T x 1
⊢ x = μ ↔ ⟨x, hx⟩ = ⟨μ, hμ⟩

Tactic:
]

Goal state after:
case e'_2
𝕜 : Type u_1
inst✝³ : RCLike 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
inst✝ : FiniteDimensional 𝕜 E
n : ℕ
hT : T.IsSymmetric
hn : finrank 𝕜 E = n
μ : 𝕜
hμ : HasEigenvalue T μ
i : Fin n
a✝ : i ∈ Finset.univ
x : 𝕜
hx : HasUnifEigenvalue T x 1
⊢ x = μ ↔ ⟨x, hx⟩ = ⟨μ, hμ⟩
Module: Mathlib.Analysis.InnerProductSpace.Spectrum

Goal state before:
pp: case neg
𝕜 : Type u_1
inst✝³ : RCLike 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
inst✝ : FiniteDimensional 𝕜 E
n : ℕ
hT : T.IsSymmetric
hn : finrank 𝕜 E = n
μ : 𝕜
hμ : ¬HasEigenvalue T μ
⊢ ∀ x ∈ Finset.univ, ¬↑(hT.unsortedEigenvalues hn x) = μ

Tactic:
]

Goal state after:
case neg
𝕜 : Type u_1
inst✝³ : RCLike 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
inst✝ : FiniteDimensional 𝕜 E
n : ℕ
hT : T.IsSymmetric
hn : finrank 𝕜 E = n
μ : 𝕜
hμ : ¬HasEigenvalue T μ
⊢ ∀ x ∈ Finset.univ, ¬↑(hT.unsortedEigenvalues hn x) = μ
Module: Mathlib.Analysis.Distribution.ContDiffMapSupportedIn

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : SMulCommClass ℝ 𝕜 F
n₁ n₂ : ℕ∞
K₁ K₂ : Compacts E
f : 𝓓^{n₁}_{K₁}(E, F)
⊢ ⇑({ toFun := fun f ↦ if h : n₂ ≤ n₁ ∧ K₁ ≤ K₂ then ContDiffMapSupportedIn.of_support_subset ⋯ ⋯ else 0, map_add' := ⋯,
          map_smul' := ⋯ }
        f) =
    ⇑(if n₂ ≤ n₁ ∧ K₁ ≤ K₂ then f else 0)

Tactic:
]

Goal state after:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : SMulCommClass ℝ 𝕜 F
n₁ n₂ : ℕ∞
K₁ K₂ : Compacts E
f : 𝓓^{n₁}_{K₁}(E, F)
⊢ ⇑({ toFun := fun f ↦ if h : n₂ ≤ n₁ ∧ K₁ ≤ K₂ then ContDiffMapSupportedIn.of_support_subset ⋯ ⋯ else 0, map_add' := ⋯,
          map_smul' := ⋯ }
        f) =
    ⇑(if n₂ ≤ n₁ ∧ K₁ ≤ K₂ then f else 0)
Module: Mathlib.Analysis.InnerProductSpace.Spectrum

Goal state before:
pp: 𝕜 : Type u_1
inst✝³ : RCLike 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
inst✝ : FiniteDimensional 𝕜 E
n : ℕ
hT : T.IsSymmetric
hn : finrank 𝕜 E = n
i : Fin n
v : E := (hT.unsortedEigenvectorBasis hn) i
μ : 𝕜 := ↑T (DirectSum.IsInternal.subordinateOrthonormalBasisIndex hn ⋯ i ⋯)
key : HasEigenvector T μ v
⊢ (starRingEnd 𝕜) μ = μ

Tactic:
]

Goal state after:
𝕜 : Type u_1
inst✝³ : RCLike 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
inst✝ : FiniteDimensional 𝕜 E
n : ℕ
hT : T.IsSymmetric
hn : finrank 𝕜 E = n
i : Fin n
v : E := (hT.unsortedEigenvectorBasis hn) i
μ : 𝕜 := ↑T (DirectSum.IsInternal.subordinateOrthonormalBasisIndex hn ⋯ i ⋯)
key : HasEigenvector T μ v
⊢ (starRingEnd 𝕜) μ = μ
Module: Mathlib.Analysis.InnerProductSpace.Spectrum

Goal state before:
pp: 𝕜 : Type u_1
inst✝³ : RCLike 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
inst✝ : FiniteDimensional 𝕜 E
n : ℕ
hT : T.IsSymmetric
hn : finrank 𝕜 E = n
μ : 𝕜
⊢ {i | ↑((hT.unsortedEigenvalues hn ∘ ⇑(Tuple.sort (hT.unsortedEigenvalues hn)) ∘ ⇑Fin.revPerm) i) = μ}.card =
    {i | ↑(hT.unsortedEigenvalues hn i) = μ}.card

Tactic:
]

Goal state after:
𝕜 : Type u_1
inst✝³ : RCLike 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
inst✝ : FiniteDimensional 𝕜 E
n : ℕ
hT : T.IsSymmetric
hn : finrank 𝕜 E = n
μ : 𝕜
⊢ {i | ↑((hT.unsortedEigenvalues hn ∘ ⇑(Tuple.sort (hT.unsortedEigenvalues hn)) ∘ ⇑Fin.revPerm) i) = μ}.card =
    {i | ↑(hT.unsortedEigenvalues hn i) = μ}.card
Module: Mathlib.Analysis.InnerProductSpace.Spectrum

Goal state before:
pp: 𝕜 : Type u_1
inst✝³ : RCLike 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
inst✝ : FiniteDimensional 𝕜 E
n : ℕ
hT : T.IsSymmetric
hn : finrank 𝕜 E = n
i : Fin n
⊢ HasEigenvector T (↑((hT.unsortedEigenvalues hn ∘ ⇑(Tuple.sort (hT.unsortedEigenvalues hn)) ∘ ⇑Fin.revPerm) i))
    ((DirectSum.IsInternal.subordinateOrthonormalBasis hn ⋯ ⋯)
      ((Equiv.symm (Tuple.sort (hT.unsortedEigenvalues hn) * Fin.revPerm)).symm i))

Tactic:
]

Goal state after:
𝕜 : Type u_1
inst✝³ : RCLike 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
inst✝ : FiniteDimensional 𝕜 E
n : ℕ
hT : T.IsSymmetric
hn : finrank 𝕜 E = n
i : Fin n
⊢ HasEigenvector T (↑((hT.unsortedEigenvalues hn ∘ ⇑(Tuple.sort (hT.unsortedEigenvalues hn)) ∘ ⇑Fin.revPerm) i))
    ((DirectSum.IsInternal.subordinateOrthonormalBasis hn ⋯ ⋯)
      ((Equiv.symm (Tuple.sort (hT.unsortedEigenvalues hn) * Fin.revPerm)).symm i))