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

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

Tactic:
apply norm_integral_le_abs_of_norm_le
        · exact (ae_restrict_mem measurableSet_uIoc).mono fun x hx ↦ by
            have hx_pos : 0 < x :=
              lt_of_lt_of_le (lt_min ha hb) (uIoc_subset_uIcc hx).1
            rw [norm_smul, Real.norm_eq_abs, abs_of_pos (inv_pos.2 hx_pos)]
            exact mul_le_mul_of_nonneg_left (h x hx) (inv_nonneg.2 hx_pos.le)
        · exact hint_inv

Goal state after:
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
⊢ t ^ (p - 1) / t * x = t ^ (p - 2) * x

Tactic:
by
    congr
    rw [← Real.rpow_sub_one (by positivity)]
    congr 1
    ring

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

Goal state before:
pp: p t : ℝ
hp : p ∈ Ioo 0 1
ht : 1 ≤ t
⊢ 1 / 2 * t ^ (p - 2) = t ^ (p - 1) * (1 / 2 * 1 / t)

Tactic:
have : p - 2 = p - 1 - 1 := by ring
            rw [this, Real.rpow_sub (by linarith), Real.rpow_one]
            ring

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

Goal state before:
pp: case refine_2
p : ℝ
hp : p ∈ Ioo 0 1
⊢ Ioi 1 ≤ᵐ[volume] Ioi 0

Tactic:
· exact .of_forall <| Set.Ioi_subset_Ioi zero_le_one

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

Goal state before:
pp: s : ℂ
hs : ∀ (m : ℕ), s ≠ -↑m
hs0 : s ≠ 0
⊢ (s + 1).digamma = s.digamma + s⁻¹

Tactic:
rw [digamma_def, logDeriv_apply, logDeriv_apply, deriv_Gamma_add_one s hs0, Gamma_add_one s hs0,
    add_div, div_mul_cancel_right₀ (Gamma_ne_zero hs), mul_div_mul_left _ _ hs0, add_comm]

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

Goal state before:
pp: A : Type u_1
inst✝⁸ : NonUnitalNormedRing A
inst✝⁷ : StarRing A
inst✝⁶ : NormedSpace ℝ A
inst✝⁵ : SMulCommClass ℝ A A
inst✝⁴ : IsScalarTower ℝ A A
inst✝³ : PartialOrder A
inst✝² : StarOrderedRing A
inst✝¹ : NonnegSpectrumClass ℝ A
inst✝ : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
p t : ℝ
hp : p ∈ Ioo 0 1
ht : 0 < t
a : A
ha : 0 ≤ a
hspec : quasispectrum ℝ a ⊆ Ici 0
h_mapsTo : MapsTo (fun x ↦ t⁻¹ • x) (Ici 0) (Ici 0)
⊢ t ^ (p - 1) • cfcₙ (fun x ↦ p.rpowIntegrand₀₁ 1 (t⁻¹ • x)) a = t ^ (p - 1) • cfcₙ (p.rpowIntegrand₀₁ 1) (t⁻¹ • a)

Tactic:
congr! 1

Goal state after:
A : Type u_1
inst✝⁸ : NonUnitalNormedRing A
inst✝⁷ : StarRing A
inst✝⁶ : NormedSpace ℝ A
inst✝⁵ : SMulCommClass ℝ A A
inst✝⁴ : IsScalarTower ℝ A A
inst✝³ : PartialOrder A
inst✝² : StarOrderedRing A
inst✝¹ : NonnegSpectrumClass ℝ A
inst✝ : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
p t : ℝ
hp : p ∈ Ioo 0 1
ht : 0 < t
a : A
ha : 0 ≤ a
hspec : quasispectrum ℝ a ⊆ Ici 0
h_mapsTo : MapsTo (fun x ↦ t⁻¹ • x) (Ici 0) (Ici 0)
⊢ cfcₙ (fun x ↦ p.rpowIntegrand₀₁ 1 (t⁻¹ • x)) a = cfcₙ (p.rpowIntegrand₀₁ 1) (t⁻¹ • a)
Module: Mathlib.NumberTheory.Harmonic.GammaDeriv

Goal state before:
pp: ⊢ γ = -deriv Gamma 1

Tactic:
rw [show (1 : ℝ) = ↑(0 : ℕ) + 1 by simp, deriv_Gamma_nat 0]

Goal state after:
⊢ γ = -(↑0! * (-γ + ↑(harmonic 0)))
Module: Mathlib.Analysis.SpecialFunctions.Gaussian.PoissonSummation

Goal state before:
pp: a : ℂ
ha : 0 < a.re
⊢ ∑' (n : ℤ), cexp (-↑π * a * ↑n ^ 2) = 1 / a ^ (1 / 2) * ∑' (n : ℤ), cexp (-↑π / a * ↑n ^ 2)

Tactic:
simpa only [mul_zero, zero_mul, add_zero] using Complex.tsum_exp_neg_quadratic ha 0

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

Goal state before:
pp: case inl
R : Type u_1
inst✝³ : Semifield R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorSemiring R
b : ℕ
hb : b ≤ 1
r : R
h : 1 ≤ r
⊢ ↑0 = 0

Tactic:
Int.ofNat_zero

Goal state after:
case inl
R : Type u_1
inst✝³ : Semifield R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorSemiring R
b : ℕ
hb : b ≤ 1
r : R
h : 1 ≤ r
⊢ 0 = 0
Module: Mathlib.Data.Int.Log

Goal state before:
pp: R : Type u_1
inst✝³ : Semifield R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorSemiring R
b : ℕ
⊢ ↑0 = 0

Tactic:
Int.ofNat_zero

Goal state after:
R : Type u_1
inst✝³ : Semifield R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorSemiring R
b : ℕ
⊢ 0 = 0
Module: Mathlib.Analysis.SpecialFunctions.Log.Base

Goal state before:
pp: b x y : ℝ
hx : 0 < x
⊢ logb b (x ^ y) = y * logb b x

Tactic:
rw [logb, log_rpow hx, logb, mul_div_assoc]

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

Goal state before:
pp: R : Type u_1
inst✝³ : Semifield R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorSemiring R
b : ℕ
r : R
hb : 1 < b
hr : 0 < r
⊢ ↑b ^ (clog b r - 1) < r

Tactic:
rw [← neg_log_inv_eq_clog, ← neg_add', zpow_neg, inv_lt_comm₀ _ hr]

Goal state after:
R : Type u_1
inst✝³ : Semifield R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorSemiring R
b : ℕ
r : R
hb : 1 < b
hr : 0 < r
⊢ r⁻¹ < ↑b ^ (log b r⁻¹ + 1)

R : Type u_1
inst✝³ : Semifield R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorSemiring R
b : ℕ
r : R
hb : 1 < b
hr : 0 < r
⊢ 0 < ↑b ^ (log b r⁻¹ + 1)
Module: Mathlib.Analysis.SpecialFunctions.MulExpNegMulSq

Goal state before:
pp: ε : ℝ
hε : 0 < ε
x : ℝ
⊢ ↑‖deriv ε.mulExpNegMulSq x‖₊ ≤ ↑1

Tactic:
coe_nnnorm

Goal state after:
ε : ℝ
hε : 0 < ε
x : ℝ
⊢ ‖deriv ε.mulExpNegMulSq x‖ ≤ ↑1
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
⊢ Int.clog b r ≤ ⌈logb (↑b) r⌉

Tactic:
← Int.le_zpow_iff_clog_le hb hr,

Goal state after:
case a
b : ℕ
r : ℝ
hr✝ : 0 ≤ r
hr : 0 < r
hb : 1 < b
hb1' : 1 < ↑b
⊢ r ≤ ↑b ^ ⌈logb (↑b) r⌉
Module: Mathlib.Analysis.SpecialFunctions.Log.Base

Goal state before:
pp: b✝ b : ℝ
hb : b ≠ -1 ∧ b ≠ 0 ∧ b ≠ 1
hb₀ : 0 < b
hb₁ : 1 < b
x : ℝ
hx₁ : 1 ≤ x
⊢ 0 ≤ logb b x

Tactic:
exact logb_nonneg hb₁ hx₁

Goal state after:
Module: Mathlib.MeasureTheory.Integral.BoundedContinuousFunction

Goal state before:

Tactic:
‖∫ x, f x ∂μ‖
    _ ≤ ∫ x, ‖f x‖ ∂μ := norm_integral_le_integral_norm _
    _ ≤ ∫ _, ‖f‖ ∂μ := ?_
    _ = μ.real Set.univ • ‖f‖ := by rw [integral_const]

Goal state after:
X : Type u_1
inst✝⁸ : MeasurableSpace X
inst✝⁷ : TopologicalSpace X
μ : Measure X
E : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : OpensMeasurableSpace X
inst✝⁴ : SecondCountableTopology E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : NormedSpace ℝ E
inst✝ : IsFiniteMeasure μ
f : X →ᵇ E
⊢ ∫ (x : X), ‖f x‖ ∂μ ≤ ∫ (x : X), ‖f‖ ∂μ
Module: Mathlib.Analysis.SpecialFunctions.Log.Base

Goal state before:
pp: b : ℝ
⊢ logb b =O[⊤] log

Tactic:
by
  by_cases! h : b = -1 ∨ b = 0 ∨ b = 1
  · obtain rfl | rfl | rfl := h
    all_goals simpa [-Asymptotics.isBigO_top] using! Asymptotics.isBigO_zero log ⊤
  · simpa [logb, div_eq_mul_inv, mul_comm]
      using! (Asymptotics.isBigO_refl log ⊤).const_mul_left (log b)⁻¹

Goal state after:
Module: Mathlib.MeasureTheory.Integral.BoundedContinuousFunction

Goal state before:
pp: X : Type u_1
inst✝⁴ : TopologicalSpace X
inst✝³ : MeasurableSpace X
inst✝² : OpensMeasurableSpace X
ι : Type u_2
L : Filter ι
μ : Measure X
inst✝¹ : IsProbabilityMeasure μ
μs : ι → Measure X
inst✝ : ∀ (i : ι), IsProbabilityMeasure (μs i)
h : ∀ (f : X →ᵇ ℝ), 0 ≤ f → limsup (fun i ↦ ∫ (x : X), f x ∂μs i) L ≤ ∫ (x : X), f x ∂μ
f : X →ᵇ ℝ
hL : L.NeBot
obs : Bornology.IsBounded (Set.range fun i ↦ ∫ (x : X), f x ∂μs i)
bdd_above : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) L fun i ↦ ∫ (x : X), f x ∂μs i
bdd_below : IsBoundedUnder (fun x1 x2 ↦ x2 ≤ x1) L fun i ↦ ∫ (x : X), f x ∂μs i
⊢ ∫ (x : X), f x ∂μ ≤ liminf (fun i ↦ ∫ (x : X), f x ∂μs i) L

pp: X : Type u_1
inst✝⁴ : TopologicalSpace X
inst✝³ : MeasurableSpace X
inst✝² : OpensMeasurableSpace X
ι : Type u_2
L : Filter ι
μ : Measure X
inst✝¹ : IsProbabilityMeasure μ
μs : ι → Measure X
inst✝ : ∀ (i : ι), IsProbabilityMeasure (μs i)
h : ∀ (f : X →ᵇ ℝ), 0 ≤ f → limsup (fun i ↦ ∫ (x : X), f x ∂μs i) L ≤ ∫ (x : X), f x ∂μ
f : X →ᵇ ℝ
hL : L.NeBot
obs : Bornology.IsBounded (Set.range fun i ↦ ∫ (x : X), f x ∂μs i)
bdd_above : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) L fun i ↦ ∫ (x : X), f x ∂μs i
bdd_below : IsBoundedUnder (fun x1 x2 ↦ x2 ≤ x1) L fun i ↦ ∫ (x : X), f x ∂μs i
⊢ limsup (fun i ↦ ∫ (x : X), f x ∂μs i) L ≤ ∫ (x : X), f x ∂μ

Tactic:
· have key := h _ (f.norm_sub_nonneg)
    simp_rw [f.integral_const_sub ‖f‖] at key
    simp only [probReal_univ, smul_eq_mul, one_mul] at key
    have := limsup_const_sub L (fun i ↦ ∫ x, f x ∂(μs i)) ‖f‖ bdd_above.isCobounded_ge bdd_below
    rwa [this, _root_.sub_le_sub_iff_left ‖f‖] at key

Goal state after:
X : Type u_1
inst✝⁴ : TopologicalSpace X
inst✝³ : MeasurableSpace X
inst✝² : OpensMeasurableSpace X
ι : Type u_2
L : Filter ι
μ : Measure X
inst✝¹ : IsProbabilityMeasure μ
μs : ι → Measure X
inst✝ : ∀ (i : ι), IsProbabilityMeasure (μs i)
h : ∀ (f : X →ᵇ ℝ), 0 ≤ f → limsup (fun i ↦ ∫ (x : X), f x ∂μs i) L ≤ ∫ (x : X), f x ∂μ
f : X →ᵇ ℝ
hL : L.NeBot
obs : Bornology.IsBounded (Set.range fun i ↦ ∫ (x : X), f x ∂μs i)
bdd_above : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) L fun i ↦ ∫ (x : X), f x ∂μs i
bdd_below : IsBoundedUnder (fun x1 x2 ↦ x2 ≤ x1) L fun i ↦ ∫ (x : X), f x ∂μs i
⊢ limsup (fun i ↦ ∫ (x : X), f x ∂μs i) L ≤ ∫ (x : X), f x ∂μ
Module: Mathlib.MeasureTheory.Measure.RegularityCompacts

Goal state before:
pp: α : Type u_1
inst✝⁵ : MeasurableSpace α
inst✝⁴ : TopologicalSpace α
inst✝³ : SecondCountableTopology α
inst✝² : IsCompletelyPseudoMetrizableSpace α
inst✝¹ : OpensMeasurableSpace α
P : Measure α
inst✝ : IsFiniteMeasure P
ε : ℝ≥0∞
hε : 0 < ε
this : UpgradedIsCompletelyPseudoMetrizableSpace α := upgradeIsCompletelyPseudoMetrizable α
h✝ : Nonempty α
seq : ℕ → α := denseSeq α
hseq_dense : DenseRange seq
t : ℕ → SetRel α α
h_basis : (𝓤 α).HasAntitoneBasis t
htu : ∀ (i : ℕ), t i ∈ 𝓤 α
hto : ∀ (i : ℕ), IsOpen (t i)
a✝ : ∀ (i : ℕ), (t i).IsSymm
f : ℕ → ℕ → Set α := fun n m ↦ UniformSpace.ball (seq m) (t n)
h_univ : ∀ (n : ℕ), ⋃ m, f n m = univ
s' : ℕ → ℝ≥0∞ → ℕ
s'bound : ∀ (n : ℕ) (ε : ℝ≥0∞), 0 < ε → P (⋂ m', ⋂ (_ : m' ≤ s' n ε), (f n m')ᶜ) < ε
δ : ℕ → ℝ≥0∞
hδ1 : ∀ (i : ℕ), 0 < δ i
hδ2 : ∑' (i : ℕ), δ i < ε
u : ℕ → ℕ := fun n ↦ s' n (δ n)
n : ℕ
h'' : ∀ (n : ℕ), Prod.swap ⁻¹' t n = t n
⊢ P (⋂ i, ⋂ (_ : i ≤ u n), (UniformSpace.ball (seq i) (t n))ᶜ) ≤ δ n

Tactic:
exact (s'bound n (δ n) (hδ1 n)).le

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

Goal state before:
pp: k n : ℕ
⊢ ↑k < ↑n - 1 → 0 ↑k = ↑(k.descFactorial n)

Tactic:
eq_comm,

Goal state after:
k n : ℕ
⊢ ↑k < ↑n - 1 → ↑(k.descFactorial n) = 0 ↑k
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
x : ℝ
⊢ (x ^ (p - 1 + 1) - 0 ^ (p - 1 + 1)) / (p - 1 + 1) = x ^ p / p

Tactic:
simp [Real.zero_rpow p_pos.ne.symm]

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

Goal state before:
pp: L : PeriodPair
⊢ L.lattice = Submodule.span ℤ (Set.range ⇑L.basis)

Tactic:
have : Finset.univ (α := Fin 2) = {0, 1} := rfl
  rw [lattice, ← Set.image_univ, ← Finset.coe_univ, this]
  simp [Set.image_insert_eq]

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
μ : Measure E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
inst✝ : μ.IsAddHaarMeasure
ε : ℝ
hε : 0 < ε
x : ↑(sphere 0 1)
this✝ : Nontrivial E
this : ∀ {ε : ℝ}, 0 < ε → ε ≤ 2 → ↑(toSphereBallBound (dim E) ε) * μ (ball 0 1) ≤ μ.toSphere (ball x ε)
hε₂ : ¬ε ≤ 2
⊢ μ.toSphere (ball x (min ε 2)) ≤ μ.toSphere (ball x ε)

Tactic:
gcongr
      simp

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

Goal state before:
pp: n : ℕ
a : Multiset ℂ
hn : n ≠ 0
⊢ (Multiset.map (fun j ↦ ↑n * (j / ↑n + 1)) a).prod = ↑n ^ a.card * (Multiset.map (fun x ↦ x / ↑n + 1) a).prod

Tactic:
by
    simp [Multiset.prod_map_mul]

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

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

Tactic:
by
  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.Stirling

Goal state before:
pp: case succ
n : ℕ
r : ℝ := (1 / (2 * (↑n + 1) + 1)) ^ 2
hr : r = (1 / (2 * (↑n + 1) + 1)) ^ 2
⊢ log (stirlingSeq (n + 1)) - log (stirlingSeq (n + 1 + 1)) ≤ 1 / (12 * ↑(n + 1) * (↑(n + 1) + 1))

Tactic:
have hr1 : r < 1 := by grw [hr, ← n.zero_le]; norm_num

Goal state after:
case succ
n : ℕ
r : ℝ := (1 / (2 * (↑n + 1) + 1)) ^ 2
hr : r = (1 / (2 * (↑n + 1) + 1)) ^ 2
hr1 : r < 1
⊢ log (stirlingSeq (n + 1)) - log (stirlingSeq (n + 1 + 1)) ≤ 1 / (12 * ↑(n + 1) * (↑(n + 1) + 1))
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: L : PeriodPair
l₀ x : ℂ
i : ℕ
hl₀ : l₀ ∈ L.lattice
⊢ (↑i + 2) * (L.sumInvPow x (i + 3) - ∑' (l : ↥L.lattice), if l = ⟨l₀, hl₀⟩ then (l₀ - x) ^ (-↑(i + 3)) else 0) =
    ∑' (l : ↥L.lattice),
      if ↑l = l₀ then 0 else (↑(i + 1) + 1) * (↑l - x) ^ (-↑(i + 1 + 2)) - Nat.casesOn (i + 1) (↑l ^ (-2)) 0

Tactic:
rw [sumInvPow, ← (hasSum_sumInvPow _ _ (by linarith)).summable.tsum_sub, ← tsum_mul_left]
        · simp_rw [Subtype.ext_iff, zpow_neg]
          congr with l
          split_ifs with e
          · simp only [e, zpow_natCast, sub_self, mul_zero]
          · dsimp; norm_cast; ring
        · exact summable_of_hasFiniteSupport ((Set.finite_singleton ⟨l₀, hl₀⟩).subset (by simp))

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

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

Tactic:
obtain ⟨m, hx⟩ := Complex.exp_eq_one_iff.mp hk

Goal state after:
n : ℕ
k : ℤ
hn : n ≠ 0
hk : Complex.exp (↑k / ↑n * ↑π * I) = 1
m : ℤ
hx : ↑k / ↑n * ↑π * I = ↑m * (2 * ↑π * I)
⊢ 2 * ↑n ∣ k
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Orthogonality

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

Tactic:
exact integral_eval_T_real_measureT_zero

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

Goal state before:
pp: case inr
n : ℕ
k : ℤ
hk : ¬2 * ↑n ∣ k
hn : n ≠ 0
⊢ ∑ i ∈ range n, 2 * ↑(cos (↑k * ((2 * ↑i + 1) / (2 * ↑n) * π))) = 0

Tactic:
suffices ∑ i ∈ range n, 2 * Complex.cos (k * ((2 * i + 1) / (2 * n) * π)) = 0 by aesop

Goal state after:
case inr
n : ℕ
k : ℤ
hk : ¬2 * ↑n ∣ k
hn : n ≠ 0
⊢ ∑ i ∈ range n, 2 * Complex.cos (↑k * ((2 * ↑i + 1) / (2 * ↑n) * ↑π)) = 0
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
⊢ (T ℝ ↑n).degree < ↑(Finset.image (fun x ↦ node n x) (Finset.range (n + 1))).card

Tactic:
degree_T,

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).natAbs < ↑(Finset.image (fun x ↦ node n x) (Finset.range (n + 1))).card
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
⊢ (T ℝ ↑n).degree < ↑(Finset.image (fun x ↦ node n x) (Finset.range (n + 1))).card

pp: case eval_fg
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
⊢ ∀ x ∈ Finset.image (fun x ↦ node n x) (Finset.range (n + 1)), eval x P = eval x (T ℝ ↑n)

Tactic:
· rw [degree_T, Int.natAbs_natCast, Nat.cast_lt,
      Finset.card_image_of_injOn (strictAntiOn_node n).injOn,
      Finset.card_range, Nat.lt_succ_iff]

Goal state after:
case eval_fg
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
⊢ ∀ x ∈ Finset.image (fun x ↦ node n x) (Finset.range (n + 1)), eval x P = eval x (T ℝ ↑n)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal

Goal state before:
pp: case eval_fg
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 ≤ n, (-1) ^ i * eval (node n i) P * ((-1) ^ i * c i) <
    ∑ i ≤ n, (-1) ^ i * eval (node n i) (T ℝ ↑n) * ((-1) ^ i * c i)

Tactic:
have h_le {i : ℕ} (hi : i ∈ Finset.Iic n) :
    (-1) ^ i * P.eval (node n i) * ((-1) ^ i * c i) ≤
    (-1) ^ i * (T ℝ n).eval (node n i) * ((-1) ^ i * c i) := by
    refine mul_le_mul_of_nonneg_right ?_ (le_of_lt (hcpos i (Finset.mem_Iic.mp hi)))
    rw [eval_T_real_node hi, ← neg_pow', neg_neg, one_pow]
    exact negOnePow_mul_le (hPbnd _ node_mem_Icc)

Goal state after:
case eval_fg
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
h_le :
  ∀ {i : ℕ},
    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)
⊢ ∑ i ≤ n, (-1) ^ i * eval (node n i) P * ((-1) ^ i * c i) <
    ∑ i ≤ n, (-1) ^ i * eval (node n i) (T ℝ ↑n) * ((-1) ^ i * c i)
Module: Mathlib.NumberTheory.Niven

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

Tactic:
rw [hr'] at hr

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

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

Tactic:
rw [hr'] at hr

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

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

Tactic:
rw [hr'] at hr

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

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

Tactic:
rw [hr'] at hr

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

Goal state before:
pp: x : Fin 2 → ℤ
hx : x ≠ 0
⊢ 1 ≤ (↑(x 0) / ‖x‖) ^ 2 ∨ 1 ≤ (↑(x 1) / ‖x‖) ^ 2

Tactic:
refine (max_choice (x 0).natAbs (x 1).natAbs).imp (fun H0 ↦ ?_) (fun H1 ↦ ?_)
  · have : x 0 ≠ 0 := by
      rwa [← norm_ne_zero_iff, norm_eq_max_natAbs, H0, Nat.cast_ne_zero, Int.natAbs_ne_zero] at hx
    simp only [norm_eq_max_natAbs, H0, Nat.cast_natAbs, Int.cast_abs, div_pow, sq_abs, ne_eq,
      OfNat.ofNat_ne_zero, not_false_eq_true, pow_eq_zero_iff, Int.cast_eq_zero, this, div_self,
      le_refl]
  · have : x 1 ≠ 0 := by
      rwa [← norm_ne_zero_iff, norm_eq_max_natAbs, H1, Nat.cast_ne_zero, Int.natAbs_ne_zero] at hx
    simp only [norm_eq_max_natAbs, H1, Nat.cast_natAbs, Int.cast_abs, div_pow, sq_abs, ne_eq,
      OfNat.ofNat_ne_zero, not_false_eq_true, pow_eq_zero_iff, Int.cast_eq_zero, this, div_self,
      le_refl]

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]

Goal state after:
L : PeriodPair
z x : ℂ
hx : ∀ (l : ↥L.lattice), ‖z - x‖ < ‖↑l - x‖
⊢ HasSum (fun i ↦ (L.weierstrassPExceptSeries (L.ω₁ / 2) x).coeff i * (z - x) ^ i) (℘[L - L.ω₁ / 2] z)
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: L : PeriodPair
x : ℂ
r : NNReal
hr0 : 0 < r
hr : Metric.closedBall x ↑r ⊆ (↑L.lattice)ᶜ
⊢ HasFPowerSeriesOnBall ℘[L] (L.weierstrassPSeries x) x ↑r

Tactic:
simp_rw [← L.weierstrassPExceptSeries_of_notMem _ L.ω₁_div_two_notMem_lattice,
    ← L.weierstrassPExcept_of_notMem _ L.ω₁_div_two_notMem_lattice]

Goal state after:
L : PeriodPair
x : ℂ
r : NNReal
hr0 : 0 < r
hr : Metric.closedBall x ↑r ⊆ (↑L.lattice)ᶜ
⊢ HasFPowerSeriesOnBall ℘[L - L.ω₁ / 2] (L.weierstrassPExceptSeries (L.ω₁ / 2) x) x ↑r
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable

Goal state before:
pp: z : ℂ
b : ℤ
⊢ Tendsto (fun d ↦ 1 / (↑b * z + ↑d)) atTop (𝓝 0)

Tactic:
apply IsBigO.trans_tendsto ?_ tendsto_inv_atTop_nhds_zero_nat (F'' := ℝ)

Goal state after:
z : ℂ
b : ℤ
⊢ (fun d ↦ 1 / (↑b * z + ↑d)) =O[atTop] fun n ↦ (↑n)⁻¹
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema

Goal state before:
pp: case refine_2
n : ℕ
hn : n ≠ 0
⊢ ↑n = (T ℝ ↑n).degree

pp: case refine_2
n : ℕ
hn : n ≠ 0
⊢ Set.InjOn (fun k ↦ cos ((2 * ↑k + 1) * π / (2 * ↑n))) ↑(Finset.range n)

Tactic:
degree_T,

Goal state after:
case refine_2
n : ℕ
hn : n ≠ 0
⊢ ↑n = ↑(↑n).natAbs

case refine_2
n : ℕ
hn : n ≠ 0
⊢ Set.InjOn (fun k ↦ cos ((2 * ↑k + 1) * π / (2 * ↑n))) ↑(Finset.range n)
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable

Goal state before:
pp: a b : ℤ
⊢ (fun m ↦ ‖![m 0 + a, m 1 + b]‖⁻¹) =Θ[cofinite] fun m ↦ ‖m‖⁻¹

Tactic:
have (x : Fin 2 → ℤ) : ![x 0 + a, x 1 + b] = x + ![a, b] := List.ofFn_inj.mp rfl
  simpa only [isTheta_inv, isTheta_norm_left, this] using! (IsTheta.add_isLittleO
  (by rw [← isTheta_norm_left]) (isLittleO_const_left_of_properSpace_of_discreteTopology ![a, b]))

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

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

Tactic:
simp [hi₃]

Goal state after:
Module: Mathlib.Tactic.NormNum.Prime

Goal state before:
pp: n k : ℕ
h1 : MinFacHelper n k
h2 : 0 = n % k
⊢ IsNat n.minFac k

Tactic:
eq_comm,

Goal state after:
n k : ℕ
h1 : MinFacHelper n k
h2 : n % k = 0
⊢ IsNat n.minFac k