mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Deligne

Goal state before:
pp: s : ℂ
hs : ∀ (n : ℕ), s ≠ -↑n
h : s = 1
⊢ 2 - 1 = 1

Tactic:
ring

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

Goal state before:
pp: s : ℂ
hs : ∀ (n : ℕ), s ≠ -↑n
h : s - 1 ≠ 0
m : ℕ
⊢ -(↑m + 1) + 1 = -↑m

Tactic:
ring

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

Goal state before:
pp: s : ℂ
hs : ∀ (n : ℕ), s ≠ -↑n
h : s - 1 ≠ 0
h' : ∀ (n : ℕ), s - 1 ≠ -↑n
⊢ 2 - s = 1 - (s - 1)

Tactic:
ring

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

Goal state before:
pp: s : ℂ
hs : ∀ (n : ℕ), s ≠ -↑n
h : s - 1 ≠ 0
h' : ∀ (n : ℕ), s - 1 ≠ -↑n
⊢ s + 1 = s - 1 + 2

Tactic:
ring

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

Goal state before:
pp: case succ
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
n : ℕ
hn : deriv f (↑n + 1) = deriv f 1 + ↑(harmonic n)
⊢ deriv f 1 + ↑(harmonic n) + 1 / (↑n + 1) = deriv f 1 + (↑(harmonic n) + (↑n + 1)⁻¹)

Tactic:
ring

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

Goal state before:
pp: p t : ℝ
hp : p ∈ Ioo 1 2
ht : 0 < t
⊢ MonotoneOn (p.rpowIntegrand₁₂ t) (Ici 0)

Tactic:
refine MonotoneOn.congr ?_ fun x hx ↦ (rpowIntegrand₁₂_eq_mul_rpowIntegrand₀₁ hx ht).symm
  apply monotoneOn_id.mul <;> grind [rpowIntegrand₀₁_monotoneOn, rpowIntegrand₀₁_nonneg]

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

Goal state before:
pp: 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)
n : ℕ
hn : 0 < n
⊢ ↑n + 1 - ↑n = 1

Tactic:
ring

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

Goal state before:
pp: 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)
n : ℕ
⊢ ↑n + 2 - (↑n + 1) = 1

Tactic:
ring

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

Goal state before:
pp: 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)
n : ℕ
⊢ ↑n + 2 = ↑n + 1 + 1

Tactic:
ring

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)
x : ℝ
⊢ -(↑π * a⁻¹ * ↑x * I * b * 2) - ↑π * a⁻¹ * ↑x ^ 2 - ↑π * a⁻¹ * -1 * b ^ 2 =
    -(↑π * a⁻¹ * ↑x * I * b * 2) - ↑π * a⁻¹ * ↑x ^ 2 + ↑π * a⁻¹ * b ^ 2

Tactic:
ring

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 * γ + -(2 * log 2) + γ) = -√π * (γ + 2 * log 2)

Tactic:
ring

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 ^ log b r ≤ r

pp: case inr
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 : r ≤ 1
⊢ ↑b ^ log b r ≤ r

Tactic:
· rw [log_of_one_le_right _ hr1]
    rw [zpow_natCast, ← Nat.cast_pow, ← Nat.le_floor_iff hr.le]
    exact Nat.pow_log_le_self b (Nat.floor_pos.mpr hr1).ne'

Goal state after:
case inr
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 : r ≤ 1
⊢ ↑b ^ log b r ≤ r
Module: Mathlib.Analysis.SpecialFunctions.Log.Base

Goal state before:
pp: case a
b x : ℝ
b_pos : 0 < b
b_ne_one : b ≠ 1
hx : x ≠ 0
⊢ b ^ logb b x ∈ Ioi 0

Tactic:
simp only [Set.mem_Ioi]
    apply rpow_pos_of_pos b_pos

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

Goal state before:
pp: ε y : ℝ
⊢ -(ε * 1 * y + ε * y * 1) = -2 * ε * y

Tactic:
ring

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

Goal state before:
pp: x : ℝ
hex : x ∈ Ici (rexp 1)
y : ℝ
hey : y ∈ Ici (rexp 1)
hxy : x ≤ y
x_pos : 0 < x
y_pos : 0 < y
hlogx : 1 ≤ log x
hyx : 0 ≤ y / x - 1
⊢ log x * (y / x - 1) = log x / x * y - log x

Tactic:
ring

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

Goal state before:
pp: ε : ℝ
hε : 0 < ε
x : ℝ
⊢ rexp (-(ε * x * x)) + x * (rexp (-(ε * x * x)) * (-2 * ε * x)) = rexp (-(ε * x * x)) * (1 - 2 * (ε * x * x))

Tactic:
ring

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

Goal state before:
pp: ε : ℝ
hε : 0 < ε
x : ℝ
⊢ (√ε)⁻¹ * |mulExpNegMulSq 1 (√ε * x)| ≤ (√ε)⁻¹

Tactic:
apply mul_le_of_le_one_right

Goal state after:
case ha
ε : ℝ
hε : 0 < ε
x : ℝ
⊢ 0 ≤ (√ε)⁻¹

case h
ε : ℝ
hε : 0 < ε
x : ℝ
⊢ |mulExpNegMulSq 1 (√ε * x)| ≤ 1
Module: Mathlib.MeasureTheory.Integral.BoundedContinuousFunction

Goal state before:
pp: X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : MeasurableSpace X
μ : Measure X
inst✝ : IsFiniteMeasure μ
f : X →ᵇ ℝ≥0
⊢ ∫⁻ (x : X), ↑(f x) ∂μ < ∞

Tactic:
apply IsFiniteMeasure.lintegral_lt_top_of_bounded_to_ennreal
  refine ⟨nndist f 0, fun x ↦ ?_⟩
  have key := BoundedContinuousFunction.NNReal.upper_bound f x
  rwa [ENNReal.coe_le_coe]

Goal state after:
Module: Mathlib.MeasureTheory.Constructions.HaarToSphere

Goal state before:
pp: E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
hx : ‖x‖ = 1
ε : ℝ
hε : 0 < ε
hε2 : ε ≤ 2
y : E
hy : dist y ((1 - ε / 4) • x) < ε / 4
habs : |1 - ε / 4| = 1 - ε / 4
hy₀ : y ≠ 0
hy₁ : ‖y‖ < 1
u : E := ‖y‖⁻¹ • y
hu₁ : ‖u‖ = 1
⊢ ε / 4 + ε / 4 = ε / 2

Tactic:
ring

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

Goal state before:
pp: case e_a
r : ℝ
hr : 0 < r
s : ℂ
hs : ‖s‖ < r
l : ℂ
h : 2 * r ≤ ‖l‖
this✝ : s ≠ l
this : 0 < ‖l‖
⊢ (‖l‖ / 2) ^ 2 * ‖l‖ ^ 2 = ‖l‖ ^ 4 / 4

Tactic:
ring

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

Goal state before:
pp: n : ℕ
hn : n ≠ 0
a : ℕ
⊢ a < (n.nthRoot a + 1) ^ n

Tactic:
match n, hn with
  | 1, _ => simp
  | n + 2, hn =>
    simp only [nthRoot]
    apply nthRoot.lt_pow_go_succ
    exact a.lt_succ_self.trans_le (Nat.le_self_pow hn _)

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

Goal state before:
pp: case h₃
L : PeriodPair
l₀ z : ℂ
l : ↥L.lattice
a✝ : ¬↑l = -l₀
⊢ (-z + ↑l) ^ 2 = (z - ↑l) ^ 2

Tactic:
ring

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

Goal state before:
pp: case e_f
L : PeriodPair
z : ℂ
l : ↥L.lattice
⊢ (-z + ↑l) ^ 2 = (z - ↑l) ^ 2

Tactic:
ring

Goal state after:
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)) 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)))

Tactic:
ring

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

Goal state before:
pp: L : PeriodPair
l₀ : ℂ
r : ℝ
hr : r > 0
s : ℂ
hs : ‖s‖ < r
l : ↥L.lattice
h : 2 * r ≤ ‖↑l‖
h✝ : ¬↑l = l₀
this✝ : s ≠ ↑l
this : l ≠ 0
⊢ 2 * (2 * ‖↑l - s‖) ^ 3 = 16 * ‖↑l - s‖ ^ 3

Tactic:
ring

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

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

Tactic:
ring

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

Goal state before:
pp: case pos
a b : Multiset ℂ
h : a.card ≤ b.card
ha : ∃ j ∈ a, ∃ k, j = -↑k
⊢ (regularizedHGFunSeries a b).radius = ⊤

Tactic:
obtain ⟨j, hj, k, ha⟩ := ha

Goal state after:
case pos
a b : Multiset ℂ
h : a.card ≤ b.card
j : ℂ
hj : j ∈ a
k : ℕ
ha : j = -↑k
⊢ (regularizedHGFunSeries a b).radius = ⊤
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: case e'_5.h₃
L : PeriodPair
l₀ z : ℂ
l : ↥L.lattice
a✝ : ¬↑l = -l₀
⊢ -2 / (↑l - z) ^ 3 = -2 / -(z - ↑l) ^ 3

Tactic:
ring

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

Goal state before:
pp: case e_a.e_z
L : PeriodPair
l₀ : ℂ
hl₀ : l₀ ∈ L.lattice
l : ↥L.lattice
hl : ↑l / 2 ∉ L.lattice
⊢ -(↑l / 2) + ↑l = ↑l / 2

Tactic:
ring

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

Goal state before:
pp: case e_a
L : PeriodPair
l₀ : ℂ
hl₀ : l₀ ∈ L.lattice
l : ↥L.lattice
hl : ↑l / 2 ∉ L.lattice
⊢ 1 / ↑⟨l₀, hl₀⟩ ^ 2 - 1 / (-(↑l / 2) + ↑l - ↑⟨l₀, hl₀⟩) ^ 2 =
    1 / ↑⟨-(l₀ - ↑l), ⋯⟩ ^ 2 - 1 / (↑l / 2 - ↑⟨-(l₀ - ↑l), ⋯⟩) ^ 2 + (1 / l₀ ^ 2 - 1 / (l₀ - ↑l) ^ 2)

Tactic:
ring

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

Goal state before:
pp: case pos
L : PeriodPair
z : ℂ
l : ↥L.lattice
hl : ↑l / 2 ∉ L.lattice
hl0 : l ≠ 0
hz : z ∈ L.lattice
this : ℘[L - z + ↑l] (z + ↑l) = ℘[L - z + ↑l - ↑l] z + (1 / (z + ↑l) ^ 2 - 1 / (z + ↑l - ↑l) ^ 2)
⊢ ℘[L - z] z + (((z + ↑l) ^ 2)⁻¹ - (z ^ 2)⁻¹) + -((z + ↑l) ^ 2)⁻¹ = ℘[L - z] z + -(z ^ 2)⁻¹

Tactic:
ring

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

Goal state before:
pp: case neg
L : PeriodPair
z : ℂ
l : ↥L.lattice
hl : ↑l / 2 ∉ L.lattice
hl0 : l ≠ 0
hz : z ∉ L.lattice
this : ℘[L - 0] (z + ↑l) = ℘[L - -↑l] z + -(↑l ^ 2)⁻¹
⊢ ℘[L - -↑l] z + -(↑l ^ 2)⁻¹ + ((z + ↑l) ^ 2)⁻¹ = ℘[L - -↑l] z + (((z + ↑l) ^ 2)⁻¹ - (↑l ^ 2)⁻¹)

Tactic:
ring

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

Goal state before:
pp: case one
θ : ℂ
⊢ 2 * cos θ * sin θ = 2 * sin θ * cos θ

Tactic:
ring

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

Goal state before:
pp: case neg_add_one
θ : ℂ
n : ℕ
ih1 : eval (cos θ) (U ℂ (-↑n)) * sin θ = sin ((↑(-↑n) + 1) * θ)
ih2 : eval (cos θ) (U ℂ (-↑n + 1)) * sin θ = sin ((↑(-↑n + 1) + 1) * θ)
⊢ eval (cos θ) (U ℂ (-↑n - 1)) * sin θ = sin ((↑(-↑n - 1) + 1) * θ)

Tactic:
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]

Goal state after:
case neg_add_one
θ : ℂ
n : ℕ
ih1 : eval (cos θ) (U ℂ (-↑n)) * sin θ = sin ((↑(-↑n) + 1) * θ)
ih2 : eval (cos θ) (U ℂ (-↑n + 1)) * sin θ = sin ((↑(-↑n + 1) + 1) * θ)
⊢ 2 * (cos θ * sin ((↑(-↑n) + 1) * θ)) =
    2 *
      (sin (((↑(-↑n + 1) + 1) * θ + (↑(-↑n - 1) + 1) * θ) / 2) *
        cos (((↑(-↑n + 1) + 1) * θ - (↑(-↑n - 1) + 1) * θ) / 2))
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.InverseDeriv

Goal state before:
pp: x : ℝ
h₁✝ : x ≠ -1
h₂ : x ≠ 1
h₁ : x < -1
⊢ 1 - x ^ 2 < 0

Tactic:
nlinarith [h₁]

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

Goal state before:
pp: L : PeriodPair
z : ℂ
l : ↥L.lattice
⊢ -(↑l - z) ^ 3 = (z - ↑l) ^ 3

Tactic:
ring

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

Goal state before:
pp: ⊢ stirlingSeq 0 = 0

Tactic:
stirlingSeq,

Goal state after:
⊢ ↑0! / (√(2 * ↑0) * (↑0 / rexp 1) ^ 0) = 0
Module: Mathlib.Analysis.SpecialFunctions.Stirling

Goal state before:
pp: ⊢ stirlingSeq 1 = rexp 1 / √2

Tactic:
stirlingSeq,

Goal state after:
⊢ ↑1! / (√(2 * ↑1) * (↑1 / rexp 1) ^ 1) = rexp 1 / √2
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: L : PeriodPair
⊢ ℘'[L] 0 = -℘'[L] 0

Tactic:
← L.derivWeierstrassP_neg,

Goal state after:
L : PeriodPair
⊢ ℘'[L] 0 = ℘'[L] (-0)
Module: Mathlib.Analysis.SpecialFunctions.Stirling

Goal state before:
pp: case succ
n✝ : ℕ
⊢ log (stirlingSeq (n✝ + 1)) = log ↑(n✝ + 1)! - 1 / 2 * log (2 * ↑(n✝ + 1)) - ↑(n✝ + 1) * log (↑(n✝ + 1) / rexp 1)

Tactic:
stirlingSeq,

Goal state after:
case succ
n✝ : ℕ
⊢ log (↑(n✝ + 1)! / (√(2 * ↑(n✝ + 1)) * (↑(n✝ + 1) / rexp 1) ^ (n✝ + 1))) =
    log ↑(n✝ + 1)! - 1 / 2 * log (2 * ↑(n✝ + 1)) - ↑(n✝ + 1) * log (↑(n✝ + 1) / rexp 1)
Module: Mathlib.Analysis.SpecialFunctions.Stirling

Goal state before:
pp: case e'_6
m : ℕ
f : ℕ → ℝ := fun k ↦ 1 / (2 * ↑k + 1) * ((1 / (2 * ↑(m + 1) + 1)) ^ 2) ^ k
h : ∀ (x : ℝ), x ≠ 0 → 1 + x⁻¹ = (x + 1) / x
⊢ log (↑m + 1) + log ↑m ! - 1 / 2 * (log 2 + log (↑m + 1)) - (↑m + 1) * (log (↑m + 1) - 1) -
        (log (↑m + 1 + 1) + (log (↑m + 1) + log ↑m !) - 1 / 2 * (log 2 + log (↑m + 1 + 1)) -
          (↑m + 1 + 1) * (log (↑m + 1 + 1) - 1)) +
      f 0 =
    (↑m + 1 + 1 / 2) * (log (↑m + 1 + 1) - log (↑m + 1))

Tactic:
ring

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

Goal state before:
pp: case neg
L : PeriodPair
l₀ x : ℂ
i : ℕ
hl₀ : l₀ ∈ L.lattice
l : ↥L.lattice
e : ¬↑l = l₀
⊢ ↑(i + 2) * (((↑l - x) ^ (i + 3))⁻¹ - 0) = ↑(i + 1 + 1) * ((↑l - x) ^ (i + 1 + 2))⁻¹ - 0

Tactic:
ring

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

Goal state before:
pp: n : ℕ
hn : n ≠ 0
this : 4 = 2 * 2
⊢ stirlingSeq n ^ 4 / stirlingSeq (2 * n) ^ 2 * (↑n / (2 * ↑n + 1)) = Wallis.W n

Tactic:
stirlingSeq,

Goal state after:
n : ℕ
hn : n ≠ 0
this : 4 = 2 * 2
⊢ (↑n ! / (√(2 * ↑n) * (↑n / rexp 1) ^ n)) ^ 4 / stirlingSeq (2 * n) ^ 2 * (↑n / (2 * ↑n + 1)) = Wallis.W n
Module: Mathlib.Analysis.SpecialFunctions.Stirling

Goal state before:
pp: n : ℕ
hn : n ≠ 0
this : 4 = 2 * 2
⊢ ((↑n ! / (√(2 * ↑n) * (↑n / rexp 1) ^ n)) ^ 2) ^ 2 / stirlingSeq (2 * n) ^ 2 * (↑n / (2 * ↑n + 1)) = Wallis.W n

Tactic:
stirlingSeq,

Goal state after:
n : ℕ
hn : n ≠ 0
this : 4 = 2 * 2
⊢ ((↑n ! / (√(2 * ↑n) * (↑n / rexp 1) ^ n)) ^ 2) ^ 2 /
        (↑(2 * n)! / (√(2 * ↑(2 * n)) * (↑(2 * n) / rexp 1) ^ (2 * n))) ^ 2 *
      (↑n / (2 * ↑n + 1)) =
    Wallis.W n
Module: Mathlib.Analysis.SpecialFunctions.Stirling

Goal state before:
pp: n : ℕ
hn : n ≠ 0
⊢ √2 * √π * √↑n * (↑n / rexp 1) ^ n = √π * (√2 * √↑n * (↑n / rexp 1) ^ n)

Tactic:
ring

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

Goal state before:
pp: n : ℕ
hn : n ≠ 0
⊢ ↑n * log ↑n - ↑n + log ↑n / 2 + log (2 * π) / 2 = (log (2 * π) + log ↑n) / 2 + ↑n * (log ↑n - 1)

Tactic:
ring

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

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

Tactic:
suffices (∑ i ∈ range n, exp ((k * ((2 * i + 1) / (2 * n) * π)) * I)) *
    exp (-(k / (2 * n) * π * I)) * (exp (k / n * π * I) - 1) = (-1) ^ k - 1 by
    rw [Complex.exp_neg] at this
    have hf {s a b t : ℂ} (h : s * a⁻¹ * b = t) (ha : a ≠ 0) (hb : b ≠ 0) : s = a / b * t := by
      linear_combination (norm := field) h * a / b
    apply hf this (Complex.exp_ne_zero _) (by grind [exp_sub_one_ne_zero])

Goal state after:
n : ℕ
k : ℤ
hn : n ≠ 0
hk : ¬2 * ↑n ∣ k
⊢ (∑ i ∈ range n, Complex.exp (↑k * ((2 * ↑i + 1) / (2 * ↑n) * ↑π) * I)) * Complex.exp (-(↑k / (2 * ↑n) * ↑π * I)) *
      (Complex.exp (↑k / ↑n * ↑π * I) - 1) =
    (-1) ^ k - 1
Module: Mathlib.NumberTheory.Niven

Goal state before:
pp: q : ℚ
⊢ IsIntegral ℤ ((cexp (-(↑q * ↑π) * I) - cexp (↑q * ↑π * I)) * I)

Tactic:
exact (isIntegral_exp_neg_rat_mul_pi_mul_I q).sub (isIntegral_exp_rat_mul_pi_mul_I q)
    |>.mul isIntegral_int_I

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

Goal state before:
pp: α β : ℝ
i : ℕ
⊢ (-1) ^ i * α * ((-1) ^ i * β) = (-1) ^ i * (-1) ^ i * α * β

Tactic:
ring

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

Goal state before:
pp: n : ℕ
c : ℝ
P : ℝ[X]
⊢ π / ↑n * (c * ∑ x ∈ range n, eval (cos ((2 * ↑x + 1) / (2 * ↑n) * π)) P) =
    c * (π / ↑n * ∑ x ∈ range n, eval (cos ((2 * ↑x + 1) / (2 * ↑n) * π)) P)

Tactic:
ring

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

Goal state before:
pp: case grind
n : ℕ
c : ℕ → ℝ
hcpos : ∀ i ≤ n, 0 < (-1) ^ i * c i
P : ℝ[X]
hPdeg : P.degree ≤ ↑n
hPbnd : ∀ x ∈ Set.Icc (-1) 1, |eval x P| ≤ 1
x : ℝ
hx : x ∈ Finset.image (fun x ↦ node n x) (Finset.range (n + 1))
hPx : eval x P ≠ eval x (T ℝ ↑n)
i : ℕ
hix : node n i = x
hi : i ∈ Finset.Iic n
h_le :
  ∀ {i : ℕ},
    i ∈ Finset.Iic n →
      (-1) ^ i * eval (node n i) P * ((-1) ^ i * c i) ≤ (-1) ^ i * eval (node n i) (T ℝ ↑n) * ((-1) ^ i * c i)
this : 0 ≠ (-1) ^ i * c i
h✝ : (-1) ^ i * eval (node n i) P * ((-1) ^ i * c i) = (-1) ^ i * eval (node n i) (T ℝ ↑n) * ((-1) ^ i * c i)
⊢ False

Tactic:
ring

Goal state after:
Module: Mathlib.Order.Interval.Finset.Box

Goal state before:
pp: α : Type u_1
inst✝⁴ : Ring α
inst✝³ : PartialOrder α
inst✝² : IsOrderedRing α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
n : ℕ
⊢ box (n + 1) = Icc (-↑n.succ) ↑n.succ \ Icc (-↑n) ↑n

Tactic:
rw [box, Icc_neg_mono.disjointed_add_one]
  simp only [Nat.cast_add_one, Nat.succ_eq_add_one]

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

Goal state before:
pp: n : ℕ
P : ℝ[X]
hPbnd : ∀ x ∈ Set.Icc (-1) 1, |eval x P| ≤ 1
hP : ¬P = 0
d : ℕ
hd : ↑d = P.degree
hPdeg : d ≤ n
⊢ P.coeff d ≤ 2 ^ (n - 1)

Tactic:
coeff_le_of_forall_abs_le_one (le_of_eq hd.symm) hPbnd,

Goal state after:
n : ℕ
P : ℝ[X]
hPbnd : ∀ x ∈ Set.Icc (-1) 1, |eval x P| ≤ 1
hP : ¬P = 0
d : ℕ
hd : ↑d = P.degree
hPdeg : d ≤ n
⊢ 2 ^ (d - 1) ≤ 2 ^ (n - 1)
Module: Mathlib.Order.Interval.Finset.Box

Goal state before:
pp: n : ℕ
x✝ : n + 1 ≠ 0
⊢ (↑n + 1 + 1 + (↑n + 1)) * (↑n + 1 + 1 + (↑n + 1)) = 8 * (↑n + 1) + (↑n + 1 + ↑n) * (↑n + 1 + ↑n)

Tactic:
ring

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

Goal state before:
pp: z : ℍ
c d : ℝ
hd : 1 ≤ d ^ 2
⊢ (c * z.re + d) ^ 2 + (c * z.im) ^ 2 = c ^ 2 * (z.re ^ 2 + z.im ^ 2) + d * 2 * c * z.re + d ^ 2

Tactic:
ring

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

Goal state before:
pp: z : ℍ
c d : ℝ
hd : 1 ≤ d ^ 2
H1 : (c * z.re + d) ^ 2 + (c * z.im) ^ 2 = c ^ 2 * (z.re ^ 2 + z.im ^ 2) + d * 2 * c * z.re + d ^ 2
⊢ (c ^ 2 * (z.re ^ 2 + z.im ^ 2) + d * 2 * c * z.re + d ^ 2) * (z.re ^ 2 + z.im ^ 2) - z.im ^ 2 =
    (c * (z.re ^ 2 + z.im ^ 2) + d * z.re) ^ 2 + (d ^ 2 - 1) * z.im ^ 2

Tactic:
ring

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

Goal state before:
pp: case e'_10
L : PeriodPair
l₀ x : ℂ
r : NNReal
hr0 : 0 < r
hr : Metric.closedBall x ↑r ⊆ (↑L.lattice \ {l₀})ᶜ
this : HasFPowerSeriesOnBall (fderiv ℂ ℘[L - l₀]) (L.weierstrassPExceptSeries l₀ x).derivSeries x ↑r
n : ℕ
⊢ (↑n + 1) * (↑n + 2) * (L.sumInvPow x (n + 3) - if l₀ ∈ L.lattice then ((l₀ - x) ^ (n + 3))⁻¹ else 0) =
    (↑n + 1) * ((↑n + 1 + 1) * (L.sumInvPow x (n + 1 + 2) - if l₀ ∈ L.lattice then ((l₀ - x) ^ (n + 1 + 2))⁻¹ else 0))

Tactic:
ring

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

Goal state before:
pp: case h
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
⊢ (k + 1) * (n + 1) = (n + 1) * (k + 1)

Tactic:
ring

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)
⊢ eval x (U ℝ ↑n) = 0

pp: case refine_2
n : ℕ
hn : n ≠ 0
⊢ ↑(Finset.image (fun k ↦ cos ((↑k + 1) * π / (↑n + 1))) (Finset.range n)).card = (U ℝ ↑n).degree

Tactic:
· obtain ⟨k, hk, hx⟩ := Finset.mem_image.mp hx
    suffices (U ℝ n).eval x * sin ((k + 1) * π / (n + 1)) = 0 by
      refine (mul_eq_zero_iff_right (ne_of_gt (sin_pos_of_pos_of_lt_pi (by positivity) ?_))).mp this
      field_simp
      norm_cast
      grind
    rw [← hx, U_real_cos, sin_eq_zero_iff]
    use k + 1
    field_simp
    norm_cast
    ring

Goal state after:
case refine_2
n : ℕ
hn : n ≠ 0
⊢ ↑(Finset.image (fun k ↦ cos ((↑k + 1) * π / (↑n + 1))) (Finset.range n)).card = (U ℝ ↑n).degree
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: L : PeriodPair
⊢ -(2 * (20 * (↑5! * L.G 6) * ↑3!)) + -(20 * (↑5! * L.G 6) * ↑3! * 2) -
        4 * (15 * (↑5! * L.G 6) * 2 + (15 * (↑5! * L.G 6) * 2 + 15 * (↑5! * L.G 6) * 2)) +
      140 * L.G 6 * ↑6! =
    0

Tactic:
ring

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

Goal state before:
pp: case neg.inr
L : PeriodPair
hi₁ : 4 < 7
hi₂ : ¬Odd 4
hi₃ : ¬4 = 0
hi₄ : ¬4 = 6
⊢ -(2 * (4 * (↑3! * L.G 4) * ↑3!)) + -(4 * (↑3! * L.G 4) * ↑3! * 2) -
        4 * (6 * (↑3! * L.G 4) * 2 + (6 * (↑3! * L.G 4) * 2 + 6 * (↑3! * L.G 4) * 2)) +
      60 * L.G 4 * ↑4! =
    0

Tactic:
ring

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

Goal state before:
pp: case succ.e_a.e_a.e_f
R : Type u_1
a b u₀ : R
inst✝ : CommSemiring R
n : ℕ
hn : arithGeom a b u₀ n = a ^ n * u₀ + b * ∑ k ∈ Finset.range n, a ^ k
k : ℕ
⊢ a * (b * a ^ k) = b * a ^ (k + 1)

Tactic:
ring

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

Goal state before:
pp: z : ℍ
⊢ ↑π * ((cexp (2 * ↑π * I * ↑z) + 1) * I * (1 - cexp (2 * ↑π * I * ↑z))⁻¹) =
    ↑π * I * ((cexp (2 * ↑π * I * ↑z) + 1) * (1 - cexp (2 * ↑π * I * ↑z))⁻¹)

Tactic:
ring

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

Goal state before:
pp: R : Type u_1
a b : R
inst✝ : Field R
ha : a ≠ 1
n : ℕ
⊢ a ^ n * (0 - b / (1 - a)) + b / (1 - a) = b * (1 - a ^ n) / (1 - a)

Tactic:
ring

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

Goal state before:
pp: R : Type u_1
a b : R
inst✝ : Field R
ha : a ≠ 1
n : ℕ
⊢ arithGeom a b 0 n = b * (1 - a ^ n) / (1 - a)

Tactic:
rw [arithGeom_eq ha n]
  ring

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

Goal state before:
pp: z : ℍ
h1 :
  ↑π * ((cexp (2 * ↑π * I * ↑z) + 1) / (I * (1 - cexp (2 * ↑π * I * ↑z)))) =
    -↑π * I * ((cexp (2 * ↑π * I * ↑z) + 1) * (1 / (1 - cexp (2 * ↑π * I * ↑z))))
⊢ -↑π * I * (2 * ∑' (i : ℕ), cexp (2 * ↑π * I * ↑z) ^ i - 1) =
    ↑π * I - 2 * ↑π * I * ∑' (n : ℕ), cexp (2 * ↑π * I * ↑z) ^ n

Tactic:
ring

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

Goal state before:
pp: x : ℂ
h0 : x ≠ 0
⊢ Complex.sin (↑π * x) / (↑π * x) = Complex.sin (↑π * x) * (1 / (↑π * x))

Tactic:
ring

Goal state after:
Module: Mathlib.Data.Int.Fib.Basic

Goal state before:
pp: n✝ : ℤ
n : ℕ
h✝ : n✝ = ↑n ∨ n✝ = -↑n
⊢ fib (-n✝) = if Even n✝ then -fib n✝ else fib n✝

Tactic:
aesop (add safe (by rw [fib_neg_natCast]))

Goal state after: