mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.SpecialFunctions.Log.RpowTendsto

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

Tactic:
by
  refine (tendstoLocallyUniformlyOn_iff_forall_isCompact isOpen_Ioi).mpr ?_
  intro s hs hs'
  rw [Metric.uniformity_basis_dist_le.tendstoUniformlyOn_iff_of_uniformity]
  intro ε hε
  let pbound : ℝ := ε / (sSup ((fun x => ‖log x‖ ^ 2) '' s) + 1)
  have hxs : ∀ x ∈ s, x ≠ 0 := by grind
  have sSup_nonneg : 0 ≤ sSup ((fun x => ‖log x‖ ^ 2) '' s) := by
    refine Real.sSup_nonneg ?_
    grind [← sq_nonneg]
  have sSup_nonneg' : 0 ≤ sSup ((fun x => ‖log x‖) '' s) := by
    refine Real.sSup_nonneg ?_
    grind [← sq_nonneg]
  have pbound_pos : 0 < pbound := by positivity
  have h₁ : ∀ᶠ p : ℝ in 𝓝[>] 0, 0 < p ∧ p < pbound := nhdsGT_basis 0 |>.mem_of_mem pbound_pos
  have h₂ : ∀ᶠ p : ℝ in 𝓝[>] 0, p ≤ 1 / (sSup ((fun x => ‖log x‖) '' s) + 1) :=
    Eventually.filter_mono nhdsWithin_le_nhds <| eventually_le_nhds (by positivity)
  have hcont : ContinuousOn (fun x => ‖log x‖ ^ 2) s := by fun_prop
  have hcont' : ContinuousOn (fun x => ‖log x‖) s := by fun_prop
  filter_upwards [h₁, h₂] with p ⟨hp₁,hp₂⟩ hp₃
  intro x hx
  have hx' : ‖p * log x‖ ≤ 1 := calc
    _ = p * ‖log x‖ := by grind [norm_mul, Real.norm_of_nonneg]
    _ ≤ 1 / (sSup ((fun y => ‖log y‖) '' s) + 1) * ‖log x‖ := by gcongr
    _ ≤ 1 / (‖log x‖ + 1) * ‖log x‖ := by
        gcongr
        refine le_csSup ?_ (by grind)
        grind [IsCompact.bddAbove, ← IsCompact.image_of_continuousOn]
    _ = ‖log x‖ / (‖log x‖ + 1) := by grind
    _ ≤ 1 := by rw [div_le_one₀] <;> grind [norm_nonneg]
  have pinv_nonneg : 0 ≤ p⁻¹ := by grind [_root_.inv_nonneg]
  rw [dist_eq_norm']
  calc
    _ ≤ p * ‖log x‖ ^ 2 := Real.norm_inv_mul_rpow_sub_one_sub_log_le hp₁ (hs hx) hx'
    _ ≤ p * sSup ((fun x => ‖log x‖ ^ 2) '' s) := by
          gcongr
          refine le_csSup ?_ (by grind)
          grind [IsCompact.bddAbove, ← IsCompact.image_of_continuousOn]
    _ ≤ pbound * (sSup ((fun x => ‖log x‖ ^ 2) '' s) + 1) := by gcongr; grind
    _ = ε := by grind

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

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
c ε r : ℝ
hc : c ≠ 0
⊢ ∫ (x : ℝ) in ε..r, x⁻¹ • f (c * x) = ∫ (x : ℝ) in c * ε..c * r, x⁻¹ • f x

Tactic:
let u : ℝ → E := fun x ↦ x⁻¹ • f x

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
c ε r : ℝ
hc : c ≠ 0
u : ℝ → E := fun x ↦ x⁻¹ • f x
⊢ ∫ (x : ℝ) in ε..r, x⁻¹ • f (c * x) = ∫ (x : ℝ) in c * ε..c * r, x⁻¹ • f x
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 • y)⁻¹ʳ = (a • (conjSqrt x) 1 + b • (conjSqrt x) z)⁻¹ʳ

Tactic:
rw [conjSqrt_conjSqrt_ringInverse _ _ xpos, conjSqrt_one x xpos.nonneg]

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 : ℝ
R : E
inst✝ : CompleteSpace E
hf : LocallyIntegrableOn f (Ioi 0) volume
ha : 0 < a
hb : 0 < b
hR : Tendsto f atTop (𝓝 R)
δ : ℝ
hδ : δ > 0
N : ℝ
hN : ∀ (b : ℝ), N ≤ b → dist (f b) R < δ
⊢ ∀ᶠ (t : ℝ) in atTop, ∀ x ∈ uIoc (a * t) (b * t), ‖f x - R‖ ≤ δ

Tactic:
have hm : 0 < min a b := lt_min ha hb

Goal state after:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
R : E
inst✝ : CompleteSpace E
hf : LocallyIntegrableOn f (Ioi 0) volume
ha : 0 < a
hb : 0 < b
hR : Tendsto f atTop (𝓝 R)
δ : ℝ
hδ : δ > 0
N : ℝ
hN : ∀ (b : ℝ), N ≤ b → dist (f b) R < δ
hm : 0 < min a b
⊢ ∀ᶠ (t : ℝ) in atTop, ∀ x ∈ uIoc (a * t) (b * t), ‖f x - R‖ ≤ δ
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation

Goal state before:
pp: p t x : ℝ
hp : p ∈ Ioo 0 1
ht : 0 ≤ t
hx : 0 ≤ x
ht' : ¬t = 0
hxt : t + x ≠ 0
⊢ t ^ p * (1 / t - 1 / (t + x)) = t ^ p * ((t + x - t) / (t * (t + x)))

Tactic:
rw [div_sub_div _ _ (by lia) (by lia)]

Goal state after:
p t x : ℝ
hp : p ∈ Ioo 0 1
ht : 0 ≤ t
hx : 0 ≤ x
ht' : ¬t = 0
hxt : t + x ≠ 0
⊢ t ^ p * ((1 * (t + x) - t * 1) / (t * (t + x))) = t ^ p * ((t + x - t) / (t * (t + x)))
Module: Mathlib.NumberTheory.Harmonic.EulerMascheroni

Goal state before:
pp: case inr
n : ℕ
hn : n > 0
⊢ ↑(↑(n + 1))⁻¹ < log (↑(n + 1) / ↑n)

Tactic:
← neg_lt_neg_iff,

Goal state after:
case inr
n : ℕ
hn : n > 0
⊢ -log (↑(n + 1) / ↑n) < -↑(↑(n + 1))⁻¹
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation

Goal state before:
pp: p x : ℝ
hp : p ∈ Ioo 0 1
hx : 0 ≤ x
h✝ : 0 < x
this : ∫ (t : ℝ) in Ioi 0, p.rpowIntegrand₀₁ t 1 ≠ 0
⊢ x ^ p = x ^ p * 1

Tactic:
mul_one

Goal state after:
p x : ℝ
hp : p ∈ Ioo 0 1
hx : 0 ≤ x
h✝ : 0 < x
this : ∫ (t : ℝ) in Ioi 0, p.rpowIntegrand₀₁ t 1 ≠ 0
⊢ x ^ p = x ^ p
Module: Mathlib.Analysis.SpecialFunctions.Log.Base

Goal state before:
pp: b x y : ℝ
b_pos : 0 < b
b_ne_one : b ≠ 1
hy : 0 < y
⊢ logb b y = x ↔ b ^ x = y

Tactic:
by
  constructor <;> rintro rfl
  · exact rpow_logb b_pos b_ne_one hy
  · exact logb_rpow b_pos b_ne_one

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

Goal state before:
pp: ε : ℝ
hε : 0 < ε
x : ℝ
heq : rexp (-(ε * x * x)) + x * (rexp (-(ε * x * x)) * (-2 * ε * x)) = rexp (-(ε * x * x)) * (1 - 2 * (ε * x * x))
⊢ |rexp (-(ε * x * x)) + x * (rexp (-(ε * x * x)) * (-2 * ε * x))| ≤ 1

Tactic:
rw [heq, abs_mul, abs_exp]

Goal state after:
ε : ℝ
hε : 0 < ε
x : ℝ
heq : rexp (-(ε * x * x)) + x * (rexp (-(ε * x * x)) * (-2 * ε * x)) = rexp (-(ε * x * x)) * (1 - 2 * (ε * x * x))
⊢ rexp (-(ε * x * x)) * |1 - 2 * (ε * x * x)| ≤ 1
Module: Mathlib.Analysis.SpecialFunctions.MulExpNegMulSq

Goal state before:
pp: ε : ℝ
hε : 0 < ε
x : ℝ
⊢ |(√ε)⁻¹| * |mulExpNegMulSq 1 (√ε * x)| ≤ (√ε)⁻¹

Tactic:
abs_of_pos (by positivity)

Goal state after:
ε : ℝ
hε : 0 < ε
x : ℝ
⊢ (√ε)⁻¹ * |mulExpNegMulSq 1 (√ε * x)| ≤ (√ε)⁻¹
Module: Mathlib.Analysis.SpecialFunctions.Log.Base

Goal state before:
pp: case a
b : ℕ
r : ℝ
hr✝ : 0 ≤ r
hr : 0 < r
hb : 1 < b
hb1' : 1 < ↑b
⊢ ↑b ^ Int.log b r ≤ r

Tactic:
exact Int.zpow_log_le_self hb hr

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

Goal state before:
pp: ε : ℝ
hε : 0 < ε
x : ℝ
⊢ |ε.mulExpNegMulSq x| ≤ (√ε)⁻¹

Tactic:
rw [mulExpNegMulSq_eq_sqrt_mul_mulExpNegMulSq_one hε x, abs_mul, abs_of_pos (by positivity)]
  apply mul_le_of_le_one_right
  · positivity
  · exact abs_mulExpNegMulSq_one_le_one (√ε * x)

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

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

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

Tactic:
· have hb1' : 1 < (b : ℝ) := Nat.one_lt_cast.mpr hb
    apply le_antisymm
    · rw [Int.ceil_le, logb_le_iff_le_rpow hb1' hr, rpow_intCast]
      exact Int.self_le_zpow_clog hb r
    · rw [← Int.le_zpow_iff_clog_le hb hr, ← rpow_intCast b]
      refine (rpow_logb (zero_lt_one.trans hb1') hb1'.ne' hr).symm.trans_le ?_
      exact rpow_le_rpow_of_exponent_le hb1'.le (Int.le_ceil _)

Goal state after:
case neg
b : ℕ
r : ℝ
hr✝ : 0 ≤ r
hr : 0 < r
hb : ¬1 < b
⊢ ⌈logb (↑b) r⌉ = Int.clog b r
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
inst✝¹ : FiniteDimensional ℝ E
inst✝ : μ.IsAddHaarMeasure
⊢ μ.toSphere = 0 ↔ dim E = 0

Tactic:
← measure_univ_eq_zero,

Goal state after:
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
μ : Measure E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
inst✝ : μ.IsAddHaarMeasure
⊢ μ.toSphere univ = 0 ↔ dim E = 0
Module: Mathlib.Analysis.SpecialFunctions.Pow.Integral

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
f : α → ℝ
f_nn : 0 ≤ᵐ[μ] f
f_mble : AEMeasurable f μ
p : ℝ
p_pos : 0 < p
one_lt_p : -1 < p - 1
g : ℝ → ℝ := fun t ↦ t ^ (p - 1)
obs : ∀ (x : ℝ), intervalIntegral g 0 x volume = x ^ p / p
g_nn : ∀ᵐ (t : ℝ) ∂volume.restrict (Ioi 0), 0 ≤ g t
g_intble : ∀ (t : ℝ), 0 < t → IntervalIntegrable g volume 0 t
key :
  ∫⁻ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0..f ω, g t) ∂μ = ∫⁻ (t : ℝ) in Ioi 0, μ {a | t ≤ f a} * ENNReal.ofReal (g t)
⊢ AEMeasurable (fun ω ↦ ENNReal.ofReal (f ω ^ p / p)) μ

Tactic:
· have aux := (measurable_const (a := p)).aemeasurable (μ := μ)
    exact measurable_id.ennreal_ofReal.comp_aemeasurable <| (f_mble.pow aux).div_const p

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

Goal state before:
pp: r : ℝ
hr : 0 < r
s : ℂ
hs : ‖s‖ < r
l : ℂ
h : 2 * r ≤ ‖l‖
this✝ : s ≠ l
this : 0 < ‖l‖
⊢ ‖(l ^ 2 - (s - l) ^ 2 * 1) / ((s - l) ^ 2 * l ^ 2)‖ = ‖(l ^ 2 - (s - l) ^ 2) / ((s - l) ^ 2 * l ^ 2)‖

pp: case hb
r : ℝ
hr : 0 < r
s : ℂ
hs : ‖s‖ < r
l : ℂ
h : 2 * r ≤ ‖l‖
this✝ : s ≠ l
this : 0 < ‖l‖
⊢ (s - l) ^ 2 ≠ 0

pp: case hd
r : ℝ
hr : 0 < r
s : ℂ
hs : ‖s‖ < r
l : ℂ
h : 2 * r ≤ ‖l‖
this✝ : s ≠ l
this : 0 < ‖l‖
⊢ l ^ 2 ≠ 0

Tactic:
mul_one

Goal state after:
r : ℝ
hr : 0 < r
s : ℂ
hs : ‖s‖ < r
l : ℂ
h : 2 * r ≤ ‖l‖
this✝ : s ≠ l
this : 0 < ‖l‖
⊢ ‖(l ^ 2 - (s - l) ^ 2) / ((s - l) ^ 2 * l ^ 2)‖ = ‖(l ^ 2 - (s - l) ^ 2) / ((s - l) ^ 2 * l ^ 2)‖

case hb
r : ℝ
hr : 0 < r
s : ℂ
hs : ‖s‖ < r
l : ℂ
h : 2 * r ≤ ‖l‖
this✝ : s ≠ l
this : 0 < ‖l‖
⊢ (s - l) ^ 2 ≠ 0

case hd
r : ℝ
hr : 0 < r
s : ℂ
hs : ‖s‖ < r
l : ℂ
h : 2 * r ≤ ‖l‖
this✝ : s ≠ l
this : 0 < ‖l‖
⊢ l ^ 2 ≠ 0
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: case neg
L : PeriodPair
l₀ : ℂ
s : Finset ↥L.lattice
i : ↥L.lattice
hi : i ∈ s
h✝ : ¬↑i = l₀
⊢ DifferentiableOn ℂ (fun z ↦ 1 / (z - ↑i) ^ 2 - 1 / ↑i ^ 2) (↑L.lattice \ {l₀})ᶜ

Tactic:
exact .sub (.div (by fun_prop) (by fun_prop) (by aesop (add simp sub_eq_zero))) (by fun_prop)

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

Goal state before:
pp: a b : Multiset ℂ
h : a.card ≤ b.card
ha : ∀ j ∈ a, ∀ (k : ℕ), j ≠ -↑k
this : Tendsto (fun x ↦ (1 / ↑x) ^ (b.card + 1 - a.card)) atTop (𝓝 0)
n : ℕ
⊢ (↑n)⁻¹ ^ (b.card + 1 - a.card) = ↑n ^ (↑a.card - ↑b.card - 1)

Tactic:
inv_pow,

Goal state after:
a b : Multiset ℂ
h : a.card ≤ b.card
ha : ∀ j ∈ a, ∀ (k : ℕ), j ≠ -↑k
this : Tendsto (fun x ↦ (1 / ↑x) ^ (b.card + 1 - a.card)) atTop (𝓝 0)
n : ℕ
⊢ (↑n ^ (b.card + 1 - a.card))⁻¹ = ↑n ^ (↑a.card - ↑b.card - 1)
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: L : PeriodPair
l₀ : ℂ
hl₀ : l₀ ∈ L.lattice
l : ↥L.lattice
hl : ↑l / 2 ∉ L.lattice
⊢ ℘[L - l₀] (-(↑l / 2) + ↑l) = ℘[L - l₀ - ↑l] (-(↑l / 2)) + (1 / l₀ ^ 2 - 1 / (l₀ - ↑l) ^ 2)

Tactic:
rw [L.weierstrassPExcept_neg, L.weierstrassPExcept_def ⟨l₀, hl₀⟩,
      L.weierstrassPExcept_def ⟨_, neg_mem (sub_mem hl₀ l.2)⟩, add_assoc]
    congr 2 <;> ring

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

Goal state before:
pp: θ : ℂ
n : ℤ
⊢ sinh ((↑n + 1) * θ) * 1 = sinh ((↑n + 1) * θ)

Tactic:
mul_one

Goal state after:
θ : ℂ
n : ℤ
⊢ sinh ((↑n + 1) * θ) = sinh ((↑n + 1) * θ)
Module: Mathlib.Analysis.SpecialFunctions.Stirling

Goal state before:
pp: case zero
⊢ 0 ≤ log (rexp 1 / √2)

Tactic:
apply Real.log_nonneg

Goal state after:
case zero
⊢ 1 ≤ rexp 1 / √2
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Orthogonality

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

Tactic:
by
  rw [integral_measureT_eq_integral_cos]; simp

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

Goal state before:
pp: n : ℕ
hn : ¬n = 0
c : ℕ → ℝ
i : ℕ
hrange : i ∈ range (2 * n)
hi : ¬i = 0
hP : (∑ i ∈ range (2 * n), c i • ↑(chebyshevTsequence ℝ) i).degree < ↑(2 * n)
⊢ i < 2 * n * 1

Tactic:
mul_one

Goal state after:
n : ℕ
hn : ¬n = 0
c : ℕ → ℝ
i : ℕ
hrange : i ∈ range (2 * n)
hi : ¬i = 0
hP : (∑ i ∈ range (2 * n), c i • ↑(chebyshevTsequence ℝ) i).degree < ↑(2 * n)
⊢ i < 2 * n
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: L : PeriodPair
l : ℂ
n : ℕ
⊢ iteratedDeriv n ℘[L - l] l = if n = 0 then ℘[L - l] l else ↑(n + 1)! * L.sumInvPow l (n + 2)

Tactic:
by
  rw [← div_mul_cancel₀ (a := iteratedDeriv _ _ _) (b := ↑n !) (by simp),
    ← eq_div_iff_mul_eq (by simp)]
  trans if n = 0 then ℘[L - l] l else (n + 1) * L.sumInvPow l (n + 2)
  · simpa using congr($((L.analyticAt_weierstrassPExcept l).hasFPowerSeriesAt
      |>.eq_formalMultilinearSeries (L.hasFPowerSeriesAt_weierstrassPExcept l)).coeff n)
  · cases n <;> simp [Nat.factorial_succ]; field

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

Goal state before:
pp: L : PeriodPair
z x : ℂ
hx : ∀ (l : ↥L.lattice), ‖z - x‖ < ‖↑l - x‖
⊢ HasSum (fun i ↦ (L.weierstrassPSeries x).coeff i * (z - x) ^ i) (℘[L] z)

Tactic:
simp_rw [← L.weierstrassPExceptSeries_of_notMem _ L.ω₁_div_two_notMem_lattice,
    ← L.weierstrassPExcept_of_notMem _ L.ω₁_div_two_notMem_lattice]
  exact L.weierstrassPExceptSeries_hasSum _ z x fun l hl ↦ hx l

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

Goal state before:
pp: case pos
n : ℕ
P : ℝ[X]
k : ℕ
x : ℝ
hx : 1 ≤ x
hPdeg : P.degree ≤ ↑n
hPbnd : ∀ x ∈ Set.Icc (-1) 1, |eval x P| ≤ 1
hk : n < k
⊢ eval x ((⇑derivative)^[k] P) ≤ eval x ((⇑derivative)^[k] (T ℝ ↑n))

pp: case neg
n : ℕ
P : ℝ[X]
k : ℕ
x : ℝ
hx : 1 ≤ x
hPdeg : P.degree ≤ ↑n
hPbnd : ∀ x ∈ Set.Icc (-1) 1, |eval x P| ≤ 1
hk : k ≤ n
⊢ eval x ((⇑derivative)^[k] P) ≤ eval x ((⇑derivative)^[k] (T ℝ ↑n))

Tactic:
· rw [iterate_derivative_eq_zero_of_degree_lt (by grw [hPdeg]; simpa),
      iterate_derivative_eq_zero_of_degree_lt (by simp [hk])]

Goal state after:
case neg
n : ℕ
P : ℝ[X]
k : ℕ
x : ℝ
hx : 1 ≤ x
hPdeg : P.degree ≤ ↑n
hPbnd : ∀ x ∈ Set.Icc (-1) 1, |eval x P| ≤ 1
hk : k ≤ n
⊢ eval x ((⇑derivative)^[k] P) ≤ eval x ((⇑derivative)^[k] (T ℝ ↑n))
Module: Mathlib.Analysis.SpecificLimits.ArithmeticGeometric

Goal state before:
pp: R : Type u_1
a b : R
inst✝ : Field R
ha : a ≠ 1
n : ℕ
⊢ arithGeom a b 0 n = b * (1 - a ^ n) / (1 - a)

Tactic:
by
  rw [arithGeom_eq ha n]
  ring

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

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

Tactic:
by
  rcases n with (n | n)
  · dsimp
    rw [← Nat.cast_ofNat, ← Nat.cast_add, ← Nat.cast_add_one, fib_natCast, fib_natCast,
      Nat.fib_add_two, Nat.cast_add]
  · rw [negSucc_eq, ← Nat.cast_add_one, fib_neg_natCast]
    simp only [Nat.cast_add, Nat.cast_one, neg_add_rev, reduceNeg, add_comm,
      add_assoc, reduceAdd, add_neg_cancel_comm_assoc, fib_neg_natCast]
    if hn0 : n = 0 then simp [hn0] else
    symm
    calc _ = (-1) ^ (n + 1) * ((n.fib - (n + 1).fib : ℤ)) := by grind
      _ = _ := by
        have : -(n : ℤ) + 1 = -((n - 1 : ℕ) : ℤ) := by grind
        obtain (⟨n, rfl⟩ | ⟨n, rfl⟩) := n.even_or_odd
        · rw [Nat.fib_add_one hn0, this, fib_neg_natCast, pow_add, ← two_mul,
            Nat.sub_add_cancel (by grind)]
          simp
        · rw [Nat.fib_add_one hn0, this, fib_neg_natCast, pow_add]
          simp

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

Goal state before:
pp: k : ℕ
x : ℝ
hx : |x| ≤ 1
n : ℕ
this : (⇑derivative)^[k] (T ℝ ↑n) ∈ Submodule.span ℕ ((fun m ↦ T ℝ ↑m) '' Set.Icc 0 (n - k))
f : ℝ[X] →₀ ℕ
hfsupp : ↑f.support ⊆ (fun m ↦ T ℝ ↑m) '' Set.Icc 0 (n - k)
hfderiv : ∑ p ∈ f.support, f p • p = (⇑derivative)^[k] (T ℝ ↑n)
hf : ∀ (y : ℝ), ∑ p ∈ f.support, f p • eval y p = eval y ((⇑derivative)^[k] (T ℝ ↑n))
i : ℝ[X]
hi✝ : i ∈ f.support
m : ℕ
hm : m ∈ Set.Icc 0 (n - k)
hi : T ℝ ↑m = i
⊢ f (T ℝ ↑m) • |eval x (T ℝ ↑m)| ≤ f (T ℝ ↑m) • eval 1 (T ℝ ↑m)

Tactic:
abs_eval_T_real_le_one m hx

Goal state after:
k : ℕ
x : ℝ
hx : |x| ≤ 1
n : ℕ
this : (⇑derivative)^[k] (T ℝ ↑n) ∈ Submodule.span ℕ ((fun m ↦ T ℝ ↑m) '' Set.Icc 0 (n - k))
f : ℝ[X] →₀ ℕ
hfsupp : ↑f.support ⊆ (fun m ↦ T ℝ ↑m) '' Set.Icc 0 (n - k)
hfderiv : ∑ p ∈ f.support, f p • p = (⇑derivative)^[k] (T ℝ ↑n)
hf : ∀ (y : ℝ), ∑ p ∈ f.support, f p • eval y p = eval y ((⇑derivative)^[k] (T ℝ ↑n))
i : ℝ[X]
hi✝ : i ∈ f.support
m : ℕ
hm : m ∈ Set.Icc 0 (n - k)
hi : T ℝ ↑m = i
⊢ f (T ℝ ↑m) • 1 ≤ f (T ℝ ↑m) • eval 1 (T ℝ ↑m)
Module: Mathlib.NumberTheory.Real.GoldenRatio

Goal state before:
pp: ⊢ 1 < φ

Tactic:
refine lt_of_mul_lt_mul_left ?_ (le_of_lt goldenRatio_pos)
  simp [← sq, zero_lt_one]

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

Goal state before:
pp: ⊢ fibRec.charPoly.IsRoot φ

Tactic:
fibRec_charPoly_eq

Goal state after:
⊢ (X ^ 2 - (X + 1)).IsRoot φ
Module: Mathlib.NumberTheory.Real.GoldenRatio

Goal state before:
pp: ⊢ fibRec.charPoly.IsRoot ψ

Tactic:
fibRec_charPoly_eq

Goal state after:
⊢ (X ^ 2 - (X + 1)).IsRoot ψ
Module: Mathlib.CategoryTheory.Generator.Abelian

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasLimits C
inst✝ : EnoughInjectives C
G : C
hG : IsSeparator G
this : WellPowered.{v, v, u} C
⊢ ∃ G, Injective G ∧ IsCoseparator G

Tactic:
have : HasProductsOfShape (Subobject (op G)) C := hasProductsOfShape_of_small.{v} _ _

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasLimits C
inst✝ : EnoughInjectives C
G : C
hG : IsSeparator G
this✝ : WellPowered.{v, v, u} C
this : HasProductsOfShape (Subobject (op G)) C
⊢ ∃ G, Injective G ∧ IsCoseparator G
Module: Mathlib.CategoryTheory.Comma.Final

Goal state before:
pp: A : Type u₁
inst✝⁵ : Category.{v₁, u₁} A
B : Type u₂
inst✝⁴ : Category.{v₂, u₂} B
T : Type u₃
inst✝³ : Category.{v₃, u₃} T
L : A ⥤ T
R : B ⥤ T
inst✝² : IsCofiltered A
inst✝¹ : IsCofiltered B
inst✝ : ∀ (b : B), IsCofiltered (CostructuredArrow L (R.obj b))
⊢ Nonempty (Comma L R)

Tactic:
obtain ⟨b⟩ := IsCofiltered.nonempty (C := B)

Goal state after:
A : Type u₁
inst✝⁵ : Category.{v₁, u₁} A
B : Type u₂
inst✝⁴ : Category.{v₂, u₂} B
T : Type u₃
inst✝³ : Category.{v₃, u₃} T
L : A ⥤ T
R : B ⥤ T
inst✝² : IsCofiltered A
inst✝¹ : IsCofiltered B
inst✝ : ∀ (b : B), IsCofiltered (CostructuredArrow L (R.obj b))
b : B
⊢ Nonempty (Comma L R)
Module: Mathlib.CategoryTheory.Comma.Final

Goal state before:
pp: case refine_1
A : Type u₁
inst✝⁵ : Category.{v₁, u₁} A
B : Type u₂
inst✝⁴ : Category.{v₂, u₂} B
T : Type u₃
inst✝³ : Category.{v₃, u₃} T
L : A ⥤ T
R : B ⥤ T
inst✝² : IsCofiltered A
inst✝¹ : IsCofiltered B
inst✝ : ∀ (b : B), IsCofiltered (CostructuredArrow L (R.obj b))
this : IsCofiltered (Comma L R)
a : A
⊢ ∃ c, Nonempty ((fst L R).obj c ⟶ a)

Tactic:
obtain ⟨b⟩ := IsCofiltered.nonempty (C := B)

Goal state after:
case refine_1
A : Type u₁
inst✝⁵ : Category.{v₁, u₁} A
B : Type u₂
inst✝⁴ : Category.{v₂, u₂} B
T : Type u₃
inst✝³ : Category.{v₃, u₃} T
L : A ⥤ T
R : B ⥤ T
inst✝² : IsCofiltered A
inst✝¹ : IsCofiltered B
inst✝ : ∀ (b : B), IsCofiltered (CostructuredArrow L (R.obj b))
this : IsCofiltered (Comma L R)
a : A
b : B
⊢ ∃ c, Nonempty ((fst L R).obj c ⟶ a)
Module: Mathlib.CategoryTheory.Comma.Final

Goal state before:
pp: A : Type u₁
inst✝⁵ : Category.{v₁, u₁} A
B : Type u₂
inst✝⁴ : Category.{v₂, u₂} B
T : Type u₃
inst✝³ : Category.{v₃, u₃} T
L : A ⥤ T
R : B ⥤ T
inst✝² : IsFiltered A
inst✝¹ : IsFiltered B
inst✝ : ∀ (a : A), IsFiltered (StructuredArrow (L.obj a) R)
⊢ IsFiltered (Comma L R)

Tactic:
by
  have (a : Aᵒᵖ) : IsCofiltered (CostructuredArrow R.op (L.op.obj a)) :=
    IsCofiltered.of_equivalence (structuredArrowOpEquivalence R (L.obj a.unop))
  have : IsCofiltered (Comma R.op L.op) := isCofiltered_of_isCofiltered_costructuredArrow _ _
  exact IsFiltered.of_equivalence (opEquiv L R).symm

Goal state after:
Module: Mathlib.CategoryTheory.Limits.FilteredColimitCommutesProduct

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
ι : Type u_2
inst✝ : HasProductsOfShape ι C
H :
  ∀ ⦃J : ι → Type w⦄ [inst : (i : ι) → SmallCategory (J i)] [∀ (i : ι), IsFiltered (J i)] (F : (i : ι) → J i ⥤ C)
    [∀ (i : ι), HasColimit (F i)], ∃ c x, Nonempty (IsColimit (coconePointwiseProduct c))
J : ι → Type w
x✝¹ : (i : ι) → SmallCategory (J i)
x✝ : ∀ (i : ι), IsFiltered (J i)
F : (i : ι) → J i ⥤ C
c : (i : ι) → Cocone (F i)
hc : (i : ι) → IsColimit (c i)
⊢ Nonempty (IsColimit (coconePointwiseProduct c))

Tactic:
by
    have (i : ι) : HasColimit (F i) := ⟨_, hc i⟩
    obtain ⟨c', hc', _⟩ := H F
    let e : coconePointwiseProduct c ≅ coconePointwiseProduct c' :=
      coconePointwiseProductIso _ fun i ↦ (hc i).uniqueUpToIso (hc' i)
    rwa [(IsColimit.equivIsoColimit e).nonempty_congr]

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.FreydMitchell

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
this✝ : (F C).Full
this : (G C).Full
⊢ (F C ⋙ G C ⋙ H C).Full

Tactic:
have : (G C ⋙ H C).Full := IsGrothendieckAbelian.OppositeModuleEmbedding.full_embedding _

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
this✝¹ : (F C).Full
this✝ : (G C).Full
this : (G C ⋙ H C).Full
⊢ (F C ⋙ G C ⋙ H C).Full
Module: Mathlib.CategoryTheory.Abelian.RightDerived

Goal state before:
pp: C : Type u
inst✝⁷ : Category.{v, u} C
D : Type u_1
inst✝⁶ : Category.{v_1, u_1} D
inst✝⁵ : Abelian C
inst✝⁴ : HasInjectiveResolutions C
inst✝³ : Abelian D
F G H : C ⥤ D
inst✝² : F.Additive
inst✝¹ : G.Additive
inst✝ : H.Additive
α : F ⟶ G
β : G ⟶ H
n : ℕ
⊢ rightDerived (α ≫ β) n = rightDerived α n ≫ rightDerived β n

Tactic:
by
  simp [NatTrans.rightDerived]

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.RightDerived

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u_1
inst✝⁴ : Category.{v_1, u_1} D
inst✝³ : Abelian C
inst✝² : HasInjectiveResolutions C
inst✝¹ : Abelian D
X : C
P : InjectiveResolution X
F : C ⥤ D
inst✝ : F.Additive
⊢ F.map 0 = 0

Tactic:
F.map_zero

Goal state after:
C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u_1
inst✝⁴ : Category.{v_1, u_1} D
inst✝³ : Abelian C
inst✝² : HasInjectiveResolutions C
inst✝¹ : Abelian D
X : C
P : InjectiveResolution X
F : C ⥤ D
inst✝ : F.Additive
⊢ 0 = 0
Module: Mathlib.CategoryTheory.Abelian.SerreClass.Localization

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : Abelian C
D : Type u'
inst✝⁴ : Category.{v', u'} D
L : C ⥤ D
P : ObjectProperty C
inst✝³ : P.IsSerreClass
inst✝² : L.IsLocalization P.isoModSerre
inst✝¹ : Preadditive D
inst✝ : L.Additive
X Y : C
f : X ⟶ Y
this : L.EssSurj
tfae_1_to_2 : Epi (L.map f) → P.epiModSerre f
tfae_2_to_3 : P.epiModSerre f → ∀ ⦃Z : C⦄ (z : Y ⟶ Z), L.map f ≫ L.map z = 0 → L.map z = 0
⊢ [Epi (L.map f), P.epiModSerre f, ∀ ⦃Z : C⦄ (z : Y ⟶ Z), L.map f ≫ L.map z = 0 → L.map z = 0].TFAE

Tactic:
tfae_have 3 → 1 := fun hf ↦ by
    rw [Preadditive.epi_iff_cancel_zero]
    intro W z hz
    obtain ⟨φ, hφ⟩ := Localization.exists_leftFraction L P.isoModSerre
      (z ≫ (L.objObjPreimageIso W).inv)
    rw [← cancel_mono (L.objObjPreimageIso W).inv, zero_comp, hφ,
      ← cancel_mono (L.map φ.s), zero_comp,
      MorphismProperty.LeftFraction.map_comp_map_s]
    apply hf φ.f
    have : L.map φ.f = z ≫ (L.objObjPreimageIso W).inv ≫ L.map φ.s := by
      simp [reassoc_of% hφ]
    rw [this, reassoc_of% hz, zero_comp]

Goal state after:
C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : Abelian C
D : Type u'
inst✝⁴ : Category.{v', u'} D
L : C ⥤ D
P : ObjectProperty C
inst✝³ : P.IsSerreClass
inst✝² : L.IsLocalization P.isoModSerre
inst✝¹ : Preadditive D
inst✝ : L.Additive
X Y : C
f : X ⟶ Y
this : L.EssSurj
tfae_1_to_2 : Epi (L.map f) → P.epiModSerre f
tfae_2_to_3 : P.epiModSerre f → ∀ ⦃Z : C⦄ (z : Y ⟶ Z), L.map f ≫ L.map z = 0 → L.map z = 0
tfae_3_to_1 : (∀ ⦃Z : C⦄ (z : Y ⟶ Z), L.map f ≫ L.map z = 0 → L.map z = 0) → Epi (L.map f)
⊢ [Epi (L.map f), P.epiModSerre f, ∀ ⦃Z : C⦄ (z : Y ⟶ Z), L.map f ≫ L.map z = 0 → L.map z = 0].TFAE