mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.NumberTheory.Real.Irrational

Goal state before:
pp: x : ℝ
h : Irrational x
m : ℤ
⊢ Irrational (↑m + x)

Tactic:
rw [← cast_intCast]

Goal state after:
x : ℝ
h : Irrational x
m : ℤ
⊢ Irrational (↑↑m + x)
Module: Mathlib.NumberTheory.Real.Irrational

Goal state before:
pp: x : ℝ
h : Irrational x
m : ℤ
hm : m ≠ 0
⊢ Irrational (x * ↑m)

Tactic:
rw [← cast_intCast]

Goal state after:
x : ℝ
h : Irrational x
m : ℤ
hm : m ≠ 0
⊢ Irrational (x * ↑↑m)
Module: Mathlib.Analysis.Real.Hyperreal

Goal state before:
pp: case refine_1
x : ℝ*
h : x.InfiniteNeg
⊢ x < 0 ∧ ArchimedeanClass.mk x < 0

Tactic:
have hx : x < 0 := h 0
    refine ⟨h 0, fun n ↦ ?_⟩
    simpa [abs_of_neg hx, lt_neg] using! h (-n)

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

Goal state before:
pp: x : ℝ
h : Irrational x
m : ℤ
hm : m ≠ 0
⊢ Irrational (x / ↑m)

Tactic:
rw [← cast_intCast]

Goal state after:
x : ℝ
h : Irrational x
m : ℤ
hm : m ≠ 0
⊢ Irrational (x / ↑↑m)
Module: Mathlib.Analysis.Real.Hyperreal

Goal state before:
pp: x : ℝ*
⊢ stdPart x = sSup {y | ↑y < x}

Tactic:
exact stdPart_eq_sSup coeRingHom x

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

Goal state before:
pp: f : ℕ → ℝ
hf : Tendsto f atTop atTop
⊢ (ofSeq f).InfinitePos

Tactic:
by
  replace hf := hf.mono_left Nat.hyperfilter_le_atTop
  rw [infinitePos_iff]
  exact ⟨lt_of_tendsto_atTop 0 hf, archimedeanClassMk_neg_of_tendsto_atTop hf⟩

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

Goal state before:
pp: case succ
n : ℕ
IH :
  ∏ i ∈ range n, (2 * ↑i + 2) / (2 * ↑i + 1) * ((2 * ↑i + 2) / (2 * ↑i + 3)) =
    2 ^ (4 * n) * ↑n ! ^ 4 / (↑(2 * n)! ^ 2 * (2 * ↑n + 1))
⊢ 2 ^ (4 * n) * ↑n ! ^ 4 / (↑(2 * n)! ^ 2 * (2 * ↑n + 1)) *
      ((2 * ↑n + 2) / (2 * ↑n + 1) * ((2 * ↑n + 2) / (2 * ↑n + 3))) =
    2 ^ (4 * (n + 1)) * ↑(n + 1)! ^ 4 / (↑(2 * (n + 1))! ^ 2 * (2 * ↑(n + 1) + 1))

Tactic:
_root_.div_mul_div_comm,

Goal state after:
case succ
n : ℕ
IH :
  ∏ i ∈ range n, (2 * ↑i + 2) / (2 * ↑i + 1) * ((2 * ↑i + 2) / (2 * ↑i + 3)) =
    2 ^ (4 * n) * ↑n ! ^ 4 / (↑(2 * n)! ^ 2 * (2 * ↑n + 1))
⊢ 2 ^ (4 * n) * ↑n ! ^ 4 / (↑(2 * n)! ^ 2 * (2 * ↑n + 1)) *
      ((2 * ↑n + 2) * (2 * ↑n + 2) / ((2 * ↑n + 1) * (2 * ↑n + 3))) =
    2 ^ (4 * (n + 1)) * ↑(n + 1)! ^ 4 / (↑(2 * (n + 1))! ^ 2 * (2 * ↑(n + 1) + 1))
Module: Mathlib.Analysis.SpecialFunctions.Choose

Goal state before:
pp: case succ
k : ℕ
h : (fun n ↦ ↑(n.descFactorial k)) ~[atTop] fun n ↦ ↑n ^ k
⊢ (fun n ↦ ↑(n.descFactorial (k + 1))) ~[atTop] fun n ↦ ↑n ^ (k + 1)

Tactic:
simp_rw [descFactorial_succ, cast_mul, _root_.pow_succ']
    refine IsEquivalent.mul ?_ h
    have hz : ∀ᶠ (x : ℕ) in atTop, (x : ℝ) ≠ 0 :=
      eventually_atTop.mpr ⟨1, fun n hn ↦ ne_of_gt (mod_cast hn)⟩
    rw [isEquivalent_iff_tendsto_one hz, ← tendsto_add_atTop_iff_nat k]
    simpa using tendsto_natCast_div_add_atTop (k : ℝ)

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

Goal state before:
pp: q : ℕ
p : ℝ
hp₀ : 0 ≤ p
hp₁ : p ≤ 1
⊢ 0 ≤ qaryEntropy q p

Tactic:
by
  obtain rfl | hp₀ := hp₀.eq_or_lt
  · simp
  obtain rfl | hp₁ := hp₁.eq_or_lt
  · simpa [qaryEntropy, -Int.cast_sub] using log_intCast_nonneg _
  exact (qaryEntropy_pos hp₀ hp₁).le

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

Goal state before:
pp: case pos
q : ℕ
p : ℝ
is_x_where_nondiff : p ≠ 0 ∧ p ≠ 1
⊢ deriv (deriv (qaryEntropy q)) p = -1 / (p * (1 - p))

pp: case neg
q : ℕ
p : ℝ
is_x_where_nondiff : ¬(p ≠ 0 ∧ p ≠ 1)
⊢ deriv (deriv (qaryEntropy q)) p = -1 / (p * (1 - p))

Tactic:
· obtain ⟨xne0, xne1⟩ := is_x_where_nondiff
    suffices ∀ᶠ y in (𝓝 p),
        deriv (fun p ↦ (qaryEntropy q) p) y = log (q - 1) + log (1 - y) - log y by
      refine (Filter.EventuallyEq.deriv_eq this).trans ?_
      rw [deriv_fun_sub ?_ (differentiableAt_log xne0)]
      · rw [deriv.log differentiableAt_fun_id xne0]
        simp only [deriv_id'', one_div]
        · have {q : ℝ} (p : ℝ) : DifferentiableAt ℝ (fun p => q - p) p := by fun_prop
          simp [field, sub_ne_zero_of_ne xne1.symm, this]
          ring
      · apply DifferentiableAt.add
        · simp only [differentiableAt_const]
        exact DifferentiableAt.log (by fun_prop) (sub_ne_zero.mpr xne1.symm)
    filter_upwards [eventually_ne_nhds xne0, eventually_ne_nhds xne1]
      with y xne0 h2 using deriv_qaryEntropy xne0 h2

Goal state after:
case neg
q : ℕ
p : ℝ
is_x_where_nondiff : ¬(p ≠ 0 ∧ p ≠ 1)
⊢ deriv (deriv (qaryEntropy q)) p = -1 / (p * (1 - p))
Module: Mathlib.Analysis.Real.Pi.Irrational

Goal state before:
pp: h' : ¬Irrational (π / 2)
a : ℤ
b : ℕ
hb : 0 < b
h : π / 2 = ↑a / ↑b
ha : 0 < ↑a
k : ∀ (n : ℕ), 0 < ↑a ^ (2 * n + 1) / ↑n !
j : ∀ᶠ (n : ℕ) in atTop, ↑a ^ (2 * n + 1) / ↑n ! * I n (π / 2) < 1
n : ℕ
hn : ↑a ^ (2 * n + 1) / ↑n ! * I n (π / 2) < 1
hn' : 0 < ↑a ^ (2 * n + 1) / ↑n ! * I n (π / 2)
z : ℤ
hz : eval₂ (Int.castRingHom ℝ) (↑a / ↑b) (sinPoly n) * ↑b ^ (2 * n + 1) = ↑z
e : I n (π / 2) * (π / 2) ^ (2 * n + 1) = ↑n ! * eval₂ (Int.castRingHom ℝ) (π / 2) (sinPoly n)
this : ↑a ^ (2 * n + 1) / ↑n ! * I n (π / 2) = eval₂ (Int.castRingHom ℝ) (π / 2) (sinPoly n) * ↑b ^ (2 * n + 1)
⊢ 0 < ↑z ∧ ↑z < 1

Tactic:
simp [← hz, ← h, ← this, hn', hn]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog.Order

Goal state before:
pp: A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
⊢ Tendsto (fun p a ↦ if a ∈ {b | IsStrictlyPositive b} then cfc (fun x ↦ p⁻¹ * (x ^ p - 1)) a else 0) (𝓝[>] 0)
    (𝓝 fun a ↦ if a ∈ {b | IsStrictlyPositive b} then log a else 0)

Tactic:
by
  rw [tendsto_pi_nhds]
  intro a
  by_cases ha : IsStrictlyPositive a
  · simpa [ha] using CFC.tendsto_cfc_rpow_sub_one_log ha
  · simp_all

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

Goal state before:
pp: p x : ℝ
hp : 0 < p ∧ p < 1
hx : 0 ≤ x
⊢ 0 < 1

Tactic:
· exact zero_lt_one

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 (Ioi 1))

Tactic:
refine ContinuousOn.aestronglyMeasurable ?_ measurableSet_Ioi
    exact continuousOn_rpowIntegrand₀₁ hp hx |>.mono (Set.Ioi_subset_Ioi zero_le_one)

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

Goal state before:
pp: ⊢ Tendsto (fun n ↦ ↑(harmonic n) - log ↑n) atTop (𝓝 eulerMascheroniConstant)

Tactic:
apply tendsto_eulerMascheroniSeq'.congr'
  filter_upwards [eventually_ne_atTop 0] with n hn
  simp_rw [eulerMascheroniSeq', hn, if_false]

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

Goal state before:
pp: p : ℝ
hp : p ∈ Ioo 0 1
⊢ 0 ≤ ∫ (t : ℝ) in Ioi 0, p.rpowIntegrand₀₁ t 1

Tactic:
exact le_of_lt <| integral_rpowIntegrand₀₁_one_pos hp

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

Goal state before:
pp: ⊢ HasDerivAt Gamma (-γ) 1

Tactic:
by
  simpa only [factorial_zero, cast_one, harmonic_zero, Rat.cast_zero, add_zero, mul_neg, one_mul,
    cast_zero, zero_add] using hasDerivAt_Gamma_nat 0

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

Goal state before:
pp: case right
a : ℂ
ha : a.re < 0
b : ℂ
s : ℝ
⊢ (fun x ↦ cexp (a * ↑x ^ 2 + b * ↑x)) =o[atTop] fun x ↦ |x| ^ s

Tactic:
· refine (cexp_neg_quadratic_isLittleO_rpow_atTop ha b s).congr' EventuallyEq.rfl ?_
    refine (eventually_gt_atTop 0).mp (Eventually.of_forall fun x hx ↦ ?_)
    simp_rw [abs_of_pos hx]

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

Goal state before:
pp: ⊢ HasDerivAt Gamma (-↑γ) 1

Tactic:
by
  simpa only [factorial_zero, cast_one, harmonic_zero, Rat.cast_zero, add_zero, mul_neg, one_mul,
    cast_zero, zero_add] using hasDerivAt_Gamma_nat 0

Goal state after:
Module: Mathlib.Data.Int.Log

Goal state before:
pp: case inl.inr
R : Type u_1
inst✝³ : Semifield R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorSemiring R
b : ℕ
r : R
hrp : 0 < r
hr : r ≤ 1
⊢ ↑(Nat.clog b ⌈r⁻¹⌉₊) = -log b r

Tactic:
log_of_right_le_one _ hr,

Goal state after:
case inl.inr
R : Type u_1
inst✝³ : Semifield R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorSemiring R
b : ℕ
r : R
hrp : 0 < r
hr : r ≤ 1
⊢ ↑(Nat.clog b ⌈r⁻¹⌉₊) = - -↑(Nat.clog b ⌈r⁻¹⌉₊)
Module: Mathlib.Data.Int.Log

Goal state before:
pp: case inr
R : Type u_1
inst✝³ : Semifield R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorSemiring R
b : ℕ
r : R
hrp : r ≤ 0
⊢ clog b r⁻¹ = -log b r

Tactic:
rw [clog_of_right_le_zero _ (inv_nonpos.mpr hrp), log_of_right_le_zero _ hrp, neg_zero]

Goal state after:
Module: Mathlib.Data.Int.Log

Goal state before:
pp: case succ
R : Type u_1
inst✝³ : Semifield R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorSemiring R
b n : ℕ
⊢ clog b ↑(n + 1) = ↑(Nat.clog b (n + 1))

Tactic:
· rw [clog_of_one_le_right, (Nat.ceil_eq_iff (Nat.succ_ne_zero n)).mpr] <;> simp

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

Goal state before:
pp: b x y : ℝ
b_pos : 0 < b
b_lt_one : b < 1
h : 0 < x
h₁ : 0 < y
⊢ log x / log b ≤ log y / log b ↔ y ≤ x

Tactic:
div_le_div_right_of_neg (log_neg b_pos b_lt_one),

Goal state after:
b x y : ℝ
b_pos : 0 < b
b_lt_one : b < 1
h : 0 < x
h₁ : 0 < y
⊢ log y ≤ log x ↔ y ≤ x
Module: Mathlib.Analysis.SpecialFunctions.Log.Base

Goal state before:
pp: b : ℝ
hb : b ≠ -1 ∧ b ≠ 0 ∧ b ≠ 1
this : ∀ {b : ℝ}, b ≠ -1 ∧ b ≠ 0 ∧ b ≠ 1 → 0 < b → Tendsto (fun x ↦ |logb b x|) atTop atTop
hb₀ : ¬0 < b
⊢ 0 < -b

Tactic:
by linarith +splitNe

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

Goal state before:
pp: b✝ b : ℝ
hb : b ≠ -1 ∧ b ≠ 0 ∧ b ≠ 1
hb₀ : 0 < b
this : ∀ {b : ℝ}, b ≠ -1 ∧ b ≠ 0 ∧ b ≠ 1 → 0 < b → 1 < b → Tendsto (fun x ↦ |logb b x|) atTop atTop
hb₁ : ¬1 < b
⊢ b < 1

Tactic:
by linarith +splitNe

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

Goal state before:
pp: X : Type u_1
inst✝² : MeasurableSpace X
inst✝¹ : TopologicalSpace X
μ : Measure X
E : Type u_2
inst✝ : NormedAddCommGroup E
f : X →ᵇ E
⊢ ∫⁻ (x : X), ↑‖f‖₊ ∂μ = ↑‖f‖₊ * μ Set.univ

Tactic:
by rw [lintegral_const]

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

Goal state before:
pp: b a c : ℝ
n : ℕ
ha : a ≠ 0
x✝ : log b = 0 ∨ log b ≠ 0
⊢ Tendsto (fun x ↦ logb b x ^ n / (a * x + c)) atTop (𝓝 0)

Tactic:
cases eq_or_ne (log b) 0 with

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

Goal state before:
pp: case h
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
⊢ ∃ a, ∀ (b : ℕ), a ≤ b → ∀ᵐ (ω : E) ∂P, ‖(u b).mulExpNegMulSq (g ω)‖ ≤ ‖g‖

Tactic:
use N

Goal state after:
case h
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
⊢ ∀ (b : ℕ), N ≤ b → ∀ᵐ (ω : E) ∂P, ‖(u b).mulExpNegMulSq (g ω)‖ ≤ ‖g‖
Module: Mathlib.Analysis.SpecialFunctions.MulExpNegMulSqIntegral

Goal state before:
pp: case h
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
⊢ ∃ a, ∀ (b : ℕ), a ≤ b → ∀ᵐ (ω : E) ∂P, ‖(g * (1 + (↑b)⁻¹ • -(ε • g * g)) ^ b) ω‖ ≤ ‖g‖

Tactic:
use N

Goal state after:
case h
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
⊢ ∀ (b : ℕ), N ≤ b → ∀ᵐ (ω : E) ∂P, ‖(g * (1 + (↑b)⁻¹ • -(ε • g * g)) ^ b) ω‖ ≤ ‖g‖
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)
⊢ ∀ i_1 ∈ (Finset.range (n + 1)).erase i, 0 ≤ a - ↑i_1

Tactic:
intro j hj

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 ∈ (Finset.range (n + 1)).erase i
⊢ 0 ≤ a - ↑j
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 x) ≤ ↑n

Tactic:
apply le_trans (le_trans _ (le_of_lt hgN)) (Nat.cast_le.mpr hn)

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 x) ≤ ε * (‖g‖ * ‖g‖)
Module: Mathlib.MeasureTheory.Constructions.HaarToSphere

Goal state before:
pp: E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
μ : Measure E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
inst✝ : μ.IsAddHaarMeasure
x : ↑(sphere 0 1)
this : Nontrivial E
ε : ℝ
hε : 0 < ε
hε₂ : ε ≤ 2
⊢ ↑(toSphereBallBound (dim E) ε) * μ (ball 0 1) ≤ μ.toSphere (ball x ε)

Tactic:
μ.toSphere_apply' measurableSet_ball,

Goal state after:
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
μ : Measure E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
inst✝ : μ.IsAddHaarMeasure
x : ↑(sphere 0 1)
this : Nontrivial E
ε : ℝ
hε : 0 < ε
hε₂ : ε ≤ 2
⊢ ↑(toSphereBallBound (dim E) ε) * μ (ball 0 1) ≤ ↑(dim E) * μ (Ioo 0 1 • Subtype.val '' ball x ε)
Module: Mathlib.Analysis.SpecialFunctions.RegularizedHypergeometric

Goal state before:
pp: a b : Multiset ℂ
n : ℕ
hb : ∀ k ∈ b, k ≠ -↑n
⊢ (Multiset.map (fun i ↦ Polynomial.eval i (ascPochhammer ℂ n) * (i + ↑n)) a).prod /
      (↑n ! * (↑n + 1) * (Multiset.map (fun j ↦ Gamma (j + ↑n) * (j + ↑n)) b).prod) =
    (Multiset.map (fun x ↦ Polynomial.eval x (ascPochhammer ℂ n)) a).prod * (Multiset.map (fun x ↦ x + ↑n) a).prod /
      (↑n ! * (Multiset.map (fun x ↦ Gamma (x + ↑n)) b).prod * ((Multiset.map (fun x ↦ x + ↑n) b).prod * (↑n + 1)))

Tactic:
Multiset.prod_map_mul

Goal state after:
a b : Multiset ℂ
n : ℕ
hb : ∀ k ∈ b, k ≠ -↑n
⊢ (Multiset.map (fun i ↦ Polynomial.eval i (ascPochhammer ℂ n)) a).prod * (Multiset.map (fun i ↦ i + ↑n) a).prod /
      (↑n ! * (↑n + 1) * ((Multiset.map (fun i ↦ Gamma (i + ↑n)) b).prod * (Multiset.map (fun i ↦ i + ↑n) b).prod)) =
    (Multiset.map (fun i ↦ Polynomial.eval i (ascPochhammer ℂ n)) a).prod * (Multiset.map (fun i ↦ i + ↑n) a).prod /
      (↑n ! * (Multiset.map (fun i ↦ Gamma (i + ↑n)) b).prod * ((Multiset.map (fun i ↦ i + ↑n) b).prod * (↑n + 1)))
Module: Mathlib.Analysis.SpecialFunctions.RegularizedHypergeometric

Goal state before:
pp: a b : Multiset ℂ
n : ℕ
hb : ∀ k ∈ b, k ≠ -↑n
⊢ (Multiset.map (fun i ↦ Polynomial.eval i (ascPochhammer ℂ n) * (i + ↑n)) a).prod /
      (↑n ! * (↑n + 1) * (Multiset.map (fun j ↦ Gamma (j + ↑n) * (j + ↑n)) b).prod) =
    (Multiset.map (fun x ↦ Polynomial.eval x (ascPochhammer ℂ n)) a).prod /
        (↑n ! * (Multiset.map (fun x ↦ Gamma (x + ↑n)) b).prod) *
      ((Multiset.map (fun x ↦ x + ↑n) a).prod / ((Multiset.map (fun x ↦ x + ↑n) b).prod * (↑n + 1)))

Tactic:
simp_rw [div_mul_div_comm, Multiset.prod_map_mul]

Goal state after:
a b : Multiset ℂ
n : ℕ
hb : ∀ k ∈ b, k ≠ -↑n
⊢ (Multiset.map (fun i ↦ Polynomial.eval i (ascPochhammer ℂ n)) a).prod * (Multiset.map (fun i ↦ i + ↑n) a).prod /
      (↑n ! * (↑n + 1) * ((Multiset.map (fun i ↦ Gamma (i + ↑n)) b).prod * (Multiset.map (fun i ↦ i + ↑n) b).prod)) =
    (Multiset.map (fun i ↦ Polynomial.eval i (ascPochhammer ℂ n)) a).prod * (Multiset.map (fun i ↦ i + ↑n) a).prod /
      (↑n ! * (Multiset.map (fun i ↦ Gamma (i + ↑n)) b).prod * ((Multiset.map (fun i ↦ i + ↑n) b).prod * (↑n + 1)))
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 : ℕ
hn₁ : regularizedHGFunCoeff a b n ≠ 0
hn₂ : 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)⁻¹)))‖ =
    ‖(Multiset.map (fun x ↦ x + ↑n) a).prod / ((Multiset.map (fun x ↦ x + ↑n) b).prod * (↑n + 1))‖

Tactic:
multiset_prod_div_multiset_prod_mul a b 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
hn₂ : 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)⁻¹)))‖ =
    ‖↑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)⁻¹))‖
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.ContDiff

Goal state before:
pp: case inl
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
inst✝ : CompleteSpace E
h : ContDiffOn ℝ 1 f [[a, b]]
hab : a ≤ b
⊢ ∫ (x : ℝ) in a..b, deriv f x = f b - f a

Tactic:
simp only [uIcc_of_le hab] at h
    exact integral_deriv_of_contDiffOn_Icc h hab

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

Goal state before:
pp: case h₁
L : PeriodPair
l₀ z x : ℂ
hx : ∀ (l : ↥L.lattice), ↑l ≠ l₀ → ‖z - x‖ < ‖↑l - x‖
κ : ℝ
hκ : 1 < κ
hκ' : ∀ (l : ↥L.lattice), ↑l ≠ l₀ → ‖z - x‖ * κ < ‖↑l - x‖
e : ℕ × ↥L.lattice ≃ ↥L.lattice ⊕ ℕ × ↥L.lattice := ⋯
⊢ Summable (((Function.uncurry fun b c ↦ L.weierstrassPExceptSummand l₀ x b c * (z - x) ^ b) ∘ ⇑e.symm) ∘ Sum.inl)

pp: case h₂
L : PeriodPair
l₀ z x : ℂ
hx : ∀ (l : ↥L.lattice), ↑l ≠ l₀ → ‖z - x‖ < ‖↑l - x‖
κ : ℝ
hκ : 1 < κ
hκ' : ∀ (l : ↥L.lattice), ↑l ≠ l₀ → ‖z - x‖ * κ < ‖↑l - x‖
e : ℕ × ↥L.lattice ≃ ↥L.lattice ⊕ ℕ × ↥L.lattice := ⋯
⊢ Summable (((Function.uncurry fun b c ↦ L.weierstrassPExceptSummand l₀ x b c * (z - x) ^ b) ∘ ⇑e.symm) ∘ Sum.inr)

Tactic:
· -- for the degree zero term, this is the usual summability of the definition of `℘`.
    simpa [weierstrassPExceptSummand, e, Function.comp_def, Function.uncurry, sub_sq_comm x,
      Denumerable.eqv] using! (L.hasSum_weierstrassPExcept l₀ x).summable

Goal state after:
case h₂
L : PeriodPair
l₀ z x : ℂ
hx : ∀ (l : ↥L.lattice), ↑l ≠ l₀ → ‖z - x‖ < ‖↑l - x‖
κ : ℝ
hκ : 1 < κ
hκ' : ∀ (l : ↥L.lattice), ↑l ≠ l₀ → ‖z - x‖ * κ < ‖↑l - x‖
e : ℕ × ↥L.lattice ≃ ↥L.lattice ⊕ ℕ × ↥L.lattice := ⋯
⊢ Summable (((Function.uncurry fun b c ↦ L.weierstrassPExceptSummand l₀ x b c * (z - x) ^ b) ∘ ⇑e.symm) ∘ Sum.inr)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Orthogonality

Goal state before:
pp: n : ℕ
hn : n ≠ 0
⊢ (0 + ∫ (x : ℝ), eval x (T ℝ 0) ∂measureT) / 2 = π / 2

Tactic:
integral_eval_T_real_measureT_zero,

Goal state after:
n : ℕ
hn : n ≠ 0
⊢ (0 + π) / 2 = π / 2
Module: Mathlib.NumberTheory.Niven

Goal state before:
pp: q : ℚ
⊢ cexp (↑q * ↑π * I) ^ (2 * q.den) = 1

Tactic:
nth_rw 1 [← q.num_div_den, ← exp_nat_mul]
  push_cast
  rw [show 2 * q.den * (q.num / q.den * π * I) = q.num * (2 * π * I) by field,
    exp_int_mul_two_pi_mul_I]

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

Goal state before:
pp: n : ℕ
ι : Type u_1
s : Finset ι
P : ι → ℝ[X]
⊢ sumZeroes n (∑ i ∈ s, P i) = ∑ i ∈ s, sumZeroes n (P i)

Tactic:
by
  simp_rw [sumZeroes, eval_finsetSum]
  rw [sum_comm, mul_sum]

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

Goal state before:
pp: n : ℕ
hn : n ≠ 0
c : ℕ → ℝ
hP : (∑ i ∈ range (2 * n), c i • ↑(chebyshevTsequence ℝ) i).degree < 2 * ↑n
i : ℕ
hrange : i ∈ range (2 * n)
hi : i = 0
⊢ ∫ (a : ℝ), eval a (T ℝ 0) ∂measureT = sumZeroes n (T ℝ 0)

Tactic:
integral_eval_T_real_measureT_zero,

Goal state after:
n : ℕ
hn : n ≠ 0
c : ℕ → ℝ
hP : (∑ i ∈ range (2 * n), c i • ↑(chebyshevTsequence ℝ) i).degree < 2 * ↑n
i : ℕ
hrange : i ∈ range (2 * n)
hi : i = 0
⊢ π = sumZeroes n (T ℝ 0)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema

Goal state before:
pp: n : ℤ
x : ℝ
hx : x ∈ Set.Icc (-1) 1
⊢ eval x (T ℝ n) ∈ Set.Icc (-1) 1

Tactic:
← cos_arccos (x := x) (by grind) (by grind)

Goal state after:
n : ℤ
x : ℝ
hx : x ∈ Set.Icc (-1) 1
⊢ eval (cos (arccos x)) (T ℝ n) ∈ Set.Icc (-1) 1
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable

Goal state before:
pp: z : ℍ
k : ℝ
hk : 0 ≤ k
x : Fin 2 → ℤ
A B : ℝ
hB : 0 < B
hz : z ∈ verticalStrip A B
⊢ r z ^ (-k) ≤ r { coe := { re := A, im := B }, coe_im_pos := hB } ^ (-k)

Tactic:
exact Real.rpow_le_rpow_of_nonpos (r_pos _) (r_lower_bound_on_verticalStrip z hB hz)
    (neg_nonpos.mpr hk)

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

Goal state before:
pp: L : PeriodPair
⊢ Meromorphic L.relation

Tactic:
have : Meromorphic fun z ↦ ℘'[L] z ^ 2 - 4 * ℘[L] z ^ 3 + L.g₂ * ℘[L] z + L.g₃ := by fun_prop
  refine fun z ↦ (this _).congr ?_
  filter_upwards [self_mem_nhdsWithin, mem_nhdsWithin_of_mem_nhds
    (L.compl_lattice_sdiff_singleton_mem_nhds _)] with w hw hw'
  rw [relation, if_neg (by simp_all)]

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

Goal state before:
pp: case mpr
n : ℕ
hn : 2 ≤ n
x : ℝ
⊢ (∃ k ∈ Finset.Ioo 0 n, x = cos (↑k * π / ↑n)) → IsLocalExtr (fun x ↦ eval x (T ℝ ↑n)) x

Tactic:
rintro ⟨k, hk, hx⟩
    rw [hx]
    exact isLocalExtr_T_real (Nat.ne_zero_of_lt hn)
      (Finset.mem_Ioo.mp hk).1 (Finset.mem_Ioo.mp hk).2

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

Goal state before:
pp: k : ℕ
hk : 1 ≤ k
K : Set ℍ
hKc : IsCompact (UpperHalfPlane.coe '' K)
A B : ℝ
hB : 0 < B
HABK : K ⊆ verticalStrip A B
⊢ ∃ u,
    Summable u ∧ ∀ (n : ℕ), ∀ k_1 ∈ UpperHalfPlane.coe '' K, ‖iteratedDerivWithin k (fun z ↦ cotTerm z n) ℍₒ k_1‖ ≤ u n

Tactic:
exact ⟨cotTermUpperBound k A B hB, summable_cotTermUpperBound A B hB hk,
    iteratedDerivWithin_cotTerm_bounded_uniformly A B hB <| by gcongr⟩

Goal state after:
Module: Mathlib.Analysis.Subadditive

Goal state before:
pp: u : ℕ → ℝ
h : Subadditive u
n r k : ℕ
IH : u (k * n + r) ≤ ↑k * u n + u r
⊢ u n + u (k * n + r) ≤ u n + (↑k * u n + u r)

Tactic:
IH

Goal state after:
u : ℕ → ℝ
h : Subadditive u
n r k : ℕ
IH : u (k * n + r) ≤ ↑k * u n + u r
⊢ u n + (↑k * u n + u r) ≤ u n + (↑k * u n + u r)