mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Fin.Tuple.Sort

Goal state before:
pp: n : ℕ
α : Type u_1
j : Fin n
f : Fin n → α
inst✝¹ : Preorder α
a : α
inst✝ : DecidableLT α
h_sorted : Monotone f
⊢ ∀ (i j : Fin n), j ≤ i → f i < a → f j < a

Tactic:
by grind [Monotone]

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

Goal state before:
pp: 𝕜 : Type u_1
E✝ : Type u_2
F✝ : Type u_3
F' : Type u_4
inst✝¹⁵ : NontriviallyNormedField 𝕜
inst✝¹⁴ : NormedAddCommGroup E✝
inst✝¹³ : NormedSpace ℝ E✝
inst✝¹² : NormedAddCommGroup F✝
inst✝¹¹ : NormedSpace ℝ F✝
inst✝¹⁰ : NormedSpace 𝕜 F✝
inst✝⁹ : SMulCommClass ℝ 𝕜 F✝
inst✝⁸ : NormedAddCommGroup F'
inst✝⁷ : NormedSpace ℝ F'
inst✝⁶ : NormedSpace 𝕜 F'
inst✝⁵ : SMulCommClass ℝ 𝕜 F'
n✝ n₁ n₂ k : ℕ∞
K✝ K₁ K₂ : Compacts E✝
B : Type u_5
E : Type u_6
F : Type u_7
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedSpace ℝ F
n : ℕ∞
K : Compacts E
inst✝ : ContDiffMapSupportedInClass B E F n K
f : B
this : HasCompactSupport ⇑f
⊢ ∃ C, ∀ (x y : E), dist (f x) (f y) ≤ C

Tactic:
rcases (map_continuous f).bounded_above_of_compact_support this with ⟨C, hC⟩

Goal state after:
𝕜 : Type u_1
E✝ : Type u_2
F✝ : Type u_3
F' : Type u_4
inst✝¹⁵ : NontriviallyNormedField 𝕜
inst✝¹⁴ : NormedAddCommGroup E✝
inst✝¹³ : NormedSpace ℝ E✝
inst✝¹² : NormedAddCommGroup F✝
inst✝¹¹ : NormedSpace ℝ F✝
inst✝¹⁰ : NormedSpace 𝕜 F✝
inst✝⁹ : SMulCommClass ℝ 𝕜 F✝
inst✝⁸ : NormedAddCommGroup F'
inst✝⁷ : NormedSpace ℝ F'
inst✝⁶ : NormedSpace 𝕜 F'
inst✝⁵ : SMulCommClass ℝ 𝕜 F'
n✝ n₁ n₂ k : ℕ∞
K✝ K₁ K₂ : Compacts E✝
B : Type u_5
E : Type u_6
F : Type u_7
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedSpace ℝ F
n : ℕ∞
K : Compacts E
inst✝ : ContDiffMapSupportedInClass B E F n K
f : B
this : HasCompactSupport ⇑f
C : ℝ
hC : ∀ (x : E), ‖f x‖ ≤ C
⊢ ∃ C, ∀ (x y : E), dist (f x) (f y) ≤ C
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
μ : 𝕜
hμ : HasEigenvalue T μ
⊢ ∃ i, ↑(hT.eigenvalues hn i) = μ

Tactic:
by
  obtain ⟨i, hi⟩ := hT.exists_unsortedEigenvalues_eq hn hμ
  use ((Tuple.sort (hT.unsortedEigenvalues hn)).symm i).revPerm
  simp [eigenvalues_def, hi]

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
inst✝ : FiniteDimensional 𝕜 E
n : ℕ
hT : T.IsSymmetric
hn : finrank 𝕜 E = n
v : E
i : Fin n
w : EuclideanSpace 𝕜 (Fin n)
⊢ T (∑ x, w.ofLp x • (hT.eigenvectorBasis hn) x) = ∑ x, (↑(hT.eigenvalues hn x) * w.ofLp x) • (hT.eigenvectorBasis hn) x

Tactic:
map_sum,

Goal state after:
𝕜 : Type u_1
inst✝³ : RCLike 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
inst✝ : FiniteDimensional 𝕜 E
n : ℕ
hT : T.IsSymmetric
hn : finrank 𝕜 E = n
v : E
i : Fin n
w : EuclideanSpace 𝕜 (Fin n)
⊢ ∑ x, T (w.ofLp x • (hT.eigenvectorBasis hn) x) = ∑ x, (↑(hT.eigenvalues hn x) * w.ofLp x) • (hT.eigenvectorBasis hn) x
Module: Mathlib.Analysis.InnerProductSpace.Spectrum

Goal state before:
pp: 𝕜 : Type u_1
inst✝³ : RCLike 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
T : E →L[𝕜] E
hT : IsCompactOperator ⇑T
μ : 𝕜
hμ : μ ≠ 0
⊢ FiniteDimensional 𝕜 ↥(eigenspace (↑T) μ)

Tactic:
replace hT := hT.restrict'
    ((mem_invtSubmodule_iff_forall_mem_of_mem _).mp (eigenspace_mem_invtSubmodule T.toLinearMap μ))
  rw [restrict_eigenspace, LinearMap.coe_smul, IsCompactOperator.smul_iff₀ hμ] at hT
  rwa [← isCompactOperator_id_iff_finiteDimensional]

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

Goal state before:
pp: E : Type u_1
n : Type u_2
𝕜 : Type u_4
inst✝³ : RCLike 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : Fintype n
v : n → E
x y : n → 𝕜
⊢ star x ⬝ᵥ gram 𝕜 v *ᵥ y = ∑ i, ∑ j, (starRingEnd 𝕜) (x i) * y j * ⟪v i, v j⟫_𝕜

Tactic:
dotProduct,

Goal state after:
E : Type u_1
n : Type u_2
𝕜 : Type u_4
inst✝³ : RCLike 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : Fintype n
v : n → E
x y : n → 𝕜
⊢ ∑ i, star x i * (gram 𝕜 v *ᵥ y) i = ∑ i, ∑ j, (starRingEnd 𝕜) (x i) * y j * ⟪v i, v j⟫_𝕜
Module: Mathlib.Analysis.InnerProductSpace.GramMatrix

Goal state before:
pp: E : Type u_1
n : Type u_2
𝕜 : Type u_4
inst✝³ : RCLike 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : Fintype n
v : n → E
x y : n → 𝕜
⊢ ∑ i, star x i * (fun j ↦ gram 𝕜 v i j) ⬝ᵥ y = ∑ x_1, (starRingEnd 𝕜) (x x_1) * ∑ i, y i * ⟪v x_1, v i⟫_𝕜

Tactic:
dotProduct,

Goal state after:
E : Type u_1
n : Type u_2
𝕜 : Type u_4
inst✝³ : RCLike 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : Fintype n
v : n → E
x y : n → 𝕜
⊢ ∑ x_1, star x x_1 * ∑ x, gram 𝕜 v x_1 x * y x = ∑ x_1, (starRingEnd 𝕜) (x x_1) * ∑ i, y i * ⟪v x_1, v i⟫_𝕜
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)
hab : Commute (abs a) (abs b)
⊢ abs (a * b) = abs a * abs b

Tactic:
abs,

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)
⊢ sqrt (star (a * b) * (a * b)) = abs a * abs b
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 : A
ha : 0 ≤ a
⊢ abs a = a

Tactic:
abs,

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 : A
ha : 0 ≤ a
⊢ sqrt (star a * a) = a
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 : A
ha : IsSelfAdjoint a
| abs a

Tactic:
abs,

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 : A
ha : IsSelfAdjoint a
| sqrt (star a * a)
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
inst✝⁴ : StarModule ℝ A
R : Type u_3
inst✝³ : Semiring R
inst✝² : SMulWithZero R ℝ≥0
inst✝¹ : SMul R A
inst✝ : IsScalarTower R ℝ≥0 A
r✝ : R
a : A
r : ℝ≥0
⊢ abs (r • a) = r • abs a

Tactic:
abs,

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
inst✝⁴ : StarModule ℝ A
R : Type u_3
inst✝³ : Semiring R
inst✝² : SMulWithZero R ℝ≥0
inst✝¹ : SMul R A
inst✝ : IsScalarTower R ℝ≥0 A
r✝ : R
a : A
r : ℝ≥0
⊢ sqrt (star (r • a) * r • a) = r • abs a
Module: Mathlib.MeasureTheory.Function.L2Space

Goal state before:
pp: case e'_2.e'_7
α : Type u_1
F : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup F
f : α → F
hf : AEStronglyMeasurable f μ
⊢ 1 = 2 * 2⁻¹

Tactic:
ENNReal.mul_inv_cancel two_ne_zero ENNReal.ofNat_ne_top

Goal state after:
case e'_2.e'_7
α : Type u_1
F : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup F
f : α → F
hf : AEStronglyMeasurable f μ
⊢ 1 = 1
Module: Mathlib.MeasureTheory.Function.L2Space

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_2
𝕜 : Type u_3
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
f : α → E
hf : Integrable f μ
c : E
⊢ Integrable (fun x ↦ ⟪f x, c⟫) μ

Tactic:
rw [← memLp_one_iff_integrable] at hf ⊢; exact hf.inner_const c

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

Goal state before:
pp: 𝕜 : 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
a : A
ha : p a
⊢ abs a = cfcₙ (fun z ↦ ↑‖z‖) a

Tactic:
abs,

Goal state after:
𝕜 : 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
a : A
ha : p a
⊢ sqrt (star a * a) = cfcₙ (fun z ↦ ↑‖z‖) a
Module: Mathlib.Analysis.Distribution.ContDiffMapSupportedIn

Goal state before:
pp: E : Type u_2
F : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
n : ℕ∞
K : Compacts E
m : MeasurableSpace E
inst✝ : OpensMeasurableSpace E
μ : Measure E
μ_finite : IsFiniteMeasure (μ.restrict ↑K)
f : 𝓓^{n}_{K}(E, F)
⊢ Integrable (⇑f) μ

Tactic:
← integrableOn_iff_integrable_of_support_subset f.support_subset

Goal state after:
E : Type u_2
F : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
n : ℕ∞
K : Compacts E
m : MeasurableSpace E
inst✝ : OpensMeasurableSpace E
μ : Measure E
μ_finite : IsFiniteMeasure (μ.restrict ↑K)
f : 𝓓^{n}_{K}(E, F)
⊢ IntegrableOn (⇑f) (↑K) μ
Module: Mathlib.Analysis.Normed.Module.Bases

Goal state before:
pp: case pos
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
X : Type u_2
inst✝¹ : NormedAddCommGroup X
inst✝ : NormedSpace 𝕜 X
P : ℕ → X →L[𝕜] X
hcomp : ∀ (n m : ℕ) (x : X), (P n) ((P m) x) = (P (min n m)) x
i j : ℕ
x : X
h : i = j
⊢ (P (j + 1)) x - (P (min j (j + 1))) x - ((P j) x - (P j) x) = (P (j + 1)) x - (P j) x

Tactic:
Nat.min_eq_left (Nat.le_succ j)

Goal state after:
case pos
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
X : Type u_2
inst✝¹ : NormedAddCommGroup X
inst✝ : NormedSpace 𝕜 X
P : ℕ → X →L[𝕜] X
hcomp : ∀ (n m : ℕ) (x : X), (P n) ((P m) x) = (P (min n m)) x
i j : ℕ
x : X
h : i = j
⊢ (P (j + 1)) x - (P j) x - ((P j) x - (P j) x) = (P (j + 1)) x - (P j) x
Module: Mathlib.Analysis.Normed.Module.Bases

Goal state before:
pp: case neg.inr
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
X : Type u_2
inst✝¹ : NormedAddCommGroup X
inst✝ : NormedSpace 𝕜 X
P : ℕ → X →L[𝕜] X
hcomp : ∀ (n m : ℕ) (x : X), (P n) ((P m) x) = (P (min n m)) x
i j : ℕ
x : X
h : ¬i = j
h' : i > j
⊢ (P (min i j + 1)) x - (P (min i (j + 1))) x - ((P (min (i + 1) j)) x - (P (min i j)) x) = 0

Tactic:
rw [min_eq_right_of_lt h', min_eq_right (Nat.succ_le_of_lt h'),
        min_eq_right_of_lt (Nat.lt_succ_of_lt h')]
      abel

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

Goal state before:
pp: E : Type u_5
F₁ : Type u_9
F₂ : Type u_10
F₃ : Type u_11
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : InnerProductSpace ℝ E
inst✝⁹ : FiniteDimensional ℝ E
inst✝⁸ : NormedAddCommGroup F₁
inst✝⁷ : NormedSpace ℝ F₁
inst✝⁶ : NormedAddCommGroup F₂
inst✝⁵ : NormedSpace ℝ F₂
inst✝⁴ : NormedAddCommGroup F₃
inst✝³ : NormedSpace ℝ F₃
inst✝² : MeasurableSpace E
μ : Measure E
inst✝¹ : BorelSpace E
inst✝ : μ.IsAddHaarMeasure
f : 𝓢(E, F₁)
g : 𝓢(E, F₂)
L : F₁ →L[ℝ] F₂ →L[ℝ] F₃
⊢ ∫ (x : E), (L (f x)) (∑ i, (∂_{(stdOrthonormalBasis ℝ E) i} (∂_{(stdOrthonormalBasis ℝ E) i} g)) x) ∂μ =
    ∫ (x : E), (L (∑ i, (∂_{(stdOrthonormalBasis ℝ E) i} (∂_{(stdOrthonormalBasis ℝ E) i} f)) x)) (g x) ∂μ

Tactic:
map_sum,

Goal state after:
E : Type u_5
F₁ : Type u_9
F₂ : Type u_10
F₃ : Type u_11
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : InnerProductSpace ℝ E
inst✝⁹ : FiniteDimensional ℝ E
inst✝⁸ : NormedAddCommGroup F₁
inst✝⁷ : NormedSpace ℝ F₁
inst✝⁶ : NormedAddCommGroup F₂
inst✝⁵ : NormedSpace ℝ F₂
inst✝⁴ : NormedAddCommGroup F₃
inst✝³ : NormedSpace ℝ F₃
inst✝² : MeasurableSpace E
μ : Measure E
inst✝¹ : BorelSpace E
inst✝ : μ.IsAddHaarMeasure
f : 𝓢(E, F₁)
g : 𝓢(E, F₂)
L : F₁ →L[ℝ] F₂ →L[ℝ] F₃
⊢ ∫ (x : E), ∑ x_1, (L (f x)) ((∂_{(stdOrthonormalBasis ℝ E) x_1} (∂_{(stdOrthonormalBasis ℝ E) x_1} g)) x) ∂μ =
    ∫ (x : E), (∑ x_1, L ((∂_{(stdOrthonormalBasis ℝ E) x_1} (∂_{(stdOrthonormalBasis ℝ E) x_1} f)) x)) (g x) ∂μ
Module: Mathlib.MeasureTheory.Function.ContinuousMapDense

Goal state before:
pp: α : 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 μ
I3 : eLpNorm (f - t.indicator fun _y ↦ c) p μ ≤ ε
⊢ ∃ g,
    eLpNorm (g - t.indicator fun x ↦ c) p μ ≤ ε ∧
      Continuous[inst✝⁶, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] g ∧ MemLp g p μ ∧ IsBounded (range g)

Tactic:
refine ⟨f, I3, f_cont, f_mem, ?_⟩

Goal state after:
α : 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 μ
I3 : eLpNorm (f - t.indicator fun _y ↦ c) p μ ≤ ε
⊢ IsBounded (range f)
Module: Mathlib.Analysis.Fourier.AddCircle

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

Tactic:
Complex.ofReal_mul,

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

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

Tactic:
Complex.ofReal_mul,

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

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

Tactic:
Complex.ofReal_mul,

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

Goal state before:
pp: T : ℝ
hT : Fact (0 < T)
⊢ Orthonormal ℂ (fourierLp 2)

Tactic:
rw [orthonormal_iff_ite]

Goal state after:
T : ℝ
hT : Fact (0 < T)
⊢ ∀ (i j : ℤ), inner ℂ (fourierLp 2 i) (fourierLp 2 j) = if i = j then 1 else 0
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
⊢ Orthonormal 𝕜 ⇑b

Tactic:
rw [orthonormal_iff_ite]

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 : ι), ⟪b i, b j⟫ = if i = j then 1 else 0
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
⊢ Orthonormal 𝕜 ⇑b

Tactic:
classical
  rw [orthonormal_iff_ite]
  intro i j
  rw [← b.repr.inner_map_map (b i) (b j), b.repr_self, b.repr_self, lp.inner_single_left,
    lp.single_apply, Pi.single_apply]
  simp

Goal state after:
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 (⇑f) x‖ * ‖c‖ ≤ @SchwartzMap.seminormAux E F inst✝⁹ inst✝⁸ inst✝⁷ inst✝⁶ k n f * ‖c‖

Tactic:
gcongr
            apply f.le_seminormAux

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

Goal state before:
pp: α : Type u_1
E : Type u_2
hm : MeasurableSpace α
μ : Measure α
inst✝⁶ : TopologicalSpace α
inst✝⁵ : BorelSpace α
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
g : α → E
x₀ : α
s : Set α
inst✝² : CompleteSpace E
inst✝¹ : MetrizableSpace α
inst✝ : IsLocallyFiniteMeasure μ
hs : IsCompact s
hμ : ∀ (u : Set α), IsOpen[inst✝⁶] u → x₀ ∈ u → 0 < μ (u ∩ s)
c : α → ℝ
hc : ContinuousOn c s
h'c : ∀ y ∈ s, y ≠ x₀ → c y < c x₀
hnc : ∀ x ∈ s, 0 ≤ c x
hnc₀ : 0 < c x₀
h₀ : x₀ ∈ s
hmg : IntegrableOn g s μ
hcg : ContinuousWithinAt g s x₀
φ : ℕ → α → ℝ := fun n x ↦ (∫ (x : α) in s, c x ^ n ∂μ)⁻¹ * c x ^ n
hnφ : ∀ (n : ℕ), ∀ x ∈ s, 0 ≤ φ n x
⊢ Tendsto (fun n ↦ (∫ (x : α) in s, c x ^ n ∂μ)⁻¹ • ∫ (x : α) in s, c x ^ n • g x ∂μ) atTop (𝓝 (g x₀))

Tactic:
have I : ∀ n, IntegrableOn (fun x => c x ^ n) s μ := fun n =>
    ContinuousOn.integrableOn_compact hs (hc.pow n)

Goal state after:
α : Type u_1
E : Type u_2
hm : MeasurableSpace α
μ : Measure α
inst✝⁶ : TopologicalSpace α
inst✝⁵ : BorelSpace α
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
g : α → E
x₀ : α
s : Set α
inst✝² : CompleteSpace E
inst✝¹ : MetrizableSpace α
inst✝ : IsLocallyFiniteMeasure μ
hs : IsCompact s
hμ : ∀ (u : Set α), IsOpen[inst✝⁶] u → x₀ ∈ u → 0 < μ (u ∩ s)
c : α → ℝ
hc : ContinuousOn c s
h'c : ∀ y ∈ s, y ≠ x₀ → c y < c x₀
hnc : ∀ x ∈ s, 0 ≤ c x
hnc₀ : 0 < c x₀
h₀ : x₀ ∈ s
hmg : IntegrableOn g s μ
hcg : ContinuousWithinAt g s x₀
φ : ℕ → α → ℝ := fun n x ↦ (∫ (x : α) in s, c x ^ n ∂μ)⁻¹ * c x ^ n
hnφ : ∀ (n : ℕ), ∀ x ∈ s, 0 ≤ φ n x
I : ∀ (n : ℕ), IntegrableOn (fun x ↦ c x ^ n) s μ
⊢ Tendsto (fun n ↦ (∫ (x : α) in s, c x ^ n ∂μ)⁻¹ • ∫ (x : α) in s, c x ^ n • g x ∂μ) atTop (𝓝 (g x₀))