mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Polynomial.Basic

Goal state before:
pp: case neg
𝕜 : Type u_1
inst✝³ : NormedField 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
h : P.degree < Q.degree
hp : ¬P = 0
⊢ (fun x ↦ eval x P) =o[atTop] fun x ↦ eval x Q

Tactic:
have hq : Q ≠ 0 := ne_zero_of_degree_ge_degree h.le hp
    have hPQ : ∀ᶠ x in atTop, Q.eval x = 0 → P.eval x = 0 :=
      mem_of_superset (eventually_atTop_not_isRoot Q hq) fun x h h' ↦ absurd h' h
    exact isLittleO_of_tendsto' hPQ (div_tendsto_atTop_zero_of_degree_lt P Q h)

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

Goal state before:
pp: case neg
P : ℝ[X]
x : ℝ
hlc : 0 < P.leadingCoeff
hdeg : 0 < P.degree
hroots : eval x P ≤ 0
z : ℝ
hz : ∀ (b : ℝ), z ≤ b → 0 < eval b P
w : ℝ := max x z
⊢ ∃ y, P.IsRoot y ∧ x ≤ y

Tactic:
have hw : x ≤ w ∧ 0 < P.eval w := ⟨le_max_left .., hz w (le_max_right ..)⟩

Goal state after:
case neg
P : ℝ[X]
x : ℝ
hlc : 0 < P.leadingCoeff
hdeg : 0 < P.degree
hroots : eval x P ≤ 0
z : ℝ
hz : ∀ (b : ℝ), z ≤ b → 0 < eval b P
w : ℝ := max x z
hw : x ≤ w ∧ 0 < eval w P
⊢ ∃ y, P.IsRoot y ∧ x ≤ y
Module: Mathlib.Analysis.Polynomial.Order

Goal state before:
pp: case refine_1
P : ℝ[X]
x : ℝ
hroots : ∀ (y : ℝ), P.IsRoot y → y < x
hlc : P.leadingCoeff ≤ 0
y : ℝ
hy : (-P).IsRoot y
⊢ P.IsRoot y

Tactic:
IsRoot,

Goal state after:
case refine_1
P : ℝ[X]
x : ℝ
hroots : ∀ (y : ℝ), P.IsRoot y → y < x
hlc : P.leadingCoeff ≤ 0
y : ℝ
hy : (-P).IsRoot y
⊢ eval y P = 0
Module: Mathlib.Analysis.Polynomial.Order

Goal state before:
pp: P : ℝ[X]
x : ℝ
hroots : ∀ (y : ℝ), P.IsRoot y → y ≤ x
hlc : P.leadingCoeff ≤ 0
this : 0 ≤ eval x (-P)
⊢ eval x P ≤ 0

Tactic:
apply neg_nonneg.mp

Goal state after:
P : ℝ[X]
x : ℝ
hroots : ∀ (y : ℝ), P.IsRoot y → y ≤ x
hlc : P.leadingCoeff ≤ 0
this : 0 ≤ eval x (-P)
⊢ 0 ≤ -eval x P
Module: Mathlib.Analysis.Polynomial.Order

Goal state before:
pp: case refine_1
P : ℝ[X]
x : ℝ
hroots : ∀ (y : ℝ), P.IsRoot y → y ≤ x
hlc : P.leadingCoeff ≤ 0
y : ℝ
hy : (-P).IsRoot y
⊢ P.IsRoot y

Tactic:
IsRoot,

Goal state after:
case refine_1
P : ℝ[X]
x : ℝ
hroots : ∀ (y : ℝ), P.IsRoot y → y ≤ x
hlc : P.leadingCoeff ≤ 0
y : ℝ
hy : (-P).IsRoot y
⊢ eval y P = 0
Module: Mathlib.Analysis.Polynomial.Order

Goal state before:
pp: case refine_1
P : ℝ[X]
x : ℝ
hroots : ∀ (y : ℝ), P.IsRoot y → x < y
hlc : P.leadingCoeff ≤ 0
y : ℝ
hy : (-P).IsRoot y
⊢ P.IsRoot y

Tactic:
IsRoot,

Goal state after:
case refine_1
P : ℝ[X]
x : ℝ
hroots : ∀ (y : ℝ), P.IsRoot y → x < y
hlc : P.leadingCoeff ≤ 0
y : ℝ
hy : (-P).IsRoot y
⊢ eval y P = 0
Module: Mathlib.Analysis.Polynomial.Order

Goal state before:
pp: P : ℝ[X]
x : ℝ
hroots : ∀ (y : ℝ), P.IsRoot y → x ≤ y
hlc : P.leadingCoeff ≤ 0
this : 0 ≤ ↑↑(↑(-P).natDegree).negOnePow * eval x (-P)
⊢ ↑↑(↑P.natDegree).negOnePow * eval x P ≤ 0

Tactic:
apply neg_nonneg.mp

Goal state after:
P : ℝ[X]
x : ℝ
hroots : ∀ (y : ℝ), P.IsRoot y → x ≤ y
hlc : P.leadingCoeff ≤ 0
this : 0 ≤ ↑↑(↑(-P).natDegree).negOnePow * eval x (-P)
⊢ 0 ≤ -(↑↑(↑P.natDegree).negOnePow * eval x P)
Module: Mathlib.Analysis.Polynomial.Order

Goal state before:
pp: case refine_1
P : ℝ[X]
x : ℝ
hroots : ∀ (y : ℝ), P.IsRoot y → x ≤ y
hlc : P.leadingCoeff ≤ 0
y : ℝ
hy : (-P).IsRoot y
⊢ P.IsRoot y

Tactic:
IsRoot,

Goal state after:
case refine_1
P : ℝ[X]
x : ℝ
hroots : ∀ (y : ℝ), P.IsRoot y → x ≤ y
hlc : P.leadingCoeff ≤ 0
y : ℝ
hy : (-P).IsRoot y
⊢ eval y P = 0
Module: Mathlib.Analysis.RCLike.BoundedContinuous

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝¹ : RCLike 𝕜
inst✝ : PseudoEMetricSpace E
A : StarSubalgebra 𝕜 (E →ᵇ 𝕜)
⊢ Subalgebra.map (toContinuousMapₐ ℝ)
      (Subalgebra.comap (AlgHom.compLeftContinuousBounded ℝ ofRealAm ⋯) (Subalgebra.restrictScalars ℝ A.toSubalgebra)) =
    Subalgebra.comap (AlgHom.compLeftContinuous ℝ ofRealAm ⋯)
      (Subalgebra.restrictScalars ℝ (StarSubalgebra.map (toContinuousMapStarₐ 𝕜) A).toSubalgebra)

Tactic:
ext g
  simp only [Subalgebra.mem_map, Subalgebra.mem_comap, Subalgebra.mem_restrictScalars,
    StarSubalgebra.mem_toSubalgebra, StarSubalgebra.mem_map]
  constructor
  · intro ⟨x, hxA, hxg⟩
    use (@ofRealAm 𝕜 _).compLeftContinuousBounded ℝ lipschitzWith_ofReal x, hxA
    ext a
    simp only [toContinuousMapStarₐ_apply_apply, AlgHom.compLeftContinuousBounded_apply_apply,
      ofRealAm_coe, AlgHom.compLeftContinuous_apply_apply, algebraMap.coe_inj]
    exact DFunLike.congr_fun hxg a
  · intro ⟨x, hxA, hxg⟩
    have hg_apply (a : E) := DFunLike.congr_fun hxg a
    simp only [toContinuousMapStarₐ_apply_apply, AlgHom.compLeftContinuous_apply_apply,
      ofRealAm_coe] at hg_apply
    have h_comp_eq : (@ofRealAm 𝕜 _).compLeftContinuousBounded ℝ lipschitzWith_ofReal
        (x.comp reCLM (@reCLM 𝕜 _).lipschitz) = x := by
      ext a
      simp [hg_apply]
    use x.comp reCLM (@reCLM 𝕜 _).lipschitz
    refine ⟨by rwa [h_comp_eq], ?_⟩
    ext a
    simp [hg_apply]

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

Goal state before:
pp: case inl
α : Type u
β : Type v
φ : Ultrafilter α
inst✝ : LinearOrder β
x y : (↑φ).Germ β
a b : α → β
h : ↑a ≤ ↑b
⊢ ↑b = ↑fun x ↦ max (a x) (b x)

Tactic:
coe_eq

Goal state after:
case inl
α : Type u
β : Type v
φ : Ultrafilter α
inst✝ : LinearOrder β
x y : (↑φ).Germ β
a b : α → β
h : ↑a ≤ ↑b
⊢ b =ᶠ[↑φ] fun x ↦ max (a x) (b x)
Module: Mathlib.Order.Filter.FilterProduct

Goal state before:
pp: case inr
α : Type u
β : Type v
φ : Ultrafilter α
inst✝ : LinearOrder β
x y : (↑φ).Germ β
a b : α → β
h : ↑b ≤ ↑a
⊢ ↑a = ↑fun x ↦ max (a x) (b x)

Tactic:
coe_eq

Goal state after:
case inr
α : Type u
β : Type v
φ : Ultrafilter α
inst✝ : LinearOrder β
x y : (↑φ).Germ β
a b : α → β
h : ↑b ≤ ↑a
⊢ a =ᶠ[↑φ] fun x ↦ max (a x) (b x)
Module: Mathlib.Order.Filter.FilterProduct

Goal state before:
pp: case inl
α : Type u
β : Type v
φ : Ultrafilter α
K : LinearOrder β
x y : (↑φ).Germ β
a b : α → β
h : ↑a ≤ ↑b
⊢ ↑a = ↑fun x ↦ min (a x) (b x)

Tactic:
coe_eq

Goal state after:
case inl
α : Type u
β : Type v
φ : Ultrafilter α
K : LinearOrder β
x y : (↑φ).Germ β
a b : α → β
h : ↑a ≤ ↑b
⊢ a =ᶠ[↑φ] fun x ↦ min (a x) (b x)
Module: Mathlib.Order.Filter.FilterProduct

Goal state before:
pp: case inr
α : Type u
β : Type v
φ : Ultrafilter α
K : LinearOrder β
x y : (↑φ).Germ β
a b : α → β
h : ↑b ≤ ↑a
⊢ ↑b = ↑fun x ↦ min (a x) (b x)

Tactic:
coe_eq

Goal state after:
case inr
α : Type u
β : Type v
φ : Ultrafilter α
K : LinearOrder β
x y : (↑φ).Germ β
a b : α → β
h : ↑b ≤ ↑a
⊢ b =ᶠ[↑φ] fun x ↦ min (a x) (b x)
Module: Mathlib.Analysis.Real.OfDigits

Goal state before:
pp: case e'_4
b : ℕ
digits : ℕ → Fin b
hb : 1 < ↑b
this : 0 < ↑b - 1
⊢ 1 = (↑b - 1) * (↑b)⁻¹ * (1 - (↑b)⁻¹)⁻¹

Tactic:
field

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

Goal state before:
pp: case neg.inr
n : ℕ
p : ℂ[X]
hp : ¬p = 0
hn : n ≤ p.natDegree
⊢ ∑ i ∈ (powersetCard (p.natDegree - n) p.roots).toFinset, ‖count i (powersetCard (p.natDegree - n) p.roots) • i.prod‖ ≤
    ↑(p.natDegree.choose n) * (Multiset.map (fun a ↦ max 1 ‖a‖) p.roots).prod

Tactic:
simp_rw [nsmul_eq_mul, norm_mul, _root_.norm_natCast]

Goal state after:
case neg.inr
n : ℕ
p : ℂ[X]
hp : ¬p = 0
hn : n ≤ p.natDegree
⊢ ∑ x ∈ (powersetCard (p.natDegree - n) p.roots).toFinset,
      ↑(count x (powersetCard (p.natDegree - n) p.roots)) * ‖x.prod‖ ≤
    ↑(p.natDegree.choose n) * (Multiset.map (fun a ↦ max 1 ‖a‖) p.roots).prod
Module: Mathlib.Analysis.Polynomial.MahlerMeasure

Goal state before:
pp: case neg.inr
n : ℕ
p : ℂ[X]
hp : ¬p = 0
hn : n ≤ p.natDegree
S : Multiset (Multiset ℂ) := powersetCard (p.natDegree - n) p.roots
⊢ ∑ x ∈ (powersetCard (p.natDegree - n) p.roots).toFinset,
      ↑(count x (powersetCard (p.natDegree - n) p.roots)) * ‖x.prod‖ ≤
    ↑(p.natDegree.choose n) * (Multiset.map (fun a ↦ max 1 ‖a‖) p.roots).prod

Tactic:
have (x : Multiset ℂ) (hx : x ∈ S.toFinset) : ∏ x_1 ∈ x.toFinset, ‖x_1‖ ^ count x_1 x
      ≤ ∏ m ∈ p.roots.toFinset, max 1 ‖m‖ ^ count m p.roots := by
    rw [mem_toFinset, mem_powersetCard] at hx
    calc
    ∏ z ∈ x.toFinset, ‖z‖ ^ count z x
      ≤ ∏ z ∈ x.toFinset, (1 ⊔ ‖z‖) ^ count z x := by
      gcongr with a
      exact le_max_right 1 ‖a‖
    _ ≤ ∏ z ∈ p.roots.toFinset, (1 ⊔ ‖z‖) ^ count z x := by
      simp_rw [← coe_nnnorm]
      norm_cast
      exact Finset.prod_le_prod_of_subset_of_one_le' (toFinset_subset.mpr (subset_of_le hx.1))
        (fun a _ _ ↦ one_le_pow₀ (le_max_left 1 ‖a‖))
    _ ≤ ∏ z ∈ p.roots.toFinset, (1 ⊔ ‖z‖) ^ count z p.roots := by
      gcongr with a
      · exact le_max_left 1 ‖a‖
      · exact hx.1

Goal state after:
case neg.inr
n : ℕ
p : ℂ[X]
hp : ¬p = 0
hn : n ≤ p.natDegree
S : Multiset (Multiset ℂ) := powersetCard (p.natDegree - n) p.roots
this : ∀ x ∈ S.toFinset, ∏ x_1 ∈ x.toFinset, ‖x_1‖ ^ count x_1 x ≤ ∏ m ∈ p.roots.toFinset, max 1 ‖m‖ ^ count m p.roots
⊢ ∑ x ∈ (powersetCard (p.natDegree - n) p.roots).toFinset,
      ↑(count x (powersetCard (p.natDegree - n) p.roots)) * ‖x.prod‖ ≤
    ↑(p.natDegree.choose n) * (Multiset.map (fun a ↦ max 1 ‖a‖) p.roots).prod
Module: Mathlib.Analysis.Real.OfDigits

Goal state before:
pp: case hf
b : ℕ
inst✝ : NeZero b
this : 1 < |↑b + 1|
⊢ Summable fun n ↦ (↑(b + 1))⁻¹ ^ (n + 1)

Tactic:
summable_nat_add_iff (f := fun n ↦ ((b + 1 : ℕ) : ℝ)⁻¹ ^ n) 1

Goal state after:
case hf
b : ℕ
inst✝ : NeZero b
this : 1 < |↑b + 1|
⊢ Summable fun n ↦ (↑(b + 1))⁻¹ ^ n
Module: Mathlib.Analysis.Real.Pi.Bounds

Goal state before:
pp: ⊢ 3.14159265358979323846 < π

Tactic:
pi_lower_bound [
    671574048197/474874563549, 58134718954/31462283181, 3090459598621/1575502640777,
    2-7143849599/741790664068, 8431536490061/4220852446654, 2-2725579171/4524814682468,
    2-2494895647/16566776788806, 2-608997841/16175484287402, 2-942567063/100141194694075,
    2-341084060/144951150987041, 2-213717653/363295959742218, 2-71906926/488934711121807,
    2-29337101/797916288104986, 2-45326311/4931175952730065, 2-7506877/3266776448781479,
    2-5854787/10191338039232571, 2-4538642/31601378399861717, 2-276149/7691013341581098,
    2-350197/39013283396653714, 2-442757/197299283738495963, 2-632505/1127415566199968707,
    2-1157/8249230030392285, 2-205461/5859619883403334178, 2-33721/3846807755987625852,
    2-11654/5317837263222296743, 2-8162/14897610345776687857, 2-731/5337002285107943372,
    2-1320/38549072592845336201, 2-707/82588467645883795866, 2-53/24764858756615791675,
    2-237/442963888703240952920, 2-128/956951523274512100791, 2-32/956951523274512100783,
    2-27/3229711391051478340136]

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

Goal state before:
pp: A : Type u_2
inst✝¹ : NormedRing A
p : A[X]
v : A →+* ℂ
inst✝ : NormOneClass A
hv : Isometry ⇑v
hp : p.Monic
⊢ 1 ≤ ‖p.leadingCoeff‖

Tactic:
hp.leadingCoeff,

Goal state after:
A : Type u_2
inst✝¹ : NormedRing A
p : A[X]
v : A →+* ℂ
inst✝ : NormOneClass A
hv : Isometry ⇑v
hp : p.Monic
⊢ 1 ≤ ‖1‖
Module: Mathlib.NumberTheory.Real.Irrational

Goal state before:
pp: x : ℝ
h : Irrational x
m : ℤ
⊢ x ≠ ↑m

Tactic:
rw [← Rat.cast_intCast]

Goal state after:
x : ℝ
h : Irrational x
m : ℤ
⊢ x ≠ ↑↑m
Module: Mathlib.NumberTheory.Real.Irrational

Goal state before:
pp: x : ℝ
n : ℕ
h : Irrational (x ^ -[n+1])
⊢ Irrational x

Tactic:
zpow_negSucc

Goal state after:
x : ℝ
n : ℕ
h : Irrational (x ^ (n + 1))⁻¹
⊢ Irrational x
Module: Mathlib.Analysis.Real.Hyperreal

Goal state before:
pp: case neg
x : ℝ*
h : ¬x.Infinite
⊢ (-x).st = -x.st

Tactic:
exact (isSt_st' (not_infinite_neg h)).unique (isSt_st' h).neg

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

Goal state before:
pp: z : ℂ
h₁ : z ≠ I
h₂ : z ≠ -I
z₁ : 1 + z * I ≠ 0
z₂ : 1 - z * I ≠ 0
⊢ cexp (2 * (-I / 2 * log ((1 + z * I) / (1 - z * I)) * I)) = (1 + z * I) / (1 - z * I)

Tactic:
← mul_rotate,

Goal state after:
z : ℂ
h₁ : z ≠ I
h₂ : z ≠ -I
z₁ : 1 + z * I ≠ 0
z₂ : 1 - z * I ≠ 0
⊢ cexp (2 * (I * (-I / 2) * log ((1 + z * I) / (1 - z * I)))) = (1 + z * I) / (1 - z * I)
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arctan

Goal state before:
pp: z : ℂ
h₀ : z ≠ ↑π / 2
h₁ : -(π / 2) < z.re
h₂ : z.re ≤ π / 2
h : cos z ≠ 0
⊢ -I / 2 * log ((cos z + sin z / cos z * I * cos z) / (cos z - sin z / cos z * I * cos z)) = z

Tactic:
← mul_rotate,

Goal state after:
z : ℂ
h₀ : z ≠ ↑π / 2
h₁ : -(π / 2) < z.re
h₂ : z.re ≤ π / 2
h : cos z ≠ 0
⊢ -I / 2 * log ((cos z + cos z * (sin z / cos z) * I) / (cos z - cos z * (sin z / cos z) * I)) = z
Module: Mathlib.Analysis.SpecialFunctions.Artanh

Goal state before:
pp: x : ℝ
h : 0 < (1 + tanh x) / (1 - tanh x)
⊢ (1 + (rexp x - (rexp x)⁻¹) / (rexp x + (rexp x)⁻¹)) / (1 - (rexp x - (rexp x)⁻¹) / (rexp x + (rexp x)⁻¹)) = rexp x ^ 2

Tactic:
field

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

Goal state before:
pp: p : ℝ
⊢ DifferentiableAt ℝ binEntropy p ↔ p ≠ 0 ∧ p ≠ 1

Tactic:
refine ⟨fun h ↦ ⟨?_, ?_⟩, fun h ↦ differentiableAt_binEntropy h.1 h.2⟩
    <;> rintro rfl <;> unfold binEntropy at h
  · rw [DifferentiableAt.fun_add_iff_left] at h
    · simp [log_inv, mul_neg, ← neg_mul, ← negMulLog_def, differentiableAt_negMulLog_iff] at h
    · fun_prop (disch := simp)
  · 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

Goal state after:
case pos
q : ℕ
p : ℝ
xne0 : p ≠ 0
xne1 : p ≠ 1
⊢ deriv (deriv (qaryEntropy q)) p = -1 / (p * (1 - p))
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Order

Goal state before:
pp: A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a b : A
hab : a ≤ b
⊢ sqrt a ≤ sqrt b

Tactic:
rw [CFC.sqrt_eq_nnrpow a, CFC.sqrt_eq_nnrpow b]

Goal state after:
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a b : A
hab : a ≤ b
⊢ a ^ (1 / 2) ≤ b ^ (1 / 2)
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
F : Filter ℝ
hpos : ∀ᶠ (t : ℝ) in F, 0 < t
V : E
huni : ∀ δ > 0, ∀ᶠ (t : ℝ) in F, ∀ x ∈ uIoc (a * t) (b * t), ‖f x - V‖ ≤ δ
δ : ℝ
hδ : δ > 0
C : ℝ := |log (b / a)|
hC_def : C = |log (b / a)|
δ' : ℝ := δ / (C + 1)
t : ℝ
ht_pos : 0 < t
hbound : ∀ x ∈ uIoc (a * t) (b * t), ‖f x - V‖ ≤ δ'
⊢ dist (∫ (x : ℝ) in a * t..b * t, x⁻¹ • f x) (log (b / a) • V) < δ

Tactic:
have hlog_eq : log (b * t / (a * t)) = log (b / a) := by
    rw [mul_div_mul_right b a (ne_of_gt ht_pos)]

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
F : Filter ℝ
hpos : ∀ᶠ (t : ℝ) in F, 0 < t
V : E
huni : ∀ δ > 0, ∀ᶠ (t : ℝ) in F, ∀ x ∈ uIoc (a * t) (b * t), ‖f x - V‖ ≤ δ
δ : ℝ
hδ : δ > 0
C : ℝ := |log (b / a)|
hC_def : C = |log (b / a)|
δ' : ℝ := δ / (C + 1)
t : ℝ
ht_pos : 0 < t
hbound : ∀ x ∈ uIoc (a * t) (b * t), ‖f x - V‖ ≤ δ'
hlog_eq : log (b * t / (a * t)) = log (b / a)
⊢ dist (∫ (x : ℝ) in a * t..b * t, x⁻¹ • f x) (log (b / a) • V) < δ
Module: Mathlib.NumberTheory.Harmonic.EulerMascheroni

Goal state before:
pp: case inr.refine_2
n : ℕ
hn : n > 0
⊢ (↑(n + 1) / ↑n)⁻¹ ≠ 1

pp: case inr.refine_3
n : ℕ
hn : n > 0
⊢ (↑(n + 1) / ↑n)⁻¹ - 1 = -↑(↑(n + 1))⁻¹

Tactic:
· simp [field]

Goal state after:
case inr.refine_3
n : ℕ
hn : n > 0
⊢ (↑(n + 1) / ↑n)⁻¹ - 1 = -↑(↑(n + 1))⁻¹
Module: Mathlib.NumberTheory.Harmonic.EulerMascheroni

Goal state before:
pp: case inr.refine_3
n : ℕ
hn : n > 0
⊢ (↑(n + 1) / ↑n)⁻¹ - 1 = -↑(↑(n + 1))⁻¹

Tactic:
· simp [field]

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

Goal state before:
pp: h1 : eulerMascheroniSeq' 6 = 49 / 20 - log 6
⊢ eulerMascheroniSeq' 6 < 2 / 3

Tactic:
rw [h1, sub_lt_iff_lt_add, ← sub_lt_iff_lt_add', lt_log_iff_exp_lt (by positivity)]

Goal state after:
h1 : eulerMascheroniSeq' 6 = 49 / 20 - log 6
⊢ rexp (49 / 20 - 2 / 3) < 6
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation

Goal state before:
pp: p : ℝ
hp : p ∈ Ioo 0 1
⊢ 0 < -1 / (2 * (p - 1))

Tactic:
by
      rw [neg_div, neg_pos, one_div_neg]
      push _ ∈ _ at hp
      linarith

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

Goal state before:
pp: case neg
s : ℂ
hs : ∀ (n : ℕ), s ≠ -↑n
h : s - 1 ≠ 0
h' : ∀ (n : ℕ), s - 1 ≠ -↑n
A : ℂ
⊢ (s - 1).Gammaℂ * sin (↑π * (s / 2)) * A =
    (s - 1).Gammaℂ * ((s - 1) / 2 / ↑π) * sin (↑π * (s / 2)) * (A * ((s - 1) / 2 / ↑π)⁻¹)

Tactic:
field

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

Goal state before:
pp: h_diff : ∀ {s : ℝ}, 0 < s → DifferentiableAt ℝ Gamma s
h_diff' : ∀ {s : ℝ}, 0 < s → DifferentiableAt ℝ (fun s ↦ Gamma (2 * s)) s
⊢ √π * (deriv (fun s ↦ Gamma (2 * s) * 2 ^ (1 - 2 * s)) (1 / 2) + γ) =
    √π * (deriv (fun s ↦ Gamma (2 * s)) (1 / 2) + deriv (fun s ↦ 2 ^ (1 - 2 * s)) (1 / 2) + γ)

Tactic:
rw [deriv_fun_mul]

Goal state after:
h_diff : ∀ {s : ℝ}, 0 < s → DifferentiableAt ℝ Gamma s
h_diff' : ∀ {s : ℝ}, 0 < s → DifferentiableAt ℝ (fun s ↦ Gamma (2 * s)) s
⊢ √π *
      (deriv (fun s ↦ Gamma (2 * s)) (1 / 2) * 2 ^ (1 - 2 * (1 / 2)) +
          Gamma (2 * (1 / 2)) * deriv (fun s ↦ 2 ^ (1 - 2 * s)) (1 / 2) +
        γ) =
    √π * (deriv (fun s ↦ Gamma (2 * s)) (1 / 2) + deriv (fun s ↦ 2 ^ (1 - 2 * s)) (1 / 2) + γ)

case hc
h_diff : ∀ {s : ℝ}, 0 < s → DifferentiableAt ℝ Gamma s
h_diff' : ∀ {s : ℝ}, 0 < s → DifferentiableAt ℝ (fun s ↦ Gamma (2 * s)) s
⊢ DifferentiableAt ℝ (fun s ↦ Gamma (2 * s)) (1 / 2)

case hd
h_diff : ∀ {s : ℝ}, 0 < s → DifferentiableAt ℝ Gamma s
h_diff' : ∀ {s : ℝ}, 0 < s → DifferentiableAt ℝ (fun s ↦ Gamma (2 * s)) s
⊢ DifferentiableAt ℝ (fun s ↦ 2 ^ (1 - 2 * s)) (1 / 2)
Module: Mathlib.Analysis.SpecialFunctions.Gaussian.PoissonSummation

Goal state before:
pp: a b : ℂ
f : ℝ → ℂ := fun x ↦ cexp (-↑π * a * ↑x ^ 2 + 2 * ↑π * b * ↑x)
hFf : 𝓕 f = fun x ↦ 1 / a ^ (1 / 2) * cexp (-↑π / a * (↑x + I * b) ^ 2)
h1 : 0 < (↑π * a).re
ha : a = 0
⊢ re 0 ≤ 0

Tactic:
zero_re

Goal state after:
a b : ℂ
f : ℝ → ℂ := fun x ↦ cexp (-↑π * a * ↑x ^ 2 + 2 * ↑π * b * ↑x)
hFf : 𝓕 f = fun x ↦ 1 / a ^ (1 / 2) * cexp (-↑π / a * (↑x + I * b) ^ 2)
h1 : 0 < (↑π * a).re
ha : a = 0
⊢ 0 ≤ 0
Module: Mathlib.NumberTheory.Harmonic.GammaDeriv

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

Tactic:
exact_mod_cast differentiableAt_Gamma_nat_add_one n

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

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

Tactic:
exact abs_of_pos hx

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

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

Tactic:
rpow_logb_eq_abs b_pos b_ne_one (ne_of_lt hx)

Goal state after:
b x : ℝ
b_pos : 0 < b
b_ne_one : b ≠ 1
hx : x < 0
⊢ |x| = -x
Module: Mathlib.Analysis.SpecialFunctions.Log.Base

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

Tactic:
rw [logb_pos_iff hb (lt_trans zero_lt_one hx)]
  exact hx

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

Goal state before:
pp: A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
p t : ℝ
hp : p ∈ Ioo 0 1
ht : 0 < t
⊢ MonotoneOn (cfcₙ (p.rpowIntegrand₀₁ t)) (Ici 0)

Tactic:
intro a (ha : 0 ≤ a) b (hb : 0 ≤ b) hab
  calc
    _ = t ^ ((p : ℝ) - 1) • cfcₙ (rpowIntegrand₀₁ p 1) (t⁻¹ • a) := by
      rw [cfcₙ_rpowIntegrand₀₁_eq_cfcₙ_rpowIntegrand₀₁_one hp ht a ha]
    _ ≤ t ^ ((p : ℝ) - 1) • cfcₙ (rpowIntegrand₀₁ p 1) (t⁻¹ • b) := by
      gcongr
      unfold rpowIntegrand₀₁
      simp only [Real.one_rpow, one_mul, inv_one]
      refine CFC.monotoneOn_one_sub_one_add_inv_real
        (?_ : 0 ≤ t⁻¹ • a) (?_ : 0 ≤ t⁻¹ • b) (by gcongr)
      all_goals positivity
    _ = cfcₙ (rpowIntegrand₀₁ p t) b := by
      rw [cfcₙ_rpowIntegrand₀₁_eq_cfcₙ_rpowIntegrand₀₁_one hp ht b hb]

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

Goal state before:
pp: b x : ℝ
b_pos : 0 < b
b_lt_one : b < 1
hx : 0 < x
⊢ 0 ≤ logb b x ↔ x ≤ 1

Tactic:
by
  rw [← not_lt, logb_neg_iff_of_base_lt_one b_pos b_lt_one hx, not_lt]

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

Goal state before:
pp: ε : ℝ
hε : 0 < ε
x : ℝ
⊢ ‖deriv ε.mulExpNegMulSq x‖ ≤ 1

Tactic:
by
  rw [norm_eq_abs, deriv_mulExpNegMulSq]
  have heq : exp (-(ε * x * x)) + x * (exp (-(ε * x * x)) * (-2 * ε * x))
      = exp (-(ε * x * x)) * (1 - 2 * (ε * x * x)) := by ring
  rw [heq, abs_mul, abs_exp]
  set y := ε * x * x with hy
  have hynonneg : 0 ≤ y := by
    rw [hy, mul_assoc]
    exact mul_nonneg hε.le (mul_self_nonneg x)
  apply mul_le_of_le_inv_mul₀ (zero_le_one' ℝ) (exp_nonneg _)
  simp only [← exp_neg (-y), neg_neg, mul_one, abs_le, neg_le_sub_iff_le_add, tsub_le_iff_right]
  refine ⟨le_trans two_mul_le_exp ((le_add_iff_nonneg_left (exp y)).mpr zero_le_one), ?_⟩
  exact le_trans (one_le_exp hynonneg) (le_add_of_nonneg_right (by simp [hynonneg]))

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

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

Tactic:
rw [Asymptotics.isLittleO_iff_tendsto']
  · simpa using tendsto_pow_logb_div_mul_add_atTop 1 0 n one_ne_zero
  · filter_upwards [eventually_ne_atTop (0 : ℝ)] with x h₁ h₂ using (h₁ h₂).elim

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

Goal state before:
pp: case inl
⊢ (fun x ↦ log (0 * x)) =O[atTop] log

pp: case inr
c : ℝ
hc : c ≠ 0
⊢ (fun x ↦ log (c * x)) =O[atTop] log

Tactic:
· simpa using isLittleO_const_log_atTop.isBigO

Goal state after:
case inr
c : ℝ
hc : c ≠ 0
⊢ (fun x ↦ log (c * x)) =O[atTop] log
Module: Mathlib.Analysis.SpecialFunctions.MulExpNegMulSqIntegral

Goal state before:
pp: case h_meas
E : Type u_1
inst✝³ : TopologicalSpace E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
P : Measure E
inst✝ : IsFiniteMeasure P
ε : ℝ
g : E →ᵇ ℝ
hε : 0 < ε
⊢ ∀ᶠ (n : ℕ) in atTop, AEStronglyMeasurable (⇑(g * (1 + (↑n)⁻¹ • -(ε • g * g)) ^ n)) P

Tactic:
apply Eventually.of_forall
    exact fun n => StronglyMeasurable.aestronglyMeasurable (Continuous.stronglyMeasurable
        (Continuous.mul g.continuous ((1 + ((n : ℝ)⁻¹ • -(ε • g * g))) ^ n).continuous))

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

Goal state before:
pp: r : ℝ
hr : 0 < r
s : ℂ
hs : ‖s‖ < r
l : ℂ
h : 2 * r ≤ ‖l‖
this✝ : s ≠ l
this : 0 < ‖l‖
⊢ ‖s‖ * ‖2 * l - s‖ / (‖l‖ ^ 4 / 4) = 4 * ‖s‖ * ‖2 * l - s‖ / ‖l‖ ^ 4

Tactic:
field

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

Goal state before:
pp: r : ℝ
hr : 0 < r
s : ℂ
hs : ‖s‖ < r
l : ℂ
h : 2 * r ≤ ‖l‖
this✝ : s ≠ l
this : 0 < ‖l‖
⊢ 4 * r * (2.5 * ‖l‖) / ‖l‖ ^ 4 = 10 * r / ‖l‖ ^ 3

Tactic:
field

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

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

Tactic:
rintro ⟨x, rfl⟩

Goal state after:
case mp
n : ℕ
hn : n ≠ 0
x : ℕ
⊢ n.nthRoot (x ^ n) ^ n = x ^ n
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: case hab
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
⊢ ‖l‖ ≤ 2 * ‖↑l - s‖

Tactic:
refine le_trans ?_ (mul_le_mul le_rfl (norm_sub_norm_le _ _) (by linarith) (by linarith))

Goal state after:
case hab
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
⊢ ‖l‖ ≤ 2 * (‖↑l‖ - ‖s‖)