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

Goal state before:
pp: p t : ℝ
hp : p ∈ Ioo 0 1
ht : 1 ≤ t
⊢ t ^ (p - 1) * (1 / (t + 1)) = p.rpowIntegrand₀₁ t 1

Tactic:
rpowIntegrand₀₁_eq_pow_div hp (by linarith) zero_le_one,

Goal state after:
p t : ℝ
hp : p ∈ Ioo 0 1
ht : 1 ≤ t
⊢ t ^ (p - 1) * (1 / (t + 1)) = t ^ (p - 1) * 1 / (t + 1)
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:
clog_of_one_le_right,

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

case succ.hr
R : Type u_1
inst✝³ : Semifield R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorSemiring R
b n : ℕ
⊢ 1 ≤ ↑(n + 1)
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 n : ℕ
⊢ clog b ↑n = ↑(Nat.clog b n)

Tactic:
by
  rcases n with - | n
  · simp [clog_of_right_le_one]
  · rw [clog_of_one_le_right, (Nat.ceil_eq_iff (Nat.succ_ne_zero n)).mpr] <;> simp

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

Goal state before:
pp: α : Type u_1
inst✝² : MeasurableSpace α
μ : Measure α
inst✝¹ : TopologicalSpace α
inst✝ : R1Space α
⊢ μ.InnerRegularWRT (fun s ↦ IsCompact s ∧ IsClosed s) IsClosed ↔ μ.InnerRegularWRT (IsCompact ∘ closure) IsClosed

Tactic:
constructor <;> intro h A hA r hr
  · obtain ⟨K, hK1, ⟨hK2, _⟩, hK4⟩ := h hA r hr
    refine ⟨K, hK1, ?_, hK4⟩
    simp only [Function.comp_apply]
    exact hK2.closure
  · obtain ⟨K, hK1, hK2, hK3⟩ := h hA r hr
    refine ⟨closure K, closure_minimal hK1 hA, ?_, ?_⟩
    · simpa only [isClosed_closure, and_true]
    · exact hK3.trans_le (measure_mono subset_closure)

Goal state after:
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
ε : ℝ
f : C(E, ℝ)
K : Set E
hK : MeasurableSet K
hε : 0 < ε
hKP : P Kᶜ < ↑ε.toNNReal
⊢ P.real Kᶜ * (√ε)⁻¹ < √ε

Tactic:
rw [mul_inv_lt_iff₀ (sqrt_pos_of_pos hε), mul_self_sqrt (le_of_lt hε)]

Goal state after:
E : Type u_1
inst✝³ : TopologicalSpace E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
P : Measure E
inst✝ : IsFiniteMeasure P
ε : ℝ
f : C(E, ℝ)
K : Set E
hK : MeasurableSet K
hε : 0 < ε
hKP : P Kᶜ < ↑ε.toNNReal
⊢ P.real Kᶜ < ε
Module: Mathlib.Analysis.SpecialFunctions.MulExpNegMulSqIntegral

Goal state before:
pp: ε : ℝ
E : Type u_2
inst✝⁶ : MeasurableSpace E
inst✝⁵ : PseudoEMetricSpace E
inst✝⁴ : BorelSpace E
inst✝³ : CompleteSpace E
inst✝² : SecondCountableTopology E
P P' : Measure E
inst✝¹ : IsFiniteMeasure P
inst✝ : IsFiniteMeasure P'
f : E →ᵇ ℝ
A : Subalgebra ℝ (E →ᵇ ℝ)
hA : (Subalgebra.map (toContinuousMapₐ ℝ) A).SeparatesPoints
heq : ∀ g ∈ A, ∫ (x : E), g x ∂P = ∫ (x : E), g x ∂P'
hε : 0 < ε
hPP' : ¬(P = 0 ∧ P' = 0)
const : ℝ := max (P.real Set.univ) (P'.real Set.univ)
pos_of_measure : 0 < const
KP : Set E
left✝¹ : KP ⊆ Set.univ
hKPco : IsCompact KP
hKPcl : IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] KP
KP' : Set E
left✝ : KP' ⊆ Set.univ
hKP'co : IsCompact KP'
hKP'cl : IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] KP'
K : Set E := KP ∪ KP'
hKco : IsCompact (KP ∪ KP')
hKcl : IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (KP ∪ KP')
hKP : P KPᶜ < ENNReal.ofReal ε
hKP' : P' KP'ᶜ < ENNReal.ofReal ε
hKPbound : P (KP ∪ KP')ᶜ < ↑ε.toNNReal
hKP'bound : P' (KP ∪ KP')ᶜ < ↑ε.toNNReal
g' : C(E, ℝ)
hg'approx : ∀ x ∈ KP ∪ KP', ‖g' x - ↑f x‖ < √ε * const⁻¹
hg'A : ∃ x ∈ A, (toContinuousMapₐ ℝ) x = g'
g : E →ᵇ ℝ := hg'A.choose
hgA : g ∈ A
hgapprox : ∀ x ∈ K, ‖g x - f x‖ < √ε * const⁻¹
line1 : |∫ (x : E), ε.mulExpNegMulSq (f x) ∂P - ∫ (x : E) in K, ε.mulExpNegMulSq (f x) ∂P| < √ε
⊢ |∫ (x : E) in K, ε.mulExpNegMulSq (g x) ∂P - ∫ (x : E), ε.mulExpNegMulSq (g x) ∂P| < √ε

Tactic:
abs_sub_comm

Goal state after:
ε : ℝ
E : Type u_2
inst✝⁶ : MeasurableSpace E
inst✝⁵ : PseudoEMetricSpace E
inst✝⁴ : BorelSpace E
inst✝³ : CompleteSpace E
inst✝² : SecondCountableTopology E
P P' : Measure E
inst✝¹ : IsFiniteMeasure P
inst✝ : IsFiniteMeasure P'
f : E →ᵇ ℝ
A : Subalgebra ℝ (E →ᵇ ℝ)
hA : (Subalgebra.map (toContinuousMapₐ ℝ) A).SeparatesPoints
heq : ∀ g ∈ A, ∫ (x : E), g x ∂P = ∫ (x : E), g x ∂P'
hε : 0 < ε
hPP' : ¬(P = 0 ∧ P' = 0)
const : ℝ := max (P.real Set.univ) (P'.real Set.univ)
pos_of_measure : 0 < const
KP : Set E
left✝¹ : KP ⊆ Set.univ
hKPco : IsCompact KP
hKPcl : IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] KP
KP' : Set E
left✝ : KP' ⊆ Set.univ
hKP'co : IsCompact KP'
hKP'cl : IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] KP'
K : Set E := KP ∪ KP'
hKco : IsCompact (KP ∪ KP')
hKcl : IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (KP ∪ KP')
hKP : P KPᶜ < ENNReal.ofReal ε
hKP' : P' KP'ᶜ < ENNReal.ofReal ε
hKPbound : P (KP ∪ KP')ᶜ < ↑ε.toNNReal
hKP'bound : P' (KP ∪ KP')ᶜ < ↑ε.toNNReal
g' : C(E, ℝ)
hg'approx : ∀ x ∈ KP ∪ KP', ‖g' x - ↑f x‖ < √ε * const⁻¹
hg'A : ∃ x ∈ A, (toContinuousMapₐ ℝ) x = g'
g : E →ᵇ ℝ := hg'A.choose
hgA : g ∈ A
hgapprox : ∀ x ∈ K, ‖g x - f x‖ < √ε * const⁻¹
line1 : |∫ (x : E), ε.mulExpNegMulSq (f x) ∂P - ∫ (x : E) in K, ε.mulExpNegMulSq (f x) ∂P| < √ε
⊢ |∫ (x : E), ε.mulExpNegMulSq (g x) ∂P - ∫ (x : E) in K, ε.mulExpNegMulSq (g x) ∂P| < √ε
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) ≤ ↑(dim E) * μ (Ioo 0 1 • Subtype.val '' ball x ε)

Tactic:
Subtype.image_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 • (ball (↑x) ε ∩ {a | a ∈ sphere 0 1}))
Module: Mathlib.Analysis.SpecialFunctions.RegularizedHypergeometric

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

Tactic:
by
      congr 1
      rw [← pow_succ', ← zpow_natCast, ← zpow_natCast, ← zpow_add' (by left; norm_cast)]
      grind

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

Goal state before:
pp: case neg
L : PeriodPair
l₀ : ℂ
s : Finset ↥L.lattice
l : ℂ
hl : l ∈ (↑L.lattice \ {l₀})ᶜ
x : ↥L.lattice
hl₁✝ : ¬↑x = l₀
hl₁ : l - ↑x ≠ 0
⊢ -2 / (l - ↑x) ^ 3 = deriv (fun x2 ↦ 1 / (x2 - ↑x) ^ 2) l - deriv (fun x2 ↦ 1 / ↑x ^ 2) l

Tactic:
deriv_const

Goal state after:
case neg
L : PeriodPair
l₀ : ℂ
s : Finset ↥L.lattice
l : ℂ
hl : l ∈ (↑L.lattice \ {l₀})ᶜ
x : ↥L.lattice
hl₁✝ : ¬↑x = l₀
hl₁ : l - ↑x ≠ 0
⊢ -2 / (l - ↑x) ^ 3 = deriv (fun x2 ↦ 1 / (x2 - ↑x) ^ 2) l - 0
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Basic

Goal state before:
pp: θ : ℂ
n : ℤ
⊢ eval (cosh θ) (U ℂ n) * sinh θ = eval (cos (θ * I)) (U ℂ n) * sin (θ * I) * -I

Tactic:
by simp [cos_mul_I, sin_mul_I, mul_assoc]

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

Goal state before:
pp: case pos
x : ℝ
h : x ≠ -1 ∧ x ≠ 1
⊢ deriv arcsin x = 1 / √(1 - x ^ 2)

pp: case neg
x : ℝ
h : ¬(x ≠ -1 ∧ x ≠ 1)
⊢ deriv arcsin x = 1 / √(1 - x ^ 2)

Tactic:
· exact (hasDerivAt_arcsin h.1 h.2).deriv

Goal state after:
case neg
x : ℝ
h : ¬(x ≠ -1 ∧ x ≠ 1)
⊢ deriv arcsin x = 1 / √(1 - x ^ 2)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Orthogonality

Goal state before:
pp: f : ℝ → ℝ
⊢ (∫ (x : ℝ) in Set.Ioc (-1) 1, f x ∂volume.withDensity fun x ↦ ↑(NNReal.mk √(1 - x ^ 2)⁻¹ ⋯)) =
    ∫ (x : ℝ) in Set.Ioc (-1) 1, f x * √(1 - x ^ 2)⁻¹ ∂volume

Tactic:
restrict_withDensity (by measurability),

Goal state after:
f : ℝ → ℝ
⊢ (∫ (x : ℝ), f x ∂(volume.restrict (Set.Ioc (-1) 1)).withDensity fun x ↦ ↑(NNReal.mk √(1 - x ^ 2)⁻¹ ⋯)) =
    ∫ (x : ℝ) in Set.Ioc (-1) 1, f x * √(1 - x ^ 2)⁻¹ ∂volume
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Orthogonality

Goal state before:
pp: f : ℝ → ℝ
hf : ContinuousOn f (Set.uIcc (-1) 1)
this : IntegrableOn (fun x ↦ f x * √(1 - x ^ 2)⁻¹) (Set.Ioc (-1) 1) volume
⊢ Integrable f ((volume.withDensity fun x ↦ ↑(NNReal.mk √(1 - x ^ 2)⁻¹ ⋯)).restrict (Set.Ioc (-1) 1))

Tactic:
restrict_withDensity (by measurability),

Goal state after:
f : ℝ → ℝ
hf : ContinuousOn f (Set.uIcc (-1) 1)
this : IntegrableOn (fun x ↦ f x * √(1 - x ^ 2)⁻¹) (Set.Ioc (-1) 1) volume
⊢ Integrable f ((volume.restrict (Set.Ioc (-1) 1)).withDensity fun x ↦ ↑(NNReal.mk √(1 - x ^ 2)⁻¹ ⋯))
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Orthogonality

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

Tactic:
← integral_comp_mul_deriv_of_deriv_nonpos (f' := fun x => -(1 / √(1 - x ^ 2)))

Goal state after:
f : ℝ → ℝ
⊢ ∫ (x : ℝ) in 1..-1, f x * -√(1 - x ^ 2)⁻¹ = ∫ (x : ℝ) in 1..-1, ((fun θ ↦ f (cos θ)) ∘ arccos) x * -(1 / √(1 - x ^ 2))

case hf
f : ℝ → ℝ
⊢ ContinuousOn arccos (uIcc 1 (-1))

case hff'
f : ℝ → ℝ
⊢ ∀ x ∈ Ioo (min 1 (-1)) (max 1 (-1)), HasDerivAt arccos (-(1 / √(1 - x ^ 2))) x

case hf'
f : ℝ → ℝ
⊢ ∀ x ∈ Ioo (min 1 (-1)) (max 1 (-1)), -(1 / √(1 - x ^ 2)) ≤ 0
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Orthogonality

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

Tactic:
T_real_cos

Goal state after:
n : ℤ
hn : n ≠ 0
hn' : ↑n ≠ 0
this : ∫ (θ : ℝ) in 0..↑n * π, cos θ = 0
⊢ ∫ (θ : ℝ) in 0..π, cos (↑n * θ) = 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)
⊢ 0 < (-1) ^ i * ∏ j ∈ (Finset.range (n + 1)).erase i, (node n i - node n j)

Tactic:
have union : (Finset.range (n + 1)).erase i = (Finset.range i) ∪ Finset.Ioc i n := by grind

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
⊢ 0 < (-1) ^ i * ∏ j ∈ (Finset.range (n + 1)).erase i, (node n i - node n j)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.ChebyshevGauss

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

Tactic:
← Complex.exp_nat_mul,

Goal state after:
case e'_2.a
n : ℕ
k : ℤ
hn : n ≠ 0
hk : ¬2 * ↑n ∣ k
i : ℕ
hi : i ∈ range n
⊢ Complex.exp (↑k * ((2 * ↑i + 1) / (2 * ↑n) * ↑π) * I) * Complex.exp (-(↑k / (2 * ↑n) * ↑π * I)) *
      (Complex.exp (↑k / ↑n * ↑π * I) - 1) =
    Complex.exp (↑i * (↑k / ↑n * ↑π * I)) * (Complex.exp (↑k / ↑n * ↑π * I) - 1)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.ChebyshevGauss

Goal state before:
pp: case e'_3
n : ℕ
k : ℤ
hn : n ≠ 0
hk : ¬2 * ↑n ∣ k
⊢ (-1) ^ k - 1 = Complex.exp (↑k / ↑n * ↑π * I) ^ n - 1

Tactic:
← Complex.exp_nat_mul,

Goal state after:
case e'_3
n : ℕ
k : ℤ
hn : n ≠ 0
hk : ¬2 * ↑n ∣ k
⊢ (-1) ^ k - 1 = Complex.exp (↑n * (↑k / ↑n * ↑π * I)) - 1
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.ChebyshevGauss

Goal state before:
pp: case inr.h
n : ℕ
k : ℤ
hk : ¬2 * ↑n ∣ k
hn : n ≠ 0
this : (-1) ^ (-k) = (-1) ^ k
z : ℂ := Complex.exp (↑k / (2 * ↑n) * ↑π * I)
hz : z = Complex.exp (↑k / (2 * ↑n) * ↑π * I)
hz₂ : Complex.exp (↑k / ↑n * ↑π * I) = z ^ 2
⊢ z / (Complex.exp (↑k / ↑n * ↑π * I) - 1) + z⁻¹ / ((Complex.exp (↑k / ↑n * ↑π * I))⁻¹ - 1) = 0

Tactic:
rw [hz₂, ← inv_pow z 2]

Goal state after:
case inr.h
n : ℕ
k : ℤ
hk : ¬2 * ↑n ∣ k
hn : n ≠ 0
this : (-1) ^ (-k) = (-1) ^ k
z : ℂ := Complex.exp (↑k / (2 * ↑n) * ↑π * I)
hz : z = Complex.exp (↑k / (2 * ↑n) * ↑π * I)
hz₂ : Complex.exp (↑k / ↑n * ↑π * I) = z ^ 2
⊢ z / (z ^ 2 - 1) + z⁻¹ / (z⁻¹ ^ 2 - 1) = 0
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.ChebyshevGauss

Goal state before:
pp: n : ℕ
P : ℝ[X]
hn : n ≠ 0
hP : P.degree < 2 * ↑n
hmem : P ∈ degreeLT ℝ (2 * n)
⊢ ∫ (x : ℝ), eval x P ∂measureT = sumZeroes n P

Tactic:
rw [← Sequence.span_degreeLT (chebyshevTsequence ℝ) (by simp),
    show Set.Iio (2 * n) = Finset.range (2 * n) by simp,
    Submodule.mem_span_image_finset_iff_exists_fun'] at hmem

Goal state after:
n : ℕ
P : ℝ[X]
hn : n ≠ 0
hP : P.degree < 2 * ↑n
hmem : ∃ c, ∑ i ∈ range (2 * n), c i • ↑(chebyshevTsequence ℝ) i = P
⊢ ∫ (x : ℝ), eval x P ∂measureT = sumZeroes n P
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal

Goal state before:
pp: n i : ℕ
hi : i ≤ n
⊢ 0 < (-1) ^ i * leadingCoeffC n i

Tactic:
by
  have := inv_pos_of_pos <| zero_lt_prod_node_sub_node hi
  rwa [mul_inv, ← inv_pow, inv_neg_one] at this

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
⊢ eval x ((⇑derivative)^[k] P) ≤ eval x ((⇑derivative)^[k] (T ℝ ↑n))

Tactic:
by_cases! hk : n < k

Goal state after:
case pos
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
⊢ eval x ((⇑derivative)^[k] P) ≤ eval x ((⇑derivative)^[k] (T ℝ ↑n))

case neg
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) ≤ eval x ((⇑derivative)^[k] (T ℝ ↑n))
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: L : PeriodPair
l₀ : ℂ
h : l₀ ∈ L.lattice
⊢ meromorphicOrderAt ℘[L] l₀ = ↑(-2)

Tactic:
rw [meromorphicOrderAt_eq_int_iff (L.meromorphic_weierstrassP l₀)]

Goal state after:
L : PeriodPair
l₀ : ℂ
h : l₀ ∈ L.lattice
⊢ ∃ g, AnalyticAt ℂ g l₀ ∧ g l₀ ≠ 0 ∧ ∀ᶠ (z : ℂ) in 𝓝[≠] l₀, ℘[L] z = (z - l₀) ^ (-2) • g z
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable

Goal state before:
pp: z : ℂ
c₁ c₂ : ℤ
⊢ Summable fun n ↦ ((↑c₁ * z + ↑n + 1) * (↑c₂ * z + ↑n))⁻¹

Tactic:
by
  apply summable_inv_of_isBigO_rpow_inv (a := 2) (by norm_cast)
  simpa [pow_two] using (linear_inv_isBigO_right c₂ z).mul
    (linear_inv_isBigO_right_add c₁ 1 z)

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

Goal state before:
pp: L : PeriodPair
⊢ AnalyticAt ℂ L.relation 0

Tactic:
by
  refine .of_meromorphicOrderAt_pos (one_pos.trans_le ?_) (by simp [relation])
  suffices 7 ≤ meromorphicOrderAt (L.relation * id ^ 6) 0 by
    rw [meromorphicOrderAt_mul (by fun_prop) (by fun_prop),
      meromorphicOrderAt_pow (by fun_prop)] at this
    rw [← WithTop.add_le_add_iff_right (z := 6) (by simp)]
    simpa [-add_le_add_iff_left_of_ne_top] using! this
  rw [AnalyticAt.meromorphicOrderAt_eq (by fun_prop)]
  refine ENat.monotone_map_iff.mpr Nat.mono_cast
    ((natCast_le_analyticOrderAt_iff_iteratedDeriv_eq_zero (by fun_prop)).mpr fun i hi₁ ↦ ?_)
  by_cases hi₂ : Odd i
  · simpa [← CharZero.eq_neg_self_iff, hi₂, (show Even 6 by decide).neg_pow] using!
      (iteratedDeriv_comp_neg i (L.relation * id ^ 6) 0 :)
  by_cases hi₃ : i = 0
  · simp [hi₃]
  by_cases hi₄ : i = 6
  · exact hi₄ ▸ L.iteratedDeriv_six_relation_mul_id_pow_six
  rw [L.relation_mul_id_pow_six_eventuallyEq.iteratedDeriv_eq]
  simp_rw [pow_succ (_ + _), pow_succ (_ - _), pow_zero, one_mul]
  simp (discharger := fun_prop) only [iteratedDeriv_fun_add, iteratedDeriv_fun_sub,
    iteratedDeriv_fun_mul, iteratedDeriv_const, iteratedDeriv_fun_pow_zero,
    iteratedDeriv_derivWeierstrassPExcept_self, iteratedDeriv_weierstrassPExcept_self]
  obtain rfl | rfl : i = 2 ∨ i = 4 := by grind
  · simp [Finset.sum_range_succ]
  · simp [Finset.sum_range_succ, show Nat.choose 4 2 = 6 by rfl, g₂]; ring

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

Goal state before:
pp: β : Type u_2
inst✝ : CommRing β
⊢ fibRec.charPoly = X ^ 2 - (X + 1)

Tactic:
rw [fibRec, LinearRecurrence.charPoly]
  simp [Finset.sum_fin_eq_sum_range, Finset.sum_range_succ', ← smul_X_eq_monomial]

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

Goal state before:
pp: k : ℕ
z : ℂ
hz : z ∈ ℍₒ
⊢ iteratedDerivWithin k (fun x ↦ ↑π * (↑π * x).cot - 1 / x) ℍₒ z =
    iteratedDerivWithin k (fun x ↦ ↑π * (↑π * x).cot) ℍₒ z - (-1) ^ k * ↑k ! * z ^ (-1 - ↑k)

Tactic:
by
  simp_rw [sub_eq_add_neg]
  rw [iteratedDerivWithin_fun_add hz isOpen_upperHalfPlaneSet.uniqueDiffOn]
  · simpa [iteratedDerivWithin_fun_neg] using! iteratedDerivWithin_one_div k
      isOpen_upperHalfPlaneSet hz
  · exact ContDiffWithinAt.mul (by fun_prop) (cot_pi_mul_contDiffWithinAt k
      (UpperHalfPlane.coe_mem_integerComplement ⟨z, hz⟩))
  · simp only [one_div]
    apply ContDiffWithinAt.neg
    exact ContDiffWithinAt.inv (by fun_prop) (ne_zero ⟨z, hz⟩)

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

Goal state before:
pp: u : ℕ → ℝ
l : ℝ
hmono : Monotone u
hlim :
  ∀ (a : ℝ),
    1 < a →
      ∃ c,
        (∀ᶠ (n : ℕ) in atTop, ↑(c (n + 1)) ≤ a * ↑(c n)) ∧
          Tendsto c atTop atTop ∧ Tendsto (fun n ↦ u (c n) / ↑(c n)) atTop (𝓝 l)
lnonneg : 0 ≤ l
ε : ℝ
εpos : 0 < ε
c : ℕ → ℕ
cgrowth : ∀ᶠ (n : ℕ) in atTop, ↑(c (n + 1)) ≤ (1 + ε) * ↑(c n)
ctop : Tendsto c atTop atTop
clim : Tendsto (fun n ↦ u (c n) / ↑(c n)) atTop (𝓝 l)
L : ∀ᶠ (n : ℕ) in atTop, u (c n) - ↑(c n) * l ≤ ε * ↑(c n)
a : ℕ
ha : ∀ (b : ℕ), a ≤ b → ↑(c (b + 1)) ≤ (1 + ε) * ↑(c b) ∧ u (c b) - ↑(c b) * l ≤ ε * ↑(c b)
M : ℕ := (image (fun i ↦ c i) (range (a + 1))).max' ⋯
n : ℕ
hn : n ∈ Set.Ici M
exN : ∃ N, n < c N
N : ℕ := Nat.find exN
ncN : n < c N
aN : a + 1 ≤ N
Npos : 0 < N
cNn : c (N - 1) ≤ n
IcN : ↑(c N) ≤ (1 + ε) * ↑(c (N - 1))
⊢ u (c N) - ↑(c N) * l + (↑(c N) - ↑(c (N - 1))) * l ≤ ε * ↑(c N) + ε * ↑(c (N - 1)) * l

Tactic:
by
        gcongr
        · exact (ha N (a.le_succ.trans aN)).2
        · linarith only [IcN]

Goal state after:
Module: Mathlib.Analysis.SumIntegralComparisons

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

Tactic:
by
      rw [Finset.sum_Ico_eq_sum_range]
      grind

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Indization

Goal state before:
pp: C : Type v
inst✝¹ : SmallCategory C
inst✝ : Abelian C
X Y : Ind C
f : X ⟶ Y
⊢ IsIso (coimageImageComparison f)

Tactic:
obtain ⟨I, _, _, F, G, ϕ, ⟨i⟩⟩ := Ind.exists_nonempty_arrow_mk_iso_ind_lim (f := f)

Goal state after:
C : Type v
inst✝¹ : SmallCategory C
inst✝ : Abelian C
X Y : Ind C
f : X ⟶ Y
I : Type v
w✝¹ : SmallCategory I
w✝ : IsFiltered I
F G : I ⥤ C
ϕ : F ⟶ G
i : Arrow.mk f ≅ Arrow.mk ((Ind.lim I).map ϕ)
⊢ IsIso (coimageImageComparison f)
Module: Mathlib.CategoryTheory.Limits.FilteredColimitCommutesProduct

Goal state before:
pp: α : Type u
I : α → Type u
inst✝¹ : (i : α) → SmallCategory (I i)
inst✝ : ∀ (i : α), IsFiltered (I i)
F : (i : α) → I i ⥤ Type u
⊢ IsIso (colimitPointwiseProductToProductColimit F)

Tactic:
refine (isIso_iff_bijective _).2 ⟨fun y y' hy => ?_, fun x => ?_⟩
  · obtain ⟨ky, yk₀, hyk₀⟩ := Types.jointly_surjective' y
    obtain ⟨ky', yk₀', hyk₀'⟩ := Types.jointly_surjective' y'
    let k := IsFiltered.max ky ky'
    let yk : (pointwiseProduct F).obj k :=
      (pointwiseProduct F).map (IsFiltered.leftToMax ky ky') yk₀
    let yk' : (pointwiseProduct F).obj k :=
      (pointwiseProduct F).map (IsFiltered.rightToMax ky ky') yk₀'
    obtain rfl : y = colimit.ι (pointwiseProduct F) k yk := by
      simp only [k, yk, colimit.w_apply, hyk₀]
    obtain rfl : y' = colimit.ι (pointwiseProduct F) k yk' := by
      simp only [k, yk', colimit.w_apply, hyk₀']
    dsimp at yk yk'
    have hch : ∀ (s : α), ∃ (i' : I s) (hi' : k s ⟶ i'),
        (F s).map hi' (Pi.π (fun s => (F s).obj (k s)) s yk) =
          (F s).map hi' (Pi.π (fun s => (F s).obj (k s)) s yk') := by
      intro s
      have hy₁ := congr_hom (ι_colimitPointwiseProductToProductColimit_π F k s) yk
      have hy₂ := congr_hom (ι_colimitPointwiseProductToProductColimit_π F k s) yk'
      dsimp at hy₁ hy₂ hy
      rw [← hy, hy₁, Types.FilteredColimit.colimit_eq_iff] at hy₂
      obtain ⟨i₀, f₀, g₀, h₀⟩ := hy₂
      refine ⟨IsFiltered.coeq f₀ g₀, f₀ ≫ IsFiltered.coeqHom f₀ g₀, ?_⟩
      conv_rhs => rw [IsFiltered.coeq_condition]
      dsimp [Functor.pi] at h₀
      simp [h₀]
    choose k' f hk' using hch
    apply Types.colimit_sound' f f
    exact Types.limit_ext' _ _ _ (fun ⟨s⟩ => by simpa [Functor.pi, Pi.map_π_apply] using hk' s)
  · have hch : ∀ (s : α), ∃ (i : I s) (xi : (F s).obj i), colimit.ι (F s) i xi =
        Pi.π (fun s => colimit (F s)) s x := fun s => Types.jointly_surjective' _
    choose k p hk using hch
    refine ⟨colimit.ι (pointwiseProduct F) k ((Types.productIso _).inv p), ?_⟩
    refine Types.limit_ext' _ _ _ (fun ⟨s⟩ => ?_)
    have := congr_hom (ι_colimitPointwiseProductToProductColimit_π F k s)
      ((Types.productIso _).inv p)
    exact this.trans (by simpa [Functor.pi] using hk _)

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ModuleEmbedding.GabrielPopescu

Goal state before:
pp: case refine_2
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : IsGrothendieckAbelian.{v, v, u} C
G : C
hG : IsSeparator G
B : C
hB : Injective B
M : Ideal (End G)ᵐᵒᵖ
g : ↥M →ₗ[(End G)ᵐᵒᵖ] G ⟶ B
l : G ⟶ B
hl :
  d (ModuleCat.ofHom { toFun := fun i ↦ MulOpposite.unop ↑i, map_add' := ⋯, map_smul' := ⋯ }) ≫ l =
    d (ModuleCat.ofHom g)
⊢ ∀ (x : (End G)ᵐᵒᵖ) (mem : x ∈ M),
    (ModuleCat.Hom.hom ((preadditiveCoyonedaObj G).map l) ∘ₗ ↑(Preadditive.homSelfLinearEquivEndMulOpposite G).symm) x =
      g ⟨x, mem⟩

Tactic:
intro f

Goal state after:
case refine_2
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : IsGrothendieckAbelian.{v, v, u} C
G : C
hG : IsSeparator G
B : C
hB : Injective B
M : Ideal (End G)ᵐᵒᵖ
g : ↥M →ₗ[(End G)ᵐᵒᵖ] G ⟶ B
l : G ⟶ B
hl :
  d (ModuleCat.ofHom { toFun := fun i ↦ MulOpposite.unop ↑i, map_add' := ⋯, map_smul' := ⋯ }) ≫ l =
    d (ModuleCat.ofHom g)
f : (End G)ᵐᵒᵖ
⊢ ∀ (mem : f ∈ M),
    (ModuleCat.Hom.hom ((preadditiveCoyonedaObj G).map l) ∘ₗ ↑(Preadditive.homSelfLinearEquivEndMulOpposite G).symm) f =
      g ⟨f, mem⟩
Module: Mathlib.CategoryTheory.Abelian.Preradical.Radical

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
Φ : Radical C
⊢ IsZero (Φ.obj.quotient ⋙ Φ.obj.r)

Tactic:
rw [← Preradical.isRadical_iff_isZero, Preradical.isRadical_iff_isIso]
  infer_instance

Goal state after: