mathlib-initiative/mathlib-tactics huggingface dataset:
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}
⊢ HasTemperateGrowth fun x ↦ (1 + ‖x‖ ^ 2) ^ r

Tactic:
have ht : Set.range (fun (x : H) ↦ (1 + ‖x‖ ^ 2)) ⊆ t := by
    rintro - ⟨y, rfl⟩
    simp only [Set.mem_ofPred_eq, t]
    exact lt_add_of_lt_add_left (c := 0) (by norm_num) (by positivity)

Goal state after:
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
⊢ HasTemperateGrowth fun x ↦ (1 + ‖x‖ ^ 2) ^ r
Module: Mathlib.Analysis.Distribution.TestFunction

Goal state before:
pp: case pos
𝕜 : 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
f : 𝓓^{n}(Ω, F)
v x : E
hk : k + 1 ≤ n
⊢ (fderiv ℝ (⇑f) x) v = lineDeriv ℝ (⇑f) x v

Tactic:
have hk' : 0 < (n : ℕ∞ω) := mod_cast (add_pos_of_right zero_lt_one k).trans_le hk

Goal state after:
case pos
𝕜 : 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
f : 𝓓^{n}(Ω, F)
v x : E
hk : k + 1 ≤ n
hk' : 0 < ↑n
⊢ (fderiv ℝ (⇑f) x) v = lineDeriv ℝ (⇑f) x v
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
v : E
hk : n < k + 1
⊢ lineDerivCLM 𝕜 v = 0

Tactic:
ext
  simp [not_le_of_gt hk]

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

Goal state before:
pp: M₁ : Type u_4
M₂ : Type u_5
M₃ : Type u_6
inst✝³ : TopologicalSpace M₁
inst✝² : TopologicalSpace M₂
inst✝¹ : TopologicalSpace M₃
inst✝ : AddCommMonoid M₁
f : M₁ → M₂
hf : IsCompactOperator f
g : M₂ → M₃
hg : Continuous[inst✝², inst✝¹] g
⊢ IsCompactOperator (g ∘ f)

Tactic:
rcases hf with ⟨K, hK, hKf⟩
  refine ⟨g '' K, hK.image hg, mem_of_superset hKf ?_⟩
  rw [preimage_comp]
  exact preimage_mono (subset_preimage_image _ _)

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.Bijective ⇑S
⊢ False

Tactic:
replace h₂ : ¬ (S : X → X).Surjective := by grind [Function.Bijective, hK.injective]

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) μ
S : X →L[𝕜] X := T - μ • 1
K : NNReal
hK : AntilipschitzWith K ⇑S
h₂ : ¬Function.Surjective ⇑S
⊢ 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
⊢ ((conjStarAlgAut 𝕜 (Matrix n n 𝕜)) (star hA.eigenvectorUnitary)) A = diagonal (RCLike.ofReal ∘ hA.eigenvalues)

Tactic:
apply Matrix.toEuclideanLin.injective <| (EuclideanSpace.basisFun n 𝕜).toBasis.ext fun i ↦ ?_
  simp only [conjStarAlgAut_star_apply, toLpLin_apply, OrthonormalBasis.coe_toBasis,
    EuclideanSpace.basisFun_apply, PiLp.ofLp_single, ← mulVec_mulVec,
    eigenvectorUnitary_mulVec, ← mulVec_mulVec, mulVec_eigenvectorBasis,
    Matrix.diagonal_mulVec_single, mulVec_smul, star_eigenvectorUnitary_mulVec,
    RCLike.real_smul_eq_coe_smul (K := 𝕜), WithLp.toLp_smul, PiLp.toLp_single,
    Function.comp_apply, mul_one]
  apply PiLp.ext fun j ↦ ?_
  simp only [PiLp.smul_apply, PiLp.single_apply, smul_eq_mul, mul_ite, mul_one, mul_zero]

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.charpoly.roots = Multiset.map (RCLike.ofReal ∘ hA.eigenvalues) Finset.univ.val

Tactic:
hA.charpoly_eq,

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
⊢ (∏ i, (Polynomial.X - Polynomial.C ↑(hA.eigenvalues i))).roots =
    Multiset.map (RCLike.ofReal ∘ hA.eigenvalues) Finset.univ.val
Module: Mathlib.Analysis.Matrix.Spectrum

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

Tactic:
hA.charpoly_eq,

