mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Measure.Hausdorff

Goal state before:
pp: ι : Type u_1
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
E : Type u_4
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
U : Set E
hU : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U
hU' : U.Nonempty
⊢ finrank ℝ E = finrank ℝ (Fin (finrank ℝ E) → ℝ)

Tactic:
simp

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

Goal state before:
pp: ι : Type u_1
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
E : Type u_4
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
U : Set E
hU : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U
hU' : U.Nonempty
e : E ≃L[ℝ] Fin (finrank ℝ E) → ℝ := ContinuousLinearEquiv.ofFinrankEq ⋯
this : 0 < μH[↑(finrank ℝ E)] (⇑e '' U)
⊢ 0 ≤ ↑(finrank ℝ E)

Tactic:
simp

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

Goal state before:
pp: case inl.inl
E : Type u_5
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
this : NullSingletonClass μH[1]
⊢ μH[1] ((fun r ↦ r • 0) '' ∅) = ‖0‖₊ • μH[1] ∅

Tactic:
simp

Goal state after:
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
⊢ ![x, x] 0 = ![x, x] 1

Tactic:
simp

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

Goal state before:
pp: case refine_2
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x : E
⊢ 0 ≠ 1

Tactic:
simp

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)
x y : E
⊢ 0 ≠ 1

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
R : Type u_2
𝕜₁ : Type u_3
𝕜₂ : Type u_4
𝕜₃ : Type u_5
inst✝⁷ : NormedField 𝕜₁
inst✝⁶ : NormedField 𝕜₂
inst✝⁵ : NormedField 𝕜₃
σ : 𝕜₁ →+* 𝕜₂
τ : 𝕜₃ →+* 𝕜₂
D : Type u_6
E : Type u_7
F : Type u_8
G : Type u_9
inst✝⁴ : AddCommGroup E
inst✝³ : TopologicalSpace E
inst✝² : Module 𝕜₁ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜₂ F
x : E
⊢ ‖0 x‖ = 0

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
R : Type u_2
𝕜₁ : Type u_3
𝕜₂ : Type u_4
𝕜₃ : Type u_5
inst✝⁷ : NormedField 𝕜₁
inst✝⁶ : NormedField 𝕜₂
inst✝⁵ : NormedField 𝕜₃
σ : 𝕜₁ →+* 𝕜₂
τ : 𝕜₃ →+* 𝕜₂
D : Type u_6
E : Type u_7
F : Type u_8
G : Type u_9
inst✝⁴ : AddCommGroup E
inst✝³ : TopologicalSpace E
inst✝² : Module 𝕜₁ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜₂ F
x : E
A : E →SLₚₜ[σ] F
⊢ ‖(-A) x‖ = ‖A x‖

Tactic:
simp

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

Goal state before:
pp: case e'_3.e'_5
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
φ : E ≃ₗᵢ[ℝ] E
hφ : 0 < LinearMap.det ↑φ.toLinearEquiv
x y : E
⊢ x = φ.symm (φ x)

Tactic:
simp

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

Goal state before:
pp: case e'_3.e'_6
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
φ : E ≃ₗᵢ[ℝ] E
hφ : 0 < LinearMap.det ↑φ.toLinearEquiv
x y : E
⊢ y = φ.symm (φ y)

Tactic:
simp

Goal state after:
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‖

pp: case refine_2
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x : E
⊢ ‖x‖ ≤ ‖o.rightAngleRotationAux₁ 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:
case refine_2
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x : E
⊢ ‖x‖ ≤ ‖o.rightAngleRotationAux₁ x‖
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 : E
⊢ ⟪o.rightAngleRotation x, x⟫ = 0

Tactic:
simp

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)
x y : E
⊢ ⟪x, o.rightAngleRotation y⟫ = -⟪o.rightAngleRotation x, y⟫

Tactic:
simp

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)
x y : E
⊢ (o.areaForm (o.rightAngleRotation x)) (o.rightAngleRotation y) = (o.areaForm x) y

Tactic:
simp

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)
x✝ : E
⊢ (o.rightAngleRotation.trans o.rightAngleRotation) x✝ = (LinearIsometryEquiv.neg ℝ) x✝

Tactic:
simp

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)
x y : E
⊢ ((-o).areaForm x) y = ⟪-o.rightAngleRotation x, y⟫

Tactic:
simp

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)), y⟫

Tactic:
simp

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

Goal state before:
pp: case e'_2
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
φ : E ≃ₗᵢ[ℝ] E
hφ : 0 < LinearMap.det ↑φ.toLinearEquiv
x : E
⊢ x = φ.symm (φ x)

Tactic:
simp

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
x y : E →SWOT[σ] F
x✝ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ (match x✝ with
    | (x_1, y_1) => y_1 ((x + y) x_1)) =
    ((fun x_1 ↦
          match x_1 with
          | (x_2, y) => y (x x_2)) +
        fun x ↦
        match x with
        | (x, y_1) => y_1 (y x))
      x✝

Tactic:
simp

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
x : 𝕜₂
y : E →SWOT[σ] F
x✝ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ (match x✝ with
    | (x_1, y_1) => y_1 ((x • y) x_1)) =
    ((RingHom.id 𝕜₂) x • fun x ↦
        match x with
        | (x, y_1) => y_1 (y x))
      x✝

Tactic:
simp

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
x : E
y : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ ‖y (0 x)‖ = 0

Tactic:
simp

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
x : E
y : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
A : E →SWOT[σ] F
⊢ ‖y ((-A) x)‖ = ‖y (A x)‖

Tactic:
simp

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
x : E
y : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
r : 𝕜₂
A : E →SWOT[σ] F
⊢ ‖y ((r • A) x)‖ = ‖r‖ * ‖y (A x)‖

Tactic:
simp

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝¹⁶ : RCLike 𝕜
inst✝¹⁵ : AddCommGroup E
inst✝¹⁴ : Module 𝕜 E
inst✝¹³ : AddCommGroup F
inst✝¹² : Module 𝕜 F
inst✝¹¹ : Module ℝ E
inst✝¹⁰ : IsScalarTower ℝ 𝕜 E
inst✝⁹ : Module ℝ F
inst✝⁸ : IsScalarTower ℝ 𝕜 F
inst✝⁷ : TopologicalSpace E
inst✝⁶ : IsTopologicalAddGroup E
inst✝⁵ : ContinuousSMul 𝕜 E
inst✝⁴ : LocallyConvexSpace ℝ E
inst✝³ : TopologicalSpace F
inst✝² : IsTopologicalAddGroup F
inst✝¹ : ContinuousSMul 𝕜 F
inst✝ : LocallyConvexSpace ℝ F
s : Set E
hs : Convex ℝ s
e : E ≃ₗ[𝕜] F
e_dual : StrongDual 𝕜 F ≃ StrongDual 𝕜 E
f : StrongDual 𝕜 E
he : ∀ (f : StrongDual 𝕜 F), ⇑(e_dual f) = ⇑(e.dualMap ↑f)
this : ∀ (g : StrongDual 𝕜 E), ⇑g = ⇑(e_dual.symm g) ∘ ⇑e
x : F
⊢ (e_dual.symm f) x = (⇑(e_dual.symm f) ∘ ⇑e) (e.symm x)

Tactic:
simp

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)
y : E
⊢ (o.kahler 0) y = 0

Tactic:
simp

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

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

Tactic:
simp

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)
y : E
⊢ ↑⟪0, y⟫ + ↑((o.areaForm 0) y) * Complex.I = 0

Tactic:
simp

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

Goal state before:
pp: case inr
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x : E
⊢ ↑⟪x, 0⟫ + ↑((o.areaForm x) 0) * Complex.I = 0

Tactic:
simp

Goal state after:
Module: Mathlib.Analysis.MellinInversion

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
x : ℝ
s : ℂ
f : E
⊢ (cexp (-↑x) * cexp (-↑x) ^ (s - 1)) • f = cexp (-s * ↑x) • f

Tactic:
conv in cexp _ * _ => lhs; rw [← cpow_one (cexp _)]

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
x : ℝ
s : ℂ
f : E
⊢ (cexp (-↑x) ^ 1 * cexp (-↑x) ^ (s - 1)) • f = cexp (-s * ↑x) • f
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
hFf : VerticalIntegrable (mellin f) σ volume
hfx : ContinuousAt f x
g : ℝ → E := fun u ↦ rexp (-σ * u) • f (rexp (-u))
hf : Integrable g volume
⊢ 2 * π ≠ 0

Tactic:
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
hfx : ContinuousAt f x
g : ℝ → E := fun u ↦ rexp (-σ * u) • f (rexp (-u))
hf : Integrable g volume
hFf : Integrable (𝓕 g) volume
⊢ mellinInv σ (mellin f) x = f x

Tactic:
replace hfx : ContinuousAt g (-Real.log x) := by
    refine ContinuousAt.fun_smul (by fun_prop) (ContinuousAt.comp ?_ (by fun_prop))
    simpa [Real.exp_log hx] using hfx

Goal state after:
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)
⊢ mellinInv σ (mellin f) x = f x
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)
⊢ 2 * π ≠ 0

Tactic:
simp

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

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

Tactic:
simp

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

Goal state before:
pp: case succ
s✝ : ℂ
hs✝ : ∀ (m : ℕ), s✝ ≠ -↑m
n : ℕ
s : ℂ
IH : DifferentiableAt ℂ Gamma (s + 1)
hsre : -↑(n + 1) < s.re
hs : ∀ (m : ℕ), s ≠ -↑m
hsne : s ≠ 0
this : DifferentiableAt ℂ (Gamma ∘ fun s ↦ s + 1) s
⊢ Gamma =ᶠ[𝓝 s] fun i ↦ (Gamma ∘ fun s ↦ s + 1) i / id i

Tactic:
filter_upwards [isOpen_ne.mem_nhds hsne] using by grind

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

Goal state before:
pp: ⊢ ∀ (m : ℕ), ¬(False ∧ m = 0)

Tactic:
simp

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

Goal state before:
pp: ⊢ Disjoint (𝓝 1) (𝓝 (0 * Gamma 0))

Tactic:
simp

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

Goal state before:
pp: n : ℕ
⊢ 0 < 1 / 2

Tactic:
simp

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

Goal state before:
pp: case refine_1.inl
z : ℂ
hz : ‖z‖ < 1
⊢ ‖z‖ ^ 0 / ↑0 ≤ ‖z‖ ^ 0

Tactic:
simp

Goal state after:
Module: Mathlib.Analysis.MellinTransform

Goal state before:
pp: case refine_1
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a b : ℝ
f : ℝ → E
hab : a < b
hf : f =O[𝓝[>] 0] fun x ↦ x ^ (-a)
t : ℝ
⊢ ((fun x ↦ -log x) ∘ fun x ↦ x⁻¹) t = log t

Tactic:
simp

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

Goal state before:
pp: z : ℂ
hz : ‖z‖ < 1
this : ∀ (n : ℕ), ‖logTaylor n z - log (1 + z)‖ ≤ max ‖log (1 + z)‖ (1 - ‖z‖)⁻¹ * ‖‖z‖ ^ n‖
⊢ (fun n ↦ logTaylor n z - log (1 + z)) =O[atTop] fun n ↦ ‖z‖ ^ n

Tactic:
exact (isBigOWith_of_le' atTop this).isBigO

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

Goal state before:
pp: case e'_5.inl
z : ℂ
hz : ‖z‖ < 1
⊢ -(z ^ 0 / ↑0) = (-1) ^ (0 + 1) * (-z) ^ 0 / ↑0

Tactic:
simp

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

Goal state before:
pp: g : ℝ → ℂ
t : ℂ
hg : Tendsto (fun x ↦ ↑x * g x) atTop (𝓝 t)
hg0 : Tendsto g atTop (𝓝 0)
⊢ 0 ≠ -1

Tactic:
simp

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

Goal state before:
pp: g : ℕ → ℂ
t : ℂ
hg : Tendsto (fun n ↦ ↑n * g n) atTop (𝓝 t)
⊢ ∀ (x : ℕ), ((fun x ↦ ↑x * log (1 + g ⌊x⌋₊)) ∘ Nat.cast) x = ↑x * log (1 + g x)

Tactic:
simp

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

Goal state before:
pp: g : ℕ → ℂ
t : ℂ
hg : Tendsto (fun n ↦ ↑n * g n) atTop (𝓝 t)
⊢ ∀ (x : ℕ), ((fun x ↦ (1 + g ⌊x⌋₊) ^ ↑x) ∘ Nat.cast) x = (1 + g x) ^ x

Tactic:
simp

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

Goal state before:
pp: t : ℂ
⊢ ∀ (x : ℕ), ((fun x ↦ (1 + t / ↑x) ^ ↑x) ∘ Nat.cast) x = (1 + t / ↑x) ^ x

Tactic:
simp

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
x✝ : ℕ
⊢ f x✝ ^ x✝ = (1 + (f x✝ - 1)) ^ x✝

Tactic:
simp

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
⊢ (1 / ↑n)⁻¹ • (f n - (1 + t / ↑n)) = ↑n * (f n - 1) - t

Tactic:
simp

Goal state after:
f : ℕ → ℂ
t : ℂ
hf : (fun n ↦ f n - (1 + t / ↑n)) =o[atTop] fun n ↦ 1 / ↑n
n : ℕ
h0 : n ≠ 0
⊢ ↑n * (f n - (1 + t / ↑n)) = ↑n * (f n - 1) - t
Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds

Goal state before:
pp: g : ℝ → ℝ
t : ℝ
hg : Tendsto (fun x ↦ x * g x) atTop (𝓝 t)
⊢ atTop ≤ Bornology.cobounded ℝ

Tactic:
simp

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 ↦ x * log (1 + g x)) atTop (𝓝 t)

Tactic:
have hg0 := tendsto_zero_of_isBoundedUnder_smul_of_tendsto_cobounded
    hg.norm.isBoundedUnder_le (tendsto_id'.mpr (by simp))

Goal state after:
g : ℝ → ℝ
t : ℝ
hg : Tendsto (fun x ↦ x * g x) atTop (𝓝 t)
hg0 : Tendsto g atTop (𝓝 0)
⊢ Tendsto (fun x ↦ x * log (1 + g x)) atTop (𝓝 t)
Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds

Goal state before:
pp: g : ℝ → ℝ
t : ℝ
hg0 : Tendsto g atTop (𝓝 0)
hg : Tendsto (fun x ↦ ↑x * ↑(g x)) atTop (𝓝 ↑t)
⊢ -1 < 0

Tactic:
simp

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))

Goal state after:
g : ℝ → ℝ
t : ℝ
hg : Tendsto (fun x ↦ x * g x) atTop (𝓝 t)
hg0 : Tendsto g atTop (𝓝 0)
⊢ Tendsto (fun x ↦ (1 + g x) ^ x) atTop (𝓝 (rexp t))
Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds

Goal state before:
pp: g : ℕ → ℝ
t : ℝ
hg : Tendsto (fun n ↦ ↑n * g n) atTop (𝓝 t)
⊢ ∀ (x : ℕ), ((fun x ↦ x * log (1 + g ⌊x⌋₊)) ∘ Nat.cast) x = ↑x * log (1 + g x)

Tactic:
simp

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

Goal state before:
pp: g : ℕ → ℝ
t : ℝ
hg : Tendsto (fun n ↦ ↑n * g n) atTop (𝓝 t)
⊢ ∀ (x : ℕ), ((fun x ↦ (1 + g ⌊x⌋₊) ^ x) ∘ Nat.cast) x = (1 + g x) ^ x

Tactic:
simp

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

Goal state before:
pp: t : ℝ
⊢ ∀ (x : ℕ), ((fun x ↦ (1 + t / x) ^ x) ∘ Nat.cast) x = (1 + t / ↑x) ^ x

Tactic:
simp

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

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

Tactic:
simp

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

Goal state before:
pp: f : ℝ → ℝ
n : ℕ
hf_feq : ∀ {y : ℝ}, 0 < y → f (y + 1) = f y + log y
hn : n ≠ 0
⊢ f ↑1 = f 1 + log ↑(1 - 1)!

Tactic:
simp

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

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

Tactic:
simp

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

Goal state before:
pp: case inl
n : ℕ
⊢ Complex.sin (↑π * 0) =
    ((↑π * 0 * ∏ j ∈ Finset.range n, (1 - 0 ^ 2 / (↑j + 1) ^ 2)) *
        ∫ (x : ℝ) in 0..π / 2, Complex.cos (2 * 0 * ↑x) * ↑(cos x) ^ (2 * n)) /
      ↑(∫ (x : ℝ) in 0..π / 2, cos x ^ (2 * n))

Tactic:
simp

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))
h4 : ∀ᵐ (t : ℝ) ∂volume.restrict (Ioi 0), ∀ z ∈ Metric.ball s v, ‖F' z t‖ ≤ bound t
⊢ ∀ {j : ℝ}, b < j → j < a → IntegrableOn (fun t ↦ t ^ (j - 1) * (|log t| * ‖f t‖)) (Ioi 0) volume

Tactic:
intro j

Goal state after:
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))
h4 : ∀ᵐ (t : ℝ) ∂volume.restrict (Ioi 0), ∀ z ∈ Metric.ball s v, ‖F' z t‖ ≤ bound t
j : ℝ
⊢ b < j → j < a → IntegrableOn (fun t ↦ t ^ (j - 1) * (|log t| * ‖f t‖)) (Ioi 0) volume
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
this✝² : ∫ (x : ℝ) in 0..π / 2, cos x ^ (2 * n.succ) = (2 * ↑n + 1) / (2 * ↑n + 2) * C
this✝¹ :
  ↑π * z * (A * (1 - z ^ 2 / (↑n + 1) ^ 2)) *
      ∫ (x : ℝ) in 0..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (2 * n.succ) =
    ↑π * z * A * ((1 - z ^ 2 / ↑n.succ ^ 2) * ∫ (x : ℝ) in 0..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (2 * n.succ))
this✝ :
  (1 - z ^ 2 / ↑n.succ ^ 2) * ∫ (x : ℝ) in 0..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (2 * n.succ) =
    (2 * ↑n + 1) / (2 * ↑n + 2) * B
this : ↑C ≠ 0
⊢ 2 * ↑n = ↑(2 * n)

Tactic:
simp

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

Goal state before:
pp: ⊢ 0 < 3 / 2

Tactic:
simp

Goal state after: