mathlib-initiative/mathlib-tactics huggingface dataset:
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
⊢ (algebraMap ℝ≥0 ℝ≥0∞) (nndist x y) = edist x y

Tactic:
exact (edist_nndist _ _).symm

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

Tactic:
by
  simp [o.inner_rightAngleRotation_swap x y]

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

Goal state before:
pp: 𝕜₁ : Type u_5
𝕜₂ : Type u_6
𝕜₃ : Type u_7
E : Type u_9
F : Type u_10
G : Type u_11
inst✝¹⁸ : NormedField 𝕜₁
inst✝¹⁷ : NormedField 𝕜₂
inst✝¹⁶ : NormedField 𝕜₃
σ₁₂ : 𝕜₁ →+* 𝕜₂
σ₁₃ : 𝕜₁ →+* 𝕜₃
σ₂₃ : 𝕜₂ →+* 𝕜₃
inst✝¹⁵ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝¹⁴ : AddCommGroup E
inst✝¹³ : TopologicalSpace E
inst✝¹² : Module 𝕜₁ E
inst✝¹¹ : AddCommGroup F
inst✝¹⁰ : TopologicalSpace F
inst✝⁹ : Module 𝕜₂ F
inst✝⁸ : AddCommGroup G
inst✝⁷ : TopologicalSpace G
inst✝⁶ : Module 𝕜₃ G
inst✝⁵ : IsTopologicalAddGroup F
inst✝⁴ : ContinuousConstSMul 𝕜₂ F
inst✝³ : IsTopologicalAddGroup G
inst✝² : ContinuousConstSMul 𝕜₃ G
inst✝¹ : RingHomSurjective σ₂₃
inst✝ : RingHomIsometric σ₂₃
g : F →SWOT[σ₂₃] G
x : E
z : StrongDual 𝕜₃ G
σ_bij : Function.Bijective ⇑σ₂₃
σ_equiv : 𝕜₂ ≃+* 𝕜₃ := RingEquiv.ofBijective σ₂₃ σ_bij
invPair : RingHomInvPair σ₂₃ ↑σ_equiv.symm := RingHomInvPair.of_ringEquiv σ_equiv
invPair_symm : RingHomInvPair (↑σ_equiv.symm) σ₂₃ := RingHomInvPair.symm σ₂₃ ↑σ_equiv.symm
σ_li : 𝕜₂ ≃ₛₗᵢ[σ₂₃] 𝕜₃ :=
  let __LinearEquiv := LinearEquiv.ofBijective σ₂₃.toSemilinearMap σ_bij;
  { toLinearEquiv := __LinearEquiv, norm_map' := ⋯ }
a : E →SWOT[σ₁₂] F
| σ_li (σ_li.symm (z ((g.comp a) x)))

Tactic:
comp_apply,

Goal state after:
𝕜₁ : Type u_5
𝕜₂ : Type u_6
𝕜₃ : Type u_7
E : Type u_9
F : Type u_10
G : Type u_11
inst✝¹⁸ : NormedField 𝕜₁
inst✝¹⁷ : NormedField 𝕜₂
inst✝¹⁶ : NormedField 𝕜₃
σ₁₂ : 𝕜₁ →+* 𝕜₂
σ₁₃ : 𝕜₁ →+* 𝕜₃
σ₂₃ : 𝕜₂ →+* 𝕜₃
inst✝¹⁵ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝¹⁴ : AddCommGroup E
inst✝¹³ : TopologicalSpace E
inst✝¹² : Module 𝕜₁ E
inst✝¹¹ : AddCommGroup F
inst✝¹⁰ : TopologicalSpace F
inst✝⁹ : Module 𝕜₂ F
inst✝⁸ : AddCommGroup G
inst✝⁷ : TopologicalSpace G
inst✝⁶ : Module 𝕜₃ G
inst✝⁵ : IsTopologicalAddGroup F
inst✝⁴ : ContinuousConstSMul 𝕜₂ F
inst✝³ : IsTopologicalAddGroup G
inst✝² : ContinuousConstSMul 𝕜₃ G
inst✝¹ : RingHomSurjective σ₂₃
inst✝ : RingHomIsometric σ₂₃
g : F →SWOT[σ₂₃] G
x : E
z : StrongDual 𝕜₃ G
σ_bij : Function.Bijective ⇑σ₂₃
σ_equiv : 𝕜₂ ≃+* 𝕜₃ := RingEquiv.ofBijective σ₂₃ σ_bij
invPair : RingHomInvPair σ₂₃ ↑σ_equiv.symm := RingHomInvPair.of_ringEquiv σ_equiv
invPair_symm : RingHomInvPair (↑σ_equiv.symm) σ₂₃ := RingHomInvPair.symm σ₂₃ ↑σ_equiv.symm
σ_li : 𝕜₂ ≃ₛₗᵢ[σ₂₃] 𝕜₃ :=
  let __LinearEquiv := LinearEquiv.ofBijective σ₂₃.toSemilinearMap σ_bij;
  { toLinearEquiv := __LinearEquiv, norm_map' := ⋯ }
a : E →SWOT[σ₁₂] F
| σ_li (σ_li.symm (z (g (a x))))
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
this :
  IntegrableOn (fun x ↦ ↑(a * x) ^ (s - 1) • f (a * x)) (Ioi 0) volume ↔
    IntegrableOn (fun t ↦ ↑t ^ (s - 1) • f t) (Ioi 0) volume
h1 : EqOn (fun t ↦ ↑(a * t) ^ (s - 1) • f (a * t)) (↑a ^ (s - 1) • fun t ↦ ↑t ^ (s - 1) • f (a * t)) (Ioi 0)
⊢ ¬(↑a = 0 ∧ s - 1 ≠ 0)

Tactic:
not_and_or,

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℝ → E
s : ℂ
a : ℝ
ha : 0 < a
this :
  IntegrableOn (fun x ↦ ↑(a * x) ^ (s - 1) • f (a * x)) (Ioi 0) volume ↔
    IntegrableOn (fun t ↦ ↑t ^ (s - 1) • f t) (Ioi 0) volume
h1 : EqOn (fun t ↦ ↑(a * t) ^ (s - 1) • f (a * t)) (↑a ^ (s - 1) • fun t ↦ ↑t ^ (s - 1) • f (a * t)) (Ioi 0)
⊢ ¬↑a = 0 ∨ ¬s - 1 ≠ 0
Module: Mathlib.Analysis.MellinInversion

Goal state before:
pp: case e_a.e_a
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℝ → E
s : ℂ
u : ℝ
⊢ -↑s.im * ↑u = ↑(-2 * π * (u * (s.im / (2 * π))))

Tactic:
simp [field]

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✝
𝕜₁ : Type u_5
𝕜₂ : Type u_6
𝕜₃ : Type u_7
𝕜₄ : Type u_8
E : Type u_9
F : Type u_10
G : Type u_11
H : Type u_12
inst✝²³ : NormedField 𝕜₁
inst✝²² : NormedField 𝕜₂
inst✝²¹ : NormedField 𝕜₃
inst✝²⁰ : NormedField 𝕜₄
σ₁₂ : 𝕜₁ →+* 𝕜₂
σ₁₃ : 𝕜₁ →+* 𝕜₃
σ₁₄ : 𝕜₁ →+* 𝕜₄
σ₂₃ : 𝕜₂ →+* 𝕜₃
σ₂₄ : 𝕜₂ →+* 𝕜₄
σ₃₄ : 𝕜₃ →+* 𝕜₄
inst✝¹⁹ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝¹⁸ : RingHomCompTriple σ₁₃ σ₃₄ σ₁₄
inst✝¹⁷ : RingHomCompTriple σ₁₂ σ₂₄ σ₁₄
inst✝¹⁶ : RingHomCompTriple σ₂₃ σ₃₄ σ₂₄
inst✝¹⁵ : AddCommGroup E
inst✝¹⁴ : TopologicalSpace E
inst✝¹³ : Module 𝕜₁ E
inst✝¹² : AddCommGroup F
inst✝¹¹ : TopologicalSpace F
inst✝¹⁰ : Module 𝕜₂ F
inst✝⁹ : AddCommGroup G
inst✝⁸ : TopologicalSpace G
inst✝⁷ : Module 𝕜₃ G
inst✝⁶ : AddCommGroup H
inst✝⁵ : TopologicalSpace H
inst✝⁴ : Module 𝕜₄ H
inst✝³ : IsTopologicalAddGroup F
inst✝² : ContinuousConstSMul 𝕜₂ F
inst✝¹ : IsTopologicalAddGroup G
inst✝ : ContinuousConstSMul 𝕜₃ G
x✝ : F →WOT[𝕜₂] F
⊢ Continuous[instTopologicalSpace, instTopologicalSpace] fun x ↦ x✝ * x

Tactic:
mul_eq_comp

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✝²⁸ : TopologicalSpace E✝
inst✝²⁷ : Module 𝕜₁✝ E✝
inst✝²⁶ : AddCommGroup F✝
inst✝²⁵ : TopologicalSpace F✝
inst✝²⁴ : Module 𝕜₂✝ F✝
𝕜₁ : Type u_5
𝕜₂ : Type u_6
𝕜₃ : Type u_7
𝕜₄ : Type u_8
E : Type u_9
F : Type u_10
G : Type u_11
H : Type u_12
inst✝²³ : NormedField 𝕜₁
inst✝²² : NormedField 𝕜₂
inst✝²¹ : NormedField 𝕜₃
inst✝²⁰ : NormedField 𝕜₄
σ₁₂ : 𝕜₁ →+* 𝕜₂
σ₁₃ : 𝕜₁ →+* 𝕜₃
σ₁₄ : 𝕜₁ →+* 𝕜₄
σ₂₃ : 𝕜₂ →+* 𝕜₃
σ₂₄ : 𝕜₂ →+* 𝕜₄
σ₃₄ : 𝕜₃ →+* 𝕜₄
inst✝¹⁹ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝¹⁸ : RingHomCompTriple σ₁₃ σ₃₄ σ₁₄
inst✝¹⁷ : RingHomCompTriple σ₁₂ σ₂₄ σ₁₄
inst✝¹⁶ : RingHomCompTriple σ₂₃ σ₃₄ σ₂₄
inst✝¹⁵ : AddCommGroup E
inst✝¹⁴ : TopologicalSpace E
inst✝¹³ : Module 𝕜₁ E
inst✝¹² : AddCommGroup F
inst✝¹¹ : TopologicalSpace F
inst✝¹⁰ : Module 𝕜₂ F
inst✝⁹ : AddCommGroup G
inst✝⁸ : TopologicalSpace G
inst✝⁷ : Module 𝕜₃ G
inst✝⁶ : AddCommGroup H
inst✝⁵ : TopologicalSpace H
inst✝⁴ : Module 𝕜₄ H
inst✝³ : IsTopologicalAddGroup F
inst✝² : ContinuousConstSMul 𝕜₂ F
inst✝¹ : IsTopologicalAddGroup G
inst✝ : ContinuousConstSMul 𝕜₃ G
x✝ : F →WOT[𝕜₂] F
⊢ Continuous[instTopologicalSpace, instTopologicalSpace] fun x ↦ x✝.comp x
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✝
𝕜₁ : Type u_5
𝕜₂ : Type u_6
𝕜₃ : Type u_7
𝕜₄ : Type u_8
E : Type u_9
F : Type u_10
G : Type u_11
H : Type u_12
inst✝²³ : NormedField 𝕜₁
inst✝²² : NormedField 𝕜₂
inst✝²¹ : NormedField 𝕜₃
inst✝²⁰ : NormedField 𝕜₄
σ₁₂ : 𝕜₁ →+* 𝕜₂
σ₁₃ : 𝕜₁ →+* 𝕜₃
σ₁₄ : 𝕜₁ →+* 𝕜₄
σ₂₃ : 𝕜₂ →+* 𝕜₃
σ₂₄ : 𝕜₂ →+* 𝕜₄
σ₃₄ : 𝕜₃ →+* 𝕜₄
inst✝¹⁹ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝¹⁸ : RingHomCompTriple σ₁₃ σ₃₄ σ₁₄
inst✝¹⁷ : RingHomCompTriple σ₁₂ σ₂₄ σ₁₄
inst✝¹⁶ : RingHomCompTriple σ₂₃ σ₃₄ σ₂₄
inst✝¹⁵ : AddCommGroup E
inst✝¹⁴ : TopologicalSpace E
inst✝¹³ : Module 𝕜₁ E
inst✝¹² : AddCommGroup F
inst✝¹¹ : TopologicalSpace F
inst✝¹⁰ : Module 𝕜₂ F
inst✝⁹ : AddCommGroup G
inst✝⁸ : TopologicalSpace G
inst✝⁷ : Module 𝕜₃ G
inst✝⁶ : AddCommGroup H
inst✝⁵ : TopologicalSpace H
inst✝⁴ : Module 𝕜₄ H
inst✝³ : IsTopologicalAddGroup F
inst✝² : ContinuousConstSMul 𝕜₂ F
inst✝¹ : IsTopologicalAddGroup G
inst✝ : ContinuousConstSMul 𝕜₃ G
x✝ : F →WOT[𝕜₂] F
⊢ Continuous[instTopologicalSpace, instTopologicalSpace] fun x ↦ x * x✝

Tactic:
mul_eq_comp

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✝²⁸ : TopologicalSpace E✝
inst✝²⁷ : Module 𝕜₁✝ E✝
inst✝²⁶ : AddCommGroup F✝
inst✝²⁵ : TopologicalSpace F✝
inst✝²⁴ : Module 𝕜₂✝ F✝
𝕜₁ : Type u_5
𝕜₂ : Type u_6
𝕜₃ : Type u_7
𝕜₄ : Type u_8
E : Type u_9
F : Type u_10
G : Type u_11
H : Type u_12
inst✝²³ : NormedField 𝕜₁
inst✝²² : NormedField 𝕜₂
inst✝²¹ : NormedField 𝕜₃
inst✝²⁰ : NormedField 𝕜₄
σ₁₂ : 𝕜₁ →+* 𝕜₂
σ₁₃ : 𝕜₁ →+* 𝕜₃
σ₁₄ : 𝕜₁ →+* 𝕜₄
σ₂₃ : 𝕜₂ →+* 𝕜₃
σ₂₄ : 𝕜₂ →+* 𝕜₄
σ₃₄ : 𝕜₃ →+* 𝕜₄
inst✝¹⁹ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝¹⁸ : RingHomCompTriple σ₁₃ σ₃₄ σ₁₄
inst✝¹⁷ : RingHomCompTriple σ₁₂ σ₂₄ σ₁₄
inst✝¹⁶ : RingHomCompTriple σ₂₃ σ₃₄ σ₂₄
inst✝¹⁵ : AddCommGroup E
inst✝¹⁴ : TopologicalSpace E
inst✝¹³ : Module 𝕜₁ E
inst✝¹² : AddCommGroup F
inst✝¹¹ : TopologicalSpace F
inst✝¹⁰ : Module 𝕜₂ F
inst✝⁹ : AddCommGroup G
inst✝⁸ : TopologicalSpace G
inst✝⁷ : Module 𝕜₃ G
inst✝⁶ : AddCommGroup H
inst✝⁵ : TopologicalSpace H
inst✝⁴ : Module 𝕜₄ H
inst✝³ : IsTopologicalAddGroup F
inst✝² : ContinuousConstSMul 𝕜₂ F
inst✝¹ : IsTopologicalAddGroup G
inst✝ : ContinuousConstSMul 𝕜₃ G
x✝ : F →WOT[𝕜₂] F
⊢ Continuous[instTopologicalSpace, instTopologicalSpace] fun x ↦ x.comp x✝
Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds

Goal state before:
pp: z : ℂ
n : ℕ
ih : HasDerivAt (logTaylor (n + 1)) (∑ j ∈ Finset.range n, (-1) ^ j * z ^ j) z
⊢ HasDerivAt (fun x ↦ x ^ (n + 1) * (↑n + 1)⁻¹) (z ^ n) z

Tactic:
convert! HasDerivAt.mul_const (hasDerivAt_pow (n + 1) z) (((n : ℂ) + 1)⁻¹) using 1

Goal state after:
case e'_9
z : ℂ
n : ℕ
ih : HasDerivAt (logTaylor (n + 1)) (∑ j ∈ Finset.range n, (-1) ^ j * z ^ j) z
⊢ z ^ n = ↑(n + 1) * z ^ (n + 1 - 1) * (↑n + 1)⁻¹
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
⊢ z ^ n = ↑(n + 1) * z ^ (n + 1 - 1) * (↑n + 1)⁻¹

Tactic:
simp [field]

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

Goal state before:
pp: case e'_9
n : ℕ
z : ℂ
hz : 1 + z ∈ slitPlane
hz' : -z ≠ 1
⊢ (-z) ^ n * (1 + z)⁻¹ = (1 + z)⁻¹ - -(((-z) ^ n - 1) / (1 + z))

Tactic:
simp [field]

Goal state after:
Module: Mathlib.Analysis.MellinTransform

Goal state before:
pp: case refine_1
f : ℝ → ℝ
hfc : AEStronglyMeasurable f (volume.restrict (Ioi 0))
a s : ℝ
hf : f =O[atTop] fun x ↦ x ^ (-a)
hs : s < a
d e : ℝ
he : ∀ (b : ℝ), e ≤ b → ‖f b‖ ≤ d * ‖b ^ (-a)‖
he' : 0 < max e 1
⊢ AEStronglyMeasurable (fun t ↦ t ^ (s - 1) * f t) (volume.restrict (Ioi (max e 1)))

Tactic:
refine AEStronglyMeasurable.mul ?_ (hfc.mono_set (Ioi_subset_Ioi he'.le))
    refine (continuousOn_of_forall_continuousAt fun t ht => ?_).aestronglyMeasurable
      measurableSet_Ioi
    exact continuousAt_rpow_const _ _ (Or.inl <| (he'.trans ht).ne')

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

Goal state before:
pp: case neg
s : ℂ
hs : s ≠ 0
h : ∀ (m : ℕ), s ≠ -↑m
⊢ HasDerivWithinAt (fun s ↦ Gamma (s + 1)) (Gamma s + s * deriv Gamma s) {0}ᶜ s

Tactic:
refine HasDerivWithinAt.congr ?_ Gamma_add_one (Gamma_add_one s hs)

Goal state after:
case neg
s : ℂ
hs : s ≠ 0
h : ∀ (m : ℕ), s ≠ -↑m
⊢ HasDerivWithinAt (fun x ↦ x * Gamma x) (Gamma s + s * deriv Gamma s) {0}ᶜ s
Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds

Goal state before:
pp: n : ℕ
z : ℂ
hz : ‖z‖ < 1
help : IntervalIntegrable (fun t ↦ t ^ n * (1 - ‖z‖)⁻¹) MeasureTheory.volume 0 1
f : ℂ → ℂ := fun z ↦ log (1 + z) - logTaylor (n + 1) z
f' : ℂ → ℂ := fun z ↦ (-z) ^ n * (1 + z)⁻¹
hderiv : ∀ t ∈ Set.Icc 0 1, HasDerivAt f (f' (0 + ↑t * z)) (0 + ↑t * z)
hcont : ContinuousOn (fun t ↦ f' (0 + ↑t * z)) (Set.Icc 0 1)
H : log (1 + z) - logTaylor (n + 1) z = z * ∫ (t : ℝ) in 0..1, (-(↑t * z)) ^ n * (1 + ↑t * z)⁻¹
⊢ (1 - ‖z‖)⁻¹ * ((1 ^ (n + 1) - 0 ^ (n + 1)) / (↑n + 1)) = (1 - ‖z‖)⁻¹ / (↑n + 1)

Tactic:
simp [field]

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‖
z : ℂ
⊢ ContinuousOn (fun t ↦ ↑t ^ (z - 1)) (Ioi 0)

Tactic:
refine continuousOn_of_forall_continuousAt fun t ht => ?_

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‖
z : ℂ
t : ℝ
ht : t ∈ Ioi 0
⊢ ContinuousAt (fun t ↦ ↑t ^ (z - 1)) t
Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds

Goal state before:
pp: g : ℝ → ℂ
t : ℂ
hg : Tendsto (fun x ↦ ↑x * g x) atTop (𝓝 t)
⊢ (fun x ↦ (↑x * g x) ^ 2 * ↑x⁻¹) =O[atTop] fun x ↦ ↑x⁻¹

Tactic:
by
      simpa using isBigO_const_of_tendsto hg (one_ne_zero (α := ℂ))
        |>.pow 2 |>.mul (isBigO_refl _ _)

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

Tactic:
hf_feq hn'

Goal state after:
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)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd

Goal state before:
pp: case inr.zero
z : ℂ
hz : z ≠ 0
⊢ Complex.sin (↑π * z) = ↑π * z * (Complex.sin (↑π * z) / (2 * z)) / ↑(π / 2)

Tactic:
simp [field]

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

Goal state before:
pp: case hx
x : ℝ
n : ℕ
⊢ ↑(n + 1) ≠ 0

Tactic:
Nat.cast_ne_zero

Goal state after:
case hx
x : ℝ
n : ℕ
⊢ n + 1 ≠ 0
Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup

Goal state before:
pp: case hy
x : ℝ
n : ℕ
⊢ ↑n ! ≠ 0

Tactic:
Nat.cast_ne_zero

Goal state after:
case hy
x : ℝ
n : ℕ
⊢ n ! ≠ 0
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
this✝ : 2 * ↑n + 1 ≠ 0
this : ↑n + 1 ≠ 0
⊢ ↑π * z * A * B / ↑C = ↑π * z * A * ((2 * ↑n + 1) / (2 * ↑n + 2) * B) / (↑(2 * ↑n + 1) / ↑(2 * ↑n + 2) * ↑C)

Tactic:
simp [field]

Goal state after:
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:
rw [hn, Finset.prod_range_succ]
    set A := ∏ j ∈ Finset.range n, ((1 : ℂ) - z ^ 2 / ((j : ℂ) + 1) ^ 2)
    set B := ∫ x in (0 : ℝ)..π / 2, Complex.cos (2 * z * x) * (cos x : ℂ) ^ (2 * n)
    set C := ∫ x in (0 : ℝ)..π / 2, cos x ^ (2 * n)
    have aux' : 2 * n.succ = 2 * n + 2 := by rw [Nat.succ_eq_add_one, mul_add, mul_one]
    have : (∫ x in (0 : ℝ)..π / 2, cos x ^ (2 * n.succ)) = (2 * (n : ℝ) + 1) / (2 * n + 2) * C := by
      rw [integral_cos_pow_eq]
      dsimp only [C]
      rw [integral_cos_pow_eq, aux', integral_sin_pow, sin_zero, sin_pi, pow_succ',
        zero_mul, zero_mul, zero_mul, sub_zero, zero_div,
        zero_add, ← mul_assoc, ← mul_assoc, mul_comm (1 / 2 : ℝ) _, Nat.cast_mul, Nat.cast_ofNat]
    rw [this]
    change
      π * z * A * B / C =
        (π * z * (A * ((1 : ℂ) - z ^ 2 / ((n : ℂ) + 1) ^ 2)) *
            ∫ x in (0 : ℝ)..π / 2, Complex.cos (2 * z * x) * (cos x : ℂ) ^ (2 * n.succ)) /
          ((2 * n + 1) / (2 * n + 2) * C : ℝ)
    have :
      (π * 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)) := by
      grind
    rw [this]
    suffices
      (((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 by
      rw [this, Complex.ofReal_mul, Complex.ofReal_div]
      have : (C : ℂ) ≠ 0 := Complex.ofReal_ne_zero.mpr (integral_cos_pow_pos _).ne'
      have : 2 * (n : ℂ) + 1 ≠ 0 := by
        convert! (Nat.cast_add_one_ne_zero (2 * n) : (↑(2 * n) + 1 : ℂ) ≠ 0)
        simp
      have : (n : ℂ) + 1 ≠ 0 := Nat.cast_add_one_ne_zero n
      simp [field]
    convert! integral_cos_mul_cos_pow_even n hz
    rw [Nat.cast_succ]

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
u v : V
p : P
⊢ u +ᵥ map (fun x ↦ x +ᵥ p) (asymptoticNhds k V v) = map (fun x ↦ x +ᵥ u +ᵥ p) (asymptoticNhds k V v)

Tactic:
← Filter.map_vadd,

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
u v : V
p : P
⊢ map (fun b ↦ u +ᵥ b) (map (fun x ↦ x +ᵥ p) (asymptoticNhds k V v)) = map (fun x ↦ x +ᵥ u +ᵥ p) (asymptoticNhds k V v)
Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup

Goal state before:
pp: ⊢ doublingGamma 1 = 1

Tactic:
simp_rw [doublingGamma, Gamma_one_half_eq, add_halves (1 : ℝ), sub_self, Gamma_one, mul_one,
    rpow_zero, mul_one, div_self (sqrt_ne_zero'.mpr pi_pos)]

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

Goal state before:
pp: s : ℂ
hs : 0 < s.re
n : ℕ
hn : n ≠ 0
this : ∀ (x : ℝ), x = x / ↑n * ↑n
x : ℝ
| ↑x

Tactic:
this x

Goal state after:
s : ℂ
hs : 0 < s.re
n : ℕ
hn : n ≠ 0
this : ∀ (x : ℝ), x = x / ↑n * ↑n
x : ℝ
| ↑(x / ↑n * ↑n)
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
s : Set P
⊢ IsClosed[inst✝⁵] (asymptoticCone k s)

Tactic:
by
  have ⟨p⟩ : Nonempty P := inferInstance
  rw [isClosed_iff_frequently]
  intro v h
  simp_rw [mem_asymptoticCone_iff, ← frequently_bind, nhds_bind_asymptoticNhds] at h
  exact h

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
j : ℕ
⊢ ↑j.succ ≠ 0

Tactic:
Nat.cast_ne_zero

Goal state after:
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
j : ℕ
⊢ j.succ ≠ 0
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta

Goal state before:
pp: s : ℂ
⊢ DifferentiableAt ℂ (fun s ↦ (Gamma s)⁻¹) s

Tactic:
rcases exists_nat_gt (-s.re) with ⟨n, hs⟩
  induction n generalizing s with
  | zero =>
    rw [Nat.cast_zero, neg_lt_zero] at hs
    suffices ∀ m : ℕ, s ≠ -↑m from (differentiableAt_Gamma _ this).inv (Gamma_ne_zero this)
    rintro m rfl
    apply hs.not_ge
    simp
  | succ n ihn =>
    rw [funext one_div_Gamma_eq_self_mul_one_div_Gamma_add_one]
    specialize ihn (s + 1) (by rwa [add_re, one_re, neg_add', sub_lt_iff_lt_add, ← Nat.cast_succ])
    exact differentiableAt_id.mul (ihn.comp s (f := fun s => s + 1) <|
      differentiableAt_id.add_const (1 : ℂ))

Goal state after:
Module: Mathlib.Analysis.Normed.Field.Approximation

Goal state before:
pp: case convert_3
K : Type u_1
inst✝ : NormedField K
f g : K[X]
ε : ℝ
hε : 0 < ε
a : K
ha : eval a f = 0
hfm : f.Monic
hgm : g.Monic
hdeg : g.natDegree = f.natDegree
hcoeff : ∀ (i : ℕ), ‖g.coeff i - f.coeff i‖ < ε
hg : g.Splits
⊢ ∀ i ∈ Finset.range (f.natDegree + 1), ‖(g.coeff i - f.coeff i) * a ^ i‖ < ε * max ‖a‖ 1 ^ f.natDegree

Tactic:
· simp only [Finset.mem_range, norm_mul, norm_pow]
      intro i hi
      apply mul_lt_mul_of_lt_of_le_of_nonneg_of_pos
      · simpa [← map_sub] using hcoeff i
      · refine (pow_le_pow_left₀ (norm_nonneg a) (le_max_left ‖a‖ 1) i).trans ?_
        exact pow_le_pow_right₀ (le_max_right ‖a‖ 1) (Nat.le_of_lt_succ hi)
      all_goals positivity

Goal state after:
Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromConst

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
c : R
f : RingSeminorm R
hf1 : f 1 ≤ 1
hc : f c ≠ 0
hpm : IsPowMul ⇑f
x : R
⊢ seminormFromConst' c f (c * x) = seminormFromConst' c f c * seminormFromConst' c f x

Tactic:
by
  have hlim : Tendsto (fun n ↦ seminormFromConst_seq c f x (n + 1)) atTop
      (𝓝 (seminormFromConst' c f x)) := by
    apply (tendsto_seminormFromConst_seq_atTop hf1 hc hpm x).comp
      (tendsto_atTop_atTop_of_monotone add_left_mono _)
    rintro n; use n; lia
  rw [seminormFromConst_apply_c hf1 hc hpm]
  apply tendsto_nhds_unique (tendsto_seminormFromConst_seq_atTop hf1 hc hpm (c * x))
  have hterm : seminormFromConst_seq c f (c * x) =
      fun n ↦ f c * seminormFromConst_seq c f x (n + 1) := by
    simp only [seminormFromConst_seq_def]
    ext n
    ring_nf
    rw [mul_assoc _ (f c), mul_inv_cancel₀ hc, mul_one]
  simpa [hterm] using tendsto_const_nhds.mul hlim

Goal state after:
Module: Mathlib.Analysis.Normed.Group.Completeness

Goal state before:
pp: E : Type u_1
inst✝ : NormedAddCommGroup E
h : ∀ (u : ℕ → E), (Summable fun x ↦ ‖u x‖) → ∃ a, Tendsto (fun n ↦ ∑ i ∈ range n, u i) atTop (𝓝 a)
⊢ ∀ (u : ℕ → E), CauchySeq u → ∃ a, Tendsto u atTop (𝓝 a)

Tactic:
intro u hu

Goal state after:
E : Type u_1
inst✝ : NormedAddCommGroup E
h : ∀ (u : ℕ → E), (Summable fun x ↦ ‖u x‖) → ∃ a, Tendsto (fun n ↦ ∑ i ∈ range n, u i) atTop (𝓝 a)
u : ℕ → E
hu : CauchySeq u
⊢ ∃ a, Tendsto u atTop (𝓝 a)