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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T S : E →ₗ[𝕜] E
hT : T.IsPositive
hS : S.IsPositive
x : E
⊢ 0 ≤ re ⟪(T + S) x, x⟫

Tactic:
rw [add_apply, inner_add_left, map_add]

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T S : E →ₗ[𝕜] E
hT : T.IsPositive
hS : S.IsPositive
x : E
⊢ 0 ≤ re ⟪T x, x⟫ + re ⟪S x, x⟫
Module: Mathlib.Analysis.InnerProductSpace.Positive

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
hT : IsIdempotentElem T
h : T.IsSymmetric
x : E
⊢ 0 ≤ re ⟪T x, x⟫

Tactic:
← hT.eq,

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
hT : IsIdempotentElem T
h : T.IsSymmetric
x : E
⊢ 0 ≤ re ⟪(T * T) x, x⟫
Module: Mathlib.Analysis.InnerProductSpace.Positive

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
p q : E →ₗ[𝕜] E
hp : p.IsSymmetricProjection
hq : q.IsSymmetricProjection
x✝ : p ≤ q
a : E
ha : a ∈ p.range
h1 : (q - p).IsSymmetric
h2 : ∀ (x : E), 0 ≤ re ⟪(q - p) x, x⟫
⊢ a ∈ q.range

Tactic:
specialize h2 a

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
p q : E →ₗ[𝕜] E
hp : p.IsSymmetricProjection
hq : q.IsSymmetricProjection
x✝ : p ≤ q
a : E
ha : a ∈ p.range
h1 : (q - p).IsSymmetric
h2 : 0 ≤ re ⟪(q - p) a, a⟫
⊢ a ∈ q.range
Module: Mathlib.Analysis.InnerProductSpace.Positive

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : InnerProductSpace 𝕜 F
inst✝¹ : CompleteSpace E
inst✝ : CompleteSpace F
T : E →L[𝕜] E
hT : T.IsPositive
S : F →L[𝕜] E
⊢ (adjoint S ∘SL T ∘SL S).IsPositive

Tactic:
by
  convert! hT.conj_adjoint (S†)
  rw [adjoint_adjoint]

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

Goal state before:
pp: case pos
V : Type u
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : CompleteSpace V
B : V →L[ℝ] V →L[ℝ] ℝ
C : ℝ
C_ge_0 : 0 < C
coercivity : ∀ (u : V), C * ‖u‖ * ‖u‖ ≤ (B u) u
v : V
h : 0 < ‖v‖
⊢ C * ‖v‖ ≤ ‖(continuousLinearMapOfBilin B) v‖

Tactic:
refine (mul_le_mul_iff_left₀ h).mp ?_
    calc
      C * ‖v‖ * ‖v‖ ≤ B v v := coercivity v
      _ = ⟪B♯ v, v⟫_ℝ := (continuousLinearMapOfBilin_apply B v v).symm
      _ ≤ ‖B♯ v‖ * ‖v‖ := real_inner_le_norm (B♯ v) v

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

Goal state before:
pp: case mp
R : Type u_1
E : Type u_2
F : Type u_3
inst✝¹¹ : CommRing R
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module R E
inst✝⁷ : Module R F
inst✝⁶ : TopologicalSpace E
inst✝⁵ : TopologicalSpace F
f : E →ₗ.[R] F
inst✝⁴ : ContinuousAdd E
inst✝³ : ContinuousAdd F
inst✝² : TopologicalSpace R
inst✝¹ : ContinuousSMul R E
inst✝ : ContinuousSMul R F
hf : f.toFun.ker = ⊥
hf' : f.IsClosable
f' : F →ₗ.[R] E
h : f.inverse.graph.topologicalClosure = f'.graph
⊢ ∀ (m : ↥f.closure.domain), f.closure.toFun m = 0 → m = 0

Tactic:
intro ⟨x, hx⟩ hx'

Goal state after:
case mp
R : Type u_1
E : Type u_2
F : Type u_3
inst✝¹¹ : CommRing R
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module R E
inst✝⁷ : Module R F
inst✝⁶ : TopologicalSpace E
inst✝⁵ : TopologicalSpace F
f : E →ₗ.[R] F
inst✝⁴ : ContinuousAdd E
inst✝³ : ContinuousAdd F
inst✝² : TopologicalSpace R
inst✝¹ : ContinuousSMul R E
inst✝ : ContinuousSMul R F
hf : f.toFun.ker = ⊥
hf' : f.IsClosable
f' : F →ₗ.[R] E
h : f.inverse.graph.topologicalClosure = f'.graph
x : E
hx : x ∈ f.closure.domain
hx' : f.closure.toFun ⟨x, hx⟩ = 0
⊢ ⟨x, hx⟩ = 0
Module: Mathlib.Analysis.InnerProductSpace.SingularValues

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁶ : RCLike 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace 𝕜 E
inst✝³ : FiniteDimensional 𝕜 E
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 F
inst✝ : FiniteDimensional 𝕜 F
T : E →ₗ[𝕜] F
n : ℕ
hn : n < finrank 𝕜 E
⊢ End.HasEigenvalue (adjoint T ∘ₗ T) (↑(T.singularValues n) ^ 2)

Tactic:
convert! T.isSymmetric_adjoint_comp_self.hasEigenvalue_eigenvalues rfl ⟨n, hn⟩ using 1
  simp [← T.sq_singularValues_fin]

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace 𝕜 F
x x' : E
y y' : F
⊢ nndist (x ⊗ₜ[𝕜] y) (x' ⊗ₜ[𝕜] y') ≤ ‖x‖₊ * ‖y‖₊ + ‖x'‖₊ * ‖y'‖₊

Tactic:
grw [nndist_eq_nnnorm, nnnorm_sub_le]

Goal state after:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace 𝕜 F
x x' : E
y y' : F
⊢ ‖x ⊗ₜ[𝕜] y‖₊ + ‖x' ⊗ₜ[𝕜] y'‖₊ ≤ ‖x‖₊ * ‖y‖₊ + ‖x'‖₊ * ‖y'‖₊
Module: Mathlib.Analysis.FunctionalSpaces.SobolevInequality

Goal state before:
pp: F : Type u_3
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace ℝ F
E : Type u_4
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : MeasurableSpace E
inst✝³ : BorelSpace E
inst✝² : FiniteDimensional ℝ E
μ : Measure E
inst✝¹ : μ.IsAddHaarMeasure
inst✝ : FiniteDimensional ℝ F
u : E → F
hu : ContDiff ℝ 1 u
h2u : HasCompactSupport u
p p' : ℝ≥0
hp : 1 ≤ p
hn : 0 < finrank ℝ E
hp' : (↑p')⁻¹ = ↑p⁻¹ - (↑(finrank ℝ E))⁻¹
F' : Type := EuclideanSpace ℝ (Fin (finrank ℝ F))
e : F ≃L[ℝ] F' := toEuclidean
C₁ : ℝ≥0 := ‖↑e.symm‖₊
C : ℝ≥0 := eLpNormLESNormFDerivOfEqInnerConst μ ↑p
C₂ : ℝ≥0 := ‖↑e‖₊
v : E → F' := ⇑e ∘ u
hv : ContDiff ℝ 1 v
h2v : HasCompactSupport v
this : eLpNorm v (↑p') μ ≤ ↑(eLpNormLESNormFDerivOfEqInnerConst μ ↑p) * eLpNorm (fderiv ℝ v) (↑p) μ
h4v : ∀ (x : E), ‖fderiv ℝ v x‖ ≤ ↑C₂ * ‖fderiv ℝ u x‖
⊢ ↑C₁ * ↑C * (↑C₂ * eLpNorm (fderiv ℝ u) (↑p) μ) = ↑(SNormLESNormFDerivOfEqConst F μ ↑p) * eLpNorm (fderiv ℝ u) (↑p) μ

Tactic:
simp_rw [C₂, C₁, C, e, SNormLESNormFDerivOfEqConst]
      push_cast
      simp_rw [mul_assoc]

Goal state after:
Module: Mathlib.Geometry.Euclidean.Volume.Measure

Goal state before:
pp: X : Type u_1
inst✝² : EMetricSpace X
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
basis : OrthonormalBasis (Fin 0) ℝ (EuclideanSpace ℝ (Fin 0)) := EuclideanSpace.basisFun (Fin 0) ℝ
heq : {0} = parallelepiped ⇑basis
h✝ : volume = volume.addHaarScalarFactor μH[↑0] • μH[↑0]
h : (volume.addHaarScalarFactor μH[↑0] • μH[↑0]) {0} = 1
⊢ μHE[0] = μH[0]

Tactic:
simp_rw [CharP.cast_eq_zero, smul_apply, hausdorffMeasure_zero_singleton, ENNReal.smul_def,
    smul_eq_mul, mul_one, ENNReal.coe_eq_one] at h

Goal state after:
X : Type u_1
inst✝² : EMetricSpace X
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
basis : OrthonormalBasis (Fin 0) ℝ (EuclideanSpace ℝ (Fin 0)) := EuclideanSpace.basisFun (Fin 0) ℝ
heq : {0} = parallelepiped ⇑basis
h✝ : volume = volume.addHaarScalarFactor μH[↑0] • μH[↑0]
h : volume.addHaarScalarFactor μH[0] = 1
⊢ μHE[0] = μH[0]
Module: Mathlib.Analysis.InnerProductSpace.NormDet

Goal state before:
pp: 𝕜 : Type u_1
U : Type u_2
V : Type u_3
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup U
inst✝³ : InnerProductSpace 𝕜 U
inst✝² : FiniteDimensional 𝕜 U
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace 𝕜 V
f : U →ₗ[𝕜] V
⊢ 0 ≤
    if h : Nonempty (OrthonormalBasis (Fin (finrank 𝕜 U)) 𝕜 ↥f.range) then
      ‖((toMatrix (stdOrthonormalBasis 𝕜 U).toBasis h.some.toBasis) f.rangeRestrict).det‖
    else 0

Tactic:
split

Goal state after:
case isTrue
𝕜 : Type u_1
U : Type u_2
V : Type u_3
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup U
inst✝³ : InnerProductSpace 𝕜 U
inst✝² : FiniteDimensional 𝕜 U
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace 𝕜 V
f : U →ₗ[𝕜] V
h✝ : Nonempty (OrthonormalBasis (Fin (finrank 𝕜 U)) 𝕜 ↥f.range)
⊢ 0 ≤ ‖((toMatrix (stdOrthonormalBasis 𝕜 U).toBasis h✝.some.toBasis) f.rangeRestrict).det‖

case isFalse
𝕜 : Type u_1
U : Type u_2
V : Type u_3
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup U
inst✝³ : InnerProductSpace 𝕜 U
inst✝² : FiniteDimensional 𝕜 U
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace 𝕜 V
f : U →ₗ[𝕜] V
h✝ : ¬Nonempty (OrthonormalBasis (Fin (finrank 𝕜 U)) 𝕜 ↥f.range)
⊢ 0 ≤ 0
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
⊢ (kernel H).IsHermitian

Tactic:
by
  ext
  refine ext_inner_right 𝕜 fun w ↦ ?_
  simp only [Matrix.conjTranspose_apply, star, adjoint_inner_left,
    ← inner_conj_symm _ (kernel H _ _ _), kernel_inner, inner_conj_symm]

Goal state after:
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)
this : ∀ {h p1 p2 p3 : Prop}, (h → [p1, p2, p3].TFAE) → [h ∧ p1, h ∧ p2, h ∧ p3].TFAE
hHerm : K.IsHermitian
x✝ : Nontrivial V
v✝ : V
hv : v✝ ≠ 0
tfae_1_to_2 :
  (∀ (x : X →₀ V →L[𝕜] V) (x_1 : V),
      0 ≤ RCLike.re (x.sum fun i a ↦ x.sum fun i_1 a_1 ↦ ⟪(K i i_1) (a_1 x_1), a x_1⟫_𝕜)) →
    ∀ (f : X × V →₀ 𝕜),
      0 ≤ RCLike.re (f.sum fun xv z ↦ f.sum fun xv' w ↦ (starRingEnd 𝕜) z * w * ⟪(K xv'.1 xv.1) xv.2, xv'.2⟫_𝕜)
tfae_2_to_3 :
  (∀ (f : X × V →₀ 𝕜),
      0 ≤ RCLike.re (f.sum fun xv z ↦ f.sum fun xv' w ↦ (starRingEnd 𝕜) z * w * ⟪(K xv'.1 xv.1) xv.2, xv'.2⟫_𝕜)) →
    ∀ (vv : X →₀ V), 0 ≤ RCLike.re (vv.sum fun x w ↦ vv.sum fun x' w' ↦ ⟪(K x' x) w, w'⟫_𝕜)
h : ∀ (vv : X →₀ V), 0 ≤ RCLike.re (vv.sum fun x w ↦ vv.sum fun x' w' ↦ ⟪(K x' x) w, w'⟫_𝕜)
ff : X →₀ V →L[𝕜] V
v : V
⊢ 0 ≤ RCLike.re (ff.sum fun i a ↦ ff.sum fun i_1 a_1 ↦ ⟪(K i i_1) (a_1 v), a v⟫_𝕜)

Tactic:
by
    rw [Finsupp.sum_comm]
    simpa [Finsupp.sum_sum_index, inner_add_right, inner_add_left] using
      h (ff.sum fun x T ↦ .single x (T v))

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝³ : RCLike 𝕜
inst✝² : Fintype ι
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
b : OrthonormalBasis ι 𝕜 E
i : ι
⊢ ((toMatrix b.toBasis b.toBasis) T).diag i = ⟪b i, T (b i)⟫_𝕜

Tactic:
Matrix.diag_apply,

Goal state after:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝³ : RCLike 𝕜
inst✝² : Fintype ι
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
b : OrthonormalBasis ι 𝕜 E
i : ι
⊢ (toMatrix b.toBasis b.toBasis) T i i = ⟪b i, T (b i)⟫_𝕜
Module: Mathlib.Analysis.InnerProductSpace.Reproducing

Goal state before:
pp: case single_add
𝕜 : 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
K : Matrix X X (V →L[𝕜] V)
inst✝ : Fact K.PosSemidef
f : OfKernel K
h : (ContinuousLinearMap.pi fun x ↦ adjoint (kerFun K x)) f = 0
i : X × V
a : 𝕜
f✝ : X × V →₀ 𝕜
a✝² : i ∉ f✝.support
a✝¹ : a ≠ 0
a✝ : ⟪↑f✝, f⟫_𝕜 = 0
this✝ : ⟪i.2, (ContinuousLinearMap.pi fun x ↦ adjoint (kerFun K x)) f i.1⟫_𝕜 = ⟪i.2, 0 i.1⟫_𝕜
this : ⟪↑(Finsupp.single i 1), f⟫_𝕜 = 0
⊢ UniformSpace.Completion.toComplL (Finsupp.single i a) = a • ↑(Finsupp.single i 1)

Tactic:
simp [← UniformSpace.Completion.coe_toComplL (𝕜 := 𝕜),
      ← map_smul, -SeparationQuotient.mkCLM_apply, -UniformSpace.Completion.coe_toComplL]

Goal state after:
Module: Mathlib.Analysis.MellinTransform

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℝ → E
s : ℂ
a : ℝ
ha : a ≠ 0
| |a|⁻¹ • ∫ (x : ℝ) in Ioi 0, (|a| * x ^ (a - 1)) • ↑(x ^ a) ^ (s / ↑a - 1) • f (x ^ a)

Tactic:
← integral_smul

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℝ → E
s : ℂ
a : ℝ
ha : a ≠ 0
| ∫ (a_1 : ℝ) in Ioi 0, |a|⁻¹ • (|a| * a_1 ^ (a - 1)) • ↑(a_1 ^ a) ^ (s / ↑a - 1) • f (a_1 ^ a)
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Deriv

Goal state before:
pp: case neg
s : ℂ
hs : s ≠ 0
h : ∀ (m : ℕ), s ≠ -↑m
⊢ deriv Gamma (s + 1) = Gamma s + s * deriv Gamma s

Tactic:
· suffices HasDerivWithinAt (fun s ↦ Gamma (s + 1)) (Gamma s + s * deriv Gamma s) {0}ᶜ s by
      rw [← deriv_comp_add_const]
      exact (this.hasDerivAt (compl_singleton_mem_nhds hs)).deriv
    refine HasDerivWithinAt.congr ?_ Gamma_add_one (Gamma_add_one s hs)
    simpa using! HasDerivWithinAt.mul (hasDerivWithinAt_id s {0}ᶜ)
      (differentiableAt_Gamma s h).hasDerivAt.hasDerivWithinAt

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

Goal state before:
pp: case e_a
s t : ℂ
a : ℝ
ha : 0 < a
ha' : ↑a ≠ 0
A : ↑a ^ (s + t - 1) = ↑a * (↑a ^ (s - 1) * ↑a ^ (t - 1))
x : ℝ
hx : x ∈ Ioc 0 a
⊢ (↑a - ↑x) ^ (t - 1) = ↑a ^ (t - 1) * (1 - ↑(x / a)) ^ (t - 1)

Tactic:
(by norm_cast : (1 : ℂ) - ↑(x / a) = ↑(1 - x / a)),

Goal state after:
case e_a
s t : ℂ
a : ℝ
ha : 0 < a
ha' : ↑a ≠ 0
A : ↑a ^ (s + t - 1) = ↑a * (↑a ^ (s - 1) * ↑a ^ (t - 1))
x : ℝ
hx : x ∈ Ioc 0 a
⊢ (↑a - ↑x) ^ (t - 1) = ↑a ^ (t - 1) * ↑(1 - x / a) ^ (t - 1)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd

Goal state before:
pp: case inr.succ
z : ℂ
hz : z ≠ 0
n : ℕ
hn :
  Complex.sin (↑π * z) =
    ((↑π * 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))
⊢ Complex.sin (↑π * z) =
    ((↑π * z * ∏ j ∈ Finset.range (n + 1), (1 - z ^ 2 / (↑j + 1) ^ 2)) *
        ∫ (x : ℝ) in 0..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (2 * (n + 1))) /
      ↑(∫ (x : ℝ) in 0..π / 2, cos x ^ (2 * (n + 1)))

Tactic:
hn,

Goal state after:
case inr.succ
z : ℂ
hz : z ≠ 0
n : ℕ
hn :
  Complex.sin (↑π * z) =
    ((↑π * 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))
⊢ ((↑π * 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)) =
    ((↑π * z * ∏ j ∈ Finset.range (n + 1), (1 - z ^ 2 / (↑j + 1) ^ 2)) *
        ∫ (x : ℝ) in 0..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (2 * (n + 1))) /
      ↑(∫ (x : ℝ) in 0..π / 2, cos x ^ (2 * (n + 1)))
Module: Mathlib.Analysis.MellinTransform

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

Tactic:
hs,

Goal state after:
s : ℂ
aux1 : -1 < (s - 1).re
hs : s = 0
⊢ re 0 ≤ 0
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)
⊢ f x - f 1 = f (x - 1) - f 1 + log (x - 1) - x * 0

Tactic:
· have := hf_feq ((Nat.cast_nonneg m).trans_lt hy)
      rw [sub_add_cancel] at this
      rw [this]
      ring

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 * u.betaIntegral (v + 1) = v * (u + 1).betaIntegral v

Tactic:
rw [betaIntegral, betaIntegral, ← sub_eq_zero]
    convert! int_ev <;> ring

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
inst✝⁴ : TopologicalSpace k
inst✝³ : OrderTopology k
inst✝² : IsStrictOrderedRing k
inst✝¹ : IsTopologicalAddGroup V
inst✝ : ContinuousSMul k V
v : V
p : P → Prop
⊢ (∀ᶠ (x : P) in (atTop • 𝓝 v).bind (asymptoticNhds k P), p x) ↔ ∀ᶠ (x : P) in asymptoticNhds k P v, p x

Tactic:
eventually_bind,

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
inst✝⁴ : TopologicalSpace k
inst✝³ : OrderTopology k
inst✝² : IsStrictOrderedRing k
inst✝¹ : IsTopologicalAddGroup V
inst✝ : ContinuousSMul k V
v : V
p : P → Prop
⊢ (∀ᶠ (x : V) in atTop • 𝓝 v, ∀ᶠ (y : P) in asymptoticNhds k P x, p y) ↔ ∀ᶠ (x : P) in asymptoticNhds k P v, p x
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta

Goal state before:
pp: case e'_3
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 : ℝ) in 0..↑n, ↑((1 - x / ↑n) ^ n) * ↑x ^ (s - 1) =
    ∫ (x : ℝ) in Ioc 0 ↑n, ↑((1 - x / ↑n) ^ n) * ↑x ^ (s - 1) ∂volume.restrict (Ioi 0)

Tactic:
intervalIntegral.integral_of_le (by positivity : 0 ≤ (n : ℝ)),

Goal state after:
case e'_3
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 : ℝ) in Ioc 0 ↑n, ↑((1 - x / ↑n) ^ n) * ↑x ^ (s - 1) ∂volume =
    ∫ (x : ℝ) in Ioc 0 ↑n, ↑((1 - x / ↑n) ^ n) * ↑x ^ (s - 1) ∂volume.restrict (Ioi 0)
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta

Goal state before:
pp: case pos
z : ℂ
pi_ne : ↑π ≠ 0
hs : sin (↑π * z) = 0
⊢ Gamma z * Gamma (1 - z) = ↑π / sin (↑π * z)

Tactic:
hs,

Goal state after:
case pos
z : ℂ
pi_ne : ↑π ≠ 0
hs : sin (↑π * z) = 0
⊢ Gamma z * Gamma (1 - z) = ↑π / 0
Module: Mathlib.Analysis.Normed.Affine.Simplex

Goal state before:
pp: case inl
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
hs : s.Scalene
i₁ i₂ i₃ i₄ : Fin (n + 1)
h₁₂ : i₁ ≠ i₂
h₃₄ : i₃ ≠ i₄
h₁₂₃₄ : ¬i₁ = i₃ ∨ ¬i₂ = i₄
h₁₂₄₃ : ¬i₁ = i₄ ∨ ¬i₂ = i₃
h₁₂lt : i₁ < i₂
⊢ dist (s.points i₁) (s.points i₂) ≠ dist (s.points i₃) (s.points i₄)

Tactic:
rcases h₃₄.lt_or_gt with h₃₄lt | h₄₃lt

Goal state after:
case inl.inl
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
hs : s.Scalene
i₁ i₂ i₃ i₄ : Fin (n + 1)
h₁₂ : i₁ ≠ i₂
h₃₄ : i₃ ≠ i₄
h₁₂₃₄ : ¬i₁ = i₃ ∨ ¬i₂ = i₄
h₁₂₄₃ : ¬i₁ = i₄ ∨ ¬i₂ = i₃
h₁₂lt : i₁ < i₂
h₃₄lt : i₃ < i₄
⊢ dist (s.points i₁) (s.points i₂) ≠ dist (s.points i₃) (s.points i₄)

case inl.inr
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
hs : s.Scalene
i₁ i₂ i₃ i₄ : Fin (n + 1)
h₁₂ : i₁ ≠ i₂
h₃₄ : i₃ ≠ i₄
h₁₂₃₄ : ¬i₁ = i₃ ∨ ¬i₂ = i₄
h₁₂₄₃ : ¬i₁ = i₄ ∨ ¬i₂ = i₃
h₁₂lt : i₁ < i₂
h₄₃lt : i₄ < i₃
⊢ dist (s.points i₁) (s.points i₂) ≠ dist (s.points i₃) (s.points i₄)
Module: Mathlib.Analysis.Normed.Affine.Simplex

Goal state before:
pp: case inr
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
hs : s.Scalene
i₁ i₂ i₃ i₄ : Fin (n + 1)
h₁₂ : i₁ ≠ i₂
h₃₄ : i₃ ≠ i₄
h₁₂₃₄ : ¬i₁ = i₃ ∨ ¬i₂ = i₄
h₁₂₄₃ : ¬i₁ = i₄ ∨ ¬i₂ = i₃
h₂₁lt : i₂ < i₁
⊢ dist (s.points i₁) (s.points i₂) ≠ dist (s.points i₃) (s.points i₄)

Tactic:
rcases h₃₄.lt_or_gt with h₃₄lt | h₄₃lt

Goal state after:
case inr.inl
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
hs : s.Scalene
i₁ i₂ i₃ i₄ : Fin (n + 1)
h₁₂ : i₁ ≠ i₂
h₃₄ : i₃ ≠ i₄
h₁₂₃₄ : ¬i₁ = i₃ ∨ ¬i₂ = i₄
h₁₂₄₃ : ¬i₁ = i₄ ∨ ¬i₂ = i₃
h₂₁lt : i₂ < i₁
h₃₄lt : i₃ < i₄
⊢ dist (s.points i₁) (s.points i₂) ≠ dist (s.points i₃) (s.points i₄)

case inr.inr
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
hs : s.Scalene
i₁ i₂ i₃ i₄ : Fin (n + 1)
h₁₂ : i₁ ≠ i₂
h₃₄ : i₃ ≠ i₄
h₁₂₃₄ : ¬i₁ = i₃ ∨ ¬i₂ = i₄
h₁₂₄₃ : ¬i₁ = i₄ ∨ ¬i₂ = i₃
h₂₁lt : i₂ < i₁
h₄₃lt : i₄ < i₃
⊢ dist (s.points i₁) (s.points i₂) ≠ dist (s.points i₃) (s.points i₄)
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta

Goal state before:
pp: case pos.ofNat
z : ℂ
pi_ne : ↑π ≠ 0
a✝ : ℕ
hk : z = -↑(Int.ofNat a✝)
⊢ Gamma (-↑↑a✝) * Gamma (1 - -↑↑a✝) = 0

Tactic:
Int.cast_natCast,

Goal state after:
case pos.ofNat
z : ℂ
pi_ne : ↑π ≠ 0
a✝ : ℕ
hk : z = -↑(Int.ofNat a✝)
⊢ Gamma (-↑a✝) * Gamma (1 - -↑a✝) = 0
Module: Mathlib.Analysis.Normed.Affine.Simplex

Goal state before:
pp: case e'_2
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
m n : ℕ
s : Simplex R P m
e : Fin (m + 1) ≃ Fin (n + 1)
f : { x // x.1 < x.2 } ≃ { y // y.1 < y.2 } :=
  { toFun := fun x ↦ if h : e (↑x).1 < e (↑x).2 then ⟨(e (↑x).1, e (↑x).2), h⟩ else ⟨(e (↑x).2, e (↑x).1), ⋯⟩,
    invFun := fun y ↦
      if h : e.symm (↑y).1 < e.symm (↑y).2 then ⟨(e.symm (↑y).1, e.symm (↑y).2), h⟩
      else ⟨(e.symm (↑y).2, e.symm (↑y).1), ⋯⟩,
    left_inv := ⋯, right_inv := ⋯ }
x✝ : { x // x.1 < x.2 }
⊢ dist (s.points (↑x✝).1) (s.points (↑x✝).2) =
    ((fun i ↦ dist ((s.reindex e).points (↑i).1) ((s.reindex e).points (↑i).2)) ∘ ⇑f) x✝

Tactic:
simp only [reindex_points, comp_apply, Equiv.coe_fn_mk, f]

Goal state after:
case e'_2
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
m n : ℕ
s : Simplex R P m
e : Fin (m + 1) ≃ Fin (n + 1)
f : { x // x.1 < x.2 } ≃ { y // y.1 < y.2 } :=
  { toFun := fun x ↦ if h : e (↑x).1 < e (↑x).2 then ⟨(e (↑x).1, e (↑x).2), h⟩ else ⟨(e (↑x).2, e (↑x).1), ⋯⟩,
    invFun := fun y ↦
      if h : e.symm (↑y).1 < e.symm (↑y).2 then ⟨(e.symm (↑y).1, e.symm (↑y).2), h⟩
      else ⟨(e.symm (↑y).2, e.symm (↑y).1), ⋯⟩,
    left_inv := ⋯, right_inv := ⋯ }
x✝ : { x // x.1 < x.2 }
⊢ dist (s.points (↑x✝).1) (s.points (↑x✝).2) =
    dist
      (s.points
        (e.symm (↑(if h : e (↑x✝).1 < e (↑x✝).2 then ⟨(e (↑x✝).1, e (↑x✝).2), h⟩ else ⟨(e (↑x✝).2, e (↑x✝).1), ⋯⟩)).1))
      (s.points
        (e.symm (↑(if h : e (↑x✝).1 < e (↑x✝).2 then ⟨(e (↑x✝).1, e (↑x✝).2), h⟩ else ⟨(e (↑x✝).2, e (↑x✝).1), ⋯⟩)).2))