mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Polynomial.Basic

Goal state before:
pp: case neg.inr
𝕜 : Type u_1
inst✝³ : NormedField 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
hQ : Q ≠ 0
h✝ : Tendsto (fun x ↦ eval x P / eval x Q) atTop (𝓝 0)
hPQ : ¬P.leadingCoeff / Q.leadingCoeff = 0
h : ↑P.natDegree - ↑Q.natDegree < 0 ∧ 0 = 0
⊢ P.degree < Q.degree

Tactic:
rw [sub_lt_iff_lt_add, zero_add, Int.ofNat_lt] at h

Goal state after:
case neg.inr
𝕜 : Type u_1
inst✝³ : NormedField 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
hQ : Q ≠ 0
h✝ : Tendsto (fun x ↦ eval x P / eval x Q) atTop (𝓝 0)
hPQ : ¬P.leadingCoeff / Q.leadingCoeff = 0
h : P.natDegree < Q.natDegree ∧ 0 = 0
⊢ P.degree < Q.degree
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 i : ℕ
hi : i < n
⊢ dist ((next hf hx)^[i] α) ((next hf hx)^[i] (next hf hx α)) ≤
    (↑K * max (tmax - ↑t₀) (↑t₀ - tmin)) ^ i / ↑i ! * dist α (next hf hx α)

Tactic:
exact dist_iterate_next_iterate_next_le hf hx _ _ i

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

Goal state before:
pp: case neg
𝕜 : Type u_1
inst✝³ : NormedField 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
h : P.degree < Q.degree
hp : ¬P = 0
hq : Q ≠ 0
hPQ : ∀ᶠ (x : 𝕜) in atTop, eval x Q = 0 → eval x P = 0
⊢ (fun x ↦ eval x P) =o[atTop] fun x ↦ eval x Q

Tactic:
exact isLittleO_of_tendsto' hPQ (div_tendsto_atTop_zero_of_degree_lt P Q h)

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₀ : E
a r L K : ℝ≥0
inst✝ : CompleteSpace E
hf : IsPicardLindelof f t₀ x₀ a r L K
m : ℕ
C : ℝ≥0
h : ∀ (x : E) (hx : x ∈ closedBall x₀ ↑r), ContractingWith C (next hf hx)^[m]
L' : ℝ := (∑ i ∈ Finset.range m, (↑K * max (tmax - ↑t₀) (↑t₀ - tmin)) ^ i / ↑i !) * ↑(1 - C)⁻¹
hL' : 0 ≤ L'
x y : E
hx : x ∈ closedBall x₀ ↑r
hy : y ∈ closedBall x₀ ↑r
α β : FunSpace t₀ x₀ r L
hα : IsFixedPt (next hf hx) α
hβ : IsFixedPt (next hf hy) β
⊢ dist α β ≤ L' * dist x y

Tactic:
apply le_of_tendsto_of_tendsto' (b := Filter.atTop) _ _ <|
    dist_iterate_iterate_next_le_of_lipschitzWith hf hy α (h y hy).2

Goal state after:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
f : ℝ → E → E
tmin tmax : ℝ
t₀ : ↑(Icc tmin tmax)
x₀ : E
a r L K : ℝ≥0
inst✝ : CompleteSpace E
hf : IsPicardLindelof f t₀ x₀ a r L K
m : ℕ
C : ℝ≥0
h : ∀ (x : E) (hx : x ∈ closedBall x₀ ↑r), ContractingWith C (next hf hx)^[m]
L' : ℝ := ⋯
hL' : 0 ≤ L'
x y : E
hx : x ∈ closedBall x₀ ↑r
hy : y ∈ closedBall x₀ ↑r
α β : FunSpace t₀ x₀ r L
hα : IsFixedPt (next hf hx) α
hβ : IsFixedPt (next hf hy) β
⊢ Filter.Tendsto (fun x ↦ dist α ((next hf hy)^[m]^[x] α)) Filter.atTop (𝓝 (dist α β))

E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
f : ℝ → E → E
tmin tmax : ℝ
t₀ : ↑(Icc tmin tmax)
x₀ : E
a r L K : ℝ≥0
inst✝ : CompleteSpace E
hf : IsPicardLindelof f t₀ x₀ a r L K
m : ℕ
C : ℝ≥0
h : ∀ (x : E) (hx : x ∈ closedBall x₀ ↑r), ContractingWith C (next hf hx)^[m]
L' : ℝ := ⋯
hL' : 0 ≤ L'
x y : E
hx : x ∈ closedBall x₀ ↑r
hy : y ∈ closedBall x₀ ↑r
α β : FunSpace t₀ x₀ r L
hα : IsFixedPt (next hf hx) α
hβ : IsFixedPt (next hf hy) β
⊢ Filter.Tendsto
    (fun x ↦
      ((∑ i ∈ Finset.range m, (↑K * max (tmax - ↑t₀) (↑t₀ - tmin)) ^ i / ↑i !) * ∑ i ∈ Finset.range x, ↑C ^ i) *
        dist α (next hf hy α))
    Filter.atTop (𝓝 (L' * dist x y))
Module: Mathlib.RingTheory.Polynomial.GaussNorm

Goal state before:
pp: c✝ : ℝ
R✝ : Type u_3
inst✝¹ : Ring R✝
v✝ : AbsoluteValue R✝ ℝ
c : ℝ
R : Type u_3
inst✝ : Ring R
v : AbsoluteValue R ℝ
hna : IsNonarchimedean ⇑v
hc : 0 < c
p q : R[X]
hc0 : 0 ≤ c
i : ℕ
hi_p : gaussNorm v c p = v (p.coeff i) * c ^ i
hlt_p : ∀ j < i, v (p.coeff j) * c ^ j < gaussNorm v c p
j : ℕ
hj_q : gaussNorm v c q = v (q.coeff j) * c ^ j
hlt_q : ∀ j_1 < j, v (q.coeff j_1) * c ^ j_1 < gaussNorm v c q
hvpq : v (p.coeff i) ≠ 0 ∧ v (q.coeff j) ≠ 0
this✝ : v (p.coeff i) ≠ 0
this : v (q.coeff j) ≠ 0
⊢ v (p.coeff i) * c ^ i * (v (q.coeff j) * c ^ j) =
    v (∑ k ∈ range (i + j).succ, p.coeff (k, i + j - k).1 * q.coeff (k, i + j - k).2) * c ^ (i + j)

Tactic:
IsNonarchimedean.apply_sum_eq_of_lt hna (k := i) (by simp) (by simp)

Goal state after:
c✝ : ℝ
R✝ : Type u_3
inst✝¹ : Ring R✝
v✝ : AbsoluteValue R✝ ℝ
c : ℝ
R : Type u_3
inst✝ : Ring R
v : AbsoluteValue R ℝ
hna : IsNonarchimedean ⇑v
hc : 0 < c
p q : R[X]
hc0 : 0 ≤ c
i : ℕ
hi_p : gaussNorm v c p = v (p.coeff i) * c ^ i
hlt_p : ∀ j < i, v (p.coeff j) * c ^ j < gaussNorm v c p
j : ℕ
hj_q : gaussNorm v c q = v (q.coeff j) * c ^ j
hlt_q : ∀ j_1 < j, v (q.coeff j_1) * c ^ j_1 < gaussNorm v c q
hvpq : v (p.coeff i) ≠ 0 ∧ v (q.coeff j) ≠ 0
this✝ : v (p.coeff i) ≠ 0
this : v (q.coeff j) ≠ 0
⊢ v (p.coeff i) * c ^ i * (v (q.coeff j) * c ^ j) =
    v (p.coeff (i, i + j - i).1 * q.coeff (i, i + j - i).2) * c ^ (i + j)

c✝ : ℝ
R✝ : Type u_3
inst✝¹ : Ring R✝
v✝ : AbsoluteValue R✝ ℝ
c : ℝ
R : Type u_3
inst✝ : Ring R
v : AbsoluteValue R ℝ
hna : IsNonarchimedean ⇑v
hc : 0 < c
p q : R[X]
hc0 : 0 ≤ c
i : ℕ
hi_p : gaussNorm v c p = v (p.coeff i) * c ^ i
hlt_p : ∀ j < i, v (p.coeff j) * c ^ j < gaussNorm v c p
j : ℕ
hj_q : gaussNorm v c q = v (q.coeff j) * c ^ j
hlt_q : ∀ j_1 < j, v (q.coeff j_1) * c ^ j_1 < gaussNorm v c q
hvpq : v (p.coeff i) ≠ 0 ∧ v (q.coeff j) ≠ 0
this✝ : v (p.coeff i) ≠ 0
this : v (q.coeff j) ≠ 0
⊢ ∀ j_1 ∈ range (i + j).succ,
    j_1 ≠ i →
      v (p.coeff (j_1, i + j - j_1).1 * q.coeff (j_1, i + j - j_1).2) <
        v (p.coeff (i, i + j - i).1 * q.coeff (i, i + j - i).2)
Module: Mathlib.Analysis.ODE.PicardLindelof

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace 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
hα : IsFixedPt (FunSpace.next hf hx) α
t : ℝ
ht : t ∈ Icc tmin tmax
⊢ (FunSpace.next hf hx α).compProj t = picard f (↑t₀) x (FunSpace.next hf hx α).compProj t

Tactic:
rw [FunSpace.compProj_apply, FunSpace.next_apply, hα, projIcc_of_mem _ ht]

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

Goal state before:
pp: R : Type u_1
σ : Type u_2
v : R → ℝ
inst✝¹ : Ring R
inst✝ : DecidableEq σ
f g : MvPowerSeries σ R
i j : σ →₀ ℕ
vna : IsNonarchimedean v
vMulEq : ∀ (a b : R), v (a * b) = v a * v b
vNeg : ∀ (a : R), v a = v (-a)
hdom :
  ∀ p ∈ Finset.antidiagonal (i + j), p ≠ (i, j) → v ((coeff p.1) f * (coeff p.2) g) < v ((coeff i) f) * v ((coeff j) g)
⊢ v ((coeff (i + j)) (f * g)) = v ((coeff i) f * (coeff j) g)

Tactic:
rw [← vMulEq] at hdom

Goal state after:
R : Type u_1
σ : Type u_2
v : R → ℝ
inst✝¹ : Ring R
inst✝ : DecidableEq σ
f g : MvPowerSeries σ R
i j : σ →₀ ℕ
vna : IsNonarchimedean v
vMulEq : ∀ (a b : R), v (a * b) = v a * v b
vNeg : ∀ (a : R), v a = v (-a)
hdom : ∀ p ∈ Finset.antidiagonal (i + j), p ≠ (i, j) → v ((coeff p.1) f * (coeff p.2) g) < v ((coeff i) f * (coeff j) g)
⊢ v ((coeff (i + j)) (f * g)) = v ((coeff i) f * (coeff j) g)
Module: Mathlib.Analysis.Polynomial.MahlerMeasure

Goal state before:
pp: a : ℂ
ha : a ≠ 0
b : ℂ
⊢ ‖a‖₊ * max 1 ‖a⁻¹ * b‖₊ = max ‖a‖₊ ‖b‖₊

Tactic:
simp [mul_max, ha]

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

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

Tactic:
cast_intCast

Goal state after:
n : ℕ
m : ℤ
hnpos : 0 < n
N : ℤ
P : 1 ≠ 0
C : N.natAbs.Coprime 1
hxr : m * ↑1 ^ n = N ^ n
hv : ¬∃ y, ↑{ num := N, den_nz := P, reduced := C } = ↑y
c1 : ↑↑1 ≠ 0
c2 : ↑↑1 ^ n ≠ 0
hdivn : 1 ∣ N.natAbs
⊢ ↑N = ↑N
Module: Mathlib.NumberTheory.Real.Irrational

Goal state before:
pp: case inr
n : ℕ
m : ℤ
hm : m ≠ 0
p : ℕ
hp : Fact (Nat.Prime p)
hv : multiplicity (↑p) m % n ≠ 0
hnpos : n > 0
y : ℤ
hxr : ↑y ^ n = ↑m
⊢ False

Tactic:
rw [← Int.cast_pow, Int.cast_inj] at hxr

Goal state after:
case inr
n : ℕ
m : ℤ
hm : m ≠ 0
p : ℕ
hp : Fact (Nat.Prime p)
hv : multiplicity (↑p) m % n ≠ 0
hnpos : n > 0
y : ℤ
hxr : y ^ n = m
⊢ False
Module: Mathlib.NumberTheory.Real.Irrational

Goal state before:
pp: x : ℝ
m : ℤ
h : Irrational (x * ↑m)
⊢ Irrational (x * ↑↑m)

Tactic:
cast_intCast

Goal state after:
x : ℝ
m : ℤ
h : Irrational (x * ↑m)
⊢ Irrational (x * ↑m)
Module: Mathlib.NumberTheory.Real.Irrational

Goal state before:
pp: x : ℝ
m : ℤ
h : Irrational (↑m * x)
⊢ Irrational (↑↑m * x)

Tactic:
cast_intCast

Goal state after:
x : ℝ
m : ℤ
h : Irrational (↑m * x)
⊢ Irrational (↑m * x)
Module: Mathlib.Analysis.Real.Hyperreal

Goal state before:
pp: x : ℝ*
r : ℝ
hxr : x.IsSt r
f : ℝ → ℝ
hf : ContinuousAt f r
⊢ IsSt (Germ.map f x) (f r)

Tactic:
rcases ofSeq_surjective x with ⟨g, rfl⟩
  exact isSt_ofSeq_iff_tendsto.2 <| hf.tendsto.comp (isSt_ofSeq_iff_tendsto.1 hxr)

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

Goal state before:
pp: x y : ℝ*
hx : x.InfinitePos
hy₁ : ¬y.Infinitesimal
hy₂ : 0 < y
r : ℝ
hy₁' : ∃ x, ¬(0 < x → -↑x < y ∧ y < ↑x)
r₁ : ℝ
hy₁'' : ¬(0 < r₁ → -↑r₁ < y ∧ y < ↑r₁)
hyr : 0 < r₁ ∧ ↑r₁ ≤ y
⊢ ↑r < x * y

Tactic:
rw [← div_mul_cancel₀ r (ne_of_gt hyr.1), coe_mul]

Goal state after:
x y : ℝ*
hx : x.InfinitePos
hy₁ : ¬y.Infinitesimal
hy₂ : 0 < y
r : ℝ
hy₁' : ∃ x, ¬(0 < x → -↑x < y ∧ y < ↑x)
r₁ : ℝ
hy₁'' : ¬(0 < r₁ → -↑r₁ < y ∧ y < ↑r₁)
hyr : 0 < r₁ ∧ ↑r₁ ≤ y
⊢ ↑(r / r₁) * ↑r₁ < x * y
Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean

Goal state before:
pp: x y : ℝ≥0
h : x ≠ y
hl : y < x
key : 0 < x * (x - y) - y * (x - y)
⊢ sqrt (x * y) < (x + y) / 2

Tactic:
mul_tsub,

Goal state after:
x y : ℝ≥0
h : x ≠ y
hl : y < x
key : 0 < x * x - x * y - y * (x - y)
⊢ sqrt (x * y) < (x + y) / 2
Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean

Goal state before:
pp: x y : ℝ≥0
h : x ≠ y
hl : y < x
key : 0 < x * x - x * y - y * (x - y)
⊢ sqrt (x * y) < (x + y) / 2

Tactic:
mul_tsub,

Goal state after:
x y : ℝ≥0
h : x ≠ y
hl : y < x
key : 0 < x * x - x * y - (y * x - y * y)
⊢ sqrt (x * y) < (x + y) / 2
Module: Mathlib.Analysis.SpecialFunctions.Artanh

Goal state before:
pp: x : ℝ
hx : 0 ≤ x
⊢ 0 ≤ artanh x

Tactic:
by_cases x < 1
  case pos =>
    rw [← artanh_zero, artanh_le_artanh_iff (by grind) (by grind)]
    exact hx
  case neg => grind [artanh_eq_zero_iff]

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

Goal state before:
pp: q : ℕ
qLe2 : 2 ≤ q
p1 : ℝ
hp1 : p1 ∈ Icc 0 (1 - 1 / ↑q)
p2 : ℝ
hp2 : p2 ∈ Icc 0 (1 - 1 / ↑q)
p1le2 : p1 < p2
p : ℝ
this✝ : 2 ≤ ↑q
zero_le_qinv : 0 < (↑q)⁻¹
this : 0 < 1 - p
hp : 0 < p ∧ p < 1 - (↑q)⁻¹
⊢ 0 < log (↑q - 1) + log (1 - p) - log p

Tactic:
simp only [sub_pos, gt_iff_lt]
      rw [← log_mul (by linarith) (by linarith)]
      apply Real.strictMonoOn_log (mem_Ioi.mpr hp.1)
      · simp_all only [mem_Ioi, mul_pos_iff_of_pos_left, show 0 < (q : ℝ) - 1 by linarith]
      · have qpos : 0 < (q : ℝ) := by positivity
        have : q * p < q - 1 := by
          convert! mul_lt_mul_of_pos_left hp.2 qpos using 1
          simp only [mul_sub, mul_one, isUnit_iff_ne_zero, ne_eq, ne_of_gt qpos, not_false_eq_true,
            IsUnit.mul_inv_cancel]
        linarith

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

Goal state before:
pp: case h
h1 : eulerMascheroniSeq' 6 = 49 / 20 - log 6
this : rexp (107 / 60) < 2.7182818286 ^ (107 / 60)
⊢ 60 ≠ 0

pp: case hx
h1 : eulerMascheroniSeq' 6 = 49 / 20 - log 6
this : rexp (107 / 60) < 2.7182818286 ^ (107 / 60)
⊢ 0 ≤ 2.7182818286

pp: case hx
h1 : eulerMascheroniSeq' 6 = 49 / 20 - log 6
this : rexp (107 / 60) < 2.7182818286 ^ (107 / 60)
⊢ 0 ≤ 2.7182818286 ^ (107 / 60)

pp: case hy
h1 : eulerMascheroniSeq' 6 = 49 / 20 - log 6
this : rexp (107 / 60) < 2.7182818286 ^ (107 / 60)
⊢ 0 ≤ 6

pp: case hz
h1 : eulerMascheroniSeq' 6 = 49 / 20 - log 6
this : rexp (107 / 60) < 2.7182818286 ^ (107 / 60)
⊢ 0 < 60

Tactic:
all_goals positivity

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

Goal state before:
pp: ⊢ digamma 1 = -↑Real.eulerMascheroniConstant

Tactic:
by
  rw [digamma_def, logDeriv_apply, hasDerivAt_Gamma_one.deriv, Gamma_one, div_one]

Goal state after:
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
x : ℝ
hx : x ∈ Ici 0
⊢ (fun x ↦ t⁻¹ • x) x ∈ Ici 0

Tactic:
simp only [mem_Ici, smul_eq_mul] at hx ⊢

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
p t : ℝ
hp : p ∈ Ioo 0 1
ht : 0 < t
a : A
ha : 0 ≤ a
hspec : quasispectrum ℝ a ⊆ Ici 0
x : ℝ
hx : 0 ≤ x
⊢ 0 ≤ t⁻¹ * x
Module: Mathlib.Analysis.SpecialFunctions.Log.Base

Goal state before:
pp: case a
b x : ℝ
b_pos : 0 < b
b_ne_one : b ≠ 1
hx : x ≠ 0
⊢ |x| ∈ Ioi 0

pp: case a
b x : ℝ
b_pos : 0 < b
b_ne_one : b ≠ 1
hx : x ≠ 0
⊢ log (b ^ logb b x) = log |x|

Tactic:
· simp only [abs_pos, mem_Ioi, Ne, hx, not_false_iff]

Goal state after:
case a
b x : ℝ
b_pos : 0 < b
b_ne_one : b ≠ 1
hx : x ≠ 0
⊢ log (b ^ logb b x) = log |x|
Module: Mathlib.Data.Int.Log

Goal state before:
pp: R : Type u_1
inst✝³ : Semifield R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorSemiring R
b n : ℕ
⊢ clog b ↑n = ↑(Nat.clog b n)

Tactic:
rcases n with - | n
  · simp [clog_of_right_le_one]
  · rw [clog_of_one_le_right, (Nat.ceil_eq_iff (Nat.succ_ne_zero n)).mpr] <;> simp

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

Goal state before:
pp: case hb.refine_1
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
p t : ℝ
hp : p ∈ Ioo 0 1
ht : 0 < t
a : A
ha : 0 ≤ a
b : A
hb : 0 ≤ b
hab : a ≤ b
⊢ 0 ≤ t⁻¹ • a

pp: case hb.refine_2
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
p t : ℝ
hp : p ∈ Ioo 0 1
ht : 0 < t
a : A
ha : 0 ≤ a
b : A
hb : 0 ≤ b
hab : a ≤ b
⊢ 0 ≤ t⁻¹ • b

Tactic:
all_goals positivity

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

Goal state before:
pp: case inl
b : ℝ
hb : 1 < b
hx : 0 ≤ 0
⊢ logb b 0 ≤ 0 ↔ 0 ≤ 1

Tactic:
simp [zero_le_one]

Goal state after:
Module: Mathlib.MeasureTheory.Integral.BoundedContinuousFunction

Goal state before:
pp: X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : MeasurableSpace X
μ : Measure X
inst✝ : IsFiniteMeasure μ
f : X →ᵇ ℝ≥0
⊢ ∃ c, ∀ (x : X), ↑(f x) ≤ ↑c

Tactic:
refine ⟨nndist f 0, fun x ↦ ?_⟩

Goal state after:
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : MeasurableSpace X
μ : Measure X
inst✝ : IsFiniteMeasure μ
f : X →ᵇ ℝ≥0
x : X
⊢ ↑(f x) ≤ ↑(nndist f 0)
Module: Mathlib.Analysis.SpecialFunctions.Pochhammer

Goal state before:
pp: case inr
n : ℕ
h✝ : n > 0
⊢ ConvexOn ℝ (Set.Ici (↑n - 1)) fun x ↦ Polynomial.eval x (descPochhammer ℝ n)

Tactic:
· apply MonotoneOn.convexOn_of_deriv (convex_Ici (n - 1 : ℝ))
      continuous_descPochhammer_eval.continuousOn
      differentiable_descPochhammer_eval.differentiableOn
    rw [interior_Ici]
    exact monotoneOn_deriv_descPochhammer_eval n

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)
⊢ 0 < const

Tactic:
rw [not_and_or] at hPP'

Goal state after:
ε : ℝ
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)
⊢ 0 < const
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
inst✝¹ : FiniteDimensional ℝ E
inst✝ : μ.IsAddHaarMeasure
⊢ μ.toSphere univ = ↑(dim E) * μ (ball 0 1)

Tactic:
nontriviality E

Goal state after:
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
μ : Measure E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
inst✝ : μ.IsAddHaarMeasure
a✝ : Nontrivial E
⊢ μ.toSphere univ = ↑(dim E) * μ (ball 0 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
inst✝¹ : FiniteDimensional ℝ E
inst✝ : μ.IsAddHaarMeasure
⊢ MeasurePreserving (⇑(homeomorphUnitSphereProd E)) (comap Subtype.val μ) (μ.toSphere.prod (volumeIoiPow (dim E - 1)))

Tactic:
nontriviality E

Goal state after:
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
μ : Measure E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
inst✝ : μ.IsAddHaarMeasure
a✝ : Nontrivial E
⊢ MeasurePreserving (⇑(homeomorphUnitSphereProd E)) (comap Subtype.val μ) (μ.toSphere.prod (volumeIoiPow (dim E - 1)))
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

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

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

Tactic:
· obtain ⟨m, n, e⟩ := mem_lattice.mp H
    have := LinearIndependent.pair_iff.mp L.indep (m - α) (n - β)
      (by simp; linear_combination e)
    simp only [sub_eq_zero] at this
    norm_cast at this
    aesop

Goal state after:
case refine_2
L : PeriodPair
α β : ℚ
x✝ : α.den = 1 ∧ β.den = 1
h₁ : α.den = 1
h₂ : β.den = 1
⊢ ↑α * L.ω₁ + ↑β * L.ω₂ ∈ L.lattice
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal

Goal state before:
pp: case inr.refine_1
n : ℕ
hn : n ≠ 0
⊢ StrictMonoOn (fun x ↦ ↑x * π / ↑n) ↑(Finset.range (n + 1))

Tactic:
apply StrictMono.strictMonoOn

Goal state after:
case inr.refine_1
n : ℕ
hn : n ≠ 0
⊢ StrictMono fun x ↦ ↑x * π / ↑n
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal

Goal state before:
pp: case inl
i : ℕ
hi : i ≤ 0
⊢ 0 < (-1) ^ i * ∏ j ∈ (Finset.range (0 + 1)).erase i, (node 0 i - node 0 j)

pp: case inr
n i : ℕ
hi : i ≤ n
hn : n ≠ 0
⊢ 0 < (-1) ^ i * ∏ j ∈ (Finset.range (n + 1)).erase i, (node n i - node n j)

Tactic:
· simp [Nat.le_zero.mp hi]

Goal state after:
case inr
n i : ℕ
hi : i ≤ n
hn : n ≠ 0
⊢ 0 < (-1) ^ i * ∏ j ∈ (Finset.range (n + 1)).erase i, (node n i - node n j)
Module: Mathlib.NumberTheory.Niven

Goal state before:
pp: q : ℚ
⊢ IsIntegral ℤ (cexp (↑q * ↑π * I) ^ (2 * q.den))

Tactic:
exact exp_rat_mul_pi_mul_I_pow_two_mul_den _ ▸ isIntegral_one

Goal state after:
Module: Mathlib.NumberTheory.Niven

Goal state before:
pp: q : ℚ
⊢ IsIntegral ℤ (cexp (↑q * ↑π * I))

Tactic:
refine .of_pow (Nat.mul_pos zero_lt_two q.den_pos) ?_
  exact exp_rat_mul_pi_mul_I_pow_two_mul_den _ ▸ isIntegral_one

Goal state after:
Module: Mathlib.NumberTheory.Niven

Goal state before:
pp: r : ℚ
hcos : ∃ q, cos (↑r * π) = ↑q
⊢ cos (↑r * π) ∈ {-1, -1 / 2, 0, 1 / 2, 1}

Tactic:
obtain ⟨k, hk⟩ : ∃ k : ℤ, 2 * cos (r * π) = k := by
    rw [← (Real.isIntegral_two_mul_cos_rat_mul_pi r).exists_int_iff_exists_rat]
    exact ⟨2 * hcos.choose, by push_cast; linarith [hcos.choose_spec]⟩

Goal state after:
r : ℚ
hcos : ∃ q, cos (↑r * π) = ↑q
k : ℤ
hk : 2 * cos (↑r * π) = ↑k
⊢ cos (↑r * π) ∈ {-1, -1 / 2, 0, 1 / 2, 1}
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema

Goal state before:
pp: n : ℤ
hn : n ≠ 0
x : ℝ
hx : 1 < x
this : arcosh x ≠ 0
⊢ arcosh x ≠ 0

Tactic:
by assumption

Goal state after:
Module: Mathlib.Topology.Algebra.InfiniteSum.TsumUniformlyOn

Goal state before:
pp: α : Type u_1
β : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : CompleteSpace F
inst✝¹ : TopologicalSpace β
inst✝ : LocallyCompactSpace β
f : α → β → F
s : Set β
hs : IsOpen[inst✝¹] s
hu : ∀ K ⊆ s, IsCompact K → ∃ u, Summable u ∧ ∀ (n : α), ∀ k ∈ K, ‖f n k‖ ≤ u n
⊢ SummableLocallyUniformlyOn f s

Tactic:
apply SummableLocallyUniformlyOn.of_locally_bounded_eventually hs

Goal state after:
α : Type u_1
β : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : CompleteSpace F
inst✝¹ : TopologicalSpace β
inst✝ : LocallyCompactSpace β
f : α → β → F
s : Set β
hs : IsOpen[inst✝¹] s
hu : ∀ K ⊆ s, IsCompact K → ∃ u, Summable u ∧ ∀ (n : α), ∀ k ∈ K, ‖f n k‖ ≤ u n
⊢ ∀ K ⊆ s, IsCompact K → ∃ u, Summable u ∧ ∀ᶠ (n : α) in cofinite, ∀ k ∈ K, ‖f n k‖ ≤ u n
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: L : PeriodPair
⊢ iteratedDeriv 6 (L.relation * id ^ 6) 0 = 0

Tactic:
rw [L.relation_mul_id_pow_six_eventuallyEq.iteratedDeriv_eq]

Goal state after:
L : PeriodPair
⊢ iteratedDeriv 6
      (fun z ↦
        (℘'[L - 0] z * z ^ 3 - 2) ^ 2 - 4 * (℘[L - 0] z * z ^ 2 + 1) ^ 3 + L.g₂ * (℘[L - 0] z * z ^ 6 + z ^ 4) +
          L.g₃ * z ^ 6)
      0 =
    0
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

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

Tactic:
rw [L.relation_mul_id_pow_six_eventuallyEq.iteratedDeriv_eq]

Goal state after:
case neg
L : PeriodPair
i : ℕ
hi₁ : i < 7
hi₂ : ¬Odd i
hi₃ : ¬i = 0
hi₄ : ¬i = 6
⊢ iteratedDeriv i
      (fun z ↦
        (℘'[L - 0] z * z ^ 3 - 2) ^ 2 - 4 * (℘[L - 0] z * z ^ 2 + 1) ^ 3 + L.g₂ * (℘[L - 0] z * z ^ 6 + z ^ 4) +
          L.g₃ * z ^ 6)
      0 =
    0
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: L : PeriodPair
x : ℂ
hx : x ∉ L.lattice
this : AnalyticAt ℂ ℘'[L] x
⊢ AnalyticAt ℂ (fun z ↦ ℘'[L] z ^ 2 - 4 * ℘[L] z ^ 3 + L.g₂ * ℘[L] z + L.g₃) x

Tactic:
have := L.analyticOnNhd_weierstrassP _ hx

Goal state after:
L : PeriodPair
x : ℂ
hx : x ∉ L.lattice
this✝ : AnalyticAt ℂ ℘'[L] x
this : AnalyticAt ℂ ℘[L] x
⊢ AnalyticAt ℂ (fun z ↦ ℘'[L] z ^ 2 - 4 * ℘[L] z ^ 3 + L.g₂ * ℘[L] z + L.g₃) x
Module: Mathlib.Topology.Algebra.InfiniteSum.TsumUniformlyOn

Goal state before:
pp: ι : Type u_1
𝕜 : Type u_2
F : Type u_3
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : IsRCLikeNormedField 𝕜
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set 𝕜
f : ι → 𝕜 → F
m : ℕ
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
x : 𝕜
hx : x ∈ s
hsum : ∀ t ∈ s, Summable fun n ↦ f n t
h : ∀ (k : ℕ), 1 ≤ k → k ≤ m → SummableLocallyUniformlyOn (fun n ↦ iteratedDerivWithin k (fun z ↦ f n z) s) s
hf2 : ∀ (n : ι) (k : ℕ) (r : 𝕜), k ≤ m → r ∈ s → DifferentiableAt 𝕜 (iteratedDerivWithin k (fun z ↦ f n z) s) r
⊢ iteratedDerivWithin m (fun z ↦ ∑' (n : ι), f n z) s x = ∑' (n : ι), iteratedDerivWithin m (f n) s x

Tactic:
induction m generalizing x with

Goal state after: