mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Order

Goal state before:
pp: A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
p : ℝ≥0
hp : p ∈ Icc 0 1
hIcc : Icc 0 1 = Ioo 0 1 ∪ {0} ∪ {1}
⊢ ConcaveOn ℝ (Ici 0) fun a ↦ a ^ p

Tactic:
hIcc

Goal state after:
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
p : ℝ≥0
hp : p ∈ Ioo 0 1 ∪ {0} ∪ {1}
hIcc : Icc 0 1 = Ioo 0 1 ∪ {0} ∪ {1}
⊢ ConcaveOn ℝ (Ici 0) fun a ↦ a ^ p
Module: Mathlib.Analysis.SpecialFunctions.Log.RpowTendsto

Goal state before:
pp: p x : ℝ
p_pos : 0 < p
x_pos : 0 < x
hx : ‖p * log x‖ ≤ 1
pinv_nonneg : 0 ≤ p⁻¹
⊢ p⁻¹ * ‖rexp (p * log x) - 1 - p * log x‖ ≤ p⁻¹ * ‖p * log x‖ ^ 2

Tactic:
by
          gcongr
          refine Real.norm_exp_sub_one_sub_id_le ?_
          simp only [hx]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog.Order

Goal state before:
pp: A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
⊢ Tendsto (fun p a ↦ if a ∈ {b | IsStrictlyPositive b} then cfc (fun x ↦ p⁻¹ * (x ^ p - 1)) a else 0) (𝓝[>] 0)
    (𝓝 fun a ↦ if a ∈ {b | IsStrictlyPositive b} then log a else 0)

Tactic:
rw [tendsto_pi_nhds]

Goal state after:
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
⊢ ∀ (x : A),
    Tendsto (fun i ↦ if x ∈ {b | IsStrictlyPositive b} then cfc (fun x ↦ i⁻¹ * (x ^ i - 1)) x else 0) (𝓝[>] 0)
      (𝓝 (if x ∈ {b | IsStrictlyPositive b} then log x else 0))
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
u : ℝ → E := fun x ↦ x⁻¹ • f x
key : (fun x ↦ x⁻¹ • f (c * x)) = fun x ↦ c • u (c * x)
⊢ c • ∫ (x : ℝ) in ε..r, u (c * x) = ∫ (x : ℝ) in c * ε..c * r, x⁻¹ • f x

Tactic:
smul_integral_comp_mul_left

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
key : (fun x ↦ x⁻¹ • f (c * x)) = fun x ↦ c • u (c * x)
⊢ ∫ (x : ℝ) in c * ε..c * r, u x = ∫ (x : ℝ) in c * ε..c * r, x⁻¹ • f x
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Deligne

Goal state before:
pp: case refine_1
s : ℂ
⊢ DifferentiableAt ℂ (fun s ↦ ↑π ^ (-s / 2)) s

Tactic:
refine ((differentiableAt_id.neg.div_const (2 : ℂ)).const_cpow ?_)
    exact Or.inl (ofReal_ne_zero.mpr pi_ne_zero)

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

Goal state before:
pp: case e_a
p t x : ℝ
hp : p ∈ Ioo 0 1
ht : 0 < t
hx : 0 ≤ x
⊢ t ^ (p - 1) / t = t ^ (p - 2)

Tactic:
← Real.rpow_sub_one (by positivity)

Goal state after:
case e_a
p t x : ℝ
hp : p ∈ Ioo 0 1
ht : 0 < t
hx : 0 ≤ x
⊢ t ^ (p - 1 - 1) = t ^ (p - 2)
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation

Goal state before:
pp: p x : ℝ
hp : p ∈ Ioo 0 1
hx : 0 ≤ x
⊢ ∀ᵐ (a : ℝ) ∂volume.restrict (Ioo 0 1), ‖p.rpowIntegrand₀₁ a x‖ ≤ a ^ (p - 1)

Tactic:
refine ae_restrict_of_forall_mem measurableSet_Ioo fun t ht => ?_
      rw [Real.norm_of_nonneg (rpowIntegrand₀₁_nonneg hp.1 (le_of_lt ht.1) hx)]
      exact rpowIntegrand₀₁_le_rpow_sub_one hp (le_of_lt ht.1) hx

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

Goal state before:
pp: n✝ : ℕ
f : ℝ → ℝ := log ∘ Gamma
hc : ConvexOn ℝ (Ioi 0) f
h_rec : ∀ (x : ℝ), 0 < x → f (x + 1) = f x + log x
hder : ∀ {x : ℝ}, 0 < x → DifferentiableAt ℝ f x
hder_rec : ∀ (x : ℝ), 0 < x → deriv f (x + 1) = deriv f x + 1 / x
n : ℕ
⊢ deriv f (↑n + 1) = deriv f 1 + ↑(harmonic n)

Tactic:
induction n with

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
inst✝ : CompleteSpace A
p : ℝ≥0
hp : p ∈ Ioo 0 1
μ : Measure ℝ
hμ :
  ∀ x ∈ Ici 0,
    IntegrableOn (fun t ↦ (↑p).rpowIntegrand₀₁ t x) (Ioi 0) μ ∧ x ^ ↑p = ∫ (t : ℝ) in Ioi 0, (↑p).rpowIntegrand₀₁ t x ∂μ
a : A
ha : 0 ≤ a
a✝ : Nontrivial A
p_pos : 0 < ↑p
f : ℝ → ℝ → ℝ := fun t ↦ (↑p).rpowIntegrand₀₁ t
maxr : ℝ := sSup (quasispectrum ℝ a)
maxr_nonneg : 0 ≤ maxr
bound : ℝ → ℝ := fun t ↦ ‖f t maxr‖
hf : ContinuousOn (Function.uncurry f) (Ioi 0 ×ˢ quasispectrum ℝ a)
hbound : ∀ᵐ (t : ℝ) ∂μ.restrict (Ioi 0), ∀ z ∈ quasispectrum ℝ a, ‖f t z‖ ≤ bound t
hbound_finite_integral : HasFiniteIntegral bound (μ.restrict (Ioi 0))
hmapzero : ∀ᵐ (x : ℝ) ∂μ.restrict (Ioi 0), (↑p).rpowIntegrand₀₁ x 0 = 0
⊢ a ^ p = cfcₙ (fun r ↦ ∫ (t : ℝ) in Ioi 0, (↑p).rpowIntegrand₀₁ t r ∂μ) a

Tactic:
rw [nnrpow_eq_cfcₙ_real _ _]
      exact cfcₙ_congr fun r _ ↦ (hμ r (by grind)).2

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

Goal state before:
pp: f : ℂ → ℂ
g : ℝ → ℝ
g' s : ℝ
hf : DifferentiableAt ℂ f ↑s
hg : HasDerivAt g g' s
hfg : ∀ (s : ℝ), f ↑s = ↑(g s)
⊢ HasDerivAt f ↑g' ↑s

Tactic:
refine HasDerivAt.congr_deriv hf.hasDerivAt ?_

Goal state after:
f : ℂ → ℂ
g : ℝ → ℝ
g' s : ℝ
hf : DifferentiableAt ℂ f ↑s
hg : HasDerivAt g g' s
hfg : ∀ (s : ℝ), f ↑s = ↑(g s)
⊢ deriv f ↑s = ↑g'
Module: Mathlib.Analysis.SpecialFunctions.Log.Base

Goal state before:
pp: a b : ℝ
h₁ : a ≠ 0
h₂ : b ≠ 0
c : ℝ
⊢ logb (a * b) c = ((logb a c)⁻¹ + (logb b c)⁻¹)⁻¹

Tactic:
by rw [← inv_logb_mul_base h₁ h₂ c, inv_inv]

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

Goal state before:
pp: b x y : ℝ
hb : 1 < b
hx : 0 < x
hxy : x < y
⊢ logb b x < logb b y

Tactic:
rw [logb, logb, div_lt_div_iff_of_pos_right (log_pos hb)]
  exact log_lt_log hx hxy

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

Goal state before:
pp: b x : ℝ
hb : 1 < b
hx : 0 < x
⊢ 0 < logb b x ↔ 1 < x

Tactic:
by
  rw [← @logb_one b]
  rw [logb_lt_logb_iff hb zero_lt_one hx]

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

Goal state before:
pp: ⊢ StrictAntiOn (fun x ↦ x * log x) (Icc 0 (rexp (-1)))

Tactic:
by
  refine strictAntiOn_of_deriv_neg (convex_Icc ..) continuous_mul_log.continuousOn fun x hx ↦ ?_
  have hgt : x < rexp (-1) := by simp_all [interior_Icc, mem_Ioo]
  have hpos : 0 < x := by simp_all [interior_Icc, mem_Ioo]
  grind [deriv_mul_log, Real.log_lt_iff_lt_exp hpos |>.mpr hgt]

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

Goal state before:
pp: b x : ℝ
b_pos : 0 < b
b_lt_one : b < 1
hx : 0 < x
hx' : x < 1
⊢ 0 < logb b x

Tactic:
rw [logb_pos_iff_of_base_lt_one b_pos b_lt_one hx]
  exact hx'

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

Goal state before:
pp: case inl
b : ℕ
hr : 0 ≤ 0
⊢ ⌊0⌋ = Int.log b 0

Tactic:
Int.log_zero_right,

Goal state after:
case inl
b : ℕ
hr : 0 ≤ 0
⊢ ⌊0⌋ = 0
Module: Mathlib.MeasureTheory.Measure.RegularityCompacts

Goal state before:
pp: case mp
α : Type u_1
inst✝² : MeasurableSpace α
μ : Measure α
inst✝¹ : TopologicalSpace α
inst✝ : R1Space α
h : μ.InnerRegularWRT (IsCompact ∘ closure) IsClosed
⊢ μ.InnerRegularWRT IsCompact IsClosed

Tactic:
A

Goal state after:
case mp
α : Type u_1
inst✝² : MeasurableSpace α
μ : Measure α
inst✝¹ : TopologicalSpace α
inst✝ : R1Space α
h : μ.InnerRegularWRT (IsCompact ∘ closure) IsClosed
A : Set α
⊢ IsClosed A → ∀ r < μ A, ∃ K ⊆ A, IsCompact K ∧ r < μ K
Module: Mathlib.Analysis.SpecialFunctions.Log.Base

Goal state before:
pp: case inl
⊢ (fun x ↦ log (0 * x)) =O[atTop] log

Tactic:
simpa using isLittleO_const_log_atTop.isBigO

Goal state after:
Module: Mathlib.MeasureTheory.Measure.RegularityCompacts

Goal state before:
pp: case mpr
α : Type u_1
inst✝² : MeasurableSpace α
μ : Measure α
inst✝¹ : TopologicalSpace α
inst✝ : R1Space α
h : μ.InnerRegularWRT IsCompact IsClosed
⊢ μ.InnerRegularWRT (IsCompact ∘ closure) IsClosed

Tactic:
A

Goal state after:
case mpr
α : Type u_1
inst✝² : MeasurableSpace α
μ : Measure α
inst✝¹ : TopologicalSpace α
inst✝ : R1Space α
h : μ.InnerRegularWRT IsCompact IsClosed
A : Set α
⊢ IsClosed A → ∀ r < μ A, ∃ K ⊆ A, (IsCompact ∘ closure) K ∧ r < μ K
Module: Mathlib.MeasureTheory.Measure.RegularityCompacts

Goal state before:
pp: case mp
α : Type u_1
inst✝² : MeasurableSpace α
μ : Measure α
inst✝¹ : TopologicalSpace α
inst✝ : R1Space α
h : μ.InnerRegularWRT (fun s ↦ IsCompact s ∧ IsClosed s) IsClosed
⊢ μ.InnerRegularWRT (IsCompact ∘ closure) IsClosed

Tactic:
A

Goal state after:
case mp
α : Type u_1
inst✝² : MeasurableSpace α
μ : Measure α
inst✝¹ : TopologicalSpace α
inst✝ : R1Space α
h : μ.InnerRegularWRT (fun s ↦ IsCompact s ∧ IsClosed s) IsClosed
A : Set α
⊢ IsClosed A → ∀ r < μ A, ∃ K ⊆ A, (IsCompact ∘ closure) K ∧ r < μ K
Module: Mathlib.MeasureTheory.Measure.RegularityCompacts

Goal state before:
pp: case mpr
α : Type u_1
inst✝² : MeasurableSpace α
μ : Measure α
inst✝¹ : TopologicalSpace α
inst✝ : R1Space α
h : μ.InnerRegularWRT (IsCompact ∘ closure) IsClosed
⊢ μ.InnerRegularWRT (fun s ↦ IsCompact s ∧ IsClosed s) IsClosed

Tactic:
A

Goal state after:
case mpr
α : Type u_1
inst✝² : MeasurableSpace α
μ : Measure α
inst✝¹ : TopologicalSpace α
inst✝ : R1Space α
h : μ.InnerRegularWRT (IsCompact ∘ closure) IsClosed
A : Set α
⊢ IsClosed A → ∀ r < μ A, ∃ K ⊆ A, (fun s ↦ IsCompact s ∧ IsClosed s) K ∧ r < μ K
Module: Mathlib.Analysis.SpecialFunctions.Log.Base

Goal state before:
pp: P : ℝ → Prop
x₀ r : ℝ
hr : 1 < r
hx₀ : 0 < x₀
base : ∀ x ∈ Ico x₀ (r * x₀), P x
step : ∀ n ≥ 1, (∀ z ∈ Ico x₀ (r ^ n * x₀), P z) → ∀ z ∈ Ico (r ^ n * x₀) (r ^ (n + 1) * x₀), P z
n : ℕ
⊢ ∀ x ∈ Ico x₀ (r ^ (n + 1) * x₀), P x

Tactic:
induction n with

Goal state after:
Module: Mathlib.MeasureTheory.Measure.RegularityCompacts

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
p q : Set α → Prop
hpq : ∀ (A B : Set α), p A → q B → p (A ∩ B)
hμ : ∀ (ε : ℝ≥0∞), 0 < ε → ∃ K, p K ∧ μ Kᶜ < ε
A : Set α
hA : q A
r : ℝ≥0∞
hr : r < μ A
⊢ ∃ K, p K ∧ K ⊆ A ∧ μ (A \ K) < μ A - r

Tactic:
by
    obtain ⟨K', hpK', hK'_lt⟩ := hμ (μ A - r) (tsub_pos_of_lt hr)
    refine ⟨K' ∩ A, hpq K' A hpK' hA, inter_subset_right, ?_⟩
    · refine (measure_mono fun x ↦ ?_).trans_lt hK'_lt
      simp only [sdiff_inter_self_eq_sdiff, mem_sdiff, mem_compl_iff, and_imp, imp_self,
        imp_true_iff]

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

Goal state before:
pp: n : ℕ
⊢ MonotoneOn (deriv fun x ↦ Polynomial.eval x (descPochhammer ℝ n)) (Set.Ioi (↑n - 1))

Tactic:
induction n with

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

Goal state before:
pp: E : Type u_1
inst✝³ : TopologicalSpace E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
P : Measure E
inst✝ : IsFiniteMeasure P
ε : ℝ
K : Set E
hK : IsCompact K
hKmeas : MeasurableSet K
f g : C(E, ℝ)
δ : ℝ
hε : 0 < ε
hfg : ∀ x ∈ K, |g x - f x| < δ
⊢ |∫ (x : E) in K, ε.mulExpNegMulSq (g x) ∂P - ∫ (x : E) in K, ε.mulExpNegMulSq (f x) ∂P| ≤ δ * (P K).toReal

Tactic:
← (integral_sub (integrable_mulExpNegMulSq_comp_restrict_of_isCompact hK hKmeas g)
      (integrable_mulExpNegMulSq_comp_restrict_of_isCompact hK hKmeas f)),

Goal state after:
E : Type u_1
inst✝³ : TopologicalSpace E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
P : Measure E
inst✝ : IsFiniteMeasure P
ε : ℝ
K : Set E
hK : IsCompact K
hKmeas : MeasurableSet K
f g : C(E, ℝ)
δ : ℝ
hε : 0 < ε
hfg : ∀ x ∈ K, |g x - f x| < δ
⊢ |∫ (a : E) in K, ε.mulExpNegMulSq (g a) - ε.mulExpNegMulSq (f a) ∂P| ≤ δ * (P K).toReal
Module: Mathlib.Analysis.SpecialFunctions.Pow.NthRootLemmas

Goal state before:
pp: n : ℕ
hn : n ≠ 0
a : ℕ
⊢ n.nthRoot (a ^ n) = a

Tactic:
by
  refine eq_of_forall_le_iff fun b ↦ ?_
  rw [le_nthRoot_iff hn]
  exact (Nat.pow_left_strictMono hn).le_iff_le

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

Goal state before:
pp: case refine_3
a b : Multiset ℂ
n : ℕ
hb : ∀ k ∈ b, k ≠ -↑n
j : ℂ
hj : j ∈ b
⊢ Gamma (j + ↑(n + 1)) = Gamma (j + ↑n) * (j + ↑n)

Tactic:
simp only [Nat.cast_add, Nat.cast_one, ← add_assoc]

Goal state after:
case refine_3
a b : Multiset ℂ
n : ℕ
hb : ∀ k ∈ b, k ≠ -↑n
j : ℂ
hj : j ∈ b
⊢ Gamma (j + ↑n + 1) = Gamma (j + ↑n) * (j + ↑n)
Module: Mathlib.Analysis.SpecialFunctions.RegularizedHypergeometric

Goal state before:
pp: ⊢ regularizedHGFunSeries 0 0 = NormedSpace.expSeries ℂ ℂ

Tactic:
ext n

Goal state after:
n : ℕ
⊢ ((regularizedHGFunSeries 0 0 n) fun x ↦ 1) = (NormedSpace.expSeries ℂ ℂ n) fun x ↦ 1
Module: Mathlib.Analysis.SpecialFunctions.RegularizedHypergeometric

Goal state before:
pp: case e_p
a b c z : ℂ
hc : ∀ (k : ℕ), c ≠ -↑k
⊢ (Gamma c)⁻¹ • ordinaryHypergeometricSeries ℂ a b c = a.regularizedGaussHGFunSeries b c

Tactic:
ext n

Goal state after:
case e_p
a b c z : ℂ
hc : ∀ (k : ℕ), c ≠ -↑k
n : ℕ
⊢ ((((Gamma c)⁻¹ • ordinaryHypergeometricSeries ℂ a b c) n) fun x ↦ 1) = (a.regularizedGaussHGFunSeries b c n) fun x ↦ 1
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
r : ℝ
⊢ Integrable (fun x ↦ (Iio r).indicator f ‖x‖) μ ↔
    IntegrableOn ((Ioo 0 r).indicator fun y ↦ y ^ (dim E - 1) • f y) (Ioi 0) volume

Tactic:
integrable_fun_norm_addHaar μ (f := indicator (Iio r) f),

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
r : ℝ
⊢ IntegrableOn (fun y ↦ y ^ (dim E - 1) • (Iio r).indicator f y) (Ioi 0) volume ↔
    IntegrableOn ((Ioo 0 r).indicator fun y ↦ y ^ (dim E - 1) • f y) (Ioi 0) volume
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
r : ℝ
⊢ EqOn (fun y ↦ y ^ (dim E - 1) • (Iio r).indicator f y) ((Ioo 0 r).indicator fun y ↦ y ^ (dim E - 1) • f y) (Ioi 0)

Tactic:
intro x (hx : 0 < x)

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
r x : ℝ
hx : 0 < x
⊢ (fun y ↦ y ^ (dim E - 1) • (Iio r).indicator f y) x = (Ioo 0 r).indicator (fun y ↦ y ^ (dim E - 1) • f y) x
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
x : ℂ
hx : x ∈ (↑L.lattice \ {l₀ - ↑l})ᶜ
⊢ deriv ℘[L - l₀] (x + ↑l) = deriv ℘[L - l₀ - ↑l] x

Tactic:
rw [L.eqOn_deriv_weierstrassPExcept_derivWeierstrassPExcept,
      L.eqOn_deriv_weierstrassPExcept_derivWeierstrassPExcept, L.derivWeierstrassPExcept_add_coe]

Goal state after:
case a
L : PeriodPair
l₀ : ℂ
hl₀ : l₀ ∈ L.lattice
l : ↥L.lattice
hl : ↑l / 2 ∉ L.lattice
x : ℂ
hx : x ∈ (↑L.lattice \ {l₀ - ↑l})ᶜ
⊢ x ∈ (↑L.lattice \ {l₀ - ↑l})ᶜ

case a
L : PeriodPair
l₀ : ℂ
hl₀ : l₀ ∈ L.lattice
l : ↥L.lattice
hl : ↑l / 2 ∉ L.lattice
x : ℂ
hx : x ∈ (↑L.lattice \ {l₀ - ↑l})ᶜ
⊢ x + ↑l ∈ (↑L.lattice \ {l₀})ᶜ
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 := UniformSpace.Completion.toComplₗᵢ
this : ‖(⇑g ∘ f) b - (⇑g ∘ f) a‖ₑ = ‖f b - f a‖ₑ
x : ℝ
hx : x ∈ Ioo a b
⊢ ‖deriv (⇑g ∘ f) x‖ₑ ≤ ‖deriv f x‖ₑ

Tactic:
rw [fderiv_comp_deriv]

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 := UniformSpace.Completion.toComplₗᵢ
this : ‖(⇑g ∘ f) b - (⇑g ∘ f) a‖ₑ = ‖f b - f a‖ₑ
x : ℝ
hx : x ∈ Ioo a b
⊢ ‖(fderiv ℝ (⇑g) (f x)) (deriv f x)‖ₑ ≤ ‖deriv f x‖ₑ

case hl
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 := UniformSpace.Completion.toComplₗᵢ
this : ‖(⇑g ∘ f) b - (⇑g ∘ f) a‖ₑ = ‖f b - f a‖ₑ
x : ℝ
hx : x ∈ Ioo a b
⊢ DifferentiableAt ℝ (⇑g) (f x)

case hf
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 := UniformSpace.Completion.toComplₗᵢ
this : ‖(⇑g ∘ f) b - (⇑g ∘ f) a‖ₑ = ‖f b - f a‖ₑ
x : ℝ
hx : x ∈ Ioo a b
⊢ DifferentiableAt ℝ f x
Module: Mathlib.Analysis.SpecialFunctions.Stirling

Goal state before:
pp: ⊢ ∃ a, 0 < a ∧ ∀ (n : ℕ), a ≤ stirlingSeq (n + 1)

Tactic:
let c := 1 - 12⁻¹ - log 2 / 2

Goal state after:
c : ℝ := 1 - 12⁻¹ - log 2 / 2
⊢ ∃ a, 0 < a ∧ ∀ (n : ℕ), a ≤ stirlingSeq (n + 1)
Module: Mathlib.Analysis.SpecialFunctions.Stirling

Goal state before:
pp: this : √π ≠ 0
⊢ ((fun n ↦ ↑n !) / fun n ↦ √(2 * ↑n * π) * (↑n / rexp 1) ^ n) = stirlingSeq / fun x ↦ √π

Tactic:
ext n

Goal state after:
this : √π ≠ 0
n : ℕ
⊢ ((fun n ↦ ↑n !) / fun n ↦ √(2 * ↑n * π) * (↑n / rexp 1) ^ n) n = (stirlingSeq / fun x ↦ √π) n
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Orthogonality

Goal state before:
pp: f : ℝ → ℝ
⊢ ∫ (x : ℝ) in 1..-1, f x * -√(1 - x ^ 2)⁻¹ = ∫ (θ : ℝ) in arccos 1..arccos (-1), f (cos θ)

Tactic:
by
    rw [← integral_comp_mul_deriv_of_deriv_nonpos (f' := fun x => -(1 / √(1 - x ^ 2)))]
    · simp_rw [Function.comp_apply]
      exact integral_congr <| fun x hx => by simp [cos_arccos (x := x) (by aesop) (by aesop)]
    · fun_prop
    · exact fun x hx ↦ (hasDerivAt_arccos (by aesop) (by aesop))
    · simp

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

Goal state before:
pp: case e'_10
L : PeriodPair
l₀ x : ℂ
r : NNReal
hr0 : 0 < r
hr : Metric.closedBall x ↑r ⊆ (↑L.lattice \ {l₀})ᶜ
this : HasFPowerSeriesOnBall (fderiv ℂ ℘[L - l₀]) (L.weierstrassPExceptSeries l₀ x).derivSeries x ↑r
⊢ L.derivWeierstrassPExceptSeries l₀ x =
    ((ContinuousLinearMap.apply ℂ ℂ) 1).compFormalMultilinearSeries (L.weierstrassPExceptSeries l₀ x).derivSeries

Tactic:
ext n

Goal state after:
case e'_10
L : PeriodPair
l₀ x : ℂ
r : NNReal
hr0 : 0 < r
hr : Metric.closedBall x ↑r ⊆ (↑L.lattice \ {l₀})ᶜ
this : HasFPowerSeriesOnBall (fderiv ℂ ℘[L - l₀]) (L.weierstrassPExceptSeries l₀ x).derivSeries x ↑r
n : ℕ
⊢ ((L.derivWeierstrassPExceptSeries l₀ x n) fun x ↦ 1) =
    (((ContinuousLinearMap.apply ℂ ℂ) 1).compFormalMultilinearSeries (L.weierstrassPExceptSeries l₀ x).derivSeries n)
      fun x ↦ 1
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'' := ℝ)
  have := (isBigO_sup.mp (Int.cofinite_eq ▸ linear_inv_isBigO_right b z)).2
  simpa [← Nat.map_cast_int_atTop, isBigO_map]

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

Goal state before:
pp: case refine_1
n k : ℕ
hn : n ≠ 0
hk₀ : 0 < k
hk₁ : k < n
hk₂ : Even k
zero_lt : 0 < ↑k * π / ↑n
lt_pi : ↑k * π / ↑n < π
⊢ ∀ y ∈ Set.Ioo (-1) 1, (fun x ↦ eval x (T ℝ ↑n)) y ≤ (fun x ↦ eval x (T ℝ ↑n)) (cos (↑k * π / ↑n))

pp: case refine_2
n k : ℕ
hn : n ≠ 0
hk₀ : 0 < k
hk₁ : k < n
hk₂ : Even k
zero_lt : 0 < ↑k * π / ↑n
lt_pi : ↑k * π / ↑n < π
⊢ -1 < cos (↑k * π / ↑n)

pp: case refine_3
n k : ℕ
hn : n ≠ 0
hk₀ : 0 < k
hk₁ : k < n
hk₂ : Even k
zero_lt : 0 < ↑k * π / ↑n
lt_pi : ↑k * π / ↑n < π
⊢ cos (↑k * π / ↑n) < 1

Tactic:
· intro x hx
    dsimp
    rw [(eval_T_real_eq_one_iff hn _).mpr ⟨k, le_of_lt hk₁, hk₂, rfl⟩]
    exact (abs_le.mp (abs_eval_T_real_le_one n (by grind))).2

Goal state after:
case refine_2
n k : ℕ
hn : n ≠ 0
hk₀ : 0 < k
hk₁ : k < n
hk₂ : Even k
zero_lt : 0 < ↑k * π / ↑n
lt_pi : ↑k * π / ↑n < π
⊢ -1 < cos (↑k * π / ↑n)

case refine_3
n k : ℕ
hn : n ≠ 0
hk₀ : 0 < k
hk₁ : k < n
hk₂ : Even k
zero_lt : 0 < ↑k * π / ↑n
lt_pi : ↑k * π / ↑n < π
⊢ cos (↑k * π / ↑n) < 1
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: case pos
L : PeriodPair
x : ℂ
hx : x ∈ L.lattice
⊢ AnalyticAt ℂ L.relation x

pp: case neg
L : PeriodPair
x : ℂ
hx : x ∉ L.lattice
⊢ AnalyticAt ℂ L.relation x

Tactic:
· lift x to L.lattice using hx
    have := L.analyticAt_relation_zero
    rw [← sub_self x.1] at this
    convert! this.comp (f := (· - x.1)) (by fun_prop)
    ext a
    simp

Goal state after:
case neg
L : PeriodPair
x : ℂ
hx : x ∉ L.lattice
⊢ AnalyticAt ℂ L.relation x
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: case neg
L : PeriodPair
x : ℂ
hx : x ∉ L.lattice
⊢ AnalyticAt ℂ L.relation x

Tactic:
have : AnalyticAt ℂ (fun z ↦ ℘'[L] z ^ 2 - 4 * ℘[L] z ^ 3 + L.g₂ * ℘[L] z + L.g₃) x := by
      have := L.analyticOnNhd_derivWeierstrassP _ hx
      have := L.analyticOnNhd_weierstrassP _ hx
      fun_prop

Goal state after:
case neg
L : PeriodPair
x : ℂ
hx : x ∉ L.lattice
this : AnalyticAt ℂ (fun z ↦ ℘'[L] z ^ 2 - 4 * ℘[L] z ^ 3 + L.g₂ * ℘[L] z + L.g₃) x
⊢ AnalyticAt ℂ L.relation x
Module: Mathlib.Analysis.SpecificLimits.ArithmeticGeometric

Goal state before:
pp: R : Type u_1
a b u₀ : R
inst✝ : CommSemiring R
n : ℕ
⊢ arithGeom a b u₀ n = a ^ n * u₀ + b * ∑ k ∈ Finset.range n, a ^ k

Tactic:
induction n with

Goal state after:
Module: Mathlib.Analysis.SpecificLimits.ArithmeticGeometric

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

Tactic:
induction n with

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

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

Tactic:
rw [Nat.Coprime.gcd_mul_left_cancel n (by simp),
      Nat.mul_div_assoc _ (Nat.gcd_dvd_left ..)]

Goal state after:
Module: Mathlib.Analysis.SpecificLimits.ArithmeticGeometric

Goal state before:
pp: R : Type u_1
a b u₀ : R
inst✝² : Field R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
ha_pos : 0 < a
ha_ne : a ≠ 1
h0 : b / (1 - a) < u₀
n : ℕ
⊢ b / (1 - a) < arithGeom a b u₀ n

Tactic:
induction n with

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))
⊢ |eval x ((⇑derivative)^[k] (T ℝ ↑n))| ≤ eval 1 ((⇑derivative)^[k] (T ℝ ↑n))

Tactic:
← hf x,

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))
⊢ |∑ p ∈ f.support, f p • eval x p| ≤ eval 1 ((⇑derivative)^[k] (T ℝ ↑n))