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
S : End 𝕜 X
hS_not_surj : ¬Function.Surjective ⇑S
hS_anti : Topology.IsClosedEmbedding ⇑S
c : 𝕜
hc : 1 < ‖c‖
R : ℝ
hR : ‖c‖ < R
V : ℕ → Submodule 𝕜 X := fun n ↦ (LinearMap.iterateRange S) n
hV_succ : ∀ (n : ℕ), V (n + 1) = Submodule.map S (V n)
hV_closed : ∀ (n : ℕ), IsClosed ↑(V n)
x : ∀ (n : ℕ), ∃ x ∈ V n, 1 ≤ ‖x‖ ∧ ‖x‖ ≤ R ∧ ∀ y ∈ V (n + 1), 1 ≤ ‖x - y‖
⊢ ∃ f,
    (∀ (n : ℕ), 1 ≤ ‖f n‖) ∧
      (∀ (n : ℕ), ‖f n‖ ≤ R) ∧
        (∀ (n : ℕ), f n ∈ LinearMap.range (S ^ n)) ∧ ∀ (n : ℕ), ∀ y ∈ LinearMap.range (S ^ (n + 1)), 1 ≤ ‖f n - y‖

Tactic:
choose x hxv hxn hxn' hxy using x

Goal state after:
𝕜 : Type u_1
X : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup X
inst✝ : NormedSpace 𝕜 X
S : End 𝕜 X
hS_not_surj : ¬Function.Surjective ⇑S
hS_anti : Topology.IsClosedEmbedding ⇑S
c : 𝕜
hc : 1 < ‖c‖
R : ℝ
hR : ‖c‖ < R
V : ℕ → Submodule 𝕜 X := fun n ↦ (LinearMap.iterateRange S) n
hV_succ : ∀ (n : ℕ), V (n + 1) = Submodule.map S (V n)
hV_closed : ∀ (n : ℕ), IsClosed ↑(V n)
x : ℕ → X
hxv : ∀ (n : ℕ), x n ∈ V n
hxn : ∀ (n : ℕ), 1 ≤ ‖x n‖
hxn' : ∀ (n : ℕ), ‖x n‖ ≤ R
hxy : ∀ (n : ℕ), ∀ y ∈ V (n + 1), 1 ≤ ‖x n - y‖
⊢ ∃ f,
    (∀ (n : ℕ), 1 ≤ ‖f n‖) ∧
      (∀ (n : ℕ), ‖f n‖ ≤ R) ∧
        (∀ (n : ℕ), f n ∈ LinearMap.range (S ^ n)) ∧ ∀ (n : ℕ), ∀ y ∈ LinearMap.range (S ^ (n + 1)), 1 ≤ ‖f n - y‖
Module: Mathlib.Analysis.Matrix.PosDef

Goal state before:
pp: n : Type u_2
𝕜 : Type u_3
inst✝² : Fintype n
inst✝¹ : RCLike 𝕜
A : Matrix n n 𝕜
inst✝ : DecidableEq n
hA : A.PosSemidef
⊢ 0 ≤ A.det

Tactic:
rw [hA.isHermitian.det_eq_prod_eigenvalues]
  exact Finset.prod_nonneg fun i _ ↦ by simpa using hA.eigenvalues_nonneg i

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝³ : RCLike 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
inst✝ : FiniteDimensional 𝕜 E
hT : T.IsSymmetric
v : E
μ : Eigenvalues T
w : PiLp 2 fun μ ↦ ↥(eigenspace T (↑T 1 μ))
hwT : ∀ (μ : Eigenvalues T), T ↑(w.ofLp μ) = ↑T 1 μ • ↑(w.ofLp μ)
⊢ T (hT.diagonalization.symm w) = hT.diagonalization.symm (toLp 2 fun μ ↦ ↑T 1 μ • w.ofLp μ)

Tactic:
simp only [diagonalization_symm_apply, map_sum, hwT, SetLike.val_smul]

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝³ : RCLike 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
inst✝ : FiniteDimensional 𝕜 E
n : ℕ
hT : T.IsSymmetric
hn : finrank 𝕜 E = n
i : Fin n
⊢ HasEigenvector T (↑((hT.unsortedEigenvalues hn ∘ ⇑(Tuple.sort (hT.unsortedEigenvalues hn)) ∘ ⇑Fin.revPerm) i))
    ((DirectSum.IsInternal.subordinateOrthonormalBasis hn ⋯ ⋯)
      ((Equiv.symm (Tuple.sort (hT.unsortedEigenvalues hn) * Fin.revPerm)).symm i))

Tactic:
apply hasEigenvector_eigenvectorBasis_helper

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝³ : RCLike 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
T : E →L[𝕜] E
hT : IsCompactOperator ⇑T
hT' : (↑T).IsSymmetric
⊢ (∀ (μ : 𝕜), HasEigenvalue (↑T) μ → μ = 0) ↔ ⨆ k ∈ spectrum 𝕜 T, ↑‖k‖₊ = 0

Tactic:
← not_iff_not,

Goal state after:
𝕜 : Type u_1
inst✝³ : RCLike 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
T : E →L[𝕜] E
hT : IsCompactOperator ⇑T
hT' : (↑T).IsSymmetric
⊢ (¬∀ (μ : 𝕜), HasEigenvalue (↑T) μ → μ = 0) ↔ ¬⨆ k ∈ spectrum 𝕜 T, ↑‖k‖₊ = 0
Module: Mathlib.Analysis.Matrix.Order

Goal state before:
pp: 𝕜 : Type u_1
inst✝ : RCLike 𝕜
ι : Type u_3
A B : Matrix ι ι 𝕜
hA : A.PosSemidef
hB : B.PosSemidef
x : ι →₀ 𝕜
hAs : (A.submatrix Subtype.val Subtype.val).PosSemidef
hBs : (B.submatrix Subtype.val Subtype.val).PosSemidef
y : ↥x.support → 𝕜
⊢ 0 ≤ star y ⬝ᵥ A.submatrix Subtype.val Subtype.val ⊙ B.submatrix Subtype.val Subtype.val *ᵥ y

Tactic:
star_dotProduct_hadamard_mulVec_eq_kronecker

Goal state after:
𝕜 : Type u_1
inst✝ : RCLike 𝕜
ι : Type u_3
A B : Matrix ι ι 𝕜
hA : A.PosSemidef
hB : B.PosSemidef
x : ι →₀ 𝕜
hAs : (A.submatrix Subtype.val Subtype.val).PosSemidef
hBs : (B.submatrix Subtype.val Subtype.val).PosSemidef
y : ↥x.support → 𝕜
⊢ 0 ≤
    star (diagonal y).vec ⬝ᵥ
      kroneckerMap (fun x1 x2 ↦ x1 * x2) (A.submatrix Subtype.val Subtype.val) (B.submatrix Subtype.val Subtype.val) *ᵥ
        (diagonal y).vec
Module: Mathlib.Analysis.Matrix.Order

Goal state before:
pp: 𝕜 : Type u_1
inst✝ : RCLike 𝕜
ι : Type u_3
A B : Matrix ι ι 𝕜
hA : A.PosDef
hB : B.PosDef
x : ι →₀ 𝕜
hx : x ≠ 0
hAs : (A.submatrix Subtype.val Subtype.val).PosDef
hBs : (B.submatrix Subtype.val Subtype.val).PosDef
y : ↥x.support → 𝕜
hy : y ≠ 0
⊢ 0 < star y ⬝ᵥ A.submatrix Subtype.val Subtype.val ⊙ B.submatrix Subtype.val Subtype.val *ᵥ y

Tactic:
star_dotProduct_hadamard_mulVec_eq_kronecker

Goal state after:
𝕜 : Type u_1
inst✝ : RCLike 𝕜
ι : Type u_3
A B : Matrix ι ι 𝕜
hA : A.PosDef
hB : B.PosDef
x : ι →₀ 𝕜
hx : x ≠ 0
hAs : (A.submatrix Subtype.val Subtype.val).PosDef
hBs : (B.submatrix Subtype.val Subtype.val).PosDef
y : ↥x.support → 𝕜
hy : y ≠ 0
⊢ 0 <
    star (diagonal y).vec ⬝ᵥ
      kroneckerMap (fun x1 x2 ↦ x1 * x2) (A.submatrix Subtype.val Subtype.val) (B.submatrix Subtype.val Subtype.val) *ᵥ
        (diagonal y).vec
Module: Mathlib.Analysis.InnerProductSpace.GramMatrix

Goal state before:
pp: E : Type u_1
n : Type u_2
𝕜 : Type u_4
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : DecidableEq n
v : n → E
⊢ gram 𝕜 v = 1 ↔ Orthonormal 𝕜 v

Tactic:
by
  simp [← Matrix.ext_iff, orthonormal_iff_ite, Matrix.one_apply]

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

Goal state before:
pp: α : Type u_1
E : Type u_2
𝕜 : Type u_4
inst✝² : RCLike 𝕜
m : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
f : ↥(Lp E 2 μ)
h_two : ENNReal.toReal 2 = 2
⊢ ∫⁻ (a : α), ↑‖↑↑f a‖₊ ^ 2 ∂μ ≠ ∞

Tactic:
refine (lintegral_rpow_enorm_lt_top_of_eLpNorm'_lt_top zero_lt_two (ε := E) ?_).ne
    rw [← h_two, ← eLpNorm_eq_eLpNorm' two_ne_zero ENNReal.ofNat_ne_top]
    finiteness

Goal state after:
Module: Mathlib.Geometry.Manifold.SmoothApprox

Goal state before:
pp: 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
⊢ ∃ g, (∀ (x : M), dist (g x) (f x) < ε x) ∧ support ⇑g ⊆ support f

Tactic:
obtain ⟨g, g_approx, -, g_supp⟩ := f_cont.exists_contMDiff_approx_and_eqOn I n ε_cont ε_pos
    isClosed_empty mem_nhdsSet_empty contMDiffOn_empty
  exact ⟨g, g_approx, g_supp⟩

Goal state after:
Module: Mathlib.Analysis.Normed.Lp.SmoothApprox

Goal state before:
pp: E : Type u_3
F : Type u_4
inst✝⁷ : MeasurableSpace E
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
inst✝² : BorelSpace E
inst✝¹ : NormedSpace ℝ F
μ : Measure E
inst✝ : IsFiniteMeasureOnCompacts μ
p : ℝ≥0∞
ε : ℝ
hε : 0 < ε
f : E → F
h₁ : HasCompactSupport f
h₂ : Continuous f
hp : p ≠ ∞
hf : ¬f =ᵐ[μ] 0
hs₁ : μ (tsupport f) ≠ ∞
⊢ 0 < (μ (tsupport f)).toReal

Tactic:
← Measure.measure_support_eq_zero_iff _

Goal state after:
E : Type u_3
F : Type u_4
inst✝⁷ : MeasurableSpace E
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
inst✝² : BorelSpace E
inst✝¹ : NormedSpace ℝ F
μ : Measure E
inst✝ : IsFiniteMeasureOnCompacts μ
p : ℝ≥0∞
ε : ℝ
hε : 0 < ε
f : E → F
h₁ : HasCompactSupport f
h₂ : Continuous f
hp : p ≠ ∞
hf : ¬μ (Function.support f) = 0
hs₁ : μ (tsupport f) ≠ ∞
⊢ 0 < (μ (tsupport f)).toReal
Module: Mathlib.Analysis.Distribution.ContDiffMapSupportedIn

Goal state before:
pp: case neg
𝕜 : 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₃
inst✝² : SMulCommClass ℝ 𝕜 F₁
inst✝¹ : NormedSpace ℝ F₃
inst✝ : SMulCommClass ℝ 𝕜 F₃
B : F₁ →L[𝕜] F₂ →L[𝕜] F₃
μ : Measure E
φ : E → F₂
f : 𝓓^{n}_{K}(E, F₁)
hφ : ¬IntegrableOn φ (↑K) μ
⊢ ‖(integralAgainstBilinLM B μ φ) f‖ ≤
    (∫ (x : E) in ↑K, ‖φ x‖ ∂μ) * ‖B‖ * (ContDiffMapSupportedIn.seminorm 𝕜 E F₁ n K 0) f

Tactic:
simp only [integralAgainstBilinLM, hφ, ↓reduceIte, LinearMap.coe_mk, AddHom.coe_mk, norm_zero]
    positivity

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
C : ℝ
hC : ∀ (A : Finset β), ‖GeneralSchauderBasis.proj b A‖ ≤ C
⊢ BddAbove (Set.range fun A ↦ ‖GeneralSchauderBasis.proj b A‖₊)

Tactic:
have hCpos : 0 ≤ C := by simpa [GeneralSchauderBasis.proj_empty] using hC ∅

Goal state after:
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
X : Type u_2
inst✝² : NormedAddCommGroup X
inst✝¹ : NormedSpace 𝕜 X
β : Type u_3
b : UnconditionalSchauderBasis β 𝕜 X
inst✝ : CompleteSpace X
C : ℝ
hC : ∀ (A : Finset β), ‖GeneralSchauderBasis.proj b A‖ ≤ C
hCpos : 0 ≤ C
⊢ BddAbove (Set.range fun A ↦ ‖GeneralSchauderBasis.proj b A‖₊)
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
b : SchauderBasis 𝕜 X
x : X
this : Tendsto (fun A ↦ (GeneralSchauderBasis.proj b A) x) (SummationFilter.conditional ℕ).filter (𝓝 x)
⊢ Tendsto (fun n ↦ (b.proj n) x) atTop (𝓝 x)

Tactic:
rwa [SummationFilter.conditional_filter_eq_map_range] at this

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

Goal state before:
pp: case succ
E : Type u_5
F : Type u_8
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : NormedSpace ℝ E
f : 𝓢(E, F)
n : ℕ
IH : ∀ (m : Fin n → E), tsupport ⇑(∂^{m} f) ⊆ tsupport ⇑f
m : Fin (n + 1) → E
⊢ tsupport ⇑(∂^{m} f) ⊆ tsupport ⇑f

Tactic:
rw [iteratedLineDerivOp_succ_left]
    exact (tsupport_lineDerivOp_subset (m 0) _).trans (IH <| Fin.tail m)

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
hdisj : U ⊓ V = ⊥
⊢ 0 < n + 1

Tactic:
exact Nat.succ_pos n

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
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
n : ℕ
x : X
⊢ ‖{ toFun := coeff n, map_add' := ⋯, map_smul' := ⋯ } x‖ ≤ ‖succSub D.P n‖ / ‖D.e n‖ * ‖x‖

Tactic:
rw [div_mul_eq_mul_div, le_div_iff₀ (norm_pos_iff.mpr (D.e_ne_zero n))]
        calc ‖coeff n x‖ * ‖D.e n‖ = ‖coeff n x • D.e n‖ := (norm_smul _ _).symm
          _ = ‖(succSub D.P n) x‖ := by rw [hcoeff]
          _ ≤ ‖succSub D.P n‖ * ‖x‖ := ContinuousLinearMap.le_opNorm _ _

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

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

Tactic:
fourierCoeffOn_eq_integral,

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

Goal state before:
pp: T : ℝ
hT : Fact (0 < T)
a : ℝ
f : ℝ → ℂ
n : ℤ
⊢ fourierCoeff (liftIoc T a f) n = fourierCoeffOn ⋯ f n

Tactic:
fourierCoeffOn_eq_integral,

Goal state after:
T : ℝ
hT : Fact (0 < T)
a : ℝ
f : ℝ → ℂ
n : ℤ
⊢ fourierCoeff (liftIoc T a f) n = (1 / (a + T - a)) • ∫ (x : ℝ) in a..a + T, (fourier (-n)) ↑x • f x
Module: Mathlib.Analysis.Fourier.AddCircle

Goal state before:
pp: T : ℝ
hT : Fact (0 < T)
a : ℝ
f : ℝ → ℂ
n : ℤ
⊢ fourierCoeff (liftIco T a f) n = fourierCoeffOn ⋯ f n

Tactic:
fourierCoeffOn_eq_integral,

Goal state after:
T : ℝ
hT : Fact (0 < T)
a : ℝ
f : ℝ → ℂ
n : ℤ
⊢ fourierCoeff (liftIco T a f) n = (1 / (a + T - a)) • ∫ (x : ℝ) in a..a + T, (fourier (-n)) ↑x • f x
Module: Mathlib.Analysis.Fourier.AddCircle

Goal state before:
pp: a b : ℝ
hab : a < b
f f' : ℝ → ℂ
n : ℤ
hn : n ≠ 0
hf : ContinuousOn f [[a, b]]
hff' : ∀ x ∈ Ioo (min a b) (max a b), HasDerivWithinAt f (f' x) (Ioi x) x
hf' : IntervalIntegrable f' volume a b
hT : Fact (0 < b - a)
⊢ fourierCoeffOn hab f n =
    1 / (-2 * ↑π * I * ↑n) * ((fourier (-n)) ↑a * (f b - f a) - ↑(b - a) * fourierCoeffOn hab f' n)

Tactic:
fourierCoeffOn_eq_integral,

Goal state after:
a b : ℝ
hab : a < b
f f' : ℝ → ℂ
n : ℤ
hn : n ≠ 0
hf : ContinuousOn f [[a, b]]
hff' : ∀ x ∈ Ioo (min a b) (max a b), HasDerivWithinAt f (f' x) (Ioi x) x
hf' : IntervalIntegrable f' volume a b
hT : Fact (0 < b - a)
⊢ (1 / (b - a)) • ∫ (x : ℝ) in a..b, (fourier (-n)) ↑x • f x =
    1 / (-2 * ↑π * I * ↑n) *
      ((fourier (-n)) ↑a * (f b - f a) - ↑(b - a) * (1 / (b - a)) • ∫ (x : ℝ) in a..b, (fourier (-n)) ↑x • f' x)
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✝¹⁰ : NormedField 𝕜
inst✝⁹ : NormedField 𝕜'
inst✝⁸ : NormedAddCommGroup D
inst✝⁷ : NormedSpace ℝ D
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : SMulCommClass ℝ 𝕜 E
inst✝⁴ : NormedAddCommGroup G
inst✝³ : NormedSpace ℝ G
inst✝² : NormedSpace 𝕜' G
inst✝¹ : SMulCommClass ℝ 𝕜' G
σ : 𝕜 →+* 𝕜'
inst✝ : RingHomIsometric σ
A : 𝓢(D, E) → F → G
hadd : ∀ (f g : 𝓢(D, E)) (x : F), A (f + g) x = A f x + A g x
hsmul : ∀ (a : 𝕜) (f : 𝓢(D, E)) (x : F), A (a • f) x = σ a • A f x
hsmooth : ∀ (f : 𝓢(D, E)), ContDiff ℝ ∞ (A f)
hbound :
  ∀ (n : ℕ × ℕ),
    ∃ s C,
      0 ≤ C ∧
        ∀ (f : 𝓢(D, E)) (x : F),
          ‖x‖ ^ n.1 * ‖iteratedFDeriv ℝ n.2 (A f) x‖ ≤ C * (s.sup (schwartzSeminormFamily 𝕜 D E)) f
⊢ Continuous (mkLM A hadd hsmul hsmooth hbound).toFun

Tactic:
change Continuous (mkLM A hadd hsmul hsmooth hbound : 𝓢(D, E) →ₛₗ[σ] 𝓢(F, G))

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✝¹⁰ : NormedField 𝕜
inst✝⁹ : NormedField 𝕜'
inst✝⁸ : NormedAddCommGroup D
inst✝⁷ : NormedSpace ℝ D
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : SMulCommClass ℝ 𝕜 E
inst✝⁴ : NormedAddCommGroup G
inst✝³ : NormedSpace ℝ G
inst✝² : NormedSpace 𝕜' G
inst✝¹ : SMulCommClass ℝ 𝕜' G
σ : 𝕜 →+* 𝕜'
inst✝ : RingHomIsometric σ
A : 𝓢(D, E) → F → G
hadd : ∀ (f g : 𝓢(D, E)) (x : F), A (f + g) x = A f x + A g x
hsmul : ∀ (a : 𝕜) (f : 𝓢(D, E)) (x : F), A (a • f) x = σ a • A f x
hsmooth : ∀ (f : 𝓢(D, E)), ContDiff ℝ ∞ (A f)
hbound :
  ∀ (n : ℕ × ℕ),
    ∃ s C,
      0 ≤ C ∧
        ∀ (f : 𝓢(D, E)) (x : F),
          ‖x‖ ^ n.1 * ‖iteratedFDeriv ℝ n.2 (A f) x‖ ≤ C * (s.sup (schwartzSeminormFamily 𝕜 D E)) f
⊢ Continuous ⇑(mkLM A hadd hsmul hsmooth hbound)
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
I₁ : ∀ (m : ℕ), ‖iteratedFDeriv ℝ m ⇑T fun x ↦ L v‖ ≤ ↑(n.descFactorial m) * 1 * (‖L‖ * ‖v‖) ^ (n - m)
I₂ :
  ∀ (m : ℕ),
    ‖iteratedFDeriv ℝ m (⇑T ∘ ⇑(ContinuousLinearMap.pi fun x ↦ L)) v‖ ≤
      ↑(n.descFactorial m) * 1 * (‖L‖ * ‖v‖) ^ (n - m) * ‖L‖ ^ m
I₃ :
  ∀ (m : ℕ),
    ‖iteratedFDeriv ℝ m (⇑T ∘ ⇑(ContinuousLinearMap.pi fun x ↦ L)) v‖ ≤ ↑(n.descFactorial m) * ‖L‖ ^ n * ‖v‖ ^ (n - m)
A : ContDiff ℝ K fun y ↦ T fun x ↦ L y
⊢ ∑ i ∈ Finset.range (k + 1), ↑(k.choose i) * ↑(n + 1) ^ k * ‖L‖ ^ n * C = (2 * ↑n + 2) ^ k * (‖L‖ ^ n * C)

Tactic:
simp only [← Finset.sum_mul, ← Nat.cast_sum, Nat.sum_range_choose, mul_one, ← mul_assoc,
      Nat.cast_pow, Nat.cast_ofNat, Nat.cast_add, Nat.cast_one, ← mul_pow, mul_add]

Goal state after:
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
A : ∀ (u : Set α), IsOpen[inst✝⁶] u → x₀ ∈ u → TendstoUniformlyOn φ 0 atTop (s \ u)
this : Tendsto (fun i ↦ ∫ (x : α) in s, φ i x • g x ∂μ) atTop (𝓝 (g x₀))
x✝ : ℕ
⊢ (∫ (x : α) in s, c x ^ x✝ ∂μ)⁻¹ • ∫ (x : α) in s, c x ^ x✝ • g x ∂μ = ∫ (x : α) in s, φ x✝ x • g x ∂μ

Tactic:
simp_rw [φ, ← smul_smul, integral_smul]

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

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

Tactic:
refine ⟨fun hf ↦ ?_, fun hf ↦ aux hf w⟩

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

Goal state before:
pp: α : Type u_1
E : Type u_2
F : Type u_3
inst✝⁷ : NormedAddCommGroup E
f : α → E
g : α → F
a : α
inst✝⁶ : TopologicalSpace α
inst✝⁵ : SecondCountableTopology α
inst✝⁴ : MeasurableSpace α
μ : Measure α
inst✝³ : NormedAddCommGroup F
inst✝² : LinearOrder α
inst✝¹ : CompactIccSpace α
inst✝ : atBot.IsMeasurablyGenerated
hf : LocallyIntegrableOn f (Iic a) μ
ho : f =O[atBot] g
hg : IntegrableAtFilter g atBot μ
⊢ IntegrableOn f (Iic a) μ

Tactic:
refine integrableOn_Iic_iff_integrableAtFilter_atBot.mpr ⟨ho.integrableAtFilter ?_ hg, hf⟩
  exact ⟨Iic a, Iic_mem_atBot a, hf.aestronglyMeasurable⟩

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

Goal state before:
pp: E : Type u_3
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℂ E
V : Type u_4
inst✝⁴ : AddCommGroup V
inst✝³ : Module ℝ V
inst✝² : MeasurableSpace V
W : Type u_5
inst✝¹ : AddCommGroup W
inst✝ : Module ℝ W
L : V →ₗ[ℝ] W →ₗ[ℝ] ℝ
μ : Measure V
f : V → E
w : W
⊢ VectorFourier.fourierIntegral 𝐞 μ L f w = ∫ (v : V), Complex.exp (↑(-2 * π * (L v) w) * Complex.I) • f v ∂μ

Tactic:
by
  simp_rw [VectorFourier.fourierIntegral, Circle.smul_def, Real.fourierChar_apply, mul_neg,
    neg_mul]

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

Goal state before:
pp: case inl
s : ℂ
h : IntegrableOn (fun x ↦ ↑x ^ s) (Ioi 0) volume
hs : s.re ≤ -1
this : IntegrableOn (fun x ↦ ↑x ^ s) (Ioo 0 1) volume
⊢ False

Tactic:
rw [integrableOn_Ioo_cpow_iff zero_lt_one] at this

Goal state after:
case inl
s : ℂ
h : IntegrableOn (fun x ↦ ↑x ^ s) (Ioi 0) volume
hs : s.re ≤ -1
this : -1 < s.re
⊢ False
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
⊢ ‖(-x) ^ s * rexp (-b * x ^ 2)‖ ≤ x ^ s * rexp (-b * x ^ 2)

Tactic:
have h'x : 0 ≤ x := le_of_lt hx

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: ⊢ Gamma 1 = 1

Tactic:
by rw [Gamma_eq_integral] <;> simp

Goal state after:
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
A : Tendsto (fun c ↦ ∫ (w : V), cexp (-↑c⁻¹ * ↑‖w‖ ^ 2 + 2 * ↑π * I * ↑⟪v, w⟫) • 𝓕 f w) atTop (𝓝 (𝓕⁻ (𝓕 f) v))
c : ℝ
hc : 0 < c
J : Integrable (fun w ↦ cexp (-↑c⁻¹ * ↑‖w‖ ^ 2 + 2 * ↑π * I * ↑⟪v, w⟫)) volume
⊢ ∫ (w : V), cexp (-↑c⁻¹ * ↑‖w‖ ^ 2 + 2 * ↑π * I * ↑⟪v, w⟫) • 𝓕 f w =
    ∫ (w : V), 𝓕 (fun w ↦ cexp (-↑c⁻¹ * ↑‖w‖ ^ 2 + 2 * ↑π * I * ↑⟪v, w⟫)) w • f w

Tactic:
simpa using! (VectorFourier.integral_fourierIntegral_smul_eq_flip (L := innerₗ V)
      Real.continuous_fourierChar continuous_inner J hf).symm

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

Goal state before:
pp: s : ℝ
hs : s ≠ 0
⊢ (↑s * Complex.Gamma ↑s).re = s * (Complex.Gamma ↑s).re

pp: case h2
s : ℝ
hs : s ≠ 0
⊢ ↑s ≠ 0

Tactic:
Complex.re_ofReal_mul

Goal state after:
s : ℝ
hs : s ≠ 0
⊢ s * (Complex.Gamma ↑s).re = s * (Complex.Gamma ↑s).re

case h2
s : ℝ
hs : s ≠ 0
⊢ ↑s ≠ 0