mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Real.Pi.Irrational

Goal state before:
pp: θ : ℝ
n : ℕ
⊢ I (n + 2) θ * θ ^ 2 = 2 * (↑n + 2) * (2 * ↑n + 3) * I (n + 1) θ - 4 * (↑n + 2) * (↑n + 1) * I n θ

Tactic:
rw [recursion' (n + 1)]

Goal state after:
θ : ℝ
n : ℕ
⊢ -(2 * 2 * ((↑(n + 1) + 1) * (0 ^ (n + 1) * cos θ))) + 2 * (↑(n + 1) + 1) * (2 * ↑(n + 1) + 1) * I (n + 1) θ -
      4 * (↑(n + 1) + 1) * ↑(n + 1) * I (n + 1 - 1) θ =
    2 * (↑n + 2) * (2 * ↑n + 3) * I (n + 1) θ - 4 * (↑n + 2) * (↑n + 1) * I n θ
Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy

Goal state before:
pp: q : ℕ
qLe2 : 2 ≤ q
p1 : ℝ
hp1 : p1 ∈ Icc 0 (1 - 1 / ↑q)
p2 : ℝ
hp2 : p2 ∈ Icc 0 (1 - 1 / ↑q)
p1le2 : p1 < p2
p : ℝ
this✝ : 2 ≤ ↑q
zero_le_qinv : 0 < (↑q)⁻¹
this : 0 < 1 - p
hp : 0 < p ∧ p < 1 - (↑q)⁻¹
⊢ 0 < log (↑q - 1) + log (1 - p) - log p

pp: q : ℕ
qLe2 : 2 ≤ q
p1 : ℝ
hp1 : p1 ∈ Icc 0 (1 - 1 / ↑q)
p2 : ℝ
hp2 : p2 ∈ Icc 0 (1 - 1 / ↑q)
p1le2 : p1 < p2
p : ℝ
this✝ : 2 ≤ ↑q
zero_le_qinv : 0 < (↑q)⁻¹
this : 0 < 1 - p
hp : 0 < p ∧ p < 1 - (↑q)⁻¹
⊢ p ≠ 1

Tactic:
· simp only [sub_pos, gt_iff_lt]
      rw [← log_mul (by linarith) (by linarith)]
      apply Real.strictMonoOn_log (mem_Ioi.mpr hp.1)
      · simp_all only [mem_Ioi, mul_pos_iff_of_pos_left, show 0 < (q : ℝ) - 1 by linarith]
      · have qpos : 0 < (q : ℝ) := by positivity
        have : q * p < q - 1 := by
          convert! mul_lt_mul_of_pos_left hp.2 qpos using 1
          simp only [mul_sub, mul_one, isUnit_iff_ne_zero, ne_eq, ne_of_gt qpos, not_false_eq_true,
            IsUnit.mul_inv_cancel]
        linarith

Goal state after:
q : ℕ
qLe2 : 2 ≤ q
p1 : ℝ
hp1 : p1 ∈ Icc 0 (1 - 1 / ↑q)
p2 : ℝ
hp2 : p2 ∈ Icc 0 (1 - 1 / ↑q)
p1le2 : p1 < p2
p : ℝ
this✝ : 2 ≤ ↑q
zero_le_qinv : 0 < (↑q)⁻¹
this : 0 < 1 - p
hp : 0 < p ∧ p < 1 - (↑q)⁻¹
⊢ p ≠ 1
Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy

Goal state before:
pp: case x
q : ℕ
qLe2 : 2 ≤ q
p1 : ℝ
hp1 : p1 ∈ Icc (1 - 1 / ↑q) 1
p2 : ℝ
hp2 : p2 ∈ Icc (1 - 1 / ↑q) 1
p1le2 : p1 < p2
p : ℝ
this : 2 ≤ ↑q
qinv_lt_1 : (↑q)⁻¹ < 1
zero_lt_1_sub_p : 0 < 1 - p
hp : 1 - (↑q)⁻¹ < p ∧ p < 1
⊢ p ∈ Ioi 0

Tactic:
simp_all only [mem_Ioi]
        linarith

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

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

Tactic:
obtain (hp | hp) | hp := hp

Goal state after:
case pos.inl.inl
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
p : ℝ≥0
a b : A
hab : a ≤ b
ha : 0 ≤ a
hb : 0 ≤ b
hIcc : Icc 0 1 = Ioo 0 1 ∪ {0} ∪ {1}
hp : p ∈ Ioo 0 1
⊢ (fun a ↦ a ^ p) a ≤ (fun a ↦ a ^ p) b

case pos.inl.inr
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
p : ℝ≥0
a b : A
hab : a ≤ b
ha : 0 ≤ a
hb : 0 ≤ b
hIcc : Icc 0 1 = Ioo 0 1 ∪ {0} ∪ {1}
hp : p ∈ {0}
⊢ (fun a ↦ a ^ p) a ≤ (fun a ↦ a ^ p) b

case pos.inr
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
p : ℝ≥0
a b : A
hab : a ≤ b
ha : 0 ≤ a
hb : 0 ≤ b
hIcc : Icc 0 1 = Ioo 0 1 ∪ {0} ∪ {1}
hp : p ∈ {1}
⊢ (fun a ↦ a ^ p) a ≤ (fun a ↦ a ^ p) b
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Order

Goal state before:
pp: case pos.inl.inl
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
p : ℝ≥0
a b : A
hab : a ≤ b
ha : 0 ≤ a
hb : 0 ≤ b
hIcc : Icc 0 1 = Ioo 0 1 ∪ {0} ∪ {1}
hp : p ∈ Ioo 0 1
⊢ (fun a ↦ a ^ p) a ≤ (fun a ↦ a ^ p) b

Tactic:
exact monotoneOn_nnrpow_Ioo hp ha hb hab

Goal state after:
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 ∪ {0} ∪ {1}
hIcc : Icc 0 1 = Ioo 0 1 ∪ {0} ∪ {1}
⊢ ConcaveOn ℝ (Ici 0) fun a ↦ a ^ p

Tactic:
obtain (hp | hp) | hp := hp

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

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

case inr
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
p : ℝ≥0
hIcc : Icc 0 1 = Ioo 0 1 ∪ {0} ∪ {1}
hp : p ∈ {1}
⊢ ConcaveOn ℝ (Ici 0) fun a ↦ a ^ p
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog.Order

Goal state before:
pp: A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : A
ha : IsStrictlyPositive a
s : Set A := {a | IsStrictlyPositive a}
f : ℝ → ℝ → ℝ := fun p x ↦ if p > 0 then p⁻¹ * (x ^ p - 1) else Real.log x
hmain : TendstoLocallyUniformlyOn (fun p x ↦ p⁻¹ * (x ^ p - 1)) Real.log (𝓝[>] 0) (Set.Ioi 0)
⊢ TendstoUniformlyOn (fun p x ↦ p⁻¹ * (x ^ p - 1)) Real.log (𝓝[>] 0) (spectrum ℝ a)

Tactic:
rw [tendstoLocallyUniformlyOn_iff_forall_isCompact isOpen_Ioi] at hmain

Goal state after:
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : A
ha : IsStrictlyPositive a
s : Set A := {a | IsStrictlyPositive a}
f : ℝ → ℝ → ℝ := fun p x ↦ if p > 0 then p⁻¹ * (x ^ p - 1) else Real.log x
hmain : ∀ K ⊆ Set.Ioi 0, IsCompact K → TendstoUniformlyOn (fun p x ↦ p⁻¹ * (x ^ p - 1)) Real.log (𝓝[>] 0) K
⊢ TendstoUniformlyOn (fun p x ↦ p⁻¹ * (x ^ p - 1)) Real.log (𝓝[>] 0) (spectrum ℝ a)
Module: Mathlib.Analysis.SpecialFunctions.FrullaniIntegral

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

Tactic:
by rw [abs_of_nonneg hδ]

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

Goal state before:
pp: case pos
p t x : ℝ
hp : p ∈ Ioo 0 1
ht : 0 ≤ t
hx : 0 ≤ x
ht' : t = 0
⊢ p.rpowIntegrand₀₁ t x = t ^ (p - 1) * x / (t + x)

Tactic:
case pos =>
    push _ ∈ _ at hp
    have hp₂ : p - 1 ≠ 0 := by linarith
    simp [rpowIntegrand₀₁, ht', hp.1.ne', hp₂]

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

Goal state before:
pp: p x : ℝ
hp : p ∈ Ioo 0 1
hx : 0 ≤ x
t : ℝ
ht : t ∈ Ioi 0
⊢ (fun x_1 ↦ p.rpowIntegrand₀₁ x_1 x) t = (fun t ↦ t ^ (p - 1) * x / (t + x)) t

Tactic:
simp [rpowIntegrand₀₁_eq_pow_div hp (le_of_lt ht) hx]

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

Goal state before:
pp: h1 : eulerMascheroniSeq' 6 = 49 / 20 - log 6
⊢ eulerMascheroniSeq' 6 < 2 / 3

Tactic:
h1,

Goal state after:
h1 : eulerMascheroniSeq' 6 = 49 / 20 - log 6
⊢ 49 / 20 - log 6 < 2 / 3
Module: Mathlib.NumberTheory.Harmonic.EulerMascheroni

Goal state before:
pp: n : ℕ
⊢ eulerMascheroniConstant < eulerMascheroniSeq' n

Tactic:
by
  refine lt_of_le_of_lt ?_ (strictAnti_eulerMascheroniSeq' (Nat.lt_succ_self n))
  apply strictAnti_eulerMascheroniSeq'.antitone.le_of_tendsto tendsto_eulerMascheroniSeq'

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

Goal state before:
pp: case refine_1
p : ℝ
hp : p ∈ Ioo 0 1
C : ℝ≥0 := NNReal.mk (∫ (t : ℝ) in Ioi 0, p.rpowIntegrand₀₁ t 1)⁻¹ ⋯
x : ℝ
hx : x ∈ Ici 0
⊢ Integrable (fun t ↦ p.rpowIntegrand₀₁ t x) ((C • volume).restrict (Ioi 0))

Tactic:
Measure.restrict_smul

Goal state after:
case refine_1
p : ℝ
hp : p ∈ Ioo 0 1
C : ℝ≥0 := NNReal.mk (∫ (t : ℝ) in Ioi 0, p.rpowIntegrand₀₁ t 1)⁻¹ ⋯
x : ℝ
hx : x ∈ Ici 0
⊢ Integrable (fun t ↦ p.rpowIntegrand₀₁ t x) (C • volume.restrict (Ioi 0))
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation

Goal state before:
pp: case refine_1
p : ℝ
hp : p ∈ Ioo 1 2
C : ℝ≥0 := NNReal.mk (∫ (t : ℝ) in Ioi 0, (p - 1).rpowIntegrand₀₁ t 1)⁻¹ ⋯
μ : Measure ℝ := C • volume
x : ℝ
hx : x ∈ Ici 0
⊢ Integrable (fun t ↦ p.rpowIntegrand₁₂ t x) ((C • volume).restrict (Ioi 0))

Tactic:
Measure.restrict_smul

Goal state after:
case refine_1
p : ℝ
hp : p ∈ Ioo 1 2
C : ℝ≥0 := NNReal.mk (∫ (t : ℝ) in Ioi 0, (p - 1).rpowIntegrand₀₁ t 1)⁻¹ ⋯
μ : Measure ℝ := C • volume
x : ℝ
hx : x ∈ Ici 0
⊢ Integrable (fun t ↦ p.rpowIntegrand₁₂ t x) (C • volume.restrict (Ioi 0))
Module: Mathlib.NumberTheory.Harmonic.GammaDeriv

Goal state before:
pp: ⊢ HasDerivAt Gammaℂ (-(↑γ + log (2 * ↑π)) / ↑π) 1

Tactic:
let f (s : ℂ) : ℂ := 2 * (2 * π) ^ (-s)
  have : HasDerivAt (fun s : ℂ ↦ 2 * (2 * π : ℂ) ^ (-s)) (-log (2 * π) / π) 1 := by
    have := (hasDerivAt_neg' (1 : ℂ)).const_cpow (c := 2 * π)
      (Or.inl (by exact_mod_cast Real.two_pi_pos.ne'))
    refine (this.const_mul 2).congr_deriv ?_
    rw [mul_neg_one, mul_neg, cpow_neg_one, ← div_eq_inv_mul, ← mul_div_assoc,
      mul_div_mul_left _ _ two_ne_zero, neg_div]
  have := this.mul hasDerivAt_Gamma_one
  rwa [Gamma_one, mul_one, cpow_neg_one, ← div_eq_mul_inv, ← div_div, div_self two_ne_zero,
    mul_comm (1 / _), mul_one_div, ← _root_.add_div, ← neg_add, add_comm] at this

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

Goal state before:
pp: f : ℂ → ℂ := fun s ↦ ↑π ^ (-s / 2)
g : ℂ → ℂ := fun s ↦ Gamma (s / 2)
aux : ↑π ^ (1 / 2) = ↑√π
aux2 : ↑√π ≠ 0
hf : HasDerivAt f (-log ↑π / 2 / ↑√π) 1
hg : HasDerivAt g (-↑√π * (↑γ + 2 * log 2) / 2) 1
⊢ -(↑γ + (↑2 * ↑(Real.log 2) + ↑(Real.log π))) / ↑2 = -(↑γ + log (4 * ↑π)) / ↑2

Tactic:
← ofReal_mul,

Goal state after:
f : ℂ → ℂ := fun s ↦ ↑π ^ (-s / 2)
g : ℂ → ℂ := fun s ↦ Gamma (s / 2)
aux : ↑π ^ (1 / 2) = ↑√π
aux2 : ↑√π ≠ 0
hf : HasDerivAt f (-log ↑π / 2 / ↑√π) 1
hg : HasDerivAt g (-↑√π * (↑γ + 2 * log 2) / 2) 1
⊢ -(↑γ + (↑(2 * Real.log 2) + ↑(Real.log π))) / ↑2 = -(↑γ + log (4 * ↑π)) / ↑2
Module: Mathlib.Analysis.SpecialFunctions.Log.Base

Goal state before:
pp: b x y : ℝ
hx : x ≠ 0
hy : y ≠ 0
⊢ (log x - log y) / log b = log x / log b - log y / log b

Tactic:
sub_div

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

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

Tactic:
inv_lt_comm₀ _ hr

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

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

Goal state before:
pp: X : Type u_1
inst✝⁸ : MeasurableSpace X
inst✝⁷ : TopologicalSpace X
μ : Measure X
E : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : OpensMeasurableSpace X
inst✝⁴ : SecondCountableTopology E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : NormedSpace ℝ E
inst✝ : IsFiniteMeasure μ
f : X →ᵇ E
⊢ ‖∫ (x : X), f x ∂μ‖ ≤ μ.real Set.univ * ‖f‖

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

Goal state after:
X : Type u_1
inst✝⁸ : MeasurableSpace X
inst✝⁷ : TopologicalSpace X
μ : Measure X
E : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : OpensMeasurableSpace X
inst✝⁴ : SecondCountableTopology E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : NormedSpace ℝ E
inst✝ : IsFiniteMeasure μ
f : X →ᵇ E
⊢ ∫ (x : X), ‖f x‖ ∂μ ≤ ∫ (x : X), ‖f‖ ∂μ
Module: Mathlib.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ᶜ < ε
⊢ μ.InnerRegularWRT p q

Tactic:
by
  intro A hA r hr
  obtain ⟨K, hK, hK_subset, h_lt⟩ : ∃ K, p K ∧ K ⊆ A ∧ μ (A \ K) < μ A - r := 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]
  refine ⟨K, hK_subset, hK, ?_⟩
  have h_lt' : μ A - μ K < μ A - r := le_measure_sdiff.trans_lt h_lt
  exact lt_of_tsub_lt_tsub_left h_lt'

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

Goal state before:
pp: case h_meas
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)
N : ℕ
hupos : ∀ (b : ℕ), N ≤ b → u b ∈ Set.Ioi 0
⊢ ∀ᶠ (n : ℕ) in atTop, AEStronglyMeasurable (fun ω ↦ (u n).mulExpNegMulSq (g ω)) P

pp: case h_bound
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)
N : ℕ
hupos : ∀ (b : ℕ), N ≤ b → u b ∈ Set.Ioi 0
⊢ ∃ C, ∀ᶠ (n : ℕ) in atTop, ∀ᵐ (ω : E) ∂P, ‖(u n).mulExpNegMulSq (g ω)‖ ≤ C

pp: case h_lim
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)
N : ℕ
hupos : ∀ (b : ℕ), N ≤ b → u b ∈ Set.Ioi 0
⊢ ∀ᵐ (ω : E) ∂P, Tendsto (fun n ↦ (u n).mulExpNegMulSq (g ω)) atTop (𝓝 (g ω))

Tactic:
· exact Eventually.of_forall (fun n => g.continuous.mulExpNegMulSq.aestronglyMeasurable)

Goal state after:
case h_bound
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)
N : ℕ
hupos : ∀ (b : ℕ), N ≤ b → u b ∈ Set.Ioi 0
⊢ ∃ C, ∀ᶠ (n : ℕ) in atTop, ∀ᵐ (ω : E) ∂P, ‖(u n).mulExpNegMulSq (g ω)‖ ≤ C

case h_lim
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)
N : ℕ
hupos : ∀ (b : ℕ), N ≤ b → u b ∈ Set.Ioi 0
⊢ ∀ᵐ (ω : E) ∂P, Tendsto (fun n ↦ (u n).mulExpNegMulSq (g ω)) atTop (𝓝 (g ω))
Module: Mathlib.Analysis.SpecialFunctions.Pow.NthRootLemmas

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

Tactic:
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_1
a b : Multiset ℂ
n : ℕ
hb : ∀ k ∈ b, k ≠ -↑n
⊢ (fun x ↦ Polynomial.eval x (ascPochhammer ℂ (n + 1))) = fun i ↦ Polynomial.eval i (ascPochhammer ℂ n) * (i + ↑n)

Tactic:
ext j

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

Goal state before:
pp: a b : Multiset ℂ
n : ℕ
hb : ∀ k ∈ b, k ≠ -↑n
⊢ regularizedHGFunCoeff a b (n + 1) =
    (Multiset.map (fun i ↦ Polynomial.eval i (ascPochhammer ℂ n) * (i + ↑n)) a).prod /
      (↑n ! * (↑n + 1) * (Multiset.map (fun j ↦ Gamma (j + ↑n) * (j + ↑n)) b).prod)

Tactic:
by
    unfold regularizedHGFunCoeff
    congrm ((a.map ?_).prod / (?_ * Multiset.prod ?_))
    · ext j
      simp [ascPochhammer_succ_right]
    · rw [Nat.factorial_succ]
      grind
    · refine Multiset.map_congr rfl (fun j hj ↦ ?_)
      simp only [Nat.cast_add, Nat.cast_one, ← add_assoc]
      grind

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

Goal state before:
pp: case e_a
n : ℕ
a b : Multiset ℂ
hn : n ≠ 0
⊢ ↑n ^ ↑a.card = ↑n ^ ↑(b.card + 1) * ↑n ^ (↑a.card - ↑b.card - 1)

Tactic:
← zpow_add' (by left; norm_cast)

Goal state after:
case e_a
n : ℕ
a b : Multiset ℂ
hn : n ≠ 0
⊢ ↑n ^ ↑a.card = ↑n ^ (↑(b.card + 1) + (↑a.card - ↑b.card - 1))
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: case neg
L : PeriodPair
l₀ : ℂ
s : Finset ↥L.lattice
l : ℂ
hl : l ∈ (↑L.lattice \ {l₀})ᶜ
x : ↥L.lattice
hl₁ : ¬↑x = l₀
⊢ -2 / (l - ↑x) ^ 3 = deriv (fun x2 ↦ 1 / (x2 - ↑x) ^ 2 - 1 / ↑x ^ 2) l

Tactic:
have hl₁ : l - x ≠ 0 := fun e ↦ hl₁ (by
        obtain rfl := sub_eq_zero.mp e
        simpa using hl)

Goal state after:
case neg
L : PeriodPair
l₀ : ℂ
s : Finset ↥L.lattice
l : ℂ
hl : l ∈ (↑L.lattice \ {l₀})ᶜ
x : ↥L.lattice
hl₁✝ : ¬↑x = l₀
hl₁ : l - ↑x ≠ 0
⊢ -2 / (l - ↑x) ^ 3 = deriv (fun x2 ↦ 1 / (x2 - ↑x) ^ 2 - 1 / ↑x ^ 2) l
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: case neg
L : PeriodPair
l₀ : ℂ
s : Finset ↥L.lattice
l : ℂ
hl : l ∈ (↑L.lattice \ {l₀})ᶜ
x : ↥L.lattice
hxs : x ∈ s
hl₁ : ¬↑x = l₀
⊢ DifferentiableAt ℂ (fun x2 ↦ 1 / (x2 - ↑x) ^ 2 - 1 / ↑x ^ 2) l

Tactic:
have hl₁ : l - x ≠ 0 := fun e ↦ hl₁ (by
        obtain rfl := sub_eq_zero.mp e
        simpa using hl)

Goal state after:
case neg
L : PeriodPair
l₀ : ℂ
s : Finset ↥L.lattice
l : ℂ
hl : l ∈ (↑L.lattice \ {l₀})ᶜ
x : ↥L.lattice
hxs : x ∈ s
hl₁✝ : ¬↑x = l₀
hl₁ : l - ↑x ≠ 0
⊢ DifferentiableAt ℂ (fun x2 ↦ 1 / (x2 - ↑x) ^ 2 - 1 / ↑x ^ 2) l
Module: Mathlib.Analysis.SpecialFunctions.Stirling

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

Tactic:
replace hf := Finset.sum_le_sum hf

Goal state after:
n : ℕ
f : ℕ → ℝ := fun k ↦ log (stirlingSeq (k + 1))
g : ℕ → ℝ := fun k ↦ 1 / (12 * (↑k + 1))
hf : ∑ i ∈ range n, (f i - f (i + 1)) ≤ ∑ i ∈ range n, (g i - g (i + 1))
⊢ log (stirlingSeq 1) - log (stirlingSeq (n + 1)) ≤ 12⁻¹
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal

Goal state before:
pp: n i : ℕ
hi : i ∈ Finset.Iic n
⊢ eval (node n i) (T ℝ ↑n) = (-1) ^ i

Tactic:
by
  rcases eq_or_ne n 0 with rfl | hn
  · simp [show i = 0 by grind]
  have : (n : ℤ) * (i * π / n) = i * π := by norm_cast; field
  rw [node, T_real_cos, this, cos_nat_mul_pi]

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

Goal state before:
pp: x : Fin 2 → ℤ
⊢ ‖x‖ = ↑(max (x 0).natAbs (x 1).natAbs)

Tactic:
← coe_nnnorm,

Goal state after:
x : Fin 2 → ℤ
⊢ ↑‖x‖₊ = ↑(max (x 0).natAbs (x 1).natAbs)
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: case hasSum
L : PeriodPair
l₀ x : ℂ
r : NNReal
hr0 : 0 < r
hr : Metric.closedBall x ↑r ⊆ (↑L.lattice \ {l₀})ᶜ
z : ℂ
hz : ‖z‖ < ↑r
this :
  (∀ (l : ↥L.lattice), ↑l ≠ l₀ → ‖z‖ < ‖↑l - x‖) →
    HasSum (fun i ↦ (L.weierstrassPExceptSeries l₀ x).coeff i * z ^ i) (℘[L - l₀] (x + z))
A : ∀ (l : ↥L.lattice), ↑l ≠ l₀ → ↑r < ‖↑l - x‖
⊢ HasSum (fun n ↦ (L.weierstrassPExceptSeries l₀ x n) fun x ↦ z) (℘[L - l₀] (x + z))

Tactic:
convert! this (fun l hl ↦ hz.trans (A l hl)) with i

Goal state after:
case e'_5
L : PeriodPair
l₀ x : ℂ
r : NNReal
hr0 : 0 < r
hr : Metric.closedBall x ↑r ⊆ (↑L.lattice \ {l₀})ᶜ
z : ℂ
hz : ‖z‖ < ↑r
this :
  (∀ (l : ↥L.lattice), ↑l ≠ l₀ → ‖z‖ < ‖↑l - x‖) →
    HasSum (fun i ↦ (L.weierstrassPExceptSeries l₀ x).coeff i * z ^ i) (℘[L - l₀] (x + z))
A : ∀ (l : ↥L.lattice), ↑l ≠ l₀ → ↑r < ‖↑l - x‖
i : ℕ
⊢ ((L.weierstrassPExceptSeries l₀ x i) fun x ↦ z) = (L.weierstrassPExceptSeries l₀ x).coeff i * z ^ i
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: L : PeriodPair
l : ℂ
⊢ HasFPowerSeriesAt ℘[L - l]
    (FormalMultilinearSeries.ofScalars ℂ fun i ↦ if i = 0 then ℘[L - l] l else (↑i + 1) * L.sumInvPow l (i + 2)) l

Tactic:
obtain ⟨r, h₁, h₂⟩ := Metric.nhds_basis_closedBall.mem_iff.mp
    (L.compl_lattice_sdiff_singleton_mem_nhds l)

Goal state after:
L : PeriodPair
l : ℂ
r : ℝ
h₁ : 0 < r
h₂ : Metric.closedBall l r ⊆ (↑L.lattice \ {l})ᶜ
⊢ HasFPowerSeriesAt ℘[L - l]
    (FormalMultilinearSeries.ofScalars ℂ fun i ↦ if i = 0 then ℘[L - l] l else (↑i + 1) * L.sumInvPow l (i + 2)) l
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: L : PeriodPair
l : ℂ
⊢ HasFPowerSeriesAt ℘'[L - l] (FormalMultilinearSeries.ofScalars ℂ fun i ↦ (↑i + 1) * (↑i + 2) * L.sumInvPow l (i + 3))
    l

Tactic:
obtain ⟨r, h₁, h₂⟩ := Metric.nhds_basis_closedBall.mem_iff.mp
    (L.compl_lattice_sdiff_singleton_mem_nhds l)

Goal state after:
L : PeriodPair
l : ℂ
r : ℝ
h₁ : 0 < r
h₂ : Metric.closedBall l r ⊆ (↑L.lattice \ {l})ᶜ
⊢ HasFPowerSeriesAt ℘'[L - l] (FormalMultilinearSeries.ofScalars ℂ fun i ↦ (↑i + 1) * (↑i + 2) * L.sumInvPow l (i + 3))
    l
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema

Goal state before:
pp: case mp
n : ℕ
hn : n ≠ 0
x : ℝ
⊢ eval x (T ℝ ↑n) = -1 → ∃ k ≤ n, Odd k ∧ x = cos (↑k * π / ↑n)

Tactic:
intro hx
    obtain ⟨k, hk₁, hk₂⟩ := (abs_eval_T_real_eq_one_iff hn x).mp
      ((abs_eq_abs.mpr (.inl hx)).trans ((abs_neg 1).trans abs_one))
    use k
    refine ⟨hk₁, ?_, hk₂⟩
    rw [hk₂, eval_T_real_cos_int_mul_pi_div hn, Int.cast_negOnePow_natCast] at hx
    exact (neg_one_pow_eq_neg_one_iff_odd (by grind)).mp hx

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

Goal state before:
pp: L : PeriodPair
x : ℂ
⊢ L.relation (-x) = L.relation x

Tactic:
classical simp [relation]

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

Goal state before:
pp: z : ℂ
h1 : cexp (z * I) + cexp (-z * I) = cexp (-(z * I)) * (cexp (2 * I * z) + 1)
h2 : cexp (-z * I) - cexp (z * I) = cexp (-(z * I)) * (1 - cexp (2 * I * z))
⊢ (cexp (z * I) + cexp (-z * I)) / 2 / ((cexp (-z * I) - cexp (z * I)) * I / 2) =
    (cexp (2 * I * z) + 1) / (I * (1 - cexp (2 * I * z)))

Tactic:
h1,

Goal state after:
z : ℂ
h1 : cexp (z * I) + cexp (-z * I) = cexp (-(z * I)) * (cexp (2 * I * z) + 1)
h2 : cexp (-z * I) - cexp (z * I) = cexp (-(z * I)) * (1 - cexp (2 * I * z))
⊢ cexp (-(z * I)) * (cexp (2 * I * z) + 1) / 2 / ((cexp (-z * I) - cexp (z * I)) * I / 2) =
    (cexp (2 * I * z) + 1) / (I * (1 - cexp (2 * I * z)))
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent

Goal state before:
pp: z : ℍ
h1 :
  ↑π * ((cexp (2 * ↑π * I * ↑z) + 1) / (I * (1 - cexp (2 * ↑π * I * ↑z)))) =
    -↑π * I * ((cexp (2 * ↑π * I * ↑z) + 1) * (1 / (1 - cexp (2 * ↑π * I * ↑z))))
⊢ ↑π * ((cexp (2 * ↑π * I * ↑z) + 1) / (I * (1 - cexp (2 * ↑π * I * ↑z)))) =
    ↑π * I - 2 * ↑π * I * ∑' (n : ℕ), cexp (2 * ↑π * I * ↑z) ^ n

Tactic:
h1,

Goal state after:
z : ℍ
h1 :
  ↑π * ((cexp (2 * ↑π * I * ↑z) + 1) / (I * (1 - cexp (2 * ↑π * I * ↑z)))) =
    -↑π * I * ((cexp (2 * ↑π * I * ↑z) + 1) * (1 / (1 - cexp (2 * ↑π * I * ↑z))))
⊢ -↑π * I * ((cexp (2 * ↑π * I * ↑z) + 1) * (1 / (1 - cexp (2 * ↑π * I * ↑z)))) =
    ↑π * I - 2 * ↑π * I * ∑' (n : ℕ), cexp (2 * ↑π * I * ↑z) ^ n
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent

Goal state before:
pp: case hg
k d : ℕ
z : ℂ
hz : z ∈ ℂ_ℤ
⊢ ContDiffAt ℂ (↑k) (fun z ↦ 1 / (z + (↑d + 1))) z

Tactic:
· simpa using (contDiffOn_inv_linear k (d + 1)).contDiffAt
      (isOpen_compl_range_intCast.mem_nhds hz)

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

Goal state before:
pp: n : ℤ
⊢ ↑(Int.fib n) = (φ ^ n - ψ ^ n) / √5

Tactic:
obtain ⟨n, (rfl | rfl)⟩ := n.eq_nat_or_neg
  · exact coe_fib_eq n
  · simp only [Int.fib_neg, Int.even_coe_nat, Int.fib_natCast, Int.cast_ite, Int.cast_neg,
      Int.cast_natCast, zpow_neg, zpow_natCast, ← inv_pow, inv_goldenRatio, inv_goldenConj,
      ← neg_one_mul ψ, ← neg_one_mul φ, mul_pow, neg_one_pow_eq_ite]
    grind [coe_fib_eq]

Goal state after: