mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Normed.Operator.ContinuousAlgEquiv

Goal state before:
pp: case pos
𝕜 : Type u_1
V : Type u_2
W : Type u_3
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace 𝕜 V
inst✝³ : CompleteSpace V
inst✝² : NormedAddCommGroup W
inst✝¹ : InnerProductSpace 𝕜 W
inst✝ : CompleteSpace W
f : (V →L[𝕜] V) ≃⋆ₐ[𝕜] W →L[𝕜] W
hf : Continuous ⇑f
h✝¹ : Subsingleton V
h✝ : Subsingleton W
⊢ ∃ U, f = U.conjStarAlgEquiv

pp: case neg
𝕜 : Type u_1
V : Type u_2
W : Type u_3
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace 𝕜 V
inst✝³ : CompleteSpace V
inst✝² : NormedAddCommGroup W
inst✝¹ : InnerProductSpace 𝕜 W
inst✝ : CompleteSpace W
f : (V →L[𝕜] V) ≃⋆ₐ[𝕜] W →L[𝕜] W
hf : Continuous ⇑f
h✝¹ : Subsingleton V
h✝ : Nontrivial W
⊢ ∃ U, f = U.conjStarAlgEquiv

Tactic:
· use { toLinearEquiv := 0,
            norm_map' _ := by simp [Subsingleton.eq_zero (α := V), Subsingleton.eq_zero (α := W)] }
      exact ext fun _ ↦ Subsingleton.allEq _ _

Goal state after:
case neg
𝕜 : Type u_1
V : Type u_2
W : Type u_3
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace 𝕜 V
inst✝³ : CompleteSpace V
inst✝² : NormedAddCommGroup W
inst✝¹ : InnerProductSpace 𝕜 W
inst✝ : CompleteSpace W
f : (V →L[𝕜] V) ≃⋆ₐ[𝕜] W →L[𝕜] W
hf : Continuous ⇑f
h✝¹ : Subsingleton V
h✝ : Nontrivial W
⊢ ∃ U, f = U.conjStarAlgEquiv
Module: Mathlib.Analysis.ODE.ExistUnique

Goal state before:
pp: case refine_2
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℝ → E → E
tmin tmax : ℝ
t₀ : ↑(Icc tmin tmax)
x₀ : E
a r L K : ℝ≥0
hf : IsPicardLindelof f t₀ x₀ a r L K
α : (x : E) → x ∈ closedBall x₀ ↑r → FunSpace t₀ x₀ r L
hα : ∀ (x : E) (hx : x ∈ closedBall x₀ ↑r), IsFixedPt (FunSpace.next hf hx) (α x hx)
α' : E → ℝ → E := fun x ↦ if hx : x ∈ closedBall x₀ ↑r then (α x hx).compProj else 0
hα' : α' = fun x ↦ if hx : x ∈ closedBall x₀ ↑r then (α x hx).compProj else 0
x : E
hx : x ∈ closedBall x₀ ↑r
t : ℝ
ht : t ∈ Icc tmin tmax
⊢ HasDerivWithinAt (α x hx).compProj (f t ((α x hx).compProj t)) (Icc tmin tmax) t

Tactic:
FunSpace.compProj_apply

Goal state after:
case refine_2
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℝ → E → E
tmin tmax : ℝ
t₀ : ↑(Icc tmin tmax)
x₀ : E
a r L K : ℝ≥0
hf : IsPicardLindelof f t₀ x₀ a r L K
α : (x : E) → x ∈ closedBall x₀ ↑r → FunSpace t₀ x₀ r L
hα : ∀ (x : E) (hx : x ∈ closedBall x₀ ↑r), IsFixedPt (FunSpace.next hf hx) (α x hx)
α' : E → ℝ → E := fun x ↦ if hx : x ∈ closedBall x₀ ↑r then (α x hx).compProj else 0
hα' : α' = fun x ↦ if hx : x ∈ closedBall x₀ ↑r then (α x hx).compProj else 0
x : E
hx : x ∈ closedBall x₀ ↑r
t : ℝ
ht : t ∈ Icc tmin tmax
⊢ HasDerivWithinAt (α x hx).compProj (f t ((α x hx).toFun (projIcc tmin tmax ⋯ t))) (Icc tmin tmax) t
Module: Mathlib.Analysis.Polynomial.CauchyBound

Goal state before:
pp: K : Type u_1
inst✝ : NormedDivisionRing K
p : K[X]
hp : p ≠ 0
a : K
h : ‖p.leadingCoeff * a ^ p.natDegree‖₊ = ‖-∑ i ∈ range p.natDegree, p.coeff i * a ^ i‖₊
⊢ ‖a‖₊ < p.cauchyBound

Tactic:
simp only [nnnorm_mul, nnnorm_pow, nnnorm_neg] at h

Goal state after:
K : Type u_1
inst✝ : NormedDivisionRing K
p : K[X]
hp : p ≠ 0
a : K
h : ‖p.leadingCoeff‖₊ * ‖a‖₊ ^ p.natDegree = ‖∑ i ∈ range p.natDegree, p.coeff i * a ^ i‖₊
⊢ ‖a‖₊ < p.cauchyBound
Module: Mathlib.Analysis.Polynomial.Fourier

Goal state before:
pp: p : ℂ[X]
n : ℕ
⊢ fourierCoeff ⇑(toAddCircle p) ↑n = p.coeff n

Tactic:
simp [fourierCoeff_toAddCircle]

Goal state after:
Module: Mathlib.RingTheory.Polynomial.GaussNorm

Goal state before:
pp: R : Type u_1
F : Type u_2
inst✝² : Semiring R
inst✝¹ : FunLike F R ℝ
v : F
c : ℝ
p : R[X]
inst✝ : NonnegHomClass F R ℝ
hc : 0 ≤ c
⊢ 0 ≤ gaussNorm v c p

Tactic:
by
  by_cases hp : p.support.Nonempty <;>
  simp_all [gaussNorm, sup'_nonneg_of_ne_zero, -Finset.le_sup'_iff]

Goal state after:
Module: Mathlib.Analysis.ODE.PicardLindelof

Goal state before:
pp: E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℝ → E → E
tmin tmax tmin' tmax' : ℝ
t₀ : ↑(Icc tmin tmax)
x₀ : E
a r L K : ℝ≥0
hf : IsPicardLindelof f t₀ x₀ a r L K
t₀' : ↑(Icc tmin' tmax')
ht₀ : ↑t₀ = ↑t₀'
htmin : tmin ≤ tmin'
htmax : tmax' ≤ tmax
⊢ ↑L * max (tmax' - ↑t₀') (↑t₀' - tmin') ≤ ↑a - ↑r

Tactic:
calc L * max (tmax' - t₀') (t₀' - tmin')
    _ ≤ L * max (tmax - t₀) (t₀ - tmin) := by gcongr <;> linarith
    _ ≤ a - r := hf.mul_max_le

Goal state after:
Module: Mathlib.Analysis.Polynomial.MahlerMeasure

Goal state before:
pp: case a.refine_2
p : ℂ[X]
⊢ p.support.card • p.supNorm ^ 2 ≤ (↑p.natDegree + 1) * p.supNorm ^ 2

Tactic:
simp only [nsmul_eq_mul]
      gcongr
      exact mod_cast p.card_supp_le_succ_natDegree

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

Goal state before:
pp: case inr
x : ℝ
hx : Irrational x
a b : ℤ
p_nonzero : C a * X + C b ≠ 0
x_is_root : (aeval x) (C a * X + C b) = 0
this : -↑b / ↑a = x
ha : ¬a = 0
⊢ False

pp: case inr
x : ℝ
hx : Irrational x
a b : ℤ
p_nonzero : C a * X + C b ≠ 0
x_is_root : (aeval x) (C a * X + C b) = 0
this : x * ↑a = -↑b
ha : ¬a = 0
⊢ ↑a ≠ 0

Tactic:
· refine hx ⟨-b / a, ?_⟩
      assumption_mod_cast

Goal state after:
case inr
x : ℝ
hx : Irrational x
a b : ℤ
p_nonzero : C a * X + C b ≠ 0
x_is_root : (aeval x) (C a * X + C b) = 0
this : x * ↑a = -↑b
ha : ¬a = 0
⊢ ↑a ≠ 0
Module: Mathlib.Analysis.Real.Hyperreal

Goal state before:
pp: r s : ℝ
f : ℝ → ℝ → ℝ
hf : ContinuousAt (Function.uncurry f) (r, s)
x : ℕ → ℝ
hxr : Tendsto x (↑(hyperfilter ℕ)) (𝓝 r)
y : ℕ → ℝ
hys : Tendsto y (↑(hyperfilter ℕ)) (𝓝 s)
⊢ IsSt (Germ.map₂ f (ofSeq x) (ofSeq y)) (f r s)

Tactic:
exact isSt_ofSeq_iff_tendsto.2 <| hf.tendsto.comp (hxr.prodMk_nhds hys)

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arctan

Goal state before:
pp: z : ℂ
h₁ : z ≠ I
h₂ : z ≠ -I
z₁ : 1 + z * I ≠ 0
z₂ : 1 - z * I ≠ 0
⊢ cexp (log ((1 + z * I) / (1 - z * I))) = (1 + z * I) / (1 - z * I)

Tactic:
exp_log

Goal state after:
z : ℂ
h₁ : z ≠ I
h₂ : z ≠ -I
z₁ : 1 + z * I ≠ 0
z₂ : 1 - z * I ≠ 0
⊢ (1 + z * I) / (1 - z * I) = (1 + z * I) / (1 - z * I)

z : ℂ
h₁ : z ≠ I
h₂ : z ≠ -I
z₁ : 1 + z * I ≠ 0
z₂ : 1 - z * I ≠ 0
⊢ (1 + z * I) / (1 - z * I) ≠ 0
Module: Mathlib.Analysis.Real.Pi.Wallis

Goal state before:
pp: k : ℕ
⊢ 2 / π * W k = 2 / π * ∏ x ∈ range k, (2 * ↑x + 2) / (2 * ↑x + 3) / ((2 * ↑x + 1) / (2 * ↑x + 2))

Tactic:
div_div_div_comm,

Goal state after:
k : ℕ
⊢ 2 / π * W k = 2 / π * ∏ x ∈ range k, (2 * ↑x + 2) / (2 * ↑x + 1) / ((2 * ↑x + 3) / (2 * ↑x + 2))
Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean

Goal state before:
pp: x✝ y✝ x y : ℝ≥0
h : x ≤ y
⊢ ↑((x + y) / 2 - x) = dist x y / 2

Tactic:
nth_rw 2 [← add_halves x]

Goal state after:
x✝ y✝ x y : ℝ≥0
h : x ≤ y
⊢ ↑((x + y) / 2 - (x / 2 + x / 2)) = dist x y / 2
Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean

Goal state before:
pp: x y : ℝ≥0
⊢ x.agm y = y.agm x

Tactic:
by
  unfold agm
  conv_rhs =>
    enter [1, n]
    rw [agmSequences_comm]

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

Goal state before:
pp: x y k : ℝ≥0
⊢ ⨅ n, ((k * x).agmSequences (k * y) n).2 = k * ⨅ n, (x.agmSequences y n).2

Tactic:
mul_iInf

Goal state after:
x y k : ℝ≥0
⊢ ⨅ n, ((k * x).agmSequences (k * y) n).2 = ⨅ i, k * (x.agmSequences y i).2
Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy

Goal state before:
pp: ⊢ binEntropy 2⁻¹ = log 2

Tactic:
by norm_num [binEntropy]; simp; ring

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

Goal state before:
pp: case inr.inl
q : ℕ
hp₀✝ : 0 ≤ 1
hp₁ : 1 ≤ 1
hp₀ : 0 < 1
⊢ 0 ≤ qaryEntropy q 1

pp: case inr.inr
q : ℕ
p : ℝ
hp₀✝ : 0 ≤ p
hp₁✝ : p ≤ 1
hp₀ : 0 < p
hp₁ : p < 1
⊢ 0 ≤ qaryEntropy q p

Tactic:
· simpa [qaryEntropy, -Int.cast_sub] using log_intCast_nonneg _

Goal state after:
case inr.inr
q : ℕ
p : ℝ
hp₀✝ : 0 ≤ p
hp₁✝ : p ≤ 1
hp₀ : 0 < p
hp₁ : p < 1
⊢ 0 ≤ qaryEntropy q p
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Order

Goal state before:
pp: A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
p : ℝ≥0
hp : p ∈ Icc 0 1
⊢ Monotone fun a ↦ a ^ p

Tactic:
intro a b hab
  by_cases ha : 0 ≤ a
  · have hb : 0 ≤ b := ha.trans hab
    have hIcc : Icc (0 : ℝ≥0) 1 = Ioo 0 1 ∪ {0} ∪ {1} := by ext; simp
    rw [hIcc] at hp
    obtain (hp | hp) | hp := hp
    · exact monotoneOn_nnrpow_Ioo hp ha hb hab
    · simp_all [mem_singleton_iff]
    · simp_all [mem_singleton_iff, nnrpow_one a, nnrpow_one b]
  · have : a ^ p = 0 := cfcₙ_apply_of_not_predicate a ha
    simp [this]

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 : ℝ
inst✝ : CompleteSpace E
hf : LocallyIntegrableOn f (Ioi 0) volume
ha : 0 < a
hb : 0 < b
F : Filter ℝ
hpos : ∀ᶠ (t : ℝ) in F, 0 < t
V : E
huni : ∀ δ > 0, ∀ᶠ (t : ℝ) in F, ∀ x ∈ uIoc (a * t) (b * t), ‖f x - V‖ ≤ δ
δ : ℝ
hδ : δ > 0
C : ℝ := |log (b / a)|
hC_def : C = |log (b / a)|
δ' : ℝ := δ / (C + 1)
t : ℝ
⊢ 0 < t →
    (∀ x ∈ uIoc (a * t) (b * t), ‖f x - V‖ ≤ δ') → dist (∫ (x : ℝ) in a * t..b * t, x⁻¹ • f x) (log (b / a) • V) < δ

Tactic:
ht_pos

Goal state after:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
inst✝ : CompleteSpace E
hf : LocallyIntegrableOn f (Ioi 0) volume
ha : 0 < a
hb : 0 < b
F : Filter ℝ
hpos : ∀ᶠ (t : ℝ) in F, 0 < t
V : E
huni : ∀ δ > 0, ∀ᶠ (t : ℝ) in F, ∀ x ∈ uIoc (a * t) (b * t), ‖f x - V‖ ≤ δ
δ : ℝ
hδ : δ > 0
C : ℝ := |log (b / a)|
hC_def : C = |log (b / a)|
δ' : ℝ := δ / (C + 1)
t : ℝ
ht_pos : 0 < t
⊢ (∀ x ∈ uIoc (a * t) (b * t), ‖f x - V‖ ≤ δ') → dist (∫ (x : ℝ) in a * t..b * t, x⁻¹ • f x) (log (b / a) • V) < δ
Module: Mathlib.Analysis.SpecialFunctions.FrullaniIntegral

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
L : E
inst✝ : CompleteSpace E
hf : LocallyIntegrableOn f (Ioi 0) volume
ha : 0 < a
hb : 0 < b
hL : Tendsto f (𝓝[>] 0) (𝓝 L)
δ : ℝ
hδ : δ > 0
η : ℝ
hη : η > 0
hη_sub : ball 0 η ∩ Ioi 0 ⊆ {x | dist (f x) L < δ}
M : ℝ := max a b
hM_def : M = max a b
hM : 0 < M
t : ℝ
⊢ 0 < t → t ∈ Iio (η / M) → ∀ x ∈ uIoc (a * t) (b * t), ‖f x - L‖ ≤ δ

Tactic:
ht_pos

Goal state after:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
L : E
inst✝ : CompleteSpace E
hf : LocallyIntegrableOn f (Ioi 0) volume
ha : 0 < a
hb : 0 < b
hL : Tendsto f (𝓝[>] 0) (𝓝 L)
δ : ℝ
hδ : δ > 0
η : ℝ
hη : η > 0
hη_sub : ball 0 η ∩ Ioi 0 ⊆ {x | dist (f x) L < δ}
M : ℝ := max a b
hM_def : M = max a b
hM : 0 < M
t : ℝ
ht_pos : 0 < t
⊢ t ∈ Iio (η / M) → ∀ x ∈ uIoc (a * t) (b * t), ‖f x - L‖ ≤ δ
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)
u : ℝ → E := fun x ↦ x⁻¹ • f x
hint : ∀ {p q : ℝ}, 0 < p → 0 < q → IntervalIntegrable u volume p q
hsplit :
  ∀ {ε r : ℝ},
    0 < ε →
      0 < r →
        ∫ (x : ℝ) in ε..r, x⁻¹ • (f (a * x) - f (b * x)) =
          (∫ (x : ℝ) in a * ε..b * ε, u x) - ∫ (x : ℝ) in a * r..b * r, u x
⊢ (fun p ↦ ∫ (x : ℝ) in p.1..p.2, x⁻¹ • (f (a * x) - f (b * x))) =ᶠ[𝓝[>] 0 ×ˢ atTop] fun p ↦
    (∫ (x : ℝ) in a * p.1..b * p.1, u x) - ∫ (x : ℝ) in a * p.2..b * p.2, u x

Tactic:
filter_upwards [prod_mem_prod (eventually_nhdsWithin_of_forall fun _ h ↦ h)
      (eventually_atTop.2 ⟨1, fun _ h ↦ lt_of_lt_of_le one_pos h⟩)] with ⟨ε, r⟩ ⟨hε, hr⟩

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)
u : ℝ → E := fun x ↦ x⁻¹ • f x
hint : ∀ {p q : ℝ}, 0 < p → 0 < q → IntervalIntegrable u volume p q
hsplit :
  ∀ {ε r : ℝ},
    0 < ε →
      0 < r →
        ∫ (x : ℝ) in ε..r, x⁻¹ • (f (a * x) - f (b * x)) =
          (∫ (x : ℝ) in a * ε..b * ε, u x) - ∫ (x : ℝ) in a * r..b * r, u x
ε r : ℝ
hε : (ε, r).1 ∈ {x | x ∈ Ioi 0}
hr : (ε, r).2 ∈ {x | 0 < x}
⊢ ∫ (x : ℝ) in (ε, r).1..(ε, r).2, x⁻¹ • (f (a * x) - f (b * x)) =
    (∫ (x : ℝ) in a * (ε, r).1..b * (ε, r).1, u x) - ∫ (x : ℝ) in a * (ε, r).2..b * (ε, r).2, u x
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
ht' : ¬t = 0
hxt : t + x ≠ 0
⊢ t ^ p * (t⁻¹ - (t + x)⁻¹) = t ^ p * ((t + x - t) / (t * (t + x)))

Tactic:
by
          simp only [inv_eq_one_div]
          rw [div_sub_div _ _ (by lia) (by lia)]
          simp

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

Goal state before:
pp: s : ℂ
| s.Gammaℝ⁻¹

Tactic:
rw [Gammaℝ, mul_inv]

Goal state after:
s : ℂ
| (↑π ^ (-s / 2))⁻¹ * (Gamma (s / 2))⁻¹
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Deligne

Goal state before:
pp: s : ℂ
| s.Gammaℂ⁻¹

Tactic:
Gammaℂ,

Goal state after:
s : ℂ
| (2 * (2 * ↑π) ^ (-s) * Gamma s)⁻¹
Module: Mathlib.NumberTheory.Harmonic.GammaDeriv

Goal state before:
pp: f : ℂ → ℂ
g : ℝ → ℝ
g' s : ℝ
hf : DifferentiableAt ℂ f ↑s
hg : HasDerivAt g g' s
hfg : ∀ (s : ℝ), f ↑s = ↑(g s)
⊢ deriv f ↑s = ↑g'

Tactic:
← (funext hfg ▸ hf.hasDerivAt.comp_ofReal.deriv :)

Goal state after:
f : ℂ → ℂ
g : ℝ → ℝ
g' s : ℝ
hf : DifferentiableAt ℂ f ↑s
hg : HasDerivAt g g' s
hfg : ∀ (s : ℝ), f ↑s = ↑(g s)
⊢ deriv (fun x ↦ ↑(g x)) s = ↑g'
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
⊢ HasDerivAt f (-log ↑π / 2 / ↑√π) 1

Tactic:
have := ((hasDerivAt_neg (1 : ℂ)).div_const 2).const_cpow (c := π) (Or.inr (by simp))

Goal state after:
f : ℂ → ℂ := fun s ↦ ↑π ^ (-s / 2)
g : ℂ → ℂ := fun s ↦ Gamma (s / 2)
aux : ↑π ^ (1 / 2) = ↑√π
aux2 : ↑√π ≠ 0
this : HasDerivAt (fun x ↦ ↑π ^ (-x / 2)) (↑π ^ (-1 / 2) * log ↑π * (-1 / 2)) 1
⊢ HasDerivAt f (-log ↑π / 2 / ↑√π) 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
this : HasDerivAt (fun x ↦ ↑π ^ (-x / 2)) (↑π ^ (-1 / 2) * log ↑π * (-1 / 2)) 1
⊢ ↑π ^ (-1 / 2) * log ↑π * (-1 / 2) = -log ↑π / 2 / ↑√π

Tactic:
rw [mul_assoc, ← mul_div_assoc, mul_neg_one, neg_div, cpow_neg, ← div_eq_inv_mul, aux]

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 : ℕ
hb : 1 < b
n : ℕ
⊢ log b (↑b ^ (-↑n)) = -↑n

Tactic:
· rw [log_of_right_le_one _ (zpow_le_one_of_nonpos₀ (mod_cast hb.le) <|
      neg_nonpos.2 (Int.natCast_nonneg _)),
      zpow_neg, inv_inv, zpow_natCast, ← Nat.cast_pow, Nat.ceil_natCast, Nat.clog_pow _ _ hb]

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

Goal state before:
pp: b x : ℝ
⊢ logb |(-b)| x = logb |b| x

Tactic:
abs_neg

Goal state after:
b x : ℝ
⊢ logb |b| x = logb |b| x
Module: Mathlib.Analysis.SpecialFunctions.Log.Base

Goal state before:
pp: b x : ℝ
⊢ logb b |(-x)| = logb b |x|

Tactic:
abs_neg

Goal state after:
b x : ℝ
⊢ logb b |x| = logb b |x|
Module: Mathlib.Analysis.SpecialFunctions.Log.Base

Goal state before:
pp: case h.left
b : ℝ
b_pos : 0 < b
b_ne_one : b ≠ 1
x : ℝ
a✝ : x ∈ univ
⊢ -b ^ x ∈ Iio 0

Tactic:
simp only [Right.neg_neg_iff, Set.mem_Iio]

Goal state after:
case h.left
b : ℝ
b_pos : 0 < b
b_ne_one : b ≠ 1
x : ℝ
a✝ : x ∈ univ
⊢ 0 < b ^ x
Module: Mathlib.MeasureTheory.Measure.RegularityCompacts

Goal state before:
pp: α : Type u_1
inst✝⁵ : MeasurableSpace α
μ : Measure α
inst✝⁴ : TopologicalSpace α
inst✝³ : SecondCountableTopology α
inst✝² : IsCompletelyPseudoMetrizableSpace α
inst✝¹ : BorelSpace α
P : Measure α
inst✝ : IsFiniteMeasure P
⊢ P.InnerRegularCompactLTTop

Tactic:
refine ⟨Measure.InnerRegularWRT.measurableSet_of_isOpen ?_ ?_⟩

Goal state after:
case refine_1
α : Type u_1
inst✝⁵ : MeasurableSpace α
μ : Measure α
inst✝⁴ : TopologicalSpace α
inst✝³ : SecondCountableTopology α
inst✝² : IsCompletelyPseudoMetrizableSpace α
inst✝¹ : BorelSpace α
P : Measure α
inst✝ : IsFiniteMeasure P
⊢ P.InnerRegularWRT IsCompact IsOpen

case refine_2
α : Type u_1
inst✝⁵ : MeasurableSpace α
μ : Measure α
inst✝⁴ : TopologicalSpace α
inst✝³ : SecondCountableTopology α
inst✝² : IsCompletelyPseudoMetrizableSpace α
inst✝¹ : BorelSpace α
P : Measure α
inst✝ : IsFiniteMeasure P
⊢ ∀ ⦃s U : Set α⦄, IsCompact s → IsOpen U → IsCompact (s \ U)
Module: Mathlib.MeasureTheory.Measure.RegularityCompacts

Goal state before:
pp: case refine_1
α : Type u_1
inst✝⁵ : MeasurableSpace α
μ : Measure α
inst✝⁴ : TopologicalSpace α
inst✝³ : SecondCountableTopology α
inst✝² : IsCompletelyPseudoMetrizableSpace α
inst✝¹ : BorelSpace α
P : Measure α
inst✝ : IsFiniteMeasure P
⊢ P.InnerRegularWRT IsCompact IsOpen

Tactic:
exact innerRegularWRT_isCompact_isOpen P

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

Goal state before:
pp: n a b : ℕ
hb : b ≠ 0
⊢ a ≤ (a ^ (n + 1) / b ^ n + n * b) / (n + 1)

Tactic:
by
  rw [Nat.le_div_iff_mul_le (by positivity), Nat.mul_comm,
    ← Nat.add_mul_div_right _ _ (by positivity),
    Nat.le_div_iff_mul_le (by positivity)]
  #adaptation_note /-- Prior to nightly-2026-04-06, this was
  ```
  have := (Commute.all (b : ℤ) (a - b)).pow_add_mul_le_add_pow_of_sq_nonneg
    (by positivity) (sq_nonneg _) (sq_nonneg _) (by grind) (n + 1)
  grind
  ```
  -/
  zify
  have h := pow_add_mul_le_add_pow_of_sq_nonneg (a := (b : ℤ)) (b := (a : ℤ) - b)
    (ha := by positivity) (Hsq := by positivity) (Hsq' := by positivity) (H := by omega)
    (n := n + 1)
  rw [← sub_nonneg] at h ⊢
  convert! h using 1
  rw [pow_succ]; push_cast; ring1

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

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

Tactic:
by
  refine L.hasSumLocallyUniformly_aux (u := (10 * · * ‖·‖ ^ (-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
  · simpa using! show 0 ≤ 10 * r * (‖↑l‖ ^ 3)⁻¹ by positivity
  · exact weierstrassP_bound r hr s hs l h

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

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

Tactic:
weierstrassPExcept,

Goal state after:
L : PeriodPair
l₀ : ↥L.lattice
z : ℂ
⊢ ((∑' (l : ↥L.lattice), if ↑l = ↑l₀ then 0 else 1 / (z - ↑l) ^ 2 - 1 / ↑l ^ 2) +
      ∑' (i : ↥L.lattice), if ↑i = ↑l₀ then 1 / (z - ↑l₀) ^ 2 - 1 / ↑l₀ ^ 2 else 0) =
    ℘[L] z
Module: Mathlib.Analysis.SpecialFunctions.Pow.NthRootLemmas

Goal state before:
pp: n a : ℕ
⊢ (∃ x, x ^ n = a) ↔ n = 0 ∧ a = 1 ∨ n ≠ 0 ∧ n.nthRoot a ^ n = a

Tactic:
rcases eq_or_ne n 0 with rfl | _ <;> grind [exists_pow_eq_iff']

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

Goal state before:
pp: a : Multiset ℂ
this : ∀ i ∈ a, Tendsto (fun n ↦ i / ↑n + 1) atTop (𝓝 ((fun x ↦ 1) i))
⊢ Tendsto (fun n ↦ (Multiset.map (fun x ↦ x / ↑n + 1) a).prod) atTop (𝓝 1)

Tactic:
by
    simpa using tendsto_multiset_prod _ this

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

Goal state before:
pp: case zero
⊢ 1 ≤ rexp 1 / √2

Tactic:
grw [one_le_div (by positivity), Real.sqrt_le_left (by positivity), ← Real.add_one_le_exp]

Goal state after:
case zero
⊢ 2 ≤ (1 + 1) ^ 2
Module: Mathlib.Analysis.SpecialFunctions.Stirling

Goal state before:
pp: c : ℝ := 1 - 12⁻¹ - log 2 / 2
⊢ ∃ a, 0 < a ∧ ∀ (n : ℕ), a ≤ stirlingSeq (n + 1)

Tactic:
have h := log_stirlingSeq_bounded_by_constant

Goal state after:
c : ℝ := 1 - 12⁻¹ - log 2 / 2
h : ∀ (n : ℕ), 1 - 12⁻¹ - log 2 / 2 ≤ log (stirlingSeq (n + 1))
⊢ ∃ a, 0 < a ∧ ∀ (n : ℕ), a ≤ stirlingSeq (n + 1)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Orthogonality

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

Tactic:
simp_rw [Function.comp_apply]

Goal state after:
f : ℝ → ℝ
⊢ ∫ (x : ℝ) in 1..-1, f x * -√(1 - x ^ 2)⁻¹ = ∫ (x : ℝ) in 1..-1, f (cos (arccos x)) * -(1 / √(1 - x ^ 2))
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Orthogonality

Goal state before:
pp: f : ℝ → ℝ
x : ℝ
hx : x ∈ uIcc 1 (-1)
⊢ f x * -√(1 - x ^ 2)⁻¹ = f (cos (arccos x)) * -(1 / √(1 - x ^ 2))

Tactic:
by simp [cos_arccos (x := x) (by aesop) (by aesop)]

Goal state after:
Module: Mathlib.Data.Int.Fib.Basic

Goal state before:
pp: n : ℤ
⊢ fib (n + n) = fib n * (2 * fib (n + 1) - fib n)

Tactic:
fib_add

Goal state after:
n : ℤ
⊢ fib (n - 1) * fib n + fib n * fib (n + 1) = fib n * (2 * fib (n + 1) - fib n)
Module: Mathlib.Analysis.SumIntegralExpDecay

Goal state before:
pp: k : ℕ
M c : ℝ
hM : 0 ≤ M
hc : 0 < c
hk : 0 < ↑k + 1
key : ∫ (t : ℝ) in Ioi 0, t ^ (↑k + 1 - 1) * rexp (-(c * t)) = (1 / c) ^ (↑k + 1) * Gamma (↑k + 1)
hint : IntegrableOn (fun x ↦ x ^ (↑k + 1 - 1) * rexp (-(c * x))) (Ioi 0) volume
⊢ ∫ (x : ℝ) in Ioc 0 M, x ^ k * rexp (-(c * x)) = ∫ (x : ℝ) in Ioc 0 M, x ^ (↑k + 1 - 1) * rexp (-(c * x))

Tactic:
by
        simp [add_sub_cancel_right, rpow_natCast]

Goal state after:
Module: Mathlib.Analysis.SumIntegralComparisons

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

Tactic:
uIcc_of_le (by simp)

Goal state after:
x₀ : ℝ
a : ℕ
f : ℝ → ℝ
hf : AntitoneOn f (Icc x₀ (x₀ + ↑a))
k : ℕ
hk : k + 1 ≤ a
⊢ Icc (x₀ + ↑k) (x₀ + ↑(k + 1)) ⊆ Icc x₀ (x₀ + ↑a)
Module: Mathlib.Analysis.SpecificLimits.FloorPow

Goal state before:
pp: N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < c⁻¹ ^ 2
⊢ c ^ 2 / (1 - c⁻¹ ^ 2) ≤ c ^ 3 / (c - 1)

Tactic:
div_le_div_iff₀ _ (sub_pos.2 hc)

Goal state after:
N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < c⁻¹ ^ 2
⊢ c ^ 2 * (c - 1) ≤ c ^ 3 * (1 - c⁻¹ ^ 2)

N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < c⁻¹ ^ 2
⊢ 0 < 1 - c⁻¹ ^ 2
Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Square

Goal state before:
pp: sq₁ : Square (Type v)
sq₂ : Square (Type u)
e₁ : sq₁.X₁ ≃ sq₂.X₁
e₂ : sq₁.X₂ ≃ sq₂.X₂
e₃ : sq₁.X₃ ≃ sq₂.X₃
e₄ : sq₁.X₄ ≃ sq₂.X₄
comm₁₂ : ⇑e₂ ∘ ⇑(ConcreteCategory.hom sq₁.f₁₂) = ⇑(ConcreteCategory.hom sq₂.f₁₂) ∘ ⇑e₁
comm₁₃ : ⇑e₃ ∘ ⇑(ConcreteCategory.hom sq₁.f₁₃) = ⇑(ConcreteCategory.hom sq₂.f₁₃) ∘ ⇑e₁
comm₂₄ : ⇑e₄ ∘ ⇑(ConcreteCategory.hom sq₁.f₂₄) = ⇑(ConcreteCategory.hom sq₂.f₂₄) ∘ ⇑e₂
comm₃₄ : ⇑e₄ ∘ ⇑(ConcreteCategory.hom sq₁.f₃₄) = ⇑(ConcreteCategory.hom sq₂.f₃₄) ∘ ⇑e₃
⊢ sq₁.IsPullback ↔ sq₂.IsPullback

Tactic:
rw [← IsPullback.map_iff sq₁ uliftFunctor.{max u v},
      ← IsPullback.map_iff sq₂ uliftFunctor.{max u v}]
  refine iff_of_iso (Square.isoMk
    (((Equiv.trans Equiv.ulift e₁).trans Equiv.ulift.symm).toIso)
    (((Equiv.trans Equiv.ulift e₂).trans Equiv.ulift.symm).toIso)
    (((Equiv.trans Equiv.ulift e₃).trans Equiv.ulift.symm).toIso)
    (((Equiv.trans Equiv.ulift e₄).trans Equiv.ulift.symm).toIso)
    ?_ ?_ ?_ ?_)
  all_goals ext; apply ULift.down_injective
  · simpa [types_comp, uliftFunctor_map] using congrFun comm₁₂ _
  · simpa [types_comp, uliftFunctor_map] using congrFun comm₁₃ _
  · simpa [types_comp, uliftFunctor_map] using congrFun comm₂₄ _
  · simpa [types_comp, uliftFunctor_map] using congrFun comm₃₄ _

Goal state after: