mathlib-initiative/mathlib-tactics huggingface dataset:
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 k : ℕ∞
inst✝¹ : Algebra ℝ 𝕜
inst✝ : IsScalarTower ℝ 𝕜 F
f : 𝓓^{n}(Ω, F)
v x : E
⊢ ((lineDerivCLM 𝕜 v) f) x = if k + 1 ≤ n then lineDeriv ℝ (⇑f) x v else 0

Tactic:
rw [lineDerivCLM_eq_fderivCLM, fderivCLM_apply]

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 k : ℕ∞
inst✝¹ : Algebra ℝ 𝕜
inst✝ : IsScalarTower ℝ 𝕜 F
f : 𝓓^{n}(Ω, F)
v x : E
⊢ ((if k + 1 ≤ n then fderiv ℝ ⇑f else 0) x) v = if k + 1 ≤ n then lineDeriv ℝ (⇑f) x v else 0
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 k : ℕ∞
inst✝¹ : Algebra ℝ 𝕜
inst✝ : IsScalarTower ℝ 𝕜 F
f : 𝓓^{n}(Ω, F)
v x : E
hk : k + 1 ≤ n
⊢ ((lineDerivCLM 𝕜 v) f) x = lineDeriv ℝ (⇑f) x v

Tactic:
simp [hk]

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

Goal state before:
pp: M₁ : Type u_3
M₂ : Type u_4
inst✝⁶ : TopologicalSpace M₁
inst✝⁵ : AddCommMonoid M₁
inst✝⁴ : TopologicalSpace M₂
inst✝³ : AddCommMonoid M₂
S : Type u_6
inst✝² : Monoid S
inst✝¹ : DistribMulAction S M₂
inst✝ : ContinuousConstSMul S M₂
f : M₁ → M₂
c : Sˣ
h : IsCompactOperator (c • f)
⊢ IsCompactOperator f

Tactic:
by simpa using h.smul c⁻¹

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

Goal state before:
pp: case h
E : Type u_5
inst✝¹ : NormedAddCommGroup E
inst✝ : MeasurableSpace E
μ : Measure E
hμ : μ.HasTemperateGrowth
p : ℝ≥0
hp : ↑p ≠ 0
h_one_add : ∀ (x : E), 0 < 1 + ‖x‖
hp_pos : 0 < ↑p
l : ℕ
hl : Integrable (fun x ↦ (1 + ‖x‖) ^ (-↑l)) μ
k : ℕ := ⋯
hlk : ↑l ≤ ↑k * ↑p
⊢ eLpNorm (fun x ↦ (1 + ‖x‖) ^ (-↑k)) (↑p) μ < ∞

Tactic:
suffices HasFiniteIntegral (fun x ↦ ((1 + ‖x‖) ^ (-(k * p) : ℝ))) μ by
        rw [hasFiniteIntegral_iff_enorm] at this
        rw [eLpNorm_lt_top_iff_lintegral_rpow_enorm_lt_top hp ENNReal.coe_ne_top]
        simp only [ENNReal.coe_toReal]
        refine Eq.subst (motive := (∫⁻ x, · x ∂μ < ⊤)) (funext fun x ↦ ?_) this
        rw [← neg_mul, Real.rpow_mul (h_one_add x).le]
        exact Real.enorm_rpow_of_nonneg (by positivity) NNReal.zero_le_coe

Goal state after:
case h
E : Type u_5
inst✝¹ : NormedAddCommGroup E
inst✝ : MeasurableSpace E
μ : Measure E
hμ : μ.HasTemperateGrowth
p : ℝ≥0
hp : ↑p ≠ 0
h_one_add : ∀ (x : E), 0 < 1 + ‖x‖
hp_pos : 0 < ↑p
l : ℕ
hl : Integrable (fun x ↦ (1 + ‖x‖) ^ (-↑l)) μ
k : ℕ := ⌈↑l / ↑p⌉₊
hlk : ↑l ≤ ↑k * ↑p
⊢ HasFiniteIntegral (fun x ↦ (1 + ‖x‖) ^ (-(↑k * ↑p))) μ
Module: Mathlib.Analysis.Matrix.Hermitian

Goal state before:
pp: 𝕜 : Type u_1
n : Type u_3
A : Matrix n n 𝕜
inst✝ : RCLike 𝕜
h : A.IsHermitian
i : n
⊢ ↑(re (A i i)) = A i i

Tactic:
by
  rw [← conj_eq_iff_re, ← star_def, ← conjTranspose_apply, h.eq]

Goal state after:
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 𝕜
hA : A.IsHermitian
h_ne : hA.eigenvalues = 0
this : A = ((Unitary.conjStarAlgAut 𝕜 (Matrix n n 𝕜)) hA.eigenvectorUnitary) (diagonal (RCLike.ofReal ∘ hA.eigenvalues))
⊢ A = 0

Tactic:
rwa [h_ne, Pi.comp_zero, RCLike.ofReal_zero, (by rfl : Function.const n (0 : 𝕜) = fun _ ↦ 0),
      diagonal_zero, map_zero] at this

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
f g : 𝓓^{n}_{K}(E, F)
h : (fun f ↦ f.toFun) f = (fun f ↦ f.toFun) g
⊢ f = g

Tactic:
cases f; cases g; congr

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
⊢ Antitone ((hT.unsortedEigenvalues hn ∘ ⇑(Tuple.sort (hT.unsortedEigenvalues hn))) ∘ ⇑Fin.revPerm)

Tactic:
refine Monotone.comp_antitone ?_ ?_

Goal state after:
case refine_1
𝕜 : 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
⊢ Monotone (hT.unsortedEigenvalues hn ∘ ⇑(Tuple.sort (hT.unsortedEigenvalues hn)))

case refine_2
𝕜 : 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
⊢ Antitone ⇑Fin.revPerm
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
⊢ Antitone (hT.eigenvalues hn)

Tactic:
by
  rw [eigenvalues_def, ← Function.comp_assoc]
  refine Monotone.comp_antitone ?_ ?_
  · apply Tuple.monotone_sort
  intro _ _ h
  exact Fin.rev_le_rev.mpr h

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 : ℕ∞
K : Compacts E
f : 𝓓^{n}_{K}(E, F)
hk : k + 1 ≤ n
⊢ ⇑((fderivLM 𝕜 n k) f) = fderiv ℝ ⇑f

Tactic:
simp [hk]

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

Goal state before:
pp: 𝕜 : Type u_1
n : Type u_2
inst✝¹ : RCLike 𝕜
inst✝ : Fintype n
X : Matrix n n 𝕜
hX : IsSelfAdjoint X
hA : 0 ≤ X * X
⊢ ∃ s, X * X = star s * s

Tactic:
exact ⟨X, hX.star_eq.symm ▸ rfl⟩

Goal state after:
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₃
B : F₁ →L[𝕜] F₂ →L[𝕜] F₃
μ : Measure E
φ : E → F₂
hφ : IntegrableOn φ (↑K) μ
f : 𝓓^{n}_{K}(E, F₁)
⊢ Integrable (fun x ↦ (B (f x)) (φ x)) μ

Tactic:
suffices IntegrableOn (fun x ↦ B (f x) (φ x)) K μ by
    rwa [integrableOn_iff_integrable_of_support_subset] at this
    refine subset_trans ?_ f.support_subset
    exact fun x hx hfx ↦ hx (by simp [hfx])
  rw [IntegrableOn, ← memLp_one_iff_integrable] at hφ ⊢
  exact B.memLp_of_bilin 1 f.memLp_top hφ

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 α
inst✝¹ : NormedSpace ℝ E
inst✝ : μ.WeaklyRegular
f : α → E
ε : ℝ≥0∞
hε : ε ≠ 0
hf : MemLp f 1 μ
⊢ ∃ g, eLpNorm (fun x ↦ f x - g x) 1 μ ≤ ε ∧ MemLp (⇑g) 1 μ

Tactic:
exact hf.exists_boundedContinuous_eLpNorm_sub_le ENNReal.one_ne_top hε

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

Goal state before:

Tactic:
_ = ∑' i, ⟪(f₁ + f₂) i, g i⟫ := ?_
        _ = ∑' i, (⟪f₁ i, g i⟫ + ⟪f₂ i, g i⟫) := by
          simp only [inner_add_left, Pi.add_apply, coeFn_add]
        _ = (∑' i, ⟪f₁ i, g i⟫) + ∑' i, ⟪f₂ i, g i⟫ := Summable.tsum_add ?_ ?_
        _ = _ := by congr

Goal state after:
case calc_1
ι : Type u_1
𝕜 : Type u_2
inst✝⁴ : RCLike 𝕜
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
G : ι → Type u_4
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)
f₁ f₂ g : ↥(lp G 2)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

case calc_2
ι : Type u_1
𝕜 : Type u_2
inst✝⁴ : RCLike 𝕜
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
G : ι → Type u_4
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)
f₁ f₂ g : ↥(lp G 2)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

case calc_3
ι : Type u_1
𝕜 : Type u_2
inst✝⁴ : RCLike 𝕜
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
G : ι → Type u_4
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)
f₁ f₂ g : ↥(lp G 2)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Module: Mathlib.Analysis.Fourier.AddCircle

Goal state before:
pp: T : ℝ
n : ℤ
⊢ Complex.exp 0 = 1

Tactic:
Complex.exp_zero

Goal state after:
T : ℝ
n : ℤ
⊢ 1 = 1
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
G : ι → Type u_4
inst✝³ : (i : ι) → NormedAddCommGroup (G i)
inst✝² : (i : ι) → InnerProductSpace 𝕜 (G i)
inst✝¹ : CompleteSpace E
V : (i : ι) → G i →ₗᵢ[𝕜] E
hV : OrthogonalFamily 𝕜 G V
inst✝ : ∀ (i : ι), CompleteSpace (G i)
⊢ hV.linearIsometry.range = (⨆ i, (V i).range).topologicalClosure

Tactic:
refine le_antisymm ?_ ?_

Goal state after:
case refine_1
ι : Type u_1
𝕜 : Type u_2
inst✝⁶ : RCLike 𝕜
E : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace 𝕜 E
G : ι → Type u_4
inst✝³ : (i : ι) → NormedAddCommGroup (G i)
inst✝² : (i : ι) → InnerProductSpace 𝕜 (G i)
inst✝¹ : CompleteSpace E
V : (i : ι) → G i →ₗᵢ[𝕜] E
hV : OrthogonalFamily 𝕜 G V
inst✝ : ∀ (i : ι), CompleteSpace (G i)
⊢ hV.linearIsometry.range ≤ (⨆ i, (V i).range).topologicalClosure

case refine_2
ι : Type u_1
𝕜 : Type u_2
inst✝⁶ : RCLike 𝕜
E : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace 𝕜 E
G : ι → Type u_4
inst✝³ : (i : ι) → NormedAddCommGroup (G i)
inst✝² : (i : ι) → InnerProductSpace 𝕜 (G i)
inst✝¹ : CompleteSpace E
V : (i : ι) → G i →ₗᵢ[𝕜] E
hV : OrthogonalFamily 𝕜 G V
inst✝ : ∀ (i : ι), CompleteSpace (G i)
⊢ (⨆ i, (V i).range).topologicalClosure ≤ hV.linearIsometry.range
Module: Mathlib.Analysis.Fourier.AddCircle

Goal state before:
pp: case hφ2
T : ℝ
hT : Fact (0 < T)
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : AddCircle T → E
hf : Integrable f haarAddCircle
n : ℤ
t : AddCircle T
⊢ ‖(fourier n) t‖ ≤ 1

Tactic:
rw [fourier_apply, Circle.norm_coe]

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

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
a b : ℝ
f : ℝ → E
n : ℤ
hab : a < b
this : Fact (0 < b - a)
⊢ fourierCoeff (liftIoc (b - a) a f) n = (1 / (b - a)) • ∫ (x : ℝ) in a..b, (fourier (-n)) ↑x • f x

Tactic:
fourierCoeff_eq_intervalIntegral _ _ a,

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
a b : ℝ
f : ℝ → E
n : ℤ
hab : a < b
this : Fact (0 < b - a)
⊢ (1 / (b - a)) • ∫ (x : ℝ) in a..a + (b - a), (fourier (-n)) ↑x • liftIoc (b - a) a f ↑x =
    (1 / (b - a)) • ∫ (x : ℝ) in a..b, (fourier (-n)) ↑x • f x
Module: Mathlib.Analysis.Fourier.AddCircle

Goal state before:
pp: T : ℝ
hT : Fact (0 < T)
a : ℝ
f : ℝ → ℂ
n : ℤ
⊢ fourierCoeff (liftIco T a f) n = (1 / (a + T - a)) • ∫ (x : ℝ) in a..a + T, (fourier (-n)) ↑x • f x

Tactic:
fourierCoeff_eq_intervalIntegral _ _ a,

Goal state after:
T : ℝ
hT : Fact (0 < T)
a : ℝ
f : ℝ → ℂ
n : ℤ
⊢ (1 / T) • ∫ (x : ℝ) in a..a + T, (fourier (-n)) ↑x • liftIco T a f ↑x =
    (1 / (a + T - a)) • ∫ (x : ℝ) in a..a + T, (fourier (-n)) ↑x • f x
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
y : W
⊢ ((-2 * ↑π * I * ↑(𝐞 (-(L v) w))) • ofRealCLM ∘SL L v) y =
    (ContinuousLinearMap.toSpanSingleton ℝ (2 * ↑π * I * ↑(𝐞 (-(L v) w))) ∘SL (-L v)) y

Tactic:
simp only [neg_mul, neg_smul, neg_apply, smul_apply, ContinuousLinearMap.comp_apply,
    ofRealCLM_apply, smul_eq_mul, ContinuousLinearMap.comp_neg,
    ContinuousLinearMap.toSpanSingleton_apply, real_smul, neg_inj]

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)) * ↑((L v) y) = ↑((L v) y) * (2 * ↑π * I * ↑(𝐞 (-(L v) w)))
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)
h : (fun f ↦ f.toFun) f = (fun f ↦ f.toFun) g
⊢ f = g

Tactic:
cases f; cases g; congr

Goal state after:
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
inst✝² : SecondCountableTopologyEither V (W →L[ℝ] ℝ)
inst✝¹ : MeasurableSpace V
inst✝ : BorelSpace V
L : V →L[ℝ] W →L[ℝ] ℝ
f : V → E
μ : Measure V
hf : AEStronglyMeasurable f μ
⊢ AEStronglyMeasurable (fun i ↦ (L i).smulRight (f i)) μ

Tactic:
have aux0 : Continuous fun p : (W →L[ℝ] ℝ) × E ↦ p.1.smulRight p.2 :=
    (ContinuousLinearMap.smulRightL ℝ W E).continuous₂

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
inst✝² : SecondCountableTopologyEither V (W →L[ℝ] ℝ)
inst✝¹ : MeasurableSpace V
inst✝ : BorelSpace V
L : V →L[ℝ] W →L[ℝ] ℝ
f : V → E
μ : Measure V
hf : AEStronglyMeasurable f μ
aux0 : Continuous[instTopologicalSpaceProd, _] fun p ↦ p.1.smulRight p.2
⊢ AEStronglyMeasurable (fun i ↦ (L i).smulRight (f i)) μ
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✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAlgebra ℝ 𝕜
inst✝⁴ : NormedAddCommGroup D
inst✝³ : NormedSpace ℝ D
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace ℝ G
inst✝ : NormedSpace 𝕜 F
L : E →L[ℝ] G →L[ℝ] ℝ
⊢ ∀ (f g : 𝓢(E, F)) (x : E), (L x).smulRight ((f + g) x) = (L x).smulRight (f x) + (L x).smulRight (g x)

Tactic:
intros; ext; simp

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

Goal state before:

Tactic:
0 < μ (u ∩ interior s) :=
      (u_open.inter isOpen_interior).measure_pos μ (_root_.mem_closure_iff.1 h₀ u u_open x₀_u)
    _ ≤ μ (u ∩ s) := by gcongr; apply interior_subset

Goal state after:
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
inst✝² : MeasurableSpace V
inst✝¹ : BorelSpace V
μ : Measure V
inst✝ : SecondCountableTopology V
N : ℕ∞
hf : ∀ (n : ℕ), ↑n ≤ N → Integrable (fun v ↦ ‖v‖ ^ n * ‖f v‖) μ
h'f : ¬Integrable f μ
w : W
⊢ fourierIntegral 𝐞 μ (ContinuousLinearMap.toLinearMap₁₂ L) f w = 0 w

Tactic:
simp [fourierIntegral, integral, h'f]

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

Goal state before:
pp: case hf.hf
𝕜 : Type u_1
inst✝²² : CommRing 𝕜
V : Type u_2
inst✝²¹ : AddCommGroup V
inst✝²⁰ : Module 𝕜 V
inst✝¹⁹ : MeasurableSpace V
W : Type u_3
inst✝¹⁸ : AddCommGroup W
inst✝¹⁷ : Module 𝕜 W
E : Type u_4
F : Type u_5
G : Type u_6
inst✝¹⁶ : NormedAddCommGroup E
inst✝¹⁵ : NormedSpace ℂ E
inst✝¹⁴ : NormedAddCommGroup F
inst✝¹³ : NormedSpace ℂ F
inst✝¹² : NormedAddCommGroup G
inst✝¹¹ : NormedSpace ℂ G
inst✝¹⁰ : TopologicalSpace 𝕜
inst✝⁹ : IsTopologicalRing 𝕜
inst✝⁸ : TopologicalSpace V
inst✝⁷ : BorelSpace V
inst✝⁶ : TopologicalSpace W
inst✝⁵ : MeasurableSpace W
inst✝⁴ : BorelSpace W
e : AddChar 𝕜 𝕊
μ : Measure V
L : V →ₗ[𝕜] W →ₗ[𝕜] 𝕜
ν : Measure W
inst✝³ : SigmaFinite μ
inst✝² : SigmaFinite ν
inst✝¹ : SecondCountableTopologyEither W V
σ : ℂ →+* ℂ
inst✝ : RingHomIsometric σ
f : V → E
g : W → F
M : F →L[ℂ] E →SL[σ] G
he : Continuous[inst✝¹⁰, _] ⇑e
hL : Continuous[instTopologicalSpaceProd, inst✝¹⁰] fun p ↦ (L p.1) p.2
hf : Integrable f μ
hg : Integrable g ν
this : Integrable (fun p ↦ ‖M‖ * (‖g p.1‖ * ‖f p.2‖)) (ν.prod μ)
A : AEStronglyMeasurable (fun p ↦ e (-(L p.2) p.1) • f p.2) (ν.prod μ)
A' : AEStronglyMeasurable (fun p ↦ (g p.1, e (-(L p.2) p.1) • f p.2)) (ν.prod μ)
hM : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun q ↦ (M q.1) q.2
⊢ AEStronglyMeasurable (fun p ↦ (M (g p.1)) (e (-(L p.2) p.1) • f p.2)) (ν.prod μ)

Tactic:
apply hM.comp_aestronglyMeasurable A'

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✝² : RCLike 𝕜
inst✝¹ : NormedSpace 𝕜 F
inst✝ : SMulCommClass ℝ 𝕜 F
⊢ ∀ (f g : 𝓢(E, F)), (f + g).toBoundedContinuousFunction = f.toBoundedContinuousFunction + g.toBoundedContinuousFunction

Tactic:
intros; ext; 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✝² : RCLike 𝕜
inst✝¹ : NormedSpace 𝕜 F
inst✝ : SMulCommClass ℝ 𝕜 F
⊢ ∀ (a : 𝕜) (f : 𝓢(E, F)), (a • f).toBoundedContinuousFunction = (RingHom.id 𝕜) a • f.toBoundedContinuousFunction

Tactic:
intros; ext; 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✝³ : ProperSpace E
inst✝² : RCLike 𝕜
inst✝¹ : NormedSpace 𝕜 F
inst✝ : SMulCommClass ℝ 𝕜 F
⊢ ∀ (f g : 𝓢(E, F)), (f + g).toZeroAtInfty = f.toZeroAtInfty + g.toZeroAtInfty

Tactic:
intros; ext; 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✝³ : ProperSpace E
inst✝² : RCLike 𝕜
inst✝¹ : NormedSpace 𝕜 F
inst✝ : SMulCommClass ℝ 𝕜 F
⊢ ∀ (a : 𝕜) (f : 𝓢(E, F)), (a • f).toZeroAtInfty = (RingHom.id 𝕜) a • f.toZeroAtInfty

Tactic:
intros; ext; simp

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

Goal state before:
pp: E : Type u_5
F : Type u_6
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : MeasurableSpace E
inst✝¹ : OpensMeasurableSpace E
inst✝ : SecondCountableTopologyEither E F
f : 𝓢(E, F)
p : ℝ≥0∞
μ : Measure E
hp₁ : p ≠ 0
hp₂ : p ≠ ∞
hμ : μ.HasTemperateGrowth
⊢ ‖f.toLp p μ‖ = (∫ (x : E), ‖f x‖ ^ p.toReal ∂μ) ^ p.toReal⁻¹

Tactic:
by
  rw [norm_toLp, MeasureTheory.MemLp.eLpNorm_eq_integral_rpow_norm hp₁ hp₂ (f.memLp p μ),
    ENNReal.toReal_ofReal (by positivity)]

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

Goal state before:
pp: case inl
s : ℝ
h : IntegrableOn (fun x ↦ x ^ s) (Ioi 0) volume
hs : s ≤ -1
⊢ False

Tactic:
have : IntegrableOn (fun x ↦ x ^ s) (Ioo (0 : ℝ) 1) := h.mono Ioo_subset_Ioi_self le_rfl
    rw [integrableOn_Ioo_rpow_iff zero_lt_one] at this
    exact hs.not_gt this

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
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) μ
h_map_neg : Measure.map Neg.neg (μ.restrict (Ici 0)) = μ.restrict (Iic 0)
⊢ IntegrableOn f (Iic 0) μ

Tactic:
rw [IntegrableOn, ← h_map_neg, measurableEmbedding_neg.integrable_map_iff]

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) μ
h_map_neg : Measure.map Neg.neg (μ.restrict (Ici 0)) = μ.restrict (Iic 0)
⊢ Integrable (f ∘ Neg.neg) (μ.restrict (Ici 0))
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic

Goal state before:
pp: s : ℝ
this : ∀ (r : ℝ), ↑r = ↑r
| ↑(∫ (x : ℝ) in Ioi 0, rexp (-x) * x ^ (s - 1))

Tactic:
← _root_.integral_ofReal

Goal state after:
s : ℝ
this : ∀ (r : ℝ), ↑r = ↑r
| ∫ (x : ℝ) in Ioi 0, ↑(rexp (-x) * x ^ (s - 1))
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic

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

Tactic:
by
  convert! (Gamma_integrand_intervalIntegrable (s + 1) _ hX).neg
  · simp only [ofReal_exp, ofReal_neg, add_sub_cancel_right]; rfl
  · simp only [add_re, one_re]; linarith

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

Goal state before:
pp: s : ℂ
⊢ Gamma ((starRingEnd ℂ) s) = (starRingEnd ℂ) (Gamma s)

Tactic:
by
  suffices ∀ (n : ℕ) (s : ℂ), GammaAux n (conj s) = conj (GammaAux n s) by
    simp [Gamma, this]
  intro n
  induction n with
  | zero => rw [GammaAux]; exact GammaIntegral_conj
  | succ n IH =>
    intro s
    rw [GammaAux]
    dsimp only
    rw [div_eq_mul_inv _ s, map_mul, conj_inv, ← div_eq_mul_inv]
    suffices conj s + 1 = conj (s + 1) by rw [this, IH]
    rw [map_add, map_one]

Goal state after: