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

Goal state before:
pp: s : ℂ
hs : ∀ (n : ℕ), s ≠ -(2 * ↑n + 1)
this : (s + 1).Gammaℝ ≠ 0
⊢ 2 * (2 * ↑π) ^ (-s) * Gamma s / (cos (↑π * s / 2))⁻¹ = s.Gammaℂ * cos (↑π * s / 2)

Tactic:
by rw [Gammaℂ_def, div_eq_mul_inv, inv_inv]

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

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

Tactic:
have h1 : Gammaℝ s ≠ 0 := by
    rw [Ne, Gammaℝ_eq_zero_iff, not_exists]
    intro n h
    specialize hs (2 * n)
    simp_all

Goal state after:
s : ℂ
hs : ∀ (n : ℕ), s ≠ -↑n
h1 : s.Gammaℝ ≠ 0
⊢ (1 - s).Gammaℝ⁻¹ = s.Gammaℂ * cos (↑π * s / 2) * s.Gammaℝ⁻¹
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Digamma

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

Tactic:
div_mul_cancel_right₀ (Gamma_ne_zero hs),

Goal state after:
s : ℂ
hs : ∀ (m : ℕ), s ≠ -↑m
hs0 : s ≠ 0
⊢ s⁻¹ + s * deriv Gamma s / (s * Gamma s) = deriv Gamma s / Gamma s + s⁻¹
Module: Mathlib.Analysis.SpecialFunctions.Gaussian.PoissonSummation

Goal state before:
pp: a : ℝ
ha : a < 0
b s : ℝ
this : (fun x ↦ rexp (a * x ^ 2 + b * x)) =o[atTop] fun x ↦ rexp (-x)
⊢ (fun x ↦ rexp (a * x ^ 2 + b * x)) =o[atTop] fun x ↦ x ^ s

Tactic:
by
    refine this.trans ?_
    simpa only [neg_one_mul] using isLittleO_exp_neg_mul_rpow_atTop zero_lt_one s

Goal state after:
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)
hbound : ∀ᵐ (t : ℝ) ∂μ.restrict (Ioi 0), ∀ z ∈ quasispectrum ℝ a, ‖f t z‖ ≤ bound t
hbound_finite_integral : HasFiniteIntegral bound (μ.restrict (Ioi 0))
hmapzero : ∀ᵐ (x : ℝ) ∂μ.restrict (Ioi 0), (↑p).rpowIntegrand₀₁ x 0 = 0
⊢ cfcₙ (fun x ↦ x ^ ↑p) a = cfcₙ (fun r ↦ ∫ (t : ℝ) in Ioi 0, (↑p).rpowIntegrand₀₁ t r ∂μ) a

Tactic:
exact cfcₙ_congr fun r _ ↦ (hμ r (by grind)).2

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
⊢ HasDerivAt Gammaℂ (-(↑γ + log (2 * ↑π)) / ↑π) 1

Tactic:
have := this.mul hasDerivAt_Gamma_one

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 * ↑π) / ↑π * Gamma 1 + 2 * (2 * ↑π) ^ (-1) * -↑γ) 1
⊢ HasDerivAt Gammaℂ (-(↑γ + log (2 * ↑π)) / ↑π) 1
Module: Mathlib.Analysis.SpecialFunctions.Log.Base

Goal state before:
pp: b : ℝ
b_pos : 0 < b
b_ne_one : b ≠ 1
⊢ SurjOn (logb b) (Iio 0) univ

Tactic:
by
  intro x _
  use -b ^ x
  constructor
  · simp only [Right.neg_neg_iff, Set.mem_Iio]
    apply rpow_pos_of_pos b_pos
  · rw [logb_neg_eq_logb, logb_rpow b_pos b_ne_one]

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

Goal state before:
pp: A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
p t : ℝ
hp : p ∈ Ioo 0 1
ht : 0 < t
a : A
⊢ a ∈ Ici 0 → ∀ ⦃b : A⦄, b ∈ Ici 0 → a ≤ b → cfcₙ (p.rpowIntegrand₀₁ t) a ≤ cfcₙ (p.rpowIntegrand₀₁ t) b

Tactic:
(ha : 0 ≤ a)

Goal state after:
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
p t : ℝ
hp : p ∈ Ioo 0 1
ht : 0 < t
a : A
ha : 0 ≤ a
⊢ ∀ ⦃b : A⦄, b ∈ Ici 0 → a ≤ b → cfcₙ (p.rpowIntegrand₀₁ t) a ≤ cfcₙ (p.rpowIntegrand₀₁ t) b
Module: Mathlib.Analysis.SpecialFunctions.Log.Base

Goal state before:
pp: case a
b : ℕ
r : ℝ
hr✝ : 0 ≤ r
hr : 0 < r
hb : 1 < b
hb1' : 1 < ↑b
⊢ Int.log b r ≤ ⌊logb (↑b) r⌋

Tactic:
rw [Int.le_floor, le_logb_iff_rpow_le hb1' hr, rpow_intCast]

Goal state after:
case a
b : ℕ
r : ℝ
hr✝ : 0 ≤ r
hr : 0 < r
hb : 1 < b
hb1' : 1 < ↑b
⊢ ↑b ^ Int.log b r ≤ r
Module: Mathlib.Analysis.SpecialFunctions.MulExpNegMulSq

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

pp: case h
ε : ℝ
hε : 0 < ε
x : ℝ
⊢ |mulExpNegMulSq 1 (√ε * x)| ≤ 1

Tactic:
· positivity

Goal state after:
case h
ε : ℝ
hε : 0 < ε
x : ℝ
⊢ |mulExpNegMulSq 1 (√ε * x)| ≤ 1
Module: Mathlib.Analysis.SpecialFunctions.MulExpNegMulSq

Goal state before:
pp: ε : ℝ
E : Type u_1
inst✝ : TopologicalSpace E
x : E
g : E →ᵇ ℝ
hε : 0 ≤ ε
⊢ 0 ≤ ε * (g x * g x)

Tactic:
exact mul_nonneg hε (mul_self_nonneg (g x))

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
hb₁ : 1 < b
x : ℝ
hx₁ : 1 ≤ x
⊢ logb b x = |logb b x|

Tactic:
rw [abs_of_nonneg]

Goal state after:
b✝ b : ℝ
hb : b ≠ -1 ∧ b ≠ 0 ∧ b ≠ 1
hb₀ : 0 < b
hb₁ : 1 < b
x : ℝ
hx₁ : 1 ≤ x
⊢ 0 ≤ logb b x
Module: Mathlib.MeasureTheory.Integral.BoundedContinuousFunction

Goal state before:
pp: X : Type u_1
inst✝⁸ : MeasurableSpace X
inst✝⁷ : TopologicalSpace X
E : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : OpensMeasurableSpace X
inst✝⁴ : SecondCountableTopology E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : NormedSpace ℝ E
ι : Type u_3
μs : ι → Measure X
inst✝ : ∀ (i : ι), IsProbabilityMeasure (μs i)
f : X →ᵇ E
v : E
i : ι
hi : (fun i ↦ ∫ (x : X), f x ∂μs i) i = v
⊢ ‖v‖ ≤ ‖f‖

Tactic:
rw [← hi]

Goal state after:
X : Type u_1
inst✝⁸ : MeasurableSpace X
inst✝⁷ : TopologicalSpace X
E : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : OpensMeasurableSpace X
inst✝⁴ : SecondCountableTopology E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : NormedSpace ℝ E
ι : Type u_3
μs : ι → Measure X
inst✝ : ∀ (i : ι), IsProbabilityMeasure (μs i)
f : X →ᵇ E
v : E
i : ι
hi : (fun i ↦ ∫ (x : X), f x ∂μs i) i = v
⊢ ‖(fun i ↦ ∫ (x : X), f x ∂μs i) i‖ ≤ ‖f‖
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
⊢ P.InnerRegularWRT IsCompact IsClosed

Tactic:
rw [← innerRegularWRT_isCompact_closure_iff]
  exact innerRegularWRT_isCompact_closure P

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

Goal state before:
pp: case neg
n : ℕ
ε : ℝ
h : ¬(n ≠ 0 ∧ 0 < ε)
⊢ 0 < 1

Tactic:
· positivity

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
F : Type u_2
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : Nontrivial E
μ : Measure E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : BorelSpace E
inst✝ : μ.IsAddHaarMeasure
f : ℝ → F
this :
  Integrable (fun x ↦ f ‖↑x‖) (Measure.comap Subtype.val μ) ↔
    Integrable (fun x ↦ f ↑x.2) (μ.toSphere.prod (Measure.volumeIoiPow (dim E - 1)))
⊢ Integrable (fun x ↦ f ↑x.2) (μ.toSphere.prod (Measure.volumeIoiPow (dim E - 1))) ↔
    IntegrableOn (fun y ↦ y ^ (dim E - 1) • f y) (Ioi 0) volume

Tactic:
Integrable.comp_snd_iff (β := Ioi 0) (f := (f <| Subtype.val ·)),

Goal state after:
E : Type u_1
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : MeasurableSpace E
F : Type u_2
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : Nontrivial E
μ : Measure E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : BorelSpace E
inst✝ : μ.IsAddHaarMeasure
f : ℝ → F
this :
  Integrable (fun x ↦ f ‖↑x‖) (Measure.comap Subtype.val μ) ↔
    Integrable (fun x ↦ f ↑x.2) (μ.toSphere.prod (Measure.volumeIoiPow (dim E - 1)))
⊢ Integrable (fun x ↦ f ↑x) (Measure.volumeIoiPow (dim E - 1)) ↔
    IntegrableOn (fun y ↦ y ^ (dim E - 1) • f y) (Ioi 0) volume

E : Type u_1
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : MeasurableSpace E
F : Type u_2
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : Nontrivial E
μ : Measure E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : BorelSpace E
inst✝ : μ.IsAddHaarMeasure
f : ℝ → F
this :
  Integrable (fun x ↦ f ‖↑x‖) (Measure.comap Subtype.val μ) ↔
    Integrable (fun x ↦ f ↑x.2) (μ.toSphere.prod (Measure.volumeIoiPow (dim E - 1)))
⊢ μ.toSphere ≠ 0
Module: Mathlib.Analysis.SpecialFunctions.RegularizedHypergeometric

Goal state before:

Tactic:
-j.re ≤ ⌈-j.re⌉₊ := Nat.le_ceil (-j.re)
      _ ≤ b.toFinset.sup (⌈-re ·⌉₊) := mod_cast Finset.le_sup (by grind) (f := (⌈-re ·⌉₊))
      _ < n := by norm_cast

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

Goal state before:
pp: case h.inr
a b : Multiset ℂ
h : ∀ j ∈ a, ∀ (k : ℕ), j ≠ -↑k
n : ℕ
hn : (b.toFinset.sup fun x ↦ ⌈-x.re⌉₊) + 1 ≤ n
j : ℂ
hj : j ∈ b
m : ℕ
h' : j + ↑n = -↑m
⊢ False

Tactic:
· suffices (m : ℝ) < 0 by grind
    suffices -j.re < n by
      have h : j = -m - n := by grind
      simpa [h] using this
    calc
      -j.re ≤ ⌈-j.re⌉₊ := Nat.le_ceil (-j.re)
      _ ≤ b.toFinset.sup (⌈-re ·⌉₊) := mod_cast Finset.le_sup (by grind) (f := (⌈-re ·⌉₊))
      _ < n := by norm_cast

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

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

Tactic:
· rw [← L.weierstrassPExcept_of_notMem _ L.ω₁_div_two_notMem_lattice,
      ← L.derivWeierstrassPExcept_of_notMem _ L.ω₁_div_two_notMem_lattice,
      L.eqOn_deriv_weierstrassPExcept_derivWeierstrassPExcept (L.ω₁ / 2) (x := x) (by simp [hx])]

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

Goal state before:
pp: n : ℕ
hn : 1 ≤ n
⊢ (2 + 1 / ↑n)⁻¹ = (fun n ↦ ↑n / (2 * ↑n + 1)) n

Tactic:
add_div' (1 : ℝ) 2 n (cast_ne_zero.mpr (one_le_iff_ne_zero.mp hn)),

Goal state after:
n : ℕ
hn : 1 ≤ n
⊢ ((2 * ↑n + 1) / ↑n)⁻¹ = (fun n ↦ ↑n / (2 * ↑n + 1)) n
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
⊢ P.leadingCoeff = 2 ^ (n - 1) ↔ P = T ℝ ↑n

Tactic:
refine ⟨fun hP => ?_, fun hP => by simp [hP]⟩
  apply (coeff_eq_iff_of_forall_abs_le_one hPdeg hPbnd).mp
  suffices hPdeg' : n ≤ P.degree by
    replace hPdeg' : P.degree = n := eq_of_le_of_ge hPdeg hPdeg'
    rwa [leadingCoeff, natDegree_eq_of_degree_eq_some hPdeg'] at hP
  lift P.degree to ℕ with d hd
  · contrapose! hP
    rw [degree_eq_bot.mp hP, leadingCoeff_zero]
    positivity
  replace hP := ge_of_eq hP
  contrapose! hP
  have : d - 1 < n - 1 := by grind [Nat.cast_withBot, WithBot.coe_le_coe, WithBot.coe_lt_coe]
  calc P.leadingCoeff ≤ 2 ^ (d - 1) := leadingCoeff_le_of_forall_abs_le_one (le_of_eq hd.symm) hPbnd
  _ < 2 ^ (n - 1) := by gcongr; norm_num

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

Goal state before:
pp: z : ℍ
x : Fin 2 → ℤ
hx : x ≠ 0
hn0 : ‖x‖ ≠ 0
⊢ ↑(x 0) * ↑z + ↑(x 1) = (↑(x 0) / ↑‖x‖ * ↑z + ↑(x 1) / ↑‖x‖) * ↑‖x‖

Tactic:
rw [div_mul_eq_mul_div, ← add_div, div_mul_cancel₀ _ (mod_cast hn0)]

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

Goal state before:
pp: case hbc
z : ℍ
x : Fin 2 → ℤ
hx : x ≠ 0
hn0 : ‖x‖ ≠ 0
h11 : ↑(x 0) * ↑z + ↑(x 1) = (↑(x 0) / ↑‖x‖ * ↑z + ↑(x 1) / ↑‖x‖) * ↑‖x‖
⊢ r z ≤ ‖↑(x 0) / ↑↑(max (x 0).natAbs (x 1).natAbs) * ↑z + ↑(x 1) / ↑↑(max (x 0).natAbs (x 1).natAbs)‖

Tactic:
· rcases div_max_sq_ge_one x hx with H1 | H2
    · simpa only [norm_eq_max_natAbs, ofReal_div, ofReal_intCast] using auxbound1 z (x 1 / ‖x‖) H1
    · simpa only [norm_eq_max_natAbs, ofReal_div, ofReal_intCast] using auxbound2 z (x 0 / ‖x‖) H2

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

Goal state before:
pp: z : ℍ
x : Fin 2 → ℤ
hx : x ≠ 0
⊢ r z * ‖x‖ ≤ ‖↑(x 0) * ↑z + ↑(x 1)‖

Tactic:
have hn0 : ‖x‖ ≠ 0 := by rwa [norm_ne_zero_iff]
  have h11 : x 0 * (z : ℂ) + x 1 = (x 0 / ‖x‖ * z + x 1 / ‖x‖) * ‖x‖ := by
    rw [div_mul_eq_mul_div, ← add_div, div_mul_cancel₀ _ (mod_cast hn0)]
  rw [norm_eq_max_natAbs, h11, norm_mul, norm_real, norm_norm, norm_eq_max_natAbs]
  gcongr
  · rcases div_max_sq_ge_one x hx with H1 | H2
    · simpa only [norm_eq_max_natAbs, ofReal_div, ofReal_intCast] using auxbound1 z (x 1 / ‖x‖) H1
    · simpa only [norm_eq_max_natAbs, ofReal_div, ofReal_intCast] using auxbound2 z (x 0 / ‖x‖) H2

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

Goal state before:
pp: n k : ℕ
hk : k < n
⊢ rootMultiplicity (cos ((2 * ↑k + 1) * π / (2 * ↑n))) (T ℝ ↑n) = 1

Tactic:
rw [← count_roots, roots_T_real, Multiset.count_eq_one_of_mem (by simp)]

Goal state after:
n k : ℕ
hk : k < n
⊢ cos ((2 * ↑k + 1) * π / (2 * ↑n)) ∈ (Finset.image (fun k ↦ cos ((2 * ↑k + 1) * π / (2 * ↑n))) (Finset.range n)).val
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema

Goal state before:
pp: case h
n : ℕ
⊢ Set.MapsTo (fun k ↦ (↑k + 1) * π / (↑n + 1)) (↑(Finset.range n)) (Set.Icc 0 π)

Tactic:
· refine fun k hk => Set.mem_Icc.mpr ⟨by positivity, ?_⟩
    field_simp
    norm_cast
    grind

Goal state after:
Module: Mathlib.Topology.Algebra.InfiniteSum.TsumUniformlyOn

Goal state before:
pp: case succ
ι : Type u_1
𝕜 : Type u_2
F : Type u_3
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : IsRCLikeNormedField 𝕜
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set 𝕜
f : ι → 𝕜 → F
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hsum : ∀ t ∈ s, Summable fun n ↦ f n t
m : ℕ
hm :
  ∀ {x : 𝕜},
    x ∈ s →
      (∀ (k : ℕ), 1 ≤ k → k ≤ m → SummableLocallyUniformlyOn (fun n ↦ iteratedDerivWithin k (fun z ↦ f n z) s) s) →
        (∀ (n : ι) (k : ℕ) (r : 𝕜), k ≤ m → r ∈ s → DifferentiableAt 𝕜 (iteratedDerivWithin k (fun z ↦ f n z) s) r) →
          iteratedDerivWithin m (fun z ↦ ∑' (n : ι), f n z) s x = ∑' (n : ι), iteratedDerivWithin m (f n) s x
x : 𝕜
hx : x ∈ s
h : ∀ (k : ℕ), 1 ≤ k → k ≤ m + 1 → SummableLocallyUniformlyOn (fun n ↦ iteratedDerivWithin k (fun z ↦ f n z) s) s
hf2 : ∀ (n : ι) (k : ℕ) (r : 𝕜), k ≤ m + 1 → r ∈ s → DifferentiableAt 𝕜 (iteratedDerivWithin k (fun z ↦ f n z) s) r
⊢ iteratedDerivWithin (m + 1) (fun z ↦ ∑' (n : ι), f n z) s x = ∑' (n : ι), iteratedDerivWithin (m + 1) (f n) s x

Tactic:
simp_rw [iteratedDerivWithin_succ]

Goal state after:
case succ
ι : Type u_1
𝕜 : Type u_2
F : Type u_3
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : IsRCLikeNormedField 𝕜
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set 𝕜
f : ι → 𝕜 → F
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hsum : ∀ t ∈ s, Summable fun n ↦ f n t
m : ℕ
hm :
  ∀ {x : 𝕜},
    x ∈ s →
      (∀ (k : ℕ), 1 ≤ k → k ≤ m → SummableLocallyUniformlyOn (fun n ↦ iteratedDerivWithin k (fun z ↦ f n z) s) s) →
        (∀ (n : ι) (k : ℕ) (r : 𝕜), k ≤ m → r ∈ s → DifferentiableAt 𝕜 (iteratedDerivWithin k (fun z ↦ f n z) s) r) →
          iteratedDerivWithin m (fun z ↦ ∑' (n : ι), f n z) s x = ∑' (n : ι), iteratedDerivWithin m (f n) s x
x : 𝕜
hx : x ∈ s
h : ∀ (k : ℕ), 1 ≤ k → k ≤ m + 1 → SummableLocallyUniformlyOn (fun n ↦ iteratedDerivWithin k (fun z ↦ f n z) s) s
hf2 : ∀ (n : ι) (k : ℕ) (r : 𝕜), k ≤ m + 1 → r ∈ s → DifferentiableAt 𝕜 (iteratedDerivWithin k (fun z ↦ f n z) s) r
⊢ derivWithin (iteratedDerivWithin m (fun z ↦ ∑' (n : ι), f n z) s) s x =
    ∑' (n : ι), derivWithin (iteratedDerivWithin m (f n) s) s x
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema

Goal state before:
pp: case refine_1
n k : ℕ
hn : n ≠ 0
hk₁ : k < n
hk₂ : Odd k
k_pos : 0 < k
zero_lt : 0 < ↑k * π / ↑n
lt_pi : ↑k * π / ↑n < π
x : ℝ
hx : x ∈ Set.Ioo (-1) 1
⊢ eval (cos (↑k * π / ↑n)) (T ℝ ↑n) ≤ eval x (T ℝ ↑n)

Tactic:
rw [(eval_T_real_eq_neg_one_iff hn _).mpr ⟨k, le_of_lt hk₁, hk₂, rfl⟩]

Goal state after:
case refine_1
n k : ℕ
hn : n ≠ 0
hk₁ : k < n
hk₂ : Odd k
k_pos : 0 < k
zero_lt : 0 < ↑k * π / ↑n
lt_pi : ↑k * π / ↑n < π
x : ℝ
hx : x ∈ Set.Ioo (-1) 1
⊢ -1 ≤ eval x (T ℝ ↑n)
Module: Mathlib.Analysis.SpecificLimits.ArithmeticGeometric

Goal state before:
pp: R : Type u_1
a b u₀ : R
inst✝⁵ : Field R
inst✝⁴ : LinearOrder R
inst✝³ : IsStrictOrderedRing R
inst✝² : Archimedean R
inst✝¹ : TopologicalSpace R
inst✝ : OrderTopology R
ha_pos : 0 ≤ a
ha : a < 1
| 𝓝 0

Tactic:
← zero_mul (u₀ - (b / (1 - a)))

Goal state after:
R : Type u_1
a b u₀ : R
inst✝⁵ : Field R
inst✝⁴ : LinearOrder R
inst✝³ : IsStrictOrderedRing R
inst✝² : Archimedean R
inst✝¹ : TopologicalSpace R
inst✝ : OrderTopology R
ha_pos : 0 ≤ a
ha : a < 1
| 𝓝 (0 * (u₀ - b / (1 - a)))
Module: Mathlib.Data.Int.Fib.Basic

Goal state before:
pp: case inl
n : ℕ
hn0 : ¬n + n = 0
this : -↑(n + n) + 1 = -↑(n + n - 1)
⊢ (-1) ^ (n + n + 1) * (↑(Nat.fib (n + n)) - ↑(Nat.fib (n + n + 1))) = fib (-↑(n + n) + 1)

Tactic:
rw [Nat.fib_add_one hn0, this, fib_neg_natCast, pow_add, ← two_mul,
            Nat.sub_add_cancel (by grind)]

Goal state after:
case inl
n : ℕ
hn0 : ¬n + n = 0
this : -↑(n + n) + 1 = -↑(n + n - 1)
⊢ (-1) ^ (2 * n) * (-1) ^ 1 * (↑(Nat.fib (2 * n)) - ↑(Nat.fib (2 * n - 1) + Nat.fib (2 * n))) =
    (-1) ^ (2 * n) * ↑(Nat.fib (2 * n - 1))
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent

Goal state before:
pp: k : ℕ
hk : 1 ≤ k
z : ℂ
hz : z ∈ ℍₒ
h0 :
  (-1) ^ k * ↑k ! * ∑' (n : ℤ), (z + ↑n) ^ (-1 - ↑k) + -(-1) ^ k * ↑k ! * z ^ (-1 - ↑k) =
    iteratedDerivWithin k (fun x ↦ ↑π * (↑π * x).cot) ℍₒ z - (-1) ^ k * ↑k ! * z ^ (-1 - ↑k)
⊢ iteratedDerivWithin k (fun x ↦ ↑π * (↑π * x).cot) ℍₒ z = (-1) ^ k * ↑k ! * ∑' (n : ℤ), (z + ↑n) ^ (-1 - ↑k)

Tactic:
rw [← add_left_inj (-(-1) ^ k * k ! * z ^ (-1 - k : ℤ)), h0]

Goal state after:
k : ℕ
hk : 1 ≤ k
z : ℂ
hz : z ∈ ℍₒ
h0 :
  (-1) ^ k * ↑k ! * ∑' (n : ℤ), (z + ↑n) ^ (-1 - ↑k) + -(-1) ^ k * ↑k ! * z ^ (-1 - ↑k) =
    iteratedDerivWithin k (fun x ↦ ↑π * (↑π * x).cot) ℍₒ z - (-1) ^ k * ↑k ! * z ^ (-1 - ↑k)
⊢ iteratedDerivWithin k (fun x ↦ ↑π * (↑π * x).cot) ℍₒ z + -(-1) ^ k * ↑k ! * z ^ (-1 - ↑k) =
    iteratedDerivWithin k (fun x ↦ ↑π * (↑π * x).cot) ℍₒ z - (-1) ^ k * ↑k ! * z ^ (-1 - ↑k)
Module: Mathlib.Analysis.SumIntegralComparisons

Goal state before:
pp: x₀ : ℝ
a : ℕ
f : ℝ → ℝ
hf : AntitoneOn f (Icc x₀ (x₀ + ↑a))
k : ℕ
hk : k + 1 ≤ a
⊢ IntervalIntegrable f volume (x₀ + ↑k) (x₀ + ↑(k + 1))

Tactic:
refine (hf.mono ?_).intervalIntegrable
  rw [uIcc_of_le (by simp)]
  apply Icc_subset_Icc <;> simp [-Nat.cast_add, hk]

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

Goal state before:
pp: case h
c : ℝ
hc : 1 < c
i : ℕ
cpos : 0 < c
hi : i ≠ 0
⊢ 1 ≤ c ^ i * c⁻¹

Tactic:
simpa only [← div_eq_mul_inv, one_le_div cpos, pow_one] using le_self_pow₀ hc.le hi

Goal state after:
Module: Mathlib.CategoryTheory.Comma.Final

Goal state before:
pp: A : Type u₁
inst✝⁵ : Category.{v₁, u₁} A
B : Type u₂
inst✝⁴ : Category.{v₂, u₂} B
T : Type u₃
inst✝³ : Category.{v₃, u₃} T
L : A ⥤ T
R : B ⥤ T
inst✝² : IsCofiltered A
inst✝¹ : IsCofiltered B
inst✝ : ∀ (b : B), IsCofiltered (CostructuredArrow L (R.obj b))
⊢ Nonempty (Comma L R)

Tactic:
obtain ⟨b⟩ := IsCofiltered.nonempty (C := B)
    obtain ⟨X⟩ : Nonempty (CostructuredArrow L (R.obj b)) := IsCofiltered.nonempty
    exact ⟨⟨X.left, b, X.hom⟩⟩

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Indization.FilteredColimits

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
I : Type v
inst✝¹ : SmallCategory I
F : I ⥤ Cᵒᵖ ⥤ Type v
inst✝ : IsFiltered I
hF : ∀ (i : I), IsIndObject (F.obj i)
J : Type v
x✝¹ : SmallCategory J
x✝ : FinCategory J
G : J ⥤ CostructuredArrow yoneda (colimit F)
h₁ : Nonempty (limit (G.op ⋙ (CostructuredArrow.toOver yoneda (colimit F)).op ⋙ yoneda.obj (Over.mk (𝟙 (colimit F)))))
i : I
hi :
  Nonempty
    (limit
      ((G.op ⋙ (CostructuredArrow.toOver yoneda (colimit F)).op) ⋙
        yoneda.obj ((colimit.toCostructuredArrow F ⋙ CostructuredArrow.toOver F (colimit F)).obj i)))
P : IndObjectPresentation (F.obj i)
hc : IsColimit ((Over.map (colimit.ι F i)).mapCocone P.cocone.toOver) :=
  isColimitOfPreserves (Over.map (colimit.ι F i)) (Over.isColimitToOver P.coconeIsColimit)
⊢ ∃ X, Nonempty (limit (G.op ⋙ yoneda.obj X))

Tactic:
obtain ⟨k, hk⟩ : ∃ k, Nonempty (limit (G.op ⋙ (CostructuredArrow.toOver yoneda (colimit F)).op ⋙
      yoneda.obj ((CostructuredArrow.toOver yoneda (colimit F)).obj <|
        (CostructuredArrow.pre P.F yoneda (colimit F)).obj <|
          (map (colimit.ι F i)).obj <| mk _))) :=
    exists_nonempty_limit_obj_of_isColimit F G _ hc _ (Iso.refl _) hi

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
I : Type v
inst✝¹ : SmallCategory I
F : I ⥤ Cᵒᵖ ⥤ Type v
inst✝ : IsFiltered I
hF : ∀ (i : I), IsIndObject (F.obj i)
J : Type v
x✝¹ : SmallCategory J
x✝ : FinCategory J
G : J ⥤ CostructuredArrow yoneda (colimit F)
h₁ : Nonempty (limit (G.op ⋙ (CostructuredArrow.toOver yoneda (colimit F)).op ⋙ yoneda.obj (Over.mk (𝟙 (colimit F)))))
i : I
hi :
  Nonempty
    (limit
      ((G.op ⋙ (CostructuredArrow.toOver yoneda (colimit F)).op) ⋙
        yoneda.obj ((colimit.toCostructuredArrow F ⋙ CostructuredArrow.toOver F (colimit F)).obj i)))
P : IndObjectPresentation (F.obj i)
hc : IsColimit ((Over.map (colimit.ι F i)).mapCocone P.cocone.toOver) :=
  isColimitOfPreserves (Over.map (colimit.ι F i)) (Over.isColimitToOver P.coconeIsColimit)
k : P.I
hk :
  Nonempty
    (limit
      (G.op ⋙
        (CostructuredArrow.toOver yoneda (colimit F)).op ⋙
          yoneda.obj
            ((CostructuredArrow.toOver yoneda (colimit F)).obj
              ((pre P.F yoneda (colimit F)).obj
                ((CostructuredArrow.map (colimit.ι F i)).obj
                  (CostructuredArrow.mk (P.cocone.toCostructuredArrow.obj k).hom))))))
⊢ ∃ X, Nonempty (limit (G.op ⋙ yoneda.obj X))
Module: Mathlib.CategoryTheory.Comma.Final

Goal state before:
pp: A : Type u₁
inst✝¹⁰ : Category.{v₁, u₁} A
B : Type u₂
inst✝⁹ : Category.{v₂, u₂} B
T : Type u₃
inst✝⁸ : Category.{v₃, u₃} T
L : A ⥤ T
R : B ⥤ T
A' : Type u₄
inst✝⁷ : Category.{v₄, u₄} A'
B' : Type u₅
inst✝⁶ : Category.{v₅, u₅} B'
T' : Type u₆
inst✝⁵ : Category.{v₆, u₆} T'
L' : A' ⥤ T'
R' : B' ⥤ T'
F : A ⥤ A'
G : B ⥤ B'
H : T ⥤ T'
iL : F ⋙ L' ≅ L ⋙ H
iR : G ⋙ R' ≅ R ⋙ H
inst✝⁴ : IsFiltered B
inst✝³ : R.Final
inst✝² : R'.Final
inst✝¹ : F.Final
inst✝ : G.Final
x✝ : Comma L' R'
i₂ : A'
j₂ : B'
u₂ : L'.obj i₂ ⟶ R'.obj j₂
this : (R ⋙ H).Final
⊢ StructuredArrow.map₂ u₂ iR.hom =
    StructuredArrow.map₂ ((𝟙 (L'.obj i₂) ≫ (𝟭 T').map u₂) ≫ (𝟭 T' ⋙ 𝟭 T').map (𝟙 (R'.obj j₂)))
      ((G.associator R' (𝟭 T' ⋙ 𝟭 T')).inv ≫
        whiskerRight (𝟙 (G ⋙ R')) (𝟭 T' ⋙ 𝟭 T') ≫
          ((𝟭 B).associator (G ⋙ R') (𝟭 T' ⋙ 𝟭 T')).hom ≫
            (𝟭 B).whiskerLeft
                (((G ⋙ R').associator (𝟭 T') (𝟭 T')).inv ≫
                  whiskerRight iR.hom (𝟭 T') ≫
                    ((𝟭 B).associator (R ⋙ H) (𝟭 T')).hom ≫
                      (𝟭 B).whiskerLeft (𝟙 (R ⋙ H)) ≫ ((𝟭 B).associator R H).inv) ≫
              ((𝟭 B).associator (𝟭 B ⋙ R) H).inv)

Tactic:
by
      congr
      · simp
      · ext; simp

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
⊢ (functor C).Faithful

Tactic:
rw [functor]
  have : (F C).Faithful := by rw [F]; infer_instance
  have : (G C).Faithful := by rw [G]; infer_instance
  have : (H C).Faithful := IsGrothendieckAbelian.OppositeModuleEmbedding.faithful_embedding _
  infer_instance

Goal state after: