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

Goal state before:
pp: α : Type u_1
inst✝⁶ : TopologicalSpace α
inst✝⁵ : NormalSpace α
inst✝⁴ : MeasurableSpace α
inst✝³ : BorelSpace α
E : Type u_2
inst✝² : NormedAddCommGroup E
μ : Measure α
p : ℝ≥0∞
inst✝¹ : NormedSpace ℝ E
inst✝ : μ.WeaklyRegular
hp : p ≠ ∞
f : α → E
hf : MemLp f p μ
ε : ℝ≥0∞
hε : ε ≠ 0
⊢ ∀ (c : E) ⦃s : Set α⦄,
    MeasurableSet s →
      μ s < ∞ →
        ∀ {ε : ℝ≥0∞},
          ε ≠ 0 →
            ∃ g,
              eLpNorm (g - s.indicator fun x ↦ c) p μ ≤ ε ∧
                Continuous[inst✝⁶, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] g ∧
                  MemLp g p μ ∧ IsBounded (range g)

Tactic:
intro c t ht htμ ε hε

Goal state after:
α : Type u_1
inst✝⁶ : TopologicalSpace α
inst✝⁵ : NormalSpace α
inst✝⁴ : MeasurableSpace α
inst✝³ : BorelSpace α
E : Type u_2
inst✝² : NormedAddCommGroup E
μ : Measure α
p : ℝ≥0∞
inst✝¹ : NormedSpace ℝ E
inst✝ : μ.WeaklyRegular
hp : p ≠ ∞
f : α → E
hf : MemLp f p μ
ε✝ : ℝ≥0∞
hε✝ : ε✝ ≠ 0
c : E
t : Set α
ht : MeasurableSet t
htμ : μ t < ∞
ε : ℝ≥0∞
hε : ε ≠ 0
⊢ ∃ g,
    eLpNorm (g - t.indicator fun x ↦ c) p μ ≤ ε ∧
      Continuous[inst✝⁶, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] g ∧ MemLp g p μ ∧ IsBounded (range g)
Module: Mathlib.MeasureTheory.Function.ContinuousMapDense

Goal state before:
pp: α : Type u_1
inst✝⁶ : TopologicalSpace α
inst✝⁵ : NormalSpace α
inst✝⁴ : MeasurableSpace α
inst✝³ : BorelSpace α
E : Type u_2
inst✝² : NormedAddCommGroup E
μ : Measure α
inst✝¹ : NormedSpace ℝ E
inst✝ : μ.WeaklyRegular
f : α → E
hf : Integrable f μ
ε : ℝ
hε : 0 < ε
⊢ ∃ g, ∫ (x : α), ‖f x - g x‖ ∂μ ≤ ε ∧ Integrable (⇑g) μ

Tactic:
simp only [← memLp_one_iff_integrable, ← ENNReal.ofReal_one]
    at hf ⊢

Goal state after:
α : Type u_1
inst✝⁶ : TopologicalSpace α
inst✝⁵ : NormalSpace α
inst✝⁴ : MeasurableSpace α
inst✝³ : BorelSpace α
E : Type u_2
inst✝² : NormedAddCommGroup E
μ : Measure α
inst✝¹ : NormedSpace ℝ E
inst✝ : μ.WeaklyRegular
f : α → E
ε : ℝ
hε : 0 < ε
hf : MemLp f (ENNReal.ofReal 1) μ
⊢ ∃ g, ∫ (x : α), ‖f x - g x‖ ∂μ ≤ ε ∧ MemLp (⇑g) (ENNReal.ofReal 1) μ
Module: Mathlib.MeasureTheory.Function.ContinuousMapDense

Goal state before:
pp: α : Type u_1
inst✝⁸ : TopologicalSpace α
inst✝⁷ : NormalSpace α
inst✝⁶ : MeasurableSpace α
inst✝⁵ : BorelSpace α
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
μ : Measure α
p : ℝ≥0∞
inst✝³ : NormedSpace ℝ E
inst✝² : SecondCountableTopologyEither α E
inst✝¹ : Fact (1 ≤ p)
hp : p ≠ ∞
inst✝ : μ.WeaklyRegular
f : ↥(Lp E p μ)
ε : ℝ≥0∞
hε : 0 < ε
⊢ ∃ y ∈ ↑(boundedContinuousFunction E p μ), y ∈ Metric.closedEBall f ε

Tactic:
obtain ⟨g, hg, g_mem⟩ :
      ∃ g : α →ᵇ E, eLpNorm ((f : α → E) - (g : α → E)) p μ ≤ ε ∧ MemLp g p μ :=
    (Lp.memLp f).exists_boundedContinuous_eLpNorm_sub_le hp hε.ne'

Goal state after:
α : Type u_1
inst✝⁸ : TopologicalSpace α
inst✝⁷ : NormalSpace α
inst✝⁶ : MeasurableSpace α
inst✝⁵ : BorelSpace α
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
μ : Measure α
p : ℝ≥0∞
inst✝³ : NormedSpace ℝ E
inst✝² : SecondCountableTopologyEither α E
inst✝¹ : Fact (1 ≤ p)
hp : p ≠ ∞
inst✝ : μ.WeaklyRegular
f : ↥(Lp E p μ)
ε : ℝ≥0∞
hε : 0 < ε
g : α →ᵇ E
hg : eLpNorm (↑↑f - ⇑g) p μ ≤ ε
g_mem : MemLp (⇑g) p μ
⊢ ∃ y ∈ ↑(boundedContinuousFunction E p μ), y ∈ Metric.closedEBall f ε
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)
⊢ HasSum (fun i_1 ↦ ⟪↑(lp.single 2 i a) i_1, ↑f i_1⟫) ⟪a, ↑f i⟫

Tactic:
lp.coeFn_single

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 ↦ ⟪Pi.single i a i_1, ↑f i_1⟫) ⟪a, ↑f i⟫
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
D : RankOneDecomposition 𝕜 X
⊢ D.basis.proj = D.P

Tactic:
ext n _

Goal state after:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
X : Type u_2
inst✝¹ : NormedAddCommGroup X
inst✝ : NormedSpace 𝕜 X
D : RankOneDecomposition 𝕜 X
n : ℕ
x✝ : X
⊢ (D.basis.proj n) x✝ = (D.P n) x✝
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
f : ↥(lp (fun x ↦ 𝕜) 2)
⊢ HasSum (fun i ↦ ↑f i • b i) (b.repr.symm f)

Tactic:
by
  classical
  suffices H : (fun i : ι => f i • b i) = fun b_1 : ι => b.repr.symm.toContinuousLinearEquiv <|
      (fun i : ι => lp.single 2 i (f i) (E := (fun _ : ι => 𝕜))) b_1 by
    rw [H]
    have : HasSum (fun i : ι => lp.single 2 i (f i)) f := lp.hasSum_single ENNReal.ofNat_ne_top f
    exact (↑b.repr.symm.toContinuousLinearEquiv : ℓ²(ι, 𝕜) →L[𝕜] E).hasSum this
  ext i
  apply b.repr.injective
  let : NormedSpace 𝕜 (lp (fun _i : ι => 𝕜) 2) := by infer_instance
  have : lp.single (E := (fun _ : ι => 𝕜)) 2 i (f i * 1) = f i • lp.single 2 i 1 :=
    lp.single_smul (E := (fun _ : ι => 𝕜)) 2 i (f i) (1 : 𝕜)
  rw [mul_one] at this
  rw [map_smul, b.repr_self, ← this, LinearIsometryEquiv.coe_toContinuousLinearEquiv]
  exact (b.repr.apply_symm_apply (lp.single 2 i (f i))).symm

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

Goal state before:
pp: T : ℝ
n : ℤ
x : ℝ
⊢ HasDerivAt (fun y ↦ cexp (2 * ↑π * I * ↑n * y / ↑T)) (cexp (2 * ↑π * I * ↑n * ↑x / ↑T) * (2 * ↑π * I * ↑n / ↑T)) ↑x

Tactic:
refine (hasDerivAt_exp _).comp (x : ℂ) ?_

Goal state after:
T : ℝ
n : ℤ
x : ℝ
⊢ HasDerivAt (fun y ↦ 2 * ↑π * I * ↑n * y / ↑T) (2 * ↑π * I * ↑n / ↑T) ↑x
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 t : Set α
φ : ι → α → ℝ
hs : MeasurableSet s
ht : MeasurableSet t
hts : t ⊆ s
h'ts : t ∈ 𝓝[s] x₀
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₀) (𝓝 0)
ε : ℝ
εpos : ε > 0
A : Tendsto (fun δ ↦ δ * ∫ (x : α) in s, ‖g x‖ ∂μ + 2 * δ) (𝓝[>] 0) (𝓝 (2 * 0))
⊢ ∃ δ, δ * ∫ (x : α) in s, ‖g x‖ ∂μ + 2 * δ < ε ∧ 0 < δ ∧ δ < 1

Tactic:
mul_zero

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 α
φ : ι → α → ℝ
hs : MeasurableSet s
ht : MeasurableSet t
hts : t ⊆ s
h'ts : t ∈ 𝓝[s] x₀
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₀) (𝓝 0)
ε : ℝ
εpos : ε > 0
A : Tendsto (fun δ ↦ δ * ∫ (x : α) in s, ‖g x‖ ∂μ + 2 * δ) (𝓝[>] 0) (𝓝 0)
⊢ ∃ δ, δ * ∫ (x : α) in s, ‖g x‖ ∂μ + 2 * δ < ε ∧ 0 < δ ∧ δ < 1
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
hnφ : ∀ (n : ℕ), ∀ x ∈ s, 0 ≤ φ n x
I : ∀ (n : ℕ), IntegrableOn (fun x ↦ c x ^ n) s μ
J : ∀ (n : ℕ), 0 ≤ᵐ[μ.restrict s] fun x ↦ c x ^ n
P : ∀ (n : ℕ), 0 < ∫ (x : α) in s, c x ^ n ∂μ
hiφ : ∀ (n : ℕ), ∫ (x : α) in s, φ n x ∂μ = 1
u : Set α
u_open : IsOpen[inst✝⁶] u
x₀u : x₀ ∈ u
t : ℝ
t_pos : 0 ≤ t
tx₀ : t < c x₀
ht : ∀ x ∈ s \ u, c x ≤ t
t' : ℝ
tt' : t < t'
t'x₀ : t' < c x₀
t'_pos : 0 < t'
v : Set α
v_open : IsOpen[inst✝⁶] v
x₀_v : x₀ ∈ v
hv : v ∩ s ⊆ c ⁻¹' Ioi t'
n : ℕ
x : α
hx : x ∈ s \ u
⊢ t' ^ n * μ.real (v ∩ s) = ∫ (x : α) in v ∩ s, t' ^ n ∂μ

Tactic:
by simp [mul_comm]

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✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAlgebra ℝ 𝕜
inst✝⁴ : NormedAddCommGroup D
inst✝³ : NormedSpace ℝ D
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace ℝ G
inst✝ : NormedSpace 𝕜 F
L : E →L[ℝ] G →L[ℝ] ℝ
⊢ ∀ (a : 𝕜) (f : 𝓢(E, F)) (x : E), (L x).smulRight ((a • f) x) = (RingHom.id 𝕜) a • (L x).smulRight (f x)

Tactic:
intro c

Goal state after:
ι : Type u_1
𝕜 : Type u_2
𝕜' : Type u_3
D : Type u_4
E : Type u_5
F : Type u_6
G : Type u_7
H : Type u_8
V : Type u_9
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace ℝ F
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAlgebra ℝ 𝕜
inst✝⁴ : NormedAddCommGroup D
inst✝³ : NormedSpace ℝ D
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace ℝ G
inst✝ : NormedSpace 𝕜 F
L : E →L[ℝ] G →L[ℝ] ℝ
c : 𝕜
⊢ ∀ (f : 𝓢(E, F)) (x : E), (L x).smulRight ((c • f) x) = (RingHom.id 𝕜) c • (L x).smulRight (f x)
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
hnφ : ∀ (n : ℕ), ∀ x ∈ s, 0 ≤ φ n x
I : ∀ (n : ℕ), IntegrableOn (fun x ↦ c x ^ n) s μ
J : ∀ (n : ℕ), 0 ≤ᵐ[μ.restrict s] fun x ↦ c x ^ n
P : ∀ (n : ℕ), 0 < ∫ (x : α) in s, c x ^ n ∂μ
hiφ : ∀ (n : ℕ), ∫ (x : α) in s, φ n x ∂μ = 1
u : Set α
u_open : IsOpen[inst✝⁶] u
x₀u : x₀ ∈ u
t : ℝ
t_pos : 0 ≤ t
tx₀ : t < c x₀
ht : ∀ x ∈ s \ u, c x ≤ t
t' : ℝ
tt' : t < t'
t'x₀ : t' < c x₀
t'_pos : 0 < t'
v : Set α
v_open : IsOpen[inst✝⁶] v
x₀_v : x₀ ∈ v
hv : v ∩ s ⊆ c ⁻¹' Ioi t'
M : ∀ (n : ℕ), ∀ x ∈ s \ u, φ n x ≤ (μ.real (v ∩ s))⁻¹ * (t / t') ^ n
N : Tendsto (fun n ↦ (μ.real (v ∩ s))⁻¹ * (t / t') ^ n) atTop (𝓝 ((μ.real (v ∩ s))⁻¹ * 0))
⊢ TendstoUniformlyOn φ 0 atTop (s \ u)

Tactic:
mul_zero

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₀
φ : ℕ → α → ℝ := fun n x ↦ (∫ (x : α) in s, c x ^ n ∂μ)⁻¹ * c x ^ n
hnφ : ∀ (n : ℕ), ∀ x ∈ s, 0 ≤ φ n x
I : ∀ (n : ℕ), IntegrableOn (fun x ↦ c x ^ n) s μ
J : ∀ (n : ℕ), 0 ≤ᵐ[μ.restrict s] fun x ↦ c x ^ n
P : ∀ (n : ℕ), 0 < ∫ (x : α) in s, c x ^ n ∂μ
hiφ : ∀ (n : ℕ), ∫ (x : α) in s, φ n x ∂μ = 1
u : Set α
u_open : IsOpen[inst✝⁶] u
x₀u : x₀ ∈ u
t : ℝ
t_pos : 0 ≤ t
tx₀ : t < c x₀
ht : ∀ x ∈ s \ u, c x ≤ t
t' : ℝ
tt' : t < t'
t'x₀ : t' < c x₀
t'_pos : 0 < t'
v : Set α
v_open : IsOpen[inst✝⁶] v
x₀_v : x₀ ∈ v
hv : v ∩ s ⊆ c ⁻¹' Ioi t'
M : ∀ (n : ℕ), ∀ x ∈ s \ u, φ n x ≤ (μ.real (v ∩ s))⁻¹ * (t / t') ^ n
N : Tendsto (fun n ↦ (μ.real (v ∩ s))⁻¹ * (t / t') ^ n) atTop (𝓝 0)
⊢ TendstoUniformlyOn φ 0 atTop (s \ u)
Module: Mathlib.Analysis.Fourier.FourierTransform

Goal state before:
pp: case e_f
𝕜 : 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✝¹ : MeasurableAdd V
e : AddChar 𝕜 𝕊
μ : Measure V
inst✝ : μ.IsAddRightInvariant
L : V →ₗ[𝕜] W →ₗ[𝕜] 𝕜
f : V → E
v₀ : V
w : W
v : V
⊢ ↑(e ((-L (v - v₀)) w)) • f v = ↑(e ((L v₀ - L v) w)) • f v

Tactic:
map_sub,

Goal state after:
case e_f
𝕜 : 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✝¹ : MeasurableAdd V
e : AddChar 𝕜 𝕊
μ : Measure V
inst✝ : μ.IsAddRightInvariant
L : V →ₗ[𝕜] W →ₗ[𝕜] 𝕜
f : V → E
v₀ : V
w : W
v : V
⊢ ↑(e ((-(L v - L v₀)) w)) • f v = ↑(e ((L v₀ - L v) w)) • f v
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
x₀ : F
hg : Integrable g μ
h'g : ContinuousAt g x₀
f : F → E := fun x ↦ g (x₀ - x)
⊢ Tendsto (fun c ↦ ∫ (x : F), (c ^ finrank ℝ F * φ (c • (x₀ - x))) • g x ∂μ) atTop (𝓝 (g x₀))

Tactic:
have If : Integrable f μ := by simpa [f, sub_eq_add_neg] using (hg.comp_add_left x₀).comp_neg

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
x₀ : F
hg : Integrable g μ
h'g : ContinuousAt g x₀
f : F → E := fun x ↦ g (x₀ - x)
If : Integrable f μ
⊢ Tendsto (fun c ↦ ∫ (x : F), (c ^ finrank ℝ F * φ (c • (x₀ - x))) • g x ∂μ) atTop (𝓝 (g x₀))
Module: Mathlib.MeasureTheory.Measure.Lebesgue.Integral

Goal state before:
pp: case neg
f : ℝ → ℝ
eq : ∫ (x : ℝ) in Ioi 0, f |x| = ∫ (x : ℝ) in Ioi 0, f x
hf : ¬IntegrableOn (fun x ↦ f |x|) (Ioi 0) volume
this : ¬Integrable (fun x ↦ f |x|) volume
⊢ 0 = 2 * 0

Tactic:
mul_zero

Goal state after:
case neg
f : ℝ → ℝ
eq : ∫ (x : ℝ) in Ioi 0, f |x| = ∫ (x : ℝ) in Ioi 0, f x
hf : ¬IntegrableOn (fun x ↦ f |x|) (Ioi 0) volume
this : ¬Integrable (fun x ↦ f |x|) volume
⊢ 0 = 0
Module: Mathlib.Analysis.SpecialFunctions.ImproperIntegrals

Goal state before:
pp: case e'_9
a : ℝ
ha : a < -1
c : ℝ
hc : 0 < c
x : ℝ
hx : x ∈ Ici c
⊢ x ^ a = (a + 1) * x ^ (a + 1 - 1) / (a + 1)

Tactic:
simp [show a + 1 ≠ 0 from ne_of_lt (by linarith), mul_comm]

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

Goal state before:
pp: s : ℂ
x : ℝ
hx : x ∈ Ioi 0
⊢ ↑(rexp (-x)) * cexp (↑(Real.log x) * ((starRingEnd ℂ) s - 1)) =
    ↑(rexp (-x)) * cexp (↑(Real.log x) * (starRingEnd ℂ) (s - 1))

Tactic:
map_sub,

Goal state after:
s : ℂ
x : ℝ
hx : x ∈ Ioi 0
⊢ ↑(rexp (-x)) * cexp (↑(Real.log x) * ((starRingEnd ℂ) s - 1)) =
    ↑(rexp (-x)) * cexp (↑(Real.log x) * ((starRingEnd ℂ) s - (starRingEnd ℂ) 1))
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
⊢ 0 = b ^ (-p⁻¹) * 0

Tactic:
mul_zero

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
⊢ 0 = 0
Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral

Goal state before:
pp: b : ℂ
hb : 0 < b.re
f : ℂ → ℝ → ℂ := fun c x ↦ cexp (-c * ↑x ^ 2)
d : ℝ
hd : 0 < d
hd' : d < b.re
⊢ ∀ x ∈ re ⁻¹' Ioi d, ∀ᵐ (x_1 : ℝ), ‖f x x_1‖ ≤ rexp (-d * x_1 ^ 2)

Tactic:
intro c

Goal state after:
b : ℂ
hb : 0 < b.re
f : ℂ → ℝ → ℂ := fun c x ↦ cexp (-c * ↑x ^ 2)
d : ℝ
hd : 0 < d
hd' : d < b.re
c : ℂ
⊢ c ∈ re ⁻¹' Ioi d → ∀ᵐ (x : ℝ), ‖f c x‖ ≤ rexp (-d * x ^ 2)
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic

Goal state before:
pp: case succ
n : ℕ
IH : Gamma (-↑n) = 0
A : -↑n.succ ≠ 0
this : -↑n = -↑n.succ + 1
⊢ Gamma (-↑(n + 1)) = 0

Tactic:
rw [this, Gamma_add_one _ A] at IH

Goal state after:
case succ
n : ℕ
IH : -↑n.succ * Gamma (-↑n.succ) = 0
A : -↑n.succ ≠ 0
this : -↑n = -↑n.succ + 1
⊢ Gamma (-↑(n + 1)) = 0
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic

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

Tactic:
nth_rewrite 2 [← cpow_one (1 / r : ℂ)]

Goal state after:
a : ℂ
r : ℝ
ha : 0 < a.re
hr : 0 < r
⊢ (1 / ↑r) ^ a = (1 / ↑r) ^ 1 * (1 / ↑r) ^ (a - 1)
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic

Goal state before:
pp: a : ℂ
r : ℝ
ha : 0 < a.re
hr : 0 < r
⊢ ∫ (t : ℝ) in Ioi 0, ↑t ^ (a - 1) * cexp (-(↑r * ↑t)) = (1 / ↑r) ^ a * Gamma a

Tactic:
have aux : (1 / r : ℂ) ^ a = 1 / r * (1 / r) ^ (a - 1) := by
    nth_rewrite 2 [← cpow_one (1 / r : ℂ)]
    rw [← cpow_add _ _ (one_div_ne_zero <| ofReal_ne_zero.mpr hr.ne'), add_sub_cancel]
  calc
    _ = ∫ (t : ℝ) in Ioi 0, (1 / r) ^ (a - 1) * (r * t) ^ (a - 1) * exp (-(r * t)) := by
      refine MeasureTheory.setIntegral_congr_fun measurableSet_Ioi (fun x hx ↦ ?_)
      rw [mem_Ioi] at hx
      rw [mul_cpow_ofReal_nonneg hr.le hx.le, ← mul_assoc, one_div, ← ofReal_inv,
        ← mul_cpow_ofReal_nonneg (inv_pos.mpr hr).le hr.le, ← ofReal_mul r⁻¹,
        inv_mul_cancel₀ hr.ne', ofReal_one, one_cpow, one_mul]
    _ = 1 / r * ∫ (t : ℝ) in Ioi 0, (1 / r) ^ (a - 1) * t ^ (a - 1) * exp (-t) := by
      simp_rw [← ofReal_mul]
      rw [integral_comp_mul_left_Ioi (fun x ↦ _ * x ^ (a - 1) * exp (-x)) _ hr, mul_zero,
        real_smul, ← one_div, ofReal_div, ofReal_one]
    _ = 1 / r * (1 / r : ℂ) ^ (a - 1) * (∫ (t : ℝ) in Ioi 0, t ^ (a - 1) * exp (-t)) := by
      simp_rw [← MeasureTheory.integral_const_mul, mul_assoc]
    _ = (1 / r) ^ a * Gamma a := by
      rw [aux, Gamma_eq_integral ha]
      congr 2 with x
      rw [ofReal_exp, ofReal_neg, mul_comm]

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

Goal state before:
pp: b : ℂ
hb : 0 < b.re
nv : ∀ {b : ℂ}, 0 < b.re → b ≠ 0
c : ℂ
hc : c ∈ {c | 0 < c.re}
⊢ (↑π / c) ^ (1 / 2) ≠ 0

Tactic:
· -- RHS doesn't vanish
    rw [Ne, cpow_eq_zero_iff, not_and_or]
    exact Or.inl (div_ne_zero (ofReal_ne_zero.mpr pi_ne_zero) (nv hc))

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

Goal state before:
pp: case h
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
v : V
h'f : ContinuousAt f v
φ : V → ℝ := fun w ↦ π ^ (↑(finrank ℝ V) / 2) * rexp (-π ^ 2 * ‖w‖ ^ 2)
A : Tendsto (fun w ↦ π ^ 2 * ‖w‖ ^ 2) (cobounded V) atTop
B :
  Tendsto
    (fun x ↦
      π ^ (-↑(finrank ℝ V) / 2) * ((fun x ↦ x ^ (↑(finrank ℝ V) / 2) * rexp (-1 * x)) ∘ fun w ↦ π ^ 2 * ‖w‖ ^ 2) x)
    (cobounded V) (𝓝 (π ^ (-↑(finrank ℝ V) / 2) * 0))
⊢ Tendsto (fun x ↦ ‖x‖ ^ finrank ℝ V * φ x) (cobounded V) (𝓝 0)

Tactic:
mul_zero

Goal state after:
case h
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
v : V
h'f : ContinuousAt f v
φ : V → ℝ := fun w ↦ π ^ (↑(finrank ℝ V) / 2) * rexp (-π ^ 2 * ‖w‖ ^ 2)
A : Tendsto (fun w ↦ π ^ 2 * ‖w‖ ^ 2) (cobounded V) atTop
B :
  Tendsto
    (fun x ↦
      π ^ (-↑(finrank ℝ V) / 2) * ((fun x ↦ x ^ (↑(finrank ℝ V) / 2) * rexp (-1 * x)) ∘ fun w ↦ π ^ 2 * ‖w‖ ^ 2) x)
    (cobounded V) (𝓝 0)
⊢ Tendsto (fun x ↦ ‖x‖ ^ finrank ℝ V * φ x) (cobounded V) (𝓝 0)
Module: Mathlib.Analysis.Fourier.Inversion

Goal state before:
pp: 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
hv : ContinuousAt f v
⊢ 𝓕 (𝓕⁻ f) v = f v

Tactic:
rw [fourierInv_comm]

Goal state after:
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
hv : ContinuousAt f v
⊢ 𝓕⁻ (𝓕 f) v = f v
Module: Mathlib.Analysis.Distribution.SchwartzSpace.Fourier

Goal state before:
pp: case h₂
𝕜 : Type u_1
inst✝⁹ : RCLike 𝕜
E : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℂ E
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : SMulCommClass ℂ 𝕜 E
V : Type u_3
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : FiniteDimensional ℝ V
inst✝¹ : MeasurableSpace V
inst✝ : BorelSpace V
k n : ℕ
f : 𝓢(V, E)
x : V
p : ℕ × ℕ
a✝ : p ∈ Finset.range (n + 1) ×ˢ Finset.range (k + 1)
⊢ (SchwartzMap.seminorm 𝕜 (p.1 + volume.integrablePower) p.2) f ≤
    ((Finset.range (n + volume.integrablePower + 1) ×ˢ Finset.range (k + 1)).sup (schwartzSeminormFamily 𝕜 V E)) f

Tactic:
have : (p.1 + integrablePower (volume : Measure V), p.2) ∈ Finset.range
            (n + integrablePower (volume : Measure V) + 1) ×ˢ Finset.range (k + 1) := by simp_all

Goal state after:
case h₂
𝕜 : Type u_1
inst✝⁹ : RCLike 𝕜
E : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℂ E
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : SMulCommClass ℂ 𝕜 E
V : Type u_3
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : FiniteDimensional ℝ V
inst✝¹ : MeasurableSpace V
inst✝ : BorelSpace V
k n : ℕ
f : 𝓢(V, E)
x : V
p : ℕ × ℕ
a✝ : p ∈ Finset.range (n + 1) ×ˢ Finset.range (k + 1)
this : (p.1 + volume.integrablePower, p.2) ∈ Finset.range (n + volume.integrablePower + 1) ×ˢ Finset.range (k + 1)
⊢ (SchwartzMap.seminorm 𝕜 (p.1 + volume.integrablePower) p.2) f ≤
    ((Finset.range (n + volume.integrablePower + 1) ×ˢ Finset.range (k + 1)).sup (schwartzSeminormFamily 𝕜 V E)) f
Module: Mathlib.Analysis.Distribution.TemperedDistribution

Goal state before:
pp: ι : Type u_1
𝕜 : Type u_2
E : Type u_3
F : Type u_4
F₁ : Type u_5
F₂ : Type u_6
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : AddCommGroup F
inst✝³ : Module ℂ F
inst✝² : TopologicalSpace F
inst✝¹ : IsTopologicalAddGroup F
inst✝ : ContinuousConstSMul ℂ F
x y : E
f : 𝓢'(E, F)
⊢ ∂_{x + y} f = ∂_{x} f + ∂_{y} f

Tactic:
ext u
    simp [lineDerivOp_left_add, add_comm]

Goal state after: