mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.MvPowerSeries.GaussNorm

Goal state before:
pp: case refine_1
R : Type u_1
σ : Type u_2
v : R → ℝ
c : σ → ℝ
inst✝ : Semiring R
f g : MvPowerSeries σ R
hc : 0 ≤ c
vNonneg : ∀ (a : R), v a ≥ 0
vMul : ∀ (a b : R), v (a * b) ≤ v a * v b
vna : IsNonarchimedean v
vZero : v 0 = 0
hbfd : HasGaussNorm v c f
hbgd : HasGaussNorm v c g
t : σ →₀ ℕ
k : (σ →₀ ℕ) × (σ →₀ ℕ)
hk : (Finset.antidiagonal t).Nonempty → k ∈ Finset.antidiagonal t
hsum : v (∑ a ∈ Finset.antidiagonal t, (coeff a.1) f * (coeff a.2) g) ≤ v ((coeff k.1) f * (coeff k.2) g)
hk' : k.1 + k.2 = t
⊢ (v ((coeff t) (f * g)) * t.prod fun x1 x2 ↦ c x1 ^ x2) ≤ gaussNorm v c f * gaussNorm v c g

Tactic:
have hprod : t.prod (c · ^ ·) = k.1.prod (c · ^ ·) * k.2.prod (c · ^ ·) := by
      simp [← hk', Finsupp.prod_add_index' (h := (c · ^ ·)) (by grind) (by grind)]

Goal state after:
case refine_1
R : Type u_1
σ : Type u_2
v : R → ℝ
c : σ → ℝ
inst✝ : Semiring R
f g : MvPowerSeries σ R
hc : 0 ≤ c
vNonneg : ∀ (a : R), v a ≥ 0
vMul : ∀ (a b : R), v (a * b) ≤ v a * v b
vna : IsNonarchimedean v
vZero : v 0 = 0
hbfd : HasGaussNorm v c f
hbgd : HasGaussNorm v c g
t : σ →₀ ℕ
k : (σ →₀ ℕ) × (σ →₀ ℕ)
hk : (Finset.antidiagonal t).Nonempty → k ∈ Finset.antidiagonal t
hsum : v (∑ a ∈ Finset.antidiagonal t, (coeff a.1) f * (coeff a.2) g) ≤ v ((coeff k.1) f * (coeff k.2) g)
hk' : k.1 + k.2 = t
hprod : (t.prod fun x1 x2 ↦ c x1 ^ x2) = (k.1.prod fun x1 x2 ↦ c x1 ^ x2) * k.2.prod fun x1 x2 ↦ c x1 ^ x2
⊢ (v ((coeff t) (f * g)) * t.prod fun x1 x2 ↦ c x1 ^ x2) ≤ gaussNorm v c f * gaussNorm v c g
Module: Mathlib.Analysis.Polynomial.Order

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

Tactic:
rw [eq_of_ge_of_le hle (hroots y hroot), hroot, mul_zero]

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

Goal state before:
pp: p : ℂ[X]
⊢ ‖p.leadingCoeff‖ ≤ p.mahlerMeasure

Tactic:
rw [← mul_one ‖_‖, mahlerMeasure_eq_leadingCoeff_mul_prod_roots]
  gcongr
  exact one_le_prod_max_one_norm_roots p

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

Goal state before:
pp: case a
n : ℕ
p : ℂ[X]
hp : ¬p = 0
hn : n ≤ p.natDegree
S : Multiset (Multiset ℂ) := ⋯
x : Multiset ℂ
hx : x ≤ p.roots ∧ x.card = p.natDegree - n
a : ℂ
a✝ : a ∈ p.roots.toFinset
⊢ x ≤ p.roots

Tactic:
exact hx.1

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

Goal state before:
pp: x : ℝ*
r : ℝ
hx : (∀ s < r, ↑s ≤ x) ∧ ∀ s > r, x ≤ ↑s
⊢ stdPart x = r

Tactic:
exact stdPart_eq coeRingHom hx.1 hx.2

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

Goal state before:
pp: case refine_1
x : ℝ*
h : x.InfiniteNeg
⊢ x < 0 ∧ ArchimedeanClass.mk x < 0

pp: case refine_2
x : ℝ*
x✝ : x < 0 ∧ ArchimedeanClass.mk x < 0
r : ℝ
hx : x < 0
hx' : ArchimedeanClass.mk x < 0
⊢ x < ↑r

Tactic:
· have hx : x < 0 := h 0
    refine ⟨h 0, fun n ↦ ?_⟩
    simpa [abs_of_neg hx, lt_neg] using! h (-n)

Goal state after:
case refine_2
x : ℝ*
x✝ : x < 0 ∧ ArchimedeanClass.mk x < 0
r : ℝ
hx : x < 0
hx' : ArchimedeanClass.mk x < 0
⊢ x < ↑r
Module: Mathlib.Analysis.Real.Hyperreal

Goal state before:
pp: x : ℝ*
hni : 0 ≤ ArchimedeanClass.mk x
⊢ x.IsSt (sSup {y | ↑y < x})

Tactic:
rw [isSt_iff]

Goal state after:
x : ℝ*
hni : 0 ≤ ArchimedeanClass.mk x
⊢ 0 ≤ ArchimedeanClass.mk x ∧ stdPart x = sSup {y | ↑y < x}
Module: Mathlib.Analysis.Real.Hyperreal

Goal state before:
pp: r : ℝ
⊢ ¬(↑r).Infinite

Tactic:
rw [not_infinite_iff_exist_lt_gt]
  exact ⟨r - 1, r + 1, coe_lt_coe.2 <| sub_one_lt r, coe_lt_coe.2 <| lt_add_one r⟩

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

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

Tactic:
rw [h.st_eq, (infinite_neg.2 h).st_eq, neg_zero]

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

Goal state before:
pp: k : ℕ
⊢ (π / 2)⁻¹ * W k = (∫ (x : ℝ) in 0..π, sin x ^ (2 * k + 1)) / (π * ∏ i ∈ range k, (2 * ↑i + 1) / (2 * ↑i + 2))

Tactic:
integral_sin_pow_odd,

Goal state after:
k : ℕ
⊢ (π / 2)⁻¹ * W k = (2 * ∏ i ∈ range k, (2 * ↑i + 2) / (2 * ↑i + 3)) / (π * ∏ i ∈ range k, (2 * ↑i + 1) / (2 * ↑i + 2))
Module: Mathlib.Analysis.SpecialFunctions.Arcosh

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

Tactic:
by
  apply exp_log
  positivity

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

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

Tactic:
sq_sqrt (sub_nonneg_of_le (one_le_pow₀ hx)),

Goal state after:
x : ℝ
hx : 1 ≤ x
⊢ x ^ 2 - (x ^ 2 - 1) = 1
Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean

Goal state before:
pp: x y : ℝ≥0
h : x ≠ y
hl : y < x
key : 0 < (x - y) ^ 2
⊢ sqrt (x * y) < (x + y) / 2

Tactic:
rw [sq, tsub_mul, mul_tsub, mul_tsub, tsub_tsub_eq_add_tsub_of_le (by gcongr),
    tsub_add_eq_add_tsub (by gcongr), tsub_tsub, show x * y + y * x = 2 * x * y by ring,
    tsub_pos_iff_lt, ← sq, ← sq] at key

Goal state after:
x y : ℝ≥0
h : x ≠ y
hl : y < x
key : 2 * x * y < x ^ 2 + y ^ 2
⊢ sqrt (x * y) < (x + y) / 2
Module: Mathlib.Analysis.SpecialFunctions.Artanh

Goal state before:
pp: x : ℝ
hx : x ∈ Ioo 0 1
⊢ 0 < x

Tactic:
exact hx.1

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

Goal state before:
pp: case e'_6
z : ℂ
hz : ‖z‖ < 1
this :
  HasSum (fun x ↦ -I / 2 * (((-1) ^ (2 * x.1 + ↑x.2 + 1) + 1) * (z * I) ^ (2 * x.1 + ↑x.2) / ↑(2 * x.1 + ↑x.2)))
    (-I / 2 * log ((1 + z * I) / (1 - z * I)))
k : ℕ
⊢ (-1) ^ k * z ^ (2 * k + 1) / ↑(2 * k + 1) =
    -I / 2 * (((-1) ^ (2 * k + 1 + 1) + 1) * (z * I) ^ (2 * k + 1) / ↑(2 * k + 1))

Tactic:
show 2 * k + 1 + 1 = 2 * (k + 1) by ring,

Goal state after:
case e'_6
z : ℂ
hz : ‖z‖ < 1
this :
  HasSum (fun x ↦ -I / 2 * (((-1) ^ (2 * x.1 + ↑x.2 + 1) + 1) * (z * I) ^ (2 * x.1 + ↑x.2) / ↑(2 * x.1 + ↑x.2)))
    (-I / 2 * log ((1 + z * I) / (1 - z * I)))
k : ℕ
⊢ (-1) ^ k * z ^ (2 * k + 1) / ↑(2 * k + 1) =
    -I / 2 * (((-1) ^ (2 * (k + 1)) + 1) * (z * I) ^ (2 * k + 1) / ↑(2 * k + 1))
Module: Mathlib.Analysis.Real.Pi.Irrational

Goal state before:
pp: case e'_2
θ : ℝ
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
⊢ ∫ (x : ℝ) in -1..1, -(u₁' x * v₁ x) * θ = ∫ (x : ℝ) in -1..1, -2 * (↑n + 1) * (u₂ x * v₂' x)

Tactic:
congr 1 with x

Goal state after:
case e'_2.e_f
θ : ℝ
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
x : ℝ
⊢ -(u₁' x * v₁ x) * θ = -2 * (↑n + 1) * (u₂ x * v₂' x)
Module: Mathlib.Analysis.SpecialFunctions.Choose

Goal state before:
pp: k : ℕ
⊢ (fun n ↦ ↑(n.choose k)) =Θ[atTop] fun n ↦ ↑n ^ k

Tactic:
apply (isEquivalent_choose k).trans_isTheta

Goal state after:
k : ℕ
⊢ (fun n ↦ ↑n ^ k / ↑k !) =Θ[atTop] fun n ↦ ↑n ^ k
Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy

Goal state before:
pp: case neg
p : ℝ
hp : ¬(p ≠ 0 ∧ p ≠ 1)
⊢ deriv binEntropy p = log (1 - p) - log p

Tactic:
· rw [deriv_zero_of_not_differentiableAt (differentiableAt_binEntropy_iff_ne_zero_one.not.2 hp)]
    push +distrib Not at hp
    obtain rfl | rfl := hp <;> simp

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

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

Tactic:
exact hx.1

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

Goal state before:
pp: ⊢ StrictAntiOn binEntropy (Icc 2⁻¹ 1)

Tactic:
by
  rw [show (Icc (2⁻¹ : ℝ) 1) = Icc (1 / 2) 1 by norm_num, ← qaryEntropy_two]
  convert! qaryEntropy_strictAntiOn (by rfl) using 1
  norm_num

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

Goal state before:
pp: case pos.inl.inr
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
p : ℝ≥0
a b : A
hab : a ≤ b
ha : 0 ≤ a
hb : 0 ≤ b
hIcc : Icc 0 1 = Ioo 0 1 ∪ {0} ∪ {1}
hp : p ∈ {0}
⊢ (fun a ↦ a ^ p) a ≤ (fun a ↦ a ^ p) b

Tactic:
simp_all [mem_singleton_iff]

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
⊢ b ^ i ∣ b ^ (k - i) * b ^ i

Tactic:
exact dvd_mul_left _ _

Goal state after:
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
g : A → A := fun a ↦ if a ∈ s then log a else 0
hg : Set.EqOn g log s
h₁ : ∀ᶠ (p : ℝ) in 𝓝[>] 0, 0 < p ∧ p < 1
p : ℝ
hp : 0 < p
hp' : p < 1
⊢ MonotoneOn (f p) {a | IsStrictlyPositive a}

Tactic:
refine MonotoneOn.congr (fun a ha b hb hab ↦ ?_) CFC.cfc_rpow_sub_one_eqOn.symm

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
hg : Set.EqOn g log s
h₁ : ∀ᶠ (p : ℝ) in 𝓝[>] 0, 0 < p ∧ p < 1
p : ℝ
hp : 0 < p
hp' : p < 1
a : A
ha : a ∈ {a | IsStrictlyPositive a}
b : A
hb : b ∈ {a | IsStrictlyPositive a}
hab : a ≤ b
⊢ p⁻¹ • (a ^ p - 1) ≤ p⁻¹ • (b ^ p - 1)
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.RingInverseOrder

Goal state before:
pp: A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
x : A
xpos : IsStrictlyPositive x
y : A
ypos : IsStrictlyPositive y
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
z : A := (conjSqrt x⁻¹ʳ) y
zpos : IsStrictlyPositive z
xinvpos : IsStrictlyPositive x⁻¹ʳ
⊢ (a • x + b • y)⁻¹ʳ ≤ a • x⁻¹ʳ + b • y⁻¹ʳ

Tactic:
have hsp : IsStrictlyPositive (a • 1 + b • z) := by
    by_cases ha' : 0 < a <;> grind [smul_nonneg]

Goal state after:
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
x : A
xpos : IsStrictlyPositive x
y : A
ypos : IsStrictlyPositive y
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
z : A := (conjSqrt x⁻¹ʳ) y
zpos : IsStrictlyPositive z
xinvpos : IsStrictlyPositive x⁻¹ʳ
hsp : IsStrictlyPositive (a • 1 + b • z)
⊢ (a • x + b • y)⁻¹ʳ ≤ a • x⁻¹ʳ + b • y⁻¹ʳ
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.RingInverseOrder

Goal state before:
pp: A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
t : ℝ
ht : 0 < t
this : ∀ x ∈ Ici 0, IsStrictlyPositive ((algebraMap ℝ A) t + x)
addl : A →ᵃ[ℝ] A := (AffineMap.toConstProdLinearMap ℝ).symm ((algebraMap ℝ A) t, LinearMap.id)
haddl : Function.Injective ⇑addl
hici : Ici 0 = ⇑addl ⁻¹' ⇑addl '' Ici 0
⊢ ConvexOn ℝ (Ici 0) fun x ↦ Ring.inverse ((algebraMap ℝ A) t + x)

Tactic:
simp_rw [add_comm]

Goal state after:
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
t : ℝ
ht : 0 < t
this : ∀ x ∈ Ici 0, IsStrictlyPositive ((algebraMap ℝ A) t + x)
addl : A →ᵃ[ℝ] A := (AffineMap.toConstProdLinearMap ℝ).symm ((algebraMap ℝ A) t, LinearMap.id)
haddl : Function.Injective ⇑addl
hici : Ici 0 = ⇑addl ⁻¹' ⇑addl '' Ici 0
⊢ ConvexOn ℝ (Ici 0) fun x ↦ Ring.inverse (x + (algebraMap ℝ A) t)
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation

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

Tactic:
simpa using Eq.symm <| Real.rpow_add' hx (by aesop : (p - 1) + 1 ≠ 0)

Goal state after:
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
⊢ p.rpowIntegrand₀₁ t x = t ^ (p - 1) * x / (t + x)

Tactic:
rw [rpowIntegrand₀₁_eq_pow_div hp ht hx]

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

Goal state before:
pp: m n : ℕ
this : ∀ (r : ℕ), eulerMascheroniSeq r < eulerMascheroniSeq' r
⊢ eulerMascheroniSeq m < eulerMascheroniSeq' n

Tactic:
apply (strictMono_eulerMascheroniSeq.monotone (le_max_left m n)).trans_lt

Goal state after:
m n : ℕ
this : ∀ (r : ℕ), eulerMascheroniSeq r < eulerMascheroniSeq' r
⊢ eulerMascheroniSeq (max m n) < eulerMascheroniSeq' n
Module: Mathlib.Data.Int.Log

Goal state before:
pp: R : Type u_1
inst✝³ : Semifield R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorSemiring R
b : ℕ
r : R
hb : 1 < b
hr : 0 < r
⊢ ↑b ^ log b r ≤ r

Tactic:
rcases le_total 1 r with hr1 | hr1

Goal state after:
case inl
R : Type u_1
inst✝³ : Semifield R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorSemiring R
b : ℕ
r : R
hb : 1 < b
hr : 0 < r
hr1 : 1 ≤ r
⊢ ↑b ^ log b r ≤ r

case inr
R : Type u_1
inst✝³ : Semifield R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorSemiring R
b : ℕ
r : R
hb : 1 < b
hr : 0 < r
hr1 : r ≤ 1
⊢ ↑b ^ log b r ≤ r
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
hf : HasDerivAt f (-log ↑π / 2 / ↑√π) 1
hg : HasDerivAt g (-↑√π * (↑γ + 2 * log 2) / 2) 1
⊢ -(↑γ + (↑2 * log ↑2 + ↑(Real.log π))) / ↑2 = -(↑γ + log (4 * ↑π)) / ↑2

Tactic:
← ofReal_log zero_le_two,

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

Goal state before:
pp: b x y : ℝ
hx : x ≠ 0
hy : y ≠ 0
⊢ logb b (x / y) = logb b x - logb b y

Tactic:
simp_rw [logb, log_div hx hy, sub_div]

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:
apply log_injOn_pos

Goal state after:
case a
b x : ℝ
b_pos : 0 < b
b_ne_one : b ≠ 1
hx : x ≠ 0
⊢ b ^ logb b x ∈ Ioi 0

case a
b x : ℝ
b_pos : 0 < b
b_ne_one : b ≠ 1
hx : x ≠ 0
⊢ |x| ∈ Ioi 0

case a
b x : ℝ
b_pos : 0 < b
b_ne_one : b ≠ 1
hx : x ≠ 0
⊢ log (b ^ logb b x) = log |x|
Module: Mathlib.Analysis.SpecialFunctions.Log.Base

Goal state before:
pp: case inl
b : ℕ
hr : 0 ≤ 0
⊢ ⌊logb (↑b) 0⌋ = Int.log b 0

Tactic:
logb_zero,

Goal state after:
case inl
b : ℕ
hr : 0 ≤ 0
⊢ ⌊0⌋ = Int.log b 0
Module: Mathlib.Analysis.SpecialFunctions.Log.Base

Goal state before:
pp: case inl
b : ℕ
hr : 0 ≤ 0
⊢ ⌈logb (↑b) 0⌉ = Int.clog b 0

Tactic:
logb_zero,

Goal state after:
case inl
b : ℕ
hr : 0 ≤ 0
⊢ ⌈0⌉ = Int.clog b 0
Module: Mathlib.Analysis.SpecialFunctions.MulExpNegMulSq

Goal state before:
pp: ε : ℝ
E : Type u_1
inst✝ : TopologicalSpace E
x : E
g : E →ᵇ ℝ
hε : 0 ≤ ε
⊢ -(ε * g x * g x) ≤ 0

Tactic:
Left.neg_nonpos_iff,

Goal state after:
ε : ℝ
E : Type u_1
inst✝ : TopologicalSpace E
x : E
g : E →ᵇ ℝ
hε : 0 ≤ ε
⊢ 0 ≤ ε * g x * g x
Module: Mathlib.Analysis.SpecialFunctions.Log.Base

Goal state before:
pp: b✝ b : ℝ
hb : b ≠ -1 ∧ b ≠ 0 ∧ b ≠ 1
hb₀ : 0 < b
hb₁ : 1 < b
⊢ Tendsto (fun x ↦ |logb b x|) atTop atTop

Tactic:
refine (tendsto_logb_atTop hb₁).congr' ?_

Goal state after:
b✝ b : ℝ
hb : b ≠ -1 ∧ b ≠ 0 ∧ b ≠ 1
hb₀ : 0 < b
hb₁ : 1 < b
⊢ logb b =ᶠ[atTop] fun x ↦ |logb b x|
Module: Mathlib.MeasureTheory.Integral.BoundedContinuousFunction

Goal state before:
pp: X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : MeasurableSpace X
inst✝ : OpensMeasurableSpace X
f : X →ᵇ ℝ≥0
μ : Measure X
⊢ (∫⁻ (x : X), ↑(f x) ∂μ).toReal = (∫⁻ (a : X), ENNReal.ofReal ↑(f a) ∂μ).toReal

pp: X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : MeasurableSpace X
inst✝ : OpensMeasurableSpace X
f : X →ᵇ ℝ≥0
μ : Measure X
⊢ 0 ≤ᵐ[μ] fun x ↦ ↑(f x)

Tactic:
· simp only [ENNReal.ofReal_coe_nnreal]

Goal state after:
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : MeasurableSpace X
inst✝ : OpensMeasurableSpace X
f : X →ᵇ ℝ≥0
μ : Measure X
⊢ 0 ≤ᵐ[μ] fun x ↦ ↑(f x)
Module: Mathlib.MeasureTheory.Measure.RegularityCompacts

Goal state before:
pp: α : Type u_1
inst✝⁴ : MeasurableSpace α
μ✝ : Measure α
inst✝³ : TopologicalSpace α
inst✝² : SecondCountableTopology α
inst✝¹ : IsCompletelyPseudoMetrizableSpace α
inst✝ : BorelSpace α
μ : Measure α
⊢ μ.InnerRegularWRT IsCompact fun s ↦ MeasurableSet s ∧ μ s ≠ ∞

Tactic:
intro A ⟨hA1, hA2⟩ r hr

Goal state after:
α : Type u_1
inst✝⁴ : MeasurableSpace α
μ✝ : Measure α
inst✝³ : TopologicalSpace α
inst✝² : SecondCountableTopology α
inst✝¹ : IsCompletelyPseudoMetrizableSpace α
inst✝ : BorelSpace α
μ : Measure α
A : Set α
hA1 : MeasurableSet A
hA2 : μ A ≠ ∞
r : ℝ≥0∞
hr : r < μ A
⊢ ∃ K ⊆ A, IsCompact K ∧ r < μ K
Module: Mathlib.Analysis.SpecialFunctions.Pochhammer

Goal state before:
pp: case succ
n : ℕ
ih : MonotoneOn (deriv fun x ↦ Polynomial.eval x (descPochhammer ℝ n)) (Set.Ioi (↑n - 1))
⊢ MonotoneOn (deriv fun x ↦ Polynomial.eval x (descPochhammer ℝ (n + 1))) (Set.Ioi (↑(n + 1) - 1))

Tactic:
intro a ha b hb hab

Goal state after:
case succ
n : ℕ
ih : MonotoneOn (deriv fun x ↦ Polynomial.eval x (descPochhammer ℝ n)) (Set.Ioi (↑n - 1))
a : ℝ
ha : a ∈ Set.Ioi (↑(n + 1) - 1)
b : ℝ
hb : b ∈ Set.Ioi (↑(n + 1) - 1)
hab : a ≤ b
⊢ deriv (fun x ↦ Polynomial.eval x (descPochhammer ℝ (n + 1))) a ≤
    deriv (fun x ↦ Polynomial.eval x (descPochhammer ℝ (n + 1))) b
Module: Mathlib.Analysis.SpecialFunctions.Pochhammer

Goal state before:
pp: case inr
n : ℕ
h✝ : n > 0
⊢ MonotoneOn (deriv fun x ↦ Polynomial.eval x (descPochhammer ℝ n)) (Set.Ioi (↑n - 1))

Tactic:
exact monotoneOn_deriv_descPochhammer_eval n

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

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
f : α → ℝ
f_nn : 0 ≤ᵐ[μ] f
f_mble : AEMeasurable f μ
p : ℝ
p_pos : 0 < p
t : ℝ
ht : μ {a | t ≤ f a} = μ {a | t < f a}
⊢ μ {a | t ≤ f a} * ENNReal.ofReal (t ^ (p - 1)) = μ {a | t < f a} * ENNReal.ofReal (t ^ (p - 1))

Tactic:
rw [ht]

Goal state after:
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
hy₀ : y ≠ 0
⊢ ‖y‖ ≤ dist y ((1 - ε / 4) • x) + ‖(1 - ε / 4) • x‖

Tactic:
simpa using dist_triangle y ((1 - ε / 4) • x) 0

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

Goal state before:
pp: L : PeriodPair
f : ↥L.lattice → ℂ → ℂ
u : ℝ → ↥L.lattice → ℝ
hu : ∀ r > 0, Summable (u r)
hf : ∀ r > 0, ∀ᶠ (R : ℝ) in atTop, ∀ (x : ℂ), ‖x‖ < r → ∀ (l : ↥L.lattice), ‖↑l‖ = R → ‖f l x‖ ≤ u r l
x : ℂ
r : ℝ
hr : 0 < r
hr' : 𝓝 x ≤ 𝓟 (Metric.ball 0 r)
R : ℝ
hR : ∀ (b : ℝ), R ≤ b → ∀ (x : ℂ), ‖x‖ < r → ∀ (l : ↥L.lattice), ‖↑l‖ = b → ‖f l x‖ ≤ u r l
l : ↥L.lattice
hl : l ∈ {x | (fun n ↦ ∀ x ∈ Metric.ball 0 r, ‖f n x‖ ≤ u r n) x}ᶜ
s : ℂ
hs : ‖s‖ < r
hs' : u r l < ‖f l s‖
⊢ l ∈ Metric.closedBall 0 R

Tactic:
simp only [Metric.mem_closedBall, dist_zero_right]

Goal state after:
L : PeriodPair
f : ↥L.lattice → ℂ → ℂ
u : ℝ → ↥L.lattice → ℝ
hu : ∀ r > 0, Summable (u r)
hf : ∀ r > 0, ∀ᶠ (R : ℝ) in atTop, ∀ (x : ℂ), ‖x‖ < r → ∀ (l : ↥L.lattice), ‖↑l‖ = R → ‖f l x‖ ≤ u r l
x : ℂ
r : ℝ
hr : 0 < r
hr' : 𝓝 x ≤ 𝓟 (Metric.ball 0 r)
R : ℝ
hR : ∀ (b : ℝ), R ≤ b → ∀ (x : ℂ), ‖x‖ < r → ∀ (l : ↥L.lattice), ‖↑l‖ = b → ‖f l x‖ ≤ u r l
l : ↥L.lattice
hl : l ∈ {x | (fun n ↦ ∀ x ∈ Metric.ball 0 r, ‖f n x‖ ≤ u r n) x}ᶜ
s : ℂ
hs : ‖s‖ < r
hs' : u r l < ‖f l s‖
⊢ ‖l‖ ≤ R
Module: Mathlib.Analysis.SpecialFunctions.Pow.NthRootLemmas

Goal state before:
pp: case inl
n a b : ℕ
hn : n ≠ 0
hle : a ≤ n.nthRoot b
⊢ a ≤ n.nthRoot b ↔ a ^ n ≤ b

Tactic:
| inl hle =>

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

Goal state before:
pp: a b : Multiset ℂ
⊢ Tendsto
    (fun n ↦ (Multiset.map (fun x ↦ x / ↑n + 1) a).prod / ((Multiset.map (fun x ↦ x / ↑n + 1) b).prod * (1 + (↑n)⁻¹)))
    atTop (𝓝 1)

Tactic:
by
  have h : Tendsto (fun n : ℕ ↦ (n : ℂ)⁻¹) atTop (𝓝 0) := tendsto_inv_atTop_nhds_zero_nat
  have := (tendsto_multiset_prod_div_add_one a).div
    ((tendsto_multiset_prod_div_add_one b).mul <| h.const_add 1) (by simp)
  simp only [add_zero, mul_one, ne_eq, one_ne_zero, not_false_eq_true, div_self] at this
  apply this.congr
  simp

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

Goal state before:
pp: ⊢ regularizedHGFunSeries 0 0 = NormedSpace.expSeries ℂ ℂ

Tactic:
by
  ext n
  simp [regularizedHGFunCoeff, NormedSpace.expSeries]

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

Goal state before:
pp: ⊢ regularizedHGFun 0 0 = NormedSpace.exp

Tactic:
NormedSpace.exp_eq_expSeries_sum (𝕂 := ℂ)

Goal state after:
⊢ regularizedHGFun 0 0 = (NormedSpace.expSeries ℂ ℂ).sum
Module: Mathlib.Analysis.SpecialFunctions.RegularizedHypergeometric

Goal state before:
pp: a b c z : ℂ
hc : ∀ (k : ℕ), c ≠ -↑k
⊢ ₂F₁ a b c z / Gamma c = a.regularizedGaussHGFun b c z

Tactic:
rw [regularizedGaussHGFun, ordinaryHypergeometric, div_eq_inv_mul, ← smul_eq_mul,
    FormalMultilinearSeries.const_smul_sum_apply]

Goal state after:
a b c z : ℂ
hc : ∀ (k : ℕ), c ≠ -↑k
⊢ ((Gamma c)⁻¹ • ordinaryHypergeometricSeries ℂ a b c).sum z = (a.regularizedGaussHGFunSeries b c).sum z
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: case e'_5
L : PeriodPair
l : ↥L.lattice
z : ℂ
⊢ -2 / (z - ↑l) ^ 3 = if ↑l = L.ω₁ / 2 then 0 else -2 / (z - ↑l) ^ 3

Tactic:
rw [if_neg, neg_div]

Goal state after:
case e'_5.hnc
L : PeriodPair
l : ↥L.lattice
z : ℂ
⊢ ¬↑l = L.ω₁ / 2
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

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

Tactic:
← L.derivWeierstrassP_add_coe _ l,

Goal state after:
L : PeriodPair
z : ℂ
l : ↥L.lattice
⊢ ℘'[L] (z - ↑l + ↑l) = ℘'[L] z
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: L : PeriodPair
l₀ x : ℂ
i : ℕ
hl₀ : l₀ ∈ L.lattice
⊢ (↑i + 2) * (L.sumInvPow x (i + 3) - ∑' (l : ↥L.lattice), if l = ⟨l₀, hl₀⟩ then (l₀ - x) ^ (-↑(i + 3)) else 0) =
    ∑' (l : ↥L.lattice),
      if ↑l = l₀ then 0 else (↑(i + 1) + 1) * (↑l - x) ^ (-↑(i + 1 + 2)) - Nat.casesOn (i + 1) (↑l ^ (-2)) 0

Tactic:
sumInvPow,

Goal state after:
L : PeriodPair
l₀ x : ℂ
i : ℕ
hl₀ : l₀ ∈ L.lattice
⊢ (↑i + 2) *
      (∑' (l : ↥L.lattice), ((↑l - x) ^ (i + 3))⁻¹ -
        ∑' (l : ↥L.lattice), if l = ⟨l₀, hl₀⟩ then (l₀ - x) ^ (-↑(i + 3)) else 0) =
    ∑' (l : ↥L.lattice),
      if ↑l = l₀ then 0 else (↑(i + 1) + 1) * (↑l - x) ^ (-↑(i + 1 + 2)) - Nat.casesOn (i + 1) (↑l ^ (-2)) 0