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

Goal state before:
pp: α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝⁹ : TopologicalSpace α
inst✝⁸ : BorelSpace α
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : SecondCountableTopologyEither α E
inst✝⁵ : IsFiniteMeasure μ
𝕜 : Type u_3
inst✝⁴ : Fact (1 ≤ p)
inst✝³ : NormedRing 𝕜
inst✝² : Module 𝕜 E
inst✝¹ : IsBoundedSMul 𝕜 E
f g : α →ᵇ E
inst✝ : μ.IsOpenPosMeasure
⊢ (toLp p μ 𝕜) f = (toLp p μ 𝕜) g ↔ f = g

Tactic:
refine ⟨fun h => ?_, by tauto⟩

Goal state after:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝⁹ : TopologicalSpace α
inst✝⁸ : BorelSpace α
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : SecondCountableTopologyEither α E
inst✝⁵ : IsFiniteMeasure μ
𝕜 : Type u_3
inst✝⁴ : Fact (1 ≤ p)
inst✝³ : NormedRing 𝕜
inst✝² : Module 𝕜 E
inst✝¹ : IsBoundedSMul 𝕜 E
f g : α →ᵇ E
inst✝ : μ.IsOpenPosMeasure
h : (toLp p μ 𝕜) f = (toLp p μ 𝕜) g
⊢ f = g
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₃
B : F₁ →L[𝕜] F₂ →L[𝕜] F₃
μ : Measure E
φ : E → F₂
hφ : IntegrableOn φ (↑K) μ
f : 𝓓^{n}_{K}(E, F₁)
this : IntegrableOn (fun x ↦ (B (f x)) (φ x)) (↑K) μ
⊢ (support fun x ↦ (B (f x)) (φ x)) ⊆ ↑K

Tactic:
refine subset_trans ?_ f.support_subset

Goal state after:
𝕜 : 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₃
B : F₁ →L[𝕜] F₂ →L[𝕜] F₃
μ : Measure E
φ : E → F₂
hφ : IntegrableOn φ (↑K) μ
f : 𝓓^{n}_{K}(E, F₁)
this : IntegrableOn (fun x ↦ (B (f x)) (φ x)) (↑K) μ
⊢ (support fun x ↦ (B (f x)) (φ x)) ⊆ support ⇑f
Module: Mathlib.Geometry.Manifold.SmoothApprox

Goal state before:
pp: case neg
E : Type u_1
F : Type u_2
H : Type u_3
M : Type u_4
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : FiniteDimensional ℝ E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℝ F
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : IsManifold I ∞ M
inst✝¹ : SigmaCompactSpace M
inst✝ : T2Space M
f : M → F
ε : M → ℝ
n : ℕ∞
f_cont : Continuous[inst✝⁴, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
ε_cont : Continuous[inst✝⁴, _] ε
ε_pos : ∀ (x : M), 0 < ε x
S U : Set M
hS : IsClosed[inst✝⁴] S
hU : U ∈ 𝓝ˢ S
hfU : ContMDiffOn I 𝓘(ℝ, F) (↑n) f U
dist_f_f : ∀ (x : M), dist (f x) (f x) < ε x
t : M → Set F := fun x ↦ {y | dist y (f x) < ε x ∧ (x ∈ S → y = f x) ∧ (f x = 0 → y = 0)}
t_conv : ∀ (x : M), Convex ℝ (t x)
x : M
hx : x ∉ S
⊢ ∃ U ∈ 𝓝 x, ∃ g, ContMDiffOn I 𝓘(ℝ, F) (↑n) g U ∧ ∀ y ∈ U, g y ∈ t y

Tactic:
· have : ∀ᶠ y in 𝓝 x, y ∉ S ∧ dist (f x) (f y) < ε y := (hS.isOpen_compl.eventually_mem hx).and
      ((continuous_const.dist f_cont).continuousAt.eventually_lt ε_cont.continuousAt (dist_f_f x))
    have : ∀ᶠ y in 𝓝 x, (y ∉ S ∧ dist (f x) (f y) < ε y) ∧ (f y = 0 → f x = 0) := by
      by_cases hx' : f x = 0
      · simpa [hx'] using this
      · simpa [hx'] using this.and (f_cont.continuousAt.eventually_ne hx')
    exact ⟨_, this, (fun _ ↦ f x), contMDiffOn_const, fun y hy ↦ ⟨hy.1.2, by simp [hy.1.1], hy.2⟩⟩

Goal state after:
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
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 := (↑(succSub P n)).range
V : Submodule 𝕜 X := (↑(P n)).range
W : Submodule 𝕜 X := (↑(P (n + 1))).range
y : X
⊢ ↑(P n) y ∈ W

Tactic:
exact ⟨P n y, by simp [ContinuousLinearMap.coe_coe, hcomp]⟩

Goal state after:
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
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 := (↑(succSub P n)).range
V : Submodule 𝕜 X := (↑(P n)).range
W : Submodule 𝕜 X := (↑(P (n + 1))).range
hV : V ≤ W
hUW : U ≤ W
hW : W = U ⊔ V
x : X
x✝ : x ∈ U ⊓ V
y : X
hy : ↑(succSub P n) y = x
z : X
hz : ↑(P n) z = x
⊢ (P n) z = (P (min n n)) z

Tactic:
min_self

Goal state after:
𝕜 : 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 := (↑(succSub P n)).range
V : Submodule 𝕜 X := (↑(P n)).range
W : Submodule 𝕜 X := (↑(P (n + 1))).range
hV : V ≤ W
hUW : U ≤ W
hW : W = U ⊔ V
x : X
x✝ : x ∈ U ⊓ V
y : X
hy : ↑(succSub P n) y = x
z : X
hz : ↑(P n) z = x
⊢ (P n) z = (P n) z
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)
inst✝ : CompleteSpace E
V : (i : ι) → G i →ₗᵢ[𝕜] E
hV✝ hV : OrthogonalFamily 𝕜 G V
f : ↥(lp G 2)
⊢ ‖{ toFun := fun f ↦ ∑' (i : ι), (V i) (↑f i), map_add' := ⋯, map_smul' := ⋯ } f‖ = ‖f‖

Tactic:
have H : 0 < (2 : ℝ≥0∞).toReal := by simp

Goal state after:
ι : 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✝ hV : OrthogonalFamily 𝕜 G V
f : ↥(lp G 2)
H : 0 < ENNReal.toReal 2
⊢ ‖{ toFun := fun f ↦ ∑' (i : ι), (V i) (↑f i), map_add' := ⋯, map_smul' := ⋯ } f‖ = ‖f‖
Module: Mathlib.Analysis.Fourier.AddCircle

Goal state before:
pp: T : ℝ
x : AddCircle T
⊢ (fourier 0) x = 1

Tactic:
by
  simp

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

Goal state before:
pp: T : ℝ
⊢ ↑(toCircle 0) = 1

Tactic:
by
  simp

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)
inst✝² : CompleteSpace E
V : (i : ι) → G i →ₗᵢ[𝕜] E
hV : OrthogonalFamily 𝕜 G V
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (G i)
W₀ : Π₀ (i : ι), G i
⊢ hV.linearIsometry (W₀.sum (lp.single 2)) = W₀.sum fun i ↦ ⇑(V i)

Tactic:
by
  simp

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

Goal state before:
pp: T : ℝ
hT : Fact (0 < T)
f : ↥(Lp ℂ 2 haarAddCircle)
H₁ : HasSum (fun i ↦ ‖↑(fourierBasis.repr f) i‖ ^ 2) (‖fourierBasis.repr f‖ ^ 2)
H₂ : ‖fourierBasis.repr f‖ ^ 2 = ‖f‖ ^ 2
H₃ : RCLike.re (inner ℂ f f) = ∫ (x : AddCircle T), RCLike.re (inner ℂ (↑↑f x) (↑↑f x)) ∂haarAddCircle
⊢ HasSum (fun i ↦ ‖↑(fourierBasis.repr f) i‖ ^ 2) (∫ (t : AddCircle T), ‖↑↑f t‖ ^ 2 ∂haarAddCircle)

Tactic:
simp only [← norm_sq_eq_re_inner] at H₃

Goal state after:
T : ℝ
hT : Fact (0 < T)
f : ↥(Lp ℂ 2 haarAddCircle)
H₁ : HasSum (fun i ↦ ‖↑(fourierBasis.repr f) i‖ ^ 2) (‖fourierBasis.repr f‖ ^ 2)
H₂ : ‖fourierBasis.repr f‖ ^ 2 = ‖f‖ ^ 2
H₃ : ‖f‖ ^ 2 = ∫ (x : AddCircle T), ‖↑↑f x‖ ^ 2 ∂haarAddCircle
⊢ HasSum (fun i ↦ ‖↑(fourierBasis.repr f) i‖ ^ 2) (∫ (t : AddCircle T), ‖↑↑f t‖ ^ 2 ∂haarAddCircle)
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✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAlgebra ℝ 𝕜
inst✝ : NormedSpace 𝕜 F
c : 𝕜
f : 𝓢(E, F)
x : E
⊢ ((smulLeftCLM F fun x ↦ c) f) x = ((c • ContinuousLinearMap.id 𝕜 𝓢(E, F)) f) x

Tactic:
have : (fun (_ : E) ↦ c).HasTemperateGrowth := by fun_prop

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✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAlgebra ℝ 𝕜
inst✝ : NormedSpace 𝕜 F
c : 𝕜
f : 𝓢(E, F)
x : E
this : Function.HasTemperateGrowth fun x ↦ c
⊢ ((smulLeftCLM F fun x ↦ c) f) x = ((c • ContinuousLinearMap.id 𝕜 𝓢(E, F)) f) x
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✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAlgebra ℝ 𝕜
inst✝ : NormedSpace 𝕜 F
g : E → 𝕜
hg : Function.HasTemperateGrowth g
c : 𝕜
⊢ smulLeftCLM F (c • g) = c • smulLeftCLM F g

Tactic:
have : (fun (_ : E) ↦ c).HasTemperateGrowth := by fun_prop

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✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAlgebra ℝ 𝕜
inst✝ : NormedSpace 𝕜 F
g : E → 𝕜
hg : Function.HasTemperateGrowth g
c : 𝕜
this : Function.HasTemperateGrowth fun x ↦ c
⊢ smulLeftCLM F (c • g) = c • smulLeftCLM F g
Module: Mathlib.Analysis.Distribution.SchwartzSpace.Basic

Goal state before:
pp: case pos
𝕜 : Type u_2
E : Type u_5
F : Type u_6
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAlgebra ℝ 𝕜
inst✝ : NormedSpace 𝕜 F
g : E → 𝕜
f : 𝓢(E, F)
hg : Function.HasTemperateGrowth g
⊢ tsupport ⇑((smulLeftCLM F g) f) ⊆ tsupport ⇑f ∩ tsupport g

pp: case neg
𝕜 : Type u_2
E : Type u_5
F : Type u_6
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAlgebra ℝ 𝕜
inst✝ : NormedSpace 𝕜 F
g : E → 𝕜
f : 𝓢(E, F)
hg : ¬Function.HasTemperateGrowth g
⊢ tsupport ⇑((smulLeftCLM F g) f) ⊆ tsupport ⇑f ∩ tsupport g

Tactic:
· simpa [smulLeftCLM_apply hg] using
      ⟨tsupport_smul_subset_right g f, tsupport_smul_subset_left g f⟩

Goal state after:
case neg
𝕜 : Type u_2
E : Type u_5
F : Type u_6
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAlgebra ℝ 𝕜
inst✝ : NormedSpace 𝕜 F
g : E → 𝕜
f : 𝓢(E, F)
hg : ¬Function.HasTemperateGrowth g
⊢ tsupport ⇑((smulLeftCLM F g) f) ⊆ tsupport ⇑f ∩ tsupport g
Module: Mathlib.Analysis.Fourier.FourierTransformDeriv

Goal state before:
pp: case cont
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 μ
⊢ ∀ (m : ℕ),
    ↑m ≤ N →
      Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] fun x ↦
        fourierIntegral 𝐞 μ (ContinuousLinearMap.toLinearMap₁₂ L) (fun v ↦ fourierPowSMulRight L f v m) x

Tactic:
intro n hn
    apply fourierIntegral_continuous Real.continuous_fourierChar (by apply L.continuous₂)
    exact integrable_fourierPowSMulRight L (hf n hn) h'f

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

Goal state before:
pp: case h
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
K N : ℕ∞
hf : ContDiff ℝ (↑N) f
h'f : ∀ (k n : ℕ), ↑k ≤ K → ↑n ≤ N → Integrable (fun v ↦ ‖v‖ ^ k * ‖iteratedFDeriv ℝ n f v‖) μ
k n : ℕ
hk : ↑k ≤ K
hn : ↑n ≤ N
w : W
m : ℕ
hm : ↑m ≤ N
I : Integrable (fun v ↦ ∑ p ∈ Finset.range (k + 1) ×ˢ Finset.range (m + 1), ‖v‖ ^ p.1 * ‖iteratedFDeriv ℝ p.2 f v‖) μ
v : V
i : ℕ
hi : i ≤ m
j : ℕ
hj : j ≤ k
⊢ (j, i) ∈ Finset.range (k + 1) ×ˢ Finset.range (m + 1)

Tactic:
simpa only [Finset.mem_product, Finset.mem_range_succ_iff] using ⟨hj, hi⟩

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

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
c : ℝ
f : ℝ → E
A : MeasurableEmbedding fun x ↦ -x
this : ∫ (y : ℝ) in Ici (-c), f y ∂Measure.map (fun x ↦ -x) volume = ∫ (x : ℝ) in (fun x ↦ -x) ⁻¹' Ici (-c), f (-x)
⊢ ∫ (x : ℝ) in Iic c, f (-x) = ∫ (x : ℝ) in Ioi (-c), f x

Tactic:
Measure.map_neg_eq_self (volume : Measure ℝ)

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
c : ℝ
f : ℝ → E
A : MeasurableEmbedding fun x ↦ -x
this : ∫ (y : ℝ) in Ici (-c), f y ∂volume = ∫ (x : ℝ) in (fun x ↦ -x) ⁻¹' Ici (-c), f (-x)
⊢ ∫ (x : ℝ) in Iic c, f (-x) = ∫ (x : ℝ) in Ioi (-c), f x
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
⊢ f |x✝| = f (-x✝)

Tactic:
abs_eq_neg_self.mpr (by exact hx)

Goal state after:
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
⊢ f (-x✝) = f (-x✝)
Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral

Goal state before:
pp: b : ℝ
hb : 0 < b
s : ℝ
hs : -1 < s
this : MeasurableSet (Ioi 0)
x : ℝ
hx : x ∈ Ioi 0
h'x : 0 ≤ x
⊢ ‖(-x) ^ s * rexp (-b * x ^ 2)‖ ≤ x ^ s * rexp (-b * x ^ 2)

Tactic:
rw [Real.norm_eq_abs, abs_mul, abs_of_nonneg (exp_pos _).le]

Goal state after:
b : ℝ
hb : 0 < b
s : ℝ
hs : -1 < s
this : MeasurableSet (Ioi 0)
x : ℝ
hx : x ∈ Ioi 0
h'x : 0 ≤ x
⊢ |(-x) ^ s| * rexp (-b * x ^ 2) ≤ x ^ s * rexp (-b * x ^ 2)
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic

Goal state before:
pp: case succ
n : ℕ
hn : Gamma (↑n + 1) = ↑n !
⊢ ↑n.succ * Gamma ↑n.succ = ↑(n + 1)!

Tactic:
simp only [Nat.cast_succ, Nat.factorial_succ, Nat.cast_mul]

Goal state after:
case succ
n : ℕ
hn : Gamma (↑n + 1) = ↑n !
⊢ (↑n + 1) * Gamma (↑n + 1) = (↑n + 1) * ↑n !
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic

Goal state before:
pp: s : ℂ
n : ℕ
⊢ ∀ (s : ℂ), GammaAux n ((starRingEnd ℂ) s) = (starRingEnd ℂ) (GammaAux n s)

Tactic:
induction n with
  | zero => rw [GammaAux]; exact GammaIntegral_conj
  | succ n IH =>
    intro s
    rw [GammaAux]
    dsimp only
    rw [div_eq_mul_inv _ s, map_mul, conj_inv, ← div_eq_mul_inv]
    suffices conj s + 1 = conj (s + 1) by rw [this, IH]
    rw [map_add, map_one]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral

Goal state before:
pp: case a
b : ℂ
hb : 0 < b.re
nv : ∀ {b : ℂ}, 0 < b.re → b ≠ 0
this : ∀ (x : ℝ), cexp (-1 * ↑x ^ 2) = ↑(rexp (-1 * x ^ 2))
| 1 / 2

Tactic:
· rw [← ofReal_one, ← ofReal_ofNat, ← ofReal_div]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform

Goal state before:
pp: b : ℂ
hb : 0 < b.re
c T : ℝ
hT : 0 ≤ T
vert_norm_bound :
  ∀ {T : ℝ},
    0 ≤ T →
      ∀ {c y : ℝ},
        |y| ≤ |c| → ‖cexp (-b * (↑T + ↑y * I) ^ 2)‖ ≤ rexp (-(b.re * T ^ 2 - 2 * |b.im| * |c| * T - b.re * c ^ 2))
y : ℝ
hy : y ∈ uIoc 0 c
absy : |y| ≤ |c|
⊢ ‖cexp (-b * (↑T + ↑y * I) ^ 2) - cexp (-b * (↑T - ↑y * I) ^ 2)‖ ≤
    2 * rexp (-(b.re * T ^ 2 - 2 * |b.im| * |c| * T - b.re * c ^ 2))

Tactic:
two_mul

Goal state after:
b : ℂ
hb : 0 < b.re
c T : ℝ
hT : 0 ≤ T
vert_norm_bound :
  ∀ {T : ℝ},
    0 ≤ T →
      ∀ {c y : ℝ},
        |y| ≤ |c| → ‖cexp (-b * (↑T + ↑y * I) ^ 2)‖ ≤ rexp (-(b.re * T ^ 2 - 2 * |b.im| * |c| * T - b.re * c ^ 2))
y : ℝ
hy : y ∈ uIoc 0 c
absy : |y| ≤ |c|
⊢ ‖cexp (-b * (↑T + ↑y * I) ^ 2) - cexp (-b * (↑T - ↑y * I) ^ 2)‖ ≤
    rexp (-(b.re * T ^ 2 - 2 * |b.im| * |c| * T - b.re * c ^ 2)) +
      rexp (-(b.re * T ^ 2 - 2 * |b.im| * |c| * T - b.re * c ^ 2))
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic

Goal state before:
pp: case inl
hs : 0 ≤ 0
⊢ 0 ≤ Gamma 0

pp: case inr
s : ℝ
hs : 0 ≤ s
h : 0 < s
⊢ 0 ≤ Gamma s

Tactic:
· rw [Gamma_zero]

Goal state after:
case inr
s : ℝ
hs : 0 ≤ s
h : 0 < s
⊢ 0 ≤ Gamma s
Module: Mathlib.Analysis.Fourier.Inversion

Goal state before:
pp: case e_f.e_a.e_a
V : Type u_1
E : Type u_2
inst✝⁷ : NormedAddCommGroup V
inst✝⁶ : InnerProductSpace ℝ V
inst✝⁵ : MeasurableSpace V
inst✝⁴ : BorelSpace V
inst✝³ : FiniteDimensional ℝ V
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
f : V → E
inst✝ : CompleteSpace E
hf : Integrable f volume
h'f : Integrable (𝓕 f) volume
v : V
A : Tendsto (fun c ↦ ∫ (w : V), cexp (-↑c⁻¹ * ↑‖w‖ ^ 2 + 2 * ↑π * I * ↑⟪v, w⟫) • 𝓕 f w) atTop (𝓝 (𝓕⁻ (𝓕 f) v))
B :
  Tendsto (fun c ↦ ∫ (w : V), 𝓕 (fun w ↦ cexp (-↑c⁻¹ * ↑‖w‖ ^ 2 + 2 * ↑π * I * ↑⟪v, w⟫)) w • f w) atTop (𝓝 (𝓕⁻ (𝓕 f) v))
c : ℝ
hc : 0 < c
w : V
⊢ -↑π ^ 2 * ↑‖v - w‖ ^ 2 / ↑c⁻¹ = -↑π ^ 2 * ↑c * ↑‖v - w‖ ^ 2

Tactic:
simp; ring

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

Goal state before:
pp: case e_f
E : Type u_3
F : Type u_4
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : InnerProductSpace ℝ E
inst✝⁴ : NormedSpace ℂ F
inst✝³ : FiniteDimensional ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
inst✝ : CompleteSpace F
f : 𝓢(E, F)
ι : Type := Fin (Module.finrank ℝ E)
b : OrthonormalBasis (Fin (Module.finrank ℝ E)) ℝ E := stdOrthonormalBasis ℝ E
this : ∀ i ∈ Finset.univ, Function.HasTemperateGrowth fun x ↦ inner ℝ x (b i) ^ 2
i : Fin (Module.finrank ℝ E)
x : E
⊢ (2 * ↑π * Complex.I) •
      (2 * ↑π * Complex.I) •
        ((fourierMultiplierCLM F fun x ↦ ↑(inner ℝ x (b i))) ((fourierMultiplierCLM F fun x ↦ inner ℝ x (b i)) f)) x =
    -(2 * π) ^ 2 • ((fourierMultiplierCLM F fun x ↦ inner ℝ x (b i) ^ 2) f) x

Tactic:
smul_smul

Goal state after:
case e_f
E : Type u_3
F : Type u_4
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : InnerProductSpace ℝ E
inst✝⁴ : NormedSpace ℂ F
inst✝³ : FiniteDimensional ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
inst✝ : CompleteSpace F
f : 𝓢(E, F)
ι : Type := Fin (Module.finrank ℝ E)
b : OrthonormalBasis (Fin (Module.finrank ℝ E)) ℝ E := stdOrthonormalBasis ℝ E
this : ∀ i ∈ Finset.univ, Function.HasTemperateGrowth fun x ↦ inner ℝ x (b i) ^ 2
i : Fin (Module.finrank ℝ E)
x : E
⊢ (2 * ↑π * Complex.I * (2 * ↑π * Complex.I)) •
      ((fourierMultiplierCLM F fun x ↦ ↑(inner ℝ x (b i))) ((fourierMultiplierCLM F fun x ↦ inner ℝ x (b i)) f)) x =
    -(2 * π) ^ 2 • ((fourierMultiplierCLM F fun x ↦ inner ℝ x (b i) ^ 2) f) x
Module: Mathlib.Analysis.Distribution.FourierMultiplier

Goal state before:
pp: case e_f
E : Type u_3
F : Type u_4
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : InnerProductSpace ℝ E
inst✝³ : NormedSpace ℂ F
inst✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
f : 𝓢'(E, F)
ι : Type := Fin (Module.finrank ℝ E)
b : OrthonormalBasis (Fin (Module.finrank ℝ E)) ℝ E := stdOrthonormalBasis ℝ E
this : ∀ i ∈ Finset.univ, Function.HasTemperateGrowth fun x ↦ ↑(inner ℝ x (b i)) ^ 2
i : Fin (Module.finrank ℝ E)
x : 𝓢(E, ℂ)
⊢ ((2 * ↑π * Complex.I) •
        (2 * ↑π * Complex.I) •
          (fourierMultiplierCLM F fun x ↦ ↑(inner ℝ x (b i))) ((fourierMultiplierCLM F fun x ↦ ↑(inner ℝ x (b i))) f))
      x =
    (-(2 * π) ^ 2 • (fourierMultiplierCLM F fun x ↦ ↑(inner ℝ x (b i)) ^ 2) f) x

Tactic:
smul_smul

Goal state after:
case e_f
E : Type u_3
F : Type u_4
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : InnerProductSpace ℝ E
inst✝³ : NormedSpace ℂ F
inst✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
f : 𝓢'(E, F)
ι : Type := Fin (Module.finrank ℝ E)
b : OrthonormalBasis (Fin (Module.finrank ℝ E)) ℝ E := stdOrthonormalBasis ℝ E
this : ∀ i ∈ Finset.univ, Function.HasTemperateGrowth fun x ↦ ↑(inner ℝ x (b i)) ^ 2
i : Fin (Module.finrank ℝ E)
x : 𝓢(E, ℂ)
⊢ ((2 * ↑π * Complex.I * (2 * ↑π * Complex.I)) •
        (fourierMultiplierCLM F fun x ↦ ↑(inner ℝ x (b i))) ((fourierMultiplierCLM F fun x ↦ ↑(inner ℝ x (b i))) f))
      x =
    (-(2 * π) ^ 2 • (fourierMultiplierCLM F fun x ↦ ↑(inner ℝ x (b i)) ^ 2) f) x
Module: Mathlib.Analysis.Fourier.BoundedContinuousFunctionChar

Goal state before:
pp: V : Type u_1
W : Type u_2
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module ℝ V
inst✝³ : TopologicalSpace V
inst✝² : AddCommGroup W
inst✝¹ : Module ℝ W
inst✝ : TopologicalSpace W
e : AddChar ℝ Circle
L : V →ₗ[ℝ] W →ₗ[ℝ] ℝ
he : Continuous ⇑e
hL : Continuous fun p ↦ (L p.1) p.2
w : AddMonoidAlgebra ℂ W
v : V
⊢ ((charAlgHom he hL) w) v = w.coeff.sum fun a z ↦ z • ↑(e ((L v) a))

Tactic:
simp [charAlgHom, charMonoidHom, char, AddMonoidAlgebra.lift_apply]

Goal state after:
V : Type u_1
W : Type u_2
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module ℝ V
inst✝³ : TopologicalSpace V
inst✝² : AddCommGroup W
inst✝¹ : Module ℝ W
inst✝ : TopologicalSpace W
e : AddChar ℝ Circle
L : V →ₗ[ℝ] W →ₗ[ℝ] ℝ
he : Continuous ⇑e
hL : Continuous fun p ↦ (L p.1) p.2
w : AddMonoidAlgebra ℂ W
v : V
⊢ (w.coeff.sum fun a b ↦ b • { toFun := fun v ↦ ↑(e ((L v) a)), continuous_toFun := ⋯, map_bounded' := ⋯ }) v =
    w.coeff.sum fun a z ↦ z * ↑(e ((L v) a))
Module: Mathlib.Analysis.Fourier.Convolution

Goal state before:
pp: E : Type u_3
F₁ : Type u_5
F₂ : Type u_6
F₃ : Type u_7
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedAddCommGroup F₁
inst✝¹¹ : NormedAddCommGroup F₂
inst✝¹⁰ : NormedAddCommGroup F₃
inst✝⁹ : InnerProductSpace ℝ E
inst✝⁸ : FiniteDimensional ℝ E
inst✝⁷ : MeasurableSpace E
inst✝⁶ : BorelSpace E
inst✝⁵ : NormedSpace ℂ F₃
inst✝⁴ : CompleteSpace F₁
inst✝³ : CompleteSpace F₂
inst✝² : CompleteSpace F₃
inst✝¹ : NormedSpace ℂ F₁
inst✝ : NormedSpace ℂ F₂
B : F₁ →L[ℂ] F₂ →L[ℂ] F₃
f₁ : E → F₁
f₂ : E → F₂
hf₁ : Integrable f₁ volume
hf₂ : Integrable f₂ volume
ξ : E
⊢ ∫ (y : E) (x : E), (𝐞 (-inner ℝ y ξ) * 𝐞 (-inner ℝ x ξ)) • (B (f₁ x)) (f₂ y) =
    ∫ (y : E) (x : E), 𝐞 (-inner ℝ y ξ) • 𝐞 (-inner ℝ x ξ) • (B (f₁ x)) (f₂ y)

Tactic:
smul_smul

Goal state after:
Module: Mathlib.GroupTheory.FiniteAbelian.Basic

Goal state before:
pp: case neg
ι : Type
inst✝ : DecidableEq ι
p n : ι → ℕ
i : ι
x : ZMod (p i ^ n i)
h : ¬n i = 0
⊢ (directSumNeZeroMulHom p n) ((DirectSum.of (fun j ↦ ZMod (p ↑j ^ n ↑j)) ⟨i, h⟩) x) =
    (DirectSum.of (fun i ↦ ZMod (p i ^ n i)) i) x

Tactic:
simp_rw [directSumNeZeroMulHom, DirectSum.toAddMonoid_of]

Goal state after:
Module: Mathlib.Data.PNat.Prime

Goal state before:
pp: p : ℕ+
⊢ p.Prime → p ≠ 1

Tactic:
by
  intro pp contra
  apply Nat.Prime.ne_one pp
  rw [PNat.coe_eq_one_iff]
  apply contra

Goal state after:
Module: Mathlib.NumberTheory.ArithmeticFunction.Moebius

Goal state before:
pp: n : ℕ
⊢ (μ * ↑ζ) n = 1 n

Tactic:
induction n using recOnPosPrimePosCoprime with
  | zero => rw [map_zero, map_zero]
  | one => simp
  | prime_pow p n hp hn =>
    rw [coe_mul_zeta_apply, sum_divisors_prime_pow hp, sum_range_succ']
    simp [moebius_apply_prime_pow, hp.ne_one, hn.ne', hp, hn]
  | coprime a b _ha _hb hab ha' hb' =>
    rw [IsMultiplicative.map_mul_of_coprime _ hab, ha', hb',
      IsMultiplicative.map_mul_of_coprime isMultiplicative_one hab]
    exact isMultiplicative_moebius.mul isMultiplicative_zeta.natCast

Goal state after: