mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.SpecialFunctions.Log.RpowTendsto

Goal state before:
pp: case h₂
s : Set ℝ
hs : s ⊆ Ioi 0
hs' : IsCompact s
ε : ℝ
hε : 0 < ε
pbound : ℝ := ⋯
hxs : ∀ x ∈ s, x ≠ 0
sSup_nonneg : 0 ≤ sSup ((fun x ↦ ‖log x‖ ^ 2) '' s)
sSup_nonneg' : 0 ≤ sSup ((fun x ↦ ‖log x‖) '' s)
pbound_pos : 0 < pbound
h₁ : ∀ᶠ (p : ℝ) in 𝓝[>] 0, 0 < p ∧ p < pbound
h₂ : ∀ᶠ (p : ℝ) in 𝓝[>] 0, p ≤ 1 / (sSup ((fun x ↦ ‖log x‖) '' s) + 1)
hcont : ContinuousOn (fun x ↦ ‖log x‖ ^ 2) s
hcont' : ContinuousOn (fun x ↦ ‖log x‖) s
p : ℝ
hp₁ : 0 < p
hp₂ : p < pbound
hp₃ : p ≤ 1 / (sSup ((fun x ↦ ‖log x‖) '' s) + 1)
x : ℝ
hx : x ∈ s
hx' : ‖p * log x‖ ≤ 1
pinv_nonneg : 0 ≤ p⁻¹
⊢ sSup ((fun x ↦ ‖log x‖ ^ 2) '' s) ≤ sSup ((fun x ↦ ‖log x‖ ^ 2) '' s) + 1

Tactic:
;

Goal state after:
case h₂
s : Set ℝ
hs : s ⊆ Ioi 0
hs' : IsCompact s
ε : ℝ
hε : 0 < ε
pbound : ℝ := ⋯
hxs : ∀ x ∈ s, x ≠ 0
sSup_nonneg : 0 ≤ sSup ((fun x ↦ ‖log x‖ ^ 2) '' s)
sSup_nonneg' : 0 ≤ sSup ((fun x ↦ ‖log x‖) '' s)
pbound_pos : 0 < pbound
h₁ : ∀ᶠ (p : ℝ) in 𝓝[>] 0, 0 < p ∧ p < pbound
h₂ : ∀ᶠ (p : ℝ) in 𝓝[>] 0, p ≤ 1 / (sSup ((fun x ↦ ‖log x‖) '' s) + 1)
hcont : ContinuousOn (fun x ↦ ‖log x‖ ^ 2) s
hcont' : ContinuousOn (fun x ↦ ‖log x‖) s
p : ℝ
hp₁ : 0 < p
hp₂ : p < pbound
hp₃ : p ≤ 1 / (sSup ((fun x ↦ ‖log x‖) '' s) + 1)
x : ℝ
hx : x ∈ s
hx' : ‖p * log x‖ ≤ 1
pinv_nonneg : 0 ≤ p⁻¹
⊢ sSup ((fun x ↦ ‖log x‖ ^ 2) '' s) ≤ sSup ((fun x ↦ ‖log x‖ ^ 2) '' s) + 1
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.RingInverseOrder

Goal state before:
pp: case h.refine_1
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
x : A
xpos : IsStrictlyPositive x
y : A
ypos : IsStrictlyPositive y
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
z : A := ⋯
zpos : IsStrictlyPositive z
xinvpos : IsStrictlyPositive x⁻¹ʳ
hsp : IsStrictlyPositive (a • 1 + b • z)
h₁ : (a • 1 + b • z) ^ (-1) = cfc (fun r ↦ (a + b * r) ^ (-1)) z
h₂ : a • 1 + b • z ^ (-1) = cfc (fun r ↦ a + b * r ^ (-1)) z
⊢ ∀ x ∈ spectrum ℝ z, a + b * x ≠ 0 ∨ 0 ≤ -1

Tactic:
intro r

Goal state after:
case h.refine_1
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
x : A
xpos : IsStrictlyPositive x
y : A
ypos : IsStrictlyPositive y
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
z : A := (conjSqrt x⁻¹ʳ) y
zpos : IsStrictlyPositive z
xinvpos : IsStrictlyPositive x⁻¹ʳ
hsp : IsStrictlyPositive (a • 1 + b • z)
h₁ : (a • 1 + b • z) ^ (-1) = cfc (fun r ↦ (a + b * r) ^ (-1)) z
h₂ : a • 1 + b • z ^ (-1) = cfc (fun r ↦ a + b * r ^ (-1)) z
r : ℝ
⊢ r ∈ spectrum ℝ z → a + b * r ≠ 0 ∨ 0 ≤ -1
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.RingInverseOrder

Goal state before:
pp: case h.refine_3
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
x : A
xpos : IsStrictlyPositive x
y : A
ypos : IsStrictlyPositive y
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
z : A := (conjSqrt x⁻¹ʳ) y
zpos : IsStrictlyPositive z
xinvpos : IsStrictlyPositive x⁻¹ʳ
hsp : IsStrictlyPositive (a • 1 + b • z)
h₁ : (a • 1 + b • z) ^ (-1) = cfc (fun r ↦ (a + b * r) ^ (-1)) z
h₂ : a • 1 + b • z ^ (-1) = cfc (fun r ↦ a + b * r ^ (-1)) z
⊢ ∀ x ∈ spectrum ℝ z, (a + b * x) ^ (-1) ≤ a + b * x ^ (-1)

Tactic:
intro r

Goal state after:
case h.refine_3
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
x : A
xpos : IsStrictlyPositive x
y : A
ypos : IsStrictlyPositive y
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
z : A := (conjSqrt x⁻¹ʳ) y
zpos : IsStrictlyPositive z
xinvpos : IsStrictlyPositive x⁻¹ʳ
hsp : IsStrictlyPositive (a • 1 + b • z)
h₁ : (a • 1 + b • z) ^ (-1) = cfc (fun r ↦ (a + b * r) ^ (-1)) z
h₂ : a • 1 + b • z ^ (-1) = cfc (fun r ↦ a + b * r ^ (-1)) z
r : ℝ
⊢ r ∈ spectrum ℝ z → (a + b * r) ^ (-1) ≤ a + b * r ^ (-1)
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation

Goal state before:
pp: case e_a.e_a
p t x : ℝ
hp : p ∈ Ioo 0 1
ht : 0 ≤ t
hx : 0 ≤ x
ht' : ¬t = 0
hxt : t + x ≠ 0
⊢ t ^ p / t = t ^ (p - 1)

Tactic:
;

Goal state after:
case e_a.e_a
p t x : ℝ
hp : p ∈ Ioo 0 1
ht : 0 ≤ t
hx : 0 ≤ x
ht' : ¬t = 0
hxt : t + x ≠ 0
⊢ t ^ p / t = t ^ (p - 1)
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.RingInverseOrder

Goal state before:
pp: A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
t : ℝ
ht : 0 < t
this : ∀ x ∈ Ici 0, IsStrictlyPositive ((algebraMap ℝ A) t + x)
addl : A →ᵃ[ℝ] A := (AffineMap.toConstProdLinearMap ℝ).symm ((algebraMap ℝ A) t, LinearMap.id)
a₁✝ a₂✝ : A
⊢ addl a₁✝ = addl a₂✝ → a₁✝ = a₂✝

Tactic:
;

Goal state after:
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
t : ℝ
ht : 0 < t
this : ∀ x ∈ Ici 0, IsStrictlyPositive ((algebraMap ℝ A) t + x)
addl : A →ᵃ[ℝ] A := (AffineMap.toConstProdLinearMap ℝ).symm ((algebraMap ℝ A) t, LinearMap.id)
a₁✝ a₂✝ : A
⊢ addl a₁✝ = addl a₂✝ → a₁✝ = a₂✝
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Deligne

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

Tactic:
;

Goal state after:
s : ℂ
| s.Gammaℝ⁻¹
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation

Goal state before:
pp: case hdb
p t x : ℝ
hp : p ∈ Ioo 0 1
ht : 0 < t
hx : 0 ≤ x
⊢ t ≤ t + x

Tactic:
;

Goal state after:
case hdb
p t x : ℝ
hp : p ∈ Ioo 0 1
ht : 0 < t
hx : 0 ≤ x
⊢ t ≤ t + x
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Deligne

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

Tactic:
;

Goal state after:
s : ℂ
| s.Gammaℂ⁻¹
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation

Goal state before:
pp: case hdb
p t x : ℝ
hp : p ∈ Ioo 0 1
ht : 0 ≤ t
hx : 0 ≤ x
hx_zero : ¬x = 0
⊢ x ≤ t + x

Tactic:
;

Goal state after:
case hdb
p t x : ℝ
hp : p ∈ Ioo 0 1
ht : 0 ≤ t
hx : 0 ≤ x
hx_zero : ¬x = 0
⊢ x ≤ t + x
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation

Goal state before:
pp: case e_a
p t x : ℝ
hp : p ∈ Ioo 0 1
ht : 0 ≤ t
hx : 0 ≤ x
hx_zero : ¬x = 0
⊢ x / x = 1

Tactic:
;

Goal state after:
case e_a
p t x : ℝ
hp : p ∈ Ioo 0 1
ht : 0 ≤ t
hx : 0 ≤ x
hx_zero : ¬x = 0
⊢ x / x = 1
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation

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

Tactic:
rw [← IntegrableOn, intervalIntegral.integrableOn_Ioo_rpow_iff]

Goal state after:
p x : ℝ
hp : 0 < p ∧ p < 1
hx : 0 ≤ x
⊢ -1 < p - 1

p x : ℝ
hp : 0 < p ∧ p < 1
hx : 0 ≤ x
⊢ 0 < 1
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Deligne

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

Tactic:
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

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

Goal state before:
pp: case hft
p x : ℝ
hp : p ∈ Ioo 0 1
hx✝ : 0 ≤ x
hx : 0 < x
this :
  ∫ (t : ℝ) in Ioi 0, ((fun x_1 ↦ p.rpowIntegrand₀₁ x_1 x) ∘ fun x_1 ↦ x * x_1) t * x =
    x ^ p * ∫ (t : ℝ) in Ioi 0, p.rpowIntegrand₀₁ t 1
⊢ Tendsto (fun x_1 ↦ x * x_1) atTop atTop

Tactic:
exact tendsto_id.const_mul_atTop hx

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

Goal state before:
pp: p : ℝ
hp : p ∈ Ioo 0 1
⊢ -1 / 2 / (p - 1) = 1 / 2 * -1 ^ (p - 1) / (p - 1)

Tactic:
;

Goal state after:
p : ℝ
hp : p ∈ Ioo 0 1
⊢ -1 / 2 / (p - 1) = 1 / 2 * -1 ^ (p - 1) / (p - 1)
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation

Goal state before:
pp: p : ℝ
hp : p ∈ Ioo 0 1
⊢ 0 ≤ ∫ (t : ℝ) in Ioi 0, p.rpowIntegrand₀₁ t 1

Tactic:
;

Goal state after:
p : ℝ
hp : p ∈ Ioo 0 1
⊢ 0 ≤ ∫ (t : ℝ) in Ioi 0, p.rpowIntegrand₀₁ t 1
Module: Mathlib.NumberTheory.Harmonic.GammaDeriv

Goal state before:
pp: n✝ : ℕ
f : ℝ → ℝ := log ∘ Gamma
hc : ConvexOn ℝ (Ioi 0) f
h_rec : ∀ (x : ℝ), 0 < x → f (x + 1) = f x + log x
hder : ∀ {x : ℝ}, 0 < x → DifferentiableAt ℝ f x
hder_rec : ∀ (x : ℝ), 0 < x → deriv f (x + 1) = deriv f x + 1 / x
hder_nat : ∀ (n : ℕ), deriv f (↑n + 1) = deriv f 1 + ↑(harmonic n)
n : ℕ
hn : 0 < n
⊢ log ↑n = slope f (↑n) (↑n + 1)

Tactic:
slope_def_field,

Goal state after:
n✝ : ℕ
f : ℝ → ℝ := log ∘ Gamma
hc : ConvexOn ℝ (Ioi 0) f
h_rec : ∀ (x : ℝ), 0 < x → f (x + 1) = f x + log x
hder : ∀ {x : ℝ}, 0 < x → DifferentiableAt ℝ f x
hder_rec : ∀ (x : ℝ), 0 < x → deriv f (x + 1) = deriv f x + 1 / x
hder_nat : ∀ (n : ℕ), deriv f (↑n + 1) = deriv f 1 + ↑(harmonic n)
n : ℕ
hn : 0 < n
⊢ log ↑n = (f (↑n + 1) - f ↑n) / (↑n + 1 - ↑n)
Module: Mathlib.NumberTheory.Harmonic.GammaDeriv

Goal state before:
pp: n✝ : ℕ
f : ℝ → ℝ := log ∘ Gamma
hc : ConvexOn ℝ (Ioi 0) f
h_rec : ∀ (x : ℝ), 0 < x → f (x + 1) = f x + log x
hder : ∀ {x : ℝ}, 0 < x → DifferentiableAt ℝ f x
hder_rec : ∀ (x : ℝ), 0 < x → deriv f (x + 1) = deriv f x + 1 / x
hder_nat : ∀ (n : ℕ), deriv f (↑n + 1) = deriv f 1 + ↑(harmonic n)
derivLB : ∀ (n : ℕ), 0 < n → log ↑n ≤ deriv f (↑n + 1)
n : ℕ
⊢ slope f (↑n + 1) (↑n + 2) = log (↑n + 1)

Tactic:
slope_def_field,

Goal state after:
n✝ : ℕ
f : ℝ → ℝ := log ∘ Gamma
hc : ConvexOn ℝ (Ioi 0) f
h_rec : ∀ (x : ℝ), 0 < x → f (x + 1) = f x + log x
hder : ∀ {x : ℝ}, 0 < x → DifferentiableAt ℝ f x
hder_rec : ∀ (x : ℝ), 0 < x → deriv f (x + 1) = deriv f x + 1 / x
hder_nat : ∀ (n : ℕ), deriv f (↑n + 1) = deriv f 1 + ↑(harmonic n)
derivLB : ∀ (n : ℕ), 0 < n → log ↑n ≤ deriv f (↑n + 1)
n : ℕ
⊢ (f (↑n + 2) - f (↑n + 1)) / (↑n + 2 - (↑n + 1)) = log (↑n + 1)
Module: Mathlib.NumberTheory.Harmonic.GammaDeriv

Goal state before:
pp: case hc
h_diff : ∀ {s : ℝ}, 0 < s → DifferentiableAt ℝ Gamma s
h_diff' : ∀ {s : ℝ}, 0 < s → DifferentiableAt ℝ (fun s ↦ Gamma (2 * s)) s
⊢ 0 < 1 / 2

Tactic:
;

Goal state after:
case hc
h_diff : ∀ {s : ℝ}, 0 < s → DifferentiableAt ℝ Gamma s
h_diff' : ∀ {s : ℝ}, 0 < s → DifferentiableAt ℝ (fun s ↦ Gamma (2 * s)) s
⊢ 0 < 1 / 2
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:
;

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

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

Tactic:
mul_comm _ (re _)

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
⊢ 0 < 2 * (1 / 2)

Tactic:
;

Goal state after:
h_diff : ∀ {s : ℝ}, 0 < s → DifferentiableAt ℝ Gamma s
h_diff' : ∀ {s : ℝ}, 0 < s → DifferentiableAt ℝ (fun s ↦ Gamma (2 * s)) s
⊢ 0 < 2 * (1 / 2)
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:
;

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 + -2 * ↑π * I * b / a * ↑x + ↑π * b ^ 2 / a
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 - ↑π * a⁻¹ * I ^ 2 * b ^ 2 =
    -(↑π * a⁻¹ * ↑x * I * b * 2) - ↑π * a⁻¹ * ↑x ^ 2 + ↑π * a⁻¹ * b ^ 2

Tactic:
;

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.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 - ↑π * a⁻¹ * -1 * b ^ 2 =
    -(↑π * a⁻¹ * ↑x * I * b * 2) - ↑π * a⁻¹ * ↑x ^ 2 + ↑π * a⁻¹ * b ^ 2

Tactic:
;

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⁻¹ * -1 * 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.hh₂
h_diff : ∀ {s : ℝ}, 0 < s → DifferentiableAt ℝ Gamma s
h_diff' : ∀ {s : ℝ}, 0 < s → DifferentiableAt ℝ (fun s ↦ Gamma (2 * s)) s
⊢ 0 < 2 * (1 / 2)

Tactic:
;

Goal state after:
case e_a.e_a.e_a.hh₂
h_diff : ∀ {s : ℝ}, 0 < s → DifferentiableAt ℝ Gamma s
h_diff' : ∀ {s : ℝ}, 0 < s → DifferentiableAt ℝ (fun s ↦ Gamma (2 * s)) s
⊢ 0 < 2 * (1 / 2)
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)
this : ∀ (x : ℝ), -↑π / a * (↑x + I * b) ^ 2 = -↑π / a * ↑x ^ 2 + -2 * ↑π * I * b / a * ↑x + ↑π * b ^ 2 / a
x : ℝ
| 1 / a ^ (1 / 2) * cexp (-↑π / a * ↑x ^ 2 + -2 * ↑π * I * b / a * ↑x + ↑π * b ^ 2 / a)

Tactic:
;

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)
this : ∀ (x : ℝ), -↑π / a * (↑x + I * b) ^ 2 = -↑π / a * ↑x ^ 2 + -2 * ↑π * I * b / a * ↑x + ↑π * b ^ 2 / a
x : ℝ
| 1 / a ^ (1 / 2) * cexp (-↑π / a * ↑x ^ 2 + -2 * ↑π * I * b / a * ↑x + ↑π * b ^ 2 / a)
Module: Mathlib.NumberTheory.Harmonic.GammaDeriv

Goal state before:
pp: f : ℂ → ℂ := fun s ↦ ↑π ^ (-s / 2)
g : ℂ → ℂ := fun s ↦ Gamma (s / 2)
aux : ↑π ^ (1 / 2) = ↑√π
⊢ √π ≠ 0

Tactic:
;

Goal state after:
f : ℂ → ℂ := fun s ↦ ↑π ^ (-s / 2)
g : ℂ → ℂ := fun s ↦ Gamma (s / 2)
aux : ↑π ^ (1 / 2) = ↑√π
⊢ √π ≠ 0
Module: Mathlib.Analysis.SpecialFunctions.Log.Base

Goal state before:
pp: x✝ : ℝ
⊢ logb 0 x✝ = 0 x✝

Tactic:
;

Goal state after:
x✝ : ℝ
⊢ logb 0 x✝ = 0 x✝
Module: Mathlib.Analysis.SpecialFunctions.Log.Base

Goal state before:
pp: x✝ : ℝ
⊢ logb 1 x✝ = 0 x✝

Tactic:
;

Goal state after:
x✝ : ℝ
⊢ logb 1 x✝ = 0 x✝
Module: Mathlib.Analysis.SpecialFunctions.Log.Base

Goal state before:
pp: b x : ℝ
⊢ logb (-b) x = logb b x

Tactic:
;

Goal state after:
b x : ℝ
⊢ logb (-b) x = logb b x
Module: Mathlib.Analysis.SpecialFunctions.Log.Base

Goal state before:
pp: b : ℝ
⊢ logb (-b) = logb b

Tactic:
by
  ext x; rw [← logb_abs_base b x, ← logb_abs_base (-b) x, abs_neg]

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

Goal state before:
pp: a b : ℝ
h₁ : a ≠ 0
h₂ : b ≠ 0
c : ℝ
⊢ logb c (a * b) = logb c a + logb c b

Tactic:
;

Goal state after:
a b : ℝ
h₁ : a ≠ 0
h₂ : b ≠ 0
c : ℝ
⊢ logb c (a * b) = logb c a + logb c b
Module: Mathlib.Analysis.SpecialFunctions.Log.Base

Goal state before:
pp: a b : ℝ
h₁ : a ≠ 0
h₂ : b ≠ 0
c : ℝ
⊢ logb c (a / b) = logb c a - logb c b

Tactic:
;

Goal state after:
a b : ℝ
h₁ : a ≠ 0
h₂ : b ≠ 0
c : ℝ
⊢ logb c (a / b) = logb c a - logb c b
Module: Mathlib.Analysis.SpecialFunctions.Log.Base

Goal state before:
pp: case a
b x : ℝ
b_pos : 0 < b
b_ne_one : b ≠ 1
hx : x ≠ 0
⊢ log x / log b * log b = log x

Tactic:
field [log_ne_zero_of_pos_of_ne_one b_pos b_ne_one]

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

Goal state before:
pp: ⊢ MonotoneOn (fun x ↦ log x * x) {x | 1 ≤ x}

Tactic:
by
  grind [mul_log_strictMonoOn.monotoneOn, MonotoneOn.mono, show exp (-1) < 1 by norm_num]

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

Goal state before:
pp: ε : ℝ
hε : 0 < ε
x : ℝ
⊢ ε.mulExpNegMulSq x = (√ε)⁻¹ * mulExpNegMulSq 1 (√ε * x)

Tactic:
by
  grind [mulExpNegMulSq]

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

Goal state before:
pp: X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : MeasurableSpace X
inst✝ : OpensMeasurableSpace X
f : X →ᵇ ℝ≥0
μ : Measure X
⊢ (∫⁻ (x : X), ↑(f x) ∂μ).toReal = ∫ (x : X), ↑(f x) ∂μ

Tactic:
rw [integral_eq_lintegral_of_nonneg_ae _ (by simpa [Function.comp_apply] using!
        (NNReal.continuous_coe.comp f.continuous).measurable.aestronglyMeasurable)]
  · simp only [ENNReal.ofReal_coe_nnreal]
  · exact Eventually.of_forall (by simp)

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

Goal state before:
pp: case _a
X : Type u_1
inst✝² : MeasurableSpace X
inst✝¹ : TopologicalSpace X
μ : Measure X
E : Type u_2
inst✝ : NormedAddCommGroup E
f : X →ᵇ E
x : X
⊢ ‖f x‖₊ ≤ ‖f‖₊

Tactic:
;

Goal state after:
case _a
X : Type u_1
inst✝² : MeasurableSpace X
inst✝¹ : TopologicalSpace X
μ : Measure X
E : Type u_2
inst✝ : NormedAddCommGroup E
f : X →ᵇ E
x : X
⊢ ‖f x‖₊ ≤ ‖f‖₊
Module: Mathlib.MeasureTheory.Measure.RegularityCompacts

Goal state before:
pp: α : Type u_1
inst✝⁵ : MeasurableSpace α
inst✝⁴ : TopologicalSpace α
inst✝³ : SecondCountableTopology α
inst✝² : IsCompletelyPseudoMetrizableSpace α
inst✝¹ : OpensMeasurableSpace α
P : Measure α
inst✝ : IsFiniteMeasure P
ε : ℝ≥0∞
hε : 0 < ε
this : UpgradedIsCompletelyPseudoMetrizableSpace α := upgradeIsCompletelyPseudoMetrizable α
h✝ : Nonempty α
seq : ℕ → α := denseSeq α
hseq_dense : DenseRange seq
t : ℕ → SetRel α α
h_basis : (𝓤 α).HasAntitoneBasis t
htu : ∀ (i : ℕ), t i ∈ 𝓤 α
hto : ∀ (i : ℕ), IsOpen (t i)
a✝ : ∀ (i : ℕ), (t i).IsSymm
f : ℕ → ℕ → Set α := fun n m ↦ UniformSpace.ball (seq m) (t n)
h_univ : ∀ (n : ℕ), ⋃ m, f n m = univ
s' : ℕ → ℝ≥0∞ → ℕ
s'bound : ∀ (n : ℕ) (ε : ℝ≥0∞), 0 < ε → P (⋂ m', ⋂ (_ : m' ≤ s' n ε), (f n m')ᶜ) < ε
δ : ℕ → ℝ≥0∞
hδ1 : ∀ (i : ℕ), 0 < δ i
hδ2 : ∑' (i : ℕ), δ i < ε
u : ℕ → ℕ := fun n ↦ s' n (δ n)
n✝ n : ℕ
x✝ : α × α
⊢ x✝ ∈ Prod.swap ⁻¹' t n ↔ x✝ ∈ t n

Tactic:
;

Goal state after:
α : Type u_1
inst✝⁵ : MeasurableSpace α
inst✝⁴ : TopologicalSpace α
inst✝³ : SecondCountableTopology α
inst✝² : IsCompletelyPseudoMetrizableSpace α
inst✝¹ : OpensMeasurableSpace α
P : Measure α
inst✝ : IsFiniteMeasure P
ε : ℝ≥0∞
hε : 0 < ε
this : UpgradedIsCompletelyPseudoMetrizableSpace α := upgradeIsCompletelyPseudoMetrizable α
h✝ : Nonempty α
seq : ℕ → α := denseSeq α
hseq_dense : DenseRange seq
t : ℕ → SetRel α α
h_basis : (𝓤 α).HasAntitoneBasis t
htu : ∀ (i : ℕ), t i ∈ 𝓤 α
hto : ∀ (i : ℕ), IsOpen (t i)
a✝ : ∀ (i : ℕ), (t i).IsSymm
f : ℕ → ℕ → Set α := fun n m ↦ UniformSpace.ball (seq m) (t n)
h_univ : ∀ (n : ℕ), ⋃ m, f n m = univ
s' : ℕ → ℝ≥0∞ → ℕ
s'bound : ∀ (n : ℕ) (ε : ℝ≥0∞), 0 < ε → P (⋂ m', ⋂ (_ : m' ≤ s' n ε), (f n m')ᶜ) < ε
δ : ℕ → ℝ≥0∞
hδ1 : ∀ (i : ℕ), 0 < δ i
hδ2 : ∑' (i : ℕ), δ i < ε
u : ℕ → ℕ := fun n ↦ s' n (δ n)
n✝ n : ℕ
x✝ : α × α
⊢ x✝ ∈ Prod.swap ⁻¹' t n ↔ x✝ ∈ t n
Module: Mathlib.Analysis.SpecialFunctions.MulExpNegMulSqIntegral

Goal state before:
pp: E : Type u_1
inst✝³ : TopologicalSpace E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
P : Measure E
inst✝ : IsFiniteMeasure P
g : E →ᵇ ℝ
⊢ Tendsto (fun ε ↦ ∫ (x : E), ε.mulExpNegMulSq (g x) ∂P) (𝓝[>] 0) (𝓝 (∫ (x : E), g x ∂P))

Tactic:
apply tendsto_of_seq_tendsto

Goal state after:
E : Type u_1
inst✝³ : TopologicalSpace E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
P : Measure E
inst✝ : IsFiniteMeasure P
g : E →ᵇ ℝ
⊢ ∀ (x : ℕ → ℝ),
    Tendsto x atTop (𝓝[>] 0) →
      Tendsto ((fun ε ↦ ∫ (x : E), ε.mulExpNegMulSq (g x) ∂P) ∘ x) atTop (𝓝 (∫ (x : E), g x ∂P))
Module: Mathlib.MeasureTheory.Constructions.HaarToSphere

Goal state before:
pp: n : ℕ
x : ↑(Ioi 0)
hr₀ : 0 ≤ ↑x
y : ℝ
hy : y ∈ Ioc 0 ↑x
⊢ 0 y ≤ y ^ n

Tactic:
exact pow_nonneg hy.1.le _

Goal state after:
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:
;

Goal state after:
L : PeriodPair
α β : ℚ
H : ↑α * L.ω₁ + ↑β * L.ω₂ ∈ L.lattice
m n : ℤ
e : ↑m * L.ω₁ + ↑n * L.ω₂ = ↑α * L.ω₁ + ↑β * L.ω₂
⊢ (↑m - ↑α) * L.ω₁ + (↑n - ↑β) * L.ω₂ = 0
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: r : ℝ
hr : 0 < r
s : ℂ
hs : ‖s‖ < r
h : 2 * r ≤ ‖s‖
⊢ False

Tactic:
;

Goal state after:
r : ℝ
hr : 0 < r
s : ℂ
hs : ‖s‖ < r
h : 2 * r ≤ ‖s‖
⊢ False
Module: Mathlib.Analysis.SpecialFunctions.Pow.NthRootLemmas

Goal state before:
pp: case e'_4
n a b : ℕ
hb : b ≠ 0
h : 0 ≤ (↑b + (↑a - ↑b)) ^ (n + 1) - (↑b ^ (n + 1) + ↑(n + 1) * ↑b ^ (n + 1 - 1) * (↑a - ↑b))
⊢ ↑a ^ n * ↑a + ↑n * ↑b * ↑b ^ n - (↑n + 1) * ↑a * ↑b ^ n =
    (↑b + (↑a - ↑b)) ^ (n + 1) - (↑b ^ (n + 1) + ↑(n + 1) * ↑b ^ (n + 1 - 1) * (↑a - ↑b))

Tactic:
;

Goal state after:
case e'_4
n a b : ℕ
hb : b ≠ 0
h : 0 ≤ (↑b + (↑a - ↑b)) ^ (n + 1) - (↑b ^ (n + 1) + ↑(n + 1) * ↑b ^ (n + 1 - 1) * (↑a - ↑b))
⊢ ↑a ^ n * ↑a + ↑n * ↑b * ↑b ^ n - (↑n + 1) * ↑a * ↑b ^ n =
    (↑b + (↑a - ↑b)) ^ (n + 1) - (↑b ^ (n + 1) + ↑(n + 1) * ↑b ^ (n + 1 - 1) * (↑a - ↑b))
Module: Mathlib.Analysis.SpecialFunctions.Pow.NthRootLemmas

Goal state before:
pp: case e'_4
n a b : ℕ
hb : b ≠ 0
h : 0 ≤ (↑b + (↑a - ↑b)) ^ (n + 1) - (↑b ^ (n + 1) + ↑(n + 1) * ↑b ^ (n + 1 - 1) * (↑a - ↑b))
⊢ ↑a ^ n * ↑a + ↑n * ↑b * ↑b ^ n - (↑n + 1) * ↑a * ↑b ^ n =
    (↑b + (↑a - ↑b)) ^ (n + 1) - (↑b ^ (n + 1) + (↑n + 1) * ↑b ^ n * (↑a - ↑b))

Tactic:
;

Goal state after:
case e'_4
n a b : ℕ
hb : b ≠ 0
h : 0 ≤ (↑b + (↑a - ↑b)) ^ (n + 1) - (↑b ^ (n + 1) + ↑(n + 1) * ↑b ^ (n + 1 - 1) * (↑a - ↑b))
⊢ ↑a ^ n * ↑a + ↑n * ↑b * ↑b ^ n - (↑n + 1) * ↑a * ↑b ^ n =
    (↑b + (↑a - ↑b)) ^ (n + 1) - (↑b ^ (n + 1) + (↑n + 1) * ↑b ^ n * (↑a - ↑b))
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 + (s - l)) * (l - (s - l))‖ = ‖s * (2 * l - s)‖

Tactic:
;

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.Elliptic.Weierstrass

Goal state before:
pp: L : PeriodPair
l₀ : ℂ
x✝¹ : ℝ
x✝ : x✝¹ > 0
⊢ 2 < 3

Tactic:
;

Goal state after:
L : PeriodPair
l₀ : ℂ
x✝¹ : ℝ
x✝ : x✝¹ > 0
⊢ 2 < 3
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: L : PeriodPair
l₀ : ℂ
r : ℝ
hr : r > 0
⊢ ∀ (b : ℝ),
    2 * r ≤ b →
      ∀ (x : ℂ),
        ‖x‖ < r →
          ∀ (l : ↥L.lattice), ‖↑l‖ = b → ‖if ↑l = l₀ then 0 else 1 / (x - ↑l) ^ 2 - 1 / ↑l ^ 2‖ ≤ 10 * r * ‖l‖ ^ (-3)

Tactic:
rintro _ h s hs l rfl

Goal state after:
L : PeriodPair
l₀ : ℂ
r : ℝ
hr : r > 0
s : ℂ
hs : ‖s‖ < r
l : ↥L.lattice
h : 2 * r ≤ ‖↑l‖
⊢ ‖if ↑l = l₀ then 0 else 1 / (s - ↑l) ^ 2 - 1 / ↑l ^ 2‖ ≤ 10 * r * ‖l‖ ^ (-3)