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

Goal state before:
pp: case hbc
K : Type u_1
inst✝ : NormedDivisionRing K
p : K[X]
hp : p ≠ 0
a : K
h : ‖p.leadingCoeff‖₊ * ‖a‖₊ ^ p.natDegree = ‖∑ i ∈ range p.natDegree, p.coeff i * a ^ i‖₊
this : ‖a‖₊ ^ p.natDegree ≤ (p.cauchyBound - 1) * ((‖a‖₊ ^ p.natDegree - 1) / (‖a‖₊ - 1))
ha✝ : ‖a‖₊ ≠ 1
ha : 1 < ‖a‖₊
⊢ ‖a‖₊ ^ p.natDegree - 1 < ‖a‖₊ ^ p.natDegree

Tactic:
simp [zero_lt_one.trans ha]

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

Goal state before:
pp: p : ℂ[X]
this :
  ∑ x ∈ p.support, ‖p.coeff x‖ ^ 2 =
    ∫ (t : AddCircle (2 * π)), ‖↑(ContinuousMap.toAEEqFun haarAddCircle (toAddCircle p)) t‖ ^ 2 ∂haarAddCircle
t : AddCircle (2 * π)
ht : ↑(ContinuousMap.toAEEqFun haarAddCircle (toAddCircle p)) t = (toAddCircle p) t
⊢ ‖(toAddCircle p) t‖ ^ 2 = ‖↑(ContinuousMap.toAEEqFun haarAddCircle (toAddCircle p)) t‖ ^ 2

Tactic:
rw [← ht]

Goal state after:
Module: Mathlib.RingTheory.PowerSeries.GaussNorm

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
v : R → ℝ
c : ℝ
f : R⟦X⟧
h : HasGaussNorm v c f
⊢ MvPowerSeries.HasGaussNorm v (fun x ↦ c) f

Tactic:
suffices (Set.range (fun (t : ℕ) ↦ (v (coeff t f) * c ^ t))) =
      Set.range fun t ↦ v ((MvPowerSeries.coeff t) f) * t.prod fun _ x2 ↦ c ^ x2 by
    simpa only [MvPowerSeries.HasGaussNorm, ← this]
  refine Set.ext (fun _ ↦ ?_)
  simp only [Set.mem_range, Finsupp.prod_pow, Finset.univ_unique, PUnit.default_eq_unit,
    Finset.prod_singleton]
  constructor
  · intro h
    obtain ⟨y, hy⟩ := h
    use (Finsupp.uniqueEquiv ()).symm y
    simpa [coeff] using hy
  · intro h
    obtain ⟨y, hy⟩ := h
    use Finsupp.uniqueEquiv () y
    simpa [coeff, show (Finsupp.single () (y PUnit.unit)) = y by grind]

Goal state after:
Module: Mathlib.RingTheory.PowerSeries.GaussNorm

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
v : R → ℝ
c : ℝ
f : R⟦X⟧
h : HasGaussNorm v c f
⊢ MvPowerSeries.HasGaussNorm v (fun x ↦ c) f

Tactic:
by
  suffices (Set.range (fun (t : ℕ) ↦ (v (coeff t f) * c ^ t))) =
      Set.range fun t ↦ v ((MvPowerSeries.coeff t) f) * t.prod fun _ x2 ↦ c ^ x2 by
    simpa only [MvPowerSeries.HasGaussNorm, ← this]
  refine Set.ext (fun _ ↦ ?_)
  simp only [Set.mem_range, Finsupp.prod_pow, Finset.univ_unique, PUnit.default_eq_unit,
    Finset.prod_singleton]
  constructor
  · intro h
    obtain ⟨y, hy⟩ := h
    use (Finsupp.uniqueEquiv ()).symm y
    simpa [coeff] using hy
  · intro h
    obtain ⟨y, hy⟩ := h
    use Finsupp.uniqueEquiv () y
    simpa [coeff, show (Finsupp.single () (y PUnit.unit)) = y by grind]

Goal state after:
Module: Mathlib.RingTheory.Polynomial.GaussNorm

Goal state before:
pp: R : Type u_1
F : Type u_2
inst✝³ : Semiring R
inst✝² : FunLike F R ℝ
v : F
c : ℝ
p : R[X]
inst✝¹ : ZeroHomClass F R ℝ
inst✝ : NonnegHomClass F R ℝ
h_eq_zero : ∀ (x : R), v x = 0 → x = 0
hc : 0 < c
⊢ p = 0 ↔ ↑p = 0

Tactic:
exact Iff.symm coe_eq_zero_iff

Goal state after:
Module: Mathlib.RingTheory.Polynomial.GaussNorm

Goal state before:
pp: R : Type u_1
F : Type u_2
inst✝³ : Semiring R
inst✝² : FunLike F R ℝ
v : F
c : ℝ
inst✝¹ : ZeroHomClass F R ℝ
inst✝ : NonnegHomClass F R ℝ
p : R[X]
hc : 0 ≤ c
i : ℕ
hi : gaussNorm v c p = v (p.coeff i) * c ^ i
⊢ {i | gaussNorm v c p = v (p.coeff i) * c ^ i}.Nonempty

Tactic:
exact ⟨i, Set.mem_ofPred.mpr hi⟩

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

Goal state before:
pp: P : ℝ[X]
x : ℝ
hlc : 0 ≤ P.leadingCoeff
hroots : P.leadingCoeff ≤ 0
⊢ ∃ y, P.IsRoot y ∧ x ≤ y

Tactic:
exact ⟨x, by simp [leadingCoeff_eq_zero.mp <| eq_of_le_of_ge hroots hlc], le_refl x⟩

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

Goal state before:
pp: n : ℕ
a : ℝ
h : (↑0 / ↑1).sqrtTwoAddSeries n ≤ 2 - (a / 2 ^ (n + 1)) ^ 2
⊢ (a / 2 ^ (n + 1)) ^ 2 ≤ 2 - sqrtTwoAddSeries 0 n

Tactic:
le_sub_comm,

Goal state after:
n : ℕ
a : ℝ
h : (↑0 / ↑1).sqrtTwoAddSeries n ≤ 2 - (a / 2 ^ (n + 1)) ^ 2
⊢ sqrtTwoAddSeries 0 n ≤ 2 - (a / 2 ^ (n + 1)) ^ 2
Module: Mathlib.Analysis.Polynomial.MahlerMeasure

Goal state before:
pp: p : ℂ[X]
i : ℕ
hi : p.supNorm = ‖p.coeff i‖
⊢ ↑(p.natDegree.choose i) ≤ ↑(p.natDegree.choose (p.natDegree / 2))

Tactic:
exact_mod_cast Nat.choose_le_middle i p.natDegree

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

Goal state before:
pp: n : ℕ
m : ℤ
hnpos : 0 < n
N : ℤ
D : ℕ
P : D ≠ 0
C : N.natAbs.Coprime D
hxr : m * ↑D ^ n = N ^ n
hv : ¬∃ y, ↑{ num := N, den := D, den_nz := P, reduced := C } = ↑y
c1 : ↑↑D ≠ 0
c2 : ↑↑D ^ n ≠ 0
hdivn : D ∣ N.natAbs
⊢ False

Tactic:
obtain rfl : D = 1 := by rw [← Nat.gcd_eq_right hdivn, C.gcd_eq_one]

Goal state after:
n : ℕ
m : ℤ
hnpos : 0 < n
N : ℤ
P : 1 ≠ 0
C : N.natAbs.Coprime 1
hxr : m * ↑1 ^ n = N ^ n
hv : ¬∃ y, ↑{ num := N, den_nz := P, reduced := C } = ↑y
c1 : ↑↑1 ≠ 0
c2 : ↑↑1 ^ n ≠ 0
hdivn : 1 ∣ N.natAbs
⊢ False
Module: Mathlib.Analysis.Real.Hyperreal

Goal state before:
pp: f : ℕ → ℝ
hf : Tendsto f atTop (𝓝 0)
r✝ : ℝ
hr : 0 < r✝
hg : Tendsto (fun x ↦ -f x) atTop (𝓝 (-0))
⊢ -ofSeq f < ↑r✝

Tactic:
by rw [neg_zero] at hg; exact lt_of_tendsto_zero_of_pos hg hr

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

Goal state before:
pp: case inl
x : ℝ
m : ℤ
hm : m ≠ 0
p : ℕ
hp : Fact (Nat.Prime p)
hxr : m = 1
hv : multiplicity (↑p) m % 0 ≠ 0
⊢ Irrational x

Tactic:
simp [hxr, multiplicity_of_one_right (mt isUnit_iff_dvd_one.1
      (mt Int.natCast_dvd_natCast.1 hp.1.not_dvd_one))] at hv

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

Goal state before:
pp: x y : ℝ*
hx : ¬x.Infinitesimal
hy : y.Infinite
⊢ (y * x).Infinite

Tactic:
exact infinite_mul_of_infinite_not_infinitesimal hy hx

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

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

Tactic:
apply inv_eq_of_mul_eq_one_right
  rw [← pow_two_sub_pow_two, sq_sqrt (sub_nonneg_of_le (one_le_pow₀ hx)), sub_sub_cancel]

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

Goal state before:
pp: case convert_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
⊢ (0 * v₁ 1 - u₁ (-1) * v₁ (-1) - ∫ (x : ℝ) in -1..1, u₁' x * v₁ x) * θ =
    -(2 * 2 * ((↑n + 1) * (0 ^ n * cos θ))) + 2 * (↑n + 1) * (2 * ↑n + 1) * I n θ - 4 * (↑n + 1) * ↑n * I (n - 1) θ

Tactic:
hu₁_eval_neg_one,

Goal state after:
case convert_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
⊢ (0 * v₁ 1 - 0 * v₁ (-1) - ∫ (x : ℝ) in -1..1, u₁' x * v₁ x) * θ =
    -(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.SpecialFunctions.CompareExp

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

Tactic:
simpa using hl.isLittleO_cpow_mul_exp hb 0 a

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

Goal state before:
pp: case succ
θ : ℝ
f : ℝ → ℝ := fun x ↦ 1 - x ^ 2
v₁ : ℝ → ℝ := fun x ↦ sin (x * θ)
v₁' : ℝ → ℝ := fun x ↦ cos (x * θ) * θ
v₂ : ℝ → ℝ := fun x ↦ cos (x * θ)
v₂' : ℝ → ℝ := fun x ↦ -sin (x * θ) * θ
hfd : Continuous f
hv₁d : Continuous v₁'
hv₂d : Continuous v₂'
hf : ∀ (x : ℝ), HasDerivAt f (-2 * x) x
hv₁ : ∀ (x : ℝ), HasDerivAt v₁ (v₁' x) x
hv₂ : ∀ (x : ℝ), HasDerivAt v₂ (v₂' x) x
x : ℝ
n : ℕ
u₁ : ℝ → ℝ := fun x ↦ f x ^ (n + 1 + 1)
u₁' : ℝ → ℝ := fun x ↦ -(2 * (↑(n + 1) + 1) * x * f x ^ (n + 1))
u₂ : ℝ → ℝ := fun x ↦ x * f x ^ (n + 1)
u₂' : ℝ → ℝ := fun x ↦ f x ^ (n + 1) - 2 * ↑(n + 1) * x ^ 2 * f x ^ (n + 1 - 1)
hu₁d : Continuous u₁'
hu₂d : Continuous u₂'
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 + 1) * cos θ)
hu₁ : ∀ (x : ℝ), HasDerivAt u₁ (u₁' x) x
hu₂ : ∀ (x : ℝ), HasDerivAt u₂ (u₂' x) x
⊢ u₂' x = (2 * ↑(n + 1) + 1) * f x ^ (n + 1) - 2 * ↑(n + 1) * f x ^ (n + 1 - 1)

Tactic:
ring!

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

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

Tactic:
simp_all only [mem_Iio, mem_Ioi, sub_pos]

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

Goal state before:
pp: case convert_2.convert_2.e_a
θ : ℝ
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₂
⊢ 2 * (↑n + 1) * ((2 * ↑n + 1) * ∫ (x : ℝ) in -1..1, f x ^ n * v₂ x) -
      2 * (↑n + 1) * (2 * ↑n * ∫ (x : ℝ) in -1..1, f x ^ (n - 1) * v₂ x) =
    2 * (↑n + 1) * (2 * ↑n + 1) * I n θ - 4 * (↑n + 1) * ↑n * I (n - 1) θ

Tactic:
ring!

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

Goal state before:
pp: ⊢ TendstoLocallyUniformlyOn (fun p x ↦ p⁻¹ * (x ^ p - 1)) log (𝓝[>] 0) (Ioi 0)

Tactic:
refine (tendstoLocallyUniformlyOn_iff_forall_isCompact isOpen_Ioi).mpr ?_

Goal state after:
⊢ ∀ K ⊆ Ioi 0, IsCompact K → TendstoUniformlyOn (fun p x ↦ p⁻¹ * (x ^ p - 1)) log (𝓝[>] 0) K
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
hxt : 0 ≤ x * t
hx_zero : ¬x = 0
⊢ (x * t) ^ (p - 1) * x / (x * t + x) = t ^ (p - 1) * 1 / (t + 1) * x ^ (p - 1)

Tactic:
calc _ = x ^ (p - 1) * (t ^ (p - 1) * (x / (x * t + x))) := by
              rw [← mul_assoc, mul_div_assoc, Real.mul_rpow hx ht]
      _ = x ^ (p - 1) * (t ^ (p - 1) * 1 / (t + 1)) := by
              have : x * t + x = x * (t + 1) := by ring
              rw [mul_div_assoc, this, div_mul_eq_div_mul_one_div, div_self hx_zero, one_mul]
      _ = t ^ (p - 1) * 1 / (t + 1) * x ^ (p - 1) := by rw [mul_comm]

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

Goal state before:
pp: p t : ℝ
hp : p ∈ Ioo 0 1
ht : 0 ≤ t
x : ℝ
hx : x ∈ Ici 0
y : ℝ
hy : y ∈ Ici 0
hxy : x ≤ y
⊢ p.rpowIntegrand₀₁ t x ≤ p.rpowIntegrand₀₁ t y

Tactic:
by_cases h : x = 0

Goal state after:
case pos
p t : ℝ
hp : p ∈ Ioo 0 1
ht : 0 ≤ t
x : ℝ
hx : x ∈ Ici 0
y : ℝ
hy : y ∈ Ici 0
hxy : x ≤ y
h : x = 0
⊢ p.rpowIntegrand₀₁ t x ≤ p.rpowIntegrand₀₁ t y

case neg
p t : ℝ
hp : p ∈ Ioo 0 1
ht : 0 ≤ t
x : ℝ
hx : x ∈ Ici 0
y : ℝ
hy : y ∈ Ici 0
hxy : x ≤ y
h : ¬x = 0
⊢ p.rpowIntegrand₀₁ t x ≤ p.rpowIntegrand₀₁ t y
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Deligne

Goal state before:
pp: h : Tendsto (fun z ↦ z / 2 * Gamma (z / 2)) (𝓝[≠] 0) (𝓝 1)
⊢ Tendsto (fun s ↦ 2 * ↑π ^ (-s / 2)) (𝓝[≠] 0) (𝓝 2)

Tactic:
rw [(by simp : 𝓝 2 = 𝓝 (2 * (π : ℂ) ^ (-(0 : ℂ) / 2)))]

Goal state after:
h : Tendsto (fun z ↦ z / 2 * Gamma (z / 2)) (𝓝[≠] 0) (𝓝 1)
⊢ Tendsto (fun s ↦ 2 * ↑π ^ (-s / 2)) (𝓝[≠] 0) (𝓝 (2 * ↑π ^ (-0 / 2)))
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation

Goal state before:
pp: p t : ℝ
ht : 0 < t
x : ℝ
hx : x ∈ Ici 0
⊢ t ^ p * (t⁻¹ - t⁻¹ * (1 + x * t⁻¹)⁻¹) = t ^ (p - 1) * (1 - (1 + x * t⁻¹)⁻¹)

Tactic:
by
          rw [Real.rpow_sub_one ht.ne']
          ring

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

Goal state before:
pp: s : ℂ
⊢ ↑π ^ ((s - 1) / 2) * ↑π ^ ((-1 - s) / 2) * ↑π ^ 1 / sin (↑π / 2 - ↑π * s / 2) = (cos (↑π * s / 2))⁻¹

Tactic:
by
    simp_rw [← cpow_add _ _ (ofReal_ne_zero.mpr pi_ne_zero),
      Complex.sin_pi_div_two_sub]
    ring_nf
    rw [cpow_zero, one_mul]

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

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

Tactic:
(by ring : 2 - 1 = (1 : ℂ)),

Goal state after:
case pos
s : ℂ
hs : ∀ (n : ℕ), s ≠ -↑n
h : s = 1
⊢ (Gammaℝ 1)⁻¹ = Gammaℂ 1 * sin (↑π * 1 / 2) * (1 + 1).Gammaℝ⁻¹
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
⊢ a.re ≤ 0

Tactic:
ha,

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
⊢ re 0 ≤ 0
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 : ℕ
hb : 1 < b
r : R
hr : r ≤ 0
⊢ r < ↑b ^ 1

Tactic:
zpow_one

Goal state after:
case inl
R : Type u_1
inst✝³ : Semifield R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorSemiring R
b : ℕ
hb : 1 < b
r : R
hr : r ≤ 0
⊢ r < ↑b
Module: Mathlib.Data.Int.Log

Goal state before:
pp: case inr.inr
R : Type u_1
inst✝³ : Semifield R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorSemiring R
b : ℕ
hb : 1 < b
r : R
hr : 0 < r
hr1 : r < 1
hcri : 1 < r⁻¹
this : 1 ≤ Nat.clog b ⌈r⁻¹⌉₊
⊢ r < ↑b ^ (-(↑(Nat.clog b ⌈r⁻¹⌉₊) - ↑1))

Tactic:
← Int.ofNat_sub this,

Goal state after:
case inr.inr
R : Type u_1
inst✝³ : Semifield R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorSemiring R
b : ℕ
hb : 1 < b
r : R
hr : 0 < r
hr1 : r < 1
hcri : 1 < r⁻¹
this : 1 ≤ Nat.clog b ⌈r⁻¹⌉₊
⊢ r < ↑b ^ (-↑(Nat.clog b ⌈r⁻¹⌉₊ - 1))
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation

Goal state before:
pp: A : Type u_1
inst✝⁹ : NonUnitalNormedRing A
inst✝⁸ : StarRing A
inst✝⁷ : NormedSpace ℝ A
inst✝⁶ : SMulCommClass ℝ A A
inst✝⁵ : IsScalarTower ℝ A A
inst✝⁴ : PartialOrder A
inst✝³ : StarOrderedRing A
inst✝² : NonnegSpectrumClass ℝ A
inst✝¹ : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝ : CompleteSpace A
p : ℝ≥0
hp : p ∈ Ioo 1 2
μ : Measure ℝ
hμ :
  ∀ x ∈ Ici 0,
    IntegrableOn (fun t ↦ (↑p).rpowIntegrand₁₂ t x) (Ioi 0) μ ∧ x ^ ↑p = ∫ (t : ℝ) in Ioi 0, (↑p).rpowIntegrand₁₂ t x ∂μ
a : A
ha : 0 ≤ a
hpcoe : ↑p ∈ Ioo 1 2
f : ℝ → ℝ → ℝ := fun t ↦ (↑p).rpowIntegrand₁₂ t
maxr : ℝ := sSup (quasispectrum ℝ a)
maxr_nonneg : 0 ≤ maxr
bound : ℝ → ℝ := fun t ↦ ‖f t maxr‖
hf : ContinuousOn (Function.uncurry f) (Ioi 0 ×ˢ quasispectrum ℝ a)
hbound : ∀ᵐ (t : ℝ) ∂μ.restrict (Ioi 0), ∀ z ∈ quasispectrum ℝ a, ‖f t z‖ ≤ bound t
hbound_finite_integral : HasFiniteIntegral bound (μ.restrict (Ioi 0))
hmapzero : ∀ᵐ (x : ℝ) ∂μ.restrict (Ioi 0), (↑p).rpowIntegrand₁₂ x 0 = 0
⊢ cfcₙ (fun x ↦ x.nnrpow p) a = cfcₙ (fun r ↦ ∫ (t : ℝ) in Ioi 0, (↑p).rpowIntegrand₁₂ t r ∂μ) a

Tactic:
by
        rw [cfcₙ_nnreal_eq_real ..]
        refine cfcₙ_congr fun r hr => ?_
        have hr' : 0 ≤ r := by grind
        simp only [sup_of_le_left hr', NNReal.nnrpow_def, NNReal.coe_rpow, coe_toNNReal']
        exact (hμ r hr').2

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

Goal state before:
pp: b x y : ℝ
hb : 1 < b
h : 0 < x
h₁ : 0 < y
⊢ logb b x ≤ logb b y ↔ x ≤ y

Tactic:
rw [logb, logb, div_le_div_iff_of_pos_right (log_pos hb), log_le_log_iff h h₁]

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

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

Tactic:
by
  rw [← @logb_one b, logb_lt_logb_iff_of_base_lt_one b_pos b_lt_one h zero_lt_one]

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

Goal state before:
pp: case pos.a
b : ℕ
r : ℝ
hr✝ : 0 ≤ r
hr : 0 < r
hb : 1 < b
hb1' : 1 < ↑b
⊢ ⌈logb (↑b) r⌉ ≤ Int.clog b r

pp: case a
b : ℕ
r : ℝ
hr✝ : 0 ≤ r
hr : 0 < r
hb : 1 < b
hb1' : 1 < ↑b
⊢ Int.clog b r ≤ ⌈logb (↑b) r⌉

Tactic:
· rw [Int.ceil_le, logb_le_iff_le_rpow hb1' hr, rpow_intCast]
      exact Int.self_le_zpow_clog hb r

Goal state after:
case a
b : ℕ
r : ℝ
hr✝ : 0 ≤ r
hr : 0 < r
hb : 1 < b
hb1' : 1 < ↑b
⊢ Int.clog b r ≤ ⌈logb (↑b) r⌉
Module: Mathlib.MeasureTheory.Integral.BoundedContinuousFunction

Goal state before:
pp: X : Type u_1
inst✝³ : TopologicalSpace X
inst✝² : MeasurableSpace X
μ : Measure X
inst✝¹ : IsFiniteMeasure μ
inst✝ : OpensMeasurableSpace X
f : X →ᵇ ℝ
⊢ ∫ (a : X), (NNReal.toReal ∘ ⇑f.nnrealPart) a ∂μ - ∫ (a : X), (NNReal.toReal ∘ ⇑(-f).nnrealPart) a ∂μ =
    ∫ (x : X), ↑(f.nnrealPart x) ∂μ - ∫ (x : X), ↑((-f).nnrealPart x) ∂μ

Tactic:
simp only [Function.comp_apply]

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

Goal state before:
pp: b c : ℝ
hb : b ≠ -1 ∧ b ≠ 0 ∧ b ≠ 1
⊢ (fun x ↦ c) =o[atTop] logb b

Tactic:
rw [Asymptotics.isLittleO_const_left, or_iff_not_imp_left]

Goal state after:
b c : ℝ
hb : b ≠ -1 ∧ b ≠ 0 ∧ b ≠ 1
⊢ ¬c = 0 → Tendsto (Norm.norm ∘ logb b) atTop atTop
Module: Mathlib.MeasureTheory.Measure.RegularityCompacts

Goal state before:
pp: case mp
α : Type u_1
inst✝² : MeasurableSpace α
μ : Measure α
inst✝¹ : TopologicalSpace α
inst✝ : R1Space α
h : μ.InnerRegularWRT (fun s ↦ IsCompact s ∧ IsClosed s) IsClosed
A : Set α
hA : IsClosed A
r : ℝ≥0∞
hr : r < μ A
K : Set α
hK1 : K ⊆ A
hK4 : r < μ K
hK2 : IsCompact K
right✝ : IsClosed K
⊢ (IsCompact ∘ closure) K

Tactic:
simp only [Function.comp_apply]

Goal state after:
case mp
α : Type u_1
inst✝² : MeasurableSpace α
μ : Measure α
inst✝¹ : TopologicalSpace α
inst✝ : R1Space α
h : μ.InnerRegularWRT (fun s ↦ IsCompact s ∧ IsClosed s) IsClosed
A : Set α
hA : IsClosed A
r : ℝ≥0∞
hr : r < μ A
K : Set α
hK1 : K ⊆ A
hK4 : r < μ K
hK2 : IsCompact K
right✝ : IsClosed K
⊢ IsCompact (closure K)
Module: Mathlib.Analysis.SpecialFunctions.MulExpNegMulSqIntegral

Goal state before:
pp: case h_bound
E : Type u_1
inst✝³ : TopologicalSpace E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
P : Measure E
inst✝ : IsFiniteMeasure P
g : E →ᵇ ℝ
u : ℕ → ℝ
hu : Tendsto u atTop (𝓝[>] 0)
N : ℕ
hupos : ∀ (b : ℕ), N ≤ b → u b ∈ Set.Ioi 0
⊢ ∃ C, ∀ᶠ (n : ℕ) in atTop, ∀ᵐ (ω : E) ∂P, ‖(u n).mulExpNegMulSq (g ω)‖ ≤ C

Tactic:
use norm g

Goal state after:
case h
E : Type u_1
inst✝³ : TopologicalSpace E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
P : Measure E
inst✝ : IsFiniteMeasure P
g : E →ᵇ ℝ
u : ℕ → ℝ
hu : Tendsto u atTop (𝓝[>] 0)
N : ℕ
hupos : ∀ (b : ℕ), N ≤ b → u b ∈ Set.Ioi 0
⊢ ∀ᶠ (n : ℕ) in atTop, ∀ᵐ (ω : E) ∂P, ‖(u n).mulExpNegMulSq (g ω)‖ ≤ ‖g‖
Module: Mathlib.Analysis.SpecialFunctions.MulExpNegMulSqIntegral

Goal state before:
pp: case h_bound
E : Type u_1
inst✝³ : TopologicalSpace E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
P : Measure E
inst✝ : IsFiniteMeasure P
ε : ℝ
g : E →ᵇ ℝ
hε : 0 < ε
N : ℕ
hgN : ε * (‖g‖ * ‖g‖) < ↑N
⊢ ∃ C, ∀ᶠ (n : ℕ) in atTop, ∀ᵐ (ω : E) ∂P, ‖(g * (1 + (↑n)⁻¹ • -(ε • g * g)) ^ n) ω‖ ≤ C

Tactic:
use norm g

Goal state after:
case h
E : Type u_1
inst✝³ : TopologicalSpace E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
P : Measure E
inst✝ : IsFiniteMeasure P
ε : ℝ
g : E →ᵇ ℝ
hε : 0 < ε
N : ℕ
hgN : ε * (‖g‖ * ‖g‖) < ↑N
⊢ ∀ᶠ (n : ℕ) in atTop, ∀ᵐ (ω : E) ∂P, ‖(g * (1 + (↑n)⁻¹ • -(ε • g * g)) ^ n) ω‖ ≤ ‖g‖
Module: Mathlib.Analysis.SpecialFunctions.MulExpNegMulSqIntegral

Goal state before:
pp: case h
E : Type u_1
inst✝³ : TopologicalSpace E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
P : Measure E
inst✝ : IsFiniteMeasure P
ε : ℝ
g : E →ᵇ ℝ
hε : 0 < ε
N : ℕ
hgN : ε * (‖g‖ * ‖g‖) < ↑N
n : ℕ
hn : N ≤ n
hnpos : 0 < ↑n
x : E
⊢ -1 ≤ 1 + -(ε * (g x * g x) / ↑n) ∧ 1 + -(ε * (g x * g x) / ↑n) ≤ 1

Tactic:
refine ⟨?_, (add_le_iff_nonpos_right 1).mpr (Left.neg_nonpos_iff.mpr
      (div_nonneg (mul_nonneg (le_of_lt hε) (mul_self_nonneg (g x))) (le_of_lt hnpos)))⟩

Goal state after:
case h
E : Type u_1
inst✝³ : TopologicalSpace E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
P : Measure E
inst✝ : IsFiniteMeasure P
ε : ℝ
g : E →ᵇ ℝ
hε : 0 < ε
N : ℕ
hgN : ε * (‖g‖ * ‖g‖) < ↑N
n : ℕ
hn : N ≤ n
hnpos : 0 < ↑n
x : E
⊢ -1 ≤ 1 + -(ε * (g x * g x) / ↑n)
Module: Mathlib.Analysis.SpecialFunctions.Pow.NthRootLemmas

Goal state before:
pp: n a b : ℕ
hb : b ≠ 0
⊢ (n + 1) * a ≤ a ^ (n + 1) / b ^ n + n * b

Tactic:
← Nat.add_mul_div_right _ _ (by positivity),

Goal state after:
n a b : ℕ
hb : b ≠ 0
⊢ (n + 1) * a ≤ (a ^ (n + 1) + n * b * b ^ n) / b ^ n
Module: Mathlib.Analysis.SpecialFunctions.RegularizedHypergeometric

Goal state before:
pp: case pos
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))

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:
· rw [regularizedHGFunCoeff_add_one hb]
    field_simp

Goal state after:
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))
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: case refine_2
L : PeriodPair
l₀ : ℂ
s : Finset ↥L.lattice
l : ℂ
hl : l ∈ (↑L.lattice \ {l₀})ᶜ
⊢ (fun x2 ↦ ∑ i ∈ s, (fun l z ↦ if ↑l = l₀ then 0 else -2 / (z - ↑l) ^ 3) i x2) l =
    (deriv ∘ fun x1 x2 ↦ ∑ i ∈ x1, (fun l z ↦ if ↑l = l₀ then 0 else 1 / (z - ↑l) ^ 2 - 1 / ↑l ^ 2) i x2) s l

Tactic:
simp only [Function.comp_apply]

Goal state after:
case refine_2
L : PeriodPair
l₀ : ℂ
s : Finset ↥L.lattice
l : ℂ
hl : l ∈ (↑L.lattice \ {l₀})ᶜ
⊢ (∑ x ∈ s, if ↑x = l₀ then 0 else -2 / (l - ↑x) ^ 3) =
    deriv (fun x2 ↦ ∑ x ∈ s, if ↑x = l₀ then 0 else 1 / (x2 - ↑x) ^ 2 - 1 / ↑x ^ 2) l
Module: Mathlib.Analysis.SpecialFunctions.Sigmoid

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

Tactic:
sigmoid_def

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

Goal state before:
pp: case e'_9
x : ℝ
⊢ x.sigmoid * (x.sigmoid * rexp (-x)) = -(rexp (-x) * -1) / (1 + rexp (-x)) ^ 2

Tactic:
sigmoid_def

Goal state after:
case e'_9
x : ℝ
⊢ (1 + rexp (-x))⁻¹ * ((1 + rexp (-x))⁻¹ * rexp (-x)) = -(rexp (-x) * -1) / (1 + rexp (-x)) ^ 2