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

Goal state before:
pp: P Q : ℤ[X]
h : Q.degree < P.degree
o : (fun x ↦ eval x Q) =o[cofinite] fun x ↦ eval x P
nr : ∀ᶠ (x : ℤ) in cofinite, ¬P.IsRoot x
key : {x | ‖eval x P‖ ≤ ‖eval x Q‖}.Finite
⊢ {x | |eval x P| ≤ |eval x Q|}.Finite

Tactic:
Int.norm_eq_abs

Goal state after:
P Q : ℤ[X]
h : Q.degree < P.degree
o : (fun x ↦ eval x Q) =o[cofinite] fun x ↦ eval x P
nr : ∀ᶠ (x : ℤ) in cofinite, ¬P.IsRoot x
key : {x | |↑(eval x P)| ≤ |↑(eval x Q)|}.Finite
⊢ {x | |eval x P| ≤ |eval x Q|}.Finite
Module: Mathlib.RingTheory.Polynomial.GaussNorm

Goal state before:
pp: case neg.a
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 ℝ
hc : 0 ≤ c
hp : ¬p = 0
n : ℕ
⊢ v (p.coeff n) * c ^ n ≤ p.support.sup' ⋯ fun i ↦ v (p.coeff i) * c ^ i

Tactic:
by_cases h : n ∈ p.support

Goal state after:
case pos
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 ℝ
hc : 0 ≤ c
hp : ¬p = 0
n : ℕ
h : n ∈ p.support
⊢ v (p.coeff n) * c ^ n ≤ p.support.sup' ⋯ fun i ↦ v (p.coeff i) * c ^ i

case neg
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 ℝ
hc : 0 ≤ c
hp : ¬p = 0
n : ℕ
h : n ∉ p.support
⊢ v (p.coeff n) * c ^ n ≤ p.support.sup' ⋯ fun i ↦ v (p.coeff i) * c ^ i
Module: Mathlib.RingTheory.Polynomial.GaussNorm

Goal state before:
pp: c✝ : ℝ
R✝ : Type u_3
inst✝¹ : Ring R✝
v✝ : AbsoluteValue R✝ ℝ
c : ℝ
R : Type u_3
inst✝ : Ring R
v : AbsoluteValue R ℝ
hna : IsNonarchimedean ⇑v
hc : 0 < c
p q : R[X]
hc0 : 0 ≤ c
i : ℕ
hi_p : gaussNorm v c p = v (p.coeff i) * c ^ i
hlt_p : ∀ j < i, v (p.coeff j) * c ^ j < gaussNorm v c p
j : ℕ
hj_q : gaussNorm v c q = v (q.coeff j) * c ^ j
hlt_q : ∀ j_1 < j, v (q.coeff j_1) * c ^ j_1 < gaussNorm v c q
hvpq : v (p.coeff i) ≠ 0 ∧ v (q.coeff j) ≠ 0
this✝ : v (p.coeff i) ≠ 0
this : v (q.coeff j) ≠ 0
⊢ v (p.coeff i) * c ^ i * (v (q.coeff j) * c ^ j) = v ((p * q).coeff (i + j)) * c ^ (i + j)

Tactic:
coeff_mul,

Goal state after:
c✝ : ℝ
R✝ : Type u_3
inst✝¹ : Ring R✝
v✝ : AbsoluteValue R✝ ℝ
c : ℝ
R : Type u_3
inst✝ : Ring R
v : AbsoluteValue R ℝ
hna : IsNonarchimedean ⇑v
hc : 0 < c
p q : R[X]
hc0 : 0 ≤ c
i : ℕ
hi_p : gaussNorm v c p = v (p.coeff i) * c ^ i
hlt_p : ∀ j < i, v (p.coeff j) * c ^ j < gaussNorm v c p
j : ℕ
hj_q : gaussNorm v c q = v (q.coeff j) * c ^ j
hlt_q : ∀ j_1 < j, v (q.coeff j_1) * c ^ j_1 < gaussNorm v c q
hvpq : v (p.coeff i) ≠ 0 ∧ v (q.coeff j) ≠ 0
this✝ : v (p.coeff i) ≠ 0
this : v (q.coeff j) ≠ 0
⊢ v (p.coeff i) * c ^ i * (v (q.coeff j) * c ^ j) =
    v (∑ x ∈ antidiagonal (i + j), p.coeff x.1 * q.coeff x.2) * c ^ (i + j)
Module: Mathlib.Analysis.Polynomial.Order

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

Tactic:
eval_comp,

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

Goal state before:
pp: c✝ : ℝ
R✝ : Type u_3
inst✝¹ : Ring R✝
v✝ : AbsoluteValue R✝ ℝ
c : ℝ
R : Type u_3
inst✝ : Ring R
v : AbsoluteValue R ℝ
hna : IsNonarchimedean ⇑v
hc : 0 < c
p q : R[X]
hc0 : 0 ≤ c
i : ℕ
hi_p : gaussNorm v c p = v (p.coeff i) * c ^ i
hlt_p : ∀ j < i, v (p.coeff j) * c ^ j < gaussNorm v c p
j : ℕ
hj_q : gaussNorm v c q = v (q.coeff j) * c ^ j
hlt_q : ∀ j_1 < j, v (q.coeff j_1) * c ^ j_1 < gaussNorm v c q
hvpq : v (p.coeff i) ≠ 0 ∧ v (q.coeff j) ≠ 0
this✝¹ : v (p.coeff i) ≠ 0
this✝ : v (q.coeff j) ≠ 0
x : ℕ
hx : x ∈ range (i + j).succ
hneq : x ≠ i
this : x + (i + j - x) = i + j
h✝ : x < i
⊢ v (p.coeff x) * c ^ x * gaussNorm v c q = v (p.coeff x) * c ^ x * (v (q.coeff j) * c ^ j)

Tactic:
by
        rw [hj_q]

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

Goal state before:
pp: z : ℂ
⊢ (C z).mahlerMeasure = ‖z‖

Tactic:
simp only [mahlerMeasure, ne_eq, map_eq_zero, logMahlerMeasure_const, ite_not]

Goal state after:
z : ℂ
⊢ (if z = 0 then 0 else rexp (log ‖z‖)) = ‖z‖
Module: Mathlib.RingTheory.MvPowerSeries.GaussNorm

Goal state before:
pp: case inl
α : Type u_3
S : Type u_4
inst✝¹ : LinearOrder S
inst✝ : AddCommGroup α
f : α → S
na : IsNonarchimedean f
Neg : ∀ (a : α), f a = f (-a)
a b : α
hne : f a ≠ f b
hab : f a > f b
h : f (a + b + -b) ≤ f (a + b)
⊢ max (f a) (f b) ≤ f (a + b)

pp: case inr
α : Type u_3
S : Type u_4
inst✝¹ : LinearOrder S
inst✝ : AddCommGroup α
f : α → S
na : IsNonarchimedean f
Neg : ∀ (a : α), f a = f (-a)
a b : α
hne : f a ≠ f b
hab : f a > f b
h : f (a + b + -b) ≤ f (-b)
⊢ max (f a) (f b) ≤ f (a + b)

Tactic:
· simpa [max_eq_left (le_of_lt hab)] using h

Goal state after:
case inr
α : Type u_3
S : Type u_4
inst✝¹ : LinearOrder S
inst✝ : AddCommGroup α
f : α → S
na : IsNonarchimedean f
Neg : ∀ (a : α), f a = f (-a)
a b : α
hne : f a ≠ f b
hab : f a > f b
h : f (a + b + -b) ≤ f (-b)
⊢ max (f a) (f b) ≤ f (a + b)
Module: Mathlib.RingTheory.MvPowerSeries.GaussNorm

Goal state before:
pp: R : Type u_1
σ : Type u_2
v : R → ℝ
inst✝¹ : Ring R
inst✝ : DecidableEq σ
f g : MvPowerSeries σ R
i j : σ →₀ ℕ
vna : IsNonarchimedean v
vMulEq : ∀ (a b : R), v (a * b) = v a * v b
vNeg : ∀ (a : R), v a = v (-a)
hdom : ∀ p ∈ Finset.antidiagonal (i + j), p ≠ (i, j) → v ((coeff p.1) f * (coeff p.2) g) < v ((coeff i) f * (coeff j) g)
⊢ v ((coeff (i + j)) (f * g)) = v ((coeff i) f * (coeff j) g)

Tactic:
coeff_mul,

Goal state after:
R : Type u_1
σ : Type u_2
v : R → ℝ
inst✝¹ : Ring R
inst✝ : DecidableEq σ
f g : MvPowerSeries σ R
i j : σ →₀ ℕ
vna : IsNonarchimedean v
vMulEq : ∀ (a b : R), v (a * b) = v a * v b
vNeg : ∀ (a : R), v a = v (-a)
hdom : ∀ p ∈ Finset.antidiagonal (i + j), p ≠ (i, j) → v ((coeff p.1) f * (coeff p.2) g) < v ((coeff i) f * (coeff j) g)
⊢ v (∑ p ∈ Finset.antidiagonal (i + j), (coeff p.1) f * (coeff p.2) g) = v ((coeff i) f * (coeff j) g)
Module: Mathlib.Analysis.Real.OfDigits

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

Tactic:
tsum_geometric_of_lt_one (by positivity) (by simp [inv_lt_one_iff₀, hb])

Goal state after:
case e'_4
b : ℕ
digits : ℕ → Fin b
hb : 1 < ↑b
⊢ 1 = (↑b - 1) * (↑b)⁻¹ * (1 - (↑b)⁻¹)⁻¹
Module: Mathlib.Analysis.Polynomial.MahlerMeasure

Goal state before:
pp: n : ℕ
p : ℂ[X]
hp : ¬p = 0
hn : n ≤ p.natDegree
S : Multiset (Multiset ℂ) := powersetCard (p.natDegree - n) p.roots
x : Multiset ℂ
hx : x ∈ S
⊢ ∏ x_1 ∈ x.toFinset, ‖x_1‖ ^ count x_1 x ≤ ∏ m ∈ p.roots.toFinset, max 1 ‖m‖ ^ count m p.roots

Tactic:
mem_powersetCard

Goal state after:
n : ℕ
p : ℂ[X]
hp : ¬p = 0
hn : n ≤ p.natDegree
S : Multiset (Multiset ℂ) := powersetCard (p.natDegree - n) p.roots
x : Multiset ℂ
hx : x ≤ p.roots ∧ x.card = p.natDegree - n
⊢ ∏ x_1 ∈ x.toFinset, ‖x_1‖ ^ count x_1 x ≤ ∏ m ∈ p.roots.toFinset, max 1 ‖m‖ ^ count m p.roots
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
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

Tactic:
calc ∑ x ∈ S.toFinset, count x S * ‖x.prod‖
    _ ≤ ∑ x ∈ S.toFinset, count x S * ((p.roots).map (fun a ↦ max 1 ‖a‖)).prod := by
      gcongr with x hx
      rw [Finset.prod_multiset_map_count, Finset.prod_multiset_count, norm_prod]
      simp_rw [norm_pow]
      exact this x hx
    _ = p.natDegree.choose n * (p.roots.map (fun a ↦ 1 ⊔ ‖a‖)).prod := by
      rw [← Finset.sum_mul]
      congr
      norm_cast
      simp only [mem_powersetCard, mem_toFinset, imp_self, implies_true, sum_count_eq_card,
        card_powersetCard, S, ← Nat.choose_symm hn]
      congr
      exact splits_iff_card_roots.mp <| IsAlgClosed.splits p

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

Goal state before:
pp: case hfa
⊢ Antitone fun i ↦ (2 * ↑i + 1)⁻¹

pp: case hf0
⊢ Tendsto (fun i ↦ (2 * ↑i + 1)⁻¹) atTop (𝓝 0)

Tactic:
· exact antitone_iff_forall_lt.mpr fun _ _ _ ↦ by gcongr

Goal state after:
case hf0
⊢ Tendsto (fun i ↦ (2 * ↑i + 1)⁻¹) atTop (𝓝 0)
Module: Mathlib.Analysis.Real.Pi.Irrational

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

Tactic:
have hv₂ (x) : HasDerivAt v₂ (v₂' x) x := (hasDerivAt_mul_const θ).cos

Goal state after:
θ : ℝ
n : ℕ
f : ℝ → ℝ := fun x ↦ 1 - x ^ 2
u₁ : ℝ → ℝ := fun x ↦ f x ^ (n + 1)
u₁' : ℝ → ℝ := fun x ↦ -(2 * (↑n + 1) * x * f x ^ n)
v₁ : ℝ → ℝ := fun x ↦ sin (x * θ)
v₁' : ℝ → ℝ := fun x ↦ cos (x * θ) * θ
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, (1 - x ^ 2) ^ (n + 1) * cos (x * θ)) * θ ^ 2 =
    -(2 * 2 * ((↑n + 1) * (0 ^ n * cos θ))) + 2 * (↑n + 1) * (2 * ↑n + 1) * I n θ - 4 * (↑n + 1) * ↑n * I (n - 1) θ
Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean

Goal state before:
pp: x : ℝ≥0
⊢ x.agm 0 = 0

Tactic:
rw [agm_comm, agm_zero_left]

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

Goal state before:
pp: x y : ℝ≥0
hn : x ≠ y
⊢ x.agm y < max x y

Tactic:
by
  wlog h : x < y generalizing x y
  · simpa [agm_comm, max_comm] using this hn.symm (hn.gt_or_lt.resolve_right h)
  rw [max_eq_right h.le]
  apply (agm_lt_agmSequences_snd_of_ne hn 0).trans_le
  rw [agmSequences_zero]
  exact (le_gm_and_am_le h.le).2

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

Goal state before:
pp: q : ℕ
qLe2 : 2 ≤ q
p1 : ℝ
hp1 : p1 ∈ Icc (1 - 1 / ↑q) 1
p2 : ℝ
hp2 : p2 ∈ Icc (1 - 1 / ↑q) 1
p1le2 : p1 < p2
p : ℝ
this : 2 ≤ ↑q
qinv_lt_1 : (↑q)⁻¹ < 1
zero_lt_1_sub_p : 0 < 1 - p
hp : 1 - (↑q)⁻¹ < p ∧ p < 1
⊢ 0 < (↑q - 1) * (1 - p)

Tactic:
nlinarith

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

Goal state before:
pp: case a
q : ℕ
qLe2 : 2 ≤ q
p1 : ℝ
hp1 : p1 ∈ Icc (1 - 1 / ↑q) 1
p2 : ℝ
hp2 : p2 ∈ Icc (1 - 1 / ↑q) 1
p1le2 : p1 < p2
p : ℝ
this✝ : 2 ≤ ↑q
qinv_lt_1 : (↑q)⁻¹ < 1
zero_lt_1_sub_p : 0 < 1 - p
hp : 1 - (↑q)⁻¹ < p ∧ p < 1
qpos : 0 < ↑q
this : ↑q - 1 < p * ↑q
⊢ -1 + ↑q - ↑q * p + p < p

Tactic:
nlinarith

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

Goal state before:
pp: case left
n : ℕ
x : ℝ
hx : -1 < x ∧ x ≤ 1
⊢ -1 ≤ 1 - x ^ 2

Tactic:
nlinarith

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

Goal state before:
pp: case right
n : ℕ
x : ℝ
hx : -1 < x ∧ x ≤ 1
⊢ 1 - x ^ 2 ≤ 1

Tactic:
nlinarith

Goal state after:
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
⊢ ‖(∫ (x : ℝ) in a..b, x⁻¹ • f x) - log (b / a) • V‖ ≤ δ * |log (b / a)|

Tactic:
have hint_V : IntervalIntegrable (fun x ↦ x⁻¹ • V) volume a b := by
    apply ContinuousOn.intervalIntegrable
    exact (continuousOn_inv₀.mono (fun x hx ↦ ne_of_gt (hsub hx))).smul continuousOn_const

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
⊢ ‖(∫ (x : ℝ) in a..b, x⁻¹ • f x) - log (b / a) • V‖ ≤ δ * |log (b / a)|
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⁻¹ʳ
hsp : IsStrictlyPositive (a • 1 + b • z)
h₁ : (a • 1 + b • z) ^ (-1) = cfc (fun r ↦ (a + b * r) ^ (-1)) z
h₂ : a • 1 + b • z ^ (-1) = cfc (fun r ↦ a + b * r ^ (-1)) z
⊢ a • x⁻¹ʳ + b • (conjSqrt x⁻¹ʳ) z⁻¹ʳ = a • x⁻¹ʳ + b • y⁻¹ʳ

Tactic:
rw [← ringInverse_conjSqrt _ _ xpos, conjSqrt_conjSqrt_ringInverse _ _ xpos]

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

Goal state before:
pp: s : ℂ
hs : s ≠ 0
⊢ (s + 1).Gammaℂ = s.Gammaℂ * s / 2 / ↑π

Tactic:
rw [Gammaℂ_def, Gammaℂ_def, Gamma_add_one _ hs, neg_add,
    cpow_add _ _ (mul_ne_zero two_ne_zero (ofReal_ne_zero.mpr pi_ne_zero)), cpow_neg_one]

Goal state after:
s : ℂ
hs : s ≠ 0
⊢ 2 * ((2 * ↑π) ^ (-s) * (2 * ↑π)⁻¹) * (s * Gamma s) = 2 * (2 * ↑π) ^ (-s) * Gamma s * s / 2 / ↑π
Module: Mathlib.Analysis.SpecialFunctions.Gaussian.PoissonSummation

Goal state before:
pp: a : ℝ
ha : a < 0
b s : ℝ
⊢ (fun x ↦ rexp (a * x ^ 2 + b * x)) =o[atTop] fun x ↦ x ^ s

Tactic:
suffices (fun x ↦ rexp (a * x ^ 2 + b * x)) =o[atTop] (fun x ↦ rexp (-x)) by
    refine this.trans ?_
    simpa only [neg_one_mul] using isLittleO_exp_neg_mul_rpow_atTop zero_lt_one s

Goal state after:
a : ℝ
ha : a < 0
b s : ℝ
⊢ (fun x ↦ rexp (a * x ^ 2 + b * x)) =o[atTop] fun x ↦ rexp (-x)
Module: Mathlib.NumberTheory.Harmonic.GammaDeriv

Goal state before:
pp: case refine_1
m : ℕ
⊢ ↑(1 / 2) ≠ -↑↑m

Tactic:
← ofReal_neg,

Goal state after:
case refine_1
m : ℕ
⊢ ↑(1 / 2) ≠ ↑(-↑m)
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
⊢ -log ↑π / 2 / ↑√π * Gamma (1 / 2) + f 1 * (-↑√π * (↑γ + 2 * log 2) / 2) = -(↑γ + log (4 * ↑π)) / 2

Tactic:
simp only [f]

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
⊢ -log ↑π / 2 / ↑√π * Gamma (1 / 2) + ↑π ^ (-1 / 2) * (-↑√π * (↑γ + 2 * log 2) / 2) = -(↑γ + log (4 * ↑π)) / 2
Module: Mathlib.Analysis.SpecialFunctions.Log.Base

Goal state before:
pp: ⊢ logb 0 = 0

Tactic:
by ext; rw [logb_zero_left, Pi.zero_apply]

Goal state after:
Module: Mathlib.Data.Int.Log

Goal state before:
pp: case inr
R : Type u_1
inst✝³ : Semifield R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorSemiring R
b : ℕ
r : R
hr : r ≤ 0
hb : 1 < b
⊢ ⌊r⁻¹⌋₊ < b ∨ b ≤ 1

Tactic:
· refine Or.inl (lt_of_le_of_lt ?_ hb)
    exact Nat.floor_le_one_of_le_one ((inv_nonpos.2 hr).trans zero_le_one)

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

Goal state before:
pp: x : ℝ
⊢ x ≤ x * x + 1

Tactic:
nlinarith

Goal state after:
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 ⊆ A, (IsCompact ∘ closure) K ∧ r < μ K

Tactic:
obtain ⟨K, hK1, ⟨hK2, _⟩, hK4⟩ := h hA r hr
    refine ⟨K, hK1, ?_, hK4⟩
    simp only [Function.comp_apply]
    exact hK2.closure

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

Goal state before:
pp: 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
⊢ g x * g x ≤ ‖g‖ * ‖g‖

Tactic:
rw [← abs_le_iff_mul_self_le, abs_norm]

Goal state after:
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
⊢ |g x| ≤ ‖g‖
Module: Mathlib.MeasureTheory.Constructions.HaarToSphere

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

Tactic:
restrict_apply (measurable_fst hs),

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

Goal state before:
pp: a b c : ℂ
hc : ∀ (k : ℕ), c ≠ -↑k
n : ℕ
⊢ (Gamma c)⁻¹ * (ordinaryHypergeometricSeries ℂ a b c).coeff n = (a.regularizedGaussHGFunSeries b c).coeff n

Tactic:
by
  rw [coeff_regularizedGaussHGFunSeries, ordinaryHypergeometricSeries,
    FormalMultilinearSeries.coeff_ofScalars, ordinaryHypergeometricCoefficient,
    ← Gamma_add_nat_div_Gamma_eq c hc]
  grind

Goal state after:
Module: Mathlib.MeasureTheory.Constructions.HaarToSphere

Goal state before:
pp: E : Type u_1
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : MeasurableSpace E
F : Type u_2
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : Nontrivial E
μ : Measure E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : BorelSpace E
inst✝ : μ.IsAddHaarMeasure
f : ℝ → F
r x : ℝ
⊢ x ∈ Ioi 0 →
    (fun y ↦ y ^ (dim E - 1) • (Iio r).indicator f y) x = (Ioo 0 r).indicator (fun y ↦ y ^ (dim E - 1) • f y) x

Tactic:
(hx : 0 < x)

Goal state after:
E : Type u_1
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : MeasurableSpace E
F : Type u_2
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : Nontrivial E
μ : Measure E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : BorelSpace E
inst✝ : μ.IsAddHaarMeasure
f : ℝ → F
r x : ℝ
hx : 0 < x
⊢ (fun y ↦ y ^ (dim E - 1) • (Iio r).indicator f y) x = (Ioo 0 r).indicator (fun y ↦ y ^ (dim E - 1) • f y) x
Module: Mathlib.Analysis.SpecialFunctions.Stirling

Goal state before:
pp: case refine_2
n : ℕ
h_nonneg : 0 ≤ (1 / (2 * ↑(n + 1) + 1)) ^ 2
this :
  HasSum (fun i ↦ (1 / (2 * ↑(n + 1) + 1)) ^ 2 * ((1 / (2 * ↑(n + 1) + 1)) ^ 2) ^ i)
    ((1 / (2 * ↑(n + 1) + 1)) ^ 2 * (1 - (1 / (2 * ↑(n + 1) + 1)) ^ 2)⁻¹)
⊢ HasSum (fun k ↦ ((1 / (2 * ↑(n + 1) + 1)) ^ 2) ^ (k + 1))
    ((1 / (2 * ↑(n + 1) + 1)) ^ 2 / (1 - (1 / (2 * ↑(n + 1) + 1)) ^ 2))

Tactic:
simp_rw [← _root_.pow_succ'] at this

Goal state after:
case refine_2
n : ℕ
h_nonneg : 0 ≤ (1 / (2 * ↑(n + 1) + 1)) ^ 2
this :
  HasSum (fun i ↦ ((1 / (2 * ↑(n + 1) + 1)) ^ 2) ^ (i + 1))
    ((1 / (2 * ↑(n + 1) + 1)) ^ 2 * (1 - (1 / (2 * ↑(n + 1) + 1)) ^ 2)⁻¹)
⊢ HasSum (fun k ↦ ((1 / (2 * ↑(n + 1) + 1)) ^ 2) ^ (k + 1))
    ((1 / (2 * ↑(n + 1) + 1)) ^ 2 / (1 - (1 / (2 * ↑(n + 1) + 1)) ^ 2))
Module: Mathlib.Analysis.SpecialFunctions.Stirling

Goal state before:
pp: n : ℕ
r : ℝ := (1 / (2 * (↑n + 1) + 1)) ^ 2
hr : r = (1 / (2 * (↑n + 1) + 1)) ^ 2
hr1 : r < 1
this : HasSum (fun j ↦ r ^ (j + 1) / 3) (1 / (12 * ↑(n + 1) * (↑(n + 1) + 1)))
j : ℕ
⊢ 1 / (2 * ↑(j + 1) + 1) * ((1 / (2 * ↑(n + 1) + 1)) ^ 2) ^ (j + 1) ≤ r ^ (j + 1) / 3

Tactic:
simpa [hr, field] using show (3 : ℝ) ≤ 2 * (j + 1) + 1 by norm_cast; grind

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

Goal state before:
pp: c : ℝ := 1 - 12⁻¹ - log 2 / 2
h : ∀ (n : ℕ), 1 - 12⁻¹ - log 2 / 2 ≤ log (stirlingSeq (n + 1))
n : ℕ
⊢ rexp c ≤ stirlingSeq (n + 1)

Tactic:
← le_log_iff_exp_le (stirlingSeq'_pos n)

Goal state after:
c : ℝ := 1 - 12⁻¹ - log 2 / 2
h : ∀ (n : ℕ), 1 - 12⁻¹ - log 2 / 2 ≤ log (stirlingSeq (n + 1))
n : ℕ
⊢ c ≤ log (stirlingSeq (n + 1))
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.ChebyshevGauss

Goal state before:
pp: n : ℕ
P : ℝ[X]
hn : n ≠ 0
hP : P.degree < 2 * ↑n
hmem : P ∈ Submodule.span ℝ (↑(chebyshevTsequence ℝ) '' Set.Iio (2 * n))
⊢ ∫ (x : ℝ), eval x P ∂measureT = sumZeroes n P

Tactic:
show Set.Iio (2 * n) = Finset.range (2 * n) by simp,

Goal state after:
n : ℕ
P : ℝ[X]
hn : n ≠ 0
hP : P.degree < 2 * ↑n
hmem : P ∈ Submodule.span ℝ (↑(chebyshevTsequence ℝ) '' ↑(range (2 * n)))
⊢ ∫ (x : ℝ), eval x P ∂measureT = sumZeroes n P
Module: Mathlib.Data.Int.Fib.Basic

Goal state before:
pp: n : ℤ
⊢ fib (2 * n + 1) = fib (n + 1) ^ 2 + fib n ^ 2

Tactic:
by
  have := fib_add (n + 1) n
  grind

Goal state after:
Module: Mathlib.Data.Int.Fib.Basic

Goal state before:
pp: case inr
n : ℤ
m : ℕ
h : -↑m ∣ n
⊢ fib (-↑m) ∣ fib n

Tactic:
simp [fib_neg_natCast, ← fib_natCast, fib_natCast_dvd <| Int.neg_dvd.mp h]

Goal state after:
Module: Mathlib.Tactic.NormNum.Prime

Goal state before:
pp: case refine_2.inr.inl
n k k' : ℕ
e : k + 2 = k'
h : MinFacHelper n k
np : n.minFac ≠ k
h2✝ : k < n.minFac
h2 : k.succ = n.minFac
h3 : 2 ∣ n.minFac
⊢ 2 = n.minFac

Tactic:
simpa [dvd_prime <| minFac_prime h.one_lt.ne'] using h3

Goal state after:
Module: Mathlib.Tactic.NormNum.Prime

Goal state before:
pp: a : ℕ
h : a % 2 = 0
⊢ a.minFac = ↑2

Tactic:
by rw [cast_ofNat, minFac_eq_two_iff, Nat.dvd_iff_mod_eq_zero, h]

Goal state after:
Module: Mathlib.Analysis.SumIntegralComparisons

Goal state before:
pp: x₀ : ℝ
a : ℕ
f : ℝ → ℝ
hf : MonotoneOn f (Icc x₀ (x₀ + ↑a))
⊢ ∫ (x : ℝ) in x₀..x₀ + ↑a, f x ≤ ∑ i ∈ Finset.range a, f (x₀ + ↑(i + 1))

Tactic:
rw [← neg_le_neg_iff, ← Finset.sum_neg_distrib, ← intervalIntegral.integral_neg]
  exact hf.neg.sum_le_integral

Goal state after: