mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Real.OfDigits

Goal state before:
pp: b : ℕ
inst✝ : NeZero b
this : 1 < |↑b + 1|
⊢ ↑↑(Fin.last b) * ∑' (i : ℕ), (↑(b + 1))⁻¹ ^ (i + 1) = 1

pp: case hf
b : ℕ
inst✝ : NeZero b
this : 1 < |↑b + 1|
⊢ Summable fun n ↦ (↑(b + 1))⁻¹ ^ (n + 1)

Tactic:
· rw [geom_series_succ _ (by simp [inv_lt_one_iff₀, this]),
      tsum_geometric_of_lt_one (by positivity) (by simp [inv_lt_one_iff₀, NeZero.pos b])]
    push_cast
    have : (b : ℝ) ≠ 0 := mod_cast NeZero.ne b
    field [*]

Goal state after:
case hf
b : ℕ
inst✝ : NeZero b
this : 1 < |↑b + 1|
⊢ Summable fun n ↦ (↑(b + 1))⁻¹ ^ (n + 1)
Module: Mathlib.Analysis.Real.OfDigits

Goal state before:
pp: b : ℕ
hb : 1 < b
⊢ Set.SurjOn ofDigits Set.univ (Set.Icc 0 1)

Tactic:
have : NeZero b := ⟨by grind⟩

Goal state after:
b : ℕ
hb : 1 < b
this : NeZero b
⊢ Set.SurjOn ofDigits Set.univ (Set.Icc 0 1)
Module: Mathlib.Data.Rat.Sqrt

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

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

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

Goal state before:
pp: x : ℝ*
hx : Germ.Tendsto x (𝓝 0)
⊢ 0 < ArchimedeanClass.mk x

Tactic:
apply (archimedeanClassMk_nonneg_of_tendsto hx).lt_of_ne'
  rw [← stdPart_eq_zero, stdPart_of_tendsto hx]

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

Goal state before:
pp: x : ℝ*
hx : Germ.Tendsto x atBot
⊢ ArchimedeanClass.mk x < 0

Tactic:
have : x < 0 := lt_of_tendsto_atBot 0 hx
  intro n
  simpa [abs_of_neg this, lt_neg] using! lt_of_tendsto_atBot (-n) hx

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

Goal state before:
pp: r s : ℝ
hrs : r < s
f : ℕ → ℝ
hxr : (ofSeq f).IsSt r
g : ℕ → ℝ
hys : (ofSeq g).IsSt s
⊢ ofSeq f < ofSeq g

Tactic:
isSt_ofSeq_iff_tendsto

Goal state after:
r s : ℝ
hrs : r < s
f : ℕ → ℝ
hxr : Tendsto f (↑(hyperfilter ℕ)) (𝓝 r)
g : ℕ → ℝ
hys : Tendsto g (↑(hyperfilter ℕ)) (𝓝 s)
⊢ ofSeq f < ofSeq g
Module: Mathlib.Analysis.Real.Hyperreal

Goal state before:
pp: r s : ℝ
f : ℕ → ℝ
hr : (ofSeq f).IsSt r
hs : (ofSeq f).IsSt s
⊢ r = s

Tactic:
isSt_ofSeq_iff_tendsto

Goal state after:
r s : ℝ
f : ℕ → ℝ
hr : Tendsto f (↑(hyperfilter ℕ)) (𝓝 r)
hs : Tendsto f (↑(hyperfilter ℕ)) (𝓝 s)
⊢ r = s
Module: Mathlib.Analysis.Real.Hyperreal

Goal state before:
pp: r s : ℝ
⊢ (↑r).IsSt s ↔ (↑s).IsSt r

Tactic:
isSt_real_iff_eq,

Goal state after:
r s : ℝ
⊢ r = s ↔ (↑s).IsSt r
Module: Mathlib.Analysis.Real.Hyperreal

Goal state before:
pp: r s : ℝ
⊢ r = s ↔ (↑s).IsSt r

Tactic:
isSt_real_iff_eq,

Goal state after:
r s : ℝ
⊢ r = s ↔ s = r
Module: Mathlib.Analysis.Real.Hyperreal

Goal state before:
pp: r s t : ℝ
⊢ (↑r).IsSt s → (↑s).IsSt t → (↑r).IsSt t

Tactic:
isSt_real_iff_eq,

Goal state after:
r s t : ℝ
⊢ r = s → (↑s).IsSt t → (↑r).IsSt t
Module: Mathlib.Analysis.Real.Hyperreal

Goal state before:
pp: r s t : ℝ
⊢ r = s → (↑s).IsSt t → (↑r).IsSt t

Tactic:
isSt_real_iff_eq,

Goal state after:
r s t : ℝ
⊢ r = s → s = t → (↑r).IsSt t
Module: Mathlib.Analysis.Real.Hyperreal

Goal state before:
pp: r s : ℝ
f : ℝ → ℝ → ℝ
hf : ContinuousAt (Function.uncurry f) (r, s)
x : ℕ → ℝ
hxr : (ofSeq x).IsSt r
y : ℕ → ℝ
hys : (ofSeq y).IsSt s
⊢ IsSt (Germ.map₂ f (ofSeq x) (ofSeq y)) (f r s)

Tactic:
isSt_ofSeq_iff_tendsto

Goal state after:
r s : ℝ
f : ℝ → ℝ → ℝ
hf : ContinuousAt (Function.uncurry f) (r, s)
x : ℕ → ℝ
hxr : Tendsto x (↑(hyperfilter ℕ)) (𝓝 r)
y : ℕ → ℝ
hys : Tendsto y (↑(hyperfilter ℕ)) (𝓝 s)
⊢ IsSt (Germ.map₂ f (ofSeq x) (ofSeq y)) (f r s)
Module: Mathlib.Analysis.Real.Hyperreal

Goal state before:
pp: x y : ℝ*
hx : ¬x.Infinitesimal
hy : y.Infinite
⊢ (x * y).Infinite

Tactic:
by
  rw [mul_comm]; exact infinite_mul_of_infinite_not_infinitesimal hy hx

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

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

Tactic:
Complex.ext_iff,

Goal state after:
z : ℂ
h₀ : ¬(z.re = (↑π / 2).re ∧ z.im = (↑π / 2).im)
h₁ : -(π / 2) < z.re
h₂ : z.re ≤ π / 2
k : ℤ
⊢ ¬(z.re = ((2 * ↑k + 1) * ↑π / 2).re ∧ z.im = ((2 * ↑k + 1) * ↑π / 2).im)
Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy

Goal state before:
pp: p : ℝ
hp : 1 ≤ p
⊢ binEntropy (1 - p) ≤ 0

Tactic:
exact binEntropy_nonpos_of_nonpos (sub_nonpos.2 hp)

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

Goal state before:
pp: p : ℝ
⊢ binEntropy p = log 2 ↔ p = 2⁻¹

Tactic:
rw [← binEntropy_le_log_two.not_lt_iff_eq, binEntropy_lt_log_two, not_ne_iff]

Goal state after:
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)
hint : IntegrableOn (fun x ↦ x⁻¹ • (f (a * x) - f (b * x))) (Ioi 0) volume
⊢ ∫ (x : ℝ) in Ioi 0, x⁻¹ • (f (a * x) - f (b * x)) = log (b / a) • (L - R)

Tactic:
have h_lim := (tendsto_intervalIntegral hf ha hb hL hR).mono_left curry_le_prod

Goal state after:
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)
hint : IntegrableOn (fun x ↦ x⁻¹ • (f (a * x) - f (b * x))) (Ioi 0) volume
h_lim :
  Tendsto (fun p ↦ ∫ (x : ℝ) in p.1..p.2, x⁻¹ • (f (a * x) - f (b * x))) ((𝓝[>] 0).curry atTop)
    (𝓝 (log (b / a) • (L - R)))
⊢ ∫ (x : ℝ) in Ioi 0, x⁻¹ • (f (a * x) - f (b * x)) = log (b / a) • (L - R)
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Deligne

Goal state before:
pp: h : Tendsto (fun z ↦ z / 2 * Gamma (z / 2)) (𝓝[≠] 0) (𝓝 1)
h' : Tendsto (fun s ↦ 2 * ↑π ^ (-s / 2)) (𝓝[≠] 0) (𝓝 2)
z : ℂ
⊢ z * z.Gammaℝ = 2 * ↑π ^ (-z / 2) * (z / 2 * Gamma (z / 2))

Tactic:
rw [Gammaℝ]

Goal state after:
h : Tendsto (fun z ↦ z / 2 * Gamma (z / 2)) (𝓝[≠] 0) (𝓝 1)
h' : Tendsto (fun s ↦ 2 * ↑π ^ (-s / 2)) (𝓝[≠] 0) (𝓝 2)
z : ℂ
⊢ z * (↑π ^ (-z / 2) * Gamma (z / 2)) = 2 * ↑π ^ (-z / 2) * (z / 2 * Gamma (z / 2))
Module: Mathlib.NumberTheory.Harmonic.EulerMascheroni

Goal state before:
pp: case inr
n : ℕ
hn : n > 0
⊢ 0 < -↑(↑(n + 1))⁻¹ + (log ↑(n + 1) - log ↑n)

Tactic:
← sub_eq_neg_add,

Goal state after:
case inr
n : ℕ
hn : n > 0
⊢ 0 < log ↑(n + 1) - log ↑n - ↑(↑(n + 1))⁻¹
Module: Mathlib.NumberTheory.Harmonic.EulerMascheroni

Goal state before:
pp: m n : ℕ
this : ∀ (r : ℕ), eulerMascheroniSeq r < eulerMascheroniSeq' r
⊢ eulerMascheroniSeq (max m n) < eulerMascheroniSeq' n

Tactic:
exact (this _).trans_le (strictAnti_eulerMascheroniSeq'.antitone (le_max_right m n))

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

Goal state before:
pp: case a
n✝ : ℕ
f : ℝ → ℝ := log ∘ Gamma
hc : ConvexOn ℝ (Ioi 0) f
h_rec : ∀ (x : ℝ), 0 < x → f (x + 1) = f x + log x
hder : ∀ {x : ℝ}, 0 < x → DifferentiableAt ℝ f x
hder_rec : ∀ (x : ℝ), 0 < x → deriv f (x + 1) = deriv f x + 1 / x
hder_nat : ∀ (n : ℕ), deriv f (↑n + 1) = deriv f 1 + ↑(harmonic n)
derivLB : ∀ (n : ℕ), 0 < n → log ↑n ≤ deriv f (↑n + 1)
derivUB : ∀ (n : ℕ), deriv f (↑n + 1) ≤ log (↑n + 1)
n : ℕ
⊢ deriv f (↑n + 1) ≤ log (↑n + 1)

Tactic:
exact derivUB n

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
⊢ deriv Gamma (1 / 2) =
    deriv Gamma (1 / 2) * Gamma (1 / 2 + 1 / 2) + √π * deriv (fun s ↦ Gamma (s + 1 / 2)) (1 / 2) + √π * γ

pp: case hc
h_diff : ∀ {s : ℝ}, 0 < s → DifferentiableAt ℝ Gamma s
h_diff' : ∀ {s : ℝ}, 0 < s → DifferentiableAt ℝ (fun s ↦ Gamma (2 * s)) s
⊢ DifferentiableAt ℝ Gamma (1 / 2)

pp: case hd
h_diff : ∀ {s : ℝ}, 0 < s → DifferentiableAt ℝ Gamma s
h_diff' : ∀ {s : ℝ}, 0 < s → DifferentiableAt ℝ (fun s ↦ Gamma (2 * s)) s
⊢ DifferentiableAt ℝ (fun s ↦ Gamma (s + 1 / 2)) (1 / 2)

Tactic:
add_assoc,

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

case hc
h_diff : ∀ {s : ℝ}, 0 < s → DifferentiableAt ℝ Gamma s
h_diff' : ∀ {s : ℝ}, 0 < s → DifferentiableAt ℝ (fun s ↦ Gamma (2 * s)) s
⊢ DifferentiableAt ℝ Gamma (1 / 2)

case hd
h_diff : ∀ {s : ℝ}, 0 < s → DifferentiableAt ℝ Gamma s
h_diff' : ∀ {s : ℝ}, 0 < s → DifferentiableAt ℝ (fun s ↦ Gamma (2 * s)) s
⊢ DifferentiableAt ℝ (fun s ↦ Gamma (s + 1 / 2)) (1 / 2)
Module: Mathlib.NumberTheory.Harmonic.GammaDeriv

Goal state before:
pp: case e_a.e_a.e_a.refine_1
h_diff : ∀ {s : ℝ}, 0 < s → DifferentiableAt ℝ Gamma s
h_diff' : ∀ {s : ℝ}, 0 < s → DifferentiableAt ℝ (fun s ↦ Gamma (2 * s)) s
⊢ HasDerivAt (fun s ↦ 1 - 2 * s) (-2) (1 / 2)

Tactic:
mul_comm (2 : ℝ) _

Goal state after:
case e_a.e_a.e_a.refine_1
h_diff : ∀ {s : ℝ}, 0 < s → DifferentiableAt ℝ Gamma s
h_diff' : ∀ {s : ℝ}, 0 < s → DifferentiableAt ℝ (fun s ↦ Gamma (2 * s)) s
⊢ HasDerivAt (fun s ↦ 1 - s * 2) (-2) (1 / 2)
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 * log 2 + log ↑π) / 2 = -(↑γ + log (4 * ↑π)) / 2

Tactic:
add_assoc,

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 * log 2 + log ↑π)) / 2 = -(↑γ + log (4 * ↑π)) / 2
Module: Mathlib.MeasureTheory.Measure.RegularityCompacts

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
p q : Set α → Prop
hpq : ∀ (A B : Set α), p A → q B → p (A ∩ B)
hμ : ∀ (ε : ℝ≥0∞), 0 < ε → ∃ K, p K ∧ μ Kᶜ < ε
A : Set α
hA : q A
r : ℝ≥0∞
hr : r < μ A
⊢ ∃ K, p K ∧ K ⊆ A ∧ μ (A \ K) < μ A - r

Tactic:
obtain ⟨K', hpK', hK'_lt⟩ := hμ (μ A - r) (tsub_pos_of_lt hr)
    refine ⟨K' ∩ A, hpq K' A hpK' hA, inter_subset_right, ?_⟩
    · refine (measure_mono fun x ↦ ?_).trans_lt hK'_lt
      simp only [sdiff_inter_self_eq_sdiff, mem_sdiff, mem_compl_iff, and_imp, imp_self,
        imp_true_iff]

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

Goal state before:
pp: case h0
n : ℕ
ih : MonotoneOn (deriv fun x ↦ Polynomial.eval x (descPochhammer ℝ n)) (Set.Ioi (↑n - 1))
a : ℝ
ha : ↑n < a
b : ℝ
hb : ↑n < b
hab : a ≤ b
i : ℕ
hi : i ∈ Finset.range (n + 1)
j : ℕ
hj : j ≠ i ∧ j < n + 1
⊢ 0 ≤ a - ↑j

Tactic:
apply sub_nonneg_of_le

Goal state after:
case h0
n : ℕ
ih : MonotoneOn (deriv fun x ↦ Polynomial.eval x (descPochhammer ℝ n)) (Set.Ioi (↑n - 1))
a : ℝ
ha : ↑n < a
b : ℝ
hb : ↑n < b
hab : a ≤ b
i : ℕ
hi : i ∈ Finset.range (n + 1)
j : ℕ
hj : j ≠ i ∧ j < n + 1
⊢ ↑j ≤ a
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
ε : ℝ
P' : Measure E
inst✝ : IsFiniteMeasure P'
A : Subalgebra ℝ (E →ᵇ ℝ)
hε : 0 < ε
heq : ∀ g ∈ A, ∫ (x : E), g x ∂P = ∫ (x : E), g x ∂P'
g : E →ᵇ ℝ
hgA : g ∈ A
one_add_inv_mul_mem : ∀ (n : ℕ), g * (1 + (↑n)⁻¹ • -(ε • g * g)) ^ n ∈ A
limP :
  Tendsto (fun n ↦ ∫ (x : E), (g * (1 + (↑n)⁻¹ • -(ε • g * g)) ^ n) x ∂P) atTop
    (𝓝 (∫ (x : E), ε.mulExpNegMulSq (g x) ∂P'))
⊢ ∫ (x : E), ε.mulExpNegMulSq (g x) ∂P = ∫ (x : E), ε.mulExpNegMulSq (g x) ∂P'

Tactic:
exact tendsto_nhds_unique
    (tendsto_integral_mul_one_add_inv_smul_sq_pow g hε) limP

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

Goal state before:
pp: L : PeriodPair
α β : ℚ
H : ↑α * L.ω₁ + ↑β * L.ω₂ ∈ L.lattice
m n : ℤ
e : ↑m * L.ω₁ + ↑n * L.ω₂ = ↑α * L.ω₁ + ↑β * L.ω₂
⊢ (↑m - ↑α) • L.ω₁ + (↑n - ↑β) • L.ω₂ = 0

Tactic:
simp; linear_combination e

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Pow.Integral

Goal state before:
pp: E : Type u_2
F : Type u_3
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : FiniteDimensional ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : NormedAddCommGroup F
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
hd : 1 ≤ Module.finrank ℝ E
f : E → F
C α r : ℝ
hα : α < ↑(Module.finrank ℝ E)
h_decay : ∀ᵐ (x : E) ∂μ.restrict (ball 0 r), ‖f x‖ ≤ C * ‖x‖ ^ (-α)
h_meas : AEStronglyMeasurable f μ
this : Nontrivial E
h_rpow : IntegrableOn (fun y ↦ y ^ (↑(Module.finrank ℝ E) - 1 - α)) (Ioo 0 r) volume
y : ℝ
hy : 0 < y
right✝ : y < r
⊢ y ^ (↑(Module.finrank ℝ E) - 1 - α) * C = y ^ (Module.finrank ℝ E - 1) * y ^ (-α) * C

Tactic:
rw [← Real.rpow_natCast y (Module.finrank ℝ E - 1), ← Real.rpow_add hy]

Goal state after:
E : Type u_2
F : Type u_3
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : FiniteDimensional ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : NormedAddCommGroup F
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
hd : 1 ≤ Module.finrank ℝ E
f : E → F
C α r : ℝ
hα : α < ↑(Module.finrank ℝ E)
h_decay : ∀ᵐ (x : E) ∂μ.restrict (ball 0 r), ‖f x‖ ≤ C * ‖x‖ ^ (-α)
h_meas : AEStronglyMeasurable f μ
this : Nontrivial E
h_rpow : IntegrableOn (fun y ↦ y ^ (↑(Module.finrank ℝ E) - 1 - α)) (Ioo 0 r) volume
y : ℝ
hy : 0 < y
right✝ : y < r
⊢ y ^ (↑(Module.finrank ℝ E) - 1 - α) * C = y ^ (↑(Module.finrank ℝ E - 1) + -α) * C
Module: Mathlib.Analysis.SpecialFunctions.Pow.NthRootLemmas

Goal state before:
pp: n a b : ℕ
h₁ : a ^ n ≤ b
h₂ : b < (a + 1) ^ n
⊢ n.nthRoot b = a

Tactic:
rcases eq_or_ne n 0 with rfl | hn
  · grind
  simp only [← le_nthRoot_iff hn, ← nthRoot_lt_iff hn] at h₁ h₂
  grind

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Basic

Goal state before:
pp: θ : ℂ
n : ℤ
⊢ eval (cos θ) (U ℂ n) * sin θ = sin ((↑n + 1) * θ)

Tactic:
by
  induction n using Polynomial.Chebyshev.induct with
  | zero => simp
  | one => simp [one_add_one_eq_two, sin_two_mul]; ring
  | add_two n ih1 ih2 =>
    simp only [U_add_two, eval_sub, eval_mul, eval_X, eval_ofNat, sub_mul,
      mul_assoc, ih1, ih2, sub_eq_iff_eq_add, sin_add_sin]
    push_cast
    ring_nf
  | neg_add_one n ih1 ih2 =>
    simp only [U_sub_one, eval_sub, eval_mul, eval_X, eval_ofNat, sub_mul,
      mul_assoc, ih1, ih2, sub_eq_iff_eq_add', sin_add_sin]
    push_cast
    ring_nf

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

Goal state before:
pp: a : ℝ
hapos : 0 < a
halimit : Tendsto stirlingSeq atTop (𝓝 a)
hπ : π / 2 = a ^ 2 / 2
⊢ Tendsto stirlingSeq atTop (𝓝 √(a ^ 2))

Tactic:
sqrt_sq hapos.le

Goal state after:
a : ℝ
hapos : 0 < a
halimit : Tendsto stirlingSeq atTop (𝓝 a)
hπ : π / 2 = a ^ 2 / 2
⊢ Tendsto stirlingSeq atTop (𝓝 a)
Module: Mathlib.Analysis.SpecialFunctions.Stirling

Goal state before:
pp: n : ℕ
⊢ √(2 * π * ↑n) * (↑n / rexp 1) ^ n ≤ ↑n !

Tactic:
by
  obtain rfl | hn := eq_or_ne n 0
  · simp
  have : √(2 * π * n) * (n / exp 1) ^ n = √π * (√(2 * n) * (n / exp 1) ^ n) := by
    simp [sqrt_mul']; ring
  rw [this, ← le_div_iff₀ (by positivity)]
  exact sqrt_pi_le_stirlingSeq hn

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal

Goal state before:
pp: n : ℕ
c : ℕ → ℝ
hcnonneg : ∀ i ≤ n, 0 ≤ (-1) ^ i * c i
P : ℝ[X]
hPbnd : ∀ x ∈ Set.Icc (-1) 1, |eval x P| ≤ 1
i : ℕ
hi : i ∈ Finset.Iic n
⊢ eval (node n i) P * c i ≤ eval (node n i) (T ℝ ↑n) * c i

Tactic:
calc
    P.eval (node n i) * (c i) =
      ((-1) ^ i * P.eval (node n i)) * ((-1) ^ i * (c i)) :=
      negOnePow_mul_negOnePow_mul_cancel.symm
    _ ≤ 1 * ((-1) ^ i * (c i)) := by
      gcongr
      · exact (hcnonneg i (Finset.mem_Iic.mp hi))
      · exact (negOnePow_mul_le (hPbnd _ node_mem_Icc))
    _ = (T ℝ n).eval (node n i) * (c i) := by
      rw [eval_T_real_node hi, one_mul]

Goal state after:
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable

Goal state before:
pp: z : ℍ
c d : ℝ
hd : 1 ≤ d ^ 2
⊢ r z ≤ ‖↑c * ↑z + ↑d‖

Tactic:
have H1 : √(r1 z) ≤ √((c * z.re + d) ^ 2 + (c * z.im) ^ 2) :=
    (Real.sqrt_le_sqrt_iff (by positivity)).mpr (r1_aux_bound _ _ hd)
  simpa only [r, norm_def, normSq_apply, add_re, re_ofReal_mul, coe_re, ofReal_re, ← pow_two,
    add_im, im_ofReal_mul, coe_im, ofReal_im, add_zero, min_le_iff] using Or.inr H1

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema

Goal state before:
pp: case refine_1
n : ℕ
hn : n ≠ 0
x : ℝ
hx✝ : x ∈ Finset.image (fun k ↦ cos ((↑k + 1) * π / (↑n + 1))) (Finset.range n)
k : ℕ
hk : k ∈ Finset.range n
hx : cos ((↑k + 1) * π / (↑n + 1)) = x
⊢ eval x (U ℝ ↑n) * sin ((↑k + 1) * π / (↑n + 1)) = 0

Tactic:
rw [← hx, U_real_cos, sin_eq_zero_iff]

Goal state after:
case refine_1
n : ℕ
hn : n ≠ 0
x : ℝ
hx✝ : x ∈ Finset.image (fun k ↦ cos ((↑k + 1) * π / (↑n + 1))) (Finset.range n)
k : ℕ
hk : k ∈ Finset.range n
hx : cos ((↑k + 1) * π / (↑n + 1)) = x
⊢ ∃ n_1, ↑n_1 * π = (↑↑n + 1) * ((↑k + 1) * π / (↑n + 1))
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent

Goal state before:
pp: x : ℂ
hx : x ∈ ℂ_ℤ
⊢ ∏' (i : ℕ), (1 + sineTerm x i) = Complex.sin (↑π * x) / (↑π * x)

Tactic:
rw [← Multipliable.hasProd_iff (multipliable_sineTerm x),
    Multipliable.hasProd_iff_tendsto_nat (multipliable_sineTerm x)]

Goal state after:
x : ℂ
hx : x ∈ ℂ_ℤ
⊢ Tendsto (fun n ↦ ∏ i ∈ Finset.range n, (1 + sineTerm x i)) atTop (𝓝 (Complex.sin (↑π * x) / (↑π * x)))
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema

Goal state before:
pp: k : ℕ
x : ℝ
hx : |x| ≤ 1
n : ℕ
this : (⇑derivative)^[k] (T ℝ ↑n) ∈ Submodule.span ℕ ((fun m ↦ T ℝ ↑m) '' Set.Icc 0 (n - k))
f : ℝ[X] →₀ ℕ
hfsupp : ↑f.support ⊆ (fun m ↦ T ℝ ↑m) '' Set.Icc 0 (n - k)
hfderiv : ∑ p ∈ f.support, f p • p = (⇑derivative)^[k] (T ℝ ↑n)
hf : ∀ (y : ℝ), ∑ p ∈ f.support, f p • eval y p = eval y ((⇑derivative)^[k] (T ℝ ↑n))
⊢ |∑ p ∈ f.support, f p • eval x p| ≤ ∑ p ∈ f.support, f p • eval 1 p

Tactic:
Finset.abs_sum_le_sum_abs

Goal state after:
k : ℕ
x : ℝ
hx : |x| ≤ 1
n : ℕ
this : (⇑derivative)^[k] (T ℝ ↑n) ∈ Submodule.span ℕ ((fun m ↦ T ℝ ↑m) '' Set.Icc 0 (n - k))
f : ℝ[X] →₀ ℕ
hfsupp : ↑f.support ⊆ (fun m ↦ T ℝ ↑m) '' Set.Icc 0 (n - k)
hfderiv : ∑ p ∈ f.support, f p • p = (⇑derivative)^[k] (T ℝ ↑n)
hf : ∀ (y : ℝ), ∑ p ∈ f.support, f p • eval y p = eval y ((⇑derivative)^[k] (T ℝ ↑n))
⊢ ∑ i ∈ f.support, |f i • eval x i| ≤ ∑ p ∈ f.support, f p • eval 1 p
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent

Goal state before:
pp: x : ℂ
hx : x ∈ ℂ_ℤ
n : ℕ
⊢ logDeriv (fun z ↦ ∏ j ∈ Finset.range n, (1 + sineTerm z j)) x = ∑ j ∈ Finset.range n, cotTerm x j

Tactic:
logDeriv_prod

Goal state after:
x : ℂ
hx : x ∈ ℂ_ℤ
n : ℕ
⊢ ∑ i ∈ Finset.range n, logDeriv (fun z ↦ 1 + sineTerm z i) x = ∑ j ∈ Finset.range n, cotTerm x j

case hf
x : ℂ
hx : x ∈ ℂ_ℤ
n : ℕ
⊢ ∀ i ∈ Finset.range n, 1 + sineTerm x i ≠ 0

case hd
x : ℂ
hx : x ∈ ℂ_ℤ
n : ℕ
⊢ ∀ i ∈ Finset.range n, DifferentiableAt ℂ (fun z ↦ 1 + sineTerm z i) x
Module: Mathlib.Tactic.NormNum.Prime

Goal state before:
pp: n : ℕ
h1 : ble 2 n = true
h2 : 1 = n % 2
⊢ 3 ≤ n.minFac

Tactic:
refine (le_minFac'.mpr fun p hp hpn ↦ ?_).resolve_left (Nat.ne_of_gt (Nat.le_of_ble_eq_true h1))

Goal state after:
n : ℕ
h1 : ble 2 n = true
h2 : 1 = n % 2
p : ℕ
hp : 2 ≤ p
hpn : p ∣ n
⊢ 3 ≤ p
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent

Goal state before:
pp: z : ℂ
k : ℕ
hk : 1 ≤ k
hz : z ∈ ℍₒ
⊢ Summable fun n ↦ (z + ↑(↑n + 1)) ^ (-1 - ↑k)

Tactic:
by simpa using aux_summable_add hk z

Goal state after:
Module: Mathlib.Analysis.SumIntegralComparisons

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

Tactic:
simp [-Nat.cast_add, hk]

Goal state after:
Module: Mathlib.Analysis.SumIntegralComparisons

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

Tactic:
simp [-Nat.cast_add, hk]

Goal state after:
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
ε : ℝ
ε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, u (c n) - ↑(c n) * l ≤ ε * ↑(c n)
a : ℕ
ha : ∀ (b : ℕ), a ≤ b → ↑(c (b + 1)) ≤ (1 + ε) * ↑(c b) ∧ u (c b) - ↑(c b) * l ≤ ε * ↑(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
cNn : c (N - 1) ≤ n
IcN : ↑(c N) ≤ (1 + ε) * ↑(c (N - 1))
⊢ u n - ↑n * l ≤ u (c N) - ↑(c (N - 1)) * l

Tactic:
by gcongr; exact hmono ncN.le

Goal state after:
Module: Mathlib.Analysis.SumIntegralComparisons

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

Tactic:
suffices ∑ i ∈ .Ico (0 + a) (b - a + a), f ↑(i + 1) ≤ ∫ x in a..a + ↑(b - a), f x by simp_all

Goal state after:
a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc ↑a ↑b)
⊢ ∑ i ∈ Finset.Ico (0 + a) (b - a + a), f ↑(i + 1) ≤ ∫ (x : ℝ) in ↑a..↑a + ↑(b - a), f x
Module: Mathlib.Analysis.SumIntegralComparisons

Goal state before:
pp: f : ℝ → ℝ
N : ℕ
anti : AntitoneOn f (Ici ↑N)
summable : Summable fun n ↦ f ↑(n + N)
nonneg : ∀ t ∈ Ioi ↑N, 0 ≤ f t
lim : Tendsto (fun n ↦ ∑ i ∈ Finset.range n, f ↑(i + N)) atTop (nhds (∑' (i : ℕ), f ↑(i + N)))
this : Tendsto (fun x ↦ ↑x + ↑N) atTop atTop
integrable : IntegrableOn f (Ioi ↑N) volume
M : ℕ
⊢ ∫ (x : ℝ) in ↑N..↑M + ↑N, f x ≤ ∑ i ∈ Finset.range M, f ↑(i + N)

Tactic:
calc
    _ ≤ ∑ n ∈ Finset.Ico N (N + M), f n := by
      convert!  AntitoneOn.integral_le_sum_Ico _ _ using 2 <;> grind [anti.mono]
    _ = _ := by
      rw [Finset.sum_Ico_eq_sum_range]
      grind

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

Goal state before:
pp: case hab
N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < 1 - c⁻¹
i : ℕ
a✝ : i ∈ {i ∈ range N | j < c ^ i}
⊢ (1 - c⁻¹) * c ^ i ≤ ↑⌊c ^ i⌋₊

Tactic:
exact mul_pow_le_nat_floor_pow hc i

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Indization.FilteredColimits

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
I : Type v
inst✝¹ : SmallCategory I
F : I ⥤ Cᵒᵖ ⥤ Type v
inst✝ : IsFiltered I
hF : ∀ (i : I), IsIndObject (F.obj i)
J : Type v
x✝¹ : SmallCategory J
x✝ : FinCategory J
G : J ⥤ CostructuredArrow yoneda (colimit F)
h₁ : Nonempty (limit (G.op ⋙ (CostructuredArrow.toOver yoneda (colimit F)).op ⋙ yoneda.obj (Over.mk (𝟙 (colimit F)))))
i : I
hi :
  Nonempty
    (limit
      ((G.op ⋙ (CostructuredArrow.toOver yoneda (colimit F)).op) ⋙
        yoneda.obj ((colimit.toCostructuredArrow F ⋙ CostructuredArrow.toOver F (colimit F)).obj i)))
⊢ ∃ X, Nonempty (limit (G.op ⋙ yoneda.obj X))

Tactic:
obtain ⟨⟨P⟩⟩ := hF i

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
I : Type v
inst✝¹ : SmallCategory I
F : I ⥤ Cᵒᵖ ⥤ Type v
inst✝ : IsFiltered I
hF : ∀ (i : I), IsIndObject (F.obj i)
J : Type v
x✝¹ : SmallCategory J
x✝ : FinCategory J
G : J ⥤ CostructuredArrow yoneda (colimit F)
h₁ : Nonempty (limit (G.op ⋙ (CostructuredArrow.toOver yoneda (colimit F)).op ⋙ yoneda.obj (Over.mk (𝟙 (colimit F)))))
i : I
hi :
  Nonempty
    (limit
      ((G.op ⋙ (CostructuredArrow.toOver yoneda (colimit F)).op) ⋙
        yoneda.obj ((colimit.toCostructuredArrow F ⋙ CostructuredArrow.toOver F (colimit F)).obj i)))
P : IndObjectPresentation (F.obj i)
⊢ ∃ X, Nonempty (limit (G.op ⋙ yoneda.obj X))