mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Order.Filter.FilterProduct

Goal state before:
pp: case inl
α : Type u
β : Type v
φ : Ultrafilter α
inst✝ : LinearOrder β
x y : (↑φ).Germ β
a b : α → β
h : ↑a ≤ ↑b
⊢ max ↑a ↑b = map₂ max ↑a ↑b

Tactic:
rw [max_eq_right h, map₂_coe, coe_eq]

Goal state after:
case inl
α : Type u
β : Type v
φ : Ultrafilter α
inst✝ : LinearOrder β
x y : (↑φ).Germ β
a b : α → β
h : ↑a ≤ ↑b
⊢ b =ᶠ[↑φ] fun x ↦ max (a x) (b x)
Module: Mathlib.Analysis.Polynomial.MahlerMeasure

Goal state before:
pp: case a
p : ℂ[X]
⊢ ∑ i ∈ p.support, ‖p.coeff i‖ ^ 2 ≤ (↑p.natDegree + 1) * p.supNorm ^ 2

Tactic:
refine (p.support.sum_le_card_nsmul _ (p.supNorm ^ 2) fun i _ ↦ ?_).trans ?_

Goal state after:
case a.refine_1
p : ℂ[X]
i : ℕ
x✝ : i ∈ p.support
⊢ ‖p.coeff i‖ ^ 2 ≤ p.supNorm ^ 2

case a.refine_2
p : ℂ[X]
⊢ p.support.card • p.supNorm ^ 2 ≤ (↑p.natDegree + 1) * p.supNorm ^ 2
Module: Mathlib.Analysis.Real.OfDigits

Goal state before:
pp: b : ℕ
a : ℕ → Fin b
n : ℕ
⊢ ∑' (n : ℕ), ofDigitsTerm a n =
    ∑ n ∈ Finset.range n, ofDigitsTerm a n + (↑b ^ n)⁻¹ * ∑' (n_1 : ℕ), ofDigitsTerm (fun i ↦ a (i + n)) n_1

Tactic:
rw [← Summable.sum_add_tsum_nat_add n summable_ofDigitsTerm,
    ← Summable.tsum_mul_left _ summable_ofDigitsTerm]

Goal state after:
b : ℕ
a : ℕ → Fin b
n : ℕ
⊢ ∑ i ∈ Finset.range n, ofDigitsTerm a i + ∑' (i : ℕ), ofDigitsTerm a (i + n) =
    ∑ n ∈ Finset.range n, ofDigitsTerm a n + ∑' (i : ℕ), (↑b ^ n)⁻¹ * ofDigitsTerm (fun i ↦ a (i + n)) i
Module: Mathlib.Analysis.Real.Pi.Bounds

Goal state before:
pp: n : ℕ
a : ℝ
h : (↑0 / ↑1).sqrtTwoAddSeries n ≤ 2 - (a / 2 ^ (n + 1)) ^ 2
⊢ a < π

Tactic:
refine lt_of_le_of_lt ?_ (pi_gt_sqrtTwoAddSeries n); rw [mul_comm]
  refine (div_le_iff₀ (pow_pos (by simp) _)).mp (le_sqrt_of_sq_le ?_)
  rwa [le_sub_comm, show (0 : ℝ) = (0 : ℕ) / (1 : ℕ) by rw [Nat.cast_zero, zero_div]]

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

Goal state before:
pp: x : ℝ
b : ℕ
inst✝ : NeZero b
hb : 1 < b
hx : x ∈ Set.Ico 0 1
⊢ Summable fun i ↦ ‖ofDigitsTerm (x.digits b) i‖

Tactic:
by exact summable_ofDigitsTerm.abs

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

Goal state before:
pp: ⊢ stdPart ω = 0

Tactic:
rw [stdPart_eq_zero]

Goal state after:
⊢ ArchimedeanClass.mk ω ≠ 0
Module: Mathlib.NumberTheory.Real.Irrational

Goal state before:
pp: n : ℕ
⊢ Irrational √↑n ↔ ¬IsSquare n

Tactic:
rw [← Rat.isSquare_natCast_iff, ← irrational_sqrt_ratCast_iff_of_nonneg n.cast_nonneg,
    Rat.cast_natCast]

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

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

Tactic:
rw [eventually_iff_exists_mem]
      use Set.Ioo (-1) 1
      exact ⟨Ioo_mem_nhdsLT <| by simp,
        fun _ _ ↦ by rwa [Set.mem_Iio, sq_lt_one_iff_abs_lt_one, abs_lt, ← Set.mem_Ioo]⟩

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

Goal state before:
pp: x✝ y✝ x y : ℝ≥0
h : x ≤ y
⊢ ↑((x + y) / 2 - x) = dist x y / 2

Tactic:
← add_halves x

Goal state after:
x✝ y✝ x y : ℝ≥0
h : x ≤ y
⊢ ↑((x + y) / 2 - (x / 2 + x / 2)) = dist x y / 2
Module: Mathlib.Analysis.SpecialFunctions.Choose

Goal state before:
pp: case succ
k : ℕ
h : (fun n ↦ ↑(n.descFactorial k)) ~[atTop] fun n ↦ ↑n ^ k
hz : ∀ᶠ (x : ℕ) in atTop, ↑x ≠ 0
⊢ (fun n ↦ ↑(n - k)) ~[atTop] Nat.cast

Tactic:
isEquivalent_iff_tendsto_one hz,

Goal state after:
case succ
k : ℕ
h : (fun n ↦ ↑(n.descFactorial k)) ~[atTop] fun n ↦ ↑n ^ k
hz : ∀ᶠ (x : ℕ) in atTop, ↑x ≠ 0
⊢ Tendsto ((fun n ↦ ↑(n - k)) / Nat.cast) atTop (𝓝 1)
Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy

Goal state before:
pp: p : ℝ
⊢ binEntropy p = 0 ↔ p = 0 ∨ p = 1

Tactic:
refine ⟨fun h ↦ ?_, by rintro (rfl | rfl) <;> simp⟩
  contrapose! h
  obtain hp₀ | hp₀ := h.1.lt_or_gt
  · exact (binEntropy_neg_of_neg hp₀).ne
  obtain hp₁ | hp₁ := h.2.lt_or_gt.symm
  · exact (binEntropy_neg_of_one_lt hp₁).ne
  · exact (binEntropy_pos hp₀ hp₁).ne'

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

Goal state before:
pp: case neg
q : ℕ
p : ℝ
is_x_where_nondiff : ¬(p ≠ 0 ∧ p ≠ 1)
this : p = 0 ∨ p = 1
h : DifferentiableAt ℝ (deriv (qaryEntropy q)) p
⊢ False

Tactic:
have contAt := h.continuousAt

Goal state after:
case neg
q : ℕ
p : ℝ
is_x_where_nondiff : ¬(p ≠ 0 ∧ p ≠ 1)
this : p = 0 ∨ p = 1
h : DifferentiableAt ℝ (deriv (qaryEntropy q)) p
contAt : ContinuousAt (deriv (qaryEntropy q)) p
⊢ False
Module: Mathlib.Analysis.SpecialFunctions.Log.RpowTendsto

Goal state before:
pp: s : Set ℝ
hs : s ⊆ Ioi 0
hs' : IsCompact s
ε : ℝ
hε : 0 < ε
pbound : ℝ := ε / (sSup ((fun x ↦ ‖log x‖ ^ 2) '' s) + 1)
hxs : ∀ x ∈ s, x ≠ 0
sSup_nonneg : 0 ≤ sSup ((fun x ↦ ‖log x‖ ^ 2) '' s)
sSup_nonneg' : 0 ≤ sSup ((fun x ↦ ‖log x‖) '' s)
pbound_pos : 0 < pbound
h₁ : ∀ᶠ (p : ℝ) in 𝓝[>] 0, 0 < p ∧ p < pbound
⊢ ∀ᶠ (n : ℝ) in 𝓝[>] 0, ∀ x ∈ s, (log x, n⁻¹ * (x ^ n - 1)) ∈ {p | dist p.1 p.2 ≤ ε}

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

Goal state after:
s : Set ℝ
hs : s ⊆ Ioi 0
hs' : IsCompact s
ε : ℝ
hε : 0 < ε
pbound : ℝ := ε / (sSup ((fun x ↦ ‖log x‖ ^ 2) '' s) + 1)
hxs : ∀ x ∈ s, x ≠ 0
sSup_nonneg : 0 ≤ sSup ((fun x ↦ ‖log x‖ ^ 2) '' s)
sSup_nonneg' : 0 ≤ sSup ((fun x ↦ ‖log x‖) '' s)
pbound_pos : 0 < pbound
h₁ : ∀ᶠ (p : ℝ) in 𝓝[>] 0, 0 < p ∧ p < pbound
h₂ : ∀ᶠ (p : ℝ) in 𝓝[>] 0, p ≤ 1 / (sSup ((fun x ↦ ‖log x‖) '' s) + 1)
⊢ ∀ᶠ (n : ℝ) in 𝓝[>] 0, ∀ x ∈ s, (log x, n⁻¹ * (x ^ n - 1)) ∈ {p | dist p.1 p.2 ≤ ε}
Module: Mathlib.Analysis.SpecialFunctions.FrullaniIntegral

Goal state before:

Tactic:
‖(∫ x in a..b, x⁻¹ • f x) - log (b / a) • V‖
    _ = ‖∫ x in a..b, x⁻¹ • (f x - V)‖ := by
        congr 1
        have : log (b / a) • V = ∫ x in a..b, x⁻¹ • V := by
          rw [intervalIntegral.integral_smul_const (f := fun x ↦ (x⁻¹ : ℝ)) (c := V),
              integral_inv_of_pos ha hb]
        rw [this, ← integral_sub hint_f hint_V]
        congr 1
        funext x
        exact (smul_sub _ _ _).symm
    _ ≤ |∫ x in a..b, x⁻¹ * δ| := by
        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
    _ = δ * |log (b / a)| := by
        simp_rw [mul_comm, intervalIntegral.integral_const_mul, integral_inv_of_pos ha hb]
        exact (abs_mul δ (log (b / a))).trans (by rw [abs_of_nonneg hδ])

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

Goal state before:
pp: p t : ℝ
hp : p ≠ 1
ht : 0 < t
⊢ p.rpowIntegrand₀₁ t = fun x ↦ t ^ (p - 1) - t ^ p * (t + x)⁻¹

Tactic:
by
  unfold rpowIntegrand₀₁
  ext x
  rw [mul_sub, ← rpow_neg_one, ← rpow_add' (by grind) (by grind)]
  grind only

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

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

Tactic:
exact (Real.rpow_sub_one ht' p).symm

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

Goal state before:
pp: case inr
p x : ℝ
hp : p ∈ Ioo 0 1
hx✝ : 0 ≤ x
hx : 0 < x
heqOn : EqOn (fun t ↦ p.rpowIntegrand₀₁ (x * t) x * x) (fun t ↦ p.rpowIntegrand₀₁ t 1 * x ^ p) (Ioi 0)
⊢ (∫ (x : ℝ) in Ioi 0, p.rpowIntegrand₀₁ x 1 ∂volume) • x ^ p = x ^ p * ∫ (x : ℝ) in Ioi 0, p.rpowIntegrand₀₁ x 1

Tactic:
rw [smul_eq_mul, mul_comm]

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

Goal state before:
pp: p x : ℝ
hp : p ∈ Ioo 1 2
hx : 0 ≤ x
hmain : (fun x_1 ↦ p.rpowIntegrand₁₂ x_1 x) =ᵐ[volume.restrict (Ioi 0)] fun x_1 ↦ x * (p - 1).rpowIntegrand₀₁ x_1 x
⊢ x ^ p = x * x ^ (p - 1)

Tactic:
rw [mul_comm, ← rpow_add_one' hx (by grind)]

Goal state after:
p x : ℝ
hp : p ∈ Ioo 1 2
hx : 0 ≤ x
hmain : (fun x_1 ↦ p.rpowIntegrand₁₂ x_1 x) =ᵐ[volume.restrict (Ioi 0)] fun x_1 ↦ x * (p - 1).rpowIntegrand₀₁ x_1 x
⊢ x ^ p = x ^ (p - 1 + 1)
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Digamma

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

Tactic:
by
  rw [digamma_def, logDeriv_apply, hasDerivAt_Gamma_one_half.deriv, add_comm, Gamma_one_half_eq,
    neg_mul, ← mul_neg, neg_add', Real.sqrt_eq_rpow, ofReal_cpow Real.pi_nonneg]
  simp

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

Goal state before:
pp: f : ℂ → ℂ := fun s ↦ 2 * (2 * ↑π) ^ (-s)
⊢ HasDerivAt (fun s ↦ 2 * (2 * ↑π) ^ (-s)) (-log (2 * ↑π) / ↑π) 1

Tactic:
have := (hasDerivAt_neg' (1 : ℂ)).const_cpow (c := 2 * π)
      (Or.inl (by exact_mod_cast Real.two_pi_pos.ne'))

Goal state after:
f : ℂ → ℂ := fun s ↦ 2 * (2 * ↑π) ^ (-s)
this : HasDerivAt (fun x ↦ (2 * ↑π) ^ (-x)) ((2 * ↑π) ^ (-1) * log (2 * ↑π) * -1) 1
⊢ HasDerivAt (fun s ↦ 2 * (2 * ↑π) ^ (-s)) (-log (2 * ↑π) / ↑π) 1
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:
simp_rw [inv_logb]; exact logb_mul h₁ h₂

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

Goal state before:
pp: x : ℝ
hex : x ∈ Ici (rexp 1)
y : ℝ
hey : y ∈ Ici (rexp 1)
hxy : x ≤ y
x_pos : 0 < x
y_pos : 0 < y
hlogx : 1 ≤ log x
hyx : 0 ≤ y / x - 1
⊢ log y ≤ (fun x ↦ log x / x) x * y

Tactic:
← sub_le_sub_iff_right (log x)

Goal state after:
x : ℝ
hex : x ∈ Ici (rexp 1)
y : ℝ
hey : y ∈ Ici (rexp 1)
hxy : x ≤ y
x_pos : 0 < x
y_pos : 0 < y
hlogx : 1 ≤ log x
hyx : 0 ≤ y / x - 1
⊢ log y - log x ≤ (fun x ↦ log x / x) x * y - log x
Module: Mathlib.Analysis.SpecialFunctions.Log.Monotone

Goal state before:
pp: ⊢ AntitoneOn (fun x ↦ log x / x) (Ici (rexp 1))

Tactic:
intro x hex y hey hxy
  have x_pos : 0 < x := (exp_pos 1).trans_le hex
  have y_pos : 0 < y := (exp_pos 1).trans_le hey
  have hlogx : 1 ≤ log x := by rwa [le_log_iff_exp_le x_pos]
  have hyx : 0 ≤ y / x - 1 := by rwa [le_sub_iff_add_le, le_div_iff₀ x_pos, zero_add, one_mul]
  rw [div_le_iff₀ y_pos, ← sub_le_sub_iff_right (log x)]
  calc
    log y - log x = log (y / x) := by rw [log_div y_pos.ne' x_pos.ne']
    _ ≤ y / x - 1 := log_le_sub_one_of_pos (div_pos y_pos x_pos)
    _ ≤ log x * (y / x - 1) := le_mul_of_one_le_left hyx hlogx
    _ = log x / x * y - log x := by ring

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

Goal state before:
pp: b : ℝ
n : ℕ
⊢ logb b ↑n = n.factorization.sum fun p t ↦ ↑t * logb b ↑p

Tactic:
by
  simp only [logb, mul_div_assoc', log_nat_eq_sum_factorization n, Finsupp.sum, Finset.sum_div]

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

Goal state before:
pp: b a c : ℝ
n : ℕ
ha : a ≠ 0
h : log b ≠ 0
x : ℝ
⊢ log x ^ n / (a * log b ^ n * x + c * log b ^ n) = logb b x ^ n / (a * x + c)

Tactic:
by simp [field, div_pow, logb]

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
μ : Measure X
inst✝ : IsFiniteMeasure μ
f : X →ᵇ ℝ
c : ℝ
⊢ ∫ (x : X), (f + const X c) x ∂μ = ∫ (x : X), f x ∂μ + μ.real Set.univ • c

Tactic:
by
  simp [integral_add (f.integrable _) (integrable_const c)]

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

Goal state before:
pp: case refine_1
α : 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
n : ℕ
ε : ℝ≥0∞
hε : 0 < ε
m : ℕ
⊢ NullMeasurableSet (f n m)ᶜ P

Tactic:
exact (measurable_prodMk_left (hto n).measurableSet).compl.nullMeasurableSet

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
s : Set ↑(sphere 0 1)
hs : MeasurableSet s
⊢ μ.toSphere s = ↑(dim E) * μ (Ioo 0 1 • Subtype.val '' s)

Tactic:
rw [toSphere, smul_apply, fst_apply hs, restrict_apply (measurable_fst hs),
    ((MeasurableEmbedding.subtype_coe (measurableSet_singleton _).compl).comp
      (Homeomorph.measurableEmbedding _)).comap_apply,
    image_comp, Homeomorph.image_symm, univ_prod, ← Set.prod_eq, nsmul_eq_mul, toSphere_apply_aux]

Goal state after:
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)
⊢ ∫⁻ (ω : α), ENNReal.ofReal (f ω ^ p) ∂μ =
    ENNReal.ofReal p * ∫⁻ (t : ℝ) in Ioi 0, μ {a | t ≤ f a} * ENNReal.ofReal (t ^ (p - 1))

Tactic:
rw [← key, ← lintegral_const_mul'' (ENNReal.ofReal p)]

Goal state after:
α : 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)
⊢ ∫⁻ (ω : α), ENNReal.ofReal (f ω ^ p) ∂μ = ∫⁻ (a : α), ENNReal.ofReal p * ENNReal.ofReal (∫ (t : ℝ) in 0..f a, g t) ∂μ

α : 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 (∫ (t : ℝ) in 0..f ω, g t)) μ
Module: Mathlib.MeasureTheory.Constructions.HaarToSphere

Goal state before:
pp: n : ℕ
x : ↑(Ioi 0)
hr₀ : 0 ≤ ↑x
⊢ ∫⁻ (x : ℝ) in Ioc 0 ↑x, ENNReal.ofReal (x ^ n) ∂volume = ENNReal.ofReal (↑x ^ (n + 1) / (↑n + 1))

Tactic:
← ofReal_integral_eq_lintegral_ofReal (intervalIntegrable_pow _).1,

Goal state after:
n : ℕ
x : ↑(Ioi 0)
hr₀ : 0 ≤ ↑x
⊢ ENNReal.ofReal (∫ (x : ℝ) in Ioc 0 ↑x, x ^ n ∂volume) = ENNReal.ofReal (↑x ^ (n + 1) / (↑n + 1))

n : ℕ
x : ↑(Ioi 0)
hr₀ : 0 ≤ ↑x
⊢ 0 ≤ᵐ[volume.restrict (Ioc 0 ↑x)] fun x ↦ x ^ n
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
⊢ μ (↑r • Ioo 0 1 • Subtype.val '' s) =
    ↑(dim E) * μ (Ioo 0 1 • Subtype.val '' s) * ENNReal.ofReal (↑r ^ (dim E - 1 + 1) / (↑(dim E - 1) + 1))

Tactic:
μ.addHaar_smul_of_nonneg r.2.out.le,

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
⊢ ENNReal.ofReal (↑r ^ dim E) * μ (Ioo 0 1 • Subtype.val '' s) =
    ↑(dim E) * μ (Ioo 0 1 • Subtype.val '' s) * ENNReal.ofReal (↑r ^ (dim E - 1 + 1) / (↑(dim E - 1) + 1))
Module: Mathlib.MeasureTheory.Constructions.Polish.EmbeddingReal

Goal state before:
pp: α : Type u_1
inst✝² : MeasurableSpace α
inst✝¹ : StandardBorelSpace α
inst✝ : Finite α
n : ℕ
n_equiv : α ≃ Fin n
⊢ Fin n ≃ ↑(range fun x ↦ ↑↑x)

Tactic:
exact Equiv.ofInjective _ (Nat.cast_injective.comp Fin.val_injective)

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

Goal state before:
pp: case pos
L : PeriodPair
z : ℂ
l : ↥L.lattice
hl : ↑l / 2 ∉ L.lattice
hl0 : l ≠ 0
hz : z ∈ L.lattice
this : ℘[L - z + ↑l] (z + ↑l) = ℘[L - z + ↑l - ↑l] z + (1 / (z + ↑l) ^ 2 - 1 / (z + ↑l - ↑l) ^ 2)
⊢ ℘[L - z + ↑l - ↑l] z + (1 / (z + ↑l) ^ 2 - 1 / (z + ↑l - ↑l) ^ 2) +
      (1 / (z + ↑l - ↑⟨z + ↑l, ⋯⟩) ^ 2 - 1 / ↑⟨z + ↑l, ⋯⟩ ^ 2) =
    ℘[L] z

Tactic:
← L.weierstrassPExcept_add ⟨z, hz⟩

Goal state after:
case pos
L : PeriodPair
z : ℂ
l : ↥L.lattice
hl : ↑l / 2 ∉ L.lattice
hl0 : l ≠ 0
hz : z ∈ L.lattice
this : ℘[L - z + ↑l] (z + ↑l) = ℘[L - z + ↑l - ↑l] z + (1 / (z + ↑l) ^ 2 - 1 / (z + ↑l - ↑l) ^ 2)
⊢ ℘[L - z + ↑l - ↑l] z + (1 / (z + ↑l) ^ 2 - 1 / (z + ↑l - ↑l) ^ 2) +
      (1 / (z + ↑l - ↑⟨z + ↑l, ⋯⟩) ^ 2 - 1 / ↑⟨z + ↑l, ⋯⟩ ^ 2) =
    ℘[L - ↑⟨z, hz⟩] z + (1 / (z - ↑⟨z, hz⟩) ^ 2 - 1 / ↑⟨z, hz⟩ ^ 2)
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.ContDiff

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

Tactic:
rw [integral_of_le hab, integral_of_le hab]

Goal state after:
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
inst✝ : CompleteSpace E
h : ContDiffOn ℝ 1 f (Icc a b)
hab : a ≤ b
⊢ ∫ (x : ℝ) in Ioc a b, derivWithin f (Icc a b) x ∂volume = ∫ (x : ℝ) in Ioc a b, deriv f x ∂volume
Module: Mathlib.Analysis.SpecialFunctions.Stirling

Goal state before:
pp: case inr
n : ℕ
hn : n ≠ 0
this : √(2 * π * ↑n) * (↑n / rexp 1) ^ n = √π * (√(2 * ↑n) * (↑n / rexp 1) ^ n)
⊢ √(2 * π * ↑n) * (↑n / rexp 1) ^ n ≤ ↑n !

Tactic:
rw [this, ← le_div_iff₀ (by positivity)]

Goal state after:
case inr
n : ℕ
hn : n ≠ 0
this : √(2 * π * ↑n) * (↑n / rexp 1) ^ n = √π * (√(2 * ↑n) * (↑n / rexp 1) ^ n)
⊢ √π ≤ ↑n ! / (√(2 * ↑n) * (↑n / rexp 1) ^ n)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Orthogonality

Goal state before:
pp: n m : ℕ
h : n ≠ m
⊢ (0 + ∫ (x : ℝ), eval x (T ℝ (↑n - ↑m)) ∂measureT) / 2 = 0

Tactic:
integral_eval_T_real_measureT_of_ne_zero (by grind)

Goal state after:
n m : ℕ
h : n ≠ m
⊢ (0 + 0) / 2 = 0
Module: Mathlib.NumberTheory.Niven

Goal state before:
pp: q : ℚ
⊢ IsIntegral ℤ (2 * cos (↑q * ↑π))

Tactic:
cos.eq_1,

Goal state after:
q : ℚ
⊢ IsIntegral ℤ (2 * ((cexp (↑q * ↑π * I) + cexp (-(↑q * ↑π) * I)) / 2))
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.ChebyshevGauss

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

Tactic:
by norm_cast at this ⊢

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

Goal state before:
pp: n : ℤ
hn : n ≠ 0
x : ℝ
hx : 1 < x
⊢ 1 < eval x (T ℝ n)

Tactic:
have : arcosh x ≠ 0 := by grind [cosh_arcosh, cosh_zero]
  rw [← cosh_arcosh (le_of_lt hx), T_real_cosh, one_lt_cosh, mul_ne_zero_iff]
  exact ⟨by norm_cast, by assumption⟩

Goal state after:
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable

Goal state before:
pp: z : ℂ
hz : z ≠ 0
c₁ c₂ : ℤ
⊢ Summable fun n ↦ ((↑n * z + ↑c₁) * (↑n * z + ↑c₂))⁻¹

Tactic:
apply summable_inv_of_isBigO_rpow_inv (a := 2) (by norm_cast)
  simp only [Real.rpow_two, abs_mul_abs_self, pow_two]
  simpa using (linear_inv_isBigO_left c₂ hz).mul (linear_inv_isBigO_left c₁ hz)

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

Goal state before:
pp: x : ℂ
hx : x ∈ ℂ_ℤ
⊢ ∏' (i : ℕ), (1 + sineTerm x i) = Complex.sin (↑π * x) / (↑π * x)

Tactic:
rw [← Multipliable.hasProd_iff (multipliable_sineTerm x),
    Multipliable.hasProd_iff_tendsto_nat (multipliable_sineTerm x)]
  exact tendsto_euler_sin_prod' (integerComplement.ne_zero hx)

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

Goal state before:
pp: n : ℕ
hn0 : ¬n = 0
⊢ fib (-↑n + 1) = (-1) ^ (n + 1) * ↑(Nat.fib n) + (-1) ^ (1 + (n + 1)) * ↑(Nat.fib (n + 1))

Tactic:
else

Goal state after:
n : ℕ
hn0 : ¬n = 0
⊢ fib (-↑n + 1) = (-1) ^ (n + 1) * ↑(Nat.fib n) + (-1) ^ (1 + (n + 1)) * ↑(Nat.fib (n + 1))
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent

Goal state before:
pp: A B : ℝ
hB : 0 < B
k : ℕ
hk : 1 ≤ k
⊢ Summable fun a ↦ cotTermUpperBound k A B hB a

Tactic:
simp_rw [← mul_assoc]
  apply Summable.mul_left
  conv => enter [1, n]; rw [show (-1 - k : ℤ) = -(1 + k :) by lia, zpow_neg, zpow_natCast];
          enter [1, 1, 1]; norm_cast
  rw [summable_norm_iff, summable_nat_add_iff (f := fun n : ℕ ↦ ((n : ℝ) ^ (1 + k))⁻¹)]
  exact summable_nat_pow_inv.mpr <| by lia

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

Goal state before:
pp: n l : ℕ
this : DifferentiableOn ℂ (fun z ↦ (-1) ^ l * ↑l ! * ((z + (↑n + 1)) ^ (-1 - ↑l) + (z - (↑n + 1)) ^ (-1 - ↑l))) ℍₒ
⊢ DifferentiableOn ℂ (iteratedDerivWithin l (fun z ↦ cotTerm z n) ℍₒ) ℍₒ

Tactic:
by
    exact this.congr fun z hz ↦ eqOn_iteratedDerivWithin_cotTerm_upperHalfPlaneSet l n hz

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

Goal state before:
pp: H : Type u
inst✝² : NormedAddCommGroup H
inst✝¹ : InnerProductSpace ℂ H
inst✝ : CompleteSpace H
S T : VonNeumannAlgebra H
h : (fun S ↦ S.carrier) S = (fun S ↦ S.carrier) T
⊢ S = T

Tactic:
obtain ⟨⟨⟨⟨⟨⟨_, _⟩, _⟩, _⟩, _⟩, _⟩, _⟩ := S; cases T; congr

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

Goal state before:
pp: u : ℕ → ℝ
l : ℝ
hmono : Monotone u
hlim :
  ∀ (a : ℝ),
    1 < a →
      ∃ c,
        (∀ᶠ (n : ℕ) in atTop, ↑(c (n + 1)) ≤ a * ↑(c n)) ∧
          Tendsto c atTop atTop ∧ Tendsto (fun n ↦ u (c n) / ↑(c n)) atTop (𝓝 l)
lnonneg : 0 ≤ l
A : ∀ (ε : ℝ), 0 < ε → ∀ᶠ (n : ℕ) in atTop, u n - ↑n * l ≤ ε * (1 + ε + l) * ↑n
B : ∀ (ε : ℝ), 0 < ε → ∀ᶠ (n : ℕ) in atTop, ↑n * l - u n ≤ ε * (1 + l) * ↑n
d : ℝ
hd : d < l
ε : ℝ
hε : d + ε * (1 + l) < l
εpos : 0 < ε
n : ℕ
hn : ↑n * l - u n ≤ ε * (1 + l) * ↑n
npos : n ∈ Set.Ioi 0
⊢ (↑n)⁻¹ * (↑n * l - ε * (1 + l) * ↑n) ≤ (↑n)⁻¹ * u n

Tactic:
by gcongr; linarith only [hn]

Goal state after:
Module: Mathlib.Analysis.SumIntegralComparisons

Goal state before:
pp: f : ℝ → ℝ
N : ℕ
anti : AntitoneOn f (Ici ↑N)
integrable : IntegrableOn f (Ioi ↑N) volume
nonneg : ∀ t ∈ Ioi ↑N, 0 ≤ f t
⊢ Summable fun n ↦ f ↑n

Tactic:
← summable_nat_add_iff (N + 1)

Goal state after:
f : ℝ → ℝ
N : ℕ
anti : AntitoneOn f (Ici ↑N)
integrable : IntegrableOn f (Ioi ↑N) volume
nonneg : ∀ t ∈ Ioi ↑N, 0 ≤ f t
⊢ Summable fun n ↦ f ↑(n + (N + 1))