mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.InnerProductSpace.l2Space

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

Tactic:
refine (hasSum_inner (lp.single 2 i a) f).unique ?_
  simp_rw [lp.coeFn_single]
  convert! hasSum_ite_eq i ⟪a, f i⟫ using 1
  ext j
  split_ifs with h
  · subst h; rw [Pi.single_eq_same]
  · simp [Pi.single_eq_of_ne h]

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
i j : ℕ
⊢ (fun x ↦ x • D.e i)
      (({ toFun := coeff i, map_add' := ⋯, map_smul' := ⋯ }.mkContinuous (‖succSub D.P i‖ / ‖D.e i‖) ⋯) (D.e j)) =
    (fun x ↦ x • D.e i) (Pi.single j 1 i)

Tactic:
by
      obtain ⟨x, hx⟩ : ∃ x, (succSub D.P j) x = D.e j := D.e_mem_range j
      simp only [mkContinuous_apply, LinearMap.coe_mk, AddHom.coe_mk]
      rw [← hcoeff, ← hx, succSub_ortho D.proj_comp, hx]
      simp only [Pi.single_apply]
      split_ifs with h <;> simp [h]

Goal state after:
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
inst✝¹ : CompleteSpace E
F : ι → Submodule 𝕜 E
inst✝ : ∀ (i : ι), CompleteSpace ↥(F i)
hFortho : OrthogonalFamily 𝕜 (fun i ↦ ↥(F i)) fun i ↦ (F i).subtypeₗᵢ
hFtotal : ⊤ ≤ (⨆ i, F i).topologicalClosure
⊢ ⊤ ≤ (⨆ i, (F i).subtypeₗᵢ.range).topologicalClosure

Tactic:
by simpa [subtypeₗᵢ_toLinearMap, range_subtype] using hFtotal

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

Goal state before:
pp: ι : Type u_1
𝕜 : Type u_2
inst✝⁷ : RCLike 𝕜
E : Type u_3
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : InnerProductSpace 𝕜 E
G : ι → Type u_4
inst✝⁴ : (i : ι) → NormedAddCommGroup (G i)
inst✝³ : (i : ι) → InnerProductSpace 𝕜 (G i)
inst✝² : CompleteSpace E
V : (i : ι) → G i →ₗᵢ[𝕜] E
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (G i)
hV : IsHilbertSum 𝕜 G V
W₀ : Π₀ (i : ι), G i
⊢ ↑(hV.linearIsometryEquiv (hV.linearIsometryEquiv.symm (W₀.sum (lp.single 2)))) = ⇑W₀

Tactic:
rw [LinearIsometryEquiv.apply_symm_apply]

Goal state after:
ι : Type u_1
𝕜 : Type u_2
inst✝⁷ : RCLike 𝕜
E : Type u_3
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : InnerProductSpace 𝕜 E
G : ι → Type u_4
inst✝⁴ : (i : ι) → NormedAddCommGroup (G i)
inst✝³ : (i : ι) → InnerProductSpace 𝕜 (G i)
inst✝² : CompleteSpace E
V : (i : ι) → G i →ₗᵢ[𝕜] E
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (G i)
hV : IsHilbertSum 𝕜 G V
W₀ : Π₀ (i : ι), G i
⊢ ↑(W₀.sum (lp.single 2)) = ⇑W₀
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 α
φ : ι → α → ℝ
a : E
hs : MeasurableSet s
h'st : t ∈ 𝓝[s] x₀
hlφ : ∀ (u : Set α), IsOpen[inst✝³] u → x₀ ∈ u → TendstoUniformlyOn φ 0 l (s \ u)
hiφ : Tendsto (fun e ↦ ‖∫ (x : α) in t, φ e x ∂μ - 1‖) l (𝓝 0)
h'iφ : ∀ᶠ (i : ι) in l, AEStronglyMeasurable (φ i) (μ.restrict s)
hmg : IntegrableOn g s μ
hcg : Tendsto g (𝓝[s] x₀) (𝓝 a)
u : Set α
u_open : IsOpen[inst✝³] u
x₀u : x₀ ∈ u
ut : s ∩ u ⊆ t
hu : ∀ x ∈ u ∩ s, g x ∈ ball a 1
i : ι
hi : ∀ x ∈ s \ u, dist (0 x) (φ i x) < 1
h'i : ‖∫ (x : α) in t, φ i x ∂μ - 1‖ < 1
h''i : AEStronglyMeasurable (φ i) (μ.restrict s)
h : ∫ (a : α) in t, φ i a ∂μ = 0
⊢ False

Tactic:
simp [h] at h'i

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 t : Set α
φ : ι → α → ℝ
a : E
hs : MeasurableSet s
h'st : t ∈ 𝓝[s] x₀
hlφ : ∀ (u : Set α), IsOpen[inst✝³] u → x₀ ∈ u → TendstoUniformlyOn φ 0 l (s \ u)
hiφ : Tendsto (fun e ↦ ‖∫ (x : α) in t, φ e x ∂μ - 1‖) l (𝓝 0)
h'iφ : ∀ᶠ (i : ι) in l, AEStronglyMeasurable (φ i) (μ.restrict s)
hmg : IntegrableOn g s μ
hcg : Tendsto g (𝓝[s] x₀) (𝓝 a)
u : Set α
u_open : IsOpen[inst✝³] u
x₀u : x₀ ∈ u
ut : s ∩ u ⊆ t
hu : ∀ x ∈ u ∩ s, g x ∈ ball a 1
i : ι
hi : ∀ x ∈ s \ u, dist (0 x) (φ i x) < 1
h'i : ‖∫ (x : α) in t, φ i x ∂μ - 1‖ < 1
h''i : AEStronglyMeasurable (φ i) (μ.restrict s)
I : IntegrableOn (φ i) t μ
⊢ IntegrableOn (fun x ↦ φ i x • g x) s μ

Tactic:
have A : IntegrableOn (fun x => φ i x • g x) (s \ u) μ := by
    refine Integrable.smul_of_top_right (hmg.mono sdiff_subset le_rfl) ?_
    apply memLp_top_of_bound (h''i.mono_set sdiff_subset) 1
    filter_upwards [self_mem_ae_restrict (hs.diff u_open.measurableSet)] with x hx
    simpa only [Pi.zero_apply, dist_zero_left] using (hi x hx).le

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 α
φ : ι → α → ℝ
a : E
hs : MeasurableSet s
h'st : t ∈ 𝓝[s] x₀
hlφ : ∀ (u : Set α), IsOpen[inst✝³] u → x₀ ∈ u → TendstoUniformlyOn φ 0 l (s \ u)
hiφ : Tendsto (fun e ↦ ‖∫ (x : α) in t, φ e x ∂μ - 1‖) l (𝓝 0)
h'iφ : ∀ᶠ (i : ι) in l, AEStronglyMeasurable (φ i) (μ.restrict s)
hmg : IntegrableOn g s μ
hcg : Tendsto g (𝓝[s] x₀) (𝓝 a)
u : Set α
u_open : IsOpen[inst✝³] u
x₀u : x₀ ∈ u
ut : s ∩ u ⊆ t
hu : ∀ x ∈ u ∩ s, g x ∈ ball a 1
i : ι
hi : ∀ x ∈ s \ u, dist (0 x) (φ i x) < 1
h'i : ‖∫ (x : α) in t, φ i x ∂μ - 1‖ < 1
h''i : AEStronglyMeasurable (φ i) (μ.restrict s)
I : IntegrableOn (φ i) t μ
A : IntegrableOn (fun x ↦ φ i x • g x) (s \ u) μ
⊢ IntegrableOn (fun x ↦ φ i x • g x) s μ
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
δ : ℝ
hδ : δ * ∫ (x : α) in s, ‖g x‖ ∂μ + 2 * δ < ε
δpos : 0 < δ
δone : δ < 1
u : Set α
u_open : IsOpen[inst✝³] u
x₀u : x₀ ∈ u
ut : s ∩ u ⊆ t
hu : ∀ x ∈ u ∩ s, g x ∈ ball 0 δ
i : ι
hi : ∀ x ∈ s \ u, dist (0 x) (φ i x) < δ
h'i : ‖∫ (x : α) in t, φ i x ∂μ - 1‖ < δ
hφpos : ∀ x ∈ s, 0 ≤ φ i x
h''i : IntegrableOn (fun x ↦ φ i x • g x) s μ
h : ∫ (a : α) in t, φ i a ∂μ = 0
⊢ False

Tactic:
simp [h] at h'i

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
δ : ℝ
hδ : δ * ∫ (x : α) in s, ‖g x‖ ∂μ + 2 * δ < ε
δpos : 0 < δ
δone : δ < 1
u : Set α
u_open : IsOpen[inst✝³] u
x₀u : x₀ ∈ u
ut : s ∩ u ⊆ t
hu : ∀ x ∈ u ∩ s, g x ∈ ball 0 δ
i : ι
hi : ∀ x ∈ s \ u, dist (0 x) (φ i x) < δ
hφpos : ∀ x ∈ s, 0 ≤ φ i x
h''i : IntegrableOn (fun x ↦ φ i x • g x) s μ
h : ∫ (a : α) in t, φ i a ∂μ = 0
h'i : 1 < δ
⊢ False
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✝⁴ : NormedSpace 𝕜 F
inst✝³ : SMulCommClass ℝ 𝕜 F
inst✝² : NormedField 𝕜'
inst✝¹ : NormedSpace 𝕜' F
inst✝ : SMulCommClass ℝ 𝕜' F
c : 𝕜
f : 𝓢(E, F)
k n : ℕ
x : E
⊢ ‖x‖ ^ k * ‖iteratedFDeriv ℝ n (c • ⇑f) x‖ = ‖x‖ ^ k * ‖iteratedFDeriv ℝ n (⇑f) x‖ * ‖c‖

Tactic:
rw [mul_comm _ ‖c‖, ← mul_assoc]

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✝⁴ : NormedSpace 𝕜 F
inst✝³ : SMulCommClass ℝ 𝕜 F
inst✝² : NormedField 𝕜'
inst✝¹ : NormedSpace 𝕜' F
inst✝ : SMulCommClass ℝ 𝕜' F
c : 𝕜
f : 𝓢(E, F)
k n : ℕ
x : E
⊢ ‖x‖ ^ k * ‖iteratedFDeriv ℝ n (c • ⇑f) x‖ = ‖c‖ * ‖x‖ ^ k * ‖iteratedFDeriv ℝ n (⇑f) 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 : 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
h : ∫ (a : α) in t, φ i a ∂μ = 0
⊢ False

Tactic:
simp [h] at h'i

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

Goal state before:
pp: case zero_eq
E : Type u_1
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℂ E
V : Type u_2
W : Type u_3
inst✝⁶ : NormedAddCommGroup V
inst✝⁵ : NormedSpace ℝ V
inst✝⁴ : NormedAddCommGroup W
inst✝³ : NormedSpace ℝ W
L : V →L[ℝ] W →L[ℝ] ℝ
f : V → E
inst✝² : MeasurableSpace V
inst✝¹ : BorelSpace V
μ : Measure V
inst✝ : SecondCountableTopology V
N : ℕ∞ω
hf : ∀ (n : ℕ), ↑n ≤ N → Integrable (fun v ↦ ‖v‖ ^ n * ‖f v‖) μ
h'f : AEStronglyMeasurable f μ
w : W
⊢ fourierIntegral 𝐞 μ (ContinuousLinearMap.toLinearMap₁₂ L) (fun x ↦ (fourierPowSMulRight L f x 0) ![]) w =
    fourierIntegral 𝐞 μ (ContinuousLinearMap.toLinearMap₁₂ L) f w

Tactic:
simp only [fourierPowSMulRight_apply, pow_zero, Finset.univ_eq_empty, Finset.prod_empty,
      one_smul]

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

Goal state before:
pp: E : Type u_1
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℂ E
V : Type u_2
W : Type u_3
inst✝⁶ : NormedAddCommGroup V
inst✝⁵ : NormedSpace ℝ V
inst✝⁴ : NormedAddCommGroup W
inst✝³ : NormedSpace ℝ W
L : V →L[ℝ] W →L[ℝ] ℝ
f : V → E
inst✝² : MeasurableSpace V
inst✝¹ : BorelSpace V
μ : Measure V
inst✝ : SecondCountableTopology V
N : ℕ∞ω
hf : ∀ (n : ℕ), ↑n ≤ N → Integrable (fun v ↦ ‖v‖ ^ n * ‖f v‖) μ
h'f : AEStronglyMeasurable f μ
n : ℕ
hn : ↑n < N
w : W
I₁ : Integrable (fun v ↦ fourierPowSMulRight L f v n) μ
v : V
⊢ ‖v‖ * ‖fourierPowSMulRight L f v n‖ ≤ (2 * π * ‖L‖) ^ n * (‖v‖ ^ (n + 1) * ‖f v‖)

Tactic:
calc
      ‖v‖ * ‖fourierPowSMulRight L f v n‖
        ≤ ‖v‖ * ((2 * π * ‖L‖) ^ n * ‖v‖ ^ n * ‖f v‖) := by
          gcongr; apply norm_fourierPowSMulRight_le
      _ = (2 * π * ‖L‖) ^ n * (‖v‖ ^ (n + 1) * ‖f v‖) := by rw [pow_succ]; ring

Goal state after:
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
inst✝² : FiniteDimensional ℝ E
inst✝¹ : BorelSpace E
p : ℝ≥0∞
hp : p ≠ ∞
hp' : Fact (1 ≤ p)
μ : Measure E
hμ : μ.HasTemperateGrowth
inst✝ : IsFiniteMeasureOnCompacts μ
⊢ DenseRange ⇑(toLpCLM ℝ F p μ)

Tactic:
by
  intro f
  refine (mem_closure_iff_nhds_basis Metric.nhds_basis_closedBall).2 fun ε hε ↦ ?_
  obtain ⟨g, hg₁, hg₂, hg₃⟩ := MemLp.exist_eLpNorm_sub_le hp hp'.out (Lp.memLp f) hε
  use (hg₁.toSchwartzMap hg₂).toLp p μ
  have : (f : E → F) - ((hg₁.toSchwartzMap hg₂).toLp p μ : E → F) =ᵐ[μ] (f : E → F) - g := by
    filter_upwards [(hg₁.toSchwartzMap hg₂).coeFn_toLp p μ]
    simp
  simp only [Set.mem_range, toLpCLM_apply, exists_apply_eq_apply, Metric.mem_closedBall', true_and,
    Lp.dist_def, eLpNorm_congr_ae this]
  grw [hg₃, ENNReal.toReal_ofReal hε.le]
  simp

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

Goal state before:
pp: ⊢ Gamma (1 / 2) = √π

Tactic:
rw [Gamma_eq_integral one_half_pos, ← integral_comp_rpow_Ioi_of_pos zero_lt_two]

Goal state after:
⊢ ∫ (x : ℝ) in Ioi 0, (2 * x ^ (2 - 1)) • (rexp (-x ^ 2) * (x ^ 2) ^ (1 / 2 - 1)) = √π
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
hs' : -↑(n✝ + 1) < s
⊢ Gamma s ≠ 0

Tactic:
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

Goal state after:
case succ
n✝ : ℕ
n_ih : ∀ {s : ℝ}, (∀ (m : ℕ), s ≠ -↑m) → -↑n✝ < s → Gamma s ≠ 0
s : ℝ
hs : ∀ (m : ℕ), s ≠ -↑m
hs' : -↑(n✝ + 1) < s
this : Gamma (s + 1) ≠ 0
⊢ Gamma s ≠ 0
Module: Mathlib.Analysis.Fourier.LpSpace

Goal state before:
pp: case h_norm
E : Type u_1
F : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : MeasurableSpace E
inst✝⁵ : BorelSpace E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace ℂ F
inst✝² : CompleteSpace F
inst✝¹ : InnerProductSpace ℝ E
inst✝ : FiniteDimensional ℝ E
f : 𝓢(E, F)
⊢ ∃ C, ∀ (x : 𝓢(E, F)), ‖(↑(toLpCLM ℂ F 2 volume) ∘ₗ ↑(fourierEquiv ℂ 𝓢(E, F))) x‖ ≤ C * ‖↑(toLpCLM ℂ F 2 volume) x‖

Tactic:
use 1

Goal state after:
case h
E : Type u_1
F : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : MeasurableSpace E
inst✝⁵ : BorelSpace E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace ℂ F
inst✝² : CompleteSpace F
inst✝¹ : InnerProductSpace ℝ E
inst✝ : FiniteDimensional ℝ E
f : 𝓢(E, F)
⊢ ∀ (x : 𝓢(E, F)), ‖(↑(toLpCLM ℂ F 2 volume) ∘ₗ ↑(fourierEquiv ℂ 𝓢(E, F))) x‖ ≤ 1 * ‖↑(toLpCLM ℂ F 2 volume) x‖
Module: Mathlib.Analysis.Fourier.LpSpace

Goal state before:
pp: case h_norm
E : Type u_1
F : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : MeasurableSpace E
inst✝⁵ : BorelSpace E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace ℂ F
inst✝² : CompleteSpace F
inst✝¹ : InnerProductSpace ℝ E
inst✝ : FiniteDimensional ℝ E
f : 𝓢(E, F)
⊢ ∃ C,
    ∀ (x : 𝓢(E, F)), ‖(↑(toLpCLM ℂ F 2 volume) ∘ₗ ↑(fourierEquiv ℂ 𝓢(E, F)).symm) x‖ ≤ C * ‖↑(toLpCLM ℂ F 2 volume) x‖

Tactic:
use 1

Goal state after:
case h
E : Type u_1
F : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : MeasurableSpace E
inst✝⁵ : BorelSpace E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace ℂ F
inst✝² : CompleteSpace F
inst✝¹ : InnerProductSpace ℝ E
inst✝ : FiniteDimensional ℝ E
f : 𝓢(E, F)
⊢ ∀ (x : 𝓢(E, F)), ‖(↑(toLpCLM ℂ F 2 volume) ∘ₗ ↑(fourierEquiv ℂ 𝓢(E, F)).symm) x‖ ≤ 1 * ‖↑(toLpCLM ℂ F 2 volume) x‖
Module: Mathlib.Analysis.Fourier.BoundedContinuousFunctionChar

Goal state before:
pp: case h
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
h : v ≠ v'
w : W
hw : (L (v - v')) w ≠ 0 w
a : ℝ
ha : e a ≠ 1 a
⊢ ¬↑(e ((L v) ((a / ((L v) w - (L v') w)) • w))) = ↑(e ((L v') ((a / ((L v) w - (L v') w)) • w)))

Tactic:
rw [← div_eq_one_iff_eq (Circle.coe_ne_zero _), div_eq_inv_mul, ← Metric.unitSphere.coe_inv,
    ← e.map_neg_eq_inv, ← Submonoid.coe_mul, ← e.map_add_eq_mul, OneMemClass.coe_eq_one]

Goal state after:
case h
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
h : v ≠ v'
w : W
hw : (L (v - v')) w ≠ 0 w
a : ℝ
ha : e a ≠ 1 a
⊢ ¬e (-(L v') ((a / ((L v) w - (L v') w)) • w) + (L v) ((a / ((L v) w - (L v') w)) • w)) = 1
Module: Mathlib.Analysis.Fourier.Convolution

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_3
F₁ : Type u_5
F₂ : Type u_6
F₃ : Type u_7
inst✝¹² : NontriviallyNormedField 𝕜
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedAddCommGroup F₁
inst✝⁹ : NormedAddCommGroup F₂
inst✝⁸ : NormedAddCommGroup F₃
inst✝⁷ : InnerProductSpace ℝ E
inst✝⁶ : FiniteDimensional ℝ E
inst✝⁵ : MeasurableSpace E
inst✝⁴ : BorelSpace E
inst✝³ : NormedSpace 𝕜 F₁
inst✝² : NormedSpace 𝕜 F₂
inst✝¹ : NormedSpace 𝕜 F₃
inst✝ : NormedSpace ℂ F₃
B : F₁ →L[𝕜] F₂ →L[𝕜] F₃
f₁ : E → F₁
f₂ : E → F₂
hf₁ : Integrable f₁ volume
hf₂ : Integrable f₂ volume
ξ : E
⊢ 𝓕 (f₁ ⋆[B, volume] f₂) ξ = 𝓕 (f₂ ⋆[B.flip, volume] f₁) ξ

Tactic:
by
    rw [convolution_flip]

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

Goal state before:
pp: E : Type u_3
F : Type u_4
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : InnerProductSpace ℝ E
inst✝⁴ : FiniteDimensional ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℂ F
f : 𝓢'(E, F)
m : E
u : 𝓢(E, ℂ)
this : Function.HasTemperateGrowth fun x ↦ inner ℝ x m
⊢ (𝓕 (∂_{m} f)) u = ((2 * ↑π * Complex.I) • (smulLeftCLM F fun x ↦ ↑(inner ℝ x m)) (𝓕 f)) u

Tactic:
simp [SchwartzMap.lineDerivOp_fourier_eq, ← smulLeftCLM_ofReal ℂ this]

Goal state after:
Module: Mathlib.Analysis.RCLike.Inner

Goal state before:
pp: ι : Type u_1
κ : Type u_2
𝕜 : Type u_3
inst✝¹ : Fintype ι
inst✝ : RCLike 𝕜
f : κ → ι → 𝕜
hf : ∀ (k : κ), f k ≠ 0
hinner : Pairwise fun k₁ k₂ ↦ ⟪f k₁, f k₂⟫_[𝕜] = 0
⊢ LinearIndependent 𝕜 f

Tactic:
by
  simp_rw [wInner_one_eq_inner] at hinner
  have := linearIndependent_of_ne_zero_of_inner_eq_zero ?_ hinner
  exacts [(WithLp.linearEquiv 2 𝕜 (ι → 𝕜)).symm.toLinearMap.linearIndependent_iff_of_injOn
    (toLp_injective 2).injOn |>.1 this, fun i ↦ (toLp_eq_zero 2).ne.2 (hf i)]

Goal state after:
Module: Mathlib.Analysis.Fourier.FiniteAbelian.PontryaginDuality

Goal state before:
pp: α : Type u_1
inst✝¹ : AddCommGroup α
a : α
inst✝ : Finite α
⊢ 𝔼 ψ, ψ a = 0 ↔ a ≠ 0

Tactic:
classical
  cases nonempty_fintype α
  rw [expect_apply_eq_ite, one_ne_zero.ite_eq_right_iff]

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
h' : (s' - s) / 2 ≤ 0
hs : s' = s' - s + s
⊢ ∃ C, ∀ (x : E), ‖↑((1 + ‖x‖ ^ 2) ^ ((s' - s) / 2))‖ ≤ C

Tactic:
use 1

Goal state after:
case h
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
h' : (s' - s) / 2 ≤ 0
hs : s' = s' - s + s
⊢ ∀ (x : E), ‖↑((1 + ‖x‖ ^ 2) ^ ((s' - s) / 2))‖ ≤ 1
Module: Mathlib.Analysis.Fourier.PoissonSummation

Goal state before:
pp: f : C(ℝ, ℂ)
hf : ∀ (K : Compacts ℝ), Summable fun n ↦ ‖ContinuousMap.restrict (↑K) (f.comp (ContinuousMap.addRight ↑n))‖
m : ℤ
e : C(ℝ, ℂ) := (fourier (-m)).comp { toFun := QuotientAddGroup.mk, continuous_toFun := ⋯ }
⊢ fourierCoeff ⋯.lift m = 𝓕 ⇑f ↑m

Tactic:
have neK : ∀ (K : Compacts ℝ) (g : C(ℝ, ℂ)), ‖(e * g).restrict K‖ = ‖g.restrict K‖ := by
    have (x : ℝ) : ‖e x‖ = 1 := (AddCircle.toCircle (-m • x)).norm_coe
    intro K g
    simp_rw [norm_eq_iSup_norm, restrict_apply, mul_apply, norm_mul, this, one_mul]

Goal state after:
f : C(ℝ, ℂ)
hf : ∀ (K : Compacts ℝ), Summable fun n ↦ ‖ContinuousMap.restrict (↑K) (f.comp (ContinuousMap.addRight ↑n))‖
m : ℤ
e : C(ℝ, ℂ) := (fourier (-m)).comp { toFun := QuotientAddGroup.mk, continuous_toFun := ⋯ }
neK : ∀ (K : Compacts ℝ) (g : C(ℝ, ℂ)), ‖ContinuousMap.restrict (↑K) (e * g)‖ = ‖ContinuousMap.restrict (↑K) g‖
⊢ fourierCoeff ⋯.lift m = 𝓕 ⇑f ↑m
Module: Mathlib.Analysis.Fourier.PoissonSummation

Goal state before:
pp: f : C(ℝ, ℂ)
hf : ∀ (K : Compacts ℝ), Summable fun n ↦ ‖ContinuousMap.restrict (↑K) (f.comp (ContinuousMap.addRight ↑n))‖
m : ℤ
e : C(ℝ, ℂ) := (fourier (-m)).comp { toFun := QuotientAddGroup.mk, continuous_toFun := ⋯ }
neK : ∀ (K : Compacts ℝ) (g : C(ℝ, ℂ)), ‖ContinuousMap.restrict (↑K) (e * g)‖ = ‖ContinuousMap.restrict (↑K) g‖
eadd : ∀ (n : ℤ), e.comp (ContinuousMap.addRight ↑n) = e
⊢ ∫ (x : ℝ) in 0..1, e x * (∑' (n : ℤ), f.comp (ContinuousMap.addRight ↑n)) x =
    ∫ (x : ℝ) in 0..1, ∑' (n : ℤ), (⇑e * ⇑(f.comp (ContinuousMap.addRight ↑n))) x

Tactic:
Pi.mul_apply,

Goal state after:
f : C(ℝ, ℂ)
hf : ∀ (K : Compacts ℝ), Summable fun n ↦ ‖ContinuousMap.restrict (↑K) (f.comp (ContinuousMap.addRight ↑n))‖
m : ℤ
e : C(ℝ, ℂ) := (fourier (-m)).comp { toFun := QuotientAddGroup.mk, continuous_toFun := ⋯ }
neK : ∀ (K : Compacts ℝ) (g : C(ℝ, ℂ)), ‖ContinuousMap.restrict (↑K) (e * g)‖ = ‖ContinuousMap.restrict (↑K) g‖
eadd : ∀ (n : ℤ), e.comp (ContinuousMap.addRight ↑n) = e
⊢ ∫ (x : ℝ) in 0..1, e x * (∑' (n : ℤ), f.comp (ContinuousMap.addRight ↑n)) x =
    ∫ (x : ℝ) in 0..1, ∑' (n : ℤ), e x * (f.comp (ContinuousMap.addRight ↑n)) 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
⊢ ∃ C, ∀ (x : E), ‖↑(‖x‖ ^ 2 * (1 + ‖x‖ ^ 2) ^ (-1))‖ ≤ C

Tactic:
use 1

Goal state after:
case h
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
⊢ ∀ (x : E), ‖↑(‖x‖ ^ 2 * (1 + ‖x‖ ^ 2) ^ (-1))‖ ≤ 1
Module: Mathlib.Analysis.Fourier.PoissonSummation

Goal state before:
pp: case e'_3
f : C(ℝ, ℂ)
h_norm : ∀ (K : Compacts ℝ), Summable fun n ↦ ‖ContinuousMap.restrict (↑K) (f.comp (ContinuousMap.addRight ↑n))‖
h_sum : Summable fun n ↦ 𝓕 ⇑f ↑n
x : ℝ
F : C(UnitAddCircle, ℂ) := { toFun := ⋯.lift, continuous_toFun := ⋯ }
this : Summable (fourierCoeff ⇑F)
⊢ ∑' (n : ℤ), 𝓕 ⇑f ↑n * (fourier n) ↑x = ∑' (b : ℤ), fourierCoeff (⇑F) b • (fourier b) ↑x

Tactic:
← Real.fourierCoeff_tsum_comp_add h_norm,

Goal state after:
case e'_3
f : C(ℝ, ℂ)
h_norm : ∀ (K : Compacts ℝ), Summable fun n ↦ ‖ContinuousMap.restrict (↑K) (f.comp (ContinuousMap.addRight ↑n))‖
h_sum : Summable fun n ↦ 𝓕 ⇑f ↑n
x : ℝ
F : C(UnitAddCircle, ℂ) := { toFun := ⋯.lift, continuous_toFun := ⋯ }
this : Summable (fourierCoeff ⇑F)
⊢ ∑' (n : ℤ), fourierCoeff ⋯.lift n * (fourier n) ↑x = ∑' (b : ℤ), fourierCoeff (⇑F) b • (fourier b) ↑x