mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Real.OfDigits

Goal state before:
pp: x : ℝ
b : ℕ
inst✝ : NeZero b
hx : x ∈ Set.Ico 0 1
n : ℕ
⊢ ↑b ^ n * ∑ i ∈ Finset.range n, ofDigitsTerm (x.digits b) i = ↑⌊↑b ^ n * x⌋₊

Tactic:
have := NeZero.ne b

Goal state after:
x : ℝ
b : ℕ
inst✝ : NeZero b
hx : x ∈ Set.Ico 0 1
n : ℕ
this : b ≠ 0
⊢ ↑b ^ n * ∑ i ∈ Finset.range n, ofDigitsTerm (x.digits b) i = ↑⌊↑b ^ n * x⌋₊
Module: Mathlib.Analysis.Real.OfDigits

Goal state before:
pp: case succ
x : ℝ
b : ℕ
inst✝ : NeZero b
hx : x ∈ Set.Ico 0 1
this : b ≠ 0
n : ℕ
ih : ↑b ^ n * ∑ i ∈ Finset.range n, ofDigitsTerm (x.digits b) i = ↑⌊↑b ^ n * x⌋₊
⊢ ↑b * ↑b ^ n * ∑ x_1 ∈ Finset.range n, ofDigitsTerm (x.digits b) x_1 + ↑b * ↑b ^ n * ofDigitsTerm (x.digits b) n =
    ↑⌊↑b * ↑b ^ n * x⌋₊

Tactic:
mul_assoc,

Goal state after:
case succ
x : ℝ
b : ℕ
inst✝ : NeZero b
hx : x ∈ Set.Ico 0 1
this : b ≠ 0
n : ℕ
ih : ↑b ^ n * ∑ i ∈ Finset.range n, ofDigitsTerm (x.digits b) i = ↑⌊↑b ^ n * x⌋₊
⊢ ↑b * (↑b ^ n * ∑ x_1 ∈ Finset.range n, ofDigitsTerm (x.digits b) x_1) + ↑b * ↑b ^ n * ofDigitsTerm (x.digits b) n =
    ↑⌊↑b * ↑b ^ n * x⌋₊
Module: Mathlib.Analysis.Real.Pi.Bounds

Goal state before:
pp: case e_a
n : ℕ
this : π < (√(2 - sqrtTwoAddSeries 0 n) / 2 + 1 / (2 ^ n) ^ 3 / 4) * 2 ^ (n + 2)
⊢ 2 ^ (2 + (n * 2 + n)) = 2 ^ (2 + (2 * n + n))

Tactic:
mul_comm n

Goal state after:
case e_a
n : ℕ
this : π < (√(2 - sqrtTwoAddSeries 0 n) / 2 + 1 / (2 ^ n) ^ 3 / 4) * 2 ^ (n + 2)
⊢ 2 ^ (2 + (2 * n + n)) = 2 ^ (2 + (2 * n + n))
Module: Mathlib.Analysis.Real.Pi.Bounds

Goal state before:
pp: ⊢ 3 < π

Tactic:
by
  -- bound[3, Iters -> 1, Rounding -> 2, Precision -> 3]
  pi_lower_bound [23 / 16]

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

Goal state before:
pp: z : ℤ
⊢ Irrational √↑z ↔ ¬IsSquare z ∧ 0 ≤ z

Tactic:
← Rat.cast_intCast,

Goal state after:
z : ℤ
⊢ Irrational √↑↑z ↔ ¬IsSquare z ∧ 0 ≤ z
Module: Mathlib.NumberTheory.Real.Irrational

Goal state before:
pp: x : ℝ
h : Irrational x
q : ℚ
hq : q ≠ 0
⊢ Irrational (x * ↑q * ↑q⁻¹)

Tactic:
mul_assoc,

Goal state after:
x : ℝ
h : Irrational x
q : ℚ
hq : q ≠ 0
⊢ Irrational (x * (↑q * ↑q⁻¹))
Module: Mathlib.Analysis.Real.Pi.Leibniz

Goal state before:
pp: case hfa
⊢ Antitone fun i ↦ (2 * ↑i + 1)⁻¹

Tactic:
exact antitone_iff_forall_lt.mpr fun _ _ _ ↦ by gcongr

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
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) θ

Tactic:
have hv₁d : Continuous v₁' := 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₁'
hv₁d : Continuous v₁'
⊢ (∫ (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.Leibniz

Goal state before:
pp: case right
l : ℝ
h : Tendsto (fun n ↦ ∑ i ∈ range n, (-1) ^ i / (2 * ↑i + 1)) atTop (𝓝 l)
m : 𝓝[<] 1 ≤ 𝓝 1
q : Tendsto (fun x ↦ x ^ 2) (𝓝[<] 1) (𝓝[<] 1)
abel : Tendsto (fun x ↦ ((fun x ↦ ∑' (n : ℕ), (-1) ^ n / (2 * ↑n + 1) * x ^ n) ∘ fun x ↦ x ^ 2) x * x) (𝓝[<] 1) (𝓝 l)
y : ℝ
hy1 : y - 1 < 1 ∧ 1 - y < 1
hy2 : y < 1
ny : ‖y‖ < 1
⊢ ∑' (x : ℕ), (-1) ^ x / (2 * ↑x + 1) * (y ^ 2) ^ x * y = ∑' (b : ℕ), (-1) ^ b * y ^ (2 * b + 1) / ↑(2 * b + 1)

Tactic:
mul_assoc,

Goal state after:
case right
l : ℝ
h : Tendsto (fun n ↦ ∑ i ∈ range n, (-1) ^ i / (2 * ↑i + 1)) atTop (𝓝 l)
m : 𝓝[<] 1 ≤ 𝓝 1
q : Tendsto (fun x ↦ x ^ 2) (𝓝[<] 1) (𝓝[<] 1)
abel : Tendsto (fun x ↦ ((fun x ↦ ∑' (n : ℕ), (-1) ^ n / (2 * ↑n + 1) * x ^ n) ∘ fun x ↦ x ^ 2) x * x) (𝓝[<] 1) (𝓝 l)
y : ℝ
hy1 : y - 1 < 1 ∧ 1 - y < 1
hy2 : y < 1
ny : ‖y‖ < 1
⊢ ∑' (x : ℕ), (-1) ^ x / (2 * ↑x + 1) * ((y ^ 2) ^ x * y) = ∑' (b : ℕ), (-1) ^ b * y ^ (2 * b + 1) / ↑(2 * b + 1)
Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy

Goal state before:
pp: p✝ p : ℝ
hp : p < 0
hp' : ¬p < -1
h : -1 < p
⊢ -p * log p ≤ 0

Tactic:
· nlinarith [log_neg_of_lt_zero hp h]

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

Goal state before:
pp: case refine_2.inr
p : ℝ
h : p ≠ 2⁻¹
this : ∀ {p : ℝ}, p ≠ 2⁻¹ → p < 2⁻¹ → binEntropy p < log 2
hp : ¬p < 2⁻¹
⊢ binEntropy p < log 2

pp: p✝ p : ℝ
h : p ≠ 2⁻¹
hp : p < 2⁻¹
⊢ binEntropy p < log 2

Tactic:
· have hp : 1 - p < 2⁻¹ := by
      rw [sub_lt_comm]; norm_num at *; linarith +splitNe
    rw [← binEntropy_one_sub]
    exact this hp.ne hp

Goal state after:
p✝ p : ℝ
h : p ≠ 2⁻¹
hp : p < 2⁻¹
⊢ binEntropy p < log 2
Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy

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

Tactic:
· have : p = 0 ∨ p = 1 := Decidable.or_iff_not_not_and_not.mpr is_x_where_nondiff
    rw [deriv_zero_of_not_differentiableAt]
    · 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]
    · intro h
      have contAt := h.continuousAt
      cases this <;>
        simp_all [not_continuousAt_deriv_qaryEntropy_zero, not_continuousAt_deriv_qaryEntropy_one]

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

Goal state before:
pp: case inr
p : ℤ[X]
a b : ℤ
k : ℕ
hp : p.natDegree ≤ k
hb : b ≠ 0
i : ℕ
hi : i ∈ p.support
ik : i ≤ k
⊢ ↑(p.coeff i) * (↑a ^ i / ↑b ^ i) * ↑b ^ k = ↑(p.coeff i) * ↑a ^ i * ↑b ^ (k - i)

Tactic:
mul_assoc,

Goal state after:
case inr
p : ℤ[X]
a b : ℤ
k : ℕ
hp : p.natDegree ≤ k
hb : b ≠ 0
i : ℕ
hi : i ∈ p.support
ik : i ≤ k
⊢ ↑(p.coeff i) * (↑a ^ i / ↑b ^ i * ↑b ^ k) = ↑(p.coeff i) * ↑a ^ i * ↑b ^ (k - i)
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Order

Goal state before:
pp: A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
⊢ Monotone sqrt

Tactic:
by
  intro a b hab
  rw [CFC.sqrt_eq_nnrpow a, CFC.sqrt_eq_nnrpow b]
  refine (monotone_nnrpow (A := A) ?_) hab
  constructor <;> norm_num

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

Goal state before:

Tactic:
_ = ‖p⁻¹ * ((x ^ p - 1) - p * log x)‖ := by grind
    _ = p⁻¹ * ‖(rexp (p * log x) - 1) - p * log x‖ := by
          simp only [norm_mul, Real.norm_of_nonneg (r := p⁻¹) pinv_nonneg]
          congr
          rw [mul_comm, Real.exp_mul, Real.exp_log (by grind)]
    _ ≤ p⁻¹ * ‖p * log x‖ ^ 2 := by
          gcongr
          refine Real.norm_exp_sub_one_sub_id_le ?_
          simp only [hx]
    _ = p * ‖log x‖ ^ 2 := by
          simp only [norm_mul]
          grind [Real.norm_of_nonneg]

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

Goal state before:
pp: s : ℂ
hs : s ≠ 0
⊢ (s + 2).Gammaℝ = s.Gammaℝ * s / 2 / ↑π

Tactic:
Gammaℝ_def,

Goal state after:
s : ℂ
hs : s ≠ 0
⊢ ↑π ^ (-(s + 2) / 2) * Gamma ((s + 2) / 2) = s.Gammaℝ * s / 2 / ↑π
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Deligne

Goal state before:
pp: s : ℂ
hs : s ≠ 0
⊢ ↑π ^ (-(s + 2) / 2) * Gamma ((s + 2) / 2) = s.Gammaℝ * s / 2 / ↑π

Tactic:
Gammaℝ_def,

Goal state after:
s : ℂ
hs : s ≠ 0
⊢ ↑π ^ (-(s + 2) / 2) * Gamma ((s + 2) / 2) = ↑π ^ (-s / 2) * Gamma (s / 2) * s / 2 / ↑π
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Deligne

Goal state before:
pp: ⊢ Gammaℝ 1 = 1

Tactic:
Gammaℝ_def,

Goal state after:
⊢ ↑π ^ (-1 / 2) * Gamma (1 / 2) = 1
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Deligne

Goal state before:
pp: s : ℂ
⊢ ↑π ^ (-s / 2 + -(s + 1) / 2) * (Gamma (2 * (s / 2)) * 2 ^ (1 - 2 * (s / 2)) * ↑π ^ (1 / ↑2)) =
    2 ^ (1 - s) * (↑π ^ (-1 / 2 - s) * ↑π ^ (1 / 2)) * Gamma s

Tactic:
ofReal_ofNat

Goal state after:
s : ℂ
⊢ ↑π ^ (-s / 2 + -(s + 1) / 2) * (Gamma (2 * (s / 2)) * 2 ^ (1 - 2 * (s / 2)) * ↑π ^ (1 / 2)) =
    2 ^ (1 - s) * (↑π ^ (-1 / 2 - s) * ↑π ^ (1 / 2)) * Gamma s
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation

Goal state before:
pp: p x : ℝ
hp : p ∈ Ioo 0 1
hx : 0 ≤ x
t : ℝ
ht : t ∈ Ioo 0 1
⊢ p.rpowIntegrand₀₁ t x ≤ t ^ (p - 1)

Tactic:
exact rpowIntegrand₀₁_le_rpow_sub_one hp (le_of_lt ht.1) hx

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

Goal state before:
pp: s : ℂ
⊢ 2 * 2 ^ (-s) * ↑π ^ (-1 / 2 - s + 1 / 2) * Gamma s = 2 * (↑2 ^ (-s) * ↑π ^ (-s)) * Gamma s

Tactic:
ofReal_ofNat

Goal state after:
s : ℂ
⊢ 2 * 2 ^ (-s) * ↑π ^ (-1 / 2 - s + 1 / 2) * Gamma s = 2 * (2 ^ (-s) * ↑π ^ (-s)) * Gamma s
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Deligne

Goal state before:
pp: s : ℂ
⊢ 2 * (↑2 * ↑π) ^ (-s) * Gamma s = 2 * (2 * ↑π) ^ (-s) * Gamma s

Tactic:
ofReal_ofNat

Goal state after:
s : ℂ
⊢ 2 * (2 * ↑π) ^ (-s) * Gamma s = 2 * (2 * ↑π) ^ (-s) * Gamma s
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation

Goal state before:
pp: p x : ℝ
hp : p ∈ Ioo 0 1
hx : 0 ≤ x
h✝ : 0 < x
this : ∫ (t : ℝ) in Ioi 0, p.rpowIntegrand₀₁ t 1 ≠ 0
⊢ x ^ p = (x ^ p * ∫ (t : ℝ) in Ioi 0, p.rpowIntegrand₀₁ t 1) * (∫ (t : ℝ) in Ioi 0, p.rpowIntegrand₀₁ t 1)⁻¹

Tactic:
mul_assoc,

Goal state after:
p x : ℝ
hp : p ∈ Ioo 0 1
hx : 0 ≤ x
h✝ : 0 < x
this : ∫ (t : ℝ) in Ioi 0, p.rpowIntegrand₀₁ t 1 ≠ 0
⊢ x ^ p = x ^ p * ((∫ (t : ℝ) in Ioi 0, p.rpowIntegrand₀₁ t 1) * (∫ (t : ℝ) in Ioi 0, p.rpowIntegrand₀₁ t 1)⁻¹)
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation

Goal state before:
pp: case refine_2
p : ℝ
hp : p ∈ Ioo 1 2
C : ℝ≥0 := NNReal.mk (∫ (t : ℝ) in Ioi 0, (p - 1).rpowIntegrand₀₁ t 1)⁻¹ ⋯
μ : Measure ℝ := C • volume
x : ℝ
hx : x ∈ Ici 0
⊢ x ^ p = ∫ (t : ℝ) in Ioi 0, p.rpowIntegrand₁₂ t x ∂μ

Tactic:
rw [Measure.restrict_smul, integral_smul_nnreal_measure,
      rpow_eq_const_mul_integral_rpowIntegrand₁₂ hp hx]

Goal state after:
case refine_2
p : ℝ
hp : p ∈ Ioo 1 2
C : ℝ≥0 := NNReal.mk (∫ (t : ℝ) in Ioi 0, (p - 1).rpowIntegrand₀₁ t 1)⁻¹ ⋯
μ : Measure ℝ := C • volume
x : ℝ
hx : x ∈ Ici 0
⊢ (∫ (t : ℝ) in Ioi 0, (p - 1).rpowIntegrand₀₁ t 1)⁻¹ * ∫ (t : ℝ) in Ioi 0, p.rpowIntegrand₁₂ t x =
    C • ∫ (x_1 : ℝ) in Ioi 0, p.rpowIntegrand₁₂ x_1 x ∂volume
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Digamma

Goal state before:
pp: s : ℂ
hs : ∀ (m : ℕ), s ≠ -↑m
⊢ (s + 1).digamma = s.digamma + s⁻¹

Tactic:
by
  have hs0 : s ≠ 0 := by simpa using hs 0
  rw [digamma_def, logDeriv_apply, logDeriv_apply, deriv_Gamma_add_one s hs0, Gamma_add_one s hs0,
    add_div, div_mul_cancel_right₀ (Gamma_ne_zero hs), mul_div_mul_left _ _ hs0, add_comm]

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
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‖
hf : ContinuousOn (Function.uncurry f) (Ioi 0 ×ˢ quasispectrum ℝ a)
t : ℝ
ht : t ∈ Ioi 0
z : ℝ
hz : z ∈ quasispectrum ℝ a
hz' : 0 ≤ z
⊢ ‖(↑p).rpowIntegrand₀₁ t z‖ ≤ ‖(↑p).rpowIntegrand₀₁ t maxr‖

Tactic:
Real.norm_of_nonneg (rpowIntegrand₀₁_nonneg p_pos (le_of_lt ht) hz'),

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‖
hf : ContinuousOn (Function.uncurry f) (Ioi 0 ×ˢ quasispectrum ℝ a)
t : ℝ
ht : t ∈ Ioi 0
z : ℝ
hz : z ∈ quasispectrum ℝ a
hz' : 0 ≤ z
⊢ (↑p).rpowIntegrand₀₁ t z ≤ ‖(↑p).rpowIntegrand₀₁ t maxr‖
Module: Mathlib.NumberTheory.Harmonic.GammaDeriv

Goal state before:
pp: f : ℂ → ℂ := fun s ↦ ↑π ^ (-s / 2)
g : ℂ → ℂ := fun s ↦ Gamma (s / 2)
⊢ ↑π ^ (1 / 2) = ↑π ^ (1 / ↑2)

Tactic:
ofReal_ofNat

Goal state after:
f : ℂ → ℂ := fun s ↦ ↑π ^ (-s / 2)
g : ℂ → ℂ := fun s ↦ Gamma (s / 2)
⊢ ↑π ^ (1 / 2) = ↑π ^ (1 / 2)
Module: Mathlib.NumberTheory.Harmonic.GammaDeriv

Goal state before:
pp: f : ℂ → ℂ := fun s ↦ ↑π ^ (-s / 2)
g : ℂ → ℂ := fun s ↦ Gamma (s / 2)
aux : ↑π ^ (1 / 2) = ↑√π
aux2 : ↑√π ≠ 0
this : HasDerivAt (fun x ↦ ↑π ^ (-x / 2)) (↑π ^ (-1 / 2) * log ↑π * (-1 / 2)) 1
⊢ ↑π ^ (-1 / 2) * log ↑π * (-1 / 2) = -log ↑π / 2 / ↑√π

Tactic:
mul_assoc,

Goal state after:
f : ℂ → ℂ := fun s ↦ ↑π ^ (-s / 2)
g : ℂ → ℂ := fun s ↦ Gamma (s / 2)
aux : ↑π ^ (1 / 2) = ↑√π
aux2 : ↑√π ≠ 0
this : HasDerivAt (fun x ↦ ↑π ^ (-x / 2)) (↑π ^ (-1 / 2) * log ↑π * (-1 / 2)) 1
⊢ ↑π ^ (-1 / 2) * (log ↑π * (-1 / 2)) = -log ↑π / 2 / ↑√π
Module: Mathlib.Analysis.SpecialFunctions.MulExpNegMulSq

Goal state before:
pp: x : ℝ
⊢ x * rexp (-(x * x)) ≤ 1

Tactic:
rw [← le_div_iff₀ (exp_pos (-(x * x))), exp_neg, div_inv_eq_mul, one_mul]

Goal state after:
x : ℝ
⊢ x ≤ rexp (x * x)
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:
by
  simpa [sub_div] using! (tendsto_log_comp_add_sub_log y).div_const (log b)

Goal state after:
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 + -((↑n)⁻¹ * (ε * g x * g x))| ≤ 1

Tactic:
mul_assoc,

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 + -((↑n)⁻¹ * (ε * (g x * g x)))| ≤ 1
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: L : PeriodPair
l₀ z : ℂ
⊢ ℘'[L - l₀] (-z) = -℘'[L - -l₀] z

Tactic:
simp only [derivWeierstrassPExcept]

Goal state after:
L : PeriodPair
l₀ z : ℂ
⊢ (∑' (l : ↥L.lattice), if ↑l = l₀ then 0 else -2 / (-z - ↑l) ^ 3) =
    -∑' (l : ↥L.lattice), if ↑l = -l₀ then 0 else -2 / (z - ↑l) ^ 3
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: L : PeriodPair
l₀ z : ℂ
l : ↥L.lattice
⊢ ℘'[L - l₀] (z + ↑l) = ℘'[L - l₀ - ↑l] z

Tactic:
simp only [derivWeierstrassPExcept]

Goal state after:
L : PeriodPair
l₀ z : ℂ
l : ↥L.lattice
⊢ (∑' (l_1 : ↥L.lattice), if ↑l_1 = l₀ then 0 else -2 / (z + ↑l - ↑l_1) ^ 3) =
    ∑' (l_1 : ↥L.lattice), if ↑l_1 = l₀ - ↑l then 0 else -2 / (z - ↑l_1) ^ 3
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Basic

Goal state before:
pp: θ : ℂ
n : ℤ
⊢ sinh ((↑n + 1) * θ) * I * -I = sinh ((↑n + 1) * θ)

Tactic:
mul_assoc,

Goal state after:
θ : ℂ
n : ℤ
⊢ sinh ((↑n + 1) * θ) * (I * -I) = sinh ((↑n + 1) * θ)
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.ContDiff

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

Tactic:
rw [← integral_deriv_of_contDiffOn_Icc h hab]

Goal state after:
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
inst✝ : CompleteSpace E
h : ContDiffOn ℝ 1 f (Icc a b)
hab : a ≤ b
⊢ ∫ (x : ℝ) in a..b, derivWithin f (Icc a b) x = ∫ (x : ℝ) in a..b, deriv f x
Module: Mathlib.NumberTheory.Niven

Goal state before:
pp: q : ℚ
⊢ IsIntegral ℤ (2 * sin (↑q * ↑π))

Tactic:
by
  rw [sin.eq_1, mul_div_cancel₀ _ two_ne_zero]
  exact (isIntegral_exp_neg_rat_mul_pi_mul_I q).sub (isIntegral_exp_rat_mul_pi_mul_I q)
    |>.mul isIntegral_int_I

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

Goal state before:
pp: n : ℕ
hn : n ≠ 0
c : ℕ → ℝ
hP : (∑ i ∈ range (2 * n), c i • ↑(chebyshevTsequence ℝ) i).degree < 2 * ↑n
i : ℕ
hrange : i ∈ range (2 * n)
hi : i = 0
⊢ π = sumZeroes n (T ℝ 0)

Tactic:
sumZeroes_T_zero hn

Goal state after:
n : ℕ
hn : n ≠ 0
c : ℕ → ℝ
hP : (∑ i ∈ range (2 * n), c i • ↑(chebyshevTsequence ℝ) i).degree < 2 * ↑n
i : ℕ
hrange : i ∈ range (2 * n)
hi : i = 0
⊢ π = π
Module: Mathlib.Order.Interval.Finset.Box

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹⁰ : Ring α
inst✝⁹ : PartialOrder α
inst✝⁸ : IsOrderedRing α
inst✝⁷ : Ring β
inst✝⁶ : PartialOrder β
inst✝⁵ : IsOrderedRing β
inst✝⁴ : LocallyFiniteOrder α
inst✝³ : LocallyFiniteOrder β
inst✝² : DecidableEq α
inst✝¹ : DecidableEq β
inst✝ : DecidableLE (α × β)
n : ℕ
⊢ #(Icc (-1 + -↑n) (↑n + 1)) * #(Icc ((-1).2 + (-↑n).2) ((↑n).2 + 1.2)) - #(Icc (-↑n) ↑n) * #(Icc (-↑n).2 (↑n).2) =
    #(Icc (-1 + -↑n) (↑n + 1)) * #(Icc (-1 + -↑n) (↑n + 1)) - #(Icc (-↑n) ↑n) * #(Icc (-↑n) ↑n)

Tactic:
snd_neg,

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹⁰ : Ring α
inst✝⁹ : PartialOrder α
inst✝⁸ : IsOrderedRing α
inst✝⁷ : Ring β
inst✝⁶ : PartialOrder β
inst✝⁵ : IsOrderedRing β
inst✝⁴ : LocallyFiniteOrder α
inst✝³ : LocallyFiniteOrder β
inst✝² : DecidableEq α
inst✝¹ : DecidableEq β
inst✝ : DecidableLE (α × β)
n : ℕ
⊢ #(Icc (-1 + -↑n) (↑n + 1)) * #(Icc (-1.2 + -(↑n).2) ((↑n).2 + 1.2)) - #(Icc (-↑n) ↑n) * #(Icc (-(↑n).2) (↑n).2) =
    #(Icc (-1 + -↑n) (↑n + 1)) * #(Icc (-1 + -↑n) (↑n + 1)) - #(Icc (-↑n) ↑n) * #(Icc (-↑n) ↑n)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema

Goal state before:
pp: n : ℤ
x : ℝ
hx : x ∈ Set.Icc (-1) 1
⊢ eval x (T ℝ n) ∈ Set.Icc (-1) 1

Tactic:
rw [← cos_arccos (x := x) (by grind) (by grind)]

Goal state after:
n : ℤ
x : ℝ
hx : x ∈ Set.Icc (-1) 1
⊢ eval (cos (arccos x)) (T ℝ n) ∈ Set.Icc (-1) 1
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema

Goal state before:
pp: n : ℤ
hn : n ≠ 0
x : ℝ
hx : 1 < |x|
h : 0 ≤ x
⊢ 1 < |eval x (T ℝ n)|

Tactic:
· exact one_lt_eval_T_real hn (abs_of_nonneg h ▸ hx) |>.trans_le <| le_abs_self _

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

Goal state before:
pp: n k i : ℕ
hk₁ : 0 < k
hk₂ : k ≤ n
hi : i ≤ n
x : ℝ
hx : 1 ≤ x
⊢ 0 < (-1) ^ i * iterateDerivativeC n k x i

Tactic:
rw [iterateDerivativeC, ← mul_assoc]
  refine mul_pos ?_ (Finset.sum_pos' ?_ ?_)
  · rw [← mul_assoc, mul_comm (a := (-1) ^ i), mul_assoc]
    exact mul_pos (Nat.cast_pos.mpr <| Nat.factorial_pos k) (negOnePow_mul_leadingCoeffC_pos hi)
  · exact fun t _ => Finset.prod_nonneg (fun a _ => by grind [show node n a ≤ 1 from cos_le_one _])
  · have : ∃ s ⊆ (Finset.range (n + 1)).erase i, s.card = n - k ∧ 0 ∉ s := by
      by_cases 1 ≤ i ∧ i ≤ n - k
      case neg => exact ⟨Finset.Icc 1 (n - k), by grind, by grind [Nat.card_Icc], by simp⟩
      case pos => exact ⟨(Finset.Icc 1 (n - k + 1)).erase i, by grind, by grind [Nat.card_Icc],
        by simp⟩
    obtain ⟨s, hs, hscard, hsn⟩ := this
    refine ⟨s, by simp [hs, hscard], Finset.prod_pos (fun a ha => ?_)⟩
    grind [show node n a < 1 by rw [← node_eq_one (n := n)]; exact node_lt (by grind) (by grind)]

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

Goal state before:
pp: z : ℍ
k : ℝ
hk : 0 ≤ k
x : Fin 2 → ℤ
⊢ ‖↑(x 0) * ↑z + ↑(x 1)‖ ^ (-k) ≤ r z ^ (-k) * ‖x‖ ^ (-k)

Tactic:
by_cases hx : x = 0
  · simp only [hx, Pi.zero_apply, Int.cast_zero, zero_mul, add_zero, norm_zero]
    by_cases h : -k = 0
    · rw [h, Real.rpow_zero, Real.rpow_zero, one_mul]
    · rw [Real.zero_rpow h, mul_zero]
  · rw [← Real.mul_rpow (r_pos _).le (norm_nonneg _)]
    exact Real.rpow_le_rpow_of_nonpos (mul_pos (r_pos _) (norm_pos_iff.mpr hx)) (r_mul_max_le z hx)
      (neg_nonpos.mpr hk)

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

Goal state before:
pp: n : ℕ
⊢ (Multiset.map (fun k ↦ cos ((↑k + 1) * π / (↑n + 1))) (Multiset.range n)).Nodup

Tactic:
refine (Finset.range n).nodup_map_iff_injOn.mpr ?_
  apply injOn_cos.comp
  · intro x hx y hy hxy
    field_simp at hxy
    aesop
  · refine fun k hk => Set.mem_Icc.mpr ⟨by positivity, ?_⟩
    field_simp
    norm_cast
    grind

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent

Goal state before:
pp: z : ℂ
⊢ cexp (z * I) + cexp (-z * I) = cexp (-(z * I)) * (cexp (2 * I * z) + 1)

Tactic:
rw [mul_add, ← Complex.exp_add]

Goal state after:
z : ℂ
⊢ cexp (z * I) + cexp (-z * I) = cexp (-(z * I) + 2 * I * z) + cexp (-(z * I)) * 1
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent

Goal state before:
pp: z : ℂ
h1 : cexp (z * I) + cexp (-z * I) = cexp (-(z * I)) * (cexp (2 * I * z) + 1)
⊢ cexp (-(z * I)) - cexp (z * I) = cexp (-(z * I)) - cexp (-(z * I)) * cexp (z * I * 2)

Tactic:
mul_assoc,

Goal state after:
z : ℂ
h1 : cexp (z * I) + cexp (-z * I) = cexp (-(z * I)) * (cexp (2 * I * z) + 1)
⊢ cexp (-(z * I)) - cexp (z * I) = cexp (-(z * I)) - cexp (-(z * I)) * cexp (z * (I * 2))
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent

Goal state before:
pp: x : ℂ
hz : x ∈ ℂ_ℤ
this : Summable fun i ↦ (x - ↑i)⁻¹ * (x + ↑i)⁻¹
⊢ Summable fun i ↦ 1 / ((x + (↑i + 1)) * (x - (↑i + 1)))

Tactic:
rw [← summable_nat_add_iff 1] at this

Goal state after:
x : ℂ
hz : x ∈ ℂ_ℤ
this : Summable fun n ↦ (x - ↑(n + 1))⁻¹ * (x + ↑(n + 1))⁻¹
⊢ Summable fun i ↦ 1 / ((x + (↑i + 1)) * (x - (↑i + 1)))
Module: Mathlib.NumberTheory.Real.GoldenRatio

Goal state before:

Tactic:
(1 + √5) / 2 < (1 + 3) / 2 := by gcongr; rw [sqrt_lt'] <;> norm_num
  _ = 2 := by norm_num

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

Goal state before:
pp: this : fibRec.IsSolution ((fun n ↦ (√5)⁻¹ * φ ^ n) - fun n ↦ (√5)⁻¹ * ψ ^ n)
⊢ fibRec.IsSolution fun n ↦ (φ ^ n - ψ ^ n) / √5

Tactic:
by
      convert! this
      rw [Pi.sub_apply]
      ring

Goal state after:
Module: Mathlib.Analysis.SumIntegralExpDecay

Goal state before:
pp: k : ℕ
M c : ℝ
hM : 0 ≤ M
hc : 0 < c
hk : 0 < ↑k + 1
key : ∫ (t : ℝ) in Ioi 0, t ^ (↑k + 1 - 1) * rexp (-(c * t)) = (1 / c) ^ (↑k + 1) * Gamma (↑k + 1)
hint : IntegrableOn (fun x ↦ x ^ (↑k + 1 - 1) * rexp (-(c * x))) (Ioi 0) volume
x : ℝ
hx : x ∈ Ioi 0
⊢ 0 x ≤ x ^ (↑k + 1 - 1) * rexp (-(c * x))

Tactic:
exact mul_nonneg (rpow_nonneg hx.le _) (exp_nonneg _)

Goal state after: