mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Order

Goal state before:
pp: A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
p : ℝ≥0
hp : p ∈ Ioo 0 1
⊢ ConcaveOn ℝ (Ici 0) fun a ↦ a ^ p

Tactic:
obtain ⟨μ, hμ⟩ := CFC.exists_measure_nnrpow_eq_integral_cfcₙ_rpowIntegrand₀₁ A hp

Goal state after:
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
p : ℝ≥0
hp : p ∈ Ioo 0 1
μ : Measure ℝ
hμ :
  ∀ a ∈ Ici 0,
    IntegrableOn (fun t ↦ cfcₙ ((↑p).rpowIntegrand₀₁ t) a) (Ioi 0) μ ∧
      a ^ p = ∫ (t : ℝ) in Ioi 0, cfcₙ ((↑p).rpowIntegrand₀₁ t) a ∂μ
⊢ ConcaveOn ℝ (Ici 0) fun a ↦ a ^ p
Module: Mathlib.Analysis.Real.Pi.Irrational

Goal state before:
pp: h' : ¬Irrational (π / 2)
a : ℤ
b : ℕ
hb : 0 < b
h : π / 2 = ↑a / ↑b
this : 0 < ↑a / ↑b
⊢ 0 < ↑a

Tactic:
lt_div_iff₀ (by positivity),

Goal state after:
h' : ¬Irrational (π / 2)
a : ℤ
b : ℕ
hb : 0 < b
h : π / 2 = ↑a / ↑b
this : 0 * ↑b < ↑a
⊢ 0 < ↑a
Module: Mathlib.Analysis.SpecialFunctions.FrullaniIntegral

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

Tactic:
have hint_inv : IntervalIntegrable (fun x : ℝ ↦ x⁻¹ * δ) volume a b := by
    apply ContinuousOn.intervalIntegrable
    exact (continuousOn_inv₀.mono (fun x hx ↦ ne_of_gt (hsub hx))).mul 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
hint_inv : IntervalIntegrable (fun x ↦ x⁻¹ * δ) volume a b
⊢ ‖(∫ (x : ℝ) in a..b, x⁻¹ • f x) - log (b / a) • V‖ ≤ δ * |log (b / a)|
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation

Goal state before:
pp: p x : ℝ
hp : 0 < p
⊢ p.rpowIntegrand₀₁ 0 x = 0

Tactic:
simp [rpowIntegrand₀₁, Real.zero_rpow hp.ne']

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

Goal state before:
pp: case hb
s : ℂ
hs : 0 < s.re
⊢ 0 < s.re / 2

Tactic:
exact div_pos hs two_pos

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

Goal state before:
pp: n : ℕ
⊢ 0 < ↑(↑(n + 1))⁻¹ + ↑(harmonic n) - ↑(harmonic n) - (log (↑(n + 1) + 1) - log (↑n + 1))

Tactic:
add_sub_cancel_right,

Goal state after:
n : ℕ
⊢ 0 < ↑(↑(n + 1))⁻¹ - (log (↑(n + 1) + 1) - log (↑n + 1))
Module: Mathlib.NumberTheory.Harmonic.EulerMascheroni

Goal state before:
pp: h1 : eulerMascheroniSeq' 6 = 49 / 20 - log 6
this : rexp (107 / 60) < 2.7182818286 ^ (107 / 60)
⊢ 2.7182818286 ^ 107 < 6 ^ 60

pp: case h
h1 : eulerMascheroniSeq' 6 = 49 / 20 - log 6
this : rexp (107 / 60) < 2.7182818286 ^ (107 / 60)
⊢ 60 ≠ 0

pp: case hx
h1 : eulerMascheroniSeq' 6 = 49 / 20 - log 6
this : rexp (107 / 60) < 2.7182818286 ^ (107 / 60)
⊢ 0 ≤ 2.7182818286

pp: case hx
h1 : eulerMascheroniSeq' 6 = 49 / 20 - log 6
this : rexp (107 / 60) < 2.7182818286 ^ (107 / 60)
⊢ 0 ≤ 2.7182818286 ^ (107 / 60)

pp: case hy
h1 : eulerMascheroniSeq' 6 = 49 / 20 - log 6
this : rexp (107 / 60) < 2.7182818286 ^ (107 / 60)
⊢ 0 ≤ 6

pp: case hz
h1 : eulerMascheroniSeq' 6 = 49 / 20 - log 6
this : rexp (107 / 60) < 2.7182818286 ^ (107 / 60)
⊢ 0 < 60

Tactic:
← Nat.cast_ofNat,

Goal state after:
h1 : eulerMascheroniSeq' 6 = 49 / 20 - log 6
this : rexp (107 / 60) < 2.7182818286 ^ (107 / 60)
⊢ 2.7182818286 ^ ↑107 < 6 ^ 60

case h
h1 : eulerMascheroniSeq' 6 = 49 / 20 - log 6
this : rexp (107 / 60) < 2.7182818286 ^ (107 / 60)
⊢ 60 ≠ 0

case hx
h1 : eulerMascheroniSeq' 6 = 49 / 20 - log 6
this : rexp (107 / 60) < 2.7182818286 ^ (107 / 60)
⊢ 0 ≤ 2.7182818286

case hx
h1 : eulerMascheroniSeq' 6 = 49 / 20 - log 6
this : rexp (107 / 60) < 2.7182818286 ^ (107 / 60)
⊢ 0 ≤ 2.7182818286 ^ (107 / 60)

case hy
h1 : eulerMascheroniSeq' 6 = 49 / 20 - log 6
this : rexp (107 / 60) < 2.7182818286 ^ (107 / 60)
⊢ 0 ≤ 6

case hz
h1 : eulerMascheroniSeq' 6 = 49 / 20 - log 6
this : rexp (107 / 60) < 2.7182818286 ^ (107 / 60)
⊢ 0 < 60
Module: Mathlib.NumberTheory.Harmonic.EulerMascheroni

Goal state before:
pp: h1 : eulerMascheroniSeq' 6 = 49 / 20 - log 6
this : rexp (107 / 60) < 2.7182818286 ^ (107 / 60)
⊢ 2.7182818286 ^ ↑107 < 6 ^ 60

pp: case h
h1 : eulerMascheroniSeq' 6 = 49 / 20 - log 6
this : rexp (107 / 60) < 2.7182818286 ^ (107 / 60)
⊢ 60 ≠ 0

pp: case hx
h1 : eulerMascheroniSeq' 6 = 49 / 20 - log 6
this : rexp (107 / 60) < 2.7182818286 ^ (107 / 60)
⊢ 0 ≤ 2.7182818286

pp: case hx
h1 : eulerMascheroniSeq' 6 = 49 / 20 - log 6
this : rexp (107 / 60) < 2.7182818286 ^ (107 / 60)
⊢ 0 ≤ 2.7182818286 ^ (107 / 60)

pp: case hy
h1 : eulerMascheroniSeq' 6 = 49 / 20 - log 6
this : rexp (107 / 60) < 2.7182818286 ^ (107 / 60)
⊢ 0 ≤ 6

pp: case hz
h1 : eulerMascheroniSeq' 6 = 49 / 20 - log 6
this : rexp (107 / 60) < 2.7182818286 ^ (107 / 60)
⊢ 0 < 60

Tactic:
← Nat.cast_ofNat,

Goal state after:
h1 : eulerMascheroniSeq' 6 = 49 / 20 - log 6
this : rexp (107 / 60) < 2.7182818286 ^ (107 / 60)
⊢ 2.7182818286 ^ ↑↑107 < 6 ^ 60

case h
h1 : eulerMascheroniSeq' 6 = 49 / 20 - log 6
this : rexp (107 / 60) < 2.7182818286 ^ (107 / 60)
⊢ 60 ≠ 0

case hx
h1 : eulerMascheroniSeq' 6 = 49 / 20 - log 6
this : rexp (107 / 60) < 2.7182818286 ^ (107 / 60)
⊢ 0 ≤ 2.7182818286

case hx
h1 : eulerMascheroniSeq' 6 = 49 / 20 - log 6
this : rexp (107 / 60) < 2.7182818286 ^ (107 / 60)
⊢ 0 ≤ 2.7182818286 ^ (107 / 60)

case hy
h1 : eulerMascheroniSeq' 6 = 49 / 20 - log 6
this : rexp (107 / 60) < 2.7182818286 ^ (107 / 60)
⊢ 0 ≤ 6

case hz
h1 : eulerMascheroniSeq' 6 = 49 / 20 - log 6
this : rexp (107 / 60) < 2.7182818286 ^ (107 / 60)
⊢ 0 < 60
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Digamma

Goal state before:
pp: ⊢ -↑Real.eulerMascheroniConstant / 1 = -↑Real.eulerMascheroniConstant

Tactic:
div_one

Goal state after:
⊢ -↑Real.eulerMascheroniConstant = -↑Real.eulerMascheroniConstant
Module: Mathlib.NumberTheory.Harmonic.GammaDeriv

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

Tactic:
← hder_nat

Goal state after:
n✝ : ℕ
f : ℝ → ℝ := log ∘ Gamma
hc : ConvexOn ℝ (Ioi 0) f
h_rec : ∀ (x : ℝ), 0 < x → f (x + 1) = f x + log x
hder : ∀ {x : ℝ}, 0 < x → DifferentiableAt ℝ f x
hder_rec : ∀ (x : ℝ), 0 < x → deriv f (x + 1) = deriv f x + 1 / x
hder_nat : ∀ (n : ℕ), deriv f (↑n + 1) = deriv f 1 + ↑(harmonic n)
derivLB : ∀ (n : ℕ), 0 < n → log ↑n ≤ deriv f (↑n + 1)
derivUB : ∀ (n : ℕ), deriv f (↑n + 1) ≤ log (↑n + 1)
n : ℕ
hn : 0 < n
⊢ log ↑n ≤ deriv f (↑n + 1)
Module: Mathlib.NumberTheory.Harmonic.GammaDeriv

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

Tactic:
← hder_nat

Goal state after:
case a
n✝ : ℕ
f : ℝ → ℝ := log ∘ Gamma
hc : ConvexOn ℝ (Ioi 0) f
h_rec : ∀ (x : ℝ), 0 < x → f (x + 1) = f x + log x
hder : ∀ {x : ℝ}, 0 < x → DifferentiableAt ℝ f x
hder_rec : ∀ (x : ℝ), 0 < x → deriv f (x + 1) = deriv f x + 1 / x
hder_nat : ∀ (n : ℕ), deriv f (↑n + 1) = deriv f 1 + ↑(harmonic n)
derivLB : ∀ (n : ℕ), 0 < n → log ↑n ≤ deriv f (↑n + 1)
derivUB : ∀ (n : ℕ), deriv f (↑n + 1) ≤ log (↑n + 1)
n : ℕ
⊢ deriv f (↑n + 1) ≤ log (↑n + 1)
Module: Mathlib.NumberTheory.Harmonic.GammaDeriv

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

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

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

Tactic:
mul_one_div,

Goal state after:
case e_a.e_a.e_a
h_diff : ∀ {s : ℝ}, 0 < s → DifferentiableAt ℝ Gamma s
h_diff' : ∀ {s : ℝ}, 0 < s → DifferentiableAt ℝ (fun s ↦ Gamma (2 * s)) s
⊢ deriv Gamma (2 / 2) * 2 = -2 * γ

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

case e_a.e_a.e_a.hh
h_diff : ∀ {s : ℝ}, 0 < s → DifferentiableAt ℝ Gamma s
h_diff' : ∀ {s : ℝ}, 0 < s → DifferentiableAt ℝ (fun s ↦ Gamma (2 * s)) s
⊢ DifferentiableAt ℝ (fun s ↦ 2 * s) (1 / 2)
Module: Mathlib.NumberTheory.Harmonic.GammaDeriv

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

Tactic:
ne_eq,

Goal state after:
case refine_1
m : ℕ
⊢ ¬↑(1 / 2) = ↑(-↑m)
Module: Mathlib.NumberTheory.Harmonic.GammaDeriv

Goal state before:
pp: f : ℂ → ℂ := fun s ↦ 2 * (2 * ↑π) ^ (-s)
this✝ : HasDerivAt (fun s ↦ 2 * (2 * ↑π) ^ (-s)) (-log (2 * ↑π) / ↑π) 1
this : HasDerivAt ((fun s ↦ 2 * (2 * ↑π) ^ (-s)) * Gamma) (-log (2 * ↑π) / ↑π + -↑γ * (1 / ↑π)) 1
⊢ HasDerivAt Gammaℂ (-(↑γ + log (2 * ↑π)) / ↑π) 1

Tactic:
mul_one_div,

Goal state after:
f : ℂ → ℂ := fun s ↦ 2 * (2 * ↑π) ^ (-s)
this✝ : HasDerivAt (fun s ↦ 2 * (2 * ↑π) ^ (-s)) (-log (2 * ↑π) / ↑π) 1
this : HasDerivAt ((fun s ↦ 2 * (2 * ↑π) ^ (-s)) * Gamma) (-log (2 * ↑π) / ↑π + -↑γ / ↑π) 1
⊢ HasDerivAt Gammaℂ (-(↑γ + log (2 * ↑π)) / ↑π) 1
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₂ : R
h₀ : 0 < r₁
h : r₁ ≤ r₂
⊢ log b r₁ ≤ log b r₂

Tactic:
rcases le_total r₁ 1 with h₁ | h₁ <;> rcases le_total r₂ 1 with h₂ | h₂

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

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

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

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

Goal state before:
pp: x : ℝ
⊢ logb 0 x = 0

Tactic:
simp only [← log_div_log, log_zero, div_zero]

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

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

Tactic:
rw [← logb_one]

Goal state after:
b x : ℝ
hb : 1 < b
h : 0 < x
⊢ logb b x < logb ?m.18 1 ↔ x < 1

b x : ℝ
hb : 1 < b
h : 0 < x
⊢ ℝ
Module: Mathlib.Analysis.SpecialFunctions.Log.Base

Goal state before:
pp: case cons
b : ℝ
α : Type u_1
f : α → ℝ
a✝¹ : α
s✝ : Finset α
h✝ : a✝¹ ∉ s✝
a✝ : (∀ x ∈ s✝, f x ≠ 0) → logb b (∏ i ∈ s✝, f i) = ∑ i ∈ s✝, logb b (f i)
hf : ∀ x ∈ Finset.cons a✝¹ s✝ h✝, f x ≠ 0
⊢ logb b (∏ i ∈ Finset.cons a✝¹ s✝ h✝, f i) = ∑ i ∈ Finset.cons a✝¹ s✝ h✝, logb b (f i)

Tactic:
simp_all [logb_mul, Finset.prod_ne_zero_iff]

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

Goal state before:
pp: c : ℝ
⊢ (fun x ↦ log (c * x)) =O[atTop] log

Tactic:
obtain rfl | hc := eq_or_ne c 0
  · simpa using isLittleO_const_log_atTop.isBigO
  · calc (fun x ↦ log (c * x))
      =ᶠ[atTop] (fun x => log c + log x) := by
          filter_upwards [eventually_gt_atTop 0] with a ha using log_mul hc ha.ne'
      _ =O[atTop] log :=
          isLittleO_const_log_atTop.isBigO.add (Asymptotics.isBigO_refl ..)

Goal state after:
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))
a : ℝ
ha : ↑n < a
b : ℝ
hb : ↑n < b
hab : a ≤ b
⊢ deriv (fun x ↦ Polynomial.eval x (descPochhammer ℝ (n + 1))) a ≤
    deriv (fun x ↦ Polynomial.eval x (descPochhammer ℝ (n + 1))) b

Tactic:
deriv_descPochhammer_eval_eq_sum_prod_range_erase

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

Goal state before:
pp: n : ℕ
hn : n ≠ 0
ι : Type u_2
t : Finset ι
p : ι → ℕ
w : ι → ℝ
h₀ : ∀ i ∈ t, 0 ≤ w i
h₁ : ∑ i ∈ t, w i = 1
h_avg : ↑n - 1 ≤ ∑ i ∈ t, w i * ↑(p i)
⊢ Polynomial.eval (∑ i ∈ t, w i * ↑(p i)) (descPochhammer ℝ n) / ↑n.factorial ≤ ∑ i ∈ t, w i * ↑((p i).choose n)

Tactic:
simp_rw [Nat.cast_choose_eq_descPochhammer_div,
    mul_div, ← Finset.sum_div, descPochhammer_eval_eq_descFactorial]
  apply div_le_div_of_nonneg_right _ (by positivity)
  exact descPochhammer_eval_le_sum_descFactorial hn p w h₀ h₁ h_avg

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
ε : ℝ
f : C(E, ℝ)
K : Set E
hK : MeasurableSet K
hε : 0 < ε
hKP : P Kᶜ < ↑ε.toNNReal
⊢ P.real Kᶜ < ε

Tactic:
exact toReal_lt_of_lt_ofReal hKP

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

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

Tactic:
refine LE.le.trans_eq (b := 2 * (2 * ‖l - s‖) ^ 3) ?_ (by ring)

Goal state after:
case neg
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
⊢ 2 * ‖l‖ ^ 3 ≤ 2 * (2 * ‖↑l - s‖) ^ 3
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Basic

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

Tactic:
| add_two n ih1 ih2 =>

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Basic

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

Tactic:
| add_two n ih1 ih2 =>

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

Goal state before:
pp: ⊢ 1 / (√2 * (1 / rexp 1)) = rexp 1 / √2

Tactic:
mul_one_div,

Goal state after:
⊢ 1 / (√2 / rexp 1) = rexp 1 / √2
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

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

Tactic:
L.derivWeierstrassP_add_coe,

Goal state after:
L : PeriodPair
l : ↥L.lattice
⊢ ℘'[L] 0 = 0
Module: Mathlib.Analysis.SpecialFunctions.Stirling

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

Tactic:
pow_add

Goal state after:
case e'_5
m : ℕ
f : ℕ → ℝ := fun k ↦ 1 / (2 * ↑k + 1) * ((1 / (2 * ↑(m + 1) + 1)) ^ 2) ^ k
k : ℕ
⊢ 1 / (2 * ↑k + 1) * (1 / (2 * ↑(m + 1) + 1)) ^ (2 * k) =
    (↑(m + 1) + 1 / 2) * (2 * (1 / (2 * ↑k + 1)) * ((1 / (2 * (↑m + 1) + 1)) ^ (2 * k) * (1 / (2 * (↑m + 1) + 1)) ^ 1))
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Orthogonality

Goal state before:
pp: f : ℝ → ℝ
⊢ ∫ (x : ℝ) in -1..1, f x * √(1 - x ^ 2)⁻¹ = ∫ (x : ℝ) in 1..-1, f x * -√(1 - x ^ 2)⁻¹

Tactic:
rw [integral_symm, ← intervalIntegral.integral_neg]

Goal state after:
f : ℝ → ℝ
⊢ ∫ (x : ℝ) in 1..-1, -(f x * √(1 - x ^ 2)⁻¹) = ∫ (x : ℝ) in 1..-1, f x * -√(1 - x ^ 2)⁻¹
Module: Mathlib.Analysis.SpecialFunctions.Stirling

Goal state before:
pp: a : ℝ
hane : a ≠ 0
ha : Tendsto stirlingSeq atTop (𝓝 a)
⊢ a ^ 2 / 2 = a ^ 4 / a ^ 2 * (1 / 2)

Tactic:
mul_one_div,

Goal state after:
a : ℝ
hane : a ≠ 0
ha : Tendsto stirlingSeq atTop (𝓝 a)
⊢ a ^ 2 / 2 = a ^ 4 / a ^ 2 / 2
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Orthogonality

Goal state before:
pp: ⊢ ∫ (x : ℝ), eval x (T ℝ 0) ∂measureT = π

Tactic:
integral_measureT_eq_integral_cos

Goal state after:
⊢ ∫ (θ : ℝ) in 0..π, eval (cos θ) (T ℝ 0) = π
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Orthogonality

Goal state before:
pp: n : ℤ
hn : n ≠ 0
hn' : ↑n ≠ 0
this : ∫ (θ : ℝ) in 0..↑n * π, cos θ = 0
⊢ ∫ (x : ℝ), eval x (T ℝ n) ∂measureT = 0

Tactic:
integral_measureT_eq_integral_cos

Goal state after:
n : ℤ
hn : n ≠ 0
hn' : ↑n ≠ 0
this : ∫ (θ : ℝ) in 0..↑n * π, cos θ = 0
⊢ ∫ (θ : ℝ) in 0..π, eval (cos θ) (T ℝ n) = 0
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Orthogonality

Goal state before:
pp: n : ℤ
hn : n ≠ 0
hn' : ↑n ≠ 0
⊢ ∫ (θ : ℝ) in 0..↑n * π, deriv sin θ = 0

Tactic:
by_cases! 0 ≤ n

Goal state after:
case pos
n : ℤ
hn : n ≠ 0
hn' : ↑n ≠ 0
h✝ : 0 ≤ n
⊢ ∫ (θ : ℝ) in 0..↑n * π, deriv sin θ = 0

case neg
n : ℤ
hn : n ≠ 0
hn' : ↑n ≠ 0
h✝ : n < 0
⊢ ∫ (θ : ℝ) in 0..↑n * π, deriv sin θ = 0
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.ChebyshevGauss

Goal state before:
pp: case a
n : ℕ
k : ℤ
hn : n ≠ 0
hk : Complex.exp (↑k / ↑n * ↑π * I) = 1
m : ℤ
hx : ↑k / ↑n * ↑π * I = ↑m * (2 * ↑π * I)
⊢ ↑k + ↑m * (2 * ↑π * I) * (↑n / ↑π / I) - (2 * ↑n * ↑m + ↑k / ↑n * ↑π * I * (↑n / ↑π / I)) = 0

Tactic:
field [show (n : ℂ) ≠ 0 by aesop]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.ChebyshevGauss

Goal state before:
pp: n : ℕ
k : ℤ
hn : n ≠ 0
hk : ¬2 * ↑n ∣ k
⊢ ↑n * (↑k / ↑n * ↑π * I) = ↑k * (↑π * I)

Tactic:
field [show (n : ℂ) ≠ 0 by aesop]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.ChebyshevGauss

Goal state before:
pp: n : ℕ
hn : n ≠ 0
c : ℕ → ℝ
hP : (∑ i ∈ range (2 * n), c i • ↑(chebyshevTsequence ℝ) i).degree < 2 * ↑n
⊢ ∫ (x : ℝ), ∑ x_1 ∈ range (2 * n), c x_1 • eval x (↑(chebyshevTsequence ℝ) x_1) ∂measureT =
    sumZeroes n (∑ i ∈ range (2 * n), c i • ↑(chebyshevTsequence ℝ) i)

Tactic:
MeasureTheory.integral_finsetSum,

Goal state after:
n : ℕ
hn : n ≠ 0
c : ℕ → ℝ
hP : (∑ i ∈ range (2 * n), c i • ↑(chebyshevTsequence ℝ) i).degree < 2 * ↑n
⊢ ∑ i ∈ range (2 * n), ∫ (a : ℝ), c i • eval a (↑(chebyshevTsequence ℝ) i) ∂measureT =
    sumZeroes n (∑ i ∈ range (2 * n), c i • ↑(chebyshevTsequence ℝ) i)

case hf
n : ℕ
hn : n ≠ 0
c : ℕ → ℝ
hP : (∑ i ∈ range (2 * n), c i • ↑(chebyshevTsequence ℝ) i).degree < 2 * ↑n
⊢ ∀ i ∈ range (2 * n), MeasureTheory.Integrable (fun x ↦ c i • eval x (↑(chebyshevTsequence ℝ) i)) measureT
Module: Mathlib.NumberTheory.Niven

Goal state before:
pp: case inl
r : ℚ
hr : 3 < (Int.fract r).den
hnz : ¬Irrational (cos (↑r * π))
hr' : Int.fract r = 0
⊢ False

Tactic:
rw [Set.mem_singleton_iff] at hr'

Goal state after:
case inl
r : ℚ
hr : 3 < (Int.fract r).den
hnz : ¬Irrational (cos (↑r * π))
hr' : Int.fract r = 0
⊢ False
Module: Mathlib.NumberTheory.Niven

Goal state before:
pp: case inr.inl
r : ℚ
hr : 3 < (Int.fract r).den
hnz : ¬Irrational (cos (↑r * π))
hr' : Int.fract r = 1 / 3
⊢ False

Tactic:
rw [Set.mem_singleton_iff] at hr'

Goal state after:
case inr.inl
r : ℚ
hr : 3 < (Int.fract r).den
hnz : ¬Irrational (cos (↑r * π))
hr' : Int.fract r = 1 / 3
⊢ False
Module: Mathlib.NumberTheory.Niven

Goal state before:
pp: case inr.inr.inl
r : ℚ
hr : 3 < (Int.fract r).den
hnz : ¬Irrational (cos (↑r * π))
hr' : Int.fract r = 1 / 2
⊢ False

Tactic:
rw [Set.mem_singleton_iff] at hr'

Goal state after:
case inr.inr.inl
r : ℚ
hr : 3 < (Int.fract r).den
hnz : ¬Irrational (cos (↑r * π))
hr' : Int.fract r = 1 / 2
⊢ False
Module: Mathlib.NumberTheory.Niven

Goal state before:
pp: case inr.inr.inr
r : ℚ
hr : 3 < (Int.fract r).den
hnz : ¬Irrational (cos (↑r * π))
hr' : Int.fract r ∈ {2 / 3}
⊢ False

Tactic:
rw [Set.mem_singleton_iff] at hr'

Goal state after:
case inr.inr.inr
r : ℚ
hr : 3 < (Int.fract r).den
hnz : ¬Irrational (cos (↑r * π))
hr' : Int.fract r = 2 / 3
⊢ False
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: L : PeriodPair
l₀ z x : ℂ
hx : ∀ (l : ↥L.lattice), ↑l ≠ l₀ → ‖z - x‖ < ‖↑l - x‖
⊢ ∑' (l : ↥L.lattice) (i : ℕ), L.weierstrassPExceptSummand l₀ x i l * (z - x) ^ i =
    ∑' (i : ℕ), (L.weierstrassPExceptSeries l₀ x).coeff i * (z - x) ^ i

Tactic:
coeff_weierstrassPExceptSeries,

Goal state after:
L : PeriodPair
l₀ z x : ℂ
hx : ∀ (l : ↥L.lattice), ↑l ≠ l₀ → ‖z - x‖ < ‖↑l - x‖
⊢ ∑' (l : ↥L.lattice) (i : ℕ), L.weierstrassPExceptSummand l₀ x i l * (z - x) ^ i =
    ∑' (i : ℕ), (∑' (l : ↥L.lattice), L.weierstrassPExceptSummand l₀ x i l) * (z - x) ^ i
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: L : PeriodPair
l₀ z x : ℂ
hx : ∀ (l : ↥L.lattice), ↑l ≠ l₀ → ‖z - x‖ < ‖↑l - x‖
⊢ Summable fun i ↦ (L.weierstrassPExceptSeries l₀ x).coeff i * (z - x) ^ i

Tactic:
coeff_weierstrassPExceptSeries,

Goal state after:
L : PeriodPair
l₀ z x : ℂ
hx : ∀ (l : ↥L.lattice), ↑l ≠ l₀ → ‖z - x‖ < ‖↑l - x‖
⊢ Summable fun i ↦ (∑' (l : ↥L.lattice), L.weierstrassPExceptSummand l₀ x i l) * (z - x) ^ i
Module: Mathlib.Order.Interval.Finset.Box

Goal state before:
pp: x : ℤ × ℤ
n : ℕ
⊢ x ∈ box (n + 1) ↔ max x.1.natAbs x.2.natAbs = n + 1

Tactic:
simp [box_succ_eq_sdiff, Prod.le_def]

Goal state after:
x : ℤ × ℤ
n : ℕ
⊢ ((-1 ≤ x.1 + ↑n ∧ -1 ≤ x.2 + ↑n) ∧ x.1 ≤ ↑n + 1 ∧ x.2 ≤ ↑n + 1) ∧ (-↑n ≤ x.1 → -↑n ≤ x.2 → x.1 ≤ ↑n → ↑n < x.2) ↔
    max x.1.natAbs x.2.natAbs = n + 1
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal

Goal state before:
pp: n k i : ℕ
hi : i ≤ n
x : ℝ
hx : 1 ≤ x
⊢ 0 ≤ (-1) ^ i * iterateDerivativeC n k x i

Tactic:
rw [iterateDerivativeC, ← mul_assoc]
  refine mul_nonneg ?_ (Finset.sum_nonneg' ?_)
  · rw [← mul_assoc, mul_comm (a := (-1) ^ i), mul_assoc]
    exact le_of_lt <| mul_pos (Nat.cast_pos.mpr <| Nat.factorial_pos k)
      (negOnePow_mul_leadingCoeffC_pos hi)
  · exact fun t => Finset.prod_nonneg (fun a _ => by grind [show node n a ≤ 1 from cos_le_one _])

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema

Goal state before:
pp: case mpr
n : ℕ
hn : n ≠ 0
x : ℝ
hx : x ∈ Set.Icc (-1) 1
⊢ (∃ k ≤ n, x = cos (↑k * π / ↑n)) → IsExtrOn (fun x ↦ eval x (T ℝ ↑n)) (Set.Icc (-1) 1) x

Tactic:
· rintro ⟨k, hk, hx⟩
    rw [hx]
    exact isExtrOn_T_real hn hk

Goal state after: