mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Polynomial.GaussNorm

Goal state before:
pp: R : Type u_1
F : Type u_2
inst✝³ : Semiring R
inst✝² : FunLike F R ℝ
v : F
p : R[X]
inst✝¹ : ZeroHomClass F R ℝ
inst✝ : NonnegHomClass F R ℝ
⊢ gaussNorm v 0 p = v (p.coeff 0)

Tactic:
by
  have : (fun i ↦ v (p.coeff i) * 0 ^ i) = fun i ↦ if i = 0 then v (p.coeff 0) else 0 := by
    aesop
  rcases eq_or_ne (p.coeff 0) 0 with _ | hcoeff0
  · simp_all [gaussNorm]
  · apply le_antisymm
    · aesop (add norm (by simp [gaussNorm, Finset.sup'_le_iff]))
    · grind [p.le_gaussNorm v (le_refl 0) 0]

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

Goal state before:
pp: case hbc
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℝ → E → E
t₀ ε : ℝ
hε : 0 < ε
x₀ : E
a r L K : ℝ≥0
hf : IsPicardLindelof f ⟨t₀, ⋯⟩ x₀ a r L K
a' r' : ℝ≥0
ha : a' ≤ a
hr : r' < a'
ha'r' : 0 < ↑a' - ↑r'
ε' : ℝ := ⋯
hε'pos : 0 < ε'
hε'_le : ε' ≤ ε
⊢ ε' ≤ (↑a' - ↑r') / (↑L + 1)

Tactic:
exact min_le_right _ _

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

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E → E
x₀ : E
hf : ContDiffAt ℝ 1 f x₀
K : ℝ≥0
s : Set E
hs : s ∈ 𝓝 x₀
hl : LipschitzOnWith K f s
a : ℝ
ha : 0 < a
has : ball x₀ a ⊆ s
L : ℝ := ⋯
hL : L = ↑K * a + ‖f x₀‖ + 1
hL0 : 0 < L
hb : ∀ x ∈ closedBall x₀ (a / 2), ‖f x‖ ≤ L
ε : ℝ := ⋯
hε0 : 0 < ε
t₀ : ℝ
⊢ ↑(NNReal.mk L ⋯) * max (t₀ + ε - ↑⟨t₀, ⋯⟩) (↑⟨t₀, ⋯⟩ - (t₀ - ε)) ≤ ↑(NNReal.mk (a / 2) ⋯) - ↑(NNReal.mk (a / 2) ⋯ / 2)

Tactic:
simp [ε, field]

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E → E
x₀ : E
hf : ContDiffAt ℝ 1 f x₀
K : ℝ≥0
s : Set E
hs : s ∈ 𝓝 x₀
hl : LipschitzOnWith K f s
a : ℝ
ha : 0 < a
has : ball x₀ a ⊆ s
L : ℝ := ↑K * a + ‖f x₀‖ + 1
hL : L = ↑K * a + ‖f x₀‖ + 1
hL0 : 0 < L
hb : ∀ x ∈ closedBall x₀ (a / 2), ‖f x‖ ≤ L
ε : ℝ := a / L / 2 / 2
hε0 : 0 < ε
t₀ : ℝ
⊢ 1 ≤ 2 - 1
Module: Mathlib.Analysis.ODE.PicardLindelof

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℝ → E → E
tmin tmax : ℝ
t₀ : ↑(Icc tmin tmax)
x₀ x : E
a r L K : ℝ≥0
hf : IsPicardLindelof f t₀ x₀ a r L K
hx : x ∈ closedBall x₀ ↑r
α : FunSpace t₀ x₀ r L
hα : IsFixedPt (FunSpace.next hf hx) α
t : ℝ
ht : t ∈ Icc tmin tmax
⊢ (FunSpace.next hf hx α).compProj t = picard f (↑t₀) x (FunSpace.next hf hx α).compProj t

Tactic:
FunSpace.compProj_apply,

Goal state after:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℝ → E → E
tmin tmax : ℝ
t₀ : ↑(Icc tmin tmax)
x₀ x : E
a r L K : ℝ≥0
hf : IsPicardLindelof f t₀ x₀ a r L K
hx : x ∈ closedBall x₀ ↑r
α : FunSpace t₀ x₀ r L
hα : IsFixedPt (FunSpace.next hf hx) α
t : ℝ
ht : t ∈ Icc tmin tmax
⊢ (FunSpace.next hf hx α).toFun (projIcc tmin tmax ⋯ t) = picard f (↑t₀) x (FunSpace.next hf hx α).compProj t
Module: Mathlib.Analysis.RCLike.ContinuousMap

Goal state before:
pp: X : Type u_1
𝕜 : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : RCLike 𝕜
f : C(X, 𝕜)
hf : IsSelfAdjoint f
a✝ : X
| f a✝

Tactic:
← hf.star_eq

Goal state after:
X : Type u_1
𝕜 : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : RCLike 𝕜
f : C(X, 𝕜)
hf : IsSelfAdjoint f
a✝ : X
| (star f) a✝
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:
max_eq_right h,

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

Goal state before:
pp: case succ
x : ℝ
b : ℕ
inst✝ : NeZero b
hx : x ∈ Set.Ico 0 1
this : b ≠ 0
n : ℕ
ih : ↑b ^ n * ∑ i ∈ Finset.range n, ofDigitsTerm (x.digits b) i = ↑⌊↑b ^ n * x⌋₊
⊢ ↑b ^ (n + 1) * ∑ i ∈ Finset.range (n + 1), ofDigitsTerm (x.digits b) i = ↑⌊↑b ^ (n + 1) * x⌋₊

Tactic:
Finset.sum_range_succ,

Goal state after:
case succ
x : ℝ
b : ℕ
inst✝ : NeZero b
hx : x ∈ Set.Ico 0 1
this : b ≠ 0
n : ℕ
ih : ↑b ^ n * ∑ i ∈ Finset.range n, ofDigitsTerm (x.digits b) i = ↑⌊↑b ^ n * x⌋₊
⊢ ↑b ^ (n + 1) * (∑ x_1 ∈ Finset.range n, ofDigitsTerm (x.digits b) x_1 + ofDigitsTerm (x.digits b) n) =
    ↑⌊↑b ^ (n + 1) * x⌋₊
Module: Mathlib.Analysis.Real.OfDigits

Goal state before:
pp: b : ℕ
inst✝ : NeZero b
this : 1 < |↑b + 1|
⊢ (↑(b + 1))⁻¹ < 1

Tactic:
simp [inv_lt_one_iff₀, NeZero.pos b]

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

Goal state before:
pp: a b c d n : ℕ
z : ℝ
hz : z ≤ (↑a / ↑b).sqrtTwoAddSeries n
hb : 0 < b
hd : 0 < d
h : a ^ 2 * d ≤ (2 * d + c) * b ^ 2
hb' : 0 < ↑b
hd' : 0 < ↑d
⊢ ↑a ^ 2 / ↑b ^ 2 ≤ 2 + ↑c / ↑d

Tactic:
add_div_eq_mul_add_div _ _ (ne_of_gt hd'),

Goal state after:
a b c d n : ℕ
z : ℝ
hz : z ≤ (↑a / ↑b).sqrtTwoAddSeries n
hb : 0 < b
hd : 0 < d
h : a ^ 2 * d ≤ (2 * d + c) * b ^ 2
hb' : 0 < ↑b
hd' : 0 < ↑d
⊢ ↑a ^ 2 / ↑b ^ 2 ≤ (2 * ↑d + ↑c) / ↑d
Module: Mathlib.Data.Rat.Sqrt

Goal state before:
pp: q : ℚ
⊢ mkRat (Int.sqrt (q * q).num) (q * q).den.sqrt = |q|

Tactic:
mul_self_num,

Goal state after:
q : ℚ
⊢ mkRat (Int.sqrt (q.num * q.num)) (q * q).den.sqrt = |q|
Module: Mathlib.NumberTheory.Real.Irrational

Goal state before:
pp: case inl
x : ℝ
m : ℤ
hm : m ≠ 0
p : ℕ
hp : Fact (Nat.Prime p)
hxr : x ^ 0 = ↑m
hv : multiplicity (↑p) m % 0 ≠ 0
⊢ Irrational x

pp: case inr
x : ℝ
n : ℕ
m : ℤ
hm : m ≠ 0
p : ℕ
hp : Fact (Nat.Prime p)
hxr : x ^ n = ↑m
hv : multiplicity (↑p) m % n ≠ 0
hnpos : n > 0
⊢ Irrational x

Tactic:
· rw [eq_comm, pow_zero, ← Int.cast_one, Int.cast_inj] at hxr
    simp [hxr, multiplicity_of_one_right (mt isUnit_iff_dvd_one.1
      (mt Int.natCast_dvd_natCast.1 hp.1.not_dvd_one))] at hv

Goal state after:
case inr
x : ℝ
n : ℕ
m : ℤ
hm : m ≠ 0
p : ℕ
hp : Fact (Nat.Prime p)
hxr : x ^ n = ↑m
hv : multiplicity (↑p) m % n ≠ 0
hnpos : n > 0
⊢ Irrational x
Module: Mathlib.Analysis.Real.Hyperreal

Goal state before:
pp: x : ℝ*
r : ℝ
h : 0 ≤ ArchimedeanClass.mk x ∧ stdPart x = r
⊢ x.IsSt r

Tactic:
by
    obtain ⟨h, rfl⟩ := h
    refine fun y hy ↦ ⟨?_, ?_⟩
    · apply lt_of_lt_stdPart coeRingHom h; simpa
    · apply lt_of_stdPart_lt coeRingHom h; simpa

Goal state after:
Module: Mathlib.NumberTheory.Real.Irrational

Goal state before:
pp: n : ℕ
x : ℝ
⊢ ↑n ≠ 0 ∧ Irrational x ↔ n ≠ 0 ∧ Irrational x

Tactic:
Nat.cast_ne_zero

Goal state after:
n : ℕ
x : ℝ
⊢ n ≠ 0 ∧ Irrational x ↔ n ≠ 0 ∧ Irrational x
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arctan

Goal state before:
pp: z : ℂ
h₁ : z ≠ I
h₂ : z ≠ -I
z₁ : 1 + z * I ≠ 0
z₂ : 1 - z * I ≠ 0
⊢ 2 * (I * (-I / 2)) = 1

Tactic:
simp [field]

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

Goal state before:
pp: case succ.refine_1
n : ℕ
IH :
  ∏ i ∈ range n, (2 * ↑i + 2) / (2 * ↑i + 1) * ((2 * ↑i + 2) / (2 * ↑i + 3)) =
    2 ^ (4 * n) * ↑n ! ^ 4 / (↑(2 * n)! ^ 2 * (2 * ↑n + 1))
⊢ ↑(2 * n)! ^ 2 * (2 * ↑n + 1) * ((2 * ↑n + 1) * (2 * ↑n + 3)) ≠ 0

Tactic:
exact ne_of_gt (by positivity)

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

Goal state before:
pp: case succ.refine_2
n : ℕ
IH :
  ∏ i ∈ range n, (2 * ↑i + 2) / (2 * ↑i + 1) * ((2 * ↑i + 2) / (2 * ↑i + 3)) =
    2 ^ (4 * n) * ↑n ! ^ 4 / (↑(2 * n)! ^ 2 * (2 * ↑n + 1))
⊢ ↑(2 * (n + 1))! ^ 2 * (2 * ↑(n + 1) + 1) ≠ 0

Tactic:
exact ne_of_gt (by positivity)

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

Goal state before:
pp: case succ.refine_3
n : ℕ
IH :
  ∏ i ∈ range n, (2 * ↑i + 2) / (2 * ↑i + 1) * ((2 * ↑i + 2) / (2 * ↑i + 3)) =
    2 ^ (4 * n) * ↑n ! ^ 4 / (↑(2 * n)! ^ 2 * (2 * ↑n + 1))
⊢ 2 ^ (4 * n) * ↑n ! ^ 4 * ((2 * ↑n + 2) * (2 * ↑n + 2)) * (↑(2 * (n + 1))! ^ 2 * (2 * ↑(n + 1) + 1)) =
    2 ^ (4 * (n + 1)) * ↑(n + 1)! ^ 4 * (↑(2 * n)! ^ 2 * (2 * ↑n + 1) * ((2 * ↑n + 1) * (2 * ↑n + 3)))

Tactic:
exact ne_of_gt (by positivity)

Goal state after:
case succ.refine_3
n : ℕ
IH :
  ∏ i ∈ range n, (2 * ↑i + 2) / (2 * ↑i + 1) * ((2 * ↑i + 2) / (2 * ↑i + 3)) =
    2 ^ (4 * n) * ↑n ! ^ 4 / (↑(2 * n)! ^ 2 * (2 * ↑n + 1))
⊢ 2 ^ (4 * n) * ↑n ! ^ 4 * ((2 * ↑n + 2) * (2 * ↑n + 2)) * (↑(2 * (n + 1))! ^ 2 * (2 * ↑(n + 1) + 1)) =
    2 ^ (4 * (n + 1)) * ↑(n + 1)! ^ 4 * (↑(2 * n)! ^ 2 * (2 * ↑n + 1) * ((2 * ↑n + 1) * (2 * ↑n + 3)))
Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean

Goal state before:
pp: x y : ℝ≥0
h : x ≠ y
⊢ sqrt (x * y) < (x + y) / 2

Tactic:
wlog hl : y < x generalizing x y

Goal state after:
case inr
x y : ℝ≥0
h : x ≠ y
this : ∀ {x y : ℝ≥0}, x ≠ y → y < x → sqrt (x * y) < (x + y) / 2
hl : ¬y < x
⊢ sqrt (x * y) < (x + y) / 2

x y : ℝ≥0
h : x ≠ y
hl : y < x
⊢ sqrt (x * y) < (x + y) / 2
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arctan

Goal state before:
pp: case hx₁
z : ℂ
h₀ : z ≠ ↑π / 2
h₁ : -(π / 2) < z.re
h₂ : z.re ≤ π / 2
h : cos z ≠ 0
⊢ -π < 2 * z.re

Tactic:
← div_lt_iff₀' two_pos,

Goal state after:
case hx₁
z : ℂ
h₀ : z ≠ ↑π / 2
h₁ : -(π / 2) < z.re
h₂ : z.re ≤ π / 2
h : cos z ≠ 0
⊢ -π / 2 < z.re
Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean

Goal state before:
pp: x : ℝ≥0
⊢ x.agm x = x

Tactic:
apply le_antisymm
  · nth_rw 3 [← max_self x]
    exact agm_le_max
  · nth_rw 1 [← min_self x]
    exact min_le_agm

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

Goal state before:
pp: x : ℝ
h : 0 < (1 + tanh x) / (1 - tanh x)
⊢ (1 + tanh x) / (1 - tanh x) = rexp x ^ 2

Tactic:
tanh_eq,

Goal state after:
x : ℝ
h : 0 < (1 + tanh x) / (1 - tanh x)
⊢ (1 + (rexp x - rexp (-x)) / (rexp x + rexp (-x))) / (1 - (rexp x - rexp (-x)) / (rexp x + rexp (-x))) = rexp x ^ 2
Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy

Goal state before:
pp: p : ℝ
⊢ binEntropy (2⁻¹ + p) = binEntropy (2⁻¹ - p)

Tactic:
rw [← binEntropy_one_sub]

Goal state after:
p : ℝ
⊢ binEntropy (1 - (2⁻¹ + p)) = binEntropy (2⁻¹ - p)
Module: Mathlib.Analysis.SpecialFunctions.Choose

Goal state before:
pp: k : ℕ
⊢ (fun n ↦ ↑(n.descFactorial k) / ↑k !) ~[atTop] fun n ↦ ↑n ^ k / ↑k !

Tactic:
exact (isEquivalent_descFactorial k).div IsEquivalent.refl

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

Goal state before:
pp: k : ℕ
⊢ (fun n ↦ ↑(n.choose k)) =Θ[atTop] fun n ↦ ↑n ^ k

Tactic:
by
  apply (isEquivalent_choose k).trans_isTheta
  simp_rw [div_eq_mul_inv, mul_comm _ (_⁻¹)]
  exact isTheta_rfl.const_mul_left <| inv_ne_zero (mod_cast k.factorial_ne_zero)

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

Goal state before:
pp: p : ℝ
hp : 1 < p
⊢ binEntropy p < 0

Tactic:
rw [← binEntropy_one_sub]

Goal state after:
p : ℝ
hp : 1 < p
⊢ binEntropy (1 - p) < 0
Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy

Goal state before:
pp: p : ℝ
hp : 1 ≤ p
⊢ binEntropy p ≤ 0

Tactic:
rw [← binEntropy_one_sub]

Goal state after:
p : ℝ
hp : 1 ≤ p
⊢ binEntropy (1 - p) ≤ 0
Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy

Goal state before:
pp: case refine_2.inr
p : ℝ
h : p ≠ 2⁻¹
this : ∀ {p : ℝ}, p ≠ 2⁻¹ → p < 2⁻¹ → binEntropy p < log 2
hp✝ : ¬p < 2⁻¹
hp : 1 - p < 2⁻¹
⊢ binEntropy p < log 2

Tactic:
rw [← binEntropy_one_sub]

Goal state after:
case refine_2.inr
p : ℝ
h : p ≠ 2⁻¹
this : ∀ {p : ℝ}, p ≠ 2⁻¹ → p < 2⁻¹ → binEntropy p < log 2
hp✝ : ¬p < 2⁻¹
hp : 1 - p < 2⁻¹
⊢ binEntropy (1 - p) < log 2
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 ∈ Ioo 0 1
μ : Measure ℝ
hμ :
  ∀ a ∈ Ici 0,
    IntegrableOn (fun t ↦ cfcₙ ((↑p).rpowIntegrand₀₁ t) a) (Ioi 0) μ ∧
      a ^ p = ∫ (t : ℝ) in Ioi 0, cfcₙ ((↑p).rpowIntegrand₀₁ t) a ∂μ
h₃' : EqOn (fun a ↦ a ^ p) (fun a ↦ ∫ (t : ℝ) in Ioi 0, cfcₙ ((↑p).rpowIntegrand₀₁ t) a ∂μ) (Ici 0)
⊢ MonotoneOn (fun a ↦ a ^ p) (Ici 0)

Tactic:
refine MonotoneOn.congr ?_ h₃'.symm

Goal state after:
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
p : ℝ≥0
hp : p ∈ Ioo 0 1
μ : Measure ℝ
hμ :
  ∀ a ∈ Ici 0,
    IntegrableOn (fun t ↦ cfcₙ ((↑p).rpowIntegrand₀₁ t) a) (Ioi 0) μ ∧
      a ^ p = ∫ (t : ℝ) in Ioi 0, cfcₙ ((↑p).rpowIntegrand₀₁ t) a ∂μ
h₃' : EqOn (fun a ↦ a ^ p) (fun a ↦ ∫ (t : ℝ) in Ioi 0, cfcₙ ((↑p).rpowIntegrand₀₁ t) a ∂μ) (Ici 0)
⊢ MonotoneOn (fun a ↦ ∫ (t : ℝ) in Ioi 0, cfcₙ ((↑p).rpowIntegrand₀₁ t) a ∂μ) (Ici 0)
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog.Order

Goal state before:
pp: case tendsto
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : A
ha : IsStrictlyPositive a
⊢ TendstoUniformlyOn (fun p x ↦ p⁻¹ * (x ^ p - 1)) Real.log (𝓝[>] 0) (spectrum ℝ a)

pp: case cont
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : A
ha : IsStrictlyPositive a
⊢ ∀ᶠ (x : ℝ) in 𝓝[>] 0, ContinuousOn (fun x_1 ↦ x⁻¹ * (x_1 ^ x - 1)) (spectrum ℝ a)

Tactic:
case cont =>
    exact .of_forall fun p ↦ by fun_prop (disch := grind -abstractProof)

Goal state after:
case tendsto
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : A
ha : IsStrictlyPositive a
⊢ TendstoUniformlyOn (fun p x ↦ p⁻¹ * (x ^ p - 1)) Real.log (𝓝[>] 0) (spectrum ℝ a)
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) / (t * (t + x))) = t ^ p / t * x / (t + x)

Tactic:
simp [field]

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

Goal state before:
pp: this : eulerMascheroniSeq 6 = 49 / 20 - log 7
⊢ 7 < ∑ i ∈ Finset.range 7, (49 / 20 - 1 / 2) ^ i / ↑i.factorial

Tactic:
Finset.sum_range_succ,

Goal state after:
this : eulerMascheroniSeq 6 = 49 / 20 - log 7
⊢ 7 <
    ∑ i ∈ Finset.range 0, (49 / 20 - 1 / 2) ^ i / ↑i.factorial + (49 / 20 - 1 / 2) ^ 0 / ↑(Nat.factorial 0) +
                (49 / 20 - 1 / 2) ^ 1 / ↑(Nat.factorial 1) +
              (49 / 20 - 1 / 2) ^ 2 / ↑(Nat.factorial 2) +
            (49 / 20 - 1 / 2) ^ 3 / ↑(Nat.factorial 3) +
          (49 / 20 - 1 / 2) ^ 4 / ↑(Nat.factorial 4) +
        (49 / 20 - 1 / 2) ^ 5 / ↑(Nat.factorial 5) +
      (49 / 20 - 1 / 2) ^ 6 / ↑(Nat.factorial 6)
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation

Goal state before:
pp: case finitebound
p x : ℝ
hp : p ∈ Ioo 0 1
hx : 0 ≤ x
⊢ HasFiniteIntegral (fun t ↦ t ^ (p - 2) * x) (volume.restrict (Ioi 1))

pp: case ae_le
p x : ℝ
hp : p ∈ Ioo 0 1
hx : 0 ≤ x
⊢ ∀ᵐ (a : ℝ) ∂volume.restrict (Ioi 1), ‖p.rpowIntegrand₀₁ a x‖ ≤ a ^ (p - 2) * x

Tactic:
case finitebound =>
      refine HasFiniteIntegral.mul_const ?_ _
      apply Integrable.hasFiniteIntegral
      rw [Set.mem_Ioo] at hp
      refine integrableOn_Ioi_rpow_of_lt ?_ zero_lt_one
      linarith

Goal state after:
case ae_le
p x : ℝ
hp : p ∈ Ioo 0 1
hx : 0 ≤ x
⊢ ∀ᵐ (a : ℝ) ∂volume.restrict (Ioi 1), ‖p.rpowIntegrand₀₁ a x‖ ≤ a ^ (p - 2) * x
Module: Mathlib.NumberTheory.Harmonic.EulerMascheroni

Goal state before:
pp: case inr.refine_2
n : ℕ
hn : n > 0
⊢ (↑(n + 1) / ↑n)⁻¹ ≠ 1

Tactic:
simp [field]

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

Goal state before:
pp: case inr.refine_3
n : ℕ
hn : n > 0
⊢ (↑(n + 1) / ↑n)⁻¹ - 1 = -↑(↑(n + 1))⁻¹

Tactic:
simp [field]

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

Goal state before:
pp: s : ℂ
⊢ ↑π ^ ((s - 1) / 2 + (-1 - s) / 2 + 1) / sin (↑π / 2 - ↑π * s / 2) = (cos (↑π * s / 2))⁻¹

Tactic:
Complex.sin_pi_div_two_sub

Goal state after:
s : ℂ
⊢ ↑π ^ ((s - 1) / 2 + (-1 - s) / 2 + 1) / cos (↑π * s / 2) = (cos (↑π * s / 2))⁻¹
Module: Mathlib.Data.Int.Log

Goal state before:
pp: case inl.inl
R : Type u_1
inst✝³ : Semifield R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorSemiring R
b : ℕ
r₁ r₂ : R
h₀ : 0 < r₁
h : r₁ ≤ r₂
h₁ : r₁ ≤ 1
h₂ : r₂ ≤ 1
h₀' : 0 < r₂
⊢ log b r₁ ≤ log b r₂

Tactic:
rw [log_of_right_le_one _ h₁, log_of_right_le_one _ h₂, neg_le_neg_iff, Nat.cast_le]

Goal state after:
case inl.inl
R : Type u_1
inst✝³ : Semifield R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorSemiring R
b : ℕ
r₁ r₂ : R
h₀ : 0 < r₁
h : r₁ ≤ r₂
h₁ : r₁ ≤ 1
h₂ : r₂ ≤ 1
h₀' : 0 < r₂
⊢ Nat.clog b ⌈r₂⁻¹⌉₊ ≤ Nat.clog b ⌈r₁⁻¹⌉₊
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
A : Set α
hA : IsClosed A
r : ℝ≥0∞
hr : r < μ A
K : Set α
hK1 : K ⊆ A
hK2 : IsCompact K
hK3 : r < μ K
⊢ ∃ K ⊆ A, (IsCompact ∘ closure) K ∧ r < μ K

Tactic:
refine ⟨closure K, closure_minimal hK1 hA, ?_, ?_⟩

Goal state after:
case mpr.refine_1
α : Type u_1
inst✝² : MeasurableSpace α
μ : Measure α
inst✝¹ : TopologicalSpace α
inst✝ : R1Space α
h : μ.InnerRegularWRT IsCompact IsClosed
A : Set α
hA : IsClosed A
r : ℝ≥0∞
hr : r < μ A
K : Set α
hK1 : K ⊆ A
hK2 : IsCompact K
hK3 : r < μ K
⊢ (IsCompact ∘ closure) (closure K)

case mpr.refine_2
α : Type u_1
inst✝² : MeasurableSpace α
μ : Measure α
inst✝¹ : TopologicalSpace α
inst✝ : R1Space α
h : μ.InnerRegularWRT IsCompact IsClosed
A : Set α
hA : IsClosed A
r : ℝ≥0∞
hr : r < μ A
K : Set α
hK1 : K ⊆ A
hK2 : IsCompact K
hK3 : r < μ K
⊢ r < μ (closure 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
A : Set α
hA : IsClosed A
r : ℝ≥0∞
hr : r < μ A
K : Set α
hK1 : K ⊆ A
hK2 : (IsCompact ∘ closure) K
hK3 : r < μ K
⊢ ∃ K ⊆ A, (fun s ↦ IsCompact s ∧ IsClosed s) K ∧ r < μ K

Tactic:
refine ⟨closure K, closure_minimal hK1 hA, ?_, ?_⟩

Goal state after:
case mpr.refine_1
α : Type u_1
inst✝² : MeasurableSpace α
μ : Measure α
inst✝¹ : TopologicalSpace α
inst✝ : R1Space α
h : μ.InnerRegularWRT (IsCompact ∘ closure) IsClosed
A : Set α
hA : IsClosed A
r : ℝ≥0∞
hr : r < μ A
K : Set α
hK1 : K ⊆ A
hK2 : (IsCompact ∘ closure) K
hK3 : r < μ K
⊢ (fun s ↦ IsCompact s ∧ IsClosed s) (closure K)

case mpr.refine_2
α : Type u_1
inst✝² : MeasurableSpace α
μ : Measure α
inst✝¹ : TopologicalSpace α
inst✝ : R1Space α
h : μ.InnerRegularWRT (IsCompact ∘ closure) IsClosed
A : Set α
hA : IsClosed A
r : ℝ≥0∞
hr : r < μ A
K : Set α
hK1 : K ⊆ A
hK2 : (IsCompact ∘ closure) K
hK3 : r < μ K
⊢ r < μ (closure K)
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
g : E →ᵇ ℝ
⊢ ∀ (x : ℕ → ℝ),
    Tendsto x atTop (𝓝[>] 0) →
      Tendsto ((fun ε ↦ ∫ (x : E), ε.mulExpNegMulSq (g x) ∂P) ∘ x) atTop (𝓝 (∫ (x : E), g x ∂P))

Tactic:
intro u hu

Goal state after:
E : Type u_1
inst✝³ : TopologicalSpace E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
P : Measure E
inst✝ : IsFiniteMeasure P
g : E →ᵇ ℝ
u : ℕ → ℝ
hu : Tendsto u atTop (𝓝[>] 0)
⊢ Tendsto ((fun ε ↦ ∫ (x : E), ε.mulExpNegMulSq (g x) ∂P) ∘ u) atTop (𝓝 (∫ (x : E), g x ∂P))
Module: Mathlib.Analysis.SpecialFunctions.Pochhammer

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

Tactic:
simp [monotoneOn_const]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Pow.Integral

Goal state before:
pp: case e_f
α : 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 * ENNReal.ofReal (f ω ^ p / p)

Tactic:
rw [← ENNReal.ofReal_mul p_pos.le, mul_div_cancel₀ (f ω ^ p) p_pos.ne.symm]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Pow.NthRootLemmas

Goal state before:
pp: n a b : ℕ
hb : b ≠ 0
c : ℕ
hc1 : c ^ (n + 1) ≤ a
hc2 : a < (c + 1) ^ (n + 1)
⊢ a < ((a / b ^ n + n * b) / (n + 1) + 1) ^ (n + 1)

Tactic:
calc a < (c + 1) ^ (n + 1) := hc2
    _ ≤ ((c ^ (n + 1) / b ^ n + n * b) / (n + 1) + 1) ^ (n + 1) := by
      gcongr
      exact nthRoot.lt_pow_go_succ_aux0 hb
    _ ≤ ((a / b ^ n + n * b) / (n + 1) + 1) ^ (n + 1) := by
      gcongr

Goal state after:
Module: Mathlib.MeasureTheory.Constructions.Polish.EmbeddingReal

Goal state before:
pp: case pos.inl
α : Type u_1
inst✝¹ : MeasurableSpace α
inst✝ : StandardBorelSpace α
hα : Countable α
h✝ : Finite α
n : ℕ
h_nonempty_equiv : Nonempty (α ≃ᵐ ↑(range fun x ↦ ↑↑x))
⊢ MeasurableSet (range fun x ↦ ↑↑x)

Tactic:
exact (Set.finite_range ((↑) : Fin n → ℝ)).measurableSet

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

Goal state before:
pp: L : PeriodPair
z✝ : ℂ
l : ↥L.lattice
z : ℂ
hz : z ∈ {z | (fun x ↦ ℘[L] (x + z)) = ℘[L]}
i : ℂ
| ℘[L] (i + -z)

Tactic:
rw [← hz]

Goal state after:
L : PeriodPair
z✝ : ℂ
l : ↥L.lattice
z : ℂ
hz : z ∈ {z | (fun x ↦ ℘[L] (x + z)) = ℘[L]}
i : ℂ
| (fun x ↦ ℘[L] (x + z)) (i + -z)
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: L : PeriodPair
⊢ ℘[L] 0 = 0

Tactic:
simp [weierstrassP]

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

Goal state before:
pp: L : PeriodPair
⊢ HasSumLocallyUniformly (fun l z ↦ -2 / (z - ↑l) ^ 3) ℘'[L]

Tactic:
convert! L.hasSumLocallyUniformly_derivWeierstrassPExcept (L.ω₁ / 2) using 3 with l z
  · rw [if_neg, neg_div]; exact fun e ↦ L.ω₁_div_two_notMem_lattice (e ▸ l.2)
  · rw [L.derivWeierstrassPExcept_of_notMem _ L.ω₁_div_two_notMem_lattice]

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

Goal state before:
pp: case pos
L : PeriodPair
x : ℂ
hx : x ∈ L.lattice
⊢ 0 = ℘'[L] x

pp: case pos
L : PeriodPair
x : ℂ
hx : x ∈ L.lattice
⊢ ¬DifferentiableAt ℂ ℘[L] x

Tactic:
L.derivWeierstrassP_coe ⟨x, hx⟩

Goal state after:
case pos
L : PeriodPair
x : ℂ
hx : x ∈ L.lattice
⊢ 0 = 0

case pos
L : PeriodPair
x : ℂ
hx : x ∈ L.lattice
⊢ ¬DifferentiableAt ℂ ℘[L] x
Module: Mathlib.Analysis.SpecialFunctions.Stirling

Goal state before:
pp: case zero
⊢ 1 / (12 * ↑0 * (↑0 + 1)) ≤ 1 / (4 * ↑0 ^ 2)

Tactic:
simp [field]

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

Goal state before:
pp: case succ
n✝ : ℕ
⊢ 1 / (12 * ↑(n✝ + 1) * (↑(n✝ + 1) + 1)) ≤ 1 / (4 * ↑(n✝ + 1) ^ 2)

Tactic:
simp [field]

Goal state after:
case succ
n✝ : ℕ
⊢ (↑n✝ + 1) * 4 ≤ (↑n✝ + 1 + 1) * 12
Module: Mathlib.Analysis.SpecialFunctions.Stirling

Goal state before:
pp: n : ℕ
f : ℕ → ℝ := fun k ↦ log (stirlingSeq (k + 1))
g : ℕ → ℝ := fun k ↦ 1 / (12 * (↑k + 1))
k : ℕ
hk : k ∈ range n
⊢ 1 / (12 * ↑(k + 1) * (↑(k + 1) + 1)) ≤ g k - g (k + 1)

Tactic:
simp [field]

Goal state after:
Module: Mathlib.NumberTheory.Niven

Goal state before:
pp: case left
r : ℚ
hcos : ∃ q, cos (↑r * π) = ↑q
k : ℤ
hk : 2 * cos (↑r * π) = ↑k
⊢ -2 ≤ ↑k

Tactic:
linarith [hk, (r * π).neg_one_le_cos, (r * π).cos_le_one]

Goal state after:
Module: Mathlib.NumberTheory.Niven

Goal state before:
pp: case right
r : ℚ
hcos : ∃ q, cos (↑r * π) = ↑q
k : ℤ
hk : 2 * cos (↑r * π) = ↑k
⊢ ↑k ≤ 2

Tactic:
linarith [hk, (r * π).neg_one_le_cos, (r * π).cos_le_one]

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

Goal state before:
pp: n : ℕ
c : ℕ → ℝ
hcpos : ∀ i ≤ n, 0 < (-1) ^ i * c i
P : ℝ[X]
hPdeg : P.degree ≤ ↑n
hPbnd : ∀ x ∈ Set.Icc (-1) 1, |eval x P| ≤ 1
h : sumNodes n c P = sumNodes n c (T ℝ ↑n)
⊢ P = T ℝ ↑n

Tactic:
rw [sumNodes, sumNodes] at h

Goal state after:
n : ℕ
c : ℕ → ℝ
hcpos : ∀ i ≤ n, 0 < (-1) ^ i * c i
P : ℝ[X]
hPdeg : P.degree ≤ ↑n
hPbnd : ∀ x ∈ Set.Icc (-1) 1, |eval x P| ≤ 1
h : ∑ i ≤ n, eval (node n i) P * c i = ∑ i ≤ n, eval (node n i) (T ℝ ↑n) * c i
⊢ P = T ℝ ↑n
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable

Goal state before:
pp: z : ℍ
c d : ℝ
hc : 1 ≤ c ^ 2
⊢ r z ≤ ‖↑c * ↑z + ↑d‖

Tactic:
rcases z with ⟨z, hz⟩

Goal state after:
c d : ℝ
hc : 1 ≤ c ^ 2
z : ℂ
hz : 0 < z.im
⊢ r { coe := z, coe_im_pos := hz } ≤ ‖↑c * ↑{ coe := z, coe_im_pos := hz } + ↑d‖