mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Convex.Side

Goal state before:
pp: case inl
R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁶ : Field R
inst✝⁵ : LinearOrder R
inst✝⁴ : IsStrictOrderedRing R
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : AffineSpace V P
n : ℕ
inst✝ : NeZero n
s : Simplex R P n
w₁ w₂ : Fin (n + 1) → R
hw₁ : ∑ j, w₁ j = 1
hw₂ : ∑ j, w₂ j = 1
i : Fin (n + 1)
h :
  (affineSpan R (Set.range (s.faceOpposite i).points)).SSameSide ((Finset.affineCombination R Finset.univ s.points) w₁)
    ((Finset.affineCombination R Finset.univ s.points) w₂)
h0 : w₁ i ≠ 0
h0' : w₂ i ≠ 0
hs : SignType.sign (w₁ i) = SignType.sign (w₂ i)
⊢ SignType.sign (w₁ i) = SignType.sign (w₂ i)

pp: case inr
R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁶ : Field R
inst✝⁵ : LinearOrder R
inst✝⁴ : IsStrictOrderedRing R
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : AffineSpace V P
n : ℕ
inst✝ : NeZero n
s : Simplex R P n
w₁ w₂ : Fin (n + 1) → R
hw₁ : ∑ j, w₁ j = 1
hw₂ : ∑ j, w₂ j = 1
i : Fin (n + 1)
h :
  (affineSpan R (Set.range (s.faceOpposite i).points)).SSameSide ((Finset.affineCombination R Finset.univ s.points) w₁)
    ((Finset.affineCombination R Finset.univ s.points) w₂)
h0 : w₁ i ≠ 0
h0' : w₂ i ≠ 0
hs : SignType.sign (w₁ i) = -SignType.sign (w₂ i)
⊢ SignType.sign (w₁ i) = SignType.sign (w₂ i)

Tactic:
· exact hs

Goal state after:
case inr
R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁶ : Field R
inst✝⁵ : LinearOrder R
inst✝⁴ : IsStrictOrderedRing R
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : AffineSpace V P
n : ℕ
inst✝ : NeZero n
s : Simplex R P n
w₁ w₂ : Fin (n + 1) → R
hw₁ : ∑ j, w₁ j = 1
hw₂ : ∑ j, w₂ j = 1
i : Fin (n + 1)
h :
  (affineSpan R (Set.range (s.faceOpposite i).points)).SSameSide ((Finset.affineCombination R Finset.univ s.points) w₁)
    ((Finset.affineCombination R Finset.univ s.points) w₂)
h0 : w₁ i ≠ 0
h0' : w₂ i ≠ 0
hs : SignType.sign (w₁ i) = -SignType.sign (w₂ i)
⊢ SignType.sign (w₁ i) = SignType.sign (w₂ i)
Module: Mathlib.Analysis.Convex.Side

Goal state before:
pp: case refine_1.inr
R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁶ : Field R
inst✝⁵ : LinearOrder R
inst✝⁴ : IsStrictOrderedRing R
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : AffineSpace V P
n : ℕ
inst✝ : NeZero n
s : Simplex R P n
w₁ w₂ : Fin (n + 1) → R
hw₁ : ∑ j, w₁ j = 1
hw₂ : ∑ j, w₂ j = 1
i : Fin (n + 1)
h :
  (affineSpan R (Set.range (s.faceOpposite i).points)).SOppSide ((Finset.affineCombination R Finset.univ s.points) w₁)
    ((Finset.affineCombination R Finset.univ s.points) w₂)
h0 : w₁ i ≠ 0
h0' : w₂ i ≠ 0
hs : SignType.sign (w₁ i) = -SignType.sign (w₂ i)
⊢ SignType.sign (w₁ i) = -SignType.sign (w₂ i)

Tactic:
· exact hs

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

Goal state before:
pp: α : Type u_1
inst✝¹ : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
μ : Measure α
inst✝ : SFinite μ
f_nn : 0 ≤ f
f_mble : Measurable f
g_intble : ∀ t > 0, IntervalIntegrable g volume 0 t
g_mble : Measurable g
g_nn : ∀ t > 0, 0 ≤ g t
g_intble' : ∀ (t : ℝ), 0 ≤ t → IntervalIntegrable g volume 0 t
ω : α
g_ae_nn : 0 ≤ᵐ[volume.restrict (Ioc 0 (f ω))] g
⊢ ENNReal.ofReal (∫ (t : ℝ) in 0..f ω, g t) = ∫⁻ (t : ℝ) in Ioc 0 (f ω), ENNReal.ofReal (g t)

Tactic:
rw [← ofReal_integral_eq_lintegral_ofReal (g_intble' (f ω) (f_nn ω)).1 g_ae_nn]

Goal state after:
α : Type u_1
inst✝¹ : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
μ : Measure α
inst✝ : SFinite μ
f_nn : 0 ≤ f
f_mble : Measurable f
g_intble : ∀ t > 0, IntervalIntegrable g volume 0 t
g_mble : Measurable g
g_nn : ∀ t > 0, 0 ≤ g t
g_intble' : ∀ (t : ℝ), 0 ≤ t → IntervalIntegrable g volume 0 t
ω : α
g_ae_nn : 0 ≤ᵐ[volume.restrict (Ioc 0 (f ω))] g
⊢ ENNReal.ofReal (∫ (t : ℝ) in 0..f ω, g t) = ENNReal.ofReal (∫ (x : ℝ) in Ioc 0 (f ω), g x ∂volume)
Module: Mathlib.Analysis.Distribution.TestFunction

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹⁴ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
Ω : Opens E
F : Type u_4
inst✝¹¹ : NormedAddCommGroup F
inst✝¹⁰ : NormedSpace ℝ F
inst✝⁹ : NormedSpace 𝕜 F
n : ℕ∞
V : Type u_6
inst✝⁸ : AddCommGroup V
inst✝⁷ : Module ℝ V
t : TopologicalSpace V
inst✝⁶ : IsTopologicalAddGroup V
inst✝⁵ : ContinuousSMul ℝ V
inst✝⁴ : LocallyConvexSpace ℝ V
inst✝³ : Algebra ℝ 𝕜
inst✝² : IsScalarTower ℝ 𝕜 F
inst✝¹ : Module 𝕜 V
inst✝ : IsScalarTower ℝ 𝕜 V
f : 𝓓^{n}(Ω, F) →ₗ[𝕜] V
⊢ topologicalSpace Ω F n ≤ induced (⇑(↑ℝ f)) t ↔
    ∀ (K : Compacts E) (K_sub_Ω : ↑K ⊆ ↑Ω), Continuous[_, t] (⇑(↑ℝ f) ∘ ofSupportedIn K_sub_Ω)

Tactic:
have : @IsTopologicalAddGroup _ (induced (f.restrictScalars ℝ) t) _ :=
    topologicalAddGroup_induced _

Goal state after:
𝕜 : Type u_1
inst✝¹⁴ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
Ω : Opens E
F : Type u_4
inst✝¹¹ : NormedAddCommGroup F
inst✝¹⁰ : NormedSpace ℝ F
inst✝⁹ : NormedSpace 𝕜 F
n : ℕ∞
V : Type u_6
inst✝⁸ : AddCommGroup V
inst✝⁷ : Module ℝ V
t : TopologicalSpace V
inst✝⁶ : IsTopologicalAddGroup V
inst✝⁵ : ContinuousSMul ℝ V
inst✝⁴ : LocallyConvexSpace ℝ V
inst✝³ : Algebra ℝ 𝕜
inst✝² : IsScalarTower ℝ 𝕜 F
inst✝¹ : Module 𝕜 V
inst✝ : IsScalarTower ℝ 𝕜 V
f : 𝓓^{n}(Ω, F) →ₗ[𝕜] V
this : IsTopologicalAddGroup 𝓓^{n}(Ω, F)
⊢ topologicalSpace Ω F n ≤ induced (⇑(↑ℝ f)) t ↔
    ∀ (K : Compacts E) (K_sub_Ω : ↑K ⊆ ↑Ω), Continuous[_, t] (⇑(↑ℝ f) ∘ ofSupportedIn K_sub_Ω)
Module: Mathlib.MeasureTheory.Integral.Layercake

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
f : α → ℝ
μ : Measure α
f_nn : 0 ≤ᵐ[μ] f
f_mble : AEMeasurable f μ
cst : ℝ → ℝ := fun x ↦ 1
cst_intble : ∀ t > 0, IntervalIntegrable cst volume 0 t
⊢ ∫⁻ (ω : α), ENNReal.ofReal (f ω) ∂μ = ∫⁻ (t : ℝ) in Ioi 0, μ {a | t ≤ f a}

Tactic:
have key :=
    lintegral_comp_eq_lintegral_meas_le_mul μ f_nn f_mble cst_intble
      (Eventually.of_forall fun _ => zero_le_one)

Goal state after:
α : Type u_1
inst✝ : MeasurableSpace α
f : α → ℝ
μ : Measure α
f_nn : 0 ≤ᵐ[μ] f
f_mble : AEMeasurable f μ
cst : ℝ → ℝ := fun x ↦ 1
cst_intble : ∀ t > 0, IntervalIntegrable cst volume 0 t
key :
  ∫⁻ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0..f ω, cst t) ∂μ =
    ∫⁻ (t : ℝ) in Ioi 0, μ {a | t ≤ f a} * ENNReal.ofReal (cst t)
⊢ ∫⁻ (ω : α), ENNReal.ofReal (f ω) ∂μ = ∫⁻ (t : ℝ) in Ioi 0, μ {a | t ≤ f a}
Module: Mathlib.Analysis.Normed.Operator.Compact.Basic

Goal state before:
pp: M₁ : Type u_3
M₄ : Type u_5
inst✝⁴ : TopologicalSpace M₁
inst✝³ : AddCommMonoid M₁
inst✝² : TopologicalSpace M₄
inst✝¹ : AddCommGroup M₄
inst✝ : IsTopologicalAddGroup M₄
f g : M₁ → M₄
hf : IsCompactOperator f
hg : IsCompactOperator g
⊢ IsCompactOperator (f - g)

Tactic:
sub_eq_add_neg

Goal state after:
M₁ : Type u_3
M₄ : Type u_5
inst✝⁴ : TopologicalSpace M₁
inst✝³ : AddCommMonoid M₁
inst✝² : TopologicalSpace M₄
inst✝¹ : AddCommGroup M₄
inst✝ : IsTopologicalAddGroup M₄
f g : M₁ → M₄
hf : IsCompactOperator f
hg : IsCompactOperator g
⊢ IsCompactOperator (f + -g)
Module: Mathlib.Analysis.InnerProductSpace.Rayleigh

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 : IsSelfAdjoint T
x₀ : E
hx₀ : x₀ ≠ 0
hextr : IsLocalExtrOn T.reApplyInnerSelf (sphere 0 ‖x₀‖) x₀
⊢ HasEigenvector (↑T) (↑(T.rayleighQuotient x₀)) x₀

Tactic:
by
  refine ⟨?_, hx₀⟩
  rw [Module.End.mem_eigenspace_iff]
  exact hT.eq_smul_self_of_isLocalExtrOn hextr

Goal state after:
Module: Mathlib.Analysis.Normed.Operator.Compact.FredholmAlternative

Goal state before:
pp: 𝕜 : Type u_1
X : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup X
inst✝ : NormedSpace 𝕜 X
T : X →L[𝕜] X
μ : 𝕜
hT : IsCompactOperator ⇑T
hμ : μ ≠ 0
h : ∀ c > 0, ∃ x, ‖(T - μ • 1) x‖ < c * ‖x‖
c : ℝ
hc₀ : c > 0
hc : ∀ ε > 0, ∃ x, ‖x‖ ≤ 1 ∧ c ≤ ‖x‖ ∧ ‖(T - μ • 1) x‖ < ε
φ : ℕ → ℝ
hφ_anti : StrictAnti φ
hφ_pos : ∀ (n : ℕ), 0 < φ n
hφ : Tendsto φ atTop (𝓝 0)
x : ℕ → X
hx_norm_upper : ∀ (n : ℕ), ‖x n‖ ≤ 1
hx_norm_lower : ∀ (n : ℕ), c ≤ ‖x n‖
hx_bound : ∀ (n : ℕ), ‖(T - μ • 1) (x n)‖ < φ n
hx_lim : Tendsto (fun n ↦ (T - μ • 1) (x n)) atTop (𝓝 0)
y_ : ℕ → X := fun n ↦ T (x n)
hy_lower : ∃ d > 0, ∀ᶠ (n : ℕ) in atTop, d ≤ ‖y_ n‖
K : Set X
hK : IsCompact K
hK' : ⇑↑T '' Metric.closedBall 0 1 ⊆ K
y : X
hyK : y ∈ K
ψ : ℕ → ℕ
hψ : StrictMono ψ
hψy : Tendsto (y_ ∘ ψ) atTop (𝓝 y)
hy_lim : Tendsto (fun n ↦ (T - μ • 1) (y_ n)) atTop (𝓝 0)
hy_eigen' : (T - μ • 1) y = 0
⊢ y ≠ 0

Tactic:
obtain ⟨d, hd₀, hd⟩ := hy_lower

Goal state after:
𝕜 : Type u_1
X : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup X
inst✝ : NormedSpace 𝕜 X
T : X →L[𝕜] X
μ : 𝕜
hT : IsCompactOperator ⇑T
hμ : μ ≠ 0
h : ∀ c > 0, ∃ x, ‖(T - μ • 1) x‖ < c * ‖x‖
c : ℝ
hc₀ : c > 0
hc : ∀ ε > 0, ∃ x, ‖x‖ ≤ 1 ∧ c ≤ ‖x‖ ∧ ‖(T - μ • 1) x‖ < ε
φ : ℕ → ℝ
hφ_anti : StrictAnti φ
hφ_pos : ∀ (n : ℕ), 0 < φ n
hφ : Tendsto φ atTop (𝓝 0)
x : ℕ → X
hx_norm_upper : ∀ (n : ℕ), ‖x n‖ ≤ 1
hx_norm_lower : ∀ (n : ℕ), c ≤ ‖x n‖
hx_bound : ∀ (n : ℕ), ‖(T - μ • 1) (x n)‖ < φ n
hx_lim : Tendsto (fun n ↦ (T - μ • 1) (x n)) atTop (𝓝 0)
y_ : ℕ → X := fun n ↦ T (x n)
K : Set X
hK : IsCompact K
hK' : ⇑↑T '' Metric.closedBall 0 1 ⊆ K
y : X
hyK : y ∈ K
ψ : ℕ → ℕ
hψ : StrictMono ψ
hψy : Tendsto (y_ ∘ ψ) atTop (𝓝 y)
hy_lim : Tendsto (fun n ↦ (T - μ • 1) (y_ n)) atTop (𝓝 0)
hy_eigen' : (T - μ • 1) y = 0
d : ℝ
hd₀ : d > 0
hd : ∀ᶠ (n : ℕ) in atTop, d ≤ ‖y_ n‖
⊢ y ≠ 0
Module: Mathlib.Analysis.Matrix.Spectrum

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : RCLike 𝕜
n : Type u_2
inst✝¹ : Fintype n
A : Matrix n n 𝕜
inst✝ : DecidableEq n
hA : A.IsHermitian
⊢ ((conjStarAlgAut 𝕜 (Matrix n n 𝕜)) (star hA.eigenvectorUnitary)) A = diagonal (RCLike.ofReal ∘ hA.eigenvalues)

Tactic:
apply Matrix.toEuclideanLin.injective <| (EuclideanSpace.basisFun n 𝕜).toBasis.ext fun i ↦ ?_

Goal state after:
𝕜 : Type u_1
inst✝² : RCLike 𝕜
n : Type u_2
inst✝¹ : Fintype n
A : Matrix n n 𝕜
inst✝ : DecidableEq n
hA : A.IsHermitian
i : n
⊢ (toEuclideanLin (((conjStarAlgAut 𝕜 (Matrix n n 𝕜)) (star hA.eigenvectorUnitary)) A))
      ((EuclideanSpace.basisFun n 𝕜).toBasis i) =
    (toEuclideanLin (diagonal (RCLike.ofReal ∘ hA.eigenvalues))) ((EuclideanSpace.basisFun n 𝕜).toBasis i)
Module: Mathlib.Analysis.Matrix.Spectrum

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : RCLike 𝕜
n : Type u_2
inst✝¹ : Fintype n
A B : Matrix n n 𝕜
inst✝ : DecidableEq n
hA : A.IsHermitian
hB : B.IsHermitian
⊢ hA.eigenvalues = hB.eigenvalues ↔ A.charpoly = B.charpoly

Tactic:
by
  constructor <;> intro h
  · rw [hA.charpoly_eq, hB.charpoly_eq, h]
  · suffices hA.eigenvalues₀ = hB.eigenvalues₀ by unfold eigenvalues; rw [this]
    simp_rw [← List.ofFn_inj, ← sort_roots_charpoly_eq_eigenvalues₀, h]

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
hT : T.IsSymmetric
v : E
μ : Eigenvalues T
⊢ (hT.diagonalization (T v)).ofLp μ = ↑T 1 μ • (hT.diagonalization v).ofLp μ

Tactic:
suffices
    ∀ w : PiLp 2 fun μ : Eigenvalues T => eigenspace T μ,
      T (hT.diagonalization.symm w) = hT.diagonalization.symm (toLp 2 fun μ => (μ : 𝕜) • w μ) by
    simpa only [LinearIsometryEquiv.symm_apply_apply, LinearIsometryEquiv.apply_symm_apply] using
      congr_arg (fun w => hT.diagonalization w μ) (this (hT.diagonalization v))
  intro w
  have hwT : ∀ μ, T (w μ) = (μ : 𝕜) • w μ := fun μ => mem_eigenspace_iff.1 (w μ).2
  simp only [diagonalization_symm_apply, map_sum, hwT, SetLike.val_smul]

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

Goal state before:
pp: α : Type u_1
E : Type u_2
𝕜 : Type u_4
inst✝⁴ : RCLike 𝕜
m : MeasurableSpace α
μ : Measure α
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
s : Set α
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
hs : MeasurableSet s
hμs : μ s ≠ ∞
c : E
f : ↥(Lp E 2 μ)
⊢ ⟪indicatorConstLp 2 hs hμs c, f⟫ = ⟪c, ∫ (x : α) in s, ↑↑f x ∂μ⟫

Tactic:
rw [← integral_inner (integrableOn_Lp_of_measure_ne_top f fact_one_le_two_ennreal.elim hμs),
    L2.inner_indicatorConstLp_eq_setIntegral_inner]

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

Goal state before:
pp: α : Type u_1
𝕜 : Type u_2
inst✝⁴ : TopologicalSpace α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
inst✝¹ : RCLike 𝕜
μ : Measure α
inst✝ : IsFiniteMeasure μ
f g : α →ᵇ 𝕜
⊢ ⟪(BoundedContinuousFunction.toLp 2 μ 𝕜) f, (BoundedContinuousFunction.toLp 2 μ 𝕜) g⟫ =
    ∫ (x : α), g x * (starRingEnd 𝕜) (f x) ∂μ

Tactic:
by
  apply integral_congr_ae
  have hf_ae := f.coeFn_toLp 2 μ 𝕜
  have hg_ae := g.coeFn_toLp 2 μ 𝕜
  filter_upwards [hf_ae, hg_ae] with _ hf hg
  rw [hf, hg]
  simp

Goal state after:
Module: Mathlib.Analysis.Normed.Module.Bases

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
X : Type u_2
inst✝¹ : NormedAddCommGroup X
inst✝ : NormedSpace 𝕜 X
b : SchauderBasis 𝕜 X
n m : ℕ
x : X
⊢ (GeneralSchauderBasis.proj b (Finset.range n ∩ Finset.range m)) x =
    (GeneralSchauderBasis.proj b (Finset.range (min n m))) x

Tactic:
congr 2

Goal state after:
case e_A
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
X : Type u_2
inst✝¹ : NormedAddCommGroup X
inst✝ : NormedSpace 𝕜 X
b : SchauderBasis 𝕜 X
n m : ℕ
x : X
⊢ Finset.range n ∩ Finset.range m = Finset.range (min n m)
Module: Mathlib.Analysis.Distribution.SchwartzSpace.Deriv

Goal state before:
pp: case succ
E : Type u_5
F : Type u_8
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : NormedSpace ℝ E
f : 𝓢(E, F)
n : ℕ
ih : ∀ {m : Fin n → E} {x : E}, (∂^{m} f) x = (iteratedFDeriv ℝ n (⇑f) x) m
m : Fin (n + 1) → E
x : E
⊢ (∂_{m 0} (∂^{Fin.tail m} f)) x = ((fderiv ℝ (iteratedFDeriv ℝ n ⇑f) x) (m 0)) (Fin.tail m)

Tactic:
← fderiv_continuousMultilinear_apply_const_apply

Goal state after:
case succ
E : Type u_5
F : Type u_8
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : NormedSpace ℝ E
f : 𝓢(E, F)
n : ℕ
ih : ∀ {m : Fin n → E} {x : E}, (∂^{m} f) x = (iteratedFDeriv ℝ n (⇑f) x) m
m : Fin (n + 1) → E
x : E
⊢ (∂_{m 0} (∂^{Fin.tail m} f)) x = (fderiv ℝ (fun y ↦ (iteratedFDeriv ℝ n (⇑f) y) (Fin.tail m)) x) (m 0)

case succ.hc
E : Type u_5
F : Type u_8
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : NormedSpace ℝ E
f : 𝓢(E, F)
n : ℕ
ih : ∀ {m : Fin n → E} {x : E}, (∂^{m} f) x = (iteratedFDeriv ℝ n (⇑f) x) m
m : Fin (n + 1) → E
x : E
⊢ DifferentiableAt ℝ (iteratedFDeriv ℝ n ⇑f) x
Module: Mathlib.Analysis.Distribution.SchwartzSpace.Deriv

Goal state before:
pp: case succ
E : Type u_5
F : Type u_8
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : NormedSpace ℝ E
f : 𝓢(E, F)
n : ℕ
ih : ∀ {m : Fin n → E} {x : E}, (∂^{m} f) x = (iteratedFDeriv ℝ n (⇑f) x) m
m : Fin (n + 1) → E
x : E
⊢ (∂^{m} f) x = (iteratedFDeriv ℝ (n + 1) (⇑f) x) m

Tactic:
rw [iteratedLineDerivOp_succ_left, iteratedFDeriv_succ_apply_left,
      ← fderiv_continuousMultilinear_apply_const_apply]
    · simp only [lineDerivOp_apply_eq_fderiv, ← ih]
    · exact (f.smooth ⊤).differentiable_iteratedFDeriv (mod_cast ENat.natCast_lt_top n) x

Goal state after:
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✝² : SecondCountableTopologyEither α E
inst✝¹ : Fact (1 ≤ p)
hp : p ≠ ∞
inst✝ : μ.WeaklyRegular
f : ↥(Lp E p μ)
ε : ℝ≥0∞
hε : 0 < ε
g : α →ᵇ E
hg : eLpNorm (↑↑f - ⇑g) p μ ≤ ε
g_mem : MemLp (⇑g) p μ
⊢ ∃ y ∈ ↑(boundedContinuousFunction E p μ), y ∈ Metric.closedEBall f ε

Tactic:
refine ⟨g_mem.toLp _, ⟨g, rfl⟩, ?_⟩

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✝² : SecondCountableTopologyEither α E
inst✝¹ : Fact (1 ≤ p)
hp : p ≠ ∞
inst✝ : μ.WeaklyRegular
f : ↥(Lp E p μ)
ε : ℝ≥0∞
hε : 0 < ε
g : α →ᵇ E
hg : eLpNorm (↑↑f - ⇑g) p μ ≤ ε
g_mem : MemLp (⇑g) p μ
⊢ MemLp.toLp (⇑g) g_mem ∈ Metric.closedEBall f ε
Module: Mathlib.Analysis.Fourier.AddCircle

Goal state before:
pp: T : ℝ
hT : Fact (0 < T)
f : ↥(Lp ℂ 2 haarAddCircle)
⊢ HasSum (fun i ↦ fourierCoeff (↑↑f) i • fourierLp 2 i) f

Tactic:
by
  simp_rw [← fourierBasis_repr]; rw [← coe_fourierBasis]
  exact HilbertBasis.hasSum_repr fourierBasis f

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

Goal state before:
pp: case refine_2
α : Type u_1
E : Type u_2
ι : Type u_3
hm : MeasurableSpace α
μ : Measure α
inst✝³ : TopologicalSpace α
inst✝² : BorelSpace α
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
g : α → E
l : Filter ι
x₀ : α
s t : Set α
φ : ι → α → ℝ
hs : MeasurableSet s
ht : MeasurableSet t
hts : t ⊆ s
h'ts : t ∈ 𝓝[s] x₀
hnφ : ∀ᶠ (i : ι) in l, ∀ x ∈ s, 0 ≤ φ i x
hlφ : ∀ (u : Set α), IsOpen[inst✝³] u → x₀ ∈ u → TendstoUniformlyOn φ 0 l (s \ u)
hiφ : Tendsto (fun i ↦ ∫ (x : α) in t, φ i x ∂μ) l (𝓝 1)
h'iφ : ∀ᶠ (i : ι) in l, AEStronglyMeasurable (φ i) (μ.restrict s)
hmg : IntegrableOn g s μ
hcg : Tendsto g (𝓝[s] x₀) (𝓝 0)
ε : ℝ
εpos : ε > 0
δ : ℝ
hδ : δ * ∫ (x : α) in s, ‖g x‖ ∂μ + 2 * δ < ε
δpos : 0 < δ
δone : δ < 1
u : Set α
u_open : IsOpen[inst✝³] u
x₀u : x₀ ∈ u
ut : s ∩ u ⊆ t
hu : ∀ x ∈ u ∩ s, g x ∈ ball 0 δ
i : ι
hi : ∀ x ∈ s \ u, dist (0 x) (φ i x) < δ
h'i : ‖∫ (x : α) in t, φ i x ∂μ - 1‖ < δ
hφpos : ∀ x ∈ s, 0 ≤ φ i x
h''i : IntegrableOn (fun x ↦ φ i x • g x) s μ
I : IntegrableOn (φ i) t μ
B : ‖∫ (x : α) in s ∩ u, φ i x • g x ∂μ‖ ≤ 2 * δ
⊢ IntegrableOn (fun x ↦ δ * ‖g x‖) (s \ u) μ

Tactic:
exact IntegrableOn.mono_set (hmg.norm.const_mul _) sdiff_subset

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

Goal state before:
pp: α : Type u_1
E : Type u_2
ι : Type u_3
hm : MeasurableSpace α
μ : Measure α
inst✝⁴ : TopologicalSpace α
inst✝³ : BorelSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
g : α → E
l : Filter ι
x₀ : α
s : Set α
φ : ι → α → ℝ
a : E
inst✝ : CompleteSpace E
hs : MeasurableSet s
t : Set α
ht : MeasurableSet t
hts : t ⊆ s
h'ts : t ∈ 𝓝[s] x₀
h't : μ t ≠ ∞
hnφ : ∀ᶠ (i : ι) in l, ∀ x ∈ s, 0 ≤ φ i x
hlφ : ∀ (u : Set α), IsOpen[inst✝⁴] u → x₀ ∈ u → TendstoUniformlyOn φ 0 l (s \ u)
hiφ : Tendsto (fun i ↦ ∫ (x : α) in t, φ i x ∂μ) l (𝓝 1)
h'iφ : ∀ᶠ (i : ι) in l, AEStronglyMeasurable (φ i) (μ.restrict s)
hmg : IntegrableOn g s μ
hcg : Tendsto g (𝓝[s] x₀) (𝓝 a)
h : α → E := g - t.indicator fun x ↦ a
⊢ Tendsto (fun i ↦ ∫ (x : α) in s, φ i x • h x ∂μ) l (𝓝 0)

Tactic:
apply tendsto_setIntegral_peak_smul_of_integrableOn_of_tendsto_aux hs ht hts h'ts
        hnφ hlφ hiφ h'iφ

Goal state after:
case hmg
α : Type u_1
E : Type u_2
ι : Type u_3
hm : MeasurableSpace α
μ : Measure α
inst✝⁴ : TopologicalSpace α
inst✝³ : BorelSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
g : α → E
l : Filter ι
x₀ : α
s : Set α
φ : ι → α → ℝ
a : E
inst✝ : CompleteSpace E
hs : MeasurableSet s
t : Set α
ht : MeasurableSet t
hts : t ⊆ s
h'ts : t ∈ 𝓝[s] x₀
h't : μ t ≠ ∞
hnφ : ∀ᶠ (i : ι) in l, ∀ x ∈ s, 0 ≤ φ i x
hlφ : ∀ (u : Set α), IsOpen[inst✝⁴] u → x₀ ∈ u → TendstoUniformlyOn φ 0 l (s \ u)
hiφ : Tendsto (fun i ↦ ∫ (x : α) in t, φ i x ∂μ) l (𝓝 1)
h'iφ : ∀ᶠ (i : ι) in l, AEStronglyMeasurable (φ i) (μ.restrict s)
hmg : IntegrableOn g s μ
hcg : Tendsto g (𝓝[s] x₀) (𝓝 a)
h : α → E := ⋯
⊢ IntegrableOn h s μ

case hcg
α : Type u_1
E : Type u_2
ι : Type u_3
hm : MeasurableSpace α
μ : Measure α
inst✝⁴ : TopologicalSpace α
inst✝³ : BorelSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
g : α → E
l : Filter ι
x₀ : α
s : Set α
φ : ι → α → ℝ
a : E
inst✝ : CompleteSpace E
hs : MeasurableSet s
t : Set α
ht : MeasurableSet t
hts : t ⊆ s
h'ts : t ∈ 𝓝[s] x₀
h't : μ t ≠ ∞
hnφ : ∀ᶠ (i : ι) in l, ∀ x ∈ s, 0 ≤ φ i x
hlφ : ∀ (u : Set α), IsOpen[inst✝⁴] u → x₀ ∈ u → TendstoUniformlyOn φ 0 l (s \ u)
hiφ : Tendsto (fun i ↦ ∫ (x : α) in t, φ i x ∂μ) l (𝓝 1)
h'iφ : ∀ᶠ (i : ι) in l, AEStronglyMeasurable (φ i) (μ.restrict s)
hmg : IntegrableOn g s μ
hcg : Tendsto g (𝓝[s] x₀) (𝓝 a)
h : α → E := ⋯
⊢ Tendsto h (𝓝[s] x₀) (𝓝 0)
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)
c : 𝕜
x : E
⊢ ‖x‖ ^ k * ‖iteratedFDeriv ℝ n (c • ⇑f) x‖ = ‖c‖ * ‖x‖ ^ k * ‖iteratedFDeriv ℝ n (⇑f) x‖

Tactic:
by
  rw [mul_comm ‖c‖, mul_assoc, iteratedFDeriv_const_smul_apply (f.smooth _).contDiffAt,
    norm_smul c (iteratedFDeriv ℝ n (⇑f) x)]

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
f g : 𝓢(E, F)
k n : ℕ
x : E
⊢ ‖x‖ ^ k * ‖iteratedFDeriv ℝ n (⇑f - ⇑g) x‖ ≤
    ‖x‖ ^ k * ‖iteratedFDeriv ℝ n (⇑f) x‖ + ‖x‖ ^ k * ‖iteratedFDeriv ℝ n (⇑g) x‖

Tactic:
sub_eq_add_neg

Goal state after:
ι : Type u_1
𝕜 : Type u_2
𝕜' : Type u_3
D : Type u_4
E : Type u_5
F : Type u_6
G : Type u_7
H : Type u_8
V : Type u_9
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f g : 𝓢(E, F)
k n : ℕ
x : E
⊢ ‖x‖ ^ k * ‖iteratedFDeriv ℝ n (⇑f + -⇑g) x‖ ≤
    ‖x‖ ^ k * ‖iteratedFDeriv ℝ n (⇑f) x‖ + ‖x‖ ^ k * ‖iteratedFDeriv ℝ n (⇑g) x‖
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
K : ℕ∞ω
C : ℝ
hf : ContDiff ℝ K f
n k : ℕ
hk : ↑k ≤ K
v : V
hv : ∀ i ≤ k, ∀ j ≤ n, ‖v‖ ^ j * ‖iteratedFDeriv ℝ i f v‖ ≤ C
T : (W →L[ℝ] ℝ) [×n]→L[ℝ] W [×n]→L[ℝ] ℝ :=
  (ContinuousMultilinearMap.mkPiAlgebra ℝ (Fin n) ℝ).compContinuousLinearMapLRight
I₁ : ∀ (m : ℕ), ‖iteratedFDeriv ℝ m ⇑T fun x ↦ L v‖ ≤ ↑(n.descFactorial m) * 1 * (‖L‖ * ‖v‖) ^ (n - m)
I₂ :
  ∀ (m : ℕ),
    ‖iteratedFDeriv ℝ m (⇑T ∘ ⇑(ContinuousLinearMap.pi fun x ↦ L)) v‖ ≤
      ↑(n.descFactorial m) * 1 * (‖L‖ * ‖v‖) ^ (n - m) * ‖L‖ ^ m
I₃ :
  ∀ (m : ℕ),
    ‖iteratedFDeriv ℝ m (⇑T ∘ ⇑(ContinuousLinearMap.pi fun x ↦ L)) v‖ ≤ ↑(n.descFactorial m) * ‖L‖ ^ n * ‖v‖ ^ (n - m)
A : ContDiff ℝ K fun y ↦ T fun x ↦ L y
⊢ ‖iteratedFDeriv ℝ k
        (fun v ↦
          (-(2 * ↑π * I)) ^ n •
            ((smulRightL ℝ (fun x ↦ W) E)
                ((ContinuousMultilinearMap.mkPiAlgebra ℝ (Fin n) ℝ).compContinuousLinearMapLRight fun x ↦ L v))
              (f v))
        v‖ ≤
    (2 * π) ^ n * (2 * ↑n + 2) ^ k * ‖L‖ ^ n * C

Tactic:
iteratedFDeriv_const_smul_apply' (hf := ((smulRightL ℝ (fun _ ↦ W)
    E).isBoundedBilinearMap.contDiff.comp₂ (A.of_le hk) (hf.of_le hk)).contDiffAt),

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
K : ℕ∞ω
C : ℝ
hf : ContDiff ℝ K f
n k : ℕ
hk : ↑k ≤ K
v : V
hv : ∀ i ≤ k, ∀ j ≤ n, ‖v‖ ^ j * ‖iteratedFDeriv ℝ i f v‖ ≤ C
T : (W →L[ℝ] ℝ) [×n]→L[ℝ] W [×n]→L[ℝ] ℝ :=
  (ContinuousMultilinearMap.mkPiAlgebra ℝ (Fin n) ℝ).compContinuousLinearMapLRight
I₁ : ∀ (m : ℕ), ‖iteratedFDeriv ℝ m ⇑T fun x ↦ L v‖ ≤ ↑(n.descFactorial m) * 1 * (‖L‖ * ‖v‖) ^ (n - m)
I₂ :
  ∀ (m : ℕ),
    ‖iteratedFDeriv ℝ m (⇑T ∘ ⇑(ContinuousLinearMap.pi fun x ↦ L)) v‖ ≤
      ↑(n.descFactorial m) * 1 * (‖L‖ * ‖v‖) ^ (n - m) * ‖L‖ ^ m
I₃ :
  ∀ (m : ℕ),
    ‖iteratedFDeriv ℝ m (⇑T ∘ ⇑(ContinuousLinearMap.pi fun x ↦ L)) v‖ ≤ ↑(n.descFactorial m) * ‖L‖ ^ n * ‖v‖ ^ (n - m)
A : ContDiff ℝ K fun y ↦ T fun x ↦ L y
⊢ ‖(-(2 * ↑π * I)) ^ n •
        iteratedFDeriv ℝ k (fun x ↦ ((smulRightL ℝ (fun x ↦ W) E) (T fun x_1 ↦ L x, f x).1) (T fun x_1 ↦ L x, f x).2)
          v‖ ≤
    (2 * π) ^ n * (2 * ↑n + 2) ^ k * ‖L‖ ^ n * C