mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd

Goal state before:
pp: case e'_3
z : ℂ
n : ℕ
hn : 2 ≤ n
hz : z ≠ 0
der1 :
  ∀ x ∈ uIcc 0 (π / 2),
    HasDerivAt (fun y ↦ ↑(sin y) * ↑(cos y) ^ (n - 1)) (↑(cos x) ^ n - (↑n - 1) * ↑(sin x) ^ 2 * ↑(cos x) ^ (n - 2)) x
⊢ (↑n / (2 * z) * ∫ (x : ℝ) in 0..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ n) -
      (↑n - 1) / (2 * z) * ∫ (x : ℝ) in 0..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (n - 2) =
    ↑(sin (π / 2)) * 0 * (-Complex.cos (2 * z * ↑(π / 2)) / (2 * z)) -
        0 * ↑(cos 0) ^ (n - 1) * (-Complex.cos (2 * z * 0) / (2 * z)) -
      ∫ (x : ℝ) in 0..π / 2,
        (↑(cos x) ^ n - (↑n - 1) * ↑(sin x) ^ 2 * ↑(cos x) ^ (n - 2)) * (-Complex.cos (2 * z * ↑x) / (2 * z))

pp: case e'_3
z : ℂ
n : ℕ
hn : 2 ≤ n
hz : z ≠ 0
der1 :
  ∀ x ∈ uIcc 0 (π / 2),
    HasDerivAt (fun y ↦ ↑(sin y) * ↑(cos y) ^ (n - 1)) (↑(cos x) ^ n - (↑n - 1) * ↑(sin x) ^ 2 * ↑(cos x) ^ (n - 2)) x
⊢ n - 1 ≠ 0

Tactic:
zero_mul,

Goal state after:
case e'_3
z : ℂ
n : ℕ
hn : 2 ≤ n
hz : z ≠ 0
der1 :
  ∀ x ∈ uIcc 0 (π / 2),
    HasDerivAt (fun y ↦ ↑(sin y) * ↑(cos y) ^ (n - 1)) (↑(cos x) ^ n - (↑n - 1) * ↑(sin x) ^ 2 * ↑(cos x) ^ (n - 2)) x
⊢ (↑n / (2 * z) * ∫ (x : ℝ) in 0..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ n) -
      (↑n - 1) / (2 * z) * ∫ (x : ℝ) in 0..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (n - 2) =
    ↑(sin (π / 2)) * 0 * (-Complex.cos (2 * z * ↑(π / 2)) / (2 * z)) - 0 * (-Complex.cos (2 * z * 0) / (2 * z)) -
      ∫ (x : ℝ) in 0..π / 2,
        (↑(cos x) ^ n - (↑n - 1) * ↑(sin x) ^ 2 * ↑(cos x) ^ (n - 2)) * (-Complex.cos (2 * z * ↑x) / (2 * z))

case e'_3
z : ℂ
n : ℕ
hn : 2 ≤ n
hz : z ≠ 0
der1 :
  ∀ x ∈ uIcc 0 (π / 2),
    HasDerivAt (fun y ↦ ↑(sin y) * ↑(cos y) ^ (n - 1)) (↑(cos x) ^ n - (↑n - 1) * ↑(sin x) ^ 2 * ↑(cos x) ^ (n - 2)) x
⊢ n - 1 ≠ 0
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd

Goal state before:
pp: case e'_3
z : ℂ
n : ℕ
hn : 2 ≤ n
hz : z ≠ 0
der1 :
  ∀ x ∈ uIcc 0 (π / 2),
    HasDerivAt (fun y ↦ ↑(sin y) * ↑(cos y) ^ (n - 1)) (↑(cos x) ^ n - (↑n - 1) * ↑(sin x) ^ 2 * ↑(cos x) ^ (n - 2)) x
⊢ (↑n / (2 * z) * ∫ (x : ℝ) in 0..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ n) -
      (↑n - 1) / (2 * z) * ∫ (x : ℝ) in 0..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (n - 2) =
    0 * (-Complex.cos (2 * z * ↑(π / 2)) / (2 * z)) - 0 * (-Complex.cos (2 * z * 0) / (2 * z)) -
      ∫ (x : ℝ) in 0..π / 2,
        (↑(cos x) ^ n - (↑n - 1) * ↑(sin x) ^ 2 * ↑(cos x) ^ (n - 2)) * (-Complex.cos (2 * z * ↑x) / (2 * z))

pp: case e'_3
z : ℂ
n : ℕ
hn : 2 ≤ n
hz : z ≠ 0
der1 :
  ∀ x ∈ uIcc 0 (π / 2),
    HasDerivAt (fun y ↦ ↑(sin y) * ↑(cos y) ^ (n - 1)) (↑(cos x) ^ n - (↑n - 1) * ↑(sin x) ^ 2 * ↑(cos x) ^ (n - 2)) x
⊢ n - 1 ≠ 0

Tactic:
zero_mul,

Goal state after:
case e'_3
z : ℂ
n : ℕ
hn : 2 ≤ n
hz : z ≠ 0
der1 :
  ∀ x ∈ uIcc 0 (π / 2),
    HasDerivAt (fun y ↦ ↑(sin y) * ↑(cos y) ^ (n - 1)) (↑(cos x) ^ n - (↑n - 1) * ↑(sin x) ^ 2 * ↑(cos x) ^ (n - 2)) x
⊢ (↑n / (2 * z) * ∫ (x : ℝ) in 0..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ n) -
      (↑n - 1) / (2 * z) * ∫ (x : ℝ) in 0..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (n - 2) =
    0 - 0 * (-Complex.cos (2 * z * 0) / (2 * z)) -
      ∫ (x : ℝ) in 0..π / 2,
        (↑(cos x) ^ n - (↑n - 1) * ↑(sin x) ^ 2 * ↑(cos x) ^ (n - 2)) * (-Complex.cos (2 * z * ↑x) / (2 * z))

case e'_3
z : ℂ
n : ℕ
hn : 2 ≤ n
hz : z ≠ 0
der1 :
  ∀ x ∈ uIcc 0 (π / 2),
    HasDerivAt (fun y ↦ ↑(sin y) * ↑(cos y) ^ (n - 1)) (↑(cos x) ^ n - (↑n - 1) * ↑(sin x) ^ 2 * ↑(cos x) ^ (n - 2)) x
⊢ n - 1 ≠ 0
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd

Goal state before:
pp: case e'_3
z : ℂ
n : ℕ
hn : 2 ≤ n
hz : z ≠ 0
der1 :
  ∀ x ∈ uIcc 0 (π / 2),
    HasDerivAt (fun y ↦ ↑(sin y) * ↑(cos y) ^ (n - 1)) (↑(cos x) ^ n - (↑n - 1) * ↑(sin x) ^ 2 * ↑(cos x) ^ (n - 2)) x
⊢ (↑n / (2 * z) * ∫ (x : ℝ) in 0..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ n) -
      (↑n - 1) / (2 * z) * ∫ (x : ℝ) in 0..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (n - 2) =
    0 - 0 * (-Complex.cos (2 * z * 0) / (2 * z)) -
      ∫ (x : ℝ) in 0..π / 2,
        (↑(cos x) ^ n - (↑n - 1) * ↑(sin x) ^ 2 * ↑(cos x) ^ (n - 2)) * (-Complex.cos (2 * z * ↑x) / (2 * z))

pp: case e'_3
z : ℂ
n : ℕ
hn : 2 ≤ n
hz : z ≠ 0
der1 :
  ∀ x ∈ uIcc 0 (π / 2),
    HasDerivAt (fun y ↦ ↑(sin y) * ↑(cos y) ^ (n - 1)) (↑(cos x) ^ n - (↑n - 1) * ↑(sin x) ^ 2 * ↑(cos x) ^ (n - 2)) x
⊢ n - 1 ≠ 0

Tactic:
zero_mul,

Goal state after:
case e'_3
z : ℂ
n : ℕ
hn : 2 ≤ n
hz : z ≠ 0
der1 :
  ∀ x ∈ uIcc 0 (π / 2),
    HasDerivAt (fun y ↦ ↑(sin y) * ↑(cos y) ^ (n - 1)) (↑(cos x) ^ n - (↑n - 1) * ↑(sin x) ^ 2 * ↑(cos x) ^ (n - 2)) x
⊢ (↑n / (2 * z) * ∫ (x : ℝ) in 0..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ n) -
      (↑n - 1) / (2 * z) * ∫ (x : ℝ) in 0..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (n - 2) =
    0 - 0 -
      ∫ (x : ℝ) in 0..π / 2,
        (↑(cos x) ^ n - (↑n - 1) * ↑(sin x) ^ 2 * ↑(cos x) ^ (n - 2)) * (-Complex.cos (2 * z * ↑x) / (2 * z))

case e'_3
z : ℂ
n : ℕ
hn : 2 ≤ n
hz : z ≠ 0
der1 :
  ∀ x ∈ uIcc 0 (π / 2),
    HasDerivAt (fun y ↦ ↑(sin y) * ↑(cos y) ^ (n - 1)) (↑(cos x) ^ n - (↑n - 1) * ↑(sin x) ^ 2 * ↑(cos x) ^ (n - 2)) x
⊢ n - 1 ≠ 0
Module: Mathlib.Analysis.MellinTransform

Goal state before:
pp: case hbc.inl
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
a b : ℝ
f : ℝ → E
s : ℂ
hfc : LocallyIntegrableOn f (Ioi 0) volume
hf_top : f =O[atTop] fun x ↦ x ^ (-a)
hs_top : s.re < a
hf_bot : f =O[𝓝[>] 0] fun x ↦ x ^ (-b)
hs_bot : b < s.re
F : ℂ → ℝ → E := fun z t ↦ ↑t ^ (z - 1) • f t
F' : ℂ → ℝ → E := fun z t ↦ (↑t ^ (z - 1) * ↑(log t)) • f t
v : ℝ
hv0 : 0 < v
hv1 : v < s.re - b
hv2 : v < a - s.re
bound : ℝ → ℝ := fun t ↦ (t ^ (s.re + v - 1) + t ^ (s.re - v - 1)) * |log t| * ‖f t‖
h1 : ∀ᶠ (z : ℂ) in 𝓝 s, AEStronglyMeasurable (F z) (volume.restrict (Ioi 0))
h2 : IntegrableOn (F s) (Ioi 0) volume
h3 : AEStronglyMeasurable (F' s) (volume.restrict (Ioi 0))
t : ℝ
ht : t ∈ Ioi 0
z : ℂ
hz : z ∈ Metric.ball s v
h : 1 ≤ t
⊢ (z - 1).re ≤ s.re + v - 1

Tactic:
rw [sub_re, one_re, sub_le_sub_iff_right]

Goal state after:
case hbc.inl
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
a b : ℝ
f : ℝ → E
s : ℂ
hfc : LocallyIntegrableOn f (Ioi 0) volume
hf_top : f =O[atTop] fun x ↦ x ^ (-a)
hs_top : s.re < a
hf_bot : f =O[𝓝[>] 0] fun x ↦ x ^ (-b)
hs_bot : b < s.re
F : ℂ → ℝ → E := fun z t ↦ ↑t ^ (z - 1) • f t
F' : ℂ → ℝ → E := fun z t ↦ (↑t ^ (z - 1) * ↑(log t)) • f t
v : ℝ
hv0 : 0 < v
hv1 : v < s.re - b
hv2 : v < a - s.re
bound : ℝ → ℝ := fun t ↦ (t ^ (s.re + v - 1) + t ^ (s.re - v - 1)) * |log t| * ‖f t‖
h1 : ∀ᶠ (z : ℂ) in 𝓝 s, AEStronglyMeasurable (F z) (volume.restrict (Ioi 0))
h2 : IntegrableOn (F s) (Ioi 0) volume
h3 : AEStronglyMeasurable (F' s) (volume.restrict (Ioi 0))
t : ℝ
ht : t ∈ Ioi 0
z : ℂ
hz : z ∈ Metric.ball s v
h : 1 ≤ t
⊢ z.re ≤ s.re + v
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta

Goal state before:
pp: case e'_4
u v : ℂ
hu : 0 < u.re
hv : 0 < v.re
⊢ (fun x ↦ ↑(-x) ^ (u - 1) * (1 - ↑(-x)) ^ (v - 1)) = fun x ↦ ↑(x + 1) ^ (v - 1) * (1 - ↑(x + 1)) ^ (u - 1)

pp: case e'_6
u v : ℂ
hu : 0 < u.re
hv : 0 < v.re
⊢ -(1 / 2) = 1 / 2 - 1

pp: case e'_7
u v : ℂ
hu : 0 < u.re
hv : 0 < v.re
⊢ -1 = 0 - 1

Tactic:
· ext1 x
    conv_lhs => rw [mul_comm]
    congr 2 <;> · push_cast; ring

Goal state after:
case e'_6
u v : ℂ
hu : 0 < u.re
hv : 0 < v.re
⊢ -(1 / 2) = 1 / 2 - 1

case e'_7
u v : ℂ
hu : 0 < u.re
hv : 0 < v.re
⊢ -1 = 0 - 1
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd

Goal state before:
pp: z : ℂ
n : ℕ
hz : z ≠ 0
⊢ 2 ≤ 2 * n + 2

Tactic:
lia

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd

Goal state before:
pp: case e_a
n : ℕ
L : IntervalIntegrable (fun i ↦ sin i ^ n) volume 0 (π / 2)
R : IntervalIntegrable (fun i ↦ sin i ^ n) volume (π / 2) π
⊢ ∫ (x : ℝ) in 0..π / 2, cos x ^ n = ∫ (x : ℝ) in 0..π / 2, sin x ^ n

Tactic:
(by ring : 0 = π / 2 - π / 2)

Goal state after:
case e_a
n : ℕ
L : IntervalIntegrable (fun i ↦ sin i ^ n) volume 0 (π / 2)
R : IntervalIntegrable (fun i ↦ sin i ^ n) volume (π / 2) π
⊢ ∫ (x : ℝ) in π / 2 - π / 2..π / 2, cos x ^ n = ∫ (x : ℝ) in 0..π / 2, sin x ^ n
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd

Goal state before:
pp: case e_a
n : ℕ
L : IntervalIntegrable (fun i ↦ sin i ^ n) volume 0 (π / 2)
R : IntervalIntegrable (fun i ↦ sin i ^ n) volume (π / 2) π
⊢ ∫ (x : ℝ) in 0..π / 2, cos x ^ n = ∫ (x : ℝ) in π / 2..π / 2 + π / 2, sin x ^ n

Tactic:
nth_rw 2 [(by ring : π / 2 = 0 + π / 2)]

Goal state after:
case e_a
n : ℕ
L : IntervalIntegrable (fun i ↦ sin i ^ n) volume 0 (π / 2)
R : IntervalIntegrable (fun i ↦ sin i ^ n) volume (π / 2) π
⊢ ∫ (x : ℝ) in 0..π / 2, cos x ^ n = ∫ (x : ℝ) in 0 + π / 2..π / 2 + π / 2, sin x ^ n
Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup

Goal state before:
pp: f : ℝ → ℝ
x : ℝ
n : ℕ
hf_conv : ConvexOn ℝ (Ioi 0) f
hf_feq : ∀ {y : ℝ}, 0 < y → f (y + 1) = f y + log y
hn : 2 ≤ n
hx : 0 < x
⊢ 1 < n

Tactic:
lia

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

Goal state before:
pp: s t : ℂ
hs : 0 < s.re
ht : 0 < t.re
conv_int :
  ∫ (x : ℝ) in Ioi 0,
      ∫ (t_1 : ℝ) in 0..x, ↑(rexp (-t_1)) * ↑t_1 ^ (s - 1) * (↑(rexp (-(x - t_1))) * ↑(x - t_1) ^ (t - 1)) ∂volume =
    (∫ (x : ℝ) in Ioi 0, ↑(rexp (-x)) * ↑x ^ (s - 1) ∂volume) * ∫ (x : ℝ) in Ioi 0, ↑(rexp (-x)) * ↑x ^ (t - 1) ∂volume
hst : 0 < (s + t).re
⊢ ∫ (x : ℝ) in Ioi 0,
      ∫ (t_1 : ℝ) in 0..x, ↑(rexp (-t_1)) * ↑t_1 ^ (s - 1) * (↑(rexp (-(x - t_1))) * ↑(x - t_1) ^ (t - 1)) ∂volume =
    ∫ (a : ℝ) in Ioi 0, ↑(rexp (-a)) * ↑a ^ (s + t - 1) * s.betaIntegral t

Tactic:
refine setIntegral_congr_fun measurableSet_Ioi fun x hx => ?_

Goal state after:
s t : ℂ
hs : 0 < s.re
ht : 0 < t.re
conv_int :
  ∫ (x : ℝ) in Ioi 0,
      ∫ (t_1 : ℝ) in 0..x, ↑(rexp (-t_1)) * ↑t_1 ^ (s - 1) * (↑(rexp (-(x - t_1))) * ↑(x - t_1) ^ (t - 1)) ∂volume =
    (∫ (x : ℝ) in Ioi 0, ↑(rexp (-x)) * ↑x ^ (s - 1) ∂volume) * ∫ (x : ℝ) in Ioi 0, ↑(rexp (-x)) * ↑x ^ (t - 1) ∂volume
hst : 0 < (s + t).re
x : ℝ
hx : x ∈ Ioi 0
⊢ ∫ (t_1 : ℝ) in 0..x, ↑(rexp (-t_1)) * ↑t_1 ^ (s - 1) * (↑(rexp (-(x - t_1))) * ↑(x - t_1) ^ (t - 1)) =
    ↑(rexp (-x)) * ↑x ^ (s + t - 1) * s.betaIntegral t
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd

Goal state before:
pp: z : ℂ
hz : z ≠ 0
n : ℕ
A : ℂ := ∏ j ∈ Finset.range n, (1 - z ^ 2 / (↑j + 1) ^ 2)
B : ℂ := ∫ (x : ℝ) in 0..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (2 * n)
C : ℝ := ∫ (x : ℝ) in 0..π / 2, cos x ^ (2 * n)
hn : Complex.sin (↑π * z) = ↑π * z * A * B / ↑C
aux' : 2 * n.succ = 2 * n + 2
⊢ 1 / 2 *
      ((0 * 0 ^ (2 * n) * cos 0 - 0 * 0 ^ (2 * n) * cos π) / (↑(2 * n) + 2) +
        (↑(2 * n) + 1) / (↑(2 * n) + 2) * ∫ (x : ℝ) in 0..π, sin x ^ (2 * n)) =
    (2 * ↑n + 1) / (2 * ↑n + 2) * (1 / 2 * ∫ (x : ℝ) in 0..π, sin x ^ (2 * n))

Tactic:
zero_mul,

Goal state after:
z : ℂ
hz : z ≠ 0
n : ℕ
A : ℂ := ∏ j ∈ Finset.range n, (1 - z ^ 2 / (↑j + 1) ^ 2)
B : ℂ := ∫ (x : ℝ) in 0..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (2 * n)
C : ℝ := ∫ (x : ℝ) in 0..π / 2, cos x ^ (2 * n)
hn : Complex.sin (↑π * z) = ↑π * z * A * B / ↑C
aux' : 2 * n.succ = 2 * n + 2
⊢ 1 / 2 *
      ((0 * cos 0 - 0 * cos π) / (↑(2 * n) + 2) +
        (↑(2 * n) + 1) / (↑(2 * n) + 2) * ∫ (x : ℝ) in 0..π, sin x ^ (2 * n)) =
    (2 * ↑n + 1) / (2 * ↑n + 2) * (1 / 2 * ∫ (x : ℝ) in 0..π, sin x ^ (2 * n))
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd

Goal state before:
pp: z : ℂ
hz : z ≠ 0
n : ℕ
A : ℂ := ∏ j ∈ Finset.range n, (1 - z ^ 2 / (↑j + 1) ^ 2)
B : ℂ := ∫ (x : ℝ) in 0..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (2 * n)
C : ℝ := ∫ (x : ℝ) in 0..π / 2, cos x ^ (2 * n)
hn : Complex.sin (↑π * z) = ↑π * z * A * B / ↑C
aux' : 2 * n.succ = 2 * n + 2
⊢ 1 / 2 *
      ((0 * cos 0 - 0 * cos π) / (↑(2 * n) + 2) +
        (↑(2 * n) + 1) / (↑(2 * n) + 2) * ∫ (x : ℝ) in 0..π, sin x ^ (2 * n)) =
    (2 * ↑n + 1) / (2 * ↑n + 2) * (1 / 2 * ∫ (x : ℝ) in 0..π, sin x ^ (2 * n))

Tactic:
zero_mul,

Goal state after:
z : ℂ
hz : z ≠ 0
n : ℕ
A : ℂ := ∏ j ∈ Finset.range n, (1 - z ^ 2 / (↑j + 1) ^ 2)
B : ℂ := ∫ (x : ℝ) in 0..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (2 * n)
C : ℝ := ∫ (x : ℝ) in 0..π / 2, cos x ^ (2 * n)
hn : Complex.sin (↑π * z) = ↑π * z * A * B / ↑C
aux' : 2 * n.succ = 2 * n + 2
⊢ 1 / 2 * ((0 - 0 * cos π) / (↑(2 * n) + 2) + (↑(2 * n) + 1) / (↑(2 * n) + 2) * ∫ (x : ℝ) in 0..π, sin x ^ (2 * n)) =
    (2 * ↑n + 1) / (2 * ↑n + 2) * (1 / 2 * ∫ (x : ℝ) in 0..π, sin x ^ (2 * n))
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd

Goal state before:
pp: z : ℂ
hz : z ≠ 0
n : ℕ
A : ℂ := ∏ j ∈ Finset.range n, (1 - z ^ 2 / (↑j + 1) ^ 2)
B : ℂ := ∫ (x : ℝ) in 0..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (2 * n)
C : ℝ := ∫ (x : ℝ) in 0..π / 2, cos x ^ (2 * n)
hn : Complex.sin (↑π * z) = ↑π * z * A * B / ↑C
aux' : 2 * n.succ = 2 * n + 2
⊢ 1 / 2 * ((0 - 0 * cos π) / (↑(2 * n) + 2) + (↑(2 * n) + 1) / (↑(2 * n) + 2) * ∫ (x : ℝ) in 0..π, sin x ^ (2 * n)) =
    (2 * ↑n + 1) / (2 * ↑n + 2) * (1 / 2 * ∫ (x : ℝ) in 0..π, sin x ^ (2 * n))

Tactic:
zero_mul,

Goal state after:
z : ℂ
hz : z ≠ 0
n : ℕ
A : ℂ := ∏ j ∈ Finset.range n, (1 - z ^ 2 / (↑j + 1) ^ 2)
B : ℂ := ∫ (x : ℝ) in 0..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (2 * n)
C : ℝ := ∫ (x : ℝ) in 0..π / 2, cos x ^ (2 * n)
hn : Complex.sin (↑π * z) = ↑π * z * A * B / ↑C
aux' : 2 * n.succ = 2 * n + 2
⊢ 1 / 2 * ((0 - 0) / (↑(2 * n) + 2) + (↑(2 * n) + 1) / (↑(2 * n) + 2) * ∫ (x : ℝ) in 0..π, sin x ^ (2 * n)) =
    (2 * ↑n + 1) / (2 * ↑n + 2) * (1 / 2 * ∫ (x : ℝ) in 0..π, sin x ^ (2 * n))
Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup

Goal state before:
pp: f : ℝ → ℝ
x : ℝ
hf_conv : ConvexOn ℝ (Ioi 0) f
hf_feq : ∀ {y : ℝ}, 0 < y → f (y + 1) = f y + log y
hx : 0 < x
hx' : x ≤ 1
n : ℕ
⊢ n + 1 ≠ 0

Tactic:
lia

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

Goal state before:
pp: case refine_2
f : ℝ → ℝ
x : ℝ
n : ℕ
hf_conv : ConvexOn ℝ (Ioi 0) f
hf_feq : ∀ {y : ℝ}, 0 < y → f (y + 1) = f y + log y
hx : 0 < x
hn : n ≠ 0
⊢ 2 ≤ n + 1

Tactic:
lia

Goal state after:
Module: Mathlib.Analysis.MellinTransform

Goal state before:
pp: s : ℂ
hs : 0 < s.re
⊢ -1 < (s - 1).re

Tactic:
simpa only [sub_re, one_re, sub_eq_add_neg] using! lt_add_of_pos_left _ hs

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

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

Tactic:
log_mul A.ne' (Gamma_pos_of_pos A).ne',

Goal state after:
case refine_2
A : 0 < 3 / 2
this : log (3 / 2) + log (Γ (3 / 2)) ≤ 1 / 2 * log 2
⊢ Γ (3 / 2) < 1
Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup

Goal state before:
pp: s : ℝ
hs : s ∈ Ioi 0
h1 : √π ≠ 0
h2 : Γ (s / 2) ≠ 0
h3 : Γ (s / 2 + 1 / 2) ≠ 0
h4 : 2 ^ (s - 1) ≠ 0
⊢ log (Γ (s / 2) * Γ (s / 2 + 1 / 2)) + log (2 ^ (s - 1)) - log √π =
    (fun s ↦ log (Γ (s / 2)) + log (Γ (s / 2 + 1 / 2)) + s * log 2 - log (2 * √π)) s

Tactic:
log_mul h2 h3,

Goal state after:
s : ℝ
hs : s ∈ Ioi 0
h1 : √π ≠ 0
h2 : Γ (s / 2) ≠ 0
h3 : Γ (s / 2 + 1 / 2) ≠ 0
h4 : 2 ^ (s - 1) ≠ 0
⊢ log (Γ (s / 2)) + log (Γ (s / 2 + 1 / 2)) + log (2 ^ (s - 1)) - log √π =
    (fun s ↦ log (Γ (s / 2)) + log (Γ (s / 2 + 1 / 2)) + s * log 2 - log (2 * √π)) s
Module: Mathlib.Topology.Algebra.AsymptoticCone

Goal state before:
pp: k : Type u_1
V : Type u_2
inst✝⁹ : Field k
inst✝⁸ : LinearOrder k
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module k V
inst✝⁵ : TopologicalSpace V
inst✝⁴ : TopologicalSpace k
inst✝³ : OrderTopology k
inst✝² : IsStrictOrderedRing k
inst✝¹ : IsTopologicalAddGroup V
inst✝ : ContinuousSMul k V
v : V
⊢ map (fun x ↦ v) atTop ≤ asymptoticNhds k V 0

Tactic:
have : (fun _ => v) =ᶠ[atTop (α := k)]
      (Function.uncurry (· • ·)) ∘ (fun c => (c, c⁻¹ • v)) := by
    filter_upwards [eventually_ne_atTop 0] with _ h
    simp [h]

Goal state after:
k : Type u_1
V : Type u_2
inst✝⁹ : Field k
inst✝⁸ : LinearOrder k
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module k V
inst✝⁵ : TopologicalSpace V
inst✝⁴ : TopologicalSpace k
inst✝³ : OrderTopology k
inst✝² : IsStrictOrderedRing k
inst✝¹ : IsTopologicalAddGroup V
inst✝ : ContinuousSMul k V
v : V
this : (fun x ↦ v) =ᶠ[atTop] (Function.uncurry fun x1 x2 ↦ x1 • x2) ∘ fun c ↦ (c, c⁻¹ • v)
⊢ map (fun x ↦ v) atTop ≤ asymptoticNhds k V 0
Module: Mathlib.Analysis.Normed.Affine.Ceva

Goal state before:
pp: 𝕜 : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : SeminormedAddCommGroup V
inst✝³ : NormedField 𝕜
inst✝² : NormedSpace 𝕜 V
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor V P
t : Triangle 𝕜 P
p : Fin 3 → P
p' : P
r : Fin 3 → 𝕜
hr : ∀ (i : Fin 3), (AffineMap.lineMap (t.points (i + 1)) (t.points (i + 2))) (r i) = p i
hp' : ∀ (i : Fin 3), p' ∈ line[𝕜, t.points i, (AffineMap.lineMap (t.points (i + 1)) (t.points (i + 2))) (r i)]
⊢ (∏ x, ‖r x‖) * ∏ x, dist (t.points (x + 1)) (t.points (x + 2)) =
    (∏ x, ‖1 - r x‖) * ∏ x, dist (t.points (x + 1)) (t.points (x + 2))

Tactic:
← norm_prod,

Goal state after:
𝕜 : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : SeminormedAddCommGroup V
inst✝³ : NormedField 𝕜
inst✝² : NormedSpace 𝕜 V
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor V P
t : Triangle 𝕜 P
p : Fin 3 → P
p' : P
r : Fin 3 → 𝕜
hr : ∀ (i : Fin 3), (AffineMap.lineMap (t.points (i + 1)) (t.points (i + 2))) (r i) = p i
hp' : ∀ (i : Fin 3), p' ∈ line[𝕜, t.points i, (AffineMap.lineMap (t.points (i + 1)) (t.points (i + 2))) (r i)]
⊢ ‖∏ b, r b‖ * ∏ x, dist (t.points (x + 1)) (t.points (x + 2)) =
    ‖∏ b, (1 - r b)‖ * ∏ x, dist (t.points (x + 1)) (t.points (x + 2))
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta

Goal state before:
pp: m : ℕ
IH : ∀ (s : ℂ), ⌊1 - s.re⌋₊ = m → Tendsto s.GammaSeq atTop (𝓝 (Gamma s))
s : ℂ
hs : ⌊1 - s.re⌋₊ = m + 1
hsne : s ≠ 0
⊢ m + 1 ≠ 0

Tactic:
lia

Goal state after:
Module: Mathlib.LinearAlgebra.AffineSpace.Ceva

Goal state before:
pp: case e'_3
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝⁴ : Ring k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
inst✝ : Fintype ι
p : ι → P
hp : AffineIndependent k p
s : Set ι
hs : s.Nonempty
w : ↑s → ι → k
hw : ∀ (i : ↑s), ∑ j, w i j = 1
p' : P
hp' : ∀ (i : ↑s), p' ∈ line[k, p ↑i, (Finset.affineCombination k Finset.univ p) (w i)]
w'' : ι → k
fs'' : Finset ι
hw'' : ∑ j ∈ fs'', w'' j = 1
hw''p' : (Finset.affineCombination k fs'' p) w'' = p'
hi : ∀ (i : ↑s), ∃ r, ∀ (j : ι), r * (↑Finset.univ \ {↑i}).indicator (w i) j = (↑fs'' \ {↑i}).indicator w'' j
i : ↑s
r : k
hr : ∀ (j : ι), r * (↑Finset.univ \ {↑i}).indicator (w i) j = (↑fs'' \ {↑i}).indicator w'' j
j : ι
⊢ {↑i}ᶜ.indicator ((↑fs'').indicator w'') j = (↑fs'' \ {↑i}).indicator w'' j

Tactic:
by_cases hj : j = (i : ι)

Goal state after:
case pos
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝⁴ : Ring k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
inst✝ : Fintype ι
p : ι → P
hp : AffineIndependent k p
s : Set ι
hs : s.Nonempty
w : ↑s → ι → k
hw : ∀ (i : ↑s), ∑ j, w i j = 1
p' : P
hp' : ∀ (i : ↑s), p' ∈ line[k, p ↑i, (Finset.affineCombination k Finset.univ p) (w i)]
w'' : ι → k
fs'' : Finset ι
hw'' : ∑ j ∈ fs'', w'' j = 1
hw''p' : (Finset.affineCombination k fs'' p) w'' = p'
hi : ∀ (i : ↑s), ∃ r, ∀ (j : ι), r * (↑Finset.univ \ {↑i}).indicator (w i) j = (↑fs'' \ {↑i}).indicator w'' j
i : ↑s
r : k
hr : ∀ (j : ι), r * (↑Finset.univ \ {↑i}).indicator (w i) j = (↑fs'' \ {↑i}).indicator w'' j
j : ι
hj : j = ↑i
⊢ {↑i}ᶜ.indicator ((↑fs'').indicator w'') j = (↑fs'' \ {↑i}).indicator w'' j

case neg
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝⁴ : Ring k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
inst✝ : Fintype ι
p : ι → P
hp : AffineIndependent k p
s : Set ι
hs : s.Nonempty
w : ↑s → ι → k
hw : ∀ (i : ↑s), ∑ j, w i j = 1
p' : P
hp' : ∀ (i : ↑s), p' ∈ line[k, p ↑i, (Finset.affineCombination k Finset.univ p) (w i)]
w'' : ι → k
fs'' : Finset ι
hw'' : ∑ j ∈ fs'', w'' j = 1
hw''p' : (Finset.affineCombination k fs'' p) w'' = p'
hi : ∀ (i : ↑s), ∃ r, ∀ (j : ι), r * (↑Finset.univ \ {↑i}).indicator (w i) j = (↑fs'' \ {↑i}).indicator w'' j
i : ↑s
r : k
hr : ∀ (j : ι), r * (↑Finset.univ \ {↑i}).indicator (w i) j = (↑fs'' \ {↑i}).indicator w'' j
j : ι
hj : ¬j = ↑i
⊢ {↑i}ᶜ.indicator ((↑fs'').indicator w'') j = (↑fs'' \ {↑i}).indicator w'' j
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta

Goal state before:
pp: s : ℂ
hs : ∀ (m : ℕ), s ≠ -↑m
h_im : s.im = 0
⊢ ↑s.re + 0 * I = ↑s.re

Tactic:
zero_mul,

Goal state after:
s : ℂ
hs : ∀ (m : ℕ), s ≠ -↑m
h_im : s.im = 0
⊢ ↑s.re + 0 = ↑s.re
Module: Mathlib.Analysis.Normed.Affine.Simplex

Goal state before:
pp: R : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : Ring R
inst✝³ : SeminormedAddCommGroup V
inst✝² : PseudoMetricSpace P
inst✝¹ : Module R V
inst✝ : NormedAddTorsor V P
n : ℕ
s : Simplex R P n
hr : s.Regular
i j : Fin (n + 1)
hij : i ≠ j
⊢ n ≠ 0

Tactic:
lia

Goal state after:
Module: Mathlib.Analysis.Normed.Affine.Simplex

Goal state before:
pp: R : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : Ring R
inst✝³ : SeminormedAddCommGroup V
inst✝² : PseudoMetricSpace P
inst✝¹ : Module R V
inst✝ : NormedAddTorsor V P
n : ℕ
s : Simplex R P n
hr : s.Regular
i j : Fin (n + 1)
hij : i ≠ j
hn : n ≠ 0
hi : i = 1
x : P ≃ᵢ P
hx : s.points ∘ ⇑(Equiv.swap 0 j) = ⇑x ∘ s.points
⊢ 1 ≠ j

Tactic:
lia

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

Goal state before:
pp: case e'_3
s : ℂ
this : (fun z ↦ (Gamma z)⁻¹ * (Gamma (z + 1 / 2))⁻¹) = fun z ↦ (Gamma (2 * z))⁻¹ * 2 ^ (2 * z - 1) / ↑√π
⊢ Gamma (2 * s) * 2 ^ (1 - 2 * s) * ↑√π = ((Gamma (2 * s))⁻¹ * 2 ^ (2 * s - 1) / ↑√π)⁻¹

Tactic:
· rw [div_eq_mul_inv, mul_inv, mul_inv, inv_inv, inv_inv, ← cpow_neg, neg_sub]

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

Goal state before:
pp: f : ℝ[X]
n : ℕ
g₁ g₂ : ℝ[X]
hf : (g₁ * g₂).IsMonicOfDegree (2 + n)
h : f = g₁ * g₂
hd₁ : g₁.IsMonicOfDegree 1
⊢ 2 + n = 1 + (n + 1)

Tactic:
lia

Goal state after: