mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Distribution.TemperateGrowth

Goal state before:
pp: case hbc
D : Type u_4
E : Type u_5
F : Type u_6
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedAddCommGroup D
inst✝ : NormedSpace ℝ D
g : E → F
f : D → E
t : Set E
ht : Set.range f ⊆ t
ht' : UniqueDiffOn ℝ t
hg₁ : ContDiffOn ℝ ∞ g t
hg₂ : ∀ (N : ℕ), ∃ k C, ∃ (_ : 0 ≤ C), ∀ n ≤ N, ∀ x ∈ t, ‖iteratedFDerivWithin ℝ n g t x‖ ≤ C * (1 + ‖x‖) ^ k
hf : HasTemperateGrowth f
n k₁ : ℕ
C₁ : ℝ
hC₁ : 0 ≤ C₁
h₁ : ∀ N ≤ n, ∀ (x : D), ‖iteratedFDeriv ℝ N f x‖ ≤ C₁ * (1 + ‖x‖) ^ k₁
k₂ : ℕ
C₂ : ℝ
hC₂ : 0 ≤ C₂
h₂ : ∀ n_1 ≤ n, ∀ x ∈ t, ‖iteratedFDerivWithin ℝ n_1 g t x‖ ≤ C₂ * (1 + ‖x‖) ^ k₂
h₁' : ∀ (x : D), ‖f x‖ ≤ C₁ * (1 + ‖x‖) ^ k₁
C₃ : ℝ := ⋯
x : D
hg' : ∀ i ≤ n, ‖iteratedFDerivWithin ℝ i g t (f x)‖ ≤ C₃ * (1 + ‖x‖) ^ (k₁ * k₂)
i : ℕ
hi : 1 ≤ i
hi' : i ≤ n
⊢ C₁ ≤ 1 + C₁

Tactic:
simp

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

Goal state before:
pp: E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
Ω : Opens E
F : Type u_4
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
n : ℕ∞
K : Compacts E
K_sub_Ω : ↑K ⊆ ↑Ω
⊢ Continuous (ofSupportedIn K_sub_Ω)

Tactic:
rw [continuous_iff_coinduced_le]

Goal state after:
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
Ω : Opens E
F : Type u_4
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
n : ℕ∞
K : Compacts E
K_sub_Ω : ↑K ⊆ ↑Ω
⊢ coinduced (ofSupportedIn K_sub_Ω) ContDiffMapSupportedIn.topologicalSpace ≤ topologicalSpace Ω F n
Module: Mathlib.Analysis.Distribution.TemperateGrowth

Goal state before:
pp: case h
D : Type u_4
E : Type u_5
F : Type u_6
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedAddCommGroup D
inst✝ : NormedSpace ℝ D
g : E → F
f : D → E
t : Set E
ht : Set.range f ⊆ t
ht' : UniqueDiffOn ℝ t
hg₁ : ContDiffOn ℝ ∞ g t
hg₂ : ∀ (N : ℕ), ∃ k C, ∃ (_ : 0 ≤ C), ∀ n ≤ N, ∀ x ∈ t, ‖iteratedFDerivWithin ℝ n g t x‖ ≤ C * (1 + ‖x‖) ^ k
hf : HasTemperateGrowth f
n k₁ : ℕ
C₁ : ℝ
hC₁ : 0 ≤ C₁
h₁ : ∀ N ≤ n, ∀ (x : D), ‖iteratedFDeriv ℝ N f x‖ ≤ C₁ * (1 + ‖x‖) ^ k₁
k₂ : ℕ
C₂ : ℝ
hC₂ : 0 ≤ C₂
h₂ : ∀ n_1 ≤ n, ∀ x ∈ t, ‖iteratedFDerivWithin ℝ n_1 g t x‖ ≤ C₂ * (1 + ‖x‖) ^ k₂
h₁' : ∀ (x : D), ‖f x‖ ≤ C₁ * (1 + ‖x‖) ^ k₁
C₃ : ℝ := ∑ k ∈ Finset.range (k₂ + 1), C₂ * ↑(k₂.choose k) * C₁ ^ k
x : D
hg' : ∀ i ≤ n, ‖iteratedFDerivWithin ℝ i g t (f x)‖ ≤ C₃ * (1 + ‖x‖) ^ (k₁ * k₂)
⊢ ‖iteratedFDeriv ℝ n (g ∘ f) x‖ ≤ ↑n ! * C₃ * (1 + C₁) ^ n * (1 + ‖x‖) ^ (k₁ * k₂ + k₁ * n)

Tactic:
have hf' : ∀ i, 1 ≤ i → i ≤ n → ‖iteratedFDeriv ℝ i f x‖ ≤ ((1 + C₁) * (1 + ‖x‖) ^ k₁) ^ i := by
    intro i hi hi'
    calc _ ≤ C₁ * (1 + ‖x‖) ^ k₁ := h₁ i hi' x
      _ ≤ (1 + C₁) * (1 + ‖x‖) ^ k₁ := by gcongr; simp
      _ ≤ _ := by
        apply le_self_pow₀ (one_le_mul_of_one_le_of_one_le (by simp [hC₁]) (by simp [one_le_pow₀]))
        grind

Goal state after:
case h
D : Type u_4
E : Type u_5
F : Type u_6
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedAddCommGroup D
inst✝ : NormedSpace ℝ D
g : E → F
f : D → E
t : Set E
ht : Set.range f ⊆ t
ht' : UniqueDiffOn ℝ t
hg₁ : ContDiffOn ℝ ∞ g t
hg₂ : ∀ (N : ℕ), ∃ k C, ∃ (_ : 0 ≤ C), ∀ n ≤ N, ∀ x ∈ t, ‖iteratedFDerivWithin ℝ n g t x‖ ≤ C * (1 + ‖x‖) ^ k
hf : HasTemperateGrowth f
n k₁ : ℕ
C₁ : ℝ
hC₁ : 0 ≤ C₁
h₁ : ∀ N ≤ n, ∀ (x : D), ‖iteratedFDeriv ℝ N f x‖ ≤ C₁ * (1 + ‖x‖) ^ k₁
k₂ : ℕ
C₂ : ℝ
hC₂ : 0 ≤ C₂
h₂ : ∀ n_1 ≤ n, ∀ x ∈ t, ‖iteratedFDerivWithin ℝ n_1 g t x‖ ≤ C₂ * (1 + ‖x‖) ^ k₂
h₁' : ∀ (x : D), ‖f x‖ ≤ C₁ * (1 + ‖x‖) ^ k₁
C₃ : ℝ := ∑ k ∈ Finset.range (k₂ + 1), C₂ * ↑(k₂.choose k) * C₁ ^ k
x : D
hg' : ∀ i ≤ n, ‖iteratedFDerivWithin ℝ i g t (f x)‖ ≤ C₃ * (1 + ‖x‖) ^ (k₁ * k₂)
hf' : ∀ (i : ℕ), 1 ≤ i → i ≤ n → ‖iteratedFDeriv ℝ i f x‖ ≤ ((1 + C₁) * (1 + ‖x‖) ^ k₁) ^ i
⊢ ‖iteratedFDeriv ℝ n (g ∘ f) x‖ ≤ ↑n ! * C₃ * (1 + C₁) ^ n * (1 + ‖x‖) ^ (k₁ * k₂ + k₁ * n)
Module: Mathlib.Analysis.Distribution.TemperateGrowth

Goal state before:
pp: case ht
D : Type u_4
E : Type u_5
F : Type u_6
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedAddCommGroup D
inst✝ : NormedSpace ℝ D
g : E → F
f : D → E
hg : HasTemperateGrowth g
hf : HasTemperateGrowth f
⊢ Set.range f ⊆ Set.univ

Tactic:
simp

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

Goal state before:
pp: case ht'
D : Type u_4
E : Type u_5
F : Type u_6
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedAddCommGroup D
inst✝ : NormedSpace ℝ D
g : E → F
f : D → E
hg : HasTemperateGrowth g
hf : HasTemperateGrowth f
⊢ UniqueDiffOn ℝ Set.univ

Tactic:
simp

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

Goal state before:
pp: case empty
ι : Type u_1
E : Type u_5
F : Type u_6
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : ι → E → F
hf : ∀ i ∈ ∅, HasTemperateGrowth (f i)
⊢ HasTemperateGrowth fun x ↦ ∑ i ∈ ∅, f i x

Tactic:
simp

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

Goal state before:
pp: case h
E : Type u_5
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
⊢ ∀ (x : E), ‖_root_.id x‖ ≤ 1 * (1 + ‖x‖) ^ 1

Tactic:
simp

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
Ω : Opens E
F : Type u_4
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : NormedSpace 𝕜 F
n k : ℕ∞
inst✝¹ : Algebra ℝ 𝕜
inst✝ : IsScalarTower ℝ 𝕜 F
K : Compacts E
K_sub_Ω : ↑K ⊆ ↑Ω
f : 𝓓^{n}_{K}(E, F)
a✝ x✝ : E
⊢ (((fderivCLM 𝕜 n k) (ofSupportedIn K_sub_Ω f)) a✝) x✝ =
    ((ofSupportedIn K_sub_Ω ((ContDiffMapSupportedIn.fderivCLM 𝕜 n k) f)) a✝) x✝

Tactic:
simp

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

Goal state before:
pp: E : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
Ω : Opens E
F : Type u_4
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
n : ℕ∞
m : MeasurableSpace E
inst✝ : OpensMeasurableSpace E
μ : Measure E
H : LocallyIntegrableOn (fun x ↦ 1) (↑Ω) μ
f : 𝓓^{n}(Ω, F)
⊢ Integrable (⇑f) μ

Tactic:
rw [← integrableOn_iff_integrable_of_support_subset (subset_tsupport f)]
  replace H := H.integrableOn_compact_subset f.tsupport_subset f.hasCompactSupport
  suffices IntegrableOn ((1 : ℝ) • f) (tsupport f) μ by simpa
  rw [IntegrableOn, ← memLp_one_iff_integrable] at H ⊢
  exact f.memLp_top.smul H

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

Goal state before:
pp: case neg
𝕜 : Type u_1
𝕂 : Type u_2
inst✝²⁰ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝¹⁹ : NormedAddCommGroup E
inst✝¹⁸ : NormedSpace ℝ E
Ω Ω₁ Ω₂ : Opens E
F : Type u_4
inst✝¹⁷ : NormedAddCommGroup F
inst✝¹⁶ : NormedSpace ℝ F
inst✝¹⁵ : NormedSpace 𝕜 F
F' : Type u_5
inst✝¹⁴ : NormedAddCommGroup F'
inst✝¹³ : NormedSpace ℝ F'
inst✝¹² : NormedSpace 𝕜 F'
n n₁ n₂ k : ℕ∞
m : MeasurableSpace E
inst✝¹¹ : OpensMeasurableSpace E
F₁ : Type u_6
F₂ : Type u_7
F₃ : Type u_8
inst✝¹⁰ : NormedAddCommGroup F₁
inst✝⁹ : NormedSpace 𝕜 F₁
inst✝⁸ : NormedSpace ℝ F₁
inst✝⁷ : NormedAddCommGroup F₂
inst✝⁶ : NormedSpace 𝕜 F₂
inst✝⁵ : NormedAddCommGroup F₃
inst✝⁴ : NormedSpace 𝕜 F₃
inst✝³ : Algebra ℝ 𝕜
inst✝² : IsScalarTower ℝ 𝕜 F₁
inst✝¹ : NormedSpace ℝ F₃
inst✝ : IsScalarTower ℝ 𝕜 F₃
B : F₁ →L[𝕜] F₂ →L[𝕜] F₃
μ : Measure E
φ : E → F₂
K : Compacts E
K_sub_Ω : ↑K ⊆ ↑Ω
f : 𝓓^{n}_{K}(E, F₁)
h : ¬LocallyIntegrableOn φ (↑Ω) μ
⊢ 0 = 0 f

Tactic:
simp

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

Goal state before:
pp: H : Type u_8
inst✝¹ : NormedAddCommGroup H
inst✝ : InnerProductSpace ℝ H
r : ℝ
t : Set ℝ := {y | 1 / 2 < y}
ht : (Set.range fun x ↦ 1 + ‖x‖ ^ 2) ⊆ t
hdiff : ContDiffOn ℝ ∞ (fun x ↦ x ^ r) t
hunique : UniqueDiffOn ℝ t
N k : ℕ
hk : max r ((↑N - r) * Real.log 2 / Real.log (3 / 2)) ≤ ↑k
hk₁ : r ≤ ↑k
hk₂ : Real.log 2 * (↑N - r) ≤ Real.log (3 / 2) * ↑k
n : ℕ
hn : n ≤ N
x : ℝ
hx : x ∈ t
this : ContDiffAt ℝ (↑n) (fun x ↦ x ^ r) x
hx' : 1 / 2 < x
hx'' : 0 < x
h : 0 ≤ r - ↑n
⊢ ↑k ≤ ↑k + ↑n

Tactic:
simp

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

Goal state before:
pp: H : Type u_8
inst✝¹ : NormedAddCommGroup H
inst✝ : InnerProductSpace ℝ H
r : ℝ
t : Set ℝ := {y | 1 / 2 < y}
ht : (Set.range fun x ↦ 1 + ‖x‖ ^ 2) ⊆ t
hdiff : ContDiffOn ℝ ∞ (fun x ↦ x ^ r) t
hunique : UniqueDiffOn ℝ t
N k : ℕ
hk : max r ((↑N - r) * Real.log 2 / Real.log (3 / 2)) ≤ ↑k
hk₁ : r ≤ ↑k
hk₂ : Real.log 2 * (↑N - r) ≤ Real.log (3 / 2) * ↑k
n : ℕ
hn : n ≤ N
x : ℝ
hx : x ∈ t
this✝ : ContDiffAt ℝ (↑n) (fun x ↦ x ^ r) x
hx' : 1 / 2 < x
hx'' : 0 < x
h : 0 ≤ r - ↑n
this : r - ↑n ≤ ↑k
⊢ |x| ≤ 1 + |x|

Tactic:
simp

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

Goal state before:
pp: H : Type u_8
inst✝¹ : NormedAddCommGroup H
inst✝ : InnerProductSpace ℝ H
r : ℝ
t : Set ℝ := {y | 1 / 2 < y}
ht : (Set.range fun x ↦ 1 + ‖x‖ ^ 2) ⊆ t
hdiff : ContDiffOn ℝ ∞ (fun x ↦ x ^ r) t
hunique : UniqueDiffOn ℝ t
N k : ℕ
hk : max r ((↑N - r) * Real.log 2 / Real.log (3 / 2)) ≤ ↑k
hk₁ : r ≤ ↑k
hk₂ : Real.log 2 * (↑N - r) ≤ Real.log (3 / 2) * ↑k
n : ℕ
hn : n ≤ N
x : ℝ
hx : x ∈ t
this✝ : ContDiffAt ℝ (↑n) (fun x ↦ x ^ r) x
hx' : 1 / 2 < x
hx'' : 0 < x
h : 0 ≤ r - ↑n
this : r - ↑n ≤ ↑k
⊢ 1 ≤ 1 + |x|

Tactic:
simp

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝³ : RCLike 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
T : E →L[𝕜] E
inst✝ : CompleteSpace E
hT : IsSelfAdjoint T
a✝ : Nontrivial E
h : (algebraMap ℝ 𝕜) ‖T‖ ∈ spectrum 𝕜 T
⊢ ↑‖T‖₊ ≤ ↑‖(algebraMap ℝ 𝕜) ‖T‖‖₊

Tactic:
simp

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝³ : RCLike 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
T : E →L[𝕜] E
inst✝ : CompleteSpace E
hT : IsSelfAdjoint T
a✝ : Nontrivial E
h : (algebraMap ℝ 𝕜) (-‖T‖) ∈ spectrum 𝕜 T
⊢ ↑‖T‖₊ ≤ ↑‖(algebraMap ℝ 𝕜) (-‖T‖)‖₊

Tactic:
simp

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

Goal state before:
pp: ι : Type u_1
𝕜 : Type u_2
R : Type u_3
D : Type u_4
E : Type u_5
F : Type u_6
G : Type u_7
H : Type u_8
inst✝¹ : NormedAddCommGroup E
inst✝ : MeasurableSpace E
μ : Measure E
h : IsFiniteMeasure μ
⊢ Integrable (fun x ↦ (1 + ‖x‖) ^ (-↑0)) μ

Tactic:
simp

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

Goal state before:
pp: F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace ℝ F
inst✝ : CompleteSpace F
T : F →L[ℝ] F
hT : IsSelfAdjoint T
x₀ : F
hextr : IsLocalExtrOn T.reApplyInnerSelf (sphere 0 ‖x₀‖) x₀
x : F
⊢ x ∈ {x | ‖x‖ ^ 2 = ‖x₀‖ ^ 2} ↔ x ∈ sphere 0 ‖x₀‖

Tactic:
simp

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

Goal state before:
pp: case h₁.hz
C₁ C₂ : ℝ
k l : ℕ
x f : ℝ
hx : 0 ≤ x
hf : 0 ≤ f
h₁ : f ≤ C₁
h₂ : x ^ (k + l) * f ≤ C₂
this✝ : 0 ≤ C₂
this : 2 ^ l * (C₁ + C₂) * (1 + x) ^ (-↑l) = ((1 + x) / 2) ^ (-↑l) * (C₁ + C₂)
h'x : x ≤ 1
⊢ -↑l ≤ 0

Tactic:
simp

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

Goal state before:
pp: C₁ C₂ : ℝ
k l : ℕ
x f : ℝ
hx : 0 ≤ x
hf : 0 ≤ f
h₁ : f ≤ C₁
h₂ : x ^ (k + l) * f ≤ C₂
this✝ : 0 ≤ C₂
this : 2 ^ l * (C₁ + C₂) * (1 + x) ^ (-↑l) = ((1 + x) / 2) ^ (-↑l) * (C₁ + C₂)
h'x : 1 ≤ x
⊢ x ^ ↑k * f = x ^ (-↑l + ↑(k + l)) * f

Tactic:
simp

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

Goal state before:
pp: C₁ C₂ : ℝ
k l : ℕ
x f : ℝ
hx : 0 ≤ x
hf : 0 ≤ f
h₁ : f ≤ C₁
h₂ : x ^ (k + l) * f ≤ C₂
this✝ : 0 ≤ C₂
this : 2 ^ l * (C₁ + C₂) * (1 + x) ^ (-↑l) = ((1 + x) / 2) ^ (-↑l) * (C₁ + C₂)
h'x : 1 ≤ x
⊢ -↑l ≤ 0

Tactic:
simp

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

Goal state before:
pp: 𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst✝¹⁰ : NontriviallyNormedField 𝕜₁
inst✝⁹ : NormedField 𝕜₂
σ₁₂ : 𝕜₁ →+* 𝕜₂
M₁ : Type u_3
M₂ : Type u_4
inst✝⁸ : SeminormedAddCommGroup M₁
inst✝⁷ : AddCommGroup M₂
inst✝⁶ : NormedSpace 𝕜₁ M₁
inst✝⁵ : Module 𝕜₂ M₂
inst✝⁴ : UniformSpace M₂
inst✝³ : IsUniformAddGroup M₂
inst✝² : ContinuousConstSMul 𝕜₂ M₂
inst✝¹ : T2Space M₂
inst✝ : CompleteSpace M₂
u : M₁ →SL[σ₁₂] M₂
hu : ∀ U ∈ 𝓝 0, ∃ y ∈ {f | IsCompactOperator ⇑f}, y - u ∈ U
U : Set M₂
hU : U ∈ 𝓝 0
V : Set M₂
hV : V ∈ 𝓝 0
hVU : ∀ v ∈ V, ∀ w ∈ V, v + w ∈ U
SV : Set M₁ × Set M₂ := (closedBall 0 1, -V)
v : M₁ →SL[σ₁₂] M₂
hv : v ∈ {f | IsCompactOperator ⇑f}
huv : v - u ∈ {f | ∀ x ∈ SV.1, f x ∈ SV.2}
T : Set M₂
hT : T.Finite
hTv✝ : closure[inst✝⁴.toTopologicalSpace] (⇑↑v '' closedBall 0 1) ⊆ ⋃ y ∈ T, y +ᵥ V
x : M₁
hTv : ∃ i, ∃ (_ : i ∈ T), x ∈ ⇑v ⁻¹' (i +ᵥ V)
hx : x ∈ closedBall 0 1
⊢ ∃ i, ∃ (_ : i ∈ T), x ∈ ⇑u ⁻¹' (i +ᵥ U)

Tactic:
rcases hTv with ⟨t, ht, htx⟩

Goal state after:
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst✝¹⁰ : NontriviallyNormedField 𝕜₁
inst✝⁹ : NormedField 𝕜₂
σ₁₂ : 𝕜₁ →+* 𝕜₂
M₁ : Type u_3
M₂ : Type u_4
inst✝⁸ : SeminormedAddCommGroup M₁
inst✝⁷ : AddCommGroup M₂
inst✝⁶ : NormedSpace 𝕜₁ M₁
inst✝⁵ : Module 𝕜₂ M₂
inst✝⁴ : UniformSpace M₂
inst✝³ : IsUniformAddGroup M₂
inst✝² : ContinuousConstSMul 𝕜₂ M₂
inst✝¹ : T2Space M₂
inst✝ : CompleteSpace M₂
u : M₁ →SL[σ₁₂] M₂
hu : ∀ U ∈ 𝓝 0, ∃ y ∈ {f | IsCompactOperator ⇑f}, y - u ∈ U
U : Set M₂
hU : U ∈ 𝓝 0
V : Set M₂
hV : V ∈ 𝓝 0
hVU : ∀ v ∈ V, ∀ w ∈ V, v + w ∈ U
SV : Set M₁ × Set M₂ := (closedBall 0 1, -V)
v : M₁ →SL[σ₁₂] M₂
hv : v ∈ {f | IsCompactOperator ⇑f}
huv : v - u ∈ {f | ∀ x ∈ SV.1, f x ∈ SV.2}
T : Set M₂
hT : T.Finite
hTv : closure[inst✝⁴.toTopologicalSpace] (⇑↑v '' closedBall 0 1) ⊆ ⋃ y ∈ T, y +ᵥ V
x : M₁
hx : x ∈ closedBall 0 1
t : M₂
ht : t ∈ T
htx : x ∈ ⇑v ⁻¹' (t +ᵥ V)
⊢ ∃ i, ∃ (_ : i ∈ T), x ∈ ⇑u ⁻¹' (i +ᵥ U)
Module: Mathlib.Analysis.InnerProductSpace.Rayleigh

Goal state before:
pp: 𝕜 : Type u_1
inst✝³ : RCLike 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
T : E →L[𝕜] E
hT : IsSelfAdjoint T
x₀ : E
hx₀ : x₀ ≠ 0
hextr : IsMaxOn T.reApplyInnerSelf (sphere 0 ‖x₀‖) x₀
hx₀' : 0 < ‖x₀‖
⊢ x₀ ∈ sphere 0 ‖x₀‖

Tactic:
simp

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝³ : RCLike 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
T : E →L[𝕜] E
hT : IsSelfAdjoint T
x₀ : E
hx₀ : x₀ ≠ 0
hextr : IsMinOn T.reApplyInnerSelf (sphere 0 ‖x₀‖) x₀
hx₀' : 0 < ‖x₀‖
⊢ x₀ ∈ sphere 0 ‖x₀‖

Tactic:
simp

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁴ : RCLike 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : FiniteDimensional 𝕜 E
T : E →ₗ[𝕜] E
inst✝ : Nontrivial E
hT : T.IsSymmetric
this : ProperSpace E
T' : ↥(selfAdjoint (E →L[𝕜] E)) := hT.toSelfAdjoint
x : E
hx : x ≠ 0
H₁ : IsCompact (sphere 0 ‖x‖)
⊢ x ∈ sphere 0 ‖x‖

Tactic:
simp

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

Goal state before:
pp: E : Type u_5
inst✝¹ : NormedAddCommGroup E
inst✝ : MeasurableSpace E
μ : Measure E
hμ : μ.HasTemperateGrowth
⊢ ∀ᵐ (x : E) ∂μ, ‖(1 + ‖x‖) ^ (-↑0)‖ ≤ 1

Tactic:
simp

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

Goal state before:
pp: 𝕜 : Type u_1
X : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup X
inst✝ : NormedSpace 𝕜 X
T : X →L[𝕜] X
μ : 𝕜
hT : IsCompactOperator ⇑T
hμ : μ ≠ 0
h : ∀ c > 0, ∃ x, ‖(T - μ • 1) x‖ < c * ‖x‖
hK : ∀ K > 0, ∃ x, ‖(T - μ • 1) x‖ < K * ‖x‖
C : 𝕜
hC : 1 < ‖C‖
ε : ℝ
hε : ε > 0
x : X
hx : ‖(T - μ • 1) x‖ < ε * ‖x‖
this : x ≠ 0
⊢ 0 < 1

Tactic:
simp

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

Goal state before:
pp: case inl
n : Type u_1
inst✝³ : Fintype n
inst✝² : DecidableEq n
R : Type u_2
inst✝¹ : CommRing R
B : Matrix n n R
inst✝ : IsDomain R
hAps : B.charpoly.Splits
h : IsEmpty n
⊢ B.trace = B.charpoly.roots.sum

Tactic:
simp

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

Goal state before:
pp: K : Type u_3
V : Type u_4
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : Module.Finite K V
f : End K V
h : (charpoly f).Splits
b : Basis (Free.ChooseBasisIndex K V) K V := Free.chooseBasis K V
⊢ ((toMatrix (Free.chooseBasis K V) (Free.chooseBasis K V)) f).trace = (charpoly f).roots.sum

Tactic:
Matrix.trace_eq_sum_roots_charpoly_of_splits (by simpa using h),

Goal state after:
K : Type u_3
V : Type u_4
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : Module.Finite K V
f : End K V
h : (charpoly f).Splits
b : Basis (Free.ChooseBasisIndex K V) K V := Free.chooseBasis K V
⊢ ((toMatrix (Free.chooseBasis K V) (Free.chooseBasis K V)) f).charpoly.roots.sum = (charpoly f).roots.sum
Module: Mathlib.Analysis.Distribution.TemperateGrowth

Goal state before:
pp: case hx
E : Type u_5
inst✝¹ : NormedAddCommGroup E
inst✝ : MeasurableSpace E
μ : Measure E
hμ : μ.HasTemperateGrowth
p : ℝ≥0
hp : ↑p ≠ 0
h_one_add : ∀ (x : E), 0 < 1 + ‖x‖
hp_pos : 0 < ↑p
l : ℕ
hl : Integrable (fun x ↦ (1 + ‖x‖) ^ (-↑l)) μ
k : ℕ := ⋯
hlk : ↑l ≤ ↑k * ↑p
x : E
⊢ 1 ≤ 1 + ‖x‖

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Fin.Tuple.Sort

Goal state before:
pp: case H
n : ℕ
α : Type u_1
inst✝ : LinearOrder α
f : Fin n → α
a₁✝ a₂✝ : Fin n
⊢ ((fun i ↦ (f i, i)) a₁✝).1 = ((fun i ↦ (f i, i)) a₂✝).1 ∧ ((fun i ↦ (f i, i)) a₁✝).2 = ((fun i ↦ (f i, i)) a₂✝).2 →
    a₁✝ = a₂✝

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Fin.Tuple.Sort

Goal state before:
pp: n : ℕ
α : Type u_1
inst✝ : LinearOrder α
f : Fin n → α
i : Fin n
⊢ (fun p ↦ (↑p).2) ((fun i ↦ ⟨(f i, i), ⋯⟩) i) = i

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Fin.Tuple.Sort

Goal state before:
pp: n : ℕ
α : Type u_1
inst✝ : LinearOrder α
f : Fin n → α
⊢ (graph f).card = n

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Fin.Tuple.Sort

Goal state before:
pp: n : ℕ
α : Type u_1
inst✝ : LinearOrder α
f : Fin n → α
⊢ graph.proj ∘ (⇑(graphEquiv₁ f) ∘ ⇑(graphEquiv₁ f).symm) ∘ ⇑(graphEquiv₂ f).toEquiv = graph.proj ∘ ⇑(graphEquiv₂ f)

Tactic:
simp

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

Goal state before:
pp: 𝕜 : Type u_1
X : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup X
inst✝ : NormedSpace 𝕜 X
S : End 𝕜 X
hS_not_surj : ¬Function.Surjective ⇑S
hS_anti : Topology.IsClosedEmbedding ⇑S
c : 𝕜
hc : 1 < ‖c‖
R : ℝ
hR : ‖c‖ < R
V : ℕ → Submodule 𝕜 X := fun n ↦ (LinearMap.iterateRange S) n
hV_succ : ∀ (n : ℕ), V (n + 1) = Submodule.map S (V n)
hV_closed : ∀ (n : ℕ), IsClosed ↑(V n)
n : ℕ
h₁ : IsClosed ↑(Submodule.comap (V n).subtype (V (n + 1)))
h₂ : ∃ x, x ∉ Submodule.comap (V n).subtype (V (n + 1))
x : X
hx : x ∈ V n
hxn : ‖⟨x, hx⟩‖ ≤ R
hxy : ∀ (a : X) (b : a ∈ V n), a ∈ V (n + 1) → 1 ≤ ‖⟨x, hx⟩ - ⟨a, b⟩‖
y : X
hy : y ∈ V (n + 1)
⊢ n ≤ n + 1

Tactic:
simp

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

Goal state before:
pp: 𝕜 : 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) μ
S : X →L[𝕜] X := T - μ • 1
K : NNReal
hK : AntilipschitzWith K ⇑S
h₂ : ¬Function.Surjective ⇑S
c : 𝕜
hc : 1 < ‖c‖
⊢ ‖c‖ < ‖c‖ + 1

Tactic:
simp

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 𝕜
inst✝ : DecidableEq n
hA : A.IsHermitian
⊢ A = ((conjStarAlgAut 𝕜 (Matrix n n 𝕜)) (hA.eigenvectorUnitary * star hA.eigenvectorUnitary)) A

Tactic:
simp

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 𝕜
inst✝ : DecidableEq n
hA : A.IsHermitian
⊢ (Finset.univ.val.bind fun i ↦ (Polynomial.X - Polynomial.C ↑(hA.eigenvalues i)).roots) =
    Multiset.map (RCLike.ofReal ∘ hA.eigenvalues) Finset.univ.val

Tactic:
simp

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 𝕜
inst✝ : DecidableEq n
hA : A.IsHermitian
⊢ Multiset.map (fun x ↦ ↑x)
      (Multiset.map hA.eigenvalues₀ (Multiset.map (⇑(Fintype.equivOfCardEq ⋯).symm) Finset.univ.val)) =
    Multiset.map RCLike.ofReal (Multiset.map hA.eigenvalues₀ Finset.univ.val)

Tactic:
simp

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 𝕜
inst✝ : DecidableEq n
hA : A.IsHermitian
⊢ List.Pairwise (fun a b ↦ a ≥ b) (List.ofFn fun x ↦ hA.eigenvalues₀ x)

Tactic:
← List.sortedGE_iff_pairwise

Goal state after:
𝕜 : Type u_1
inst✝² : RCLike 𝕜
n : Type u_2
inst✝¹ : Fintype n
A : Matrix n n 𝕜
inst✝ : DecidableEq n
hA : A.IsHermitian
⊢ (List.ofFn fun x ↦ hA.eigenvalues₀ x).SortedGE
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
x : 𝕜
⊢ x ∈
      spectrum 𝕜
        (((conjStarAlgAut 𝕜 (Matrix n n 𝕜)) hA.eigenvectorUnitary) (diagonal (RCLike.ofReal ∘ hA.eigenvalues))) ↔
    x ∈ RCLike.ofReal '' Set.range hA.eigenvalues

Tactic:
simp

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 𝕜
inst✝ : DecidableEq n
hA : A.IsHermitian
x : ℝ
⊢ (algebraMap ℝ 𝕜) x ∈
      spectrum 𝕜
        (((conjStarAlgAut 𝕜 (Matrix n n 𝕜)) hA.eigenvectorUnitary) (diagonal (RCLike.ofReal ∘ hA.eigenvalues))) ↔
    x ∈ Set.range hA.eigenvalues

Tactic:
simp

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
hT : T.IsSymmetric
μ : 𝕜
v : E
hv : v ∈ (eigenspace T μ)ᗮ
w : E
⊢ w ∈ eigenspace T μ → ⟪w, T v⟫ = 0

Tactic:
hw

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 : w ∈ eigenspace T μ
⊢ ⟪w, T v⟫ = 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.IsHermitian
⊢ A.PosDef ↔ ∀ (i : n), 0 < hA.eigenvalues i

Tactic:
conv_lhs => rw [hA.spectral_theorem]
  simp [isUnit_coe.posDef_star_right_conjugate_iff]

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

Goal state before:
pp: case pos
𝕜 : 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)
h✝ : n₂ ≤ n₁ ∧ K₁ ≤ K₂
a✝ : E
⊢ (ContDiffMapSupportedIn.of_support_subset ⋯ ⋯) a✝ =
    (ContDiffMapSupportedIn.of_support_subset ⋯ ⋯ + ContDiffMapSupportedIn.of_support_subset ⋯ ⋯) a✝

Tactic:
simp

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

Goal state before:
pp: case neg
𝕜 : 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)
h✝ : ¬(n₂ ≤ n₁ ∧ K₁ ≤ K₂)
a✝ : E
⊢ 0 a✝ = (0 + 0) a✝

Tactic:
simp

Goal state after: