mathlib-initiative/mathlib-tactics huggingface dataset:
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.Surjective ⇑S
c : 𝕜
hc : 1 < ‖c‖
f : ℕ → X
hf_norm_lower : ∀ (n : ℕ), 1 ≤ ‖f n‖
hf_norm_upper : ∀ (n : ℕ), ‖f n‖ ≤ ‖c‖ + 1
hf_far : ∀ (n : ℕ), ∀ y ∈ LinearMap.range (↑S ^ (n + 1)), 1 ≤ ‖f n - y‖
hf_mem : ∀ {n m : ℕ}, m ≤ n → f n ∈ (↑S ^ m).range
hf_mem' : ∀ {n m : ℕ}, m ≤ n → S (f n) ∈ (↑S ^ (m + 1)).range
hp : Pairwise fun x₁ x₂ ↦ ‖μ‖ ≤ ‖T (f x₁) - T (f x₂)‖
K : Set X
hK : IsCompact K
hK' : ⇑↑T '' Metric.closedBall 0 (‖c‖ + 1) ⊆ K
y : X
hyK : y ∈ K
ψ : ℕ → ℕ
hψ : StrictMono ψ
hψy : ∀ ε > 0, ∃ N, ∀ n ≥ N, dist (((fun n ↦ ↑T (f n)) ∘ ψ) n) (((fun n ↦ ↑T (f n)) ∘ ψ) N) < ε
N : ℕ
hN : ∀ n ≥ N, dist (((fun n ↦ ↑T (f n)) ∘ ψ) n) (((fun n ↦ ↑T (f n)) ∘ ψ) N) < ‖μ‖
this : ‖T (f (ψ (N + 1))) - T (f (ψ N))‖ < ‖μ‖
⊢ False

Tactic:
refine this.not_ge (hp ?_)

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
c : 𝕜
hc : 1 < ‖c‖
f : ℕ → X
hf_norm_lower : ∀ (n : ℕ), 1 ≤ ‖f n‖
hf_norm_upper : ∀ (n : ℕ), ‖f n‖ ≤ ‖c‖ + 1
hf_far : ∀ (n : ℕ), ∀ y ∈ LinearMap.range (↑S ^ (n + 1)), 1 ≤ ‖f n - y‖
hf_mem : ∀ {n m : ℕ}, m ≤ n → f n ∈ (↑S ^ m).range
hf_mem' : ∀ {n m : ℕ}, m ≤ n → S (f n) ∈ (↑S ^ (m + 1)).range
hp : Pairwise fun x₁ x₂ ↦ ‖μ‖ ≤ ‖T (f x₁) - T (f x₂)‖
K : Set X
hK : IsCompact K
hK' : ⇑↑T '' Metric.closedBall 0 (‖c‖ + 1) ⊆ K
y : X
hyK : y ∈ K
ψ : ℕ → ℕ
hψ : StrictMono ψ
hψy : ∀ ε > 0, ∃ N, ∀ n ≥ N, dist (((fun n ↦ ↑T (f n)) ∘ ψ) n) (((fun n ↦ ↑T (f n)) ∘ ψ) N) < ε
N : ℕ
hN : ∀ n ≥ N, dist (((fun n ↦ ↑T (f n)) ∘ ψ) n) (((fun n ↦ ↑T (f n)) ∘ ψ) N) < ‖μ‖
this : ‖T (f (ψ (N + 1))) - T (f (ψ N))‖ < ‖μ‖
⊢ ψ (N + 1) ≠ ψ N
Module: Mathlib.Analysis.Distribution.ContDiffMapSupportedIn

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : SMulCommClass ℝ 𝕜 F
n k : ℕ∞
K : Compacts E
i : ℕ
f : 𝓓^{n}_{K}(E, F)
hin : k + ↑i ≤ n
⊢ ⇑((iteratedFDerivLM 𝕜 n k i) f) = iteratedFDeriv ℝ i ⇑f

Tactic:
simp [hin]

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
s t : Set α
hs : MeasurableSet s
ht : MeasurableSet t
hμs : μ s ≠ ∞
hμt : μ t ≠ ∞
⊢ ⟪indicatorConstLp 2 hs hμs 1, indicatorConstLp 2 ht hμt 1⟫_ℝ = μ.real (s ∩ t)

Tactic:
simp [inner_indicatorConstLp_indicatorConstLp]

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

Goal state before:
pp: case neg
ι : 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 ι
i : ι
x : G i
j : ι
h : ¬j = i
⊢ (V j) (Pi.single i x j) = 0

Tactic:
simp [h]

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

Goal state before:
pp: case pos
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
X : Type u_2
inst✝¹ : NormedAddCommGroup X
inst✝ : NormedSpace 𝕜 X
β : Type u_3
L : SummationFilter β
b : SchauderBasis 𝕜 X
D : RankOneDecomposition 𝕜 X
coeff : ℕ → X → 𝕜 := D.basisCoeff
hcoeff : ∀ (n : ℕ) (x : X), (succSub D.P n) x = coeff n x • D.e n
i j : ℕ
x : X
hx : (succSub D.P j) x = D.e j
h : i = j
⊢ D.e j = 1 • D.e i

Tactic:
simp [h]

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

Goal state before:
pp: case neg
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
X : Type u_2
inst✝¹ : NormedAddCommGroup X
inst✝ : NormedSpace 𝕜 X
β : Type u_3
L : SummationFilter β
b : SchauderBasis 𝕜 X
D : RankOneDecomposition 𝕜 X
coeff : ℕ → X → 𝕜 := D.basisCoeff
hcoeff : ∀ (n : ℕ) (x : X), (succSub D.P n) x = coeff n x • D.e n
i j : ℕ
x : X
hx : (succSub D.P j) x = D.e j
h : ¬i = j
⊢ 0 = 0 • D.e i

Tactic:
simp [h]

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

Goal state before:
pp: case refine_1
T : ℝ
x : C(AddCircle T, ℂ)
hx : x ∈ ↑(Submonoid.closure (range fourier))
⊢ fourier 0 = 1

Tactic:
ext1 z

Goal state after:
case refine_1
T : ℝ
x : C(AddCircle T, ℂ)
hx : x ∈ ↑(Submonoid.closure (range fourier))
z : AddCircle T
⊢ (fourier 0) z = 1 z
Module: Mathlib.Analysis.Fourier.AddCircle

Goal state before:
pp: case refine_2
T : ℝ
x : C(AddCircle T, ℂ)
hx : x ∈ ↑(Submonoid.closure (range fourier))
m n : ℤ
⊢ fourier (m + n) = fourier m * fourier n

Tactic:
ext1 z

Goal state after:
case refine_2
T : ℝ
x : C(AddCircle T, ℂ)
hx : x ∈ ↑(Submonoid.closure (range fourier))
m n : ℤ
z : AddCircle T
⊢ (fourier (m + n)) z = (fourier m * fourier n) z
Module: Mathlib.Analysis.Fourier.AddCircle

Goal state before:
pp: T : ℝ
hT : Fact (0 < T)
⊢ (span ℂ (range fourier)).topologicalClosure = ⊤

Tactic:
by
  rw [← fourierSubalgebra_coe]
  exact congr_arg (Subalgebra.toSubmodule <| StarSubalgebra.toSubalgebra ·)
    fourierSubalgebra_closure_eq_top

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

Goal state before:
pp: case pos
T : ℝ
hT : Fact (0 < T)
i j : ℤ
h : i = j
⊢ ∫ (x : AddCircle T), (fourier (j + -i)) x ∂haarAddCircle = 1

Tactic:
simp [h]

Goal state after:
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 := 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
⊢ ∫ (x : α) in s, φ i x • g x - t.indicator (fun a_1 ↦ φ i a_1 • a) x ∂μ + (∫ (x : α) in t, φ i x ∂μ) • a =
    ∫ (x : α) in s, φ i x • g x ∂μ

Tactic:
integral_sub hi,

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
⊢ ∫ (a : α) in s, φ i a • g a ∂μ - ∫ (a_1 : α) in s, t.indicator (fun a_2 ↦ φ i a_2 • a) a_1 ∂μ +
      (∫ (x : α) in t, φ i x ∂μ) • a =
    ∫ (x : α) in s, φ i x • g x ∂μ

α : 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 (t.indicator fun a_1 ↦ φ i a_1 • a) (μ.restrict s)
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
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[ℝ] ℝ :=
  (ContinuousMultilinearMap.mkPiAlgebra ℝ (Fin n) ℝ).compContinuousLinearMapLRight
m : ℕ
this : ‖T‖ ≤ 1
⊢ ‖iteratedFDeriv ℝ m ⇑T fun x ↦ L v‖ ≤ ↑(n.descFactorial m) * 1 * (‖L‖ * ‖v‖) ^ (n - m)

Tactic:
apply (ContinuousMultilinearMap.norm_iteratedFDeriv_le _ _ _).trans

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
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[ℝ] ℝ := ⋯
m : ℕ
this : ‖T‖ ≤ 1
⊢ ↑((Fintype.card (Fin n)).descFactorial m) * ‖T‖ * ‖fun x ↦ L v‖ ^ (Fintype.card (Fin n) - m) ≤
    ↑(n.descFactorial m) * 1 * (‖L‖ * ‖v‖) ^ (n - m)
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✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NormedAlgebra ℝ 𝕜
inst✝⁶ : NormedAddCommGroup D
inst✝⁵ : NormedSpace ℝ D
inst✝⁴ : NormedAddCommGroup G
inst✝³ : NormedSpace ℝ G
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedSpace 𝕜 E
inst✝ : NormedSpace 𝕜 G
B : E →L[𝕜] F →L[𝕜] G
g : D → F
hg : Function.HasTemperateGrowth g
k n l : ℕ
C : ℝ
hC : 0 ≤ C
f : 𝓢(D, E)
x : D
hxk : 0 ≤ ‖x‖ ^ k
hnorm_mul :
  ‖iteratedFDeriv ℝ n (fun y ↦ ((ContinuousLinearMap.bilinearRestrictScalars ℝ B) (f y)) (g y)) x‖ ≤
    ‖ContinuousLinearMap.bilinearRestrictScalars ℝ B‖ *
      ∑ i ∈ Finset.range (n + 1), ↑(n.choose i) * ‖iteratedFDeriv ℝ i (⇑f) x‖ * ‖iteratedFDeriv ℝ (n - i) g x‖
this : ∑ _x ∈ Finset.range (n + 1), 1 = ↑n + 1
i : ℕ
hgrowth : ‖iteratedFDeriv ℝ (n - i) g x‖ ≤ C * (1 + ‖x‖) ^ l
hi : i ∈ Finset.range (n + 1)
⊢ ‖x‖ ^ k * ‖iteratedFDeriv ℝ i (⇑f) x‖ * (1 + ‖x‖) ^ l * C ≤
    2 ^ (l + k) * ((Finset.Iic (l + k, n)).sup (schwartzSeminormFamily 𝕜 D E)) f * C

Tactic:
gcongr ?_ * C

Goal state after:
case hbc
ι : Type u_1
𝕜 : Type u_2
𝕜' : Type u_3
D : Type u_4
E : Type u_5
F : Type u_6
G : Type u_7
H : Type u_8
V : Type u_9
inst✝¹² : NormedAddCommGroup E
inst✝¹¹ : NormedSpace ℝ E
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NormedSpace ℝ F
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NormedAlgebra ℝ 𝕜
inst✝⁶ : NormedAddCommGroup D
inst✝⁵ : NormedSpace ℝ D
inst✝⁴ : NormedAddCommGroup G
inst✝³ : NormedSpace ℝ G
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedSpace 𝕜 E
inst✝ : NormedSpace 𝕜 G
B : E →L[𝕜] F →L[𝕜] G
g : D → F
hg : Function.HasTemperateGrowth g
k n l : ℕ
C : ℝ
hC : 0 ≤ C
f : 𝓢(D, E)
x : D
hxk : 0 ≤ ‖x‖ ^ k
hnorm_mul :
  ‖iteratedFDeriv ℝ n (fun y ↦ ((ContinuousLinearMap.bilinearRestrictScalars ℝ B) (f y)) (g y)) x‖ ≤
    ‖ContinuousLinearMap.bilinearRestrictScalars ℝ B‖ *
      ∑ i ∈ Finset.range (n + 1), ↑(n.choose i) * ‖iteratedFDeriv ℝ i (⇑f) x‖ * ‖iteratedFDeriv ℝ (n - i) g x‖
this : ∑ _x ∈ Finset.range (n + 1), 1 = ↑n + 1
i : ℕ
hgrowth : ‖iteratedFDeriv ℝ (n - i) g x‖ ≤ C * (1 + ‖x‖) ^ l
hi : i ∈ Finset.range (n + 1)
⊢ ‖x‖ ^ k * ‖iteratedFDeriv ℝ i (⇑f) x‖ * (1 + ‖x‖) ^ l ≤
    2 ^ (l + k) * ((Finset.Iic (l + k, n)).sup (schwartzSeminormFamily 𝕜 D E)) f
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✝⁴ : MeasurableSpace E
inst✝³ : OpensMeasurableSpace E
inst✝² : NormedField 𝕜
inst✝¹ : NormedSpace 𝕜 F
inst✝ : SMulCommClass ℝ 𝕜 F
p : ℝ≥0∞
μ : Measure E
hμ : μ.HasTemperateGrowth
k : ℕ
hk : eLpNorm (fun x ↦ (1 + ‖x‖) ^ (-↑k)) p μ < ∞
f : 𝓢(E, F)
h_one_add : ∀ (x : E), 0 < 1 + ‖x‖
⊢ eLpNorm (fun x ↦ (1 + ‖x‖) ^ (-↑k)) p μ * eLpNorm (fun x ↦ (1 + ‖x‖) ^ k • f x) ∞ μ ≤
    eLpNorm (fun x ↦ (1 + ‖x‖) ^ (-↑k)) p μ *
      (2 ^ k * ENNReal.ofReal (((Finset.Iic (k, 0)).sup (schwartzSeminormFamily 𝕜 E F)) f))

Tactic:
gcongr
    refine eLpNormEssSup_le_of_ae_nnnorm_bound (ae_of_all μ fun x ↦ ?_)
    rw [← norm_toNNReal, Real.toNNReal_le_iff_le_coe]
    simpa [norm_smul, abs_of_nonneg (h_one_add x).le] using!
      one_add_le_sup_seminorm_apply (m := (k, 0)) (le_refl k) (le_refl 0) f x

Goal state after:
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)
If : Integrable f μ
this : Tendsto (fun c ↦ ∫ (x : F), (c ^ finrank ℝ F * φ (c • x)) • g (x₀ - x) ∂μ) atTop (𝓝 (g x₀))
⊢ Tendsto (fun c ↦ ∫ (x : F), (c ^ finrank ℝ F * φ (c • (x₀ - x))) • g x ∂μ) atTop (𝓝 (g x₀))

Tactic:
convert! this using 2 with c

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 μ
this : Tendsto (fun c ↦ ∫ (x : F), (c ^ finrank ℝ F * φ (c • x)) • g (x₀ - x) ∂μ) atTop (𝓝 (g x₀))
c : ℝ
⊢ ∫ (x : F), (c ^ finrank ℝ F * φ (c • (x₀ - x))) • g x ∂μ = ∫ (x : F), (c ^ finrank ℝ F * φ (c • x)) • g (x₀ - x) ∂μ
Module: Mathlib.Analysis.Distribution.SchwartzSpace.Basic

Goal state before:
pp: E : Type u_5
F : Type u_6
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : MeasurableSpace E
inst✝² : OpensMeasurableSpace E
inst✝¹ : SecondCountableTopologyEither E F
p : ℝ≥0∞
μ : Measure E
hμ : μ.HasTemperateGrowth
inst✝ : μ.IsOpenPosMeasure
f g : 𝓢(E, F)
⊢ (fun f ↦ f.toLp p μ) f = (fun f ↦ f.toLp p μ) g → f = g

Tactic:
simpa [toLp] using (Continuous.ae_eq_iff_eq μ f.continuous g.continuous).mp

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.ImproperIntegrals

Goal state before:
pp: a : ℝ
ha : a < 0
c : ℝ
⊢ (↑a).re < 0

Tactic:
by simpa using ha

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

Goal state before:
pp: case refine_1
s x : ℝ
hx : rexp (-(1 / 2) * x) = 0
⊢ False

Tactic:
exact (exp_pos (-(1 / 2) * x)).ne' hx

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

Goal state before:
pp: b : ℂ
hb : 0 < b.re
⊢ -π ≤ π

Tactic:
by linarith [pi_nonneg]

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

Goal state before:
pp: b : ℂ
hb : 0 < b.re
⊢ ∫ (x : ℝ), cexp (-b * ↑x ^ 2) = (↑π / b) ^ (1 / 2)

Tactic:
by
  have nv : ∀ {b : ℂ}, 0 < re b → b ≠ 0 := by intro b hb; contrapose! hb; rw [hb]; simp
  apply
    (convex_halfSpace_re_gt 0).isPreconnected.eq_of_sq_eq ?_ ?_ (fun c hc => ?_) (fun {c} hc => ?_)
      (by simp : 0 < re (1 : ℂ)) ?_ hb
  · -- integral is continuous
    exact continuousOn_of_forall_continuousAt continuousAt_gaussian_integral
  · -- `(π / b) ^ (1 / 2 : ℂ)` is continuous
    refine
      continuousOn_of_forall_continuousAt fun b hb =>
        (continuousAt_cpow_const (Or.inl ?_)).comp (continuousAt_const.div continuousAt_id (nv hb))
    rw [div_re, ofReal_im, ofReal_re, zero_mul, zero_div, add_zero]
    exact div_pos (mul_pos pi_pos hb) (normSq_pos.mpr (nv hb))
  · -- equality at 1
    have : ∀ x : ℝ, cexp (-(1 : ℂ) * (x : ℂ) ^ 2) = exp (-(1 : ℝ) * x ^ 2) := by
      intro x
      simp only [ofReal_exp, neg_mul, one_mul, ofReal_neg, ofReal_pow]
    simp_rw [this, ← coe_algebraMap, RCLike.algebraMap_eq_ofReal, integral_ofReal,
      ← RCLike.algebraMap_eq_ofReal, coe_algebraMap]
    conv_rhs =>
      congr
      · rw [← ofReal_one, ← ofReal_div]
      · rw [← ofReal_one, ← ofReal_ofNat, ← ofReal_div]
    rw [← ofReal_cpow, ofReal_inj]
    · convert! integral_gaussian (1 : ℝ) using 1
      rw [sqrt_eq_rpow]
    · rw [div_one]; exact pi_pos.le
  · -- squares of both sides agree
    dsimp only [Pi.pow_apply]
    rw [integral_gaussian_sq_complex hc, sq]
    conv_lhs => rw [← cpow_one (↑π / c)]
    rw [← cpow_add _ _ (div_ne_zero (ofReal_ne_zero.mpr pi_ne_zero) (nv hc))]
    norm_num
  · -- 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.SpecialFunctions.Gamma.Basic

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

Tactic:
← Gamma_ofReal,

Goal state after:
a r : ℝ
ha : 0 < a
hr : 0 < r
⊢ ↑(∫ (t : ℝ) in Ioi 0, t ^ (a - 1) * rexp (-(r * t))) = ↑((1 / r) ^ a) * Complex.Gamma ↑a
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic

Goal state before:
pp: case a
s : ℝ
hs : ∀ (m : ℕ), s ≠ -↑m
this : ∀ {n : ℕ}, -↑n < s → Gamma s ≠ 0
⊢ -↑?n < s

pp: case n
s : ℝ
hs : ∀ (m : ℕ), s ≠ -↑m
this : ∀ {n : ℕ}, -↑n < s → Gamma s ≠ 0
⊢ ℕ

Tactic:
swap

Goal state after:
case n
s : ℝ
hs : ∀ (m : ℕ), s ≠ -↑m
this : ∀ {n : ℕ}, -↑n < s → Gamma s ≠ 0
⊢ ℕ

case a
s : ℝ
hs : ∀ (m : ℕ), s ≠ -↑m
this : ∀ {n : ℕ}, -↑n < s → Gamma s ≠ 0
⊢ -↑?n < s
Module: Mathlib.Analysis.Distribution.Sobolev

Goal state before:
pp: E : Type u_1
F : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : InnerProductSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
inst✝ : NormedSpace ℂ F
s s' : ℝ
f : 𝓢'(E, F)
⊢ (besselPotential E F s') ((besselPotential E F s) f) = (besselPotential E F (s + s')) f

Tactic:
by
  simp only [besselPotential]
  rw [fourierMultiplierCLM_fourierMultiplierCLM_apply (by fun_prop) (by fun_prop)]
  congr
  ext x
  simp only [Pi.mul_apply]
  norm_cast
  calc
    _ = (1 + ‖x‖ ^ 2) ^ (s / 2 + s' / 2) := by
      rw [← Real.rpow_add (by positivity)]
    _ = _ := by congr; ring

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

Goal state before:
pp: d : Type u_1
inst✝ : Fintype d
⊢ Orthonormal ℂ (mFourierLp 2)

Tactic:
rw [orthonormal_iff_ite]
  intro m n
  simp only [ContinuousMap.inner_toLp, ← mFourier_neg, ← mFourier_add]
  split_ifs with h
  · simpa only [h, add_neg_cancel, mFourier_zero, probReal_univ, one_smul] using!
      integral_const (α := UnitAddTorus d) (μ := volume) (1 : ℂ)
  rw [mFourier, ContinuousMap.coe_mk, MeasureTheory.integral_fintype_prod_volume_eq_prod]
  obtain ⟨i, hi⟩ := Function.ne_iff.mp h
  apply Finset.prod_eq_zero (Finset.mem_univ i)
  simpa only [eq_false_intro hi, if_false, ContinuousMap.inner_toLp, ← fourier_neg,
    ← fourier_add] using! (orthonormal_iff_ite.mp <| orthonormal_fourier) (m i) (n i)

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

Goal state before:
pp: 𝕜 : Type u_1
R : Type u_2
E : Type u_3
F : Type u_4
F₁ : Type u_5
F₂ : Type u_6
F₃ : Type u_7
inst✝¹⁷ : RCLike 𝕜
inst✝¹⁶ : NormedAddCommGroup E
inst✝¹⁵ : InnerProductSpace ℝ E
inst✝¹⁴ : FiniteDimensional ℝ E
inst✝¹³ : MeasurableSpace E
inst✝¹² : BorelSpace 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₂
inst✝³ : NormedAddCommGroup F₃
inst✝² : NormedSpace ℂ F₃
inst✝¹ : NormedSpace 𝕜 F₃
inst✝ : SMulCommClass ℂ 𝕜 F₃
B : F₁ →L[𝕜] F₂ →L[𝕜] F₃
⊢ ∀ (m : 𝕜) (x : 𝓢(E, F₁)),
    fourierInvCLM 𝕜 𝓢(E, F₃) ∘SL (pairing B) (𝓕 (m • x)) ∘SL fourierCLM 𝕜 𝓢(E, F₂) =
      (RingHom.id 𝕜) m • fourierInvCLM 𝕜 𝓢(E, F₃) ∘SL (pairing B) (𝓕 x) ∘SL fourierCLM 𝕜 𝓢(E, F₂)

Tactic:
simp [FourierTransform.fourier_smul]

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

Goal state before:
pp: E : Type u_1
F : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : InnerProductSpace ℝ E
inst✝⁴ : FiniteDimensional ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : InnerProductSpace ℂ F
inst✝ : CompleteSpace F
s s' : ℝ
h : s' ≤ s
f : 𝓢'(E, F)
hf : MemSobolev s 2 f
⊢ s' - s ≤ 0 * 2

Tactic:
simp [h]

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

Goal state before:
pp: case mp
n : ℕ
h : ¬Squarefree n
⊢ μ n = 0

Tactic:
simp [h]

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

Goal state before:
pp: case mpr
n : ℕ
h : Squarefree n
⊢ μ n ≠ 0

Tactic:
simp [h]

Goal state after: