mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup

Goal state before:
pp: case e'_5
f : ℝ → ℝ
hf_conv : ConvexOn ℝ (Ioi 0) f
hf_feq : ∀ {y : ℝ}, 0 < y → f (y + 1) = f y + log y
m : ℕ
x : ℝ
hx : 0 < x
hy : ↑m < x - 1
hy' : x - 1 ≤ ↑m + 1
this✝¹ :
  ∀ᶠ (n : ℕ) in atTop,
    logGammaSeq (x - 1) n = logGammaSeq x (n - 1) + x * (log (↑(n - 1) + 1) - log ↑(n - 1)) - log (x - 1)
hm : Tendsto (fun n ↦ logGammaSeq x n + x * (log (↑n + 1) - log ↑n)) atTop (𝓝 (f (x - 1) - f 1 + log (x - 1)))
this✝ :
  ((fun x_1 ↦
        (fun n ↦ logGammaSeq x (n - 1) + x * (log (↑(n - 1) + 1) - log ↑(n - 1)) - log (x - 1)) x_1 +
          (fun b ↦ log (x - 1)) x_1) ∘
      fun a ↦ a + 1) =
    fun n ↦ logGammaSeq x n + x * (log (↑n + 1) - log ↑n)
this : f x = f (x - 1) + log (x - 1)
⊢ f (x - 1) + log (x - 1) - f 1 = f (x - 1) - f 1 + log (x - 1) - x * 0

Tactic:
]

Goal state after:
case e'_5
f : ℝ → ℝ
hf_conv : ConvexOn ℝ (Ioi 0) f
hf_feq : ∀ {y : ℝ}, 0 < y → f (y + 1) = f y + log y
m : ℕ
x : ℝ
hx : 0 < x
hy : ↑m < x - 1
hy' : x - 1 ≤ ↑m + 1
this✝¹ :
  ∀ᶠ (n : ℕ) in atTop,
    logGammaSeq (x - 1) n = logGammaSeq x (n - 1) + x * (log (↑(n - 1) + 1) - log ↑(n - 1)) - log (x - 1)
hm : Tendsto (fun n ↦ logGammaSeq x n + x * (log (↑n + 1) - log ↑n)) atTop (𝓝 (f (x - 1) - f 1 + log (x - 1)))
this✝ :
  ((fun x_1 ↦
        (fun n ↦ logGammaSeq x (n - 1) + x * (log (↑(n - 1) + 1) - log ↑(n - 1)) - log (x - 1)) x_1 +
          (fun b ↦ log (x - 1)) x_1) ∘
      fun a ↦ a + 1) =
    fun n ↦ logGammaSeq x n + x * (log (↑n + 1) - log ↑n)
this : f x = f (x - 1) + log (x - 1)
⊢ f (x - 1) + log (x - 1) - f 1 = f (x - 1) - f 1 + log (x - 1) - x * 0
Module: Mathlib.Analysis.MellinTransform

Goal state before:
pp: s : ℂ
hs : 0 < s.re
aux1 : -1 < (s - 1).re
aux2 : s ≠ 0
aux3 : MeasurableSet (Ioc 0 1)
⊢ IntervalIntegrable (fun a ↦ ↑a ^ (s - 1)) volume 0 1 ∧ ∫ (a : ℝ) in Ioc 0 1, ↑a ^ (s - 1) ∂volume = 1 / s

Tactic:
]

Goal state after:
s : ℂ
hs : 0 < s.re
aux1 : -1 < (s - 1).re
aux2 : s ≠ 0
aux3 : MeasurableSet (Ioc 0 1)
⊢ IntervalIntegrable (fun a ↦ ↑a ^ (s - 1)) volume 0 1 ∧ ∫ (a : ℝ) in Ioc 0 1, ↑a ^ (s - 1) ∂volume = 1 / s
Module: Mathlib.Analysis.MellinTransform

Goal state before:
pp: s : ℂ
hs : 0 < s.re
aux1 : -1 < (s - 1).re
aux2 : s ≠ 0
aux3 : MeasurableSet (Ioc 0 1)
⊢ 1 / s = 1 / s

Tactic:
]

Goal state after:
Module: Mathlib.Analysis.MellinTransform

Goal state before:
pp: a s : ℂ
hs : 0 < s.re + a.re
⊢ 0 < s.re + a.re

Tactic:
]

Goal state after:
a s : ℂ
hs : 0 < s.re + a.re
⊢ 0 < s.re + a.re
Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup

Goal state before:
pp: x : ℝ
hx : 0 < x
this : log (Γ x) = (log ∘ Γ) x - (log ∘ Γ) 1
⊢ Tendsto (logGammaSeq x) atTop (𝓝 ((log ∘ Γ) x - (log ∘ Γ) 1))

Tactic:
]

Goal state after:
x : ℝ
hx : 0 < x
this : log (Γ x) = (log ∘ Γ) x - (log ∘ Γ) 1
⊢ Tendsto (logGammaSeq x) atTop (𝓝 ((log ∘ Γ) x - (log ∘ Γ) 1))
Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup

Goal state before:
pp: x : ℝ
hx : 0 < x
this : log (Γ x) = (log ∘ Γ) x - (log ∘ Γ) 1
y : ℝ
hy : 0 < y
⊢ log (Γ y) + log y = log (Γ y) + log y

Tactic:
]

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

Goal state before:
pp: u v : ℂ
hu : 0 < u.re
hv : 0 < v.re
F : ℝ → ℂ := fun x ↦ ↑x ^ u * (1 - ↑x) ^ v
hu' : 0 < (u + 1).re
hv' : 0 < (v + 1).re
hc : ContinuousOn F (Icc 0 1)
hder : ∀ x ∈ Ioo 0 1, HasDerivAt F (u * (↑x ^ (u - 1) * (1 - ↑x) ^ v) - v * (↑x ^ u * (1 - ↑x) ^ (v - 1))) x
h_int : IntervalIntegrable (fun x ↦ u * (↑x ^ (u - 1) * (1 - ↑x) ^ v) - v * (↑x ^ u * (1 - ↑x) ^ (v - 1))) volume 0 1
int_ev : (u * ∫ (x : ℝ) in 0..1, ↑x ^ (u - 1) * (1 - ↑x) ^ v) - v * ∫ (x : ℝ) in 0..1, ↑x ^ u * (1 - ↑x) ^ (v - 1) = 0
hF0 : F 0 = 0
hF1 : F 1 = 0
⊢ (u * ∫ (x : ℝ) in 0..1, ↑x ^ (u - 1) * (1 - ↑x) ^ (v + 1 - 1)) -
      v * ∫ (x : ℝ) in 0..1, ↑x ^ (u + 1 - 1) * (1 - ↑x) ^ (v - 1) =
    0

Tactic:
]

Goal state after:
u v : ℂ
hu : 0 < u.re
hv : 0 < v.re
F : ℝ → ℂ := fun x ↦ ↑x ^ u * (1 - ↑x) ^ v
hu' : 0 < (u + 1).re
hv' : 0 < (v + 1).re
hc : ContinuousOn F (Icc 0 1)
hder : ∀ x ∈ Ioo 0 1, HasDerivAt F (u * (↑x ^ (u - 1) * (1 - ↑x) ^ v) - v * (↑x ^ u * (1 - ↑x) ^ (v - 1))) x
h_int : IntervalIntegrable (fun x ↦ u * (↑x ^ (u - 1) * (1 - ↑x) ^ v) - v * (↑x ^ u * (1 - ↑x) ^ (v - 1))) volume 0 1
int_ev : (u * ∫ (x : ℝ) in 0..1, ↑x ^ (u - 1) * (1 - ↑x) ^ v) - v * ∫ (x : ℝ) in 0..1, ↑x ^ u * (1 - ↑x) ^ (v - 1) = 0
hF0 : F 0 = 0
hF1 : F 1 = 0
⊢ (u * ∫ (x : ℝ) in 0..1, ↑x ^ (u - 1) * (1 - ↑x) ^ (v + 1 - 1)) -
      v * ∫ (x : ℝ) in 0..1, ↑x ^ (u + 1 - 1) * (1 - ↑x) ^ (v - 1) =
    0
Module: Mathlib.Analysis.Meromorphic.LogDeriv

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
𝕜' : Type u_2
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
f g : 𝕜 → 𝕜'
U : Set 𝕜
hf : MeromorphicOn f U
hg : MeromorphicOn g U
h'f : ∀ x ∈ U, meromorphicOrderAt f x ≠ ⊤
h'g : ∀ x ∈ U, meromorphicOrderAt g x ≠ ⊤
y : 𝕜
h₁y : AnalyticAt 𝕜 f y
h₂y : AnalyticAt 𝕜 g y
h₃y : f y ≠ 0
h₄y : g y ≠ 0
⊢ logDeriv (fun i ↦ f i * g i) y = logDeriv f y + logDeriv g y

Tactic:
]

Goal state after:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
𝕜' : Type u_2
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
f g : 𝕜 → 𝕜'
U : Set 𝕜
hf : MeromorphicOn f U
hg : MeromorphicOn g U
h'f : ∀ x ∈ U, meromorphicOrderAt f x ≠ ⊤
h'g : ∀ x ∈ U, meromorphicOrderAt g x ≠ ⊤
y : 𝕜
h₁y : AnalyticAt 𝕜 f y
h₂y : AnalyticAt 𝕜 g y
h₃y : f y ≠ 0
h₄y : g y ≠ 0
⊢ logDeriv (fun i ↦ f i * g i) y = logDeriv f y + logDeriv g y
Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup

Goal state before:
pp: case refine_2
f : ℝ → ℝ
hf_conv : ConvexOn ℝ (Ioi 0) (log ∘ f)
hf_feq : ∀ {y : ℝ}, 0 < y → f (y + 1) = y * f y
hf_pos : ∀ {y : ℝ}, 0 < y → 0 < f y
hf_one : f 1 = 1
x : ℝ
hx : x ∈ Ioi 0
e1 : Tendsto (BohrMollerup.logGammaSeq x) atTop (𝓝 ((log ∘ f) x))
⊢ (log ∘ f) x = (log ∘ Γ) x

Tactic:
]

Goal state after:
case refine_2
f : ℝ → ℝ
hf_conv : ConvexOn ℝ (Ioi 0) (log ∘ f)
hf_feq : ∀ {y : ℝ}, 0 < y → f (y + 1) = y * f y
hf_pos : ∀ {y : ℝ}, 0 < y → 0 < f y
hf_one : f 1 = 1
x : ℝ
hx : x ∈ Ioi 0
e1 : Tendsto (BohrMollerup.logGammaSeq x) atTop (𝓝 ((log ∘ f) x))
⊢ (log ∘ f) x = (log ∘ Γ) x
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd

Goal state before:
pp: case e'_3.e_a.e_f
z : ℂ
this✝ : 𝓝 (Complex.sin (↑π * z)) = 𝓝 (Complex.sin (↑π * z) * 1)
A :
  Tendsto
    (fun n ↦
      (↑π * z * ∏ j ∈ Finset.range n, (1 - z ^ 2 / (↑j + 1) ^ 2)) *
        ((∫ (x : ℝ) in 0..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (2 * n)) /
          ↑(∫ (x : ℝ) in 0..π / 2, cos x ^ (2 * n))))
    atTop (𝓝 (Complex.sin (↑π * z) * 1))
this : ContinuousOn (fun x ↦ Complex.cos (2 * z * ↑x)) (Icc 0 (π / 2))
n : ℕ
x : ℝ
⊢ ↑(cos x) ^ n * Complex.cos (2 * z * ↑x) = ↑(cos x) ^ n * Complex.cos (2 * z * ↑x)

Tactic:
]

Goal state after:
Module: Mathlib.Analysis.Meromorphic.LogDeriv

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
𝕜' : Type u_2
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
U : Set 𝕜
ι : Type u_3
s : Finset ι
F : ι → 𝕜 → 𝕜'
h : ∀ i ∈ s, MeromorphicOn (F i) U
h' : ∀ i ∈ s, ∀ x ∈ U, meromorphicOrderAt (F i) x ≠ ⊤
hA : ∀ᶠ (y : 𝕜) in codiscreteWithin U, ∀ i ∈ s, AnalyticAt 𝕜 (F i) y
hN : ∀ᶠ (y : 𝕜) in codiscreteWithin U, ∀ i ∈ s, F i y ≠ 0
y : 𝕜
h₁y : ∀ i ∈ s, AnalyticAt 𝕜 (F i) y
h₂y : ∀ i ∈ s, F i y ≠ 0
⊢ logDeriv (fun a ↦ ∏ c ∈ s, F c a) y = ∑ c ∈ s, logDeriv (F c) y

Tactic:
]

Goal state after:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
𝕜' : Type u_2
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
U : Set 𝕜
ι : Type u_3
s : Finset ι
F : ι → 𝕜 → 𝕜'
h : ∀ i ∈ s, MeromorphicOn (F i) U
h' : ∀ i ∈ s, ∀ x ∈ U, meromorphicOrderAt (F i) x ≠ ⊤
hA : ∀ᶠ (y : 𝕜) in codiscreteWithin U, ∀ i ∈ s, AnalyticAt 𝕜 (F i) y
hN : ∀ᶠ (y : 𝕜) in codiscreteWithin U, ∀ i ∈ s, F i y ≠ 0
y : 𝕜
h₁y : ∀ i ∈ s, AnalyticAt 𝕜 (F i) y
h₂y : ∀ i ∈ s, F i y ≠ 0
⊢ logDeriv (fun a ↦ ∏ c ∈ s, F c a) y = ∑ c ∈ s, logDeriv (F c) y
Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup

Goal state before:
pp: case refine_1
f : ℝ → ℝ
hf_conv : ConvexOn ℝ (Ioi 0) (log ∘ f)
hf_feq : ∀ {y : ℝ}, 0 < y → f (y + 1) = y * f y
hf_pos : ∀ {y : ℝ}, 0 < y → 0 < f y
hf_one : f 1 = 1
x : ℝ
hx : x ∈ Ioi 0
y : ℝ
hy : 0 < y
⊢ log y + log (f y) = log (f y) + log y

Tactic:
]

Goal state after:
case refine_1
f : ℝ → ℝ
hf_conv : ConvexOn ℝ (Ioi 0) (log ∘ f)
hf_feq : ∀ {y : ℝ}, 0 < y → f (y + 1) = y * f y
hf_pos : ∀ {y : ℝ}, 0 < y → 0 < f y
hf_one : f 1 = 1
x : ℝ
hx : x ∈ Ioi 0
y : ℝ
hy : 0 < y
⊢ log y + log (f y) = log (f y) + log y
Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup

Goal state before:
pp: case refine_1
A : 0 < 3 / 2
y : ℝ
hy : 0 < y
⊢ log (Γ y) + log y = log (Γ y) + log y

Tactic:
]

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

Goal state before:
pp: case refine_2
A : 0 < 3 / 2
this : Γ (3 / 2) ≤ rexp (1 / 2 * log 2 - log (3 / 2))
⊢ Γ (3 / 2) < 1

Tactic:
]

Goal state after:
case refine_2
A : 0 < 3 / 2
this : Γ (3 / 2) ≤ rexp (1 / 2 * log 2 - log (3 / 2))
⊢ Γ (3 / 2) < 1
Module: Mathlib.Analysis.Meromorphic.LogDeriv

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
𝕜' : Type u_2
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
U : Set 𝕜
ι : Type u_3
F : ι → 𝕜 → 𝕜'
hF : (mulSupport F).Finite
h : ∀ (i : ι), MeromorphicOn (F i) U
h' : ∀ (i : ι), ∀ x ∈ U, meromorphicOrderAt (F i) x ≠ ⊤
hsub : (support fun i ↦ logDeriv (F i)) ⊆ ↑hF.toFinset
⊢ logDeriv (∏ i ∈ hF.toFinset, F i) =ᶠ[codiscreteWithin U] ∑ i ∈ hF.toFinset, logDeriv (F i)

Tactic:
]

Goal state after:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
𝕜' : Type u_2
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
U : Set 𝕜
ι : Type u_3
F : ι → 𝕜 → 𝕜'
hF : (mulSupport F).Finite
h : ∀ (i : ι), MeromorphicOn (F i) U
h' : ∀ (i : ι), ∀ x ∈ U, meromorphicOrderAt (F i) x ≠ ⊤
hsub : (support fun i ↦ logDeriv (F i)) ⊆ ↑hF.toFinset
⊢ logDeriv (∏ i ∈ hF.toFinset, F i) =ᶠ[codiscreteWithin U] ∑ i ∈ hF.toFinset, logDeriv (F i)
Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup

Goal state before:
pp: case refine_2
A : 0 < 3 / 2
this : Γ (3 / 2) ≤ rexp (1 / 2 * log 2 - log (3 / 2))
⊢ (log 2 * 1 - 2 * log (3 / 2)) / 2 < 0

Tactic:
]

Goal state after:
case refine_2
A : 0 < 3 / 2
this : Γ (3 / 2) ≤ rexp (1 / 2 * log 2 - log (3 / 2))
⊢ (log 2 * 1 - 2 * log (3 / 2)) / 2 < 0
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd

Goal state before:
pp: case e'_5
z : ℂ
this✝ : 𝓝 (Complex.sin (↑π * z)) = 𝓝 (Complex.sin (↑π * z) * 1)
A :
  Tendsto
    (fun n ↦
      (↑π * z * ∏ j ∈ Finset.range n, (1 - z ^ 2 / (↑j + 1) ^ 2)) *
        ((∫ (x : ℝ) in 0..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (2 * n)) /
          ↑(∫ (x : ℝ) in 0..π / 2, cos x ^ (2 * n))))
    atTop (𝓝 (Complex.sin (↑π * z) * 1))
this : ContinuousOn (fun x ↦ Complex.cos (2 * z * ↑x)) (Icc 0 (π / 2))
⊢ 𝓝 1 = 𝓝 1

Tactic:
]

Goal state after:
Module: Mathlib.Analysis.Meromorphic.LogDeriv

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
𝕜' : Type u_2
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
f : 𝕜 → 𝕜'
U : Set 𝕜
hf : MeromorphicOn f U
n : ℤ
y : 𝕜
hy : AnalyticAt 𝕜 f y
⊢ logDeriv (fun x ↦ f x ^ n) y = ↑n * logDeriv f y

Tactic:
]

Goal state after:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
𝕜' : Type u_2
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
f : 𝕜 → 𝕜'
U : Set 𝕜
hf : MeromorphicOn f U
n : ℤ
y : 𝕜
hy : AnalyticAt 𝕜 f y
⊢ logDeriv (fun x ↦ f x ^ n) y = ↑n * logDeriv f y
Module: Mathlib.Analysis.Meromorphic.LogDeriv

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
𝕜' : Type u_2
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
f : 𝕜 → 𝕜'
U : Set 𝕜
hf : MeromorphicOn f U
n : ℤ
y : 𝕜
hy : AnalyticAt 𝕜 f y
⊢ logDeriv (f ^ n) y = (n • logDeriv f) y

Tactic:
rw [Pi.smul_apply, zsmul_eq_mul, show f ^ n = (f · ^ n) from rfl]

Goal state after:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
𝕜' : Type u_2
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
f : 𝕜 → 𝕜'
U : Set 𝕜
hf : MeromorphicOn f U
n : ℤ
y : 𝕜
hy : AnalyticAt 𝕜 f y
⊢ logDeriv (fun x ↦ f x ^ n) y = ↑n * logDeriv f y
Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup

Goal state before:
pp: case refine_2
A : 0 < 3 / 2
this : Γ (3 / 2) ≤ rexp (1 / 2 * log 2 - log (3 / 2))
⊢ 2 < (3 / 2) ^ 2

pp: case refine_2
A : 0 < 3 / 2
this : Γ (3 / 2) ≤ rexp (1 / 2 * log 2 - log (3 / 2))
⊢ 0 < (3 / 2) ^ 2

Tactic:
]

Goal state after:
case refine_2
A : 0 < 3 / 2
this : Γ (3 / 2) ≤ rexp (1 / 2 * log 2 - log (3 / 2))
⊢ 2 < (3 / 2) ^ 2

case refine_2
A : 0 < 3 / 2
this : Γ (3 / 2) ≤ rexp (1 / 2 * log 2 - log (3 / 2))
⊢ 0 < (3 / 2) ^ 2
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd

Goal state before:
pp: case e'_3
x : ℝ
n : ℕ
⊢ π * x * ∏ j ∈ Finset.range n, (1 - x ^ 2 / (↑j + 1) ^ 2) =
    π * x * (∏ j ∈ Finset.range n, (1 - ↑x ^ 2 / (↑j + 1) ^ 2)).re

Tactic:
]

Goal state after:
case e'_3
x : ℝ
n : ℕ
⊢ π * x * ∏ j ∈ Finset.range n, (1 - x ^ 2 / (↑j + 1) ^ 2) =
    π * x * (∏ j ∈ Finset.range n, (1 - ↑x ^ 2 / (↑j + 1) ^ 2)).re
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd

Goal state before:
pp: x : ℝ
n : ℕ
this : ∏ j ∈ Finset.range n, (1 - ↑x ^ 2 / (↑j + 1) ^ 2) = ↑(∏ j ∈ Finset.range n, (1 - x ^ 2 / (↑j + 1) ^ 2))
⊢ π * x * ∏ j ∈ Finset.range n, (1 - x ^ 2 / (↑j + 1) ^ 2) = π * x * ∏ j ∈ Finset.range n, (1 - x ^ 2 / (↑j + 1) ^ 2)

Tactic:
]

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

Goal state before:
pp: case zero
u : ℂ
hu : 0 < u.re
⊢ 1 / u = 1 / ∏ j ∈ Finset.range (0 + 1), (u + ↑j)

Tactic:
]

Goal state after:
case zero
u : ℂ
hu : 0 < u.re
⊢ 1 / u = 1 / ∏ j ∈ Finset.range (0 + 1), (u + ↑j)
Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup

Goal state before:
pp: case e'_6
⊢ Ici 2 ⊆ Ioi 0

Tactic:
]

Goal state after:
case e'_6
⊢ Ici 2 ⊆ Ioi 0
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd

Goal state before:
pp: case e'_5
x : ℝ
⊢ 𝓝 (sin (π * x)) = 𝓝 (sin (π * x))

Tactic:
]

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

Goal state before:
pp: case succ.refine_1
n : ℕ
IH : ∀ {u : ℂ}, 0 < u.re → u.betaIntegral (↑n + 1) = ↑n ! / ∏ j ∈ Finset.range (n + 1), (u + ↑j)
u : ℂ
hu : 0 < u.re
⊢ 0 < ↑n.succ

Tactic:
]

Goal state after:
case succ.refine_1
n : ℕ
IH : ∀ {u : ℂ}, 0 < u.re → u.betaIntegral (↑n + 1) = ↑n ! / ∏ j ∈ Finset.range (n + 1), (u + ↑j)
u : ℂ
hu : 0 < u.re
⊢ 0 < ↑n.succ
Module: Mathlib.Analysis.Meromorphic.LogDeriv

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
𝕜' : Type u_2
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
U : Set 𝕜
ι : Type u_3
F : ι → 𝕜 → 𝕜'
d : ι → ℤ
hd : (support d).Finite
h : ∀ (i : ι), MeromorphicOn (F i) U
h' : ∀ (i : ι), ∀ x ∈ U, meromorphicOrderAt (F i) x ≠ ⊤
hA : ∀ᶠ (y : 𝕜) in codiscreteWithin U, ∀ i ∈ hd.toFinset, AnalyticAt 𝕜 (F i) y
hN : ∀ᶠ (y : 𝕜) in codiscreteWithin U, ∀ i ∈ hd.toFinset, F i y ≠ 0
y : 𝕜
h₁y : ∀ i ∈ hd.toFinset, AnalyticAt 𝕜 (F i) y
h₂y : ∀ i ∈ hd.toFinset, F i y ≠ 0
h₀ : ∏ᶠ (i : ι), F i ^ d i = ∏ i ∈ hd.toFinset, F i ^ d i
hsub : (support fun i ↦ d i • logDeriv (F i) y) ⊆ ↑hd.toFinset
⊢ logDeriv (fun a ↦ ∏ c ∈ hd.toFinset, (F c ^ d c) a) y = logDeriv (fun z ↦ ∏ i ∈ hd.toFinset, (F i ^ d i) z) y

Tactic:
]

Goal state after:
Module: Mathlib.Topology.Algebra.AsymptoticCone

Goal state before:
pp: k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁵ : Field k
inst✝⁴ : LinearOrder k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AddTorsor V P
inst✝ : TopologicalSpace V
u v : V
p : P
⊢ u +ᵥ asymptoticNhds k V v +ᵥ pure p = asymptoticNhds k P v

Tactic:
]

Goal state after:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁵ : Field k
inst✝⁴ : LinearOrder k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AddTorsor V P
inst✝ : TopologicalSpace V
u v : V
p : P
⊢ u +ᵥ asymptoticNhds k V v +ᵥ pure p = asymptoticNhds k P v
Module: Mathlib.Topology.Algebra.AsymptoticCone

Goal state before:
pp: k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁵ : Field k
inst✝⁴ : LinearOrder k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AddTorsor V P
inst✝ : TopologicalSpace V
α : Type u_4
l : Filter α
f : α → V
v : V
p : P
hf : Tendsto f l (asymptoticNhds k V v)
⊢ Tendsto (fun x ↦ f x +ᵥ p) l (map (fun x ↦ x +ᵥ ?m.44) (asymptoticNhds k V v))

pp: k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁵ : Field k
inst✝⁴ : LinearOrder k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AddTorsor V P
inst✝ : TopologicalSpace V
α : Type u_4
l : Filter α
f : α → V
v : V
p : P
hf : Tendsto f l (asymptoticNhds k V v)
⊢ P

Tactic:
]

Goal state after:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁵ : Field k
inst✝⁴ : LinearOrder k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AddTorsor V P
inst✝ : TopologicalSpace V
α : Type u_4
l : Filter α
f : α → V
v : V
p : P
hf : Tendsto f l (asymptoticNhds k V v)
⊢ Tendsto (fun x ↦ f x +ᵥ p) l (map (fun x ↦ x +ᵥ ?m.44) (asymptoticNhds k V v))

k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁵ : Field k
inst✝⁴ : LinearOrder k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AddTorsor V P
inst✝ : TopologicalSpace V
α : Type u_4
l : Filter α
f : α → V
v : V
p : P
hf : Tendsto f l (asymptoticNhds k V v)
⊢ P
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta

Goal state before:
pp: case succ.refine_2
n : ℕ
IH : ∀ {u : ℂ}, 0 < u.re → u.betaIntegral (↑n + 1) = ↑n ! / ∏ j ∈ Finset.range (n + 1), (u + ↑j)
u : ℂ
hu : 0 < u.re
this : u.betaIntegral (↑n.succ + 1) = ↑n.succ * (u + 1).betaIntegral ↑n.succ / u
⊢ u.betaIntegral (↑(n + 1) + 1) = ↑(n + 1)! / ∏ j ∈ Finset.range (n + 1 + 1), (u + ↑j)

pp: case succ.refine_2
n : ℕ
IH : ∀ {u : ℂ}, 0 < u.re → u.betaIntegral (↑n + 1) = ↑n ! / ∏ j ∈ Finset.range (n + 1), (u + ↑j)
u : ℂ
hu : 0 < u.re
this : u.betaIntegral (↑n.succ + 1) * u = ↑n.succ * (u + 1).betaIntegral ↑n.succ
⊢ u ≠ 0

Tactic:
]

Goal state after:
case succ.refine_2
n : ℕ
IH : ∀ {u : ℂ}, 0 < u.re → u.betaIntegral (↑n + 1) = ↑n ! / ∏ j ∈ Finset.range (n + 1), (u + ↑j)
u : ℂ
hu : 0 < u.re
this : u.betaIntegral (↑n.succ + 1) = ↑n.succ * (u + 1).betaIntegral ↑n.succ / u
⊢ u.betaIntegral (↑(n + 1) + 1) = ↑(n + 1)! / ∏ j ∈ Finset.range (n + 1 + 1), (u + ↑j)

case succ.refine_2
n : ℕ
IH : ∀ {u : ℂ}, 0 < u.re → u.betaIntegral (↑n + 1) = ↑n ! / ∏ j ∈ Finset.range (n + 1), (u + ↑j)
u : ℂ
hu : 0 < u.re
this : u.betaIntegral (↑n.succ + 1) * u = ↑n.succ * (u + 1).betaIntegral ↑n.succ
⊢ u ≠ 0
Module: Mathlib.Topology.Algebra.AsymptoticCone

Goal state before:
pp: k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁵ : Field k
inst✝⁴ : LinearOrder k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AddTorsor V P
inst✝ : TopologicalSpace V
α : Type u_4
l : Filter α
f : α → P
v u : V
hf : Tendsto f l (asymptoticNhds k P v)
⊢ Tendsto (fun x ↦ u +ᵥ f x) l (map (fun b ↦ u +ᵥ b) (asymptoticNhds k P v))

Tactic:
]

Goal state after:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁵ : Field k
inst✝⁴ : LinearOrder k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AddTorsor V P
inst✝ : TopologicalSpace V
α : Type u_4
l : Filter α
f : α → P
v u : V
hf : Tendsto f l (asymptoticNhds k P v)
⊢ Tendsto (fun x ↦ u +ᵥ f x) l (map (fun b ↦ u +ᵥ b) (asymptoticNhds k P v))
Module: Mathlib.Topology.Algebra.AsymptoticCone

Goal state before:
pp: k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁵ : Field k
inst✝⁴ : LinearOrder k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AddTorsor V P
inst✝ : TopologicalSpace V
α : Type u_4
l : Filter α
f : α → P
v u : V
hf : Tendsto f l (asymptoticNhds k P v)
⊢ Tendsto (fun x ↦ u +ᵥ f x) l (asymptoticNhds k P v)

Tactic:
rw [← vadd_asymptoticNhds u, ← Filter.map_vadd]
  exact tendsto_map.comp hf

Goal state after:
Module: Mathlib.Analysis.Meromorphic.LogDeriv

Goal state before:
pp: case a
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
𝕜' : Type u_2
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
U : Set 𝕜
ι : Type u_3
F : ι → 𝕜 → 𝕜'
d : ι → ℤ
hd : (support d).Finite
h : ∀ (i : ι), MeromorphicOn (F i) U
h' : ∀ (i : ι), ∀ x ∈ U, meromorphicOrderAt (F i) x ≠ ⊤
hA : ∀ᶠ (y : 𝕜) in codiscreteWithin U, ∀ i ∈ hd.toFinset, AnalyticAt 𝕜 (F i) y
hN : ∀ᶠ (y : 𝕜) in codiscreteWithin U, ∀ i ∈ hd.toFinset, F i y ≠ 0
y : 𝕜
h₁y : ∀ i ∈ hd.toFinset, AnalyticAt 𝕜 (F i) y
h₂y : ∀ i ∈ hd.toFinset, F i y ≠ 0
h₀ : ∏ᶠ (i : ι), F i ^ d i = ∏ i ∈ hd.toFinset, F i ^ d i
hsub : (support fun i ↦ d i • logDeriv (F i) y) ⊆ ↑hd.toFinset
i : ι
hi : i ∈ hd.toFinset
⊢ logDeriv (fun i_1 ↦ F i i_1 ^ d i) y = ↑(d i) * logDeriv (F i) y

Tactic:
]

Goal state after:
case a
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
𝕜' : Type u_2
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
U : Set 𝕜
ι : Type u_3
F : ι → 𝕜 → 𝕜'
d : ι → ℤ
hd : (support d).Finite
h : ∀ (i : ι), MeromorphicOn (F i) U
h' : ∀ (i : ι), ∀ x ∈ U, meromorphicOrderAt (F i) x ≠ ⊤
hA : ∀ᶠ (y : 𝕜) in codiscreteWithin U, ∀ i ∈ hd.toFinset, AnalyticAt 𝕜 (F i) y
hN : ∀ᶠ (y : 𝕜) in codiscreteWithin U, ∀ i ∈ hd.toFinset, F i y ≠ 0
y : 𝕜
h₁y : ∀ i ∈ hd.toFinset, AnalyticAt 𝕜 (F i) y
h₂y : ∀ i ∈ hd.toFinset, F i y ≠ 0
h₀ : ∏ᶠ (i : ι), F i ^ d i = ∏ i ∈ hd.toFinset, F i ^ d i
hsub : (support fun i ↦ d i • logDeriv (F i) y) ⊆ ↑hd.toFinset
i : ι
hi : i ∈ hd.toFinset
⊢ logDeriv (fun i_1 ↦ F i i_1 ^ d i) y = ↑(d i) * logDeriv (F i) y
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta

Goal state before:
pp: case succ.refine_2
n : ℕ
IH : ∀ {u : ℂ}, 0 < u.re → u.betaIntegral (↑n + 1) = ↑n ! / ∏ j ∈ Finset.range (n + 1), (u + ↑j)
u : ℂ
this : u.betaIntegral (↑n.succ + 1) * u = ↑n.succ * (u + 1).betaIntegral ↑n.succ
hu : u = 0
⊢ 0 ≤ 0

Tactic:
]

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

Goal state before:
pp: s : ℝ
hs : s ≠ 0
⊢ Γ (s / 2 + 1 / 2) * (s / 2 * Γ (s / 2)) * (2 ^ (s - 1) * 2) / √π =
    s * (Γ (s / 2) * Γ (s / 2 + 1 / 2) * 2 ^ (s - 1) / √π)

Tactic:
]

Goal state after:
s : ℝ
hs : s ≠ 0
⊢ Γ (s / 2 + 1 / 2) * (s / 2 * Γ (s / 2)) * (2 ^ (s - 1) * 2) / √π =
    s * (Γ (s / 2) * Γ (s / 2 + 1 / 2) * 2 ^ (s - 1) / √π)
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta

Goal state before:
pp: case succ.refine_2
n : ℕ
IH : ∀ {u : ℂ}, 0 < u.re → u.betaIntegral (↑n + 1) = ↑n ! / ∏ j ∈ Finset.range (n + 1), (u + ↑j)
u : ℂ
hu : 0 < u.re
this : u.betaIntegral (↑n.succ + 1) = ↑n.succ * (u + 1).betaIntegral ↑n.succ / u
⊢ (↑n + 1) * (↑n ! / ∏ j ∈ Finset.range (n + 1), (u + 1 + ↑j)) / u =
    ↑(n + 1)! / ((∏ k ∈ Finset.range (n + 1), (u + ↑(k + 1))) * (u + ↑0))

pp: case succ.refine_2
n : ℕ
IH : ∀ {u : ℂ}, 0 < u.re → u.betaIntegral (↑n + 1) = ↑n ! / ∏ j ∈ Finset.range (n + 1), (u + ↑j)
u : ℂ
hu : 0 < u.re
this : u.betaIntegral (↑n.succ + 1) = ↑n.succ * (u + 1).betaIntegral ↑n.succ / u
⊢ 0 < (u + 1).re

Tactic:
]

Goal state after:
case succ.refine_2
n : ℕ
IH : ∀ {u : ℂ}, 0 < u.re → u.betaIntegral (↑n + 1) = ↑n ! / ∏ j ∈ Finset.range (n + 1), (u + ↑j)
u : ℂ
hu : 0 < u.re
this : u.betaIntegral (↑n.succ + 1) = ↑n.succ * (u + 1).betaIntegral ↑n.succ / u
⊢ (↑n + 1) * (↑n ! / ∏ j ∈ Finset.range (n + 1), (u + 1 + ↑j)) / u =
    ↑(n + 1)! / ((∏ k ∈ Finset.range (n + 1), (u + ↑(k + 1))) * (u + ↑0))

case succ.refine_2
n : ℕ
IH : ∀ {u : ℂ}, 0 < u.re → u.betaIntegral (↑n + 1) = ↑n ! / ∏ j ∈ Finset.range (n + 1), (u + ↑j)
u : ℂ
hu : 0 < u.re
this : u.betaIntegral (↑n.succ + 1) = ↑n.succ * (u + 1).betaIntegral ↑n.succ / u
⊢ 0 < (u + 1).re