mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Normed.Group.ZeroAtInfty

Goal state before:
pp: E : Type u_1
F : Type u_2
inst✝² : SeminormedAddGroup E
inst✝¹ : SeminormedAddCommGroup F
inst✝ : ProperSpace E
f : E → F
h : ∀ (ε : ℝ), 0 < ε → ∃ r, ∀ (x : E), r < ‖x‖ → ‖f x‖ < ε
⊢ Tendsto f (cocompact E) (𝓝 0)

Tactic:
by
  rw [tendsto_zero_iff_norm_tendsto_zero]
  intro s hs
  rw [mem_map, Metric.mem_cocompact_iff_closedBall_compl_subset 0]
  rw [Metric.mem_nhds_iff] at hs
  rcases hs with ⟨ε, hε, hs⟩
  rcases h ε hε with ⟨r, hr⟩
  use r
  intro
  aesop

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

Goal state before:
pp: 𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst✝¹⁰ : NontriviallyNormedField 𝕜₁
inst✝⁹ : NormedField 𝕜₂
σ₁₂ : 𝕜₁ →+* 𝕜₂
M₁ : Type u_3
M₂ : Type u_4
inst✝⁸ : SeminormedAddCommGroup M₁
inst✝⁷ : AddCommGroup M₂
inst✝⁶ : NormedSpace 𝕜₁ M₁
inst✝⁵ : Module 𝕜₂ M₂
inst✝⁴ : UniformSpace M₂
inst✝³ : IsUniformAddGroup M₂
inst✝² : ContinuousConstSMul 𝕜₂ M₂
inst✝¹ : T2Space M₂
inst✝ : CompleteSpace M₂
u : M₁ →SL[σ₁₂] M₂
hu : ∀ U ∈ 𝓝 0, ∃ y ∈ {f | IsCompactOperator ⇑f}, y - u ∈ U
U : Set M₂
hU : U ∈ 𝓝 0
V : Set M₂
hV : V ∈ 𝓝 0
hVU : ∀ v ∈ V, ∀ w ∈ V, v + w ∈ U
SV : Set M₁ × Set M₂ := (closedBall 0 1, -V)
v : M₁ →SL[σ₁₂] M₂
hv : v ∈ {f | IsCompactOperator ⇑f}
huv : v - u ∈ {f | ∀ x ∈ SV.1, f x ∈ SV.2}
T : Set M₂
hT : T.Finite
hTv : closure[inst✝⁴.toTopologicalSpace] (⇑↑v '' closedBall 0 1) ⊆ ⋃ y ∈ T, y +ᵥ V
x : M₁
hx : x ∈ closedBall 0 1
t : M₂
ht : t ∈ T
htx : v x - t ∈ V
⊢ u x - t = v x - t + -(v - u) x

Tactic:
sub_apply

Goal state after:
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst✝¹⁰ : NontriviallyNormedField 𝕜₁
inst✝⁹ : NormedField 𝕜₂
σ₁₂ : 𝕜₁ →+* 𝕜₂
M₁ : Type u_3
M₂ : Type u_4
inst✝⁸ : SeminormedAddCommGroup M₁
inst✝⁷ : AddCommGroup M₂
inst✝⁶ : NormedSpace 𝕜₁ M₁
inst✝⁵ : Module 𝕜₂ M₂
inst✝⁴ : UniformSpace M₂
inst✝³ : IsUniformAddGroup M₂
inst✝² : ContinuousConstSMul 𝕜₂ M₂
inst✝¹ : T2Space M₂
inst✝ : CompleteSpace M₂
u : M₁ →SL[σ₁₂] M₂
hu : ∀ U ∈ 𝓝 0, ∃ y ∈ {f | IsCompactOperator ⇑f}, y - u ∈ U
U : Set M₂
hU : U ∈ 𝓝 0
V : Set M₂
hV : V ∈ 𝓝 0
hVU : ∀ v ∈ V, ∀ w ∈ V, v + w ∈ U
SV : Set M₁ × Set M₂ := (closedBall 0 1, -V)
v : M₁ →SL[σ₁₂] M₂
hv : v ∈ {f | IsCompactOperator ⇑f}
huv : v - u ∈ {f | ∀ x ∈ SV.1, f x ∈ SV.2}
T : Set M₂
hT : T.Finite
hTv : closure[inst✝⁴.toTopologicalSpace] (⇑↑v '' closedBall 0 1) ⊆ ⋃ y ∈ T, y +ᵥ V
x : M₁
hx : x ∈ closedBall 0 1
t : M₂
ht : t ∈ T
htx : v x - t ∈ V
⊢ u x - t = v x - t + -(v x - u x)
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)
⊢ ∃ d > 0, ∀ᶠ (n : ℕ) in atTop, d ≤ ‖y_ n‖

Tactic:
refine ⟨(‖μ‖ * c) / 2, by positivity, ?_⟩

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)
⊢ ∀ᶠ (n : ℕ) in atTop, ‖μ‖ * c / 2 ≤ ‖y_ n‖
Module: Mathlib.Data.Fin.Tuple.Sort

Goal state before:
pp: case mpr
n : ℕ
α : Type u_1
inst✝ : LinearOrder α
f : Fin n → α
σ : Equiv.Perm (Fin n)
h : StrictMono ⇑(Equiv.trans σ (graphEquiv₁ f))
⊢ σ = sort f

Tactic:
have := Subsingleton.elim (graphEquiv₂ f) (h.orderIsoOfSurjective _ <| Equiv.surjective _)
    ext1 x
    exact (graphEquiv₁ f).eq_symm_apply.2 (DFunLike.congr_fun this x).symm

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
⊢ A.charpoly = ∏ i, (X - C ↑(hA.eigenvalues i))

Tactic:
conv_lhs => rw [hA.spectral_theorem, conjStarAlgAut_apply, charpoly_mul_comm, ← mul_assoc]

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
⊢ (star ↑hA.eigenvectorUnitary * ↑hA.eigenvectorUnitary * diagonal (RCLike.ofReal ∘ hA.eigenvalues)).charpoly =
    ∏ i, (X - C ↑(hA.eigenvalues i))
Module: Mathlib.Analysis.Matrix.Order

Goal state before:
pp: 𝕜 : Type u_1
n : Type u_2
inst✝ : RCLike 𝕜
A : Matrix n n 𝕜
h₁ : A.PosSemidef
h₂ : (-A).PosSemidef
i j : n
hdiag : True
h1 : 0 ≤ A i j * star (A i j) + A i j * star (A i j)
h2 : A i j * star (A i j) + A i j * star (A i j) ≤ 0
⊢ A i j = 0

Tactic:
simpa using le_antisymm h2 h1

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

Goal state before:
pp: 𝕜 : Type u_1
n : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : Fintype n
inst✝ : DecidableEq n
v : n → 𝕜
y : Matrix n n 𝕜
hx : (star y * y).PosSemidef
h : IsUnit (star y * y)
hv : y *ᵥ v = 0
⊢ (yᴴ * y).mulVecLin v = 0

Tactic:
mulVecLin_apply,

Goal state after:
𝕜 : Type u_1
n : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : Fintype n
inst✝ : DecidableEq n
v : n → 𝕜
y : Matrix n n 𝕜
hx : (star y * y).PosSemidef
h : IsUnit (star y * y)
hv : y *ᵥ v = 0
⊢ (yᴴ * y) *ᵥ v = 0
Module: Mathlib.Analysis.InnerProductSpace.GramMatrix

Goal state before:
pp: case inr.inl
E : Type u_1
n : Type u_2
𝕜 : Type u_4
inst✝³ : RCLike 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : DecidableEq n
i : n
x : E
k : n
hik : i ≠ k
⊢ gram 𝕜 (Pi.single i x) i k = single i i (⟪x, x⟫_𝕜) i k

pp: case inr.inr
E : Type u_1
n : Type u_2
𝕜 : Type u_4
inst✝³ : RCLike 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : DecidableEq n
i : n
x : E
⊢ gram 𝕜 (Pi.single i x) i i = single i i (⟪x, x⟫_𝕜) i i

Tactic:
· simp [hik]

Goal state after:
case inr.inr
E : Type u_1
n : Type u_2
𝕜 : Type u_4
inst✝³ : RCLike 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : DecidableEq n
i : n
x : E
⊢ gram 𝕜 (Pi.single i x) i i = single i i (⟪x, x⟫_𝕜) i 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
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
⊢ abs (r • a) = r • abs a

Tactic:
suffices ∀ r : ℝ≥0, abs (r • a) = r • abs a by simpa using this (r • 1)
  intro r
  rw [abs, sqrt_eq_iff _ _ (star_mul_self_nonneg _) (smul_nonneg (by positivity) (abs_nonneg _))]
  simp [mul_smul_comm, smul_mul_assoc, abs_mul_abs]

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
h : MemLp f 2 μ
⊢ Integrable (fun x ↦ f x ^ 2) μ

Tactic:
by
  simpa [← memLp_one_iff_integrable] using h.norm_rpow two_ne_zero ENNReal.ofNat_ne_top

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
E : Type u_2
𝕜 : Type u_3
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
f : α → E
hf : MemLp f p μ
c : E
x : α
⊢ ‖⟪f x, c⟫‖ ≤ ‖c‖ * ‖f x‖

Tactic:
rw [mul_comm]; exact norm_inner_le_norm _ _

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

Goal state before:
pp: case pos
α : Type u_1
inst✝⁶ : TopologicalSpace α
inst✝⁵ : NormalSpace α
inst✝⁴ : MeasurableSpace α
inst✝³ : BorelSpace α
E : Type u_2
inst✝² : NormedAddCommGroup E
μ : Measure α
p : ℝ≥0∞
inst✝¹ : NormedSpace ℝ E
inst✝ : μ.OuterRegular
hp : p ≠ ∞
s u : Set α
s_closed : IsClosed[inst✝⁶] s
u_open : IsOpen[inst✝⁶] u
hsu : s ⊆ u
hs : μ s ≠ ∞
c : E
ε : ℝ≥0∞
hε : ε ≠ 0
η : ℝ≥0
η_pos : 0 < η
hη : ∀ (s : Set α), μ s ≤ ↑η → eLpNorm (s.indicator fun _x ↦ c) p μ ≤ ε
ηpos : 0 < ↑η
V : Set α
sV : V ⊇ s
V_open : IsOpen[inst✝⁶] V
h'V : μ V < ∞
hV : μ (V \ s) < ↑η
v : Set α := u ∩ V
hsv : s ⊆ v
hμv : μ v < ∞
g : C(α, ℝ)
hgv : EqOn (⇑g) 0 (u ∩ V)ᶜ
hgs : EqOn (⇑g) 1 s
hg_range : ∀ (x : α), g x ∈ Icc 0 1
g_norm : ∀ (x : α), ‖g x‖ = g x
gc_bd0 : ∀ (x : α), ‖g x • c‖ ≤ ‖c‖
gc_bd : ∀ (x : α), ‖g x • c - s.indicator (fun _x ↦ c) x‖ ≤ ‖(v \ s).indicator (fun _x ↦ c) x‖
gc_support : (Function.support fun x ↦ g x • c) ⊆ v
this : eLpNorm (v.indicator fun _x ↦ 1) p μ < ∞
x : α
hx : x ∈ v
⊢ ‖g x‖ ≤ ‖v.indicator (fun _x ↦ 1) x‖

Tactic:
simp only [hx, abs_of_nonneg (hg_range x).1, (hg_range x).2, Real.norm_eq_abs,
        indicator_of_mem, CStarRing.norm_one]

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

Goal state before:
pp: T : ℝ
n : ℤ
⊢ (fourier n) 0 = 1

Tactic:
by
  rw [← QuotientAddGroup.mk_zero, fourier_coe_apply, Complex.ofReal_zero, mul_zero,
    zero_div, Complex.exp_zero]

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

Goal state before:
pp: T : ℝ
n : ℤ
x : AddCircle T
⊢ (fourier (-n)) x = (starRingEnd ℂ) ((fourier n) x)

Tactic:
induction x using QuotientAddGroup.induction_on
  simp_rw [fourier_apply, toCircle]
  rw [← QuotientAddGroup.mk_zsmul, ← QuotientAddGroup.mk_zsmul]
  simp_rw [Function.Periodic.lift_coe, ← Circle.coe_inv_eq_conj, ← Circle.exp_neg,
    neg_smul, mul_neg]

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

Goal state before:
pp: T : ℝ
hT : Fact (0 < T)
⊢ fourierSubalgebra.SeparatesPoints

Tactic:
by
  intro x y hxy
  refine ⟨_, ⟨fourier 1, subset_adjoin ⟨1, rfl⟩, rfl⟩, ?_⟩
  dsimp only; rw [fourier_one, fourier_one]
  contrapose hxy
  rw [Subtype.coe_inj] at hxy
  exact injective_toCircle hT.elim.ne' hxy

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

Goal state before:
pp: case e'_9
T : ℝ
hT : Fact (0 < T)
p : ℝ≥0∞
inst✝ : Fact (1 ≤ p)
hp : p ≠ ∞
e_3✝ : Complex.instSemiring = NormedField.toNormedCommRing.toSemiring
e_6✝ : Lp.instModule ≍ Lp.instModule
⊢ span ℂ (range (fourierLp p)) = Submodule.map (↑(toLp p haarAddCircle ℂ)) (span ℂ (range fourier))

Tactic:
map_span

Goal state after:
case e'_9
T : ℝ
hT : Fact (0 < T)
p : ℝ≥0∞
inst✝ : Fact (1 ≤ p)
hp : p ≠ ∞
e_3✝ : Complex.instSemiring = NormedField.toNormedCommRing.toSemiring
e_6✝ : Lp.instModule ≍ Lp.instModule
⊢ span ℂ (range (fourierLp p)) = span ℂ (⇑↑(toLp p haarAddCircle ℂ) '' range fourier)
Module: Mathlib.Analysis.Fourier.AddCircle

Goal state before:
pp: T : ℝ
n : ℤ
x : ℝ
⊢ HasDerivAt (fun y ↦ 2 * ↑π * I * ↑n * y / ↑T) (2 * ↑π * I * ↑n / ↑T) ↑x

Tactic:
convert! hasDerivAt_mul_const (2 * ↑π * I * ↑n / T) using 1

Goal state after:
case e'_8
T : ℝ
n : ℤ
x : ℝ
⊢ (fun y ↦ 2 * ↑π * I * ↑n * y / ↑T) = fun x ↦ x * (2 * ↑π * I * ↑n / ↑T)
Module: Mathlib.Analysis.Distribution.SchwartzSpace.Basic

Goal state before:
pp: 𝕜 : Type u_2
E : Type u_5
F : Type u_6
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : NormedField 𝕜
inst✝¹ : NormedSpace 𝕜 F
inst✝ : SMulCommClass ℝ 𝕜 F
f : 𝓢(E, F)
k : ℕ
x₀ : E
⊢ ‖x₀‖ ^ k * ‖f x₀‖ ≤ (SchwartzMap.seminorm 𝕜 k 0) f

Tactic:
have := SchwartzMap.le_seminorm 𝕜 k 0 f x₀
  rwa [norm_iteratedFDeriv_zero] at this

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✝³ : NormedAddCommGroup G
inst✝² : NormedSpace ℝ G
inst✝¹ : NormedSpace 𝕜 G
inst✝ : SMulCommClass ℝ 𝕜 G
m : F
⊢ ∀ (n : ℕ × ℕ),
    ∃ s C,
      0 ≤ C ∧
        ∀ (f : 𝓢(E, F →L[ℝ] G)) (x : E),
          ‖x‖ ^ n.1 * ‖iteratedFDeriv ℝ n.2 (fun x ↦ (f x) m) x‖ ≤
            C * (s.sup (schwartzSeminormFamily 𝕜 E (F →L[ℝ] G))) f

Tactic:
by
  rintro ⟨k, n⟩
  use {(k, n)}, ‖m‖, norm_nonneg _
  intro f x
  simp only [Finset.sup_singleton, schwartzSeminormFamily_apply]
  calc
    ‖x‖ ^ k * ‖iteratedFDeriv ℝ n (f · m) x‖ ≤ ‖x‖ ^ k * (‖m‖ * ‖iteratedFDeriv ℝ n f x‖) := by
      gcongr
      exact norm_iteratedFDeriv_clm_apply_const (f.smooth _).contDiffAt le_rfl
    _ ≤ ‖m‖ * SchwartzMap.seminorm 𝕜 k n f := by
      move_mul [‖m‖]
      gcongr
      apply le_seminorm

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

Goal state before:

Tactic:
_ ≤ ‖x‖ ^ k * ∑ i ∈ Finset.range (n + 1), (n.choose i) *
            ‖iteratedFDeriv ℝ i L x‖ * ‖iteratedFDeriv ℝ (n - i) f x‖ := by
          gcongr 1
          exact norm_iteratedFDeriv_le_of_bilinear_of_le_one (smulRightL ℝ G F)
            (by fun_prop) (f.smooth ⊤) x (mod_cast le_top) norm_smulRightL_le
        _ ≤ ‖x‖ ^ k *
            (‖L x‖ * ‖iteratedFDeriv ℝ n f x‖ + n * ‖L‖ * ‖iteratedFDeriv ℝ (n - 1) f x‖) := by
          gcongr 1
          rw [Finset.sum_range_succ', add_comm]
          cases n with
          | zero => simp
          | succ n =>
            have : ∑ k ∈ Finset.range n,
                (((n + 1).choose (k + 1 + 1)) : ℝ) * ‖iteratedFDeriv ℝ (k + 1 + 1) L x‖ *
                ‖iteratedFDeriv ℝ (n + 1 - (k + 1 + 1)) f x‖ = 0 := by
              apply Finset.sum_eq_zero
              simp [iteratedFDeriv_succ_eq_comp_right, iteratedFDeriv_succ_const]
            simp [Finset.sum_range_succ', this]
        _ = ‖x‖ ^ k * ‖L x‖ * ‖iteratedFDeriv ℝ n f x‖ +
              ‖x‖ ^ k * n * ‖L‖ * ‖iteratedFDeriv ℝ (n - 1) f x‖ := by ring
        _ ≤ ‖L‖ * 1 * (SchwartzMap.seminorm 𝕜 (k + 1) n) f +
              ‖L‖ * n * (SchwartzMap.seminorm 𝕜 k (n - 1) f) := by
          grw [le_opNorm, ← le_seminorm 𝕜 (k + 1) n f x, ← le_seminorm 𝕜 k (n - 1) f x]
          apply le_of_eq
          ring
        _ ≤ ‖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) := by
          gcongr <;> simp
        _ = _ := by
          simp only [Finset.sup_insert, schwartzSeminormFamily_apply, Finset.sup_singleton,
            Seminorm.coe_sup, Pi.sup_apply]
          ring

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

Goal state before:
pp: α : Type u_1
inst✝¹ : MeasurableSpace α
μ : Measure α
f g : α → ℝ
s : Set α
inst✝ : SigmaFinite μ
f_int : IntegrableOn f s μ
g_int : IntegrableOn g s μ
hs : MeasurableSet s
hfg : f ≤ᵐ[μ.restrict s] g
⊢ (μ.prod volume) (regionBetween f g s) = ENNReal.ofReal (∫ (y : α) in s, (g - f) y ∂μ)

Tactic:
by
  have h : g - f =ᵐ[μ.restrict s] fun x => Real.toNNReal (g x - f x) :=
    hfg.mono fun x hx => (Real.coe_toNNReal _ <| sub_nonneg.2 hx).symm
  rw [volume_regionBetween_eq_lintegral f_int.aemeasurable g_int.aemeasurable hs,
    integral_congr_ae h, lintegral_congr_ae,
    lintegral_coe_eq_integral _ ((integrable_congr h).mp (g_int.sub f_int))]
  rfl

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

Goal state before:
pp: c y : ℝ
x✝ : y ∈ Iic 0
⊢ ∫ (x : ℝ) in id y..c, ‖rexp x‖ ≤ rexp c

Tactic:
simp_rw [norm_of_nonneg (exp_pos _).le, integral_exp, sub_le_self_iff]

Goal state after:
c y : ℝ
x✝ : y ∈ Iic 0
⊢ 0 ≤ rexp (id y)
Module: Mathlib.Analysis.SpecialFunctions.ImproperIntegrals

Goal state before:
pp: case e'_9
a c m : ℝ
ha : a < -1
hc : -m < c
x : ℝ
hx : x ∈ Ici c
⊢ (x + m) ^ a = 1 * (a + 1) * (id x + m) ^ (a + 1 - 1) / (a + 1)

pp: case convert_3
a c m : ℝ
ha : a < -1
hc : -m < c
x : ℝ
hx : x ∈ Ici c
⊢ id x + m ≠ 0 ∨ 1 ≤ a + 1

Tactic:
· simp [show a + 1 ≠ 0 by linarith]

Goal state after:
case convert_3
a c m : ℝ
ha : a < -1
hc : -m < c
x : ℝ
hx : x ∈ Ici c
⊢ id x + m ≠ 0 ∨ 1 ≤ a + 1
Module: Mathlib.Analysis.SpecialFunctions.ImproperIntegrals

Goal state before:
pp: a : ℂ
ha : a.re < -1
c : ℝ
hc : 0 < c
⊢ IntegrableOn (fun t ↦ ↑t ^ a) (Ioi c) volume

Tactic:
by
  refine (integrable_norm_iff ?_).mp <| integrableOn_Ioi_norm_cpow_of_lt ha hc
  refine ContinuousOn.aestronglyMeasurable (fun t ht ↦ ?_) measurableSet_Ioi
  exact (Complex.continuousAt_ofReal_cpow_const _ _ (Or.inr (hc.trans ht).ne')).continuousWithinAt

Goal state after:
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:
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.Gaussian.GaussianIntegral

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

Tactic:
by
  simpa using integrable_rpow_mul_exp_neg_mul_sq hb (by simp : (-1 : ℝ) < 0)

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

Goal state before:
pp: b : ℝ
h : IntegrableOn (fun x ↦ rexp (-b * x ^ 2)) (Ioi 0) volume
hb : b ≤ 0
⊢ ∫⁻ (x : ℝ) in Ioi 0, 1 ≤ ∫⁻ (x : ℝ) in Ioi 0, ↑‖rexp (-b * x ^ 2)‖₊

Tactic:
apply lintegral_mono (fun x ↦ _)

Goal state after:
b : ℝ
h : IntegrableOn (fun x ↦ rexp (-b * x ^ 2)) (Ioi 0) volume
hb : b ≤ 0
⊢ ∀ (x : ℝ), 1 ≤ ↑‖rexp (-b * x ^ 2)‖₊
Module: Mathlib.Analysis.SpecialFunctions.PolarCoord

Goal state before:
pp: ι : Type u_1
inst✝ : Finite ι
p : ι → ℝ × ℝ
this : Fintype ι
⊢ HasFDerivAt (fun x i ↦ ↑polarCoord.symm (x i)) (fderivPiPolarCoordSymm p) p

Tactic:
fderivPiPolarCoordSymm,

Goal state after:
ι : Type u_1
inst✝ : Finite ι
p : ι → ℝ × ℝ
this : Fintype ι
⊢ HasFDerivAt (fun x i ↦ ↑polarCoord.symm (x i))
    (ContinuousLinearMap.pi fun i ↦ fderivPolarCoordSymm (p i) ∘SL ContinuousLinearMap.proj i) p
Module: Mathlib.Analysis.SpecialFunctions.PolarCoord

Goal state before:
pp: ι : Type u_1
inst✝ : Fintype ι
p : ι → ℝ × ℝ
⊢ (fderivPiPolarCoordSymm p).det = ∏ i, (p i).1

Tactic:
fderivPiPolarCoordSymm,

Goal state after:
ι : Type u_1
inst✝ : Fintype ι
p : ι → ℝ × ℝ
⊢ (ContinuousLinearMap.pi fun i ↦ fderivPolarCoordSymm (p i) ∘SL ContinuousLinearMap.proj i).det = ∏ i, (p i).1
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic

Goal state before:
pp: s : ℂ
hs : 0 < s.re
⊢ (s + 1).GammaIntegral = s * s.GammaIntegral

Tactic:
suffices Tendsto (s + 1).partialGamma atTop (𝓝 <| s * GammaIntegral s) by
    refine tendsto_nhds_unique ?_ this
    apply tendsto_partialGamma; rw [add_re, one_re]; linarith
  have : (fun X : ℝ => s * partialGamma s X - X ^ s * (-X).exp) =ᶠ[atTop]
      (s + 1).partialGamma := by
    apply eventuallyEq_of_mem (Ici_mem_atTop (0 : ℝ))
    intro X hX
    rw [partialGamma_add_one hs (mem_Ici.mp hX)]
    ring_nf
  refine Tendsto.congr' this ?_
  suffices Tendsto (fun X => -X ^ s * (-X).exp : ℝ → ℂ) atTop (𝓝 0) by
    simpa using! Tendsto.add (Tendsto.const_mul s (tendsto_partialGamma hs)) this
  rw [tendsto_zero_iff_norm_tendsto_zero]
  have :
      (fun e : ℝ => ‖-(e : ℂ) ^ s * (-e).exp‖) =ᶠ[atTop] fun e : ℝ => e ^ s.re * (-1 * e).exp := by
    refine eventuallyEq_of_mem (Ioi_mem_atTop 0) ?_
    intro x hx; dsimp only
    rw [norm_mul, norm_neg, norm_cpow_eq_rpow_re_of_pos hx,
      Complex.norm_of_nonneg (exp_pos (-x)).le, neg_mul, one_mul]
  exact (tendsto_congr' this).mpr (tendsto_rpow_mul_exp_neg_mul_atTop_nhds_zero _ _ zero_lt_one)

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

Goal state before:
pp: ι : Type u_1
inst✝ : Fintype ι
f : (ι → ℝ × ℝ) → ℝ≥0∞
⊢ (∫⁻ (p : ι → ℝ × ℝ) in Set.univ.pi fun x ↦ polarCoord.target,
      (∏ i, ENNReal.ofReal (p i).1) * f fun i ↦ ↑polarCoord.symm (p i)) =
    ∫⁻ (p : ι → ℝ × ℝ), f p

Tactic:
rw [← setLIntegral_univ f, ← setLIntegral_congr pi_polarCoord_symm_target_ae_eq_univ]
  convert!
    (lintegral_image_eq_lintegral_abs_det_fderiv_mul volume measurableSet_pi_polarCoord_target
        (fun p _ ↦ (hasFDerivAt_pi_polarCoord_symm p).hasFDerivWithinAt) injOn_pi_polarCoord_symm
        f).symm using 1
  refine setLIntegral_congr_fun measurableSet_pi_polarCoord_target (fun x hx ↦ ?_)
  simp_rw [det_fderivPiPolarCoordSymm, Finset.abs_prod, ENNReal.ofReal_prod_of_nonneg (fun _ _ ↦
    abs_nonneg _), abs_fst_of_mem_pi_polarCoord_target hx]

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

Goal state before:
pp: s : ℂ
n : ℕ
h1 : -s.re < ↑n
⊢ GammaAux n s = GammaAux n (s + 1) / s

Tactic:
induction n generalizing s with

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

Goal state before:
pp: case n
s : ℝ
hs : ∀ (m : ℕ), s ≠ -↑m
this : ∀ {n : ℕ}, -↑n < s → Gamma s ≠ 0
⊢ ℕ

Tactic:
exact ⌊-s⌋₊ + 1

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

Goal state before:
pp: s : ℝ
hs : ∀ (m : ℕ), s ≠ -↑m
n : ℕ
⊢ -↑n < s → Gamma s ≠ 0

Tactic:
induction n generalizing s with

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

Goal state before:
pp: case e'_3
b : ℂ
V : Type u_1
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : FiniteDimensional ℝ V
inst✝¹ : MeasurableSpace V
inst✝ : BorelSpace V
hb : 0 < b.re
x w : V
⊢ -(↑π ^ 2 * ↑‖x - w‖ ^ 2) / b = (2 * ↑π * I) ^ 2 * ↑‖x - w‖ ^ 2 / (4 * b)

Tactic:
· have : b ≠ 0 := by contrapose! hb; rw [hb, zero_re]
    simp [mul_pow]
    ring

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

Goal state before:
pp: E : Type u_1
F : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : InnerProductSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
inst✝ : NormedSpace ℂ F
⊢ besselPotential E F 0 = ContinuousLinearMap.id ℂ 𝓢'(E, F)

Tactic:
ext f
  simp [besselPotential]

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

Goal state before:
pp: ι : Type u_1
𝕜 : Type u_2
E : Type u_3
F : Type u_4
F₁ : Type u_5
F₂ : Type u_6
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℂ F
r : ℝ
x : E
f : 𝓢'(E, F)
u : 𝓢(E, ℂ)
⊢ (∂_{r • x} f) u = (r • ∂_{x} f) u

Tactic:
simp [lineDerivOp_left_smul, map_smul_of_tower f]

Goal state after:
Module: Mathlib.Analysis.RCLike.Inner

Goal state before:
pp: ι : Type u_1
𝕜 : Type u_3
E : ι → Type u_4
inst✝³ : Fintype ι
inst✝² : RCLike 𝕜
inst✝¹ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝ : (i : ι) → InnerProductSpace 𝕜 (E i)
w : ι → ℝ
f₁ f₂ g : (i : ι) → E i
⊢ ⟪f₁ - f₂, g⟫_[𝕜, w] = ⟪f₁, g⟫_[𝕜, w] - ⟪f₂, g⟫_[𝕜, w]

Tactic:
by
  simp_rw [sub_eq_add_neg, wInner_add_left, wInner_neg_left]

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

Goal state before:
pp: case pos
ι : Type
inst✝ : DecidableEq ι
p n : ι → ℕ
i : ι
x : ZMod (p i ^ n i)
h : n i = 0
⊢ (directSumNeZeroMulHom p n) (0 x) = (DirectSum.of (fun i ↦ ZMod (p i ^ n i)) i) x

Tactic:
simp [(ZMod.subsingleton_iff.2 <| by rw [h, pow_zero]).elim x 0]

Goal state after:
Module: Mathlib.Analysis.Fourier.FiniteAbelian.PontryaginDuality

Goal state before:
pp: n : ℕ
inst✝ : NeZero n
⊢ ∀ (x y : ZMod n), zmod n (x + y) = zmod n x * zmod n y

Tactic:
by
  simp [DFunLike.ext_iff, zmod, add_mul, map_add_eq_mul]

Goal state after:
Module: Mathlib.Analysis.Fourier.FiniteAbelian.PontryaginDuality

Goal state before:
pp: α : Type u_1
inst✝¹ : AddCommGroup α
inst✝ : Fintype α
ι : Type
w✝ : Fintype ι
n : ι → ℕ
hn : ∀ (i : ι), 1 < n i
e : α ≃+ ⨁ (i : ι), ZMod (n i)
hn' : ∀ (i : ι), NeZero (n i)
f : α → AddChar α ℂ := fun a ↦ coeHom.compAddChar ((mkZModAux n ⇑(e a)).compAddMonoidHom ↑e)
hf : Injective f
⊢ Fintype.card (AddChar α ℂ) = Fintype.card α

Tactic:
exact (card_addChar_le _ _).antisymm (Fintype.card_le_of_injective _ hf)

Goal state after: