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

Goal state before:
pp: 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)
hs₁ : 0 < w₁ i
hs₂ : w₂ i < 0
w₃ : Fin (n + 1) → R := (lineMap w₁ w₂) (w₁ i / (w₁ i - w₂ i))
hp : 0 < w₁ i - w₂ i
hw₃ : ∑ j, w₃ j = 1
h : Sbtw R w₁ w₃ w₂
⊢ Sbtw R ((Finset.affineCombination R Finset.univ s.points) w₁) ((Finset.affineCombination R Finset.univ s.points) w₃)
    ((Finset.affineCombination R Finset.univ s.points) w₂)

Tactic:
rwa [s.independent.injOn_affineCombination_fintypeAffineCoords.sbtw_map_iff
     (mem_fintypeAffineCoords_iff_sum.2 hw₁) (mem_fintypeAffineCoords_iff_sum.2 hw₃)
     (mem_fintypeAffineCoords_iff_sum.2 hw₂)]

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

Goal state before:
pp: α : Type u_1
𝕜 : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
m : MeasurableSpace α
μ : Measure α
p q r : ℝ≥0∞
hpqr : p.HolderTriple q r
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedSpace 𝕜 F
inst✝ : NormedSpace 𝕜 G
B : E →L[𝕜] F →L[𝕜] G
f : ↥(Lp E p μ)
g₁ g₂ : ↥(Lp F q μ)
⊢ holder r B f (g₁ + g₂) = holder r B f g₁ + holder r B f g₂

Tactic:
by
  simp only [holder, ← MemLp.toLp_add]
  apply MemLp.toLp_congr
  filter_upwards [AEEqFun.coeFn_add g₁.val g₂.val] with x hx
  simp [hx]

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

Goal state before:
pp: α : Type u_1
𝕜 : Type u_3
E : Type u_4
m : MeasurableSpace α
μ : Measure α
p q r : ℝ≥0∞
hpqr : p.HolderTriple q r
inst✝³ : NormedRing 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : IsBoundedSMul 𝕜 E
f : ↥(Lp 𝕜 p μ)
g : ↥(Lp E q μ)
⊢ f • -g = -(f • g)

Tactic:
by
  simp [eq_neg_iff_add_eq_zero, ← Lp.add_smul]

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

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
f : α → ℝ
μ : Measure α
f_nn : 0 ≤ᵐ[μ] f
f_mble : AEMeasurable f μ
⊢ ∫⁻ (ω : α), ENNReal.ofReal (f ω) ∂μ = ∫⁻ (t : ℝ) in Ioi 0, μ {a | t < f a}

Tactic:
by
  rw [lintegral_eq_lintegral_meas_le μ f_nn f_mble]
  apply lintegral_congr_ae
  filter_upwards [meas_le_ae_eq_meas_lt μ (volume.restrict (Ioi 0)) f]
    with t ht
  rw [ht]

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

Goal state before:
pp: ι : Type u_1
E : Type u_5
F : Type u_6
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : ι → E → F
s : Finset ι
hf : ∀ i ∈ s, HasTemperateGrowth (f i)
⊢ HasTemperateGrowth fun x ↦ ∑ i ∈ s, f i x

Tactic:
classical
  induction s using Finset.induction_on with
  | empty => simp
  | insert a s has ih =>
    obtain ⟨hf, h⟩ := by simpa using! hf
    simpa [has] using! hf.add (ih h)

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 𝕜
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)

Tactic:
simp only [conjStarAlgAut_star_apply, toLpLin_apply, OrthonormalBasis.coe_toBasis,
    EuclideanSpace.basisFun_apply, PiLp.ofLp_single, ← mulVec_mulVec,
    eigenvectorUnitary_mulVec, ← mulVec_mulVec, mulVec_eigenvectorBasis,
    Matrix.diagonal_mulVec_single, mulVec_smul, star_eigenvectorUnitary_mulVec,
    RCLike.real_smul_eq_coe_smul (K := 𝕜), WithLp.toLp_smul, PiLp.toLp_single,
    Function.comp_apply, mul_one]

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
⊢ ↑(hA.eigenvalues i) • PiLp.single 2 i 1 = PiLp.single 2 i ↑(hA.eigenvalues i)
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
K : Compacts E
C : ℝ
hC : 0 ≤ C
i : ℕ
f : 𝓓_{K}(E, F)
⊢ (ContDiffMapSupportedIn.seminorm 𝕜 E F ⊤ K i) f ≤ C ↔ ∀ x ∈ K, ‖iteratedFDeriv ℝ i (⇑f) x‖ ≤ C

Tactic:
ContDiffMapSupportedIn.seminorm_le_iff 𝕜 hC,

Goal state after:
𝕜 : 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
K : Compacts E
C : ℝ
hC : 0 ≤ C
i : ℕ
f : 𝓓_{K}(E, F)
⊢ (↑i ≤ ⊤ → ∀ x ∈ K, ‖iteratedFDeriv ℝ i (⇑f) x‖ ≤ C) ↔ ∀ x ∈ K, ‖iteratedFDeriv ℝ i (⇑f) x‖ ≤ C
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, ∑ j, (starRingEnd 𝕜) (x i) * y j * ⟪v i, v j⟫_𝕜 = ⟪∑ i, x i • v i, ∑ i, y i • v i⟫_𝕜

Tactic:
simp_rw [sum_inner, inner_sum, inner_smul_left, inner_smul_right, mul_assoc]

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✝ : Finite n
v : n → E
this : Fintype n
x : n → 𝕜
⊢ 0 ≤ star x ⬝ᵥ gram 𝕜 v *ᵥ x

Tactic:
rw [star_dotProduct_gram_mulVec, le_iff_re_im]

Goal state after:
E : Type u_1
n : Type u_2
𝕜 : Type u_4
inst✝³ : RCLike 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : Finite n
v : n → E
this : Fintype n
x : n → 𝕜
⊢ re 0 ≤ re ⟪∑ i, x i • v i, ∑ i, x i • v i⟫_𝕜 ∧ im 0 = im ⟪∑ i, x i • v i, ∑ i, x i • v i⟫_𝕜
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, star (c x) * gram 𝕜 (⇑f ∘ v) x y * c y = ↑‖f (∑ x ∈ c.support, c x • v x)‖ ^ 2

Tactic:
simp [← inner_self_eq_norm_sq_to_K, inner_sum, sum_inner, inner_smul_left, inner_smul_right,
      Finset.mul_sum, Finset.smul_sum, RCLike.real_smul_eq_coe_mul]

Goal state after:
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)⟫_𝕜)
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 →₀ 𝕜
⊢ ‖f‖ ^ 2 • ↑‖∑ i ∈ c.support, c i • v i‖ ^ 2 =
    ∑ y ∈ c.support, ∑ x ∈ c.support, star (c x) * ‖f‖ ^ 2 • gram 𝕜 v x y * c y

Tactic:
simp [← inner_self_eq_norm_sq_to_K, inner_sum, sum_inner, inner_smul_left, inner_smul_right,
      Finset.mul_sum, Finset.smul_sum, RCLike.real_smul_eq_coe_mul]

Goal state after:
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
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 (min j j + 1)) x - (P (min j (j + 1))) x - ((P (min (j + 1) j)) x - (P (min j j)) x) = (P (j + 1)) x - (P j) x

Tactic:
min_self,

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 (min j (j + 1))) x - ((P (min (j + 1) j)) x - (P j) x) = (P (j + 1)) x - (P j) 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 α
inst✝¹ : NormedSpace ℝ E
inst✝ : μ.WeaklyRegular
f : α → E
ε : ℝ
hε : 0 < ε
hf : MemLp f (ENNReal.ofReal 1) μ
⊢ ∃ g, ∫ (x : α), ‖f x - g x‖ ∂μ ≤ ε ∧ MemLp (⇑g) (ENNReal.ofReal 1) μ

Tactic:
simpa using hf.exists_boundedContinuous_integral_rpow_sub_le zero_lt_one hε

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
β : Type u_3
L : SummationFilter β
b : SchauderBasis 𝕜 X
D : RankOneDecomposition 𝕜 X
coeff : ℕ → X → 𝕜 := D.basisCoeff
hcoeff : ∀ (n : ℕ) (x : X), (succSub D.P n) x = coeff n x • D.e n
n : ℕ
c : 𝕜
x : X
⊢ coeff n (c • x) • D.e n = (c • coeff n x) • D.e n

Tactic:
rw [smul_eq_mul, ← smul_smul, ← hcoeff, ← hcoeff, map_smul]

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

Goal state before:
pp: T : ℝ
hT : Fact (0 < T)
i j : ℤ
h : ¬i = j
⊢ j + -i ≠ 0

Tactic:
exact sub_ne_zero.mpr (Ne.symm h)

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 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
⊢ ∃ δ, δ * ∫ (x : α) in s, ‖g x‖ ∂μ + 2 * δ < ε ∧ 0 < δ ∧ δ < 1

Tactic:
have A :
      Tendsto (fun δ => (δ * ∫ x in s, ‖g x‖ ∂μ) + 2 * δ) (𝓝[>] 0)
        (𝓝 ((0 * ∫ x in s, ‖g x‖ ∂μ) + 2 * 0)) := by
      apply Tendsto.mono_left _ nhdsWithin_le_nhds
      exact (tendsto_id.mul tendsto_const_nhds).add (tendsto_id.const_mul _)

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
A : Tendsto (fun δ ↦ δ * ∫ (x : α) in s, ‖g x‖ ∂μ + 2 * δ) (𝓝[>] 0) (𝓝 (0 * ∫ (x : α) in s, ‖g x‖ ∂μ + 2 * 0))
⊢ ∃ δ, δ * ∫ (x : α) in s, ‖g x‖ ∂μ + 2 * δ < ε ∧ 0 < δ ∧ δ < 1
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
k n : ℕ
f g : 𝓢(E, F)
x : E
⊢ ‖x‖ ^ k * ‖iteratedFDeriv ℝ n (⇑f + ⇑g) x‖ ≤
    ‖x‖ ^ k * ‖iteratedFDeriv ℝ n (⇑f) x‖ + ‖x‖ ^ k * ‖iteratedFDeriv ℝ n (⇑g) x‖

Tactic:
← mul_add

Goal state after:
E : Type u_5
F : Type u_6
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
k n : ℕ
f g : 𝓢(E, F)
x : E
⊢ ‖x‖ ^ k * ‖iteratedFDeriv ℝ n (⇑f + ⇑g) x‖ ≤ ‖x‖ ^ k * (‖iteratedFDeriv ℝ n (⇑f) x‖ + ‖iteratedFDeriv ℝ n (⇑g) x‖)
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
I : ∀ (n : ℕ), IntegrableOn (fun x ↦ c x ^ n) s μ
J : ∀ (n : ℕ), 0 ≤ᵐ[μ.restrict s] fun x ↦ c x ^ n
P : ∀ (n : ℕ), 0 < ∫ (x : α) in s, c x ^ n ∂μ
hiφ : ∀ (n : ℕ), ∫ (x : α) in s, φ n x ∂μ = 1
u : Set α
u_open : IsOpen[inst✝⁶] u
⊢ x₀ ∈ u → TendstoUniformlyOn φ 0 atTop (s \ u)

Tactic:
x₀u

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 μ
J : ∀ (n : ℕ), 0 ≤ᵐ[μ.restrict s] fun x ↦ c x ^ n
P : ∀ (n : ℕ), 0 < ∫ (x : α) in s, c x ^ n ∂μ
hiφ : ∀ (n : ℕ), ∫ (x : α) in s, φ n x ∂μ = 1
u : Set α
u_open : IsOpen[inst✝⁶] u
x₀u : x₀ ∈ u
⊢ TendstoUniformlyOn φ 0 atTop (s \ u)
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[ℝ] ℝ
k n : ℕ
f : 𝓢(E, F)
x : E
⊢ ‖L‖ * 1 * (SchwartzMap.seminorm 𝕜 (k + 1) n) f + ‖L‖ * ↑n * (SchwartzMap.seminorm 𝕜 k (n - 1)) f ≤
    ‖L‖ * ↑(max 1 n) * max ((SchwartzMap.seminorm 𝕜 (k + 1) n) f) ((SchwartzMap.seminorm 𝕜 k (n - 1)) f) +
      ‖L‖ * ↑(max 1 n) * max ((SchwartzMap.seminorm 𝕜 (k + 1) n) f) ((SchwartzMap.seminorm 𝕜 k (n - 1)) f)

Tactic:
gcongr <;> simp

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

Goal state before:
pp: case h
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
inst✝¹ : FiniteDimensional ℝ V
μ : Measure V
inst✝ : μ.IsAddHaarMeasure
K N : ℕ∞
hf : ContDiff ℝ (↑N) f
h'f : ∀ (k n : ℕ), ↑k ≤ K → ↑n ≤ N → Integrable (fun v ↦ ‖v‖ ^ k * ‖iteratedFDeriv ℝ n f v‖) μ
k n : ℕ
hk : ↑k ≤ K
hn : ↑n ≤ N
w : W
I : ∀ p ∈ Finset.range (k + 1) ×ˢ Finset.range (n + 1), Integrable (fun v ↦ ‖v‖ ^ p.1 * ‖iteratedFDeriv ℝ p.2 f v‖) μ
v : V
i : ℕ
hi : i ≤ n
j : ℕ
hj : j ≤ k
⊢ (j, i) ∈ Finset.range (k + 1) ×ˢ Finset.range (n + 1)

Tactic:
simp only [Finset.mem_product, Finset.mem_range_succ_iff]
      exact ⟨hj, hi⟩

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

Goal state before:
pp: a : ℝ
ha : a < 0
c : ℝ
⊢ ∫ (x : ℝ) in Ioi c, RCLike.re (Complex.exp (↑a * ↑x)) = -RCLike.re (Complex.exp (↑a * ↑c)) / a

Tactic:
rw [integral_re, integral_exp_mul_complex_Ioi (by simpa using ha), RCLike.re_to_complex,
    RCLike.re_to_complex, Complex.div_ofReal_re, Complex.neg_re]

Goal state after:
a : ℝ
ha : a < 0
c : ℝ
⊢ Integrable (fun x ↦ Complex.exp (↑a * ↑x)) (volume.restrict (Ioi c))
Module: Mathlib.Analysis.SpecialFunctions.ImproperIntegrals

Goal state before:
pp: a c m : ℝ
ha : a < -1
hc : -m < c
⊢ IntegrableOn (fun x ↦ (x + m) ^ a) (Ioi c) volume

Tactic:
have hd : ∀ x ∈ Ici c, HasDerivAt (fun t ↦ (t + m) ^ (a + 1) / (a + 1)) ((x + m) ^ a) x := by
    intro x hx
    convert! (((hasDerivAt_id _).add_const _).rpow_const _).div_const _ using 1
    · simp [show a + 1 ≠ 0 by linarith]
    left; linarith [mem_Ici.mp hx, id_eq x]

Goal state after:
a c m : ℝ
ha : a < -1
hc : -m < c
hd : ∀ x ∈ Ici c, HasDerivAt (fun t ↦ (t + m) ^ (a + 1) / (a + 1)) ((x + m) ^ a) x
⊢ IntegrableOn (fun x ↦ (x + m) ^ a) (Ioi c) volume
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) μ
⊢ Integrable f μ

Tactic:
← integrableOn_univ,

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

Goal state before:
pp: p b : ℝ
hb : 0 < b
hp : 1 < p
⊢ (fun x ↦ rexp (-b * x ^ p)) =o[atTop] fun x ↦ rexp (-x)

Tactic:
rw [isLittleO_exp_comp_exp_comp]

Goal state after:
p b : ℝ
hb : 0 < b
hp : 1 < p
⊢ Tendsto (fun x ↦ -x - -b * x ^ p) atTop atTop
Module: Mathlib.Analysis.SpecialFunctions.PolarCoord

Goal state before:
pp: ⊢ ∀ ⦃x : ℝ × ℝ⦄,
    x ∈ {q | 0 < q.1} ∪ {q | q.2 ≠ 0} →
      ((√(x.1 ^ 2 + x.2 ^ 2), (Complex.equivRealProd.symm x).arg).1 *
            cos (√(x.1 ^ 2 + x.2 ^ 2), (Complex.equivRealProd.symm x).arg).2,
          (√(x.1 ^ 2 + x.2 ^ 2), (Complex.equivRealProd.symm x).arg).1 *
            sin (√(x.1 ^ 2 + x.2 ^ 2), (Complex.equivRealProd.symm x).arg).2) =
        x

Tactic:
rintro ⟨x, y⟩ _
    have A : √(x ^ 2 + y ^ 2) = ‖x + y * Complex.I‖ := by
      rw [Complex.norm_def, Complex.normSq_add_mul_I]
    simp [A]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral

Goal state before:
pp: b : ℝ
hb : 0 < b
s : ℝ
hs : -1 < s
⊢ Integrable (fun x ↦ x ^ s * rexp (-b * x ^ 2)) volume

Tactic:
← integrableOn_univ,

Goal state after:
b : ℝ
hb : 0 < b
s : ℝ
hs : -1 < s
⊢ IntegrableOn (fun x ↦ x ^ s * rexp (-b * x ^ 2)) univ volume
Module: Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform

Goal state before:
pp: case hbc
b : ℂ
hb : 0 < b.re
c✝ T✝ : ℝ
hT✝ : 0 ≤ T✝
T : ℝ
hT : 0 ≤ T
c y : ℝ
hy : |y| ≤ |c|
⊢ y ^ 2 ≤ c ^ 2

Tactic:
rwa [sq_le_sq]

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

Goal state before:
pp: case succ
n : ℕ
IH : Gamma (-↑n) = 0
⊢ Gamma (-↑(n + 1)) = 0

Tactic:
have A : -(n.succ : ℂ) ≠ 0 := by
      rw [neg_ne_zero, Nat.cast_ne_zero]
      apply Nat.succ_ne_zero
    have : -(n : ℂ) = -↑n.succ + 1 := by simp
    rw [this, Gamma_add_one _ A] at IH
    contrapose! IH
    exact mul_ne_zero A IH

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

Goal state before:
pp: s : ℝ
hs : 0 < s
⊢ (↑(∫ (x : ℝ) in Ioi 0, rexp (-x) * x ^ (s - 1))).re = ∫ (x : ℝ) in Ioi 0, rexp (-x) * x ^ (s - 1)

Tactic:
Complex.ofReal_re

Goal state after:
s : ℝ
hs : 0 < s
⊢ ∫ (x : ℝ) in Ioi 0, rexp (-x) * x ^ (s - 1) = ∫ (x : ℝ) in Ioi 0, rexp (-x) * x ^ (s - 1)
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic

Goal state before:
pp: s : ℝ
hs : s ≠ 0
⊢ Gamma (s + 1) = s * Gamma s

Tactic:
by
  simp_rw [Gamma]
  rw [Complex.ofReal_add, Complex.ofReal_one, Complex.Gamma_add_one, Complex.re_ofReal_mul]
  rwa [Complex.ofReal_ne_zero]

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

Goal state before:
pp: n : ℕ
⊢ (↑↑n !).re = ↑n !

Tactic:
Complex.ofReal_re

Goal state after:
n : ℕ
⊢ ↑n ! = ↑n !
Module: Mathlib.Analysis.Distribution.SchwartzSpace.Fourier

Goal state before:
pp: E : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℂ E
V : Type u_3
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : FiniteDimensional ℝ V
inst✝¹ : MeasurableSpace V
inst✝ : BorelSpace V
f : 𝓢(V, E)
m : V
⊢ ∂_{m} (𝓕 f) = 𝓕 (-(2 * ↑π * Complex.I) • (smulLeftCLM E fun x ↦ inner ℝ x m) f)

Tactic:
by
  change SchwartzMap.evalCLM ℝ V E m (fderivCLM ℝ V E (𝓕 f)) = _
  rw [fderivCLM_fourier_eq, ← fourier_evalCLM_eq]
  congr
  ext
  have : (inner ℝ · m).HasTemperateGrowth := ((innerSL ℝ).flip m).hasTemperateGrowth
  simp [this, innerSL_apply_apply ℝ]

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

Goal state before:
pp: E : Type u_3
F : Type u_4
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : AddCommGroup F
inst✝³ : Module ℂ F
inst✝² : TopologicalSpace F
inst✝¹ : IsTopologicalAddGroup F
inst✝ : ContinuousConstSMul ℂ F
g₁ g₂ : E → ℂ
hg₁ : Function.HasTemperateGrowth g₁
hg₂ : Function.HasTemperateGrowth g₂
⊢ smulLeftCLM F (g₁ - g₂) = smulLeftCLM F g₁ - smulLeftCLM F g₂

Tactic:
by
  ext f u
  simp [SchwartzMap.smulLeftCLM_sub hg₁ hg₂]

Goal state after:
Module: Mathlib.GroupTheory.FiniteAbelian.Basic

Goal state before:
pp: case of
ι : Type
inst✝ : DecidableEq ι
p n : ι → ℕ
i : { i // n i ≠ 0 }
x : ZMod (p ↑i ^ n ↑i)
⊢ (DirectSum.toAddMonoid fun i ↦ if h : n i = 0 then 0 else DirectSum.of (fun j ↦ ZMod (p ↑j ^ n ↑j)) ⟨i, h⟩)
      ((DirectSum.toAddMonoid fun i ↦ DirectSum.of (fun i ↦ ZMod (p i ^ n i)) ↑i)
        ((DirectSum.of (fun i ↦ ZMod (p ↑i ^ n ↑i)) i) x)) =
    (DirectSum.of (fun i ↦ ZMod (p ↑i ^ n ↑i)) i) x

Tactic:
DirectSum.toAddMonoid_of,

Goal state after:
case of
ι : Type
inst✝ : DecidableEq ι
p n : ι → ℕ
i : { i // n i ≠ 0 }
x : ZMod (p ↑i ^ n ↑i)
⊢ (DirectSum.toAddMonoid fun i ↦ if h : n i = 0 then 0 else DirectSum.of (fun j ↦ ZMod (p ↑j ^ n ↑j)) ⟨i, h⟩)
      ((DirectSum.of (fun i ↦ ZMod (p i ^ n i)) ↑i) x) =
    (DirectSum.of (fun i ↦ ZMod (p ↑i ^ n ↑i)) i) x