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

Goal state before:
pp: case convert_2.convert_2.hf
θ : ℝ
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₂
⊢ IntervalIntegrable (fun x ↦ (2 * ↑n + 1) * (f x ^ n * v₂ x)) volume (-1) 1

pp: case convert_2.convert_2.hg
θ : ℝ
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₂
⊢ IntervalIntegrable (fun x ↦ 2 * ↑n * (f x ^ (n - 1) * v₂ x)) volume (-1) 1

Tactic:
all_goals exact Continuous.intervalIntegrable (by fun_prop) _ _

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

Goal state before:
pp: θ : ℝ
n : ℕ
⊢ -(2 * 2 * ((↑(n + 1) + 1) * (0 ^ (n + 1) * cos θ))) + 2 * (↑(n + 1) + 1) * (2 * ↑(n + 1) + 1) * I (n + 1) θ -
      4 * (↑(n + 1) + 1) * ↑(n + 1) * I (n + 1 - 1) θ =
    2 * (↑n + 2) * (2 * ↑n + 3) * I (n + 1) θ - 4 * (↑n + 2) * (↑n + 1) * I n θ

Tactic:
push_cast

Goal state after:
θ : ℝ
n : ℕ
⊢ -(2 * 2 * ((↑n + 1 + 1) * (0 ^ (n + 1) * cos θ))) + 2 * (↑n + 1 + 1) * (2 * (↑n + 1) + 1) * I (n + 1) θ -
      4 * (↑n + 1 + 1) * (↑n + 1) * I n θ =
    2 * (↑n + 2) * (2 * ↑n + 3) * I (n + 1) θ - 4 * (↑n + 2) * (↑n + 1) * I n θ
Module: Mathlib.Analysis.Real.Pi.Irrational

Goal state before:
pp: θ : ℝ
⊢ I 0 θ * θ ^ (2 * 0 + 1) =
    ↑0! * (eval₂ (Int.castRingHom ℝ) θ (sinPoly 0) * sin θ + eval₂ (Int.castRingHom ℝ) θ (cosPoly 0) * cos θ)

Tactic:
simp [sinPoly, cosPoly, I_zero]

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

Goal state before:
pp: a : ℝ
⊢ Tendsto (fun n ↦ a ^ (2 * n + 1) / ↑n !) atTop (nhds (a * 0))

Tactic:
refine ((FloorSemiring.tendsto_pow_div_factorial_atTop (a ^ 2)).const_mul a).congr (fun x => ?_)

Goal state after:
a : ℝ
x : ℕ
⊢ a * ((a ^ 2) ^ x / ↑x !) = a ^ (2 * x + 1) / ↑x !
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 : ℝ
⊢ 0 < p ∧ p < pbound → p ≤ 1 / (sSup ((fun x ↦ ‖log x‖) '' s) + 1) → ∀ x ∈ s, dist (log x) (p⁻¹ * (x ^ p - 1)) ≤ ε

Tactic:
⟨hp₁,hp₂⟩

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
⊢ p ≤ 1 / (sSup ((fun x ↦ ‖log x‖) '' s) + 1) → ∀ x ∈ s, dist (log x) (p⁻¹ * (x ^ p - 1)) ≤ ε
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog.Order

Goal state before:
pp: A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
s : Set A := {a | IsStrictlyPositive a}
f : ℝ → A → A := fun p a ↦ if a ∈ s then cfc (fun x ↦ p⁻¹ * (x ^ p - 1)) a else 0
⊢ MonotoneOn log {a | IsStrictlyPositive a}

Tactic:
let g := fun a => if a ∈ s then log (A := A) a else 0

Goal state after:
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
s : Set A := {a | IsStrictlyPositive a}
f : ℝ → A → A := fun p a ↦ if a ∈ s then cfc (fun x ↦ p⁻¹ * (x ^ p - 1)) a else 0
g : A → A := fun a ↦ if a ∈ s then log a else 0
⊢ MonotoneOn log {a | IsStrictlyPositive a}
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog.Order

Goal state before:
pp: A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
s : Set A := {a | IsStrictlyPositive a}
f : ℝ → A → A := fun p a ↦ if a ∈ s then cfc (fun x ↦ p⁻¹ * (x ^ p - 1)) a else 0
⊢ ConcaveOn ℝ s log

Tactic:
let g := fun a => if a ∈ s then log (A := A) a else 0

Goal state after:
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
s : Set A := {a | IsStrictlyPositive a}
f : ℝ → A → A := fun p a ↦ if a ∈ s then cfc (fun x ↦ p⁻¹ * (x ^ p - 1)) a else 0
g : A → A := fun a ↦ if a ∈ s then log a else 0
⊢ ConcaveOn ℝ s log
Module: Mathlib.Analysis.SpecialFunctions.FrullaniIntegral

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
inst✝ : CompleteSpace E
hf : LocallyIntegrableOn f (Ioi 0) volume
ha : 0 < a
hb : 0 < b
V : E
δ : ℝ
hδ : 0 ≤ δ
h : ∀ x ∈ uIoc a b, ‖f x - V‖ ≤ δ
hsub : uIcc a b ⊆ Ioi 0
hint_f : IntervalIntegrable (fun x ↦ x⁻¹ • f x) volume a b
⊢ IntervalIntegrable (fun x ↦ x⁻¹ • V) volume a b

Tactic:
apply ContinuousOn.intervalIntegrable

Goal state after:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
inst✝ : CompleteSpace E
hf : LocallyIntegrableOn f (Ioi 0) volume
ha : 0 < a
hb : 0 < b
V : E
δ : ℝ
hδ : 0 ≤ δ
h : ∀ x ∈ uIoc a b, ‖f x - V‖ ≤ δ
hsub : uIcc a b ⊆ Ioi 0
hint_f : IntervalIntegrable (fun x ↦ x⁻¹ • f x) volume a b
⊢ ContinuousOn (fun x ↦ x⁻¹ • V) (uIcc a b)
Module: Mathlib.Analysis.SpecialFunctions.FrullaniIntegral

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
inst✝ : CompleteSpace E
hf : LocallyIntegrableOn f (Ioi 0) volume
ha : 0 < a
hb : 0 < b
V : E
δ : ℝ
hδ : 0 ≤ δ
h : ∀ x ∈ uIoc a b, ‖f x - V‖ ≤ δ
hsub : uIcc a b ⊆ Ioi 0
hint_f : IntervalIntegrable (fun x ↦ x⁻¹ • f x) volume a b
hint_V : IntervalIntegrable (fun x ↦ x⁻¹ • V) volume a b
⊢ IntervalIntegrable (fun x ↦ x⁻¹ * δ) volume a b

Tactic:
apply ContinuousOn.intervalIntegrable

Goal state after:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
inst✝ : CompleteSpace E
hf : LocallyIntegrableOn f (Ioi 0) volume
ha : 0 < a
hb : 0 < b
V : E
δ : ℝ
hδ : 0 ≤ δ
h : ∀ x ∈ uIoc a b, ‖f x - V‖ ≤ δ
hsub : uIcc a b ⊆ Ioi 0
hint_f : IntervalIntegrable (fun x ↦ x⁻¹ • f x) volume a b
hint_V : IntervalIntegrable (fun x ↦ x⁻¹ • V) volume a b
⊢ ContinuousOn (fun x ↦ x⁻¹ * δ) (uIcc a b)
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation

Goal state before:
pp: p t x : ℝ
hp : p ∈ Ioo 0 1
ht : 0 ≤ t
hx : 0 ≤ x
hx_zero : ¬x = 0
⊢ t ^ (p - 1) * (x / x) = t ^ (p - 1) * 1

Tactic:
by congr; exact (div_eq_one_iff_eq hx_zero).mpr rfl

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

Goal state before:
pp: p x : ℝ
hp : p ∈ Ioo 0 1
hx : 0 ≤ x
⊢ ∀ᵐ (a : ℝ) ∂volume.restrict (Ioi 1), ‖p.rpowIntegrand₀₁ a x‖ ≤ a ^ (p - 2) * x

Tactic:
refine ae_restrict_of_forall_mem measurableSet_Ioi fun t (ht : 1 < t) => ?_
      rw [Real.norm_of_nonneg (rpowIntegrand₀₁_nonneg hp.1 (by positivity) hx)]
      exact rpowIntegrand₀₁_le_rpow_sub_two_mul_self hp (by positivity) hx

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

Goal state before:
pp: s : ℂ
hs : ∀ (n : ℕ), s ≠ -(2 * ↑n + 1)
⊢ s.Gammaℝ / (1 - s).Gammaℝ = s.Gammaℂ * cos (↑π * s / 2)

Tactic:
have : Gammaℝ (s + 1) ≠ 0 := by
    simpa only [Ne, Gammaℝ_eq_zero_iff, not_exists, ← eq_sub_iff_add_eq,
      sub_eq_add_neg, ← neg_add]

Goal state after:
s : ℂ
hs : ∀ (n : ℕ), s ≠ -(2 * ↑n + 1)
this : (s + 1).Gammaℝ ≠ 0
⊢ s.Gammaℝ / (1 - s).Gammaℝ = s.Gammaℂ * cos (↑π * s / 2)
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Deligne

Goal state before:
pp: s : ℂ
hs : ∀ (n : ℕ), s ≠ -↑n
h : s - 1 ≠ 0
m : ℕ
⊢ -↑(m + 1) + 1 = -↑m

Tactic:
push_cast

Goal state after:
s : ℂ
hs : ∀ (n : ℕ), s ≠ -↑n
h : s - 1 ≠ 0
m : ℕ
⊢ -(↑m + 1) + 1 = -↑m
Module: Mathlib.NumberTheory.Harmonic.GammaDeriv

Goal state before:
pp: case succ
n✝ : ℕ
f : ℝ → ℝ := log ∘ Gamma
hc : ConvexOn ℝ (Ioi 0) f
h_rec : ∀ (x : ℝ), 0 < x → f (x + 1) = f x + log x
hder : ∀ {x : ℝ}, 0 < x → DifferentiableAt ℝ f x
hder_rec : ∀ (x : ℝ), 0 < x → deriv f (x + 1) = deriv f x + 1 / x
n : ℕ
hn : deriv f (↑n + 1) = deriv f 1 + ↑(harmonic n)
⊢ deriv f 1 + ↑(harmonic n) + 1 / (↑n + 1) = deriv f 1 + ↑(harmonic n + (↑(n + 1))⁻¹)

Tactic:
push_cast

Goal state after:
case succ
n✝ : ℕ
f : ℝ → ℝ := log ∘ Gamma
hc : ConvexOn ℝ (Ioi 0) f
h_rec : ∀ (x : ℝ), 0 < x → f (x + 1) = f x + log x
hder : ∀ {x : ℝ}, 0 < x → DifferentiableAt ℝ f x
hder_rec : ∀ (x : ℝ), 0 < x → deriv f (x + 1) = deriv f x + 1 / x
n : ℕ
hn : deriv f (↑n + 1) = deriv f 1 + ↑(harmonic n)
⊢ deriv f 1 + ↑(harmonic n) + 1 / (↑n + 1) = deriv f 1 + (↑(harmonic n) + (↑n + 1)⁻¹)
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation

Goal state before:
pp: p x : ℝ
hp : p ∈ Ioo 1 2
hx : 0 ≤ x
hmain : (fun x_1 ↦ p.rpowIntegrand₁₂ x_1 x) =ᵐ[volume.restrict (Ioi 0)] fun x_1 ↦ x * (p - 1).rpowIntegrand₀₁ x_1 x
⊢ IntegrableOn (fun x_1 ↦ p.rpowIntegrand₁₂ x_1 x) (Ioi 0) volume

Tactic:
rw [integrableOn_congr_fun_ae hmain]

Goal state after:
p x : ℝ
hp : p ∈ Ioo 1 2
hx : 0 ≤ x
hmain : (fun x_1 ↦ p.rpowIntegrand₁₂ x_1 x) =ᵐ[volume.restrict (Ioi 0)] fun x_1 ↦ x * (p - 1).rpowIntegrand₀₁ x_1 x
⊢ IntegrableOn (fun x_1 ↦ x * (p - 1).rpowIntegrand₀₁ x_1 x) (Ioi 0) volume
Module: Mathlib.NumberTheory.Harmonic.GammaDeriv

Goal state before:
pp: h_diff : ∀ {s : ℝ}, 0 < s → DifferentiableAt ℝ Gamma s
⊢ HasDerivAt Gamma (-√π * (γ + 2 * log 2)) (1 / 2)

Tactic:
have h_diff' {s : ℝ} (hs : 0 < s) : DifferentiableAt ℝ (fun s ↦ Gamma (2 * s)) s :=
    .comp (g := Gamma) _ (h_diff <| mul_pos two_pos hs) (differentiableAt_id.const_mul _)

Goal state after:
h_diff : ∀ {s : ℝ}, 0 < s → DifferentiableAt ℝ Gamma s
h_diff' : ∀ {s : ℝ}, 0 < s → DifferentiableAt ℝ (fun s ↦ Gamma (2 * s)) s
⊢ HasDerivAt Gamma (-√π * (γ + 2 * log 2)) (1 / 2)
Module: Mathlib.Analysis.SpecialFunctions.Gaussian.PoissonSummation

Goal state before:
pp: a : ℂ
ha : a.re < 0
b : ℂ
s : ℝ
⊢ (fun x ↦ cexp (a * ↑x ^ 2 + b * ↑x)) =o[cocompact ℝ] fun x ↦ |x| ^ s

Tactic:
cocompact_eq_atBot_atTop,

Goal state after:
a : ℂ
ha : a.re < 0
b : ℂ
s : ℝ
⊢ (fun x ↦ cexp (a * ↑x ^ 2 + b * ↑x)) =o[atBot ⊔ atTop] fun x ↦ |x| ^ s
Module: Mathlib.Analysis.SpecialFunctions.Gaussian.PoissonSummation

Goal state before:
pp: a : ℝ
ha : 0 < a
s : ℝ
⊢ Tendsto (fun x ↦ |x| ^ s * rexp (-a * |x| ^ 2)) (cocompact ℝ) (𝓝 0)

Tactic:
cocompact_eq_atBot_atTop,

Goal state after:
a : ℝ
ha : 0 < a
s : ℝ
⊢ Tendsto (fun x ↦ |x| ^ s * rexp (-a * |x| ^ 2)) (atBot ⊔ atTop) (𝓝 0)
Module: Mathlib.NumberTheory.Harmonic.GammaDeriv

Goal state before:
pp: f : ℂ → ℂ
g : ℝ → ℝ
g' s : ℝ
hf : DifferentiableAt ℂ f ↑s
hg : HasDerivAt g g' s
hfg : ∀ (s : ℝ), f ↑s = ↑(g s)
⊢ deriv (fun x ↦ ↑(g x)) s = ↑g'

Tactic:
exact hg.ofReal_comp.deriv

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

Goal state before:
pp: n : ℕ
⊢ DifferentiableAt ℂ Gamma (↑n + 1)

Tactic:
refine differentiableAt_Gamma _ (fun m ↦ ?_)

Goal state after:
n m : ℕ
⊢ ↑n + 1 ≠ -↑m
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 : ℕ
hr : 1 ≤ 1
⊢ log b 1 = -↑(Nat.clog b ⌈1⁻¹⌉₊)

pp: case inr
R : Type u_1
inst✝³ : Semifield R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorSemiring R
b : ℕ
r : R
hr✝ : r ≤ 1
hr : r < 1
⊢ log b r = -↑(Nat.clog b ⌈r⁻¹⌉₊)

Tactic:
· rw [log, if_pos hr, inv_one, Nat.ceil_one, Nat.floor_one, Nat.log_one_right, Nat.clog_one_right,
      Int.ofNat_zero, neg_zero]

Goal state after:
case inr
R : Type u_1
inst✝³ : Semifield R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorSemiring R
b : ℕ
r : R
hr✝ : r ≤ 1
hr : r < 1
⊢ log b r = -↑(Nat.clog b ⌈r⁻¹⌉₊)
Module: Mathlib.Data.Int.Log

Goal state before:
pp: case inr.inl
R : Type u_1
inst✝³ : Semifield R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorSemiring R
b : ℕ
r₁ r₂ : R
h₀ : 0 < r₁
h : r₁ ≤ r₂
h₁ : 1 ≤ r₁
h₂ : r₂ ≤ 1
⊢ log b r₁ ≤ log b r₂

pp: case inr.inr
R : Type u_1
inst✝³ : Semifield R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorSemiring R
b : ℕ
r₁ r₂ : R
h₀ : 0 < r₁
h : r₁ ≤ r₂
h₁ : 1 ≤ r₁
h₂ : 1 ≤ r₂
⊢ log b r₁ ≤ log b r₂

Tactic:
· obtain rfl := le_antisymm h (h₂.trans h₁)
    rfl

Goal state after:
case inr.inr
R : Type u_1
inst✝³ : Semifield R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorSemiring R
b : ℕ
r₁ r₂ : R
h₀ : 0 < r₁
h : r₁ ≤ r₂
h₁ : 1 ≤ r₁
h₂ : 1 ≤ r₂
⊢ log b r₁ ≤ log b r₂
Module: Mathlib.Analysis.SpecialFunctions.Log.Base

Goal state before:
pp: case mp
b x y : ℝ
b_pos : 0 < b
b_ne_one : b ≠ 1
hy : 0 < y
⊢ logb b y = x → b ^ x = y

Tactic:
rintro rfl

Goal state after:
case mp
b y : ℝ
b_pos : 0 < b
b_ne_one : b ≠ 1
hy : 0 < y
⊢ b ^ logb b y = y
Module: Mathlib.Analysis.SpecialFunctions.Log.Base

Goal state before:
pp: case mpr
b x y : ℝ
b_pos : 0 < b
b_ne_one : b ≠ 1
hy : 0 < y
⊢ b ^ x = y → logb b y = x

Tactic:
rintro rfl

Goal state after:
case mpr
b x : ℝ
b_pos : 0 < b
b_ne_one : b ≠ 1
hy : 0 < b ^ x
⊢ logb b (b ^ x) = x
Module: Mathlib.Analysis.SpecialFunctions.Log.Base

Goal state before:
pp: b : ℝ
n : ℕ
⊢ (fun x ↦ logb b x ^ n) =o[atTop] id

Tactic:
Asymptotics.isLittleO_iff_tendsto'

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

b : ℝ
n : ℕ
⊢ ∀ᶠ (x : ℝ) in atTop, id x = 0 → logb b x ^ n = 0
Module: Mathlib.MeasureTheory.Constructions.HaarToSphere

Goal state before:
pp: E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
hx : ‖x‖ = 1
ε : ℝ
hε : 0 < ε
hε2 : ε ≤ 2
y : E
hy : dist y ((1 - ε / 4) • x) < ε / 4
habs : |1 - ε / 4| = 1 - ε / 4
⊢ y ≠ 0

Tactic:
rintro rfl

Goal state after:
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
hx : ‖x‖ = 1
ε : ℝ
hε : 0 < ε
hε2 : ε ≤ 2
habs : |1 - ε / 4| = 1 - ε / 4
hy : dist 0 ((1 - ε / 4) • x) < ε / 4
⊢ False
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: r : ℝ
hr : 0 < r
s : ℂ
hs : ‖s‖ < r
l : ℂ
h : 2 * r ≤ ‖l‖
⊢ s ≠ l

Tactic:
rintro rfl

Goal state after:
r : ℝ
hr : 0 < r
s : ℂ
hs : ‖s‖ < r
h : 2 * r ≤ ‖s‖
⊢ False
Module: Mathlib.Analysis.SpecialFunctions.Pow.NthRootLemmas

Goal state before:
pp: case e'_4
n a b : ℕ
hb : b ≠ 0
h : 0 ≤ (↑b + (↑a - ↑b)) ^ (n + 1) - (↑b ^ (n + 1) + ↑(n + 1) * ↑b ^ (n + 1 - 1) * (↑a - ↑b))
⊢ ↑a ^ n * ↑a + ↑n * ↑b * ↑b ^ n - (↑n + 1) * ↑a * ↑b ^ n =
    (↑b + (↑a - ↑b)) ^ (n + 1) - (↑b ^ (n + 1) + ↑(n + 1) * ↑b ^ (n + 1 - 1) * (↑a - ↑b))

Tactic:
push_cast

Goal state after:
case e'_4
n a b : ℕ
hb : b ≠ 0
h : 0 ≤ (↑b + (↑a - ↑b)) ^ (n + 1) - (↑b ^ (n + 1) + ↑(n + 1) * ↑b ^ (n + 1 - 1) * (↑a - ↑b))
⊢ ↑a ^ n * ↑a + ↑n * ↑b * ↑b ^ n - (↑n + 1) * ↑a * ↑b ^ n =
    (↑b + (↑a - ↑b)) ^ (n + 1) - (↑b ^ (n + 1) + (↑n + 1) * ↑b ^ n * (↑a - ↑b))
Module: Mathlib.Analysis.SpecialFunctions.Pow.NthRootLemmas

Goal state before:
pp: n a : ℕ
H : ∃ c, a < (c + 1) ^ (n + 1)
c : ℕ
hc : c = Nat.find H
⊢ c ^ (n + 1) ≤ a

Tactic:
cases c with
  | zero => simp
  | succ k => simpa using Nat.find_min H hc.le

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

Goal state before:
pp: L : PeriodPair
l₀ : ℂ
hl : l₀ ∉ L.lattice
z : ℂ
l : ↥L.lattice
⊢ ↑l ≠ l₀

Tactic:
rintro rfl

Goal state after:
L : PeriodPair
z : ℂ
l : ↥L.lattice
hl : ↑l ∉ L.lattice
⊢ False
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

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

Tactic:
rintro rfl

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

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

Tactic:
rintro rfl

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

Goal state before:
pp: case neg
a b : Multiset ℂ
n : ℕ
h : regularizedHGFunCoeff a b n ≠ 0
hb : ∃ k ∈ b, k = -↑n
⊢ regularizedHGFunCoeff a b (n + 1) / regularizedHGFunCoeff a b n =
    (Multiset.map (fun x ↦ x + ↑n) a).prod / ((Multiset.map (fun x ↦ x + ↑n) b).prod * (↑n + 1))

Tactic:
obtain ⟨j, hj⟩ := hb
    have h₁ : (b.map (· + (n : ℂ))).prod = 0 := by
      grind [Multiset.prod_eq_zero, Multiset.mem_map]
    simp [regularizedHGFunCoeff_eq_zero_right a b n 0, h₁]

Goal state after:
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₀
x : ℂ
hx : x ∈ (↑L.lattice \ {l₀})ᶜ
⊢ x ≠ ↑i

Tactic:
rintro rfl

Goal state after:
L : PeriodPair
l₀ : ℂ
s : Finset ↥L.lattice
i : ↥L.lattice
hi : i ∈ s
h✝ : ¬↑i = l₀
hx : ↑i ∈ (↑L.lattice \ {l₀})ᶜ
⊢ False
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 : ℂ
h₁ : x ∈ (↑L.lattice \ {l₀ - ↑l})ᶜ
h₂ : x + ↑l ∈ ↑L.lattice
h₃ : x + ↑l ≠ l₀
⊢ x ∉ {l₀ - ↑l}

Tactic:
rintro rfl

Goal state after:
L : PeriodPair
l₀ : ℂ
hl₀ : l₀ ∈ L.lattice
l : ↥L.lattice
hl : ↑l / 2 ∉ L.lattice
h₁ : l₀ - ↑l ∈ (↑L.lattice \ {l₀ - ↑l})ᶜ
h₂ : l₀ - ↑l + ↑l ∈ ↑L.lattice
h₃ : l₀ - ↑l + ↑l ≠ l₀
⊢ False
Module: Mathlib.Analysis.SpecialFunctions.Sigmoid

Goal state before:
pp: x : ℝ
⊢ x.sigmoid * rexp (-x) = (-x).sigmoid

Tactic:
rw [sigmoid_neg, sigmoid_def]

Goal state after:
x : ℝ
⊢ (1 + rexp (-x))⁻¹ * rexp (-x) = 1 - (1 + rexp (-x))⁻¹
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: L : PeriodPair
z : ℂ
l : ↥L.lattice
hl : ↑l / 2 ∉ L.lattice
⊢ l ≠ 0

Tactic:
rintro rfl

Goal state after:
L : PeriodPair
z : ℂ
hl : ↑0 / 2 ∉ L.lattice
⊢ False
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Basic

Goal state before:
pp: case add_two
θ : ℂ
n : ℕ
ih1 : eval (cos θ) (T ℂ (↑n + 1)) = cos (↑(↑n + 1) * θ)
ih2 : eval (cos θ) (T ℂ ↑n) = cos (↑↑n * θ)
⊢ 2 * cos θ * cos (↑(↑n + 1) * θ) = 2 * cos ((↑(↑n + 2) * θ + ↑↑n * θ) / 2) * cos ((↑(↑n + 2) * θ - ↑↑n * θ) / 2)

Tactic:
push_cast

Goal state after:
case add_two
θ : ℂ
n : ℕ
ih1 : eval (cos θ) (T ℂ (↑n + 1)) = cos (↑(↑n + 1) * θ)
ih2 : eval (cos θ) (T ℂ ↑n) = cos (↑↑n * θ)
⊢ 2 * cos θ * cos ((↑n + 1) * θ) = 2 * cos (((↑n + 2) * θ + ↑n * θ) / 2) * cos (((↑n + 2) * θ - ↑n * θ) / 2)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Basic

Goal state before:
pp: case neg_add_one
θ : ℂ
n : ℕ
ih1 : eval (cos θ) (T ℂ (-↑n)) = cos (↑(-↑n) * θ)
ih2 : eval (cos θ) (T ℂ (-↑n + 1)) = cos (↑(-↑n + 1) * θ)
⊢ 2 * cos θ * cos (↑(-↑n) * θ) =
    2 * cos ((↑(-↑n + 1) * θ + ↑(-↑n - 1) * θ) / 2) * cos ((↑(-↑n + 1) * θ - ↑(-↑n - 1) * θ) / 2)

Tactic:
push_cast

Goal state after:
case neg_add_one
θ : ℂ
n : ℕ
ih1 : eval (cos θ) (T ℂ (-↑n)) = cos (↑(-↑n) * θ)
ih2 : eval (cos θ) (T ℂ (-↑n + 1)) = cos (↑(-↑n + 1) * θ)
⊢ 2 * cos θ * cos (-↑n * θ) = 2 * cos (((-↑n + 1) * θ + (-↑n - 1) * θ) / 2) * cos (((-↑n + 1) * θ - (-↑n - 1) * θ) / 2)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Basic

Goal state before:
pp: case add_two
θ : ℂ
n : ℕ
ih1 : eval (cos θ) (U ℂ (↑n + 1)) * sin θ = sin ((↑(↑n + 1) + 1) * θ)
ih2 : eval (cos θ) (U ℂ ↑n) * sin θ = sin ((↑↑n + 1) * θ)
⊢ 2 * (cos θ * sin ((↑(↑n + 1) + 1) * θ)) =
    2 * (sin (((↑(↑n + 2) + 1) * θ + (↑↑n + 1) * θ) / 2) * cos (((↑(↑n + 2) + 1) * θ - (↑↑n + 1) * θ) / 2))

Tactic:
push_cast

Goal state after:
case add_two
θ : ℂ
n : ℕ
ih1 : eval (cos θ) (U ℂ (↑n + 1)) * sin θ = sin ((↑(↑n + 1) + 1) * θ)
ih2 : eval (cos θ) (U ℂ ↑n) * sin θ = sin ((↑↑n + 1) * θ)
⊢ 2 * (cos θ * sin ((↑n + 1 + 1) * θ)) =
    2 * (sin (((↑n + 2 + 1) * θ + (↑n + 1) * θ) / 2) * cos (((↑n + 2 + 1) * θ - (↑n + 1) * θ) / 2))
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Basic

Goal state before:
pp: case neg_add_one
θ : ℂ
n : ℕ
ih1 : eval (cos θ) (U ℂ (-↑n)) * sin θ = sin ((↑(-↑n) + 1) * θ)
ih2 : eval (cos θ) (U ℂ (-↑n + 1)) * sin θ = sin ((↑(-↑n + 1) + 1) * θ)
⊢ 2 * (cos θ * sin ((↑(-↑n) + 1) * θ)) =
    2 *
      (sin (((↑(-↑n + 1) + 1) * θ + (↑(-↑n - 1) + 1) * θ) / 2) *
        cos (((↑(-↑n + 1) + 1) * θ - (↑(-↑n - 1) + 1) * θ) / 2))

Tactic:
push_cast

Goal state after:
case neg_add_one
θ : ℂ
n : ℕ
ih1 : eval (cos θ) (U ℂ (-↑n)) * sin θ = sin ((↑(-↑n) + 1) * θ)
ih2 : eval (cos θ) (U ℂ (-↑n + 1)) * sin θ = sin ((↑(-↑n + 1) + 1) * θ)
⊢ 2 * (cos θ * sin ((-↑n + 1) * θ)) =
    2 * (sin (((-↑n + 1 + 1) * θ + (-↑n - 1 + 1) * θ) / 2) * cos (((-↑n + 1 + 1) * θ - (-↑n - 1 + 1) * θ) / 2))
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

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

Tactic:
by
  trans ℘'[L - l₀] z + ∑' i : L.lattice, if i.1 = l₀.1 then (- 2 / (z - l₀) ^ 3) else 0
  · simp [sub_eq_add_neg, neg_div]
  rw [derivWeierstrassP, derivWeierstrassPExcept, ← Summable.tsum_add, ← tsum_neg]
  · congr with w; split_ifs <;> simp only [zero_add, add_zero, *, neg_div]
  · exact ⟨_, L.hasSum_derivWeierstrassPExcept _ _⟩
  · exact summable_of_hasFiniteSupport ((Set.finite_singleton l₀).subset (by simp))

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

Goal state before:
pp: case refine_1
x : ℝ
n : ℕ∞ω
h : ContDiffAt ℝ n arccos x
⊢ ContDiffAt ℝ n arcsin x

Tactic:
simpa [arccos] using! (contDiffAt_const (c := π / 2)).sub h

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

Goal state before:
pp: case refine_2
x : ℝ
n : ℕ∞ω
h : ContDiffAt ℝ n arcsin x
⊢ ContDiffAt ℝ n arccos x

Tactic:
simpa [arccos] using! (contDiffAt_const (c := π / 2)).sub h

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

Goal state before:
pp: case e'_5
m : ℕ
f : ℕ → ℝ := fun k ↦ 1 / (2 * ↑k + 1) * ((1 / (2 * ↑(m + 1) + 1)) ^ 2) ^ k
k : ℕ
⊢ 1 / (2 * ↑k + 1) * (1 / (2 * ↑(m + 1) + 1)) ^ (2 * k) =
    (↑(m + 1) + 1 / 2) * (2 * (1 / (2 * ↑k + 1)) * ((1 / (2 * (↑m + 1) + 1)) ^ (2 * k) * (1 / (2 * (↑m + 1) + 1)) ^ 1))

Tactic:
push_cast

Goal state after:
case e'_5
m : ℕ
f : ℕ → ℝ := fun k ↦ 1 / (2 * ↑k + 1) * ((1 / (2 * ↑(m + 1) + 1)) ^ 2) ^ k
k : ℕ
⊢ 1 / (2 * ↑k + 1) * (1 / (2 * (↑m + 1) + 1)) ^ (2 * k) =
    (↑m + 1 + 1 / 2) * (2 * (1 / (2 * ↑k + 1)) * ((1 / (2 * (↑m + 1) + 1)) ^ (2 * k) * (1 / (2 * (↑m + 1) + 1)) ^ 1))