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

Goal state before:
pp: θ : ℝ
n : ℕ
f : ℝ → ℝ := fun x ↦ 1 - x ^ 2
u₁ : ℝ → ℝ := fun x ↦ f x ^ (n + 1)
u₁' : ℝ → ℝ := fun x ↦ -(2 * (↑n + 1) * x * f x ^ n)
v₁ : ℝ → ℝ := fun x ↦ sin (x * θ)
v₁' : ℝ → ℝ := fun x ↦ cos (x * θ) * θ
u₂ : ℝ → ℝ := fun x ↦ x * f x ^ n
u₂' : ℝ → ℝ := fun x ↦ f x ^ n - 2 * ↑n * x ^ 2 * f x ^ (n - 1)
v₂ : ℝ → ℝ := fun x ↦ cos (x * θ)
v₂' : ℝ → ℝ := fun x ↦ -sin (x * θ) * θ
hfd : Continuous f
hu₁d : Continuous u₁'
hv₁d : Continuous v₁'
hu₂d : Continuous u₂'
hv₂d : Continuous v₂'
hu₁_eval_one : u₁ 1 = 0
hu₁_eval_neg_one : u₁ (-1) = 0
t : u₂ 1 * v₂ 1 - u₂ (-1) * v₂ (-1) = 2 * (0 ^ n * cos θ)
⊢ (∫ (x : ℝ) in -1..1, (1 - x ^ 2) ^ (n + 1) * cos (x * θ)) * θ ^ 2 =
    -(2 * 2 * ((↑n + 1) * (0 ^ n * cos θ))) + 2 * (↑n + 1) * (2 * ↑n + 1) * I n θ - 4 * (↑n + 1) * ↑n * I (n - 1) θ

Tactic:
have hf (x) : HasDerivAt f (- 2 * x) x := by
    convert! (hasDerivAt_pow 2 x).const_sub 1 using 1
    simp

Goal state after:
θ : ℝ
n : ℕ
f : ℝ → ℝ := fun x ↦ 1 - x ^ 2
u₁ : ℝ → ℝ := fun x ↦ f x ^ (n + 1)
u₁' : ℝ → ℝ := fun x ↦ -(2 * (↑n + 1) * x * f x ^ n)
v₁ : ℝ → ℝ := fun x ↦ sin (x * θ)
v₁' : ℝ → ℝ := fun x ↦ cos (x * θ) * θ
u₂ : ℝ → ℝ := fun x ↦ x * f x ^ n
u₂' : ℝ → ℝ := fun x ↦ f x ^ n - 2 * ↑n * x ^ 2 * f x ^ (n - 1)
v₂ : ℝ → ℝ := fun x ↦ cos (x * θ)
v₂' : ℝ → ℝ := fun x ↦ -sin (x * θ) * θ
hfd : Continuous f
hu₁d : Continuous u₁'
hv₁d : Continuous v₁'
hu₂d : Continuous u₂'
hv₂d : Continuous v₂'
hu₁_eval_one : u₁ 1 = 0
hu₁_eval_neg_one : u₁ (-1) = 0
t : u₂ 1 * v₂ 1 - u₂ (-1) * v₂ (-1) = 2 * (0 ^ n * cos θ)
hf : ∀ (x : ℝ), HasDerivAt f (-2 * x) x
⊢ (∫ (x : ℝ) in -1..1, (1 - x ^ 2) ^ (n + 1) * cos (x * θ)) * θ ^ 2 =
    -(2 * 2 * ((↑n + 1) * (0 ^ n * cos θ))) + 2 * (↑n + 1) * (2 * ↑n + 1) * I n θ - 4 * (↑n + 1) * ↑n * I (n - 1) θ
Module: Mathlib.Analysis.SpecialFunctions.Arcosh

Goal state before:
pp: x : ℝ
hx : 1 ≤ x
⊢ arcosh x = 0 ↔ x = 1

Tactic:
rw [← exp_injective.eq_iff, exp_arcosh hx, exp_zero]
  grind

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

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

Tactic:
sub_div' (ne_of_gt (add_pos_of_nonneg_of_pos (mul_nonneg
      (two_pos : 0 < (2 : ℝ)).le (Nat.cast_nonneg _)) two_pos)),

Goal state after:
this : 𝓝 (π / 2) = 𝓝 ((1 - 0) * (π / 2))
n : ℕ
⊢ (2 * ↑n + 1) / (2 * ↑n + 2) = (1 * (2 * ↑n + 2) - 1) / (2 * ↑n + 2)
Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy

Goal state before:
pp: p : ℝ
hp : p < 0
hp' : ¬p < -1
⊢ -p * log p ≤ 0

Tactic:
wlog h : -1 < p

Goal state after:
case inr
p : ℝ
hp : p < 0
hp' : ¬p < -1
this : ∀ {p : ℝ}, p < 0 → ¬p < -1 → -1 < p → -p * log p ≤ 0
h : ¬-1 < p
⊢ -p * log p ≤ 0

p✝ p : ℝ
hp : p < 0
hp' : ¬p < -1
h : -1 < p
⊢ -p * log p ≤ 0
Module: Mathlib.Analysis.SpecialFunctions.CompareExp

Goal state before:
pp: l : Filter ℂ
hl : IsExpCmpFilter l
a z : ℂ
hz : z ≠ 0
⊢ (fun z ↦ ‖z‖ ^ a.re) z = (fun z ↦ Real.exp (a.re * Real.log ‖z‖)) z

Tactic:
by simp
        [Real.rpow_def_of_pos, norm_pos_iff.mpr hz, mul_comm]

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

Goal state before:
pp: q : ℕ
⊢ ¬ContinuousAt (deriv (qaryEntropy q)) 1

Tactic:
have tendstoBot : Tendsto (fun p ↦ log (q - 1) + log (1 - p) - log p) (𝓝[<] 1) atBot := by
    have : (fun p ↦ log (q - 1) + log (1 - p) - log p)
      = (fun p ↦ log (q - 1) + (log (1 - p) - log p)) := by
      ext
      ring
    rw [this]
    apply tendsto_atBot_add_const_left
    exact tendsto_log_one_sub_sub_log_nhdsLT_one_atBot

Goal state after:
q : ℕ
tendstoBot : Tendsto (fun p ↦ log (↑q - 1) + log (1 - p) - log p) (𝓝[<] 1) atBot
⊢ ¬ContinuousAt (deriv (qaryEntropy q)) 1
Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy

Goal state before:
pp: q : ℕ
tendstoTop : Tendsto (fun p ↦ log (↑q - 1) + log (1 - p) - log p) (𝓝[>] 0) atTop
⊢ Disjoint (𝓝 (deriv (qaryEntropy q) 0)) atTop

Tactic:
simp only [disjoint_nhds_atTop_iff, not_isTop, not_false_eq_true]

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

Goal state before:
pp: θ : ℝ
⊢ I 1 θ * θ ^ 3 = 4 * sin θ - 4 * θ * cos θ

Tactic:
rw [_root_.pow_succ, ← mul_assoc, recursion' 0, sub_mul, add_mul, mul_assoc _ (I 0 θ), I_zero]
  ring

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

Goal state before:
pp: n : ℕ
⊢ ↑(harmonic n) - log (↑n + 1) < ↑(harmonic (n + 1)) - log (↑(n + 1) + 1)

Tactic:
← sub_pos,

Goal state after:
n : ℕ
⊢ 0 < ↑(harmonic (n + 1)) - log (↑(n + 1) + 1) - (↑(harmonic n) - log (↑n + 1))
Module: Mathlib.NumberTheory.Harmonic.EulerMascheroni

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

Tactic:
← sub_pos,

Goal state after:
case inr
n : ℕ
hn : n > 0
⊢ 0 < ↑(harmonic n) - log ↑n - (↑(harmonic (n + 1)) - log ↑(n + 1))
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation

Goal state before:
pp: case hg2
p x : ℝ
hp : p ∈ Ioo 0 1
hx✝ : 0 ≤ x
hx : 0 < x
this :
  ∫ (t : ℝ) in Ioi 0, ((fun x_1 ↦ p.rpowIntegrand₀₁ x_1 x) ∘ fun x_1 ↦ x * x_1) t * x =
    x ^ p * ∫ (t : ℝ) in Ioi 0, p.rpowIntegrand₀₁ t 1
⊢ IntegrableOn (fun x_1 ↦ p.rpowIntegrand₀₁ (x * x_1) x * x) (Ici 0) volume

Tactic:
rw [integrableOn_congr_fun (rpowIntegrand₀₁_apply_mul_eqOn_Ici hp hx.le) measurableSet_Ici]

Goal state after:
case hg2
p x : ℝ
hp : p ∈ Ioo 0 1
hx✝ : 0 ≤ x
hx : 0 < x
this :
  ∫ (t : ℝ) in Ioi 0, ((fun x_1 ↦ p.rpowIntegrand₀₁ x_1 x) ∘ fun x_1 ↦ x * x_1) t * x =
    x ^ p * ∫ (t : ℝ) in Ioi 0, p.rpowIntegrand₀₁ t 1
⊢ IntegrableOn (fun t ↦ p.rpowIntegrand₀₁ t 1 * x ^ p) (Ici 0) volume
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation

Goal state before:
pp: A : Type u_1
inst✝⁹ : NonUnitalNormedRing A
inst✝⁸ : StarRing A
inst✝⁷ : NormedSpace ℝ A
inst✝⁶ : SMulCommClass ℝ A A
inst✝⁵ : IsScalarTower ℝ A A
inst✝⁴ : PartialOrder A
inst✝³ : StarOrderedRing A
inst✝² : NonnegSpectrumClass ℝ A
inst✝¹ : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝ : CompleteSpace A
p : ℝ≥0
hp : p ∈ Ioo 0 1
μ : Measure ℝ
hμ :
  ∀ x ∈ Ici 0,
    IntegrableOn (fun t ↦ (↑p).rpowIntegrand₀₁ t x) (Ioi 0) μ ∧ x ^ ↑p = ∫ (t : ℝ) in Ioi 0, (↑p).rpowIntegrand₀₁ t x ∂μ
a : A
ha : 0 ≤ a
a✝ : Nontrivial A
p_pos : 0 < ↑p
f : ℝ → ℝ → ℝ := fun t ↦ (↑p).rpowIntegrand₀₁ t
maxr : ℝ := sSup (quasispectrum ℝ a)
maxr_nonneg : 0 ≤ maxr
bound : ℝ → ℝ := fun t ↦ ‖f t maxr‖
hf : ContinuousOn (Function.uncurry f) (Ioi 0 ×ˢ quasispectrum ℝ a)
t : ℝ
ht : t ∈ Ioi 0
z : ℝ
hz : z ∈ quasispectrum ℝ a
hz' : 0 ≤ z
⊢ ‖(↑p).rpowIntegrand₀₁ t z‖ ≤ ‖(↑p).rpowIntegrand₀₁ t maxr‖

Tactic:
rw [Real.norm_of_nonneg (rpowIntegrand₀₁_nonneg p_pos (le_of_lt ht) hz'),
        Real.norm_of_nonneg (rpowIntegrand₀₁_nonneg p_pos (le_of_lt ht) maxr_nonneg)]

Goal state after:
A : Type u_1
inst✝⁹ : NonUnitalNormedRing A
inst✝⁸ : StarRing A
inst✝⁷ : NormedSpace ℝ A
inst✝⁶ : SMulCommClass ℝ A A
inst✝⁵ : IsScalarTower ℝ A A
inst✝⁴ : PartialOrder A
inst✝³ : StarOrderedRing A
inst✝² : NonnegSpectrumClass ℝ A
inst✝¹ : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝ : CompleteSpace A
p : ℝ≥0
hp : p ∈ Ioo 0 1
μ : Measure ℝ
hμ :
  ∀ x ∈ Ici 0,
    IntegrableOn (fun t ↦ (↑p).rpowIntegrand₀₁ t x) (Ioi 0) μ ∧ x ^ ↑p = ∫ (t : ℝ) in Ioi 0, (↑p).rpowIntegrand₀₁ t x ∂μ
a : A
ha : 0 ≤ a
a✝ : Nontrivial A
p_pos : 0 < ↑p
f : ℝ → ℝ → ℝ := fun t ↦ (↑p).rpowIntegrand₀₁ t
maxr : ℝ := sSup (quasispectrum ℝ a)
maxr_nonneg : 0 ≤ maxr
bound : ℝ → ℝ := fun t ↦ ‖f t maxr‖
hf : ContinuousOn (Function.uncurry f) (Ioi 0 ×ˢ quasispectrum ℝ a)
t : ℝ
ht : t ∈ Ioi 0
z : ℝ
hz : z ∈ quasispectrum ℝ a
hz' : 0 ≤ z
⊢ (↑p).rpowIntegrand₀₁ t z ≤ (↑p).rpowIntegrand₀₁ t maxr
Module: Mathlib.NumberTheory.Harmonic.GammaDeriv

Goal state before:
pp: ⊢ HasDerivAt Gamma (-√π * (γ + 2 * log 2)) (1 / 2)

Tactic:
have h_diff {s : ℝ} (hs : 0 < s) : DifferentiableAt ℝ Gamma s :=
    differentiableAt_Gamma fun m ↦ ((neg_nonpos.mpr m.cast_nonneg).trans_lt hs).ne'

Goal state after:
h_diff : ∀ {s : ℝ}, 0 < s → DifferentiableAt ℝ Gamma s
⊢ HasDerivAt Gamma (-√π * (γ + 2 * log 2)) (1 / 2)
Module: Mathlib.NumberTheory.Harmonic.GammaDeriv

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

Tactic:
exact .comp (g := Gamma) _ (by apply h_diff; simp) -- s = 1
        (differentiableAt_id.const_mul _)

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

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

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

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

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

Tactic:
exact logb_mul h₁ h₂

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 : ℕ
hb : 1 < b
r : R
hr : r ≤ 0
⊢ r ≤ 1

Tactic:
exact hr.trans zero_le_one

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

Goal state before:
pp: 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
⊢ 0 < ↑b ^ (log b r⁻¹ + 1)

Tactic:
· exact zpow_pos (Nat.cast_pos.mpr <| zero_le_one.trans_lt hb) _

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

Goal state before:
pp: b x : ℝ
hb : 1 < b
hx : 0 ≤ x
⊢ logb b x ≤ 0 ↔ x ≤ 1

Tactic:
rcases hx.eq_or_lt with (rfl | hx)
  · simp [zero_le_one]
  exact logb_nonpos_iff hb hx

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

Goal state before:
pp: case succ
n : ℕ
ih : MonotoneOn (deriv fun x ↦ Polynomial.eval x (descPochhammer ℝ n)) (Set.Ioi (↑n - 1))
a : ℝ
ha : ↑n < a
b : ℝ
hb : ↑n < b
hab : a ≤ b
⊢ deriv (fun x ↦ Polynomial.eval x (descPochhammer ℝ (n + 1))) a ≤
    deriv (fun x ↦ Polynomial.eval x (descPochhammer ℝ (n + 1))) b

Tactic:
simp_rw [deriv_descPochhammer_eval_eq_sum_prod_range_erase]

Goal state after:
case succ
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 ∈ Finset.range (n + 1), ∏ j ∈ (Finset.range (n + 1)).erase i, (a - ↑j) ≤
    ∑ i ∈ Finset.range (n + 1), ∏ j ∈ (Finset.range (n + 1)).erase i, (b - ↑j)
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
x : ℂ
r : ℝ
hr : 0 < r
hr' : 𝓝 x ≤ 𝓟 (Metric.ball 0 r)
R : ℝ
hR : ∀ (b : ℝ), R ≤ b → ∀ (x : ℂ), ‖x‖ < r → ∀ (l : ↥L.lattice), ‖↑l‖ = b → ‖f l x‖ ≤ u r l
l : ↥L.lattice
hl : l ∈ {x | (fun n ↦ ∀ x ∈ Metric.ball 0 r, ‖f n x‖ ≤ u r n) x}ᶜ
⊢ ∃ x, ‖x‖ < r ∧ u r l < ‖f l x‖

Tactic:
simpa using hl

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

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

pp: case hg
L : PeriodPair
l₀ : ↥L.lattice
z : ℂ
⊢ Summable fun i ↦ if ↑i = ↑l₀ then 1 / (z - ↑l₀) ^ 2 - 1 / ↑l₀ ^ 2 else 0

Tactic:
· exact ⟨_, L.hasSum_weierstrassPExcept _ _⟩

Goal state after:
case hg
L : PeriodPair
l₀ : ↥L.lattice
z : ℂ
⊢ Summable fun i ↦ if ↑i = ↑l₀ then 1 / (z - ↑l₀) ^ 2 - 1 / ↑l₀ ^ 2 else 0
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: L : PeriodPair
l₀ : ℂ
s : Finset ↥L.lattice
x : ↥L.lattice
hl₁ : ¬↑x = l₀
hl : ↑x ∈ (↑L.lattice \ {l₀})ᶜ
e : ↑x - ↑x = 0
⊢ ↑x = l₀

Tactic:
simpa using hl

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

Goal state before:
pp: L : PeriodPair
l₀ : ℂ
s : Finset ↥L.lattice
x : ↥L.lattice
hxs : x ∈ s
hl₁ : ¬↑x = l₀
hl : ↑x ∈ (↑L.lattice \ {l₀})ᶜ
e : ↑x - ↑x = 0
⊢ ↑x = l₀

Tactic:
simpa using hl

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

Goal state before:
pp: case refine_2
L : PeriodPair
l₀ : ℂ
⊢ TendstoLocallyUniformlyOn
    (deriv ∘ fun x1 x2 ↦ ∑ i ∈ x1, (fun l z ↦ if ↑l = l₀ then 0 else 1 / (z - ↑l) ^ 2 - 1 / ↑l ^ 2) i x2) ℘'[L - l₀]
    atTop (↑L.lattice \ {l₀})ᶜ

Tactic:
refine (L.hasSumLocallyUniformly_derivWeierstrassPExcept l₀).tendstoLocallyUniformlyOn.congr ?_
    intro s l hl
    simp only [Function.comp_apply]
    rw [deriv_fun_sum]
    · congr with x
      split_ifs with hl₁
      · simp
      have hl₁ : l - x ≠ 0 := fun e ↦ hl₁ (by
        obtain rfl := sub_eq_zero.mp e
        simpa using hl)
      rw [deriv_fun_sub (.fun_div (by fun_prop) (by fun_prop) (by simpa)) (by fun_prop),
        deriv_const]
      simp_rw [← zpow_natCast, one_div, ← zpow_neg, Nat.cast_ofNat]
      rw [deriv_comp_sub_const (f := (· ^ (-2 : ℤ))), deriv_zpow]
      simp
      field_simp
    · intros x hxs
      split_ifs with hl₁
      · simp
      have hl₁ : l - x ≠ 0 := fun e ↦ hl₁ (by
        obtain rfl := sub_eq_zero.mp e
        simpa using hl)
      exact .sub (.div (by fun_prop) (by fun_prop) (by simpa)) (by fun_prop)

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

Goal state before:
pp: L : PeriodPair
l₀ : ℂ
hl₀ : l₀ ∈ L.lattice
l : ↥L.lattice
hl : ↑l / 2 ∉ L.lattice
⊢ DifferentiableOn ℂ (fun x ↦ ℘[L - l₀] (x + ↑l)) (↑L.lattice \ {l₀ - ↑l})ᶜ

pp: L : PeriodPair
l₀ : ℂ
hl₀ : l₀ ∈ L.lattice
l : ↥L.lattice
hl : ↑l / 2 ∉ L.lattice
⊢ DifferentiableOn ℂ (fun x ↦ ℘[L - l₀ - ↑l] x + (1 / l₀ ^ 2 - 1 / (l₀ - ↑l) ^ 2)) (↑L.lattice \ {l₀ - ↑l})ᶜ

pp: L : PeriodPair
l₀ : ℂ
hl₀ : l₀ ∈ L.lattice
l : ↥L.lattice
hl : ↑l / 2 ∉ L.lattice
⊢ Set.EqOn (deriv fun x ↦ ℘[L - l₀] (x + ↑l)) (deriv fun x ↦ ℘[L - l₀ - ↑l] x + (1 / l₀ ^ 2 - 1 / (l₀ - ↑l) ^ 2))
    (↑L.lattice \ {l₀ - ↑l})ᶜ

pp: L : PeriodPair
l₀ : ℂ
hl₀ : l₀ ∈ L.lattice
l : ↥L.lattice
hl : ↑l / 2 ∉ L.lattice
⊢ -(↑l / 2) ∈ (↑L.lattice \ {l₀ - ↑l})ᶜ

pp: L : PeriodPair
l₀ : ℂ
hl₀ : l₀ ∈ L.lattice
l : ↥L.lattice
hl : ↑l / 2 ∉ L.lattice
⊢ ℘[L - l₀] (-(↑l / 2) + ↑l) = ℘[L - l₀ - ↑l] (-(↑l / 2)) + (1 / l₀ ^ 2 - 1 / (l₀ - ↑l) ^ 2)

Tactic:
· refine (L.differentiableOn_weierstrassPExcept l₀).comp (f := (· + l.1)) (by fun_prop) ?_
    rintro x h₁ ⟨h₂ : x + l ∈ _, h₃ : x + l ≠ l₀⟩
    exact h₁ ⟨by simpa using sub_mem h₂ l.2, by rintro rfl; simp at h₃⟩

Goal state after:
L : PeriodPair
l₀ : ℂ
hl₀ : l₀ ∈ L.lattice
l : ↥L.lattice
hl : ↑l / 2 ∉ L.lattice
⊢ DifferentiableOn ℂ (fun x ↦ ℘[L - l₀ - ↑l] x + (1 / l₀ ^ 2 - 1 / (l₀ - ↑l) ^ 2)) (↑L.lattice \ {l₀ - ↑l})ᶜ

L : PeriodPair
l₀ : ℂ
hl₀ : l₀ ∈ L.lattice
l : ↥L.lattice
hl : ↑l / 2 ∉ L.lattice
⊢ Set.EqOn (deriv fun x ↦ ℘[L - l₀] (x + ↑l)) (deriv fun x ↦ ℘[L - l₀ - ↑l] x + (1 / l₀ ^ 2 - 1 / (l₀ - ↑l) ^ 2))
    (↑L.lattice \ {l₀ - ↑l})ᶜ

L : PeriodPair
l₀ : ℂ
hl₀ : l₀ ∈ L.lattice
l : ↥L.lattice
hl : ↑l / 2 ∉ L.lattice
⊢ -(↑l / 2) ∈ (↑L.lattice \ {l₀ - ↑l})ᶜ

L : PeriodPair
l₀ : ℂ
hl₀ : l₀ ∈ L.lattice
l : ↥L.lattice
hl : ↑l / 2 ∉ L.lattice
⊢ ℘[L - l₀] (-(↑l / 2) + ↑l) = ℘[L - l₀ - ↑l] (-(↑l / 2)) + (1 / l₀ ^ 2 - 1 / (l₀ - ↑l) ^ 2)
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: L : PeriodPair
l₀ : ℂ
hl₀ : l₀ ∈ L.lattice
l : ↥L.lattice
hl : ↑l / 2 ∉ L.lattice
⊢ Set.EqOn (fun x ↦ ℘[L - l₀] (x + ↑l)) (fun x ↦ ℘[L - l₀ - ↑l] x + (1 / l₀ ^ 2 - 1 / (l₀ - ↑l) ^ 2))
    (↑L.lattice \ {l₀ - ↑l})ᶜ

Tactic:
by
  apply IsOpen.eqOn_of_deriv_eq (𝕜 := ℂ) L.isOpen_compl_lattice_sdiff
    ?_ ?_ ?_ ?_ (x := -(l / 2)) ?_ ?_
  · refine (Set.Countable.isConnected_compl_of_one_lt_rank (by simp) ?_).2
    exact .mono sdiff_le (countable_of_Lindelof_of_discrete (X := L.lattice))
  · refine (L.differentiableOn_weierstrassPExcept l₀).comp (f := (· + l.1)) (by fun_prop) ?_
    rintro x h₁ ⟨h₂ : x + l ∈ _, h₃ : x + l ≠ l₀⟩
    exact h₁ ⟨by simpa using sub_mem h₂ l.2, by rintro rfl; simp at h₃⟩
  · refine .add (L.differentiableOn_weierstrassPExcept _) (by simp)
  · intro x hx
    simp only [deriv_add_const', deriv_comp_add_const]
    rw [L.eqOn_deriv_weierstrassPExcept_derivWeierstrassPExcept,
      L.eqOn_deriv_weierstrassPExcept_derivWeierstrassPExcept, L.derivWeierstrassPExcept_add_coe]
    · simpa using hx
    · simp only [Set.mem_compl_iff, Set.mem_sdiff, SetLike.mem_coe, Set.mem_singleton_iff, not_and,
        Decidable.not_not, eq_sub_iff_add_eq] at hx ⊢
      exact fun H ↦ hx (by simpa using sub_mem H l.2)
  · simp [hl]
  · rw [L.weierstrassPExcept_neg, L.weierstrassPExcept_def ⟨l₀, hl₀⟩,
      L.weierstrassPExcept_def ⟨_, neg_mem (sub_mem hl₀ l.2)⟩, add_assoc]
    congr 2 <;> ring

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

Goal state before:
pp: L : PeriodPair
l₀ : ↥L.lattice
z : ℂ
⊢ ℘'[L - ↑l₀] z = ℘'[L] z + 2 / (z - ↑l₀) ^ 3

Tactic:
← L.derivWeierstrassPExcept_sub l₀,

Goal state after:
L : PeriodPair
l₀ : ↥L.lattice
z : ℂ
⊢ ℘'[L - ↑l₀] z = ℘'[L - ↑l₀] z - 2 / (z - ↑l₀) ^ 3 + 2 / (z - ↑l₀) ^ 3
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

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

Tactic:
Subtype.ext_iff,

Goal state after:
L : PeriodPair
l₀ x : ℂ
i : ℕ
hl₀ : l₀ ∈ L.lattice
⊢ ∑' (x_1 : ↥L.lattice), (↑i + 2) * (((↑x_1 - x) ^ (i + 3))⁻¹ - if ↑x_1 = l₀ then (l₀ - x) ^ (-↑(i + 3)) else 0) =
    ∑' (l : ↥L.lattice), if ↑l = l₀ then 0 else (↑(i + 1) + 1) * (↑l - x) ^ (-↑(i + 1 + 2)) - 0 i
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Orthogonality

Goal state before:
pp: f : ℝ → ℝ
⊢ ∫ (x : ℝ), f x ∂measureT = ∫ (x : ℝ) in -1..1, f x * √(1 - x ^ 2)⁻¹

Tactic:
by
  rw [integral_of_le (by norm_num), measureT,
    restrict_withDensity (by measurability),
    integral_withDensity_eq_integral_smul (by fun_prop)]
  congr! 2 with x hx
  simp [NNReal.smul_def, mul_comm]

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

Goal state before:
pp: n : ℤ
hn : n ≠ 0
hn' : ↑n ≠ 0
this : ∫ (θ : ℝ) in 0..↑n * π, cos θ = 0
⊢ ∫ (x : ℝ) in ↑n * 0..↑n * π, cos x = 0

Tactic:
mul_zero

Goal state after:
n : ℤ
hn : n ≠ 0
hn' : ↑n ≠ 0
this : ∫ (θ : ℝ) in 0..↑n * π, cos θ = 0
⊢ ∫ (x : ℝ) in 0..↑n * π, cos x = 0
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Orthogonality

Goal state before:
pp: case pos
n : ℤ
hn : n ≠ 0
hn' : ↑n ≠ 0
h✝ : 0 ≤ n
⊢ ∫ (θ : ℝ) in 0..↑n * π, deriv sin θ = 0

pp: case neg
n : ℤ
hn : n ≠ 0
hn' : ↑n ≠ 0
h✝ : n < 0
⊢ ∫ (θ : ℝ) in 0..↑n * π, deriv sin θ = 0

Tactic:
case pos => rw [integral_deriv_of_contDiffOn_Icc contDiff_sin.contDiffOn (by positivity)]; simp

Goal state after:
case neg
n : ℤ
hn : n ≠ 0
hn' : ↑n ≠ 0
h✝ : n < 0
⊢ ∫ (θ : ℝ) in 0..↑n * π, deriv sin θ = 0
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal

Goal state before:
pp: case inr
n i : ℕ
hi : i ≤ n
hn : n ≠ 0
h₁ : 0 < (-1) ^ i * ∏ x ∈ Finset.range i, (node n i - node n x)
h₂ : 0 < ∏ j ∈ Finset.Ioc i n, (node n i - node n j)
union : (Finset.range (n + 1)).erase i = Finset.range i ∪ Finset.Ioc i n
⊢ 0 < (-1) ^ i * ∏ j ∈ (Finset.range (n + 1)).erase i, (node n i - node n j)

Tactic:
have disjoint : Disjoint (Finset.range i) (Finset.Ioc i n) := by grind [Finset.disjoint_iff_ne]

Goal state after:
case inr
n i : ℕ
hi : i ≤ n
hn : n ≠ 0
h₁ : 0 < (-1) ^ i * ∏ x ∈ Finset.range i, (node n i - node n x)
h₂ : 0 < ∏ j ∈ Finset.Ioc i n, (node n i - node n j)
union : (Finset.range (n + 1)).erase i = Finset.range i ∪ Finset.Ioc i n
disjoint : Disjoint (Finset.range i) (Finset.Ioc i n)
⊢ 0 < (-1) ^ i * ∏ j ∈ (Finset.range (n + 1)).erase i, (node n i - node n j)
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: L : PeriodPair
l₀ x : ℂ
r : NNReal
hr0 : 0 < r
hr : Metric.closedBall x ↑r ⊆ (↑L.lattice \ {l₀})ᶜ
⊢ HasFPowerSeriesOnBall ℘'[L - l₀] (L.derivWeierstrassPExceptSeries l₀ x) x ↑r

Tactic:
refine .congr ?_
    ((L.eqOn_deriv_weierstrassPExcept_derivWeierstrassPExcept l₀).mono (.trans ?_ hr))

Goal state after:
case refine_1
L : PeriodPair
l₀ x : ℂ
r : NNReal
hr0 : 0 < r
hr : Metric.closedBall x ↑r ⊆ (↑L.lattice \ {l₀})ᶜ
⊢ HasFPowerSeriesOnBall (deriv ℘[L - l₀]) (L.derivWeierstrassPExceptSeries l₀ x) x ↑r

case refine_2
L : PeriodPair
l₀ x : ℂ
r : NNReal
hr0 : 0 < r
hr : Metric.closedBall x ↑r ⊆ (↑L.lattice \ {l₀})ᶜ
⊢ Metric.eball x ↑r ⊆ Metric.closedBall x ↑r
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable

Goal state before:
pp: case neg
z : ℍ
k : ℝ
hk : 0 ≤ k
x : Fin 2 → ℤ
hx : x = 0
h : ¬-k = 0
⊢ 0 ≤ r z ^ (-k) * 0

Tactic:
mul_zero

Goal state after:
case neg
z : ℍ
k : ℝ
hk : 0 ≤ k
x : Fin 2 → ℤ
hx : x = 0
h : ¬-k = 0
⊢ 0 ≤ 0
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: L : PeriodPair
l₀ : ℂ
h : l₀ ∈ L.lattice
⊢ ∃ g, AnalyticAt ℂ g l₀ ∧ g l₀ ≠ 0 ∧ ∀ᶠ (z : ℂ) in 𝓝[≠] l₀, ℘[L] z = (z - l₀) ^ (-2) • g z

Tactic:
refine ⟨fun z ↦ (z - l₀) ^ 2 * ℘[L - l₀] z + 1 - (z - l₀) ^ 2 / l₀ ^ 2, ?_, ?_, ?_⟩

Goal state after:
case refine_1
L : PeriodPair
l₀ : ℂ
h : l₀ ∈ L.lattice
⊢ AnalyticAt ℂ (fun z ↦ (z - l₀) ^ 2 * ℘[L - l₀] z + 1 - (z - l₀) ^ 2 / l₀ ^ 2) l₀

case refine_2
L : PeriodPair
l₀ : ℂ
h : l₀ ∈ L.lattice
⊢ (fun z ↦ (z - l₀) ^ 2 * ℘[L - l₀] z + 1 - (z - l₀) ^ 2 / l₀ ^ 2) l₀ ≠ 0

case refine_3
L : PeriodPair
l₀ : ℂ
h : l₀ ∈ L.lattice
⊢ ∀ᶠ (z : ℂ) in 𝓝[≠] l₀, ℘[L] z = (z - l₀) ^ (-2) • (fun z ↦ (z - l₀) ^ 2 * ℘[L - l₀] z + 1 - (z - l₀) ^ 2 / l₀ ^ 2) z
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: L : PeriodPair
⊢ L.relation = 0

Tactic:
by
  ext x
  have : Differentiable ℂ L.relation := fun x ↦ (L.analyticAt_relation x).differentiableAt
  exact (this.apply_eq_apply_of_bounded (IsZLattice.isCompact_range_of_periodic L.lattice _
    this.continuous fun z w hw ↦ by lift w to L.lattice using hw; simp).isBounded x 0).trans
    (if_pos (by simp))

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

Goal state before:
pp: n : ℕ
x : ℝ
hroot : x ∈ Finset.image (fun k ↦ cos ((2 * ↑k + 1) * π / (2 * ↑n))) (Finset.range n)
k : ℕ
hk₁ : k ∈ Finset.range n
hk₂ : cos ((2 * ↑k + 1) * π / (2 * ↑n)) = x
hn✝ : n ≠ 0
hnz : (Rat.divInt (2 * ↑k + 1) (2 * ↑n)).den ≤ 3
this : (Rat.divInt (2 * ↑k + 1) (2 * ↑n)).den = 2 * (n / n.gcd (2 * k + 1))
hn : 2 * k + 1 = n
⊢ x = 0

Tactic:
rw_mod_cast [← hk₂, hn]

Goal state after:
n : ℕ
x : ℝ
k : ℕ
hk₁ : k ∈ Finset.range n
hn✝ : ¬n = 0
hn : 2 * k + 1 = n
hroot : x ∈ Finset.image (fun k ↦ cos (↑(2 * k + 1) * π / ↑(2 * n))) (Finset.range n)
hk₂ : cos (↑(2 * k + 1) * π / ↑(2 * n)) = x
hnz : (NNRat.divNat (2 * k + 1) (2 * n)).den ≤ 3
this : (NNRat.divNat (2 * k + 1) (2 * n)).den = 2 * (n / n.gcd (2 * k + 1))
⊢ cos (↑n * π / ↑(2 * n)) = 0