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

Goal state before:
pp: case pos
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)
r : ℝ
hr : r ∈ spectrum ℝ z
ha' : a = 0
⊢ 0 < a + b * r

pp: case neg
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)
r : ℝ
hr : r ∈ spectrum ℝ z
ha' : ¬a = 0
⊢ 0 < a + b * r

Tactic:
· have hb' : b = 1 := by grind
      simp only [ha', hb', one_mul, zero_add, gt_iff_lt]
      #adaptation_note /-- Before nightly-2026-06-04, this was just `grind.
      `spectrum_pos` is not activating in `grind` despite the
      ```
      grind_pattern IsStrictlyPositive.spectrum_pos => x ∈ spectrum 𝕜 a, IsStrictlyPositive a
      ```
      rule, because `grind` will not fill in the `𝕜 := ℝ`. -/
      exact zpos.spectrum_pos hr

Goal state after:
case neg
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)
r : ℝ
hr : r ∈ spectrum ℝ z
ha' : ¬a = 0
⊢ 0 < a + b * r
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Deligne

Goal state before:
pp: s : ℂ
hs : s ≠ 0
⊢ (s + 2).Gammaℝ = s.Gammaℝ * s / 2 / ↑π

Tactic:
by
  rw [Gammaℝ_def, Gammaℝ_def, neg_div, add_div, neg_add, div_self two_ne_zero,
    Gamma_add_one _ (div_ne_zero hs two_ne_zero),
    cpow_add _ _ (ofReal_ne_zero.mpr pi_ne_zero), cpow_neg_one]
  field_simp

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

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
L R : E
inst✝ : CompleteSpace E
hf : LocallyIntegrableOn f (Ioi 0) volume
ha : 0 < a
hb : 0 < b
hL : Tendsto f (𝓝[>] 0) (𝓝 L)
hR : Tendsto f atTop (𝓝 R)
g : ℝ → E := fun x ↦ x⁻¹ • (f (a * x) - f (b * x))
hint : IntegrableOn g (Ioi 0) volume
hg : g = fun x ↦ x⁻¹ • (f (a * x) - f (b * x))
ε : ℝ
hε : ε > 0
δ : ℝ
hδ_pos : δ > 0
hδ :
  ball 0 δ ∩ Ioi 0 ⊆
    {x | ∀ᶠ (y : ℝ) in atTop, dist (intervalIntegral g (x, y).1 (x, y).2 volume) (log (b / a) • (L - R)) < ε / 2}
⊢ ∃ δ > 0, ∀ ⦃x : ℝ⦄, x ∈ Ioi 0 → dist x 0 < δ → dist (∫ (x : ℝ) in Ioi x, g x ∂volume) (log (b / a) • (L - R)) < ε

Tactic:
simp_rw [subset_def, mem_inter_iff, mem_ball] at hδ

Goal state after:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
L R : E
inst✝ : CompleteSpace E
hf : LocallyIntegrableOn f (Ioi 0) volume
ha : 0 < a
hb : 0 < b
hL : Tendsto f (𝓝[>] 0) (𝓝 L)
hR : Tendsto f atTop (𝓝 R)
g : ℝ → E := fun x ↦ x⁻¹ • (f (a * x) - f (b * x))
hint : IntegrableOn g (Ioi 0) volume
hg : g = fun x ↦ x⁻¹ • (f (a * x) - f (b * x))
ε : ℝ
hε : ε > 0
δ : ℝ
hδ_pos : δ > 0
hδ :
  ∀ (x : ℝ),
    dist x 0 < δ ∧ x ∈ Ioi 0 →
      x ∈ {x | ∀ᶠ (y : ℝ) in atTop, dist (intervalIntegral g x y volume) (log (b / a) • (L - R)) < ε / 2}
⊢ ∃ δ > 0, ∀ ⦃x : ℝ⦄, x ∈ Ioi 0 → dist x 0 < δ → dist (∫ (x : ℝ) in Ioi x, g x ∂volume) (log (b / a) • (L - R)) < ε
Module: Mathlib.NumberTheory.Harmonic.EulerMascheroni

Goal state before:
pp: n : ℕ
⊢ eulerMascheroniSeq n < eulerMascheroniSeq (n + 1)

Tactic:
rw [eulerMascheroniSeq, eulerMascheroniSeq, ← sub_pos, sub_sub_sub_comm,
    harmonic_succ, add_comm, Rat.cast_add, add_sub_cancel_right,
    ← log_div (by positivity) (by positivity), add_div, Nat.cast_add_one,
    Nat.cast_add_one, div_self (by positivity), sub_pos, one_div, Rat.cast_inv, Rat.cast_add,
    Rat.cast_one, Rat.cast_natCast]

Goal state after:
n : ℕ
⊢ log (1 + (↑n + 1)⁻¹) < (↑n + 1)⁻¹
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation

Goal state before:
pp: p t : ℝ
ht : 0 < t
x : ℝ
hx : x ∈ Ici 0
⊢ t ^ (p - 1) * (1 - (1 + x * t⁻¹)⁻¹) = (fun x ↦ t ^ (p - 1) * p.rpowIntegrand₀₁ 1 (t⁻¹ • x)) x

Tactic:
by simp [mul_comm, smul_eq_mul, rpowIntegrand₀₁]

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

Goal state before:
pp: case ae_le
p x : ℝ
hp : p ∈ Ioo 0 1
hx : 0 ≤ x
⊢ ∀ᵐ (a : ℝ) ∂volume.restrict (Ioo 0 1), ‖p.rpowIntegrand₀₁ a x‖ ≤ a ^ (p - 1)

Tactic:
case ae_le =>
      refine ae_restrict_of_forall_mem measurableSet_Ioo fun t ht => ?_
      rw [Real.norm_of_nonneg (rpowIntegrand₀₁_nonneg hp.1 (le_of_lt ht.1) hx)]
      exact rpowIntegrand₀₁_le_rpow_sub_one hp (le_of_lt ht.1) hx

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

Goal state before:
pp: case meas
p x : ℝ
hp : p ∈ Ioo 0 1
hx : 0 ≤ x
⊢ AEStronglyMeasurable (fun x_1 ↦ p.rpowIntegrand₀₁ x_1 x) (volume.restrict (Ioi 1))

pp: case finite
p x : ℝ
hp : p ∈ Ioo 0 1
hx : 0 ≤ x
⊢ HasFiniteIntegral (fun x_1 ↦ p.rpowIntegrand₀₁ x_1 x) (volume.restrict (Ioi 1))

Tactic:
case meas =>
    refine ContinuousOn.aestronglyMeasurable ?_ measurableSet_Ioi
    exact continuousOn_rpowIntegrand₀₁ hp hx |>.mono (Set.Ioi_subset_Ioi zero_le_one)

Goal state after:
case finite
p x : ℝ
hp : p ∈ Ioo 0 1
hx : 0 ≤ x
⊢ HasFiniteIntegral (fun x_1 ↦ p.rpowIntegrand₀₁ x_1 x) (volume.restrict (Ioi 1))
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:
rw [← Ne, ← sub_ne_zero] at h

Goal state after:
case neg
s : ℂ
hs : ∀ (n : ℕ), s ≠ -↑n
h : s - 1 ≠ 0
⊢ (2 - s).Gammaℝ⁻¹ = s.Gammaℂ * sin (↑π * s / 2) * (s + 1).Gammaℝ⁻¹
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 : ℕ
r : R
hr✝ : r ≤ 1
hr : r < 1
⊢ log b r = -↑(Nat.clog b ⌈r⁻¹⌉₊)

Tactic:
exact if_neg hr.not_ge

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

Goal state before:
pp: f : ℂ → ℂ := fun s ↦ ↑π ^ (-s / 2)
g : ℂ → ℂ := fun s ↦ Gamma (s / 2)
aux : ↑π ^ (1 / 2) = ↑√π
aux2 : ↑√π ≠ 0
hf : HasDerivAt f (-log ↑π / 2 / ↑√π) 1
⊢ HasDerivAt Gammaℝ (-(↑γ + log (4 * ↑π)) / 2) 1

Tactic:
have hg : HasDerivAt g (-√π * (γ + 2 * log 2) / 2) 1 := by
    have := hasDerivAt_Gamma_one_half.comp 1 (?_ : HasDerivAt (fun s : ℂ ↦ s / 2) (1 / 2) 1)
    · rwa [mul_one_div] at this
    · exact (hasDerivAt_id _).div_const _

Goal state after:
f : ℂ → ℂ := fun s ↦ ↑π ^ (-s / 2)
g : ℂ → ℂ := fun s ↦ Gamma (s / 2)
aux : ↑π ^ (1 / 2) = ↑√π
aux2 : ↑√π ≠ 0
hf : HasDerivAt f (-log ↑π / 2 / ↑√π) 1
hg : HasDerivAt g (-↑√π * (↑γ + 2 * log 2) / 2) 1
⊢ HasDerivAt Gammaℝ (-(↑γ + log (4 * ↑π)) / 2) 1
Module: Mathlib.Data.Int.Log

Goal state before:
pp: case inl.inl
R : Type u_1
inst✝³ : Semifield R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorSemiring R
b : ℕ
r₁ r₂ : R
h₀ : 0 < r₁
h : r₁ ≤ r₂
h₁ : r₁ ≤ 1
h₂ : r₂ ≤ 1
⊢ log b r₁ ≤ log b r₂

Tactic:
have h₀' : 0 < r₂ := lt_of_lt_of_le h₀ h

Goal state after:
case inl.inl
R : Type u_1
inst✝³ : Semifield R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorSemiring R
b : ℕ
r₁ r₂ : R
h₀ : 0 < r₁
h : r₁ ≤ r₂
h₁ : r₁ ≤ 1
h₂ : r₂ ≤ 1
h₀' : 0 < r₂
⊢ log b r₁ ≤ log b r₂
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 1 2
⊢ ∃ μ,
    ∀ a ∈ Ici 0,
      IntegrableOn (fun t ↦ cfcₙ ((↑p).rpowIntegrand₁₂ t) a) (Ioi 0) μ ∧
        a ^ p = ∫ (t : ℝ) in Ioi 0, cfcₙ ((↑p).rpowIntegrand₁₂ t) a ∂μ

Tactic:
obtain ⟨μ, hμ⟩ := exists_measure_rpow_eq_integral_rpowIntegrand₁₂ hp
  refine ⟨μ, fun a (ha : 0 ≤ a) => ?_⟩
  have hpcoe : (p : ℝ) ∈ Ioo 1 2 := by exact_mod_cast hp
  let f t := rpowIntegrand₁₂ p t
  let maxr := sSup (quasispectrum ℝ a)
  have maxr_nonneg : 0 ≤ maxr :=
    le_csSup_of_le (b := 0) (IsCompact.bddAbove (quasispectrum.isCompact _)) (by simp) le_rfl
  let bound (t : ℝ) := ‖f t maxr‖
  have hf : ContinuousOn (Function.uncurry f) (Ioi (0 : ℝ) ×ˢ quasispectrum ℝ a) :=
    continuousOn_rpowIntegrand₁₂_uncurry hpcoe.1 (quasispectrum ℝ a) (by grind)
  have hbound : ∀ᵐ t ∂μ.restrict (Ioi 0), ∀ z ∈ quasispectrum ℝ a, ‖f t z‖ ≤ bound t := by
    filter_upwards [ae_restrict_mem measurableSet_Ioi] with t ht
    intro z hz
    have hz' : 0 ≤ z := by grind
    unfold bound f
    rw [Real.norm_of_nonneg (rpowIntegrand₁₂_nonneg (by grind) (by grind) hz'),
        Real.norm_of_nonneg (rpowIntegrand₁₂_nonneg (by grind) (by grind) maxr_nonneg)]
    refine monotoneOn_rpowIntegrand₁₂ (by grind) (by grind) hz' maxr_nonneg ?_
    exact le_csSup (IsCompact.bddAbove (quasispectrum.isCompact _)) hz
  have hbound_finite_integral : HasFiniteIntegral bound (μ.restrict (Ioi 0)) := by
    rw [hasFiniteIntegral_norm_iff]
    exact (hμ maxr maxr_nonneg).1.2
  have hmapzero : ∀ᵐ (x : ℝ) ∂μ.restrict (Ioi 0), rpowIntegrand₁₂ p x 0 = 0 := by
    filter_upwards [ae_restrict_mem measurableSet_Ioi] with t ht
    simp [rpowIntegrand₁₂_zero ht]
  refine ⟨?integrable, ?integral⟩
  case integrable =>
    exact integrableOn_cfcₙ measurableSet_Ioi _ bound a hf hmapzero hbound hbound_finite_integral
  case integral => calc
      a ^ p = cfcₙ (fun x => NNReal.nnrpow x p) a := by
        rw [CFC.nnrpow_def]
      _ = cfcₙ (fun r => ∫ t in Ioi 0, rpowIntegrand₁₂ p t r ∂μ) a := by
        rw [cfcₙ_nnreal_eq_real ..]
        refine cfcₙ_congr fun r hr => ?_
        have hr' : 0 ≤ r := by grind
        simp only [sup_of_le_left hr', NNReal.nnrpow_def, NNReal.coe_rpow, coe_toNNReal']
        exact (hμ r hr').2
      _ = ∫ t in Ioi 0, cfcₙ (rpowIntegrand₁₂ p t) a ∂μ :=
        cfcₙ_setIntegral measurableSet_Ioi _ bound a hf hmapzero hbound
          hbound_finite_integral ha.isSelfAdjoint

Goal state after:
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 : ℕ
r : R
hr✝ : r ≤ 1
hr : r < 1
⊢ clog b r = -↑(Nat.log b ⌊r⁻¹⌋₊)

Tactic:
exact if_neg hr.not_ge

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

Goal state before:
pp: R : Type u_1
inst✝³ : Semifield R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorSemiring R
b : ℕ
r₁ r₂ : R
h₀ : 0 < r₁
h : r₁ ≤ r₂
⊢ clog b r₁ ≤ clog b r₂

Tactic:
have h₀' : 0 < r₂ := lt_of_lt_of_le h₀ h

Goal state after:
R : Type u_1
inst✝³ : Semifield R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorSemiring R
b : ℕ
r₁ r₂ : R
h₀ : 0 < r₁
h : r₁ ≤ r₂
h₀' : 0 < r₂
⊢ clog b r₁ ≤ clog b r₂
Module: Mathlib.Analysis.SpecialFunctions.MulExpNegMulSq

Goal state before:
pp: ε : ℝ
hε : 0 < ε
x y : ℝ
⊢ dist (ε.mulExpNegMulSq x) (ε.mulExpNegMulSq y) ≤ 2 * (√ε)⁻¹

Tactic:
apply le_trans (dist_triangle (mulExpNegMulSq ε x) 0 (mulExpNegMulSq ε y))
  simp only [dist_zero_right, norm_eq_abs, dist_zero_left, two_mul]
  exact add_le_add (abs_mulExpNegMulSq_le hε) (abs_mulExpNegMulSq_le hε)

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

Goal state before:
pp: b : ℝ
hb : b ≠ -1 ∧ b ≠ 0 ∧ b ≠ 1
this : ∀ {b : ℝ}, b ≠ -1 ∧ b ≠ 0 ∧ b ≠ 1 → 0 < b → Tendsto (fun x ↦ |logb b x|) atTop atTop
hb₀ : ¬0 < b
⊢ -b ≠ -1 ∧ -b ≠ 0 ∧ -b ≠ 1

Tactic:
simp [hb, neg_eq_iff_eq_neg]

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

Goal state before:
pp: b : ℝ
n : ℕ
x : ℝ
⊢ x ≠ 0 → id x = 0 → logb b x ^ n = 0

Tactic:
h₁

Goal state after:
b : ℝ
n : ℕ
x : ℝ
h₁ : x ≠ 0
⊢ id x = 0 → logb b x ^ n = 0
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 α
seq : ℕ → α := denseSeq α
hseq_dense : DenseRange seq
t : ℕ → SetRel α α
h_basis : (𝓤 α).HasAntitoneBasis t
htu : ∀ (i : ℕ), t i ∈ 𝓤 α
hto : ∀ (i : ℕ), IsOpen (t i)
a✝ : ∀ (i : ℕ), (t i).IsSymm
f : ℕ → ℕ → Set α := fun n m ↦ UniformSpace.ball (seq m) (t n)
⊢ ∃ K, IsCompact (closure K) ∧ P Kᶜ < ε

Tactic:
have h_univ n : (⋃ m, f n m) = univ := hseq_dense.iUnion_uniformity_ball (htu n)

Goal state after:
α : 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 α
seq : ℕ → α := denseSeq α
hseq_dense : DenseRange seq
t : ℕ → SetRel α α
h_basis : (𝓤 α).HasAntitoneBasis t
htu : ∀ (i : ℕ), t i ∈ 𝓤 α
hto : ∀ (i : ℕ), IsOpen (t i)
a✝ : ∀ (i : ℕ), (t i).IsSymm
f : ℕ → ℕ → Set α := fun n m ↦ UniformSpace.ball (seq m) (t n)
h_univ : ∀ (n : ℕ), ⋃ m, f n m = univ
⊢ ∃ K, IsCompact (closure K) ∧ P Kᶜ < ε
Module: Mathlib.MeasureTheory.Measure.RegularityCompacts

Goal state before:
pp: case refine_2
α : Type u_1
inst✝⁵ : MeasurableSpace α
inst✝⁴ : TopologicalSpace α
inst✝³ : SecondCountableTopology α
inst✝² : IsCompletelyPseudoMetrizableSpace α
inst✝¹ : BorelSpace α
P : Measure α
inst✝ : IsFiniteMeasure P
s t : Set α
hs_compact : IsCompact s
hs_closed : IsClosed s
ht_open : IsOpen t
⊢ IsCompact (s \ t) ∧ IsClosed (s \ t)

Tactic:
sdiff_eq

Goal state after:
case refine_2
α : Type u_1
inst✝⁵ : MeasurableSpace α
inst✝⁴ : TopologicalSpace α
inst✝³ : SecondCountableTopology α
inst✝² : IsCompletelyPseudoMetrizableSpace α
inst✝¹ : BorelSpace α
P : Measure α
inst✝ : IsFiniteMeasure P
s t : Set α
hs_compact : IsCompact s
hs_closed : IsClosed s
ht_open : IsOpen t
⊢ IsCompact (s ∩ tᶜ) ∧ IsClosed (s ∩ tᶜ)
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

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

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

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

Tactic:
· congr with w; split_ifs <;> simp only [zero_add, add_zero, *, neg_div]

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

case hg
L : PeriodPair
l₀ : ↥L.lattice
z : ℂ
⊢ Summable fun i ↦ if ↑i = ↑l₀ then -2 / (z - ↑l₀) ^ 3 else 0
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
⊢ HasStrictDerivAt arcsin (1 / √(1 - x ^ 2)) x ∧ ContDiffAt ℝ ω arcsin x

Tactic:
have : 0 < √(1 - x ^ 2) := sqrt_pos.2 (by nlinarith [h₁, h₂])
    simp only [← cos_arcsin, one_div] at this ⊢
    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.Elliptic.Weierstrass

Goal state before:
pp: L : PeriodPair
z : ℂ
l : ↥L.lattice
⊢ ℘'[L] (z + ↑l) = ℘'[L] z

Tactic:
by
  simp only [derivWeierstrassP]
  rw [← (Equiv.addRight l).tsum_eq]
  simp only [← tsum_neg, ← div_neg, Equiv.coe_addRight, Submodule.coe_add, add_sub_add_right_eq_sub]

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

Goal state before:
pp: L : PeriodPair
⊢ ℘'[L] 0 = 0

Tactic:
by
  rw [← CharZero.eq_neg_self_iff, ← L.derivWeierstrassP_neg, neg_zero]

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

Goal state before:
pp: n : ℕ
⊢ log (stirlingSeq (n + 1)) - log (stirlingSeq (n + 2)) ≤
    (1 / (2 * ↑(n + 1) + 1)) ^ 2 / (1 - (1 / (2 * ↑(n + 1) + 1)) ^ 2)

Tactic:
have h_nonneg : (0 : ℝ) ≤ ((1 : ℝ) / (2 * ↑(n + 1) + 1)) ^ 2 := sq_nonneg _

Goal state after:
n : ℕ
h_nonneg : 0 ≤ (1 / (2 * ↑(n + 1) + 1)) ^ 2
⊢ log (stirlingSeq (n + 1)) - log (stirlingSeq (n + 2)) ≤
    (1 / (2 * ↑(n + 1) + 1)) ^ 2 / (1 - (1 / (2 * ↑(n + 1) + 1)) ^ 2)
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.ContDiff

Goal state before:
pp: case hf
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
h : ContDiffOn ℝ 1 f (Icc a b)
hab : a ≤ b
g : E →ₗᵢ[ℝ] UniformSpace.Completion E := UniformSpace.Completion.toComplₗᵢ
this : ‖(⇑g ∘ f) b - (⇑g ∘ f) a‖ₑ = ‖f b - f a‖ₑ
x : ℝ
hx : x ∈ Ioo a b
⊢ DifferentiableAt ℝ f x

Tactic:
exact (h x ⟨hx.1.le, hx.2.le⟩).contDiffAt (Icc_mem_nhds hx.1 hx.2)
      |>.differentiableAt one_ne_zero

Goal state after:
Module: Mathlib.Order.Interval.Finset.Box

Goal state before:
pp: α : Type u_1
inst✝⁴ : Ring α
inst✝³ : PartialOrder α
inst✝² : IsOrderedRing α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
n : ℕ
⊢ (box (n + 1)).disjUnion (Icc (-↑n) ↑n) ⋯ = Icc (-↑n.succ) ↑n.succ

Tactic:
disjUnion_eq_union,

Goal state after:
α : Type u_1
inst✝⁴ : Ring α
inst✝³ : PartialOrder α
inst✝² : IsOrderedRing α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
n : ℕ
⊢ box (n + 1) ∪ Icc (-↑n) ↑n = Icc (-↑n.succ) ↑n.succ
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: case r_le
L : PeriodPair
l₀ x : ℂ
r : NNReal
hr0 : 0 < r
hr : Metric.closedBall x ↑r ⊆ (↑L.lattice \ {l₀})ᶜ
⊢ ∀ (l : ↥L.lattice), ↑l ≠ l₀ → ‖x + ↑↑r - x‖ < ‖↑l - x‖

Tactic:
· intro l hl
      simpa [-Metric.mem_closedBall, mem_closedBall_iff_norm]
        using Set.subset_compl_comm.mp hr ⟨l.2, hl⟩

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

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

Tactic:
by
  rw [← neg_neg x, T_eval_neg]
  convert! one_lt_eval_T_real hn (lt_neg_of_lt_neg hx)
  rw [Int.cast_negOnePow, ← mul_assoc, ← mul_zpow]
  simp

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

Goal state before:
pp: case mp
n : ℕ
hn : 2 ≤ n
x : ℝ
⊢ IsLocalExtr (fun x ↦ eval x (T ℝ ↑n)) x → ∃ k ∈ Finset.Ioo 0 n, x = cos (↑k * π / ↑n)

Tactic:
intro hx
    replace hx := hx.deriv_eq_zero
    rw [Polynomial.deriv, T_derivative_eq_U, eval_mul, Int.cast_natCast, eval_natCast,
      mul_eq_zero_iff_left (by aesop)] at hx
    replace hx : x ∈ (U ℝ (n - 1)).roots :=
      (mem_roots (degree_ne_bot.mp (ne_of_eq_of_ne (by grind [degree_U_natCast])
        (WithBot.natCast_ne_bot (n - 1))))).mpr hx
    rw [show (n - 1 : ℤ) = (n - 1 : ℕ) by grind, roots_U_real, Finset.mem_val] at hx
    obtain ⟨k, hk₁, hx⟩ := Finset.mem_image.mp hx
    refine ⟨k + 1, Finset.mem_Ioo.mpr ⟨k.zero_lt_succ, by grind⟩, ?_⟩
    rw [← hx]
    congr <;> norm_cast
    exact Nat.sub_add_cancel (Nat.one_le_of_lt hn)

Goal state after:
Module: Mathlib.CategoryTheory.Limits.IndYoneda

Goal state before:
pp: C : Type u₁
inst✝² : Category.{u₂, u₁} C
I : Type v₁
inst✝¹ : Category.{v₂, v₁} I
F : Iᵒᵖ ⥤ C
inst✝ : HasColimit F
i : I
⊢ (coyonedaOpColimitIsoLimitCoyoneda' F).inv ≫ coyoneda.map (colimit.ι F (op i)).op = limit.π (F.rightOp ⋙ coyoneda) i

Tactic:
← coyonedaOpColimitIsoLimitCoyoneda'_hom_comp_π,

Goal state after:
C : Type u₁
inst✝² : Category.{u₂, u₁} C
I : Type v₁
inst✝¹ : Category.{v₂, v₁} I
F : Iᵒᵖ ⥤ C
inst✝ : HasColimit F
i : I
⊢ (coyonedaOpColimitIsoLimitCoyoneda' F).inv ≫
      (coyonedaOpColimitIsoLimitCoyoneda' F).hom ≫ limit.π (F.rightOp ⋙ coyoneda) i =
    limit.π (F.rightOp ⋙ coyoneda) i
Module: Mathlib.CategoryTheory.Limits.Indization.Category

Goal state before:
pp: case refine_2
C : Type u
inst✝ : Category.{v, u} C
A B : Ind C
f : A ⟶ B
P : IndParallelPairPresentation ((Ind.inclusion C).map f) ((Ind.inclusion C).map f)
⊢ (Arrow.mk f).right ≅ (Arrow.mk ((Ind.lim P.I).map P.φ)).right

pp: case refine_3
C : Type u
inst✝ : Category.{v, u} C
A B : Ind C
f : A ⟶ B
P : IndParallelPairPresentation ((Ind.inclusion C).map f) ((Ind.inclusion C).map f)
⊢ (P.parallelPairIsoParallelPairCompIndYoneda.app WalkingParallelPair.zero).hom ≫
      (Arrow.mk ((Ind.lim P.I).map P.φ)).hom =
    (Arrow.mk f).hom ≫ Iso.hom ?refine_2

Tactic:
· exact P.parallelPairIsoParallelPairCompIndYoneda.app WalkingParallelPair.one

Goal state after:
case refine_3
C : Type u
inst✝ : Category.{v, u} C
A B : Ind C
f : A ⟶ B
P : IndParallelPairPresentation ((Ind.inclusion C).map f) ((Ind.inclusion C).map f)
⊢ (P.parallelPairIsoParallelPairCompIndYoneda.app WalkingParallelPair.zero).hom ≫
      (Arrow.mk ((Ind.lim P.I).map P.φ)).hom =
    (Arrow.mk f).hom ≫ (P.parallelPairIsoParallelPairCompIndYoneda.app WalkingParallelPair.one).hom
Module: Mathlib.CategoryTheory.Limits.FilteredColimitCommutesProduct

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
D : Type u_2
inst✝² : Category.{v_2, u_2} D
α : Type u_3
I : α → Type u_4
inst✝¹ : (i : α) → Category.{?u.15, u_4} (I i)
inst✝ : HasLimitsOfShape (Discrete α) C
F : (i : α) → I i ⥤ D ⥤ C
X : D
c : (i : α) → Cocone (F i)
j : (i : α) → I i
⊢ (((evaluation D C).obj X).mapCocone (coconePointwiseProduct c)).ι.app j ≫ (piObjIso (fun i ↦ (c i).pt) X).hom =
    ((Cocone.precompose (pointwiseProductCompEvaluation F X).hom).obj
            (coconePointwiseProduct fun i ↦ ((evaluation D C).obj X).mapCocone (c i))).ι.app
      j

Tactic:
by
    dsimp
    ext
    simp [Functor.pi, NatTrans.pi, ← NatTrans.comp_app]

Goal state after:
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
ky : (i : α) → I i
yk₀ : (pointwiseProduct F).obj ky
ky' : (i : α) → I i
yk₀' : (pointwiseProduct F).obj ky'
k : (i : α) → I i := IsFiltered.max ky ky'
yk : ∏ᶜ (Functor.pi F).obj k := (hom ((pointwiseProduct F).map (IsFiltered.leftToMax ky ky'))) yk₀
yk' : ∏ᶜ (Functor.pi F).obj k := (hom ((pointwiseProduct F).map (IsFiltered.rightToMax ky ky'))) yk₀'
hyk₀ : (hom (colimit.ι (pointwiseProduct F) ky)) yk₀ = (hom (colimit.ι (pointwiseProduct F) k)) yk
hyk₀' : (hom (colimit.ι (pointwiseProduct F) ky')) yk₀' = (hom (colimit.ι (pointwiseProduct F) k)) yk'
hy :
  (hom (colimitPointwiseProductToProductColimit F)) ((hom (colimit.ι (pointwiseProduct F) k)) yk) =
    (hom (colimitPointwiseProductToProductColimit F)) ((hom (colimit.ι (pointwiseProduct F) k)) yk')
k' : (s : α) → I s
f : (s : α) → k s ⟶ k' s
hk' :
  ∀ (s : α),
    (hom ((F s).map (f s))) ((hom (Pi.π (fun s ↦ (F s).obj (k s)) s)) yk) =
      (hom ((F s).map (f s))) ((hom (Pi.π (fun s ↦ (F s).obj (k s)) s)) yk')
x✝ : Discrete α
s : α
⊢ (hom (limit.π (Discrete.functor ((Functor.pi F).obj k')) { as := s })) ((hom ((pointwiseProduct F).map f)) yk) =
    (hom (limit.π (Discrete.functor ((Functor.pi F).obj k')) { as := s })) ((hom ((pointwiseProduct F).map f)) yk')

Tactic:
simpa [Functor.pi, Pi.map_π_apply] using hk' s

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Preradical.Basic

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
Φ : Preradical C
D : Type u_1
inst✝ : Category.{v_1, u_1} D
F : D ⥤ C
⊢ Mono (F.whiskerLeft Φ.ι)

Tactic:
rw [NatTrans.mono_iff_mono_app]

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
Φ : Preradical C
D : Type u_1
inst✝ : Category.{v_1, u_1} D
F : D ⥤ C
⊢ ∀ (k : D), Mono ((F.whiskerLeft Φ.ι).app k)