mathlib-initiative/mathlib-tactics huggingface dataset:
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
x : ℕ
hx : x ∈ range (i + j).succ
hneq : x ≠ i
⊢ x + (i + j - x) = i + j

Tactic:
simp_all

Goal state after:
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
⊢ 0 ≤ ↑↑(↑(P.comp (-X)).natDegree).negOnePow * (P.leadingCoeff * ↑↑(↑P.natDegree).negOnePow)

Tactic:
show (P.comp (-X)).natDegree = P.natDegree by simp [natDegree_comp],

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
⊢ 0 ≤ ↑↑(↑P.natDegree).negOnePow * (P.leadingCoeff * ↑↑(↑P.natDegree).negOnePow)
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:
by
  rw [← vMulEq] at hdom
  rw [coeff_mul, IsNonarchimedean.apply_sum_eq_of_lt vna (by grind) (k := (i, j))
    (s := Finset.antidiagonal (i + j)) (Finset.mem_antidiagonal.mpr rfl) hdom]

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

Goal state before:
pp: case neg
p : ℂ[X]
hp : ¬p = 0
this : ∀ x ∈ Multiset.map (fun x ↦ max 1 ‖x‖) p.roots, x ≠ 0
⊢ (C p.leadingCoeff * (Multiset.map (fun x ↦ X - C x) p.roots).prod).logMahlerMeasure =
    log ‖p.leadingCoeff‖ + (Multiset.map (fun a ↦ log⁺ ‖a‖) p.roots).sum

Tactic:
logMahlerMeasure_mul_eq_add_logMahlerMeasure (by simp [hp, X_sub_C_ne_zero])

Goal state after:
case neg
p : ℂ[X]
hp : ¬p = 0
this : ∀ x ∈ Multiset.map (fun x ↦ max 1 ‖x‖) p.roots, x ≠ 0
⊢ (C p.leadingCoeff).logMahlerMeasure + (Multiset.map (fun x ↦ X - C x) p.roots).prod.logMahlerMeasure =
    log ‖p.leadingCoeff‖ + (Multiset.map (fun a ↦ log⁺ ‖a‖) p.roots).sum
Module: Mathlib.RingTheory.MvPowerSeries.GaussNorm

Goal state before:
pp: case pos
R : Type u_1
σ : Type u_2
v : R → ℝ
c : σ → ℝ
inst✝¹ : Ring R
inst✝ : DecidableEq σ
f g : MvPowerSeries σ R
hf : HasGaussNorm v c f
hg : HasGaussNorm v c g
hfg : HasGaussNorm v c (f * g)
vNonneg : ∀ (a : R), v a ≥ 0
vZero : v 0 = 0
vNA : IsNonarchimedean v
vMulEq : ∀ (a b : R), v (a * b) = v a * v b
vNeg : ∀ (a : R), v (-a) = v a
h_eq_zero : ∀ (x : R), v x = 0 → x = 0
hc : ∀ (i : σ), 0 < c i
hdom :
  ∃ i j,
    AchievesGaussNorm v c f i ∧
      AchievesGaussNorm v c g j ∧
        ∀ 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)
hf' : f = 0
⊢ gaussNorm v c (f * g) = gaussNorm v c f * gaussNorm v c g

Tactic:
simp [hf', gaussNorm_zero v c vZero]

Goal state after:
Module: Mathlib.Order.Filter.FilterProduct

Goal state before:
pp: α : Type u
β : Type v
φ : Ultrafilter α
inst✝ : LinearOrder β
x y : β
⊢ ↑(max x y) = max ↑x ↑y

Tactic:
rw [max_def, map₂_const]

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.Analysis.Polynomial.MahlerMeasure

Goal state before:
pp: A : Type u_2
inst✝ : NormedRing A
p : A[X]
v : A →+* ℂ
hv : Isometry ⇑v
⊢ ((map v p).sum fun x a ↦ ‖a‖) = p.sum fun x a ↦ ‖a‖

Tactic:
sum_def,

Goal state after:
A : Type u_2
inst✝ : NormedRing A
p : A[X]
v : A →+* ℂ
hv : Isometry ⇑v
⊢ ∑ n ∈ (map v p).support, ‖(map v p).coeff n‖ = p.sum fun x a ↦ ‖a‖
Module: Mathlib.Analysis.Polynomial.MahlerMeasure

Goal state before:
pp: A : Type u_2
inst✝ : NormedRing A
p : A[X]
v : A →+* ℂ
hv : Isometry ⇑v
⊢ ∑ n ∈ (map v p).support, ‖(map v p).coeff n‖ = p.sum fun x a ↦ ‖a‖

Tactic:
sum_def,

Goal state after:
A : Type u_2
inst✝ : NormedRing A
p : A[X]
v : A →+* ℂ
hv : Isometry ⇑v
⊢ ∑ n ∈ (map v p).support, ‖(map v p).coeff n‖ = ∑ n ∈ p.support, ‖p.coeff n‖
Module: Mathlib.Analysis.Real.Pi.Irrational

Goal state before:
pp: θ : ℝ
n : ℕ
f : ℝ → ℝ := fun x ↦ 1 - x ^ 2
u₁ : ℝ → ℝ := fun x ↦ f x ^ (n + 1)
u₁' : ℝ → ℝ := fun x ↦ -(2 * (↑n + 1) * x * f x ^ n)
v₁ : ℝ → ℝ := fun x ↦ sin (x * θ)
v₁' : ℝ → ℝ := fun x ↦ cos (x * θ) * θ
u₂ : ℝ → ℝ := fun x ↦ x * f x ^ n
u₂' : ℝ → ℝ := fun x ↦ f x ^ n - 2 * ↑n * x ^ 2 * f x ^ (n - 1)
v₂ : ℝ → ℝ := fun x ↦ cos (x * θ)
v₂' : ℝ → ℝ := fun x ↦ -sin (x * θ) * θ
⊢ (∫ (x : ℝ) in -1..1, (1 - x ^ 2) ^ (n + 1) * cos (x * θ)) * θ ^ 2 =
    -(2 * 2 * ((↑n + 1) * (0 ^ n * cos θ))) + 2 * (↑n + 1) * (2 * ↑n + 1) * I n θ - 4 * (↑n + 1) * ↑n * I (n - 1) θ

Tactic:
have hfd : Continuous f := by fun_prop

Goal state after:
θ : ℝ
n : ℕ
f : ℝ → ℝ := fun x ↦ 1 - x ^ 2
u₁ : ℝ → ℝ := fun x ↦ f x ^ (n + 1)
u₁' : ℝ → ℝ := fun x ↦ -(2 * (↑n + 1) * x * f x ^ n)
v₁ : ℝ → ℝ := fun x ↦ sin (x * θ)
v₁' : ℝ → ℝ := fun x ↦ cos (x * θ) * θ
u₂ : ℝ → ℝ := fun x ↦ x * f x ^ n
u₂' : ℝ → ℝ := fun x ↦ f x ^ n - 2 * ↑n * x ^ 2 * f x ^ (n - 1)
v₂ : ℝ → ℝ := fun x ↦ cos (x * θ)
v₂' : ℝ → ℝ := fun x ↦ -sin (x * θ) * θ
hfd : Continuous f
⊢ (∫ (x : ℝ) in -1..1, (1 - x ^ 2) ^ (n + 1) * cos (x * θ)) * θ ^ 2 =
    -(2 * 2 * ((↑n + 1) * (0 ^ n * cos θ))) + 2 * (↑n + 1) * (2 * ↑n + 1) * I n θ - 4 * (↑n + 1) * ↑n * I (n - 1) θ
Module: Mathlib.Analysis.Real.Pi.Wallis

Goal state before:
pp: k : ℕ
⊢ 0 < W k

Tactic:
induction k with
  | zero => unfold W; simp
  | succ k hk =>
    rw [W_succ]
    refine mul_pos hk (mul_pos (div_pos ?_ ?_) (div_pos ?_ ?_)) <;> positivity

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

Goal state before:
pp: case inl
z : ℂ
k : ℤ
nr : z.re = ↑(2 * k + 1) * π / 2
h₂ : 2 * k + 1 ≤ 1
h₁ : -1 < 2 * k + 1
⊢ z.re = π / 2

Tactic:
show 2 * k + 1 = 1 by lia,

Goal state after:
case inl
z : ℂ
k : ℤ
nr : z.re = ↑1 * π / 2
h₂ : 2 * k + 1 ≤ 1
h₁ : -1 < 2 * k + 1
⊢ z.re = π / 2
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arctan

Goal state before:
pp: case inl
z : ℂ
k : ℤ
nr : z.re = ↑(2 * k + 1) * π / 2
h₂ : 2 * k + 1 ≤ 1
h₁ : -1 < 2 * k + 1
⊢ z.re = π / 2

Tactic:
rwa [show 2 * k + 1 = 1 by lia, Int.cast_one, one_mul] at nr

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

Goal state before:
pp: x : ℝ
hx : 1 ≤ x
⊢ sinh (log (x + √(x ^ 2 - 1))) = √(x ^ 2 - 1)

Tactic:
sinh_eq,

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

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

Tactic:
lt_div_iff₀' (by positivity),

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

Goal state before:
pp: q : ℕ
p : ℝ
hp₀ : p ≠ 0
hp₁ : p ≠ 1
⊢ deriv (fun p ↦ p * log ↑(↑q - 1) + binEntropy p) p = log (↑q - 1) + log (1 - p) - log p

Tactic:
rw [deriv_fun_add]

Goal state after:
q : ℕ
p : ℝ
hp₀ : p ≠ 0
hp₁ : p ≠ 1
⊢ deriv (fun p ↦ p * log ↑(↑q - 1)) p + deriv binEntropy p = log (↑q - 1) + log (1 - p) - log p

case hf
q : ℕ
p : ℝ
hp₀ : p ≠ 0
hp₁ : p ≠ 1
⊢ DifferentiableAt ℝ (fun p ↦ p * log ↑(↑q - 1)) p

case hg
q : ℕ
p : ℝ
hp₀ : p ≠ 0
hp₁ : p ≠ 1
⊢ DifferentiableAt ℝ binEntropy p
Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy

Goal state before:
pp: case neg
q : ℕ
p : ℝ
is_x_where_nondiff : ¬(p ≠ 0 ∧ p ≠ 1)
this : p = 0 ∨ p = 1
⊢ 0 = -1 / (p * (1 - p))

pp: case neg
q : ℕ
p : ℝ
is_x_where_nondiff : ¬(p ≠ 0 ∧ p ≠ 1)
this : p = 0 ∨ p = 1
⊢ ¬DifferentiableAt ℝ (deriv (qaryEntropy q)) p

Tactic:
· simp_all only [ne_eq, not_and, Decidable.not_not]
      cases this <;>
        simp_all only [mul_zero, one_ne_zero, zero_ne_one, sub_zero, mul_one, div_zero, sub_self]

Goal state after:
case neg
q : ℕ
p : ℝ
is_x_where_nondiff : ¬(p ≠ 0 ∧ p ≠ 1)
this : p = 0 ∨ p = 1
⊢ ¬DifferentiableAt ℝ (deriv (qaryEntropy q)) p
Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy

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

Tactic:
simp only [sub_neg, gt_iff_lt]

Goal state after:
q : ℕ
qLe2 : 2 ≤ q
p1 : ℝ
hp1 : p1 ∈ Icc (1 - 1 / ↑q) 1
p2 : ℝ
hp2 : p2 ∈ Icc (1 - 1 / ↑q) 1
p1le2 : p1 < p2
p : ℝ
this : 2 ≤ ↑q
qinv_lt_1 : (↑q)⁻¹ < 1
zero_lt_1_sub_p : 0 < 1 - p
hp : 1 - (↑q)⁻¹ < p ∧ p < 1
⊢ log (↑q - 1) + log (1 - p) < log p
Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy

Goal state before:
pp: case ha
q : ℕ
p : ℝ
hp : 0 < p ∧ p < 1
⊢ -1 < 0

pp: case hb
q : ℕ
p : ℝ
hp : 0 < p ∧ p < 1
⊢ 0 < p * (1 - p)

Tactic:
· norm_num [show 0 < log 2 by positivity]

Goal state after:
case hb
q : ℕ
p : ℝ
hp : 0 < p ∧ p < 1
⊢ 0 < p * (1 - p)
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog.Order

Goal state before:
pp: case neg
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : A
ha : ¬IsStrictlyPositive a
⊢ Tendsto (fun i ↦ if a ∈ {b | IsStrictlyPositive b} then cfc (fun x ↦ i⁻¹ * (x ^ i - 1)) a else 0) (𝓝[>] 0)
    (𝓝 (if a ∈ {b | IsStrictlyPositive b} then log a else 0))

Tactic:
simp_all

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

Goal state before:
pp: s : Set ℝ
hs : s ⊆ Ioi 0
hs' : IsCompact s
ε : ℝ
hε : 0 < ε
pbound : ℝ := ε / (sSup ((fun x ↦ ‖log x‖ ^ 2) '' s) + 1)
hxs : ∀ x ∈ s, x ≠ 0
sSup_nonneg : 0 ≤ sSup ((fun x ↦ ‖log x‖ ^ 2) '' s)
sSup_nonneg' : 0 ≤ sSup ((fun x ↦ ‖log x‖) '' s)
pbound_pos : 0 < pbound
h₁ : ∀ᶠ (p : ℝ) in 𝓝[>] 0, 0 < p ∧ p < pbound
h₂ : ∀ᶠ (p : ℝ) in 𝓝[>] 0, p ≤ 1 / (sSup ((fun x ↦ ‖log x‖) '' s) + 1)
hcont : ContinuousOn (fun x ↦ ‖log x‖ ^ 2) s
hcont' : ContinuousOn (fun x ↦ ‖log x‖) s
p : ℝ
hp₁ : 0 < p
hp₂ : p < pbound
hp₃ : p ≤ 1 / (sSup ((fun x ↦ ‖log x‖) '' s) + 1)
x : ℝ
hx : x ∈ s
hx' : ‖p * log x‖ ≤ 1
pinv_nonneg : 0 ≤ p⁻¹
⊢ p * ‖log x‖ ^ 2 ≤ p * sSup ((fun x ↦ ‖log x‖ ^ 2) '' s)

Tactic:
by
          gcongr
          refine le_csSup ?_ (by grind)
          grind [IsCompact.bddAbove, ← IsCompact.image_of_continuousOn]

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

Goal state before:
pp: A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
⊢ ConvexOn ℝ {a | IsStrictlyPositive a} inverse

Tactic:
refine ⟨by grind [convex_iff_forall_pos], ?_⟩

Goal state after:
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
⊢ ∀ ⦃x : A⦄,
    x ∈ {a | IsStrictlyPositive a} →
      ∀ ⦃y : A⦄,
        y ∈ {a | IsStrictlyPositive a} →
          ∀ ⦃a b : ℝ⦄, 0 ≤ a → 0 ≤ b → a + b = 1 → (a • x + b • y)⁻¹ʳ ≤ a • x⁻¹ʳ + b • y⁻¹ʳ
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.RingInverseOrder

Goal state before:
pp: case h.refine_3
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
x : A
xpos : IsStrictlyPositive x
y : A
ypos : IsStrictlyPositive y
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
z : A := (conjSqrt x⁻¹ʳ) y
zpos : IsStrictlyPositive z
xinvpos : IsStrictlyPositive x⁻¹ʳ
hsp : IsStrictlyPositive (a • 1 + b • z)
h₁ : (a • 1 + b • z) ^ (-1) = cfc (fun r ↦ (a + b * r) ^ (-1)) z
h₂ : a • 1 + b • z ^ (-1) = cfc (fun r ↦ a + b * r ^ (-1)) z
⊢ ∀ x ∈ spectrum ℝ z, (a + b * x) ^ (-1) ≤ a + b * x ^ (-1)

Tactic:
intro r hr
          suffices (a • 1 + b • r) ^ (-1 : ℤ) ≤ a • 1 ^ (-1 : ℤ) + b • r ^ (-1 : ℤ) by
            simp_rw [← Real.rpow_intCast] at this
            simpa using this
          have : ConvexOn ℝ (Set.Ioi 0) (fun z : ℝ => z ^ (-1 : ℤ)) := convexOn_zpow (-1)
          grind [ConvexOn, IsStrictlyPositive.spectrum_pos]

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

Goal state before:
pp: p : ℝ
hp : p ∈ Ioo 0 1
s : Set ℝ
hs : s ⊆ Ici 0
g : ℝ × ℝ → ℝ := fun q ↦ q.1 ^ (p - 1) * q.2 / (q.1 + q.2)
⊢ ContinuousOn (Function.uncurry p.rpowIntegrand₀₁) (Ioi 0 ×ˢ s)

Tactic:
refine ContinuousOn.congr (f := g) ?_ fun q => ?_

Goal state after:
case refine_1
p : ℝ
hp : p ∈ Ioo 0 1
s : Set ℝ
hs : s ⊆ Ici 0
g : ℝ × ℝ → ℝ := fun q ↦ q.1 ^ (p - 1) * q.2 / (q.1 + q.2)
⊢ ContinuousOn g (Ioi 0 ×ˢ s)

case refine_2
p : ℝ
hp : p ∈ Ioo 0 1
s : Set ℝ
hs : s ⊆ Ici 0
g : ℝ × ℝ → ℝ := fun q ↦ q.1 ^ (p - 1) * q.2 / (q.1 + q.2)
q : ℝ × ℝ
⊢ q ∈ Ioi 0 ×ˢ s → Function.uncurry p.rpowIntegrand₀₁ q = g q
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Deligne

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

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

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

Goal state before:
pp: ⊢ eulerMascheroniSeq' 6 = 49 / 20 - log 6

Tactic:
eulerMascheroniSeq'

Goal state after:
⊢ (if 6 = 0 then 2 else ↑(harmonic 6) - log ↑6) = 49 / 20 - log 6
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Deligne

Goal state before:
pp: s : ℂ
n : ℕ
hs : s ≠ -↑(2 * n)
h : s = -(2 * ↑n)
⊢ False

Tactic:
simp_all

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

Goal state before:
pp: s : ℂ
h1 : s.Gammaℝ ≠ 0
n : ℕ
hs : s ≠ -↑(2 * n + 1)
h : s = -(2 * ↑n + 1)
⊢ False

Tactic:
simp_all

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

Goal state before:
pp: p t : ℝ
hp : p ∈ Ioo 1 2
ht : 0 < t
⊢ MonotoneOn (p.rpowIntegrand₁₂ t) (Ici 0)

Tactic:
refine MonotoneOn.congr ?_ fun x hx ↦ (rpowIntegrand₁₂_eq_mul_rpowIntegrand₀₁ hx ht).symm

Goal state after:
p t : ℝ
hp : p ∈ Ioo 1 2
ht : 0 < t
⊢ MonotoneOn (fun x ↦ x * (p - 1).rpowIntegrand₀₁ t x) (Ici 0)
Module: Mathlib.NumberTheory.Harmonic.GammaDeriv

Goal state before:
pp: n : ℕ
⊢ HasDerivAt Gamma (↑n ! * (-↑γ + ↑(harmonic n))) (↑n + 1)

Tactic:
exact_mod_cast HasDerivAt.complex_of_real
    (by exact_mod_cast differentiableAt_Gamma_nat_add_one n)
    (Real.hasDerivAt_Gamma_nat n) Gamma_ofReal

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 : ℕ
r : R
hb : 1 < b
hr : 0 < r
hr1 : r ≤ 1
⊢ ↑b ^ log b r ≤ r

Tactic:
rw [log_of_right_le_one _ hr1, zpow_neg]

Goal state after:
case inr
R : Type u_1
inst✝³ : Semifield R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorSemiring R
b : ℕ
r : R
hb : 1 < b
hr : 0 < r
hr1 : r ≤ 1
⊢ (↑b ^ ↑(Nat.clog b ⌈r⁻¹⌉₊))⁻¹ ≤ r
Module: Mathlib.Analysis.SpecialFunctions.Log.Base

Goal state before:
pp: x✝ : ℝ
⊢ 0 = 0 x✝

Tactic:
Pi.zero_apply

Goal state after:
x✝ : ℝ
⊢ 0 = 0
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 : ℕ
r : R
⊢ -clog b r⁻¹ = log b r

Tactic:
rw [clog_inv, neg_neg]

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

Goal state before:
pp: b : ℝ
hb : 1 < b
x : ℝ
hx : x < 0
y : ℝ
hy : y < 0
hxy : x < y
⊢ logb b y < logb b x

Tactic:
← logb_abs b y,

Goal state after:
b : ℝ
hb : 1 < b
x : ℝ
hx : x < 0
y : ℝ
hy : y < 0
hxy : x < y
⊢ logb b |y| < logb b x
Module: Mathlib.Analysis.SpecialFunctions.Log.Base

Goal state before:
pp: b : ℝ
hb : 1 < b
x : ℝ
hx : x < 0
y : ℝ
hy : y < 0
hxy : x < y
⊢ -y < -x

Tactic:
neg_lt_neg_iff

Goal state after:
b : ℝ
hb : 1 < b
x : ℝ
hx : x < 0
y : ℝ
hy : y < 0
hxy : x < y
⊢ x < y
Module: Mathlib.Analysis.SpecialFunctions.Log.Base

Goal state before:
pp: b : ℝ
b_pos : 0 < b
b_lt_one : b < 1
x : ℝ
hx : x < 0
y : ℝ
hy : y < 0
hxy : x < y
⊢ logb b x < logb b y

Tactic:
← logb_abs b y,

Goal state after:
b : ℝ
b_pos : 0 < b
b_lt_one : b < 1
x : ℝ
hx : x < 0
y : ℝ
hy : y < 0
hxy : x < y
⊢ logb b x < logb b |y|
Module: Mathlib.Analysis.SpecialFunctions.Log.Base

Goal state before:
pp: b : ℝ
b_pos : 0 < b
b_lt_one : b < 1
x : ℝ
hx : x < 0
y : ℝ
hy : y < 0
hxy : x < y
⊢ -y < -x

Tactic:
neg_lt_neg_iff

Goal state after:
b : ℝ
b_pos : 0 < b
b_lt_one : b < 1
x : ℝ
hx : x < 0
y : ℝ
hy : y < 0
hxy : x < y
⊢ x < y
Module: Mathlib.Analysis.SpecialFunctions.Log.Base

Goal state before:
pp: b : ℝ
n : ℕ
⊢ Tendsto (fun x ↦ logb b x ^ n / id x) atTop (𝓝 0)

pp: b : ℝ
n : ℕ
⊢ ∀ᶠ (x : ℝ) in atTop, id x = 0 → logb b x ^ n = 0

Tactic:
· simpa using tendsto_pow_logb_div_mul_add_atTop 1 0 n one_ne_zero

Goal state after:
b : ℝ
n : ℕ
⊢ ∀ᶠ (x : ℝ) in atTop, id x = 0 → logb b x ^ n = 0
Module: Mathlib.Analysis.SpecialFunctions.Log.Base

Goal state before:
pp: b : ℝ
⊢ logb b =O[⊤] log

Tactic:
by_cases! h : b = -1 ∨ b = 0 ∨ b = 1
  · obtain rfl | rfl | rfl := h
    all_goals simpa [-Asymptotics.isBigO_top] using! Asymptotics.isBigO_zero log ⊤
  · simpa [logb, div_eq_mul_inv, mul_comm]
      using! (Asymptotics.isBigO_refl log ⊤).const_mul_left (log b)⁻¹

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

Goal state before:
pp: b y : ℝ
⊢ Tendsto (fun x ↦ logb b (x + y) - logb b x) atTop (𝓝 0)

Tactic:
simpa [sub_div] using! (tendsto_log_comp_add_sub_log y).div_const (log b)

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

Goal state before:
pp: case inr
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)
h : (a / guess ^ (n + 1) + (n + 1) * guess) / (n + 2) < guess
hguess : guess ≠ 0
⊢ a < (go n a fuel ((a / guess ^ (n + 1) + (n + 1) * guess) / (n + 2)) + 1) ^ (n + 2)

Tactic:
· exact ih <| Nat.nthRoot.lt_pow_go_succ_aux hguess

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

Goal state before:
pp: L : PeriodPair
l₀ : ℂ
r : ℝ
hr : r > 0
s : ℂ
hs : ‖s‖ < r
h : 2 * r ≤ ‖↑0‖
h✝ : ¬↑0 = l₀
this : s ≠ ↑0
⊢ False

Tactic:
simp_all

Goal state after:
L : PeriodPair
l₀ : ℂ
r : ℝ
s : ℂ
hr : 0 < r
hs : ‖s‖ < r
h : 2 * r ≤ 0
h✝ : ¬0 = l₀
this : ¬s = 0
⊢ False
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: L : PeriodPair
l₀ : ℂ
s : Finset ↥L.lattice
i : ↥L.lattice
hi : i ∈ s
h✝ : ¬↑i = l₀
hx : ↑i ∈ (↑L.lattice \ {l₀})ᶜ
⊢ False

Tactic:
simp_all

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

Goal state before:
pp: E : Type u_1
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : MeasurableSpace E
F : Type u_2
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : Nontrivial E
μ : Measure E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : BorelSpace E
inst✝ : μ.IsAddHaarMeasure
f : ℝ → F
r : ℝ
⊢ IntegrableOn (fun x ↦ f ‖x‖) (ball 0 r) μ ↔ Integrable (fun x ↦ (Iio r).indicator f ‖x‖) μ

Tactic:
rw [← integrable_indicator_iff measurableSet_ball]

Goal state after:
E : Type u_1
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : MeasurableSpace E
F : Type u_2
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : Nontrivial E
μ : Measure E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : BorelSpace E
inst✝ : μ.IsAddHaarMeasure
f : ℝ → F
r : ℝ
⊢ Integrable ((ball 0 r).indicator fun x ↦ f ‖x‖) μ ↔ Integrable (fun x ↦ (Iio r).indicator f ‖x‖) μ
Module: Mathlib.MeasureTheory.Constructions.Polish.EmbeddingReal

Goal state before:
pp: case neg
α : Type u_1
inst✝¹ : MeasurableSpace α
inst✝ : StandardBorelSpace α
hα : ¬Countable α
⊢ ¬univ.Countable

Tactic:
exact Cardinal.not_countable_real

Goal state after:
Module: Mathlib.NumberTheory.Niven

Goal state before:
pp: r : ℚ
hr : 3 < (Int.fract r).den
⊢ Irrational (cos (↑r * π))

Tactic:
by_contra! hnz

Goal state after:
r : ℚ
hr : 3 < (Int.fract r).den
hnz : ¬Irrational (cos (↑r * π))
⊢ False
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal

Goal state before:
pp: n : ℕ
P : ℝ[X]
hPdeg : P.degree ≤ ↑n
hPbnd : ∀ x ∈ Set.Icc (-1) 1, |eval x P| ≤ 1
hP : ¬P = 0
⊢ P.leadingCoeff ≤ 2 ^ (n - 1)

Tactic:
lift P.degree to ℕ using degree_ne_bot.mpr hP with d hd
    replace hPdeg : d ≤ n := (WithBot.coe_le rfl).mp hPdeg
    rw [leadingCoeff, natDegree_eq_of_degree_eq_some hd.symm]
    grw [coeff_le_of_forall_abs_le_one (le_of_eq hd.symm) hPbnd, hPdeg]
    norm_num

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema

Goal state before:
pp: case mp
n : ℕ
hn : n ≠ 0
x : ℝ
hTx : |eval x (T ℝ ↑n)| = 1
hx : |x| ≤ 1
⊢ ∃ k ≤ n, x = cos (↑k * π / ↑n)

Tactic:
← cos_arccos (neg_le_of_abs_le hx) (le_of_max_le_left hx),

Goal state after:
case mp
n : ℕ
hn : n ≠ 0
x : ℝ
hTx : |eval (cos (arccos x)) (T ℝ ↑n)| = 1
hx : |x| ≤ 1
⊢ ∃ k ≤ n, x = cos (↑k * π / ↑n)
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable

Goal state before:
pp: case hΘ
d : ℤ
z : ℂ
hz : z ≠ 0
⊢ (fun c ↦ ↑c * z) =Θ[cofinite] fun n ↦ ↑n

Tactic:
simp_rw [mul_comm]

Goal state after:
case hΘ
d : ℤ
z : ℂ
hz : z ≠ 0
⊢ (fun c ↦ z * ↑c) =Θ[cofinite] fun n ↦ ↑n
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: L : PeriodPair
this : Meromorphic fun z ↦ ℘'[L] z ^ 2 - 4 * ℘[L] z ^ 3 + L.g₂ * ℘[L] z + L.g₃
z w : ℂ
hw : w ∈ {z}ᶜ
hw' : w ∈ (↑L.lattice \ {z})ᶜ
⊢ w ∉ L.lattice

Tactic:
simp_all

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

Goal state before:
pp: L : PeriodPair
z : ℂ
hz : z ∈ (↑L.lattice \ {0})ᶜ
hz0 : ¬z = 0
⊢ z ∉ L.lattice

Tactic:
simp_all

Goal state after:
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable

Goal state before:
pp: z : ℂ
hz : z ≠ 0
d k : ℤ
hk : 2 ≤ k
⊢ Summable fun c ↦ ((↑c * z + ↑d) ^ k)⁻¹

Tactic:
by
  apply summable_inv_of_isBigO_rpow_inv (a := k) (by norm_cast)
  lift k to ℕ using (by lia)
  simp only [zpow_natCast, Int.cast_natCast, Real.rpow_natCast, ← inv_pow, ← abs_inv]
  apply (linear_inv_isBigO_left d hz).abs_right.pow

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

Goal state before:
pp: n : ℕ
⊢ fib (-↑n) = (-1) ^ (n + 1) * ↑(Nat.fib n)

Tactic:
by
  rcases n.even_or_odd with (hn | hn)
  · simp [fib, hn, pow_add]
  · simp [fib_of_odd, hn]

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

Goal state before:
pp: case inr
n : ℤ
m : ℕ
h : -↑m ∣ n
⊢ fib (-↑m) ∣ fib n

Tactic:
· simp [fib_neg_natCast, ← fib_natCast, fib_natCast_dvd <| Int.neg_dvd.mp h]

Goal state after:
Module: Mathlib.Tactic.NormNum.Prime

Goal state before:
pp: case inr.inl
k : ℕ
h✝ : MinFacHelper (succ 0) k
this : 2 < (succ 0).minFac
h : succ 0 > 0
⊢ 1 < succ 0

Tactic:
simp_all

Goal state after:
Module: Mathlib.Analysis.SumIntegralComparisons

Goal state before:
pp: a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc ↑a ↑b)
this : ∫ (x : ℝ) in ↑a..↑a + ↑(b - a), f x ≤ ∑ x ∈ Finset.Ico (0 + a) (b - a + a), f ↑x
⊢ ∫ (x : ℝ) in ↑a..↑b, f x ≤ ∑ x ∈ Finset.Ico a b, f ↑x

Tactic:
simp_all

Goal state after:
Module: Mathlib.Analysis.SumIntegralComparisons

Goal state before:
pp: a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc ↑a ↑b)
this : ∫ (x : ℝ) in ↑a..↑a + ↑(b - a), f x ≤ ∑ x ∈ Finset.range (b - a), f (↑a + ↑x)
⊢ ∫ (x : ℝ) in ↑a..↑a + ↑(b - a), f x ≤ ∑ x ∈ Finset.range (b - a), f ↑(a + x)

Tactic:
simp_all

Goal state after:
Module: Mathlib.Analysis.SumIntegralComparisons

Goal state before:
pp: a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc ↑a ↑b)
this : ∑ i ∈ Finset.Ico (0 + a) (b - a + a), f ↑(i + 1) ≤ ∫ (x : ℝ) in ↑a..↑a + ↑(b - a), f x
⊢ ∑ i ∈ Finset.Ico a b, f ↑(i + 1) ≤ ∫ (x : ℝ) in ↑a..↑b, f x

Tactic:
simp_all

Goal state after: