mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Geometry.Euclidean.Volume.Measure

Goal state before:
pp: case e_f
V : Type u_3
P : Type u_4
inst✝⁸ : NormedAddCommGroup V
inst✝⁷ : InnerProductSpace ℝ V
inst✝⁶ : MeasurableSpace V
inst✝⁵ : BorelSpace V
inst✝⁴ : FiniteDimensional ℝ V
inst✝³ : MetricSpace P
inst✝² : MeasurableSpace P
inst✝¹ : BorelSpace P
inst✝ : NormedAddTorsor V P
s : AffineSubspace ℝ P
hs : Nonempty ↥s
t : Set P
ht : MeasurableSet t
p : ↥s
x : ↥s.direction
u : Set ↥(mk' (↑(x +ᵥ p)) s.directionᗮ) := Subtype.val ⁻¹' (t ∩ ↑(mk' (↑(x +ᵥ p)) s.directionᗮ))
hu : MeasurableSet u
hinter : t ∩ ↑(mk' (↑(x +ᵥ p)) s.directionᗮ) = Subtype.val '' u
hxp : ↑(x +ᵥ p) ∈ mk' (↑(x +ᵥ p)) s.directionᗮ
hrank : finrank ℝ ↥s.directionᗮ = finrank ℝ ↥(mk' (↑(x +ᵥ p)) s.directionᗮ).direction
⊢ μHE[finrank ℝ ↥s.directionᗮ] (Subtype.val '' Prod.mk x ⁻¹' ⇑(s.direction.measurableEquivProd ↑p).symm ⁻¹' t) =
    μHE[finrank ℝ ↥(mk' (↑(x +ᵥ p)) s.directionᗮ).direction]
      (Subtype.val '' ⇑(IsometryEquiv.vaddConst ⟨↑(x +ᵥ p), hxp⟩) ⁻¹' u)

Tactic:
congrm μHE[$hrank] ?_

Goal state after:
case e_f
V : Type u_3
P : Type u_4
inst✝⁸ : NormedAddCommGroup V
inst✝⁷ : InnerProductSpace ℝ V
inst✝⁶ : MeasurableSpace V
inst✝⁵ : BorelSpace V
inst✝⁴ : FiniteDimensional ℝ V
inst✝³ : MetricSpace P
inst✝² : MeasurableSpace P
inst✝¹ : BorelSpace P
inst✝ : NormedAddTorsor V P
s : AffineSubspace ℝ P
hs : Nonempty ↥s
t : Set P
ht : MeasurableSet t
p : ↥s
x : ↥s.direction
u : Set ↥(mk' (↑(x +ᵥ p)) s.directionᗮ) := Subtype.val ⁻¹' (t ∩ ↑(mk' (↑(x +ᵥ p)) s.directionᗮ))
hu : MeasurableSet u
hinter : t ∩ ↑(mk' (↑(x +ᵥ p)) s.directionᗮ) = Subtype.val '' u
hxp : ↑(x +ᵥ p) ∈ mk' (↑(x +ᵥ p)) s.directionᗮ
hrank : finrank ℝ ↥s.directionᗮ = finrank ℝ ↥(mk' (↑(x +ᵥ p)) s.directionᗮ).direction
⊢ Subtype.val '' Prod.mk x ⁻¹' ⇑(s.direction.measurableEquivProd ↑p).symm ⁻¹' t =
    Subtype.val '' ⇑(IsometryEquiv.vaddConst ⟨↑(x +ᵥ p), hxp⟩) ⁻¹' u
Module: Mathlib.Analysis.InnerProductSpace.OfNorm

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : RCLike 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : E
h₁ : ‖x - x‖ = 0
h₂ : ‖x + x‖ = 2 • ‖x‖
⊢ ‖x‖ ^ 2 =
    4 / (4 * 4 + 0 * 0) *
        (2 • ‖x‖ * 2 • ‖x‖ - 0 * 0 - (0 * 0 - 0 * 0) +
            ((0 * ‖I • x + x‖ - im I * 0) * ‖I • x + x‖ - (0 * 0 + im I * ‖I • x + x‖) * 0) -
          ((0 * ‖I • x - x‖ - im I * 0) * ‖I • x - x‖ - (0 * 0 + im I * ‖I • x - x‖) * 0)) -
      -0 / (4 * 4 + 0 * 0) *
        (2 • ‖x‖ * 0 + 0 * 2 • ‖x‖ - (0 * 0 + 0 * 0) +
            ((0 * ‖I • x + x‖ - im I * 0) * 0 + (0 * 0 + im I * ‖I • x + x‖) * ‖I • x + x‖) -
          ((0 * ‖I • x - x‖ - im I * 0) * 0 + (0 * 0 + im I * ‖I • x - x‖) * ‖I • x - x‖))

Tactic:
ring

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

Goal state before:
pp: case neg
𝕜 : Type u_1
inst✝² : RCLike 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x y : E
hI : ¬I = 0
hI' : I * I = -1
I_smul : ∀ (v : E), ‖I • v‖ = ‖v‖
h₁ : ‖I • y - x‖ = ‖I • x + y‖
h₂ : ‖I • y + x‖ = ‖I • x - y‖
⊢ 4⁻¹ *
      (↑‖x + y‖ * ↑‖x + y‖ - ↑‖x - y‖ * ↑‖x - y‖ + -I * ↑‖I • x - y‖ * ↑‖I • x - y‖ -
        -I * ↑‖I • x + y‖ * ↑‖I • x + y‖) =
    4⁻¹ *
      (𝓚 ‖x + y‖ * 𝓚 ‖x + y‖ - 𝓚 ‖x - y‖ * 𝓚 ‖x - y‖ + I * 𝓚 ‖I • x + y‖ * 𝓚 ‖I • x + y‖ -
        I * 𝓚 ‖I • x - y‖ * 𝓚 ‖I • x - y‖)

Tactic:
ring

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
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)
⊢ TendstoUniformlyOn (fun n ↦ ⇑(F n)) (⇑f) l s

Tactic:
rw [Metric.tendstoUniformlyOn_iff]

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)
⊢ ∀ ε > 0, ∀ᶠ (n : ι) in l, ∀ x ∈ s, dist (f x) ((F n) x) < ε
Module: Mathlib.Analysis.InnerProductSpace.StandardSubspace

Goal state before:
pp: case mp
H : Type u_1
inst✝ : NormedAddCommGroup H
ipc : InnerProductSpace ℂ H
S : ClosedSubmodule ℝ H
x : H
h : ∀ (a : ℝ), a • (scalarSMulCLE H UnitI).symm x ∈ S.mulI
⊢ x ∈ S

Tactic:
simpa [← smul_assoc, Units.smul_def] using (h (-1 : ℝ))

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

Goal state before:
pp: case mpr
H : Type u_1
inst✝ : NormedAddCommGroup H
ipc : InnerProductSpace ℂ H
S : ClosedSubmodule ℝ H
x : H
h : ∀ (a : ℝ), a • x ∈ S
⊢ x ∈ S.mulI.mulI

Tactic:
simpa [← smul_assoc, Units.smul_def] using (h (-1 : ℝ))

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝³ : RCLike 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : InnerProductSpaceable E
r : 𝕜
x y : E
⊢ ↑(re r) * inner_ 𝕜 x y + ↑(im r) * (-I * inner_ 𝕜 x y) = (↑(re r) + ↑(im r) * -I) * inner_ 𝕜 x y

Tactic:
ring

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

Goal state before:
pp: case inr
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
C r : ℝ≥0
f : X → Y
s : Set X
h : HolderOnWith C r f s
hr : 0 < r
d : ℝ
hd : 0 ≤ d
hC0 : 0 < C
⊢ μH[d] (f '' s) ≤ ↑C ^ d * μH[↑r * d] s

Tactic:
· have hCd0 : (C : ℝ≥0∞) ^ d ≠ 0 := by simp [hC0.ne']
    have hCd : (C : ℝ≥0∞) ^ d ≠ ∞ := by simp [hd]
    simp only [hausdorffMeasure_apply, ENNReal.mul_iSup, ENNReal.mul_iInf_of_ne hCd0 hCd,
      ← ENNReal.tsum_mul_left]
    refine iSup_le fun R => iSup_le fun hR => ?_
    have : Tendsto (fun d : ℝ≥0∞ => (C : ℝ≥0∞) * d ^ (r : ℝ)) (𝓝 0) (𝓝 0) :=
      ENNReal.tendsto_const_mul_rpow_nhds_zero_of_pos ENNReal.coe_ne_top hr
    rcases ENNReal.nhds_zero_basis_Iic.eventually_iff.1 (this.eventually (gt_mem_nhds hR)) with
      ⟨δ, δ0, H⟩
    refine le_iSup₂_of_le δ δ0 <| iInf₂_mono' fun t hst ↦
      ⟨fun n => f '' (t n ∩ s), ?_, iInf_mono' fun htδ ↦
        ⟨fun n => (h.ediam_image_inter_le (t n)).trans (H (htδ n)).le, ?_⟩⟩
    · grw [← image_iUnion, ← iUnion_inter, ← hst, inter_self]
    · refine ENNReal.tsum_le_tsum fun n => ?_
      simp only [iSup_le_iff, image_nonempty]
      intro hft
      simp only [Nonempty.mono ((t n).inter_subset_left) hft, ciSup_pos]
      rw [ENNReal.rpow_mul, ← ENNReal.mul_rpow_of_nonneg _ _ hd]
      gcongr
      exact h.ediam_image_inter_le _

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

Goal state before:
pp: 𝕜 : Type u_4
E : Type u_5
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedDivisionRing 𝕜
inst✝³ : Module 𝕜 E
inst✝² : NormSMulClass 𝕜 E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
d : ℝ
hd : 0 ≤ d
r : 𝕜
hr : r ≠ 0
s : Set E
this : ∀ {r : 𝕜} (s : Set E), μH[d] (r • s) ≤ ‖r‖₊ ^ d • μH[d] s
⊢ μH[d] s ≤ ↑(‖r‖₊ ^ d)⁻¹ * μH[d] (r • s)

Tactic:
rw [← NNReal.inv_rpow, ← nnnorm_inv]

Goal state after:
𝕜 : Type u_4
E : Type u_5
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedDivisionRing 𝕜
inst✝³ : Module 𝕜 E
inst✝² : NormSMulClass 𝕜 E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
d : ℝ
hd : 0 ≤ d
r : 𝕜
hr : r ≠ 0
s : Set E
this : ∀ {r : 𝕜} (s : Set E), μH[d] (r • s) ≤ ‖r‖₊ ^ d • μH[d] s
⊢ μH[d] s ≤ ↑(‖r⁻¹‖₊ ^ d) * μH[d] (r • s)
Module: Mathlib.MeasureTheory.Measure.Hausdorff

Goal state before:
pp: ι : Type u_4
inst✝ : Fintype ι
s : ι → Set ℝ
hs : ∀ (i : ι), ∃ i_1 i_2, ∃ (_ : i_1 < i_2), s i = Ioo ↑i_1 ↑i_2
⊢ μH[↑(Fintype.card ι)] (univ.pi s) = ∏ x, volume (s x)

Tactic:
choose a b H using hs

Goal state after:
ι : Type u_4
inst✝ : Fintype ι
s : ι → Set ℝ
a b : ι → ℚ
H : ∀ (i : ι), ∃ (_ : a i < b i), s i = Ioo ↑(a i) ↑(b i)
⊢ μH[↑(Fintype.card ι)] (univ.pi s) = ∏ x, volume (s x)
Module: Mathlib.Analysis.LocallyConvex.Montel

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✝¹⁰ : Module 𝕜₁ E
inst✝⁹ : TopologicalSpace E
inst✝⁸ : IsTopologicalAddGroup E
inst✝⁷ : ContinuousSMul 𝕜₁ E
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module 𝕜₂ F
inst✝⁴ : TopologicalSpace F
inst✝³ : IsTopologicalAddGroup F
inst✝² : ContinuousSMul 𝕜₂ F
inst✝¹ : T1Space E
inst✝ : MontelSpace 𝕜₁ E
⊢ ContinuousAt (⇑(LinearEquiv.toCompactConvergenceCLM σ E F).symm) 0

Tactic:
rw [ContinuousAt, _root_.map_zero, CompactConvergenceCLM.hasBasis_nhds_zero.tendsto_iff
      ContinuousLinearMap.hasBasis_nhds_zero]

Goal state after:
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst✝¹³ : NormedField 𝕜₁
inst✝¹² : NormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
E : Type u_3
F : Type u_4
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : Module 𝕜₁ E
inst✝⁹ : TopologicalSpace E
inst✝⁸ : IsTopologicalAddGroup E
inst✝⁷ : ContinuousSMul 𝕜₁ E
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module 𝕜₂ F
inst✝⁴ : TopologicalSpace F
inst✝³ : IsTopologicalAddGroup F
inst✝² : ContinuousSMul 𝕜₂ F
inst✝¹ : T1Space E
inst✝ : MontelSpace 𝕜₁ E
⊢ ∀ (ib : Set E × Set F),
    IsVonNBounded 𝕜₁ ib.1 ∧ ib.2 ∈ 𝓝 0 →
      ∃ ia,
        (IsCompact ia.1 ∧ ia.2 ∈ 𝓝 0) ∧
          ∀ x ∈ {f | ∀ x ∈ ia.1, f x ∈ ia.2},
            (LinearEquiv.toCompactConvergenceCLM σ E F).symm x ∈ {f | ∀ x ∈ ib.1, f x ∈ ib.2}
Module: Mathlib.Analysis.InnerProductSpace.TwoDim

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

Tactic:
rcases eq_or_lt_of_le (norm_nonneg (o.rightAngleRotationAux₁ x)) with h | h
        · rw [← h]
          positivity
        refine le_of_mul_le_mul_right ?_ h
        rw [← real_inner_self_eq_norm_mul_norm, o.inner_rightAngleRotationAux₁_left]
        exact o.areaForm_le x (o.rightAngleRotationAux₁ x)

Goal state after:
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)
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
hF : Fact (finrank ℝ F = 2)
φ : E ≃ₗᵢ[ℝ] F
x y : F
⊢ ⟪o.rightAngleRotation (φ.symm x), φ.symm y⟫ = ⟪φ (o.rightAngleRotation (φ.symm x)), φ (φ.symm y)⟫

Tactic:
rw [φ.inner_map_map]

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

Goal state before:
pp: w z : ℂ
o : Orientation ℝ ℂ (Fin 2) := Complex.orientation
⊢ w.re * z.im - z.re * w.im = w.re * z.im + -w.im * z.re

Tactic:
ring

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

Goal state before:
pp: z w : ℂ
⊢ ⟪Complex.orientation.rightAngleRotation z, w⟫ = ⟪I * z, w⟫

Tactic:
Orientation.inner_rightAngleRotation_left

Goal state after:
z w : ℂ
⊢ (Complex.orientation.areaForm z) w = ⟪I * z, w⟫
Module: Mathlib.Analysis.InnerProductSpace.TwoDim

Goal state before:
pp: z w : ℂ
⊢ z.re * w.im + -z.im * w.re = w.re * (-0 * z.re - -1 * -z.im) - w.im * (-0 * -z.im + -1 * z.re)

Tactic:
ring

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 : 0 < a
t : ℝ
ht : t ∈ Ioi 0
⊢ 1 - s = -(s - 1)

Tactic:
ring

Goal state after:
Module: Mathlib.Analysis.MellinTransform

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f g : ℝ → E
s : ℂ
hf : MellinConvergent f s
hg : MellinConvergent g s
⊢ MellinConvergent (fun t ↦ f t + g t) s

Tactic:
by simpa only [MellinConvergent, smul_add] using! hf.add hg

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

Goal state before:
pp: case e'_9
z : ℂ
n : ℕ
ih : HasDerivAt (logTaylor (n + 1)) (∑ j ∈ Finset.range n, (-1) ^ j * z ^ j) z
this : HasDerivAt (fun x ↦ x ^ (n + 1) / (↑n + 1)) (z ^ n) z
⊢ (-1) ^ n = (-1) ^ (n + 1 + 1)

Tactic:
ring

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

Goal state before:
pp: t : ℝ
ht : 0 ≤ t ∧ t ≤ 1
z : ℂ
hz : ‖z‖ < 1
⊢ 1 - t * ‖z‖ = 1 - ‖↑t‖ * ‖z‖

Tactic:
Complex.norm_of_nonneg ht.1

Goal state after:
t : ℝ
ht : 0 ≤ t ∧ t ≤ 1
z : ℂ
hz : ‖z‖ < 1
⊢ 1 - t * ‖z‖ = 1 - t * ‖z‖
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.Trigonometric.EulerSineProd

Goal state before:
pp: case e'_9
z : ℂ
n : ℕ
hn : 2 ≤ n
hz : z ≠ 0
x : ℝ
a✝ : x ∈ uIcc 0 (π / 2)
b : HasDerivAt (fun y ↦ ↑(cos y)) (-↑(sin x)) x
⊢ -↑n * ↑(sin x) * ↑(cos x) ^ (n - 1) = ↑n * ↑(cos x) ^ (n - 1) * -↑(sin x)

Tactic:
ring

Goal state after:
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 ↦ ↑(cos y) ^ n) (-↑n * ↑(sin x) * ↑(cos x) ^ (n - 1)) x
x : ℝ
x✝ : x ∈ uIcc 0 (π / 2)
⊢ ↑n / (2 * z) * (Complex.sin (2 * z * ↑x) * ↑(sin x) * ↑(cos x) ^ (n - 1)) =
    -(-↑n * ↑(sin x) * ↑(cos x) ^ (n - 1) * (Complex.sin (2 * z * ↑x) / (2 * z)))

Tactic:
ring

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

Goal state before:
pp: z : ℂ
hz : ‖z‖ < 1
| Tendsto (fun x ↦ ∑ i ∈ Finset.range x, (-1) ^ (i + 1) * z ^ i / ↑i - log (1 + z)) atTop (nhds 0)

Tactic:
enter [1, x]; rw [← div_one (_ - _), ← logTaylor]

Goal state after:
z : ℂ
hz : ‖z‖ < 1
x : ℕ
| (logTaylor x z - log (1 + z)) / 1
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd

Goal state before:
pp: case e'_9.e_a
z : ℂ
n : ℕ
hn : 2 ≤ n
hz : z ≠ 0
x : ℝ
a✝ : x ∈ uIcc 0 (π / 2)
c : HasDerivAt ((fun x ↦ x ^ (n - 1)) ∘ Complex.cos) (↑(n - 1) * Complex.cos ↑x ^ (n - 1 - 1) * -Complex.sin ↑x) ↑x
this : ↑(n - 1) = ↑n - 1
⊢ (↑n - 1) * Complex.sin ↑x ^ 2 * Complex.cos ↑x ^ (n - 2) =
    Complex.sin ↑x * ((↑n - 1) * Complex.cos ↑x ^ (n - (1 + 1)) * Complex.sin ↑x)

Tactic:
ring

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
hst : 0 < a * s + b * t
posf : ∀ (c u x : ℝ), x ∈ Ioi 0 → 0 ≤ f c u x
posf' : ∀ (c u : ℝ), ∀ᵐ (x : ℝ) ∂volume.restrict (Ioi 0), 0 ≤ f c u x
fpow : ∀ {c x : ℝ}, 0 < c → ∀ (u : ℝ), 0 < x → rexp (-x) * x ^ (u - 1) = f c u x ^ (1 / c)
f_mem_Lp : ∀ {c u : ℝ}, 0 < c → 0 < u → MemLp (f c u) (ENNReal.ofReal (1 / c)) (volume.restrict (Ioi 0))
x : ℝ
hx : x ∈ Ioi 0
⊢ rexp (-x) = rexp (-a * x) * rexp (-b * x)

Tactic:
← exp_add,

Goal state after:
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
hst : 0 < a * s + b * t
posf : ∀ (c u x : ℝ), x ∈ Ioi 0 → 0 ≤ f c u x
posf' : ∀ (c u : ℝ), ∀ᵐ (x : ℝ) ∂volume.restrict (Ioi 0), 0 ≤ f c u x
fpow : ∀ {c x : ℝ}, 0 < c → ∀ (u : ℝ), 0 < x → rexp (-x) * x ^ (u - 1) = f c u x ^ (1 / c)
f_mem_Lp : ∀ {c u : ℝ}, 0 < c → 0 < u → MemLp (f c u) (ENNReal.ofReal (1 / c)) (volume.restrict (Ioi 0))
x : ℝ
hx : x ∈ Ioi 0
⊢ rexp (-x) = rexp (-a * x + -b * x)
Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup

Goal state before:
pp: case e_a
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
hst : 0 < a * s + b * t
posf : ∀ (c u x : ℝ), x ∈ Ioi 0 → 0 ≤ f c u x
posf' : ∀ (c u : ℝ), ∀ᵐ (x : ℝ) ∂volume.restrict (Ioi 0), 0 ≤ f c u x
fpow : ∀ {c x : ℝ}, 0 < c → ∀ (u : ℝ), 0 < x → rexp (-x) * x ^ (u - 1) = f c u x ^ (1 / c)
f_mem_Lp : ∀ {c u : ℝ}, 0 < c → 0 < u → MemLp (f c u) (ENNReal.ofReal (1 / c)) (volume.restrict (Ioi 0))
x : ℝ
hx : x ∈ Ioi 0
A : rexp (-x) = rexp (-a * x) * rexp (-b * x)
⊢ a * s + (1 - a) * t - 1 = a * (s - 1) + (1 - a) * (t - 1)

Tactic:
ring

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

Goal state before:
pp: g : ℝ → ℂ
t : ℂ
hg : Tendsto (fun x ↦ ↑x * g x) atTop (𝓝 t)
x : ℝ
hx0 : x ≠ 0
⊢ ↑x * g x ^ 2 * ↑x = (↑x * g x) ^ 2

Tactic:
ring

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

Goal state before:
pp: case e'_3
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
hst : 0 < a * s + b * t
posf : ∀ (c u x : ℝ), x ∈ Ioi 0 → 0 ≤ f c u x
posf' : ∀ (c u : ℝ), ∀ᵐ (x : ℝ) ∂volume.restrict (Ioi 0), 0 ≤ f c u x
fpow : ∀ {c x : ℝ}, 0 < c → ∀ (u : ℝ), 0 < x → rexp (-x) * x ^ (u - 1) = f c u x ^ (1 / c)
f_mem_Lp : ∀ {c u : ℝ}, 0 < c → 0 < u → MemLp (f c u) (ENNReal.ofReal (1 / c)) (volume.restrict (Ioi 0))
x : ℝ
hx : x ∈ Ioi 0
A : rexp (-x) = rexp (-a * x) * rexp (-b * x)
B : x ^ (a * s + b * t - 1) = x ^ (a * (s - 1)) * x ^ (b * (t - 1))
⊢ rexp (-a * x) * rexp (-b * x) * (x ^ (a * (s - 1)) * x ^ (b * (t - 1))) = f a s x * f b t x

Tactic:
ring

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

Goal state before:
pp: f : ℕ → ℂ
t : ℂ
hf : (fun n ↦ f n - (1 + t / ↑n)) =o[atTop] fun n ↦ 1 / ↑n
n : ℕ
h0 : n ≠ 0
⊢ ↑n * f n - (↑n + t) = ↑n * (f n - 1) - t

Tactic:
ring

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

Goal state before:
pp: case e'_3.e_a
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
x : ℝ
x✝ : x ∈ uIcc 0 (π / 2)
this : Complex.cos ↑x ^ n = Complex.cos ↑x ^ (n - 2) * Complex.cos ↑x ^ 2
⊢ ↑n * (Complex.cos (2 * z * ↑x) * (Complex.cos ↑x ^ (n - 2) * Complex.cos ↑x ^ 2)) -
      (↑n - 1) * (Complex.cos (2 * z * ↑x) * Complex.cos ↑x ^ (n - 2)) =
    -((Complex.cos ↑x ^ (n - 2) * Complex.cos ↑x ^ 2 - (↑n - 1) * (1 - Complex.cos ↑x ^ 2) * Complex.cos ↑x ^ (n - 2)) *
        -Complex.cos (2 * z * ↑x))

Tactic:
ring

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

Goal state before:
pp: u v : ℂ
hu : 0 < u.re
hv : 0 < v.re
⊢ IntervalIntegrable (fun x ↦ ↑x ^ (u - 1) * (1 - ↑x) ^ (v - 1)) volume 0 1

Tactic:
refine (betaIntegral_convergent_left hu v).trans ?_

Goal state after:
u v : ℂ
hu : 0 < u.re
hv : 0 < v.re
⊢ IntervalIntegrable (fun x ↦ ↑x ^ (u - 1) * (1 - ↑x) ^ (v - 1)) volume (1 / 2) 1
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta

Goal state before:
pp: case e'_4.e_a.e_a
u v : ℂ
hu : 0 < u.re
hv : 0 < v.re
x : ℝ
⊢ 1 - -↑x = ↑x + 1

Tactic:
ring

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

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

Tactic:
ring

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

Goal state before:
pp: case e'_2
z : ℂ
n : ℕ
hz : z ≠ 0
⊢ z ^ 2 / (↑n + 1) ^ 2 = 4 * z ^ 2 / 2 ^ 2 / (↑n + 1) ^ 2

Tactic:
ring

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

Goal state before:
pp: case e'_3.e'_5.e'_5
z : ℂ
n : ℕ
hz : z ≠ 0
⊢ 2 * ↑n + 1 = 2 * ↑n + 2 - 1

Tactic:
ring

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

Goal state before:
pp: case e'_3.e'_5.e'_6
z : ℂ
n : ℕ
hz : z ≠ 0
⊢ 2 * ↑n + 2 = 2 * ↑n + 2

Tactic:
ring

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

Goal state before:
pp: f : ℝ → ℝ
x : ℝ
hf_feq : ∀ {y : ℝ}, 0 < y → f (y + 1) = f y + log y
hx : 0 < x
n : ℕ
hn : f (x + ↑n) = f x + ∑ m ∈ Finset.range n, log (x + ↑m)
⊢ x + (↑n + 1) = x + ↑n + 1

Tactic:
ring

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

Goal state before:
pp: n : ℕ
L : IntervalIntegrable (fun i ↦ sin i ^ n) volume 0 (π / 2)
R : IntervalIntegrable (fun i ↦ sin i ^ n) volume (π / 2) π
⊢ 0 = π / 2 - π / 2

Tactic:
ring

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

Goal state before:
pp: n : ℕ
L : IntervalIntegrable (fun i ↦ sin i ^ n) volume 0 (π / 2)
R : IntervalIntegrable (fun i ↦ sin i ^ n) volume (π / 2) π
⊢ π / 2 = π / 2 - 0

Tactic:
ring

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

Goal state before:
pp: n : ℕ
L : IntervalIntegrable (fun i ↦ sin i ^ n) volume 0 (π / 2)
R : IntervalIntegrable (fun i ↦ sin i ^ n) volume (π / 2) π
⊢ π = π / 2 + π / 2

Tactic:
ring

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

Goal state before:
pp: n : ℕ
L : IntervalIntegrable (fun i ↦ sin i ^ n) volume 0 (π / 2)
R : IntervalIntegrable (fun i ↦ sin i ^ n) volume (π / 2) π
⊢ π / 2 = 0 + π / 2

Tactic:
ring

Goal state after:
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 : n ≠ 0
hx : 0 < x
hx' : x ≤ 1
hn' : 0 < ↑n
⊢ f ↑n + x * log ↑n = (1 - x) * f ↑n + x * (f ↑n + log ↑n)

Tactic:
ring

Goal state after:
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 : n ≠ 0
hx : 0 < x
hx' : x ≤ 1
hn' : 0 < ↑n
this : f ↑n + x * log ↑n = (1 - x) * f ↑n + x * f (↑n + 1)
⊢ ↑n + x = (1 - x) * ↑n + x * (↑n + 1)

Tactic:
ring

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

Goal state before:
pp: z : ℂ
hz : z ≠ 0
⊢ 2 * z * (↑π / 2) = ↑π * z

Tactic:
ring

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 : ℝ
hx : x ∈ Ioi 0
y : ℝ
this : cexp (-↑x) = cexp (-↑y) * cexp (-(↑x - ↑y))
⊢ cexp (-↑y) * ↑y ^ (s - 1) * (cexp (-(↑x - ↑y)) * (↑x - ↑y) ^ (t - 1)) =
    cexp (-↑y) * cexp (-(↑x - ↑y)) * (↑y ^ (s - 1) * (↑x - ↑y) ^ (t - 1))

Tactic:
ring

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

Goal state before:
pp: x : ℝ
n : ℕ
this : ∑ m ∈ Finset.range (n + 1), log (x + 1 + ↑m) = ∑ k ∈ Finset.range (n + 1), log (x + ↑(k + 1))
⊢ (x + 1) * log ↑n + log ↑n ! - ∑ m ∈ Finset.range (n + 1), log (x + 1 + ↑m) =
    x * log (↑n + 1) + (log (↑n + 1) + log ↑n !) - (∑ m ∈ Finset.range (n + 1), log (x + 1 + ↑m) + log x) + log x -
      (x + 1) * (log (↑n + 1) - log ↑n)

Tactic:
ring

Goal state after:
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 : ℕ
⊢ f 1 + log ↑n ! + x * log (↑n + 1) = f 1 + x * log (↑n + 1) - x * log ↑n + (x * log ↑n + log ↑n !)

Tactic:
ring

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

Goal state before:
pp: case refine_1
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
⊢ f 1 + (x * log ↑n + log ↑n !) = f 1 + log ↑n ! + x * log ↑n

Tactic:
ring

Goal state after: