mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Rat.NatSqrt.Defs

Goal state before:
pp: x prec : ℕ
h : 0 < prec
⊢ ↑x < (↑(x * prec ^ 2).sqrt / ↑prec + 1 / ↑prec) ^ 2

Tactic:
rw [← mul_lt_mul_iff_of_pos_right (a := (prec ^ 2 : ℚ)) (by positivity)]

Goal state after:
x prec : ℕ
h : 0 < prec
⊢ ↑x * ↑prec ^ 2 < (↑(x * prec ^ 2).sqrt / ↑prec + 1 / ↑prec) ^ 2 * ↑prec ^ 2
Module: Mathlib.Analysis.Polynomial.MahlerMeasure

Goal state before:
pp: p : ℂ[X]
⊢ p.logMahlerMeasure = log ‖p.leadingCoeff‖ + (Multiset.map (fun a ↦ log⁺ ‖a‖) p.roots).sum

Tactic:
by
  by_cases hp : p = 0
  · simp [hp]
  have : ∀ x ∈ Multiset.map (fun x ↦ max 1 ‖x‖) p.roots, x ≠ 0 := by grind [Multiset.mem_map]
  nth_rw 1 [(IsAlgClosed.splits p).eq_prod_roots]
  rw [logMahlerMeasure_mul_eq_add_logMahlerMeasure (by simp [hp, X_sub_C_ne_zero])]
  simp [posLog_eq_log_max_one, logMahlerMeasure_eq_log_MahlerMeasure,
    prod_mahlerMeasure_eq_mahlerMeasure_prod, log_multiset_prod this]

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

Goal state before:
pp: b : ℕ
x y : ℕ → Fin b
n : ℕ
hxy : ∀ i < n, x i = y i
⊢ |ofDigits x - ofDigits y| ≤ (↑b ^ n)⁻¹

Tactic:
rw [ofDigits_eq_sum_add_ofDigits x n, ofDigits_eq_sum_add_ofDigits y n]

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

Goal state before:
pp: c d a b n : ℕ
z : ℝ
hz : (↑c / ↑d).sqrtTwoAddSeries n ≤ z
hb : 0 < b
hd : 0 < d
h : (2 * b + a) * d ^ 2 ≤ c ^ 2 * b
⊢ (√(2 + ↑a / ↑b)).sqrtTwoAddSeries n ≤ (↑c / ↑d).sqrtTwoAddSeries n

Tactic:
apply sqrtTwoAddSeries_monotone_left

Goal state after:
c d a b n : ℕ
z : ℝ
hz : (↑c / ↑d).sqrtTwoAddSeries n ≤ z
hb : 0 < b
hd : 0 < d
h : (2 * b + a) * d ^ 2 ≤ c ^ 2 * b
⊢ √(2 + ↑a / ↑b) ≤ ↑c / ↑d
Module: Mathlib.Analysis.Real.Pi.Bounds

Goal state before:
pp: a b c d n : ℕ
z : ℝ
hz : z ≤ (↑a / ↑b).sqrtTwoAddSeries n
hb : 0 < b
hd : 0 < d
h : a ^ 2 * d ≤ (2 * d + c) * b ^ 2
⊢ (↑a / ↑b).sqrtTwoAddSeries n ≤ (√(2 + ↑c / ↑d)).sqrtTwoAddSeries n

Tactic:
apply sqrtTwoAddSeries_monotone_left

Goal state after:
a b c d n : ℕ
z : ℝ
hz : z ≤ (↑a / ↑b).sqrtTwoAddSeries n
hb : 0 < b
hd : 0 < d
h : a ^ 2 * d ≤ (2 * d + c) * b ^ 2
⊢ ↑a / ↑b ≤ √(2 + ↑c / ↑d)
Module: Mathlib.Analysis.Real.Pi.Bounds

Goal state before:
pp: a b c d n : ℕ
z : ℝ
hz : z ≤ (↑a / ↑b).sqrtTwoAddSeries n
hb : 0 < b
hd : 0 < d
h : a ^ 2 * d ≤ (2 * d + c) * b ^ 2
⊢ z ≤ (↑c / ↑d).sqrtTwoAddSeries (n + 1)

Tactic:
apply le_trans hz; rw [sqrtTwoAddSeries_succ]; apply sqrtTwoAddSeries_monotone_left
  apply le_sqrt_of_sq_le
  have hb' : 0 < (b : ℝ) := Nat.cast_pos.2 hb
  have hd' : 0 < (d : ℝ) := Nat.cast_pos.2 hd
  rw [div_pow, add_div_eq_mul_add_div _ _ (ne_of_gt hd'), div_le_div_iff₀ (pow_pos hb' _) hd']
  exact mod_cast h

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

Goal state before:
pp: x : ℝ
n : ℕ
m : ℤ
hm : m ≠ 0
p : ℕ
hp : Fact (Nat.Prime p)
hxr : x ^ n = ↑m
hv : multiplicity (↑p) m % n ≠ 0
⊢ Irrational x

Tactic:
rcases Nat.eq_zero_or_pos n with (rfl | hnpos)
  · rw [eq_comm, pow_zero, ← Int.cast_one, Int.cast_inj] at hxr
    simp [hxr, multiplicity_of_one_right (mt isUnit_iff_dvd_one.1
      (mt Int.natCast_dvd_natCast.1 hp.1.not_dvd_one))] at hv
  refine irrational_nrt_of_notint_nrt _ _ hxr ?_ hnpos
  rintro ⟨y, rfl⟩
  rw [← Int.cast_pow, Int.cast_inj] at hxr
  subst m
  have : y ≠ 0 := by rintro rfl; rw [zero_pow hnpos.ne'] at hm; exact hm rfl
  rw [(Int.finiteMultiplicity_iff.2 ⟨by simp [hp.1.ne_one], this⟩).multiplicity_pow
    (Nat.prime_iff_prime_int.1 hp.1), Nat.mul_mod_right] at hv
  exact hv rfl

Goal state after:
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 * θ) * θ
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) θ

Tactic:
have hu₁d : Continuous u₁' := 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
hu₁d : Continuous u₁'
⊢ (∫ (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.SpecialFunctions.Complex.Arctan

Goal state before:
pp: z : ℂ
hz : ‖z‖ < 1
z₁ : (1 + z * I).arg ≠ π ∧ 1 + z * I ≠ 0
z₂ : (1 - z * I).arg ≠ π ∧ 1 - z * I ≠ 0
b₁ : (1 + z * I).arg ∈ Set.Ioo (-(π / 2)) (π / 2)
⊢ (if False then π else -(1 - z * I).arg) ∈ Set.Ioo (-(π / 2)) (π / 2)

Tactic:
ite_false,

Goal state after:
z : ℂ
hz : ‖z‖ < 1
z₁ : (1 + z * I).arg ≠ π ∧ 1 + z * I ≠ 0
z₂ : (1 - z * I).arg ≠ π ∧ 1 - z * I ≠ 0
b₁ : (1 + z * I).arg ∈ Set.Ioo (-(π / 2)) (π / 2)
⊢ -(1 - z * I).arg ∈ Set.Ioo (-(π / 2)) (π / 2)
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arctan

Goal state before:
pp: 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) = -I / 2 * ((1 + 1) * (z * I) ^ (2 * k + 1) / ↑(2 * k + 1))

Tactic:
← mul_div_assoc (_ / _),

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) = -I / 2 * ((1 + 1) * (z * I) ^ (2 * k + 1)) / ↑(2 * k + 1)
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arctan

Goal state before:
pp: case e'_6.e_a
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) = -I * (z ^ (2 * k + 1) * (I * I ^ (2 * k)))

Tactic:
pow_mul,

Goal state after:
case e'_6.e_a
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) = -I * (z ^ (2 * k + 1) * (I * (I ^ 2) ^ k))
Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy

Goal state before:
pp: ⊢ Continuous binEntropy

Tactic:
binEntropy_eq_negMulLog_add_negMulLog_one_sub'

Goal state after:
⊢ Continuous fun p ↦ p.negMulLog + (1 - p).negMulLog
Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy

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

Tactic:
rw [DifferentiableAt.fun_add_iff_right, differentiableAt_iff_comp_const_sub (b := 1)] 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
q : ℕ
p : ℝ
is_x_where_nondiff : p ≠ 0 ∧ p ≠ 1
⊢ deriv (deriv (qaryEntropy q)) p = -1 / (p * (1 - p))

Tactic:
obtain ⟨xne0, xne1⟩ := is_x_where_nondiff
    suffices ∀ᶠ y in (𝓝 p),
        deriv (fun p ↦ (qaryEntropy q) p) y = log (q - 1) + log (1 - y) - log y by
      refine (Filter.EventuallyEq.deriv_eq this).trans ?_
      rw [deriv_fun_sub ?_ (differentiableAt_log xne0)]
      · rw [deriv.log differentiableAt_fun_id xne0]
        simp only [deriv_id'', one_div]
        · have {q : ℝ} (p : ℝ) : DifferentiableAt ℝ (fun p => q - p) p := by fun_prop
          simp [field, sub_ne_zero_of_ne xne1.symm, this]
          ring
      · apply DifferentiableAt.add
        · simp only [differentiableAt_const]
        exact DifferentiableAt.log (by fun_prop) (sub_ne_zero.mpr xne1.symm)
    filter_upwards [eventually_ne_nhds xne0, eventually_ne_nhds xne1]
      with y xne0 h2 using deriv_qaryEntropy xne0 h2

Goal state after:
Module: Mathlib.Analysis.Real.Pi.Irrational

Goal state before:
pp: case convert_2.convert_2.e_a
θ : ℝ
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
hu₁d : Continuous u₁'
hv₁d : Continuous v₁'
hu₂d : Continuous u₂'
hv₂d : Continuous v₂'
hu₁_eval_one : u₁ 1 = 0
hu₁_eval_neg_one : u₁ (-1) = 0
t : u₂ 1 * v₂ 1 - u₂ (-1) * v₂ (-1) = 2 * (0 ^ n * cos θ)
hf : ∀ (x : ℝ), HasDerivAt f (-2 * x) x
hu₁ : ∀ (x : ℝ), HasDerivAt u₁ (u₁' x) x
hv₁ : ∀ (x : ℝ), HasDerivAt v₁ (v₁' x) x
hu₂ : ∀ (x : ℝ), HasDerivAt u₂ (u₂' x) x
hv₂ : ∀ (x : ℝ), HasDerivAt v₂ (v₂' x) x
this✝ : ∀ (x : ℝ), u₂' x = (2 * ↑n + 1) * f x ^ n - 2 * ↑n * f x ^ (n - 1)
this : Continuous v₂
⊢ (2 * (↑n + 1) * ∫ (x : ℝ) in -1..1, (2 * ↑n + 1) * (f x ^ n * v₂ x)) -
      2 * (↑n + 1) * ∫ (x : ℝ) in -1..1, 2 * ↑n * (f x ^ (n - 1) * v₂ x) =
    2 * (↑n + 1) * (2 * ↑n + 1) * I n θ - 4 * (↑n + 1) * ↑n * I (n - 1) θ

Tactic:
simp_rw [integral_const_mul]

Goal state after:
case convert_2.convert_2.e_a
θ : ℝ
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
hu₁d : Continuous u₁'
hv₁d : Continuous v₁'
hu₂d : Continuous u₂'
hv₂d : Continuous v₂'
hu₁_eval_one : u₁ 1 = 0
hu₁_eval_neg_one : u₁ (-1) = 0
t : u₂ 1 * v₂ 1 - u₂ (-1) * v₂ (-1) = 2 * (0 ^ n * cos θ)
hf : ∀ (x : ℝ), HasDerivAt f (-2 * x) x
hu₁ : ∀ (x : ℝ), HasDerivAt u₁ (u₁' x) x
hv₁ : ∀ (x : ℝ), HasDerivAt v₁ (v₁' x) x
hu₂ : ∀ (x : ℝ), HasDerivAt u₂ (u₂' x) x
hv₂ : ∀ (x : ℝ), HasDerivAt v₂ (v₂' x) x
this✝ : ∀ (x : ℝ), u₂' x = (2 * ↑n + 1) * f x ^ n - 2 * ↑n * f x ^ (n - 1)
this : Continuous v₂
⊢ 2 * (↑n + 1) * ((2 * ↑n + 1) * ∫ (x : ℝ) in -1..1, f x ^ n * v₂ x) -
      2 * (↑n + 1) * (2 * ↑n * ∫ (x : ℝ) in -1..1, f x ^ (n - 1) * v₂ x) =
    2 * (↑n + 1) * (2 * ↑n + 1) * I n θ - 4 * (↑n + 1) * ↑n * I (n - 1) θ
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.ConjSqrt

Goal state before:
pp: A : Type u_1
inst✝⁸ : PartialOrder A
inst✝⁷ : Ring A
inst✝⁶ : StarRing A
inst✝⁵ : TopologicalSpace A
inst✝⁴ : StarOrderedRing A
inst✝³ : Algebra ℝ A
inst✝² : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝¹ : NonnegSpectrumClass ℝ A
inst✝ : SeparatelyContinuousMul A
c a : A
hc : ¬0 ≤ c
⊢ (conjSqrt c) a = 0

Tactic:
simp [conjSqrt_apply, sqrt_of_not_nonneg hc]

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

Goal state before:
pp: case a
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)⁻¹
⊢ p < (↑q - 1) * (1 - p)

Tactic:
· 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.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.ConjSqrt

Goal state before:
pp: A : Type u_1
inst✝¹⁰ : PartialOrder A
inst✝⁹ : Ring A
inst✝⁸ : StarRing A
inst✝⁷ : TopologicalSpace A
inst✝⁶ : StarOrderedRing A
inst✝⁵ : Algebra ℝ A
inst✝⁴ : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝³ : NonnegSpectrumClass ℝ A
inst✝² : SeparatelyContinuousMul A
inst✝¹ : IsSemitopologicalRing A
inst✝ : T2Space A
c a : A
hc : IsStrictlyPositive c
⊢ ((conjSqrt c) a)⁻¹ʳ = (conjSqrt c⁻¹ʳ) a⁻¹ʳ

Tactic:
by_cases ha : IsUnit a
  · grind [conjSqrt_apply]
  · have : ¬IsUnit (conjSqrt c a) := by grind [conjSqrt_apply, IsUnit.mul_left_iff]
    simp [inverse_non_unit a ha, inverse_non_unit _ this]

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

Goal state before:
pp: case neg
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
p : ℝ≥0
hp : p ∈ Icc 0 1
a b : A
hab : a ≤ b
ha : ¬0 ≤ a
⊢ (fun a ↦ a ^ p) a ≤ (fun a ↦ a ^ p) b

Tactic:
have : a ^ p = 0 := cfcₙ_apply_of_not_predicate a ha
    simp [this]

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

Goal state before:
pp: A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
⊢ ConcaveOn ℝ (Ici 0) sqrt

Tactic:
by
  eta_expand
  simp_rw [sqrt_eq_nnrpow]
  exact concaveOn_nnrpow ⟨by norm_num, by norm_num⟩

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

Goal state before:
pp: p x : ℝ
hp : p ∈ Ioo 0 1
hx : 0 ≤ x
⊢ IntegrableOn (fun x_1 ↦ p.rpowIntegrand₀₁ x_1 x) (Ioo 0 1) volume

Tactic:
refine ⟨?meas, ?finite⟩

Goal state after:
case meas
p x : ℝ
hp : p ∈ Ioo 0 1
hx : 0 ≤ x
⊢ AEStronglyMeasurable (fun x_1 ↦ p.rpowIntegrand₀₁ x_1 x) (volume.restrict (Ioo 0 1))

case finite
p x : ℝ
hp : p ∈ Ioo 0 1
hx : 0 ≤ x
⊢ HasFiniteIntegral (fun x_1 ↦ p.rpowIntegrand₀₁ x_1 x) (volume.restrict (Ioo 0 1))
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation

Goal state before:
pp: p x : ℝ
hp : p ∈ Ioo 0 1
hx : 0 ≤ x
⊢ IntegrableOn (fun x_1 ↦ p.rpowIntegrand₀₁ x_1 x) (Ioi 1) volume

Tactic:
refine ⟨?meas, ?finite⟩

Goal state after:
case meas
p x : ℝ
hp : p ∈ Ioo 0 1
hx : 0 ≤ x
⊢ AEStronglyMeasurable (fun x_1 ↦ p.rpowIntegrand₀₁ x_1 x) (volume.restrict (Ioi 1))

case finite
p x : ℝ
hp : p ∈ Ioo 0 1
hx : 0 ≤ x
⊢ HasFiniteIntegral (fun x_1 ↦ p.rpowIntegrand₀₁ x_1 x) (volume.restrict (Ioi 1))
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation

Goal state before:
pp: p t x : ℝ
hx : 0 ≤ x
ht : 0 < t
⊢ p.rpowIntegrand₁₂ t x = x * (p - 1).rpowIntegrand₀₁ t x

Tactic:
by
  grind [rpowIntegrand₁₂, rpowIntegrand₀₁]

Goal state after:
Module: Mathlib.Data.Int.Log

Goal state before:
pp: case inl
R : Type u_1
inst✝³ : Semifield R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorSemiring R
b : ℕ
hb : b ≤ 1
r : R
h : 1 ≤ r
⊢ log b r = 0

Tactic:
log_of_one_le_right _ h,

Goal state after:
case inl
R : Type u_1
inst✝³ : Semifield R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorSemiring R
b : ℕ
hb : b ≤ 1
r : R
h : 1 ≤ r
⊢ ↑(Nat.log b ⌊r⌋₊) = 0
Module: Mathlib.Data.Int.Log

Goal state before:
pp: case inr
R : Type u_1
inst✝³ : Semifield R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorSemiring R
b : ℕ
hb : b ≤ 1
r : R
h : r ≤ 1
⊢ log b r = 0

Tactic:
· rw [log_of_right_le_one _ h, Nat.clog_of_left_le_one hb, Int.ofNat_zero, neg_zero]

Goal state after:
Module: Mathlib.Data.Int.Log

Goal state before:
pp: case inr
R : Type u_1
inst✝³ : Semifield R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorSemiring R
b : ℕ
hb : 1 < b
n : ℕ
⊢ -↑(Nat.clog b ⌈↑(b ^ n)⌉₊) = -↑n

Tactic:
Nat.ceil_natCast,

Goal state after:
case inr
R : Type u_1
inst✝³ : Semifield R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorSemiring R
b : ℕ
hb : 1 < b
n : ℕ
⊢ -↑(Nat.clog b (b ^ n)) = -↑n
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

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

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

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

Tactic:
← rpow_lt_rpow_left_iff hb,

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

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

Tactic:
← rpow_lt_rpow_left_iff hb,

Goal state after:
b x y : ℝ
hb : 1 < b
hy : 0 < y
⊢ b ^ x < b ^ logb b y ↔ b ^ x < y
Module: Mathlib.Analysis.SpecialFunctions.MulExpNegMulSq

Goal state before:
pp: x : ℝ
⊢ -1 ≤ mulExpNegMulSq 1 x

Tactic:
rw [← neg_mulExpNegMulSq_neg, neg_le_neg_iff]
  exact mulExpNegMulSq_one_le_one (-x)

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

Goal state before:
pp: case neg
b : ℕ
r : ℝ
hr✝ : 0 ≤ r
hr : 0 < r
hb : ¬(b ≠ 0 ∧ b ≠ 1)
⊢ ⌊logb (↑b) r⌋ = Int.log b r

Tactic:
← or_iff_not_and_not

Goal state after:
case neg
b : ℕ
r : ℝ
hr✝ : 0 ≤ r
hr : 0 < r
hb : b = 0 ∨ b = 1
⊢ ⌊logb (↑b) r⌋ = Int.log b r
Module: Mathlib.Analysis.SpecialFunctions.Log.Base

Goal state before:
pp: case neg
b : ℕ
r : ℝ
hr✝ : 0 ≤ r
hr : 0 < r
hb : ¬(b ≠ 0 ∧ b ≠ 1)
⊢ ⌈logb (↑b) r⌉ = Int.clog b r

Tactic:
← or_iff_not_and_not

Goal state after:
case neg
b : ℕ
r : ℝ
hr✝ : 0 ≤ r
hr : 0 < r
hb : b = 0 ∨ b = 1
⊢ ⌈logb (↑b) r⌉ = Int.clog b r
Module: Mathlib.Analysis.SpecialFunctions.Pow.NthRootLemmas

Goal state before:
pp: case mp
n : ℕ
hn : n ≠ 0
x : ℕ
⊢ n.nthRoot (x ^ n) ^ n = x ^ n

Tactic:
rw [nthRoot_pow hn]

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

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

Tactic:
by_cases! ha : ∃ j ∈ a, ∃ k : ℕ, j = -k

Goal state after:
case pos
a b : Multiset ℂ
h : a.card ≤ b.card
ha : ∃ j ∈ a, ∃ k, j = -↑k
⊢ (regularizedHGFunSeries a b).radius = ⊤

case neg
a b : Multiset ℂ
h : a.card ≤ b.card
ha : ∀ j ∈ a, ∀ (k : ℕ), j ≠ -↑k
⊢ (regularizedHGFunSeries a b).radius = ⊤
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: L : PeriodPair
l₀ : ℂ
hl₀ : l₀ ∈ L.lattice
l : ↥L.lattice
hl : ↑l / 2 ∉ L.lattice
⊢ ℘[L] (-(↑l / 2) + ↑l) + (1 / ↑⟨l₀, hl₀⟩ ^ 2 - 1 / (-(↑l / 2) + ↑l - ↑⟨l₀, hl₀⟩) ^ 2) =
    ℘[L] (↑l / 2) + (1 / ↑⟨-(l₀ - ↑l), ⋯⟩ ^ 2 - 1 / (↑l / 2 - ↑⟨-(l₀ - ↑l), ⋯⟩) ^ 2 + (1 / l₀ ^ 2 - 1 / (l₀ - ↑l) ^ 2))

Tactic:
congr 2 <;> ring

Goal state after:
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.ContDiff

Goal state before:
pp: case inl
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
inst✝ : CompleteSpace E
h : ContDiffOn ℝ 1 f [[a, b]]
hab : a ≤ b
⊢ ∫ (x : ℝ) in a..b, derivWithin f [[a, b]] x = f b - f a

Tactic:
simp only [uIcc_of_le hab] at h ⊢
    exact integral_derivWithin_Icc_of_contDiffOn_Icc h hab

Goal state after:
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 := ⋯
this : ‖(⇑g ∘ f) b - (⇑g ∘ f) a‖ₑ = ‖f b - f a‖ₑ
⊢ ∀ᵐ (a : ℝ) ∂volume.restrict (Icc a b), ‖deriv (⇑g ∘ f) a‖ₑ ≤ ‖deriv f a‖ₑ

Tactic:
rw [← restrict_Ioo_eq_restrict_Icc]

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ₗᵢ
this : ‖(⇑g ∘ f) b - (⇑g ∘ f) a‖ₑ = ‖f b - f a‖ₑ
⊢ ∀ᵐ (a : ℝ) ∂volume.restrict (Ioo a b), ‖deriv (⇑g ∘ f) a‖ₑ ≤ ‖deriv f a‖ₑ
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
⊢ (fun a ↦ ‖deriv f a‖ₑ) =ᵐ[volume.restrict (Icc a b)] fun a_1 ↦ ‖derivWithin f (Icc a b) a_1‖ₑ

Tactic:
rw [← restrict_Ioo_eq_restrict_Icc]

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
⊢ (fun a ↦ ‖deriv f a‖ₑ) =ᵐ[volume.restrict (Ioo a b)] fun a_1 ↦ ‖derivWithin f (Icc a b) a_1‖ₑ
Module: Mathlib.Analysis.SpecialFunctions.Stirling

Goal state before:
pp: n : ℕ
hn : n ≠ 0
this : 4 = 2 * 2
⊢ (↑n ! / (√(2 * ↑n) * (↑n / rexp 1) ^ n)) ^ (2 * 2) / stirlingSeq (2 * n) ^ 2 * (↑n / (2 * ↑n + 1)) = Wallis.W n

Tactic:
pow_mul,

Goal state after:
n : ℕ
hn : n ≠ 0
this : 4 = 2 * 2
⊢ ((↑n ! / (√(2 * ↑n) * (↑n / rexp 1) ^ n)) ^ 2) ^ 2 / stirlingSeq (2 * n) ^ 2 * (↑n / (2 * ↑n + 1)) = Wallis.W n
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.ChebyshevGauss

Goal state before:
pp: case inr.h
n : ℕ
k : ℤ
hk : ¬2 * ↑n ∣ k
hn : n ≠ 0
this : (-1) ^ (-k) = (-1) ^ k
z : ℂ := Complex.exp (↑k / (2 * ↑n) * ↑π * I)
hz : z = Complex.exp (↑k / (2 * ↑n) * ↑π * I)
hz₂ : Complex.exp (↑k / ↑n * ↑π * I) = z ^ 2
⊢ z / (z ^ 2 - 1) + z⁻¹ / ((z ^ 2)⁻¹ - 1) = 0

Tactic:
← inv_pow z 2

Goal state after:
case inr.h
n : ℕ
k : ℤ
hk : ¬2 * ↑n ∣ k
hn : n ≠ 0
this : (-1) ^ (-k) = (-1) ^ k
z : ℂ := Complex.exp (↑k / (2 * ↑n) * ↑π * I)
hz : z = Complex.exp (↑k / (2 * ↑n) * ↑π * I)
hz₂ : Complex.exp (↑k / ↑n * ↑π * I) = z ^ 2
⊢ z / (z ^ 2 - 1) + z⁻¹ / (z⁻¹ ^ 2 - 1) = 0
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable

Goal state before:
pp: z : ℍ
⊢ r1 z = 1 / ((z.re / z.im) ^ 2 + 1)

Tactic:
by
  rw [div_pow, div_add_one (by positivity), one_div_div, r1]

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

Goal state before:
pp: case hbc.inl
z : ℍ
x : Fin 2 → ℤ
hx : x ≠ 0
hn0 : ‖x‖ ≠ 0
h11 : ↑(x 0) * ↑z + ↑(x 1) = (↑(x 0) / ↑‖x‖ * ↑z + ↑(x 1) / ↑‖x‖) * ↑‖x‖
H1 : 1 ≤ (↑(x 0) / ‖x‖) ^ 2
⊢ r z ≤ ‖↑(x 0) / ↑↑(max (x 0).natAbs (x 1).natAbs) * ↑z + ↑(x 1) / ↑↑(max (x 0).natAbs (x 1).natAbs)‖

Tactic:
simpa only [norm_eq_max_natAbs, ofReal_div, ofReal_intCast] using auxbound1 z (x 1 / ‖x‖) H1

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

Goal state before:
pp: n : ℕ
hn : n ≠ 0
x : ℝ
hx : |x| ≤ 1
k : ℕ
hk : ↑k * π = ↑n * arccos x
hk' : ↑k = ↑n * (arccos x / π)
hkn : ↑k ≤ ↑n
⊢ k ≤ n

Tactic:
simpa using hkn

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

Goal state before:
pp: case refine_3
n k : ℕ
hn : n ≠ 0
hk₀ : 0 < k
hk₁ : k < n
hk₂ : Even k
zero_lt : 0 < ↑k * π / ↑n
lt_pi : ↑k * π / ↑n < π
⊢ cos (↑k * π / ↑n) < 1

Tactic:
rw [← cos_zero]
    exact cos_lt_cos_of_nonneg_of_le_pi (le_refl 0) (le_of_lt lt_pi) zero_lt

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

Goal state before:
pp: case refine_3
n k : ℕ
hn : n ≠ 0
hk₁ : k < n
hk₂ : Odd k
k_pos : 0 < k
zero_lt : 0 < ↑k * π / ↑n
lt_pi : ↑k * π / ↑n < π
⊢ cos (↑k * π / ↑n) < 1

Tactic:
rw [← cos_zero]
    exact cos_lt_cos_of_nonneg_of_le_pi (le_refl 0) (le_of_lt lt_pi) zero_lt

Goal state after:
Module: Mathlib.Analysis.SpecificLimits.ArithmeticGeometric

Goal state before:
pp: R : Type u_1
a b u₀ : R
inst✝⁵ : Field R
inst✝⁴ : LinearOrder R
inst✝³ : IsStrictOrderedRing R
inst✝² : Archimedean R
inst✝¹ : TopologicalSpace R
inst✝ : OrderTopology R
ha_pos : 0 ≤ a
ha : a < 1
⊢ Tendsto (fun n ↦ a ^ n * (u₀ - b / (1 - a))) atTop (𝓝 0)

Tactic:
conv_rhs => rw [← zero_mul (u₀ - (b / (1 - a)))]

Goal state after:
R : Type u_1
a b u₀ : R
inst✝⁵ : Field R
inst✝⁴ : LinearOrder R
inst✝³ : IsStrictOrderedRing R
inst✝² : Archimedean R
inst✝¹ : TopologicalSpace R
inst✝ : OrderTopology R
ha_pos : 0 ≤ a
ha : a < 1
⊢ Tendsto (fun n ↦ a ^ n * (u₀ - b / (1 - a))) atTop (𝓝 (0 * (u₀ - b / (1 - a))))