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

Goal state before:
pp: q : ℕ
p : ℝ
xne0 : p ≠ 0
xne1 : p ≠ 1
this : ∀ᶠ (y : ℝ) in 𝓝 p, deriv (fun p ↦ qaryEntropy q p) y = log (↑q - 1) + log (1 - y) - log y
⊢ deriv (fun x ↦ log (↑q - 1) + log (1 - x) - log x) p = -1 / (p * (1 - p))

Tactic:
rw [deriv_fun_sub ?_ (differentiableAt_log xne0)]

Goal state after:
q : ℕ
p : ℝ
xne0 : p ≠ 0
xne1 : p ≠ 1
this : ∀ᶠ (y : ℝ) in 𝓝 p, deriv (fun p ↦ qaryEntropy q p) y = log (↑q - 1) + log (1 - y) - log y
⊢ deriv (fun x ↦ log (↑q - 1) + log (1 - x)) p - deriv log p = -1 / (p * (1 - p))

q : ℕ
p : ℝ
xne0 : p ≠ 0
xne1 : p ≠ 1
this : ∀ᶠ (y : ℝ) in 𝓝 p, deriv (fun p ↦ qaryEntropy q p) y = log (↑q - 1) + log (1 - y) - log y
⊢ DifferentiableAt ℝ (fun x ↦ log (↑q - 1) + log (1 - x)) p
Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy

Goal state before:
pp: case neg
q : ℕ
p : ℝ
is_x_where_nondiff : ¬(p ≠ 0 ∧ p ≠ 1)
⊢ deriv (deriv (qaryEntropy q)) p = -1 / (p * (1 - p))

Tactic:
have : p = 0 ∨ p = 1 := Decidable.or_iff_not_not_and_not.mpr is_x_where_nondiff
    rw [deriv_zero_of_not_differentiableAt]
    · simp_all only [ne_eq, not_and, Decidable.not_not]
      cases this <;>
        simp_all only [mul_zero, one_ne_zero, zero_ne_one, sub_zero, mul_one, div_zero, sub_self]
    · intro h
      have contAt := h.continuousAt
      cases this <;>
        simp_all [not_continuousAt_deriv_qaryEntropy_zero, not_continuousAt_deriv_qaryEntropy_one]

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

Goal state before:
pp: a : ℝ
x : ℕ
⊢ a * a ^ (2 * x) / ↑x ! = a ^ (2 * x + 1) / ↑x !

Tactic:
_root_.pow_succ'

Goal state after:
a : ℝ
x : ℕ
⊢ a * a ^ (2 * x) / ↑x ! = a * a ^ (2 * x) / ↑x !
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
⊢ uIcc (c * a) (c * b) ⊆ Ioi 0

Tactic:
simp [uIcc, Icc_subset_Ioi_iff, mul_pos hc ha,
        mul_pos hc hb]

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

Goal state before:

Tactic:
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)

Goal state after:
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
r : ℝ
hr : r ∈ spectrum ℝ z
this : (a • 1 + b • r) ^ ↑(-1) ≤ a • 1 ^ ↑(-1) + b • r ^ ↑(-1)
⊢ (a + b * r) ^ (-1) ≤ a + b * r ^ (-1)

Tactic:
simpa using this

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

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

Tactic:
cpow_one,

Goal state after:
s : ℂ
⊢ 2 * 2 ^ (-s) * (↑π ^ (-1 / 2 - s) * ↑π ^ (1 / 2)) * Gamma s = 2 * (↑2 ^ (-s) * ↑π ^ (-s)) * Gamma s
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Digamma

Goal state before:
pp: ⊢ ↑√Real.pi * (-(2 * log 2) - ↑Real.eulerMascheroniConstant) / ↑Real.pi ^ (1 / 2) =
    -2 * log 2 - ↑Real.eulerMascheroniConstant

Tactic:
Real.sqrt_eq_rpow,

Goal state after:
⊢ ↑(Real.pi ^ (1 / 2)) * (-(2 * log 2) - ↑Real.eulerMascheroniConstant) / ↑Real.pi ^ (1 / 2) =
    -2 * log 2 - ↑Real.eulerMascheroniConstant
Module: Mathlib.NumberTheory.Harmonic.GammaDeriv

Goal state before:
pp: n : ℕ
⊢ deriv Gamma (↑n + 1) = ↑n ! * (-γ + ↑(harmonic n))

Tactic:
let f := log ∘ Gamma
  -- First reduce to computing derivative of `log ∘ Gamma`.
  suffices deriv (log ∘ Gamma) (n + 1) = -γ + harmonic n by
    rwa [Function.comp_def, deriv.log (differentiableAt_Gamma (fun m ↦ by linarith))
      (by positivity), Gamma_nat_eq_factorial, div_eq_iff_mul_eq (by positivity),
      mul_comm, Eq.comm] at this
  have hc : ConvexOn ℝ (Ioi 0) f := convexOn_log_Gamma
  have h_rec (x : ℝ) (hx : 0 < x) : f (x + 1) = f x + log x := by simp only [f, Function.comp_apply,
      Gamma_add_one hx.ne', log_mul hx.ne' (Gamma_pos_of_pos hx).ne', add_comm]
  have hder {x : ℝ} (hx : 0 < x) : DifferentiableAt ℝ f x := by
    refine ((differentiableAt_Gamma ?_).log (Gamma_ne_zero ?_)) <;>
    exact fun m ↦ ne_of_gt (by linarith)
  -- Express derivative at general `n` in terms of value at `1` using recurrence relation
  have hder_rec (x : ℝ) (hx : 0 < x) : deriv f (x + 1) = deriv f x + 1 / x := by
    rw [← deriv_comp_add_const, one_div, ← deriv_log,
      ← deriv_add (hder <| by positivity) (differentiableAt_log hx.ne')]
    apply EventuallyEq.deriv_eq
    filter_upwards [eventually_gt_nhds hx] using h_rec
  have hder_nat (n : ℕ) : deriv f (n + 1) = deriv f 1 + harmonic n := by
    induction n with
    | zero => simp
    | succ n hn =>
      rw [cast_succ, hder_rec (n + 1) (by positivity), hn, harmonic_succ]
      push_cast
      ring
  suffices -deriv f 1 = γ by rw [hder_nat n, ← this, neg_neg]
  -- Use convexity to show derivative of `f` at `n + 1` is between `log n` and `log (n + 1)`
  have derivLB (n : ℕ) (hn : 0 < n) : log n ≤ deriv f (n + 1) := by
    refine (le_of_eq ?_).trans <| hc.slope_le_deriv (mem_Ioi.mpr <| Nat.cast_pos.mpr hn)
      (by positivity : _ < (_ : ℝ)) (by linarith) (hder <| by positivity)
    rw [slope_def_field, show n + 1 - n = (1 : ℝ) by ring, div_one, h_rec n (by positivity),
      add_sub_cancel_left]
  have derivUB (n : ℕ) : deriv f (n + 1) ≤ log (n + 1) := by
    refine (hc.deriv_le_slope (by positivity : (0 : ℝ) < n + 1) (by positivity : (0 : ℝ) < n + 2)
        (by linarith) (hder <| by positivity)).trans (le_of_eq ?_)
    rw [slope_def_field, show n + 2 - (n + 1) = (1 : ℝ) by ring, div_one,
      show n + 2 = (n + 1) + (1 : ℝ) by ring, h_rec (n + 1) (by positivity), add_sub_cancel_left]
  -- deduce `-deriv f 1` is bounded above + below by sequences which both tend to `γ`
  apply le_antisymm
  · apply ge_of_tendsto tendsto_harmonic_sub_log
    filter_upwards [eventually_gt_atTop 0] with n hn
    rw [le_sub_iff_add_le', ← sub_eq_add_neg, sub_le_iff_le_add', ← hder_nat]
    exact derivLB n hn
  · apply le_of_tendsto tendsto_harmonic_sub_log_add_one
    filter_upwards with n
    rw [sub_le_iff_le_add', ← sub_eq_add_neg, le_sub_iff_add_le', ← hder_nat]
    exact derivUB n

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

Goal state before:
pp: f : ℂ → ℂ := fun s ↦ ↑π ^ (-s / 2)
g : ℂ → ℂ := fun s ↦ Gamma (s / 2)
⊢ ↑π ^ (1 / 2) = ↑√π

Tactic:
Real.sqrt_eq_rpow,

Goal state after:
f : ℂ → ℂ := fun s ↦ ↑π ^ (-s / 2)
g : ℂ → ℂ := fun s ↦ Gamma (s / 2)
⊢ ↑π ^ (1 / 2) = ↑(π ^ (1 / 2))
Module: Mathlib.NumberTheory.Harmonic.GammaDeriv

Goal state before:
pp: f : ℂ → ℂ := fun s ↦ ↑π ^ (-s / 2)
g : ℂ → ℂ := fun s ↦ Gamma (s / 2)
aux : ↑π ^ (1 / 2) = ↑√π
aux2 : ↑√π ≠ 0
this : HasDerivAt (fun x ↦ ↑π ^ (-x / 2)) (↑π ^ (-1 / 2) * log ↑π * (-1 / 2)) 1
⊢ HasDerivAt f (-log ↑π / 2 / ↑√π) 1

Tactic:
refine this.congr_deriv ?_

Goal state after:
f : ℂ → ℂ := fun s ↦ ↑π ^ (-s / 2)
g : ℂ → ℂ := fun s ↦ Gamma (s / 2)
aux : ↑π ^ (1 / 2) = ↑√π
aux2 : ↑√π ≠ 0
this : HasDerivAt (fun x ↦ ↑π ^ (-x / 2)) (↑π ^ (-1 / 2) * log ↑π * (-1 / 2)) 1
⊢ ↑π ^ (-1 / 2) * log ↑π * (-1 / 2) = -log ↑π / 2 / ↑√π
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 : 1 < b
n : ℕ
⊢ log b (↑b ^ (-↑n)) = -↑n

Tactic:
log_of_right_le_one _ (zpow_le_one_of_nonpos₀ (mod_cast hb.le) <|
      neg_nonpos.2 (Int.natCast_nonneg _)),

Goal state after:
case inr
R : Type u_1
inst✝³ : Semifield R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorSemiring R
b : ℕ
hb : 1 < b
n : ℕ
⊢ -↑(Nat.clog b ⌈(↑b ^ (-↑n))⁻¹⌉₊) = -↑n
Module: Mathlib.Analysis.SpecialFunctions.Log.Base

Goal state before:
pp: b x : ℝ
⊢ logb b⁻¹ x = -logb b x

Tactic:
by simp [logb, div_neg]

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

Goal state before:
pp: b x : ℝ
hb₀ : 0 < b
hb : b ≠ 1
⊢ ContinuousAt (logb b) x → x ≠ 0

Tactic:
rintro h rfl

Goal state after:
b : ℝ
hb₀ : 0 < b
hb : b ≠ 1
h : ContinuousAt (logb b) 0
⊢ False
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
a✝ : Nontrivial E
s : Set ↑(sphere 0 1)
hs : s ∈ {s | MeasurableSet s}
r : ↑(Ioi 0)
this : Ioo 0 ↑r = ↑r • Ioo 0 1
hpos : 0 < dim E
⊢ (map (⇑(homeomorphUnitSphereProd E)) (comap Subtype.val μ)) (s ×ˢ Iio r) =
    μ.toSphere s * (volumeIoiPow (dim E - 1)) (Iio r)

Tactic:
(Homeomorph.measurableEmbedding _).map_apply,

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
a✝ : Nontrivial E
s : Set ↑(sphere 0 1)
hs : s ∈ {s | MeasurableSet s}
r : ↑(Ioi 0)
this : Ioo 0 ↑r = ↑r • Ioo 0 1
hpos : 0 < dim E
⊢ (comap Subtype.val μ) (⇑(homeomorphUnitSphereProd E) ⁻¹' s ×ˢ Iio r) =
    μ.toSphere s * (volumeIoiPow (dim E - 1)) (Iio r)
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: L : PeriodPair
⊢ L.ω₂ / 2 ∉ L.lattice

Tactic:
by
  simpa [inv_mul_eq_div] using
    (L.mul_ω₁_add_mul_ω₂_mem_lattice (α := 0) (β := 1 / 2)).not.mpr (by norm_num)

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

Goal state before:
pp: E : Type u_1
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : MeasurableSpace E
F : Type u_2
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : Nontrivial E
μ : Measure E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : BorelSpace E
inst✝ : μ.IsAddHaarMeasure
f : ℝ → F
this :
  Integrable (fun x ↦ f ‖↑x‖) (Measure.comap Subtype.val μ) ↔
    Integrable (fun x ↦ f ↑x.2) (μ.toSphere.prod (Measure.volumeIoiPow (dim E - 1)))
⊢ MeasurableSet (Ioi 0)

pp: E : Type u_1
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : MeasurableSpace E
F : Type u_2
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : Nontrivial E
μ : Measure E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : BorelSpace E
inst✝ : μ.IsAddHaarMeasure
f : ℝ → F
this :
  Integrable (fun x ↦ f ‖↑x‖) (Measure.comap Subtype.val μ) ↔
    Integrable (fun x ↦ f ↑x.2) (μ.toSphere.prod (Measure.volumeIoiPow (dim E - 1)))
⊢ μ.toSphere ≠ 0

Tactic:
· measurability

Goal state after:
E : Type u_1
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : MeasurableSpace E
F : Type u_2
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : Nontrivial E
μ : Measure E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : BorelSpace E
inst✝ : μ.IsAddHaarMeasure
f : ℝ → F
this :
  Integrable (fun x ↦ f ‖↑x‖) (Measure.comap Subtype.val μ) ↔
    Integrable (fun x ↦ f ↑x.2) (μ.toSphere.prod (Measure.volumeIoiPow (dim E - 1)))
⊢ μ.toSphere ≠ 0
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: case neg
L : PeriodPair
z : ℂ
l : ↥L.lattice
hl : ↑l / 2 ∉ L.lattice
hl0 : l ≠ 0
hz : z ∉ L.lattice
this : (fun x ↦ ℘[L - 0] (x + ↑l)) z = (fun x ↦ ℘[L - 0 - ↑l] x + (1 / 0 ^ 2 - 1 / (0 - ↑l) ^ 2)) z
⊢ ℘[L] (z + ↑l) = ℘[L] z

Tactic:
simp only [zero_sub, ne_eq, OfNat.ofNat_ne_zero, not_false_eq_true, zero_pow, div_zero,
      even_two, Even.neg_pow, one_div] at this

Goal state after:
case neg
L : PeriodPair
z : ℂ
l : ↥L.lattice
hl : ↑l / 2 ∉ L.lattice
hl0 : l ≠ 0
hz : z ∉ L.lattice
this : ℘[L - 0] (z + ↑l) = ℘[L - -↑l] z + -(↑l ^ 2)⁻¹
⊢ ℘[L] (z + ↑l) = ℘[L] z
Module: Mathlib.MeasureTheory.Constructions.HaarToSphere

Goal state before:
pp: E : Type u_1
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : MeasurableSpace E
F : Type u_2
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : Nontrivial E
μ : Measure E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : BorelSpace E
inst✝ : μ.IsAddHaarMeasure
f : ℝ → F
⊢ μ.toSphere.real univ • ∫ (x : ↑(Ioi 0)), f ↑x ∂Measure.volumeIoiPow (dim E - 1) =
    dim E • μ.real (ball 0 1) • ∫ (y : ℝ) in Ioi 0, y ^ (dim E - 1) • f y

Tactic:
by
      simp only [Measure.volumeIoiPow, ENNReal.ofReal]
      rw [integral_withDensity_eq_integral_smul, μ.toSphere_real_apply_univ,
        ← nsmul_eq_mul, smul_assoc,
        integral_subtype_comap measurableSet_Ioi fun a ↦ Real.toNNReal (a ^ (dim E - 1)) • f a,
        setIntegral_congr_fun measurableSet_Ioi fun x hx ↦ ?_]
      · rw [NNReal.smul_def, Real.coe_toNNReal _ (pow_nonneg hx.out.le _)]
      · exact (measurable_subtype_coe.pow_const _).real_toNNReal

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

Goal state before:
pp: L : PeriodPair
l₀ : ↥L.lattice
z : ℂ
⊢ (℘'[L - ↑l₀] z + ∑' (i : ↥L.lattice), if ↑i = ↑l₀ then -2 / (z - ↑l₀) ^ 3 else 0) =
    -∑' (l : ↥L.lattice), 2 / (z - ↑l) ^ 3

Tactic:
derivWeierstrassPExcept,

Goal state after:
L : PeriodPair
l₀ : ↥L.lattice
z : ℂ
⊢ ((∑' (l : ↥L.lattice), if ↑l = ↑l₀ then 0 else -2 / (z - ↑l) ^ 3) +
      ∑' (i : ↥L.lattice), if ↑i = ↑l₀ then -2 / (z - ↑l₀) ^ 3 else 0) =
    -∑' (l : ↥L.lattice), 2 / (z - ↑l) ^ 3
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: L : PeriodPair
z : ℂ
⊢ ℘'[L] (-z) = -℘'[L] z

Tactic:
simp only [derivWeierstrassP]
  rw [← (Equiv.neg L.lattice).tsum_eq]
  simp only [Equiv.neg_apply, NegMemClass.coe_neg, sub_neg_eq_add, neg_add_eq_sub, neg_neg,
    ← div_neg, ← tsum_neg]
  congr! with l
  ring

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.InverseDeriv

Goal state before:
pp: x : ℝ
⊢ DifferentiableWithinAt ℝ arcsin (Ici x) x → x ≠ -1

Tactic:
rintro h rfl

Goal state after:
h : DifferentiableWithinAt ℝ arcsin (Ici (-1)) (-1)
⊢ False
Module: Mathlib.Analysis.SpecialFunctions.Stirling

Goal state before:
pp: ⊢ stirlingSeq 1 = rexp 1 / √2

Tactic:
by
  rw [stirlingSeq, pow_one, factorial_one, cast_one, mul_one, mul_one_div, one_div_div]

Goal state after:
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.ContDiff

Goal state before:
pp: case inr
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
inst✝ : CompleteSpace E
hab : b < a
h : ContDiffOn ℝ 1 f (Icc b a)
⊢ -∫ (x : ℝ) in b..a, derivWithin f (Icc b a) x = f b - f a

Tactic:
integral_derivWithin_Icc_of_contDiffOn_Icc h hab.le

Goal state after:
case inr
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
inst✝ : CompleteSpace E
hab : b < a
h : ContDiffOn ℝ 1 f (Icc b a)
⊢ -(f a - f b) = f b - f a
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.ContDiff

Goal state before:
pp: E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
h : ContDiffOn ℝ 1 f (Icc a b)
hab : a ≤ b
g : E →ₗᵢ[ℝ] UniformSpace.Completion E := ⋯
this : ‖(⇑g ∘ f) b - (⇑g ∘ f) a‖ₑ = ‖f b - f a‖ₑ
⊢ ∫⁻ (a : ℝ) in Icc a b, ‖deriv (⇑g ∘ f) a‖ₑ ∂volume ≤ ∫⁻ (x : ℝ) in Icc a b, ‖deriv f x‖ₑ

Tactic:
apply lintegral_mono_ae

Goal state after:
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
h : ContDiffOn ℝ 1 f (Icc a b)
hab : a ≤ b
g : E →ₗᵢ[ℝ] UniformSpace.Completion E := ⋯
this : ‖(⇑g ∘ f) b - (⇑g ∘ f) a‖ₑ = ‖f b - f a‖ₑ
⊢ ∀ᵐ (a : ℝ) ∂volume.restrict (Icc a b), ‖deriv (⇑g ∘ f) a‖ₑ ≤ ‖deriv f a‖ₑ
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.ContDiff

Goal state before:
pp: E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
h : ContDiffOn ℝ 1 f (Icc a b)
hab : a ≤ b
⊢ ‖f b - f a‖ₑ ≤ ∫⁻ (x : ℝ) in Icc a b, ‖deriv f x‖ₑ

Tactic:
let g := UniformSpace.Completion.toComplₗᵢ (𝕜 := ℝ) (E := E)
  have : ‖(g ∘ f) b - (g ∘ f) a‖ₑ = ‖f b - f a‖ₑ := by
    rw [← edist_eq_enorm_sub, Function.comp_def, g.isometry.edist_eq, edist_eq_enorm_sub]
  rw [← this, ← integral_deriv_of_contDiffOn_Icc (g.contDiff.comp_contDiffOn h) hab,
    integral_of_le hab, restrict_Ioc_eq_restrict_Icc]
  apply (enorm_integral_le_lintegral_enorm _).trans
  apply lintegral_mono_ae
  rw [← restrict_Ioo_eq_restrict_Icc]
  filter_upwards [self_mem_ae_restrict measurableSet_Ioo] with x hx
  rw [fderiv_comp_deriv]; rotate_left
  · exact (g.contDiff.differentiable one_ne_zero).differentiableAt
  · exact (h x ⟨hx.1.le, hx.2.le⟩).contDiffAt (Icc_mem_nhds hx.1 hx.2)
      |>.differentiableAt one_ne_zero
  have : fderiv ℝ g (f x) = g.toContinuousLinearMap := g.toContinuousLinearMap.fderiv
  simp [this]

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

Goal state before:
pp: case inr
n i : ℕ
hi : i ≤ n
hn : n ≠ 0
h₁ : 0 < (-1) ^ i * ∏ x ∈ Finset.range i, (node n i - node n x)
h₂ : 0 < ∏ j ∈ Finset.Ioc i n, (node n i - node n j)
union : (Finset.range (n + 1)).erase i = Finset.range i ∪ Finset.Ioc i n
disjoint : Disjoint (Finset.range i) (Finset.Ioc i n)
⊢ 0 < ((-1) ^ i * ∏ x ∈ Finset.range i, (node n i - node n x)) * ∏ x ∈ Finset.Ioc i n, (node n i - node n x)

Tactic:
exact mul_pos h₁ h₂

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

Goal state before:
pp: 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
x : ℝ
hx : x ∈ Finset.image (fun x ↦ node n x) (Finset.range (n + 1))
hPx : eval x P ≠ eval x (T ℝ ↑n)
i✝ : ℕ
hix : node n i✝ = x
hi✝ : i✝ ∈ Finset.Iic n
i : ℕ
hi : i ∈ Finset.Iic n
⊢ (-1) ^ i * eval (node n i) P * ((-1) ^ i * c i) ≤ (-1) ^ i * eval (node n i) (T ℝ ↑n) * ((-1) ^ i * c i)

Tactic:
refine mul_le_mul_of_nonneg_right ?_ (le_of_lt (hcpos i (Finset.mem_Iic.mp hi)))

Goal state after:
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
x : ℝ
hx : x ∈ Finset.image (fun x ↦ node n x) (Finset.range (n + 1))
hPx : eval x P ≠ eval x (T ℝ ↑n)
i✝ : ℕ
hix : node n i✝ = x
hi✝ : i✝ ∈ Finset.Iic n
i : ℕ
hi : i ∈ Finset.Iic n
⊢ (-1) ^ i * eval (node n i) P ≤ (-1) ^ i * eval (node n i) (T ℝ ↑n)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema

Goal state before:
pp: n : ℤ
x : ℝ
hx : 1 ≤ x
⊢ 1 ≤ eval x (T ℝ n)

Tactic:
rw [← cosh_arcosh hx]

Goal state after:
n : ℤ
x : ℝ
hx : 1 ≤ x
⊢ 1 ≤ eval (cosh (arcosh x)) (T ℝ n)
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable

Goal state before:
pp: z : ℍ
x : Fin 2 → ℤ
hx : x ≠ 0
hn0 : ‖x‖ ≠ 0
h11 : ↑(x 0) * ↑z + ↑(x 1) = (↑(x 0) / ↑‖x‖ * ↑z + ↑(x 1) / ↑‖x‖) * ↑‖x‖
⊢ r z * ↑(max (x 0).natAbs (x 1).natAbs) ≤ ‖↑(x 0) / ↑‖x‖ * ↑z + ↑(x 1) / ↑‖x‖‖ * ‖↑‖x‖‖

Tactic:
norm_real,

Goal state after:
z : ℍ
x : Fin 2 → ℤ
hx : x ≠ 0
hn0 : ‖x‖ ≠ 0
h11 : ↑(x 0) * ↑z + ↑(x 1) = (↑(x 0) / ↑‖x‖ * ↑z + ↑(x 1) / ↑‖x‖) * ↑‖x‖
⊢ r z * ↑(max (x 0).natAbs (x 1).natAbs) ≤ ‖↑(x 0) / ↑‖x‖ * ↑z + ↑(x 1) / ↑‖x‖‖ * ‖‖x‖‖
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema

Goal state before:
pp: case mp
n : ℕ
hn : n ≠ 0
x : ℝ
hTx : |eval x (T ℝ ↑n)| = 1
⊢ ∃ k ≤ n, x = cos (↑k * π / ↑n)

Tactic:
have hx := (abs_eval_T_real_le_one_iff (Nat.cast_ne_zero.mpr hn) x).mpr (le_of_eq hTx)

Goal state after:
case mp
n : ℕ
hn : n ≠ 0
x : ℝ
hTx : |eval x (T ℝ ↑n)| = 1
hx : |x| ≤ 1
⊢ ∃ k ≤ n, x = cos (↑k * π / ↑n)
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable

Goal state before:
pp: case hΘ
c e : ℤ
z : ℂ
⊢ (fun d ↦ ↑c * z + ↑d) =Θ[cofinite] fun n ↦ ↑n

Tactic:
refine Asymptotics.IsLittleO.add_isTheta ?_ (Int.cast_complex_isTheta_cast_real)

Goal state after:
case hΘ
c e : ℤ
z : ℂ
⊢ (fun d ↦ ↑c * z) =o[cofinite] fun n ↦ ↑n
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema

Goal state before:
pp: case inr
n : ℕ
this : ∀ (n : ℕ), n ≠ 0 → (Multiset.map (fun k ↦ cos ((2 * ↑k + 1) * π / (2 * ↑n))) (Multiset.range n)).Nodup
hn : n = 0
⊢ (Multiset.map (fun k ↦ cos ((2 * ↑k + 1) * π / (2 * ↑n))) (Multiset.range n)).Nodup

pp: n : ℕ
hn : n ≠ 0
⊢ (Multiset.map (fun k ↦ cos ((2 * ↑k + 1) * π / (2 * ↑n))) (Multiset.range n)).Nodup

Tactic:
· simp [hn]

Goal state after:
n : ℕ
hn : n ≠ 0
⊢ (Multiset.map (fun k ↦ cos ((2 * ↑k + 1) * π / (2 * ↑n))) (Multiset.range n)).Nodup
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: L : PeriodPair
n : ℕ
hn : Odd n
⊢ L.G n = -L.G n

Tactic:
G,

Goal state after:
L : PeriodPair
n : ℕ
hn : Odd n
⊢ ∑' (l : ↥L.lattice), (↑l ^ n)⁻¹ = -∑' (l : ↥L.lattice), (↑l ^ n)⁻¹
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema

Goal state before:
pp: case inr
n : ℕ
this :
  ∀ (n : ℕ), n ≠ 0 → (T ℝ ↑n).roots = (Finset.image (fun k ↦ cos ((2 * ↑k + 1) * π / (2 * ↑n))) (Finset.range n)).val
hn : n = 0
⊢ (T ℝ ↑n).roots = (Finset.image (fun k ↦ cos ((2 * ↑k + 1) * π / (2 * ↑n))) (Finset.range n)).val

pp: n : ℕ
hn : n ≠ 0
⊢ (T ℝ ↑n).roots = (Finset.image (fun k ↦ cos ((2 * ↑k + 1) * π / (2 * ↑n))) (Finset.range n)).val

Tactic:
· simp [hn]

Goal state after:
n : ℕ
hn : n ≠ 0
⊢ (T ℝ ↑n).roots = (Finset.image (fun k ↦ cos ((2 * ↑k + 1) * π / (2 * ↑n))) (Finset.range n)).val
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal

Goal state before:
pp: case e'_2
n : ℕ
P : ℝ[X]
k : ℕ
hk₁ : 0 < k
hk₂ : k ≤ n
x : ℝ
hx : 1 ≤ x
hPdeg : P.degree ≤ ↑n
hPbnd : ∀ x ∈ Set.Icc (-1) 1, |eval x P| ≤ 1
⊢ eval x ((⇑derivative)^[k] P) = sumNodes n (fun i ↦ iterateDerivativeC n k x i) P

pp: case e'_3
n : ℕ
P : ℝ[X]
k : ℕ
hk₁ : 0 < k
hk₂ : k ≤ n
x : ℝ
hx : 1 ≤ x
hPdeg : P.degree ≤ ↑n
hPbnd : ∀ x ∈ Set.Icc (-1) 1, |eval x P| ≤ 1
⊢ eval x ((⇑derivative)^[k] (T ℝ ↑n)) = sumNodes n (fun i ↦ iterateDerivativeC n k x i) (T ℝ ↑n)

Tactic:
· rw [sumNodes_eq_eval_iterate_derivative hk₂ x hPdeg]

Goal state after:
case e'_3
n : ℕ
P : ℝ[X]
k : ℕ
hk₁ : 0 < k
hk₂ : k ≤ n
x : ℝ
hx : 1 ≤ x
hPdeg : P.degree ≤ ↑n
hPbnd : ∀ x ∈ Set.Icc (-1) 1, |eval x P| ≤ 1
⊢ eval x ((⇑derivative)^[k] (T ℝ ↑n)) = sumNodes n (fun i ↦ iterateDerivativeC n k x i) (T ℝ ↑n)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal

Goal state before:
pp: case e'_3
n : ℕ
P : ℝ[X]
k : ℕ
hk₁ : 0 < k
hk₂ : k ≤ n
x : ℝ
hx : 1 ≤ x
hPdeg : P.degree ≤ ↑n
hPbnd : ∀ x ∈ Set.Icc (-1) 1, |eval x P| ≤ 1
⊢ eval x ((⇑derivative)^[k] (T ℝ ↑n)) = sumNodes n (fun i ↦ iterateDerivativeC n k x i) (T ℝ ↑n)

Tactic:
· rw [sumNodes_eq_eval_iterate_derivative hk₂ x (le_of_eq (degree_T ℝ n))]

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

Goal state before:
pp: case inr
n : ℕ
this : ∀ (n : ℕ), n ≠ 0 → (U ℝ ↑n).roots = (Finset.image (fun k ↦ cos ((↑k + 1) * π / (↑n + 1))) (Finset.range n)).val
hn : n = 0
⊢ (U ℝ ↑n).roots = (Finset.image (fun k ↦ cos ((↑k + 1) * π / (↑n + 1))) (Finset.range n)).val

pp: n : ℕ
hn : n ≠ 0
⊢ (U ℝ ↑n).roots = (Finset.image (fun k ↦ cos ((↑k + 1) * π / (↑n + 1))) (Finset.range n)).val

Tactic:
· simp [hn]

Goal state after:
n : ℕ
hn : n ≠ 0
⊢ (U ℝ ↑n).roots = (Finset.image (fun k ↦ cos ((↑k + 1) * π / (↑n + 1))) (Finset.range n)).val
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent

Goal state before:
pp: case refine_1
Z : Set ℂ
hZ : IsCompact Z
hf : ContinuousOn (fun x ↦ ‖-x ^ 2‖) Z
s : ℝ
hs : ∀ y ∈ (fun x ↦ ‖-x ^ 2‖) '' Z, y ≤ s
⊢ Summable fun n ↦ ‖↑s / (↑n + 1) ^ 2‖

Tactic:
simpa using summable_pow_div_add (s : ℂ) 2 1 (Nat.one_lt_two)

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent

Goal state before:
pp: x : ℂ
hz : x ∈ ℂ_ℤ
this : Summable fun n ↦ (x - ↑(n + 1))⁻¹ * (x + ↑(n + 1))⁻¹
⊢ Summable fun i ↦ 1 / ((x + (↑i + 1)) * (x - (↑i + 1)))

Tactic:
simpa using this

Goal state after: