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

Goal state before:
pp: case h.refine_2
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
x : A
xpos : IsStrictlyPositive x
y : A
ypos : IsStrictlyPositive y
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
z : A := (conjSqrt x⁻¹ʳ) y
zpos : IsStrictlyPositive z
xinvpos : IsStrictlyPositive x⁻¹ʳ
hsp : IsStrictlyPositive (a • 1 + b • z)
h₁ : (a • 1 + b • z) ^ (-1) = cfc (fun r ↦ (a + b * r) ^ (-1)) z
h₂ : a • 1 + b • z ^ (-1) = cfc (fun r ↦ a + b * r ^ (-1)) z
⊢ ContinuousOn (fun r ↦ a + b * r ^ (-1)) (spectrum ℝ z)

pp: case h.refine_3
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
x : A
xpos : IsStrictlyPositive x
y : A
ypos : IsStrictlyPositive y
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
z : A := (conjSqrt x⁻¹ʳ) y
zpos : IsStrictlyPositive z
xinvpos : IsStrictlyPositive x⁻¹ʳ
hsp : IsStrictlyPositive (a • 1 + b • z)
h₁ : (a • 1 + b • z) ^ (-1) = cfc (fun r ↦ (a + b * r) ^ (-1)) z
h₂ : a • 1 + b • z ^ (-1) = cfc (fun r ↦ a + b * r ^ (-1)) z
⊢ ∀ x ∈ spectrum ℝ z, (a + b * x) ^ (-1) ≤ a + b * x ^ (-1)

Tactic:
· refine ContinuousOn.const_add (ContinuousOn.const_mul ?_ _) _
          exact ContinuousOn.rpow_const (by fun_prop) (by
            #adaptation_note /-- Before nightly-2026-06-04, this was just `grind. -/
            intro x h
            have := IsStrictlyPositive.spectrum_pos (𝕜 := ℝ) zpos h
            grind)

Goal state after:
case h.refine_3
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
x : A
xpos : IsStrictlyPositive x
y : A
ypos : IsStrictlyPositive y
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
z : A := (conjSqrt x⁻¹ʳ) y
zpos : IsStrictlyPositive z
xinvpos : IsStrictlyPositive x⁻¹ʳ
hsp : IsStrictlyPositive (a • 1 + b • z)
h₁ : (a • 1 + b • z) ^ (-1) = cfc (fun r ↦ (a + b * r) ^ (-1)) z
h₂ : a • 1 + b • z ^ (-1) = cfc (fun r ↦ a + b * r ^ (-1)) z
⊢ ∀ x ∈ spectrum ℝ z, (a + b * x) ^ (-1) ≤ a + b * x ^ (-1)
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.RingInverseOrder

Goal state before:
pp: case h.refine_3
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
x : A
xpos : IsStrictlyPositive x
y : A
ypos : IsStrictlyPositive y
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
z : A := (conjSqrt x⁻¹ʳ) y
zpos : IsStrictlyPositive z
xinvpos : IsStrictlyPositive x⁻¹ʳ
hsp : IsStrictlyPositive (a • 1 + b • z)
h₁ : (a • 1 + b • z) ^ (-1) = cfc (fun r ↦ (a + b * r) ^ (-1)) z
h₂ : a • 1 + b • z ^ (-1) = cfc (fun r ↦ a + b * r ^ (-1)) z
⊢ ∀ x ∈ spectrum ℝ z, (a + b * x) ^ (-1) ≤ a + b * x ^ (-1)

Tactic:
· intro r hr
          suffices (a • 1 + b • r) ^ (-1 : ℤ) ≤ a • 1 ^ (-1 : ℤ) + b • r ^ (-1 : ℤ) by
            simp_rw [← Real.rpow_intCast] at this
            simpa using this
          have : ConvexOn ℝ (Set.Ioi 0) (fun z : ℝ => z ^ (-1 : ℤ)) := convexOn_zpow (-1)
          grind [ConvexOn, IsStrictlyPositive.spectrum_pos]

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

Goal state before:
pp: p t : ℝ
hp : p ≠ 1
ht : 0 < t
x : ℝ
⊢ t ^ p * t⁻¹ - t ^ p * (t + x)⁻¹ = t ^ (p - 1) - t ^ p * (t + x)⁻¹

Tactic:
← rpow_neg_one,

Goal state after:
p t : ℝ
hp : p ≠ 1
ht : 0 < t
x : ℝ
⊢ t ^ p * t ^ (-1) - t ^ p * (t + x)⁻¹ = t ^ (p - 1) - t ^ p * (t + x)⁻¹
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation

Goal state before:
pp: p t x : ℝ
hp : 0 < p
ht : 0 ≤ t
hx : 0 ≤ x
⊢ 0 ≤ p.rpowIntegrand₀₁ t x

Tactic:
unfold rpowIntegrand₀₁
  cases eq_or_lt_of_le' ht with
  | inl ht_zero => simp [ht_zero, Real.zero_rpow (ne_of_gt hp)]
  | inr ht_pos =>
    refine mul_nonneg (by positivity) ?_
    rw [sub_nonneg]
    gcongr
    linarith

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

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

Tactic:
simp only [rpowIntegrand₀₁, hx_zero, add_zero, sub_self, mul_zero]
    positivity

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

Goal state before:
pp: case refine_2
p : ℝ
hp : p ∈ Ioo 0 1
⊢ Ioi 1 ≤ᵐ[volume] Ioi 0

Tactic:
exact .of_forall <| Set.Ioi_subset_Ioi zero_le_one

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

Goal state before:
pp: p x : ℝ
hp : p ∈ Ioo 0 1
hx : 0 ≤ x
h✝ : 0 < x
this : ∫ (t : ℝ) in Ioi 0, p.rpowIntegrand₀₁ t 1 ≠ 0
⊢ x ^ p = (∫ (t : ℝ) in Ioi 0, p.rpowIntegrand₀₁ t 1)⁻¹ * ∫ (t : ℝ) in Ioi 0, p.rpowIntegrand₀₁ t x

Tactic:
rw [integral_rpowIntegrand₀₁_eq_rpow_mul_const hp hx, mul_comm, mul_assoc, mul_inv_cancel₀
      this, mul_one]

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

Goal state before:
pp: case succ
n✝ : ℕ
f : ℝ → ℝ := log ∘ Gamma
hc : ConvexOn ℝ (Ioi 0) f
h_rec : ∀ (x : ℝ), 0 < x → f (x + 1) = f x + log x
hder : ∀ {x : ℝ}, 0 < x → DifferentiableAt ℝ f x
hder_rec : ∀ (x : ℝ), 0 < x → deriv f (x + 1) = deriv f x + 1 / x
n : ℕ
hn : deriv f (↑n + 1) = deriv f 1 + ↑(harmonic n)
⊢ deriv f (↑(n + 1) + 1) = deriv f 1 + ↑(harmonic (n + 1))

Tactic:
rw [cast_succ, hder_rec (n + 1) (by positivity), hn, harmonic_succ]
      push_cast
      ring

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
p t : ℝ
hp : p ∈ Ioo 0 1
ht : 0 < t
a : A
ha : 0 ≤ a
hspec : quasispectrum ℝ a ⊆ Ici 0
h_mapsTo : MapsTo (fun x ↦ t⁻¹ • x) (Ici 0) (Ici 0)
⊢ ContinuousOn (fun x ↦ p.rpowIntegrand₀₁ 1 (t⁻¹ • x)) (Ici 0)

Tactic:
have := continuousOn_rpowIntegrand₀₁_Ici hp zero_lt_one

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
p t : ℝ
hp : p ∈ Ioo 0 1
ht : 0 < t
a : A
ha : 0 ≤ a
hspec : quasispectrum ℝ a ⊆ Ici 0
h_mapsTo : MapsTo (fun x ↦ t⁻¹ • x) (Ici 0) (Ici 0)
this : ContinuousOn (p.rpowIntegrand₀₁ 1) (Ici 0)
⊢ ContinuousOn (fun x ↦ p.rpowIntegrand₀₁ 1 (t⁻¹ • x)) (Ici 0)
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:
refine rpowIntegrand₀₁_monotoneOn hp (le_of_lt ht) hz' 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
⊢ z ≤ maxr
Module: Mathlib.Analysis.SpecialFunctions.Log.Base

Goal state before:
pp: x✝ : ℝ
⊢ logb 0 x✝ = 0 x✝

Tactic:
logb_zero_left,

Goal state after:
x✝ : ℝ
⊢ 0 = 0 x✝
Module: Mathlib.Analysis.SpecialFunctions.Log.Base

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

Tactic:
logb_neg_iff_of_base_lt_one b_pos b_lt_one hx,

Goal state after:
b x : ℝ
b_pos : 0 < b
b_lt_one : b < 1
hx : 0 < x
⊢ ¬1 < x ↔ x ≤ 1
Module: Mathlib.MeasureTheory.Measure.RegularityCompacts

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
p q : Set α → Prop
hpq : ∀ (A B : Set α), p A → q B → p (A ∩ B)
hμ : ∀ (ε : ℝ≥0∞), 0 < ε → ∃ K, p K ∧ μ Kᶜ < ε
A : Set α
hA : q A
r : ℝ≥0∞
hr : r < μ A
K' : Set α
hpK' : p K'
hK'_lt : μ K'ᶜ < μ A - r
⊢ μ (A \ (K' ∩ A)) < μ A - r

Tactic:
· refine (measure_mono fun x ↦ ?_).trans_lt hK'_lt
      simp only [sdiff_inter_self_eq_sdiff, mem_sdiff, mem_compl_iff, and_imp, imp_self,
        imp_true_iff]

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

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
f : α → ℝ
f_nn : 0 ≤ᵐ[μ] f
f_mble : AEMeasurable f μ
p : ℝ
p_pos : 0 < p
one_lt_p : -1 < p - 1
g : ℝ → ℝ := fun t ↦ t ^ (p - 1)
obs : ∀ (x : ℝ), intervalIntegral g 0 x volume = x ^ p / p
⊢ ∀ᵐ (t : ℝ) ∂volume.restrict (Ioi 0), 0 ≤ g t

Tactic:
filter_upwards [self_mem_ae_restrict (measurableSet_Ioi : MeasurableSet (Ioi (0 : ℝ)))]

Goal state after:
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
f : α → ℝ
f_nn : 0 ≤ᵐ[μ] f
f_mble : AEMeasurable f μ
p : ℝ
p_pos : 0 < p
one_lt_p : -1 < p - 1
g : ℝ → ℝ := fun t ↦ t ^ (p - 1)
obs : ∀ (x : ℝ), intervalIntegral g 0 x volume = x ^ p / p
⊢ ∀ a ∈ Ioi 0, 0 ≤ g a
Module: Mathlib.MeasureTheory.Constructions.HaarToSphere

Goal state before:
pp: n : ℕ
x : ↑(Ioi 0)
⊢ (volumeIoiPow n) (Iio x) = ENNReal.ofReal (↑x ^ (n + 1) / (↑n + 1))

Tactic:
by
  have hr₀ : 0 ≤ x.1 := le_of_lt x.2
  rw [volumeIoiPow, withDensity_apply _ measurableSet_Iio,
    setLIntegral_subtype measurableSet_Ioi _ fun a : ℝ ↦ .ofReal (a ^ n),
    image_subtype_val_Ioi_Iio, restrict_congr_set Ioo_ae_eq_Ioc,
    ← ofReal_integral_eq_lintegral_ofReal (intervalIntegrable_pow _).1, ← integral_of_le hr₀]
  · simp
  · filter_upwards [ae_restrict_mem measurableSet_Ioc] with y hy
    exact pow_nonneg hy.1.le _

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
a✝ : Nontrivial E
s : Set ↑(sphere 0 1)
hs : s ∈ {s | MeasurableSet s}
r : ↑(Ioi 0)
⊢ (map (⇑(homeomorphUnitSphereProd E)) (comap Subtype.val μ)) (s ×ˢ Iio r) =
    μ.toSphere s * (volumeIoiPow (dim E - 1)) (Iio r)

Tactic:
have : Ioo (0 : ℝ) r = r.1 • Ioo (0 : ℝ) 1 := by simp [LinearOrderedField.smul_Ioo r.2.out]

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
a✝ : Nontrivial E
s : Set ↑(sphere 0 1)
hs : s ∈ {s | MeasurableSet s}
r : ↑(Ioi 0)
this : Ioo 0 ↑r = ↑r • Ioo 0 1
⊢ (map (⇑(homeomorphUnitSphereProd E)) (comap Subtype.val μ)) (s ×ˢ Iio r) =
    μ.toSphere s * (volumeIoiPow (dim E - 1)) (Iio r)
Module: Mathlib.Analysis.SpecialFunctions.Pow.Integral

Goal state before:
pp: E : Type u_2
F : Type u_3
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : FiniteDimensional ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : NormedAddCommGroup F
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
hd : 1 ≤ Module.finrank ℝ E
f : E → F
C α r : ℝ
hα : α < ↑(Module.finrank ℝ E)
h_decay : ∀ᵐ (x : E) ∂μ.restrict (ball 0 r), ‖f x‖ ≤ C * ‖x‖ ^ (-α)
h_meas : AEStronglyMeasurable f μ
this : Nontrivial E
h_rpow : IntegrableOn (fun y ↦ y ^ (↑(Module.finrank ℝ E) - 1 - α)) (Ioo 0 r) volume
y : ℝ
hy : 0 < y
right✝ : y < r
⊢ y ^ (↑(Module.finrank ℝ E) - 1 - α) * C = y ^ ↑(Module.finrank ℝ E - 1) * y ^ (-α) * C

Tactic:
← Real.rpow_add hy

Goal state after:
E : Type u_2
F : Type u_3
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : FiniteDimensional ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : NormedAddCommGroup F
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
hd : 1 ≤ Module.finrank ℝ E
f : E → F
C α r : ℝ
hα : α < ↑(Module.finrank ℝ E)
h_decay : ∀ᵐ (x : E) ∂μ.restrict (ball 0 r), ‖f x‖ ≤ C * ‖x‖ ^ (-α)
h_meas : AEStronglyMeasurable f μ
this : Nontrivial E
h_rpow : IntegrableOn (fun y ↦ y ^ (↑(Module.finrank ℝ E) - 1 - α)) (Ioo 0 r) volume
y : ℝ
hy : 0 < y
right✝ : y < r
⊢ y ^ (↑(Module.finrank ℝ E) - 1 - α) * C = y ^ (↑(Module.finrank ℝ E - 1) + -α) * C
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
r : ℝ
⊢ ((ball 0 r).indicator fun x ↦ f ‖x‖) =ᵐ[μ] fun x ↦ (Iio r).indicator f ‖x‖

Tactic:
filter_upwards with x

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
r : ℝ
x : E
⊢ (ball 0 r).indicator (fun x ↦ f ‖x‖) x = (Iio r).indicator f ‖x‖
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: L : PeriodPair
l₀ : ℂ
hl : l₀ ∉ L.lattice
⊢ (fun z ↦ ∑' (l : ↥L.lattice), if ↑l = l₀ then 0 else -2 / (z - ↑l) ^ 3) = fun z ↦
    -∑' (l : ↥L.lattice), 2 / (z - ↑l) ^ 3

Tactic:
simp_rw [← tsum_neg]

Goal state after:
L : PeriodPair
l₀ : ℂ
hl : l₀ ∉ L.lattice
⊢ (fun z ↦ ∑' (l : ↥L.lattice), if ↑l = l₀ then 0 else -2 / (z - ↑l) ^ 3) = fun z ↦
    ∑' (b : ↥L.lattice), -(2 / (z - ↑b) ^ 3)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.InverseDeriv

Goal state before:
pp: case inr.inl
x : ℝ
h₁✝ : x ≠ -1
h₂✝ : x ≠ 1
h₁ : -1 < x
h₂ : x < 1
this : 0 < cos (arcsin x)
⊢ HasStrictDerivAt arcsin (cos (arcsin x))⁻¹ x ∧ ContDiffAt ℝ ω arcsin x

Tactic:
exact ⟨sinPartialHomeomorph.hasStrictDerivAt_symm ⟨h₁, h₂⟩ this.ne' (hasStrictDerivAt_sin _),
      sinPartialHomeomorph.contDiffAt_symm_deriv this.ne' ⟨h₁, h₂⟩ (hasDerivAt_sin _)
        contDiff_sin.contDiffAt⟩

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

Goal state before:
pp: ⊢ IntervalIntegrable (fun x ↦ √(1 - x ^ 2)⁻¹) volume (-1) 1

Tactic:
by
  rw [intervalIntegrable_iff]
  refine integrableOn_deriv_of_nonneg continuous_arccos.neg.continuousOn (fun x hx ↦ ?_) (by simp)
  simpa using! (hasDerivAt_arccos (by aesop) (by aesop)).neg

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

Goal state before:
pp: n : ℕ
c : ℕ → ℝ
hcnonneg : ∀ i ≤ n, 0 ≤ (-1) ^ i * c i
P : ℝ[X]
hPbnd : ∀ x ∈ Set.Icc (-1) 1, |eval x P| ≤ 1
i : ℕ
hi : i ∈ Finset.Iic n
⊢ (-1) ^ i * eval (node n i) P * ((-1) ^ i * c i) ≤ 1 * ((-1) ^ i * c i)

Tactic:
gcongr
      · exact (hcnonneg i (Finset.mem_Iic.mp hi))
      · exact (negOnePow_mul_le (hPbnd _ node_mem_Icc))

Goal state after:
Module: Mathlib.NumberTheory.Niven

Goal state before:
pp: r : ℚ
hcos : ∃ q, cos (↑r * π) = ↑q
h_bnd : r ∈ Set.Icc 0 1
⊢ r • π ∈ (fun x ↦ x • π) '' {0, 1 / 3, 1 / 2, 2 / 3, 1}

Tactic:
replace h_bnd : (r : ℝ) * π ∈ Set.Icc (0 * π) (1 * π) := by
    obtain ⟨hr, hr'⟩ := h_bnd; constructor <;> gcongr <;> norm_cast

Goal state after:
r : ℚ
hcos : ∃ q, cos (↑r * π) = ↑q
h_bnd : ↑r * π ∈ Set.Icc (0 * π) (1 * π)
⊢ r • π ∈ (fun x ↦ x • π) '' {0, 1 / 3, 1 / 2, 2 / 3, 1}
Module: Mathlib.Order.Interval.Finset.Box

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹⁰ : Ring α
inst✝⁹ : PartialOrder α
inst✝⁸ : IsOrderedRing α
inst✝⁷ : Ring β
inst✝⁶ : PartialOrder β
inst✝⁵ : IsOrderedRing β
inst✝⁴ : LocallyFiniteOrder α
inst✝³ : LocallyFiniteOrder β
inst✝² : DecidableEq α
inst✝¹ : DecidableEq β
inst✝ : DecidableLE (α × β)
n : ℕ
⊢ #(Icc (-1 + -↑n).1 (↑n + 1).1) * #(Icc (-1 + -↑n).2 (↑n + 1).2) - #(Icc (-↑n).1 (↑n).1) * #(Icc (-↑n).2 (↑n).2) =
    #(Icc (-1 + -↑n) (↑n + 1)) * #(Icc (-1 + -↑n) (↑n + 1)) - #(Icc (-↑n) ↑n) * #(Icc (-↑n) ↑n)

Tactic:
fst_add,

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹⁰ : Ring α
inst✝⁹ : PartialOrder α
inst✝⁸ : IsOrderedRing α
inst✝⁷ : Ring β
inst✝⁶ : PartialOrder β
inst✝⁵ : IsOrderedRing β
inst✝⁴ : LocallyFiniteOrder α
inst✝³ : LocallyFiniteOrder β
inst✝² : DecidableEq α
inst✝¹ : DecidableEq β
inst✝ : DecidableLE (α × β)
n : ℕ
⊢ #(Icc ((-1).1 + (-↑n).1) ((↑n).1 + 1.1)) * #(Icc (-1 + -↑n).2 (↑n + 1).2) -
      #(Icc (-↑n).1 (↑n).1) * #(Icc (-↑n).2 (↑n).2) =
    #(Icc (-1 + -↑n) (↑n + 1)) * #(Icc (-1 + -↑n) (↑n + 1)) - #(Icc (-↑n) ↑n) * #(Icc (-↑n) ↑n)
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable

Goal state before:
pp: x y : ℤ
⊢ ‖![x, y]‖ = ‖![y, x]‖

Tactic:
simp [EisensteinSeries.norm_eq_max_natAbs, max_comm]

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

Goal state before:
pp: n : ℤ
x : ℝ
hx : x ≤ -1
⊢ 1 ≤ ↑↑n.negOnePow * eval x (T ℝ n)

Tactic:
by
  rw [← neg_neg x, T_eval_neg]
  convert! one_le_eval_T_real n (le_neg_of_le_neg hx)
  rw [Int.cast_negOnePow, ← mul_assoc, ← mul_zpow]
  simp

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

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

Tactic:
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.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
  by_cases! hk : n < k
  · rw [iterate_derivative_eq_zero_of_degree_lt (by grw [hPdeg]; simpa),
      iterate_derivative_eq_zero_of_degree_lt (by simp [hk])]
  convert!
    sumNodes_le_sumNodes_T (fun i hi => negOnePow_mul_iterateDerivativeC_nonneg hi hx) hPbnd using 1
  · rw [sumNodes_eq_eval_iterate_derivative hk x hPdeg]
  · rw [sumNodes_eq_eval_iterate_derivative hk x (le_of_eq (degree_T ℝ n))]

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

Goal state before:
pp: L : PeriodPair
⊢ iteratedDeriv 6 (L.relation * id ^ 6) 0 = 0

Tactic:
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]
  simp [Finset.sum_range_succ, L.G_eq_zero_of_odd 3 (by decide), g₃,
    show Nat.choose 6 4 = 15 by rfl, show Nat.choose 6 3 = 20 by rfl]
  ring

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

Goal state before:
pp: case neg
ι : 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
r : 𝕜
hr : r ∈ s
hm2 : ¬m = 0
⊢ Summable fun n ↦ iteratedDerivWithin m (fun z ↦ f n z) s r

Tactic:
· exact ((h m (by lia) (by lia)).summable hr).congr (fun _ ↦ by simp)

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

Goal state before:
pp: x : ℂ
hz : x ∈ ℂ_ℤ
⊢ ↑π * (↑π * x).cot - 1 / x = ∑' (n : ℕ), (1 / (x - (↑n + 1)) + 1 / (x + (↑n + 1)))

Tactic:
rw [HasSum.tsum_eq]
  apply (Summable.hasSum_iff_tendsto_nat (summable_cotTerm hz)).mpr
    (tendsto_logDeriv_euler_cot_sub hz)

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

Goal state before:
pp: k d : ℕ
z : ℂ
hz : z ∈ ℂ_ℤ
h2 : (deriv^[k] fun x ↦ (x - (↑d + 1))⁻¹) = fun x ↦ (-1) ^ k * ↑k ! * (x - (↑d + 1)) ^ (-1 - ↑k)
h3 : (deriv^[k] fun x ↦ (x + (↑d + 1))⁻¹) = fun x ↦ (-1) ^ k * ↑k ! * (x + (↑d + 1)) ^ (-1 - ↑k)
⊢ (fun x ↦ (-1) ^ k * ↑k ! * (x - (↑d + 1)) ^ (-1 - ↑k)) z + deriv^[k] (fun z ↦ (z + (↑d + 1))⁻¹) z =
    (-1) ^ k * ↑k ! * ((z + (↑d + 1)) ^ (-1 - ↑k) + (z - (↑d + 1)) ^ (-1 - ↑k))

Tactic:
h3

Goal state after:
k d : ℕ
z : ℂ
hz : z ∈ ℂ_ℤ
h2 : (deriv^[k] fun x ↦ (x - (↑d + 1))⁻¹) = fun x ↦ (-1) ^ k * ↑k ! * (x - (↑d + 1)) ^ (-1 - ↑k)
h3 : (deriv^[k] fun x ↦ (x + (↑d + 1))⁻¹) = fun x ↦ (-1) ^ k * ↑k ! * (x + (↑d + 1)) ^ (-1 - ↑k)
⊢ (fun x ↦ (-1) ^ k * ↑k ! * (x - (↑d + 1)) ^ (-1 - ↑k)) z + (fun x ↦ (-1) ^ k * ↑k ! * (x + (↑d + 1)) ^ (-1 - ↑k)) z =
    (-1) ^ k * ↑k ! * ((z + (↑d + 1)) ^ (-1 - ↑k) + (z - (↑d + 1)) ^ (-1 - ↑k))
Module: Mathlib.Analysis.SumIntegralComparisons

Goal state before:
pp: a b : ℕ
f g : ℝ → ℝ
hab : a ≤ b
h : ∀ i ∈ Ico a b, ∀ x ∈ Ico ↑i ↑(i + 1), f ↑i ≤ g x
hg : IntegrableOn g (Ico ↑a ↑b) volume
A : ∀ i ∈ Finset.Ico a b, IntervalIntegrable g volume ↑i ↑(i + 1)
⊢ ∑ i ∈ Finset.Ico a b, ∫ (x : ℝ) in ↑i..↑(i + 1), g x = ∫ (x : ℝ) in ↑a..↑b, g x

Tactic:
by rw [sum_integral_adjacent_intervals_Ico (a := (↑·)) hab]; grind

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.DiagramLemmas.KernelCokernelComp

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
⊢ ι f g ≫ biprod.fst = kernel.ι (f ≫ g)

Tactic:
by simp [ι]

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.DiagramLemmas.KernelCokernelComp

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
⊢ ι f g ≫ biprod.snd = kernel.ι (f ≫ g) ≫ f

Tactic:
by simp [ι]

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
G : C
inst✝¹ : Projective G
hG : IsSeparator G
X : C
p : G ⟶ X
inst✝ : Epi p
Y : C
cm : ShortComplex C := { X₁ := kernel p, X₂ := G, X₃ := X, f := kernel.ι p, g := p, zero := ⋯ }
exact : cm.Exact
⊢ Mono cm.op.f

Tactic:
dsimp [cm]

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
G : C
inst✝¹ : Projective G
hG : IsSeparator G
X : C
p : G ⟶ X
inst✝ : Epi p
Y : C
cm : ShortComplex C := { X₁ := kernel p, X₂ := G, X₃ := X, f := kernel.ι p, g := p, zero := ⋯ }
exact : cm.Exact
⊢ Mono p.op