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

Goal state before:
pp: case monomial.inr
p : ℂ[X]
m : ℕ
a : ℂ
k : ℕ
⊢ fourierCoeff ⇑(toAddCircle ((monomial m) a)) ↑k = if 0 ≤ ↑k then ((monomial m) a).coeff (↑k).natAbs else 0

Tactic:
| monomial m a =>

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

Goal state before:
pp: case 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
⊢ (p.support.sup' ⋯ fun i ↦ v (p.coeff i) * c ^ i) ≤ ⨆ i, v (p.coeff i) * c ^ i

Tactic:
obtain ⟨i, hi⟩ := exists_eq_gaussNorm v c p

Goal state after:
case 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
i : ℕ
hi : gaussNorm v c p = v (p.coeff i) * c ^ i
⊢ (p.support.sup' ⋯ fun i ↦ v (p.coeff i) * c ^ i) ≤ ⨆ i, v (p.coeff i) * c ^ i
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 | gaussNorm v c p = v (p.coeff i) * c ^ i}.Nonempty

Tactic:
obtain ⟨i, hi⟩ := exists_eq_gaussNorm v c p

Goal state after:
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
Module: Mathlib.RingTheory.MvPowerSeries.GaussNorm

Goal state before:
pp: R : Type u_1
σ : Type u_2
v : R → ℝ
c : σ → ℝ
f : MvPowerSeries σ R
inst✝ : Semiring R
vZero : v 0 = 0
vNonneg : ∀ (a : R), v a ≥ 0
h_eq_zero : ∀ (x : R), v x = 0 → x = 0
hc : ∀ (i : σ), 0 < c i
hbd : HasGaussNorm v c f
⊢ f ≠ 0 → gaussNorm v c f ≠ 0

Tactic:
intro hf

Goal state after:
R : Type u_1
σ : Type u_2
v : R → ℝ
c : σ → ℝ
f : MvPowerSeries σ R
inst✝ : Semiring R
vZero : v 0 = 0
vNonneg : ∀ (a : R), v a ≥ 0
h_eq_zero : ∀ (x : R), v x = 0 → x = 0
hc : ∀ (i : σ), 0 < c i
hbd : HasGaussNorm v c f
hf : f ≠ 0
⊢ gaussNorm v c f ≠ 0
Module: Mathlib.RingTheory.MvPowerSeries.GaussNorm

Goal state before:
pp: case inl
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
hbfd : HasGaussNorm v c f
hbgd : HasGaussNorm v c g
H : ∀ (t : σ →₀ ℕ), 0 ≤ ∏ i ∈ t.support, c i ^ t i
t : σ →₀ ℕ
hv : v ((coeff t) f + (coeff t) g) ≤ max (v ((coeff t) f)) (v ((coeff t) g))
h : max (v ((coeff t) f)) (v ((coeff t) g)) = v ((coeff t) f)
⊢ v ((coeff t) (f + g)) * ∏ i ∈ t.support, c i ^ t i ≤
    max (v ((coeff t) f) * ∏ i ∈ t.support, c i ^ t i) (v ((coeff t) g) * ∏ i ∈ t.support, c i ^ t i)

Tactic:
have : max (v ((coeff t) f) * ∏ i ∈ t.support, c ↑i ^ t ↑i)
          (v ((coeff t) g) * ∏ i ∈ t.support, c ↑i ^ t ↑i) =
          (v ((coeff t) f) * ∏ i ∈ t.support, c ↑i ^ t ↑i) := by
        simp only [sup_eq_left]
        exact mul_le_mul_of_nonneg (by aesop) (by aesop) (by aesop) (H t)
      simp_rw [this]
      exact mul_le_mul_of_nonneg (by aesop) (by aesop) (by aesop) (H t)

Goal state after:
Module: Mathlib.Analysis.ODE.PicardLindelof

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E → E
x₀ : E
hf : ContDiffAt ℝ 1 f x₀
K : ℝ≥0
s : Set E
hs : s ∈ 𝓝 x₀
hl : LipschitzOnWith K f s
a : ℝ
ha : 0 < a
has : ball x₀ a ⊆ s
L : ℝ := ↑K * a + ‖f x₀‖ + 1
hL : L = ↑K * a + ‖f x₀‖ + 1
hL0 : 0 < L
x : E
hx : x ∈ closedBall x₀ (a / 2)
⊢ ‖f x‖ ≤ L

Tactic:
rw [hL]

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E → E
x₀ : E
hf : ContDiffAt ℝ 1 f x₀
K : ℝ≥0
s : Set E
hs : s ∈ 𝓝 x₀
hl : LipschitzOnWith K f s
a : ℝ
ha : 0 < a
has : ball x₀ a ⊆ s
L : ℝ := ↑K * a + ‖f x₀‖ + 1
hL : L = ↑K * a + ‖f x₀‖ + 1
hL0 : 0 < L
x : E
hx : x ∈ closedBall x₀ (a / 2)
⊢ ‖f x‖ ≤ ↑K * a + ‖f x₀‖ + 1
Module: Mathlib.Analysis.Polynomial.Order

Goal state before:
pp: case pos
P : ℝ[X]
x : ℝ
hroots : ∀ (y : ℝ), P.IsRoot y → y ≤ x
hlc : 0 ≤ P.leadingCoeff
hroots' : ∃ y, P.IsRoot y ∧ x ≤ y
⊢ 0 ≤ eval x P

Tactic:
obtain ⟨y, hroot, hle⟩ := hroots'

Goal state after:
case pos
P : ℝ[X]
x : ℝ
hroots : ∀ (y : ℝ), P.IsRoot y → y ≤ x
hlc : 0 ≤ P.leadingCoeff
y : ℝ
hroot : P.IsRoot y
hle : x ≤ y
⊢ 0 ≤ eval x P
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
hroots' : ∃ y, P.IsRoot y ∧ y ≤ x
⊢ 0 ≤ ↑↑(↑P.natDegree).negOnePow * eval x P

Tactic:
obtain ⟨y, hroot, hle⟩ := hroots'

Goal state after:
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
Module: Mathlib.Analysis.RCLike.BoundedContinuous

Goal state before:
pp: case mpr
𝕜 : Type u_1
E : Type u_2
inst✝¹ : RCLike 𝕜
inst✝ : PseudoEMetricSpace E
A : StarSubalgebra 𝕜 (E →ᵇ 𝕜)
g : C(E, ℝ)
x : E →ᵇ 𝕜
hxA : x ∈ A
hxg : (toContinuousMapStarₐ 𝕜) x = (AlgHom.compLeftContinuous ℝ ofRealAm ⋯) g
hg_apply : ∀ (a : E), ((toContinuousMapStarₐ 𝕜) x) a = ((AlgHom.compLeftContinuous ℝ ofRealAm ⋯) g) a
⊢ ∃ x, (AlgHom.compLeftContinuousBounded ℝ ofRealAm ⋯) x ∈ A ∧ (toContinuousMapₐ ℝ) x = g

Tactic:
simp only [toContinuousMapStarₐ_apply_apply, AlgHom.compLeftContinuous_apply_apply,
      ofRealAm_coe] at hg_apply

Goal state after:
case mpr
𝕜 : Type u_1
E : Type u_2
inst✝¹ : RCLike 𝕜
inst✝ : PseudoEMetricSpace E
A : StarSubalgebra 𝕜 (E →ᵇ 𝕜)
g : C(E, ℝ)
x : E →ᵇ 𝕜
hxA : x ∈ A
hxg : (toContinuousMapStarₐ 𝕜) x = (AlgHom.compLeftContinuous ℝ ofRealAm ⋯) g
hg_apply : ∀ (a : E), x a = ↑(g a)
⊢ ∃ x, (AlgHom.compLeftContinuousBounded ℝ ofRealAm ⋯) x ∈ A ∧ (toContinuousMapₐ ℝ) x = g
Module: Mathlib.Analysis.Polynomial.MahlerMeasure

Goal state before:
pp: p q : ℂ[X]
hpq : ¬p = 0 ∧ ¬q = 0
a✝ : ℂ
w✝ : ℝ
right✝ : circleMap 0 1 w✝ = a✝
left✝ : w✝ ∈ Set.uIoc 0 (2 * π)
h :
  ¬log (‖eval (circleMap 0 1 w✝) p‖ * ‖eval (circleMap 0 1 w✝) q‖) =
      log ‖eval (circleMap 0 1 w✝) p‖ + log ‖eval (circleMap 0 1 w✝) q‖
⊢ a✝ ∈ {x | x ∈ (p * q).roots}

Tactic:
contrapose h

Goal state after:
p q : ℂ[X]
hpq : ¬p = 0 ∧ ¬q = 0
a✝ : ℂ
w✝ : ℝ
right✝ : circleMap 0 1 w✝ = a✝
left✝ : w✝ ∈ Set.uIoc 0 (2 * π)
h : a✝ ∉ {x | x ∈ (p * q).roots}
⊢ log (‖eval (circleMap 0 1 w✝) p‖ * ‖eval (circleMap 0 1 w✝) q‖) =
    log ‖eval (circleMap 0 1 w✝) p‖ + log ‖eval (circleMap 0 1 w✝) q‖
Module: Mathlib.Analysis.Rat.NatSqrt.Real

Goal state before:
pp: x prec : ℕ
h : 0 < prec
⊢ √↑x < ↑(x.ratSqrt prec) + 1 / ↑prec

Tactic:
by
  have := lt_ratSqrt_add_inv_prec_sq (x := x) h
  have : (x : ℝ) < ↑((x.ratSqrt prec + 1 / prec) ^ 2 : ℚ) := by norm_cast
  have := Real.sqrt_lt_sqrt (by simp) this
  rw [Rat.cast_pow, Real.sqrt_sq] at this
  · push_cast at this
    exact this
  · push_cast
    exact add_nonneg (by simpa using ratSqrt_nonneg _ _) (by simp)

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

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

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

pp: n : ℕ
a : ℝ
h : 2 - ((a - 1 / 4 ^ n) / 2 ^ (n + 1)) ^ 2 ≤ (↑0 / ↑1).sqrtTwoAddSeries n
h₂ : 1 / 4 ^ n ≤ a
⊢ 0 < 2 ^ (n + 1)

Tactic:
sub_le_comm

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

n : ℕ
a : ℝ
h : 2 - ((a - 1 / 4 ^ n) / 2 ^ (n + 1)) ^ 2 ≤ (↑0 / ↑1).sqrtTwoAddSeries n
h₂ : 1 / 4 ^ n ≤ a
⊢ 0 ≤ (a - 1 / 4 ^ n) / 2 ^ (n + 1)

n : ℕ
a : ℝ
h : 2 - ((a - 1 / 4 ^ n) / 2 ^ (n + 1)) ^ 2 ≤ (↑0 / ↑1).sqrtTwoAddSeries n
h₂ : 1 / 4 ^ n ≤ a
⊢ 0 < 2 ^ (n + 1)
Module: Mathlib.Analysis.Real.Hyperreal

Goal state before:
pp: x : ℝ*
r : ℝ
⊢ Germ.Tendsto x (𝓝 r) ↔ (∀ s < r, ↑s ≤ x) ∧ ∀ s > r, x ≤ ↑s

Tactic:
rcases ofSeq_surjective x with ⟨f, rfl⟩
  rw [tendsto_ofSeq, (nhds_basis_Ioo _).tendsto_right_iff]
  simp_rw [Set.mem_Ioo, eventually_and, ← ofSeq_lt_ofSeq]
  refine ⟨fun H ↦ ⟨fun s hs ↦ ?_, fun s hs ↦ ?_⟩, fun H ⟨s, t⟩ ⟨hs, ht⟩ ↦ ⟨?_, ?_⟩⟩
  · obtain ⟨t, ht⟩ := exists_gt r
    exact (H ⟨s, t⟩ ⟨hs, ht⟩).1.le
  · obtain ⟨t, ht⟩ := exists_lt r
    exact (H ⟨t, s⟩ ⟨ht, hs⟩).2.le
  · obtain ⟨u, hu, hu'⟩ := exists_between hs
    exact (coe_lt_coe.2 hu).trans_le (H.1 _ hu')
  · obtain ⟨u, hu, hu'⟩ := exists_between ht
    exact (H.2 _ hu).trans_lt (coe_lt_coe.2 hu')

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

Goal state before:
pp: x : ℝ*
hx : Germ.Tendsto x (𝓝 0)
⊢ 0 < ArchimedeanClass.mk x

Tactic:
by
  apply (archimedeanClassMk_nonneg_of_tendsto hx).lt_of_ne'
  rw [← stdPart_eq_zero, stdPart_of_tendsto hx]

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

Goal state before:
pp: case inl
x : ℝ*
h0 : x ≠ 0
hi : x⁻¹.Infinitesimal
hn : x < 0
⊢ x.Infinite

pp: case inr
x : ℝ*
h0 : x ≠ 0
hi : x⁻¹.Infinitesimal
hp : 0 < x
⊢ x.Infinite

Tactic:
· exact Or.inr (infiniteNeg_iff_infinitesimal_inv_neg.mpr ⟨hi, inv_lt_zero.mpr hn⟩)

Goal state after:
case inr
x : ℝ*
h0 : x ≠ 0
hi : x⁻¹.Infinitesimal
hp : 0 < x
⊢ x.Infinite
Module: Mathlib.Analysis.SpecialFunctions.Arcosh

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

Tactic:
apply log_pos

Goal state after:
x : ℝ
hx : 1 < x
⊢ 1 < x + √(x ^ 2 - 1)
Module: Mathlib.Analysis.SpecialFunctions.CompareExp

Goal state before:
pp: l : Filter ℂ
hl : IsExpCmpFilter l
n : ℕ
⊢ (fun z ↦ |z.im| ^ n) ≤ᶠ[l] fun z ↦ Real.exp z.re

Tactic:
by
  simpa using! (hl.isLittleO_im_pow_exp_re n).bound zero_lt_one

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

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

Tactic:
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.Gaussian.PoissonSummation

Goal state before:
pp: a : ℝ
ha : a < 0
b s : ℝ
⊢ (fun x ↦ -x - (a * x ^ 2 + b * x)) = fun x ↦ x * (-a * x - (b + 1))

Tactic:
ext1 x

Goal state after:
a : ℝ
ha : a < 0
b s x : ℝ
⊢ -x - (a * x ^ 2 + b * x) = x * (-a * x - (b + 1))
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 : ℕ
hb : b ≤ 1
r : R
h : r ≤ 1
⊢ log b r = 0

Tactic:
rw [log_of_right_le_one _ h, Nat.clog_of_left_le_one hb, Int.ofNat_zero, neg_zero]

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

Goal state before:
pp: case neg
R : Type u_1
inst✝² : Semifield R
inst✝¹ : LinearOrder R
inst✝ : FloorSemiring R
r : R
hr : ¬1 ≤ r
⊢ log 1 r = 0

Tactic:
simp only [log, Nat.log_one_left, Nat.cast_zero, Nat.clog_one_left, neg_zero, ite_self]

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

Goal state before:
pp: b✝ b : ℝ
hb : b ≠ -1 ∧ b ≠ 0 ∧ b ≠ 1
hb₀ : 0 < b
this : ∀ {b : ℝ}, b ≠ -1 ∧ b ≠ 0 ∧ b ≠ 1 → 0 < b → 1 < b → Tendsto (fun x ↦ |logb b x|) atTop atTop
hb₁ : ¬1 < b
⊢ b⁻¹ ≠ -1 ∧ b⁻¹ ≠ 0 ∧ b⁻¹ ≠ 1

Tactic:
by simp [hb, inv_eq_iff_eq_inv, inv_neg]

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

Goal state before:
pp: P : ℝ → Prop
x₀ r : ℝ
hr : 1 < r
hx₀ : 0 < x₀
base : ∀ x ∈ Ico x₀ (r * x₀), P x
step : ∀ n ≥ 1, (∀ z ∈ Ico x₀ (r ^ n * x₀), P z) → ∀ z ∈ Ico (r ^ n * x₀) (r ^ (n + 1) * x₀), P z
this : ∀ (n : ℕ), ∀ x ∈ Ico x₀ (r ^ (n + 1) * x₀), P x
x : ℝ
hx : x ≥ x₀
hx' : 0 < x / x₀
⊢ x₀ ≤ x ∧ x / x₀ < r ^ (⌊logb r (x / x₀)⌋₊ + 1)

Tactic:
← rpow_natCast,

Goal state after:
P : ℝ → Prop
x₀ r : ℝ
hr : 1 < r
hx₀ : 0 < x₀
base : ∀ x ∈ Ico x₀ (r * x₀), P x
step : ∀ n ≥ 1, (∀ z ∈ Ico x₀ (r ^ n * x₀), P z) → ∀ z ∈ Ico (r ^ n * x₀) (r ^ (n + 1) * x₀), P z
this : ∀ (n : ℕ), ∀ x ∈ Ico x₀ (r ^ (n + 1) * x₀), P x
x : ℝ
hx : x ≥ x₀
hx' : 0 < x / x₀
⊢ x₀ ≤ x ∧ x / x₀ < r ^ ↑(⌊logb r (x / x₀)⌋₊ + 1)
Module: Mathlib.MeasureTheory.Measure.RegularityCompacts

Goal state before:
pp: case refine_1
α : Type u_1
inst✝⁵ : MeasurableSpace α
inst✝⁴ : TopologicalSpace α
inst✝³ : SecondCountableTopology α
inst✝² : IsCompletelyPseudoMetrizableSpace α
inst✝¹ : BorelSpace α
P : Measure α
inst✝ : IsFiniteMeasure P
⊢ P.InnerRegularWRT (fun s ↦ IsCompact s ∧ IsClosed s) IsOpen

pp: case refine_2
α : Type u_1
inst✝⁵ : MeasurableSpace α
inst✝⁴ : TopologicalSpace α
inst✝³ : SecondCountableTopology α
inst✝² : IsCompletelyPseudoMetrizableSpace α
inst✝¹ : BorelSpace α
P : Measure α
inst✝ : IsFiniteMeasure P
⊢ ∀ ⦃s U : Set α⦄, IsCompact s ∧ IsClosed s → IsOpen U → IsCompact (s \ U) ∧ IsClosed (s \ U)

Tactic:
· exact innerRegularWRT_isCompact_isClosed_isOpen P

Goal state after:
case refine_2
α : Type u_1
inst✝⁵ : MeasurableSpace α
inst✝⁴ : TopologicalSpace α
inst✝³ : SecondCountableTopology α
inst✝² : IsCompletelyPseudoMetrizableSpace α
inst✝¹ : BorelSpace α
P : Measure α
inst✝ : IsFiniteMeasure P
⊢ ∀ ⦃s U : Set α⦄, IsCompact s ∧ IsClosed s → IsOpen U → IsCompact (s \ U) ∧ IsClosed (s \ U)
Module: Mathlib.Analysis.SpecialFunctions.Pochhammer

Goal state before:
pp: case h0
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 : ℕ
hi : i ∈ Finset.range (n + 1)
j : ℕ
⊢ j ∈ (Finset.range (n + 1)).erase i → 0 ≤ a - ↑j

Tactic:
hj

Goal state after:
case h0
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 : ℕ
hi : i ∈ Finset.range (n + 1)
j : ℕ
hj : j ∈ (Finset.range (n + 1)).erase i
⊢ 0 ≤ a - ↑j
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.InverseDeriv

Goal state before:
pp: x : ℝ
n : ℕ∞ω
⊢ ContDiffAt ℝ n arccos x ↔ n = 0 ∨ x ≠ -1 ∧ x ≠ 1

Tactic:
refine Iff.trans ⟨fun h => ?_, fun h => ?_⟩ contDiffAt_arcsin_iff <;>
    simpa [arccos] using! (contDiffAt_const (c := π / 2)).sub h

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

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

Tactic:
measureT,

Goal state after:
f : ℝ → ℝ
⊢ (∫ (x : ℝ) in Set.Ioc (-1) 1, f x ∂volume.withDensity fun x ↦ ↑(NNReal.mk √(1 - x ^ 2)⁻¹ ⋯)) =
    ∫ (x : ℝ) in Set.Ioc (-1) 1, f x * √(1 - x ^ 2)⁻¹ ∂volume
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Orthogonality

Goal state before:
pp: f : ℝ → ℝ
hf : ContinuousOn f (Set.uIcc (-1) 1)
this : IntegrableOn (fun x ↦ f x * √(1 - x ^ 2)⁻¹) (Set.Ioc (-1) 1) volume
⊢ Integrable f measureT

Tactic:
measureT,

Goal state after:
f : ℝ → ℝ
hf : ContinuousOn f (Set.uIcc (-1) 1)
this : IntegrableOn (fun x ↦ f x * √(1 - x ^ 2)⁻¹) (Set.Ioc (-1) 1) volume
⊢ Integrable f ((volume.withDensity fun x ↦ ↑(NNReal.mk √(1 - x ^ 2)⁻¹ ⋯)).restrict (Set.Ioc (-1) 1))
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.ChebyshevGauss

Goal state before:
pp: n : ℕ
ι : Type u_1
s : Finset ι
P : ι → ℝ[X]
⊢ π / ↑n * ∑ x ∈ range n, ∑ i ∈ s, eval (cos ((2 * ↑x + 1) / (2 * ↑n) * π)) (P i) =
    ∑ i ∈ s, π / ↑n * ∑ i_1 ∈ range n, eval (cos ((2 * ↑i_1 + 1) / (2 * ↑n) * π)) (P i)

Tactic:
rw [sum_comm, mul_sum]

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

Goal state before:
pp: case degree_g_lt
n : ℕ
c : ℕ → ℝ
hcpos : ∀ i ≤ n, 0 < (-1) ^ i * c i
P : ℝ[X]
hPdeg : P.degree ≤ ↑n
hPbnd : ∀ x ∈ Set.Icc (-1) 1, |eval x P| ≤ 1
h : ∑ i ≤ n, eval (node n i) P * c i = ∑ i ≤ n, eval (node n i) (T ℝ ↑n) * c i
⊢ ↑(↑n).natAbs < ↑(Finset.image (fun x ↦ node n x) (Finset.range (n + 1))).card

Tactic:
Int.natAbs_natCast,

Goal state after:
case degree_g_lt
n : ℕ
c : ℕ → ℝ
hcpos : ∀ i ≤ n, 0 < (-1) ^ i * c i
P : ℝ[X]
hPdeg : P.degree ≤ ↑n
hPbnd : ∀ x ∈ Set.Icc (-1) 1, |eval x P| ≤ 1
h : ∑ i ≤ n, eval (node n i) P * c i = ∑ i ≤ n, eval (node n i) (T ℝ ↑n) * c i
⊢ ↑n < ↑(Finset.image (fun x ↦ node n x) (Finset.range (n + 1))).card
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal

Goal state before:
pp: n : ℕ
P : ℝ[X]
hP : P.degree ≤ ↑n
this : P.degree < ↑(Finset.range (n + 1)).card
⊢ ∑ i ≤ n, eval (node n i) P * (∏ j ∈ (Finset.range (n + 1)).erase i, (node n i - node n j))⁻¹ = P.coeff n

Tactic:
convert! (Lagrange.coeff_eq_sum (strictAntiOn_node n).injOn this).symm using 2

Goal state after:
case e'_2.h
n : ℕ
P : ℝ[X]
hP : P.degree ≤ ↑n
this : P.degree < ↑(Finset.range (n + 1)).card
⊢ Finset.Iic n = Finset.range (n + 1)

case e'_3.e'_4
n : ℕ
P : ℝ[X]
hP : P.degree ≤ ↑n
this : P.degree < ↑(Finset.range (n + 1)).card
⊢ n = (Finset.range (n + 1)).card - 1
Module: Mathlib.Order.Interval.Finset.Box

Goal state before:
pp: α : Type u_1
inst✝³ : Ring α
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
⊢ box 0 = {0}

Tactic:
by simp [box]

Goal state after:
Module: Mathlib.Order.Interval.Finset.Box

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹⁰ : Ring α
inst✝⁹ : PartialOrder α
inst✝⁸ : IsOrderedRing α
inst✝⁷ : Ring β
inst✝⁶ : PartialOrder β
inst✝⁵ : IsOrderedRing β
inst✝⁴ : LocallyFiniteOrder α
inst✝³ : LocallyFiniteOrder β
inst✝² : DecidableEq α
inst✝¹ : DecidableEq β
inst✝ : DecidableLE (α × β)
n : ℕ
⊢ #(box (n + 1)) = #(Icc (-↑n.succ) ↑n.succ) * #(Icc (-↑n.succ) ↑n.succ) - #(Icc (-↑n) ↑n) * #(Icc (-↑n) ↑n)

Tactic:
rw [box_succ_eq_sdiff, card_sdiff_of_subset (Icc_neg_mono n.le_succ), Finset.card_Icc_prod,
    Finset.card_Icc_prod]

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹⁰ : Ring α
inst✝⁹ : PartialOrder α
inst✝⁸ : IsOrderedRing α
inst✝⁷ : Ring β
inst✝⁶ : PartialOrder β
inst✝⁵ : IsOrderedRing β
inst✝⁴ : LocallyFiniteOrder α
inst✝³ : LocallyFiniteOrder β
inst✝² : DecidableEq α
inst✝¹ : DecidableEq β
inst✝ : DecidableLE (α × β)
n : ℕ
⊢ #(Icc (-↑n.succ).1 (↑n.succ).1) * #(Icc (-↑n.succ).2 (↑n.succ).2) - #(Icc (-↑n).1 (↑n).1) * #(Icc (-↑n).2 (↑n).2) =
    #(Icc (-↑n.succ) ↑n.succ) * #(Icc (-↑n.succ) ↑n.succ) - #(Icc (-↑n) ↑n) * #(Icc (-↑n) ↑n)
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: case neg
L : PeriodPair
i : ℕ
hi₁ : i < 7
hi₂ : ¬Odd i
hi₃ : ¬i = 0
⊢ iteratedDeriv i (L.relation * id ^ 6) 0 = 0

Tactic:
by_cases hi₄ : i = 6

Goal state after:
case pos
L : PeriodPair
i : ℕ
hi₁ : i < 7
hi₂ : ¬Odd i
hi₃ : ¬i = 0
hi₄ : i = 6
⊢ iteratedDeriv i (L.relation * id ^ 6) 0 = 0

case neg
L : PeriodPair
i : ℕ
hi₁ : i < 7
hi₂ : ¬Odd i
hi₃ : ¬i = 0
hi₄ : ¬i = 6
⊢ iteratedDeriv i (L.relation * id ^ 6) 0 = 0
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema

Goal state before:
pp: n : ℕ
x : ℝ
hroot : x ∈ Finset.image (fun k ↦ cos ((2 * ↑k + 1) * π / (2 * ↑n))) (Finset.range n)
hnz : x ≠ 0
k : ℕ
hk₁ : k ∈ Finset.range n
hk₂ : cos ((2 * ↑k + 1) * π / (2 * ↑n)) = x
hn : n ≠ 0
this : Irrational (cos (↑(Rat.divInt (2 * ↑k + 1) (2 * ↑n)) * π))
⊢ Irrational x

Tactic:
rw [← hk₂]; convert! this using 2; push_cast; field_simp

Goal state after:
Module: Mathlib.Analysis.SumIntegralComparisons

Goal state before:
pp: a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc ↑a ↑b)
⊢ ∑ x ∈ Finset.Ico 0 (b - a), f ↑(a + x + 1) ≤ ∫ (x : ℝ) in ↑a..↑a + ↑(b - a), f x

Tactic:
Nat.Ico_zero_eq_range,

Goal state after:
a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc ↑a ↑b)
⊢ ∑ x ∈ Finset.range (b - a), f ↑(a + x + 1) ≤ ∫ (x : ℝ) in ↑a..↑a + ↑(b - a), f x
Module: Mathlib.Analysis.SpecificLimits.FloorPow

Goal state before:
pp: u : ℕ → ℝ
l : ℝ
hmono : Monotone u
hlim :
  ∀ (a : ℝ),
    1 < a →
      ∃ c,
        (∀ᶠ (n : ℕ) in atTop, ↑(c (n + 1)) ≤ a * ↑(c n)) ∧
          Tendsto c atTop atTop ∧ Tendsto (fun n ↦ u (c n) / ↑(c n)) atTop (𝓝 l)
lnonneg : 0 ≤ l
A : ∀ (ε : ℝ), 0 < ε → ∀ᶠ (n : ℕ) in atTop, u n - ↑n * l ≤ ε * (1 + ε + l) * ↑n
ε : ℝ
εpos : 0 < ε
c : ℕ → ℕ
cgrowth : ∀ᶠ (n : ℕ) in atTop, ↑(c (n + 1)) ≤ (1 + ε) * ↑(c n)
ctop : Tendsto c atTop atTop
clim : Tendsto (fun n ↦ u (c n) / ↑(c n)) atTop (𝓝 l)
L : ∀ᶠ (n : ℕ) in atTop, ↑(c n) * l - u (c n) ≤ ε * ↑(c n)
a : ℕ
ha : ∀ (b : ℕ), a ≤ b → ↑(c (b + 1)) ≤ (1 + ε) * ↑(c b) ∧ ↑(c b) * l - u (c b) ≤ ε * ↑(c b)
M : ℕ := (image (fun i ↦ c i) (range (a + 1))).max' ⋯
n : ℕ
hn : n ∈ Set.Ici M
exN : ∃ N, n < c N
N : ℕ := Nat.find exN
ncN : n < c N
aN : a + 1 ≤ N
Npos : 0 < N
⊢ ↑n * l - u n ≤ ε * (1 + l) * ↑n

Tactic:
have aN' : a ≤ N - 1 := (Nat.le_sub_one_iff_lt Npos).mpr aN

Goal state after:
u : ℕ → ℝ
l : ℝ
hmono : Monotone u
hlim :
  ∀ (a : ℝ),
    1 < a →
      ∃ c,
        (∀ᶠ (n : ℕ) in atTop, ↑(c (n + 1)) ≤ a * ↑(c n)) ∧
          Tendsto c atTop atTop ∧ Tendsto (fun n ↦ u (c n) / ↑(c n)) atTop (𝓝 l)
lnonneg : 0 ≤ l
A : ∀ (ε : ℝ), 0 < ε → ∀ᶠ (n : ℕ) in atTop, u n - ↑n * l ≤ ε * (1 + ε + l) * ↑n
ε : ℝ
εpos : 0 < ε
c : ℕ → ℕ
cgrowth : ∀ᶠ (n : ℕ) in atTop, ↑(c (n + 1)) ≤ (1 + ε) * ↑(c n)
ctop : Tendsto c atTop atTop
clim : Tendsto (fun n ↦ u (c n) / ↑(c n)) atTop (𝓝 l)
L : ∀ᶠ (n : ℕ) in atTop, ↑(c n) * l - u (c n) ≤ ε * ↑(c n)
a : ℕ
ha : ∀ (b : ℕ), a ≤ b → ↑(c (b + 1)) ≤ (1 + ε) * ↑(c b) ∧ ↑(c b) * l - u (c b) ≤ ε * ↑(c b)
M : ℕ := (image (fun i ↦ c i) (range (a + 1))).max' ⋯
n : ℕ
hn : n ∈ Set.Ici M
exN : ∃ N, n < c N
N : ℕ := Nat.find exN
ncN : n < c N
aN : a + 1 ≤ N
Npos : 0 < N
aN' : a ≤ N - 1
⊢ ↑n * l - u n ≤ ε * (1 + l) * ↑n
Module: Mathlib.Analysis.SpecificLimits.FloorPow

Goal state before:
pp: case refine_1
u : ℕ → ℝ
l : ℝ
hmono : Monotone u
c : ℕ → ℝ
cone : ∀ (k : ℕ), 1 < c k
clim : Tendsto c atTop (𝓝 1)
hc : ∀ (k : ℕ), Tendsto (fun n ↦ u ⌊c k ^ n⌋₊ / ↑⌊c k ^ n⌋₊) atTop (𝓝 l)
a : ℝ
ha : 1 < a
k : ℕ
hk : c k < a
H : ∀ (n : ℕ), 0 < ↑⌊c k ^ n⌋₊
⊢ Tendsto (fun n ↦ ↑⌊c k ^ (n + 1)⌋₊ / c k ^ (n + 1)) atTop (𝓝 1)

Tactic:
refine tendsto_nat_floor_div_atTop.comp ?_

Goal state after:
case refine_1
u : ℕ → ℝ
l : ℝ
hmono : Monotone u
c : ℕ → ℝ
cone : ∀ (k : ℕ), 1 < c k
clim : Tendsto c atTop (𝓝 1)
hc : ∀ (k : ℕ), Tendsto (fun n ↦ u ⌊c k ^ n⌋₊ / ↑⌊c k ^ n⌋₊) atTop (𝓝 l)
a : ℝ
ha : 1 < a
k : ℕ
hk : c k < a
H : ∀ (n : ℕ), 0 < ↑⌊c k ^ n⌋₊
⊢ Tendsto (fun n ↦ c k ^ (n + 1)) atTop atTop
Module: Mathlib.Analysis.SpecificLimits.FloorPow

Goal state before:
pp: case refine_2
u : ℕ → ℝ
l : ℝ
hmono : Monotone u
c : ℕ → ℝ
cone : ∀ (k : ℕ), 1 < c k
clim : Tendsto c atTop (𝓝 1)
hc : ∀ (k : ℕ), Tendsto (fun n ↦ u ⌊c k ^ n⌋₊ / ↑⌊c k ^ n⌋₊) atTop (𝓝 l)
a : ℝ
ha : 1 < a
k : ℕ
hk : c k < a
H : ∀ (n : ℕ), 0 < ↑⌊c k ^ n⌋₊
⊢ Tendsto (fun n ↦ ↑⌊c k ^ n⌋₊ / c k ^ n) atTop (𝓝 1)

Tactic:
refine tendsto_nat_floor_div_atTop.comp ?_

Goal state after:
case refine_2
u : ℕ → ℝ
l : ℝ
hmono : Monotone u
c : ℕ → ℝ
cone : ∀ (k : ℕ), 1 < c k
clim : Tendsto c atTop (𝓝 1)
hc : ∀ (k : ℕ), Tendsto (fun n ↦ u ⌊c k ^ n⌋₊ / ↑⌊c k ^ n⌋₊) atTop (𝓝 l)
a : ℝ
ha : 1 < a
k : ℕ
hk : c k < a
H : ∀ (n : ℕ), 0 < ↑⌊c k ^ n⌋₊
⊢ Tendsto (HPow.hPow (c k)) atTop atTop
Module: Mathlib.Analysis.SpecificLimits.FloorPow

Goal state before:
pp: u : ℕ → ℝ
l : ℝ
hmono : Monotone u
c : ℕ → ℝ
cone : ∀ (k : ℕ), 1 < c k
clim : Tendsto c atTop (𝓝 1)
hc : ∀ (k : ℕ), Tendsto (fun n ↦ u ⌊c k ^ n⌋₊ / ↑⌊c k ^ n⌋₊) atTop (𝓝 l)
a : ℝ
ha : 1 < a
k : ℕ
hk : c k < a
H : ∀ (n : ℕ), 0 < ↑⌊c k ^ n⌋₊
A : Tendsto (fun n ↦ ↑⌊c k ^ (n + 1)⌋₊ / c k ^ (n + 1) * c k / (↑⌊c k ^ n⌋₊ / c k ^ n)) atTop (𝓝 (1 * c k / 1))
⊢ ∀ᶠ (n : ℕ) in atTop, ↑((fun n ↦ ⌊c k ^ n⌋₊) (n + 1)) ≤ a * ↑((fun n ↦ ⌊c k ^ n⌋₊) n)

Tactic:
have B : Tendsto (fun n : ℕ => (⌊c k ^ (n + 1)⌋₊ : ℝ) / ⌊c k ^ n⌋₊) atTop (𝓝 (c k)) := by
    simp only [one_mul, div_one] at A
    convert! A using 1
    ext1 n
    field [(zero_lt_one.trans (cone k)).ne']

Goal state after:
u : ℕ → ℝ
l : ℝ
hmono : Monotone u
c : ℕ → ℝ
cone : ∀ (k : ℕ), 1 < c k
clim : Tendsto c atTop (𝓝 1)
hc : ∀ (k : ℕ), Tendsto (fun n ↦ u ⌊c k ^ n⌋₊ / ↑⌊c k ^ n⌋₊) atTop (𝓝 l)
a : ℝ
ha : 1 < a
k : ℕ
hk : c k < a
H : ∀ (n : ℕ), 0 < ↑⌊c k ^ n⌋₊
A : Tendsto (fun n ↦ ↑⌊c k ^ (n + 1)⌋₊ / c k ^ (n + 1) * c k / (↑⌊c k ^ n⌋₊ / c k ^ n)) atTop (𝓝 (1 * c k / 1))
B : Tendsto (fun n ↦ ↑⌊c k ^ (n + 1)⌋₊ / ↑⌊c k ^ n⌋₊) atTop (𝓝 (c k))
⊢ ∀ᶠ (n : ℕ) in atTop, ↑((fun n ↦ ⌊c k ^ n⌋₊) (n + 1)) ≤ a * ↑((fun n ↦ ⌊c k ^ n⌋₊) n)