mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Normed.Order.UpperLower

Goal state before:
pp: α : Type u_1
inst✝² : NormedCommGroup α
inst✝¹ : Preorder α
inst✝ : IsOrderedMonoid α
s : Set α
hs : IsLowerSet s
ε : ℝ
⊢ IsLowerSet (⋂ ε_1, ⋂ (_ : max 0 ε < ε_1), thickening ε_1 s)

Tactic:
exact isLowerSet_iInter₂ fun δ _ => hs.thickening' _

Goal state after:
Module: Mathlib.Topology.MetricSpace.Contracting

Goal state before:
pp: K : ℝ≥0
⊢ 1 - ↑K ≠ ∞

Tactic:
by
  norm_cast
  exact ENNReal.coe_ne_top

Goal state after:
Module: Mathlib.Analysis.ODE.ExistUnique

Goal state before:
pp: case refine_3
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℝ → E → E
tmin tmax : ℝ
t₀ : ↑(Icc tmin tmax)
x₀ : E
a r L K : ℝ≥0
hf : IsPicardLindelof f t₀ x₀ a r L K
α : (x : E) → x ∈ closedBall x₀ ↑r → FunSpace t₀ x₀ r L
hα : ∀ (x : E) (hx : x ∈ closedBall x₀ ↑r), IsFixedPt (FunSpace.next hf hx) (α x hx)
α' : E → ℝ → E := fun x ↦ if hx : x ∈ closedBall x₀ ↑r then (α x hx).compProj else 0
hα' : α' = fun x ↦ if hx : x ∈ closedBall x₀ ↑r then (α x hx).compProj else 0
⊢ ∃ L', ∀ t ∈ Icc tmin tmax, LipschitzOnWith L' (fun x ↦ α' x t) (closedBall x₀ ↑r)

Tactic:
· obtain ⟨L', h⟩ := FunSpace.exists_forall_closedBall_funSpace_dist_le_mul hf
    refine ⟨L', fun t ht ↦ LipschitzOnWith.of_dist_le_mul fun x hx y hy ↦ ?_⟩
    simp_rw [hα']
    rw [dif_pos hx, dif_pos hy, FunSpace.compProj_apply, FunSpace.compProj_apply,
      ← FunSpace.toContinuousMap_apply_eq_apply, ← FunSpace.toContinuousMap_apply_eq_apply]
    have : Nonempty (Icc tmin tmax) := ⟨t₀⟩
    apply ContinuousMap.dist_le_iff_of_nonempty.mp
    exact h x y hx hy (α x hx) (α y hy) (hα x hx) (hα y hy)

Goal state after:
Module: Mathlib.Analysis.Polynomial.CauchyBound

Goal state before:
pp: K : Type u_1
inst✝ : NormedDivisionRing K
p : K[X]
hp : p ≠ 0
a : K
h : ‖p.leadingCoeff‖₊ * ‖a‖₊ ^ p.natDegree ≤ ‖∑ i ∈ range p.natDegree, p.coeff i * a ^ i‖₊
pld : ‖p.leadingCoeff‖₊ ≠ 0
⊢ (∑ x ∈ range p.natDegree, ‖p.coeff x‖₊ * ‖a‖₊ ^ x) / ‖p.leadingCoeff‖₊ ≤
    (∑ x ∈ range p.natDegree, ‖p.leadingCoeff‖₊ * (p.cauchyBound - 1) * ‖a‖₊ ^ x) / ‖p.leadingCoeff‖₊

Tactic:
by
      gcongr (∑ x ∈ _, ?_ * _) / _
      rw [cauchyBound, add_tsub_cancel_right]
      field_simp
      apply le_sup (f := (‖p.coeff ·‖₊)) ‹_›

Goal state after:
Module: Mathlib.Analysis.Polynomial.Norm

Goal state before:
pp: case pos
A : Type u_1
inst✝ : SeminormedRing A
p : A[X]
h : p.support.Nonempty
⊢ p.supNorm = p.support.sup' h (norm ∘ p.coeff)

Tactic:
simp only [supNorm, gaussNorm, h, ↓reduceDIte, one_pow, mul_one, Function.comp_apply]
    congr

Goal state after:
Module: Mathlib.RingTheory.Polynomial.GaussNorm

Goal state before:
pp: c : ℝ
R : Type u_3
inst✝ : Ring R
v : AbsoluteValue R ℝ
hna : IsNonarchimedean ⇑v
hc : 0 < c
p q : R[X]
hc0 : 0 ≤ c
i : ℕ
hi_p : gaussNorm v c p = v (p.coeff i) * c ^ i
hlt_p : ∀ j < i, v (p.coeff j) * c ^ j < gaussNorm v c p
j : ℕ
hj_q : gaussNorm v c q = v (q.coeff j) * c ^ j
hlt_q : ∀ j_1 < j, v (q.coeff j_1) * c ^ j_1 < gaussNorm v c q
⊢ gaussNorm v c p * gaussNorm v c q ≤ gaussNorm v c (p * q)

Tactic:
wlog hvpq : v (p.coeff i) ≠ 0 ∧ v (q.coeff j) ≠ 0

Goal state after:
case inr
c : ℝ
R : Type u_3
inst✝ : Ring R
v : AbsoluteValue R ℝ
hna : IsNonarchimedean ⇑v
hc : 0 < c
p q : R[X]
hc0 : 0 ≤ c
i : ℕ
hi_p : gaussNorm v c p = v (p.coeff i) * c ^ i
hlt_p : ∀ j < i, v (p.coeff j) * c ^ j < gaussNorm v c p
j : ℕ
hj_q : gaussNorm v c q = v (q.coeff j) * c ^ j
hlt_q : ∀ j_1 < j, v (q.coeff j_1) * c ^ j_1 < gaussNorm v c q
this :
  ∀ {c : ℝ} {R : Type u_3} [inst : Ring R] {v : AbsoluteValue R ℝ},
    IsNonarchimedean ⇑v →
      0 < c →
        ∀ (p q : R[X]),
          0 ≤ c →
            ∀ (i : ℕ),
              gaussNorm v c p = v (p.coeff i) * c ^ i →
                (∀ j < i, v (p.coeff j) * c ^ j < gaussNorm v c p) →
                  ∀ (j : ℕ),
                    gaussNorm v c q = v (q.coeff j) * c ^ j →
                      (∀ j_1 < j, v (q.coeff j_1) * c ^ j_1 < gaussNorm v c q) →
                        v (p.coeff i) ≠ 0 ∧ v (q.coeff j) ≠ 0 →
                          gaussNorm v c p * gaussNorm v c q ≤ gaussNorm v c (p * q)
hvpq : ¬(v (p.coeff i) ≠ 0 ∧ v (q.coeff j) ≠ 0)
⊢ gaussNorm v c p * gaussNorm v c q ≤ gaussNorm v c (p * q)

c✝ : ℝ
R✝ : Type u_3
inst✝¹ : Ring R✝
v✝ : AbsoluteValue R✝ ℝ
c : ℝ
R : Type u_3
inst✝ : Ring R
v : AbsoluteValue R ℝ
hna : IsNonarchimedean ⇑v
hc : 0 < c
p q : R[X]
hc0 : 0 ≤ c
i : ℕ
hi_p : gaussNorm v c p = v (p.coeff i) * c ^ i
hlt_p : ∀ j < i, v (p.coeff j) * c ^ j < gaussNorm v c p
j : ℕ
hj_q : gaussNorm v c q = v (q.coeff j) * c ^ j
hlt_q : ∀ j_1 < j, v (q.coeff j_1) * c ^ j_1 < gaussNorm v c q
hvpq : v (p.coeff i) ≠ 0 ∧ v (q.coeff j) ≠ 0
⊢ gaussNorm v c p * gaussNorm v c q ≤ gaussNorm v c (p * q)
Module: Mathlib.RingTheory.MvPowerSeries.GaussNorm

Goal state before:
pp: α : Type u_3
S : Type u_4
inst✝¹ : LinearOrder S
inst✝ : AddCommGroup α
f : α → S
na : IsNonarchimedean f
Neg : ∀ (a : α), f a = f (-a)
a b : α
hne : f a ≠ f b
hab : f a > f b
h : f (a + b + -b) ≤ f (-b)
⊢ f (-b) < f (a + b + -b)

Tactic:
simpa [Neg b] using hab

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

Goal state before:
pp: case inr
b : ℕ
digits : ℕ → Fin b
hb : 1 < b
⊢ Summable fun x ↦ (↑b - 1) * (↑b * ↑b ^ x)⁻¹

Tactic:
mul_inv,

Goal state after:
case inr
b : ℕ
digits : ℕ → Fin b
hb : 1 < b
⊢ Summable fun x ↦ (↑b - 1) * ((↑b)⁻¹ * (↑b ^ x)⁻¹)
Module: Mathlib.Analysis.Real.OfDigits

Goal state before:
pp: case e'_4
b : ℕ
digits : ℕ → Fin b
hb : 1 < ↑b
⊢ 1 = ∑' (n : ℕ), (↑b - 1) * (↑b * ↑b ^ n)⁻¹

Tactic:
mul_inv,

Goal state after:
case e'_4
b : ℕ
digits : ℕ → Fin b
hb : 1 < ↑b
⊢ 1 = ∑' (n : ℕ), (↑b - 1) * ((↑b)⁻¹ * (↑b ^ n)⁻¹)
Module: Mathlib.Analysis.Real.OfDigits

Goal state before:
pp: case inr.convert_1
b : ℕ
digits : ℕ → Fin b
hb : 1 < ↑b
⊢ Summable fun x ↦ (↑b - 1) * (↑b * ↑b ^ x)⁻¹

Tactic:
mul_inv,

Goal state after:
case inr.convert_1
b : ℕ
digits : ℕ → Fin b
hb : 1 < ↑b
⊢ Summable fun x ↦ (↑b - 1) * ((↑b)⁻¹ * (↑b ^ x)⁻¹)
Module: Mathlib.Analysis.Real.Hyperreal

Goal state before:
pp: ⊢ stdPart ω = 0

Tactic:
by
  rw [stdPart_eq_zero]
  exact archimedeanClassMk_omega_neg.ne

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

Goal state before:
pp: r : ℝ
f : ℝ → ℝ
hf : ContinuousAt f r
g : ℕ → ℝ
hxr : Germ.Tendsto (ofSeq g) (𝓝 r)
⊢ (Germ.map f (ofSeq g)).Tendsto (𝓝 (f r))

Tactic:
exact hf.tendsto.comp hxr

Goal state after:
Module: Mathlib.Analysis.Polynomial.MahlerMeasure

Goal state before:
pp: A : Type u_1
inst✝ : Semiring A
v : A →+* ℂ
⊢ mapMahlerMeasure 0 v = 0

Tactic:
simp [mapMahlerMeasure]

Goal state after:
Module: Mathlib.Analysis.Polynomial.MahlerMeasure

Goal state before:
pp: A : Type u_1
inst✝ : Semiring A
v : A →+* ℂ
⊢ mapMahlerMeasure 1 v = 1

Tactic:
simp [mapMahlerMeasure]

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

Goal state before:
pp: x : ℝ*
⊢ x.Infinitesimal ↔ 0 < ArchimedeanClass.mk x

Tactic:
by
  rw [Infinitesimal, isSt_iff, stdPart_eq_zero, lt_iff_le_and_ne']

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

Goal state before:
pp: x : ℝ
hx : x ∈ Ioi 1
⊢ ¬sinh (arcosh x) = 0

Tactic:
sinh_eq_zero

Goal state after:
x : ℝ
hx : x ∈ Ioi 1
⊢ ¬arcosh x = 0
Module: Mathlib.Analysis.SpecialFunctions.Arcosh

Goal state before:
pp: n : WithTop ℕ∞
x : ℝ
hx : x ∈ Ioi 1
⊢ ¬sinh (↑coshOpenPartialHomeomorph.symm x) = 0

Tactic:
sinh_eq_zero

Goal state after:
n : WithTop ℕ∞
x : ℝ
hx : x ∈ Ioi 1
⊢ ¬↑coshOpenPartialHomeomorph.symm x = 0
Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean

Goal state before:
pp: x y : ℝ≥0
⊢ x.agm y ≤ max x y

Tactic:
wlog h : x ≤ y generalizing x y
  · simpa [agm_comm, max_comm] using this (not_le.mp h).le
  rw [max_eq_right h]
  apply (agm_le_agmSequences_snd 0).trans
  rw [agmSequences_zero]
  exact (le_gm_and_am_le h).2

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arctan

Goal state before:
pp: case e'_6
z : ℂ
hz : ‖z‖ < 1
this :
  HasSum (fun x ↦ -I / 2 * (((-1) ^ (2 * x.1 + ↑x.2 + 1) + 1) * (z * I) ^ (2 * x.1 + ↑x.2) / ↑(2 * x.1 + ↑x.2)))
    (-I / 2 * log ((1 + z * I) / (1 - z * I)))
k : ℕ
⊢ (-1) ^ k * z ^ (2 * k + 1) / ↑(2 * k + 1) =
    -I / 2 * (((-1) ^ (2 * k + 0 + 1) + 1) * (z * I) ^ (2 * k + 0) / ↑(2 * k + 0)) +
      -I / 2 * (((-1) ^ (2 * k + 1 + 1) + 1) * (z * I) ^ (2 * k + 1) / ↑(2 * k + 1))

Tactic:
Odd.neg_one_pow (n := 2 * k + 0 + 1) (by simp),

Goal state after:
case e'_6
z : ℂ
hz : ‖z‖ < 1
this :
  HasSum (fun x ↦ -I / 2 * (((-1) ^ (2 * x.1 + ↑x.2 + 1) + 1) * (z * I) ^ (2 * x.1 + ↑x.2) / ↑(2 * x.1 + ↑x.2)))
    (-I / 2 * log ((1 + z * I) / (1 - z * I)))
k : ℕ
⊢ (-1) ^ k * z ^ (2 * k + 1) / ↑(2 * k + 1) =
    -I / 2 * ((-1 + 1) * (z * I) ^ (2 * k + 0) / ↑(2 * k + 0)) +
      -I / 2 * (((-1) ^ (2 * k + 1 + 1) + 1) * (z * I) ^ (2 * k + 1) / ↑(2 * k + 1))
Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean

Goal state before:
pp: x y : ℝ≥0
hn : x ≠ y
n : ℕ
p : ℝ≥0 := (x.agmSequences y n).1
q : ℝ≥0 := (x.agmSequences y n).2
plq : p < q
⊢ (p + q) / 2 < q

Tactic:
← add_halves q

Goal state after:
x y : ℝ≥0
hn : x ≠ y
n : ℕ
p : ℝ≥0 := (x.agmSequences y n).1
q : ℝ≥0 := (x.agmSequences y n).2
plq : p < q
⊢ (p + q) / 2 < q / 2 + q / 2
Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy

Goal state before:
pp: p : ℝ
⊢ binEntropy p ≤ log 2

Tactic:
by
  obtain rfl | hp := eq_or_ne p 2⁻¹
  · simp
  · exact (binEntropy_lt_log_two.2 hp).le

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

Goal state before:
pp: p : ℝ
⊢ deriv binEntropy p = log (1 - p) - log p

Tactic:
by_cases hp : p ≠ 0 ∧ p ≠ 1

Goal state after:
case pos
p : ℝ
hp : p ≠ 0 ∧ p ≠ 1
⊢ deriv binEntropy p = log (1 - p) - log p

case neg
p : ℝ
hp : ¬(p ≠ 0 ∧ p ≠ 1)
⊢ deriv binEntropy p = log (1 - p) - log p
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
h₂ : ∀ᶠ (p : ℝ) in 𝓝[>] 0, p ≤ 1 / (sSup ((fun x ↦ ‖log x‖) '' s) + 1)
hcont : ContinuousOn (fun x ↦ ‖log x‖ ^ 2) s
hcont' : ContinuousOn (fun x ↦ ‖log x‖) s
p : ℝ
hp₁ : 0 < p
hp₂ : p < pbound
hp₃ : p ≤ 1 / (sSup ((fun x ↦ ‖log x‖) '' s) + 1)
x : ℝ
hx : x ∈ s
hx' : ‖p * log x‖ ≤ 1
pinv_nonneg : 0 ≤ p⁻¹
⊢ ‖p⁻¹ * (x ^ p - 1) - log x‖ ≤ ε

Tactic:
calc
    _ ≤ p * ‖log x‖ ^ 2 := Real.norm_inv_mul_rpow_sub_one_sub_log_le hp₁ (hs hx) hx'
    _ ≤ p * sSup ((fun x => ‖log x‖ ^ 2) '' s) := by
          gcongr
          refine le_csSup ?_ (by grind)
          grind [IsCompact.bddAbove, ← IsCompact.image_of_continuousOn]
    _ ≤ pbound * (sSup ((fun x => ‖log x‖ ^ 2) '' s) + 1) := by gcongr; grind
    _ = ε := by grind

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

Goal state before:
pp: case e_f
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
this : log (b / a) • V = ∫ (x : ℝ) in a..b, x⁻¹ • V
x : ℝ
⊢ x⁻¹ • f x - x⁻¹ • V = x⁻¹ • (f x - V)

Tactic:
exact (smul_sub _ _ _).symm

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

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
L R : E
inst✝ : CompleteSpace E
hf : LocallyIntegrableOn f (Ioi 0) volume
ha : 0 < a
hb : 0 < b
hL : Tendsto f (𝓝[>] 0) (𝓝 L)
hR : Tendsto f atTop (𝓝 R)
u : ℝ → E := fun x ↦ x⁻¹ • f x
hint : ∀ {p q : ℝ}, 0 < p → 0 < q → IntervalIntegrable u volume p q
ε r : ℝ
hε : 0 < ε
hr : 0 < r
⊢ (∫ (x : ℝ) in ε..r, x⁻¹ • f (a * x)) - ∫ (x : ℝ) in ε..r, x⁻¹ • f (b * x) =
    (∫ (y : ℝ) in a * ε..a * r, u y) - ∫ (y : ℝ) in b * ε..b * r, u y

Tactic:
integral_comp_mul_inv_smul ha.ne',

Goal state after:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
L R : E
inst✝ : CompleteSpace E
hf : LocallyIntegrableOn f (Ioi 0) volume
ha : 0 < a
hb : 0 < b
hL : Tendsto f (𝓝[>] 0) (𝓝 L)
hR : Tendsto f atTop (𝓝 R)
u : ℝ → E := fun x ↦ x⁻¹ • f x
hint : ∀ {p q : ℝ}, 0 < p → 0 < q → IntervalIntegrable u volume p q
ε r : ℝ
hε : 0 < ε
hr : 0 < r
⊢ (∫ (x : ℝ) in a * ε..a * r, x⁻¹ • f x) - ∫ (x : ℝ) in ε..r, x⁻¹ • f (b * x) =
    (∫ (y : ℝ) in a * ε..a * r, u y) - ∫ (y : ℝ) in b * ε..b * r, u y
Module: Mathlib.Analysis.SpecialFunctions.FrullaniIntegral

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
L R : E
inst✝ : CompleteSpace E
hf : LocallyIntegrableOn f (Ioi 0) volume
ha : 0 < a
hb : 0 < b
hL : Tendsto f (𝓝[>] 0) (𝓝 L)
hR : Tendsto f atTop (𝓝 R)
u : ℝ → E := fun x ↦ x⁻¹ • f x
hint : ∀ {p q : ℝ}, 0 < p → 0 < q → IntervalIntegrable u volume p q
ε r : ℝ
hε : 0 < ε
hr : 0 < r
⊢ ∫ (x : ℝ) in ε..r, x⁻¹ • (f (a * x) - f (b * x)) = (∫ (x : ℝ) in a * ε..b * ε, u x) - ∫ (x : ℝ) in a * r..b * r, u x

Tactic:
calc ∫ x in ε..r, x⁻¹ • (f (a * x) - f (b * x))
      _ = (∫ x in ε..r, x⁻¹ • f (a * x)) - ∫ x in ε..r, x⁻¹ • f (b * x) := by
        simp_rw [smul_sub]
        exact integral_sub (intervalIntegrable_inv_smul_comp_mul hf hε hr ha)
          (intervalIntegrable_inv_smul_comp_mul hf hε hr hb)
      _ = (∫ y in a * ε..a * r, u y) - ∫ y in b * ε..b * r, u y := by
        rw [integral_comp_mul_inv_smul ha.ne', integral_comp_mul_inv_smul hb.ne']
      _ = _ := integral_interval_sub_interval_comm
                 (hint (mul_pos ha hε) (mul_pos ha hr))
                 (hint (mul_pos hb hε) (mul_pos hb hr))
                 (hint (mul_pos ha hε) (mul_pos hb hε))

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
ht' : ¬t = 0
hxt : t + x ≠ 0
⊢ t ^ p / t * x / (t + x) = t ^ (p - 1) * x / (t + x)

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

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
hx_zero : ¬x = 0
⊢ p.rpowIntegrand₀₁ t x = t ^ (p - 1) * x / (t + x)

Tactic:
rpowIntegrand₀₁_eq_pow_div hp ht hx

Goal state after:
p t x : ℝ
hp : p ∈ Ioo 0 1
ht : 0 ≤ t
hx : 0 ≤ x
hx_zero : ¬x = 0
⊢ t ^ (p - 1) * x / (t + x) = t ^ (p - 1) * x / (t + x)
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation

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

Tactic:
gcongr t ^ (p - 1) * ?_

Goal state after:
case hbc
p t : ℝ
hp : p ∈ Ioo 0 1
ht : 1 ≤ t
⊢ 1 / 2 * 1 / t ≤ 1 / (t + 1)
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation

Goal state before:
pp: case meas
p x : ℝ
hp : p ∈ Ioo 0 1
hx : 0 ≤ x
⊢ AEStronglyMeasurable (fun x_1 ↦ p.rpowIntegrand₀₁ x_1 x) (volume.restrict (Ioo 0 1))

pp: case finite
p x : ℝ
hp : p ∈ Ioo 0 1
hx : 0 ≤ x
⊢ HasFiniteIntegral (fun x_1 ↦ p.rpowIntegrand₀₁ x_1 x) (volume.restrict (Ioo 0 1))

Tactic:
case meas =>
    refine ContinuousOn.aestronglyMeasurable ?_ measurableSet_Ioo
    exact ContinuousOn.mono (continuousOn_rpowIntegrand₀₁ hp hx) Ioo_subset_Ioi_self

Goal state after:
case finite
p x : ℝ
hp : p ∈ Ioo 0 1
hx : 0 ≤ x
⊢ HasFiniteIntegral (fun x_1 ↦ p.rpowIntegrand₀₁ x_1 x) (volume.restrict (Ioo 0 1))
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation

Goal state before:
pp: case hff'
p x : ℝ
hp : p ∈ Ioo 0 1
hx✝ : 0 ≤ x
hx : 0 < x
this :
  ∫ (t : ℝ) in Ioi 0, ((fun x_1 ↦ p.rpowIntegrand₀₁ x_1 x) ∘ fun x_1 ↦ x * x_1) t * x =
    x ^ p * ∫ (t : ℝ) in Ioi 0, p.rpowIntegrand₀₁ t 1
⊢ ∀ x_1 ∈ Ioi 0, HasDerivWithinAt (fun x_2 ↦ x * x_2) x (Ioi x_1) x_1

pp: case hg_cont
p x : ℝ
hp : p ∈ Ioo 0 1
hx✝ : 0 ≤ x
hx : 0 < x
this :
  ∫ (t : ℝ) in Ioi 0, ((fun x_1 ↦ p.rpowIntegrand₀₁ x_1 x) ∘ fun x_1 ↦ x * x_1) t * x =
    x ^ p * ∫ (t : ℝ) in Ioi 0, p.rpowIntegrand₀₁ t 1
⊢ ContinuousOn (fun x_1 ↦ p.rpowIntegrand₀₁ x_1 x) ((fun x_1 ↦ x * x_1) '' Ioi 0)

pp: case hg1
p x : ℝ
hp : p ∈ Ioo 0 1
hx✝ : 0 ≤ x
hx : 0 < x
this :
  ∫ (t : ℝ) in Ioi 0, ((fun x_1 ↦ p.rpowIntegrand₀₁ x_1 x) ∘ fun x_1 ↦ x * x_1) t * x =
    x ^ p * ∫ (t : ℝ) in Ioi 0, p.rpowIntegrand₀₁ t 1
⊢ IntegrableOn (fun x_1 ↦ p.rpowIntegrand₀₁ x_1 x) ((fun x_1 ↦ x * x_1) '' Ici 0) volume

pp: case hg2
p x : ℝ
hp : p ∈ Ioo 0 1
hx✝ : 0 ≤ x
hx : 0 < x
this :
  ∫ (t : ℝ) in Ioi 0, ((fun x_1 ↦ p.rpowIntegrand₀₁ x_1 x) ∘ fun x_1 ↦ x * x_1) t * x =
    x ^ p * ∫ (t : ℝ) in Ioi 0, p.rpowIntegrand₀₁ t 1
⊢ IntegrableOn (fun x_1 ↦ ((fun x_2 ↦ p.rpowIntegrand₀₁ x_2 x) ∘ fun x_2 ↦ x * x_2) x_1 * x) (Ici 0) volume

Tactic:
· simpa using fun t _ ↦ hasDerivWithinAt_id t (Ioi t) |>.const_mul x

Goal state after:
case hg_cont
p x : ℝ
hp : p ∈ Ioo 0 1
hx✝ : 0 ≤ x
hx : 0 < x
this :
  ∫ (t : ℝ) in Ioi 0, ((fun x_1 ↦ p.rpowIntegrand₀₁ x_1 x) ∘ fun x_1 ↦ x * x_1) t * x =
    x ^ p * ∫ (t : ℝ) in Ioi 0, p.rpowIntegrand₀₁ t 1
⊢ ContinuousOn (fun x_1 ↦ p.rpowIntegrand₀₁ x_1 x) ((fun x_1 ↦ x * x_1) '' Ioi 0)

case hg1
p x : ℝ
hp : p ∈ Ioo 0 1
hx✝ : 0 ≤ x
hx : 0 < x
this :
  ∫ (t : ℝ) in Ioi 0, ((fun x_1 ↦ p.rpowIntegrand₀₁ x_1 x) ∘ fun x_1 ↦ x * x_1) t * x =
    x ^ p * ∫ (t : ℝ) in Ioi 0, p.rpowIntegrand₀₁ t 1
⊢ IntegrableOn (fun x_1 ↦ p.rpowIntegrand₀₁ x_1 x) ((fun x_1 ↦ x * x_1) '' Ici 0) volume

case hg2
p x : ℝ
hp : p ∈ Ioo 0 1
hx✝ : 0 ≤ x
hx : 0 < x
this :
  ∫ (t : ℝ) in Ioi 0, ((fun x_1 ↦ p.rpowIntegrand₀₁ x_1 x) ∘ fun x_1 ↦ x * x_1) t * x =
    x ^ p * ∫ (t : ℝ) in Ioi 0, p.rpowIntegrand₀₁ t 1
⊢ IntegrableOn (fun x_1 ↦ ((fun x_2 ↦ p.rpowIntegrand₀₁ x_2 x) ∘ fun x_2 ↦ x * x_2) x_1 * x) (Ici 0) volume
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation

Goal state before:
pp: p : ℝ
hp : p ∈ Ioo 0 1
⊢ ∫ (t : ℝ) in Ioi 1, 1 / 2 * t ^ (p - 2) ≤ ∫ (t : ℝ) in Ioi 1, p.rpowIntegrand₀₁ t 1

Tactic:
refine setIntegral_mono_on ?_ ?_ measurableSet_Ioi ?_

Goal state after:
case refine_1
p : ℝ
hp : p ∈ Ioo 0 1
⊢ IntegrableOn (fun t ↦ 1 / 2 * t ^ (p - 2)) (Ioi 1) volume

case refine_2
p : ℝ
hp : p ∈ Ioo 0 1
⊢ IntegrableOn (fun t ↦ p.rpowIntegrand₀₁ t 1) (Ioi 1) volume

case refine_3
p : ℝ
hp : p ∈ Ioo 0 1
⊢ ∀ x ∈ Ioi 1, 1 / 2 * x ^ (p - 2) ≤ p.rpowIntegrand₀₁ x 1
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
h₁ : x ^ p = x * x ^ (p - 1)
⊢ x * x ^ (p - 1) =
    (∫ (t : ℝ) in Ioi 0, (p - 1).rpowIntegrand₀₁ t 1)⁻¹ * (x * ∫ (x_1 : ℝ) in Ioi 0, (p - 1).rpowIntegrand₀₁ x_1 x)

Tactic:
rpow_eq_const_mul_integral (by grind) hx

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
h₁ : x ^ p = x * x ^ (p - 1)
⊢ x * ((∫ (t : ℝ) in Ioi 0, (p - 1).rpowIntegrand₀₁ t 1)⁻¹ * ∫ (t : ℝ) in Ioi 0, (p - 1).rpowIntegrand₀₁ t x) =
    (∫ (t : ℝ) in Ioi 0, (p - 1).rpowIntegrand₀₁ t 1)⁻¹ * (x * ∫ (x_1 : ℝ) in Ioi 0, (p - 1).rpowIntegrand₀₁ x_1 x)
Module: Mathlib.Data.Int.Log

Goal state before:
pp: case succ
R : Type u_1
inst✝³ : Semifield R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorSemiring R
b n✝ : ℕ
⊢ log b ↑(n✝ + 1) = ↑(Nat.log b (n✝ + 1))

Tactic:
rw [log_of_one_le_right, Nat.floor_natCast]
    simp

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

Goal state before:
pp: b x y : ℝ
hb : 1 < b
hy : 0 < y
⊢ x < logb b y ↔ b ^ x < y

Tactic:
by
  rw [← rpow_lt_rpow_left_iff hb, rpow_logb (b_pos hb) (b_ne_one' hb) hy]

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

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

Tactic:
by
  rw [logb_pos_iff hb (lt_trans zero_lt_one hx)]
  exact hx

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

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

Tactic:
rw [norm_eq_abs, deriv_mulExpNegMulSq]
  have heq : exp (-(ε * x * x)) + x * (exp (-(ε * x * x)) * (-2 * ε * x))
      = exp (-(ε * x * x)) * (1 - 2 * (ε * x * x)) := by ring
  rw [heq, abs_mul, abs_exp]
  set y := ε * x * x with hy
  have hynonneg : 0 ≤ y := by
    rw [hy, mul_assoc]
    exact mul_nonneg hε.le (mul_self_nonneg x)
  apply mul_le_of_le_inv_mul₀ (zero_le_one' ℝ) (exp_nonneg _)
  simp only [← exp_neg (-y), neg_neg, mul_one, abs_le, neg_le_sub_iff_le_add, tsub_le_iff_right]
  refine ⟨le_trans two_mul_le_exp ((le_add_iff_nonneg_left (exp y)).mpr zero_le_one), ?_⟩
  exact le_trans (one_le_exp hynonneg) (le_add_of_nonneg_right (by simp [hynonneg]))

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

Goal state before:
pp: x : ℝ
this : x = (fun ε ↦ ε.mulExpNegMulSq x) 0
⊢ Tendsto (fun ε ↦ ε.mulExpNegMulSq x) (𝓝 0) (𝓝 x)

Tactic:
nth_rw 2 [this]

Goal state after:
x : ℝ
this : x = (fun ε ↦ ε.mulExpNegMulSq x) 0
⊢ Tendsto (fun ε ↦ ε.mulExpNegMulSq x) (𝓝 0) (𝓝 ((fun ε ↦ ε.mulExpNegMulSq x) 0))
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)
⊢ ∃ K, IsCompact (closure K) ∧ P Kᶜ < ε

Tactic:
refine ⟨interUnionBalls seq u t, isCompact_closure_interUnionBalls h_basis.toHasBasis seq u, ?_⟩

Goal state after:
α : 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)
⊢ P (interUnionBalls seq u t)ᶜ < ε
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✝ : μ.IsOpenPosMeasure
a✝ : Nontrivial E
⊢ ∀ (U : Set ↑(sphere 0 1)), IsOpen U → U.Nonempty → μ.toSphere U ≠ 0

Tactic:
rintro U hUo hU

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✝ : μ.IsOpenPosMeasure
a✝ : Nontrivial E
U : Set ↑(sphere 0 1)
hUo : IsOpen U
hU : U.Nonempty
⊢ μ.toSphere U ≠ 0