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)

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:
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
r : ℝ
⊢ r ∈ spectrum ℝ z → (a + b * r) ^ (-1) ≤ a + b * r ^ (-1)

Tactic:
hr

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
r : ℝ
hr : r ∈ spectrum ℝ z
⊢ (a + b * r) ^ (-1) ≤ a + b * r ^ (-1)
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Deligne

Goal state before:
pp: s : ℂ
hs : s ≠ 0
⊢ ↑π ^ (-(s / 2)) * (↑π)⁻¹ * (s / 2 * Gamma (s / 2)) = ↑π ^ (-s / 2) * Gamma (s / 2) * s / 2 / ↑π

Tactic:
field_simp

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

Goal state before:
pp: this : eulerMascheroniSeq 6 = 49 / 20 - log 7
⊢ 7 <
    ∑ i ∈ Finset.range 0, (49 / 20 - 1 / 2) ^ i / ↑i.factorial + (49 / 20 - 1 / 2) ^ 0 / ↑(Nat.factorial 0) +
                (49 / 20 - 1 / 2) ^ 1 / ↑(Nat.factorial 1) +
              (49 / 20 - 1 / 2) ^ 2 / ↑(Nat.factorial 2) +
            (49 / 20 - 1 / 2) ^ 3 / ↑(Nat.factorial 3) +
          (49 / 20 - 1 / 2) ^ 4 / ↑(Nat.factorial 4) +
        (49 / 20 - 1 / 2) ^ 5 / ↑(Nat.factorial 5) +
      (49 / 20 - 1 / 2) ^ 6 / ↑(Nat.factorial 6)

Tactic:
Nat.factorial_succ

Goal state after:
this : eulerMascheroniSeq 6 = 49 / 20 - log 7
⊢ 7 <
    ∑ i ∈ Finset.range 0, (49 / 20 - 1 / 2) ^ i / ↑i.factorial + (49 / 20 - 1 / 2) ^ 0 / ↑(Nat.factorial 0) +
                (49 / 20 - 1 / 2) ^ 1 / ↑((0 + 1) * Nat.factorial 0) +
              (49 / 20 - 1 / 2) ^ 2 / ↑((1 + 1) * ((0 + 1) * Nat.factorial 0)) +
            (49 / 20 - 1 / 2) ^ 3 / ↑((2 + 1) * ((1 + 1) * ((0 + 1) * Nat.factorial 0))) +
          (49 / 20 - 1 / 2) ^ 4 / ↑((3 + 1) * ((2 + 1) * ((1 + 1) * ((0 + 1) * Nat.factorial 0)))) +
        (49 / 20 - 1 / 2) ^ 5 / ↑((4 + 1) * ((3 + 1) * ((2 + 1) * ((1 + 1) * ((0 + 1) * Nat.factorial 0))))) +
      (49 / 20 - 1 / 2) ^ 6 / ↑((5 + 1) * ((4 + 1) * ((3 + 1) * ((2 + 1) * ((1 + 1) * ((0 + 1) * Nat.factorial 0))))))
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Deligne

Goal state before:

Tactic:
_ = (π ^ (-s / 2) * π ^ (-(s + 1) / 2)) * (Gamma (s / 2) * Gamma (s / 2 + 1 / 2)) := by ring_nf
  _ = 2 ^ (1 - s) * (π ^ (-1 / 2 - s) * π ^ (1 / 2 : ℂ)) * Gamma s := by
    rw [← cpow_add _ _ (ofReal_ne_zero.mpr pi_ne_zero), Complex.Gamma_mul_Gamma_add_half,
      sqrt_eq_rpow, ofReal_cpow pi_pos.le, ofReal_div, ofReal_one, ofReal_ofNat]
    ring_nf
  _ = 2 * ((2 : ℝ) ^ (-s) * π ^ (-s)) * Gamma s := by
    rw [sub_eq_add_neg, cpow_add _ _ two_ne_zero, cpow_one,
      ← cpow_add _ _ (ofReal_ne_zero.mpr pi_ne_zero), ofReal_ofNat]
    ring_nf
  _ = 2 * (2 * π) ^ (-s) * Gamma s := by
    rw [← mul_cpow_ofReal_nonneg two_pos.le pi_pos.le, ofReal_ofNat]

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
  have h2 : ∀ (n : ℕ), s ≠ -(2 * ↑n + 1) := by
    intro n h
    specialize hs (2 * n + 1)
    simp_all
  rw [← Gammaℝ_div_Gammaℝ_one_sub h2, ← div_eq_mul_inv, div_right_comm, div_self h1, one_div]

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

Goal state before:
pp: ⊢ (1 / 2).digamma = -2 * log 2 - ↑Real.eulerMascheroniConstant

Tactic:
rw [digamma_def, logDeriv_apply, hasDerivAt_Gamma_one_half.deriv, add_comm, Gamma_one_half_eq,
    neg_mul, ← mul_neg, neg_add', Real.sqrt_eq_rpow, ofReal_cpow Real.pi_nonneg]
  simp

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

Goal state before:
pp: 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
hder_nat : ∀ (n : ℕ), deriv f (↑n + 1) = deriv f 1 + ↑(harmonic n)
derivLB : ∀ (n : ℕ), 0 < n → log ↑n ≤ deriv f (↑n + 1)
n : ℕ
⊢ deriv f (↑n + 1) ≤ log (↑n + 1)

Tactic:
refine (hc.deriv_le_slope (by positivity : (0 : ℝ) < n + 1) (by positivity : (0 : ℝ) < n + 2)
        (by linarith) (hder <| by positivity)).trans (le_of_eq ?_)

Goal state after:
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
hder_nat : ∀ (n : ℕ), deriv f (↑n + 1) = deriv f 1 + ↑(harmonic n)
derivLB : ∀ (n : ℕ), 0 < n → log ↑n ≤ deriv f (↑n + 1)
n : ℕ
⊢ slope f (↑n + 1) (↑n + 2) = log (↑n + 1)
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
hg : HasDerivAt g (-↑√π * (↑γ + 2 * log 2) / 2) 1
⊢ -log ↑π / 2 / ↑√π * Gamma (1 / 2) + ↑π ^ (-1 / 2) * (-↑√π * (↑γ + 2 * log 2) / 2) = -(↑γ + log (4 * ↑π)) / 2

Tactic:
rw [Gamma_one_half_eq, aux, div_mul_cancel₀ _ aux2, neg_div _ (1 : ℂ), cpow_neg, aux,
    mul_div_assoc, ← mul_assoc, mul_neg, inv_mul_cancel₀ aux2, neg_one_mul, ← neg_div,
    ← _root_.add_div, ← neg_add, add_comm, add_assoc, ← ofReal_log Real.pi_pos.le, ← ofReal_ofNat,
    ← ofReal_log zero_le_two,
    ← ofReal_mul, ← Nat.cast_ofNat (R := ℝ), ← Real.log_pow, ← ofReal_add,
    ← Real.log_mul (by positivity) (by positivity),
    Nat.cast_ofNat, ofReal_ofNat, ofReal_log (by positivity)]

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
⊢ -(↑γ + log ↑(2 ^ 2 * π)) / 2 = -(↑γ + log (4 * ↑π)) / 2
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
hrp : 0 < r
hr : 1 ≤ r
⊢ clog b r⁻¹ = -log b r

Tactic:
rw [clog_of_right_le_one _ (inv_le_one_of_one_le₀ hr), log_of_one_le_right _ hr, inv_inv]

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

Goal state before:
pp: ⊢ StrictAntiOn (fun x ↦ x * log x) (Icc 0 (rexp (-1)))

Tactic:
refine strictAntiOn_of_deriv_neg (convex_Icc ..) continuous_mul_log.continuousOn fun x hx ↦ ?_
  have hgt : x < rexp (-1) := by simp_all [interior_Icc, mem_Ioo]
  have hpos : 0 < x := by simp_all [interior_Icc, mem_Ioo]
  grind [deriv_mul_log, Real.log_lt_iff_lt_exp hpos |>.mpr hgt]

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

Goal state before:
pp: ε : ℝ
hε : 0 < ε
x : ℝ
⊢ ‖deriv ε.mulExpNegMulSq x‖ ≤ ↑1

Tactic:
exact norm_deriv_mulExpNegMulSq_le_one hε x

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

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

pp: b✝ b : ℝ
hb : b ≠ -1 ∧ b ≠ 0 ∧ b ≠ 1
hb₀ : 0 < b
hb₁ : 1 < b
⊢ Tendsto (fun x ↦ |logb b x|) atTop atTop

Tactic:
· exact (this (b := b⁻¹) (by simp [hb, inv_eq_iff_eq_inv, inv_neg]) (by simpa)
      ((one_lt_inv₀ hb₀).2 (by linarith +splitNe))).congr (by simp)

Goal state after:
b✝ b : ℝ
hb : b ≠ -1 ∧ b ≠ 0 ∧ b ≠ 1
hb₀ : 0 < b
hb₁ : 1 < b
⊢ Tendsto (fun x ↦ |logb b x|) atTop atTop
Module: Mathlib.MeasureTheory.Measure.RegularityCompacts

Goal state before:
pp: case mp
α : Type u_1
inst✝² : MeasurableSpace α
μ : Measure α
inst✝¹ : TopologicalSpace α
inst✝ : R1Space α
h : μ.InnerRegularWRT (IsCompact ∘ closure) IsClosed
A : Set α
hA : IsClosed A
r : ℝ≥0∞
⊢ r < μ A → ∃ K ⊆ A, IsCompact K ∧ r < μ K

Tactic:
hr

Goal state after:
case mp
α : Type u_1
inst✝² : MeasurableSpace α
μ : Measure α
inst✝¹ : TopologicalSpace α
inst✝ : R1Space α
h : μ.InnerRegularWRT (IsCompact ∘ closure) IsClosed
A : Set α
hA : IsClosed A
r : ℝ≥0∞
hr : r < μ A
⊢ ∃ K ⊆ A, IsCompact K ∧ r < μ K
Module: Mathlib.MeasureTheory.Measure.RegularityCompacts

Goal state before:
pp: case mpr
α : Type u_1
inst✝² : MeasurableSpace α
μ : Measure α
inst✝¹ : TopologicalSpace α
inst✝ : R1Space α
h : μ.InnerRegularWRT IsCompact IsClosed
A : Set α
hA : IsClosed A
r : ℝ≥0∞
⊢ r < μ A → ∃ K ⊆ A, (IsCompact ∘ closure) K ∧ r < μ K

Tactic:
hr

Goal state after:
case mpr
α : Type u_1
inst✝² : MeasurableSpace α
μ : Measure α
inst✝¹ : TopologicalSpace α
inst✝ : R1Space α
h : μ.InnerRegularWRT IsCompact IsClosed
A : Set α
hA : IsClosed A
r : ℝ≥0∞
hr : r < μ A
⊢ ∃ K ⊆ A, (IsCompact ∘ closure) K ∧ r < μ K
Module: Mathlib.MeasureTheory.Measure.RegularityCompacts

Goal state before:
pp: case mp
α : Type u_1
inst✝² : MeasurableSpace α
μ : Measure α
inst✝¹ : TopologicalSpace α
inst✝ : R1Space α
h : μ.InnerRegularWRT (fun s ↦ IsCompact s ∧ IsClosed s) IsClosed
A : Set α
hA : IsClosed A
r : ℝ≥0∞
⊢ r < μ A → ∃ K ⊆ A, (IsCompact ∘ closure) K ∧ r < μ K

Tactic:
hr

Goal state after:
case mp
α : Type u_1
inst✝² : MeasurableSpace α
μ : Measure α
inst✝¹ : TopologicalSpace α
inst✝ : R1Space α
h : μ.InnerRegularWRT (fun s ↦ IsCompact s ∧ IsClosed s) IsClosed
A : Set α
hA : IsClosed A
r : ℝ≥0∞
hr : r < μ A
⊢ ∃ K ⊆ A, (IsCompact ∘ closure) K ∧ r < μ K
Module: Mathlib.MeasureTheory.Measure.RegularityCompacts

Goal state before:
pp: case mpr
α : Type u_1
inst✝² : MeasurableSpace α
μ : Measure α
inst✝¹ : TopologicalSpace α
inst✝ : R1Space α
h : μ.InnerRegularWRT (IsCompact ∘ closure) IsClosed
A : Set α
hA : IsClosed A
r : ℝ≥0∞
⊢ r < μ A → ∃ K ⊆ A, (fun s ↦ IsCompact s ∧ IsClosed s) K ∧ r < μ K

Tactic:
hr

Goal state after:
case mpr
α : Type u_1
inst✝² : MeasurableSpace α
μ : Measure α
inst✝¹ : TopologicalSpace α
inst✝ : R1Space α
h : μ.InnerRegularWRT (IsCompact ∘ closure) IsClosed
A : Set α
hA : IsClosed A
r : ℝ≥0∞
hr : r < μ A
⊢ ∃ K ⊆ A, (fun s ↦ IsCompact s ∧ IsClosed s) K ∧ r < μ K
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∞
⊢ r < μ A → ∃ K ⊆ A, p K ∧ r < μ K

Tactic:
hr

Goal state after:
α : 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 ⊆ A, p K ∧ r < μ K
Module: Mathlib.MeasureTheory.Measure.RegularityCompacts

Goal state before:
pp: α : Type u_1
inst✝⁴ : MeasurableSpace α
μ✝ : Measure α
inst✝³ : TopologicalSpace α
inst✝² : SecondCountableTopology α
inst✝¹ : IsCompletelyPseudoMetrizableSpace α
inst✝ : BorelSpace α
μ : Measure α
A : Set α
hA1 : MeasurableSet A
hA2 : μ A ≠ ∞
r : ℝ≥0∞
⊢ r < μ A → ∃ K ⊆ A, IsCompact K ∧ r < μ K

Tactic:
hr

Goal state after:
α : Type u_1
inst✝⁴ : MeasurableSpace α
μ✝ : Measure α
inst✝³ : TopologicalSpace α
inst✝² : SecondCountableTopology α
inst✝¹ : IsCompletelyPseudoMetrizableSpace α
inst✝ : BorelSpace α
μ : Measure α
A : Set α
hA1 : MeasurableSet A
hA2 : μ A ≠ ∞
r : ℝ≥0∞
hr : r < μ A
⊢ ∃ K ⊆ A, IsCompact K ∧ r < μ K
Module: Mathlib.Analysis.SpecialFunctions.MulExpNegMulSqIntegral

Goal state before:
pp: case h_lim
E : Type u_1
inst✝³ : TopologicalSpace E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
P : Measure E
inst✝ : IsFiniteMeasure P
g : E →ᵇ ℝ
u : ℕ → ℝ
hu : Tendsto u atTop (𝓝[>] 0)
N : ℕ
hupos : ∀ (b : ℕ), N ≤ b → u b ∈ Set.Ioi 0
⊢ ∀ᵐ (ω : E) ∂P, Tendsto (fun n ↦ (u n).mulExpNegMulSq (g ω)) atTop (𝓝 (g ω))

Tactic:
· exact Eventually.of_forall (fun _ => (tendsto_nhdsWithin_of_tendsto_nhds
        tendsto_mulExpNegMulSq).comp hu)

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

Goal state before:
pp: case h_bound
E : Type u_1
inst✝³ : TopologicalSpace E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
P : Measure E
inst✝ : IsFiniteMeasure P
ε : ℝ
g : E →ᵇ ℝ
hε : 0 < ε
⊢ ∃ C, ∀ᶠ (n : ℕ) in atTop, ∀ᵐ (ω : E) ∂P, ‖(g * (1 + (↑n)⁻¹ • -(ε • g * g)) ^ n) ω‖ ≤ C

pp: case h_lim
E : Type u_1
inst✝³ : TopologicalSpace E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
P : Measure E
inst✝ : IsFiniteMeasure P
ε : ℝ
g : E →ᵇ ℝ
hε : 0 < ε
⊢ ∀ᵐ (ω : E) ∂P, Tendsto (fun n ↦ (g * (1 + (↑n)⁻¹ • -(ε • g * g)) ^ n) ω) atTop (𝓝 (ε.mulExpNegMulSq (g ω)))

Tactic:
· obtain ⟨N, hgN⟩ := exists_nat_gt (ε * (norm g * norm g))
    use norm g
    rw [eventually_atTop]
    use N
    intro n hn
    have hnpos : 0 < (n : ℝ) := by
      apply lt_of_lt_of_le (lt_of_le_of_lt _ hgN) (Nat.cast_le.mpr hn)
      exact (mul_nonneg (le_of_lt hε) (mul_self_nonneg (norm g)))
    apply Eventually.of_forall
    intro x
    simp only [smul_neg, BoundedContinuousFunction.coe_mul, Pi.mul_apply, pow_apply,
      BoundedContinuousFunction.coe_add, BoundedContinuousFunction.coe_one, coe_neg,
      BoundedContinuousFunction.coe_smul, smul_eq_mul, Pi.add_apply, Pi.one_apply, Pi.neg_apply,
      norm_mul, norm_eq_abs, norm_pow]
    refine (mul_le_mul_of_nonneg_right (norm_coe_le_norm g x) (pow_nonneg (abs_nonneg _) n)).trans
      <| mul_le_of_le_one_right (norm_nonneg _) ?_
    apply pow_le_one₀ (abs_nonneg _)
    rw [mul_assoc, inv_mul_eq_div, abs_le]
    refine ⟨?_, (add_le_iff_nonpos_right 1).mpr (Left.neg_nonpos_iff.mpr
      (div_nonneg (mul_nonneg (le_of_lt hε) (mul_self_nonneg (g x))) (le_of_lt hnpos)))⟩
    apply le_trans (by linarith) (sub_nonneg_of_le ((div_le_one hnpos).mpr _))
    apply le_trans (le_trans _ (le_of_lt hgN)) (Nat.cast_le.mpr hn)
    apply mul_le_mul (le_refl ε) _ (mul_self_nonneg (g x)) (le_of_lt hε)
    rw [← abs_le_iff_mul_self_le, abs_norm]
    exact norm_coe_le_norm g x

Goal state after:
case h_lim
E : Type u_1
inst✝³ : TopologicalSpace E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
P : Measure E
inst✝ : IsFiniteMeasure P
ε : ℝ
g : E →ᵇ ℝ
hε : 0 < ε
⊢ ∀ᵐ (ω : E) ∂P, Tendsto (fun n ↦ (g * (1 + (↑n)⁻¹ • -(ε • g * g)) ^ n) ω) atTop (𝓝 (ε.mulExpNegMulSq (g ω)))
Module: Mathlib.Analysis.SpecialFunctions.Pow.NthRootLemmas

Goal state before:
pp: case inr
n a b : ℕ
hn : n ≠ 0
hlt : n.nthRoot b < a
⊢ b < a ^ n

Tactic:
refine (lt_pow_nthRoot_add_one hn b).trans_le ?_

Goal state after:
case inr
n a b : ℕ
hn : n ≠ 0
hlt : n.nthRoot b < a
⊢ (n.nthRoot b + 1) ^ n ≤ a ^ n
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: L : PeriodPair
l₀ z : ℂ
⊢ ℘[L - l₀] (-z) = ℘[L - -l₀] z

Tactic:
by
  simp only [weierstrassPExcept]
  rw [← (Equiv.neg L.lattice).tsum_eq]
  congr! 3 with l
  · simp [neg_eq_iff_eq_neg]
  simp
  ring

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

Goal state before:
pp: case refine_2
a b : Multiset ℂ
n : ℕ
hb : ∀ k ∈ b, k ≠ -↑n
⊢ ↑(n + 1)! = ↑n ! * (↑n + 1)

Tactic:
Nat.factorial_succ

Goal state after:
case refine_2
a b : Multiset ℂ
n : ℕ
hb : ∀ k ∈ b, k ≠ -↑n
⊢ ↑((n + 1) * n !) = ↑n ! * (↑n + 1)
Module: Mathlib.Analysis.SpecialFunctions.RegularizedHypergeometric

Goal state before:
pp: case pos
a b : Multiset ℂ
n : ℕ
h : regularizedHGFunCoeff a b n ≠ 0
hb : ∀ k ∈ b, k ≠ -↑n
⊢ regularizedHGFunCoeff a b n *
        ((Multiset.map (fun x ↦ x + ↑n) a).prod / ((Multiset.map (fun x ↦ x + ↑n) b).prod * (↑n + 1))) /
      regularizedHGFunCoeff a b n =
    (Multiset.map (fun x ↦ x + ↑n) a).prod / ((Multiset.map (fun x ↦ x + ↑n) b).prod * (↑n + 1))

Tactic:
field_simp

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

Goal state before:
pp: case e_f
n : ℕ
a : Multiset ℂ
hn : n ≠ 0
x✝ : ℂ
⊢ x✝ + ↑n = ↑n * (x✝ / ↑n + 1)

Tactic:
field_simp

Goal state after:
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 + 1) a).prod /
      (↑n ^ b.card * (Multiset.map (fun x ↦ x / ↑n + 1) b).prod * (↑n + 1)) =
    ↑n ^ (↑a.card - ↑b.card - 1) * (Multiset.map (fun x ↦ x / ↑n + 1) a).prod /
      ((Multiset.map (fun x ↦ x / ↑n + 1) b).prod * (1 + (↑n)⁻¹))

Tactic:
field_simp

Goal state after:
n : ℕ
a b : Multiset ℂ
hn : n ≠ 0
⊢ ↑n ^ a.card * (Multiset.map (fun x ↦ (x + ↑n) / ↑n) a).prod / (Multiset.map (fun x ↦ (x + ↑n) / ↑n) b).prod =
    ↑n * (Multiset.map (fun x ↦ (x + ↑n) / ↑n) a).prod * ↑n ^ b.card * ↑n ^ (↑a.card - ↑b.card - 1) /
      (Multiset.map (fun x ↦ (x + ↑n) / ↑n) b).prod
Module: Mathlib.Analysis.SpecialFunctions.RegularizedHypergeometric

Goal state before:
pp: a b : Multiset ℂ
n : ℕ
j : ℂ
ha : j ∈ a
hj : j = -↑n
⊢ ∃ a_1, ∀ (b_1 : ℕ), a_1 ≤ b_1 → regularizedHGFunSeries a b b_1 = 0

Tactic:
use n + 1

Goal state after:
case h
a b : Multiset ℂ
n : ℕ
j : ℂ
ha : j ∈ a
hj : j = -↑n
⊢ ∀ (b_1 : ℕ), n + 1 ≤ b_1 → regularizedHGFunSeries a b b_1 = 0
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: L : PeriodPair
l₀ : ℂ
⊢ HasSumLocallyUniformly (fun l z ↦ if ↑l = l₀ then 0 else -2 / (z - ↑l) ^ 3) ℘'[L - l₀]

Tactic:
by
  refine L.hasSumLocallyUniformly_aux (u := fun _ ↦ (16 * ‖·‖ ^ (-3 : ℝ))) _
    (fun _ _ ↦ (ZLattice.summable_norm_rpow _ _ (by simp; norm_num)).mul_left _) fun r hr ↦
    Filter.eventually_atTop.mpr ⟨2 * r, ?_⟩
  rintro _ h s hs l rfl
  split_ifs
  · simp
  have : s ≠ ↑l := by rintro rfl; exfalso; linarith
  have : l ≠ 0 := by rintro rfl; simp_all; linarith
  simp only [Complex.norm_div, norm_neg, Complex.norm_ofNat, norm_pow]
  rw [Real.rpow_neg (by positivity), ← div_eq_mul_inv, div_le_div_iff₀, norm_sub_rev]
  · refine LE.le.trans_eq (b := 2 * (2 * ‖l - s‖) ^ 3) ?_ (by ring)
    norm_cast
    gcongr
    refine le_trans ?_ (mul_le_mul le_rfl (norm_sub_norm_le _ _) (by linarith) (by linarith))
    norm_cast at *
    linarith
  · exact pow_pos (by simpa [sub_eq_zero]) _
  · exact Real.rpow_pos_of_pos (by simpa) _

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

Goal state before:
pp: E : Type u_1
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : MeasurableSpace E
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

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)))
⊢ μ.toSphere ≠ 0

Tactic:
integrableOn_iff_comap_subtypeVal,

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)) ↔
    Integrable ((fun y ↦ y ^ (dim E - 1) • f y) ∘ Subtype.val) (Measure.comap Subtype.val 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)))
⊢ MeasurableSet (Ioi 0)

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.Elliptic.Weierstrass

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

Tactic:
obtain rfl := sub_eq_zero.mp e

Goal state after:
L : PeriodPair
l₀ : ℂ
s : Finset ↥L.lattice
x : ↥L.lattice
hl₁ : ¬↑x = l₀
hl : ↑x ∈ (↑L.lattice \ {l₀})ᶜ
e : ↑x - ↑x = 0
⊢ ↑x = l₀
Module: Mathlib.Analysis.SpecialFunctions.RegularizedHypergeometric

Goal state before:
pp: case neg.hc
a b : Multiset ℂ
h : a.card ≤ b.card
ha : ∀ j ∈ a, ∀ (k : ℕ), j ≠ -↑k
⊢ ∀ᶠ (n : ℕ) in atTop, regularizedHGFunCoeff a b n ≠ 0

Tactic:
apply eventually_atTop_regularizedHGFunCoeff_ne_zero b ha

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 = -(2 * ((l - ↑x) ^ 3)⁻¹)

Tactic:
field_simp

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

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

Tactic:
obtain rfl := sub_eq_zero.mp e

Goal state after:
L : PeriodPair
l₀ : ℂ
s : Finset ↥L.lattice
x : ↥L.lattice
hxs : x ∈ s
hl₁ : ¬↑x = l₀
hl : ↑x ∈ (↑L.lattice \ {l₀})ᶜ
e : ↑x - ↑x = 0
⊢ ↑x = l₀
Module: Mathlib.Analysis.SpecialFunctions.Sigmoid

Goal state before:
pp: x : ℝ
⊢ (1 + rexp (- -x))⁻¹ = 1 - (1 + rexp (-x))⁻¹

Tactic:
field_simp

Goal state after:
x : ℝ
⊢ 1 + rexp (-x) = (1 + rexp x) * (1 + rexp (-x) - 1)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Basic

Goal state before:
pp: θ : ℂ
n : ℤ
⊢ eval (cosh θ) (T ℂ n) = eval (cos (θ * I)) (T ℂ n)

Tactic:
by rw [cos_mul_I]

Goal state after: