mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.InnerProductSpace.Reproducing

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁷ : RCLike 𝕜
X : Type u_2
V : Type u_3
inst✝⁶ : NormedAddCommGroup V
inst✝⁵ : InnerProductSpace 𝕜 V
H : Type u_4
inst✝⁴ : NormedAddCommGroup H
inst✝³ : InnerProductSpace 𝕜 H
inst✝² : RKHS 𝕜 H X V
inst✝¹ : CompleteSpace H
inst✝ : CompleteSpace V
C : ℝ
s : Set X
hC : ∀ x ∈ s, ‖kerFun H x‖ ≤ C
ι : Type u_5
l : Filter ι
F : ι → H
f : H
h : Tendsto F l (𝓝 f)
ε : ℝ
hε : ε > 0
hnorm : Tendsto (fun x ↦ ‖F x - f‖ * C) l (𝓝 0)
n : ι
hn : ‖F n - f‖ * C < ε
x : X
hx : x ∈ s
⊢ ‖F n - f‖ * ‖kerFun H x‖ < ε

Tactic:
hC x hx,

Goal state after:
𝕜 : Type u_1
inst✝⁷ : RCLike 𝕜
X : Type u_2
V : Type u_3
inst✝⁶ : NormedAddCommGroup V
inst✝⁵ : InnerProductSpace 𝕜 V
H : Type u_4
inst✝⁴ : NormedAddCommGroup H
inst✝³ : InnerProductSpace 𝕜 H
inst✝² : RKHS 𝕜 H X V
inst✝¹ : CompleteSpace H
inst✝ : CompleteSpace V
C : ℝ
s : Set X
hC : ∀ x ∈ s, ‖kerFun H x‖ ≤ C
ι : Type u_5
l : Filter ι
F : ι → H
f : H
h : Tendsto F l (𝓝 f)
ε : ℝ
hε : ε > 0
hnorm : Tendsto (fun x ↦ ‖F x - f‖ * C) l (𝓝 0)
n : ι
hn : ‖F n - f‖ * C < ε
x : X
hx : x ∈ s
⊢ ‖F n - f‖ * C < ε
Module: Mathlib.MeasureTheory.Measure.Hausdorff

Goal state before:
pp: case inr
X : Type u_2
inst✝² : EMetricSpace X
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
s : Set X
hs : s.Subsingleton
d : ℝ
hd : 0 ≤ d
x : X
hx : x ∈ s
⊢ μH[d] s ≤ 1

Tactic:
(subsingleton_iff_singleton hx).1 hs

Goal state after:
case inr
X : Type u_2
inst✝² : EMetricSpace X
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
s : Set X
hs : s.Subsingleton
d : ℝ
hd : 0 ≤ d
x : X
hx : x ∈ s
⊢ μH[d] {x} ≤ 1
Module: Mathlib.Analysis.InnerProductSpace.StarOrder

Goal state before:
pp: 𝕜 : Type u_1
H : Type u_2
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup H
inst✝³ : InnerProductSpace 𝕜 H
inst✝² : CompleteSpace H
inst✝¹ : Algebra ℝ (H →L[𝕜] H)
inst✝ : IsScalarTower ℝ 𝕜 (H →L[𝕜] H)
f : H →L[𝕜] H
hf : f.IsPositive
c✝ : ℝ
c : ℝ := -c✝
hc : 0 < c
x : H
⊢ ‖x‖ ^ 2 * c = re (↑c * ⟪x, x⟫_𝕜)

Tactic:
re_ofReal_mul,

Goal state after:
𝕜 : Type u_1
H : Type u_2
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup H
inst✝³ : InnerProductSpace 𝕜 H
inst✝² : CompleteSpace H
inst✝¹ : Algebra ℝ (H →L[𝕜] H)
inst✝ : IsScalarTower ℝ 𝕜 (H →L[𝕜] H)
f : H →L[𝕜] H
hf : f.IsPositive
c✝ : ℝ
c : ℝ := -c✝
hc : 0 < c
x : H
⊢ ‖x‖ ^ 2 * c = c * re ⟪x, x⟫_𝕜
Module: Mathlib.MeasureTheory.Measure.Hausdorff

Goal state before:
pp: X : Type u_2
Y : Type u_3
inst✝⁵ : EMetricSpace X
inst✝⁴ : EMetricSpace Y
inst✝³ : MeasurableSpace X
inst✝² : BorelSpace X
inst✝¹ : MeasurableSpace Y
inst✝ : BorelSpace Y
f : X → Y
d : ℝ
hd : 0 ≤ d
s : Set Y
hf : AntilipschitzWith 0 f
x : X
hx : x ∈ f ⁻¹' s
this : Subsingleton X
⊢ f ⁻¹' s = {x}

Tactic:
have : (f ⁻¹' s).Subsingleton := subsingleton_univ.anti (subset_univ _)

Goal state after:
X : Type u_2
Y : Type u_3
inst✝⁵ : EMetricSpace X
inst✝⁴ : EMetricSpace Y
inst✝³ : MeasurableSpace X
inst✝² : BorelSpace X
inst✝¹ : MeasurableSpace Y
inst✝ : BorelSpace Y
f : X → Y
d : ℝ
hd : 0 ≤ d
s : Set Y
hf : AntilipschitzWith 0 f
x : X
hx : x ∈ f ⁻¹' s
this✝ : Subsingleton X
this : (f ⁻¹' s).Subsingleton
⊢ f ⁻¹' s = {x}
Module: Mathlib.Analysis.InnerProductSpace.Reproducing

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁴ : RCLike 𝕜
X : Type u_2
V : Type u_3
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace 𝕜 V
inst✝¹ : CompleteSpace V
K : Matrix X X (V →L[𝕜] V)
inst✝ : Fact K.PosSemidef
⊢ kernel (OfKernel K) = K

Tactic:
ext x y v
  refine ext_inner_right 𝕜 fun w ↦ ?_
  simp [kernel, adjoint_inner_left, -inner_kerFun, -kerFun_inner,
    coeCLM, OfKernel.kerFun, inner_H₀_def, RKHS.kerFun]

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Hausdorff

Goal state before:
pp: E : Type u_5
P : Type u_6
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace P
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor E P
inst✝ : BorelSpace P
x y : P
s : Set ℝ
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
⊢ μH[1] ((fun x_1 ↦ x_1 • (y -ᵥ x)) '' s) = nndist x y • μH[1] s

Tactic:
hausdorffMeasure_smul_right_image,

Goal state after:
E : Type u_5
P : Type u_6
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace P
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor E P
inst✝ : BorelSpace P
x y : P
s : Set ℝ
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
⊢ ‖y -ᵥ x‖₊ • μH[1] s = nndist x y • μH[1] s
Module: Mathlib.Analysis.InnerProductSpace.TwoDim

Goal state before:
pp: case refine_1.inl
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x : E
h : 0 = ‖o.rightAngleRotationAux₁ x‖
⊢ ‖o.rightAngleRotationAux₁ x‖ ≤ ‖x‖

Tactic:
rw [← h]

Goal state after:
case refine_1.inl
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x : E
h : 0 = ‖o.rightAngleRotationAux₁ x‖
⊢ 0 ≤ ‖x‖
Module: Mathlib.Analysis.InnerProductSpace.TwoDim

Goal state before:
pp: case refine_1.inl
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x : E
h : 0 = ‖o.rightAngleRotationAux₁ x‖
⊢ 0 ≤ ‖x‖

Tactic:
positivity

Goal state after:
Module: Mathlib.Analysis.LocallyConvex.WeakSpace

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁸ : RCLike 𝕜
inst✝⁷ : AddCommGroup E
inst✝⁶ : Module 𝕜 E
inst✝⁵ : Module ℝ E
inst✝⁴ : IsScalarTower ℝ 𝕜 E
inst✝³ : TopologicalSpace E
inst✝² : IsTopologicalAddGroup E
inst✝¹ : ContinuousSMul 𝕜 E
inst✝ : LocallyConvexSpace ℝ E
s : Set E
hs : Convex ℝ s
x : E
hx : (toWeakSpace 𝕜 E).toEquiv x ∈ (⇑(toWeakSpace 𝕜 E) '' closure s)ᶜ
this : ContinuousSMul ℝ E
f : StrongDual 𝕜 E
u : ℝ
hus : ∀ a ∈ closure s, RCLike.re (f a) < u
hux : u < RCLike.re (f x)
f' : StrongDual 𝕜 (WeakSpace 𝕜 E) :=
  let __LinearMap := ↑f ∘ₗ ↑(toWeakSpace 𝕜 E).symm;
  { toLinearMap := __LinearMap, cont := ⋯ }
hux' : u < (RCLike.reCLM ∘SL ContinuousLinearMap.restrictScalars ℝ f') ((toWeakSpace 𝕜 E) x)
⊢ closure (⇑(toWeakSpace 𝕜 E) '' s) ⊆ {y | (RCLike.reCLM ∘SL ContinuousLinearMap.restrictScalars ℝ f') y ≤ u}

Tactic:
refine closure_minimal ?_ <| isClosed_le (by fun_prop) (by fun_prop)

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝⁸ : RCLike 𝕜
inst✝⁷ : AddCommGroup E
inst✝⁶ : Module 𝕜 E
inst✝⁵ : Module ℝ E
inst✝⁴ : IsScalarTower ℝ 𝕜 E
inst✝³ : TopologicalSpace E
inst✝² : IsTopologicalAddGroup E
inst✝¹ : ContinuousSMul 𝕜 E
inst✝ : LocallyConvexSpace ℝ E
s : Set E
hs : Convex ℝ s
x : E
hx : (toWeakSpace 𝕜 E).toEquiv x ∈ (⇑(toWeakSpace 𝕜 E) '' closure s)ᶜ
this : ContinuousSMul ℝ E
f : StrongDual 𝕜 E
u : ℝ
hus : ∀ a ∈ closure s, RCLike.re (f a) < u
hux : u < RCLike.re (f x)
f' : StrongDual 𝕜 (WeakSpace 𝕜 E) :=
  let __LinearMap := ↑f ∘ₗ ↑(toWeakSpace 𝕜 E).symm;
  { toLinearMap := __LinearMap, cont := ⋯ }
hux' : u < (RCLike.reCLM ∘SL ContinuousLinearMap.restrictScalars ℝ f') ((toWeakSpace 𝕜 E) x)
⊢ ⇑(toWeakSpace 𝕜 E) '' s ⊆ {y | (RCLike.reCLM ∘SL ContinuousLinearMap.restrictScalars ℝ f') y ≤ u}
Module: Mathlib.Analysis.LocallyConvex.WeakSpace

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁸ : RCLike 𝕜
inst✝⁷ : AddCommGroup E
inst✝⁶ : Module 𝕜 E
inst✝⁵ : Module ℝ E
inst✝⁴ : IsScalarTower ℝ 𝕜 E
inst✝³ : TopologicalSpace E
inst✝² : IsTopologicalAddGroup E
inst✝¹ : ContinuousSMul 𝕜 E
inst✝ : LocallyConvexSpace ℝ E
s : Set E
⊢ ⇑(toWeakSpace 𝕜 E) '' (closedConvexHull 𝕜) s = (closedConvexHull 𝕜) (⇑(toWeakSpace 𝕜 E) '' s)

Tactic:
rw [closedConvexHull_eq_closure_convexHull (𝕜 := 𝕜),
    ((convex_convexHull 𝕜 s).lift ℝ).toWeakSpace_closure _, closedConvexHull_eq_closure_convexHull]
  congr
  refine LinearMap.image_convexHull (toWeakSpace 𝕜 E).toLinearMap s

Goal state after:
Module: Mathlib.Analysis.LocallyConvex.WeakOperatorTopology

Goal state before:
pp: 𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst✝¹⁵ : NormedField 𝕜₁
inst✝¹⁴ : NormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
E : Type u_3
F : Type u_4
inst✝¹³ : AddCommGroup E
inst✝¹² : TopologicalSpace E
inst✝¹¹ : Module 𝕜₁ E
inst✝¹⁰ : AddCommGroup F
inst✝⁹ : TopologicalSpace F
inst✝⁸ : Module 𝕜₂ F
inst✝⁷ : IsTopologicalAddGroup F
inst✝⁶ : ContinuousConstSMul 𝕜₂ F
S : Type u_5
inst✝⁵ : DistribSMul S F
inst✝⁴ : SMulCommClass 𝕜₂ S F
inst✝³ : ContinuousConstSMul S F
inst✝² : SMul S 𝕜₂
inst✝¹ : IsScalarTower S 𝕜₂ 𝕜₂
inst✝ : IsScalarTower S 𝕜₂ F
c : S
⊢ Continuous[instTopologicalSpace, instTopologicalSpace] fun x ↦ c • x

Tactic:
apply continuous_of_dual_apply_continuous fun _ _ ↦ ?_
    simp only [smul_apply, ContinuousLinearMap.map_smul_of_tower]
    exact continuous_const_smul c |>.comp <| continuous_dual_apply ..

Goal state after:
Module: Mathlib.Analysis.InnerProductSpace.TwoDim

Goal state before:
pp: case neg.mpr
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x : E
hx : ¬x = 0
r : ℝ
hr : 0 ≤ r
h : SameRay ℝ x (r • x)
⊢ 0 ≤ r * ‖x‖ ^ 2

Tactic:
positivity

Goal state after:
Module: Mathlib.Analysis.InnerProductSpace.TwoDim

Goal state before:
pp: case ha
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x y : E
⊢ 0 ≤ ‖(o.kahler x) y‖

Tactic:
positivity

Goal state after:
Module: Mathlib.Analysis.InnerProductSpace.TwoDim

Goal state before:
pp: case hb
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x y : E
⊢ 0 ≤ ‖x‖ * ‖y‖

Tactic:
positivity

Goal state after:
Module: Mathlib.Analysis.InnerProductSpace.TwoDim

Goal state before:
pp: case inl
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x y : E
hx : (o.kahler x) y = 0
this : ‖x‖ * ‖y‖ = 0
h : ‖x‖ = 0
⊢ x = 0 ∨ y = 0

pp: case inr
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x y : E
hx : (o.kahler x) y = 0
this : ‖x‖ * ‖y‖ = 0
h : ‖y‖ = 0
⊢ x = 0 ∨ y = 0

Tactic:
· left
    simpa using h

Goal state after:
case inr
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x y : E
hx : (o.kahler x) y = 0
this : ‖x‖ * ‖y‖ = 0
h : ‖y‖ = 0
⊢ x = 0 ∨ y = 0
Module: Mathlib.Analysis.InnerProductSpace.TwoDim

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x y : E
⊢ (o.kahler x) y = 0 ↔ x = 0 ∨ y = 0

Tactic:
refine ⟨o.eq_zero_or_eq_zero_of_kahler_eq_zero, ?_⟩
  rintro (rfl | rfl) <;> simp

Goal state after:
Module: Mathlib.Analysis.MellinInversion

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
σ : ℝ
f : ℝ → E
x : ℝ
hx : 0 < x
g : ℝ → E := fun u ↦ rexp (-σ * u) • f (rexp (-u))
hf : Integrable g volume
hFf : Integrable (𝓕 g) volume
hfx : ContinuousAt g (-Real.log x)
⊢ ↑x ^ (-↑σ) • rexp (σ * Real.log x) • f (rexp (Real.log x)) = f x

Tactic:
by
      norm_cast
      rw [mul_comm σ, ← rpow_def_of_pos hx, Real.exp_log hx, ← Complex.ofReal_cpow hx.le]
      norm_cast
      rw [← smul_assoc, smul_eq_mul, Real.rpow_neg hx.le,
        inv_mul_cancel₀ (ne_of_gt (rpow_pos_of_pos hx σ)), one_smul]

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

Goal state before:
pp: s t a b : ℝ
hs : 0 < s
ht : 0 < t
ha : 0 < a
hb : 0 < b
hab : a + b = 1
f : ℝ → ℝ → ℝ → ℝ := fun c u x ↦ rexp (-c * x) * x ^ (c * (u - 1))
e : (1 / a).HolderConjugate (1 / b)
hab' : b = 1 - a
⊢ 0 < a * s + b * t

Tactic:
positivity

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

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

Tactic:
positivity

Goal state after:
Module: Mathlib.Analysis.MellinTransform

Goal state before:
pp: 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
⊢ 0 ≤ t ^ (s.re - v - 1)

Tactic:
positivity

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds

Goal state before:
pp: g : ℝ → ℝ
t : ℝ
hg : Tendsto (fun x ↦ x * g x) atTop (𝓝 t)
⊢ Tendsto (fun x ↦ (1 + g x) ^ x) atTop (𝓝 (rexp t))

Tactic:
have hg0 := tendsto_zero_of_isBoundedUnder_smul_of_tendsto_cobounded
    hg.norm.isBoundedUnder_le (tendsto_id'.mpr (by simp))
  rw [← tendsto_ofReal_iff] at hg ⊢
  push_cast at hg ⊢
  apply (Complex.tendsto_one_add_cpow_exp_of_tendsto hg).congr'
  filter_upwards [hg0.eventually_const_le (show (-1 : ℝ) < 0 by simp)] with x hg1
  rw [Complex.ofReal_cpow (by linarith), Complex.ofReal_add, Complex.ofReal_one]

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

Goal state before:
pp: u : ℂ
hu : 0 < u.re
v : ℂ
x : ℝ
hx : x ∈ uIcc 0 (1 / 2)
⊢ 0 ≤ 1 / 2

Tactic:
positivity

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

Goal state before:
pp: case hx
x y a : ℝ
ha : 0 < a
hb : 0 < 1 - a
hab : a + (1 - a) = 1
hx : 0 < x
hy : 0 < y
⊢ Γ x ^ a ≠ 0

Tactic:
positivity

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

Goal state before:
pp: case hy
x y a : ℝ
ha : 0 < a
hb : 0 < 1 - a
hab : a + (1 - a) = 1
hx : 0 < x
hy : 0 < y
⊢ Γ y ^ (1 - a) ≠ 0

Tactic:
positivity

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

Goal state before:
pp: case hx
x y a : ℝ
ha : 0 < a
hb : 0 < 1 - a
hab : a + (1 - a) = 1
hx : 0 < x
hy : 0 < y
⊢ 0 < Γ y

Tactic:
positivity

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

Goal state before:
pp: case hx
x y a : ℝ
ha : 0 < a
hb : 0 < 1 - a
hab : a + (1 - a) = 1
hx : 0 < x
hy : 0 < y
⊢ 0 < Γ x

Tactic:
positivity

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

Goal state before:
pp: z : ℂ
n : ℕ
hn : 2 ≤ n
hz : z ≠ 0
nne : ↑n ≠ 0
this :
  ∫ (x : ℝ) in 0..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ n =
    ↑n / (2 * z) * ∫ (x : ℝ) in 0..π / 2, Complex.sin (2 * z * ↑x) * ↑(sin x) * ↑(cos x) ^ (n - 1)
⊢ (1 - 4 * z ^ 2 / ↑n ^ 2) * ∫ (x : ℝ) in 0..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ n =
    (↑n - 1) / ↑n * ∫ (x : ℝ) in 0..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (n - 2)

Tactic:
rw [integral_sin_mul_sin_mul_cos_pow_eq hn hz, sub_eq_neg_add, mul_add, ← sub_eq_iff_eq_add]
    at this

Goal state after:
z : ℂ
n : ℕ
hn : 2 ≤ n
hz : z ≠ 0
nne : ↑n ≠ 0
this :
  (∫ (x : ℝ) in 0..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ n) -
      ↑n / (2 * z) * (↑n / (2 * z) * ∫ (x : ℝ) in 0..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ n) =
    ↑n / (2 * z) * -((↑n - 1) / (2 * z) * ∫ (x : ℝ) in 0..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (n - 2))
⊢ (1 - 4 * z ^ 2 / ↑n ^ 2) * ∫ (x : ℝ) in 0..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ n =
    (↑n - 1) / ↑n * ∫ (x : ℝ) in 0..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (n - 2)
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
⊢ 0 < u.re + 1

Tactic:
positivity

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
⊢ 0 < v.re + 1

Tactic:
positivity

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

Goal state before:
pp: case refine_3
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
⊢ ∀ᶠ (b : ℕ) in atTop, logGammaSeq x b ≤ f x - f 1

Tactic:
change ∀ᶠ n : ℕ in atTop, logGammaSeq x n ≤ f x - f 1

Goal state after:
case refine_3
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 : ℕ) in atTop, logGammaSeq x n ≤ f x - f 1
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd

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

Tactic:
ext1 n
    rw [Function.comp_apply, ← Complex.ofReal_mul, Complex.re_ofReal_mul]
    suffices
      (∏ j ∈ Finset.range n, (1 - x ^ 2 / (j + 1) ^ 2) : ℂ) =
        (∏ j ∈ Finset.range n, (1 - x ^ 2 / (j + 1) ^ 2) : ℝ) by
      rw [this, Complex.ofReal_re]
    simp

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

Goal state after:
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
⊢ 0 < u.re + 1

Tactic:
positivity

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

Goal state before:
pp: s : ℂ
hs : 0 < s.re
f : ℕ → ℝ → ℂ := fun n ↦ (Ioc 0 ↑n).indicator fun x ↦ ↑((1 - x / ↑n) ^ n) * ↑x ^ (s - 1)
n : ℕ
⊢ 0 ≤ ↑n

Tactic:
positivity

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

Goal state before:
pp: s : ℂ
hs : 0 < s.re
f : ℕ → ℝ → ℂ := fun n ↦ (Ioc 0 ↑n).indicator fun x ↦ ↑((1 - x / ↑n) ^ n) * ↑x ^ (s - 1)
f_ible : ∀ (n : ℕ), Integrable (f n) (volume.restrict (Ioi 0))
f_tends : ∀ x ∈ Ioi 0, Tendsto (fun n ↦ f n x) atTop (𝓝 (↑(rexp (-x)) * ↑x ^ (s - 1)))
n : ℕ
⊢ 0 ≤ ↑n

Tactic:
positivity

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

Goal state before:
pp: case inl
s : ℂ
hs : 0 < s.re
f : ℕ → ℝ → ℂ := fun n ↦ (Ioc 0 ↑n).indicator fun x ↦ ↑((1 - x / ↑n) ^ n) * ↑x ^ (s - 1)
f_ible : ∀ (n : ℕ), Integrable (f n) (volume.restrict (Ioi 0))
f_tends : ∀ x ∈ Ioi 0, Tendsto (fun n ↦ f n x) atTop (𝓝 (↑(rexp (-x)) * ↑x ^ (s - 1)))
n : ℕ
x : ℝ
hx : 0 < x
hxn : ↑n < x
⊢ 0 ≤ x ^ (s.re - 1)

Tactic:
positivity

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

Goal state before:
pp: s : ℂ
hs : 0 < s.re
f : ℕ → ℝ → ℂ := fun n ↦ (Ioc 0 ↑n).indicator fun x ↦ ↑((1 - x / ↑n) ^ n) * ↑x ^ (s - 1)
f_ible : ∀ (n : ℕ), Integrable (f n) (volume.restrict (Ioi 0))
f_tends : ∀ x ∈ Ioi 0, Tendsto (fun n ↦ f n x) atTop (𝓝 (↑(rexp (-x)) * ↑x ^ (s - 1)))
n : ℕ
x : ℝ
hx : 0 < x
hxn : x ≤ ↑n
⊢ 0 ≤ ↑n

Tactic:
positivity

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

Goal state before:
pp: z : ℂ
n : ℕ
hn : n ≠ 0
aux : ∀ (a b c d : ℂ), a * b * (c * d) = a * c * (b * d)
this✝ : ↑n ^ z * ↑n ^ (1 - z) = ↑n
this : ∀ (j : ℕ), (z + ↑(j + 1)) * (1 - z + ↑j) = ↑((j + 1) ^ 2) * (1 - z ^ 2 / (↑j + 1) ^ 2)
⊢ n ! ≠ 0

Tactic:
positivity

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

Goal state before:
pp: z : ℂ
⊢ Gamma z * Gamma (1 - z) = ↑π / sin (↑π * z)

Tactic:
have pi_ne : (π : ℂ) ≠ 0 := Complex.ofReal_ne_zero.mpr pi_ne_zero
  by_cases hs : sin (↑π * z) = 0
  · -- first deal with silly case z = integer
    rw [hs, div_zero]
    rw [← neg_eq_zero, ← Complex.sin_neg, ← mul_neg, Complex.sin_eq_zero_iff, mul_comm] at hs
    obtain ⟨k, hk⟩ := hs
    rw [mul_eq_mul_right_iff, eq_false (ofReal_ne_zero.mpr pi_pos.ne'), or_false,
      neg_eq_iff_eq_neg] at hk
    rw [hk]
    cases k
    · rw [Int.ofNat_eq_natCast, Int.cast_natCast, Complex.Gamma_neg_nat_eq_zero, zero_mul]
    · rw [Int.cast_negSucc, neg_neg, Nat.cast_add, Nat.cast_one, add_comm, sub_add_cancel_left,
        Complex.Gamma_neg_nat_eq_zero, mul_zero]
  refine tendsto_nhds_unique ((GammaSeq_tendsto_Gamma z).mul (GammaSeq_tendsto_Gamma <| 1 - z)) ?_
  have : ↑π / sin (↑π * z) = 1 * (π / sin (π * z)) := by rw [one_mul]
  convert!
    Tendsto.congr'
      ((eventually_ne_atTop 0).mp (Eventually.of_forall fun n hn => (GammaSeq_mul z hn).symm))
      (Tendsto.mul _ _)
  · convert! tendsto_natCast_div_add_atTop (1 - z) using 1; ext1 n; rw [add_sub_assoc]
  · have : ↑π / sin (↑π * z) = 1 / (sin (π * z) / π) := by simp
    convert! tendsto_const_nhds.div _ (div_ne_zero hs pi_ne)
    rw [← tendsto_mul_iff_of_ne_zero tendsto_const_nhds pi_ne, div_mul_cancel₀ _ pi_ne]
    convert! tendsto_euler_sin_prod z using 1
    ext1 n; rw [mul_comm, ← mul_assoc]

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

Goal state before:
pp: case inr
⊢ (Gamma 0)⁻¹ = 0 * (Gamma (0 + 1))⁻¹

Tactic:
rw [zero_add, Gamma_zero, inv_zero, zero_mul]

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 ≠ 0

Tactic:
simp [hn]

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.trans (Equiv.swap 0 i) (Equiv.swap 1 j)) = ⇑x ∘ s.points
⊢ 1 ≠ 0

Tactic:
simp [hn]

Goal state after:
Module: Mathlib.Analysis.Normed.Algebra.GelfandMazur

Goal state before:
pp: X : Type u_1
E : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : PreconnectedSpace X
inst✝ : SeminormedAddCommGroup E
f : X → E
M : ℝ
x : X
hM : 0 < M
hx : ‖f x‖ = M
h : IsMinOn (fun x ↦ ‖f x‖) univ x
hf : Continuous[inst✝², PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
H : ∀ {y : X} (z : X), ‖f y‖ = M → ∀ n > 0, ‖f z‖ ≤ M * (1 + (‖f z - f y‖ / M) ^ n)
y w : X
hw : w ∈ {y | ‖f y‖ = M}
u : X
hu : ‖f u - f w‖ / M < 1
⊢ 0 ≤ ‖f u - f w‖ / M

Tactic:
positivity

Goal state after:
Module: Mathlib.Analysis.Normed.Algebra.TrivSqZeroExt

Goal state before:
pp: 𝕜 : Type u_1
S : Type u_2
R : Type u_3
M : Type u_4
inst✝¹¹ : SeminormedCommRing S
inst✝¹⁰ : SeminormedRing R
inst✝⁹ : SeminormedAddCommGroup M
inst✝⁸ : Algebra S R
inst✝⁷ : Module S M
inst✝⁶ : IsBoundedSMul S R
inst✝⁵ : IsBoundedSMul S M
inst✝⁴ : Module R M
inst✝³ : IsBoundedSMul R M
inst✝² : Module Rᵐᵒᵖ M
inst✝¹ : IsBoundedSMul Rᵐᵒᵖ M
inst✝ : SMulCommClass R Rᵐᵒᵖ M
r₁ : R
m₁ : M
r₂ : R
m₂ : M
⊢ 0 ≤ ‖m₁‖ * ‖m₂‖

Tactic:
positivity

Goal state after:
Module: Mathlib.Analysis.Normed.Algebra.GelfandMazur

Goal state before:
pp: F : Type u_1
inst✝³ : NormedRing F
inst✝² : NormOneClass F
inst✝¹ : NormMulClass F
inst✝ : NormedAlgebra ℂ F
x : F
z : ℂ
hz : IsMinOn (fun x_1 ↦ ‖x - (algebraMap ℂ F) x_1‖) univ z
H : ∀ (z' : ℂ), ‖x - (algebraMap ℂ F) z'‖ ≠ 0
c : ℂ
M : ℝ := ‖x - (algebraMap ℂ F) z‖
hMdef : M = ‖x - (algebraMap ℂ F) z‖
this : ‖x - (algebraMap ℂ F) z‖ ≠ 0
⊢ 0 < M

Tactic:
positivity

Goal state after:
Module: Mathlib.Analysis.Normed.Algebra.GelfandMazur

Goal state before:
pp: F : Type u_1
inst✝³ : NormedRing F
inst✝² : NormOneClass F
inst✝¹ : NormMulClass F
inst✝ : NormedAlgebra ℂ F
x : F
z : ℂ
hz : IsMinOn (fun x_1 ↦ ‖x - (algebraMap ℂ F) x_1‖) univ z
H : ∀ (z' : ℂ), ‖x - (algebraMap ℂ F) z'‖ ≠ 0
c : ℂ
M : ℝ := ‖x - (algebraMap ℂ F) z‖
hMdef : M = ‖x - (algebraMap ℂ F) z‖
hM₀ : 0 < M
y w : ℂ
hy : ‖x - (algebraMap ℂ F) y‖ = M
n : ℕ
hn : n > 0
⊢ 0 < M ^ (n - 1)

Tactic:
positivity

Goal state after: