mathlib-initiative/mathlib-tactics huggingface dataset:
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
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 g : 𝓓^{n}_{K}(E, F₁)
hφ : IntegrableOn φ (↑K) μ
⊢ ∫ (x : E), (B (f x + g x)) (φ x) ∂μ = ∫ (x : E), (B (f x)) (φ x) ∂μ + ∫ (x : E), (B (g x)) (φ x) ∂μ

Tactic:
map_add,

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
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 g : 𝓓^{n}_{K}(E, F₁)
hφ : IntegrableOn φ (↑K) μ
⊢ ∫ (x : E), (B (f x) + B (g x)) (φ x) ∂μ = ∫ (x : E), (B (f x)) (φ x) ∂μ + ∫ (x : E), (B (g x)) (φ x) ∂μ
Module: Mathlib.Analysis.Normed.Module.Bases

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
X : Type u_2
inst✝¹ : NormedAddCommGroup X
inst✝ : NormedSpace 𝕜 X
β : Type u_3
L : SummationFilter β
b : GeneralSchauderBasis β 𝕜 X L
⊢ b.proj ∅ = 0

Tactic:
simp [proj]

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
β : 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 β
hdecomp :
  (GeneralSchauderBasis.proj b A) x =
    (GeneralSchauderBasis.proj b (A ∩ A₀)) x + (GeneralSchauderBasis.proj b (A \ A₀)) x
htail : ‖(GeneralSchauderBasis.proj b (A \ A₀)) x‖ < 1
⊢ ‖(GeneralSchauderBasis.proj b (A ∩ A₀)) x‖ ≤
    (Finset.image (fun B ↦ ‖(GeneralSchauderBasis.proj b B) x‖) A₀.powerset).sup' ⋯ _root_.id

Tactic:
exact Finset.le_sup' id <| Finset.mem_image_of_mem (fun B ↦ ‖b.proj B x‖)
      (Finset.mem_powerset.2 Finset.inter_subset_right)

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

Goal state before:
pp: ι : Type u_1
𝕜 : Type u_2
inst✝³ : RCLike 𝕜
G : ι → Type u_4
inst✝² : (i : ι) → NormedAddCommGroup (G i)
inst✝¹ : (i : ι) → InnerProductSpace 𝕜 (G i)
inst✝ : DecidableEq ι
i : ι
a : G i
f : ↥(lp G 2)
⊢ ⟪lp.single 2 i a, f⟫ = ⟪a, ↑f i⟫

Tactic:
refine (hasSum_inner (lp.single 2 i a) f).unique ?_

Goal state after:
ι : Type u_1
𝕜 : Type u_2
inst✝³ : RCLike 𝕜
G : ι → Type u_4
inst✝² : (i : ι) → NormedAddCommGroup (G i)
inst✝¹ : (i : ι) → InnerProductSpace 𝕜 (G i)
inst✝ : DecidableEq ι
i : ι
a : G i
f : ↥(lp G 2)
⊢ HasSum (fun i_1 ↦ ⟪↑(lp.single 2 i a) i_1, ↑f i_1⟫) ⟪a, ↑f i⟫
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
inst✝ : ∀ (i : ι), CompleteSpace (G i)
hVortho : OrthogonalFamily 𝕜 G V
hVtotal : ⊤ ≤ (⨆ i, (V i).range).topologicalClosure
⊢ Function.Surjective ⇑hVortho.linearIsometry

Tactic:
rw [← LinearIsometry.coe_toLinearMap]

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
inst✝ : ∀ (i : ι), CompleteSpace (G i)
hVortho : OrthogonalFamily 𝕜 G V
hVtotal : ⊤ ≤ (⨆ i, (V i).range).topologicalClosure
⊢ Function.Surjective ⇑hVortho.linearIsometry.toLinearMap
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
inst✝ : ∀ (i : ι), CompleteSpace (G i)
hVortho : OrthogonalFamily 𝕜 G V
hVtotal : ⊤ ≤ (⨆ i, (V i).range).topologicalClosure
⊢ Function.Surjective ⇑hVortho.linearIsometry

Tactic:
by
      rw [← LinearIsometry.coe_toLinearMap]
      exact LinearMap.range_eq_top.mp
        (eq_top_iff.mpr <| hVtotal.trans_eq hVortho.range_linearIsometry.symm)

Goal state after:
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
s : Set E
hs : Orthonormal 𝕜 Subtype.val
w : Set E
hws : w ⊇ s
hw_ortho : Orthonormal 𝕜 Subtype.val
hw_max : ∀ u ⊇ w, Orthonormal 𝕜 Subtype.val → u = w
⊢ (span 𝕜 (Set.range Subtype.val))ᗮ = ⊥

Tactic:
by simpa only [Subtype.range_coe_subtype, Set.ofPred_mem_eq,
      maximal_orthonormal_iff_orthogonalComplement_eq_bot hw_ortho] using hw_max

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

Tactic:
by
  let F : W → V → E := fun w' v ↦ 𝐞 (-L v w') • f v
  let F' : W → V → W →L[ℝ] E := fun w' v ↦ 𝐞 (-L v w') • fourierSMulRight L f v
  let B : V → ℝ := fun v ↦ 2 * π * ‖L‖ * ‖v‖ * ‖f v‖
  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
  have h1 : ∀ᶠ w' in 𝓝 w, AEStronglyMeasurable (F w') μ :=
    Eventually.of_forall (fun w' ↦ (h0 w').aestronglyMeasurable)
  have h3 : AEStronglyMeasurable (F' w) μ := by
    refine .fun_smul ?_ hf.1.fourierSMulRight
    refine (continuous_fourierChar.comp ?_).aestronglyMeasurable
    fun_prop
  have h4 : (∀ᵐ v ∂μ, ∀ (w' : W), w' ∈ Metric.ball w 1 → ‖F' w' v‖ ≤ B v) := by
    filter_upwards with v w' _
    rw [Circle.norm_smul _ (fourierSMulRight L f v)]
    exact norm_fourierSMulRight_le L f v
  have h5 : Integrable B μ := by simpa only [← mul_assoc] using hf'.const_mul (2 * π * ‖L‖)
  have h6 : ∀ᵐ v ∂μ, ∀ w', w' ∈ Metric.ball w 1 → HasFDerivAt (fun x ↦ F x v) (F' w' v) w' :=
    ae_of_all _ (fun v w' _ ↦ hasFDerivAt_fourierChar_smul L f v w')
  exact hasFDerivAt_integral_of_dominated_of_fderiv_le (Metric.ball_mem_nhds _ one_pos) h1 (h0 w)
    h3 h4 h5 h6

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

Goal state before:
pp: 𝕜 : Type u_2
F : Type u_6
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : NormedField 𝕜
inst✝¹ : NormedSpace 𝕜 F
inst✝ : SMulCommClass ℝ 𝕜 F
k n : ℕ
f : 𝓢(ℝ, F)
M : ℝ
hMp : 0 ≤ M
hM : ∀ (x : ℝ), |x| ^ k * ‖iteratedDeriv n (⇑f) x‖ ≤ M
⊢ ∀ (x : ℝ), ‖x‖ ^ k * ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤ M

Tactic:
simpa only [Real.norm_eq_abs, norm_iteratedFDeriv_eq_norm_iteratedDeriv]

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
K : ℕ∞ω
C : ℝ
hf : ContDiff ℝ K f
n k : ℕ
hk : ↑k ≤ K
v : V
hv : ∀ i ≤ k, ∀ j ≤ n, ‖v‖ ^ j * ‖iteratedFDeriv ℝ i f v‖ ≤ C
T : (W →L[ℝ] ℝ) [×n]→L[ℝ] W [×n]→L[ℝ] ℝ := ⋯
I₁ : ∀ (m : ℕ), ‖iteratedFDeriv ℝ m ⇑T fun x ↦ L v‖ ≤ ↑(n.descFactorial m) * 1 * (‖L‖ * ‖v‖) ^ (n - m)
m : ℕ
⊢ ‖iteratedFDeriv ℝ m (⇑T) ((ContinuousLinearMap.pi fun x ↦ L) v)‖ ≤ ↑(n.descFactorial m) * 1 * (‖L‖ * ‖v‖) ^ (n - m)

Tactic:
exact I₁ m

Goal state after:
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
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup D
inst✝¹ : NormedSpace ℝ D
inst✝ : NormedSpace 𝕜 F
K : ℝ≥0
g : D → E
hg : Function.HasTemperateGrowth g
h'g : AntilipschitzWith K g
⊢ 𝓢(E, F) →L[𝕜] 𝓢(D, F)

Tactic:
refine compCLM 𝕜 hg ⟨1, K * max 1 ‖g 0‖, fun x ↦ ?_⟩
  calc
  ‖x‖ ≤ K * ‖g x - g 0‖ := by
    rw [← dist_zero_right, ← dist_eq_norm]
    apply h'g.le_mul_dist
  _ ≤ K * (‖g x‖ + ‖g 0‖) := by
    gcongr
    exact norm_sub_le _ _
  _ ≤ K * (‖g x‖ + max 1 ‖g 0‖) := by
    gcongr
    exact le_max_right _ _
  _ ≤ (K * max 1 ‖g 0‖ : ℝ) * (1 + ‖g x‖) ^ 1 := by
    simp only [mul_add, add_comm (K * ‖g x‖), pow_one, mul_one, add_le_add_iff_left]
    gcongr
    exact le_mul_of_one_le_right (by positivity) (le_max_left _ _)

Goal state after:
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✝¹ : 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
⊢ fourierPowSMulRight (-L.flip) (iteratedFDeriv ℝ k (fourierIntegral 𝐞 μ (ContinuousLinearMap.toLinearMap₁₂ L) f)) w n =
    fourierIntegral 𝐞 μ (ContinuousLinearMap.toLinearMap₁₂ L) (iteratedFDeriv ℝ n fun v ↦ fourierPowSMulRight L f v k) w

Tactic:
rw [fourierIntegral_iteratedFDeriv (N := N) _ (hf.fourierPowSMulRight _ _) _ hn]

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✝¹ : 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
⊢ fourierPowSMulRight (-L.flip) (iteratedFDeriv ℝ k (fourierIntegral 𝐞 μ (ContinuousLinearMap.toLinearMap₁₂ L) f)) w n =
    (fun w ↦
        fourierPowSMulRight (-L.flip)
          (fourierIntegral 𝐞 μ (ContinuousLinearMap.toLinearMap₁₂ L) fun v ↦ fourierPowSMulRight L f v k) w n)
      w

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
⊢ ∀ (n : ℕ), ↑n ≤ N → Integrable (iteratedFDeriv ℝ n fun v ↦ fourierPowSMulRight L f v k) μ
Module: Mathlib.Analysis.Distribution.SchwartzSpace.Basic

Goal state before:
pp: case h
ι : 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✝⁸ : 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
n : ℕ
h : Integrable (fun x ↦ (1 + ‖x‖) ^ (-↑n)) μ
m : ℕ × ℕ := (n, 0)
f : 𝓢(D, V)
h' : ∀ (x : D), ‖f x‖ ≤ (1 + ‖x‖) ^ (-↑n) * (2 ^ n * ((Finset.Iic m).sup fun m' ↦ SchwartzMap.seminorm 𝕜 m'.1 m'.2) f)
⊢ (∫ (a : D), (1 + ‖a‖) ^ (-↑n) ∂μ) * (2 ^ n * ((Finset.Iic m).sup fun m' ↦ SchwartzMap.seminorm 𝕜 m'.1 m'.2) f) ≤
    (2 ^ n * ∫ (x : D), (1 + ‖x‖) ^ (-↑n) ∂μ) * ((Finset.Iic m).sup fun m ↦ SchwartzMap.seminorm 𝕜 m.1 m.2) f

Tactic:
← mul_assoc,

Goal state after:
case h
ι : 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✝⁸ : 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
n : ℕ
h : Integrable (fun x ↦ (1 + ‖x‖) ^ (-↑n)) μ
m : ℕ × ℕ := (n, 0)
f : 𝓢(D, V)
h' : ∀ (x : D), ‖f x‖ ≤ (1 + ‖x‖) ^ (-↑n) * (2 ^ n * ((Finset.Iic m).sup fun m' ↦ SchwartzMap.seminorm 𝕜 m'.1 m'.2) f)
⊢ (∫ (a : D), (1 + ‖a‖) ^ (-↑n) ∂μ) * 2 ^ n * ((Finset.Iic m).sup fun m' ↦ SchwartzMap.seminorm 𝕜 m'.1 m'.2) f ≤
    (2 ^ n * ∫ (x : D), (1 + ‖x‖) ^ (-↑n) ∂μ) * ((Finset.Iic m).sup fun m ↦ SchwartzMap.seminorm 𝕜 m.1 m.2) f
Module: Mathlib.MeasureTheory.Integral.PeakFunction

Goal state before:
pp: E : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : CompleteSpace E
F : Type u_4
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : FiniteDimensional ℝ F
inst✝² : MeasurableSpace F
inst✝¹ : BorelSpace F
μ : Measure F
inst✝ : μ.IsAddHaarMeasure
φ : F → ℝ
hφ : ∀ (x : F), 0 ≤ φ x
h'φ : ∫ (x : F), φ x ∂μ = 1
h : Tendsto (fun x ↦ ‖x‖ ^ finrank ℝ F * φ x) (cobounded F) (𝓝 0)
g : F → E
hg : Integrable g μ
h'g : ContinuousAt g 0
I : Integrable φ μ
this : Tendsto (fun c ↦ ∫ (x : F) in closedBall 0 c, φ x ∂μ) atTop (𝓝 1)
c : ℝ
hc : 0 < c
⊢ ∫ (x : F) in closedBall 0 c, φ x ∂μ =
    c ^ finrank ℝ F * ((c ^ finrank ℝ F)⁻¹ * ∫ (x : F) in c • closedBall 0 1, φ x ∂μ)

Tactic:
← mul_assoc,

Goal state after:
E : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : CompleteSpace E
F : Type u_4
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : FiniteDimensional ℝ F
inst✝² : MeasurableSpace F
inst✝¹ : BorelSpace F
μ : Measure F
inst✝ : μ.IsAddHaarMeasure
φ : F → ℝ
hφ : ∀ (x : F), 0 ≤ φ x
h'φ : ∫ (x : F), φ x ∂μ = 1
h : Tendsto (fun x ↦ ‖x‖ ^ finrank ℝ F * φ x) (cobounded F) (𝓝 0)
g : F → E
hg : Integrable g μ
h'g : ContinuousAt g 0
I : Integrable φ μ
this : Tendsto (fun c ↦ ∫ (x : F) in closedBall 0 c, φ x ∂μ) atTop (𝓝 1)
c : ℝ
hc : 0 < c
⊢ ∫ (x : F) in closedBall 0 c, φ x ∂μ = c ^ finrank ℝ F * (c ^ finrank ℝ F)⁻¹ * ∫ (x : F) in c • closedBall 0 1, φ x ∂μ
Module: Mathlib.MeasureTheory.Measure.Lebesgue.Integral

Goal state before:
pp: α : Type u_1
inst✝¹ : MeasurableSpace α
μ : Measure α
f g : α → ℝ
s : Set α
inst✝ : SigmaFinite μ
f_int : IntegrableOn f s μ
g_int : IntegrableOn g s μ
hs : MeasurableSet s
hfg : f ≤ᵐ[μ.restrict s] g
⊢ (μ.prod volume) (regionBetween f g s) = ENNReal.ofReal (∫ (y : α) in s, (g - f) y ∂μ)

Tactic:
have h : g - f =ᵐ[μ.restrict s] fun x => Real.toNNReal (g x - f x) :=
    hfg.mono fun x hx => (Real.coe_toNNReal _ <| sub_nonneg.2 hx).symm
  rw [volume_regionBetween_eq_lintegral f_int.aemeasurable g_int.aemeasurable hs,
    integral_congr_ae h, lintegral_congr_ae,
    lintegral_coe_eq_integral _ ((integrable_congr h).mp (g_int.sub f_int))]
  rfl

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

Goal state before:
pp: case refine_1
E : Type u_1
inst✝ : NormedAddCommGroup E
f : C(ℝ, E)
hf : Summable fun n ↦ ‖ContinuousMap.restrict (Icc 0 1) (f.comp (ContinuousMap.addRight ↑n))‖
n : ℤ
⊢ ‖ContinuousMap.restrict (↑{ carrier := Icc (↑n) (↑n + 1), isCompact' := ⋯ }) f‖ *
      volume.real ↑{ carrier := Icc (↑n) (↑n + 1), isCompact' := ⋯ } ≤
    ‖ContinuousMap.restrict (Icc 0 1) (f.comp (ContinuousMap.addRight ↑n))‖

pp: case refine_2
E : Type u_1
inst✝ : NormedAddCommGroup E
f : C(ℝ, E)
hf : Summable fun n ↦ ‖ContinuousMap.restrict (Icc 0 1) (f.comp (ContinuousMap.addRight ↑n))‖
⊢ ⋃ i, ↑{ carrier := Icc (↑i) (↑i + 1), isCompact' := ⋯ } = univ

Tactic:
· simp only [Compacts.coe_mk, le_add_iff_nonneg_right, zero_le_one, volume_real_Icc_of_le,
      add_sub_cancel_left, mul_one, norm_le _ (norm_nonneg _), ContinuousMap.restrict_apply]
    intro x
    have := ((f.comp <| ContinuousMap.addRight n).restrict (Icc 0 1)).norm_coe_le_norm
        ⟨x - n, ⟨sub_nonneg.mpr x.2.1, sub_le_iff_le_add'.mpr x.2.2⟩⟩
    simpa only [ContinuousMap.restrict_apply, comp_apply, coe_addRight, Subtype.coe_mk,
      sub_add_cancel] using this

Goal state after:
case refine_2
E : Type u_1
inst✝ : NormedAddCommGroup E
f : C(ℝ, E)
hf : Summable fun n ↦ ‖ContinuousMap.restrict (Icc 0 1) (f.comp (ContinuousMap.addRight ↑n))‖
⊢ ⋃ i, ↑{ carrier := Icc (↑i) (↑i + 1), isCompact' := ⋯ } = univ
Module: Mathlib.Analysis.SpecialFunctions.ImproperIntegrals

Goal state before:
pp: c : ℝ
⊢ Tendsto (fun i ↦ ∫ (x : ℝ) in id i..c, rexp x) atBot (𝓝 (rexp c))

Tactic:
simp_rw [integral_exp, show 𝓝 (exp c) = 𝓝 (exp c - 0) by rw [sub_zero]]

Goal state after:
c : ℝ
⊢ Tendsto (fun i ↦ rexp c - rexp (id i)) atBot (𝓝 (rexp c - 0))
Module: Mathlib.Analysis.SpecialFunctions.ImproperIntegrals

Goal state before:
pp: a : ℂ
ha : 0 < a.re
c : ℝ
⊢ IntegrableOn (fun x ↦ Complex.exp (a * ↑x)) (Iic c) volume

Tactic:
by
  simpa using Iff.mpr integrableOn_Iic_iff_integrableOn_Iio
    (integrableOn_exp_mul_complex_Ioi (a := -a) (by simpa) (-c)).comp_neg_Iio

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

Goal state before:
pp: case hg
V : Type u_1
W : Type u_2
E : Type u_3
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace ℂ E
inst✝⁹ : NormedAddCommGroup V
inst✝⁸ : InnerProductSpace ℝ V
inst✝⁷ : MeasurableSpace V
inst✝⁶ : BorelSpace V
inst✝⁵ : NormedAddCommGroup W
inst✝⁴ : InnerProductSpace ℝ W
inst✝³ : MeasurableSpace W
inst✝² : BorelSpace W
inst✝¹ : FiniteDimensional ℝ W
inst✝ : FiniteDimensional ℝ V
f g : ↥(Lp E 1 volume)
x : V
⊢ Integrable (fun v ↦ 𝐞 (-⟪v, x⟫) • ↑↑g v) volume

Tactic:
rw [Real.fourierIntegral_convergent_iff]
          exact L1.integrable_coeFn g

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

Goal state before:
pp: p s : ℝ
hs : -1 < s
hp : 0 < p
ht : 0 < (s + 1) / p
x : ℝ
hx : x ∈ Ioi 0
⊢ x ^ (p - 1) * ((x ^ p) ^ ((s + 1) / p - 1) * rexp (-x ^ p)) = x ^ s * rexp (-x ^ p)

Tactic:
← mul_assoc,

Goal state after:
p s : ℝ
hs : -1 < s
hp : 0 < p
ht : 0 < (s + 1) / p
x : ℝ
hx : x ∈ Ioi 0
⊢ x ^ (p - 1) * (x ^ p) ^ ((s + 1) / p - 1) * rexp (-x ^ p) = x ^ s * rexp (-x ^ p)
Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral

Goal state before:
pp: p s b : ℝ
hs : -1 < s
hp : 0 < p
hb : 0 < b
hib : 0 < b ^ (-p⁻¹)
this : IntegrableOn (fun x ↦ (b ^ (-p⁻¹)) ^ s * (x ^ s * rexp (-x ^ p))) (Ioi 0) volume
x✝ : ℝ
hx : x✝ ∈ Ioi 0
⊢ (b ^ (-p⁻¹)) ^ s * (x✝ ^ s * rexp (-x✝ ^ p)) = (b ^ (-p⁻¹) * x✝) ^ s * rexp (-b * (b ^ (-p⁻¹) * x✝) ^ p)

Tactic:
← mul_assoc,

Goal state after:
p s b : ℝ
hs : -1 < s
hp : 0 < p
hb : 0 < b
hib : 0 < b ^ (-p⁻¹)
this : IntegrableOn (fun x ↦ (b ^ (-p⁻¹)) ^ s * (x ^ s * rexp (-x ^ p))) (Ioi 0) volume
x✝ : ℝ
hx : x✝ ∈ Ioi 0
⊢ (b ^ (-p⁻¹)) ^ s * x✝ ^ s * rexp (-x✝ ^ p) = (b ^ (-p⁻¹) * x✝) ^ s * rexp (-b * (b ^ (-p⁻¹) * x✝) ^ p)
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic

Goal state before:
pp: s : ℂ
h2 : s ≠ 0
n : ℕ := ⌊1 - s.re⌋₊
t1 : -s.re < ↑n
t2 : -(s + 1).re < ↑n
⊢ Gamma (s + 1) = s * GammaAux n s

Tactic:
Gamma_eq_GammaAux (s + 1) n t2,

Goal state after:
s : ℂ
h2 : s ≠ 0
n : ℕ := ⌊1 - s.re⌋₊
t1 : -s.re < ↑n
t2 : -(s + 1).re < ↑n
⊢ GammaAux n (s + 1) = s * GammaAux n s
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic

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

Tactic:
by
    simp [Gamma, this]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic

Goal state before:
pp: s : ℂ
⊢ Gamma ((starRingEnd ℂ) s) = (starRingEnd ℂ) (Gamma s)

Tactic:
suffices ∀ (n : ℕ) (s : ℂ), GammaAux n (conj s) = conj (GammaAux n s) by
    simp [Gamma, this]

Goal state after:
s : ℂ
⊢ ∀ (n : ℕ) (s : ℂ), GammaAux n ((starRingEnd ℂ) s) = (starRingEnd ℂ) (GammaAux n s)
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic

Goal state before:
pp: case succ
s✝ : ℂ
n : ℕ
IH : ∀ (s : ℂ), GammaAux n ((starRingEnd ℂ) s) = (starRingEnd ℂ) (GammaAux n s)
s : ℂ
⊢ (starRingEnd ℂ) s + 1 = (starRingEnd ℂ) (s + 1)

Tactic:
map_add,

Goal state after:
case succ
s✝ : ℂ
n : ℕ
IH : ∀ (s : ℂ), GammaAux n ((starRingEnd ℂ) s) = (starRingEnd ℂ) (GammaAux n s)
s : ℂ
⊢ (starRingEnd ℂ) s + 1 = (starRingEnd ℂ) s + (starRingEnd ℂ) 1
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic

Goal state before:
pp: a : ℂ
r : ℝ
ha : 0 < a.re
hr : 0 < r
aux : (1 / ↑r) ^ a = 1 / ↑r * (1 / ↑r) ^ (a - 1)
x : ℝ
hx : 0 < x
⊢ ↑x ^ (a - 1) * cexp (-(↑r * ↑x)) = (1 / ↑r) ^ (a - 1) * (↑r ^ (a - 1) * ↑x ^ (a - 1)) * cexp (-(↑r * ↑x))

Tactic:
← mul_assoc,

Goal state after:
a : ℂ
r : ℝ
ha : 0 < a.re
hr : 0 < r
aux : (1 / ↑r) ^ a = 1 / ↑r * (1 / ↑r) ^ (a - 1)
x : ℝ
hx : 0 < x
⊢ ↑x ^ (a - 1) * cexp (-(↑r * ↑x)) = (1 / ↑r) ^ (a - 1) * ↑r ^ (a - 1) * ↑x ^ (a - 1) * cexp (-(↑r * ↑x))
Module: Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform

Goal state before:
pp: b : ℂ
hb : 0 < b.re
c : ℝ
⊢ Tendsto (fun x ↦ b.re * (x * x) - 2 * |b.im| * |c| * x) atTop atTop

Tactic:
← mul_assoc,

Goal state after:
b : ℂ
hb : 0 < b.re
c : ℝ
⊢ Tendsto (fun x ↦ b.re * x * x - 2 * |b.im| * |c| * x) atTop atTop
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic

Goal state before:
pp: ⊢ Gamma 1 = 1

Tactic:
rw [Gamma, Complex.ofReal_one, Complex.Gamma_one, Complex.one_re]

Goal state after: