mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.ODE.PicardLindelof

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E → E
tmin tmax : ℝ
t₀ : ↑(Icc tmin tmax)
x₀ x : E
a r L K : ℝ≥0
hf : IsPicardLindelof f t₀ x₀ a r L K
hx : x ∈ closedBall x₀ ↑r
α β : FunSpace t₀ x₀ r L
n : ℕ
hn :
  ∀ (t : ↑(Icc tmin tmax)),
    dist (((next hf hx)^[n] α).toFun t) (((next hf hx)^[n] β).toFun t) ≤ (↑K * |↑t - ↑t₀|) ^ n / ↑n ! * dist α β
t : ↑(Icc tmin tmax)
⊢ |↑K ^ (n + 1) * ∫ (x : ℝ) in ↑t₀..↑t, |x - ↑t₀| ^ n| / |↑n !| * |dist α β| ≤
    (↑K * |↑t - ↑t₀|) ^ (n + 1) / ↑(n + 1)! * dist α β

Tactic:
abs_mul,

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E → E
tmin tmax : ℝ
t₀ : ↑(Icc tmin tmax)
x₀ x : E
a r L K : ℝ≥0
hf : IsPicardLindelof f t₀ x₀ a r L K
hx : x ∈ closedBall x₀ ↑r
α β : FunSpace t₀ x₀ r L
n : ℕ
hn :
  ∀ (t : ↑(Icc tmin tmax)),
    dist (((next hf hx)^[n] α).toFun t) (((next hf hx)^[n] β).toFun t) ≤ (↑K * |↑t - ↑t₀|) ^ n / ↑n ! * dist α β
t : ↑(Icc tmin tmax)
⊢ |↑K ^ (n + 1)| * |∫ (x : ℝ) in ↑t₀..↑t, |x - ↑t₀| ^ n| / |↑n !| * |dist α β| ≤
    (↑K * |↑t - ↑t₀|) ^ (n + 1) / ↑(n + 1)! * dist α β
Module: Mathlib.Analysis.Polynomial.Basic

Goal state before:
pp: 𝕜 : Type u_1
inst✝³ : NormedField 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
hdeg : Q.degree < P.degree
hpos : 0 < P.leadingCoeff / Q.leadingCoeff
h : Q = 0
⊢ False

Tactic:
simp only [h, div_zero, leadingCoeff_zero] at hpos

Goal state after:
𝕜 : Type u_1
inst✝³ : NormedField 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
hdeg : Q.degree < P.degree
h : Q = 0
hpos : 0 < 0
⊢ False
Module: Mathlib.Analysis.Polynomial.Basic

Goal state before:
pp: P Q : ℤ[X]
mQ : Q.Monic
h : {a | eval a Q ∣ eval a P}.Infinite
⊢ Q ∣ P

Tactic:
have eqR := modByMonic_add_div P Q

Goal state after:
P Q : ℤ[X]
mQ : Q.Monic
h : {a | eval a Q ∣ eval a P}.Infinite
eqR : P %ₘ Q + Q * (P /ₘ Q) = P
⊢ Q ∣ P
Module: Mathlib.RingTheory.Polynomial.GaussNorm

Goal state before:
pp: c : ℝ
R : Type u_3
inst✝ : Ring R
v : AbsoluteValue R ℝ
hna : IsNonarchimedean ⇑v
hc : 0 < c
p q : R[X]
⊢ gaussNorm v c (p + q) ≤ gaussNorm v c p + gaussNorm v c q

Tactic:
grind [isNonarchimedean_gaussNorm v hna (le_of_lt hc) p q, gaussNorm_nonneg]

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

Goal state before:
pp: c : ℝ
R : Type u_3
inst✝ : Ring R
v : AbsoluteValue R ℝ
hna : IsNonarchimedean ⇑v
hc : 0 < c
p q : R[X]
⊢ gaussNorm v c (p + q) ≤ gaussNorm v c p + gaussNorm v c q

Tactic:
by
    grind [isNonarchimedean_gaussNorm v hna (le_of_lt hc) p q, gaussNorm_nonneg]

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

Goal state before:
pp: a : ℂ
ha : a ≠ 0
b : ℂ
⊢ (C a * X + C b).logMahlerMeasure = log ‖a‖ + log⁺ ‖a⁻¹ * b‖

Tactic:
by
  rw [show C a * X + C b = C a * (X + C (a⁻¹ * b)) by simp [mul_add, ← map_mul, ha],
    logMahlerMeasure_C_mul ha (X_add_C_ne_zero (a⁻¹ * b)), logMahlerMeasure_X_add_C]

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

Goal state before:
pp: α : Type u_5
S : Type u_6
inst✝¹ : LinearOrder S
inst✝ : AddCommMonoid α
g : α → S
ι : Type u_7
s : Finset ι
hs : s.Nonempty
f : ι → α
na : ∀ (a b : α), g (a + b) ≤ max (g a) (g b)
⊢ ∃ b ∈ s, g (∑ i ∈ s, f i) ≤ g (f b)

Tactic:
induction hs using Finset.Nonempty.cons_induction with

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

Goal state before:
pp: case hbc
p : ℂ[X]
⊢ 1 ≤ (Multiset.map (fun a ↦ max 1 ‖a‖) p.roots).prod

Tactic:
exact one_le_prod_max_one_norm_roots p

Goal state after:
Module: Mathlib.Analysis.Real.OfDigits

Goal state before:
pp: case e'_4
b : ℕ
digits : ℕ → Fin b
hb : 1 < ↑b
⊢ 1 = ∑' (n : ℕ), (↑b - 1) * (↑b)⁻¹ * (↑b)⁻¹ ^ n

Tactic:
tsum_mul_left,

Goal state after:
case e'_4
b : ℕ
digits : ℕ → Fin b
hb : 1 < ↑b
⊢ 1 = (↑b - 1) * (↑b)⁻¹ * ∑' (x : ℕ), (↑b)⁻¹ ^ x
Module: Mathlib.Analysis.Real.OfDigits

Goal state before:
pp: b : ℕ
x y : ℕ → Fin b
n : ℕ
hxy : ∀ i < n, x i = y i
this : ∑ i ∈ Finset.range n, ofDigitsTerm x i = ∑ i ∈ Finset.range n, ofDigitsTerm y i
⊢ |(↑b ^ n)⁻¹ * ((ofDigits fun i ↦ x (i + n)) - ofDigits fun i ↦ y (i + n))| ≤ (↑b ^ n)⁻¹

Tactic:
abs_mul,

Goal state after:
b : ℕ
x y : ℕ → Fin b
n : ℕ
hxy : ∀ i < n, x i = y i
this : ∑ i ∈ Finset.range n, ofDigitsTerm x i = ∑ i ∈ Finset.range n, ofDigitsTerm y i
⊢ |(↑b ^ n)⁻¹| * |(ofDigits fun i ↦ x (i + n)) - ofDigits fun i ↦ y (i + n)| ≤ (↑b ^ n)⁻¹
Module: Mathlib.Analysis.Real.OfDigits

Goal state before:
pp: b : ℕ
inst✝ : NeZero b
this : 1 < |↑b + 1|
⊢ ↑↑(Fin.last b) * ∑' (i : ℕ), (↑(b + 1))⁻¹ ^ (i + 1) = 1

Tactic:
rw [geom_series_succ _ (by simp [inv_lt_one_iff₀, this]),
      tsum_geometric_of_lt_one (by positivity) (by simp [inv_lt_one_iff₀, NeZero.pos b])]
    push_cast
    have : (b : ℝ) ≠ 0 := mod_cast NeZero.ne b
    field [*]

Goal state after:
Module: Mathlib.Analysis.Real.OfDigits

Goal state before:
pp: b : ℕ
hb : 1 < b
⊢ (ofDigits fun x ↦ ⟨b - 1, ⋯⟩) = 1

Tactic:
convert! ofDigits_const_last_eq_one (b - 1)

Goal state after:
case e'_1
b : ℕ
hb : 1 < b
⊢ b = b - 1 + 1

b : ℕ
hb : 1 < b
⊢ NeZero (b - 1)
Module: Mathlib.Analysis.Real.Hyperreal

Goal state before:
pp: x y : ℝ*
⊢ (-x).InfinitePos → ¬y.InfinitePos → (-(x + y)).InfinitePos

Tactic:
← @infiniteNeg_neg y,

Goal state after:
x y : ℝ*
⊢ (-x).InfinitePos → ¬(-y).InfiniteNeg → (-(x + y)).InfinitePos
Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean

Goal state before:
pp: case succ
x y : ℝ≥0
n : ℕ
ih : dist (x.agmSequences y n).1 (x.agmSequences y n).2 ≤ dist x y / 2 ^ (n + 1)
⊢ dist (x.agmSequences y n).1 (x.agmSequences y n).2 / 2 ≤ dist x y / (2 ^ (n + 1) * 2)

Tactic:
← div_div

Goal state after:
case succ
x y : ℝ≥0
n : ℕ
ih : dist (x.agmSequences y n).1 (x.agmSequences y n).2 ≤ dist x y / 2 ^ (n + 1)
⊢ dist (x.agmSequences y n).1 (x.agmSequences y n).2 / 2 ≤ dist x y / 2 ^ (n + 1) / 2
Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy

Goal state before:
pp: case refine_1
h : DifferentiableAt ℝ (fun p ↦ p * log p⁻¹ + (1 - p) * log (1 - p)⁻¹) 0
⊢ False

Tactic:
rw [DifferentiableAt.fun_add_iff_left] at h
    · simp [log_inv, mul_neg, ← neg_mul, ← negMulLog_def, differentiableAt_negMulLog_iff] at h
    · fun_prop (disch := simp)

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

Goal state before:
pp: case pos
p : ℝ
hp₀ : p ≠ 0
hp₁ : 1 - p ≠ 0
⊢ deriv negMulLog p + deriv (fun p ↦ (1 - p).negMulLog) p = log (1 - p) - log p

pp: case pos.hf
p : ℝ
hp₀ : p ≠ 0
hp₁ : 1 - p ≠ 0
⊢ DifferentiableAt ℝ negMulLog p

pp: case pos.hg
p : ℝ
hp₀ : p ≠ 0
hp₁ : 1 - p ≠ 0
⊢ DifferentiableAt ℝ (fun p ↦ (1 - p).negMulLog) p

Tactic:
deriv_comp_const_sub,

Goal state after:
case pos
p : ℝ
hp₀ : p ≠ 0
hp₁ : 1 - p ≠ 0
⊢ deriv negMulLog p + -deriv negMulLog (1 - p) = log (1 - p) - log p

case pos.hf
p : ℝ
hp₀ : p ≠ 0
hp₁ : 1 - p ≠ 0
⊢ DifferentiableAt ℝ negMulLog p

case pos.hg
p : ℝ
hp₀ : p ≠ 0
hp₁ : 1 - p ≠ 0
⊢ DifferentiableAt ℝ (fun p ↦ (1 - p).negMulLog) p
Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy

Goal state before:
pp: q : ℕ
tendstoBot : Tendsto (fun p ↦ log (↑q - 1) + log (1 - p) - log p) (𝓝[<] 1) atBot
a✝¹ : ℝ
a✝ : a✝¹ ∈ Ioo (1 - 2⁻¹) 1
⊢ a✝¹ ≠ 0

Tactic:
simp_all only [mem_Ioo, ne_eq]

Goal state after:
q : ℕ
tendstoBot : Tendsto (fun p ↦ log (↑q - 1) + log (1 - p) - log p) (𝓝[<] 1) atBot
a✝¹ : ℝ
a✝ : 1 - 2⁻¹ < a✝¹ ∧ a✝¹ < 1
⊢ ¬a✝¹ = 0
Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy

Goal state before:
pp: q : ℕ
tendstoBot : Tendsto (fun p ↦ log (↑q - 1) + log (1 - p) - log p) (𝓝[<] 1) atBot
a✝¹ : ℝ
a✝ : a✝¹ ∈ Ioo (1 - 2⁻¹) 1
⊢ a✝¹ ≠ 1

Tactic:
simp_all only [mem_Ioo, ne_eq]

Goal state after:
q : ℕ
tendstoBot : Tendsto (fun p ↦ log (↑q - 1) + log (1 - p) - log p) (𝓝[<] 1) atBot
a✝¹ : ℝ
a✝ : 1 - 2⁻¹ < a✝¹ ∧ a✝¹ < 1
⊢ ¬a✝¹ = 1
Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy

Goal state before:
pp: q : ℕ
tendstoTop : Tendsto (fun p ↦ log (↑q - 1) + log (1 - p) - log p) (𝓝[>] 0) atTop
a✝¹ : ℝ
a✝ : a✝¹ ∈ Ioo 0 2⁻¹
⊢ a✝¹ ≠ 0

Tactic:
simp_all only [mem_Ioo, ne_eq]

Goal state after:
q : ℕ
tendstoTop : Tendsto (fun p ↦ log (↑q - 1) + log (1 - p) - log p) (𝓝[>] 0) atTop
a✝¹ : ℝ
a✝ : 0 < a✝¹ ∧ a✝¹ < 2⁻¹
⊢ ¬a✝¹ = 0
Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy

Goal state before:
pp: q : ℕ
tendstoTop : Tendsto (fun p ↦ log (↑q - 1) + log (1 - p) - log p) (𝓝[>] 0) atTop
a✝¹ : ℝ
a✝ : a✝¹ ∈ Ioo 0 2⁻¹
⊢ a✝¹ ≠ 1

Tactic:
simp_all only [mem_Ioo, ne_eq]

Goal state after:
q : ℕ
tendstoTop : Tendsto (fun p ↦ log (↑q - 1) + log (1 - p) - log p) (𝓝[>] 0) atTop
a✝¹ : ℝ
a✝ : 0 < a✝¹ ∧ a✝¹ < 2⁻¹
⊢ ¬a✝¹ = 1
Module: Mathlib.Analysis.Real.Pi.Irrational

Goal state before:
pp: n : ℕ
x : ℝ
hx : -1 < x ∧ x ≤ 1
⊢ |(1 - x ^ 2) ^ n * cos (x * (π / 2))| ≤ 1

Tactic:
abs_mul,

Goal state after:
n : ℕ
x : ℝ
hx : -1 < x ∧ x ≤ 1
⊢ |(1 - x ^ 2) ^ n| * |cos (x * (π / 2))| ≤ 1
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Deligne

Goal state before:
pp: ⊢ Differentiable ℂ fun s ↦ s.Gammaℝ⁻¹

Tactic:
conv => enter [2, s]; rw [Gammaℝ, mul_inv]

Goal state after:
⊢ Differentiable ℂ fun s ↦ (↑π ^ (-s / 2))⁻¹ * (Gamma (s / 2))⁻¹
Module: Mathlib.NumberTheory.Harmonic.EulerMascheroni

Goal state before:
pp: ⊢ 1 / 2 < eulerMascheroniSeq 6

Tactic:
have : eulerMascheroniSeq 6 = 49 / 20 - log 7 := by
    rw [eulerMascheroniSeq]
    norm_num
  rw [this, lt_sub_iff_add_lt, ← lt_sub_iff_add_lt', log_lt_iff_lt_exp (by positivity)]
  refine lt_of_lt_of_le ?_ (Real.sum_le_exp_of_nonneg (by norm_num) 7)
  simp_rw [Finset.sum_range_succ, Nat.factorial_succ]
  norm_num

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

Goal state before:
pp: n : ℕ
f : ℝ → ℝ := log ∘ Gamma
this : deriv (log ∘ Gamma) (↑n + 1) = -γ + ↑(harmonic n)
⊢ deriv Gamma (↑n + 1) = ↑n ! * (-γ + ↑(harmonic n))

Tactic:
Function.comp_def,

Goal state after:
n : ℕ
f : ℝ → ℝ := log ∘ Gamma
this : deriv (fun x ↦ log (Gamma x)) (↑n + 1) = -γ + ↑(harmonic n)
⊢ deriv Gamma (↑n + 1) = ↑n ! * (-γ + ↑(harmonic n))
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation

Goal state before:
pp: p : ℝ
hp : p ∈ Ioo 0 1
⊢ -1 / (2 * (p - 1)) = 1 / 2 * -1 ^ (p - 1) / (p - 1)

Tactic:
← div_div

Goal state after:
p : ℝ
hp : p ∈ Ioo 0 1
⊢ -1 / 2 / (p - 1) = 1 / 2 * -1 ^ (p - 1) / (p - 1)
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Deligne

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

Tactic:
Gammaℝ_add_two h,

Goal state after:
case neg
s : ℂ
hs : ∀ (n : ℕ), s ≠ -↑n
h : s - 1 ≠ 0
h' : ∀ (n : ℕ), s - 1 ≠ -↑n
⊢ (s - 1).Gammaℂ * cos (↑π * (s - 1) / 2) * (s - 1).Gammaℝ⁻¹ =
    (s - 1).Gammaℂ * (s - 1) / 2 / ↑π * sin (↑π * s / 2) * ((s - 1).Gammaℝ * (s - 1) / 2 / ↑π)⁻¹
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)
⊢ t ^ (p - 1) • cfcₙ (fun x ↦ p.rpowIntegrand₀₁ 1 (t⁻¹ • x)) a = t ^ (p - 1) • cfcₙ (p.rpowIntegrand₀₁ 1) (t⁻¹ • a)

Tactic:
congr! 1
          refine cfcₙ_comp_smul (R := ℝ) t⁻¹ (fun x => rpowIntegrand₀₁ p 1 x) a ?_
          exact continuousOn_rpowIntegrand₀₁_Ici hp zero_lt_one |>.mono <|
            (h_mapsTo.mono_left hspec).image_subset

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)
derivUB : ∀ (n : ℕ), deriv f (↑n + 1) ≤ log (↑n + 1)
n : ℕ
hn : 0 < n
⊢ log ↑n - deriv f 1 ≤ ↑(harmonic n)

Tactic:
sub_le_iff_le_add',

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)
derivUB : ∀ (n : ℕ), deriv f (↑n + 1) ≤ log (↑n + 1)
n : ℕ
hn : 0 < n
⊢ log ↑n ≤ deriv f 1 + ↑(harmonic n)
Module: Mathlib.NumberTheory.Harmonic.GammaDeriv

Goal state before:
pp: case a
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)
derivUB : ∀ (n : ℕ), deriv f (↑n + 1) ≤ log (↑n + 1)
n : ℕ
⊢ ↑(harmonic n) - log (↑n + 1) ≤ -deriv f 1

Tactic:
sub_le_iff_le_add',

Goal state after:
case a
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)
derivUB : ∀ (n : ℕ), deriv f (↑n + 1) ≤ log (↑n + 1)
n : ℕ
⊢ ↑(harmonic n) ≤ log (↑n + 1) + -deriv f 1
Module: Mathlib.NumberTheory.Harmonic.GammaDeriv

Goal state before:
pp: case e_a.e_a.e_a
h_diff : ∀ {s : ℝ}, 0 < s → DifferentiableAt ℝ Gamma s
h_diff' : ∀ {s : ℝ}, 0 < s → DifferentiableAt ℝ (fun s ↦ Gamma (2 * s)) s
⊢ deriv Gamma 1 * 2 = -2 * γ

pp: case e_a.e_a.e_a.hh₂
h_diff : ∀ {s : ℝ}, 0 < s → DifferentiableAt ℝ Gamma s
h_diff' : ∀ {s : ℝ}, 0 < s → DifferentiableAt ℝ (fun s ↦ Gamma (2 * s)) s
⊢ DifferentiableAt ℝ Gamma (2 * (1 / 2))

pp: case e_a.e_a.e_a.hh
h_diff : ∀ {s : ℝ}, 0 < s → DifferentiableAt ℝ Gamma s
h_diff' : ∀ {s : ℝ}, 0 < s → DifferentiableAt ℝ (fun s ↦ Gamma (2 * s)) s
⊢ DifferentiableAt ℝ (fun s ↦ 2 * s) (1 / 2)

Tactic:
· rw [mul_comm, hasDerivAt_Gamma_one.deriv, mul_neg, neg_mul]

Goal state after:
case e_a.e_a.e_a.hh₂
h_diff : ∀ {s : ℝ}, 0 < s → DifferentiableAt ℝ Gamma s
h_diff' : ∀ {s : ℝ}, 0 < s → DifferentiableAt ℝ (fun s ↦ Gamma (2 * s)) s
⊢ DifferentiableAt ℝ Gamma (2 * (1 / 2))

case e_a.e_a.e_a.hh
h_diff : ∀ {s : ℝ}, 0 < s → DifferentiableAt ℝ Gamma s
h_diff' : ∀ {s : ℝ}, 0 < s → DifferentiableAt ℝ (fun s ↦ Gamma (2 * s)) s
⊢ DifferentiableAt ℝ (fun s ↦ 2 * s) (1 / 2)
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation

Goal state before:
pp: A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
p t : ℝ
hp : p ∈ Ioo 0 1
ht : 0 < t
⊢ ConcaveOn ℝ (Unitization.inr '' Ici 0) (cfc (p.rpowIntegrand₀₁ t))

Tactic:
refine ConcaveOn.subset (concaveOn_cfc_rpowIntegrand₀₁ hp ht) inr_map_Ici_zero ?_

Goal state after:
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
p t : ℝ
hp : p ∈ Ioo 0 1
ht : 0 < t
⊢ Convex ℝ (Unitization.inr '' Ici 0)
Module: Mathlib.Analysis.SpecialFunctions.MulExpNegMulSq

Goal state before:
pp: ε : ℝ
hε : 0 < ε
x : ℝ
heq : rexp (-(ε * x * x)) + x * (rexp (-(ε * x * x)) * (-2 * ε * x)) = rexp (-(ε * x * x)) * (1 - 2 * (ε * x * x))
⊢ |rexp (-(ε * x * x)) * (1 - 2 * (ε * x * x))| ≤ 1

Tactic:
abs_mul,

Goal state after:
ε : ℝ
hε : 0 < ε
x : ℝ
heq : rexp (-(ε * x * x)) + x * (rexp (-(ε * x * x)) * (-2 * ε * x)) = rexp (-(ε * x * x)) * (1 - 2 * (ε * x * x))
⊢ |rexp (-(ε * x * x))| * |1 - 2 * (ε * x * x)| ≤ 1
Module: Mathlib.Analysis.SpecialFunctions.MulExpNegMulSq

Goal state before:
pp: ε : ℝ
hε : 0 < ε
x : ℝ
heq : rexp (-(ε * x * x)) + x * (rexp (-(ε * x * x)) * (-2 * ε * x)) = rexp (-(ε * x * x)) * (1 - 2 * (ε * x * x))
⊢ rexp (-(ε * x * x)) * |1 - 2 * (ε * x * x)| ≤ 1

Tactic:
set y := ε * x * x with hy

Goal state after:
ε : ℝ
hε : 0 < ε
x : ℝ
y : ℝ := ε * x * x
heq : rexp (-y) + x * (rexp (-y) * (-2 * ε * x)) = rexp (-y) * (1 - 2 * y)
hy : y = ε * x * x
⊢ rexp (-y) * |1 - 2 * y| ≤ 1
Module: Mathlib.Analysis.SpecialFunctions.MulExpNegMulSq

Goal state before:
pp: ε : ℝ
hε : 0 < ε
x : ℝ
⊢ |(√ε)⁻¹ * mulExpNegMulSq 1 (√ε * x)| ≤ (√ε)⁻¹

Tactic:
abs_mul,

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

Goal state before:
pp: b x : ℝ
hb₀ : 0 < b
hb : b ≠ 1
⊢ ContinuousAt (logb b) x ↔ x ≠ 0

Tactic:
refine ⟨?_, continuousAt_logb⟩

Goal state after:
b x : ℝ
hb₀ : 0 < b
hb : b ≠ 1
⊢ ContinuousAt (logb b) x → x ≠ 0
Module: Mathlib.Analysis.SpecialFunctions.Log.Base

Goal state before:
pp: b : ℝ
n : ℕ
⊢ logb b ↑n = n.factorization.sum fun p t ↦ ↑t * logb b ↑p

Tactic:
simp only [logb, mul_div_assoc', log_nat_eq_sum_factorization n, Finsupp.sum, Finset.sum_div]

Goal state after:
Module: Mathlib.MeasureTheory.Measure.RegularityCompacts

Goal state before:
pp: case right
α : 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
this : Fact (μ A < ∞)
hA2' : (μ.restrict A) A ≠ ∞
hr' : r < (μ.restrict A) A
K : Set α
hK1 : K ⊆ A
hK2 : IsCompact K
hK3 : r < (μ.restrict A) K
⊢ r < μ K

Tactic:
rwa [Measure.restrict_eq_self μ hK1] at hK3

Goal state after:
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 →ᵇ ℝ
hε : 0 < ε
x : E
⊢ Tendsto (fun n ↦ (g * (1 + (↑n)⁻¹ • -(ε • g * g)) ^ n) x) atTop (𝓝 (ε.mulExpNegMulSq (g x)))

Tactic:
apply Tendsto.const_mul (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 < ε
x : E
⊢ Tendsto (fun x_1 ↦ ((1 + (↑x_1)⁻¹ • -(ε • g * g)) ^ x_1) x) atTop (𝓝 (rexp (-(ε * g x * g x))))
Module: Mathlib.MeasureTheory.Constructions.HaarToSphere

Goal state before:
pp: E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
hx : ‖x‖ = 1
ε : ℝ
hε : 0 < ε
hε2 : ε ≤ 2
y : E
hy : dist y ((1 - ε / 4) • x) < ε / 4
habs : |1 - ε / 4| = 1 - ε / 4
hy₀ : y ≠ 0
hy₁ : ‖y‖ < 1
u : E := ‖y‖⁻¹ • y
hu₁ : ‖u‖ = 1
⊢ dist u x < ε

Tactic:
have hyx := calc
    dist y x ≤ dist y ((1 - ε / 4) • x) + dist ((1 - ε / 4) • x) x := dist_triangle ..
    _ < ε / 4 + dist ((1 - ε / 4) • x) x := by gcongr
    _ = ε / 4 + ε / 4 := by simp [sub_smul, norm_smul, hx, abs_of_pos hε]
    _ = ε / 2 := by ring

Goal state after:
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
hx : ‖x‖ = 1
ε : ℝ
hε : 0 < ε
hε2 : ε ≤ 2
y : E
hy : dist y ((1 - ε / 4) • x) < ε / 4
habs : |1 - ε / 4| = 1 - ε / 4
hy₀ : y ≠ 0
hy₁ : ‖y‖ < 1
u : E := ‖y‖⁻¹ • y
hu₁ : ‖u‖ = 1
hyx : dist y x < ε / 2
⊢ dist u x < ε
Module: Mathlib.Analysis.SpecialFunctions.Pow.NthRootLemmas

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

Tactic:
← sub_nonneg

Goal state after:
n a b : ℕ
hb : b ≠ 0
h : 0 ≤ (↑b + (↑a - ↑b)) ^ (n + 1) - (↑b ^ (n + 1) + ↑(n + 1) * ↑b ^ (n + 1 - 1) * (↑a - ↑b))
⊢ 0 ≤ ↑a ^ (n + 1) + ↑n * ↑b * ↑b ^ n - (↑n + 1) * ↑a * ↑b ^ n
Module: Mathlib.Analysis.SpecialFunctions.RegularizedHypergeometric

Goal state before:
pp: a b : Multiset ℂ
h : a.card = b.card + 1
⊢ 1 ≤ (regularizedHGFunSeries a b).radius

Tactic:
by_cases! h' : ∀ j ∈ a, ∀ k : ℕ, j ≠ -k
  · grind
  · obtain ⟨j, hj, k, h'⟩ := h'
    rw [radius_regularizedHGFunSeries_eq_top_of_finite hj h']
    simp

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

Goal state before:
pp: ε : ℝ
E : Type u_2
inst✝⁶ : MeasurableSpace E
inst✝⁵ : PseudoEMetricSpace E
inst✝⁴ : BorelSpace E
inst✝³ : CompleteSpace E
inst✝² : SecondCountableTopology E
P P' : Measure E
inst✝¹ : IsFiniteMeasure P
inst✝ : IsFiniteMeasure P'
f : E →ᵇ ℝ
A : Subalgebra ℝ (E →ᵇ ℝ)
hA : (Subalgebra.map (toContinuousMapₐ ℝ) A).SeparatesPoints
heq : ∀ g ∈ A, ∫ (x : E), g x ∂P = ∫ (x : E), g x ∂P'
hε : 0 < ε
hPP' : ¬(P = 0 ∧ P' = 0)
const : ℝ := max (P.real Set.univ) (P'.real Set.univ)
pos_of_measure : 0 < const
KP : Set E
left✝¹ : KP ⊆ Set.univ
hKPco : IsCompact KP
hKPcl : IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] KP
KP' : Set E
left✝ : KP' ⊆ Set.univ
hKP'co : IsCompact KP'
hKP'cl : IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] KP'
K : Set E := KP ∪ KP'
hKco : IsCompact (KP ∪ KP')
hKcl : IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (KP ∪ KP')
hKP : P KPᶜ < ENNReal.ofReal ε
hKP' : P' KP'ᶜ < ENNReal.ofReal ε
hKPbound : P (KP ∪ KP')ᶜ < ↑ε.toNNReal
hKP'bound : P' (KP ∪ KP')ᶜ < ↑ε.toNNReal
g' : C(E, ℝ)
hg'approx : ∀ x ∈ KP ∪ KP', ‖g' x - ↑f x‖ < √ε * const⁻¹
hg'A : ∃ x ∈ A, (toContinuousMapₐ ℝ) x = g'
g : E →ᵇ ℝ := hg'A.choose
hgA : g ∈ A
hgapprox : ∀ x ∈ K, ‖g x - f x‖ < √ε * const⁻¹
line1 : |∫ (x : E), ε.mulExpNegMulSq (f x) ∂P - ∫ (x : E) in K, ε.mulExpNegMulSq (f x) ∂P| < √ε
line3 : |∫ (x : E) in K, ε.mulExpNegMulSq (g x) ∂P - ∫ (x : E), ε.mulExpNegMulSq (g x) ∂P| < √ε
line5 : |∫ (x : E), ε.mulExpNegMulSq (g x) ∂P' - ∫ (x : E) in K, ε.mulExpNegMulSq (g x) ∂P'| < √ε
line7 : |∫ (x : E) in K, ε.mulExpNegMulSq (f x) ∂P' - ∫ (x : E), ε.mulExpNegMulSq (f x) ∂P'| < √ε
line2 : |∫ (x : E) in K, ε.mulExpNegMulSq (f x) ∂P - ∫ (x : E) in K, ε.mulExpNegMulSq (g x) ∂P| ≤ √ε
line6 : |∫ (x : E) in K, ε.mulExpNegMulSq (g x) ∂P' - ∫ (x : E) in K, ε.mulExpNegMulSq (f x) ∂P'| ≤ √ε
⊢ ∫ (x : E), ε.mulExpNegMulSq (g x) ∂P = ∫ (x : E), ε.mulExpNegMulSq (g x) ∂P'

Tactic:
exact integral_mulExpNegMulSq_comp_eq hε heq hgA

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

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

Tactic:
by simp [weierstrassP]

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

Goal state before:
pp: L : PeriodPair
l : ↥L.lattice
⊢ ℘'[L] 0 = 0

Tactic:
L.derivWeierstrassP_zero

Goal state after:
L : PeriodPair
l : ↥L.lattice
⊢ 0 = 0
Module: Mathlib.Analysis.SpecialFunctions.Stirling

Goal state before:
pp: m : ℕ
f : ℕ → ℝ := fun k ↦ 1 / (2 * ↑k + 1) * ((1 / (2 * ↑(m + 1) + 1)) ^ 2) ^ k
⊢ HasSum (fun k ↦ f (k + 1)) (log (stirlingSeq (m + 1)) - log (stirlingSeq (m + 2)))

Tactic:
rw [hasSum_nat_add_iff]

Goal state after:
m : ℕ
f : ℕ → ℝ := fun k ↦ 1 / (2 * ↑k + 1) * ((1 / (2 * ↑(m + 1) + 1)) ^ 2) ^ k
⊢ HasSum f (log (stirlingSeq (m + 1)) - log (stirlingSeq (m + 2)) + ∑ i ∈ range 1, f i)
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.ContDiff

Goal state before:
pp: 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ₗᵢ
⊢ edist ((⇑g ∘ f) b) ((⇑g ∘ f) a) = ‖f b - f a‖ₑ

Tactic:
Function.comp_def,

Goal state after:
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ₗᵢ
⊢ edist ((fun x ↦ g (f x)) b) ((fun x ↦ g (f x)) a) = ‖f b - f a‖ₑ
Module: Mathlib.NumberTheory.Niven

Goal state before:
pp: q : ℚ
⊢ IsIntegral ℤ ((algebraMap ℝ ℂ) (2 * cos (↑q * π)))

Tactic:
simp [Complex.isIntegral_two_mul_cos_rat_mul_pi]

Goal state after: