mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.MetricSpace.Contracting

Goal state before:
pp: α : Type u_1
inst✝¹ : EMetricSpace α
K : ℝ≥0
f : α → α
inst✝ : CompleteSpace α
hf : ContractingWith K f
x : α
hx : edist x (f x) ≠ ∞
y : α
hy : edist y (f y) ≠ ∞
h : edist x y ≠ ∞
h' : edist (efixedPoint f hf x hx) (efixedPoint f hf y hy) = ∞
⊢ Metric.edistLtTopSetoid (efixedPoint f hf x hx) x

Tactic:
apply Setoid.symm'
    exact hf.edist_efixedPoint_lt_top hx

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

Goal state before:
pp: δ K ε : ℝ
⊢ gronwallBound δ K ε 0 = δ

Tactic:
by_cases hK : K = 0
  · simp only [gronwallBound, if_pos hK, mul_zero, add_zero]
  · simp only [gronwallBound, if_neg hK, mul_zero, exp_zero, sub_self, mul_one,
      add_zero]

Goal state after:
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)
t' : ℝ
ht'✝ : t' ∈ Ioc (min ↑t₀ ↑t) (max ↑t₀ ↑t)
ht' : t' ∈ Icc tmin tmax
⊢ ‖f t' (((next hf hx)^[n] α).compProj t') - f t' (((next hf hx)^[n] β).compProj t')‖ ≤
    ↑K ^ (n + 1) * |t' - ↑t₀| ^ n / ↑n ! * dist α β

Tactic:
← dist_eq_norm,

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)
t' : ℝ
ht'✝ : t' ∈ Ioc (min ↑t₀ ↑t) (max ↑t₀ ↑t)
ht' : t' ∈ Icc tmin tmax
⊢ dist (f t' (((next hf hx)^[n] α).compProj t')) (f t' (((next hf hx)^[n] β).compProj t')) ≤
    ↑K ^ (n + 1) * |t' - ↑t₀| ^ n / ↑n ! * dist α β
Module: Mathlib.Analysis.Polynomial.Order

Goal state before:
pp: P : ℝ[X]
x : ℝ
hroots : ∀ (y : ℝ), P.IsRoot y → x < y
hlc : 0 ≤ P.leadingCoeff
hroots' : ∀ (y : ℝ), (P.comp (-X)).IsRoot y → y < -x
h : Even P.natDegree
hlc' : 0 ≤ 1 * (P.comp (-X)).leadingCoeff
⊢ 0 < 1 * eval x P

Tactic:
rw [one_mul] at hlc' ⊢

Goal state after:
P : ℝ[X]
x : ℝ
hroots : ∀ (y : ℝ), P.IsRoot y → x < y
hlc : 0 ≤ P.leadingCoeff
hroots' : ∀ (y : ℝ), (P.comp (-X)).IsRoot y → y < -x
h : Even P.natDegree
hlc' : 0 ≤ (P.comp (-X)).leadingCoeff
⊢ 0 < eval x P
Module: Mathlib.Analysis.Polynomial.MahlerMeasure

Goal state before:
pp: a : ℂ
ha : a ≠ 0
p : ℂ[X]
hp : p ≠ 0
⊢ (C a).logMahlerMeasure + p.logMahlerMeasure = log ‖a‖ + p.logMahlerMeasure

Tactic:
logMahlerMeasure_const

Goal state after:
a : ℂ
ha : a ≠ 0
p : ℂ[X]
hp : p ≠ 0
⊢ log ‖a‖ + p.logMahlerMeasure = log ‖a‖ + p.logMahlerMeasure
Module: Mathlib.Analysis.Polynomial.MahlerMeasure

Goal state before:
pp: p : ℂ[X]
hp : ¬p = 0
this : 0 < p.sum fun x a ↦ ‖a‖
⊢ ({x | eval (circleMap 0 1 x) p = 0} ∩ Ico 0 (2 * π)).Finite

Tactic:
ofPred_inter_eq_sep

Goal state after:
p : ℂ[X]
hp : ¬p = 0
this : 0 < p.sum fun x a ↦ ‖a‖
⊢ {a | a ∈ Ico 0 (2 * π) ∧ eval (circleMap 0 1 a) p = 0}.Finite
Module: Mathlib.Analysis.Real.Pi.Bounds

Goal state before:
pp: n : ℕ
a : ℝ
h : 2 - ((a - 1 / 4 ^ n) / 2 ^ (n + 1)) ^ 2 ≤ (↑0 / ↑1).sqrtTwoAddSeries n
h₂ : 1 / 4 ^ n ≤ a
⊢ 2 - ((a - 1 / 4 ^ n) / 2 ^ (n + 1)) ^ 2 ≤ sqrtTwoAddSeries 0 n

pp: n : ℕ
a : ℝ
h : 2 - ((a - 1 / 4 ^ n) / 2 ^ (n + 1)) ^ 2 ≤ (↑0 / ↑1).sqrtTwoAddSeries n
h₂ : 1 / 4 ^ n ≤ a
⊢ 0 ≤ (a - 1 / 4 ^ n) / 2 ^ (n + 1)

pp: n : ℕ
a : ℝ
h : 2 - ((a - 1 / 4 ^ n) / 2 ^ (n + 1)) ^ 2 ≤ (↑0 / ↑1).sqrtTwoAddSeries n
h₂ : 1 / 4 ^ n ≤ a
⊢ 0 < 2 ^ (n + 1)

Tactic:
· rwa [Nat.cast_zero, zero_div] at h

Goal state after:
n : ℕ
a : ℝ
h : 2 - ((a - 1 / 4 ^ n) / 2 ^ (n + 1)) ^ 2 ≤ (↑0 / ↑1).sqrtTwoAddSeries n
h₂ : 1 / 4 ^ n ≤ a
⊢ 0 ≤ (a - 1 / 4 ^ n) / 2 ^ (n + 1)

n : ℕ
a : ℝ
h : 2 - ((a - 1 / 4 ^ n) / 2 ^ (n + 1)) ^ 2 ≤ (↑0 / ↑1).sqrtTwoAddSeries n
h₂ : 1 / 4 ^ n ≤ a
⊢ 0 < 2 ^ (n + 1)
Module: Mathlib.NumberTheory.Real.Irrational

Goal state before:
pp: n : ℕ
m : ℤ
hnpos : 0 < n
N : ℤ
D : ℕ
P : D ≠ 0
C : N.natAbs.Coprime D
hxr : ↑({ num := N, den := D, den_nz := P, reduced := C } ^ n) = ↑m
hv : ¬∃ y, ↑{ num := N, den := D, den_nz := P, reduced := C } = ↑y
c1 : ↑↑D ≠ 0
c2 : ↑↑D ^ n ≠ 0
⊢ False

Tactic:
rw [mk_eq_divInt, cast_pow, cast_divInt, div_pow, div_eq_iff_mul_eq c2, ← Int.cast_pow,
    ← Int.cast_pow, ← Int.cast_mul, Int.cast_inj] at hxr

Goal state after:
n : ℕ
m : ℤ
hnpos : 0 < n
N : ℤ
D : ℕ
P : D ≠ 0
C : N.natAbs.Coprime D
hxr : m * ↑D ^ n = N ^ n
hv : ¬∃ y, ↑{ num := N, den := D, den_nz := P, reduced := C } = ↑y
c1 : ↑↑D ≠ 0
c2 : ↑↑D ^ n ≠ 0
⊢ False
Module: Mathlib.Analysis.Polynomial.MahlerMeasure

Goal state before:
pp: A : Type u_2
inst✝ : NormedRing A
v : A →+* ℂ
hv : Isometry ⇑v
n : ℕ
p : A[X]
⊢ ‖p.coeff n‖ ≤ ↑(p.natDegree.choose n) * p.mapMahlerMeasure v

Tactic:
have hv_norm : ‖p.coeff n‖ = ‖v (p.coeff n)‖ :=
    (hv.norm_map_of_map_zero (map_zero _) _).symm

Goal state after:
A : Type u_2
inst✝ : NormedRing A
v : A →+* ℂ
hv : Isometry ⇑v
n : ℕ
p : A[X]
hv_norm : ‖p.coeff n‖ = ‖v (p.coeff n)‖
⊢ ‖p.coeff n‖ ≤ ↑(p.natDegree.choose n) * p.mapMahlerMeasure v
Module: Mathlib.Analysis.Real.Pi.Leibniz

Goal state before:
pp: l : ℝ
h : Tendsto (fun n ↦ ∑ i ∈ range n, (-1) ^ i / (2 * ↑i + 1)) atTop (𝓝 l)
abel : Tendsto (fun x ↦ ∑' (n : ℕ), (-1) ^ n / (2 * ↑n + 1) * x ^ n) (𝓝[<] 1) (𝓝 l)
m : 𝓝[<] 1 ≤ 𝓝 1
x✝¹ : ℝ
x✝ : x✝¹ ∈ Set.Ioo (-1) 1
⊢ x✝¹ ^ 2 < 1

Tactic:
sq_lt_one_iff_abs_lt_one,

Goal state after:
l : ℝ
h : Tendsto (fun n ↦ ∑ i ∈ range n, (-1) ^ i / (2 * ↑i + 1)) atTop (𝓝 l)
abel : Tendsto (fun x ↦ ∑' (n : ℕ), (-1) ^ n / (2 * ↑n + 1) * x ^ n) (𝓝[<] 1) (𝓝 l)
m : 𝓝[<] 1 ≤ 𝓝 1
x✝¹ : ℝ
x✝ : x✝¹ ∈ Set.Ioo (-1) 1
⊢ |x✝¹| < 1
Module: Mathlib.Analysis.SpecialFunctions.Arcosh

Goal state before:
pp: x : ℝ
hx : 1 ≤ x
⊢ cosh (arcosh x) = x

Tactic:
rw [arcosh, cosh_eq, exp_neg, exp_log (by positivity), add_sqrt_self_sq_sub_one_inv hx]

Goal state after:
x : ℝ
hx : 1 ≤ x
⊢ (x + √(x ^ 2 - 1) + (x - √(x ^ 2 - 1))) / 2 = x
Module: Mathlib.Analysis.SpecialFunctions.Arcosh

Goal state before:
pp: x : ℝ
hx : 0 ≤ x
⊢ arcosh (cosh x) = x

Tactic:
by
  rw [arcosh, ← exp_eq_exp, exp_log (by positivity), ← eq_sub_iff_add_eq', exp_sub_cosh,
    ← sq_eq_sq₀ (sqrt_nonneg _) (sinh_nonneg_iff.mpr hx), ← sinh_sq, sq_sqrt (pow_two_nonneg _)]

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

Goal state before:
pp: z : ℂ
hz : ‖z‖ < 1
this :
  HasSum (fun x ↦ -I / 2 * (((-1) ^ (2 * x.1 + ↑x.2 + 1) + 1) * (z * I) ^ (2 * x.1 + ↑x.2) / ↑(2 * x.1 + ↑x.2)))
    (-I / 2 * log ((1 + z * I) / (1 - z * I)))
k : ℕ
⊢ HasSum (fun c ↦ -I / 2 * (((-1) ^ (2 * k + ↑c + 1) + 1) * (z * I) ^ (2 * k + ↑c) / ↑(2 * k + ↑c)))
    ((-1) ^ k * z ^ (2 * k + 1) / ↑(2 * k + 1))

Tactic:
convert! hasSum_fintype (_ : Fin 2 → ℂ) using 1

Goal state after:
case e'_6
z : ℂ
hz : ‖z‖ < 1
this :
  HasSum (fun x ↦ -I / 2 * (((-1) ^ (2 * x.1 + ↑x.2 + 1) + 1) * (z * I) ^ (2 * x.1 + ↑x.2) / ↑(2 * x.1 + ↑x.2)))
    (-I / 2 * log ((1 + z * I) / (1 - z * I)))
k : ℕ
⊢ (-1) ^ k * z ^ (2 * k + 1) / ↑(2 * k + 1) =
    ∑ b, -I / 2 * (((-1) ^ (2 * k + ↑b + 1) + 1) * (z * I) ^ (2 * k + ↑b) / ↑(2 * k + ↑b))
Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean

Goal state before:
pp: x y : ℝ≥0
hx : 0 < x
hy : 0 < y
hn : x ≠ y
n : ℕ
p : ℝ≥0 := (x.agmSequences y n).1
q : ℝ≥0 := (x.agmSequences y n).2
ppos : 0 < p
⊢ p < sqrt (p * q)

Tactic:
have plq : p < q := agmSequences_fst_lt_snd_of_ne hn ..

Goal state after:
x y : ℝ≥0
hx : 0 < x
hy : 0 < y
hn : x ≠ y
n : ℕ
p : ℝ≥0 := (x.agmSequences y n).1
q : ℝ≥0 := (x.agmSequences y n).2
ppos : 0 < p
plq : p < q
⊢ p < sqrt (p * q)
Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean

Goal state before:
pp: x y : ℝ≥0
hn : x ≠ y
n : ℕ
p : ℝ≥0 := (x.agmSequences y n).1
q : ℝ≥0 := (x.agmSequences y n).2
⊢ (p + q) / 2 < q

Tactic:
have plq : p < q := agmSequences_fst_lt_snd_of_ne hn ..

Goal state after:
x y : ℝ≥0
hn : x ≠ y
n : ℕ
p : ℝ≥0 := (x.agmSequences y n).1
q : ℝ≥0 := (x.agmSequences y n).2
plq : p < q
⊢ (p + q) / 2 < q
Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy

Goal state before:
pp: p : ℝ
hp₀ : 0 ≤ p
hp₁ : p ≤ 1
⊢ 0 ≤ binEntropy p

Tactic:
obtain rfl | hp₀ := hp₀.eq_or_lt

Goal state after:
case inl
hp₀ : 0 ≤ 0
hp₁ : 0 ≤ 1
⊢ 0 ≤ binEntropy 0

case inr
p : ℝ
hp₀✝ : 0 ≤ p
hp₁ : p ≤ 1
hp₀ : 0 < p
⊢ 0 ≤ binEntropy p
Module: Mathlib.Analysis.SpecialFunctions.CompareExp

Goal state before:
pp: l : Filter ℂ
hl : IsExpCmpFilter l
a : ℂ
b : ℝ
hb : 0 < b
⊢ (fun z ↦ Real.exp (a.re * Real.log ‖z‖)) =o[l] fun x ↦ ‖cexp (↑b * x)‖

Tactic:
simp only [norm_exp, re_ofReal_mul, Real.isLittleO_exp_comp_exp_comp]
        refine (IsEquivalent.refl.sub_isLittleO ?_).symm.tendsto_atTop
          (hl.tendsto_re.const_mul_atTop hb)
        exact (hl.isLittleO_log_norm_re.const_mul_left _).const_mul_right hb.ne'

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

Goal state before:
pp: q : ℕ
p : ℝ
hp₀ : 0 ≤ p
hp₁ : p ≤ 1
⊢ 0 ≤ qaryEntropy q p

Tactic:
obtain rfl | hp₀ := hp₀.eq_or_lt

Goal state after:
case inl
q : ℕ
hp₀ : 0 ≤ 0
hp₁ : 0 ≤ 1
⊢ 0 ≤ qaryEntropy q 0

case inr
q : ℕ
p : ℝ
hp₀✝ : 0 ≤ p
hp₁ : p ≤ 1
hp₀ : 0 < p
⊢ 0 ≤ qaryEntropy q p
Module: Mathlib.Analysis.Real.Pi.Irrational

Goal state before:
pp: case refine_1
n : ℕ
x : ℝ
hx : x ∈ Ioc (-1) 1
⊢ |x| ≤ 1

Tactic:
abs_le

Goal state after:
case refine_1
n : ℕ
x : ℝ
hx : x ∈ Ioc (-1) 1
⊢ -1 ≤ x ∧ x ≤ 1
Module: Mathlib.Analysis.Real.Pi.Irrational

Goal state before:
pp: n : ℕ
x : ℝ
hx : -1 < x ∧ x ≤ 1
⊢ |1 - x ^ 2| ≤ 1

Tactic:
abs_le

Goal state after:
n : ℕ
x : ℝ
hx : -1 < x ∧ x ≤ 1
⊢ -1 ≤ 1 - x ^ 2 ∧ 1 - x ^ 2 ≤ 1
Module: Mathlib.Analysis.Real.Pi.Irrational

Goal state before:
pp: n : ℕ
⊢ I n (π / 2) ≤ 2

Tactic:
rw [← norm_of_nonneg I_pos.le]
  refine (norm_integral_le_of_norm_le_const ?_).trans (show (1 : ℝ) * _ ≤ _ by norm_num)
  intro x hx
  simp only [uIoc_of_le, neg_le_self_iff, zero_le_one, mem_Ioc] at hx
  rw [norm_eq_abs, abs_mul, abs_pow]
  refine mul_le_one₀ (pow_le_one₀ (abs_nonneg _) ?_) (abs_nonneg _) (abs_cos_le_one _)
  rw [abs_le]
  constructor <;> nlinarith

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

Goal state before:
pp: s : Set ℝ
hs : s ⊆ Ioi 0
hs' : IsCompact s
ε : ℝ
hε : 0 < ε
⊢ ∀ᶠ (n : ℝ) in 𝓝[>] 0, ∀ x ∈ s, (log x, n⁻¹ * (x ^ n - 1)) ∈ {p | dist p.1 p.2 ≤ ε}

Tactic:
let pbound : ℝ := ε / (sSup ((fun x => ‖log x‖ ^ 2) '' s) + 1)

Goal state after:
s : Set ℝ
hs : s ⊆ Ioi 0
hs' : IsCompact s
ε : ℝ
hε : 0 < ε
pbound : ℝ := ε / (sSup ((fun x ↦ ‖log x‖ ^ 2) '' s) + 1)
⊢ ∀ᶠ (n : ℝ) in 𝓝[>] 0, ∀ x ∈ s, (log x, n⁻¹ * (x ^ n - 1)) ∈ {p | dist p.1 p.2 ≤ ε}
Module: Mathlib.NumberTheory.Harmonic.EulerMascheroni

Goal state before:
pp: case refine_2
this : Tendsto eulerMascheroniSeq atTop (𝓝 (⨆ i, eulerMascheroniSeq i))
⊢ Tendsto eulerMascheroniSeq atTop (𝓝 eulerMascheroniConstant)

Tactic:
eulerMascheroniConstant,

Goal state after:
case refine_2
this : Tendsto eulerMascheroniSeq atTop (𝓝 (⨆ i, eulerMascheroniSeq i))
⊢ Tendsto eulerMascheroniSeq atTop (𝓝 (atTop.limUnder eulerMascheroniSeq))
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation

Goal state before:
pp: case inr
p x : ℝ
hp : p ∈ Ioo 0 1
hx✝ : 0 ≤ x
hx : 0 < x
⊢ ∫ (t : ℝ) in Ioi 0, ((fun x_1 ↦ p.rpowIntegrand₀₁ x_1 x) ∘ fun x_1 ↦ x * x_1) t * x =
    x ^ p * ∫ (t : ℝ) in Ioi 0, p.rpowIntegrand₀₁ t 1

Tactic:
have heqOn : EqOn (fun t => rpowIntegrand₀₁ p (x * t) x * x)
      (fun t => (rpowIntegrand₀₁ p t 1) * x ^ p) (Ioi 0) :=
    EqOn.mono Ioi_subset_Ici_self (rpowIntegrand₀₁_apply_mul_eqOn_Ici hp hx.le)

Goal state after:
case inr
p x : ℝ
hp : p ∈ Ioo 0 1
hx✝ : 0 ≤ x
hx : 0 < x
heqOn : EqOn (fun t ↦ p.rpowIntegrand₀₁ (x * t) x * x) (fun t ↦ p.rpowIntegrand₀₁ t 1 * x ^ p) (Ioi 0)
⊢ ∫ (t : ℝ) in Ioi 0, ((fun x_1 ↦ p.rpowIntegrand₀₁ x_1 x) ∘ fun x_1 ↦ x * x_1) t * x =
    x ^ p * ∫ (t : ℝ) in Ioi 0, p.rpowIntegrand₀₁ t 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
⊢ (1 - (s - 1)).Gammaℝ⁻¹ = s.Gammaℂ * sin (↑π * s / 2) * (s + 1).Gammaℝ⁻¹

Tactic:
inv_Gammaℝ_one_sub 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.Gammaℂ * sin (↑π * s / 2) * (s + 1).Gammaℝ⁻¹
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation

Goal state before:
pp: p : ℝ
hp : p ∈ Ioi 1
s : Set ℝ
hs : s ⊆ Ici 0
⊢ ContinuousOn (Function.uncurry p.rpowIntegrand₁₂) (Ioi 0 ×ˢ s)

Tactic:
unfold rpowIntegrand₁₂

Goal state after:
p : ℝ
hp : p ∈ Ioi 1
s : Set ℝ
hs : s ⊆ Ici 0
⊢ ContinuousOn (Function.uncurry fun t x ↦ t ^ (p - 1) * (t⁻¹ * x + t * (t + x)⁻¹ - 1)) (Ioi 0 ×ˢ s)
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation

Goal state before:
pp: p x : ℝ
hp : p ∈ Ioo 1 2
hx : 0 ≤ x
hmain : (fun x_1 ↦ p.rpowIntegrand₁₂ x_1 x) =ᵐ[volume.restrict (Ioi 0)] fun x_1 ↦ x * (p - 1).rpowIntegrand₀₁ x_1 x
⊢ x ^ p = (∫ (t : ℝ) in Ioi 0, (p - 1).rpowIntegrand₀₁ t 1)⁻¹ * ∫ (t : ℝ) in Ioi 0, p.rpowIntegrand₁₂ t x

Tactic:
rw [integral_congr_ae hmain, integral_const_mul_of_integrable
      (integrableOn_rpowIntegrand₀₁_Ioi (by grind) hx)]

Goal state after:
p x : ℝ
hp : p ∈ Ioo 1 2
hx : 0 ≤ x
hmain : (fun x_1 ↦ p.rpowIntegrand₁₂ x_1 x) =ᵐ[volume.restrict (Ioi 0)] fun x_1 ↦ x * (p - 1).rpowIntegrand₀₁ x_1 x
⊢ x ^ p =
    (∫ (t : ℝ) in Ioi 0, (p - 1).rpowIntegrand₀₁ t 1)⁻¹ * (x * ∫ (x_1 : ℝ) in Ioi 0, (p - 1).rpowIntegrand₀₁ x_1 x)
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation

Goal state before:
pp: A : Type u_1
inst✝⁹ : NonUnitalNormedRing A
inst✝⁸ : StarRing A
inst✝⁷ : NormedSpace ℝ A
inst✝⁶ : SMulCommClass ℝ A A
inst✝⁵ : IsScalarTower ℝ A A
inst✝⁴ : PartialOrder A
inst✝³ : StarOrderedRing A
inst✝² : NonnegSpectrumClass ℝ A
inst✝¹ : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝ : CompleteSpace A
p : ℝ≥0
hp : p ∈ Ioo 0 1
μ : Measure ℝ
hμ :
  ∀ x ∈ Ici 0,
    IntegrableOn (fun t ↦ (↑p).rpowIntegrand₀₁ t x) (Ioi 0) μ ∧ x ^ ↑p = ∫ (t : ℝ) in Ioi 0, (↑p).rpowIntegrand₀₁ t x ∂μ
a : A
ha : 0 ≤ a
a✝ : Nontrivial A
p_pos : 0 < ↑p
f : ℝ → ℝ → ℝ := fun t ↦ (↑p).rpowIntegrand₀₁ t
maxr : ℝ := sSup (quasispectrum ℝ a)
maxr_nonneg : 0 ≤ maxr
bound : ℝ → ℝ := fun t ↦ ‖f t maxr‖
⊢ ContinuousOn (Function.uncurry f) (Ioi 0 ×ˢ quasispectrum ℝ a)

Tactic:
refine continuousOn_rpowIntegrand₀₁_uncurry hp (quasispectrum ℝ a) ?_

Goal state after:
A : Type u_1
inst✝⁹ : NonUnitalNormedRing A
inst✝⁸ : StarRing A
inst✝⁷ : NormedSpace ℝ A
inst✝⁶ : SMulCommClass ℝ A A
inst✝⁵ : IsScalarTower ℝ A A
inst✝⁴ : PartialOrder A
inst✝³ : StarOrderedRing A
inst✝² : NonnegSpectrumClass ℝ A
inst✝¹ : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝ : CompleteSpace A
p : ℝ≥0
hp : p ∈ Ioo 0 1
μ : Measure ℝ
hμ :
  ∀ x ∈ Ici 0,
    IntegrableOn (fun t ↦ (↑p).rpowIntegrand₀₁ t x) (Ioi 0) μ ∧ x ^ ↑p = ∫ (t : ℝ) in Ioi 0, (↑p).rpowIntegrand₀₁ t x ∂μ
a : A
ha : 0 ≤ a
a✝ : Nontrivial A
p_pos : 0 < ↑p
f : ℝ → ℝ → ℝ := fun t ↦ (↑p).rpowIntegrand₀₁ t
maxr : ℝ := sSup (quasispectrum ℝ a)
maxr_nonneg : 0 ≤ maxr
bound : ℝ → ℝ := fun t ↦ ‖f t maxr‖
⊢ quasispectrum ℝ a ⊆ Ici 0
Module: Mathlib.Analysis.SpecialFunctions.Log.Base

Goal state before:
pp: a b : ℝ
h₁ : a ≠ 0
h₂ : b ≠ 0
c : ℝ
⊢ (logb (a / b) c)⁻¹ = (logb a c)⁻¹ - (logb b c)⁻¹

Tactic:
by
  simp_rw [inv_logb]; exact logb_div h₁ h₂

Goal state after:
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 ℝ (Ici 0) (cfcₙ (p.rpowIntegrand₀₁ t))

Tactic:
apply concaveOn_cfcₙ_of_concaveOn_cfc

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
⊢ ConcaveOn ℝ (Unitization.inr '' Ici 0) (cfc (p.rpowIntegrand₀₁ t))
Module: Mathlib.Analysis.SpecialFunctions.MulExpNegMulSqIntegral

Goal state before:
pp: case h
E : Type u_1
inst✝³ : TopologicalSpace E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
P : Measure E
inst✝ : IsFiniteMeasure P
ε : ℝ
g : E →ᵇ ℝ
hε : 0 < ε
N : ℕ
hgN : ε * (‖g‖ * ‖g‖) < ↑N
n : ℕ
hn : N ≤ n
hnpos : 0 < ↑n
x : E
⊢ |1 + -(ε * (g x * g x) / ↑n)| ≤ 1

Tactic:
abs_le

Goal state after:
case h
E : Type u_1
inst✝³ : TopologicalSpace E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
P : Measure E
inst✝ : IsFiniteMeasure P
ε : ℝ
g : E →ᵇ ℝ
hε : 0 < ε
N : ℕ
hgN : ε * (‖g‖ * ‖g‖) < ↑N
n : ℕ
hn : N ≤ n
hnpos : 0 < ↑n
x : E
⊢ -1 ≤ 1 + -(ε * (g x * g x) / ↑n) ∧ 1 + -(ε * (g x * g x) / ↑n) ≤ 1
Module: Mathlib.MeasureTheory.Constructions.HaarToSphere

Goal state before:
pp: E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : MeasurableSpace E
μ : Measure E
inst✝ : BorelSpace E
⊢ μ.toSphere univ = ↑(dim E) * μ (ball 0 1 \ {0})

Tactic:
μ.toSphere_apply' .univ,

Goal state after:
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : MeasurableSpace E
μ : Measure E
inst✝ : BorelSpace E
⊢ ↑(dim E) * μ (Ioo 0 1 • Subtype.val '' univ) = ↑(dim E) * μ (ball 0 1 \ {0})
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: case refine_2
L : PeriodPair
α β : ℚ
x✝ : α.den = 1 ∧ β.den = 1
h₁ : α.den = 1
h₂ : β.den = 1
⊢ ↑α * L.ω₁ + ↑β * L.ω₂ ∈ L.lattice

Tactic:
lift α to ℤ using h₁
    lift β to ℤ using h₂
    simp only [Rat.cast_intCast, ← zsmul_eq_mul]
    exact add_mem (Submodule.smul_mem _ _ L.ω₁_mem_lattice)
      (Submodule.smul_mem _ _ L.ω₂_mem_lattice)

Goal state after:
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
⊢ (fun x1 x2 ↦ x1 • x2) ‖y‖ u = y

Tactic:
by simp [u, hy₀]

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

Goal state before:
pp: case succ
n a fuel : ℕ
ih : ∀ {guess : ℕ}, a < (guess + 1) ^ (n + 2) → a < (go n a fuel guess + 1) ^ (n + 2)
guess : ℕ
hlt : a < (guess + 1) ^ (n + 2)
⊢ a < (go n a (fuel + 1) guess + 1) ^ (n + 2)

Tactic:
rw [go]
    split_ifs with h
    case pos =>
      rcases eq_or_ne guess 0 with rfl | hguess
      · grind
      · exact ih <| Nat.nthRoot.lt_pow_go_succ_aux hguess
    case neg =>
      assumption

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

Goal state before:
pp: case neg
L : PeriodPair
l₀ : ℂ
r : ℝ
hr : r > 0
s : ℂ
hs : ‖s‖ < r
l : ↥L.lattice
h : 2 * r ≤ ‖↑l‖
h✝ : ¬↑l = l₀
this✝ : s ≠ ↑l
this : l ≠ 0
⊢ ‖-2 / (s - ↑l) ^ 3‖ ≤ 16 * ‖l‖ ^ (-3)

Tactic:
simp only [Complex.norm_div, norm_neg, Complex.norm_ofNat, norm_pow]

Goal state after:
case neg
L : PeriodPair
l₀ : ℂ
r : ℝ
hr : r > 0
s : ℂ
hs : ‖s‖ < r
l : ↥L.lattice
h : 2 * r ≤ ‖↑l‖
h✝ : ¬↑l = l₀
this✝ : s ≠ ↑l
this : l ≠ 0
⊢ 2 / ‖s - ↑l‖ ^ 3 ≤ 16 * ‖l‖ ^ (-3)
Module: Mathlib.Analysis.SpecialFunctions.Stirling

Goal state before:
pp: n : ℕ
r : ℝ := (1 / (2 * (↑n + 1) + 1)) ^ 2
hr : r = (1 / (2 * (↑n + 1) + 1)) ^ 2
hr1 : r < 1
this : HasSum (fun j ↦ r ^ (j + 1) / 3) (1 / (12 * ↑(n + 1) * (↑(n + 1) + 1)))
j : ℕ
⊢ 3 ≤ 2 * (↑j + 1) + 1

Tactic:
norm_cast; grind

Goal state after:
Module: Mathlib.NumberTheory.Niven

Goal state before:
pp: case convert_2
θ : ℝ
hθ : ∃ r, θ = ↑r * π
hcos : ∃ q, sin θ = ↑q
⊢ ∃ q, cos (θ - π / 2) = ↑q

Tactic:
simpa [cos_sub_pi_div_two]

Goal state after:
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₀})ᶜ
⊢ ↑r ≤ (L.weierstrassPExceptSeries l₀ x).radius

Tactic:
apply FormalMultilinearSeries.le_radius_of_tendsto (l := 0)
    convert!
      tendsto_norm.comp
        (L.weierstrassPExceptSeries_hasSum l₀ (x + r) x ?_).summable.tendsto_atTop_zero using
      2 with i
    · simp
    · simp
    · 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.NumberTheory.ModularForms.EisensteinSeries.Summable

Goal state before:
pp: k : ℝ
hk : 2 < k
n : ℕ
hn : 0 < n
⊢ ↑(8 * n) * ↑n ^ (-k) ≤ 8 * (↑n ^ 1 * ↑n ^ (-k))

Tactic:
Real.rpow_one,

Goal state after:
k : ℝ
hk : 2 < k
n : ℕ
hn : 0 < n
⊢ ↑(8 * n) * ↑n ^ (-k) ≤ 8 * (↑n * ↑n ^ (-k))
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable

Goal state before:
pp: z : ℂ
c₁ c₂ : ℤ
⊢ (fun n ↦ ((↑c₁ * z - ↑n) * (↑c₂ * z + ↑n))⁻¹) =O[cofinite] fun n ↦ (|↑n| ^ 2)⁻¹

Tactic:
simpa [pow_two] using! (linear_inv_isBigO_right c₂ z).mul
      (linear_inv_isBigO_right c₁ z).comp_neg_int

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

Goal state before:
pp: case pos
L : PeriodPair
i : ℕ
hi₁ : i < 7
hi₂ : Odd i
⊢ iteratedDeriv i (L.relation * id ^ 6) 0 = 0

pp: case neg
L : PeriodPair
i : ℕ
hi₁ : i < 7
hi₂ : ¬Odd i
⊢ iteratedDeriv i (L.relation * id ^ 6) 0 = 0

Tactic:
· simpa [← CharZero.eq_neg_self_iff, hi₂, (show Even 6 by decide).neg_pow] using!
      (iteratedDeriv_comp_neg i (L.relation * id ^ 6) 0 :)

Goal state after:
case neg
L : PeriodPair
i : ℕ
hi₁ : i < 7
hi₂ : ¬Odd i
⊢ iteratedDeriv i (L.relation * id ^ 6) 0 = 0
Module: Mathlib.Data.Int.Fib.Basic

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

Tactic:
calc _ = fib (m + n) + fib (m + n + 1) := by grind [fib_add_two]
      _ = fib (m - 1) * fib n + fib m * fib (n + 1) + fib ((m + 1 : ℕ) + n) := by
        rw [fib_natCast_add]; grind
      _ = fib (m - 1) * fib n + fib m * fib (n + 1) + fib m * fib n +
          fib (m + 1) * fib (n + 1) := by rw [fib_natCast_add]; grind
      _ = _ := by grind [fib_add_two]

Goal state after:
Module: Mathlib.Analysis.VonNeumannAlgebra.Basic

Goal state before:
pp: H : Type u
inst✝² : NormedAddCommGroup H
inst✝¹ : InnerProductSpace ℂ H
inst✝ : CompleteSpace H
S : VonNeumannAlgebra H
z : H →L[ℂ] H
⊢ z ∈ S.commutant ↔ ∀ g ∈ S, g * z = z * g

Tactic:
rw [← SetLike.mem_coe, coe_commutant]
  rfl

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

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

Tactic:
simp [π]

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

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

Tactic:
simp [π]

Goal state after: