mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Function.Holder

Goal state before:
pp: α : Type u_1
𝕜 : Type u_3
E : Type u_4
m : MeasurableSpace α
μ : Measure α
p q r : ℝ≥0∞
hpqr : p.HolderTriple q r
inst✝³ : NormedRing 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : IsBoundedSMul 𝕜 E
f : ↥(Lp 𝕜 p μ)
⊢ f • 0 = 0

Tactic:
convert! MemLp.zero (ε := E) |>.toLp_zero

Goal state after:
case e'_2
α : Type u_1
𝕜 : Type u_3
E : Type u_4
m : MeasurableSpace α
μ : Measure α
p q r : ℝ≥0∞
hpqr : p.HolderTriple q r
inst✝³ : NormedRing 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : IsBoundedSMul 𝕜 E
f : ↥(Lp 𝕜 p μ)
⊢ f • 0 = MemLp.toLp 0 ⋯
Module: Mathlib.MeasureTheory.Function.Holder

Goal state before:
pp: α : Type u_1
𝕜 : Type u_3
E : Type u_4
m : MeasurableSpace α
μ : Measure α
p q r : ℝ≥0∞
hpqr : p.HolderTriple q r
inst✝³ : NormedRing 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : IsBoundedSMul 𝕜 E
f : ↥(Lp E q μ)
⊢ 0 • f = 0

Tactic:
convert! MemLp.zero (ε := E) |>.toLp_zero

Goal state after:
case e'_2
α : Type u_1
𝕜 : Type u_3
E : Type u_4
m : MeasurableSpace α
μ : Measure α
p q r : ℝ≥0∞
hpqr : p.HolderTriple q r
inst✝³ : NormedRing 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : IsBoundedSMul 𝕜 E
f : ↥(Lp E q μ)
⊢ 0 • f = MemLp.toLp 0 ⋯
Module: Mathlib.MeasureTheory.Integral.Layercake

Goal state before:
pp: case hfi
α : Type u_1
inst✝ : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
μ : Measure α
f_nn : 0 ≤ f
f_mble : Measurable f
g_intble : ∀ t > 0, IntervalIntegrable g volume 0 t
g_mble : Measurable g
g_nn : ∀ t > 0, 0 ≤ g t
f_nonneg : ∀ (ω : α), 0 ≤ f ω
H1 : ¬g =ᵐ[volume.restrict (Ioi 0)] 0
s : ℝ
s_pos : s > 0
hs : 0 < ∫ (x : ℝ) in Ioc 0 s, g x ∂volume
h's : μ {a | s < f a} = ∞
A : ∫⁻ (t : ℝ) in Ioi 0, μ {a | t ≤ f a} * ENNReal.ofReal (g t) = ∞
a : α
ha : a ∈ {a | s < f a}
⊢ IntervalIntegrable g volume 0 (f a)

Tactic:
exact g_intble _ (s_pos.trans ha)

Goal state after:
Module: Mathlib.MeasureTheory.Integral.Layercake

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
μ : Measure α
f_nn : 0 ≤ f
f_mble : Measurable f
g_intble : ∀ t > 0, IntervalIntegrable g volume 0 t
g_mble : Measurable g
g_nn : ∀ t > 0, 0 ≤ g t
f_nonneg : ∀ (ω : α), 0 ≤ f ω
H2 : ∀ s > 0, 0 < ∫ (t : ℝ) in 0..s, g t → μ {a | s < f a} ≠ ∞
H1 : ¬BddAbove {s | g =ᵐ[volume.restrict (Ioc 0 s)] 0}
⊢ ∀ (n : ℕ), g =ᵐ[volume.restrict (Ioc 0 ↑n)] 0

Tactic:
intro n

Goal state after:
α : Type u_1
inst✝ : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
μ : Measure α
f_nn : 0 ≤ f
f_mble : Measurable f
g_intble : ∀ t > 0, IntervalIntegrable g volume 0 t
g_mble : Measurable g
g_nn : ∀ t > 0, 0 ≤ g t
f_nonneg : ∀ (ω : α), 0 ≤ f ω
H2 : ∀ s > 0, 0 < ∫ (t : ℝ) in 0..s, g t → μ {a | s < f a} ≠ ∞
H1 : ¬BddAbove {s | g =ᵐ[volume.restrict (Ioc 0 s)] 0}
n : ℕ
⊢ g =ᵐ[volume.restrict (Ioc 0 ↑n)] 0
Module: Mathlib.MeasureTheory.Integral.Layercake

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
μ : Measure α
f_nn : 0 ≤ f
f_mble : Measurable f
g_intble : ∀ t > 0, IntervalIntegrable g volume 0 t
g_mble : Measurable g
g_nn : ∀ t > 0, 0 ≤ g t
f_nonneg : ∀ (ω : α), 0 ≤ f ω
H1 : ¬g =ᵐ[volume.restrict (Ioi 0)] 0
H2 : ∀ s > 0, 0 < ∫ (t : ℝ) in 0..s, g t → μ {a | s < f a} ≠ ∞
M_bdd : BddAbove {s | g =ᵐ[volume.restrict (Ioc 0 s)] 0}
M : ℝ := sSup {s | g =ᵐ[volume.restrict (Ioc 0 s)] 0}
zero_mem : 0 ∈ {s | g =ᵐ[volume.restrict (Ioc 0 s)] 0}
M_nonneg : 0 ≤ M
u : ℕ → ℝ
uM : ∀ (n : ℕ), u n < M
ulim : Tendsto u atTop (𝓝 M)
⊢ ∀ (n : ℕ), g =ᵐ[volume.restrict (Ioc 0 (u n))] 0

Tactic:
intro n

Goal state after:
α : Type u_1
inst✝ : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
μ : Measure α
f_nn : 0 ≤ f
f_mble : Measurable f
g_intble : ∀ t > 0, IntervalIntegrable g volume 0 t
g_mble : Measurable g
g_nn : ∀ t > 0, 0 ≤ g t
f_nonneg : ∀ (ω : α), 0 ≤ f ω
H1 : ¬g =ᵐ[volume.restrict (Ioi 0)] 0
H2 : ∀ s > 0, 0 < ∫ (t : ℝ) in 0..s, g t → μ {a | s < f a} ≠ ∞
M_bdd : BddAbove {s | g =ᵐ[volume.restrict (Ioc 0 s)] 0}
M : ℝ := sSup {s | g =ᵐ[volume.restrict (Ioc 0 s)] 0}
zero_mem : 0 ∈ {s | g =ᵐ[volume.restrict (Ioc 0 s)] 0}
M_nonneg : 0 ≤ M
u : ℕ → ℝ
uM : ∀ (n : ℕ), u n < M
ulim : Tendsto u atTop (𝓝 M)
n : ℕ
⊢ g =ᵐ[volume.restrict (Ioc 0 (u n))] 0
Module: Mathlib.MeasureTheory.Integral.Layercake

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
μ : Measure α
f_nn : 0 ≤ f
f_mble : Measurable f
g_intble : ∀ t > 0, IntervalIntegrable g volume 0 t
g_mble : Measurable g
g_nn : ∀ t > 0, 0 ≤ g t
f_nonneg : ∀ (ω : α), 0 ≤ f ω
H1 : ¬g =ᵐ[volume.restrict (Ioi 0)] 0
H2 : ∀ s > 0, 0 < ∫ (t : ℝ) in 0..s, g t → μ {a | s < f a} ≠ ∞
M_bdd : BddAbove {s | g =ᵐ[volume.restrict (Ioc 0 s)] 0}
M : ℝ := sSup {s | g =ᵐ[volume.restrict (Ioc 0 s)] 0}
zero_mem : 0 ∈ {s | g =ᵐ[volume.restrict (Ioc 0 s)] 0}
M_nonneg : 0 ≤ M
hgM : g =ᵐ[volume.restrict (Ioc 0 M)] 0
ν : Measure α := μ.restrict {a | M < f a}
u : ℕ → ℝ
uM : ∀ (n : ℕ), M < u n
ulim : Tendsto u atTop (𝓝 M)
⊢ ∀ (i : ℕ), ν ({a | f a ≤ M} ∪ {a | u i < f a}) < ∞

Tactic:
intro n

Goal state after:
α : Type u_1
inst✝ : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
μ : Measure α
f_nn : 0 ≤ f
f_mble : Measurable f
g_intble : ∀ t > 0, IntervalIntegrable g volume 0 t
g_mble : Measurable g
g_nn : ∀ t > 0, 0 ≤ g t
f_nonneg : ∀ (ω : α), 0 ≤ f ω
H1 : ¬g =ᵐ[volume.restrict (Ioi 0)] 0
H2 : ∀ s > 0, 0 < ∫ (t : ℝ) in 0..s, g t → μ {a | s < f a} ≠ ∞
M_bdd : BddAbove {s | g =ᵐ[volume.restrict (Ioc 0 s)] 0}
M : ℝ := sSup {s | g =ᵐ[volume.restrict (Ioc 0 s)] 0}
zero_mem : 0 ∈ {s | g =ᵐ[volume.restrict (Ioc 0 s)] 0}
M_nonneg : 0 ≤ M
hgM : g =ᵐ[volume.restrict (Ioc 0 M)] 0
ν : Measure α := μ.restrict {a | M < f a}
u : ℕ → ℝ
uM : ∀ (n : ℕ), M < u n
ulim : Tendsto u atTop (𝓝 M)
n : ℕ
⊢ ν ({a | f a ≤ M} ∪ {a | u n < f a}) < ∞
Module: Mathlib.Analysis.Distribution.TemperateGrowth

Goal state before:
pp: case h
E : Type u_5
F : Type u_6
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → F
hf_temperate : HasTemperateGrowth f
N : ℕ
k : ℕ → ℕ
hk : ∀ (n : ℕ), iteratedFDeriv ℝ n f =O[⊤] fun x ↦ (1 + ‖x‖) ^ k n
⊢ ∀ n ≤ N, iteratedFDeriv ℝ n f =O[⊤] fun x ↦ (1 + ‖x‖) ^ (Finset.range (N + 1)).sup k

Tactic:
intro n

Goal state after:
case h
E : Type u_5
F : Type u_6
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → F
hf_temperate : HasTemperateGrowth f
N : ℕ
k : ℕ → ℕ
hk : ∀ (n : ℕ), iteratedFDeriv ℝ n f =O[⊤] fun x ↦ (1 + ‖x‖) ^ k n
n : ℕ
⊢ n ≤ N → iteratedFDeriv ℝ n f =O[⊤] fun x ↦ (1 + ‖x‖) ^ (Finset.range (N + 1)).sup k
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 : ℕ∞
V : Type u_6
inst✝⁸ : AddCommGroup V
inst✝⁷ : Module ℝ V
t : TopologicalSpace V
inst✝⁶ : IsTopologicalAddGroup V
inst✝⁵ : ContinuousSMul ℝ V
inst✝⁴ : LocallyConvexSpace ℝ V
inst✝³ : Algebra ℝ 𝕜
inst✝² : IsScalarTower ℝ 𝕜 F
inst✝¹ : Module 𝕜 V
inst✝ : IsScalarTower ℝ 𝕜 V
f : 𝓓^{n}(Ω, F) →ₗ[𝕜] V
this✝ : IsTopologicalAddGroup 𝓓^{n}(Ω, F)
this : ContinuousSMul ℝ 𝓓^{n}(Ω, F)
⊢ topologicalSpace Ω F n ≤ induced (⇑(↑ℝ f)) t ↔
    ∀ (K : Compacts E) (K_sub_Ω : ↑K ⊆ ↑Ω), Continuous[_, t] (⇑(↑ℝ f) ∘ ofSupportedIn K_sub_Ω)

Tactic:
have : @LocallyConvexSpace ℝ _ _ _ _ _ (induced (f.restrictScalars ℝ) t) := .induced _

Goal state after:
𝕜 : 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 : ℕ∞
V : Type u_6
inst✝⁸ : AddCommGroup V
inst✝⁷ : Module ℝ V
t : TopologicalSpace V
inst✝⁶ : IsTopologicalAddGroup V
inst✝⁵ : ContinuousSMul ℝ V
inst✝⁴ : LocallyConvexSpace ℝ V
inst✝³ : Algebra ℝ 𝕜
inst✝² : IsScalarTower ℝ 𝕜 F
inst✝¹ : Module 𝕜 V
inst✝ : IsScalarTower ℝ 𝕜 V
f : 𝓓^{n}(Ω, F) →ₗ[𝕜] V
this✝¹ : IsTopologicalAddGroup 𝓓^{n}(Ω, F)
this✝ : ContinuousSMul ℝ 𝓓^{n}(Ω, F)
this : LocallyConvexSpace ℝ 𝓓^{n}(Ω, F)
⊢ topologicalSpace Ω F n ≤ induced (⇑(↑ℝ f)) t ↔
    ∀ (K : Compacts E) (K_sub_Ω : ↑K ⊆ ↑Ω), Continuous[_, t] (⇑(↑ℝ f) ∘ ofSupportedIn K_sub_Ω)
Module: Mathlib.Analysis.Distribution.TemperateGrowth

Goal state before:
pp: case h
E : Type u_5
F : Type u_6
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f g : E → F
hf : ContDiff ℝ ∞ f ∧ ∀ (n : ℕ), ∃ k, iteratedFDeriv ℝ n f =O[⊤] fun x ↦ (1 + ‖x‖) ^ k
hg : ContDiff ℝ ∞ g ∧ ∀ (n : ℕ), ∃ k, iteratedFDeriv ℝ n g =O[⊤] fun x ↦ (1 + ‖x‖) ^ k
n k₁ : ℕ
h₁ : iteratedFDeriv ℝ n f =O[⊤] fun x ↦ (1 + ‖x‖) ^ k₁
k₂ : ℕ
h₂ : iteratedFDeriv ℝ n g =O[⊤] fun x ↦ (1 + ‖x‖) ^ k₂
this : 1 ≤ᶠ[⊤] fun x ↦ 1 + ‖x‖
⊢ (iteratedFDeriv ℝ n f + iteratedFDeriv ℝ n g) =O[⊤] fun x ↦ (1 + ‖x‖) ^ max k₁ k₂

Tactic:
exact (h₁.trans (IsBigO.pow_of_le_right this (k₁.le_max_left k₂))).add
    (h₂.trans (IsBigO.pow_of_le_right this (k₁.le_max_right k₂)))

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

Goal state before:
pp: case right
𝕜 : Type u_2
D : Type u_4
E : Type u_5
F : Type u_6
G : Type u_7
inst✝¹² : NormedAddCommGroup E
inst✝¹¹ : NormedSpace ℝ E
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NormedSpace ℝ F
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NormedAlgebra ℝ 𝕜
inst✝⁶ : NormedAddCommGroup D
inst✝⁵ : NormedSpace ℝ D
inst✝⁴ : NormedAddCommGroup G
inst✝³ : NormedSpace ℝ G
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedSpace 𝕜 G
inst✝ : NormedSpace 𝕜 E
B : E →L[𝕜] F →L[𝕜] G
f : D → E
g : D → F
hf : HasTemperateGrowth f
hg : HasTemperateGrowth g
⊢ ∀ (n : ℕ), ∃ k, (iteratedFDeriv ℝ n fun x ↦ (B (f x)) (g x)) =O[⊤] fun x ↦ (1 + ‖x‖) ^ k

Tactic:
intro n

Goal state after:
case right
𝕜 : Type u_2
D : Type u_4
E : Type u_5
F : Type u_6
G : Type u_7
inst✝¹² : NormedAddCommGroup E
inst✝¹¹ : NormedSpace ℝ E
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NormedSpace ℝ F
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NormedAlgebra ℝ 𝕜
inst✝⁶ : NormedAddCommGroup D
inst✝⁵ : NormedSpace ℝ D
inst✝⁴ : NormedAddCommGroup G
inst✝³ : NormedSpace ℝ G
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedSpace 𝕜 G
inst✝ : NormedSpace 𝕜 E
B : E →L[𝕜] F →L[𝕜] G
f : D → E
g : D → F
hf : HasTemperateGrowth f
hg : HasTemperateGrowth g
n : ℕ
⊢ ∃ k, (iteratedFDeriv ℝ n fun x ↦ (B (f x)) (g x)) =O[⊤] fun x ↦ (1 + ‖x‖) ^ k
Module: Mathlib.Analysis.Distribution.TemperateGrowth

Goal state before:
pp: case h
H : Type u_8
inst✝¹ : NormedAddCommGroup H
inst✝ : InnerProductSpace ℝ H
r : ℝ
t : Set ℝ := ⋯
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 ≤ N,
    ∀ x ∈ t,
      ‖iteratedFDerivWithin ℝ n (fun x ↦ x ^ r) t x‖ ≤
        (∑ k ∈ Finset.range (N + 1), ‖Polynomial.eval r (descPochhammer ℝ k)‖) * (1 + ‖x‖) ^ k

Tactic:
intro n

Goal state after:
case h
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 : ℕ
⊢ n ≤ N →
    ∀ x ∈ t,
      ‖iteratedFDerivWithin ℝ n (fun x ↦ x ^ r) t x‖ ≤
        (∑ k ∈ Finset.range (N + 1), ‖Polynomial.eval r (descPochhammer ℝ k)‖) * (1 + ‖x‖) ^ k
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
⊢ HasEigenvalue T ↑(⨆ x, re ⟪T ↑x, ↑x⟫_𝕜 / ‖↑x‖ ^ 2)

Tactic:
have := FiniteDimensional.proper_rclike 𝕜 E
  let T' := hT.toSelfAdjoint
  obtain ⟨x, hx⟩ : ∃ x : E, x ≠ 0 := exists_ne 0
  have H₁ : IsCompact (sphere (0 : E) ‖x‖) := isCompact_sphere _ _
  have H₂ : (sphere (0 : E) ‖x‖).Nonempty := ⟨x, by simp⟩
  -- key point: in finite dimension, a continuous function on the sphere has a max
  obtain ⟨x₀, hx₀', hTx₀⟩ :=
    H₁.exists_isMaxOn H₂ T'.val.reApplyInnerSelf_continuous.continuousOn
  have hx₀ : ‖x₀‖ = ‖x‖ := by simpa using hx₀'
  have : IsMaxOn T'.val.reApplyInnerSelf (sphere 0 ‖x₀‖) x₀ := by simpa only [← hx₀] using hTx₀
  have hx₀_ne : x₀ ≠ 0 := by
    have : ‖x₀‖ ≠ 0 := by simp only [hx₀, norm_eq_zero, hx, Ne, not_false_iff]
    simpa [← norm_eq_zero, Ne]
  exact hasEigenvalue_of_hasEigenvector (T'.prop.hasEigenvector_of_isMaxOn hx₀_ne this)

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‖
c : ℝ
hc₀ : c > 0
hc : ∀ ε > 0, ∃ x, ‖x‖ ≤ 1 ∧ c ≤ ‖x‖ ∧ ‖(T - μ • 1) x‖ < ε
φ : ℕ → ℝ
hφ_anti : StrictAnti φ
hφ_pos : ∀ (n : ℕ), 0 < φ n
hφ : Tendsto φ atTop (𝓝 0)
x : ℕ → X
hx_norm_upper : ∀ (n : ℕ), ‖x n‖ ≤ 1
hx_norm_lower : ∀ (n : ℕ), c ≤ ‖x n‖
hx_bound : ∀ (n : ℕ), ‖(T - μ • 1) (x n)‖ < φ n
hx_lim : Tendsto (fun n ↦ (T - μ • 1) (x n)) atTop (𝓝 0)
y_ : ℕ → X := fun n ↦ T (x n)
n : ℕ
hn : φ n ≤ ‖μ‖ * c / 2
⊢ ‖μ‖ * c / 2 ≤ ‖y_ n‖

Tactic:
have h₁ : ‖T (x n) - μ • x n‖ < φ n := by simpa using hx_bound n

Goal state after:
𝕜 : 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‖
c : ℝ
hc₀ : c > 0
hc : ∀ ε > 0, ∃ x, ‖x‖ ≤ 1 ∧ c ≤ ‖x‖ ∧ ‖(T - μ • 1) x‖ < ε
φ : ℕ → ℝ
hφ_anti : StrictAnti φ
hφ_pos : ∀ (n : ℕ), 0 < φ n
hφ : Tendsto φ atTop (𝓝 0)
x : ℕ → X
hx_norm_upper : ∀ (n : ℕ), ‖x n‖ ≤ 1
hx_norm_lower : ∀ (n : ℕ), c ≤ ‖x n‖
hx_bound : ∀ (n : ℕ), ‖(T - μ • 1) (x n)‖ < φ n
hx_lim : Tendsto (fun n ↦ (T - μ • 1) (x n)) atTop (𝓝 0)
y_ : ℕ → X := fun n ↦ T (x n)
n : ℕ
hn : φ n ≤ ‖μ‖ * c / 2
h₁ : ‖T (x n) - μ • x n‖ < φ n
⊢ ‖μ‖ * c / 2 ≤ ‖y_ n‖
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
⊢ (spectrum ℝ A).Finite

Tactic:
rw [← spectrum.preimage_algebraMap 𝕜]
  exact A.finite_spectrum.preimage (FaithfulSMul.algebraMap_injective ℝ 𝕜).injOn

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 ∈ ⨅ i, (eigenspace T i)ᗮ
⊢ T v ∈ ⨅ i, (eigenspace T i)ᗮ

Tactic:
exact T.iInf_invariant hT.invariant_orthogonalComplement_eigenspace v hv

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 (RCLike.ofReal ∘ ⇑f ∘ fun i ↦ ⟨ha.eigenvalues i, ⋯⟩))ᴴ =
    ((conjStarAlgAut 𝕜 (Matrix n n 𝕜)) ha.eigenvectorUnitary)
      (diagonal (RCLike.ofReal ∘ ⇑f ∘ fun i ↦ ⟨ha.eigenvalues i, ⋯⟩))

Tactic:
diagonal_conjTranspose

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
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : SMulCommClass ℝ 𝕜 F
K : Compacts E
i : ℕ
f : 𝓓_{K}(E, F)
⊢ ⇑((structureMapLM 𝕜 ⊤ i) f) = iteratedFDeriv ℝ i ⇑f

Tactic:
simp [structureMapLM_eq]

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

Goal state before:
pp: 𝕜 : Type u_1
n : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n 𝕜
⊢ A.PosSemidef ↔ A.IsHermitian ∧ spectrum 𝕜 A ⊆ {a | 0 ≤ a}

Tactic:
refine ⟨fun h => ⟨h.isHermitian, fun a => ?_⟩, fun ⟨h1, h2⟩ => ?_⟩
  · simp only [h.isHermitian.spectrum_eq_image_range, Set.mem_image, Set.mem_range,
      exists_exists_eq_and, Set.mem_ofPred_eq, forall_exists_index]
    rintro i rfl
    exact_mod_cast h.eigenvalues_nonneg _
  · rw [h1.posSemidef_iff_eigenvalues_nonneg]
    intro i
    simpa [h1.spectrum_eq_image_range] using @h2 (h1.eigenvalues i)

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

Goal state before:
pp: E : Type u_1
n : Type u_2
𝕜 : Type u_4
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : Finite n
v : n → E
h_li : LinearIndependent 𝕜 v
⊢ (gram 𝕜 v).PosDef

Tactic:
have := Fintype.ofFinite n
  rw [Fintype.linearIndependent_iff] at h_li
  refine .of_dotProduct_mulVec_pos (isHermitian_gram _ _) fun x hx ↦
    ((posSemidef_gram ..).dotProduct_mulVec_nonneg _).lt_of_ne' ?_
  rw [star_dotProduct_gram_mulVec, inner_self_eq_zero.ne]
  exact mt (h_li x) (mt funext hx)

Goal state after:
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
i : ℕ
h₁ : n₁ = n₂
h₂ : K₁ ≤ K₂
f : 𝓓^{n₁}_{K₁}(E, F)
⊢ (ContDiffMapSupportedIn.seminorm 𝕜 E F n₂ K₂ i) ((monoLM 𝕜) f) = (ContDiffMapSupportedIn.seminorm 𝕜 E F n₁ K₁ i) f

Tactic:
simp [BoundedContinuousFunction.norm_eq_iSup_norm, ContDiffMapSupportedIn.seminorm_apply,
    structureMapCLM_apply, h₁, h₂]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Abs

Goal state before:
pp: case ofNat
A : Type u_2
inst✝¹⁰ : Ring A
inst✝⁹ : StarRing A
inst✝⁸ : TopologicalSpace A
inst✝⁷ : Algebra ℝ A
inst✝⁶ : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝⁵ : PartialOrder A
inst✝⁴ : StarOrderedRing A
inst✝³ : NonnegSpectrumClass ℝ A
inst✝² : IsTopologicalRing A
inst✝¹ : T2Space A
inst✝ : StarModule ℝ A
a✝ : ℕ
⊢ abs ↑(Int.ofNat a✝) = ↑|Int.ofNat a✝|

Tactic:
| ofNat _ =>

Goal state after:
Module: Mathlib.MeasureTheory.Function.ContinuousMapDense

Goal state before:
pp: α : Type u_1
inst✝⁸ : TopologicalSpace α
inst✝⁷ : NormalSpace α
inst✝⁶ : MeasurableSpace α
inst✝⁵ : BorelSpace α
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
μ : Measure α
p : ℝ≥0∞
inst✝³ : NormedSpace ℝ E
inst✝² : R1Space α
inst✝¹ : WeaklyLocallyCompactSpace α
inst✝ : μ.Regular
hp : p ≠ ∞
f : α → E
hf : MemLp f p μ
ε✝ : ℝ≥0∞
hε✝ : ε✝ ≠ 0
c : E
t : Set α
ht : MeasurableSet t
htμ : μ t < ∞
ε : ℝ≥0∞
hε : ε ≠ 0
δ : ℝ≥0∞
δpos : 0 < δ
hδ :
  ∀ (f g : α → E),
    AEStronglyMeasurable f μ →
      AEStronglyMeasurable g μ → eLpNorm f p μ ≤ δ → eLpNorm g p μ ≤ δ → eLpNorm (f + g) p μ < ε
η : ℝ≥0
ηpos : 0 < η
hη : ∀ (s : Set α), μ s ≤ ↑η → eLpNorm (s.indicator fun _x ↦ c) p μ ≤ δ
hη_pos' : 0 < ↑η
s : Set α
st : s ⊆ t
s_compact : IsCompact s
s_closed : IsClosed[inst✝⁸] s
μs : μ (t \ s) < ↑η
hsμ : μ s < ∞
I1 : eLpNorm ((s.indicator fun _y ↦ c) - t.indicator fun _y ↦ c) p μ ≤ δ
k : Set α
k_compact : IsCompact k
sk : s ⊆ interior k
⊢ ∃ g,
    eLpNorm (g - t.indicator fun x ↦ c) p μ ≤ ε ∧
      Continuous[inst✝⁸, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] g ∧ MemLp g p μ ∧ HasCompactSupport g

Tactic:
rcases exists_continuous_eLpNorm_sub_le_of_closed hp s_closed isOpen_interior sk hsμ.ne c δpos.ne'
    with ⟨f, f_cont, I2, _f_bound, f_support, f_mem⟩

Goal state after:
α : Type u_1
inst✝⁸ : TopologicalSpace α
inst✝⁷ : NormalSpace α
inst✝⁶ : MeasurableSpace α
inst✝⁵ : BorelSpace α
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
μ : Measure α
p : ℝ≥0∞
inst✝³ : NormedSpace ℝ E
inst✝² : R1Space α
inst✝¹ : WeaklyLocallyCompactSpace α
inst✝ : μ.Regular
hp : p ≠ ∞
f✝ : α → E
hf : MemLp f✝ p μ
ε✝ : ℝ≥0∞
hε✝ : ε✝ ≠ 0
c : E
t : Set α
ht : MeasurableSet t
htμ : μ t < ∞
ε : ℝ≥0∞
hε : ε ≠ 0
δ : ℝ≥0∞
δpos : 0 < δ
hδ :
  ∀ (f g : α → E),
    AEStronglyMeasurable f μ →
      AEStronglyMeasurable g μ → eLpNorm f p μ ≤ δ → eLpNorm g p μ ≤ δ → eLpNorm (f + g) p μ < ε
η : ℝ≥0
ηpos : 0 < η
hη : ∀ (s : Set α), μ s ≤ ↑η → eLpNorm (s.indicator fun _x ↦ c) p μ ≤ δ
hη_pos' : 0 < ↑η
s : Set α
st : s ⊆ t
s_compact : IsCompact s
s_closed : IsClosed[inst✝⁸] s
μs : μ (t \ s) < ↑η
hsμ : μ s < ∞
I1 : eLpNorm ((s.indicator fun _y ↦ c) - t.indicator fun _y ↦ c) p μ ≤ δ
k : Set α
k_compact : IsCompact k
sk : s ⊆ interior k
f : α → E
f_cont : Continuous[inst✝⁸, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
I2 : eLpNorm (fun x ↦ f x - s.indicator (fun _y ↦ c) x) p μ ≤ δ
_f_bound : ∀ (x : α), ‖f x‖ ≤ ‖c‖
f_support : Function.support f ⊆ interior k
f_mem : MemLp f p μ
⊢ ∃ g,
    eLpNorm (g - t.indicator fun x ↦ c) p μ ≤ ε ∧
      Continuous[inst✝⁸, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] g ∧ MemLp g p μ ∧ HasCompactSupport g
Module: Mathlib.Analysis.Normed.Module.Bases

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
X : Type u_2
inst✝¹ : NormedAddCommGroup X
inst✝ : NormedSpace 𝕜 X
β : Type u_3
L : SummationFilter β
b : SchauderBasis 𝕜 X
D : RankOneDecomposition 𝕜 X
coeff : ℕ → X → 𝕜 := D.basisCoeff
hcoeff : ∀ (n : ℕ) (x : X), (succSub D.P n) x = coeff n x • D.e n
n : ℕ
c : 𝕜
x : X
⊢ (fun x ↦ x • D.e n) (coeff n (c • x)) = (fun x ↦ x • D.e n) ((RingHom.id 𝕜) c • coeff n x)

Tactic:
dsimp only [RingHom.id_apply]

Goal state after:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
X : Type u_2
inst✝¹ : NormedAddCommGroup X
inst✝ : NormedSpace 𝕜 X
β : Type u_3
L : SummationFilter β
b : SchauderBasis 𝕜 X
D : RankOneDecomposition 𝕜 X
coeff : ℕ → X → 𝕜 := D.basisCoeff
hcoeff : ∀ (n : ℕ) (x : X), (succSub D.P n) x = coeff n x • D.e n
n : ℕ
c : 𝕜
x : X
⊢ coeff n (c • x) • D.e n = (c • coeff n x) • D.e n
Module: Mathlib.Analysis.Normed.Module.Bases

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
X : Type u_2
inst✝¹ : NormedAddCommGroup X
inst✝ : NormedSpace 𝕜 X
β : Type u_3
L : SummationFilter β
b : SchauderBasis 𝕜 X
D : RankOneDecomposition 𝕜 X
coeff : ℕ → X → 𝕜 := D.basisCoeff
hcoeff : ∀ (n : ℕ) (x : X), (succSub D.P n) x = coeff n x • D.e n
n : ℕ
c : 𝕜
x : X
⊢ (succSub D.P n) (c • x) = c • (succSub D.P n) x

Tactic:
map_smul

Goal state after:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
X : Type u_2
inst✝¹ : NormedAddCommGroup X
inst✝ : NormedSpace 𝕜 X
β : Type u_3
L : SummationFilter β
b : SchauderBasis 𝕜 X
D : RankOneDecomposition 𝕜 X
coeff : ℕ → X → 𝕜 := D.basisCoeff
hcoeff : ∀ (n : ℕ) (x : X), (succSub D.P n) x = coeff n x • D.e n
n : ℕ
c : 𝕜
x : X
⊢ c • (succSub D.P n) x = c • (succSub D.P n) x
Module: Mathlib.Analysis.Normed.Module.Bases

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
X : Type u_2
inst✝¹ : NormedAddCommGroup X
inst✝ : NormedSpace 𝕜 X
D : RankOneDecomposition 𝕜 X
n : ℕ
x✝¹ : X
i : ℕ
x✝ : i ∈ Finset.range n
⊢ D.basisCoeff i x✝¹ • D.e i = (succSub D.P i) x✝¹

Tactic:
rw [basisCoeff_spec]

Goal state after: