mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Integral.Layercake

Goal state before:
pp: case neg
α : Type u_1
inst✝¹ : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
μ : Measure α
inst✝ : SFinite μ
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
g_intble' : ∀ (t : ℝ), 0 ≤ t → IntervalIntegrable g volume 0 t
integrand_eq : ∀ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0..f ω, g t) = ∫⁻ (t : ℝ) in Ioc 0 (f ω), ENNReal.ofReal (g t)
p_fst : α
p_snd : ℝ
h : p_snd ∉ Ioc 0 (f p_fst)
h' : (p_fst, p_snd) ∉ {p | p.2 ∈ Ioc 0 (f p.1)}
⊢ (Ioc 0 (f p_fst)).indicator (fun t ↦ ENNReal.ofReal (g t)) p_snd = 0

Tactic:
Set.indicator_of_notMem h

Goal state after:
case neg
α : Type u_1
inst✝¹ : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
μ : Measure α
inst✝ : SFinite μ
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
g_intble' : ∀ (t : ℝ), 0 ≤ t → IntervalIntegrable g volume 0 t
integrand_eq : ∀ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0..f ω, g t) = ∫⁻ (t : ℝ) in Ioc 0 (f ω), ENNReal.ofReal (g t)
p_fst : α
p_snd : ℝ
h : p_snd ∉ Ioc 0 (f p_fst)
h' : (p_fst, p_snd) ∉ {p | p.2 ∈ Ioc 0 (f p.1)}
⊢ 0 = 0
Module: Mathlib.MeasureTheory.Integral.Layercake

Goal state before:
pp: case pos
α : 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} = ∞
⊢ ∫⁻ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0..f ω, g t) ∂μ = ∫⁻ (t : ℝ) in Ioi 0, μ {a | t ≤ f a} * ENNReal.ofReal (g t)

Tactic:
rcases H2 with ⟨s, s_pos, hs, h's⟩
    rw [intervalIntegral.integral_of_le s_pos.le] at hs
    /- The first integral is infinite, as for `t ∈ [0, s]` one has `μ {a : α | t ≤ f a} = ∞`,
    and moreover the additional integral `g` is not uniformly zero. -/
    have A : ∫⁻ t in Ioi 0, μ {a : α | t ≤ f a} * ENNReal.ofReal (g t) = ∞ := by
      rw [eq_top_iff]
      calc
      ∞ = ∫⁻ t in Ioc 0 s, ∞ * ENNReal.ofReal (g t) := by
          have I_pos : ∫⁻ (a : ℝ) in Ioc 0 s, ENNReal.ofReal (g a) ≠ 0 := by
            rw [← ofReal_integral_eq_lintegral_ofReal (g_intble s s_pos).1]
            · simpa only [not_lt, ne_eq, ENNReal.ofReal_eq_zero, not_le] using hs
            · filter_upwards [ae_restrict_mem measurableSet_Ioc] with t ht using g_nn _ ht.1
          rw [lintegral_const_mul, ENNReal.top_mul I_pos]
          exact ENNReal.measurable_ofReal.comp g_mble
      _ ≤ ∫⁻ t in Ioc 0 s, μ {a : α | t ≤ f a} * ENNReal.ofReal (g t) := by
          apply setLIntegral_mono' measurableSet_Ioc (fun x hx ↦ ?_)
          rw [← h's]
          gcongr
          exact fun ha ↦ hx.2.trans (le_of_lt ha)
      _ ≤ ∫⁻ t in Ioi 0, μ {a : α | t ≤ f a} * ENNReal.ofReal (g t) :=
          lintegral_mono_set Ioc_subset_Ioi_self
    /- The second integral is infinite, as one integrates among other things on those `ω` where
    `f ω > s`: this is an infinite measure set, and on it the integrand is bounded below
    by `∫ t in 0..s, g t` which is positive. -/
    have B : ∫⁻ ω, ENNReal.ofReal (∫ t in 0..f ω, g t) ∂μ = ∞ := by
      rw [eq_top_iff]
      calc
      ∞ = ∫⁻ _ in {a | s < f a}, ENNReal.ofReal (∫ t in 0..s, g t) ∂μ := by
          simp only [lintegral_const, MeasurableSet.univ, Measure.restrict_apply, univ_inter,
            h's]
          rw [ENNReal.mul_top]
          simpa [intervalIntegral.integral_of_le s_pos.le] using hs
      _ ≤ ∫⁻ ω in {a | s < f a}, ENNReal.ofReal (∫ t in 0..f ω, g t) ∂μ := by
          apply setLIntegral_mono' (measurableSet_lt measurable_const f_mble) (fun a ha ↦ ?_)
          apply ENNReal.ofReal_le_ofReal
          apply intervalIntegral.integral_mono_interval le_rfl s_pos.le (le_of_lt ha)
          · filter_upwards [ae_restrict_mem measurableSet_Ioc] with t ht using g_nn _ ht.1
          · exact g_intble _ (s_pos.trans ha)
      _ ≤ ∫⁻ ω, ENNReal.ofReal (∫ t in 0..f ω, g t) ∂μ := setLIntegral_le_lintegral _ _
    rw [A, B]

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

Goal state before:
pp: case succ
R : Type u_3
E : Type u_5
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedRing R
inst✝ : NormedAlgebra ℝ R
f : E → R
hf : HasTemperateGrowth f
k : ℕ
IH : HasTemperateGrowth (f ^ k)
⊢ HasTemperateGrowth (f ^ (k + 1))

Tactic:
rw [pow_succ]

Goal state after:
case succ
R : Type u_3
E : Type u_5
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedRing R
inst✝ : NormedAlgebra ℝ R
f : E → R
hf : HasTemperateGrowth f
k : ℕ
IH : HasTemperateGrowth (f ^ k)
⊢ HasTemperateGrowth (f ^ k * f)
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) μ
h₂ : μ ∉ resolventSet 𝕜 T
⊢ False

Tactic:
let S := T - μ • 1

Goal state after:
𝕜 : 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) μ
h₂ : μ ∉ resolventSet 𝕜 T
S : X →L[𝕜] X := T - μ • 1
⊢ False
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.ofFn fun x ↦ hA.eigenvalues₀ x)).sort fun x1 x2 ↦ x1 ≥ x2) = List.ofFn hA.eigenvalues₀

Tactic:
Multiset.coe_sort

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).mergeSort fun x1 x2 ↦ decide (x1 ≥ x2)) = List.ofFn hA.eigenvalues₀
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
⊢ ((↑(List.ofFn fun x ↦ hT.eigenvalues ⋯ x)).sort fun x1 x2 ↦ x1 ≥ x2) = List.ofFn (hT.eigenvalues hn)

Tactic:
Multiset.coe_sort

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
⊢ ((List.ofFn fun x ↦ hT.eigenvalues ⋯ x).mergeSort fun x1 x2 ↦ decide (x1 ≥ x2)) = List.ofFn (hT.eigenvalues hn)
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
⊢ ((Multiset.map (⇑RCLike.re) T.charpoly.roots).sort fun x1 x2 ↦ x1 ≥ x2) = List.ofFn (hT.eigenvalues hn)

Tactic:
simp_rw [hT.roots_charpoly_eq_eigenvalues, Fin.univ_val_map, Multiset.map_coe, List.map_ofFn,
    Function.comp_def, RCLike.ofReal_re, Multiset.coe_sort]

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
⊢ ((List.ofFn fun x ↦ hT.eigenvalues ⋯ x).mergeSort fun x1 x2 ↦ decide (x1 ≥ x2)) = List.ofFn (hT.eigenvalues hn)
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 𝕜
hA✝ : IsSelfAdjoint A
hA : A.IsHermitian
⊢ Isometry ⇑(cfcHom hA✝)

Tactic:
rw [IsHermitian.cfcHom_eq_cfcAux hA, AddMonoidHomClass.isometry_iff_norm]

Goal state after:
𝕜 : Type u_1
n : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n 𝕜
hA✝ : IsSelfAdjoint A
hA : A.IsHermitian
⊢ ∀ (x : C(↑(spectrum ℝ A), ℝ)), ‖hA.cfcAux x‖ = ‖x‖
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Abs

Goal state before:
pp: 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
a : A
ha : IsSelfAdjoint a
⊢ cfcₙ (fun x ↦ ‖x‖) a = cfc (fun x ↦ ‖x‖) a

Tactic:
cfcₙ_eq_cfc

Goal state after:
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
a : A
ha : IsSelfAdjoint a
⊢ cfc (fun x ↦ ‖x‖) a = cfc (fun x ↦ ‖x‖) a
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Abs

Goal state before:
pp: A : Type u_2
inst✝⁹ : NonUnitalNormedRing A
inst✝⁸ : StarRing A
inst✝⁷ : CStarRing A
inst✝⁶ : NormedSpace ℝ A
inst✝⁵ : SMulCommClass ℝ A A
inst✝⁴ : IsScalarTower ℝ A A
inst✝³ : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝² : PartialOrder A
inst✝¹ : StarOrderedRing A
inst✝ : NonnegSpectrumClass ℝ A
a : A
⊢ star a * a = 0 ↔ a = 0

Tactic:
CStarRing.star_mul_self_eq_zero_iff

Goal state after:
A : Type u_2
inst✝⁹ : NonUnitalNormedRing A
inst✝⁸ : StarRing A
inst✝⁷ : CStarRing A
inst✝⁶ : NormedSpace ℝ A
inst✝⁵ : SMulCommClass ℝ A A
inst✝⁴ : IsScalarTower ℝ A A
inst✝³ : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝² : PartialOrder A
inst✝¹ : StarOrderedRing A
inst✝ : NonnegSpectrumClass ℝ A
a : A
⊢ a = 0 ↔ a = 0
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
⊢ ∃ g,
    eLpNorm (g - t.indicator fun x ↦ c) p μ ≤ ε ∧
      Continuous[inst✝⁸, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] g ∧ MemLp g p μ ∧ HasCompactSupport g

Tactic:
rcases exists_Lp_half E μ p hε with ⟨δ, δpos, hδ⟩

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 μ < ε
⊢ ∃ g,
    eLpNorm (g - t.indicator fun x ↦ c) p μ ≤ ε ∧
      Continuous[inst✝⁸, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] g ∧ MemLp g p μ ∧ HasCompactSupport g
Module: Mathlib.Analysis.Distribution.SchwartzSpace.Deriv

Goal state before:
pp: E : Type u_5
F₁ : Type u_9
F₂ : Type u_10
F₃ : Type u_11
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : InnerProductSpace ℝ E
inst✝⁹ : FiniteDimensional ℝ E
inst✝⁸ : NormedAddCommGroup F₁
inst✝⁷ : NormedSpace ℝ F₁
inst✝⁶ : NormedAddCommGroup F₂
inst✝⁵ : NormedSpace ℝ F₂
inst✝⁴ : NormedAddCommGroup F₃
inst✝³ : NormedSpace ℝ F₃
inst✝² : MeasurableSpace E
μ : Measure E
inst✝¹ : BorelSpace E
inst✝ : μ.IsAddHaarMeasure
f : 𝓢(E, F₁)
g : 𝓢(E, F₂)
L : F₁ →L[ℝ] F₂ →L[ℝ] F₃
⊢ ∫ (x : E), ∑ x_1, (L (f x)) ((∂_{(stdOrthonormalBasis ℝ E) x_1} (∂_{(stdOrthonormalBasis ℝ E) x_1} g)) x) ∂μ =
    ∫ (x : E), ∑ i, (L ((∂_{(stdOrthonormalBasis ℝ E) i} (∂_{(stdOrthonormalBasis ℝ E) i} f)) x)) (g x) ∂μ

Tactic:
rw [MeasureTheory.integral_finsetSum, MeasureTheory.integral_finsetSum]

Goal state after:
E : Type u_5
F₁ : Type u_9
F₂ : Type u_10
F₃ : Type u_11
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : InnerProductSpace ℝ E
inst✝⁹ : FiniteDimensional ℝ E
inst✝⁸ : NormedAddCommGroup F₁
inst✝⁷ : NormedSpace ℝ F₁
inst✝⁶ : NormedAddCommGroup F₂
inst✝⁵ : NormedSpace ℝ F₂
inst✝⁴ : NormedAddCommGroup F₃
inst✝³ : NormedSpace ℝ F₃
inst✝² : MeasurableSpace E
μ : Measure E
inst✝¹ : BorelSpace E
inst✝ : μ.IsAddHaarMeasure
f : 𝓢(E, F₁)
g : 𝓢(E, F₂)
L : F₁ →L[ℝ] F₂ →L[ℝ] F₃
⊢ ∑ i, ∫ (a : E), (L (f a)) ((∂_{(stdOrthonormalBasis ℝ E) i} (∂_{(stdOrthonormalBasis ℝ E) i} g)) a) ∂μ =
    ∑ i, ∫ (a : E), (L ((∂_{(stdOrthonormalBasis ℝ E) i} (∂_{(stdOrthonormalBasis ℝ E) i} f)) a)) (g a) ∂μ

case hf
E : Type u_5
F₁ : Type u_9
F₂ : Type u_10
F₃ : Type u_11
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : InnerProductSpace ℝ E
inst✝⁹ : FiniteDimensional ℝ E
inst✝⁸ : NormedAddCommGroup F₁
inst✝⁷ : NormedSpace ℝ F₁
inst✝⁶ : NormedAddCommGroup F₂
inst✝⁵ : NormedSpace ℝ F₂
inst✝⁴ : NormedAddCommGroup F₃
inst✝³ : NormedSpace ℝ F₃
inst✝² : MeasurableSpace E
μ : Measure E
inst✝¹ : BorelSpace E
inst✝ : μ.IsAddHaarMeasure
f : 𝓢(E, F₁)
g : 𝓢(E, F₂)
L : F₁ →L[ℝ] F₂ →L[ℝ] F₃
⊢ ∀ i ∈ Finset.univ,
    Integrable (fun x ↦ (L ((∂_{(stdOrthonormalBasis ℝ E) i} (∂_{(stdOrthonormalBasis ℝ E) i} f)) x)) (g x)) μ

case hf
E : Type u_5
F₁ : Type u_9
F₂ : Type u_10
F₃ : Type u_11
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : InnerProductSpace ℝ E
inst✝⁹ : FiniteDimensional ℝ E
inst✝⁸ : NormedAddCommGroup F₁
inst✝⁷ : NormedSpace ℝ F₁
inst✝⁶ : NormedAddCommGroup F₂
inst✝⁵ : NormedSpace ℝ F₂
inst✝⁴ : NormedAddCommGroup F₃
inst✝³ : NormedSpace ℝ F₃
inst✝² : MeasurableSpace E
μ : Measure E
inst✝¹ : BorelSpace E
inst✝ : μ.IsAddHaarMeasure
f : 𝓢(E, F₁)
g : 𝓢(E, F₂)
L : F₁ →L[ℝ] F₂ →L[ℝ] F₃
⊢ ∀ i ∈ Finset.univ,
    Integrable (fun x ↦ (L (f x)) ((∂_{(stdOrthonormalBasis ℝ E) i} (∂_{(stdOrthonormalBasis ℝ E) i} g)) x)) μ
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✝ : μ.WeaklyRegular
hp : p ≠ ∞
f : α → E
hf : MemLp f p μ
ε✝ : ℝ≥0∞
hε✝ : ε✝ ≠ 0
c : E
t : Set α
ht : MeasurableSet t
htμ : μ t < ∞
ε : ℝ≥0∞
hε : ε ≠ 0
⊢ ∃ g,
    eLpNorm (g - t.indicator fun x ↦ c) p μ ≤ ε ∧
      Continuous[inst✝⁶, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] g ∧ MemLp g p μ ∧ IsBounded (range g)

Tactic:
rcases exists_Lp_half E μ p hε with ⟨δ, δpos, hδ⟩

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✝ : μ.WeaklyRegular
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 μ < ε
⊢ ∃ g,
    eLpNorm (g - t.indicator fun x ↦ c) p μ ≤ ε ∧
      Continuous[inst✝⁶, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] g ∧ MemLp g p μ ∧ IsBounded (range g)
Module: Mathlib.Analysis.Fourier.AddCircle

Goal state before:
pp: T : ℝ
n : ℤ
⊢ Complex.exp (0 / ↑T) = 1

Tactic:
zero_div,

Goal state after:
T : ℝ
n : ℤ
⊢ Complex.exp 0 = 1
Module: Mathlib.Analysis.Fourier.AddCircle

Goal state before:
pp: T : ℝ
m n : ℤ
x : AddCircle T
⊢ ↑(m • x + n • x).toCircle = ↑(m • x).toCircle * ↑(n • x).toCircle

Tactic:
toCircle_add,

Goal state after:
T : ℝ
m n : ℤ
x : AddCircle T
⊢ ↑((m • x).toCircle * (n • x).toCircle) = ↑(m • x).toCircle * ↑(n • x).toCircle
Module: Mathlib.Analysis.Fourier.AddCircle

Goal state before:
pp: T : ℝ
n : ℤ
hn : n ≠ 0
hT : 0 < T
x : AddCircle T
⊢ ↑(n • x + ↑(n • (T / 2 / ↑n))).toCircle = -(fourier n) x

Tactic:
toCircle_add,

Goal state after:
T : ℝ
n : ℤ
hn : n ≠ 0
hT : 0 < T
x : AddCircle T
⊢ ↑((n • x).toCircle * toCircle ↑(n • (T / 2 / ↑n))) = -(fourier n) x
Module: Mathlib.Analysis.Fourier.AddCircle

Goal state before:
pp: T : ℝ
hT : Fact (0 < T)
x y : AddCircle T
hxy : x ≠ y
⊢ (fun f ↦ ⇑f) (fourier 1) x ≠ (fun f ↦ ⇑f) (fourier 1) y

Tactic:
dsimp only

Goal state after:
T : ℝ
hT : Fact (0 < T)
x y : AddCircle T
hxy : x ≠ y
⊢ (fourier 1) x ≠ (fourier 1) y
Module: Mathlib.Analysis.Distribution.SchwartzSpace.Basic

Goal state before:
pp: E : Type u_5
F : Type u_6
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
k n : ℕ
f g : 𝓢(E, F)
x : E
⊢ ‖x‖ ^ k * ‖iteratedFDeriv ℝ n (⇑f + ⇑g) x‖ ≤
    ‖x‖ ^ k * ‖iteratedFDeriv ℝ n (⇑f) x‖ + ‖x‖ ^ k * ‖iteratedFDeriv ℝ n (⇑g) x‖

Tactic:
rw [← mul_add]

Goal state after:
E : Type u_5
F : Type u_6
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
k n : ℕ
f g : 𝓢(E, F)
x : E
⊢ ‖x‖ ^ k * ‖iteratedFDeriv ℝ n (⇑f + ⇑g) x‖ ≤ ‖x‖ ^ k * (‖iteratedFDeriv ℝ n (⇑f) x‖ + ‖iteratedFDeriv ℝ n (⇑g) x‖)
Module: Mathlib.Analysis.Distribution.SchwartzSpace.Basic

Goal state before:
pp: E : Type u_5
F : Type u_6
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
k n : ℕ
f g : 𝓢(E, F)
x : E
⊢ ‖x‖ ^ k * ‖iteratedFDeriv ℝ n (⇑f + ⇑g) x‖ ≤ ‖x‖ ^ k * (‖iteratedFDeriv ℝ n (⇑f) x‖ + ‖iteratedFDeriv ℝ n (⇑g) x‖)

Tactic:
gcongr _ * ?_

Goal state after:
case hbc
E : Type u_5
F : Type u_6
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
k n : ℕ
f g : 𝓢(E, F)
x : E
⊢ ‖iteratedFDeriv ℝ n (⇑f + ⇑g) x‖ ≤ ‖iteratedFDeriv ℝ n (⇑f) x‖ + ‖iteratedFDeriv ℝ n (⇑g) x‖
Module: Mathlib.Analysis.Distribution.SchwartzSpace.Basic

Goal state before:
pp: ι : Type u_1
𝕜 : Type u_2
𝕜' : Type u_3
D : Type u_4
E : Type u_5
F : Type u_6
G : Type u_7
H : Type u_8
V : Type u_9
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → F
h₁ : HasCompactSupport f
h₂ : ContDiff ℝ ∞ f
k n : ℕ
g : E → ℝ := fun x ↦ ‖x‖ ^ k * ‖iteratedFDeriv ℝ n f x‖
hg₁ : Continuous g
⊢ ∃ C, ∀ (x : E), ‖x‖ ^ k * ‖iteratedFDeriv ℝ n f x‖ ≤ C

Tactic:
have hg₂ : HasCompactSupport g := (h₁.iteratedFDeriv _).norm.mul_left

Goal state after:
ι : Type u_1
𝕜 : Type u_2
𝕜' : Type u_3
D : Type u_4
E : Type u_5
F : Type u_6
G : Type u_7
H : Type u_8
V : Type u_9
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → F
h₁ : HasCompactSupport f
h₂ : ContDiff ℝ ∞ f
k n : ℕ
g : E → ℝ := fun x ↦ ‖x‖ ^ k * ‖iteratedFDeriv ℝ n f x‖
hg₁ : Continuous g
hg₂ : HasCompactSupport g
⊢ ∃ C, ∀ (x : E), ‖x‖ ^ k * ‖iteratedFDeriv ℝ n f x‖ ≤ C
Module: Mathlib.Analysis.Distribution.SchwartzSpace.Basic

Goal state before:
pp: case hbc
ι : Type u_1
𝕜 : Type u_2
𝕜' : Type u_3
D : Type u_4
E : Type u_5
F : Type u_6
G : Type u_7
H : Type u_8
V : Type u_9
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 𝕜 E
inst✝ : NormedSpace 𝕜 G
B : E →L[𝕜] F →L[𝕜] G
g : D → F
hg : Function.HasTemperateGrowth g
k n l : ℕ
C : ℝ
hC : 0 ≤ C
f : 𝓢(D, E)
x : D
hxk : 0 ≤ ‖x‖ ^ k
hnorm_mul :
  ‖iteratedFDeriv ℝ n (fun y ↦ ((ContinuousLinearMap.bilinearRestrictScalars ℝ B) (f y)) (g y)) x‖ ≤
    ‖ContinuousLinearMap.bilinearRestrictScalars ℝ B‖ *
      ∑ i ∈ Finset.range (n + 1), ↑(n.choose i) * ‖iteratedFDeriv ℝ i (⇑f) x‖ * ‖iteratedFDeriv ℝ (n - i) g x‖
this : ∑ _x ∈ Finset.range (n + 1), 1 = ↑n + 1
i : ℕ
hgrowth : ‖iteratedFDeriv ℝ (n - i) g x‖ ≤ C * (1 + ‖x‖) ^ l
hi : i ≤ (l + k, n).2
⊢ ‖x‖ ^ k * ‖iteratedFDeriv ℝ i (⇑f) x‖ * (1 + ‖x‖) ^ l ≤ (1 + ‖x‖) ^ l * (1 + ‖x‖) ^ k * ‖iteratedFDeriv ℝ i (⇑f) x‖

Tactic:
move_mul [(1 + ‖x‖) ^ l]

Goal state after:
case hbc
ι : Type u_1
𝕜 : Type u_2
𝕜' : Type u_3
D : Type u_4
E : Type u_5
F : Type u_6
G : Type u_7
H : Type u_8
V : Type u_9
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 𝕜 E
inst✝ : NormedSpace 𝕜 G
B : E →L[𝕜] F →L[𝕜] G
g : D → F
hg : Function.HasTemperateGrowth g
k n l : ℕ
C : ℝ
hC : 0 ≤ C
f : 𝓢(D, E)
x : D
hxk : 0 ≤ ‖x‖ ^ k
hnorm_mul :
  ‖iteratedFDeriv ℝ n (fun y ↦ ((ContinuousLinearMap.bilinearRestrictScalars ℝ B) (f y)) (g y)) x‖ ≤
    ‖ContinuousLinearMap.bilinearRestrictScalars ℝ B‖ *
      ∑ i ∈ Finset.range (n + 1), ↑(n.choose i) * ‖iteratedFDeriv ℝ i (⇑f) x‖ * ‖iteratedFDeriv ℝ (n - i) g x‖
this : ∑ _x ∈ Finset.range (n + 1), 1 = ↑n + 1
i : ℕ
hgrowth : ‖iteratedFDeriv ℝ (n - i) g x‖ ≤ C * (1 + ‖x‖) ^ l
hi : i ≤ (l + k, n).2
⊢ ‖x‖ ^ k * ‖iteratedFDeriv ℝ i (⇑f) x‖ * (1 + ‖x‖) ^ l ≤ (1 + ‖x‖) ^ k * ‖iteratedFDeriv ℝ i (⇑f) x‖ * (1 + ‖x‖) ^ l
Module: Mathlib.Analysis.Fourier.FourierTransformDeriv

Goal state before:
pp: E : Type u_1
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℂ E
V : Type u_2
W : Type u_3
inst✝⁶ : NormedAddCommGroup V
inst✝⁵ : NormedSpace ℝ V
inst✝⁴ : NormedAddCommGroup W
inst✝³ : NormedSpace ℝ W
L : V →L[ℝ] W →L[ℝ] ℝ
f : V → E
inst✝² : MeasurableSpace V
inst✝¹ : BorelSpace V
μ : Measure V
inst✝ : SecondCountableTopology V
N : ℕ∞ω
hf : ∀ (n : ℕ), ↑n ≤ N → Integrable (fun v ↦ ‖v‖ ^ n * ‖f v‖) μ
h'f : AEStronglyMeasurable f μ
n : ℕ
hn : ↑n < N
w : W
I₁ : Integrable (fun v ↦ fourierPowSMulRight L f v n) μ
v : V
⊢ ‖v‖ * ((2 * π * ‖L‖) ^ n * ‖v‖ ^ n * ‖f v‖) = (2 * π * ‖L‖) ^ n * (‖v‖ ^ (n + 1) * ‖f v‖)

Tactic:
rw [pow_succ]

Goal state after:
E : Type u_1
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℂ E
V : Type u_2
W : Type u_3
inst✝⁶ : NormedAddCommGroup V
inst✝⁵ : NormedSpace ℝ V
inst✝⁴ : NormedAddCommGroup W
inst✝³ : NormedSpace ℝ W
L : V →L[ℝ] W →L[ℝ] ℝ
f : V → E
inst✝² : MeasurableSpace V
inst✝¹ : BorelSpace V
μ : Measure V
inst✝ : SecondCountableTopology V
N : ℕ∞ω
hf : ∀ (n : ℕ), ↑n ≤ N → Integrable (fun v ↦ ‖v‖ ^ n * ‖f v‖) μ
h'f : AEStronglyMeasurable f μ
n : ℕ
hn : ↑n < N
w : W
I₁ : Integrable (fun v ↦ fourierPowSMulRight L f v n) μ
v : V
⊢ ‖v‖ * ((2 * π * ‖L‖) ^ n * ‖v‖ ^ n * ‖f v‖) = (2 * π * ‖L‖) ^ n * (‖v‖ ^ n * ‖v‖ * ‖f v‖)