mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Distribution.Sobolev

Goal state before:
pp: 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✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
s : ℝ
p : ℝ≥0∞
hp : Fact (1 ≤ p)
c : ℂ
f : 𝓢'(E, F)
f' : ↥(Lp F p volume)
hf : (besselPotential E F s) f = Lp.toTemperedDistribution f'
⊢ (besselPotential E F s) (c • f) = (Lp.toTemperedDistributionCLM F volume p) (c • f')

Tactic:
]

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✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
s : ℝ
p : ℝ≥0∞
hp : Fact (1 ≤ p)
c : ℂ
f : 𝓢'(E, F)
f' : ↥(Lp F p volume)
hf : (besselPotential E F s) f = Lp.toTemperedDistribution f'
⊢ (besselPotential E F s) (c • f) = (Lp.toTemperedDistributionCLM F volume p) (c • f')
Module: Mathlib.Analysis.Fourier.AddCircleMulti

Goal state before:
pp: d : Type u_1
inst✝ : Fintype d
x y : UnitAddTorus d
hxy : ∃ x_1, ¬x x_1 = y x_1
⊢ ∃ f ∈ (fun f ↦ ⇑f) '' ↑(mFourierSubalgebra d).toSubalgebra, f x ≠ f y

Tactic:
]

Goal state after:
d : Type u_1
inst✝ : Fintype d
x y : UnitAddTorus d
hxy : ∃ x_1, ¬x x_1 = y x_1
⊢ ∃ f ∈ (fun f ↦ ⇑f) '' ↑(mFourierSubalgebra d).toSubalgebra, f x ≠ f y
Module: Mathlib.Analysis.Distribution.Sobolev

Goal state before:
pp: 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✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
s : ℝ
p : ℝ≥0∞
hp : Fact (1 ≤ p)
⊢ (besselPotential E F s) 0 = (Lp.toTemperedDistributionCLM F volume p) 0

Tactic:
]

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✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
s : ℝ
p : ℝ≥0∞
hp : Fact (1 ≤ p)
⊢ (besselPotential E F s) 0 = (Lp.toTemperedDistributionCLM F volume p) 0
Module: Mathlib.Analysis.Fourier.AddCircleMulti

Goal state before:
pp: d : Type u_1
inst✝ : Fintype d
x y : UnitAddTorus d
i : d
hi : ¬x i = y i
⊢ ¬AddCircle.toCircle (x i) = AddCircle.toCircle (y i)

Tactic:
]

Goal state after:
d : Type u_1
inst✝ : Fintype d
x y : UnitAddTorus d
i : d
hi : ¬x i = y i
⊢ ¬AddCircle.toCircle (x i) = AddCircle.toCircle (y i)
Module: Mathlib.Analysis.Fourier.AddCircleMulti

Goal state before:
pp: d : Type u_1
inst✝ : Fintype d
⊢ (Subalgebra.toSubmodule (mFourierSubalgebra d).toSubalgebra).topologicalClosure = ⊤

Tactic:
]

Goal state after:
d : Type u_1
inst✝ : Fintype d
⊢ (Subalgebra.toSubmodule (mFourierSubalgebra d).toSubalgebra).topologicalClosure = ⊤
Module: Mathlib.Analysis.Distribution.Sobolev

Goal state before:
pp: 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✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
s : ℝ
p : ℝ≥0∞
hp : Fact (1 ≤ p)
f : 𝓢(E, F)
⊢ (SchwartzMap.toTemperedDistributionCLM E F volume)
      ((SchwartzMap.fourierMultiplierCLM F fun x ↦ ↑((1 + ‖x‖ ^ 2) ^ (s / 2))) f) =
    (SchwartzMap.toTemperedDistributionCLM E F volume)
      ((SchwartzMap.fourierMultiplierCLM F fun x ↦ (1 + ‖x‖ ^ 2) ^ (s / 2)) f)

Tactic:
]

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✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
s : ℝ
p : ℝ≥0∞
hp : Fact (1 ≤ p)
f : 𝓢(E, F)
⊢ (SchwartzMap.toTemperedDistributionCLM E F volume)
      ((SchwartzMap.fourierMultiplierCLM F fun x ↦ ↑((1 + ‖x‖ ^ 2) ^ (s / 2))) f) =
    (SchwartzMap.toTemperedDistributionCLM E F volume)
      ((SchwartzMap.fourierMultiplierCLM F fun x ↦ (1 + ‖x‖ ^ 2) ^ (s / 2)) f)
Module: Mathlib.Analysis.Fourier.AddCircleMulti

Goal state before:
pp: case e'_3
d : Type u_1
inst✝ : Fintype d
f : UnitAddTorus d → ℝ≥0∞
a : d → ℝ
⊢ ∫⁻ (x : ↑{f | ∀ (i : d), f i ∈ Ioc (a i) (a i + 1)}), f fun i ↦ ↑(↑x i) ∂Measure.comap Subtype.val volume =
    ∫⁻ (a_1 : { x // ∀ (i : d), x i ∈ Ioc (a i) (a i + 1) }),
      f ((measurableEquivPiIoc a).symm a_1) ∂Measure.comap Subtype.val volume

Tactic:
]

Goal state after:
case e'_3
d : Type u_1
inst✝ : Fintype d
f : UnitAddTorus d → ℝ≥0∞
a : d → ℝ
⊢ ∫⁻ (x : ↑{f | ∀ (i : d), f i ∈ Ioc (a i) (a i + 1)}), f fun i ↦ ↑(↑x i) ∂Measure.comap Subtype.val volume =
    ∫⁻ (a_1 : { x // ∀ (i : d), x i ∈ Ioc (a i) (a i + 1) }),
      f ((measurableEquivPiIoc a).symm a_1) ∂Measure.comap Subtype.val volume
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, volume] f₂) ξ

Tactic:
]

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

Goal state before:
pp: case e'_3
d : Type u_1
inst✝² : Fintype d
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : UnitAddTorus d → E
a : d → ℝ
⊢ ∫ (x : ↑{f | ∀ (i : d), f i ∈ Ioc (a i) (a i + 1)}), f fun i ↦ ↑(↑x i) ∂Measure.comap Subtype.val volume =
    ∫ (x : { x // ∀ (i : d), x i ∈ Ioc (a i) (a i + 1) }),
      f ((measurableEquivPiIoc a).symm x) ∂Measure.comap Subtype.val volume

Tactic:
]

Goal state after:
case e'_3
d : Type u_1
inst✝² : Fintype d
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : UnitAddTorus d → E
a : d → ℝ
⊢ ∫ (x : ↑{f | ∀ (i : d), f i ∈ Ioc (a i) (a i + 1)}), f fun i ↦ ↑(↑x i) ∂Measure.comap Subtype.val volume =
    ∫ (x : { x // ∀ (i : d), x i ∈ Ioc (a i) (a i + 1) }),
      f ((measurableEquivPiIoc a).symm x) ∂Measure.comap Subtype.val volume
Module: Mathlib.Analysis.Fourier.AddCircleMulti

Goal state before:
pp: d : Type u_1
inst✝ : Fintype d
⊢ ∀ (i j : d → ℤ), inner ℂ (mFourierLp 2 i) (mFourierLp 2 j) = if i = j then 1 else 0

Tactic:
]

Goal state after:
d : Type u_1
inst✝ : Fintype d
⊢ ∀ (i j : d → ℤ), inner ℂ (mFourierLp 2 i) (mFourierLp 2 j) = if i = j then 1 else 0
Module: Mathlib.Analysis.Distribution.Sobolev

Goal state before:
pp: 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)
f' : ↥(Lp F 2 volume)
hf' : (smulLeftCLM F fun x ↦ ↑((1 + ‖x‖ ^ 2) ^ (s / 2))) (𝓕 f) = 𝓕 (Lp.toTemperedDistribution f')
⊢ (smulLeftCLM F fun x ↦ ↑((1 + ‖x‖ ^ 2) ^ (s / 2))) (𝓕 f) = Lp.toTemperedDistribution (𝓕 f')

Tactic:
]

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)
f' : ↥(Lp F 2 volume)
hf' : (smulLeftCLM F fun x ↦ ↑((1 + ‖x‖ ^ 2) ^ (s / 2))) (𝓕 f) = 𝓕 (Lp.toTemperedDistribution f')
⊢ (smulLeftCLM F fun x ↦ ↑((1 + ‖x‖ ^ 2) ^ (s / 2))) (𝓕 f) = Lp.toTemperedDistribution (𝓕 f')
Module: Mathlib.Analysis.Fourier.AddCircleMulti

Goal state before:
pp: case neg
d : Type u_1
inst✝ : Fintype d
m n : d → ℤ
h : ¬m = n
⊢ ∏ i, ∫ (x : UnitAddCircle), (fourier ((n + -m) i)) x = 0

Tactic:
]

Goal state after:
case neg
d : Type u_1
inst✝ : Fintype d
m n : d → ℤ
h : ¬m = n
⊢ ∏ i, ∫ (x : UnitAddCircle), (fourier ((n + -m) i)) x = 0
Module: Mathlib.Analysis.Distribution.Sobolev

Goal state before:
pp: 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)
f' : ↥(Lp F 2 volume)
hf' : (smulLeftCLM F fun x ↦ ↑((1 + ‖x‖ ^ 2) ^ (s / 2))) (𝓕 f) = 𝓕 (Lp.toTemperedDistribution f')
⊢ Lp.toTemperedDistribution (𝓕 f') = Lp.toTemperedDistribution (𝓕 f')

Tactic:
]

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

Goal state before:
pp: case mp
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)
⊢ MemSobolev s 2 f → ∃ f', (smulLeftCLM F fun x ↦ ↑((1 + ‖x‖ ^ 2) ^ (s / 2))) (𝓕 f) = Lp.toTemperedDistribution f'

pp: case mpr
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)
⊢ (∃ f', (smulLeftCLM F fun x ↦ ↑((1 + ‖x‖ ^ 2) ^ (s / 2))) (𝓕 f) = Lp.toTemperedDistribution f') → MemSobolev s 2 f

Tactic:
· intro ⟨f', hf'⟩
    use 𝓕 f'
    apply_fun 𝓕 at hf'
    rw [fourier_besselPotential_eq_smulLeftCLM_fourier_apply] at hf'
    rw [hf', Lp.fourier_toTemperedDistribution_eq f']

Goal state after:
case mpr
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)
⊢ (∃ f', (smulLeftCLM F fun x ↦ ↑((1 + ‖x‖ ^ 2) ^ (s / 2))) (𝓕 f) = Lp.toTemperedDistribution f') → MemSobolev s 2 f
Module: Mathlib.Analysis.Fourier.AddCircleMulti

Goal state before:
pp: d : Type u_1
inst✝ : Fintype d
f : ↥(Lp ℂ 2 volume)
i : d → ℤ
⊢ ∫ (a : UnitAddTorus d), inner ℂ (↑↑(mFourierLp 2 i) a) (↑↑f a) =
    ∫ (t : UnitAddTorus d), (starRingEnd ℂ) (↑↑(mFourierLp 2 i) t) * ↑↑f t

Tactic:
]

Goal state after:
d : Type u_1
inst✝ : Fintype d
f : ↥(Lp ℂ 2 volume)
i : d → ℤ
⊢ ∫ (a : UnitAddTorus d), inner ℂ (↑↑(mFourierLp 2 i) a) (↑↑f a) =
    ∫ (t : UnitAddTorus d), (starRingEnd ℂ) (↑↑(mFourierLp 2 i) t) * ↑↑f t
Module: Mathlib.Analysis.Distribution.Sobolev

Goal state before:
pp: case mpr
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)
f' : ↥(Lp F 2 volume)
hf' : (smulLeftCLM F fun x ↦ ↑((1 + ‖x‖ ^ 2) ^ (s / 2))) (𝓕 f) = Lp.toTemperedDistribution f'
⊢ MemSobolev s 2 f

Tactic:
use 𝓕⁻ f'

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)
f' : ↥(Lp F 2 volume)
hf' : (smulLeftCLM F fun x ↦ ↑((1 + ‖x‖ ^ 2) ^ (s / 2))) (𝓕 f) = Lp.toTemperedDistribution f'
⊢ (besselPotential E F s) f = Lp.toTemperedDistribution (𝓕⁻ f')
Module: Mathlib.Analysis.Distribution.Sobolev

Goal state before:
pp: 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)
f' : ↥(Lp F 2 volume)
hf' : (smulLeftCLM F fun x ↦ ↑((1 + ‖x‖ ^ 2) ^ (s / 2))) (𝓕 f) = Lp.toTemperedDistribution f'
⊢ 𝓕⁻ ((smulLeftCLM F fun x ↦ ↑((1 + ‖x‖ ^ 2) ^ (s / 2))) (𝓕 f)) = Lp.toTemperedDistribution (𝓕⁻ f')

Tactic:
]

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)
f' : ↥(Lp F 2 volume)
hf' : (smulLeftCLM F fun x ↦ ↑((1 + ‖x‖ ^ 2) ^ (s / 2))) (𝓕 f) = Lp.toTemperedDistribution f'
⊢ 𝓕⁻ ((smulLeftCLM F fun x ↦ ↑((1 + ‖x‖ ^ 2) ^ (s / 2))) (𝓕 f)) = Lp.toTemperedDistribution (𝓕⁻ f')
Module: Mathlib.Analysis.Fourier.AddCircleMulti

Goal state before:
pp: d : Type u_1
inst✝ : Fintype d
f : ↥(Lp ℂ 2 volume)
i : d → ℤ
a✝ : UnitAddTorus d
ht : ↑↑(mFourierLp 2 i) a✝ = (mFourier i) a✝
⊢ (mFourier (-i)) a✝ * ↑↑f a✝ = (mFourier (-i)) a✝ * ↑↑f a✝

Tactic:
]

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

Goal state before:
pp: 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)
f' : ↥(Lp F 2 volume)
hf' : 𝓕⁻ ((smulLeftCLM F fun x ↦ ↑((1 + ‖x‖ ^ 2) ^ (s / 2))) (𝓕 f)) = 𝓕⁻ (Lp.toTemperedDistribution f')
⊢ Lp.toTemperedDistribution (𝓕⁻ f') = Lp.toTemperedDistribution (𝓕⁻ f')

Tactic:
]

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
inst✝ : CompleteSpace F
f : 𝓢(E, F)
⊢ 𝓕⁻ ((toTemperedDistributionCLM E F volume) (𝓕 (𝓕⁻ f))) = 𝓕⁻ ((toTemperedDistributionCLM E F volume) (𝓕 (𝓕⁻ f)))

Tactic:
]

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

Goal state before:
pp: ι : Type u_1
𝕜 : Type u_3
E : ι → Type u_4
inst✝³ : Fintype ι
inst✝² : RCLike 𝕜
inst✝¹ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝ : (i : ι) → InnerProductSpace 𝕜 (E i)
c : 𝕜
w : ι → ℝ
f g : (i : ι) → E i
⊢ c * ⟪f, g⟫_[𝕜, w] = c * ⟪f, g⟫_[𝕜, w]

Tactic:
]

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

Goal state before:
pp: case right
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
⊢ ∫⁻ (a : E), ‖(1 + ‖a‖ ^ 2) ^ (-s / 2)‖ₑ ^ ENNReal.toReal 2 < ∞

Tactic:
]

Goal state after:
case right
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
⊢ ∫⁻ (a : E), ‖(1 + ‖a‖ ^ 2) ^ (-s / 2)‖ₑ ^ ENNReal.toReal 2 < ∞
Module: Mathlib.Analysis.Fourier.Convolution

Goal state before:
pp: E : Type u_3
F₁ : Type u_5
F₂ : Type u_6
F₃ : Type u_7
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✝⁴ : CompleteSpace F₁
inst✝³ : CompleteSpace F₂
inst✝² : CompleteSpace 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
⊢ ∫ (y : E), (∫ (x : E), B (𝐞 (-inner ℝ x ξ) • f₁ x)) (𝐞 (-inner ℝ y ξ) • f₂ y) =
    ∫ (x : E), (∫ (x : E), B (𝐞 (-inner ℝ x ξ) • f₁ x)) (𝐞 (-inner ℝ x ξ) • f₂ x)

Tactic:
]

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

Goal state before:
pp: G : Type u_1
R : Type u_3
inst✝³ : AddGroup G
inst✝² : Fintype G
inst✝¹ : Semifield R
inst✝ : CharZero R
ψ : AddChar G R
⊢ ¬ψ = 0 ↔ ψ ≠ 0

Tactic:
]

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

Goal state before:
pp: case pos
G : Type u_1
R : Type u_3
inst✝² : AddCommGroup G
inst✝¹ : RCLike R
inst✝ : Fintype G
ψ₁ ψ₂ : AddChar G R
h : ψ₁ = ψ₂
⊢ 1 = 1

Tactic:
]

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

Goal state before:
pp: E : Type u_3
F₁ : Type u_5
F₂ : Type u_6
F₃ : Type u_7
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : InnerProductSpace ℝ E
inst✝¹¹ : FiniteDimensional ℝ E
inst✝¹⁰ : MeasurableSpace E
inst✝⁹ : BorelSpace E
inst✝⁸ : NormedAddCommGroup F₁
inst✝⁷ : NormedSpace ℂ F₁
inst✝⁶ : NormedAddCommGroup F₂
inst✝⁵ : NormedSpace ℂ F₂
inst✝⁴ : NormedAddCommGroup F₃
inst✝³ : NormedSpace ℂ F₃
inst✝² : CompleteSpace F₃
inst✝¹ : CompleteSpace F₁
inst✝ : CompleteSpace F₂
B : F₁ →L[ℂ] F₂ →L[ℂ] F₃
f : 𝓢(E, F₁)
g : 𝓢(E, F₂)
x : E
⊢ 𝓕⁻ (⇑(𝓕 (((convolution B) f) g))) x = 𝓕⁻ (fun y ↦ 𝓕 (⇑f ⋆[B, volume] ⇑g) y) x

Tactic:
]

Goal state after:
E : Type u_3
F₁ : Type u_5
F₂ : Type u_6
F₃ : Type u_7
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : InnerProductSpace ℝ E
inst✝¹¹ : FiniteDimensional ℝ E
inst✝¹⁰ : MeasurableSpace E
inst✝⁹ : BorelSpace E
inst✝⁸ : NormedAddCommGroup F₁
inst✝⁷ : NormedSpace ℂ F₁
inst✝⁶ : NormedAddCommGroup F₂
inst✝⁵ : NormedSpace ℂ F₂
inst✝⁴ : NormedAddCommGroup F₃
inst✝³ : NormedSpace ℂ F₃
inst✝² : CompleteSpace F₃
inst✝¹ : CompleteSpace F₁
inst✝ : CompleteSpace F₂
B : F₁ →L[ℂ] F₂ →L[ℂ] F₃
f : 𝓢(E, F₁)
g : 𝓢(E, F₂)
x : E
⊢ 𝓕⁻ (⇑(𝓕 (((convolution B) f) g))) x = 𝓕⁻ (fun y ↦ 𝓕 (⇑f ⋆[B, volume] ⇑g) y) x
Module: Mathlib.Analysis.Fourier.FiniteAbelian.Orthogonality

Goal state before:
pp: G : Type u_1
R : Type u_3
inst✝² : AddCommGroup G
inst✝¹ : RCLike R
inst✝ : Fintype G
ψ₁ ψ₂ : AddChar G R
h : ¬ψ₁ = ψ₂
⊢ ¬ψ₁ = ψ₂

Tactic:
]

Goal state after:
G : Type u_1
R : Type u_3
inst✝² : AddCommGroup G
inst✝¹ : RCLike R
inst✝ : Fintype G
ψ₁ ψ₂ : AddChar G R
h : ¬ψ₁ = ψ₂
⊢ ¬ψ₁ = ψ₂
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), ‖(1 + ‖a‖ ^ 2) ^ (-s)‖ₑ < ∞
x✝ : E
⊢ (1 + ‖x✝‖ ^ 2) ^ (-s / 2 * ↑2) = (1 + ‖x✝‖ ^ 2) ^ (-s)

Tactic:
]

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)‖ₑ < ∞
x✝ : E
⊢ (1 + ‖x✝‖ ^ 2) ^ (-s / 2 * ↑2) = (1 + ‖x✝‖ ^ 2) ^ (-s)
Module: Mathlib.Analysis.Fourier.Convolution

Goal state before:
pp: E : Type u_3
F₁ : Type u_5
F₂ : Type u_6
F₃ : Type u_7
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : InnerProductSpace ℝ E
inst✝¹¹ : FiniteDimensional ℝ E
inst✝¹⁰ : MeasurableSpace E
inst✝⁹ : BorelSpace E
inst✝⁸ : NormedAddCommGroup F₁
inst✝⁷ : NormedSpace ℂ F₁
inst✝⁶ : NormedAddCommGroup F₂
inst✝⁵ : NormedSpace ℂ F₂
inst✝⁴ : NormedAddCommGroup F₃
inst✝³ : NormedSpace ℂ F₃
inst✝² : CompleteSpace F₃
inst✝¹ : CompleteSpace F₁
inst✝ : CompleteSpace F₂
B : F₁ →L[ℂ] F₂ →L[ℂ] F₃
f : 𝓢(E, F₁)
g : 𝓢(E, F₂)
x✝ x : E
⊢ 𝐞 (-((-innerₗ E) x) x✝) • 𝓕 (⇑f ⋆[B, volume] ⇑g) x = 𝐞 (-((-innerₗ E) x) x✝) • 𝓕 (⇑f ⋆[B, volume] ⇑g) x

Tactic:
]

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

Goal state before:
pp: G : Type u_1
R : Type u_3
inst✝² : AddCommGroup G
inst✝¹ : RCLike R
ψ₁ ψ₂ : AddChar G R
inst✝ : Fintype G
⊢ ¬ψ₁ = ψ₂ ↔ ψ₁ ≠ ψ₂

Tactic:
]

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

Goal state before:
pp: G : Type u_1
R : Type u_3
inst✝² : AddCommGroup G
inst✝¹ : RCLike R
ψ₁ ψ₂ : AddChar G R
inst✝ : Fintype G
⊢ ψ₁ = ψ₂ ↔ ψ₁ = ψ₂

Tactic:
]

Goal state after:
Module: Mathlib.GroupTheory.FiniteAbelian.Basic

Goal state before:
pp: case of
ι : Type
inst✝ : DecidableEq ι
p n : ι → ℕ
i : { i // n i ≠ 0 }
x : ZMod (p ↑i ^ n ↑i)
⊢ (DirectSum.of (fun j ↦ ZMod (p ↑j ^ n ↑j)) ⟨↑i, ⋯⟩) x = (DirectSum.of (fun i ↦ ZMod (p ↑i ^ n ↑i)) i) x

Tactic:
]

Goal state after:
Module: Mathlib.GroupTheory.FiniteAbelian.Basic

Goal state before:
pp: case add
ι : Type
inst✝ : DecidableEq ι
p n : ι → ℕ
x y : ⨁ (i : { i // n i ≠ 0 }), ZMod (p ↑i ^ n ↑i)
hx :
  (DirectSum.toAddMonoid fun i ↦ if h : n i = 0 then 0 else DirectSum.of (fun j ↦ ZMod (p ↑j ^ n ↑j)) ⟨i, h⟩)
      ((directSumNeZeroMulHom p n) x) =
    x
hy :
  (DirectSum.toAddMonoid fun i ↦ if h : n i = 0 then 0 else DirectSum.of (fun j ↦ ZMod (p ↑j ^ n ↑j)) ⟨i, h⟩)
      ((directSumNeZeroMulHom p n) y) =
    y
⊢ x + y = x + y

Tactic:
]

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
x : E
⊢ (1 + ‖x‖ ^ 2) ^ (-(2 * s) / 2) = (1 + ‖x‖ ^ 2) ^ (-s)

Tactic:
]

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
x : E
⊢ (1 + ‖x‖ ^ 2) ^ (-(2 * s) / 2) = (1 + ‖x‖ ^ 2) ^ (-s)
Module: Mathlib.GroupTheory.FiniteAbelian.Basic

Goal state before:
pp: case zero
ι : Type
inst✝ : DecidableEq ι
p n : ι → ℕ
⊢ 0 = 0

Tactic:
]

Goal state after:
Module: Mathlib.GroupTheory.FiniteAbelian.Basic

Goal state before:
pp: case of
ι : Type
inst✝ : DecidableEq ι
p n : ι → ℕ
i : ι
x : ZMod (p i ^ n i)
⊢ (directSumNeZeroMulHom p n) ((if h : n i = 0 then 0 else DirectSum.of (fun j ↦ ZMod (p ↑j ^ n ↑j)) ⟨i, h⟩) x) =
    (DirectSum.of (fun i ↦ ZMod (p i ^ n i)) i) x

Tactic:
]

Goal state after:
case of
ι : Type
inst✝ : DecidableEq ι
p n : ι → ℕ
i : ι
x : ZMod (p i ^ n i)
⊢ (directSumNeZeroMulHom p n) ((if h : n i = 0 then 0 else DirectSum.of (fun j ↦ ZMod (p ↑j ^ n ↑j)) ⟨i, h⟩) x) =
    (DirectSum.of (fun i ↦ ZMod (p i ^ n i)) i) x
Module: Mathlib.GroupTheory.FiniteAbelian.Basic

Goal state before:
pp: ι : Type
inst✝ : DecidableEq ι
p n : ι → ℕ
i : ι
x : ZMod (p i ^ n i)
h : n i = 0
⊢ 1 = 1

Tactic:
]

Goal state after: