mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm

Goal state before:
pp: case h
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
hμ1 : μ 1 ≤ 1
s : ℕ → ℕ
hs : ∀ (n : ℕ), s n ≤ n
x : R
ψ : ℕ → ℕ
hψ : ∀ (n : ℕ), 0 ≤ 1 / ↑(ψ n)
hx : 1 < μ x
n : ℕ
⊢ μ (x ^ s (ψ n)) ^ (1 / ↑(ψ n)) ≤ μ x

Tactic:
apply le_trans (rpow_le_rpow (apply_nonneg _ _) (map_pow_le_pow' hμ1 _ _) (hψ n))

Goal state after:
case h
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
hμ1 : μ 1 ≤ 1
s : ℕ → ℕ
hs : ∀ (n : ℕ), s n ≤ n
x : R
ψ : ℕ → ℕ
hψ : ∀ (n : ℕ), 0 ≤ 1 / ↑(ψ n)
hx : 1 < μ x
n : ℕ
⊢ (μ x ^ s (ψ n)) ^ (1 / ↑(ψ n)) ≤ μ x
Module: Mathlib.Analysis.Normed.Unbundled.SpectralNorm

Goal state before:
pp: K : Type u_2
inst✝³ : NormedField K
L : Type u_3
inst✝² : Field L
inst✝¹ : Algebra K L
h_fin : FiniteDimensional K L
hn : Normal K L
inst✝ : IsUltrametricDist K
⊢ IsNonarchimedean (spectralNorm K L)

Tactic:
rw [spectralNorm_eq_invariantExtension]
  exact isNonarchimedean_invariantExtension K L

Goal state after:
Module: Mathlib.Analysis.Normed.Unbundled.SpectralNorm

Goal state before:
pp: K : Type u_2
inst✝³ : NormedField K
L : Type u_3
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsUltrametricDist K
k : K
y : L
hy : IsAlgebraic K y
E : IntermediateField K L := K⟮y⟯
h_finiteDimensional_E : FiniteDimensional K ↥E
g : ↥K⟮y⟯ := AdjoinSimple.gen K y
hgy : k • y = (algebraMap (↥K⟮y⟯) L) (k • g)
⊢ (k • g) • 1 = k • g • 1

Tactic:
smul_assoc

Goal state after:
K : Type u_2
inst✝³ : NormedField K
L : Type u_3
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsUltrametricDist K
k : K
y : L
hy : IsAlgebraic K y
E : IntermediateField K L := K⟮y⟯
h_finiteDimensional_E : FiniteDimensional K ↥E
g : ↥K⟮y⟯ := AdjoinSimple.gen K y
hgy : k • y = (algebraMap (↥K⟮y⟯) L) (k • g)
⊢ k • g • 1 = k • g • 1
Module: Mathlib.Analysis.Normed.Group.Tannery

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
G : Type u_3
𝓕 : Filter α
inst✝¹ : NormedAddCommGroup G
inst✝ : CompleteSpace G
f : α → β → G
g : β → G
bound : β → ℝ
h_sum : Summable bound
hab : ∀ (k : β), Tendsto (fun x ↦ f x k) 𝓕 (𝓝 (g k))
h_bound : ∀ᶠ (n : α) in 𝓕, ∀ (k : β), ‖f n k‖ ≤ bound k
h✝ : IsEmpty β
⊢ Tendsto (fun x ↦ ∑' (k : β), f x k) 𝓕 (𝓝 (∑' (k : β), g k))

pp: case inr
α : Type u_1
β : Type u_2
G : Type u_3
𝓕 : Filter α
inst✝¹ : NormedAddCommGroup G
inst✝ : CompleteSpace G
f : α → β → G
g : β → G
bound : β → ℝ
h_sum : Summable bound
hab : ∀ (k : β), Tendsto (fun x ↦ f x k) 𝓕 (𝓝 (g k))
h_bound : ∀ᶠ (n : α) in 𝓕, ∀ (k : β), ‖f n k‖ ≤ bound k
h✝ : Nonempty β
⊢ Tendsto (fun x ↦ ∑' (k : β), f x k) 𝓕 (𝓝 (∑' (k : β), g k))

Tactic:
· simpa only [tsum_empty] using tendsto_const_nhds

Goal state after:
case inr
α : Type u_1
β : Type u_2
G : Type u_3
𝓕 : Filter α
inst✝¹ : NormedAddCommGroup G
inst✝ : CompleteSpace G
f : α → β → G
g : β → G
bound : β → ℝ
h_sum : Summable bound
hab : ∀ (k : β), Tendsto (fun x ↦ f x k) 𝓕 (𝓝 (g k))
h_bound : ∀ᶠ (n : α) in 𝓕, ∀ (k : β), ‖f n k‖ ≤ bound k
h✝ : Nonempty β
⊢ Tendsto (fun x ↦ ∑' (k : β), f x k) 𝓕 (𝓝 (∑' (k : β), g k))
Module: Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm

Goal state before:
pp: case h
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
hμ1 : μ 1 ≤ 1
x : R
hx : ∀ (y : R), μ (x * y) = μ x * μ y
y : R
hlim : Tendsto (fun n ↦ μ x * smoothingSeminormSeq μ y n) atTop (𝓝 (smoothingFun μ x * smoothingFun μ y))
n : ℕ
hn1 : 1 ≤ n
hn0 : ↑n ≠ 0
⊢ μ ((x * y) ^ n) ^ (1 / ↑n) = μ x * μ (y ^ n) ^ (1 / ↑n)

Tactic:
rw [mul_pow, pow_mul_apply_eq_pow_mul μ hx, mul_rpow (pow_nonneg (apply_nonneg μ _) _)
    (apply_nonneg μ _), ← rpow_natCast, ← rpow_mul (apply_nonneg μ _), mul_one_div_cancel hn0,
    rpow_one]

Goal state after:
Module: Mathlib.Topology.Algebra.InfiniteSum.Field

Goal state before:
pp: α : Type u_1
E : Type u_2
inst✝² : SeminormedCommRing E
inst✝¹ : NormMulClass E
inst✝ : NormOneClass E
f : α → E
x : E
hfx : HasProd f x
⊢ HasProd (fun x ↦ ‖f x‖) ‖x‖

Tactic:
by
  simp only [HasProd, ← norm_prod]
  exact hfx.norm

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

Goal state before:
pp: X : Type u_1
inst✝³ : NormedAddCommGroup X
M : Type u_2
inst✝² : Ring M
inst✝¹ : Module M X
inst✝ : FaithfulSMul M X
P Q R : { P // IsLprojection X P }
e₁ : ↑((P ⊔ Q) ⊓ (P ⊔ R)) = ↑P + ↑Q * ↑R * ↑Pᶜ
⊢ (↑P + ↑Pᶜ * ↑Q) * (↑P + (↑R - ↑P * ↑R)) * (↑P + (↑(Q ⊓ R) - ↑P * ↑(Q ⊓ R))) = ↑P + ↑Q * ↑R * ↑Pᶜ

Tactic:
←
        compl_mul,

Goal state after:
X : Type u_1
inst✝³ : NormedAddCommGroup X
M : Type u_2
inst✝² : Ring M
inst✝¹ : Module M X
inst✝ : FaithfulSMul M X
P Q R : { P // IsLprojection X P }
e₁ : ↑((P ⊔ Q) ⊓ (P ⊔ R)) = ↑P + ↑Q * ↑R * ↑Pᶜ
⊢ (↑P + ↑Pᶜ * ↑Q) * (↑P + ↑Pᶜ * ↑R) * (↑P + (↑(Q ⊓ R) - ↑P * ↑(Q ⊓ R))) = ↑P + ↑Q * ↑R * ↑Pᶜ
Module: Mathlib.Analysis.Normed.Module.MStructure

Goal state before:
pp: X : Type u_1
inst✝³ : NormedAddCommGroup X
M : Type u_2
inst✝² : Ring M
inst✝¹ : Module M X
inst✝ : FaithfulSMul M X
P : { P // IsLprojection X P }
⊢ 1 = 1 - 0

Tactic:
sub_zero

Goal state after:
X : Type u_1
inst✝³ : NormedAddCommGroup X
M : Type u_2
inst✝² : Ring M
inst✝¹ : Module M X
inst✝ : FaithfulSMul M X
P : { P // IsLprojection X P }
⊢ 1 = 1
Module: Mathlib.Analysis.Normed.Lp.lpHolder

Goal state before:
pp: case inr.inl
ι : Type u_1
𝕜 : Type u_2
E : ι → Type u_3
F : ι → Type u_4
G : ι → Type u_5
inst✝⁹ : RCLike 𝕜
inst✝⁸ : (i : ι) → NormedAddCommGroup (E i)
inst✝⁷ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝⁶ : (i : ι) → NormedAddCommGroup (F i)
inst✝⁵ : (i : ι) → NormedSpace 𝕜 (F i)
inst✝⁴ : (i : ι) → NormedAddCommGroup (G i)
inst✝³ : (i : ι) → NormedSpace 𝕜 (G i)
r : ℝ≥0∞
inst✝² : Fact (1 ≤ r)
B : (i : ι) → E i →L[𝕜] F i →L[𝕜] G i
K : ℝ≥0
hBK : ∀ (i : ι), ‖B i‖ ≤ ↑K
inst✝¹ : Fact (1 ≤ ∞)
f : ↥(lp F ∞)
inst✝ : Fact (1 ≤ r)
e : ↥(lp E r)
hp : 1 ≤ r.toReal
hpqr : r.HolderTriple ∞ r
s : Finset ι
⊢ ∀ (s : Finset ι), ∑ i ∈ s, ‖↑e i‖ ^ r.toReal ≤ ‖e‖ ^ r.toReal

Tactic:
exact sum_rpow_le_norm_rpow (zero_lt_one.trans_le hp) e

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : AddCommGroup F
inst✝³ : Module 𝕜 E
inst✝² : Module 𝕜 F
inst✝¹ : TopologicalSpace E
inst✝ : TopologicalSpace F
u : E →L[𝕜] F
pkg : u.FredholmPackage
⊢ ↑pkg.equiv = u.restrict ⋯

Tactic:
ext x
  simp [pkg.eq_equiv]

Goal state after:
Module: Mathlib.Topology.MetricSpace.Contracting

Goal state before:
pp: α : Type u_1
inst✝ : MetricSpace α
K : ℝ≥0
f : α → α
hf : ContractingWith K f
g : α → α
x y : α
hx : IsFixedPt f x
hy : IsFixedPt g y
C : ℝ
hfg : ∀ (z : α), dist (f z) (g z) ≤ C
⊢ dist y (f y) / (1 - ↑K) = dist (f y) y / (1 - ↑K)

Tactic:
dist_comm

Goal state after:
α : Type u_1
inst✝ : MetricSpace α
K : ℝ≥0
f : α → α
hf : ContractingWith K f
g : α → α
x y : α
hx : IsFixedPt f x
hy : IsFixedPt g y
C : ℝ
hfg : ∀ (z : α), dist (f z) (g z) ≤ C
⊢ dist (f y) y / (1 - ↑K) = dist (f y) y / (1 - ↑K)
Module: Mathlib.Analysis.Polynomial.Fourier

Goal state before:
pp: p : ℂ[X]
n : ℤ
this : n < 0 ∨ ∃ k, n = ↑k
⊢ fourierCoeff (⇑(toAddCircle p)) n = if 0 ≤ n then p.coeff n.natAbs else 0

Tactic:
induction p using Polynomial.induction_on' with obtain (hn | ⟨k, rfl⟩) := this
  | add p q hp hq =>
    simp_all [not_le_of_gt, fourierCoeff.add (toAddCircle.integrable p) (toAddCircle.integrable q)]
  | monomial m a =>
    simp_all [not_le_of_gt, coeff_monomial, toAddCircle_monomial_eq_smul_fourier,
      fourierCoeff.const_smul, fourierCoeff_fourier, Pi.single_apply]
    grind

Goal state after:
Module: Mathlib.Analysis.Polynomial.Basic

Goal state before:
pp: case e'_6
𝕜 : Type u_1
inst✝³ : NormedField 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
P : 𝕜[X]
inst✝ : OrderTopology 𝕜
x✝ : 𝕜
⊢ P.leadingCoeff * x✝ ^ P.natDegree = (P.comp (-X)).leadingCoeff * (-x✝) ^ (P.comp (-X)).natDegree

Tactic:
comp_neg_X_leadingCoeff_eq,

Goal state after:
case e'_6
𝕜 : Type u_1
inst✝³ : NormedField 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
P : 𝕜[X]
inst✝ : OrderTopology 𝕜
x✝ : 𝕜
⊢ P.leadingCoeff * x✝ ^ P.natDegree = (-1) ^ P.natDegree * P.leadingCoeff * (-x✝) ^ (P.comp (-X)).natDegree
Module: Mathlib.RingTheory.PowerSeries.GaussNorm

Goal state before:
pp: case mp
R : Type u_1
inst✝ : Semiring R
v : R → ℝ
c : ℝ
f : R⟦X⟧
h : HasGaussNorm v c f
x✝ : ℝ
⊢ (∃ y, v ((coeff y) f) * c ^ y = x✝) → ∃ y, v ((MvPowerSeries.coeff y) f) * c ^ y PUnit.unit = x✝

Tactic:
intro h
    obtain ⟨y, hy⟩ := h
    use (Finsupp.uniqueEquiv ()).symm y
    simpa [coeff] using hy

Goal state after:
Module: Mathlib.Analysis.ODE.PicardLindelof

Goal state before:
pp: case neg.inl
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℝ → E → E
α : ℝ → E
u : Set E
tmin tmax : ℝ
n : ℕ∞
hf : ContDiffOn ℝ (↑n) (uncurry f) (Icc tmin tmax ×ˢ u)
hα : ∀ t ∈ Icc tmin tmax, HasDerivWithinAt α (f t (α t)) (Icc tmin tmax) t
hmem : MapsTo α (Icc tmin tmax) u
h : tmax < tmin
⊢ ContDiffOn ℝ (↑n) α (Icc tmin tmax)

Tactic:
intro _ ht
      rw [Icc_eq_empty (not_le.mpr h)] at ht
      exfalso
      exact notMem_empty _ ht

Goal state after:
Module: Mathlib.Analysis.Real.OfDigits

Goal state before:
pp: case neg
b : ℕ
hb : 1 < b
this : NeZero b
y : ℝ
hy : y ∈ Set.Icc 0 1
hy' : y ∉ Set.Ico 0 1
⊢ ∃ y, ofDigits y = 1

Tactic:
exact ⟨_, ofDigits_const_last_eq_one' hb⟩

Goal state after:
Module: Mathlib.Analysis.Real.Hyperreal

Goal state before:
pp: x : ℝ*
r : ℝ
hx : Germ.Tendsto x (𝓝 r)
⊢ 0 ≤ ArchimedeanClass.mk x

Tactic:
rw [tendsto_iff_forall] at hx

Goal state after:
x : ℝ*
r : ℝ
hx : (∀ s < r, ↑s ≤ x) ∧ ∀ s > r, x ≤ ↑s
⊢ 0 ≤ ArchimedeanClass.mk x
Module: Mathlib.Analysis.Real.Hyperreal

Goal state before:
pp: x : ℝ*
r : ℝ
hx : Germ.Tendsto x (𝓝 r)
⊢ stdPart x = r

Tactic:
rw [tendsto_iff_forall] at hx

Goal state after:
x : ℝ*
r : ℝ
hx : (∀ s < r, ↑s ≤ x) ∧ ∀ s > r, x ≤ ↑s
⊢ stdPart x = r
Module: Mathlib.Analysis.Real.Pi.Leibniz

Goal state before:
pp: ⊢ Tendsto (fun k ↦ ∑ i ∈ range k, (-1) ^ i / (2 * ↑i + 1)) atTop (𝓝 (π / 4))

Tactic:
obtain ⟨l, h⟩ :
      ∃ l, Tendsto (fun n ↦ ∑ i ∈ range n, (-1 : ℝ) ^ i / (2 * i + 1)) atTop (𝓝 l) := by
    apply Antitone.tendsto_alternating_series_of_tendsto_zero
    · exact antitone_iff_forall_lt.mpr fun _ _ _ ↦ by gcongr
    · apply Tendsto.inv_tendsto_atTop; apply tendsto_atTop_add_const_right
      exact tendsto_natCast_atTop_atTop.const_mul_atTop zero_lt_two
  -- Abel's limit theorem states that the corresponding power series has the same limit as `x → 1⁻`
  have abel := tendsto_tsum_powerSeries_nhdsWithin_lt h
  -- Massage the expression to get `x ^ (2 * n + 1)` in the tsum rather than `x ^ n`...
  have m : 𝓝[<] (1 : ℝ) ≤ 𝓝 1 := tendsto_nhdsWithin_of_tendsto_nhds fun _ a ↦ a
  have q : Tendsto (fun x : ℝ ↦ x ^ 2) (𝓝[<] 1) (𝓝[<] 1) := by
    apply tendsto_nhdsWithin_of_tendsto_nhds_of_eventually_within
    · nth_rw 3 [← one_pow 2]
      exact Tendsto.pow ‹_› _
    · rw [eventually_iff_exists_mem]
      use Set.Ioo (-1) 1
      exact ⟨Ioo_mem_nhdsLT <| by simp,
        fun _ _ ↦ by rwa [Set.mem_Iio, sq_lt_one_iff_abs_lt_one, abs_lt, ← Set.mem_Ioo]⟩
  replace abel := (abel.comp q).mul m
  rw [mul_one] at abel
  -- ...so that we can replace the tsum with the real arctangent function
  replace abel : Tendsto arctan (𝓝[<] 1) (𝓝 l) := by
    apply abel.congr'
    rw [eventuallyEq_nhdsWithin_iff, Metric.eventually_nhds_iff]
    use 1, zero_lt_one
    intro y hy1 hy2
    rw [dist_eq, abs_sub_lt_iff] at hy1
    rw [Set.mem_Iio] at hy2
    have ny : ‖y‖ < 1 := by rw [norm_eq_abs, abs_lt]; constructor <;> linarith
    rw [← (hasSum_arctan ny).tsum_eq, Function.comp_apply, ← tsum_mul_right]
    simp_rw [mul_assoc, ← pow_mul, ← pow_succ, div_mul_eq_mul_div]
    norm_cast
  -- But `arctan` is continuous everywhere, so the limit is `arctan 1 = π / 4`
  rwa [tendsto_nhds_unique abel ((continuous_arctan.tendsto 1).mono_left m), arctan_one] at h

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

Goal state before:
pp: case left
x y : ℝ≥0
h : x ≤ y
⊢ x ^ 2 ≤ x * y

Tactic:
sq

Goal state after:
case left
x y : ℝ≥0
h : x ≤ y
⊢ x * x ≤ x * y
Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean

Goal state before:
pp: case hcd
x✝ y✝ x y : ℝ≥0
h : x ≤ y
⊢ x ^ 2 ≤ x * y

Tactic:
sq

Goal state after:
case hcd
x✝ y✝ x y : ℝ≥0
h : x ≤ y
⊢ x * x ≤ x * y
Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean

Goal state before:
pp: x y : ℝ≥0
n : ℕ
| dist (x.agmSequences y n).2 (x.agmSequences y n).1

Tactic:
dist_comm

Goal state after:
x y : ℝ≥0
n : ℕ
| dist (x.agmSequences y n).1 (x.agmSequences y n).2
Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy

Goal state before:
pp: ⊢ binEntropy 2⁻¹ = log 2

Tactic:
norm_num [binEntropy]; simp; ring

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

Goal state before:
pp: l : Filter ℂ
hl : IsExpCmpFilter l
n : ℕ
⊢ (fun z ↦ |z.im| ^ n) ≤ᶠ[l] fun z ↦ Real.exp z.re

Tactic:
simpa using! (hl.isLittleO_im_pow_exp_re n).bound zero_lt_one

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

Goal state before:
pp: case inr
p : ℝ
hp : p < 0
hp' : ¬p < -1
this : ∀ {p : ℝ}, p < 0 → ¬p < -1 → -1 < p → -p * log p ≤ 0
h : ¬-1 < p
⊢ -p * log p ≤ 0

pp: p✝ p : ℝ
hp : p < 0
hp' : ¬p < -1
h : -1 < p
⊢ -p * log p ≤ 0

Tactic:
· simp only [show p = -1 by linarith, log_neg_eq_log, log_one, le_refl, mul_zero]

Goal state after:
p✝ p : ℝ
hp : p < 0
hp' : ¬p < -1
h : -1 < p
⊢ -p * log p ≤ 0
Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy

Goal state before:
pp: q : ℕ
p : ℝ
hp₀ : 0 < p
hp₁ : p < 1
⊢ 0 < qaryEntropy q p

Tactic:
unfold qaryEntropy

Goal state after:
q : ℕ
p : ℝ
hp₀ : 0 < p
hp₁ : p < 1
⊢ 0 < p * log ↑(↑q - 1) + binEntropy p
Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy

Goal state before:
pp: q : ℕ
⊢ Continuous (qaryEntropy q)

Tactic:
unfold qaryEntropy

Goal state after:
q : ℕ
⊢ Continuous fun p ↦ p * log ↑(↑q - 1) + binEntropy p
Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy

Goal state before:
pp: q : ℕ
p : ℝ
hp₀ : p ≠ 0
hp₁ : p ≠ 1
⊢ DifferentiableAt ℝ (qaryEntropy q) p

Tactic:
unfold qaryEntropy

Goal state after:
q : ℕ
p : ℝ
hp₀ : p ≠ 0
hp₁ : p ≠ 1
⊢ DifferentiableAt ℝ (fun p ↦ p * log ↑(↑q - 1) + binEntropy p) p
Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy

Goal state before:
pp: q : ℕ
p : ℝ
hp₀ : p ≠ 0
hp₁ : p ≠ 1
⊢ deriv (qaryEntropy q) p = log (↑q - 1) + log (1 - p) - log p

Tactic:
unfold qaryEntropy

Goal state after:
q : ℕ
p : ℝ
hp₀ : p ≠ 0
hp₁ : p ≠ 1
⊢ deriv (fun p ↦ p * log ↑(↑q - 1) + binEntropy p) p = log (↑q - 1) + log (1 - p) - log p
Module: Mathlib.Analysis.Real.Pi.Irrational

Goal state before:
pp: case refine_2
n : ℕ
⊢ ((monomial 2) (-4)).natDegree + (sinPoly n).natDegree ≤ n + 2

Tactic:
simpa [add_comm 2] using sinPoly_natDegree_le n

Goal state after:
Module: Mathlib.Analysis.Real.Pi.Irrational

Goal state before:
pp: θ : ℝ
n : ℕ
⊢ 2 * (↑n + 2) * (2 * ↑n + 3) * (I (n + 1) θ * θ ^ (2 * (n + 1) + 1)) -
      4 * (↑n + 2) * (↑n + 1) * θ ^ 2 * (I n θ * θ ^ (2 * n + 1)) =
    ↑(n + 2)! *
      (eval₂ (Int.castRingHom ℝ) θ (sinPoly (n + 2)) * sin θ + eval₂ (Int.castRingHom ℝ) θ (cosPoly (n + 2)) * cos θ)

Tactic:
simp [sinPoly_add_cosPoly_eval, sinPoly, cosPoly, Nat.factorial_succ]; ring

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Log.RpowTendsto

Goal state before:
pp: ⊢ TendstoLocallyUniformlyOn (fun p x ↦ p⁻¹ * (x ^ p - 1)) log (𝓝[>] 0) (Ioi 0)

Tactic:
refine (tendstoLocallyUniformlyOn_iff_forall_isCompact isOpen_Ioi).mpr ?_
  intro s hs hs'
  rw [Metric.uniformity_basis_dist_le.tendstoUniformlyOn_iff_of_uniformity]
  intro ε hε
  let pbound : ℝ := ε / (sSup ((fun x => ‖log x‖ ^ 2) '' s) + 1)
  have hxs : ∀ x ∈ s, x ≠ 0 := by grind
  have sSup_nonneg : 0 ≤ sSup ((fun x => ‖log x‖ ^ 2) '' s) := by
    refine Real.sSup_nonneg ?_
    grind [← sq_nonneg]
  have sSup_nonneg' : 0 ≤ sSup ((fun x => ‖log x‖) '' s) := by
    refine Real.sSup_nonneg ?_
    grind [← sq_nonneg]
  have pbound_pos : 0 < pbound := by positivity
  have h₁ : ∀ᶠ p : ℝ in 𝓝[>] 0, 0 < p ∧ p < pbound := nhdsGT_basis 0 |>.mem_of_mem pbound_pos
  have h₂ : ∀ᶠ p : ℝ in 𝓝[>] 0, p ≤ 1 / (sSup ((fun x => ‖log x‖) '' s) + 1) :=
    Eventually.filter_mono nhdsWithin_le_nhds <| eventually_le_nhds (by positivity)
  have hcont : ContinuousOn (fun x => ‖log x‖ ^ 2) s := by fun_prop
  have hcont' : ContinuousOn (fun x => ‖log x‖) s := by fun_prop
  filter_upwards [h₁, h₂] with p ⟨hp₁,hp₂⟩ hp₃
  intro x hx
  have hx' : ‖p * log x‖ ≤ 1 := calc
    _ = p * ‖log x‖ := by grind [norm_mul, Real.norm_of_nonneg]
    _ ≤ 1 / (sSup ((fun y => ‖log y‖) '' s) + 1) * ‖log x‖ := by gcongr
    _ ≤ 1 / (‖log x‖ + 1) * ‖log x‖ := by
        gcongr
        refine le_csSup ?_ (by grind)
        grind [IsCompact.bddAbove, ← IsCompact.image_of_continuousOn]
    _ = ‖log x‖ / (‖log x‖ + 1) := by grind
    _ ≤ 1 := by rw [div_le_one₀] <;> grind [norm_nonneg]
  have pinv_nonneg : 0 ≤ p⁻¹ := by grind [_root_.inv_nonneg]
  rw [dist_eq_norm']
  calc
    _ ≤ p * ‖log x‖ ^ 2 := Real.norm_inv_mul_rpow_sub_one_sub_log_le hp₁ (hs hx) hx'
    _ ≤ p * sSup ((fun x => ‖log x‖ ^ 2) '' s) := by
          gcongr
          refine le_csSup ?_ (by grind)
          grind [IsCompact.bddAbove, ← IsCompact.image_of_continuousOn]
    _ ≤ pbound * (sSup ((fun x => ‖log x‖ ^ 2) '' s) + 1) := by gcongr; grind
    _ = ε := by grind

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation

Goal state before:
pp: p x : ℝ
hp : p ∈ Ioo 0 1
hx : 0 ≤ x
⊢ IntegrableOn (fun x_1 ↦ p.rpowIntegrand₀₁ x_1 x) (Ioc 0 1) volume

Tactic:
by
  refine IntegrableOn.congr_set_ae (t := Ioo 0 1) ?_ (Filter.EventuallyEq.symm Ioo_ae_eq_Ioc)
  refine ⟨?meas, ?finite⟩
  case meas =>
    refine ContinuousOn.aestronglyMeasurable ?_ measurableSet_Ioo
    exact ContinuousOn.mono (continuousOn_rpowIntegrand₀₁ hp hx) Ioo_subset_Ioi_self
  case finite =>
    refine HasFiniteIntegral.mono' (g := fun t => t ^ (p - 1)) ?finitebound ?ae_le
    case finitebound =>
      apply Integrable.hasFiniteIntegral
      rw [Set.mem_Ioo] at hp
      rw [← IntegrableOn, intervalIntegral.integrableOn_Ioo_rpow_iff]
      · linarith
      · exact zero_lt_one
    case ae_le =>
      refine ae_restrict_of_forall_mem measurableSet_Ioo fun t ht => ?_
      rw [Real.norm_of_nonneg (rpowIntegrand₀₁_nonneg hp.1 (le_of_lt ht.1) hx)]
      exact rpowIntegrand₀₁_le_rpow_sub_one hp (le_of_lt ht.1) hx

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

Goal state before:
pp: s : ℂ
⊢ ↑π ^ (-s / 2) * Gamma (s / 2) * (↑π ^ (-(s + 1) / 2) * Gamma ((s + 1) / 2)) = 2 * (2 * ↑π) ^ (-s) * Gamma s

Tactic:
calc
  _ = (π ^ (-s / 2) * π ^ (-(s + 1) / 2)) * (Gamma (s / 2) * Gamma (s / 2 + 1 / 2)) := by ring_nf
  _ = 2 ^ (1 - s) * (π ^ (-1 / 2 - s) * π ^ (1 / 2 : ℂ)) * Gamma s := by
    rw [← cpow_add _ _ (ofReal_ne_zero.mpr pi_ne_zero), Complex.Gamma_mul_Gamma_add_half,
      sqrt_eq_rpow, ofReal_cpow pi_pos.le, ofReal_div, ofReal_one, ofReal_ofNat]
    ring_nf
  _ = 2 * ((2 : ℝ) ^ (-s) * π ^ (-s)) * Gamma s := by
    rw [sub_eq_add_neg, cpow_add _ _ two_ne_zero, cpow_one,
      ← cpow_add _ _ (ofReal_ne_zero.mpr pi_ne_zero), ofReal_ofNat]
    ring_nf
  _ = 2 * (2 * π) ^ (-s) * Gamma s := by
    rw [← mul_cpow_ofReal_nonneg two_pos.le pi_pos.le, ofReal_ofNat]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation

Goal state before:
pp: A : Type u_1
inst✝⁹ : NonUnitalNormedRing A
inst✝⁸ : StarRing A
inst✝⁷ : NormedSpace ℝ A
inst✝⁶ : SMulCommClass ℝ A A
inst✝⁵ : IsScalarTower ℝ A A
inst✝⁴ : PartialOrder A
inst✝³ : StarOrderedRing A
inst✝² : NonnegSpectrumClass ℝ A
inst✝¹ : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝ : CompleteSpace A
p : ℝ≥0
hp : p ∈ Ioo 1 2
μ : Measure ℝ
hμ :
  ∀ x ∈ Ici 0,
    IntegrableOn (fun t ↦ (↑p).rpowIntegrand₁₂ t x) (Ioi 0) μ ∧ x ^ ↑p = ∫ (t : ℝ) in Ioi 0, (↑p).rpowIntegrand₁₂ t x ∂μ
a : A
ha : 0 ≤ a
⊢ ↑p ∈ Ioo 1 2

Tactic:
exact_mod_cast hp

Goal state after:
Module: Mathlib.NumberTheory.Harmonic.GammaDeriv

Goal state before:
pp: h_diff : ∀ {s : ℝ}, 0 < s → DifferentiableAt ℝ Gamma s
h_diff' : ∀ {s : ℝ}, 0 < s → DifferentiableAt ℝ (fun s ↦ Gamma (2 * s)) s
⊢ √π * (deriv (fun s ↦ Gamma (2 * s)) (1 / 2) + deriv (fun s ↦ 2 ^ (1 - 2 * s)) (1 / 2) + γ) =
    √π * (-2 * γ + deriv (fun s ↦ 2 ^ (1 - 2 * s)) (1 / 2) + γ)

Tactic:
congr 3
    change deriv (Gamma ∘ fun s ↦ 2 * s) _ = _
    rw [deriv_comp, deriv_const_mul_id, mul_one_div, div_self two_ne_zero]
    · rw [mul_comm, hasDerivAt_Gamma_one.deriv, mul_neg, neg_mul]
    · apply h_diff; simp -- s = 1
    · fun_prop

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Log.Monotone

Goal state before:
pp: a : ℝ
ha : 0 < a
x : ℝ
hex : x ∈ Ici (rexp a⁻¹)
y : ℝ
x✝ : y ∈ Ici (rexp a⁻¹)
hxy : x ≤ y
x_pos : 0 < x
y_pos : 0 < y
⊢ log ((y ^ a) ^ (1 / a)) / y ^ a ≤ log (x ^ (a * (1 / a))) / x ^ a

Tactic:
rpow_mul x_pos.le,

Goal state after:
a : ℝ
ha : 0 < a
x : ℝ
hex : x ∈ Ici (rexp a⁻¹)
y : ℝ
x✝ : y ∈ Ici (rexp a⁻¹)
hxy : x ≤ y
x_pos : 0 < x
y_pos : 0 < y
⊢ log ((y ^ a) ^ (1 / a)) / y ^ a ≤ log ((x ^ a) ^ (1 / a)) / x ^ a
Module: Mathlib.Analysis.SpecialFunctions.Log.Base

Goal state before:
pp: b✝ b : ℝ
hb : b ≠ -1 ∧ b ≠ 0 ∧ b ≠ 1
hb₀ : 0 < b
hb₁ : 1 < b
x : ℝ
hx₁ : 1 ≤ x
⊢ logb b x = |logb b x|

Tactic:
abs_of_nonneg

Goal state after:
b✝ b : ℝ
hb : b ≠ -1 ∧ b ≠ 0 ∧ b ≠ 1
hb₀ : 0 < b
hb₁ : 1 < b
x : ℝ
hx₁ : 1 ≤ x
⊢ logb b x = logb b x

b✝ b : ℝ
hb : b ≠ -1 ∧ b ≠ 0 ∧ b ≠ 1
hb₀ : 0 < b
hb₁ : 1 < b
x : ℝ
hx₁ : 1 ≤ x
⊢ 0 ≤ logb b x
Module: Mathlib.Analysis.SpecialFunctions.Log.Base

Goal state before:
pp: case inr
b : ℝ
hb₀ : 0 < b
hb : b ≠ 1
h : ContinuousAt (logb b) 0
hb₁ : 1 < b
⊢ False

Tactic:
exact not_tendsto_nhds_of_tendsto_atBot (tendsto_logb_nhdsNE_zero hb₁)
        _ (h.tendsto.mono_left inf_le_left)

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

Goal state before:
pp: case h0
n : ℕ
ih : MonotoneOn (deriv fun x ↦ Polynomial.eval x (descPochhammer ℝ n)) (Set.Ioi (↑n - 1))
a : ℝ
ha : ↑n < a
b : ℝ
hb : ↑n < b
hab : a ≤ b
i : ℕ
hi : i ∈ Finset.range (n + 1)
j : ℕ
hj : j ∈ (Finset.range (n + 1)).erase i
⊢ 0 ≤ a - ↑j

Tactic:
Finset.mem_erase,

Goal state after:
case h0
n : ℕ
ih : MonotoneOn (deriv fun x ↦ Polynomial.eval x (descPochhammer ℝ n)) (Set.Ioi (↑n - 1))
a : ℝ
ha : ↑n < a
b : ℝ
hb : ↑n < b
hab : a ≤ b
i : ℕ
hi : i ∈ Finset.range (n + 1)
j : ℕ
hj : j ≠ i ∧ j ∈ Finset.range (n + 1)
⊢ 0 ≤ a - ↑j
Module: Mathlib.MeasureTheory.Constructions.HaarToSphere

Goal state before:
pp: E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : MeasurableSpace E
μ : Measure E
inst✝ : BorelSpace E
⊢ ↑(dim E) * μ (Ioo 0 1 • sphere 0 1) = ↑(dim E) * μ (ball 0 1 \ {0})

Tactic:
Ioo_smul_sphere_zero

Goal state after:
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : MeasurableSpace E
μ : Measure E
inst✝ : BorelSpace E
⊢ ↑(dim E) * μ (ball 0 (1 * 1) \ closedBall 0 (0 * 1)) = ↑(dim E) * μ (ball 0 1 \ {0})

case ha
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : MeasurableSpace E
μ : Measure E
inst✝ : BorelSpace E
⊢ 0 ≤ 0

case hr
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : MeasurableSpace E
μ : Measure E
inst✝ : BorelSpace E
⊢ 0 < 1