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
i j : Fin n
⊢ (if i = j then ↑(hT.eigenvalues hn j) else 0) = if i = j then ↑(hT.eigenvalues hn i) else 0

Tactic:
grind

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

Goal state before:
pp: case pos
𝕜 : 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)
h✝ : k + 1 ≤ n
⊢ ⇑({ toFun := fun f ↦ ContDiffMapSupportedIn.of_support_subset ⋯ ⋯, map_add' := ⋯, map_smul' := ⋯ } f) = fderiv ℝ ⇑f

Tactic:
rfl

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

Goal state before:
pp: case neg
𝕜 : 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)
h✝ : ¬k + 1 ≤ n
⊢ ⇑({ toFun := fun f ↦ 0, map_add' := ⋯, map_smul' := ⋯ } f) = 0

Tactic:
rfl

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : RCLike 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
μ : ℝ
T : E →ₗ[𝕜] E
hμ : HasEigenvalue T ↑μ
hnn : ∀ (x : E), 0 ≤ RCLike.re ⟪x, T x⟫
v : E
hv₂ : v ≠ 0
hpos : 0 < ‖v‖ ^ 2
hv₁ : T v = ↑μ • v
⊢ 0 ≤ μ

Tactic:
have : RCLike.re ⟪v, T v⟫ = μ * ‖v‖ ^ 2 :=
    mod_cast congr_arg RCLike.re (inner_product_apply_eigenvector hv₁)

Goal state after:
𝕜 : Type u_1
inst✝² : RCLike 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
μ : ℝ
T : E →ₗ[𝕜] E
hμ : HasEigenvalue T ↑μ
hnn : ∀ (x : E), 0 ≤ RCLike.re ⟪x, T x⟫
v : E
hv₂ : v ≠ 0
hpos : 0 < ‖v‖ ^ 2
hv₁ : T v = ↑μ • v
this : RCLike.re ⟪v, T v⟫ = μ * ‖v‖ ^ 2
⊢ 0 ≤ μ
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
hμ : HasEigenvalue T ↑μ
hnn : ∀ (x : E), 0 < RCLike.re ⟪x, T x⟫
v : E
hv₂ : v ≠ 0
hpos : 0 < ‖v‖ ^ 2
hv₁ : T v = ↑μ • v
⊢ 0 < μ

Tactic:
have : RCLike.re ⟪v, T v⟫ = μ * ‖v‖ ^ 2 :=
    mod_cast congr_arg RCLike.re (inner_product_apply_eigenvector hv₁)

Goal state after:
𝕜 : Type u_1
inst✝² : RCLike 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
μ : ℝ
T : E →ₗ[𝕜] E
hμ : HasEigenvalue T ↑μ
hnn : ∀ (x : E), 0 < RCLike.re ⟪x, T x⟫
v : E
hv₂ : v ≠ 0
hpos : 0 < ‖v‖ ^ 2
hv₁ : T v = ↑μ • v
this : RCLike.re ⟪v, T v⟫ = μ * ‖v‖ ^ 2
⊢ 0 < μ
Module: Mathlib.Analysis.Distribution.ContDiffMapSupportedIn

Goal state before:
pp: case pos
𝕜 : 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)
h✝ : k + ↑i ≤ n
⊢ ⇑({ toFun := fun f ↦ ContDiffMapSupportedIn.of_support_subset ⋯ ⋯, map_add' := ⋯, map_smul' := ⋯ } f) =
    iteratedFDeriv ℝ i ⇑f

Tactic:
rfl

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

Goal state before:
pp: case neg
𝕜 : 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)
h✝ : ¬k + ↑i ≤ n
⊢ ⇑({ toFun := fun f ↦ 0, map_add' := ⋯, map_smul' := ⋯ } f) = 0

Tactic:
rfl

Goal state after:
Module: Mathlib.Analysis.Matrix.Order

Goal state before:
pp: 𝕜 : Type u_1
n : Type u_2
inst✝ : RCLike 𝕜
A : Matrix n n 𝕜
h₁ : A.PosSemidef
h₂ : (-A).PosSemidef
⊢ A = 0

Tactic:
by
  classical
  ext i j
  have hdiag i : A i i = 0 :=
    le_antisymm (by simpa using h₂.diag_nonneg) (by simpa using h₁.diag_nonneg)
  have h1 := h₁.2 (.single i 1 + .single j (A j i))
  have h2 := h₂.2 (.single i 1 + .single j (A j i))
  simp [Finsupp.sum_add_index, mul_add, add_mul,
      -neg_add_rev, hdiag, ← h₁.1.apply j i, -RCLike.star_def] at *
  simpa using le_antisymm h2 h1

Goal state after:
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 : Compacts E
⊢ ⨅ i, comap (eval i ∘ ⇑(ContinuousLinearMap.pi (structureMapCLM 𝕜 n))) PseudoMetricSpace.toUniformSpace =
    ⨅ i, comap (⇑(structureMapLM ℝ n i)) inferInstance

Tactic:
rfl

Goal state after:
Module: Mathlib.Analysis.Matrix.Order

Goal state before:
pp: 𝕜 : Type u_1
n : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n 𝕜
hA : A.PosSemidef
⊢ ↑(∏ i, √(max (⋯.eigenvalues i) 0)) = ↑(∏ i, √(⋯.eigenvalues i))

Tactic:
grind

Goal state after:
Module: Mathlib.Analysis.Matrix.Order

Goal state before:
pp: 𝕜 : Type u_1
inst✝ : RCLike 𝕜
ι : Type u_3
A B : Matrix ι ι 𝕜
hA : A.PosDef
hB : B.PosDef
⊢ (A ⊙ B).PosDef

Tactic:
refine ⟨hA.isHermitian.hadamard hB.isHermitian, fun x hx ↦ ?_⟩
  have hAB : ((A ⊙ B).submatrix (↑) (↑) : Matrix x.support _ _).PosDef := by
    have hAs : (A.submatrix (↑) (↑) : Matrix x.support _ _).PosDef :=
      hA.submatrix Subtype.coe_injective
    have hBs : (B.submatrix (↑) (↑) : Matrix x.support _ _).PosDef :=
      hB.submatrix Subtype.coe_injective
    rw [submatrix_hadamard, posDef_iff_dotProduct_mulVec]
    refine ⟨hAs.isHermitian.hadamard hBs.isHermitian, fun y hy ↦ ?_⟩
    rw [star_dotProduct_hadamard_mulVec_eq_kronecker]
    exact (hAs.kronecker hBs).dotProduct_mulVec_pos <| by simpa
  simp_rw [RCLike.star_def, hadamard_apply, Finsupp.sum,
    ← Finset.sum_attach x.support, ← Finset.subtype_mem_eq_attach,
    ← Finsupp.subtypeDomain_apply, ← Finsupp.support_subtypeDomain]
  refine hAB.2 ?_
  simpa [← Finsupp.support_nonempty_iff] using Finsupp.support_nonempty_iff.mpr hx

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

Goal state before:
pp: case h1
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 →₀ 𝕜
⊢ ∑ y ∈ c.support, ∑ x ∈ c.support, (starRingEnd 𝕜) (c x) * ⟪f (v x), f (v y)⟫_𝕜 * c y =
    ∑ x ∈ c.support, ∑ i ∈ c.support, c x * ((starRingEnd 𝕜) (c i) * ⟪f (v i), f (v x)⟫_𝕜)

Tactic:
grind

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

Goal state before:
pp: case h2
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 →₀ 𝕜
⊢ ∑ x ∈ c.support, ∑ x_1 ∈ c.support, (algebraMap ℝ 𝕜) ‖f‖ ^ 2 * (c x * ((starRingEnd 𝕜) (c x_1) * ⟪v x_1, v x⟫_𝕜)) =
    ∑ x ∈ c.support, ∑ x_1 ∈ c.support, (starRingEnd 𝕜) (c x_1) * ((algebraMap ℝ 𝕜) ‖f‖ ^ 2 * ⟪v x_1, v x⟫_𝕜) * c x

Tactic:
grind

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

Goal state before:
pp: A : Type u_2
inst✝⁹ : NonUnitalNormedRing A
inst✝⁸ : StarRing A
inst✝⁷ : CStarRing A
inst✝⁶ : NormedSpace ℝ A
inst✝⁵ : SMulCommClass ℝ A A
inst✝⁴ : IsScalarTower ℝ A A
inst✝³ : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝² : PartialOrder A
inst✝¹ : StarOrderedRing A
inst✝ : NonnegSpectrumClass ℝ A
a : A
⊢ ‖abs a * abs a‖ = ‖a‖ * ‖a‖

Tactic:
CFC.abs_mul_abs,

Goal state after:
A : Type u_2
inst✝⁹ : NonUnitalNormedRing A
inst✝⁸ : StarRing A
inst✝⁷ : CStarRing A
inst✝⁶ : NormedSpace ℝ A
inst✝⁵ : SMulCommClass ℝ A A
inst✝⁴ : IsScalarTower ℝ A A
inst✝³ : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝² : PartialOrder A
inst✝¹ : StarOrderedRing A
inst✝ : NonnegSpectrumClass ℝ A
a : A
⊢ ‖star a * a‖ = ‖a‖ * ‖a‖
Module: Mathlib.Analysis.Distribution.ContDiffMapSupportedIn

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝¹³ : NontriviallyNormedField 𝕜
inst✝¹² : NormedAddCommGroup E
inst✝¹¹ : NormedSpace ℝ E
n : ℕ∞
K : Compacts E
m : MeasurableSpace E
inst✝¹⁰ : OpensMeasurableSpace E
F₁ : Type u_5
F₂ : Type u_6
F₃ : Type u_7
inst✝⁹ : NormedAddCommGroup F₁
inst✝⁸ : NormedSpace 𝕜 F₁
inst✝⁷ : NormedSpace ℝ F₁
inst✝⁶ : NormedAddCommGroup F₂
inst✝⁵ : NormedSpace 𝕜 F₂
inst✝⁴ : NormedAddCommGroup F₃
inst✝³ : NormedSpace 𝕜 F₃
inst✝² : SMulCommClass ℝ 𝕜 F₁
inst✝¹ : NormedSpace ℝ F₃
inst✝ : SMulCommClass ℝ 𝕜 F₃
B : F₁ →L[𝕜] F₂ →L[𝕜] F₃
μ : Measure E
φ : E → F₂
f : 𝓓^{n}_{K}(E, F₁)
⊢ (integralAgainstBilinLM B μ φ) f = if IntegrableOn φ (↑K) μ then ∫ (x : E), (B (f x)) (φ x) ∂μ else 0

Tactic:
rfl

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

Goal state before:
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:
· simp [hgv hv, show x ∉ s from fun h => hv (hsv h)]

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

Goal state before:
pp: case e'_3
α : 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✝² : R1Space α
inst✝¹ : WeaklyLocallyCompactSpace α
inst✝ : μ.Regular
hp : p ≠ ∞
f✝ : α → E
hf : MemLp f✝ p μ
ε✝ : ℝ≥0∞
hε✝ : ε✝ ≠ 0
c : E
t : Set α
ht : MeasurableSet t
htμ : μ t < ∞
ε : ℝ≥0∞
hε : ε ≠ 0
δ : ℝ≥0∞
δpos : 0 < δ
hδ :
  ∀ (f g : α → E),
    AEStronglyMeasurable f μ →
      AEStronglyMeasurable g μ → eLpNorm f p μ ≤ δ → eLpNorm g p μ ≤ δ → eLpNorm (f + g) p μ < ε
η : ℝ≥0
ηpos : 0 < η
hη : ∀ (s : Set α), μ s ≤ ↑η → eLpNorm (s.indicator fun _x ↦ c) p μ ≤ δ
hη_pos' : 0 < ↑η
s : Set α
st : s ⊆ t
s_compact : IsCompact s
s_closed : IsClosed[inst✝⁸] s
μs : μ (t \ s) < ↑η
hsμ : μ s < ∞
I1 : eLpNorm ((s.indicator fun _y ↦ c) - t.indicator fun _y ↦ c) p μ ≤ δ
k : Set α
k_compact : IsCompact k
sk : s ⊆ interior k
f : α → E
f_cont : Continuous[inst✝⁸, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
I2 : eLpNorm (fun x ↦ f x - s.indicator (fun _y ↦ c) x) p μ ≤ δ
_f_bound : ∀ (x : α), ‖f x‖ ≤ ‖c‖
f_support : Function.support f ⊆ interior k
f_mem : MemLp f p μ
⊢ (f - t.indicator fun _y ↦ c) = (f - s.indicator fun x ↦ c) + ((s.indicator fun x ↦ c) - t.indicator fun x ↦ c)

Tactic:
simp only [sub_add_sub_cancel]

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

Goal state before:
pp: E : Type u_5
F : Type u_8
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : InnerProductSpace ℝ E
inst✝ : FiniteDimensional ℝ E
f : 𝓢(E, F)
x : E
⊢ (∑ i, ∂_{(stdOrthonormalBasis ℝ E) i} (∂_{(stdOrthonormalBasis ℝ E) i} f)) x = Δ (⇑f) x

Tactic:
simp [InnerProductSpace.laplacian_eq_iteratedFDeriv_orthonormalBasis f (stdOrthonormalBasis ℝ E),
    sum_apply, ← iteratedLineDerivOp_eq_iteratedFDeriv, iteratedLineDerivOp_succ_left]

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

Goal state before:
pp: case e'_3
α : 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✝ : μ.WeaklyRegular
hp : p ≠ ∞
f✝ : α → E
hf : MemLp f✝ p μ
ε✝ : ℝ≥0∞
hε✝ : ε✝ ≠ 0
c : E
t : Set α
ht : MeasurableSet t
htμ : μ t < ∞
ε : ℝ≥0∞
hε : ε ≠ 0
δ : ℝ≥0∞
δpos : 0 < δ
hδ :
  ∀ (f g : α → E),
    AEStronglyMeasurable f μ →
      AEStronglyMeasurable g μ → eLpNorm f p μ ≤ δ → eLpNorm g p μ ≤ δ → eLpNorm (f + g) p μ < ε
η : ℝ≥0
ηpos : 0 < η
hη : ∀ (s : Set α), μ s ≤ ↑η → eLpNorm (s.indicator fun _x ↦ c) p μ ≤ δ
hη_pos' : 0 < ↑η
s : Set α
st : s ⊆ t
s_closed : IsClosed[inst✝⁶] s
μs : μ (t \ s) < ↑η
hsμ : μ s < ∞
I1 : eLpNorm ((s.indicator fun _y ↦ c) - t.indicator fun _y ↦ c) p μ ≤ δ
f : α → E
f_cont : Continuous[inst✝⁶, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
I2 : eLpNorm (fun x ↦ f x - s.indicator (fun _y ↦ c) x) p μ ≤ δ
f_bound : ∀ (x : α), ‖f x‖ ≤ ‖c‖
f_mem : MemLp f p μ
⊢ (f - t.indicator fun _y ↦ c) = (f - s.indicator fun x ↦ c) + ((s.indicator fun x ↦ c) - t.indicator fun x ↦ c)

Tactic:
simp only [sub_add_sub_cancel]

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

Goal state before:
pp: T : ℝ
hT : Fact (0 < T)
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : AddCircle T → E
n : ℤ
a x : ℝ
⊢ (fourier (-n)) ↑x • f ↑x = (fun z ↦ (fourier (-n)) z • f z) ↑x

Tactic:
rfl

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
b : HilbertBasis ι 𝕜 E
i j : ι
⊢ ⟪1, ↑(lp.single 2 j 1) i⟫ = if i = j then 1 else 0

Tactic:
lp.single_apply,

Goal state after:
ι : Type u_1
𝕜 : Type u_2
inst✝² : RCLike 𝕜
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
b : HilbertBasis ι 𝕜 E
i j : ι
⊢ ⟪1, Pi.single j 1 i⟫ = if i = j then 1 else 0
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 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)
u : Set α
u_open : IsOpen[inst✝³] u
x₀u : x₀ ∈ u
hu : u ∩ s ⊆ t ∩ g ⁻¹' ball a 1
⊢ ∃ u, IsOpen[inst✝³] u ∧ x₀ ∈ u ∧ s ∩ u ⊆ t ∧ ∀ x ∈ u ∩ s, g x ∈ ball a 1

Tactic:
refine ⟨u, u_open, x₀u, ?_, hu.trans inter_subset_right⟩

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 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)
u : Set α
u_open : IsOpen[inst✝³] u
x₀u : x₀ ∈ u
hu : u ∩ s ⊆ t ∩ g ⁻¹' ball a 1
⊢ s ∩ u ⊆ t
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
hu : u ∩ s ⊆ t ∩ g ⁻¹' ball 0 δ
⊢ ∃ u, IsOpen[inst✝³] u ∧ x₀ ∈ u ∧ s ∩ u ⊆ t ∧ ∀ x ∈ u ∩ s, g x ∈ ball 0 δ

Tactic:
refine ⟨u, u_open, x₀u, ?_, hu.trans inter_subset_right⟩

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
hu : u ∩ s ⊆ t ∩ g ⁻¹' ball 0 δ
⊢ s ∩ u ⊆ t
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✝² : NormedField 𝕜
inst✝¹ : NormedSpace 𝕜 F
inst✝ : SMulCommClass ℝ 𝕜 F
k n : ℕ
f : 𝓢(E, F)
⊢ (SchwartzMap.seminorm 𝕜 k n) f = sInf {c | 0 ≤ c ∧ ∀ (x : E), ‖x‖ ^ k * ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤ c}

Tactic:
rfl

Goal state after:
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✝² : NormedField 𝕜
inst✝¹ : NormedSpace 𝕜 F
inst✝ : SMulCommClass ℝ 𝕜 F
m : ℕ × ℕ
k n : ℕ
hk : k ≤ m.1
hn : n ≤ m.2
f : 𝓢(E, F)
x : E
⊢ Finset.range (k + 1) ⊆ Finset.range (m.1 + 1)

Tactic:
grind

Goal state after:
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✝² : NormedField 𝕜
inst✝¹ : NormedSpace 𝕜 F
inst✝ : SMulCommClass ℝ 𝕜 F
A : nhds 0 = ⨅ i, Filter.comap (⇑(schwartzSeminormFamily ℝ E F i)) (nhds 0)
⊢ ⨅ i, Filter.comap (⇑(schwartzSeminormFamily ℝ E F i)) (nhds 0) =
    ⨅ i, Filter.comap (⇑(schwartzSeminormFamily 𝕜 E F i)) (nhds 0)

Tactic:
rfl

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

Goal state before:
pp: 𝕜 : Type u_2
D : Type u_4
V : Type u_9
inst✝⁸ : RCLike 𝕜
inst✝⁷ : NormedAddCommGroup D
inst✝⁶ : NormedSpace ℝ D
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : NormedSpace ℝ V
inst✝³ : NormedSpace 𝕜 V
inst✝² : MeasurableSpace D
μ : Measure D
hμ : μ.HasTemperateGrowth
inst✝¹ : BorelSpace D
inst✝ : SecondCountableTopology D
f : 𝓢(D, V)
⊢ (integralCLM 𝕜 μ) f = ∫ (x : D), f x ∂μ

Tactic:
rfl

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Lebesgue.Integral

Goal state before:
pp: α : Type u_1
inst✝¹ : MeasurableSpace α
μ : Measure α
f g : α → ℝ
s : Set α
inst✝ : SigmaFinite μ
f_int : IntegrableOn f s μ
g_int : IntegrableOn g s μ
hs : MeasurableSet s
hfg : f ≤ᵐ[μ.restrict s] g
h : g - f =ᵐ[μ.restrict s] fun x ↦ ↑(g x - f x).toNNReal
⊢ (fun y ↦ ENNReal.ofReal ((g - f) y)) =ᵐ[μ.restrict s] fun a ↦ ↑(g a - f a).toNNReal

Tactic:
rfl

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_3
F : Type u_4
V : Type u_5
W : Type u_6
inst✝¹⁰ : NontriviallyNormedField 𝕜
inst✝⁹ : NormedAddCommGroup V
inst✝⁸ : NormedSpace 𝕜 V
inst✝⁷ : MeasurableSpace V
inst✝⁶ : BorelSpace V
inst✝⁵ : NormedAddCommGroup W
inst✝⁴ : NormedSpace 𝕜 W
e : AddChar 𝕜 𝕊
μ : Measure V
L : V →L[𝕜] W →L[𝕜] 𝕜
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : V → F →L[ℝ] E
a : F
w : W
he : Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] ⇑e
hf : Integrable f μ
⊢ ∫ (x : V), (e (-((ContinuousLinearMap.toLinearMap₁₂ L) x) w) • f x) a ∂μ =
    fourierIntegral e μ (ContinuousLinearMap.toLinearMap₁₂ L) (fun x ↦ (f x) a) w

Tactic:
rfl

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

Goal state before:
pp: 𝕜 : Type u_1
ι : Type u_2
E : Type u_3
V : Type u_5
W : Type u_6
inst✝¹¹ : Fintype ι
inst✝¹⁰ : NontriviallyNormedField 𝕜
inst✝⁹ : NormedAddCommGroup V
inst✝⁸ : NormedSpace 𝕜 V
inst✝⁷ : MeasurableSpace V
inst✝⁶ : BorelSpace V
inst✝⁵ : NormedAddCommGroup W
inst✝⁴ : NormedSpace 𝕜 W
e : AddChar 𝕜 𝕊
μ : Measure V
L : V →L[𝕜] W →L[𝕜] 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
M : ι → Type u_7
inst✝¹ : (i : ι) → NormedAddCommGroup (M i)
inst✝ : (i : ι) → NormedSpace ℝ (M i)
f : V → ContinuousMultilinearMap ℝ M E
m : (i : ι) → M i
w : W
he : Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] ⇑e
hf : Integrable f μ
⊢ ∫ (x : V), (e (-((ContinuousLinearMap.toLinearMap₁₂ L) x) w) • f x) m ∂μ =
    fourierIntegral e μ (ContinuousLinearMap.toLinearMap₁₂ L) (fun x ↦ (f x) m) w

Tactic:
rfl

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

Goal state before:
pp: α : Type u_1
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
g : α → F
l : Filter α
ι : Type u_4
inst✝² : MeasurableSpace ι
f : ι × α → E
s : Set ι
μ : Measure ι
inst✝¹ : NormedSpace ℝ E
inst✝ : NormedAddCommGroup F
hf : f =O[𝓟 s ×ˢ l] (g ∘ Prod.snd)
hμ : μ s < ⊤
⊢ (fun x ↦ ∫ (i : ι) in s, f (i, x) ∂μ) =O[l] g

Tactic:
by
  obtain ⟨C, hC⟩ := hf.bound
  obtain ⟨t, htl, ht⟩ := hC.exists_mem
  obtain ⟨u, hu, v, hv, huv⟩ := mem_prod_iff.mp htl
  refine isBigO_iff.mpr ⟨C * μ.real s, eventually_iff_exists_mem.mpr ⟨v, hv, fun x hx ↦ ?_⟩⟩
  calc
    _ ≤ C * ‖g x‖ * μ.real s :=
      norm_setIntegral_le_of_norm_le_const hμ fun y hy ↦ ht (y, x) <| huv ⟨hu hy, hx⟩
    _ = _ := by ring

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

Goal state before:
pp: c : ℝ
hc : 1 < c
t : ℝ
a✝ : t ∈ Ici c
⊢ t ≠ 0

Tactic:
grind

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

Goal state before:
pp: c : ℝ
hc : 1 < c
t : ℝ
a✝ : t ∈ Ici c
⊢ t ≠ 1

Tactic:
grind

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

Goal state before:
pp: c : ℝ
hc : 1 < c
t : ℝ
a✝ : t ∈ Ici c
⊢ t ≠ -1

Tactic:
grind

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

Goal state before:
pp: E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℝ → E
w : ℝ
⊢ 𝓕 f w = ∫ (v : ℝ), 𝐞 (-(w * v)) • f v

Tactic:
rfl

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

Goal state before:
pp: c : ℝ
hc : 1 < c
t : ℝ
a✝ : t ∈ Ioi c
⊢ 0 < t

Tactic:
grind

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

Goal state before:
pp: case convert_2
c : ℝ
hc : 1 < c
⊢ Tendsto (fun t ↦ -(log t)⁻¹) atTop (𝓝 0)

Tactic:
convert! tendsto_log_atTop.inv_tendsto_atTop.neg using 1

Goal state after:
case e'_5
c : ℝ
hc : 1 < c
⊢ 𝓝 0 = 𝓝 (-0)
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic

Goal state before:
pp: s : ℝ
h : 0 < s
⊢ ∀ x ∈ Ici 1, id x ≠ 0 ∨ 0 ≤ s - 1

Tactic:
grind

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

Goal state before:
pp: s : ℂ
hs : 0 < s.re
X : ℝ
hX : 0 ≤ X
x✝ : ℝ
⊢ -(cexp (-↑x✝) * ↑x✝ ^ s) = (-fun x ↦ cexp (-↑x) * ↑x ^ s) x✝

Tactic:
rfl

Goal state after: