mathlib-initiative/mathlib-tactics huggingface dataset:
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
⊢ (A ⊙ B).PosSemidef

Tactic:
classical
  refine ⟨hA.isHermitian.hadamard hB.isHermitian, fun x ↦ ?_⟩
  have hAB : ((A ⊙ B).submatrix (↑) (↑) : Matrix x.support _ _).PosSemidef := by
    have hAs := hA.submatrix ((↑) : x.support → ι)
    have hBs := hB.submatrix ((↑) : x.support → ι)
    rw [submatrix_hadamard, posSemidef_iff_dotProduct_mulVec]
    refine ⟨hAs.isHermitian.hadamard hBs.isHermitian, fun y ↦ ?_⟩
    rw [star_dotProduct_hadamard_mulVec_eq_kronecker]
    exact (hAs.kronecker hBs).dotProduct_mulVec_nonneg _
  simpa [Finsupp.sum, ← Finset.sum_attach x.support, ← Finset.subtype_mem_eq_attach,
    ← Finsupp.subtypeDomain_apply, ← Finsupp.support_subtypeDomain] using hAB.2 _

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Abs

Goal state before:
pp: A : Type u_2
inst✝¹¹ : NonUnitalRing A
inst✝¹⁰ : StarRing A
inst✝⁹ : TopologicalSpace A
inst✝⁸ : Module ℝ A
inst✝⁷ : SMulCommClass ℝ A A
inst✝⁶ : IsScalarTower ℝ A A
inst✝⁵ : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝⁴ : PartialOrder A
inst✝³ : StarOrderedRing A
inst✝² : NonnegSpectrumClass ℝ A
inst✝¹ : IsTopologicalRing A
inst✝ : T2Space A
a b : A
h₁ : Commute a b
h₂ : Commute a (star b)
⊢ abs (a * b) = abs a * abs b

Tactic:
have hab := h₁.cfcAbs_cfcAbs h₂

Goal state after:
A : Type u_2
inst✝¹¹ : NonUnitalRing A
inst✝¹⁰ : StarRing A
inst✝⁹ : TopologicalSpace A
inst✝⁸ : Module ℝ A
inst✝⁷ : SMulCommClass ℝ A A
inst✝⁶ : IsScalarTower ℝ A A
inst✝⁵ : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝⁴ : PartialOrder A
inst✝³ : StarOrderedRing A
inst✝² : NonnegSpectrumClass ℝ A
inst✝¹ : IsTopologicalRing A
inst✝ : T2Space A
a b : A
h₁ : Commute a b
h₂ : Commute a (star b)
hab : Commute (abs a) (abs b)
⊢ abs (a * b) = abs a * abs b
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
F : Type u_5
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace 𝕜 F
v : n → E
f : E →L[𝕜] F
c : n →₀ 𝕜
⊢ 0 ≤
    ∑ x ∈ c.support,
      ∑ x_1 ∈ c.support, (star (c x) * ‖f‖ ^ 2 • gram 𝕜 v x x_1 * c x_1 - star (c x) * gram 𝕜 (⇑f ∘ v) x x_1 * c x_1)

Tactic:
Finset.sum_sub_distrib,

Goal state after:
E : Type u_1
n : Type u_2
𝕜 : Type u_4
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
F : Type u_5
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace 𝕜 F
v : n → E
f : E →L[𝕜] F
c : n →₀ 𝕜
⊢ 0 ≤
    ∑ x ∈ c.support, ∑ x_1 ∈ c.support, star (c x) * ‖f‖ ^ 2 • gram 𝕜 v x x_1 * c x_1 -
      ∑ x ∈ c.support, ∑ x_1 ∈ c.support, star (c x) * gram 𝕜 (⇑f ∘ v) x x_1 * c x_1
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Abs

Goal state before:
pp: case inl
𝕜 : Type u_1
A : Type u_2
p : A → Prop
inst✝¹⁶ : RCLike 𝕜
inst✝¹⁵ : NonUnitalRing A
inst✝¹⁴ : TopologicalSpace A
inst✝¹³ : Module 𝕜 A
inst✝¹² : StarRing A
inst✝¹¹ : PartialOrder A
inst✝¹⁰ : StarOrderedRing A
inst✝⁹ : IsScalarTower 𝕜 A A
inst✝⁸ : SMulCommClass 𝕜 A A
inst✝⁷ : NonUnitalContinuousFunctionalCalculus 𝕜 A p
inst✝⁶ : Module ℝ A
inst✝⁵ : SMulCommClass ℝ A A
inst✝⁴ : IsScalarTower ℝ A A
inst✝³ : NonnegSpectrumClass ℝ A
inst✝² : IsTopologicalRing A
inst✝¹ : T2Space A
inst✝ : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
f : 𝕜 → 𝕜
a : A
ha : p a
hf : ContinuousOn f ((fun z ↦ ↑‖z‖) '' quasispectrum 𝕜 a)
hf0 : f 0 = 0
⊢ cfcₙ f (cfcₙ (fun x ↦ ↑‖x‖) a) = cfcₙ f (abs a)

Tactic:
← abs_eq_cfcₙ_coe_norm _ a

Goal state after:
case inl
𝕜 : Type u_1
A : Type u_2
p : A → Prop
inst✝¹⁶ : RCLike 𝕜
inst✝¹⁵ : NonUnitalRing A
inst✝¹⁴ : TopologicalSpace A
inst✝¹³ : Module 𝕜 A
inst✝¹² : StarRing A
inst✝¹¹ : PartialOrder A
inst✝¹⁰ : StarOrderedRing A
inst✝⁹ : IsScalarTower 𝕜 A A
inst✝⁸ : SMulCommClass 𝕜 A A
inst✝⁷ : NonUnitalContinuousFunctionalCalculus 𝕜 A p
inst✝⁶ : Module ℝ A
inst✝⁵ : SMulCommClass ℝ A A
inst✝⁴ : IsScalarTower ℝ A A
inst✝³ : NonnegSpectrumClass ℝ A
inst✝² : IsTopologicalRing A
inst✝¹ : T2Space A
inst✝ : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
f : 𝕜 → 𝕜
a : A
ha : p a
hf : ContinuousOn f ((fun z ↦ ↑‖z‖) '' quasispectrum 𝕜 a)
hf0 : f 0 = 0
⊢ cfcₙ f (abs a) = cfcₙ f (abs a)
Module: Mathlib.MeasureTheory.Function.ContinuousMapDense

Goal state before:
pp: case pos
α : Type u_1
inst✝⁶ : TopologicalSpace α
inst✝⁵ : NormalSpace α
inst✝⁴ : MeasurableSpace α
inst✝³ : BorelSpace α
E : Type u_2
inst✝² : NormedAddCommGroup E
μ : Measure α
p : ℝ≥0∞
inst✝¹ : NormedSpace ℝ E
inst✝ : μ.OuterRegular
hp : p ≠ ∞
s u : Set α
s_closed : IsClosed[inst✝⁶] s
u_open : IsOpen[inst✝⁶] u
hsu : s ⊆ u
hs : μ s ≠ ∞
c : E
ε : ℝ≥0∞
hε : ε ≠ 0
η : ℝ≥0
η_pos : 0 < η
hη : ∀ (s : Set α), μ s ≤ ↑η → eLpNorm (s.indicator fun _x ↦ c) p μ ≤ ε
ηpos : 0 < ↑η
V : Set α
sV : V ⊇ s
V_open : IsOpen[inst✝⁶] V
h'V : μ V < ∞
hV : μ (V \ s) < ↑η
v : Set α := u ∩ V
hsv : s ⊆ v
hμv : μ v < ∞
g : C(α, ℝ)
hgv : EqOn (⇑g) 0 (u ∩ V)ᶜ
hgs : EqOn (⇑g) 1 s
hg_range : ∀ (x : α), g x ∈ Icc 0 1
g_norm : ∀ (x : α), ‖g x‖ = g x
gc_bd0 : ∀ (x : α), ‖g x • c‖ ≤ ‖c‖
x : α
hv : x ∈ v
⊢ ‖g x • c - s.indicator (fun _x ↦ c) x‖ ≤ ‖(v \ s).indicator (fun _x ↦ c) x‖

pp: case neg
α : Type u_1
inst✝⁶ : TopologicalSpace α
inst✝⁵ : NormalSpace α
inst✝⁴ : MeasurableSpace α
inst✝³ : BorelSpace α
E : Type u_2
inst✝² : NormedAddCommGroup E
μ : Measure α
p : ℝ≥0∞
inst✝¹ : NormedSpace ℝ E
inst✝ : μ.OuterRegular
hp : p ≠ ∞
s u : Set α
s_closed : IsClosed[inst✝⁶] s
u_open : IsOpen[inst✝⁶] u
hsu : s ⊆ u
hs : μ s ≠ ∞
c : E
ε : ℝ≥0∞
hε : ε ≠ 0
η : ℝ≥0
η_pos : 0 < η
hη : ∀ (s : Set α), μ s ≤ ↑η → eLpNorm (s.indicator fun _x ↦ c) p μ ≤ ε
ηpos : 0 < ↑η
V : Set α
sV : V ⊇ s
V_open : IsOpen[inst✝⁶] V
h'V : μ V < ∞
hV : μ (V \ s) < ↑η
v : Set α := u ∩ V
hsv : s ⊆ v
hμv : μ v < ∞
g : C(α, ℝ)
hgv : EqOn (⇑g) 0 (u ∩ V)ᶜ
hgs : EqOn (⇑g) 1 s
hg_range : ∀ (x : α), g x ∈ Icc 0 1
g_norm : ∀ (x : α), ‖g x‖ = g x
gc_bd0 : ∀ (x : α), ‖g x • c‖ ≤ ‖c‖
x : α
hv : x ∉ v
⊢ ‖g x • c - s.indicator (fun _x ↦ c) x‖ ≤ ‖(v \ s).indicator (fun _x ↦ c) x‖

Tactic:
· rw [← Set.sdiff_union_of_subset hsv] at hv
      rcases hv with hsv | hs
      · simpa only [hsv.2, Set.indicator_of_notMem, not_false_iff, sub_zero, hsv,
          Set.indicator_of_mem] using gc_bd0 x
      · simp [hgs hs, hs]

Goal state after:
case neg
α : Type u_1
inst✝⁶ : TopologicalSpace α
inst✝⁵ : NormalSpace α
inst✝⁴ : MeasurableSpace α
inst✝³ : BorelSpace α
E : Type u_2
inst✝² : NormedAddCommGroup E
μ : Measure α
p : ℝ≥0∞
inst✝¹ : NormedSpace ℝ E
inst✝ : μ.OuterRegular
hp : p ≠ ∞
s u : Set α
s_closed : IsClosed[inst✝⁶] s
u_open : IsOpen[inst✝⁶] u
hsu : s ⊆ u
hs : μ s ≠ ∞
c : E
ε : ℝ≥0∞
hε : ε ≠ 0
η : ℝ≥0
η_pos : 0 < η
hη : ∀ (s : Set α), μ s ≤ ↑η → eLpNorm (s.indicator fun _x ↦ c) p μ ≤ ε
ηpos : 0 < ↑η
V : Set α
sV : V ⊇ s
V_open : IsOpen[inst✝⁶] V
h'V : μ V < ∞
hV : μ (V \ s) < ↑η
v : Set α := u ∩ V
hsv : s ⊆ v
hμv : μ v < ∞
g : C(α, ℝ)
hgv : EqOn (⇑g) 0 (u ∩ V)ᶜ
hgs : EqOn (⇑g) 1 s
hg_range : ∀ (x : α), g x ∈ Icc 0 1
g_norm : ∀ (x : α), ‖g x‖ = g x
gc_bd0 : ∀ (x : α), ‖g x • c‖ ≤ ‖c‖
x : α
hv : x ∉ v
⊢ ‖g x • c - s.indicator (fun _x ↦ c) x‖ ≤ ‖(v \ s).indicator (fun _x ↦ c) x‖
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 y : X
⊢ (fun x ↦ x • D.e n) (coeff n (x + y)) = (fun x ↦ x • D.e n) (coeff n x + coeff n y)

Tactic:
simp only [add_smul, ← hcoeff, map_add]

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

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

Tactic:
Function.Periodic.lift_coe,

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

Goal state before:
pp: case H
T : ℝ
n : ℤ
z✝ : ℝ
⊢ ↑(⋯.lift ↑(-n • z✝)) = (starRingEnd ℂ) ↑(⋯.lift ↑(n • z✝))

Tactic:
Function.Periodic.lift_coe,

Goal state after:
case H
T : ℝ
n : ℤ
z✝ : ℝ
⊢ ↑(Circle.exp (2 * π / T * -n • z✝)) = (starRingEnd ℂ) ↑(Circle.exp (2 * π / T * n • z✝))
Module: Mathlib.Analysis.Fourier.AddCircle

Goal state before:
pp: T : ℝ
n : ℤ
hn : n ≠ 0
hT : 0 < T
x : AddCircle T
⊢ ↑(⋯.lift ↑(↑n * (T / 2 / ↑n))) = -1

Tactic:
Function.Periodic.lift_coe,

Goal state after:
T : ℝ
n : ℤ
hn : n ≠ 0
hT : 0 < T
x : AddCircle T
⊢ ↑(Circle.exp (2 * π / T * (↑n * (T / 2 / ↑n)))) = -1
Module: Mathlib.Analysis.Fourier.AddCircle

Goal state before:
pp: T : ℝ
hT : Fact (0 < T)
x y : AddCircle T
hxy : x ≠ y
⊢ ↑x.toCircle ≠ ↑y.toCircle

Tactic:
contrapose hxy

Goal state after:
T : ℝ
hT : Fact (0 < T)
x y : AddCircle T
hxy : ↑x.toCircle = ↑y.toCircle
⊢ x = y
Module: Mathlib.Analysis.Fourier.AddCircle

Goal state before:
pp: case e'_9
T : ℝ
hT : Fact (0 < T)
p : ℝ≥0∞
inst✝ : Fact (1 ≤ p)
hp : p ≠ ∞
e_3✝ : Complex.instSemiring = NormedField.toNormedCommRing.toSemiring
e_6✝ : Lp.instModule ≍ Lp.instModule
⊢ span ℂ (range (fourierLp p)) = span ℂ (⇑↑(toLp p haarAddCircle ℂ) '' range fourier)

Tactic:
unfold fourierLp

Goal state after:
case e'_9
T : ℝ
hT : Fact (0 < T)
p : ℝ≥0∞
inst✝ : Fact (1 ≤ p)
hp : p ≠ ∞
e_3✝ : Complex.instSemiring = NormedField.toNormedCommRing.toSemiring
e_6✝ : Lp.instModule ≍ Lp.instModule
⊢ span ℂ (range fun n ↦ (toLp p haarAddCircle ℂ) (fourier n)) = span ℂ (⇑↑(toLp p haarAddCircle ℂ) '' range fourier)
Module: Mathlib.Analysis.Fourier.FourierTransformDeriv

Goal state before:
pp: V : Type u_1
W : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : NormedSpace ℝ V
inst✝¹ : NormedAddCommGroup W
inst✝ : NormedSpace ℝ W
L : V →L[ℝ] W →L[ℝ] ℝ
v : V
w : W
⊢ HasFDerivAt (fun w ↦ ↑(𝐞 (-(L v) w))) ((-2 * ↑π * I * ↑(𝐞 (-(L v) w))) • ofRealCLM ∘SL L v) w

Tactic:
have ha : HasFDerivAt (fun w' : W ↦ L v w') (L v) w := ContinuousLinearMap.hasFDerivAt (L v)

Goal state after:
V : Type u_1
W : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : NormedSpace ℝ V
inst✝¹ : NormedAddCommGroup W
inst✝ : NormedSpace ℝ W
L : V →L[ℝ] W →L[ℝ] ℝ
v : V
w : W
ha : HasFDerivAt (fun w' ↦ (L v) w') (L v) w
⊢ HasFDerivAt (fun w ↦ ↑(𝐞 (-(L v) w))) ((-2 * ↑π * I * ↑(𝐞 (-(L v) w))) • ofRealCLM ∘SL L v) w
Module: Mathlib.Analysis.Fourier.FourierTransformDeriv

Goal state before:
pp: case e'_12
V : Type u_1
W : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : NormedSpace ℝ V
inst✝¹ : NormedAddCommGroup W
inst✝ : NormedSpace ℝ W
L : V →L[ℝ] W →L[ℝ] ℝ
v : V
w : W
ha : HasFDerivAt (fun w' ↦ (L v) w') (L v) w
e_8✝ : addCommGroup = instNormedAddCommGroup.toAddCommGroup
e_9✝ : NormedSpace.complexToReal.toModule ≍ instInnerProductSpaceRealComplex.toModule
⊢ (-2 * ↑π * I * ↑(𝐞 (-(L v) w))) • ofRealCLM ∘SL L v =
    ContinuousLinearMap.toSpanSingleton ℝ (2 * ↑π * I * ↑(𝐞 (-(L v) w))) ∘SL (-L v)

Tactic:
ext y

Goal state after:
case e'_12
V : Type u_1
W : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : NormedSpace ℝ V
inst✝¹ : NormedAddCommGroup W
inst✝ : NormedSpace ℝ W
L : V →L[ℝ] W →L[ℝ] ℝ
v : V
w : W
ha : HasFDerivAt (fun w' ↦ (L v) w') (L v) w
e_8✝ : addCommGroup = instNormedAddCommGroup.toAddCommGroup
e_9✝ : NormedSpace.complexToReal.toModule ≍ instInnerProductSpaceRealComplex.toModule
y : W
⊢ ((-2 * ↑π * I * ↑(𝐞 (-(L v) w))) • ofRealCLM ∘SL L v) y =
    (ContinuousLinearMap.toSpanSingleton ℝ (2 * ↑π * I * ↑(𝐞 (-(L v) w))) ∘SL (-L v)) y
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
v : V
w : W
⊢ HasFDerivAt (fun w' ↦ 𝐞 (-(L v) w') • f v) (𝐞 (-(L v) w) • fourierSMulRight L f v) w

Tactic:
have ha : HasFDerivAt (fun w' : W ↦ L v w') (L v) w := ContinuousLinearMap.hasFDerivAt (L v)

Goal state after:
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℂ E
V : Type u_2
W : Type u_3
inst✝³ : NormedAddCommGroup V
inst✝² : NormedSpace ℝ V
inst✝¹ : NormedAddCommGroup W
inst✝ : NormedSpace ℝ W
L : V →L[ℝ] W →L[ℝ] ℝ
f : V → E
v : V
w : W
ha : HasFDerivAt (fun w' ↦ (L v) w') (L v) w
⊢ HasFDerivAt (fun w' ↦ 𝐞 (-(L v) w') • f v) (𝐞 (-(L v) w) • fourierSMulRight L f v) w
Module: Mathlib.Analysis.Distribution.SchwartzSpace.Basic

Goal state before:
pp: case hbc
ι : Type u_1
𝕜 : Type u_2
𝕜' : Type u_3
D : Type u_4
E : Type u_5
F : Type u_6
G : Type u_7
H : Type u_8
V : Type u_9
inst✝¹² : NormedAddCommGroup E
inst✝¹¹ : NormedSpace ℝ E
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NormedSpace ℝ F
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NormedAlgebra ℝ 𝕜
inst✝⁶ : NormedAddCommGroup D
inst✝⁵ : NormedSpace ℝ D
inst✝⁴ : NormedAddCommGroup G
inst✝³ : NormedSpace ℝ G
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedSpace 𝕜 E
inst✝ : NormedSpace 𝕜 G
B : E →L[𝕜] F →L[𝕜] G
g : D → F
hg : Function.HasTemperateGrowth g
k n l : ℕ
C : ℝ
hC : 0 ≤ C
f : 𝓢(D, E)
x : D
hxk : 0 ≤ ‖x‖ ^ k
hnorm_mul :
  ‖iteratedFDeriv ℝ n (fun y ↦ ((ContinuousLinearMap.bilinearRestrictScalars ℝ B) (f y)) (g y)) x‖ ≤
    ‖ContinuousLinearMap.bilinearRestrictScalars ℝ B‖ *
      ∑ i ∈ Finset.range (n + 1), ↑(n.choose i) * ‖iteratedFDeriv ℝ i (⇑f) x‖ * ‖iteratedFDeriv ℝ (n - i) g x‖
this : ∑ _x ∈ Finset.range (n + 1), 1 = ↑n + 1
i : ℕ
hgrowth : ‖iteratedFDeriv ℝ (n - i) g x‖ ≤ C * (1 + ‖x‖) ^ l
hi : i ∈ Finset.range (n + 1)
⊢ ‖x‖ ^ k * ‖iteratedFDeriv ℝ i (⇑f) x‖ * (1 + ‖x‖) ^ l ≤
    2 ^ (l + k) * ((Finset.Iic (l + k, n)).sup (schwartzSeminormFamily 𝕜 D E)) f

Tactic:
Finset.mem_range_succ_iff

Goal state after:
case hbc
ι : Type u_1
𝕜 : Type u_2
𝕜' : Type u_3
D : Type u_4
E : Type u_5
F : Type u_6
G : Type u_7
H : Type u_8
V : Type u_9
inst✝¹² : NormedAddCommGroup E
inst✝¹¹ : NormedSpace ℝ E
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NormedSpace ℝ F
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NormedAlgebra ℝ 𝕜
inst✝⁶ : NormedAddCommGroup D
inst✝⁵ : NormedSpace ℝ D
inst✝⁴ : NormedAddCommGroup G
inst✝³ : NormedSpace ℝ G
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedSpace 𝕜 E
inst✝ : NormedSpace 𝕜 G
B : E →L[𝕜] F →L[𝕜] G
g : D → F
hg : Function.HasTemperateGrowth g
k n l : ℕ
C : ℝ
hC : 0 ≤ C
f : 𝓢(D, E)
x : D
hxk : 0 ≤ ‖x‖ ^ k
hnorm_mul :
  ‖iteratedFDeriv ℝ n (fun y ↦ ((ContinuousLinearMap.bilinearRestrictScalars ℝ B) (f y)) (g y)) x‖ ≤
    ‖ContinuousLinearMap.bilinearRestrictScalars ℝ B‖ *
      ∑ i ∈ Finset.range (n + 1), ↑(n.choose i) * ‖iteratedFDeriv ℝ i (⇑f) x‖ * ‖iteratedFDeriv ℝ (n - i) g x‖
this : ∑ _x ∈ Finset.range (n + 1), 1 = ↑n + 1
i : ℕ
hgrowth : ‖iteratedFDeriv ℝ (n - i) g x‖ ≤ C * (1 + ‖x‖) ^ l
hi : i ≤ n
⊢ ‖x‖ ^ k * ‖iteratedFDeriv ℝ i (⇑f) x‖ * (1 + ‖x‖) ^ l ≤
    2 ^ (l + k) * ((Finset.Iic (l + k, n)).sup (schwartzSeminormFamily 𝕜 D E)) f
Module: Mathlib.Analysis.Distribution.SchwartzSpace.Basic

Goal state before:
pp: 𝕜 : Type u_2
E : Type u_5
F : Type u_6
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAlgebra ℝ 𝕜
inst✝ : NormedSpace 𝕜 F
g : E → 𝕜
f : 𝓢(E, F)
⊢ tsupport ⇑((smulLeftCLM F g) f) ⊆ tsupport ⇑f ∩ tsupport g

Tactic:
by_cases hg : g.HasTemperateGrowth

Goal state after:
case pos
𝕜 : Type u_2
E : Type u_5
F : Type u_6
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAlgebra ℝ 𝕜
inst✝ : NormedSpace 𝕜 F
g : E → 𝕜
f : 𝓢(E, F)
hg : Function.HasTemperateGrowth g
⊢ tsupport ⇑((smulLeftCLM F g) f) ⊆ tsupport ⇑f ∩ tsupport g

case neg
𝕜 : Type u_2
E : Type u_5
F : Type u_6
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAlgebra ℝ 𝕜
inst✝ : NormedSpace 𝕜 F
g : E → 𝕜
f : 𝓢(E, F)
hg : ¬Function.HasTemperateGrowth g
⊢ tsupport ⇑((smulLeftCLM F g) f) ⊆ tsupport ⇑f ∩ tsupport g
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
inst✝¹⁰ : TopologicalSpace α
inst✝⁹ : SecondCountableTopology α
inst✝⁸ : MeasurableSpace α
μ : Measure α
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : AddCommGroup α
inst✝⁵ : LinearOrder α
inst✝⁴ : IsOrderedAddMonoid α
inst✝³ : CompactIccSpace α
inst✝² : atTop.IsMeasurablyGenerated
inst✝¹ : MeasurableNeg α
inst✝ : μ.IsNegInvariant
hf : LocallyIntegrable f μ
hsymm : norm ∘ f =ᵐ[μ] norm ∘ f ∘ Neg.neg
ho : f =O[atTop] g
hg : IntegrableAtFilter g atTop μ
h_int : IntegrableOn f (Ici 0) μ
⊢ IntegrableOn f univ μ

Tactic:
← Iic_union_Ici_of_le le_rfl,

Goal state after:
α : Type u_1
E : Type u_2
F : Type u_3
inst✝¹¹ : NormedAddCommGroup E
f : α → E
g : α → F
inst✝¹⁰ : TopologicalSpace α
inst✝⁹ : SecondCountableTopology α
inst✝⁸ : MeasurableSpace α
μ : Measure α
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : AddCommGroup α
inst✝⁵ : LinearOrder α
inst✝⁴ : IsOrderedAddMonoid α
inst✝³ : CompactIccSpace α
inst✝² : atTop.IsMeasurablyGenerated
inst✝¹ : MeasurableNeg α
inst✝ : μ.IsNegInvariant
hf : LocallyIntegrable f μ
hsymm : norm ∘ f =ᵐ[μ] norm ∘ f ∘ Neg.neg
ho : f =O[atTop] g
hg : IntegrableAtFilter g atTop μ
h_int : IntegrableOn f (Ici 0) μ
⊢ IntegrableOn f (Iic ?m.106 ∪ Ici ?m.106) μ

α : Type u_1
E : Type u_2
F : Type u_3
inst✝¹¹ : NormedAddCommGroup E
f : α → E
g : α → F
inst✝¹⁰ : TopologicalSpace α
inst✝⁹ : SecondCountableTopology α
inst✝⁸ : MeasurableSpace α
μ : Measure α
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : AddCommGroup α
inst✝⁵ : LinearOrder α
inst✝⁴ : IsOrderedAddMonoid α
inst✝³ : CompactIccSpace α
inst✝² : atTop.IsMeasurablyGenerated
inst✝¹ : MeasurableNeg α
inst✝ : μ.IsNegInvariant
hf : LocallyIntegrable f μ
hsymm : norm ∘ f =ᵐ[μ] norm ∘ f ∘ Neg.neg
ho : f =O[atTop] g
hg : IntegrableAtFilter g atTop μ
h_int : IntegrableOn f (Ici 0) μ
⊢ α
Module: Mathlib.Analysis.Fourier.FourierTransform

Goal state before:
pp: V : Type u_1
E : Type u_3
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℂ E
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MeasurableSpace V
inst✝¹ : BorelSpace V
inst✝ : FiniteDimensional ℝ V
f : V → E
⊢ 𝓕⁻ f = 𝓕 fun x ↦ f (-x)

Tactic:
ext y

Goal state after:
V : Type u_1
E : Type u_3
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℂ E
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MeasurableSpace V
inst✝¹ : BorelSpace V
inst✝ : FiniteDimensional ℝ V
f : V → E
y : V
⊢ 𝓕⁻ f y = 𝓕 (fun x ↦ f (-x)) y
Module: Mathlib.Analysis.SpecialFunctions.PolarCoord

Goal state before:
pp: ⊢ ∀ ⦃x : ℝ × ℝ⦄,
    x ∈ {q | 0 < q.1} ∪ {q | q.2 ≠ 0} → (√(x.1 ^ 2 + x.2 ^ 2), (Complex.equivRealProd.symm x).arg) ∈ Ioi 0 ×ˢ Ioo (-π) π

Tactic:
rintro ⟨x, y⟩ hxy
    simp only [prodMk_mem_set_prod_eq, mem_Ioi, sqrt_pos, mem_Ioo, Complex.neg_pi_lt_arg,
      true_and, Complex.arg_lt_pi_iff]
    constructor
    · rcases hxy with hxy | hxy
      · dsimp at hxy; linarith [sq_pos_of_ne_zero hxy.ne', sq_nonneg y]
      · linarith [sq_nonneg x, sq_pos_of_ne_zero hxy]
    · rcases hxy with hxy | hxy
      · exact Or.inl (le_of_lt hxy)
      · exact Or.inr hxy

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

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℂ → E
⊢ ∫ (p : ℝ × ℝ) in polarCoord.target, p.1 • f (↑Complex.polarCoord.symm p) =
    ∫ (p : ℝ × ℝ) in polarCoord.target, p.1 • f (measurableEquivRealProd.symm (↑polarCoord.symm p))

Tactic:
measurableEquivRealProd_symm_polarCoord_symm_apply

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

Goal state before:
pp: f : ℂ → ℝ≥0∞
⊢ ∫⁻ (p : ℝ × ℝ) in polarCoord.target, ENNReal.ofReal p.1 • f (↑Complex.polarCoord.symm p) =
    ∫⁻ (p : ℝ × ℝ) in polarCoord.target, ENNReal.ofReal p.1 • f (measurableEquivRealProd.symm (↑polarCoord.symm p))

Tactic:
measurableEquivRealProd_symm_polarCoord_symm_apply

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

Goal state before:
pp: case e'_3
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
this : Integrable (fun w ↦ 𝐞 ⟪w, v⟫ • 𝓕 f w) volume
c : ℝ
w : V
⊢ cexp (-↑c⁻¹ * ↑‖w‖ ^ 2 + 2 * ↑π * I * ↑⟪v, w⟫) • 𝓕 f w = cexp (-↑c⁻¹ * ↑‖w‖ ^ 2) • 𝐞 ⟪w, v⟫ • 𝓕 f w

Tactic:
rw [Submonoid.smul_def, Real.fourierChar_apply, smul_smul, ← Complex.exp_add, real_inner_comm]

Goal state after:
case e'_3
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
this : Integrable (fun w ↦ 𝐞 ⟪w, v⟫ • 𝓕 f w) volume
c : ℝ
w : V
⊢ cexp (-↑c⁻¹ * ↑‖w‖ ^ 2 + 2 * ↑π * I * ↑⟪w, v⟫) • 𝓕 f w = cexp (-↑c⁻¹ * ↑‖w‖ ^ 2 + ↑(2 * π * ⟪w, v⟫) * I) • 𝓕 f w
Module: Mathlib.Analysis.Distribution.Support

Goal state before:
pp: E : Type u_5
F : Type u_6
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ E
inst✝ : NormedSpace ℂ F
f : 𝓢'(E, F)
s : Set E
hf : IsVanishingOn (⇑f) s
g : E → ℂ
hg : Function.HasTemperateGrowth g
u : 𝓢(E, ℂ)
hu : tsupport ⇑u ⊆ s
⊢ tsupport ⇑((SchwartzMap.smulLeftCLM ℂ g) u) ⊆ s

Tactic:
rw [SchwartzMap.smulLeftCLM_apply hg]

Goal state after:
E : Type u_5
F : Type u_6
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ E
inst✝ : NormedSpace ℂ F
f : 𝓢'(E, F)
s : Set E
hf : IsVanishingOn (⇑f) s
g : E → ℂ
hg : Function.HasTemperateGrowth g
u : 𝓢(E, ℂ)
hu : tsupport ⇑u ⊆ s
⊢ (tsupport fun x ↦ g x • u x) ⊆ s
Module: Mathlib.Analysis.Distribution.Sobolev

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

Tactic:
ext f

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✝ : NormedSpace ℂ F
f : 𝓢'(E, F)
x✝ : 𝓢(E, ℂ)
⊢ ((besselPotential E F 0) f) x✝ = ((ContinuousLinearMap.id ℂ 𝓢'(E, F)) f) x✝
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
t : Set E := s ∩ ↑Ω
⊢ ∃ u, tsupport ⇑u ⊆ s ∧ (delta x) u ≠ 0

Tactic:
have ht : IsOpen t := hs.inter Ω.isOpen

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 ∩ ↑Ω
ht : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t
⊢ ∃ u, tsupport ⇑u ⊆ s ∧ (delta x) u ≠ 0