Goal state after:
case mp
𝕜 : Type u_1
inst✝² : RCLike 𝕜
n : Type u_2
inst✝¹ : Fintype n
A B : Matrix n n 𝕜
inst✝ : DecidableEq n
hA : A.IsHermitian
hB : B.IsHermitian
h : hA.eigenvalues = hB.eigenvalues
⊢ ∏ i, (Polynomial.X - Polynomial.C ↑(hA.eigenvalues i)) = B.charpoly
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
μ : 𝕜
hμ : HasEigenvalue T μ
x : Eigenvalues T := ⟨μ, hμ⟩
hx : x = ⟨μ, hμ⟩
i : Fin n
hi : DirectSum.IsInternal.subordinateOrthonormalBasisIndex hn ⋯ i ⋯ = x
⊢ ∃ i, ↑(hT.unsortedEigenvalues hn i) = μ

Tactic:
use i

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

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

Tactic:
rw [← RCLike.conj_eq_iff_re]

Goal state after:
𝕜 : Type u_1
inst✝³ : RCLike 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
inst✝ : FiniteDimensional 𝕜 E
n : ℕ
hT : T.IsSymmetric
hn : finrank 𝕜 E = n
i : Fin n
v : E := (hT.unsortedEigenvectorBasis hn) i
μ : 𝕜 := ↑T (DirectSum.IsInternal.subordinateOrthonormalBasisIndex hn ⋯ i ⋯)
key : HasEigenvector T μ v
⊢ (starRingEnd 𝕜) μ = μ
Module: Mathlib.Analysis.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)
hk : k + 1 ≤ n
⊢ ContDiffMapSupportedIn.of_support_subset ⋯ ⋯ =
    ContDiffMapSupportedIn.of_support_subset ⋯ ⋯ + ContDiffMapSupportedIn.of_support_subset ⋯ ⋯

Tactic:
have hk' : 0 < (n : ℕ∞ω) := mod_cast (add_pos_of_right zero_lt_one k).trans_le hk

Goal state after:
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)
hk : k + 1 ≤ n
hk' : 0 < ↑n
⊢ ContDiffMapSupportedIn.of_support_subset ⋯ ⋯ =
    ContDiffMapSupportedIn.of_support_subset ⋯ ⋯ + ContDiffMapSupportedIn.of_support_subset ⋯ ⋯
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
c : 𝕜
f : 𝓓^{n}_{K}(E, F)
hk : k + 1 ≤ n
⊢ ContDiffMapSupportedIn.of_support_subset ⋯ ⋯ = (RingHom.id 𝕜) c • ContDiffMapSupportedIn.of_support_subset ⋯ ⋯

Tactic:
have hk' : 0 < (n : ℕ∞ω) := mod_cast (add_pos_of_right zero_lt_one k).trans_le hk

Goal state after:
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
c : 𝕜
f : 𝓓^{n}_{K}(E, F)
hk : k + 1 ≤ n
hk' : 0 < ↑n
⊢ ContDiffMapSupportedIn.of_support_subset ⋯ ⋯ = (RingHom.id 𝕜) c • ContDiffMapSupportedIn.of_support_subset ⋯ ⋯
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
b : UnconditionalSchauderBasis β 𝕜 X
inst✝ : CompleteSpace X
x : X
A₀ : Finset β
hA₀ : ∀ (t : Finset β), Disjoint t A₀ → ‖∑ i ∈ t, (b.coord i) x • ↑b i‖ < 1
A : Finset β
⊢ ∑ i ∈ A, (b.coord i) x • ↑b i = ∑ i ∈ A ∩ A₀, (b.coord i) x • ↑b i + ∑ i ∈ A \ A₀, (b.coord i) x • ↑b i

Tactic:
rw [← Finset.sum_union (Finset.disjoint_sdiff_inter A A₀).symm,
      Finset.union_comm, Finset.sdiff_union_inter]

Goal state after:
Module: Mathlib.Analysis.Normed.Module.Bases

Goal state before:
pp: case a
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
X : Type u_2
inst✝¹ : NormedAddCommGroup X
inst✝ : NormedSpace 𝕜 X
P : ℕ → X →L[𝕜] X
hrank : ∀ (n : ℕ), Module.finrank 𝕜 ↥(↑(P n)).range = n
hcomp : ∀ (n m : ℕ) (x : X), (P n) ((P m) x) = (P (min n m)) x
n : ℕ
U : Submodule 𝕜 X := ⋯
V : Submodule 𝕜 X := ⋯
W : Submodule 𝕜 X := ⋯
hV : V ≤ W
hUW : U ≤ W
⊢ W ≤ U ⊔ V

pp: case a
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
X : Type u_2
inst✝¹ : NormedAddCommGroup X
inst✝ : NormedSpace 𝕜 X
P : ℕ → X →L[𝕜] X
hrank : ∀ (n : ℕ), Module.finrank 𝕜 ↥(↑(P n)).range = n
hcomp : ∀ (n m : ℕ) (x : X), (P n) ((P m) x) = (P (min n m)) x
n : ℕ
U : Submodule 𝕜 X := ⋯
V : Submodule 𝕜 X := ⋯
W : Submodule 𝕜 X := ⋯
hV : V ≤ W
hUW : U ≤ W
⊢ U ⊔ V ≤ W

Tactic:
· rintro x ⟨y, hy⟩
      rw [← hy, ContinuousLinearMap.coe_coe, ← sub_add_cancel ((P (n + 1)) y) ((P n) y)]
      exact Submodule.add_mem_sup ⟨y, rfl⟩ ⟨y, rfl⟩

Goal state after:
case a
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
X : Type u_2
inst✝¹ : NormedAddCommGroup X
inst✝ : NormedSpace 𝕜 X
P : ℕ → X →L[𝕜] X
hrank : ∀ (n : ℕ), Module.finrank 𝕜 ↥(↑(P n)).range = n
hcomp : ∀ (n m : ℕ) (x : X), (P n) ((P m) x) = (P (min n m)) x
n : ℕ
U : Submodule 𝕜 X := ⋯
V : Submodule 𝕜 X := ⋯
W : Submodule 𝕜 X := ⋯
hV : V ≤ W
hUW : U ≤ W
⊢ U ⊔ V ≤ W
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
⊢ (span 𝕜 (Set.range ⇑b)).topologicalClosure = ⊤

Tactic:
rw [eq_top_iff]
  rintro x -
  refine mem_closure_of_tendsto (b.hasSum_repr x) (Eventually.of_forall ?_)
  intro s
  simp only [SetLike.mem_coe]
  refine sum_mem ?_
  rintro i -
  refine smul_mem _ _ ?_
  exact subset_span ⟨i, rfl⟩

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

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
a b : ℝ
hab : a < b
f g : ℝ → E
h : f =ᵐ[volume.restrict (Ioc a b)] g
n : ℤ
⊢ (fun x ↦ (fourier (-n)) ↑x • f x) =ᵐ[volume.restrict (Ioc a b)] fun x ↦ (fourier (-n)) ↑x • g x

Tactic:
filter_upwards [h] with x hx

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
a b : ℝ
hab : a < b
f g : ℝ → E
h : f =ᵐ[volume.restrict (Ioc a b)] g
n : ℤ
x : ℝ
hx : f x = g x
⊢ (fourier (-n)) ↑x • f x = (fourier (-n)) ↑x • g x
Module: Mathlib.Analysis.Fourier.AddCircle

Goal state before:
pp: T : ℝ
hT : Fact (0 < T)
f : ↥(Lp ℂ 2 haarAddCircle)
i : ℤ
⊢ ∫ (t : AddCircle T), (starRingEnd ℂ) (↑↑(fourierLp 2 i) t) * ↑↑f t ∂haarAddCircle = fourierCoeff (↑↑f) i

Tactic:
apply integral_congr_ae
    filter_upwards [coeFn_fourierLp 2 i] with _ ht
    rw [ht, ← fourier_neg, smul_eq_mul]

Goal state after:
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) μ
⊢ MemLp g ∞ (μ.restrict (s ∩ u))

Tactic:
apply
        memLp_top_of_bound (hmg.mono_set inter_subset_left).aestronglyMeasurable (‖a‖ + 1)

Goal state after:
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
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‖
⊢ HasFDerivAt (fourierIntegral 𝐞 μ (ContinuousLinearMap.toLinearMap₁₂ L) f)
    (fourierIntegral 𝐞 μ (ContinuousLinearMap.toLinearMap₁₂ L) (fourierSMulRight L f) w) w

Tactic:
have h0 (w' : W) : Integrable (F w') μ :=
    (fourierIntegral_convergent_iff continuous_fourierChar
      (by apply L.continuous₂ : Continuous (fun p : V × W ↦ L.toLinearMap₁₂ p.1 p.2)) w').2 hf

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') μ
⊢ HasFDerivAt (fourierIntegral 𝐞 μ (ContinuousLinearMap.toLinearMap₁₂ L) f)
    (fourierIntegral 𝐞 μ (ContinuousLinearMap.toLinearMap₁₂ L) (fourierSMulRight L f) w) w
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
f : 𝓢(E, F)
k : ℕ
x₀ : E
this : ‖x₀‖ ^ k * ‖iteratedFDeriv ℝ 0 (⇑f) x₀‖ ≤ (SchwartzMap.seminorm 𝕜 k 0) f
⊢ ‖x₀‖ ^ k * ‖f x₀‖ ≤ (SchwartzMap.seminorm 𝕜 k 0) f

Tactic:
norm_iteratedFDeriv_zero

Goal state after:
𝕜 : 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
f : 𝓢(E, F)
k : ℕ
x₀ : E
this : ‖x₀‖ ^ k * ‖f x₀‖ ≤ (SchwartzMap.seminorm 𝕜 k 0) f
⊢ ‖x₀‖ ^ k * ‖f x₀‖ ≤ (SchwartzMap.seminorm 𝕜 k 0) f
Module: Mathlib.MeasureTheory.Integral.PeakFunction

Goal state before:
pp: α : 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 : Set α
φ : ι → α → ℝ
a : E
inst✝ : CompleteSpace E
hs : MeasurableSet s
t : Set α
ht : MeasurableSet t
hts : t ⊆ s
h'ts : t ∈ 𝓝[s] x₀
h't : μ t ≠ ∞
hnφ : ∀ᶠ (i : ι) in l, ∀ x ∈ s, 0 ≤ φ i x
hlφ : ∀ (u : Set α), IsOpen[inst✝⁴] u → x₀ ∈ u → TendstoUniformlyOn φ 0 l (s \ u)
hiφ : Tendsto (fun i ↦ ∫ (x : α) in t, φ i x ∂μ) l (𝓝 1)
h'iφ : ∀ᶠ (i : ι) in l, AEStronglyMeasurable (φ i) (μ.restrict s)
hmg : IntegrableOn g s μ
hcg : Tendsto g (𝓝[s] x₀) (𝓝 a)
h : α → E := ⋯
A : Tendsto (fun i ↦ ∫ (x : α) in s, φ i x • h x ∂μ + (∫ (x : α) in t, φ i x ∂μ) • a) l (𝓝 a)
i : ι
hi : IntegrableOn (fun x ↦ φ i x • g x) s μ
h'i : ‖∫ (x : α) in t, φ i x ∂μ - 1‖ < 1
⊢ Integrable (φ i) ((μ.restrict s).restrict t)

Tactic:
rw [restrict_restrict ht, inter_eq_left.mpr hts]

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 : Set α
φ : ι → α → ℝ
a : E
inst✝ : CompleteSpace E
hs : MeasurableSet s
t : Set α
ht : MeasurableSet t
hts : t ⊆ s
h'ts : t ∈ 𝓝[s] x₀
h't : μ t ≠ ∞
hnφ : ∀ᶠ (i : ι) in l, ∀ x ∈ s, 0 ≤ φ i x
hlφ : ∀ (u : Set α), IsOpen[inst✝⁴] u → x₀ ∈ u → TendstoUniformlyOn φ 0 l (s \ u)
hiφ : Tendsto (fun i ↦ ∫ (x : α) in t, φ i x ∂μ) l (𝓝 1)
h'iφ : ∀ᶠ (i : ι) in l, AEStronglyMeasurable (φ i) (μ.restrict s)
hmg : IntegrableOn g s μ
hcg : Tendsto g (𝓝[s] x₀) (𝓝 a)
h : α → E := g - t.indicator fun x ↦ a
A : Tendsto (fun i ↦ ∫ (x : α) in s, φ i x • h x ∂μ + (∫ (x : α) in t, φ i x ∂μ) • a) l (𝓝 a)
i : ι
hi : IntegrableOn (fun x ↦ φ i x • g x) s μ
h'i : ‖∫ (x : α) in t, φ i x ∂μ - 1‖ < 1
⊢ Integrable (φ i) (μ.restrict t)
Module: Mathlib.MeasureTheory.Integral.PeakFunction

Goal state before:
pp: α : Type u_1
E : Type u_2
hm : MeasurableSpace α
μ : Measure α
inst✝⁶ : TopologicalSpace α
inst✝⁵ : BorelSpace α
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
g : α → E
x₀ : α
s : Set α
inst✝² : CompleteSpace E
inst✝¹ : MetrizableSpace α
inst✝ : IsLocallyFiniteMeasure μ
hs : IsCompact s
hμ : ∀ (u : Set α), IsOpen[inst✝⁶] u → x₀ ∈ u → 0 < μ (u ∩ s)
c : α → ℝ
hc : ContinuousOn c s
h'c : ∀ y ∈ s, y ≠ x₀ → c y < c x₀
hnc : ∀ x ∈ s, 0 ≤ c x
hnc₀ : 0 < c x₀
h₀ : x₀ ∈ s
hmg : IntegrableOn g s μ
hcg : ContinuousWithinAt g s x₀
φ : ℕ → α → ℝ := fun n x ↦ (∫ (x : α) in s, c x ^ n ∂μ)⁻¹ * c x ^ n
n : ℕ
x : α
hx : x ∈ s
⊢ 0 ≤ φ n x

Tactic:
apply mul_nonneg (inv_nonneg.2 _) (pow_nonneg (hnc x hx) _)

Goal state after:
α : Type u_1
E : Type u_2
hm : MeasurableSpace α
μ : Measure α
inst✝⁶ : TopologicalSpace α
inst✝⁵ : BorelSpace α
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
g : α → E
x₀ : α
s : Set α
inst✝² : CompleteSpace E
inst✝¹ : MetrizableSpace α
inst✝ : IsLocallyFiniteMeasure μ
hs : IsCompact s
hμ : ∀ (u : Set α), IsOpen[inst✝⁶] u → x₀ ∈ u → 0 < μ (u ∩ s)
c : α → ℝ
hc : ContinuousOn c s
h'c : ∀ y ∈ s, y ≠ x₀ → c y < c x₀
hnc : ∀ x ∈ s, 0 ≤ c x
hnc₀ : 0 < c x₀
h₀ : x₀ ∈ s
hmg : IntegrableOn g s μ
hcg : ContinuousWithinAt g s x₀
φ : ℕ → α → ℝ := ⋯
n : ℕ
x : α
hx : x ∈ s
⊢ 0 ≤ ∫ (x : α) in s, c x ^ n ∂μ
Module: Mathlib.Analysis.Fourier.FourierTransform

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹² : CommRing 𝕜
V : Type u_2
inst✝¹¹ : AddCommGroup V
inst✝¹⁰ : Module 𝕜 V
inst✝⁹ : MeasurableSpace V
W : Type u_3
inst✝⁸ : AddCommGroup W
inst✝⁷ : Module 𝕜 W
E : Type u_4
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℂ E
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : IsTopologicalRing 𝕜
inst✝² : TopologicalSpace V
inst✝¹ : BorelSpace V
inst✝ : TopologicalSpace W
e : AddChar 𝕜 𝕊
μ : Measure V
L : V →ₗ[𝕜] W →ₗ[𝕜] 𝕜
he : Continuous[inst✝⁴, _] ⇑e
hL : Continuous[instTopologicalSpaceProd, inst✝⁴] fun p ↦ (L p.1) p.2
f : V → E
w : W
⊢ Integrable (fun v ↦ e (-(L v) w) • f v) μ ↔ Integrable f μ

Tactic:
by
  -- first prove one-way implication
  have aux {g : V → E} (hg : Integrable g μ) (x : W) :
      Integrable (fun v : V ↦ e (-L v x) • g v) μ := by
    have c : Continuous fun v ↦ e (-L v x) := he.comp (hL.comp (.prodMk_left _)).neg
    simp_rw [← integrable_norm_iff (c.aestronglyMeasurable.fun_smul hg.1), Circle.norm_smul]
    exact hg.norm
  -- then use it for both directions
  refine ⟨fun hf ↦ ?_, fun hf ↦ aux hf w⟩
  have := aux hf (-w)
  simp_rw [← mul_smul (e _) (e _) (f _), ← e.map_add_eq_mul, map_neg, neg_add_cancel,
    e.map_zero_eq_one, one_smul] at this -- the `(e _)` speeds up elaboration considerably
  exact this

Goal state after: