mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.NumberTheory.Real.Irrational

Goal state before:
pp: x : ℝ
h : Irrational (-x)
x✝ : x ∈ Set.range Rat.cast
q : ℚ
hx : ↑q = x
⊢ -↑q = -x

Tactic:
hx

Goal state after:
x : ℝ
h : Irrational (-x)
x✝ : x ∈ Set.range Rat.cast
q : ℚ
hx : ↑q = x
⊢ -x = -x
Module: Mathlib.NumberTheory.Real.Irrational

Goal state before:
pp: n : ℕ
x : ℝ
⊢ Irrational (x * ↑n) ↔ n ≠ 0 ∧ Irrational x

Tactic:
rw [← cast_natCast, irrational_mul_ratCast_iff, Nat.cast_ne_zero]

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 * θ)
⊢ (∫ (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:
let v₁' (x : ℝ) : ℝ := cos (x * θ) * θ

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 * θ) * θ
⊢ (∫ (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: case zero
⊢ 0 < W 0

Tactic:
unfold W

Goal state after:
case zero
⊢ 0 < ∏ i ∈ range 0, (2 * ↑i + 2) / (2 * ↑i + 1) * ((2 * ↑i + 2) / (2 * ↑i + 3))
Module: Mathlib.Analysis.SpecialFunctions.Arcosh

Goal state before:
pp: x : ℝ
hx : 0 ≤ x
⊢ cosh x + √(cosh x ^ 2 - 1) = rexp x

Tactic:
← eq_sub_iff_add_eq',

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

Goal state before:
pp: x : ℝ
hx : x ∈ Ioi 1
⊢ HasStrictDerivAt arcosh (√(x ^ 2 - 1))⁻¹ x

Tactic:
rw [← sinh_arcosh (le_of_lt hx)]

Goal state after:
x : ℝ
hx : x ∈ Ioi 1
⊢ HasStrictDerivAt arcosh (sinh (arcosh x))⁻¹ x
Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean

Goal state before:
pp: case zero
y : ℝ≥0
⊢ (agmSequences 0 y 0).1 = 0

Tactic:
simp [agmSequences]

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

Goal state before:
pp: x : ℝ
hx : x ∈ Ioo (-1) 1
⊢ cosh (artanh x) = 1 / √(1 - x ^ 2)

Tactic:
have : 0 < √((1 + x) / (1 - x)) := sqrt_pos_of_pos <| div_pos (by grind) (by grind)
  rw [← one_pow, sq_sub_sq 1 x, sqrt_mul]
    <;> grind [artanh, cosh_eq, exp_neg, exp_log, sqrt_div]

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

Goal state before:
pp: x : ℝ
⊢ x ∈ Ioo (-1) 1 → ∀ ⦃b : ℝ⦄, b ∈ Ioo (-1) 1 → x < b → (fun x ↦ (1 + x) / (1 - x)) x < (fun x ↦ (1 + x) / (1 - x)) b

Tactic:
hx

Goal state after:
x : ℝ
hx : x ∈ Ioo (-1) 1
⊢ ∀ ⦃b : ℝ⦄, b ∈ Ioo (-1) 1 → x < b → (fun x ↦ (1 + x) / (1 - x)) x < (fun x ↦ (1 + x) / (1 - x)) b
Module: Mathlib.Analysis.SpecialFunctions.CompareExp

Goal state before:
pp: l : Filter ℂ
b₁ b₂ : ℝ
hl : IsExpCmpFilter l
hb : b₁ < b₂
m n : ℤ
⊢ (fun z ↦ z ^ m * cexp (↑b₁ * z)) =o[l] fun z ↦ z ^ n * cexp (↑b₂ * z)

Tactic:
by
  simpa only [cpow_intCast] using hl.isLittleO_cpow_mul_exp hb m n

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

Goal state before:
pp: h₁ : 0 < 1 / 2
p : ℝ
⊢ p ∈ Ioc 0 (1 / 2) → log (1 / 2) ≤ log (1 - p)

Tactic:
hx

Goal state after:
h₁ : 0 < 1 / 2
p : ℝ
hx : p ∈ Ioc 0 (1 / 2)
⊢ log (1 / 2) ≤ log (1 - p)
Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy

Goal state before:
pp: this : Tendsto log (𝓝[>] 0) atBot
contF : Continuous fun x ↦ 1 - x
p : ℝ
⊢ p ∈ Iio 1 → (fun x ↦ 1 - x) p ∈ Ioi 0

Tactic:
hx

Goal state after:
this : Tendsto log (𝓝[>] 0) atBot
contF : Continuous fun x ↦ 1 - x
p : ℝ
hx : p ∈ Iio 1
⊢ (fun x ↦ 1 - x) p ∈ Ioi 0
Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy

Goal state before:
pp: h₁ : 1 - 2⁻¹ < 1
p : ℝ
⊢ p ∈ Ico (1 - 2⁻¹) 1 → -log p ≤ -log (1 - 2⁻¹)

Tactic:
hx

Goal state after:
h₁ : 1 - 2⁻¹ < 1
p : ℝ
hx : p ∈ Ico (1 - 2⁻¹) 1
⊢ -log p ≤ -log (1 - 2⁻¹)
Module: Mathlib.Analysis.Real.Pi.Irrational

Goal state before:
pp: n : ℕ
x : ℝ
⊢ x ∈ uIoc (-1) 1 → ‖(1 - x ^ 2) ^ n * cos (x * (π / 2))‖ ≤ 1

Tactic:
hx

Goal state after:
n : ℕ
x : ℝ
hx : x ∈ uIoc (-1) 1
⊢ ‖(1 - x ^ 2) ^ n * cos (x * (π / 2))‖ ≤ 1
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 : ℝ
⊢ x ∈ s → dist (log x) (p⁻¹ * (x ^ p - 1)) ≤ ε

Tactic:
hx

Goal state after:
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
⊢ dist (log x) (p⁻¹ * (x ^ p - 1)) ≤ ε
Module: Mathlib.Analysis.SpecialFunctions.FrullaniIntegral

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
L : E
inst✝ : CompleteSpace E
hf : LocallyIntegrableOn f (Ioi 0) volume
ha : 0 < a
hb : 0 < b
hL : Tendsto f (𝓝[>] 0) (𝓝 L)
δ : ℝ
hδ : δ > 0
η : ℝ
hη : η > 0
hη_sub : ball 0 η ∩ Ioi 0 ⊆ {x | dist (f x) L < δ}
M : ℝ := max a b
hM_def : M = max a b
hM : 0 < M
t : ℝ
ht_pos : 0 < t
ht_bound : t ∈ Iio (η / M)
x : ℝ
⊢ x ∈ uIoc (a * t) (b * t) → ‖f x - L‖ ≤ δ

Tactic:
hx

Goal state after:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
L : E
inst✝ : CompleteSpace E
hf : LocallyIntegrableOn f (Ioi 0) volume
ha : 0 < a
hb : 0 < b
hL : Tendsto f (𝓝[>] 0) (𝓝 L)
δ : ℝ
hδ : δ > 0
η : ℝ
hη : η > 0
hη_sub : ball 0 η ∩ Ioi 0 ⊆ {x | dist (f x) L < δ}
M : ℝ := max a b
hM_def : M = max a b
hM : 0 < M
t : ℝ
ht_pos : 0 < t
ht_bound : t ∈ Iio (η / M)
x : ℝ
hx : x ∈ uIoc (a * t) (b * t)
⊢ ‖f x - L‖ ≤ δ
Module: Mathlib.Analysis.SpecialFunctions.FrullaniIntegral

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
R : E
inst✝ : CompleteSpace E
hf : LocallyIntegrableOn f (Ioi 0) volume
ha : 0 < a
hb : 0 < b
hR : Tendsto f atTop (𝓝 R)
δ : ℝ
hδ : δ > 0
N : ℝ
hN : ∀ (b : ℝ), N ≤ b → dist (f b) R < δ
hm : 0 < min a b
t : ℝ
ht : max 1 (N / min a b) ≤ t
x : ℝ
⊢ x ∈ uIoc (a * t) (b * t) → ‖f x - R‖ ≤ δ

Tactic:
hx

Goal state after:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
R : E
inst✝ : CompleteSpace E
hf : LocallyIntegrableOn f (Ioi 0) volume
ha : 0 < a
hb : 0 < b
hR : Tendsto f atTop (𝓝 R)
δ : ℝ
hδ : δ > 0
N : ℝ
hN : ∀ (b : ℝ), N ≤ b → dist (f b) R < δ
hm : 0 < min a b
t : ℝ
ht : max 1 (N / min a b) ≤ t
x : ℝ
hx : x ∈ uIoc (a * t) (b * t)
⊢ ‖f x - R‖ ≤ δ
Module: Mathlib.Analysis.SpecialFunctions.FrullaniIntegral

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
L R : E
inst✝ : CompleteSpace E
hf : LocallyIntegrableOn f (Ioi 0) volume
ha : 0 < a
hb : 0 < b
hL : Tendsto f (𝓝[>] 0) (𝓝 L)
hR : Tendsto f atTop (𝓝 R)
g : ℝ → E := fun x ↦ x⁻¹ • (f (a * x) - f (b * x))
hint : IntegrableOn g (Ioi 0) volume
h_lim : Tendsto (fun p ↦ intervalIntegral g p.1 p.2 volume) ((𝓝[>] 0).curry atTop) (𝓝 (log (b / a) • (L - R)))
hg : g = fun x ↦ x⁻¹ • (f (a * x) - f (b * x))
⊢ integral (volume.restrict (Ioi 0)) g = log (b / a) • (L - R)

Tactic:
apply tendsto_nhds_unique
    (hint.continuousWithinAt_Ici_primitive_Ioi.mono_left (nhdsWithin_mono 0 Ioi_subset_Ici_self))

Goal state after:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
L R : E
inst✝ : CompleteSpace E
hf : LocallyIntegrableOn f (Ioi 0) volume
ha : 0 < a
hb : 0 < b
hL : Tendsto f (𝓝[>] 0) (𝓝 L)
hR : Tendsto f atTop (𝓝 R)
g : ℝ → E := ⋯
hint : IntegrableOn g (Ioi 0) volume
h_lim : Tendsto (fun p ↦ intervalIntegral g p.1 p.2 volume) ((𝓝[>] 0).curry atTop) (𝓝 (log (b / a) • (L - R)))
hg : g = fun x ↦ x⁻¹ • (f (a * x) - f (b * x))
⊢ Tendsto (fun b ↦ ∫ (x : ℝ) in Ioi b, g x ∂volume) (𝓝[>] 0) (𝓝 (log (b / a) • (L - R)))
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation

Goal state before:
pp: p t : ℝ
hp : p ∈ Ioo 0 1
ht : 0 ≤ t
x : ℝ
⊢ x ∈ Ici 0 → ∀ ⦃b : ℝ⦄, b ∈ Ici 0 → x ≤ b → p.rpowIntegrand₀₁ t x ≤ p.rpowIntegrand₀₁ t b

Tactic:
hx

Goal state after:
p t : ℝ
hp : p ∈ Ioo 0 1
ht : 0 ≤ t
x : ℝ
hx : x ∈ Ici 0
⊢ ∀ ⦃b : ℝ⦄, b ∈ Ici 0 → x ≤ b → p.rpowIntegrand₀₁ t x ≤ p.rpowIntegrand₀₁ t b
Module: Mathlib.Analysis.SpecialFunctions.FrullaniIntegral

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
L R : E
inst✝ : CompleteSpace E
hf : LocallyIntegrableOn f (Ioi 0) volume
ha : 0 < a
hb : 0 < b
hL : Tendsto f (𝓝[>] 0) (𝓝 L)
hR : Tendsto f atTop (𝓝 R)
g : ℝ → E := fun x ↦ x⁻¹ • (f (a * x) - f (b * x))
hint : IntegrableOn g (Ioi 0) volume
hg : g = fun x ↦ x⁻¹ • (f (a * x) - f (b * x))
ε : ℝ
hε : ε > 0
δ : ℝ
hδ_pos : δ > 0
hδ :
  ∀ (x : ℝ),
    dist x 0 < δ ∧ x ∈ Ioi 0 →
      x ∈ {x | ∀ᶠ (y : ℝ) in atTop, dist (intervalIntegral g x y volume) (log (b / a) • (L - R)) < ε / 2}
x : ℝ
⊢ x ∈ Ioi 0 → dist x 0 < δ → dist (∫ (x : ℝ) in Ioi x, g x ∂volume) (log (b / a) • (L - R)) < ε

Tactic:
hx

Goal state after:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
L R : E
inst✝ : CompleteSpace E
hf : LocallyIntegrableOn f (Ioi 0) volume
ha : 0 < a
hb : 0 < b
hL : Tendsto f (𝓝[>] 0) (𝓝 L)
hR : Tendsto f atTop (𝓝 R)
g : ℝ → E := fun x ↦ x⁻¹ • (f (a * x) - f (b * x))
hint : IntegrableOn g (Ioi 0) volume
hg : g = fun x ↦ x⁻¹ • (f (a * x) - f (b * x))
ε : ℝ
hε : ε > 0
δ : ℝ
hδ_pos : δ > 0
hδ :
  ∀ (x : ℝ),
    dist x 0 < δ ∧ x ∈ Ioi 0 →
      x ∈ {x | ∀ᶠ (y : ℝ) in atTop, dist (intervalIntegral g x y volume) (log (b / a) • (L - R)) < ε / 2}
x : ℝ
hx : x ∈ Ioi 0
⊢ dist x 0 < δ → dist (∫ (x : ℝ) in Ioi x, g x ∂volume) (log (b / a) • (L - R)) < ε
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation

Goal state before:
pp: p t : ℝ
ht : 0 < t
x : ℝ
⊢ x ∈ Ici 0 → p.rpowIntegrand₀₁ t x = (fun x ↦ t ^ (p - 1) * p.rpowIntegrand₀₁ 1 (t⁻¹ • x)) x

Tactic:
hx

Goal state after:
p t : ℝ
ht : 0 < t
x : ℝ
hx : x ∈ Ici 0
⊢ p.rpowIntegrand₀₁ t x = (fun x ↦ t ^ (p - 1) * p.rpowIntegrand₀₁ 1 (t⁻¹ • x)) x
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation

Goal state before:
pp: A : Type u_1
inst✝⁸ : NonUnitalNormedRing A
inst✝⁷ : StarRing A
inst✝⁶ : NormedSpace ℝ A
inst✝⁵ : SMulCommClass ℝ A A
inst✝⁴ : IsScalarTower ℝ A A
inst✝³ : PartialOrder A
inst✝² : StarOrderedRing A
inst✝¹ : NonnegSpectrumClass ℝ A
inst✝ : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
p t : ℝ
hp : p ∈ Ioo 0 1
ht : 0 < t
a : A
ha : 0 ≤ a
hspec : quasispectrum ℝ a ⊆ Ici 0
x : ℝ
⊢ x ∈ Ici 0 → (fun x ↦ t⁻¹ • x) x ∈ Ici 0

Tactic:
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 : x ∈ Ici 0
⊢ (fun x ↦ t⁻¹ • x) x ∈ Ici 0
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
⊢ -log ↑π / 2 / ↑π ^ (1 / 2) = -log ↑π / 2 / ↑√π

Tactic:
aux

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
⊢ -log ↑π / 2 / ↑√π = -log ↑π / 2 / ↑√π
Module: Mathlib.NumberTheory.Harmonic.GammaDeriv

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

pp: case refine_1
f : ℂ → ℂ := fun s ↦ ↑π ^ (-s / 2)
g : ℂ → ℂ := fun s ↦ Gamma (s / 2)
aux : ↑π ^ (1 / 2) = ↑√π
aux2 : ↑√π ≠ 0
hf : HasDerivAt f (-log ↑π / 2 / ↑√π) 1
⊢ HasDerivAt (fun s ↦ s / 2) (1 / 2) 1

Tactic:
· rwa [mul_one_div] at this

Goal state after:
case refine_1
f : ℂ → ℂ := fun s ↦ ↑π ^ (-s / 2)
g : ℂ → ℂ := fun s ↦ Gamma (s / 2)
aux : ↑π ^ (1 / 2) = ↑√π
aux2 : ↑√π ≠ 0
hf : HasDerivAt f (-log ↑π / 2 / ↑√π) 1
⊢ HasDerivAt (fun s ↦ s / 2) (1 / 2) 1
Module: Mathlib.Analysis.SpecialFunctions.Log.Base

Goal state before:
pp: x : ℝ
⊢ logb 1 x = 0

Tactic:
by simp only [← log_div_log, log_one, div_zero]

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

Goal state before:
pp: A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
p t : ℝ
hp : p ∈ Ioo 0 1
ht : 0 < t
x : A
⊢ x ∈ Ici 0 →
    cfc (p.rpowIntegrand₀₁ t) x =
      (fun x ↦ (algebraMap ℝ A) (t ^ (p - 1)) - t ^ p • Ring.inverse ((algebraMap ℝ A) t + x)) x

Tactic:
hx

Goal state after:
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
p t : ℝ
hp : p ∈ Ioo 0 1
ht : 0 < t
x : A
hx : x ∈ Ici 0
⊢ cfc (p.rpowIntegrand₀₁ t) x =
    (fun x ↦ (algebraMap ℝ A) (t ^ (p - 1)) - t ^ p • Ring.inverse ((algebraMap ℝ A) t + x)) x
Module: Mathlib.Analysis.SpecialFunctions.Log.Base

Goal state before:
pp: b x : ℝ
b_pos : 0 < b
b_ne_one : b ≠ 1
hx : 0 < x
⊢ b ^ logb b x = x

Tactic:
rw [rpow_logb_eq_abs b_pos b_ne_one hx.ne']
  exact abs_of_pos hx

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

Goal state before:
pp: P : ℝ → Prop
x₀ r : ℝ
hr : 1 < r
hx₀ : 0 < x₀
base : ∀ x ∈ Ico x₀ (r * x₀), P x
step : ∀ n ≥ 1, (∀ z ∈ Ico x₀ (r ^ n * x₀), P z) → ∀ z ∈ Ico (r ^ n * x₀) (r ^ (n + 1) * x₀), P z
this : ∀ (n : ℕ), ∀ x ∈ Ico x₀ (r ^ (n + 1) * x₀), P x
x : ℝ
⊢ x ≥ x₀ → P x

Tactic:
hx

Goal state after:
P : ℝ → Prop
x₀ r : ℝ
hr : 1 < r
hx₀ : 0 < x₀
base : ∀ x ∈ Ico x₀ (r * x₀), P x
step : ∀ n ≥ 1, (∀ z ∈ Ico x₀ (r ^ n * x₀), P z) → ∀ z ∈ Ico (r ^ n * x₀) (r ^ (n + 1) * x₀), P z
this : ∀ (n : ℕ), ∀ x ∈ Ico x₀ (r ^ (n + 1) * x₀), P x
x : ℝ
hx : x ≥ x₀
⊢ P x
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
s : Set ↑(sphere 0 1)
hs : MeasurableSet s
⊢ μ.toSphere s = ↑(dim E) * μ (Ioo 0 1 • Subtype.val '' s)

Tactic:
toSphere,

Goal state after:
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : MeasurableSpace E
μ : Measure E
inst✝ : BorelSpace E
s : Set ↑(sphere 0 1)
hs : MeasurableSet s
⊢ (dim E •
        ((comap (Subtype.val ∘ ⇑(homeomorphUnitSphereProd E).symm) μ).restrict
            (univ ×ˢ Iio ⟨1, toSphere._proof_1⟩)).fst)
      s =
    ↑(dim E) * μ (Ioo 0 1 • Subtype.val '' s)
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

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

Tactic:
exact pow_pos (by simpa [sub_eq_zero]) _

Goal state after:
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
x : ℂ
⊢ x ∈ (↑L.lattice \ {l₀ - ↑l})ᶜ →
    deriv (fun x ↦ ℘[L - l₀] (x + ↑l)) x = deriv (fun x ↦ ℘[L - l₀ - ↑l] x + (1 / l₀ ^ 2 - 1 / (l₀ - ↑l) ^ 2)) x

Tactic:
hx

Goal state after:
L : PeriodPair
l₀ : ℂ
hl₀ : l₀ ∈ L.lattice
l : ↥L.lattice
hl : ↑l / 2 ∉ L.lattice
x : ℂ
hx : x ∈ (↑L.lattice \ {l₀ - ↑l})ᶜ
⊢ deriv (fun x ↦ ℘[L - l₀] (x + ↑l)) x = deriv (fun x ↦ ℘[L - l₀ - ↑l] x + (1 / l₀ ^ 2 - 1 / (l₀ - ↑l) ^ 2)) x
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 x : ℝ
⊢ x ∈ support ((Ioo 0 r).indicator fun y ↦ y ^ (dim E - 1) • f y) → x ∈ Ioi 0

Tactic:
hx

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 x : ℝ
hx : x ∈ support ((Ioo 0 r).indicator fun y ↦ y ^ (dim E - 1) • f y)
⊢ x ∈ Ioi 0
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.InverseDeriv

Goal state before:
pp: x : ℝ
h₁✝ : x ≠ -1
h₂✝ : x ≠ 1
h₁ : -1 < x
h₂ : 1 < x
⊢ 1 - x ^ 2 < 0

Tactic:
nlinarith [h₂]

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

Goal state before:
pp: case inr.hderiv
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
h'ab : a < b
x : ℝ
⊢ x ∈ Ioo a b → HasDerivAt f (deriv f x) x

Tactic:
hx

Goal state after:
case inr.hderiv
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
h'ab : a < b
x : ℝ
hx : x ∈ Ioo a b
⊢ HasDerivAt f (deriv f x) x
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
h'ab : a < b
this : ContinuousOn (derivWithin f (Icc a b)) (Icc a b)
x : ℝ
⊢ x ∈ Ioo a b → derivWithin f (Icc a b) x = deriv f x

Tactic:
hx

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
h'ab : a < b
this : ContinuousOn (derivWithin f (Icc a b)) (Icc a b)
x : ℝ
hx : x ∈ Ioo a b
⊢ derivWithin f (Icc a b) x = deriv f x
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 : ℝ
⊢ x ∈ Ioo a b → derivWithin f (Icc a b) x = deriv f x

Tactic:
hx

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 : ℝ
hx : x ∈ Ioo a b
⊢ derivWithin f (Icc a b) x = deriv f x
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 := UniformSpace.Completion.toComplₗᵢ
this : ‖(⇑g ∘ f) b - (⇑g ∘ f) a‖ₑ = ‖f b - f a‖ₑ
x : ℝ
⊢ x ∈ Ioo a b → ‖deriv (⇑g ∘ f) x‖ₑ ≤ ‖deriv f x‖ₑ

Tactic:
hx

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‖ₑ
x : ℝ
hx : x ∈ Ioo a b
⊢ ‖deriv (⇑g ∘ f) x‖ₑ ≤ ‖deriv f x‖ₑ
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
x : ℝ
⊢ x ∈ Ioo a b → ‖deriv f x‖ₑ = ‖derivWithin f (Icc a b) x‖ₑ

Tactic:
hx

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
x : ℝ
hx : x ∈ Ioo a b
⊢ ‖deriv f x‖ₑ = ‖derivWithin f (Icc a b) x‖ₑ
Module: Mathlib.Analysis.SpecialFunctions.Stirling

Goal state before:
pp: ⊢ Tendsto (fun n ↦ ↑n / (2 * ↑n + 1)) atTop (𝓝 (1 / 2))

Tactic:
conv =>
    congr
    · skip
    · skip
    rw [one_div, ← add_zero (2 : ℝ)]
  refine (((tendsto_const_div_atTop_nhds_zero_nat 1).const_add (2 : ℝ)).inv₀
    ((add_zero (2 : ℝ)).symm ▸ two_ne_zero)).congr' (eventually_atTop.mpr ⟨1, fun n hn => ?_⟩)
  rw [add_div' (1 : ℝ) 2 n (cast_ne_zero.mpr (one_le_iff_ne_zero.mp hn)), inv_div]

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

Goal state before:
pp: case a
z : ℍ
A B : ℝ
h : 0 < B
hz : z ∈ verticalStrip A B
⊢ ({ coe := { re := A, im := B }, coe_im_pos := h }.re ^ 2 / { coe := { re := A, im := B }, coe_im_pos := h }.im ^ 2 +
        1)⁻¹ ≤
    (z.re ^ 2 / z.im ^ 2 + 1)⁻¹

Tactic:
rw [inv_le_inv₀ (by positivity) (by positivity), add_le_add_iff_right, ← even_two.pow_abs]

Goal state after:
case a
z : ℍ
A B : ℝ
h : 0 < B
hz : z ∈ verticalStrip A B
⊢ |z.re| ^ 2 / z.im ^ 2 ≤
    { coe := { re := A, im := B }, coe_im_pos := h }.re ^ 2 / { coe := { re := A, im := B }, coe_im_pos := h }.im ^ 2
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema

Goal state before:
pp: case hf
n x : ℕ
⊢ x ∈ ↑(Finset.range n) →
    ∀ ⦃x₂ : ℕ⦄,
      x₂ ∈ ↑(Finset.range n) → (fun k ↦ (↑k + 1) * π / (↑n + 1)) x = (fun k ↦ (↑k + 1) * π / (↑n + 1)) x₂ → x = x₂

Tactic:
hx

Goal state after:
case hf
n x : ℕ
hx : x ∈ ↑(Finset.range n)
⊢ ∀ ⦃x₂ : ℕ⦄,
    x₂ ∈ ↑(Finset.range n) → (fun k ↦ (↑k + 1) * π / (↑n + 1)) x = (fun k ↦ (↑k + 1) * π / (↑n + 1)) x₂ → x = x₂
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal

Goal state before:
pp: n : ℕ
P : ℝ[X]
k : ℕ
hk₁ : 0 < k
hk₂ : k ≤ n
x : ℝ
hx : 1 ≤ x
hPdeg : P.degree ≤ ↑n
hPbnd : ∀ x ∈ Set.Icc (-1) 1, |eval x P| ≤ 1
⊢ eval x ((⇑derivative)^[k] P) = eval x ((⇑derivative)^[k] (T ℝ ↑n)) ↔ P = T ℝ ↑n

Tactic:
by
  convert!
    sumNodes_eq_sumNodes_T_iff (fun i hi => negOnePow_mul_iterateDerivativeC_pos hk₁ hk₂ hi hx)
      hPdeg hPbnd using 2
  · rw [sumNodes_eq_eval_iterate_derivative hk₂ x hPdeg]
  · rw [sumNodes_eq_eval_iterate_derivative hk₂ x (le_of_eq (degree_T ℝ n))]

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

Goal state before:
pp: case refine_1
n k : ℕ
hn : n ≠ 0
hk₀ : 0 < k
hk₁ : k < n
hk₂ : Even k
zero_lt : 0 < ↑k * π / ↑n
lt_pi : ↑k * π / ↑n < π
x : ℝ
⊢ x ∈ Set.Ioo (-1) 1 → (fun x ↦ eval x (T ℝ ↑n)) x ≤ (fun x ↦ eval x (T ℝ ↑n)) (cos (↑k * π / ↑n))

Tactic:
hx

Goal state after:
case refine_1
n k : ℕ
hn : n ≠ 0
hk₀ : 0 < k
hk₁ : k < n
hk₂ : Even k
zero_lt : 0 < ↑k * π / ↑n
lt_pi : ↑k * π / ↑n < π
x : ℝ
hx : x ∈ Set.Ioo (-1) 1
⊢ (fun x ↦ eval x (T ℝ ↑n)) x ≤ (fun x ↦ eval x (T ℝ ↑n)) (cos (↑k * π / ↑n))
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema

Goal state before:
pp: case refine_1
n k : ℕ
hn : n ≠ 0
hk₁ : k < n
hk₂ : Odd k
k_pos : 0 < k
zero_lt : 0 < ↑k * π / ↑n
lt_pi : ↑k * π / ↑n < π
x : ℝ
⊢ x ∈ Set.Ioo (-1) 1 → (fun x ↦ eval x (T ℝ ↑n)) (cos (↑k * π / ↑n)) ≤ (fun x ↦ eval x (T ℝ ↑n)) x

Tactic:
hx

Goal state after:
case refine_1
n k : ℕ
hn : n ≠ 0
hk₁ : k < n
hk₂ : Odd k
k_pos : 0 < k
zero_lt : 0 < ↑k * π / ↑n
lt_pi : ↑k * π / ↑n < π
x : ℝ
hx : x ∈ Set.Ioo (-1) 1
⊢ (fun x ↦ eval x (T ℝ ↑n)) (cos (↑k * π / ↑n)) ≤ (fun x ↦ eval x (T ℝ ↑n)) x