mathlib-initiative/mathlib-tactics huggingface dataset:
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
⊢ Antitone (hT.eigenvalues hn)

Tactic:
rw [eigenvalues_def, ← Function.comp_assoc]

Goal state after:
𝕜 : 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
⊢ Antitone ((hT.unsortedEigenvalues hn ∘ ⇑(Tuple.sort (hT.unsortedEigenvalues hn))) ∘ ⇑Fin.revPerm)
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
f : 𝓓^{n}_{K}(E, F)
hk : n < k + 1
⊢ (fderivLM 𝕜 n k) f = 0

Tactic:
ext : 1

Goal state after:
𝕜 : 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
f : 𝓓^{n}_{K}(E, F)
hk : n < k + 1
a✝ : E
⊢ ((fderivLM 𝕜 n k) f) a✝ = 0 a✝
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 : n < k + ↑i
⊢ (iteratedFDerivLM 𝕜 n k i) f = 0

Tactic:
ext : 1

Goal state after:
𝕜 : 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 : n < k + ↑i
a✝ : E
⊢ ((iteratedFDerivLM 𝕜 n k i) f) a✝ = 0 a✝
Module: Mathlib.Analysis.Distribution.ContDiffMapSupportedIn

Goal state before:
pp: 𝕜 : 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
x✝ : Fin 1
f : 𝓓^{n}_{K}(E, F)
⊢ (((fun x ↦ normSeminorm 𝕜 (E →ᵇ F)) x✝).comp (toBoundedContinuousFunctionLM 𝕜)) f ≤
    (1 • {0}.sup (ContDiffMapSupportedIn.seminorm 𝕜 E F n K)) f

Tactic:
simp [norm_toBoundedContinuousFunction 𝕜 f]

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

Goal state before:
pp: case e_f
α : 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 μ)
x : α
h_two : 2 = ↑2
⊢ ENNReal.ofReal ‖↑↑f x‖ ^ 2 = ↑(‖↑↑f x‖₊ ^ 2)

Tactic:
ofReal_norm

Goal state after:
case e_f
α : 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 μ)
x : α
h_two : 2 = ↑2
⊢ ‖↑↑f x‖ₑ ^ 2 = ↑(‖↑↑f x‖₊ ^ 2)
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 g : ↥(Lp E 2 μ)
⊢ eLpNorm (fun x ↦ ⟪↑↑f x, ↑↑g x⟫) 1 μ < ∞

Tactic:
exact eLpNorm_inner_lt_top f g

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

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
V : Type u_7
F : Type u_8
F₁ : Type u_9
F₂ : Type u_10
F₃ : Type u_11
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : NormedSpace ℝ E
inst✝² : RCLike 𝕜
inst✝¹ : NormedSpace 𝕜 F
inst✝ : SMulCommClass ℝ 𝕜 F
v w : E
f : 𝓢(E, F)
⊢ ∂_{v + w} f = ∂_{v} f + ∂_{w} f

Tactic:
by
    ext x
    simp [lineDerivOp_apply_eq_fderiv]

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

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
V : Type u_7
F : Type u_8
F₁ : Type u_9
F₂ : Type u_10
F₃ : Type u_11
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : NormedSpace ℝ E
inst✝² : RCLike 𝕜
inst✝¹ : NormedSpace 𝕜 F
inst✝ : SMulCommClass ℝ 𝕜 F
r : ℝ
y : E
f : 𝓢(E, F)
⊢ ∂_{r • y} f = r • ∂_{y} f

Tactic:
by
    ext x
    simp [lineDerivOp_apply_eq_fderiv]

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

Goal state before:
pp: T : ℝ
n : ℤ
x : ℝ
⊢ ↑(Circle.exp (2 * π / T * n • x)) = Complex.exp (2 * ↑π * Complex.I * ↑n * ↑x / ↑T)

Tactic:
Circle.coe_exp,

Goal state after:
T : ℝ
n : ℤ
x : ℝ
⊢ Complex.exp (↑(2 * π / T * n • x) * Complex.I) = Complex.exp (2 * ↑π * Complex.I * ↑n * ↑x / ↑T)
Module: Mathlib.Analysis.Fourier.AddCircle

Goal state before:
pp: T : ℝ
hT : Fact (0 < T)
f : ↥(Lp ℂ 2 haarAddCircle)
⊢ HasSum (fun i ↦ ‖fourierCoeff (↑↑f) i‖ ^ 2) (∫ (t : AddCircle T), ‖↑↑f t‖ ^ 2 ∂haarAddCircle)

Tactic:
simp_rw [← fourierBasis_repr]
  have H₁ : HasSum (fun i => ‖fourierBasis.repr f i‖ ^ 2) (‖fourierBasis.repr f‖ ^ 2) := by
    apply_mod_cast lp.hasSum_norm ?_ (fourierBasis.repr f)
    simp
  have H₂ : ‖fourierBasis.repr f‖ ^ 2 = ‖f‖ ^ 2 := by simp
  have H₃ := congr_arg RCLike.re (@L2.inner_def (AddCircle T) ℂ ℂ _ _ _ _ _ f f)
  rw [← integral_re] at H₃
  · simp only [← norm_sq_eq_re_inner] at H₃
    rwa [H₂, H₃] at H₁
  · exact L2.integrable_inner f f

Goal state after:
Module: Mathlib.MeasureTheory.Integral.PeakFunction

Goal state before:
pp: case inl
α : 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
h : s \ u = ∅
⊢ ∃ t, 0 ≤ t ∧ t < c x₀ ∧ ∀ x ∈ s \ u, c x ≤ t

pp: case inr
α : 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
h : (s \ u).Nonempty
⊢ ∃ t, 0 ≤ t ∧ t < c x₀ ∧ ∀ x ∈ s \ u, c x ≤ t

Tactic:
· exact
          ⟨0, le_rfl, hnc₀, by simp only [h, mem_empty_iff_false, IsEmpty.forall_iff, imp_true_iff]⟩

Goal state after:
case inr
α : 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
h : (s \ u).Nonempty
⊢ ∃ t, 0 ≤ t ∧ t < c x₀ ∧ ∀ x ∈ s \ u, c x ≤ t
Module: Mathlib.MeasureTheory.Integral.PeakFunction

Goal state before:
pp: case hnφ
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 φ μ
⊢ ∀ᶠ (i : ℝ) in atTop, ∀ (x : F), 0 ≤ i ^ finrank ℝ F * φ (i • x)

Tactic:
filter_upwards [Ici_mem_atTop 0] with c (hc : 0 ≤ c) x using mul_nonneg (by positivity) (hφ _)

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
F : Type u_5
G : Type u_6
inst✝¹⁷ : NormedAddCommGroup E
inst✝¹⁶ : NormedSpace ℂ E
inst✝¹⁵ : NormedAddCommGroup F
inst✝¹⁴ : NormedSpace ℂ F
inst✝¹³ : NormedAddCommGroup G
inst✝¹² : NormedSpace ℂ G
inst✝¹¹ : TopologicalSpace 𝕜
inst✝¹⁰ : IsTopologicalRing 𝕜
inst✝⁹ : TopologicalSpace V
inst✝⁸ : BorelSpace V
inst✝⁷ : TopologicalSpace W
inst✝⁶ : MeasurableSpace W
inst✝⁵ : BorelSpace W
e : AddChar 𝕜 𝕊
μ : Measure V
L : V →ₗ[𝕜] W →ₗ[𝕜] 𝕜
ν : Measure W
inst✝⁴ : SigmaFinite μ
inst✝³ : SigmaFinite ν
inst✝² : SecondCountableTopologyEither W V
inst✝¹ : CompleteSpace E
inst✝ : CompleteSpace F
f : V → E
g : W → F
M : E →L⋆[ℂ] F →L[ℂ] G
he : Continuous[inst✝¹¹, _] ⇑e
hL : Continuous[instTopologicalSpaceProd, inst✝¹¹] fun p ↦ (L p.1) p.2
hf : Integrable f μ
hg : Integrable g ν
hG : CompleteSpace G
⊢ ∫ (x : V), ∫ (ξ : W), (M (f x)) (e ((L.flip ξ) x) • g ξ) ∂ν ∂μ =
    ∫ (x : V), ∫ (ξ : W), (M (f x)) (e (-(-L.flip ξ) x) • g ξ) ∂ν ∂μ

Tactic:
by
    simp only [LinearMap.flip_apply, ContinuousLinearMap.map_smul_of_tower, LinearMap.neg_apply,
      neg_neg]

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

Goal state before:
pp: s : ℂ
hs : 0 < s.re
X : ℝ
hX : 0 ≤ X
⊢ 0 < (s + 1).re

Tactic:
simp only [add_re, one_re]; linarith

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

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

Tactic:
abs_of_nonneg (exp_pos _).le

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

Goal state before:
pp: case succ
𝕜 : Type u_1
inst✝¹ : NormedCommRing 𝕜
n : ℕ
n_ih :
  ∀ {E : Fin n → Type u_3} {mE : (i : Fin n) → MeasurableSpace (E i)} {μ : (i : Fin n) → Measure (E i)}
    [∀ (i : Fin n), SigmaFinite (μ i)] {f : (i : Fin n) → E i → 𝕜},
    (∀ (i : Fin n), Integrable (f i) (μ i)) → Integrable (fun x ↦ ∏ i, f i (x i)) (Measure.pi μ)
E : Fin (n + 1) → Type u_3
mE : (i : Fin (n + 1)) → MeasurableSpace (E i)
μ : (i : Fin (n + 1)) → Measure (E i)
inst✝ : ∀ (i : Fin (n + 1)), SigmaFinite (μ i)
f : (i : Fin (n + 1)) → E i → 𝕜
hf : ∀ (i : Fin (n + 1)), Integrable (f i) (μ i)
this :
  MeasurePreserving (⇑(MeasurableEquiv.piFinSuccAbove E 0).symm) ((μ 0).prod (Measure.pi fun j ↦ μ (Fin.succAbove 0 j)))
    (Measure.pi μ)
⊢ Integrable
    ((fun x ↦ f 0 (x 0) * ∏ i, f i.succ (x i.succ)) ∘
      ⇑{ toFun := fun f ↦ Fin.cons f.1 fun j ↦ cast ⋯ (f.2 j), invFun := fun f ↦ (f 0, Fin.removeNth 0 f),
          left_inv := ⋯, right_inv := ⋯ })
    ((μ 0).prod (Measure.pi fun j ↦ μ (Fin.succAbove 0 j)))

Tactic:
simp only [Fin.zero_succAbove, Function.comp_def]

Goal state after:
case succ
𝕜 : Type u_1
inst✝¹ : NormedCommRing 𝕜
n : ℕ
n_ih :
  ∀ {E : Fin n → Type u_3} {mE : (i : Fin n) → MeasurableSpace (E i)} {μ : (i : Fin n) → Measure (E i)}
    [∀ (i : Fin n), SigmaFinite (μ i)] {f : (i : Fin n) → E i → 𝕜},
    (∀ (i : Fin n), Integrable (f i) (μ i)) → Integrable (fun x ↦ ∏ i, f i (x i)) (Measure.pi μ)
E : Fin (n + 1) → Type u_3
mE : (i : Fin (n + 1)) → MeasurableSpace (E i)
μ : (i : Fin (n + 1)) → Measure (E i)
inst✝ : ∀ (i : Fin (n + 1)), SigmaFinite (μ i)
f : (i : Fin (n + 1)) → E i → 𝕜
hf : ∀ (i : Fin (n + 1)), Integrable (f i) (μ i)
this :
  MeasurePreserving (⇑(MeasurableEquiv.piFinSuccAbove E 0).symm) ((μ 0).prod (Measure.pi fun j ↦ μ (Fin.succAbove 0 j)))
    (Measure.pi μ)
⊢ Integrable
    (fun x ↦
      f 0
          ({ toFun := fun f ↦ Fin.cons f.1 fun j ↦ cast ⋯ (f.2 j), invFun := fun f ↦ (f 0, Fin.removeNth 0 f),
              left_inv := ⋯, right_inv := ⋯ }
            x 0) *
        ∏ i,
          f i.succ
            ({ toFun := fun f ↦ Fin.cons f.1 fun j ↦ cast ⋯ (f.2 j), invFun := fun f ↦ (f 0, Fin.removeNth 0 f),
                left_inv := ⋯, right_inv := ⋯ }
              x i.succ))
    ((μ 0).prod (Measure.pi fun j ↦ μ j.succ))
Module: Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform

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

Tactic:
refine (tendsto_exp_atBot.comp (tendsto_neg_atTop_atBot.comp ?_)).const_mul _

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

Goal state before:
pp: b : ℂ
hb : 0 < b.re
c : ℝ
I₁ : ℝ → ℂ := fun T ↦ ∫ (x : ℝ) in -T..T, cexp (-b * (↑x + ↑c * I) ^ 2)
HI₁ : I₁ = fun T ↦ ∫ (x : ℝ) in -T..T, cexp (-b * (↑x + ↑c * I) ^ 2)
I₂ : ℝ → ℂ := fun T ↦ ∫ (x : ℝ) in -T..T, cexp (-b * ↑x ^ 2)
⊢ Tendsto (fun i ↦ ∫ (x : ℝ) in -i..id i, cexp (-b * (↑x + ↑c * I) ^ 2)) atTop (𝓝 ((↑π / b) ^ (1 / 2)))

Tactic:
let I₄ := fun T : ℝ => ∫ y : ℝ in (0 : ℝ)..c, cexp (-b * (T + y * I) ^ 2)

Goal state after:
b : ℂ
hb : 0 < b.re
c : ℝ
I₁ : ℝ → ℂ := fun T ↦ ∫ (x : ℝ) in -T..T, cexp (-b * (↑x + ↑c * I) ^ 2)
HI₁ : I₁ = fun T ↦ ∫ (x : ℝ) in -T..T, cexp (-b * (↑x + ↑c * I) ^ 2)
I₂ : ℝ → ℂ := fun T ↦ ∫ (x : ℝ) in -T..T, cexp (-b * ↑x ^ 2)
I₄ : ℝ → ℂ := fun T ↦ ∫ (y : ℝ) in 0..c, cexp (-b * (↑T + ↑y * I) ^ 2)
⊢ Tendsto (fun i ↦ ∫ (x : ℝ) in -i..id i, cexp (-b * (↑x + ↑c * I) ^ 2)) atTop (𝓝 ((↑π / b) ^ (1 / 2)))
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic

Goal state before:
pp: case succ
n✝ : ℕ
n_ih : ∀ {s : ℝ}, (∀ (m : ℕ), s ≠ -↑m) → -↑n✝ < s → Gamma s ≠ 0
s : ℝ
hs : ∀ (m : ℕ), s ≠ -↑m
⊢ -↑(n✝ + 1) < s → Gamma s ≠ 0

Tactic:
intro hs'
    have : Gamma (s + 1) ≠ 0 := by
      apply n_ih
      · intro m
        specialize hs (1 + m)
        contrapose hs
        rw [← eq_sub_iff_add_eq] at hs
        rw [hs]
        push_cast
        ring
      · rw [Nat.cast_add, Nat.cast_one, neg_add] at hs'
        linarith
    rw [Gamma_add_one, mul_ne_zero_iff] at this
    · exact this.2
    · simpa using hs 0

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

Goal state before:
pp: b : ℂ
hb : b.re < 0
c d : ℂ
hb' : b ≠ 0
h : ∀ (x : ℝ), cexp (b * ↑x ^ 2 + c * ↑x + d) = cexp (- -b * (↑x + c / (2 * b)) ^ 2) * cexp (d - c ^ 2 / (4 * b))
⊢ (∫ (x : ℝ), cexp (- -b * (↑x + ↑(c / (2 * b)).im * I) ^ 2) ∂volume) * cexp (d - c ^ 2 / (4 * b)) =
    (↑π / -b) ^ (1 / 2) * cexp (d - c ^ 2 / (4 * b))

Tactic:
integral_cexp_neg_mul_sq_add_real_mul_I ((neg_re b).symm ▸ (neg_pos.mpr hb))

Goal state after:
b : ℂ
hb : b.re < 0
c d : ℂ
hb' : b ≠ 0
h : ∀ (x : ℝ), cexp (b * ↑x ^ 2 + c * ↑x + d) = cexp (- -b * (↑x + c / (2 * b)) ^ 2) * cexp (d - c ^ 2 / (4 * b))
⊢ (↑π / -b) ^ (1 / 2) * cexp (d - c ^ 2 / (4 * b)) = (↑π / -b) ^ (1 / 2) * cexp (d - c ^ 2 / (4 * b))
Module: Mathlib.Analysis.Distribution.SchwartzSpace.Fourier

Goal state before:
pp: case refine_3
𝕜 : 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
⊢ ∀ (f : 𝓢(V, E)), ContDiff ℝ (↑⊤) (𝓕 ⇑f)

Tactic:
exact fun f ↦ contDiff_fourier (fun n _ ↦ integrable_pow_mul volume f n)

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

Goal state before:
pp: 𝕜 : 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
f : 𝓢(V, E)
x : V
⊢ fderiv ℝ (𝓕 ⇑f) x = 𝓕 (VectorFourier.fourierSMulRight (innerSL ℝ) ⇑f) x

Tactic:
fderiv_fourier f.integrable

Goal state after:
𝕜 : 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
f : 𝓢(V, E)
x : V
⊢ 𝓕 (VectorFourier.fourierSMulRight (innerSL ℝ) ⇑f) x = 𝓕 (VectorFourier.fourierSMulRight (innerSL ℝ) ⇑f) x

𝕜 : 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
f : 𝓢(V, E)
x : V
⊢ Integrable (fun v ↦ ‖v‖ * ‖f v‖) volume
Module: Mathlib.Analysis.Distribution.Support

Goal state before:
pp: case a
E : Type u_11
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
Ω : Opens E
n : ℕ∞
inst✝ : FiniteDimensional ℝ E
x : E
hx : x ∈ Ω
s : Set E
hxs : x ∈ s
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
⊢ ∃ u, tsupport ⇑u ⊆ s ∧ (delta x) u ≠ 0

Tactic:
set t := s ∩ Ω

Goal state after:
case a
E : Type u_11
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
Ω : Opens E
n : ℕ∞
inst✝ : FiniteDimensional ℝ E
x : E
hx : x ∈ Ω
s : Set E
hxs : x ∈ s
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
t : Set E := s ∩ ↑Ω
⊢ ∃ u, tsupport ⇑u ⊆ s ∧ (delta x) u ≠ 0
Module: Mathlib.Analysis.Fourier.BoundedContinuousFunctionChar

Goal state before:
pp: V : Type u_1
W : Type u_2
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module ℝ V
inst✝³ : TopologicalSpace V
inst✝² : AddCommGroup W
inst✝¹ : Module ℝ W
inst✝ : TopologicalSpace W
e : AddChar ℝ Circle
L : V →ₗ[ℝ] W →ₗ[ℝ] ℝ
he : Continuous ⇑e
he' : e ≠ 1
hL : Continuous fun p ↦ (L p.1) p.2
hL' : ∀ (v : V), v ≠ 0 → L v ≠ 0
v v' : V
hvv' : v ≠ v'
⊢ ∃ w, (char he hL w) v ≠ (char he hL w) v'

Tactic:
by
    contrapose! hvv'
    exact ext_of_char_eq he he' hL hL' hvv'

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 : ℝ
hs : ↑(Module.finrank ℝ E) < 2 * s
f : 𝓢'(E, F)
hf : MemSobolev s 2 f
u : ↥(Lp F 2 volume)
hu : (smulLeftCLM F fun x ↦ ↑((1 + ‖x‖ ^ 2) ^ (s / 2))) (𝓕 f) = Lp.toTemperedDistribution u
h : ∫⁻ (a : E), ENNReal.ofReal ‖(1 + ‖a‖ ^ 2) ^ (-s)‖ < ∞
⊢ ∫⁻ (a : E), ‖(1 + ‖a‖ ^ 2) ^ (-s / 2)‖ₑ ^ 2 < ∞

Tactic:
ofReal_norm

Goal state after:
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 : ℝ
hs : ↑(Module.finrank ℝ E) < 2 * s
f : 𝓢'(E, F)
hf : MemSobolev s 2 f
u : ↥(Lp F 2 volume)
hu : (smulLeftCLM F fun x ↦ ↑((1 + ‖x‖ ^ 2) ^ (s / 2))) (𝓕 f) = Lp.toTemperedDistribution u
h : ∫⁻ (a : E), ‖(1 + ‖a‖ ^ 2) ^ (-s)‖ₑ < ∞
⊢ ∫⁻ (a : E), ‖(1 + ‖a‖ ^ 2) ^ (-s / 2)‖ₑ ^ 2 < ∞
Module: Mathlib.Analysis.Fourier.FiniteAbelian.PontryaginDuality

Goal state before:
pp: α : Type u_1
inst✝² : AddCommGroup α
n✝ : ℕ
a✝ b✝ : α
n : ℕ
inst✝¹ : NeZero n
inst✝ : Finite α
ψ : AddChar α ℂ
a b : α
⊢ ⟨ψ (a + b), ⋯⟩ = ⟨ψ a, ⋯⟩ * ⟨ψ b, ⋯⟩

Tactic:
ext : 1

Goal state after:
α : Type u_1
inst✝² : AddCommGroup α
n✝ : ℕ
a✝ b✝ : α
n : ℕ
inst✝¹ : NeZero n
inst✝ : Finite α
ψ : AddChar α ℂ
a b : α
⊢ ↑⟨ψ (a + b), ⋯⟩ = ↑(⟨ψ a, ⋯⟩ * ⟨ψ b, ⋯⟩)
Module: Mathlib.Analysis.Fourier.FiniteAbelian.PontryaginDuality

Goal state before:
pp: α : Type u_1
inst✝² : AddCommGroup α
n✝ : ℕ
a b : α
n : ℕ
inst✝¹ : NeZero n
inst✝ : Finite α
ψ : AddChar α Circle
⊢ (fun ψ ↦ { toFun := fun a ↦ ⟨ψ a, ⋯⟩, map_zero_eq_one' := ⋯, map_add_eq_mul' := ⋯ })
      ((fun ψ ↦ toMonoidHomEquiv.symm (coeHom.comp ψ.toMonoidHom)) ψ) =
    ψ

Tactic:
ext : 1

Goal state after:
α : Type u_1
inst✝² : AddCommGroup α
n✝ : ℕ
a b : α
n : ℕ
inst✝¹ : NeZero n
inst✝ : Finite α
ψ : AddChar α Circle
x✝ : α
⊢ ((fun ψ ↦ { toFun := fun a ↦ ⟨ψ a, ⋯⟩, map_zero_eq_one' := ⋯, map_add_eq_mul' := ⋯ })
        ((fun ψ ↦ toMonoidHomEquiv.symm (coeHom.comp ψ.toMonoidHom)) ψ))
      x✝ =
    ψ x✝
Module: Mathlib.Analysis.Fourier.FiniteAbelian.PontryaginDuality

Goal state before:
pp: α : Type u_1
inst✝² : AddCommGroup α
n✝ : ℕ
a b : α
n : ℕ
inst✝¹ : NeZero n
inst✝ : Finite α
ψ : AddChar α ℂ
⊢ (fun ψ ↦ toMonoidHomEquiv.symm (coeHom.comp ψ.toMonoidHom))
      ((fun ψ ↦ { toFun := fun a ↦ ⟨ψ a, ⋯⟩, map_zero_eq_one' := ⋯, map_add_eq_mul' := ⋯ }) ψ) =
    ψ

Tactic:
ext : 1

Goal state after:
α : Type u_1
inst✝² : AddCommGroup α
n✝ : ℕ
a b : α
n : ℕ
inst✝¹ : NeZero n
inst✝ : Finite α
ψ : AddChar α ℂ
x✝ : α
⊢ ((fun ψ ↦ toMonoidHomEquiv.symm (coeHom.comp ψ.toMonoidHom))
        ((fun ψ ↦ { toFun := fun a ↦ ⟨ψ a, ⋯⟩, map_zero_eq_one' := ⋯, map_add_eq_mul' := ⋯ }) ψ))
      x✝ =
    ψ x✝
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 : ℝ
f : 𝓢'(E, F)
hf : MemSobolev s 2 f
m x : E
⊢ 1 + ‖x‖ ^ 2 = ((1 + ‖x‖ ^ 2) ^ (1 / 2)) ^ 2

Tactic:
← Real.rpow_mul (by positivity)

Goal state after:
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 : ℝ
f : 𝓢'(E, F)
hf : MemSobolev s 2 f
m x : E
⊢ 1 + ‖x‖ ^ 2 = (1 + ‖x‖ ^ 2) ^ (1 / 2 * 2)
Module: Mathlib.Data.PNat.Prime

Goal state before:
pp: m n : ℕ+
k l : ℕ
h : (↑m).Coprime ↑n
⊢ (↑m).Coprime ↑n

Tactic:
apply h

Goal state after: