mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Order

Goal state before:
pp: case inl.inl
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
p : ℝ≥0
hIcc : Icc 0 1 = Ioo 0 1 ∪ {0} ∪ {1}
hp : p ∈ Ioo 0 1
⊢ ConcaveOn ℝ (Ici 0) fun a ↦ a ^ p

pp: case inl.inr
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
p : ℝ≥0
hIcc : Icc 0 1 = Ioo 0 1 ∪ {0} ∪ {1}
hp : p ∈ {0}
⊢ ConcaveOn ℝ (Ici 0) fun a ↦ a ^ p

pp: case inr
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
p : ℝ≥0
hIcc : Icc 0 1 = Ioo 0 1 ∪ {0} ∪ {1}
hp : p ∈ {1}
⊢ ConcaveOn ℝ (Ici 0) fun a ↦ a ^ p

Tactic:
· exact concaveOn_nnrpow_Ioo hp

Goal state after:
case inl.inr
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
p : ℝ≥0
hIcc : Icc 0 1 = Ioo 0 1 ∪ {0} ∪ {1}
hp : p ∈ {0}
⊢ ConcaveOn ℝ (Ici 0) fun a ↦ a ^ p

case inr
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
p : ℝ≥0
hIcc : Icc 0 1 = Ioo 0 1 ∪ {0} ∪ {1}
hp : p ∈ {1}
⊢ ConcaveOn ℝ (Ici 0) fun a ↦ a ^ p
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Order

Goal state before:
pp: case inl
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
p : ℝ
hp : p ∈ Icc 0 1
q : ℝ≥0 := ⟨p, ⋯⟩
hq : q = 0
a : A
⊢ ∀ ⦃b : A⦄, a ≤ b → (fun a ↦ a ^ ↑0) a ≤ (fun a ↦ a ^ ↑0) b

Tactic:
b

Goal state after:
case inl
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
p : ℝ
hp : p ∈ Icc 0 1
q : ℝ≥0 := ⟨p, ⋯⟩
hq : q = 0
a b : A
⊢ a ≤ b → (fun a ↦ a ^ ↑0) a ≤ (fun a ↦ a ^ ↑0) b
Module: Mathlib.Analysis.SpecialFunctions.Log.RpowTendsto

Goal state before:
pp: p x : ℝ
p_pos : 0 < p
x_pos : 0 < x
hx : ‖p * log x‖ ≤ 1
pinv_nonneg : 0 ≤ p⁻¹
⊢ p⁻¹ * ‖p * log x‖ ^ 2 = p * ‖log x‖ ^ 2

Tactic:
simp only [norm_mul]
          grind [Real.norm_of_nonneg]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.RingInverseOrder

Goal state before:
pp: A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
x : A
xpos : IsStrictlyPositive x
y : A
ypos : IsStrictlyPositive y
a : ℝ
⊢ ∀ ⦃b : ℝ⦄, 0 ≤ a → 0 ≤ b → a + b = 1 → (a • x + b • y)⁻¹ʳ ≤ a • x⁻¹ʳ + b • y⁻¹ʳ

Tactic:
b

Goal state after:
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
x : A
xpos : IsStrictlyPositive x
y : A
ypos : IsStrictlyPositive y
a b : ℝ
⊢ 0 ≤ a → 0 ≤ b → a + b = 1 → (a • x + b • y)⁻¹ʳ ≤ a • x⁻¹ʳ + b • y⁻¹ʳ
Module: Mathlib.Analysis.SpecialFunctions.FrullaniIntegral

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
L R : E
inst✝ : CompleteSpace E
hf : LocallyIntegrableOn f (Ioi 0) volume
ha : 0 < a
hb : 0 < b
hL : Tendsto f (𝓝[>] 0) (𝓝 L)
hR : Tendsto f atTop (𝓝 R)
u : ℝ → E := fun x ↦ x⁻¹ • f x
hint : ∀ {p q : ℝ}, 0 < p → 0 < q → IntervalIntegrable u volume p q
hsplit :
  ∀ {ε r : ℝ},
    0 < ε →
      0 < r →
        ∫ (x : ℝ) in ε..r, x⁻¹ • (f (a * x) - f (b * x)) =
          (∫ (x : ℝ) in a * ε..b * ε, u x) - ∫ (x : ℝ) in a * r..b * r, u x
ε r : ℝ
hε : (ε, r).1 ∈ {x | x ∈ Ioi 0}
hr : (ε, r).2 ∈ {x | 0 < x}
⊢ ∫ (x : ℝ) in (ε, r).1..(ε, r).2, x⁻¹ • (f (a * x) - f (b * x)) =
    (∫ (x : ℝ) in a * (ε, r).1..b * (ε, r).1, u x) - ∫ (x : ℝ) in a * (ε, r).2..b * (ε, r).2, u x

Tactic:
exact hsplit hε hr

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

Goal state before:
pp: ⊢ Tendsto (fun s ↦ s * s.Gammaℝ) (𝓝[≠] 0) (𝓝 2)

Tactic:
have h : Tendsto (fun z : ℂ ↦ z / 2 * Gamma (z / 2)) (𝓝[≠] 0) (𝓝 1) := by
    refine tendsto_self_mul_Gamma_nhds_zero.comp ?_
    rw [tendsto_nhdsWithin_iff, (by simp : 𝓝 (0 : ℂ) = 𝓝 (0 / 2))]
    exact ⟨(tendsto_id.div_const _).mono_left nhdsWithin_le_nhds,
      eventually_of_mem self_mem_nhdsWithin fun x hx ↦ div_ne_zero hx two_ne_zero⟩
  have h' : Tendsto (fun s : ℂ ↦ 2 * (π : ℂ) ^ (-s / 2)) (𝓝[≠] 0) (𝓝 2) := by
    rw [(by simp : 𝓝 2 = 𝓝 (2 * (π : ℂ) ^ (-(0 : ℂ) / 2)))]
    refine Tendsto.mono_left (ContinuousAt.tendsto ?_) nhdsWithin_le_nhds
    exact continuousAt_const.mul ((continuousAt_const_cpow (ofReal_ne_zero.mpr pi_ne_zero)).comp
      (by fun_prop))
  convert! mul_one (2 : ℂ) ▸ (h'.mul h) using 2 with z
  rw [Gammaℝ]
  ring_nf

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation

Goal state before:
pp: p x : ℝ
hp : p ∈ Ioo 0 1
hx : 0 ≤ x
⊢ AEStronglyMeasurable (fun x_1 ↦ p.rpowIntegrand₀₁ x_1 x) (volume.restrict (Ioo 0 1))

Tactic:
refine ContinuousOn.aestronglyMeasurable ?_ measurableSet_Ioo

Goal state after:
p x : ℝ
hp : p ∈ Ioo 0 1
hx : 0 ≤ x
⊢ ContinuousOn (fun x_1 ↦ p.rpowIntegrand₀₁ x_1 x) (Ioo 0 1)
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation

Goal state before:
pp: case finite
p x : ℝ
hp : p ∈ Ioo 0 1
hx : 0 ≤ x
⊢ HasFiniteIntegral (fun x_1 ↦ p.rpowIntegrand₀₁ x_1 x) (volume.restrict (Ioi 1))

Tactic:
case finite =>
    refine HasFiniteIntegral.mono' (g := fun t => t ^ (p - 2) * x) ?finitebound ?ae_le
    case finitebound =>
      refine HasFiniteIntegral.mul_const ?_ _
      apply Integrable.hasFiniteIntegral
      rw [Set.mem_Ioo] at hp
      refine integrableOn_Ioi_rpow_of_lt ?_ zero_lt_one
      linarith
    case ae_le =>
      refine ae_restrict_of_forall_mem measurableSet_Ioi fun t (ht : 1 < t) => ?_
      rw [Real.norm_of_nonneg (rpowIntegrand₀₁_nonneg hp.1 (by positivity) hx)]
      exact rpowIntegrand₀₁_le_rpow_sub_two_mul_self hp (by positivity) hx

Goal state after:
Module: Mathlib.NumberTheory.Harmonic.GammaDeriv

Goal state before:
pp: h_diff : ∀ {s : ℝ}, 0 < s → DifferentiableAt ℝ Gamma s
h_diff' : ∀ {s : ℝ}, 0 < s → DifferentiableAt ℝ (fun s ↦ Gamma (2 * s)) s
⊢ √π * (-2 * γ + deriv (fun s ↦ 2 ^ (1 - 2 * s)) (1 / 2) + γ) = √π * (-2 * γ + -(2 * log 2) + γ)

Tactic:
by
    congr 3
    apply HasDerivAt.deriv
    have := HasDerivAt.rpow (hasDerivAt_const (1 / 2 : ℝ) (2 : ℝ))
      (?_ : HasDerivAt (fun s : ℝ ↦ 1 - 2 * s) (-2) (1 / 2)) two_pos
    · simpa
    simp_rw [mul_comm (2 : ℝ) _]
    apply HasDerivAt.const_sub
    exact hasDerivAt_mul_const (2 : ℝ)

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Gaussian.PoissonSummation

Goal state before:
pp: a : ℂ
ha : 0 < a.re
b : ℂ
f : ℝ → ℂ := fun x ↦ cexp (-↑π * a * ↑x ^ 2 + 2 * ↑π * b * ↑x)
hFf : 𝓕 f = fun x ↦ 1 / a ^ (1 / 2) * cexp (-↑π / a * (↑x + I * b) ^ 2)
h1 : 0 < (↑π * a).re
h2 : 0 < (↑π / a).re
f_bd : f =O[cocompact ℝ] fun x ↦ |x| ^ (-2)
this : ∀ (x : ℝ), -↑π / a * (↑x + I * b) ^ 2 = -↑π / a * ↑x ^ 2 + -2 * ↑π * I * b / a * ↑x + ↑π * b ^ 2 / a
| (fun x ↦ 1 / a ^ (1 / 2) * cexp (-↑π / a * ↑x ^ 2 + -2 * ↑π * I * b / a * ↑x + ↑π * b ^ 2 / a)) =O[cocompact ℝ]
    fun x ↦ |x| ^ (-2)

Tactic:
enter [2, x]; rw [Complex.exp_add, ← mul_assoc _ _ (Complex.exp _), mul_comm]

Goal state after:
a : ℂ
ha : 0 < a.re
b : ℂ
f : ℝ → ℂ := fun x ↦ cexp (-↑π * a * ↑x ^ 2 + 2 * ↑π * b * ↑x)
hFf : 𝓕 f = fun x ↦ 1 / a ^ (1 / 2) * cexp (-↑π / a * (↑x + I * b) ^ 2)
h1 : 0 < (↑π * a).re
h2 : 0 < (↑π / a).re
f_bd : f =O[cocompact ℝ] fun x ↦ |x| ^ (-2)
this : ∀ (x : ℝ), -↑π / a * (↑x + I * b) ^ 2 = -↑π / a * ↑x ^ 2 + -2 * ↑π * I * b / a * ↑x + ↑π * b ^ 2 / a
x : ℝ
| cexp (↑π * b ^ 2 / a) * (1 / a ^ (1 / 2) * cexp (-↑π / a * ↑x ^ 2 + -2 * ↑π * I * b / a * ↑x))
Module: Mathlib.Data.Int.Log

Goal state before:
pp: case inl
R : Type u_1
inst✝³ : Semifield R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorSemiring R
b : ℕ
r : R
hb : 1 < b
hr : 0 < r
hr1 : 1 ≤ r
⊢ ↑b ^ log b r ≤ r

Tactic:
log_of_one_le_right _ hr1

Goal state after:
case inl
R : Type u_1
inst✝³ : Semifield R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorSemiring R
b : ℕ
r : R
hb : 1 < b
hr : 0 < r
hr1 : 1 ≤ r
⊢ ↑b ^ ↑(Nat.log b ⌊r⌋₊) ≤ r
Module: Mathlib.Analysis.SpecialFunctions.Log.Base

Goal state before:
pp: a b : ℝ
h₁ : a ≠ 0
h₂ : b ≠ 0
c : ℝ
⊢ (logb (a * b) c)⁻¹ = (logb a c)⁻¹ + (logb b c)⁻¹

Tactic:
by
  simp_rw [inv_logb]; exact logb_mul h₁ h₂

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation

Goal state before:
pp: A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
p t : ℝ
hp : p ∈ Ioo 0 1
ht : 0 < t
a : A
ha : 0 ≤ a
⊢ ∀ ⦃b : A⦄, b ∈ Ici 0 → a ≤ b → cfcₙ (p.rpowIntegrand₀₁ t) a ≤ cfcₙ (p.rpowIntegrand₀₁ t) b

Tactic:
b

Goal state after:
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
p t : ℝ
hp : p ∈ Ioo 0 1
ht : 0 < t
a : A
ha : 0 ≤ a
b : A
⊢ b ∈ Ici 0 → a ≤ b → cfcₙ (p.rpowIntegrand₀₁ t) a ≤ cfcₙ (p.rpowIntegrand₀₁ t) b
Module: Mathlib.Analysis.SpecialFunctions.MulExpNegMulSq

Goal state before:
pp: ε x : ℝ
⊢ -ε.mulExpNegMulSq (-x) = ε.mulExpNegMulSq x

Tactic:
simp [mulExpNegMulSq]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Log.Base

Goal state before:
pp: b x : ℝ
b_pos : 0 < b
b_lt_one : b < 1
hx : 0 < x
hx' : x < 1
⊢ x < 1

Tactic:
exact hx'

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Log.Base

Goal state before:
pp: b x : ℝ
b_pos : 0 < b
b_lt_one : b < 1
hx : 0 < x
hx' : x ≤ 1
⊢ x ≤ 1

Tactic:
exact hx'

Goal state after:
Module: Mathlib.MeasureTheory.Integral.BoundedContinuousFunction

Goal state before:
pp: X : Type u_1
inst✝⁸ : MeasurableSpace X
inst✝⁷ : TopologicalSpace X
E : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : OpensMeasurableSpace X
inst✝⁴ : SecondCountableTopology E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : NormedSpace ℝ E
ι : Type u_3
μs : ι → Measure X
inst✝ : ∀ (i : ι), IsProbabilityMeasure (μs i)
f : X →ᵇ E
v : E
i : ι
hi : (fun i ↦ ∫ (x : X), f x ∂μs i) i = v
⊢ ‖(fun i ↦ ∫ (x : X), f x ∂μs i) i‖ ≤ ‖f‖

Tactic:
apply f.norm_integral_le_norm (μs i)

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Pochhammer

Goal state before:
pp: case succ
n : ℕ
ih : MonotoneOn (deriv fun x ↦ Polynomial.eval x (descPochhammer ℝ n)) (Set.Ioi (↑n - 1))
a : ℝ
ha : a ∈ Set.Ioi (↑(n + 1) - 1)
⊢ ∀ ⦃b : ℝ⦄,
    b ∈ Set.Ioi (↑(n + 1) - 1) →
      a ≤ b →
        deriv (fun x ↦ Polynomial.eval x (descPochhammer ℝ (n + 1))) a ≤
          deriv (fun x ↦ Polynomial.eval x (descPochhammer ℝ (n + 1))) b

Tactic:
b

Goal state after:
case succ
n : ℕ
ih : MonotoneOn (deriv fun x ↦ Polynomial.eval x (descPochhammer ℝ n)) (Set.Ioi (↑n - 1))
a : ℝ
ha : a ∈ Set.Ioi (↑(n + 1) - 1)
b : ℝ
⊢ b ∈ Set.Ioi (↑(n + 1) - 1) →
    a ≤ b →
      deriv (fun x ↦ Polynomial.eval x (descPochhammer ℝ (n + 1))) a ≤
        deriv (fun x ↦ Polynomial.eval x (descPochhammer ℝ (n + 1))) b
Module: Mathlib.Analysis.SpecialFunctions.MulExpNegMulSqIntegral

Goal state before:
pp: E : Type u_1
inst✝³ : TopologicalSpace E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
P : Measure E
inst✝ : IsFiniteMeasure P
ε : ℝ
g : E →ᵇ ℝ
hε : 0 < ε
N : ℕ
hgN : ε * (‖g‖ * ‖g‖) < ↑N
n : ℕ
hn : N ≤ n
hnpos : 0 < ↑n
x : E
⊢ |g x| ≤ |‖g‖|

Tactic:
abs_norm

Goal state after:
E : Type u_1
inst✝³ : TopologicalSpace E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
P : Measure E
inst✝ : IsFiniteMeasure P
ε : ℝ
g : E →ᵇ ℝ
hε : 0 < ε
N : ℕ
hgN : ε * (‖g‖ * ‖g‖) < ↑N
n : ℕ
hn : N ≤ n
hnpos : 0 < ↑n
x : E
⊢ |g x| ≤ ‖g‖
Module: Mathlib.MeasureTheory.Integral.BoundedContinuousFunction

Goal state before:
pp: case inr.hinf
X : Type u_1
inst✝⁴ : TopologicalSpace X
inst✝³ : MeasurableSpace X
inst✝² : OpensMeasurableSpace X
ι : Type u_2
L : Filter ι
μ : Measure X
inst✝¹ : IsProbabilityMeasure μ
μs : ι → Measure X
inst✝ : ∀ (i : ι), IsProbabilityMeasure (μs i)
h : ∀ (f : X →ᵇ ℝ), 0 ≤ f → ∫ (x : X), f x ∂μ ≤ liminf (fun i ↦ ∫ (x : X), f x ∂μs i) L
f : X →ᵇ ℝ
hL : L.NeBot
obs : Bornology.IsBounded (Set.range fun i ↦ ∫ (x : X), f x ∂μs i)
bdd_above : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) L fun i ↦ ∫ (x : X), f x ∂μs i
bdd_below : IsBoundedUnder (fun x1 x2 ↦ x2 ≤ x1) L fun i ↦ ∫ (x : X), f x ∂μs i
key : ∫ (x : X), f x ∂μ + ‖f‖ ≤ liminf (fun i ↦ ∫ (x : X), f x ∂μs i + ‖f‖) L
⊢ ∫ (x : X), f x ∂μ ≤ liminf (fun i ↦ ∫ (x : X), f x ∂μs i) L

Tactic:
have := liminf_add_const L (fun i ↦ ∫ x, f x ∂(μs i)) ‖f‖ bdd_above.isCobounded_ge bdd_below

Goal state after:
case inr.hinf
X : Type u_1
inst✝⁴ : TopologicalSpace X
inst✝³ : MeasurableSpace X
inst✝² : OpensMeasurableSpace X
ι : Type u_2
L : Filter ι
μ : Measure X
inst✝¹ : IsProbabilityMeasure μ
μs : ι → Measure X
inst✝ : ∀ (i : ι), IsProbabilityMeasure (μs i)
h : ∀ (f : X →ᵇ ℝ), 0 ≤ f → ∫ (x : X), f x ∂μ ≤ liminf (fun i ↦ ∫ (x : X), f x ∂μs i) L
f : X →ᵇ ℝ
hL : L.NeBot
obs : Bornology.IsBounded (Set.range fun i ↦ ∫ (x : X), f x ∂μs i)
bdd_above : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) L fun i ↦ ∫ (x : X), f x ∂μs i
bdd_below : IsBoundedUnder (fun x1 x2 ↦ x2 ≤ x1) L fun i ↦ ∫ (x : X), f x ∂μs i
key : ∫ (x : X), f x ∂μ + ‖f‖ ≤ liminf (fun i ↦ ∫ (x : X), f x ∂μs i + ‖f‖) L
this : liminf (fun i ↦ ∫ (x : X), f x ∂μs i + ‖f‖) L = liminf (fun i ↦ ∫ (x : X), f x ∂μs i) L + ‖f‖
⊢ ∫ (x : X), f x ∂μ ≤ liminf (fun i ↦ ∫ (x : X), f x ∂μs i) L
Module: Mathlib.MeasureTheory.Constructions.HaarToSphere

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : MeasurableSpace E
μ : Measure E
s : Set ↑(sphere 0 1)
r : ↑(Ioi 0)
⊢ μ ((fun x ↦ ↑((homeomorphUnitSphereProd E).symm x)) '' s ×ˢ Iio r) = μ (image2 (fun a b ↦ a • ↑b) (Ioo 0 ↑r) s)

Tactic:
← image_subtype_val_Ioi_Iio,

Goal state after:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : MeasurableSpace E
μ : Measure E
s : Set ↑(sphere 0 1)
r : ↑(Ioi 0)
⊢ μ ((fun x ↦ ↑((homeomorphUnitSphereProd E).symm x)) '' s ×ˢ Iio r) =
    μ (image2 (fun a b ↦ a • ↑b) (Subtype.val '' Iio r) s)
Module: Mathlib.Analysis.SpecialFunctions.Pow.NthRootLemmas

Goal state before:
pp: n a b : ℕ
hb : b ≠ 0
c : ℕ
hc1 : c ^ (n + 1) ≤ a
hc2 : a < (c + 1) ^ (n + 1)
⊢ ((c ^ (n + 1) / b ^ n + n * b) / (n + 1) + 1) ^ (n + 1) ≤ ((a / b ^ n + n * b) / (n + 1) + 1) ^ (n + 1)

Tactic:
by
      gcongr

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: case e'_5
L : PeriodPair
l : ↥L.lattice
x✝ : ℂ
⊢ 1 / (x✝ - ↑l) ^ 2 - 1 / ↑l ^ 2 = if ↑l = L.ω₁ / 2 then 0 else 1 / (x✝ - ↑l) ^ 2 - 1 / ↑l ^ 2

Tactic:
if_neg

Goal state after:
case e'_5
L : PeriodPair
l : ↥L.lattice
x✝ : ℂ
⊢ 1 / (x✝ - ↑l) ^ 2 - 1 / ↑l ^ 2 = 1 / (x✝ - ↑l) ^ 2 - 1 / ↑l ^ 2

case e'_5.hnc
L : PeriodPair
l : ↥L.lattice
x✝ : ℂ
⊢ ¬↑l = L.ω₁ / 2
Module: Mathlib.Analysis.SpecialFunctions.RegularizedHypergeometric

Goal state before:
pp: n : ℕ
a : Multiset ℂ
hn : n ≠ 0
⊢ (Multiset.map (fun j ↦ ↑n * (j / ↑n + 1)) a).prod = ↑n ^ a.card * (Multiset.map (fun x ↦ x / ↑n + 1) a).prod

Tactic:
simp [Multiset.prod_map_mul]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: case refine_2
L : PeriodPair
l₀ : ℂ
s : Finset ↥L.lattice
l : ℂ
hl : l ∈ (↑L.lattice \ {l₀})ᶜ
⊢ (∑ x ∈ s, if ↑x = l₀ then 0 else -2 / (l - ↑x) ^ 3) =
    deriv (fun x2 ↦ ∑ x ∈ s, if ↑x = l₀ then 0 else 1 / (x2 - ↑x) ^ 2 - 1 / ↑x ^ 2) l

Tactic:
rw [deriv_fun_sum]

Goal state after:
case refine_2
L : PeriodPair
l₀ : ℂ
s : Finset ↥L.lattice
l : ℂ
hl : l ∈ (↑L.lattice \ {l₀})ᶜ
⊢ (∑ x ∈ s, if ↑x = l₀ then 0 else -2 / (l - ↑x) ^ 3) =
    ∑ i ∈ s, deriv (fun x2 ↦ if ↑i = l₀ then 0 else 1 / (x2 - ↑i) ^ 2 - 1 / ↑i ^ 2) l

case refine_2
L : PeriodPair
l₀ : ℂ
s : Finset ↥L.lattice
l : ℂ
hl : l ∈ (↑L.lattice \ {l₀})ᶜ
⊢ ∀ i ∈ s, DifferentiableAt ℂ (fun x2 ↦ if ↑i = l₀ then 0 else 1 / (x2 - ↑i) ^ 2 - 1 / ↑i ^ 2) l
Module: Mathlib.Analysis.SpecialFunctions.RegularizedHypergeometric

Goal state before:
pp: a b : Multiset ℂ
h : a.card ≤ b.card
ha : ∀ j ∈ a, ∀ (k : ℕ), j ≠ -↑k
h₁ : Tendsto (fun n ↦ ↑n ^ (↑a.card - ↑b.card - 1)) atTop (𝓝 0)
this :
  Tendsto
    (fun x ↦
      ‖↑x ^ (↑a.card - ↑b.card - 1) *
          ((Multiset.map (fun x_1 ↦ x_1 / ↑x + 1) a).prod /
            ((Multiset.map (fun x_1 ↦ x_1 / ↑x + 1) b).prod * (1 + (↑x)⁻¹)))‖)
    atTop (𝓝 0)
h_ne : ∀ᶠ (n : ℕ) in atTop, regularizedHGFunCoeff a b n ≠ 0
n : ℕ
⊢ regularizedHGFunCoeff a b n ≠ 0 →
    n ≠ 0 →
      ‖↑n ^ (↑a.card - ↑b.card - 1) *
            ((Multiset.map (fun x ↦ x / ↑n + 1) a).prod /
              ((Multiset.map (fun x ↦ x / ↑n + 1) b).prod * (1 + (↑n)⁻¹)))‖ =
        ‖regularizedHGFunCoeff a b (n + 1)‖ / ‖regularizedHGFunCoeff a b n‖

Tactic:
hn₁

Goal state after:
a b : Multiset ℂ
h : a.card ≤ b.card
ha : ∀ j ∈ a, ∀ (k : ℕ), j ≠ -↑k
h₁ : Tendsto (fun n ↦ ↑n ^ (↑a.card - ↑b.card - 1)) atTop (𝓝 0)
this :
  Tendsto
    (fun x ↦
      ‖↑x ^ (↑a.card - ↑b.card - 1) *
          ((Multiset.map (fun x_1 ↦ x_1 / ↑x + 1) a).prod /
            ((Multiset.map (fun x_1 ↦ x_1 / ↑x + 1) b).prod * (1 + (↑x)⁻¹)))‖)
    atTop (𝓝 0)
h_ne : ∀ᶠ (n : ℕ) in atTop, regularizedHGFunCoeff a b n ≠ 0
n : ℕ
hn₁ : regularizedHGFunCoeff a b n ≠ 0
⊢ n ≠ 0 →
    ‖↑n ^ (↑a.card - ↑b.card - 1) *
          ((Multiset.map (fun x ↦ x / ↑n + 1) a).prod / ((Multiset.map (fun x ↦ x / ↑n + 1) b).prod * (1 + (↑n)⁻¹)))‖ =
      ‖regularizedHGFunCoeff a b (n + 1)‖ / ‖regularizedHGFunCoeff a b n‖
Module: Mathlib.Analysis.SpecialFunctions.RegularizedHypergeometric

Goal state before:
pp: a b : Multiset ℂ
h : a.card = b.card + 1
h' : ∀ j ∈ a, ∀ (k : ℕ), j ≠ -↑k
this :
  Tendsto
    (fun x ↦
      ‖(Multiset.map (fun x_1 ↦ x_1 / ↑x + 1) a).prod /
          ((Multiset.map (fun x_1 ↦ x_1 / ↑x + 1) b).prod * (1 + (↑x)⁻¹))‖)
    atTop (𝓝 1)
h_ne : ∀ᶠ (n : ℕ) in atTop, regularizedHGFunCoeff a b n ≠ 0
n : ℕ
⊢ regularizedHGFunCoeff a b n ≠ 0 →
    n ≠ 0 →
      ‖(Multiset.map (fun x ↦ x / ↑n + 1) a).prod / ((Multiset.map (fun x ↦ x / ↑n + 1) b).prod * (1 + (↑n)⁻¹))‖ =
        ‖regularizedHGFunCoeff a b n.succ‖ / ‖regularizedHGFunCoeff a b n‖

Tactic:
hn₁

Goal state after:
a b : Multiset ℂ
h : a.card = b.card + 1
h' : ∀ j ∈ a, ∀ (k : ℕ), j ≠ -↑k
this :
  Tendsto
    (fun x ↦
      ‖(Multiset.map (fun x_1 ↦ x_1 / ↑x + 1) a).prod /
          ((Multiset.map (fun x_1 ↦ x_1 / ↑x + 1) b).prod * (1 + (↑x)⁻¹))‖)
    atTop (𝓝 1)
h_ne : ∀ᶠ (n : ℕ) in atTop, regularizedHGFunCoeff a b n ≠ 0
n : ℕ
hn₁ : regularizedHGFunCoeff a b n ≠ 0
⊢ n ≠ 0 →
    ‖(Multiset.map (fun x ↦ x / ↑n + 1) a).prod / ((Multiset.map (fun x ↦ x / ↑n + 1) b).prod * (1 + (↑n)⁻¹))‖ =
      ‖regularizedHGFunCoeff a b n.succ‖ / ‖regularizedHGFunCoeff a b n‖
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: case hf
L : PeriodPair
l₀ : ↥L.lattice
z : ℂ
⊢ Summable fun l ↦ if ↑l = ↑l₀ then 0 else -2 / (z - ↑l) ^ 3

Tactic:
exact ⟨_, L.hasSum_derivWeierstrassPExcept _ _⟩

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

Goal state before:
pp: case inr
x : ℝ
h : x ≠ -1
h' : x ≠ 1
⊢ HasDerivWithinAt arcsin (1 / √(1 - x ^ 2)) (Ici x) x

Tactic:
· exact (hasDerivAt_arcsin h h').hasDerivWithinAt

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Stirling

Goal state before:
pp: n : ℕ
r : ℝ := (1 / (2 * (↑n + 1) + 1)) ^ 2
hr : r = (1 / (2 * (↑n + 1) + 1)) ^ 2
hr1 : r < 1
this : HasSum (fun j ↦ r ^ (j + 1) / 3) (1 / (12 * ↑(n + 1) * (↑(n + 1) + 1)))
⊢ log (stirlingSeq (n + 1)) - log (stirlingSeq (n + 1 + 1)) ≤ 1 / (12 * ↑(n + 1) * (↑(n + 1) + 1))

Tactic:
refine hasSum_le (fun j ↦ ?_) (log_stirlingSeq_sdiff_hasSum n) this
    simpa [hr, field] using show (3 : ℝ) ≤ 2 * (j + 1) + 1 by norm_cast; grind

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: L : PeriodPair
l₀ x : ℂ
i : ℕ
hl₀ : l₀ ∈ L.lattice
⊢ ∑' (x_1 : ↥L.lattice), (↑i + 2) * (((↑x_1 - x) ^ (i + 3))⁻¹ - if x_1 = ⟨l₀, hl₀⟩ then (l₀ - x) ^ (-↑(i + 3)) else 0) =
    ∑' (l : ↥L.lattice),
      if ↑l = l₀ then 0 else (↑(i + 1) + 1) * (↑l - x) ^ (-↑(i + 1 + 2)) - Nat.casesOn (i + 1) (↑l ^ (-2)) 0

Tactic:
simp_rw [Subtype.ext_iff, zpow_neg]
          congr with l
          split_ifs with e
          · simp only [e, zpow_natCast, sub_self, mul_zero]
          · dsimp; norm_cast; ring

Goal state after:
Module: Mathlib.NumberTheory.Niven

Goal state before:
pp: case inr.inr.inl
θ : ℝ
hθ : ∃ r, θ = ↑r * π
hcos : ∃ q, cos θ = ↑q
h_bnd : θ ∈ Set.Icc 0 π
h : cos θ = 0
⊢ θ ∈ {0, π / 3, π / 2, π * (2 / 3), π}

Tactic:
have h₂ := cos_pi_div_two

Goal state after:
case inr.inr.inl
θ : ℝ
hθ : ∃ r, θ = ↑r * π
hcos : ∃ q, cos θ = ↑q
h_bnd : θ ∈ Set.Icc 0 π
h : cos θ = 0
h₂ : cos (π / 2) = 0
⊢ θ ∈ {0, π / 3, π / 2, π * (2 / 3), π}
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: case r_le
L : PeriodPair
l₀ x : ℂ
r : NNReal
hr0 : 0 < r
hr : Metric.closedBall x ↑r ⊆ (↑L.lattice \ {l₀})ᶜ
⊢ ↑r ≤ (L.weierstrassPExceptSeries l₀ x).radius

Tactic:
apply FormalMultilinearSeries.le_radius_of_tendsto (l := 0)

Goal state after:
case r_le
L : PeriodPair
l₀ x : ℂ
r : NNReal
hr0 : 0 < r
hr : Metric.closedBall x ↑r ⊆ (↑L.lattice \ {l₀})ᶜ
⊢ Tendsto (fun n ↦ ‖L.weierstrassPExceptSeries l₀ x n‖ * ↑r ^ n) atTop (𝓝 0)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema

Goal state before:
pp: k n : ℕ
hn : n ≠ 0
⊢ eval (cos (↑k * π / ↑n)) (T ℝ ↑n) = ↑↑(↑k).negOnePow

Tactic:
rw [T_real_cos, Int.cast_negOnePow]

Goal state after:
k n : ℕ
hn : n ≠ 0
⊢ cos (↑↑n * (↑k * π / ↑n)) = (-1) ^ ↑k
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: case neg
L : PeriodPair
x : ℂ
hx : x ∉ L.lattice
⊢ MeromorphicAt ℘[L] x

Tactic:
· exact (L.analyticOnNhd_weierstrassP x hx).meromorphicAt

Goal state after:
Module: Mathlib.Analysis.SpecificLimits.ArithmeticGeometric

Goal state before:
pp: R : Type u_1
a b u₀ : R
inst✝⁵ : Field R
inst✝⁴ : LinearOrder R
inst✝³ : IsStrictOrderedRing R
inst✝² : Archimedean R
inst✝¹ : TopologicalSpace R
inst✝ : OrderTopology R
ha_pos : 0 ≤ a
ha : a < 1
| 𝓝 (b / (1 - a))

Tactic:
rw [← zero_add (b / (1 - a))]

Goal state after:
R : Type u_1
a b u₀ : R
inst✝⁵ : Field R
inst✝⁴ : LinearOrder R
inst✝³ : IsStrictOrderedRing R
inst✝² : Archimedean R
inst✝¹ : TopologicalSpace R
inst✝ : OrderTopology R
ha_pos : 0 ≤ a
ha : a < 1
| 𝓝 (0 + b / (1 - a))
Module: Mathlib.Analysis.SpecificLimits.ArithmeticGeometric

Goal state before:
pp: R : Type u_1
a b u₀ : R
inst✝⁵ : Field R
inst✝⁴ : LinearOrder R
inst✝³ : IsStrictOrderedRing R
inst✝² : Archimedean R
inst✝¹ : TopologicalSpace R
inst✝ : OrderTopology R
ha_pos : 0 ≤ a
ha : a < 1
⊢ Tendsto (fun n ↦ a ^ n * (u₀ - b / (1 - a)) + b / (1 - a)) atTop (𝓝 (b / (1 - a)))

Tactic:
conv_rhs => rw [← zero_add (b / (1 - a))]

Goal state after:
R : Type u_1
a b u₀ : R
inst✝⁵ : Field R
inst✝⁴ : LinearOrder R
inst✝³ : IsStrictOrderedRing R
inst✝² : Archimedean R
inst✝¹ : TopologicalSpace R
inst✝ : OrderTopology R
ha_pos : 0 ≤ a
ha : a < 1
⊢ Tendsto (fun n ↦ a ^ n * (u₀ - b / (1 - a)) + b / (1 - a)) atTop (𝓝 (0 + b / (1 - a)))
Module: Mathlib.Tactic.NormNum.Prime

Goal state before:
pp: n k : ℕ
h1 : MinFacHelper n k
h2 : (k * k).ble n = false
⊢ 2 ≤ n ∧ ∀ (m : ℕ), 2 ≤ m → m ≤ n.sqrt → ¬m ∣ n

Tactic:
refine ⟨h1.one_lt, fun m hm hmn h2mn ↦ ?_⟩

Goal state after:
n k : ℕ
h1 : MinFacHelper n k
h2 : (k * k).ble n = false
m : ℕ
hm : 2 ≤ m
hmn : m ≤ n.sqrt
h2mn : m ∣ n
⊢ False
Module: Mathlib.Analysis.SumIntegralComparisons

Goal state before:
pp: a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : MonotoneOn f (Icc ↑a ↑b)
⊢ ∫ (x : ℝ) in ↑a..↑b, -f x ≤ ∑ x ∈ Finset.Ico a b, -f ↑x

Tactic:
exact hf.neg.integral_le_sum_Ico hab

Goal state after:
Module: Mathlib.CategoryTheory.Generator.Abelian

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasLimits C
inst✝ : EnoughInjectives C
G : C
hG : IsSeparator G
this✝ : WellPowered.{v, v, u} C
this : HasProductsOfShape (Subobject (op G)) C
T : C := Injective.under (∏ᶜ fun P ↦ unop (Subobject.underlying.obj P))
X Y : C
f : X ⟶ Y
hf : ∀ (h : Y ⟶ T), f ≫ h = 0
⊢ f = 0

Tactic:
refine (Preadditive.isSeparator_iff _).1 hG _ fun h => ?_

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasLimits C
inst✝ : EnoughInjectives C
G : C
hG : IsSeparator G
this✝ : WellPowered.{v, v, u} C
this : HasProductsOfShape (Subobject (op G)) C
T : C := Injective.under (∏ᶜ fun P ↦ unop (Subobject.underlying.obj P))
X Y : C
f : X ⟶ Y
hf : ∀ (h : Y ⟶ T), f ≫ h = 0
h : G ⟶ X
⊢ h ≫ f = 0