mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.RingInverseOrder

Goal state before:
pp: A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
t : ℝ
ht : 0 < t
this : ∀ x ∈ Ici 0, IsStrictlyPositive ((algebraMap ℝ A) t + x)
addl : A →ᵃ[ℝ] A := (AffineMap.toConstProdLinearMap ℝ).symm ((algebraMap ℝ A) t, LinearMap.id)
haddl : Function.Injective ⇑addl
hici : Ici 0 = ⇑addl ⁻¹' ⇑addl '' Ici 0
⊢ ConvexOn ℝ (Ici 0) fun x ↦ Ring.inverse ((algebraMap ℝ A) t + x)

Tactic:
add_comm

Goal state after:
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
t : ℝ
ht : 0 < t
this : ∀ x ∈ Ici 0, IsStrictlyPositive ((algebraMap ℝ A) t + x)
addl : A →ᵃ[ℝ] A := (AffineMap.toConstProdLinearMap ℝ).symm ((algebraMap ℝ A) t, LinearMap.id)
haddl : Function.Injective ⇑addl
hici : Ici 0 = ⇑addl ⁻¹' ⇑addl '' Ici 0
⊢ ConvexOn ℝ (Ici 0) fun x ↦ Ring.inverse (x + (algebraMap ℝ A) t)
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Deligne

Goal state before:
pp: case neg
s : ℂ
hs : ∀ (n : ℕ), s ≠ -↑n
h : ¬s = 1
⊢ (2 - s).Gammaℝ⁻¹ = s.Gammaℂ * sin (↑π * s / 2) * (s + 1).Gammaℝ⁻¹

Tactic:
← Ne,

Goal state after:
case neg
s : ℂ
hs : ∀ (n : ℕ), s ≠ -↑n
h : s ≠ 1
⊢ (2 - s).Gammaℝ⁻¹ = s.Gammaℂ * sin (↑π * s / 2) * (s + 1).Gammaℝ⁻¹
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation

Goal state before:
pp: p x : ℝ
hp : p ∈ Ioo 1 2
hx : 0 ≤ x
a : ℝ
ha : a ∈ Ioi 0
⊢ p.rpowIntegrand₁₂ a x = x * (p - 1).rpowIntegrand₀₁ a x

Tactic:
rpowIntegrand₁₂_eq_mul_rpowIntegrand₀₁ hx ha

Goal state after:
p x : ℝ
hp : p ∈ Ioo 1 2
hx : 0 ≤ x
a : ℝ
ha : a ∈ Ioi 0
⊢ x * (p - 1).rpowIntegrand₀₁ a x = x * (p - 1).rpowIntegrand₀₁ a x
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Digamma

Goal state before:
pp: s : ℂ
hs : ∀ (m : ℕ), s ≠ -↑m
hs0 : s ≠ 0
⊢ s⁻¹ + deriv Gamma s / Gamma s = deriv Gamma s / Gamma s + s⁻¹

Tactic:
add_comm

Goal state after:
s : ℂ
hs : ∀ (m : ℕ), s ≠ -↑m
hs0 : s ≠ 0
⊢ deriv Gamma s / Gamma s + s⁻¹ = deriv Gamma s / Gamma s + s⁻¹
Module: Mathlib.NumberTheory.Harmonic.GammaDeriv

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

Tactic:
simpa

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

Goal state before:
pp: f : ℂ → ℂ := fun s ↦ 2 * (2 * ↑π) ^ (-s)
this✝ : HasDerivAt (fun s ↦ 2 * (2 * ↑π) ^ (-s)) (-log (2 * ↑π) / ↑π) 1
this : HasDerivAt ((fun s ↦ 2 * (2 * ↑π) ^ (-s)) * Gamma) (-(log (2 * ↑π) + ↑γ) / ↑π) 1
⊢ HasDerivAt Gammaℂ (-(↑γ + log (2 * ↑π)) / ↑π) 1

Tactic:
add_comm

Goal state after:
f : ℂ → ℂ := fun s ↦ 2 * (2 * ↑π) ^ (-s)
this✝ : HasDerivAt (fun s ↦ 2 * (2 * ↑π) ^ (-s)) (-log (2 * ↑π) / ↑π) 1
this : HasDerivAt ((fun s ↦ 2 * (2 * ↑π) ^ (-s)) * Gamma) (-(↑γ + log (2 * ↑π)) / ↑π) 1
⊢ HasDerivAt Gammaℂ (-(↑γ + log (2 * ↑π)) / ↑π) 1
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 : ℕ
hb : b ≤ 1
r : R
h : r ≤ 1
⊢ log b r = 0

Tactic:
log_of_right_le_one _ h,

Goal state after:
case inr
R : Type u_1
inst✝³ : Semifield R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorSemiring R
b : ℕ
hb : b ≤ 1
r : R
h : r ≤ 1
⊢ -↑(Nat.clog b ⌈r⁻¹⌉₊) = 0
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 : ℕ
⊢ log b 1 = 0

Tactic:
rw [log_of_one_le_right _ le_rfl, Nat.floor_one, Nat.log_one_right, Int.ofNat_zero]

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
⊢ 0 < b⁻¹

Tactic:
simpa

Goal state after:
Module: Mathlib.MeasureTheory.Measure.RegularityCompacts

Goal state before:
pp: α : Type u_1
inst✝⁵ : MeasurableSpace α
inst✝⁴ : TopologicalSpace α
inst✝³ : SecondCountableTopology α
inst✝² : IsCompletelyPseudoMetrizableSpace α
inst✝¹ : OpensMeasurableSpace α
P : Measure α
inst✝ : IsFiniteMeasure P
ε : ℝ≥0∞
hε : 0 < ε
this : UpgradedIsCompletelyPseudoMetrizableSpace α := upgradeIsCompletelyPseudoMetrizable α
h✝ : Nonempty α
⊢ ∃ K, IsCompact (closure K) ∧ P Kᶜ < ε

Tactic:
let seq := TopologicalSpace.denseSeq α
    have hseq_dense : DenseRange seq := TopologicalSpace.denseRange_denseSeq α
    obtain ⟨t : ℕ → SetRel α α,
        ht : ∀ i, t i ∈ 𝓤 α ∧ IsOpen (t i) ∧ (t i).IsSymm,
        h_basis : (uniformity α).HasAntitoneBasis t⟩ :=
      (@uniformity_hasBasis_open_symmetric α _).exists_antitone_subbasis
    choose htu hto _ using ht
    let f : ℕ → ℕ → Set α := fun n m ↦ UniformSpace.ball (seq m) (t n)
    have h_univ n : (⋃ m, f n m) = univ := hseq_dense.iUnion_uniformity_ball (htu n)
    have h3 n (ε : ℝ≥0∞) (hε : 0 < ε) : ∃ m, P (⋂ m' ≤ m, (f n m')ᶜ) < ε := by
      refine exists_measure_iInter_lt (fun m ↦ ?_) hε ⟨0, measure_ne_top P _⟩ ?_
      · exact (measurable_prodMk_left (hto n).measurableSet).compl.nullMeasurableSet
      · rw [← compl_iUnion, h_univ, compl_univ]
    choose! s' s'bound using h3
    rcases ENNReal.exists_pos_sum_of_countable' (ne_of_gt hε) ℕ with ⟨δ, hδ1, hδ2⟩
    let u : ℕ → ℕ := fun n ↦ s' n (δ n)
    refine ⟨interUnionBalls seq u t, isCompact_closure_interUnionBalls h_basis.toHasBasis seq u, ?_⟩
    rw [interUnionBalls, Set.compl_iInter]
    refine ((measure_iUnion_le _).trans ?_).trans_lt hδ2
    refine ENNReal.tsum_le_tsum (fun n ↦ ?_)
    have h'' n : Prod.swap ⁻¹' t n = t n := by ext; exact (t n).comm
    simp only [h'', compl_iUnion, ge_iff_le]
    exact (s'bound n (δ n) (hδ1 n)).le

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

Goal state before:
pp: case inr.hinf
X : Type u_1
inst✝⁴ : TopologicalSpace X
inst✝³ : MeasurableSpace X
inst✝² : OpensMeasurableSpace X
ι : Type u_2
L : Filter ι
μ : Measure X
inst✝¹ : IsProbabilityMeasure μ
μs : ι → Measure X
inst✝ : ∀ (i : ι), IsProbabilityMeasure (μs i)
h : ∀ (f : X →ᵇ ℝ), 0 ≤ f → ∫ (x : X), f x ∂μ ≤ liminf (fun i ↦ ∫ (x : X), f x ∂μs i) L
f : X →ᵇ ℝ
hL : L.NeBot
obs : Bornology.IsBounded (Set.range fun i ↦ ∫ (x : X), f x ∂μs i)
bdd_above : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) L fun i ↦ ∫ (x : X), f x ∂μs i
bdd_below : IsBoundedUnder (fun x1 x2 ↦ x2 ≤ x1) L fun i ↦ ∫ (x : X), f x ∂μs i
⊢ ∫ (x : X), f x ∂μ ≤ liminf (fun i ↦ ∫ (x : X), f x ∂μs i) L

Tactic:
have key := h _ (f.add_norm_nonneg)
    simp_rw [f.integral_add_const ‖f‖] at key
    simp only [probReal_univ, smul_eq_mul, one_mul] at key
    have := liminf_add_const L (fun i ↦ ∫ x, f x ∂(μs i)) ‖f‖ bdd_above.isCobounded_ge bdd_below
    rwa [this, add_le_add_iff_right] at key

Goal state after:
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✝ : μ.IsOpenPosMeasure
a✝ : Nontrivial E
U : Set ↑(sphere 0 1)
hUo : IsOpen U
hU : U.Nonempty
⊢ (Ioo 0 1 • Subtype.val '' U).Nonempty

Tactic:
simpa

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

Goal state before:
pp: case e'_2
L : PeriodPair
s : Set ℂ
hs : s ⊆ ↑L.lattice
⊢ s = s ∩ Set.range Subtype.val

Tactic:
simpa

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
⊢ 0 < ‖y‖

Tactic:
simpa

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
⊢ u ∈ sphere 0 1

Tactic:
simpa

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 + dist ((1 - ε / 4) • x) x = ε / 4 + ε / 4

Tactic:
by simp [sub_smul, norm_smul, hx, abs_of_pos hε]

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

Goal state before:
pp: case hd
r : ℝ
hr : 0 < r
s : ℂ
hs : ‖s‖ < r
l : ℂ
h : 2 * r ≤ ‖l‖
this✝ : s ≠ l
this : 0 < ‖l‖
⊢ l ^ 2 ≠ 0

Tactic:
simpa

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

Goal state before:
pp: case succ
n a : ℕ
H : ∃ c, a < (c + 1) ^ (n + 1)
k : ℕ
hc : k + 1 = Nat.find H
⊢ (k + 1) ^ (n + 1) ≤ a

Tactic:
| succ k =>

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

Goal state before:
pp: L : PeriodPair
l₀ : ℂ
hl : l₀ ∉ L.lattice
⊢ ℘[L - l₀] = ℘[L]

Tactic:
delta weierstrassPExcept weierstrassP

Goal state after:
L : PeriodPair
l₀ : ℂ
hl : l₀ ∉ L.lattice
⊢ (fun z ↦ ∑' (l : ↥L.lattice), if ↑l = l₀ then 0 else 1 / (z - ↑l) ^ 2 - 1 / ↑l ^ 2) = fun z ↦
    ∑' (l : ↥L.lattice), (1 / (z - ↑l) ^ 2 - 1 / ↑l ^ 2)
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
hdim : dim E ≠ 0
⊢ min (ENNReal.ofReal ε) 2 = ENNReal.ofReal ε

Tactic:
simpa

Goal state after:
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
ε : ℝ
hε : 0 < ε
x : ↑(sphere 0 1)
⊢ ↑(toSphereBallBound (dim E) ε) * (μ (ball 0 1)).toReal ≤ (↑(toSphereBallBound (dim E) ε) * μ (ball 0 1)).toReal

pp: case hb
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
μ : Measure E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
inst✝ : μ.IsAddHaarMeasure
ε : ℝ
hε : 0 < ε
x : ↑(sphere 0 1)
⊢ μ.toSphere (ball x ε) ≠ ∞

Tactic:
ENNReal.toReal_mul,

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
ε : ℝ
hε : 0 < ε
x : ↑(sphere 0 1)
⊢ ↑(toSphereBallBound (dim E) ε) * (μ (ball 0 1)).toReal ≤
    (↑(toSphereBallBound (dim E) ε)).toReal * (μ (ball 0 1)).toReal

case hb
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
μ : Measure E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
inst✝ : μ.IsAddHaarMeasure
ε : ℝ
hε : 0 < ε
x : ↑(sphere 0 1)
⊢ μ.toSphere (ball x ε) ≠ ∞
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
⊢ 0 < ‖l‖

Tactic:
simpa

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

Goal state before:
pp: a : Multiset ℂ
⊢ ∀ i ∈ a, Tendsto (fun n ↦ i / ↑n + 1) atTop (𝓝 ((fun x ↦ 1) i))

Tactic:
intro i hi

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

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

Tactic:
simpa

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

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

Tactic:
simpa

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

Goal state before:
pp: a b : Multiset ℂ
h : a.card = b.card + 1
h' : ∀ j ∈ a, ∀ (k : ℕ), j ≠ -↑k
this✝ : Tendsto (fun n ↦ ‖regularizedHGFunCoeff a b n.succ‖ / ‖regularizedHGFunCoeff a b n‖) atTop (𝓝 1)
this : (FormalMultilinearSeries.ofScalars ℂ (regularizedHGFunCoeff a b)).radius = ↑1⁻¹
⊢ (regularizedHGFunSeries a b).radius = 1

Tactic:
simpa

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

Goal state before:
pp: case pos
L : PeriodPair
x : ℂ
hx : x ∈ L.lattice
⊢ deriv ℘[L] x = ℘'[L] x

Tactic:
rw [deriv_zero_of_not_differentiableAt, L.derivWeierstrassP_coe ⟨x, hx⟩]

Goal state after:
case pos
L : PeriodPair
x : ℂ
hx : x ∈ L.lattice
⊢ ¬DifferentiableAt ℂ ℘[L] x
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: L : PeriodPair
x : ℂ
r : ℕ
hr : 2 < r
⊢ -↑r < -↑(finrank ℤ ↥L.lattice)

Tactic:
simpa

Goal state after:
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.ContDiff

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

Tactic:
rw [← integral_deriv_of_contDiffOn_Icc h hab]
  rw [integral_of_le hab, integral_of_le hab]
  apply MeasureTheory.integral_congr_ae
  rw [← restrict_Ioo_eq_restrict_Ioc]
  filter_upwards [self_mem_ae_restrict measurableSet_Ioo] with x hx
  exact derivWithin_of_mem_nhds (Icc_mem_nhds hx.1 hx.2)

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

Goal state before:
pp: this : 0 ≤ log (rexp 1 / √2)
⊢ log (stirlingSeq 0) - log (stirlingSeq (0 + 1)) ≤ 1 / (12 * ↑0 * (↑0 + 1))

Tactic:
simpa

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

Goal state before:
pp: case pos
L : PeriodPair
l₀ x : ℂ
i : ℕ
hl₀ : l₀ ∈ L.lattice
⊢ (FormalMultilinearSeries.ofScalars ℂ fun i ↦
          if i = 0 then ℘[L - l₀] x else (↑i + 1) * (L.sumInvPow x (i + 2) - ((l₀ - x) ^ (i + 2))⁻¹)).coeff
      (i + 1) =
    ∑' (l : ↥L.lattice),
      if ↑l = l₀ then 0 else (↑(i + 1) + 1) * (↑l - x) ^ (-↑(i + 1 + 2)) - Nat.casesOn (i + 1) (↑l ^ (-2)) 0

Tactic:
trans (i + 2) * (L.sumInvPow x (i + 3) -
        ∑' l : L.lattice, if l = ⟨l₀, hl₀⟩ then (l₀ - x) ^ (-↑(i + 3) : ℤ) else 0)
      · rw [FormalMultilinearSeries.coeff_ofScalars, tsum_ite_eq, zpow_neg, zpow_natCast]
        simp [add_assoc, one_add_one_eq_two]
      · rw [sumInvPow, ← (hasSum_sumInvPow _ _ (by linarith)).summable.tsum_sub, ← tsum_mul_left]
        · simp_rw [Subtype.ext_iff, zpow_neg]
          congr with l
          split_ifs with e
          · simp only [e, zpow_natCast, sub_self, mul_zero]
          · dsimp; norm_cast; ring
        · exact summable_of_hasFiniteSupport ((Set.finite_singleton ⟨l₀, hl₀⟩).subset (by simp))

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

Goal state before:
pp: L : PeriodPair
l₀ z x : ℂ
hx : ∀ (l : ↥L.lattice), ↑l ≠ l₀ → ‖z - x‖ < ‖↑l - x‖
κ : ℝ
hκ : κ > 0
hκ' : Metric.ball 1 κ ⊆ (fun x_1 ↦ x_1 * ‖z - x‖) ⁻¹' (↑(upperClosure (dist x '' (↑L.lattice \ {l₀}))))ᶜ
⊢ 1 < κ / 2 + 1

Tactic:
simpa

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

Goal state before:
pp: ⊢ Tendsto (fun n ↦ ↑n / (2 * ↑n + 1)) atTop (𝓝 (1 / 2))

Tactic:
by
  conv =>
    congr
    · skip
    · skip
    rw [one_div, ← add_zero (2 : ℝ)]
  refine (((tendsto_const_div_atTop_nhds_zero_nat 1).const_add (2 : ℝ)).inv₀
    ((add_zero (2 : ℝ)).symm ▸ two_ne_zero)).congr' (eventually_atTop.mpr ⟨1, fun n hn => ?_⟩)
  rw [add_div' (1 : ℝ) 2 n (cast_ne_zero.mpr (one_le_iff_ne_zero.mp hn)), inv_div]

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:
sumZeroes,

Goal state after:
n : ℕ
ι : Type u_1
s : Finset ι
P : ι → ℝ[X]
⊢ π / ↑n * ∑ i ∈ range n, eval (cos ((2 * ↑i + 1) / (2 * ↑n) * π)) (∑ i ∈ s, P i) =
    ∑ i ∈ s, π / ↑n * ∑ i_1 ∈ range n, eval (cos ((2 * ↑i_1 + 1) / (2 * ↑n) * π)) (P i)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.ChebyshevGauss

Goal state before:
pp: n : ℕ
c : ℝ
P : ℝ[X]
⊢ sumZeroes n (c • P) = c * sumZeroes n P

Tactic:
sumZeroes,

Goal state after:
n : ℕ
c : ℝ
P : ℝ[X]
⊢ π / ↑n * ∑ i ∈ range n, eval (cos ((2 * ↑i + 1) / (2 * ↑n) * π)) (c • P) =
    c * (π / ↑n * ∑ i ∈ range n, eval (cos ((2 * ↑i + 1) / (2 * ↑n) * π)) P)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.ChebyshevGauss

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

Tactic:
sumZeroes,

Goal state after:
n : ℕ
k : ℤ
hk : ¬2 * ↑n ∣ k
hn : n ≠ 0
this : ∑ i ∈ range n, 2 * cos (↑k * ((2 * ↑i + 1) / (2 * ↑n) * π)) = 0
⊢ π / ↑n * ∑ i ∈ range n, eval (cos ((2 * ↑i + 1) / (2 * ↑n) * π)) (T ℝ k) = 0
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.ChebyshevGauss

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

Tactic:
norm_cast at this ⊢

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

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

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

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

Goal state after:
n : ℕ
P : ℝ[X]
hn : 2 ≤ n
hPbnd : ∀ x ∈ Set.Icc (-1) 1, |eval x P| ≤ 1
hP : P.leadingCoeff = 2 ^ (n - 1)
d : ℕ
hd : ↑d = P.degree
hPdeg : ↑d ≤ ↑n
⊢ ↑n ≤ ↑d
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable

Goal state before:
pp: case refine_1
x : Fin 2 → ℤ
hx : x ≠ 0
H0 : max (x 0).natAbs (x 1).natAbs = (x 0).natAbs
⊢ 1 ≤ (↑(x 0) / ‖x‖) ^ 2

Tactic:
have : x 0 ≠ 0 := by
      rwa [← norm_ne_zero_iff, norm_eq_max_natAbs, H0, Nat.cast_ne_zero, Int.natAbs_ne_zero] at hx
    simp only [norm_eq_max_natAbs, H0, Nat.cast_natAbs, Int.cast_abs, div_pow, sq_abs, ne_eq,
      OfNat.ofNat_ne_zero, not_false_eq_true, pow_eq_zero_iff, Int.cast_eq_zero, this, div_self,
      le_refl]

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

Goal state before:
pp: n : ℤ
x : ℝ
hx : |x| ≤ 1
⊢ |eval x (T ℝ n)| ≤ 1

Tactic:
#adaptation_note /-- Before nightly-2026-04-07, this was just
  `grind [eval_T_real_mem_Icc]`. `grind`'s e-matching now keeps the
  `Polynomial.eval` produced by the lemma (which uses `instCommSemiring.toSemiring`)
  and the `Polynomial.eval` propagated by abs unfolding (which uses `Real.semiring`)
  as distinct atoms, even though they are `rfl`-equal, so the contradiction is
  never found. -/
  have h := eval_T_real_mem_Icc n (Set.mem_Icc.mpr (abs_le.mp hx))
  exact abs_le.mpr (Set.mem_Icc.mp h)

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

Goal state before:
pp: case refine_2
n k i : ℕ
hk₁ : 0 < k
hk₂ : k ≤ n
hi : i ≤ n
x : ℝ
hx : 1 ≤ x
⊢ ∀ i_1 ∈ Finset.powersetCard (n - k) ((Finset.range (n + 1)).erase i), 0 ≤ ∏ a ∈ i_1, (x - node n a)

pp: case refine_3
n k i : ℕ
hk₁ : 0 < k
hk₂ : k ≤ n
hi : i ≤ n
x : ℝ
hx : 1 ≤ x
⊢ ∃ i_1 ∈ Finset.powersetCard (n - k) ((Finset.range (n + 1)).erase i), 0 < ∏ a ∈ i_1, (x - node n a)

Tactic:
· exact fun t _ => Finset.prod_nonneg (fun a _ => by grind [show node n a ≤ 1 from cos_le_one _])

Goal state after:
case refine_3
n k i : ℕ
hk₁ : 0 < k
hk₂ : k ≤ n
hi : i ≤ n
x : ℝ
hx : 1 ≤ x
⊢ ∃ i_1 ∈ Finset.powersetCard (n - k) ((Finset.range (n + 1)).erase i), 0 < ∏ a ∈ i_1, (x - node n a)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema

Goal state before:
pp: n : ℕ
hn : n ≠ 0
x : ℝ
hx : |x| ≤ 1
k : ℤ
hk : ↑k * π = ↑n * arccos x
⊢ ↑k = ↑n * (arccos x / π)

Tactic:
simpa [field]

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

Goal state before:
pp: n : ℕ
hn : n ≠ 0
x : ℝ
hx : |x| ≤ 1
k : ℕ
hk : ↑k * π = ↑n * arccos x
hk' : ↑k = ↑n * (arccos x / π)
hkn : ↑k ≤ ↑n
⊢ ↑n ≠ 0

Tactic:
simpa

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

Goal state before:
pp: n : ℕ
P : ℝ[X]
k : ℕ
x : ℝ
hx : 1 ≤ x
hPdeg : P.degree ≤ ↑n
hPbnd : ∀ x ∈ Set.Icc (-1) 1, |eval x P| ≤ 1
hk : n < k
⊢ ↑n < ↑k

Tactic:
simpa

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

Goal state before:
pp: case e'_3
n : ℕ
P : ℝ[X]
k : ℕ
x : ℝ
hx : 1 ≤ x
hPdeg : P.degree ≤ ↑n
hPbnd : ∀ x ∈ Set.Icc (-1) 1, |eval x P| ≤ 1
hk : k ≤ n
⊢ eval x ((⇑derivative)^[k] P) =
    sumNodes ?neg.convert_1✝ (fun i ↦ iterateDerivativeC ?neg.convert_1✝ (?neg.convert_2✝ i) x i) P

Tactic:
rw [sumNodes_eq_eval_iterate_derivative hk x hPdeg]

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

Goal state before:
pp: k : ℝ
hk : 2 < k
this : Summable fun n ↦ ∑' (x : ↥(box n)), ↑n ^ (-k)
n : ℕ
p : ↥(box n)
⊢ ↑n ^ (-k) = ‖![(↑p).1, (↑p).2]‖ ^ (-k)

Tactic:
simp only [← Int.mem_box.mp p.2, Nat.cast_max, norm_eq_max_natAbs, Matrix.cons_val_zero,
        Matrix.cons_val_one]

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

Goal state before:
pp: k : ℝ
hk : 2 < k
n : ℕ
hn : 0 < n
⊢ ‖↑(#(box n)) * ↑n ^ (-k)‖ ≤ 8 * ↑n ^ (1 - k)

Tactic:
rw [Int.card_box hn.ne', Real.norm_of_nonneg (by positivity), sub_eq_add_neg,
      Real.rpow_add (Nat.cast_pos.mpr hn), Real.rpow_one, Nat.cast_mul, Nat.cast_ofNat, mul_assoc]

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

Goal state before:
pp: α : Type u_1
inst✝ : CommSemiring α
n : ℕ
⊢ ↑(Nat.fib n + Nat.fib (n + 1)) = ∑ x, ![1, 1] x * ↑(Nat.fib (n + ↑x))

Tactic:
add_comm

Goal state after:
α : Type u_1
inst✝ : CommSemiring α
n : ℕ
⊢ ↑(Nat.fib (n + 1) + Nat.fib n) = ∑ x, ![1, 1] x * ↑(Nat.fib (n + ↑x))
Module: Mathlib.NumberTheory.Real.GoldenRatio

Goal state before:
pp: ⊢ Set.EqOn (fun n ↦ ↑(Nat.fib n)) (fun n ↦ (φ ^ n - ψ ^ n) / √5) ↑(Finset.range fibRec.order)

Tactic:
intro i hi

Goal state after:
i : ℕ
hi : i ∈ ↑(Finset.range fibRec.order)
⊢ (fun n ↦ ↑(Nat.fib n)) i = (fun n ↦ (φ ^ n - ψ ^ n) / √5) i
Module: Mathlib.Analysis.Subadditive

Goal state before:
pp: u : ℕ → ℝ
h : Subadditive u
L : ℝ
n : ℕ
hn : n ≠ 0
hL : u n / ↑n < L
r : ℕ
x✝ : r < n
⊢ ↑n + 0 ≠ 0

Tactic:
simpa

Goal state after:
Module: Mathlib.Analysis.Subadditive

Goal state before:
pp: u : ℕ → ℝ
h : Subadditive u
hbdd : BddBelow (range fun n ↦ u n / ↑n)
L : ℝ
hL : L > h.lim
⊢ ∃ n, 0 < n ∧ u n / ↑n < L

Tactic:
rw [Subadditive.lim] at hL
      rcases exists_lt_of_csInf_lt (by simp) hL with ⟨x, hx, xL⟩
      rcases (mem_image _ _ _).1 hx with ⟨n, hn, rfl⟩
      exact ⟨n, zero_lt_one.trans_le hn, xL⟩

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

Goal state before:
pp: case hg
k : ℕ
z : ℂ
hz : z ∈ ℍₒ
⊢ ContDiffWithinAt ℂ (↑k) (fun x ↦ -(1 / x)) ℍₒ z

Tactic:
· simp only [one_div]
    apply ContDiffWithinAt.neg
    exact ContDiffWithinAt.inv (by fun_prop) (ne_zero ⟨z, hz⟩)

Goal state after: