mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.MvPowerSeries.GaussNorm

Goal state before:
pp: case refine_1
R : Type u_1
σ : Type u_2
v : R → ℝ
c : σ → ℝ
inst✝ : Semiring R
f g : MvPowerSeries σ R
hc : 0 ≤ c
vNonneg : ∀ (a : R), v a ≥ 0
vMul : ∀ (a b : R), v (a * b) ≤ v a * v b
vna : IsNonarchimedean v
vZero : v 0 = 0
hbfd : HasGaussNorm v c f
hbgd : HasGaussNorm v c g
t : σ →₀ ℕ
k : (σ →₀ ℕ) × (σ →₀ ℕ)
hk : (Finset.antidiagonal t).Nonempty → k ∈ Finset.antidiagonal t
hsum : v (∑ a ∈ Finset.antidiagonal t, (coeff a.1) f * (coeff a.2) g) ≤ v ((coeff k.1) f * (coeff k.2) g)
hk' : k.1 + k.2 = t
hprod : (t.prod fun x1 x2 ↦ c x1 ^ x2) = (k.1.prod fun x1 x2 ↦ c x1 ^ x2) * k.2.prod fun x1 x2 ↦ c x1 ^ x2
⊢ v ((coeff t) (f * g)) * ((k.1.prod fun x1 x2 ↦ c x1 ^ x2) * k.2.prod fun x1 x2 ↦ c x1 ^ x2) ≤
    gaussNorm v c f * gaussNorm v c g

Tactic:
refine (mul_le_mul hsum (by rfl) (mul_nonneg (c_prod_nonneg c hc k.1) (c_prod_nonneg c hc k.2))
      (vNonneg _)).trans ?_

Goal state after:
case refine_1
R : Type u_1
σ : Type u_2
v : R → ℝ
c : σ → ℝ
inst✝ : Semiring R
f g : MvPowerSeries σ R
hc : 0 ≤ c
vNonneg : ∀ (a : R), v a ≥ 0
vMul : ∀ (a b : R), v (a * b) ≤ v a * v b
vna : IsNonarchimedean v
vZero : v 0 = 0
hbfd : HasGaussNorm v c f
hbgd : HasGaussNorm v c g
t : σ →₀ ℕ
k : (σ →₀ ℕ) × (σ →₀ ℕ)
hk : (Finset.antidiagonal t).Nonempty → k ∈ Finset.antidiagonal t
hsum : v (∑ a ∈ Finset.antidiagonal t, (coeff a.1) f * (coeff a.2) g) ≤ v ((coeff k.1) f * (coeff k.2) g)
hk' : k.1 + k.2 = t
hprod : (t.prod fun x1 x2 ↦ c x1 ^ x2) = (k.1.prod fun x1 x2 ↦ c x1 ^ x2) * k.2.prod fun x1 x2 ↦ c x1 ^ x2
⊢ v ((coeff k.1) f * (coeff k.2) g) * ((k.1.prod fun x1 x2 ↦ c x1 ^ x2) * k.2.prod fun x1 x2 ↦ c x1 ^ x2) ≤
    gaussNorm v c f * gaussNorm v c g
Module: Mathlib.RingTheory.MvPowerSeries.GaussNorm

Goal state before:
pp: case neg.left
R : Type u_1
σ : Type u_2
v : R → ℝ
c : σ → ℝ
inst✝¹ : Ring R
inst✝ : DecidableEq σ
f g : MvPowerSeries σ R
hf : HasGaussNorm v c f
hg : HasGaussNorm v c g
hfg : HasGaussNorm v c (f * g)
vNonneg : ∀ (a : R), v a ≥ 0
vZero : v 0 = 0
vNA : IsNonarchimedean v
vMulEq : ∀ (a b : R), v (a * b) = v a * v b
vNeg : ∀ (a : R), v (-a) = v a
h_eq_zero : ∀ (x : R), v x = 0 → x = 0
hc : ∀ (i : σ), 0 < c i
hdom :
  ∃ i j,
    AchievesGaussNorm v c f i ∧
      AchievesGaussNorm v c g j ∧
        ∀ p ∈ Finset.antidiagonal (i + j),
          p ≠ (i, j) → v ((coeff p.1) f * (coeff p.2) g) < v ((coeff i) f) * v ((coeff j) g)
hf' : ¬f = 0
hg' : ¬g = 0
hf1 : gaussNorm v c f ≠ 0
hg1 : gaussNorm v c g ≠ 0
⊢ gaussNorm v c f * gaussNorm v c g ≤ gaussNorm v c (f * g)

pp: case neg.right
R : Type u_1
σ : Type u_2
v : R → ℝ
c : σ → ℝ
inst✝¹ : Ring R
inst✝ : DecidableEq σ
f g : MvPowerSeries σ R
hf : HasGaussNorm v c f
hg : HasGaussNorm v c g
hfg : HasGaussNorm v c (f * g)
vNonneg : ∀ (a : R), v a ≥ 0
vZero : v 0 = 0
vNA : IsNonarchimedean v
vMulEq : ∀ (a b : R), v (a * b) = v a * v b
vNeg : ∀ (a : R), v (-a) = v a
h_eq_zero : ∀ (x : R), v x = 0 → x = 0
hc : ∀ (i : σ), 0 < c i
hdom :
  ∃ i j,
    AchievesGaussNorm v c f i ∧
      AchievesGaussNorm v c g j ∧
        ∀ p ∈ Finset.antidiagonal (i + j),
          p ≠ (i, j) → v ((coeff p.1) f * (coeff p.2) g) < v ((coeff i) f) * v ((coeff j) g)
hf' : ¬f = 0
hg' : ¬g = 0
hf1 : gaussNorm v c f ≠ 0
hg1 : gaussNorm v c g ≠ 0
⊢ gaussNorm v c (f * g) ≤ gaussNorm v c f * gaussNorm v c g

Tactic:
· exact gaussNorm_le_mul v c f g vMulEq vNA (by grind) hfg hdom

Goal state after:
case neg.right
R : Type u_1
σ : Type u_2
v : R → ℝ
c : σ → ℝ
inst✝¹ : Ring R
inst✝ : DecidableEq σ
f g : MvPowerSeries σ R
hf : HasGaussNorm v c f
hg : HasGaussNorm v c g
hfg : HasGaussNorm v c (f * g)
vNonneg : ∀ (a : R), v a ≥ 0
vZero : v 0 = 0
vNA : IsNonarchimedean v
vMulEq : ∀ (a b : R), v (a * b) = v a * v b
vNeg : ∀ (a : R), v (-a) = v a
h_eq_zero : ∀ (x : R), v x = 0 → x = 0
hc : ∀ (i : σ), 0 < c i
hdom :
  ∃ i j,
    AchievesGaussNorm v c f i ∧
      AchievesGaussNorm v c g j ∧
        ∀ p ∈ Finset.antidiagonal (i + j),
          p ≠ (i, j) → v ((coeff p.1) f * (coeff p.2) g) < v ((coeff i) f) * v ((coeff j) g)
hf' : ¬f = 0
hg' : ¬g = 0
hf1 : gaussNorm v c f ≠ 0
hg1 : gaussNorm v c g ≠ 0
⊢ gaussNorm v c (f * g) ≤ gaussNorm v c f * gaussNorm v c g
Module: Mathlib.Analysis.Real.OfDigits

Goal state before:
pp: b : ℕ
x y : ℕ → Fin b
n : ℕ
hxy : ∀ i < n, x i = y i
⊢ |ofDigits x - ofDigits y| ≤ (↑b ^ n)⁻¹

Tactic:
by
  rw [ofDigits_eq_sum_add_ofDigits x n, ofDigits_eq_sum_add_ofDigits y n]
  have : ∑ i ∈ Finset.range n, ofDigitsTerm x i = ∑ i ∈ Finset.range n, ofDigitsTerm y i :=
    Finset.sum_congr rfl fun i hi ↦ by simp [ofDigitsTerm, hxy i (Finset.mem_range.mp hi)]
  rw [this, add_sub_add_left_eq_sub, ← mul_sub, abs_mul, abs_of_nonneg (by positivity)]
  apply mul_le_of_le_one_right (by positivity)
  convert!
    abs_sub_le_of_le_of_le (ofDigits_nonneg _) (ofDigits_le_one _) (ofDigits_nonneg _)
      (ofDigits_le_one _)
  simp

Goal state after:
Module: Mathlib.Analysis.Real.Pi.Bounds

Goal state before:
pp: c d a b n : ℕ
z : ℝ
hz : (↑c / ↑d).sqrtTwoAddSeries n ≤ z
hb : 0 < b
hd : 0 < d
h : (2 * b + a) * d ^ 2 ≤ c ^ 2 * b
hb' : 0 < ↑b
⊢ √(2 + ↑a / ↑b) ≤ ↑c / ↑d

Tactic:
have hd' : 0 < (d : ℝ) := Nat.cast_pos.2 hd

Goal state after:
c d a b n : ℕ
z : ℝ
hz : (↑c / ↑d).sqrtTwoAddSeries n ≤ z
hb : 0 < b
hd : 0 < d
h : (2 * b + a) * d ^ 2 ≤ c ^ 2 * b
hb' : 0 < ↑b
hd' : 0 < ↑d
⊢ √(2 + ↑a / ↑b) ≤ ↑c / ↑d
Module: Mathlib.Analysis.Real.Pi.Bounds

Goal state before:
pp: a b c d n : ℕ
z : ℝ
hz : z ≤ (↑a / ↑b).sqrtTwoAddSeries n
hb : 0 < b
hd : 0 < d
h : a ^ 2 * d ≤ (2 * d + c) * b ^ 2
hb' : 0 < ↑b
⊢ (↑a / ↑b) ^ 2 ≤ 2 + ↑c / ↑d

Tactic:
have hd' : 0 < (d : ℝ) := Nat.cast_pos.2 hd

Goal state after:
a b c d n : ℕ
z : ℝ
hz : z ≤ (↑a / ↑b).sqrtTwoAddSeries n
hb : 0 < b
hd : 0 < d
h : a ^ 2 * d ≤ (2 * d + c) * b ^ 2
hb' : 0 < ↑b
hd' : 0 < ↑d
⊢ (↑a / ↑b) ^ 2 ≤ 2 + ↑c / ↑d
Module: Mathlib.Data.Rat.Sqrt

Goal state before:
pp: m : ℚ
⊢ IsSquare m ↔ sqrt m * sqrt m = m

Tactic:
by
    simp_rw [← exists_mul_self m, IsSquare, eq_comm]

Goal state after:
Module: Mathlib.Analysis.Polynomial.MahlerMeasure

Goal state before:
pp: p : ℂ[X]
⊢ p.supNorm ≤ ↑(p.natDegree.choose (p.natDegree / 2)) * p.mahlerMeasure

Tactic:
obtain ⟨i, hi⟩ := p.exists_eq_supNorm

Goal state after:
p : ℂ[X]
i : ℕ
hi : p.supNorm = ‖p.coeff i‖
⊢ p.supNorm ≤ ↑(p.natDegree.choose (p.natDegree / 2)) * p.mahlerMeasure
Module: Mathlib.Analysis.Polynomial.MahlerMeasure

Goal state before:
pp: p : ℂ[X]
i : ℕ
hi : p.supNorm = ‖p.coeff i‖
⊢ ↑(p.natDegree.choose i) ≤ ↑(p.natDegree.choose (p.natDegree / 2))

Tactic:
by exact_mod_cast Nat.choose_le_middle i p.natDegree

Goal state after:
Module: Mathlib.NumberTheory.Real.Irrational

Goal state before:
pp: case inr
q : ℚ
hq : q < 0
⊢ Irrational √↑q ↔ ¬IsSquare q ∧ 0 ≤ q

Tactic:
rw [sqrt_eq_zero_of_nonpos (Rat.cast_nonpos.2 hq.le)]
    simp_rw [not_irrational_zero, false_iff, not_and, not_le, hq, implies_true]

Goal state after:
Module: Mathlib.NumberTheory.Real.Irrational

Goal state before:
pp: x y : ℝ
⊢ Irrational (x * y) → Irrational x ∨ Irrational y

Tactic:
delta Irrational
  contrapose!
  rintro ⟨⟨rx, rfl⟩, ⟨ry, rfl⟩⟩
  exact ⟨rx * ry, cast_mul rx ry⟩

Goal state after:
Module: Mathlib.Analysis.Real.Hyperreal

Goal state before:
pp: x : ℝ*
⊢ x.Infinite ↔ ArchimedeanClass.mk x < 0

Tactic:
Infinite,

Goal state after:
x : ℝ*
⊢ x.InfinitePos ∨ x.InfiniteNeg ↔ ArchimedeanClass.mk x < 0
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arctan

Goal state before:
pp: case inr
z : ℂ
h₁ : -(π / 2) < z.re
h₂ : z.re ≤ π / 2
k : ℤ
ni : ¬z.im = 0
⊢ ¬z.re = ↑(2 * k + 1) * π / 2 ∨ ¬z.im = 0

Tactic:
exact Or.inr ni

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

Goal state before:
pp: x y : ℝ≥0
⊢ x.agm y = ⨆ n, (x.agmSequences y n).1

Tactic:
refine tendsto_nhds_unique (tendsto_agmSequences_snd_agm.congr_dist ?_)
    (tendsto_atTop_ciSup agmSequences_fst_monotone bddAbove_range_agmSequences_fst)

Goal state after:
x y : ℝ≥0
⊢ Tendsto (fun x_1 ↦ dist (x.agmSequences y x_1).2 (x.agmSequences y x_1).1) atTop (𝓝 0)
Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy

Goal state before:
pp: case inl
p : ℝ
h : p ≠ 0 ∧ p ≠ 1
hp₀ : p < 0
⊢ binEntropy p ≠ 0

pp: case inr
p : ℝ
h : p ≠ 0 ∧ p ≠ 1
hp₀ : 0 < p
⊢ binEntropy p ≠ 0

Tactic:
· exact (binEntropy_neg_of_neg hp₀).ne

Goal state after:
case inr
p : ℝ
h : p ≠ 0 ∧ p ≠ 1
hp₀ : 0 < p
⊢ binEntropy p ≠ 0
Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy

Goal state before:
pp: q : ℕ
qLe2 : 2 ≤ q
p1 : ℝ
hp1 : p1 ∈ Icc 0 (1 - 1 / ↑q)
p2 : ℝ
hp2 : p2 ∈ Icc 0 (1 - 1 / ↑q)
p1le2 : p1 < p2
p : ℝ
hp : p ∈ interior (Icc 0 (1 - 1 / ↑q))
this : 2 ≤ ↑q
zero_le_qinv : 0 < (↑q)⁻¹
⊢ 0 < 1 - p

Tactic:
simp only [sub_pos]

Goal state after:
q : ℕ
qLe2 : 2 ≤ q
p1 : ℝ
hp1 : p1 ∈ Icc 0 (1 - 1 / ↑q)
p2 : ℝ
hp2 : p2 ∈ Icc 0 (1 - 1 / ↑q)
p1le2 : p1 < p2
p : ℝ
hp : p ∈ interior (Icc 0 (1 - 1 / ↑q))
this : 2 ≤ ↑q
zero_le_qinv : 0 < (↑q)⁻¹
⊢ p < 1
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.ConjSqrt

Goal state before:
pp: A : Type u_1
inst✝¹⁰ : PartialOrder A
inst✝⁹ : Ring A
inst✝⁸ : StarRing A
inst✝⁷ : TopologicalSpace A
inst✝⁶ : StarOrderedRing A
inst✝⁵ : Algebra ℝ A
inst✝⁴ : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝³ : NonnegSpectrumClass ℝ A
inst✝² : SeparatelyContinuousMul A
inst✝¹ : IsSemitopologicalRing A
inst✝ : T2Space A
c a : A
hc : IsStrictlyPositive c
hc' : IsSelfAdjoint (sqrt c)
⊢ IsStrictlyPositive ((conjSqrt c) a) ↔ IsStrictlyPositive a

Tactic:
conjSqrt_apply

Goal state after:
A : Type u_1
inst✝¹⁰ : PartialOrder A
inst✝⁹ : Ring A
inst✝⁸ : StarRing A
inst✝⁷ : TopologicalSpace A
inst✝⁶ : StarOrderedRing A
inst✝⁵ : Algebra ℝ A
inst✝⁴ : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝³ : NonnegSpectrumClass ℝ A
inst✝² : SeparatelyContinuousMul A
inst✝¹ : IsSemitopologicalRing A
inst✝ : T2Space A
c a : A
hc : IsStrictlyPositive c
hc' : IsSelfAdjoint (sqrt c)
⊢ IsStrictlyPositive (sqrt c * a * sqrt c) ↔ IsStrictlyPositive a
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation

Goal state before:
pp: p t x : ℝ
hp : p ∈ Ioo 0 1
ht : 0 ≤ t
hx : 0 ≤ x
hxt : 0 ≤ x * t
⊢ p.rpowIntegrand₀₁ (x * t) x = p.rpowIntegrand₀₁ t 1 * x ^ (p - 1)

Tactic:
rpowIntegrand₀₁_eq_pow_div hp hxt hx,

Goal state after:
p t x : ℝ
hp : p ∈ Ioo 0 1
ht : 0 ≤ t
hx : 0 ≤ x
hxt : 0 ≤ x * t
⊢ (x * t) ^ (p - 1) * x / (x * t + x) = p.rpowIntegrand₀₁ t 1 * x ^ (p - 1)
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Deligne

Goal state before:
pp: ⊢ Differentiable ℂ fun s ↦ 2 * (2 * ↑π) ^ (-s)

Tactic:
exact (differentiable_neg.const_cpow (by simp)).const_mul _

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

Goal state before:
pp: case refine_2
p : ℝ
hp : p ∈ Ioo 0 1
C : ℝ≥0 := NNReal.mk (∫ (t : ℝ) in Ioi 0, p.rpowIntegrand₀₁ t 1)⁻¹ ⋯
x : ℝ
hx : x ∈ Ici 0
⊢ (∫ (t : ℝ) in Ioi 0, p.rpowIntegrand₀₁ t 1)⁻¹ * ∫ (t : ℝ) in Ioi 0, p.rpowIntegrand₀₁ t x =
    ↑(NNReal.mk (∫ (t : ℝ) in Ioi 0, p.rpowIntegrand₀₁ t 1)⁻¹ ⋯) • ∫ (t : ℝ) in Ioi 0, p.rpowIntegrand₀₁ t x ∂volume

Tactic:
NNReal.coe_mk,

Goal state after:
case refine_2
p : ℝ
hp : p ∈ Ioo 0 1
C : ℝ≥0 := NNReal.mk (∫ (t : ℝ) in Ioi 0, p.rpowIntegrand₀₁ t 1)⁻¹ ⋯
x : ℝ
hx : x ∈ Ici 0
⊢ (∫ (t : ℝ) in Ioi 0, p.rpowIntegrand₀₁ t 1)⁻¹ * ∫ (t : ℝ) in Ioi 0, p.rpowIntegrand₀₁ t x =
    (∫ (t : ℝ) in Ioi 0, p.rpowIntegrand₀₁ t 1)⁻¹ • ∫ (t : ℝ) in Ioi 0, p.rpowIntegrand₀₁ t x ∂volume
Module: Mathlib.Analysis.SpecialFunctions.Gaussian.PoissonSummation

Goal state before:
pp: a : ℂ
ha : 0 < a.re
s : ℝ
⊢ (fun x ↦ cexp (-a * ↑x ^ 2)) = fun x ↦ cexp (-a * ↑x ^ 2 + 0 * ↑x)

Tactic:
simp_rw [zero_mul, add_zero]

Goal state after:
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 ^ ↑(Nat.log b ⌊r⌋₊) ≤ r

Tactic:
rw [zpow_natCast, ← Nat.cast_pow, ← Nat.le_floor_iff hr.le]

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.NumberTheory.Harmonic.GammaDeriv

Goal state before:
pp: f : ℂ → ℂ := fun s ↦ ↑π ^ (-s / 2)
g : ℂ → ℂ := fun s ↦ Gamma (s / 2)
aux : ↑π ^ (1 / 2) = ↑√π
aux2 : ↑√π ≠ 0
hf : HasDerivAt f (-log ↑π / 2 / ↑√π) 1
hg : HasDerivAt g (-↑√π * (↑γ + 2 * log 2) / 2) 1
⊢ -(↑γ + (↑(2 * Real.log 2) + ↑(Real.log π))) / ↑2 = -(↑γ + log (4 * ↑π)) / ↑2

Tactic:
← Nat.cast_ofNat (R := ℝ),

Goal state after:
f : ℂ → ℂ := fun s ↦ ↑π ^ (-s / 2)
g : ℂ → ℂ := fun s ↦ Gamma (s / 2)
aux : ↑π ^ (1 / 2) = ↑√π
aux2 : ↑√π ≠ 0
hf : HasDerivAt f (-log ↑π / 2 / ↑√π) 1
hg : HasDerivAt g (-↑√π * (↑γ + 2 * log 2) / 2) 1
⊢ -(↑γ + (↑(↑2 * Real.log ↑2) + ↑(Real.log π))) / ↑↑2 = -(↑γ + log (4 * ↑π)) / ↑↑2
Module: Mathlib.Analysis.SpecialFunctions.Log.Base

Goal state before:
pp: a b : ℝ
⊢ (logb a b)⁻¹ = logb b a

Tactic:
simp_rw [logb, inv_div]

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

Goal state before:
pp: case cons
b : ℝ
α : Type u_1
f : α → ℝ
a✝¹ : α
s✝ : Finset α
h✝ : a✝¹ ∉ s✝
a✝ : (∀ x ∈ s✝, f x ≠ 0) → logb b (∏ i ∈ s✝, f i) = ∑ i ∈ s✝, logb b (f i)
hf : ∀ x ∈ Finset.cons a✝¹ s✝ h✝, f x ≠ 0
⊢ logb b (∏ i ∈ Finset.cons a✝¹ s✝ h✝, f i) = ∑ i ∈ Finset.cons a✝¹ s✝ h✝, logb b (f i)

Tactic:
| cons =>

Goal state after:
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 →ᵇ ℝ
u : ℕ → ℝ
hu : Tendsto u atTop (𝓝[>] 0)
⊢ Tendsto ((fun ε ↦ ∫ (x : E), ε.mulExpNegMulSq (g x) ∂P) ∘ u) atTop (𝓝 (∫ (x : E), g x ∂P))

Tactic:
obtain ⟨N, hupos⟩ := eventually_atTop.mp (tendsto_nhdsWithin_iff.mp hu).2

Goal state after:
E : Type u_1
inst✝³ : TopologicalSpace E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
P : Measure E
inst✝ : IsFiniteMeasure P
g : E →ᵇ ℝ
u : ℕ → ℝ
hu : Tendsto u atTop (𝓝[>] 0)
N : ℕ
hupos : ∀ (b : ℕ), N ≤ b → u b ∈ Set.Ioi 0
⊢ Tendsto ((fun ε ↦ ∫ (x : E), ε.mulExpNegMulSq (g x) ∂P) ∘ u) atTop (𝓝 (∫ (x : E), g x ∂P))
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: L : PeriodPair
f : ↥L.lattice → ℂ → ℂ
u : ℝ → ↥L.lattice → ℝ
hu : ∀ r > 0, Summable (u r)
hf : ∀ r > 0, ∀ᶠ (R : ℝ) in atTop, ∀ (x : ℂ), ‖x‖ < r → ∀ (l : ↥L.lattice), ‖↑l‖ = R → ‖f l x‖ ≤ u r l
⊢ HasSumLocallyUniformly f fun x ↦ ∑' (j : ↥L.lattice), f j x

Tactic:
by
  rw [hasSumLocallyUniformly_iff_tendstoLocallyUniformly, tendstoLocallyUniformly_iff_filter]
  intro x
  obtain ⟨r, hr, hr'⟩ : ∃ r, 0 < r ∧ 𝓝 x ≤ 𝓟 (Metric.ball 0 r) :=
    ⟨‖x‖ + 1, by positivity, Filter.le_principal_iff.mpr (Metric.isOpen_ball.mem_nhds (by simp))⟩
  refine .mono_right ?_ hr'
  rw [← tendstoUniformlyOn_iff_tendstoUniformlyOnFilter]
  refine tendstoUniformlyOn_tsum_of_cofinite_eventually (hu r hr) ?_
  obtain ⟨R, hR⟩ := eventually_atTop.mp (hf r hr)
  refine (isCompact_iff_finite.mp (isCompact_closedBall (0 : L.lattice) R)).subset ?_
  intros l hl
  obtain ⟨s, hs, hs'⟩ : ∃ x, ‖x‖ < r ∧ u r l < ‖f l x‖ := by simpa using hl
  simp only [Metric.mem_closedBall, dist_zero_right]
  contrapose! hs'
  exact hR _ hs'.le _ hs _ rfl

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

Goal state before:
pp: a b : Multiset ℂ
h : ∀ j ∈ a, ∀ (k : ℕ), j ≠ -↑k
⊢ ∀ᶠ (n : ℕ) in atTop, regularizedHGFunCoeff a b n ≠ 0

Tactic:
rw [Filter.eventually_atTop]

Goal state after:
a b : Multiset ℂ
h : ∀ j ∈ a, ∀ (k : ℕ), j ≠ -↑k
⊢ ∃ a_1, ∀ (b_1 : ℕ), a_1 ≤ b_1 → regularizedHGFunCoeff a b b_1 ≠ 0
Module: Mathlib.Analysis.SpecialFunctions.RegularizedHypergeometric

Goal state before:
pp: a : Multiset ℂ
⊢ Tendsto (fun n ↦ (Multiset.map (fun x ↦ x / ↑n + 1) a).prod) atTop (𝓝 1)

Tactic:
suffices ∀ i ∈ a, Tendsto (fun n : ℕ ↦ (i / n + 1)) atTop (𝓝 <| (fun _ : _ ↦ 1) i) by
    simpa using tendsto_multiset_prod _ this

Goal state after:
a : Multiset ℂ
⊢ ∀ i ∈ a, Tendsto (fun n ↦ i / ↑n + 1) atTop (𝓝 ((fun x ↦ 1) i))
Module: Mathlib.Analysis.SpecialFunctions.RegularizedHypergeometric

Goal state before:
pp: case neg
a b : Multiset ℂ
h : a.card = b.card + 1
j : ℂ
hj : j ∈ a
k : ℕ
h' : j = -↑k
⊢ 1 ≤ (regularizedHGFunSeries a b).radius

Tactic:
rw [radius_regularizedHGFunSeries_eq_top_of_finite hj h']

Goal state after:
case neg
a b : Multiset ℂ
h : a.card = b.card + 1
j : ℂ
hj : j ∈ a
k : ℕ
h' : j = -↑k
⊢ 1 ≤ ⊤
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.InverseDeriv

Goal state before:
pp: case inr.inl
x : ℝ
h₁✝ : x ≠ -1
h₂✝ : x ≠ 1
h₁ : -1 < x
h₂ : x < 1
⊢ HasStrictDerivAt arcsin (1 / √(1 - x ^ 2)) x ∧ ContDiffAt ℝ ω arcsin x

pp: case inr.inr
x : ℝ
h₁✝ : x ≠ -1
h₂✝ : x ≠ 1
h₁ : -1 < x
h₂ : 1 < x
⊢ HasStrictDerivAt arcsin (1 / √(1 - x ^ 2)) x ∧ ContDiffAt ℝ ω arcsin x

Tactic:
· have : 0 < √(1 - x ^ 2) := sqrt_pos.2 (by nlinarith [h₁, h₂])
    simp only [← cos_arcsin, one_div] at this ⊢
    exact ⟨sinPartialHomeomorph.hasStrictDerivAt_symm ⟨h₁, h₂⟩ this.ne' (hasStrictDerivAt_sin _),
      sinPartialHomeomorph.contDiffAt_symm_deriv this.ne' ⟨h₁, h₂⟩ (hasDerivAt_sin _)
        contDiff_sin.contDiffAt⟩

Goal state after:
case inr.inr
x : ℝ
h₁✝ : x ≠ -1
h₂✝ : x ≠ 1
h₁ : -1 < x
h₂ : 1 < x
⊢ HasStrictDerivAt arcsin (1 / √(1 - x ^ 2)) x ∧ ContDiffAt ℝ ω arcsin x
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

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

Tactic:
tsum_ite_eq,

Goal state after:
L : PeriodPair
l₀ x : ℂ
i : ℕ
hl₀ : l₀ ∈ L.lattice
⊢ (if i + 1 = 0 then ℘[L - l₀] x else (↑(i + 1) + 1) * (L.sumInvPow x (i + 1 + 2) - ((l₀ - x) ^ (i + 1 + 2))⁻¹)) =
    (↑i + 2) * (L.sumInvPow x (i + 3) - (l₀ - x) ^ (-↑(i + 3)))
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.ChebyshevGauss

Goal state before:
pp: case inr
n : ℕ
k : ℤ
hk : ¬2 * ↑n ∣ k
hn : n ≠ 0
⊢ ∑ i ∈ range n, 2 * Complex.cos (↑k * ((2 * ↑i + 1) / (2 * ↑n) * ↑π)) = 0

Tactic:
Complex.two_cos,

Goal state after:
case inr
n : ℕ
k : ℤ
hk : ¬2 * ↑n ∣ k
hn : n ≠ 0
⊢ ∑ x ∈ range n,
      (Complex.exp (↑k * ((2 * ↑x + 1) / (2 * ↑n) * ↑π) * I) +
        Complex.exp (-(↑k * ((2 * ↑x + 1) / (2 * ↑n) * ↑π)) * I)) =
    0
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal

Goal state before:
pp: n : ℕ
P : ℝ[X]
hn : 2 ≤ n
hPdeg : P.degree ≤ ↑n
hPbnd : ∀ x ∈ Set.Icc (-1) 1, |eval x P| ≤ 1
hP : P.leadingCoeff = 2 ^ (n - 1)
⊢ P.degree ≠ ⊥

Tactic:
contrapose! hP
    rw [degree_eq_bot.mp hP, leadingCoeff_zero]
    positivity

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

Goal state before:
pp: L : PeriodPair
z x : ℂ
hx : ∀ (l : ↥L.lattice), ‖z - x‖ < ‖↑l - x‖
⊢ HasSum (fun i ↦ (L.weierstrassPExceptSeries (L.ω₁ / 2) x).coeff i * (z - x) ^ i) (℘[L - L.ω₁ / 2] z)

Tactic:
exact L.weierstrassPExceptSeries_hasSum _ z x fun l hl ↦ hx l

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

Goal state before:
pp: k d : ℕ
z : ℂ
hz : z ∈ ℂ_ℤ
⊢ iteratedDeriv k ((fun z ↦ 1 / (z - (↑d + 1))) + fun z ↦ 1 / (z + (↑d + 1))) z =
    (fun z ↦ (-1) ^ k * ↑k ! * ((z + (↑d + 1)) ^ (-1 - ↑k) + (z - (↑d + 1)) ^ (-1 - ↑k))) z

Tactic:
iteratedDeriv_add

Goal state after:
k d : ℕ
z : ℂ
hz : z ∈ ℂ_ℤ
⊢ iteratedDeriv k (fun z ↦ 1 / (z - (↑d + 1))) z + iteratedDeriv k (fun z ↦ 1 / (z + (↑d + 1))) z =
    (fun z ↦ (-1) ^ k * ↑k ! * ((z + (↑d + 1)) ^ (-1 - ↑k) + (z - (↑d + 1)) ^ (-1 - ↑k))) z

case hf
k d : ℕ
z : ℂ
hz : z ∈ ℂ_ℤ
⊢ ContDiffAt ℂ (↑k) (fun z ↦ 1 / (z - (↑d + 1))) z

case hg
k d : ℕ
z : ℂ
hz : z ∈ ℂ_ℤ
⊢ ContDiffAt ℂ (↑k) (fun z ↦ 1 / (z + (↑d + 1))) z
Module: Mathlib.Analysis.SumIntegralExpDecay

Goal state before:
pp: k : ℕ
M c : ℝ
hM : 0 ≤ M
hc : 0 < c
hk : 0 < ↑k + 1
key : ∫ (t : ℝ) in Ioi 0, t ^ (↑k + 1 - 1) * rexp (-(c * t)) = (1 / c) ^ (↑k + 1) * Gamma (↑k + 1)
hint : IntegrableOn (fun x ↦ x ^ (↑k + 1 - 1) * rexp (-(c * x))) (Ioi 0) volume
⊢ ∫ (x : ℝ) in Ioc 0 M, x ^ (↑k + 1 - 1) * rexp (-(c * x)) ≤ ∫ (x : ℝ) in Ioi 0, x ^ (↑k + 1 - 1) * rexp (-(c * x))

Tactic:
apply setIntegral_mono_set hint _ Ioc_subset_Ioi_self.eventuallyLE

Goal state after:
k : ℕ
M c : ℝ
hM : 0 ≤ M
hc : 0 < c
hk : 0 < ↑k + 1
key : ∫ (t : ℝ) in Ioi 0, t ^ (↑k + 1 - 1) * rexp (-(c * t)) = (1 / c) ^ (↑k + 1) * Gamma (↑k + 1)
hint : IntegrableOn (fun x ↦ x ^ (↑k + 1 - 1) * rexp (-(c * x))) (Ioi 0) volume
⊢ 0 ≤ᵐ[volume.restrict (Ioi 0)] fun x ↦ x ^ (↑k + 1 - 1) * rexp (-(c * x))
Module: Mathlib.Analysis.SumIntegralComparisons

Goal state before:
pp: x₀ : ℝ
a : ℕ
f : ℝ → ℝ
hf : AntitoneOn f (Icc x₀ (x₀ + ↑a))
k : ℕ
hk : k + 1 ≤ a
⊢ uIcc (x₀ + ↑k) (x₀ + ↑(k + 1)) ⊆ Icc x₀ (x₀ + ↑a)

Tactic:
rw [uIcc_of_le (by simp)]

Goal state after:
x₀ : ℝ
a : ℕ
f : ℝ → ℝ
hf : AntitoneOn f (Icc x₀ (x₀ + ↑a))
k : ℕ
hk : k + 1 ≤ a
⊢ Icc (x₀ + ↑k) (x₀ + ↑(k + 1)) ⊆ Icc x₀ (x₀ + ↑a)
Module: Mathlib.Analysis.SpecificLimits.FloorPow

Goal state before:
pp: u : ℕ → ℝ
l : ℝ
hmono : Monotone u
hlim :
  ∀ (a : ℝ),
    1 < a →
      ∃ c,
        (∀ᶠ (n : ℕ) in atTop, ↑(c (n + 1)) ≤ a * ↑(c n)) ∧
          Tendsto c atTop atTop ∧ Tendsto (fun n ↦ u (c n) / ↑(c n)) atTop (𝓝 l)
lnonneg : 0 ≤ l
A : ∀ (ε : ℝ), 0 < ε → ∀ᶠ (n : ℕ) in atTop, u n - ↑n * l ≤ ε * (1 + ε + l) * ↑n
ε : ℝ
εpos : 0 < ε
c : ℕ → ℕ
cgrowth : ∀ᶠ (n : ℕ) in atTop, ↑(c (n + 1)) ≤ (1 + ε) * ↑(c n)
ctop : Tendsto c atTop atTop
clim : Tendsto (fun n ↦ u (c n) / ↑(c n)) atTop (𝓝 l)
⊢ ∀ᶠ (n : ℕ) in atTop, ↑n * l - u n ≤ ε * (1 + l) * ↑n

Tactic:
have L : ∀ᶠ n : ℕ in atTop, (c n : ℝ) * l - u (c n) ≤ ε * c n := by
      rw [← tendsto_sub_nhds_zero_iff, ← Asymptotics.isLittleO_one_iff ℝ,
        Asymptotics.isLittleO_iff] at clim
      filter_upwards [clim εpos, ctop (Ioi_mem_atTop 0)] with n hn cnpos'
      have cnpos : 0 < c n := cnpos'
      calc
        (c n : ℝ) * l - u (c n) = -(u (c n) / c n - l) * c n := by field
        _ ≤ ε * c n := by
          gcongr
          refine le_trans (neg_le_abs _) ?_
          simpa using hn

Goal state after:
u : ℕ → ℝ
l : ℝ
hmono : Monotone u
hlim :
  ∀ (a : ℝ),
    1 < a →
      ∃ c,
        (∀ᶠ (n : ℕ) in atTop, ↑(c (n + 1)) ≤ a * ↑(c n)) ∧
          Tendsto c atTop atTop ∧ Tendsto (fun n ↦ u (c n) / ↑(c n)) atTop (𝓝 l)
lnonneg : 0 ≤ l
A : ∀ (ε : ℝ), 0 < ε → ∀ᶠ (n : ℕ) in atTop, u n - ↑n * l ≤ ε * (1 + ε + l) * ↑n
ε : ℝ
εpos : 0 < ε
c : ℕ → ℕ
cgrowth : ∀ᶠ (n : ℕ) in atTop, ↑(c (n + 1)) ≤ (1 + ε) * ↑(c n)
ctop : Tendsto c atTop atTop
clim : Tendsto (fun n ↦ u (c n) / ↑(c n)) atTop (𝓝 l)
L : ∀ᶠ (n : ℕ) in atTop, ↑(c n) * l - u (c n) ≤ ε * ↑(c n)
⊢ ∀ᶠ (n : ℕ) in atTop, ↑n * l - u n ≤ ε * (1 + l) * ↑n
Module: Mathlib.Analysis.SpecificLimits.FloorPow

Goal state before:
pp: u : ℕ → ℝ
l : ℝ
hmono : Monotone u
hlim :
  ∀ (a : ℝ),
    1 < a →
      ∃ c,
        (∀ᶠ (n : ℕ) in atTop, ↑(c (n + 1)) ≤ a * ↑(c n)) ∧
          Tendsto c atTop atTop ∧ Tendsto (fun n ↦ u (c n) / ↑(c n)) atTop (𝓝 l)
lnonneg : 0 ≤ l
A : ∀ (ε : ℝ), 0 < ε → ∀ᶠ (n : ℕ) in atTop, u n - ↑n * l ≤ ε * (1 + ε + l) * ↑n
ε : ℝ
εpos : 0 < ε
c : ℕ → ℕ
cgrowth : ∀ᶠ (n : ℕ) in atTop, ↑(c (n + 1)) ≤ (1 + ε) * ↑(c n)
ctop : Tendsto c atTop atTop
clim : Tendsto (fun n ↦ u (c n) / ↑(c n)) atTop (𝓝 l)
L : ∀ᶠ (n : ℕ) in atTop, ↑(c n) * l - u (c n) ≤ ε * ↑(c n)
a : ℕ
ha : ∀ (b : ℕ), a ≤ b → ↑(c (b + 1)) ≤ (1 + ε) * ↑(c b) ∧ ↑(c b) * l - u (c b) ≤ ε * ↑(c b)
M : ℕ := (image (fun i ↦ c i) (range (a + 1))).max' ⋯
n : ℕ
hn : n ∈ Set.Ici M
exN : ∃ N, n < c N
N : ℕ := Nat.find exN
ncN : n < c N
aN : a + 1 ≤ N
Npos : 0 < N
aN' : a ≤ N - 1
cNn : c (N - 1) ≤ n
⊢ ↑n * l - u n ≤ ε * (1 + l) * ↑n

Tactic:
calc
      (n : ℝ) * l - u n ≤ c N * l - u (c (N - 1)) := by
        gcongr
        exact hmono cNn
      _ ≤ (1 + ε) * c (N - 1) * l - u (c (N - 1)) := by
        gcongr
        have B : N - 1 + 1 = N := Nat.succ_pred_eq_of_pos Npos
        simpa [B] using (ha _ aN').1
      _ = c (N - 1) * l - u (c (N - 1)) + ε * c (N - 1) * l := by ring
      _ ≤ ε * c (N - 1) + ε * c (N - 1) * l := add_le_add (ha _ aN').2 le_rfl
      _ = ε * (1 + l) * c (N - 1) := by ring
      _ ≤ ε * (1 + l) * n := by gcongr

Goal state after: