mathlib-initiative/mathlib-tactics huggingface dataset:
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}
this : SigmaFinite ν
A : ∫⁻ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0..f ω, g t) ∂μ = ∫⁻ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0..f ω, g t) ∂ν
B1 :
  ∫⁻ (t : ℝ) in Ioc 0 M, μ {a | t ≤ f a} * ENNReal.ofReal (g t) =
    ∫⁻ (t : ℝ) in Ioc 0 M, ν {a | t ≤ f a} * ENNReal.ofReal (g t)
⊢ ∫⁻ (t : ℝ) in Ioi M, μ {a | t ≤ f a} * ENNReal.ofReal (g t) =
    ∫⁻ (t : ℝ) in Ioi M, ν {a | t ≤ f a} * ENNReal.ofReal (g t)

Tactic:
apply setLIntegral_congr_fun measurableSet_Ioi (fun t ht ↦ ?_)

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}
this : SigmaFinite ν
A : ∫⁻ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0..f ω, g t) ∂μ = ∫⁻ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0..f ω, g t) ∂ν
B1 :
  ∫⁻ (t : ℝ) in Ioc 0 M, μ {a | t ≤ f a} * ENNReal.ofReal (g t) =
    ∫⁻ (t : ℝ) in Ioc 0 M, ν {a | t ≤ f a} * ENNReal.ofReal (g t)
t : ℝ
ht : t ∈ Ioi M
⊢ μ {a | t ≤ f a} * ENNReal.ofReal (g t) = ν {a | t ≤ f a} * ENNReal.ofReal (g t)
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]
  exact le_trans (le_iSup₂_of_le K K_sub_Ω le_rfl) originalTop_le

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

Goal state before:
pp: case pos
𝕜 : Type u_1
inst✝² : RCLike 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : E →L[𝕜] E
hT : (↑T).IsSymmetric
M : ℝ := ⨆ x, |T.rayleighQuotient x|
nonneg : 0 ≤ M
x : E
hM : |re ⟪T x, x⟫_𝕜| / ‖x‖ ^ 2 ≤ M
hx : 0 < ‖x‖ ^ 2
⊢ |re ⟪T x, x⟫_𝕜| ≤ M * ‖x‖ ^ 2

Tactic:
div_le_iff₀ hx

Goal state after:
case pos
𝕜 : Type u_1
inst✝² : RCLike 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : E →L[𝕜] E
hT : (↑T).IsSymmetric
M : ℝ := ⨆ x, |T.rayleighQuotient x|
nonneg : 0 ≤ M
x : E
hM : |re ⟪T x, x⟫_𝕜| ≤ M * ‖x‖ ^ 2
hx : 0 < ‖x‖ ^ 2
⊢ |re ⟪T x, x⟫_𝕜| ≤ M * ‖x‖ ^ 2
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
hT : (↑T).IsSymmetric
M : ℝ := ⨆ x, |T.rayleighQuotient x|
nonneg : 0 ≤ M
hM : ∀ (x : E), |re ⟪T x, x⟫_𝕜| ≤ M * ‖x‖ ^ 2
x y : E
hx : ‖x‖ = 1
hy : ‖y‖ = 1
key : re (⟪T x, y⟫_𝕜 + (starRingEnd 𝕜) ⟪T x, y⟫_𝕜) = re (2 * ↑(re ⟪T x, y⟫_𝕜))
⊢ re ⟪T x, y⟫_𝕜 ≤ M * (‖x + y‖ ^ 2 + ‖x - y‖ ^ 2) / 4

Tactic:
rw [map_add, conj_inner_symm, ← coe_coe, ← hT, coe_coe, re_mul_ofReal, ofNat_re] at key

Goal state after:
𝕜 : Type u_1
inst✝² : RCLike 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : E →L[𝕜] E
hT : (↑T).IsSymmetric
M : ℝ := ⨆ x, |T.rayleighQuotient x|
nonneg : 0 ≤ M
hM : ∀ (x : E), |re ⟪T x, x⟫_𝕜| ≤ M * ‖x‖ ^ 2
x y : E
hx : ‖x‖ = 1
hy : ‖y‖ = 1
key : re ⟪T x, y⟫_𝕜 + re ⟪T y, x⟫_𝕜 = 2 * re ⟪T x, y⟫_𝕜
⊢ re ⟪T x, y⟫_𝕜 ≤ M * (‖x + y‖ ^ 2 + ‖x - y‖ ^ 2) / 4
Module: Mathlib.Analysis.Normed.Operator.Compact.Basic

Goal state before:
pp: M₁ : Type u_3
M₂ : Type u_4
inst✝⁶ : TopologicalSpace M₁
inst✝⁵ : AddCommMonoid M₁
inst✝⁴ : TopologicalSpace M₂
inst✝³ : AddCommMonoid M₂
S : Type u_6
inst✝² : Monoid S
inst✝¹ : DistribMulAction S M₂
inst✝ : ContinuousConstSMul S M₂
f : M₁ → M₂
c : Sˣ
h : IsCompactOperator (c • f)
⊢ IsCompactOperator f

Tactic:
simpa using h.smul c⁻¹

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
⊢ ↑‖T‖₊ ≤ spectralRadius 𝕜 T

Tactic:
suffices h : algebraMap ℝ 𝕜 ‖T‖ ∈ spectrum 𝕜 T ∨ algebraMap ℝ 𝕜 (-‖T‖) ∈ spectrum 𝕜 T by
    rcases h with h | h <;> exact le_trans (by simp) (le_biSup _ h)

Goal state after:
𝕜 : 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
⊢ (algebraMap ℝ 𝕜) ‖T‖ ∈ spectrum 𝕜 T ∨ (algebraMap ℝ 𝕜) (-‖T‖) ∈ spectrum 𝕜 T
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⟩‖
⊢ 1 ≤ ‖x‖

Tactic:
simpa using! hxy 0

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 (⇑RCLike.re) A.charpoly.roots).sort fun x1 x2 ↦ x1 ≥ x2) = List.ofFn hA.eigenvalues₀

Tactic:
by
  simp_rw [hA.roots_charpoly_eq_eigenvalues₀, Fin.univ_val_map, Multiset.map_coe, List.map_ofFn,
    Function.comp_def, RCLike.ofReal_re, Multiset.coe_sort]
  apply List.mergeSort_of_pairwise
  simp_rw [decide_eq_true_eq, ← List.sortedGE_iff_pairwise]
  exact (eigenvalues₀_antitone hA).sortedGE_ofFn

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 = ((Unitary.conjStarAlgAut 𝕜 (Matrix n n 𝕜)) hA.eigenvectorUnitary) (diagonal (Function.const n 0))
⊢ Function.const n 0 = fun x ↦ 0

Tactic:
by rfl

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✝² : SeminormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : Finite n
v : n → E
⊢ (gram 𝕜 v).PosSemidef

Tactic:
by
  have := Fintype.ofFinite n
  refine .of_dotProduct_mulVec_nonneg (isHermitian_gram _ _) fun x ↦ ?_
  rw [star_dotProduct_gram_mulVec, le_iff_re_im]
  simp

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

Goal state before:
pp: α : Type u_1
F : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup F
f : ↥(Lp F 2 μ)
h_two : ENNReal.ofReal 2 = 2
⊢ eLpNorm (fun x ↦ ‖↑↑f x‖ ^ 2) 1 μ < ∞

Tactic:
eLpNorm_norm_rpow f zero_lt_two,

Goal state after:
α : Type u_1
F : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup F
f : ↥(Lp F 2 μ)
h_two : ENNReal.ofReal 2 = 2
⊢ eLpNorm (↑↑f) (1 * ENNReal.ofReal 2) μ ^ 2 < ∞
Module: Mathlib.Analysis.Distribution.ContDiffMapSupportedIn

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝¹³ : NontriviallyNormedField 𝕜
inst✝¹² : NormedAddCommGroup E
inst✝¹¹ : NormedSpace ℝ E
n : ℕ∞
K : Compacts E
m : MeasurableSpace E
inst✝¹⁰ : OpensMeasurableSpace E
F₁ : Type u_5
F₂ : Type u_6
F₃ : Type u_7
inst✝⁹ : NormedAddCommGroup F₁
inst✝⁸ : NormedSpace 𝕜 F₁
inst✝⁷ : NormedSpace ℝ F₁
inst✝⁶ : NormedAddCommGroup F₂
inst✝⁵ : NormedSpace 𝕜 F₂
inst✝⁴ : NormedAddCommGroup F₃
inst✝³ : NormedSpace 𝕜 F₃
inst✝² : SMulCommClass ℝ 𝕜 F₁
inst✝¹ : NormedSpace ℝ F₃
inst✝ : SMulCommClass ℝ 𝕜 F₃
B : F₁ →L[𝕜] F₂ →L[𝕜] F₃
μ : Measure E
φ : E → F₂
f : 𝓓^{n}_{K}(E, F₁)
⊢ ‖(integralAgainstBilinLM B μ φ) f‖ ≤
    (∫ (x : E) in ↑K, ‖φ x‖ ∂μ) * ‖B‖ * (ContDiffMapSupportedIn.seminorm 𝕜 E F₁ n K 0) f

Tactic:
by_cases hφ : IntegrableOn φ K μ
  · have h : ∀ᵐ x ∂(μ.restrict K), ‖B (f x) (φ x)‖ ≤ ‖φ x‖ * ‖B‖ * N[𝕜]_{K, n, 0} f := by
      filter_upwards [] with x
      grw [ContinuousLinearMap.le_opNorm, ContinuousLinearMap.le_opNorm, norm_apply_le_seminorm 𝕜,
        mul_comm, mul_assoc]
    rw [integralAgainstBilinLM_eq_setIntegral hφ]
    apply le_trans (norm_integral_le_of_norm_le ((hφ.norm.mul_const _).mul_const _) h)
    rw [integral_mul_const, integral_mul_const]
  · simp only [integralAgainstBilinLM, hφ, ↓reduceIte, LinearMap.coe_mk, AddHom.coe_mk, norm_zero]
    positivity

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

Goal state before:
pp: ι : Type u_1
𝕜 : Type u_2
inst✝⁴ : RCLike 𝕜
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
G : ι → Type u_4
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)
f₁ f₂ g : ↥(lp G 2)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
simp only [inner_add_left, Pi.add_apply, coeFn_add]

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

Goal state before:
pp: case refine_1
ι : Type u_1
𝕜 : Type u_2
inst✝⁶ : RCLike 𝕜
E : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace 𝕜 E
G : ι → Type u_4
inst✝³ : (i : ι) → NormedAddCommGroup (G i)
inst✝² : (i : ι) → InnerProductSpace 𝕜 (G i)
inst✝¹ : CompleteSpace E
V : (i : ι) → G i →ₗᵢ[𝕜] E
hV : OrthogonalFamily 𝕜 G V
inst✝ : ∀ (i : ι), CompleteSpace (G i)
f : ↥(lp G 2)
s : Finset ι
⊢ ∑ b ∈ s, (fun i ↦ (V i) (↑f i)) b ∈ (⨆ i, (V i).range).toAddSubmonoid

Tactic:
refine sum_mem ?_

Goal state after:
case refine_1
ι : Type u_1
𝕜 : Type u_2
inst✝⁶ : RCLike 𝕜
E : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace 𝕜 E
G : ι → Type u_4
inst✝³ : (i : ι) → NormedAddCommGroup (G i)
inst✝² : (i : ι) → InnerProductSpace 𝕜 (G i)
inst✝¹ : CompleteSpace E
V : (i : ι) → G i →ₗᵢ[𝕜] E
hV : OrthogonalFamily 𝕜 G V
inst✝ : ∀ (i : ι), CompleteSpace (G i)
f : ↥(lp G 2)
s : Finset ι
⊢ ∀ c ∈ s, (V c) (↑f c) ∈ (⨆ i, (V i).range).toAddSubmonoid
Module: Mathlib.Analysis.InnerProductSpace.l2Space

Goal state before:
pp: 𝕜 : Type u_2
inst✝³ : RCLike 𝕜
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
K : Submodule 𝕜 E
hK : CompleteSpace ↥K
⊢ IsHilbertSum 𝕜 (fun b ↦ ↥(bif b then K else Kᗮ)) fun b ↦ (bif b then K else Kᗮ).subtypeₗᵢ

Tactic:
by
  have : ∀ b, CompleteSpace (↥(cond b K Kᗮ)) := by
    intro b
    cases b <;> first | exact instOrthogonalCompleteSpace K | assumption
  refine IsHilbertSum.mkInternal _ K.orthogonalFamily_self ?_
  refine le_trans ?_ (Submodule.le_topologicalClosure _)
  rw [iSup_bool_eq, cond, cond]
  refine Codisjoint.top_le ?_
  exact K.isCompl_orthogonal.codisjoint

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

Goal state before:
pp: ι : Type u_1
𝕜 : Type u_2
inst✝³ : RCLike 𝕜
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : DecidableEq ι
b : HilbertBasis ι 𝕜 E
i : ι
⊢ b.repr (b i) = lp.single 2 i 1

Tactic:
simp only [LinearIsometryEquiv.apply_symm_apply, ← b.repr_symm_single]

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

Goal state before:
pp: ι : Type u_1
𝕜 : Type u_2
inst✝² : RCLike 𝕜
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
b : HilbertBasis ι 𝕜 E
x : E
s : Finset ι
⊢ ∑ x_1 ∈ s, ↑(b.repr x) x_1 • b x_1 ∈ (span 𝕜 (Set.range ⇑b)).toAddSubmonoid

Tactic:
refine sum_mem ?_

Goal state after:
ι : Type u_1
𝕜 : Type u_2
inst✝² : RCLike 𝕜
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
b : HilbertBasis ι 𝕜 E
x : E
s : Finset ι
⊢ ∀ c ∈ s, ↑(b.repr x) c • b c ∈ (span 𝕜 (Set.range ⇑b)).toAddSubmonoid
Module: Mathlib.MeasureTheory.Integral.PeakFunction

Goal state before:
pp: case hf
α : Type u_1
E : Type u_2
ι : Type u_3
hm : MeasurableSpace α
μ : Measure α
inst✝³ : TopologicalSpace α
inst✝² : BorelSpace α
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
g : α → E
l : Filter ι
x₀ : α
s t : Set α
φ : ι → α → ℝ
a : E
hs : MeasurableSet s
h'st : t ∈ 𝓝[s] x₀
hlφ : ∀ (u : Set α), IsOpen[inst✝³] u → x₀ ∈ u → TendstoUniformlyOn φ 0 l (s \ u)
hiφ : Tendsto (fun e ↦ ‖∫ (x : α) in t, φ e x ∂μ - 1‖) l (𝓝 0)
h'iφ : ∀ᶠ (i : ι) in l, AEStronglyMeasurable (φ i) (μ.restrict s)
hmg : IntegrableOn g s μ
hcg : Tendsto g (𝓝[s] x₀) (𝓝 a)
u : Set α
u_open : IsOpen[inst✝³] u
x₀u : x₀ ∈ u
ut : s ∩ u ⊆ t
hu : ∀ x ∈ u ∩ s, g x ∈ ball a 1
i : ι
hi : ∀ x ∈ s \ u, dist (0 x) (φ i x) < 1
h'i : ‖∫ (x : α) in t, φ i x ∂μ - 1‖ < 1
h''i : AEStronglyMeasurable (φ i) (μ.restrict s)
I : IntegrableOn (φ i) t μ
A : IntegrableOn (fun x ↦ φ i x • g x) (s \ u) μ
⊢ ∀ᵐ (x : α) ∂μ.restrict (s ∩ u), ‖g x‖ ≤ ‖a‖ + 1

Tactic:
filter_upwards [self_mem_ae_restrict (hs.inter u_open.measurableSet)] with x hx

Goal state after:
α : Type u_1
E : Type u_2
ι : Type u_3
hm : MeasurableSpace α
μ : Measure α
inst✝³ : TopologicalSpace α
inst✝² : BorelSpace α
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
g : α → E
l : Filter ι
x₀ : α
s t : Set α
φ : ι → α → ℝ
a : E
hs : MeasurableSet s
h'st : t ∈ 𝓝[s] x₀
hlφ : ∀ (u : Set α), IsOpen[inst✝³] u → x₀ ∈ u → TendstoUniformlyOn φ 0 l (s \ u)
hiφ : Tendsto (fun e ↦ ‖∫ (x : α) in t, φ e x ∂μ - 1‖) l (𝓝 0)
h'iφ : ∀ᶠ (i : ι) in l, AEStronglyMeasurable (φ i) (μ.restrict s)
hmg : IntegrableOn g s μ
hcg : Tendsto g (𝓝[s] x₀) (𝓝 a)
u : Set α
u_open : IsOpen[inst✝³] u
x₀u : x₀ ∈ u
ut : s ∩ u ⊆ t
hu : ∀ x ∈ u ∩ s, g x ∈ ball a 1
i : ι
hi : ∀ x ∈ s \ u, dist (0 x) (φ i x) < 1
h'i : ‖∫ (x : α) in t, φ i x ∂μ - 1‖ < 1
h''i : AEStronglyMeasurable (φ i) (μ.restrict s)
I : IntegrableOn (φ i) t μ
A : IntegrableOn (fun x ↦ φ i x • g x) (s \ u) μ
x : α
hx : x ∈ s ∩ u
⊢ ‖g x‖ ≤ ‖a‖ + 1
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
inst✝ : SecondCountableTopology V
μ : Measure V
hf : Integrable f μ
hf' : Integrable (fun v ↦ ‖v‖ * ‖f v‖) μ
w : W
F : W → V → E := fun w' v ↦ 𝐞 (-(L v) w') • f v
F' : W → V → W →L[ℝ] E := fun w' v ↦ 𝐞 (-(L v) w') • fourierSMulRight L f v
B : V → ℝ := fun v ↦ 2 * π * ‖L‖ * ‖v‖ * ‖f v‖
h0 : ∀ (w' : W), Integrable (F w') μ
h1 : ∀ᶠ (w' : W) in 𝓝 w, AEStronglyMeasurable (F w') μ
h3 : AEStronglyMeasurable (F' w) μ
v : V
w' : W
a✝ : w' ∈ Metric.ball w 1
⊢ ‖F' w' v‖ ≤ B v

Tactic:
Circle.norm_smul _ (fourierSMulRight L f v)

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
inst✝ : SecondCountableTopology V
μ : Measure V
hf : Integrable f μ
hf' : Integrable (fun v ↦ ‖v‖ * ‖f v‖) μ
w : W
F : W → V → E := fun w' v ↦ 𝐞 (-(L v) w') • f v
F' : W → V → W →L[ℝ] E := fun w' v ↦ 𝐞 (-(L v) w') • fourierSMulRight L f v
B : V → ℝ := fun v ↦ 2 * π * ‖L‖ * ‖v‖ * ‖f v‖
h0 : ∀ (w' : W), Integrable (F w') μ
h1 : ∀ᶠ (w' : W) in 𝓝 w, AEStronglyMeasurable (F w') μ
h3 : AEStronglyMeasurable (F' w) μ
v : V
w' : W
a✝ : w' ∈ Metric.ball w 1
⊢ ‖fourierSMulRight L f v‖ ≤ B v
Module: Mathlib.Analysis.Distribution.SchwartzSpace.Basic

Goal state before:
pp: 𝕜 : Type u_2
E : Type u_5
F : Type u_6
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : NormedField 𝕜
inst✝¹ : NormedSpace 𝕜 F
inst✝ : SMulCommClass ℝ 𝕜 F
k n : ℕ
f : 𝓢(E, F)
⊢ (SchwartzMap.seminorm 𝕜 k n) f = sInf {c | 0 ≤ c ∧ ∀ (x : E), ‖x‖ ^ k * ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤ c}

Tactic:
by rfl

Goal state after:
Module: Mathlib.Analysis.Fourier.FourierTransformDeriv

Goal state before:
pp: case hfg
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
inst✝¹ : FiniteDimensional ℝ V
μ : Measure V
inst✝ : μ.IsAddHaarMeasure
hf : Integrable f μ
h'f : Differentiable ℝ f
hf' : Integrable (fderiv ℝ f) μ
w : W
y : V
g : V → ℂ := fun v ↦ ↑(𝐞 (-(L v) w))
A : ∀ (x : V), (fderiv ℝ g x) y = -2 * ↑π * I * ↑((L y) w) * g x
⊢ Integrable (fun x ↦ g x • f x) μ

Tactic:
exact (fourierIntegral_convergent_iff' _ _).2 hf

Goal state after:
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✝⁴ : NormedField 𝕜
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace ℝ G
inst✝¹ : NormedSpace 𝕜 G
inst✝ : SMulCommClass ℝ 𝕜 G
m : F
k n : ℕ
f : 𝓢(E, F →L[ℝ] G)
x : E
⊢ ‖x‖ ^ k * ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤ (SchwartzMap.seminorm 𝕜 k n) f

Tactic:
apply le_seminorm

Goal state after:
Module: Mathlib.Analysis.Distribution.SchwartzSpace.Basic

Goal state before:
pp: 𝕜 : Type u_2
D : Type u_4
V : Type u_9
inst✝⁸ : RCLike 𝕜
inst✝⁷ : NormedAddCommGroup D
inst✝⁶ : NormedSpace ℝ D
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : NormedSpace ℝ V
inst✝³ : NormedSpace 𝕜 V
inst✝² : MeasurableSpace D
μ : Measure D
hμ : μ.HasTemperateGrowth
inst✝¹ : BorelSpace D
inst✝ : SecondCountableTopology D
f : 𝓢(D, V)
⊢ (integralCLM 𝕜 μ) f = ∫ (x : D), f x ∂μ

Tactic:
by rfl

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Lebesgue.Integral

Goal state before:
pp: f : ℝ → ℝ
x✝ : ℝ
hx : x✝ ∈ Ioi 0
⊢ 0 < x✝

Tactic:
exact hx

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Lebesgue.Integral

Goal state before:
pp: f : ℝ → ℝ
eq : ∫ (x : ℝ) in Ioi 0, f |x| = ∫ (x : ℝ) in Ioi 0, f x
hf : IntegrableOn (fun x ↦ f |x|) (Ioi 0) volume
int_Iic : IntegrableOn (fun x ↦ f |x|) (Iic 0) volume
⊢ ∫ (x : ℝ), f |x| = (∫ (x : ℝ) in Iic 0, f |x|) + ∫ (x : ℝ) in Ioi 0, f |x|

Tactic:
rw [← setIntegral_union (Iic_disjoint_Ioi le_rfl) measurableSet_Ioi int_Iic hf,
          Iic_union_Ioi, restrict_univ]

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Lebesgue.Integral

Goal state before:
pp: f : ℝ → ℝ
eq : ∫ (x : ℝ) in Ioi 0, f |x| = ∫ (x : ℝ) in Ioi 0, f x
hf : IntegrableOn (fun x ↦ f |x|) (Ioi 0) volume
int_Iic : IntegrableOn (fun x ↦ f |x|) (Iic 0) volume
x✝ : ℝ
hx : x✝ ∈ Iic 0
⊢ x✝ ≤ 0

Tactic:
exact hx

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

Goal state before:
pp: α : Type u_1
E : Type u_2
F : Type u_3
inst✝² : NormedAddCommGroup E
g : α → F
l : Filter α
ι : Type u_4
inst✝¹ : MeasurableSpace ι
f : ι × α → E
s : Set ι
μ : Measure ι
inst✝ : Norm F
hf : f =O[𝓟 s ×ˢ l] (g ∘ Prod.snd)
hfm : ∀ᶠ (x : α) in l, AEStronglyMeasurable (fun i ↦ f (i, x)) (μ.restrict s)
hs : MeasurableSet s
hμ : μ s < ⊤
C : ℝ
hC : ∀ᶠ (x : ι × α) in 𝓟 s ×ˢ l, ‖f x‖ ≤ C * ‖(g ∘ Prod.snd) x‖
t : Set (ι × α)
htl : t ∈ 𝓟 s ×ˢ l
ht : ∀ y ∈ t, ‖f y‖ ≤ C * ‖(g ∘ Prod.snd) y‖
u : Set ι
hu : u ∈ 𝓟 s
v : Set α
hv : v ∈ l
huv : u ×ˢ v ⊆ t
w : Set α
hwl : w ∈ l
hw : ∀ y ∈ w, AEStronglyMeasurable (fun i ↦ f (i, y)) (μ.restrict s)
⊢ ∀ᶠ (x : α) in l, IntegrableOn (fun i ↦ f (i, x)) s μ

Tactic:
refine eventually_iff_exists_mem.mpr ⟨w ∩ v, inter_mem hwl hv, fun x hx ↦ ?_⟩

Goal state after:
α : Type u_1
E : Type u_2
F : Type u_3
inst✝² : NormedAddCommGroup E
g : α → F
l : Filter α
ι : Type u_4
inst✝¹ : MeasurableSpace ι
f : ι × α → E
s : Set ι
μ : Measure ι
inst✝ : Norm F
hf : f =O[𝓟 s ×ˢ l] (g ∘ Prod.snd)
hfm : ∀ᶠ (x : α) in l, AEStronglyMeasurable (fun i ↦ f (i, x)) (μ.restrict s)
hs : MeasurableSet s
hμ : μ s < ⊤
C : ℝ
hC : ∀ᶠ (x : ι × α) in 𝓟 s ×ˢ l, ‖f x‖ ≤ C * ‖(g ∘ Prod.snd) x‖
t : Set (ι × α)
htl : t ∈ 𝓟 s ×ˢ l
ht : ∀ y ∈ t, ‖f y‖ ≤ C * ‖(g ∘ Prod.snd) y‖
u : Set ι
hu : u ∈ 𝓟 s
v : Set α
hv : v ∈ l
huv : u ×ˢ v ⊆ t
w : Set α
hwl : w ∈ l
hw : ∀ y ∈ w, AEStronglyMeasurable (fun i ↦ f (i, y)) (μ.restrict s)
x : α
hx : x ∈ w ∩ v
⊢ IntegrableOn (fun i ↦ f (i, x)) s μ
Module: Mathlib.Analysis.Fourier.FourierTransform

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_3
F : Type u_4
V : Type u_5
W : Type u_6
inst✝¹⁰ : NontriviallyNormedField 𝕜
inst✝⁹ : NormedAddCommGroup V
inst✝⁸ : NormedSpace 𝕜 V
inst✝⁷ : MeasurableSpace V
inst✝⁶ : BorelSpace V
inst✝⁵ : NormedAddCommGroup W
inst✝⁴ : NormedSpace 𝕜 W
e : AddChar 𝕜 𝕊
μ : Measure V
L : V →L[𝕜] W →L[𝕜] 𝕜
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : V → F →L[ℝ] E
a : F
w : W
he : Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] ⇑e
hf : Integrable f μ
⊢ Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun p ↦
    ((ContinuousLinearMap.toLinearMap₁₂ L) p.1) p.2

Tactic:
exact L.continuous₂

Goal state after:
Module: Mathlib.Analysis.Fourier.FourierTransform

Goal state before:
pp: 𝕜 : Type u_1
ι : Type u_2
E : Type u_3
V : Type u_5
W : Type u_6
inst✝¹¹ : Fintype ι
inst✝¹⁰ : NontriviallyNormedField 𝕜
inst✝⁹ : NormedAddCommGroup V
inst✝⁸ : NormedSpace 𝕜 V
inst✝⁷ : MeasurableSpace V
inst✝⁶ : BorelSpace V
inst✝⁵ : NormedAddCommGroup W
inst✝⁴ : NormedSpace 𝕜 W
e : AddChar 𝕜 𝕊
μ : Measure V
L : V →L[𝕜] W →L[𝕜] 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
M : ι → Type u_7
inst✝¹ : (i : ι) → NormedAddCommGroup (M i)
inst✝ : (i : ι) → NormedSpace ℝ (M i)
f : V → ContinuousMultilinearMap ℝ M E
m : (i : ι) → M i
w : W
he : Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] ⇑e
hf : Integrable f μ
⊢ Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun p ↦
    ((ContinuousLinearMap.toLinearMap₁₂ L) p.1) p.2

Tactic:
exact L.continuous₂

Goal state after:
Module: Mathlib.Analysis.Fourier.FourierTransform

Goal state before:
pp: V : Type u_1
E : Type u_3
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℂ E
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MeasurableSpace V
inst✝¹ : BorelSpace V
inst✝ : FiniteDimensional ℝ V
f : V → E
w : V
⊢ 𝓕⁻ f w = 𝓕 f (-w)

Tactic:
by
  simp [fourier_eq, fourierInv_eq]

Goal state after:
Module: Mathlib.Analysis.Fourier.FourierTransformDeriv

Goal state before:
pp: case e'_6
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℝ → E
hf : Integrable f volume
hf' : Integrable (fun x ↦ x • f x) volume
w : ℝ
hf'' : Integrable (fun v ↦ ‖v‖ * ‖f v‖) volume
L : ℝ →L[ℝ] ℝ →L[ℝ] ℝ := ⋯
v : ℝ
⊢ ((L v).smulRight (f v)) 1 = (↑↑(ContinuousLinearMap.toSpanSingletonLIE ℝ E) (v • f v)) 1

Tactic:
ContinuousLinearMap.smulRight_apply,

Goal state after:
case e'_6
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℝ → E
hf : Integrable f volume
hf' : Integrable (fun x ↦ x • f x) volume
w : ℝ
hf'' : Integrable (fun v ↦ ‖v‖ * ‖f v‖) volume
L : ℝ →L[ℝ] ℝ →L[ℝ] ℝ := (ContinuousLinearMap.mul ℝ ℝ).flip
v : ℝ
⊢ (L v) 1 • f v = (↑↑(ContinuousLinearMap.toSpanSingletonLIE ℝ E) (v • f v)) 1