mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Real.OfDigits

Goal state before:
pp: x : ℝ
b : ℕ
inst✝ : NeZero b
hx : x ∈ Set.Ico 0 1
n : ℕ
this✝ : 0 < b
this : ↑b ^ n * ∑ i ∈ Finset.range n, ofDigitsTerm (x.digits b) i = ↑⌊↑b ^ n * x⌋₊
h_le : ↑b ^ n * x < ↑b ^ n * ∑ i ∈ Finset.range n, ofDigitsTerm (x.digits b) i + 1
⊢ ↑b ^ n * x - ↑b ^ n * (↑b ^ n)⁻¹ ≤ ↑b ^ n * ∑ i ∈ Finset.range n, ofDigitsTerm (x.digits b) i

Tactic:
mul_inv_cancel₀ (by positivity)

Goal state after:
x : ℝ
b : ℕ
inst✝ : NeZero b
hx : x ∈ Set.Ico 0 1
n : ℕ
this✝ : 0 < b
this : ↑b ^ n * ∑ i ∈ Finset.range n, ofDigitsTerm (x.digits b) i = ↑⌊↑b ^ n * x⌋₊
h_le : ↑b ^ n * x < ↑b ^ n * ∑ i ∈ Finset.range n, ofDigitsTerm (x.digits b) i + 1
⊢ ↑b ^ n * x - 1 ≤ ↑b ^ n * ∑ i ∈ Finset.range n, ofDigitsTerm (x.digits b) i
Module: Mathlib.Analysis.Real.OfDigits

Goal state before:
pp: x : ℝ
b : ℕ
inst✝ : NeZero b
hb : 1 < b
hx : x ∈ Set.Ico 0 1
⊢ Filter.Tendsto (fun i ↦ x - (↑b)⁻¹ ^ i) Filter.atTop (nhds x)

Tactic:
convert! tendsto_const_nhds.sub (tendsto_pow_atTop_nhds_zero_of_abs_lt_one _)

Goal state after:
case e'_5
x : ℝ
b : ℕ
inst✝ : NeZero b
hb : 1 < b
hx : x ∈ Set.Ico 0 1
⊢ x = x - 0

case convert_3
x : ℝ
b : ℕ
inst✝ : NeZero b
hb : 1 < b
hx : x ∈ Set.Ico 0 1
⊢ |(↑b)⁻¹| < 1
Module: Mathlib.NumberTheory.Real.Irrational

Goal state before:
pp: n : ℕ
m : ℤ
hnpos : 0 < n
N : ℤ
D : ℕ
P : D ≠ 0
C : N.natAbs.Coprime D
hxr : ↑((N /. ↑D) ^ n) = ↑m
hv : ¬∃ y, ↑{ num := N, den := D, den_nz := P, reduced := C } = ↑y
c1 : ↑↑D ≠ 0
c2 : ↑↑D ^ n ≠ 0
⊢ False

Tactic:
cast_pow,

Goal state after:
n : ℕ
m : ℤ
hnpos : 0 < n
N : ℤ
D : ℕ
P : D ≠ 0
C : N.natAbs.Coprime D
hxr : ↑(N /. ↑D) ^ n = ↑m
hv : ¬∃ y, ↑{ num := N, den := D, den_nz := P, reduced := C } = ↑y
c1 : ↑↑D ≠ 0
c2 : ↑↑D ^ n ≠ 0
⊢ False
Module: Mathlib.NumberTheory.Real.Irrational

Goal state before:
pp: x : ℝ
h : Irrational x
⊢ Irrational x⁻¹⁻¹

Tactic:
rwa [inv_inv]

Goal state after:
Module: Mathlib.NumberTheory.Real.Irrational

Goal state before:
pp: x : ℝ
n : ℕ
h : Irrational (x ^ ↑n)
⊢ Irrational x

Tactic:
zpow_natCast

Goal state after:
x : ℝ
n : ℕ
h : Irrational (x ^ n)
⊢ Irrational x
Module: Mathlib.Analysis.Real.Hyperreal

Goal state before:
pp: x y : ℝ*
hx : x.InfinitePos
hy₁ : ¬y.Infinitesimal
hy₂ : 0 < y
r : ℝ
hy₁' : ∃ x, ¬(0 < x → -↑x < y ∧ y < ↑x)
⊢ ↑r < x * y

Tactic:
let ⟨r₁, hy₁''⟩ := hy₁'

Goal state after:
x y : ℝ*
hx : x.InfinitePos
hy₁ : ¬y.Infinitesimal
hy₂ : 0 < y
r : ℝ
hy₁' : ∃ x, ¬(0 < x → -↑x < y ∧ y < ↑x)
r₁ : ℝ
hy₁'' : ¬(0 < r₁ → -↑r₁ < y ∧ y < ↑r₁)
⊢ ↑r < x * y
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arctan

Goal state before:
pp: z : ℂ
h₂ : z ≠ -I
h₁ : -1 = z * I
⊢ z = I

Tactic:
← div_eq_iff I_ne_zero,

Goal state after:
z : ℂ
h₂ : z ≠ -I
h₁ : -1 / I = z
⊢ z = I
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arctan

Goal state before:
pp: z : ℂ
h₁ : z ≠ I
z₁ : 1 + z * I ≠ 0
h₂ : 1 = z * I
⊢ z = -I

Tactic:
← div_eq_iff I_ne_zero,

Goal state after:
z : ℂ
h₁ : z ≠ I
z₁ : 1 + z * I ≠ 0
h₂ : 1 / I = z
⊢ z = -I
Module: Mathlib.Analysis.Real.Pi.Wallis

Goal state before:
pp: case succ.refine_3
n : ℕ
IH :
  ∏ i ∈ range n, (2 * ↑i + 2) / (2 * ↑i + 1) * ((2 * ↑i + 2) / (2 * ↑i + 3)) =
    2 ^ (4 * n) * ↑n ! ^ 4 / (↑(2 * n)! ^ 2 * (2 * ↑n + 1))
⊢ 2 ^ (4 * n) * (↑n ! ^ 0 * ↑n ! * ↑n ! * ↑n ! * ↑n !) * ((2 * ↑n + 2) * (2 * ↑n + 2)) *
      (((2 * ↑n + 1 + 1) * ((2 * ↑n + 1) * ↑(2 * n)!)) ^ 0 * ((2 * ↑n + 1 + 1) * ((2 * ↑n + 1) * ↑(2 * n)!)) *
          ((2 * ↑n + 1 + 1) * ((2 * ↑n + 1) * ↑(2 * n)!)) *
        (2 * (↑n + 1) + 1)) =
    2 ^ (4 * n) * 2 * 2 * 2 * 2 *
        (((↑n + 1) * ↑n !) ^ 0 * ((↑n + 1) * ↑n !) * ((↑n + 1) * ↑n !) * ((↑n + 1) * ↑n !) * ((↑n + 1) * ↑n !)) *
      (↑(2 * n)! ^ 0 * ↑(2 * n)! * ↑(2 * n)! * (2 * ↑n + 1) * ((2 * ↑n + 1) * (2 * ↑n + 3)))

Tactic:
ring_nf

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

Goal state before:
pp: k : ℕ
⊢ (2 * ↑k + 1) / (2 * ↑k + 2) ≤ W k / (π / 2)

Tactic:
div_eq_inv_mul (W k) _

Goal state after:
k : ℕ
⊢ (2 * ↑k + 1) / (2 * ↑k + 2) ≤ (π / 2)⁻¹ * W k
Module: Mathlib.Analysis.SpecialFunctions.Artanh

Goal state before:
pp: x : ℝ
hx : x ∈ Icc (-1) 1
⊢ artanh x = 1 / 2 * log ((1 + x) / (1 - x))

Tactic:
by
  rw [artanh, log_sqrt <| div_nonneg (by grind) (by grind), one_div_mul_eq_div]

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

Goal state before:
pp: p : ℝ
⊢ binEntropy (1 - (2⁻¹ + p)) = binEntropy (2⁻¹ - p)

Tactic:
ring_nf

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

Goal state before:
pp: q : ℕ
tendstoBot : Tendsto (fun p ↦ log (↑q - 1) + log (1 - p) - log p) (𝓝[<] 1) atBot
a✝¹ : ℝ
a✝ : a✝¹ ∈ Ioo (1 - 2⁻¹) 1
⊢ a✝¹ ≠ 1

Tactic:
· simp_all only [mem_Ioo, ne_eq]
    linarith [two_inv_lt_one (α := ℝ)]

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

Goal state before:
pp: q : ℕ
tendstoTop : Tendsto (fun p ↦ log (↑q - 1) + log (1 - p) - log p) (𝓝[>] 0) atTop
a✝¹ : ℝ
a✝ : a✝¹ ∈ Ioo 0 2⁻¹
⊢ a✝¹ ≠ 1

Tactic:
· simp_all only [mem_Ioo, ne_eq]
    linarith [two_inv_lt_one (α := ℝ)]

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

Goal state before:
pp: case refine_1
n : ℕ
⊢ (sinPoly (n + 1)).natDegree ≤ n + 2

Tactic:
exact (sinPoly_natDegree_le (n + 1)).trans (by simp)

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

Goal state before:
pp: case a
q : ℕ
qLe2 : 2 ≤ q
p1 : ℝ
hp1 : p1 ∈ Icc (1 - 1 / ↑q) 1
p2 : ℝ
hp2 : p2 ∈ Icc (1 - 1 / ↑q) 1
p1le2 : p1 < p2
p : ℝ
this : 2 ≤ ↑q
qinv_lt_1 : (↑q)⁻¹ < 1
zero_lt_1_sub_p : 0 < 1 - p
hp : 1 - (↑q)⁻¹ < p ∧ p < 1
qpos : 0 < ↑q
⊢ (↑q - 1) * (1 - p) < p

Tactic:
ring_nf

Goal state after:
case a
q : ℕ
qLe2 : 2 ≤ q
p1 : ℝ
hp1 : p1 ∈ Icc (1 - 1 / ↑q) 1
p2 : ℝ
hp2 : p2 ∈ Icc (1 - 1 / ↑q) 1
p1le2 : p1 < p2
p : ℝ
this : 2 ≤ ↑q
qinv_lt_1 : (↑q)⁻¹ < 1
zero_lt_1_sub_p : 0 < 1 - p
hp : 1 - (↑q)⁻¹ < p ∧ p < 1
qpos : 0 < ↑q
⊢ -1 + ↑q - ↑q * p + p < p
Module: Mathlib.Analysis.SpecialFunctions.FrullaniIntegral

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
inst✝ : CompleteSpace E
hf : LocallyIntegrableOn f (Ioi 0) volume
ha : 0 < a
hb : 0 < b
V : E
δ : ℝ
hδ : 0 ≤ δ
h : ∀ x ∈ uIoc a b, ‖f x - V‖ ≤ δ
hsub : uIcc a b ⊆ Ioi 0
hint_f : IntervalIntegrable (fun x ↦ x⁻¹ • f x) volume a b
hint_V : IntervalIntegrable (fun x ↦ x⁻¹ • V) volume a b
hint_inv : IntervalIntegrable (fun x ↦ x⁻¹ * δ) volume a b
⊢ log (b / a) • V = ∫ (x : ℝ) in a..b, x⁻¹ • V

Tactic:
intervalIntegral.integral_smul_const (f := fun x ↦ (x⁻¹ : ℝ)) (c := V),

Goal state after:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
inst✝ : CompleteSpace E
hf : LocallyIntegrableOn f (Ioi 0) volume
ha : 0 < a
hb : 0 < b
V : E
δ : ℝ
hδ : 0 ≤ δ
h : ∀ x ∈ uIoc a b, ‖f x - V‖ ≤ δ
hsub : uIcc a b ⊆ Ioi 0
hint_f : IntervalIntegrable (fun x ↦ x⁻¹ • f x) volume a b
hint_V : IntervalIntegrable (fun x ↦ x⁻¹ • V) volume a b
hint_inv : IntervalIntegrable (fun x ↦ x⁻¹ * δ) volume a b
⊢ log (b / a) • V = (∫ (x : ℝ) in a..b, x⁻¹) • V
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Deligne

Goal state before:
pp: s : ℂ
| s.Gammaℝ⁻¹

Tactic:
Gammaℝ,

Goal state after:
s : ℂ
| (↑π ^ (-s / 2) * Gamma (s / 2))⁻¹
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Deligne

Goal state before:
pp: h : Tendsto (fun z ↦ z / 2 * Gamma (z / 2)) (𝓝[≠] 0) (𝓝 1)
h' : Tendsto (fun s ↦ 2 * ↑π ^ (-s / 2)) (𝓝[≠] 0) (𝓝 2)
z : ℂ
⊢ z * (↑π ^ (-z / 2) * Gamma (z / 2)) = 2 * ↑π ^ (-z / 2) * (z / 2 * Gamma (z / 2))

Tactic:
ring_nf

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)) =
    ↑π ^ (-s / 2) * ↑π ^ (-(s + 1) / 2) * (Gamma (s / 2) * Gamma (s / 2 + 1 / 2))

Tactic:
ring_nf

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

Goal state before:
pp: p x : ℝ
hp : p ∈ Ioo 0 1
hx : 0 ≤ x
⊢ HasFiniteIntegral (fun t ↦ t ^ (p - 1)) (volume.restrict (Ioo 0 1))

Tactic:
apply Integrable.hasFiniteIntegral
      rw [Set.mem_Ioo] at hp
      rw [← IntegrableOn, intervalIntegral.integrableOn_Ioo_rpow_iff]
      · linarith
      · exact zero_lt_one

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

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

Tactic:
ring_nf

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

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

Tactic:
ring_nf

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

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

Tactic:
ring_nf

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

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

Tactic:
ring_nf

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

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

Tactic:
ring_nf

Goal state after:
s : ℂ
⊢ ↑π ^ 0 * (cos (s * ↑π * (1 / 2)))⁻¹ = (cos (s * ↑π * (1 / 2)))⁻¹
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Deligne

Goal state before:
pp: case pos
s : ℂ
hs : ∀ (n : ℕ), s ≠ -↑n
h : s = 1
⊢ 1⁻¹ = Gammaℂ 1 * sin (↑π * 1 / 2) * (1 + 1).Gammaℝ⁻¹

Tactic:
Gammaℝ,

Goal state after:
case pos
s : ℂ
hs : ∀ (n : ℕ), s ≠ -↑n
h : s = 1
⊢ 1⁻¹ = Gammaℂ 1 * sin (↑π * 1 / 2) * (↑π ^ (-(1 + 1) / 2) * Gamma ((1 + 1) / 2))⁻¹
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation

Goal state before:
pp: p : ℝ
hp : 0 < p ∧ p < 1
⊢ 1 / 2 * -1 ^ (p - 1) / (p - 1) = ∫ (t : ℝ) in Ioi 1, 1 / 2 * t ^ (p - 2)

Tactic:
integral_const_mul,

Goal state after:
p : ℝ
hp : 0 < p ∧ p < 1
⊢ 1 / 2 * -1 ^ (p - 1) / (p - 1) = 1 / 2 * ∫ (a : ℝ) in Ioi 1, a ^ (p - 2)
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation

Goal state before:
pp: p : ℝ
hp : 0 < p ∧ p < 1
⊢ 1 / 2 * -1 ^ (p - 1) / (p - 1) = 1 / 2 * (-1 ^ (p - 2 + 1) / (p - 2 + 1))

Tactic:
ring_nf

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

Goal state before:
pp: ⊢ logDeriv Gamma 1 = -↑Real.eulerMascheroniConstant

Tactic:
logDeriv_apply,

Goal state after:
⊢ deriv Gamma 1 / Gamma 1 = -↑Real.eulerMascheroniConstant
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Digamma

Goal state before:
pp: ⊢ logDeriv Gamma (1 / 2) = -2 * log 2 - ↑Real.eulerMascheroniConstant

Tactic:
logDeriv_apply,

Goal state after:
⊢ deriv Gamma (1 / 2) / Gamma (1 / 2) = -2 * log 2 - ↑Real.eulerMascheroniConstant
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Digamma

Goal state before:
pp: s : ℂ
hs : ∀ (m : ℕ), s ≠ -↑m
hs0 : s ≠ 0
⊢ logDeriv Gamma (s + 1) = logDeriv Gamma s + s⁻¹

Tactic:
logDeriv_apply,

Goal state after:
s : ℂ
hs : ∀ (m : ℕ), s ≠ -↑m
hs0 : s ≠ 0
⊢ deriv Gamma (s + 1) / Gamma (s + 1) = logDeriv Gamma s + s⁻¹
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Digamma

Goal state before:
pp: s : ℂ
hs : ∀ (m : ℕ), s ≠ -↑m
hs0 : s ≠ 0
⊢ deriv Gamma (s + 1) / Gamma (s + 1) = logDeriv Gamma s + s⁻¹

Tactic:
logDeriv_apply,

Goal state after:
s : ℂ
hs : ∀ (m : ℕ), s ≠ -↑m
hs0 : s ≠ 0
⊢ deriv Gamma (s + 1) / Gamma (s + 1) = deriv Gamma s / Gamma s + s⁻¹
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 0 1
μ : 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
a✝ : Nontrivial A
p_pos : 0 < ↑p
f : ℝ → ℝ → ℝ := fun t ↦ (↑p).rpowIntegrand₀₁ t
maxr : ℝ := sSup (quasispectrum ℝ a)
maxr_nonneg : 0 ≤ maxr
bound : ℝ → ℝ := fun t ↦ ‖f t maxr‖
hf : ContinuousOn (Function.uncurry f) (Ioi 0 ×ˢ quasispectrum ℝ a)
t : ℝ
ht : t ∈ Ioi 0
z : ℝ
hz : z ∈ quasispectrum ℝ a
hz' : 0 ≤ z
⊢ (↑p).rpowIntegrand₀₁ t z ≤ ‖(↑p).rpowIntegrand₀₁ t maxr‖

Tactic:
Real.norm_of_nonneg (rpowIntegrand₀₁_nonneg p_pos (le_of_lt ht) maxr_nonneg)

Goal state after:
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 0 1
μ : 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
a✝ : Nontrivial A
p_pos : 0 < ↑p
f : ℝ → ℝ → ℝ := fun t ↦ (↑p).rpowIntegrand₀₁ t
maxr : ℝ := sSup (quasispectrum ℝ a)
maxr_nonneg : 0 ≤ maxr
bound : ℝ → ℝ := fun t ↦ ‖f t maxr‖
hf : ContinuousOn (Function.uncurry f) (Ioi 0 ×ˢ quasispectrum ℝ a)
t : ℝ
ht : t ∈ Ioi 0
z : ℝ
hz : z ∈ quasispectrum ℝ a
hz' : 0 ≤ z
⊢ (↑p).rpowIntegrand₀₁ t z ≤ (↑p).rpowIntegrand₀₁ t maxr
Module: Mathlib.Analysis.SpecialFunctions.Gaussian.PoissonSummation

Goal state before:
pp: a : ℝ
ha : a < 0
b s x : ℝ
⊢ -x - (a * x ^ 2 + b * x) = x * (-a * x - (b + 1))

Tactic:
ring_nf

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

Goal state before:
pp: a : ℂ
ha : a.re < 0
b : ℂ
s x : ℝ
⊢ ‖cexp (a * ↑x ^ 2 + b * ↑x)‖ = rexp (a.re * x ^ 2 + b.re * x)

Tactic:
Complex.norm_exp,

Goal state after:
a : ℂ
ha : a.re < 0
b : ℂ
s x : ℝ
⊢ rexp (a * ↑x ^ 2 + b * ↑x).re = rexp (a.re * x ^ 2 + b.re * x)
Module: Mathlib.Analysis.SpecialFunctions.Gaussian.PoissonSummation

Goal state before:
pp: a : ℂ
ha : a.re < 0
b : ℂ
s : ℝ
⊢ (fun x ↦ cexp (a * ↑x ^ 2 + b * ↑x)) =o[cocompact ℝ] fun x ↦ |x| ^ s

Tactic:
rw [cocompact_eq_atBot_atTop, isLittleO_sup]

Goal state after:
a : ℂ
ha : a.re < 0
b : ℂ
s : ℝ
⊢ ((fun x ↦ cexp (a * ↑x ^ 2 + b * ↑x)) =o[atBot] fun x ↦ |x| ^ s) ∧
    (fun x ↦ cexp (a * ↑x ^ 2 + b * ↑x)) =o[atTop] fun x ↦ |x| ^ s
Module: Mathlib.Analysis.SpecialFunctions.Gaussian.PoissonSummation

Goal state before:
pp: a : ℂ
ha : 0 < a.re
b : ℂ
f : ℝ → ℂ := fun x ↦ cexp (-↑π * a * ↑x ^ 2 + 2 * ↑π * b * ↑x)
hFf : 𝓕 f = fun x ↦ 1 / a ^ (1 / 2) * cexp (-↑π / a * (↑x + I * b) ^ 2)
h1 : 0 < (↑π * a).re
h2 : 0 < (↑π / a).re
f_bd : f =O[cocompact ℝ] fun x ↦ |x| ^ (-2)
x : ℝ
⊢ -↑π / a * (↑x + I * b) ^ 2 = -↑π / a * ↑x ^ 2 + -2 * ↑π * I * b / a * ↑x + ↑π * b ^ 2 / a

Tactic:
ring_nf

Goal state after:
a : ℂ
ha : 0 < a.re
b : ℂ
f : ℝ → ℂ := fun x ↦ cexp (-↑π * a * ↑x ^ 2 + 2 * ↑π * b * ↑x)
hFf : 𝓕 f = fun x ↦ 1 / a ^ (1 / 2) * cexp (-↑π / a * (↑x + I * b) ^ 2)
h1 : 0 < (↑π * a).re
h2 : 0 < (↑π / a).re
f_bd : f =O[cocompact ℝ] fun x ↦ |x| ^ (-2)
x : ℝ
⊢ -(↑π * a⁻¹ * ↑x * I * b * 2) - ↑π * a⁻¹ * ↑x ^ 2 - ↑π * a⁻¹ * I ^ 2 * b ^ 2 =
    -(↑π * a⁻¹ * ↑x * I * b * 2) - ↑π * a⁻¹ * ↑x ^ 2 + ↑π * a⁻¹ * b ^ 2
Module: Mathlib.NumberTheory.Harmonic.GammaDeriv

Goal state before:
pp: case e_a.e_a.e_a
h_diff : ∀ {s : ℝ}, 0 < s → DifferentiableAt ℝ Gamma s
h_diff' : ∀ {s : ℝ}, 0 < s → DifferentiableAt ℝ (fun s ↦ Gamma (2 * s)) s
⊢ -(2 * γ) = -2 * γ

Tactic:
neg_mul

Goal state after:
case e_a.e_a.e_a
h_diff : ∀ {s : ℝ}, 0 < s → DifferentiableAt ℝ Gamma s
h_diff' : ∀ {s : ℝ}, 0 < s → DifferentiableAt ℝ (fun s ↦ Gamma (2 * s)) s
⊢ -(2 * γ) = -(2 * γ)
Module: Mathlib.NumberTheory.Harmonic.GammaDeriv

Goal state before:

Tactic:
deriv Gamma (1 / 2)
  _ = (deriv (fun s ↦ Gamma s * Gamma (s + 1 / 2)) (1 / 2)) + √π * γ := by
    rw [deriv_fun_mul, Gamma_one_half_eq,
      add_assoc, ← mul_add, deriv_comp_add_const,
      (by norm_num : 1 / 2 + 1 / 2 = (1 : ℝ)), Gamma_one, mul_one,
      eulerMascheroniConstant_eq_neg_deriv, add_neg_cancel, mul_zero, add_zero]
    · apply h_diff; simp -- s = 1
    · exact ((h_diff (by simp)).hasDerivAt.comp_add_const).differentiableAt -- s = 1
  _ = (deriv (fun s ↦ Gamma (2 * s) * 2 ^ (1 - 2 * s) * √π) (1 / 2)) + √π * γ := by
    rw [funext Gamma_mul_Gamma_add_half]
  _ = √π * (deriv (fun s ↦ Gamma (2 * s) * 2 ^ (1 - 2 * s)) (1 / 2) + γ) := by
    rw [mul_comm √π, mul_comm √π, deriv_mul_const, add_mul]
    apply DifferentiableAt.mul
    · exact .comp (g := Gamma) _ (by apply h_diff; simp) -- s = 1
        (differentiableAt_id.const_mul _)
    · exact (differentiableAt_const _).rpow (by fun_prop) two_ne_zero
  _ = √π * (deriv (fun s ↦ Gamma (2 * s)) (1 / 2) +
              deriv (fun s : ℝ ↦ 2 ^ (1 - 2 * s)) (1 / 2) + γ) := by
    rw [deriv_fun_mul]
    · simp
    · exact h_diff' one_half_pos
    · exact DifferentiableAt.rpow (by fun_prop) (by fun_prop) two_ne_zero
  _ = √π * (-2 * γ + deriv (fun s : ℝ ↦ 2 ^ (1 - 2 * s)) (1 / 2) + γ) := by
    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
  _ = √π * (-2 * γ + -(2 * log 2) + γ) := by
    congr 3
    apply HasDerivAt.deriv
    have := HasDerivAt.rpow (hasDerivAt_const (1 / 2 : ℝ) (2 : ℝ))
      (?_ : HasDerivAt (fun s : ℝ ↦ 1 - 2 * s) (-2) (1 / 2)) two_pos
    · simpa
    simp_rw [mul_comm (2 : ℝ) _]
    apply HasDerivAt.const_sub
    exact hasDerivAt_mul_const (2 : ℝ)
  _ = -√π * (γ + 2 * log 2) := by ring

Goal state after:
Module: Mathlib.Data.Int.Log

Goal state before:
pp: case inr
R : Type u_1
inst✝³ : Semifield R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorSemiring R
b : ℕ
hb : 1 < b
r : R
hr : 0 < r
⊢ ↑b ^ log b r⁻¹ ≤ r⁻¹

Tactic:
exact zpow_log_le_self hb (inv_pos.mpr hr)

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

Goal state before:
pp: b x : ℝ
hb : 1 < b
hx : 0 < x
⊢ 0 < logb b x ↔ 1 < x

Tactic:
← @logb_one b

Goal state after:
b x : ℝ
hb : 1 < b
hx : 0 < x
⊢ logb b 1 < logb b x ↔ 1 < x
Module: Mathlib.Data.Int.Log

Goal state before:
pp: R : Type u_1
inst✝³ : Semifield R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorSemiring R
b : ℕ
hb : 1 < b
z : ℤ
⊢ clog b (↑b ^ z) = z

Tactic:
rw [← neg_log_inv_eq_clog, ← zpow_neg, log_zpow hb, neg_neg]

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

Goal state before:
pp: b x y : ℝ
b_pos : 0 < b
b_lt_one : b < 1
hy : 0 < y
⊢ b ^ logb b y ≤ b ^ x ↔ y ≤ b ^ x

Tactic:
rpow_logb b_pos (b_ne_one b_lt_one) hy

Goal state after:
b x y : ℝ
b_pos : 0 < b
b_lt_one : b < 1
hy : 0 < y
⊢ y ≤ b ^ x ↔ y ≤ b ^ x
Module: Mathlib.Analysis.SpecialFunctions.Log.Base

Goal state before:
pp: b x y : ℝ
b_pos : 0 < b
b_lt_one : b < 1
hy : 0 < y
⊢ b ^ logb b y < b ^ x ↔ y < b ^ x

Tactic:
rpow_logb b_pos (b_ne_one b_lt_one) hy

Goal state after:
b x y : ℝ
b_pos : 0 < b
b_lt_one : b < 1
hy : 0 < y
⊢ y < b ^ x ↔ y < b ^ x
Module: Mathlib.Analysis.SpecialFunctions.MulExpNegMulSq

Goal state before:
pp: ε : ℝ
hε : 0 < ε
x y : ℝ
h : edist (ε.mulExpNegMulSq x) (ε.mulExpNegMulSq y) ≤ edist x y
⊢ dist (ε.mulExpNegMulSq x) (ε.mulExpNegMulSq y) ≤ dist x y

Tactic:
← (toReal_le_toReal (edist_ne_top _ _) (edist_ne_top _ _))

Goal state after:
ε : ℝ
hε : 0 < ε
x y : ℝ
h : (edist (ε.mulExpNegMulSq x) (ε.mulExpNegMulSq y)).toReal ≤ (edist x y).toReal
⊢ dist (ε.mulExpNegMulSq x) (ε.mulExpNegMulSq y) ≤ dist x y
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: L : PeriodPair
α β : ℚ
H : ↑α * L.ω₁ + ↑β * L.ω₂ ∈ L.lattice
m n : ℤ
e : ↑m * L.ω₁ + ↑n * L.ω₂ = ↑α * L.ω₁ + ↑β * L.ω₂
⊢ (↑m - ↑α) • L.ω₁ + (↑n - ↑β) • L.ω₂ = 0

Tactic:
by simp; linear_combination e

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: case e_a
r : ℝ
hr : 0 < r
s : ℂ
hs : ‖s‖ < r
l : ℂ
h : 2 * r ≤ ‖l‖
this✝ : s ≠ l
this : 0 < ‖l‖
⊢ ‖l ^ 2 - (s - l) ^ 2‖ = ‖s * (2 * l - s)‖

Tactic:
rw [sq_sub_sq]

Goal state after:
case e_a
r : ℝ
hr : 0 < r
s : ℂ
hs : ‖s‖ < r
l : ℂ
h : 2 * r ≤ ‖l‖
this✝ : s ≠ l
this : 0 < ‖l‖
⊢ ‖(l + (s - l)) * (l - (s - l))‖ = ‖s * (2 * l - s)‖
Module: Mathlib.Analysis.SpecialFunctions.Pow.NthRootLemmas

Goal state before:
pp: n a b : ℕ
hn : n ≠ 0
⊢ a ≤ n.nthRoot b ↔ a ^ n ≤ b

Tactic:
by
  cases le_or_gt a (nthRoot n b) with
  | inl hle =>
    simp only [hle, true_iff]
    refine le_trans ?_ (pow_nthRoot_le (.inl hn))
    gcongr
  | inr hlt =>
    simp only [hlt.not_ge, false_iff, not_le]
    refine (lt_pow_nthRoot_add_one hn b).trans_le ?_
    gcongr
    assumption

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

Goal state before:
pp: a b : Multiset ℂ
h : a.card ≤ b.card
ha : ∀ j ∈ a, ∀ (k : ℕ), j ≠ -↑k
this : Tendsto (fun x ↦ (1 / ↑x) ^ (b.card + 1 - a.card)) atTop (𝓝 0)
n : ℕ
⊢ ↑n ^ (-(↑b.card + 1 - ↑a.card)) = ↑n ^ (↑a.card - ↑b.card - 1)

Tactic:
ring_nf

Goal state after:
Module: Mathlib.MeasureTheory.Constructions.HaarToSphere

Goal state before:
pp: E : Type u_1
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : MeasurableSpace E
F : Type u_2
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : Nontrivial E
μ : Measure E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : BorelSpace E
inst✝ : μ.IsAddHaarMeasure
f : ℝ → F
r : ℝ
⊢ Integrable ((Ioo 0 r).indicator fun y ↦ y ^ (dim E - 1) • f y) volume ↔
    IntegrableOn (fun y ↦ y ^ (dim E - 1) • f y) (Ioo 0 r) volume

Tactic:
by
      rw [← integrable_indicator_iff measurableSet_Ioo, ← integrableOn_univ]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Basic

Goal state before:
pp: case add_two
θ : ℂ
n : ℕ
ih1 : eval (cos θ) (T ℂ (↑n + 1)) = cos (↑(↑n + 1) * θ)
ih2 : eval (cos θ) (T ℂ ↑n) = cos (↑↑n * θ)
⊢ 2 * cos θ * cos ((↑n + 1) * θ) = 2 * cos (((↑n + 2) * θ + ↑n * θ) / 2) * cos (((↑n + 2) * θ - ↑n * θ) / 2)

Tactic:
ring_nf

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Basic

Goal state before:
pp: case neg_add_one
θ : ℂ
n : ℕ
ih1 : eval (cos θ) (T ℂ (-↑n)) = cos (↑(-↑n) * θ)
ih2 : eval (cos θ) (T ℂ (-↑n + 1)) = cos (↑(-↑n + 1) * θ)
⊢ 2 * cos θ * cos (-↑n * θ) = 2 * cos (((-↑n + 1) * θ + (-↑n - 1) * θ) / 2) * cos (((-↑n + 1) * θ - (-↑n - 1) * θ) / 2)

Tactic:
ring_nf

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Basic

Goal state before:
pp: case add_two
θ : ℂ
n : ℕ
ih1 : eval (cos θ) (U ℂ (↑n + 1)) * sin θ = sin ((↑(↑n + 1) + 1) * θ)
ih2 : eval (cos θ) (U ℂ ↑n) * sin θ = sin ((↑↑n + 1) * θ)
⊢ 2 * (cos θ * sin ((↑n + 1 + 1) * θ)) =
    2 * (sin (((↑n + 2 + 1) * θ + (↑n + 1) * θ) / 2) * cos (((↑n + 2 + 1) * θ - (↑n + 1) * θ) / 2))

Tactic:
ring_nf

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Basic

Goal state before:
pp: case neg_add_one
θ : ℂ
n : ℕ
ih1 : eval (cos θ) (U ℂ (-↑n)) * sin θ = sin ((↑(-↑n) + 1) * θ)
ih2 : eval (cos θ) (U ℂ (-↑n + 1)) * sin θ = sin ((↑(-↑n + 1) + 1) * θ)
⊢ 2 * (cos θ * sin ((-↑n + 1) * θ)) =
    2 * (sin (((-↑n + 1 + 1) * θ + (-↑n - 1 + 1) * θ) / 2) * cos (((-↑n + 1 + 1) * θ - (-↑n - 1 + 1) * θ) / 2))

Tactic:
ring_nf

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: L : PeriodPair
l₀ x : ℂ
i : ℕ
hl₀ : l₀ ∈ L.lattice
⊢ (if i + 1 = 0 then ℘[L - l₀] x else (↑(i + 1) + 1) * (L.sumInvPow x (i + 1 + 2) - ((l₀ - x) ^ (i + 1 + 2))⁻¹)) =
    (↑i + 2) * (L.sumInvPow x (i + 3) - ((l₀ - x) ^ ↑(i + 3))⁻¹)

Tactic:
zpow_natCast

Goal state after:
L : PeriodPair
l₀ x : ℂ
i : ℕ
hl₀ : l₀ ∈ L.lattice
⊢ (if i + 1 = 0 then ℘[L - l₀] x else (↑(i + 1) + 1) * (L.sumInvPow x (i + 1 + 2) - ((l₀ - x) ^ (i + 1 + 2))⁻¹)) =
    (↑i + 2) * (L.sumInvPow x (i + 3) - ((l₀ - x) ^ (i + 3))⁻¹)