mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Normed.Order.UpperLower

Goal state before:
pp: ι : Type u_2
inst✝ : Finite ι
s : Set (ι → ℝ)
x y : ι → ℝ
hs : IsLowerSet s
hx : x ∈ closure s
h : ∀ (i : ι), y i < x i
val✝ : Fintype ι
ε : ℝ
hε : 0 < ε
hxy : ∀ (i : ι), y i + ε < x i
z : ι → ℝ
hz : z ∈ s
hxz : ∀ (b : ι), dist (x b) (z b) < ε
i : ι
⊢ dist (x i) (z i) ≤ ε

Tactic:
exact (hxz _).le

Goal state after:
Module: Mathlib.Topology.MetricSpace.Contracting

Goal state before:
pp: α : Type u_1
inst✝ : EMetricSpace α
K : ℝ≥0
f : α → α
hf : ContractingWith K f
x y : α
h : edist x y ≠ ∞
this : edist x y ≤ edist x (f x) + edist y (f y) + ↑K * edist x y
⊢ (1 - ↑K) * edist x y ≤ edist x (f x) + edist y (f y)

Tactic:
ENNReal.sub_mul fun _ _ ↦ h,

Goal state after:
α : Type u_1
inst✝ : EMetricSpace α
K : ℝ≥0
f : α → α
hf : ContractingWith K f
x y : α
h : edist x y ≠ ∞
this : edist x y ≤ edist x (f x) + edist y (f y) + ↑K * edist x y
⊢ 1 * edist x y - ↑K * edist x y ≤ edist x (f x) + edist y (f y)
Module: Mathlib.Analysis.ODE.PicardLindelof

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E → E
tmin tmax : ℝ
t₀ : ↑(Icc tmin tmax)
x₀ x : E
a r L K : ℝ≥0
hf : IsPicardLindelof f t₀ x₀ a r L K
hx : x ∈ closedBall x₀ ↑r
n : ℕ
t : ↑(Icc tmin tmax)
α β : FunSpace t₀ x₀ r L
h : dist (((next hf hx)^[n] α).toFun t) (((next hf hx)^[n] β).toFun t) ≤ (↑K * |↑t - ↑t₀|) ^ n / ↑n ! * dist α β
⊢ ↑K * dist (((next hf hx)^[n] α).toFun t) (((next hf hx)^[n] β).toFun t) ≤
    ↑K ^ (n + 1) * |↑t - ↑t₀| ^ n / ↑n ! * dist α β

Tactic:
rw [pow_succ', mul_assoc, mul_div_assoc, mul_assoc]
      gcongr
      rwa [← mul_pow]

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
tmin tmax : ℝ
t₀ : ↑(Icc tmin tmax)
x₀ x : E
a r L K : ℝ≥0
hf : IsPicardLindelof f t₀ x₀ a r L K
hx : x ∈ closedBall x₀ ↑r
α β : FunSpace t₀ x₀ r L
n : ℕ
hn :
  ∀ (t : ↑(Icc tmin tmax)),
    dist (((next hf hx)^[n] α).toFun t) (((next hf hx)^[n] β).toFun t) ≤ (↑K * |↑t - ↑t₀|) ^ n / ↑n ! * dist α β
t : ↑(Icc tmin tmax)
⊢ ↑K ^ (n + 1) * |↑t - ↑t₀| ^ (n + 1) / |↑n.succ * ↑n !| * dist α β ≤ (↑K * |↑t - ↑t₀|) ^ (n + 1) / ↑(n + 1)! * dist α β

Tactic:
← Nat.cast_mul,

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E → E
tmin tmax : ℝ
t₀ : ↑(Icc tmin tmax)
x₀ x : E
a r L K : ℝ≥0
hf : IsPicardLindelof f t₀ x₀ a r L K
hx : x ∈ closedBall x₀ ↑r
α β : FunSpace t₀ x₀ r L
n : ℕ
hn :
  ∀ (t : ↑(Icc tmin tmax)),
    dist (((next hf hx)^[n] α).toFun t) (((next hf hx)^[n] β).toFun t) ≤ (↑K * |↑t - ↑t₀|) ^ n / ↑n ! * dist α β
t : ↑(Icc tmin tmax)
⊢ ↑K ^ (n + 1) * |↑t - ↑t₀| ^ (n + 1) / |↑(n.succ * n !)| * dist α β ≤
    (↑K * |↑t - ↑t₀|) ^ (n + 1) / ↑(n + 1)! * dist α β
Module: Mathlib.Analysis.ODE.PicardLindelof

Goal state before:
pp: case succ
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E → E
tmin tmax : ℝ
t₀ : ↑(Icc tmin tmax)
x₀ x : E
a r L K : ℝ≥0
hf : IsPicardLindelof f t₀ x₀ a r L K
hx : x ∈ closedBall x₀ ↑r
α β : FunSpace t₀ x₀ r L
n : ℕ
hn :
  ∀ (t : ↑(Icc tmin tmax)),
    dist (((next hf hx)^[n] α).toFun t) (((next hf hx)^[n] β).toFun t) ≤ (↑K * |↑t - ↑t₀|) ^ n / ↑n ! * dist α β
t : ↑(Icc tmin tmax)
⊢ dist (((next hf hx)^[n + 1] α).toFun t) (((next hf hx)^[n + 1] β).toFun t) ≤
    (↑K * |↑t - ↑t₀|) ^ (n + 1) / ↑(n + 1)! * dist α β

Tactic:
rw [iterate_succ_apply', iterate_succ_apply', dist_eq_norm, next_apply,
      next_apply, picard_apply, picard_apply, add_sub_add_left_eq_sub,
      ← intervalIntegral.integral_sub (intervalIntegrable_comp_compProj hf _ t)
        (intervalIntegrable_comp_compProj hf _ t)]
    calc
      _ ≤ ∫ τ in uIoc t₀.1 t.1, K ^ (n + 1) * |τ - t₀| ^ n / n ! * dist α β := by
        rw [intervalIntegral.norm_intervalIntegral_eq]
        apply MeasureTheory.norm_integral_le_of_norm_le (Continuous.integrableOn_uIoc (by fun_prop))
        apply ae_restrict_mem measurableSet_Ioc |>.mono
        intro t' ht'
        -- Can `grind` do this in the future?
        have ht' : t' ∈ Icc tmin tmax :=
          subset_trans uIoc_subset_uIcc (uIcc_subset_Icc t₀.2 t.2) ht'
        rw [← dist_eq_norm, compProj_of_mem, compProj_of_mem]
        exact dist_comp_iterate_next_le hf hx _ ⟨t', ht'⟩ (hn _)
      _ ≤ (K * |t.1 - t₀.1|) ^ (n + 1) / (n + 1) ! * dist α β := by
        apply le_of_abs_le
        -- critical: `integral_pow_abs_sub_uIoc`
        rw [← intervalIntegral.abs_intervalIntegral_eq, intervalIntegral.integral_mul_const,
          intervalIntegral.integral_div, intervalIntegral.integral_const_mul, abs_mul, abs_div,
          abs_mul, intervalIntegral.abs_intervalIntegral_eq, integral_pow_abs_sub_uIoc, abs_div,
          abs_pow, abs_pow, abs_dist, NNReal.abs_eq, abs_abs, mul_div, div_div, ← abs_mul,
          ← Nat.cast_succ, ← Nat.cast_mul, ← Nat.factorial_succ, Nat.abs_cast, ← mul_pow]

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝³ : NormedField 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
⊢ (fun x ↦ eval x P / eval x Q) ~[atTop] fun x ↦ P.leadingCoeff / Q.leadingCoeff * x ^ (↑P.natDegree - ↑Q.natDegree)

Tactic:
by_cases hP : P = 0

Goal state after:
case pos
𝕜 : Type u_1
inst✝³ : NormedField 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
hP : P = 0
⊢ (fun x ↦ eval x P / eval x Q) ~[atTop] fun x ↦ P.leadingCoeff / Q.leadingCoeff * x ^ (↑P.natDegree - ↑Q.natDegree)

case neg
𝕜 : Type u_1
inst✝³ : NormedField 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
hP : ¬P = 0
⊢ (fun x ↦ eval x P / eval x Q) ~[atTop] fun x ↦ P.leadingCoeff / Q.leadingCoeff * x ^ (↑P.natDegree - ↑Q.natDegree)
Module: Mathlib.Analysis.Polynomial.Basic

Goal state before:
pp: 𝕜 : Type u_1
inst✝³ : NormedField 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
hdeg : P.degree < Q.degree
⊢ Tendsto (fun x ↦ eval x P / eval x Q) atTop (𝓝 0)

Tactic:
by_cases hP : P = 0

Goal state after:
case pos
𝕜 : Type u_1
inst✝³ : NormedField 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
hdeg : P.degree < Q.degree
hP : P = 0
⊢ Tendsto (fun x ↦ eval x P / eval x Q) atTop (𝓝 0)

case neg
𝕜 : Type u_1
inst✝³ : NormedField 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
hdeg : P.degree < Q.degree
hP : ¬P = 0
⊢ Tendsto (fun x ↦ eval x P / eval x Q) atTop (𝓝 0)
Module: Mathlib.Analysis.Polynomial.Basic

Goal state before:
pp: 𝕜 : Type u_1
inst✝³ : NormedField 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
⊢ (fun x ↦ eval x P / eval x Q) ~[atBot] fun x ↦ P.leadingCoeff / Q.leadingCoeff * x ^ (↑P.natDegree - ↑Q.natDegree)

Tactic:
by_cases hP : P = 0

Goal state after:
case pos
𝕜 : Type u_1
inst✝³ : NormedField 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
hP : P = 0
⊢ (fun x ↦ eval x P / eval x Q) ~[atBot] fun x ↦ P.leadingCoeff / Q.leadingCoeff * x ^ (↑P.natDegree - ↑Q.natDegree)

case neg
𝕜 : Type u_1
inst✝³ : NormedField 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
hP : ¬P = 0
⊢ (fun x ↦ eval x P / eval x Q) ~[atBot] fun x ↦ P.leadingCoeff / Q.leadingCoeff * x ^ (↑P.natDegree - ↑Q.natDegree)
Module: Mathlib.Analysis.Polynomial.Basic

Goal state before:
pp: R : Type u_2
inst✝¹ : NormedRing R
inst✝ : NormMulClass R
P Q : R[X]
h : P.degree < Q.degree
⊢ (fun x ↦ eval x P) =o[cobounded R] fun x ↦ eval x Q

Tactic:
by_cases hP : P = 0

Goal state after:
case pos
R : Type u_2
inst✝¹ : NormedRing R
inst✝ : NormMulClass R
P Q : R[X]
h : P.degree < Q.degree
hP : P = 0
⊢ (fun x ↦ eval x P) =o[cobounded R] fun x ↦ eval x Q

case neg
R : Type u_2
inst✝¹ : NormedRing R
inst✝ : NormMulClass R
P Q : R[X]
h : P.degree < Q.degree
hP : ¬P = 0
⊢ (fun x ↦ eval x P) =o[cobounded R] fun x ↦ eval x Q
Module: Mathlib.Analysis.ODE.PicardLindelof

Goal state before:
pp: case pos.zero
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℝ → E → E
α : ℝ → E
u : Set E
t₀ tmin tmax : ℝ
ht₀ : t₀ ∈ Icc tmin tmax
hα : ContinuousOn α (Icc tmin tmax)
hmem : ∀ t ∈ Icc tmin tmax, α t ∈ u
x₀ : E
heqon : ∀ t ∈ Icc tmin tmax, α t = picard f t₀ x₀ α t
hlt : tmin < tmax
this : ∀ t ∈ Icc tmin tmax, HasDerivWithinAt (picard f t₀ x₀ α) (f t (α t)) (Icc tmin tmax) t
hf : ContDiffOn ℝ (↑0) (uncurry f) (Icc tmin tmax ×ˢ u)
⊢ ContDiffOn ℝ (↑0) (picard f t₀ x₀ α) (Icc tmin tmax)

Tactic:
simp only [Nat.cast_zero, contDiffOn_zero] at *

Goal state after:
case pos.zero
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℝ → E → E
α : ℝ → E
u : Set E
t₀ tmin tmax : ℝ
ht₀ : t₀ ∈ Icc tmin tmax
hα : ContinuousOn α (Icc tmin tmax)
hmem : ∀ t ∈ Icc tmin tmax, α t ∈ u
x₀ : E
heqon : ∀ t ∈ Icc tmin tmax, α t = picard f t₀ x₀ α t
hlt : tmin < tmax
this : ∀ t ∈ Icc tmin tmax, HasDerivWithinAt (picard f t₀ x₀ α) (f t (α t)) (Icc tmin tmax) t
hf : ContinuousOn (uncurry f) (Icc tmin tmax ×ˢ u)
⊢ ContinuousOn (picard f t₀ x₀ α) (Icc tmin tmax)
Module: Mathlib.Analysis.Polynomial.Order

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

Tactic:
by apply neg_pos.mp; rwa [← eval_neg]

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

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

Tactic:
obtain ⟨k, hk, hsum⟩ := IsNonarchimedean.finset_image_add vZero vNonneg vna
      (fun a ↦ coeff a.1 f * coeff a.2 g) (Finset.antidiagonal t)

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

Goal state before:
pp: case cons.refine_2
α : Type u_5
S : Type u_6
inst✝¹ : LinearOrder S
inst✝ : AddCommMonoid α
g : α → S
ι : Type u_7
s✝ : Finset ι
f : ι → α
na : ∀ (a b : α), g (a + b) ≤ max (g a) (g b)
j : ι
s : Finset ι
hj : j ∉ s
hs✝ : s.Nonempty
IH : ∃ b ∈ s, g (∑ i ∈ s, f i) ≤ g (f b)
h : g (f j) ≤ g (∑ i ∈ s, f i)
⊢ ∃ a ∈ s, g (f j + ∑ i ∈ s, f i) ≤ g (f a)

Tactic:
exact ⟨_, IH.choose_spec.left, (na _ _).trans <|
          ((max_eq_right h).le.trans IH.choose_spec.right)⟩

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

Goal state before:
pp: p : ℂ[X]
hlc : 1 ≤ ‖p.leadingCoeff‖
⊢ (Multiset.map (fun a ↦ max 1 ‖a‖) p.roots).prod ≤ p.mahlerMeasure

Tactic:
by
  rw [← one_mul (Multiset.prod _), mahlerMeasure_eq_leadingCoeff_mul_prod_roots]
  gcongr
  exact zero_le_one.trans <| one_le_prod_max_one_norm_roots p

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

Goal state before:
pp: case hbc
p : ℂ[X]
hp : ¬p = 0
this : 0 < p.sum fun x a ↦ ‖a‖
⊢ ∀ᵐ (x : ℝ) ∂volume.restrict (Icc 0 (2 * π)), log ‖eval (circleMap 0 1 x) p‖ ≤ log (p.sum fun x a ↦ ‖a‖)

Tactic:
eventually_iff_exists_mem

Goal state after:
case hbc
p : ℂ[X]
hp : ¬p = 0
this : 0 < p.sum fun x a ↦ ‖a‖
⊢ ∃ v ∈ ae (volume.restrict (Icc 0 (2 * π))), ∀ y ∈ v, log ‖eval (circleMap 0 1 y) p‖ ≤ log (p.sum fun x a ↦ ‖a‖)
Module: Mathlib.Analysis.Real.OfDigits

Goal state before:
pp: b : ℕ
x y : ℕ → Fin b
n : ℕ
hxy : ∀ i < n, x i = y i
⊢ |ofDigits x - ofDigits y| ≤ (↑b ^ n)⁻¹

Tactic:
rw [ofDigits_eq_sum_add_ofDigits x n, ofDigits_eq_sum_add_ofDigits y n]
  have : ∑ i ∈ Finset.range n, ofDigitsTerm x i = ∑ i ∈ Finset.range n, ofDigitsTerm y i :=
    Finset.sum_congr rfl fun i hi ↦ by simp [ofDigitsTerm, hxy i (Finset.mem_range.mp hi)]
  rw [this, add_sub_add_left_eq_sub, ← mul_sub, abs_mul, abs_of_nonneg (by positivity)]
  apply mul_le_of_le_one_right (by positivity)
  convert!
    abs_sub_le_of_le_of_le (ofDigits_nonneg _) (ofDigits_le_one _) (ofDigits_nonneg _)
      (ofDigits_le_one _)
  simp

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

Goal state before:
pp: case inl
q : ℚ
hq : 0 ≤ q
⊢ ¬IsSquare q ↔ ¬IsSquare q ∧ 0 ≤ q

Tactic:
and_iff_left hq

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

Goal state before:
pp: x : ℝ*
⊢ x.InfinitePos ∨ x.InfiniteNeg ↔ ArchimedeanClass.mk x < 0

Tactic:
infinitePos_iff,

Goal state after:
x : ℝ*
⊢ 0 < x ∧ ArchimedeanClass.mk x < 0 ∨ x.InfiniteNeg ↔ ArchimedeanClass.mk x < 0
Module: Mathlib.Analysis.Real.Hyperreal

Goal state before:
pp: x : ℝ*
⊢ x.InfinitePos ↔ x⁻¹.Infinitesimal ∧ 0 < x⁻¹

Tactic:
infinitePos_iff,

Goal state after:
x : ℝ*
⊢ 0 < x ∧ ArchimedeanClass.mk x < 0 ↔ x⁻¹.Infinitesimal ∧ 0 < x⁻¹
Module: Mathlib.Analysis.Real.Pi.Leibniz

Goal state before:
pp: case h2
l : ℝ
h : Tendsto (fun n ↦ ∑ i ∈ range n, (-1) ^ i / (2 * ↑i + 1)) atTop (𝓝 l)
abel : Tendsto (fun x ↦ ∑' (n : ℕ), (-1) ^ n / (2 * ↑n + 1) * x ^ n) (𝓝[<] 1) (𝓝 l)
m : 𝓝[<] 1 ≤ 𝓝 1
⊢ ∀ᶠ (x : ℝ) in 𝓝[<] 1, x ^ 2 ∈ Set.Iio 1

Tactic:
eventually_iff_exists_mem

Goal state after:
case h2
l : ℝ
h : Tendsto (fun n ↦ ∑ i ∈ range n, (-1) ^ i / (2 * ↑i + 1)) atTop (𝓝 l)
abel : Tendsto (fun x ↦ ∑' (n : ℕ), (-1) ^ n / (2 * ↑n + 1) * x ^ n) (𝓝[<] 1) (𝓝 l)
m : 𝓝[<] 1 ≤ 𝓝 1
⊢ ∃ v ∈ 𝓝[<] 1, ∀ y ∈ v, y ^ 2 ∈ Set.Iio 1
Module: Mathlib.Analysis.Real.Pi.Leibniz

Goal state before:
pp: l : ℝ
h : Tendsto (fun n ↦ ∑ i ∈ range n, (-1) ^ i / (2 * ↑i + 1)) atTop (𝓝 l)
m : 𝓝[<] 1 ≤ 𝓝 1
q : Tendsto (fun x ↦ x ^ 2) (𝓝[<] 1) (𝓝[<] 1)
abel : Tendsto (fun x ↦ ((fun x ↦ ∑' (n : ℕ), (-1) ^ n / (2 * ↑n + 1) * x ^ n) ∘ fun x ↦ x ^ 2) x * x) (𝓝[<] 1) (𝓝 l)
⊢ ∀ᶠ (x : ℝ) in 𝓝 1,
    x ∈ Set.Iio 1 → ((fun x ↦ ∑' (n : ℕ), (-1) ^ n / (2 * ↑n + 1) * x ^ n) ∘ fun x ↦ x ^ 2) x * x = arctan x

Tactic:
Metric.eventually_nhds_iff

Goal state after:
l : ℝ
h : Tendsto (fun n ↦ ∑ i ∈ range n, (-1) ^ i / (2 * ↑i + 1)) atTop (𝓝 l)
m : 𝓝[<] 1 ≤ 𝓝 1
q : Tendsto (fun x ↦ x ^ 2) (𝓝[<] 1) (𝓝[<] 1)
abel : Tendsto (fun x ↦ ((fun x ↦ ∑' (n : ℕ), (-1) ^ n / (2 * ↑n + 1) * x ^ n) ∘ fun x ↦ x ^ 2) x * x) (𝓝[<] 1) (𝓝 l)
⊢ ∃ ε > 0,
    ∀ ⦃y : ℝ⦄,
      dist y 1 < ε →
        y ∈ Set.Iio 1 → ((fun x ↦ ∑' (n : ℕ), (-1) ^ n / (2 * ↑n + 1) * x ^ n) ∘ fun x ↦ x ^ 2) y * y = arctan y
Module: Mathlib.Analysis.Real.Pi.Leibniz

Goal state before:
pp: case right
l : ℝ
h : Tendsto (fun n ↦ ∑ i ∈ range n, (-1) ^ i / (2 * ↑i + 1)) atTop (𝓝 l)
m : 𝓝[<] 1 ≤ 𝓝 1
q : Tendsto (fun x ↦ x ^ 2) (𝓝[<] 1) (𝓝[<] 1)
abel : Tendsto (fun x ↦ ((fun x ↦ ∑' (n : ℕ), (-1) ^ n / (2 * ↑n + 1) * x ^ n) ∘ fun x ↦ x ^ 2) x * x) (𝓝[<] 1) (𝓝 l)
y : ℝ
hy1 : y - 1 < 1 ∧ 1 - y < 1
hy2 : y ∈ Set.Iio 1
⊢ ((fun x ↦ ∑' (n : ℕ), (-1) ^ n / (2 * ↑n + 1) * x ^ n) ∘ fun x ↦ x ^ 2) y * y = arctan y

Tactic:
rw [Set.mem_Iio] at hy2

Goal state after:
case right
l : ℝ
h : Tendsto (fun n ↦ ∑ i ∈ range n, (-1) ^ i / (2 * ↑i + 1)) atTop (𝓝 l)
m : 𝓝[<] 1 ≤ 𝓝 1
q : Tendsto (fun x ↦ x ^ 2) (𝓝[<] 1) (𝓝[<] 1)
abel : Tendsto (fun x ↦ ((fun x ↦ ∑' (n : ℕ), (-1) ^ n / (2 * ↑n + 1) * x ^ n) ∘ fun x ↦ x ^ 2) x * x) (𝓝[<] 1) (𝓝 l)
y : ℝ
hy1 : y - 1 < 1 ∧ 1 - y < 1
hy2 : y < 1
⊢ ((fun x ↦ ∑' (n : ℕ), (-1) ^ n / (2 * ↑n + 1) * x ^ n) ∘ fun x ↦ x ^ 2) y * y = arctan y
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arctan

Goal state before:
pp: x : ℝ
⊢ ↑(Real.arctan x) = (↑x).arctan

Tactic:
conv_rhs => rw [← Real.tan_arctan x]

Goal state after:
x : ℝ
⊢ ↑(Real.arctan x) = (↑(Real.tan (Real.arctan x))).arctan
Module: Mathlib.Analysis.SpecialFunctions.Artanh

Goal state before:
pp: x : ℝ
hx : 0 ≤ x
h✝ : x < 1
⊢ 0 ≤ artanh x

Tactic:
rw [← artanh_zero, artanh_le_artanh_iff (by grind) (by grind)]

Goal state after:
x : ℝ
hx : 0 ≤ x
h✝ : x < 1
⊢ 0 ≤ x
Module: Mathlib.Analysis.SpecialFunctions.Artanh

Goal state before:
pp: x : ℝ
hx : x ≤ 0
h✝ : -1 < x
⊢ artanh x ≤ 0

Tactic:
rw [← artanh_zero, artanh_le_artanh_iff (by grind) (by grind)]

Goal state after:
x : ℝ
hx : x ≤ 0
h✝ : -1 < x
⊢ x ≤ 0
Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean

Goal state before:
pp: x y k : ℝ≥0
⊢ (k * x).agm (k * y) = k * x.agm y

Tactic:
simp_rw [agm, mul_iInf]
  congr! with n
  induction n generalizing x y with
  | zero => simp [← mul_div_assoc, mul_add]
  | succ n ih =>
    rw [agmSequences_succ, ← mul_add, mul_div_assoc, mul_mul_mul_comm,
      ← sq, sqrt_mul, sqrt_sq, ih, agmSequences_succ]

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

Goal state before:
pp: l : Filter ℂ
b₁ b₂ : ℝ
hl : IsExpCmpFilter l
hb : b₁ < b₂
a₁ a₂ z : ℂ
hz : z ≠ 0
⊢ z ^ a₁ * cexp (↑b₁ * z) = z ^ a₂ * z ^ (a₁ - a₂) * cexp (↑b₁ * z)

Tactic:
← cpow_add _ _ hz,

Goal state after:
l : Filter ℂ
b₁ b₂ : ℝ
hl : IsExpCmpFilter l
hb : b₁ < b₂
a₁ a₂ z : ℂ
hz : z ≠ 0
⊢ z ^ a₁ * cexp (↑b₁ * z) = z ^ (a₂ + (a₁ - a₂)) * cexp (↑b₁ * z)
Module: Mathlib.Analysis.SpecialFunctions.FrullaniIntegral

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
hf : LocallyIntegrableOn f (Ioi 0) volume
ha : 0 < a
hb : 0 < b
⊢ IntervalIntegrable (fun x ↦ x⁻¹ • f x) volume a b

Tactic:
have hsub : uIcc a b ⊆ Ioi 0 := by simp [uIcc, Icc_subset_Ioi_iff, ha, hb]

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
hf : LocallyIntegrableOn f (Ioi 0) volume
ha : 0 < a
hb : 0 < b
hsub : uIcc a b ⊆ Ioi 0
⊢ IntervalIntegrable (fun x ↦ x⁻¹ • f x) volume a b
Module: Mathlib.Analysis.SpecialFunctions.FrullaniIntegral

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
a b c : ℝ
hf : LocallyIntegrableOn f (Ioi 0) volume
ha : 0 < a
hb : 0 < b
hc : 0 < c
⊢ IntervalIntegrable (fun x ↦ x⁻¹ • f (c * x)) volume a b

Tactic:
have hsub : uIcc a b ⊆ Ioi 0 := by simp [uIcc, Icc_subset_Ioi_iff, ha, hb]

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
a b c : ℝ
hf : LocallyIntegrableOn f (Ioi 0) volume
ha : 0 < a
hb : 0 < b
hc : 0 < c
hsub : uIcc a b ⊆ Ioi 0
⊢ IntervalIntegrable (fun x ↦ x⁻¹ • f (c * x)) volume a b
Module: Mathlib.Analysis.SpecialFunctions.FrullaniIntegral

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
a b c : ℝ
hf : LocallyIntegrableOn f (Ioi 0) volume
ha : 0 < a
hb : 0 < b
hc : 0 < c
hsub : uIcc a b ⊆ Ioi 0
hf_cint : IntervalIntegrable f volume (c * a) (c * b)
⊢ IntervalIntegrable (fun x ↦ f (c * x)) volume a b

Tactic:
have h := hf_cint.comp_mul_left (c := c)

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
a b c : ℝ
hf : LocallyIntegrableOn f (Ioi 0) volume
ha : 0 < a
hb : 0 < b
hc : 0 < c
hsub : uIcc a b ⊆ Ioi 0
hf_cint : IntervalIntegrable f volume (c * a) (c * b)
h : IntervalIntegrable (fun x ↦ f (c * x)) volume (c * a / c) (c * b / c)
⊢ IntervalIntegrable (fun x ↦ f (c * x)) volume a b
Module: Mathlib.Analysis.SpecialFunctions.FrullaniIntegral

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
a b c : ℝ
hf : LocallyIntegrableOn f (Ioi 0) volume
ha : 0 < a
hb : 0 < b
hc : 0 < c
⊢ IntervalIntegrable (fun x ↦ x⁻¹ • f (c * x)) volume a b

Tactic:
have hsub : uIcc a b ⊆ Ioi 0 := by simp [uIcc, Icc_subset_Ioi_iff, ha, hb]
  have hf_cint : IntervalIntegrable f volume (c * a) (c * b) :=
    intervalIntegrable_iff.mpr
      ((hf.integrableOn_compact_subset (by simp [uIcc, Icc_subset_Ioi_iff, mul_pos hc ha,
        mul_pos hc hb]) isCompact_uIcc).mono_set uIoc_subset_uIcc)
  have hf_comp : IntervalIntegrable (fun x ↦ f (c * x)) volume a b := by
    have h := hf_cint.comp_mul_left (c := c)
    rwa [mul_div_cancel_left₀ a hc.ne', mul_div_cancel_left₀ b hc.ne'] at h
  exact hf_comp.continuousOn_smul (continuousOn_inv₀.mono fun x hx ↦ ne_of_gt (hsub hx))

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

Tactic:
have hsub : uIcc a b ⊆ Ioi 0 := by simp [uIcc, Icc_subset_Ioi_iff, ha, hb]

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
⊢ ‖(∫ (x : ℝ) in a..b, x⁻¹ • f x) - log (b / a) • V‖ ≤ δ * |log (b / a)|
Module: Mathlib.Analysis.SpecialFunctions.FrullaniIntegral

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
L : E
inst✝ : CompleteSpace E
hf : LocallyIntegrableOn f (Ioi 0) volume
ha : 0 < a
hb : 0 < b
hL : Tendsto f (𝓝[>] 0) (𝓝 L)
⊢ Tendsto (fun ε ↦ ∫ (x : ℝ) in a * ε..b * ε, x⁻¹ • f x) (𝓝[>] 0) (𝓝 (log (b / a) • L))

Tactic:
apply tendsto_integral_inv_smul_of_tendsto_uniform hf ha hb self_mem_nhdsWithin
  intro δ hδ
  have hev : ∀ᶠ x in 𝓝[>] (0 : ℝ), dist (f x) L < δ :=
    hL.eventually (ball_mem_nhds L hδ)
  rw [Filter.Eventually, mem_nhdsWithin_iff] at hev
  obtain ⟨η, hη, hη_sub⟩ := hev
  set M := max a b with hM_def
  have hM : 0 < M := lt_max_of_lt_left ha
  filter_upwards [self_mem_nhdsWithin,
    nhdsWithin_le_nhds (Iio_mem_nhds (div_pos hη hM))] with t ht_pos ht_bound
  intro x hx
  have hx_pos : 0 < x := (lt_min (by positivity) (by positivity)).trans_le (uIoc_subset_uIcc hx).1
  have hx_lt_η : dist x 0 < η := by
    rw [Real.dist_eq, sub_zero, abs_of_pos hx_pos]
    calc x
      _ ≤ max (a * t) (b * t) := (uIoc_subset_uIcc hx).2
      _ = M * t := by rw [hM_def, max_mul_of_nonneg _ _ ht_pos.le]
      _ < M * (η / M) := mul_lt_mul_of_pos_left ht_bound hM
      _ = η := mul_div_cancel₀ η (ne_of_gt hM)
  have := hη_sub ⟨mem_ball.2 hx_lt_η, hx_pos⟩
  rw [mem_ofPred_eq, dist_eq_norm] at this
  exact le_of_lt this

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

Goal state before:
pp: p t x : ℝ
hp : 0 < p
ht : 0 ≤ t
hx : 0 ≤ x
x✝ : t = 0 ∨ 0 < t
⊢ 0 ≤ t ^ p * (t⁻¹ - (t + x)⁻¹)

Tactic:
cases eq_or_lt_of_le' ht with

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

Goal state before:
pp: p t : ℝ
hp : p ∈ Ioo 0 1
ht : 0 ≤ t
⊢ MonotoneOn (p.rpowIntegrand₀₁ t) (Ici 0)

Tactic:
intro x hx y hy hxy
  by_cases h : x = 0
  case pos => simpa [h, rpowIntegrand₀₁] using rpowIntegrand₀₁_nonneg hp.1 ht hy
  case neg =>
    simp only [rpowIntegrand₀₁, mem_Ici] at hx h ⊢
    gcongr

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

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

Tactic:
by
    rw [Complex.Gamma_mul_Gamma_one_sub, cpow_one]
    ring_nf

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

Goal state before:
pp: p : ℝ
hp : p ∈ Ioo 0 1
⊢ 0 ≤ (∫ (t : ℝ) in Ioi 0, p.rpowIntegrand₀₁ t 1)⁻¹

Tactic:
rw [inv_nonneg]

Goal state after:
p : ℝ
hp : p ∈ Ioo 0 1
⊢ 0 ≤ ∫ (t : ℝ) in Ioi 0, p.rpowIntegrand₀₁ t 1